%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : SWC386+1 : TPTP v8.1.0. Released v2.4.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n028.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:44 EDT 2022 % Result : Theorem 1.36s 1.55s % Output : Refutation 1.36s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : SWC386+1 : TPTP v8.1.0. Released v2.4.0. % 0.11/0.12 % Command : run_spass %d %s % 0.12/0.33 % Computer : n028.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 600 % 0.12/0.33 % DateTime : Sun Jun 12 20:41:21 EDT 2022 % 0.12/0.33 % CPUTime : % 1.36/1.55 % 1.36/1.55 SPASS V 3.9 % 1.36/1.55 SPASS beiseite: Proof found. % 1.36/1.55 % SZS status Theorem % 1.36/1.55 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 1.36/1.55 SPASS derived 2468 clauses, backtracked 1431 clauses, performed 41 splits and kept 2783 clauses. % 1.36/1.55 SPASS allocated 100169 KBytes. % 1.36/1.55 SPASS spent 0:00:01.21 on the problem. % 1.36/1.55 0:00:00.04 for the input. % 1.36/1.55 0:00:00.07 for the FLOTTER CNF translation. % 1.36/1.55 0:00:00.02 for inferences. % 1.36/1.55 0:00:00.02 for the backtracking. % 1.36/1.55 0:00:00.88 for the reduction. % 1.36/1.55 % 1.36/1.55 % 1.36/1.55 Here is a proof with depth 6, length 242 : % 1.36/1.55 % SZS output start Refutation % 1.36/1.55 1[0:Inp] || -> ssList(skc5)*. % 1.36/1.55 2[0:Inp] || -> ssList(skc4)*. % 1.36/1.55 3[0:Inp] || -> ssItem(skc7)*. % 1.36/1.55 4[0:Inp] || -> ssItem(skc6)*. % 1.36/1.55 5[0:Inp] || -> ssList(nil)*. % 1.36/1.55 6[0:Inp] || -> cyclefreeP(nil)*. % 1.36/1.55 7[0:Inp] || -> totalorderP(nil)*. % 1.36/1.55 8[0:Inp] || -> strictorderP(nil)*. % 1.36/1.55 9[0:Inp] || -> totalorderedP(nil)*. % 1.36/1.55 10[0:Inp] || -> strictorderedP(nil)*. % 1.36/1.55 11[0:Inp] || -> duplicatefreeP(nil)*. % 1.36/1.55 12[0:Inp] || -> equalelemsP(nil)*. % 1.36/1.55 13[0:Inp] || -> ssItem(skf47(u))*. % 1.36/1.55 51[0:Inp] || -> ssItem(skf44(u,v))*. % 1.36/1.55 52[0:Inp] || equal(skc7,skc6)** -> . % 1.36/1.55 59[0:Inp] || -> SkP1(u,v)* equal(nil,v). % 1.36/1.55 68[0:Inp] || SkP0(skc5,skc4)* -> equal(nil,skc5). % 1.36/1.55 69[0:Inp] || SkP0(skc5,skc4)* -> equal(nil,skc4). % 1.36/1.55 70[0:Inp] || SkP1(skc4,skc5) -> neq(skc5,nil)*. % 1.36/1.55 71[0:Inp] || equal(nil,u) -> SkP1(u,v)*. % 1.36/1.55 72[0:Inp] ssItem(u) || memberP(nil,u)* -> . % 1.36/1.55 73[0:Inp] ssItem(u) || -> cyclefreeP(cons(u,nil))*. % 1.36/1.55 74[0:Inp] ssItem(u) || -> totalorderP(cons(u,nil))*. % 1.36/1.55 75[0:Inp] ssItem(u) || -> strictorderP(cons(u,nil))*. % 1.36/1.55 76[0:Inp] ssItem(u) || -> totalorderedP(cons(u,nil))*. % 1.36/1.55 77[0:Inp] ssItem(u) || -> strictorderedP(cons(u,nil))*. % 1.36/1.55 78[0:Inp] ssItem(u) || -> duplicatefreeP(cons(u,nil))*. % 1.36/1.55 79[0:Inp] ssItem(u) || -> equalelemsP(cons(u,nil))*. % 1.36/1.55 81[0:Inp] || -> SkP0(u,v) memberP(u,skf44(u,v))*. % 1.36/1.55 82[0:Inp] ssList(u) || -> equal(app(nil,u),u)**. % 1.36/1.55 88[0:Inp] || -> SkP0(u,v) equal(cons(skf44(u,v),nil),v)**. % 1.36/1.55 89[0:Inp] ssList(u) || -> cyclefreeP(u) leq(skf53(u),skf52(u))*. % 1.36/1.55 91[0:Inp] ssList(u) || -> duplicatefreeP(u) equal(skf78(u),skf77(u))**. % 1.36/1.55 92[0:Inp] ssItem(u) ssList(v) || -> ssList(cons(u,v))*. % 1.36/1.55 108[0:Inp] ssList(u) singletonP(u) || -> equal(cons(skf47(u),nil),u)**. % 1.36/1.55 111[0:Inp] ssItem(u) ssList(v) || equal(cons(u,v),nil)** -> . % 1.36/1.55 112[0:Inp] ssItem(u) ssList(v) || -> equal(hd(cons(u,v)),u)**. % 1.36/1.55 122[0:Inp] ssList(u) ssItem(v) || equal(cons(v,nil),u)* -> singletonP(u)*. % 1.36/1.55 123[0:Inp] ssList(u) ssList(v) || equal(v,u) neq(v,u)* -> . % 1.36/1.55 134[0:Inp] ssList(u) ssList(v) || -> equal(nil,v) equal(hd(app(v,u)),hd(v))**. % 1.36/1.55 137[0:Inp] ssItem(u) || memberP(skc5,u) SkP1(skc4,skc5) equal(cons(u,nil),skc4)** -> . % 1.36/1.55 175[0:Inp] ssList(u) || -> strictorderedP(u) equal(app(app(skf74(u),cons(skf72(u),skf75(u))),cons(skf73(u),skf76(u))),u)**. % 1.36/1.55 176[0:Inp] ssList(u) || -> totalorderedP(u) equal(app(app(skf69(u),cons(skf67(u),skf70(u))),cons(skf68(u),skf71(u))),u)**. % 1.36/1.55 177[0:Inp] ssList(u) || -> strictorderP(u) equal(app(app(skf64(u),cons(skf62(u),skf65(u))),cons(skf63(u),skf66(u))),u)**. % 1.36/1.55 178[0:Inp] ssList(u) || -> totalorderP(u) equal(app(app(skf59(u),cons(skf57(u),skf60(u))),cons(skf58(u),skf61(u))),u)**. % 1.36/1.55 189[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). % 1.36/1.55 198[0:Rew:69.1,68.1] || SkP0(skc5,skc4)* -> equal(skc5,skc4). % 1.36/1.55 220[0:Res:2.0,178.0] || -> totalorderP(skc4) equal(app(app(skf59(skc4),cons(skf57(skc4),skf60(skc4))),cons(skf58(skc4),skf61(skc4))),skc4)**. % 1.36/1.55 221[0:Res:2.0,177.0] || -> strictorderP(skc4) equal(app(app(skf64(skc4),cons(skf62(skc4),skf65(skc4))),cons(skf63(skc4),skf66(skc4))),skc4)**. % 1.36/1.55 222[0:Res:2.0,176.0] || -> totalorderedP(skc4) equal(app(app(skf69(skc4),cons(skf67(skc4),skf70(skc4))),cons(skf68(skc4),skf71(skc4))),skc4)**. % 1.36/1.55 223[0:Res:2.0,175.0] || -> strictorderedP(skc4) equal(app(app(skf74(skc4),cons(skf72(skc4),skf75(skc4))),cons(skf73(skc4),skf76(skc4))),skc4)**. % 1.36/1.55 246[0:Res:2.0,134.0] ssList(u) || -> equal(nil,skc4) equal(hd(app(skc4,u)),hd(skc4))**. % 1.36/1.55 250[0:Res:2.0,123.0] ssList(u) || equal(skc4,u) neq(skc4,u)* -> . % 1.36/1.55 253[0:Res:2.0,108.1] singletonP(skc4) || -> equal(cons(skf47(skc4),nil),skc4)**. % 1.36/1.55 257[0:Res:2.0,112.0] ssItem(u) || -> equal(hd(cons(u,skc4)),u)**. % 1.36/1.55 266[0:Res:2.0,89.0] || -> cyclefreeP(skc4) leq(skf53(skc4),skf52(skc4))*. % 1.36/1.55 268[0:Res:2.0,91.0] || -> duplicatefreeP(skc4) equal(skf78(skc4),skf77(skc4))**. % 1.36/1.55 269[0:Res:2.0,92.0] ssItem(u) || -> ssList(cons(u,skc4))*. % 1.36/1.55 287[0:Res:2.0,189.1] ssList(u) || equal(tl(skc4),tl(u))* equal(hd(skc4),hd(u)) -> equal(nil,u) equal(skc4,u) equal(nil,skc4). % 1.36/1.55 322[0:Res:2.0,122.1] ssItem(u) || equal(cons(u,nil),skc4)** -> singletonP(skc4). % 1.36/1.55 417[0:Res:1.0,134.0] ssList(u) || -> equal(nil,skc5) equal(hd(app(skc5,u)),hd(skc5))**. % 1.36/1.55 458[0:Res:1.0,189.1] ssList(u) || equal(tl(skc5),tl(u))* equal(hd(skc5),hd(u)) -> equal(nil,u) equal(skc5,u) equal(nil,skc5). % 1.36/1.55 550[1:Spt:417.0,417.2] ssList(u) || -> equal(hd(app(skc5,u)),hd(skc5))**. % 1.36/1.55 552[2:Spt:246.0,246.2] ssList(u) || -> equal(hd(app(skc4,u)),hd(skc4))**. % 1.36/1.55 558[3:Spt:458.5] || -> equal(nil,skc5)**. % 1.36/1.55 590[3:Rew:558.0,79.1] ssItem(u) || -> equalelemsP(cons(u,skc5))*. % 1.36/1.55 591[3:Rew:558.0,78.1] ssItem(u) || -> duplicatefreeP(cons(u,skc5))*. % 1.36/1.55 592[3:Rew:558.0,77.1] ssItem(u) || -> strictorderedP(cons(u,skc5))*. % 1.36/1.55 593[3:Rew:558.0,76.1] ssItem(u) || -> totalorderedP(cons(u,skc5))*. % 1.36/1.55 594[3:Rew:558.0,75.1] ssItem(u) || -> strictorderP(cons(u,skc5))*. % 1.36/1.55 595[3:Rew:558.0,74.1] ssItem(u) || -> totalorderP(cons(u,skc5))*. % 1.36/1.55 596[3:Rew:558.0,73.1] ssItem(u) || -> cyclefreeP(cons(u,skc5))*. % 1.36/1.55 634[3:Rew:558.0,12.0] || -> equalelemsP(skc5)*. % 1.36/1.55 635[3:Rew:558.0,11.0] || -> duplicatefreeP(skc5)*. % 1.36/1.55 636[3:Rew:558.0,10.0] || -> strictorderedP(skc5)*. % 1.36/1.55 637[3:Rew:558.0,9.0] || -> totalorderedP(skc5)*. % 1.36/1.55 638[3:Rew:558.0,8.0] || -> strictorderP(skc5)*. % 1.36/1.55 639[3:Rew:558.0,7.0] || -> totalorderP(skc5)*. % 1.36/1.55 640[3:Rew:558.0,6.0] || -> cyclefreeP(skc5)*. % 1.36/1.55 656[3:Rew:558.0,72.1] ssItem(u) || memberP(skc5,u)* -> . % 1.36/1.55 659[3:Rew:558.0,82.1] ssList(u) || -> equal(app(skc5,u),u)**. % 1.36/1.55 717[3:Rew:659.1,550.1] ssList(u) || -> equal(hd(u),hd(skc5))*. % 1.36/1.55 763[4:Spt:198.1] || -> equal(skc5,skc4)**. % 1.36/1.55 772[4:Rew:763.0,590.1] ssItem(u) || -> equalelemsP(cons(u,skc4))*. % 1.36/1.55 773[4:Rew:763.0,591.1] ssItem(u) || -> duplicatefreeP(cons(u,skc4))*. % 1.36/1.55 774[4:Rew:763.0,592.1] ssItem(u) || -> strictorderedP(cons(u,skc4))*. % 1.36/1.55 775[4:Rew:763.0,593.1] ssItem(u) || -> totalorderedP(cons(u,skc4))*. % 1.36/1.55 776[4:Rew:763.0,594.1] ssItem(u) || -> strictorderP(cons(u,skc4))*. % 1.36/1.55 777[4:Rew:763.0,595.1] ssItem(u) || -> totalorderP(cons(u,skc4))*. % 1.36/1.55 778[4:Rew:763.0,596.1] ssItem(u) || -> cyclefreeP(cons(u,skc4))*. % 1.36/1.55 889[4:Rew:763.0,717.1] ssList(u) || -> equal(hd(u),hd(skc4))*. % 1.36/1.55 1034[4:SpR:257.1,889.1] ssItem(u) ssList(cons(u,skc4)) || -> equal(u,hd(skc4))*. % 1.36/1.55 1036[4:SSi:1034.1,269.1,772.1,773.1,774.1,775.1,776.1,777.1,778.1] ssItem(u) || -> equal(u,hd(skc4))*. % 1.36/1.55 1102[4:SpR:1036.1,1036.1] ssItem(u) ssItem(v) || -> equal(v,u)*. % 1.36/1.55 1165[4:EmS:1102.0,3.0] ssItem(u) || -> equal(u,skc7)*. % 1.36/1.55 1187[4:EmS:1165.0,4.0] || -> equal(skc7,skc6)**. % 1.36/1.55 1188[4:MRR:1187.0,52.0] || -> . % 1.36/1.55 1326[4:Spt:1188.0,198.1,763.0] || equal(skc5,skc4)** -> . % 1.36/1.55 1327[4:Spt:1188.0,198.0] || SkP0(skc5,skc4)* -> . % 1.36/1.55 1474[3:Res:81.1,656.1] ssItem(skf44(skc5,u)) || -> SkP0(skc5,u)*. % 1.36/1.55 1475[3:SSi:1474.0,51.0,640.0,639.0,638.0,637.0,636.0,635.0,634.0,1.0] || -> SkP0(skc5,u)*. % 1.36/1.55 1476[4:UnC:1475.0,1327.0] || -> . % 1.36/1.55 1478[3:Spt:1476.0,458.5,558.0] || equal(nil,skc5)** -> . % 1.36/1.55 1479[3:Spt:1476.0,458.0,458.1,458.2,458.3,458.4] ssList(u) || equal(tl(skc5),tl(u))* equal(hd(skc5),hd(u)) -> equal(nil,u) equal(skc5,u). % 1.36/1.55 1498[4:Spt:287.5] || -> equal(nil,skc4)**. % 1.36/1.55 1541[4:Rew:1498.0,73.1] ssItem(u) || -> cyclefreeP(cons(u,skc4))*. % 1.36/1.55 1542[4:Rew:1498.0,74.1] ssItem(u) || -> totalorderP(cons(u,skc4))*. % 1.36/1.55 1543[4:Rew:1498.0,75.1] ssItem(u) || -> strictorderP(cons(u,skc4))*. % 1.36/1.55 1544[4:Rew:1498.0,76.1] ssItem(u) || -> totalorderedP(cons(u,skc4))*. % 1.36/1.55 1545[4:Rew:1498.0,77.1] ssItem(u) || -> strictorderedP(cons(u,skc4))*. % 1.36/1.55 1546[4:Rew:1498.0,78.1] ssItem(u) || -> duplicatefreeP(cons(u,skc4))*. % 1.36/1.55 1547[4:Rew:1498.0,79.1] ssItem(u) || -> equalelemsP(cons(u,skc4))*. % 1.36/1.55 1576[4:Rew:1498.0,82.1] ssList(u) || -> equal(app(skc4,u),u)**. % 1.36/1.55 1629[4:Rew:1576.1,552.1] ssList(u) || -> equal(hd(u),hd(skc4))*. % 1.36/1.55 1698[4:SpR:1629.1,257.1] ssList(cons(u,skc4)) ssItem(u) || -> equal(hd(skc4),u)*. % 1.36/1.55 1707[4:SSi:1698.0,269.1,1541.1,1542.1,1543.1,1544.1,1545.1,1546.1,1547.1] ssItem(u) || -> equal(hd(skc4),u)*. % 1.36/1.55 1724[4:SpR:1707.1,1707.1] ssItem(u) ssItem(v) || -> equal(u,v)*. % 1.36/1.55 1914[4:EmS:1724.0,3.0] ssItem(u) || -> equal(skc7,u)*. % 1.36/1.55 1937[4:EmS:1914.0,4.0] || -> equal(skc7,skc6)**. % 1.36/1.55 1938[4:MRR:1937.0,52.0] || -> . % 1.36/1.55 2122[4:Spt:1938.0,287.5,1498.0] || equal(nil,skc4)** -> . % 1.36/1.55 2123[4:Spt:1938.0,287.0,287.1,287.2,287.3,287.4] ssList(u) || equal(tl(skc4),tl(u))* equal(hd(skc4),hd(u)) -> equal(nil,u) equal(skc4,u). % 1.36/1.55 2129[4:MRR:69.1,2122.0] || SkP0(skc5,skc4)* -> . % 1.36/1.55 2148[5:Spt:137.0,137.1,137.3] ssItem(u) || memberP(skc5,u) equal(cons(u,nil),skc4)** -> . % 1.36/1.55 2156[6:Spt:222.0] || -> totalorderedP(skc4)*. % 1.36/1.55 2160[7:Spt:223.0] || -> strictorderedP(skc4)*. % 1.36/1.55 2165[8:Spt:266.0] || -> cyclefreeP(skc4)*. % 1.36/1.55 2169[9:Spt:220.0] || -> totalorderP(skc4)*. % 1.36/1.55 2170[10:Spt:221.0] || -> strictorderP(skc4)*. % 1.36/1.55 2183[11:Spt:268.0] || -> duplicatefreeP(skc4)*. % 1.36/1.55 2208[0:Res:81.1,72.1] ssItem(skf44(nil,u)) || -> SkP0(nil,u)*. % 1.36/1.55 2209[0:SSi:2208.0,51.0,12.0,11.0,10.0,9.0,8.0,7.0,6.0,5.0] || -> SkP0(nil,u)*. % 1.36/1.55 2248[0:SpR:88.1,79.1] ssItem(skf44(u,v)) || -> SkP0(u,v)* equalelemsP(v). % 1.36/1.55 2249[0:SpR:88.1,78.1] ssItem(skf44(u,v)) || -> SkP0(u,v)* duplicatefreeP(v). % 1.36/1.55 2250[0:SpR:88.1,77.1] ssItem(skf44(u,v)) || -> SkP0(u,v)* strictorderedP(v). % 1.36/1.55 2251[0:SpR:88.1,76.1] ssItem(skf44(u,v)) || -> SkP0(u,v)* totalorderedP(v). % 1.36/1.55 2252[0:SpR:88.1,75.1] ssItem(skf44(u,v)) || -> SkP0(u,v)* strictorderP(v). % 1.36/1.55 2253[0:SpR:88.1,74.1] ssItem(skf44(u,v)) || -> SkP0(u,v)* totalorderP(v). % 1.36/1.55 2254[0:SpR:88.1,73.1] ssItem(skf44(u,v)) || -> SkP0(u,v)* cyclefreeP(v). % 1.36/1.55 2257[0:SSi:2248.0,51.0] || -> SkP0(u,v)* equalelemsP(v). % 1.36/1.55 2258[0:SSi:2249.0,51.0] || -> SkP0(u,v)* duplicatefreeP(v). % 1.36/1.55 2259[0:SSi:2250.0,51.0] || -> SkP0(u,v)* strictorderedP(v). % 1.36/1.55 2260[0:SSi:2251.0,51.0] || -> SkP0(u,v)* totalorderedP(v). % 1.36/1.55 2261[0:SSi:2252.0,51.0] || -> SkP0(u,v)* strictorderP(v). % 1.36/1.55 2262[0:SSi:2253.0,51.0] || -> SkP0(u,v)* totalorderP(v). % 1.36/1.55 2263[0:SSi:2254.0,51.0] || -> SkP0(u,v)* cyclefreeP(v). % 1.36/1.55 2266[4:Res:2257.0,2129.0] || -> equalelemsP(skc4)*. % 1.36/1.55 2268[4:Res:2258.0,2129.0] || -> duplicatefreeP(skc4)*. % 1.36/1.55 2269[4:Res:2259.0,2129.0] || -> strictorderedP(skc4)*. % 1.36/1.55 2270[4:Res:2260.0,2129.0] || -> totalorderedP(skc4)*. % 1.36/1.55 2271[4:Res:2261.0,2129.0] || -> strictorderP(skc4)*. % 1.36/1.55 2272[4:Res:2262.0,2129.0] || -> totalorderP(skc4)*. % 1.36/1.55 2273[4:Res:2263.0,2129.0] || -> cyclefreeP(skc4)*. % 1.36/1.55 2275[0:SpL:88.1,322.1] ssItem(skf44(u,v)) || equal(v,skc4) -> SkP0(u,v)* singletonP(skc4). % 1.36/1.55 2276[0:SSi:2275.0,51.0] || equal(u,skc4) -> SkP0(v,u)* singletonP(skc4). % 1.36/1.55 2277[12:Spt:2276.0,2276.1] || equal(u,skc4) -> SkP0(v,u)*. % 1.36/1.55 2278[12:Res:2277.1,2129.0] || equal(skc4,skc4)* -> . % 1.36/1.55 2279[12:Obv:2278.0] || -> . % 1.36/1.55 2280[12:Spt:2279.0,2276.2] || -> singletonP(skc4)*. % 1.36/1.55 2281[12:MRR:253.0,2280.0] || -> equal(cons(skf47(skc4),nil),skc4)**. % 1.36/1.55 2291[12:SpL:2281.0,2148.2] ssItem(skf47(skc4)) || memberP(skc5,skf47(skc4))* equal(skc4,skc4) -> . % 1.36/1.55 2292[12:Obv:2291.2] ssItem(skf47(skc4)) || memberP(skc5,skf47(skc4))* -> . % 1.36/1.55 2293[12:SSi:2292.0,13.0,2.0,2156.0,2160.0,2165.0,2169.0,2170.0,2183.0,2266.0,2280.0] || memberP(skc5,skf47(skc4))* -> . % 1.36/1.55 2333[0:SpL:88.1,111.2] ssItem(skf44(u,v)) ssList(nil) || equal(v,nil) -> SkP0(u,v)*. % 1.36/1.55 2334[0:SSi:2333.1,2333.0,12.0,11.0,10.0,9.0,8.0,7.0,6.0,5.0,51.0] || equal(u,nil) -> SkP0(v,u)*. % 1.36/1.55 2433[12:SpR:2281.0,112.2] ssItem(skf47(skc4)) ssList(nil) || -> equal(skf47(skc4),hd(skc4))**. % 1.36/1.55 2435[0:SpR:88.1,112.2] ssItem(skf44(u,v)) ssList(nil) || -> SkP0(u,v) equal(skf44(u,v),hd(v))**. % 1.36/1.55 2437[12:SSi:2433.1,2433.0,12.0,11.0,10.0,9.0,8.0,7.0,6.0,5.0,13.0,2.0,2156.0,2160.0,2165.0,2169.0,2170.0,2183.0,2266.0,2280.0] || -> equal(skf47(skc4),hd(skc4))**. % 1.36/1.55 2439[12:Rew:2437.0,2293.0] || memberP(skc5,hd(skc4))* -> . % 1.36/1.55 2443[0:SSi:2435.1,2435.0,12.0,11.0,10.0,9.0,8.0,7.0,6.0,5.0,51.0] || -> SkP0(u,v) equal(skf44(u,v),hd(v))**. % 1.36/1.55 2444[0:Rew:2443.1,81.1] || -> SkP0(u,v) memberP(u,hd(v))*. % 1.36/1.55 2496[12:Res:2444.1,2439.0] || -> SkP0(skc5,skc4)*. % 1.36/1.55 2497[12:MRR:2496.0,2129.0] || -> . % 1.36/1.55 2498[11:Spt:2497.0,268.0,2183.0] || duplicatefreeP(skc4)* -> . % 1.36/1.55 2499[11:Spt:2497.0,268.1] || -> equal(skf78(skc4),skf77(skc4))**. % 1.36/1.55 2500[11:MRR:2498.0,2268.0] || -> . % 1.36/1.55 2508[10:Spt:2500.0,221.0,2170.0] || strictorderP(skc4)* -> . % 1.36/1.55 2509[10:Spt:2500.0,221.1] || -> equal(app(app(skf64(skc4),cons(skf62(skc4),skf65(skc4))),cons(skf63(skc4),skf66(skc4))),skc4)**. % 1.36/1.55 2510[10:MRR:2508.0,2271.0] || -> . % 1.36/1.55 2517[9:Spt:2510.0,220.0,2169.0] || totalorderP(skc4)* -> . % 1.36/1.55 2518[9:Spt:2510.0,220.1] || -> equal(app(app(skf59(skc4),cons(skf57(skc4),skf60(skc4))),cons(skf58(skc4),skf61(skc4))),skc4)**. % 1.36/1.55 2519[9:MRR:2517.0,2272.0] || -> . % 1.36/1.55 2523[8:Spt:2519.0,266.0,2165.0] || cyclefreeP(skc4)* -> . % 1.36/1.55 2524[8:Spt:2519.0,266.1] || -> leq(skf53(skc4),skf52(skc4))*. % 1.36/1.55 2525[8:MRR:2523.0,2273.0] || -> . % 1.36/1.55 2533[7:Spt:2525.0,223.0,2160.0] || strictorderedP(skc4)* -> . % 1.36/1.55 2534[7:Spt:2525.0,223.1] || -> equal(app(app(skf74(skc4),cons(skf72(skc4),skf75(skc4))),cons(skf73(skc4),skf76(skc4))),skc4)**. % 1.36/1.55 2535[7:MRR:2533.0,2269.0] || -> . % 1.36/1.55 2544[6:Spt:2535.0,222.0,2156.0] || totalorderedP(skc4)* -> . % 1.36/1.55 2545[6:Spt:2535.0,222.1] || -> equal(app(app(skf69(skc4),cons(skf67(skc4),skf70(skc4))),cons(skf68(skc4),skf71(skc4))),skc4)**. % 1.36/1.55 2546[6:MRR:2544.0,2270.0] || -> . % 1.36/1.55 2553[5:Spt:2546.0,137.2] || SkP1(skc4,skc5)* -> . % 1.36/1.55 2558[5:Res:59.0,2553.0] || -> equal(nil,skc5)**. % 1.36/1.55 2559[5:MRR:2558.0,1478.0] || -> . % 1.36/1.55 2560[2:Spt:2559.0,246.1] || -> equal(nil,skc4)**. % 1.36/1.55 2569[2:Rew:2560.0,71.0] || equal(skc4,u) -> SkP1(u,v)*. % 1.36/1.55 2579[2:Rew:2560.0,12.0] || -> equalelemsP(skc4)*. % 1.36/1.55 2580[2:Rew:2560.0,11.0] || -> duplicatefreeP(skc4)*. % 1.36/1.55 2581[2:Rew:2560.0,10.0] || -> strictorderedP(skc4)*. % 1.36/1.55 2582[2:Rew:2560.0,9.0] || -> totalorderedP(skc4)*. % 1.36/1.55 2583[2:Rew:2560.0,8.0] || -> strictorderP(skc4)*. % 1.36/1.55 2584[2:Rew:2560.0,7.0] || -> totalorderP(skc4)*. % 1.36/1.55 2585[2:Rew:2560.0,6.0] || -> cyclefreeP(skc4)*. % 1.36/1.55 2610[2:Rew:2560.0,2334.0] || equal(u,skc4) -> SkP0(v,u)*. % 1.36/1.55 2655[2:Rew:2560.0,70.1] || SkP1(skc4,skc5) -> neq(skc5,skc4)*. % 1.36/1.55 2745[3:Spt:198.1] || -> equal(skc5,skc4)**. % 1.36/1.55 2900[3:Rew:2745.0,2655.0] || SkP1(skc4,skc4) -> neq(skc5,skc4)*. % 1.36/1.55 2912[3:Rew:2745.0,2900.1] || SkP1(skc4,skc4) -> neq(skc4,skc4)*. % 1.36/1.55 2996[3:Res:2912.1,250.2] ssList(skc4) || SkP1(skc4,skc4)* equal(skc4,skc4) -> . % 1.36/1.55 2998[3:Obv:2996.2] ssList(skc4) || SkP1(skc4,skc4)* -> . % 1.36/1.55 2999[3:SSi:2998.0,2.0,2579.0,2580.0,2581.0,2582.0,2583.0,2584.0,2585.0] || SkP1(skc4,skc4)* -> . % 1.36/1.55 3003[3:Res:2569.1,2999.0] || equal(skc4,skc4)* -> . % 1.36/1.55 3004[3:Obv:3003.0] || -> . % 1.36/1.55 3005[3:Spt:3004.0,198.1,2745.0] || equal(skc5,skc4)** -> . % 1.36/1.55 3006[3:Spt:3004.0,198.0] || SkP0(skc5,skc4)* -> . % 1.36/1.55 3079[3:Res:2610.1,3006.0] || equal(skc4,skc4)* -> . % 1.36/1.55 3080[3:Obv:3079.0] || -> . % 1.36/1.55 3081[1:Spt:3080.0,417.1] || -> equal(nil,skc5)**. % 1.36/1.55 3083[1:Rew:3081.0,6.0] || -> cyclefreeP(skc5)*. % 1.36/1.55 3084[1:Rew:3081.0,7.0] || -> totalorderP(skc5)*. % 1.36/1.55 3085[1:Rew:3081.0,8.0] || -> strictorderP(skc5)*. % 1.36/1.55 3086[1:Rew:3081.0,9.0] || -> totalorderedP(skc5)*. % 1.36/1.55 3087[1:Rew:3081.0,10.0] || -> strictorderedP(skc5)*. % 1.36/1.55 3088[1:Rew:3081.0,11.0] || -> duplicatefreeP(skc5)*. % 1.36/1.55 3089[1:Rew:3081.0,12.0] || -> equalelemsP(skc5)*. % 1.36/1.55 3090[1:Rew:3081.0,2209.0] || -> SkP0(skc5,u)*. % 1.36/1.55 3124[1:MRR:198.0,3090.0] || -> equal(skc5,skc4)**. % 1.36/1.55 3210[1:Rew:3124.0,3081.0] || -> equal(nil,skc4)**. % 1.36/1.55 3211[1:Rew:3124.0,3083.0] || -> cyclefreeP(skc4)*. % 1.36/1.55 3212[1:Rew:3124.0,3084.0] || -> totalorderP(skc4)*. % 1.36/1.55 3213[1:Rew:3124.0,3085.0] || -> strictorderP(skc4)*. % 1.36/1.55 3214[1:Rew:3124.0,3086.0] || -> totalorderedP(skc4)*. % 1.36/1.55 3215[1:Rew:3124.0,3087.0] || -> strictorderedP(skc4)*. % 1.36/1.55 3216[1:Rew:3124.0,3088.0] || -> duplicatefreeP(skc4)*. % 1.36/1.55 3217[1:Rew:3124.0,3089.0] || -> equalelemsP(skc4)*. % 1.36/1.55 3239[1:Rew:3210.0,71.0] || equal(skc4,u) -> SkP1(u,v)*. % 1.36/1.55 3241[1:Rew:3124.0,70.1,3210.0,70.1,3124.0,70.0] || SkP1(skc4,skc4) -> neq(skc4,skc4)*. % 1.36/1.55 3447[1:Res:3241.1,250.2] ssList(skc4) || SkP1(skc4,skc4)* equal(skc4,skc4) -> . % 1.36/1.55 3449[1:Obv:3447.2] ssList(skc4) || SkP1(skc4,skc4)* -> . % 1.36/1.55 3450[1:SSi:3449.0,2.0,3211.0,3212.0,3213.0,3214.0,3215.0,3216.0,3217.0] || SkP1(skc4,skc4)* -> . % 1.36/1.55 3454[1:Res:3239.1,3450.0] || equal(skc4,skc4)* -> . % 1.36/1.55 3455[1:Obv:3454.0] || -> . % 1.36/1.55 % SZS output end Refutation % 1.36/1.55 Formulae used in the proof : co1 ax2 ax17 ax60 ax62 ax64 ax66 ax69 ax72 ax74 ax4 ax38 ax59 ax61 ax63 ax65 ax68 ax71 ax73 ax28 ax8 ax13 ax16 ax21 ax23 ax15 ax85 ax12 ax11 ax10 ax9 ax77 % 1.36/1.58 %------------------------------------------------------------------------------