%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : RNG039-2 : TPTP v8.1.0. Released v1.0.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n025.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 20:41:18 EDT 2022 % Result : Unsatisfiable 140.97s 141.18s % Output : Refutation 140.97s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.10/0.12 % Problem : RNG039-2 : TPTP v8.1.0. Released v1.0.0. % 0.10/0.12 % Command : run_spass %d %s % 0.14/0.33 % Computer : n025.cluster.edu % 0.14/0.33 % Model : x86_64 x86_64 % 0.14/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.33 % Memory : 8042.1875MB % 0.14/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.33 % CPULimit : 300 % 0.14/0.33 % WCLimit : 600 % 0.14/0.34 % DateTime : Mon May 30 17:05:12 EDT 2022 % 0.14/0.34 % CPUTime : % 140.97/141.18 % 140.97/141.18 SPASS V 3.9 % 140.97/141.18 SPASS beiseite: Proof found. % 140.97/141.18 % SZS status Theorem % 140.97/141.18 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 140.97/141.18 SPASS derived 57832 clauses, backtracked 0 clauses, performed 0 splits and kept 40334 clauses. % 140.97/141.18 SPASS allocated 99561 KBytes. % 140.97/141.18 SPASS spent 0:2:19.80 on the problem. % 140.97/141.18 0:00:00.04 for the input. % 140.97/141.18 0:00:00.00 for the FLOTTER CNF translation. % 140.97/141.18 0:00:00.56 for inferences. % 140.97/141.18 0:00:00.00 for the backtracking. % 140.97/141.18 0:2:18.18 for the reduction. % 140.97/141.18 % 140.97/141.18 % 140.97/141.18 Here is a proof with depth 9, length 60 : % 140.97/141.18 % SZS output start Refutation % 140.97/141.18 9[0:Inp] || equalish(u,v)*+ product(w,u,x)* -> product(w,v,x)*. % 140.97/141.18 10[0:Inp] || equalish(u,v)*+ product(w,x,u)* -> product(w,x,v)*. % 140.97/141.18 15[0:Inp] || -> product(u,v,multiply(u,v))*. % 140.97/141.18 20[0:Inp] || product(u,v,w)*+ product(x,v,y)* product(z,x,u)* -> product(z,y,w)*. % 140.97/141.18 21[0:Inp] || product(u,v,w)*+ product(x,y,v)* product(u,x,z)* -> product(z,y,w)*. % 140.97/141.18 26[0:Inp] || -> product(additive_identity,u,additive_identity)*. % 140.97/141.18 29[0:Inp] || product(u,v,w)*+ product(u,v,x)* -> equalish(x,w)*. % 140.97/141.18 37[0:Inp] || -> equalish(multiply(u,u),u)*l. % 140.97/141.18 39[0:Inp] || -> equalish(multiply(b,a),d)*l. % 140.97/141.18 41[0:Inp] || -> product(a,c,c)*. % 140.97/141.18 42[0:Inp] || -> product(b,d,d)*. % 140.97/141.18 46[0:Inp] || -> product(a,multiply(b,u),multiply(v,u))*. % 140.97/141.18 60[0:Inp] || -> product(b,a,multiply(b,d))*. % 140.97/141.18 71[0:Inp] || -> product(u,u,u)*. % 140.97/141.18 72[0:Inp] || -> product(a,b,c)*. % 140.97/141.18 73[0:Inp] || -> product(b,a,d)*. % 140.97/141.18 74[0:Inp] || equalish(c,d)*l -> . % 140.97/141.18 80[0:Res:73.0,21.0] || product(b,u,v)*+ product(a,w,u)* -> product(d,w,v)*. % 140.97/141.18 89[0:Res:73.0,20.2] || product(u,v,b)*+ product(v,a,w)* -> product(u,w,d)*. % 140.97/141.18 91[0:Res:73.0,20.1] || product(u,a,v)*+ product(w,b,u)* -> product(w,d,v)*. % 140.97/141.18 92[0:Res:73.0,21.1] || product(u,d,v)*+ product(u,b,w)* -> product(w,a,v)*. % 140.97/141.18 102[0:Res:72.0,29.0] || product(a,b,u)* -> equalish(c,u). % 140.97/141.18 105[0:Res:72.0,21.2] || product(u,v,b)*+ product(a,u,w)* -> product(w,v,c)*. % 140.97/141.18 112[0:Res:72.0,20.1] || product(u,b,v)*+ product(w,a,u)* -> product(w,c,v)*. % 140.97/141.18 120[0:Res:29.2,74.0] || product(u,v,d) product(u,v,c)* -> . % 140.97/141.18 126[0:Res:72.0,92.0] || product(a,d,u)* -> product(c,a,u). % 140.97/141.18 219[0:Res:37.0,10.0] || product(u,v,multiply(w,w))* -> product(u,v,w). % 140.97/141.18 230[0:Res:37.0,9.0] || product(u,multiply(v,v),w)* -> product(u,v,w). % 140.97/141.18 231[0:Res:39.0,9.0] || product(u,multiply(b,a),v)* -> product(u,d,v). % 140.97/141.18 451[0:Res:26.0,21.0] || product(u,v,w)*+ product(additive_identity,u,x)* -> product(x,v,additive_identity)*. % 140.97/141.18 464[0:Res:46.0,21.0] || product(u,v,multiply(b,w))*+ product(a,u,x)* -> product(x,v,multiply(y,w))*. % 140.97/141.18 482[0:Res:42.0,20.0] || product(u,d,v)*+ product(w,u,b)* -> product(w,v,d)*. % 140.97/141.18 487[0:Res:41.0,20.0] || product(u,c,v)*+ product(w,u,a)* -> product(w,v,c)*. % 140.97/141.18 1150[0:Res:46.0,231.0] || -> product(a,d,multiply(u,a))*. % 140.97/141.18 1190[0:Res:1150.0,126.0] || -> product(c,a,multiply(u,a))*. % 140.97/141.18 2135[0:Res:46.0,219.0] || -> product(a,multiply(b,u),u)*. % 140.97/141.18 2141[0:Res:1190.0,219.0] || -> product(c,a,a)*. % 140.97/141.18 2191[0:Res:2135.0,230.0] || -> product(a,b,b)*. % 140.97/141.18 2599[0:Res:2191.0,102.0] || -> equalish(c,b)*r. % 140.97/141.18 2602[0:Res:2599.0,10.0] || product(u,v,c) -> product(u,v,b)*. % 140.97/141.18 3617[0:Res:2191.0,112.0] || product(u,a,a)* -> product(u,c,b). % 140.97/141.18 3693[0:Res:2141.0,91.0] || product(u,b,c)* -> product(u,d,a). % 140.97/141.18 3740[0:Res:71.0,105.0] || product(a,b,u)*+ -> product(u,b,c)*. % 140.97/141.18 4203[0:Res:26.0,482.0] || product(u,additive_identity,b)* -> product(u,additive_identity,d). % 140.97/141.18 4490[0:Res:15.0,451.0] || product(additive_identity,u,v)*+ -> product(v,w,additive_identity)*. % 140.97/141.18 6100[0:Res:71.0,3617.0] || -> product(a,c,b)*. % 140.97/141.18 6121[0:Res:6100.0,89.0] || product(c,a,u) -> product(a,u,d)*. % 140.97/141.18 8751[0:Res:2191.0,3740.0] || -> product(b,b,c)*. % 140.97/141.18 8825[0:Res:8751.0,3693.0] || -> product(b,d,a)*. % 140.97/141.18 8828[0:Res:8825.0,80.0] || product(a,u,d)* -> product(d,u,a). % 140.97/141.18 13903[0:Res:60.0,464.0] || product(a,b,u) -> product(u,a,multiply(v,d))*. % 140.97/141.18 27475[0:Res:6121.1,8828.0] || product(c,a,u)* -> product(d,u,a). % 140.97/141.18 38256[0:Res:15.0,4490.0] || -> product(multiply(additive_identity,u),v,additive_identity)*. % 140.97/141.18 38308[0:Res:38256.0,487.0] || product(u,multiply(additive_identity,v),a)* -> product(u,additive_identity,c). % 140.97/141.18 54735[0:Res:13903.1,27475.0] || product(a,b,c) -> product(d,multiply(u,d),a)*. % 140.97/141.18 54825[0:MRR:54735.0,72.0] || -> product(d,multiply(u,d),a)*. % 140.97/141.18 58155[0:Res:2602.1,4203.0] || product(u,additive_identity,c)* -> product(u,additive_identity,d). % 140.97/141.18 58194[0:MRR:58155.1,120.0] || product(u,additive_identity,c)* -> . % 140.97/141.18 58196[0:MRR:38308.1,58194.0] || product(u,multiply(additive_identity,v),a)* -> . % 140.97/141.18 58208[0:UnC:58196.0,54825.0] || -> . % 140.97/141.18 % SZS output end Refutation % 140.97/141.18 Formulae used in the proof : product_substitution2 product_substitution3 closure_of_multiplication associativity_of_multiplication1 associativity_of_multiplication2 multiplicative_identity1 multiplication_is_well_defined clause35 clause37 clause39 clause40 clause44 clause58 clause71 a_times_b b_times_a prove_c_equals_d % 140.97/141.18 %------------------------------------------------------------------------------