%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : SWC415+1 : TPTP v8.1.0. Released v2.4.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n005.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:56 EDT 2022 % Result : Theorem 1.92s 2.11s % Output : Refutation 1.92s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.08/0.13 % Problem : SWC415+1 : TPTP v8.1.0. Released v2.4.0. % 0.08/0.14 % Command : run_spass %d %s % 0.14/0.35 % Computer : n005.cluster.edu % 0.14/0.35 % Model : x86_64 x86_64 % 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.35 % Memory : 8042.1875MB % 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.35 % CPULimit : 300 % 0.14/0.35 % WCLimit : 600 % 0.14/0.35 % DateTime : Sun Jun 12 05:16:09 EDT 2022 % 0.14/0.36 % CPUTime : % 1.92/2.11 % 1.92/2.11 SPASS V 3.9 % 1.92/2.11 SPASS beiseite: Proof found. % 1.92/2.11 % SZS status Theorem % 1.92/2.11 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 1.92/2.11 SPASS derived 3803 clauses, backtracked 1542 clauses, performed 39 splits and kept 3602 clauses. % 1.92/2.11 SPASS allocated 101401 KBytes. % 1.92/2.11 SPASS spent 0:00:01.69 on the problem. % 1.92/2.11 0:00:00.04 for the input. % 1.92/2.11 0:00:00.06 for the FLOTTER CNF translation. % 1.92/2.11 0:00:00.03 for inferences. % 1.92/2.11 0:00:00.03 for the backtracking. % 1.92/2.11 0:00:01.32 for the reduction. % 1.92/2.11 % 1.92/2.11 % 1.92/2.11 Here is a proof with depth 6, length 74 : % 1.92/2.11 % SZS output start Refutation % 1.92/2.11 1[0:Inp] || -> ssList(skc5)*. % 1.92/2.11 2[0:Inp] || -> ssList(skc4)*. % 1.92/2.11 3[0:Inp] || -> ssItem(skc7)*. % 1.92/2.11 4[0:Inp] || -> ssItem(skc6)*. % 1.92/2.11 5[0:Inp] || -> ssList(nil)*. % 1.92/2.11 6[0:Inp] || -> cyclefreeP(nil)*. % 1.92/2.11 7[0:Inp] || -> totalorderP(nil)*. % 1.92/2.11 8[0:Inp] || -> strictorderP(nil)*. % 1.92/2.11 9[0:Inp] || -> totalorderedP(nil)*. % 1.92/2.11 10[0:Inp] || -> strictorderedP(nil)*. % 1.92/2.11 11[0:Inp] || -> duplicatefreeP(nil)*. % 1.92/2.11 12[0:Inp] || -> equalelemsP(nil)*. % 1.92/2.11 51[0:Inp] || equal(skc7,skc6)** -> . % 1.92/2.11 58[0:Inp] || -> SkP0(u,v)* neq(v,nil). % 1.92/2.11 67[0:Inp] || SkP0(skc4,skc5)* -> neq(skc5,nil). % 1.92/2.11 69[0:Inp] ssItem(u) || -> cyclefreeP(cons(u,nil))*. % 1.92/2.11 70[0:Inp] ssItem(u) || -> totalorderP(cons(u,nil))*. % 1.92/2.11 71[0:Inp] ssItem(u) || -> strictorderP(cons(u,nil))*. % 1.92/2.11 72[0:Inp] ssItem(u) || -> totalorderedP(cons(u,nil))*. % 1.92/2.11 73[0:Inp] ssItem(u) || -> strictorderedP(cons(u,nil))*. % 1.92/2.11 74[0:Inp] ssItem(u) || -> duplicatefreeP(cons(u,nil))*. % 1.92/2.11 75[0:Inp] ssItem(u) || -> equalelemsP(cons(u,nil))*. % 1.92/2.11 77[0:Inp] || neq(skc5,nil) SkP0(skc4,skc5)* -> . % 1.92/2.11 78[0:Inp] ssList(u) || -> equal(app(nil,u),u)**. % 1.92/2.11 83[0:Inp] ssList(u) || -> ssList(tl(u))* equal(nil,u). % 1.92/2.11 87[0:Inp] ssItem(u) ssList(v) || -> ssList(cons(u,v))*. % 1.92/2.11 104[0:Inp] ssList(u) ssList(v) || -> neq(v,u)* equal(v,u). % 1.92/2.11 107[0:Inp] ssItem(u) ssList(v) || -> equal(hd(cons(u,v)),u)**. % 1.92/2.11 118[0:Inp] ssList(u) ssList(v) || equal(v,u) neq(v,u)* -> . % 1.92/2.11 124[0:Inp] || ssList(tl(u)) neq(nil,u) -> SkP0(v,u)* equal(v,tl(u)). % 1.92/2.11 128[0:Inp] || ssList(tl(u)) equal(v,tl(u)) neq(nil,u) -> SkP0(v,u)*. % 1.92/2.11 131[0:Inp] ssList(u) ssList(v) || -> equal(nil,v) equal(hd(app(v,u)),hd(v))**. % 1.92/2.11 185[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). % 1.92/2.11 194[0:MRR:67.0,58.1] || -> neq(skc5,nil)*. % 1.92/2.11 195[0:MRR:77.0,194.0] || SkP0(skc4,skc5)* -> . % 1.92/2.11 414[0:Res:1.0,131.0] ssList(u) || -> equal(skc5,nil) equal(hd(app(skc5,u)),hd(skc5))**. % 1.92/2.11 418[0:Res:1.0,118.0] ssList(u) || equal(skc5,u) neq(skc5,u)* -> . % 1.92/2.11 425[0:Res:1.0,107.0] ssItem(u) || -> equal(hd(cons(u,skc5)),u)**. % 1.92/2.11 437[0:Res:1.0,87.0] ssItem(u) || -> ssList(cons(u,skc5))*. % 1.92/2.11 446[0:Res:1.0,83.0] || -> ssList(tl(skc5))* equal(skc5,nil). % 1.92/2.11 455[0:Res:1.0,185.1] ssList(u) || equal(tl(skc5),tl(u)) equal(hd(skc5),hd(u))* -> equal(nil,u) equal(skc5,u) equal(skc5,nil). % 1.92/2.11 494[0:Res:1.0,104.1] ssList(u) || -> neq(u,skc5)* equal(u,skc5). % 1.92/2.11 543[1:Spt:414.0,414.2] ssList(u) || -> equal(hd(app(skc5,u)),hd(skc5))**. % 1.92/2.11 551[2:Spt:455.5] || -> equal(skc5,nil)**. % 1.92/2.11 552[2:Rew:551.0,543.1] ssList(u) || -> equal(hd(app(nil,u)),hd(nil))**. % 1.92/2.11 568[2:Rew:551.0,437.1] ssItem(u) || -> ssList(cons(u,nil))*. % 1.92/2.11 569[2:Rew:551.0,425.1] ssItem(u) || -> equal(hd(cons(u,nil)),u)**. % 1.92/2.11 723[2:Rew:78.1,552.1] ssList(u) || -> equal(hd(u),hd(nil))*. % 1.92/2.11 1169[2:SpR:569.1,723.1] ssItem(u) ssList(cons(u,nil)) || -> equal(u,hd(nil))*. % 1.92/2.11 1172[2:SSi:1169.1,75.1,74.1,71.1,70.1,69.1,73.1,72.1,568.1] ssItem(u) || -> equal(u,hd(nil))*. % 1.92/2.11 1238[2:SpR:1172.1,1172.1] ssItem(u) ssItem(v) || -> equal(v,u)*. % 1.92/2.11 1276[2:EmS:1238.0,3.0] ssItem(u) || -> equal(u,skc7)*. % 1.92/2.11 1297[2:EmS:1276.0,4.0] || -> equal(skc7,skc6)**. % 1.92/2.11 1298[2:MRR:1297.0,51.0] || -> . % 1.92/2.11 1426[2:Spt:1298.0,455.5,551.0] || equal(skc5,nil)** -> . % 1.92/2.11 1427[2:Spt:1298.0,455.0,455.1,455.2,455.3,455.4] ssList(u) || equal(tl(skc5),tl(u)) equal(hd(skc5),hd(u))* -> equal(nil,u) equal(skc5,u). % 1.92/2.11 1428[2:MRR:446.1,1426.0] || -> ssList(tl(skc5))*. % 1.92/2.11 4607[0:Res:124.2,195.0] || ssList(tl(skc5)) neq(nil,skc5)* -> equal(tl(skc5),skc4). % 1.92/2.11 4608[2:MRR:4607.0,1428.0] || neq(nil,skc5)* -> equal(tl(skc5),skc4). % 1.92/2.11 4688[2:Res:494.1,4608.0] ssList(nil) || -> equal(skc5,nil) equal(tl(skc5),skc4)**. % 1.92/2.11 4690[2:SSi:4688.0,12.0,11.0,8.0,7.0,6.0,10.0,9.0,5.0] || -> equal(skc5,nil) equal(tl(skc5),skc4)**. % 1.92/2.11 4691[2:MRR:4690.0,1426.0] || -> equal(tl(skc5),skc4)**. % 1.92/2.11 4955[0:Res:194.0,418.2] ssList(nil) || equal(skc5,nil)** -> . % 1.92/2.11 4982[0:Res:128.3,195.0] || ssList(tl(skc5)) equal(tl(skc5),skc4) neq(nil,skc5)* -> . % 1.92/2.11 4983[2:Rew:4691.0,4982.1,4691.0,4982.0] || ssList(skc4) equal(skc4,skc4) neq(nil,skc5)* -> . % 1.92/2.11 4984[2:Obv:4983.1] || ssList(skc4) neq(nil,skc5)* -> . % 1.92/2.11 4985[2:MRR:4984.0,2.0] || neq(nil,skc5)* -> . % 1.92/2.11 4986[2:Res:494.1,4985.0] ssList(nil) || -> equal(skc5,nil)**. % 1.92/2.11 4989[2:SSi:4986.0,12.0,11.0,8.0,7.0,6.0,10.0,9.0,5.0] || -> equal(skc5,nil)**. % 1.92/2.11 4990[2:MRR:4989.0,1426.0] || -> . % 1.92/2.11 4994[1:Spt:4990.0,414.1] || -> equal(skc5,nil)**. % 1.92/2.11 5120[1:Rew:4994.0,4955.1] ssList(nil) || equal(nil,nil)* -> . % 1.92/2.11 5121[1:Obv:5120.1] ssList(nil) || -> . % 1.92/2.11 5122[1:SSi:5121.0,12.0,11.0,8.0,7.0,6.0,10.0,9.0,5.0] || -> . % 1.92/2.11 % SZS output end Refutation % 1.92/2.11 Formulae used in the proof : co1 ax2 ax17 ax60 ax62 ax64 ax66 ax69 ax72 ax74 ax59 ax61 ax63 ax65 ax68 ax71 ax73 ax28 ax76 ax16 ax15 ax23 ax85 ax77 % 1.92/2.11 %------------------------------------------------------------------------------