%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : SWV858-1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n018.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:04:50 AM UTC 2026
% Result : Unsatisfiable 183.17s 33.16s
% Output : CNFRefutation 183.17s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 13
% Syntax : Number of clauses : 40 ( 22 unt; 4 nHn; 24 RR)
% Number of literals : 62 ( 12 equ; 20 neg)
% Maximal clause size : 3 ( 1 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 5 ( 3 usr; 1 prp; 0-3 aty)
% Number of functors : 15 ( 15 usr; 7 con; 0-3 aty)
% Number of variables : 63 ( 13 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(cls_Un__Diff__cancel_0,axiom,
'c$uLattices$uOupper$u$usemilattice$u$uclass$uOsup'(X0,'c$uHOL$uOminus$u$uclass$uOminus'(X1,X0,'tc$ufun'(X2,'tc$ubool')),'tc$ufun'(X2,'tc$ubool')) = 'c$uLattices$uOupper$u$usemilattice$u$uclass$uOsup'(X0,X1,'tc$ufun'(X2,'tc$ubool')) ).
cnf(cls_Diff__partition_0,axiom,
( ~ 'c$ulessequals'(X0,X1,'tc$ufun'(X2,'tc$ubool'))
| 'c$uLattices$uOupper$u$usemilattice$u$uclass$uOsup'(X0,'c$uHOL$uOminus$u$uclass$uOminus'(X1,X0,'tc$ufun'(X2,'tc$ubool')),'tc$ufun'(X2,'tc$ubool')) = X1 ) ).
cnf(cls_Un__commute_0,axiom,
'c$uLattices$uOupper$u$usemilattice$u$uclass$uOsup'(X0,X1,'tc$ufun'(X2,'tc$ubool')) = 'c$uLattices$uOupper$u$usemilattice$u$uclass$uOsup'(X1,X0,'tc$ufun'(X2,'tc$ubool')) ).
cnf(cls_insert__absorb_0,axiom,
( ~ hBOOL(hAPP(hAPP('c$uin'(X2),X0),X1))
| 'c$uSet$uOinsert'(X0,X1,X2) = X1 ) ).
cnf(cls_sup1CI_0,axiom,
( ~ hBOOL(hAPP(X1,X3))
| hBOOL(hAPP('c$uLattices$uOupper$u$usemilattice$u$uclass$uOsup'(X0,X1,'tc$ufun'(X2,'tc$ubool')),X3)) ) ).
cnf(cls_insert__code_1,axiom,
hBOOL(hAPP('c$uSet$uOinsert'(X0,X1,X2),X0)) ).
cnf(cls_mem__def_1,axiom,
( ~ hBOOL(hAPP(X2,X1))
| hBOOL(hAPP(hAPP('c$uin'(X0),X1),X2)) ) ).
cnf(cls_conjecture_1,negated_conjecture,
'c$ulessequals'('v$utsa','v$uts$uH','tc$ufun'('tc$uHoare$u$uMirabelle$uOtriple'('t$ua'),'tc$ubool')) ).
cnf(cls_conjecture_2,negated_conjecture,
hBOOL(hAPP(hAPP('c$uin'('tc$uHoare$u$uMirabelle$uOtriple'('t$ua')),'v$uxa'),'v$utsa')) ).
cnf(cls_conjecture_3,negated_conjecture,
~ 'c$uHoare$u$uMirabelle$uOtriple$u$uvalid'('v$ux','v$uxa','t$ua') ).
cnf(cls_conjecture_4,negated_conjecture,
( ~ hBOOL(hAPP(hAPP('c$uin'('tc$uHoare$u$uMirabelle$uOtriple'('t$ua')),X0),'v$uGa'))
| 'c$uHoare$u$uMirabelle$uOtriple$u$uvalid'('v$ux',X0,'t$ua') ) ).
cnf(cls_conjecture_5,negated_conjecture,
( hBOOL(hAPP(hAPP('c$uin'('tc$uHoare$u$uMirabelle$uOtriple'('t$ua')),'v$un'(X0)),'v$uGa'))
| ~ hBOOL(hAPP(hAPP('c$uin'('tc$uHoare$u$uMirabelle$uOtriple'('t$ua')),X1),'v$uts$uH'))
| 'c$uHoare$u$uMirabelle$uOtriple$u$uvalid'(X0,X1,'t$ua') ) ).
cnf(cls_conjecture_6,negated_conjecture,
( ~ 'c$uHoare$u$uMirabelle$uOtriple$u$uvalid'(X0,'v$un'(X0),'t$ua')
| ~ hBOOL(hAPP(hAPP('c$uin'('tc$uHoare$u$uMirabelle$uOtriple'('t$ua')),X1),'v$uts$uH'))
| 'c$uHoare$u$uMirabelle$uOtriple$u$uvalid'(X0,X1,'t$ua') ) ).
cnf(c3,plain,
'c$uLattices$uOupper$u$usemilattice$u$uclass$uOsup'(X0,X1,'tc$ufun'(X2,'tc$ubool')) = 'c$uLattices$uOupper$u$usemilattice$u$uclass$uOsup'(X0,'c$uHOL$uOminus$u$uclass$uOminus'(X1,X0,'tc$ufun'(X2,'tc$ubool')),'tc$ufun'(X2,'tc$ubool')),
inference(clausification,[status(esa)],[cls_Un__Diff__cancel_0]) ).
cnf(c25,plain,
( ~ 'c$ulessequals'(X0,X1,'tc$ufun'(X2,'tc$ubool'))
| 'c$uLattices$uOupper$u$usemilattice$u$uclass$uOsup'(X0,'c$uHOL$uOminus$u$uclass$uOminus'(X1,X0,'tc$ufun'(X2,'tc$ubool')),'tc$ufun'(X2,'tc$ubool')) = X1 ),
inference(clausification,[status(esa)],[cls_Diff__partition_0]) ).
cnf(c53,plain,
'c$uLattices$uOupper$u$usemilattice$u$uclass$uOsup'(X0,X1,'tc$ufun'(X2,'tc$ubool')) = 'c$uLattices$uOupper$u$usemilattice$u$uclass$uOsup'(X1,X0,'tc$ufun'(X2,'tc$ubool')),
inference(clausification,[status(esa)],[cls_Un__commute_0]) ).
cnf(c145,plain,
( ~ hBOOL(hAPP(hAPP('c$uin'(X2),X0),X1))
| 'c$uSet$uOinsert'(X0,X1,X2) = X1 ),
inference(clausification,[status(esa)],[cls_insert__absorb_0]) ).
cnf(c217,plain,
( ~ hBOOL(hAPP(X1,X3))
| hBOOL(hAPP('c$uLattices$uOupper$u$usemilattice$u$uclass$uOsup'(X0,X1,'tc$ufun'(X2,'tc$ubool')),X3)) ),
inference(clausification,[status(esa)],[cls_sup1CI_0]) ).
cnf(c392,plain,
hBOOL(hAPP('c$uSet$uOinsert'(X0,X1,X2),X0)),
inference(clausification,[status(esa)],[cls_insert__code_1]) ).
cnf(c544,plain,
( ~ hBOOL(hAPP(X2,X1))
| hBOOL(hAPP(hAPP('c$uin'(X0),X1),X2)) ),
inference(clausification,[status(esa)],[cls_mem__def_1]) ).
cnf(c549,plain,
'c$ulessequals'('v$utsa','v$uts$uH','tc$ufun'('tc$uHoare$u$uMirabelle$uOtriple'('t$ua'),'tc$ubool')),
inference(clausification,[status(esa)],[cls_conjecture_1]) ).
cnf(c550,plain,
hBOOL(hAPP(hAPP('c$uin'('tc$uHoare$u$uMirabelle$uOtriple'('t$ua')),'v$uxa'),'v$utsa')),
inference(clausification,[status(esa)],[cls_conjecture_2]) ).
cnf(c551,plain,
~ 'c$uHoare$u$uMirabelle$uOtriple$u$uvalid'('v$ux','v$uxa','t$ua'),
inference(clausification,[status(esa)],[cls_conjecture_3]) ).
cnf(c552,plain,
( ~ hBOOL(hAPP(hAPP('c$uin'('tc$uHoare$u$uMirabelle$uOtriple'('t$ua')),X0),'v$uGa'))
| 'c$uHoare$u$uMirabelle$uOtriple$u$uvalid'('v$ux',X0,'t$ua') ),
inference(clausification,[status(esa)],[cls_conjecture_4]) ).
cnf(c553,plain,
( hBOOL(hAPP(hAPP('c$uin'('tc$uHoare$u$uMirabelle$uOtriple'('t$ua')),'v$un'(X1)),'v$uGa'))
| 'c$uHoare$u$uMirabelle$uOtriple$u$uvalid'(X1,X0,'t$ua')
| ~ hBOOL(hAPP(hAPP('c$uin'('tc$uHoare$u$uMirabelle$uOtriple'('t$ua')),X0),'v$uts$uH')) ),
inference(clausification,[status(esa)],[cls_conjecture_5]) ).
cnf(c554,plain,
( ~ 'c$uHoare$u$uMirabelle$uOtriple$u$uvalid'(X1,'v$un'(X1),'t$ua')
| 'c$uHoare$u$uMirabelle$uOtriple$u$uvalid'(X1,X0,'t$ua')
| ~ hBOOL(hAPP(hAPP('c$uin'('tc$uHoare$u$uMirabelle$uOtriple'('t$ua')),X0),'v$uts$uH')) ),
inference(clausification,[status(esa)],[cls_conjecture_6]) ).
cnf(d0,plain,
'c$uSet$uOinsert'('v$uxa','v$utsa','tc$uHoare$u$uMirabelle$uOtriple'('t$ua')) = 'v$utsa',
inference(resolution,[status(thm)],[c145,c550]) ).
cnf(d1,plain,
hBOOL(hAPP('v$utsa','v$uxa')),
inference(superposition,[status(thm)],[d0,c392]) ).
cnf(d2,plain,
hBOOL(hAPP('c$uLattices$uOupper$u$usemilattice$u$uclass$uOsup'(X0,'v$utsa','tc$ufun'(X1,'tc$ubool')),'v$uxa')),
inference(resolution,[status(thm)],[c217,d1]) ).
cnf(d3,plain,
( ~ 'c$ulessequals'(X0,X1,'tc$ufun'(X2,'tc$ubool'))
| 'c$uLattices$uOupper$u$usemilattice$u$uclass$uOsup'(X0,X1,'tc$ufun'(X2,'tc$ubool')) = X1 ),
inference(demodulation,[status(thm)],[c25,c3]) ).
cnf(d4,plain,
'c$uLattices$uOupper$u$usemilattice$u$uclass$uOsup'('v$utsa','v$uts$uH','tc$ufun'('tc$uHoare$u$uMirabelle$uOtriple'('t$ua'),'tc$ubool')) = 'v$uts$uH',
inference(resolution,[status(thm)],[c549,d3]) ).
cnf(d5,plain,
'c$uLattices$uOupper$u$usemilattice$u$uclass$uOsup'('v$uts$uH','v$utsa','tc$ufun'('tc$uHoare$u$uMirabelle$uOtriple'('t$ua'),'tc$ubool')) = 'v$uts$uH',
inference(demodulation,[status(thm)],[d4,c53]) ).
cnf(d6,plain,
hBOOL(hAPP('v$uts$uH','v$uxa')),
inference(superposition,[status(thm)],[d5,d2]) ).
cnf(d7,plain,
hBOOL(hAPP(hAPP('c$uin'(X0),'v$uxa'),'v$uts$uH')),
inference(resolution,[status(thm)],[c544,d6]) ).
cnf(d8,plain,
( ~ 'c$uHoare$u$uMirabelle$uOtriple$u$uvalid'(X0,'v$un'(X0),'t$ua')
| 'c$uHoare$u$uMirabelle$uOtriple$u$uvalid'(X0,'v$uxa','t$ua') ),
inference(resolution,[status(thm)],[c554,d7]) ).
cnf(d9,plain,
( 'c$uHoare$u$uMirabelle$uOtriple$u$uvalid'(X0,'v$uxa','t$ua')
| hBOOL(hAPP(hAPP('c$uin'('tc$uHoare$u$uMirabelle$uOtriple'('t$ua')),'v$un'(X0)),'v$uGa')) ),
inference(resolution,[status(thm)],[c553,d7]) ).
cnf(d10,plain,
( 'c$uHoare$u$uMirabelle$uOtriple$u$uvalid'('v$ux','v$un'(X0),'t$ua')
| 'c$uHoare$u$uMirabelle$uOtriple$u$uvalid'(X0,'v$uxa','t$ua') ),
inference(resolution,[status(thm)],[d9,c552]) ).
cnf(d11,plain,
'c$uHoare$u$uMirabelle$uOtriple$u$uvalid'('v$ux','v$un'('v$ux'),'t$ua'),
inference(resolution,[status(thm)],[d10,c551]) ).
cnf(d12,plain,
'c$uHoare$u$uMirabelle$uOtriple$u$uvalid'('v$ux','v$uxa','t$ua'),
inference(resolution,[status(thm)],[d11,d8]) ).
cnf(d13,plain,
$false,
inference(resolution,[status(thm)],[c551,d12]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWV858-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.04 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n018.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Sat Sep 26 15:07:07 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.08/0.35 Running casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 183.17/33.16 % SZS status Unsatisfiable for theBenchmark.p
% 183.17/33.16 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
%------------------------------------------------------------------------------