%------------------------------------------------------------------------------
% File : Enigma---0.5.1
% Problem : MGT091+1 : TPTP v9.3.1. Bugfixed v9.3.1.
% Transfm : none
% Format : tptp:raw
% Command : enigmatic-eprover.py %s %d 1
% Computer : n015.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:08:05 AM UTC 2026
% Result : Theorem 13.48s 3.25s
% Output : CNFRefutation 13.48s
% Verified :
% SZS Type : Refutation
% Derivation depth : 7
% Number of leaves : 8
% Syntax : Number of formulae : 31 ( 14 unt; 0 def)
% Number of atoms : 78 ( 4 equ)
% Maximal formula atoms : 7 ( 2 avg)
% Number of connectives : 82 ( 35 ~; 32 |; 11 &)
% ( 4 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 15 ( 4 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 7 ( 5 usr; 1 prp; 0-8 aty)
% Number of functors : 5 ( 5 usr; 4 con; 0-4 aty)
% Number of variables : 73 ( 0 sgn 39 !; 1 ?)
% Comments :
%------------------------------------------------------------------------------
fof(in_closed,axiom,
! [X1,X4,X5] :
( in_closed(X1,X4,X5)
<=> ( leq(X4,X1)
& leq(X1,X5) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/MGT002+2.ax',in_closed) ).
fof(leq_def,axiom,
! [X1,X2] :
( leq(X1,X2)
<=> ( less(X1,X2)
| X1 = X2 ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/MGT002+0.ax',leq_def) ).
fof(odrl624,conjecture,
box2_compatible(v0,v600,v0,v600,v400,v800,v400,v800),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',odrl624) ).
fof(box2_overlap,axiom,
! [X15,X16,X17,X18,X22,X23,X24,X25] :
( box2_compatible(X15,X16,X17,X18,X22,X23,X24,X25)
<=> ( axis_compatible(X15,X16,X22,X23)
& axis_compatible(X17,X18,X24,X25) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/MGT002+6.ax',box2_overlap) ).
fof(axis_compatible_def,axiom,
! [X6,X7,X8,X9] :
( axis_compatible(X6,X7,X8,X9)
<=> ? [X1] :
( in_closed(X1,X6,X7)
& in_closed(X1,X8,X9) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/MGT002+2.ax',axis_compatible_def) ).
fof(ord_v400_v800,axiom,
less(v400,v800),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ord_v400_v800) ).
fof(ord_v400_v600,axiom,
less(v400,v600),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ord_v400_v600) ).
fof(ord_v0_v400,axiom,
less(v0,v400),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ord_v0_v400) ).
fof(c_0_8,plain,
! [X47,X48,X49] :
( ( leq(X48,X47)
| ~ in_closed(X47,X48,X49) )
& ( leq(X47,X49)
| ~ in_closed(X47,X48,X49) )
& ( ~ leq(X48,X47)
| ~ leq(X47,X49)
| in_closed(X47,X48,X49) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[in_closed])])]) ).
fof(c_0_9,plain,
! [X32,X33] :
( ( ~ leq(X32,X33)
| less(X32,X33)
| X32 = X33 )
& ( ~ less(X32,X33)
| leq(X32,X33) )
& ( X32 != X33
| leq(X32,X33) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[leq_def])])]) ).
fof(c_0_10,negated_conjecture,
~ box2_compatible(v0,v600,v0,v600,v400,v800,v400,v800),
inference(assume_negation,[status(cth)],[odrl624]) ).
cnf(c_0_11,plain,
( in_closed(X2,X1,X3)
| ~ leq(X1,X2)
| ~ leq(X2,X3) ),
inference(split_conjunct,[status(thm)],[c_0_8]) ).
cnf(c_0_12,plain,
( leq(X1,X2)
| ~ less(X1,X2) ),
inference(split_conjunct,[status(thm)],[c_0_9]) ).
cnf(c_0_13,plain,
( leq(X1,X2)
| X1 != X2 ),
inference(split_conjunct,[status(thm)],[c_0_9]) ).
fof(c_0_14,negated_conjecture,
~ box2_compatible(v0,v600,v0,v600,v400,v800,v400,v800),
inference(fof_simplification,[status(thm)],[c_0_10]) ).
fof(c_0_15,plain,
! [X113,X114,X115,X116,X117,X118,X119,X120] :
( ( axis_compatible(X113,X114,X117,X118)
| ~ box2_compatible(X113,X114,X115,X116,X117,X118,X119,X120) )
& ( axis_compatible(X115,X116,X119,X120)
| ~ box2_compatible(X113,X114,X115,X116,X117,X118,X119,X120) )
& ( ~ axis_compatible(X113,X114,X117,X118)
| ~ axis_compatible(X115,X116,X119,X120)
| box2_compatible(X113,X114,X115,X116,X117,X118,X119,X120) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[box2_overlap])])]) ).
fof(c_0_16,plain,
! [X69,X70,X71,X72,X74,X75,X76,X77,X78] :
( ( in_closed(esk2_4(X69,X70,X71,X72),X69,X70)
| ~ axis_compatible(X69,X70,X71,X72) )
& ( in_closed(esk2_4(X69,X70,X71,X72),X71,X72)
| ~ axis_compatible(X69,X70,X71,X72) )
& ( ~ in_closed(X78,X74,X75)
| ~ in_closed(X78,X76,X77)
| axis_compatible(X74,X75,X76,X77) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[axis_compatible_def])])])])])]) ).
cnf(c_0_17,plain,
( in_closed(X1,X2,X3)
| ~ leq(X2,X1)
| ~ less(X1,X3) ),
inference(spm,[status(thm)],[c_0_11,c_0_12]) ).
cnf(c_0_18,plain,
leq(X1,X1),
inference(er,[status(thm)],[c_0_13]) ).
cnf(c_0_19,negated_conjecture,
~ box2_compatible(v0,v600,v0,v600,v400,v800,v400,v800),
inference(split_conjunct,[status(thm)],[c_0_14]) ).
cnf(c_0_20,plain,
( box2_compatible(X1,X2,X5,X6,X3,X4,X7,X8)
| ~ axis_compatible(X1,X2,X3,X4)
| ~ axis_compatible(X5,X6,X7,X8) ),
inference(split_conjunct,[status(thm)],[c_0_15]) ).
cnf(c_0_21,plain,
( axis_compatible(X2,X3,X4,X5)
| ~ in_closed(X1,X2,X3)
| ~ in_closed(X1,X4,X5) ),
inference(split_conjunct,[status(thm)],[c_0_16]) ).
cnf(c_0_22,plain,
( in_closed(X1,X1,X2)
| ~ less(X1,X2) ),
inference(spm,[status(thm)],[c_0_17,c_0_18]) ).
cnf(c_0_23,negated_conjecture,
~ axis_compatible(v0,v600,v400,v800),
inference(spm,[status(thm)],[c_0_19,c_0_20]) ).
cnf(c_0_24,plain,
( axis_compatible(X1,X2,X3,X4)
| ~ in_closed(X3,X1,X2)
| ~ less(X3,X4) ),
inference(spm,[status(thm)],[c_0_21,c_0_22]) ).
cnf(c_0_25,plain,
less(v400,v800),
inference(split_conjunct,[status(thm)],[ord_v400_v800]) ).
cnf(c_0_26,negated_conjecture,
~ in_closed(v400,v0,v600),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_23,c_0_24]),c_0_25])]) ).
cnf(c_0_27,plain,
( in_closed(X1,X2,X3)
| ~ less(X1,X3)
| ~ less(X2,X1) ),
inference(spm,[status(thm)],[c_0_17,c_0_12]) ).
cnf(c_0_28,plain,
less(v400,v600),
inference(split_conjunct,[status(thm)],[ord_v400_v600]) ).
cnf(c_0_29,plain,
less(v0,v400),
inference(split_conjunct,[status(thm)],[ord_v0_v400]) ).
cnf(c_0_30,negated_conjecture,
$false,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_26,c_0_27]),c_0_28]),c_0_29])]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT091+1 : TPTP v9.3.1. Bugfixed v9.3.1.
% 0.00/0.03 % Command : enigmatic-eprover.py %s %d 1
% 0.10/0.37 % Computer : n015.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Mon Sep 7 14:26:19 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.23/0.47 # ENIGMATIC: Selected SinE mode:
% 0.23/0.47 # Parsing /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.23/0.47 # Filter: axfilter_auto 0 goes into file theBenchmark_axfilter_auto 0.p
% 0.23/0.47 # Filter: axfilter_auto 1 goes into file theBenchmark_axfilter_auto 1.p
% 0.23/0.47 # Filter: axfilter_auto 2 goes into file theBenchmark_axfilter_auto 2.p
% 13.48/3.25 # ENIGMATIC: Solved by autoschedule:
% 13.48/3.25 # No SInE strategy applied
% 13.48/3.25 # Trying AutoSched0 for 150 seconds
% 13.48/3.25 # AutoSched0-Mode selected heuristic G_E___302_C18_F1_URBAN_S0Y
% 13.48/3.25 # and selection function SelectMaxLComplexAvoidPosPred.
% 13.48/3.25 #
% 13.48/3.25 # Preprocessing time : 0.033 s
% 13.48/3.25
% 13.48/3.25 # Proof found!
% 13.48/3.25 # SZS status Theorem
% 13.48/3.25 # SZS output start CNFRefutation
% See solution above
% 13.48/3.25 # Training examples: 0 positive, 0 negative
% 13.48/3.25
% 13.48/3.25 # -------------------------------------------------
% 13.48/3.25 # User time : 0.110 s
% 13.48/3.25 # System time : 0.004 s
% 13.48/3.25 # Total time : 0.114 s
% 13.48/3.25 # Maximum resident set size: 3584 pages
% 13.48/3.25
%------------------------------------------------------------------------------