%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : SWC188+1 : TPTP v8.1.0. Released v2.4.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n022.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:21 EDT 2022 % Result : Theorem 10.27s 10.48s % Output : Refutation 10.27s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.13 % Problem : SWC188+1 : TPTP v8.1.0. Released v2.4.0. % 0.03/0.13 % Command : run_spass %d %s % 0.13/0.35 % Computer : n022.cluster.edu % 0.13/0.35 % Model : x86_64 x86_64 % 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.35 % Memory : 8042.1875MB % 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.35 % CPULimit : 300 % 0.13/0.35 % WCLimit : 600 % 0.13/0.35 % DateTime : Sun Jun 12 20:58:03 EDT 2022 % 0.13/0.35 % CPUTime : % 10.27/10.48 % 10.27/10.48 SPASS V 3.9 % 10.27/10.48 SPASS beiseite: Proof found. % 10.27/10.48 % SZS status Theorem % 10.27/10.48 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 10.27/10.48 SPASS derived 10007 clauses, backtracked 2269 clauses, performed 42 splits and kept 6503 clauses. % 10.27/10.48 SPASS allocated 111172 KBytes. % 10.27/10.48 SPASS spent 0:00:09.46 on the problem. % 10.27/10.48 0:00:00.04 for the input. % 10.27/10.48 0:00:00.07 for the FLOTTER CNF translation. % 10.27/10.48 0:00:00.12 for inferences. % 10.27/10.48 0:00:00.29 for the backtracking. % 10.27/10.48 0:00:08.66 for the reduction. % 10.27/10.48 % 10.27/10.48 % 10.27/10.48 Here is a proof with depth 6, length 84 : % 10.27/10.48 % SZS output start Refutation % 10.27/10.48 1[0:Inp] || -> ssList(skc13)*. % 10.27/10.48 2[0:Inp] || -> ssList(skc12)*. % 10.27/10.48 3[0:Inp] || -> ssItem(skc11)*. % 10.27/10.48 4[0:Inp] || -> ssItem(skc10)*. % 10.27/10.48 6[0:Inp] || -> ssList(skc8)*. % 10.27/10.48 8[0:Inp] || -> ssItem(skc14)*. % 10.27/10.48 9[0:Inp] || -> ssList(nil)*. % 10.27/10.48 10[0:Inp] || -> cyclefreeP(nil)*. % 10.27/10.48 11[0:Inp] || -> totalorderP(nil)*. % 10.27/10.48 12[0:Inp] || -> strictorderP(nil)*. % 10.27/10.48 13[0:Inp] || -> totalorderedP(nil)*. % 10.27/10.48 14[0:Inp] || -> strictorderedP(nil)*. % 10.27/10.48 15[0:Inp] || -> duplicatefreeP(nil)*. % 10.27/10.48 16[0:Inp] || -> equalelemsP(nil)*. % 10.27/10.48 55[0:Inp] || -> ssItem(skf44(u,v))*. % 10.27/10.48 56[0:Inp] || equal(skc11,skc10)** -> . % 10.27/10.48 73[0:Inp] || SkP0(skc9,skc8)* -> equal(nil,skc8). % 10.27/10.48 75[0:Inp] ssItem(u) || -> cyclefreeP(cons(u,nil))*. % 10.27/10.48 76[0:Inp] ssItem(u) || -> totalorderP(cons(u,nil))*. % 10.27/10.48 77[0:Inp] ssItem(u) || -> strictorderP(cons(u,nil))*. % 10.27/10.48 78[0:Inp] ssItem(u) || -> totalorderedP(cons(u,nil))*. % 10.27/10.48 79[0:Inp] ssItem(u) || -> strictorderedP(cons(u,nil))*. % 10.27/10.48 80[0:Inp] ssItem(u) || -> duplicatefreeP(cons(u,nil))*. % 10.27/10.48 81[0:Inp] ssItem(u) || -> equalelemsP(cons(u,nil))*. % 10.27/10.48 84[0:Inp] ssList(u) || -> equal(app(nil,u),u)**. % 10.27/10.48 90[0:Inp] || -> SkP0(u,v) equal(cons(skf44(u,v),nil),v)**. % 10.27/10.48 94[0:Inp] ssItem(u) ssList(v) || -> ssList(cons(u,v))*. % 10.27/10.48 95[0:Inp] ssList(u) ssList(v) || -> ssList(app(v,u))*. % 10.27/10.48 114[0:Inp] ssItem(u) ssList(v) || -> equal(hd(cons(u,v)),u)**. % 10.27/10.48 116[0:Inp] || -> equal(app(app(app(skc12,cons(skc10,nil)),cons(skc11,nil)),skc13),skc8)**. % 10.27/10.48 125[0:Inp] ssList(u) ssItem(v) || equal(cons(v,nil),u)*+ -> singletonP(u)*. % 10.27/10.48 132[0:Inp] ssItem(u) ssList(v) || -> equal(app(cons(u,nil),v),cons(u,v))**. % 10.27/10.48 137[0:Inp] ssList(u) ssList(v) || -> equal(nil,v) equal(hd(app(v,u)),hd(v))**. % 10.27/10.48 163[0:Inp] ssList(u) ssList(v) ssList(w) || -> equal(app(app(w,v),u),app(w,app(v,u)))**. % 10.27/10.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). % 10.27/10.48 194[0:Inp] ssList(u) ssList(v) ssList(w) ssItem(x) ssItem(y) equalelemsP(u) || equal(app(w,cons(y,cons(x,v))),u)* -> equal(y,x). % 10.27/10.48 249[0:Res:6.0,137.0] ssList(u) || -> equal(nil,skc8) equal(hd(app(skc8,u)),hd(skc8))**. % 10.27/10.48 260[0:Res:6.0,114.0] ssItem(u) || -> equal(hd(cons(u,skc8)),u)**. % 10.27/10.48 272[0:Res:6.0,94.0] ssItem(u) || -> ssList(cons(u,skc8))*. % 10.27/10.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). % 10.27/10.48 555[1:Spt:249.0,249.2] ssList(u) || -> equal(hd(app(skc8,u)),hd(skc8))**. % 10.27/10.48 1595[2:Spt:290.5] || -> equal(nil,skc8)**. % 10.27/10.48 1631[2:Rew:1595.0,75.1] ssItem(u) || -> cyclefreeP(cons(u,skc8))*. % 10.27/10.48 1632[2:Rew:1595.0,76.1] ssItem(u) || -> totalorderP(cons(u,skc8))*. % 10.27/10.48 1633[2:Rew:1595.0,77.1] ssItem(u) || -> strictorderP(cons(u,skc8))*. % 10.27/10.48 1634[2:Rew:1595.0,78.1] ssItem(u) || -> totalorderedP(cons(u,skc8))*. % 10.27/10.48 1635[2:Rew:1595.0,79.1] ssItem(u) || -> strictorderedP(cons(u,skc8))*. % 10.27/10.48 1636[2:Rew:1595.0,80.1] ssItem(u) || -> duplicatefreeP(cons(u,skc8))*. % 10.27/10.48 1637[2:Rew:1595.0,81.1] ssItem(u) || -> equalelemsP(cons(u,skc8))*. % 10.27/10.48 1643[2:Rew:1595.0,84.1] ssList(u) || -> equal(app(skc8,u),u)**. % 10.27/10.48 1723[2:Rew:1643.1,555.1] ssList(u) || -> equal(hd(u),hd(skc8))*. % 10.27/10.48 1796[2:SpR:1723.1,260.1] ssList(cons(u,skc8)) ssItem(u) || -> equal(hd(skc8),u)*. % 10.27/10.48 1805[2:SSi:1796.0,272.1,1631.1,1632.1,1633.1,1634.1,1635.1,1636.1,1637.1] ssItem(u) || -> equal(hd(skc8),u)*. % 10.27/10.48 1823[2:SpR:1805.1,1805.1] ssItem(u) ssItem(v) || -> equal(u,v)*. % 10.27/10.48 2012[2:EmS:1823.0,8.0] ssItem(u) || -> equal(skc14,u)*. % 10.27/10.48 2038[2:EmS:2012.0,3.0] || -> equal(skc14,skc11)**. % 10.27/10.48 2039[2:EmS:2012.0,4.0] || -> equal(skc14,skc10)**. % 10.27/10.48 2044[2:Rew:2038.0,2039.0] || -> equal(skc11,skc10)**. % 10.27/10.48 2045[2:MRR:2044.0,56.0] || -> . % 10.27/10.48 2250[2:Spt:2045.0,290.5,1595.0] || equal(nil,skc8)** -> . % 10.27/10.48 2251[2:Spt:2045.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). % 10.27/10.48 2257[2:MRR:73.1,2250.0] || SkP0(skc9,skc8)* -> . % 10.27/10.48 2375[0:SpR:90.1,81.1] ssItem(skf44(u,v)) || -> SkP0(u,v)* equalelemsP(v). % 10.27/10.48 2383[0:SSi:2375.0,55.0] || -> SkP0(u,v)* equalelemsP(v). % 10.27/10.48 2391[2:Res:2383.0,2257.0] || -> equalelemsP(skc8)*. % 10.27/10.48 3162[0:EqR:125.2] ssList(cons(u,nil)) ssItem(u) || -> singletonP(cons(u,nil))*. % 10.27/10.48 3167[0:SSi:3162.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))*. % 10.27/10.48 5313[0:SpR:163.3,116.0] ssList(skc13) ssList(cons(skc11,nil)) ssList(app(skc12,cons(skc10,nil))) || -> equal(app(app(skc12,cons(skc10,nil)),app(cons(skc11,nil),skc13)),skc8)**. % 10.27/10.48 5377[0:SSi:5313.2,5313.1,5313.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,3167.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,3.0,80.0,3.0,79.0,3.0,78.0,3.0,77.2,3.0,76.1,3.0,75.1,3.0,3167.1,3.0,94.1,3.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(skc11,nil),skc13)),skc8)**. % 10.27/10.48 10992[0:SpR:132.2,5377.0] ssItem(skc11) ssList(skc13) || -> equal(app(app(skc12,cons(skc10,nil)),cons(skc11,skc13)),skc8)**. % 10.27/10.48 11006[0:SSi:10992.1,10992.0,1.0,3.0] || -> equal(app(app(skc12,cons(skc10,nil)),cons(skc11,skc13)),skc8)**. % 10.27/10.48 11104[0:SpR:11006.0,163.3] ssList(cons(skc11,skc13)) ssList(cons(skc10,nil)) ssList(skc12) || -> equal(app(skc12,app(cons(skc10,nil),cons(skc11,skc13))),skc8)**. % 10.27/10.48 11136[0:SSi:11104.2,11104.1,11104.0,2.0,81.0,4.2,80.0,4.0,79.0,4.0,78.0,4.0,77.0,4.0,76.0,4.2,75.0,4.1,3167.0,4.1,94.0,4.1,16.0,15.1,14.0,13.1,12.0,11.1,10.0,9.1,94.0,3.1,1.0] || -> equal(app(skc12,app(cons(skc10,nil),cons(skc11,skc13))),skc8)**. % 10.27/10.48 11279[0:SpR:132.2,11136.0] ssItem(skc10) ssList(cons(skc11,skc13)) || -> equal(app(skc12,cons(skc10,cons(skc11,skc13))),skc8)**. % 10.27/10.48 11293[0:SSi:11279.1,11279.0,94.0,3.0,1.0,4.2] || -> equal(app(skc12,cons(skc10,cons(skc11,skc13))),skc8)**. % 10.27/10.48 13388[0:SpL:11293.0,194.6] ssList(u) ssList(skc13) ssList(skc12) ssItem(skc11) ssItem(skc10) equalelemsP(u) || equal(skc8,u)* -> equal(skc11,skc10)**. % 10.27/10.48 13392[0:SSi:13388.4,13388.3,13388.2,13388.1,4.0,3.0,2.0,1.0] ssList(u) equalelemsP(u) || equal(skc8,u)* -> equal(skc11,skc10)**. % 10.27/10.48 13393[0:MRR:13392.3,56.0] ssList(u) equalelemsP(u) || equal(skc8,u)* -> . % 10.27/10.48 13691[2:EmS:13393.0,13393.1,6.0,2391.0] || equal(skc8,skc8)* -> . % 10.27/10.48 13745[0:EmS:13393.0,13393.1,9.0,16.0] || equal(nil,skc8)** -> . % 10.27/10.48 13746[2:Obv:13691.0] || -> . % 10.27/10.48 13793[1:Spt:13746.0,249.1] || -> equal(nil,skc8)**. % 10.27/10.48 14229[1:Rew:13793.0,13745.0] || equal(skc8,skc8)* -> . % 10.27/10.48 14230[1:Obv:14229.0] || -> . % 10.27/10.48 % SZS output end Refutation % 10.27/10.48 Formulae used in the proof : co1 ax2 ax17 ax60 ax62 ax64 ax66 ax69 ax72 ax74 ax59 ax61 ax63 ax65 ax68 ax71 ax73 ax28 ax16 ax26 ax23 ax4 ax81 ax85 ax82 ax77 ax14 % 10.27/10.48 %------------------------------------------------------------------------------