%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : SCT120+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 : n004.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 47.00s 9.31s
% Output : CNFRefutation 47.00s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SCT120+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.03 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.06/0.56 % Computer : n004.cluster.edu
% 0.06/0.56 % Model : x86_64 x86_64
% 0.06/0.56 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.06/0.56 % Memory : 8046.5625MB
% 0.06/0.56 % OS : Linux 6.8.0-71-generic
% 0.06/0.56 % CPULimit : 300
% 0.06/0.56 % WCLimit : 300
% 0.06/0.56 % DateTime : Sat Sep 26 06:29:53 UTC 2026
% 0.06/0.56 % CPUTime :
% 0.06/0.56 Running casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 47.00/9.31 % SZS status Theorem for theBenchmark.p
% 47.00/9.31 % SZS output start CNFRefutation for theBenchmark.p
% 47.00/9.31 fof(fact_UNIV__I, axiom, ! [X0] : ! [X1] : 'c$umember'(X1,X0,'c$uOrderings$uOtop$u$uclass$uOtop'('tc$ufun'(X1,'tc$uHOL$uObool')))).
% 47.00/9.31 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)))).
% 47.00/9.31 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)))))))))).
% 47.00/9.31 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)))))))).
% 47.00/9.31 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))))) => ('c$uRelation$uOtrans'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt','v$uF'(X0)) & ('c$uRelation$uOirrefl'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt','v$uF'(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')),'v$uF'(X0))))))).
% 47.00/9.31 fof(conj_1, 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)))))))).
% 47.00/9.31 fof(conj_2, 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)))))).
% 47.00/9.31 fof(conj_3, 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'))).
% 47.00/9.31 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'))).
% 47.00/9.31 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])).
% 47.00/9.31 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])).
% 47.00/9.31 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])).
% 47.00/9.31 cnf(c4, plain, ~'c$uRelation$uOtotal$u$uon'(X0,X1,X2) | X3(X0,X1,X2), inference(clausification, [status(esa)], [fact_total__on__def])).
% 47.00/9.31 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])).
% 47.00/9.31 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])).
% 47.00/9.31 cnf(c53, plain, ~'c$uRelation$uOtrans'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt',hAPP(X0,sK100(X0))) | ~'c$uRelation$uOirrefl'('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))) | 'c$uRelation$uOtrans'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt','v$uF'(X0)), inference(clausification, [status(esa)], [conj_0])).
% 47.00/9.31 cnf(c54, plain, ~'c$uRelation$uOtrans'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt',hAPP(X0,sK100(X0))) | ~'c$uRelation$uOirrefl'('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))) | 'c$uRelation$uOirrefl'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt','v$uF'(X0)), inference(clausification, [status(esa)], [conj_0])).
% 47.00/9.31 cnf(c56, plain, X0 = X1 | ~'c$uRelation$uOtrans'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt',hAPP(X2,sK102(X2))) | ~'c$uRelation$uOirrefl'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt',hAPP(X2,sK102(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',X0,X1),hAPP(X2,'v$ui')) | ~'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(X2,sK102(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',X0,X1),'v$uF'(X2)), inference(clausification, [status(esa)], [conj_1])).
% 47.00/9.31 cnf(c57, plain, 'c$uRelation$uOtrans'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt',hAPP('v$uP',X0)), inference(clausification, [status(esa)], [conj_2])).
% 47.00/9.31 cnf(c58, plain, 'c$uRelation$uOirrefl'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt',hAPP('v$uP',X0)), inference(clausification, [status(esa)], [conj_2])).
% 47.00/9.31 cnf(c59, 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_2])).
% 47.00/9.31 cnf(c60, 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_3])).
% 47.00/9.31 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])).
% 47.00/9.31 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)], [c59,c4])).
% 47.00/9.31 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,c60])).
% 47.00/9.31 cnf(d2, plain, ~'c$uRelation$uOirrefl'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt',hAPP('v$uP',sK100('v$uP'))) | ~'c$uRelation$uOtrans'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt',hAPP('v$uP',sK100('v$uP'))) | 'c$uRelation$uOtrans'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt','v$uF'('v$uP')), inference(resolution, [status(thm)], [c53,c59])).
% 47.00/9.31 cnf(d3, plain, ~'c$uRelation$uOirrefl'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt',hAPP('v$uP',sK100('v$uP'))) | 'c$uRelation$uOtrans'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt','v$uF'('v$uP')), inference(resolution, [status(thm)], [c57,d2])).
% 47.00/9.31 cnf(d4, plain, 'c$uRelation$uOtrans'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt','v$uF'('v$uP')), inference(resolution, [status(thm)], [c58,d3])).
% 47.00/9.31 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])).
% 47.00/9.31 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])).
% 47.00/9.31 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',sK102('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',sK102('v$uP'))) | ~'c$uRelation$uOtrans'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt',hAPP('v$uP',sK102('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)], [c56,d6])).
% 47.00/9.31 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',sK102('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',sK102('v$uP'))) | ~'Ts9'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt',X0,hAPP('v$uP','v$ui')), inference(resolution, [status(thm)], [c57,d7])).
% 47.00/9.31 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',sK102('v$uP'))) | ~'Ts9'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt',X0,hAPP('v$uP','v$ui')), inference(resolution, [status(thm)], [c58,d8])).
% 47.00/9.31 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)], [c59,d9])).
% 47.00/9.31 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])).
% 47.00/9.31 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])).
% 47.00/9.31 cnf(d13, plain, ~'c$uRelation$uOirrefl'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt',hAPP('v$uP',sK100('v$uP'))) | 'c$uRelation$uOirrefl'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt','v$uF'('v$uP')) | ~'c$uRelation$uOtrans'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt',hAPP('v$uP',sK100('v$uP'))), inference(resolution, [status(thm)], [c54,c59])).
% 47.00/9.31 cnf(d14, plain, ~'c$uRelation$uOirrefl'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt',hAPP('v$uP',sK100('v$uP'))) | 'c$uRelation$uOirrefl'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt','v$uF'('v$uP')), inference(resolution, [status(thm)], [c57,d13])).
% 47.00/9.31 cnf(d15, plain, 'c$uRelation$uOirrefl'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt','v$uF'('v$uP')), inference(resolution, [status(thm)], [c58,d14])).
% 47.00/9.31 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])).
% 47.00/9.31 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])).
% 47.00/9.31 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])).
% 47.00/9.31 cnf(d19, plain, 'v$ua' = 'v$ub' | 'v$ub' = 'v$ua', inference(resolution, [status(thm)], [d18,c1])).
% 47.00/9.31 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,c60])).
% 47.00/9.31 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])).
% 47.00/9.31 cnf(d22, plain, 'v$ua' = 'v$ub', inference(resolution, [status(thm)], [d15,d21])).
% 47.00/9.31 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)], [c60,d22])).
% 47.00/9.31 cnf(d24, plain, ~'c$uRelation$uOirrefl'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt','v$uF'('v$uP')), inference(resolution, [status(thm)], [d23,c2])).
% 47.00/9.31 cnf(d25, plain, $false, inference(resolution, [status(thm)], [d15,d24])).
% 47.00/9.31 % SZS output end CNFRefutation for theBenchmark.p
%------------------------------------------------------------------------------