%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : HWV029-1 : TPTP v9.0.0. Released v2.5.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 : n012.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 06:46:50 PM UTC 2025
% Result : Unsatisfiable 32.05s 18.97s
% Output : CNFRefutation 32.37s
% Verified :
% SZS Type : Refutation
% Derivation depth : 22
% Number of leaves : 30
% Syntax : Number of formulae : 275 ( 109 unt; 0 typ; 0 def)
% Number of atoms : 640 ( 183 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 580 ( 215 ~; 365 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 3 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 14 ( 12 usr; 1 prp; 0-3 aty)
% Number of functors : 11 ( 11 usr; 4 con; 0-2 aty)
% Number of variables : 162 ( 162 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ p_Mem > p_Data_out > p_Data_in > gt > def_10 > p_Wr_error > p_Wr > p_Reset > p_Rd_error > p_Rd > p_Full > p_Empty > plus > minus > #nlpp > y_27 > wr_level > rd_level > level > int_level > x_139 > n1 > n0 > fifo_length
%Foreground sorts:
%Background operators:
%Foreground operators:
tff(p_Data_out,type,
p_Data_out: ( $i * $i ) > $o ).
tff(rd_level,type,
rd_level: $i > $i ).
tff(p_Mem,type,
p_Mem: ( $i * $i * $i ) > $o ).
tff(p_Rd_error,type,
p_Rd_error: $i > $o ).
tff(fifo_length,type,
fifo_length: $i ).
tff(p_Wr,type,
p_Wr: $i > $o ).
tff(def_10,type,
def_10: ( $i * $i ) > $o ).
tff(y_27,type,
y_27: $i > $i ).
tff(n1,type,
n1: $i ).
tff(plus,type,
plus: ( $i * $i ) > $i ).
tff(wr_level,type,
wr_level: $i > $i ).
tff(int_level,type,
int_level: $i > $i ).
tff(p_Full,type,
p_Full: $i > $o ).
tff(n0,type,
n0: $i ).
tff(p_Reset,type,
p_Reset: $i > $o ).
tff(gt,type,
gt: ( $i * $i ) > $o ).
tff(p_Empty,type,
p_Empty: $i > $o ).
tff(p_Wr_error,type,
p_Wr_error: $i > $o ).
tff(p_Data_in,type,
p_Data_in: ( $i * $i ) > $o ).
tff(x_139,type,
x_139: $i ).
tff(level,type,
level: $i > $i ).
tff(p_Rd,type,
p_Rd: $i > $o ).
tff(minus,type,
minus: ( $i * $i ) > $i ).
tff(f_80,axiom,
! [Y_4,X_3] :
( ~ def_10(Y_4,X_3)
| ( X_3 != Y_4 ) ),
file(unknown,unknown) ).
tff(f_942,axiom,
gt(fifo_length,n0),
file(unknown,unknown) ).
tff(f_143,axiom,
! [X_31] : ( plus(n0,X_31) = X_31 ),
file(unknown,unknown) ).
tff(f_85,axiom,
! [Y_12,X_11] :
( ~ gt(Y_12,X_11)
| gt(plus(Y_12,n1),plus(X_11,n1)) ),
file(unknown,unknown) ).
tff(f_104,axiom,
! [X_15,Y_16] :
( ~ gt(plus(X_15,n1),Y_16)
| gt(X_15,Y_16)
| ( X_15 = Y_16 ) ),
file(unknown,unknown) ).
tff(f_74,axiom,
! [Y_4,X_3] :
( ~ def_10(Y_4,X_3)
| ~ gt(X_3,Y_4) ),
file(unknown,unknown) ).
tff(f_61,axiom,
! [X_3,Y_4,Z_5] :
( ( minus(X_3,Y_4) != Z_5 )
| ( plus(Z_5,Y_4) = X_3 )
| def_10(Y_4,X_3) ),
file(unknown,unknown) ).
tff(f_47,axiom,
! [X_0] : ( plus(X_0,n1) != n0 ),
file(unknown,unknown) ).
tff(f_133,axiom,
! [X_26] :
( ( X_26 = n0 )
| ( X_26 = plus(y_27(X_26),n1) ) ),
file(unknown,unknown) ).
tff(f_141,axiom,
! [X_29,Y_30] :
( ( plus(X_29,n1) != plus(Y_30,n1) )
| ( X_29 = Y_30 ) ),
file(unknown,unknown) ).
tff(f_171,axiom,
! [X_t_37] :
( ~ p_Reset(X_t_37)
| ( int_level(plus(X_t_37,n1)) = n0 ) ),
file(unknown,unknown) ).
tff(f_146,axiom,
! [X_t_32] : ( level(X_t_32) = int_level(X_t_32) ),
file(unknown,unknown) ).
tff(f_941,axiom,
gt(level(plus(x_139,n1)),fifo_length),
file(unknown,unknown) ).
tff(f_136,axiom,
! [X_28] : ~ gt(X_28,X_28),
file(unknown,unknown) ).
tff(f_129,axiom,
! [X_25] :
( ( X_25 = n0 )
| gt(X_25,n0) ),
file(unknown,unknown) ).
tff(f_118,axiom,
! [Z_21,Y_20,X_19] :
( ~ gt(Z_21,Y_20)
| gt(Z_21,X_19)
| ~ gt(Y_20,X_19) ),
file(unknown,unknown) ).
tff(f_940,axiom,
~ gt(level(x_139),fifo_length),
file(unknown,unknown) ).
tff(f_856,axiom,
! [X_t_42] :
( p_Reset(X_t_42)
| p_Wr(X_t_42)
| p_Rd(X_t_42)
| ( int_level(plus(X_t_42,n1)) = int_level(X_t_42) ) ),
file(unknown,unknown) ).
tff(f_110,axiom,
! [Y_18,X_17] :
( gt(Y_18,X_17)
| ( X_17 = Y_18 )
| gt(X_17,Y_18) ),
file(unknown,unknown) ).
tff(f_554,axiom,
! [X_t_42] :
( p_Reset(X_t_42)
| ~ p_Wr(X_t_42)
| ~ p_Rd(X_t_42)
| gt(int_level(X_t_42),n0)
| p_Rd_error(plus(X_t_42,n1)) ),
file(unknown,unknown) ).
tff(f_239,axiom,
! [X_t_42] :
( p_Reset(X_t_42)
| ~ p_Wr(X_t_42)
| p_Rd(X_t_42)
| ~ gt(fifo_length,int_level(X_t_42))
| ( int_level(plus(X_t_42,n1)) = plus(int_level(X_t_42),n1) ) ),
file(unknown,unknown) ).
tff(f_566,axiom,
! [X_t_42] :
( p_Reset(X_t_42)
| ~ p_Wr(X_t_42)
| ~ p_Rd(X_t_42)
| gt(int_level(X_t_42),n0)
| ( int_level(plus(X_t_42,n1)) = plus(int_level(X_t_42),n1) ) ),
file(unknown,unknown) ).
tff(f_812,axiom,
! [X_t_42] :
( p_Reset(X_t_42)
| p_Wr(X_t_42)
| ~ p_Rd(X_t_42)
| gt(int_level(X_t_42),n0)
| ( int_level(plus(X_t_42,n1)) = int_level(X_t_42) ) ),
file(unknown,unknown) ).
tff(f_90,axiom,
! [Y_12,X_11] :
( gt(Y_12,X_11)
| ~ gt(plus(Y_12,n1),plus(X_11,n1)) ),
file(unknown,unknown) ).
tff(f_479,axiom,
! [X_t_42] :
( p_Reset(X_t_42)
| ~ p_Wr(X_t_42)
| ~ p_Rd(X_t_42)
| ~ gt(int_level(X_t_42),n0)
| ( int_level(plus(X_t_42,n1)) = int_level(X_t_42) ) ),
file(unknown,unknown) ).
tff(f_125,axiom,
! [Y_24,X_23] :
( ~ gt(Y_24,X_23)
| ( plus(X_23,n1) = Y_24 )
| gt(Y_24,plus(X_23,n1)) ),
file(unknown,unknown) ).
tff(f_720,axiom,
! [X_t_42] :
( p_Reset(X_t_42)
| p_Wr(X_t_42)
| ~ p_Rd(X_t_42)
| ~ gt(int_level(X_t_42),n0)
| ( int_level(plus(X_t_42,n1)) = minus(int_level(X_t_42),n1) ) ),
file(unknown,unknown) ).
tff(f_54,axiom,
! [X_2] :
( ~ gt(X_2,n0)
| gt(X_2,minus(X_2,n1)) ),
file(unknown,unknown) ).
tff(f_466,axiom,
! [X_t_42] :
( p_Reset(X_t_42)
| ~ p_Wr(X_t_42)
| ~ p_Rd(X_t_42)
| ~ gt(int_level(X_t_42),n0)
| ~ p_Rd_error(plus(X_t_42,n1)) ),
file(unknown,unknown) ).
tff(f_365,axiom,
! [X_t_42] :
( p_Reset(X_t_42)
| ~ p_Wr(X_t_42)
| p_Rd(X_t_42)
| gt(fifo_length,int_level(X_t_42))
| ( int_level(plus(X_t_42,n1)) = int_level(X_t_42) ) ),
file(unknown,unknown) ).
tff(c_14,plain,
! [Y_4_12] : ~ def_10(Y_4_12,Y_4_12),
inference(cnfTransformation,[status(thm)],[f_80]) ).
tff(c_186,plain,
gt(fifo_length,n0),
inference(cnfTransformation,[status(thm)],[f_942]) ).
tff(c_38,plain,
! [X_31_34] : ( plus(n0,X_31_34) = X_31_34 ),
inference(cnfTransformation,[status(thm)],[f_143]) ).
tff(c_151072,plain,
! [Y_12_1723,X_11_1724] :
( gt(plus(Y_12_1723,n1),plus(X_11_1724,n1))
| ~ gt(Y_12_1723,X_11_1724) ),
inference(cnfTransformation,[status(thm)],[f_85]) ).
tff(c_151165,plain,
! [Y_12_1726] :
( gt(plus(Y_12_1726,n1),n1)
| ~ gt(Y_12_1726,n0) ),
inference(superposition,[status(thm),theory(equality)],[c_38,c_151072]) ).
tff(c_22,plain,
! [Y_16_21,X_15_20] :
( ( Y_16_21 = X_15_20 )
| gt(X_15_20,Y_16_21)
| ~ gt(plus(X_15_20,n1),Y_16_21) ),
inference(cnfTransformation,[status(thm)],[f_104]) ).
tff(c_154800,plain,
! [Y_12_1819] :
( ( n1 = Y_12_1819 )
| gt(Y_12_1819,n1)
| ~ gt(Y_12_1819,n0) ),
inference(resolution,[status(thm)],[c_151165,c_22]) ).
tff(c_12,plain,
! [X_3_11,Y_4_10] :
( ~ gt(X_3_11,Y_4_10)
| ~ def_10(Y_4_10,X_3_11) ),
inference(cnfTransformation,[status(thm)],[f_74]) ).
tff(c_154881,plain,
! [Y_12_1821] :
( ~ def_10(n1,Y_12_1821)
| ( n1 = Y_12_1821 )
| ~ gt(Y_12_1821,n0) ),
inference(resolution,[status(thm)],[c_154800,c_12]) ).
tff(c_154936,plain,
( ~ def_10(n1,fifo_length)
| ( n1 = fifo_length ) ),
inference(resolution,[status(thm)],[c_186,c_154881]) ).
tff(c_154937,plain,
~ def_10(n1,fifo_length),
inference(splitLeft,[status(thm)],[c_154936]) ).
tff(c_8,plain,
! [Y_4_5,X_3_4] :
( def_10(Y_4_5,X_3_4)
| ( plus(minus(X_3_4,Y_4_5),Y_4_5) = X_3_4 ) ),
inference(cnfTransformation,[status(thm)],[f_61]) ).
tff(c_2,plain,
! [X_0_1] : ( plus(X_0_1,n1) != n0 ),
inference(cnfTransformation,[status(thm)],[f_47]) ).
tff(c_32,plain,
! [X_26_30] :
( ( plus(y_27(X_26_30),n1) = X_26_30 )
| ( n0 = X_26_30 ) ),
inference(cnfTransformation,[status(thm)],[f_133]) ).
tff(c_367,plain,
! [Y_30_164,X_29_165] :
( ( Y_30_164 = X_29_165 )
| ( plus(Y_30_164,n1) != plus(X_29_165,n1) ) ),
inference(cnfTransformation,[status(thm)],[f_141]) ).
tff(c_373,plain,
! [X_26_30,Y_30_164] :
( ( y_27(X_26_30) = Y_30_164 )
| ( plus(Y_30_164,n1) != X_26_30 )
| ( n0 = X_26_30 ) ),
inference(superposition,[status(thm),theory(equality)],[c_32,c_367]) ).
tff(c_155462,plain,
! [Y_30_164] :
( ( y_27(plus(Y_30_164,n1)) = Y_30_164 )
| ( plus(Y_30_164,n1) = n0 ) ),
inference(reflexivity,[status(thm),theory(equality)],[c_373]) ).
tff(c_155476,plain,
! [Y_30_1838] : ( y_27(plus(Y_30_1838,n1)) = Y_30_1838 ),
inference(negUnitSimplification,[status(thm)],[c_2,c_155462]) ).
tff(c_155597,plain,
! [X_3_1840] :
( ( minus(X_3_1840,n1) = y_27(X_3_1840) )
| def_10(n1,X_3_1840) ),
inference(superposition,[status(thm),theory(equality)],[c_8,c_155476]) ).
tff(c_155622,plain,
minus(fifo_length,n1) = y_27(fifo_length),
inference(resolution,[status(thm)],[c_155597,c_154937]) ).
tff(c_155634,plain,
( def_10(n1,fifo_length)
| ( plus(y_27(fifo_length),n1) = fifo_length ) ),
inference(superposition,[status(thm),theory(equality)],[c_155622,c_8]) ).
tff(c_155643,plain,
plus(y_27(fifo_length),n1) = fifo_length,
inference(negUnitSimplification,[status(thm)],[c_154937,c_155634]) ).
tff(c_299,plain,
! [X_t_37_158] :
( ( int_level(plus(X_t_37_158,n1)) = n0 )
| ~ p_Reset(X_t_37_158) ),
inference(cnfTransformation,[status(thm)],[f_171]) ).
tff(c_42,plain,
! [X_t_32_35] : ( level(X_t_32_35) = int_level(X_t_32_35) ),
inference(cnfTransformation,[status(thm)],[f_146]) ).
tff(c_184,plain,
gt(level(plus(x_139,n1)),fifo_length),
inference(cnfTransformation,[status(thm)],[f_941]) ).
tff(c_188,plain,
gt(int_level(plus(x_139,n1)),fifo_length),
inference(demodulation,[status(thm),theory(equality)],[c_42,c_184]) ).
tff(c_308,plain,
( gt(n0,fifo_length)
| ~ p_Reset(x_139) ),
inference(superposition,[status(thm),theory(equality)],[c_299,c_188]) ).
tff(c_321,plain,
~ p_Reset(x_139),
inference(splitLeft,[status(thm)],[c_308]) ).
tff(c_34,plain,
! [X_28_31] : ~ gt(X_28_31,X_28_31),
inference(cnfTransformation,[status(thm)],[f_136]) ).
tff(c_30,plain,
! [X_25_29] :
( gt(X_25_29,n0)
| ( n0 = X_25_29 ) ),
inference(cnfTransformation,[status(thm)],[f_129]) ).
tff(c_568,plain,
! [Y_20_184,X_19_185,Z_21_186] :
( ~ gt(Y_20_184,X_19_185)
| gt(Z_21_186,X_19_185)
| ~ gt(Z_21_186,Y_20_184) ),
inference(cnfTransformation,[status(thm)],[f_118]) ).
tff(c_776,plain,
! [Z_21_200,X_25_201] :
( gt(Z_21_200,n0)
| ~ gt(Z_21_200,X_25_201)
| ( n0 = X_25_201 ) ),
inference(resolution,[status(thm)],[c_30,c_568]) ).
tff(c_812,plain,
( gt(int_level(plus(x_139,n1)),n0)
| ( n0 = fifo_length ) ),
inference(resolution,[status(thm)],[c_188,c_776]) ).
tff(c_934,plain,
n0 = fifo_length,
inference(splitLeft,[status(thm)],[c_812]) ).
tff(c_976,plain,
gt(fifo_length,fifo_length),
inference(demodulation,[status(thm),theory(equality)],[c_934,c_186]) ).
tff(c_978,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_34,c_976]) ).
tff(c_980,plain,
n0 != fifo_length,
inference(splitRight,[status(thm)],[c_812]) ).
tff(c_1115,plain,
! [Y_12_211,X_11_212] :
( gt(plus(Y_12_211,n1),plus(X_11_212,n1))
| ~ gt(Y_12_211,X_11_212) ),
inference(cnfTransformation,[status(thm)],[f_85]) ).
tff(c_1168,plain,
! [X_11_213] :
( gt(n1,plus(X_11_213,n1))
| ~ gt(n0,X_11_213) ),
inference(superposition,[status(thm),theory(equality)],[c_38,c_1115]) ).
tff(c_981,plain,
! [Y_16_208,X_15_209] :
( ( Y_16_208 = X_15_209 )
| gt(X_15_209,Y_16_208)
| ~ gt(plus(X_15_209,n1),Y_16_208) ),
inference(cnfTransformation,[status(thm)],[f_104]) ).
tff(c_1027,plain,
! [Y_16_208] :
( ( n0 = Y_16_208 )
| gt(n0,Y_16_208)
| ~ gt(n1,Y_16_208) ),
inference(superposition,[status(thm),theory(equality)],[c_38,c_981]) ).
tff(c_1171,plain,
! [X_11_213] :
( ( plus(X_11_213,n1) = n0 )
| gt(n0,plus(X_11_213,n1))
| ~ gt(n0,X_11_213) ),
inference(resolution,[status(thm)],[c_1168,c_1027]) ).
tff(c_1265,plain,
! [X_11_218] :
( gt(n0,plus(X_11_218,n1))
| ~ gt(n0,X_11_218) ),
inference(negUnitSimplification,[status(thm)],[c_2,c_1171]) ).
tff(c_597,plain,
! [Z_21_186,X_25_29] :
( gt(Z_21_186,n0)
| ~ gt(Z_21_186,X_25_29)
| ( n0 = X_25_29 ) ),
inference(resolution,[status(thm)],[c_30,c_568]) ).
tff(c_1267,plain,
! [X_11_218] :
( gt(n0,n0)
| ( plus(X_11_218,n1) = n0 )
| ~ gt(n0,X_11_218) ),
inference(resolution,[status(thm)],[c_1265,c_597]) ).
tff(c_1289,plain,
! [X_11_218] : ~ gt(n0,X_11_218),
inference(negUnitSimplification,[status(thm)],[c_2,c_34,c_1267]) ).
tff(c_482,plain,
! [Y_4_177,X_3_178] :
( def_10(Y_4_177,X_3_178)
| ( plus(minus(X_3_178,Y_4_177),Y_4_177) = X_3_178 ) ),
inference(cnfTransformation,[status(thm)],[f_61]) ).
tff(c_537,plain,
! [X_3_178] :
( ( n0 != X_3_178 )
| def_10(n1,X_3_178) ),
inference(superposition,[status(thm),theory(equality)],[c_482,c_2]) ).
tff(c_182,plain,
~ gt(level(x_139),fifo_length),
inference(cnfTransformation,[status(thm)],[f_940]) ).
tff(c_187,plain,
~ gt(int_level(x_139),fifo_length),
inference(demodulation,[status(thm),theory(equality)],[c_42,c_182]) ).
tff(c_1603,plain,
! [X_t_42_228] :
( ( int_level(plus(X_t_42_228,n1)) = int_level(X_t_42_228) )
| p_Rd(X_t_42_228)
| p_Wr(X_t_42_228)
| p_Reset(X_t_42_228) ),
inference(cnfTransformation,[status(thm)],[f_856]) ).
tff(c_1621,plain,
( gt(int_level(x_139),fifo_length)
| p_Rd(x_139)
| p_Wr(x_139)
| p_Reset(x_139) ),
inference(superposition,[status(thm),theory(equality)],[c_1603,c_188]) ).
tff(c_1643,plain,
( p_Rd(x_139)
| p_Wr(x_139) ),
inference(negUnitSimplification,[status(thm)],[c_321,c_187,c_1621]) ).
tff(c_1699,plain,
p_Wr(x_139),
inference(splitLeft,[status(thm)],[c_1643]) ).
tff(c_442,plain,
! [X_17_172,Y_18_173] :
( gt(X_17_172,Y_18_173)
| ( Y_18_173 = X_17_172 )
| gt(Y_18_173,X_17_172) ),
inference(cnfTransformation,[status(thm)],[f_110]) ).
tff(c_460,plain,
( ( int_level(x_139) = fifo_length )
| gt(fifo_length,int_level(x_139)) ),
inference(resolution,[status(thm)],[c_442,c_187]) ).
tff(c_463,plain,
gt(fifo_length,int_level(x_139)),
inference(splitLeft,[status(thm)],[c_460]) ).
tff(c_24,plain,
! [X_17_23,Y_18_22] :
( gt(X_17_23,Y_18_22)
| ( Y_18_22 = X_17_23 )
| gt(Y_18_22,X_17_23) ),
inference(cnfTransformation,[status(thm)],[f_110]) ).
tff(c_591,plain,
! [Z_21_186] :
( gt(Z_21_186,int_level(x_139))
| ~ gt(Z_21_186,fifo_length) ),
inference(resolution,[status(thm)],[c_463,c_568]) ).
tff(c_1418,plain,
! [Y_16_224] :
( ( n0 = Y_16_224 )
| ~ gt(n1,Y_16_224) ),
inference(negUnitSimplification,[status(thm)],[c_1289,c_1027]) ).
tff(c_1455,plain,
( ( int_level(x_139) = n0 )
| ~ gt(n1,fifo_length) ),
inference(resolution,[status(thm)],[c_591,c_1418]) ).
tff(c_1543,plain,
~ gt(n1,fifo_length),
inference(splitLeft,[status(thm)],[c_1455]) ).
tff(c_1555,plain,
( gt(fifo_length,n1)
| ( n1 = fifo_length ) ),
inference(resolution,[status(thm)],[c_24,c_1543]) ).
tff(c_1602,plain,
n1 = fifo_length,
inference(splitLeft,[status(thm)],[c_1555]) ).
tff(c_1321,plain,
! [Y_16_208] :
( ( n0 = Y_16_208 )
| ~ gt(n1,Y_16_208) ),
inference(negUnitSimplification,[status(thm)],[c_1289,c_1027]) ).
tff(c_1782,plain,
! [Y_16_235] :
( ( n0 = Y_16_235 )
| ~ gt(fifo_length,Y_16_235) ),
inference(demodulation,[status(thm),theory(equality)],[c_1602,c_1321]) ).
tff(c_1816,plain,
int_level(x_139) = n0,
inference(resolution,[status(thm)],[c_463,c_1782]) ).
tff(c_116,plain,
! [X_t_42_89] :
( p_Rd_error(plus(X_t_42_89,n1))
| gt(int_level(X_t_42_89),n0)
| ~ p_Rd(X_t_42_89)
| ~ p_Wr(X_t_42_89)
| p_Reset(X_t_42_89) ),
inference(cnfTransformation,[status(thm)],[f_554]) ).
tff(c_2879,plain,
! [X_t_42_281] :
( p_Rd_error(plus(X_t_42_281,fifo_length))
| gt(int_level(X_t_42_281),n0)
| ~ p_Rd(X_t_42_281)
| ~ p_Wr(X_t_42_281)
| p_Reset(X_t_42_281) ),
inference(demodulation,[status(thm),theory(equality)],[c_1602,c_116]) ).
tff(c_2901,plain,
( p_Rd_error(plus(x_139,fifo_length))
| gt(n0,n0)
| ~ p_Rd(x_139)
| ~ p_Wr(x_139)
| p_Reset(x_139) ),
inference(superposition,[status(thm),theory(equality)],[c_1816,c_2879]) ).
tff(c_2910,plain,
( p_Rd_error(plus(x_139,fifo_length))
| gt(n0,n0)
| ~ p_Rd(x_139)
| p_Reset(x_139) ),
inference(demodulation,[status(thm),theory(equality)],[c_1699,c_2901]) ).
tff(c_2911,plain,
( p_Rd_error(plus(x_139,fifo_length))
| ~ p_Rd(x_139) ),
inference(negUnitSimplification,[status(thm)],[c_321,c_34,c_2910]) ).
tff(c_2912,plain,
~ p_Rd(x_139),
inference(splitLeft,[status(thm)],[c_2911]) ).
tff(c_70,plain,
! [X_t_42_52] :
( ( plus(int_level(X_t_42_52),n1) = int_level(plus(X_t_42_52,n1)) )
| ~ gt(fifo_length,int_level(X_t_42_52))
| p_Rd(X_t_42_52)
| ~ p_Wr(X_t_42_52)
| p_Reset(X_t_42_52) ),
inference(cnfTransformation,[status(thm)],[f_239]) ).
tff(c_4547,plain,
! [X_t_42_337] :
( ( plus(int_level(X_t_42_337),fifo_length) = int_level(plus(X_t_42_337,fifo_length)) )
| ~ gt(fifo_length,int_level(X_t_42_337))
| p_Rd(X_t_42_337)
| ~ p_Wr(X_t_42_337)
| p_Reset(X_t_42_337) ),
inference(demodulation,[status(thm),theory(equality)],[c_1602,c_1602,c_70]) ).
tff(c_4566,plain,
( ( plus(int_level(x_139),fifo_length) = int_level(plus(x_139,fifo_length)) )
| ~ gt(fifo_length,n0)
| p_Rd(x_139)
| ~ p_Wr(x_139)
| p_Reset(x_139) ),
inference(superposition,[status(thm),theory(equality)],[c_1816,c_4547]) ).
tff(c_4579,plain,
( ( int_level(plus(x_139,fifo_length)) = fifo_length )
| p_Rd(x_139)
| p_Reset(x_139) ),
inference(demodulation,[status(thm),theory(equality)],[c_1699,c_186,c_38,c_1816,c_4566]) ).
tff(c_4580,plain,
int_level(plus(x_139,fifo_length)) = fifo_length,
inference(negUnitSimplification,[status(thm)],[c_321,c_2912,c_4579]) ).
tff(c_1685,plain,
gt(int_level(plus(x_139,fifo_length)),fifo_length),
inference(demodulation,[status(thm),theory(equality)],[c_1602,c_188]) ).
tff(c_4587,plain,
gt(fifo_length,fifo_length),
inference(demodulation,[status(thm),theory(equality)],[c_4580,c_1685]) ).
tff(c_4590,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_34,c_4587]) ).
tff(c_4592,plain,
p_Rd(x_139),
inference(splitRight,[status(thm)],[c_2911]) ).
tff(c_118,plain,
! [X_t_42_90] :
( ( plus(int_level(X_t_42_90),n1) = int_level(plus(X_t_42_90,n1)) )
| gt(int_level(X_t_42_90),n0)
| ~ p_Rd(X_t_42_90)
| ~ p_Wr(X_t_42_90)
| p_Reset(X_t_42_90) ),
inference(cnfTransformation,[status(thm)],[f_566]) ).
tff(c_5849,plain,
! [X_t_42_383] :
( ( plus(int_level(X_t_42_383),fifo_length) = int_level(plus(X_t_42_383,fifo_length)) )
| gt(int_level(X_t_42_383),n0)
| ~ p_Rd(X_t_42_383)
| ~ p_Wr(X_t_42_383)
| p_Reset(X_t_42_383) ),
inference(demodulation,[status(thm),theory(equality)],[c_1602,c_1602,c_118]) ).
tff(c_5876,plain,
( ( plus(int_level(x_139),fifo_length) = int_level(plus(x_139,fifo_length)) )
| gt(n0,n0)
| ~ p_Rd(x_139)
| ~ p_Wr(x_139)
| p_Reset(x_139) ),
inference(superposition,[status(thm),theory(equality)],[c_1816,c_5849]) ).
tff(c_5888,plain,
( ( int_level(plus(x_139,fifo_length)) = fifo_length )
| gt(n0,n0)
| p_Reset(x_139) ),
inference(demodulation,[status(thm),theory(equality)],[c_1699,c_4592,c_38,c_1816,c_5876]) ).
tff(c_5889,plain,
int_level(plus(x_139,fifo_length)) = fifo_length,
inference(negUnitSimplification,[status(thm)],[c_321,c_1289,c_5888]) ).
tff(c_5895,plain,
gt(fifo_length,fifo_length),
inference(demodulation,[status(thm),theory(equality)],[c_5889,c_1685]) ).
tff(c_5898,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_34,c_5895]) ).
tff(c_5900,plain,
~ p_Wr(x_139),
inference(splitRight,[status(thm)],[c_1643]) ).
tff(c_1673,plain,
! [X_3_178] :
( ( n0 != X_3_178 )
| def_10(fifo_length,X_3_178) ),
inference(demodulation,[status(thm),theory(equality)],[c_1602,c_537]) ).
tff(c_276,plain,
~ def_10(fifo_length,int_level(plus(x_139,n1))),
inference(resolution,[status(thm)],[c_188,c_12]) ).
tff(c_1683,plain,
~ def_10(fifo_length,int_level(plus(x_139,fifo_length))),
inference(demodulation,[status(thm),theory(equality)],[c_1602,c_276]) ).
tff(c_6275,plain,
int_level(plus(x_139,fifo_length)) != n0,
inference(resolution,[status(thm)],[c_1673,c_1683]) ).
tff(c_5899,plain,
p_Rd(x_139),
inference(splitRight,[status(thm)],[c_1643]) ).
tff(c_5925,plain,
! [Y_16_386] :
( ( n0 = Y_16_386 )
| ~ gt(fifo_length,Y_16_386) ),
inference(demodulation,[status(thm),theory(equality)],[c_1602,c_1321]) ).
tff(c_5959,plain,
int_level(x_139) = n0,
inference(resolution,[status(thm)],[c_463,c_5925]) ).
tff(c_156,plain,
! [X_t_42_119] :
( ( int_level(plus(X_t_42_119,n1)) = int_level(X_t_42_119) )
| gt(int_level(X_t_42_119),n0)
| ~ p_Rd(X_t_42_119)
| p_Wr(X_t_42_119)
| p_Reset(X_t_42_119) ),
inference(cnfTransformation,[status(thm)],[f_812]) ).
tff(c_7723,plain,
! [X_t_42_457] :
( ( int_level(plus(X_t_42_457,fifo_length)) = int_level(X_t_42_457) )
| gt(int_level(X_t_42_457),n0)
| ~ p_Rd(X_t_42_457)
| p_Wr(X_t_42_457)
| p_Reset(X_t_42_457) ),
inference(demodulation,[status(thm),theory(equality)],[c_1602,c_156]) ).
tff(c_7748,plain,
( ( int_level(plus(x_139,fifo_length)) = int_level(x_139) )
| gt(n0,n0)
| ~ p_Rd(x_139)
| p_Wr(x_139)
| p_Reset(x_139) ),
inference(superposition,[status(thm),theory(equality)],[c_5959,c_7723]) ).
tff(c_7758,plain,
( ( int_level(plus(x_139,fifo_length)) = n0 )
| gt(n0,n0)
| p_Wr(x_139)
| p_Reset(x_139) ),
inference(demodulation,[status(thm),theory(equality)],[c_5899,c_5959,c_7748]) ).
tff(c_7760,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_321,c_5900,c_1289,c_6275,c_7758]) ).
tff(c_7761,plain,
gt(fifo_length,n1),
inference(splitRight,[status(thm)],[c_1555]) ).
tff(c_26,plain,
! [Y_20_25,X_19_26,Z_21_24] :
( ~ gt(Y_20_25,X_19_26)
| gt(Z_21_24,X_19_26)
| ~ gt(Z_21_24,Y_20_25) ),
inference(cnfTransformation,[status(thm)],[f_118]) ).
tff(c_7828,plain,
! [Z_21_459] :
( gt(Z_21_459,n1)
| ~ gt(Z_21_459,fifo_length) ),
inference(resolution,[status(thm)],[c_7761,c_26]) ).
tff(c_7893,plain,
! [Z_21_461] :
( ~ def_10(n1,Z_21_461)
| ~ gt(Z_21_461,fifo_length) ),
inference(resolution,[status(thm)],[c_7828,c_12]) ).
tff(c_7912,plain,
~ def_10(n1,int_level(plus(x_139,n1))),
inference(resolution,[status(thm)],[c_188,c_7893]) ).
tff(c_7928,plain,
int_level(plus(x_139,n1)) != n0,
inference(resolution,[status(thm)],[c_537,c_7912]) ).
tff(c_7778,plain,
! [Z_21_24] :
( gt(Z_21_24,n1)
| ~ gt(Z_21_24,fifo_length) ),
inference(resolution,[status(thm)],[c_7761,c_26]) ).
tff(c_382,plain,
! [X_29_166] :
( ( n0 = X_29_166 )
| ( plus(X_29_166,n1) != n1 ) ),
inference(superposition,[status(thm),theory(equality)],[c_38,c_367]) ).
tff(c_385,plain,
! [X_26_30] :
( ( y_27(X_26_30) = n0 )
| ( n1 != X_26_30 )
| ( n0 = X_26_30 ) ),
inference(superposition,[status(thm),theory(equality)],[c_32,c_382]) ).
tff(c_855,plain,
! [Y_12_204,X_11_205] :
( ~ gt(plus(Y_12_204,n1),plus(X_11_205,n1))
| gt(Y_12_204,X_11_205) ),
inference(cnfTransformation,[status(thm)],[f_90]) ).
tff(c_909,plain,
! [Y_12_207] :
( ~ gt(plus(Y_12_207,n1),n1)
| gt(Y_12_207,n0) ),
inference(superposition,[status(thm),theory(equality)],[c_38,c_855]) ).
tff(c_15604,plain,
! [X_26_645] :
( ~ gt(X_26_645,n1)
| gt(y_27(X_26_645),n0)
| ( n0 = X_26_645 ) ),
inference(superposition,[status(thm),theory(equality)],[c_32,c_909]) ).
tff(c_15648,plain,
! [X_26_30] :
( ~ gt(X_26_30,n1)
| gt(n0,n0)
| ( n0 = X_26_30 )
| ( n1 != X_26_30 )
| ( n0 = X_26_30 ) ),
inference(superposition,[status(thm),theory(equality)],[c_385,c_15604]) ).
tff(c_15754,plain,
! [X_26_648] :
( ~ gt(X_26_648,n1)
| ( n0 = X_26_648 )
| ( n1 != X_26_648 )
| ( n0 = X_26_648 ) ),
inference(negUnitSimplification,[status(thm)],[c_1289,c_15648]) ).
tff(c_16241,plain,
! [Z_21_654] :
( ( n1 != Z_21_654 )
| ( n0 = Z_21_654 )
| ~ gt(Z_21_654,fifo_length) ),
inference(resolution,[status(thm)],[c_7778,c_15754]) ).
tff(c_16291,plain,
( ( int_level(plus(x_139,n1)) != n1 )
| ( int_level(plus(x_139,n1)) = n0 ) ),
inference(resolution,[status(thm)],[c_188,c_16241]) ).
tff(c_16316,plain,
int_level(plus(x_139,n1)) != n1,
inference(negUnitSimplification,[status(thm)],[c_7928,c_16291]) ).
tff(c_7783,plain,
! [X_t_42_458] :
( ( int_level(plus(X_t_42_458,n1)) = int_level(X_t_42_458) )
| p_Rd(X_t_42_458)
| p_Wr(X_t_42_458)
| p_Reset(X_t_42_458) ),
inference(cnfTransformation,[status(thm)],[f_856]) ).
tff(c_7801,plain,
( gt(int_level(x_139),fifo_length)
| p_Rd(x_139)
| p_Wr(x_139)
| p_Reset(x_139) ),
inference(superposition,[status(thm),theory(equality)],[c_7783,c_188]) ).
tff(c_7823,plain,
( p_Rd(x_139)
| p_Wr(x_139) ),
inference(negUnitSimplification,[status(thm)],[c_321,c_187,c_7801]) ).
tff(c_7827,plain,
p_Wr(x_139),
inference(splitLeft,[status(thm)],[c_7823]) ).
tff(c_461,plain,
! [X_17_172,Y_18_173] :
( ~ def_10(X_17_172,Y_18_173)
| gt(X_17_172,Y_18_173)
| ( Y_18_173 = X_17_172 ) ),
inference(resolution,[status(thm)],[c_442,c_12]) ).
tff(c_1553,plain,
( ~ def_10(n1,fifo_length)
| ( n1 = fifo_length ) ),
inference(resolution,[status(thm)],[c_461,c_1543]) ).
tff(c_1593,plain,
~ def_10(n1,fifo_length),
inference(splitLeft,[status(thm)],[c_1553]) ).
tff(c_9086,plain,
! [Y_30_164] :
( ( y_27(plus(Y_30_164,n1)) = Y_30_164 )
| ( plus(Y_30_164,n1) = n0 ) ),
inference(reflexivity,[status(thm),theory(equality)],[c_373]) ).
tff(c_9100,plain,
! [Y_30_500] : ( y_27(plus(Y_30_500,n1)) = Y_30_500 ),
inference(negUnitSimplification,[status(thm)],[c_2,c_9086]) ).
tff(c_9220,plain,
! [X_3_502] :
( ( minus(X_3_502,n1) = y_27(X_3_502) )
| def_10(n1,X_3_502) ),
inference(superposition,[status(thm),theory(equality)],[c_8,c_9100]) ).
tff(c_9261,plain,
minus(fifo_length,n1) = y_27(fifo_length),
inference(resolution,[status(thm)],[c_9220,c_1593]) ).
tff(c_9276,plain,
( def_10(n1,fifo_length)
| ( plus(y_27(fifo_length),n1) = fifo_length ) ),
inference(superposition,[status(thm),theory(equality)],[c_9261,c_8]) ).
tff(c_9285,plain,
plus(y_27(fifo_length),n1) = fifo_length,
inference(negUnitSimplification,[status(thm)],[c_1593,c_9276]) ).
tff(c_10590,plain,
! [X_t_42_541] :
( ( int_level(plus(X_t_42_541,n1)) = int_level(X_t_42_541) )
| ~ gt(int_level(X_t_42_541),n0)
| ~ p_Rd(X_t_42_541)
| ~ p_Wr(X_t_42_541)
| p_Reset(X_t_42_541) ),
inference(cnfTransformation,[status(thm)],[f_479]) ).
tff(c_10632,plain,
! [X_t_42_541] :
( ( int_level(plus(X_t_42_541,n1)) = int_level(X_t_42_541) )
| ~ p_Rd(X_t_42_541)
| ~ p_Wr(X_t_42_541)
| p_Reset(X_t_42_541)
| ( int_level(X_t_42_541) = n0 )
| gt(n0,int_level(X_t_42_541)) ),
inference(resolution,[status(thm)],[c_24,c_10590]) ).
tff(c_45487,plain,
! [X_t_42_880] :
( ( int_level(plus(X_t_42_880,n1)) = int_level(X_t_42_880) )
| ~ p_Rd(X_t_42_880)
| ~ p_Wr(X_t_42_880)
| p_Reset(X_t_42_880)
| ( int_level(X_t_42_880) = n0 ) ),
inference(negUnitSimplification,[status(thm)],[c_1289,c_10632]) ).
tff(c_45616,plain,
( gt(int_level(x_139),fifo_length)
| ~ p_Rd(x_139)
| ~ p_Wr(x_139)
| p_Reset(x_139)
| ( int_level(x_139) = n0 ) ),
inference(superposition,[status(thm),theory(equality)],[c_45487,c_188]) ).
tff(c_45721,plain,
( gt(int_level(x_139),fifo_length)
| ~ p_Rd(x_139)
| p_Reset(x_139)
| ( int_level(x_139) = n0 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_7827,c_45616]) ).
tff(c_45722,plain,
( ~ p_Rd(x_139)
| ( int_level(x_139) = n0 ) ),
inference(negUnitSimplification,[status(thm)],[c_321,c_187,c_45721]) ).
tff(c_45733,plain,
~ p_Rd(x_139),
inference(splitLeft,[status(thm)],[c_45722]) ).
tff(c_11057,plain,
! [X_t_42_553] :
( ( plus(int_level(X_t_42_553),n1) = int_level(plus(X_t_42_553,n1)) )
| ~ gt(fifo_length,int_level(X_t_42_553))
| p_Rd(X_t_42_553)
| ~ p_Wr(X_t_42_553)
| p_Reset(X_t_42_553) ),
inference(cnfTransformation,[status(thm)],[f_239]) ).
tff(c_11088,plain,
( ( plus(int_level(x_139),n1) = int_level(plus(x_139,n1)) )
| p_Rd(x_139)
| ~ p_Wr(x_139)
| p_Reset(x_139) ),
inference(resolution,[status(thm)],[c_463,c_11057]) ).
tff(c_11107,plain,
( ( plus(int_level(x_139),n1) = int_level(plus(x_139,n1)) )
| p_Rd(x_139)
| p_Reset(x_139) ),
inference(demodulation,[status(thm),theory(equality)],[c_7827,c_11088]) ).
tff(c_11108,plain,
( ( plus(int_level(x_139),n1) = int_level(plus(x_139,n1)) )
| p_Rd(x_139) ),
inference(negUnitSimplification,[status(thm)],[c_321,c_11107]) ).
tff(c_61261,plain,
plus(int_level(x_139),n1) = int_level(plus(x_139,n1)),
inference(negUnitSimplification,[status(thm)],[c_45733,c_11108]) ).
tff(c_18,plain,
! [Y_12_16,X_11_17] :
( ~ gt(plus(Y_12_16,n1),plus(X_11_17,n1))
| gt(Y_12_16,X_11_17) ),
inference(cnfTransformation,[status(thm)],[f_90]) ).
tff(c_9398,plain,
! [Y_12_16] :
( ~ gt(plus(Y_12_16,n1),fifo_length)
| gt(Y_12_16,y_27(fifo_length)) ),
inference(superposition,[status(thm),theory(equality)],[c_9285,c_18]) ).
tff(c_61407,plain,
( ~ gt(int_level(plus(x_139,n1)),fifo_length)
| gt(int_level(x_139),y_27(fifo_length)) ),
inference(superposition,[status(thm),theory(equality)],[c_61261,c_9398]) ).
tff(c_61722,plain,
gt(int_level(x_139),y_27(fifo_length)),
inference(demodulation,[status(thm),theory(equality)],[c_188,c_61407]) ).
tff(c_8191,plain,
! [Y_24_470,X_23_471] :
( gt(Y_24_470,plus(X_23_471,n1))
| ( plus(X_23_471,n1) = Y_24_470 )
| ~ gt(Y_24_470,X_23_471) ),
inference(cnfTransformation,[status(thm)],[f_125]) ).
tff(c_8236,plain,
! [Y_24_470,X_26_30] :
( gt(Y_24_470,X_26_30)
| ( plus(y_27(X_26_30),n1) = Y_24_470 )
| ~ gt(Y_24_470,y_27(X_26_30))
| ( n0 = X_26_30 ) ),
inference(superposition,[status(thm),theory(equality)],[c_32,c_8191]) ).
tff(c_62275,plain,
( gt(int_level(x_139),fifo_length)
| ( plus(y_27(fifo_length),n1) = int_level(x_139) )
| ( n0 = fifo_length ) ),
inference(resolution,[status(thm)],[c_61722,c_8236]) ).
tff(c_62332,plain,
( gt(int_level(x_139),fifo_length)
| ( int_level(x_139) = fifo_length )
| ( n0 = fifo_length ) ),
inference(demodulation,[status(thm),theory(equality)],[c_9285,c_62275]) ).
tff(c_62333,plain,
int_level(x_139) = fifo_length,
inference(negUnitSimplification,[status(thm)],[c_980,c_187,c_62332]) ).
tff(c_62388,plain,
gt(fifo_length,fifo_length),
inference(demodulation,[status(thm),theory(equality)],[c_62333,c_463]) ).
tff(c_62395,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_34,c_62388]) ).
tff(c_62397,plain,
p_Rd(x_139),
inference(splitRight,[status(thm)],[c_45722]) ).
tff(c_62396,plain,
int_level(x_139) = n0,
inference(splitRight,[status(thm)],[c_45722]) ).
tff(c_62417,plain,
( ( plus(int_level(x_139),n1) = int_level(plus(x_139,n1)) )
| gt(n0,n0)
| ~ p_Rd(x_139)
| ~ p_Wr(x_139)
| p_Reset(x_139) ),
inference(superposition,[status(thm),theory(equality)],[c_62396,c_118]) ).
tff(c_62472,plain,
( ( int_level(plus(x_139,n1)) = n1 )
| gt(n0,n0)
| p_Reset(x_139) ),
inference(demodulation,[status(thm),theory(equality)],[c_7827,c_62397,c_38,c_62396,c_62417]) ).
tff(c_62474,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_321,c_1289,c_16316,c_62472]) ).
tff(c_62476,plain,
~ p_Wr(x_139),
inference(splitRight,[status(thm)],[c_7823]) ).
tff(c_62495,plain,
! [Z_21_979] :
( gt(Z_21_979,n1)
| ~ gt(Z_21_979,fifo_length) ),
inference(resolution,[status(thm)],[c_7761,c_26]) ).
tff(c_62542,plain,
! [Z_21_980] :
( ~ def_10(n1,Z_21_980)
| ~ gt(Z_21_980,fifo_length) ),
inference(resolution,[status(thm)],[c_62495,c_12]) ).
tff(c_62561,plain,
~ def_10(n1,int_level(plus(x_139,n1))),
inference(resolution,[status(thm)],[c_188,c_62542]) ).
tff(c_62577,plain,
int_level(plus(x_139,n1)) != n0,
inference(resolution,[status(thm)],[c_537,c_62561]) ).
tff(c_62475,plain,
p_Rd(x_139),
inference(splitRight,[status(thm)],[c_7823]) ).
tff(c_810,plain,
! [X_17_23,Y_18_22] :
( gt(X_17_23,n0)
| ( n0 = Y_18_22 )
| ( Y_18_22 = X_17_23 )
| gt(Y_18_22,X_17_23) ),
inference(resolution,[status(thm)],[c_24,c_776]) ).
tff(c_65715,plain,
! [X_t_42_1073] :
( ( minus(int_level(X_t_42_1073),n1) = int_level(plus(X_t_42_1073,n1)) )
| ~ gt(int_level(X_t_42_1073),n0)
| ~ p_Rd(X_t_42_1073)
| p_Wr(X_t_42_1073)
| p_Reset(X_t_42_1073) ),
inference(cnfTransformation,[status(thm)],[f_720]) ).
tff(c_65760,plain,
! [X_t_42_1073] :
( ( minus(int_level(X_t_42_1073),n1) = int_level(plus(X_t_42_1073,n1)) )
| ~ p_Rd(X_t_42_1073)
| p_Wr(X_t_42_1073)
| p_Reset(X_t_42_1073)
| ( int_level(X_t_42_1073) = n0 )
| gt(n0,int_level(X_t_42_1073)) ),
inference(resolution,[status(thm)],[c_24,c_65715]) ).
tff(c_65785,plain,
! [X_t_42_1073] :
( ( minus(int_level(X_t_42_1073),n1) = int_level(plus(X_t_42_1073,n1)) )
| ~ p_Rd(X_t_42_1073)
| p_Wr(X_t_42_1073)
| p_Reset(X_t_42_1073)
| ( int_level(X_t_42_1073) = n0 ) ),
inference(negUnitSimplification,[status(thm)],[c_1289,c_65760]) ).
tff(c_6,plain,
! [X_2_3] :
( gt(X_2_3,minus(X_2_3,n1))
| ~ gt(X_2_3,n0) ),
inference(cnfTransformation,[status(thm)],[f_54]) ).
tff(c_76159,plain,
! [Z_21_1229,X_2_1230] :
( gt(Z_21_1229,minus(X_2_1230,n1))
| ~ gt(Z_21_1229,X_2_1230)
| ~ gt(X_2_1230,n0) ),
inference(resolution,[status(thm)],[c_6,c_568]) ).
tff(c_76279,plain,
! [X_2_1231] :
( ~ gt(minus(X_2_1231,n1),X_2_1231)
| ~ gt(X_2_1231,n0) ),
inference(resolution,[status(thm)],[c_76159,c_34]) ).
tff(c_76473,plain,
( ~ gt(int_level(x_139),n0)
| ~ gt(minus(int_level(x_139),n1),fifo_length) ),
inference(resolution,[status(thm)],[c_591,c_76279]) ).
tff(c_149739,plain,
~ gt(minus(int_level(x_139),n1),fifo_length),
inference(splitLeft,[status(thm)],[c_76473]) ).
tff(c_149742,plain,
( ~ gt(int_level(plus(x_139,n1)),fifo_length)
| ~ p_Rd(x_139)
| p_Wr(x_139)
| p_Reset(x_139)
| ( int_level(x_139) = n0 ) ),
inference(superposition,[status(thm),theory(equality)],[c_65785,c_149739]) ).
tff(c_149774,plain,
( p_Wr(x_139)
| p_Reset(x_139)
| ( int_level(x_139) = n0 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_62475,c_188,c_149742]) ).
tff(c_149775,plain,
int_level(x_139) = n0,
inference(negUnitSimplification,[status(thm)],[c_321,c_62476,c_149774]) ).
tff(c_149865,plain,
( ( int_level(plus(x_139,n1)) = int_level(x_139) )
| gt(n0,n0)
| ~ p_Rd(x_139)
| p_Wr(x_139)
| p_Reset(x_139) ),
inference(superposition,[status(thm),theory(equality)],[c_149775,c_156]) ).
tff(c_149945,plain,
( ( int_level(plus(x_139,n1)) = n0 )
| gt(n0,n0)
| p_Wr(x_139)
| p_Reset(x_139) ),
inference(demodulation,[status(thm),theory(equality)],[c_62475,c_149775,c_149865]) ).
tff(c_149947,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_321,c_62476,c_1289,c_62577,c_149945]) ).
tff(c_149948,plain,
~ gt(int_level(x_139),n0),
inference(splitRight,[status(thm)],[c_76473]) ).
tff(c_149973,plain,
( gt(n0,n0)
| ( int_level(x_139) = n0 ) ),
inference(resolution,[status(thm)],[c_810,c_149948]) ).
tff(c_150029,plain,
int_level(x_139) = n0,
inference(negUnitSimplification,[status(thm)],[c_1289,c_149973]) ).
tff(c_150148,plain,
( ( int_level(plus(x_139,n1)) = int_level(x_139) )
| gt(n0,n0)
| ~ p_Rd(x_139)
| p_Wr(x_139)
| p_Reset(x_139) ),
inference(superposition,[status(thm),theory(equality)],[c_150029,c_156]) ).
tff(c_150228,plain,
( ( int_level(plus(x_139,n1)) = n0 )
| gt(n0,n0)
| p_Wr(x_139)
| p_Reset(x_139) ),
inference(demodulation,[status(thm),theory(equality)],[c_62475,c_150029,c_150148]) ).
tff(c_150230,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_321,c_62476,c_1289,c_62577,c_150228]) ).
tff(c_150231,plain,
n1 = fifo_length,
inference(splitRight,[status(thm)],[c_1553]) ).
tff(c_150232,plain,
def_10(n1,fifo_length),
inference(splitRight,[status(thm)],[c_1553]) ).
tff(c_150328,plain,
def_10(fifo_length,fifo_length),
inference(demodulation,[status(thm),theory(equality)],[c_150231,c_150232]) ).
tff(c_150329,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_14,c_150328]) ).
tff(c_150331,plain,
gt(n1,fifo_length),
inference(splitRight,[status(thm)],[c_1455]) ).
tff(c_150384,plain,
n0 = fifo_length,
inference(resolution,[status(thm)],[c_150331,c_1321]) ).
tff(c_150399,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_980,c_150384]) ).
tff(c_150400,plain,
int_level(x_139) = fifo_length,
inference(splitRight,[status(thm)],[c_460]) ).
tff(c_151616,plain,
! [X_t_42_1740] :
( ( int_level(plus(X_t_42_1740,n1)) = int_level(X_t_42_1740) )
| p_Rd(X_t_42_1740)
| p_Wr(X_t_42_1740)
| p_Reset(X_t_42_1740) ),
inference(cnfTransformation,[status(thm)],[f_856]) ).
tff(c_151634,plain,
( gt(int_level(x_139),fifo_length)
| p_Rd(x_139)
| p_Wr(x_139)
| p_Reset(x_139) ),
inference(superposition,[status(thm),theory(equality)],[c_151616,c_188]) ).
tff(c_151659,plain,
( gt(fifo_length,fifo_length)
| p_Rd(x_139)
| p_Wr(x_139)
| p_Reset(x_139) ),
inference(demodulation,[status(thm),theory(equality)],[c_150400,c_151634]) ).
tff(c_151660,plain,
( p_Rd(x_139)
| p_Wr(x_139) ),
inference(negUnitSimplification,[status(thm)],[c_321,c_34,c_151659]) ).
tff(c_151664,plain,
p_Wr(x_139),
inference(splitLeft,[status(thm)],[c_151660]) ).
tff(c_153350,plain,
! [X_t_42_1787] :
( ~ p_Rd_error(plus(X_t_42_1787,n1))
| ~ gt(int_level(X_t_42_1787),n0)
| ~ p_Rd(X_t_42_1787)
| ~ p_Wr(X_t_42_1787)
| p_Reset(X_t_42_1787) ),
inference(cnfTransformation,[status(thm)],[f_466]) ).
tff(c_153383,plain,
( ~ p_Rd_error(plus(x_139,n1))
| ~ gt(fifo_length,n0)
| ~ p_Rd(x_139)
| ~ p_Wr(x_139)
| p_Reset(x_139) ),
inference(superposition,[status(thm),theory(equality)],[c_150400,c_153350]) ).
tff(c_153406,plain,
( ~ p_Rd_error(plus(x_139,n1))
| ~ p_Rd(x_139)
| p_Reset(x_139) ),
inference(demodulation,[status(thm),theory(equality)],[c_151664,c_186,c_153383]) ).
tff(c_153407,plain,
( ~ p_Rd_error(plus(x_139,n1))
| ~ p_Rd(x_139) ),
inference(negUnitSimplification,[status(thm)],[c_321,c_153406]) ).
tff(c_153415,plain,
~ p_Rd(x_139),
inference(splitLeft,[status(thm)],[c_153407]) ).
tff(c_154382,plain,
! [X_t_42_1813] :
( ( int_level(plus(X_t_42_1813,n1)) = int_level(X_t_42_1813) )
| gt(fifo_length,int_level(X_t_42_1813))
| p_Rd(X_t_42_1813)
| ~ p_Wr(X_t_42_1813)
| p_Reset(X_t_42_1813) ),
inference(cnfTransformation,[status(thm)],[f_365]) ).
tff(c_154398,plain,
( ( int_level(plus(x_139,n1)) = int_level(x_139) )
| gt(fifo_length,fifo_length)
| p_Rd(x_139)
| ~ p_Wr(x_139)
| p_Reset(x_139) ),
inference(superposition,[status(thm),theory(equality)],[c_150400,c_154382]) ).
tff(c_154408,plain,
( ( int_level(plus(x_139,n1)) = fifo_length )
| gt(fifo_length,fifo_length)
| p_Rd(x_139)
| p_Reset(x_139) ),
inference(demodulation,[status(thm),theory(equality)],[c_151664,c_150400,c_154398]) ).
tff(c_154409,plain,
int_level(plus(x_139,n1)) = fifo_length,
inference(negUnitSimplification,[status(thm)],[c_321,c_153415,c_34,c_154408]) ).
tff(c_154416,plain,
gt(fifo_length,fifo_length),
inference(demodulation,[status(thm),theory(equality)],[c_154409,c_188]) ).
tff(c_154419,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_34,c_154416]) ).
tff(c_154421,plain,
p_Rd(x_139),
inference(splitRight,[status(thm)],[c_153407]) ).
tff(c_154675,plain,
! [X_t_42_1815] :
( ( int_level(plus(X_t_42_1815,n1)) = int_level(X_t_42_1815) )
| ~ gt(int_level(X_t_42_1815),n0)
| ~ p_Rd(X_t_42_1815)
| ~ p_Wr(X_t_42_1815)
| p_Reset(X_t_42_1815) ),
inference(cnfTransformation,[status(thm)],[f_479]) ).
tff(c_154708,plain,
( ( int_level(plus(x_139,n1)) = int_level(x_139) )
| ~ gt(fifo_length,n0)
| ~ p_Rd(x_139)
| ~ p_Wr(x_139)
| p_Reset(x_139) ),
inference(superposition,[status(thm),theory(equality)],[c_150400,c_154675]) ).
tff(c_154731,plain,
( ( int_level(plus(x_139,n1)) = fifo_length )
| p_Reset(x_139) ),
inference(demodulation,[status(thm),theory(equality)],[c_151664,c_154421,c_186,c_150400,c_154708]) ).
tff(c_154732,plain,
int_level(plus(x_139,n1)) = fifo_length,
inference(negUnitSimplification,[status(thm)],[c_321,c_154731]) ).
tff(c_154745,plain,
gt(fifo_length,fifo_length),
inference(demodulation,[status(thm),theory(equality)],[c_154732,c_188]) ).
tff(c_154748,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_34,c_154745]) ).
tff(c_154750,plain,
~ p_Wr(x_139),
inference(splitRight,[status(thm)],[c_151660]) ).
tff(c_154749,plain,
p_Rd(x_139),
inference(splitRight,[status(thm)],[c_151660]) ).
tff(c_158032,plain,
! [X_t_42_1907] :
( ( minus(int_level(X_t_42_1907),n1) = int_level(plus(X_t_42_1907,n1)) )
| ~ gt(int_level(X_t_42_1907),n0)
| ~ p_Rd(X_t_42_1907)
| p_Wr(X_t_42_1907)
| p_Reset(X_t_42_1907) ),
inference(cnfTransformation,[status(thm)],[f_720]) ).
tff(c_158080,plain,
( ( minus(int_level(x_139),n1) = int_level(plus(x_139,n1)) )
| ~ gt(fifo_length,n0)
| ~ p_Rd(x_139)
| p_Wr(x_139)
| p_Reset(x_139) ),
inference(superposition,[status(thm),theory(equality)],[c_150400,c_158032]) ).
tff(c_158108,plain,
( ( int_level(plus(x_139,n1)) = y_27(fifo_length) )
| p_Wr(x_139)
| p_Reset(x_139) ),
inference(demodulation,[status(thm),theory(equality)],[c_154749,c_186,c_155622,c_150400,c_158080]) ).
tff(c_158109,plain,
int_level(plus(x_139,n1)) = y_27(fifo_length),
inference(negUnitSimplification,[status(thm)],[c_321,c_154750,c_158108]) ).
tff(c_155463,plain,
! [Y_30_164] : ( y_27(plus(Y_30_164,n1)) = Y_30_164 ),
inference(negUnitSimplification,[status(thm)],[c_2,c_155462]) ).
tff(c_156789,plain,
! [X_26_1865] :
( ( y_27(fifo_length) = y_27(X_26_1865) )
| ( fifo_length != X_26_1865 )
| ( n0 = X_26_1865 ) ),
inference(superposition,[status(thm),theory(equality)],[c_155643,c_373]) ).
tff(c_155640,plain,
( gt(fifo_length,y_27(fifo_length))
| ~ gt(fifo_length,n0) ),
inference(superposition,[status(thm),theory(equality)],[c_155622,c_6]) ).
tff(c_155647,plain,
gt(fifo_length,y_27(fifo_length)),
inference(demodulation,[status(thm),theory(equality)],[c_186,c_155640]) ).
tff(c_156188,plain,
! [Z_21_1855] :
( gt(Z_21_1855,y_27(fifo_length))
| ~ gt(Z_21_1855,fifo_length) ),
inference(resolution,[status(thm)],[c_155647,c_26]) ).
tff(c_156233,plain,
~ gt(y_27(fifo_length),fifo_length),
inference(resolution,[status(thm)],[c_156188,c_34]) ).
tff(c_157424,plain,
! [X_26_1888] :
( ~ gt(y_27(X_26_1888),fifo_length)
| ( fifo_length != X_26_1888 )
| ( n0 = X_26_1888 ) ),
inference(superposition,[status(thm),theory(equality)],[c_156789,c_156233]) ).
tff(c_157436,plain,
! [Y_30_164] :
( ~ gt(Y_30_164,fifo_length)
| ( plus(Y_30_164,n1) != fifo_length )
| ( plus(Y_30_164,n1) = n0 ) ),
inference(superposition,[status(thm),theory(equality)],[c_155463,c_157424]) ).
tff(c_157496,plain,
! [Y_30_1890] :
( ~ gt(Y_30_1890,fifo_length)
| ( plus(Y_30_1890,n1) != fifo_length ) ),
inference(negUnitSimplification,[status(thm)],[c_2,c_157436]) ).
tff(c_157538,plain,
plus(int_level(plus(x_139,n1)),n1) != fifo_length,
inference(resolution,[status(thm)],[c_188,c_157496]) ).
tff(c_158117,plain,
plus(y_27(fifo_length),n1) != fifo_length,
inference(demodulation,[status(thm),theory(equality)],[c_158109,c_157538]) ).
tff(c_158126,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_155643,c_158117]) ).
tff(c_158127,plain,
n1 = fifo_length,
inference(splitRight,[status(thm)],[c_154936]) ).
tff(c_158128,plain,
def_10(n1,fifo_length),
inference(splitRight,[status(thm)],[c_154936]) ).
tff(c_158220,plain,
def_10(fifo_length,fifo_length),
inference(demodulation,[status(thm),theory(equality)],[c_158127,c_158128]) ).
tff(c_158221,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_14,c_158220]) ).
tff(c_158222,plain,
gt(n0,fifo_length),
inference(splitRight,[status(thm)],[c_308]) ).
tff(c_158381,plain,
! [Y_20_1926,X_19_1927,Z_21_1928] :
( ~ gt(Y_20_1926,X_19_1927)
| gt(Z_21_1928,X_19_1927)
| ~ gt(Z_21_1928,Y_20_1926) ),
inference(cnfTransformation,[status(thm)],[f_118]) ).
tff(c_158412,plain,
! [Z_21_1929] :
( gt(Z_21_1929,n0)
| ~ gt(Z_21_1929,fifo_length) ),
inference(resolution,[status(thm)],[c_186,c_158381]) ).
tff(c_158421,plain,
~ gt(n0,fifo_length),
inference(resolution,[status(thm)],[c_158412,c_34]) ).
tff(c_158427,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_158222,c_158421]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : HWV029-1 : TPTP v9.0.0. Released v2.5.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.13/0.34 % Computer : n012.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % 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 : Mon Apr 7 22:57:15 EDT 2025
% 0.13/0.34 % CPUTime :
% 32.05/18.97 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 32.24/19.01
% 32.24/19.01 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------