%------------------------------------------------------------------------------
% File : ConnectPP---0.7.2
% Problem : HWV032-2 : 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 : n017.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:41 AM UTC 2026
% Result : Unsatisfiable 30.95s 31.24s
% Output : Proof 30.95s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(axiom_2,axiom,
f__length_(fwork_DOTfifo_DOTrtl_DOTmem_(Vt___)) = f_ADD_(f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,n1),n1),
file('HWV004-0.ax',axiom_2) ).
cnf(axiom_3,axiom,
f__length_(fwork_DOTfifo_DOTrtl_DOTdata__out_(Vt___)) = f_ADD_(f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__width_,n1),n1),
file('HWV004-0.ax',axiom_3) ).
cnf(axiom_4,axiom,
f__length_(fwork_DOTfifo_DOTrtl_DOTdata__in_(Vt___)) = f_ADD_(f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__width_,n1),n1),
file('HWV004-0.ax',axiom_4) ).
cnf(axiom_5,axiom,
fwork_DOTfifo_DOTrtl_DOTlevel_(T_0) = fwork_DOTfifo_DOTrtl_DOTint__level_(T_0),
file('HWV004-0.ax',axiom_5) ).
cnf(axiom_6,axiom,
( fwork_DOTfifo_DOTrtl_DOTint__level_(T_1) != fwork_DOTfifo_DOTrtl_DOTfifo__length_
| p__pred_(fwork_DOTfifo_DOTrtl_DOTfull_(T_1)) ),
file('HWV004-0.ax',axiom_6) ).
cnf(axiom_7,axiom,
( fwork_DOTfifo_DOTrtl_DOTint__level_(T_2) = fwork_DOTfifo_DOTrtl_DOTfifo__length_
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTfull_(T_2)) ),
file('HWV004-0.ax',axiom_7) ).
cnf(axiom_8,axiom,
( fwork_DOTfifo_DOTrtl_DOTint__level_(T_3) != n0
| p__pred_(fwork_DOTfifo_DOTrtl_DOTempty_(T_3)) ),
file('HWV004-0.ax',axiom_8) ).
cnf(axiom_9,axiom,
( fwork_DOTfifo_DOTrtl_DOTint__level_(T_4) = n0
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTempty_(T_4)) ),
file('HWV004-0.ax',axiom_9) ).
cnf(axiom_10,axiom,
( ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(T_5))
| fwork_DOTfifo_DOTrtl_DOTrd__level_(f_ADD_(T_5,n1)) = n0 ),
file('HWV004-0.ax',axiom_10) ).
cnf(axiom_11,axiom,
( ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(T_5))
| fwork_DOTfifo_DOTrtl_DOTwr__level_(f_ADD_(T_5,n1)) = n0 ),
file('HWV004-0.ax',axiom_11) ).
cnf(axiom_12,axiom,
( ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(T_5))
| fwork_DOTfifo_DOTrtl_DOTint__level_(f_ADD_(T_5,n1)) = n0 ),
file('HWV004-0.ax',axiom_12) ).
cnf(axiom_13,axiom,
( ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(T_5))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTwr__error_(f_ADD_(T_5,n1))) ),
file('HWV004-0.ax',axiom_13) ).
cnf(axiom_14,axiom,
( ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(T_5))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTrd__error_(f_ADD_(T_5,n1))) ),
file('HWV004-0.ax',axiom_14) ).
cnf(axiom_15,axiom,
( ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(T_5))
| ~ p_LES_EQU_(I1_6,f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,n1))
| ~ p_LES_EQU_(n0,I1_6)
| ~ p_LES_EQU_(I2_7,f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__width_,n1))
| ~ p_LES_EQU_(n0,I2_7)
| ~ p__pred_(f__index_(f__index_(fwork_DOTfifo_DOTrtl_DOTmem_(f_ADD_(T_5,n1)),I1_6),I2_7)) ),
file('HWV004-0.ax',axiom_15) ).
cnf(axiom_16,axiom,
( ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(T_5))
| ~ p_LES_EQU_(I1_10,f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__width_,n1))
| ~ p_LES_EQU_(n0,I1_10)
| ~ p__pred_(f__index_(fwork_DOTfifo_DOTrtl_DOTdata__out_(f_ADD_(T_5,n1)),I1_10)) ),
file('HWV004-0.ax',axiom_16) ).
cnf(axiom_17,axiom,
( p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(T_13))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(T_13))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(T_13))
| fwork_DOTfifo_DOTrtl_DOTrd__level_(f_ADD_(T_13,n1)) = fwork_DOTfifo_DOTrtl_DOTrd__level_(T_13) ),
file('HWV004-0.ax',axiom_17) ).
cnf(axiom_18,axiom,
( p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(T_13))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(T_13))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(T_13))
| p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,fwork_DOTfifo_DOTrtl_DOTint__level_(T_13))
| fwork_DOTfifo_DOTrtl_DOTint__level_(f_ADD_(T_13,n1)) = f_ADD_(fwork_DOTfifo_DOTrtl_DOTint__level_(T_13),n1) ),
file('HWV004-0.ax',axiom_18) ).
cnf(axiom_19,axiom,
( p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(T_13))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(T_13))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(T_13))
| p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,fwork_DOTfifo_DOTrtl_DOTint__level_(T_13))
| fwork_DOTfifo_DOTrtl_DOTwr__level_(f_ADD_(T_13,n1)) = fstd_DOTstandard_DOTmod_(f_ADD_(fwork_DOTfifo_DOTrtl_DOTwr__level_(T_13),n1),fwork_DOTfifo_DOTrtl_DOTfifo__length_) ),
file('HWV004-0.ax',axiom_19) ).
cnf(axiom_20,axiom,
( p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(T_13))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(T_13))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(T_13))
| p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,fwork_DOTfifo_DOTrtl_DOTint__level_(T_13))
| ~ p_LES_EQU_(I1_14,f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__width_,n1))
| ~ p_LES_EQU_(n0,I1_14)
| f__index_(f__index_(fwork_DOTfifo_DOTrtl_DOTmem_(f_ADD_(T_13,n1)),f_SUB_(f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,n1),fwork_DOTfifo_DOTrtl_DOTwr__level_(T_13))),I1_14) = f__index_(fwork_DOTfifo_DOTrtl_DOTdata__in_(T_13),I1_14) ),
file('HWV004-0.ax',axiom_20) ).
cnf(axiom_21,axiom,
( p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(T_13))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(T_13))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(T_13))
| p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,fwork_DOTfifo_DOTrtl_DOTint__level_(T_13))
| ~ p_LES_EQU_(Cindex_16,f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,n1))
| ~ p_LES_EQU_(n0,Cindex_16)
| Cindex_16 = f_SUB_(f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,n1),fwork_DOTfifo_DOTrtl_DOTwr__level_(T_13))
| ~ p_LES_EQU_(I1_17,f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__width_,n1))
| ~ p_LES_EQU_(n0,I1_17)
| f__index_(f__index_(fwork_DOTfifo_DOTrtl_DOTmem_(f_ADD_(T_13,n1)),Cindex_16),I1_17) = f__index_(f__index_(fwork_DOTfifo_DOTrtl_DOTmem_(T_13),Cindex_16),I1_17) ),
file('HWV004-0.ax',axiom_21) ).
cnf(axiom_22,axiom,
( p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(T_13))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(T_13))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(T_13))
| p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,fwork_DOTfifo_DOTrtl_DOTint__level_(T_13))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTwr__error_(f_ADD_(T_13,n1))) ),
file('HWV004-0.ax',axiom_22) ).
cnf(axiom_23,axiom,
( p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(T_13))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(T_13))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(T_13))
| ~ p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,fwork_DOTfifo_DOTrtl_DOTint__level_(T_13))
| fwork_DOTfifo_DOTrtl_DOTint__level_(f_ADD_(T_13,n1)) = fwork_DOTfifo_DOTrtl_DOTint__level_(T_13) ),
file('HWV004-0.ax',axiom_23) ).
cnf(axiom_24,axiom,
( p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(T_13))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(T_13))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(T_13))
| ~ p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,fwork_DOTfifo_DOTrtl_DOTint__level_(T_13))
| fwork_DOTfifo_DOTrtl_DOTwr__level_(f_ADD_(T_13,n1)) = fwork_DOTfifo_DOTrtl_DOTwr__level_(T_13) ),
file('HWV004-0.ax',axiom_24) ).
cnf(axiom_25,axiom,
( p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(T_13))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(T_13))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(T_13))
| ~ p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,fwork_DOTfifo_DOTrtl_DOTint__level_(T_13))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTwr__error_(f_ADD_(T_13,n1))) ),
file('HWV004-0.ax',axiom_25) ).
cnf(axiom_26,axiom,
( p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(T_13))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(T_13))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(T_13))
| ~ p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,fwork_DOTfifo_DOTrtl_DOTint__level_(T_13))
| ~ p_LES_EQU_(I1_22,f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,n1))
| ~ p_LES_EQU_(n0,I1_22)
| ~ p_LES_EQU_(I2_23,f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__width_,n1))
| ~ p_LES_EQU_(n0,I2_23)
| f__index_(f__index_(fwork_DOTfifo_DOTrtl_DOTmem_(f_ADD_(T_13,n1)),I1_22),I2_23) = f__index_(f__index_(fwork_DOTfifo_DOTrtl_DOTmem_(T_13),I1_22),I2_23) ),
file('HWV004-0.ax',axiom_26) ).
cnf(axiom_27,axiom,
( p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(T_13))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(T_13))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(T_13))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTrd__error_(f_ADD_(T_13,n1)))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTrd__error_(T_13)) ),
file('HWV004-0.ax',axiom_27) ).
cnf(axiom_28,axiom,
( p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(T_13))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(T_13))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(T_13))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTrd__error_(f_ADD_(T_13,n1)))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTrd__error_(T_13)) ),
file('HWV004-0.ax',axiom_28) ).
cnf(axiom_29,axiom,
( p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(T_13))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(T_13))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(T_13))
| ~ p_LES_EQU_(I1_31,f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__width_,n1))
| ~ p_LES_EQU_(n0,I1_31)
| f__index_(fwork_DOTfifo_DOTrtl_DOTdata__out_(f_ADD_(T_13,n1)),I1_31) = f__index_(fwork_DOTfifo_DOTrtl_DOTdata__out_(T_13),I1_31) ),
file('HWV004-0.ax',axiom_29) ).
cnf(axiom_30,axiom,
( p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(T_13))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(T_13))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(T_13))
| fwork_DOTfifo_DOTrtl_DOTwr__level_(f_ADD_(T_13,n1)) = fstd_DOTstandard_DOTmod_(f_ADD_(fwork_DOTfifo_DOTrtl_DOTwr__level_(T_13),n1),fwork_DOTfifo_DOTrtl_DOTfifo__length_) ),
file('HWV004-0.ax',axiom_30) ).
cnf(axiom_31,axiom,
( p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(T_13))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(T_13))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(T_13))
| p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTint__level_(T_13),n0)
| fwork_DOTfifo_DOTrtl_DOTint__level_(f_ADD_(T_13,n1)) = fwork_DOTfifo_DOTrtl_DOTint__level_(T_13) ),
file('HWV004-0.ax',axiom_31) ).
cnf(axiom_32,axiom,
( p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(T_13))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(T_13))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(T_13))
| p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTint__level_(T_13),n0)
| fwork_DOTfifo_DOTrtl_DOTrd__level_(f_ADD_(T_13,n1)) = fstd_DOTstandard_DOTmod_(f_ADD_(fwork_DOTfifo_DOTrtl_DOTrd__level_(T_13),n1),fwork_DOTfifo_DOTrtl_DOTfifo__length_) ),
file('HWV004-0.ax',axiom_32) ).
cnf(axiom_33,axiom,
( p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(T_13))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(T_13))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(T_13))
| p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTint__level_(T_13),n0)
| ~ p_LES_EQU_(I1_35,f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__width_,n1))
| ~ p_LES_EQU_(n0,I1_35)
| f__index_(fwork_DOTfifo_DOTrtl_DOTdata__out_(f_ADD_(T_13,n1)),I1_35) = f__index_(f__index_(fwork_DOTfifo_DOTrtl_DOTmem_(T_13),f_SUB_(f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,n1),fwork_DOTfifo_DOTrtl_DOTrd__level_(T_13))),I1_35) ),
file('HWV004-0.ax',axiom_33) ).
cnf(axiom_34,axiom,
( p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(T_13))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(T_13))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(T_13))
| p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTint__level_(T_13),n0)
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTrd__error_(f_ADD_(T_13,n1))) ),
file('HWV004-0.ax',axiom_34) ).
cnf(axiom_35,axiom,
( p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(T_13))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(T_13))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(T_13))
| ~ p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTint__level_(T_13),n0)
| fwork_DOTfifo_DOTrtl_DOTrd__level_(f_ADD_(T_13,n1)) = fwork_DOTfifo_DOTrtl_DOTrd__level_(T_13) ),
file('HWV004-0.ax',axiom_35) ).
cnf(axiom_36,axiom,
( p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(T_13))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(T_13))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(T_13))
| ~ p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTint__level_(T_13),n0)
| fwork_DOTfifo_DOTrtl_DOTint__level_(f_ADD_(T_13,n1)) = f_ADD_(fwork_DOTfifo_DOTrtl_DOTint__level_(T_13),n1) ),
file('HWV004-0.ax',axiom_36) ).
cnf(axiom_37,axiom,
( p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(T_13))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(T_13))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(T_13))
| ~ p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTint__level_(T_13),n0)
| p__pred_(fwork_DOTfifo_DOTrtl_DOTrd__error_(f_ADD_(T_13,n1))) ),
file('HWV004-0.ax',axiom_37) ).
cnf(axiom_38,axiom,
( p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(T_13))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(T_13))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(T_13))
| ~ p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTint__level_(T_13),n0)
| ~ p_LES_EQU_(I1_39,f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__width_,n1))
| ~ p_LES_EQU_(n0,I1_39)
| f__index_(fwork_DOTfifo_DOTrtl_DOTdata__out_(f_ADD_(T_13,n1)),I1_39) = f__index_(fwork_DOTfifo_DOTrtl_DOTdata__out_(T_13),I1_39) ),
file('HWV004-0.ax',axiom_38) ).
cnf(axiom_39,axiom,
( p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(T_13))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(T_13))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(T_13))
| ~ p_LES_EQU_(I1_43,f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__width_,n1))
| ~ p_LES_EQU_(n0,I1_43)
| f__index_(f__index_(fwork_DOTfifo_DOTrtl_DOTmem_(f_ADD_(T_13,n1)),f_SUB_(f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,n1),fwork_DOTfifo_DOTrtl_DOTwr__level_(T_13))),I1_43) = f__index_(fwork_DOTfifo_DOTrtl_DOTdata__in_(T_13),I1_43) ),
file('HWV004-0.ax',axiom_39) ).
cnf(axiom_40,axiom,
( p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(T_13))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(T_13))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(T_13))
| ~ p_LES_EQU_(Cindex_45,f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,n1))
| ~ p_LES_EQU_(n0,Cindex_45)
| Cindex_45 = f_SUB_(f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,n1),fwork_DOTfifo_DOTrtl_DOTwr__level_(T_13))
| ~ p_LES_EQU_(I1_46,f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__width_,n1))
| ~ p_LES_EQU_(n0,I1_46)
| f__index_(f__index_(fwork_DOTfifo_DOTrtl_DOTmem_(f_ADD_(T_13,n1)),Cindex_45),I1_46) = f__index_(f__index_(fwork_DOTfifo_DOTrtl_DOTmem_(T_13),Cindex_45),I1_46) ),
file('HWV004-0.ax',axiom_40) ).
cnf(axiom_41,axiom,
( p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(T_13))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(T_13))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(T_13))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTwr__error_(f_ADD_(T_13,n1))) ),
file('HWV004-0.ax',axiom_41) ).
cnf(axiom_42,axiom,
( p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(T_13))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(T_13))
| fwork_DOTfifo_DOTrtl_DOTwr__level_(f_ADD_(T_13,n1)) = fwork_DOTfifo_DOTrtl_DOTwr__level_(T_13) ),
file('HWV004-0.ax',axiom_42) ).
cnf(axiom_43,axiom,
( p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(T_13))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(T_13))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(T_13))
| p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTint__level_(T_13),n0)
| fwork_DOTfifo_DOTrtl_DOTint__level_(f_ADD_(T_13,n1)) = f_SUB_(fwork_DOTfifo_DOTrtl_DOTint__level_(T_13),n1) ),
file('HWV004-0.ax',axiom_43) ).
cnf(axiom_44,axiom,
( p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(T_13))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(T_13))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(T_13))
| p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTint__level_(T_13),n0)
| fwork_DOTfifo_DOTrtl_DOTrd__level_(f_ADD_(T_13,n1)) = fstd_DOTstandard_DOTmod_(f_ADD_(fwork_DOTfifo_DOTrtl_DOTrd__level_(T_13),n1),fwork_DOTfifo_DOTrtl_DOTfifo__length_) ),
file('HWV004-0.ax',axiom_44) ).
cnf(axiom_45,axiom,
( p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(T_13))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(T_13))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(T_13))
| p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTint__level_(T_13),n0)
| ~ p_LES_EQU_(I1_53,f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__width_,n1))
| ~ p_LES_EQU_(n0,I1_53)
| f__index_(fwork_DOTfifo_DOTrtl_DOTdata__out_(f_ADD_(T_13,n1)),I1_53) = f__index_(f__index_(fwork_DOTfifo_DOTrtl_DOTmem_(T_13),f_SUB_(f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,n1),fwork_DOTfifo_DOTrtl_DOTrd__level_(T_13))),I1_53) ),
file('HWV004-0.ax',axiom_45) ).
cnf(axiom_46,axiom,
( p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(T_13))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(T_13))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(T_13))
| p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTint__level_(T_13),n0)
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTrd__error_(f_ADD_(T_13,n1))) ),
file('HWV004-0.ax',axiom_46) ).
cnf(axiom_47,axiom,
( p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(T_13))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(T_13))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(T_13))
| ~ p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTint__level_(T_13),n0)
| fwork_DOTfifo_DOTrtl_DOTint__level_(f_ADD_(T_13,n1)) = fwork_DOTfifo_DOTrtl_DOTint__level_(T_13) ),
file('HWV004-0.ax',axiom_47) ).
cnf(axiom_48,axiom,
( p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(T_13))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(T_13))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(T_13))
| ~ p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTint__level_(T_13),n0)
| fwork_DOTfifo_DOTrtl_DOTrd__level_(f_ADD_(T_13,n1)) = fwork_DOTfifo_DOTrtl_DOTrd__level_(T_13) ),
file('HWV004-0.ax',axiom_48) ).
cnf(axiom_49,axiom,
( p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(T_13))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(T_13))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(T_13))
| ~ p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTint__level_(T_13),n0)
| p__pred_(fwork_DOTfifo_DOTrtl_DOTrd__error_(f_ADD_(T_13,n1))) ),
file('HWV004-0.ax',axiom_49) ).
cnf(axiom_50,axiom,
( p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(T_13))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(T_13))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(T_13))
| ~ p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTint__level_(T_13),n0)
| ~ p_LES_EQU_(I1_57,f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__width_,n1))
| ~ p_LES_EQU_(n0,I1_57)
| f__index_(fwork_DOTfifo_DOTrtl_DOTdata__out_(f_ADD_(T_13,n1)),I1_57) = f__index_(fwork_DOTfifo_DOTrtl_DOTdata__out_(T_13),I1_57) ),
file('HWV004-0.ax',axiom_50) ).
cnf(axiom_51,axiom,
( p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(T_13))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(T_13))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(T_13))
| fwork_DOTfifo_DOTrtl_DOTint__level_(f_ADD_(T_13,n1)) = fwork_DOTfifo_DOTrtl_DOTint__level_(T_13) ),
file('HWV004-0.ax',axiom_51) ).
cnf(axiom_52,axiom,
( p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(T_13))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(T_13))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(T_13))
| fwork_DOTfifo_DOTrtl_DOTrd__level_(f_ADD_(T_13,n1)) = fwork_DOTfifo_DOTrtl_DOTrd__level_(T_13) ),
file('HWV004-0.ax',axiom_52) ).
cnf(axiom_53,axiom,
( p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(T_13))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(T_13))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(T_13))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTrd__error_(f_ADD_(T_13,n1)))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTrd__error_(T_13)) ),
file('HWV004-0.ax',axiom_53) ).
cnf(axiom_54,axiom,
( p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(T_13))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(T_13))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(T_13))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTrd__error_(f_ADD_(T_13,n1)))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTrd__error_(T_13)) ),
file('HWV004-0.ax',axiom_54) ).
cnf(axiom_55,axiom,
( p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(T_13))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(T_13))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(T_13))
| ~ p_LES_EQU_(I1_66,f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__width_,n1))
| ~ p_LES_EQU_(n0,I1_66)
| f__index_(fwork_DOTfifo_DOTrtl_DOTdata__out_(f_ADD_(T_13,n1)),I1_66) = f__index_(fwork_DOTfifo_DOTrtl_DOTdata__out_(T_13),I1_66) ),
file('HWV004-0.ax',axiom_55) ).
cnf(axiom_56,axiom,
( p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(T_13))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(T_13))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTwr__error_(f_ADD_(T_13,n1)))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTwr__error_(T_13)) ),
file('HWV004-0.ax',axiom_56) ).
cnf(axiom_57,axiom,
( p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(T_13))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(T_13))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTwr__error_(f_ADD_(T_13,n1)))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTwr__error_(T_13)) ),
file('HWV004-0.ax',axiom_57) ).
cnf(axiom_58,axiom,
( p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(T_13))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(T_13))
| ~ p_LES_EQU_(I1_73,f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,n1))
| ~ p_LES_EQU_(n0,I1_73)
| ~ p_LES_EQU_(I2_74,f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__width_,n1))
| ~ p_LES_EQU_(n0,I2_74)
| f__index_(f__index_(fwork_DOTfifo_DOTrtl_DOTmem_(f_ADD_(T_13,n1)),I1_73),I2_74) = f__index_(f__index_(fwork_DOTfifo_DOTrtl_DOTmem_(T_13),I1_73),I2_74) ),
file('HWV004-0.ax',axiom_58) ).
cnf(axiom_59,axiom,
f_ADD_(X_80,n1) != n0,
file('HWV004-0.ax',axiom_59) ).
cnf(axiom_60,axiom,
~ p_LES_EQU_(f_ADD_(X_81,n1),n0),
file('HWV004-0.ax',axiom_60) ).
cnf(axiom_61,axiom,
( p_LES_EQU_(X_82,n0)
| ~ p_LES_EQU_(X_82,f_SUB_(X_82,n1)) ),
file('HWV004-0.ax',axiom_61) ).
cnf(axiom_62,axiom,
( f_SUB_(X_83,Y_84) != Z_85
| f_ADD_(Z_85,Y_84) = X_83
| def_89(Y_84,X_83) ),
file('HWV004-0.ax',axiom_62) ).
cnf(axiom_63,axiom,
( f_SUB_(X_83,Y_84) = Z_85
| f_ADD_(Z_85,Y_84) != X_83
| def_89(Y_84,X_83) ),
file('HWV004-0.ax',axiom_63) ).
cnf(axiom_64,axiom,
( ~ def_89(Y_84,X_83)
| X_83 != Y_84 ),
file('HWV004-0.ax',axiom_64) ).
cnf(axiom_65,axiom,
( ~ def_89(Y_84,X_83)
| p_LES_EQU_(X_83,Y_84) ),
file('HWV004-0.ax',axiom_65) ).
cnf(axiom_66,axiom,
( p_LES_EQU_(Y_91,X_90)
| ~ p_LES_EQU_(f_ADD_(Y_91,n1),f_ADD_(X_90,n1)) ),
file('HWV004-0.ax',axiom_66) ).
cnf(axiom_67,axiom,
( ~ p_LES_EQU_(Y_91,X_90)
| p_LES_EQU_(f_ADD_(Y_91,n1),f_ADD_(X_90,n1)) ),
file('HWV004-0.ax',axiom_67) ).
cnf(axiom_68,axiom,
( p_LES_EQU_(f_ADD_(X_92,n1),Y_93)
| ~ p_LES_EQU_(X_92,Y_93)
| Y_93 = X_92 ),
file('HWV004-0.ax',axiom_68) ).
cnf(axiom_69,axiom,
( p_LES_EQU_(f_ADD_(X_94,n1),Y_95)
| X_94 = Y_95
| ~ p_LES_EQU_(X_94,Y_95) ),
file('HWV004-0.ax',axiom_69) ).
cnf(axiom_70,axiom,
( ~ p_LES_EQU_(Y_97,X_96)
| ~ p_LES_EQU_(X_96,Y_97)
| X_96 = Y_97 ),
file('HWV004-0.ax',axiom_70) ).
cnf(axiom_71,axiom,
( p_LES_EQU_(Z_100,Y_99)
| p_LES_EQU_(Y_99,X_98)
| ~ p_LES_EQU_(Z_100,X_98) ),
file('HWV004-0.ax',axiom_71) ).
cnf(axiom_72,axiom,
( p_LES_EQU_(Y_102,X_101)
| ~ p_LES_EQU_(Y_102,f_ADD_(X_101,n1))
| f_ADD_(X_101,n1) = Y_102 ),
file('HWV004-0.ax',axiom_72) ).
cnf(axiom_73,axiom,
( X_103 = n0
| ~ p_LES_EQU_(X_103,n0) ),
file('HWV004-0.ax',axiom_73) ).
cnf(axiom_74,axiom,
( X_104 = n0
| X_104 = f_ADD_(y_105(X_104),n1) ),
file('HWV004-0.ax',axiom_74) ).
cnf(axiom_75,axiom,
p_LES_EQU_(X_106,X_106),
file('HWV004-0.ax',axiom_75) ).
cnf(axiom_76,axiom,
( f_ADD_(X_107,n1) != f_ADD_(Y_108,n1)
| X_107 = Y_108 ),
file('HWV004-0.ax',axiom_76) ).
cnf(axiom_77,axiom,
f_ADD_(n0,X_109) = X_109,
file('HWV004-0.ax',axiom_77) ).
cnf(axiom_78,axiom,
n1 = f_ADD_(n0,n1),
file('HWV004-0.ax',axiom_78) ).
cnf(axiom_79,axiom,
f__length_(f__cons_(X_110,Xs_111)) = f_ADD_(f__length_(Xs_111),n1),
file('HWV004-0.ax',axiom_79) ).
cnf(axiom_80,axiom,
f__length_(f__empty_) = n0,
file('HWV004-0.ax',axiom_80) ).
cnf(axiom_81,axiom,
f__length_(f__concat_(A_112,B_113)) = f_ADD_(f__length_(A_112),f__length_(B_113)),
file('HWV004-0.ax',axiom_81) ).
cnf(axiom_82,axiom,
f__length_(f__slice_(A_114,I1_115,I2_116)) = f_SUB_(I2_116,f_ADD_(I1_115,n1)),
file('HWV004-0.ax',axiom_82) ).
cnf(axiom_83,axiom,
f__index_(f__others_(E_117),I_118) = E_117,
file('HWV004-0.ax',axiom_83) ).
cnf(axiom_84,axiom,
( f__index_(f__cons_(X_120,Xs_121),I_119) = X_120
| I_119 != n0 ),
file('HWV004-0.ax',axiom_84) ).
cnf(axiom_85,axiom,
( f__index_(f__cons_(X_123,Xs_124),I_122) = f__index_(Xs_124,f_SUB_(I_122,n1))
| p_LES_EQU_(I_122,n0) ),
file('HWV004-0.ax',axiom_85) ).
cnf(axiom_86,axiom,
( f__index_(f__concat_(A_126,B_127),I_125) = f__index_(A_126,I_125)
| p_LES_EQU_(length(A_126),I_125) ),
file('HWV004-0.ax',axiom_86) ).
cnf(axiom_87,axiom,
( f__index_(f__concat_(A_129,B_130),I_128) = f__index_(B_130,f_SUB_(I_128,length(A_129)))
| ~ p_LES_EQU_(length(A_129),I_128) ),
file('HWV004-0.ax',axiom_87) ).
cnf(axiom_88,axiom,
f__index_(f__slice_(A_131,I1_132,I2_133),I_134) = f__index_(A_131,f_ADD_(I_134,I1_132)),
file('HWV004-0.ax',axiom_88) ).
cnf(axiom_89,axiom,
f__index_(f__and_(A_135,B_136),X_137) = f__and_(f__index_(A_135,X_137),f__index_(B_136,X_137)),
file('HWV004-0.ax',axiom_89) ).
cnf(axiom_90,axiom,
f__index_(f__or_(A_138,B_139),X_140) = f__or_(f__index_(A_138,X_140),f__index_(B_139,X_140)),
file('HWV004-0.ax',axiom_90) ).
cnf(axiom_91,axiom,
f__index_(f__xor_(A_141,B_142),X_143) = f__xor_(f__index_(A_141,X_143),f__index_(B_142,X_143)),
file('HWV004-0.ax',axiom_91) ).
cnf(axiom_92,axiom,
f__index_(f__nand_(A_144,B_145),X_146) = f__nand_(f__index_(A_144,X_146),f__index_(B_145,X_146)),
file('HWV004-0.ax',axiom_92) ).
cnf(axiom_93,axiom,
f__index_(f__nor_(A_147,B_148),X_149) = f__nor_(f__index_(A_147,X_149),f__index_(B_148,X_149)),
file('HWV004-0.ax',axiom_93) ).
cnf(axiom_94,axiom,
f__index_(f__xnor_(A_150,B_151),X_152) = f__xnor_(f__index_(A_150,X_152),f__index_(B_151,X_152)),
file('HWV004-0.ax',axiom_94) ).
cnf(axiom_95,axiom,
f__index_(f__not_(A_153),X_154) = f__not_(f__index_(A_153,X_154)),
file('HWV004-0.ax',axiom_95) ).
cnf(axiom_96,axiom,
p__pred_(f__true_),
file('HWV004-0.ax',axiom_96) ).
cnf(axiom_97,axiom,
~ p__pred_(f__false_),
file('HWV004-0.ax',axiom_97) ).
cnf(axiom_98,axiom,
f__false_ != f__true_,
file('HWV004-0.ax',axiom_98) ).
cnf(axiom_99,axiom,
( ~ p__pred_(f__equiv_(A_155,B_156))
| ~ p__pred_(A_155)
| p__pred_(B_156) ),
file('HWV004-0.ax',axiom_99) ).
cnf(axiom_100,axiom,
( ~ p__pred_(f__equiv_(A_155,B_156))
| p__pred_(A_155)
| ~ p__pred_(B_156) ),
file('HWV004-0.ax',axiom_100) ).
cnf(axiom_101,axiom,
( p__pred_(f__equiv_(A_155,B_156))
| ~ p__pred_(A_155)
| ~ p__pred_(B_156) ),
file('HWV004-0.ax',axiom_101) ).
cnf(axiom_102,axiom,
( p__pred_(f__equiv_(A_155,B_156))
| p__pred_(A_155)
| p__pred_(B_156) ),
file('HWV004-0.ax',axiom_102) ).
cnf(axiom_103,axiom,
( ~ p__pred_(f__equal_(A_163,B_164))
| A_163 = B_164 ),
file('HWV004-0.ax',axiom_103) ).
cnf(axiom_104,axiom,
( p__pred_(f__equal_(A_163,B_164))
| A_163 != B_164 ),
file('HWV004-0.ax',axiom_104) ).
cnf(axiom_105,axiom,
( ~ p__pred_(f__and_(A_165,B_166))
| p__pred_(B_166) ),
file('HWV004-0.ax',axiom_105) ).
cnf(axiom_106,axiom,
( ~ p__pred_(f__and_(A_165,B_166))
| p__pred_(A_165) ),
file('HWV004-0.ax',axiom_106) ).
cnf(axiom_107,axiom,
( p__pred_(f__and_(A_165,B_166))
| ~ p__pred_(B_166)
| ~ p__pred_(A_165) ),
file('HWV004-0.ax',axiom_107) ).
cnf(axiom_108,axiom,
( ~ p__pred_(f__or_(A_169,B_170))
| p__pred_(B_170)
| p__pred_(A_169) ),
file('HWV004-0.ax',axiom_108) ).
cnf(axiom_109,axiom,
( p__pred_(f__or_(A_169,B_170))
| ~ p__pred_(B_170) ),
file('HWV004-0.ax',axiom_109) ).
cnf(axiom_110,axiom,
( p__pred_(f__or_(A_169,B_170))
| ~ p__pred_(A_169) ),
file('HWV004-0.ax',axiom_110) ).
cnf(axiom_111,axiom,
( ~ p__pred_(f__xor_(A_173,B_174))
| ~ p__pred_(A_173)
| ~ p__pred_(B_174) ),
file('HWV004-0.ax',axiom_111) ).
cnf(axiom_112,axiom,
( ~ p__pred_(f__xor_(A_173,B_174))
| p__pred_(A_173)
| p__pred_(B_174) ),
file('HWV004-0.ax',axiom_112) ).
cnf(axiom_113,axiom,
( p__pred_(f__xor_(A_173,B_174))
| ~ p__pred_(A_173)
| p__pred_(B_174) ),
file('HWV004-0.ax',axiom_113) ).
cnf(axiom_114,axiom,
( p__pred_(f__xor_(A_173,B_174))
| p__pred_(A_173)
| ~ p__pred_(B_174) ),
file('HWV004-0.ax',axiom_114) ).
cnf(axiom_115,axiom,
( ~ p__pred_(f__nand_(A_181,B_182))
| ~ p__pred_(B_182)
| ~ p__pred_(A_181) ),
file('HWV004-0.ax',axiom_115) ).
cnf(axiom_116,axiom,
( p__pred_(f__nand_(A_181,B_182))
| p__pred_(B_182) ),
file('HWV004-0.ax',axiom_116) ).
cnf(axiom_117,axiom,
( p__pred_(f__nand_(A_181,B_182))
| p__pred_(A_181) ),
file('HWV004-0.ax',axiom_117) ).
cnf(axiom_118,axiom,
( ~ p__pred_(f__nor_(A_185,B_186))
| ~ p__pred_(B_186) ),
file('HWV004-0.ax',axiom_118) ).
cnf(axiom_119,axiom,
( ~ p__pred_(f__nor_(A_185,B_186))
| ~ p__pred_(A_185) ),
file('HWV004-0.ax',axiom_119) ).
cnf(axiom_120,axiom,
( p__pred_(f__nor_(A_185,B_186))
| p__pred_(B_186)
| p__pred_(A_185) ),
file('HWV004-0.ax',axiom_120) ).
cnf(axiom_121,axiom,
( ~ p__pred_(f__xnor_(A_189,B_190))
| ~ p__pred_(A_189)
| p__pred_(B_190) ),
file('HWV004-0.ax',axiom_121) ).
cnf(axiom_122,axiom,
( ~ p__pred_(f__xnor_(A_189,B_190))
| p__pred_(A_189)
| ~ p__pred_(B_190) ),
file('HWV004-0.ax',axiom_122) ).
cnf(axiom_123,axiom,
( p__pred_(f__xnor_(A_189,B_190))
| ~ p__pred_(A_189)
| ~ p__pred_(B_190) ),
file('HWV004-0.ax',axiom_123) ).
cnf(axiom_124,axiom,
( p__pred_(f__xnor_(A_189,B_190))
| p__pred_(A_189)
| p__pred_(B_190) ),
file('HWV004-0.ax',axiom_124) ).
cnf(axiom_125,axiom,
( ~ p__pred_(f__not_(A_197))
| ~ p__pred_(A_197) ),
file('HWV004-0.ax',axiom_125) ).
cnf(axiom_126,axiom,
( p__pred_(f__not_(A_197))
| p__pred_(A_197) ),
file('HWV004-0.ax',axiom_126) ).
cnf(axiom_127,axiom,
( ~ p__pred_(f__lt_(A_198,B_199))
| ~ p_LES_EQU_(B_199,A_198) ),
file('HWV004-0.ax',axiom_127) ).
cnf(axiom_128,axiom,
( p__pred_(f__lt_(A_198,B_199))
| p_LES_EQU_(B_199,A_198) ),
file('HWV004-0.ax',axiom_128) ).
cnf(axiom_129,axiom,
( ~ p__pred_(f__leq_(A_200,B_201))
| p_LES_EQU_(A_200,B_201) ),
file('HWV004-0.ax',axiom_129) ).
cnf(axiom_130,axiom,
( p__pred_(f__leq_(A_200,B_201))
| ~ p_LES_EQU_(A_200,B_201) ),
file('HWV004-0.ax',axiom_130) ).
cnf(axiom_131,axiom,
( ~ p__pred_(f__gt_(A_202,B_203))
| ~ p_LES_EQU_(A_202,B_203) ),
file('HWV004-0.ax',axiom_131) ).
cnf(axiom_132,axiom,
( p__pred_(f__gt_(A_202,B_203))
| p_LES_EQU_(A_202,B_203) ),
file('HWV004-0.ax',axiom_132) ).
cnf(axiom_133,axiom,
( ~ p__pred_(f__geq_(A_204,B_205))
| p_LES_EQU_(B_205,A_204) ),
file('HWV004-0.ax',axiom_133) ).
cnf(axiom_134,axiom,
( p__pred_(f__geq_(A_204,B_205))
| ~ p_LES_EQU_(B_205,A_204) ),
file('HWV004-0.ax',axiom_134) ).
cnf(quest_1,negated_conjecture,
p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(t_206)),
file('theBenchmark.p',quest_1) ).
cnf(quest_2,negated_conjecture,
p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,fwork_DOTfifo_DOTrtl_DOTrd__level_(f_ADD_(t_206,n1))),
file('theBenchmark.p',quest_2) ).
cnf(quest_3,negated_conjecture,
~ p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,n0),
file('theBenchmark.p',quest_3) ).
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,
( fwork_DOTfifo_DOTrtl_DOTmem_(Eq_x_0) = fwork_DOTfifo_DOTrtl_DOTmem_(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_5,axiom,
( f__length_(Eq_x_0) = f__length_(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_6,axiom,
( f_SUB_(Eq_x_0,Eq_x_1) = f_SUB_(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_7,axiom,
( f_ADD_(Eq_x_0,Eq_x_1) = f_ADD_(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_8,axiom,
( fwork_DOTfifo_DOTrtl_DOTdata__out_(Eq_x_0) = fwork_DOTfifo_DOTrtl_DOTdata__out_(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_9,axiom,
( fwork_DOTfifo_DOTrtl_DOTdata__in_(Eq_x_0) = fwork_DOTfifo_DOTrtl_DOTdata__in_(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_10,axiom,
( fwork_DOTfifo_DOTrtl_DOTlevel_(Eq_x_0) = fwork_DOTfifo_DOTrtl_DOTlevel_(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_11,axiom,
( fwork_DOTfifo_DOTrtl_DOTint__level_(Eq_x_0) = fwork_DOTfifo_DOTrtl_DOTint__level_(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_12,axiom,
( fwork_DOTfifo_DOTrtl_DOTfull_(Eq_x_0) = fwork_DOTfifo_DOTrtl_DOTfull_(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_13,axiom,
( fwork_DOTfifo_DOTrtl_DOTempty_(Eq_x_0) = fwork_DOTfifo_DOTrtl_DOTempty_(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_14,axiom,
( fwork_DOTfifo_DOTrtl_DOTrd__level_(Eq_x_0) = fwork_DOTfifo_DOTrtl_DOTrd__level_(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_15,axiom,
( fwork_DOTfifo_DOTrtl_DOTreset_(Eq_x_0) = fwork_DOTfifo_DOTrtl_DOTreset_(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_16,axiom,
( fwork_DOTfifo_DOTrtl_DOTwr__level_(Eq_x_0) = fwork_DOTfifo_DOTrtl_DOTwr__level_(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_17,axiom,
( fwork_DOTfifo_DOTrtl_DOTwr__error_(Eq_x_0) = fwork_DOTfifo_DOTrtl_DOTwr__error_(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_18,axiom,
( fwork_DOTfifo_DOTrtl_DOTrd__error_(Eq_x_0) = fwork_DOTfifo_DOTrtl_DOTrd__error_(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_19,axiom,
( f__index_(Eq_x_0,Eq_x_1) = f__index_(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_20,axiom,
( fwork_DOTfifo_DOTrtl_DOTrd_(Eq_x_0) = fwork_DOTfifo_DOTrtl_DOTrd_(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_21,axiom,
( fwork_DOTfifo_DOTrtl_DOTwr_(Eq_x_0) = fwork_DOTfifo_DOTrtl_DOTwr_(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_22,axiom,
( fstd_DOTstandard_DOTmod_(Eq_x_0,Eq_x_1) = fstd_DOTstandard_DOTmod_(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_23,axiom,
( y_105(Eq_x_0) = y_105(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_24,axiom,
( f__cons_(Eq_x_0,Eq_x_1) = f__cons_(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_25,axiom,
( f__concat_(Eq_x_0,Eq_x_1) = f__concat_(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_26,axiom,
( f__slice_(Eq_x_0,Eq_x_1,Eq_x_2) = f__slice_(Eq_y_0,Eq_y_1,Eq_y_2)
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_27,axiom,
( f__others_(Eq_x_0) = f__others_(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_28,axiom,
( length(Eq_x_0) = length(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_29,axiom,
( f__and_(Eq_x_0,Eq_x_1) = f__and_(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_30,axiom,
( f__or_(Eq_x_0,Eq_x_1) = f__or_(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_31,axiom,
( f__xor_(Eq_x_0,Eq_x_1) = f__xor_(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_32,axiom,
( f__nand_(Eq_x_0,Eq_x_1) = f__nand_(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_33,axiom,
( f__nor_(Eq_x_0,Eq_x_1) = f__nor_(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_34,axiom,
( f__xnor_(Eq_x_0,Eq_x_1) = f__xnor_(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_35,axiom,
( f__not_(Eq_x_0) = f__not_(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_36,axiom,
( f__equiv_(Eq_x_0,Eq_x_1) = f__equiv_(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_37,axiom,
( f__equal_(Eq_x_0,Eq_x_1) = f__equal_(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_38,axiom,
( f__lt_(Eq_x_0,Eq_x_1) = f__lt_(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_39,axiom,
( f__leq_(Eq_x_0,Eq_x_1) = f__leq_(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_40,axiom,
( f__gt_(Eq_x_0,Eq_x_1) = f__gt_(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_41,axiom,
( f__geq_(Eq_x_0,Eq_x_1) = f__geq_(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_42,axiom,
( p__pred_(Eq_y_0)
| ~ p__pred_(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_43,axiom,
( p_LES_EQU_(Eq_y_0,Eq_y_1)
| ~ p_LES_EQU_(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_44,axiom,
( def_89(Eq_y_0,Eq_y_1)
| ~ def_89(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.03 % Problem : HWV032-2 : 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.11/0.37 % Computer : n017.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.37 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Sat Sep 19 10:43:24 UTC 2026
% 0.11/0.37 % CPUTime :
% 30.95/31.24 % SZS status Unsatisfiable for theBenchmark
% 30.95/31.24 % SZS output start Proof for theBenchmark
% See solution above
%------------------------------------------------------------------------------