%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : SCT162+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 : n008.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 08:27:52 AM UTC 2026
% Result : Theorem 141.09s 39.42s
% Output : CNFRefutation 141.09s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SCT162+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.06 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.17/10.65 % Computer : n008.cluster.edu
% 0.17/10.65 % Model : x86_64 x86_64
% 0.17/10.65 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/10.65 % Memory : 8046.5625MB
% 0.17/10.65 % OS : Linux 6.8.0-71-generic
% 0.17/10.65 % CPULimit : 300
% 0.17/10.65 % WCLimit : 300
% 0.17/10.65 % DateTime : Sat Sep 26 06:35:38 UTC 2026
% 0.17/10.65 % CPUTime :
% 0.17/10.65 Running casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 141.09/39.42 % SZS status Theorem for theBenchmark.p
% 141.09/39.42 % SZS output start CNFRefutation for theBenchmark.p
% 141.09/39.42 fof(fact__096c_A_126_061_Ad_096, axiom, 'v$uc' != 'v$ud').
% 141.09/39.42 fof(fact_top1I, axiom, ! [X0] : ! [X1] : hBOOL(hAPP('c$uOrderings$uOtop$u$uclass$uOtop'('tc$ufun'(X1,'tc$uHOL$uObool')),X0))).
% 141.09/39.42 fof(fact_eq__mem, axiom, ! [X0] : ! [X1] : ! [X2] : ((hBOOL(hAPP(hAPP('c$umember'(X2),X1),hAPP('c$ufequal',X0))) <=> X1 = X0))).
% 141.09/39.42 fof(fact_mem__def, axiom, ! [X0] : ! [X1] : ! [X2] : ((hBOOL(hAPP(hAPP('c$umember'(X2),X1),X0)) <=> hBOOL(hAPP(X0,X1))))).
% 141.09/39.42 fof(fact_inv__f__f, axiom, ! [X0] : ! [X1] : ! [X2] : ! [X3] : (('c$uFun$uOinj$u$uon'(X3,X2,X1,'c$uOrderings$uOtop$u$uclass$uOtop'('tc$ufun'(X3,'tc$uHOL$uObool'))) => hAPP('c$uHilbert$u$uChoice$uOinv$u$uinto'(X3,X2,'c$uOrderings$uOtop$u$uclass$uOtop'('tc$ufun'(X3,'tc$uHOL$uObool')),X1),hAPP(X1,X0)) = X0))).
% 141.09/39.42 fof(fact_inj__on__def, axiom, ! [X0] : ! [X1] : ! [X2] : ! [X3] : (('c$uFun$uOinj$u$uon'(X3,X2,X1,X0) <=> ! [X4] : ((hBOOL(hAPP(hAPP('c$umember'(X3),X4),X0)) => ! [X5] : ((hBOOL(hAPP(hAPP('c$umember'(X3),X5),X0)) => (hAPP(X1,X4) = hAPP(X1,X5) => X4 = X5)))))))).
% 141.09/39.42 fof(fact_subset__UNIV, axiom, ! [X0] : ! [X1] : hBOOL(hAPP('c$uOrderings$uOord$u$uclass$uOless$u$ueq'('tc$ufun'(X1,'tc$uHOL$uObool'),X0),'c$uOrderings$uOtop$u$uclass$uOtop'('tc$ufun'(X1,'tc$uHOL$uObool'))))).
% 141.09/39.42 fof(fact_subset__inj__on, axiom, ! [X0] : ! [X1] : ! [X2] : ! [X3] : ! [X4] : (('c$uFun$uOinj$u$uon'(X4,X3,X2,X1) => (hBOOL(hAPP('c$uOrderings$uOord$u$uclass$uOless$u$ueq'('tc$ufun'(X4,'tc$uHOL$uObool'),X0),X1)) => 'c$uFun$uOinj$u$uon'(X4,X3,X2,X0))))).
% 141.09/39.42 fof(fact_finite__indi, axiom, 'c$uFinite$u$uSet$uOfinite'('tc$uArrow$u$uOrder$u$uMirabelle$uOindi','c$uOrderings$uOtop$u$uclass$uOtop'('tc$ufun'('tc$uArrow$u$uOrder$u$uMirabelle$uOindi','tc$uHOL$uObool')))).
% 141.09/39.42 fof(fact_rev__finite__subset, axiom, ! [X0] : ! [X1] : ! [X2] : (('c$uFinite$u$uSet$uOfinite'(X2,X1) => (hBOOL(hAPP('c$uOrderings$uOord$u$uclass$uOless$u$ueq'('tc$ufun'(X2,'tc$uHOL$uObool'),X0),X1)) => 'c$uFinite$u$uSet$uOfinite'(X2,X0))))).
% 141.09/39.42 fof(fact_finite__imageD, axiom, ! [X0] : ! [X1] : ! [X2] : ! [X3] : (('c$uFinite$u$uSet$uOfinite'(X3,'c$uSet$uOimage'(X2,X3,X1,X0)) => ('c$uFun$uOinj$u$uon'(X2,X3,X1,X0) => 'c$uFinite$u$uSet$uOfinite'(X2,X0))))).
% 141.09/39.42 fof(fact_image__iff, axiom, ! [X0] : ! [X1] : ! [X2] : ! [X3] : ! [X4] : ((hBOOL(hAPP(hAPP('c$umember'(X4),X3),'c$uSet$uOimage'(X2,X4,X1,X0))) <=> ? [X5] : ((hBOOL(hAPP(hAPP('c$umember'(X2),X5),X0)) & X3 = hAPP(X1,X5)))))).
% 141.09/39.42 fof(fact_finite__UNIV__inj__surj, axiom, ! [X0] : ! [X1] : (('c$uFinite$u$uSet$uOfinite'(X1,'c$uOrderings$uOtop$u$uclass$uOtop'('tc$ufun'(X1,'tc$uHOL$uObool'))) => ('c$uFun$uOinj$u$uon'(X1,X1,X0,'c$uOrderings$uOtop$u$uclass$uOtop'('tc$ufun'(X1,'tc$uHOL$uObool'))) => 'c$uSet$uOimage'(X1,X1,X0,'c$uOrderings$uOtop$u$uclass$uOtop'('tc$ufun'(X1,'tc$uHOL$uObool'))) = 'c$uOrderings$uOtop$u$uclass$uOtop'('tc$ufun'(X1,'tc$uHOL$uObool')))))).
% 141.09/39.42 fof(help_c__COMBK__1, axiom, ! [X0] : ! [X1] : ! [X2] : ! [X3] : hAPP(hAPP('c$uCOMBK'(X3,X2),X1),X0) = X1).
% 141.09/39.42 fof(help_c__COMBS__1, axiom, ! [X0] : ! [X1] : ! [X2] : ! [X3] : ! [X4] : ! [X5] : hAPP('c$uCOMBS'(X5,X4,X3,X2,X1),X0) = hAPP(hAPP(X2,X0),hAPP(X1,X0))).
% 141.09/39.42 fof(help_c__fequal__1, axiom, ! [X0] : ! [X1] : ((~hBOOL(hAPP(hAPP('c$ufequal',X1),X0)) | X1 = X0))).
% 141.09/39.42 fof(help_c__fequal__2, axiom, ! [X0] : ! [X1] : ((X1 != X0 | hBOOL(hAPP(hAPP('c$ufequal',X1),X0))))).
% 141.09/39.42 cnf(c2, plain, 'v$uc' != 'v$ud', inference(clausification, [status(esa)], [fact__096c_A_126_061_Ad_096])).
% 141.09/39.42 cnf(c22, plain, hBOOL(hAPP('c$uOrderings$uOtop$u$uclass$uOtop'('tc$ufun'(X0,'tc$uHOL$uObool')),X1)), inference(clausification, [status(esa)], [fact_top1I])).
% 141.09/39.42 cnf(c30, plain, ~hBOOL(hAPP(hAPP('c$umember'(X0),X1),hAPP('c$ufequal',X2))) | X1 = X2, inference(clausification, [status(esa)], [fact_eq__mem])).
% 141.09/39.42 cnf(c33, plain, hBOOL(hAPP(hAPP('c$umember'(X0),X1),X2)) | ~hBOOL(hAPP(X2,X1)), inference(clausification, [status(esa)], [fact_mem__def])).
% 141.09/39.42 cnf(c95, plain, ~'c$uFun$uOinj$u$uon'(X0,X1,X2,'c$uOrderings$uOtop$u$uclass$uOtop'('tc$ufun'(X0,'tc$uHOL$uObool'))) | hAPP('c$uHilbert$u$uChoice$uOinv$u$uinto'(X0,X1,'c$uOrderings$uOtop$u$uclass$uOtop'('tc$ufun'(X0,'tc$uHOL$uObool')),X2),hAPP(X2,X3)) = X3, inference(clausification, [status(esa)], [fact_inv__f__f])).
% 141.09/39.42 cnf(c106, plain, 'c$uFun$uOinj$u$uon'(X0,X1,X2,X3) | ~X4(X0,X3,X2), inference(clausification, [status(esa)], [fact_inj__on__def])).
% 141.09/39.42 cnf(c108, plain, X0(X1,X2,X3) | hBOOL(hAPP(hAPP('c$umember'(X1),sK158(X1,X2,X3)),X2)), inference(clausification, [status(esa)], [fact_inj__on__def])).
% 141.09/39.42 cnf(c109, plain, X0(X1,X2,X3) | hBOOL(hAPP(hAPP('c$umember'(X1),sK159(X1,X2,X3)),X2)), inference(clausification, [status(esa)], [fact_inj__on__def])).
% 141.09/39.42 cnf(c110, plain, X0(X1,X2,X3) | hAPP(X3,sK158(X1,X2,X3)) = hAPP(X3,sK159(X1,X2,X3)), inference(clausification, [status(esa)], [fact_inj__on__def])).
% 141.09/39.42 cnf(c111, plain, X0(X1,X2,X3) | sK158(X1,X2,X3) != sK159(X1,X2,X3), inference(clausification, [status(esa)], [fact_inj__on__def])).
% 141.09/39.42 cnf(c228, plain, hBOOL(hAPP('c$uOrderings$uOord$u$uclass$uOless$u$ueq'('tc$ufun'(X0,'tc$uHOL$uObool'),X1),'c$uOrderings$uOtop$u$uclass$uOtop'('tc$ufun'(X0,'tc$uHOL$uObool')))), inference(clausification, [status(esa)], [fact_subset__UNIV])).
% 141.09/39.42 cnf(c229, plain, ~'c$uFun$uOinj$u$uon'(X0,X1,X2,X3) | ~hBOOL(hAPP('c$uOrderings$uOord$u$uclass$uOless$u$ueq'('tc$ufun'(X0,'tc$uHOL$uObool'),X4),X3)) | 'c$uFun$uOinj$u$uon'(X0,X1,X2,X4), inference(clausification, [status(esa)], [fact_subset__inj__on])).
% 141.09/39.42 cnf(c267, plain, 'c$uFinite$u$uSet$uOfinite'('tc$uArrow$u$uOrder$u$uMirabelle$uOindi','c$uOrderings$uOtop$u$uclass$uOtop'('tc$ufun'('tc$uArrow$u$uOrder$u$uMirabelle$uOindi','tc$uHOL$uObool'))), inference(clausification, [status(esa)], [fact_finite__indi])).
% 141.09/39.42 cnf(c272, plain, ~'c$uFinite$u$uSet$uOfinite'(X0,X1) | ~hBOOL(hAPP('c$uOrderings$uOord$u$uclass$uOless$u$ueq'('tc$ufun'(X0,'tc$uHOL$uObool'),X2),X1)) | 'c$uFinite$u$uSet$uOfinite'(X0,X2), inference(clausification, [status(esa)], [fact_rev__finite__subset])).
% 141.09/39.42 cnf(c312, plain, ~'c$uFinite$u$uSet$uOfinite'(X0,'c$uSet$uOimage'(X1,X0,X2,X3)) | ~'c$uFun$uOinj$u$uon'(X1,X0,X2,X3) | 'c$uFinite$u$uSet$uOfinite'(X1,X3), inference(clausification, [status(esa)], [fact_finite__imageD])).
% 141.09/39.42 cnf(c328, plain, ~hBOOL(hAPP(hAPP('c$umember'(X0),X1),'c$uSet$uOimage'(X2,X0,X3,X4))) | X1 = hAPP(X3,sK620(X4,X3,X2,X1)), inference(clausification, [status(esa)], [fact_image__iff])).
% 141.09/39.42 cnf(c345, plain, ~'c$uFinite$u$uSet$uOfinite'(X0,'c$uOrderings$uOtop$u$uclass$uOtop'('tc$ufun'(X0,'tc$uHOL$uObool'))) | ~'c$uFun$uOinj$u$uon'(X0,X0,X1,'c$uOrderings$uOtop$u$uclass$uOtop'('tc$ufun'(X0,'tc$uHOL$uObool'))) | 'c$uSet$uOimage'(X0,X0,X1,'c$uOrderings$uOtop$u$uclass$uOtop'('tc$ufun'(X0,'tc$uHOL$uObool'))) = 'c$uOrderings$uOtop$u$uclass$uOtop'('tc$ufun'(X0,'tc$uHOL$uObool')), inference(clausification, [status(esa)], [fact_finite__UNIV__inj__surj])).
% 141.09/39.42 cnf(c358, plain, hAPP(hAPP('c$uCOMBK'(X0,X1),X2),X3) = X2, inference(clausification, [status(esa)], [help_c__COMBK__1])).
% 141.09/39.42 cnf(c361, plain, hAPP('c$uCOMBS'(X0,X1,X2,X3,X4),X5) = hAPP(hAPP(X3,X5),hAPP(X4,X5)), inference(clausification, [status(esa)], [help_c__COMBS__1])).
% 141.09/39.42 cnf(c362, plain, ~hBOOL(hAPP(hAPP('c$ufequal',X0),X1)) | X0 = X1, inference(clausification, [status(esa)], [help_c__fequal__1])).
% 141.09/39.42 cnf(c363, plain, X0 != X1 | hBOOL(hAPP(hAPP('c$ufequal',X0),X1)), inference(clausification, [status(esa)], [help_c__fequal__2])).
% 141.09/39.42 cnf(d0, plain, hAPP('c$uHilbert$u$uChoice$uOinv$u$uinto'(X4,X5,'c$uOrderings$uOtop$u$uclass$uOtop'('tc$ufun'(X4,'tc$uHOL$uObool')),hAPP('c$uCOMBK'(X0,X1),X2)),X2) = X3 | ~'c$uFun$uOinj$u$uon'(X4,X5,hAPP('c$uCOMBK'(X0,X1),X2),'c$uOrderings$uOtop$u$uclass$uOtop'('tc$ufun'(X4,'tc$uHOL$uObool'))), inference(superposition, [status(thm)], [c358,c95])).
% 141.09/39.42 cnf(d1, plain, X5 = X6 | ~'c$uFun$uOinj$u$uon'(X0,X1,hAPP('c$uCOMBK'(X2,X3),X4),'c$uOrderings$uOtop$u$uclass$uOtop'('tc$ufun'(X0,'tc$uHOL$uObool'))) | ~'c$uFun$uOinj$u$uon'(X0,X1,hAPP('c$uCOMBK'(X2,X3),X4),'c$uOrderings$uOtop$u$uclass$uOtop'('tc$ufun'(X0,'tc$uHOL$uObool'))), inference(superposition, [status(thm)], [d0,d0])).
% 141.09/39.42 cnf(d2, plain, X0 = X1 | ~'Ts151'(X2,'c$uOrderings$uOtop$u$uclass$uOtop'('tc$ufun'(X2,'tc$uHOL$uObool')),hAPP('c$uCOMBK'(X3,X4),X5)), inference(resolution, [status(thm)], [d1,c106])).
% 141.09/39.42 cnf(d3, plain, 'Ts151'(X0,hAPP('c$ufequal',X1),X2) | sK159(X0,hAPP('c$ufequal',X1),X2) = X1, inference(resolution, [status(thm)], [c109,c30])).
% 141.09/39.42 cnf(d4, plain, sK158(X0,hAPP('c$ufequal',X1),X2) != X1 | 'Ts151'(X0,hAPP('c$ufequal',X1),X2) | 'Ts151'(X0,hAPP('c$ufequal',X1),X2), inference(superposition, [status(thm)], [d3,c111])).
% 141.09/39.42 cnf(d5, plain, 'Ts151'(X0,hAPP('c$ufequal',X1),X2) | sK158(X0,hAPP('c$ufequal',X1),X2) = X1, inference(resolution, [status(thm)], [c108,c30])).
% 141.09/39.42 cnf(d6, plain, X1 != X1 | 'Ts151'(X0,hAPP('c$ufequal',X1),X2) | 'Ts151'(X0,hAPP('c$ufequal',X1),X2), inference(superposition, [status(thm)], [d5,d4])).
% 141.09/39.42 cnf(d7, plain, 'Ts151'(X0,hAPP('c$ufequal',X1),X2), inference(equality_resolution, [status(thm)], [d6])).
% 141.09/39.42 cnf(d8, plain, X0 = hAPP(X1,sK620(X2,X1,X3,X0)) | ~hBOOL(hAPP('c$uSet$uOimage'(X3,X4,X1,X2),X0)), inference(resolution, [status(thm)], [c328,c33])).
% 141.09/39.42 cnf(d9, plain, 'Ts151'(X3,X2,X4) | ~hBOOL(hAPP('c$uSet$uOimage'(X1,X5,'c$ufequal',X0),X2)), inference(superposition, [status(thm)], [d8,d7])).
% 141.09/39.42 cnf(d10, plain, ~'c$uFinite$u$uSet$uOfinite'(X0,'c$uOrderings$uOtop$u$uclass$uOtop'('tc$ufun'(X0,'tc$uHOL$uObool'))) | 'c$uFinite$u$uSet$uOfinite'(X0,X1), inference(resolution, [status(thm)], [c272,c228])).
% 141.09/39.42 cnf(d11, plain, 'c$uFinite$u$uSet$uOfinite'('tc$uArrow$u$uOrder$u$uMirabelle$uOindi',X0), inference(resolution, [status(thm)], [d10,c267])).
% 141.09/39.42 cnf(d12, plain, ~'c$uFun$uOinj$u$uon'(X0,'tc$uArrow$u$uOrder$u$uMirabelle$uOindi',X1,X2) | 'c$uFinite$u$uSet$uOfinite'(X0,X2), inference(resolution, [status(thm)], [c312,d11])).
% 141.09/39.42 cnf(d13, plain, 'c$uFinite$u$uSet$uOfinite'(X0,X1) | ~'Ts151'(X0,X1,X2), inference(resolution, [status(thm)], [d12,c106])).
% 141.09/39.42 cnf(d14, plain, hBOOL(hAPP(hAPP('c$ufequal',X0),X0)), inference(equality_resolution, [status(thm)], [c363])).
% 141.09/39.42 cnf(d15, plain, hBOOL(hAPP(hAPP('c$ufequal',sK158(X0,X1,'c$ufequal')),sK159(X0,X1,'c$ufequal'))) | 'Ts151'(X0,X1,'c$ufequal'), inference(superposition, [status(thm)], [c110,d14])).
% 141.09/39.42 cnf(d16, plain, 'Ts151'(X0,X1,'c$ufequal') | sK158(X0,X1,'c$ufequal') = sK159(X0,X1,'c$ufequal'), inference(resolution, [status(thm)], [d15,c362])).
% 141.09/39.42 cnf(d17, plain, sK158(X0,X1,'c$ufequal') != sK158(X0,X1,'c$ufequal') | 'Ts151'(X0,X1,'c$ufequal') | 'Ts151'(X0,X1,'c$ufequal'), inference(superposition, [status(thm)], [d16,c111])).
% 141.09/39.42 cnf(d18, plain, hAPP('c$uCOMBS'(X4,X5,X6,'c$uCOMBK'(X0,X1),X3),X2) = X2, inference(superposition, [status(thm)], [c361,c358])).
% 141.09/39.42 cnf(d19, plain, X6 = hAPP(hAPP('c$uCOMBK'(X3,X4),X6),hAPP(X5,X6)), inference(superposition, [status(thm)], [d18,c361])).
% 141.09/39.42 cnf(d20, plain, X2 = X2, inference(demodulation, [status(thm)], [d19,c358])).
% 141.09/39.42 cnf(d21, plain, 'Ts151'(X0,X1,'c$ufequal'), inference(resolution, [status(thm)], [d20,d17])).
% 141.09/39.42 cnf(d22, plain, 'c$uFinite$u$uSet$uOfinite'(X0,X1), inference(resolution, [status(thm)], [d21,d13])).
% 141.09/39.42 cnf(d23, plain, 'c$uSet$uOimage'(X0,X0,X1,'c$uOrderings$uOtop$u$uclass$uOtop'('tc$ufun'(X0,'tc$uHOL$uObool'))) = 'c$uOrderings$uOtop$u$uclass$uOtop'('tc$ufun'(X0,'tc$uHOL$uObool')) | ~'c$uFun$uOinj$u$uon'(X0,X0,X1,'c$uOrderings$uOtop$u$uclass$uOtop'('tc$ufun'(X0,'tc$uHOL$uObool'))), inference(resolution, [status(thm)], [d22,c345])).
% 141.09/39.42 cnf(d24, plain, ~hBOOL(hAPP('c$uOrderings$uOtop$u$uclass$uOtop'('tc$ufun'(X0,'tc$uHOL$uObool')),X1)) | 'Ts151'(X2,X1,X3) | ~'c$uFun$uOinj$u$uon'(X0,X0,'c$ufequal','c$uOrderings$uOtop$u$uclass$uOtop'('tc$ufun'(X0,'tc$uHOL$uObool'))), inference(superposition, [status(thm)], [d23,d9])).
% 141.09/39.42 cnf(d25, plain, ~'c$uFun$uOinj$u$uon'(X0,X0,'c$ufequal','c$uOrderings$uOtop$u$uclass$uOtop'('tc$ufun'(X0,'tc$uHOL$uObool'))) | 'Ts151'(X1,X2,X3), inference(resolution, [status(thm)], [c22,d24])).
% 141.09/39.42 cnf(d26, plain, ~'c$uFun$uOinj$u$uon'(X0,X1,X2,'c$uOrderings$uOtop$u$uclass$uOtop'('tc$ufun'(X0,'tc$uHOL$uObool'))) | 'c$uFun$uOinj$u$uon'(X0,X1,X2,X3), inference(resolution, [status(thm)], [c229,c228])).
% 141.09/39.42 cnf(d27, plain, 'c$uFun$uOinj$u$uon'(X0,X1,X2,X3) | ~'Ts151'(X0,'c$uOrderings$uOtop$u$uclass$uOtop'('tc$ufun'(X0,'tc$uHOL$uObool')),X2), inference(resolution, [status(thm)], [d26,c106])).
% 141.09/39.42 cnf(d28, plain, 'c$uFun$uOinj$u$uon'(X0,X1,'c$ufequal',X2), inference(resolution, [status(thm)], [d27,d21])).
% 141.09/39.42 cnf(d29, plain, 'Ts151'(X0,X1,X2), inference(resolution, [status(thm)], [d28,d25])).
% 141.09/39.42 cnf(d30, plain, X0 = X1, inference(resolution, [status(thm)], [d29,d2])).
% 141.09/39.42 cnf(d31, plain, $false, inference(resolution, [status(thm)], [d30,c2])).
% 141.09/39.42 % SZS output end CNFRefutation for theBenchmark.p
%------------------------------------------------------------------------------