%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : SWC163+1 : TPTP v8.1.0. Released v2.4.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n029.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.62s 13.89s % Output : Refutation 13.62s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.10/0.12 % Problem : SWC163+1 : TPTP v8.1.0. Released v2.4.0. % 0.10/0.12 % Command : run_spass %d %s % 0.13/0.33 % Computer : n029.cluster.edu % 0.13/0.33 % Model : x86_64 x86_64 % 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.33 % Memory : 8042.1875MB % 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.33 % CPULimit : 300 % 0.13/0.33 % WCLimit : 600 % 0.13/0.33 % DateTime : Sun Jun 12 02:33:24 EDT 2022 % 0.13/0.34 % CPUTime : % 13.62/13.89 % 13.62/13.89 SPASS V 3.9 % 13.62/13.89 SPASS beiseite: Proof found. % 13.62/13.89 % SZS status Theorem % 13.62/13.89 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 13.62/13.89 SPASS derived 10107 clauses, backtracked 4344 clauses, performed 42 splits and kept 7797 clauses. % 13.62/13.89 SPASS allocated 113068 KBytes. % 13.62/13.89 SPASS spent 0:0:12.60 on the problem. % 13.62/13.89 0:00:00.04 for the input. % 13.62/13.89 0:00:00.06 for the FLOTTER CNF translation. % 13.62/13.89 0:00:00.11 for inferences. % 13.62/13.89 0:00:00.43 for the backtracking. % 13.62/13.89 0:0:11.72 for the reduction. % 13.62/13.89 % 13.62/13.89 % 13.62/13.89 Here is a proof with depth 6, length 97 : % 13.62/13.89 % SZS output start Refutation % 13.62/13.89 1[0:Inp] || -> ssList(skc13)*. % 13.62/13.89 2[0:Inp] || -> ssList(skc12)*. % 13.62/13.89 3[0:Inp] || -> ssItem(skc11)*. % 13.62/13.89 4[0:Inp] || -> ssItem(skc10)*. % 13.62/13.89 6[0:Inp] || -> ssList(skc8)*. % 13.62/13.89 7[0:Inp] || -> ssItem(skc15)*. % 13.62/13.89 8[0:Inp] || -> ssItem(skc14)*. % 13.62/13.89 9[0:Inp] || -> ssList(nil)*. % 13.62/13.89 10[0:Inp] || -> cyclefreeP(nil)*. % 13.62/13.89 11[0:Inp] || -> totalorderP(nil)*. % 13.62/13.89 12[0:Inp] || -> strictorderP(nil)*. % 13.62/13.89 13[0:Inp] || -> totalorderedP(nil)*. % 13.62/13.89 14[0:Inp] || -> strictorderedP(nil)*. % 13.62/13.89 15[0:Inp] || -> duplicatefreeP(nil)*. % 13.62/13.89 16[0:Inp] || -> equalelemsP(nil)*. % 13.62/13.89 17[0:Inp] || -> ssItem(skf47(u))*. % 13.62/13.89 55[0:Inp] || -> ssItem(skf44(u,v))*. % 13.62/13.89 56[0:Inp] || neq(skc10,skc11)* -> . % 13.62/13.89 57[0:Inp] || equal(skc15,skc14)** -> . % 13.62/13.89 73[0:Inp] || SkP0(skc9,skc8)* -> equal(nil,skc8). % 13.62/13.89 75[0:Inp] ssItem(u) || -> cyclefreeP(cons(u,nil))*. % 13.62/13.89 76[0:Inp] ssItem(u) || -> totalorderP(cons(u,nil))*. % 13.62/13.89 77[0:Inp] ssItem(u) || -> strictorderP(cons(u,nil))*. % 13.62/13.89 78[0:Inp] ssItem(u) || -> totalorderedP(cons(u,nil))*. % 13.62/13.89 79[0:Inp] ssItem(u) || -> strictorderedP(cons(u,nil))*. % 13.62/13.89 80[0:Inp] ssItem(u) || -> duplicatefreeP(cons(u,nil))*. % 13.62/13.89 81[0:Inp] ssItem(u) || -> equalelemsP(cons(u,nil))*. % 13.62/13.89 84[0:Inp] ssList(u) || -> equal(app(nil,u),u)**. % 13.62/13.89 90[0:Inp] || -> SkP0(u,v) equal(cons(skf44(u,v),nil),v)**. % 13.62/13.89 94[0:Inp] ssItem(u) ssList(v) || -> ssList(cons(u,v))*. % 13.62/13.89 95[0:Inp] ssList(u) ssList(v) || -> ssList(app(v,u))*. % 13.62/13.89 109[0:Inp] ssItem(u) ssItem(v) || -> neq(v,u)* equal(v,u). % 13.62/13.89 110[0:Inp] ssList(u) singletonP(u) || -> equal(cons(skf47(u),nil),u)**. % 13.62/13.89 114[0:Inp] ssItem(u) ssList(v) || -> equal(hd(cons(u,v)),u)**. % 13.62/13.89 116[0:Inp] || -> equal(app(app(app(skc12,cons(skc10,nil)),cons(skc11,nil)),skc13),skc8)**. % 13.62/13.89 125[0:Inp] ssList(u) ssItem(v) || equal(cons(v,nil),u)*+ -> singletonP(u)*. % 13.62/13.89 132[0:Inp] ssItem(u) ssList(v) || -> equal(app(cons(u,nil),v),cons(u,v))**. % 13.62/13.89 137[0:Inp] ssList(u) ssList(v) || -> equal(nil,v) equal(hd(app(v,u)),hd(v))**. % 13.62/13.89 163[0:Inp] ssList(u) ssList(v) ssList(w) || -> equal(app(app(w,v),u),app(w,app(v,u)))**. % 13.62/13.89 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.62/13.89 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.62/13.89 249[0:Res:6.0,137.0] ssList(u) || -> equal(nil,skc8) equal(hd(app(skc8,u)),hd(skc8))**. % 13.62/13.89 260[0:Res:6.0,114.0] ssItem(u) || -> equal(hd(cons(u,skc8)),u)**. % 13.62/13.89 272[0:Res:6.0,94.0] ssItem(u) || -> ssList(cons(u,skc8))*. % 13.62/13.89 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.62/13.89 555[1:Spt:249.0,249.2] ssList(u) || -> equal(hd(app(skc8,u)),hd(skc8))**. % 13.62/13.89 1624[2:Spt:290.5] || -> equal(nil,skc8)**. % 13.62/13.89 1660[2:Rew:1624.0,75.1] ssItem(u) || -> cyclefreeP(cons(u,skc8))*. % 13.62/13.89 1661[2:Rew:1624.0,76.1] ssItem(u) || -> totalorderP(cons(u,skc8))*. % 13.62/13.89 1662[2:Rew:1624.0,77.1] ssItem(u) || -> strictorderP(cons(u,skc8))*. % 13.62/13.89 1663[2:Rew:1624.0,78.1] ssItem(u) || -> totalorderedP(cons(u,skc8))*. % 13.62/13.89 1664[2:Rew:1624.0,79.1] ssItem(u) || -> strictorderedP(cons(u,skc8))*. % 13.62/13.89 1665[2:Rew:1624.0,80.1] ssItem(u) || -> duplicatefreeP(cons(u,skc8))*. % 13.62/13.89 1666[2:Rew:1624.0,81.1] ssItem(u) || -> equalelemsP(cons(u,skc8))*. % 13.62/13.89 1672[2:Rew:1624.0,84.1] ssList(u) || -> equal(app(skc8,u),u)**. % 13.62/13.89 1752[2:Rew:1672.1,555.1] ssList(u) || -> equal(hd(u),hd(skc8))*. % 13.62/13.89 1825[2:SpR:1752.1,260.1] ssList(cons(u,skc8)) ssItem(u) || -> equal(hd(skc8),u)*. % 13.62/13.89 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.62/13.89 1852[2:SpR:1834.1,1834.1] ssItem(u) ssItem(v) || -> equal(u,v)*. % 13.62/13.89 2041[2:EmS:1852.0,8.0] ssItem(u) || -> equal(skc14,u)*. % 13.62/13.89 2066[2:EmS:2041.0,7.0] || -> equal(skc15,skc14)**. % 13.62/13.89 2069[2:MRR:2066.0,57.0] || -> . % 13.62/13.89 2285[2:Spt:2069.0,290.5,1624.0] || equal(nil,skc8)** -> . % 13.62/13.89 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.62/13.89 2292[2:MRR:73.1,2285.0] || SkP0(skc9,skc8)* -> . % 13.62/13.89 2410[0:SpR:90.1,81.1] ssItem(skf44(u,v)) || -> SkP0(u,v)* equalelemsP(v). % 13.62/13.89 2418[0:SSi:2410.0,55.0] || -> SkP0(u,v)* equalelemsP(v). % 13.62/13.89 2426[2:Res:2418.0,2292.0] || -> equalelemsP(skc8)*. % 13.62/13.89 2492[0:SpR:110.2,80.1] ssList(u) singletonP(u) ssItem(skf47(u)) || -> duplicatefreeP(u)*. % 13.62/13.89 2503[0:SSi:2492.2,17.0] ssList(u) singletonP(u) || -> duplicatefreeP(u)*. % 13.62/13.89 2568[0:SpR:90.1,114.2] ssItem(skf44(u,v)) ssList(nil) || -> SkP0(u,v) equal(skf44(u,v),hd(v))**. % 13.62/13.89 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.62/13.89 2574[0:Rew:2572.1,90.1] || -> SkP0(u,v)* equal(cons(hd(v),nil),v)**. % 13.62/13.89 2638[0:SpR:2572.1,55.0] || -> SkP0(u,v)* ssItem(hd(v)). % 13.62/13.89 2719[0:Res:109.2,56.0] ssItem(skc11) ssItem(skc10) || -> equal(skc11,skc10)**. % 13.62/13.89 2720[0:SSi:2719.1,2719.0,4.0,3.0] || -> equal(skc11,skc10)**. % 13.62/13.89 2723[0:Rew:2720.0,116.0] || -> equal(app(app(app(skc12,cons(skc10,nil)),cons(skc10,nil)),skc13),skc8)**. % 13.62/13.89 3144[0:EqR:125.2] ssList(cons(u,nil)) ssItem(u) || -> singletonP(cons(u,nil))*. % 13.62/13.89 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.62/13.89 3200[0:SpR:2574.1,3149.1] ssItem(hd(u)) || -> SkP0(v,u)* singletonP(u). % 13.62/13.89 3202[0:MRR:3200.0,2638.1] || -> SkP0(u,v)* singletonP(v). % 13.62/13.89 3205[2:Res:3202.0,2292.0] || -> singletonP(skc8)*. % 13.62/13.89 5193[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.62/13.89 5250[0:SSi:5193.2,5193.1,5193.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.62/13.89 10565[0:SpR:132.2,5250.0] ssItem(skc10) ssList(skc13) || -> equal(app(app(skc12,cons(skc10,nil)),cons(skc10,skc13)),skc8)**. % 13.62/13.89 10579[0:SSi:10565.1,10565.0,1.0,4.0] || -> equal(app(app(skc12,cons(skc10,nil)),cons(skc10,skc13)),skc8)**. % 13.62/13.89 13942[0:SpL:10579.0,197.8] ssList(u) ssList(skc13) ssList(nil) ssList(skc12) ssItem(skc10) ssItem(skc10) duplicatefreeP(u) || equal(skc10,skc10)* equal(skc8,u)* -> . % 13.62/13.89 13960[0:Obv:13942.7] ssList(u) ssList(skc13) ssList(nil) ssList(skc12) ssItem(skc10) duplicatefreeP(u) || equal(skc8,u)* -> . % 13.62/13.89 13961[0:SSi:13960.4,13960.3,13960.2,13960.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.62/13.89 14024[0:EmS:13961.0,13961.1,6.0,2503.2] singletonP(skc8) ssList(skc8) || equal(skc8,skc8)* -> . % 13.62/13.89 14028[0:EmS:13961.0,13961.1,9.0,15.0] || equal(nil,skc8)** -> . % 13.62/13.89 15582[0:Obv:14024.2] singletonP(skc8) ssList(skc8) || -> . % 13.62/13.89 15583[2:SSi:15582.1,6.0,2426.0] singletonP(skc8) || -> . % 13.62/13.89 15584[2:MRR:15583.0,3205.0] || -> . % 13.62/13.89 15761[1:Spt:15584.0,249.1] || -> equal(nil,skc8)**. % 13.62/13.89 16217[1:Rew:15761.0,14028.0] || equal(skc8,skc8)* -> . % 13.62/13.89 16218[1:Obv:16217.0] || -> . % 13.62/13.89 % SZS output end Refutation % 13.62/13.89 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.62/13.89 %------------------------------------------------------------------------------