%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : ANA003-4 : TPTP v8.1.0. Released v1.0.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n011.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 : Thu Jul 14 19:28:33 EDT 2022 % Result : Unsatisfiable 0.36s 0.54s % Output : Refutation 0.36s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : ANA003-4 : TPTP v8.1.0. Released v1.0.0. % 0.07/0.13 % Command : run_spass %d %s % 0.14/0.34 % Computer : n011.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 : Fri Jul 8 03:22:09 EDT 2022 % 0.14/0.34 % CPUTime : % 0.36/0.54 % 0.36/0.54 SPASS V 3.9 % 0.36/0.54 SPASS beiseite: Proof found. % 0.36/0.54 % SZS status Theorem % 0.36/0.54 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.36/0.54 SPASS derived 524 clauses, backtracked 14 clauses, performed 4 splits and kept 538 clauses. % 0.36/0.54 SPASS allocated 64865 KBytes. % 0.36/0.54 SPASS spent 0:00:00.18 on the problem. % 0.36/0.54 0:00:00.04 for the input. % 0.36/0.54 0:00:00.00 for the FLOTTER CNF translation. % 0.36/0.54 0:00:00.02 for inferences. % 0.36/0.54 0:00:00.00 for the backtracking. % 0.36/0.54 0:00:00.09 for the reduction. % 0.36/0.54 % 0.36/0.54 % 0.36/0.54 Here is a proof with depth 10, length 34 : % 0.36/0.54 % SZS output start Refutation % 0.36/0.54 1[0:Inp] || less_or_equal(u,minimum(v,w))* -> less_or_equal(u,v). % 0.36/0.54 2[0:Inp] || less_or_equal(u,minimum(v,w))* -> less_or_equal(u,w). % 0.36/0.54 3[0:Inp] || less_or_equal(minimum(u,v),n0)* -> less_or_equal(v,n0) less_or_equal(u,n0). % 0.36/0.54 4[0:Inp] || less_or_equal(u,half(v)) less_or_equal(w,half(v)) -> less_or_equal(add(w,u),v)*. % 0.36/0.54 5[0:Inp] || less_or_equal(half(u),n0)* -> less_or_equal(u,n0). % 0.36/0.54 6[0:Inp] || less_or_equal(delta_1(u),n0)* -> less_or_equal(u,n0). % 0.36/0.54 7[0:Inp] || less_or_equal(delta_2(u),n0)* -> less_or_equal(u,n0). % 0.36/0.54 8[0:Inp] || less_or_equal(absolute(add(u,negate(a_real_number))),delta_1(v)) -> less_or_equal(v,n0) less_or_equal(absolute(add(f(u),negate(f(a_real_number)))),v)*. % 0.36/0.54 9[0:Inp] || less_or_equal(absolute(add(u,negate(a_real_number))),delta_2(v)) -> less_or_equal(v,n0) less_or_equal(absolute(add(g(u),negate(g(a_real_number)))),v)*. % 0.36/0.54 10[0:Inp] || less_or_equal(epsilon_0,n0)* -> . % 0.36/0.54 11[0:Inp] || -> less_or_equal(u,n0) less_or_equal(absolute(add(xs(u),negate(a_real_number))),u)*. % 0.36/0.54 12[0:Inp] || less_or_equal(add(absolute(add(f(xs(u)),negate(f(a_real_number)))),absolute(add(g(xs(u)),negate(g(a_real_number))))),epsilon_0)* -> less_or_equal(u,n0). % 0.36/0.54 14[0:Res:11.1,1.0] || -> less_or_equal(minimum(u,v),n0) less_or_equal(absolute(add(xs(minimum(u,v)),negate(a_real_number))),u)*. % 0.36/0.54 15[0:Res:11.1,2.0] || -> less_or_equal(minimum(u,v),n0) less_or_equal(absolute(add(xs(minimum(u,v)),negate(a_real_number))),v)*. % 0.36/0.54 55[0:Res:4.2,12.0] || less_or_equal(absolute(add(g(xs(u)),negate(g(a_real_number)))),half(epsilon_0)) less_or_equal(absolute(add(f(xs(u)),negate(f(a_real_number)))),half(epsilon_0))* -> less_or_equal(u,n0). % 0.36/0.54 195[0:Res:8.2,55.1] || less_or_equal(absolute(add(xs(u),negate(a_real_number))),delta_1(half(epsilon_0))) less_or_equal(absolute(add(g(xs(u)),negate(g(a_real_number)))),half(epsilon_0))* -> less_or_equal(half(epsilon_0),n0) less_or_equal(u,n0). % 0.36/0.54 480[1:Spt:195.0,195.1,195.3] || less_or_equal(absolute(add(xs(u),negate(a_real_number))),delta_1(half(epsilon_0))) less_or_equal(absolute(add(g(xs(u)),negate(g(a_real_number)))),half(epsilon_0))* -> less_or_equal(u,n0). % 0.36/0.54 491[1:Res:9.2,480.1] || less_or_equal(absolute(add(xs(u),negate(a_real_number))),delta_2(half(epsilon_0))) less_or_equal(absolute(add(xs(u),negate(a_real_number))),delta_1(half(epsilon_0)))* -> less_or_equal(half(epsilon_0),n0) less_or_equal(u,n0). % 0.36/0.54 522[2:Spt:491.0,491.1,491.3] || less_or_equal(absolute(add(xs(u),negate(a_real_number))),delta_2(half(epsilon_0))) less_or_equal(absolute(add(xs(u),negate(a_real_number))),delta_1(half(epsilon_0)))* -> less_or_equal(u,n0). % 0.36/0.54 544[2:Res:15.1,522.1] || less_or_equal(absolute(add(xs(minimum(u,delta_1(half(epsilon_0)))),negate(a_real_number))),delta_2(half(epsilon_0)))* -> less_or_equal(minimum(u,delta_1(half(epsilon_0))),n0) less_or_equal(minimum(u,delta_1(half(epsilon_0))),n0). % 0.36/0.54 555[2:Obv:544.1] || less_or_equal(absolute(add(xs(minimum(u,delta_1(half(epsilon_0)))),negate(a_real_number))),delta_2(half(epsilon_0)))* -> less_or_equal(minimum(u,delta_1(half(epsilon_0))),n0). % 0.36/0.54 589[2:Res:14.1,555.0] || -> less_or_equal(minimum(delta_2(half(epsilon_0)),delta_1(half(epsilon_0))),n0)* less_or_equal(minimum(delta_2(half(epsilon_0)),delta_1(half(epsilon_0))),n0)*. % 0.36/0.54 604[2:Obv:589.0] || -> less_or_equal(minimum(delta_2(half(epsilon_0)),delta_1(half(epsilon_0))),n0)*. % 0.36/0.54 619[2:Res:604.0,3.0] || -> less_or_equal(delta_1(half(epsilon_0)),n0)* less_or_equal(delta_2(half(epsilon_0)),n0). % 0.36/0.54 620[2:Res:619.0,6.0] || -> less_or_equal(delta_2(half(epsilon_0)),n0)* less_or_equal(half(epsilon_0),n0). % 0.36/0.54 621[2:MRR:620.0,7.0] || -> less_or_equal(half(epsilon_0),n0)*. % 0.36/0.54 622[2:Res:621.0,5.0] || -> less_or_equal(epsilon_0,n0)*. % 0.36/0.54 623[2:MRR:622.0,10.0] || -> . % 0.36/0.54 624[2:Spt:623.0,491.2] || -> less_or_equal(half(epsilon_0),n0)*. % 0.36/0.54 625[2:Res:624.0,5.0] || -> less_or_equal(epsilon_0,n0)*. % 0.36/0.54 626[2:MRR:625.0,10.0] || -> . % 0.36/0.54 627[1:Spt:626.0,195.2] || -> less_or_equal(half(epsilon_0),n0)*. % 0.36/0.54 628[1:Res:627.0,5.0] || -> less_or_equal(epsilon_0,n0)*. % 0.36/0.54 629[1:MRR:628.0,10.0] || -> . % 0.36/0.54 % SZS output end Refutation % 0.36/0.54 Formulae used in the proof : minimum3 minimum7 minimum9 less_or_equal_sum_of_halves zero_and_half clause_1 clause_2 clause_3 clause_4 clause_5 clause_6 clause_7_2 % 0.36/0.54 %------------------------------------------------------------------------------