%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : SWW341+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 : n006.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:43 AM UTC 2026
% Result : Theorem 32.64s 19.89s
% Output : CNFRefutation 32.64s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWW341+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.10/5.38 % Computer : n006.cluster.edu
% 0.10/5.38 % Model : x86_64 x86_64
% 0.10/5.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/5.38 % Memory : 8046.5625MB
% 0.10/5.38 % OS : Linux 6.8.0-71-generic
% 0.10/5.38 % CPULimit : 300
% 0.10/5.38 % WCLimit : 300
% 0.10/5.38 % DateTime : Sat Sep 26 15:41:48 UTC 2026
% 0.10/5.38 % CPUTime :
% 0.10/5.38 Running casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 32.64/19.89 % SZS status Theorem for theBenchmark.p
% 32.64/19.89 % SZS output start CNFRefutation for theBenchmark.p
% 32.64/19.89 fof(conj_0, hypothesis, ! [X0] : ! [X1] : (('v$uP'(X0,X1) => ? [X2] : ? [X3] : (('c$uHoare$u$uMirabelle$uOhoare$u$uderivs'('t$ua','v$uG',hAPP(hAPP('c$uSet$uOinsert'('tc$uHoare$u$uMirabelle$uOtriple'('t$ua')),hAPP(hAPP(hAPP('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')))) & (! [X4] : ((! [X5] : ((hBOOL(hAPP(hAPP('c$umember'('tc$uHoare$u$uMirabelle$uOtriple'('t$ua')),X5),'v$uG')) => 'c$uHoare$u$uMirabelle$uOtriple$u$uvalid'('t$ua',X4,X5))) => ! [X6] : ! [X7] : ((hBOOL(hAPP(hAPP(X2,X6),X7)) => ! [X8] : (('c$uNatural$uOevaln'('v$uc',X7,X4,X8) => hBOOL(hAPP(hAPP(X3,X6),X8)))))))) & ! [X8] : ((! [X9] : ((hBOOL(hAPP(hAPP(X2,X9),X1)) => hBOOL(hAPP(hAPP(X3,X9),X8)))) => 'v$uQ'(X0,X8))))))))).
% 32.64/19.89 fof(conj_1, hypothesis, ! [X0] : ((hBOOL(hAPP(hAPP('c$umember'('tc$uHoare$u$uMirabelle$uOtriple'('t$ua')),X0),'v$uG')) => 'c$uHoare$u$uMirabelle$uOtriple$u$uvalid'('t$ua','v$un',X0)))).
% 32.64/19.89 fof(conj_2, conjecture, ! [X0] : ! [X1] : (('v$uP'(X0,X1) => ! [X2] : (('c$uNatural$uOevaln'('v$uc',X1,'v$un',X2) => 'v$uQ'(X0,X2)))))).
% 32.64/19.89 fof(negated_conjecture, negated_conjecture, ~! [X0] : ! [X1] : (('v$uP'(X0,X1) => ! [X2] : (('c$uNatural$uOevaln'('v$uc',X1,'v$un',X2) => 'v$uQ'(X0,X2))))), inference(negate_conjecture, [status(cth)], [conj_2])).
% 32.64/19.89 cnf(c42, plain, ~'v$uP'(X0,X1) | X2(X0,X1), inference(clausification, [status(esa)], [conj_0])).
% 32.64/19.89 cnf(c44, plain, ~X0(X1,X2) | hBOOL(hAPP(hAPP(sK92(X1,X2),sK95(X1,X2,X3)),X2)) | 'v$uQ'(X1,X3), inference(clausification, [status(esa)], [conj_0])).
% 32.64/19.89 cnf(c45, plain, ~X0(X1,X2) | ~hBOOL(hAPP(hAPP(sK93(X1,X2),sK95(X1,X2,X3)),X3)) | 'v$uQ'(X1,X3), inference(clausification, [status(esa)], [conj_0])).
% 32.64/19.89 cnf(c46, plain, ~hBOOL(hAPP(hAPP(sK92(X0,X1),X2),X3)) | hBOOL(hAPP(hAPP('c$umember'('tc$uHoare$u$uMirabelle$uOtriple'('t$ua')),sK97(X4)),'v$uG')) | ~'c$uNatural$uOevaln'('v$uc',X3,X4,X5) | ~X6(X0,X1) | hBOOL(hAPP(hAPP(sK93(X0,X1),X2),X5)), inference(clausification, [status(esa)], [conj_0])).
% 32.64/19.89 cnf(c47, plain, ~hBOOL(hAPP(hAPP(sK92(X0,X1),X2),X3)) | ~'c$uHoare$u$uMirabelle$uOtriple$u$uvalid'('t$ua',X4,sK97(X4)) | ~'c$uNatural$uOevaln'('v$uc',X3,X4,X5) | ~X6(X0,X1) | hBOOL(hAPP(hAPP(sK93(X0,X1),X2),X5)), inference(clausification, [status(esa)], [conj_0])).
% 32.64/19.89 cnf(c48, plain, ~hBOOL(hAPP(hAPP('c$umember'('tc$uHoare$u$uMirabelle$uOtriple'('t$ua')),X0),'v$uG')) | 'c$uHoare$u$uMirabelle$uOtriple$u$uvalid'('t$ua','v$un',X0), inference(clausification, [status(esa)], [conj_1])).
% 32.64/19.89 cnf(c49, plain, 'v$uP'(sK102,sK103), inference(clausification, [status(esa)], [negated_conjecture])).
% 32.64/19.89 cnf(c50, plain, 'c$uNatural$uOevaln'('v$uc',sK103,'v$un',sK104), inference(clausification, [status(esa)], [negated_conjecture])).
% 32.64/19.89 cnf(c51, plain, ~'v$uQ'(sK102,sK104), inference(clausification, [status(esa)], [negated_conjecture])).
% 32.64/19.89 cnf(d0, plain, 'Ts89'(sK102,sK103), inference(resolution, [status(thm)], [c42,c49])).
% 32.64/19.89 cnf(d1, plain, hBOOL(hAPP(hAPP(sK92(sK102,sK103),sK95(sK102,sK103,X0)),sK103)) | 'v$uQ'(sK102,X0), inference(resolution, [status(thm)], [c44,d0])).
% 32.64/19.90 cnf(d2, plain, ~hBOOL(hAPP(hAPP(sK92(X0,X1),X2),sK103)) | hBOOL(hAPP(hAPP(sK93(X0,X1),X2),sK104)) | ~'Ts89'(X0,X1) | ~'c$uHoare$u$uMirabelle$uOtriple$u$uvalid'('t$ua','v$un',sK97('v$un')), inference(resolution, [status(thm)], [c47,c50])).
% 32.64/19.90 cnf(d3, plain, hBOOL(hAPP(hAPP(sK93(sK102,sK103),sK95(sK102,sK103,X0)),sK104)) | ~'Ts89'(sK102,sK103) | ~'c$uHoare$u$uMirabelle$uOtriple$u$uvalid'('t$ua','v$un',sK97('v$un')) | 'v$uQ'(sK102,X0), inference(resolution, [status(thm)], [d2,d1])).
% 32.64/19.90 cnf(d4, plain, hBOOL(hAPP(hAPP(sK93(sK102,sK103),sK95(sK102,sK103,X0)),sK104)) | 'v$uQ'(sK102,X0) | ~'c$uHoare$u$uMirabelle$uOtriple$u$uvalid'('t$ua','v$un',sK97('v$un')), inference(resolution, [status(thm)], [d0,d3])).
% 32.64/19.90 cnf(d5, plain, ~hBOOL(hAPP(hAPP(sK92(X0,X1),X2),sK103)) | hBOOL(hAPP(hAPP(sK93(X0,X1),X2),sK104)) | hBOOL(hAPP(hAPP('c$umember'('tc$uHoare$u$uMirabelle$uOtriple'('t$ua')),sK97('v$un')),'v$uG')) | ~'Ts89'(X0,X1), inference(resolution, [status(thm)], [c46,c50])).
% 32.64/19.90 cnf(d6, plain, hBOOL(hAPP(hAPP(sK93(sK102,sK103),sK95(sK102,sK103,X0)),sK104)) | hBOOL(hAPP(hAPP('c$umember'('tc$uHoare$u$uMirabelle$uOtriple'('t$ua')),sK97('v$un')),'v$uG')) | ~'Ts89'(sK102,sK103) | 'v$uQ'(sK102,X0), inference(resolution, [status(thm)], [d5,d1])).
% 32.64/19.90 cnf(d7, plain, hBOOL(hAPP(hAPP(sK93(sK102,sK103),sK95(sK102,sK103,X0)),sK104)) | hBOOL(hAPP(hAPP('c$umember'('tc$uHoare$u$uMirabelle$uOtriple'('t$ua')),sK97('v$un')),'v$uG')) | 'v$uQ'(sK102,X0), inference(resolution, [status(thm)], [d0,d6])).
% 32.64/19.90 cnf(d8, plain, hBOOL(hAPP(hAPP('c$umember'('tc$uHoare$u$uMirabelle$uOtriple'('t$ua')),sK97('v$un')),'v$uG')) | 'v$uQ'(sK102,sK104) | ~'Ts89'(sK102,sK103) | 'v$uQ'(sK102,sK104), inference(resolution, [status(thm)], [d7,c45])).
% 32.64/19.90 cnf(d9, plain, hBOOL(hAPP(hAPP('c$umember'('tc$uHoare$u$uMirabelle$uOtriple'('t$ua')),sK97('v$un')),'v$uG')) | ~'Ts89'(sK102,sK103), inference(resolution, [status(thm)], [c51,d8])).
% 32.64/19.90 cnf(d10, plain, hBOOL(hAPP(hAPP('c$umember'('tc$uHoare$u$uMirabelle$uOtriple'('t$ua')),sK97('v$un')),'v$uG')), inference(resolution, [status(thm)], [d0,d9])).
% 32.64/19.90 cnf(d11, plain, 'c$uHoare$u$uMirabelle$uOtriple$u$uvalid'('t$ua','v$un',sK97('v$un')), inference(resolution, [status(thm)], [d10,c48])).
% 32.64/19.90 cnf(d12, plain, hBOOL(hAPP(hAPP(sK93(sK102,sK103),sK95(sK102,sK103,X0)),sK104)) | 'v$uQ'(sK102,X0), inference(resolution, [status(thm)], [d11,d4])).
% 32.64/19.90 cnf(d13, plain, 'v$uQ'(sK102,sK104) | ~'Ts89'(sK102,sK103) | 'v$uQ'(sK102,sK104), inference(resolution, [status(thm)], [d12,c45])).
% 32.64/19.90 cnf(d14, plain, ~'Ts89'(sK102,sK103), inference(resolution, [status(thm)], [c51,d13])).
% 32.64/19.90 cnf(d15, plain, $false, inference(resolution, [status(thm)], [d0,d14])).
% 32.64/19.90 % SZS output end CNFRefutation for theBenchmark.p
%------------------------------------------------------------------------------