%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : SWV033+1 : TPTP v9.0.0. Bugfixed v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% Computer : n026.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Apr 9 09:29:22 PM UTC 2025
% Result : Theorem 26.58s 11.01s
% Output : CNFRefutation 26.58s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 9
% Syntax : Number of formulae : 117 ( 62 unt; 0 typ; 0 def)
% Number of atoms : 214 ( 73 equ)
% Maximal formula atoms : 20 ( 1 avg)
% Number of connectives : 167 ( 70 ~; 73 |; 14 &)
% ( 1 <=>; 9 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 3 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 7 ( 5 usr; 2 prp; 0-2 aty)
% Number of functors : 62 ( 62 usr; 17 con; 0-8 aty)
% Number of variables : 52 ( 52 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ lt > leq > gt > geq > tptp_update3 > tptp_update2 > tptp_const_array2 > sum > a_select3 > uniform_int_rnd > tptp_msub > tptp_mmul > tptp_madd > tptp_const_array1 > plus > minus > dim > a_select2 > #nlpp > trans > succ > pred > inv > use > true > tptp_minus_1 > tptp_float_0_0 > simplex7_init > s_values7_init > pv1376 > n5 > n4 > n3 > n2 > n1 > n0 > init > def > #skF_13 > #skF_24 > #skF_17 > #skF_23 > #skF_6 > #skF_19 > #skF_27 > #skF_21 > #skF_25 > #skF_12 > #skF_18 > #skF_3 > #skF_26 > #skF_20 > #skF_11 > #skF_7 > #skF_9 > #skF_15 > #skF_22 > #skF_30 > #skF_14 > #skF_29 > #skF_28 > #skF_2 > #skF_8 > #skF_1 > #skF_5 > #skF_4 > #skF_16 > #skF_10
%Foreground sorts:
%Background operators:
%Foreground operators:
tff('#skF_13',type,
'#skF_13': ( $i * $i * $i ) > $i ).
tff('#skF_24',type,
'#skF_24': ( $i * $i * $i * $i * $i * $i * $i * $i ) > $i ).
tff(true,type,
true: $o ).
tff('#skF_17',type,
'#skF_17': ( $i * $i * $i * $i ) > $i ).
tff(tptp_const_array2,type,
tptp_const_array2: ( $i * $i * $i ) > $i ).
tff('#skF_23',type,
'#skF_23': ( $i * $i * $i * $i * $i * $i * $i * $i ) > $i ).
tff('#skF_6',type,
'#skF_6': ( $i * $i ) > $i ).
tff(tptp_minus_1,type,
tptp_minus_1: $i ).
tff('#skF_19',type,
'#skF_19': ( $i * $i * $i * $i * $i * $i * $i * $i ) > $i ).
tff('#skF_27',type,
'#skF_27': ( $i * $i * $i * $i ) > $i ).
tff('#skF_21',type,
'#skF_21': ( $i * $i * $i * $i * $i * $i * $i * $i ) > $i ).
tff('#skF_25',type,
'#skF_25': ( $i * $i * $i * $i * $i * $i ) > $i ).
tff('#skF_12',type,
'#skF_12': ( $i * $i * $i ) > $i ).
tff('#skF_18',type,
'#skF_18': ( $i * $i * $i * $i ) > $i ).
tff(a_select3,type,
a_select3: ( $i * $i * $i ) > $i ).
tff(tptp_float_0_0,type,
tptp_float_0_0: $i ).
tff(a_select2,type,
a_select2: ( $i * $i ) > $i ).
tff('#skF_3',type,
'#skF_3': ( $i * $i ) > $i ).
tff(trans,type,
trans: $i > $i ).
tff(tptp_update3,type,
tptp_update3: ( $i * $i * $i * $i ) > $i ).
tff(n3,type,
n3: $i ).
tff('#skF_26',type,
'#skF_26': ( $i * $i * $i * $i * $i * $i ) > $i ).
tff(use,type,
use: $i ).
tff(inv,type,
inv: $i > $i ).
tff(n1,type,
n1: $i ).
tff(tptp_madd,type,
tptp_madd: ( $i * $i ) > $i ).
tff(plus,type,
plus: ( $i * $i ) > $i ).
tff('#skF_20',type,
'#skF_20': ( $i * $i * $i * $i * $i * $i * $i * $i ) > $i ).
tff(n0,type,
n0: $i ).
tff(s_values7_init,type,
s_values7_init: $i ).
tff(pv1376,type,
pv1376: $i ).
tff('#skF_11',type,
'#skF_11': ( $i * $i * $i ) > $i ).
tff(tptp_update2,type,
tptp_update2: ( $i * $i * $i ) > $i ).
tff(gt,type,
gt: ( $i * $i ) > $o ).
tff('#skF_7',type,
'#skF_7': ( $i * $i * $i ) > $i ).
tff(n4,type,
n4: $i ).
tff(tptp_msub,type,
tptp_msub: ( $i * $i ) > $i ).
tff('#skF_9',type,
'#skF_9': ( $i * $i * $i ) > $i ).
tff(tptp_const_array1,type,
tptp_const_array1: ( $i * $i ) > $i ).
tff('#skF_15',type,
'#skF_15': ( $i * $i * $i ) > $i ).
tff('#skF_22',type,
'#skF_22': ( $i * $i * $i * $i * $i * $i * $i * $i ) > $i ).
tff('#skF_30',type,
'#skF_30': $i ).
tff('#skF_14',type,
'#skF_14': ( $i * $i * $i ) > $i ).
tff(tptp_mmul,type,
tptp_mmul: ( $i * $i ) > $i ).
tff(init,type,
init: $i ).
tff(uniform_int_rnd,type,
uniform_int_rnd: ( $i * $i ) > $i ).
tff(geq,type,
geq: ( $i * $i ) > $o ).
tff(leq,type,
leq: ( $i * $i ) > $o ).
tff('#skF_29',type,
'#skF_29': $i ).
tff('#skF_28',type,
'#skF_28': $i ).
tff(lt,type,
lt: ( $i * $i ) > $o ).
tff('#skF_2',type,
'#skF_2': ( $i * $i ) > $i ).
tff(simplex7_init,type,
simplex7_init: $i ).
tff(def,type,
def: $i ).
tff('#skF_8',type,
'#skF_8': ( $i * $i * $i ) > $i ).
tff(n2,type,
n2: $i ).
tff(n5,type,
n5: $i ).
tff('#skF_1',type,
'#skF_1': ( $i * $i ) > $i ).
tff(succ,type,
succ: $i > $i ).
tff(pred,type,
pred: $i > $i ).
tff(sum,type,
sum: ( $i * $i * $i ) > $i ).
tff('#skF_5',type,
'#skF_5': ( $i * $i ) > $i ).
tff('#skF_4',type,
'#skF_4': ( $i * $i ) > $i ).
tff('#skF_16',type,
'#skF_16': ( $i * $i * $i ) > $i ).
tff('#skF_10',type,
'#skF_10': ( $i * $i * $i ) > $i ).
tff(dim,type,
dim: ( $i * $i ) > $i ).
tff(minus,type,
minus: ( $i * $i ) > $i ).
tff(f_526,negated_conjecture,
~ ( ( ( init = init )
& leq(n0,pv1376)
& leq(pv1376,n3)
& ! [A] :
( ( leq(n0,A)
& leq(A,n2) )
=> ! [B] :
( ( leq(n0,B)
& leq(B,n3) )
=> ( a_select3(simplex7_init,B,A) = init ) ) )
& ! [C] :
( ( leq(n0,C)
& leq(C,minus(pv1376,n1)) )
=> ( a_select2(s_values7_init,C) = init ) ) )
=> ( ( init = init )
& ! [D] :
( ( leq(n0,D)
& leq(D,n2) )
=> ! [E] :
( ( leq(n0,E)
& leq(E,n3) )
=> ( a_select3(simplex7_init,E,D) = init ) ) )
& ! [F] :
( ( leq(n0,F)
& leq(F,minus(plus(n1,pv1376),n1)) )
=> ( a_select2(tptp_update2(s_values7_init,pv1376,init),F) = init ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gauss_init_0045) ).
tff(f_71,axiom,
! [X] : ~ gt(X,X),
file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax',irreflexivity_gt) ).
tff(f_453,axiom,
! [X,U,VAL] : ( a_select2(tptp_update2(X,U,VAL),U) = VAL ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax',sel2_update_1) ).
tff(f_106,axiom,
! [X,Y] :
( leq(X,pred(Y))
<=> gt(Y,X) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax',leq_gt_pred) ).
tff(f_400,axiom,
! [X] : ( minus(X,n1) = pred(X) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax',pred_minus_1) ).
tff(f_402,axiom,
! [X] : ( pred(succ(X)) = X ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax',pred_succ) ).
tff(f_382,axiom,
! [X] : ( plus(n1,X) = succ(X) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax',succ_plus_1_l) ).
tff(f_101,axiom,
! [X,Y] :
( ( leq(X,Y)
& ( X != Y ) )
=> gt(Y,X) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax',leq_gt2) ).
tff(f_460,axiom,
! [I,U,X,VAL,VAL2] :
( ( ( I != U )
& ( a_select2(X,U) = VAL ) )
=> ( a_select2(tptp_update2(X,I,VAL2),U) = VAL ) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax',sel2_update_2) ).
tff(c_523,plain,
( ( a_select3(simplex7_init,'#skF_29','#skF_28') != init )
| ( a_select2(tptp_update2(s_values7_init,pv1376,init),'#skF_30') != init ) ),
inference(cnfTransformation,[status(thm)],[f_526]) ).
tff(c_31232,plain,
a_select2(tptp_update2(s_values7_init,pv1376,init),'#skF_30') != init,
inference(splitLeft,[status(thm)],[c_523]) ).
tff(c_527,plain,
( leq(n0,'#skF_29')
| ( a_select2(tptp_update2(s_values7_init,pv1376,init),'#skF_30') != init ) ),
inference(cnfTransformation,[status(thm)],[f_526]) ).
tff(c_28565,plain,
a_select2(tptp_update2(s_values7_init,pv1376,init),'#skF_30') != init,
inference(splitLeft,[status(thm)],[c_527]) ).
tff(c_525,plain,
( leq('#skF_29',n3)
| ( a_select2(tptp_update2(s_values7_init,pv1376,init),'#skF_30') != init ) ),
inference(cnfTransformation,[status(thm)],[f_526]) ).
tff(c_26817,plain,
a_select2(tptp_update2(s_values7_init,pv1376,init),'#skF_30') != init,
inference(splitLeft,[status(thm)],[c_525]) ).
tff(c_529,plain,
( leq('#skF_28',n2)
| ( a_select2(tptp_update2(s_values7_init,pv1376,init),'#skF_30') != init ) ),
inference(cnfTransformation,[status(thm)],[f_526]) ).
tff(c_1071,plain,
a_select2(tptp_update2(s_values7_init,pv1376,init),'#skF_30') != init,
inference(splitLeft,[status(thm)],[c_529]) ).
tff(c_531,plain,
( leq(n0,'#skF_28')
| ( a_select2(tptp_update2(s_values7_init,pv1376,init),'#skF_30') != init ) ),
inference(cnfTransformation,[status(thm)],[f_526]) ).
tff(c_1373,plain,
a_select2(tptp_update2(s_values7_init,pv1376,init),'#skF_30') != init,
inference(splitLeft,[status(thm)],[c_531]) ).
tff(c_6,plain,
! [X_6] : ~ gt(X_6,X_6),
inference(cnfTransformation,[status(thm)],[f_71]) ).
tff(c_498,plain,
! [X_168,U_169,VAL_170] : ( a_select2(tptp_update2(X_168,U_169,VAL_170),U_169) = VAL_170 ),
inference(cnfTransformation,[status(thm)],[f_453]) ).
tff(c_545,plain,
( leq('#skF_29',n3)
| leq(n0,'#skF_30') ),
inference(cnfTransformation,[status(thm)],[f_526]) ).
tff(c_670,plain,
leq(n0,'#skF_30'),
inference(splitLeft,[status(thm)],[c_545]) ).
tff(c_26,plain,
! [X_19,Y_20] :
( leq(X_19,pred(Y_20))
| ~ gt(Y_20,X_19) ),
inference(cnfTransformation,[status(thm)],[f_106]) ).
tff(c_470,plain,
! [X_140] : ( minus(X_140,n1) = pred(X_140) ),
inference(cnfTransformation,[status(thm)],[f_400]) ).
tff(c_512,plain,
! [C_184] :
( ( a_select2(s_values7_init,C_184) = init )
| ~ leq(C_184,minus(pv1376,n1))
| ~ leq(n0,C_184) ),
inference(cnfTransformation,[status(thm)],[f_526]) ).
tff(c_2687,plain,
! [C_262] :
( ( a_select2(s_values7_init,C_262) = init )
| ~ leq(C_262,pred(pv1376))
| ~ leq(n0,C_262) ),
inference(demodulation,[status(thm),theory(equality)],[c_470,c_512]) ).
tff(c_22958,plain,
! [X_722] :
( ( a_select2(s_values7_init,X_722) = init )
| ~ leq(n0,X_722)
| ~ gt(pv1376,X_722) ),
inference(resolution,[status(thm)],[c_26,c_2687]) ).
tff(c_23072,plain,
( ( a_select2(s_values7_init,'#skF_30') = init )
| ~ gt(pv1376,'#skF_30') ),
inference(resolution,[status(thm)],[c_670,c_22958]) ).
tff(c_23362,plain,
~ gt(pv1376,'#skF_30'),
inference(splitLeft,[status(thm)],[c_23072]) ).
tff(c_472,plain,
! [X_141] : ( pred(succ(X_141)) = X_141 ),
inference(cnfTransformation,[status(thm)],[f_402]) ).
tff(c_452,plain,
! [X_131] : ( plus(n1,X_131) = succ(X_131) ),
inference(cnfTransformation,[status(thm)],[f_382]) ).
tff(c_539,plain,
( leq('#skF_28',n2)
| leq('#skF_30',minus(plus(n1,pv1376),n1)) ),
inference(cnfTransformation,[status(thm)],[f_526]) ).
tff(c_623,plain,
( leq('#skF_28',n2)
| leq('#skF_30',pred(plus(n1,pv1376))) ),
inference(demodulation,[status(thm),theory(equality)],[c_470,c_539]) ).
tff(c_635,plain,
( leq('#skF_28',n2)
| leq('#skF_30',pred(succ(pv1376))) ),
inference(demodulation,[status(thm),theory(equality)],[c_452,c_623]) ).
tff(c_640,plain,
( leq('#skF_28',n2)
| leq('#skF_30',pv1376) ),
inference(demodulation,[status(thm),theory(equality)],[c_472,c_635]) ).
tff(c_870,plain,
leq('#skF_30',pv1376),
inference(splitLeft,[status(thm)],[c_640]) ).
tff(c_23443,plain,
! [Y_728,X_729] :
( gt(Y_728,X_729)
| ( Y_728 = X_729 )
| ~ leq(X_729,Y_728) ),
inference(cnfTransformation,[status(thm)],[f_101]) ).
tff(c_23512,plain,
( gt(pv1376,'#skF_30')
| ( pv1376 = '#skF_30' ) ),
inference(resolution,[status(thm)],[c_870,c_23443]) ).
tff(c_23551,plain,
pv1376 = '#skF_30',
inference(negUnitSimplification,[status(thm)],[c_23362,c_23512]) ).
tff(c_1562,plain,
a_select2(tptp_update2(s_values7_init,pv1376,init),'#skF_30') != init,
inference(splitLeft,[status(thm)],[c_523]) ).
tff(c_23573,plain,
a_select2(tptp_update2(s_values7_init,'#skF_30',init),'#skF_30') != init,
inference(demodulation,[status(thm),theory(equality)],[c_23551,c_1562]) ).
tff(c_23582,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_498,c_23573]) ).
tff(c_23583,plain,
a_select2(s_values7_init,'#skF_30') = init,
inference(splitRight,[status(thm)],[c_23072]) ).
tff(c_24637,plain,
! [X_752,I_753,VAL2_754,U_755] :
( ( a_select2(tptp_update2(X_752,I_753,VAL2_754),U_755) = a_select2(X_752,U_755) )
| ( U_755 = I_753 ) ),
inference(cnfTransformation,[status(thm)],[f_460]) ).
tff(c_24643,plain,
( ( a_select2(s_values7_init,'#skF_30') != init )
| ( pv1376 = '#skF_30' ) ),
inference(superposition,[status(thm),theory(equality)],[c_24637,c_1562]) ).
tff(c_24656,plain,
pv1376 = '#skF_30',
inference(demodulation,[status(thm),theory(equality)],[c_23583,c_24643]) ).
tff(c_23584,plain,
gt(pv1376,'#skF_30'),
inference(splitRight,[status(thm)],[c_23072]) ).
tff(c_24667,plain,
gt('#skF_30','#skF_30'),
inference(demodulation,[status(thm),theory(equality)],[c_24656,c_23584]) ).
tff(c_24680,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_6,c_24667]) ).
tff(c_24682,plain,
a_select2(tptp_update2(s_values7_init,pv1376,init),'#skF_30') = init,
inference(splitRight,[status(thm)],[c_523]) ).
tff(c_25702,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_1373,c_24682]) ).
tff(c_25704,plain,
a_select2(tptp_update2(s_values7_init,pv1376,init),'#skF_30') = init,
inference(splitRight,[status(thm)],[c_531]) ).
tff(c_26699,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_1071,c_25704]) ).
tff(c_26701,plain,
a_select2(tptp_update2(s_values7_init,pv1376,init),'#skF_30') = init,
inference(splitRight,[status(thm)],[c_529]) ).
tff(c_28520,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_26817,c_26701]) ).
tff(c_28522,plain,
a_select2(tptp_update2(s_values7_init,pv1376,init),'#skF_30') = init,
inference(splitRight,[status(thm)],[c_525]) ).
tff(c_29786,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_28565,c_28522]) ).
tff(c_29788,plain,
a_select2(tptp_update2(s_values7_init,pv1376,init),'#skF_30') = init,
inference(splitRight,[status(thm)],[c_527]) ).
tff(c_32110,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_31232,c_29788]) ).
tff(c_32111,plain,
a_select3(simplex7_init,'#skF_29','#skF_28') != init,
inference(splitRight,[status(thm)],[c_523]) ).
tff(c_29842,plain,
a_select2(tptp_update2(s_values7_init,pv1376,init),'#skF_30') != init,
inference(splitLeft,[status(thm)],[c_531]) ).
tff(c_31195,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_29842,c_26701]) ).
tff(c_31196,plain,
leq(n0,'#skF_28'),
inference(splitRight,[status(thm)],[c_531]) ).
tff(c_26700,plain,
leq('#skF_28',n2),
inference(splitRight,[status(thm)],[c_529]) ).
tff(c_29787,plain,
leq(n0,'#skF_29'),
inference(splitRight,[status(thm)],[c_527]) ).
tff(c_28521,plain,
leq('#skF_29',n3),
inference(splitRight,[status(thm)],[c_525]) ).
tff(c_32236,plain,
! [B_958,A_959] :
( ( a_select3(simplex7_init,B_958,A_959) = init )
| ~ leq(B_958,n3)
| ~ leq(n0,B_958)
| ~ leq(A_959,n2)
| ~ leq(n0,A_959) ),
inference(cnfTransformation,[status(thm)],[f_526]) ).
tff(c_32238,plain,
! [A_959] :
( ( a_select3(simplex7_init,'#skF_29',A_959) = init )
| ~ leq(n0,'#skF_29')
| ~ leq(A_959,n2)
| ~ leq(n0,A_959) ),
inference(resolution,[status(thm)],[c_28521,c_32236]) ).
tff(c_45134,plain,
! [A_1337] :
( ( a_select3(simplex7_init,'#skF_29',A_1337) = init )
| ~ leq(A_1337,n2)
| ~ leq(n0,A_1337) ),
inference(demodulation,[status(thm),theory(equality)],[c_29787,c_32238]) ).
tff(c_45146,plain,
( ( a_select3(simplex7_init,'#skF_29','#skF_28') = init )
| ~ leq(n0,'#skF_28') ),
inference(resolution,[status(thm)],[c_26700,c_45134]) ).
tff(c_45166,plain,
a_select3(simplex7_init,'#skF_29','#skF_28') = init,
inference(demodulation,[status(thm),theory(equality)],[c_31196,c_45146]) ).
tff(c_45168,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_32111,c_45166]) ).
tff(c_45170,plain,
~ leq('#skF_30',pv1376),
inference(splitRight,[status(thm)],[c_640]) ).
tff(c_533,plain,
( ( a_select3(simplex7_init,'#skF_29','#skF_28') != init )
| leq('#skF_30',minus(plus(n1,pv1376),n1)) ),
inference(cnfTransformation,[status(thm)],[f_526]) ).
tff(c_625,plain,
( ( a_select3(simplex7_init,'#skF_29','#skF_28') != init )
| leq('#skF_30',pred(plus(n1,pv1376))) ),
inference(demodulation,[status(thm),theory(equality)],[c_470,c_533]) ).
tff(c_637,plain,
( ( a_select3(simplex7_init,'#skF_29','#skF_28') != init )
| leq('#skF_30',pred(succ(pv1376))) ),
inference(demodulation,[status(thm),theory(equality)],[c_452,c_625]) ).
tff(c_642,plain,
( ( a_select3(simplex7_init,'#skF_29','#skF_28') != init )
| leq('#skF_30',pv1376) ),
inference(demodulation,[status(thm),theory(equality)],[c_472,c_637]) ).
tff(c_56429,plain,
a_select3(simplex7_init,'#skF_29','#skF_28') != init,
inference(negUnitSimplification,[status(thm)],[c_45170,c_642]) ).
tff(c_541,plain,
( leq(n0,'#skF_28')
| leq('#skF_30',minus(plus(n1,pv1376),n1)) ),
inference(cnfTransformation,[status(thm)],[f_526]) ).
tff(c_622,plain,
( leq(n0,'#skF_28')
| leq('#skF_30',pred(plus(n1,pv1376))) ),
inference(demodulation,[status(thm),theory(equality)],[c_470,c_541]) ).
tff(c_634,plain,
( leq(n0,'#skF_28')
| leq('#skF_30',pred(succ(pv1376))) ),
inference(demodulation,[status(thm),theory(equality)],[c_452,c_622]) ).
tff(c_639,plain,
( leq(n0,'#skF_28')
| leq('#skF_30',pv1376) ),
inference(demodulation,[status(thm),theory(equality)],[c_472,c_634]) ).
tff(c_45372,plain,
leq(n0,'#skF_28'),
inference(negUnitSimplification,[status(thm)],[c_45170,c_639]) ).
tff(c_45169,plain,
leq('#skF_28',n2),
inference(splitRight,[status(thm)],[c_640]) ).
tff(c_537,plain,
( leq(n0,'#skF_29')
| leq('#skF_30',minus(plus(n1,pv1376),n1)) ),
inference(cnfTransformation,[status(thm)],[f_526]) ).
tff(c_621,plain,
( leq(n0,'#skF_29')
| leq('#skF_30',pred(plus(n1,pv1376))) ),
inference(demodulation,[status(thm),theory(equality)],[c_470,c_537]) ).
tff(c_633,plain,
( leq(n0,'#skF_29')
| leq('#skF_30',pred(succ(pv1376))) ),
inference(demodulation,[status(thm),theory(equality)],[c_452,c_621]) ).
tff(c_638,plain,
( leq(n0,'#skF_29')
| leq('#skF_30',pv1376) ),
inference(demodulation,[status(thm),theory(equality)],[c_472,c_633]) ).
tff(c_45350,plain,
leq(n0,'#skF_29'),
inference(negUnitSimplification,[status(thm)],[c_45170,c_638]) ).
tff(c_535,plain,
( leq('#skF_29',n3)
| leq('#skF_30',minus(plus(n1,pv1376),n1)) ),
inference(cnfTransformation,[status(thm)],[f_526]) ).
tff(c_624,plain,
( leq('#skF_29',n3)
| leq('#skF_30',pred(plus(n1,pv1376))) ),
inference(demodulation,[status(thm),theory(equality)],[c_470,c_535]) ).
tff(c_636,plain,
( leq('#skF_29',n3)
| leq('#skF_30',pred(succ(pv1376))) ),
inference(demodulation,[status(thm),theory(equality)],[c_452,c_624]) ).
tff(c_641,plain,
( leq('#skF_29',n3)
| leq('#skF_30',pv1376) ),
inference(demodulation,[status(thm),theory(equality)],[c_472,c_636]) ).
tff(c_45286,plain,
leq('#skF_29',n3),
inference(negUnitSimplification,[status(thm)],[c_45170,c_641]) ).
tff(c_46201,plain,
! [B_1368,A_1369] :
( ( a_select3(simplex7_init,B_1368,A_1369) = init )
| ~ leq(B_1368,n3)
| ~ leq(n0,B_1368)
| ~ leq(A_1369,n2)
| ~ leq(n0,A_1369) ),
inference(cnfTransformation,[status(thm)],[f_526]) ).
tff(c_46203,plain,
! [A_1369] :
( ( a_select3(simplex7_init,'#skF_29',A_1369) = init )
| ~ leq(n0,'#skF_29')
| ~ leq(A_1369,n2)
| ~ leq(n0,A_1369) ),
inference(resolution,[status(thm)],[c_45286,c_46201]) ).
tff(c_61626,plain,
! [A_1758] :
( ( a_select3(simplex7_init,'#skF_29',A_1758) = init )
| ~ leq(A_1758,n2)
| ~ leq(n0,A_1758) ),
inference(demodulation,[status(thm),theory(equality)],[c_45350,c_46203]) ).
tff(c_61639,plain,
( ( a_select3(simplex7_init,'#skF_29','#skF_28') = init )
| ~ leq(n0,'#skF_28') ),
inference(resolution,[status(thm)],[c_45169,c_61626]) ).
tff(c_61649,plain,
a_select3(simplex7_init,'#skF_29','#skF_28') = init,
inference(demodulation,[status(thm),theory(equality)],[c_45372,c_61639]) ).
tff(c_61651,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_56429,c_61649]) ).
tff(c_61653,plain,
~ leq(n0,'#skF_30'),
inference(splitRight,[status(thm)],[c_545]) ).
tff(c_543,plain,
( ( a_select3(simplex7_init,'#skF_29','#skF_28') != init )
| leq(n0,'#skF_30') ),
inference(cnfTransformation,[status(thm)],[f_526]) ).
tff(c_61958,plain,
a_select3(simplex7_init,'#skF_29','#skF_28') != init,
inference(negUnitSimplification,[status(thm)],[c_61653,c_543]) ).
tff(c_551,plain,
( leq(n0,'#skF_28')
| leq(n0,'#skF_30') ),
inference(cnfTransformation,[status(thm)],[f_526]) ).
tff(c_61888,plain,
leq(n0,'#skF_28'),
inference(negUnitSimplification,[status(thm)],[c_61653,c_551]) ).
tff(c_549,plain,
( leq('#skF_28',n2)
| leq(n0,'#skF_30') ),
inference(cnfTransformation,[status(thm)],[f_526]) ).
tff(c_61695,plain,
leq('#skF_28',n2),
inference(negUnitSimplification,[status(thm)],[c_61653,c_549]) ).
tff(c_547,plain,
( leq(n0,'#skF_29')
| leq(n0,'#skF_30') ),
inference(cnfTransformation,[status(thm)],[f_526]) ).
tff(c_61817,plain,
leq(n0,'#skF_29'),
inference(negUnitSimplification,[status(thm)],[c_61653,c_547]) ).
tff(c_61652,plain,
leq('#skF_29',n3),
inference(splitRight,[status(thm)],[c_545]) ).
tff(c_62828,plain,
! [B_1797,A_1798] :
( ( a_select3(simplex7_init,B_1797,A_1798) = init )
| ~ leq(B_1797,n3)
| ~ leq(n0,B_1797)
| ~ leq(A_1798,n2)
| ~ leq(n0,A_1798) ),
inference(cnfTransformation,[status(thm)],[f_526]) ).
tff(c_62836,plain,
! [A_1798] :
( ( a_select3(simplex7_init,'#skF_29',A_1798) = init )
| ~ leq(n0,'#skF_29')
| ~ leq(A_1798,n2)
| ~ leq(n0,A_1798) ),
inference(resolution,[status(thm)],[c_61652,c_62828]) ).
tff(c_65282,plain,
! [A_1855] :
( ( a_select3(simplex7_init,'#skF_29',A_1855) = init )
| ~ leq(A_1855,n2)
| ~ leq(n0,A_1855) ),
inference(demodulation,[status(thm),theory(equality)],[c_61817,c_62836]) ).
tff(c_65290,plain,
( ( a_select3(simplex7_init,'#skF_29','#skF_28') = init )
| ~ leq(n0,'#skF_28') ),
inference(resolution,[status(thm)],[c_61695,c_65282]) ).
tff(c_65298,plain,
a_select3(simplex7_init,'#skF_29','#skF_28') = init,
inference(demodulation,[status(thm),theory(equality)],[c_61888,c_65290]) ).
tff(c_65300,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_61958,c_65298]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12 % Problem : SWV033+1 : TPTP v9.0.0. Bugfixed v3.3.0.
% 0.06/0.13 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% 0.13/0.33 % Computer : n026.cluster.edu
% 0.13/0.33 % Model : x86_64 x86_64
% 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.33 % Memory : 8042.1875MB
% 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Wed Apr 9 02:38:38 EDT 2025
% 0.13/0.34 % CPUTime :
% 26.58/11.01 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 26.58/11.02
% 26.58/11.02 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------