%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : MGT086+1 : TPTP v9.3.1. Bugfixed v9.3.1. % 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 : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 8 06:20:00 AM UTC 2026 % Result : Theorem 78.65s 79.00s % Output : Refutation 78.65s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : MGT086+1 : TPTP v9.3.1. Bugfixed v9.3.1. % 0.00/0.04 % Command : run_spass %d %s % 0.09/0.35 % Computer : n028.cluster.edu % 0.09/0.35 % Model : x86_64 x86_64 % 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.35 % Memory : 8046.5625MB % 0.09/0.35 % OS : Linux 6.8.0-71-generic % 0.09/0.35 % CPULimit : 300 % 0.09/0.35 % WCLimit : 300 % 0.09/0.35 % DateTime : Mon Sep 7 14:22:17 UTC 2026 % 0.09/0.35 % CPUTime : % 78.65/79.00 % 78.65/79.00 SPASS V 3.9 % 78.65/79.00 SPASS beiseite: Proof found. % 78.65/79.00 % SZS status Theorem % 78.65/79.00 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 78.65/79.00 SPASS derived 48473 clauses, backtracked 15 clauses, performed 14 splits and kept 13850 clauses. % 78.65/79.00 SPASS allocated 132233 KBytes. % 78.65/79.00 SPASS spent 0:1:16.12 on the problem. % 78.65/79.00 0:00:00.06 for the input. % 78.65/79.00 0:00:00.06 for the FLOTTER CNF translation. % 78.65/79.00 0:00:01.22 for inferences. % 78.65/79.00 0:00:00.63 for the backtracking. % 78.65/79.00 0:1:13.24 for the reduction. % 78.65/79.00 % 78.65/79.00 % 78.65/79.00 Here is a proof with depth 4, length 29 : % 78.65/79.00 % SZS output start Refutation % 78.65/79.00 9[0:Inp] || -> less(v0,v200)*r. % 78.65/79.00 13[0:Inp] || -> less(v200,v400)*r. % 78.65/79.00 18[0:Inp] || -> less(v600,v800)*r. % 78.65/79.00 28[0:Inp] || equal(v800,v600)** -> . % 78.65/79.00 34[0:Inp] || equal(u,v)* -> leq(u,v). % 78.65/79.00 35[0:Inp] || less(u,v)* -> leq(u,v). % 78.65/79.00 38[0:Inp] || in_lopen(u,v,w)* -> less(v,u). % 78.65/79.00 39[0:Inp] || in_lopen(u,v,w)* -> leq(u,w). % 78.65/79.00 48[0:Inp] || leq(u,v)*+ leq(v,u)* -> equal(v,u). % 78.65/79.00 51[0:Inp] || leq(u,v)* leq(v,w)* -> leq(u,w)*. % 78.65/79.00 53[0:Inp] || less(u,v) leq(v,w) -> in_lopen(v,u,w)*. % 78.65/79.00 69[0:Inp] || leq(v800,u)+ in_lopen(v,v0,v200) in_lopen(v,v0,v400)* -> in_lopen(u,v0,v600)*. % 78.65/79.00 98[0:EqR:34.0] || -> leq(u,u)*. % 78.65/79.00 136[0:Res:18.0,35.0] || -> leq(v600,v800)*r. % 78.65/79.00 143[0:Res:13.0,35.0] || -> leq(v200,v400)*r. % 78.65/79.00 332[0:Res:136.0,48.0] || leq(v800,v600)*l -> equal(v800,v600). % 78.65/79.00 362[0:MRR:332.1,28.0] || leq(v800,v600)*l -> . % 78.65/79.00 440[1:Spt:69.0,69.3] || leq(v800,u) -> in_lopen(u,v0,v600)*. % 78.65/79.00 443[1:Res:440.1,39.0] || leq(v800,u)* -> leq(u,v600). % 78.65/79.00 934[1:Res:98.0,443.0] || -> leq(v800,v600)*l. % 78.65/79.00 943[1:MRR:934.0,362.0] || -> . % 78.65/79.00 944[1:Spt:943.0,69.1,69.2] || in_lopen(u,v0,v200) in_lopen(u,v0,v400)* -> . % 78.65/79.00 946[1:Res:53.2,944.1] || less(v0,u) leq(u,v400) in_lopen(u,v0,v200)* -> . % 78.65/79.00 947[1:MRR:946.0,38.1] || leq(u,v400) in_lopen(u,v0,v200)* -> . % 78.65/79.00 948[1:Res:53.2,947.1] || less(v0,u) leq(u,v200) leq(u,v400)* -> . % 78.65/79.00 36243[0:CRe:51.1,143.0] || leq(u,v200)*+ -> leq(u,v400)*. % 78.65/79.00 36261[1:MRR:948.2,36243.1] || less(v0,u) leq(u,v200)* -> . % 78.65/79.00 51293[1:Res:98.0,36261.1] || less(v0,v200)*r -> . % 78.65/79.00 51384[1:MRR:51293.0,9.0] || -> . % 78.65/79.00 % SZS output end Refutation % 78.65/79.00 Formulae used in the proof : ord_v0_v200 ord_v200_v400 ord_v600_v800 distinct leq_def less_implies_leq in_lopen leq_antisym leq_trans odrl462 % 78.65/79.00 %------------------------------------------------------------------------------