%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : MGT091+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:01 AM UTC 2026 % Result : Theorem 9.15s 9.48s % Output : Refutation 9.15s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : MGT091+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:25:32 UTC 2026 % 0.13/0.36 % CPUTime : % 9.15/9.48 % 9.15/9.48 SPASS V 3.9 % 9.15/9.48 SPASS beiseite: Proof found. % 9.15/9.48 % SZS status Theorem % 9.15/9.48 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 9.15/9.48 SPASS derived 8863 clauses, backtracked 0 clauses, performed 0 splits and kept 3605 clauses. % 9.15/9.48 SPASS allocated 103739 KBytes. % 9.15/9.48 SPASS spent 0:00:09.00 on the problem. % 9.15/9.48 0:00:00.06 for the input. % 9.15/9.48 0:00:00.06 for the FLOTTER CNF translation. % 9.15/9.48 0:00:00.22 for inferences. % 9.15/9.48 0:00:00.00 for the backtracking. % 9.15/9.48 0:00:08.57 for the reduction. % 9.15/9.48 % 9.15/9.48 % 9.15/9.48 Here is a proof with depth 8, length 50 : % 9.15/9.48 % SZS output start Refutation % 9.15/9.48 8[0:Inp] || -> less(v0,v400)*r. % 9.15/9.48 10[0:Inp] || -> less(v400,v600)*r. % 9.15/9.48 11[0:Inp] || -> less(v400,v800)*r. % 9.15/9.48 25[0:Inp] || less(u,v)* -> leq(u,v). % 9.15/9.48 35[0:Inp] || in_closed(u,v,v)* -> equal(u,v). % 9.15/9.48 36[0:Inp] || equal(u,v) -> in_closed(u,v,v)*. % 9.15/9.48 37[0:Inp] || in_closed(u,v,w)* -> leq(v,u). % 9.15/9.48 38[0:Inp] || in_closed(u,v,w)* -> leq(u,w). % 9.15/9.48 46[0:Inp] || box2_compatible(v0,v600,v0,v600,v400,v800,v400,v800)* -> . % 9.15/9.48 50[0:Inp] || less(u,v)*+ leq(w,u)* -> less(w,v)*. % 9.15/9.48 53[0:Inp] || leq(u,v) leq(v,w) -> in_closed(v,u,w)*. % 9.15/9.48 64[0:Inp] || -> in_closed(skf3(u,v,w,x),x,w)* axis_conflict(x,w,v,u). % 9.15/9.48 65[0:Inp] || -> in_closed(skf3(u,v,w,x),v,u)* axis_conflict(y,z,v,u)*. % 9.15/9.48 66[0:Inp] || -> in_closed(skf5(u,v,w,x),x,w)* axis_subsumes(x,w,v,u). % 9.15/9.48 69[0:Inp] || in_closed(skf5(u,v,w,x),v,u)*+ -> axis_subsumes(y,z,v,u)*. % 9.15/9.48 70[0:Inp] || in_closed(u,v,w)*+ in_closed(u,x,y)* -> axis_compatible(x,y,v,w)*. % 9.15/9.48 71[0:Inp] || in_closed(u,v,w)* axis_subsumes(v,w,x,y)*+ -> in_closed(u,x,y)*. % 9.15/9.48 81[0:Inp] || in_closed(u,v,w)* in_closed(u,x,y)* axis_conflict(x,y,v,w)*+ -> . % 9.15/9.48 84[0:Inp] || axis_compatible(u,v,w,x) axis_compatible(y,z,x1,x2) -> box2_compatible(u,v,y,z,w,x,x1,x2)*. % 9.15/9.48 90[0:Res:84.2,46.0] || axis_compatible(v0,v600,v400,v800)* axis_compatible(v0,v600,v400,v800)* -> . % 9.15/9.48 91[0:Obv:90.0] || axis_compatible(v0,v600,v400,v800)* -> . % 9.15/9.48 110[0:Res:66.0,35.0] || -> axis_subsumes(u,u,v,w) equal(skf5(w,v,u,u),u)**. % 9.15/9.48 111[0:Res:66.0,37.0] || -> axis_subsumes(u,v,w,x) leq(u,skf5(x,w,v,u))*r. % 9.15/9.48 112[0:Res:66.0,38.0] || -> axis_subsumes(u,v,w,x) leq(skf5(x,w,v,u),v)*l. % 9.15/9.48 113[0:SpR:110.1,66.0] || -> axis_subsumes(u,u,v,w)* in_closed(u,u,u)* axis_subsumes(u,u,v,w)*. % 9.15/9.48 115[0:Obv:113.0] || -> in_closed(u,u,u)* axis_subsumes(u,u,v,w)*. % 9.15/9.48 165[0:Res:64.0,70.0] || in_closed(skf3(u,v,w,x),y,z)* -> axis_conflict(x,w,v,u) axis_compatible(y,z,x,w). % 9.15/9.48 170[0:Res:115.1,71.1] || in_closed(u,v,v)*+ -> in_closed(v,v,v)* in_closed(u,w,x)*. % 9.15/9.48 186[0:Res:36.1,170.0] || equal(u,v)*+ -> in_closed(v,v,v)* in_closed(u,w,x)*. % 9.15/9.48 197[0:EqR:186.0] || -> in_closed(u,u,u)* in_closed(u,v,w)*. % 9.15/9.48 198[0:Con:197.1] || -> in_closed(u,u,u)*. % 9.15/9.48 289[0:Res:10.0,25.0] || -> leq(v400,v600)*r. % 9.15/9.48 291[0:Res:8.0,25.0] || -> leq(v0,v400)*r. % 9.15/9.48 820[0:Res:53.2,69.0] || leq(u,skf5(v,u,w,x))+ leq(skf5(v,u,w,x),v)*l -> axis_subsumes(y,z,u,v)*. % 9.15/9.48 920[0:Res:11.0,50.0] || leq(u,v400)*+ -> less(u,v800)*. % 9.15/9.48 959[0:Res:112.1,920.0] || -> axis_subsumes(u,v400,v,w) less(skf5(w,v,v400,u),v800)*l. % 9.15/9.48 1047[0:Res:959.1,25.0] || -> axis_subsumes(u,v400,v,w) leq(skf5(w,v,v400,u),v800)*l. % 9.15/9.48 3072[0:Res:65.0,165.0] || -> axis_conflict(u,v,w,x)* axis_conflict(y,z,w,x) axis_compatible(w,x,y,z)*. % 9.15/9.48 3077[0:Con:3072.0] || -> axis_conflict(u,v,w,x) axis_compatible(w,x,u,v)*. % 9.15/9.48 3158[0:Res:3077.1,91.0] || -> axis_conflict(v400,v800,v0,v600)*. % 9.15/9.48 3167[0:Res:3158.0,81.2] || in_closed(u,v0,v600) in_closed(u,v400,v800)* -> . % 9.15/9.48 6467[0:Res:111.1,820.0] || leq(skf5(u,v,w,v),u)*l -> axis_subsumes(v,w,v,u) axis_subsumes(x,y,v,u)*. % 9.15/9.48 6473[0:Con:6467.2] || leq(skf5(u,v,w,v),u)*l -> axis_subsumes(v,w,v,u). % 9.15/9.48 8281[0:Res:1047.1,6473.0] || -> axis_subsumes(u,v400,u,v800)* axis_subsumes(u,v400,u,v800)*. % 9.15/9.48 8312[0:Obv:8281.0] || -> axis_subsumes(u,v400,u,v800)*. % 9.15/9.48 8328[0:Res:8312.0,71.1] || in_closed(u,v,v400) -> in_closed(u,v,v800)*. % 9.15/9.48 8460[0:Res:8328.1,3167.1] || in_closed(u,v400,v400)* in_closed(u,v0,v600) -> . % 9.15/9.48 9715[0:Res:198.0,8460.0] || in_closed(v400,v0,v600)* -> . % 9.15/9.48 9732[0:Res:53.2,9715.0] || leq(v0,v400) leq(v400,v600)*r -> . % 9.15/9.48 9733[0:MRR:9732.0,9732.1,291.0,289.0] || -> . % 9.15/9.48 % SZS output end Refutation % 9.15/9.48 Formulae used in the proof : ord_v0_v400 ord_v400_v600 ord_v400_v800 less_implies_leq shape_point shape_closed odrl624 leq_less_trans in_closed axis_conflict_def axis_subsumes_def axis_compatible_def box2_overlap % 9.15/9.48 %------------------------------------------------------------------------------