%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : SWC164+1 : TPTP v8.1.0. Released v2.4.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n024.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:02:10 EDT 2022 % Result : Theorem 13.29s 13.48s % Output : Refutation 13.29s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : SWC164+1 : TPTP v8.1.0. Released v2.4.0. % 0.03/0.13 % Command : run_spass %d %s % 0.13/0.34 % Computer : n024.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 600 % 0.13/0.34 % DateTime : Mon Jun 13 00:16:03 EDT 2022 % 0.13/0.34 % CPUTime : % 13.29/13.48 % 13.29/13.48 SPASS V 3.9 % 13.29/13.48 SPASS beiseite: Proof found. % 13.29/13.48 % SZS status Theorem % 13.29/13.48 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 13.29/13.48 SPASS derived 10103 clauses, backtracked 4340 clauses, performed 42 splits and kept 7788 clauses. % 13.29/13.48 SPASS allocated 113064 KBytes. % 13.29/13.48 SPASS spent 0:0:12.20 on the problem. % 13.29/13.48 0:00:00.04 for the input. % 13.29/13.48 0:00:00.07 for the FLOTTER CNF translation. % 13.29/13.48 0:00:00.11 for inferences. % 13.29/13.48 0:00:00.42 for the backtracking. % 13.29/13.48 0:0:11.34 for the reduction. % 13.29/13.48 % 13.29/13.48 % 13.29/13.48 Here is a proof with depth 6, length 97 : % 13.29/13.48 % SZS output start Refutation % 13.29/13.48 1[0:Inp] || -> ssList(skc13)*. % 13.29/13.48 2[0:Inp] || -> ssList(skc12)*. % 13.29/13.48 3[0:Inp] || -> ssItem(skc11)*. % 13.29/13.48 4[0:Inp] || -> ssItem(skc10)*. % 13.29/13.48 6[0:Inp] || -> ssList(skc8)*. % 13.29/13.48 7[0:Inp] || -> ssItem(skc15)*. % 13.29/13.48 8[0:Inp] || -> ssItem(skc14)*. % 13.29/13.48 9[0:Inp] || -> ssList(nil)*. % 13.29/13.48 10[0:Inp] || -> cyclefreeP(nil)*. % 13.29/13.48 11[0:Inp] || -> totalorderP(nil)*. % 13.29/13.48 12[0:Inp] || -> strictorderP(nil)*. % 13.29/13.48 13[0:Inp] || -> totalorderedP(nil)*. % 13.29/13.48 14[0:Inp] || -> strictorderedP(nil)*. % 13.29/13.48 15[0:Inp] || -> duplicatefreeP(nil)*. % 13.29/13.48 16[0:Inp] || -> equalelemsP(nil)*. % 13.29/13.48 17[0:Inp] || -> ssItem(skf47(u))*. % 13.29/13.48 55[0:Inp] || -> ssItem(skf44(u,v))*. % 13.29/13.48 56[0:Inp] || neq(skc10,skc11)* -> . % 13.29/13.48 57[0:Inp] || equal(skc15,skc14)** -> . % 13.29/13.48 73[0:Inp] || SkP0(skc9,skc8)* -> equal(nil,skc8). % 13.29/13.48 75[0:Inp] ssItem(u) || -> cyclefreeP(cons(u,nil))*. % 13.29/13.48 76[0:Inp] ssItem(u) || -> totalorderP(cons(u,nil))*. % 13.29/13.48 77[0:Inp] ssItem(u) || -> strictorderP(cons(u,nil))*. % 13.29/13.48 78[0:Inp] ssItem(u) || -> totalorderedP(cons(u,nil))*. % 13.29/13.48 79[0:Inp] ssItem(u) || -> strictorderedP(cons(u,nil))*. % 13.29/13.48 80[0:Inp] ssItem(u) || -> duplicatefreeP(cons(u,nil))*. % 13.29/13.48 81[0:Inp] ssItem(u) || -> equalelemsP(cons(u,nil))*. % 13.29/13.48 84[0:Inp] ssList(u) || -> equal(app(nil,u),u)**. % 13.29/13.48 90[0:Inp] || -> SkP0(u,v) equal(cons(skf44(u,v),nil),v)**. % 13.29/13.48 94[0:Inp] ssItem(u) ssList(v) || -> ssList(cons(u,v))*. % 13.29/13.48 95[0:Inp] ssList(u) ssList(v) || -> ssList(app(v,u))*. % 13.29/13.48 109[0:Inp] ssItem(u) ssItem(v) || -> neq(v,u)* equal(v,u). % 13.29/13.48 110[0:Inp] ssList(u) singletonP(u) || -> equal(cons(skf47(u),nil),u)**. % 13.29/13.48 114[0:Inp] ssItem(u) ssList(v) || -> equal(hd(cons(u,v)),u)**. % 13.29/13.48 116[0:Inp] || -> equal(app(app(app(skc12,cons(skc10,nil)),cons(skc11,nil)),skc13),skc8)**. % 13.29/13.48 125[0:Inp] ssList(u) ssItem(v) || equal(cons(v,nil),u)*+ -> singletonP(u)*. % 13.29/13.48 132[0:Inp] ssItem(u) ssList(v) || -> equal(app(cons(u,nil),v),cons(u,v))**. % 13.29/13.48 137[0:Inp] ssList(u) ssList(v) || -> equal(nil,v) equal(hd(app(v,u)),hd(v))**. % 13.29/13.48 163[0:Inp] ssList(u) ssList(v) ssList(w) || -> equal(app(app(w,v),u),app(w,app(v,u)))**. % 13.29/13.48 192[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). % 13.29/13.48 197[0:Inp] ssList(u) ssList(v) ssList(w) ssList(x) ssItem(y) ssItem(z) duplicatefreeP(u) || equal(z,y) equal(app(app(x,cons(z,w)),cons(y,v)),u)* -> . % 13.29/13.48 249[0:Res:6.0,137.0] ssList(u) || -> equal(nil,skc8) equal(hd(app(skc8,u)),hd(skc8))**. % 13.29/13.48 260[0:Res:6.0,114.0] ssItem(u) || -> equal(hd(cons(u,skc8)),u)**. % 13.29/13.48 272[0:Res:6.0,94.0] ssItem(u) || -> ssList(cons(u,skc8))*. % 13.29/13.48 290[0:Res:6.0,192.1] ssList(u) || equal(tl(skc8),tl(u))* equal(hd(skc8),hd(u)) -> equal(nil,u) equal(skc8,u) equal(nil,skc8). % 13.29/13.48 555[1:Spt:249.0,249.2] ssList(u) || -> equal(hd(app(skc8,u)),hd(skc8))**. % 13.29/13.48 1624[2:Spt:290.5] || -> equal(nil,skc8)**. % 13.29/13.48 1660[2:Rew:1624.0,75.1] ssItem(u) || -> cyclefreeP(cons(u,skc8))*. % 13.29/13.48 1661[2:Rew:1624.0,76.1] ssItem(u) || -> totalorderP(cons(u,skc8))*. % 13.29/13.48 1662[2:Rew:1624.0,77.1] ssItem(u) || -> strictorderP(cons(u,skc8))*. % 13.29/13.48 1663[2:Rew:1624.0,78.1] ssItem(u) || -> totalorderedP(cons(u,skc8))*. % 13.29/13.48 1664[2:Rew:1624.0,79.1] ssItem(u) || -> strictorderedP(cons(u,skc8))*. % 13.29/13.48 1665[2:Rew:1624.0,80.1] ssItem(u) || -> duplicatefreeP(cons(u,skc8))*. % 13.29/13.48 1666[2:Rew:1624.0,81.1] ssItem(u) || -> equalelemsP(cons(u,skc8))*. % 13.29/13.48 1672[2:Rew:1624.0,84.1] ssList(u) || -> equal(app(skc8,u),u)**. % 13.29/13.48 1752[2:Rew:1672.1,555.1] ssList(u) || -> equal(hd(u),hd(skc8))*. % 13.29/13.48 1825[2:SpR:1752.1,260.1] ssList(cons(u,skc8)) ssItem(u) || -> equal(hd(skc8),u)*. % 13.29/13.48 1834[2:SSi:1825.0,272.1,1660.1,1661.1,1662.1,1663.1,1664.1,1665.1,1666.1] ssItem(u) || -> equal(hd(skc8),u)*. % 13.29/13.48 1852[2:SpR:1834.1,1834.1] ssItem(u) ssItem(v) || -> equal(u,v)*. % 13.29/13.48 2041[2:EmS:1852.0,8.0] ssItem(u) || -> equal(skc14,u)*. % 13.29/13.48 2066[2:EmS:2041.0,7.0] || -> equal(skc15,skc14)**. % 13.29/13.48 2069[2:MRR:2066.0,57.0] || -> . % 13.29/13.48 2285[2:Spt:2069.0,290.5,1624.0] || equal(nil,skc8)** -> . % 13.29/13.48 2286[2:Spt:2069.0,290.0,290.1,290.2,290.3,290.4] ssList(u) || equal(tl(skc8),tl(u))* equal(hd(skc8),hd(u)) -> equal(nil,u) equal(skc8,u). % 13.29/13.48 2292[2:MRR:73.1,2285.0] || SkP0(skc9,skc8)* -> . % 13.29/13.48 2410[0:SpR:90.1,81.1] ssItem(skf44(u,v)) || -> SkP0(u,v)* equalelemsP(v). % 13.29/13.48 2418[0:SSi:2410.0,55.0] || -> SkP0(u,v)* equalelemsP(v). % 13.29/13.48 2426[2:Res:2418.0,2292.0] || -> equalelemsP(skc8)*. % 13.29/13.48 2492[0:SpR:110.2,80.1] ssList(u) singletonP(u) ssItem(skf47(u)) || -> duplicatefreeP(u)*. % 13.29/13.48 2503[0:SSi:2492.2,17.0] ssList(u) singletonP(u) || -> duplicatefreeP(u)*. % 13.29/13.48 2568[0:SpR:90.1,114.2] ssItem(skf44(u,v)) ssList(nil) || -> SkP0(u,v) equal(skf44(u,v),hd(v))**. % 13.29/13.48 2572[0:SSi:2568.1,2568.0,16.0,15.0,14.0,13.0,12.0,11.0,10.0,9.0,55.0] || -> SkP0(u,v) equal(skf44(u,v),hd(v))**. % 13.29/13.48 2574[0:Rew:2572.1,90.1] || -> SkP0(u,v)* equal(cons(hd(v),nil),v)**. % 13.29/13.48 2638[0:SpR:2572.1,55.0] || -> SkP0(u,v)* ssItem(hd(v)). % 13.29/13.48 2719[0:Res:109.2,56.0] ssItem(skc11) ssItem(skc10) || -> equal(skc11,skc10)**. % 13.29/13.48 2720[0:SSi:2719.1,2719.0,4.0,3.0] || -> equal(skc11,skc10)**. % 13.29/13.48 2723[0:Rew:2720.0,116.0] || -> equal(app(app(app(skc12,cons(skc10,nil)),cons(skc10,nil)),skc13),skc8)**. % 13.29/13.48 3144[0:EqR:125.2] ssList(cons(u,nil)) ssItem(u) || -> singletonP(cons(u,nil))*. % 13.29/13.48 3149[0:SSi:3144.0,81.0,80.0,79.0,78.0,77.0,76.0,75.0,94.0,16.2,15.1,14.1,13.1,12.1,11.1,10.1,9.1] ssItem(u) || -> singletonP(cons(u,nil))*. % 13.29/13.48 3200[0:SpR:2574.1,3149.1] ssItem(hd(u)) || -> SkP0(v,u)* singletonP(u). % 13.29/13.48 3202[0:MRR:3200.0,2638.1] || -> SkP0(u,v)* singletonP(v). % 13.29/13.48 3205[2:Res:3202.0,2292.0] || -> singletonP(skc8)*. % 13.29/13.48 5191[0:SpR:163.3,2723.0] ssList(skc13) ssList(cons(skc10,nil)) ssList(app(skc12,cons(skc10,nil))) || -> equal(app(app(skc12,cons(skc10,nil)),app(cons(skc10,nil),skc13)),skc8)**. % 13.29/13.48 5248[0:SSi:5191.2,5191.1,5191.0,95.0,2.0,81.0,4.0,80.0,4.0,79.0,4.0,78.0,4.0,77.2,4.0,76.1,4.0,75.1,4.0,3149.1,4.0,94.1,4.0,16.1,15.0,14.1,13.0,12.1,11.0,10.1,9.0,81.0,4.0,80.0,4.0,79.0,4.0,78.0,4.0,77.2,4.0,76.1,4.0,75.1,4.0,3149.1,4.0,94.1,4.0,16.1,15.0,14.1,13.0,12.1,11.0,10.1,9.0,1.2] || -> equal(app(app(skc12,cons(skc10,nil)),app(cons(skc10,nil),skc13)),skc8)**. % 13.29/13.48 10560[0:SpR:132.2,5248.0] ssItem(skc10) ssList(skc13) || -> equal(app(app(skc12,cons(skc10,nil)),cons(skc10,skc13)),skc8)**. % 13.29/13.48 10574[0:SSi:10560.1,10560.0,1.0,4.0] || -> equal(app(app(skc12,cons(skc10,nil)),cons(skc10,skc13)),skc8)**. % 13.29/13.48 13934[0:SpL:10574.0,197.8] ssList(u) ssList(skc13) ssList(nil) ssList(skc12) ssItem(skc10) ssItem(skc10) duplicatefreeP(u) || equal(skc10,skc10)* equal(skc8,u)* -> . % 13.29/13.48 13952[0:Obv:13934.7] ssList(u) ssList(skc13) ssList(nil) ssList(skc12) ssItem(skc10) duplicatefreeP(u) || equal(skc8,u)* -> . % 13.29/13.48 13953[0:SSi:13952.4,13952.3,13952.2,13952.1,4.0,2.0,16.0,15.0,14.0,13.0,12.0,11.0,10.0,9.0,1.0] ssList(u) duplicatefreeP(u) || equal(skc8,u)* -> . % 13.29/13.48 14016[0:EmS:13953.0,13953.1,6.0,2503.2] singletonP(skc8) ssList(skc8) || equal(skc8,skc8)* -> . % 13.29/13.48 14020[0:EmS:13953.0,13953.1,9.0,15.0] || equal(nil,skc8)** -> . % 13.29/13.48 15574[0:Obv:14016.2] singletonP(skc8) ssList(skc8) || -> . % 13.29/13.48 15575[2:SSi:15574.1,6.0,2426.0] singletonP(skc8) || -> . % 13.29/13.48 15576[2:MRR:15575.0,3205.0] || -> . % 13.29/13.48 15753[1:Spt:15576.0,249.1] || -> equal(nil,skc8)**. % 13.29/13.48 16209[1:Rew:15753.0,14020.0] || equal(skc8,skc8)* -> . % 13.29/13.48 16210[1:Obv:16209.0] || -> . % 13.29/13.48 % SZS output end Refutation % 13.29/13.48 Formulae used in the proof : co1 ax2 ax17 ax60 ax62 ax64 ax66 ax69 ax72 ax74 ax4 ax59 ax61 ax63 ax65 ax68 ax71 ax73 ax28 ax16 ax26 ax1 ax23 ax81 ax85 ax82 ax77 ax13 % 13.29/13.48 %------------------------------------------------------------------------------