%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SET888+1 : TPTP v9.3.1. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n004.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:44:55 PM UTC 2026
% Result : Theorem 23.88s 6.32s
% Output : Refutation 23.88s
% Verified :
% SZS Type : Refutation
% Derivation depth : 58
% Number of leaves : 12
% Syntax : Number of formulae : 137 ( 29 unt; 6 def)
% Number of atoms : 489 ( 356 equ)
% Maximal formula atoms : 14 ( 3 avg)
% Number of connectives : 459 ( 107 ~; 308 |; 34 &)
% ( 7 <=>; 2 =>; 0 <=; 1 <~>)
% Maximal formula depth : 11 ( 5 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 15 ( 15 usr; 8 con; 0-3 aty)
% Number of variables : 185 ( 178 !; 7 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f3,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] :
( X1 = singleton(X0)
<=> ! [X2] :
( in(X2,X1)
<=> X2 = X0 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d1_tarski) ).
fof(f6,axiom,
! [X0,X1,X2] :
( X2 = unordered_pair(X0,X1)
<=> ! [X3] :
( in(X3,X2)
<=> ( X3 = X0
| X3 = X1 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d2_tarski) ).
fof(f7,axiom,
! [X0,X1] : symmetric_difference(X0,X1) = set_union2(set_difference(X0,X1),set_difference(X1,X0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d6_xboole_0) ).
fof(f13,axiom,
! [X0,X1,X2] :
( in(X0,symmetric_difference(X1,X2))
<=> ~ ( in(X0,X1)
<=> in(X0,X2) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t1_xboole_0) ).
fof(f14,conjecture,
! [X0,X1] :
( X0 != X1
=> symmetric_difference(singleton(X0),singleton(X1)) = unordered_pair(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t29_zfmisc_1) ).
fof(f15,negated_conjecture,
~ ! [X0,X1] :
( X0 != X1
=> symmetric_difference(singleton(X0),singleton(X1)) = unordered_pair(X0,X1) ),
inference(negated_conjecture,[status(cth)],[f14]) ).
fof(f20,plain,
! [X0,X1,X2] :
( in(X0,symmetric_difference(X1,X2))
<=> ( in(X0,X1)
<~> in(X0,X2) ) ),
inference(ennf_transformation,[],[f13]) ).
fof(f21,plain,
? [X0,X1] :
( unordered_pair(X0,X1) != symmetric_difference(singleton(X0),singleton(X1))
& X0 != X1 ),
inference(ennf_transformation,[],[f15]) ).
fof(f22,plain,
! [X0,X1] :
( ( X1 = singleton(X0)
| ? [X2] :
( ( X0 != X2
| ~ in(X2,X1) )
& ( X2 = X0
| in(X2,X1) ) ) )
& ( ! [X2] :
( ( in(X2,X1)
| X0 != X2 )
& ( X2 = X0
| ~ in(X2,X1) ) )
| singleton(X0) != X1 ) ),
inference(nnf_transformation,[],[f5]) ).
fof(f23,plain,
! [X0,X1] :
( ( X1 = singleton(X0)
| ? [X2] :
( ( X0 != X2
| ~ in(X2,X1) )
& ( X2 = X0
| in(X2,X1) ) ) )
& ( ! [X3] :
( ( in(X3,X1)
| X0 != X3 )
& ( X0 = X3
| ~ in(X3,X1) ) )
| singleton(X0) != X1 ) ),
inference(rectify,[],[f22]) ).
fof(f24,plain,
! [X0,X1] :
( ( X1 = singleton(X0)
| ( ( sK0(X0,X1) != X0
| ~ in(sK0(X0,X1),X1) )
& ( sK0(X0,X1) = X0
| in(sK0(X0,X1),X1) ) ) )
& ( ! [X3] :
( ( in(X3,X1)
| X0 != X3 )
& ( X0 = X3
| ~ in(X3,X1) ) )
| singleton(X0) != X1 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0]),skolemize(X2,sK0(X0,X1))],[f23]) ).
fof(f25,plain,
! [X0,X1,X2] :
( ( X2 = unordered_pair(X0,X1)
| ? [X3] :
( ( ( X0 != X3
& X1 != X3 )
| ~ in(X3,X2) )
& ( X3 = X0
| X3 = X1
| in(X3,X2) ) ) )
& ( ! [X3] :
( ( in(X3,X2)
| ( X0 != X3
& X1 != X3 ) )
& ( X3 = X0
| X3 = X1
| ~ in(X3,X2) ) )
| unordered_pair(X0,X1) != X2 ) ),
inference(nnf_transformation,[],[f6]) ).
fof(f26,plain,
! [X0,X1,X2] :
( ( X2 = unordered_pair(X0,X1)
| ? [X3] :
( ( ( X0 != X3
& X1 != X3 )
| ~ in(X3,X2) )
& ( X3 = X0
| X3 = X1
| in(X3,X2) ) ) )
& ( ! [X3] :
( ( in(X3,X2)
| ( X0 != X3
& X1 != X3 ) )
& ( X3 = X0
| X3 = X1
| ~ in(X3,X2) ) )
| unordered_pair(X0,X1) != X2 ) ),
inference(flattening,[],[f25]) ).
fof(f27,plain,
! [X0,X1,X2] :
( ( X2 = unordered_pair(X0,X1)
| ? [X3] :
( ( ( X0 != X3
& X1 != X3 )
| ~ in(X3,X2) )
& ( X3 = X0
| X3 = X1
| in(X3,X2) ) ) )
& ( ! [X4] :
( ( in(X4,X2)
| ( X0 != X4
& X1 != X4 ) )
& ( X0 = X4
| X1 = X4
| ~ in(X4,X2) ) )
| unordered_pair(X0,X1) != X2 ) ),
inference(rectify,[],[f26]) ).
fof(f28,plain,
! [X0,X1,X2] :
( ( X2 = unordered_pair(X0,X1)
| ( ( ( sK1(X0,X1,X2) != X0
& sK1(X0,X1,X2) != X1 )
| ~ in(sK1(X0,X1,X2),X2) )
& ( sK1(X0,X1,X2) = X0
| sK1(X0,X1,X2) = X1
| in(sK1(X0,X1,X2),X2) ) ) )
& ( ! [X4] :
( ( in(X4,X2)
| ( X0 != X4
& X1 != X4 ) )
& ( X0 = X4
| X1 = X4
| ~ in(X4,X2) ) )
| unordered_pair(X0,X1) != X2 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1]),skolemize(X3,sK1(X0,X1,X2))],[f27]) ).
fof(f31,plain,
! [X0,X1,X2] :
( ( in(X0,symmetric_difference(X1,X2))
| ( ( in(X0,X1)
| ~ in(X0,X2) )
& ( in(X0,X2)
| ~ in(X0,X1) ) ) )
& ( ( ( ~ in(X0,X2)
| ~ in(X0,X1) )
& ( in(X0,X2)
| in(X0,X1) ) )
| ~ in(X0,symmetric_difference(X1,X2)) ) ),
inference(nnf_transformation,[],[f20]) ).
fof(f32,plain,
( unordered_pair(sK4,sK5) != symmetric_difference(singleton(sK4),singleton(sK5))
& sK4 != sK5 ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4,sK5]),skolemize(X0,sK4),skolemize(X1,sK5)],[f21]) ).
fof(f35,plain,
! [X0,X1] : set_union2(X0,X1) = set_union2(X1,X0),
inference(cnf_transformation,[],[f3]) ).
fof(f37,plain,
! [X3,X0,X1] :
( X0 = X3
| ~ in(X3,X1)
| singleton(X0) != X1 ),
inference(cnf_transformation,[],[f24]) ).
fof(f38,plain,
! [X3,X0,X1] :
( in(X3,X1)
| X0 != X3
| singleton(X0) != X1 ),
inference(cnf_transformation,[],[f24]) ).
fof(f39,plain,
! [X0,X1] :
( in(sK0(X0,X1),X1)
| sK0(X0,X1) = X0
| singleton(X0) = X1 ),
inference(cnf_transformation,[],[f24]) ).
fof(f40,plain,
! [X0,X1] :
( sK0(X0,X1) != X0
| singleton(X0) = X1
| ~ in(sK0(X0,X1),X1) ),
inference(cnf_transformation,[],[f24]) ).
fof(f44,plain,
! [X2,X0,X1] :
( in(sK1(X0,X1,X2),X2)
| sK1(X0,X1,X2) = X0
| sK1(X0,X1,X2) = X1
| unordered_pair(X0,X1) = X2 ),
inference(cnf_transformation,[],[f28]) ).
fof(f45,plain,
! [X2,X0,X1] :
( sK1(X0,X1,X2) != X1
| unordered_pair(X0,X1) = X2
| ~ in(sK1(X0,X1,X2),X2) ),
inference(cnf_transformation,[],[f28]) ).
fof(f46,plain,
! [X2,X0,X1] :
( sK1(X0,X1,X2) != X0
| unordered_pair(X0,X1) = X2
| ~ in(sK1(X0,X1,X2),X2) ),
inference(cnf_transformation,[],[f28]) ).
fof(f47,plain,
! [X0,X1] : symmetric_difference(X0,X1) = set_union2(set_difference(X0,X1),set_difference(X1,X0)),
inference(cnf_transformation,[],[f7]) ).
fof(f53,plain,
! [X2,X0,X1] :
( in(X0,X2)
| in(X0,X1)
| ~ in(X0,symmetric_difference(X1,X2)) ),
inference(cnf_transformation,[],[f31]) ).
fof(f56,plain,
! [X2,X0,X1] :
( in(X0,symmetric_difference(X1,X2))
| in(X0,X1)
| ~ in(X0,X2) ),
inference(cnf_transformation,[],[f31]) ).
fof(f57,plain,
sK4 != sK5,
inference(cnf_transformation,[],[f32]) ).
fof(f58,plain,
unordered_pair(sK4,sK5) != symmetric_difference(singleton(sK4),singleton(sK5)),
inference(cnf_transformation,[],[f32]) ).
fof(f60,plain,
! [X2,X0,X1] :
( in(X0,set_union2(set_difference(X1,X2),set_difference(X2,X1)))
| in(X0,X1)
| ~ in(X0,X2) ),
inference(definition_unfolding,[],[f56,f47]) ).
fof(f63,plain,
! [X2,X0,X1] :
( ~ in(X0,set_union2(set_difference(X1,X2),set_difference(X2,X1)))
| in(X0,X1)
| in(X0,X2) ),
inference(definition_unfolding,[],[f53,f47]) ).
fof(f64,plain,
unordered_pair(sK4,sK5) != set_union2(set_difference(singleton(sK4),singleton(sK5)),set_difference(singleton(sK5),singleton(sK4))),
inference(definition_unfolding,[],[f58,f47]) ).
fof(f65,plain,
! [X3,X1] :
( in(X3,X1)
| singleton(X3) != X1 ),
inference(equality_resolution,[],[f38]) ).
fof(f66,plain,
! [X3] : in(X3,singleton(X3)),
inference(equality_resolution,[],[f65]) ).
fof(f67,plain,
! [X3,X0] :
( ~ in(X3,singleton(X0))
| X0 = X3 ),
inference(equality_resolution,[],[f37]) ).
fof(f73,definition,
sF6 = unordered_pair(sK4,sK5),
introduced(definition,[new_symbols(definition,[sF6])],[function_definition]) ).
fof(f74,plain,
unordered_pair(sK4,sK5) = sF6,
inference(reorient_equations,[],[f73]) ).
fof(f75,definition,
sF7 = singleton(sK4),
introduced(definition,[new_symbols(definition,[sF7])],[function_definition]) ).
fof(f76,plain,
singleton(sK4) = sF7,
inference(reorient_equations,[],[f75]) ).
fof(f77,definition,
sF8 = singleton(sK5),
introduced(definition,[new_symbols(definition,[sF8])],[function_definition]) ).
fof(f78,plain,
singleton(sK5) = sF8,
inference(reorient_equations,[],[f77]) ).
fof(f79,definition,
sF9 = set_difference(sF7,sF8),
introduced(definition,[new_symbols(definition,[sF9])],[function_definition]) ).
fof(f80,plain,
set_difference(sF7,sF8) = sF9,
inference(reorient_equations,[],[f79]) ).
fof(f81,definition,
sF10 = set_difference(sF8,sF7),
introduced(definition,[new_symbols(definition,[sF10])],[function_definition]) ).
fof(f82,plain,
set_difference(sF8,sF7) = sF10,
inference(reorient_equations,[],[f81]) ).
fof(f83,definition,
sF11 = set_union2(sF9,sF10),
introduced(definition,[new_symbols(definition,[sF11])],[function_definition]) ).
fof(f84,plain,
set_union2(sF9,sF10) = sF11,
inference(reorient_equations,[],[f83]) ).
fof(f85,plain,
sF6 != sF11,
inference(definition_folding,[],[f64,f84,f82,f76,f78,f80,f78,f76,f74]) ).
fof(f86,plain,
in(sK4,sF7),
inference(superposition,[],[f66,f76]) ).
fof(f87,plain,
in(sK5,sF8),
inference(superposition,[],[f66,f78]) ).
fof(f110,plain,
! [X0] :
( ~ in(X0,sF7)
| sK4 = X0 ),
inference(superposition,[],[f67,f76]) ).
fof(f111,plain,
! [X0] :
( ~ in(X0,sF8)
| sK5 = X0 ),
inference(superposition,[],[f67,f78]) ).
fof(f140,plain,
! [X0] :
( in(X0,set_union2(sF9,set_difference(sF8,sF7)))
| in(X0,sF7)
| ~ in(X0,sF8) ),
inference(superposition,[],[f60,f80]) ).
fof(f142,plain,
! [X0] :
( in(X0,set_union2(set_difference(sF8,sF7),sF9))
| in(X0,sF8)
| ~ in(X0,sF7) ),
inference(superposition,[],[f60,f80]) ).
fof(f150,plain,
! [X0] :
( in(X0,set_union2(sF9,set_difference(sF8,sF7)))
| in(X0,sF8)
| ~ in(X0,sF7) ),
inference(forward_demodulation,[],[f142,f35]) ).
fof(f152,plain,
! [X0] :
( in(X0,set_union2(sF9,sF10))
| in(X0,sF7)
| ~ in(X0,sF8) ),
inference(forward_demodulation,[],[f140,f82]) ).
fof(f154,plain,
! [X0] :
( in(X0,set_union2(sF9,sF10))
| in(X0,sF8)
| ~ in(X0,sF7) ),
inference(forward_demodulation,[],[f150,f82]) ).
fof(f156,plain,
! [X0] :
( ~ in(X0,sF8)
| in(X0,sF7)
| in(X0,sF11) ),
inference(forward_demodulation,[],[f152,f84]) ).
fof(f158,plain,
! [X0] :
( ~ in(X0,sF7)
| in(X0,sF8)
| in(X0,sF11) ),
inference(forward_demodulation,[],[f154,f84]) ).
fof(f221,plain,
! [X0] :
( ~ in(X0,set_union2(sF9,set_difference(sF8,sF7)))
| in(X0,sF7)
| in(X0,sF8) ),
inference(superposition,[],[f63,f80]) ).
fof(f237,plain,
! [X0] :
( ~ in(X0,set_union2(sF9,sF10))
| in(X0,sF7)
| in(X0,sF8) ),
inference(forward_demodulation,[],[f221,f82]) ).
fof(f241,plain,
! [X0] :
( ~ in(X0,sF11)
| in(X0,sF7)
| in(X0,sF8) ),
inference(forward_demodulation,[],[f237,f84]) ).
fof(f251,plain,
( in(sK5,sF11)
| in(sK5,sF7) ),
inference(resolution,[],[f156,f87]) ).
fof(f254,plain,
! [X2,X3,X0,X1] :
( in(sK1(X0,X1,set_union2(set_difference(X2,X3),set_difference(X3,X2))),X3)
| in(sK1(X0,X1,set_union2(set_difference(X2,X3),set_difference(X3,X2))),X2)
| unordered_pair(X0,X1) = set_union2(set_difference(X2,X3),set_difference(X3,X2))
| sK1(X0,X1,set_union2(set_difference(X2,X3),set_difference(X3,X2))) = X1
| sK1(X0,X1,set_union2(set_difference(X2,X3),set_difference(X3,X2))) = X0 ),
inference(resolution,[],[f44,f63]) ).
fof(f266,plain,
( in(sK4,sF11)
| in(sK4,sF8) ),
inference(resolution,[],[f158,f86]) ).
fof(f272,plain,
! [X0] :
( in(sK0(X0,sF11),sF8)
| in(sK0(X0,sF11),sF7)
| sK0(X0,sF11) = X0
| singleton(X0) = sF11 ),
inference(resolution,[],[f241,f39]) ).
fof(f706,plain,
! [X2,X0,X1] :
( in(sK1(X0,X1,set_union2(set_difference(X2,sF7),set_difference(sF7,X2))),X2)
| unordered_pair(X0,X1) = set_union2(set_difference(X2,sF7),set_difference(sF7,X2))
| sK1(X0,X1,set_union2(set_difference(X2,sF7),set_difference(sF7,X2))) = X1
| sK1(X0,X1,set_union2(set_difference(X2,sF7),set_difference(sF7,X2))) = X0
| sK4 = sK1(X0,X1,set_union2(set_difference(X2,sF7),set_difference(sF7,X2))) ),
inference(resolution,[],[f254,f110]) ).
fof(f1027,plain,
! [X0] :
( in(sK0(X0,sF11),sF7)
| sK0(X0,sF11) = X0
| singleton(X0) = sF11
| sK5 = sK0(X0,sF11) ),
inference(resolution,[],[f272,f111]) ).
fof(f1199,plain,
! [X0] :
( sK5 = sK0(X0,sF11)
| sK0(X0,sF11) = X0
| singleton(X0) = sF11
| sK4 = sK0(X0,sF11) ),
inference(resolution,[],[f1027,f110]) ).
fof(f1282,plain,
! [X0] :
( sK5 != X0
| sK0(X0,sF11) = X0
| singleton(X0) = sF11
| sK4 = sK0(X0,sF11) ),
inference(equality_factoring,[],[f1199]) ).
fof(f1310,plain,
( sK5 = sK0(sK5,sF11)
| singleton(sK5) = sF11
| sK4 = sK0(sK5,sF11) ),
inference(equality_resolution,[],[f1282]) ).
fof(f1311,plain,
( sK5 = sK0(sK5,sF11)
| sF8 = sF11
| sK4 = sK0(sK5,sF11) ),
inference(forward_demodulation,[],[f1310,f78]) ).
fof(f1336,plain,
( sK5 != sK5
| singleton(sK5) = sF11
| ~ in(sK5,sF11)
| sF8 = sF11
| sK4 = sK0(sK5,sF11) ),
inference(superposition,[],[f40,f1311]) ).
fof(f1338,plain,
( singleton(sK5) = sF11
| ~ in(sK5,sF11)
| sF8 = sF11
| sK4 = sK0(sK5,sF11) ),
inference(trivial_inequality_removal,[],[f1336]) ).
fof(f1339,plain,
( sF8 = sF11
| ~ in(sK5,sF11)
| sF8 = sF11
| sK4 = sK0(sK5,sF11) ),
inference(forward_demodulation,[],[f1338,f78]) ).
fof(f1340,plain,
( ~ in(sK5,sF11)
| sF8 = sF11
| sK4 = sK0(sK5,sF11) ),
inference(duplicate_literal_removal,[],[f1339]) ).
fof(f1365,plain,
( in(sK5,sF7)
| sK4 = sK0(sK5,sF11)
| sF8 = sF11 ),
inference(resolution,[],[f1340,f251]) ).
fof(f1369,plain,
( sK4 = sK0(sK5,sF11)
| sF8 = sF11
| sK4 = sK5 ),
inference(resolution,[],[f1365,f110]) ).
fof(f1371,plain,
( sK4 = sK0(sK5,sF11)
| sF8 = sF11 ),
inference(forward_subsumption_resolution,[],[f1369,f57]) ).
fof(f1382,plain,
( in(sK4,sF11)
| sK4 = sK5
| singleton(sK5) = sF11
| sF8 = sF11 ),
inference(superposition,[],[f39,f1371]) ).
fof(f1385,plain,
( in(sK4,sF11)
| singleton(sK5) = sF11
| sF8 = sF11 ),
inference(forward_subsumption_resolution,[],[f1382,f57]) ).
fof(f1387,plain,
( sF8 = sF11
| in(sK4,sF11)
| sF8 = sF11 ),
inference(forward_demodulation,[],[f1385,f78]) ).
fof(f1388,plain,
( in(sK4,sF11)
| sF8 = sF11 ),
inference(duplicate_literal_removal,[],[f1387]) ).
fof(f4917,plain,
! [X0,X1] :
( unordered_pair(X0,X1) = set_union2(set_difference(sF8,sF7),set_difference(sF7,sF8))
| sK1(X0,X1,set_union2(set_difference(sF8,sF7),set_difference(sF7,sF8))) = X1
| sK1(X0,X1,set_union2(set_difference(sF8,sF7),set_difference(sF7,sF8))) = X0
| sK4 = sK1(X0,X1,set_union2(set_difference(sF8,sF7),set_difference(sF7,sF8)))
| sK5 = sK1(X0,X1,set_union2(set_difference(sF8,sF7),set_difference(sF7,sF8))) ),
inference(resolution,[],[f706,f111]) ).
fof(f4935,plain,
! [X0,X1] :
( unordered_pair(X0,X1) = set_union2(set_difference(sF7,sF8),set_difference(sF8,sF7))
| sK1(X0,X1,set_union2(set_difference(sF8,sF7),set_difference(sF7,sF8))) = X1
| sK1(X0,X1,set_union2(set_difference(sF8,sF7),set_difference(sF7,sF8))) = X0
| sK4 = sK1(X0,X1,set_union2(set_difference(sF8,sF7),set_difference(sF7,sF8)))
| sK5 = sK1(X0,X1,set_union2(set_difference(sF8,sF7),set_difference(sF7,sF8))) ),
inference(forward_demodulation,[],[f4917,f35]) ).
fof(f4969,plain,
! [X0,X1] :
( unordered_pair(X0,X1) = set_union2(set_difference(sF7,sF8),sF10)
| sK1(X0,X1,set_union2(set_difference(sF8,sF7),set_difference(sF7,sF8))) = X1
| sK1(X0,X1,set_union2(set_difference(sF8,sF7),set_difference(sF7,sF8))) = X0
| sK4 = sK1(X0,X1,set_union2(set_difference(sF8,sF7),set_difference(sF7,sF8)))
| sK5 = sK1(X0,X1,set_union2(set_difference(sF8,sF7),set_difference(sF7,sF8))) ),
inference(forward_demodulation,[],[f4935,f82]) ).
fof(f5003,plain,
! [X0,X1] :
( unordered_pair(X0,X1) = set_union2(sF10,set_difference(sF7,sF8))
| sK1(X0,X1,set_union2(set_difference(sF8,sF7),set_difference(sF7,sF8))) = X1
| sK1(X0,X1,set_union2(set_difference(sF8,sF7),set_difference(sF7,sF8))) = X0
| sK4 = sK1(X0,X1,set_union2(set_difference(sF8,sF7),set_difference(sF7,sF8)))
| sK5 = sK1(X0,X1,set_union2(set_difference(sF8,sF7),set_difference(sF7,sF8))) ),
inference(forward_demodulation,[],[f4969,f35]) ).
fof(f5037,plain,
! [X0,X1] :
( unordered_pair(X0,X1) = set_union2(sF10,sF9)
| sK1(X0,X1,set_union2(set_difference(sF8,sF7),set_difference(sF7,sF8))) = X1
| sK1(X0,X1,set_union2(set_difference(sF8,sF7),set_difference(sF7,sF8))) = X0
| sK4 = sK1(X0,X1,set_union2(set_difference(sF8,sF7),set_difference(sF7,sF8)))
| sK5 = sK1(X0,X1,set_union2(set_difference(sF8,sF7),set_difference(sF7,sF8))) ),
inference(forward_demodulation,[],[f5003,f80]) ).
fof(f5067,plain,
! [X0,X1] :
( unordered_pair(X0,X1) = set_union2(sF9,sF10)
| sK1(X0,X1,set_union2(set_difference(sF8,sF7),set_difference(sF7,sF8))) = X1
| sK1(X0,X1,set_union2(set_difference(sF8,sF7),set_difference(sF7,sF8))) = X0
| sK4 = sK1(X0,X1,set_union2(set_difference(sF8,sF7),set_difference(sF7,sF8)))
| sK5 = sK1(X0,X1,set_union2(set_difference(sF8,sF7),set_difference(sF7,sF8))) ),
inference(forward_demodulation,[],[f5037,f35]) ).
fof(f5089,plain,
! [X0,X1] :
( unordered_pair(X0,X1) = sF11
| sK1(X0,X1,set_union2(set_difference(sF8,sF7),set_difference(sF7,sF8))) = X1
| sK1(X0,X1,set_union2(set_difference(sF8,sF7),set_difference(sF7,sF8))) = X0
| sK4 = sK1(X0,X1,set_union2(set_difference(sF8,sF7),set_difference(sF7,sF8)))
| sK5 = sK1(X0,X1,set_union2(set_difference(sF8,sF7),set_difference(sF7,sF8))) ),
inference(forward_demodulation,[],[f5067,f84]) ).
fof(f5107,plain,
! [X0,X1] :
( sK1(X0,X1,set_union2(set_difference(sF7,sF8),set_difference(sF8,sF7))) = X1
| unordered_pair(X0,X1) = sF11
| sK1(X0,X1,set_union2(set_difference(sF8,sF7),set_difference(sF7,sF8))) = X0
| sK4 = sK1(X0,X1,set_union2(set_difference(sF8,sF7),set_difference(sF7,sF8)))
| sK5 = sK1(X0,X1,set_union2(set_difference(sF8,sF7),set_difference(sF7,sF8))) ),
inference(forward_demodulation,[],[f5089,f35]) ).
fof(f5120,plain,
! [X0,X1] :
( sK1(X0,X1,set_union2(set_difference(sF7,sF8),sF10)) = X1
| unordered_pair(X0,X1) = sF11
| sK1(X0,X1,set_union2(set_difference(sF8,sF7),set_difference(sF7,sF8))) = X0
| sK4 = sK1(X0,X1,set_union2(set_difference(sF8,sF7),set_difference(sF7,sF8)))
| sK5 = sK1(X0,X1,set_union2(set_difference(sF8,sF7),set_difference(sF7,sF8))) ),
inference(forward_demodulation,[],[f5107,f82]) ).
fof(f5129,plain,
! [X0,X1] :
( sK1(X0,X1,set_union2(sF10,set_difference(sF7,sF8))) = X1
| unordered_pair(X0,X1) = sF11
| sK1(X0,X1,set_union2(set_difference(sF8,sF7),set_difference(sF7,sF8))) = X0
| sK4 = sK1(X0,X1,set_union2(set_difference(sF8,sF7),set_difference(sF7,sF8)))
| sK5 = sK1(X0,X1,set_union2(set_difference(sF8,sF7),set_difference(sF7,sF8))) ),
inference(forward_demodulation,[],[f5120,f35]) ).
fof(f5136,plain,
! [X0,X1] :
( sK1(X0,X1,set_union2(sF10,sF9)) = X1
| unordered_pair(X0,X1) = sF11
| sK1(X0,X1,set_union2(set_difference(sF8,sF7),set_difference(sF7,sF8))) = X0
| sK4 = sK1(X0,X1,set_union2(set_difference(sF8,sF7),set_difference(sF7,sF8)))
| sK5 = sK1(X0,X1,set_union2(set_difference(sF8,sF7),set_difference(sF7,sF8))) ),
inference(forward_demodulation,[],[f5129,f80]) ).
fof(f5143,plain,
! [X0,X1] :
( sK1(X0,X1,set_union2(sF9,sF10)) = X1
| unordered_pair(X0,X1) = sF11
| sK1(X0,X1,set_union2(set_difference(sF8,sF7),set_difference(sF7,sF8))) = X0
| sK4 = sK1(X0,X1,set_union2(set_difference(sF8,sF7),set_difference(sF7,sF8)))
| sK5 = sK1(X0,X1,set_union2(set_difference(sF8,sF7),set_difference(sF7,sF8))) ),
inference(forward_demodulation,[],[f5136,f35]) ).
fof(f5150,plain,
! [X0,X1] :
( sK1(X0,X1,sF11) = X1
| unordered_pair(X0,X1) = sF11
| sK1(X0,X1,set_union2(set_difference(sF8,sF7),set_difference(sF7,sF8))) = X0
| sK4 = sK1(X0,X1,set_union2(set_difference(sF8,sF7),set_difference(sF7,sF8)))
| sK5 = sK1(X0,X1,set_union2(set_difference(sF8,sF7),set_difference(sF7,sF8))) ),
inference(forward_demodulation,[],[f5143,f84]) ).
fof(f5157,plain,
! [X0,X1] :
( sK1(X0,X1,set_union2(set_difference(sF7,sF8),set_difference(sF8,sF7))) = X0
| sK1(X0,X1,sF11) = X1
| unordered_pair(X0,X1) = sF11
| sK4 = sK1(X0,X1,set_union2(set_difference(sF8,sF7),set_difference(sF7,sF8)))
| sK5 = sK1(X0,X1,set_union2(set_difference(sF8,sF7),set_difference(sF7,sF8))) ),
inference(forward_demodulation,[],[f5150,f35]) ).
fof(f5164,plain,
! [X0,X1] :
( sK1(X0,X1,set_union2(set_difference(sF7,sF8),sF10)) = X0
| sK1(X0,X1,sF11) = X1
| unordered_pair(X0,X1) = sF11
| sK4 = sK1(X0,X1,set_union2(set_difference(sF8,sF7),set_difference(sF7,sF8)))
| sK5 = sK1(X0,X1,set_union2(set_difference(sF8,sF7),set_difference(sF7,sF8))) ),
inference(forward_demodulation,[],[f5157,f82]) ).
fof(f5171,plain,
! [X0,X1] :
( sK1(X0,X1,set_union2(sF10,set_difference(sF7,sF8))) = X0
| sK1(X0,X1,sF11) = X1
| unordered_pair(X0,X1) = sF11
| sK4 = sK1(X0,X1,set_union2(set_difference(sF8,sF7),set_difference(sF7,sF8)))
| sK5 = sK1(X0,X1,set_union2(set_difference(sF8,sF7),set_difference(sF7,sF8))) ),
inference(forward_demodulation,[],[f5164,f35]) ).
fof(f5176,plain,
! [X0,X1] :
( sK1(X0,X1,set_union2(sF10,sF9)) = X0
| sK1(X0,X1,sF11) = X1
| unordered_pair(X0,X1) = sF11
| sK4 = sK1(X0,X1,set_union2(set_difference(sF8,sF7),set_difference(sF7,sF8)))
| sK5 = sK1(X0,X1,set_union2(set_difference(sF8,sF7),set_difference(sF7,sF8))) ),
inference(forward_demodulation,[],[f5171,f80]) ).
fof(f5181,plain,
! [X0,X1] :
( sK1(X0,X1,set_union2(sF9,sF10)) = X0
| sK1(X0,X1,sF11) = X1
| unordered_pair(X0,X1) = sF11
| sK4 = sK1(X0,X1,set_union2(set_difference(sF8,sF7),set_difference(sF7,sF8)))
| sK5 = sK1(X0,X1,set_union2(set_difference(sF8,sF7),set_difference(sF7,sF8))) ),
inference(forward_demodulation,[],[f5176,f35]) ).
fof(f5186,plain,
! [X0,X1] :
( sK1(X0,X1,sF11) = X0
| sK1(X0,X1,sF11) = X1
| unordered_pair(X0,X1) = sF11
| sK4 = sK1(X0,X1,set_union2(set_difference(sF8,sF7),set_difference(sF7,sF8)))
| sK5 = sK1(X0,X1,set_union2(set_difference(sF8,sF7),set_difference(sF7,sF8))) ),
inference(forward_demodulation,[],[f5181,f84]) ).
fof(f5191,plain,
! [X0,X1] :
( sK4 = sK1(X0,X1,set_union2(set_difference(sF7,sF8),set_difference(sF8,sF7)))
| sK1(X0,X1,sF11) = X0
| sK1(X0,X1,sF11) = X1
| unordered_pair(X0,X1) = sF11
| sK5 = sK1(X0,X1,set_union2(set_difference(sF8,sF7),set_difference(sF7,sF8))) ),
inference(forward_demodulation,[],[f5186,f35]) ).
fof(f5196,plain,
! [X0,X1] :
( sK4 = sK1(X0,X1,set_union2(set_difference(sF7,sF8),sF10))
| sK1(X0,X1,sF11) = X0
| sK1(X0,X1,sF11) = X1
| unordered_pair(X0,X1) = sF11
| sK5 = sK1(X0,X1,set_union2(set_difference(sF8,sF7),set_difference(sF7,sF8))) ),
inference(forward_demodulation,[],[f5191,f82]) ).
fof(f5201,plain,
! [X0,X1] :
( sK4 = sK1(X0,X1,set_union2(sF10,set_difference(sF7,sF8)))
| sK1(X0,X1,sF11) = X0
| sK1(X0,X1,sF11) = X1
| unordered_pair(X0,X1) = sF11
| sK5 = sK1(X0,X1,set_union2(set_difference(sF8,sF7),set_difference(sF7,sF8))) ),
inference(forward_demodulation,[],[f5196,f35]) ).
fof(f5206,plain,
! [X0,X1] :
( sK4 = sK1(X0,X1,set_union2(sF10,sF9))
| sK1(X0,X1,sF11) = X0
| sK1(X0,X1,sF11) = X1
| unordered_pair(X0,X1) = sF11
| sK5 = sK1(X0,X1,set_union2(set_difference(sF8,sF7),set_difference(sF7,sF8))) ),
inference(forward_demodulation,[],[f5201,f80]) ).
fof(f5211,plain,
! [X0,X1] :
( sK4 = sK1(X0,X1,set_union2(sF9,sF10))
| sK1(X0,X1,sF11) = X0
| sK1(X0,X1,sF11) = X1
| unordered_pair(X0,X1) = sF11
| sK5 = sK1(X0,X1,set_union2(set_difference(sF8,sF7),set_difference(sF7,sF8))) ),
inference(forward_demodulation,[],[f5206,f35]) ).
fof(f5216,plain,
! [X0,X1] :
( sK4 = sK1(X0,X1,sF11)
| sK1(X0,X1,sF11) = X0
| sK1(X0,X1,sF11) = X1
| unordered_pair(X0,X1) = sF11
| sK5 = sK1(X0,X1,set_union2(set_difference(sF8,sF7),set_difference(sF7,sF8))) ),
inference(forward_demodulation,[],[f5211,f84]) ).
fof(f5221,plain,
! [X0,X1] :
( sK5 = sK1(X0,X1,set_union2(set_difference(sF7,sF8),set_difference(sF8,sF7)))
| sK4 = sK1(X0,X1,sF11)
| sK1(X0,X1,sF11) = X0
| sK1(X0,X1,sF11) = X1
| unordered_pair(X0,X1) = sF11 ),
inference(forward_demodulation,[],[f5216,f35]) ).
fof(f5226,plain,
! [X0,X1] :
( sK5 = sK1(X0,X1,set_union2(set_difference(sF7,sF8),sF10))
| sK4 = sK1(X0,X1,sF11)
| sK1(X0,X1,sF11) = X0
| sK1(X0,X1,sF11) = X1
| unordered_pair(X0,X1) = sF11 ),
inference(forward_demodulation,[],[f5221,f82]) ).
fof(f5231,plain,
! [X0,X1] :
( sK5 = sK1(X0,X1,set_union2(sF10,set_difference(sF7,sF8)))
| sK4 = sK1(X0,X1,sF11)
| sK1(X0,X1,sF11) = X0
| sK1(X0,X1,sF11) = X1
| unordered_pair(X0,X1) = sF11 ),
inference(forward_demodulation,[],[f5226,f35]) ).
fof(f5236,plain,
! [X0,X1] :
( sK5 = sK1(X0,X1,set_union2(sF10,sF9))
| sK4 = sK1(X0,X1,sF11)
| sK1(X0,X1,sF11) = X0
| sK1(X0,X1,sF11) = X1
| unordered_pair(X0,X1) = sF11 ),
inference(forward_demodulation,[],[f5231,f80]) ).
fof(f5241,plain,
! [X0,X1] :
( sK5 = sK1(X0,X1,set_union2(sF9,sF10))
| sK4 = sK1(X0,X1,sF11)
| sK1(X0,X1,sF11) = X0
| sK1(X0,X1,sF11) = X1
| unordered_pair(X0,X1) = sF11 ),
inference(forward_demodulation,[],[f5236,f35]) ).
fof(f5246,plain,
! [X0,X1] :
( sK5 = sK1(X0,X1,sF11)
| sK1(X0,X1,sF11) = X1
| sK1(X0,X1,sF11) = X0
| sK4 = sK1(X0,X1,sF11)
| unordered_pair(X0,X1) = sF11 ),
inference(forward_demodulation,[],[f5241,f84]) ).
fof(f16240,plain,
! [X0,X1] :
( sK5 != X1
| sK1(X0,X1,sF11) = X1
| sK1(X0,X1,sF11) = X0
| sK4 = sK1(X0,X1,sF11)
| unordered_pair(X0,X1) = sF11 ),
inference(equality_factoring,[],[f5246]) ).
fof(f28149,plain,
! [X0] :
( sK5 = sK1(X0,sK5,sF11)
| sK1(X0,sK5,sF11) = X0
| sK4 = sK1(X0,sK5,sF11)
| sF11 = unordered_pair(X0,sK5) ),
inference(equality_resolution,[],[f16240]) ).
fof(f28543,plain,
! [X0] :
( sK4 != X0
| sK5 = sK1(X0,sK5,sF11)
| sK4 = sK1(X0,sK5,sF11)
| sF11 = unordered_pair(X0,sK5) ),
inference(equality_factoring,[],[f28149]) ).
fof(f29390,plain,
( sK5 = sK1(sK4,sK5,sF11)
| sK4 = sK1(sK4,sK5,sF11)
| unordered_pair(sK4,sK5) = sF11 ),
inference(equality_resolution,[],[f28543]) ).
fof(f29391,plain,
( sF6 = sF11
| sK5 = sK1(sK4,sK5,sF11)
| sK4 = sK1(sK4,sK5,sF11) ),
inference(forward_demodulation,[],[f29390,f74]) ).
fof(f29392,plain,
( sK5 = sK1(sK4,sK5,sF11)
| sK4 = sK1(sK4,sK5,sF11) ),
inference(forward_subsumption_resolution,[],[f29391,f85]) ).
fof(f29399,plain,
( sK5 != sK5
| unordered_pair(sK4,sK5) = sF11
| ~ in(sK5,sF11)
| sK4 = sK1(sK4,sK5,sF11) ),
inference(superposition,[],[f45,f29392]) ).
fof(f29401,plain,
( unordered_pair(sK4,sK5) = sF11
| ~ in(sK5,sF11)
| sK4 = sK1(sK4,sK5,sF11) ),
inference(trivial_inequality_removal,[],[f29399]) ).
fof(f29402,plain,
( sF6 = sF11
| ~ in(sK5,sF11)
| sK4 = sK1(sK4,sK5,sF11) ),
inference(forward_demodulation,[],[f29401,f74]) ).
fof(f29403,plain,
( ~ in(sK5,sF11)
| sK4 = sK1(sK4,sK5,sF11) ),
inference(forward_subsumption_resolution,[],[f29402,f85]) ).
fof(f29453,plain,
( in(sK5,sF7)
| sK4 = sK1(sK4,sK5,sF11) ),
inference(resolution,[],[f29403,f251]) ).
fof(f29503,plain,
( sK4 = sK1(sK4,sK5,sF11)
| sK4 = sK5 ),
inference(resolution,[],[f29453,f110]) ).
fof(f29531,plain,
sK4 = sK1(sK4,sK5,sF11),
inference(forward_subsumption_resolution,[],[f29503,f57]) ).
fof(f29584,plain,
( sK4 != sK4
| unordered_pair(sK4,sK5) = sF11
| ~ in(sK4,sF11) ),
inference(superposition,[],[f46,f29531]) ).
fof(f29586,plain,
( unordered_pair(sK4,sK5) = sF11
| ~ in(sK4,sF11) ),
inference(trivial_inequality_removal,[],[f29584]) ).
fof(f29588,plain,
( sF6 = sF11
| ~ in(sK4,sF11) ),
inference(forward_demodulation,[],[f29586,f74]) ).
fof(f29589,plain,
~ in(sK4,sF11),
inference(forward_subsumption_resolution,[],[f29588,f85]) ).
fof(f29637,plain,
sF8 = sF11,
inference(resolution,[],[f29589,f1388]) ).
fof(f29638,plain,
in(sK4,sF8),
inference(resolution,[],[f29589,f266]) ).
fof(f30525,plain,
~ in(sK4,sF8),
inference(superposition,[],[f29589,f29637]) ).
fof(f30538,plain,
$false,
inference(forward_subsumption_resolution,[],[f30525,f29638]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SET888+1 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.04 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.09/0.37 % Computer : n004.cluster.edu
% 0.09/0.37 % Model : x86_64 x86_64
% 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37 % Memory : 8046.5625MB
% 0.09/0.37 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Mon Sep 28 03:06:37 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.09/0.39 Running first-order model finding
% 0.09/0.39 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
% 14.85/2.54 % (4111346)Will run a generic schedule for satisfiability detection.
% 14.85/2.54 % (4111353)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3759736502:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 14.85/2.54 % (4111352)% WARNING: option uhcvi not known.
% 14.85/2.54 % (4111351)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3234835482_2999 on theBenchmark for (2999ds/0Mi)
% 14.85/2.54 % (4111352)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3677843429:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 14.85/2.54 % (4111357)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=801571549:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 14.85/2.54 % (4111354)dis+10_1_sil=32000:sp=arity:random_seed=3516213010:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 14.85/2.54 % (4111355)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2192492645:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 14.85/2.54 % (4111356)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=470906900:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 14.85/2.54 % TRYING [1]
% 14.85/2.54 % TRYING [2]
% 14.85/2.54 % TRYING [3]
% 14.85/2.54 % TRYING [4]
% 14.85/2.54 % TRYING [5]
% 14.85/2.54 % (4111354)Instruction limit reached!
% 14.85/2.54 % (4111354)------------------------------
% 14.85/2.54 % (4111354)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.85/2.54 % (4111354)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.85/2.54 % (4111354)CaDiCaL version: 2.1.3
% 14.85/2.54 % (4111354)Termination reason: Instruction limit
% 14.85/2.54 % (4111354)Termination phase: Saturation
% 14.85/2.54 % (4111354)Time elapsed: 0.057 s
% 14.85/2.54 % (4111354)Peak memory usage: 12 MB
% 14.85/2.54 % (4111354)Instructions burned: 103 (million)
% 14.85/2.54 % (4111355)Instruction limit reached!
% 14.85/2.54 % (4111355)------------------------------
% 14.85/2.54 % (4111355)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.85/2.54 % (4111355)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.85/2.54 % (4111355)CaDiCaL version: 2.1.3
% 14.85/2.54 % (4111355)Termination reason: Instruction limit
% 14.85/2.54 % (4111355)Termination phase: Saturation
% 14.85/2.54 % (4111355)Time elapsed: 0.066 s
% 14.85/2.54 % (4111355)Peak memory usage: 12 MB
% 14.85/2.54 % (4111355)Instructions burned: 116 (million)
% 14.85/2.54 % (4111356)Instruction limit reached!
% 14.85/2.54 % (4111356)------------------------------
% 14.85/2.54 % (4111356)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.85/2.54 % (4111356)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.85/2.54 % (4111356)CaDiCaL version: 2.1.3
% 14.85/2.54 % (4111356)Termination reason: Instruction limit
% 14.85/2.54 % (4111356)Termination phase: Saturation
% 14.85/2.54 % (4111356)Time elapsed: 0.071 s
% 14.85/2.54 % (4111356)Peak memory usage: 12 MB
% 14.85/2.54 % (4111356)Instructions burned: 131 (million)
% 14.85/2.54 % TRYING [6]
% 14.85/2.54 % (4111365)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=785906653:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 14.85/2.54 % TRYING [1]
% 14.85/2.54 % TRYING [2]
% 14.85/2.54 % TRYING [3]
% 14.85/2.54 % (4111366)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2089475951:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 14.85/2.54 % TRYING [4]
% 14.85/2.54 % (4111357)Instruction limit reached!
% 14.85/2.54 % (4111357)------------------------------
% 14.85/2.54 % (4111357)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.85/2.54 % (4111357)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.85/2.54 % (4111357)CaDiCaL version: 2.1.3
% 14.85/2.54 % (4111357)Termination reason: Instruction limit
% 14.85/2.54 % (4111357)Termination phase: Saturation
% 14.85/2.54 % (4111357)Time elapsed: 0.092 s
% 14.85/2.54 % (4111357)Peak memory usage: 12 MB
% 14.85/2.54 % (4111357)Instructions burned: 159 (million)
% 14.85/2.54 % (4111367)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=813637988:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 14.85/2.54 % TRYING [5]
% 14.85/2.54 % (4111371)ott-21_1_sil=16000:fs=off:random_seed=3824467225:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 14.85/2.54 % TRYING [6]
% 14.85/2.54 % (4111366)Instruction limit reached!
% 14.85/2.54 % (4111366)------------------------------
% 14.85/2.54 % (4111366)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.88/6.32 % (4111366)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.88/6.32 % (4111366)CaDiCaL version: 2.1.3
% 23.88/6.32 % (4111366)Termination reason: Instruction limit
% 23.88/6.32 % (4111366)Termination phase: Saturation
% 23.88/6.32 % (4111366)Time elapsed: 0.076 s
% 23.88/6.32 % (4111366)Peak memory usage: 12 MB
% 23.88/6.32 % (4111366)Instructions burned: 132 (million)
% 23.88/6.32 % (4111373)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=170153773:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 23.88/6.32 % (4111371)Instruction limit reached!
% 23.88/6.32 % (4111371)------------------------------
% 23.88/6.32 % (4111371)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.88/6.32 % (4111371)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.88/6.32 % (4111371)CaDiCaL version: 2.1.3
% 23.88/6.32 % (4111371)Termination reason: Instruction limit
% 23.88/6.32 % (4111371)Termination phase: Saturation
% 23.88/6.32 % (4111371)Time elapsed: 0.084 s
% 23.88/6.32 % (4111371)Peak memory usage: 12 MB
% 23.88/6.32 % (4111371)Instructions burned: 182 (million)
% 23.88/6.32 % TRYING [7]
% 23.88/6.32 % (4111375)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3770788657:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 23.88/6.32 % TRYING [1]
% 23.88/6.32 % TRYING [2]
% 23.88/6.32 % TRYING [3]
% 23.88/6.32 % TRYING [4]
% 23.88/6.32 % TRYING [5]
% 23.88/6.32 % TRYING [7]
% 23.88/6.32 % (4111365)Instruction limit reached!
% 23.88/6.32 % (4111365)------------------------------
% 23.88/6.32 % (4111365)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.88/6.32 % (4111365)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.88/6.32 % (4111365)CaDiCaL version: 2.1.3
% 23.88/6.32 % (4111365)Termination reason: Instruction limit
% 23.88/6.32 % (4111365)Termination phase: Finite model building constraint generation
% 23.88/6.32 % (4111365)Time elapsed: 0.252 s
% 23.88/6.32 % (4111365)Peak memory usage: 27 MB
% 23.88/6.32 % (4111365)Instructions burned: 716 (million)
% 23.88/6.32 % (4111377)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=4164718797:i=1179_2996 on theBenchmark for (2996ds/1179Mi)
% 23.88/6.32 % TRYING [6]
% 23.88/6.32 % (4111367)Instruction limit reached!
% 23.88/6.32 % (4111367)------------------------------
% 23.88/6.32 % (4111367)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.88/6.32 % (4111367)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.88/6.32 % (4111367)CaDiCaL version: 2.1.3
% 23.88/6.32 % (4111367)Termination reason: Instruction limit
% 23.88/6.32 % (4111367)Termination phase: Saturation
% 23.88/6.32 % (4111367)Time elapsed: 0.328 s
% 23.88/6.32 % (4111367)Peak memory usage: 13 MB
% 23.88/6.32 % (4111367)Instructions burned: 686 (million)
% 23.88/6.32 % (4111379)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=817001085:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi)
% 23.88/6.32 % (4111373)Instruction limit reached!
% 23.88/6.32 % (4111373)------------------------------
% 23.88/6.32 % (4111373)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.88/6.32 % (4111373)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.88/6.32 % (4111373)CaDiCaL version: 2.1.3
% 23.88/6.32 % (4111373)Termination reason: Instruction limit
% 23.88/6.32 % (4111373)Termination phase: Saturation
% 23.88/6.32 % (4111373)Time elapsed: 0.292 s
% 23.88/6.32 % (4111373)Peak memory usage: 13 MB
% 23.88/6.32 % (4111373)Instructions burned: 478 (million)
% 23.88/6.32 % TRYING [14]
% 23.88/6.32 % (4111381)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=3756122117: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)
% 23.88/6.32 % TRYING [8]
% 23.88/6.32 % (4111375)Instruction limit reached!
% 23.88/6.32 % (4111375)------------------------------
% 23.88/6.32 % (4111375)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.88/6.32 % (4111375)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.88/6.32 % (4111375)CaDiCaL version: 2.1.3
% 23.88/6.32 % (4111375)Termination reason: Instruction limit
% 23.88/6.32 % (4111375)Termination phase: Finite model building SAT solving
% 23.88/6.32 % (4111375)Time elapsed: 0.313 s
% 23.88/6.32 % (4111375)Peak memory usage: 25 MB
% 23.88/6.32 % (4111375)Instructions burned: 867 (million)
% 23.88/6.32 % (4111383)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1625635091:i=879:kws=inv_precedence:fsr=off_2994 on theBenchmark for (2994ds/879Mi)
% 23.88/6.32 % (4111379)Instruction limit reached!
% 23.88/6.32 % (4111379)------------------------------
% 23.88/6.32 % (4111379)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.88/6.32 % (4111379)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.88/6.32 % (4111379)CaDiCaL version: 2.1.3
% 23.88/6.32 % (4111379)Termination reason: Instruction limit
% 23.88/6.32 % (4111379)Termination phase: Finite model building constraint generation
% 23.88/6.32 % (4111379)Time elapsed: 0.304 s
% 23.88/6.32 % (4111379)Peak memory usage: 62 MB
% 23.88/6.32 % (4111379)Instructions burned: 889 (million)
% 23.88/6.32 % (4111385)fmb+10_1_sil=64000:random_seed=861573080:i=22061:nm=2:gsp=on_2992 on theBenchmark for (2992ds/22061Mi)
% 23.88/6.32 % TRYING [1]
% 23.88/6.32 % TRYING [2]
% 23.88/6.32 % TRYING [3]
% 23.88/6.32 % TRYING [4]
% 23.88/6.32 % TRYING [5]
% 23.88/6.32 % (4111381)Instruction limit reached!
% 23.88/6.32 % (4111381)------------------------------
% 23.88/6.32 % (4111381)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.88/6.32 % (4111381)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.88/6.32 % (4111381)CaDiCaL version: 2.1.3
% 23.88/6.32 % (4111381)Termination reason: Instruction limit
% 23.88/6.32 % (4111381)Termination phase: Saturation
% 23.88/6.32 % (4111381)Time elapsed: 0.360 s
% 23.88/6.32 % (4111381)Peak memory usage: 15 MB
% 23.88/6.32 % (4111381)Instructions burned: 693 (million)
% 23.88/6.32 % (4111387)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2371471543:i=9515:nm=5_2991 on theBenchmark for (2991ds/9515Mi)
% 23.88/6.32 % TRYING [20]
% 23.88/6.32 % (4111377)Instruction limit reached!
% 23.88/6.32 % (4111377)------------------------------
% 23.88/6.32 % (4111377)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.88/6.32 % (4111377)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.88/6.32 % (4111377)CaDiCaL version: 2.1.3
% 23.88/6.32 % (4111377)Termination reason: Instruction limit
% 23.88/6.32 % (4111377)Termination phase: Saturation
% 23.88/6.32 % (4111377)Time elapsed: 0.556 s
% 23.88/6.32 % (4111377)Peak memory usage: 15 MB
% 23.88/6.32 % (4111377)Instructions burned: 1179 (million)
% 23.88/6.32 % TRYING [6]
% 23.88/6.32 % (4111389)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1456902405:fmbsr=1.7:i=920_2990 on theBenchmark for (2990ds/920Mi)
% 23.88/6.32 % TRYING [8]
% 23.88/6.32 % (4111383)Instruction limit reached!
% 23.88/6.32 % (4111383)------------------------------
% 23.88/6.32 % (4111383)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.88/6.32 % (4111383)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.88/6.32 % (4111383)CaDiCaL version: 2.1.3
% 23.88/6.32 % (4111383)Termination reason: Instruction limit
% 23.88/6.32 % (4111383)Termination phase: Saturation
% 23.88/6.32 % (4111383)Time elapsed: 0.467 s
% 23.88/6.32 % (4111383)Peak memory usage: 17 MB
% 23.88/6.32 % (4111383)Instructions burned: 880 (million)
% 23.88/6.32 % (4111391)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1122260415:i=5131_2989 on theBenchmark for (2989ds/5131Mi)
% 23.88/6.32 % TRYING [7]
% 23.88/6.32 % TRYING [9]
% 23.88/6.32 % (4111389)Instruction limit reached!
% 23.88/6.32 % (4111389)------------------------------
% 23.88/6.32 % (4111389)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.88/6.32 % (4111389)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.88/6.32 % (4111389)CaDiCaL version: 2.1.3
% 23.88/6.32 % (4111389)Termination reason: Instruction limit
% 23.88/6.32 % (4111389)Termination phase: Finite model building constraint generation
% 23.88/6.32 % (4111389)Time elapsed: 0.331 s
% 23.88/6.32 % (4111389)Peak memory usage: 58 MB
% 23.88/6.32 % (4111389)Instructions burned: 921 (million)
% 23.88/6.32 % (4111393)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3644191724:i=1472:ins=7:fdi=8:gsp=on_2987 on theBenchmark for (2987ds/1472Mi)
% 23.88/6.32 % TRYING [8]
% 23.88/6.32 % (4111393)Instruction limit reached!
% 23.88/6.32 % (4111393)------------------------------
% 23.88/6.32 % (4111393)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.88/6.32 % (4111393)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.88/6.32 % (4111393)CaDiCaL version: 2.1.3
% 23.88/6.32 % (4111393)Termination reason: Instruction limit
% 23.88/6.32 % (4111393)Termination phase: Saturation
% 23.88/6.32 % (4111393)Time elapsed: 0.798 s
% 23.88/6.32 % (4111393)Peak memory usage: 27 MB
% 23.88/6.32 % (4111393)Instructions burned: 1474 (million)
% 23.88/6.32 % (4111395)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=640963652:i=6324_2978 on theBenchmark for (2978ds/6324Mi)
% 23.88/6.32 % TRYING [77]
% 23.88/6.32 % TRYING [9]
% 23.88/6.32 % TRYING [10]
% 23.88/6.32 % (4111391)Instruction limit reached!
% 23.88/6.32 % (4111391)------------------------------
% 23.88/6.32 % (4111391)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.88/6.32 % (4111391)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.88/6.32 % (4111391)CaDiCaL version: 2.1.3
% 23.88/6.32 % (4111391)Termination reason: Instruction limit
% 23.88/6.32 % (4111391)Termination phase: Saturation
% 23.88/6.32 % (4111391)Time elapsed: 2.551 s
% 23.88/6.32 % (4111391)Peak memory usage: 25 MB
% 23.88/6.32 % (4111391)Instructions burned: 5132 (million)
% 23.88/6.32 % (4111397)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=256154607:fmbsr=2.30978:i=2174_2963 on theBenchmark for (2963ds/2174Mi)
% 23.88/6.32 % TRYING [16]
% 23.88/6.32 % (4111387)Instruction limit reached!
% 23.88/6.32 % (4111387)------------------------------
% 23.88/6.32 % (4111387)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.88/6.32 % (4111387)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.88/6.32 % (4111387)CaDiCaL version: 2.1.3
% 23.88/6.32 % (4111387)Termination reason: Instruction limit
% 23.88/6.32 % (4111387)Termination phase: Finite model building constraint generation
% 23.88/6.32 % (4111387)Time elapsed: 3.229 s
% 23.88/6.32 % (4111387)Peak memory usage: 523 MB
% 23.88/6.32 % (4111387)Instructions burned: 9517 (million)
% 23.88/6.32 % (4111399)ott-2_1_sil=16000:newcnf=on:random_seed=1492137298:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2957 on theBenchmark for (2957ds/869Mi)
% 23.88/6.32 % (4111397)Instruction limit reached!
% 23.88/6.32 % (4111397)------------------------------
% 23.88/6.32 % (4111397)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.88/6.32 % (4111397)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.88/6.32 % (4111397)CaDiCaL version: 2.1.3
% 23.88/6.32 % (4111397)Termination reason: Instruction limit
% 23.88/6.32 % (4111397)Termination phase: Finite model building constraint generation
% 23.88/6.32 % (4111397)Time elapsed: 0.729 s
% 23.88/6.32 % (4111397)Peak memory usage: 131 MB
% 23.88/6.32 % (4111397)Instructions burned: 2175 (million)
% 23.88/6.32 % (4111401)ott+10_1_sil=32000:tgt=ground:random_seed=594087329:i=5114:av=off_2956 on theBenchmark for (2956ds/5114Mi)
% 23.88/6.32 % (4111395)Instruction limit reached!
% 23.88/6.32 % (4111395)------------------------------
% 23.88/6.32 % (4111395)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.88/6.32 % (4111395)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.88/6.32 % (4111395)CaDiCaL version: 2.1.3
% 23.88/6.32 % (4111395)Termination reason: Instruction limit
% 23.88/6.32 % (4111395)Termination phase: Finite model building constraint generation
% 23.88/6.32 % (4111395)Time elapsed: 2.334 s
% 23.88/6.32 % (4111395)Peak memory usage: 523 MB
% 23.88/6.32 % (4111395)Instructions burned: 6326 (million)
% 23.88/6.32 % (4111399)Instruction limit reached!
% 23.88/6.32 % (4111399)------------------------------
% 23.88/6.32 % (4111399)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.88/6.32 % (4111399)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.88/6.32 % (4111399)CaDiCaL version: 2.1.3
% 23.88/6.32 % (4111399)Termination reason: Instruction limit
% 23.88/6.32 % (4111399)Termination phase: Saturation
% 23.88/6.32 % (4111399)Time elapsed: 0.254 s
% 23.88/6.32 % (4111399)Peak memory usage: 13 MB
% 23.88/6.32 % (4111399)Instructions burned: 871 (million)
% 23.88/6.32 % (4111403)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=3587051909:i=54282_2955 on theBenchmark for (2955ds/54282Mi)
% 23.88/6.32 % TRYING [1]
% 23.88/6.32 % TRYING [2]
% 23.88/6.32 % TRYING [3]
% 23.88/6.32 % TRYING [4]
% 23.88/6.32 % TRYING [5]
% 23.88/6.32 % (4111405)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=133304514:i=3512:aac=none_2954 on theBenchmark for (2954ds/3512Mi)
% 23.88/6.32 % TRYING [6]
% 23.88/6.32 % TRYING [7]
% 23.88/6.32 % TRYING [8]
% 23.88/6.32 % TRYING [10]
% 23.88/6.32 % TRYING [9]
% 23.88/6.32 % (4111401) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-4111346-4111401"...
% 23.88/6.32 % (4111401)...printing done.
% 23.88/6.32 % (4111401)Refutation found. Thanks to Tanya!
% 23.88/6.32 % SZS status Theorem for theBenchmark
% 23.88/6.32 % SZS output start Proof for theBenchmark
% See solution above
% 23.88/6.32 % (4111401)------------------------------
% 23.88/6.32 % (4111401)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.88/6.32 % (4111401)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.88/6.32 % (4111401)CaDiCaL version: 2.1.3
% 23.88/6.32 % (4111401)Termination reason: Refutation
% 23.88/6.32 % (4111401)Time elapsed: 1.446 s
% 23.88/6.32 % (4111401)Peak memory usage: 21 MB
% 23.88/6.32 % (4111401)Instructions burned: 3070 (million)
% 23.88/6.32 % (4111346)Success in time 5.919 s
% 23.88/6.32 % Vampire exiting
%------------------------------------------------------------------------------