%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : MGT068+1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% Computer : n029.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:03:04 AM UTC 2026
% Result : Theorem 93.25s 54.83s
% Output : CNFRefutation 93.25s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 23
% Syntax : Number of formulae : 105 ( 46 unt; 0 typ; 0 def)
% Number of atoms : 216 ( 17 equ)
% Maximal formula atoms : 7 ( 2 avg)
% Number of connectives : 195 ( 84 ~; 76 |; 20 &)
% ( 6 <=>; 9 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 4 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 19 ( 17 usr; 1 prp; 0-8 aty)
% Number of functors : 22 ( 22 usr; 17 con; 0-4 aty)
% Number of variables : 163 ( 159 !; 4 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ disjoint > prec > completion_conflict > axis_subsumes > axis_conflict > axis_compatible > in_ropen > in_open > in_lopen > in_closed > completion_compatible > upper_tag > lower_tag > less > leq > is_verdict > is_ep_type > box_verdict > #nlpp > unknown > o > nsup > ninf > n5 > n3 > n20 > n10 > n0 > lteq > lt > gteq > gt > eq > conflict > compatible > c > #skF_2 > #skF_4 > #skF_3 > #skF_1
%Foreground sorts:
%Background operators:
%Foreground operators:
tff(lower_tag,type,
lower_tag: ( $i * $i ) > $o ).
tff(is_verdict,type,
is_verdict: $i > $o ).
tff(axis_conflict,type,
axis_conflict: ( $i * $i * $i * $i ) > $o ).
tff(upper_tag,type,
upper_tag: ( $i * $i ) > $o ).
tff(in_lopen,type,
in_lopen: ( $i * $i * $i ) > $o ).
tff(lteq,type,
lteq: $i ).
tff(box_verdict,type,
box_verdict: ( $i * $i ) > $i ).
tff(unknown,type,
unknown: $i ).
tff(in_ropen,type,
in_ropen: ( $i * $i * $i ) > $o ).
tff(completion_compatible,type,
completion_compatible: ( $i * $i * $i ) > $o ).
tff(in_open,type,
in_open: ( $i * $i * $i ) > $o ).
tff(completion_conflict,type,
completion_conflict: ( $i * $i * $i * $i ) > $o ).
tff(ninf,type,
ninf: $i ).
tff(compatible,type,
compatible: $i ).
tff(n3,type,
n3: $i ).
tff(eq,type,
eq: $i ).
tff(less,type,
less: ( $i * $i ) > $o ).
tff('#skF_2',type,
'#skF_2': ( $i * $i * $i * $i ) > $i ).
tff(lt,type,
lt: $i ).
tff(n0,type,
n0: $i ).
tff(gteq,type,
gteq: $i ).
tff(in_closed,type,
in_closed: ( $i * $i * $i ) > $o ).
tff(disjoint,type,
disjoint: ( $i * $i * $i * $i * $i * $i * $i * $i ) > $o ).
tff(n10,type,
n10: $i ).
tff('#skF_4',type,
'#skF_4': ( $i * $i * $i * $i ) > $i ).
tff(axis_subsumes,type,
axis_subsumes: ( $i * $i * $i * $i ) > $o ).
tff(n20,type,
n20: $i ).
tff(leq,type,
leq: ( $i * $i ) > $o ).
tff(is_ep_type,type,
is_ep_type: $i > $o ).
tff(prec,type,
prec: ( $i * $i * $i * $i ) > $o ).
tff('#skF_3',type,
'#skF_3': ( $i * $i * $i * $i ) > $i ).
tff(nsup,type,
nsup: $i ).
tff(axis_compatible,type,
axis_compatible: ( $i * $i * $i * $i ) > $o ).
tff(n5,type,
n5: $i ).
tff('#skF_1',type,
'#skF_1': ( $i * $i ) > $i ).
tff(o,type,
o: $i ).
tff(conflict,type,
conflict: $i ).
tff(gt,type,
gt: $i ).
tff(c,type,
c: $i ).
tff(f_62,axiom,
! [X] : ~ less(X,X),
file('/export/starexec/sandbox2/benchmark/Axioms/MGT002+0.ax',irreflexive) ).
tff(f_502,hypothesis,
less(n5,n10),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',h_5_10) ).
tff(f_97,axiom,
! [X,Y] :
( less(X,Y)
=> leq(X,Y) ),
file('/export/starexec/sandbox2/benchmark/Axioms/MGT002+0.ax',less_implies_leq) ).
tff(f_92,axiom,
! [X,Y] :
( ( leq(X,Y)
& leq(Y,X) )
=> ( X = Y ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/MGT002+0.ax',leq_antisym) ).
tff(f_153,axiom,
! [X,Y] :
( less(X,Y)
=> ? [Z] :
( less(X,Z)
& less(Z,Y) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/MGT002+1.ax',dense) ).
tff(f_507,hypothesis,
! [X] : leq(ninf,X),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',h_inf_lb) ).
tff(f_509,hypothesis,
! [X] : leq(X,nsup),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',h_sup_ub) ).
tff(f_345,axiom,
! [V,InfD,SupD] :
( ( leq(InfD,V)
& leq(V,SupD) )
=> completion_compatible(V,InfD,SupD) ),
file('/export/starexec/sandbox2/benchmark/Axioms/MGT002+4.ax',completion_compat) ).
tff(f_384,axiom,
! [U,V,InfD,SupD] :
( ( leq(InfD,U)
& leq(U,SupD)
& less(U,V)
& leq(V,SupD) )
=> completion_conflict(U,V,InfD,SupD) ),
file('/export/starexec/sandbox2/benchmark/Axioms/MGT002+4.ax',sharpness_conflict) ).
tff(f_501,hypothesis,
less(n3,n5),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',h_3_5) ).
tff(f_69,axiom,
! [X,Y,Z] :
( ( less(X,Y)
& less(Y,Z) )
=> less(X,Z) ),
file('/export/starexec/sandbox2/benchmark/Axioms/MGT002+0.ax',transitive) ).
tff(f_226,axiom,
! [I1lo,I1hi,I2lo,I2hi] :
( axis_conflict(I1lo,I1hi,I2lo,I2hi)
<=> ~ ? [X] :
( in_closed(X,I1lo,I1hi)
& in_closed(X,I2lo,I2hi) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/MGT002+2.ax',axis_conflict_def) ).
tff(f_233,axiom,
! [I1lo,I1hi,I2lo,I2hi] :
( axis_compatible(I1lo,I1hi,I2lo,I2hi)
<=> ? [X] :
( in_closed(X,I1lo,I1hi)
& in_closed(X,I2lo,I2hi) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/MGT002+2.ax',axis_compatible_def) ).
tff(f_532,negated_conjecture,
~ ( axis_conflict(n0,n3,n10,n20)
& ? [Z] :
( less(n5,Z)
& less(Z,n10) )
& ~ disjoint(n5,nsup,o,c,ninf,n10,c,o)
& completion_conflict(n5,n10,ninf,nsup)
& completion_compatible(n5,ninf,nsup)
& ( box_verdict(conflict,unknown) = conflict ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hard_chain) ).
tff(f_199,axiom,
! [X,A,B] :
( in_closed(X,A,B)
<=> ( leq(A,X)
& leq(X,B) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/MGT002+2.ax',in_closed) ).
tff(f_116,axiom,
! [X,Y,Z] :
( ( leq(X,Y)
& leq(Y,Z) )
=> leq(X,Z) ),
file('/export/starexec/sandbox2/benchmark/Axioms/MGT002+0.ax',leq_trans) ).
tff(f_244,axiom,
is_verdict(unknown),
file('/export/starexec/sandbox2/benchmark/Axioms/MGT002+2.ax',unknown_is_verdict) ).
tff(f_242,axiom,
is_verdict(conflict),
file('/export/starexec/sandbox2/benchmark/Axioms/MGT002+2.ax',conflict_is_verdict) ).
tff(f_269,axiom,
! [V1,V2] :
( ( is_verdict(V1)
& is_verdict(V2)
& ( ( V1 = conflict )
| ( V2 = conflict ) ) )
=> ( box_verdict(V1,V2) = conflict ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/MGT002+2.ax',box_conflict) ).
tff(f_476,axiom,
! [L1,U1,CL1,CU1,L2,U2,CL2,CU2] :
( disjoint(L1,U1,CL1,CU1,L2,U2,CL2,CU2)
<=> ( prec(U1,L2,CU1,CL2)
| prec(U2,L1,CU2,CL1) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/MGT002+5.ax',disjoint_def) ).
tff(f_456,axiom,
! [U,L] :
( prec(U,L,c,c)
<=> less(U,L) ),
file('/export/starexec/sandbox2/benchmark/Axioms/MGT002+5.ax',prec_cc) ).
tff(f_110,axiom,
! [X,Y,Z] :
( ( less(X,Y)
& leq(Y,Z) )
=> less(X,Z) ),
file('/export/starexec/sandbox2/benchmark/Axioms/MGT002+0.ax',less_leq_trans) ).
tff(f_468,axiom,
! [U,L] :
( prec(U,L,o,o)
<=> leq(U,L) ),
file('/export/starexec/sandbox2/benchmark/Axioms/MGT002+5.ax',prec_oo) ).
tff(c_2,plain,
! [X_1] : ~ less(X_1,X_1),
inference(cnfTransformation,[status(thm)],[f_62]) ).
tff(c_162,plain,
less(n5,n10),
inference(cnfTransformation,[status(thm)],[f_502]) ).
tff(c_488758,plain,
! [X_111488,Y_111489] :
( leq(X_111488,Y_111489)
| ~ less(X_111488,Y_111489) ),
inference(cnfTransformation,[status(thm)],[f_97]) ).
tff(c_488772,plain,
leq(n5,n10),
inference(resolution,[status(thm)],[c_162,c_488758]) ).
tff(c_489975,plain,
! [Y_111646,X_111647] :
( ( Y_111646 = X_111647 )
| ~ leq(Y_111646,X_111647)
| ~ leq(X_111647,Y_111646) ),
inference(cnfTransformation,[status(thm)],[f_92]) ).
tff(c_489992,plain,
( ( n5 = n10 )
| ~ leq(n10,n5) ),
inference(resolution,[status(thm)],[c_488772,c_489975]) ).
tff(c_490026,plain,
~ leq(n10,n5),
inference(splitLeft,[status(thm)],[c_489992]) ).
tff(c_26,plain,
! [X_22,Y_23] :
( less(X_22,'#skF_1'(X_22,Y_23))
| ~ less(X_22,Y_23) ),
inference(cnfTransformation,[status(thm)],[f_153]) ).
tff(c_489866,plain,
! [X_111632,Y_111633] :
( less('#skF_1'(X_111632,Y_111633),Y_111633)
| ~ less(X_111632,Y_111633) ),
inference(cnfTransformation,[status(thm)],[f_153]) ).
tff(c_166,plain,
! [X_111] : leq(ninf,X_111),
inference(cnfTransformation,[status(thm)],[f_507]) ).
tff(c_168,plain,
! [X_112] : leq(X_112,nsup),
inference(cnfTransformation,[status(thm)],[f_509]) ).
tff(c_489654,plain,
! [V_111585,InfD_111586,SupD_111587] :
( completion_compatible(V_111585,InfD_111586,SupD_111587)
| ~ leq(V_111585,SupD_111587)
| ~ leq(InfD_111586,V_111585) ),
inference(cnfTransformation,[status(thm)],[f_345]) ).
tff(c_488736,plain,
! [U_111484,V_111485,InfD_111486,SupD_111487] :
( completion_conflict(U_111484,V_111485,InfD_111486,SupD_111487)
| ~ leq(V_111485,SupD_111487)
| ~ less(U_111484,V_111485)
| ~ leq(U_111484,SupD_111487)
| ~ leq(InfD_111486,U_111484) ),
inference(cnfTransformation,[status(thm)],[f_384]) ).
tff(c_160,plain,
less(n3,n5),
inference(cnfTransformation,[status(thm)],[f_501]) ).
tff(c_657,plain,
! [X_192,Z_193,Y_194] :
( less(X_192,Z_193)
| ~ less(Y_194,Z_193)
| ~ less(X_192,Y_194) ),
inference(cnfTransformation,[status(thm)],[f_69]) ).
tff(c_951,plain,
! [X_207] :
( less(X_207,n10)
| ~ less(X_207,n5) ),
inference(resolution,[status(thm)],[c_162,c_657]) ).
tff(c_992,plain,
less(n3,n10),
inference(resolution,[status(thm)],[c_160,c_951]) ).
tff(c_16,plain,
! [X_11,Y_12] :
( leq(X_11,Y_12)
| ~ less(X_11,Y_12) ),
inference(cnfTransformation,[status(thm)],[f_97]) ).
tff(c_1002,plain,
leq(n3,n10),
inference(resolution,[status(thm)],[c_992,c_16]) ).
tff(c_14,plain,
! [Y_10,X_9] :
( ( Y_10 = X_9 )
| ~ leq(Y_10,X_9)
| ~ leq(X_9,Y_10) ),
inference(cnfTransformation,[status(thm)],[f_92]) ).
tff(c_1020,plain,
( ( n3 = n10 )
| ~ leq(n10,n3) ),
inference(resolution,[status(thm)],[c_1002,c_14]) ).
tff(c_1040,plain,
~ leq(n10,n3),
inference(splitLeft,[status(thm)],[c_1020]) ).
tff(c_56,plain,
! [I1lo_37,I1hi_38,I2lo_39,I2hi_40] :
( in_closed('#skF_2'(I1lo_37,I1hi_38,I2lo_39,I2hi_40),I1lo_37,I1hi_38)
| axis_conflict(I1lo_37,I1hi_38,I2lo_39,I2hi_40) ),
inference(cnfTransformation,[status(thm)],[f_226]) ).
tff(c_54,plain,
! [I1lo_37,I1hi_38,I2lo_39,I2hi_40] :
( in_closed('#skF_2'(I1lo_37,I1hi_38,I2lo_39,I2hi_40),I2lo_39,I2hi_40)
| axis_conflict(I1lo_37,I1hi_38,I2lo_39,I2hi_40) ),
inference(cnfTransformation,[status(thm)],[f_226]) ).
tff(c_1709,plain,
! [I2hi_277,I2lo_273,I1lo_274,I1hi_275,X_276] :
( axis_compatible(I1lo_274,I1hi_275,I2lo_273,I2hi_277)
| ~ in_closed(X_276,I2lo_273,I2hi_277)
| ~ in_closed(X_276,I1lo_274,I1hi_275) ),
inference(cnfTransformation,[status(thm)],[f_233]) ).
tff(c_121862,plain,
! [I1hi_37313,I1lo_37312,I2lo_37315,I1hi_37316,I2hi_37317,I1lo_37314] :
( axis_compatible(I1lo_37314,I1hi_37316,I2lo_37315,I2hi_37317)
| ~ in_closed('#skF_2'(I1lo_37312,I1hi_37313,I2lo_37315,I2hi_37317),I1lo_37314,I1hi_37316)
| axis_conflict(I1lo_37312,I1hi_37313,I2lo_37315,I2hi_37317) ),
inference(resolution,[status(thm)],[c_54,c_1709]) ).
tff(c_233239,plain,
! [I1lo_64704,I1hi_64705,I2lo_64706,I2hi_64707] :
( axis_compatible(I1lo_64704,I1hi_64705,I2lo_64706,I2hi_64707)
| axis_conflict(I1lo_64704,I1hi_64705,I2lo_64706,I2hi_64707) ),
inference(resolution,[status(thm)],[c_56,c_121862]) ).
tff(c_170,plain,
! [Z_113] :
( ( box_verdict(conflict,unknown) != conflict )
| ~ completion_compatible(n5,ninf,nsup)
| ~ completion_conflict(n5,n10,ninf,nsup)
| disjoint(n5,nsup,o,c,ninf,n10,c,o)
| ~ less(Z_113,n10)
| ~ less(n5,Z_113)
| ~ axis_conflict(n0,n3,n10,n20) ),
inference(cnfTransformation,[status(thm)],[f_532]) ).
tff(c_183,plain,
~ axis_conflict(n0,n3,n10,n20),
inference(splitLeft,[status(thm)],[c_170]) ).
tff(c_233250,plain,
axis_compatible(n0,n3,n10,n20),
inference(resolution,[status(thm)],[c_233239,c_183]) ).
tff(c_1509,plain,
! [I1lo_258,I1hi_259,I2lo_260,I2hi_261] :
( in_closed('#skF_3'(I1lo_258,I1hi_259,I2lo_260,I2hi_261),I2lo_260,I2hi_261)
| ~ axis_compatible(I1lo_258,I1hi_259,I2lo_260,I2hi_261) ),
inference(cnfTransformation,[status(thm)],[f_233]) ).
tff(c_32,plain,
! [A_26,X_25,B_27] :
( leq(A_26,X_25)
| ~ in_closed(X_25,A_26,B_27) ),
inference(cnfTransformation,[status(thm)],[f_199]) ).
tff(c_1520,plain,
! [I2lo_260,I1lo_258,I1hi_259,I2hi_261] :
( leq(I2lo_260,'#skF_3'(I1lo_258,I1hi_259,I2lo_260,I2hi_261))
| ~ axis_compatible(I1lo_258,I1hi_259,I2lo_260,I2hi_261) ),
inference(resolution,[status(thm)],[c_1509,c_32]) ).
tff(c_1785,plain,
! [I1lo_280,I1hi_281,I2lo_282,I2hi_283] :
( in_closed('#skF_3'(I1lo_280,I1hi_281,I2lo_282,I2hi_283),I1lo_280,I1hi_281)
| ~ axis_compatible(I1lo_280,I1hi_281,I2lo_282,I2hi_283) ),
inference(cnfTransformation,[status(thm)],[f_233]) ).
tff(c_30,plain,
! [X_25,B_27,A_26] :
( leq(X_25,B_27)
| ~ in_closed(X_25,A_26,B_27) ),
inference(cnfTransformation,[status(thm)],[f_199]) ).
tff(c_76273,plain,
! [I1lo_26858,I1hi_26859,I2lo_26860,I2hi_26861] :
( leq('#skF_3'(I1lo_26858,I1hi_26859,I2lo_26860,I2hi_26861),I1hi_26859)
| ~ axis_compatible(I1lo_26858,I1hi_26859,I2lo_26860,I2hi_26861) ),
inference(resolution,[status(thm)],[c_1785,c_30]) ).
tff(c_22,plain,
! [X_19,Z_21,Y_20] :
( leq(X_19,Z_21)
| ~ leq(Y_20,Z_21)
| ~ leq(X_19,Y_20) ),
inference(cnfTransformation,[status(thm)],[f_116]) ).
tff(c_483174,plain,
! [I1hi_110503,I2lo_110506,X_110502,I2hi_110504,I1lo_110505] :
( leq(X_110502,I1hi_110503)
| ~ leq(X_110502,'#skF_3'(I1lo_110505,I1hi_110503,I2lo_110506,I2hi_110504))
| ~ axis_compatible(I1lo_110505,I1hi_110503,I2lo_110506,I2hi_110504) ),
inference(resolution,[status(thm)],[c_76273,c_22]) ).
tff(c_486855,plain,
! [I2lo_111151,I1hi_111152,I1lo_111153,I2hi_111154] :
( leq(I2lo_111151,I1hi_111152)
| ~ axis_compatible(I1lo_111153,I1hi_111152,I2lo_111151,I2hi_111154) ),
inference(resolution,[status(thm)],[c_1520,c_483174]) ).
tff(c_486918,plain,
leq(n10,n3),
inference(resolution,[status(thm)],[c_233250,c_486855]) ).
tff(c_486966,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_1040,c_486918]) ).
tff(c_486967,plain,
n3 = n10,
inference(splitRight,[status(thm)],[c_1020]) ).
tff(c_486970,plain,
less(n10,n10),
inference(demodulation,[status(thm),theory(equality)],[c_486967,c_992]) ).
tff(c_486986,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_2,c_486970]) ).
tff(c_486987,plain,
! [Z_113] :
( ~ completion_conflict(n5,n10,ninf,nsup)
| ~ completion_compatible(n5,ninf,nsup)
| ( box_verdict(conflict,unknown) != conflict )
| ~ less(Z_113,n10)
| ~ less(n5,Z_113)
| disjoint(n5,nsup,o,c,ninf,n10,c,o) ),
inference(splitRight,[status(thm)],[c_170]) ).
tff(c_486992,plain,
box_verdict(conflict,unknown) != conflict,
inference(splitLeft,[status(thm)],[c_486987]) ).
tff(c_74,plain,
is_verdict(unknown),
inference(cnfTransformation,[status(thm)],[f_244]) ).
tff(c_70,plain,
is_verdict(conflict),
inference(cnfTransformation,[status(thm)],[f_242]) ).
tff(c_86,plain,
! [V2_60] :
( ( box_verdict(conflict,V2_60) = conflict )
| ~ is_verdict(V2_60)
| ~ is_verdict(conflict) ),
inference(cnfTransformation,[status(thm)],[f_269]) ).
tff(c_487030,plain,
! [V2_111290] :
( ( box_verdict(conflict,V2_111290) = conflict )
| ~ is_verdict(V2_111290) ),
inference(demodulation,[status(thm),theory(equality)],[c_70,c_86]) ).
tff(c_487039,plain,
box_verdict(conflict,unknown) = conflict,
inference(resolution,[status(thm)],[c_74,c_487030]) ).
tff(c_487045,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_486992,c_487039]) ).
tff(c_487046,plain,
! [Z_113] :
( ~ completion_compatible(n5,ninf,nsup)
| ~ completion_conflict(n5,n10,ninf,nsup)
| ~ less(Z_113,n10)
| ~ less(n5,Z_113)
| disjoint(n5,nsup,o,c,ninf,n10,c,o) ),
inference(splitRight,[status(thm)],[c_486987]) ).
tff(c_487085,plain,
~ completion_conflict(n5,n10,ninf,nsup),
inference(splitLeft,[status(thm)],[c_487046]) ).
tff(c_488739,plain,
( ~ leq(n10,nsup)
| ~ less(n5,n10)
| ~ leq(n5,nsup)
| ~ leq(ninf,n5) ),
inference(resolution,[status(thm)],[c_488736,c_487085]) ).
tff(c_488743,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_166,c_168,c_162,c_168,c_488739]) ).
tff(c_488744,plain,
! [Z_113] :
( ~ completion_compatible(n5,ninf,nsup)
| ~ less(Z_113,n10)
| ~ less(n5,Z_113)
| disjoint(n5,nsup,o,c,ninf,n10,c,o) ),
inference(splitRight,[status(thm)],[c_487046]) ).
tff(c_488796,plain,
~ completion_compatible(n5,ninf,nsup),
inference(splitLeft,[status(thm)],[c_488744]) ).
tff(c_489657,plain,
( ~ leq(n5,nsup)
| ~ leq(ninf,n5) ),
inference(resolution,[status(thm)],[c_489654,c_488796]) ).
tff(c_489661,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_166,c_168,c_489657]) ).
tff(c_489662,plain,
! [Z_113] :
( ~ less(Z_113,n10)
| ~ less(n5,Z_113)
| disjoint(n5,nsup,o,c,ninf,n10,c,o) ),
inference(splitRight,[status(thm)],[c_488744]) ).
tff(c_489708,plain,
! [Z_113] :
( ~ less(Z_113,n10)
| ~ less(n5,Z_113) ),
inference(splitLeft,[status(thm)],[c_489662]) ).
tff(c_489906,plain,
! [X_111637] :
( ~ less(n5,'#skF_1'(X_111637,n10))
| ~ less(X_111637,n10) ),
inference(resolution,[status(thm)],[c_489866,c_489708]) ).
tff(c_489910,plain,
~ less(n5,n10),
inference(resolution,[status(thm)],[c_26,c_489906]) ).
tff(c_489916,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_162,c_489910]) ).
tff(c_489917,plain,
disjoint(n5,nsup,o,c,ninf,n10,c,o),
inference(splitRight,[status(thm)],[c_489662]) ).
tff(c_491583,plain,
! [CU2_111804,CU1_111811,L2_111806,CL1_111809,U2_111807,U1_111805,L1_111808,CL2_111810] :
( prec(U2_111807,L1_111808,CU2_111804,CL1_111809)
| prec(U1_111805,L2_111806,CU1_111811,CL2_111810)
| ~ disjoint(L1_111808,U1_111805,CL1_111809,CU1_111811,L2_111806,U2_111807,CL2_111810,CU2_111804) ),
inference(cnfTransformation,[status(thm)],[f_476]) ).
tff(c_491595,plain,
( prec(n10,n5,o,o)
| prec(nsup,ninf,c,c) ),
inference(resolution,[status(thm)],[c_489917,c_491583]) ).
tff(c_491743,plain,
prec(nsup,ninf,c,c),
inference(splitLeft,[status(thm)],[c_491595]) ).
tff(c_116,plain,
! [U_95,L_96] :
( less(U_95,L_96)
| ~ prec(U_95,L_96,c,c) ),
inference(cnfTransformation,[status(thm)],[f_456]) ).
tff(c_491747,plain,
less(nsup,ninf),
inference(resolution,[status(thm)],[c_491743,c_116]) ).
tff(c_490347,plain,
! [X_111682,Z_111683,Y_111684] :
( less(X_111682,Z_111683)
| ~ leq(Y_111684,Z_111683)
| ~ less(X_111682,Y_111684) ),
inference(cnfTransformation,[status(thm)],[f_110]) ).
tff(c_490372,plain,
! [X_111682,X_112] :
( less(X_111682,nsup)
| ~ less(X_111682,X_112) ),
inference(resolution,[status(thm)],[c_168,c_490347]) ).
tff(c_491749,plain,
less(nsup,nsup),
inference(resolution,[status(thm)],[c_491747,c_490372]) ).
tff(c_491762,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_2,c_491749]) ).
tff(c_491763,plain,
prec(n10,n5,o,o),
inference(splitRight,[status(thm)],[c_491595]) ).
tff(c_128,plain,
! [U_101,L_102] :
( leq(U_101,L_102)
| ~ prec(U_101,L_102,o,o) ),
inference(cnfTransformation,[status(thm)],[f_468]) ).
tff(c_491767,plain,
leq(n10,n5),
inference(resolution,[status(thm)],[c_491763,c_128]) ).
tff(c_491771,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_490026,c_491767]) ).
tff(c_491772,plain,
n5 = n10,
inference(splitRight,[status(thm)],[c_489992]) ).
tff(c_491779,plain,
less(n10,n10),
inference(demodulation,[status(thm),theory(equality)],[c_491772,c_162]) ).
tff(c_491783,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_2,c_491779]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT068+1 : TPTP v9.3.0. Released v9.3.0.
% 0.00/0.04 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% 0.10/0.36 % Computer : n029.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Mon Sep 7 13:54:27 UTC 2026
% 0.10/0.36 % CPUTime :
% 93.25/54.83 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 93.25/54.85
% 93.25/54.85 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------