%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SCT161+1 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n012.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:37:37 PM UTC 2026
% Result : ContradictoryAxioms 16.27s 2.85s
% Output : Refutation 16.27s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 16
% Syntax : Number of formulae : 68 ( 32 unt; 2 def)
% Number of atoms : 134 ( 38 equ)
% Maximal formula atoms : 6 ( 1 avg)
% Number of connectives : 115 ( 49 ~; 43 |; 12 &)
% ( 4 <=>; 7 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 5 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 5 ( 3 usr; 1 prp; 0-2 aty)
% Number of functors : 17 ( 17 usr; 5 con; 0-4 aty)
% Number of variables : 170 ( 163 !; 7 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] :
( ! [X2] : hAPP(X1,X2) = hAPP(X0,X2)
=> X1 = X0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_ext) ).
fof(f5,axiom,
! [X0,X1,X2] :
( class_Orderings_Otop(X2)
=> hAPP(c_Orderings_Otop__class_Otop(tc_fun(X1,X2)),X0) = c_Orderings_Otop__class_Otop(X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_top__apply) ).
fof(f68,axiom,
! [X0,X1,X2] :
( hBOOL(hAPP(hAPP(c_member(X2),X1),X0))
<=> hBOOL(hAPP(X0,X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_mem__def) ).
fof(f70,axiom,
! [X0,X1] : c_Set_Oimage(X1,X1,c_COMBI(X1),X0) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_image__ident) ).
fof(f81,axiom,
! [X0,X1,X2,X3,X4] : c_Set_Oimage(X4,X3,hAPP(c_COMBB(X2,X3,X4,X1),X0),c_Orderings_Otop__class_Otop(tc_fun(X4,tc_HOL_Obool))) = c_Set_Oimage(X2,X3,X1,c_Set_Oimage(X4,X2,X0,c_Orderings_Otop__class_Otop(tc_fun(X4,tc_HOL_Obool)))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_range__composition) ).
fof(f83,axiom,
! [X0,X1,X2,X3,X4] :
( X4 = hAPP(X3,X2)
=> hBOOL(hAPP(hAPP(c_member(X1),X4),c_Set_Oimage(X0,X1,X3,c_Orderings_Otop__class_Otop(tc_fun(X0,tc_HOL_Obool))))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_range__eqI) ).
fof(f156,axiom,
! [X0,X1,X2] :
( c_Finite__Set_Ofinite(X2,X1)
=> ( hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(X2,tc_HOL_Obool),X0),X1))
=> c_Finite__Set_Ofinite(X2,X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_rev__finite__subset) ).
fof(f211,axiom,
! [X0,X1] : hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(X1,tc_HOL_Obool),X0),c_Orderings_Otop__class_Otop(tc_fun(X1,tc_HOL_Obool)))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_subset__UNIV) ).
fof(f216,axiom,
! [X0] :
( c_Finite__Set_Ofinite(tc_Nat_Onat,X0)
<=> ? [X1] :
! [X2] :
( hBOOL(hAPP(hAPP(c_member(tc_Nat_Onat),X2),X0))
=> hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),X2),X1)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_finite__nat__set__iff__bounded) ).
fof(f227,axiom,
c_Finite__Set_Ofinite(tc_Arrow__Order__Mirabelle_Oindi,c_Orderings_Otop__class_Otop(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_HOL_Obool))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_finite__indi) ).
fof(f231,axiom,
! [X0,X1,X2,X3,X4] :
( c_Finite__Set_Ofinite(X4,c_Set_Oimage(X3,X4,X2,c_Orderings_Otop__class_Otop(tc_fun(X3,tc_HOL_Obool))))
=> c_Finite__Set_Ofinite(X1,c_Set_Oimage(X3,X1,hAPP(c_COMBB(X4,X1,X3,X0),X2),c_Orderings_Otop__class_Otop(tc_fun(X3,tc_HOL_Obool)))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_finite__range__imageI) ).
fof(f258,axiom,
! [X0,X1] :
( hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),X1),X0))
<=> ( hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,X1),X0))
& X1 != X0 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_nat__less__le) ).
fof(f520,axiom,
class_Orderings_Otop(tc_HOL_Obool),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',arity_HOL__Obool__Orderings_Otop) ).
fof(f526,axiom,
! [X0,X1] : hAPP(c_COMBI(X1),X0) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',help_c__COMBI__1) ).
fof(f555,plain,
! [X0,X1] :
( X1 = X0
| ? [X2] : hAPP(X1,X2) != hAPP(X0,X2) ),
inference(ennf_transformation,[],[f1]) ).
fof(f556,plain,
! [X0,X1,X2] :
( hAPP(c_Orderings_Otop__class_Otop(tc_fun(X1,X2)),X0) = c_Orderings_Otop__class_Otop(X2)
| ~ class_Orderings_Otop(X2) ),
inference(ennf_transformation,[],[f5]) ).
fof(f639,plain,
! [X0,X1,X2,X3,X4] :
( hBOOL(hAPP(hAPP(c_member(X1),X4),c_Set_Oimage(X0,X1,X3,c_Orderings_Otop__class_Otop(tc_fun(X0,tc_HOL_Obool)))))
| hAPP(X3,X2) != X4 ),
inference(ennf_transformation,[],[f83]) ).
fof(f720,plain,
! [X0,X1,X2] :
( c_Finite__Set_Ofinite(X2,X0)
| ~ hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(X2,tc_HOL_Obool),X0),X1))
| ~ c_Finite__Set_Ofinite(X2,X1) ),
inference(ennf_transformation,[],[f156]) ).
fof(f721,plain,
! [X0,X1,X2] :
( c_Finite__Set_Ofinite(X2,X0)
| ~ hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(X2,tc_HOL_Obool),X0),X1))
| ~ c_Finite__Set_Ofinite(X2,X1) ),
inference(flattening,[],[f720]) ).
fof(f815,plain,
! [X0] :
( c_Finite__Set_Ofinite(tc_Nat_Onat,X0)
<=> ? [X1] :
! [X2] :
( hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),X2),X1))
| ~ hBOOL(hAPP(hAPP(c_member(tc_Nat_Onat),X2),X0)) ) ),
inference(ennf_transformation,[],[f216]) ).
fof(f832,plain,
! [X0,X1,X2,X3,X4] :
( c_Finite__Set_Ofinite(X1,c_Set_Oimage(X3,X1,hAPP(c_COMBB(X4,X1,X3,X0),X2),c_Orderings_Otop__class_Otop(tc_fun(X3,tc_HOL_Obool))))
| ~ c_Finite__Set_Ofinite(X4,c_Set_Oimage(X3,X4,X2,c_Orderings_Otop__class_Otop(tc_fun(X3,tc_HOL_Obool)))) ),
inference(ennf_transformation,[],[f231]) ).
fof(f1056,plain,
! [X0,X1] :
( X1 = X0
| hAPP(X1,sK2(X0,X1)) != hAPP(X0,sK2(X0,X1)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2]),skolemize(X2,sK2(X0,X1))],[f555]) ).
fof(f1081,plain,
! [X0,X1,X2] :
( ( hBOOL(hAPP(hAPP(c_member(X2),X1),X0))
| ~ hBOOL(hAPP(X0,X1)) )
& ( hBOOL(hAPP(X0,X1))
| ~ hBOOL(hAPP(hAPP(c_member(X2),X1),X0)) ) ),
inference(nnf_transformation,[],[f68]) ).
fof(f1164,plain,
! [X0] :
( ( c_Finite__Set_Ofinite(tc_Nat_Onat,X0)
| ! [X1] :
? [X2] :
( ~ hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),X2),X1))
& hBOOL(hAPP(hAPP(c_member(tc_Nat_Onat),X2),X0)) ) )
& ( ? [X1] :
! [X2] :
( hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),X2),X1))
| ~ hBOOL(hAPP(hAPP(c_member(tc_Nat_Onat),X2),X0)) )
| ~ c_Finite__Set_Ofinite(tc_Nat_Onat,X0) ) ),
inference(nnf_transformation,[],[f815]) ).
fof(f1165,plain,
! [X0] :
( ( c_Finite__Set_Ofinite(tc_Nat_Onat,X0)
| ! [X1] :
? [X2] :
( ~ hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),X2),X1))
& hBOOL(hAPP(hAPP(c_member(tc_Nat_Onat),X2),X0)) ) )
& ( ? [X3] :
! [X4] :
( hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),X4),X3))
| ~ hBOOL(hAPP(hAPP(c_member(tc_Nat_Onat),X4),X0)) )
| ~ c_Finite__Set_Ofinite(tc_Nat_Onat,X0) ) ),
inference(rectify,[],[f1164]) ).
fof(f1166,plain,
! [X0] :
( ( c_Finite__Set_Ofinite(tc_Nat_Onat,X0)
| ! [X1] :
( ~ hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),sK30(X0,X1)),X1))
& hBOOL(hAPP(hAPP(c_member(tc_Nat_Onat),sK30(X0,X1)),X0)) ) )
& ( ! [X4] :
( hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),X4),sK31(X0)))
| ~ hBOOL(hAPP(hAPP(c_member(tc_Nat_Onat),X4),X0)) )
| ~ c_Finite__Set_Ofinite(tc_Nat_Onat,X0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK30,sK31]),skolemize(X2,sK30(X0,X1)),skolemize(X3,sK31(X0))],[f1165]) ).
fof(f1187,plain,
! [X0,X1] :
( ( hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),X1),X0))
| ~ hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,X1),X0))
| X0 = X1 )
& ( ( hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,X1),X0))
& X1 != X0 )
| ~ hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),X1),X0)) ) ),
inference(nnf_transformation,[],[f258]) ).
fof(f1188,plain,
! [X0,X1] :
( ( hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),X1),X0))
| ~ hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,X1),X0))
| X0 = X1 )
& ( ( hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,X1),X0))
& X1 != X0 )
| ~ hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),X1),X0)) ) ),
inference(flattening,[],[f1187]) ).
fof(f1284,plain,
! [X0,X1] :
( hAPP(X1,sK2(X0,X1)) != hAPP(X0,sK2(X0,X1))
| X0 = X1 ),
inference(cnf_transformation,[],[f1056]) ).
fof(f1288,plain,
! [X2,X0,X1] :
( ~ class_Orderings_Otop(X2)
| hAPP(c_Orderings_Otop__class_Otop(tc_fun(X1,X2)),X0) = c_Orderings_Otop__class_Otop(X2) ),
inference(cnf_transformation,[],[f556]) ).
fof(f1385,plain,
! [X2,X0,X1] :
( ~ hBOOL(hAPP(hAPP(c_member(X2),X1),X0))
| hBOOL(hAPP(X0,X1)) ),
inference(cnf_transformation,[],[f1081]) ).
fof(f1386,plain,
! [X2,X0,X1] :
( hBOOL(hAPP(hAPP(c_member(X2),X1),X0))
| ~ hBOOL(hAPP(X0,X1)) ),
inference(cnf_transformation,[],[f1081]) ).
fof(f1392,plain,
! [X0,X1] : c_Set_Oimage(X1,X1,c_COMBI(X1),X0) = X0,
inference(cnf_transformation,[],[f70]) ).
fof(f1407,plain,
! [X2,X3,X0,X1,X4] : c_Set_Oimage(X4,X3,hAPP(c_COMBB(X2,X3,X4,X1),X0),c_Orderings_Otop__class_Otop(tc_fun(X4,tc_HOL_Obool))) = c_Set_Oimage(X2,X3,X1,c_Set_Oimage(X4,X2,X0,c_Orderings_Otop__class_Otop(tc_fun(X4,tc_HOL_Obool)))),
inference(cnf_transformation,[],[f81]) ).
fof(f1409,plain,
! [X2,X3,X0,X1,X4] :
( hBOOL(hAPP(hAPP(c_member(X1),X4),c_Set_Oimage(X0,X1,X3,c_Orderings_Otop__class_Otop(tc_fun(X0,tc_HOL_Obool)))))
| hAPP(X3,X2) != X4 ),
inference(cnf_transformation,[],[f639]) ).
fof(f1561,plain,
! [X2,X0,X1] :
( ~ hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(X2,tc_HOL_Obool),X0),X1))
| c_Finite__Set_Ofinite(X2,X0)
| ~ c_Finite__Set_Ofinite(X2,X1) ),
inference(cnf_transformation,[],[f721]) ).
fof(f1636,plain,
! [X0,X1] : hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(X1,tc_HOL_Obool),X0),c_Orderings_Otop__class_Otop(tc_fun(X1,tc_HOL_Obool)))),
inference(cnf_transformation,[],[f211]) ).
fof(f1643,plain,
! [X0,X4] :
( hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),X4),sK31(X0)))
| ~ hBOOL(hAPP(hAPP(c_member(tc_Nat_Onat),X4),X0))
| ~ c_Finite__Set_Ofinite(tc_Nat_Onat,X0) ),
inference(cnf_transformation,[],[f1166]) ).
fof(f1663,plain,
c_Finite__Set_Ofinite(tc_Arrow__Order__Mirabelle_Oindi,c_Orderings_Otop__class_Otop(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_HOL_Obool))),
inference(cnf_transformation,[],[f227]) ).
fof(f1667,plain,
! [X2,X3,X0,X1,X4] :
( ~ c_Finite__Set_Ofinite(X4,c_Set_Oimage(X3,X4,X2,c_Orderings_Otop__class_Otop(tc_fun(X3,tc_HOL_Obool))))
| c_Finite__Set_Ofinite(X1,c_Set_Oimage(X3,X1,hAPP(c_COMBB(X4,X1,X3,X0),X2),c_Orderings_Otop__class_Otop(tc_fun(X3,tc_HOL_Obool)))) ),
inference(cnf_transformation,[],[f832]) ).
fof(f1706,plain,
! [X0,X1] :
( X0 != X1
| ~ hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),X1),X0)) ),
inference(cnf_transformation,[],[f1188]) ).
fof(f2054,plain,
class_Orderings_Otop(tc_HOL_Obool),
inference(cnf_transformation,[],[f520]) ).
fof(f2060,plain,
! [X0,X1] : hAPP(c_COMBI(X1),X0) = X0,
inference(cnf_transformation,[],[f526]) ).
fof(f2108,plain,
! [X2,X3,X0,X1] : hBOOL(hAPP(hAPP(c_member(X1),hAPP(X3,X2)),c_Set_Oimage(X0,X1,X3,c_Orderings_Otop__class_Otop(tc_fun(X0,tc_HOL_Obool))))),
inference(equality_resolution,[],[f1409]) ).
fof(f2165,plain,
! [X1] : ~ hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),X1),X1)),
inference(equality_resolution,[],[f1706]) ).
fof(f2221,definition,
sF53 = tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_HOL_Obool),
introduced(definition,[new_symbols(definition,[sF53])],[function_definition]) ).
fof(f2222,plain,
tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_HOL_Obool) = sF53,
inference(reorient_equations,[],[f2221]) ).
fof(f2223,definition,
sF54 = c_Orderings_Otop__class_Otop(sF53),
introduced(definition,[new_symbols(definition,[sF54])],[function_definition]) ).
fof(f2224,plain,
c_Orderings_Otop__class_Otop(sF53) = sF54,
inference(reorient_equations,[],[f2223]) ).
fof(f2323,plain,
! [X0,X1] : hAPP(c_Orderings_Otop__class_Otop(tc_fun(X0,tc_HOL_Obool)),X1) = c_Orderings_Otop__class_Otop(tc_HOL_Obool),
inference(resolution,[],[f1288,f2054]) ).
fof(f2327,plain,
! [X0] : hAPP(c_Orderings_Otop__class_Otop(sF53),X0) = c_Orderings_Otop__class_Otop(tc_HOL_Obool),
inference(superposition,[],[f2323,f2222]) ).
fof(f2329,plain,
! [X0] : hAPP(sF54,X0) = c_Orderings_Otop__class_Otop(tc_HOL_Obool),
inference(forward_demodulation,[],[f2327,f2224]) ).
fof(f2548,plain,
! [X0] :
( c_Orderings_Otop__class_Otop(tc_HOL_Obool) != hAPP(X0,sK2(X0,sF54))
| sF54 = X0 ),
inference(superposition,[],[f1284,f2329]) ).
fof(f2574,plain,
! [X0,X1] :
( ~ c_Finite__Set_Ofinite(X0,c_Orderings_Otop__class_Otop(tc_fun(X0,tc_HOL_Obool)))
| c_Finite__Set_Ofinite(X0,X1) ),
inference(resolution,[],[f1561,f1636]) ).
fof(f2581,plain,
! [X0] : c_Finite__Set_Ofinite(tc_Arrow__Order__Mirabelle_Oindi,X0),
inference(resolution,[],[f2574,f1663]) ).
fof(f4276,plain,
! [X2,X3,X0,X1] : hBOOL(hAPP(c_Set_Oimage(X0,X1,X2,c_Orderings_Otop__class_Otop(tc_fun(X0,tc_HOL_Obool))),hAPP(X2,X3))),
inference(resolution,[],[f2108,f1385]) ).
fof(f5429,plain,
! [X0] :
( ~ hBOOL(hAPP(hAPP(c_member(tc_Nat_Onat),sK31(X0)),X0))
| ~ c_Finite__Set_Ofinite(tc_Nat_Onat,X0) ),
inference(resolution,[],[f1643,f2165]) ).
fof(f5466,plain,
! [X0] :
( ~ hBOOL(hAPP(X0,sK31(X0)))
| ~ c_Finite__Set_Ofinite(tc_Nat_Onat,X0) ),
inference(resolution,[],[f5429,f1386]) ).
fof(f6600,plain,
! [X0] :
( c_Orderings_Otop__class_Otop(tc_HOL_Obool) != c_Orderings_Otop__class_Otop(tc_HOL_Obool)
| c_Orderings_Otop__class_Otop(tc_fun(X0,tc_HOL_Obool)) = sF54 ),
inference(superposition,[],[f2548,f2323]) ).
fof(f6606,plain,
! [X0] : c_Orderings_Otop__class_Otop(tc_fun(X0,tc_HOL_Obool)) = sF54,
inference(trivial_inequality_removal,[],[f6600]) ).
fof(f12496,plain,
! [X2,X3,X0,X1] : c_Finite__Set_Ofinite(X0,c_Set_Oimage(X1,X0,hAPP(c_COMBB(tc_Arrow__Order__Mirabelle_Oindi,X0,X1,X2),X3),c_Orderings_Otop__class_Otop(tc_fun(X1,tc_HOL_Obool)))),
inference(resolution,[],[f1667,f2581]) ).
fof(f12563,plain,
! [X2,X3,X0,X1] : c_Finite__Set_Ofinite(X0,c_Set_Oimage(tc_Arrow__Order__Mirabelle_Oindi,X0,X2,c_Set_Oimage(X1,tc_Arrow__Order__Mirabelle_Oindi,X3,c_Orderings_Otop__class_Otop(tc_fun(X1,tc_HOL_Obool))))),
inference(forward_demodulation,[],[f12496,f1407]) ).
fof(f12578,plain,
! [X2,X3,X0,X1] : c_Finite__Set_Ofinite(X0,c_Set_Oimage(tc_Arrow__Order__Mirabelle_Oindi,X0,X2,c_Set_Oimage(X1,tc_Arrow__Order__Mirabelle_Oindi,X3,sF54))),
inference(forward_demodulation,[],[f12563,f6606]) ).
fof(f16307,plain,
! [X0,X1] : c_Finite__Set_Ofinite(X0,c_Set_Oimage(tc_Arrow__Order__Mirabelle_Oindi,X0,X1,sF54)),
inference(superposition,[],[f12578,f1392]) ).
fof(f30316,plain,
! [X2,X3,X0,X1] : hBOOL(hAPP(c_Set_Oimage(X1,X2,c_COMBI(X3),c_Orderings_Otop__class_Otop(tc_fun(X1,tc_HOL_Obool))),X0)),
inference(superposition,[],[f4276,f2060]) ).
fof(f30366,plain,
! [X2,X3,X0,X1] : hBOOL(hAPP(c_Set_Oimage(X1,X2,c_COMBI(X3),sF54),X0)),
inference(forward_demodulation,[],[f30316,f6606]) ).
fof(f30797,plain,
! [X2,X0,X1] : ~ c_Finite__Set_Ofinite(tc_Nat_Onat,c_Set_Oimage(X0,X1,c_COMBI(X2),sF54)),
inference(resolution,[],[f30366,f5466]) ).
fof(f30811,plain,
$false,
inference(resolution,[],[f30797,f16307]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : SCT161+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.03 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.04/0.32 % Computer : n012.cluster.edu
% 0.04/0.32 % Model : x86_64 x86_64
% 0.04/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.04/0.32 % Memory : 8046.5625MB
% 0.04/0.32 % OS : Linux 6.8.0-71-generic
% 0.04/0.32 % CPULimit : 300
% 0.04/0.32 % WCLimit : 300
% 0.04/0.32 % DateTime : Sun Sep 27 23:51:20 UTC 2026
% 0.04/0.32 % CPUTime :
% 0.04/0.32 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.07/0.33 Running first-order model finding
% 0.07/0.34 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
% 6.88/1.57 % (2880386)Will run a generic schedule for satisfiability detection.
% 6.88/1.57 % (2880392)% WARNING: option uhcvi not known.
% 6.88/1.57 % (2880392)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3351382296:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 6.88/1.57 % (2880391)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3524244188_2999 on theBenchmark for (2999ds/0Mi)
% 6.88/1.57 % (2880394)dis+10_1_sil=32000:sp=arity:random_seed=3224182466:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 6.88/1.57 % (2880393)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2944209306:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 6.88/1.57 % (2880395)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=582743193:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 6.88/1.57 % (2880396)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1936092375:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 6.88/1.57 % (2880397)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3655133937:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 6.88/1.57 % (2880395)Instruction limit reached!
% 6.88/1.57 % (2880395)------------------------------
% 6.88/1.57 % (2880395)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.88/1.57 % (2880395)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.88/1.57 % (2880395)CaDiCaL version: 2.1.3
% 6.88/1.57 % (2880395)Termination reason: Instruction limit
% 6.88/1.57 % (2880395)Termination phase: Saturation
% 6.88/1.57 % (2880395)Time elapsed: 0.032 s
% 6.88/1.57 % (2880395)Peak memory usage: 13 MB
% 6.88/1.57 % (2880395)Instructions burned: 118 (million)
% 6.88/1.57 % (2880394)Instruction limit reached!
% 6.88/1.57 % (2880394)------------------------------
% 6.88/1.57 % (2880394)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.88/1.57 % (2880394)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.88/1.57 % (2880394)CaDiCaL version: 2.1.3
% 6.88/1.57 % (2880394)Termination reason: Instruction limit
% 6.88/1.57 % (2880394)Termination phase: Saturation
% 6.88/1.57 % (2880394)Time elapsed: 0.032 s
% 6.88/1.57 % (2880394)Peak memory usage: 13 MB
% 6.88/1.57 % (2880394)Instructions burned: 105 (million)
% 6.88/1.57 % (2880396)Instruction limit reached!
% 6.88/1.57 % (2880396)------------------------------
% 6.88/1.57 % (2880396)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.88/1.57 % (2880396)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.88/1.57 % (2880396)CaDiCaL version: 2.1.3
% 6.88/1.57 % (2880396)Termination reason: Instruction limit
% 6.88/1.57 % (2880396)Termination phase: Saturation
% 6.88/1.57 % (2880396)Time elapsed: 0.042 s
% 6.88/1.57 % (2880396)Peak memory usage: 14 MB
% 6.88/1.57 % (2880396)Instructions burned: 131 (million)
% 6.88/1.57 % (2880405)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=152473858:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 6.88/1.57 % (2880406)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=4230475735:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 6.88/1.57 % (2880397)Instruction limit reached!
% 6.88/1.57 % (2880397)------------------------------
% 6.88/1.57 % (2880397)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.88/1.57 % (2880397)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.88/1.57 % (2880397)CaDiCaL version: 2.1.3
% 6.88/1.57 % (2880397)Termination reason: Instruction limit
% 6.88/1.57 % (2880397)Termination phase: Saturation
% 6.88/1.57 % (2880397)Time elapsed: 0.048 s
% 6.88/1.57 % (2880397)Peak memory usage: 14 MB
% 6.88/1.57 % (2880397)Instructions burned: 160 (million)
% 6.88/1.57 % (2880407)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=2626582000:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 6.88/1.57 % (2880410)ott-21_1_sil=16000:fs=off:random_seed=4185010682:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi)
% 6.88/1.57 % (2880406)Instruction limit reached!
% 6.88/1.57 % (2880406)------------------------------
% 6.88/1.57 % (2880406)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.88/1.57 % (2880406)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.88/1.57 % (2880406)CaDiCaL version: 2.1.3
% 16.27/2.85 % (2880406)Termination reason: Instruction limit
% 16.27/2.85 % (2880406)Termination phase: Saturation
% 16.27/2.85 % (2880406)Time elapsed: 0.037 s
% 16.27/2.85 % (2880406)Peak memory usage: 13 MB
% 16.27/2.85 % (2880406)Instructions burned: 133 (million)
% 16.27/2.85 % (2880413)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2046777933:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 16.27/2.85 % (2880410)Instruction limit reached!
% 16.27/2.85 % (2880410)------------------------------
% 16.27/2.85 % (2880410)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.27/2.85 % (2880410)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.27/2.85 % (2880410)CaDiCaL version: 2.1.3
% 16.27/2.85 % (2880410)Termination reason: Instruction limit
% 16.27/2.85 % (2880410)Termination phase: Saturation
% 16.27/2.85 % (2880410)Time elapsed: 0.049 s
% 16.27/2.85 % (2880410)Peak memory usage: 13 MB
% 16.27/2.85 % (2880410)Instructions burned: 182 (million)
% 16.27/2.85 % (2880415)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2736514552:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi)
% 16.27/2.85 % (2880405)Instruction limit reached!
% 16.27/2.85 % (2880405)------------------------------
% 16.27/2.85 % (2880405)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.27/2.85 % (2880405)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.27/2.85 % (2880405)CaDiCaL version: 2.1.3
% 16.27/2.85 % (2880405)Termination reason: Instruction limit
% 16.27/2.85 % (2880405)Termination phase: Finite model building preprocessing
% 16.27/2.85 % (2880405)Time elapsed: 0.187 s
% 16.27/2.85 % (2880405)Peak memory usage: 20 MB
% 16.27/2.85 % (2880405)Instructions burned: 717 (million)
% 16.27/2.85 % (2880417)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2800786052:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 16.27/2.85 % (2880413)Instruction limit reached!
% 16.27/2.85 % (2880413)------------------------------
% 16.27/2.85 % (2880413)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.27/2.85 % (2880413)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.27/2.85 % (2880413)CaDiCaL version: 2.1.3
% 16.27/2.85 % (2880413)Termination reason: Instruction limit
% 16.27/2.85 % (2880413)Termination phase: Saturation
% 16.27/2.85 % (2880413)Time elapsed: 0.161 s
% 16.27/2.85 % (2880413)Peak memory usage: 15 MB
% 16.27/2.85 % (2880413)Instructions burned: 477 (million)
% 16.27/2.85 % (2880419)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1350262818:i=889:ins=1_2996 on theBenchmark for (2996ds/889Mi)
% 16.27/2.85 % (2880407)Instruction limit reached!
% 16.27/2.85 % (2880407)------------------------------
% 16.27/2.85 % (2880407)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.27/2.85 % (2880407)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.27/2.85 % (2880407)CaDiCaL version: 2.1.3
% 16.27/2.85 % (2880407)Termination reason: Instruction limit
% 16.27/2.85 % (2880407)Termination phase: Saturation
% 16.27/2.85 % (2880407)Time elapsed: 0.220 s
% 16.27/2.85 % (2880407)Peak memory usage: 20 MB
% 16.27/2.85 % (2880407)Instructions burned: 686 (million)
% 16.27/2.85 % (2880421)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=3130462993:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2996 on theBenchmark for (2996ds/692Mi)
% 16.27/2.85 % TRYING [1]
% 16.27/2.85 % TRYING [2]
% 16.27/2.85 % (2880415)Instruction limit reached!
% 16.27/2.85 % (2880415)------------------------------
% 16.27/2.85 % (2880415)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.27/2.85 % (2880415)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.27/2.85 % (2880415)CaDiCaL version: 2.1.3
% 16.27/2.85 % (2880415)Termination reason: Instruction limit
% 16.27/2.85 % (2880415)Termination phase: Finite model building preprocessing
% 16.27/2.85 % (2880415)Time elapsed: 0.226 s
% 16.27/2.85 % (2880415)Peak memory usage: 19 MB
% 16.27/2.85 % (2880415)Instructions burned: 865 (million)
% 16.27/2.85 % (2880423)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3897513295:i=879:kws=inv_precedence:fsr=off_2996 on theBenchmark for (2996ds/879Mi)
% 16.27/2.85 % TRYING [3]
% 16.27/2.85 % (2880419)Instruction limit reached!
% 16.27/2.85 % (2880419)------------------------------
% 16.27/2.85 % (2880419)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.27/2.85 % (2880419)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.27/2.85 % (2880419)CaDiCaL version: 2.1.3
% 16.27/2.85 % (2880419)Termination reason: Instruction limit
% 16.27/2.85 % (2880419)Termination phase: Finite model building preprocessing
% 16.27/2.85 % (2880419)Time elapsed: 0.234 s
% 16.27/2.85 % (2880419)Peak memory usage: 20 MB
% 16.27/2.85 % (2880419)Instructions burned: 892 (million)
% 16.27/2.85 % (2880421)Instruction limit reached!
% 16.27/2.85 % (2880421)------------------------------
% 16.27/2.85 % (2880421)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.27/2.85 % (2880421)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.27/2.85 % (2880421)CaDiCaL version: 2.1.3
% 16.27/2.85 % (2880421)Termination reason: Instruction limit
% 16.27/2.85 % (2880421)Termination phase: Saturation
% 16.27/2.85 % (2880421)Time elapsed: 0.222 s
% 16.27/2.85 % (2880421)Peak memory usage: 25 MB
% 16.27/2.85 % (2880421)Instructions burned: 693 (million)
% 16.27/2.85 % (2880425)fmb+10_1_sil=64000:random_seed=1285849401:i=22061:nm=2:gsp=on_2994 on theBenchmark for (2994ds/22061Mi)
% 16.27/2.85 % (2880426)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1238463694:i=9515:nm=5_2994 on theBenchmark for (2994ds/9515Mi)
% 16.27/2.85 % (2880423)Instruction limit reached!
% 16.27/2.85 % (2880423)------------------------------
% 16.27/2.85 % (2880423)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.27/2.85 % (2880423)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.27/2.85 % (2880423)CaDiCaL version: 2.1.3
% 16.27/2.85 % (2880423)Termination reason: Instruction limit
% 16.27/2.85 % (2880423)Termination phase: Saturation
% 16.27/2.85 % (2880423)Time elapsed: 0.258 s
% 16.27/2.85 % (2880423)Peak memory usage: 20 MB
% 16.27/2.85 % (2880423)Instructions burned: 882 (million)
% 16.27/2.85 % (2880417)Instruction limit reached!
% 16.27/2.85 % (2880417)------------------------------
% 16.27/2.85 % (2880417)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.27/2.85 % (2880417)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.27/2.85 % (2880417)CaDiCaL version: 2.1.3
% 16.27/2.85 % (2880417)Termination reason: Instruction limit
% 16.27/2.85 % (2880417)Termination phase: Saturation
% 16.27/2.85 % (2880417)Time elapsed: 0.379 s
% 16.27/2.85 % (2880417)Peak memory usage: 23 MB
% 16.27/2.85 % (2880417)Instructions burned: 1179 (million)
% 16.27/2.85 % (2880429)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2913406173:fmbsr=1.7:i=920_2993 on theBenchmark for (2993ds/920Mi)
% 16.27/2.85 % (2880430)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3554574562:i=5131_2993 on theBenchmark for (2993ds/5131Mi)
% 16.27/2.85 % TRYING [1]
% 16.27/2.85 % TRYING [2]
% 16.27/2.85 % (2880426)Cannot represent all propositional literals internally
% 16.27/2.85 % (2880426)Refutation not found, incomplete strategy
% 16.27/2.85 % (2880426)------------------------------
% 16.27/2.85 % (2880426)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.27/2.85 % (2880426)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.27/2.85 % (2880426)CaDiCaL version: 2.1.3
% 16.27/2.85 % (2880426)Termination reason: Refutation not found, incomplete strategy
% 16.27/2.85 % (2880426)Time elapsed: 0.283 s
% 16.27/2.85 % (2880426)Peak memory usage: 24 MB
% 16.27/2.85 % (2880426)Instructions burned: 1091 (million)
% 16.27/2.85 % (2880426)------------------------------
% 16.27/2.85 % (2880426)------------------------------
% 16.27/2.85 % (2880433)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2755175016:i=1472:ins=7:fdi=8:gsp=on_2991 on theBenchmark for (2991ds/1472Mi)
% 16.27/2.85 % (2880429)Instruction limit reached!
% 16.27/2.85 % (2880429)------------------------------
% 16.27/2.85 % (2880429)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.27/2.85 % (2880429)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.27/2.85 % (2880429)CaDiCaL version: 2.1.3
% 16.27/2.85 % (2880429)Termination reason: Instruction limit
% 16.27/2.85 % (2880429)Termination phase: Finite model building preprocessing
% 16.27/2.85 % (2880429)Time elapsed: 0.245 s
% 16.27/2.85 % (2880429)Peak memory usage: 21 MB
% 16.27/2.85 % (2880429)Instructions burned: 924 (million)
% 16.27/2.85 % (2880435)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=2454748095:i=6324_2990 on theBenchmark for (2990ds/6324Mi)
% 16.27/2.85 % TRYING [4]
% 16.27/2.85 % TRYING [3]
% 16.27/2.85 % (2880435)Cannot represent all propositional literals internally
% 16.27/2.85 % (2880435)Refutation not found, incomplete strategy
% 16.27/2.85 % (2880435)------------------------------
% 16.27/2.85 % (2880435)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.27/2.85 % (2880435)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.27/2.85 % (2880435)CaDiCaL version: 2.1.3
% 16.27/2.85 % (2880435)Termination reason: Refutation not found, incomplete strategy
% 16.27/2.85 % (2880435)Time elapsed: 0.295 s
% 16.27/2.85 % (2880435)Peak memory usage: 24 MB
% 16.27/2.85 % (2880435)Instructions burned: 1129 (million)
% 16.27/2.85 % (2880435)------------------------------
% 16.27/2.85 % (2880435)------------------------------
% 16.27/2.85 % (2880437)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3105287955:fmbsr=2.30978:i=2174_2987 on theBenchmark for (2987ds/2174Mi)
% 16.27/2.85 % (2880433)Instruction limit reached!
% 16.27/2.85 % (2880433)------------------------------
% 16.27/2.85 % (2880433)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.27/2.85 % (2880433)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.27/2.85 % (2880433)CaDiCaL version: 2.1.3
% 16.27/2.85 % (2880433)Termination reason: Instruction limit
% 16.27/2.85 % (2880433)Termination phase: Saturation
% 16.27/2.85 % (2880433)Time elapsed: 0.432 s
% 16.27/2.85 % (2880433)Peak memory usage: 32 MB
% 16.27/2.85 % (2880433)Instructions burned: 1474 (million)
% 16.27/2.85 % (2880439)ott-2_1_sil=16000:newcnf=on:random_seed=4267105063:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2986 on theBenchmark for (2986ds/869Mi)
% 16.27/2.85 % (2880439)Instruction limit reached!
% 16.27/2.85 % (2880439)------------------------------
% 16.27/2.85 % (2880439)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.27/2.85 % (2880439)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.27/2.85 % (2880439)CaDiCaL version: 2.1.3
% 16.27/2.85 % (2880439)Termination reason: Instruction limit
% 16.27/2.85 % (2880439)Termination phase: Saturation
% 16.27/2.85 % (2880439)Time elapsed: 0.255 s
% 16.27/2.85 % (2880439)Peak memory usage: 18 MB
% 16.27/2.85 % (2880439)Instructions burned: 870 (million)
% 16.27/2.85 % (2880441)ott+10_1_sil=32000:tgt=ground:random_seed=375653636:i=5114:av=off_2984 on theBenchmark for (2984ds/5114Mi)
% 16.27/2.85 % (2880437)Instruction limit reached!
% 16.27/2.85 % (2880437)------------------------------
% 16.27/2.85 % (2880437)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.27/2.85 % (2880437)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.27/2.85 % (2880437)CaDiCaL version: 2.1.3
% 16.27/2.85 % (2880437)Termination reason: Instruction limit
% 16.27/2.85 % (2880437)Termination phase: Finite model building preprocessing
% 16.27/2.85 % (2880437)Time elapsed: 0.577 s
% 16.27/2.85 % (2880437)Peak memory usage: 27 MB
% 16.27/2.85 % (2880437)Instructions burned: 2176 (million)
% 16.27/2.85 % (2880443)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=210238634:i=54282_2981 on theBenchmark for (2981ds/54282Mi)
% 16.27/2.85 % TRYING [1]
% 16.27/2.85 % TRYING [2]
% 16.27/2.85 % TRYING [3]
% 16.27/2.85 % (2880430)Instruction limit reached!
% 16.27/2.85 % (2880430)------------------------------
% 16.27/2.85 % (2880430)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.27/2.85 % (2880430)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.27/2.85 % (2880430)CaDiCaL version: 2.1.3
% 16.27/2.85 % (2880430)Termination reason: Instruction limit
% 16.27/2.85 % (2880430)Termination phase: Saturation
% 16.27/2.85 % (2880430)Time elapsed: 1.588 s
% 16.27/2.85 % (2880430)Peak memory usage: 43 MB
% 16.27/2.85 % (2880430)Instructions burned: 5132 (million)
% 16.27/2.85 % (2880445)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=7545798:i=3512:aac=none_2977 on theBenchmark for (2977ds/3512Mi)
% 16.27/2.85 % (2880441) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-2880386-2880441"...
% 16.27/2.85 % (2880441)...printing done.
% 16.27/2.85 % (2880441)Refutation found. Thanks to Tanya!
% 16.27/2.85 % SZS status ContradictoryAxioms for theBenchmark
% 16.27/2.85 % SZS output start Proof for theBenchmark
% See solution above
% 16.27/2.86 % (2880441)------------------------------
% 16.27/2.86 % (2880441)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.27/2.86 % (2880441)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.27/2.86 % (2880441)CaDiCaL version: 2.1.3
% 16.27/2.86 % (2880441)Termination reason: Refutation
% 16.27/2.86 % (2880441)Time elapsed: 0.876 s
% 16.27/2.86 % (2880441)Peak memory usage: 28 MB
% 16.27/2.86 % (2880441)Instructions burned: 2644 (million)
% 16.27/2.86 % (2880386)Success in time 2.513 s
% 16.27/2.86 % Vampire exiting
%------------------------------------------------------------------------------