%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : FLD060-1 : TPTP v8.1.0. Bugfixed v2.1.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n024.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 31.98s 32.23s % Output : Refutation 31.98s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.04/0.14 % Problem : FLD060-1 : TPTP v8.1.0. Bugfixed v2.1.0. % 0.04/0.15 % Command : run_spass %d %s % 0.14/0.36 % Computer : n024.cluster.edu % 0.14/0.36 % Model : x86_64 x86_64 % 0.14/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.36 % Memory : 8042.1875MB % 0.14/0.36 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.36 % CPULimit : 300 % 0.14/0.36 % WCLimit : 600 % 0.14/0.36 % DateTime : Mon Jun 6 11:00:05 EDT 2022 % 0.14/0.36 % CPUTime : % 31.98/32.23 % 31.98/32.23 SPASS V 3.9 % 31.98/32.23 SPASS beiseite: Proof found. % 31.98/32.23 % SZS status Theorem % 31.98/32.23 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 31.98/32.23 SPASS derived 13836 clauses, backtracked 0 clauses, performed 1 splits and kept 9125 clauses. % 31.98/32.23 SPASS allocated 90185 KBytes. % 31.98/32.23 SPASS spent 0:0:31.28 on the problem. % 31.98/32.23 0:00:00.04 for the input. % 31.98/32.23 0:00:00.00 for the FLOTTER CNF translation. % 31.98/32.23 0:00:00.20 for inferences. % 31.98/32.23 0:00:00.03 for the backtracking. % 31.98/32.23 0:0:30.92 for the reduction. % 31.98/32.23 % 31.98/32.23 % 31.98/32.23 Here is a proof with depth 8, length 34 : % 31.98/32.23 % SZS output start Refutation % 31.98/32.23 1[0:Inp] || -> defined(a)*. % 31.98/32.23 2[0:Inp] || -> defined(b)*. % 31.98/32.23 3[0:Inp] || -> less_or_equal(a,b)*l. % 31.98/32.23 4[0:Inp] || less_or_equal(add(a,a),add(b,b))*l -> . % 31.98/32.23 8[0:Inp] defined(u) defined(v) || -> equalish(add(v,u),add(u,v))*. % 31.98/32.23 14[0:Inp] defined(u) defined(v) || -> defined(add(v,u))*. % 31.98/32.23 20[0:Inp] || less_or_equal(u,v)*+ less_or_equal(v,u)* -> equalish(v,u). % 31.98/32.23 21[0:Inp] || less_or_equal(u,v)* less_or_equal(v,w)* -> less_or_equal(u,w)*. % 31.98/32.23 22[0:Inp] defined(u) defined(v) || -> less_or_equal(u,v)* less_or_equal(v,u)*. % 31.98/32.23 23[0:Inp] defined(u) || less_or_equal(v,w) -> less_or_equal(add(v,u),add(w,u))*. % 31.98/32.23 26[0:Inp] || equalish(u,v)* -> equalish(v,u). % 31.98/32.23 27[0:Inp] || equalish(u,v)* equalish(v,w)* -> equalish(u,w)*. % 31.98/32.23 30[0:Inp] || equalish(u,v)*+ less_or_equal(u,w)* -> less_or_equal(v,w)*. % 31.98/32.23 35[0:Res:3.0,23.1] defined(u) || -> less_or_equal(add(a,u),add(b,u))*l. % 31.98/32.23 37[0:Res:30.2,4.0] || equalish(u,add(a,a))* less_or_equal(u,add(b,b)) -> . % 31.98/32.23 110[0:NCh:27.2,27.1,8.2,26.0] defined(u) defined(v) || equalish(w,add(v,u))*+ -> equalish(add(u,v),w)*. % 31.98/32.23 183[0:NCh:21.2,21.0,22.3,4.0] defined(u) defined(add(a,a)) || less_or_equal(u,add(b,b))* -> less_or_equal(u,add(a,a))*. % 31.98/32.23 213[0:SSi:183.1,14.0,1.0,1.2] defined(u) || less_or_equal(u,add(b,b))*+ -> less_or_equal(u,add(a,a))*. % 31.98/32.23 560[0:Res:23.2,20.0] defined(u) || less_or_equal(v,w) less_or_equal(add(w,u),add(v,u))* -> equalish(add(w,u),add(v,u)). % 31.98/32.23 629[0:Res:8.2,30.0] defined(u) defined(v) || less_or_equal(add(v,u),w)*+ -> less_or_equal(add(u,v),w)*. % 31.98/32.23 2268[0:Res:35.1,213.1] defined(b) defined(add(a,b)) || -> less_or_equal(add(a,b),add(a,a))*r. % 31.98/32.23 2284[0:SSi:2268.1,2268.0,14.0,1.0,2.0,2.2] || -> less_or_equal(add(a,b),add(a,a))*r. % 31.98/32.23 5352[0:Res:2284.0,629.2] defined(b) defined(a) || -> less_or_equal(add(b,a),add(a,a))*r. % 31.98/32.23 5386[0:SSi:5352.1,5352.0,1.0,2.0] || -> less_or_equal(add(b,a),add(a,a))*r. % 31.98/32.23 17406[0:Res:5386.0,560.2] defined(a) || less_or_equal(a,b) -> equalish(add(b,a),add(a,a))*r. % 31.98/32.23 17451[0:SSi:17406.0,1.0] || less_or_equal(a,b) -> equalish(add(b,a),add(a,a))*r. % 31.98/32.23 17452[0:MRR:17451.0,3.0] || -> equalish(add(b,a),add(a,a))*r. % 31.98/32.23 17484[0:Res:17452.0,26.0] || -> equalish(add(a,a),add(b,a))*l. % 31.98/32.23 17545[0:Res:17484.0,110.2] defined(a) defined(b) || -> equalish(add(a,b),add(a,a))*r. % 31.98/32.23 17569[0:SSi:17545.1,17545.0,2.0,1.0] || -> equalish(add(a,b),add(a,a))*r. % 31.98/32.23 17635[0:Res:17569.0,37.0] || less_or_equal(add(a,b),add(b,b))*l -> . % 31.98/32.23 17801[0:Res:23.2,17635.0] defined(b) || less_or_equal(a,b)*l -> . % 31.98/32.23 17818[0:SSi:17801.0,2.0] || less_or_equal(a,b)*l -> . % 31.98/32.23 17819[0:MRR:17818.0,3.0] || -> . % 31.98/32.23 % SZS output end Refutation % 31.98/32.23 Formulae used in the proof : a_is_defined b_is_defined less_or_equal_3 not_less_or_equal_4 commutativity_addition well_definedness_of_addition 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_order_relation % 31.98/32.23 %------------------------------------------------------------------------------