%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : NUM541+2 : TPTP v8.1.0. Released v4.0.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n028.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 : Mon Jul 18 14:27:18 EDT 2022 % Result : Theorem 0.65s 0.83s % Output : Refutation 0.65s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.12 % Problem : NUM541+2 : TPTP v8.1.0. Released v4.0.0. % 0.06/0.13 % Command : run_spass %d %s % 0.12/0.32 % Computer : n028.cluster.edu % 0.12/0.32 % Model : x86_64 x86_64 % 0.12/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.32 % Memory : 8042.1875MB % 0.12/0.32 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.32 % CPULimit : 300 % 0.12/0.32 % WCLimit : 600 % 0.12/0.32 % DateTime : Fri Jul 8 01:13:09 EDT 2022 % 0.12/0.32 % CPUTime : % 0.65/0.83 % 0.65/0.83 SPASS V 3.9 % 0.65/0.83 SPASS beiseite: Proof found. % 0.65/0.83 % SZS status Theorem % 0.65/0.83 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 0.65/0.83 SPASS derived 1590 clauses, backtracked 162 clauses, performed 8 splits and kept 827 clauses. % 0.65/0.83 SPASS allocated 99649 KBytes. % 0.65/0.83 SPASS spent 0:00:00.49 on the problem. % 0.65/0.83 0:00:00.04 for the input. % 0.65/0.83 0:00:00.11 for the FLOTTER CNF translation. % 0.65/0.83 0:00:00.03 for inferences. % 0.65/0.83 0:00:00.00 for the backtracking. % 0.65/0.83 0:00:00.28 for the reduction. % 0.65/0.83 % 0.65/0.83 % 0.65/0.83 Here is a proof with depth 3, length 44 : % 0.65/0.83 % SZS output start Refutation % 0.65/0.83 5[0:Inp] || -> aElementOf0(xm,szNzAzT0)*. % 0.65/0.83 6[0:Inp] || -> aElementOf0(xn,szNzAzT0)*. % 0.65/0.83 9[0:Inp] || equal(xn,xm) -> SkC0*. % 0.65/0.83 10[0:Inp] || -> SkC0 sdtlseqdt0(szszuzczcdt0(xm),szszuzczcdt0(xn))*. % 0.65/0.83 12[0:Inp] || sdtlseqdt0(szszuzczcdt0(xm),xn)* -> SkC0. % 0.65/0.83 21[0:Inp] || aElementOf0(u,szNzAzT0) -> sdtlseqdt0(u,u)*. % 0.65/0.83 23[0:Inp] || SkC0 sdtlseqdt0(szszuzczcdt0(xm),szszuzczcdt0(xn))* -> . % 0.65/0.83 27[0:Inp] || aElementOf0(u,szNzAzT0) -> aElementOf0(szszuzczcdt0(u),szNzAzT0)*. % 0.65/0.83 28[0:Inp] || aElementOf0(u,szNzAzT0) -> sdtlseqdt0(u,szszuzczcdt0(u))*. % 0.65/0.83 30[0:Inp] || SkC0 -> equal(xn,xm) sdtlseqdt0(szszuzczcdt0(xm),xn)*. % 0.65/0.83 31[0:Inp] || SkC0 -> equal(xn,xm) aElementOf0(xm,slbdtrb0(xn))*. % 0.65/0.83 61[0:Inp] || aElementOf0(u,szNzAzT0) aElementOf0(v,szNzAzT0) -> sdtlseqdt0(v,u) sdtlseqdt0(szszuzczcdt0(u),v)*. % 0.65/0.83 69[0:Inp] || aElementOf0(u,szNzAzT0) aElementOf0(v,szNzAzT0) sdtlseqdt0(szszuzczcdt0(v),szszuzczcdt0(u))* -> sdtlseqdt0(v,u). % 0.65/0.83 73[0:Inp] || sdtlseqdt0(u,v)*+ sdtlseqdt0(v,u)* aElementOf0(u,szNzAzT0) aElementOf0(v,szNzAzT0) -> equal(v,u). % 0.65/0.83 90[0:Inp] || sdtlseqdt0(u,v)*+ sdtlseqdt0(w,u)* aElementOf0(v,szNzAzT0) aElementOf0(u,szNzAzT0) aElementOf0(w,szNzAzT0) -> sdtlseqdt0(w,v)*. % 0.65/0.83 108[1:Spt:9.1] || -> SkC0*. % 0.65/0.83 110[1:MRR:23.0,108.0] || sdtlseqdt0(szszuzczcdt0(xm),szszuzczcdt0(xn))* -> . % 0.65/0.83 111[1:MRR:31.0,108.0] || -> equal(xn,xm) aElementOf0(xm,slbdtrb0(xn))*. % 0.65/0.83 112[1:MRR:30.0,108.0] || -> equal(xn,xm) sdtlseqdt0(szszuzczcdt0(xm),xn)*. % 0.65/0.83 114[2:Spt:111.0] || -> equal(xn,xm)**. % 0.65/0.83 117[2:Rew:114.0,110.0] || sdtlseqdt0(szszuzczcdt0(xm),szszuzczcdt0(xm))* -> . % 0.65/0.83 120[2:Res:21.1,117.0] || aElementOf0(szszuzczcdt0(xm),szNzAzT0)* -> . % 0.65/0.83 124[2:Res:27.1,120.0] || aElementOf0(xm,szNzAzT0)* -> . % 0.65/0.83 125[2:MRR:124.0,5.0] || -> . % 0.65/0.83 126[2:Spt:125.0,111.0,114.0] || equal(xn,xm)** -> . % 0.65/0.83 127[2:Spt:125.0,111.1] || -> aElementOf0(xm,slbdtrb0(xn))*. % 0.65/0.83 128[2:MRR:112.0,126.0] || -> sdtlseqdt0(szszuzczcdt0(xm),xn)*. % 0.65/0.83 1673[0:Res:28.1,90.0] || aElementOf0(u,szNzAzT0) sdtlseqdt0(v,u) aElementOf0(szszuzczcdt0(u),szNzAzT0) aElementOf0(u,szNzAzT0) aElementOf0(v,szNzAzT0) -> sdtlseqdt0(v,szszuzczcdt0(u))*. % 0.65/0.83 1682[0:Obv:1673.0] || sdtlseqdt0(u,v) aElementOf0(szszuzczcdt0(v),szNzAzT0) aElementOf0(v,szNzAzT0) aElementOf0(u,szNzAzT0) -> sdtlseqdt0(u,szszuzczcdt0(v))*. % 0.65/0.83 1683[0:MRR:1682.1,27.1] || sdtlseqdt0(u,v) aElementOf0(v,szNzAzT0) aElementOf0(u,szNzAzT0) -> sdtlseqdt0(u,szszuzczcdt0(v))*. % 0.65/0.83 2275[1:Res:1683.3,110.0] || sdtlseqdt0(szszuzczcdt0(xm),xn)* aElementOf0(xn,szNzAzT0) aElementOf0(szszuzczcdt0(xm),szNzAzT0) -> . % 0.65/0.83 2284[2:MRR:2275.0,2275.1,128.0,6.0] || aElementOf0(szszuzczcdt0(xm),szNzAzT0)* -> . % 0.65/0.83 2294[2:Res:27.1,2284.0] || aElementOf0(xm,szNzAzT0)* -> . % 0.65/0.83 2296[2:MRR:2294.0,5.0] || -> . % 0.65/0.83 2299[1:Spt:2296.0,9.1,108.0] || SkC0* -> . % 0.65/0.83 2300[1:Spt:2296.0,9.0] || equal(xn,xm)** -> . % 0.65/0.83 2302[1:MRR:12.1,2299.0] || sdtlseqdt0(szszuzczcdt0(xm),xn)* -> . % 0.65/0.83 2304[1:MRR:10.0,2299.0] || -> sdtlseqdt0(szszuzczcdt0(xm),szszuzczcdt0(xn))*. % 0.65/0.83 2351[1:Res:61.3,2302.0] || aElementOf0(xm,szNzAzT0) aElementOf0(xn,szNzAzT0) -> sdtlseqdt0(xn,xm)*. % 0.65/0.83 2352[1:MRR:2351.0,2351.1,5.0,6.0] || -> sdtlseqdt0(xn,xm)*. % 0.65/0.83 2358[1:Res:2352.0,73.0] || sdtlseqdt0(xm,xn)* aElementOf0(xn,szNzAzT0) aElementOf0(xm,szNzAzT0) -> equal(xn,xm). % 0.65/0.83 2359[1:MRR:2358.1,2358.2,2358.3,6.0,5.0,2300.0] || sdtlseqdt0(xm,xn)* -> . % 0.65/0.83 2361[1:Res:2304.0,69.2] || aElementOf0(xn,szNzAzT0) aElementOf0(xm,szNzAzT0) -> sdtlseqdt0(xm,xn)*. % 0.65/0.83 2364[1:MRR:2361.0,2361.1,2361.2,6.0,5.0,2359.0] || -> . % 0.65/0.83 % SZS output end Refutation % 0.65/0.83 Formulae used in the proof : m__1936 m__ mLessRefl mSuccNum mLessSucc mLessTotal mSuccLess mLessASymm mLessTrans % 0.65/0.83 %------------------------------------------------------------------------------