%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : LCL901+1 : TPTP v9.3.1. Released v5.5.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n027.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Mon Sep 7 01:08:40 PM UTC 2026 % Result : Theorem 123.16s 123.43s % Output : Refutation 123.16s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.04 % Problem : LCL901+1 : TPTP v9.3.1. Released v5.5.0. % 0.00/0.06 % Command : run_spass %d %s % 0.16/0.41 % Computer : n027.cluster.edu % 0.16/0.41 % Model : x86_64 x86_64 % 0.16/0.41 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.16/0.41 % Memory : 8046.5625MB % 0.16/0.41 % OS : Linux 6.8.0-71-generic % 0.16/0.41 % CPULimit : 300 % 0.16/0.41 % WCLimit : 300 % 0.16/0.41 % DateTime : Sat Sep 5 10:25:28 UTC 2026 % 0.16/0.42 % CPUTime : % 123.16/123.43 % 123.16/123.43 SPASS V 3.9 % 123.16/123.43 SPASS beiseite: Proof found. % 123.16/123.43 % SZS status Theorem % 123.16/123.43 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 123.16/123.43 SPASS derived 40985 clauses, backtracked 0 clauses, performed 0 splits and kept 8505 clauses. % 123.16/123.43 SPASS allocated 125379 KBytes. % 123.16/123.43 SPASS spent 0:02:00.50 on the problem. % 123.16/123.43 0:00:00.09 for the input. % 123.16/123.43 0:00:00.07 for the FLOTTER CNF translation. % 123.16/123.43 0:00:00.91 for inferences. % 123.16/123.43 0:00:00.00 for the backtracking. % 123.16/123.43 0:1:59.29 for the reduction. % 123.16/123.43 % 123.16/123.43 % 123.16/123.43 Here is a proof with depth 8, length 48 : % 123.16/123.43 % SZS output start Refutation % 123.16/123.43 1[0:Inp] || -> a62__a61_(u,u)*. % 123.16/123.43 2[0:Inp] || -> a62__a61_(u,0)*. % 123.16/123.43 3[0:Inp] || -> equal(a43_(u,0),u)**. % 123.16/123.43 4[0:Inp] || -> equal(a43_(u,1),1)**. % 123.16/123.43 5[0:Inp] || -> equal(a43_(u,u),u)**. % 123.16/123.43 6[0:Inp] || -> equal(a43_(u,v),a43_(v,u))*. % 123.16/123.43 7[0:Inp] || equal(a61__a61__a62_(a61__a61__a62_(a61__a61__a62_(skc1,1),skc1),skc1),0)** -> . % 123.16/123.43 8[0:Inp] || -> equal(a43_(a43_(u,v),w),a43_(u,a43_(v,w)))**. % 123.16/123.43 10[0:Inp] || a62__a61_(u,v)*+ a62__a61_(v,u)* -> equal(v,u). % 123.16/123.43 11[0:Inp] || a62__a61_(a43_(u,v),w)*+ -> a62__a61_(v,a61__a61__a62_(u,w))*. % 123.16/123.43 12[0:Inp] || a62__a61_(u,a61__a61__a62_(v,w))*+ -> a62__a61_(a43_(v,u),w)*. % 123.16/123.43 13[0:Inp] || a62__a61_(u,v) -> a62__a61_(a43_(u,w),a43_(v,w))*. % 123.16/123.43 15[0:Inp] || a62__a61_(u,v) -> a62__a61_(a61__a61__a62_(w,u),a61__a61__a62_(w,v))*. % 123.16/123.43 16[0:Inp] || -> equal(a61__a61__a62_(a61__a61__a62_(u,v),v),a61__a61__a62_(a61__a61__a62_(v,u),u))*. % 123.16/123.43 25[0:SpR:6.0,4.0] || -> equal(a43_(1,u),1)**. % 123.16/123.43 26[0:SpR:6.0,3.0] || -> equal(a43_(0,u),u)**. % 123.16/123.43 60[0:SpR:5.0,8.0] || -> equal(a43_(u,a43_(u,v)),a43_(u,v))**. % 123.16/123.43 199[0:Res:2.0,10.0] || a62__a61_(0,u)* -> equal(0,u). % 123.16/123.43 568[0:Res:15.1,10.0] || a62__a61_(u,v) a62__a61_(a61__a61__a62_(w,v),a61__a61__a62_(w,u))* -> equal(a61__a61__a62_(w,v),a61__a61__a62_(w,u)). % 123.16/123.43 2464[0:SpR:26.0,13.1] || a62__a61_(u,0) -> a62__a61_(a43_(u,v),v)*l. % 123.16/123.43 2524[0:MRR:2464.0,2.0] || -> a62__a61_(a43_(u,v),v)*l. % 123.16/123.43 2538[0:SpR:25.0,2524.0] || -> a62__a61_(1,u)*. % 123.16/123.43 2561[0:Res:2538.0,10.0] || a62__a61_(u,1)* -> equal(u,1). % 123.16/123.43 2580[0:Res:1.0,12.0] || -> a62__a61_(a43_(u,a61__a61__a62_(u,v)),v)*l. % 123.16/123.43 2792[0:SpL:25.0,11.0] || a62__a61_(1,u) -> a62__a61_(v,a61__a61__a62_(1,u))*. % 123.16/123.43 2812[0:Res:1.0,11.0] || -> a62__a61_(u,a61__a61__a62_(v,a43_(v,u)))*r. % 123.16/123.43 2814[0:Res:2524.0,11.0] || -> a62__a61_(u,a61__a61__a62_(v,u))*r. % 123.16/123.43 2832[0:MRR:2792.0,2538.0] || -> a62__a61_(u,a61__a61__a62_(1,v))*. % 123.16/123.43 3051[0:SpR:26.0,2580.0] || -> a62__a61_(a61__a61__a62_(0,u),u)*l. % 123.16/123.43 3055[0:Res:2580.0,12.0] || -> a62__a61_(a43_(u,a43_(v,a61__a61__a62_(v,a61__a61__a62_(u,w)))),w)*l. % 123.16/123.43 3302[0:SpR:6.0,2812.0] || -> a62__a61_(u,a61__a61__a62_(v,a43_(u,v)))*r. % 123.16/123.43 3333[0:Res:2812.0,199.0] || -> equal(a61__a61__a62_(u,a43_(u,0)),0)**. % 123.16/123.43 3347[0:Rew:3.0,3333.0] || -> equal(a61__a61__a62_(u,u),0)**. % 123.16/123.43 3474[0:Res:2832.0,199.0] || -> equal(a61__a61__a62_(1,u),0)**. % 123.16/123.43 3540[0:SpR:3474.0,16.0] || -> equal(a61__a61__a62_(a61__a61__a62_(u,1),1),a61__a61__a62_(0,u))**. % 123.16/123.43 4031[0:Res:3051.0,10.0] || a62__a61_(u,a61__a61__a62_(0,u))*r -> equal(a61__a61__a62_(0,u),u). % 123.16/123.43 4050[0:MRR:4031.0,2814.0] || -> equal(a61__a61__a62_(0,u),u)**. % 123.16/123.43 4053[0:Rew:4050.0,3540.0] || -> equal(a61__a61__a62_(a61__a61__a62_(u,1),1),u)**. % 123.16/123.43 14729[0:Res:3302.0,568.1] || a62__a61_(a43_(a61__a61__a62_(u,v),u),v) -> equal(a61__a61__a62_(u,a43_(a61__a61__a62_(u,v),u)),a61__a61__a62_(u,v))**. % 123.16/123.43 14783[0:Rew:6.0,14729.1,6.0,14729.0] || a62__a61_(a43_(u,a61__a61__a62_(u,v)),v) -> equal(a61__a61__a62_(u,a43_(u,a61__a61__a62_(u,v))),a61__a61__a62_(u,v))**. % 123.16/123.43 14784[0:MRR:14783.0,2580.0] || -> equal(a61__a61__a62_(u,a43_(u,a61__a61__a62_(u,v))),a61__a61__a62_(u,v))**. % 123.16/123.43 60874[0:Res:3055.0,2561.0] || -> equal(a43_(u,a43_(v,a61__a61__a62_(v,a61__a61__a62_(u,1)))),1)**. % 123.16/123.43 61117[0:SpR:60874.0,60.0] || -> equal(a43_(u,a61__a61__a62_(u,a61__a61__a62_(u,1))),1)**. % 123.16/123.43 61744[0:SpR:61117.0,14784.0] || -> equal(a61__a61__a62_(u,a61__a61__a62_(u,1)),a61__a61__a62_(u,1))**. % 123.16/123.43 62304[0:SpR:4053.0,61744.0] || -> equal(a61__a61__a62_(a61__a61__a62_(u,1),u),u)**. % 123.16/123.43 62400[0:Rew:62304.0,7.0] || equal(a61__a61__a62_(skc1,skc1),0)** -> . % 123.16/123.43 62412[0:Rew:3347.0,62400.0] || equal(0,0)* -> . % 123.16/123.43 62413[0:Obv:62412.0] || -> . % 123.16/123.43 % SZS output end Refutation % 123.16/123.43 Formulae used in the proof : sos_04 sos_08 sos_03 sos_12 sos_14 sos_02 goals_15 sos_01 sos_06 sos_07 sos_09 sos_11 sos_13 % 123.16/123.43 %------------------------------------------------------------------------------