%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : SWC285+1 : TPTP v8.1.0. Released v2.4.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n026.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:03 EDT 2022 % Result : Theorem 3.84s 4.05s % Output : Refutation 4.06s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.13 % Problem : SWC285+1 : TPTP v8.1.0. Released v2.4.0. % 0.07/0.13 % Command : run_spass %d %s % 0.13/0.35 % Computer : n026.cluster.edu % 0.13/0.35 % Model : x86_64 x86_64 % 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.35 % Memory : 8042.1875MB % 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.35 % CPULimit : 300 % 0.13/0.35 % WCLimit : 600 % 0.13/0.35 % DateTime : Sun Jun 12 04:55:50 EDT 2022 % 0.13/0.35 % CPUTime : % 3.84/4.05 % 3.84/4.05 SPASS V 3.9 % 3.84/4.05 SPASS beiseite: Proof found. % 3.84/4.05 % SZS status Theorem % 3.84/4.05 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 3.84/4.05 SPASS derived 5886 clauses, backtracked 1953 clauses, performed 49 splits and kept 4179 clauses. % 3.84/4.05 SPASS allocated 105809 KBytes. % 3.84/4.05 SPASS spent 0:00:03.69 on the problem. % 3.84/4.05 0:00:00.04 for the input. % 3.84/4.05 0:00:00.06 for the FLOTTER CNF translation. % 3.84/4.05 0:00:00.06 for inferences. % 3.84/4.05 0:00:00.07 for the backtracking. % 3.84/4.05 0:00:03.23 for the reduction. % 3.84/4.05 % 3.84/4.05 % 3.84/4.05 Here is a proof with depth 8, length 289 : % 3.84/4.05 % SZS output start Refutation % 3.84/4.05 1[0:Inp] || -> ssItem(skc13)*. % 3.84/4.05 2[0:Inp] || -> ssList(skc12)*. % 3.84/4.05 3[0:Inp] || -> ssList(skc11)*. % 3.84/4.05 4[0:Inp] || -> ssItem(skc10)*. % 3.84/4.05 5[0:Inp] || -> ssList(skc9)*. % 3.84/4.05 6[0:Inp] || -> ssList(skc8)*. % 3.84/4.05 7[0:Inp] || -> ssItem(skc15)*. % 3.84/4.05 8[0:Inp] || -> ssItem(skc14)*. % 3.84/4.05 9[0:Inp] || -> ssList(nil)*. % 3.84/4.05 10[0:Inp] || -> cyclefreeP(nil)*. % 3.84/4.05 11[0:Inp] || -> totalorderP(nil)*. % 3.84/4.05 12[0:Inp] || -> strictorderP(nil)*. % 3.84/4.05 13[0:Inp] || -> totalorderedP(nil)*. % 3.84/4.05 14[0:Inp] || -> strictorderedP(nil)*. % 3.84/4.05 15[0:Inp] || -> duplicatefreeP(nil)*. % 3.84/4.05 16[0:Inp] || -> equalelemsP(nil)*. % 3.84/4.05 17[0:Inp] || -> segmentP(skc9,skc8)*. % 3.84/4.05 18[0:Inp] || -> ssItem(skf45(u))*. % 3.84/4.05 56[0:Inp] || equal(skc15,skc14)** -> . % 3.84/4.05 63[0:Inp] || neq(skc9,nil)* -> singletonP(skc8). % 3.84/4.05 65[0:Inp] ssList(u) || -> frontsegP(u,u)*. % 3.84/4.05 72[0:Inp] || -> memberP(u,v) SkP0(w,v,u)*. % 3.84/4.05 73[0:Inp] ssItem(u) || memberP(nil,u)* -> . % 3.84/4.05 74[0:Inp] ssItem(u) || -> cyclefreeP(cons(u,nil))*. % 3.84/4.05 75[0:Inp] ssItem(u) || -> totalorderP(cons(u,nil))*. % 3.84/4.05 76[0:Inp] ssItem(u) || -> strictorderP(cons(u,nil))*. % 3.84/4.05 77[0:Inp] ssItem(u) || -> totalorderedP(cons(u,nil))*. % 3.84/4.05 78[0:Inp] ssItem(u) || -> strictorderedP(cons(u,nil))*. % 3.84/4.05 79[0:Inp] ssItem(u) || -> duplicatefreeP(cons(u,nil))*. % 3.84/4.05 80[0:Inp] ssItem(u) || -> equalelemsP(cons(u,nil))*. % 3.84/4.05 82[0:Inp] || SkP0(skc10,skc13,skc11)* -> memberP(skc12,skc13). % 3.84/4.05 84[0:Inp] ssList(u) || -> equal(app(nil,u),u)**. % 3.84/4.05 86[0:Inp] || -> equal(app(app(skc11,cons(skc10,nil)),skc12),skc8)**. % 3.84/4.05 91[0:Inp] ssList(u) || -> ssList(tl(u))* equal(nil,u). % 3.84/4.05 92[0:Inp] ssList(u) || -> cyclefreeP(u) leq(skf51(u),skf50(u))*. % 3.84/4.05 95[0:Inp] ssItem(u) ssList(v) || -> ssList(cons(u,v))*. % 3.84/4.05 96[0:Inp] ssList(u) ssList(v) || -> ssList(app(v,u))*. % 3.84/4.05 97[0:Inp] ssList(u) || frontsegP(nil,u)* -> equal(nil,u). % 3.84/4.05 99[0:Inp] ssList(u) || rearsegP(nil,u)* -> equal(nil,u). % 3.84/4.05 101[0:Inp] ssList(u) || segmentP(nil,u)* -> equal(nil,u). % 3.84/4.05 111[0:Inp] ssList(u) singletonP(u) || -> equal(cons(skf45(u),nil),u)**. % 3.84/4.05 112[0:Inp] ssList(u) ssList(v) || -> neq(v,u)* equal(v,u). % 3.84/4.05 114[0:Inp] ssItem(u) ssList(v) || equal(cons(u,v),nil)** -> . % 3.84/4.05 115[0:Inp] ssItem(u) ssList(v) || -> equal(hd(cons(u,v)),u)**. % 3.84/4.05 116[0:Inp] ssItem(u) ssList(v) || -> equal(tl(cons(u,v)),v)**. % 3.84/4.05 122[0:Inp] ssList(u) || -> equal(nil,u) equal(cons(hd(u),tl(u)),u)**. % 3.84/4.05 125[0:Inp] ssList(u) ssItem(v) || equal(cons(v,nil),u)*+ -> singletonP(u)*. % 3.84/4.05 132[0:Inp] ssItem(u) ssList(v) || -> equal(app(cons(u,nil),v),cons(u,v))**. % 3.84/4.05 134[0:Inp] ssList(u) ssList(v) || equal(app(v,u),nil)** -> equal(nil,v). % 3.84/4.05 137[0:Inp] ssList(u) ssList(v) || -> equal(nil,v) equal(hd(app(v,u)),hd(v))**. % 3.84/4.05 143[0:Inp] ssList(u) ssList(v) || frontsegP(u,v)*+ frontsegP(v,u)* -> equal(v,u). % 3.84/4.05 147[0:Inp] ssList(u) ssList(v) ssList(w) || equal(app(u,w),v)*+ -> frontsegP(v,u)*. % 3.84/4.05 148[0:Inp] ssList(u) ssList(v) ssList(w) || equal(app(w,u),v)*+ -> rearsegP(v,u)*. % 3.84/4.05 154[0:Inp] ssList(u) ssList(v) ssList(w) || frontsegP(w,v) -> frontsegP(app(w,u),v)*. % 3.84/4.05 156[0:Inp] ssList(u) ssItem(v) || totalorderedP(cons(v,u))* -> leq(v,hd(u)) equal(nil,u). % 3.84/4.05 157[0:Inp] ssList(u) ssItem(v) || strictorderedP(cons(v,u))* -> lt(v,hd(u)) equal(nil,u). % 3.84/4.05 158[0:Inp] ssList(u) ssList(v) || -> equal(nil,v) equal(app(tl(v),u),tl(app(v,u)))**. % 3.84/4.05 163[0:Inp] ssList(u) ssList(v) ssList(w) || -> equal(app(app(w,v),u),app(w,app(v,u)))**. % 3.84/4.05 177[0:Inp] ssList(u) || -> strictorderedP(u) equal(app(app(skf72(u),cons(skf70(u),skf73(u))),cons(skf71(u),skf74(u))),u)**. % 3.84/4.05 178[0:Inp] ssList(u) || -> totalorderedP(u) equal(app(app(skf67(u),cons(skf65(u),skf68(u))),cons(skf66(u),skf69(u))),u)**. % 3.84/4.05 179[0:Inp] ssList(u) || -> strictorderP(u) equal(app(app(skf62(u),cons(skf60(u),skf63(u))),cons(skf61(u),skf64(u))),u)**. % 3.84/4.05 180[0:Inp] ssList(u) || -> totalorderP(u) equal(app(app(skf57(u),cons(skf55(u),skf58(u))),cons(skf56(u),skf59(u))),u)**. % 3.84/4.05 221[0:Res:6.0,180.0] || -> totalorderP(skc8) equal(app(app(skf57(skc8),cons(skf55(skc8),skf58(skc8))),cons(skf56(skc8),skf59(skc8))),skc8)**. % 3.84/4.05 222[0:Res:6.0,179.0] || -> strictorderP(skc8) equal(app(app(skf62(skc8),cons(skf60(skc8),skf63(skc8))),cons(skf61(skc8),skf64(skc8))),skc8)**. % 3.84/4.05 223[0:Res:6.0,178.0] || -> totalorderedP(skc8) equal(app(app(skf67(skc8),cons(skf65(skc8),skf68(skc8))),cons(skf66(skc8),skf69(skc8))),skc8)**. % 3.84/4.05 224[0:Res:6.0,177.0] || -> strictorderedP(skc8) equal(app(app(skf72(skc8),cons(skf70(skc8),skf73(skc8))),cons(skf71(skc8),skf74(skc8))),skc8)**. % 3.84/4.05 241[0:Res:6.0,158.0] ssList(u) || -> equal(skc8,nil) equal(app(tl(skc8),u),tl(app(skc8,u)))**. % 3.84/4.05 247[0:Res:6.0,137.0] ssList(u) || -> equal(skc8,nil) equal(hd(app(skc8,u)),hd(skc8))**. % 3.84/4.05 250[0:Res:6.0,134.0] ssList(u) || equal(app(skc8,u),nil)** -> equal(skc8,nil). % 3.84/4.05 254[0:Res:6.0,111.1] singletonP(skc8) || -> equal(cons(skf45(skc8),nil),skc8)**. % 3.84/4.05 258[0:Res:6.0,115.0] ssItem(u) || -> equal(hd(cons(u,skc8)),u)**. % 3.84/4.05 267[0:Res:6.0,92.0] || -> cyclefreeP(skc8) leq(skf51(skc8),skf50(skc8))*. % 3.84/4.05 270[0:Res:6.0,95.0] ssItem(u) || -> ssList(cons(u,skc8))*. % 3.84/4.05 271[0:Res:6.0,96.0] ssList(u) || -> ssList(app(skc8,u))*. % 3.84/4.05 276[0:Res:6.0,101.0] || segmentP(nil,skc8)* -> equal(skc8,nil). % 3.84/4.05 311[0:Res:6.0,157.1] ssItem(u) || strictorderedP(cons(u,skc8))* -> lt(u,hd(skc8)) equal(skc8,nil). % 3.84/4.05 426[0:Res:5.0,112.0] ssList(u) || -> neq(skc9,u)* equal(skc9,u). % 3.84/4.05 481[0:Res:5.0,156.1] ssItem(u) || totalorderedP(cons(u,skc9))* -> leq(u,hd(skc9)) equal(skc9,nil). % 3.84/4.05 547[1:Spt:247.0,247.2] ssList(u) || -> equal(hd(app(skc8,u)),hd(skc8))**. % 3.84/4.05 549[2:Spt:241.0,241.2] ssList(u) || -> equal(app(tl(skc8),u),tl(app(skc8,u)))**. % 3.84/4.05 555[3:Spt:311.3] || -> equal(skc8,nil)**. % 3.84/4.05 556[3:Rew:555.0,547.1] ssList(u) || -> equal(hd(app(nil,u)),hd(nil))**. % 3.84/4.05 574[3:Rew:555.0,270.1] ssItem(u) || -> ssList(cons(u,nil))*. % 3.84/4.05 575[3:Rew:555.0,258.1] ssItem(u) || -> equal(hd(cons(u,nil)),u)**. % 3.84/4.05 729[3:Rew:84.1,556.1] ssList(u) || -> equal(hd(u),hd(nil))*. % 3.84/4.05 1059[0:Res:72.1,82.0] || -> memberP(skc11,skc13) memberP(skc12,skc13)*. % 3.84/4.05 1198[3:SpR:575.1,729.1] ssItem(u) ssList(cons(u,nil)) || -> equal(u,hd(nil))*. % 3.84/4.05 1201[3:SSi:1198.1,80.1,79.1,76.1,75.1,74.1,78.1,77.1,574.1] ssItem(u) || -> equal(u,hd(nil))*. % 3.84/4.05 1270[3:SpR:1201.1,1201.1] ssItem(u) ssItem(v) || -> equal(v,u)*. % 3.84/4.05 1310[3:EmS:1270.0,1.0] ssItem(u) || -> equal(u,skc13)*. % 3.84/4.05 1333[3:EmS:1310.0,4.0] || -> equal(skc13,skc10)**. % 3.84/4.05 1334[3:EmS:1310.0,7.0] || -> equal(skc15,skc13)**. % 3.84/4.05 1335[3:EmS:1310.0,8.0] || -> equal(skc14,skc13)**. % 3.84/4.05 1342[3:Rew:1333.0,1334.0] || -> equal(skc15,skc10)**. % 3.84/4.05 1344[3:Rew:1342.0,56.0] || equal(skc14,skc10)** -> . % 3.84/4.05 1346[3:Rew:1333.0,1335.0] || -> equal(skc14,skc10)**. % 3.84/4.05 1468[3:Rew:1346.0,1344.0] || equal(skc10,skc10)* -> . % 3.84/4.05 1469[3:Obv:1468.0] || -> . % 3.84/4.05 1504[3:Spt:1469.0,311.3,555.0] || equal(skc8,nil)** -> . % 3.84/4.05 1505[3:Spt:1469.0,311.0,311.1,311.2] ssItem(u) || strictorderedP(cons(u,skc8))* -> lt(u,hd(skc8)). % 3.84/4.05 1508[3:MRR:276.1,1504.0] || segmentP(nil,skc8)* -> . % 3.84/4.05 1514[3:MRR:250.2,1504.0] ssList(u) || equal(app(skc8,u),nil)** -> . % 3.84/4.05 1519[4:Spt:481.3] || -> equal(skc9,nil)**. % 3.84/4.05 1527[4:Rew:1519.0,17.0] || -> segmentP(nil,skc8)*. % 3.84/4.05 1672[4:MRR:1527.0,1508.0] || -> . % 3.84/4.05 1783[4:Spt:1672.0,481.3,1519.0] || equal(skc9,nil)** -> . % 3.84/4.05 1784[4:Spt:1672.0,481.0,481.1,481.2] ssItem(u) || totalorderedP(cons(u,skc9))* -> leq(u,hd(skc9)). % 3.84/4.05 1798[5:Spt:224.0] || -> strictorderedP(skc8)*. % 3.84/4.05 1801[6:Spt:223.0] || -> totalorderedP(skc8)*. % 3.84/4.05 1812[7:Spt:267.0] || -> cyclefreeP(skc8)*. % 3.84/4.05 1816[8:Spt:222.0] || -> strictorderP(skc8)*. % 3.84/4.05 1817[9:Spt:221.0] || -> totalorderP(skc8)*. % 3.84/4.05 1825[10:Spt:63.0] || neq(skc9,nil)* -> . % 3.84/4.05 1882[10:Res:426.1,1825.0] ssList(nil) || -> equal(skc9,nil)**. % 3.84/4.05 1883[10:SSi:1882.0,16.0,15.0,12.0,11.0,10.0,14.0,13.0,9.0] || -> equal(skc9,nil)**. % 3.84/4.05 1884[10:MRR:1883.0,1783.0] || -> . % 3.84/4.05 1885[10:Spt:1884.0,63.0,1825.0] || -> neq(skc9,nil)*. % 3.84/4.05 1886[10:Spt:1884.0,63.1] || -> singletonP(skc8)*. % 3.84/4.05 1887[10:MRR:254.0,1886.0] || -> equal(cons(skf45(skc8),nil),skc8)**. % 3.84/4.05 1888[11:Spt:1059.0] || -> memberP(skc11,skc13)*. % 3.84/4.05 1889[10:SpR:1887.0,80.1] ssItem(skf45(skc8)) || -> equalelemsP(skc8)*. % 3.84/4.05 1890[10:SpR:1887.0,79.1] ssItem(skf45(skc8)) || -> duplicatefreeP(skc8)*. % 3.84/4.05 1898[10:SSi:1889.0,18.0,6.0,1798.0,1801.0,1812.0,1816.0,1817.0,1886.0] || -> equalelemsP(skc8)*. % 3.84/4.05 1900[10:SSi:1890.0,18.0,6.0,1798.0,1801.0,1812.0,1816.0,1817.0,1886.0] || -> duplicatefreeP(skc8)*. % 3.84/4.05 1969[0:SpR:111.2,76.1] ssList(u) singletonP(u) ssItem(skf45(u)) || -> strictorderP(u)*. % 3.84/4.05 1970[0:SpR:111.2,75.1] ssList(u) singletonP(u) ssItem(skf45(u)) || -> totalorderP(u)*. % 3.84/4.05 1971[0:SpR:111.2,74.1] ssList(u) singletonP(u) ssItem(skf45(u)) || -> cyclefreeP(u)*. % 3.84/4.05 1972[0:SpR:111.2,78.1] ssList(u) singletonP(u) ssItem(skf45(u)) || -> strictorderedP(u)*. % 3.84/4.05 1973[0:SpR:111.2,77.1] ssList(u) singletonP(u) ssItem(skf45(u)) || -> totalorderedP(u)*. % 3.84/4.05 1982[0:SSi:1969.2,18.0] ssList(u) singletonP(u) || -> strictorderP(u)*. % 3.84/4.05 1983[0:SSi:1970.2,18.0] ssList(u) singletonP(u) || -> totalorderP(u)*. % 3.84/4.05 1984[0:SSi:1971.2,18.0] ssList(u) singletonP(u) || -> cyclefreeP(u)*. % 3.84/4.05 1985[0:SSi:1972.2,18.0] ssList(u) singletonP(u) || -> strictorderedP(u)*. % 3.84/4.05 1986[0:SSi:1973.2,18.0] ssList(u) singletonP(u) || -> totalorderedP(u)*. % 3.84/4.05 1994[10:SpR:1887.0,116.2] ssItem(skf45(skc8)) ssList(nil) || -> equal(tl(skc8),nil)**. % 3.84/4.05 2000[10:SSi:1994.1,1994.0,16.0,15.0,12.0,11.0,10.0,14.0,13.0,9.0,18.0,6.0,1798.0,1801.0,1812.0,1816.0,1817.0,1886.0,1898.0,1900.0] || -> equal(tl(skc8),nil)**. % 3.84/4.05 2003[10:Rew:2000.0,549.1] ssList(u) || -> equal(tl(app(skc8,u)),app(nil,u))**. % 3.84/4.05 2005[10:Rew:84.1,2003.1] ssList(u) || -> equal(tl(app(skc8,u)),u)**. % 3.84/4.05 2185[10:SpR:2005.1,122.2] ssList(u) ssList(app(skc8,u)) || -> equal(app(skc8,u),nil) equal(cons(hd(app(skc8,u)),u),app(skc8,u))**. % 3.84/4.05 2199[10:Rew:547.1,2185.3] ssList(u) ssList(app(skc8,u)) || -> equal(app(skc8,u),nil) equal(cons(hd(skc8),u),app(skc8,u))**. % 3.84/4.05 2200[10:SSi:2199.1,271.1] ssList(u) || -> equal(app(skc8,u),nil) equal(cons(hd(skc8),u),app(skc8,u))**. % 3.84/4.05 2201[10:MRR:2200.1,1514.1] ssList(u) || -> equal(cons(hd(skc8),u),app(skc8,u))**. % 3.84/4.05 2600[0:EqR:125.2] ssList(cons(u,nil)) ssItem(u) || -> singletonP(cons(u,nil))*. % 3.84/4.05 2605[0:SSi:2600.0,95.1,16.1,15.1,12.1,11.1,10.1,14.1,13.0,9.0,80.0,79.0,76.0,75.0,74.0,78.0,77.2] ssItem(u) || -> singletonP(cons(u,nil))*. % 3.84/4.05 3854[0:SpL:86.0,148.3] ssList(skc12) ssList(u) ssList(app(skc11,cons(skc10,nil))) || equal(skc8,u) -> rearsegP(u,skc12)*. % 3.84/4.05 3867[0:SSi:3854.2,3854.0,96.0,3.0,95.1,4.0,16.1,15.0,12.1,11.0,10.1,14.0,13.1,9.0,80.1,4.0,79.1,4.0,76.1,4.0,75.0,4.0,74.0,4.0,78.0,4.0,77.0,4.0,2605.2,4.0,2.2] ssList(u) || equal(skc8,u) -> rearsegP(u,skc12)*. % 3.84/4.05 3891[0:Res:3867.2,99.1] ssList(nil) ssList(skc12) || equal(skc8,nil) -> equal(skc12,nil)**. % 3.84/4.05 3897[0:EqR:147.3] ssList(u) ssList(app(u,v)) ssList(v) || -> frontsegP(app(u,v),u)*. % 3.84/4.05 3912[0:SSi:3897.1,96.2] ssList(u) ssList(v) || -> frontsegP(app(u,v),u)*. % 3.84/4.05 4276[0:SpR:163.3,86.0] ssList(skc12) ssList(cons(skc10,nil)) ssList(skc11) || -> equal(app(skc11,app(cons(skc10,nil),skc12)),skc8)**. % 3.84/4.05 4319[0:SSi:4276.2,4276.1,4276.0,3.0,95.0,4.1,16.0,15.1,12.0,11.1,10.0,14.1,13.0,9.1,80.0,4.1,79.0,4.1,76.0,4.1,75.0,4.0,74.0,4.0,78.0,4.0,77.0,4.0,2605.0,4.2,2.0] || -> equal(app(skc11,app(cons(skc10,nil),skc12)),skc8)**. % 3.84/4.05 4376[0:SpR:4319.0,137.3] ssList(app(cons(skc10,nil),skc12)) ssList(skc11) || -> equal(skc11,nil) equal(hd(skc11),hd(skc8))**. % 3.84/4.05 4379[0:SpR:4319.0,154.4] ssList(app(cons(skc10,nil),skc12)) ssList(u) ssList(skc11) || frontsegP(skc11,u)* -> frontsegP(skc8,u). % 3.84/4.05 4383[0:SpR:132.2,4319.0] ssItem(skc10) ssList(skc12) || -> equal(app(skc11,cons(skc10,skc12)),skc8)**. % 3.84/4.05 4385[0:SpL:4319.0,147.3] ssList(skc11) ssList(u) ssList(app(cons(skc10,nil),skc12)) || equal(skc8,u) -> frontsegP(u,skc11)*. % 3.84/4.05 4389[0:SSi:4383.1,4383.0,2.0,4.0] || -> equal(app(skc11,cons(skc10,skc12)),skc8)**. % 3.84/4.05 4390[0:SSi:4376.1,4376.0,3.0,96.0,95.1,4.0,16.1,15.0,12.1,11.0,10.1,14.0,13.1,9.0,80.1,4.0,79.1,4.0,76.1,4.0,75.0,4.0,74.0,4.0,78.0,4.0,77.0,4.0,2605.2,4.2,2.0] || -> equal(skc11,nil) equal(hd(skc11),hd(skc8))**. % 3.84/4.05 4392[0:SSi:4385.2,4385.0,96.0,95.0,4.0,16.1,15.0,12.1,11.0,10.1,14.0,13.1,9.0,80.1,4.0,79.1,4.0,76.1,4.0,75.1,4.0,74.0,4.0,78.0,4.0,77.0,4.0,2605.0,4.0,2.2,3.2] ssList(u) || equal(skc8,u) -> frontsegP(u,skc11)*. % 3.84/4.05 4393[0:SSi:4379.2,4379.0,3.0,96.0,95.1,4.0,16.1,15.0,12.1,11.0,10.1,14.0,13.1,9.0,80.1,4.0,79.1,4.0,76.1,4.0,75.0,4.0,74.0,4.0,78.0,4.0,77.0,4.0,2605.2,4.2,2.0] ssList(u) || frontsegP(skc11,u)* -> frontsegP(skc8,u). % 3.84/4.05 4421[12:Spt:4390.0] || -> equal(skc11,nil)**. % 3.84/4.05 4424[12:Rew:4421.0,1888.0] || -> memberP(nil,skc13)*. % 3.84/4.05 4457[12:Res:4424.0,73.1] ssItem(skc13) || -> . % 3.84/4.05 4458[12:SSi:4457.0,1.0] || -> . % 3.84/4.05 4459[12:Spt:4458.0,4390.0,4421.0] || equal(skc11,nil)** -> . % 3.84/4.05 4460[12:Spt:4458.0,4390.1] || -> equal(hd(skc11),hd(skc8))**. % 3.84/4.05 4464[12:SpR:4460.0,122.2] ssList(skc11) || -> equal(skc11,nil) equal(cons(hd(skc8),tl(skc11)),skc11)**. % 3.84/4.05 4468[12:MRR:4464.0,4464.1,3.0,4459.0] || -> equal(cons(hd(skc8),tl(skc11)),skc11)**. % 3.84/4.05 4512[12:SpR:4468.0,2201.1] ssList(tl(skc11)) || -> equal(app(skc8,tl(skc11)),skc11)**. % 3.84/4.05 4640[12:SoR:4512.0,91.1] ssList(skc11) || -> equal(app(skc8,tl(skc11)),skc11)** equal(skc11,nil). % 3.84/4.05 4641[12:SSi:4640.0,3.0] || -> equal(app(skc8,tl(skc11)),skc11)** equal(skc11,nil). % 3.84/4.05 4642[12:MRR:4641.1,4459.0] || -> equal(app(skc8,tl(skc11)),skc11)**. % 3.84/4.05 4768[0:Res:65.1,4393.1] ssList(skc11) ssList(skc11) || -> frontsegP(skc8,skc11)*. % 3.84/4.05 4771[0:Obv:4768.0] ssList(skc11) || -> frontsegP(skc8,skc11)*. % 3.84/4.05 4772[0:SSi:4771.0,3.0] || -> frontsegP(skc8,skc11)*. % 3.84/4.05 4774[0:Res:4772.0,143.2] ssList(skc8) ssList(skc11) || frontsegP(skc11,skc8)* -> equal(skc11,skc8). % 3.84/4.05 4775[10:SSi:4774.1,4774.0,3.0,6.0,1798.0,1801.0,1812.0,1816.0,1817.0,1886.0,1898.0,1900.0] || frontsegP(skc11,skc8)* -> equal(skc11,skc8). % 3.84/4.05 4782[0:Res:4392.2,97.1] ssList(nil) ssList(skc11) || equal(skc8,nil) -> equal(skc11,nil)**. % 3.84/4.05 5362[12:SpR:4642.0,3912.2] ssList(skc8) ssList(tl(skc11)) || -> frontsegP(skc11,skc8)*. % 3.84/4.05 5373[12:SSi:5362.0,6.0,1798.0,1801.0,1812.0,1816.0,1817.0,1886.0,1898.0,1900.0] ssList(tl(skc11)) || -> frontsegP(skc11,skc8)*. % 3.84/4.05 5435[12:SoR:5373.0,91.1] ssList(skc11) || -> frontsegP(skc11,skc8)* equal(skc11,nil). % 3.84/4.05 5436[12:SSi:5435.0,3.0] || -> frontsegP(skc11,skc8)* equal(skc11,nil). % 3.84/4.05 5437[12:MRR:5436.1,4459.0] || -> frontsegP(skc11,skc8)*. % 3.84/4.05 5438[12:MRR:4775.0,5437.0] || -> equal(skc11,skc8)**. % 3.84/4.05 5445[12:Rew:5438.0,4389.0] || -> equal(app(skc8,cons(skc10,skc12)),skc8)**. % 3.84/4.05 5529[12:SpR:5445.0,2005.1] ssList(cons(skc10,skc12)) || -> equal(cons(skc10,skc12),tl(skc8))**. % 3.84/4.05 5551[12:Rew:2000.0,5529.1] ssList(cons(skc10,skc12)) || -> equal(cons(skc10,skc12),nil)**. % 3.84/4.05 5552[12:SSi:5551.0,95.0,4.0,2.2] || -> equal(cons(skc10,skc12),nil)**. % 3.84/4.05 5609[12:SpL:5552.0,114.2] ssItem(skc10) ssList(skc12) || equal(nil,nil)* -> . % 3.84/4.05 5617[12:Obv:5609.2] ssItem(skc10) ssList(skc12) || -> . % 3.84/4.05 5618[12:SSi:5617.1,5617.0,2.0,4.0] || -> . % 3.84/4.05 5638[11:Spt:5618.0,1059.0,1888.0] || memberP(skc11,skc13)* -> . % 3.84/4.05 5639[11:Spt:5618.0,1059.1] || -> memberP(skc12,skc13)*. % 3.84/4.05 6195[12:Spt:4390.0] || -> equal(skc11,nil)**. % 3.84/4.05 6198[12:Rew:6195.0,5638.0] || memberP(nil,skc13)* -> . % 3.84/4.05 6203[12:Rew:6195.0,4389.0] || -> equal(app(nil,cons(skc10,skc12)),skc8)**. % 3.84/4.05 6289[12:SpR:6203.0,84.1] ssList(cons(skc10,skc12)) || -> equal(cons(skc10,skc12),skc8)**. % 3.84/4.05 6310[12:SSi:6289.0,95.0,4.0,2.2] || -> equal(cons(skc10,skc12),skc8)**. % 3.84/4.05 6336[12:SpR:6310.0,116.2] ssItem(skc10) ssList(skc12) || -> equal(tl(skc8),skc12)**. % 3.84/4.05 6352[12:Rew:2000.0,6336.2] ssItem(skc10) ssList(skc12) || -> equal(skc12,nil)**. % 3.84/4.05 6353[12:SSi:6352.1,6352.0,2.0,4.0] || -> equal(skc12,nil)**. % 3.84/4.05 6360[12:Rew:6353.0,5639.0] || -> memberP(nil,skc13)*. % 3.84/4.05 6375[12:MRR:6360.0,6198.0] || -> . % 3.84/4.05 6423[12:Spt:6375.0,4390.0,6195.0] || equal(skc11,nil)** -> . % 3.84/4.05 6424[12:Spt:6375.0,4390.1] || -> equal(hd(skc11),hd(skc8))**. % 3.84/4.05 6428[12:SpR:6424.0,122.2] ssList(skc11) || -> equal(skc11,nil) equal(cons(hd(skc8),tl(skc11)),skc11)**. % 3.84/4.05 6432[12:MRR:6428.0,6428.1,3.0,6423.0] || -> equal(cons(hd(skc8),tl(skc11)),skc11)**. % 3.84/4.05 6509[12:SpR:6432.0,2201.1] ssList(tl(skc11)) || -> equal(app(skc8,tl(skc11)),skc11)**. % 3.84/4.05 7340[12:SoR:6509.0,91.1] ssList(skc11) || -> equal(app(skc8,tl(skc11)),skc11)** equal(skc11,nil). % 3.84/4.05 7341[12:SSi:7340.0,3.0] || -> equal(app(skc8,tl(skc11)),skc11)** equal(skc11,nil). % 3.84/4.05 7342[12:MRR:7341.1,6423.0] || -> equal(app(skc8,tl(skc11)),skc11)**. % 4.06/4.29 7344[12:SpR:7342.0,3912.2] ssList(skc8) ssList(tl(skc11)) || -> frontsegP(skc11,skc8)*. % 4.06/4.29 7373[12:SSi:7344.0,6.0,1798.0,1801.0,1812.0,1816.0,1817.0,1886.0,1898.0,1900.0] ssList(tl(skc11)) || -> frontsegP(skc11,skc8)*. % 4.06/4.29 7385[12:SoR:7373.0,91.1] ssList(skc11) || -> frontsegP(skc11,skc8)* equal(skc11,nil). % 4.06/4.29 7386[12:SSi:7385.0,3.0] || -> frontsegP(skc11,skc8)* equal(skc11,nil). % 4.06/4.29 7387[12:MRR:7386.1,6423.0] || -> frontsegP(skc11,skc8)*. % 4.06/4.29 7388[12:MRR:4775.0,7387.0] || -> equal(skc11,skc8)**. % 4.06/4.29 7394[12:Rew:7388.0,4389.0] || -> equal(app(skc8,cons(skc10,skc12)),skc8)**. % 4.06/4.29 7498[12:SpR:7394.0,2005.1] ssList(cons(skc10,skc12)) || -> equal(cons(skc10,skc12),tl(skc8))**. % 4.06/4.29 7524[12:Rew:2000.0,7498.1] ssList(cons(skc10,skc12)) || -> equal(cons(skc10,skc12),nil)**. % 4.06/4.29 7525[12:SSi:7524.0,95.0,4.0,2.2] || -> equal(cons(skc10,skc12),nil)**. % 4.06/4.29 7561[12:SpL:7525.0,114.2] ssItem(skc10) ssList(skc12) || equal(nil,nil)* -> . % 4.06/4.29 7579[12:Obv:7561.2] ssItem(skc10) ssList(skc12) || -> . % 4.06/4.29 7580[12:SSi:7579.1,7579.0,2.0,4.0] || -> . % 4.06/4.29 7608[9:Spt:7580.0,221.0,1817.0] || totalorderP(skc8)* -> . % 4.06/4.29 7609[9:Spt:7580.0,221.1] || -> equal(app(app(skf57(skc8),cons(skf55(skc8),skf58(skc8))),cons(skf56(skc8),skf59(skc8))),skc8)**. % 4.06/4.29 7716[9:Res:1983.2,7608.0] ssList(skc8) singletonP(skc8) || -> . % 4.06/4.29 7717[9:SSi:7716.0,6.0,1798.0,1801.0,1812.0,1816.0] singletonP(skc8) || -> . % 4.06/4.29 7718[9:MRR:63.1,7717.0] || neq(skc9,nil)* -> . % 4.06/4.29 7720[9:Res:426.1,7718.0] ssList(nil) || -> equal(skc9,nil)**. % 4.06/4.29 7723[9:SSi:7720.0,16.0,15.0,12.0,11.0,10.0,14.0,13.0,9.0] || -> equal(skc9,nil)**. % 4.06/4.29 7724[9:MRR:7723.0,1783.0] || -> . % 4.06/4.29 7728[8:Spt:7724.0,222.0,1816.0] || strictorderP(skc8)* -> . % 4.06/4.29 7729[8:Spt:7724.0,222.1] || -> equal(app(app(skf62(skc8),cons(skf60(skc8),skf63(skc8))),cons(skf61(skc8),skf64(skc8))),skc8)**. % 4.06/4.29 7796[8:Res:1982.2,7728.0] ssList(skc8) singletonP(skc8) || -> . % 4.06/4.29 7797[8:SSi:7796.0,6.0,1798.0,1801.0,1812.0] singletonP(skc8) || -> . % 4.06/4.29 7798[8:MRR:63.1,7797.0] || neq(skc9,nil)* -> . % 4.06/4.29 7803[8:Res:426.1,7798.0] ssList(nil) || -> equal(skc9,nil)**. % 4.06/4.29 7806[8:SSi:7803.0,16.0,15.0,12.0,11.0,10.0,14.0,13.0,9.0] || -> equal(skc9,nil)**. % 4.06/4.29 7807[8:MRR:7806.0,1783.0] || -> . % 4.06/4.29 7811[7:Spt:7807.0,267.0,1812.0] || cyclefreeP(skc8)* -> . % 4.06/4.29 7812[7:Spt:7807.0,267.1] || -> leq(skf51(skc8),skf50(skc8))*. % 4.06/4.29 7863[7:Res:1984.2,7811.0] ssList(skc8) singletonP(skc8) || -> . % 4.06/4.29 7864[7:SSi:7863.0,6.0,1798.0,1801.0] singletonP(skc8) || -> . % 4.06/4.29 7865[7:MRR:63.1,7864.0] || neq(skc9,nil)* -> . % 4.06/4.29 7868[7:Res:426.1,7865.0] ssList(nil) || -> equal(skc9,nil)**. % 4.06/4.29 7871[7:SSi:7868.0,16.0,15.0,12.0,11.0,10.0,14.0,13.0,9.0] || -> equal(skc9,nil)**. % 4.06/4.29 7872[7:MRR:7871.0,1783.0] || -> . % 4.06/4.29 7876[6:Spt:7872.0,223.0,1801.0] || totalorderedP(skc8)* -> . % 4.06/4.29 7877[6:Spt:7872.0,223.1] || -> equal(app(app(skf67(skc8),cons(skf65(skc8),skf68(skc8))),cons(skf66(skc8),skf69(skc8))),skc8)**. % 4.06/4.29 7971[6:Res:1986.2,7876.0] ssList(skc8) singletonP(skc8) || -> . % 4.06/4.29 7972[6:SSi:7971.0,6.0,1798.0] singletonP(skc8) || -> . % 4.06/4.29 7973[6:MRR:63.1,7972.0] || neq(skc9,nil)* -> . % 4.06/4.29 7984[6:Res:426.1,7973.0] ssList(nil) || -> equal(skc9,nil)**. % 4.06/4.29 7987[6:SSi:7984.0,16.0,15.0,12.0,11.0,10.0,14.0,13.0,9.0] || -> equal(skc9,nil)**. % 4.06/4.29 7988[6:MRR:7987.0,1783.0] || -> . % 4.06/4.29 7992[5:Spt:7988.0,224.0,1798.0] || strictorderedP(skc8)* -> . % 4.06/4.29 7993[5:Spt:7988.0,224.1] || -> equal(app(app(skf72(skc8),cons(skf70(skc8),skf73(skc8))),cons(skf71(skc8),skf74(skc8))),skc8)**. % 4.06/4.29 8066[5:Res:1985.2,7992.0] ssList(skc8) singletonP(skc8) || -> . % 4.06/4.29 8067[5:SSi:8066.0,6.0] singletonP(skc8) || -> . % 4.06/4.29 8068[5:MRR:63.1,8067.0] || neq(skc9,nil)* -> . % 4.06/4.29 8075[5:Res:426.1,8068.0] ssList(nil) || -> equal(skc9,nil)**. % 4.06/4.29 8078[5:SSi:8075.0,16.0,15.0,12.0,11.0,10.0,14.0,13.0,9.0] || -> equal(skc9,nil)**. % 4.06/4.29 8079[5:MRR:8078.0,1783.0] || -> . % 4.06/4.29 8083[2:Spt:8079.0,241.1] || -> equal(skc8,nil)**. % 4.06/4.29 8322[2:Rew:8083.0,3891.2] ssList(nil) ssList(skc12) || equal(nil,nil) -> equal(skc12,nil)**. % 4.06/4.29 8323[2:Obv:8322.2] ssList(nil) ssList(skc12) || -> equal(skc12,nil)**. % 4.06/4.29 8324[2:SSi:8323.1,8323.0,2.0,16.0,15.0,12.0,11.0,10.0,14.0,13.0,9.0] || -> equal(skc12,nil)**. % 4.06/4.29 8328[2:Rew:8324.0,1059.1] || -> memberP(skc11,skc13)* memberP(nil,skc13). % 4.06/4.29 8346[2:Rew:8083.0,4782.2] ssList(nil) ssList(skc11) || equal(nil,nil) -> equal(skc11,nil)**. % 4.06/4.29 8347[2:Obv:8346.2] ssList(nil) ssList(skc11) || -> equal(skc11,nil)**. % 4.06/4.29 8348[2:SSi:8347.1,8347.0,3.0,16.0,15.0,12.0,11.0,10.0,14.0,13.0,9.0] || -> equal(skc11,nil)**. % 4.06/4.29 8350[2:Rew:8348.0,8328.0] || -> memberP(nil,skc13)* memberP(nil,skc13)*. % 4.06/4.29 8361[2:Obv:8350.0] || -> memberP(nil,skc13)*. % 4.06/4.29 8950[2:Res:8361.0,73.1] ssItem(skc13) || -> . % 4.06/4.29 8951[2:SSi:8950.0,1.0] || -> . % 4.06/4.29 8952[1:Spt:8951.0,247.1] || -> equal(skc8,nil)**. % 4.06/4.29 9037[1:Rew:8952.0,3891.2] ssList(nil) ssList(skc12) || equal(nil,nil) -> equal(skc12,nil)**. % 4.06/4.29 9038[1:Obv:9037.2] ssList(nil) ssList(skc12) || -> equal(skc12,nil)**. % 4.06/4.29 9039[1:SSi:9038.0,16.0,15.0,12.0,11.0,10.0,14.0,13.0,9.0] ssList(skc12) || -> equal(skc12,nil)**. % 4.06/4.29 9040[1:MRR:9039.0,2.0] || -> equal(skc12,nil)**. % 4.06/4.29 9051[1:Rew:9040.0,1059.1] || -> memberP(skc11,skc13)* memberP(nil,skc13). % 4.06/4.29 9063[1:Rew:8952.0,4782.2] ssList(nil) ssList(skc11) || equal(nil,nil) -> equal(skc11,nil)**. % 4.06/4.29 9064[1:Obv:9063.2] ssList(nil) ssList(skc11) || -> equal(skc11,nil)**. % 4.06/4.29 9065[1:SSi:9064.0,16.0,15.0,12.0,11.0,10.0,14.0,13.0,9.0] ssList(skc11) || -> equal(skc11,nil)**. % 4.06/4.29 9066[1:MRR:9065.0,3.0] || -> equal(skc11,nil)**. % 4.06/4.29 9069[1:Rew:9066.0,9051.0] || -> memberP(nil,skc13)* memberP(nil,skc13)*. % 4.06/4.29 9078[1:Obv:9069.0] || -> memberP(nil,skc13)*. % 4.06/4.29 9725[1:Res:9078.0,73.1] ssItem(skc13) || -> . % 4.06/4.29 9726[1:SSi:9725.0,1.0] || -> . % 4.06/4.29 % SZS output end Refutation % 4.06/4.29 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 ax16 ax26 ax46 ax52 ax58 ax15 ax21 ax23 ax25 ax78 ax81 ax83 ax85 ax41 ax5 ax6 ax43 ax67 ax70 ax86 ax82 ax12 ax11 ax10 ax9 % 4.06/4.29 %------------------------------------------------------------------------------