%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : SWW470+2 : TPTP v9.3.1. Released v5.3.0.
% Transfm : none
% Format : tptp:raw
% Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n010.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:55 AM UTC 2026
% Result : Theorem 37.19s 6.21s
% Output : CNFRefutation 37.19s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 17
% Syntax : Number of formulae : 58 ( 34 unt; 0 def)
% Number of atoms : 88 ( 30 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 49 ( 19 ~; 19 |; 0 &)
% ( 4 <=>; 7 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 2 avg)
% Maximal term depth : 11 ( 2 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-2 aty)
% Number of functors : 58 ( 58 usr; 26 con; 0-3 aty)
% Number of variables : 83 ( 26 sgn 28 !; 1 ?)
% Comments :
%------------------------------------------------------------------------------
fof(gsy_c_Orderings_Obot__class_Obot_000tc__HOL__Obool,axiom,
'is$ubool'('bot$ubot$ubool') ).
fof(gsy_c_fFalse,hypothesis,
'is$ubool'(fFalse) ).
fof(fact_8_constant,axiom,
! [X0,X1,X2,X3,X4] :
( ( hBOOL(X4)
=> hBOOL('hAPP$uf540970102l$ubool'('hoare$u606018542rivs$ua'(X0),'hAPP$uf1591852335a$ubool'('hAPP$uH1641355846a$ubool'('insert873085594iple$ua','hoare$u1760757500iple$ua'(X1,X2,X3)),'bot$ubo1181479936a$ubool'))) )
=> hBOOL('hAPP$uf540970102l$ubool'('hoare$u606018542rivs$ua'(X0),'hAPP$uf1591852335a$ubool'('hAPP$uH1641355846a$ubool'('insert873085594iple$ua','hoare$u1760757500iple$ua'('hAPP$ub540892988e$ubool'('hAPP$uf1824947087e$ubool'('cOMBC$u41962815e$ubool','hAPP$uf340725611e$ubool'('hAPP$uf1006724181e$ubool'('cOMBB$u1348041619bool$ua','cOMBC$u231445413l$ubool'),'hAPP$uf1509969235l$ubool'('hAPP$uf1178339559l$ubool'('cOMBB$u1355796797bool$ua','hAPP$uf1561913689l$ubool'('cOMBB$u188601460$ustate',fconj)),X1))),X4),X2,X3)),'bot$ubo1181479936a$ubool'))) ) ).
fof(fact_14_conseq1,axiom,
! [X0,X1,X2,X3,X4] :
( hBOOL('hAPP$uf540970102l$ubool'('hoare$u606018542rivs$ua'(X1),'hAPP$uf1591852335a$ubool'('hAPP$uH1641355846a$ubool'('insert873085594iple$ua','hoare$u1760757500iple$ua'(X2,X3,X4)),'bot$ubo1181479936a$ubool')))
=> ( ! [X5,X6] :
( hBOOL('hAPP$ustate$ubool'('hAPP$ua2036067514e$ubool'(X0,X5),X6))
=> hBOOL('hAPP$ustate$ubool'('hAPP$ua2036067514e$ubool'(X2,X5),X6)) )
=> hBOOL('hAPP$uf540970102l$ubool'('hoare$u606018542rivs$ua'(X1),'hAPP$uf1591852335a$ubool'('hAPP$uH1641355846a$ubool'('insert873085594iple$ua','hoare$u1760757500iple$ua'(X0,X3,X4)),'bot$ubo1181479936a$ubool'))) ) ) ).
fof(fact_24_emptyE,axiom,
! [X0] : ~ hBOOL('hAPP$uf540970102l$ubool'('hAPP$uH1840393229l$ubool'('member1713797107iple$ua',X0),'bot$ubo1181479936a$ubool')) ).
fof(fact_27_singleton__conv2,axiom,
! [X0] : 'collec268032053iple$ua'('hAPP$uH1190454433a$ubool'('fequal879838495iple$ua',X0)) = 'hAPP$uf1591852335a$ubool'('hAPP$uH1641355846a$ubool'('insert873085594iple$ua',X0),'bot$ubo1181479936a$ubool') ).
fof(fact_46_Collect__empty__eq,axiom,
! [X0] :
( 'collect$unat'(X0) = 'bot$ubot$ufun$unat$ubool'
<=> ! [X1] : ~ hBOOL('hAPP$unat$ubool'(X0,X1)) ) ).
fof(fact_59_ex__in__conv,axiom,
! [X0] :
( ? [X1] : hBOOL('hAPP$uf54304608l$ubool'('hAPP$un215258509l$ubool'('member$unat',X1),X0))
<=> X0 != 'bot$ubot$ufun$unat$ubool' ) ).
fof(fact_63_empty__def,axiom,
'bot$ubot$ufun$unat$ubool' = 'collect$unat'('hAPP$ub1013836512t$ubool'('cOMBK$ubool$unat',fFalse)) ).
fof(fact_125_bot__apply,axiom,
! [X0] :
( hBOOL('hAPP$unat$ubool'('bot$ubot$ufun$unat$ubool',X0))
<=> hBOOL('bot$ubot$ubool') ) ).
fof(fact_231_mem__def,axiom,
! [X0,X1] :
( hBOOL('hAPP$uf54304608l$ubool'('hAPP$un215258509l$ubool'('member$unat',X0),X1))
<=> hBOOL('hAPP$unat$ubool'(X1,X0)) ) ).
fof(fact_232_Collect__def,axiom,
! [X0] : 'collec268032053iple$ua'(X0) = X0 ).
fof(fact_233_Collect__def,axiom,
! [X0] : 'collect$unat'(X0) = X0 ).
fof(help_COMBK_1_1_COMBK_000tc__HOL__Obool_000tc__Nat__Onat_U,axiom,
! [X0,X1] :
( 'is$ubool'(X0)
=> 'hAPP$unat$ubool'('hAPP$ub1013836512t$ubool'('cOMBK$ubool$unat',X0),X1) = X0 ) ).
fof(help_COMBK_1_1_COMBK_000tc__HOL__Obool_000tc__Com__Ostate_U,axiom,
! [X0,X1] :
( 'is$ubool'(X0)
=> 'hAPP$ustate$ubool'('hAPP$ub2019457360e$ubool'('cOMBK$ubool$ustate',X0),X1) = X0 ) ).
fof(help_COMBK_1_1_COMBK_000tc__fun_Itc__Com__Ostate_Mtc__HOL__Obool_J_000t__a_U,axiom,
! [X0,X1] : 'hAPP$ua2036067514e$ubool'('hAPP$uf762886889e$ubool'('cOMBK$u1458035955bool$ua',X0),X1) = X0 ).
fof(conj_0,conjecture,
hBOOL('hAPP$uf540970102l$ubool'('hoare$u606018542rivs$ua'(g),'hAPP$uf1591852335a$ubool'('hAPP$uH1641355846a$ubool'('insert873085594iple$ua','hoare$u1760757500iple$ua'('hAPP$uf762886889e$ubool'('cOMBK$u1458035955bool$ua','hAPP$ub2019457360e$ubool'('cOMBK$ubool$ustate',fFalse)),c,'hAPP$uf762886889e$ubool'('hAPP$uf1261923407e$ubool'('cOMBC$u892787026e$ubool','hAPP$uf963367678e$ubool'('hAPP$uf375255701e$ubool'('cOMBB$u145932198bool$ua','cOMBS$u1378840469l$ubool'),'hAPP$uf1509969235l$ubool'('hAPP$uf1178339559l$ubool'('cOMBB$u1355796797bool$ua','hAPP$uf1561913689l$ubool'('cOMBB$u188601460$ustate',fconj)),p))),'hAPP$uf1759915619e$ubool'('hAPP$uf2073279419e$ubool'('cOMBB$u160679318$ustate',fNot),b)))),'bot$ubo1181479936a$ubool'))) ).
fof(negated_conjecture,negated_conjecture,
~ hBOOL('hAPP$uf540970102l$ubool'('hoare$u606018542rivs$ua'(g),'hAPP$uf1591852335a$ubool'('hAPP$uH1641355846a$ubool'('insert873085594iple$ua','hoare$u1760757500iple$ua'('hAPP$uf762886889e$ubool'('cOMBK$u1458035955bool$ua','hAPP$ub2019457360e$ubool'('cOMBK$ubool$ustate',fFalse)),c,'hAPP$uf762886889e$ubool'('hAPP$uf1261923407e$ubool'('cOMBC$u892787026e$ubool','hAPP$uf963367678e$ubool'('hAPP$uf375255701e$ubool'('cOMBB$u145932198bool$ua','cOMBS$u1378840469l$ubool'),'hAPP$uf1509969235l$ubool'('hAPP$uf1178339559l$ubool'('cOMBB$u1355796797bool$ua','hAPP$uf1561913689l$ubool'('cOMBB$u188601460$ustate',fconj)),p))),'hAPP$uf1759915619e$ubool'('hAPP$uf2073279419e$ubool'('cOMBB$u160679318$ustate',fNot),b)))),'bot$ubo1181479936a$ubool'))),
inference(negate_conjecture,[status(cth)],[conj_0]) ).
cnf(c16,plain,
'is$ubool'('bot$ubot$ubool'),
inference(clausification,[status(esa)],[gsy_c_Orderings_Obot__class_Obot_000tc__HOL__Obool]) ).
cnf(c17,plain,
'is$ubool'(fFalse),
inference(clausification,[status(esa)],[gsy_c_fFalse]) ).
cnf(c42,plain,
( hBOOL('hAPP$uf540970102l$ubool'('hoare$u606018542rivs$ua'(X1),'hAPP$uf1591852335a$ubool'('hAPP$uH1641355846a$ubool'('insert873085594iple$ua','hoare$u1760757500iple$ua'('hAPP$ub540892988e$ubool'('hAPP$uf1824947087e$ubool'('cOMBC$u41962815e$ubool','hAPP$uf340725611e$ubool'('hAPP$uf1006724181e$ubool'('cOMBB$u1348041619bool$ua','cOMBC$u231445413l$ubool'),'hAPP$uf1509969235l$ubool'('hAPP$uf1178339559l$ubool'('cOMBB$u1355796797bool$ua','hAPP$uf1561913689l$ubool'('cOMBB$u188601460$ustate',fconj)),X2))),X0),X3,X4)),'bot$ubo1181479936a$ubool')))
| hBOOL(X0) ),
inference(clausification,[status(esa)],[fact_8_constant]) ).
cnf(c54,plain,
( hBOOL('hAPP$uf540970102l$ubool'('hoare$u606018542rivs$ua'(X0),'hAPP$uf1591852335a$ubool'('hAPP$uH1641355846a$ubool'('insert873085594iple$ua','hoare$u1760757500iple$ua'(X4,X2,X3)),'bot$ubo1181479936a$ubool')))
| hBOOL('hAPP$ustate$ubool'('hAPP$ua2036067514e$ubool'(X4,sK109(X4,X1)),sK110(X4,X1)))
| ~ hBOOL('hAPP$uf540970102l$ubool'('hoare$u606018542rivs$ua'(X0),'hAPP$uf1591852335a$ubool'('hAPP$uH1641355846a$ubool'('insert873085594iple$ua','hoare$u1760757500iple$ua'(X1,X2,X3)),'bot$ubo1181479936a$ubool'))) ),
inference(clausification,[status(esa)],[fact_14_conseq1]) ).
cnf(c73,plain,
~ hBOOL('hAPP$uf540970102l$ubool'('hAPP$uH1840393229l$ubool'('member1713797107iple$ua',X0),'bot$ubo1181479936a$ubool')),
inference(clausification,[status(esa)],[fact_24_emptyE]) ).
cnf(c76,plain,
'collec268032053iple$ua'('hAPP$uH1190454433a$ubool'('fequal879838495iple$ua',X0)) = 'hAPP$uf1591852335a$ubool'('hAPP$uH1641355846a$ubool'('insert873085594iple$ua',X0),'bot$ubo1181479936a$ubool'),
inference(clausification,[status(esa)],[fact_27_singleton__conv2]) ).
cnf(c103,plain,
( ~ hBOOL('hAPP$unat$ubool'(X0,X1))
| 'collect$unat'(X0) != 'bot$ubot$ufun$unat$ubool' ),
inference(clausification,[status(esa)],[fact_46_Collect__empty__eq]) ).
cnf(c127,plain,
( X0 = 'bot$ubot$ufun$unat$ubool'
| hBOOL('hAPP$uf54304608l$ubool'('hAPP$un215258509l$ubool'('member$unat',sK224(X0)),X0)) ),
inference(clausification,[status(esa)],[fact_59_ex__in__conv]) ).
cnf(c134,plain,
'bot$ubot$ufun$unat$ubool' = 'collect$unat'('hAPP$ub1013836512t$ubool'('cOMBK$ubool$unat',fFalse)),
inference(clausification,[status(esa)],[fact_63_empty__def]) ).
cnf(c237,plain,
( ~ hBOOL('bot$ubot$ubool')
| hBOOL('hAPP$unat$ubool'('bot$ubot$ufun$unat$ubool',X0)) ),
inference(clausification,[status(esa)],[fact_125_bot__apply]) ).
cnf(c400,plain,
( hBOOL('hAPP$unat$ubool'(X1,X0))
| ~ hBOOL('hAPP$uf54304608l$ubool'('hAPP$un215258509l$ubool'('member$unat',X0),X1)) ),
inference(clausification,[status(esa)],[fact_231_mem__def]) ).
cnf(c402,plain,
'collec268032053iple$ua'(X0) = X0,
inference(clausification,[status(esa)],[fact_232_Collect__def]) ).
cnf(c403,plain,
'collect$unat'(X0) = X0,
inference(clausification,[status(esa)],[fact_233_Collect__def]) ).
cnf(c1181,plain,
( 'hAPP$unat$ubool'('hAPP$ub1013836512t$ubool'('cOMBK$ubool$unat',X0),X1) = X0
| ~ 'is$ubool'(X0) ),
inference(clausification,[status(esa)],[help_COMBK_1_1_COMBK_000tc__HOL__Obool_000tc__Nat__Onat_U]) ).
cnf(c1182,plain,
( 'hAPP$ustate$ubool'('hAPP$ub2019457360e$ubool'('cOMBK$ubool$ustate',X0),X1) = X0
| ~ 'is$ubool'(X0) ),
inference(clausification,[status(esa)],[help_COMBK_1_1_COMBK_000tc__HOL__Obool_000tc__Com__Ostate_U]) ).
cnf(c1188,plain,
'hAPP$ua2036067514e$ubool'('hAPP$uf762886889e$ubool'('cOMBK$u1458035955bool$ua',X0),X1) = X0,
inference(clausification,[status(esa)],[help_COMBK_1_1_COMBK_000tc__fun_Itc__Com__Ostate_Mtc__HOL__Obool_J_000t__a_U]) ).
cnf(c1263,plain,
~ hBOOL('hAPP$uf540970102l$ubool'('hoare$u606018542rivs$ua'(g),'hAPP$uf1591852335a$ubool'('hAPP$uH1641355846a$ubool'('insert873085594iple$ua','hoare$u1760757500iple$ua'('hAPP$uf762886889e$ubool'('cOMBK$u1458035955bool$ua','hAPP$ub2019457360e$ubool'('cOMBK$ubool$ustate',fFalse)),c,'hAPP$uf762886889e$ubool'('hAPP$uf1261923407e$ubool'('cOMBC$u892787026e$ubool','hAPP$uf963367678e$ubool'('hAPP$uf375255701e$ubool'('cOMBB$u145932198bool$ua','cOMBS$u1378840469l$ubool'),'hAPP$uf1509969235l$ubool'('hAPP$uf1178339559l$ubool'('cOMBB$u1355796797bool$ua','hAPP$uf1561913689l$ubool'('cOMBB$u188601460$ustate',fconj)),p))),'hAPP$uf1759915619e$ubool'('hAPP$uf2073279419e$ubool'('cOMBB$u160679318$ustate',fNot),b)))),'bot$ubo1181479936a$ubool'))),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(d0,plain,
'hAPP$ustate$ubool'('hAPP$ub2019457360e$ubool'('cOMBK$ubool$ustate','bot$ubot$ubool'),X0) = 'bot$ubot$ubool',
inference(resolution,[status(thm)],[c1182,c16]) ).
cnf(d1,plain,
( X0 = 'bot$ubot$ufun$unat$ubool'
| hBOOL('hAPP$unat$ubool'(X0,sK224(X0))) ),
inference(resolution,[status(thm)],[c400,c127]) ).
cnf(d2,plain,
'hAPP$unat$ubool'('hAPP$ub1013836512t$ubool'('cOMBK$ubool$unat','bot$ubot$ubool'),X0) = 'bot$ubot$ubool',
inference(resolution,[status(thm)],[c1181,c16]) ).
cnf(d3,plain,
( 'hAPP$ub1013836512t$ubool'('cOMBK$ubool$unat','bot$ubot$ubool') = 'bot$ubot$ufun$unat$ubool'
| hBOOL('bot$ubot$ubool') ),
inference(superposition,[status(thm)],[d2,d1]) ).
cnf(d4,plain,
( ~ hBOOL('hAPP$unat$ubool'(X0,X1))
| X0 != 'bot$ubot$ufun$unat$ubool' ),
inference(demodulation,[status(thm)],[c103,c403]) ).
cnf(d5,plain,
~ hBOOL('hAPP$unat$ubool'('bot$ubot$ufun$unat$ubool',X0)),
inference(equality_resolution,[status(thm)],[d4]) ).
cnf(d6,plain,
~ hBOOL('bot$ubot$ubool'),
inference(resolution,[status(thm)],[d5,c237]) ).
cnf(d7,plain,
'hAPP$ub1013836512t$ubool'('cOMBK$ubool$unat','bot$ubot$ubool') = 'bot$ubot$ufun$unat$ubool',
inference(resolution,[status(thm)],[d6,d3]) ).
cnf(d8,plain,
'hAPP$unat$ubool'('bot$ubot$ufun$unat$ubool',X0) = 'bot$ubot$ubool',
inference(demodulation,[status(thm)],[d2,d7]) ).
cnf(d9,plain,
'bot$ubot$ufun$unat$ubool' = 'hAPP$ub1013836512t$ubool'('cOMBK$ubool$unat',fFalse),
inference(demodulation,[status(thm)],[c134,c403]) ).
cnf(d10,plain,
'hAPP$unat$ubool'('hAPP$ub1013836512t$ubool'('cOMBK$ubool$unat',fFalse),X0) = fFalse,
inference(resolution,[status(thm)],[c1181,c17]) ).
cnf(d11,plain,
'hAPP$unat$ubool'('bot$ubot$ufun$unat$ubool',X0) = fFalse,
inference(demodulation,[status(thm)],[d10,d9]) ).
cnf(d12,plain,
'bot$ubot$ubool' = fFalse,
inference(demodulation,[status(thm)],[d11,d8]) ).
cnf(d13,plain,
'hAPP$uH1190454433a$ubool'('fequal879838495iple$ua',X0) = 'hAPP$uf1591852335a$ubool'('hAPP$uH1641355846a$ubool'('insert873085594iple$ua',X0),'bot$ubo1181479936a$ubool'),
inference(demodulation,[status(thm)],[c76,c402]) ).
cnf(d14,plain,
~ hBOOL('hAPP$uf540970102l$ubool'('hoare$u606018542rivs$ua'(g),'hAPP$uH1190454433a$ubool'('fequal879838495iple$ua','hoare$u1760757500iple$ua'('hAPP$uf762886889e$ubool'('cOMBK$u1458035955bool$ua','hAPP$ub2019457360e$ubool'('cOMBK$ubool$ustate',fFalse)),c,'hAPP$uf762886889e$ubool'('hAPP$uf1261923407e$ubool'('cOMBC$u892787026e$ubool','hAPP$uf963367678e$ubool'('hAPP$uf375255701e$ubool'('cOMBB$u145932198bool$ua','cOMBS$u1378840469l$ubool'),'hAPP$uf1509969235l$ubool'('hAPP$uf1178339559l$ubool'('cOMBB$u1355796797bool$ua','hAPP$uf1561913689l$ubool'('cOMBB$u188601460$ustate',fconj)),p))),'hAPP$uf1759915619e$ubool'('hAPP$uf2073279419e$ubool'('cOMBB$u160679318$ustate',fNot),b)))))),
inference(demodulation,[status(thm)],[c1263,d13]) ).
cnf(d15,plain,
~ hBOOL('hAPP$uf540970102l$ubool'('hoare$u606018542rivs$ua'(g),'hAPP$uH1190454433a$ubool'('fequal879838495iple$ua','hoare$u1760757500iple$ua'('hAPP$uf762886889e$ubool'('cOMBK$u1458035955bool$ua','hAPP$ub2019457360e$ubool'('cOMBK$ubool$ustate','bot$ubot$ubool')),c,'hAPP$uf762886889e$ubool'('hAPP$uf1261923407e$ubool'('cOMBC$u892787026e$ubool','hAPP$uf963367678e$ubool'('hAPP$uf375255701e$ubool'('cOMBB$u145932198bool$ua','cOMBS$u1378840469l$ubool'),'hAPP$uf1509969235l$ubool'('hAPP$uf1178339559l$ubool'('cOMBB$u1355796797bool$ua','hAPP$uf1561913689l$ubool'('cOMBB$u188601460$ustate',fconj)),p))),'hAPP$uf1759915619e$ubool'('hAPP$uf2073279419e$ubool'('cOMBB$u160679318$ustate',fNot),b)))))),
inference(demodulation,[status(thm)],[d14,d12]) ).
cnf(d16,plain,
( hBOOL(X2)
| hBOOL('hAPP$uf540970102l$ubool'('hoare$u606018542rivs$ua'(X3),'hAPP$uf1591852335a$ubool'('hAPP$uH1641355846a$ubool'('insert873085594iple$ua','hoare$u1760757500iple$ua'(X0,X4,X5)),'bot$ubo1181479936a$ubool')))
| hBOOL('hAPP$ustate$ubool'('hAPP$ua2036067514e$ubool'(X0,sK109(X0,'hAPP$ub540892988e$ubool'('hAPP$uf1824947087e$ubool'('cOMBC$u41962815e$ubool','hAPP$uf340725611e$ubool'('hAPP$uf1006724181e$ubool'('cOMBB$u1348041619bool$ua','cOMBC$u231445413l$ubool'),'hAPP$uf1509969235l$ubool'('hAPP$uf1178339559l$ubool'('cOMBB$u1355796797bool$ua','hAPP$uf1561913689l$ubool'('cOMBB$u188601460$ustate',fconj)),X1))),X2))),sK110(X0,'hAPP$ub540892988e$ubool'('hAPP$uf1824947087e$ubool'('cOMBC$u41962815e$ubool','hAPP$uf340725611e$ubool'('hAPP$uf1006724181e$ubool'('cOMBB$u1348041619bool$ua','cOMBC$u231445413l$ubool'),'hAPP$uf1509969235l$ubool'('hAPP$uf1178339559l$ubool'('cOMBB$u1355796797bool$ua','hAPP$uf1561913689l$ubool'('cOMBB$u188601460$ustate',fconj)),X1))),X2)))) ),
inference(resolution,[status(thm)],[c54,c42]) ).
cnf(d17,plain,
( hBOOL('hAPP$uf540970102l$ubool'('hoare$u606018542rivs$ua'(X5),'hAPP$uH1190454433a$ubool'('fequal879838495iple$ua','hoare$u1760757500iple$ua'(X0,X1,X2))))
| hBOOL('hAPP$ustate$ubool'('hAPP$ua2036067514e$ubool'(X0,sK109(X0,'hAPP$ub540892988e$ubool'('hAPP$uf1824947087e$ubool'('cOMBC$u41962815e$ubool','hAPP$uf340725611e$ubool'('hAPP$uf1006724181e$ubool'('cOMBB$u1348041619bool$ua','cOMBC$u231445413l$ubool'),'hAPP$uf1509969235l$ubool'('hAPP$uf1178339559l$ubool'('cOMBB$u1355796797bool$ua','hAPP$uf1561913689l$ubool'('cOMBB$u188601460$ustate',fconj)),X4))),X3))),sK110(X0,'hAPP$ub540892988e$ubool'('hAPP$uf1824947087e$ubool'('cOMBC$u41962815e$ubool','hAPP$uf340725611e$ubool'('hAPP$uf1006724181e$ubool'('cOMBB$u1348041619bool$ua','cOMBC$u231445413l$ubool'),'hAPP$uf1509969235l$ubool'('hAPP$uf1178339559l$ubool'('cOMBB$u1355796797bool$ua','hAPP$uf1561913689l$ubool'('cOMBB$u188601460$ustate',fconj)),X4))),X3))))
| hBOOL(X3) ),
inference(demodulation,[status(thm)],[d16,d13]) ).
cnf(d18,plain,
( hBOOL('hAPP$ustate$ubool'('hAPP$ua2036067514e$ubool'('hAPP$uf762886889e$ubool'('cOMBK$u1458035955bool$ua','hAPP$ub2019457360e$ubool'('cOMBK$ubool$ustate','bot$ubot$ubool')),sK109('hAPP$uf762886889e$ubool'('cOMBK$u1458035955bool$ua','hAPP$ub2019457360e$ubool'('cOMBK$ubool$ustate','bot$ubot$ubool')),'hAPP$ub540892988e$ubool'('hAPP$uf1824947087e$ubool'('cOMBC$u41962815e$ubool','hAPP$uf340725611e$ubool'('hAPP$uf1006724181e$ubool'('cOMBB$u1348041619bool$ua','cOMBC$u231445413l$ubool'),'hAPP$uf1509969235l$ubool'('hAPP$uf1178339559l$ubool'('cOMBB$u1355796797bool$ua','hAPP$uf1561913689l$ubool'('cOMBB$u188601460$ustate',fconj)),X1))),X0))),sK110('hAPP$uf762886889e$ubool'('cOMBK$u1458035955bool$ua','hAPP$ub2019457360e$ubool'('cOMBK$ubool$ustate','bot$ubot$ubool')),'hAPP$ub540892988e$ubool'('hAPP$uf1824947087e$ubool'('cOMBC$u41962815e$ubool','hAPP$uf340725611e$ubool'('hAPP$uf1006724181e$ubool'('cOMBB$u1348041619bool$ua','cOMBC$u231445413l$ubool'),'hAPP$uf1509969235l$ubool'('hAPP$uf1178339559l$ubool'('cOMBB$u1355796797bool$ua','hAPP$uf1561913689l$ubool'('cOMBB$u188601460$ustate',fconj)),X1))),X0))))
| hBOOL(X0) ),
inference(resolution,[status(thm)],[d17,d15]) ).
cnf(d19,plain,
( hBOOL('hAPP$ustate$ubool'('hAPP$ub2019457360e$ubool'('cOMBK$ubool$ustate','bot$ubot$ubool'),sK110('hAPP$uf762886889e$ubool'('cOMBK$u1458035955bool$ua','hAPP$ub2019457360e$ubool'('cOMBK$ubool$ustate','bot$ubot$ubool')),'hAPP$ub540892988e$ubool'('hAPP$uf1824947087e$ubool'('cOMBC$u41962815e$ubool','hAPP$uf340725611e$ubool'('hAPP$uf1006724181e$ubool'('cOMBB$u1348041619bool$ua','cOMBC$u231445413l$ubool'),'hAPP$uf1509969235l$ubool'('hAPP$uf1178339559l$ubool'('cOMBB$u1355796797bool$ua','hAPP$uf1561913689l$ubool'('cOMBB$u188601460$ustate',fconj)),X0))),X1))))
| hBOOL(X1) ),
inference(demodulation,[status(thm)],[d18,c1188]) ).
cnf(d20,plain,
( hBOOL('bot$ubot$ubool')
| hBOOL(X1) ),
inference(demodulation,[status(thm)],[d19,d0]) ).
cnf(d21,plain,
hBOOL(X0),
inference(resolution,[status(thm)],[d6,d20]) ).
cnf(d22,plain,
$false,
inference(resolution,[status(thm)],[d21,c73]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWW470+2 : TPTP v9.3.1. Released v5.3.0.
% 0.00/0.04 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.37 % Computer : n010.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Sat Sep 26 15:58:15 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.14/0.37 Running casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 37.19/6.21 % SZS status Theorem for theBenchmark.p
% 37.19/6.21 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
%------------------------------------------------------------------------------