%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : SWC184+1 : TPTP v8.1.0. Released v2.4.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n015.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:02:19 EDT 2022 % Result : Theorem 7.71s 7.89s % Output : Refutation 8.25s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.11 % Problem : SWC184+1 : TPTP v8.1.0. Released v2.4.0. % 0.07/0.12 % Command : run_spass %d %s % 0.13/0.33 % Computer : n015.cluster.edu % 0.13/0.33 % Model : x86_64 x86_64 % 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.33 % Memory : 8042.1875MB % 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.33 % CPULimit : 300 % 0.13/0.33 % WCLimit : 600 % 0.13/0.33 % DateTime : Sun Jun 12 17:20:22 EDT 2022 % 0.13/0.33 % CPUTime : % 7.71/7.89 % 7.71/7.89 SPASS V 3.9 % 7.71/7.89 SPASS beiseite: Proof found. % 7.71/7.89 % SZS status Theorem % 7.71/7.89 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 7.71/7.89 SPASS derived 7594 clauses, backtracked 3163 clauses, performed 40 splits and kept 5755 clauses. % 7.71/7.89 SPASS allocated 109019 KBytes. % 7.71/7.89 SPASS spent 0:00:07.54 on the problem. % 7.71/7.89 0:00:00.04 for the input. % 7.71/7.89 0:00:00.07 for the FLOTTER CNF translation. % 7.71/7.89 0:00:00.07 for inferences. % 7.71/7.89 0:00:00.19 for the backtracking. % 7.71/7.89 0:00:06.98 for the reduction. % 7.71/7.89 % 7.71/7.89 % 7.71/7.89 Here is a proof with depth 8, length 240 : % 7.71/7.89 % SZS output start Refutation % 7.71/7.89 1[0:Inp] || -> ssList(skc11)*. % 7.71/7.89 2[0:Inp] || -> ssList(skc10)*. % 7.71/7.89 3[0:Inp] || -> ssItem(skc9)*. % 7.71/7.89 5[0:Inp] || -> ssList(skc7)*. % 7.71/7.89 6[0:Inp] || -> ssItem(skc13)*. % 7.71/7.89 7[0:Inp] || -> ssItem(skc12)*. % 7.71/7.89 8[0:Inp] || -> ssList(nil)*. % 7.71/7.89 9[0:Inp] || -> cyclefreeP(nil)*. % 7.71/7.89 10[0:Inp] || -> totalorderP(nil)*. % 7.71/7.89 11[0:Inp] || -> strictorderP(nil)*. % 7.71/7.89 12[0:Inp] || -> totalorderedP(nil)*. % 7.71/7.89 13[0:Inp] || -> strictorderedP(nil)*. % 7.71/7.89 14[0:Inp] || -> duplicatefreeP(nil)*. % 7.71/7.89 15[0:Inp] || -> equalelemsP(nil)*. % 7.71/7.89 16[0:Inp] || -> ssItem(skf47(u))*. % 7.71/7.89 54[0:Inp] || -> ssItem(skf44(u,v))*. % 7.71/7.89 55[0:Inp] || equal(skc13,skc12)** -> . % 7.71/7.89 62[0:Inp] || -> memberP(skc11,skc9)* memberP(skc10,skc9). % 7.71/7.89 64[0:Inp] ssList(u) || -> frontsegP(u,u)*. % 7.71/7.89 72[0:Inp] || SkP0(skc8,skc7)* -> equal(nil,skc7). % 7.71/7.89 73[0:Inp] ssItem(u) || memberP(nil,u)* -> . % 7.71/7.89 74[0:Inp] ssItem(u) || -> cyclefreeP(cons(u,nil))*. % 7.71/7.89 75[0:Inp] ssItem(u) || -> totalorderP(cons(u,nil))*. % 7.71/7.89 76[0:Inp] ssItem(u) || -> strictorderP(cons(u,nil))*. % 7.71/7.89 77[0:Inp] ssItem(u) || -> totalorderedP(cons(u,nil))*. % 7.71/7.89 78[0:Inp] ssItem(u) || -> strictorderedP(cons(u,nil))*. % 7.71/7.89 79[0:Inp] ssItem(u) || -> duplicatefreeP(cons(u,nil))*. % 7.71/7.89 80[0:Inp] ssItem(u) || -> equalelemsP(cons(u,nil))*. % 7.71/7.89 83[0:Inp] ssList(u) || -> equal(app(nil,u),u)**. % 7.71/7.89 85[0:Inp] || -> equal(app(app(skc10,cons(skc9,nil)),skc11),skc7)**. % 7.71/7.89 89[0:Inp] ssList(u) || -> ssList(tl(u))* equal(nil,u). % 7.71/7.89 90[0:Inp] || -> SkP0(u,v) equal(cons(skf44(u,v),nil),v)**. % 7.71/7.89 91[0:Inp] ssList(u) || -> cyclefreeP(u) leq(skf53(u),skf52(u))*. % 7.71/7.89 93[0:Inp] ssList(u) || -> duplicatefreeP(u) equal(skf78(u),skf77(u))**. % 7.71/7.89 94[0:Inp] ssItem(u) ssList(v) || -> ssList(cons(u,v))*. % 7.71/7.89 95[0:Inp] ssList(u) ssList(v) || -> ssList(app(v,u))*. % 7.71/7.89 110[0:Inp] ssList(u) singletonP(u) || -> equal(cons(skf47(u),nil),u)**. % 7.71/7.89 113[0:Inp] ssItem(u) ssList(v) || equal(cons(u,v),nil)** -> . % 7.71/7.89 114[0:Inp] ssItem(u) ssList(v) || -> equal(hd(cons(u,v)),u)**. % 7.71/7.89 115[0:Inp] ssItem(u) ssList(v) || -> equal(tl(cons(u,v)),v)**. % 7.71/7.89 121[0:Inp] ssList(u) || -> equal(nil,u) equal(cons(hd(u),tl(u)),u)**. % 7.71/7.89 124[0:Inp] ssList(u) ssItem(v) || equal(cons(v,nil),u)* -> singletonP(u)*. % 7.71/7.89 131[0:Inp] ssItem(u) ssList(v) || -> equal(app(cons(u,nil),v),cons(u,v))**. % 7.71/7.89 133[0:Inp] ssList(u) ssList(v) || equal(app(v,u),nil)** -> equal(nil,v). % 7.71/7.89 136[0:Inp] ssList(u) ssList(v) || -> equal(nil,v) equal(hd(app(v,u)),hd(v))**. % 7.71/7.89 142[0:Inp] ssList(u) ssList(v) || frontsegP(u,v)*+ frontsegP(v,u)* -> equal(v,u). % 7.71/7.89 146[0:Inp] ssList(u) ssList(v) ssList(w) || equal(app(u,w),v)*+ -> frontsegP(v,u)*. % 7.71/7.89 153[0:Inp] ssList(u) ssList(v) ssList(w) || frontsegP(w,v) -> frontsegP(app(w,u),v)*. % 7.71/7.89 157[0:Inp] ssList(u) ssList(v) || -> equal(nil,v) equal(app(tl(v),u),tl(app(v,u)))**. % 7.71/7.89 162[0:Inp] ssList(u) ssList(v) ssList(w) || -> equal(app(app(w,v),u),app(w,app(v,u)))**. % 7.71/7.89 176[0:Inp] ssList(u) || -> strictorderedP(u) equal(app(app(skf74(u),cons(skf72(u),skf75(u))),cons(skf73(u),skf76(u))),u)**. % 7.71/7.89 177[0:Inp] ssList(u) || -> totalorderedP(u) equal(app(app(skf69(u),cons(skf67(u),skf70(u))),cons(skf68(u),skf71(u))),u)**. % 7.71/7.89 178[0:Inp] ssList(u) || -> strictorderP(u) equal(app(app(skf64(u),cons(skf62(u),skf65(u))),cons(skf63(u),skf66(u))),u)**. % 7.71/7.89 179[0:Inp] ssList(u) || -> totalorderP(u) equal(app(app(skf59(u),cons(skf57(u),skf60(u))),cons(skf58(u),skf61(u))),u)**. % 7.71/7.89 190[0:Inp] ssItem(u) ssList(v) ssList(w) ssList(x) || equal(app(x,cons(u,w)),v)*+ -> memberP(v,u)*. % 7.71/7.89 191[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). % 7.71/7.89 222[0:Res:5.0,179.0] || -> totalorderP(skc7) equal(app(app(skf59(skc7),cons(skf57(skc7),skf60(skc7))),cons(skf58(skc7),skf61(skc7))),skc7)**. % 7.71/7.89 223[0:Res:5.0,178.0] || -> strictorderP(skc7) equal(app(app(skf64(skc7),cons(skf62(skc7),skf65(skc7))),cons(skf63(skc7),skf66(skc7))),skc7)**. % 7.71/7.89 224[0:Res:5.0,177.0] || -> totalorderedP(skc7) equal(app(app(skf69(skc7),cons(skf67(skc7),skf70(skc7))),cons(skf68(skc7),skf71(skc7))),skc7)**. % 7.71/7.89 225[0:Res:5.0,176.0] || -> strictorderedP(skc7) equal(app(app(skf74(skc7),cons(skf72(skc7),skf75(skc7))),cons(skf73(skc7),skf76(skc7))),skc7)**. % 7.71/7.89 242[0:Res:5.0,157.0] ssList(u) || -> equal(nil,skc7) equal(app(tl(skc7),u),tl(app(skc7,u)))**. % 7.71/7.89 248[0:Res:5.0,136.0] ssList(u) || -> equal(nil,skc7) equal(hd(app(skc7,u)),hd(skc7))**. % 7.71/7.89 251[0:Res:5.0,133.0] ssList(u) || equal(app(skc7,u),nil)** -> equal(nil,skc7). % 7.71/7.89 254[0:Res:5.0,121.0] || -> equal(nil,skc7) equal(cons(hd(skc7),tl(skc7)),skc7)**. % 7.71/7.89 255[0:Res:5.0,110.1] singletonP(skc7) || -> equal(cons(skf47(skc7),nil),skc7)**. % 7.71/7.89 259[0:Res:5.0,114.0] ssItem(u) || -> equal(hd(cons(u,skc7)),u)**. % 7.71/7.89 268[0:Res:5.0,91.0] || -> cyclefreeP(skc7) leq(skf53(skc7),skf52(skc7))*. % 7.71/7.89 270[0:Res:5.0,93.0] || -> duplicatefreeP(skc7) equal(skf78(skc7),skf77(skc7))**. % 7.71/7.89 271[0:Res:5.0,94.0] ssItem(u) || -> ssList(cons(u,skc7))*. % 7.71/7.89 289[0:Res:5.0,191.1] ssList(u) || equal(tl(skc7),tl(u))* equal(hd(skc7),hd(u)) -> equal(nil,u) equal(skc7,u) equal(nil,skc7). % 7.71/7.89 324[0:Res:5.0,124.1] ssItem(u) || equal(cons(u,nil),skc7)** -> singletonP(skc7). % 7.71/7.89 554[1:Spt:248.0,248.2] ssList(u) || -> equal(hd(app(skc7,u)),hd(skc7))**. % 7.71/7.89 558[2:Spt:242.0,242.2] ssList(u) || -> equal(app(tl(skc7),u),tl(app(skc7,u)))**. % 7.71/7.89 1500[3:Spt:289.5] || -> equal(nil,skc7)**. % 7.71/7.89 1536[3:Rew:1500.0,74.1] ssItem(u) || -> cyclefreeP(cons(u,skc7))*. % 7.71/7.89 1537[3:Rew:1500.0,75.1] ssItem(u) || -> totalorderP(cons(u,skc7))*. % 7.71/7.89 1538[3:Rew:1500.0,76.1] ssItem(u) || -> strictorderP(cons(u,skc7))*. % 7.71/7.89 1539[3:Rew:1500.0,77.1] ssItem(u) || -> totalorderedP(cons(u,skc7))*. % 7.71/7.89 1540[3:Rew:1500.0,78.1] ssItem(u) || -> strictorderedP(cons(u,skc7))*. % 7.71/7.89 1541[3:Rew:1500.0,79.1] ssItem(u) || -> duplicatefreeP(cons(u,skc7))*. % 7.71/7.89 1542[3:Rew:1500.0,80.1] ssItem(u) || -> equalelemsP(cons(u,skc7))*. % 7.71/7.89 1548[3:Rew:1500.0,83.1] ssList(u) || -> equal(app(skc7,u),u)**. % 7.71/7.89 1628[3:Rew:1548.1,554.1] ssList(u) || -> equal(hd(u),hd(skc7))*. % 7.71/7.89 1701[3:SpR:1628.1,259.1] ssList(cons(u,skc7)) ssItem(u) || -> equal(hd(skc7),u)*. % 7.71/7.89 1710[3:SSi:1701.0,271.1,1536.1,1537.1,1538.1,1539.1,1540.1,1541.1,1542.1] ssItem(u) || -> equal(hd(skc7),u)*. % 7.71/7.89 1728[3:SpR:1710.1,1710.1] ssItem(u) ssItem(v) || -> equal(u,v)*. % 7.71/7.89 1919[3:EmS:1728.0,7.0] ssItem(u) || -> equal(skc12,u)*. % 7.71/7.89 1943[3:EmS:1919.0,6.0] || -> equal(skc13,skc12)**. % 7.71/7.89 1945[3:MRR:1943.0,55.0] || -> . % 7.71/7.89 2155[3:Spt:1945.0,289.5,1500.0] || equal(nil,skc7)** -> . % 7.71/7.89 2156[3:Spt:1945.0,289.0,289.1,289.2,289.3,289.4] ssList(u) || equal(tl(skc7),tl(u))* equal(hd(skc7),hd(u)) -> equal(nil,u) equal(skc7,u). % 7.71/7.89 2162[3:MRR:72.1,2155.0] || SkP0(skc8,skc7)* -> . % 7.71/7.89 2163[3:MRR:254.0,2155.0] || -> equal(cons(hd(skc7),tl(skc7)),skc7)**. % 7.71/7.89 2166[3:MRR:251.2,2155.0] ssList(u) || equal(app(skc7,u),nil)** -> . % 7.71/7.89 2188[4:Spt:224.0] || -> totalorderedP(skc7)*. % 7.71/7.89 2192[5:Spt:225.0] || -> strictorderedP(skc7)*. % 7.71/7.89 2197[6:Spt:268.0] || -> cyclefreeP(skc7)*. % 7.71/7.89 2201[7:Spt:222.0] || -> totalorderP(skc7)*. % 7.71/7.89 2202[8:Spt:223.0] || -> strictorderP(skc7)*. % 7.71/7.89 2215[9:Spt:270.0] || -> duplicatefreeP(skc7)*. % 7.71/7.89 2282[0:SpR:90.1,80.1] ssItem(skf44(u,v)) || -> SkP0(u,v)* equalelemsP(v). % 7.71/7.89 2283[0:SpR:90.1,79.1] ssItem(skf44(u,v)) || -> SkP0(u,v)* duplicatefreeP(v). % 7.71/7.89 2284[0:SpR:90.1,78.1] ssItem(skf44(u,v)) || -> SkP0(u,v)* strictorderedP(v). % 7.71/7.89 2285[0:SpR:90.1,77.1] ssItem(skf44(u,v)) || -> SkP0(u,v)* totalorderedP(v). % 7.71/7.89 2286[0:SpR:90.1,76.1] ssItem(skf44(u,v)) || -> SkP0(u,v)* strictorderP(v). % 7.71/7.89 2287[0:SpR:90.1,75.1] ssItem(skf44(u,v)) || -> SkP0(u,v)* totalorderP(v). % 7.71/7.89 2288[0:SpR:90.1,74.1] ssItem(skf44(u,v)) || -> SkP0(u,v)* cyclefreeP(v). % 7.71/7.89 2290[0:SSi:2282.0,54.0] || -> SkP0(u,v)* equalelemsP(v). % 7.71/7.89 2291[0:SSi:2283.0,54.0] || -> SkP0(u,v)* duplicatefreeP(v). % 7.71/7.89 2292[0:SSi:2284.0,54.0] || -> SkP0(u,v)* strictorderedP(v). % 7.71/7.89 2293[0:SSi:2285.0,54.0] || -> SkP0(u,v)* totalorderedP(v). % 7.71/7.89 2294[0:SSi:2286.0,54.0] || -> SkP0(u,v)* strictorderP(v). % 7.71/7.89 2295[0:SSi:2287.0,54.0] || -> SkP0(u,v)* totalorderP(v). % 7.71/7.89 2296[0:SSi:2288.0,54.0] || -> SkP0(u,v)* cyclefreeP(v). % 7.71/7.89 2298[3:Res:2290.0,2162.0] || -> equalelemsP(skc7)*. % 7.71/7.89 2300[3:Res:2291.0,2162.0] || -> duplicatefreeP(skc7)*. % 7.71/7.89 2301[3:Res:2292.0,2162.0] || -> strictorderedP(skc7)*. % 7.71/7.89 2302[3:Res:2293.0,2162.0] || -> totalorderedP(skc7)*. % 7.71/7.89 2303[3:Res:2294.0,2162.0] || -> strictorderP(skc7)*. % 7.71/7.89 2304[3:Res:2295.0,2162.0] || -> totalorderP(skc7)*. % 7.71/7.89 2305[3:Res:2296.0,2162.0] || -> cyclefreeP(skc7)*. % 7.71/7.89 2311[0:SpL:90.1,324.1] ssItem(skf44(u,v)) || equal(v,skc7) -> SkP0(u,v)* singletonP(skc7). % 7.71/7.89 2312[0:SSi:2311.0,54.0] || equal(u,skc7) -> SkP0(v,u)* singletonP(skc7). % 7.71/7.89 2313[10:Spt:2312.0,2312.1] || equal(u,skc7) -> SkP0(v,u)*. % 7.71/7.89 2314[10:Res:2313.1,2162.0] || equal(skc7,skc7)* -> . % 7.71/7.89 2315[10:Obv:2314.0] || -> . % 7.71/7.89 2316[10:Spt:2315.0,2312.2] || -> singletonP(skc7)*. % 7.71/7.89 2317[10:MRR:255.0,2316.0] || -> equal(cons(skf47(skc7),nil),skc7)**. % 7.71/7.89 2393[10:SpR:2317.0,115.2] ssItem(skf47(skc7)) ssList(nil) || -> equal(tl(skc7),nil)**. % 7.71/7.89 2397[10:SSi:2393.1,2393.0,15.0,14.0,13.0,12.0,11.0,10.0,9.0,8.0,16.0,5.0,2188.0,2192.0,2197.0,2201.0,2202.0,2215.0,2298.0,2316.0] || -> equal(tl(skc7),nil)**. % 7.71/7.89 2400[10:Rew:2397.0,2163.0] || -> equal(cons(hd(skc7),nil),skc7)**. % 7.71/7.89 2401[10:Rew:2397.0,558.1] ssList(u) || -> equal(tl(app(skc7,u)),app(nil,u))**. % 7.71/7.89 2404[10:Rew:83.1,2401.1] ssList(u) || -> equal(tl(app(skc7,u)),u)**. % 7.71/7.89 2440[0:SpR:90.1,114.2] ssItem(skf44(u,v)) ssList(nil) || -> SkP0(u,v) equal(skf44(u,v),hd(v))**. % 7.71/7.89 2444[0:SSi:2440.1,2440.0,15.0,14.0,13.0,12.0,11.0,10.0,9.0,8.0,54.0] || -> SkP0(u,v) equal(skf44(u,v),hd(v))**. % 7.71/7.89 2446[0:Rew:2444.1,90.1] || -> SkP0(u,v)* equal(cons(hd(v),nil),v)**. % 7.71/7.89 2633[10:SpR:2404.1,121.2] ssList(u) ssList(app(skc7,u)) || -> equal(app(skc7,u),nil) equal(cons(hd(app(skc7,u)),u),app(skc7,u))**. % 7.71/7.89 2649[10:Rew:554.1,2633.3] ssList(u) ssList(app(skc7,u)) || -> equal(app(skc7,u),nil) equal(cons(hd(skc7),u),app(skc7,u))**. % 7.71/7.89 2650[10:SSi:2649.1,95.0,5.0,2188.0,2192.0,2197.0,2201.0,2202.0,2215.0,2298.0,2316.2] ssList(u) || -> equal(app(skc7,u),nil) equal(cons(hd(skc7),u),app(skc7,u))**. % 7.71/7.89 2651[10:MRR:2650.1,2166.1] ssList(u) || -> equal(cons(hd(skc7),u),app(skc7,u))**. % 7.71/7.89 3005[0:EqR:124.2] ssList(cons(u,nil)) ssItem(u) || -> singletonP(cons(u,nil))*. % 7.71/7.89 3010[0:SSi:3005.0,80.0,79.0,78.0,77.0,76.0,75.0,74.0,94.0,15.2,14.1,13.1,12.1,11.1,10.1,9.1,8.1] ssItem(u) || -> singletonP(cons(u,nil))*. % 7.71/7.89 4575[0:EqR:146.3] ssList(u) ssList(app(u,v)) ssList(v) || -> frontsegP(app(u,v),u)*. % 7.71/7.89 4590[0:SSi:4575.1,95.2] ssList(u) ssList(v) || -> frontsegP(app(u,v),u)*. % 7.71/7.89 5046[0:SpR:162.3,85.0] ssList(skc11) ssList(cons(skc9,nil)) ssList(skc10) || -> equal(app(skc10,app(cons(skc9,nil),skc11)),skc7)**. % 7.71/7.89 5079[0:SSi:5046.2,5046.1,5046.0,2.0,80.0,3.0,79.0,3.0,78.0,3.0,77.0,3.0,76.0,3.2,75.0,3.1,74.0,3.1,3010.0,3.1,94.0,3.1,15.0,14.1,13.0,12.1,11.0,10.1,9.0,8.1,1.0] || -> equal(app(skc10,app(cons(skc9,nil),skc11)),skc7)**. % 7.71/7.89 5142[0:SpR:5079.0,136.3] ssList(app(cons(skc9,nil),skc11)) ssList(skc10) || -> equal(skc10,nil) equal(hd(skc10),hd(skc7))**. % 7.71/7.89 5145[0:SpR:5079.0,153.4] ssList(app(cons(skc9,nil),skc11)) ssList(u) ssList(skc10) || frontsegP(skc10,u)* -> frontsegP(skc7,u). % 7.71/7.89 5150[0:SpR:131.2,5079.0] ssItem(skc9) ssList(skc11) || -> equal(app(skc10,cons(skc9,skc11)),skc7)**. % 7.71/7.89 5156[0:SSi:5150.1,5150.0,1.0,3.0] || -> equal(app(skc10,cons(skc9,skc11)),skc7)**. % 7.71/7.89 5157[0:SSi:5142.1,5142.0,2.0,95.0,80.0,3.0,79.0,3.0,78.0,3.0,77.0,3.0,76.2,3.0,75.1,3.0,74.1,3.0,3010.1,3.0,94.1,3.0,15.1,14.0,13.1,12.0,11.1,10.0,9.1,8.2,1.0] || -> equal(skc10,nil) equal(hd(skc10),hd(skc7))**. % 7.71/7.89 5160[0:SSi:5145.2,5145.0,2.0,95.0,80.0,3.0,79.0,3.0,78.0,3.0,77.0,3.0,76.2,3.0,75.1,3.0,74.1,3.0,3010.1,3.0,94.1,3.0,15.1,14.0,13.1,12.0,11.1,10.0,9.1,8.2,1.0] ssList(u) || frontsegP(skc10,u)* -> frontsegP(skc7,u). % 7.71/7.89 5188[11:Spt:5157.0] || -> equal(skc10,nil)**. % 7.71/7.89 5191[11:Rew:5188.0,62.1] || -> memberP(skc11,skc9)* memberP(nil,skc9). % 7.71/7.89 5197[11:Rew:5188.0,5156.0] || -> equal(app(nil,cons(skc9,skc11)),skc7)**. % 7.71/7.89 5234[11:SpR:5197.0,83.1] ssList(cons(skc9,skc11)) || -> equal(cons(skc9,skc11),skc7)**. % 7.71/7.89 5243[11:SSi:5234.0,94.0,3.0,1.2] || -> equal(cons(skc9,skc11),skc7)**. % 7.71/7.89 5257[11:SpR:5243.0,115.2] ssItem(skc9) ssList(skc11) || -> equal(tl(skc7),skc11)**. % 7.71/7.89 5273[11:Rew:2397.0,5257.2] ssItem(skc9) ssList(skc11) || -> equal(skc11,nil)**. % 7.71/7.89 5274[11:SSi:5273.1,5273.0,1.0,3.0] || -> equal(skc11,nil)**. % 7.71/7.89 5289[11:Rew:5274.0,5191.0] || -> memberP(nil,skc9)* memberP(nil,skc9)*. % 7.71/7.89 5314[11:Obv:5289.0] || -> memberP(nil,skc9)*. % 7.71/7.89 5359[11:Res:5314.0,73.1] ssItem(skc9) || -> . % 7.71/7.89 5360[11:SSi:5359.0,3.0] || -> . % 7.71/7.89 5361[11:Spt:5360.0,5157.0,5188.0] || equal(skc10,nil)** -> . % 7.71/7.89 5362[11:Spt:5360.0,5157.1] || -> equal(hd(skc10),hd(skc7))**. % 7.71/7.89 5366[11:SpR:5362.0,121.2] ssList(skc10) || -> equal(skc10,nil) equal(cons(hd(skc7),tl(skc10)),skc10)**. % 7.71/7.89 5368[11:SpR:5362.0,2446.1] || -> SkP0(u,skc10)* equal(cons(hd(skc7),nil),skc10)**. % 7.71/7.89 5372[11:Rew:2400.0,5368.1] || -> SkP0(u,skc10)* equal(skc10,skc7). % 7.71/7.89 5377[11:MRR:5366.0,5366.1,2.0,5361.0] || -> equal(cons(hd(skc7),tl(skc10)),skc10)**. % 7.71/7.89 5396[12:Spt:5372.1] || -> equal(skc10,skc7)**. % 7.71/7.89 5402[12:Rew:5396.0,5156.0] || -> equal(app(skc7,cons(skc9,skc11)),skc7)**. % 7.71/7.89 5450[12:SpR:5402.0,2404.1] ssList(cons(skc9,skc11)) || -> equal(cons(skc9,skc11),tl(skc7))**. % 7.71/7.89 5463[12:Rew:2397.0,5450.1] ssList(cons(skc9,skc11)) || -> equal(cons(skc9,skc11),nil)**. % 7.71/7.89 5464[12:SSi:5463.0,94.0,3.0,1.2] || -> equal(cons(skc9,skc11),nil)**. % 7.71/7.89 5488[12:SpL:5464.0,113.2] ssItem(skc9) ssList(skc11) || equal(nil,nil)* -> . % 7.71/7.89 5496[12:Obv:5488.2] ssItem(skc9) ssList(skc11) || -> . % 7.71/7.89 5497[12:SSi:5496.1,5496.0,1.0,3.0] || -> . % 7.71/7.89 5517[12:Spt:5497.0,5372.1,5396.0] || equal(skc10,skc7)** -> . % 7.71/7.89 5518[12:Spt:5497.0,5372.0] || -> SkP0(u,skc10)*. % 7.71/7.89 5542[11:SpR:5377.0,2651.1] ssList(tl(skc10)) || -> equal(app(skc7,tl(skc10)),skc10)**. % 7.71/7.89 5810[11:SoR:5542.0,89.1] ssList(skc10) || -> equal(app(skc7,tl(skc10)),skc10)** equal(skc10,nil). % 7.71/7.89 5812[11:SSi:5810.0,2.0] || -> equal(app(skc7,tl(skc10)),skc10)** equal(skc10,nil). % 7.71/7.89 5813[11:MRR:5812.1,5361.0] || -> equal(app(skc7,tl(skc10)),skc10)**. % 7.71/7.89 5915[0:Res:64.1,5160.1] ssList(skc10) ssList(skc10) || -> frontsegP(skc7,skc10)*. % 7.71/7.89 5920[0:Obv:5915.0] ssList(skc10) || -> frontsegP(skc7,skc10)*. % 7.71/7.89 5921[0:SSi:5920.0,2.0] || -> frontsegP(skc7,skc10)*. % 7.71/7.89 5924[0:Res:5921.0,142.2] ssList(skc7) ssList(skc10) || frontsegP(skc10,skc7)* -> equal(skc10,skc7). % 7.71/7.89 5925[10:SSi:5924.1,5924.0,2.0,5.0,2188.0,2192.0,2197.0,2201.0,2202.0,2215.0,2298.0,2316.0] || frontsegP(skc10,skc7)* -> equal(skc10,skc7). % 7.71/7.89 5926[12:MRR:5925.1,5517.0] || frontsegP(skc10,skc7)* -> . % 7.71/7.89 7429[0:SpL:5156.0,190.4] ssItem(skc9) ssList(u) ssList(skc11) ssList(skc10) || equal(skc7,u) -> memberP(u,skc9)*. % 7.71/7.89 7439[0:SSi:7429.3,7429.2,7429.0,2.0,1.0,3.0] ssList(u) || equal(skc7,u) -> memberP(u,skc9)*. % 7.71/7.89 10017[11:SpR:5813.0,4590.2] ssList(skc7) ssList(tl(skc10)) || -> frontsegP(skc10,skc7)*. % 7.71/7.89 10026[11:SSi:10017.0,5.0,2188.0,2192.0,2197.0,2201.0,2202.0,2215.0,2298.0,2316.0] ssList(tl(skc10)) || -> frontsegP(skc10,skc7)*. % 7.71/7.89 10027[12:MRR:10026.1,5926.0] ssList(tl(skc10)) || -> . % 7.71/7.89 10063[12:SoR:10027.0,89.1] ssList(skc10) || -> equal(skc10,nil)**. % 7.71/7.89 10065[12:SSi:10063.0,2.0] || -> equal(skc10,nil)**. % 7.71/7.89 10066[12:MRR:10065.0,5361.0] || -> . % 7.71/7.89 10067[9:Spt:10066.0,270.0,2215.0] || duplicatefreeP(skc7)* -> . % 7.71/7.89 10068[9:Spt:10066.0,270.1] || -> equal(skf78(skc7),skf77(skc7))**. % 7.71/7.89 10069[9:MRR:10067.0,2300.0] || -> . % 7.71/7.89 10216[8:Spt:10069.0,223.0,2202.0] || strictorderP(skc7)* -> . % 7.71/7.89 10217[8:Spt:10069.0,223.1] || -> equal(app(app(skf64(skc7),cons(skf62(skc7),skf65(skc7))),cons(skf63(skc7),skf66(skc7))),skc7)**. % 7.71/7.89 10218[8:MRR:10216.0,2303.0] || -> . % 7.71/7.89 10408[7:Spt:10218.0,222.0,2201.0] || totalorderP(skc7)* -> . % 7.71/7.89 10409[7:Spt:10218.0,222.1] || -> equal(app(app(skf59(skc7),cons(skf57(skc7),skf60(skc7))),cons(skf58(skc7),skf61(skc7))),skc7)**. % 7.71/7.89 10410[7:MRR:10408.0,2304.0] || -> . % 7.71/7.89 10500[6:Spt:10410.0,268.0,2197.0] || cyclefreeP(skc7)* -> . % 7.71/7.89 10501[6:Spt:10410.0,268.1] || -> leq(skf53(skc7),skf52(skc7))*. % 7.71/7.89 10502[6:MRR:10500.0,2305.0] || -> . % 7.71/7.89 10677[5:Spt:10502.0,225.0,2192.0] || strictorderedP(skc7)* -> . % 7.71/7.89 10678[5:Spt:10502.0,225.1] || -> equal(app(app(skf74(skc7),cons(skf72(skc7),skf75(skc7))),cons(skf73(skc7),skf76(skc7))),skc7)**. % 7.71/7.89 10679[5:MRR:10677.0,2301.0] || -> . % 8.25/8.43 10856[4:Spt:10679.0,224.0,2188.0] || totalorderedP(skc7)* -> . % 8.25/8.43 10857[4:Spt:10679.0,224.1] || -> equal(app(app(skf69(skc7),cons(skf67(skc7),skf70(skc7))),cons(skf68(skc7),skf71(skc7))),skc7)**. % 8.25/8.43 10858[4:MRR:10856.0,2302.0] || -> . % 8.25/8.43 10953[2:Spt:10858.0,242.1] || -> equal(nil,skc7)**. % 8.25/8.43 10976[2:Rew:10953.0,15.0] || -> equalelemsP(skc7)*. % 8.25/8.43 10977[2:Rew:10953.0,14.0] || -> duplicatefreeP(skc7)*. % 8.25/8.43 10978[2:Rew:10953.0,13.0] || -> strictorderedP(skc7)*. % 8.25/8.43 10979[2:Rew:10953.0,12.0] || -> totalorderedP(skc7)*. % 8.25/8.43 10980[2:Rew:10953.0,11.0] || -> strictorderP(skc7)*. % 8.25/8.43 10981[2:Rew:10953.0,10.0] || -> totalorderP(skc7)*. % 8.25/8.43 10982[2:Rew:10953.0,9.0] || -> cyclefreeP(skc7)*. % 8.25/8.43 11009[2:Rew:10953.0,73.1] ssItem(u) || memberP(skc7,u)* -> . % 8.25/8.43 12237[2:Res:7439.2,11009.1] ssList(skc7) ssItem(skc9) || equal(skc7,skc7)* -> . % 8.25/8.43 12239[2:Obv:12237.2] ssList(skc7) ssItem(skc9) || -> . % 8.25/8.43 12240[2:SSi:12239.1,12239.0,3.0,5.0,10976.0,10977.0,10978.0,10979.0,10980.0,10981.0,10982.0] || -> . % 8.25/8.43 12241[1:Spt:12240.0,248.1] || -> equal(nil,skc7)**. % 8.25/8.43 12243[1:Rew:12241.0,9.0] || -> cyclefreeP(skc7)*. % 8.25/8.43 12244[1:Rew:12241.0,10.0] || -> totalorderP(skc7)*. % 8.25/8.43 12245[1:Rew:12241.0,11.0] || -> strictorderP(skc7)*. % 8.25/8.43 12246[1:Rew:12241.0,12.0] || -> totalorderedP(skc7)*. % 8.25/8.43 12247[1:Rew:12241.0,13.0] || -> strictorderedP(skc7)*. % 8.25/8.43 12248[1:Rew:12241.0,14.0] || -> duplicatefreeP(skc7)*. % 8.25/8.43 12249[1:Rew:12241.0,15.0] || -> equalelemsP(skc7)*. % 8.25/8.43 12272[1:Rew:12241.0,73.1] ssItem(u) || memberP(skc7,u)* -> . % 8.25/8.43 13186[1:Res:7439.2,12272.1] ssList(skc7) ssItem(skc9) || equal(skc7,skc7)* -> . % 8.25/8.43 13188[1:Obv:13186.2] ssList(skc7) ssItem(skc9) || -> . % 8.25/8.43 13189[1:SSi:13188.1,13188.0,3.0,5.0,12243.0,12244.0,12245.0,12246.0,12247.0,12248.0,12249.0] || -> . % 8.25/8.43 % SZS output end Refutation % 8.25/8.43 Formulae used in the proof : co1 ax2 ax17 ax60 ax62 ax64 ax66 ax69 ax72 ax74 ax4 ax42 ax38 ax59 ax61 ax63 ax65 ax68 ax71 ax73 ax28 ax76 ax8 ax13 ax16 ax26 ax21 ax23 ax25 ax78 ax81 ax83 ax85 ax41 ax5 ax43 ax86 ax82 ax12 ax11 ax10 ax9 ax3 ax77 % 8.25/8.43 %------------------------------------------------------------------------------