%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : FLD032-1 : TPTP v8.1.0. Bugfixed v2.1.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 : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 600s % DateTime : Sat Jul 16 02:28:24 EDT 2022 % Result : Unsatisfiable 1.06s 1.25s % Output : Refutation 1.06s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : FLD032-1 : TPTP v8.1.0. Bugfixed v2.1.0. % 0.03/0.13 % Command : run_spass %d %s % 0.13/0.34 % Computer : n027.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 600 % 0.13/0.34 % DateTime : Tue Jun 7 03:30:25 EDT 2022 % 0.13/0.34 % CPUTime : % 1.06/1.25 % 1.06/1.25 SPASS V 3.9 % 1.06/1.25 SPASS beiseite: Proof found. % 1.06/1.25 % SZS status Theorem % 1.06/1.25 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 1.06/1.25 SPASS derived 2472 clauses, backtracked 0 clauses, performed 0 splits and kept 1651 clauses. % 1.06/1.25 SPASS allocated 78309 KBytes. % 1.06/1.25 SPASS spent 0:00:00.89 on the problem. % 1.06/1.25 0:00:00.03 for the input. % 1.06/1.25 0:00:00.00 for the FLOTTER CNF translation. % 1.06/1.25 0:00:00.04 for inferences. % 1.06/1.25 0:00:00.00 for the backtracking. % 1.06/1.25 0:00:00.78 for the reduction. % 1.06/1.25 % 1.06/1.25 % 1.06/1.25 Here is a proof with depth 5, length 26 : % 1.06/1.25 % SZS output start Refutation % 1.06/1.25 1[0:Inp] || -> defined(a)*. % 1.06/1.25 2[0:Inp] || equalish(a,additive_identity)*l -> . % 1.06/1.25 3[0:Inp] || -> equalish(multiplicative_inverse(a),multiplicative_identity)*l. % 1.06/1.25 4[0:Inp] || equalish(a,multiplicative_identity)*l -> . % 1.06/1.25 10[0:Inp] defined(u) || -> equalish(multiply(multiplicative_identity,u),u)*l. % 1.06/1.25 11[0:Inp] defined(u) || -> equalish(u,additive_identity) equalish(multiply(u,multiplicative_inverse(u)),multiplicative_identity)*l. % 1.06/1.25 12[0:Inp] defined(u) defined(v) || -> equalish(multiply(v,u),multiply(u,v))*. % 1.06/1.25 19[0:Inp] defined(u) || -> defined(multiplicative_inverse(u))* equalish(u,additive_identity). % 1.06/1.25 26[0:Inp] || equalish(u,v)* -> equalish(v,u). % 1.06/1.25 27[0:Inp] || equalish(u,v)* equalish(v,w)* -> equalish(u,w)*. % 1.06/1.25 29[0:Inp] defined(u) || equalish(v,w) -> equalish(multiply(v,u),multiply(w,u))*. % 1.06/1.25 32[0:Res:26.1,4.0] || equalish(multiplicative_identity,a)*r -> . % 1.06/1.25 38[0:Res:11.2,2.0] defined(a) || -> equalish(multiply(a,multiplicative_inverse(a)),multiplicative_identity)*l. % 1.06/1.25 39[0:Res:19.2,2.0] defined(a) || -> defined(multiplicative_inverse(a))*. % 1.06/1.25 42[0:MRR:39.0,1.0] || -> defined(multiplicative_inverse(a))*. % 1.06/1.25 43[0:MRR:38.0,1.0] || -> equalish(multiply(a,multiplicative_inverse(a)),multiplicative_identity)*l. % 1.06/1.25 55[0:Res:43.0,26.0] || -> equalish(multiplicative_identity,multiply(a,multiplicative_inverse(a)))*r. % 1.06/1.25 80[0:NCh:27.2,27.1,12.2,26.0] defined(u) defined(v) || equalish(w,multiply(v,u))*+ -> equalish(multiply(u,v),w)*. % 1.06/1.25 252[0:OCh:27.1,27.0,29.2,10.1] defined(u) defined(u) || equalish(v,multiplicative_identity) -> equalish(multiply(v,u),u)*l. % 1.06/1.25 265[0:Obv:252.0] defined(u) || equalish(v,multiplicative_identity) -> equalish(multiply(v,u),u)*l. % 1.06/1.25 3023[0:Res:55.0,80.2] defined(multiplicative_inverse(a)) defined(a) || -> equalish(multiply(multiplicative_inverse(a),a),multiplicative_identity)*l. % 1.06/1.25 3150[0:SSi:3023.1,3023.0,1.0,42.0] || -> equalish(multiply(multiplicative_inverse(a),a),multiplicative_identity)*l. % 1.06/1.25 3202[0:Res:3150.0,26.0] || -> equalish(multiplicative_identity,multiply(multiplicative_inverse(a),a))*r. % 1.06/1.25 3271[0:OCh:27.1,27.0,3202.0,265.2] defined(a) || equalish(multiplicative_inverse(a),multiplicative_identity)*l -> equalish(multiplicative_identity,a). % 1.06/1.25 3285[0:SSi:3271.0,1.0] || equalish(multiplicative_inverse(a),multiplicative_identity)*l -> equalish(multiplicative_identity,a). % 1.06/1.25 3286[0:MRR:3285.0,3285.1,3.0,32.0] || -> . % 1.06/1.25 % SZS output end Refutation % 1.06/1.25 Formulae used in the proof : a_is_defined a_not_equal_to_additive_identity_2 multiplicative_inverses_equal a_not_equal_to_multiplicative_identity_4 existence_of_identity_multiplication existence_of_inverse_multiplication commutativity_multiplication well_definedness_of_multiplicative_inverse symmetry_of_equality transitivity_of_equality compatibility_of_equality_and_multiplication % 1.06/1.25 %------------------------------------------------------------------------------