%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SEU282+1 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 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:48:09 PM UTC 2026
% Result : Theorem 34.65s 5.74s
% Output : Refutation 35.14s
% Verified :
% SZS Type : Refutation
% Derivation depth : 41
% Number of leaves : 10
% Syntax : Number of formulae : 179 ( 29 unt; 1 def)
% Number of atoms : 723 ( 213 equ)
% Maximal formula atoms : 15 ( 4 avg)
% Number of connectives : 921 ( 377 ~; 384 |; 131 &)
% ( 15 <=>; 12 =>; 0 <=; 2 <~>)
% Maximal formula depth : 14 ( 7 avg)
% Maximal term depth : 8 ( 2 avg)
% Number of predicates : 6 ( 4 usr; 1 prp; 0-2 aty)
% Number of functors : 21 ( 21 usr; 1 con; 0-2 aty)
% Number of variables : 518 ( 448 !; 70 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
! [X0] :
( ! [X1,X2,X3] :
( ( in(X1,X0)
& X2 = singleton(X1)
& in(X1,X0)
& X3 = singleton(X1) )
=> X2 = X3 )
=> ? [X1] :
( relation(X1)
& function(X1)
& ! [X2,X3] :
( in(ordered_pair(X2,X3),X1)
<=> ( in(X2,X0)
& in(X2,X0)
& X3 = singleton(X2) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',s1_funct_1__e16_22__wellord2__1) ).
fof(f2,negated_conjecture,
~ ! [X0] :
( ! [X1,X2,X3] :
( ( in(X1,X0)
& X2 = singleton(X1)
& in(X1,X0)
& X3 = singleton(X1) )
=> X2 = X3 )
=> ? [X1] :
( relation(X1)
& function(X1)
& ! [X2,X3] :
( in(ordered_pair(X2,X3),X1)
<=> ( in(X2,X0)
& in(X2,X0)
& X3 = singleton(X2) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f20,axiom,
! [X0] :
( ! [X1,X2,X3] :
( ( in(X1,X0)
& X2 = singleton(X1)
& in(X1,X0)
& X3 = singleton(X1) )
=> X2 = X3 )
=> ? [X1] :
! [X2] :
( in(X2,X1)
<=> ? [X3] :
( in(X3,X0)
& in(X3,X0)
& X2 = singleton(X3) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',s1_tarski__e16_22__wellord2__1) ).
fof(f21,axiom,
! [X0,X1] :
? [X2] :
! [X3] :
( in(X3,X2)
<=> ( in(X3,cartesian_product2(X0,X1))
& ? [X4,X5] :
( ordered_pair(X4,X5) = X3
& in(X4,X0)
& X5 = singleton(X4) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',s1_xboole_0__e16_22__wellord2__1) ).
fof(f23,axiom,
! [X0,X1] : unordered_pair(X0,X1) = unordered_pair(X1,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',commutativity_k2_tarski) ).
fof(f24,axiom,
! [X0] :
( function(X0)
<=> ! [X1,X2,X3] :
( ( in(ordered_pair(X1,X2),X0)
& in(ordered_pair(X1,X3),X0) )
=> X2 = X3 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d1_funct_1) ).
fof(f25,axiom,
! [X0] :
( relation(X0)
<=> ! [X1] :
~ ( in(X1,X0)
& ! [X2,X3] : X1 != ordered_pair(X2,X3) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d1_relat_1) ).
fof(f26,axiom,
! [X0,X1] : ordered_pair(X0,X1) = unordered_pair(unordered_pair(X0,X1),singleton(X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d5_tarski) ).
fof(f41,axiom,
! [X0,X1,X2,X3] :
( in(ordered_pair(X0,X1),cartesian_product2(X2,X3))
<=> ( in(X0,X2)
& in(X1,X3) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t106_zfmisc_1) ).
fof(f44,axiom,
! [X0,X1,X2,X3] :
( ordered_pair(X0,X1) = ordered_pair(X2,X3)
=> ( X0 = X2
& X1 = X3 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t33_zfmisc_1) ).
fof(f48,plain,
~ ! [X0] :
( ! [X1,X2,X3] :
( ( in(X1,X0)
& X2 = singleton(X1)
& in(X1,X0)
& X3 = singleton(X1) )
=> X2 = X3 )
=> ? [X4] :
( relation(X4)
& function(X4)
& ! [X5,X6] :
( in(ordered_pair(X5,X6),X4)
<=> ( in(X5,X0)
& in(X5,X0)
& singleton(X5) = X6 ) ) ) ),
inference(rectify,[],[f2]) ).
fof(f49,plain,
! [X0] :
( ! [X1,X2,X3] :
( ( in(X1,X0)
& X2 = singleton(X1)
& in(X1,X0)
& X3 = singleton(X1) )
=> X2 = X3 )
=> ? [X4] :
! [X5] :
( in(X5,X4)
<=> ? [X6] :
( in(X6,X0)
& in(X6,X0)
& singleton(X6) = X5 ) ) ),
inference(rectify,[],[f20]) ).
fof(f55,plain,
? [X0] :
( ! [X4] :
( ~ relation(X4)
| ~ function(X4)
| ? [X5,X6] :
( in(ordered_pair(X5,X6),X4)
<~> ( in(X5,X0)
& in(X5,X0)
& singleton(X5) = X6 ) ) )
& ! [X1,X2,X3] :
( X2 = X3
| ~ in(X1,X0)
| singleton(X1) != X2
| ~ in(X1,X0)
| singleton(X1) != X3 ) ),
inference(ennf_transformation,[],[f48]) ).
fof(f56,plain,
? [X0] :
( ! [X4] :
( ~ relation(X4)
| ~ function(X4)
| ? [X5,X6] :
( in(ordered_pair(X5,X6),X4)
<~> ( in(X5,X0)
& in(X5,X0)
& singleton(X5) = X6 ) ) )
& ! [X1,X2,X3] :
( X2 = X3
| ~ in(X1,X0)
| singleton(X1) != X2
| ~ in(X1,X0)
| singleton(X1) != X3 ) ),
inference(flattening,[],[f55]) ).
fof(f65,plain,
! [X0] :
( ? [X4] :
! [X5] :
( in(X5,X4)
<=> ? [X6] :
( in(X6,X0)
& in(X6,X0)
& singleton(X6) = X5 ) )
| ? [X1,X2,X3] :
( X2 != X3
& in(X1,X0)
& X2 = singleton(X1)
& in(X1,X0)
& X3 = singleton(X1) ) ),
inference(ennf_transformation,[],[f49]) ).
fof(f66,plain,
! [X0] :
( ? [X4] :
! [X5] :
( in(X5,X4)
<=> ? [X6] :
( in(X6,X0)
& in(X6,X0)
& singleton(X6) = X5 ) )
| ? [X1,X2,X3] :
( X2 != X3
& in(X1,X0)
& X2 = singleton(X1)
& in(X1,X0)
& X3 = singleton(X1) ) ),
inference(flattening,[],[f65]) ).
fof(f68,plain,
! [X0] :
( function(X0)
<=> ! [X1,X2,X3] :
( X2 = X3
| ~ in(ordered_pair(X1,X2),X0)
| ~ in(ordered_pair(X1,X3),X0) ) ),
inference(ennf_transformation,[],[f24]) ).
fof(f69,plain,
! [X0] :
( function(X0)
<=> ! [X1,X2,X3] :
( X2 = X3
| ~ in(ordered_pair(X1,X2),X0)
| ~ in(ordered_pair(X1,X3),X0) ) ),
inference(flattening,[],[f68]) ).
fof(f70,plain,
! [X0] :
( relation(X0)
<=> ! [X1] :
( ~ in(X1,X0)
| ? [X2,X3] : ordered_pair(X2,X3) = X1 ) ),
inference(ennf_transformation,[],[f25]) ).
fof(f76,plain,
! [X0,X1,X2,X3] :
( ( X0 = X2
& X1 = X3 )
| ordered_pair(X2,X3) != ordered_pair(X0,X1) ),
inference(ennf_transformation,[],[f44]) ).
fof(f80,definition,
! [X0] :
( ? [X1,X2,X3] :
( X2 != X3
& in(X1,X0)
& X2 = singleton(X1)
& in(X1,X0)
& X3 = singleton(X1) )
| ~ sP0(X0) ),
introduced(definition,[new_symbols(definition,[sP0])],[predicate_definition_introduction]) ).
fof(f81,plain,
! [X0] :
( ? [X4] :
! [X5] :
( in(X5,X4)
<=> ? [X6] :
( in(X6,X0)
& in(X6,X0)
& singleton(X6) = X5 ) )
| sP0(X0) ),
inference(definition_folding,[],[f66,f80]) ).
fof(f82,plain,
? [X0] :
( ! [X4] :
( ~ relation(X4)
| ~ function(X4)
| ? [X5,X6] :
( ( ~ in(X5,X0)
| ~ in(X5,X0)
| singleton(X5) != X6
| ~ in(ordered_pair(X5,X6),X4) )
& ( ( in(X5,X0)
& in(X5,X0)
& singleton(X5) = X6 )
| in(ordered_pair(X5,X6),X4) ) ) )
& ! [X1,X2,X3] :
( X2 = X3
| ~ in(X1,X0)
| singleton(X1) != X2
| ~ in(X1,X0)
| singleton(X1) != X3 ) ),
inference(nnf_transformation,[],[f56]) ).
fof(f83,plain,
? [X0] :
( ! [X4] :
( ~ relation(X4)
| ~ function(X4)
| ? [X5,X6] :
( ( ~ in(X5,X0)
| ~ in(X5,X0)
| singleton(X5) != X6
| ~ in(ordered_pair(X5,X6),X4) )
& ( ( in(X5,X0)
& in(X5,X0)
& singleton(X5) = X6 )
| in(ordered_pair(X5,X6),X4) ) ) )
& ! [X1,X2,X3] :
( X2 = X3
| ~ in(X1,X0)
| singleton(X1) != X2
| ~ in(X1,X0)
| singleton(X1) != X3 ) ),
inference(flattening,[],[f82]) ).
fof(f84,plain,
? [X0] :
( ! [X1] :
( ~ relation(X1)
| ~ function(X1)
| ? [X2,X3] :
( ( ~ in(X2,X0)
| ~ in(X2,X0)
| singleton(X2) != X3
| ~ in(ordered_pair(X2,X3),X1) )
& ( ( in(X2,X0)
& in(X2,X0)
& singleton(X2) = X3 )
| in(ordered_pair(X2,X3),X1) ) ) )
& ! [X4,X5,X6] :
( X5 = X6
| ~ in(X4,X0)
| singleton(X4) != X5
| ~ in(X4,X0)
| singleton(X4) != X6 ) ),
inference(rectify,[],[f83]) ).
fof(f85,plain,
( ! [X1] :
( ~ relation(X1)
| ~ function(X1)
| ( ( ~ in(sK2(X1),sK1)
| ~ in(sK2(X1),sK1)
| sK3(X1) != singleton(sK2(X1))
| ~ in(ordered_pair(sK2(X1),sK3(X1)),X1) )
& ( ( in(sK2(X1),sK1)
& in(sK2(X1),sK1)
& sK3(X1) = singleton(sK2(X1)) )
| in(ordered_pair(sK2(X1),sK3(X1)),X1) ) ) )
& ! [X4,X5,X6] :
( X5 = X6
| ~ in(X4,sK1)
| singleton(X4) != X5
| ~ in(X4,sK1)
| singleton(X4) != X6 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1,sK2,sK3]),skolemize(X0,sK1),skolemize(X2,sK2(X1)),skolemize(X3,sK3(X1))],[f84]) ).
fof(f94,plain,
! [X0] :
( ? [X1,X2,X3] :
( X2 != X3
& in(X1,X0)
& X2 = singleton(X1)
& in(X1,X0)
& X3 = singleton(X1) )
| ~ sP0(X0) ),
inference(nnf_transformation,[],[f80]) ).
fof(f95,plain,
! [X0] :
( ( sK13(X0) != sK14(X0)
& in(sK12(X0),X0)
& sK13(X0) = singleton(sK12(X0))
& in(sK12(X0),X0)
& sK14(X0) = singleton(sK12(X0)) )
| ~ sP0(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK12,sK13,sK14]),skolemize(X1,sK12(X0)),skolemize(X2,sK13(X0)),skolemize(X3,sK14(X0))],[f94]) ).
fof(f96,plain,
! [X0] :
( ? [X4] :
! [X5] :
( ( in(X5,X4)
| ! [X6] :
( ~ in(X6,X0)
| ~ in(X6,X0)
| singleton(X6) != X5 ) )
& ( ? [X6] :
( in(X6,X0)
& in(X6,X0)
& singleton(X6) = X5 )
| ~ in(X5,X4) ) )
| sP0(X0) ),
inference(nnf_transformation,[],[f81]) ).
fof(f97,plain,
! [X0] :
( ? [X1] :
! [X2] :
( ( in(X2,X1)
| ! [X3] :
( ~ in(X3,X0)
| ~ in(X3,X0)
| singleton(X3) != X2 ) )
& ( ? [X4] :
( in(X4,X0)
& in(X4,X0)
& singleton(X4) = X2 )
| ~ in(X2,X1) ) )
| sP0(X0) ),
inference(rectify,[],[f96]) ).
fof(f98,plain,
! [X0] :
( ! [X2] :
( ( in(X2,sK15(X0))
| ! [X3] :
( ~ in(X3,X0)
| ~ in(X3,X0)
| singleton(X3) != X2 ) )
& ( ( in(sK16(X0,X2),X0)
& in(sK16(X0,X2),X0)
& singleton(sK16(X0,X2)) = X2 )
| ~ in(X2,sK15(X0)) ) )
| sP0(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK15,sK16]),skolemize(X1,sK15(X0)),skolemize(X4,sK16(X0,X2))],[f97]) ).
fof(f99,plain,
! [X0,X1] :
? [X2] :
! [X3] :
( ( in(X3,X2)
| ~ in(X3,cartesian_product2(X0,X1))
| ! [X4,X5] :
( ordered_pair(X4,X5) != X3
| ~ in(X4,X0)
| singleton(X4) != X5 ) )
& ( ( in(X3,cartesian_product2(X0,X1))
& ? [X4,X5] :
( ordered_pair(X4,X5) = X3
& in(X4,X0)
& X5 = singleton(X4) ) )
| ~ in(X3,X2) ) ),
inference(nnf_transformation,[],[f21]) ).
fof(f100,plain,
! [X0,X1] :
? [X2] :
! [X3] :
( ( in(X3,X2)
| ~ in(X3,cartesian_product2(X0,X1))
| ! [X4,X5] :
( ordered_pair(X4,X5) != X3
| ~ in(X4,X0)
| singleton(X4) != X5 ) )
& ( ( in(X3,cartesian_product2(X0,X1))
& ? [X4,X5] :
( ordered_pair(X4,X5) = X3
& in(X4,X0)
& X5 = singleton(X4) ) )
| ~ in(X3,X2) ) ),
inference(flattening,[],[f99]) ).
fof(f101,plain,
! [X0,X1] :
? [X2] :
! [X3] :
( ( in(X3,X2)
| ~ in(X3,cartesian_product2(X0,X1))
| ! [X4,X5] :
( ordered_pair(X4,X5) != X3
| ~ in(X4,X0)
| singleton(X4) != X5 ) )
& ( ( in(X3,cartesian_product2(X0,X1))
& ? [X6,X7] :
( ordered_pair(X6,X7) = X3
& in(X6,X0)
& singleton(X6) = X7 ) )
| ~ in(X3,X2) ) ),
inference(rectify,[],[f100]) ).
fof(f102,plain,
! [X0,X1,X3] :
( ( in(X3,sK17(X0,X1))
| ~ in(X3,cartesian_product2(X0,X1))
| ! [X4,X5] :
( ordered_pair(X4,X5) != X3
| ~ in(X4,X0)
| singleton(X4) != X5 ) )
& ( ( in(X3,cartesian_product2(X0,X1))
& ordered_pair(sK18(X0,X3),sK19(X0,X3)) = X3
& in(sK18(X0,X3),X0)
& sK19(X0,X3) = singleton(sK18(X0,X3)) )
| ~ in(X3,sK17(X0,X1)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK17,sK18,sK19]),skolemize(X2,sK17(X0,X1)),skolemize(X6,sK18(X0,X3)),skolemize(X7,sK19(X0,X3))],[f101]) ).
fof(f103,plain,
! [X0] :
( ( function(X0)
| ? [X1,X2,X3] :
( X2 != X3
& in(ordered_pair(X1,X2),X0)
& in(ordered_pair(X1,X3),X0) ) )
& ( ! [X1,X2,X3] :
( X2 = X3
| ~ in(ordered_pair(X1,X2),X0)
| ~ in(ordered_pair(X1,X3),X0) )
| ~ function(X0) ) ),
inference(nnf_transformation,[],[f69]) ).
fof(f104,plain,
! [X0] :
( ( function(X0)
| ? [X1,X2,X3] :
( X2 != X3
& in(ordered_pair(X1,X2),X0)
& in(ordered_pair(X1,X3),X0) ) )
& ( ! [X4,X5,X6] :
( X5 = X6
| ~ in(ordered_pair(X4,X5),X0)
| ~ in(ordered_pair(X4,X6),X0) )
| ~ function(X0) ) ),
inference(rectify,[],[f103]) ).
fof(f105,plain,
! [X0] :
( ( function(X0)
| ( sK21(X0) != sK22(X0)
& in(ordered_pair(sK20(X0),sK21(X0)),X0)
& in(ordered_pair(sK20(X0),sK22(X0)),X0) ) )
& ( ! [X4,X5,X6] :
( X5 = X6
| ~ in(ordered_pair(X4,X5),X0)
| ~ in(ordered_pair(X4,X6),X0) )
| ~ function(X0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK20,sK21,sK22]),skolemize(X1,sK20(X0)),skolemize(X2,sK21(X0)),skolemize(X3,sK22(X0))],[f104]) ).
fof(f106,plain,
! [X0] :
( ( relation(X0)
| ? [X1] :
( in(X1,X0)
& ! [X2,X3] : ordered_pair(X2,X3) != X1 ) )
& ( ! [X1] :
( ~ in(X1,X0)
| ? [X2,X3] : ordered_pair(X2,X3) = X1 )
| ~ relation(X0) ) ),
inference(nnf_transformation,[],[f70]) ).
fof(f107,plain,
! [X0] :
( ( relation(X0)
| ? [X1] :
( in(X1,X0)
& ! [X2,X3] : ordered_pair(X2,X3) != X1 ) )
& ( ! [X4] :
( ~ in(X4,X0)
| ? [X5,X6] : ordered_pair(X5,X6) = X4 )
| ~ relation(X0) ) ),
inference(rectify,[],[f106]) ).
fof(f108,plain,
! [X0] :
( ( relation(X0)
| ( in(sK23(X0),X0)
& ! [X2,X3] : ordered_pair(X2,X3) != sK23(X0) ) )
& ( ! [X4] :
( ~ in(X4,X0)
| ordered_pair(sK24(X4),sK25(X4)) = X4 )
| ~ relation(X0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK23,sK24,sK25]),skolemize(X1,sK23(X0)),skolemize(X5,sK24(X4)),skolemize(X6,sK25(X4))],[f107]) ).
fof(f113,plain,
! [X0,X1,X2,X3] :
( ( in(ordered_pair(X0,X1),cartesian_product2(X2,X3))
| ~ in(X0,X2)
| ~ in(X1,X3) )
& ( ( in(X0,X2)
& in(X1,X3) )
| ~ in(ordered_pair(X0,X1),cartesian_product2(X2,X3)) ) ),
inference(nnf_transformation,[],[f41]) ).
fof(f114,plain,
! [X0,X1,X2,X3] :
( ( in(ordered_pair(X0,X1),cartesian_product2(X2,X3))
| ~ in(X0,X2)
| ~ in(X1,X3) )
& ( ( in(X0,X2)
& in(X1,X3) )
| ~ in(ordered_pair(X0,X1),cartesian_product2(X2,X3)) ) ),
inference(flattening,[],[f113]) ).
fof(f116,plain,
! [X1] :
( ~ relation(X1)
| ~ function(X1)
| sK3(X1) = singleton(sK2(X1))
| in(ordered_pair(sK2(X1),sK3(X1)),X1) ),
inference(cnf_transformation,[],[f85]) ).
fof(f117,plain,
! [X1] :
( ~ relation(X1)
| ~ function(X1)
| in(sK2(X1),sK1)
| in(ordered_pair(sK2(X1),sK3(X1)),X1) ),
inference(cnf_transformation,[],[f85]) ).
fof(f119,plain,
! [X1] :
( ~ relation(X1)
| ~ function(X1)
| ~ in(sK2(X1),sK1)
| ~ in(sK2(X1),sK1)
| sK3(X1) != singleton(sK2(X1))
| ~ in(ordered_pair(sK2(X1),sK3(X1)),X1) ),
inference(cnf_transformation,[],[f85]) ).
fof(f153,plain,
! [X0] :
( sK14(X0) = singleton(sK12(X0))
| ~ sP0(X0) ),
inference(cnf_transformation,[],[f95]) ).
fof(f155,plain,
! [X0] :
( sK13(X0) = singleton(sK12(X0))
| ~ sP0(X0) ),
inference(cnf_transformation,[],[f95]) ).
fof(f157,plain,
! [X0] :
( sK13(X0) != sK14(X0)
| ~ sP0(X0) ),
inference(cnf_transformation,[],[f95]) ).
fof(f161,plain,
! [X2,X3,X0] :
( in(X2,sK15(X0))
| ~ in(X3,X0)
| ~ in(X3,X0)
| singleton(X3) != X2
| sP0(X0) ),
inference(cnf_transformation,[],[f98]) ).
fof(f162,plain,
! [X3,X0,X1] :
( sK19(X0,X3) = singleton(sK18(X0,X3))
| ~ in(X3,sK17(X0,X1)) ),
inference(cnf_transformation,[],[f102]) ).
fof(f164,plain,
! [X3,X0,X1] :
( ordered_pair(sK18(X0,X3),sK19(X0,X3)) = X3
| ~ in(X3,sK17(X0,X1)) ),
inference(cnf_transformation,[],[f102]) ).
fof(f165,plain,
! [X3,X0,X1] :
( ~ in(X3,sK17(X0,X1))
| in(X3,cartesian_product2(X0,X1)) ),
inference(cnf_transformation,[],[f102]) ).
fof(f166,plain,
! [X3,X0,X1,X4,X5] :
( in(X3,sK17(X0,X1))
| ~ in(X3,cartesian_product2(X0,X1))
| ordered_pair(X4,X5) != X3
| ~ in(X4,X0)
| singleton(X4) != X5 ),
inference(cnf_transformation,[],[f102]) ).
fof(f168,plain,
! [X0,X1] : unordered_pair(X0,X1) = unordered_pair(X1,X0),
inference(cnf_transformation,[],[f23]) ).
fof(f169,plain,
! [X0,X6,X4,X5] :
( X5 = X6
| ~ in(ordered_pair(X4,X5),X0)
| ~ in(ordered_pair(X4,X6),X0)
| ~ function(X0) ),
inference(cnf_transformation,[],[f105]) ).
fof(f170,plain,
! [X0] :
( function(X0)
| in(ordered_pair(sK20(X0),sK22(X0)),X0) ),
inference(cnf_transformation,[],[f105]) ).
fof(f171,plain,
! [X0] :
( function(X0)
| in(ordered_pair(sK20(X0),sK21(X0)),X0) ),
inference(cnf_transformation,[],[f105]) ).
fof(f172,plain,
! [X0] :
( sK21(X0) != sK22(X0)
| function(X0) ),
inference(cnf_transformation,[],[f105]) ).
fof(f173,plain,
! [X0,X4] :
( ~ in(X4,X0)
| ordered_pair(sK24(X4),sK25(X4)) = X4
| ~ relation(X0) ),
inference(cnf_transformation,[],[f108]) ).
fof(f174,plain,
! [X2,X3,X0] :
( relation(X0)
| ordered_pair(X2,X3) != sK23(X0) ),
inference(cnf_transformation,[],[f108]) ).
fof(f175,plain,
! [X0] :
( in(sK23(X0),X0)
| relation(X0) ),
inference(cnf_transformation,[],[f108]) ).
fof(f176,plain,
! [X0,X1] : ordered_pair(X0,X1) = unordered_pair(unordered_pair(X0,X1),singleton(X0)),
inference(cnf_transformation,[],[f26]) ).
fof(f191,plain,
! [X2,X3,X0,X1] :
( in(X1,X3)
| ~ in(ordered_pair(X0,X1),cartesian_product2(X2,X3)) ),
inference(cnf_transformation,[],[f114]) ).
fof(f192,plain,
! [X2,X3,X0,X1] :
( in(X0,X2)
| ~ in(ordered_pair(X0,X1),cartesian_product2(X2,X3)) ),
inference(cnf_transformation,[],[f114]) ).
fof(f193,plain,
! [X2,X3,X0,X1] :
( in(ordered_pair(X0,X1),cartesian_product2(X2,X3))
| ~ in(X0,X2)
| ~ in(X1,X3) ),
inference(cnf_transformation,[],[f114]) ).
fof(f196,plain,
! [X2,X3,X0,X1] :
( X1 = X3
| ordered_pair(X2,X3) != ordered_pair(X0,X1) ),
inference(cnf_transformation,[],[f76]) ).
fof(f197,plain,
! [X2,X3,X0,X1] :
( X0 = X2
| ordered_pair(X2,X3) != ordered_pair(X0,X1) ),
inference(cnf_transformation,[],[f76]) ).
fof(f201,plain,
! [X1] :
( ~ relation(X1)
| ~ function(X1)
| ~ in(sK2(X1),sK1)
| ~ in(sK2(X1),sK1)
| sK3(X1) != singleton(sK2(X1))
| ~ in(unordered_pair(unordered_pair(sK2(X1),sK3(X1)),singleton(sK2(X1))),X1) ),
inference(definition_unfolding,[],[f119,f176]) ).
fof(f203,plain,
! [X1] :
( ~ relation(X1)
| ~ function(X1)
| in(sK2(X1),sK1)
| in(unordered_pair(unordered_pair(sK2(X1),sK3(X1)),singleton(sK2(X1))),X1) ),
inference(definition_unfolding,[],[f117,f176]) ).
fof(f204,plain,
! [X1] :
( ~ relation(X1)
| ~ function(X1)
| sK3(X1) = singleton(sK2(X1))
| in(unordered_pair(unordered_pair(sK2(X1),sK3(X1)),singleton(sK2(X1))),X1) ),
inference(definition_unfolding,[],[f116,f176]) ).
fof(f206,plain,
! [X3,X0,X1,X4,X5] :
( in(X3,sK17(X0,X1))
| ~ in(X3,cartesian_product2(X0,X1))
| unordered_pair(unordered_pair(X4,X5),singleton(X4)) != X3
| ~ in(X4,X0)
| singleton(X4) != X5 ),
inference(definition_unfolding,[],[f166,f176]) ).
fof(f207,plain,
! [X3,X0,X1] :
( unordered_pair(unordered_pair(sK18(X0,X3),sK19(X0,X3)),singleton(sK18(X0,X3))) = X3
| ~ in(X3,sK17(X0,X1)) ),
inference(definition_unfolding,[],[f164,f176]) ).
fof(f208,plain,
! [X0] :
( function(X0)
| in(unordered_pair(unordered_pair(sK20(X0),sK21(X0)),singleton(sK20(X0))),X0) ),
inference(definition_unfolding,[],[f171,f176]) ).
fof(f209,plain,
! [X0] :
( function(X0)
| in(unordered_pair(unordered_pair(sK20(X0),sK22(X0)),singleton(sK20(X0))),X0) ),
inference(definition_unfolding,[],[f170,f176]) ).
fof(f210,plain,
! [X0,X6,X4,X5] :
( X5 = X6
| ~ in(unordered_pair(unordered_pair(X4,X5),singleton(X4)),X0)
| ~ in(unordered_pair(unordered_pair(X4,X6),singleton(X4)),X0)
| ~ function(X0) ),
inference(definition_unfolding,[],[f169,f176,f176]) ).
fof(f211,plain,
! [X2,X3,X0] :
( relation(X0)
| sK23(X0) != unordered_pair(unordered_pair(X2,X3),singleton(X2)) ),
inference(definition_unfolding,[],[f174,f176]) ).
fof(f212,plain,
! [X0,X4] :
( ~ in(X4,X0)
| unordered_pair(unordered_pair(sK24(X4),sK25(X4)),singleton(sK24(X4))) = X4
| ~ relation(X0) ),
inference(definition_unfolding,[],[f173,f176]) ).
fof(f213,plain,
! [X2,X3,X0,X1] :
( in(unordered_pair(unordered_pair(X0,X1),singleton(X0)),cartesian_product2(X2,X3))
| ~ in(X0,X2)
| ~ in(X1,X3) ),
inference(definition_unfolding,[],[f193,f176]) ).
fof(f214,plain,
! [X2,X3,X0,X1] :
( in(X0,X2)
| ~ in(unordered_pair(unordered_pair(X0,X1),singleton(X0)),cartesian_product2(X2,X3)) ),
inference(definition_unfolding,[],[f192,f176]) ).
fof(f215,plain,
! [X2,X3,X0,X1] :
( in(X1,X3)
| ~ in(unordered_pair(unordered_pair(X0,X1),singleton(X0)),cartesian_product2(X2,X3)) ),
inference(definition_unfolding,[],[f191,f176]) ).
fof(f216,plain,
! [X2,X3,X0,X1] :
( X0 = X2
| unordered_pair(unordered_pair(X0,X1),singleton(X0)) != unordered_pair(unordered_pair(X2,X3),singleton(X2)) ),
inference(definition_unfolding,[],[f197,f176,f176]) ).
fof(f217,plain,
! [X2,X3,X0,X1] :
( X1 = X3
| unordered_pair(unordered_pair(X0,X1),singleton(X0)) != unordered_pair(unordered_pair(X2,X3),singleton(X2)) ),
inference(definition_unfolding,[],[f196,f176,f176]) ).
fof(f220,plain,
! [X3,X0] :
( in(singleton(X3),sK15(X0))
| ~ in(X3,X0)
| ~ in(X3,X0)
| sP0(X0) ),
inference(equality_resolution,[],[f161]) ).
fof(f221,plain,
! [X0,X1,X4,X5] :
( in(unordered_pair(unordered_pair(X4,X5),singleton(X4)),sK17(X0,X1))
| ~ in(unordered_pair(unordered_pair(X4,X5),singleton(X4)),cartesian_product2(X0,X1))
| ~ in(X4,X0)
| singleton(X4) != X5 ),
inference(equality_resolution,[],[f206]) ).
fof(f222,plain,
! [X0,X1,X4] :
( in(unordered_pair(unordered_pair(X4,singleton(X4)),singleton(X4)),sK17(X0,X1))
| ~ in(unordered_pair(unordered_pair(X4,singleton(X4)),singleton(X4)),cartesian_product2(X0,X1))
| ~ in(X4,X0) ),
inference(equality_resolution,[],[f221]) ).
fof(f223,plain,
! [X3,X0] :
( in(singleton(X3),sK15(X0))
| ~ in(X3,X0)
| sP0(X0) ),
inference(duplicate_literal_removal,[],[f220]) ).
fof(f225,plain,
! [X1] :
( ~ relation(X1)
| ~ function(X1)
| ~ in(sK2(X1),sK1)
| sK3(X1) != singleton(sK2(X1))
| ~ in(unordered_pair(unordered_pair(sK2(X1),sK3(X1)),singleton(sK2(X1))),X1) ),
inference(duplicate_literal_removal,[],[f201]) ).
fof(f226,plain,
! [X0,X6,X4,X5] :
( ~ in(unordered_pair(singleton(X4),unordered_pair(X4,X5)),X0)
| X5 = X6
| ~ in(unordered_pair(unordered_pair(X4,X6),singleton(X4)),X0)
| ~ function(X0) ),
inference(backward_demodulation,[],[f210,f168]) ).
fof(f227,plain,
! [X2,X3,X0] :
( sK23(X0) != unordered_pair(singleton(X2),unordered_pair(X2,X3))
| relation(X0) ),
inference(backward_demodulation,[],[f211,f168]) ).
fof(f228,plain,
! [X2,X3,X0,X1] :
( in(unordered_pair(singleton(X0),unordered_pair(X0,X1)),cartesian_product2(X2,X3))
| ~ in(X0,X2)
| ~ in(X1,X3) ),
inference(backward_demodulation,[],[f213,f168]) ).
fof(f229,plain,
! [X2,X3,X0,X1] :
( ~ in(unordered_pair(singleton(X0),unordered_pair(X0,X1)),cartesian_product2(X2,X3))
| in(X0,X2) ),
inference(backward_demodulation,[],[f214,f168]) ).
fof(f230,plain,
! [X2,X3,X0,X1] :
( ~ in(unordered_pair(singleton(X0),unordered_pair(X0,X1)),cartesian_product2(X2,X3))
| in(X1,X3) ),
inference(backward_demodulation,[],[f215,f168]) ).
fof(f231,plain,
! [X2,X3,X0,X1] :
( unordered_pair(unordered_pair(X2,X3),singleton(X2)) != unordered_pair(singleton(X0),unordered_pair(X0,X1))
| X0 = X2 ),
inference(backward_demodulation,[],[f216,f168]) ).
fof(f232,plain,
! [X2,X3,X0,X1] :
( unordered_pair(unordered_pair(X2,X3),singleton(X2)) != unordered_pair(singleton(X0),unordered_pair(X0,X1))
| X1 = X3 ),
inference(backward_demodulation,[],[f217,f168]) ).
fof(f233,plain,
! [X0,X4] :
( unordered_pair(singleton(sK24(X4)),unordered_pair(sK24(X4),sK25(X4))) = X4
| ~ in(X4,X0)
| ~ relation(X0) ),
inference(backward_demodulation,[],[f212,f168]) ).
fof(f234,plain,
! [X0] :
( in(unordered_pair(singleton(sK20(X0)),unordered_pair(sK20(X0),sK22(X0))),X0)
| function(X0) ),
inference(backward_demodulation,[],[f209,f168]) ).
fof(f235,plain,
! [X0] :
( in(unordered_pair(singleton(sK20(X0)),unordered_pair(sK20(X0),sK21(X0))),X0)
| function(X0) ),
inference(backward_demodulation,[],[f208,f168]) ).
fof(f236,plain,
! [X3,X0,X1] :
( unordered_pair(singleton(sK18(X0,X3)),unordered_pair(sK18(X0,X3),sK19(X0,X3))) = X3
| ~ in(X3,sK17(X0,X1)) ),
inference(forward_demodulation,[],[f207,f168]) ).
fof(f237,plain,
! [X0,X1,X4] :
( in(unordered_pair(singleton(X4),unordered_pair(X4,singleton(X4))),sK17(X0,X1))
| ~ in(unordered_pair(unordered_pair(X4,singleton(X4)),singleton(X4)),cartesian_product2(X0,X1))
| ~ in(X4,X0) ),
inference(forward_demodulation,[],[f222,f168]) ).
fof(f238,plain,
! [X1] :
( in(unordered_pair(singleton(sK2(X1)),unordered_pair(sK2(X1),sK3(X1))),X1)
| ~ relation(X1)
| ~ function(X1)
| sK3(X1) = singleton(sK2(X1)) ),
inference(forward_demodulation,[],[f204,f168]) ).
fof(f239,plain,
! [X1] :
( in(unordered_pair(singleton(sK2(X1)),unordered_pair(sK2(X1),sK3(X1))),X1)
| ~ relation(X1)
| ~ function(X1)
| in(sK2(X1),sK1) ),
inference(forward_demodulation,[],[f203,f168]) ).
fof(f241,plain,
! [X1] :
( sK3(X1) != singleton(sK2(X1))
| ~ relation(X1)
| ~ function(X1)
| ~ in(sK2(X1),sK1)
| ~ in(unordered_pair(singleton(sK2(X1)),unordered_pair(sK2(X1),sK3(X1))),X1) ),
inference(forward_demodulation,[],[f225,f168]) ).
fof(f242,plain,
! [X2,X3,X0,X1] :
( unordered_pair(singleton(X2),unordered_pair(X2,X3)) != unordered_pair(singleton(X0),unordered_pair(X0,X1))
| X1 = X3 ),
inference(forward_demodulation,[],[f232,f168]) ).
fof(f243,plain,
! [X2,X3,X0,X1] :
( unordered_pair(singleton(X2),unordered_pair(X2,X3)) != unordered_pair(singleton(X0),unordered_pair(X0,X1))
| X0 = X2 ),
inference(forward_demodulation,[],[f231,f168]) ).
fof(f244,plain,
! [X0,X6,X4,X5] :
( ~ in(unordered_pair(singleton(X4),unordered_pair(X4,X6)),X0)
| ~ in(unordered_pair(singleton(X4),unordered_pair(X4,X5)),X0)
| X5 = X6
| ~ function(X0) ),
inference(forward_demodulation,[],[f226,f168]) ).
fof(f245,plain,
! [X0,X1,X4] :
( ~ in(unordered_pair(singleton(X4),unordered_pair(X4,singleton(X4))),cartesian_product2(X0,X1))
| in(unordered_pair(singleton(X4),unordered_pair(X4,singleton(X4))),sK17(X0,X1))
| ~ in(X4,X0) ),
inference(forward_demodulation,[],[f237,f168]) ).
fof(f246,plain,
! [X0,X1,X4] :
( ~ in(unordered_pair(singleton(X4),unordered_pair(X4,singleton(X4))),cartesian_product2(X0,X1))
| in(unordered_pair(singleton(X4),unordered_pair(X4,singleton(X4))),sK17(X0,X1)) ),
inference(forward_subsumption_resolution,[],[f245,f229]) ).
fof(f300,plain,
! [X2,X3,X0,X1] :
( unordered_pair(singleton(X1),unordered_pair(X1,X2)) != X0
| sK25(X0) = X2
| ~ in(X0,X3)
| ~ relation(X3) ),
inference(superposition,[],[f242,f233]) ).
fof(f302,plain,
! [X2,X3,X0,X1] :
( unordered_pair(singleton(X1),unordered_pair(X1,X2)) != X0
| sK24(X0) = X1
| ~ in(X0,X3)
| ~ relation(X3) ),
inference(superposition,[],[f243,f233]) ).
fof(f353,plain,
! [X2,X0,X1] :
( sK25(unordered_pair(singleton(X0),unordered_pair(X0,X1))) = X1
| ~ in(unordered_pair(singleton(X0),unordered_pair(X0,X1)),X2)
| ~ relation(X2) ),
inference(equality_resolution,[],[f300]) ).
fof(f379,plain,
! [X2,X0,X1] :
( in(unordered_pair(singleton(X0),unordered_pair(X0,singleton(X0))),sK17(X1,X2))
| ~ in(X0,X1)
| ~ in(singleton(X0),X2) ),
inference(resolution,[],[f246,f228]) ).
fof(f390,plain,
! [X2,X0,X1] :
( sK24(unordered_pair(singleton(X0),unordered_pair(X0,X1))) = X0
| ~ in(unordered_pair(singleton(X0),unordered_pair(X0,X1)),X2)
| ~ relation(X2) ),
inference(equality_resolution,[],[f302]) ).
fof(f403,plain,
! [X0,X1] :
( ~ relation(X0)
| ~ function(X0)
| singleton(sK2(X0)) = sK3(X0)
| ~ in(unordered_pair(singleton(sK2(X0)),unordered_pair(sK2(X0),X1)),X0)
| sK3(X0) = X1
| ~ function(X0) ),
inference(resolution,[],[f238,f244]) ).
fof(f404,plain,
! [X0,X1] :
( ~ in(unordered_pair(singleton(sK2(X0)),unordered_pair(sK2(X0),X1)),X0)
| ~ function(X0)
| singleton(sK2(X0)) = sK3(X0)
| ~ relation(X0)
| sK3(X0) = X1 ),
inference(duplicate_literal_removal,[],[f403]) ).
fof(f424,plain,
! [X2,X3,X0,X1] :
( sK23(X1) != X0
| relation(X1)
| ~ in(X0,sK17(X2,X3)) ),
inference(superposition,[],[f227,f236]) ).
fof(f429,plain,
! [X2,X3,X0,X1,X4] :
( unordered_pair(singleton(X1),unordered_pair(X1,X2)) != X0
| sK19(X3,X0) = X2
| ~ in(X0,sK17(X3,X4)) ),
inference(superposition,[],[f242,f236]) ).
fof(f431,plain,
! [X2,X3,X0,X1,X4] :
( unordered_pair(singleton(X1),unordered_pair(X1,X2)) != X0
| sK18(X3,X0) = X1
| ~ in(X0,sK17(X3,X4)) ),
inference(superposition,[],[f243,f236]) ).
fof(f438,plain,
! [X2,X3,X0,X1] :
( sK25(X0) = sK19(X1,X0)
| ~ in(X0,X2)
| ~ relation(X2)
| ~ in(X0,sK17(X1,X3)) ),
inference(superposition,[],[f353,f236]) ).
fof(f439,plain,
! [X2,X3,X0,X1] :
( sK24(X0) = sK18(X1,X0)
| ~ in(X0,X2)
| ~ relation(X2)
| ~ in(X0,sK17(X1,X3)) ),
inference(superposition,[],[f390,f236]) ).
fof(f486,plain,
! [X2,X3,X0,X1] :
( ~ in(unordered_pair(singleton(X1),unordered_pair(X1,X2)),sK17(X0,X3))
| sK18(X0,unordered_pair(singleton(X1),unordered_pair(X1,X2))) = X1 ),
inference(equality_resolution,[],[f431]) ).
fof(f497,plain,
! [X2,X3,X0,X1] :
( ~ in(unordered_pair(singleton(X1),unordered_pair(X1,X2)),sK17(X0,X3))
| sK19(X0,unordered_pair(singleton(X1),unordered_pair(X1,X2))) = X2 ),
inference(equality_resolution,[],[f429]) ).
fof(f582,plain,
! [X0] :
( sK13(X0) = sK14(X0)
| ~ sP0(X0)
| ~ sP0(X0) ),
inference(superposition,[],[f153,f155]) ).
fof(f609,plain,
! [X0] :
( sK13(X0) = sK14(X0)
| ~ sP0(X0) ),
inference(duplicate_literal_removal,[],[f582]) ).
fof(f611,plain,
! [X0] : ~ sP0(X0),
inference(forward_subsumption_resolution,[],[f609,f157]) ).
fof(f734,plain,
! [X0,X1] :
( ~ in(sK2(sK17(X0,X1)),X0)
| ~ in(singleton(sK2(sK17(X0,X1))),X1)
| ~ function(sK17(X0,X1))
| singleton(sK2(sK17(X0,X1))) = sK3(sK17(X0,X1))
| ~ relation(sK17(X0,X1))
| singleton(sK2(sK17(X0,X1))) = sK3(sK17(X0,X1)) ),
inference(resolution,[],[f379,f404]) ).
fof(f742,plain,
! [X0,X1] :
( singleton(sK2(sK17(X0,X1))) = sK3(sK17(X0,X1))
| ~ in(singleton(sK2(sK17(X0,X1))),X1)
| ~ function(sK17(X0,X1))
| ~ in(sK2(sK17(X0,X1)),X0)
| ~ relation(sK17(X0,X1)) ),
inference(duplicate_literal_removal,[],[f734]) ).
fof(f768,plain,
! [X0,X1] :
( sK3(sK17(X0,X1)) != sK3(sK17(X0,X1))
| ~ relation(sK17(X0,X1))
| ~ function(sK17(X0,X1))
| ~ in(sK2(sK17(X0,X1)),sK1)
| ~ in(unordered_pair(sK3(sK17(X0,X1)),unordered_pair(sK2(sK17(X0,X1)),sK3(sK17(X0,X1)))),sK17(X0,X1))
| ~ in(singleton(sK2(sK17(X0,X1))),X1)
| ~ function(sK17(X0,X1))
| ~ in(sK2(sK17(X0,X1)),X0)
| ~ relation(sK17(X0,X1)) ),
inference(superposition,[],[f241,f742]) ).
fof(f791,plain,
! [X2,X3,X0,X1] :
( in(unordered_pair(sK3(sK17(X0,X1)),unordered_pair(sK2(sK17(X0,X1)),sK3(sK17(X0,X1)))),sK17(X2,X3))
| ~ in(sK2(sK17(X0,X1)),X2)
| ~ in(sK3(sK17(X0,X1)),X3)
| ~ in(singleton(sK2(sK17(X0,X1))),X1)
| ~ function(sK17(X0,X1))
| ~ in(sK2(sK17(X0,X1)),X0)
| ~ relation(sK17(X0,X1)) ),
inference(superposition,[],[f379,f742]) ).
fof(f800,plain,
! [X0,X1] :
( sK3(sK17(X0,X1)) != sK3(sK17(X0,X1))
| ~ relation(sK17(X0,X1))
| ~ function(sK17(X0,X1))
| ~ in(sK2(sK17(X0,X1)),sK1)
| ~ in(unordered_pair(sK3(sK17(X0,X1)),unordered_pair(sK2(sK17(X0,X1)),sK3(sK17(X0,X1)))),sK17(X0,X1))
| ~ in(singleton(sK2(sK17(X0,X1))),X1)
| ~ in(sK2(sK17(X0,X1)),X0) ),
inference(duplicate_literal_removal,[],[f768]) ).
fof(f801,plain,
! [X0,X1] :
( ~ in(unordered_pair(sK3(sK17(X0,X1)),unordered_pair(sK2(sK17(X0,X1)),sK3(sK17(X0,X1)))),sK17(X0,X1))
| ~ function(sK17(X0,X1))
| ~ in(sK2(sK17(X0,X1)),sK1)
| ~ relation(sK17(X0,X1))
| ~ in(singleton(sK2(sK17(X0,X1))),X1)
| ~ in(sK2(sK17(X0,X1)),X0) ),
inference(trivial_inequality_removal,[],[f800]) ).
fof(f841,plain,
! [X2,X0,X1] :
( ~ in(sK23(X0),sK17(X1,X2))
| relation(X0) ),
inference(equality_resolution,[],[f424]) ).
fof(f842,plain,
! [X0,X1] :
( relation(sK17(X0,X1))
| relation(sK17(X0,X1)) ),
inference(resolution,[],[f841,f175]) ).
fof(f843,plain,
! [X0,X1] : relation(sK17(X0,X1)),
inference(duplicate_literal_removal,[],[f842]) ).
fof(f934,plain,
! [X0,X1] :
( in(unordered_pair(singleton(sK2(sK17(X0,X1))),unordered_pair(sK2(sK17(X0,X1)),sK3(sK17(X0,X1)))),cartesian_product2(X0,X1))
| ~ relation(sK17(X0,X1))
| ~ function(sK17(X0,X1))
| singleton(sK2(sK17(X0,X1))) = sK3(sK17(X0,X1)) ),
inference(resolution,[],[f165,f238]) ).
fof(f935,plain,
! [X0,X1] :
( in(unordered_pair(singleton(sK2(sK17(X0,X1))),unordered_pair(sK2(sK17(X0,X1)),sK3(sK17(X0,X1)))),cartesian_product2(X0,X1))
| ~ relation(sK17(X0,X1))
| ~ function(sK17(X0,X1))
| in(sK2(sK17(X0,X1)),sK1) ),
inference(resolution,[],[f165,f239]) ).
fof(f952,plain,
! [X0,X1] :
( in(unordered_pair(singleton(sK2(sK17(X0,X1))),unordered_pair(sK2(sK17(X0,X1)),sK3(sK17(X0,X1)))),cartesian_product2(X0,X1))
| ~ function(sK17(X0,X1))
| in(sK2(sK17(X0,X1)),sK1) ),
inference(forward_subsumption_resolution,[],[f935,f843]) ).
fof(f953,plain,
! [X0,X1] :
( in(unordered_pair(singleton(sK2(sK17(X0,X1))),unordered_pair(sK2(sK17(X0,X1)),sK3(sK17(X0,X1)))),cartesian_product2(X0,X1))
| ~ function(sK17(X0,X1))
| singleton(sK2(sK17(X0,X1))) = sK3(sK17(X0,X1)) ),
inference(forward_subsumption_resolution,[],[f934,f843]) ).
fof(f956,plain,
! [X0,X1] :
( in(sK2(sK17(X0,X1)),sK1)
| ~ function(sK17(X0,X1))
| in(sK2(sK17(X0,X1)),X0) ),
inference(resolution,[],[f952,f229]) ).
fof(f964,plain,
! [X0] :
( in(sK2(sK17(sK1,X0)),sK1)
| ~ function(sK17(sK1,X0)) ),
inference(factoring,[],[f956]) ).
fof(f966,plain,
! [X0,X1] :
( singleton(sK2(sK17(X0,X1))) = sK3(sK17(X0,X1))
| ~ function(sK17(X0,X1))
| in(sK3(sK17(X0,X1)),X1) ),
inference(resolution,[],[f953,f230]) ).
fof(f977,plain,
! [X2,X0,X1] :
( in(sK3(sK17(X0,X1)),sK15(X2))
| ~ in(sK2(sK17(X0,X1)),X2)
| sP0(X2)
| ~ function(sK17(X0,X1))
| in(sK3(sK17(X0,X1)),X1) ),
inference(superposition,[],[f223,f966]) ).
fof(f1021,plain,
! [X2,X0,X1] :
( in(sK3(sK17(X0,X1)),sK15(X2))
| ~ in(sK2(sK17(X0,X1)),X2)
| ~ function(sK17(X0,X1))
| in(sK3(sK17(X0,X1)),X1) ),
inference(forward_subsumption_resolution,[],[f977,f611]) ).
fof(f1108,plain,
! [X0,X1] :
( in(sK3(sK17(X0,sK15(X1))),sK15(X1))
| ~ in(sK2(sK17(X0,sK15(X1))),X1)
| ~ function(sK17(X0,sK15(X1))) ),
inference(factoring,[],[f1021]) ).
fof(f1568,plain,
! [X0,X1] :
( ~ in(sK2(sK17(X0,X1)),X0)
| ~ in(sK3(sK17(X0,X1)),X1)
| ~ in(singleton(sK2(sK17(X0,X1))),X1)
| ~ function(sK17(X0,X1))
| ~ in(sK2(sK17(X0,X1)),X0)
| ~ relation(sK17(X0,X1))
| ~ function(sK17(X0,X1))
| ~ in(sK2(sK17(X0,X1)),sK1)
| ~ relation(sK17(X0,X1))
| ~ in(singleton(sK2(sK17(X0,X1))),X1)
| ~ in(sK2(sK17(X0,X1)),X0) ),
inference(resolution,[],[f791,f801]) ).
fof(f1582,plain,
! [X0,X1] :
( ~ in(sK2(sK17(X0,X1)),X0)
| ~ in(sK3(sK17(X0,X1)),X1)
| ~ in(singleton(sK2(sK17(X0,X1))),X1)
| ~ function(sK17(X0,X1))
| ~ relation(sK17(X0,X1))
| ~ in(sK2(sK17(X0,X1)),sK1) ),
inference(duplicate_literal_removal,[],[f1568]) ).
fof(f1588,plain,
! [X0,X1] :
( ~ in(singleton(sK2(sK17(X0,X1))),X1)
| ~ in(sK3(sK17(X0,X1)),X1)
| ~ in(sK2(sK17(X0,X1)),X0)
| ~ function(sK17(X0,X1))
| ~ in(sK2(sK17(X0,X1)),sK1) ),
inference(forward_subsumption_resolution,[],[f1582,f843]) ).
fof(f1592,plain,
! [X0,X1] :
( ~ in(sK3(sK17(X0,sK15(X1))),sK15(X1))
| ~ in(sK2(sK17(X0,sK15(X1))),X0)
| ~ function(sK17(X0,sK15(X1)))
| ~ in(sK2(sK17(X0,sK15(X1))),sK1)
| ~ in(sK2(sK17(X0,sK15(X1))),X1)
| sP0(X1) ),
inference(resolution,[],[f1588,f223]) ).
fof(f1599,plain,
! [X0,X1] :
( ~ in(sK2(sK17(X0,sK15(X1))),X0)
| ~ function(sK17(X0,sK15(X1)))
| ~ in(sK2(sK17(X0,sK15(X1))),sK1)
| ~ in(sK2(sK17(X0,sK15(X1))),X1)
| sP0(X1) ),
inference(forward_subsumption_resolution,[],[f1592,f1108]) ).
fof(f1600,plain,
! [X0,X1] :
( ~ in(sK2(sK17(X0,sK15(X1))),sK1)
| ~ function(sK17(X0,sK15(X1)))
| ~ in(sK2(sK17(X0,sK15(X1))),X0)
| ~ in(sK2(sK17(X0,sK15(X1))),X1) ),
inference(forward_subsumption_resolution,[],[f1599,f611]) ).
fof(f1602,plain,
! [X0] :
( ~ function(sK17(sK1,sK15(X0)))
| ~ in(sK2(sK17(sK1,sK15(X0))),sK1)
| ~ in(sK2(sK17(sK1,sK15(X0))),X0)
| ~ function(sK17(sK1,sK15(X0))) ),
inference(resolution,[],[f1600,f964]) ).
fof(f1603,plain,
! [X0] :
( ~ function(sK17(sK1,sK15(X0)))
| ~ in(sK2(sK17(sK1,sK15(X0))),sK1)
| ~ in(sK2(sK17(sK1,sK15(X0))),X0) ),
inference(duplicate_literal_removal,[],[f1602]) ).
fof(f1605,plain,
! [X0] :
( ~ in(sK2(sK17(sK1,sK15(X0))),X0)
| ~ function(sK17(sK1,sK15(X0))) ),
inference(forward_subsumption_resolution,[],[f1603,f964]) ).
fof(f1606,plain,
( ~ function(sK17(sK1,sK15(sK1)))
| ~ function(sK17(sK1,sK15(sK1))) ),
inference(resolution,[],[f1605,f964]) ).
fof(f1609,plain,
~ function(sK17(sK1,sK15(sK1))),
inference(duplicate_literal_removal,[],[f1606]) ).
fof(f1610,plain,
sK21(sK17(sK1,sK15(sK1))) != sK22(sK17(sK1,sK15(sK1))),
inference(unit_resulting_resolution,[],[f172,f1609]) ).
fof(f1611,plain,
in(unordered_pair(singleton(sK20(sK17(sK1,sK15(sK1)))),unordered_pair(sK20(sK17(sK1,sK15(sK1))),sK22(sK17(sK1,sK15(sK1))))),sK17(sK1,sK15(sK1))),
inference(unit_resulting_resolution,[],[f234,f1609]) ).
fof(f1612,plain,
in(unordered_pair(singleton(sK20(sK17(sK1,sK15(sK1)))),unordered_pair(sK20(sK17(sK1,sK15(sK1))),sK21(sK17(sK1,sK15(sK1))))),sK17(sK1,sK15(sK1))),
inference(unit_resulting_resolution,[],[f235,f1609]) ).
fof(f1629,plain,
sK19(sK1,unordered_pair(singleton(sK20(sK17(sK1,sK15(sK1)))),unordered_pair(sK20(sK17(sK1,sK15(sK1))),sK21(sK17(sK1,sK15(sK1)))))) = singleton(sK18(sK1,unordered_pair(singleton(sK20(sK17(sK1,sK15(sK1)))),unordered_pair(sK20(sK17(sK1,sK15(sK1))),sK21(sK17(sK1,sK15(sK1))))))),
inference(unit_resulting_resolution,[],[f162,f1612]) ).
fof(f1648,plain,
sK20(sK17(sK1,sK15(sK1))) = sK18(sK1,unordered_pair(singleton(sK20(sK17(sK1,sK15(sK1)))),unordered_pair(sK20(sK17(sK1,sK15(sK1))),sK21(sK17(sK1,sK15(sK1)))))),
inference(resolution,[],[f1612,f486]) ).
fof(f1649,plain,
sK21(sK17(sK1,sK15(sK1))) = sK19(sK1,unordered_pair(singleton(sK20(sK17(sK1,sK15(sK1)))),unordered_pair(sK20(sK17(sK1,sK15(sK1))),sK21(sK17(sK1,sK15(sK1)))))),
inference(resolution,[],[f1612,f497]) ).
fof(f1656,plain,
singleton(sK20(sK17(sK1,sK15(sK1)))) = sK19(sK1,unordered_pair(singleton(sK20(sK17(sK1,sK15(sK1)))),unordered_pair(sK20(sK17(sK1,sK15(sK1))),sK21(sK17(sK1,sK15(sK1)))))),
inference(forward_demodulation,[],[f1629,f1648]) ).
fof(f1664,plain,
sK21(sK17(sK1,sK15(sK1))) = singleton(sK20(sK17(sK1,sK15(sK1)))),
inference(forward_demodulation,[],[f1656,f1649]) ).
fof(f1667,plain,
in(unordered_pair(sK21(sK17(sK1,sK15(sK1))),unordered_pair(sK20(sK17(sK1,sK15(sK1))),sK22(sK17(sK1,sK15(sK1))))),sK17(sK1,sK15(sK1))),
inference(backward_demodulation,[],[f1611,f1664]) ).
fof(f1763,plain,
sK19(sK1,unordered_pair(sK21(sK17(sK1,sK15(sK1))),unordered_pair(sK20(sK17(sK1,sK15(sK1))),sK22(sK17(sK1,sK15(sK1)))))) = singleton(sK18(sK1,unordered_pair(sK21(sK17(sK1,sK15(sK1))),unordered_pair(sK20(sK17(sK1,sK15(sK1))),sK22(sK17(sK1,sK15(sK1))))))),
inference(unit_resulting_resolution,[],[f162,f1667]) ).
fof(f1767,plain,
sK19(sK1,unordered_pair(sK21(sK17(sK1,sK15(sK1))),unordered_pair(sK20(sK17(sK1,sK15(sK1))),sK22(sK17(sK1,sK15(sK1)))))) = sK25(unordered_pair(sK21(sK17(sK1,sK15(sK1))),unordered_pair(sK20(sK17(sK1,sK15(sK1))),sK22(sK17(sK1,sK15(sK1)))))),
inference(unit_resulting_resolution,[],[f438,f843,f1667,f1667]) ).
fof(f1768,plain,
sK18(sK1,unordered_pair(sK21(sK17(sK1,sK15(sK1))),unordered_pair(sK20(sK17(sK1,sK15(sK1))),sK22(sK17(sK1,sK15(sK1)))))) = sK24(unordered_pair(sK21(sK17(sK1,sK15(sK1))),unordered_pair(sK20(sK17(sK1,sK15(sK1))),sK22(sK17(sK1,sK15(sK1)))))),
inference(unit_resulting_resolution,[],[f439,f843,f1667,f1667]) ).
fof(f1797,plain,
singleton(sK18(sK1,unordered_pair(sK21(sK17(sK1,sK15(sK1))),unordered_pair(sK20(sK17(sK1,sK15(sK1))),sK22(sK17(sK1,sK15(sK1))))))) = sK25(unordered_pair(sK21(sK17(sK1,sK15(sK1))),unordered_pair(sK20(sK17(sK1,sK15(sK1))),sK22(sK17(sK1,sK15(sK1)))))),
inference(backward_demodulation,[],[f1763,f1767]) ).
fof(f1808,plain,
sK25(unordered_pair(sK21(sK17(sK1,sK15(sK1))),unordered_pair(sK20(sK17(sK1,sK15(sK1))),sK22(sK17(sK1,sK15(sK1)))))) = singleton(sK24(unordered_pair(sK21(sK17(sK1,sK15(sK1))),unordered_pair(sK20(sK17(sK1,sK15(sK1))),sK22(sK17(sK1,sK15(sK1))))))),
inference(forward_demodulation,[],[f1797,f1768]) ).
fof(f1889,plain,
! [X2,X0,X1] :
( sK20(sK17(sK1,sK15(sK1))) = sK18(X1,unordered_pair(sK21(sK17(sK1,sK15(sK1))),unordered_pair(sK20(sK17(sK1,sK15(sK1))),X0)))
| ~ in(unordered_pair(sK21(sK17(sK1,sK15(sK1))),unordered_pair(sK20(sK17(sK1,sK15(sK1))),X0)),sK17(X1,X2)) ),
inference(superposition,[],[f486,f1664]) ).
fof(f1890,plain,
! [X2,X0,X1] :
( ~ in(unordered_pair(sK21(sK17(sK1,sK15(sK1))),unordered_pair(sK20(sK17(sK1,sK15(sK1))),X0)),sK17(X1,X2))
| sK19(X1,unordered_pair(sK21(sK17(sK1,sK15(sK1))),unordered_pair(sK20(sK17(sK1,sK15(sK1))),X0))) = X0 ),
inference(superposition,[],[f497,f1664]) ).
fof(f1915,plain,
sK22(sK17(sK1,sK15(sK1))) = sK19(sK1,unordered_pair(sK21(sK17(sK1,sK15(sK1))),unordered_pair(sK20(sK17(sK1,sK15(sK1))),sK22(sK17(sK1,sK15(sK1)))))),
inference(resolution,[],[f1890,f1667]) ).
fof(f1918,plain,
sK22(sK17(sK1,sK15(sK1))) = sK25(unordered_pair(sK21(sK17(sK1,sK15(sK1))),unordered_pair(sK20(sK17(sK1,sK15(sK1))),sK22(sK17(sK1,sK15(sK1)))))),
inference(backward_demodulation,[],[f1767,f1915]) ).
fof(f1920,plain,
sK22(sK17(sK1,sK15(sK1))) = singleton(sK24(unordered_pair(sK21(sK17(sK1,sK15(sK1))),unordered_pair(sK20(sK17(sK1,sK15(sK1))),sK22(sK17(sK1,sK15(sK1))))))),
inference(backward_demodulation,[],[f1808,f1918]) ).
fof(f9981,plain,
sK20(sK17(sK1,sK15(sK1))) = sK18(sK1,unordered_pair(sK21(sK17(sK1,sK15(sK1))),unordered_pair(sK20(sK17(sK1,sK15(sK1))),sK22(sK17(sK1,sK15(sK1)))))),
inference(unit_resulting_resolution,[],[f1889,f1667]) ).
fof(f10025,plain,
sK20(sK17(sK1,sK15(sK1))) = sK24(unordered_pair(sK21(sK17(sK1,sK15(sK1))),unordered_pair(sK20(sK17(sK1,sK15(sK1))),sK22(sK17(sK1,sK15(sK1)))))),
inference(backward_demodulation,[],[f1768,f9981]) ).
fof(f10040,plain,
sK22(sK17(sK1,sK15(sK1))) = singleton(sK20(sK17(sK1,sK15(sK1)))),
inference(backward_demodulation,[],[f1920,f10025]) ).
fof(f10065,plain,
sK21(sK17(sK1,sK15(sK1))) = sK22(sK17(sK1,sK15(sK1))),
inference(forward_demodulation,[],[f10040,f1664]) ).
fof(f10073,plain,
$false,
inference(forward_subsumption_resolution,[],[f10065,f1610]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU282+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.13/0.38 % Computer : n020.cluster.edu
% 0.13/0.38 % Model : x86_64 x86_64
% 0.13/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.38 % Memory : 8046.5625MB
% 0.13/0.38 % OS : Linux 6.8.0-71-generic
% 0.13/0.39 % CPULimit : 300
% 0.13/0.39 % WCLimit : 300
% 0.13/0.39 % DateTime : Mon Sep 28 04:29:19 UTC 2026
% 0.13/0.39 % CPUTime :
% 0.13/0.39 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.13/0.42 Running first-order theorem proving
% 0.13/0.42 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 14.14/2.97 % (4023259)Detected formulas, will run a generic FOF schedule.
% 14.14/2.97 % (4023270)dis-21_1_sil=8000:lcm=predicate:random_seed=3200666466:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 14.14/2.97 % (4023269)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=114865955:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 14.14/2.97 % (4023266)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=673855390:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 14.14/2.97 % (4023268)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1670247955:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 14.14/2.97 % (4023267)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=167574437:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 14.14/2.97 % (4023264)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=1482362392:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 14.14/2.97 % (4023265)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=3682135583:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 14.14/2.97 % (4023270)Instruction limit reached!
% 14.14/2.97 % (4023270)------------------------------
% 14.14/2.97 % (4023270)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.14/2.97 % (4023270)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.14/2.97 % (4023270)CaDiCaL version: 2.1.3
% 14.14/2.97 % (4023270)Termination reason: Instruction limit
% 14.14/2.97 % (4023270)Termination phase: Saturation
% 14.14/2.97 % (4023270)Time elapsed: 0.043 s
% 14.14/2.97 % (4023270)Peak memory usage: 90 MB
% 14.14/2.97 % (4023270)Instructions burned: 130 (million)
% 14.14/2.97 % (4023267)Refutation not found, incomplete strategy
% 14.14/2.97 % (4023267)------------------------------
% 14.14/2.97 % (4023267)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.14/2.97 % (4023267)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.14/2.97 % (4023267)CaDiCaL version: 2.1.3
% 14.14/2.97 % (4023267)Termination reason: Refutation not found, incomplete strategy
% 14.14/2.97 % (4023267)Time elapsed: 0.004 s
% 14.14/2.97 % (4023267)Peak memory usage: 88 MB
% 14.14/2.97 % (4023267)Instructions burned: 4 (million)
% 14.14/2.97 % (4023268)Instruction limit reached!
% 14.14/2.97 % (4023268)------------------------------
% 14.14/2.97 % (4023268)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.14/2.97 % (4023268)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.14/2.97 % (4023268)CaDiCaL version: 2.1.3
% 14.14/2.97 % (4023268)Termination reason: Instruction limit
% 14.14/2.97 % (4023268)Termination phase: Saturation
% 14.14/2.97 % (4023268)Time elapsed: 0.058 s
% 14.14/2.97 % (4023268)Peak memory usage: 88 MB
% 14.14/2.97 % (4023268)Instructions burned: 119 (million)
% 14.14/2.97 % (4023269)Instruction limit reached!
% 14.14/2.97 % (4023269)------------------------------
% 14.14/2.97 % (4023269)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.14/2.97 % (4023269)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.14/2.97 % (4023269)CaDiCaL version: 2.1.3
% 14.14/2.97 % (4023269)Termination reason: Instruction limit
% 14.14/2.97 % (4023269)Termination phase: Saturation
% 14.14/2.97 % (4023269)Time elapsed: 0.093 s
% 14.14/2.97 % (4023269)Peak memory usage: 89 MB
% 14.14/2.97 % (4023269)Instructions burned: 139 (million)
% 14.14/2.97 % (4023278)lrs+10_1_sil=8000:sp=occurrence:random_seed=142466336:i=285:sd=3:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/285Mi)
% 14.14/2.97 % (4023278)Instruction limit reached!
% 14.14/2.97 % (4023278)------------------------------
% 14.14/2.97 % (4023278)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.14/2.97 % (4023278)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.14/2.97 % (4023278)CaDiCaL version: 2.1.3
% 14.14/2.97 % (4023278)Termination reason: Instruction limit
% 14.14/2.97 % (4023278)Termination phase: Saturation
% 14.14/2.97 % (4023278)Time elapsed: 0.091 s
% 14.14/2.97 % (4023278)Peak memory usage: 91 MB
% 14.14/2.97 % (4023278)Instructions burned: 286 (million)
% 14.14/2.97 % (4023279)lrs+10_1_sil=32000:urr=on:br=off:random_seed=2072948145:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 19.92/3.72 % (4023267)------------------------------
% 19.92/3.72 % (4023267)------------------------------
% 19.92/3.72 % (4023280)lrs+1011_1_sil=32000:sp=occurrence:random_seed=3838502956:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 19.92/3.72 % (4023279)Instruction limit reached!
% 19.92/3.72 % (4023279)------------------------------
% 19.92/3.72 % (4023279)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.92/3.72 % (4023279)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.92/3.72 % (4023279)CaDiCaL version: 2.1.3
% 19.92/3.72 % (4023279)Termination reason: Instruction limit
% 19.92/3.72 % (4023279)Termination phase: Saturation
% 19.92/3.72 % (4023279)Time elapsed: 0.094 s
% 19.92/3.72 % (4023279)Peak memory usage: 90 MB
% 19.92/3.72 % (4023279)Instructions burned: 158 (million)
% 19.92/3.72 % (4023282)dis+10_5:1_slsqr=1,4:sil=8000:fde=unused:erd=off:urr=full:fd=off:s2agt=8:br=off:slsq=on:random_seed=3848453170:s2a=on:i=248:s2at=1.23:gtg=position_2996 on theBenchmark for (2996ds/248Mi)
% 19.92/3.72 % (4023282)Instruction limit reached!
% 19.92/3.72 % (4023282)------------------------------
% 19.92/3.72 % (4023282)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.92/3.72 % (4023282)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.92/3.72 % (4023282)CaDiCaL version: 2.1.3
% 19.92/3.72 % (4023282)Termination reason: Instruction limit
% 19.92/3.72 % (4023282)Termination phase: Saturation
% 19.92/3.72 % (4023282)Time elapsed: 0.075 s
% 19.92/3.72 % (4023282)Peak memory usage: 94 MB
% 19.92/3.72 % (4023282)Instructions burned: 250 (million)
% 19.92/3.72 % (4023285)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=3889715684:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2995 on theBenchmark for (2995ds/294Mi)
% 19.92/3.72 % (4023285)Refutation not found, incomplete strategy
% 19.92/3.72 % (4023285)------------------------------
% 19.92/3.72 % (4023285)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.92/3.72 % (4023285)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.92/3.72 % (4023285)CaDiCaL version: 2.1.3
% 19.92/3.72 % (4023285)Termination reason: Refutation not found, incomplete strategy
% 19.92/3.72 % (4023285)Time elapsed: 0.005 s
% 19.92/3.72 % (4023285)Peak memory usage: 89 MB
% 19.92/3.72 % (4023285)Instructions burned: 5 (million)
% 19.92/3.72 % (4023280)Instruction limit reached!
% 19.92/3.72 % (4023280)------------------------------
% 19.92/3.72 % (4023280)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.92/3.72 % (4023280)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.92/3.72 % (4023280)CaDiCaL version: 2.1.3
% 19.92/3.72 % (4023280)Termination reason: Instruction limit
% 19.92/3.72 % (4023280)Termination phase: Saturation
% 19.92/3.72 % (4023280)Time elapsed: 0.194 s
% 19.92/3.72 % (4023280)Peak memory usage: 91 MB
% 19.92/3.72 % (4023280)Instructions burned: 325 (million)
% 19.92/3.72 % (4023286)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=1275029164:i=2350_2995 on theBenchmark for (2995ds/2350Mi)
% 19.92/3.72 % (4023289)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=2692261345:cts=off:i=113:fsr=off:ss=included:sgt=4_2994 on theBenchmark for (2994ds/113Mi)
% 19.92/3.72 % (4023289)Instruction limit reached!
% 19.92/3.72 % (4023289)------------------------------
% 19.92/3.72 % (4023289)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.92/3.72 % (4023289)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.92/3.72 % (4023289)CaDiCaL version: 2.1.3
% 19.92/3.72 % (4023289)Termination reason: Instruction limit
% 19.92/3.72 % (4023289)Termination phase: Saturation
% 19.92/3.72 % (4023289)Time elapsed: 0.044 s
% 19.92/3.72 % (4023289)Peak memory usage: 90 MB
% 19.92/3.72 % (4023289)Instructions burned: 115 (million)
% 19.92/3.72 % (4023290)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=2172837528:i=127:av=off:fsr=off:sup=off_2993 on theBenchmark for (2993ds/127Mi)
% 19.92/3.72 % (4023285)------------------------------
% 19.92/3.72 % (4023285)------------------------------
% 19.92/3.72 % (4023290)Instruction limit reached!
% 19.92/3.72 % (4023290)------------------------------
% 19.92/3.72 % (4023290)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.92/3.72 % (4023290)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.65/5.74 % (4023290)CaDiCaL version: 2.1.3
% 34.65/5.74 % (4023290)Termination reason: Instruction limit
% 34.65/5.74 % (4023290)Termination phase: Saturation
% 34.65/5.74 % (4023290)Time elapsed: 0.064 s
% 34.65/5.74 % (4023290)Peak memory usage: 88 MB
% 34.65/5.74 % (4023290)Instructions burned: 128 (million)
% 34.65/5.74 % (4023293)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=1694245277:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2992 on theBenchmark for (2992ds/114Mi)
% 34.65/5.74 % (4023293)Instruction limit reached!
% 34.65/5.74 % (4023293)------------------------------
% 34.65/5.74 % (4023293)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.65/5.74 % (4023293)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.65/5.74 % (4023293)CaDiCaL version: 2.1.3
% 34.65/5.74 % (4023293)Termination reason: Instruction limit
% 34.65/5.74 % (4023293)Termination phase: Saturation
% 34.65/5.74 % (4023293)Time elapsed: 0.032 s
% 34.65/5.74 % (4023293)Peak memory usage: 89 MB
% 34.65/5.74 % (4023293)Instructions burned: 115 (million)
% 34.65/5.74 % (4023295)lrs+10_1_sil=8000:sp=occurrence:random_seed=2888620337:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2991 on theBenchmark for (2991ds/907Mi)
% 34.65/5.74 % (4023296)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=874654400:i=437:sd=1:aac=none:ss=included_2991 on theBenchmark for (2991ds/437Mi)
% 34.65/5.74 % (4023298)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=3981020827:i=5202:ss=axioms:sgt=16_2990 on theBenchmark for (2990ds/5202Mi)
% 34.65/5.74 % (4023296)Instruction limit reached!
% 34.65/5.74 % (4023296)------------------------------
% 34.65/5.74 % (4023296)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.65/5.74 % (4023296)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.65/5.74 % (4023296)CaDiCaL version: 2.1.3
% 34.65/5.74 % (4023296)Termination reason: Instruction limit
% 34.65/5.74 % (4023296)Termination phase: Saturation
% 34.65/5.74 % (4023296)Time elapsed: 0.255 s
% 34.65/5.74 % (4023296)Peak memory usage: 90 MB
% 34.65/5.74 % (4023296)Instructions burned: 437 (million)
% 34.65/5.74 % (4023302)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=447381437:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2987 on theBenchmark for (2987ds/134Mi)
% 34.65/5.74 % (4023295)Instruction limit reached!
% 34.65/5.74 % (4023295)------------------------------
% 34.65/5.74 % (4023295)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.65/5.74 % (4023295)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.65/5.74 % (4023295)CaDiCaL version: 2.1.3
% 34.65/5.74 % (4023295)Termination reason: Instruction limit
% 34.65/5.74 % (4023295)Termination phase: Saturation
% 34.65/5.74 % (4023295)Time elapsed: 0.493 s
% 34.65/5.74 % (4023295)Peak memory usage: 97 MB
% 34.65/5.74 % (4023295)Instructions burned: 908 (million)
% 34.65/5.74 % (4023302)Instruction limit reached!
% 34.65/5.74 % (4023302)------------------------------
% 34.65/5.74 % (4023302)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.65/5.74 % (4023302)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.65/5.74 % (4023302)CaDiCaL version: 2.1.3
% 34.65/5.74 % (4023302)Termination reason: Instruction limit
% 34.65/5.74 % (4023302)Termination phase: Saturation
% 34.65/5.74 % (4023302)Time elapsed: 0.073 s
% 34.65/5.74 % (4023302)Peak memory usage: 92 MB
% 34.65/5.74 % (4023302)Instructions burned: 134 (million)
% 34.65/5.74 % (4023305)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=928252826:st=3:i=13193:sd=3:ss=axioms_2985 on theBenchmark for (2985ds/13193Mi)
% 34.65/5.74 % (4023304)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=2291043737:st=8:i=592:sd=3:ep=RST:ss=axioms_2985 on theBenchmark for (2985ds/592Mi)
% 34.65/5.74 % (4023304)Instruction limit reached!
% 34.65/5.74 % (4023304)------------------------------
% 34.65/5.74 % (4023304)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.65/5.74 % (4023304)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.65/5.74 % (4023304)CaDiCaL version: 2.1.3
% 34.65/5.74 % (4023304)Termination reason: Instruction limit
% 34.65/5.74 % (4023304)Termination phase: Saturation
% 34.65/5.74 % (4023304)Time elapsed: 0.279 s
% 34.65/5.74 % (4023304)Peak memory usage: 90 MB
% 34.65/5.74 % (4023304)Instructions burned: 592 (million)
% 34.65/5.74 % (4023308)lrs+1666_7_slsqr=4,1:sil=8000:plsq=on:plsqc=1:sos=on:urr=on:plsql=on:rp=on:alpa=false:sac=on:slsq=on:random_seed=44301931:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2980 on theBenchmark for (2980ds/125Mi)
% 34.65/5.74 % (4023286)Instruction limit reached!
% 34.65/5.74 % (4023286)------------------------------
% 34.65/5.74 % (4023286)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.65/5.74 % (4023286)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.65/5.74 % (4023286)CaDiCaL version: 2.1.3
% 34.65/5.74 % (4023286)Termination reason: Instruction limit
% 34.65/5.74 % (4023286)Termination phase: Saturation
% 34.65/5.74 % (4023286)Time elapsed: 1.486 s
% 34.65/5.74 % (4023286)Peak memory usage: 141 MB
% 34.65/5.74 % (4023286)Instructions burned: 2350 (million)
% 34.65/5.74 % (4023308)Instruction limit reached!
% 34.65/5.74 % (4023308)------------------------------
% 34.65/5.74 % (4023308)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.65/5.74 % (4023308)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.65/5.74 % (4023308)CaDiCaL version: 2.1.3
% 34.65/5.74 % (4023308)Termination reason: Instruction limit
% 34.65/5.74 % (4023308)Termination phase: Saturation
% 34.65/5.74 % (4023308)Time elapsed: 0.075 s
% 34.65/5.74 % (4023308)Peak memory usage: 92 MB
% 34.65/5.74 % (4023308)Instructions burned: 125 (million)
% 34.65/5.74 % (4023310)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=4093532586:i=134:gtgl=5:slsql=off:gtg=exists_sym_2978 on theBenchmark for (2978ds/134Mi)
% 34.65/5.74 % (4023311)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=1728561846:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2978 on theBenchmark for (2978ds/141Mi)
% 34.65/5.74 % (4023310)Instruction limit reached!
% 34.65/5.74 % (4023310)------------------------------
% 34.65/5.74 % (4023310)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.65/5.74 % (4023310)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.65/5.74 % (4023310)CaDiCaL version: 2.1.3
% 34.65/5.74 % (4023310)Termination reason: Instruction limit
% 34.65/5.74 % (4023310)Termination phase: Saturation
% 34.65/5.74 % (4023310)Time elapsed: 0.074 s
% 34.65/5.74 % (4023310)Peak memory usage: 90 MB
% 34.65/5.74 % (4023310)Instructions burned: 134 (million)
% 34.65/5.74 % (4023311)Instruction limit reached!
% 34.65/5.74 % (4023311)------------------------------
% 34.65/5.74 % (4023311)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.65/5.74 % (4023311)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.65/5.74 % (4023311)CaDiCaL version: 2.1.3
% 34.65/5.74 % (4023311)Termination reason: Instruction limit
% 34.65/5.74 % (4023311)Termination phase: Saturation
% 34.65/5.74 % (4023311)Time elapsed: 0.079 s
% 34.65/5.74 % (4023311)Peak memory usage: 89 MB
% 34.65/5.74 % (4023311)Instructions burned: 141 (million)
% 34.65/5.74 % (4023314)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=3853107995:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2976 on theBenchmark for (2976ds/431Mi)
% 34.65/5.74 % (4023315)lrs+1010_1_ncem=casc2026/models/loop6.pt:sil=64000:tgt=full:npcc=on:prc=on:urr=ec_only:bsr=on:fd=preordered:gs=on:sac=on:newcnf=on:random_seed=3352903385:i=6060:aac=none:ins=25_2975 on theBenchmark for (2975ds/6060Mi)
% 34.65/5.74 % (4023298)Instruction limit reached!
% 34.65/5.74 % (4023298)------------------------------
% 34.65/5.74 % (4023298)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.65/5.74 % (4023298)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.65/5.74 % (4023298)CaDiCaL version: 2.1.3
% 34.65/5.74 % (4023298)Termination reason: Instruction limit
% 34.65/5.74 % (4023298)Termination phase: Saturation
% 34.65/5.74 % (4023298)Time elapsed: 1.698 s
% 34.65/5.74 % (4023298)Peak memory usage: 159 MB
% 34.65/5.74 % (4023298)Instructions burned: 5205 (million)
% 34.65/5.74 % (4023314)Instruction limit reached!
% 34.65/5.74 % (4023314)------------------------------
% 34.65/5.74 % (4023314)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.65/5.74 % (4023314)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.65/5.74 % (4023314)CaDiCaL version: 2.1.3
% 34.65/5.74 % (4023314)Termination reason: Instruction limit
% 34.65/5.74 % (4023314)Termination phase: Saturation
% 34.65/5.74 % (4023314)Time elapsed: 0.212 s
% 34.65/5.74 % (4023314)Peak memory usage: 94 MB
% 34.65/5.74 % (4023314)Instructions burned: 432 (million)
% 34.65/5.74 % (4023318)lrs+10_16_anc=all:slsqr=32,1:sil=8000:avsql=on:sp=unary_frequency:lcm=predicate:urr=full:rp=on:br=off:slsqc=4:flr=on:sac=on:slsq=on:avsqc=1:random_seed=1133943061:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2972 on theBenchmark for (2972ds/150Mi)
% 34.65/5.74 % (4023318)Instruction limit reached!
% 34.65/5.74 % (4023318)------------------------------
% 34.65/5.74 % (4023318)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.65/5.74 % (4023318)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.65/5.74 % (4023318)CaDiCaL version: 2.1.3
% 34.65/5.74 % (4023318)Termination reason: Instruction limit
% 34.65/5.74 % (4023318)Termination phase: Saturation
% 34.65/5.74 % (4023318)Time elapsed: 0.045 s
% 34.65/5.74 % (4023318)Peak memory usage: 90 MB
% 34.65/5.74 % (4023318)Instructions burned: 151 (million)
% 34.65/5.74 % (4023319)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=2658889890:i=14155:bd=all_2972 on theBenchmark for (2972ds/14155Mi)
% 34.65/5.74 % (4023321)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=1864773866:i=667:av=off:fsr=off_2970 on theBenchmark for (2970ds/667Mi)
% 34.65/5.74 % (4023321)Instruction limit reached!
% 34.65/5.74 % (4023321)------------------------------
% 34.65/5.74 % (4023321)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.65/5.74 % (4023321)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.65/5.74 % (4023321)CaDiCaL version: 2.1.3
% 34.65/5.74 % (4023321)Termination reason: Instruction limit
% 34.65/5.74 % (4023321)Termination phase: Saturation
% 34.65/5.74 % (4023321)Time elapsed: 0.167 s
% 34.65/5.74 % (4023321)Peak memory usage: 90 MB
% 34.65/5.74 % (4023321)Instructions burned: 668 (million)
% 34.65/5.74 % (4023324)ott-1011_3:1_anc=all_dependent:to=lpo:sil=8000:drc=ordering:sas=cadical:fdtod=off:sp=reverse_frequency:spb=goal_then_units:urr=full:lftc=20:newcnf=on:random_seed=293961310:s2a=on:i=185:s2at=1.8:fdi=4_2968 on theBenchmark for (2968ds/185Mi)
% 34.65/5.74 % (4023324)Instruction limit reached!
% 34.65/5.74 % (4023324)------------------------------
% 34.65/5.74 % (4023324)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.65/5.74 % (4023324)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.65/5.74 % (4023324)CaDiCaL version: 2.1.3
% 34.65/5.74 % (4023324)Termination reason: Instruction limit
% 34.65/5.74 % (4023324)Termination phase: Saturation
% 34.65/5.74 % (4023324)Time elapsed: 0.060 s
% 34.65/5.74 % (4023324)Peak memory usage: 91 MB
% 34.65/5.74 % (4023324)Instructions burned: 186 (million)
% 34.65/5.74 % (4023326)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=1653990554:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2966 on theBenchmark for (2966ds/193Mi)
% 34.65/5.74 % (4023326)Instruction limit reached!
% 34.65/5.74 % (4023326)------------------------------
% 34.65/5.74 % (4023326)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.65/5.74 % (4023326)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.65/5.74 % (4023326)CaDiCaL version: 2.1.3
% 34.65/5.74 % (4023326)Termination reason: Instruction limit
% 34.65/5.74 % (4023326)Termination phase: Saturation
% 34.65/5.74 % (4023326)Time elapsed: 0.054 s
% 34.65/5.74 % (4023326)Peak memory usage: 90 MB
% 34.65/5.74 % (4023326)Instructions burned: 197 (million)
% 34.65/5.74 % (4023328)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=103702936:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2964 on theBenchmark for (2964ds/4850Mi)
% 34.65/5.74 % (4023319)First to succeed.
% 34.65/5.74 % (4023319)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-4023259"
% 34.65/5.74 % (4023319)Refutation found. Thanks to Tanya!
% 34.65/5.74 % SZS status Theorem for theBenchmark
% 34.65/5.74 % SZS output start Proof for theBenchmark
% See solution above
% 35.14/5.94 % (4023319)------------------------------
% 35.14/5.94 % (4023319)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.14/5.94 % (4023319)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.14/5.94 % (4023319)CaDiCaL version: 2.1.3
% 35.14/5.94 % (4023319)Termination reason: Refutation
% 35.14/5.94 % (4023319)Time elapsed: 1.652 s
% 35.14/5.94 % (4023319)Peak memory usage: 142 MB
% 35.14/5.94 % (4023319)Instructions burned: 2658 (million)
% 35.14/5.94 % (4023319)------------------------------
% 35.14/5.94 % (4023319)------------------------------
% 35.14/5.94 % (4023259)Success in time 4.873 s
% 35.14/5.94 % Vampire exiting
%------------------------------------------------------------------------------