%------------------------------------------------------------------------------
% File : ConnectPP---0.7.2
% Problem : HWV024-1 : TPTP v9.3.1. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n016.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 08:42:39 AM UTC 2026
% Result : Unsatisfiable 0.39s 0.68s
% Output : Proof 0.39s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(axiom_1,axiom,
plus(X_0,n1) != n0,
file('HWV003-0.ax',axiom_1) ).
cnf(axiom_2,axiom,
gt(plus(X_1,n1),n0),
file('HWV003-0.ax',axiom_2) ).
cnf(axiom_3,axiom,
( gt(X_2,minus(X_2,n1))
| ~ gt(X_2,n0) ),
file('HWV003-0.ax',axiom_3) ).
cnf(axiom_4,axiom,
( def_10(Y_4,X_3)
| plus(Z_5,Y_4) = X_3
| minus(X_3,Y_4) != Z_5 ),
file('HWV003-0.ax',axiom_4) ).
cnf(axiom_5,axiom,
( def_10(Y_4,X_3)
| plus(Z_5,Y_4) != X_3
| minus(X_3,Y_4) = Z_5 ),
file('HWV003-0.ax',axiom_5) ).
cnf(axiom_6,axiom,
( ~ gt(X_3,Y_4)
| ~ def_10(Y_4,X_3) ),
file('HWV003-0.ax',axiom_6) ).
cnf(axiom_7,axiom,
( X_3 != Y_4
| ~ def_10(Y_4,X_3) ),
file('HWV003-0.ax',axiom_7) ).
cnf(axiom_8,axiom,
( gt(plus(Y_12,n1),plus(X_11,n1))
| ~ gt(Y_12,X_11) ),
file('HWV003-0.ax',axiom_8) ).
cnf(axiom_9,axiom,
( ~ gt(plus(Y_12,n1),plus(X_11,n1))
| gt(Y_12,X_11) ),
file('HWV003-0.ax',axiom_9) ).
cnf(axiom_10,axiom,
( Y_14 = X_13
| ~ gt(plus(X_13,n1),Y_14)
| gt(X_13,Y_14) ),
file('HWV003-0.ax',axiom_10) ).
cnf(axiom_11,axiom,
( X_15 = Y_16
| gt(X_15,Y_16)
| ~ gt(plus(X_15,n1),Y_16) ),
file('HWV003-0.ax',axiom_11) ).
cnf(axiom_12,axiom,
( gt(X_17,Y_18)
| X_17 = Y_18
| gt(Y_18,X_17) ),
file('HWV003-0.ax',axiom_12) ).
cnf(axiom_13,axiom,
( ~ gt(Y_20,X_19)
| gt(Z_21,X_19)
| ~ gt(Z_21,Y_20) ),
file('HWV003-0.ax',axiom_13) ).
cnf(axiom_14,axiom,
( gt(Y_24,plus(X_23,n1))
| plus(X_23,n1) = Y_24
| ~ gt(Y_24,X_23) ),
file('HWV003-0.ax',axiom_14) ).
cnf(axiom_15,axiom,
( gt(X_25,n0)
| X_25 = n0 ),
file('HWV003-0.ax',axiom_15) ).
cnf(axiom_16,axiom,
( X_26 = plus(y_27(X_26),n1)
| X_26 = n0 ),
file('HWV003-0.ax',axiom_16) ).
cnf(axiom_17,axiom,
~ gt(X_28,X_28),
file('HWV003-0.ax',axiom_17) ).
cnf(axiom_18,axiom,
( X_29 = Y_30
| plus(X_29,n1) != plus(Y_30,n1) ),
file('HWV003-0.ax',axiom_18) ).
cnf(axiom_19,axiom,
plus(n0,X_31) = X_31,
file('HWV003-0.ax',axiom_19) ).
cnf(axiom_20,axiom,
n1 = plus(n0,n1),
file('HWV003-0.ax',axiom_20) ).
cnf(axiom_21,axiom,
level(X_t_32) = int_level(X_t_32),
file('HWV003-0.ax',axiom_21) ).
cnf(axiom_22,axiom,
( p_Full(X_t_33)
| int_level(X_t_33) != fifo_length ),
file('HWV003-0.ax',axiom_22) ).
cnf(axiom_23,axiom,
( ~ p_Full(X_t_34)
| int_level(X_t_34) = fifo_length ),
file('HWV003-0.ax',axiom_23) ).
cnf(axiom_24,axiom,
( p_Empty(X_t_35)
| int_level(X_t_35) != n0 ),
file('HWV003-0.ax',axiom_24) ).
cnf(axiom_25,axiom,
( ~ p_Empty(X_t_36)
| int_level(X_t_36) = n0 ),
file('HWV003-0.ax',axiom_25) ).
cnf(axiom_26,axiom,
( int_level(plus(X_t_37,n1)) = n0
| ~ p_Reset(X_t_37) ),
file('HWV003-0.ax',axiom_26) ).
cnf(axiom_27,axiom,
( wr_level(plus(X_t_37,n1)) = n0
| ~ p_Reset(X_t_37) ),
file('HWV003-0.ax',axiom_27) ).
cnf(axiom_28,axiom,
( rd_level(plus(X_t_37,n1)) = n0
| ~ p_Reset(X_t_37) ),
file('HWV003-0.ax',axiom_28) ).
cnf(axiom_29,axiom,
( ~ p_Wr_error(plus(X_t_37,n1))
| ~ p_Reset(X_t_37) ),
file('HWV003-0.ax',axiom_29) ).
cnf(axiom_30,axiom,
( ~ p_Rd_error(plus(X_t_37,n1))
| ~ p_Reset(X_t_37) ),
file('HWV003-0.ax',axiom_30) ).
cnf(axiom_31,axiom,
( ~ p_Mem(X_k1_38,X_k2_39,plus(X_t_37,n1))
| ~ p_Reset(X_t_37) ),
file('HWV003-0.ax',axiom_31) ).
cnf(axiom_32,axiom,
( ~ p_Data_out(X_k1_40,plus(X_t_37,n1))
| ~ p_Reset(X_t_37) ),
file('HWV003-0.ax',axiom_32) ).
cnf(axiom_33,axiom,
( rd_level(plus(X_t_42,n1)) = rd_level(X_t_42)
| p_Rd(X_t_42)
| ~ p_Wr(X_t_42)
| p_Reset(X_t_42) ),
file('HWV003-0.ax',axiom_33) ).
cnf(axiom_34,axiom,
( ~ p_Wr_error(plus(X_t_42,n1))
| ~ gt(fifo_length,int_level(X_t_42))
| p_Rd(X_t_42)
| ~ p_Wr(X_t_42)
| p_Reset(X_t_42) ),
file('HWV003-0.ax',axiom_34) ).
cnf(axiom_35,axiom,
( int_level(plus(X_t_42,n1)) = plus(int_level(X_t_42),n1)
| ~ gt(fifo_length,int_level(X_t_42))
| p_Rd(X_t_42)
| ~ p_Wr(X_t_42)
| p_Reset(X_t_42) ),
file('HWV003-0.ax',axiom_35) ).
cnf(axiom_36,axiom,
( p_Data_in(X_k1_43,X_t_42)
| ~ p_Mem(wr_level(X_t_42),X_k1_43,plus(X_t_42,n1))
| ~ gt(fifo_length,int_level(X_t_42))
| p_Rd(X_t_42)
| ~ p_Wr(X_t_42)
| p_Reset(X_t_42) ),
file('HWV003-0.ax',axiom_36) ).
cnf(axiom_37,axiom,
( ~ p_Data_in(X_k1_43,X_t_42)
| p_Mem(wr_level(X_t_42),X_k1_43,plus(X_t_42,n1))
| ~ gt(fifo_length,int_level(X_t_42))
| p_Rd(X_t_42)
| ~ p_Wr(X_t_42)
| p_Reset(X_t_42) ),
file('HWV003-0.ax',axiom_37) ).
cnf(axiom_38,axiom,
( p_Mem(X_c1_47,X_k1_48,X_t_42)
| ~ p_Mem(X_c1_47,X_k1_48,plus(X_t_42,n1))
| X_c1_47 = wr_level(X_t_42)
| ~ gt(fifo_length,int_level(X_t_42))
| p_Rd(X_t_42)
| ~ p_Wr(X_t_42)
| p_Reset(X_t_42) ),
file('HWV003-0.ax',axiom_38) ).
cnf(axiom_39,axiom,
( ~ p_Mem(X_c1_47,X_k1_48,X_t_42)
| p_Mem(X_c1_47,X_k1_48,plus(X_t_42,n1))
| X_c1_47 = wr_level(X_t_42)
| ~ gt(fifo_length,int_level(X_t_42))
| p_Rd(X_t_42)
| ~ p_Wr(X_t_42)
| p_Reset(X_t_42) ),
file('HWV003-0.ax',axiom_39) ).
cnf(axiom_40,axiom,
( wr_level(plus(X_t_42,n1)) = plus(wr_level(X_t_42),n1)
| ~ gt(minus(fifo_length,n1),wr_level(X_t_42))
| ~ gt(fifo_length,int_level(X_t_42))
| p_Rd(X_t_42)
| ~ p_Wr(X_t_42)
| p_Reset(X_t_42) ),
file('HWV003-0.ax',axiom_40) ).
cnf(axiom_41,axiom,
( wr_level(plus(X_t_42,n1)) = n0
| gt(minus(fifo_length,n1),wr_level(X_t_42))
| ~ gt(fifo_length,int_level(X_t_42))
| p_Rd(X_t_42)
| ~ p_Wr(X_t_42)
| p_Reset(X_t_42) ),
file('HWV003-0.ax',axiom_41) ).
cnf(axiom_42,axiom,
( p_Wr_error(plus(X_t_42,n1))
| gt(fifo_length,int_level(X_t_42))
| p_Rd(X_t_42)
| ~ p_Wr(X_t_42)
| p_Reset(X_t_42) ),
file('HWV003-0.ax',axiom_42) ).
cnf(axiom_43,axiom,
( wr_level(plus(X_t_42,n1)) = wr_level(X_t_42)
| gt(fifo_length,int_level(X_t_42))
| p_Rd(X_t_42)
| ~ p_Wr(X_t_42)
| p_Reset(X_t_42) ),
file('HWV003-0.ax',axiom_43) ).
cnf(axiom_44,axiom,
( int_level(plus(X_t_42,n1)) = int_level(X_t_42)
| gt(fifo_length,int_level(X_t_42))
| p_Rd(X_t_42)
| ~ p_Wr(X_t_42)
| p_Reset(X_t_42) ),
file('HWV003-0.ax',axiom_44) ).
cnf(axiom_45,axiom,
( p_Mem(X_k1_57,X_k2_58,X_t_42)
| ~ p_Mem(X_k1_57,X_k2_58,plus(X_t_42,n1))
| gt(fifo_length,int_level(X_t_42))
| p_Rd(X_t_42)
| ~ p_Wr(X_t_42)
| p_Reset(X_t_42) ),
file('HWV003-0.ax',axiom_45) ).
cnf(axiom_46,axiom,
( ~ p_Mem(X_k1_57,X_k2_58,X_t_42)
| p_Mem(X_k1_57,X_k2_58,plus(X_t_42,n1))
| gt(fifo_length,int_level(X_t_42))
| p_Rd(X_t_42)
| ~ p_Wr(X_t_42)
| p_Reset(X_t_42) ),
file('HWV003-0.ax',axiom_46) ).
cnf(axiom_47,axiom,
( p_Data_out(X_k1_64,X_t_42)
| ~ p_Data_out(X_k1_64,plus(X_t_42,n1))
| p_Rd(X_t_42)
| ~ p_Wr(X_t_42)
| p_Reset(X_t_42) ),
file('HWV003-0.ax',axiom_47) ).
cnf(axiom_48,axiom,
( ~ p_Data_out(X_k1_64,X_t_42)
| p_Data_out(X_k1_64,plus(X_t_42,n1))
| p_Rd(X_t_42)
| ~ p_Wr(X_t_42)
| p_Reset(X_t_42) ),
file('HWV003-0.ax',axiom_48) ).
cnf(axiom_49,axiom,
( p_Rd_error(X_t_42)
| ~ p_Rd_error(plus(X_t_42,n1))
| p_Rd(X_t_42)
| ~ p_Wr(X_t_42)
| p_Reset(X_t_42) ),
file('HWV003-0.ax',axiom_49) ).
cnf(axiom_50,axiom,
( ~ p_Rd_error(X_t_42)
| p_Rd_error(plus(X_t_42,n1))
| p_Rd(X_t_42)
| ~ p_Wr(X_t_42)
| p_Reset(X_t_42) ),
file('HWV003-0.ax',axiom_50) ).
cnf(axiom_51,axiom,
( ~ p_Wr_error(plus(X_t_42,n1))
| ~ p_Rd(X_t_42)
| ~ p_Wr(X_t_42)
| p_Reset(X_t_42) ),
file('HWV003-0.ax',axiom_51) ).
cnf(axiom_52,axiom,
( ~ p_Rd_error(plus(X_t_42,n1))
| ~ gt(int_level(X_t_42),n0)
| ~ p_Rd(X_t_42)
| ~ p_Wr(X_t_42)
| p_Reset(X_t_42) ),
file('HWV003-0.ax',axiom_52) ).
cnf(axiom_53,axiom,
( int_level(plus(X_t_42,n1)) = int_level(X_t_42)
| ~ gt(int_level(X_t_42),n0)
| ~ p_Rd(X_t_42)
| ~ p_Wr(X_t_42)
| p_Reset(X_t_42) ),
file('HWV003-0.ax',axiom_53) ).
cnf(axiom_54,axiom,
( p_Mem(rd_level(X_t_42),X_k1_73,X_t_42)
| ~ p_Data_out(X_k1_73,plus(X_t_42,n1))
| ~ gt(int_level(X_t_42),n0)
| ~ p_Rd(X_t_42)
| ~ p_Wr(X_t_42)
| p_Reset(X_t_42) ),
file('HWV003-0.ax',axiom_54) ).
cnf(axiom_55,axiom,
( ~ p_Mem(rd_level(X_t_42),X_k1_73,X_t_42)
| p_Data_out(X_k1_73,plus(X_t_42,n1))
| ~ gt(int_level(X_t_42),n0)
| ~ p_Rd(X_t_42)
| ~ p_Wr(X_t_42)
| p_Reset(X_t_42) ),
file('HWV003-0.ax',axiom_55) ).
cnf(axiom_56,axiom,
( rd_level(plus(X_t_42,n1)) = plus(rd_level(X_t_42),n1)
| ~ gt(minus(fifo_length,n1),rd_level(X_t_42))
| ~ gt(int_level(X_t_42),n0)
| ~ p_Rd(X_t_42)
| ~ p_Wr(X_t_42)
| p_Reset(X_t_42) ),
file('HWV003-0.ax',axiom_56) ).
cnf(axiom_57,axiom,
( rd_level(plus(X_t_42,n1)) = n0
| gt(minus(fifo_length,n1),rd_level(X_t_42))
| ~ gt(int_level(X_t_42),n0)
| ~ p_Rd(X_t_42)
| ~ p_Wr(X_t_42)
| p_Reset(X_t_42) ),
file('HWV003-0.ax',axiom_57) ).
cnf(axiom_58,axiom,
( p_Rd_error(plus(X_t_42,n1))
| gt(int_level(X_t_42),n0)
| ~ p_Rd(X_t_42)
| ~ p_Wr(X_t_42)
| p_Reset(X_t_42) ),
file('HWV003-0.ax',axiom_58) ).
cnf(axiom_59,axiom,
( int_level(plus(X_t_42,n1)) = plus(int_level(X_t_42),n1)
| gt(int_level(X_t_42),n0)
| ~ p_Rd(X_t_42)
| ~ p_Wr(X_t_42)
| p_Reset(X_t_42) ),
file('HWV003-0.ax',axiom_59) ).
cnf(axiom_60,axiom,
( rd_level(plus(X_t_42,n1)) = rd_level(X_t_42)
| gt(int_level(X_t_42),n0)
| ~ p_Rd(X_t_42)
| ~ p_Wr(X_t_42)
| p_Reset(X_t_42) ),
file('HWV003-0.ax',axiom_60) ).
cnf(axiom_61,axiom,
( p_Data_out(X_k1_81,X_t_42)
| ~ p_Data_out(X_k1_81,plus(X_t_42,n1))
| gt(int_level(X_t_42),n0)
| ~ p_Rd(X_t_42)
| ~ p_Wr(X_t_42)
| p_Reset(X_t_42) ),
file('HWV003-0.ax',axiom_61) ).
cnf(axiom_62,axiom,
( ~ p_Data_out(X_k1_81,X_t_42)
| p_Data_out(X_k1_81,plus(X_t_42,n1))
| gt(int_level(X_t_42),n0)
| ~ p_Rd(X_t_42)
| ~ p_Wr(X_t_42)
| p_Reset(X_t_42) ),
file('HWV003-0.ax',axiom_62) ).
cnf(axiom_63,axiom,
( p_Data_in(X_k1_87,X_t_42)
| ~ p_Mem(wr_level(X_t_42),X_k1_87,plus(X_t_42,n1))
| ~ p_Rd(X_t_42)
| ~ p_Wr(X_t_42)
| p_Reset(X_t_42) ),
file('HWV003-0.ax',axiom_63) ).
cnf(axiom_64,axiom,
( ~ p_Data_in(X_k1_87,X_t_42)
| p_Mem(wr_level(X_t_42),X_k1_87,plus(X_t_42,n1))
| ~ p_Rd(X_t_42)
| ~ p_Wr(X_t_42)
| p_Reset(X_t_42) ),
file('HWV003-0.ax',axiom_64) ).
cnf(axiom_65,axiom,
( p_Mem(X_c1_91,X_k1_92,X_t_42)
| ~ p_Mem(X_c1_91,X_k1_92,plus(X_t_42,n1))
| X_c1_91 = wr_level(X_t_42)
| ~ p_Rd(X_t_42)
| ~ p_Wr(X_t_42)
| p_Reset(X_t_42) ),
file('HWV003-0.ax',axiom_65) ).
cnf(axiom_66,axiom,
( ~ p_Mem(X_c1_91,X_k1_92,X_t_42)
| p_Mem(X_c1_91,X_k1_92,plus(X_t_42,n1))
| X_c1_91 = wr_level(X_t_42)
| ~ p_Rd(X_t_42)
| ~ p_Wr(X_t_42)
| p_Reset(X_t_42) ),
file('HWV003-0.ax',axiom_66) ).
cnf(axiom_67,axiom,
( wr_level(plus(X_t_42,n1)) = plus(wr_level(X_t_42),n1)
| ~ gt(minus(fifo_length,n1),wr_level(X_t_42))
| ~ p_Rd(X_t_42)
| ~ p_Wr(X_t_42)
| p_Reset(X_t_42) ),
file('HWV003-0.ax',axiom_67) ).
cnf(axiom_68,axiom,
( wr_level(plus(X_t_42,n1)) = n0
| gt(minus(fifo_length,n1),wr_level(X_t_42))
| ~ p_Rd(X_t_42)
| ~ p_Wr(X_t_42)
| p_Reset(X_t_42) ),
file('HWV003-0.ax',axiom_68) ).
cnf(axiom_69,axiom,
( wr_level(plus(X_t_42,n1)) = wr_level(X_t_42)
| p_Wr(X_t_42)
| p_Reset(X_t_42) ),
file('HWV003-0.ax',axiom_69) ).
cnf(axiom_70,axiom,
( ~ p_Rd_error(plus(X_t_42,n1))
| ~ gt(int_level(X_t_42),n0)
| ~ p_Rd(X_t_42)
| p_Wr(X_t_42)
| p_Reset(X_t_42) ),
file('HWV003-0.ax',axiom_70) ).
cnf(axiom_71,axiom,
( int_level(plus(X_t_42,n1)) = minus(int_level(X_t_42),n1)
| ~ gt(int_level(X_t_42),n0)
| ~ p_Rd(X_t_42)
| p_Wr(X_t_42)
| p_Reset(X_t_42) ),
file('HWV003-0.ax',axiom_71) ).
cnf(axiom_72,axiom,
( p_Mem(rd_level(X_t_42),X_k1_103,X_t_42)
| ~ p_Data_out(X_k1_103,plus(X_t_42,n1))
| ~ gt(int_level(X_t_42),n0)
| ~ p_Rd(X_t_42)
| p_Wr(X_t_42)
| p_Reset(X_t_42) ),
file('HWV003-0.ax',axiom_72) ).
cnf(axiom_73,axiom,
( ~ p_Mem(rd_level(X_t_42),X_k1_103,X_t_42)
| p_Data_out(X_k1_103,plus(X_t_42,n1))
| ~ gt(int_level(X_t_42),n0)
| ~ p_Rd(X_t_42)
| p_Wr(X_t_42)
| p_Reset(X_t_42) ),
file('HWV003-0.ax',axiom_73) ).
cnf(axiom_74,axiom,
( rd_level(plus(X_t_42,n1)) = plus(rd_level(X_t_42),n1)
| ~ gt(minus(fifo_length,n1),rd_level(X_t_42))
| ~ gt(int_level(X_t_42),n0)
| ~ p_Rd(X_t_42)
| p_Wr(X_t_42)
| p_Reset(X_t_42) ),
file('HWV003-0.ax',axiom_74) ).
cnf(axiom_75,axiom,
( rd_level(plus(X_t_42,n1)) = n0
| gt(minus(fifo_length,n1),rd_level(X_t_42))
| ~ gt(int_level(X_t_42),n0)
| ~ p_Rd(X_t_42)
| p_Wr(X_t_42)
| p_Reset(X_t_42) ),
file('HWV003-0.ax',axiom_75) ).
cnf(axiom_76,axiom,
( p_Rd_error(plus(X_t_42,n1))
| gt(int_level(X_t_42),n0)
| ~ p_Rd(X_t_42)
| p_Wr(X_t_42)
| p_Reset(X_t_42) ),
file('HWV003-0.ax',axiom_76) ).
cnf(axiom_77,axiom,
( rd_level(plus(X_t_42,n1)) = rd_level(X_t_42)
| gt(int_level(X_t_42),n0)
| ~ p_Rd(X_t_42)
| p_Wr(X_t_42)
| p_Reset(X_t_42) ),
file('HWV003-0.ax',axiom_77) ).
cnf(axiom_78,axiom,
( int_level(plus(X_t_42,n1)) = int_level(X_t_42)
| gt(int_level(X_t_42),n0)
| ~ p_Rd(X_t_42)
| p_Wr(X_t_42)
| p_Reset(X_t_42) ),
file('HWV003-0.ax',axiom_78) ).
cnf(axiom_79,axiom,
( p_Data_out(X_k1_111,X_t_42)
| ~ p_Data_out(X_k1_111,plus(X_t_42,n1))
| gt(int_level(X_t_42),n0)
| ~ p_Rd(X_t_42)
| p_Wr(X_t_42)
| p_Reset(X_t_42) ),
file('HWV003-0.ax',axiom_79) ).
cnf(axiom_80,axiom,
( ~ p_Data_out(X_k1_111,X_t_42)
| p_Data_out(X_k1_111,plus(X_t_42,n1))
| gt(int_level(X_t_42),n0)
| ~ p_Rd(X_t_42)
| p_Wr(X_t_42)
| p_Reset(X_t_42) ),
file('HWV003-0.ax',axiom_80) ).
cnf(axiom_81,axiom,
( rd_level(plus(X_t_42,n1)) = rd_level(X_t_42)
| p_Rd(X_t_42)
| p_Wr(X_t_42)
| p_Reset(X_t_42) ),
file('HWV003-0.ax',axiom_81) ).
cnf(axiom_82,axiom,
( int_level(plus(X_t_42,n1)) = int_level(X_t_42)
| p_Rd(X_t_42)
| p_Wr(X_t_42)
| p_Reset(X_t_42) ),
file('HWV003-0.ax',axiom_82) ).
cnf(axiom_83,axiom,
( p_Data_out(X_k1_119,X_t_42)
| ~ p_Data_out(X_k1_119,plus(X_t_42,n1))
| p_Rd(X_t_42)
| p_Wr(X_t_42)
| p_Reset(X_t_42) ),
file('HWV003-0.ax',axiom_83) ).
cnf(axiom_84,axiom,
( ~ p_Data_out(X_k1_119,X_t_42)
| p_Data_out(X_k1_119,plus(X_t_42,n1))
| p_Rd(X_t_42)
| p_Wr(X_t_42)
| p_Reset(X_t_42) ),
file('HWV003-0.ax',axiom_84) ).
cnf(axiom_85,axiom,
( p_Rd_error(X_t_42)
| ~ p_Rd_error(plus(X_t_42,n1))
| p_Rd(X_t_42)
| p_Wr(X_t_42)
| p_Reset(X_t_42) ),
file('HWV003-0.ax',axiom_85) ).
cnf(axiom_86,axiom,
( ~ p_Rd_error(X_t_42)
| p_Rd_error(plus(X_t_42,n1))
| p_Rd(X_t_42)
| p_Wr(X_t_42)
| p_Reset(X_t_42) ),
file('HWV003-0.ax',axiom_86) ).
cnf(axiom_87,axiom,
( p_Mem(X_k1_128,X_k2_129,X_t_42)
| ~ p_Mem(X_k1_128,X_k2_129,plus(X_t_42,n1))
| p_Wr(X_t_42)
| p_Reset(X_t_42) ),
file('HWV003-0.ax',axiom_87) ).
cnf(axiom_88,axiom,
( ~ p_Mem(X_k1_128,X_k2_129,X_t_42)
| p_Mem(X_k1_128,X_k2_129,plus(X_t_42,n1))
| p_Wr(X_t_42)
| p_Reset(X_t_42) ),
file('HWV003-0.ax',axiom_88) ).
cnf(axiom_89,axiom,
( p_Wr_error(X_t_42)
| ~ p_Wr_error(plus(X_t_42,n1))
| p_Wr(X_t_42)
| p_Reset(X_t_42) ),
file('HWV003-0.ax',axiom_89) ).
cnf(axiom_90,axiom,
( ~ p_Wr_error(X_t_42)
| p_Wr_error(plus(X_t_42,n1))
| p_Wr(X_t_42)
| p_Reset(X_t_42) ),
file('HWV003-0.ax',axiom_90) ).
cnf(quest_1,negated_conjecture,
~ p_Rd(x_140),
file('theBenchmark.p',quest_1) ).
cnf(quest_2,negated_conjecture,
~ p_Reset(x_140),
file('theBenchmark.p',quest_2) ).
cnf(quest_3,negated_conjecture,
( ~ p_Data_out(x_139,plus(x_140,n1))
| ~ p_Data_out(x_139,x_140) ),
file('theBenchmark.p',quest_3) ).
cnf(quest_4,negated_conjecture,
( p_Data_out(x_139,plus(x_140,n1))
| p_Data_out(x_139,x_140) ),
file('theBenchmark.p',quest_4) ).
cnf(equality_1,axiom,
Eq_x_0 = Eq_x_0,
theory(equality,[reflexivity]) ).
cnf(equality_2,axiom,
( Eq_x_1 = Eq_x_0
| Eq_x_0 != Eq_x_1 ),
theory(equality,[symmetry]) ).
cnf(equality_3,axiom,
( Eq_x_0 = Eq_x_2
| Eq_x_1 != Eq_x_2
| Eq_x_0 != Eq_x_1 ),
theory(equality,[transitivity]) ).
cnf(equality_4,axiom,
( plus(Eq_x_0,Eq_x_1) = plus(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_5,axiom,
( minus(Eq_x_0,Eq_x_1) = minus(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_6,axiom,
( y_27(Eq_x_0) = y_27(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_7,axiom,
( level(Eq_x_0) = level(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_8,axiom,
( int_level(Eq_x_0) = int_level(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_9,axiom,
( wr_level(Eq_x_0) = wr_level(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_10,axiom,
( rd_level(Eq_x_0) = rd_level(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_11,axiom,
( gt(Eq_y_0,Eq_y_1)
| ~ gt(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_12,axiom,
( def_10(Eq_y_0,Eq_y_1)
| ~ def_10(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_13,axiom,
( p_Full(Eq_y_0)
| ~ p_Full(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_14,axiom,
( p_Empty(Eq_y_0)
| ~ p_Empty(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_15,axiom,
( p_Reset(Eq_y_0)
| ~ p_Reset(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_16,axiom,
( p_Wr_error(Eq_y_0)
| ~ p_Wr_error(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_17,axiom,
( p_Rd_error(Eq_y_0)
| ~ p_Rd_error(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_18,axiom,
( p_Mem(Eq_y_0,Eq_y_1,Eq_y_2)
| ~ p_Mem(Eq_x_0,Eq_x_1,Eq_x_2)
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_19,axiom,
( p_Data_out(Eq_y_0,Eq_y_1)
| ~ p_Data_out(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_20,axiom,
( p_Wr(Eq_y_0)
| ~ p_Wr(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_21,axiom,
( p_Rd(Eq_y_0)
| ~ p_Rd(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_22,axiom,
( p_Data_in(Eq_y_0,Eq_y_1)
| ~ p_Data_in(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(sat_proved,plain,
$false,
inference(cadical,[status(thm)],[]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : HWV024-1 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.03 This is a CNF_UNS_RFO_SEQ_NHN problem
% 0.00/0.04 % Command : /export/starexec/sandbox/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.35 % Computer : n016.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Sat Sep 19 10:51:34 UTC 2026
% 0.09/0.35 % CPUTime :
% 0.39/0.68 % SZS status Unsatisfiable for theBenchmark
% 0.39/0.68 % SZS output start Proof for theBenchmark
% See solution above
%------------------------------------------------------------------------------