%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : SCT121+1 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/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 08:27:48 AM UTC 2026
% Result : Theorem 56.98s 8.97s
% Output : CNFRefutation 56.98s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SCT121+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.04 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.36 % Computer : n006.cluster.edu
% 0.08/0.36 % Model : x86_64 x86_64
% 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36 % Memory : 8046.5625MB
% 0.08/0.36 % OS : Linux 6.8.0-71-generic
% 0.08/0.36 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.08/0.36 % DateTime : Sat Sep 26 06:30:14 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.08/0.36 Running casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 56.98/8.97 % SZS status Theorem for theBenchmark.p
% 56.98/8.97 % SZS output start CNFRefutation for theBenchmark.p
% 56.98/8.97 fof(fact_UNIV__I, axiom, ! [X0] : ! [X1] : 'c$umember'(X1,X0,'c$uOrderings$uOtop$u$uclass$uOtop'('tc$ufun'(X1,'tc$uHOL$uObool')))).
% 56.98/8.97 fof(fact_irrefl__def, axiom, ! [X0] : ! [X1] : (('c$uRelation$uOirrefl'(X1,X0) <=> ! [X2] : ~'c$umember'('tc$uprod'(X1,X1),'c$uProduct$u$uType$uOPair'(X1,X1,X2,X2),X0)))).
% 56.98/8.97 fof(fact_total__on__def, axiom, ! [X0] : ! [X1] : ! [X2] : (('c$uRelation$uOtotal$u$uon'(X2,X1,X0) <=> ! [X3] : (('c$umember'(X2,X3,X1) => ! [X4] : (('c$umember'(X2,X4,X1) => (X3 != X4 => ('c$umember'('tc$uprod'(X2,X2),'c$uProduct$u$uType$uOPair'(X2,X2,X3,X4),X0) | 'c$umember'('tc$uprod'(X2,X2),'c$uProduct$u$uType$uOPair'(X2,X2,X4,X3),X0)))))))))).
% 56.98/8.97 fof(fact_trans__def, axiom, ! [X0] : ! [X1] : (('c$uRelation$uOtrans'(X1,X0) <=> ! [X2] : ! [X3] : (('c$umember'('tc$uprod'(X1,X1),'c$uProduct$u$uType$uOPair'(X1,X1,X2,X3),X0) => ! [X4] : (('c$umember'('tc$uprod'(X1,X1),'c$uProduct$u$uType$uOPair'(X1,X1,X3,X4),X0) => 'c$umember'('tc$uprod'(X1,X1),'c$uProduct$u$uType$uOPair'(X1,X1,X2,X4),X0)))))))).
% 56.98/8.97 fof(conj_0, hypothesis, ! [X0] : ((! [X1] : (('c$uRelation$uOtrans'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt',hAPP(X0,X1)) & ('c$uRelation$uOirrefl'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt',hAPP(X0,X1)) & 'c$uRelation$uOtotal$u$uon'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt','c$uOrderings$uOtop$u$uclass$uOtop'('tc$ufun'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt','tc$uHOL$uObool')),hAPP(X0,X1))))) => ! [X2] : ! [X3] : ((X2 != X3 => ('c$umember'('tc$uprod'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt','tc$uArrow$u$uOrder$u$uMirabelle$uOalt'),'c$uProduct$u$uType$uOPair'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt','tc$uArrow$u$uOrder$u$uMirabelle$uOalt',X2,X3),hAPP(X0,'v$ui')) => 'c$umember'('tc$uprod'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt','tc$uArrow$u$uOrder$u$uMirabelle$uOalt'),'c$uProduct$u$uType$uOPair'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt','tc$uArrow$u$uOrder$u$uMirabelle$uOalt',X2,X3),'v$uF'(X0)))))))).
% 56.98/8.97 fof(conj_1, hypothesis, ! [X0] : (('c$uRelation$uOtrans'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt',hAPP('v$uP',X0)) & ('c$uRelation$uOirrefl'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt',hAPP('v$uP',X0)) & 'c$uRelation$uOtotal$u$uon'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt','c$uOrderings$uOtop$u$uclass$uOtop'('tc$ufun'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt','tc$uHOL$uObool')),hAPP('v$uP',X0)))))).
% 56.98/8.97 fof(conj_2, hypothesis, 'c$umember'('tc$uprod'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt','tc$uArrow$u$uOrder$u$uMirabelle$uOalt'),'c$uProduct$u$uType$uOPair'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt','tc$uArrow$u$uOrder$u$uMirabelle$uOalt','v$ua','v$ub'),'v$uF'('v$uP'))).
% 56.98/8.97 fof(conj_3, hypothesis, (! [X0] : (('c$uRelation$uOtrans'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt',hAPP('v$uP',X0)) & ('c$uRelation$uOirrefl'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt',hAPP('v$uP',X0)) & 'c$uRelation$uOtotal$u$uon'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt','c$uOrderings$uOtop$u$uclass$uOtop'('tc$ufun'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt','tc$uHOL$uObool')),hAPP('v$uP',X0))))) => ('c$uRelation$uOtrans'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt','v$uF'('v$uP')) & ('c$uRelation$uOirrefl'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt','v$uF'('v$uP')) & 'c$uRelation$uOtotal$u$uon'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt','c$uOrderings$uOtop$u$uclass$uOtop'('tc$ufun'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt','tc$uHOL$uObool')),'v$uF'('v$uP')))))).
% 56.98/8.97 fof(conj_4, conjecture, 'c$umember'('tc$uprod'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt','tc$uArrow$u$uOrder$u$uMirabelle$uOalt'),'c$uProduct$u$uType$uOPair'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt','tc$uArrow$u$uOrder$u$uMirabelle$uOalt','v$ua','v$ub'),hAPP('v$uP','v$ui'))).
% 56.98/8.97 fof(negated_conjecture, negated_conjecture, ~'c$umember'('tc$uprod'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt','tc$uArrow$u$uOrder$u$uMirabelle$uOalt'),'c$uProduct$u$uType$uOPair'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt','tc$uArrow$u$uOrder$u$uMirabelle$uOalt','v$ua','v$ub'),hAPP('v$uP','v$ui')), inference(negate_conjecture, [status(cth)], [conj_4])).
% 56.98/8.97 cnf(c1, plain, 'c$umember'(X0,X1,'c$uOrderings$uOtop$u$uclass$uOtop'('tc$ufun'(X0,'tc$uHOL$uObool'))), inference(clausification, [status(esa)], [fact_UNIV__I])).
% 56.98/8.97 cnf(c2, plain, ~'c$uRelation$uOirrefl'(X0,X1) | ~'c$umember'('tc$uprod'(X0,X0),'c$uProduct$u$uType$uOPair'(X0,X0,X2,X2),X1), inference(clausification, [status(esa)], [fact_irrefl__def])).
% 56.98/8.97 cnf(c4, plain, ~'c$uRelation$uOtotal$u$uon'(X0,X1,X2) | X3(X0,X1,X2), inference(clausification, [status(esa)], [fact_total__on__def])).
% 56.98/8.97 cnf(c6, plain, X0 = X1 | ~'c$umember'(X2,X0,X3) | ~X4(X2,X3,X5) | ~'c$umember'(X2,X1,X3) | 'c$umember'('tc$uprod'(X2,X2),'c$uProduct$u$uType$uOPair'(X2,X2,X1,X0),X5) | 'c$umember'('tc$uprod'(X2,X2),'c$uProduct$u$uType$uOPair'(X2,X2,X0,X1),X5), inference(clausification, [status(esa)], [fact_total__on__def])).
% 56.98/8.97 cnf(c12, plain, ~'c$uRelation$uOtrans'(X0,X1) | ~'c$umember'('tc$uprod'(X0,X0),'c$uProduct$u$uType$uOPair'(X0,X0,X2,X3),X1) | ~'c$umember'('tc$uprod'(X0,X0),'c$uProduct$u$uType$uOPair'(X0,X0,X3,X4),X1) | 'c$umember'('tc$uprod'(X0,X0),'c$uProduct$u$uType$uOPair'(X0,X0,X2,X4),X1), inference(clausification, [status(esa)], [fact_trans__def])).
% 56.98/8.97 cnf(c53, plain, ~'c$uRelation$uOtrans'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt',hAPP(X0,sK100(X0))) | ~'c$uRelation$uOtotal$u$uon'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt','c$uOrderings$uOtop$u$uclass$uOtop'('tc$ufun'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt','tc$uHOL$uObool')),hAPP(X0,sK100(X0))) | X1 = X2 | ~'c$umember'('tc$uprod'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt','tc$uArrow$u$uOrder$u$uMirabelle$uOalt'),'c$uProduct$u$uType$uOPair'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt','tc$uArrow$u$uOrder$u$uMirabelle$uOalt',X1,X2),hAPP(X0,'v$ui')) | 'c$umember'('tc$uprod'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt','tc$uArrow$u$uOrder$u$uMirabelle$uOalt'),'c$uProduct$u$uType$uOPair'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt','tc$uArrow$u$uOrder$u$uMirabelle$uOalt',X1,X2),'v$uF'(X0)) | ~'c$uRelation$uOirrefl'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt',hAPP(X0,sK100(X0))), inference(clausification, [status(esa)], [conj_0])).
% 56.98/8.97 cnf(c54, plain, 'c$uRelation$uOtrans'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt',hAPP('v$uP',X0)), inference(clausification, [status(esa)], [conj_1])).
% 56.98/8.97 cnf(c55, plain, 'c$uRelation$uOirrefl'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt',hAPP('v$uP',X0)), inference(clausification, [status(esa)], [conj_1])).
% 56.98/8.97 cnf(c56, plain, 'c$uRelation$uOtotal$u$uon'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt','c$uOrderings$uOtop$u$uclass$uOtop'('tc$ufun'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt','tc$uHOL$uObool')),hAPP('v$uP',X0)), inference(clausification, [status(esa)], [conj_1])).
% 56.98/8.97 cnf(c57, plain, 'c$umember'('tc$uprod'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt','tc$uArrow$u$uOrder$u$uMirabelle$uOalt'),'c$uProduct$u$uType$uOPair'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt','tc$uArrow$u$uOrder$u$uMirabelle$uOalt','v$ua','v$ub'),'v$uF'('v$uP')), inference(clausification, [status(esa)], [conj_2])).
% 56.98/8.97 cnf(c58, plain, ~'c$uRelation$uOtrans'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt',hAPP('v$uP',sK104)) | ~'c$uRelation$uOirrefl'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt',hAPP('v$uP',sK104)) | ~'c$uRelation$uOtotal$u$uon'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt','c$uOrderings$uOtop$u$uclass$uOtop'('tc$ufun'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt','tc$uHOL$uObool')),hAPP('v$uP',sK104)) | 'c$uRelation$uOtrans'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt','v$uF'('v$uP')), inference(clausification, [status(esa)], [conj_3])).
% 56.98/8.97 cnf(c59, plain, ~'c$uRelation$uOtrans'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt',hAPP('v$uP',sK104)) | ~'c$uRelation$uOirrefl'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt',hAPP('v$uP',sK104)) | ~'c$uRelation$uOtotal$u$uon'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt','c$uOrderings$uOtop$u$uclass$uOtop'('tc$ufun'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt','tc$uHOL$uObool')),hAPP('v$uP',sK104)) | 'c$uRelation$uOirrefl'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt','v$uF'('v$uP')), inference(clausification, [status(esa)], [conj_3])).
% 56.98/8.97 cnf(c61, plain, ~'c$umember'('tc$uprod'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt','tc$uArrow$u$uOrder$u$uMirabelle$uOalt'),'c$uProduct$u$uType$uOPair'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt','tc$uArrow$u$uOrder$u$uMirabelle$uOalt','v$ua','v$ub'),hAPP('v$uP','v$ui')), inference(clausification, [status(esa)], [negated_conjecture])).
% 56.98/8.97 cnf(d0, plain, 'Ts9'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt','c$uOrderings$uOtop$u$uclass$uOtop'('tc$ufun'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt','tc$uHOL$uObool')),hAPP('v$uP',X0)), inference(resolution, [status(thm)], [c56,c4])).
% 56.98/8.97 cnf(d1, plain, 'c$umember'('tc$uprod'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt','tc$uArrow$u$uOrder$u$uMirabelle$uOalt'),'c$uProduct$u$uType$uOPair'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt','tc$uArrow$u$uOrder$u$uMirabelle$uOalt',X0,'v$ub'),'v$uF'('v$uP')) | ~'c$umember'('tc$uprod'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt','tc$uArrow$u$uOrder$u$uMirabelle$uOalt'),'c$uProduct$u$uType$uOPair'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt','tc$uArrow$u$uOrder$u$uMirabelle$uOalt',X0,'v$ua'),'v$uF'('v$uP')) | ~'c$uRelation$uOtrans'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt','v$uF'('v$uP')), inference(resolution, [status(thm)], [c12,c57])).
% 56.98/8.97 cnf(d2, plain, ~'c$uRelation$uOirrefl'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt',hAPP('v$uP',sK104)) | ~'c$uRelation$uOtotal$u$uon'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt','c$uOrderings$uOtop$u$uclass$uOtop'('tc$ufun'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt','tc$uHOL$uObool')),hAPP('v$uP',sK104)) | 'c$uRelation$uOtrans'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt','v$uF'('v$uP')), inference(resolution, [status(thm)], [c54,c58])).
% 56.98/8.97 cnf(d3, plain, ~'c$uRelation$uOtotal$u$uon'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt','c$uOrderings$uOtop$u$uclass$uOtop'('tc$ufun'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt','tc$uHOL$uObool')),hAPP('v$uP',sK104)) | 'c$uRelation$uOtrans'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt','v$uF'('v$uP')), inference(resolution, [status(thm)], [c55,d2])).
% 56.98/8.97 cnf(d4, plain, 'c$uRelation$uOtrans'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt','v$uF'('v$uP')), inference(resolution, [status(thm)], [c56,d3])).
% 56.98/8.97 cnf(d5, plain, ~'c$umember'('tc$uprod'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt','tc$uArrow$u$uOrder$u$uMirabelle$uOalt'),'c$uProduct$u$uType$uOPair'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt','tc$uArrow$u$uOrder$u$uMirabelle$uOalt',X0,'v$ua'),'v$uF'('v$uP')) | 'c$umember'('tc$uprod'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt','tc$uArrow$u$uOrder$u$uMirabelle$uOalt'),'c$uProduct$u$uType$uOPair'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt','tc$uArrow$u$uOrder$u$uMirabelle$uOalt',X0,'v$ub'),'v$uF'('v$uP')), inference(resolution, [status(thm)], [d4,d1])).
% 56.98/8.97 cnf(d6, plain, 'v$ua' = 'v$ub' | ~'c$umember'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt','v$ub',X0) | ~'c$umember'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt','v$ua',X0) | 'c$umember'('tc$uprod'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt','tc$uArrow$u$uOrder$u$uMirabelle$uOalt'),'c$uProduct$u$uType$uOPair'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt','tc$uArrow$u$uOrder$u$uMirabelle$uOalt','v$ub','v$ua'),hAPP('v$uP','v$ui')) | ~'Ts9'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt',X0,hAPP('v$uP','v$ui')), inference(resolution, [status(thm)], [c6,c61])).
% 56.98/8.97 cnf(d7, plain, 'v$ub' = 'v$ua' | 'c$umember'('tc$uprod'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt','tc$uArrow$u$uOrder$u$uMirabelle$uOalt'),'c$uProduct$u$uType$uOPair'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt','tc$uArrow$u$uOrder$u$uMirabelle$uOalt','v$ub','v$ua'),'v$uF'('v$uP')) | ~'c$uRelation$uOirrefl'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt',hAPP('v$uP',sK100('v$uP'))) | ~'c$uRelation$uOtotal$u$uon'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt','c$uOrderings$uOtop$u$uclass$uOtop'('tc$ufun'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt','tc$uHOL$uObool')),hAPP('v$uP',sK100('v$uP'))) | ~'c$uRelation$uOtrans'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt',hAPP('v$uP',sK100('v$uP'))) | 'v$ua' = 'v$ub' | ~'c$umember'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt','v$ua',X0) | ~'c$umember'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt','v$ub',X0) | ~'Ts9'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt',X0,hAPP('v$uP','v$ui')), inference(resolution, [status(thm)], [c53,d6])).
% 56.98/8.97 cnf(d8, plain, 'v$ua' = 'v$ub' | 'v$ub' = 'v$ua' | 'c$umember'('tc$uprod'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt','tc$uArrow$u$uOrder$u$uMirabelle$uOalt'),'c$uProduct$u$uType$uOPair'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt','tc$uArrow$u$uOrder$u$uMirabelle$uOalt','v$ub','v$ua'),'v$uF'('v$uP')) | ~'c$umember'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt','v$ua',X0) | ~'c$umember'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt','v$ub',X0) | ~'c$uRelation$uOirrefl'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt',hAPP('v$uP',sK100('v$uP'))) | ~'c$uRelation$uOtotal$u$uon'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt','c$uOrderings$uOtop$u$uclass$uOtop'('tc$ufun'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt','tc$uHOL$uObool')),hAPP('v$uP',sK100('v$uP'))) | ~'Ts9'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt',X0,hAPP('v$uP','v$ui')), inference(resolution, [status(thm)], [c54,d7])).
% 56.98/8.97 cnf(d9, plain, 'v$ua' = 'v$ub' | 'v$ub' = 'v$ua' | 'c$umember'('tc$uprod'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt','tc$uArrow$u$uOrder$u$uMirabelle$uOalt'),'c$uProduct$u$uType$uOPair'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt','tc$uArrow$u$uOrder$u$uMirabelle$uOalt','v$ub','v$ua'),'v$uF'('v$uP')) | ~'c$umember'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt','v$ua',X0) | ~'c$umember'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt','v$ub',X0) | ~'c$uRelation$uOtotal$u$uon'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt','c$uOrderings$uOtop$u$uclass$uOtop'('tc$ufun'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt','tc$uHOL$uObool')),hAPP('v$uP',sK100('v$uP'))) | ~'Ts9'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt',X0,hAPP('v$uP','v$ui')), inference(resolution, [status(thm)], [c55,d8])).
% 56.98/8.97 cnf(d10, plain, 'v$ua' = 'v$ub' | 'v$ub' = 'v$ua' | 'c$umember'('tc$uprod'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt','tc$uArrow$u$uOrder$u$uMirabelle$uOalt'),'c$uProduct$u$uType$uOPair'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt','tc$uArrow$u$uOrder$u$uMirabelle$uOalt','v$ub','v$ua'),'v$uF'('v$uP')) | ~'c$umember'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt','v$ua',X0) | ~'c$umember'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt','v$ub',X0) | ~'Ts9'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt',X0,hAPP('v$uP','v$ui')), inference(resolution, [status(thm)], [c56,d9])).
% 56.98/8.97 cnf(d11, plain, 'v$ua' = 'v$ub' | 'v$ub' = 'v$ua' | ~'c$umember'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt','v$ua',X0) | ~'c$umember'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt','v$ub',X0) | ~'Ts9'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt',X0,hAPP('v$uP','v$ui')) | 'c$umember'('tc$uprod'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt','tc$uArrow$u$uOrder$u$uMirabelle$uOalt'),'c$uProduct$u$uType$uOPair'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt','tc$uArrow$u$uOrder$u$uMirabelle$uOalt','v$ub','v$ub'),'v$uF'('v$uP')), inference(resolution, [status(thm)], [d10,d5])).
% 56.98/8.97 cnf(d12, plain, 'v$ua' = 'v$ub' | 'v$ub' = 'v$ua' | ~'c$umember'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt','v$ua',X0) | ~'c$umember'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt','v$ub',X0) | ~'Ts9'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt',X0,hAPP('v$uP','v$ui')) | ~'c$uRelation$uOirrefl'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt','v$uF'('v$uP')), inference(resolution, [status(thm)], [d11,c2])).
% 56.98/8.97 cnf(d13, plain, ~'c$uRelation$uOirrefl'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt',hAPP('v$uP',sK104)) | 'c$uRelation$uOirrefl'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt','v$uF'('v$uP')) | ~'c$uRelation$uOtotal$u$uon'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt','c$uOrderings$uOtop$u$uclass$uOtop'('tc$ufun'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt','tc$uHOL$uObool')),hAPP('v$uP',sK104)), inference(resolution, [status(thm)], [c54,c59])).
% 56.98/8.97 cnf(d14, plain, 'c$uRelation$uOirrefl'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt','v$uF'('v$uP')) | ~'c$uRelation$uOtotal$u$uon'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt','c$uOrderings$uOtop$u$uclass$uOtop'('tc$ufun'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt','tc$uHOL$uObool')),hAPP('v$uP',sK104)), inference(resolution, [status(thm)], [c55,d13])).
% 56.98/8.97 cnf(d15, plain, 'c$uRelation$uOirrefl'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt','v$uF'('v$uP')), inference(resolution, [status(thm)], [c56,d14])).
% 56.98/8.97 cnf(d16, plain, 'v$ua' = 'v$ub' | 'v$ub' = 'v$ua' | ~'c$umember'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt','v$ua',X0) | ~'c$umember'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt','v$ub',X0) | ~'Ts9'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt',X0,hAPP('v$uP','v$ui')), inference(resolution, [status(thm)], [d15,d12])).
% 56.98/8.97 cnf(d17, plain, 'v$ua' = 'v$ub' | 'v$ub' = 'v$ua' | ~'c$umember'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt','v$ua','c$uOrderings$uOtop$u$uclass$uOtop'('tc$ufun'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt','tc$uHOL$uObool'))) | ~'c$umember'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt','v$ub','c$uOrderings$uOtop$u$uclass$uOtop'('tc$ufun'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt','tc$uHOL$uObool'))), inference(resolution, [status(thm)], [d16,d0])).
% 56.98/8.97 cnf(d18, plain, 'v$ua' = 'v$ub' | 'v$ub' = 'v$ua' | ~'c$umember'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt','v$ub','c$uOrderings$uOtop$u$uclass$uOtop'('tc$ufun'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt','tc$uHOL$uObool'))), inference(resolution, [status(thm)], [c1,d17])).
% 56.98/8.97 cnf(d19, plain, 'v$ua' = 'v$ub' | 'v$ub' = 'v$ua', inference(resolution, [status(thm)], [d18,c1])).
% 56.98/8.97 cnf(d20, plain, 'c$umember'('tc$uprod'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt','tc$uArrow$u$uOrder$u$uMirabelle$uOalt'),'c$uProduct$u$uType$uOPair'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt','tc$uArrow$u$uOrder$u$uMirabelle$uOalt','v$ua','v$ua'),'v$uF'('v$uP')) | 'v$ua' = 'v$ub', inference(superposition, [status(thm)], [d19,c57])).
% 56.98/8.97 cnf(d21, plain, 'v$ua' = 'v$ub' | ~'c$uRelation$uOirrefl'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt','v$uF'('v$uP')), inference(resolution, [status(thm)], [d20,c2])).
% 56.98/8.97 cnf(d22, plain, 'v$ua' = 'v$ub', inference(resolution, [status(thm)], [d15,d21])).
% 56.98/8.97 cnf(d23, plain, 'c$umember'('tc$uprod'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt','tc$uArrow$u$uOrder$u$uMirabelle$uOalt'),'c$uProduct$u$uType$uOPair'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt','tc$uArrow$u$uOrder$u$uMirabelle$uOalt','v$ua','v$ua'),'v$uF'('v$uP')), inference(demodulation, [status(thm)], [c57,d22])).
% 56.98/8.97 cnf(d24, plain, ~'c$uRelation$uOirrefl'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt','v$uF'('v$uP')), inference(resolution, [status(thm)], [d23,c2])).
% 56.98/8.97 cnf(d25, plain, $false, inference(resolution, [status(thm)], [d15,d24])).
% 56.98/8.97 % SZS output end CNFRefutation for theBenchmark.p
%------------------------------------------------------------------------------