%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : SWC313+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:14 EDT 2022 % Result : Theorem 4.74s 4.96s % Output : Refutation 4.74s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.08/0.11 % Problem : SWC313+1 : TPTP v8.1.0. Released v2.4.0. % 0.08/0.12 % Command : run_spass %d %s % 0.12/0.33 % Computer : n026.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 05:35:20 EDT 2022 % 0.12/0.33 % CPUTime : % 4.74/4.96 % 4.74/4.96 SPASS V 3.9 % 4.74/4.96 SPASS beiseite: Proof found. % 4.74/4.96 % SZS status Theorem % 4.74/4.96 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 4.74/4.96 SPASS derived 8561 clauses, backtracked 2270 clauses, performed 48 splits and kept 5950 clauses. % 4.74/4.96 SPASS allocated 107204 KBytes. % 4.74/4.96 SPASS spent 0:00:04.21 on the problem. % 4.74/4.96 0:00:00.04 for the input. % 4.74/4.96 0:00:00.07 for the FLOTTER CNF translation. % 4.74/4.96 0:00:00.08 for inferences. % 4.74/4.96 0:00:00.08 for the backtracking. % 4.74/4.96 0:00:03.73 for the reduction. % 4.74/4.96 % 4.74/4.96 % 4.74/4.96 Here is a proof with depth 6, length 82 : % 4.74/4.96 % SZS output start Refutation % 4.74/4.96 1[0:Inp] || -> ssList(skc5)*. % 4.74/4.96 3[0:Inp] || -> ssItem(skc7)*. % 4.74/4.96 4[0:Inp] || -> ssItem(skc6)*. % 4.74/4.96 5[0:Inp] || -> ssList(nil)*. % 4.74/4.96 6[0:Inp] || -> cyclefreeP(nil)*. % 4.74/4.96 7[0:Inp] || -> totalorderP(nil)*. % 4.74/4.96 8[0:Inp] || -> strictorderP(nil)*. % 4.74/4.96 9[0:Inp] || -> totalorderedP(nil)*. % 4.74/4.96 10[0:Inp] || -> strictorderedP(nil)*. % 4.74/4.96 11[0:Inp] || -> duplicatefreeP(nil)*. % 4.74/4.96 12[0:Inp] || -> equalelemsP(nil)*. % 4.74/4.96 51[0:Inp] || equal(skc7,skc6)** -> . % 4.74/4.96 58[0:Inp] || -> SkP0(u,v)* equal(nil,v). % 4.74/4.96 67[0:Inp] || equal(skc5,nil)** -> equal(skc4,nil). % 4.74/4.96 68[0:Inp] || SkP0(skc4,skc5) -> neq(skc5,nil)*. % 4.74/4.96 69[0:Inp] || equal(nil,u) -> SkP0(u,v)*. % 4.74/4.96 71[0:Inp] ssItem(u) || -> cyclefreeP(cons(u,nil))*. % 4.74/4.96 72[0:Inp] ssItem(u) || -> totalorderP(cons(u,nil))*. % 4.74/4.96 73[0:Inp] ssItem(u) || -> strictorderP(cons(u,nil))*. % 4.74/4.96 74[0:Inp] ssItem(u) || -> totalorderedP(cons(u,nil))*. % 4.74/4.96 75[0:Inp] ssItem(u) || -> strictorderedP(cons(u,nil))*. % 4.74/4.96 76[0:Inp] ssItem(u) || -> duplicatefreeP(cons(u,nil))*. % 4.74/4.96 77[0:Inp] ssItem(u) || -> equalelemsP(cons(u,nil))*. % 4.74/4.96 79[0:Inp] ssList(u) || -> equal(app(nil,u),u)**. % 4.74/4.96 83[0:Inp] ssList(u) || -> ssItem(hd(u))* equal(nil,u). % 4.74/4.96 84[0:Inp] ssList(u) || -> ssList(tl(u))* equal(nil,u). % 4.74/4.96 88[0:Inp] ssItem(u) ssList(v) || -> ssList(cons(u,v))*. % 4.74/4.96 108[0:Inp] ssItem(u) ssList(v) || -> equal(hd(cons(u,v)),u)**. % 4.74/4.96 115[0:Inp] ssList(u) || -> equal(nil,u) equal(cons(hd(u),tl(u)),u)**. % 4.74/4.96 119[0:Inp] ssList(u) ssList(v) || equal(v,u) neq(v,u)* -> . % 4.74/4.96 125[0:Inp] ssItem(u) ssList(v) || -> equal(app(cons(u,nil),v),cons(u,v))**. % 4.74/4.96 130[0:Inp] ssList(u) ssList(v) || -> equal(nil,v) equal(hd(app(v,u)),hd(v))**. % 4.74/4.96 150[0:Inp] ssList(u) ssItem(v) || strictorderedP(cons(v,u))* -> lt(v,hd(u)) equal(nil,u). % 4.74/4.96 177[0:Inp] ssItem(u) ssList(v) || equal(app(cons(u,nil),v),skc5)** -> equal(app(v,cons(u,nil)),skc4)**. % 4.74/4.96 185[0:Inp] ssItem(u) ssList(v) || equal(app(cons(u,nil),v),skc5)** equal(app(v,cons(u,nil)),skc4)** SkP0(skc4,skc5) -> . % 4.74/4.96 198[0:Rew:125.2,177.2] ssList(u) ssItem(v) || equal(cons(v,u),skc5) -> equal(app(u,cons(v,nil)),skc4)**. % 4.74/4.96 201[0:Rew:198.3,185.3,125.2,185.2] ssItem(u) ssList(v) || equal(cons(u,v),skc5)** equal(skc4,skc4) SkP0(skc4,skc5) -> . % 4.74/4.96 202[0:Obv:201.3] ssList(u) ssItem(v) || SkP0(skc4,skc5) equal(cons(v,u),skc5)** -> . % 4.74/4.96 418[0:Res:1.0,130.0] ssList(u) || -> equal(skc5,nil) equal(hd(app(skc5,u)),hd(skc5))**. % 4.74/4.96 422[0:Res:1.0,119.0] ssList(u) || equal(skc5,u) neq(skc5,u)* -> . % 4.74/4.96 424[0:Res:1.0,115.0] || -> equal(skc5,nil) equal(cons(hd(skc5),tl(skc5)),skc5)**. % 4.74/4.96 429[0:Res:1.0,108.0] ssItem(u) || -> equal(hd(cons(u,skc5)),u)**. % 4.74/4.96 441[0:Res:1.0,88.0] ssItem(u) || -> ssList(cons(u,skc5))*. % 4.74/4.96 449[0:Res:1.0,83.0] || -> ssItem(hd(skc5))* equal(skc5,nil). % 4.74/4.96 450[0:Res:1.0,84.0] || -> ssList(tl(skc5))* equal(skc5,nil). % 4.74/4.96 484[0:Res:1.0,150.1] ssItem(u) || strictorderedP(cons(u,skc5))* -> lt(u,hd(skc5)) equal(skc5,nil). % 4.74/4.96 549[1:Spt:418.0,418.2] ssList(u) || -> equal(hd(app(skc5,u)),hd(skc5))**. % 4.74/4.96 557[2:Spt:202.0,202.1,202.3] ssList(u) ssItem(v) || equal(cons(v,u),skc5)** -> . % 4.74/4.96 558[3:Spt:484.3] || -> equal(skc5,nil)**. % 4.74/4.96 559[3:Rew:558.0,549.1] ssList(u) || -> equal(hd(app(nil,u)),hd(nil))**. % 4.74/4.96 579[3:Rew:558.0,441.1] ssItem(u) || -> ssList(cons(u,nil))*. % 4.74/4.96 580[3:Rew:558.0,429.1] ssItem(u) || -> equal(hd(cons(u,nil)),u)**. % 4.74/4.96 905[3:Rew:79.1,559.1] ssList(u) || -> equal(hd(u),hd(nil))*. % 4.74/4.96 1183[3:SpR:580.1,905.1] ssItem(u) ssList(cons(u,nil)) || -> equal(u,hd(nil))*. % 4.74/4.96 1186[3:SSi:1183.1,77.1,76.1,73.1,72.1,71.1,75.1,74.1,579.1] ssItem(u) || -> equal(u,hd(nil))*. % 4.74/4.96 1253[3:SpR:1186.1,1186.1] ssItem(u) ssItem(v) || -> equal(v,u)*. % 4.74/4.96 1293[3:EmS:1253.0,3.0] ssItem(u) || -> equal(u,skc7)*. % 4.74/4.96 1314[3:EmS:1293.0,4.0] || -> equal(skc7,skc6)**. % 4.74/4.96 1315[3:MRR:1314.0,51.0] || -> . % 4.74/4.96 1447[3:Spt:1315.0,484.3,558.0] || equal(skc5,nil)** -> . % 4.74/4.96 1448[3:Spt:1315.0,484.0,484.1,484.2] ssItem(u) || strictorderedP(cons(u,skc5))* -> lt(u,hd(skc5)). % 4.74/4.96 1449[3:MRR:450.1,1447.0] || -> ssList(tl(skc5))*. % 4.74/4.96 1450[3:MRR:449.1,1447.0] || -> ssItem(hd(skc5))*. % 4.74/4.96 1454[3:MRR:424.0,1447.0] || -> equal(cons(hd(skc5),tl(skc5)),skc5)**. % 4.74/4.96 7207[0:Res:68.1,422.2] ssList(nil) || SkP0(skc4,skc5)* equal(skc5,nil) -> . % 4.74/4.96 11631[3:SpL:1454.0,557.2] ssList(tl(skc5)) ssItem(hd(skc5)) || equal(skc5,skc5)* -> . % 4.74/4.96 11673[3:Obv:11631.2] ssList(tl(skc5)) ssItem(hd(skc5)) || -> . % 4.74/4.96 11674[3:SSi:11673.1,11673.0,1450.0,1449.0] || -> . % 4.74/4.96 11747[2:Spt:11674.0,202.2] || SkP0(skc4,skc5)* -> . % 4.74/4.96 11784[2:Res:69.1,11747.0] || equal(skc4,nil)** -> . % 4.74/4.96 11785[2:Res:58.0,11747.0] || -> equal(skc5,nil)**. % 4.74/4.96 11946[2:Rew:11785.0,67.0] || equal(nil,nil) -> equal(skc4,nil)**. % 4.74/4.96 11972[2:Obv:11946.0] || -> equal(skc4,nil)**. % 4.74/4.96 11973[2:MRR:11972.0,11784.0] || -> . % 4.74/4.96 12080[1:Spt:11973.0,418.1] || -> equal(skc5,nil)**. % 4.74/4.96 12102[1:Rew:12080.0,67.0] || equal(nil,nil) -> equal(skc4,nil)**. % 4.74/4.96 12103[1:Obv:12102.0] || -> equal(skc4,nil)**. % 4.74/4.96 12290[1:Rew:12080.0,7207.2,12103.0,7207.1,12080.0,7207.1] ssList(nil) || SkP0(nil,nil)* equal(nil,nil) -> . % 4.74/4.96 12291[1:Obv:12290.2] ssList(nil) || SkP0(nil,nil)* -> . % 4.74/4.96 12292[1:SSi:12291.0,12.0,11.0,8.0,7.0,6.0,10.0,9.0,5.0] || SkP0(nil,nil)* -> . % 4.74/4.96 12571[1:Res:69.1,12292.0] || equal(nil,nil)* -> . % 4.74/4.96 12573[1:Obv:12571.0] || -> . % 4.74/4.96 % SZS output end Refutation % 4.74/4.96 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 ax23 ax78 ax15 ax81 ax85 ax70 % 4.74/4.96 %------------------------------------------------------------------------------