%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : FLD061-1 : TPTP v8.1.0. Bugfixed v2.1.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n019.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:35 EDT 2022 % Result : Unsatisfiable 37.26s 37.52s % Output : Refutation 37.26s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.12/0.12 % Problem : FLD061-1 : TPTP v8.1.0. Bugfixed v2.1.0. % 0.12/0.13 % Command : run_spass %d %s % 0.13/0.35 % Computer : n019.cluster.edu % 0.13/0.35 % Model : x86_64 x86_64 % 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.35 % Memory : 8042.1875MB % 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.35 % CPULimit : 300 % 0.13/0.35 % WCLimit : 600 % 0.13/0.35 % DateTime : Tue Jun 7 00:40:40 EDT 2022 % 0.13/0.35 % CPUTime : % 37.26/37.52 % 37.26/37.52 SPASS V 3.9 % 37.26/37.52 SPASS beiseite: Proof found. % 37.26/37.52 % SZS status Theorem % 37.26/37.52 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 37.26/37.52 SPASS derived 14890 clauses, backtracked 0 clauses, performed 3 splits and kept 9852 clauses. % 37.26/37.52 SPASS allocated 91323 KBytes. % 37.26/37.52 SPASS spent 0:0:36.50 on the problem. % 37.26/37.52 0:00:00.04 for the input. % 37.26/37.52 0:00:00.00 for the FLOTTER CNF translation. % 37.26/37.52 0:00:00.22 for inferences. % 37.26/37.52 0:00:00.05 for the backtracking. % 37.26/37.52 0:0:36.09 for the reduction. % 37.26/37.52 % 37.26/37.52 % 37.26/37.52 Here is a proof with depth 8, length 36 : % 37.26/37.52 % SZS output start Refutation % 37.26/37.52 1[0:Inp] || -> defined(a)*. % 37.26/37.52 2[0:Inp] || -> defined(b)*. % 37.26/37.52 3[0:Inp] || -> defined(c)*. % 37.26/37.52 5[0:Inp] || -> less_or_equal(a,b)*l. % 37.26/37.52 6[0:Inp] || -> less_or_equal(c,d)*l. % 37.26/37.52 7[0:Inp] || less_or_equal(add(a,c),add(d,b))*l -> . % 37.26/37.52 11[0:Inp] defined(u) defined(v) || -> equalish(add(v,u),add(u,v))*. % 37.26/37.52 17[0:Inp] defined(u) defined(v) || -> defined(add(v,u))*. % 37.26/37.52 23[0:Inp] || less_or_equal(u,v)*+ less_or_equal(v,u)* -> equalish(v,u). % 37.26/37.52 24[0:Inp] || less_or_equal(u,v)* less_or_equal(v,w)* -> less_or_equal(u,w)*. % 37.26/37.52 25[0:Inp] defined(u) defined(v) || -> less_or_equal(u,v)* less_or_equal(v,u)*. % 37.26/37.52 26[0:Inp] defined(u) || less_or_equal(v,w) -> less_or_equal(add(v,u),add(w,u))*. % 37.26/37.52 29[0:Inp] || equalish(u,v)* -> equalish(v,u). % 37.26/37.52 30[0:Inp] || equalish(u,v)* equalish(v,w)* -> equalish(u,w)*. % 37.26/37.52 33[0:Inp] || equalish(u,v)*+ less_or_equal(u,w)* -> less_or_equal(v,w)*. % 37.26/37.52 38[0:Res:6.0,26.1] defined(u) || -> less_or_equal(add(c,u),add(d,u))*l. % 37.26/37.52 44[0:Res:33.2,7.0] || equalish(u,add(a,c))* less_or_equal(u,add(d,b)) -> . % 37.26/37.52 114[0:NCh:30.2,30.1,11.2,29.0] defined(u) defined(v) || equalish(w,add(v,u))*+ -> equalish(add(u,v),w)*. % 37.26/37.52 171[0:NCh:24.2,24.0,25.3,7.0] defined(u) defined(add(a,c)) || less_or_equal(u,add(d,b))* -> less_or_equal(u,add(a,c))*. % 37.26/37.52 194[0:SSi:171.1,17.0,1.0,3.2] defined(u) || less_or_equal(u,add(d,b))*+ -> less_or_equal(u,add(a,c))*. % 37.26/37.52 477[0:Res:26.2,23.0] defined(u) || less_or_equal(v,w) less_or_equal(add(w,u),add(v,u))* -> equalish(add(w,u),add(v,u)). % 37.26/37.52 568[0:Res:11.2,33.0] defined(u) defined(v) || less_or_equal(add(v,u),w)*+ -> less_or_equal(add(u,v),w)*. % 37.26/37.52 2417[0:Res:38.1,194.1] defined(b) defined(add(c,b)) || -> less_or_equal(add(c,b),add(a,c))*r. % 37.26/37.52 2437[0:SSi:2417.1,2417.0,17.0,3.0,2.0,2.2] || -> less_or_equal(add(c,b),add(a,c))*r. % 37.26/37.52 5662[0:Res:2437.0,568.2] defined(b) defined(c) || -> less_or_equal(add(b,c),add(a,c))*r. % 37.26/37.52 5708[0:SSi:5662.1,5662.0,3.0,2.0] || -> less_or_equal(add(b,c),add(a,c))*r. % 37.26/37.52 18222[0:Res:5708.0,477.2] defined(c) || less_or_equal(a,b) -> equalish(add(b,c),add(a,c))*r. % 37.26/37.52 18277[0:SSi:18222.0,3.0] || less_or_equal(a,b) -> equalish(add(b,c),add(a,c))*r. % 37.26/37.52 18278[0:MRR:18277.0,5.0] || -> equalish(add(b,c),add(a,c))*r. % 37.26/37.52 18317[0:Res:18278.0,29.0] || -> equalish(add(a,c),add(b,c))*l. % 37.26/37.52 18380[0:Res:18317.0,114.2] defined(c) defined(b) || -> equalish(add(c,b),add(a,c))*r. % 37.26/37.52 18404[0:SSi:18380.1,18380.0,2.0,3.0] || -> equalish(add(c,b),add(a,c))*r. % 37.26/37.52 18584[0:Res:18404.0,44.0] || less_or_equal(add(c,b),add(d,b))*l -> . % 37.26/37.52 19118[0:Res:26.2,18584.0] defined(b) || less_or_equal(c,d)*l -> . % 37.26/37.52 19135[0:SSi:19118.0,2.0] || less_or_equal(c,d)*l -> . % 37.26/37.52 19136[0:MRR:19135.0,6.0] || -> . % 37.26/37.52 % SZS output end Refutation % 37.26/37.52 Formulae used in the proof : a_is_defined b_is_defined c_is_defined less_or_equal_5 less_or_equal_6 not_less_or_equal_7 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 % 37.26/37.52 %------------------------------------------------------------------------------