%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : SWV089+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/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 : n005.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:30 PM UTC 2025
% Result : Theorem 15.03s 4.57s
% Output : CNFRefutation 15.03s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 16
% Syntax : Number of formulae : 118 ( 82 unt; 0 typ; 0 def)
% Number of atoms : 172 ( 107 equ)
% Maximal formula atoms : 7 ( 1 avg)
% Number of connectives : 130 ( 76 ~; 40 |; 8 &)
% ( 2 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 3 avg)
% Maximal term depth : 8 ( 2 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 : 57 ( 57 usr; 12 con; 0-8 aty)
% Number of variables : 101 ( 101 !; 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 > xinit_defuse > use > u_defuse > true > tptp_minus_1 > tptp_float_0_0 > n5 > n4 > n3 > n2 > n1 > n0 > 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_14 > #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(xinit_defuse,type,
xinit_defuse: $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('#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_14',type,
'#skF_14': ( $i * $i * $i ) > $i ).
tff(tptp_mmul,type,
tptp_mmul: ( $i * $i ) > $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(lt,type,
lt: ( $i * $i ) > $o ).
tff('#skF_2',type,
'#skF_2': ( $i * $i ) > $i ).
tff(def,type,
def: $i ).
tff('#skF_8',type,
'#skF_8': ( $i * $i * $i ) > $i ).
tff(u_defuse,type,
u_defuse: $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_74,axiom,
! [X] : leq(X,X),
file('/export/starexec/sandbox2/benchmark/Axioms/SWV003+0.ax',reflexivity_leq) ).
tff(f_89,axiom,
! [X,Y] :
( geq(X,Y)
<=> leq(Y,X) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWV003+0.ax',leq_geq) ).
tff(f_453,axiom,
! [X,U,VAL] : ( a_select2(tptp_update2(X,U,VAL),U) = VAL ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWV003+0.ax',sel2_update_1) ).
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/sandbox2/benchmark/Axioms/SWV003+0.ax',sel2_update_2) ).
tff(f_421,axiom,
! [X,U,V,VAL] : ( a_select3(tptp_update3(X,U,V,VAL),U,V) = VAL ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWV003+0.ax',sel3_update_1) ).
tff(f_430,axiom,
! [I,J,U,V,X,VAL,VAL2] :
( ( ( I != U )
& ( J = V )
& ( a_select3(X,U,V) = VAL ) )
=> ( a_select3(tptp_update3(X,I,J,VAL2),U,V) = VAL ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWV003+0.ax',sel3_update_2) ).
tff(f_586,axiom,
succ(succ(n0)) = n2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',successor_2) ).
tff(f_587,axiom,
succ(succ(succ(n0))) = n3,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',successor_3) ).
tff(f_585,axiom,
succ(n0) = n1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',successor_1) ).
tff(f_583,axiom,
succ(succ(succ(succ(n0)))) = n4,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',successor_4) ).
tff(f_494,negated_conjecture,
~ ( true
=> ( ( a_select3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(u_defuse,n2,n0,use),n1,n0,use),n2,n0,use),n0,n0,use),n1,n0,use),n0,n0,use),n0,n0) = use )
& ( a_select3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(u_defuse,n2,n0,use),n1,n0,use),n2,n0,use),n0,n0,use),n1,n0,use),n0,n0,use),n1,n0) = use )
& ( a_select3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(u_defuse,n2,n0,use),n1,n0,use),n2,n0,use),n0,n0,use),n1,n0,use),n0,n0,use),n2,n0) = use )
& ( a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse,n5,use),n4,use),n5,use),n3,use),n4,use),n3,use),n3) = use )
& ( a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse,n5,use),n4,use),n5,use),n3,use),n4,use),n3,use),n4) = use )
& ( a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse,n5,use),n4,use),n5,use),n3,use),n4,use),n3,use),n5) = use ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',quaternion_ds1_inuse_0001) ).
tff(f_116,axiom,
! [X,Y] :
( leq(X,Y)
<=> gt(succ(Y),X) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWV003+0.ax',leq_succ_gt_equiv) ).
tff(f_71,axiom,
! [X] : ~ gt(X,X),
file('/export/starexec/sandbox2/benchmark/Axioms/SWV003+0.ax',irreflexivity_gt) ).
tff(f_584,axiom,
succ(succ(succ(succ(succ(n0))))) = n5,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',successor_5) ).
tff(f_384,axiom,
! [X] : ( plus(X,n2) = succ(succ(X)) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWV003+0.ax',succ_plus_2_r) ).
tff(f_112,axiom,
! [X,Y] :
( leq(X,Y)
=> leq(X,succ(Y)) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWV003+0.ax',leq_succ) ).
tff(c_8,plain,
! [X_7] : leq(X_7,X_7),
inference(cnfTransformation,[status(thm)],[f_74]) ).
tff(c_12370,plain,
! [X_582,Y_583] :
( geq(X_582,Y_583)
| ~ leq(Y_583,X_582) ),
inference(cnfTransformation,[status(thm)],[f_89]) ).
tff(c_12382,plain,
! [X_7] : geq(X_7,X_7),
inference(resolution,[status(thm)],[c_8,c_12370]) ).
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_14723,plain,
! [X_654,I_655,VAL2_656,U_657] :
( ( a_select2(tptp_update2(X_654,I_655,VAL2_656),U_657) = a_select2(X_654,U_657) )
| ( U_657 = I_655 ) ),
inference(cnfTransformation,[status(thm)],[f_460]) ).
tff(c_7611,plain,
! [X_430,Y_431] :
( geq(X_430,Y_431)
| ~ leq(Y_431,X_430) ),
inference(cnfTransformation,[status(thm)],[f_89]) ).
tff(c_7623,plain,
! [X_7] : geq(X_7,X_7),
inference(resolution,[status(thm)],[c_8,c_7611]) ).
tff(c_484,plain,
! [X_149,U_150,V_151,VAL_152] : ( a_select3(tptp_update3(X_149,U_150,V_151,VAL_152),U_150,V_151) = VAL_152 ),
inference(cnfTransformation,[status(thm)],[f_421]) ).
tff(c_486,plain,
! [VAL2_159,V_156,I_153,U_155,X_157] :
( ( a_select3(tptp_update3(X_157,I_153,V_156,VAL2_159),U_155,V_156) = a_select3(X_157,U_155,V_156) )
| ( U_155 = I_153 ) ),
inference(cnfTransformation,[status(thm)],[f_430]) ).
tff(c_10118,plain,
! [I_517,V_515,U_516,X_518,VAL2_519] :
( ( a_select3(tptp_update3(X_518,I_517,V_515,VAL2_519),U_516,V_515) = a_select3(X_518,U_516,V_515) )
| ( U_516 = I_517 ) ),
inference(cnfTransformation,[status(thm)],[f_430]) ).
tff(c_3674,plain,
! [X_311,Y_312] :
( geq(X_311,Y_312)
| ~ leq(Y_312,X_311) ),
inference(cnfTransformation,[status(thm)],[f_89]) ).
tff(c_3686,plain,
! [X_7] : geq(X_7,X_7),
inference(resolution,[status(thm)],[c_8,c_3674]) ).
tff(c_576,plain,
succ(succ(n0)) = n2,
inference(cnfTransformation,[status(thm)],[f_586]) ).
tff(c_578,plain,
succ(succ(succ(n0))) = n3,
inference(cnfTransformation,[status(thm)],[f_587]) ).
tff(c_579,plain,
succ(n2) = n3,
inference(demodulation,[status(thm),theory(equality)],[c_576,c_578]) ).
tff(c_574,plain,
succ(n0) = n1,
inference(cnfTransformation,[status(thm)],[f_585]) ).
tff(c_580,plain,
succ(n1) = n2,
inference(demodulation,[status(thm),theory(equality)],[c_574,c_576]) ).
tff(c_570,plain,
succ(succ(succ(succ(n0)))) = n4,
inference(cnfTransformation,[status(thm)],[f_583]) ).
tff(c_582,plain,
succ(n3) = n4,
inference(demodulation,[status(thm),theory(equality)],[c_579,c_580,c_574,c_570]) ).
tff(c_500,plain,
! [X_173,I_171,VAL2_175,U_172] :
( ( a_select2(tptp_update2(X_173,I_171,VAL2_175),U_172) = a_select2(X_173,U_172) )
| ( U_172 = I_171 ) ),
inference(cnfTransformation,[status(thm)],[f_460]) ).
tff(c_6165,plain,
! [X_383,I_384,VAL2_385,U_386] :
( ( a_select2(tptp_update2(X_383,I_384,VAL2_385),U_386) = a_select2(X_383,U_386) )
| ( U_386 = I_384 ) ),
inference(cnfTransformation,[status(thm)],[f_460]) ).
tff(c_994,plain,
! [X_207,Y_208] :
( geq(X_207,Y_208)
| ~ leq(Y_208,X_207) ),
inference(cnfTransformation,[status(thm)],[f_89]) ).
tff(c_1006,plain,
! [X_7] : geq(X_7,X_7),
inference(resolution,[status(thm)],[c_8,c_994]) ).
tff(c_3368,plain,
! [X_291,V_288,U_289,VAL2_292,I_290] :
( ( a_select3(tptp_update3(X_291,I_290,V_288,VAL2_292),U_289,V_288) = a_select3(X_291,U_289,V_288) )
| ( U_289 = I_290 ) ),
inference(cnfTransformation,[status(thm)],[f_430]) ).
tff(c_512,plain,
( ( a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse,n5,use),n4,use),n5,use),n3,use),n4,use),n3,use),n5) != use )
| ( a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse,n5,use),n4,use),n5,use),n3,use),n4,use),n3,use),n4) != use )
| ( a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse,n5,use),n4,use),n5,use),n3,use),n4,use),n3,use),n3) != use )
| ( a_select3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(u_defuse,n2,n0,use),n1,n0,use),n2,n0,use),n0,n0,use),n1,n0,use),n0,n0,use),n2,n0) != use )
| ( a_select3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(u_defuse,n2,n0,use),n1,n0,use),n2,n0,use),n0,n0,use),n1,n0,use),n0,n0,use),n1,n0) != use )
| ( a_select3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(u_defuse,n2,n0,use),n1,n0,use),n2,n0,use),n0,n0,use),n1,n0,use),n0,n0,use),n0,n0) != use ) ),
inference(cnfTransformation,[status(thm)],[f_494]) ).
tff(c_586,plain,
( ( a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse,n5,use),n4,use),n5,use),n3,use),n4,use),n3,use),n5) != use )
| ( a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse,n5,use),n4,use),n5,use),n3,use),n4,use),n3,use),n4) != use )
| ( a_select3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(u_defuse,n2,n0,use),n1,n0,use),n2,n0,use),n0,n0,use),n1,n0,use),n0,n0,use),n2,n0) != use )
| ( a_select3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(u_defuse,n2,n0,use),n1,n0,use),n2,n0,use),n0,n0,use),n1,n0,use),n0,n0,use),n1,n0) != use )
| ( a_select3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(u_defuse,n2,n0,use),n1,n0,use),n2,n0,use),n0,n0,use),n1,n0,use),n0,n0,use),n0,n0) != use ) ),
inference(demodulation,[status(thm),theory(equality)],[c_498,c_512]) ).
tff(c_588,plain,
( ( a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse,n5,use),n4,use),n5,use),n3,use),n4,use),n3,use),n5) != use )
| ( a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse,n5,use),n4,use),n5,use),n3,use),n4,use),n3,use),n4) != use )
| ( a_select3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(u_defuse,n2,n0,use),n1,n0,use),n2,n0,use),n0,n0,use),n1,n0,use),n0,n0,use),n2,n0) != use )
| ( a_select3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(u_defuse,n2,n0,use),n1,n0,use),n2,n0,use),n0,n0,use),n1,n0,use),n0,n0,use),n1,n0) != use ) ),
inference(demodulation,[status(thm),theory(equality)],[c_484,c_586]) ).
tff(c_608,plain,
a_select3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(u_defuse,n2,n0,use),n1,n0,use),n2,n0,use),n0,n0,use),n1,n0,use),n0,n0,use),n1,n0) != use,
inference(splitLeft,[status(thm)],[c_588]) ).
tff(c_3378,plain,
( ( a_select3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(u_defuse,n2,n0,use),n1,n0,use),n2,n0,use),n0,n0,use),n1,n0,use),n1,n0) != use )
| ( n1 = n0 ) ),
inference(superposition,[status(thm),theory(equality)],[c_3368,c_608]) ).
tff(c_3388,plain,
n1 = n0,
inference(demodulation,[status(thm),theory(equality)],[c_484,c_3378]) ).
tff(c_16,plain,
! [Y_14,X_13] :
( leq(Y_14,X_13)
| ~ geq(X_13,Y_14) ),
inference(cnfTransformation,[status(thm)],[f_89]) ).
tff(c_1280,plain,
! [Y_218,X_219] :
( gt(succ(Y_218),X_219)
| ~ leq(X_219,Y_218) ),
inference(cnfTransformation,[status(thm)],[f_116]) ).
tff(c_6,plain,
! [X_6] : ~ gt(X_6,X_6),
inference(cnfTransformation,[status(thm)],[f_71]) ).
tff(c_1371,plain,
! [Y_225] : ~ leq(succ(Y_225),Y_225),
inference(resolution,[status(thm)],[c_1280,c_6]) ).
tff(c_1406,plain,
~ leq(n1,n0),
inference(superposition,[status(thm),theory(equality)],[c_574,c_1371]) ).
tff(c_1491,plain,
~ geq(n0,n1),
inference(resolution,[status(thm)],[c_16,c_1406]) ).
tff(c_3413,plain,
~ geq(n0,n0),
inference(demodulation,[status(thm),theory(equality)],[c_3388,c_1491]) ).
tff(c_3447,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_1006,c_3413]) ).
tff(c_3448,plain,
( ( a_select3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(u_defuse,n2,n0,use),n1,n0,use),n2,n0,use),n0,n0,use),n1,n0,use),n0,n0,use),n2,n0) != use )
| ( a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse,n5,use),n4,use),n5,use),n3,use),n4,use),n3,use),n4) != use )
| ( a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse,n5,use),n4,use),n5,use),n3,use),n4,use),n3,use),n5) != use ) ),
inference(splitRight,[status(thm)],[c_588]) ).
tff(c_3468,plain,
a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse,n5,use),n4,use),n5,use),n3,use),n4,use),n3,use),n5) != use,
inference(splitLeft,[status(thm)],[c_3448]) ).
tff(c_6175,plain,
( ( a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse,n5,use),n4,use),n5,use),n3,use),n4,use),n5) != use )
| ( n5 = n3 ) ),
inference(superposition,[status(thm),theory(equality)],[c_6165,c_3468]) ).
tff(c_6376,plain,
a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse,n5,use),n4,use),n5,use),n3,use),n4,use),n5) != use,
inference(splitLeft,[status(thm)],[c_6175]) ).
tff(c_6773,plain,
( ( a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse,n5,use),n4,use),n5,use),n3,use),n5) != use )
| ( n5 = n4 ) ),
inference(superposition,[status(thm),theory(equality)],[c_500,c_6376]) ).
tff(c_6861,plain,
a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse,n5,use),n4,use),n5,use),n3,use),n5) != use,
inference(splitLeft,[status(thm)],[c_6773]) ).
tff(c_7089,plain,
( ( a_select2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse,n5,use),n4,use),n5,use),n5) != use )
| ( n5 = n3 ) ),
inference(superposition,[status(thm),theory(equality)],[c_500,c_6861]) ).
tff(c_7091,plain,
n5 = n3,
inference(demodulation,[status(thm),theory(equality)],[c_498,c_7089]) ).
tff(c_7092,plain,
a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse,n3,use),n4,use),n3,use),n3,use),n3) != use,
inference(demodulation,[status(thm),theory(equality)],[c_7091,c_7091,c_7091,c_6861]) ).
tff(c_7144,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_498,c_7092]) ).
tff(c_7145,plain,
n5 = n4,
inference(splitRight,[status(thm)],[c_6773]) ).
tff(c_7152,plain,
a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse,n4,use),n4,use),n4,use),n3,use),n4,use),n4) != use,
inference(demodulation,[status(thm),theory(equality)],[c_7145,c_7145,c_7145,c_6376]) ).
tff(c_7195,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_498,c_7152]) ).
tff(c_7196,plain,
n5 = n3,
inference(splitRight,[status(thm)],[c_6175]) ).
tff(c_572,plain,
succ(succ(succ(succ(succ(n0))))) = n5,
inference(cnfTransformation,[status(thm)],[f_584]) ).
tff(c_581,plain,
succ(succ(n3)) = n5,
inference(demodulation,[status(thm),theory(equality)],[c_579,c_580,c_574,c_572]) ).
tff(c_583,plain,
succ(n4) = n5,
inference(demodulation,[status(thm),theory(equality)],[c_582,c_581]) ).
tff(c_3688,plain,
! [X_314] : ( succ(succ(X_314)) = plus(X_314,n2) ),
inference(cnfTransformation,[status(thm)],[f_384]) ).
tff(c_3715,plain,
plus(n4,n2) = succ(n5),
inference(superposition,[status(thm),theory(equality)],[c_583,c_3688]) ).
tff(c_454,plain,
! [X_132] : ( succ(succ(X_132)) = plus(X_132,n2) ),
inference(cnfTransformation,[status(thm)],[f_384]) ).
tff(c_30,plain,
! [X_22,Y_23] :
( leq(X_22,succ(Y_23))
| ~ leq(X_22,Y_23) ),
inference(cnfTransformation,[status(thm)],[f_112]) ).
tff(c_3834,plain,
! [Y_316,X_317] :
( gt(succ(Y_316),X_317)
| ~ leq(X_317,Y_316) ),
inference(cnfTransformation,[status(thm)],[f_116]) ).
tff(c_3912,plain,
! [Y_320] : ~ leq(succ(Y_320),Y_320),
inference(resolution,[status(thm)],[c_3834,c_6]) ).
tff(c_3916,plain,
! [Y_23] : ~ leq(succ(succ(Y_23)),Y_23),
inference(resolution,[status(thm)],[c_30,c_3912]) ).
tff(c_4562,plain,
! [Y_341] : ~ leq(plus(Y_341,n2),Y_341),
inference(demodulation,[status(thm),theory(equality)],[c_454,c_3916]) ).
tff(c_4565,plain,
~ leq(succ(n5),n4),
inference(superposition,[status(thm),theory(equality)],[c_3715,c_4562]) ).
tff(c_4937,plain,
~ geq(n4,succ(n5)),
inference(resolution,[status(thm)],[c_16,c_4565]) ).
tff(c_7215,plain,
~ geq(n4,succ(n3)),
inference(demodulation,[status(thm),theory(equality)],[c_7196,c_4937]) ).
tff(c_7249,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_3686,c_582,c_7215]) ).
tff(c_7250,plain,
( ( a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse,n5,use),n4,use),n5,use),n3,use),n4,use),n3,use),n4) != use )
| ( a_select3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(u_defuse,n2,n0,use),n1,n0,use),n2,n0,use),n0,n0,use),n1,n0,use),n0,n0,use),n2,n0) != use ) ),
inference(splitRight,[status(thm)],[c_3448]) ).
tff(c_7381,plain,
a_select3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(u_defuse,n2,n0,use),n1,n0,use),n2,n0,use),n0,n0,use),n1,n0,use),n0,n0,use),n2,n0) != use,
inference(splitLeft,[status(thm)],[c_7250]) ).
tff(c_10128,plain,
( ( a_select3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(u_defuse,n2,n0,use),n1,n0,use),n2,n0,use),n0,n0,use),n1,n0,use),n2,n0) != use )
| ( n2 = n0 ) ),
inference(superposition,[status(thm),theory(equality)],[c_10118,c_7381]) ).
tff(c_10337,plain,
a_select3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(u_defuse,n2,n0,use),n1,n0,use),n2,n0,use),n0,n0,use),n1,n0,use),n2,n0) != use,
inference(splitLeft,[status(thm)],[c_10128]) ).
tff(c_11352,plain,
( ( a_select3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(u_defuse,n2,n0,use),n1,n0,use),n2,n0,use),n0,n0,use),n2,n0) != use )
| ( n2 = n1 ) ),
inference(superposition,[status(thm),theory(equality)],[c_486,c_10337]) ).
tff(c_11621,plain,
a_select3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(u_defuse,n2,n0,use),n1,n0,use),n2,n0,use),n0,n0,use),n2,n0) != use,
inference(splitLeft,[status(thm)],[c_11352]) ).
tff(c_11911,plain,
( ( a_select3(tptp_update3(tptp_update3(tptp_update3(u_defuse,n2,n0,use),n1,n0,use),n2,n0,use),n2,n0) != use )
| ( n2 = n0 ) ),
inference(superposition,[status(thm),theory(equality)],[c_486,c_11621]) ).
tff(c_11913,plain,
n2 = n0,
inference(demodulation,[status(thm),theory(equality)],[c_484,c_11911]) ).
tff(c_11914,plain,
a_select3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(u_defuse,n0,n0,use),n1,n0,use),n0,n0,use),n0,n0,use),n0,n0) != use,
inference(demodulation,[status(thm),theory(equality)],[c_11913,c_11913,c_11913,c_11621]) ).
tff(c_11986,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_484,c_11914]) ).
tff(c_11987,plain,
n2 = n1,
inference(splitRight,[status(thm)],[c_11352]) ).
tff(c_11991,plain,
a_select3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(u_defuse,n1,n0,use),n1,n0,use),n1,n0,use),n0,n0,use),n1,n0,use),n1,n0) != use,
inference(demodulation,[status(thm),theory(equality)],[c_11987,c_11987,c_11987,c_10337]) ).
tff(c_12062,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_484,c_11991]) ).
tff(c_12063,plain,
n2 = n0,
inference(splitRight,[status(thm)],[c_10128]) ).
tff(c_7455,plain,
! [X_424] : ( succ(succ(X_424)) = plus(X_424,n2) ),
inference(cnfTransformation,[status(thm)],[f_384]) ).
tff(c_7491,plain,
plus(n0,n2) = succ(n1),
inference(superposition,[status(thm),theory(equality)],[c_574,c_7455]) ).
tff(c_7500,plain,
plus(n0,n2) = n2,
inference(demodulation,[status(thm),theory(equality)],[c_580,c_7491]) ).
tff(c_8152,plain,
! [X_453,Y_454] :
( leq(X_453,succ(Y_454))
| ~ leq(X_453,Y_454) ),
inference(cnfTransformation,[status(thm)],[f_112]) ).
tff(c_7965,plain,
! [Y_448,X_449] :
( gt(succ(Y_448),X_449)
| ~ leq(X_449,Y_448) ),
inference(cnfTransformation,[status(thm)],[f_116]) ).
tff(c_8011,plain,
! [Y_448] : ~ leq(succ(Y_448),Y_448),
inference(resolution,[status(thm)],[c_7965,c_6]) ).
tff(c_8156,plain,
! [Y_454] : ~ leq(succ(succ(Y_454)),Y_454),
inference(resolution,[status(thm)],[c_8152,c_8011]) ).
tff(c_8583,plain,
! [Y_470] : ~ leq(plus(Y_470,n2),Y_470),
inference(demodulation,[status(thm),theory(equality)],[c_454,c_8156]) ).
tff(c_8607,plain,
~ leq(n2,n0),
inference(superposition,[status(thm),theory(equality)],[c_7500,c_8583]) ).
tff(c_8823,plain,
~ geq(n0,n2),
inference(resolution,[status(thm)],[c_16,c_8607]) ).
tff(c_12078,plain,
~ geq(n0,n0),
inference(demodulation,[status(thm),theory(equality)],[c_12063,c_8823]) ).
tff(c_12129,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_7623,c_12078]) ).
tff(c_12130,plain,
a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse,n5,use),n4,use),n5,use),n3,use),n4,use),n3,use),n4) != use,
inference(splitRight,[status(thm)],[c_7250]) ).
tff(c_14733,plain,
( ( a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse,n5,use),n4,use),n5,use),n3,use),n4,use),n4) != use )
| ( n4 = n3 ) ),
inference(superposition,[status(thm),theory(equality)],[c_14723,c_12130]) ).
tff(c_14749,plain,
n4 = n3,
inference(demodulation,[status(thm),theory(equality)],[c_498,c_14733]) ).
tff(c_12673,plain,
! [Y_593,X_594] :
( gt(succ(Y_593),X_594)
| ~ leq(X_594,Y_593) ),
inference(cnfTransformation,[status(thm)],[f_116]) ).
tff(c_12792,plain,
! [Y_598] : ~ leq(succ(Y_598),Y_598),
inference(resolution,[status(thm)],[c_12673,c_6]) ).
tff(c_12828,plain,
~ leq(n4,n3),
inference(superposition,[status(thm),theory(equality)],[c_582,c_12792]) ).
tff(c_12898,plain,
~ geq(n3,n4),
inference(resolution,[status(thm)],[c_16,c_12828]) ).
tff(c_14766,plain,
~ geq(n3,n3),
inference(demodulation,[status(thm),theory(equality)],[c_14749,c_12898]) ).
tff(c_14801,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_12382,c_14766]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.13 % Problem : SWV089+1 : TPTP v9.0.0. Bugfixed v3.3.0.
% 0.07/0.13 % 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.14/0.35 % Computer : n005.cluster.edu
% 0.14/0.35 % Model : x86_64 x86_64
% 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.35 % Memory : 8042.1875MB
% 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.35 % CPULimit : 300
% 0.14/0.35 % WCLimit : 300
% 0.14/0.35 % DateTime : Wed Apr 9 02:43:12 EDT 2025
% 0.14/0.35 % CPUTime :
% 15.03/4.57 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 15.03/4.59
% 15.03/4.59 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------