%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : SWC323+1 : TPTP v8.1.0. Released v2.4.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n011.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:18 EDT 2022 % Result : Theorem 2.43s 2.65s % Output : Refutation 2.54s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : SWC323+1 : TPTP v8.1.0. Released v2.4.0. % 0.03/0.13 % Command : run_spass %d %s % 0.12/0.34 % Computer : n011.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 600 % 0.12/0.34 % DateTime : Sun Jun 12 16:44:33 EDT 2022 % 0.12/0.34 % CPUTime : % 2.43/2.65 % 2.43/2.65 SPASS V 3.9 % 2.43/2.65 SPASS beiseite: Proof found. % 2.43/2.65 % SZS status Theorem % 2.43/2.65 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 2.43/2.65 SPASS derived 5618 clauses, backtracked 3518 clauses, performed 198 splits and kept 5887 clauses. % 2.43/2.65 SPASS allocated 102921 KBytes. % 2.43/2.65 SPASS spent 0:00:02.29 on the problem. % 2.43/2.65 0:00:00.04 for the input. % 2.43/2.65 0:00:00.07 for the FLOTTER CNF translation. % 2.43/2.65 0:00:00.05 for inferences. % 2.43/2.65 0:00:00.06 for the backtracking. % 2.43/2.65 0:00:01.87 for the reduction. % 2.43/2.65 % 2.43/2.65 % 2.43/2.65 Here is a proof with depth 3, length 984 : % 2.43/2.65 % SZS output start Refutation % 2.43/2.65 1[0:Inp] || -> ssList(skc9)*. % 2.43/2.65 2[0:Inp] || -> ssItem(skc8)*. % 2.43/2.65 3[0:Inp] || -> ssList(skc7)*. % 2.43/2.65 4[0:Inp] || -> ssList(skc6)*. % 2.43/2.65 7[0:Inp] || -> ssList(nil)*. % 2.43/2.65 8[0:Inp] || -> cyclefreeP(nil)*. % 2.43/2.65 9[0:Inp] || -> totalorderP(nil)*. % 2.43/2.65 10[0:Inp] || -> strictorderP(nil)*. % 2.43/2.65 11[0:Inp] || -> totalorderedP(nil)*. % 2.43/2.65 12[0:Inp] || -> strictorderedP(nil)*. % 2.43/2.65 13[0:Inp] || -> duplicatefreeP(nil)*. % 2.43/2.65 14[0:Inp] || -> equalelemsP(nil)*. % 2.43/2.65 68[0:Inp] || equal(skc7,nil)** -> equal(skc6,nil). % 2.43/2.65 70[0:Inp] ssItem(u) || -> cyclefreeP(cons(u,nil))*. % 2.43/2.65 71[0:Inp] ssItem(u) || -> totalorderP(cons(u,nil))*. % 2.43/2.65 72[0:Inp] ssItem(u) || -> strictorderP(cons(u,nil))*. % 2.43/2.65 73[0:Inp] ssItem(u) || -> totalorderedP(cons(u,nil))*. % 2.43/2.65 74[0:Inp] ssItem(u) || -> strictorderedP(cons(u,nil))*. % 2.43/2.65 75[0:Inp] ssItem(u) || -> duplicatefreeP(cons(u,nil))*. % 2.43/2.65 76[0:Inp] ssItem(u) || -> equalelemsP(cons(u,nil))*. % 2.43/2.65 78[0:Inp] ssList(u) || -> equal(app(nil,u),u)**. % 2.43/2.65 79[0:Inp] ssList(u) || -> equal(app(u,nil),u)**. % 2.43/2.65 82[0:Inp] ssList(u) || -> ssItem(hd(u))* equal(nil,u). % 2.43/2.65 84[0:Inp] ssList(u) || -> cyclefreeP(u) leq(skf51(u),skf50(u))*. % 2.43/2.65 85[0:Inp] ssList(u) || -> cyclefreeP(u) leq(skf50(u),skf51(u))*. % 2.43/2.65 86[0:Inp] ssList(u) || -> duplicatefreeP(u) equal(skf76(u),skf75(u))**. % 2.43/2.65 87[0:Inp] ssItem(u) ssList(v) || -> ssList(cons(u,v))*. % 2.43/2.65 95[0:Inp] || neq(skc7,nil) -> equal(app(cons(skc8,nil),skc9),skc7)**. % 2.43/2.65 96[0:Inp] || neq(skc7,nil) -> equal(app(skc9,cons(skc8,nil)),skc6)**. % 2.43/2.65 106[0:Inp] ssList(u) ssList(v) || -> neq(v,u)* equal(v,u). % 2.43/2.65 109[0:Inp] ssItem(u) ssList(v) || -> equal(hd(cons(u,v)),u)**. % 2.43/2.65 110[0:Inp] ssItem(u) ssList(v) || -> equal(tl(cons(u,v)),v)**. % 2.43/2.65 116[0:Inp] ssList(u) || -> equal(nil,u) equal(cons(hd(u),tl(u)),u)**. % 2.43/2.65 119[0:Inp] ssList(u) ssItem(v) || equal(cons(v,nil),u)*+ -> singletonP(u)*. % 2.43/2.65 122[0:Inp] ssList(u) ssItem(v) || equal(nil,u) -> totalorderedP(cons(v,u))*. % 2.43/2.65 123[0:Inp] ssList(u) ssItem(v) || equal(nil,u) -> strictorderedP(cons(v,u))*. % 2.43/2.65 126[0:Inp] ssItem(u) ssList(v) || -> equal(app(cons(u,nil),v),cons(u,v))**. % 2.43/2.65 129[0:Inp] ssList(u) ssItem(v) || totalorderedP(cons(v,u))* -> totalorderedP(u) equal(nil,u). % 2.43/2.65 130[0:Inp] ssList(u) ssItem(v) || strictorderedP(cons(v,u))* -> strictorderedP(u) equal(nil,u). % 2.43/2.65 141[0:Inp] ssList(u) ssList(v) || equal(app(u,v),skc6)**+ equal(app(v,u),skc7)** -> . % 2.43/2.65 172[0:Inp] ssList(u) || -> strictorderedP(u) equal(app(app(skf72(u),cons(skf70(u),skf73(u))),cons(skf71(u),skf74(u))),u)**. % 2.43/2.65 173[0:Inp] ssList(u) || -> totalorderedP(u) equal(app(app(skf67(u),cons(skf65(u),skf68(u))),cons(skf66(u),skf69(u))),u)**. % 2.43/2.65 174[0:Inp] ssList(u) || -> strictorderP(u) equal(app(app(skf62(u),cons(skf60(u),skf63(u))),cons(skf61(u),skf64(u))),u)**. % 2.43/2.65 175[0:Inp] ssList(u) || -> totalorderP(u) equal(app(app(skf57(u),cons(skf55(u),skf58(u))),cons(skf56(u),skf59(u))),u)**. % 2.43/2.65 186[0:Inp] ssList(u) ssList(v) || equal(tl(u),tl(v))* equal(hd(u),hd(v)) -> equal(u,v) equal(nil,v) equal(nil,u). % 2.43/2.65 218[0:Res:4.0,173.0] || -> totalorderedP(skc6) equal(app(app(skf67(skc6),cons(skf65(skc6),skf68(skc6))),cons(skf66(skc6),skf69(skc6))),skc6)**. % 2.43/2.65 219[0:Res:4.0,172.0] || -> strictorderedP(skc6) equal(app(app(skf72(skc6),cons(skf70(skc6),skf73(skc6))),cons(skf71(skc6),skf74(skc6))),skc6)**. % 2.43/2.65 263[0:Res:4.0,84.0] || -> cyclefreeP(skc6) leq(skf51(skc6),skf50(skc6))*. % 2.43/2.65 276[0:Res:4.0,78.0] || -> equal(app(nil,skc6),skc6)**. % 2.43/2.65 277[0:Res:4.0,79.0] || -> equal(app(skc6,nil),skc6)**. % 2.43/2.65 389[0:Res:3.0,175.0] || -> totalorderP(skc7) equal(app(app(skf57(skc7),cons(skf55(skc7),skf58(skc7))),cons(skf56(skc7),skf59(skc7))),skc7)**. % 2.43/2.65 390[0:Res:3.0,174.0] || -> strictorderP(skc7) equal(app(app(skf62(skc7),cons(skf60(skc7),skf63(skc7))),cons(skf61(skc7),skf64(skc7))),skc7)**. % 2.43/2.65 391[0:Res:3.0,173.0] || -> totalorderedP(skc7) equal(app(app(skf67(skc7),cons(skf65(skc7),skf68(skc7))),cons(skf66(skc7),skf69(skc7))),skc7)**. % 2.43/2.65 392[0:Res:3.0,172.0] || -> strictorderedP(skc7) equal(app(app(skf72(skc7),cons(skf70(skc7),skf73(skc7))),cons(skf71(skc7),skf74(skc7))),skc7)**. % 2.43/2.65 422[0:Res:3.0,116.0] || -> equal(skc7,nil) equal(cons(hd(skc7),tl(skc7)),skc7)**. % 2.43/2.65 424[0:Res:3.0,106.0] ssList(u) || -> neq(skc7,u)* equal(skc7,u). % 2.43/2.65 436[0:Res:3.0,84.0] || -> cyclefreeP(skc7) leq(skf51(skc7),skf50(skc7))*. % 2.43/2.65 437[0:Res:3.0,85.0] || -> cyclefreeP(skc7) leq(skf50(skc7),skf51(skc7))*. % 2.43/2.65 438[0:Res:3.0,86.0] || -> duplicatefreeP(skc7) equal(skf76(skc7),skf75(skc7))**. % 2.43/2.65 447[0:Res:3.0,82.0] || -> ssItem(hd(skc7))* equal(skc7,nil). % 2.43/2.65 449[0:Res:3.0,78.0] || -> equal(app(nil,skc7),skc7)**. % 2.43/2.65 457[0:Res:3.0,186.1] ssList(u) || equal(tl(skc7),tl(u))* equal(hd(skc7),hd(u)) -> equal(nil,u) equal(skc7,u) equal(skc7,nil). % 2.43/2.65 473[0:Res:3.0,141.1] ssList(u) || equal(app(u,skc7),skc7)** equal(app(skc7,u),skc6)** -> . % 2.43/2.65 554[1:Spt:457.5] || -> equal(skc7,nil)**. % 2.43/2.65 561[1:Rew:554.0,68.0] || equal(nil,nil) -> equal(skc6,nil)**. % 2.43/2.65 589[1:Rew:554.0,473.2] ssList(u) || equal(app(u,skc7),skc7)** equal(app(nil,u),skc6)** -> . % 2.43/2.65 713[1:Obv:561.0] || -> equal(skc6,nil)**. % 2.43/2.65 950[1:Rew:78.1,589.2,713.0,589.2,79.1,589.1,554.0,589.1] ssList(u) || equal(u,nil)* equal(u,nil)* -> . % 2.43/2.65 951[1:Obv:950.1] ssList(u) || equal(u,nil)* -> . % 2.43/2.65 1099[1:EmS:951.0,7.0] || equal(nil,nil)* -> . % 2.43/2.65 1100[1:Obv:1099.0] || -> . % 2.43/2.65 1101[1:Spt:1100.0,457.5,554.0] || equal(skc7,nil)** -> . % 2.43/2.65 1102[1:Spt:1100.0,457.0,457.1,457.2,457.3,457.4] ssList(u) || equal(tl(skc7),tl(u))* equal(hd(skc7),hd(u)) -> equal(nil,u) equal(skc7,u). % 2.43/2.65 1104[1:MRR:447.1,1101.0] || -> ssItem(hd(skc7))*. % 2.43/2.65 1108[1:MRR:422.0,1101.0] || -> equal(cons(hd(skc7),tl(skc7)),skc7)**. % 2.43/2.65 1908[2:Spt:391.0] || -> totalorderedP(skc7)*. % 2.43/2.65 1912[3:Spt:392.0] || -> strictorderedP(skc7)*. % 2.43/2.65 1915[4:Spt:218.0] || -> totalorderedP(skc6)*. % 2.43/2.65 1919[5:Spt:219.0] || -> strictorderedP(skc6)*. % 2.43/2.65 1922[6:Spt:437.0] || -> cyclefreeP(skc7)*. % 2.43/2.65 1924[7:Spt:263.0] || -> cyclefreeP(skc6)*. % 2.43/2.65 1926[8:Spt:389.0] || -> totalorderP(skc7)*. % 2.43/2.65 1927[9:Spt:390.0] || -> strictorderP(skc7)*. % 2.43/2.65 1940[10:Spt:438.0] || -> duplicatefreeP(skc7)*. % 2.43/2.65 2487[0:EqR:119.2] ssList(cons(u,nil)) ssItem(u) || -> singletonP(cons(u,nil))*. % 2.43/2.65 2490[0:SSi:2487.0,87.1,14.1,13.1,10.1,9.1,8.1,12.1,11.0,7.0,76.0,75.0,72.0,71.0,70.0,74.0,73.2] ssItem(u) || -> singletonP(cons(u,nil))*. % 2.43/2.65 2894[0:SpR:126.2,95.1] ssItem(skc8) ssList(skc9) || neq(skc7,nil) -> equal(cons(skc8,skc9),skc7)**. % 2.43/2.65 2905[0:SSi:2894.1,2894.0,1.0,2.0] || neq(skc7,nil) -> equal(cons(skc8,skc9),skc7)**. % 2.43/2.65 2913[0:SpR:2905.1,110.2] ssItem(skc8) ssList(skc9) || neq(skc7,nil)* -> equal(tl(skc7),skc9). % 2.43/2.65 2914[0:SpR:2905.1,109.2] ssItem(skc8) ssList(skc9) || neq(skc7,nil)* -> equal(hd(skc7),skc8). % 2.43/2.65 2920[0:SSi:2913.1,2913.0,1.0,2.0] || neq(skc7,nil)* -> equal(tl(skc7),skc9). % 2.43/2.65 2921[0:SSi:2914.1,2914.0,1.0,2.0] || neq(skc7,nil)* -> equal(hd(skc7),skc8). % 2.43/2.65 2923[0:Res:424.1,2920.0] ssList(nil) || -> equal(skc7,nil) equal(tl(skc7),skc9)**. % 2.43/2.65 2926[0:SSi:2923.0,14.0,13.0,10.0,9.0,8.0,12.0,11.0,7.0] || -> equal(skc7,nil) equal(tl(skc7),skc9)**. % 2.43/2.65 2927[1:MRR:2926.0,1101.0] || -> equal(tl(skc7),skc9)**. % 2.43/2.65 2929[1:Rew:2927.0,1108.0] || -> equal(cons(hd(skc7),skc9),skc7)**. % 2.43/2.65 2992[1:SpL:2929.0,130.2] ssList(skc9) ssItem(hd(skc7)) || strictorderedP(skc7) -> strictorderedP(skc9)* equal(skc9,nil). % 2.43/2.65 2993[1:SSi:2992.1,2992.0,1104.0,1.0] || strictorderedP(skc7) -> strictorderedP(skc9)* equal(skc9,nil). % 2.43/2.65 2994[3:MRR:2993.0,1912.0] || -> strictorderedP(skc9)* equal(skc9,nil). % 2.43/2.65 3720[0:SpL:276.0,141.2] ssList(nil) ssList(skc6) || equal(skc6,skc6) equal(app(skc6,nil),skc7)** -> . % 2.43/2.65 3729[0:Obv:3720.2] ssList(nil) ssList(skc6) || equal(app(skc6,nil),skc7)** -> . % 2.43/2.65 3730[0:Rew:277.0,3729.2] ssList(nil) ssList(skc6) || equal(skc7,skc6)** -> . % 2.43/2.65 3786[11:Spt:95.0] || neq(skc7,nil)* -> . % 2.43/2.65 3788[11:Res:106.2,3786.0] ssList(nil) ssList(skc7) || -> equal(skc7,nil)**. % 2.43/2.65 3790[11:SSi:3788.1,3788.0,1940.0,1927.0,1926.0,1922.0,3.0,1912.0,1908.0,14.0,13.0,10.0,9.0,8.0,12.0,11.0,7.0] || -> equal(skc7,nil)**. % 2.43/2.65 3791[11:MRR:3790.0,1101.0] || -> . % 2.43/2.65 3792[11:Spt:3791.0,95.0,3786.0] || -> neq(skc7,nil)*. % 2.43/2.65 3793[11:Spt:3791.0,95.1] || -> equal(app(cons(skc8,nil),skc9),skc7)**. % 2.43/2.65 3806[11:MRR:96.0,3792.0] || -> equal(app(skc9,cons(skc8,nil)),skc6)**. % 2.43/2.65 3834[11:SpL:3806.0,141.2] ssList(skc9) ssList(cons(skc8,nil)) || equal(skc6,skc6) equal(app(cons(skc8,nil),skc9),skc7)** -> . % 2.43/2.65 3839[11:Obv:3834.2] ssList(skc9) ssList(cons(skc8,nil)) || equal(app(cons(skc8,nil),skc9),skc7)** -> . % 2.43/2.65 3840[11:Rew:3793.0,3839.2] ssList(skc9) ssList(cons(skc8,nil)) || equal(skc7,skc7)* -> . % 2.43/2.65 3841[11:Obv:3840.2] ssList(skc9) ssList(cons(skc8,nil)) || -> . % 2.43/2.65 3842[11:SSi:3841.1,3841.0,87.0,2.0,14.1,13.0,10.1,9.0,8.1,12.0,11.1,7.0,76.1,2.0,75.1,2.0,72.1,2.0,71.1,2.0,70.0,2.0,74.0,2.0,73.0,2.0,2490.0,2.0,1.2] || -> . % 2.43/2.65 3843[10:Spt:3842.0,438.0,1940.0] || duplicatefreeP(skc7)* -> . % 2.43/2.65 3844[10:Spt:3842.0,438.1] || -> equal(skf76(skc7),skf75(skc7))**. % 2.43/2.65 3887[11:Spt:96.0] || neq(skc7,nil)* -> . % 2.43/2.65 3889[11:Res:106.2,3887.0] ssList(nil) ssList(skc7) || -> equal(skc7,nil)**. % 2.43/2.65 3891[11:SSi:3889.1,3889.0,1927.0,1926.0,1922.0,3.0,1912.0,1908.0,14.0,13.0,10.0,9.0,8.0,12.0,11.0,7.0] || -> equal(skc7,nil)**. % 2.43/2.65 3892[11:MRR:3891.0,1101.0] || -> . % 2.43/2.65 3893[11:Spt:3892.0,96.0,3887.0] || -> neq(skc7,nil)*. % 2.43/2.65 3894[11:Spt:3892.0,96.1] || -> equal(app(skc9,cons(skc8,nil)),skc6)**. % 2.43/2.65 3906[11:MRR:95.0,3893.0] || -> equal(app(cons(skc8,nil),skc9),skc7)**. % 2.43/2.65 3910[11:SpL:3894.0,141.2] ssList(skc9) ssList(cons(skc8,nil)) || equal(skc6,skc6) equal(app(cons(skc8,nil),skc9),skc7)** -> . % 2.43/2.65 3915[11:Obv:3910.2] ssList(skc9) ssList(cons(skc8,nil)) || equal(app(cons(skc8,nil),skc9),skc7)** -> . % 2.43/2.65 3916[11:Rew:3906.0,3915.2] ssList(skc9) ssList(cons(skc8,nil)) || equal(skc7,skc7)* -> . % 2.43/2.65 3917[11:Obv:3916.2] ssList(skc9) ssList(cons(skc8,nil)) || -> . % 2.43/2.65 3918[11:SSi:3917.1,3917.0,87.0,2.0,14.1,13.0,10.1,9.0,8.1,12.0,11.1,7.0,76.1,2.0,75.1,2.0,72.1,2.0,71.1,2.0,70.0,2.0,74.0,2.0,73.0,2.0,2490.0,2.0,1.2] || -> . % 2.43/2.65 3919[9:Spt:3918.0,390.0,1927.0] || strictorderP(skc7)* -> . % 2.43/2.65 3920[9:Spt:3918.0,390.1] || -> equal(app(app(skf62(skc7),cons(skf60(skc7),skf63(skc7))),cons(skf61(skc7),skf64(skc7))),skc7)**. % 2.43/2.65 3924[7:SSi:3730.1,3730.0,4.0,1915.0,1919.0,1924.0,14.0,13.0,10.0,9.0,8.0,12.0,11.0,7.0] || equal(skc7,skc6)** -> . % 2.43/2.65 3968[10:Spt:95.0] || neq(skc7,nil)* -> . % 2.43/2.65 3970[10:Res:106.2,3968.0] ssList(nil) ssList(skc7) || -> equal(skc7,nil)**. % 2.43/2.65 3972[10:SSi:3970.1,3970.0,1926.0,1922.0,3.0,1912.0,1908.0,14.0,13.0,10.0,9.0,8.0,12.0,11.0,7.0] || -> equal(skc7,nil)**. % 2.43/2.65 3973[10:MRR:3972.0,1101.0] || -> . % 2.43/2.65 3974[10:Spt:3973.0,95.0,3968.0] || -> neq(skc7,nil)*. % 2.43/2.65 3975[10:Spt:3973.0,95.1] || -> equal(app(cons(skc8,nil),skc9),skc7)**. % 2.43/2.65 3988[10:MRR:96.0,3974.0] || -> equal(app(skc9,cons(skc8,nil)),skc6)**. % 2.43/2.65 4019[10:SpL:3988.0,141.2] ssList(skc9) ssList(cons(skc8,nil)) || equal(skc6,skc6) equal(app(cons(skc8,nil),skc9),skc7)** -> . % 2.43/2.65 4024[10:Obv:4019.2] ssList(skc9) ssList(cons(skc8,nil)) || equal(app(cons(skc8,nil),skc9),skc7)** -> . % 2.43/2.65 4025[10:Rew:3975.0,4024.2] ssList(skc9) ssList(cons(skc8,nil)) || equal(skc7,skc7)* -> . % 2.43/2.65 4026[10:Obv:4025.2] ssList(skc9) ssList(cons(skc8,nil)) || -> . % 2.43/2.65 4027[10:SSi:4026.1,4026.0,87.0,2.0,14.1,13.0,10.1,9.0,8.1,12.0,11.1,7.0,76.1,2.0,75.1,2.0,72.1,2.0,71.1,2.0,70.0,2.0,74.0,2.0,73.0,2.0,2490.0,2.0,1.2] || -> . % 2.43/2.65 4028[8:Spt:4027.0,389.0,1926.0] || totalorderP(skc7)* -> . % 2.43/2.65 4029[8:Spt:4027.0,389.1] || -> equal(app(app(skf57(skc7),cons(skf55(skc7),skf58(skc7))),cons(skf56(skc7),skf59(skc7))),skc7)**. % 2.43/2.65 4062[9:Spt:390.0] || -> strictorderP(skc7)*. % 2.43/2.65 4067[10:Spt:96.0] || neq(skc7,nil)* -> . % 2.43/2.65 4069[10:Res:106.2,4067.0] ssList(nil) ssList(skc7) || -> equal(skc7,nil)**. % 2.43/2.65 4071[10:SSi:4069.1,4069.0,1922.0,3.0,1912.0,1908.0,4062.0,14.0,13.0,10.0,9.0,8.0,12.0,11.0,7.0] || -> equal(skc7,nil)**. % 2.43/2.65 4072[10:MRR:4071.0,1101.0] || -> . % 2.43/2.65 4073[10:Spt:4072.0,96.0,4067.0] || -> neq(skc7,nil)*. % 2.43/2.65 4074[10:Spt:4072.0,96.1] || -> equal(app(skc9,cons(skc8,nil)),skc6)**. % 2.43/2.65 4087[10:MRR:95.0,4073.0] || -> equal(app(cons(skc8,nil),skc9),skc7)**. % 2.43/2.65 4091[10:SpL:4074.0,141.2] ssList(skc9) ssList(cons(skc8,nil)) || equal(skc6,skc6) equal(app(cons(skc8,nil),skc9),skc7)** -> . % 2.43/2.65 4096[10:Obv:4091.2] ssList(skc9) ssList(cons(skc8,nil)) || equal(app(cons(skc8,nil),skc9),skc7)** -> . % 2.43/2.65 4097[10:Rew:4087.0,4096.2] ssList(skc9) ssList(cons(skc8,nil)) || equal(skc7,skc7)* -> . % 2.43/2.65 4098[10:Obv:4097.2] ssList(skc9) ssList(cons(skc8,nil)) || -> . % 2.43/2.65 4099[10:SSi:4098.1,4098.0,87.0,2.0,14.1,13.0,10.1,9.0,8.1,12.0,11.1,7.0,76.1,2.0,75.1,2.0,72.1,2.0,71.1,2.0,70.0,2.0,74.0,2.0,73.0,2.0,2490.0,2.0,1.2] || -> . % 2.43/2.65 4100[9:Spt:4099.0,390.0,4062.0] || strictorderP(skc7)* -> . % 2.43/2.65 4101[9:Spt:4099.0,390.1] || -> equal(app(app(skf62(skc7),cons(skf60(skc7),skf63(skc7))),cons(skf61(skc7),skf64(skc7))),skc7)**. % 2.43/2.65 4119[10:Spt:2994.1] || -> equal(skc9,nil)**. % 2.43/2.65 4134[10:Rew:4119.0,2905.1] || neq(skc7,nil) -> equal(cons(skc8,nil),skc7)**. % 2.43/2.65 4136[10:Rew:4119.0,96.1] || neq(skc7,nil) -> equal(app(nil,cons(skc8,nil)),skc6)**. % 2.43/2.65 4144[10:Rew:4134.1,4136.1] || neq(skc7,nil) -> equal(app(nil,skc7),skc6)**. % 2.43/2.65 4145[10:Rew:449.0,4144.1] || neq(skc7,nil)* -> equal(skc7,skc6). % 2.43/2.65 4146[10:MRR:4145.1,3924.0] || neq(skc7,nil)* -> . % 2.43/2.65 4154[10:Res:106.2,4146.0] ssList(nil) ssList(skc7) || -> equal(skc7,nil)**. % 2.43/2.65 4156[10:SSi:4154.1,4154.0,1922.0,3.0,1912.0,1908.0,14.0,13.0,10.0,9.0,8.0,12.0,11.0,7.0] || -> equal(skc7,nil)**. % 2.43/2.65 4157[10:MRR:4156.0,1101.0] || -> . % 2.43/2.65 4158[10:Spt:4157.0,2994.1,4119.0] || equal(skc9,nil)** -> . % 2.43/2.65 4159[10:Spt:4157.0,2994.0] || -> strictorderedP(skc9)*. % 2.43/2.65 4176[11:Spt:96.0] || neq(skc7,nil)* -> . % 2.43/2.65 4178[11:Res:106.2,4176.0] ssList(nil) ssList(skc7) || -> equal(skc7,nil)**. % 2.43/2.65 4180[11:SSi:4178.1,4178.0,1922.0,3.0,1912.0,1908.0,14.0,13.0,10.0,9.0,8.0,12.0,11.0,7.0] || -> equal(skc7,nil)**. % 2.43/2.65 4181[11:MRR:4180.0,1101.0] || -> . % 2.43/2.65 4182[11:Spt:4181.0,96.0,4176.0] || -> neq(skc7,nil)*. % 2.43/2.65 4183[11:Spt:4181.0,96.1] || -> equal(app(skc9,cons(skc8,nil)),skc6)**. % 2.43/2.65 4197[11:MRR:95.0,4182.0] || -> equal(app(cons(skc8,nil),skc9),skc7)**. % 2.43/2.65 4201[11:SpL:4183.0,141.2] ssList(skc9) ssList(cons(skc8,nil)) || equal(skc6,skc6) equal(app(cons(skc8,nil),skc9),skc7)** -> . % 2.43/2.65 4207[11:Obv:4201.2] ssList(skc9) ssList(cons(skc8,nil)) || equal(app(cons(skc8,nil),skc9),skc7)** -> . % 2.43/2.65 4208[11:Rew:4197.0,4207.2] ssList(skc9) ssList(cons(skc8,nil)) || equal(skc7,skc7)* -> . % 2.43/2.65 4209[11:Obv:4208.2] ssList(skc9) ssList(cons(skc8,nil)) || -> . % 2.43/2.65 4210[11:SSi:4209.1,4209.0,87.0,2.0,14.0,13.1,10.0,9.1,8.0,12.1,11.0,7.1,76.0,2.1,75.0,2.1,72.0,2.1,71.0,2.1,70.0,2.0,74.0,2.0,73.0,2.0,2490.0,2.0,4159.0,1.2] || -> . % 2.43/2.65 4211[7:Spt:4210.0,263.0,1924.0] || cyclefreeP(skc6)* -> . % 2.43/2.65 4212[7:Spt:4210.0,263.1] || -> leq(skf51(skc6),skf50(skc6))*. % 2.43/2.65 4214[5:SSi:3730.1,3730.0,4.0,1915.0,1919.0,14.0,13.0,10.0,9.0,8.0,12.0,11.0,7.0] || equal(skc7,skc6)** -> . % 2.43/2.65 4235[8:Spt:390.0] || -> strictorderP(skc7)*. % 2.43/2.65 4243[9:Spt:389.0] || -> totalorderP(skc7)*. % 2.43/2.65 4244[10:Spt:95.0] || neq(skc7,nil)* -> . % 2.43/2.65 4246[10:Res:106.2,4244.0] ssList(nil) ssList(skc7) || -> equal(skc7,nil)**. % 2.43/2.65 4248[10:SSi:4246.1,4246.0,1922.0,3.0,1912.0,1908.0,4235.0,4243.0,14.0,13.0,10.0,9.0,8.0,12.0,11.0,7.0] || -> equal(skc7,nil)**. % 2.43/2.65 4249[10:MRR:4248.0,1101.0] || -> . % 2.43/2.65 4250[10:Spt:4249.0,95.0,4244.0] || -> neq(skc7,nil)*. % 2.43/2.65 4251[10:Spt:4249.0,95.1] || -> equal(app(cons(skc8,nil),skc9),skc7)**. % 2.43/2.65 4252[10:MRR:2921.0,4250.0] || -> equal(hd(skc7),skc8)**. % 2.43/2.65 4254[10:Rew:4252.0,2929.0] || -> equal(cons(skc8,skc9),skc7)**. % 2.43/2.65 4263[10:MRR:96.0,4250.0] || -> equal(app(skc9,cons(skc8,nil)),skc6)**. % 2.43/2.65 4282[11:Spt:2994.1] || -> equal(skc9,nil)**. % 2.43/2.65 4297[11:Rew:4282.0,4254.0] || -> equal(cons(skc8,nil),skc7)**. % 2.43/2.65 4298[11:Rew:4282.0,4263.0] || -> equal(app(nil,cons(skc8,nil)),skc6)**. % 2.43/2.65 4304[11:Rew:4297.0,4298.0] || -> equal(app(nil,skc7),skc6)**. % 2.43/2.65 4305[11:Rew:449.0,4304.0] || -> equal(skc7,skc6)**. % 2.43/2.65 4306[11:MRR:4305.0,4214.0] || -> . % 2.43/2.65 4338[11:Spt:4306.0,2994.1,4282.0] || equal(skc9,nil)** -> . % 2.43/2.65 4339[11:Spt:4306.0,2994.0] || -> strictorderedP(skc9)*. % 2.43/2.65 4360[10:SpL:4263.0,141.2] ssList(skc9) ssList(cons(skc8,nil)) || equal(skc6,skc6) equal(app(cons(skc8,nil),skc9),skc7)** -> . % 2.43/2.65 4366[10:Obv:4360.2] ssList(skc9) ssList(cons(skc8,nil)) || equal(app(cons(skc8,nil),skc9),skc7)** -> . % 2.43/2.65 4367[10:Rew:4251.0,4366.2] ssList(skc9) ssList(cons(skc8,nil)) || equal(skc7,skc7)* -> . % 2.43/2.65 4368[10:Obv:4367.2] ssList(skc9) ssList(cons(skc8,nil)) || -> . % 2.43/2.65 4369[11:SSi:4368.1,4368.0,87.0,2.0,14.0,13.1,10.0,9.1,8.0,12.1,11.0,7.1,76.0,2.1,75.0,2.1,72.0,2.1,71.0,2.1,70.0,2.0,74.0,2.0,73.0,2.0,2490.0,2.0,4339.0,1.2] || -> . % 2.43/2.65 4370[9:Spt:4369.0,389.0,4243.0] || totalorderP(skc7)* -> . % 2.43/2.65 4371[9:Spt:4369.0,389.1] || -> equal(app(app(skf57(skc7),cons(skf55(skc7),skf58(skc7))),cons(skf56(skc7),skf59(skc7))),skc7)**. % 2.43/2.65 4389[10:Spt:96.0] || neq(skc7,nil)* -> . % 2.43/2.65 4391[10:Res:106.2,4389.0] ssList(nil) ssList(skc7) || -> equal(skc7,nil)**. % 2.43/2.65 4393[10:SSi:4391.1,4391.0,1922.0,3.0,1912.0,1908.0,4235.0,14.0,13.0,10.0,9.0,8.0,12.0,11.0,7.0] || -> equal(skc7,nil)**. % 2.43/2.65 4394[10:MRR:4393.0,1101.0] || -> . % 2.43/2.65 4395[10:Spt:4394.0,96.0,4389.0] || -> neq(skc7,nil)*. % 2.43/2.65 4396[10:Spt:4394.0,96.1] || -> equal(app(skc9,cons(skc8,nil)),skc6)**. % 2.43/2.65 4409[10:MRR:95.0,4395.0] || -> equal(app(cons(skc8,nil),skc9),skc7)**. % 2.43/2.65 4413[10:SpL:4396.0,141.2] ssList(skc9) ssList(cons(skc8,nil)) || equal(skc6,skc6) equal(app(cons(skc8,nil),skc9),skc7)** -> . % 2.43/2.65 4418[10:Obv:4413.2] ssList(skc9) ssList(cons(skc8,nil)) || equal(app(cons(skc8,nil),skc9),skc7)** -> . % 2.43/2.65 4419[10:Rew:4409.0,4418.2] ssList(skc9) ssList(cons(skc8,nil)) || equal(skc7,skc7)* -> . % 2.43/2.65 4420[10:Obv:4419.2] ssList(skc9) ssList(cons(skc8,nil)) || -> . % 2.43/2.65 4421[10:SSi:4420.1,4420.0,87.0,2.0,14.1,13.0,10.1,9.0,8.1,12.0,11.1,7.0,76.1,2.0,75.1,2.0,72.1,2.0,71.1,2.0,70.0,2.0,74.0,2.0,73.0,2.0,2490.0,2.0,1.2] || -> . % 2.43/2.65 4422[8:Spt:4421.0,390.0,4235.0] || strictorderP(skc7)* -> . % 2.43/2.65 4423[8:Spt:4421.0,390.1] || -> equal(app(app(skf62(skc7),cons(skf60(skc7),skf63(skc7))),cons(skf61(skc7),skf64(skc7))),skc7)**. % 2.43/2.65 4436[9:Spt:389.0] || -> totalorderP(skc7)*. % 2.43/2.65 4445[10:Spt:95.0] || neq(skc7,nil)* -> . % 2.43/2.65 4447[10:Res:106.2,4445.0] ssList(nil) ssList(skc7) || -> equal(skc7,nil)**. % 2.43/2.65 4449[10:SSi:4447.1,4447.0,1922.0,3.0,1912.0,1908.0,4436.0,14.0,13.0,10.0,9.0,8.0,12.0,11.0,7.0] || -> equal(skc7,nil)**. % 2.43/2.65 4450[10:MRR:4449.0,1101.0] || -> . % 2.43/2.65 4451[10:Spt:4450.0,95.0,4445.0] || -> neq(skc7,nil)*. % 2.43/2.65 4452[10:Spt:4450.0,95.1] || -> equal(app(cons(skc8,nil),skc9),skc7)**. % 2.43/2.65 4465[10:MRR:96.0,4451.0] || -> equal(app(skc9,cons(skc8,nil)),skc6)**. % 2.43/2.65 4490[10:SpL:4465.0,141.2] ssList(skc9) ssList(cons(skc8,nil)) || equal(skc6,skc6) equal(app(cons(skc8,nil),skc9),skc7)** -> . % 2.43/2.65 4495[10:Obv:4490.2] ssList(skc9) ssList(cons(skc8,nil)) || equal(app(cons(skc8,nil),skc9),skc7)** -> . % 2.43/2.65 4496[10:Rew:4452.0,4495.2] ssList(skc9) ssList(cons(skc8,nil)) || equal(skc7,skc7)* -> . % 2.43/2.65 4497[10:Obv:4496.2] ssList(skc9) ssList(cons(skc8,nil)) || -> . % 2.43/2.65 4498[10:SSi:4497.1,4497.0,87.0,2.0,14.1,13.0,10.1,9.0,8.1,12.0,11.1,7.0,76.1,2.0,75.1,2.0,72.1,2.0,71.1,2.0,70.0,2.0,74.0,2.0,73.0,2.0,2490.0,2.0,1.2] || -> . % 2.43/2.65 4499[9:Spt:4498.0,389.0,4436.0] || totalorderP(skc7)* -> . % 2.43/2.65 4500[9:Spt:4498.0,389.1] || -> equal(app(app(skf57(skc7),cons(skf55(skc7),skf58(skc7))),cons(skf56(skc7),skf59(skc7))),skc7)**. % 2.43/2.65 4517[10:Spt:2994.1] || -> equal(skc9,nil)**. % 2.43/2.65 4532[10:Rew:4517.0,2905.1] || neq(skc7,nil) -> equal(cons(skc8,nil),skc7)**. % 2.43/2.65 4533[10:Rew:4517.0,96.1] || neq(skc7,nil) -> equal(app(nil,cons(skc8,nil)),skc6)**. % 2.43/2.65 4541[10:Rew:4532.1,4533.1] || neq(skc7,nil) -> equal(app(nil,skc7),skc6)**. % 2.43/2.65 4542[10:Rew:449.0,4541.1] || neq(skc7,nil)* -> equal(skc7,skc6). % 2.43/2.65 4543[10:MRR:4542.1,4214.0] || neq(skc7,nil)* -> . % 2.43/2.65 4551[10:Res:106.2,4543.0] ssList(nil) ssList(skc7) || -> equal(skc7,nil)**. % 2.43/2.65 4553[10:SSi:4551.1,4551.0,1922.0,3.0,1912.0,1908.0,14.0,13.0,10.0,9.0,8.0,12.0,11.0,7.0] || -> equal(skc7,nil)**. % 2.43/2.65 4554[10:MRR:4553.0,1101.0] || -> . % 2.43/2.65 4555[10:Spt:4554.0,2994.1,4517.0] || equal(skc9,nil)** -> . % 2.43/2.65 4556[10:Spt:4554.0,2994.0] || -> strictorderedP(skc9)*. % 2.43/2.65 4573[11:Spt:95.0] || neq(skc7,nil)* -> . % 2.43/2.65 4575[11:Res:106.2,4573.0] ssList(nil) ssList(skc7) || -> equal(skc7,nil)**. % 2.43/2.65 4577[11:SSi:4575.1,4575.0,1922.0,3.0,1912.0,1908.0,14.0,13.0,10.0,9.0,8.0,12.0,11.0,7.0] || -> equal(skc7,nil)**. % 2.43/2.65 4578[11:MRR:4577.0,1101.0] || -> . % 2.43/2.65 4579[11:Spt:4578.0,95.0,4573.0] || -> neq(skc7,nil)*. % 2.43/2.65 4580[11:Spt:4578.0,95.1] || -> equal(app(cons(skc8,nil),skc9),skc7)**. % 2.43/2.65 4581[11:MRR:2921.0,4579.0] || -> equal(hd(skc7),skc8)**. % 2.43/2.65 4590[11:Rew:4581.0,2929.0] || -> equal(cons(skc8,skc9),skc7)**. % 2.43/2.65 4594[11:MRR:96.0,4579.0] || -> equal(app(skc9,cons(skc8,nil)),skc6)**. % 2.43/2.65 4621[11:SpL:4590.0,129.2] ssList(skc9) ssItem(skc8) || totalorderedP(skc7) -> totalorderedP(skc9)* equal(skc9,nil). % 2.43/2.65 4622[11:SSi:4621.1,4621.0,2.0,4556.0,1.0] || totalorderedP(skc7) -> totalorderedP(skc9)* equal(skc9,nil). % 2.43/2.65 4623[11:MRR:4622.0,4622.2,1908.0,4555.0] || -> totalorderedP(skc9)*. % 2.43/2.65 4627[11:SpL:4594.0,141.2] ssList(skc9) ssList(cons(skc8,nil)) || equal(skc6,skc6) equal(app(cons(skc8,nil),skc9),skc7)** -> . % 2.43/2.65 4633[11:Obv:4627.2] ssList(skc9) ssList(cons(skc8,nil)) || equal(app(cons(skc8,nil),skc9),skc7)** -> . % 2.43/2.65 4634[11:Rew:4580.0,4633.2] ssList(skc9) ssList(cons(skc8,nil)) || equal(skc7,skc7)* -> . % 2.43/2.65 4635[11:Obv:4634.2] ssList(skc9) ssList(cons(skc8,nil)) || -> . % 2.43/2.65 4636[11:SSi:4635.1,4635.0,87.0,2.0,14.0,13.0,10.1,9.0,8.1,12.0,11.1,7.0,76.1,2.0,75.1,2.0,72.1,2.0,71.1,2.0,70.1,2.0,74.0,2.0,73.0,2.0,2490.0,2.0,4556.0,1.0,4623.2] || -> . % 2.43/2.65 4637[6:Spt:4636.0,437.0,1922.0] || cyclefreeP(skc7)* -> . % 2.43/2.65 4638[6:Spt:4636.0,437.1] || -> leq(skf50(skc7),skf51(skc7))*. % 2.43/2.65 4676[7:Spt:389.0] || -> totalorderP(skc7)*. % 2.43/2.65 4680[8:Spt:390.0] || -> strictorderP(skc7)*. % 2.43/2.65 4681[9:Spt:96.0] || neq(skc7,nil)* -> . % 2.43/2.65 4683[9:Res:106.2,4681.0] ssList(nil) ssList(skc7) || -> equal(skc7,nil)**. % 2.43/2.65 4685[9:SSi:4683.1,4683.0,3.0,1912.0,1908.0,4676.0,4680.0,14.0,13.0,10.0,9.0,8.0,12.0,11.0,7.0] || -> equal(skc7,nil)**. % 2.43/2.65 4686[9:MRR:4685.0,1101.0] || -> . % 2.43/2.65 4687[9:Spt:4686.0,96.0,4681.0] || -> neq(skc7,nil)*. % 2.43/2.65 4688[9:Spt:4686.0,96.1] || -> equal(app(skc9,cons(skc8,nil)),skc6)**. % 2.43/2.65 4700[9:MRR:95.0,4687.0] || -> equal(app(cons(skc8,nil),skc9),skc7)**. % 2.43/2.65 4704[9:SpL:4688.0,141.2] ssList(skc9) ssList(cons(skc8,nil)) || equal(skc6,skc6) equal(app(cons(skc8,nil),skc9),skc7)** -> . % 2.43/2.65 4709[9:Obv:4704.2] ssList(skc9) ssList(cons(skc8,nil)) || equal(app(cons(skc8,nil),skc9),skc7)** -> . % 2.43/2.65 4710[9:Rew:4700.0,4709.2] ssList(skc9) ssList(cons(skc8,nil)) || equal(skc7,skc7)* -> . % 2.43/2.65 4711[9:Obv:4710.2] ssList(skc9) ssList(cons(skc8,nil)) || -> . % 2.43/2.65 4712[9:SSi:4711.1,4711.0,87.0,2.0,14.1,13.0,10.1,9.0,8.1,12.0,11.1,7.0,76.1,2.0,75.1,2.0,72.1,2.0,71.1,2.0,70.0,2.0,74.0,2.0,73.0,2.0,2490.0,2.0,1.2] || -> . % 2.43/2.65 4713[8:Spt:4712.0,390.0,4680.0] || strictorderP(skc7)* -> . % 2.43/2.65 4714[8:Spt:4712.0,390.1] || -> equal(app(app(skf62(skc7),cons(skf60(skc7),skf63(skc7))),cons(skf61(skc7),skf64(skc7))),skc7)**. % 2.43/2.65 4725[9:Spt:2994.1] || -> equal(skc9,nil)**. % 2.43/2.65 4740[9:Rew:4725.0,2905.1] || neq(skc7,nil) -> equal(cons(skc8,nil),skc7)**. % 2.43/2.65 4742[9:Rew:4725.0,96.1] || neq(skc7,nil) -> equal(app(nil,cons(skc8,nil)),skc6)**. % 2.43/2.65 4750[9:Rew:4740.1,4742.1] || neq(skc7,nil) -> equal(app(nil,skc7),skc6)**. % 2.43/2.65 4751[9:Rew:449.0,4750.1] || neq(skc7,nil)* -> equal(skc7,skc6). % 2.43/2.65 4752[9:MRR:4751.1,4214.0] || neq(skc7,nil)* -> . % 2.43/2.65 4765[9:Res:106.2,4752.0] ssList(nil) ssList(skc7) || -> equal(skc7,nil)**. % 2.43/2.65 4767[9:SSi:4765.1,4765.0,3.0,1912.0,1908.0,4676.0,14.0,13.0,10.0,9.0,8.0,12.0,11.0,7.0] || -> equal(skc7,nil)**. % 2.43/2.65 4768[9:MRR:4767.0,1101.0] || -> . % 2.43/2.65 4769[9:Spt:4768.0,2994.1,4725.0] || equal(skc9,nil)** -> . % 2.43/2.65 4770[9:Spt:4768.0,2994.0] || -> strictorderedP(skc9)*. % 2.43/2.65 4791[10:Spt:96.0] || neq(skc7,nil)* -> . % 2.43/2.65 4793[10:Res:106.2,4791.0] ssList(nil) ssList(skc7) || -> equal(skc7,nil)**. % 2.43/2.65 4795[10:SSi:4793.1,4793.0,3.0,1912.0,1908.0,4676.0,14.0,13.0,10.0,9.0,8.0,12.0,11.0,7.0] || -> equal(skc7,nil)**. % 2.43/2.65 4796[10:MRR:4795.0,1101.0] || -> . % 2.43/2.65 4797[10:Spt:4796.0,96.0,4791.0] || -> neq(skc7,nil)*. % 2.43/2.65 4798[10:Spt:4796.0,96.1] || -> equal(app(skc9,cons(skc8,nil)),skc6)**. % 2.43/2.65 4811[10:MRR:95.0,4797.0] || -> equal(app(cons(skc8,nil),skc9),skc7)**. % 2.43/2.65 4815[10:SpL:4798.0,141.2] ssList(skc9) ssList(cons(skc8,nil)) || equal(skc6,skc6) equal(app(cons(skc8,nil),skc9),skc7)** -> . % 2.43/2.65 4821[10:Obv:4815.2] ssList(skc9) ssList(cons(skc8,nil)) || equal(app(cons(skc8,nil),skc9),skc7)** -> . % 2.43/2.65 4822[10:Rew:4811.0,4821.2] ssList(skc9) ssList(cons(skc8,nil)) || equal(skc7,skc7)* -> . % 2.43/2.65 4823[10:Obv:4822.2] ssList(skc9) ssList(cons(skc8,nil)) || -> . % 2.43/2.65 4824[10:SSi:4823.1,4823.0,87.0,2.0,14.0,13.1,10.0,9.1,8.0,12.1,11.0,7.1,76.0,2.1,75.0,2.1,72.0,2.1,71.0,2.1,70.0,2.0,74.0,2.0,73.0,2.0,2490.0,2.0,4770.0,1.2] || -> . % 2.43/2.65 4825[7:Spt:4824.0,389.0,4676.0] || totalorderP(skc7)* -> . % 2.43/2.65 4826[7:Spt:4824.0,389.1] || -> equal(app(app(skf57(skc7),cons(skf55(skc7),skf58(skc7))),cons(skf56(skc7),skf59(skc7))),skc7)**. % 2.43/2.65 4836[8:Spt:390.0] || -> strictorderP(skc7)*. % 2.43/2.65 4838[9:Spt:2994.1] || -> equal(skc9,nil)**. % 2.43/2.65 4853[9:Rew:4838.0,2905.1] || neq(skc7,nil) -> equal(cons(skc8,nil),skc7)**. % 2.43/2.65 4855[9:Rew:4838.0,96.1] || neq(skc7,nil) -> equal(app(nil,cons(skc8,nil)),skc6)**. % 2.43/2.65 4863[9:Rew:4853.1,4855.1] || neq(skc7,nil) -> equal(app(nil,skc7),skc6)**. % 2.43/2.65 4864[9:Rew:449.0,4863.1] || neq(skc7,nil)* -> equal(skc7,skc6). % 2.43/2.65 4865[9:MRR:4864.1,4214.0] || neq(skc7,nil)* -> . % 2.43/2.65 4876[9:Res:106.2,4865.0] ssList(nil) ssList(skc7) || -> equal(skc7,nil)**. % 2.43/2.65 4878[9:SSi:4876.1,4876.0,3.0,1912.0,1908.0,4836.0,14.0,13.0,10.0,9.0,8.0,12.0,11.0,7.0] || -> equal(skc7,nil)**. % 2.43/2.65 4879[9:MRR:4878.0,1101.0] || -> . % 2.43/2.65 4880[9:Spt:4879.0,2994.1,4838.0] || equal(skc9,nil)** -> . % 2.43/2.65 4881[9:Spt:4879.0,2994.0] || -> strictorderedP(skc9)*. % 2.43/2.65 4903[1:SpL:2929.0,129.2] ssList(skc9) ssItem(hd(skc7)) || totalorderedP(skc7) -> totalorderedP(skc9)* equal(skc9,nil). % 2.43/2.65 4904[9:SSi:4903.1,4903.0,1104.0,4881.0,1.0] || totalorderedP(skc7) -> totalorderedP(skc9)* equal(skc9,nil). % 2.43/2.65 4905[9:MRR:4904.0,4904.2,1908.0,4880.0] || -> totalorderedP(skc9)*. % 2.43/2.65 4906[10:Spt:96.0] || neq(skc7,nil)* -> . % 2.43/2.65 4908[10:Res:106.2,4906.0] ssList(nil) ssList(skc7) || -> equal(skc7,nil)**. % 2.43/2.65 4910[10:SSi:4908.1,4908.0,3.0,1912.0,1908.0,4836.0,14.0,13.0,10.0,9.0,8.0,12.0,11.0,7.0] || -> equal(skc7,nil)**. % 2.43/2.65 4911[10:MRR:4910.0,1101.0] || -> . % 2.43/2.65 4912[10:Spt:4911.0,96.0,4906.0] || -> neq(skc7,nil)*. % 2.43/2.65 4913[10:Spt:4911.0,96.1] || -> equal(app(skc9,cons(skc8,nil)),skc6)**. % 2.43/2.65 4926[10:MRR:95.0,4912.0] || -> equal(app(cons(skc8,nil),skc9),skc7)**. % 2.43/2.65 4930[10:SpL:4913.0,141.2] ssList(skc9) ssList(cons(skc8,nil)) || equal(skc6,skc6) equal(app(cons(skc8,nil),skc9),skc7)** -> . % 2.43/2.65 4936[10:Obv:4930.2] ssList(skc9) ssList(cons(skc8,nil)) || equal(app(cons(skc8,nil),skc9),skc7)** -> . % 2.43/2.65 4937[10:Rew:4926.0,4936.2] ssList(skc9) ssList(cons(skc8,nil)) || equal(skc7,skc7)* -> . % 2.43/2.65 4938[10:Obv:4937.2] ssList(skc9) ssList(cons(skc8,nil)) || -> . % 2.43/2.65 4939[10:SSi:4938.1,4938.0,87.0,2.0,14.0,13.0,10.1,9.0,8.1,12.0,11.1,7.0,76.1,2.0,75.1,2.0,72.1,2.0,71.1,2.0,70.1,2.0,74.0,2.0,73.0,2.0,2490.0,2.0,4881.0,1.0,4905.2] || -> . % 2.43/2.65 4940[8:Spt:4939.0,390.0,4836.0] || strictorderP(skc7)* -> . % 2.43/2.65 4941[8:Spt:4939.0,390.1] || -> equal(app(app(skf62(skc7),cons(skf60(skc7),skf63(skc7))),cons(skf61(skc7),skf64(skc7))),skc7)**. % 2.43/2.65 4944[1:SSi:4903.0,1.0] ssItem(hd(skc7)) || totalorderedP(skc7) -> totalorderedP(skc9)* equal(skc9,nil). % 2.43/2.65 4945[2:MRR:4944.1,1908.0] ssItem(hd(skc7)) || -> totalorderedP(skc9)* equal(skc9,nil). % 2.43/2.65 4946[2:MRR:4945.0,1104.0] || -> totalorderedP(skc9)* equal(skc9,nil). % 2.43/2.65 4955[9:Spt:2994.1] || -> equal(skc9,nil)**. % 2.43/2.65 4970[9:Rew:4955.0,2905.1] || neq(skc7,nil) -> equal(cons(skc8,nil),skc7)**. % 2.43/2.65 4972[9:Rew:4955.0,96.1] || neq(skc7,nil) -> equal(app(nil,cons(skc8,nil)),skc6)**. % 2.43/2.65 4980[9:Rew:4970.1,4972.1] || neq(skc7,nil) -> equal(app(nil,skc7),skc6)**. % 2.43/2.65 4981[9:Rew:449.0,4980.1] || neq(skc7,nil)* -> equal(skc7,skc6). % 2.43/2.65 4982[9:MRR:4981.1,4214.0] || neq(skc7,nil)* -> . % 2.43/2.65 4995[9:Res:106.2,4982.0] ssList(nil) ssList(skc7) || -> equal(skc7,nil)**. % 2.43/2.65 4997[9:SSi:4995.1,4995.0,3.0,1912.0,1908.0,14.0,13.0,10.0,9.0,8.0,12.0,11.0,7.0] || -> equal(skc7,nil)**. % 2.43/2.65 4998[9:MRR:4997.0,1101.0] || -> . % 2.43/2.65 4999[9:Spt:4998.0,2994.1,4955.0] || equal(skc9,nil)** -> . % 2.43/2.65 5000[9:Spt:4998.0,2994.0] || -> strictorderedP(skc9)*. % 2.43/2.65 5001[9:MRR:4946.1,4999.0] || -> totalorderedP(skc9)*. % 2.43/2.65 5028[10:Spt:96.0] || neq(skc7,nil)* -> . % 2.43/2.65 5030[10:Res:106.2,5028.0] ssList(nil) ssList(skc7) || -> equal(skc7,nil)**. % 2.43/2.65 5032[10:SSi:5030.1,5030.0,3.0,1912.0,1908.0,14.0,13.0,10.0,9.0,8.0,12.0,11.0,7.0] || -> equal(skc7,nil)**. % 2.43/2.65 5033[10:MRR:5032.0,1101.0] || -> . % 2.43/2.65 5034[10:Spt:5033.0,96.0,5028.0] || -> neq(skc7,nil)*. % 2.43/2.65 5035[10:Spt:5033.0,96.1] || -> equal(app(skc9,cons(skc8,nil)),skc6)**. % 2.43/2.65 5049[10:MRR:95.0,5034.0] || -> equal(app(cons(skc8,nil),skc9),skc7)**. % 2.43/2.65 5053[10:SpL:5035.0,141.2] ssList(skc9) ssList(cons(skc8,nil)) || equal(skc6,skc6) equal(app(cons(skc8,nil),skc9),skc7)** -> . % 2.43/2.65 5059[10:Obv:5053.2] ssList(skc9) ssList(cons(skc8,nil)) || equal(app(cons(skc8,nil),skc9),skc7)** -> . % 2.43/2.65 5060[10:Rew:5049.0,5059.2] ssList(skc9) ssList(cons(skc8,nil)) || equal(skc7,skc7)* -> . % 2.43/2.65 5061[10:Obv:5060.2] ssList(skc9) ssList(cons(skc8,nil)) || -> . % 2.43/2.65 5062[10:SSi:5061.1,5061.0,87.0,2.0,14.0,13.0,10.1,9.0,8.1,12.0,11.1,7.0,76.1,2.0,75.1,2.0,72.1,2.0,71.1,2.0,70.1,2.0,74.0,2.0,73.0,2.0,2490.0,2.0,5000.0,1.0,5001.2] || -> . % 2.43/2.65 5063[5:Spt:5062.0,219.0,1919.0] || strictorderedP(skc6)* -> . % 2.43/2.65 5064[5:Spt:5062.0,219.1] || -> equal(app(app(skf72(skc6),cons(skf70(skc6),skf73(skc6))),cons(skf71(skc6),skf74(skc6))),skc6)**. % 2.43/2.65 5067[4:SSi:3730.1,3730.0,4.0,1915.0,14.0,13.0,10.0,9.0,8.0,12.0,11.0,7.0] || equal(skc7,skc6)** -> . % 2.43/2.65 5092[6:Spt:436.0] || -> cyclefreeP(skc7)*. % 2.43/2.65 5098[7:Spt:390.0] || -> strictorderP(skc7)*. % 2.43/2.65 5100[8:Spt:389.0] || -> totalorderP(skc7)*. % 2.43/2.65 5103[9:Spt:95.0] || neq(skc7,nil)* -> . % 2.43/2.65 5105[9:Res:106.2,5103.0] ssList(nil) ssList(skc7) || -> equal(skc7,nil)**. % 2.43/2.65 5107[9:SSi:5105.1,5105.0,3.0,1912.0,1908.0,5092.0,5098.0,5100.0,14.0,13.0,10.0,9.0,8.0,12.0,11.0,7.0] || -> equal(skc7,nil)**. % 2.43/2.65 5108[9:MRR:5107.0,1101.0] || -> . % 2.43/2.65 5109[9:Spt:5108.0,95.0,5103.0] || -> neq(skc7,nil)*. % 2.43/2.65 5110[9:Spt:5108.0,95.1] || -> equal(app(cons(skc8,nil),skc9),skc7)**. % 2.43/2.65 5111[9:MRR:2921.0,5109.0] || -> equal(hd(skc7),skc8)**. % 2.43/2.65 5113[9:Rew:5111.0,2929.0] || -> equal(cons(skc8,skc9),skc7)**. % 2.43/2.65 5122[9:MRR:96.0,5109.0] || -> equal(app(skc9,cons(skc8,nil)),skc6)**. % 2.43/2.65 5142[10:Spt:4946.1] || -> equal(skc9,nil)**. % 2.43/2.65 5157[10:Rew:5142.0,5113.0] || -> equal(cons(skc8,nil),skc7)**. % 2.43/2.65 5158[10:Rew:5142.0,5122.0] || -> equal(app(nil,cons(skc8,nil)),skc6)**. % 2.43/2.65 5164[10:Rew:5157.0,5158.0] || -> equal(app(nil,skc7),skc6)**. % 2.43/2.65 5165[10:Rew:449.0,5164.0] || -> equal(skc7,skc6)**. % 2.43/2.65 5166[10:MRR:5165.0,5067.0] || -> . % 2.43/2.65 5198[10:Spt:5166.0,4946.1,5142.0] || equal(skc9,nil)** -> . % 2.43/2.65 5199[10:Spt:5166.0,4946.0] || -> totalorderedP(skc9)*. % 2.43/2.65 5200[10:MRR:2994.1,5198.0] || -> strictorderedP(skc9)*. % 2.43/2.65 5218[9:SpL:5122.0,141.2] ssList(skc9) ssList(cons(skc8,nil)) || equal(skc6,skc6) equal(app(cons(skc8,nil),skc9),skc7)** -> . % 2.43/2.65 5224[9:Obv:5218.2] ssList(skc9) ssList(cons(skc8,nil)) || equal(app(cons(skc8,nil),skc9),skc7)** -> . % 2.43/2.65 5225[9:Rew:5110.0,5224.2] ssList(skc9) ssList(cons(skc8,nil)) || equal(skc7,skc7)* -> . % 2.43/2.65 5226[9:Obv:5225.2] ssList(skc9) ssList(cons(skc8,nil)) || -> . % 2.43/2.65 5227[10:SSi:5226.1,5226.0,87.0,2.0,14.0,13.0,10.1,9.0,8.1,12.0,11.1,7.0,76.1,2.0,75.1,2.0,72.1,2.0,71.1,2.0,70.1,2.0,74.0,2.0,73.0,2.0,2490.0,2.0,5199.0,1.0,5200.2] || -> . % 2.43/2.65 5228[8:Spt:5227.0,389.0,5100.0] || totalorderP(skc7)* -> . % 2.43/2.65 5229[8:Spt:5227.0,389.1] || -> equal(app(app(skf57(skc7),cons(skf55(skc7),skf58(skc7))),cons(skf56(skc7),skf59(skc7))),skc7)**. % 2.43/2.65 5250[9:Spt:96.0] || neq(skc7,nil)* -> . % 2.43/2.65 5252[9:Res:106.2,5250.0] ssList(nil) ssList(skc7) || -> equal(skc7,nil)**. % 2.43/2.65 5254[9:SSi:5252.1,5252.0,3.0,1912.0,1908.0,5092.0,5098.0,14.0,13.0,10.0,9.0,8.0,12.0,11.0,7.0] || -> equal(skc7,nil)**. % 2.43/2.65 5255[9:MRR:5254.0,1101.0] || -> . % 2.43/2.65 5256[9:Spt:5255.0,96.0,5250.0] || -> neq(skc7,nil)*. % 2.43/2.65 5257[9:Spt:5255.0,96.1] || -> equal(app(skc9,cons(skc8,nil)),skc6)**. % 2.43/2.65 5270[9:MRR:95.0,5256.0] || -> equal(app(cons(skc8,nil),skc9),skc7)**. % 2.43/2.65 5274[9:SpL:5257.0,141.2] ssList(skc9) ssList(cons(skc8,nil)) || equal(skc6,skc6) equal(app(cons(skc8,nil),skc9),skc7)** -> . % 2.43/2.65 5279[9:Obv:5274.2] ssList(skc9) ssList(cons(skc8,nil)) || equal(app(cons(skc8,nil),skc9),skc7)** -> . % 2.43/2.65 5280[9:Rew:5270.0,5279.2] ssList(skc9) ssList(cons(skc8,nil)) || equal(skc7,skc7)* -> . % 2.43/2.65 5281[9:Obv:5280.2] ssList(skc9) ssList(cons(skc8,nil)) || -> . % 2.43/2.65 5282[9:SSi:5281.1,5281.0,87.0,2.0,14.1,13.0,10.1,9.0,8.1,12.0,11.1,7.0,76.1,2.0,75.1,2.0,72.1,2.0,71.1,2.0,70.0,2.0,74.0,2.0,73.0,2.0,2490.0,2.0,1.2] || -> . % 2.43/2.65 5283[7:Spt:5282.0,390.0,5098.0] || strictorderP(skc7)* -> . % 2.43/2.65 5284[7:Spt:5282.0,390.1] || -> equal(app(app(skf62(skc7),cons(skf60(skc7),skf63(skc7))),cons(skf61(skc7),skf64(skc7))),skc7)**. % 2.43/2.65 5301[8:Spt:389.0] || -> totalorderP(skc7)*. % 2.43/2.65 5306[9:Spt:95.0] || neq(skc7,nil)* -> . % 2.43/2.65 5308[9:Res:106.2,5306.0] ssList(nil) ssList(skc7) || -> equal(skc7,nil)**. % 2.43/2.65 5310[9:SSi:5308.1,5308.0,3.0,1912.0,1908.0,5092.0,5301.0,14.0,13.0,10.0,9.0,8.0,12.0,11.0,7.0] || -> equal(skc7,nil)**. % 2.43/2.65 5311[9:MRR:5310.0,1101.0] || -> . % 2.43/2.65 5312[9:Spt:5311.0,95.0,5306.0] || -> neq(skc7,nil)*. % 2.43/2.65 5313[9:Spt:5311.0,95.1] || -> equal(app(cons(skc8,nil),skc9),skc7)**. % 2.43/2.65 5314[9:MRR:2921.0,5312.0] || -> equal(hd(skc7),skc8)**. % 2.43/2.65 5316[9:Rew:5314.0,2929.0] || -> equal(cons(skc8,skc9),skc7)**. % 2.43/2.65 5326[9:MRR:96.0,5312.0] || -> equal(app(skc9,cons(skc8,nil)),skc6)**. % 2.43/2.65 5344[10:Spt:2994.1] || -> equal(skc9,nil)**. % 2.43/2.65 5359[10:Rew:5344.0,5316.0] || -> equal(cons(skc8,nil),skc7)**. % 2.43/2.65 5360[10:Rew:5344.0,5326.0] || -> equal(app(nil,cons(skc8,nil)),skc6)**. % 2.43/2.65 5366[10:Rew:5359.0,5360.0] || -> equal(app(nil,skc7),skc6)**. % 2.43/2.65 5367[10:Rew:449.0,5366.0] || -> equal(skc7,skc6)**. % 2.43/2.65 5368[10:MRR:5367.0,5067.0] || -> . % 2.43/2.65 5400[10:Spt:5368.0,2994.1,5344.0] || equal(skc9,nil)** -> . % 2.43/2.65 5401[10:Spt:5368.0,2994.0] || -> strictorderedP(skc9)*. % 2.43/2.65 5402[10:MRR:4946.1,5400.0] || -> totalorderedP(skc9)*. % 2.43/2.65 5419[9:SpL:5326.0,141.2] ssList(skc9) ssList(cons(skc8,nil)) || equal(skc6,skc6) equal(app(cons(skc8,nil),skc9),skc7)** -> . % 2.43/2.65 5425[9:Obv:5419.2] ssList(skc9) ssList(cons(skc8,nil)) || equal(app(cons(skc8,nil),skc9),skc7)** -> . % 2.43/2.65 5426[9:Rew:5313.0,5425.2] ssList(skc9) ssList(cons(skc8,nil)) || equal(skc7,skc7)* -> . % 2.43/2.65 5427[9:Obv:5426.2] ssList(skc9) ssList(cons(skc8,nil)) || -> . % 2.43/2.65 5428[10:SSi:5427.1,5427.0,87.0,2.0,14.0,13.0,10.1,9.0,8.1,12.0,11.1,7.0,76.1,2.0,75.1,2.0,72.1,2.0,71.1,2.0,70.1,2.0,74.0,2.0,73.0,2.0,2490.0,2.0,5401.0,1.0,5402.2] || -> . % 2.43/2.65 5429[8:Spt:5428.0,389.0,5301.0] || totalorderP(skc7)* -> . % 2.43/2.65 5430[8:Spt:5428.0,389.1] || -> equal(app(app(skf57(skc7),cons(skf55(skc7),skf58(skc7))),cons(skf56(skc7),skf59(skc7))),skc7)**. % 2.43/2.65 5441[9:Spt:4946.1] || -> equal(skc9,nil)**. % 2.43/2.65 5456[9:Rew:5441.0,2905.1] || neq(skc7,nil) -> equal(cons(skc8,nil),skc7)**. % 2.43/2.65 5457[9:Rew:5441.0,96.1] || neq(skc7,nil) -> equal(app(nil,cons(skc8,nil)),skc6)**. % 2.43/2.65 5465[9:Rew:5456.1,5457.1] || neq(skc7,nil) -> equal(app(nil,skc7),skc6)**. % 2.43/2.65 5466[9:Rew:449.0,5465.1] || neq(skc7,nil)* -> equal(skc7,skc6). % 2.43/2.65 5467[9:MRR:5466.1,5067.0] || neq(skc7,nil)* -> . % 2.43/2.65 5478[9:Res:106.2,5467.0] ssList(nil) ssList(skc7) || -> equal(skc7,nil)**. % 2.43/2.65 5480[9:SSi:5478.1,5478.0,3.0,1912.0,1908.0,5092.0,14.0,13.0,10.0,9.0,8.0,12.0,11.0,7.0] || -> equal(skc7,nil)**. % 2.43/2.65 5481[9:MRR:5480.0,1101.0] || -> . % 2.43/2.65 5482[9:Spt:5481.0,4946.1,5441.0] || equal(skc9,nil)** -> . % 2.43/2.65 5483[9:Spt:5481.0,4946.0] || -> totalorderedP(skc9)*. % 2.43/2.65 5484[9:MRR:2994.1,5482.0] || -> strictorderedP(skc9)*. % 2.43/2.65 5503[10:Spt:95.0] || neq(skc7,nil)* -> . % 2.43/2.65 5505[10:Res:106.2,5503.0] ssList(nil) ssList(skc7) || -> equal(skc7,nil)**. % 2.43/2.65 5507[10:SSi:5505.1,5505.0,3.0,1912.0,1908.0,5092.0,14.0,13.0,10.0,9.0,8.0,12.0,11.0,7.0] || -> equal(skc7,nil)**. % 2.43/2.65 5508[10:MRR:5507.0,1101.0] || -> . % 2.43/2.65 5509[10:Spt:5508.0,95.0,5503.0] || -> neq(skc7,nil)*. % 2.43/2.65 5510[10:Spt:5508.0,95.1] || -> equal(app(cons(skc8,nil),skc9),skc7)**. % 2.43/2.65 5524[10:MRR:96.0,5509.0] || -> equal(app(skc9,cons(skc8,nil)),skc6)**. % 2.43/2.65 5555[10:SpL:5524.0,141.2] ssList(skc9) ssList(cons(skc8,nil)) || equal(skc6,skc6) equal(app(cons(skc8,nil),skc9),skc7)** -> . % 2.43/2.65 5561[10:Obv:5555.2] ssList(skc9) ssList(cons(skc8,nil)) || equal(app(cons(skc8,nil),skc9),skc7)** -> . % 2.43/2.65 5562[10:Rew:5510.0,5561.2] ssList(skc9) ssList(cons(skc8,nil)) || equal(skc7,skc7)* -> . % 2.43/2.65 5563[10:Obv:5562.2] ssList(skc9) ssList(cons(skc8,nil)) || -> . % 2.43/2.65 5564[10:SSi:5563.1,5563.0,87.0,2.0,14.0,13.0,10.1,9.0,8.1,12.0,11.1,7.0,76.1,2.0,75.1,2.0,72.1,2.0,71.1,2.0,70.1,2.0,74.0,2.0,73.0,2.0,2490.0,2.0,5483.0,1.0,5484.2] || -> . % 2.43/2.65 5565[6:Spt:5564.0,436.0,5092.0] || cyclefreeP(skc7)* -> . % 2.43/2.65 5566[6:Spt:5564.0,436.1] || -> leq(skf51(skc7),skf50(skc7))*. % 2.43/2.65 5577[7:Spt:389.0] || -> totalorderP(skc7)*. % 2.43/2.65 5586[8:Spt:390.0] || -> strictorderP(skc7)*. % 2.43/2.65 5587[9:Spt:2994.1] || -> equal(skc9,nil)**. % 2.43/2.65 5602[9:Rew:5587.0,2905.1] || neq(skc7,nil) -> equal(cons(skc8,nil),skc7)**. % 2.43/2.65 5603[9:Rew:5587.0,96.1] || neq(skc7,nil) -> equal(app(nil,cons(skc8,nil)),skc6)**. % 2.43/2.65 5611[9:Rew:5602.1,5603.1] || neq(skc7,nil) -> equal(app(nil,skc7),skc6)**. % 2.43/2.65 5612[9:Rew:449.0,5611.1] || neq(skc7,nil)* -> equal(skc7,skc6). % 2.43/2.65 5613[9:MRR:5612.1,5067.0] || neq(skc7,nil)* -> . % 2.43/2.65 5621[9:Res:106.2,5613.0] ssList(nil) ssList(skc7) || -> equal(skc7,nil)**. % 2.43/2.65 5623[9:SSi:5621.1,5621.0,3.0,1912.0,1908.0,5577.0,5586.0,14.0,13.0,10.0,9.0,8.0,12.0,11.0,7.0] || -> equal(skc7,nil)**. % 2.43/2.65 5624[9:MRR:5623.0,1101.0] || -> . % 2.43/2.65 5625[9:Spt:5624.0,2994.1,5587.0] || equal(skc9,nil)** -> . % 2.43/2.65 5626[9:Spt:5624.0,2994.0] || -> strictorderedP(skc9)*. % 2.43/2.65 5627[9:MRR:4946.1,5625.0] || -> totalorderedP(skc9)*. % 2.43/2.65 5654[10:Spt:95.0] || neq(skc7,nil)* -> . % 2.43/2.65 5656[10:Res:106.2,5654.0] ssList(nil) ssList(skc7) || -> equal(skc7,nil)**. % 2.43/2.65 5658[10:SSi:5656.1,5656.0,3.0,1912.0,1908.0,5577.0,5586.0,14.0,13.0,10.0,9.0,8.0,12.0,11.0,7.0] || -> equal(skc7,nil)**. % 2.43/2.65 5659[10:MRR:5658.0,1101.0] || -> . % 2.43/2.65 5660[10:Spt:5659.0,95.0,5654.0] || -> neq(skc7,nil)*. % 2.43/2.65 5661[10:Spt:5659.0,95.1] || -> equal(app(cons(skc8,nil),skc9),skc7)**. % 2.43/2.65 5673[10:MRR:96.0,5660.0] || -> equal(app(skc9,cons(skc8,nil)),skc6)**. % 2.43/2.65 5719[10:SpL:5673.0,141.2] ssList(skc9) ssList(cons(skc8,nil)) || equal(skc6,skc6) equal(app(cons(skc8,nil),skc9),skc7)** -> . % 2.43/2.65 5725[10:Obv:5719.2] ssList(skc9) ssList(cons(skc8,nil)) || equal(app(cons(skc8,nil),skc9),skc7)** -> . % 2.43/2.65 5726[10:Rew:5661.0,5725.2] ssList(skc9) ssList(cons(skc8,nil)) || equal(skc7,skc7)* -> . % 2.43/2.65 5727[10:Obv:5726.2] ssList(skc9) ssList(cons(skc8,nil)) || -> . % 2.43/2.65 5728[10:SSi:5727.1,5727.0,87.0,2.0,14.0,13.0,10.1,9.0,8.1,12.0,11.1,7.0,76.1,2.0,75.1,2.0,72.1,2.0,71.1,2.0,70.1,2.0,74.0,2.0,73.0,2.0,2490.0,2.0,5626.0,1.0,5627.2] || -> . % 2.43/2.65 5729[8:Spt:5728.0,390.0,5586.0] || strictorderP(skc7)* -> . % 2.43/2.65 5730[8:Spt:5728.0,390.1] || -> equal(app(app(skf62(skc7),cons(skf60(skc7),skf63(skc7))),cons(skf61(skc7),skf64(skc7))),skc7)**. % 2.43/2.65 5743[9:Spt:4946.1] || -> equal(skc9,nil)**. % 2.43/2.65 5757[9:Rew:5743.0,2905.1] || neq(skc7,nil) -> equal(cons(skc8,nil),skc7)**. % 2.43/2.65 5758[9:Rew:5743.0,96.1] || neq(skc7,nil) -> equal(app(nil,cons(skc8,nil)),skc6)**. % 2.43/2.65 5766[9:Rew:5757.1,5758.1] || neq(skc7,nil) -> equal(app(nil,skc7),skc6)**. % 2.43/2.65 5767[9:Rew:449.0,5766.1] || neq(skc7,nil)* -> equal(skc7,skc6). % 2.43/2.65 5768[9:MRR:5767.1,5067.0] || neq(skc7,nil)* -> . % 2.43/2.65 5779[9:Res:106.2,5768.0] ssList(nil) ssList(skc7) || -> equal(skc7,nil)**. % 2.43/2.65 5781[9:SSi:5779.1,5779.0,3.0,1912.0,1908.0,5577.0,14.0,13.0,10.0,9.0,8.0,12.0,11.0,7.0] || -> equal(skc7,nil)**. % 2.43/2.65 5782[9:MRR:5781.0,1101.0] || -> . % 2.43/2.65 5783[9:Spt:5782.0,4946.1,5743.0] || equal(skc9,nil)** -> . % 2.43/2.65 5784[9:Spt:5782.0,4946.0] || -> totalorderedP(skc9)*. % 2.43/2.65 5785[9:MRR:2994.1,5783.0] || -> strictorderedP(skc9)*. % 2.43/2.65 5805[10:Spt:95.0] || neq(skc7,nil)* -> . % 2.43/2.65 5807[10:Res:106.2,5805.0] ssList(nil) ssList(skc7) || -> equal(skc7,nil)**. % 2.43/2.65 5809[10:SSi:5807.1,5807.0,3.0,1912.0,1908.0,5577.0,14.0,13.0,10.0,9.0,8.0,12.0,11.0,7.0] || -> equal(skc7,nil)**. % 2.43/2.65 5810[10:MRR:5809.0,1101.0] || -> . % 2.43/2.65 5811[10:Spt:5810.0,95.0,5805.0] || -> neq(skc7,nil)*. % 2.43/2.65 5812[10:Spt:5810.0,95.1] || -> equal(app(cons(skc8,nil),skc9),skc7)**. % 2.43/2.65 5826[10:MRR:96.0,5811.0] || -> equal(app(skc9,cons(skc8,nil)),skc6)**. % 2.43/2.65 5860[10:SpL:5826.0,141.2] ssList(skc9) ssList(cons(skc8,nil)) || equal(skc6,skc6) equal(app(cons(skc8,nil),skc9),skc7)** -> . % 2.43/2.65 5866[10:Obv:5860.2] ssList(skc9) ssList(cons(skc8,nil)) || equal(app(cons(skc8,nil),skc9),skc7)** -> . % 2.43/2.65 5867[10:Rew:5812.0,5866.2] ssList(skc9) ssList(cons(skc8,nil)) || equal(skc7,skc7)* -> . % 2.43/2.65 5868[10:Obv:5867.2] ssList(skc9) ssList(cons(skc8,nil)) || -> . % 2.43/2.65 5869[10:SSi:5868.1,5868.0,87.0,2.0,14.0,13.0,10.1,9.0,8.1,12.0,11.1,7.0,76.1,2.0,75.1,2.0,72.1,2.0,71.1,2.0,70.1,2.0,74.0,2.0,73.0,2.0,2490.0,2.0,5784.0,1.0,5785.2] || -> . % 2.43/2.65 5870[7:Spt:5869.0,389.0,5577.0] || totalorderP(skc7)* -> . % 2.43/2.65 5871[7:Spt:5869.0,389.1] || -> equal(app(app(skf57(skc7),cons(skf55(skc7),skf58(skc7))),cons(skf56(skc7),skf59(skc7))),skc7)**. % 2.43/2.65 5886[8:Spt:390.0] || -> strictorderP(skc7)*. % 2.43/2.65 5892[9:Spt:2994.1] || -> equal(skc9,nil)**. % 2.43/2.65 5906[9:Rew:5892.0,2905.1] || neq(skc7,nil) -> equal(cons(skc8,nil),skc7)**. % 2.43/2.65 5907[9:Rew:5892.0,96.1] || neq(skc7,nil) -> equal(app(nil,cons(skc8,nil)),skc6)**. % 2.43/2.65 5915[9:Rew:5906.1,5907.1] || neq(skc7,nil) -> equal(app(nil,skc7),skc6)**. % 2.43/2.65 5916[9:Rew:449.0,5915.1] || neq(skc7,nil)* -> equal(skc7,skc6). % 2.43/2.65 5917[9:MRR:5916.1,5067.0] || neq(skc7,nil)* -> . % 2.43/2.65 5925[9:Res:106.2,5917.0] ssList(nil) ssList(skc7) || -> equal(skc7,nil)**. % 2.43/2.65 5927[9:SSi:5925.1,5925.0,3.0,1912.0,1908.0,5886.0,14.0,13.0,10.0,9.0,8.0,12.0,11.0,7.0] || -> equal(skc7,nil)**. % 2.43/2.65 5928[9:MRR:5927.0,1101.0] || -> . % 2.43/2.65 5929[9:Spt:5928.0,2994.1,5892.0] || equal(skc9,nil)** -> . % 2.43/2.65 5930[9:Spt:5928.0,2994.0] || -> strictorderedP(skc9)*. % 2.43/2.65 5931[9:MRR:4946.1,5929.0] || -> totalorderedP(skc9)*. % 2.43/2.65 5947[10:Spt:95.0] || neq(skc7,nil)* -> . % 2.43/2.65 5949[10:Res:106.2,5947.0] ssList(nil) ssList(skc7) || -> equal(skc7,nil)**. % 2.43/2.65 5951[10:SSi:5949.1,5949.0,3.0,1912.0,1908.0,5886.0,14.0,13.0,10.0,9.0,8.0,12.0,11.0,7.0] || -> equal(skc7,nil)**. % 2.43/2.65 5952[10:MRR:5951.0,1101.0] || -> . % 2.43/2.65 5953[10:Spt:5952.0,95.0,5947.0] || -> neq(skc7,nil)*. % 2.43/2.65 5954[10:Spt:5952.0,95.1] || -> equal(app(cons(skc8,nil),skc9),skc7)**. % 2.43/2.65 5968[10:MRR:96.0,5953.0] || -> equal(app(skc9,cons(skc8,nil)),skc6)**. % 2.43/2.65 6002[10:SpL:5968.0,141.2] ssList(skc9) ssList(cons(skc8,nil)) || equal(skc6,skc6) equal(app(cons(skc8,nil),skc9),skc7)** -> . % 2.43/2.65 6008[10:Obv:6002.2] ssList(skc9) ssList(cons(skc8,nil)) || equal(app(cons(skc8,nil),skc9),skc7)** -> . % 2.43/2.65 6009[10:Rew:5954.0,6008.2] ssList(skc9) ssList(cons(skc8,nil)) || equal(skc7,skc7)* -> . % 2.43/2.65 6010[10:Obv:6009.2] ssList(skc9) ssList(cons(skc8,nil)) || -> . % 2.43/2.65 6011[10:SSi:6010.1,6010.0,87.0,2.0,14.0,13.0,10.1,9.0,8.1,12.0,11.1,7.0,76.1,2.0,75.1,2.0,72.1,2.0,71.1,2.0,70.1,2.0,74.0,2.0,73.0,2.0,2490.0,2.0,5930.0,1.0,5931.2] || -> . % 2.43/2.65 6012[8:Spt:6011.0,390.0,5886.0] || strictorderP(skc7)* -> . % 2.43/2.65 6013[8:Spt:6011.0,390.1] || -> equal(app(app(skf62(skc7),cons(skf60(skc7),skf63(skc7))),cons(skf61(skc7),skf64(skc7))),skc7)**. % 2.43/2.65 6030[9:Spt:4946.1] || -> equal(skc9,nil)**. % 2.43/2.65 6044[9:Rew:6030.0,2905.1] || neq(skc7,nil) -> equal(cons(skc8,nil),skc7)**. % 2.43/2.65 6045[9:Rew:6030.0,96.1] || neq(skc7,nil) -> equal(app(nil,cons(skc8,nil)),skc6)**. % 2.43/2.65 6053[9:Rew:6044.1,6045.1] || neq(skc7,nil) -> equal(app(nil,skc7),skc6)**. % 2.43/2.65 6054[9:Rew:449.0,6053.1] || neq(skc7,nil)* -> equal(skc7,skc6). % 2.43/2.65 6055[9:MRR:6054.1,5067.0] || neq(skc7,nil)* -> . % 2.43/2.65 6063[9:Res:106.2,6055.0] ssList(nil) ssList(skc7) || -> equal(skc7,nil)**. % 2.43/2.65 6065[9:SSi:6063.1,6063.0,3.0,1912.0,1908.0,14.0,13.0,10.0,9.0,8.0,12.0,11.0,7.0] || -> equal(skc7,nil)**. % 2.43/2.65 6066[9:MRR:6065.0,1101.0] || -> . % 2.43/2.65 6067[9:Spt:6066.0,4946.1,6030.0] || equal(skc9,nil)** -> . % 2.43/2.65 6068[9:Spt:6066.0,4946.0] || -> totalorderedP(skc9)*. % 2.43/2.65 6069[9:MRR:2994.1,6067.0] || -> strictorderedP(skc9)*. % 2.43/2.65 6096[10:Spt:95.0] || neq(skc7,nil)* -> . % 2.43/2.65 6098[10:Res:106.2,6096.0] ssList(nil) ssList(skc7) || -> equal(skc7,nil)**. % 2.43/2.65 6100[10:SSi:6098.1,6098.0,3.0,1912.0,1908.0,14.0,13.0,10.0,9.0,8.0,12.0,11.0,7.0] || -> equal(skc7,nil)**. % 2.43/2.65 6101[10:MRR:6100.0,1101.0] || -> . % 2.43/2.65 6102[10:Spt:6101.0,95.0,6096.0] || -> neq(skc7,nil)*. % 2.43/2.65 6103[10:Spt:6101.0,95.1] || -> equal(app(cons(skc8,nil),skc9),skc7)**. % 2.43/2.65 6118[10:MRR:96.0,6102.0] || -> equal(app(skc9,cons(skc8,nil)),skc6)**. % 2.43/2.65 6152[10:SpL:6118.0,141.2] ssList(skc9) ssList(cons(skc8,nil)) || equal(skc6,skc6) equal(app(cons(skc8,nil),skc9),skc7)** -> . % 2.43/2.65 6158[10:Obv:6152.2] ssList(skc9) ssList(cons(skc8,nil)) || equal(app(cons(skc8,nil),skc9),skc7)** -> . % 2.43/2.65 6159[10:Rew:6103.0,6158.2] ssList(skc9) ssList(cons(skc8,nil)) || equal(skc7,skc7)* -> . % 2.43/2.65 6160[10:Obv:6159.2] ssList(skc9) ssList(cons(skc8,nil)) || -> . % 2.43/2.65 6161[10:SSi:6160.1,6160.0,87.0,2.0,14.0,13.0,10.1,9.0,8.1,12.0,11.1,7.0,76.1,2.0,75.1,2.0,72.1,2.0,71.1,2.0,70.1,2.0,74.0,2.0,73.0,2.0,2490.0,2.0,6068.0,1.0,6069.2] || -> . % 2.43/2.65 6162[4:Spt:6161.0,218.0,1915.0] || totalorderedP(skc6)* -> . % 2.43/2.65 6163[4:Spt:6161.0,218.1] || -> equal(app(app(skf67(skc6),cons(skf65(skc6),skf68(skc6))),cons(skf66(skc6),skf69(skc6))),skc6)**. % 2.43/2.65 6166[0:SSi:3730.1,3730.0,4.0,14.0,13.0,10.0,9.0,8.0,12.0,11.0,7.0] || equal(skc7,skc6)** -> . % 2.43/2.65 6192[5:Spt:437.0] || -> cyclefreeP(skc7)*. % 2.43/2.65 6204[6:Spt:96.0] || neq(skc7,nil)* -> . % 2.43/2.65 6206[6:Res:106.2,6204.0] ssList(nil) ssList(skc7) || -> equal(skc7,nil)**. % 2.43/2.65 6208[6:SSi:6206.1,6206.0,3.0,1912.0,1908.0,6192.0,14.0,13.0,10.0,9.0,8.0,12.0,11.0,7.0] || -> equal(skc7,nil)**. % 2.43/2.65 6209[6:MRR:6208.0,1101.0] || -> . % 2.43/2.65 6210[6:Spt:6209.0,96.0,6204.0] || -> neq(skc7,nil)*. % 2.43/2.65 6211[6:Spt:6209.0,96.1] || -> equal(app(skc9,cons(skc8,nil)),skc6)**. % 2.43/2.65 6224[6:MRR:95.0,6210.0] || -> equal(app(cons(skc8,nil),skc9),skc7)**. % 2.43/2.65 6228[6:SpL:6211.0,141.2] ssList(skc9) ssList(cons(skc8,nil)) || equal(skc6,skc6) equal(app(cons(skc8,nil),skc9),skc7)** -> . % 2.43/2.65 6233[6:Obv:6228.2] ssList(skc9) ssList(cons(skc8,nil)) || equal(app(cons(skc8,nil),skc9),skc7)** -> . % 2.43/2.65 6234[6:Rew:6224.0,6233.2] ssList(skc9) ssList(cons(skc8,nil)) || equal(skc7,skc7)* -> . % 2.43/2.65 6235[6:Obv:6234.2] ssList(skc9) ssList(cons(skc8,nil)) || -> . % 2.43/2.65 6236[6:SSi:6235.1,6235.0,87.0,2.0,14.1,13.0,10.1,9.0,8.1,12.0,11.1,7.0,76.1,2.0,75.1,2.0,72.1,2.0,71.1,2.0,70.0,2.0,74.0,2.0,73.0,2.0,2490.0,2.0,1.2] || -> . % 2.43/2.65 6237[5:Spt:6236.0,437.0,6192.0] || cyclefreeP(skc7)* -> . % 2.43/2.65 6238[5:Spt:6236.0,437.1] || -> leq(skf50(skc7),skf51(skc7))*. % 2.43/2.65 6250[6:Spt:390.0] || -> strictorderP(skc7)*. % 2.43/2.65 6255[7:Spt:389.0] || -> totalorderP(skc7)*. % 2.43/2.65 6259[8:Spt:2994.1] || -> equal(skc9,nil)**. % 2.43/2.65 6273[8:Rew:6259.0,2905.1] || neq(skc7,nil) -> equal(cons(skc8,nil),skc7)**. % 2.43/2.65 6275[8:Rew:6259.0,96.1] || neq(skc7,nil) -> equal(app(nil,cons(skc8,nil)),skc6)**. % 2.43/2.65 6283[8:Rew:6273.1,6275.1] || neq(skc7,nil) -> equal(app(nil,skc7),skc6)**. % 2.43/2.65 6284[8:Rew:449.0,6283.1] || neq(skc7,nil)* -> equal(skc7,skc6). % 2.43/2.65 6285[8:MRR:6284.1,6166.0] || neq(skc7,nil)* -> . % 2.43/2.65 6294[8:Res:106.2,6285.0] ssList(nil) ssList(skc7) || -> equal(skc7,nil)**. % 2.43/2.65 6296[8:SSi:6294.1,6294.0,3.0,1912.0,1908.0,6250.0,6255.0,14.0,13.0,10.0,9.0,8.0,12.0,11.0,7.0] || -> equal(skc7,nil)**. % 2.43/2.65 6297[8:MRR:6296.0,1101.0] || -> . % 2.43/2.65 6298[8:Spt:6297.0,2994.1,6259.0] || equal(skc9,nil)** -> . % 2.43/2.65 6299[8:Spt:6297.0,2994.0] || -> strictorderedP(skc9)*. % 2.43/2.65 6300[8:MRR:4946.1,6298.0] || -> totalorderedP(skc9)*. % 2.43/2.65 6323[9:Spt:96.0] || neq(skc7,nil)* -> . % 2.43/2.65 6325[9:Res:106.2,6323.0] ssList(nil) ssList(skc7) || -> equal(skc7,nil)**. % 2.43/2.65 6327[9:SSi:6325.1,6325.0,3.0,1912.0,1908.0,6250.0,6255.0,14.0,13.0,10.0,9.0,8.0,12.0,11.0,7.0] || -> equal(skc7,nil)**. % 2.43/2.65 6328[9:MRR:6327.0,1101.0] || -> . % 2.43/2.65 6329[9:Spt:6328.0,96.0,6323.0] || -> neq(skc7,nil)*. % 2.43/2.65 6330[9:Spt:6328.0,96.1] || -> equal(app(skc9,cons(skc8,nil)),skc6)**. % 2.43/2.65 6343[9:MRR:95.0,6329.0] || -> equal(app(cons(skc8,nil),skc9),skc7)**. % 2.43/2.65 6347[9:SpL:6330.0,141.2] ssList(skc9) ssList(cons(skc8,nil)) || equal(skc6,skc6) equal(app(cons(skc8,nil),skc9),skc7)** -> . % 2.43/2.65 6353[9:Obv:6347.2] ssList(skc9) ssList(cons(skc8,nil)) || equal(app(cons(skc8,nil),skc9),skc7)** -> . % 2.43/2.65 6354[9:Rew:6343.0,6353.2] ssList(skc9) ssList(cons(skc8,nil)) || equal(skc7,skc7)* -> . % 2.43/2.65 6355[9:Obv:6354.2] ssList(skc9) ssList(cons(skc8,nil)) || -> . % 2.43/2.65 6356[9:SSi:6355.1,6355.0,87.0,2.0,14.0,13.0,10.1,9.0,8.1,12.0,11.1,7.0,76.1,2.0,75.1,2.0,72.1,2.0,71.1,2.0,70.1,2.0,74.0,2.0,73.0,2.0,2490.0,2.0,6299.0,1.0,6300.2] || -> . % 2.43/2.65 6357[7:Spt:6356.0,389.0,6255.0] || totalorderP(skc7)* -> . % 2.43/2.65 6358[7:Spt:6356.0,389.1] || -> equal(app(app(skf57(skc7),cons(skf55(skc7),skf58(skc7))),cons(skf56(skc7),skf59(skc7))),skc7)**. % 2.43/2.65 6376[8:Spt:95.0] || neq(skc7,nil)* -> . % 2.43/2.65 6378[8:Res:106.2,6376.0] ssList(nil) ssList(skc7) || -> equal(skc7,nil)**. % 2.43/2.65 6380[8:SSi:6378.1,6378.0,3.0,1912.0,1908.0,6250.0,14.0,13.0,10.0,9.0,8.0,12.0,11.0,7.0] || -> equal(skc7,nil)**. % 2.43/2.65 6381[8:MRR:6380.0,1101.0] || -> . % 2.43/2.65 6382[8:Spt:6381.0,95.0,6376.0] || -> neq(skc7,nil)*. % 2.43/2.65 6383[8:Spt:6381.0,95.1] || -> equal(app(cons(skc8,nil),skc9),skc7)**. % 2.43/2.65 6384[8:MRR:2921.0,6382.0] || -> equal(hd(skc7),skc8)**. % 2.43/2.65 6387[8:Rew:6384.0,2929.0] || -> equal(cons(skc8,skc9),skc7)**. % 2.43/2.65 6397[8:MRR:96.0,6382.0] || -> equal(app(skc9,cons(skc8,nil)),skc6)**. % 2.43/2.65 6418[9:Spt:4946.1] || -> equal(skc9,nil)**. % 2.43/2.65 6432[9:Rew:6418.0,6387.0] || -> equal(cons(skc8,nil),skc7)**. % 2.43/2.65 6433[9:Rew:6418.0,6397.0] || -> equal(app(nil,cons(skc8,nil)),skc6)**. % 2.43/2.65 6439[9:Rew:6432.0,6433.0] || -> equal(app(nil,skc7),skc6)**. % 2.43/2.65 6440[9:Rew:449.0,6439.0] || -> equal(skc7,skc6)**. % 2.43/2.65 6441[9:MRR:6440.0,6166.0] || -> . % 2.43/2.65 6473[9:Spt:6441.0,4946.1,6418.0] || equal(skc9,nil)** -> . % 2.43/2.65 6474[9:Spt:6441.0,4946.0] || -> totalorderedP(skc9)*. % 2.43/2.65 6475[9:MRR:2994.1,6473.0] || -> strictorderedP(skc9)*. % 2.43/2.65 6502[8:SpL:6397.0,141.2] ssList(skc9) ssList(cons(skc8,nil)) || equal(skc6,skc6) equal(app(cons(skc8,nil),skc9),skc7)** -> . % 2.43/2.65 6508[8:Obv:6502.2] ssList(skc9) ssList(cons(skc8,nil)) || equal(app(cons(skc8,nil),skc9),skc7)** -> . % 2.43/2.65 6509[8:Rew:6383.0,6508.2] ssList(skc9) ssList(cons(skc8,nil)) || equal(skc7,skc7)* -> . % 2.43/2.65 6510[8:Obv:6509.2] ssList(skc9) ssList(cons(skc8,nil)) || -> . % 2.43/2.65 6511[9:SSi:6510.1,6510.0,87.0,2.0,14.0,13.0,10.1,9.0,8.1,12.0,11.1,7.0,76.1,2.0,75.1,2.0,72.1,2.0,71.1,2.0,70.1,2.0,74.0,2.0,73.0,2.0,2490.0,2.0,6474.0,1.0,6475.2] || -> . % 2.43/2.65 6512[6:Spt:6511.0,390.0,6250.0] || strictorderP(skc7)* -> . % 2.43/2.65 6513[6:Spt:6511.0,390.1] || -> equal(app(app(skf62(skc7),cons(skf60(skc7),skf63(skc7))),cons(skf61(skc7),skf64(skc7))),skc7)**. % 2.43/2.65 6530[7:Spt:389.0] || -> totalorderP(skc7)*. % 2.43/2.65 6532[8:Spt:2994.1] || -> equal(skc9,nil)**. % 2.43/2.65 6546[8:Rew:6532.0,2905.1] || neq(skc7,nil) -> equal(cons(skc8,nil),skc7)**. % 2.43/2.65 6547[8:Rew:6532.0,96.1] || neq(skc7,nil) -> equal(app(nil,cons(skc8,nil)),skc6)**. % 2.43/2.65 6555[8:Rew:6546.1,6547.1] || neq(skc7,nil) -> equal(app(nil,skc7),skc6)**. % 2.43/2.65 6556[8:Rew:449.0,6555.1] || neq(skc7,nil)* -> equal(skc7,skc6). % 2.43/2.65 6557[8:MRR:6556.1,6166.0] || neq(skc7,nil)* -> . % 2.43/2.65 6565[8:Res:106.2,6557.0] ssList(nil) ssList(skc7) || -> equal(skc7,nil)**. % 2.43/2.65 6567[8:SSi:6565.1,6565.0,3.0,1912.0,1908.0,6530.0,14.0,13.0,10.0,9.0,8.0,12.0,11.0,7.0] || -> equal(skc7,nil)**. % 2.43/2.65 6568[8:MRR:6567.0,1101.0] || -> . % 2.43/2.65 6569[8:Spt:6568.0,2994.1,6532.0] || equal(skc9,nil)** -> . % 2.43/2.65 6570[8:Spt:6568.0,2994.0] || -> strictorderedP(skc9)*. % 2.43/2.65 6571[8:MRR:4946.1,6569.0] || -> totalorderedP(skc9)*. % 2.43/2.65 6591[9:Spt:95.0] || neq(skc7,nil)* -> . % 2.43/2.65 6593[9:Res:106.2,6591.0] ssList(nil) ssList(skc7) || -> equal(skc7,nil)**. % 2.43/2.65 6595[9:SSi:6593.1,6593.0,3.0,1912.0,1908.0,6530.0,14.0,13.0,10.0,9.0,8.0,12.0,11.0,7.0] || -> equal(skc7,nil)**. % 2.43/2.65 6596[9:MRR:6595.0,1101.0] || -> . % 2.43/2.65 6597[9:Spt:6596.0,95.0,6591.0] || -> neq(skc7,nil)*. % 2.43/2.65 6598[9:Spt:6596.0,95.1] || -> equal(app(cons(skc8,nil),skc9),skc7)**. % 2.43/2.65 6612[9:MRR:96.0,6597.0] || -> equal(app(skc9,cons(skc8,nil)),skc6)**. % 2.43/2.65 6646[9:SpL:6612.0,141.2] ssList(skc9) ssList(cons(skc8,nil)) || equal(skc6,skc6) equal(app(cons(skc8,nil),skc9),skc7)** -> . % 2.43/2.65 6652[9:Obv:6646.2] ssList(skc9) ssList(cons(skc8,nil)) || equal(app(cons(skc8,nil),skc9),skc7)** -> . % 2.43/2.65 6653[9:Rew:6598.0,6652.2] ssList(skc9) ssList(cons(skc8,nil)) || equal(skc7,skc7)* -> . % 2.43/2.65 6654[9:Obv:6653.2] ssList(skc9) ssList(cons(skc8,nil)) || -> . % 2.43/2.65 6655[9:SSi:6654.1,6654.0,87.0,2.0,14.0,13.0,10.1,9.0,8.1,12.0,11.1,7.0,76.1,2.0,75.1,2.0,72.1,2.0,71.1,2.0,70.1,2.0,74.0,2.0,73.0,2.0,2490.0,2.0,6570.0,1.0,6571.2] || -> . % 2.43/2.65 6656[7:Spt:6655.0,389.0,6530.0] || totalorderP(skc7)* -> . % 2.43/2.65 6657[7:Spt:6655.0,389.1] || -> equal(app(app(skf57(skc7),cons(skf55(skc7),skf58(skc7))),cons(skf56(skc7),skf59(skc7))),skc7)**. % 2.43/2.65 6673[8:Spt:4946.1] || -> equal(skc9,nil)**. % 2.43/2.65 6687[8:Rew:6673.0,2905.1] || neq(skc7,nil) -> equal(cons(skc8,nil),skc7)**. % 2.43/2.65 6688[8:Rew:6673.0,96.1] || neq(skc7,nil) -> equal(app(nil,cons(skc8,nil)),skc6)**. % 2.43/2.65 6696[8:Rew:6687.1,6688.1] || neq(skc7,nil) -> equal(app(nil,skc7),skc6)**. % 2.43/2.65 6697[8:Rew:449.0,6696.1] || neq(skc7,nil)* -> equal(skc7,skc6). % 2.43/2.65 6698[8:MRR:6697.1,6166.0] || neq(skc7,nil)* -> . % 2.43/2.65 6706[8:Res:106.2,6698.0] ssList(nil) ssList(skc7) || -> equal(skc7,nil)**. % 2.43/2.65 6708[8:SSi:6706.1,6706.0,3.0,1912.0,1908.0,14.0,13.0,10.0,9.0,8.0,12.0,11.0,7.0] || -> equal(skc7,nil)**. % 2.43/2.65 6709[8:MRR:6708.0,1101.0] || -> . % 2.43/2.65 6710[8:Spt:6709.0,4946.1,6673.0] || equal(skc9,nil)** -> . % 2.43/2.65 6711[8:Spt:6709.0,4946.0] || -> totalorderedP(skc9)*. % 2.43/2.65 6712[8:MRR:2994.1,6710.0] || -> strictorderedP(skc9)*. % 2.43/2.65 6729[1:SpR:2929.0,123.3] ssList(skc9) ssItem(hd(skc7)) || equal(skc9,nil) -> strictorderedP(skc7)*. % 2.43/2.65 6735[9:Spt:95.0] || neq(skc7,nil)* -> . % 2.43/2.65 6737[9:Res:106.2,6735.0] ssList(nil) ssList(skc7) || -> equal(skc7,nil)**. % 2.43/2.65 6739[9:SSi:6737.1,6737.0,3.0,1912.0,1908.0,14.0,13.0,10.0,9.0,8.0,12.0,11.0,7.0] || -> equal(skc7,nil)**. % 2.43/2.65 6740[9:MRR:6739.0,1101.0] || -> . % 2.43/2.65 6741[9:Spt:6740.0,95.0,6735.0] || -> neq(skc7,nil)*. % 2.43/2.65 6742[9:Spt:6740.0,95.1] || -> equal(app(cons(skc8,nil),skc9),skc7)**. % 2.43/2.65 6757[9:MRR:96.0,6741.0] || -> equal(app(skc9,cons(skc8,nil)),skc6)**. % 2.43/2.65 6791[9:SpL:6757.0,141.2] ssList(skc9) ssList(cons(skc8,nil)) || equal(skc6,skc6) equal(app(cons(skc8,nil),skc9),skc7)** -> . % 2.43/2.65 6797[9:Obv:6791.2] ssList(skc9) ssList(cons(skc8,nil)) || equal(app(cons(skc8,nil),skc9),skc7)** -> . % 2.43/2.65 6798[9:Rew:6742.0,6797.2] ssList(skc9) ssList(cons(skc8,nil)) || equal(skc7,skc7)* -> . % 2.43/2.65 6799[9:Obv:6798.2] ssList(skc9) ssList(cons(skc8,nil)) || -> . % 2.43/2.65 6800[9:SSi:6799.1,6799.0,87.0,2.0,14.0,13.0,10.1,9.0,8.1,12.0,11.1,7.0,76.1,2.0,75.1,2.0,72.1,2.0,71.1,2.0,70.1,2.0,74.0,2.0,73.0,2.0,2490.0,2.0,6711.0,1.0,6712.2] || -> . % 2.43/2.65 6801[3:Spt:6800.0,392.0,1912.0] || strictorderedP(skc7)* -> . % 2.43/2.65 6802[3:Spt:6800.0,392.1] || -> equal(app(app(skf72(skc7),cons(skf70(skc7),skf73(skc7))),cons(skf71(skc7),skf74(skc7))),skc7)**. % 2.43/2.65 6808[1:SSi:6729.0,1.0] ssItem(hd(skc7)) || equal(skc9,nil) -> strictorderedP(skc7)*. % 2.43/2.65 6809[3:MRR:6808.0,6808.2,1104.0,6801.0] || equal(skc9,nil)** -> . % 2.43/2.65 6810[3:MRR:4946.1,6809.0] || -> totalorderedP(skc9)*. % 2.43/2.65 6844[4:Spt:436.0] || -> cyclefreeP(skc7)*. % 2.43/2.65 6847[5:Spt:389.0] || -> totalorderP(skc7)*. % 2.43/2.65 6848[6:Spt:96.0] || neq(skc7,nil)* -> . % 2.43/2.65 6850[6:Res:106.2,6848.0] ssList(nil) ssList(skc7) || -> equal(skc7,nil)**. % 2.43/2.65 6852[6:SSi:6850.1,6850.0,3.0,1908.0,6844.0,6847.0,14.0,13.0,10.0,9.0,8.0,12.0,11.0,7.0] || -> equal(skc7,nil)**. % 2.43/2.65 6853[6:MRR:6852.0,1101.0] || -> . % 2.43/2.65 6854[6:Spt:6853.0,96.0,6848.0] || -> neq(skc7,nil)*. % 2.43/2.65 6855[6:Spt:6853.0,96.1] || -> equal(app(skc9,cons(skc8,nil)),skc6)**. % 2.43/2.65 6867[6:MRR:95.0,6854.0] || -> equal(app(cons(skc8,nil),skc9),skc7)**. % 2.43/2.65 6871[6:SpL:6855.0,141.2] ssList(skc9) ssList(cons(skc8,nil)) || equal(skc6,skc6) equal(app(cons(skc8,nil),skc9),skc7)** -> . % 2.43/2.65 6877[6:Obv:6871.2] ssList(skc9) ssList(cons(skc8,nil)) || equal(app(cons(skc8,nil),skc9),skc7)** -> . % 2.43/2.65 6878[6:Rew:6867.0,6877.2] ssList(skc9) ssList(cons(skc8,nil)) || equal(skc7,skc7)* -> . % 2.43/2.65 6879[6:Obv:6878.2] ssList(skc9) ssList(cons(skc8,nil)) || -> . % 2.43/2.65 6880[6:SSi:6879.1,6879.0,87.0,2.0,14.0,13.1,10.0,9.1,8.0,12.1,11.0,7.1,76.0,2.1,75.0,2.1,72.0,2.1,71.0,2.1,70.0,2.0,74.0,2.0,73.0,2.0,2490.0,2.0,1.0,6810.2] || -> . % 2.43/2.65 6881[5:Spt:6880.0,389.0,6847.0] || totalorderP(skc7)* -> . % 2.43/2.65 6882[5:Spt:6880.0,389.1] || -> equal(app(app(skf57(skc7),cons(skf55(skc7),skf58(skc7))),cons(skf56(skc7),skf59(skc7))),skc7)**. % 2.43/2.65 6895[6:Spt:390.0] || -> strictorderP(skc7)*. % 2.43/2.65 6900[7:Spt:95.0] || neq(skc7,nil)* -> . % 2.43/2.65 6902[7:Res:106.2,6900.0] ssList(nil) ssList(skc7) || -> equal(skc7,nil)**. % 2.43/2.65 6904[7:SSi:6902.1,6902.0,3.0,1908.0,6844.0,6895.0,14.0,13.0,10.0,9.0,8.0,12.0,11.0,7.0] || -> equal(skc7,nil)**. % 2.43/2.65 6905[7:MRR:6904.0,1101.0] || -> . % 2.43/2.65 6906[7:Spt:6905.0,95.0,6900.0] || -> neq(skc7,nil)*. % 2.43/2.65 6907[7:Spt:6905.0,95.1] || -> equal(app(cons(skc8,nil),skc9),skc7)**. % 2.43/2.65 6920[7:MRR:96.0,6906.0] || -> equal(app(skc9,cons(skc8,nil)),skc6)**. % 2.43/2.65 6953[7:SpL:6920.0,141.2] ssList(skc9) ssList(cons(skc8,nil)) || equal(skc6,skc6) equal(app(cons(skc8,nil),skc9),skc7)** -> . % 2.43/2.65 6959[7:Obv:6953.2] ssList(skc9) ssList(cons(skc8,nil)) || equal(app(cons(skc8,nil),skc9),skc7)** -> . % 2.43/2.65 6960[7:Rew:6907.0,6959.2] ssList(skc9) ssList(cons(skc8,nil)) || equal(skc7,skc7)* -> . % 2.43/2.65 6961[7:Obv:6960.2] ssList(skc9) ssList(cons(skc8,nil)) || -> . % 2.43/2.65 6962[7:SSi:6961.1,6961.0,87.0,2.0,14.0,13.1,10.0,9.1,8.0,12.1,11.0,7.1,76.0,2.1,75.0,2.1,72.0,2.1,71.0,2.1,70.0,2.0,74.0,2.0,73.0,2.0,2490.0,2.0,1.0,6810.2] || -> . % 2.43/2.65 6963[6:Spt:6962.0,390.0,6895.0] || strictorderP(skc7)* -> . % 2.43/2.65 6964[6:Spt:6962.0,390.1] || -> equal(app(app(skf62(skc7),cons(skf60(skc7),skf63(skc7))),cons(skf61(skc7),skf64(skc7))),skc7)**. % 2.43/2.65 6992[7:Spt:96.0] || neq(skc7,nil)* -> . % 2.43/2.65 6994[7:Res:106.2,6992.0] ssList(nil) ssList(skc7) || -> equal(skc7,nil)**. % 2.43/2.65 6996[7:SSi:6994.1,6994.0,3.0,1908.0,6844.0,14.0,13.0,10.0,9.0,8.0,12.0,11.0,7.0] || -> equal(skc7,nil)**. % 2.43/2.65 6997[7:MRR:6996.0,1101.0] || -> . % 2.43/2.65 6998[7:Spt:6997.0,96.0,6992.0] || -> neq(skc7,nil)*. % 2.43/2.65 6999[7:Spt:6997.0,96.1] || -> equal(app(skc9,cons(skc8,nil)),skc6)**. % 2.43/2.65 7014[7:MRR:95.0,6998.0] || -> equal(app(cons(skc8,nil),skc9),skc7)**. % 2.43/2.65 7018[7:SpL:6999.0,141.2] ssList(skc9) ssList(cons(skc8,nil)) || equal(skc6,skc6) equal(app(cons(skc8,nil),skc9),skc7)** -> . % 2.43/2.65 7024[7:Obv:7018.2] ssList(skc9) ssList(cons(skc8,nil)) || equal(app(cons(skc8,nil),skc9),skc7)** -> . % 2.43/2.65 7025[7:Rew:7014.0,7024.2] ssList(skc9) ssList(cons(skc8,nil)) || equal(skc7,skc7)* -> . % 2.43/2.65 7026[7:Obv:7025.2] ssList(skc9) ssList(cons(skc8,nil)) || -> . % 2.43/2.65 7027[7:SSi:7026.1,7026.0,87.0,2.0,14.0,13.1,10.0,9.1,8.0,12.1,11.0,7.1,76.0,2.1,75.0,2.1,72.0,2.1,71.0,2.1,70.0,2.0,74.0,2.0,73.0,2.0,2490.0,2.0,1.0,6810.2] || -> . % 2.43/2.65 7028[4:Spt:7027.0,436.0,6844.0] || cyclefreeP(skc7)* -> . % 2.43/2.65 7029[4:Spt:7027.0,436.1] || -> leq(skf51(skc7),skf50(skc7))*. % 2.43/2.65 7042[5:Spt:390.0] || -> strictorderP(skc7)*. % 2.43/2.65 7050[6:Spt:389.0] || -> totalorderP(skc7)*. % 2.43/2.65 7054[7:Spt:95.0] || neq(skc7,nil)* -> . % 2.43/2.65 7056[7:Res:106.2,7054.0] ssList(nil) ssList(skc7) || -> equal(skc7,nil)**. % 2.43/2.65 7058[7:SSi:7056.1,7056.0,3.0,1908.0,7042.0,7050.0,14.0,13.0,10.0,9.0,8.0,12.0,11.0,7.0] || -> equal(skc7,nil)**. % 2.43/2.65 7059[7:MRR:7058.0,1101.0] || -> . % 2.43/2.65 7060[7:Spt:7059.0,95.0,7054.0] || -> neq(skc7,nil)*. % 2.43/2.65 7061[7:Spt:7059.0,95.1] || -> equal(app(cons(skc8,nil),skc9),skc7)**. % 2.43/2.65 7074[7:MRR:96.0,7060.0] || -> equal(app(skc9,cons(skc8,nil)),skc6)**. % 2.43/2.65 7099[7:SpL:7074.0,141.2] ssList(skc9) ssList(cons(skc8,nil)) || equal(skc6,skc6) equal(app(cons(skc8,nil),skc9),skc7)** -> . % 2.43/2.65 7105[7:Obv:7099.2] ssList(skc9) ssList(cons(skc8,nil)) || equal(app(cons(skc8,nil),skc9),skc7)** -> . % 2.43/2.65 7106[7:Rew:7061.0,7105.2] ssList(skc9) ssList(cons(skc8,nil)) || equal(skc7,skc7)* -> . % 2.43/2.65 7107[7:Obv:7106.2] ssList(skc9) ssList(cons(skc8,nil)) || -> . % 2.43/2.65 7108[7:SSi:7107.1,7107.0,87.0,2.0,14.0,13.1,10.0,9.1,8.0,12.1,11.0,7.1,76.0,2.1,75.0,2.1,72.0,2.1,71.0,2.1,70.0,2.0,74.0,2.0,73.0,2.0,2490.0,2.0,1.0,6810.2] || -> . % 2.43/2.65 7109[6:Spt:7108.0,389.0,7050.0] || totalorderP(skc7)* -> . % 2.43/2.65 7110[6:Spt:7108.0,389.1] || -> equal(app(app(skf57(skc7),cons(skf55(skc7),skf58(skc7))),cons(skf56(skc7),skf59(skc7))),skc7)**. % 2.43/2.65 7129[1:SpR:2929.0,122.3] ssList(skc9) ssItem(hd(skc7)) || equal(skc9,nil) -> totalorderedP(skc7)*. % 2.43/2.65 7134[7:Spt:96.0] || neq(skc7,nil)* -> . % 2.43/2.65 7136[7:Res:106.2,7134.0] ssList(nil) ssList(skc7) || -> equal(skc7,nil)**. % 2.43/2.65 7138[7:SSi:7136.1,7136.0,3.0,1908.0,7042.0,14.0,13.0,10.0,9.0,8.0,12.0,11.0,7.0] || -> equal(skc7,nil)**. % 2.43/2.65 7139[7:MRR:7138.0,1101.0] || -> . % 2.43/2.65 7140[7:Spt:7139.0,96.0,7134.0] || -> neq(skc7,nil)*. % 2.43/2.65 7141[7:Spt:7139.0,96.1] || -> equal(app(skc9,cons(skc8,nil)),skc6)**. % 2.43/2.65 7155[7:MRR:95.0,7140.0] || -> equal(app(cons(skc8,nil),skc9),skc7)**. % 2.43/2.65 7159[7:SpL:7141.0,141.2] ssList(skc9) ssList(cons(skc8,nil)) || equal(skc6,skc6) equal(app(cons(skc8,nil),skc9),skc7)** -> . % 2.43/2.65 7165[7:Obv:7159.2] ssList(skc9) ssList(cons(skc8,nil)) || equal(app(cons(skc8,nil),skc9),skc7)** -> . % 2.43/2.65 7166[7:Rew:7155.0,7165.2] ssList(skc9) ssList(cons(skc8,nil)) || equal(skc7,skc7)* -> . % 2.43/2.65 7167[7:Obv:7166.2] ssList(skc9) ssList(cons(skc8,nil)) || -> . % 2.43/2.65 7168[7:SSi:7167.1,7167.0,87.0,2.0,14.0,13.1,10.0,9.1,8.0,12.1,11.0,7.1,76.0,2.1,75.0,2.1,72.0,2.1,71.0,2.1,70.0,2.0,74.0,2.0,73.0,2.0,2490.0,2.0,1.0,6810.2] || -> . % 2.43/2.65 7169[5:Spt:7168.0,390.0,7042.0] || strictorderP(skc7)* -> . % 2.43/2.65 7170[5:Spt:7168.0,390.1] || -> equal(app(app(skf62(skc7),cons(skf60(skc7),skf63(skc7))),cons(skf61(skc7),skf64(skc7))),skc7)**. % 2.43/2.65 7180[6:Spt:389.0] || -> totalorderP(skc7)*. % 2.43/2.65 7197[7:Spt:95.0] || neq(skc7,nil)* -> . % 2.43/2.65 7199[7:Res:106.2,7197.0] ssList(nil) ssList(skc7) || -> equal(skc7,nil)**. % 2.43/2.65 7201[7:SSi:7199.1,7199.0,3.0,1908.0,7180.0,14.0,13.0,10.0,9.0,8.0,12.0,11.0,7.0] || -> equal(skc7,nil)**. % 2.43/2.65 7202[7:MRR:7201.0,1101.0] || -> . % 2.43/2.65 7203[7:Spt:7202.0,95.0,7197.0] || -> neq(skc7,nil)*. % 2.43/2.65 7204[7:Spt:7202.0,95.1] || -> equal(app(cons(skc8,nil),skc9),skc7)**. % 2.43/2.65 7218[7:MRR:96.0,7203.0] || -> equal(app(skc9,cons(skc8,nil)),skc6)**. % 2.43/2.65 7252[7:SpL:7218.0,141.2] ssList(skc9) ssList(cons(skc8,nil)) || equal(skc6,skc6) equal(app(cons(skc8,nil),skc9),skc7)** -> . % 2.43/2.65 7258[7:Obv:7252.2] ssList(skc9) ssList(cons(skc8,nil)) || equal(app(cons(skc8,nil),skc9),skc7)** -> . % 2.43/2.65 7259[7:Rew:7204.0,7258.2] ssList(skc9) ssList(cons(skc8,nil)) || equal(skc7,skc7)* -> . % 2.43/2.65 7260[7:Obv:7259.2] ssList(skc9) ssList(cons(skc8,nil)) || -> . % 2.43/2.65 7261[7:SSi:7260.1,7260.0,87.0,2.0,14.0,13.1,10.0,9.1,8.0,12.1,11.0,7.1,76.0,2.1,75.0,2.1,72.0,2.1,71.0,2.1,70.0,2.0,74.0,2.0,73.0,2.0,2490.0,2.0,1.0,6810.2] || -> . % 2.43/2.65 7262[6:Spt:7261.0,389.0,7180.0] || totalorderP(skc7)* -> . % 2.43/2.65 7263[6:Spt:7261.0,389.1] || -> equal(app(app(skf57(skc7),cons(skf55(skc7),skf58(skc7))),cons(skf56(skc7),skf59(skc7))),skc7)**. % 2.43/2.65 7281[7:Spt:96.0] || neq(skc7,nil)* -> . % 2.43/2.65 7283[7:Res:106.2,7281.0] ssList(nil) ssList(skc7) || -> equal(skc7,nil)**. % 2.43/2.65 7285[7:SSi:7283.1,7283.0,3.0,1908.0,14.0,13.0,10.0,9.0,8.0,12.0,11.0,7.0] || -> equal(skc7,nil)**. % 2.43/2.65 7286[7:MRR:7285.0,1101.0] || -> . % 2.43/2.65 7287[7:Spt:7286.0,96.0,7281.0] || -> neq(skc7,nil)*. % 2.43/2.65 7288[7:Spt:7286.0,96.1] || -> equal(app(skc9,cons(skc8,nil)),skc6)**. % 2.43/2.65 7303[7:MRR:95.0,7287.0] || -> equal(app(cons(skc8,nil),skc9),skc7)**. % 2.43/2.65 7307[7:SpL:7288.0,141.2] ssList(skc9) ssList(cons(skc8,nil)) || equal(skc6,skc6) equal(app(cons(skc8,nil),skc9),skc7)** -> . % 2.43/2.65 7313[7:Obv:7307.2] ssList(skc9) ssList(cons(skc8,nil)) || equal(app(cons(skc8,nil),skc9),skc7)** -> . % 2.43/2.65 7314[7:Rew:7303.0,7313.2] ssList(skc9) ssList(cons(skc8,nil)) || equal(skc7,skc7)* -> . % 2.43/2.65 7315[7:Obv:7314.2] ssList(skc9) ssList(cons(skc8,nil)) || -> . % 2.43/2.65 7316[7:SSi:7315.1,7315.0,87.0,2.0,14.0,13.1,10.0,9.1,8.0,12.1,11.0,7.1,76.0,2.1,75.0,2.1,72.0,2.1,71.0,2.1,70.0,2.0,74.0,2.0,73.0,2.0,2490.0,2.0,1.0,6810.2] || -> . % 2.43/2.65 7317[2:Spt:7316.0,391.0,1908.0] || totalorderedP(skc7)* -> . % 2.43/2.65 7318[2:Spt:7316.0,391.1] || -> equal(app(app(skf67(skc7),cons(skf65(skc7),skf68(skc7))),cons(skf66(skc7),skf69(skc7))),skc7)**. % 2.43/2.65 7326[1:SSi:7129.0,1.0] ssItem(hd(skc7)) || equal(skc9,nil) -> totalorderedP(skc7)*. % 2.43/2.65 7327[2:MRR:7326.0,7326.2,1104.0,7317.0] || equal(skc9,nil)** -> . % 2.43/2.65 7328[2:MRR:2993.2,7327.0] || strictorderedP(skc7) -> strictorderedP(skc9)*. % 2.43/2.65 7361[3:Spt:392.0] || -> strictorderedP(skc7)*. % 2.43/2.65 7363[3:MRR:7328.0,7361.0] || -> strictorderedP(skc9)*. % 2.43/2.65 7365[4:Spt:437.0] || -> cyclefreeP(skc7)*. % 2.43/2.65 7370[5:Spt:95.0] || neq(skc7,nil)* -> . % 2.43/2.65 7372[5:Res:106.2,7370.0] ssList(nil) ssList(skc7) || -> equal(skc7,nil)**. % 2.43/2.65 7374[5:SSi:7372.1,7372.0,3.0,7361.0,7365.0,14.0,13.0,10.0,9.0,8.0,12.0,11.0,7.0] || -> equal(skc7,nil)**. % 2.43/2.65 7375[5:MRR:7374.0,1101.0] || -> . % 2.43/2.65 7376[5:Spt:7375.0,95.0,7370.0] || -> neq(skc7,nil)*. % 2.43/2.65 7377[5:Spt:7375.0,95.1] || -> equal(app(cons(skc8,nil),skc9),skc7)**. % 2.43/2.65 7389[5:MRR:96.0,7376.0] || -> equal(app(skc9,cons(skc8,nil)),skc6)**. % 2.43/2.65 7418[5:SpL:7389.0,141.2] ssList(skc9) ssList(cons(skc8,nil)) || equal(skc6,skc6) equal(app(cons(skc8,nil),skc9),skc7)** -> . % 2.43/2.65 7424[5:Obv:7418.2] ssList(skc9) ssList(cons(skc8,nil)) || equal(app(cons(skc8,nil),skc9),skc7)** -> . % 2.43/2.65 7425[5:Rew:7377.0,7424.2] ssList(skc9) ssList(cons(skc8,nil)) || equal(skc7,skc7)* -> . % 2.43/2.65 7426[5:Obv:7425.2] ssList(skc9) ssList(cons(skc8,nil)) || -> . % 2.43/2.65 7427[5:SSi:7426.1,7426.0,87.0,2.0,14.0,13.1,10.0,9.1,8.0,12.1,11.0,7.1,76.0,2.1,75.0,2.1,72.0,2.1,71.0,2.1,70.0,2.0,74.0,2.0,73.0,2.0,2490.0,2.0,1.0,7363.2] || -> . % 2.43/2.65 7428[4:Spt:7427.0,437.0,7365.0] || cyclefreeP(skc7)* -> . % 2.43/2.65 7429[4:Spt:7427.0,437.1] || -> leq(skf50(skc7),skf51(skc7))*. % 2.43/2.65 7441[5:Spt:390.0] || -> strictorderP(skc7)*. % 2.43/2.65 7443[6:Spt:389.0] || -> totalorderP(skc7)*. % 2.43/2.65 7451[7:Spt:96.0] || neq(skc7,nil)* -> . % 2.43/2.65 7453[7:Res:106.2,7451.0] ssList(nil) ssList(skc7) || -> equal(skc7,nil)**. % 2.43/2.65 7455[7:SSi:7453.1,7453.0,3.0,7361.0,7441.0,7443.0,14.0,13.0,10.0,9.0,8.0,12.0,11.0,7.0] || -> equal(skc7,nil)**. % 2.43/2.65 7456[7:MRR:7455.0,1101.0] || -> . % 2.43/2.65 7457[7:Spt:7456.0,96.0,7451.0] || -> neq(skc7,nil)*. % 2.43/2.65 7458[7:Spt:7456.0,96.1] || -> equal(app(skc9,cons(skc8,nil)),skc6)**. % 2.43/2.65 7470[7:MRR:95.0,7457.0] || -> equal(app(cons(skc8,nil),skc9),skc7)**. % 2.43/2.65 7474[7:SpL:7458.0,141.2] ssList(skc9) ssList(cons(skc8,nil)) || equal(skc6,skc6) equal(app(cons(skc8,nil),skc9),skc7)** -> . % 2.43/2.65 7480[7:Obv:7474.2] ssList(skc9) ssList(cons(skc8,nil)) || equal(app(cons(skc8,nil),skc9),skc7)** -> . % 2.43/2.65 7481[7:Rew:7470.0,7480.2] ssList(skc9) ssList(cons(skc8,nil)) || equal(skc7,skc7)* -> . % 2.43/2.65 7482[7:Obv:7481.2] ssList(skc9) ssList(cons(skc8,nil)) || -> . % 2.43/2.65 7483[7:SSi:7482.1,7482.0,87.0,2.0,14.0,13.1,10.0,9.1,8.0,12.1,11.0,7.1,76.0,2.1,75.0,2.1,72.0,2.1,71.0,2.1,70.0,2.0,74.0,2.0,73.0,2.0,2490.0,2.0,1.0,7363.2] || -> . % 2.43/2.65 7484[6:Spt:7483.0,389.0,7443.0] || totalorderP(skc7)* -> . % 2.43/2.65 7485[6:Spt:7483.0,389.1] || -> equal(app(app(skf57(skc7),cons(skf55(skc7),skf58(skc7))),cons(skf56(skc7),skf59(skc7))),skc7)**. % 2.43/2.65 7511[7:Spt:95.0] || neq(skc7,nil)* -> . % 2.43/2.65 7513[7:Res:106.2,7511.0] ssList(nil) ssList(skc7) || -> equal(skc7,nil)**. % 2.43/2.66 7515[7:SSi:7513.1,7513.0,3.0,7361.0,7441.0,14.0,13.0,10.0,9.0,8.0,12.0,11.0,7.0] || -> equal(skc7,nil)**. % 2.43/2.66 7516[7:MRR:7515.0,1101.0] || -> . % 2.43/2.66 7517[7:Spt:7516.0,95.0,7511.0] || -> neq(skc7,nil)*. % 2.43/2.66 7518[7:Spt:7516.0,95.1] || -> equal(app(cons(skc8,nil),skc9),skc7)**. % 2.43/2.66 7532[7:MRR:96.0,7517.0] || -> equal(app(skc9,cons(skc8,nil)),skc6)**. % 2.43/2.66 7566[7:SpL:7532.0,141.2] ssList(skc9) ssList(cons(skc8,nil)) || equal(skc6,skc6) equal(app(cons(skc8,nil),skc9),skc7)** -> . % 2.43/2.66 7572[7:Obv:7566.2] ssList(skc9) ssList(cons(skc8,nil)) || equal(app(cons(skc8,nil),skc9),skc7)** -> . % 2.43/2.66 7573[7:Rew:7518.0,7572.2] ssList(skc9) ssList(cons(skc8,nil)) || equal(skc7,skc7)* -> . % 2.43/2.66 7574[7:Obv:7573.2] ssList(skc9) ssList(cons(skc8,nil)) || -> . % 2.43/2.66 7575[7:SSi:7574.1,7574.0,87.0,2.0,14.0,13.1,10.0,9.1,8.0,12.1,11.0,7.1,76.0,2.1,75.0,2.1,72.0,2.1,71.0,2.1,70.0,2.0,74.0,2.0,73.0,2.0,2490.0,2.0,1.0,7363.2] || -> . % 2.43/2.66 7576[5:Spt:7575.0,390.0,7441.0] || strictorderP(skc7)* -> . % 2.43/2.66 7577[5:Spt:7575.0,390.1] || -> equal(app(app(skf62(skc7),cons(skf60(skc7),skf63(skc7))),cons(skf61(skc7),skf64(skc7))),skc7)**. % 2.43/2.66 7592[6:Spt:389.0] || -> totalorderP(skc7)*. % 2.43/2.66 7607[7:Spt:96.0] || neq(skc7,nil)* -> . % 2.43/2.66 7609[7:Res:106.2,7607.0] ssList(nil) ssList(skc7) || -> equal(skc7,nil)**. % 2.43/2.66 7611[7:SSi:7609.1,7609.0,3.0,7361.0,7592.0,14.0,13.0,10.0,9.0,8.0,12.0,11.0,7.0] || -> equal(skc7,nil)**. % 2.43/2.66 7612[7:MRR:7611.0,1101.0] || -> . % 2.43/2.66 7613[7:Spt:7612.0,96.0,7607.0] || -> neq(skc7,nil)*. % 2.43/2.66 7614[7:Spt:7612.0,96.1] || -> equal(app(skc9,cons(skc8,nil)),skc6)**. % 2.43/2.66 7628[7:MRR:95.0,7613.0] || -> equal(app(cons(skc8,nil),skc9),skc7)**. % 2.43/2.66 7632[7:SpL:7614.0,141.2] ssList(skc9) ssList(cons(skc8,nil)) || equal(skc6,skc6) equal(app(cons(skc8,nil),skc9),skc7)** -> . % 2.43/2.66 7638[7:Obv:7632.2] ssList(skc9) ssList(cons(skc8,nil)) || equal(app(cons(skc8,nil),skc9),skc7)** -> . % 2.43/2.66 7639[7:Rew:7628.0,7638.2] ssList(skc9) ssList(cons(skc8,nil)) || equal(skc7,skc7)* -> . % 2.43/2.66 7640[7:Obv:7639.2] ssList(skc9) ssList(cons(skc8,nil)) || -> . % 2.43/2.66 7641[7:SSi:7640.1,7640.0,87.0,2.0,14.0,13.1,10.0,9.1,8.0,12.1,11.0,7.1,76.0,2.1,75.0,2.1,72.0,2.1,71.0,2.1,70.0,2.0,74.0,2.0,73.0,2.0,2490.0,2.0,1.0,7363.2] || -> . % 2.43/2.66 7642[6:Spt:7641.0,389.0,7592.0] || totalorderP(skc7)* -> . % 2.43/2.66 7643[6:Spt:7641.0,389.1] || -> equal(app(app(skf57(skc7),cons(skf55(skc7),skf58(skc7))),cons(skf56(skc7),skf59(skc7))),skc7)**. % 2.43/2.66 7659[7:Spt:95.0] || neq(skc7,nil)* -> . % 2.43/2.66 7661[7:Res:106.2,7659.0] ssList(nil) ssList(skc7) || -> equal(skc7,nil)**. % 2.43/2.66 7663[7:SSi:7661.1,7661.0,3.0,7361.0,14.0,13.0,10.0,9.0,8.0,12.0,11.0,7.0] || -> equal(skc7,nil)**. % 2.43/2.66 7664[7:MRR:7663.0,1101.0] || -> . % 2.43/2.66 7665[7:Spt:7664.0,95.0,7659.0] || -> neq(skc7,nil)*. % 2.43/2.66 7666[7:Spt:7664.0,95.1] || -> equal(app(cons(skc8,nil),skc9),skc7)**. % 2.43/2.66 7681[7:MRR:96.0,7665.0] || -> equal(app(skc9,cons(skc8,nil)),skc6)**. % 2.43/2.66 7715[7:SpL:7681.0,141.2] ssList(skc9) ssList(cons(skc8,nil)) || equal(skc6,skc6) equal(app(cons(skc8,nil),skc9),skc7)** -> . % 2.43/2.66 7721[7:Obv:7715.2] ssList(skc9) ssList(cons(skc8,nil)) || equal(app(cons(skc8,nil),skc9),skc7)** -> . % 2.43/2.66 7722[7:Rew:7666.0,7721.2] ssList(skc9) ssList(cons(skc8,nil)) || equal(skc7,skc7)* -> . % 2.43/2.66 7723[7:Obv:7722.2] ssList(skc9) ssList(cons(skc8,nil)) || -> . % 2.43/2.66 7724[7:SSi:7723.1,7723.0,87.0,2.0,14.0,13.1,10.0,9.1,8.0,12.1,11.0,7.1,76.0,2.1,75.0,2.1,72.0,2.1,71.0,2.1,70.0,2.0,74.0,2.0,73.0,2.0,2490.0,2.0,1.0,7363.2] || -> . % 2.43/2.66 7725[3:Spt:7724.0,392.0,7361.0] || strictorderedP(skc7)* -> . % 2.43/2.66 7726[3:Spt:7724.0,392.1] || -> equal(app(app(skf72(skc7),cons(skf70(skc7),skf73(skc7))),cons(skf71(skc7),skf74(skc7))),skc7)**. % 2.43/2.66 7741[4:Spt:436.0] || -> cyclefreeP(skc7)*. % 2.43/2.66 7744[5:Spt:389.0] || -> totalorderP(skc7)*. % 2.43/2.66 7761[6:Spt:96.0] || neq(skc7,nil)* -> . % 2.43/2.66 7763[6:Res:106.2,7761.0] ssList(nil) ssList(skc7) || -> equal(skc7,nil)**. % 2.43/2.66 7765[6:SSi:7763.1,7763.0,3.0,7741.0,7744.0,14.0,13.0,10.0,9.0,8.0,12.0,11.0,7.0] || -> equal(skc7,nil)**. % 2.43/2.66 7766[6:MRR:7765.0,1101.0] || -> . % 2.43/2.66 7767[6:Spt:7766.0,96.0,7761.0] || -> neq(skc7,nil)*. % 2.43/2.66 7768[6:Spt:7766.0,96.1] || -> equal(app(skc9,cons(skc8,nil)),skc6)**. % 2.43/2.66 7781[6:MRR:95.0,7767.0] || -> equal(app(cons(skc8,nil),skc9),skc7)**. % 2.43/2.66 7785[6:SpL:7768.0,141.2] ssList(skc9) ssList(cons(skc8,nil)) || equal(skc6,skc6) equal(app(cons(skc8,nil),skc9),skc7)** -> . % 2.43/2.66 7791[6:Obv:7785.2] ssList(skc9) ssList(cons(skc8,nil)) || equal(app(cons(skc8,nil),skc9),skc7)** -> . % 2.43/2.66 7792[6:Rew:7781.0,7791.2] ssList(skc9) ssList(cons(skc8,nil)) || equal(skc7,skc7)* -> . % 2.43/2.66 7793[6:Obv:7792.2] ssList(skc9) ssList(cons(skc8,nil)) || -> . % 2.43/2.66 7794[6:SSi:7793.1,7793.0,87.0,2.0,14.1,13.0,10.1,9.0,8.1,12.0,11.1,7.0,76.1,2.0,75.1,2.0,72.1,2.0,71.1,2.0,70.0,2.0,74.0,2.0,73.0,2.0,2490.0,2.0,1.2] || -> . % 2.43/2.66 7795[5:Spt:7794.0,389.0,7744.0] || totalorderP(skc7)* -> . % 2.43/2.66 7796[5:Spt:7794.0,389.1] || -> equal(app(app(skf57(skc7),cons(skf55(skc7),skf58(skc7))),cons(skf56(skc7),skf59(skc7))),skc7)**. % 2.43/2.66 7806[6:Spt:390.0] || -> strictorderP(skc7)*. % 2.43/2.66 7816[7:Spt:95.0] || neq(skc7,nil)* -> . % 2.43/2.66 7818[7:Res:106.2,7816.0] ssList(nil) ssList(skc7) || -> equal(skc7,nil)**. % 2.43/2.66 7820[7:SSi:7818.1,7818.0,3.0,7741.0,7806.0,14.0,13.0,10.0,9.0,8.0,12.0,11.0,7.0] || -> equal(skc7,nil)**. % 2.43/2.66 7821[7:MRR:7820.0,1101.0] || -> . % 2.43/2.66 7822[7:Spt:7821.0,95.0,7816.0] || -> neq(skc7,nil)*. % 2.43/2.66 7823[7:Spt:7821.0,95.1] || -> equal(app(cons(skc8,nil),skc9),skc7)**. % 2.43/2.66 7837[7:MRR:96.0,7822.0] || -> equal(app(skc9,cons(skc8,nil)),skc6)**. % 2.43/2.66 7871[7:SpL:7837.0,141.2] ssList(skc9) ssList(cons(skc8,nil)) || equal(skc6,skc6) equal(app(cons(skc8,nil),skc9),skc7)** -> . % 2.43/2.66 7877[7:Obv:7871.2] ssList(skc9) ssList(cons(skc8,nil)) || equal(app(cons(skc8,nil),skc9),skc7)** -> . % 2.43/2.66 7878[7:Rew:7823.0,7877.2] ssList(skc9) ssList(cons(skc8,nil)) || equal(skc7,skc7)* -> . % 2.43/2.66 7879[7:Obv:7878.2] ssList(skc9) ssList(cons(skc8,nil)) || -> . % 2.43/2.66 7880[7:SSi:7879.1,7879.0,87.0,2.0,14.1,13.0,10.1,9.0,8.1,12.0,11.1,7.0,76.1,2.0,75.1,2.0,72.1,2.0,71.1,2.0,70.0,2.0,74.0,2.0,73.0,2.0,2490.0,2.0,1.2] || -> . % 2.43/2.66 7881[6:Spt:7880.0,390.0,7806.0] || strictorderP(skc7)* -> . % 2.43/2.66 7882[6:Spt:7880.0,390.1] || -> equal(app(app(skf62(skc7),cons(skf60(skc7),skf63(skc7))),cons(skf61(skc7),skf64(skc7))),skc7)**. % 2.43/2.66 7899[7:Spt:96.0] || neq(skc7,nil)* -> . % 2.43/2.66 7901[7:Res:106.2,7899.0] ssList(nil) ssList(skc7) || -> equal(skc7,nil)**. % 2.43/2.66 7903[7:SSi:7901.1,7901.0,3.0,7741.0,14.0,13.0,10.0,9.0,8.0,12.0,11.0,7.0] || -> equal(skc7,nil)**. % 2.43/2.66 7904[7:MRR:7903.0,1101.0] || -> . % 2.43/2.66 7905[7:Spt:7904.0,96.0,7899.0] || -> neq(skc7,nil)*. % 2.43/2.66 7906[7:Spt:7904.0,96.1] || -> equal(app(skc9,cons(skc8,nil)),skc6)**. % 2.43/2.66 7921[7:MRR:95.0,7905.0] || -> equal(app(cons(skc8,nil),skc9),skc7)**. % 2.43/2.66 7925[7:SpL:7906.0,141.2] ssList(skc9) ssList(cons(skc8,nil)) || equal(skc6,skc6) equal(app(cons(skc8,nil),skc9),skc7)** -> . % 2.43/2.66 7931[7:Obv:7925.2] ssList(skc9) ssList(cons(skc8,nil)) || equal(app(cons(skc8,nil),skc9),skc7)** -> . % 2.43/2.66 7932[7:Rew:7921.0,7931.2] ssList(skc9) ssList(cons(skc8,nil)) || equal(skc7,skc7)* -> . % 2.43/2.66 7933[7:Obv:7932.2] ssList(skc9) ssList(cons(skc8,nil)) || -> . % 2.43/2.66 7934[7:SSi:7933.1,7933.0,87.0,2.0,14.1,13.0,10.1,9.0,8.1,12.0,11.1,7.0,76.1,2.0,75.1,2.0,72.1,2.0,71.1,2.0,70.0,2.0,74.0,2.0,73.0,2.0,2490.0,2.0,1.2] || -> . % 2.43/2.66 7935[4:Spt:7934.0,436.0,7741.0] || cyclefreeP(skc7)* -> . % 2.43/2.66 7936[4:Spt:7934.0,436.1] || -> leq(skf51(skc7),skf50(skc7))*. % 2.43/2.66 7950[5:Spt:390.0] || -> strictorderP(skc7)*. % 2.43/2.66 7955[6:Spt:389.0] || -> totalorderP(skc7)*. % 2.43/2.66 7960[7:Spt:95.0] || neq(skc7,nil)* -> . % 2.43/2.66 7962[7:Res:106.2,7960.0] ssList(nil) ssList(skc7) || -> equal(skc7,nil)**. % 2.43/2.66 7964[7:SSi:7962.1,7962.0,3.0,7950.0,7955.0,14.0,13.0,10.0,9.0,8.0,12.0,11.0,7.0] || -> equal(skc7,nil)**. % 2.43/2.66 7965[7:MRR:7964.0,1101.0] || -> . % 2.43/2.66 7966[7:Spt:7965.0,95.0,7960.0] || -> neq(skc7,nil)*. % 2.43/2.66 7967[7:Spt:7965.0,95.1] || -> equal(app(cons(skc8,nil),skc9),skc7)**. % 2.43/2.66 7980[7:MRR:96.0,7966.0] || -> equal(app(skc9,cons(skc8,nil)),skc6)**. % 2.43/2.66 8005[7:SpL:7980.0,141.2] ssList(skc9) ssList(cons(skc8,nil)) || equal(skc6,skc6) equal(app(cons(skc8,nil),skc9),skc7)** -> . % 2.43/2.66 8011[7:Obv:8005.2] ssList(skc9) ssList(cons(skc8,nil)) || equal(app(cons(skc8,nil),skc9),skc7)** -> . % 2.43/2.66 8012[7:Rew:7967.0,8011.2] ssList(skc9) ssList(cons(skc8,nil)) || equal(skc7,skc7)* -> . % 2.43/2.66 8013[7:Obv:8012.2] ssList(skc9) ssList(cons(skc8,nil)) || -> . % 2.43/2.66 8014[7:SSi:8013.1,8013.0,87.0,2.0,14.1,13.0,10.1,9.0,8.1,12.0,11.1,7.0,76.1,2.0,75.1,2.0,72.1,2.0,71.1,2.0,70.0,2.0,74.0,2.0,73.0,2.0,2490.0,2.0,1.2] || -> . % 2.54/2.72 8015[6:Spt:8014.0,389.0,7955.0] || totalorderP(skc7)* -> . % 2.54/2.72 8016[6:Spt:8014.0,389.1] || -> equal(app(app(skf57(skc7),cons(skf55(skc7),skf58(skc7))),cons(skf56(skc7),skf59(skc7))),skc7)**. % 2.54/2.72 8040[7:Spt:96.0] || neq(skc7,nil)* -> . % 2.54/2.72 8042[7:Res:106.2,8040.0] ssList(nil) ssList(skc7) || -> equal(skc7,nil)**. % 2.54/2.72 8044[7:SSi:8042.1,8042.0,3.0,7950.0,14.0,13.0,10.0,9.0,8.0,12.0,11.0,7.0] || -> equal(skc7,nil)**. % 2.54/2.72 8045[7:MRR:8044.0,1101.0] || -> . % 2.54/2.72 8046[7:Spt:8045.0,96.0,8040.0] || -> neq(skc7,nil)*. % 2.54/2.72 8047[7:Spt:8045.0,96.1] || -> equal(app(skc9,cons(skc8,nil)),skc6)**. % 2.54/2.72 8061[7:MRR:95.0,8046.0] || -> equal(app(cons(skc8,nil),skc9),skc7)**. % 2.54/2.72 8065[7:SpL:8047.0,141.2] ssList(skc9) ssList(cons(skc8,nil)) || equal(skc6,skc6) equal(app(cons(skc8,nil),skc9),skc7)** -> . % 2.54/2.72 8071[7:Obv:8065.2] ssList(skc9) ssList(cons(skc8,nil)) || equal(app(cons(skc8,nil),skc9),skc7)** -> . % 2.54/2.72 8072[7:Rew:8061.0,8071.2] ssList(skc9) ssList(cons(skc8,nil)) || equal(skc7,skc7)* -> . % 2.54/2.72 8073[7:Obv:8072.2] ssList(skc9) ssList(cons(skc8,nil)) || -> . % 2.54/2.72 8074[7:SSi:8073.1,8073.0,87.0,2.0,14.1,13.0,10.1,9.0,8.1,12.0,11.1,7.0,76.1,2.0,75.1,2.0,72.1,2.0,71.1,2.0,70.0,2.0,74.0,2.0,73.0,2.0,2490.0,2.0,1.2] || -> . % 2.54/2.72 8075[5:Spt:8074.0,390.0,7950.0] || strictorderP(skc7)* -> . % 2.54/2.72 8076[5:Spt:8074.0,390.1] || -> equal(app(app(skf62(skc7),cons(skf60(skc7),skf63(skc7))),cons(skf61(skc7),skf64(skc7))),skc7)**. % 2.54/2.72 8086[6:Spt:389.0] || -> totalorderP(skc7)*. % 2.54/2.72 8102[7:Spt:95.0] || neq(skc7,nil)* -> . % 2.54/2.72 8104[7:Res:106.2,8102.0] ssList(nil) ssList(skc7) || -> equal(skc7,nil)**. % 2.54/2.72 8106[7:SSi:8104.1,8104.0,3.0,8086.0,14.0,13.0,10.0,9.0,8.0,12.0,11.0,7.0] || -> equal(skc7,nil)**. % 2.54/2.72 8107[7:MRR:8106.0,1101.0] || -> . % 2.54/2.72 8108[7:Spt:8107.0,95.0,8102.0] || -> neq(skc7,nil)*. % 2.54/2.72 8109[7:Spt:8107.0,95.1] || -> equal(app(cons(skc8,nil),skc9),skc7)**. % 2.54/2.72 8123[7:MRR:96.0,8108.0] || -> equal(app(skc9,cons(skc8,nil)),skc6)**. % 2.54/2.72 8157[7:SpL:8123.0,141.2] ssList(skc9) ssList(cons(skc8,nil)) || equal(skc6,skc6) equal(app(cons(skc8,nil),skc9),skc7)** -> . % 2.54/2.72 8163[7:Obv:8157.2] ssList(skc9) ssList(cons(skc8,nil)) || equal(app(cons(skc8,nil),skc9),skc7)** -> . % 2.54/2.72 8164[7:Rew:8109.0,8163.2] ssList(skc9) ssList(cons(skc8,nil)) || equal(skc7,skc7)* -> . % 2.54/2.72 8165[7:Obv:8164.2] ssList(skc9) ssList(cons(skc8,nil)) || -> . % 2.54/2.72 8166[7:SSi:8165.1,8165.0,87.0,2.0,14.1,13.0,10.1,9.0,8.1,12.0,11.1,7.0,76.1,2.0,75.1,2.0,72.1,2.0,71.1,2.0,70.0,2.0,74.0,2.0,73.0,2.0,2490.0,2.0,1.2] || -> . % 2.54/2.72 8167[6:Spt:8166.0,389.0,8086.0] || totalorderP(skc7)* -> . % 2.54/2.72 8168[6:Spt:8166.0,389.1] || -> equal(app(app(skf57(skc7),cons(skf55(skc7),skf58(skc7))),cons(skf56(skc7),skf59(skc7))),skc7)**. % 2.54/2.72 8184[7:Spt:96.0] || neq(skc7,nil)* -> . % 2.54/2.72 8186[7:Res:106.2,8184.0] ssList(nil) ssList(skc7) || -> equal(skc7,nil)**. % 2.54/2.72 8188[7:SSi:8186.1,8186.0,3.0,14.0,13.0,10.0,9.0,8.0,12.0,11.0,7.0] || -> equal(skc7,nil)**. % 2.54/2.72 8189[7:MRR:8188.0,1101.0] || -> . % 2.54/2.72 8190[7:Spt:8189.0,96.0,8184.0] || -> neq(skc7,nil)*. % 2.54/2.72 8191[7:Spt:8189.0,96.1] || -> equal(app(skc9,cons(skc8,nil)),skc6)**. % 2.54/2.72 8206[7:MRR:95.0,8190.0] || -> equal(app(cons(skc8,nil),skc9),skc7)**. % 2.54/2.72 8210[7:SpL:8191.0,141.2] ssList(skc9) ssList(cons(skc8,nil)) || equal(skc6,skc6) equal(app(cons(skc8,nil),skc9),skc7)** -> . % 2.54/2.72 8216[7:Obv:8210.2] ssList(skc9) ssList(cons(skc8,nil)) || equal(app(cons(skc8,nil),skc9),skc7)** -> . % 2.54/2.72 8217[7:Rew:8206.0,8216.2] ssList(skc9) ssList(cons(skc8,nil)) || equal(skc7,skc7)* -> . % 2.54/2.72 8218[7:Obv:8217.2] ssList(skc9) ssList(cons(skc8,nil)) || -> . % 2.54/2.72 8219[7:SSi:8218.1,8218.0,87.0,2.0,14.1,13.0,10.1,9.0,8.1,12.0,11.1,7.0,76.1,2.0,75.1,2.0,72.1,2.0,71.1,2.0,70.0,2.0,74.0,2.0,73.0,2.0,2490.0,2.0,1.2] || -> . % 2.54/2.72 % SZS output end Refutation % 2.54/2.72 Formulae used in the proof : co1 ax2 ax17 ax60 ax62 ax64 ax66 ax69 ax72 ax74 ax59 ax61 ax63 ax65 ax68 ax71 ax73 ax28 ax84 ax75 ax8 ax13 ax16 ax15 ax23 ax25 ax78 ax4 ax67 ax70 ax81 ax12 ax11 ax10 ax9 ax77 % 2.54/2.72 %------------------------------------------------------------------------------