%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : SWW474+5 : TPTP v9.3.1. Released v5.3.0.
% Transfm : none
% Format : tptp:raw
% Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n014.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:12:00 AM UTC 2026
% Result : Theorem 44.07s 21.05s
% Output : CNFRefutation 44.07s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 17
% Syntax : Number of formulae : 60 ( 33 unt; 0 def)
% Number of atoms : 100 ( 43 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 69 ( 29 ~; 31 |; 1 &)
% ( 0 <=>; 8 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 3 avg)
% Maximal term depth : 10 ( 2 avg)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 28 ( 28 usr; 14 con; 0-4 aty)
% Number of variables : 75 ( 9 sgn 28 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(tsy_c_Com_OWT__bodies_res,hypothesis,
ti(bool,'wT$ubodies') = 'wT$ubodies' ).
fof(tsy_c_Hoare__Mirabelle__pjuwniqynr_Ostate__not__singleton_res,hypothesis,
ti(bool,'hoare$u1883395792gleton') = 'hoare$u1883395792gleton' ).
fof(tsy_c_hAPP_res,axiom,
! [X0,X1,X2,X3] : ti(X0,hAPP(X1,X0,X2,X3)) = hAPP(X1,X0,X2,X3) ).
fof(fact_0_empty,axiom,
! [X0,X1] : hBOOL(hAPP(fun('hoare$u509422987triple'(X0),bool),bool,hAPP(fun('hoare$u509422987triple'(X0),bool),fun(fun('hoare$u509422987triple'(X0),bool),bool),'hoare$u122391849derivs'(X0),X1),'bot$ubot'(fun('hoare$u509422987triple'(X0),bool)))) ).
fof(fact_4_cut,axiom,
! [X0,X1,X2,X3] :
( hBOOL(hAPP(fun('hoare$u509422987triple'(X0),bool),bool,hAPP(fun('hoare$u509422987triple'(X0),bool),fun(fun('hoare$u509422987triple'(X0),bool),bool),'hoare$u122391849derivs'(X0),X2),X3))
=> ( hBOOL(hAPP(fun('hoare$u509422987triple'(X0),bool),bool,hAPP(fun('hoare$u509422987triple'(X0),bool),fun(fun('hoare$u509422987triple'(X0),bool),bool),'hoare$u122391849derivs'(X0),X1),X2))
=> hBOOL(hAPP(fun('hoare$u509422987triple'(X0),bool),bool,hAPP(fun('hoare$u509422987triple'(X0),bool),fun(fun('hoare$u509422987triple'(X0),bool),bool),'hoare$u122391849derivs'(X0),X1),X3)) ) ) ).
fof(fact_6_derivs__insertD,axiom,
! [X0,X1,X2,X3] :
( hBOOL(hAPP(fun('hoare$u509422987triple'(X0),bool),bool,hAPP(fun('hoare$u509422987triple'(X0),bool),fun(fun('hoare$u509422987triple'(X0),bool),bool),'hoare$u122391849derivs'(X0),X1),hAPP(fun('hoare$u509422987triple'(X0),bool),fun('hoare$u509422987triple'(X0),bool),hAPP('hoare$u509422987triple'(X0),fun(fun('hoare$u509422987triple'(X0),bool),fun('hoare$u509422987triple'(X0),bool)),insert('hoare$u509422987triple'(X0)),X2),X3)))
=> ( hBOOL(hAPP(fun('hoare$u509422987triple'(X0),bool),bool,hAPP(fun('hoare$u509422987triple'(X0),bool),fun(fun('hoare$u509422987triple'(X0),bool),bool),'hoare$u122391849derivs'(X0),X1),X3))
& hBOOL(hAPP(fun('hoare$u509422987triple'(X0),bool),bool,hAPP(fun('hoare$u509422987triple'(X0),bool),fun(fun('hoare$u509422987triple'(X0),bool),bool),'hoare$u122391849derivs'(X0),X1),hAPP(fun('hoare$u509422987triple'(X0),bool),fun('hoare$u509422987triple'(X0),bool),hAPP('hoare$u509422987triple'(X0),fun(fun('hoare$u509422987triple'(X0),bool),fun('hoare$u509422987triple'(X0),bool)),insert('hoare$u509422987triple'(X0)),X2),'bot$ubot'(fun('hoare$u509422987triple'(X0),bool))))) ) ) ).
fof(fact_19_MGF,axiom,
! [X0] :
( hBOOL('hoare$u1883395792gleton')
=> ( hBOOL('wT$ubodies')
=> ( hBOOL(hAPP(com,bool,wt,X0))
=> hBOOL(hAPP(fun('hoare$u509422987triple'(state),bool),bool,hAPP(fun('hoare$u509422987triple'(state),bool),fun(fun('hoare$u509422987triple'(state),bool),bool),'hoare$u122391849derivs'(state),'bot$ubot'(fun('hoare$u509422987triple'(state),bool))),hAPP(fun('hoare$u509422987triple'(state),bool),fun('hoare$u509422987triple'(state),bool),hAPP('hoare$u509422987triple'(state),fun(fun('hoare$u509422987triple'(state),bool),fun('hoare$u509422987triple'(state),bool)),insert('hoare$u509422987triple'(state)),hAPP(com,'hoare$u509422987triple'(state),'hoare$uMirabelle$uMGT',X0)),'bot$ubot'(fun('hoare$u509422987triple'(state),bool))))) ) ) ) ).
fof(fact_60_image__image,axiom,
! [X0,X1,X2,X3,X4,X5] : hAPP(fun(X0,bool),fun(X1,bool),hAPP(fun(X0,X1),fun(fun(X0,bool),fun(X1,bool)),image(X0,X1),X3),hAPP(fun(X2,bool),fun(X0,bool),hAPP(fun(X2,X0),fun(fun(X2,bool),fun(X0,bool)),image(X2,X0),X4),X5)) = hAPP(fun(X2,bool),fun(X1,bool),hAPP(fun(X2,X1),fun(fun(X2,bool),fun(X1,bool)),image(X2,X1),hAPP(fun(X2,X0),fun(X2,X1),hAPP(fun(X0,X1),fun(fun(X2,X0),fun(X2,X1)),combb(X0,X1,X2),X3),X4)),X5) ).
fof(fact_77_Collect__def,axiom,
! [X0,X1] : hAPP(fun(X0,bool),fun(X0,bool),collect(X0),X1) = ti(fun(X0,bool),X1) ).
fof(fact_90_singleton__conv2,axiom,
! [X0,X1] : hAPP(fun(X0,bool),fun(X0,bool),collect(X0),hAPP(X0,fun(X0,bool),fequal(X0),X1)) = hAPP(fun(X0,bool),fun(X0,bool),hAPP(X0,fun(fun(X0,bool),fun(X0,bool)),insert(X0),X1),'bot$ubot'(fun(X0,bool))) ).
fof(fact_92_WT__bodiesD,axiom,
! [X0,X1] :
( hBOOL('wT$ubodies')
=> ( hAPP(pname,option(com),body,X0) = hAPP(com,option(com),some(com),X1)
=> hBOOL(hAPP(com,bool,wt,X1)) ) ) ).
fof(help_fFalse_1_1_U,axiom,
~ hBOOL(fFalse) ).
fof(help_fFalse_1_1_T,axiom,
! [X0] :
( ti(bool,X0) = fFalse
| ti(bool,X0) = fTrue ) ).
fof(conj_0,hypothesis,
hBOOL('hoare$u1883395792gleton') ).
fof(conj_1,hypothesis,
hBOOL('wT$ubodies') ).
fof(conj_5,hypothesis,
hAPP(pname,option(com),body,pn) = hAPP(com,option(com),some(com),y) ).
fof(conj_7,conjecture,
hBOOL(hAPP(fun('hoare$u509422987triple'(state),bool),bool,hAPP(fun('hoare$u509422987triple'(state),bool),fun(fun('hoare$u509422987triple'(state),bool),bool),'hoare$u122391849derivs'(state),hAPP(fun(pname,bool),fun('hoare$u509422987triple'(state),bool),hAPP(fun(pname,'hoare$u509422987triple'(state)),fun(fun(pname,bool),fun('hoare$u509422987triple'(state),bool)),image(pname,'hoare$u509422987triple'(state)),hAPP(fun(pname,com),fun(pname,'hoare$u509422987triple'(state)),hAPP(fun(com,'hoare$u509422987triple'(state)),fun(fun(pname,com),fun(pname,'hoare$u509422987triple'(state))),combb(com,'hoare$u509422987triple'(state),pname),'hoare$uMirabelle$uMGT'),'body$u1')),hAPP(fun(pname,option(com)),fun(pname,bool),dom(pname,com),body))),hAPP(fun('hoare$u509422987triple'(state),bool),fun('hoare$u509422987triple'(state),bool),hAPP('hoare$u509422987triple'(state),fun(fun('hoare$u509422987triple'(state),bool),fun('hoare$u509422987triple'(state),bool)),insert('hoare$u509422987triple'(state)),hAPP(com,'hoare$u509422987triple'(state),'hoare$uMirabelle$uMGT',y)),'bot$ubot'(fun('hoare$u509422987triple'(state),bool))))) ).
fof(negated_conjecture,negated_conjecture,
~ hBOOL(hAPP(fun('hoare$u509422987triple'(state),bool),bool,hAPP(fun('hoare$u509422987triple'(state),bool),fun(fun('hoare$u509422987triple'(state),bool),bool),'hoare$u122391849derivs'(state),hAPP(fun(pname,bool),fun('hoare$u509422987triple'(state),bool),hAPP(fun(pname,'hoare$u509422987triple'(state)),fun(fun(pname,bool),fun('hoare$u509422987triple'(state),bool)),image(pname,'hoare$u509422987triple'(state)),hAPP(fun(pname,com),fun(pname,'hoare$u509422987triple'(state)),hAPP(fun(com,'hoare$u509422987triple'(state)),fun(fun(pname,com),fun(pname,'hoare$u509422987triple'(state))),combb(com,'hoare$u509422987triple'(state),pname),'hoare$uMirabelle$uMGT'),'body$u1')),hAPP(fun(pname,option(com)),fun(pname,bool),dom(pname,com),body))),hAPP(fun('hoare$u509422987triple'(state),bool),fun('hoare$u509422987triple'(state),bool),hAPP('hoare$u509422987triple'(state),fun(fun('hoare$u509422987triple'(state),bool),fun('hoare$u509422987triple'(state),bool)),insert('hoare$u509422987triple'(state)),hAPP(com,'hoare$u509422987triple'(state),'hoare$uMirabelle$uMGT',y)),'bot$ubot'(fun('hoare$u509422987triple'(state),bool))))),
inference(negate_conjecture,[status(cth)],[conj_7]) ).
cnf(c6,plain,
ti(bool,'wT$ubodies') = 'wT$ubodies',
inference(clausification,[status(esa)],[tsy_c_Com_OWT__bodies_res]) ).
cnf(c13,plain,
ti(bool,'hoare$u1883395792gleton') = 'hoare$u1883395792gleton',
inference(clausification,[status(esa)],[tsy_c_Hoare__Mirabelle__pjuwniqynr_Ostate__not__singleton_res]) ).
cnf(c31,plain,
ti(X0,hAPP(X1,X0,X2,X3)) = hAPP(X1,X0,X2,X3),
inference(clausification,[status(esa)],[tsy_c_hAPP_res]) ).
cnf(c38,plain,
hBOOL(hAPP(fun('hoare$u509422987triple'(X0),bool),bool,hAPP(fun('hoare$u509422987triple'(X0),bool),fun(fun('hoare$u509422987triple'(X0),bool),bool),'hoare$u122391849derivs'(X0),X1),'bot$ubot'(fun('hoare$u509422987triple'(X0),bool)))),
inference(clausification,[status(esa)],[fact_0_empty]) ).
cnf(c42,plain,
( hBOOL(hAPP(fun('hoare$u509422987triple'(X0),bool),bool,hAPP(fun('hoare$u509422987triple'(X0),bool),fun(fun('hoare$u509422987triple'(X0),bool),bool),'hoare$u122391849derivs'(X0),X3),X2))
| ~ hBOOL(hAPP(fun('hoare$u509422987triple'(X0),bool),bool,hAPP(fun('hoare$u509422987triple'(X0),bool),fun(fun('hoare$u509422987triple'(X0),bool),bool),'hoare$u122391849derivs'(X0),X3),X1))
| ~ hBOOL(hAPP(fun('hoare$u509422987triple'(X0),bool),bool,hAPP(fun('hoare$u509422987triple'(X0),bool),fun(fun('hoare$u509422987triple'(X0),bool),bool),'hoare$u122391849derivs'(X0),X1),X2)) ),
inference(clausification,[status(esa)],[fact_4_cut]) ).
cnf(c44,plain,
( hBOOL(hAPP(fun('hoare$u509422987triple'(X0),bool),bool,hAPP(fun('hoare$u509422987triple'(X0),bool),fun(fun('hoare$u509422987triple'(X0),bool),bool),'hoare$u122391849derivs'(X0),X1),hAPP(fun('hoare$u509422987triple'(X0),bool),fun('hoare$u509422987triple'(X0),bool),hAPP('hoare$u509422987triple'(X0),fun(fun('hoare$u509422987triple'(X0),bool),fun('hoare$u509422987triple'(X0),bool)),insert('hoare$u509422987triple'(X0)),X2),'bot$ubot'(fun('hoare$u509422987triple'(X0),bool)))))
| ~ hBOOL(hAPP(fun('hoare$u509422987triple'(X0),bool),bool,hAPP(fun('hoare$u509422987triple'(X0),bool),fun(fun('hoare$u509422987triple'(X0),bool),bool),'hoare$u122391849derivs'(X0),X1),hAPP(fun('hoare$u509422987triple'(X0),bool),fun('hoare$u509422987triple'(X0),bool),hAPP('hoare$u509422987triple'(X0),fun(fun('hoare$u509422987triple'(X0),bool),fun('hoare$u509422987triple'(X0),bool)),insert('hoare$u509422987triple'(X0)),X2),X3))) ),
inference(clausification,[status(esa)],[fact_6_derivs__insertD]) ).
cnf(c60,plain,
( hBOOL(hAPP(fun('hoare$u509422987triple'(state),bool),bool,hAPP(fun('hoare$u509422987triple'(state),bool),fun(fun('hoare$u509422987triple'(state),bool),bool),'hoare$u122391849derivs'(state),'bot$ubot'(fun('hoare$u509422987triple'(state),bool))),hAPP(fun('hoare$u509422987triple'(state),bool),fun('hoare$u509422987triple'(state),bool),hAPP('hoare$u509422987triple'(state),fun(fun('hoare$u509422987triple'(state),bool),fun('hoare$u509422987triple'(state),bool)),insert('hoare$u509422987triple'(state)),hAPP(com,'hoare$u509422987triple'(state),'hoare$uMirabelle$uMGT',X0)),'bot$ubot'(fun('hoare$u509422987triple'(state),bool)))))
| ~ hBOOL(hAPP(com,bool,wt,X0))
| ~ hBOOL('wT$ubodies')
| ~ hBOOL('hoare$u1883395792gleton') ),
inference(clausification,[status(esa)],[fact_19_MGF]) ).
cnf(c118,plain,
hAPP(fun(X0,bool),fun(X1,bool),hAPP(fun(X0,X1),fun(fun(X0,bool),fun(X1,bool)),image(X0,X1),X2),hAPP(fun(X3,bool),fun(X0,bool),hAPP(fun(X3,X0),fun(fun(X3,bool),fun(X0,bool)),image(X3,X0),X4),X5)) = hAPP(fun(X3,bool),fun(X1,bool),hAPP(fun(X3,X1),fun(fun(X3,bool),fun(X1,bool)),image(X3,X1),hAPP(fun(X3,X0),fun(X3,X1),hAPP(fun(X0,X1),fun(fun(X3,X0),fun(X3,X1)),combb(X0,X1,X3),X2),X4)),X5),
inference(clausification,[status(esa)],[fact_60_image__image]) ).
cnf(c148,plain,
hAPP(fun(X0,bool),fun(X0,bool),collect(X0),X1) = ti(fun(X0,bool),X1),
inference(clausification,[status(esa)],[fact_77_Collect__def]) ).
cnf(c168,plain,
hAPP(fun(X0,bool),fun(X0,bool),collect(X0),hAPP(X0,fun(X0,bool),fequal(X0),X1)) = hAPP(fun(X0,bool),fun(X0,bool),hAPP(X0,fun(fun(X0,bool),fun(X0,bool)),insert(X0),X1),'bot$ubot'(fun(X0,bool))),
inference(clausification,[status(esa)],[fact_90_singleton__conv2]) ).
cnf(c171,plain,
( hBOOL(hAPP(com,bool,wt,X1))
| hAPP(pname,option(com),body,X0) != hAPP(com,option(com),some(com),X1)
| ~ hBOOL('wT$ubodies') ),
inference(clausification,[status(esa)],[fact_92_WT__bodiesD]) ).
cnf(c206,plain,
~ hBOOL(fFalse),
inference(clausification,[status(esa)],[help_fFalse_1_1_U]) ).
cnf(c207,plain,
( ti(bool,X0) = fFalse
| ti(bool,X0) = fTrue ),
inference(clausification,[status(esa)],[help_fFalse_1_1_T]) ).
cnf(c213,plain,
hBOOL('hoare$u1883395792gleton'),
inference(clausification,[status(esa)],[conj_0]) ).
cnf(c214,plain,
hBOOL('wT$ubodies'),
inference(clausification,[status(esa)],[conj_1]) ).
cnf(c218,plain,
hAPP(pname,option(com),body,pn) = hAPP(com,option(com),some(com),y),
inference(clausification,[status(esa)],[conj_5]) ).
cnf(c220,plain,
~ hBOOL(hAPP(fun('hoare$u509422987triple'(state),bool),bool,hAPP(fun('hoare$u509422987triple'(state),bool),fun(fun('hoare$u509422987triple'(state),bool),bool),'hoare$u122391849derivs'(state),hAPP(fun(pname,bool),fun('hoare$u509422987triple'(state),bool),hAPP(fun(pname,'hoare$u509422987triple'(state)),fun(fun(pname,bool),fun('hoare$u509422987triple'(state),bool)),image(pname,'hoare$u509422987triple'(state)),hAPP(fun(pname,com),fun(pname,'hoare$u509422987triple'(state)),hAPP(fun(com,'hoare$u509422987triple'(state)),fun(fun(pname,com),fun(pname,'hoare$u509422987triple'(state))),combb(com,'hoare$u509422987triple'(state),pname),'hoare$uMirabelle$uMGT'),'body$u1')),hAPP(fun(pname,option(com)),fun(pname,bool),dom(pname,com),body))),hAPP(fun('hoare$u509422987triple'(state),bool),fun('hoare$u509422987triple'(state),bool),hAPP('hoare$u509422987triple'(state),fun(fun('hoare$u509422987triple'(state),bool),fun('hoare$u509422987triple'(state),bool)),insert('hoare$u509422987triple'(state)),hAPP(com,'hoare$u509422987triple'(state),'hoare$uMirabelle$uMGT',y)),'bot$ubot'(fun('hoare$u509422987triple'(state),bool))))),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(d0,plain,
( ti(bool,'wT$ubodies') = fFalse
| fTrue = 'wT$ubodies' ),
inference(superposition,[status(thm)],[c207,c6]) ).
cnf(d1,plain,
( fTrue = 'wT$ubodies'
| 'wT$ubodies' = fFalse ),
inference(demodulation,[status(thm)],[d0,c6]) ).
cnf(d2,plain,
( ti(bool,'hoare$u1883395792gleton') = fFalse
| fTrue = 'hoare$u1883395792gleton' ),
inference(superposition,[status(thm)],[c207,c13]) ).
cnf(d3,plain,
( fTrue = 'hoare$u1883395792gleton'
| 'hoare$u1883395792gleton' = fFalse ),
inference(demodulation,[status(thm)],[d2,c13]) ).
cnf(d4,plain,
( 'hoare$u1883395792gleton' = fFalse
| 'wT$ubodies' = fFalse
| 'hoare$u1883395792gleton' = 'wT$ubodies' ),
inference(superposition,[status(thm)],[d3,d1]) ).
cnf(d5,plain,
( 'hoare$u1883395792gleton' = fFalse
| 'hoare$u1883395792gleton' = 'wT$ubodies'
| ~ hBOOL('wT$ubodies') ),
inference(superposition,[status(thm)],[d4,c206]) ).
cnf(d6,plain,
( 'hoare$u1883395792gleton' = fFalse
| 'hoare$u1883395792gleton' = 'wT$ubodies' ),
inference(resolution,[status(thm)],[c214,d5]) ).
cnf(d7,plain,
( 'hoare$u1883395792gleton' = 'wT$ubodies'
| ~ hBOOL('hoare$u1883395792gleton') ),
inference(superposition,[status(thm)],[d6,c206]) ).
cnf(d8,plain,
'hoare$u1883395792gleton' = 'wT$ubodies',
inference(resolution,[status(thm)],[c213,d7]) ).
cnf(d9,plain,
( hBOOL(hAPP(com,bool,wt,X1))
| ~ hBOOL('hoare$u1883395792gleton')
| hAPP(pname,option(com),body,X0) != hAPP(com,option(com),some(com),X1) ),
inference(demodulation,[status(thm)],[c171,d8]) ).
cnf(d10,plain,
( hBOOL(hAPP(com,bool,wt,X1))
| hAPP(pname,option(com),body,X0) != hAPP(com,option(com),some(com),X1) ),
inference(resolution,[status(thm)],[c213,d9]) ).
cnf(d11,plain,
( hBOOL(hAPP(com,bool,wt,y))
| hAPP(pname,option(com),body,X0) != hAPP(pname,option(com),body,pn) ),
inference(superposition,[status(thm)],[c218,d10]) ).
cnf(d12,plain,
ti(fun(X0,bool),hAPP(X0,fun(X0,bool),fequal(X0),X1)) = hAPP(fun(X0,bool),fun(X0,bool),hAPP(X0,fun(fun(X0,bool),fun(X0,bool)),insert(X0),X1),'bot$ubot'(fun(X0,bool))),
inference(demodulation,[status(thm)],[c168,c148]) ).
cnf(d13,plain,
hAPP(X0,fun(X0,bool),fequal(X0),X1) = hAPP(fun(X0,bool),fun(X0,bool),hAPP(X0,fun(fun(X0,bool),fun(X0,bool)),insert(X0),X1),'bot$ubot'(fun(X0,bool))),
inference(demodulation,[status(thm)],[d12,c31]) ).
cnf(d14,plain,
~ hBOOL(hAPP(fun('hoare$u509422987triple'(state),bool),bool,hAPP(fun('hoare$u509422987triple'(state),bool),fun(fun('hoare$u509422987triple'(state),bool),bool),'hoare$u122391849derivs'(state),hAPP(fun(com,bool),fun('hoare$u509422987triple'(state),bool),hAPP(fun(com,'hoare$u509422987triple'(state)),fun(fun(com,bool),fun('hoare$u509422987triple'(state),bool)),image(com,'hoare$u509422987triple'(state)),'hoare$uMirabelle$uMGT'),hAPP(fun(pname,bool),fun(com,bool),hAPP(fun(pname,com),fun(fun(pname,bool),fun(com,bool)),image(pname,com),'body$u1'),hAPP(fun(pname,option(com)),fun(pname,bool),dom(pname,com),body)))),hAPP(fun('hoare$u509422987triple'(state),bool),fun('hoare$u509422987triple'(state),bool),hAPP('hoare$u509422987triple'(state),fun(fun('hoare$u509422987triple'(state),bool),fun('hoare$u509422987triple'(state),bool)),insert('hoare$u509422987triple'(state)),hAPP(com,'hoare$u509422987triple'(state),'hoare$uMirabelle$uMGT',y)),'bot$ubot'(fun('hoare$u509422987triple'(state),bool))))),
inference(demodulation,[status(thm)],[c220,c118]) ).
cnf(d15,plain,
~ hBOOL(hAPP(fun('hoare$u509422987triple'(state),bool),bool,hAPP(fun('hoare$u509422987triple'(state),bool),fun(fun('hoare$u509422987triple'(state),bool),bool),'hoare$u122391849derivs'(state),hAPP(fun(com,bool),fun('hoare$u509422987triple'(state),bool),hAPP(fun(com,'hoare$u509422987triple'(state)),fun(fun(com,bool),fun('hoare$u509422987triple'(state),bool)),image(com,'hoare$u509422987triple'(state)),'hoare$uMirabelle$uMGT'),hAPP(fun(pname,bool),fun(com,bool),hAPP(fun(pname,com),fun(fun(pname,bool),fun(com,bool)),image(pname,com),'body$u1'),hAPP(fun(pname,option(com)),fun(pname,bool),dom(pname,com),body)))),hAPP('hoare$u509422987triple'(state),fun('hoare$u509422987triple'(state),bool),fequal('hoare$u509422987triple'(state)),hAPP(com,'hoare$u509422987triple'(state),'hoare$uMirabelle$uMGT',y)))),
inference(demodulation,[status(thm)],[d14,d13]) ).
cnf(d16,plain,
( hBOOL(hAPP(fun('hoare$u509422987triple'(X0),bool),bool,hAPP(fun('hoare$u509422987triple'(X0),bool),fun(fun('hoare$u509422987triple'(X0),bool),bool),'hoare$u122391849derivs'(X0),X2),X1))
| ~ hBOOL(hAPP(fun('hoare$u509422987triple'(X0),bool),bool,hAPP(fun('hoare$u509422987triple'(X0),bool),fun(fun('hoare$u509422987triple'(X0),bool),bool),'hoare$u122391849derivs'(X0),'bot$ubot'(fun('hoare$u509422987triple'(X0),bool))),X1)) ),
inference(resolution,[status(thm)],[c42,c38]) ).
cnf(d17,plain,
( ~ hBOOL(hAPP(com,bool,wt,X0))
| hBOOL(hAPP(fun('hoare$u509422987triple'(state),bool),bool,hAPP(fun('hoare$u509422987triple'(state),bool),fun(fun('hoare$u509422987triple'(state),bool),bool),'hoare$u122391849derivs'(state),'bot$ubot'(fun('hoare$u509422987triple'(state),bool))),hAPP(fun('hoare$u509422987triple'(state),bool),fun('hoare$u509422987triple'(state),bool),hAPP('hoare$u509422987triple'(state),fun(fun('hoare$u509422987triple'(state),bool),fun('hoare$u509422987triple'(state),bool)),insert('hoare$u509422987triple'(state)),hAPP(com,'hoare$u509422987triple'(state),'hoare$uMirabelle$uMGT',X0)),'bot$ubot'(fun('hoare$u509422987triple'(state),bool)))))
| ~ hBOOL('wT$ubodies') ),
inference(resolution,[status(thm)],[c213,c60]) ).
cnf(d18,plain,
( ~ hBOOL(hAPP(com,bool,wt,X0))
| hBOOL(hAPP(fun('hoare$u509422987triple'(state),bool),bool,hAPP(fun('hoare$u509422987triple'(state),bool),fun(fun('hoare$u509422987triple'(state),bool),bool),'hoare$u122391849derivs'(state),'bot$ubot'(fun('hoare$u509422987triple'(state),bool))),hAPP(fun('hoare$u509422987triple'(state),bool),fun('hoare$u509422987triple'(state),bool),hAPP('hoare$u509422987triple'(state),fun(fun('hoare$u509422987triple'(state),bool),fun('hoare$u509422987triple'(state),bool)),insert('hoare$u509422987triple'(state)),hAPP(com,'hoare$u509422987triple'(state),'hoare$uMirabelle$uMGT',X0)),'bot$ubot'(fun('hoare$u509422987triple'(state),bool))))) ),
inference(resolution,[status(thm)],[c214,d17]) ).
cnf(d19,plain,
( hBOOL(hAPP(fun('hoare$u509422987triple'(state),bool),bool,hAPP(fun('hoare$u509422987triple'(state),bool),fun(fun('hoare$u509422987triple'(state),bool),bool),'hoare$u122391849derivs'(state),'bot$ubot'(fun('hoare$u509422987triple'(state),bool))),hAPP(fun('hoare$u509422987triple'(state),bool),fun('hoare$u509422987triple'(state),bool),hAPP('hoare$u509422987triple'(state),fun(fun('hoare$u509422987triple'(state),bool),fun('hoare$u509422987triple'(state),bool)),insert('hoare$u509422987triple'(state)),hAPP(com,'hoare$u509422987triple'(state),'hoare$uMirabelle$uMGT',X0)),'bot$ubot'(fun('hoare$u509422987triple'(state),bool)))))
| ~ hBOOL(hAPP(com,bool,wt,X0)) ),
inference(resolution,[status(thm)],[d18,c44]) ).
cnf(d20,plain,
( ~ hBOOL(hAPP(com,bool,wt,X0))
| hBOOL(hAPP(fun('hoare$u509422987triple'(state),bool),bool,hAPP(fun('hoare$u509422987triple'(state),bool),fun(fun('hoare$u509422987triple'(state),bool),bool),'hoare$u122391849derivs'(state),'bot$ubot'(fun('hoare$u509422987triple'(state),bool))),hAPP('hoare$u509422987triple'(state),fun('hoare$u509422987triple'(state),bool),fequal('hoare$u509422987triple'(state)),hAPP(com,'hoare$u509422987triple'(state),'hoare$uMirabelle$uMGT',X0)))) ),
inference(demodulation,[status(thm)],[d19,d13]) ).
cnf(d21,plain,
( hBOOL(hAPP(fun('hoare$u509422987triple'(state),bool),bool,hAPP(fun('hoare$u509422987triple'(state),bool),fun(fun('hoare$u509422987triple'(state),bool),bool),'hoare$u122391849derivs'(state),X1),hAPP('hoare$u509422987triple'(state),fun('hoare$u509422987triple'(state),bool),fequal('hoare$u509422987triple'(state)),hAPP(com,'hoare$u509422987triple'(state),'hoare$uMirabelle$uMGT',X0))))
| ~ hBOOL(hAPP(com,bool,wt,X0)) ),
inference(resolution,[status(thm)],[d20,d16]) ).
cnf(d22,plain,
~ hBOOL(hAPP(com,bool,wt,y)),
inference(resolution,[status(thm)],[d21,d15]) ).
cnf(d23,plain,
hAPP(pname,option(com),body,X0) != hAPP(pname,option(com),body,pn),
inference(resolution,[status(thm)],[d22,d11]) ).
cnf(d24,plain,
$false,
inference(equality_resolution,[status(thm)],[d23]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWW474+5 : TPTP v9.3.1. Released v5.3.0.
% 0.00/0.04 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n014.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Sat Sep 26 16:02:48 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.36 Running casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 44.07/21.05 % SZS status Theorem for theBenchmark.p
% 44.07/21.05 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
%------------------------------------------------------------------------------