%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : FLD071-3 : TPTP v8.1.0. Bugfixed v2.1.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n017.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:39 EDT 2022 % Result : Unsatisfiable 0.23s 0.45s % Output : Refutation 0.23s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.13/0.14 % Problem : FLD071-3 : TPTP v8.1.0. Bugfixed v2.1.0. % 0.13/0.15 % Command : run_spass %d %s % 0.16/0.37 % Computer : n017.cluster.edu % 0.16/0.37 % Model : x86_64 x86_64 % 0.16/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.16/0.37 % Memory : 8042.1875MB % 0.16/0.37 % OS : Linux 3.10.0-693.el7.x86_64 % 0.16/0.37 % CPULimit : 300 % 0.16/0.37 % WCLimit : 600 % 0.16/0.37 % DateTime : Mon Jun 6 17:25:16 EDT 2022 % 0.16/0.37 % CPUTime : % 0.23/0.45 % 0.23/0.45 SPASS V 3.9 % 0.23/0.45 SPASS beiseite: Proof found. % 0.23/0.45 % SZS status Theorem % 0.23/0.45 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 0.23/0.45 SPASS derived 68 clauses, backtracked 0 clauses, performed 0 splits and kept 76 clauses. % 0.23/0.45 SPASS allocated 75702 KBytes. % 0.23/0.45 SPASS spent 0:00:00.07 on the problem. % 0.23/0.45 0:00:00.03 for the input. % 0.23/0.45 0:00:00.00 for the FLOTTER CNF translation. % 0.23/0.45 0:00:00.00 for inferences. % 0.23/0.45 0:00:00.00 for the backtracking. % 0.23/0.45 0:00:00.01 for the reduction. % 0.23/0.45 % 0.23/0.45 % 0.23/0.45 Here is a proof with depth 3, length 14 : % 0.23/0.45 % SZS output start Refutation % 0.23/0.45 1[0:Inp] || -> defined(a)*. % 0.23/0.45 2[0:Inp] || -> defined(b)*. % 0.23/0.45 3[0:Inp] || -> less_or_equal(additive_identity,a)*r. % 0.23/0.45 4[0:Inp] || -> less_or_equal(additive_identity,b)*r. % 0.23/0.45 5[0:Inp] || less_or_equal(additive_identity,multiply(a,b))*r -> . % 0.23/0.45 15[0:Inp] || product(u,v,w)*+ -> product(v,u,w)*. % 0.23/0.45 25[0:Inp] defined(u) defined(v) || -> product(v,u,multiply(v,u))*. % 0.23/0.45 30[0:Inp] || less_or_equal(additive_identity,u) less_or_equal(additive_identity,v) product(v,u,w)* -> less_or_equal(additive_identity,w). % 0.23/0.45 32[0:Res:4.0,30.0] || less_or_equal(additive_identity,u) product(b,u,v)* -> less_or_equal(additive_identity,v). % 0.23/0.45 48[0:Res:3.0,32.0] || product(b,a,u)* -> less_or_equal(additive_identity,u). % 0.23/0.45 84[0:Res:25.2,15.0] defined(u) defined(v) || -> product(u,v,multiply(v,u))*. % 0.23/0.45 108[0:Res:84.2,48.0] defined(b) defined(a) || -> less_or_equal(additive_identity,multiply(a,b))*r. % 0.23/0.45 110[0:SSi:108.1,108.0,1.0,2.0] || -> less_or_equal(additive_identity,multiply(a,b))*r. % 0.23/0.45 111[0:MRR:110.0,5.0] || -> . % 0.23/0.45 % SZS output end Refutation % 0.23/0.45 Formulae used in the proof : a_is_defined b_is_defined less_or_equal_3 less_or_equal_4 not_less_or_equal_5 commutativity_multiplication totality_of_multiplication compatibility_of_order_relation_and_multiplication % 0.23/0.45 %------------------------------------------------------------------------------