%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : SWC387-1 : TPTP v8.1.0. Released v2.4.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n022.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:45 EDT 2022 % Result : Unsatisfiable 1.83s 2.03s % Output : Refutation 1.83s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.13/0.13 % Problem : SWC387-1 : TPTP v8.1.0. Released v2.4.0. % 0.13/0.14 % Command : run_spass %d %s % 0.14/0.35 % Computer : n022.cluster.edu % 0.14/0.35 % Model : x86_64 x86_64 % 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.35 % Memory : 8042.1875MB % 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.35 % CPULimit : 300 % 0.14/0.35 % WCLimit : 600 % 0.14/0.35 % DateTime : Sun Jun 12 21:11:33 EDT 2022 % 0.14/0.35 % CPUTime : % 1.83/2.03 % 1.83/2.03 SPASS V 3.9 % 1.83/2.03 SPASS beiseite: Proof found. % 1.83/2.03 % SZS status Theorem % 1.83/2.03 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 1.83/2.03 SPASS derived 3546 clauses, backtracked 2448 clauses, performed 128 splits and kept 4714 clauses. % 1.83/2.03 SPASS allocated 78486 KBytes. % 1.83/2.03 SPASS spent 0:00:01.67 on the problem. % 1.83/2.03 0:00:00.04 for the input. % 1.83/2.03 0:00:00.00 for the FLOTTER CNF translation. % 1.83/2.03 0:00:00.02 for inferences. % 1.83/2.03 0:00:00.03 for the backtracking. % 1.83/2.03 0:00:01.39 for the reduction. % 1.83/2.03 % 1.83/2.03 % 1.83/2.03 Here is a proof with depth 2, length 480 : % 1.83/2.03 % SZS output start Refutation % 1.83/2.03 1[0:Inp] || -> ssList(sk1)*. % 1.83/2.03 2[0:Inp] || -> ssList(sk2)*. % 1.83/2.03 5[0:Inp] || -> equal(sk4,sk2)**. % 1.83/2.03 6[0:Inp] || -> equal(sk3,sk1)**. % 1.83/2.03 7[0:Inp] ssItem(u) || memberP(sk2,u) equal(cons(u,nil),sk1)** -> . % 1.83/2.03 8[0:Inp] || equal(nil,sk4) -> equal(sk3,nil)**. % 1.83/2.03 9[0:Inp] || equal(nil,sk2)** equal(nil,sk1) -> . % 1.83/2.03 10[0:Inp] || neq(sk4,nil)* -> ssItem(sk5). % 1.83/2.03 11[0:Inp] || neq(sk4,nil) -> equal(cons(sk5,nil),sk3)**. % 1.83/2.03 12[0:Inp] || neq(sk4,nil) -> memberP(sk4,sk5)*. % 1.83/2.03 13[0:Inp] || -> equalelemsP(nil)*. % 1.83/2.03 14[0:Inp] || -> duplicatefreeP(nil)*. % 1.83/2.03 15[0:Inp] || -> strictorderedP(nil)*. % 1.83/2.03 16[0:Inp] || -> totalorderedP(nil)*. % 1.83/2.03 17[0:Inp] || -> strictorderP(nil)*. % 1.83/2.03 18[0:Inp] || -> totalorderP(nil)*. % 1.83/2.03 19[0:Inp] || -> cyclefreeP(nil)*. % 1.83/2.03 20[0:Inp] || -> ssList(nil)*. % 1.83/2.03 84[0:Inp] ssList(u) || -> ssItem(v)* duplicatefreeP(u)*. % 1.83/2.03 99[0:Inp] ssList(u) || -> cyclefreeP(u) leq(skaf50(u),skaf49(u))*. % 1.83/2.03 100[0:Inp] ssList(u) || -> cyclefreeP(u) leq(skaf49(u),skaf50(u))*. % 1.83/2.03 111[0:Inp] ssList(u) ssItem(v) || equal(cons(v,u),u)** -> . % 1.83/2.03 112[0:Inp] ssList(u) ssList(v) || -> equal(u,v) neq(u,v)*. % 1.83/2.03 114[0:Inp] ssItem(u) ssItem(v) || -> equal(u,v) neq(u,v)*. % 1.83/2.03 175[0:Inp] ssList(u) || -> strictorderedP(u) equal(app(app(skaf71(u),cons(skaf69(u),skaf72(u))),cons(skaf70(u),skaf73(u))),u)**. % 1.83/2.03 176[0:Inp] ssList(u) || -> totalorderedP(u) equal(app(app(skaf66(u),cons(skaf64(u),skaf67(u))),cons(skaf65(u),skaf68(u))),u)**. % 1.83/2.03 177[0:Inp] ssList(u) || -> strictorderP(u) equal(app(app(skaf61(u),cons(skaf59(u),skaf62(u))),cons(skaf60(u),skaf63(u))),u)**. % 1.83/2.03 178[0:Inp] ssList(u) || -> totalorderP(u) equal(app(app(skaf56(u),cons(skaf54(u),skaf57(u))),cons(skaf55(u),skaf58(u))),u)**. % 1.83/2.03 189[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). % 1.83/2.03 200[0:Rew:5.0,10.0] || neq(sk2,nil)* -> ssItem(sk5). % 1.83/2.03 201[0:Rew:5.0,12.1,5.0,12.0] || neq(sk2,nil) -> memberP(sk2,sk5)*. % 1.83/2.03 202[0:Rew:6.0,8.1,5.0,8.0] || equal(nil,sk2)** -> equal(nil,sk1). % 1.83/2.03 203[0:Rew:202.1,9.1] || equal(nil,sk2)** equal(sk1,sk1) -> . % 1.83/2.03 204[0:Obv:203.1] || equal(nil,sk2)** -> . % 1.83/2.03 205[0:Rew:6.0,11.1,5.0,11.0] || neq(sk2,nil) -> equal(cons(sk5,nil),sk1)**. % 1.83/2.03 226[0:Res:2.0,178.0] || -> totalorderP(sk2) equal(app(app(skaf56(sk2),cons(skaf54(sk2),skaf57(sk2))),cons(skaf55(sk2),skaf58(sk2))),sk2)**. % 1.83/2.03 227[0:Res:2.0,177.0] || -> strictorderP(sk2) equal(app(app(skaf61(sk2),cons(skaf59(sk2),skaf62(sk2))),cons(skaf60(sk2),skaf63(sk2))),sk2)**. % 1.83/2.03 228[0:Res:2.0,176.0] || -> totalorderedP(sk2) equal(app(app(skaf66(sk2),cons(skaf64(sk2),skaf67(sk2))),cons(skaf65(sk2),skaf68(sk2))),sk2)**. % 1.83/2.03 229[0:Res:2.0,175.0] || -> strictorderedP(sk2) equal(app(app(skaf71(sk2),cons(skaf69(sk2),skaf72(sk2))),cons(skaf70(sk2),skaf73(sk2))),sk2)**. % 1.83/2.03 285[0:Res:2.0,99.0] || -> cyclefreeP(sk2) leq(skaf50(sk2),skaf49(sk2))*. % 1.83/2.03 286[0:Res:2.0,100.0] || -> cyclefreeP(sk2) leq(skaf49(sk2),skaf50(sk2))*. % 1.83/2.03 291[0:Res:2.0,84.0] || -> ssItem(u)* duplicatefreeP(sk2)*. % 1.83/2.03 345[0:Res:2.0,112.1] ssList(u) || -> equal(sk2,u) neq(sk2,u)*. % 1.83/2.03 440[0:Res:1.0,112.0] ssList(u) || -> equal(u,sk1) neq(u,sk1)*. % 1.83/2.03 462[0:Res:1.0,84.0] || -> ssItem(u)* duplicatefreeP(sk1)*. % 1.83/2.03 477[0:Res:1.0,189.1] ssList(u) || equal(hd(u),hd(sk1))* equal(tl(u),tl(sk1)) -> equal(u,sk1) equal(nil,u) equal(nil,sk1). % 1.83/2.03 515[0:Res:1.0,111.1] ssItem(u) || equal(cons(u,sk1),sk1)** -> . % 1.83/2.03 570[1:Spt:84.1] || -> ssItem(u)*. % 1.83/2.03 602[1:MRR:114.1,114.0,570.0] || -> equal(u,v) neq(u,v)*. % 1.83/2.03 610[1:MRR:7.0,570.0] || memberP(sk2,u) equal(cons(u,nil),sk1)** -> . % 1.83/2.03 1213[1:SpL:205.1,610.1] || neq(sk2,nil) memberP(sk2,sk5)* equal(sk1,sk1) -> . % 1.83/2.03 1216[1:Obv:1213.2] || neq(sk2,nil) memberP(sk2,sk5)* -> . % 1.83/2.03 1217[1:MRR:1216.1,201.1] || neq(sk2,nil)* -> . % 1.83/2.03 1220[1:Res:602.1,1217.0] || -> equal(nil,sk2)**. % 1.83/2.03 1221[1:MRR:1220.0,204.0] || -> . % 1.83/2.03 1222[1:Spt:1221.0,84.0,84.2] ssList(u) || -> duplicatefreeP(u)*. % 1.83/2.03 1242[2:Spt:462.0] || -> ssItem(u)*. % 1.83/2.03 1270[2:MRR:114.1,114.0,1242.0] || -> equal(u,v) neq(u,v)*. % 1.83/2.03 1275[2:MRR:7.0,1242.0] || memberP(sk2,u) equal(cons(u,nil),sk1)** -> . % 1.83/2.03 1890[2:SpL:205.1,1275.1] || neq(sk2,nil) memberP(sk2,sk5)* equal(sk1,sk1) -> . % 1.83/2.03 1893[2:Obv:1890.2] || neq(sk2,nil) memberP(sk2,sk5)* -> . % 1.83/2.03 1894[2:MRR:1893.1,201.1] || neq(sk2,nil)* -> . % 1.83/2.03 1895[2:Res:1270.1,1894.0] || -> equal(nil,sk2)**. % 1.83/2.03 1896[2:MRR:1895.0,204.0] || -> . % 1.83/2.03 1897[2:Spt:1896.0,462.1] || -> duplicatefreeP(sk1)*. % 1.83/2.03 1900[3:Spt:291.0] || -> ssItem(u)*. % 1.83/2.03 1932[3:MRR:114.1,114.0,1900.0] || -> equal(u,v) neq(u,v)*. % 1.83/2.03 1940[3:MRR:7.0,1900.0] || memberP(sk2,u) equal(cons(u,nil),sk1)** -> . % 1.83/2.03 2532[3:SpL:205.1,1940.1] || neq(sk2,nil) memberP(sk2,sk5)* equal(sk1,sk1) -> . % 1.83/2.03 2535[3:Obv:2532.2] || neq(sk2,nil) memberP(sk2,sk5)* -> . % 1.83/2.03 2536[3:MRR:2535.1,201.1] || neq(sk2,nil)* -> . % 1.83/2.03 2539[3:Res:1932.1,2536.0] || -> equal(nil,sk2)**. % 1.83/2.03 2540[3:MRR:2539.0,204.0] || -> . % 1.83/2.03 2541[3:Spt:2540.0,291.1] || -> duplicatefreeP(sk2)*. % 1.83/2.03 2542[4:Spt:477.5] || -> equal(nil,sk1)**. % 1.83/2.03 2557[4:Rew:2542.0,204.0] || equal(sk2,sk1)** -> . % 1.83/2.03 2609[4:Rew:2542.0,205.0] || neq(sk2,sk1) -> equal(cons(sk5,nil),sk1)**. % 1.83/2.03 2611[4:Rew:2542.0,200.0] || neq(sk2,sk1)* -> ssItem(sk5). % 1.83/2.03 2690[4:Rew:2542.0,2609.1] || neq(sk2,sk1) -> equal(cons(sk5,sk1),sk1)**. % 1.83/2.03 2720[5:Spt:229.0] || -> strictorderedP(sk2)*. % 1.83/2.03 2723[6:Spt:228.0] || -> totalorderedP(sk2)*. % 1.83/2.03 2727[7:Spt:286.0] || -> cyclefreeP(sk2)*. % 1.83/2.03 2729[8:Spt:227.0] || -> strictorderP(sk2)*. % 1.83/2.03 2730[9:Spt:226.0] || -> totalorderP(sk2)*. % 1.83/2.03 2731[10:Spt:2611.0] || neq(sk2,sk1)* -> . % 1.83/2.03 2904[10:Res:440.2,2731.0] ssList(sk2) || -> equal(sk2,sk1)**. % 1.83/2.03 2905[10:SSi:2904.0,2.0,2541.0,2720.0,2723.0,2727.0,2729.0,2730.0] || -> equal(sk2,sk1)**. % 1.83/2.03 2906[10:MRR:2905.0,2557.0] || -> . % 1.83/2.03 2907[10:Spt:2906.0,2611.0,2731.0] || -> neq(sk2,sk1)*. % 1.83/2.03 2908[10:Spt:2906.0,2611.1] || -> ssItem(sk5)*. % 1.83/2.03 2910[10:MRR:2690.0,2907.0] || -> equal(cons(sk5,sk1),sk1)**. % 1.83/2.03 2923[10:SpL:2910.0,515.1] ssItem(sk5) || equal(sk1,sk1)* -> . % 1.83/2.03 2926[10:Obv:2923.1] ssItem(sk5) || -> . % 1.83/2.03 2927[10:SSi:2926.0,2908.0] || -> . % 1.83/2.03 2937[9:Spt:2927.0,226.0,2730.0] || totalorderP(sk2)* -> . % 1.83/2.03 2938[9:Spt:2927.0,226.1] || -> equal(app(app(skaf56(sk2),cons(skaf54(sk2),skaf57(sk2))),cons(skaf55(sk2),skaf58(sk2))),sk2)**. % 1.83/2.03 2952[10:Spt:2611.0] || neq(sk2,sk1)* -> . % 1.83/2.03 2953[10:Res:440.2,2952.0] ssList(sk2) || -> equal(sk2,sk1)**. % 1.83/2.03 2954[10:SSi:2953.0,2.0,2541.0,2720.0,2723.0,2727.0,2729.0] || -> equal(sk2,sk1)**. % 1.83/2.03 2955[10:MRR:2954.0,2557.0] || -> . % 1.83/2.03 2956[10:Spt:2955.0,2611.0,2952.0] || -> neq(sk2,sk1)*. % 1.83/2.03 2957[10:Spt:2955.0,2611.1] || -> ssItem(sk5)*. % 1.83/2.03 2959[10:MRR:2690.0,2956.0] || -> equal(cons(sk5,sk1),sk1)**. % 1.83/2.03 2972[10:SpL:2959.0,515.1] ssItem(sk5) || equal(sk1,sk1)* -> . % 1.83/2.03 2975[10:Obv:2972.1] ssItem(sk5) || -> . % 1.83/2.03 2976[10:SSi:2975.0,2957.0] || -> . % 1.83/2.03 2986[8:Spt:2976.0,227.0,2729.0] || strictorderP(sk2)* -> . % 1.83/2.03 2987[8:Spt:2976.0,227.1] || -> equal(app(app(skaf61(sk2),cons(skaf59(sk2),skaf62(sk2))),cons(skaf60(sk2),skaf63(sk2))),sk2)**. % 1.83/2.03 2997[9:Spt:226.0] || -> totalorderP(sk2)*. % 1.83/2.03 3002[10:Spt:2611.0] || neq(sk2,sk1)* -> . % 1.83/2.03 3003[10:Res:440.2,3002.0] ssList(sk2) || -> equal(sk2,sk1)**. % 1.83/2.03 3004[10:SSi:3003.0,2.0,2541.0,2720.0,2723.0,2727.0,2997.0] || -> equal(sk2,sk1)**. % 1.83/2.03 3005[10:MRR:3004.0,2557.0] || -> . % 1.83/2.03 3006[10:Spt:3005.0,2611.0,3002.0] || -> neq(sk2,sk1)*. % 1.83/2.03 3007[10:Spt:3005.0,2611.1] || -> ssItem(sk5)*. % 1.83/2.03 3009[10:MRR:2690.0,3006.0] || -> equal(cons(sk5,sk1),sk1)**. % 1.83/2.03 3022[10:SpL:3009.0,515.1] ssItem(sk5) || equal(sk1,sk1)* -> . % 1.83/2.03 3025[10:Obv:3022.1] ssItem(sk5) || -> . % 1.83/2.03 3026[10:SSi:3025.0,3007.0] || -> . % 1.83/2.03 3036[9:Spt:3026.0,226.0,2997.0] || totalorderP(sk2)* -> . % 1.83/2.03 3037[9:Spt:3026.0,226.1] || -> equal(app(app(skaf56(sk2),cons(skaf54(sk2),skaf57(sk2))),cons(skaf55(sk2),skaf58(sk2))),sk2)**. % 1.83/2.03 3045[10:Spt:2611.0] || neq(sk2,sk1)* -> . % 1.83/2.03 3046[10:Res:440.2,3045.0] ssList(sk2) || -> equal(sk2,sk1)**. % 1.83/2.03 3047[10:SSi:3046.0,2.0,2541.0,2720.0,2723.0,2727.0] || -> equal(sk2,sk1)**. % 1.83/2.03 3048[10:MRR:3047.0,2557.0] || -> . % 1.83/2.03 3049[10:Spt:3048.0,2611.0,3045.0] || -> neq(sk2,sk1)*. % 1.83/2.03 3050[10:Spt:3048.0,2611.1] || -> ssItem(sk5)*. % 1.83/2.03 3052[10:MRR:2690.0,3049.0] || -> equal(cons(sk5,sk1),sk1)**. % 1.83/2.03 3065[10:SpL:3052.0,515.1] ssItem(sk5) || equal(sk1,sk1)* -> . % 1.83/2.03 3068[10:Obv:3065.1] ssItem(sk5) || -> . % 1.83/2.03 3069[10:SSi:3068.0,3050.0] || -> . % 1.83/2.03 3079[7:Spt:3069.0,286.0,2727.0] || cyclefreeP(sk2)* -> . % 1.83/2.03 3080[7:Spt:3069.0,286.1] || -> leq(skaf49(sk2),skaf50(sk2))*. % 1.83/2.03 3085[8:Spt:226.0] || -> totalorderP(sk2)*. % 1.83/2.03 3086[9:Spt:227.0] || -> strictorderP(sk2)*. % 1.83/2.03 3087[10:Spt:2611.0] || neq(sk2,sk1)* -> . % 1.83/2.03 3088[10:Res:440.2,3087.0] ssList(sk2) || -> equal(sk2,sk1)**. % 1.83/2.03 3089[10:SSi:3088.0,2.0,2541.0,2720.0,2723.0,3085.0,3086.0] || -> equal(sk2,sk1)**. % 1.83/2.03 3090[10:MRR:3089.0,2557.0] || -> . % 1.83/2.03 3091[10:Spt:3090.0,2611.0,3087.0] || -> neq(sk2,sk1)*. % 1.83/2.03 3092[10:Spt:3090.0,2611.1] || -> ssItem(sk5)*. % 1.83/2.03 3094[10:MRR:2690.0,3091.0] || -> equal(cons(sk5,sk1),sk1)**. % 1.83/2.03 3111[10:SpL:3094.0,515.1] ssItem(sk5) || equal(sk1,sk1)* -> . % 1.83/2.03 3114[10:Obv:3111.1] ssItem(sk5) || -> . % 1.83/2.03 3115[10:SSi:3114.0,3092.0] || -> . % 1.83/2.03 3125[9:Spt:3115.0,227.0,3086.0] || strictorderP(sk2)* -> . % 1.83/2.03 3126[9:Spt:3115.0,227.1] || -> equal(app(app(skaf61(sk2),cons(skaf59(sk2),skaf62(sk2))),cons(skaf60(sk2),skaf63(sk2))),sk2)**. % 1.83/2.03 3134[10:Spt:2611.0] || neq(sk2,sk1)* -> . % 1.83/2.03 3135[10:Res:440.2,3134.0] ssList(sk2) || -> equal(sk2,sk1)**. % 1.83/2.03 3136[10:SSi:3135.0,2.0,2541.0,2720.0,2723.0,3085.0] || -> equal(sk2,sk1)**. % 1.83/2.03 3137[10:MRR:3136.0,2557.0] || -> . % 1.83/2.03 3138[10:Spt:3137.0,2611.0,3134.0] || -> neq(sk2,sk1)*. % 1.83/2.03 3139[10:Spt:3137.0,2611.1] || -> ssItem(sk5)*. % 1.83/2.03 3141[10:MRR:2690.0,3138.0] || -> equal(cons(sk5,sk1),sk1)**. % 1.83/2.03 3154[10:SpL:3141.0,515.1] ssItem(sk5) || equal(sk1,sk1)* -> . % 1.83/2.03 3157[10:Obv:3154.1] ssItem(sk5) || -> . % 1.83/2.03 3158[10:SSi:3157.0,3139.0] || -> . % 1.83/2.03 3168[8:Spt:3158.0,226.0,3085.0] || totalorderP(sk2)* -> . % 1.83/2.03 3169[8:Spt:3158.0,226.1] || -> equal(app(app(skaf56(sk2),cons(skaf54(sk2),skaf57(sk2))),cons(skaf55(sk2),skaf58(sk2))),sk2)**. % 1.83/2.03 3177[9:Spt:227.0] || -> strictorderP(sk2)*. % 1.83/2.03 3178[10:Spt:2611.0] || neq(sk2,sk1)* -> . % 1.83/2.03 3179[10:Res:440.2,3178.0] ssList(sk2) || -> equal(sk2,sk1)**. % 1.83/2.03 3180[10:SSi:3179.0,2.0,2541.0,2720.0,2723.0,3177.0] || -> equal(sk2,sk1)**. % 1.83/2.03 3181[10:MRR:3180.0,2557.0] || -> . % 1.83/2.03 3182[10:Spt:3181.0,2611.0,3178.0] || -> neq(sk2,sk1)*. % 1.83/2.03 3183[10:Spt:3181.0,2611.1] || -> ssItem(sk5)*. % 1.83/2.03 3185[10:MRR:2690.0,3182.0] || -> equal(cons(sk5,sk1),sk1)**. % 1.83/2.03 3198[10:SpL:3185.0,515.1] ssItem(sk5) || equal(sk1,sk1)* -> . % 1.83/2.03 3201[10:Obv:3198.1] ssItem(sk5) || -> . % 1.83/2.03 3202[10:SSi:3201.0,3183.0] || -> . % 1.83/2.03 3212[9:Spt:3202.0,227.0,3177.0] || strictorderP(sk2)* -> . % 1.83/2.03 3213[9:Spt:3202.0,227.1] || -> equal(app(app(skaf61(sk2),cons(skaf59(sk2),skaf62(sk2))),cons(skaf60(sk2),skaf63(sk2))),sk2)**. % 1.83/2.03 3221[10:Spt:2611.0] || neq(sk2,sk1)* -> . % 1.83/2.03 3222[10:Res:440.2,3221.0] ssList(sk2) || -> equal(sk2,sk1)**. % 1.83/2.03 3223[10:SSi:3222.0,2.0,2541.0,2720.0,2723.0] || -> equal(sk2,sk1)**. % 1.83/2.03 3224[10:MRR:3223.0,2557.0] || -> . % 1.83/2.03 3225[10:Spt:3224.0,2611.0,3221.0] || -> neq(sk2,sk1)*. % 1.83/2.03 3226[10:Spt:3224.0,2611.1] || -> ssItem(sk5)*. % 1.83/2.03 3228[10:MRR:2690.0,3225.0] || -> equal(cons(sk5,sk1),sk1)**. % 1.83/2.03 3241[10:SpL:3228.0,515.1] ssItem(sk5) || equal(sk1,sk1)* -> . % 1.83/2.03 3244[10:Obv:3241.1] ssItem(sk5) || -> . % 1.83/2.03 3245[10:SSi:3244.0,3226.0] || -> . % 1.83/2.03 3255[6:Spt:3245.0,228.0,2723.0] || totalorderedP(sk2)* -> . % 1.83/2.03 3256[6:Spt:3245.0,228.1] || -> equal(app(app(skaf66(sk2),cons(skaf64(sk2),skaf67(sk2))),cons(skaf65(sk2),skaf68(sk2))),sk2)**. % 1.83/2.03 3267[7:Spt:285.0] || -> cyclefreeP(sk2)*. % 1.83/2.03 3269[8:Spt:227.0] || -> strictorderP(sk2)*. % 1.83/2.03 3274[9:Spt:226.0] || -> totalorderP(sk2)*. % 1.83/2.03 3276[10:Spt:2611.0] || neq(sk2,sk1)* -> . % 1.83/2.03 3277[10:Res:440.2,3276.0] ssList(sk2) || -> equal(sk2,sk1)**. % 1.83/2.03 3278[10:SSi:3277.0,2.0,2541.0,2720.0,3267.0,3269.0,3274.0] || -> equal(sk2,sk1)**. % 1.83/2.03 3279[10:MRR:3278.0,2557.0] || -> . % 1.83/2.03 3280[10:Spt:3279.0,2611.0,3276.0] || -> neq(sk2,sk1)*. % 1.83/2.03 3281[10:Spt:3279.0,2611.1] || -> ssItem(sk5)*. % 1.83/2.03 3283[10:MRR:2690.0,3280.0] || -> equal(cons(sk5,sk1),sk1)**. % 1.83/2.03 3296[10:SpL:3283.0,515.1] ssItem(sk5) || equal(sk1,sk1)* -> . % 1.83/2.03 3299[10:Obv:3296.1] ssItem(sk5) || -> . % 1.83/2.03 3300[10:SSi:3299.0,3281.0] || -> . % 1.83/2.03 3310[9:Spt:3300.0,226.0,3274.0] || totalorderP(sk2)* -> . % 1.83/2.03 3311[9:Spt:3300.0,226.1] || -> equal(app(app(skaf56(sk2),cons(skaf54(sk2),skaf57(sk2))),cons(skaf55(sk2),skaf58(sk2))),sk2)**. % 1.83/2.03 3319[10:Spt:2611.0] || neq(sk2,sk1)* -> . % 1.83/2.03 3320[10:Res:440.2,3319.0] ssList(sk2) || -> equal(sk2,sk1)**. % 1.83/2.03 3321[10:SSi:3320.0,2.0,2541.0,2720.0,3267.0,3269.0] || -> equal(sk2,sk1)**. % 1.83/2.03 3322[10:MRR:3321.0,2557.0] || -> . % 1.83/2.03 3323[10:Spt:3322.0,2611.0,3319.0] || -> neq(sk2,sk1)*. % 1.83/2.03 3324[10:Spt:3322.0,2611.1] || -> ssItem(sk5)*. % 1.83/2.03 3326[10:MRR:2690.0,3323.0] || -> equal(cons(sk5,sk1),sk1)**. % 1.83/2.03 3339[10:SpL:3326.0,515.1] ssItem(sk5) || equal(sk1,sk1)* -> . % 1.83/2.03 3342[10:Obv:3339.1] ssItem(sk5) || -> . % 1.83/2.03 3343[10:SSi:3342.0,3324.0] || -> . % 1.83/2.03 3353[8:Spt:3343.0,227.0,3269.0] || strictorderP(sk2)* -> . % 1.83/2.03 3354[8:Spt:3343.0,227.1] || -> equal(app(app(skaf61(sk2),cons(skaf59(sk2),skaf62(sk2))),cons(skaf60(sk2),skaf63(sk2))),sk2)**. % 1.83/2.03 3362[9:Spt:226.0] || -> totalorderP(sk2)*. % 1.83/2.03 3364[10:Spt:2611.0] || neq(sk2,sk1)* -> . % 1.83/2.03 3365[10:Res:440.2,3364.0] ssList(sk2) || -> equal(sk2,sk1)**. % 1.83/2.03 3366[10:SSi:3365.0,2.0,2541.0,2720.0,3267.0,3362.0] || -> equal(sk2,sk1)**. % 1.83/2.03 3367[10:MRR:3366.0,2557.0] || -> . % 1.83/2.03 3368[10:Spt:3367.0,2611.0,3364.0] || -> neq(sk2,sk1)*. % 1.83/2.03 3369[10:Spt:3367.0,2611.1] || -> ssItem(sk5)*. % 1.83/2.03 3371[10:MRR:2690.0,3368.0] || -> equal(cons(sk5,sk1),sk1)**. % 1.83/2.03 3384[10:SpL:3371.0,515.1] ssItem(sk5) || equal(sk1,sk1)* -> . % 1.83/2.03 3387[10:Obv:3384.1] ssItem(sk5) || -> . % 1.83/2.03 3388[10:SSi:3387.0,3369.0] || -> . % 1.83/2.03 3398[9:Spt:3388.0,226.0,3362.0] || totalorderP(sk2)* -> . % 1.83/2.03 3399[9:Spt:3388.0,226.1] || -> equal(app(app(skaf56(sk2),cons(skaf54(sk2),skaf57(sk2))),cons(skaf55(sk2),skaf58(sk2))),sk2)**. % 1.83/2.03 3407[10:Spt:2611.0] || neq(sk2,sk1)* -> . % 1.83/2.03 3408[10:Res:440.2,3407.0] ssList(sk2) || -> equal(sk2,sk1)**. % 1.83/2.03 3409[10:SSi:3408.0,2.0,2541.0,2720.0,3267.0] || -> equal(sk2,sk1)**. % 1.83/2.03 3410[10:MRR:3409.0,2557.0] || -> . % 1.83/2.03 3411[10:Spt:3410.0,2611.0,3407.0] || -> neq(sk2,sk1)*. % 1.83/2.03 3412[10:Spt:3410.0,2611.1] || -> ssItem(sk5)*. % 1.83/2.03 3414[10:MRR:2690.0,3411.0] || -> equal(cons(sk5,sk1),sk1)**. % 1.83/2.03 3427[10:SpL:3414.0,515.1] ssItem(sk5) || equal(sk1,sk1)* -> . % 1.83/2.03 3430[10:Obv:3427.1] ssItem(sk5) || -> . % 1.83/2.03 3431[10:SSi:3430.0,3412.0] || -> . % 1.83/2.03 3441[7:Spt:3431.0,285.0,3267.0] || cyclefreeP(sk2)* -> . % 1.83/2.03 3442[7:Spt:3431.0,285.1] || -> leq(skaf50(sk2),skaf49(sk2))*. % 1.83/2.03 3445[8:Spt:226.0] || -> totalorderP(sk2)*. % 1.83/2.03 3447[9:Spt:227.0] || -> strictorderP(sk2)*. % 1.83/2.03 3448[10:Spt:2611.0] || neq(sk2,sk1)* -> . % 1.83/2.03 3449[10:Res:440.2,3448.0] ssList(sk2) || -> equal(sk2,sk1)**. % 1.83/2.03 3450[10:SSi:3449.0,2.0,2541.0,2720.0,3445.0,3447.0] || -> equal(sk2,sk1)**. % 1.83/2.03 3451[10:MRR:3450.0,2557.0] || -> . % 1.83/2.03 3452[10:Spt:3451.0,2611.0,3448.0] || -> neq(sk2,sk1)*. % 1.83/2.03 3453[10:Spt:3451.0,2611.1] || -> ssItem(sk5)*. % 1.83/2.03 3455[10:MRR:2690.0,3452.0] || -> equal(cons(sk5,sk1),sk1)**. % 1.83/2.03 3468[10:SpL:3455.0,515.1] ssItem(sk5) || equal(sk1,sk1)* -> . % 1.83/2.03 3471[10:Obv:3468.1] ssItem(sk5) || -> . % 1.83/2.03 3472[10:SSi:3471.0,3453.0] || -> . % 1.83/2.03 3482[9:Spt:3472.0,227.0,3447.0] || strictorderP(sk2)* -> . % 1.83/2.03 3483[9:Spt:3472.0,227.1] || -> equal(app(app(skaf61(sk2),cons(skaf59(sk2),skaf62(sk2))),cons(skaf60(sk2),skaf63(sk2))),sk2)**. % 1.83/2.03 3491[10:Spt:2611.0] || neq(sk2,sk1)* -> . % 1.83/2.03 3492[10:Res:440.2,3491.0] ssList(sk2) || -> equal(sk2,sk1)**. % 1.83/2.03 3493[10:SSi:3492.0,2.0,2541.0,2720.0,3445.0] || -> equal(sk2,sk1)**. % 1.83/2.03 3494[10:MRR:3493.0,2557.0] || -> . % 1.83/2.03 3495[10:Spt:3494.0,2611.0,3491.0] || -> neq(sk2,sk1)*. % 1.83/2.03 3496[10:Spt:3494.0,2611.1] || -> ssItem(sk5)*. % 1.83/2.03 3498[10:MRR:2690.0,3495.0] || -> equal(cons(sk5,sk1),sk1)**. % 1.83/2.03 3511[10:SpL:3498.0,515.1] ssItem(sk5) || equal(sk1,sk1)* -> . % 1.83/2.03 3514[10:Obv:3511.1] ssItem(sk5) || -> . % 1.83/2.03 3515[10:SSi:3514.0,3496.0] || -> . % 1.83/2.03 3525[8:Spt:3515.0,226.0,3445.0] || totalorderP(sk2)* -> . % 1.83/2.03 3526[8:Spt:3515.0,226.1] || -> equal(app(app(skaf56(sk2),cons(skaf54(sk2),skaf57(sk2))),cons(skaf55(sk2),skaf58(sk2))),sk2)**. % 1.83/2.03 3534[9:Spt:227.0] || -> strictorderP(sk2)*. % 1.83/2.03 3535[10:Spt:2611.0] || neq(sk2,sk1)* -> . % 1.83/2.03 3536[10:Res:440.2,3535.0] ssList(sk2) || -> equal(sk2,sk1)**. % 1.83/2.03 3537[10:SSi:3536.0,2.0,2541.0,2720.0,3534.0] || -> equal(sk2,sk1)**. % 1.83/2.03 3538[10:MRR:3537.0,2557.0] || -> . % 1.83/2.03 3539[10:Spt:3538.0,2611.0,3535.0] || -> neq(sk2,sk1)*. % 1.83/2.03 3540[10:Spt:3538.0,2611.1] || -> ssItem(sk5)*. % 1.83/2.03 3542[10:MRR:2690.0,3539.0] || -> equal(cons(sk5,sk1),sk1)**. % 1.83/2.03 3555[10:SpL:3542.0,515.1] ssItem(sk5) || equal(sk1,sk1)* -> . % 1.83/2.03 3558[10:Obv:3555.1] ssItem(sk5) || -> . % 1.83/2.03 3559[10:SSi:3558.0,3540.0] || -> . % 1.83/2.03 3569[9:Spt:3559.0,227.0,3534.0] || strictorderP(sk2)* -> . % 1.83/2.03 3570[9:Spt:3559.0,227.1] || -> equal(app(app(skaf61(sk2),cons(skaf59(sk2),skaf62(sk2))),cons(skaf60(sk2),skaf63(sk2))),sk2)**. % 1.83/2.03 3578[10:Spt:2611.0] || neq(sk2,sk1)* -> . % 1.83/2.03 3579[10:Res:440.2,3578.0] ssList(sk2) || -> equal(sk2,sk1)**. % 1.83/2.03 3580[10:SSi:3579.0,2.0,2541.0,2720.0] || -> equal(sk2,sk1)**. % 1.83/2.03 3581[10:MRR:3580.0,2557.0] || -> . % 1.83/2.03 3582[10:Spt:3581.0,2611.0,3578.0] || -> neq(sk2,sk1)*. % 1.83/2.03 3583[10:Spt:3581.0,2611.1] || -> ssItem(sk5)*. % 1.83/2.03 3585[10:MRR:2690.0,3582.0] || -> equal(cons(sk5,sk1),sk1)**. % 1.83/2.03 3598[10:SpL:3585.0,515.1] ssItem(sk5) || equal(sk1,sk1)* -> . % 1.83/2.03 3601[10:Obv:3598.1] ssItem(sk5) || -> . % 1.83/2.03 3602[10:SSi:3601.0,3583.0] || -> . % 1.83/2.03 3612[5:Spt:3602.0,229.0,2720.0] || strictorderedP(sk2)* -> . % 1.83/2.03 3613[5:Spt:3602.0,229.1] || -> equal(app(app(skaf71(sk2),cons(skaf69(sk2),skaf72(sk2))),cons(skaf70(sk2),skaf73(sk2))),sk2)**. % 1.83/2.03 3624[6:Spt:228.0] || -> totalorderedP(sk2)*. % 1.83/2.03 3628[7:Spt:286.0] || -> cyclefreeP(sk2)*. % 1.83/2.03 3634[8:Spt:227.0] || -> strictorderP(sk2)*. % 1.83/2.03 3636[9:Spt:2611.0] || neq(sk2,sk1)* -> . % 1.83/2.03 3637[9:Res:440.2,3636.0] ssList(sk2) || -> equal(sk2,sk1)**. % 1.83/2.03 3638[9:SSi:3637.0,2.0,2541.0,3624.0,3628.0,3634.0] || -> equal(sk2,sk1)**. % 1.83/2.03 3639[9:MRR:3638.0,2557.0] || -> . % 1.83/2.03 3640[9:Spt:3639.0,2611.0,3636.0] || -> neq(sk2,sk1)*. % 1.83/2.03 3641[9:Spt:3639.0,2611.1] || -> ssItem(sk5)*. % 1.83/2.03 3643[9:MRR:2690.0,3640.0] || -> equal(cons(sk5,sk1),sk1)**. % 1.83/2.03 3657[9:SpL:3643.0,515.1] ssItem(sk5) || equal(sk1,sk1)* -> . % 1.83/2.03 3660[9:Obv:3657.1] ssItem(sk5) || -> . % 1.83/2.03 3661[9:SSi:3660.0,3641.0] || -> . % 1.83/2.03 3671[8:Spt:3661.0,227.0,3634.0] || strictorderP(sk2)* -> . % 1.83/2.03 3672[8:Spt:3661.0,227.1] || -> equal(app(app(skaf61(sk2),cons(skaf59(sk2),skaf62(sk2))),cons(skaf60(sk2),skaf63(sk2))),sk2)**. % 1.83/2.03 3680[9:Spt:226.0] || -> totalorderP(sk2)*. % 1.83/2.03 3681[10:Spt:2611.0] || neq(sk2,sk1)* -> . % 1.83/2.03 3682[10:Res:440.2,3681.0] ssList(sk2) || -> equal(sk2,sk1)**. % 1.83/2.03 3683[10:SSi:3682.0,2.0,2541.0,3624.0,3628.0,3680.0] || -> equal(sk2,sk1)**. % 1.83/2.03 3684[10:MRR:3683.0,2557.0] || -> . % 1.83/2.03 3685[10:Spt:3684.0,2611.0,3681.0] || -> neq(sk2,sk1)*. % 1.83/2.03 3686[10:Spt:3684.0,2611.1] || -> ssItem(sk5)*. % 1.83/2.03 3688[10:MRR:2690.0,3685.0] || -> equal(cons(sk5,sk1),sk1)**. % 1.83/2.03 3701[10:SpL:3688.0,515.1] ssItem(sk5) || equal(sk1,sk1)* -> . % 1.83/2.03 3704[10:Obv:3701.1] ssItem(sk5) || -> . % 1.83/2.03 3705[10:SSi:3704.0,3686.0] || -> . % 1.83/2.03 3715[9:Spt:3705.0,226.0,3680.0] || totalorderP(sk2)* -> . % 1.83/2.03 3716[9:Spt:3705.0,226.1] || -> equal(app(app(skaf56(sk2),cons(skaf54(sk2),skaf57(sk2))),cons(skaf55(sk2),skaf58(sk2))),sk2)**. % 1.83/2.03 3724[10:Spt:2611.0] || neq(sk2,sk1)* -> . % 1.83/2.03 3725[10:Res:440.2,3724.0] ssList(sk2) || -> equal(sk2,sk1)**. % 1.83/2.03 3726[10:SSi:3725.0,2.0,2541.0,3624.0,3628.0] || -> equal(sk2,sk1)**. % 1.83/2.03 3727[10:MRR:3726.0,2557.0] || -> . % 1.83/2.03 3728[10:Spt:3727.0,2611.0,3724.0] || -> neq(sk2,sk1)*. % 1.83/2.03 3729[10:Spt:3727.0,2611.1] || -> ssItem(sk5)*. % 1.83/2.03 3731[10:MRR:2690.0,3728.0] || -> equal(cons(sk5,sk1),sk1)**. % 1.83/2.03 3744[10:SpL:3731.0,515.1] ssItem(sk5) || equal(sk1,sk1)* -> . % 1.83/2.03 3747[10:Obv:3744.1] ssItem(sk5) || -> . % 1.83/2.03 3748[10:SSi:3747.0,3729.0] || -> . % 1.83/2.03 3758[7:Spt:3748.0,286.0,3628.0] || cyclefreeP(sk2)* -> . % 1.83/2.03 3759[7:Spt:3748.0,286.1] || -> leq(skaf49(sk2),skaf50(sk2))*. % 1.83/2.03 3762[8:Spt:226.0] || -> totalorderP(sk2)*. % 1.83/2.03 3763[9:Spt:227.0] || -> strictorderP(sk2)*. % 1.83/2.03 3765[10:Spt:2611.0] || neq(sk2,sk1)* -> . % 1.83/2.03 3766[10:Res:440.2,3765.0] ssList(sk2) || -> equal(sk2,sk1)**. % 1.83/2.03 3767[10:SSi:3766.0,2.0,2541.0,3624.0,3762.0,3763.0] || -> equal(sk2,sk1)**. % 1.83/2.03 3768[10:MRR:3767.0,2557.0] || -> . % 1.83/2.03 3769[10:Spt:3768.0,2611.0,3765.0] || -> neq(sk2,sk1)*. % 1.83/2.03 3770[10:Spt:3768.0,2611.1] || -> ssItem(sk5)*. % 1.83/2.03 3772[10:MRR:2690.0,3769.0] || -> equal(cons(sk5,sk1),sk1)**. % 1.83/2.03 3785[10:SpL:3772.0,515.1] ssItem(sk5) || equal(sk1,sk1)* -> . % 1.83/2.03 3788[10:Obv:3785.1] ssItem(sk5) || -> . % 1.83/2.03 3789[10:SSi:3788.0,3770.0] || -> . % 1.83/2.03 3799[9:Spt:3789.0,227.0,3763.0] || strictorderP(sk2)* -> . % 1.83/2.03 3800[9:Spt:3789.0,227.1] || -> equal(app(app(skaf61(sk2),cons(skaf59(sk2),skaf62(sk2))),cons(skaf60(sk2),skaf63(sk2))),sk2)**. % 1.83/2.03 3808[10:Spt:2611.0] || neq(sk2,sk1)* -> . % 1.83/2.03 3809[10:Res:440.2,3808.0] ssList(sk2) || -> equal(sk2,sk1)**. % 1.83/2.03 3810[10:SSi:3809.0,2.0,2541.0,3624.0,3762.0] || -> equal(sk2,sk1)**. % 1.83/2.03 3811[10:MRR:3810.0,2557.0] || -> . % 1.83/2.03 3812[10:Spt:3811.0,2611.0,3808.0] || -> neq(sk2,sk1)*. % 1.83/2.03 3813[10:Spt:3811.0,2611.1] || -> ssItem(sk5)*. % 1.83/2.03 3815[10:MRR:2690.0,3812.0] || -> equal(cons(sk5,sk1),sk1)**. % 1.83/2.03 3828[10:SpL:3815.0,515.1] ssItem(sk5) || equal(sk1,sk1)* -> . % 1.83/2.03 3831[10:Obv:3828.1] ssItem(sk5) || -> . % 1.83/2.03 3832[10:SSi:3831.0,3813.0] || -> . % 1.83/2.03 3842[8:Spt:3832.0,226.0,3762.0] || totalorderP(sk2)* -> . % 1.83/2.03 3843[8:Spt:3832.0,226.1] || -> equal(app(app(skaf56(sk2),cons(skaf54(sk2),skaf57(sk2))),cons(skaf55(sk2),skaf58(sk2))),sk2)**. % 1.83/2.03 3851[9:Spt:227.0] || -> strictorderP(sk2)*. % 1.83/2.03 3853[10:Spt:2611.0] || neq(sk2,sk1)* -> . % 1.83/2.03 3854[10:Res:440.2,3853.0] ssList(sk2) || -> equal(sk2,sk1)**. % 1.83/2.03 3855[10:SSi:3854.0,2.0,2541.0,3624.0,3851.0] || -> equal(sk2,sk1)**. % 1.83/2.03 3856[10:MRR:3855.0,2557.0] || -> . % 1.83/2.03 3857[10:Spt:3856.0,2611.0,3853.0] || -> neq(sk2,sk1)*. % 1.83/2.03 3858[10:Spt:3856.0,2611.1] || -> ssItem(sk5)*. % 1.83/2.03 3860[10:MRR:2690.0,3857.0] || -> equal(cons(sk5,sk1),sk1)**. % 1.83/2.03 3873[10:SpL:3860.0,515.1] ssItem(sk5) || equal(sk1,sk1)* -> . % 1.83/2.03 3876[10:Obv:3873.1] ssItem(sk5) || -> . % 1.83/2.03 3877[10:SSi:3876.0,3858.0] || -> . % 1.83/2.03 3887[9:Spt:3877.0,227.0,3851.0] || strictorderP(sk2)* -> . % 1.83/2.03 3888[9:Spt:3877.0,227.1] || -> equal(app(app(skaf61(sk2),cons(skaf59(sk2),skaf62(sk2))),cons(skaf60(sk2),skaf63(sk2))),sk2)**. % 1.83/2.03 3896[10:Spt:2611.0] || neq(sk2,sk1)* -> . % 1.83/2.03 3897[10:Res:440.2,3896.0] ssList(sk2) || -> equal(sk2,sk1)**. % 1.83/2.03 3898[10:SSi:3897.0,2.0,2541.0,3624.0] || -> equal(sk2,sk1)**. % 1.83/2.03 3899[10:MRR:3898.0,2557.0] || -> . % 1.83/2.03 3900[10:Spt:3899.0,2611.0,3896.0] || -> neq(sk2,sk1)*. % 1.83/2.03 3901[10:Spt:3899.0,2611.1] || -> ssItem(sk5)*. % 1.83/2.03 3903[10:MRR:2690.0,3900.0] || -> equal(cons(sk5,sk1),sk1)**. % 1.83/2.03 3916[10:SpL:3903.0,515.1] ssItem(sk5) || equal(sk1,sk1)* -> . % 1.83/2.03 3919[10:Obv:3916.1] ssItem(sk5) || -> . % 1.83/2.03 3920[10:SSi:3919.0,3901.0] || -> . % 1.83/2.03 3930[6:Spt:3920.0,228.0,3624.0] || totalorderedP(sk2)* -> . % 1.83/2.03 3931[6:Spt:3920.0,228.1] || -> equal(app(app(skaf66(sk2),cons(skaf64(sk2),skaf67(sk2))),cons(skaf65(sk2),skaf68(sk2))),sk2)**. % 1.83/2.03 3940[7:Spt:285.0] || -> cyclefreeP(sk2)*. % 1.83/2.03 3942[8:Spt:227.0] || -> strictorderP(sk2)*. % 1.83/2.03 3944[9:Spt:2611.0] || neq(sk2,sk1)* -> . % 1.83/2.03 3945[9:Res:440.2,3944.0] ssList(sk2) || -> equal(sk2,sk1)**. % 1.83/2.03 3946[9:SSi:3945.0,2.0,2541.0,3940.0,3942.0] || -> equal(sk2,sk1)**. % 1.83/2.03 3947[9:MRR:3946.0,2557.0] || -> . % 1.83/2.03 3948[9:Spt:3947.0,2611.0,3944.0] || -> neq(sk2,sk1)*. % 1.83/2.03 3949[9:Spt:3947.0,2611.1] || -> ssItem(sk5)*. % 1.83/2.03 3951[9:MRR:2690.0,3948.0] || -> equal(cons(sk5,sk1),sk1)**. % 1.83/2.03 3966[9:SpL:3951.0,515.1] ssItem(sk5) || equal(sk1,sk1)* -> . % 1.83/2.03 3969[9:Obv:3966.1] ssItem(sk5) || -> . % 1.83/2.03 3970[9:SSi:3969.0,3949.0] || -> . % 1.83/2.03 3980[8:Spt:3970.0,227.0,3942.0] || strictorderP(sk2)* -> . % 1.83/2.03 3981[8:Spt:3970.0,227.1] || -> equal(app(app(skaf61(sk2),cons(skaf59(sk2),skaf62(sk2))),cons(skaf60(sk2),skaf63(sk2))),sk2)**. % 1.83/2.03 3989[9:Spt:226.0] || -> totalorderP(sk2)*. % 1.83/2.03 3991[10:Spt:2611.0] || neq(sk2,sk1)* -> . % 1.83/2.03 3992[10:Res:440.2,3991.0] ssList(sk2) || -> equal(sk2,sk1)**. % 1.83/2.03 3993[10:SSi:3992.0,2.0,2541.0,3940.0,3989.0] || -> equal(sk2,sk1)**. % 1.83/2.03 3994[10:MRR:3993.0,2557.0] || -> . % 1.83/2.03 3995[10:Spt:3994.0,2611.0,3991.0] || -> neq(sk2,sk1)*. % 1.83/2.03 3996[10:Spt:3994.0,2611.1] || -> ssItem(sk5)*. % 1.83/2.03 3998[10:MRR:2690.0,3995.0] || -> equal(cons(sk5,sk1),sk1)**. % 1.83/2.03 4011[10:SpL:3998.0,515.1] ssItem(sk5) || equal(sk1,sk1)* -> . % 1.83/2.03 4014[10:Obv:4011.1] ssItem(sk5) || -> . % 1.83/2.03 4015[10:SSi:4014.0,3996.0] || -> . % 1.83/2.03 4025[9:Spt:4015.0,226.0,3989.0] || totalorderP(sk2)* -> . % 1.83/2.03 4026[9:Spt:4015.0,226.1] || -> equal(app(app(skaf56(sk2),cons(skaf54(sk2),skaf57(sk2))),cons(skaf55(sk2),skaf58(sk2))),sk2)**. % 1.83/2.03 4034[10:Spt:2611.0] || neq(sk2,sk1)* -> . % 1.83/2.03 4035[10:Res:440.2,4034.0] ssList(sk2) || -> equal(sk2,sk1)**. % 1.83/2.03 4036[10:SSi:4035.0,2.0,2541.0,3940.0] || -> equal(sk2,sk1)**. % 1.83/2.03 4037[10:MRR:4036.0,2557.0] || -> . % 1.83/2.03 4038[10:Spt:4037.0,2611.0,4034.0] || -> neq(sk2,sk1)*. % 1.83/2.03 4039[10:Spt:4037.0,2611.1] || -> ssItem(sk5)*. % 1.83/2.03 4041[10:MRR:2690.0,4038.0] || -> equal(cons(sk5,sk1),sk1)**. % 1.83/2.03 4054[10:SpL:4041.0,515.1] ssItem(sk5) || equal(sk1,sk1)* -> . % 1.83/2.06 4057[10:Obv:4054.1] ssItem(sk5) || -> . % 1.83/2.06 4058[10:SSi:4057.0,4039.0] || -> . % 1.83/2.06 4068[7:Spt:4058.0,285.0,3940.0] || cyclefreeP(sk2)* -> . % 1.83/2.06 4069[7:Spt:4058.0,285.1] || -> leq(skaf50(sk2),skaf49(sk2))*. % 1.83/2.06 4072[8:Spt:226.0] || -> totalorderP(sk2)*. % 1.83/2.06 4074[9:Spt:227.0] || -> strictorderP(sk2)*. % 1.83/2.06 4076[10:Spt:2611.0] || neq(sk2,sk1)* -> . % 1.83/2.06 4077[10:Res:440.2,4076.0] ssList(sk2) || -> equal(sk2,sk1)**. % 1.83/2.06 4078[10:SSi:4077.0,2.0,2541.0,4072.0,4074.0] || -> equal(sk2,sk1)**. % 1.83/2.06 4079[10:MRR:4078.0,2557.0] || -> . % 1.83/2.06 4080[10:Spt:4079.0,2611.0,4076.0] || -> neq(sk2,sk1)*. % 1.83/2.06 4081[10:Spt:4079.0,2611.1] || -> ssItem(sk5)*. % 1.83/2.06 4083[10:MRR:2690.0,4080.0] || -> equal(cons(sk5,sk1),sk1)**. % 1.83/2.06 4096[10:SpL:4083.0,515.1] ssItem(sk5) || equal(sk1,sk1)* -> . % 1.83/2.06 4099[10:Obv:4096.1] ssItem(sk5) || -> . % 1.83/2.06 4100[10:SSi:4099.0,4081.0] || -> . % 1.83/2.06 4110[9:Spt:4100.0,227.0,4074.0] || strictorderP(sk2)* -> . % 1.83/2.06 4111[9:Spt:4100.0,227.1] || -> equal(app(app(skaf61(sk2),cons(skaf59(sk2),skaf62(sk2))),cons(skaf60(sk2),skaf63(sk2))),sk2)**. % 1.83/2.06 4119[10:Spt:2611.0] || neq(sk2,sk1)* -> . % 1.83/2.06 4120[10:Res:440.2,4119.0] ssList(sk2) || -> equal(sk2,sk1)**. % 1.83/2.06 4121[10:SSi:4120.0,2.0,2541.0,4072.0] || -> equal(sk2,sk1)**. % 1.83/2.06 4122[10:MRR:4121.0,2557.0] || -> . % 1.83/2.06 4123[10:Spt:4122.0,2611.0,4119.0] || -> neq(sk2,sk1)*. % 1.83/2.06 4124[10:Spt:4122.0,2611.1] || -> ssItem(sk5)*. % 1.83/2.06 4126[10:MRR:2690.0,4123.0] || -> equal(cons(sk5,sk1),sk1)**. % 1.83/2.06 4139[10:SpL:4126.0,515.1] ssItem(sk5) || equal(sk1,sk1)* -> . % 1.83/2.06 4142[10:Obv:4139.1] ssItem(sk5) || -> . % 1.83/2.06 4143[10:SSi:4142.0,4124.0] || -> . % 1.83/2.06 4153[8:Spt:4143.0,226.0,4072.0] || totalorderP(sk2)* -> . % 1.83/2.06 4154[8:Spt:4143.0,226.1] || -> equal(app(app(skaf56(sk2),cons(skaf54(sk2),skaf57(sk2))),cons(skaf55(sk2),skaf58(sk2))),sk2)**. % 1.83/2.06 4162[9:Spt:227.0] || -> strictorderP(sk2)*. % 1.83/2.06 4164[10:Spt:2611.0] || neq(sk2,sk1)* -> . % 1.83/2.06 4165[10:Res:440.2,4164.0] ssList(sk2) || -> equal(sk2,sk1)**. % 1.83/2.06 4166[10:SSi:4165.0,2.0,2541.0,4162.0] || -> equal(sk2,sk1)**. % 1.83/2.06 4167[10:MRR:4166.0,2557.0] || -> . % 1.83/2.06 4168[10:Spt:4167.0,2611.0,4164.0] || -> neq(sk2,sk1)*. % 1.83/2.06 4169[10:Spt:4167.0,2611.1] || -> ssItem(sk5)*. % 1.83/2.06 4171[10:MRR:2690.0,4168.0] || -> equal(cons(sk5,sk1),sk1)**. % 1.83/2.06 4184[10:SpL:4171.0,515.1] ssItem(sk5) || equal(sk1,sk1)* -> . % 1.83/2.06 4187[10:Obv:4184.1] ssItem(sk5) || -> . % 1.83/2.06 4188[10:SSi:4187.0,4169.0] || -> . % 1.83/2.06 4198[9:Spt:4188.0,227.0,4162.0] || strictorderP(sk2)* -> . % 1.83/2.06 4199[9:Spt:4188.0,227.1] || -> equal(app(app(skaf61(sk2),cons(skaf59(sk2),skaf62(sk2))),cons(skaf60(sk2),skaf63(sk2))),sk2)**. % 1.83/2.06 4207[10:Spt:2611.0] || neq(sk2,sk1)* -> . % 1.83/2.06 4208[10:Res:440.2,4207.0] ssList(sk2) || -> equal(sk2,sk1)**. % 1.83/2.06 4209[10:SSi:4208.0,2.0,2541.0] || -> equal(sk2,sk1)**. % 1.83/2.06 4210[10:MRR:4209.0,2557.0] || -> . % 1.83/2.06 4211[10:Spt:4210.0,2611.0,4207.0] || -> neq(sk2,sk1)*. % 1.83/2.06 4212[10:Spt:4210.0,2611.1] || -> ssItem(sk5)*. % 1.83/2.06 4214[10:MRR:2690.0,4211.0] || -> equal(cons(sk5,sk1),sk1)**. % 1.83/2.06 4227[10:SpL:4214.0,515.1] ssItem(sk5) || equal(sk1,sk1)* -> . % 1.83/2.06 4230[10:Obv:4227.1] ssItem(sk5) || -> . % 1.83/2.06 4231[10:SSi:4230.0,4212.0] || -> . % 1.83/2.06 4241[4:Spt:4231.0,477.5,2542.0] || equal(nil,sk1)** -> . % 1.83/2.06 4242[4:Spt:4231.0,477.0,477.1,477.2,477.3,477.4] ssList(u) || equal(hd(u),hd(sk1))* equal(tl(u),tl(sk1)) -> equal(u,sk1) equal(nil,u). % 1.83/2.06 4290[5:Spt:200.0] || neq(sk2,nil)* -> . % 1.83/2.06 4332[5:Res:345.2,4290.0] ssList(nil) || -> equal(nil,sk2)**. % 1.83/2.06 4333[5:SSi:4332.0,20.0,19.0,18.0,17.0,16.0,15.0,14.0,13.0] || -> equal(nil,sk2)**. % 1.83/2.06 4334[5:MRR:4333.0,204.0] || -> . % 1.83/2.06 4335[5:Spt:4334.0,200.0,4290.0] || -> neq(sk2,nil)*. % 1.83/2.06 4336[5:Spt:4334.0,200.1] || -> ssItem(sk5)*. % 1.83/2.06 4337[5:MRR:201.0,4335.0] || -> memberP(sk2,sk5)*. % 1.83/2.06 4338[5:MRR:205.0,4335.0] || -> equal(cons(sk5,nil),sk1)**. % 1.83/2.06 4630[5:SpL:4338.0,7.2] ssItem(sk5) || memberP(sk2,sk5)* equal(sk1,sk1) -> . % 1.83/2.06 4632[5:Obv:4630.2] ssItem(sk5) || memberP(sk2,sk5)* -> . % 1.83/2.06 4633[5:SSi:4632.0,4336.0] || memberP(sk2,sk5)* -> . % 1.83/2.06 4634[5:MRR:4633.0,4337.0] || -> . % 1.83/2.06 % SZS output end Refutation % 1.83/2.06 Formulae used in the proof : co1_1 co1_2 co1_5 co1_6 co1_7 co1_8 co1_9 co1_10 co1_11 co1_12 clause1 clause2 clause3 clause4 clause5 clause6 clause7 clause8 clause72 clause87 clause88 clause99 clause100 clause102 clause163 clause164 clause165 clause166 clause177 % 1.83/2.06 %------------------------------------------------------------------------------