%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : NUM577+3 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p 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 : Fri Sep 25 02:26:05 PM UTC 2026
% Result : Theorem 22.64s 4.02s
% Output : CNFRefutation 22.64s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named f229ERROR: Could not build tree for root c_17826ERROR: MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
fof(f10,axiom,
! [X0] :
( aSet0(X0)
=> ! [X1] :
( aSubsetOf0(X1,X0)
<=> ( ! [X2] :
( aElementOf0(X2,X1)
=> aElementOf0(X2,X0) )
& aSet0(X1) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mDefSub) ).
fof(f25,axiom,
! [X0] :
( aElementOf0(X0,szNzAzT0)
=> ( szszuzczcdt0(X0) != sz00
& aElementOf0(szszuzczcdt0(X0),szNzAzT0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mSuccNum) ).
fof(f81,axiom,
( ! [X0] :
( aElementOf0(X0,szNzAzT0)
=> ( ( isCountable0(sdtlpdtrp0(xN,X0))
& ( aSubsetOf0(sdtlpdtrp0(xN,X0),szNzAzT0)
| ( ! [X1] :
( aElementOf0(X1,sdtlpdtrp0(xN,X0))
=> aElementOf0(X1,szNzAzT0) )
& aSet0(sdtlpdtrp0(xN,X0)) ) ) )
=> ( isCountable0(sdtlpdtrp0(xN,szszuzczcdt0(X0)))
& aSubsetOf0(sdtlpdtrp0(xN,szszuzczcdt0(X0)),sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
& ! [X1] :
( aElementOf0(X1,sdtlpdtrp0(xN,szszuzczcdt0(X0)))
=> aElementOf0(X1,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0)))) )
& aSet0(sdtlpdtrp0(xN,szszuzczcdt0(X0)))
& ! [X1] :
( aElementOf0(X1,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
<=> ( X1 != szmzizndt0(sdtlpdtrp0(xN,X0))
& aElementOf0(X1,sdtlpdtrp0(xN,X0))
& aElement0(X1) ) )
& aSet0(sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
& ! [X1] :
( aElementOf0(X1,sdtlpdtrp0(xN,X0))
=> sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X0)),X1) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X0)),sdtlpdtrp0(xN,X0)) ) ) )
& sdtlpdtrp0(xN,sz00) = xS
& szDzozmdt0(xN) = szNzAzT0
& aFunction0(xN) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__3623) ).
fof(f82,axiom,
! [X0] :
( aElementOf0(X0,szNzAzT0)
=> ( isCountable0(sdtlpdtrp0(xN,X0))
& aSubsetOf0(sdtlpdtrp0(xN,X0),szNzAzT0)
& ! [X1] :
( aElementOf0(X1,sdtlpdtrp0(xN,X0))
=> aElementOf0(X1,szNzAzT0) )
& aSet0(sdtlpdtrp0(xN,X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__3671) ).
fof(f83,axiom,
! [X0,X1] :
( ( aElementOf0(X1,szNzAzT0)
& aElementOf0(X0,szNzAzT0) )
=> ( sdtlseqdt0(X1,X0)
=> ( aSubsetOf0(sdtlpdtrp0(xN,X0),sdtlpdtrp0(xN,X1))
& ! [X2] :
( aElementOf0(X2,sdtlpdtrp0(xN,X0))
=> aElementOf0(X2,sdtlpdtrp0(xN,X1)) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__3754) ).
fof(f86,axiom,
( aElementOf0(xm,szNzAzT0)
& aElementOf0(xn,szNzAzT0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__3904) ).
fof(f98,plain,
( ! [X0] :
( aElementOf0(X0,szNzAzT0)
=> ( ( isCountable0(sdtlpdtrp0(xN,X0))
& ( aSubsetOf0(sdtlpdtrp0(xN,X0),szNzAzT0)
| ( ! [X1] :
( aElementOf0(X1,sdtlpdtrp0(xN,X0))
=> aElementOf0(X1,szNzAzT0) )
& aSet0(sdtlpdtrp0(xN,X0)) ) ) )
=> ( isCountable0(sdtlpdtrp0(xN,szszuzczcdt0(X0)))
& aSubsetOf0(sdtlpdtrp0(xN,szszuzczcdt0(X0)),sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
& ! [X4] :
( aElementOf0(X4,sdtlpdtrp0(xN,szszuzczcdt0(X0)))
=> aElementOf0(X4,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0)))) )
& aSet0(sdtlpdtrp0(xN,szszuzczcdt0(X0)))
& ! [X3] :
( aElementOf0(X3,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
<=> ( szmzizndt0(sdtlpdtrp0(xN,X0)) != X3
& aElementOf0(X3,sdtlpdtrp0(xN,X0))
& aElement0(X3) ) )
& aSet0(sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
& ! [X2] :
( aElementOf0(X2,sdtlpdtrp0(xN,X0))
=> sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X0)),X2) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X0)),sdtlpdtrp0(xN,X0)) ) ) )
& sdtlpdtrp0(xN,sz00) = xS
& szDzozmdt0(xN) = szNzAzT0
& aFunction0(xN) ),
inference(rectify,[],[f81]) ).
fof(f106,plain,
! [X0] :
( ~ aSet0(X0)
| ! [X1] :
( aSubsetOf0(X1,X0)
<=> ( ! [X2] :
( ~ aElementOf0(X2,X1)
| aElementOf0(X2,X0) )
& aSet0(X1) ) ) ),
inference(ennf_transformation,[],[f10]) ).
fof(f129,plain,
! [X0] :
( ~ aElementOf0(X0,szNzAzT0)
| ( szszuzczcdt0(X0) != sz00
& aElementOf0(szszuzczcdt0(X0),szNzAzT0) ) ),
inference(ennf_transformation,[],[f25]) ).
fof(f204,plain,
( ! [X0] :
( ~ aElementOf0(X0,szNzAzT0)
| ~ isCountable0(sdtlpdtrp0(xN,X0))
| ( ~ aSubsetOf0(sdtlpdtrp0(xN,X0),szNzAzT0)
& ( ? [X1] :
( aElementOf0(X1,sdtlpdtrp0(xN,X0))
& ~ aElementOf0(X1,szNzAzT0) )
| ~ aSet0(sdtlpdtrp0(xN,X0)) ) )
| ( isCountable0(sdtlpdtrp0(xN,szszuzczcdt0(X0)))
& aSubsetOf0(sdtlpdtrp0(xN,szszuzczcdt0(X0)),sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
& ! [X4] :
( ~ aElementOf0(X4,sdtlpdtrp0(xN,szszuzczcdt0(X0)))
| aElementOf0(X4,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0)))) )
& aSet0(sdtlpdtrp0(xN,szszuzczcdt0(X0)))
& ! [X3] :
( aElementOf0(X3,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
<=> ( szmzizndt0(sdtlpdtrp0(xN,X0)) != X3
& aElementOf0(X3,sdtlpdtrp0(xN,X0))
& aElement0(X3) ) )
& aSet0(sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
& ! [X2] :
( ~ aElementOf0(X2,sdtlpdtrp0(xN,X0))
| sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X0)),X2) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X0)),sdtlpdtrp0(xN,X0)) ) )
& sdtlpdtrp0(xN,sz00) = xS
& szDzozmdt0(xN) = szNzAzT0
& aFunction0(xN) ),
inference(ennf_transformation,[],[f98]) ).
fof(f205,plain,
( ! [X0] :
( ~ aElementOf0(X0,szNzAzT0)
| ~ isCountable0(sdtlpdtrp0(xN,X0))
| ( ~ aSubsetOf0(sdtlpdtrp0(xN,X0),szNzAzT0)
& ( ? [X1] :
( aElementOf0(X1,sdtlpdtrp0(xN,X0))
& ~ aElementOf0(X1,szNzAzT0) )
| ~ aSet0(sdtlpdtrp0(xN,X0)) ) )
| ( isCountable0(sdtlpdtrp0(xN,szszuzczcdt0(X0)))
& aSubsetOf0(sdtlpdtrp0(xN,szszuzczcdt0(X0)),sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
& ! [X4] :
( ~ aElementOf0(X4,sdtlpdtrp0(xN,szszuzczcdt0(X0)))
| aElementOf0(X4,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0)))) )
& aSet0(sdtlpdtrp0(xN,szszuzczcdt0(X0)))
& ! [X3] :
( aElementOf0(X3,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
<=> ( szmzizndt0(sdtlpdtrp0(xN,X0)) != X3
& aElementOf0(X3,sdtlpdtrp0(xN,X0))
& aElement0(X3) ) )
& aSet0(sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
& ! [X2] :
( ~ aElementOf0(X2,sdtlpdtrp0(xN,X0))
| sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X0)),X2) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X0)),sdtlpdtrp0(xN,X0)) ) )
& sdtlpdtrp0(xN,sz00) = xS
& szDzozmdt0(xN) = szNzAzT0
& aFunction0(xN) ),
inference(flattening,[],[f204]) ).
fof(f206,plain,
! [X0] :
( ~ aElementOf0(X0,szNzAzT0)
| ( isCountable0(sdtlpdtrp0(xN,X0))
& aSubsetOf0(sdtlpdtrp0(xN,X0),szNzAzT0)
& ! [X1] :
( ~ aElementOf0(X1,sdtlpdtrp0(xN,X0))
| aElementOf0(X1,szNzAzT0) )
& aSet0(sdtlpdtrp0(xN,X0)) ) ),
inference(ennf_transformation,[],[f82]) ).
fof(f207,plain,
! [X0,X1] :
( ~ aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(X0,szNzAzT0)
| ~ sdtlseqdt0(X1,X0)
| ( aSubsetOf0(sdtlpdtrp0(xN,X0),sdtlpdtrp0(xN,X1))
& ! [X2] :
( ~ aElementOf0(X2,sdtlpdtrp0(xN,X0))
| aElementOf0(X2,sdtlpdtrp0(xN,X1)) ) ) ),
inference(ennf_transformation,[],[f83]) ).
fof(f208,plain,
! [X0,X1] :
( ~ aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(X0,szNzAzT0)
| ~ sdtlseqdt0(X1,X0)
| ( aSubsetOf0(sdtlpdtrp0(xN,X0),sdtlpdtrp0(xN,X1))
& ! [X2] :
( ~ aElementOf0(X2,sdtlpdtrp0(xN,X0))
| aElementOf0(X2,sdtlpdtrp0(xN,X1)) ) ) ),
inference(flattening,[],[f207]) ).
fof(f234,plain,
! [X0] :
( ~ aSet0(X0)
| ! [X1] :
( ( ~ aSubsetOf0(X1,X0)
| ( ! [X2] :
( ~ aElementOf0(X2,X1)
| aElementOf0(X2,X0) )
& aSet0(X1) ) )
& ( ? [X2] :
( aElementOf0(X2,X1)
& ~ aElementOf0(X2,X0) )
| ~ aSet0(X1)
| aSubsetOf0(X1,X0) ) ) ),
inference(nnf_transformation,[],[f106]) ).
fof(f235,plain,
! [X0] :
( ~ aSet0(X0)
| ! [X1] :
( ( ~ aSubsetOf0(X1,X0)
| ( ! [X2] :
( ~ aElementOf0(X2,X1)
| aElementOf0(X2,X0) )
& aSet0(X1) ) )
& ( ? [X2] :
( aElementOf0(X2,X1)
& ~ aElementOf0(X2,X0) )
| ~ aSet0(X1)
| aSubsetOf0(X1,X0) ) ) ),
inference(flattening,[],[f234]) ).
fof(f236,plain,
! [X0] :
( ~ aSet0(X0)
| ! [X1] :
( ( ~ aSubsetOf0(X1,X0)
| ( ! [X3] :
( ~ aElementOf0(X3,X1)
| aElementOf0(X3,X0) )
& aSet0(X1) ) )
& ( ? [X2] :
( aElementOf0(X2,X1)
& ~ aElementOf0(X2,X0) )
| ~ aSet0(X1)
| aSubsetOf0(X1,X0) ) ) ),
inference(rectify,[],[f235]) ).
fof(f237,plain,
! [X0] :
( ~ aSet0(X0)
| ! [X1] :
( ( ~ aSubsetOf0(X1,X0)
| ( ! [X3] :
( ~ aElementOf0(X3,X1)
| aElementOf0(X3,X0) )
& aSet0(X1) ) )
& ( ( aElementOf0(sK13(X0,X1),X1)
& ~ aElementOf0(sK13(X0,X1),X0) )
| ~ aSet0(X1)
| aSubsetOf0(X1,X0) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK13]),skolemize(X2,sK13(X0,X1))],[f236]) ).
fof(f305,plain,
! [X0] :
( ~ sP9(X0)
| ( isCountable0(sdtlpdtrp0(xN,szszuzczcdt0(X0)))
& aSubsetOf0(sdtlpdtrp0(xN,szszuzczcdt0(X0)),sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
& ! [X4] :
( ~ aElementOf0(X4,sdtlpdtrp0(xN,szszuzczcdt0(X0)))
| aElementOf0(X4,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0)))) )
& aSet0(sdtlpdtrp0(xN,szszuzczcdt0(X0)))
& sP8(X0)
& aSet0(sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
& ! [X2] :
( ~ aElementOf0(X2,sdtlpdtrp0(xN,X0))
| sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X0)),X2) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X0)),sdtlpdtrp0(xN,X0)) ) ),
inference(nnf_transformation,[],[f225]) ).
fof(f306,plain,
! [X0] :
( ~ sP9(X0)
| ( isCountable0(sdtlpdtrp0(xN,szszuzczcdt0(X0)))
& aSubsetOf0(sdtlpdtrp0(xN,szszuzczcdt0(X0)),sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
& ! [X2] :
( ~ aElementOf0(X2,sdtlpdtrp0(xN,szszuzczcdt0(X0)))
| aElementOf0(X2,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0)))) )
& aSet0(sdtlpdtrp0(xN,szszuzczcdt0(X0)))
& sP8(X0)
& aSet0(sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
& ! [X1] :
( ~ aElementOf0(X1,sdtlpdtrp0(xN,X0))
| sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X0)),X1) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X0)),sdtlpdtrp0(xN,X0)) ) ),
inference(rectify,[],[f305]) ).
fof(f310,plain,
( ! [X0] :
( ~ aElementOf0(X0,szNzAzT0)
| ~ isCountable0(sdtlpdtrp0(xN,X0))
| ( ~ aSubsetOf0(sdtlpdtrp0(xN,X0),szNzAzT0)
& ( ( aElementOf0(sK41(X0),sdtlpdtrp0(xN,X0))
& ~ aElementOf0(sK41(X0),szNzAzT0) )
| ~ aSet0(sdtlpdtrp0(xN,X0)) ) )
| sP9(X0) )
& sdtlpdtrp0(xN,sz00) = xS
& szDzozmdt0(xN) = szNzAzT0
& aFunction0(xN) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK41]),skolemize(X1,sK41(X0))],[f226]) ).
fof(f311,plain,
( ~ sP11
| ( ! [X0] :
( ~ aElementOf0(X0,sdtlpdtrp0(xN,xn))
| sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xn)),X0) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xn)),sdtlpdtrp0(xN,xn))
& sP10
& aSet0(sdtmndt0(sdtlpdtrp0(xN,xn),szmzizndt0(sdtlpdtrp0(xN,xn))))
& ~ aSubsetOf0(sdtlpdtrp0(xN,xm),sdtmndt0(sdtlpdtrp0(xN,xn),szmzizndt0(sdtlpdtrp0(xN,xn))))
& ? [X2] :
( aElementOf0(X2,sdtlpdtrp0(xN,xm))
& ~ aElementOf0(X2,sdtmndt0(sdtlpdtrp0(xN,xn),szmzizndt0(sdtlpdtrp0(xN,xn)))) ) ) ),
inference(nnf_transformation,[],[f228]) ).
fof(f312,plain,
( ~ sP11
| ( ! [X1] :
( ~ aElementOf0(X1,sdtlpdtrp0(xN,xn))
| sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xn)),X1) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xn)),sdtlpdtrp0(xN,xn))
& sP10
& aSet0(sdtmndt0(sdtlpdtrp0(xN,xn),szmzizndt0(sdtlpdtrp0(xN,xn))))
& ~ aSubsetOf0(sdtlpdtrp0(xN,xm),sdtmndt0(sdtlpdtrp0(xN,xn),szmzizndt0(sdtlpdtrp0(xN,xn))))
& ? [X0] :
( aElementOf0(X0,sdtlpdtrp0(xN,xm))
& ~ aElementOf0(X0,sdtmndt0(sdtlpdtrp0(xN,xn),szmzizndt0(sdtlpdtrp0(xN,xn)))) ) ) ),
inference(rectify,[],[f311]) ).
fof(f313,plain,
( ~ sP11
| ( ! [X1] :
( ~ aElementOf0(X1,sdtlpdtrp0(xN,xn))
| sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xn)),X1) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xn)),sdtlpdtrp0(xN,xn))
& sP10
& aSet0(sdtmndt0(sdtlpdtrp0(xN,xn),szmzizndt0(sdtlpdtrp0(xN,xn))))
& ~ aSubsetOf0(sdtlpdtrp0(xN,xm),sdtmndt0(sdtlpdtrp0(xN,xn),szmzizndt0(sdtlpdtrp0(xN,xn))))
& aElementOf0(sK42,sdtlpdtrp0(xN,xm))
& ~ aElementOf0(sK42,sdtmndt0(sdtlpdtrp0(xN,xn),szmzizndt0(sdtlpdtrp0(xN,xn)))) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK42]),skolemize(X0,sK42)],[f312]) ).
fof(f317,plain,
( sdtlseqdt0(szszuzczcdt0(xn),xm)
& ( ( szmzizndt0(sdtlpdtrp0(xN,xm)) = szmzizndt0(sdtlpdtrp0(xN,xn))
& ! [X1] :
( ~ aElementOf0(X1,sdtlpdtrp0(xN,xn))
| sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xm)),X1) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xm)),sdtlpdtrp0(xN,xn))
& ! [X0] :
( ~ aElementOf0(X0,sdtlpdtrp0(xN,xm))
| sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xm)),X0) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xm)),sdtlpdtrp0(xN,xm)) )
| sP11 ) ),
inference(rectify,[],[f229]) ).
fof(f325,plain,
! [X3,X0,X1] :
( ~ aSet0(X0)
| ~ aSubsetOf0(X1,X0)
| ~ aElementOf0(X3,X1)
| aElementOf0(X3,X0) ),
inference(cnf_transformation,[],[f237]) ).
fof(f367,plain,
! [X0] :
( ~ aElementOf0(X0,szNzAzT0)
| aElementOf0(szszuzczcdt0(X0),szNzAzT0) ),
inference(cnf_transformation,[],[f129]) ).
fof(f520,plain,
! [X2,X0] :
( ~ sP9(X0)
| ~ aElementOf0(X2,sdtlpdtrp0(xN,szszuzczcdt0(X0)))
| aElementOf0(X2,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0)))) ),
inference(cnf_transformation,[],[f306]) ).
fof(f522,plain,
! [X0] :
( ~ sP9(X0)
| sP8(X0) ),
inference(cnf_transformation,[],[f306]) ).
fof(f525,plain,
! [X0] :
( ~ sP9(X0)
| aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X0)),sdtlpdtrp0(xN,X0)) ),
inference(cnf_transformation,[],[f306]) ).
fof(f530,plain,
! [X0] :
( ~ aElementOf0(X0,szNzAzT0)
| ~ isCountable0(sdtlpdtrp0(xN,X0))
| ~ aSubsetOf0(sdtlpdtrp0(xN,X0),szNzAzT0)
| sP9(X0) ),
inference(cnf_transformation,[],[f310]) ).
fof(f531,plain,
! [X0] :
( ~ aElementOf0(X0,szNzAzT0)
| ~ isCountable0(sdtlpdtrp0(xN,X0))
| aElementOf0(sK41(X0),sdtlpdtrp0(xN,X0))
| ~ aSet0(sdtlpdtrp0(xN,X0))
| sP9(X0) ),
inference(cnf_transformation,[],[f310]) ).
fof(f536,plain,
! [X0] :
( ~ aElementOf0(X0,szNzAzT0)
| isCountable0(sdtlpdtrp0(xN,X0)) ),
inference(cnf_transformation,[],[f206]) ).
fof(f537,plain,
! [X0] :
( ~ aElementOf0(X0,szNzAzT0)
| aSubsetOf0(sdtlpdtrp0(xN,X0),szNzAzT0) ),
inference(cnf_transformation,[],[f206]) ).
fof(f539,plain,
! [X0] :
( ~ aElementOf0(X0,szNzAzT0)
| aSet0(sdtlpdtrp0(xN,X0)) ),
inference(cnf_transformation,[],[f206]) ).
fof(f540,plain,
! [X0,X1] :
( ~ aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(X0,szNzAzT0)
| ~ sdtlseqdt0(X1,X0)
| aSubsetOf0(sdtlpdtrp0(xN,X0),sdtlpdtrp0(xN,X1)) ),
inference(cnf_transformation,[],[f208]) ).
fof(f541,plain,
! [X2,X0,X1] :
( ~ aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(X0,szNzAzT0)
| ~ sdtlseqdt0(X1,X0)
| ~ aElementOf0(X2,sdtlpdtrp0(xN,X0))
| aElementOf0(X2,sdtlpdtrp0(xN,X1)) ),
inference(cnf_transformation,[],[f208]) ).
fof(f545,plain,
aElementOf0(xm,szNzAzT0),
inference(cnf_transformation,[],[f86]) ).
fof(f546,plain,
aElementOf0(xn,szNzAzT0),
inference(cnf_transformation,[],[f86]) ).
fof(f552,plain,
( ~ sP11
| aElementOf0(sK42,sdtlpdtrp0(xN,xm)) ),
inference(cnf_transformation,[],[f313]) ).
fof(f553,plain,
( ~ sP11
| ~ aElementOf0(sK42,sdtmndt0(sdtlpdtrp0(xN,xn),szmzizndt0(sdtlpdtrp0(xN,xn)))) ),
inference(cnf_transformation,[],[f313]) ).
fof(f558,plain,
sdtlseqdt0(szszuzczcdt0(xn),xm),
inference(cnf_transformation,[],[f317]) ).
fof(f559,plain,
( szmzizndt0(sdtlpdtrp0(xN,xn)) = szmzizndt0(sdtlpdtrp0(xN,xm))
| sP11 ),
inference(cnf_transformation,[],[f317]) ).
fof(f563,plain,
( aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xm)),sdtlpdtrp0(xN,xm))
| sP11 ),
inference(cnf_transformation,[],[f317]) ).
tcf(c_59,plain,
! [X0: $i,X1: $i,X2: $i] :
( aElementOf0(X0,X2)
| ~ aSet0(X2)
| ~ aSubsetOf0(X1,X2)
| ~ aElementOf0(X0,X1) ),
inference(cnf_transformation,[],[f325]) ).
tcf(c_97,plain,
! [X0: $i] :
( aElementOf0(szszuzczcdt0(X0),szNzAzT0)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[],[f367]) ).
tcf(c_249,plain,
! [X0: $i] :
( aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X0)),sdtlpdtrp0(xN,X0))
| ~ sP9(X0) ),
inference(cnf_transformation,[],[f525]) ).
tcf(c_252,plain,
! [X0: $i] :
( sP8(X0)
| ~ sP9(X0) ),
inference(cnf_transformation,[],[f522]) ).
tcf(c_254,plain,
! [X0: $i,X1: $i] :
( aElementOf0(X0,sdtmndt0(sdtlpdtrp0(xN,X1),szmzizndt0(sdtlpdtrp0(xN,X1))))
| ~ sP9(X1)
| ~ aElementOf0(X0,sdtlpdtrp0(xN,szszuzczcdt0(X1))) ),
inference(cnf_transformation,[],[f520]) ).
tcf(c_265,plain,
! [X0: $i] :
( sP9(X0)
| aElementOf0(sK41(X0),sdtlpdtrp0(xN,X0))
| ~ aElementOf0(X0,szNzAzT0)
| ~ isCountable0(sdtlpdtrp0(xN,X0))
| ~ aSet0(sdtlpdtrp0(xN,X0)) ),
inference(cnf_transformation,[],[f531]) ).
tcf(c_266,plain,
! [X0: $i] :
( sP9(X0)
| ~ aElementOf0(X0,szNzAzT0)
| ~ isCountable0(sdtlpdtrp0(xN,X0))
| ~ aSubsetOf0(sdtlpdtrp0(xN,X0),szNzAzT0) ),
inference(cnf_transformation,[],[f530]) ).
tcf(c_267,plain,
! [X0: $i] :
( aSet0(sdtlpdtrp0(xN,X0))
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[],[f539]) ).
tcf(c_269,plain,
! [X0: $i] :
( aSubsetOf0(sdtlpdtrp0(xN,X0),szNzAzT0)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[],[f537]) ).
tcf(c_270,plain,
! [X0: $i] :
( isCountable0(sdtlpdtrp0(xN,X0))
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[],[f536]) ).
tcf(c_271,plain,
! [X0: $i,X1: $i,X2: $i] :
( aElementOf0(X0,sdtlpdtrp0(xN,X2))
| ~ aElementOf0(X2,szNzAzT0)
| ~ aElementOf0(X1,szNzAzT0)
| ~ sdtlseqdt0(X2,X1)
| ~ aElementOf0(X0,sdtlpdtrp0(xN,X1)) ),
inference(cnf_transformation,[],[f541]) ).
tcf(c_272,plain,
! [X0: $i,X1: $i] :
( aSubsetOf0(sdtlpdtrp0(xN,X1),sdtlpdtrp0(xN,X0))
| ~ aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(X0,szNzAzT0)
| ~ sdtlseqdt0(X0,X1) ),
inference(cnf_transformation,[],[f540]) ).
tcf(c_276,plain,
aElementOf0(xn,szNzAzT0),
inference(cnf_transformation,[],[f546]) ).
tcf(c_277,plain,
aElementOf0(xm,szNzAzT0),
inference(cnf_transformation,[],[f545]) ).
tcf(c_278,negated_conjecture,
( ~ sP11
| ~ aElementOf0(sK42,sdtmndt0(sdtlpdtrp0(xN,xn),szmzizndt0(sdtlpdtrp0(xN,xn)))) ),
inference(cnf_transformation,[],[f553]) ).
tcf(c_279,plain,
( aElementOf0(sK42,sdtlpdtrp0(xN,xm))
| ~ sP11 ),
inference(cnf_transformation,[],[f552]) ).
tcf(c_289,negated_conjecture,
( sP11
| aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xm)),sdtlpdtrp0(xN,xm)) ),
inference(cnf_transformation,[],[f563]) ).
tcf(c_293,negated_conjecture,
( sP11
| ( szmzizndt0(sdtlpdtrp0(xN,xn)) = szmzizndt0(sdtlpdtrp0(xN,xm)) ) ),
inference(cnf_transformation,[],[f559]) ).
tcf(c_294,negated_conjecture,
sdtlseqdt0(szszuzczcdt0(xn),xm),
inference(cnf_transformation,[],[f558]) ).
tcf(c_486,plain,
! [X0: $i] :
( sP9(X0)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(global_subsumption_just,[status(thm)],[c_265,c_270,c_269,c_266]) ).
tcf(c_776,plain,
( aElementOf0(szszuzczcdt0(xn),szNzAzT0)
| ~ aElementOf0(xn,szNzAzT0) ),
inference(instantiation,[status(thm)],[c_97]) ).
tcf(c_827,plain,
( sP9(xn)
| ~ aElementOf0(xn,szNzAzT0) ),
inference(instantiation,[status(thm)],[c_486]) ).
tcf(c_828,plain,
( sP9(xm)
| ~ aElementOf0(xm,szNzAzT0) ),
inference(instantiation,[status(thm)],[c_486]) ).
tcf(c_1235,plain,
( aSubsetOf0(sdtlpdtrp0(xN,xm),sdtlpdtrp0(xN,szszuzczcdt0(xn)))
| ~ aElementOf0(xm,szNzAzT0)
| ~ sdtlseqdt0(szszuzczcdt0(xn),xm)
| ~ aElementOf0(szszuzczcdt0(xn),szNzAzT0) ),
inference(instantiation,[status(thm)],[c_272]) ).
tcf(c_1362,plain,
! [X0: $i] :
( aElementOf0(X0,sdtlpdtrp0(xN,szszuzczcdt0(xn)))
| ~ aElementOf0(xm,szNzAzT0)
| ~ sdtlseqdt0(szszuzczcdt0(xn),xm)
| ~ aElementOf0(szszuzczcdt0(xn),szNzAzT0)
| ~ aElementOf0(X0,sdtlpdtrp0(xN,xm)) ),
inference(instantiation,[status(thm)],[c_271]) ).
tcf(c_2432,plain,
( aElementOf0(sK42,sdtlpdtrp0(xN,szszuzczcdt0(xn)))
| ~ aElementOf0(xm,szNzAzT0)
| ~ sdtlseqdt0(szszuzczcdt0(xn),xm)
| ~ aElementOf0(szszuzczcdt0(xn),szNzAzT0)
| ~ aElementOf0(sK42,sdtlpdtrp0(xN,xm)) ),
inference(instantiation,[status(thm)],[c_1362]) ).
tcf(c_3606,plain,
( aSet0(sdtlpdtrp0(xN,szszuzczcdt0(xn)))
| ~ aElementOf0(szszuzczcdt0(xn),szNzAzT0) ),
inference(instantiation,[status(thm)],[c_267]) ).
tcf(c_7082,plain,
( aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xm)),sdtlpdtrp0(xN,xm))
| ~ sP9(xm) ),
inference(instantiation,[status(thm)],[c_249]) ).
tcf(c_13952,plain,
( ~ sP11
| ~ sP9(xn)
| ~ aElementOf0(sK42,sdtlpdtrp0(xN,szszuzczcdt0(xn))) ),
inference(superposition,[status(thm)],[c_254,c_278]) ).
tcf(c_14476,plain,
~ sP11,
inference(global_subsumption_just,[status(thm)],[c_13952,c_277,c_276,c_294,c_279,c_776,c_827,c_2432,c_13952]) ).
tcf(c_14883,negated_conjecture,
aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xm)),sdtlpdtrp0(xN,xm)),
inference(global_subsumption_just,[status(thm)],[c_289,c_277,c_828,c_7082]) ).
tcf(c_14887,negated_conjecture,
szmzizndt0(sdtlpdtrp0(xN,xn)) = szmzizndt0(sdtlpdtrp0(xN,xm)),
inference(global_subsumption_just,[status(thm)],[c_293,c_293,c_14476]) ).
tcf(c_14890,plain,
aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xn)),sdtlpdtrp0(xN,xm)),
inference(superposition,[status(thm)],[c_14887,c_14883]) ).
tcf(c_15693,plain,
! [X0: $i] :
( aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xn)),X0)
| ~ aSet0(X0)
| ~ aSubsetOf0(sdtlpdtrp0(xN,xm),X0) ),
inference(superposition,[status(thm)],[c_14890,c_59]) ).
fof(f224,definition,
! [X0] :
( ~ sP8(X0)
| ! [X3] :
( aElementOf0(X3,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
<=> ( szmzizndt0(sdtlpdtrp0(xN,X0)) != X3
& aElementOf0(X3,sdtlpdtrp0(xN,X0))
& aElement0(X3) ) ) ),
introduced(definition,[new_symbols(definition,[sP8])],[predicate_definition_introduction]) ).
fof(f225,definition,
! [X0] :
( ~ sP9(X0)
| ( isCountable0(sdtlpdtrp0(xN,szszuzczcdt0(X0)))
& aSubsetOf0(sdtlpdtrp0(xN,szszuzczcdt0(X0)),sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
& ! [X4] :
( ~ aElementOf0(X4,sdtlpdtrp0(xN,szszuzczcdt0(X0)))
| aElementOf0(X4,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0)))) )
& aSet0(sdtlpdtrp0(xN,szszuzczcdt0(X0)))
& sP8(X0)
& aSet0(sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
& ! [X2] :
( ~ aElementOf0(X2,sdtlpdtrp0(xN,X0))
| sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X0)),X2) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X0)),sdtlpdtrp0(xN,X0)) ) ),
introduced(definition,[new_symbols(definition,[sP9])],[predicate_definition_introduction]) ).
fof(f226,plain,
( ! [X0] :
( ~ aElementOf0(X0,szNzAzT0)
| ~ isCountable0(sdtlpdtrp0(xN,X0))
| ( ~ aSubsetOf0(sdtlpdtrp0(xN,X0),szNzAzT0)
& ( ? [X1] :
( aElementOf0(X1,sdtlpdtrp0(xN,X0))
& ~ aElementOf0(X1,szNzAzT0) )
| ~ aSet0(sdtlpdtrp0(xN,X0)) ) )
| sP9(X0) )
& sdtlpdtrp0(xN,sz00) = xS
& szDzozmdt0(xN) = szNzAzT0
& aFunction0(xN) ),
inference(definition_folding,[],[f205,f225,f224]) ).
fof(f307,plain,
! [X0] :
( ~ sP8(X0)
| ! [X3] :
( ( ~ aElementOf0(X3,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
| ( szmzizndt0(sdtlpdtrp0(xN,X0)) != X3
& aElementOf0(X3,sdtlpdtrp0(xN,X0))
& aElement0(X3) ) )
& ( szmzizndt0(sdtlpdtrp0(xN,X0)) = X3
| ~ aElementOf0(X3,sdtlpdtrp0(xN,X0))
| ~ aElement0(X3)
| aElementOf0(X3,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0)))) ) ) ),
inference(nnf_transformation,[],[f224]) ).
fof(f308,plain,
! [X0] :
( ~ sP8(X0)
| ! [X3] :
( ( ~ aElementOf0(X3,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
| ( szmzizndt0(sdtlpdtrp0(xN,X0)) != X3
& aElementOf0(X3,sdtlpdtrp0(xN,X0))
& aElement0(X3) ) )
& ( szmzizndt0(sdtlpdtrp0(xN,X0)) = X3
| ~ aElementOf0(X3,sdtlpdtrp0(xN,X0))
| ~ aElement0(X3)
| aElementOf0(X3,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0)))) ) ) ),
inference(flattening,[],[f307]) ).
fof(f309,plain,
! [X0] :
( ~ sP8(X0)
| ! [X1] :
( ( ~ aElementOf0(X1,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
| ( szmzizndt0(sdtlpdtrp0(xN,X0)) != X1
& aElementOf0(X1,sdtlpdtrp0(xN,X0))
& aElement0(X1) ) )
& ( szmzizndt0(sdtlpdtrp0(xN,X0)) = X1
| ~ aElementOf0(X1,sdtlpdtrp0(xN,X0))
| ~ aElement0(X1)
| aElementOf0(X1,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0)))) ) ) ),
inference(rectify,[],[f308]) ).
fof(f526,plain,
! [X0,X1] :
( ~ sP8(X0)
| ~ aElementOf0(X1,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
| szmzizndt0(sdtlpdtrp0(xN,X0)) != X1 ),
inference(cnf_transformation,[],[f309]) ).
fof(f606,plain,
! [X0] :
( ~ sP8(X0)
| ~ aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X0)),sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0)))) ),
inference(equality_resolution,[],[f526]) ).
tcf(c_260,negated_conjecture,
! [X0: $i] :
( ~ sP8(X0)
| ~ aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X0)),sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0)))) ),
inference(cnf_transformation,[],[f606]) ).
tcf(c_13951,plain,
! [X0: $i] :
( ~ sP8(X0)
| ~ sP9(X0)
| ~ aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X0)),sdtlpdtrp0(xN,szszuzczcdt0(X0))) ),
inference(superposition,[status(thm)],[c_254,c_260]) ).
tcf(c_17710,plain,
! [X0: $i] :
( ~ sP8(X0)
| ~ sP9(X0)
| ~ aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X0)),sdtlpdtrp0(xN,szszuzczcdt0(X0))) ),
inference(superposition,[status(thm)],[c_254,c_260]) ).
tcf(c_17810,plain,
! [X0: $i] :
( ~ aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X0)),sdtlpdtrp0(xN,szszuzczcdt0(X0)))
| ~ sP9(X0) ),
inference(global_subsumption_just,[status(thm)],[c_17710,c_252,c_13951]) ).
tcf(c_17811,plain,
! [X0: $i] :
( ~ sP9(X0)
| ~ aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X0)),sdtlpdtrp0(xN,szszuzczcdt0(X0))) ),
inference(renaming,[status(thm)],[c_17810]) ).
tcf(c_17818,plain,
( ~ sP9(xn)
| ~ aSet0(sdtlpdtrp0(xN,szszuzczcdt0(xn)))
| ~ aSubsetOf0(sdtlpdtrp0(xN,xm),sdtlpdtrp0(xN,szszuzczcdt0(xn))) ),
inference(superposition,[status(thm)],[c_15693,c_17811]) ).
tcf(c_17826,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_17818,c_3606,c_1235,c_827,c_776,c_294,c_276,c_277]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : NUM577+3 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.07 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.18/0.45 % Computer : n020.cluster.edu
% 0.18/0.45 % Model : x86_64 x86_64
% 0.18/0.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.45 % Memory : 8046.5625MB
% 0.18/0.45 % OS : Linux 6.8.0-71-generic
% 0.18/0.45 % CPULimit : 300
% 0.18/0.45 % WCLimit : 300
% 0.18/0.45 % DateTime : Thu Sep 24 04:44:04 UTC 2026
% 0.18/0.45 % CPUTime :
% 0.18/0.45 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.23/0.51 Running first-order theorem proving
% 0.23/0.51 Running: /export/starexec/sandbox/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.23/0.53
% 0.23/0.53 % ======== iProver multi-core TPTP/SMT =========
% 0.23/0.53
% 0.23/0.53 % Detected problem language: tptp
% 0.23/0.54 % Proving...
% 22.64/4.02 % SZS status Started for theBenchmark.p
% 22.64/4.02 % SZS status Theorem for theBenchmark.p
% 22.64/4.02
% 22.64/4.02 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 22.64/4.02
% 22.64/4.02 % ------ iProver source info
% 22.64/4.02
% 22.64/4.02 % git: date: 2026-07-19 20:42:38 +0200
% 22.64/4.02 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 22.64/4.02 % git: non_committed_changes: false
% 22.64/4.02
% 22.64/4.02 % ------ Parsing...
% 22.64/4.02 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 22.64/4.02
% 22.64/4.02 % ------ Preprocessing... sup_sim: 0 sf_s rm: 1 0s sf_e sup_sim: 0 sf_s rm: 1 0s sf_e %
% 22.64/4.02
% 22.64/4.02 % ------ Preprocessing...%
% 22.64/4.02
% 22.64/4.02 % ------ Preprocessing... sf_s rm: 1 0s sf_e sf_s rm: 0 0s sf_e
% 22.64/4.02 % ------ Proving...
% 22.64/4.02 % ------ Problem Properties
% 22.64/4.02
% 22.64/4.02 %
% 22.64/4.02 % clauses 243
% 22.64/4.02 % conjectures 22
% 22.64/4.02 % EPR 52
% 22.64/4.02 % Horn 186
% 22.64/4.02 % unary 30
% 22.64/4.02 % binary 61
% 22.64/4.02 % lits 802
% 22.64/4.02 % lits eq 100
% 22.64/4.02 % fd_pure 0
% 22.64/4.02 % fd_pseudo 0
% 22.64/4.02 % fd_cond 11
% 22.64/4.02 % fd_pseudo_cond 30
% 22.64/4.02 % AC symbols 0
% 22.64/4.02
% 22.64/4.02 % ------ Input Options Time Limit: Unbounded
% 22.64/4.02
% 22.64/4.02
% 22.64/4.02 % ------
% 22.64/4.02 % Current options:
% 22.64/4.02 % ------
% 22.64/4.02
% 22.64/4.02
% 22.64/4.02 %
% 22.64/4.02
% 22.64/4.02 % ------ Proving...
% 22.64/4.02 %
% 22.64/4.02
% 22.64/4.02 % SZS status Theorem for theBenchmark.p
% 22.64/4.02
% 22.64/4.02 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 22.64/4.02
% 22.64/4.02
%------------------------------------------------------------------------------