%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : SWC067+1 : TPTP v8.1.0. Released v2.4.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n011.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:01:30 EDT 2022 % Result : Theorem 14.96s 15.13s % Output : Refutation 14.96s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.12 % Problem : SWC067+1 : TPTP v8.1.0. Released v2.4.0. % 0.06/0.12 % Command : run_spass %d %s % 0.12/0.33 % Computer : n011.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 10:34:47 EDT 2022 % 0.12/0.33 % CPUTime : % 14.96/15.13 % 14.96/15.13 SPASS V 3.9 % 14.96/15.13 SPASS beiseite: Proof found. % 14.96/15.13 % SZS status Theorem % 14.96/15.13 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 14.96/15.13 SPASS derived 14147 clauses, backtracked 4421 clauses, performed 82 splits and kept 8545 clauses. % 14.96/15.13 SPASS allocated 114675 KBytes. % 14.96/15.13 SPASS spent 0:0:13.28 on the problem. % 14.96/15.13 0:00:00.04 for the input. % 14.96/15.13 0:00:00.07 for the FLOTTER CNF translation. % 14.96/15.13 0:00:00.16 for inferences. % 14.96/15.13 0:00:00.24 for the backtracking. % 14.96/15.13 0:0:12.54 for the reduction. % 14.96/15.13 % 14.96/15.13 % 14.96/15.13 Here is a proof with depth 6, length 114 : % 14.96/15.13 % SZS output start Refutation % 14.96/15.13 1[0:Inp] || -> ssList(skc9)*. % 14.96/15.13 2[0:Inp] || -> ssList(skc8)*. % 14.96/15.13 3[0:Inp] || -> ssList(skc7)*. % 14.96/15.13 4[0:Inp] || -> ssList(skc6)*. % 14.96/15.13 5[0:Inp] || -> strictorderedP(skc6)*. % 14.96/15.13 6[0:Inp] || -> ssItem(skc11)*. % 14.96/15.13 7[0:Inp] || -> ssItem(skc10)*. % 14.96/15.13 8[0:Inp] || -> ssList(nil)*. % 14.96/15.13 9[0:Inp] || -> cyclefreeP(nil)*. % 14.96/15.13 10[0:Inp] || -> totalorderP(nil)*. % 14.96/15.13 11[0:Inp] || -> strictorderP(nil)*. % 14.96/15.13 12[0:Inp] || -> totalorderedP(nil)*. % 14.96/15.13 13[0:Inp] || -> strictorderedP(nil)*. % 14.96/15.13 14[0:Inp] || -> duplicatefreeP(nil)*. % 14.96/15.13 15[0:Inp] || -> equalelemsP(nil)*. % 14.96/15.13 54[0:Inp] || equal(skc11,skc10)** -> . % 14.96/15.13 61[0:Inp] || -> SkP0(u,v)* equal(nil,v). % 14.96/15.13 67[0:Inp] ssList(u) || -> segmentP(u,u)*. % 14.96/15.13 68[0:Inp] ssList(u) || -> segmentP(u,nil)*. % 14.96/15.13 70[0:Inp] || -> equal(app(app(skc8,skc6),skc9),skc7)**. % 14.96/15.13 71[0:Inp] || equal(skc6,nil) -> equal(skc7,nil)**. % 14.96/15.13 72[0:Inp] || SkP0(skc6,skc7) -> neq(skc7,nil)*. % 14.96/15.13 73[0:Inp] || equal(nil,u) -> SkP0(u,v)*. % 14.96/15.13 83[0:Inp] ssList(u) || -> equal(app(nil,u),u)**. % 14.96/15.13 84[0:Inp] ssList(u) || -> equal(app(u,nil),u)**. % 14.96/15.13 92[0:Inp] ssItem(u) ssList(v) || -> ssList(cons(u,v))*. % 14.96/15.13 93[0:Inp] ssList(u) ssList(v) || -> ssList(app(v,u))*. % 14.96/15.13 96[0:Inp] ssList(u) || rearsegP(nil,u)* -> equal(nil,u). % 14.96/15.13 109[0:Inp] ssList(u) ssList(v) || -> neq(v,u)* equal(v,u). % 14.96/15.13 112[0:Inp] ssItem(u) ssList(v) || -> equal(hd(cons(u,v)),u)**. % 14.96/15.13 131[0:Inp] ssList(u) ssList(v) || equal(app(v,u),nil)** -> equal(nil,v). % 14.96/15.13 134[0:Inp] ssList(u) ssList(v) || -> equal(nil,v) equal(hd(app(v,u)),hd(v))**. % 14.96/15.13 145[0:Inp] ssList(u) ssList(v) ssList(w) || equal(app(w,u),v)*+ -> rearsegP(v,u)*. % 14.96/15.13 153[0:Inp] ssList(u) ssItem(v) || totalorderedP(cons(v,u))* -> leq(v,hd(u)) equal(nil,u). % 14.96/15.13 154[0:Inp] ssList(u) ssItem(v) || strictorderedP(cons(v,u)) -> lt(v,hd(u))* equal(nil,u). % 14.96/15.13 156[0:Inp] ssList(u) || neq(u,nil) segmentP(skc6,u) segmentP(skc7,u)* SkP0(skc6,skc7) -> . % 14.96/15.13 161[0:Inp] ssList(u) ssList(v) ssList(w) || -> equal(app(app(w,v),u),app(w,app(v,u)))**. % 14.96/15.13 182[0:Inp] ssList(u) ssList(v) ssList(w) ssList(x) || segmentP(u,v) -> segmentP(app(app(w,u),x),v)*. % 14.96/15.13 203[0:Rew:161.3,182.5] ssList(u) ssList(v) ssList(w) ssList(x) || segmentP(x,w) -> segmentP(app(v,app(x,u)),w)*. % 14.96/15.13 263[0:Res:4.0,112.0] ssItem(u) || -> equal(hd(cons(u,skc6)),u)**. % 14.96/15.13 275[0:Res:4.0,92.0] ssItem(u) || -> ssList(cons(u,skc6))*. % 14.96/15.13 285[0:Res:4.0,83.0] || -> equal(app(nil,skc6),skc6)**. % 14.96/15.13 286[0:Res:4.0,84.0] || -> equal(app(skc6,nil),skc6)**. % 14.96/15.13 291[0:Res:4.0,67.0] || -> segmentP(skc6,skc6)*. % 14.96/15.13 292[0:Res:4.0,68.0] || -> segmentP(skc6,nil)*. % 14.96/15.13 317[0:Res:4.0,153.1] ssItem(u) || totalorderedP(cons(u,skc6))* -> leq(u,hd(skc6)) equal(skc6,nil). % 14.96/15.13 335[0:Res:4.0,93.1] ssList(u) || -> ssList(app(u,skc6))*. % 14.96/15.13 415[0:Res:3.0,156.0] || neq(skc7,nil) segmentP(skc7,skc7)* segmentP(skc6,skc7) SkP0(skc6,skc7) -> . % 14.96/15.13 428[0:Res:3.0,134.0] ssList(u) || -> equal(skc7,nil) equal(hd(app(skc7,u)),hd(skc7))**. % 14.96/15.13 467[0:Res:3.0,67.0] || -> segmentP(skc7,skc7)*. % 14.96/15.13 494[0:Res:3.0,154.1] ssItem(u) || strictorderedP(cons(u,skc7)) -> lt(u,hd(skc7))* equal(skc7,nil). % 14.96/15.13 563[0:MRR:415.0,415.1,72.1,467.0] || SkP0(skc6,skc7) segmentP(skc6,skc7)* -> . % 14.96/15.13 569[1:Spt:428.0,428.2] ssList(u) || -> equal(hd(app(skc7,u)),hd(skc7))**. % 14.96/15.13 573[2:Spt:317.3] || -> equal(skc6,nil)**. % 14.96/15.13 578[2:Rew:573.0,563.0] || SkP0(nil,skc7) segmentP(skc6,skc7)* -> . % 14.96/15.13 584[2:Rew:573.0,71.0] || equal(nil,nil) -> equal(skc7,nil)**. % 14.96/15.13 683[2:Rew:573.0,292.0] || -> segmentP(nil,nil)*. % 14.96/15.13 737[2:Obv:584.0] || -> equal(skc7,nil)**. % 14.96/15.13 911[2:Rew:573.0,578.1,737.0,578.1,737.0,578.0] || SkP0(nil,nil) segmentP(nil,nil)* -> . % 14.96/15.13 912[2:MRR:911.1,683.0] || SkP0(nil,nil)* -> . % 14.96/15.13 1099[2:Res:73.1,912.0] || equal(nil,nil)* -> . % 14.96/15.13 1100[2:Obv:1099.0] || -> . % 14.96/15.13 1101[2:Spt:1100.0,317.3,573.0] || equal(skc6,nil)** -> . % 14.96/15.13 1102[2:Spt:1100.0,317.0,317.1,317.2] ssItem(u) || totalorderedP(cons(u,skc6))* -> leq(u,hd(skc6)). % 14.96/15.13 1115[3:Spt:494.3] || -> equal(skc7,nil)**. % 14.96/15.13 1149[3:Rew:1115.0,569.1] ssList(u) || -> equal(hd(app(nil,u)),hd(nil))**. % 14.96/15.13 1295[3:Rew:83.1,1149.1] ssList(u) || -> equal(hd(u),hd(nil))*. % 14.96/15.13 1446[3:SpR:263.1,1295.1] ssItem(u) ssList(cons(u,skc6)) || -> equal(u,hd(nil))*. % 14.96/15.13 1449[3:SSi:1446.1,275.1] ssItem(u) || -> equal(u,hd(nil))*. % 14.96/15.13 1539[3:SpR:1449.1,1449.1] ssItem(u) ssItem(v) || -> equal(v,u)*. % 14.96/15.13 1674[3:EmS:1539.0,6.0] ssItem(u) || -> equal(u,skc11)*. % 14.96/15.13 1696[3:EmS:1674.0,7.0] || -> equal(skc11,skc10)**. % 14.96/15.13 1697[3:MRR:1696.0,54.0] || -> . % 14.96/15.13 1925[3:Spt:1697.0,494.3,1115.0] || equal(skc7,nil)** -> . % 14.96/15.13 1926[3:Spt:1697.0,494.0,494.1,494.2] ssItem(u) || strictorderedP(cons(u,skc7)) -> lt(u,hd(skc7))*. % 14.96/15.13 1943[4:Spt:156.0,156.1,156.2,156.3] ssList(u) || neq(u,nil) segmentP(skc6,u) segmentP(skc7,u)* -> . % 14.96/15.13 3927[0:SpL:70.0,145.3] ssList(skc9) ssList(u) ssList(app(skc8,skc6)) || equal(skc7,u) -> rearsegP(u,skc9)*. % 14.96/15.13 3935[0:SSi:3927.2,3927.0,335.0,2.0,1.1] ssList(u) || equal(skc7,u) -> rearsegP(u,skc9)*. % 14.96/15.13 3963[0:Res:3935.2,96.1] ssList(nil) ssList(skc9) || equal(skc7,nil) -> equal(skc9,nil)**. % 14.96/15.13 4464[0:SpR:161.3,70.0] ssList(skc9) ssList(skc6) ssList(skc8) || -> equal(app(skc8,app(skc6,skc9)),skc7)**. % 14.96/15.13 15848[0:SSi:4464.2,4464.1,4464.0,2.0,4.0,5.0,1.0] || -> equal(app(skc8,app(skc6,skc9)),skc7)**. % 14.96/15.13 16215[0:SpR:15848.0,203.5] ssList(skc9) ssList(skc8) ssList(u) ssList(skc6) || segmentP(skc6,u) -> segmentP(skc7,u)*. % 14.96/15.13 19217[0:SSi:16215.3,16215.1,16215.0,4.0,5.0,2.0,1.0] ssList(u) || segmentP(skc6,u) -> segmentP(skc7,u)*. % 14.96/15.13 19218[4:MRR:1943.3,19217.2] ssList(u) || neq(u,nil) segmentP(skc6,u)* -> . % 14.96/15.13 20003[4:Res:291.0,19218.2] ssList(skc6) || neq(skc6,nil)* -> . % 14.96/15.13 20037[4:SSi:20003.0,4.0,5.0] || neq(skc6,nil)* -> . % 14.96/15.13 20109[4:Res:109.2,20037.0] ssList(nil) ssList(skc6) || -> equal(skc6,nil)**. % 14.96/15.13 20113[4:SSi:20109.1,20109.0,4.0,5.0,15.0,14.0,11.0,10.0,9.0,13.0,12.0,8.0] || -> equal(skc6,nil)**. % 14.96/15.13 20114[4:MRR:20113.0,1101.0] || -> . % 14.96/15.13 20115[4:Spt:20114.0,156.4] || SkP0(skc6,skc7)* -> . % 14.96/15.13 20179[4:Res:61.0,20115.0] || -> equal(skc7,nil)**. % 14.96/15.13 20180[4:MRR:20179.0,1925.0] || -> . % 14.96/15.13 20181[1:Spt:20180.0,428.1] || -> equal(skc7,nil)**. % 14.96/15.13 20208[1:Rew:20181.0,15848.0] || -> equal(app(skc8,app(skc6,skc9)),nil)**. % 14.96/15.13 20377[1:Rew:20181.0,563.1,20181.0,563.0] || SkP0(skc6,nil) segmentP(skc6,nil)* -> . % 14.96/15.13 20378[1:MRR:20377.1,292.0] || SkP0(skc6,nil)* -> . % 14.96/15.13 20403[1:Rew:20181.0,3963.2] ssList(nil) ssList(skc9) || equal(nil,nil) -> equal(skc9,nil)**. % 14.96/15.13 20404[1:Obv:20403.2] ssList(nil) ssList(skc9) || -> equal(skc9,nil)**. % 14.96/15.13 20405[1:SSi:20404.1,20404.0,1.0,15.0,14.0,11.0,10.0,9.0,13.0,12.0,8.0] || -> equal(skc9,nil)**. % 14.96/15.13 20420[1:Rew:20405.0,20208.0] || -> equal(app(skc8,app(skc6,nil)),nil)**. % 14.96/15.13 20427[1:Rew:286.0,20420.0] || -> equal(app(skc8,skc6),nil)**. % 14.96/15.13 20613[2:Spt:317.3] || -> equal(skc6,nil)**. % 14.96/15.13 20806[2:Rew:20613.0,20378.0] || SkP0(nil,nil)* -> . % 14.96/15.13 20932[2:Res:73.1,20806.0] || equal(nil,nil)* -> . % 14.96/15.13 20934[2:Obv:20932.0] || -> . % 14.96/15.13 20935[2:Spt:20934.0,317.3,20613.0] || equal(skc6,nil)** -> . % 14.96/15.13 20936[2:Spt:20934.0,317.0,317.1,317.2] ssItem(u) || totalorderedP(cons(u,skc6))* -> leq(u,hd(skc6)). % 14.96/15.13 21090[1:SpL:20427.0,131.2] ssList(skc6) ssList(skc8) || equal(nil,nil) -> equal(skc8,nil)**. % 14.96/15.13 21102[1:Obv:21090.2] ssList(skc6) ssList(skc8) || -> equal(skc8,nil)**. % 14.96/15.13 21224[1:SSi:21102.0,5.0,4.0] ssList(skc8) || -> equal(skc8,nil)**. % 14.96/15.13 21225[1:MRR:21224.0,2.0] || -> equal(skc8,nil)**. % 14.96/15.13 21227[1:Rew:21225.0,20427.0] || -> equal(app(nil,skc6),nil)**. % 14.96/15.13 21229[1:Rew:285.0,21227.0] || -> equal(skc6,nil)**. % 14.96/15.13 21230[2:MRR:21229.0,20935.0] || -> . % 14.96/15.13 % SZS output end Refutation % 14.96/15.13 Formulae used in the proof : co1 ax2 ax17 ax60 ax62 ax64 ax66 ax69 ax72 ax74 ax55 ax57 ax28 ax84 ax16 ax26 ax52 ax15 ax23 ax83 ax85 ax6 ax67 ax70 ax82 ax56 % 14.96/15.13 %------------------------------------------------------------------------------