%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : SWC100+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:43 EDT 2022 % Result : Theorem 7.72s 7.92s % Output : Refutation 7.72s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.11 % Problem : SWC100+1 : TPTP v8.1.0. Released v2.4.0. % 0.12/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 16:01:03 EDT 2022 % 0.12/0.33 % CPUTime : % 7.72/7.92 % 7.72/7.92 SPASS V 3.9 % 7.72/7.92 SPASS beiseite: Proof found. % 7.72/7.92 % SZS status Theorem % 7.72/7.92 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 7.72/7.92 SPASS derived 8108 clauses, backtracked 2694 clauses, performed 68 splits and kept 5080 clauses. % 7.72/7.92 SPASS allocated 108521 KBytes. % 7.72/7.92 SPASS spent 0:00:07.09 on the problem. % 7.72/7.92 0:00:00.04 for the input. % 7.72/7.92 0:00:00.07 for the FLOTTER CNF translation. % 7.72/7.92 0:00:00.11 for inferences. % 7.72/7.92 0:00:00.10 for the backtracking. % 7.72/7.92 0:00:06.50 for the reduction. % 7.72/7.92 % 7.72/7.92 % 7.72/7.92 Here is a proof with depth 4, length 65 : % 7.72/7.92 % SZS output start Refutation % 7.72/7.92 1[0:Inp] || -> ssList(skc7)*. % 7.72/7.92 2[0:Inp] || -> ssList(skc6)*. % 7.72/7.92 3[0:Inp] || -> ssList(skc5)*. % 7.72/7.92 4[0:Inp] || -> strictorderedP(skc5)*. % 7.72/7.92 7[0:Inp] || -> ssList(nil)*. % 7.72/7.92 8[0:Inp] || -> cyclefreeP(nil)*. % 7.72/7.92 9[0:Inp] || -> totalorderP(nil)*. % 7.72/7.92 10[0:Inp] || -> strictorderP(nil)*. % 7.72/7.92 11[0:Inp] || -> totalorderedP(nil)*. % 7.72/7.92 12[0:Inp] || -> strictorderedP(nil)*. % 7.72/7.92 13[0:Inp] || -> duplicatefreeP(nil)*. % 7.72/7.92 14[0:Inp] || -> equalelemsP(nil)*. % 7.72/7.92 60[0:Inp] || -> equal(app(skc5,skc7),skc6)**. % 7.72/7.92 61[0:Inp] || -> SkP0(u,v)* equal(nil,v). % 7.72/7.92 63[0:Inp] ssList(u) || -> frontsegP(u,u)*. % 7.72/7.92 64[0:Inp] ssList(u) || -> frontsegP(u,nil)*. % 7.72/7.92 70[0:Inp] || equal(skc5,nil) -> equal(skc6,nil)**. % 7.72/7.92 71[0:Inp] || SkP0(skc5,skc6) -> neq(skc6,nil)*. % 7.72/7.92 72[0:Inp] || equal(nil,u) -> SkP0(u,v)*. % 7.72/7.92 93[0:Inp] ssList(u) || frontsegP(nil,u)* -> equal(nil,u). % 7.72/7.92 106[0:Inp] || SkP0(skc5,skc6) frontsegP(skc6,skc5)* neq(skc5,nil) -> . % 7.72/7.92 109[0:Inp] ssList(u) ssList(v) || -> neq(v,u)* equal(v,u). % 7.72/7.92 131[0:Inp] ssList(u) ssList(v) || equal(app(v,u),nil)** -> equal(nil,v). % 7.72/7.92 151[0:Inp] ssList(u) ssList(v) ssList(w) || frontsegP(w,v) -> frontsegP(app(w,u),v)*. % 7.72/7.92 188[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.72/7.92 251[0:Res:3.0,131.0] ssList(u) || equal(app(skc5,u),nil)** -> equal(skc5,nil). % 7.72/7.92 256[0:Res:3.0,109.0] ssList(u) || -> neq(skc5,u)* equal(skc5,u). % 7.72/7.92 273[0:Res:3.0,93.0] || frontsegP(nil,skc5)* -> equal(skc5,nil). % 7.72/7.92 283[0:Res:3.0,63.0] || -> frontsegP(skc5,skc5)*. % 7.72/7.92 290[0:Res:3.0,188.1] ssList(u) || equal(tl(skc5),tl(u))* equal(hd(skc5),hd(u)) -> equal(nil,u) equal(skc5,u) equal(skc5,nil). % 7.72/7.92 457[0:Res:2.0,64.0] || -> frontsegP(skc6,nil)*. % 7.72/7.92 463[0:Res:2.0,188.1] ssList(u) || equal(tl(skc6),tl(u))* equal(hd(skc6),hd(u)) -> equal(nil,u) equal(skc6,u) equal(skc6,nil). % 7.72/7.92 562[1:Spt:463.5] || -> equal(skc6,nil)**. % 7.72/7.92 565[1:Rew:562.0,106.0] || SkP0(skc5,nil) frontsegP(skc6,skc5)* neq(skc5,nil) -> . % 7.72/7.92 566[1:Rew:562.0,71.0] || SkP0(skc5,nil) -> neq(skc6,nil)*. % 7.72/7.92 673[1:Rew:562.0,457.0] || -> frontsegP(nil,nil)*. % 7.72/7.92 677[1:Rew:562.0,60.0] || -> equal(app(skc5,skc7),nil)**. % 7.72/7.92 718[1:Rew:562.0,566.1] || SkP0(skc5,nil) -> neq(nil,nil)*. % 7.72/7.92 747[1:Rew:273.1,565.2,562.0,565.1] || SkP0(skc5,nil) frontsegP(nil,skc5)* neq(nil,nil) -> . % 7.72/7.92 748[1:MRR:747.2,718.1] || SkP0(skc5,nil) frontsegP(nil,skc5)* -> . % 7.72/7.92 825[2:Spt:290.5] || -> equal(skc5,nil)**. % 7.72/7.92 859[2:Rew:825.0,748.1] || SkP0(skc5,nil) frontsegP(nil,nil)* -> . % 7.72/7.92 992[2:Rew:825.0,859.0] || SkP0(nil,nil) frontsegP(nil,nil)* -> . % 7.72/7.92 993[2:MRR:992.1,673.0] || SkP0(nil,nil)* -> . % 7.72/7.92 1079[2:Res:72.1,993.0] || equal(nil,nil)* -> . % 7.72/7.92 1080[2:Obv:1079.0] || -> . % 7.72/7.92 1081[2:Spt:1080.0,290.5,825.0] || equal(skc5,nil)** -> . % 7.72/7.92 1082[2:Spt:1080.0,290.0,290.1,290.2,290.3,290.4] ssList(u) || equal(tl(skc5),tl(u))* equal(hd(skc5),hd(u)) -> equal(nil,u) equal(skc5,u). % 7.72/7.92 1091[2:MRR:251.2,1081.0] ssList(u) || equal(app(skc5,u),nil)** -> . % 7.72/7.92 1158[2:SpL:677.0,1091.1] ssList(skc7) || equal(nil,nil)* -> . % 7.72/7.92 1161[2:Obv:1158.1] ssList(skc7) || -> . % 7.72/7.92 1162[2:SSi:1161.0,1.0] || -> . % 7.72/7.92 1163[1:Spt:1162.0,463.5,562.0] || equal(skc6,nil)** -> . % 7.72/7.92 1164[1:Spt:1162.0,463.0,463.1,463.2,463.3,463.4] ssList(u) || equal(tl(skc6),tl(u))* equal(hd(skc6),hd(u)) -> equal(nil,u) equal(skc6,u). % 7.72/7.92 1170[1:MRR:70.1,1163.0] || equal(skc5,nil)** -> . % 7.72/7.92 3478[0:SpR:60.0,151.4] ssList(skc7) ssList(u) ssList(skc5) || frontsegP(skc5,u) -> frontsegP(skc6,u)*. % 7.72/7.92 10771[0:SSi:3478.2,3478.0,3.0,4.0,1.0] ssList(u) || frontsegP(skc5,u) -> frontsegP(skc6,u)*. % 7.72/7.92 11648[0:Res:10771.2,106.1] ssList(skc5) || frontsegP(skc5,skc5)* SkP0(skc5,skc6) neq(skc5,nil) -> . % 7.72/7.92 12394[0:SSi:11648.0,3.0,4.0] || frontsegP(skc5,skc5)* SkP0(skc5,skc6) neq(skc5,nil) -> . % 7.72/7.92 12395[0:MRR:12394.0,283.0] || SkP0(skc5,skc6) neq(skc5,nil)* -> . % 7.72/7.92 12678[0:Res:256.1,12395.1] ssList(nil) || SkP0(skc5,skc6)* -> equal(skc5,nil). % 7.72/7.92 12681[0:SSi:12678.0,14.0,13.0,10.0,9.0,8.0,12.0,11.0,7.0] || SkP0(skc5,skc6)* -> equal(skc5,nil). % 7.72/7.92 12682[1:MRR:12681.1,1170.0] || SkP0(skc5,skc6)* -> . % 7.72/7.92 12684[1:Res:61.0,12682.0] || -> equal(skc6,nil)**. % 7.72/7.92 12685[1:MRR:12684.0,1163.0] || -> . % 7.72/7.92 % SZS output end Refutation % 7.72/7.92 Formulae used in the proof : co1 ax17 ax60 ax62 ax64 ax66 ax69 ax72 ax74 ax42 ax45 ax46 ax15 ax83 ax43 ax77 % 7.72/7.92 %------------------------------------------------------------------------------