%------------------------------------------------------------------------------
% File : hopCoP---0.1
% Problem : MGT070+1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n018.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:11:31 AM UTC 2026
% Result : Theorem 0.11s 0.37s
% Output : CNFRefutation 0.11s
% Verified :
% SZS Type : Refutation
% Derivation depth : 4
% Number of leaves : 6
% Syntax : Number of formulae : 22 ( 12 unt; 0 def)
% Number of atoms : 46 ( 3 equ)
% Maximal formula atoms : 5 ( 2 avg)
% Number of connectives : 41 ( 17 ~; 15 |; 7 &)
% ( 1 <=>; 1 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 3 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 5 ( 3 usr; 1 prp; 0-3 aty)
% Number of functors : 3 ( 3 usr; 3 con; 0-0 aty)
% Number of variables : 19 ( 2 sgn 8 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(unknown_sound_compatible,plain,
? [V] :
( leq(ninf,V)
& leq(V,nsup)
& completion_compatible(V,ninf,nsup) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unknown_sound_compatible) ).
fof(unknown_sound_compatible_negated,plain,
~ ? [V] :
( leq(ninf,V)
& leq(V,nsup)
& completion_compatible(V,ninf,nsup) ),
inference(negate_conjecture,[status(cth)],[unknown_sound_compatible]) ).
cnf(58,plain,
( ~ completion_compatible(X0,ninf,nsup)
| ~ leq(X0,nsup)
| ~ leq(ninf,X0) ),
inference(cnf,[status(esa)],[unknown_sound_compatible_negated]) ).
cnf(l0,plain,
( ~ completion_compatible(ninf,ninf,nsup)
| ~ leq(ninf,nsup)
| ~ leq(ninf,ninf) ),
inference(instantiation,[status(thm)],[58]) ).
fof(h_inf_lb,plain,
! [X] : leq(ninf,X),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',h_inf_lb) ).
cnf(55,plain,
leq(ninf,X0),
inference(cnf,[status(esa)],[h_inf_lb]) ).
cnf(l1,plain,
leq(ninf,nsup),
inference(instantiation,[status(thm)],[55]) ).
fof(sharpness_compat,plain,
! [U,V,InfD,SupD] :
( ( leq(InfD,U)
& leq(U,SupD)
& less(U,V)
& leq(V,SupD) )
=> completion_compatible(U,InfD,SupD) ),
file('Axioms/MGT002+4.ax',sharpness_compat) ).
cnf(49,plain,
( ~ leq(X0,X1)
| ~ leq(X2,X1)
| ~ leq(X3,X0)
| ~ less(X0,X2)
| completion_compatible(X0,X3,X1) ),
inference(cnf,[status(esa)],[sharpness_compat]) ).
cnf(l2,plain,
( ~ leq(ninf,nsup)
| ~ leq(n0,nsup)
| ~ leq(ninf,ninf)
| ~ less(ninf,n0)
| completion_compatible(ninf,ninf,nsup) ),
inference(instantiation,[status(thm)],[49]) ).
fof(h_inf_0,plain,
less(ninf,n0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',h_inf_0) ).
cnf(53,plain,
less(ninf,n0),
inference(cnf,[status(esa)],[h_inf_0]) ).
cnf(l6,plain,
less(ninf,n0),
inference(instantiation,[status(thm)],[53]) ).
cnf(l5,plain,
leq(ninf,ninf),
inference(instantiation,[status(thm)],[55]) ).
fof(h_sup_ub,plain,
! [X] : leq(X,nsup),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',h_sup_ub) ).
cnf(56,plain,
leq(X0,nsup),
inference(cnf,[status(esa)],[h_sup_ub]) ).
cnf(l3,plain,
leq(ninf,nsup),
inference(instantiation,[status(thm)],[56]) ).
cnf(l8,plain,
leq(n0,nsup),
inference(instantiation,[status(thm)],[56]) ).
fof(leq_def,plain,
! [X,Y] :
( leq(X,Y)
<=> ( less(X,Y)
| X = Y ) ),
file('Axioms/MGT002+0.ax',leq_def) ).
cnf(5,plain,
( X0 != X1
| leq(X0,X1) ),
inference(cnf,[status(esa)],[leq_def]) ).
cnf(l4,plain,
( ninf != ninf
| leq(ninf,ninf) ),
inference(instantiation,[status(thm)],[5]) ).
cnf(final,plain,
$false,
inference(ground_refutation,[status(thm)],[l0,l1,l2,l6,l5,l3,l8,l4]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT070+1 : TPTP v9.3.0. Released v9.3.0.
% 0.00/0.04 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.11/0.36 % Computer : n018.cluster.edu
% 0.11/0.36 % Model : x86_64 x86_64
% 0.11/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.36 % Memory : 8046.5625MB
% 0.11/0.36 % OS : Linux 6.8.0-71-generic
% 0.11/0.36 % CPULimit : 300
% 0.11/0.36 % WCLimit : 300
% 0.11/0.36 % DateTime : Mon Sep 7 13:55:52 UTC 2026
% 0.11/0.36 % CPUTime :
% 0.11/0.37 % launching worker at depth: 1
% 0.11/0.37 % launching worker at depth: 4
% 0.11/0.37 % launching worker at depth: 8
% 0.11/0.37 % launching worker at depth: 3
% 0.11/0.37 % launching worker at depth: 5
% 0.11/0.37 % launching worker at depth: 6
% 0.11/0.37 % launching worker at depth: 2
% 0.11/0.37 % launching worker at depth: 7
% 0.11/0.37 % launching worker at depth: 9
% 0.11/0.37 % SZS status Theorem for theBenchmark
% 0.11/0.37 % SZS output start CNFRefutation
% See solution above
%------------------------------------------------------------------------------