%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : FLD059-2 : TPTP v8.1.0. Bugfixed v2.1.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 : Sat Jul 16 02:28:34 EDT 2022 % Result : Unsatisfiable 96.46s 96.71s % Output : Refutation 96.46s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.12/0.12 % Problem : FLD059-2 : TPTP v8.1.0. Bugfixed v2.1.0. % 0.12/0.13 % Command : run_spass %d %s % 0.14/0.34 % Computer : n028.cluster.edu % 0.14/0.34 % Model : x86_64 x86_64 % 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.34 % Memory : 8042.1875MB % 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.34 % CPULimit : 300 % 0.14/0.34 % WCLimit : 600 % 0.14/0.34 % DateTime : Mon Jun 6 12:32:28 EDT 2022 % 0.14/0.34 % CPUTime : % 96.46/96.71 % 96.46/96.71 SPASS V 3.9 % 96.46/96.71 SPASS beiseite: Proof found. % 96.46/96.71 % SZS status Theorem % 96.46/96.71 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 96.46/96.71 SPASS derived 26024 clauses, backtracked 0 clauses, performed 0 splits and kept 17014 clauses. % 96.46/96.71 SPASS allocated 101903 KBytes. % 96.46/96.71 SPASS spent 0:1:34.27 on the problem. % 96.46/96.71 0:00:00.03 for the input. % 96.46/96.71 0:00:00.00 for the FLOTTER CNF translation. % 96.46/96.71 0:00:00.38 for inferences. % 96.46/96.71 0:00:00.00 for the backtracking. % 96.46/96.71 0:1:33.61 for the reduction. % 96.46/96.71 % 96.46/96.71 % 96.46/96.71 Here is a proof with depth 7, length 60 : % 96.46/96.71 % SZS output start Refutation % 96.46/96.71 1[0:Inp] || -> defined(a)*. % 96.46/96.71 2[0:Inp] || -> defined(u__dfg)*. % 96.46/96.71 3[0:Inp] || -> less_or_equal(additive_identity,a)*r. % 96.46/96.71 4[0:Inp] || -> equalish(add(a,a),u__dfg)*l. % 96.46/96.71 5[0:Inp] || less_or_equal(additive_identity,u__dfg)*r -> . % 96.46/96.71 7[0:Inp] defined(u) || -> equalish(add(additive_identity,u),u)*l. % 96.46/96.71 8[0:Inp] defined(u) || -> equalish(add(u,additive_inverse(u)),additive_identity)*l. % 96.46/96.71 9[0:Inp] defined(u) defined(v) || -> equalish(add(v,u),add(u,v))*. % 96.46/96.71 15[0:Inp] defined(u) defined(v) || -> defined(add(v,u))*. % 96.46/96.71 16[0:Inp] || -> defined(additive_identity)*. % 96.46/96.71 17[0:Inp] defined(u) || -> defined(additive_inverse(u))*. % 96.46/96.71 21[0:Inp] || less_or_equal(u,v)*+ less_or_equal(v,u)* -> equalish(v,u). % 96.46/96.71 22[0:Inp] || less_or_equal(u,v)* less_or_equal(v,w)* -> less_or_equal(u,w)*. % 96.46/96.71 23[0:Inp] defined(u) defined(v) || -> less_or_equal(u,v)* less_or_equal(v,u)*. % 96.46/96.71 24[0:Inp] defined(u) || less_or_equal(v,w) -> less_or_equal(add(v,u),add(w,u))*. % 96.46/96.71 27[0:Inp] || equalish(u,v)* -> equalish(v,u). % 96.46/96.71 28[0:Inp] || equalish(u,v)* equalish(v,w)* -> equalish(u,w)*. % 96.46/96.71 29[0:Inp] defined(u) || equalish(v,w) -> equalish(add(v,u),add(w,u))*. % 96.46/96.71 31[0:Inp] || equalish(u,v)*+ less_or_equal(u,w)* -> less_or_equal(v,w)*. % 96.46/96.71 34[0:Res:3.0,31.0] || equalish(additive_identity,u)*+ -> less_or_equal(u,a)*. % 96.46/96.71 38[0:Res:3.0,24.1] defined(u) || -> less_or_equal(add(additive_identity,u),add(a,u))*r. % 96.46/96.71 39[0:Res:23.2,5.0] defined(additive_identity) defined(u__dfg) || -> less_or_equal(u__dfg,additive_identity)*l. % 96.46/96.71 40[0:Res:31.2,5.0] || equalish(u,additive_identity)*+ less_or_equal(u,u__dfg)* -> . % 96.46/96.71 42[0:Res:4.0,27.0] || -> equalish(u__dfg,add(a,a))*r. % 96.46/96.71 46[0:MRR:39.0,39.1,16.0,2.0] || -> less_or_equal(u__dfg,additive_identity)*l. % 96.46/96.71 66[0:Res:7.1,27.0] defined(u) || -> equalish(u,add(additive_identity,u))*r. % 96.46/96.71 70[0:NCh:28.2,28.0,27.0,7.1] defined(u) || equalish(u,v)*+ -> equalish(v,add(additive_identity,u))*. % 96.46/96.71 81[0:OCh:28.1,28.0,66.1,8.1] defined(additive_inverse(additive_identity)) defined(additive_identity) || -> equalish(additive_inverse(additive_identity),additive_identity)*l. % 96.46/96.71 87[0:SSi:81.1,81.0,16.0,17.1,16.0] || -> equalish(additive_inverse(additive_identity),additive_identity)*l. % 96.46/96.71 88[0:Res:87.0,27.0] || -> equalish(additive_identity,additive_inverse(additive_identity))*r. % 96.46/96.71 104[0:Res:88.0,34.0] || -> less_or_equal(additive_inverse(additive_identity),a)*l. % 96.46/96.71 116[0:NCh:28.2,28.0,9.2,27.0] defined(u) defined(v) || equalish(add(u,v),w)*+ -> equalish(w,add(v,u))*. % 96.46/96.71 171[0:Fac:23.2,23.3] defined(u) defined(u) || -> less_or_equal(u,u)*. % 96.46/96.71 234[0:Obv:171.0] defined(u) || -> less_or_equal(u,u)*. % 96.46/96.71 316[0:NCh:28.2,28.0,40.0,4.0] || equalish(u__dfg,additive_identity) less_or_equal(add(a,a),u__dfg)*l -> . % 96.46/96.71 399[0:OCh:28.1,28.0,29.2,7.1] defined(u) defined(u) || equalish(v,additive_identity) -> equalish(add(v,u),u)*l. % 96.46/96.71 408[0:Obv:399.0] defined(u) || equalish(v,additive_identity) -> equalish(add(v,u),u)*l. % 96.46/96.71 649[0:Res:42.0,31.0] || less_or_equal(u__dfg,u)*+ -> less_or_equal(add(a,a),u)*. % 96.46/96.71 654[0:Res:7.1,31.0] defined(u) || less_or_equal(add(additive_identity,u),v)* -> less_or_equal(u,v). % 96.46/96.71 656[0:Res:87.0,31.0] || less_or_equal(additive_inverse(additive_identity),u)* -> less_or_equal(additive_identity,u). % 96.46/96.71 781[0:NCh:22.2,22.0,656.0,104.0] || less_or_equal(a,u)* -> less_or_equal(additive_identity,u). % 96.46/96.71 1256[0:Res:4.0,70.1] defined(add(a,a)) || -> equalish(u__dfg,add(additive_identity,add(a,a)))*r. % 96.46/96.71 1367[0:SSi:1256.0,15.0,1.0,1.2] || -> equalish(u__dfg,add(additive_identity,add(a,a)))*r. % 96.46/96.71 1918[0:Res:38.1,654.1] defined(u) defined(u) || -> less_or_equal(u,add(a,u))*r. % 96.46/96.71 1949[0:Obv:1918.0] defined(u) || -> less_or_equal(u,add(a,u))*r. % 96.46/96.71 2058[0:Res:1367.0,27.0] || -> equalish(add(additive_identity,add(a,a)),u__dfg)*l. % 96.46/96.71 4120[0:Res:2058.0,116.2] defined(additive_identity) defined(add(a,a)) || -> equalish(u__dfg,add(add(a,a),additive_identity))*r. % 96.46/96.71 4266[0:SSi:4120.1,4120.0,15.0,1.0,1.0,16.2] || -> equalish(u__dfg,add(add(a,a),additive_identity))*r. % 96.46/96.71 5738[0:OCh:28.1,28.0,4266.0,408.2] defined(additive_identity) || equalish(add(a,a),additive_identity)*l -> equalish(u__dfg,additive_identity). % 96.46/96.71 5755[0:SSi:5738.0,16.0] || equalish(add(a,a),additive_identity)*l -> equalish(u__dfg,additive_identity). % 96.46/96.71 22620[0:Res:1949.1,781.0] defined(a) || -> less_or_equal(additive_identity,add(a,a))*r. % 96.46/96.71 22690[0:SSi:22620.0,1.0] || -> less_or_equal(additive_identity,add(a,a))*r. % 96.46/96.71 22889[0:Res:22690.0,21.0] || less_or_equal(add(a,a),additive_identity)*l -> equalish(add(a,a),additive_identity). % 96.46/96.71 33200[0:Res:46.0,649.0] || -> less_or_equal(add(a,a),additive_identity)*l. % 96.46/96.71 33210[0:Res:234.1,649.0] defined(u__dfg) || -> less_or_equal(add(a,a),u__dfg)*l. % 96.46/96.71 33358[0:MRR:22889.0,33200.0] || -> equalish(add(a,a),additive_identity)*l. % 96.46/96.71 33369[0:MRR:5755.0,33358.0] || -> equalish(u__dfg,additive_identity)*l. % 96.46/96.71 33382[0:MRR:316.0,33369.0] || less_or_equal(add(a,a),u__dfg)*l -> . % 96.46/96.71 33536[0:SSi:33210.0,2.0] || -> less_or_equal(add(a,a),u__dfg)*l. % 96.46/96.71 33537[0:MRR:33536.0,33382.0] || -> . % 96.46/96.71 % SZS output end Refutation % 96.46/96.71 Formulae used in the proof : a_is_defined u_is_defined less_or_equal_3 add_equals_u_4 not_less_or_equal_5 existence_of_identity_addition existence_of_inverse_addition commutativity_addition well_definedness_of_addition well_definedness_of_additive_identity well_definedness_of_additive_inverse antisymmetry_of_order_relation transitivity_of_order_relation totality_of_order_relation compatibility_of_order_relation_and_addition symmetry_of_equality transitivity_of_equality compatibility_of_equality_and_addition compatibility_of_equality_and_order_relation % 96.46/96.71 %------------------------------------------------------------------------------