%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : SWW306+1 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n017.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 : Sun Sep 27 09:11:40 AM UTC 2026
% Result : Theorem 119.90s 19.55s
% Output : CNFRefutation 119.90s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 6
% Syntax : Number of formulae : 27 ( 10 unt; 0 def)
% Number of atoms : 57 ( 8 equ)
% Maximal formula atoms : 5 ( 2 avg)
% Number of connectives : 57 ( 27 ~; 21 |; 2 &)
% ( 0 <=>; 7 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 4 avg)
% Maximal term depth : 8 ( 2 avg)
% Number of predicates : 5 ( 3 usr; 1 prp; 0-3 aty)
% Number of functors : 19 ( 19 usr; 8 con; 0-4 aty)
% Number of variables : 71 ( 8 sgn 24 !; 4 ?)
% Comments :
%------------------------------------------------------------------------------
fof(fact_singleton__conv2,axiom,
! [X0,X1] : hAPP('c$uSet$uOCollect'(X1),hAPP('c$ufequal',X0)) = hAPP(hAPP('c$uSet$uOinsert'(X1),X0),'c$uOrderings$uObot$u$uclass$uObot'('tc$ufun'(X1,'tc$uHOL$uObool'))) ).
fof(help_c__COMBK__1,axiom,
! [X0,X1,X2,X3] : hAPP(hAPP('c$uCOMBK'(X3,X2),X1),X0) = X1 ).
fof(help_c__COMBC__1,axiom,
! [X0,X1,X2,X3,X4,X5] : hAPP(hAPP(hAPP('c$uCOMBC'(X5,X4,X3),X2),X1),X0) = hAPP(hAPP(X2,X0),X1) ).
fof(help_c__fequal__2,axiom,
! [X0,X1] :
( hBOOL(hAPP(hAPP('c$ufequal',X1),X0))
| X1 != X0 ) ).
fof(conj_0,hypothesis,
! [X0,X1] :
( 'v$uP'(X0,X1)
=> 'c$uHoare$u$uMirabelle$uOhoare$u$uderivs'('t$ua','v$uG',hAPP(hAPP('c$uSet$uOinsert'('tc$uHoare$u$uMirabelle$uOtriple'('t$ua')),'c$uHoare$u$uMirabelle$uOtriple$uOtriple'('t$ua',hAPP('c$uCOMBK'('tc$ufun'('tc$uCom$uOstate','tc$uHOL$uObool'),'t$ua'),hAPP(hAPP('c$uCOMBC'('tc$uCom$uOstate','tc$uCom$uOstate','tc$uHOL$uObool'),'c$ufequal'),X1)),'v$uc',hAPP('c$uCOMBK'('tc$ufun'('tc$uCom$uOstate','tc$uHOL$uObool'),'t$ua'),'v$uQ'(X0)))),'c$uOrderings$uObot$u$uclass$uObot'('tc$ufun'('tc$uHoare$u$uMirabelle$uOtriple'('t$ua'),'tc$uHOL$uObool')))) ) ).
fof(conj_1,conjecture,
! [X0,X1] :
( 'v$uP'(X0,X1)
=> ? [X2,X3] :
( ! [X4] :
( ! [X5] :
( hBOOL(hAPP(hAPP(X2,X5),X1))
=> hBOOL(hAPP(hAPP(X3,X5),X4)) )
=> hBOOL(hAPP('v$uQ'(X0),X4)) )
& 'c$uHoare$u$uMirabelle$uOhoare$u$uderivs'('t$ua','v$uG',hAPP(hAPP('c$uSet$uOinsert'('tc$uHoare$u$uMirabelle$uOtriple'('t$ua')),'c$uHoare$u$uMirabelle$uOtriple$uOtriple'('t$ua',X2,'v$uc',X3)),'c$uOrderings$uObot$u$uclass$uObot'('tc$ufun'('tc$uHoare$u$uMirabelle$uOtriple'('t$ua'),'tc$uHOL$uObool')))) ) ) ).
fof(negated_conjecture,negated_conjecture,
~ ! [X0,X1] :
( 'v$uP'(X0,X1)
=> ? [X2,X3] :
( ! [X4] :
( ! [X5] :
( hBOOL(hAPP(hAPP(X2,X5),X1))
=> hBOOL(hAPP(hAPP(X3,X5),X4)) )
=> hBOOL(hAPP('v$uQ'(X0),X4)) )
& 'c$uHoare$u$uMirabelle$uOhoare$u$uderivs'('t$ua','v$uG',hAPP(hAPP('c$uSet$uOinsert'('tc$uHoare$u$uMirabelle$uOtriple'('t$ua')),'c$uHoare$u$uMirabelle$uOtriple$uOtriple'('t$ua',X2,'v$uc',X3)),'c$uOrderings$uObot$u$uclass$uObot'('tc$ufun'('tc$uHoare$u$uMirabelle$uOtriple'('t$ua'),'tc$uHOL$uObool')))) ) ),
inference(negate_conjecture,[status(cth)],[conj_1]) ).
cnf(c40,plain,
hAPP('c$uSet$uOCollect'(X0),hAPP('c$ufequal',X1)) = hAPP(hAPP('c$uSet$uOinsert'(X0),X1),'c$uOrderings$uObot$u$uclass$uObot'('tc$ufun'(X0,'tc$uHOL$uObool'))),
inference(clausification,[status(esa)],[fact_singleton__conv2]) ).
cnf(c687,plain,
hAPP(hAPP('c$uCOMBK'(X0,X1),X2),X3) = X2,
inference(clausification,[status(esa)],[help_c__COMBK__1]) ).
cnf(c688,plain,
hAPP(hAPP(hAPP('c$uCOMBC'(X0,X1,X2),X3),X4),X5) = hAPP(hAPP(X3,X5),X4),
inference(clausification,[status(esa)],[help_c__COMBC__1]) ).
cnf(c690,plain,
( hBOOL(hAPP(hAPP('c$ufequal',X0),X1))
| X0 != X1 ),
inference(clausification,[status(esa)],[help_c__fequal__2]) ).
cnf(c691,plain,
( 'c$uHoare$u$uMirabelle$uOhoare$u$uderivs'('t$ua','v$uG',hAPP(hAPP('c$uSet$uOinsert'('tc$uHoare$u$uMirabelle$uOtriple'('t$ua')),'c$uHoare$u$uMirabelle$uOtriple$uOtriple'('t$ua',hAPP('c$uCOMBK'('tc$ufun'('tc$uCom$uOstate','tc$uHOL$uObool'),'t$ua'),hAPP(hAPP('c$uCOMBC'('tc$uCom$uOstate','tc$uCom$uOstate','tc$uHOL$uObool'),'c$ufequal'),X1)),'v$uc',hAPP('c$uCOMBK'('tc$ufun'('tc$uCom$uOstate','tc$uHOL$uObool'),'t$ua'),'v$uQ'(X0)))),'c$uOrderings$uObot$u$uclass$uObot'('tc$ufun'('tc$uHoare$u$uMirabelle$uOtriple'('t$ua'),'tc$uHOL$uObool'))))
| ~ 'v$uP'(X0,X1) ),
inference(clausification,[status(esa)],[conj_0]) ).
cnf(c692,plain,
'v$uP'(sK1634,sK1635),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(c693,plain,
( hBOOL(hAPP(hAPP(X1,X2),sK1638(X0,X1)))
| ~ hBOOL(hAPP(hAPP(X0,X2),sK1635))
| ~ 'c$uHoare$u$uMirabelle$uOhoare$u$uderivs'('t$ua','v$uG',hAPP(hAPP('c$uSet$uOinsert'('tc$uHoare$u$uMirabelle$uOtriple'('t$ua')),'c$uHoare$u$uMirabelle$uOtriple$uOtriple'('t$ua',X0,'v$uc',X1)),'c$uOrderings$uObot$u$uclass$uObot'('tc$ufun'('tc$uHoare$u$uMirabelle$uOtriple'('t$ua'),'tc$uHOL$uObool')))) ),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(c694,plain,
( ~ hBOOL(hAPP('v$uQ'(sK1634),sK1638(X0,X1)))
| ~ 'c$uHoare$u$uMirabelle$uOhoare$u$uderivs'('t$ua','v$uG',hAPP(hAPP('c$uSet$uOinsert'('tc$uHoare$u$uMirabelle$uOtriple'('t$ua')),'c$uHoare$u$uMirabelle$uOtriple$uOtriple'('t$ua',X0,'v$uc',X1)),'c$uOrderings$uObot$u$uclass$uObot'('tc$ufun'('tc$uHoare$u$uMirabelle$uOtriple'('t$ua'),'tc$uHOL$uObool')))) ),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(d0,plain,
hBOOL(hAPP(hAPP('c$ufequal',X0),X0)),
inference(equality_resolution,[status(thm)],[c690]) ).
cnf(d1,plain,
( ~ hBOOL(hAPP('v$uQ'(sK1634),sK1638(X0,X1)))
| ~ 'c$uHoare$u$uMirabelle$uOhoare$u$uderivs'('t$ua','v$uG',hAPP('c$uSet$uOCollect'('tc$uHoare$u$uMirabelle$uOtriple'('t$ua')),hAPP('c$ufequal','c$uHoare$u$uMirabelle$uOtriple$uOtriple'('t$ua',X0,'v$uc',X1)))) ),
inference(demodulation,[status(thm)],[c694,c40]) ).
cnf(d2,plain,
( ~ 'v$uP'(X1,X0)
| 'c$uHoare$u$uMirabelle$uOhoare$u$uderivs'('t$ua','v$uG',hAPP('c$uSet$uOCollect'('tc$uHoare$u$uMirabelle$uOtriple'('t$ua')),hAPP('c$ufequal','c$uHoare$u$uMirabelle$uOtriple$uOtriple'('t$ua',hAPP('c$uCOMBK'('tc$ufun'('tc$uCom$uOstate','tc$uHOL$uObool'),'t$ua'),hAPP(hAPP('c$uCOMBC'('tc$uCom$uOstate','tc$uCom$uOstate','tc$uHOL$uObool'),'c$ufequal'),X0)),'v$uc',hAPP('c$uCOMBK'('tc$ufun'('tc$uCom$uOstate','tc$uHOL$uObool'),'t$ua'),'v$uQ'(X1)))))) ),
inference(demodulation,[status(thm)],[c691,c40]) ).
cnf(d3,plain,
( ~ hBOOL(hAPP('v$uQ'(sK1634),sK1638(hAPP('c$uCOMBK'('tc$ufun'('tc$uCom$uOstate','tc$uHOL$uObool'),'t$ua'),hAPP(hAPP('c$uCOMBC'('tc$uCom$uOstate','tc$uCom$uOstate','tc$uHOL$uObool'),'c$ufequal'),X1)),hAPP('c$uCOMBK'('tc$ufun'('tc$uCom$uOstate','tc$uHOL$uObool'),'t$ua'),'v$uQ'(X0)))))
| ~ 'v$uP'(X0,X1) ),
inference(resolution,[status(thm)],[d2,d1]) ).
cnf(d4,plain,
( ~ hBOOL(hAPP(hAPP(X0,X2),sK1635))
| hBOOL(hAPP(hAPP(X1,X2),sK1638(X0,X1)))
| ~ 'c$uHoare$u$uMirabelle$uOhoare$u$uderivs'('t$ua','v$uG',hAPP('c$uSet$uOCollect'('tc$uHoare$u$uMirabelle$uOtriple'('t$ua')),hAPP('c$ufequal','c$uHoare$u$uMirabelle$uOtriple$uOtriple'('t$ua',X0,'v$uc',X1)))) ),
inference(demodulation,[status(thm)],[c693,c40]) ).
cnf(d5,plain,
( ~ hBOOL(hAPP(hAPP(hAPP('c$uCOMBK'('tc$ufun'('tc$uCom$uOstate','tc$uHOL$uObool'),'t$ua'),hAPP(hAPP('c$uCOMBC'('tc$uCom$uOstate','tc$uCom$uOstate','tc$uHOL$uObool'),'c$ufequal'),X1)),X2),sK1635))
| hBOOL(hAPP(hAPP(hAPP('c$uCOMBK'('tc$ufun'('tc$uCom$uOstate','tc$uHOL$uObool'),'t$ua'),'v$uQ'(X0)),X2),sK1638(hAPP('c$uCOMBK'('tc$ufun'('tc$uCom$uOstate','tc$uHOL$uObool'),'t$ua'),hAPP(hAPP('c$uCOMBC'('tc$uCom$uOstate','tc$uCom$uOstate','tc$uHOL$uObool'),'c$ufequal'),X1)),hAPP('c$uCOMBK'('tc$ufun'('tc$uCom$uOstate','tc$uHOL$uObool'),'t$ua'),'v$uQ'(X0)))))
| ~ 'v$uP'(X0,X1) ),
inference(resolution,[status(thm)],[d2,d4]) ).
cnf(d6,plain,
( ~ 'v$uP'(X2,X0)
| hBOOL(hAPP(hAPP(hAPP('c$uCOMBK'('tc$ufun'('tc$uCom$uOstate','tc$uHOL$uObool'),'t$ua'),'v$uQ'(X2)),X1),sK1638(hAPP('c$uCOMBK'('tc$ufun'('tc$uCom$uOstate','tc$uHOL$uObool'),'t$ua'),hAPP(hAPP('c$uCOMBC'('tc$uCom$uOstate','tc$uCom$uOstate','tc$uHOL$uObool'),'c$ufequal'),X0)),hAPP('c$uCOMBK'('tc$ufun'('tc$uCom$uOstate','tc$uHOL$uObool'),'t$ua'),'v$uQ'(X2)))))
| ~ hBOOL(hAPP(hAPP(hAPP('c$uCOMBC'('tc$uCom$uOstate','tc$uCom$uOstate','tc$uHOL$uObool'),'c$ufequal'),X0),sK1635)) ),
inference(demodulation,[status(thm)],[d5,c687]) ).
cnf(d7,plain,
( ~ 'v$uP'(X1,X0)
| hBOOL(hAPP(hAPP(hAPP('c$uCOMBK'('tc$ufun'('tc$uCom$uOstate','tc$uHOL$uObool'),'t$ua'),'v$uQ'(X1)),X2),sK1638(hAPP('c$uCOMBK'('tc$ufun'('tc$uCom$uOstate','tc$uHOL$uObool'),'t$ua'),hAPP(hAPP('c$uCOMBC'('tc$uCom$uOstate','tc$uCom$uOstate','tc$uHOL$uObool'),'c$ufequal'),X0)),hAPP('c$uCOMBK'('tc$ufun'('tc$uCom$uOstate','tc$uHOL$uObool'),'t$ua'),'v$uQ'(X1)))))
| ~ hBOOL(hAPP(hAPP('c$ufequal',sK1635),X0)) ),
inference(demodulation,[status(thm)],[d6,c688]) ).
cnf(d8,plain,
( ~ 'v$uP'(X0,X2)
| hBOOL(hAPP('v$uQ'(X0),sK1638(hAPP('c$uCOMBK'('tc$ufun'('tc$uCom$uOstate','tc$uHOL$uObool'),'t$ua'),hAPP(hAPP('c$uCOMBC'('tc$uCom$uOstate','tc$uCom$uOstate','tc$uHOL$uObool'),'c$ufequal'),X2)),hAPP('c$uCOMBK'('tc$ufun'('tc$uCom$uOstate','tc$uHOL$uObool'),'t$ua'),'v$uQ'(X0)))))
| ~ hBOOL(hAPP(hAPP('c$ufequal',sK1635),X2)) ),
inference(demodulation,[status(thm)],[d7,c687]) ).
cnf(d9,plain,
( ~ 'v$uP'(sK1634,X0)
| ~ 'v$uP'(sK1634,X0)
| ~ hBOOL(hAPP(hAPP('c$ufequal',sK1635),X0)) ),
inference(resolution,[status(thm)],[d8,d3]) ).
cnf(d10,plain,
~ 'v$uP'(sK1634,sK1635),
inference(resolution,[status(thm)],[d9,d0]) ).
cnf(d11,plain,
$false,
inference(resolution,[status(thm)],[c692,d10]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWW306+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.04 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.36 % Computer : n017.cluster.edu
% 0.08/0.36 % Model : x86_64 x86_64
% 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36 % Memory : 8046.5625MB
% 0.08/0.36 % OS : Linux 6.8.0-71-generic
% 0.08/0.36 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.08/0.36 % DateTime : Sat Sep 26 15:33:18 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.08/0.36 Running casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 119.90/19.55 % SZS status Theorem for theBenchmark.p
% 119.90/19.55 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
%------------------------------------------------------------------------------