%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : NUM592+3 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% Computer : n002.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:09 PM UTC 2026
% Result : Theorem 29.42s 19.85s
% Output : CNFRefutation 29.42s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named f271ERROR: Could not build tree for root c_17783ERROR: MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
fof(f91,axiom,
( xd = sdtlpdtrp0(xC,xi)
& xY = sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi)))
& ! [X0] :
( aElementOf0(X0,xY)
<=> ( X0 != szmzizndt0(sdtlpdtrp0(xN,xi))
& aElementOf0(X0,sdtlpdtrp0(xN,xi))
& aElement0(X0) ) )
& aSet0(xY)
& ! [X0] :
( aElementOf0(X0,sdtlpdtrp0(xN,xi))
=> sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),X0) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__4448_02) ).
fof(f93,axiom,
( ! [X0] :
( ( ( aElementOf0(X0,slbdtsldtrb0(xX,xk))
| ( sbrdtbr0(X0) = xk
& ( aSubsetOf0(X0,xX)
| ! [X1] :
( aElementOf0(X1,X0)
=> aElementOf0(X1,xX) ) ) ) )
& aSet0(X0) )
=> sdtlpdtrp0(xd,X0) = xu )
& isCountable0(xX)
& aSubsetOf0(xX,xY)
& ! [X0] :
( aElementOf0(X0,xX)
=> aElementOf0(X0,xY) )
& aSet0(xX)
& aElementOf0(xu,xT) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__4545) ).
fof(f111,plain,
( xd = sdtlpdtrp0(xC,xi)
& xY = sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi)))
& ! [X1] :
( aElementOf0(X1,xY)
<=> ( szmzizndt0(sdtlpdtrp0(xN,xi)) != X1
& aElementOf0(X1,sdtlpdtrp0(xN,xi))
& aElement0(X1) ) )
& aSet0(xY)
& ! [X0] :
( aElementOf0(X0,sdtlpdtrp0(xN,xi))
=> sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),X0) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi)) ),
inference(rectify,[],[f91]) ).
fof(f113,plain,
( ! [X1] :
( ( ( aElementOf0(X1,slbdtsldtrb0(xX,xk))
| ( sbrdtbr0(X1) = xk
& ( aSubsetOf0(X1,xX)
| ! [X2] :
( aElementOf0(X2,X1)
=> aElementOf0(X2,xX) ) ) ) )
& aSet0(X1) )
=> sdtlpdtrp0(xd,X1) = xu )
& isCountable0(xX)
& aSubsetOf0(xX,xY)
& ! [X0] :
( aElementOf0(X0,xX)
=> aElementOf0(X0,xY) )
& aSet0(xX)
& aElementOf0(xu,xT) ),
inference(rectify,[],[f93]) ).
fof(f233,plain,
( xd = sdtlpdtrp0(xC,xi)
& xY = sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi)))
& ! [X1] :
( aElementOf0(X1,xY)
<=> ( szmzizndt0(sdtlpdtrp0(xN,xi)) != X1
& aElementOf0(X1,sdtlpdtrp0(xN,xi))
& aElement0(X1) ) )
& aSet0(xY)
& ! [X0] :
( ~ aElementOf0(X0,sdtlpdtrp0(xN,xi))
| sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),X0) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi)) ),
inference(ennf_transformation,[],[f111]) ).
fof(f236,plain,
( ! [X1] :
( ( ~ aElementOf0(X1,slbdtsldtrb0(xX,xk))
& ( sbrdtbr0(X1) != xk
| ( ~ aSubsetOf0(X1,xX)
& ? [X2] :
( aElementOf0(X2,X1)
& ~ aElementOf0(X2,xX) ) ) ) )
| ~ aSet0(X1)
| sdtlpdtrp0(xd,X1) = xu )
& isCountable0(xX)
& aSubsetOf0(xX,xY)
& ! [X0] :
( ~ aElementOf0(X0,xX)
| aElementOf0(X0,xY) )
& aSet0(xX)
& aElementOf0(xu,xT) ),
inference(ennf_transformation,[],[f113]) ).
fof(f237,plain,
( ! [X1] :
( ( ~ aElementOf0(X1,slbdtsldtrb0(xX,xk))
& ( sbrdtbr0(X1) != xk
| ( ~ aSubsetOf0(X1,xX)
& ? [X2] :
( aElementOf0(X2,X1)
& ~ aElementOf0(X2,xX) ) ) ) )
| ~ aSet0(X1)
| sdtlpdtrp0(xd,X1) = xu )
& isCountable0(xX)
& aSubsetOf0(xX,xY)
& ! [X0] :
( ~ aElementOf0(X0,xX)
| aElementOf0(X0,xY) )
& aSet0(xX)
& aElementOf0(xu,xT) ),
inference(flattening,[],[f236]) ).
fof(f396,plain,
( xd = sdtlpdtrp0(xC,xi)
& xY = sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi)))
& ! [X1] :
( ( ~ aElementOf0(X1,xY)
| ( szmzizndt0(sdtlpdtrp0(xN,xi)) != X1
& aElementOf0(X1,sdtlpdtrp0(xN,xi))
& aElement0(X1) ) )
& ( szmzizndt0(sdtlpdtrp0(xN,xi)) = X1
| ~ aElementOf0(X1,sdtlpdtrp0(xN,xi))
| ~ aElement0(X1)
| aElementOf0(X1,xY) ) )
& aSet0(xY)
& ! [X0] :
( ~ aElementOf0(X0,sdtlpdtrp0(xN,xi))
| sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),X0) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi)) ),
inference(nnf_transformation,[],[f233]) ).
fof(f397,plain,
( xd = sdtlpdtrp0(xC,xi)
& xY = sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi)))
& ! [X1] :
( ( ~ aElementOf0(X1,xY)
| ( szmzizndt0(sdtlpdtrp0(xN,xi)) != X1
& aElementOf0(X1,sdtlpdtrp0(xN,xi))
& aElement0(X1) ) )
& ( szmzizndt0(sdtlpdtrp0(xN,xi)) = X1
| ~ aElementOf0(X1,sdtlpdtrp0(xN,xi))
| ~ aElement0(X1)
| aElementOf0(X1,xY) ) )
& aSet0(xY)
& ! [X0] :
( ~ aElementOf0(X0,sdtlpdtrp0(xN,xi))
| sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),X0) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi)) ),
inference(flattening,[],[f396]) ).
fof(f401,plain,
( ! [X1] :
( ( ~ aElementOf0(X1,slbdtsldtrb0(xX,xk))
& ( sbrdtbr0(X1) != xk
| ( ~ aSubsetOf0(X1,xX)
& aElementOf0(sK63(X1),X1)
& ~ aElementOf0(sK63(X1),xX) ) ) )
| ~ aSet0(X1)
| sdtlpdtrp0(xd,X1) = xu )
& isCountable0(xX)
& aSubsetOf0(xX,xY)
& ! [X0] :
( ~ aElementOf0(X0,xX)
| aElementOf0(X0,xY) )
& aSet0(xX)
& aElementOf0(xu,xT) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK63]),skolemize(X2,sK63(X1))],[f237]) ).
fof(f402,plain,
! [X1] :
( ~ sP23(X1)
| ( ! [X2] :
( ~ aElementOf0(X2,sdtlpdtrp0(xN,xi))
| sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),X2) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi))
& sP22
& aSet0(sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))
& ~ aSubsetOf0(X1,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))
& ( ? [X4] :
( aElementOf0(X4,X1)
& ~ aElementOf0(X4,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi)))) )
| ~ aSet0(X1) ) ) ),
inference(nnf_transformation,[],[f270]) ).
fof(f403,plain,
! [X0] :
( ~ sP23(X0)
| ( ! [X2] :
( ~ aElementOf0(X2,sdtlpdtrp0(xN,xi))
| sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),X2) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi))
& sP22
& aSet0(sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))
& ~ aSubsetOf0(X0,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))
& ( ? [X1] :
( aElementOf0(X1,X0)
& ~ aElementOf0(X1,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi)))) )
| ~ aSet0(X0) ) ) ),
inference(rectify,[],[f402]) ).
fof(f404,plain,
! [X0] :
( ~ sP23(X0)
| ( ! [X2] :
( ~ aElementOf0(X2,sdtlpdtrp0(xN,xi))
| sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),X2) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi))
& sP22
& aSet0(sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))
& ~ aSubsetOf0(X0,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))
& ( ( aElementOf0(sK64(X0),X0)
& ~ aElementOf0(sK64(X0),sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi)))) )
| ~ aSet0(X0) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK64]),skolemize(X1,sK64(X0))],[f403]) ).
fof(f408,plain,
! [X0] :
( ! [X1] :
( ? [X2] :
( aElementOf0(X2,slbdtsldtrb0(X1,xk))
& sbrdtbr0(X2) = xk
& aSubsetOf0(X2,X1)
& ! [X3] :
( ~ aElementOf0(X3,X2)
| aElementOf0(X3,X1) )
& aSet0(X2)
& sdtlpdtrp0(sdtlpdtrp0(xC,xi),X2) != X0 )
| ~ isCountable0(X1)
| sP23(X1) )
| ~ aElementOf0(X0,xT) ),
inference(rectify,[],[f271]) ).
fof(f409,plain,
! [X0] :
( ! [X1] :
( ( aElementOf0(sK65(X0,X1),slbdtsldtrb0(X1,xk))
& xk = sbrdtbr0(sK65(X0,X1))
& aSubsetOf0(sK65(X0,X1),X1)
& ! [X3] :
( ~ aElementOf0(X3,sK65(X0,X1))
| aElementOf0(X3,X1) )
& aSet0(sK65(X0,X1))
& sdtlpdtrp0(sdtlpdtrp0(xC,xi),sK65(X0,X1)) != X0 )
| ~ isCountable0(X1)
| sP23(X1) )
| ~ aElementOf0(X0,xT) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK65]),skolemize(X2,sK65(X0,X1))],[f408]) ).
fof(f737,plain,
xd = sdtlpdtrp0(xC,xi),
inference(cnf_transformation,[],[f397]) ).
fof(f738,plain,
xY = sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))),
inference(cnf_transformation,[],[f397]) ).
fof(f761,plain,
! [X1] :
( ~ aElementOf0(X1,slbdtsldtrb0(xX,xk))
| ~ aSet0(X1)
| sdtlpdtrp0(xd,X1) = xu ),
inference(cnf_transformation,[],[f401]) ).
fof(f765,plain,
isCountable0(xX),
inference(cnf_transformation,[],[f401]) ).
fof(f766,plain,
aSubsetOf0(xX,xY),
inference(cnf_transformation,[],[f401]) ).
fof(f769,plain,
aElementOf0(xu,xT),
inference(cnf_transformation,[],[f401]) ).
fof(f774,plain,
! [X0] :
( ~ sP23(X0)
| ~ aSubsetOf0(X0,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi)))) ),
inference(cnf_transformation,[],[f404]) ).
fof(f781,plain,
! [X0,X1] :
( aElementOf0(sK65(X0,X1),slbdtsldtrb0(X1,xk))
| ~ isCountable0(X1)
| sP23(X1)
| ~ aElementOf0(X0,xT) ),
inference(cnf_transformation,[],[f409]) ).
fof(f785,plain,
! [X0,X1] :
( aSet0(sK65(X0,X1))
| ~ isCountable0(X1)
| sP23(X1)
| ~ aElementOf0(X0,xT) ),
inference(cnf_transformation,[],[f409]) ).
fof(f786,plain,
! [X0,X1] :
( sdtlpdtrp0(sdtlpdtrp0(xC,xi),sK65(X0,X1)) != X0
| ~ isCountable0(X1)
| sP23(X1)
| ~ aElementOf0(X0,xT) ),
inference(cnf_transformation,[],[f409]) ).
tcf(c_383,plain,
sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))) = xY,
inference(cnf_transformation,[],[f738]) ).
tcf(c_384,plain,
sdtlpdtrp0(xC,xi) = xd,
inference(cnf_transformation,[],[f737]) ).
tcf(c_400,plain,
aElementOf0(xu,xT),
inference(cnf_transformation,[],[f769]) ).
tcf(c_403,plain,
aSubsetOf0(xX,xY),
inference(cnf_transformation,[],[f766]) ).
tcf(c_404,plain,
isCountable0(xX),
inference(cnf_transformation,[],[f765]) ).
tcf(c_408,plain,
! [X0: $i] :
( ( sdtlpdtrp0(xd,X0) = xu )
| ~ aSet0(X0)
| ~ aElementOf0(X0,slbdtsldtrb0(xX,xk)) ),
inference(cnf_transformation,[],[f761]) ).
tcf(c_411,plain,
! [X0: $i] :
( ~ sP23(X0)
| ~ aSubsetOf0(X0,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi)))) ),
inference(cnf_transformation,[],[f774]) ).
tcf(c_420,negated_conjecture,
! [X0: $i,X1: $i] :
( sP23(X1)
| ~ isCountable0(X1)
| ~ aElementOf0(X0,xT)
| ( sdtlpdtrp0(sdtlpdtrp0(xC,xi),sK65(X0,X1)) != X0 ) ),
inference(cnf_transformation,[],[f786]) ).
tcf(c_421,negated_conjecture,
! [X0: $i,X1: $i] :
( sP23(X1)
| aSet0(sK65(X0,X1))
| ~ isCountable0(X1)
| ~ aElementOf0(X0,xT) ),
inference(cnf_transformation,[],[f785]) ).
tcf(c_425,negated_conjecture,
! [X0: $i,X1: $i] :
( sP23(X1)
| aElementOf0(sK65(X0,X1),slbdtsldtrb0(X1,xk))
| ~ isCountable0(X1)
| ~ aElementOf0(X0,xT) ),
inference(cnf_transformation,[],[f781]) ).
tcf(c_3143,plain,
! [X0: $i] :
( ~ sP23(X0)
| ~ aSubsetOf0(X0,xY) ),
inference(light_normalisation,[status(thm)],[c_411,c_383]) ).
tcf(c_3148,plain,
! [X0: $i,X1: $i] :
( sP23(X1)
| ~ isCountable0(X1)
| ~ aElementOf0(X0,xT)
| ( sdtlpdtrp0(xd,sK65(X0,X1)) != X0 ) ),
inference(light_normalisation,[status(thm)],[c_420,c_384]) ).
tcf(c_14578,plain,
! [X0: $i] :
( sP23(xX)
| ~ isCountable0(xX)
| ~ aElementOf0(X0,xT)
| ( sdtlpdtrp0(xd,sK65(X0,xX)) != X0 ) ),
inference(instantiation,[status(thm)],[c_3148]) ).
tcf(c_14603,plain,
! [X0: $i] :
( sP23(xX)
| aSet0(sK65(X0,xX))
| ~ isCountable0(xX)
| ~ aElementOf0(X0,xT) ),
inference(instantiation,[status(thm)],[c_421]) ).
tcf(c_14703,plain,
! [X0: $i] :
( sP23(xX)
| aElementOf0(sK65(X0,xX),slbdtsldtrb0(xX,xk))
| ~ isCountable0(xX)
| ~ aElementOf0(X0,xT) ),
inference(instantiation,[status(thm)],[c_425]) ).
tcf(c_14888,plain,
( sP23(xX)
| ~ isCountable0(xX)
| ~ aElementOf0(xu,xT)
| ( sdtlpdtrp0(xd,sK65(xu,xX)) != xu ) ),
inference(instantiation,[status(thm)],[c_14578]) ).
tcf(c_15505,plain,
( sP23(xX)
| aSet0(sK65(xu,xX))
| ~ isCountable0(xX)
| ~ aElementOf0(xu,xT) ),
inference(instantiation,[status(thm)],[c_14603]) ).
tcf(c_15723,plain,
( ~ sP23(xX)
| ~ aSubsetOf0(xX,xY) ),
inference(instantiation,[status(thm)],[c_3143]) ).
tcf(c_15987,plain,
( sP23(xX)
| aElementOf0(sK65(xu,xX),slbdtsldtrb0(xX,xk))
| ~ isCountable0(xX)
| ~ aElementOf0(xu,xT) ),
inference(instantiation,[status(thm)],[c_14703]) ).
tcf(c_17782,plain,
( ( sdtlpdtrp0(xd,sK65(xu,xX)) = xu )
| ~ aSet0(sK65(xu,xX))
| ~ aElementOf0(sK65(xu,xX),slbdtsldtrb0(xX,xk)) ),
inference(instantiation,[status(thm)],[c_408]) ).
tcf(c_17783,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_17782,c_15987,c_15723,c_15505,c_14888,c_400,c_403,c_404]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM592+3 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.12/15.40 % Computer : n002.cluster.edu
% 0.12/15.40 % Model : x86_64 x86_64
% 0.12/15.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/15.40 % Memory : 8046.5625MB
% 0.12/15.40 % OS : Linux 6.8.0-71-generic
% 0.12/15.40 % CPULimit : 300
% 0.12/15.40 % WCLimit : 300
% 0.12/15.40 % DateTime : Thu Sep 24 04:51:20 UTC 2026
% 0.12/15.40 % CPUTime :
% 0.12/15.40 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.12/15.44 Running first-order theorem proving
% 0.12/15.44 Running: /export/starexec/sandbox2/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.12/15.45
% 0.12/15.45 % ======== iProver multi-core TPTP/SMT =========
% 0.12/15.45
% 0.12/15.45 % Detected problem language: tptp
% 0.12/15.46 % Proving...
% 29.42/19.85 % SZS status Started for theBenchmark.p
% 29.42/19.85 % SZS status Theorem for theBenchmark.p
% 29.42/19.85
% 29.42/19.85 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 29.42/19.85
% 29.42/19.85 % ------ iProver source info
% 29.42/19.85
% 29.42/19.85 % git: date: 2026-07-19 20:42:38 +0200
% 29.42/19.85 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 29.42/19.85 % git: non_committed_changes: false
% 29.42/19.85
% 29.42/19.85 % ------ Parsing...
% 29.42/19.85 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 29.42/19.85
% 29.42/19.85 % ------ Preprocessing... sup_sim: 9 sf_s rm: 1 0s sf_e pe_s pe:1:0s pe:2:0s pe:4:0s pe:8:0s pe_e %
% 29.42/19.85
% 29.42/19.85 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 29.42/19.85
% 29.42/19.85 % ------ Preprocessing... sf_s rm: 1 0s sf_e
% 29.42/19.85 % ------ Proving...
% 29.42/19.85 % ------ Problem Properties
% 29.42/19.85
% 29.42/19.85 %
% 29.42/19.85 % clauses 346
% 29.42/19.85 % conjectures 5
% 29.42/19.85 % EPR 63
% 29.42/19.85 % Horn 267
% 29.42/19.85 % unary 41
% 29.42/19.85 % binary 85
% 29.42/19.85 % lits 1123
% 29.42/19.85 % lits eq 142
% 29.42/19.85 % fd_pure 0
% 29.42/19.85 % fd_pseudo 0
% 29.42/19.85 % fd_cond 11
% 29.42/19.85 % fd_pseudo_cond 39
% 29.42/19.85 % AC symbols 0
% 29.42/19.85
% 29.42/19.85 % ------ Input Options Time Limit: Unbounded
% 29.42/19.85
% 29.42/19.85
% 29.42/19.85 % ------
% 29.42/19.85 % Current options:
% 29.42/19.85 % ------
% 29.42/19.85
% 29.42/19.85
% 29.42/19.85 %
% 29.42/19.85
% 29.42/19.85 % ------ Proving...
% 29.42/19.85 %
% 29.42/19.85
% 29.42/19.85 % SZS status Theorem for theBenchmark.p
% 29.42/19.85
% 29.42/19.85 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 29.42/19.85
% 29.42/19.85
%------------------------------------------------------------------------------