%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : SCT158+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 : n015.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:51 AM UTC 2026
% Result : Theorem 42.72s 7.25s
% Output : CNFRefutation 42.72s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SCT158+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/0.35 % Computer : n015.cluster.edu
% 0.10/0.35 % Model : x86_64 x86_64
% 0.10/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.35 % Memory : 8046.5625MB
% 0.10/0.35 % OS : Linux 6.8.0-71-generic
% 0.10/0.35 % CPULimit : 300
% 0.10/0.35 % WCLimit : 300
% 0.10/0.35 % DateTime : Sat Sep 26 06:37:14 UTC 2026
% 0.10/0.35 % CPUTime :
% 0.10/0.35 Running casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 42.72/7.25 % SZS status Theorem for theBenchmark.p
% 42.72/7.25 % SZS output start CNFRefutation for theBenchmark.p
% 42.72/7.25 fof(fact_A_I1_J, axiom, 'v$ua' != 'v$ub').
% 42.72/7.25 fof(fact_A_I2_J, axiom, 'v$ua$uH' != 'v$ub$uH').
% 42.72/7.25 fof(fact__096a_A_061_Ab_H_A_G_Ab_A_061_Aa_H_096, axiom, ('v$ua' = 'v$ub$uH' & 'v$ub' = 'v$ua$uH')).
% 42.72/7.25 fof(fact_A_I5_J, axiom, ! [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$ua','v$ub'),hAPP('v$uP',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$ua$uH','v$ub$uH'),hAPP('v$uP$uH',X0))))).
% 42.72/7.25 fof(fact_A_I3_J, axiom, 'c$umember'('tc$ufun'('tc$uArrow$u$uOrder$u$uMirabelle$uOindi','tc$ufun'('tc$uprod'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt','tc$uArrow$u$uOrder$u$uMirabelle$uOalt'),'tc$uHOL$uObool')),'v$uP','c$uArrow$u$uOrder$u$uMirabelle$uOProf')).
% 42.72/7.25 fof(fact_A_I4_J, axiom, 'c$umember'('tc$ufun'('tc$uArrow$u$uOrder$u$uMirabelle$uOindi','tc$ufun'('tc$uprod'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt','tc$uArrow$u$uOrder$u$uMirabelle$uOalt'),'tc$uHOL$uObool')),'v$uP$uH','c$uArrow$u$uOrder$u$uMirabelle$uOProf')).
% 42.72/7.25 fof(fact__C3_C, axiom, ! [X0] : ! [X1] : ! [X2] : ! [X3] : ((X3 != X2 => ('c$umember'('tc$ufun'('tc$uArrow$u$uOrder$u$uMirabelle$uOindi','tc$ufun'('tc$uprod'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt','tc$uArrow$u$uOrder$u$uMirabelle$uOalt'),'tc$uHOL$uObool')),X1,'c$uArrow$u$uOrder$u$uMirabelle$uOProf') => ('c$umember'('tc$ufun'('tc$uArrow$u$uOrder$u$uMirabelle$uOindi','tc$ufun'('tc$uprod'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt','tc$uArrow$u$uOrder$u$uMirabelle$uOalt'),'tc$uHOL$uObool')),X0,'c$uArrow$u$uOrder$u$uMirabelle$uOProf') => (! [X4] : (('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',X3,X2),hAPP(X1,X4)) <=> '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,X4)))) => ('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',X3,X2),hAPP('v$uF',X1)) <=> '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('v$uF',X0))))))))).
% 42.72/7.25 fof(conj_0, 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$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','v$ua$uH','v$ub$uH'),hAPP('v$uF','v$uP$uH')))).
% 42.72/7.25 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$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','v$ua$uH','v$ub$uH'),hAPP('v$uF','v$uP$uH')))), inference(negate_conjecture, [status(cth)], [conj_0])).
% 42.72/7.25 cnf(c1, plain, 'v$ub' != 'v$ua', inference(clausification, [status(esa)], [fact_A_I1_J])).
% 42.72/7.25 cnf(c2, plain, 'v$ub$uH' != 'v$ua$uH', inference(clausification, [status(esa)], [fact_A_I2_J])).
% 42.72/7.25 cnf(c3, plain, 'v$ub$uH' = 'v$ua', inference(clausification, [status(esa)], [fact__096a_A_061_Ab_H_A_G_Ab_A_061_Aa_H_096])).
% 42.72/7.25 cnf(c4, plain, 'v$ua$uH' = 'v$ub', inference(clausification, [status(esa)], [fact__096a_A_061_Ab_H_A_G_Ab_A_061_Aa_H_096])).
% 42.72/7.25 cnf(c5, 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',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$ua$uH','v$ub$uH'),hAPP('v$uP$uH',X0)), inference(clausification, [status(esa)], [fact_A_I5_J])).
% 42.72/7.25 cnf(c6, 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',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$ua$uH','v$ub$uH'),hAPP('v$uP$uH',X0)), inference(clausification, [status(esa)], [fact_A_I5_J])).
% 42.72/7.25 cnf(c13, plain, 'c$umember'('tc$ufun'('tc$uArrow$u$uOrder$u$uMirabelle$uOindi','tc$ufun'('tc$uprod'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt','tc$uArrow$u$uOrder$u$uMirabelle$uOalt'),'tc$uHOL$uObool')),'v$uP','c$uArrow$u$uOrder$u$uMirabelle$uOProf'), inference(clausification, [status(esa)], [fact_A_I3_J])).
% 42.72/7.25 cnf(c14, plain, 'c$umember'('tc$ufun'('tc$uArrow$u$uOrder$u$uMirabelle$uOindi','tc$ufun'('tc$uprod'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt','tc$uArrow$u$uOrder$u$uMirabelle$uOalt'),'tc$uHOL$uObool')),'v$uP$uH','c$uArrow$u$uOrder$u$uMirabelle$uOProf'), inference(clausification, [status(esa)], [fact_A_I4_J])).
% 42.72/7.25 cnf(c19, 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,X1),hAPP('v$uF',X2)) | ~'c$umember'('tc$ufun'('tc$uArrow$u$uOrder$u$uMirabelle$uOindi','tc$ufun'('tc$uprod'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt','tc$uArrow$u$uOrder$u$uMirabelle$uOalt'),'tc$uHOL$uObool')),X3,'c$uArrow$u$uOrder$u$uMirabelle$uOProf') | X0 = X1 | ~'c$umember'('tc$ufun'('tc$uArrow$u$uOrder$u$uMirabelle$uOindi','tc$ufun'('tc$uprod'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt','tc$uArrow$u$uOrder$u$uMirabelle$uOalt'),'tc$uHOL$uObool')),X2,'c$uArrow$u$uOrder$u$uMirabelle$uOProf') | X4(X2,X3,X1,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',X1,X0),hAPP('v$uF',X3)), inference(clausification, [status(esa)], [fact__C3_C])).
% 42.72/7.25 cnf(c22, plain, ~X0(X1,X2,X3,X4) | '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',X3,X4),hAPP(X2,sK13(X4,X1,X3,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',X4,X3),hAPP(X1,sK13(X4,X1,X3,X2))), inference(clausification, [status(esa)], [fact__C3_C])).
% 42.72/7.25 cnf(c23, plain, ~X0(X1,X2,X3,X4) | ~'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',X4,X3),hAPP(X1,sK13(X4,X1,X3,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',X3,X4),hAPP(X2,sK13(X4,X1,X3,X2))), inference(clausification, [status(esa)], [fact__C3_C])).
% 42.72/7.25 cnf(c52, 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$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','v$ua$uH','v$ub$uH'),hAPP('v$uF','v$uP$uH')), inference(clausification, [status(esa)], [negated_conjecture])).
% 42.72/7.25 cnf(c53, 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$uH','v$ub$uH'),hAPP('v$uF','v$uP$uH')) | ~'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$uF','v$uP')), inference(clausification, [status(esa)], [negated_conjecture])).
% 42.72/7.25 cnf(d0, 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',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$ub$uH'),hAPP('v$uP$uH',X0)), inference(demodulation, [status(thm)], [c5,c4])).
% 42.72/7.25 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','v$ua','v$ub'),hAPP('v$uP',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$uH',X0)), inference(demodulation, [status(thm)], [d0,c3])).
% 42.72/7.25 cnf(d2, 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',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$ub$uH'),hAPP('v$uP$uH',X0)), inference(demodulation, [status(thm)], [c6,c4])).
% 42.72/7.25 cnf(d3, 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',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$uH',X0)), inference(demodulation, [status(thm)], [d2,c3])).
% 42.72/7.25 cnf(d4, 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$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','v$ub','v$ub$uH'),hAPP('v$uF','v$uP$uH')), inference(demodulation, [status(thm)], [c52,c4])).
% 42.72/7.25 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','v$ua','v$ub'),hAPP('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','v$ub','v$ua'),hAPP('v$uF','v$uP$uH')), inference(demodulation, [status(thm)], [d4,c3])).
% 42.72/7.25 cnf(d6, 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'),hAPP('v$uF',X0)) | ~'c$umember'('tc$ufun'('tc$uArrow$u$uOrder$u$uMirabelle$uOindi','tc$ufun'('tc$uprod'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt','tc$uArrow$u$uOrder$u$uMirabelle$uOalt'),'tc$uHOL$uObool')),X0,'c$uArrow$u$uOrder$u$uMirabelle$uOProf') | ~'c$umember'('tc$ufun'('tc$uArrow$u$uOrder$u$uMirabelle$uOindi','tc$ufun'('tc$uprod'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt','tc$uArrow$u$uOrder$u$uMirabelle$uOalt'),'tc$uHOL$uObool')),'v$uP','c$uArrow$u$uOrder$u$uMirabelle$uOProf') | 'Ts8'(X0,'v$uP','v$ua','v$ub') | '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$uF','v$uP$uH')), inference(resolution, [status(thm)], [c19,d5])).
% 42.72/7.25 cnf(d7, 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$ub','v$ua'),hAPP('v$uF',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$uF','v$uP$uH')) | ~'c$umember'('tc$ufun'('tc$uArrow$u$uOrder$u$uMirabelle$uOindi','tc$ufun'('tc$uprod'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt','tc$uArrow$u$uOrder$u$uMirabelle$uOalt'),'tc$uHOL$uObool')),X0,'c$uArrow$u$uOrder$u$uMirabelle$uOProf') | ~'c$umember'('tc$ufun'('tc$uArrow$u$uOrder$u$uMirabelle$uOindi','tc$ufun'('tc$uprod'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt','tc$uArrow$u$uOrder$u$uMirabelle$uOalt'),'tc$uHOL$uObool')),'v$uP','c$uArrow$u$uOrder$u$uMirabelle$uOProf') | 'Ts8'(X0,'v$uP','v$ua','v$ub'), inference(resolution, [status(thm)], [c1,d6])).
% 42.72/7.25 cnf(d8, 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$ub','v$ua'),hAPP('v$uF',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$uF','v$uP$uH')) | ~'c$umember'('tc$ufun'('tc$uArrow$u$uOrder$u$uMirabelle$uOindi','tc$ufun'('tc$uprod'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt','tc$uArrow$u$uOrder$u$uMirabelle$uOalt'),'tc$uHOL$uObool')),X0,'c$uArrow$u$uOrder$u$uMirabelle$uOProf') | 'Ts8'(X0,'v$uP','v$ua','v$ub'), inference(resolution, [status(thm)], [c13,d7])).
% 42.72/7.25 cnf(d9, 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$ub','v$ua'),hAPP('v$uF','v$uP$uH')) | '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$uF','v$uP$uH')) | 'Ts8'('v$uP$uH','v$uP','v$ua','v$ub'), inference(resolution, [status(thm)], [d8,c14])).
% 42.72/7.25 cnf(d10, 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$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','v$ub','v$ub$uH'),hAPP('v$uF','v$uP$uH')), inference(demodulation, [status(thm)], [c53,c4])).
% 42.72/7.25 cnf(d11, 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$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','v$ub','v$ua'),hAPP('v$uF','v$uP$uH')), inference(demodulation, [status(thm)], [d10,c3])).
% 42.72/7.25 cnf(d12, plain, 'Ts8'('v$uP$uH','v$uP','v$ua','v$ub') | 'v$ua' = 'v$ub' | '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$uF',X0)) | ~'c$umember'('tc$ufun'('tc$uArrow$u$uOrder$u$uMirabelle$uOindi','tc$ufun'('tc$uprod'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt','tc$uArrow$u$uOrder$u$uMirabelle$uOalt'),'tc$uHOL$uObool')),X0,'c$uArrow$u$uOrder$u$uMirabelle$uOProf') | ~'c$umember'('tc$ufun'('tc$uArrow$u$uOrder$u$uMirabelle$uOindi','tc$ufun'('tc$uprod'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt','tc$uArrow$u$uOrder$u$uMirabelle$uOalt'),'tc$uHOL$uObool')),'v$uP$uH','c$uArrow$u$uOrder$u$uMirabelle$uOProf') | 'Ts8'(X0,'v$uP$uH','v$ub','v$ua'), inference(resolution, [status(thm)], [d9,c19])).
% 42.72/7.25 cnf(d13, plain, 'v$ua' != 'v$ua$uH', inference(demodulation, [status(thm)], [c2,c3])).
% 42.72/7.25 cnf(d14, plain, 'v$ua' != 'v$ub', inference(demodulation, [status(thm)], [d13,c4])).
% 42.72/7.25 cnf(d15, 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$uF',X0)) | ~'c$umember'('tc$ufun'('tc$uArrow$u$uOrder$u$uMirabelle$uOindi','tc$ufun'('tc$uprod'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt','tc$uArrow$u$uOrder$u$uMirabelle$uOalt'),'tc$uHOL$uObool')),X0,'c$uArrow$u$uOrder$u$uMirabelle$uOProf') | ~'c$umember'('tc$ufun'('tc$uArrow$u$uOrder$u$uMirabelle$uOindi','tc$ufun'('tc$uprod'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt','tc$uArrow$u$uOrder$u$uMirabelle$uOalt'),'tc$uHOL$uObool')),'v$uP$uH','c$uArrow$u$uOrder$u$uMirabelle$uOProf') | 'Ts8'(X0,'v$uP$uH','v$ub','v$ua') | 'Ts8'('v$uP$uH','v$uP','v$ua','v$ub'), inference(resolution, [status(thm)], [d14,d12])).
% 42.72/7.25 cnf(d16, 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$uF',X0)) | ~'c$umember'('tc$ufun'('tc$uArrow$u$uOrder$u$uMirabelle$uOindi','tc$ufun'('tc$uprod'('tc$uArrow$u$uOrder$u$uMirabelle$uOalt','tc$uArrow$u$uOrder$u$uMirabelle$uOalt'),'tc$uHOL$uObool')),X0,'c$uArrow$u$uOrder$u$uMirabelle$uOProf') | 'Ts8'(X0,'v$uP$uH','v$ub','v$ua') | 'Ts8'('v$uP$uH','v$uP','v$ua','v$ub'), inference(resolution, [status(thm)], [c14,d15])).
% 42.72/7.25 cnf(d17, 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$uF','v$uP')) | 'Ts8'('v$uP','v$uP$uH','v$ub','v$ua') | 'Ts8'('v$uP$uH','v$uP','v$ua','v$ub'), inference(resolution, [status(thm)], [d16,c13])).
% 42.72/7.25 cnf(d18, plain, 'Ts8'('v$uP','v$uP$uH','v$ub','v$ua') | 'Ts8'('v$uP$uH','v$uP','v$ua','v$ub') | ~'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$uF','v$uP$uH')), inference(resolution, [status(thm)], [d17,d11])).
% 42.72/7.25 cnf(d19, plain, 'Ts8'('v$uP','v$uP$uH','v$ub','v$ua') | 'Ts8'('v$uP$uH','v$uP','v$ua','v$ub') | 'Ts8'('v$uP$uH','v$uP','v$ua','v$ub'), inference(resolution, [status(thm)], [d18,d9])).
% 42.72/7.25 cnf(d20, plain, 'Ts8'('v$uP$uH','v$uP','v$ua','v$ub') | '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',sK13('v$ua','v$uP','v$ub','v$uP$uH'))) | '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$uH',sK13('v$ua','v$uP','v$ub','v$uP$uH'))), inference(resolution, [status(thm)], [d19,c22])).
% 42.72/7.25 cnf(d21, 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',sK13('v$ua','v$uP','v$ub','v$uP$uH'))) | 'Ts8'('v$uP$uH','v$uP','v$ua','v$ub') | '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',sK13('v$ua','v$uP','v$ub','v$uP$uH'))), inference(resolution, [status(thm)], [d20,d3])).
% 42.72/7.25 cnf(d22, plain, 'Ts8'('v$uP$uH','v$uP','v$ua','v$ub') | '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$uH',sK13('v$ua','v$uP','v$ub','v$uP$uH'))), inference(resolution, [status(thm)], [d21,d1])).
% 42.72/7.25 cnf(d23, plain, 'Ts8'('v$uP$uH','v$uP','v$ua','v$ub') | ~'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$uH',sK13('v$ua','v$uP','v$ub','v$uP$uH'))) | ~'Ts8'('v$uP','v$uP$uH','v$ub','v$ua'), inference(resolution, [status(thm)], [d21,c23])).
% 42.72/7.25 cnf(d24, plain, ~'Ts8'('v$uP','v$uP$uH','v$ub','v$ua') | 'Ts8'('v$uP$uH','v$uP','v$ua','v$ub') | 'Ts8'('v$uP$uH','v$uP','v$ua','v$ub'), inference(resolution, [status(thm)], [d23,d22])).
% 42.72/7.25 cnf(d25, plain, 'Ts8'('v$uP$uH','v$uP','v$ua','v$ub') | 'Ts8'('v$uP$uH','v$uP','v$ua','v$ub'), inference(resolution, [status(thm)], [d24,d19])).
% 42.72/7.25 cnf(d26, 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$ub','v$ua'),hAPP('v$uP$uH',sK13('v$ub','v$uP$uH','v$ua','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','v$ua','v$ub'),hAPP('v$uP',sK13('v$ub','v$uP$uH','v$ua','v$uP'))), inference(resolution, [status(thm)], [d25,c22])).
% 42.72/7.25 cnf(d27, 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',sK13('v$ub','v$uP$uH','v$ua','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','v$ua','v$ub'),hAPP('v$uP',sK13('v$ub','v$uP$uH','v$ua','v$uP'))), inference(resolution, [status(thm)], [d26,d3])).
% 42.72/7.25 cnf(d28, 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$ub','v$ua'),hAPP('v$uP$uH',sK13('v$ub','v$uP$uH','v$ua','v$uP'))), inference(resolution, [status(thm)], [d27,d1])).
% 42.72/7.25 cnf(d29, 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',sK13('v$ub','v$uP$uH','v$ua','v$uP'))) | ~'Ts8'('v$uP$uH','v$uP','v$ua','v$ub'), inference(resolution, [status(thm)], [d28,c23])).
% 42.72/7.25 cnf(d30, 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',sK13('v$ub','v$uP$uH','v$ua','v$uP'))), inference(resolution, [status(thm)], [d25,d29])).
% 42.72/7.25 cnf(d31, plain, $false, inference(resolution, [status(thm)], [d27,d30])).
% 42.72/7.25 % SZS output end CNFRefutation for theBenchmark.p
%------------------------------------------------------------------------------