%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : SWC284-1 : TPTP v8.1.0. Released v2.4.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n006.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 600s % DateTime : Tue Jul 19 22:03:02 EDT 2022 % Result : Unsatisfiable 34.78s 34.98s % Output : Refutation 46.34s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SWC284-1 : TPTP v8.1.0. Released v2.4.0. % 0.12/0.13 % Command : run_spass %d %s % 0.13/0.34 % Computer : n006.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 600 % 0.13/0.34 % DateTime : Sun Jun 12 22:38:57 EDT 2022 % 0.13/0.34 % CPUTime : % 34.78/34.98 % 34.78/34.98 SPASS V 3.9 % 34.78/34.98 SPASS beiseite: Proof found. % 34.78/34.98 % SZS status Theorem % 34.78/34.98 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 34.78/34.98 SPASS derived 37489 clauses, backtracked 13633 clauses, performed 104 splits and kept 28765 clauses. % 34.78/34.98 SPASS allocated 110331 KBytes. % 34.78/34.98 SPASS spent 0:0:34.58 on the problem. % 34.78/34.98 0:00:00.04 for the input. % 34.78/34.98 0:00:00.00 for the FLOTTER CNF translation. % 34.78/34.98 0:00:00.38 for inferences. % 34.78/34.98 0:00:01.26 for the backtracking. % 34.78/34.98 0:0:32.51 for the reduction. % 34.78/34.98 % 34.78/34.98 % 34.78/34.98 Here is a proof with depth 9, length 724 : % 34.78/34.98 % SZS output start Refutation % 34.78/34.98 1[0:Inp] || -> ssList(sk1)*. % 34.78/34.98 2[0:Inp] || -> ssList(sk2)*. % 34.78/34.98 5[0:Inp] || -> equal(sk4,sk2)**. % 34.78/34.98 6[0:Inp] || -> equal(sk3,sk1)**. % 34.78/34.98 8[0:Inp] || -> ssList(sk6)*. % 34.78/34.98 9[0:Inp] || -> ssList(sk7)*. % 34.78/34.98 10[0:Inp] || -> equal(app(app(sk6,cons(sk5,nil)),sk7),sk1)**. % 34.78/34.98 12[0:Inp] || -> memberP(sk7,sk8)* memberP(sk6,sk8). % 34.78/34.98 13[0:Inp] || leq(sk5,sk8) -> memberP(sk6,sk8)*. % 34.78/34.98 14[0:Inp] || leq(sk8,sk5) -> memberP(sk7,sk8)*. % 34.78/34.98 15[0:Inp] || leq(sk5,sk8) leq(sk8,sk5)* -> . % 34.78/34.98 16[0:Inp] || equal(nil,sk4) -> equal(sk3,nil)**. % 34.78/34.98 18[0:Inp] || neq(sk4,nil) -> equal(cons(sk9,nil),sk3)**. % 34.78/34.98 19[0:Inp] || neq(sk4,nil) -> memberP(sk4,sk9)*. % 34.78/34.98 20[0:Inp] || -> equalelemsP(nil)*. % 34.78/34.98 21[0:Inp] || -> duplicatefreeP(nil)*. % 34.78/34.98 22[0:Inp] || -> strictorderedP(nil)*. % 34.78/34.98 23[0:Inp] || -> totalorderedP(nil)*. % 34.78/34.98 24[0:Inp] || -> strictorderP(nil)*. % 34.78/34.98 25[0:Inp] || -> totalorderP(nil)*. % 34.78/34.98 26[0:Inp] || -> cyclefreeP(nil)*. % 34.78/34.98 27[0:Inp] || -> ssList(nil)*. % 34.78/34.98 31[0:Inp] || -> ssItem(skaf83(u))*. % 34.78/34.98 32[0:Inp] || -> ssList(skaf82(u))*. % 34.78/34.98 73[0:Inp] || equal(skac2,skac3)** -> . % 34.78/34.98 81[0:Inp] ssItem(u) || -> leq(u,u)*. % 34.78/34.98 82[0:Inp] ssItem(u) || lt(u,u)* -> . % 34.78/34.98 83[0:Inp] ssItem(u) || -> equalelemsP(cons(u,nil))*. % 34.78/34.98 84[0:Inp] ssItem(u) || -> duplicatefreeP(cons(u,nil))*. % 34.78/34.98 85[0:Inp] ssItem(u) || -> strictorderedP(cons(u,nil))*. % 34.78/34.98 86[0:Inp] ssItem(u) || -> totalorderedP(cons(u,nil))*. % 34.78/34.98 87[0:Inp] ssItem(u) || -> strictorderP(cons(u,nil))*. % 34.78/34.98 88[0:Inp] ssItem(u) || -> totalorderP(cons(u,nil))*. % 34.78/34.98 89[0:Inp] ssItem(u) || -> cyclefreeP(cons(u,nil))*. % 34.78/34.98 90[0:Inp] ssItem(u) || memberP(nil,u)* -> . % 34.78/34.98 91[0:Inp] ssList(u) || -> ssItem(v)* duplicatefreeP(u)*. % 34.78/34.98 93[0:Inp] ssList(u) || -> equal(app(nil,u),u)**. % 34.78/34.98 104[0:Inp] ssList(u) ssList(v) || -> ssList(app(u,v))*. % 34.78/34.98 105[0:Inp] ssList(u) ssItem(v) || -> ssList(cons(v,u))*. % 34.78/34.98 106[0:Inp] ssList(u) || -> cyclefreeP(u) leq(skaf50(u),skaf49(u))*. % 34.78/34.98 115[0:Inp] ssList(u) ssItem(v) || -> equal(tl(cons(v,u)),u)**. % 34.78/34.98 116[0:Inp] ssList(u) ssItem(v) || -> equal(hd(cons(v,u)),v)**. % 34.78/34.98 117[0:Inp] ssList(u) ssItem(v) || equal(cons(v,u),nil)** -> . % 34.78/34.98 118[0:Inp] ssList(u) ssItem(v) || equal(cons(v,u),u)** -> . % 34.78/34.98 120[0:Inp] ssList(u) singletonP(u) || -> equal(cons(skaf44(u),nil),u)**. % 34.78/34.98 121[0:Inp] ssItem(u) ssItem(v) || -> equal(u,v) neq(u,v)*. % 34.78/34.98 128[0:Inp] ssList(u) || -> equal(nil,u) equal(cons(skaf83(u),skaf82(u)),u)**. % 34.78/34.98 132[0:Inp] ssItem(u) ssList(v) || equal(nil,v) -> totalorderedP(cons(u,v))*. % 34.78/34.98 135[0:Inp] ssList(u) ssItem(v) || equal(cons(v,nil),u)*+ -> singletonP(u)*. % 34.78/34.98 138[0:Inp] ssList(u) ssList(v) || equal(app(u,v),nil)** -> equal(nil,v). % 34.78/34.98 139[0:Inp] ssList(u) ssItem(v) || -> equal(app(cons(v,nil),u),cons(v,u))**. % 34.78/34.98 142[0:Inp] ssList(u) ssList(v) || -> equal(nil,u) equal(hd(app(u,v)),hd(u))**. % 34.78/34.98 143[0:Inp] ssItem(u) ssList(v) || strictorderedP(cons(u,v))* -> strictorderedP(v) equal(nil,v). % 34.78/34.98 144[0:Inp] ssItem(u) ssList(v) || totalorderedP(cons(u,v))* -> totalorderedP(v) equal(nil,v). % 34.78/34.98 148[0:Inp] ssList(u) ssList(v) || frontsegP(u,v)*+ frontsegP(v,u)* -> equal(u,v). % 34.78/34.98 153[0:Inp] ssItem(u) ssList(v) || strictorderedP(cons(u,v)) -> lt(u,hd(v))* equal(nil,v). % 34.78/34.98 154[0:Inp] ssItem(u) ssList(v) || totalorderedP(cons(u,v))* -> leq(u,hd(v)) equal(nil,v). % 34.78/34.98 157[0:Inp] ssItem(u) ssItem(v) ssList(w) || equal(u,v) -> memberP(cons(v,w),u)*. % 34.78/34.98 159[0:Inp] ssItem(u) ssList(v) ssList(w) || memberP(v,u) -> memberP(app(v,w),u)*. % 34.78/34.98 160[0:Inp] ssItem(u) ssList(v) ssList(w) || memberP(w,u) -> memberP(app(v,w),u)*. % 34.78/34.98 163[0:Inp] ssList(u) ssList(v) ssList(w) || equal(app(v,w),u)*+ -> frontsegP(u,v)*. % 34.78/34.98 168[0:Inp] ssList(u) ssList(v) ssList(w) || -> equal(app(app(u,v),w),app(u,app(v,w)))**. % 34.78/34.98 176[0:Inp] ssList(u) ssList(v) ssItem(w) || -> equal(app(cons(w,v),u),cons(w,app(v,u)))**. % 34.78/34.98 178[0:Inp] totalorderedP(u) ssList(u) ssItem(v) || leq(v,hd(u)) -> totalorderedP(cons(v,u))* equal(nil,u). % 34.78/34.98 180[0:Inp] ssItem(u) ssItem(v) ssList(w) || memberP(cons(v,w),u)* -> equal(u,v) memberP(w,u). % 34.78/34.98 182[0:Inp] ssList(u) || -> strictorderedP(u) equal(app(app(skaf71(u),cons(skaf69(u),skaf72(u))),cons(skaf70(u),skaf73(u))),u)**. % 34.78/34.98 183[0:Inp] ssList(u) || -> totalorderedP(u) equal(app(app(skaf66(u),cons(skaf64(u),skaf67(u))),cons(skaf65(u),skaf68(u))),u)**. % 34.78/34.98 184[0:Inp] ssList(u) || -> strictorderP(u) equal(app(app(skaf61(u),cons(skaf59(u),skaf62(u))),cons(skaf60(u),skaf63(u))),u)**. % 34.78/34.98 185[0:Inp] ssList(u) || -> totalorderP(u) equal(app(app(skaf56(u),cons(skaf54(u),skaf57(u))),cons(skaf55(u),skaf58(u))),u)**. % 34.78/34.98 189[0:Inp] ssList(u) ssList(v) ssItem(w) ssItem(x) || equal(cons(w,u),cons(x,v))* -> equal(w,x). % 34.78/34.98 194[0:Inp] ssList(u) ssItem(v) ssList(w) ssList(x) || equal(app(w,cons(v,x)),u)*+ -> memberP(u,v)*. % 34.78/34.98 196[0:Inp] ssList(u) ssList(v) || equal(hd(v),hd(u))* equal(tl(v),tl(u)) -> equal(v,u) equal(nil,v) equal(nil,u). % 34.78/34.98 198[0:Inp] ssList(u) duplicatefreeP(u) ssItem(v) ssList(w) ssList(x) ssList(y) || equal(app(app(w,cons(v,x)),cons(v,y)),u)* -> . % 34.78/34.98 208[0:Rew:5.0,19.1,5.0,19.0] || neq(sk2,nil) -> memberP(sk2,sk9)*. % 34.78/34.98 209[0:Rew:6.0,16.1,5.0,16.0] || equal(nil,sk2)** -> equal(nil,sk1). % 34.78/34.98 210[0:Rew:6.0,18.1,5.0,18.0] || neq(sk2,nil) -> equal(cons(sk9,nil),sk1)**. % 34.78/34.98 211[0:MRR:178.5,132.2] ssItem(u) ssList(v) totalorderedP(v) || leq(u,hd(v)) -> totalorderedP(cons(u,v))*. % 34.78/34.98 333[0:Res:9.0,185.0] || -> totalorderP(sk7) equal(app(app(skaf56(sk7),cons(skaf54(sk7),skaf57(sk7))),cons(skaf55(sk7),skaf58(sk7))),sk7)**. % 34.78/34.98 334[0:Res:9.0,184.0] || -> strictorderP(sk7) equal(app(app(skaf61(sk7),cons(skaf59(sk7),skaf62(sk7))),cons(skaf60(sk7),skaf63(sk7))),sk7)**. % 34.78/34.98 335[0:Res:9.0,183.0] || -> totalorderedP(sk7) equal(app(app(skaf66(sk7),cons(skaf64(sk7),skaf67(sk7))),cons(skaf65(sk7),skaf68(sk7))),sk7)**. % 34.78/34.98 336[0:Res:9.0,182.0] || -> strictorderedP(sk7) equal(app(app(skaf71(sk7),cons(skaf69(sk7),skaf72(sk7))),cons(skaf70(sk7),skaf73(sk7))),sk7)**. % 34.78/34.98 340[0:Res:9.0,211.1] ssItem(u) totalorderedP(sk7) || leq(u,hd(sk7)) -> totalorderedP(cons(u,sk7))*. % 34.78/34.98 350[0:Res:9.0,153.0] ssItem(u) || strictorderedP(cons(u,sk7)) -> lt(u,hd(sk7))* equal(nil,sk7). % 34.78/34.98 351[0:Res:9.0,154.0] ssItem(u) || totalorderedP(cons(u,sk7))* -> leq(u,hd(sk7)) equal(nil,sk7). % 34.78/34.98 370[0:Res:9.0,138.0] ssList(u) || equal(app(u,sk7),nil)** -> equal(nil,sk7). % 34.78/34.98 375[0:Res:9.0,128.0] || -> equal(nil,sk7) equal(cons(skaf83(sk7),skaf82(sk7)),sk7)**. % 34.78/34.98 377[0:Res:9.0,120.1] singletonP(sk7) || -> equal(cons(skaf44(sk7),nil),sk7)**. % 34.78/34.98 392[0:Res:9.0,106.0] || -> cyclefreeP(sk7) leq(skaf50(sk7),skaf49(sk7))*. % 34.78/34.98 413[0:Res:9.0,196.1] ssList(u) || equal(hd(u),hd(sk7))* equal(tl(u),tl(sk7)) -> equal(u,sk7) equal(nil,u) equal(nil,sk7). % 34.78/34.98 442[0:Res:9.0,142.1] ssList(u) || -> equal(nil,sk7) equal(hd(app(sk7,u)),hd(sk7))**. % 34.78/34.98 445[0:Res:9.0,139.1] ssItem(u) || -> equal(app(cons(u,nil),sk7),cons(u,sk7))**. % 34.78/34.98 447[0:Res:9.0,135.1] ssItem(u) || equal(cons(u,nil),sk7)** -> singletonP(sk7). % 34.78/34.98 448[0:Res:9.0,115.1] ssItem(u) || -> equal(tl(cons(u,sk7)),sk7)**. % 34.78/34.98 449[0:Res:9.0,116.1] ssItem(u) || -> equal(hd(cons(u,sk7)),u)**. % 34.78/34.98 450[0:Res:9.0,117.1] ssItem(u) || equal(cons(u,sk7),nil)** -> . % 34.78/34.98 451[0:Res:9.0,118.1] ssItem(u) || equal(cons(u,sk7),sk7)** -> . % 34.78/34.98 454[0:Res:9.0,105.1] ssItem(u) || -> ssList(cons(u,sk7))*. % 34.78/34.98 465[0:Res:9.0,176.2] ssList(u) ssItem(v) || -> equal(app(cons(v,u),sk7),cons(v,app(u,sk7)))**. % 34.78/34.98 490[1:Spt:91.1] || -> ssItem(u)*. % 34.78/34.98 491[1:MRR:81.0,490.0] || -> leq(u,u)*. % 34.78/34.98 493[1:MRR:454.0,490.0] || -> ssList(cons(u,sk7))*. % 34.78/34.98 494[1:MRR:90.0,490.0] || memberP(nil,u)* -> . % 34.78/34.98 495[1:MRR:89.0,490.0] || -> cyclefreeP(cons(u,nil))*. % 34.78/34.98 496[1:MRR:88.0,490.0] || -> totalorderP(cons(u,nil))*. % 34.78/34.98 497[1:MRR:87.0,490.0] || -> strictorderP(cons(u,nil))*. % 34.78/34.98 498[1:MRR:86.0,490.0] || -> totalorderedP(cons(u,nil))*. % 34.78/34.98 499[1:MRR:85.0,490.0] || -> strictorderedP(cons(u,nil))*. % 34.78/34.98 500[1:MRR:84.0,490.0] || -> duplicatefreeP(cons(u,nil))*. % 34.78/34.98 501[1:MRR:83.0,490.0] || -> equalelemsP(cons(u,nil))*. % 34.78/34.98 502[1:MRR:82.0,490.0] || lt(u,u)* -> . % 34.78/34.98 503[1:MRR:451.0,490.0] || equal(cons(u,sk7),sk7)** -> . % 34.78/34.98 504[1:MRR:450.0,490.0] || equal(cons(u,sk7),nil)** -> . % 34.78/34.98 505[1:MRR:449.0,490.0] || -> equal(hd(cons(u,sk7)),u)**. % 34.78/34.98 506[1:MRR:448.0,490.0] || -> equal(tl(cons(u,sk7)),sk7)**. % 34.78/34.98 519[1:MRR:447.0,490.0] || equal(cons(u,nil),sk7)** -> singletonP(sk7). % 34.78/34.98 528[1:MRR:445.0,490.0] || -> equal(app(cons(u,nil),sk7),cons(u,sk7))**. % 34.78/34.98 529[1:MRR:121.1,121.0,490.0] || -> equal(u,v) neq(u,v)*. % 34.78/34.98 553[1:MRR:351.0,490.0] || totalorderedP(cons(u,sk7))* -> leq(u,hd(sk7)) equal(nil,sk7). % 34.78/34.98 554[1:MRR:350.0,490.0] || strictorderedP(cons(u,sk7)) -> lt(u,hd(sk7))* equal(nil,sk7). % 34.78/34.98 555[1:MRR:340.0,490.0] totalorderedP(sk7) || leq(u,hd(sk7)) -> totalorderedP(cons(u,sk7))*. % 34.78/34.98 561[1:MRR:144.0,490.0] ssList(u) || totalorderedP(cons(v,u))* -> totalorderedP(u) equal(nil,u). % 34.78/34.98 562[1:MRR:143.0,490.0] ssList(u) || strictorderedP(cons(v,u))* -> strictorderedP(u) equal(nil,u). % 34.78/34.98 587[1:MRR:160.0,490.0] ssList(u) ssList(v) || memberP(v,w) -> memberP(app(u,v),w)*. % 34.78/34.98 588[1:MRR:159.0,490.0] ssList(u) ssList(v) || memberP(u,w) -> memberP(app(u,v),w)*. % 34.78/34.98 590[1:MRR:157.1,157.0,490.0] ssList(u) || equal(v,w) -> memberP(cons(w,u),v)*. % 34.78/34.98 609[1:MRR:180.1,180.0,490.0] ssList(u) || memberP(cons(v,u),w)* -> equal(w,v) memberP(u,w). % 34.78/34.98 625[1:MRR:105.1,490.0] ssList(u) || -> ssList(cons(v,u))*. % 34.78/34.98 626[1:MRR:118.1,490.0] ssList(u) || equal(cons(v,u),u)** -> . % 34.78/34.98 628[1:MRR:116.1,490.0] ssList(u) || -> equal(hd(cons(v,u)),v)**. % 34.78/34.98 629[1:MRR:115.1,490.0] ssList(u) || -> equal(tl(cons(v,u)),u)**. % 34.78/34.98 630[1:MRR:135.1,490.0] ssList(u) || equal(cons(v,nil),u)*+ -> singletonP(u)*. % 34.78/34.98 631[1:MRR:139.1,490.0] ssList(u) || -> equal(app(cons(v,nil),u),cons(v,u))**. % 34.78/34.98 632[1:MRR:465.1,490.0] ssList(u) || -> equal(app(cons(v,u),sk7),cons(v,app(u,sk7)))**. % 34.78/34.98 639[1:MRR:194.1,490.0] ssList(u) ssList(v) ssList(w) || equal(app(v,cons(x,w)),u)*+ -> memberP(u,x)*. % 34.78/34.98 683[1:MRR:189.3,189.2,490.0] ssList(u) ssList(v) || equal(cons(w,u),cons(x,v))* -> equal(w,x). % 34.78/34.98 684[2:Spt:442.0,442.2] ssList(u) || -> equal(hd(app(sk7,u)),hd(sk7))**. % 34.78/34.98 688[3:Spt:413.5] || -> equal(nil,sk7)**. % 34.78/34.98 741[3:Rew:688.0,93.1] ssList(u) || -> equal(app(sk7,u),u)**. % 34.78/34.98 747[3:Rew:688.0,495.0] || -> cyclefreeP(cons(u,sk7))*. % 34.78/34.98 748[3:Rew:688.0,496.0] || -> totalorderP(cons(u,sk7))*. % 34.78/34.98 749[3:Rew:688.0,497.0] || -> strictorderP(cons(u,sk7))*. % 34.78/34.98 750[3:Rew:688.0,498.0] || -> totalorderedP(cons(u,sk7))*. % 34.78/34.98 751[3:Rew:688.0,499.0] || -> strictorderedP(cons(u,sk7))*. % 34.78/34.98 752[3:Rew:688.0,500.0] || -> duplicatefreeP(cons(u,sk7))*. % 34.78/34.98 753[3:Rew:688.0,501.0] || -> equalelemsP(cons(u,sk7))*. % 34.78/34.98 759[3:Rew:688.0,631.1] ssList(u) || -> equal(app(cons(v,sk7),u),cons(v,u))**. % 34.78/34.98 797[3:Rew:741.1,684.1] ssList(u) || -> equal(hd(u),hd(sk7))*. % 34.78/34.98 1334[3:SpR:797.1,505.0] ssList(cons(u,sk7)) || -> equal(hd(sk7),u)*. % 34.78/34.98 1339[3:SSi:1334.0,753.0,752.0,751.0,750.0,749.0,748.0,747.0,493.0] || -> equal(hd(sk7),u)*. % 34.78/34.98 1445[3:Rew:1339.0,759.1] ssList(u) || -> equal(cons(v,u),hd(sk7))**. % 34.78/34.98 1456[3:Rew:1339.0,683.2] ssList(u) ssList(v) || equal(cons(w,u),hd(sk7))** -> equal(w,x)*. % 34.78/34.98 1529[3:Con:1456.1] ssList(u) || equal(cons(v,u),hd(sk7))** -> equal(v,w)*. % 34.78/34.98 1530[3:AED:73.0,1529.2] ssList(u) || equal(cons(v,u),hd(sk7))** -> . % 34.78/34.98 1531[3:Rew:1445.1,1530.1] ssList(u) || equal(hd(sk7),hd(sk7))* -> . % 34.78/34.98 1532[3:Obv:1531.1] ssList(u) || -> . % 34.78/34.98 1533[3:UnC:1532.0,2.0] || -> . % 34.78/34.98 1619[3:Spt:1533.0,413.5,688.0] || equal(nil,sk7)** -> . % 34.78/34.98 1620[3:Spt:1533.0,413.0,413.1,413.2,413.3,413.4] ssList(u) || equal(hd(u),hd(sk7))* equal(tl(u),tl(sk7)) -> equal(u,sk7) equal(nil,u). % 34.78/34.98 1625[3:MRR:375.0,1619.0] || -> equal(cons(skaf83(sk7),skaf82(sk7)),sk7)**. % 34.78/34.98 1630[3:MRR:370.2,1619.0] ssList(u) || equal(app(u,sk7),nil)** -> . % 34.78/34.98 1631[3:MRR:553.2,1619.0] || totalorderedP(cons(u,sk7))* -> leq(u,hd(sk7)). % 34.78/34.98 1632[3:MRR:554.2,1619.0] || strictorderedP(cons(u,sk7)) -> lt(u,hd(sk7))*. % 34.78/34.98 1634[4:Spt:209.1] || -> equal(nil,sk1)**. % 34.78/34.98 1636[4:Rew:1634.0,20.0] || -> equalelemsP(sk1)*. % 34.78/34.98 1637[4:Rew:1634.0,21.0] || -> duplicatefreeP(sk1)*. % 34.78/34.98 1638[4:Rew:1634.0,22.0] || -> strictorderedP(sk1)*. % 34.78/34.98 1639[4:Rew:1634.0,23.0] || -> totalorderedP(sk1)*. % 34.78/34.98 1640[4:Rew:1634.0,24.0] || -> strictorderP(sk1)*. % 34.78/34.98 1641[4:Rew:1634.0,25.0] || -> totalorderP(sk1)*. % 34.78/34.98 1642[4:Rew:1634.0,26.0] || -> cyclefreeP(sk1)*. % 34.78/34.98 1648[4:Rew:1634.0,501.0] || -> equalelemsP(cons(u,sk1))*. % 34.78/34.98 1649[4:Rew:1634.0,500.0] || -> duplicatefreeP(cons(u,sk1))*. % 34.78/34.98 1650[4:Rew:1634.0,499.0] || -> strictorderedP(cons(u,sk1))*. % 34.78/34.98 1651[4:Rew:1634.0,498.0] || -> totalorderedP(cons(u,sk1))*. % 34.78/34.98 1652[4:Rew:1634.0,497.0] || -> strictorderP(cons(u,sk1))*. % 34.78/34.98 1653[4:Rew:1634.0,496.0] || -> totalorderP(cons(u,sk1))*. % 34.78/34.98 1654[4:Rew:1634.0,495.0] || -> cyclefreeP(cons(u,sk1))*. % 34.78/34.98 1673[4:Rew:1634.0,10.0] || -> equal(app(app(sk6,cons(sk5,sk1)),sk7),sk1)**. % 34.78/34.98 1700[4:Rew:1634.0,1630.1] ssList(u) || equal(app(u,sk7),sk1)** -> . % 34.78/34.98 1772[3:Res:1632.1,502.0] || strictorderedP(cons(hd(sk7),sk7))* -> . % 34.78/34.98 1785[4:SpL:1673.0,1700.1] ssList(app(sk6,cons(sk5,sk1))) || equal(sk1,sk1)* -> . % 34.78/34.98 1788[4:Obv:1785.1] ssList(app(sk6,cons(sk5,sk1))) || -> . % 34.78/34.98 1810[3:SpR:1625.0,628.1] ssList(skaf82(sk7)) || -> equal(hd(sk7),skaf83(sk7))**. % 34.78/34.98 1848[4:SoR:1788.0,104.2] ssList(cons(sk5,sk1)) ssList(sk6) || -> . % 34.78/34.98 1855[4:SSi:1848.1,1848.0,8.0,625.0,1.0,1636.0,1637.0,1638.0,1639.0,1640.0,1641.0,1642.0,1648.0,1649.0,1650.0,1651.0,1652.0,1653.1,1654.0] || -> . % 34.78/34.98 1856[4:Spt:1855.0,209.1,1634.0] || equal(nil,sk1)** -> . % 34.78/34.98 1857[4:Spt:1855.0,209.0] || equal(nil,sk2)** -> . % 34.78/34.98 1863[3:SSi:1810.0,32.0,9.0] || -> equal(hd(sk7),skaf83(sk7))**. % 34.78/34.98 1864[3:Rew:1863.0,1772.0] || strictorderedP(cons(skaf83(sk7),sk7))* -> . % 34.78/34.98 1867[3:Rew:1863.0,1631.1] || totalorderedP(cons(u,sk7))* -> leq(u,skaf83(sk7)). % 34.78/34.98 1874[3:Rew:1863.0,555.1] totalorderedP(sk7) || leq(u,skaf83(sk7)) -> totalorderedP(cons(u,sk7))*. % 34.78/34.98 1876[5:Spt:336.0] || -> strictorderedP(sk7)*. % 34.78/34.98 1879[6:Spt:335.0] || -> totalorderedP(sk7)*. % 34.78/34.98 1880[6:MRR:1874.0,1879.0] || leq(u,skaf83(sk7)) -> totalorderedP(cons(u,sk7))*. % 34.78/34.98 1883[7:Spt:392.0] || -> cyclefreeP(sk7)*. % 34.78/34.98 1885[8:Spt:334.0] || -> strictorderP(sk7)*. % 34.78/34.98 1886[9:Spt:333.0] || -> totalorderP(sk7)*. % 34.78/34.98 1891[10:Spt:12.1] || -> memberP(sk6,sk8)*. % 34.78/34.98 1909[1:SpR:210.1,495.0] || neq(sk2,nil)* -> cyclefreeP(sk1). % 34.78/34.98 1910[1:SpR:210.1,496.0] || neq(sk2,nil)* -> totalorderP(sk1). % 34.78/34.98 1911[1:SpR:210.1,497.0] || neq(sk2,nil)* -> strictorderP(sk1). % 34.78/34.98 1912[1:SpR:210.1,498.0] || neq(sk2,nil)* -> totalorderedP(sk1). % 34.78/34.98 1913[1:SpR:210.1,499.0] || neq(sk2,nil)* -> strictorderedP(sk1). % 34.78/34.98 1914[1:SpR:210.1,500.0] || neq(sk2,nil)* -> duplicatefreeP(sk1). % 34.78/34.98 1915[1:SpR:210.1,501.0] || neq(sk2,nil)* -> equalelemsP(sk1). % 34.78/34.98 1917[1:SpR:210.1,629.1] ssList(nil) || neq(sk2,nil)* -> equal(tl(sk1),nil). % 34.78/34.98 1918[1:SpR:210.1,628.1] ssList(nil) || neq(sk2,nil)* -> equal(hd(sk1),sk9). % 34.78/34.98 1920[1:SpL:210.1,519.0] || neq(sk2,nil)* equal(sk7,sk1) -> singletonP(sk7). % 34.78/34.98 1922[1:SSi:1917.0,27.0,26.0,25.0,24.0,23.0,22.0,21.0,20.0] || neq(sk2,nil)* -> equal(tl(sk1),nil). % 34.78/34.98 1923[1:SSi:1918.0,27.0,26.0,25.0,24.0,23.0,22.0,21.0,20.0] || neq(sk2,nil)* -> equal(hd(sk1),sk9). % 34.78/34.98 1924[1:Res:529.1,1909.0] || -> equal(nil,sk2) cyclefreeP(sk1)*. % 34.78/34.98 1925[4:MRR:1924.0,1857.0] || -> cyclefreeP(sk1)*. % 34.78/34.98 1929[1:Res:529.1,1910.0] || -> equal(nil,sk2) totalorderP(sk1)*. % 34.78/34.98 1930[4:MRR:1929.0,1857.0] || -> totalorderP(sk1)*. % 34.78/34.98 1931[1:Res:529.1,1911.0] || -> equal(nil,sk2) strictorderP(sk1)*. % 34.78/34.98 1932[4:MRR:1931.0,1857.0] || -> strictorderP(sk1)*. % 34.78/34.98 1935[1:Res:529.1,1912.0] || -> equal(nil,sk2) totalorderedP(sk1)*. % 34.78/34.98 1936[4:MRR:1935.0,1857.0] || -> totalorderedP(sk1)*. % 34.78/34.98 1937[1:Res:529.1,1913.0] || -> equal(nil,sk2) strictorderedP(sk1)*. % 34.78/34.98 1938[4:MRR:1937.0,1857.0] || -> strictorderedP(sk1)*. % 34.78/34.98 1941[1:Res:529.1,1914.0] || -> equal(nil,sk2) duplicatefreeP(sk1)*. % 34.78/34.98 1942[4:MRR:1941.0,1857.0] || -> duplicatefreeP(sk1)*. % 34.78/34.98 1943[1:Res:529.1,1915.0] || -> equal(nil,sk2) equalelemsP(sk1)*. % 34.78/34.98 1944[4:MRR:1943.0,1857.0] || -> equalelemsP(sk1)*. % 34.78/34.98 1947[1:Res:529.1,1922.0] || -> equal(nil,sk2) equal(tl(sk1),nil)**. % 34.78/34.98 1948[4:MRR:1947.0,1857.0] || -> equal(tl(sk1),nil)**. % 34.78/34.98 1951[1:Res:529.1,1923.0] || -> equal(nil,sk2) equal(hd(sk1),sk9)**. % 34.78/34.98 1952[4:MRR:1951.0,1857.0] || -> equal(hd(sk1),sk9)**. % 34.78/34.98 1970[1:SpR:210.1,528.0] || neq(sk2,nil) -> equal(app(sk1,sk7),cons(sk9,sk7))**. % 34.78/34.98 1976[1:Res:529.1,1920.0] || equal(sk7,sk1) -> equal(nil,sk2) singletonP(sk7)*. % 34.78/34.98 2044[1:EqR:630.1] ssList(cons(u,nil)) || -> singletonP(cons(u,nil))*. % 34.78/34.98 2045[1:SpL:210.1,630.1] ssList(u) || neq(sk2,nil)* equal(sk1,u) -> singletonP(u)*. % 34.78/34.98 2047[1:SSi:2044.0,625.0,27.0,26.0,25.0,24.0,23.0,22.0,21.0,20.0,495.0,496.0,497.0,498.0,499.0,500.0,501.1] || -> singletonP(cons(u,nil))*. % 34.78/34.98 2049[1:SpR:210.1,2047.0] || neq(sk2,nil)* -> singletonP(sk1). % 34.78/34.98 2051[1:Res:529.1,2049.0] || -> equal(nil,sk2) singletonP(sk1)*. % 34.78/34.98 2052[4:MRR:2051.0,1857.0] || -> singletonP(sk1)*. % 34.78/34.98 2094[1:SpR:120.2,496.0] ssList(u) singletonP(u) || -> totalorderP(u)*. % 34.78/34.98 2103[1:SpR:120.2,629.1] ssList(u) singletonP(u) ssList(nil) || -> equal(tl(u),nil)**. % 34.78/34.98 2104[1:SpR:120.2,628.1] ssList(u) singletonP(u) ssList(nil) || -> equal(hd(u),skaf44(u))**. % 34.78/34.98 2110[1:SpL:120.2,626.1] ssList(u) singletonP(u) ssList(nil) || equal(u,nil)* -> . % 34.78/34.98 2113[1:SSi:2103.2,27.0,26.0,25.0,24.0,23.0,22.0,21.0,20.0] ssList(u) singletonP(u) || -> equal(tl(u),nil)**. % 34.78/34.98 2114[1:SSi:2110.2,27.0,26.0,25.0,24.0,23.0,22.0,21.0,20.0] ssList(u) singletonP(u) || equal(u,nil)* -> . % 34.78/34.98 2115[1:SSi:2104.2,27.0,26.0,25.0,24.0,23.0,22.0,21.0,20.0] ssList(u) singletonP(u) || -> equal(hd(u),skaf44(u))**. % 34.78/34.98 2126[1:SpR:210.1,631.1] ssList(u) || neq(sk2,nil) -> equal(app(sk1,u),cons(sk9,u))**. % 34.78/34.98 2149[3:SpR:1625.0,590.2] ssList(skaf82(sk7)) || equal(u,skaf83(sk7)) -> memberP(sk7,u)*. % 34.78/34.98 2153[9:SSi:2149.0,32.0,9.0,1876.0,1879.0,1883.0,1885.0,1886.0] || equal(u,skaf83(sk7)) -> memberP(sk7,u)*. % 34.78/34.98 2156[1:SpR:2113.2,506.0] ssList(cons(u,sk7)) singletonP(cons(u,sk7)) || -> equal(nil,sk7)**. % 34.78/34.98 2163[1:SSi:2156.0,493.0] singletonP(cons(u,sk7)) || -> equal(nil,sk7)**. % 34.78/34.98 2164[3:MRR:2163.1,1619.0] singletonP(cons(u,sk7)) || -> . % 34.78/34.98 2167[3:SoR:2164.0,630.2] ssList(cons(u,sk7)) || equal(cons(v,nil),cons(u,sk7))* -> . % 34.78/34.98 2168[3:SSi:2167.0,493.0] || equal(cons(u,nil),cons(v,sk7))* -> . % 34.78/34.98 2175[1:SpR:128.2,629.1] ssList(u) ssList(skaf82(u)) || -> equal(nil,u) equal(tl(u),skaf82(u))**. % 34.78/34.98 2176[1:SpR:128.2,628.1] ssList(u) ssList(skaf82(u)) || -> equal(nil,u) equal(hd(u),skaf83(u))**. % 34.78/34.98 2185[1:SSi:2175.1,32.0] ssList(u) || -> equal(nil,u) equal(tl(u),skaf82(u))**. % 34.78/34.98 2192[1:SSi:2176.1,32.0] ssList(u) || -> equal(nil,u) equal(hd(u),skaf83(u))**. % 34.78/34.98 2196[1:Rew:2192.2,142.3] ssList(u) ssList(v) || -> equal(nil,u) equal(hd(app(u,v)),skaf83(u))**. % 34.78/34.98 2206[3:SpL:210.1,2168.0] || neq(sk2,nil) equal(cons(u,sk7),sk1)** -> . % 34.78/34.98 2282[3:SpL:1625.0,561.1] ssList(skaf82(sk7)) || totalorderedP(sk7) -> totalorderedP(skaf82(sk7))* equal(skaf82(sk7),nil). % 34.78/34.98 2291[9:SSi:2282.0,32.0,9.0,1876.0,1879.0,1883.0,1885.0,1886.0] || totalorderedP(sk7) -> totalorderedP(skaf82(sk7))* equal(skaf82(sk7),nil). % 34.78/34.98 2292[9:MRR:2291.0,1879.0] || -> totalorderedP(skaf82(sk7))* equal(skaf82(sk7),nil). % 34.78/34.98 2294[11:Spt:2292.1] || -> equal(skaf82(sk7),nil)**. % 34.78/34.98 2295[11:Rew:2294.0,1625.0] || -> equal(cons(skaf83(sk7),nil),sk7)**. % 34.78/34.98 2312[11:SpR:2295.0,500.0] || -> duplicatefreeP(sk7)*. % 34.78/34.98 2313[11:SpR:2295.0,501.0] || -> equalelemsP(sk7)*. % 34.78/34.98 2314[11:SpR:2295.0,528.0] || -> equal(cons(skaf83(sk7),sk7),app(sk7,sk7))**. % 34.78/34.98 2315[11:SpR:2295.0,2047.0] || -> singletonP(sk7)*. % 34.78/34.98 2400[11:SpR:2314.0,1880.1] || leq(skaf83(sk7),skaf83(sk7))* -> totalorderedP(app(sk7,sk7)). % 34.78/34.98 2422[11:MRR:2400.0,491.0] || -> totalorderedP(app(sk7,sk7))*. % 34.78/34.98 2572[1:SpR:10.0,587.3] ssList(app(sk6,cons(sk5,nil))) ssList(sk7) || memberP(sk7,u)* -> memberP(sk1,u). % 34.78/34.98 2579[11:SSi:2572.1,2572.0,9.0,1876.0,1879.0,1883.0,1885.0,1886.0,2312.0,2313.0,2315.0,104.0,8.0,625.0,27.0,26.0,25.0,24.0,23.1,22.0,21.2,20.0,495.0,496.0,497.0,498.0,499.0,500.0,501.0,2047.0] || memberP(sk7,u)* -> memberP(sk1,u). % 34.78/34.98 2581[11:Res:2153.1,2579.0] || equal(u,skaf83(sk7)) -> memberP(sk1,u)*. % 34.78/34.98 2585[1:SpR:10.0,588.3] ssList(app(sk6,cons(sk5,nil))) ssList(sk7) || memberP(app(sk6,cons(sk5,nil)),u)* -> memberP(sk1,u). % 34.78/34.98 2594[11:SSi:2585.1,2585.0,9.0,1876.0,1879.0,1883.0,1885.0,1886.0,2312.0,2313.0,2315.0,104.0,8.0,625.0,27.0,26.0,25.0,24.0,23.1,22.0,21.2,20.0,495.0,496.0,497.0,498.0,499.0,500.0,501.0,2047.0] || memberP(app(sk6,cons(sk5,nil)),u)* -> memberP(sk1,u). % 34.78/34.98 2599[1:SpL:210.1,609.1] ssList(nil) || neq(sk2,nil) memberP(sk1,u) -> equal(u,sk9) memberP(nil,u)*. % 34.78/34.98 2610[1:SSi:2599.0,27.0,26.0,25.0,24.0,23.0,22.0,21.0,20.0] || neq(sk2,nil) memberP(sk1,u) -> equal(u,sk9) memberP(nil,u)*. % 34.78/34.98 2611[1:MRR:2610.3,494.0] || neq(sk2,nil) memberP(sk1,u)* -> equal(u,sk9). % 34.78/34.98 2628[1:SpR:1970.1,2196.3] ssList(sk1) ssList(sk7) || neq(sk2,nil) -> equal(nil,sk1) equal(hd(cons(sk9,sk7)),skaf83(sk1))**. % 34.78/34.98 2631[1:SpR:631.1,2196.3] ssList(u) ssList(cons(v,nil)) ssList(u) || -> equal(cons(v,nil),nil) equal(hd(cons(v,u)),skaf83(cons(v,nil)))**. % 34.78/34.98 2634[1:Rew:628.1,2628.4] ssList(sk1) ssList(sk7) || neq(sk2,nil)* -> equal(nil,sk1) equal(skaf83(sk1),sk9). % 34.78/34.98 2635[11:SSi:2634.1,2634.0,9.0,1876.0,1879.0,1883.0,1885.0,1886.0,2312.0,2313.0,2315.0,1.0,1925.0,1930.0,1932.0,1936.0,1938.0,1942.0,1944.0,2052.0] || neq(sk2,nil)* -> equal(nil,sk1) equal(skaf83(sk1),sk9). % 34.78/34.98 2636[11:MRR:2635.1,1856.0] || neq(sk2,nil)* -> equal(skaf83(sk1),sk9). % 34.78/34.98 2639[1:Obv:2631.0] ssList(cons(u,nil)) ssList(v) || -> equal(cons(u,nil),nil) equal(hd(cons(u,v)),skaf83(cons(u,nil)))**. % 34.78/34.98 2640[1:Rew:628.1,2639.3] ssList(cons(u,nil)) ssList(v) || -> equal(cons(u,nil),nil) equal(skaf83(cons(u,nil)),u)**. % 34.78/34.98 2641[1:Con:2640.1] ssList(cons(u,nil)) || -> equal(cons(u,nil),nil) equal(skaf83(cons(u,nil)),u)**. % 34.78/34.98 2645[11:Res:529.1,2636.0] || -> equal(nil,sk2) equal(skaf83(sk1),sk9)**. % 34.78/34.98 2646[11:MRR:2645.0,1857.0] || -> equal(skaf83(sk1),sk9)**. % 34.78/34.98 2647[11:SpR:2646.0,128.2] ssList(sk1) || -> equal(nil,sk1) equal(cons(sk9,skaf82(sk1)),sk1)**. % 34.78/34.98 2650[11:SSi:2647.0,1.0,1925.0,1930.0,1932.0,1936.0,1938.0,1942.0,1944.0,2052.0] || -> equal(nil,sk1) equal(cons(sk9,skaf82(sk1)),sk1)**. % 34.78/34.98 2651[11:MRR:2650.0,1856.0] || -> equal(cons(sk9,skaf82(sk1)),sk1)**. % 34.78/34.98 2656[11:SpR:2651.0,629.1] ssList(skaf82(sk1)) || -> equal(tl(sk1),skaf82(sk1))**. % 34.78/34.98 2668[11:SpL:2651.0,609.1] ssList(skaf82(sk1)) || memberP(sk1,u) -> equal(u,sk9) memberP(skaf82(sk1),u)*. % 34.78/34.98 2669[11:Rew:1948.0,2656.1] ssList(skaf82(sk1)) || -> equal(skaf82(sk1),nil)**. % 34.78/34.98 2670[11:SSi:2669.0,32.0,1.0,1925.0,1930.0,1932.0,1936.0,1938.0,1942.0,1944.0,2052.0] || -> equal(skaf82(sk1),nil)**. % 34.78/34.98 2671[11:Rew:2670.0,2651.0] || -> equal(cons(sk9,nil),sk1)**. % 34.78/34.98 2675[11:Rew:2670.0,2668.3] ssList(skaf82(sk1)) || memberP(sk1,u) -> equal(u,sk9) memberP(nil,u)*. % 34.78/34.98 2676[11:SSi:2675.0,32.0,1.0,1925.0,1930.0,1932.0,1936.0,1938.0,1942.0,1944.0,2052.0] || memberP(sk1,u) -> equal(u,sk9) memberP(nil,u)*. % 34.78/34.98 2677[11:MRR:2676.2,494.0] || memberP(sk1,u)* -> equal(u,sk9). % 34.78/34.98 2768[11:Res:2581.1,2677.0] || equal(u,skaf83(sk7))* -> equal(u,sk9). % 34.78/34.98 2790[11:EqR:2768.0] || -> equal(skaf83(sk7),sk9)**. % 34.78/34.98 2796[11:Rew:2790.0,1867.1] || totalorderedP(cons(u,sk7))* -> leq(u,sk9). % 34.78/34.98 2805[11:Rew:2790.0,2295.0] || -> equal(cons(sk9,nil),sk7)**. % 34.78/34.98 2807[11:Rew:2790.0,2314.0] || -> equal(app(sk7,sk7),cons(sk9,sk7))**. % 34.78/34.98 2822[11:Rew:2671.0,2805.0] || -> equal(sk7,sk1)**. % 34.78/34.98 2828[11:Rew:2822.0,505.0] || -> equal(hd(cons(u,sk1)),u)**. % 34.78/34.98 2859[11:Rew:2822.0,10.0] || -> equal(app(app(sk6,cons(sk5,nil)),sk1),sk1)**. % 34.78/34.98 2860[11:Rew:2822.0,528.0] || -> equal(app(cons(u,nil),sk1),cons(u,sk1))**. % 34.78/34.98 2868[11:Rew:2822.0,2422.0] || -> totalorderedP(app(sk1,sk1))*. % 34.78/34.98 3016[11:Rew:2822.0,2807.0] || -> equal(app(sk1,sk1),cons(sk9,sk1))**. % 34.78/34.98 3018[11:Rew:3016.0,2868.0] || -> totalorderedP(cons(sk9,sk1))*. % 34.78/34.98 3029[11:Rew:2822.0,2796.0] || totalorderedP(cons(u,sk1))* -> leq(u,sk9). % 34.78/34.98 3497[0:EqR:163.3] ssList(app(u,v)) ssList(u) ssList(v) || -> frontsegP(app(u,v),u)*. % 34.78/34.98 3511[0:SSi:3497.0,104.2] ssList(u) ssList(v) || -> frontsegP(app(u,v),u)*. % 34.78/34.98 3776[11:Res:588.3,2594.0] ssList(sk6) ssList(cons(sk5,nil)) || memberP(sk6,u)* -> memberP(sk1,u). % 34.78/34.98 3777[11:Res:587.3,2594.0] ssList(sk6) ssList(cons(sk5,nil)) || memberP(cons(sk5,nil),u)* -> memberP(sk1,u). % 34.78/34.98 3778[11:SSi:3776.1,3776.0,625.0,27.0,26.0,25.0,24.0,23.0,22.0,21.0,20.0,495.0,496.0,497.0,498.0,499.0,500.0,501.0,2047.0,8.1] || memberP(sk6,u)* -> memberP(sk1,u). % 34.78/34.98 3779[11:SSi:3777.1,3777.0,625.0,27.0,26.0,25.0,24.0,23.0,22.0,21.0,20.0,495.0,496.0,497.0,498.0,499.0,500.0,501.0,2047.0,8.1] || memberP(cons(sk5,nil),u)* -> memberP(sk1,u). % 34.78/34.98 3780[11:Res:1891.0,3778.0] || -> memberP(sk1,sk8)*. % 34.78/34.98 3781[11:Res:3780.0,2677.0] || -> equal(sk9,sk8)**. % 34.78/34.98 3789[11:Rew:3781.0,2677.1] || memberP(sk1,u)* -> equal(u,sk8). % 34.78/34.98 3792[11:Rew:3781.0,3018.0] || -> totalorderedP(cons(sk8,sk1))*. % 34.78/34.98 3796[11:Rew:3781.0,3029.1] || totalorderedP(cons(u,sk1))* -> leq(u,sk8). % 34.78/34.98 3971[11:Res:590.2,3779.0] ssList(nil) || equal(u,sk5) -> memberP(sk1,u)*. % 34.78/34.98 3973[11:SSi:3971.0,27.0,26.0,25.0,24.0,23.0,22.0,21.0,20.0] || equal(u,sk5) -> memberP(sk1,u)*. % 34.78/34.98 4040[11:Res:3973.1,3789.0] || equal(u,sk5) -> equal(u,sk8)*. % 34.78/34.98 4162[11:SpR:4040.1,3792.0] || equal(u,sk5) -> totalorderedP(cons(u,sk1))*. % 34.78/34.98 4238[11:SpL:4040.1,15.1] || equal(u,sk5) leq(sk5,sk8)* leq(u,sk5)* -> . % 34.78/34.98 4373[11:SpR:168.3,2859.0] ssList(sk6) ssList(cons(sk5,nil)) ssList(sk1) || -> equal(app(sk6,app(cons(sk5,nil),sk1)),sk1)**. % 34.78/34.98 4409[11:Rew:2860.0,4373.3] ssList(sk6) ssList(cons(sk5,nil)) ssList(sk1) || -> equal(app(sk6,cons(sk5,sk1)),sk1)**. % 34.78/34.98 4410[11:SSi:4409.2,4409.1,4409.0,1.0,1925.0,1930.0,1932.0,1936.0,1938.0,1942.0,1944.0,2052.0,625.0,27.0,26.0,25.0,24.0,23.0,22.0,21.0,20.1,495.0,496.0,497.0,498.0,499.0,500.0,501.0,2047.0,8.0] || -> equal(app(sk6,cons(sk5,sk1)),sk1)**. % 34.78/34.98 5185[11:Res:4162.1,3796.0] || equal(u,sk5) -> leq(u,sk8)*. % 34.78/34.98 6396[11:SpL:4410.0,639.3] ssList(u) ssList(sk6) ssList(sk1) || equal(sk1,u) -> memberP(u,sk5)*. % 34.78/34.98 6401[11:SSi:6396.2,6396.1,1.0,1925.0,1930.0,1932.0,1936.0,1938.0,1942.0,1944.0,2052.0,8.0] ssList(u) || equal(sk1,u) -> memberP(u,sk5)*. % 34.78/34.98 7101[11:Res:6401.2,3789.0] ssList(sk1) || equal(sk1,sk1) -> equal(sk8,sk5)**. % 34.78/34.98 7111[11:Obv:7101.1] ssList(sk1) || -> equal(sk8,sk5)**. % 34.78/34.98 7112[11:SSi:7111.0,1.0,1925.0,1930.0,1932.0,1936.0,1938.0,1942.0,1944.0,2052.0] || -> equal(sk8,sk5)**. % 34.78/34.98 7137[11:Rew:7112.0,5185.1] || equal(u,sk5) -> leq(u,sk5)*. % 34.78/34.98 7280[11:Rew:7112.0,4238.1] || equal(u,sk5) leq(sk5,sk5)* leq(u,sk5)* -> . % 34.78/34.98 7470[11:MRR:7280.1,491.0] || equal(u,sk5) leq(u,sk5)* -> . % 34.78/34.98 7471[11:MRR:7470.1,7137.1] || equal(u,sk5)* -> . % 34.78/34.98 7472[11:UnC:7471.0,2828.0] || -> . % 34.78/34.98 7495[11:Spt:7472.0,2292.1,2294.0] || equal(skaf82(sk7),nil)** -> . % 34.78/34.98 7496[11:Spt:7472.0,2292.0] || -> totalorderedP(skaf82(sk7))*. % 34.78/34.98 7501[1:SSi:2641.0,2047.0,501.0,500.0,499.0,498.0,497.0,496.0,495.0,625.1,20.0,21.0,22.0,23.0,24.0,25.0,26.0,27.0] || -> equal(cons(u,nil),nil) equal(skaf83(cons(u,nil)),u)**. % 34.78/34.98 7502[1:SSi:2572.0,104.0,8.0,2047.0,501.0,500.0,499.0,498.0,497.0,496.1,495.0,625.0,20.0,21.0,22.0,23.0,24.0,25.0,26.0,27.2] ssList(sk7) || memberP(sk7,u)* -> memberP(sk1,u). % 34.78/34.98 7503[1:MRR:7502.0,9.0] || memberP(sk7,u)* -> memberP(sk1,u). % 34.78/34.98 7510[1:SSi:2585.0,104.0,8.0,2047.0,501.0,500.0,499.0,498.0,497.0,496.1,495.0,625.0,20.0,21.0,22.0,23.0,24.0,25.0,26.0,27.2] ssList(sk7) || memberP(app(sk6,cons(sk5,nil)),u)* -> memberP(sk1,u). % 34.78/34.98 7511[1:MRR:7510.0,9.0] || memberP(app(sk6,cons(sk5,nil)),u)* -> memberP(sk1,u). % 34.78/34.98 7534[12:Spt:208.0] || neq(sk2,nil)* -> . % 34.78/34.98 7535[12:Res:529.1,7534.0] || -> equal(nil,sk2)**. % 34.78/34.98 7536[12:MRR:7535.0,1857.0] || -> . % 34.78/34.98 7537[12:Spt:7536.0,208.0,7534.0] || -> neq(sk2,nil)*. % 34.78/34.98 7538[12:Spt:7536.0,208.1] || -> memberP(sk2,sk9)*. % 34.78/34.98 7540[12:MRR:210.0,7537.0] || -> equal(cons(sk9,nil),sk1)**. % 34.78/34.98 7543[12:MRR:2611.0,7537.0] || memberP(sk1,u)* -> equal(u,sk9). % 34.78/34.98 7544[12:MRR:1970.0,7537.0] || -> equal(app(sk1,sk7),cons(sk9,sk7))**. % 34.78/34.98 7546[12:MRR:2045.1,7537.0] ssList(u) || equal(sk1,u) -> singletonP(u)*. % 34.78/34.98 7548[12:MRR:2126.1,7537.0] ssList(u) || -> equal(app(sk1,u),cons(sk9,u))**. % 34.78/34.98 7699[0:SpR:10.0,168.3] ssList(sk6) ssList(cons(sk5,nil)) ssList(sk7) || -> equal(app(sk6,app(cons(sk5,nil),sk7)),sk1)**. % 34.78/34.98 7712[1:Rew:631.1,7699.3] ssList(sk6) ssList(cons(sk5,nil)) ssList(sk7) || -> equal(app(sk6,cons(sk5,sk7)),sk1)**. % 34.78/34.98 7713[9:SSi:7712.2,7712.1,7712.0,9.0,1886.0,1885.0,1883.0,1879.0,1876.0,2047.0,501.0,500.0,499.1,498.0,497.0,496.0,495.0,625.0,20.0,21.0,22.0,23.0,24.0,25.0,26.0,27.0,8.0] || -> equal(app(sk6,cons(sk5,sk7)),sk1)**. % 34.78/34.98 7910[9:SpR:7713.0,588.3] ssList(sk6) ssList(cons(sk5,sk7)) || memberP(sk6,u)* -> memberP(sk1,u). % 34.78/34.98 7911[9:SpR:7713.0,587.3] ssList(sk6) ssList(cons(sk5,sk7)) || memberP(cons(sk5,sk7),u)* -> memberP(sk1,u). % 34.78/34.98 7914[9:SpR:7713.0,2196.3] ssList(sk6) ssList(cons(sk5,sk7)) || -> equal(nil,sk6) equal(hd(sk1),skaf83(sk6))**. % 34.78/34.98 7929[9:SSi:7910.1,7910.0,625.0,9.0,1886.0,1885.0,1883.0,1879.0,1876.0,8.1] || memberP(sk6,u)* -> memberP(sk1,u). % 34.78/34.98 7930[9:Rew:1952.0,7914.3] ssList(sk6) ssList(cons(sk5,sk7)) || -> equal(nil,sk6) equal(skaf83(sk6),sk9)**. % 34.78/34.98 7931[9:SSi:7930.1,7930.0,625.0,9.0,1886.0,1885.0,1883.0,1879.0,1876.0,8.1] || -> equal(nil,sk6) equal(skaf83(sk6),sk9)**. % 34.78/34.98 7933[9:SSi:7911.1,7911.0,625.0,9.0,1886.0,1885.0,1883.0,1879.0,1876.0,8.1] || memberP(cons(sk5,sk7),u)* -> memberP(sk1,u). % 34.78/34.98 8016[13:Spt:7931.0] || -> equal(nil,sk6)**. % 34.78/34.98 8038[13:Rew:8016.0,494.0] || memberP(sk6,u)* -> . % 34.78/34.98 8280[13:UnC:8038.0,1891.0] || -> . % 34.78/34.98 8390[13:Spt:8280.0,7931.0,8016.0] || equal(nil,sk6)** -> . % 34.78/34.98 8391[13:Spt:8280.0,7931.1] || -> equal(skaf83(sk6),sk9)**. % 34.78/34.98 8567[10:Res:1891.0,7929.0] || -> memberP(sk1,sk8)*. % 34.78/34.98 8568[12:Res:8567.0,7543.0] || -> equal(sk9,sk8)**. % 34.78/34.98 8572[12:Rew:8568.0,7544.0] || -> equal(app(sk1,sk7),cons(sk8,sk7))**. % 34.78/34.98 8573[13:Rew:8568.0,8391.0] || -> equal(skaf83(sk6),sk8)**. % 34.78/34.98 8574[12:Rew:8568.0,7540.0] || -> equal(cons(sk8,nil),sk1)**. % 34.78/34.98 8575[12:Rew:8568.0,7543.1] || memberP(sk1,u)* -> equal(u,sk8). % 34.78/34.98 8586[12:Rew:8568.0,7548.1] ssList(u) || -> equal(app(sk1,u),cons(sk8,u))**. % 34.78/34.98 8677[9:Res:2153.1,7503.0] || equal(u,skaf83(sk7)) -> memberP(sk1,u)*. % 34.78/34.98 8684[12:Res:8677.1,8575.0] || equal(u,skaf83(sk7))* -> equal(u,sk8). % 34.78/34.98 8685[12:EqR:8684.0] || -> equal(skaf83(sk7),sk8)**. % 34.78/34.98 8687[12:Rew:8685.0,1864.0] || strictorderedP(cons(sk8,sk7))* -> . % 34.78/34.98 8786[9:Res:590.2,7933.0] ssList(sk7) || equal(u,sk5) -> memberP(sk1,u)*. % 34.78/34.98 8788[9:SSi:8786.0,9.0,1886.0,1885.0,1883.0,1879.0,1876.0] || equal(u,sk5) -> memberP(sk1,u)*. % 34.78/34.98 8789[12:Res:8788.1,8575.0] || equal(u,sk5) -> equal(u,sk8)*. % 34.78/34.98 8968[12:SpR:8789.1,8574.0] || equal(u,sk5) -> equal(cons(u,nil),sk1)**. % 34.78/34.98 9226[13:SpR:8573.0,128.2] ssList(sk6) || -> equal(nil,sk6) equal(cons(sk8,skaf82(sk6)),sk6)**. % 34.78/34.98 9242[13:SSi:9226.0,8.0] || -> equal(nil,sk6) equal(cons(sk8,skaf82(sk6)),sk6)**. % 34.78/34.98 9243[13:MRR:9242.0,8390.0] || -> equal(cons(sk8,skaf82(sk6)),sk6)**. % 34.78/34.98 9246[13:SpR:9243.0,629.1] ssList(skaf82(sk6)) || -> equal(tl(sk6),skaf82(sk6))**. % 34.78/34.98 9274[13:SSi:9246.0,32.0,8.0] || -> equal(tl(sk6),skaf82(sk6))**. % 34.78/34.98 9300[13:SpL:9243.0,561.1] ssList(skaf82(sk6)) || totalorderedP(sk6) -> totalorderedP(skaf82(sk6))* equal(skaf82(sk6),nil). % 34.78/34.98 9308[13:SSi:9300.0,32.0,8.0] || totalorderedP(sk6) -> totalorderedP(skaf82(sk6))* equal(skaf82(sk6),nil). % 34.78/34.98 9919[12:SpR:8968.1,10.0] || equal(sk5,sk5) -> equal(app(app(sk6,sk1),sk7),sk1)**. % 34.78/34.98 9981[12:Obv:9919.0] || -> equal(app(app(sk6,sk1),sk7),sk1)**. % 34.78/34.98 10019[12:SpR:9981.0,168.3] ssList(sk6) ssList(sk1) ssList(sk7) || -> equal(app(sk6,app(sk1,sk7)),sk1)**. % 34.78/34.98 10035[12:Rew:8572.0,10019.3] ssList(sk6) ssList(sk1) ssList(sk7) || -> equal(app(sk6,cons(sk8,sk7)),sk1)**. % 34.78/34.98 10036[12:SSi:10035.2,10035.1,10035.0,9.0,1886.0,1885.0,1883.0,1879.0,1876.0,1.0,1925.0,1930.0,1932.0,1936.0,1938.0,1942.0,1944.0,2052.0,8.0] || -> equal(app(sk6,cons(sk8,sk7)),sk1)**. % 34.78/34.98 10576[14:Spt:9308.2] || -> equal(skaf82(sk6),nil)**. % 34.78/34.98 10577[14:Rew:10576.0,9243.0] || -> equal(cons(sk8,nil),sk6)**. % 34.78/34.98 10610[14:Rew:8574.0,10577.0] || -> equal(sk6,sk1)**. % 34.78/34.98 10624[14:Rew:10610.0,9981.0] || -> equal(app(app(sk1,sk1),sk7),sk1)**. % 34.78/34.98 11296[14:SpR:8586.1,10624.0] ssList(sk1) || -> equal(app(cons(sk8,sk1),sk7),sk1)**. % 34.78/34.98 11318[14:Rew:632.1,11296.1] ssList(sk1) || -> equal(cons(sk8,app(sk1,sk7)),sk1)**. % 34.78/34.98 11319[14:Rew:8572.0,11318.1] ssList(sk1) || -> equal(cons(sk8,cons(sk8,sk7)),sk1)**. % 34.78/34.98 11320[14:SSi:11319.0,1.0,1925.0,1930.0,1932.0,1936.0,1938.0,1942.0,1944.0,2052.0] || -> equal(cons(sk8,cons(sk8,sk7)),sk1)**. % 34.78/34.98 11379[14:SpL:11320.0,562.1] ssList(cons(sk8,sk7)) || strictorderedP(sk1) -> strictorderedP(cons(sk8,sk7))* equal(cons(sk8,sk7),nil). % 34.78/34.98 11411[14:SSi:11379.0,625.0,9.0,1886.0,1885.0,1883.0,1879.0,1876.1] || strictorderedP(sk1) -> strictorderedP(cons(sk8,sk7))* equal(cons(sk8,sk7),nil). % 34.78/34.98 11412[14:MRR:11411.0,11411.1,11411.2,1938.0,8687.0,504.0] || -> . % 34.78/34.98 11422[14:Spt:11412.0,9308.2,10576.0] || equal(skaf82(sk6),nil)** -> . % 34.78/34.98 11423[14:Spt:11412.0,9308.0,9308.1] || totalorderedP(sk6) -> totalorderedP(skaf82(sk6))*. % 34.78/34.98 11441[13:SpR:9274.0,2113.2] ssList(sk6) singletonP(sk6) || -> equal(skaf82(sk6),nil)**. % 34.78/34.98 11443[13:SSi:11441.0,8.0] singletonP(sk6) || -> equal(skaf82(sk6),nil)**. % 34.78/34.98 11444[14:MRR:11443.1,11422.0] singletonP(sk6) || -> . % 34.78/34.98 11446[14:SoR:11444.0,7546.2] ssList(sk6) || equal(sk6,sk1)** -> . % 34.78/34.98 11447[14:SSi:11446.0,8.0] || equal(sk6,sk1)** -> . % 34.78/34.98 11634[1:Res:588.3,7511.0] ssList(sk6) ssList(cons(sk5,nil)) || memberP(sk6,u)* -> memberP(sk1,u). % 34.78/34.98 11635[1:Res:587.3,7511.0] ssList(sk6) ssList(cons(sk5,nil)) || memberP(cons(sk5,nil),u)* -> memberP(sk1,u). % 34.78/34.98 11637[1:SSi:11635.1,11635.0,495.0,496.0,497.0,498.0,499.0,500.0,501.0,2047.0,625.0,27.1,26.0,25.0,24.0,23.0,22.0,21.0,20.0,8.0] || memberP(cons(sk5,nil),u)* -> memberP(sk1,u). % 34.78/34.98 11657[1:SpR:120.2,7501.1] ssList(u) singletonP(u) || -> equal(cons(skaf44(u),nil),nil)** equal(skaf44(u),skaf83(u)). % 34.78/34.98 11659[1:Rew:120.2,11657.2] ssList(u) singletonP(u) || -> equal(u,nil) equal(skaf44(u),skaf83(u))**. % 34.78/34.98 11660[1:MRR:11659.2,2114.2] ssList(u) singletonP(u) || -> equal(skaf44(u),skaf83(u))**. % 34.78/34.98 11662[1:Rew:11660.2,2115.2] ssList(u) singletonP(u) || -> equal(hd(u),skaf83(u))**. % 34.78/34.98 11784[1:Res:590.2,11637.0] ssList(nil) || equal(u,sk5) -> memberP(sk1,u)*. % 34.78/34.98 11839[4:SpR:2185.2,1948.0] ssList(sk1) || -> equal(nil,sk1) equal(skaf82(sk1),nil)**. % 34.78/34.98 12044[12:SpR:8586.1,3511.2] ssList(u) ssList(sk1) ssList(u) || -> frontsegP(cons(sk8,u),sk1)*. % 34.78/34.98 12053[12:SpR:10036.0,3511.2] ssList(sk6) ssList(cons(sk8,sk7)) || -> frontsegP(sk1,sk6)*. % 34.78/34.98 12068[12:SSi:12053.1,12053.0,625.0,9.0,1886.0,1885.0,1883.0,1879.0,1876.0,8.1] || -> frontsegP(sk1,sk6)*. % 34.78/34.98 12073[12:Obv:12044.0] ssList(sk1) ssList(u) || -> frontsegP(cons(sk8,u),sk1)*. % 34.78/34.98 12074[12:SSi:12073.0,1.0,1925.0,1930.0,1932.0,1936.0,1938.0,1942.0,1944.0,2052.0] ssList(u) || -> frontsegP(cons(sk8,u),sk1)*. % 34.78/34.98 12102[12:Res:12068.0,148.2] ssList(sk1) ssList(sk6) || frontsegP(sk6,sk1)* -> equal(sk6,sk1). % 34.78/34.98 12103[12:SSi:12102.1,12102.0,8.0,1.0,1925.0,1930.0,1932.0,1936.0,1938.0,1942.0,1944.0,2052.0] || frontsegP(sk6,sk1)* -> equal(sk6,sk1). % 34.78/34.98 12104[14:MRR:12103.1,11447.0] || frontsegP(sk6,sk1)* -> . % 34.78/34.98 12264[13:SpR:9243.0,12074.1] ssList(skaf82(sk6)) || -> frontsegP(sk6,sk1)*. % 34.78/34.98 12271[13:SSi:12264.0,32.0,8.0] || -> frontsegP(sk6,sk1)*. % 34.78/34.98 12272[14:MRR:12271.0,12104.0] || -> . % 34.78/34.98 12275[10:Spt:12272.0,12.1,1891.0] || memberP(sk6,sk8)* -> . % 34.78/34.98 12276[10:Spt:12272.0,12.0] || -> memberP(sk7,sk8)*. % 34.78/34.98 12278[4:SSi:11839.0,1.0,1925.0,1930.0,1932.0,1936.0,1938.0,1942.0,1944.0,2052.0] || -> equal(nil,sk1) equal(skaf82(sk1),nil)**. % 34.78/34.98 12279[4:MRR:12278.0,1856.0] || -> equal(skaf82(sk1),nil)**. % 34.78/34.98 12306[10:Res:12276.0,7503.0] || -> memberP(sk1,sk8)*. % 34.78/34.98 12311[4:SpR:1952.0,11662.2] ssList(sk1) singletonP(sk1) || -> equal(skaf83(sk1),sk9)**. % 34.78/34.98 12315[4:SSi:12311.1,12311.0,1.0,1925.0,1930.0,1932.0,1936.0,1938.0,1942.0,1944.0,2052.0,1.0,1925.0,1930.0,1932.0,1936.0,1938.0,1942.0,1944.0,2052.0] || -> equal(skaf83(sk1),sk9)**. % 34.78/34.98 12317[4:SpR:12279.0,128.2] ssList(sk1) || -> equal(nil,sk1) equal(cons(skaf83(sk1),nil),sk1)**. % 34.78/34.98 12323[4:Rew:12315.0,12317.2] ssList(sk1) || -> equal(nil,sk1) equal(cons(sk9,nil),sk1)**. % 34.78/34.98 12324[4:SSi:12323.0,1.0,1925.0,1930.0,1932.0,1936.0,1938.0,1942.0,1944.0,2052.0] || -> equal(nil,sk1) equal(cons(sk9,nil),sk1)**. % 34.78/34.98 12325[4:MRR:12324.0,1856.0] || -> equal(cons(sk9,nil),sk1)**. % 34.78/34.98 12340[11:Spt:208.0] || neq(sk2,nil)* -> . % 34.78/34.98 12341[11:Res:529.1,12340.0] || -> equal(nil,sk2)**. % 34.78/34.98 12342[11:MRR:12341.0,1857.0] || -> . % 34.78/34.98 12343[11:Spt:12342.0,208.0,12340.0] || -> neq(sk2,nil)*. % 34.78/34.98 12344[11:Spt:12342.0,208.1] || -> memberP(sk2,sk9)*. % 34.78/34.98 12345[11:MRR:2206.0,12343.0] || equal(cons(u,sk7),sk1)** -> . % 34.78/34.98 12348[11:MRR:2611.0,12343.0] || memberP(sk1,u)* -> equal(u,sk9). % 34.78/34.98 12389[4:SpL:12325.0,2168.0] || equal(cons(u,sk7),sk1)** -> . % 34.78/34.98 12394[4:SpL:12325.0,609.1] ssList(nil) || memberP(sk1,u) -> equal(u,sk9) memberP(nil,u)*. % 34.78/34.98 12511[12:Spt:7931.0] || -> equal(nil,sk6)**. % 34.78/34.98 12550[12:Rew:12511.0,93.1] ssList(u) || -> equal(app(sk6,u),u)**. % 34.78/34.98 13082[12:SpR:12550.1,7713.0] ssList(cons(sk5,sk7)) || -> equal(cons(sk5,sk7),sk1)**. % 34.78/34.98 13105[12:SSi:13082.0,625.0,9.0,1886.0,1885.0,1883.0,1879.0,1876.1] || -> equal(cons(sk5,sk7),sk1)**. % 34.78/34.98 13106[12:MRR:13105.0,12345.0] || -> . % 34.78/34.98 13122[12:Spt:13106.0,7931.0,12511.0] || equal(nil,sk6)** -> . % 34.78/34.98 13123[12:Spt:13106.0,7931.1] || -> equal(skaf83(sk6),sk9)**. % 34.78/34.98 13536[11:Res:12306.0,12348.0] || -> equal(sk9,sk8)**. % 34.78/34.98 13545[12:Rew:13536.0,13123.0] || -> equal(skaf83(sk6),sk8)**. % 34.78/34.98 14228[12:SpR:13545.0,128.2] ssList(sk6) || -> equal(nil,sk6) equal(cons(sk8,skaf82(sk6)),sk6)**. % 34.78/34.98 14256[12:SSi:14228.0,8.0] || -> equal(nil,sk6) equal(cons(sk8,skaf82(sk6)),sk6)**. % 34.78/34.98 14257[12:MRR:14256.0,13122.0] || -> equal(cons(sk8,skaf82(sk6)),sk6)**. % 34.78/34.98 14271[12:SpR:14257.0,590.2] ssList(skaf82(sk6)) || equal(u,sk8) -> memberP(sk6,u)*. % 34.78/34.98 14311[12:SSi:14271.0,32.0,8.0] || equal(u,sk8) -> memberP(sk6,u)*. % 34.78/34.98 14358[12:Res:14311.1,12275.0] || equal(sk8,sk8)* -> . % 34.78/34.98 14360[12:Obv:14358.0] || -> . % 34.78/34.98 14363[9:Spt:14360.0,333.0,1886.0] || totalorderP(sk7)* -> . % 34.78/34.98 14364[9:Spt:14360.0,333.1] || -> equal(app(app(skaf56(sk7),cons(skaf54(sk7),skaf57(sk7))),cons(skaf55(sk7),skaf58(sk7))),sk7)**. % 34.78/34.98 14370[1:SSi:11784.0,20.0,21.0,22.0,23.0,24.0,25.0,26.0,27.0] || equal(u,sk5) -> memberP(sk1,u)*. % 34.78/34.98 14373[8:SSi:2149.0,32.0,9.0,1885.0,1883.0,1879.0,1876.0] || equal(u,skaf83(sk7)) -> memberP(sk7,u)*. % 34.78/34.98 14374[4:SSi:12394.0,20.0,21.0,22.0,23.0,24.0,25.0,26.0,27.0] || memberP(sk1,u) -> equal(u,sk9) memberP(nil,u)*. % 34.78/34.98 14375[4:MRR:14374.2,494.0] || memberP(sk1,u)* -> equal(u,sk9). % 34.78/34.98 14377[8:SSi:2282.0,32.0,9.0,1885.0,1883.0,1879.0,1876.0] || totalorderedP(sk7) -> totalorderedP(skaf82(sk7))* equal(skaf82(sk7),nil). % 34.78/34.98 14378[8:MRR:14377.0,1879.0] || -> totalorderedP(skaf82(sk7))* equal(skaf82(sk7),nil). % 34.78/34.98 14383[1:SSi:11634.1,11634.0,501.0,2047.0,500.0,499.0,498.0,497.0,496.0,495.0,625.0,20.1,21.0,22.0,23.0,24.0,25.0,26.0,27.0,8.0] || memberP(sk6,u)* -> memberP(sk1,u). % 34.78/34.98 14400[8:SSi:7712.2,7712.1,7712.0,9.0,1885.0,1883.0,1879.0,1876.0,501.0,2047.0,500.0,499.0,498.1,497.0,496.0,495.0,625.0,20.0,21.0,22.0,23.0,24.0,25.0,26.0,27.0,8.0] || -> equal(app(sk6,cons(sk5,sk7)),sk1)**. % 34.78/34.98 14499[9:Res:2094.2,14363.0] ssList(sk7) singletonP(sk7) || -> . % 34.78/34.98 14500[9:SSi:14499.0,9.0,1885.0,1883.0,1879.0,1876.0] singletonP(sk7) || -> . % 34.78/34.98 14501[9:MRR:519.1,14500.0] || equal(cons(u,nil),sk7)** -> . % 34.78/34.98 14503[10:Spt:12.0] || -> memberP(sk7,sk8)*. % 34.78/34.98 14504[10:Res:14503.0,7503.0] || -> memberP(sk1,sk8)*. % 34.78/34.98 14514[11:Spt:208.0] || neq(sk2,nil)* -> . % 34.78/34.98 14515[11:Res:529.1,14514.0] || -> equal(nil,sk2)**. % 34.78/34.98 14516[11:MRR:14515.0,1857.0] || -> . % 34.78/34.98 14517[11:Spt:14516.0,208.0,14514.0] || -> neq(sk2,nil)*. % 34.78/34.98 14518[11:Spt:14516.0,208.1] || -> memberP(sk2,sk9)*. % 34.78/34.98 14703[12:Spt:14378.1] || -> equal(skaf82(sk7),nil)**. % 34.78/34.98 14706[12:Rew:14703.0,1625.0] || -> equal(cons(skaf83(sk7),nil),sk7)**. % 34.78/34.98 14716[12:MRR:14706.0,14501.0] || -> . % 34.78/34.98 14724[12:Spt:14716.0,14378.1,14703.0] || equal(skaf82(sk7),nil)** -> . % 34.78/34.98 14725[12:Spt:14716.0,14378.0] || -> totalorderedP(skaf82(sk7))*. % 34.78/34.98 14886[4:Res:14370.1,14375.0] || equal(u,sk5) -> equal(u,sk9)*. % 34.78/34.98 14888[10:Res:14504.0,14375.0] || -> equal(sk9,sk8)**. % 34.78/34.98 14891[10:Rew:14888.0,1952.0] || -> equal(hd(sk1),sk8)**. % 34.78/34.98 14932[10:Rew:14888.0,14886.1] || equal(u,sk5) -> equal(u,sk8)*. % 34.78/34.98 14960[8:SpR:14400.0,2196.3] ssList(sk6) ssList(cons(sk5,sk7)) || -> equal(nil,sk6) equal(hd(sk1),skaf83(sk6))**. % 34.78/34.98 14969[10:Rew:14891.0,14960.3] ssList(sk6) ssList(cons(sk5,sk7)) || -> equal(nil,sk6) equal(skaf83(sk6),sk8)**. % 34.78/34.98 14970[10:SSi:14969.1,14969.0,625.0,9.0,1885.0,1883.0,1879.0,1876.0,8.1] || -> equal(nil,sk6) equal(skaf83(sk6),sk8)**. % 34.78/34.98 15138[13:Spt:14970.0] || -> equal(nil,sk6)**. % 34.78/34.98 15178[13:Rew:15138.0,93.1] ssList(u) || -> equal(app(sk6,u),u)**. % 34.78/34.98 16058[13:SpR:15178.1,14400.0] ssList(cons(sk5,sk7)) || -> equal(cons(sk5,sk7),sk1)**. % 34.78/34.98 16082[13:SSi:16058.0,625.0,9.0,1885.0,1883.0,1879.0,1876.1] || -> equal(cons(sk5,sk7),sk1)**. % 34.78/34.98 16083[13:MRR:16082.0,12389.0] || -> . % 34.78/34.98 16100[13:Spt:16083.0,14970.0,15138.0] || equal(nil,sk6)** -> . % 34.78/34.98 16101[13:Spt:16083.0,14970.1] || -> equal(skaf83(sk6),sk8)**. % 34.78/34.98 16246[14:Spt:15.0] || leq(sk5,sk8)* -> . % 34.78/34.98 16249[14:SpL:14932.1,16246.0] || equal(u,sk5) leq(sk5,u)* -> . % 34.78/34.98 16453[8:Res:14373.1,7503.0] || equal(u,skaf83(sk7)) -> memberP(sk1,u)*. % 34.78/34.98 16484[14:Res:491.0,16249.1] || equal(sk5,sk5)* -> . % 34.78/34.98 16485[14:Obv:16484.0] || -> . % 34.78/34.98 16486[14:Spt:16485.0,15.0,16246.0] || -> leq(sk5,sk8)*. % 34.78/34.98 16487[14:Spt:16485.0,15.1] || leq(sk8,sk5)* -> . % 34.78/34.98 16492[14:SpL:14932.1,16487.0] || equal(u,sk5) leq(u,sk5)* -> . % 34.78/34.98 16495[14:SpR:14932.1,16486.0] || equal(u,sk5) -> leq(sk5,u)*. % 34.78/34.98 16835[14:Res:16495.1,16492.1] || equal(sk5,sk5)* equal(sk5,sk5)* -> . % 34.78/34.98 16837[14:Obv:16835.1] || -> . % 34.78/34.98 16838[10:Spt:16837.0,12.0,14503.0] || memberP(sk7,sk8)* -> . % 34.78/34.98 16839[10:Spt:16837.0,12.1] || -> memberP(sk6,sk8)*. % 34.78/34.98 16850[10:Res:16839.0,14383.0] || -> memberP(sk1,sk8)*. % 34.78/34.98 16851[10:Res:14373.1,16838.0] || equal(skaf83(sk7),sk8)** -> . % 34.78/34.98 17618[8:Res:16453.1,14375.0] || equal(u,skaf83(sk7))* -> equal(u,sk9). % 34.78/34.98 17620[10:Res:16850.0,14375.0] || -> equal(sk9,sk8)**. % 34.78/34.98 17667[10:Rew:17620.0,17618.1] || equal(u,skaf83(sk7))* -> equal(u,sk8). % 34.78/34.98 18341[10:EqR:17667.0] || -> equal(skaf83(sk7),sk8)**. % 34.78/34.98 18343[10:MRR:18341.0,16851.0] || -> . % 34.78/34.98 18344[8:Spt:18343.0,334.0,1885.0] || strictorderP(sk7)* -> . % 34.78/34.98 18345[8:Spt:18343.0,334.1] || -> equal(app(app(skaf61(sk7),cons(skaf59(sk7),skaf62(sk7))),cons(skaf60(sk7),skaf63(sk7))),sk7)**. % 34.78/34.98 18351[7:SSi:2149.0,32.0,9.0,1883.0,1879.0,1876.0] || equal(u,skaf83(sk7)) -> memberP(sk7,u)*. % 34.78/34.98 18502[9:Spt:12.0] || -> memberP(sk7,sk8)*. % 34.78/34.98 18503[9:Res:18502.0,7503.0] || -> memberP(sk1,sk8)*. % 34.78/34.98 18836[4:Res:14370.1,14375.0] || equal(u,sk5) -> equal(u,sk9)*. % 34.78/34.98 18837[9:Res:18503.0,14375.0] || -> equal(sk9,sk8)**. % 34.78/34.98 18844[9:Rew:18837.0,208.1] || neq(sk2,nil) -> memberP(sk2,sk8)*. % 34.78/34.98 18882[9:Rew:18837.0,18836.1] || equal(u,sk5) -> equal(u,sk8)*. % 34.78/34.98 19284[9:SpL:18882.1,15.1] || equal(u,sk5) leq(sk5,sk8)* leq(u,sk5)* -> . % 34.78/34.98 20326[10:Spt:18844.0] || neq(sk2,nil)* -> . % 34.78/34.98 20327[10:Res:529.1,20326.0] || -> equal(nil,sk2)**. % 34.78/34.98 20328[10:MRR:20327.0,1857.0] || -> . % 34.78/34.98 20329[10:Spt:20328.0,18844.0,20326.0] || -> neq(sk2,nil)*. % 34.78/34.98 20330[10:Spt:20328.0,18844.1] || -> memberP(sk2,sk8)*. % 34.78/34.98 20341[11:Spt:13.0] || leq(sk5,sk8)* -> . % 34.78/34.98 20344[11:SpL:18882.1,20341.0] || equal(u,sk5) leq(sk5,u)* -> . % 34.78/34.98 20507[7:Res:18351.1,7503.0] || equal(u,skaf83(sk7)) -> memberP(sk1,u)*. % 34.78/34.98 20535[11:Res:491.0,20344.1] || equal(sk5,sk5)* -> . % 34.78/34.98 20536[11:Obv:20535.0] || -> . % 34.78/34.98 20537[11:Spt:20536.0,13.0,20341.0] || -> leq(sk5,sk8)*. % 34.78/34.98 20538[11:Spt:20536.0,13.1] || -> memberP(sk6,sk8)*. % 34.78/34.98 20541[11:MRR:19284.1,20537.0] || equal(u,sk5) leq(u,sk5)* -> . % 34.78/34.98 20548[11:SpR:18882.1,20537.0] || equal(u,sk5) -> leq(sk5,u)*. % 34.78/34.98 20597[11:Res:20548.1,20541.1] || equal(sk5,sk5)* equal(sk5,sk5)* -> . % 34.78/34.98 20599[11:Obv:20597.1] || -> . % 34.78/34.98 20600[9:Spt:20599.0,12.0,18502.0] || memberP(sk7,sk8)* -> . % 34.78/34.98 20601[9:Spt:20599.0,12.1] || -> memberP(sk6,sk8)*. % 34.78/34.98 20607[9:Res:20601.0,14383.0] || -> memberP(sk1,sk8)*. % 34.78/34.98 20608[9:Res:18351.1,20600.0] || equal(skaf83(sk7),sk8)** -> . % 34.78/34.98 21340[7:Res:20507.1,14375.0] || equal(u,skaf83(sk7))* -> equal(u,sk9). % 34.78/34.98 21342[9:Res:20607.0,14375.0] || -> equal(sk9,sk8)**. % 34.78/34.98 21389[9:Rew:21342.0,21340.1] || equal(u,skaf83(sk7))* -> equal(u,sk8). % 34.78/34.98 22123[9:EqR:21389.0] || -> equal(skaf83(sk7),sk8)**. % 34.78/34.98 22125[9:MRR:22123.0,20608.0] || -> . % 34.78/34.98 22126[7:Spt:22125.0,392.0,1883.0] || cyclefreeP(sk7)* -> . % 34.78/34.98 22127[7:Spt:22125.0,392.1] || -> leq(skaf50(sk7),skaf49(sk7))*. % 34.78/34.98 22132[6:SSi:2149.0,32.0,9.0,1879.0,1876.0] || equal(u,skaf83(sk7)) -> memberP(sk7,u)*. % 34.78/34.98 22234[8:Spt:12.0] || -> memberP(sk7,sk8)*. % 34.78/34.98 22235[8:Res:22234.0,7503.0] || -> memberP(sk1,sk8)*. % 34.78/34.98 22520[4:Res:14370.1,14375.0] || equal(u,sk5) -> equal(u,sk9)*. % 34.78/34.98 22521[8:Res:22235.0,14375.0] || -> equal(sk9,sk8)**. % 34.78/34.98 22528[8:Rew:22521.0,208.1] || neq(sk2,nil) -> memberP(sk2,sk8)*. % 34.78/34.98 22566[8:Rew:22521.0,22520.1] || equal(u,sk5) -> equal(u,sk8)*. % 34.78/34.98 22954[8:SpL:22566.1,15.1] || equal(u,sk5) leq(sk5,sk8)* leq(u,sk5)* -> . % 34.78/34.98 23978[9:Spt:22528.0] || neq(sk2,nil)* -> . % 34.78/34.98 23979[9:Res:529.1,23978.0] || -> equal(nil,sk2)**. % 34.78/34.98 23980[9:MRR:23979.0,1857.0] || -> . % 34.78/34.98 23981[9:Spt:23980.0,22528.0,23978.0] || -> neq(sk2,nil)*. % 34.78/34.98 23982[9:Spt:23980.0,22528.1] || -> memberP(sk2,sk8)*. % 34.78/34.98 23993[10:Spt:13.0] || leq(sk5,sk8)* -> . % 34.78/34.98 23996[10:SpL:22566.1,23993.0] || equal(u,sk5) leq(sk5,u)* -> . % 34.78/34.98 24168[6:Res:22132.1,7503.0] || equal(u,skaf83(sk7)) -> memberP(sk1,u)*. % 34.78/34.98 24193[10:Res:491.0,23996.1] || equal(sk5,sk5)* -> . % 34.78/34.98 24194[10:Obv:24193.0] || -> . % 34.78/34.98 24195[10:Spt:24194.0,13.0,23993.0] || -> leq(sk5,sk8)*. % 34.78/34.98 24196[10:Spt:24194.0,13.1] || -> memberP(sk6,sk8)*. % 34.78/34.98 24199[10:MRR:22954.1,24195.0] || equal(u,sk5) leq(u,sk5)* -> . % 34.78/34.98 24206[10:SpR:22566.1,24195.0] || equal(u,sk5) -> leq(sk5,u)*. % 34.78/34.98 24260[10:Res:24206.1,24199.1] || equal(sk5,sk5)* equal(sk5,sk5)* -> . % 34.78/34.98 24262[10:Obv:24260.1] || -> . % 34.78/34.98 24263[8:Spt:24262.0,12.0,22234.0] || memberP(sk7,sk8)* -> . % 34.78/34.98 24264[8:Spt:24262.0,12.1] || -> memberP(sk6,sk8)*. % 34.78/34.98 24270[8:Res:24264.0,14383.0] || -> memberP(sk1,sk8)*. % 34.78/34.98 24271[8:Res:22132.1,24263.0] || equal(skaf83(sk7),sk8)** -> . % 34.78/34.98 25002[6:Res:24168.1,14375.0] || equal(u,skaf83(sk7))* -> equal(u,sk9). % 34.78/34.98 25004[8:Res:24270.0,14375.0] || -> equal(sk9,sk8)**. % 34.78/34.98 25051[8:Rew:25004.0,25002.1] || equal(u,skaf83(sk7))* -> equal(u,sk8). % 34.78/34.98 25770[8:EqR:25051.0] || -> equal(skaf83(sk7),sk8)**. % 34.78/34.98 25772[8:MRR:25770.0,24271.0] || -> . % 34.78/34.98 25773[6:Spt:25772.0,335.0,1879.0] || totalorderedP(sk7)* -> . % 34.78/34.98 25774[6:Spt:25772.0,335.1] || -> equal(app(app(skaf66(sk7),cons(skaf64(sk7),skaf67(sk7))),cons(skaf65(sk7),skaf68(sk7))),sk7)**. % 34.78/34.98 25783[5:SSi:2149.0,32.0,9.0,1876.0] || equal(u,skaf83(sk7)) -> memberP(sk7,u)*. % 34.78/34.98 25937[7:Spt:12.0] || -> memberP(sk7,sk8)*. % 34.78/34.98 25938[7:Res:25937.0,7503.0] || -> memberP(sk1,sk8)*. % 34.78/34.98 26166[4:Res:14370.1,14375.0] || equal(u,sk5) -> equal(u,sk9)*. % 34.78/34.98 26167[7:Res:25938.0,14375.0] || -> equal(sk9,sk8)**. % 34.78/34.98 26171[7:Rew:26167.0,208.1] || neq(sk2,nil) -> memberP(sk2,sk8)*. % 34.78/34.98 26212[7:Rew:26167.0,26166.1] || equal(u,sk5) -> equal(u,sk8)*. % 34.78/34.98 26633[7:SpL:26212.1,15.1] || equal(u,sk5) leq(sk5,sk8)* leq(u,sk5)* -> . % 34.78/34.98 27632[8:Spt:26171.0] || neq(sk2,nil)* -> . % 34.78/34.98 27633[8:Res:529.1,27632.0] || -> equal(nil,sk2)**. % 34.78/34.98 27634[8:MRR:27633.0,1857.0] || -> . % 34.78/34.98 27635[8:Spt:27634.0,26171.0,27632.0] || -> neq(sk2,nil)*. % 34.78/34.98 27636[8:Spt:27634.0,26171.1] || -> memberP(sk2,sk8)*. % 34.78/34.98 27647[9:Spt:13.0] || leq(sk5,sk8)* -> . % 34.78/34.98 27650[9:SpL:26212.1,27647.0] || equal(u,sk5) leq(sk5,u)* -> . % 34.78/34.98 27827[5:Res:25783.1,7503.0] || equal(u,skaf83(sk7)) -> memberP(sk1,u)*. % 34.78/34.98 27854[9:Res:491.0,27650.1] || equal(sk5,sk5)* -> . % 34.78/34.98 27855[9:Obv:27854.0] || -> . % 34.78/34.98 27856[9:Spt:27855.0,13.0,27647.0] || -> leq(sk5,sk8)*. % 34.78/34.98 27857[9:Spt:27855.0,13.1] || -> memberP(sk6,sk8)*. % 34.78/34.98 27860[9:MRR:26633.1,27856.0] || equal(u,sk5) leq(u,sk5)* -> . % 34.78/34.98 27867[9:SpR:26212.1,27856.0] || equal(u,sk5) -> leq(sk5,u)*. % 34.78/34.98 27927[9:Res:27867.1,27860.1] || equal(sk5,sk5)* equal(sk5,sk5)* -> . % 34.78/34.98 27929[9:Obv:27927.1] || -> . % 34.78/34.98 27930[7:Spt:27929.0,12.0,25937.0] || memberP(sk7,sk8)* -> . % 34.78/34.98 27931[7:Spt:27929.0,12.1] || -> memberP(sk6,sk8)*. % 34.78/34.98 27937[7:Res:27931.0,14383.0] || -> memberP(sk1,sk8)*. % 34.78/34.98 27938[7:Res:25783.1,27930.0] || equal(skaf83(sk7),sk8)** -> . % 34.78/34.98 28662[5:Res:27827.1,14375.0] || equal(u,skaf83(sk7))* -> equal(u,sk9). % 34.78/34.98 28664[7:Res:27937.0,14375.0] || -> equal(sk9,sk8)**. % 34.78/34.98 28711[7:Rew:28664.0,28662.1] || equal(u,skaf83(sk7))* -> equal(u,sk8). % 34.78/34.98 29307[7:EqR:28711.0] || -> equal(skaf83(sk7),sk8)**. % 34.78/34.98 29309[7:MRR:29307.0,27938.0] || -> . % 34.78/34.98 29310[5:Spt:29309.0,336.0,1876.0] || strictorderedP(sk7)* -> . % 34.78/34.98 29311[5:Spt:29309.0,336.1] || -> equal(app(app(skaf71(sk7),cons(skaf69(sk7),skaf72(sk7))),cons(skaf70(sk7),skaf73(sk7))),sk7)**. % 34.78/34.98 29321[3:SSi:2149.0,32.0,9.0] || equal(u,skaf83(sk7)) -> memberP(sk7,u)*. % 34.78/34.98 29343[1:SSi:7712.2,7712.1,7712.0,9.0,501.0,2047.0,500.0,499.0,498.0,497.0,496.0,495.0,625.1,20.0,21.0,22.0,23.0,24.0,25.0,26.0,27.0,8.0] || -> equal(app(sk6,cons(sk5,sk7)),sk1)**. % 34.78/34.98 29477[6:Spt:12.0] || -> memberP(sk7,sk8)*. % 34.78/34.98 29478[6:Res:29477.0,7503.0] || -> memberP(sk1,sk8)*. % 34.78/34.98 29814[4:Res:14370.1,14375.0] || equal(u,sk5) -> equal(u,sk9)*. % 34.78/34.98 29815[6:Res:29478.0,14375.0] || -> equal(sk9,sk8)**. % 34.78/34.98 29818[6:Rew:29815.0,208.1] || neq(sk2,nil) -> memberP(sk2,sk8)*. % 34.78/34.98 29860[6:Rew:29815.0,29814.1] || equal(u,sk5) -> equal(u,sk8)*. % 34.78/34.98 30258[6:SpL:29860.1,15.1] || equal(u,sk5) leq(sk5,sk8)* leq(u,sk5)* -> . % 34.78/34.98 30338[1:SpL:29343.0,138.2] ssList(sk6) ssList(cons(sk5,sk7)) || equal(nil,sk1) -> equal(cons(sk5,sk7),nil)**. % 34.78/34.98 31298[7:Spt:29818.0] || neq(sk2,nil)* -> . % 34.78/34.98 31299[7:Res:529.1,31298.0] || -> equal(nil,sk2)**. % 34.78/34.98 31300[7:MRR:31299.0,1857.0] || -> . % 34.78/34.98 31301[7:Spt:31300.0,29818.0,31298.0] || -> neq(sk2,nil)*. % 34.78/34.98 31302[7:Spt:31300.0,29818.1] || -> memberP(sk2,sk8)*. % 34.78/34.98 31313[8:Spt:13.0] || leq(sk5,sk8)* -> . % 34.78/34.98 31316[8:SpL:29860.1,31313.0] || equal(u,sk5) leq(sk5,u)* -> . % 34.78/34.98 31486[3:Res:29321.1,7503.0] || equal(u,skaf83(sk7)) -> memberP(sk1,u)*. % 34.78/34.98 31508[8:Res:491.0,31316.1] || equal(sk5,sk5)* -> . % 34.78/34.98 31509[8:Obv:31508.0] || -> . % 34.78/34.98 31510[8:Spt:31509.0,13.0,31313.0] || -> leq(sk5,sk8)*. % 34.78/34.98 31511[8:Spt:31509.0,13.1] || -> memberP(sk6,sk8)*. % 34.78/34.98 31514[8:MRR:30258.1,31510.0] || equal(u,sk5) leq(u,sk5)* -> . % 46.34/46.53 31521[8:SpR:29860.1,31510.0] || equal(u,sk5) -> leq(sk5,u)*. % 46.34/46.53 31577[8:Res:31521.1,31514.1] || equal(sk5,sk5)* equal(sk5,sk5)* -> . % 46.34/46.53 31579[8:Obv:31577.1] || -> . % 46.34/46.53 31580[6:Spt:31579.0,12.0,29477.0] || memberP(sk7,sk8)* -> . % 46.34/46.53 31581[6:Spt:31579.0,12.1] || -> memberP(sk6,sk8)*. % 46.34/46.53 31617[6:Res:31581.0,14383.0] || -> memberP(sk1,sk8)*. % 46.34/46.53 31627[6:Res:29321.1,31580.0] || equal(skaf83(sk7),sk8)** -> . % 46.34/46.53 32292[4:Res:31486.1,14375.0] || equal(u,skaf83(sk7))* -> equal(u,sk9). % 46.34/46.53 32294[6:Res:31617.0,14375.0] || -> equal(sk9,sk8)**. % 46.34/46.53 32341[6:Rew:32294.0,32292.1] || equal(u,skaf83(sk7))* -> equal(u,sk8). % 46.34/46.53 33010[6:EqR:32341.0] || -> equal(skaf83(sk7),sk8)**. % 46.34/46.53 33012[6:MRR:33010.0,31627.0] || -> . % 46.34/46.53 33013[2:Spt:33012.0,442.1] || -> equal(nil,sk7)**. % 46.34/46.53 33034[2:Rew:33013.0,494.0] || memberP(sk7,u)* -> . % 46.34/46.53 33293[2:Rew:33013.0,1924.0] || -> equal(sk7,sk2) cyclefreeP(sk1)*. % 46.34/46.53 33301[2:MRR:12.0,33034.0] || -> memberP(sk6,sk8)*. % 46.34/46.53 33323[2:MRR:14.1,33034.0] || leq(sk8,sk5)* -> . % 46.34/46.53 33324[2:Rew:33013.0,208.0] || neq(sk2,sk7) -> memberP(sk2,sk9)*. % 46.34/46.53 33327[2:Rew:33013.0,209.1,33013.0,209.0] || equal(sk7,sk2)** -> equal(sk7,sk1). % 46.34/46.53 33361[2:Rew:33013.0,377.1] singletonP(sk7) || -> equal(cons(skaf44(sk7),sk7),sk7)**. % 46.34/46.53 33362[2:MRR:33361.1,503.0] singletonP(sk7) || -> . % 46.34/46.53 33363[2:Rew:33013.0,1976.1] || equal(sk7,sk1) -> equal(sk7,sk2) singletonP(sk7)*. % 46.34/46.53 33364[2:MRR:33363.2,33362.0] || equal(sk7,sk1)** -> equal(sk7,sk2). % 46.34/46.53 33387[2:Rew:33013.0,2611.0] || neq(sk2,sk7) memberP(sk1,u)* -> equal(u,sk9). % 46.34/46.53 33483[2:Rew:33364.1,30338.3,33013.0,30338.3,33013.0,30338.2] ssList(sk6) ssList(cons(sk5,sk7)) || equal(sk7,sk1) -> equal(cons(sk5,sk2),sk2)**. % 46.34/46.53 33484[2:SSi:33483.1,33483.0,625.0,9.0,8.1] || equal(sk7,sk1) -> equal(cons(sk5,sk2),sk2)**. % 46.34/46.53 33610[2:Res:33301.0,14383.0] || -> memberP(sk1,sk8)*. % 46.34/46.53 33616[3:Spt:33293.0] || -> equal(sk7,sk2)**. % 46.34/46.53 33633[3:Rew:33616.0,503.0] || equal(cons(u,sk2),sk2)** -> . % 46.34/46.53 33884[3:Rew:33616.0,33327.0] || equal(sk2,sk2) -> equal(sk7,sk1)**. % 46.34/46.53 33901[3:Rew:33616.0,33484.0] || equal(sk2,sk1) -> equal(cons(sk5,sk2),sk2)**. % 46.34/46.53 33965[3:Obv:33884.0] || -> equal(sk7,sk1)**. % 46.34/46.53 33966[3:Rew:33616.0,33965.0] || -> equal(sk2,sk1)**. % 46.34/46.53 34009[3:Rew:33966.0,33633.0] || equal(cons(u,sk1),sk1)** -> . % 46.34/46.53 34039[3:Rew:33966.0,33901.1,33966.0,33901.0] || equal(sk1,sk1) -> equal(cons(sk5,sk1),sk1)**. % 46.34/46.53 34040[3:Obv:34039.0] || -> equal(cons(sk5,sk1),sk1)**. % 46.34/46.53 34041[3:MRR:34040.0,34009.0] || -> . % 46.34/46.53 34455[3:Spt:34041.0,33293.0,33616.0] || equal(sk7,sk2)** -> . % 46.34/46.53 34456[3:Spt:34041.0,33293.1] || -> cyclefreeP(sk1)*. % 46.34/46.53 34593[4:Spt:33324.0] || neq(sk2,sk7)* -> . % 46.34/46.53 34594[4:Res:529.1,34593.0] || -> equal(sk7,sk2)**. % 46.34/46.53 34595[4:MRR:34594.0,34455.0] || -> . % 46.34/46.53 34596[4:Spt:34595.0,33324.0,34593.0] || -> neq(sk2,sk7)*. % 46.34/46.53 34597[4:Spt:34595.0,33324.1] || -> memberP(sk2,sk9)*. % 46.34/46.53 34600[4:MRR:33387.0,34596.0] || memberP(sk1,u)* -> equal(u,sk9). % 46.34/46.53 35403[4:Res:14370.1,34600.0] || equal(u,sk5) -> equal(u,sk9)*. % 46.34/46.53 35404[4:Res:33610.0,34600.0] || -> equal(sk9,sk8)**. % 46.34/46.53 35434[4:Rew:35404.0,35403.1] || equal(u,sk5) -> equal(u,sk8)*. % 46.34/46.53 35774[4:SpL:35434.1,33323.0] || equal(u,sk5) leq(u,sk5)* -> . % 46.34/46.53 36049[4:Res:491.0,35774.1] || equal(sk5,sk5)* -> . % 46.34/46.53 36050[4:Obv:36049.0] || -> . % 46.34/46.53 36051[1:Spt:36050.0,91.0,91.2] ssList(u) || -> duplicatefreeP(u)*. % 46.34/46.53 36090[1:MRR:198.1,36051.1] ssList(u) ssItem(v) ssList(w) ssList(x) ssList(y) || equal(app(app(w,cons(v,x)),cons(v,y)),u)* -> . % 46.34/46.53 48545[0:SpR:176.3,104.2] ssList(u) ssList(v) ssItem(w) ssList(cons(w,v)) ssList(u) || -> ssList(cons(w,app(v,u)))*. % 46.34/46.53 48579[0:Obv:48545.0] ssList(u) ssItem(v) ssList(cons(v,u)) ssList(w) || -> ssList(cons(v,app(u,w)))*. % 46.34/46.53 48580[0:SSi:48579.2,105.2] ssList(u) ssItem(v) ssList(w) || -> ssList(cons(v,app(u,w)))*. % 46.34/46.53 51055[1:EqR:36090.5] ssList(app(app(u,cons(v,w)),cons(v,x))) ssItem(v) ssList(u) ssList(w) ssList(x) || -> . % 46.34/46.53 51080[1:SSi:51055.0,104.2,104.2,105.2,105.2] ssItem(u) ssList(v) ssList(w) ssList(x) || -> . % 46.34/46.53 51081[1:MRR:48580.3,51080.1] ssList(u) ssItem(v) ssList(w) || -> . % 46.34/46.53 51084[1:Con:51081.2] ssList(u) ssItem(v) || -> . % 46.34/46.53 51122[1:MRR:454.1,51084.0] ssItem(u) || -> . % 46.34/46.53 51123[1:UnC:51122.0,31.0] || -> . % 46.34/46.53 % SZS output end Refutation % 46.34/46.53 Formulae used in the proof : co1_1 co1_2 co1_5 co1_6 co1_8 co1_9 co1_10 co1_12 co1_13 co1_14 co1_15 co1_16 co1_18 co1_19 clause1 clause2 clause3 clause4 clause5 clause6 clause7 clause8 clause12 clause13 clause54 clause62 clause63 clause64 clause65 clause66 clause67 clause68 clause69 clause70 clause71 clause72 clause74 clause85 clause86 clause87 clause96 clause97 clause98 clause99 clause101 clause102 clause109 clause113 clause116 clause119 clause120 clause123 clause124 clause125 clause129 clause134 clause135 clause138 clause140 clause141 clause144 clause149 clause157 clause159 clause161 clause163 clause164 clause165 clause166 clause170 clause175 clause177 clause179 % 46.34/46.53 %------------------------------------------------------------------------------