%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : SWC380+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:42 EDT 2022 % Result : Theorem 3.36s 3.57s % Output : Refutation 3.52s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : SWC380+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 : Sat Jun 11 23:39:05 EDT 2022 % 0.12/0.33 % CPUTime : % 3.36/3.57 % 3.36/3.57 SPASS V 3.9 % 3.36/3.57 SPASS beiseite: Proof found. % 3.36/3.57 % SZS status Theorem % 3.36/3.57 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 3.36/3.57 SPASS derived 4843 clauses, backtracked 1532 clauses, performed 44 splits and kept 3612 clauses. % 3.36/3.57 SPASS allocated 104950 KBytes. % 3.36/3.57 SPASS spent 0:00:03.23 on the problem. % 3.36/3.57 0:00:00.04 for the input. % 3.36/3.57 0:00:00.07 for the FLOTTER CNF translation. % 3.36/3.57 0:00:00.05 for inferences. % 3.36/3.57 0:00:00.06 for the backtracking. % 3.36/3.57 0:00:02.78 for the reduction. % 3.36/3.57 % 3.36/3.57 % 3.36/3.57 Here is a proof with depth 7, length 149 : % 3.36/3.57 % SZS output start Refutation % 3.36/3.57 1[0:Inp] || -> ssList(skc5)*. % 3.36/3.57 2[0:Inp] || -> ssList(skc4)*. % 3.36/3.57 3[0:Inp] || -> ssItem(skc7)*. % 3.36/3.57 4[0:Inp] || -> ssItem(skc6)*. % 3.36/3.57 5[0:Inp] || -> ssList(nil)*. % 3.36/3.57 6[0:Inp] || -> cyclefreeP(nil)*. % 3.36/3.57 7[0:Inp] || -> totalorderP(nil)*. % 3.36/3.57 8[0:Inp] || -> strictorderP(nil)*. % 3.36/3.57 9[0:Inp] || -> totalorderedP(nil)*. % 3.36/3.57 10[0:Inp] || -> strictorderedP(nil)*. % 3.36/3.57 11[0:Inp] || -> duplicatefreeP(nil)*. % 3.36/3.57 12[0:Inp] || -> equalelemsP(nil)*. % 3.36/3.57 51[0:Inp] || -> ssList(skf46(u,v))*. % 3.36/3.57 52[0:Inp] || -> ssItem(skf45(u,v))*. % 3.36/3.57 53[0:Inp] || equal(skc7,skc6)** -> . % 3.36/3.58 60[0:Inp] || -> SkP0(u,v)* neq(v,nil)*. % 3.36/3.58 69[0:Inp] || SkP0(skc4,skc5) -> neq(skc5,nil)*. % 3.36/3.58 71[0:Inp] ssItem(u) || -> cyclefreeP(cons(u,nil))*. % 3.36/3.58 72[0:Inp] ssItem(u) || -> totalorderP(cons(u,nil))*. % 3.36/3.58 73[0:Inp] ssItem(u) || -> strictorderP(cons(u,nil))*. % 3.36/3.58 74[0:Inp] ssItem(u) || -> totalorderedP(cons(u,nil))*. % 3.36/3.58 75[0:Inp] ssItem(u) || -> strictorderedP(cons(u,nil))*. % 3.36/3.58 76[0:Inp] ssItem(u) || -> duplicatefreeP(cons(u,nil))*. % 3.36/3.58 77[0:Inp] ssItem(u) || -> equalelemsP(cons(u,nil))*. % 3.36/3.58 79[0:Inp] || neq(skc5,nil)* SkP0(skc4,skc5) -> . % 3.36/3.58 80[0:Inp] ssList(u) || -> equal(app(nil,u),u)**. % 3.36/3.58 84[0:Inp] ssList(u) || -> ssItem(hd(u))* equal(nil,u). % 3.36/3.58 85[0:Inp] ssList(u) || -> ssList(tl(u))* equal(nil,u). % 3.36/3.58 86[0:Inp] || -> SkP0(u,v) equal(cons(skf45(u,v),nil),u)**. % 3.36/3.58 90[0:Inp] ssItem(u) ssList(v) || -> ssList(cons(u,v))*. % 3.36/3.58 109[0:Inp] ssItem(u) ssList(v) || equal(cons(u,v),nil)** -> . % 3.36/3.58 110[0:Inp] ssItem(u) ssList(v) || -> equal(hd(cons(u,v)),u)**. % 3.36/3.58 111[0:Inp] ssItem(u) ssList(v) || -> equal(tl(cons(u,v)),v)**. % 3.36/3.58 117[0:Inp] ssList(u) || -> equal(nil,u) equal(cons(hd(u),tl(u)),u)**. % 3.36/3.58 119[0:Inp] || -> equal(app(cons(skf45(u,v),nil),skf46(v,u)),v)** SkP0(u,v). % 3.36/3.58 121[0:Inp] ssList(u) ssItem(v) || equal(cons(v,nil),u)*+ -> singletonP(u)*. % 3.36/3.58 122[0:Inp] ssList(u) ssList(v) || equal(v,u) neq(v,u)* -> . % 3.36/3.58 128[0:Inp] ssItem(u) ssList(v) || -> equal(app(cons(u,nil),v),cons(u,v))**. % 3.36/3.58 131[0:Inp] ssItem(u) || memberP(v,u)* equal(cons(u,nil),w)*+ -> SkP0(w,v)*. % 3.36/3.58 134[0:Inp] ssList(u) ssList(v) || -> equal(nil,v) equal(hd(app(v,u)),hd(v))**. % 3.36/3.58 147[0:Inp] ssList(u) ssList(v) ssItem(w) || memberP(v,w) -> memberP(app(v,u),w)*. % 3.36/3.58 149[0:Inp] ssList(u) ssItem(v) ssItem(w) || equal(w,v) -> memberP(cons(v,u),w)*. % 3.36/3.58 153[0:Inp] ssList(u) ssItem(v) || totalorderedP(cons(v,u))* -> leq(v,hd(u)) equal(nil,u). % 3.36/3.58 154[0:Inp] ssList(u) ssItem(v) || strictorderedP(cons(v,u))* -> lt(v,hd(u)) equal(nil,u). % 3.36/3.58 197[0:MRR:69.0,60.1] || -> neq(skc5,nil)*. % 3.36/3.58 198[0:MRR:79.0,197.0] || SkP0(skc4,skc5)* -> . % 3.36/3.58 199[0:Rew:86.0,119.0] || -> SkP0(u,v) equal(app(u,skf46(v,u)),v)**. % 3.36/3.58 253[0:Res:2.0,117.0] || -> equal(skc4,nil) equal(cons(hd(skc4),tl(skc4)),skc4)**. % 3.36/3.58 257[0:Res:2.0,109.0] ssItem(u) || equal(cons(u,skc4),nil)** -> . % 3.36/3.58 278[0:Res:2.0,84.0] || -> ssItem(hd(skc4))* equal(skc4,nil). % 3.36/3.58 310[0:Res:2.0,153.1] ssItem(u) || totalorderedP(cons(u,skc4))* -> leq(u,hd(skc4)) equal(skc4,nil). % 3.36/3.58 323[0:Res:2.0,121.1] ssItem(u) || equal(cons(u,nil),skc4)** -> singletonP(skc4). % 3.36/3.58 418[0:Res:1.0,134.0] ssList(u) || -> equal(skc5,nil) equal(hd(app(skc5,u)),hd(skc5))**. % 3.36/3.58 422[0:Res:1.0,122.0] ssList(u) || equal(skc5,u) neq(skc5,u)* -> . % 3.36/3.58 424[0:Res:1.0,117.0] || -> equal(skc5,nil) equal(cons(hd(skc5),tl(skc5)),skc5)**. % 3.36/3.58 429[0:Res:1.0,110.0] ssItem(u) || -> equal(hd(cons(u,skc5)),u)**. % 3.36/3.58 441[0:Res:1.0,90.0] ssItem(u) || -> ssList(cons(u,skc5))*. % 3.36/3.58 450[0:Res:1.0,85.0] || -> ssList(tl(skc5))* equal(skc5,nil). % 3.36/3.58 482[0:Res:1.0,154.1] ssItem(u) || strictorderedP(cons(u,skc5))* -> lt(u,hd(skc5)) equal(skc5,nil). % 3.36/3.58 547[1:Spt:418.0,418.2] ssList(u) || -> equal(hd(app(skc5,u)),hd(skc5))**. % 3.36/3.58 555[2:Spt:482.3] || -> equal(skc5,nil)**. % 3.36/3.58 556[2:Rew:555.0,547.1] ssList(u) || -> equal(hd(app(nil,u)),hd(nil))**. % 3.36/3.58 572[2:Rew:555.0,441.1] ssItem(u) || -> ssList(cons(u,nil))*. % 3.36/3.58 573[2:Rew:555.0,429.1] ssItem(u) || -> equal(hd(cons(u,nil)),u)**. % 3.36/3.58 727[2:Rew:80.1,556.1] ssList(u) || -> equal(hd(u),hd(nil))*. % 3.36/3.58 1176[2:SpR:573.1,727.1] ssItem(u) ssList(cons(u,nil)) || -> equal(u,hd(nil))*. % 3.36/3.58 1179[2:SSi:1176.1,77.1,76.1,73.1,72.1,71.1,75.1,74.1,572.1] ssItem(u) || -> equal(u,hd(nil))*. % 3.36/3.58 1248[2:SpR:1179.1,1179.1] ssItem(u) ssItem(v) || -> equal(v,u)*. % 3.36/3.58 1289[2:EmS:1248.0,3.0] ssItem(u) || -> equal(u,skc7)*. % 3.36/3.58 1311[2:EmS:1289.0,4.0] || -> equal(skc7,skc6)**. % 3.36/3.58 1312[2:MRR:1311.0,53.0] || -> . % 3.36/3.58 1448[2:Spt:1312.0,482.3,555.0] || equal(skc5,nil)** -> . % 3.36/3.58 1449[2:Spt:1312.0,482.0,482.1,482.2] ssItem(u) || strictorderedP(cons(u,skc5))* -> lt(u,hd(skc5)). % 3.36/3.58 1450[2:MRR:450.1,1448.0] || -> ssList(tl(skc5))*. % 3.36/3.58 1455[2:MRR:424.0,1448.0] || -> equal(cons(hd(skc5),tl(skc5)),skc5)**. % 3.36/3.58 1463[3:Spt:310.3] || -> equal(skc4,nil)**. % 3.36/3.58 1471[3:Rew:1463.0,198.0] || SkP0(nil,skc5)* -> . % 3.36/3.58 1503[3:Rew:1463.0,257.1] ssItem(u) || equal(cons(u,nil),nil)** -> . % 3.36/3.58 1795[0:SpR:86.1,77.1] ssItem(skf45(u,v)) || -> SkP0(u,v)* equalelemsP(u). % 3.36/3.58 1796[0:SpR:86.1,76.1] ssItem(skf45(u,v)) || -> SkP0(u,v)* duplicatefreeP(u). % 3.36/3.58 1797[0:SpR:86.1,73.1] ssItem(skf45(u,v)) || -> SkP0(u,v)* strictorderP(u). % 3.36/3.58 1798[0:SpR:86.1,72.1] ssItem(skf45(u,v)) || -> SkP0(u,v)* totalorderP(u). % 3.36/3.58 1799[0:SpR:86.1,71.1] ssItem(skf45(u,v)) || -> SkP0(u,v)* cyclefreeP(u). % 3.36/3.58 1800[0:SpR:86.1,75.1] ssItem(skf45(u,v)) || -> SkP0(u,v)* strictorderedP(u). % 3.36/3.58 1801[0:SpR:86.1,74.1] ssItem(skf45(u,v)) || -> SkP0(u,v)* totalorderedP(u). % 3.36/3.58 1804[0:SpR:86.1,90.2] ssItem(skf45(u,v)) ssList(nil) || -> SkP0(u,v)* ssList(u). % 3.36/3.58 1806[3:SpL:86.1,1503.1] ssItem(skf45(u,v)) || equal(u,nil) -> SkP0(u,v)*. % 3.36/3.58 1807[0:SSi:1795.0,52.0] || -> SkP0(u,v)* equalelemsP(u). % 3.36/3.58 1808[0:SSi:1796.0,52.0] || -> SkP0(u,v)* duplicatefreeP(u). % 3.36/3.58 1809[0:SSi:1797.0,52.0] || -> SkP0(u,v)* strictorderP(u). % 3.36/3.58 1810[0:SSi:1798.0,52.0] || -> SkP0(u,v)* totalorderP(u). % 3.36/3.58 1811[0:SSi:1799.0,52.0] || -> SkP0(u,v)* cyclefreeP(u). % 3.36/3.58 1812[0:SSi:1800.0,52.0] || -> SkP0(u,v)* strictorderedP(u). % 3.36/3.58 1813[0:SSi:1801.0,52.0] || -> SkP0(u,v)* totalorderedP(u). % 3.36/3.58 1816[3:SSi:1806.0,52.0] || equal(u,nil) -> SkP0(u,v)*. % 3.36/3.58 1848[3:Res:1816.1,1471.0] || equal(nil,nil)* -> . % 3.36/3.58 1849[3:Obv:1848.0] || -> . % 3.36/3.58 1850[3:Spt:1849.0,310.3,1463.0] || equal(skc4,nil)** -> . % 3.36/3.58 1851[3:Spt:1849.0,310.0,310.1,310.2] ssItem(u) || totalorderedP(cons(u,skc4))* -> leq(u,hd(skc4)). % 3.36/3.58 1853[3:MRR:278.1,1850.0] || -> ssItem(hd(skc4))*. % 3.36/3.58 1858[3:MRR:253.0,1850.0] || -> equal(cons(hd(skc4),tl(skc4)),skc4)**. % 3.36/3.58 1865[0:SSi:1804.1,1804.0,12.0,11.0,8.0,7.0,6.0,10.0,9.0,5.0,52.0] || -> SkP0(u,v)* ssList(u). % 3.36/3.58 1883[0:Res:1813.0,198.0] || -> totalorderedP(skc4)*. % 3.36/3.58 1884[0:Res:1812.0,198.0] || -> strictorderedP(skc4)*. % 3.36/3.58 1885[0:Res:1811.0,198.0] || -> cyclefreeP(skc4)*. % 3.36/3.58 1886[0:Res:1810.0,198.0] || -> totalorderP(skc4)*. % 3.36/3.58 1887[0:Res:1809.0,198.0] || -> strictorderP(skc4)*. % 3.36/3.58 1888[0:Res:1808.0,198.0] || -> duplicatefreeP(skc4)*. % 3.36/3.58 1889[0:Res:1807.0,198.0] || -> equalelemsP(skc4)*. % 3.36/3.58 1980[0:SpR:86.1,111.2] ssItem(skf45(u,v)) ssList(nil) || -> SkP0(u,v)* equal(tl(u),nil). % 3.36/3.58 1985[0:SSi:1980.1,1980.0,12.0,11.0,8.0,7.0,6.0,10.0,9.0,5.0,52.0] || -> SkP0(u,v)* equal(tl(u),nil). % 3.36/3.58 2007[0:SpR:86.1,110.2] ssItem(skf45(u,v)) ssList(nil) || -> SkP0(u,v) equal(skf45(u,v),hd(u))**. % 3.36/3.58 2012[0:SSi:2007.1,2007.0,12.0,11.0,8.0,7.0,6.0,10.0,9.0,5.0,52.0] || -> SkP0(u,v) equal(skf45(u,v),hd(u))**. % 3.36/3.58 2013[0:Rew:2012.1,86.1] || -> SkP0(u,v)* equal(cons(hd(u),nil),u)**. % 3.36/3.58 2020[0:Res:1985.0,198.0] || -> equal(tl(skc4),nil)**. % 3.36/3.58 2022[3:Rew:2020.0,1858.0] || -> equal(cons(hd(skc4),nil),skc4)**. % 3.36/3.58 2112[0:SpR:2012.1,52.0] || -> SkP0(u,v)* ssItem(hd(u)). % 3.36/3.58 2491[3:SpL:2022.0,323.1] ssItem(hd(skc4)) || equal(skc4,skc4) -> singletonP(skc4)*. % 3.36/3.58 2492[3:Obv:2491.1] ssItem(hd(skc4)) || -> singletonP(skc4)*. % 3.36/3.58 2493[3:SSi:2492.0,1853.0] || -> singletonP(skc4)*. % 3.36/3.58 2963[3:SpR:2022.0,128.2] ssItem(hd(skc4)) ssList(u) || -> equal(cons(hd(skc4),u),app(skc4,u))**. % 3.36/3.58 3086[0:SpR:199.1,134.3] ssList(skf46(u,v)) ssList(v) || -> SkP0(v,u)* equal(nil,v) equal(hd(u),hd(v)). % 3.52/3.75 3090[0:SSi:3086.0,51.0] ssList(u) || -> SkP0(u,v)* equal(nil,u) equal(hd(v),hd(u)). % 3.52/3.75 3091[0:MRR:3090.0,1865.1] || -> SkP0(u,v)* equal(nil,u) equal(hd(v),hd(u)). % 3.52/3.75 3112[0:EqR:131.2] ssItem(u) || memberP(v,u) -> SkP0(cons(u,nil),v)*. % 3.52/3.75 3269[0:SpR:2013.1,3112.2] ssItem(hd(u)) || memberP(v,hd(u))* -> SkP0(u,w)* SkP0(u,v). % 3.52/3.75 3273[0:Con:3269.2] ssItem(hd(u)) || memberP(v,hd(u))* -> SkP0(u,v). % 3.52/3.75 3274[0:MRR:3273.0,2112.1] || memberP(u,hd(v))* -> SkP0(v,u). % 3.52/3.75 3845[3:SpR:2022.0,149.4] ssList(nil) ssItem(hd(skc4)) ssItem(u) || equal(u,hd(skc4)) -> memberP(skc4,u)*. % 3.52/3.75 3854[3:SSi:3845.1,3845.0,1853.0,12.0,11.0,8.0,7.0,6.0,10.0,9.0,5.0] ssItem(u) || equal(u,hd(skc4)) -> memberP(skc4,u)*. % 3.52/3.75 3907[0:Res:3091.0,198.0] || -> equal(skc4,nil) equal(hd(skc5),hd(skc4))**. % 3.52/3.75 4791[3:MRR:3907.0,1850.0] || -> equal(hd(skc5),hd(skc4))**. % 3.52/3.75 4793[3:Rew:4791.0,1455.0] || -> equal(cons(hd(skc4),tl(skc5)),skc5)**. % 3.52/3.75 4817[3:SSi:2963.0,1853.0] ssList(u) || -> equal(cons(hd(skc4),u),app(skc4,u))**. % 3.52/3.75 6300[0:Res:197.0,422.2] ssList(nil) || equal(skc5,nil)** -> . % 3.52/3.75 6380[3:SpR:4817.1,4793.0] ssList(tl(skc5)) || -> equal(app(skc4,tl(skc5)),skc5)**. % 3.52/3.75 6580[3:SSi:6380.0,1450.0] || -> equal(app(skc4,tl(skc5)),skc5)**. % 3.52/3.75 6825[3:SpR:6580.0,147.4] ssList(tl(skc5)) ssList(skc4) ssItem(u) || memberP(skc4,u) -> memberP(skc5,u)*. % 3.52/3.75 7237[3:SSi:6825.1,6825.0,2.0,1885.0,1886.0,1887.0,1888.0,1889.0,2493.0,1884.0,1883.0,1450.0] ssItem(u) || memberP(skc4,u) -> memberP(skc5,u)*. % 3.52/3.75 7700[3:Res:7237.2,3274.0] ssItem(hd(u)) || memberP(skc4,hd(u))* -> SkP0(u,skc5). % 3.52/3.75 7701[3:MRR:7700.0,2112.1] || memberP(skc4,hd(u))* -> SkP0(u,skc5). % 3.52/3.75 7713[3:Res:3854.2,7701.0] ssItem(hd(u)) || equal(hd(u),hd(skc4)) -> SkP0(u,skc5)*. % 3.52/3.75 7714[3:MRR:7713.0,2112.1] || equal(hd(u),hd(skc4)) -> SkP0(u,skc5)*. % 3.52/3.75 7715[3:Res:7714.1,198.0] || equal(hd(skc4),hd(skc4))* -> . % 3.52/3.75 7716[3:Obv:7715.0] || -> . % 3.52/3.75 7717[1:Spt:7716.0,418.1] || -> equal(skc5,nil)**. % 3.52/3.75 7856[1:Rew:7717.0,6300.1] ssList(nil) || equal(nil,nil)* -> . % 3.52/3.75 7857[1:Obv:7856.1] ssList(nil) || -> . % 3.52/3.75 7858[1:SSi:7857.0,12.0,11.0,8.0,7.0,6.0,10.0,9.0,5.0] || -> . % 3.52/3.75 % SZS output end Refutation % 3.52/3.75 Formulae used in the proof : co1 ax2 ax17 ax60 ax62 ax64 ax66 ax69 ax72 ax74 ax59 ax61 ax63 ax65 ax68 ax71 ax73 ax28 ax75 ax76 ax16 ax21 ax23 ax25 ax78 ax4 ax15 ax81 ax85 ax36 ax37 ax67 ax70 % 3.52/3.75 %------------------------------------------------------------------------------