%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : HWV026-3 : TPTP v9.2.1. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox/solver/bin/cse --final-prover /export/starexec/sandbox/solver/bin/eprover --proof-time %d --global-time-limit %d
% Computer : n005.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue May 5 04:29:00 PM UTC 2026
% Result : Unsatisfiable 0.33s 1.62s
% Output : CNFRefutation 0.33s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named c_0_138)
% Comments :
%------------------------------------------------------------------------------
cnf(axiom_20,axiom,
( f__index_(f__index_(fwork_DOTfifo_DOTrtl_DOTmem_(f_ADD_(X1,n1)),f_SUB_(f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,n1),fwork_DOTfifo_DOTrtl_DOTwr__level_(X1))),X2) = f__index_(fwork_DOTfifo_DOTrtl_DOTdata__in_(X1),X2)
| p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,fwork_DOTfifo_DOTrtl_DOTint__level_(X1))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(X1))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X1))
| ~ p_LES_EQU_(n0,X2)
| ~ p_LES_EQU_(X2,f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__width_,n1))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X1)) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV004-0.ax',axiom_20) ).
cnf(axiom_5,axiom,
fwork_DOTfifo_DOTrtl_DOTlevel_(X1) = fwork_DOTfifo_DOTrtl_DOTint__level_(X1),
file('/export/starexec/sandbox/benchmark/Axioms/HWV004-0.ax',axiom_5) ).
cnf(axiom_21,axiom,
( f__index_(f__index_(fwork_DOTfifo_DOTrtl_DOTmem_(f_ADD_(X1,n1)),X2),X3) = f__index_(f__index_(fwork_DOTfifo_DOTrtl_DOTmem_(X1),X2),X3)
| X2 = f_SUB_(f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,n1),fwork_DOTfifo_DOTrtl_DOTwr__level_(X1))
| p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,fwork_DOTfifo_DOTrtl_DOTint__level_(X1))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(X1))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X1))
| ~ p_LES_EQU_(n0,X3)
| ~ p_LES_EQU_(X3,f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__width_,n1))
| ~ p_LES_EQU_(n0,X2)
| ~ p_LES_EQU_(X2,f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,n1))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X1)) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV004-0.ax',axiom_21) ).
cnf(axiom_26,axiom,
( f__index_(f__index_(fwork_DOTfifo_DOTrtl_DOTmem_(f_ADD_(X1,n1)),X2),X3) = f__index_(f__index_(fwork_DOTfifo_DOTrtl_DOTmem_(X1),X2),X3)
| p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(X1))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X1))
| ~ p_LES_EQU_(n0,X3)
| ~ p_LES_EQU_(X3,f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__width_,n1))
| ~ p_LES_EQU_(n0,X2)
| ~ p_LES_EQU_(X2,f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,n1))
| ~ p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,fwork_DOTfifo_DOTrtl_DOTint__level_(X1))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X1)) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV004-0.ax',axiom_26) ).
cnf(axiom_33,axiom,
( f__index_(fwork_DOTfifo_DOTrtl_DOTdata__out_(f_ADD_(X1,n1)),X2) = f__index_(f__index_(fwork_DOTfifo_DOTrtl_DOTmem_(X1),f_SUB_(f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,n1),fwork_DOTfifo_DOTrtl_DOTrd__level_(X1))),X2)
| p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTint__level_(X1),n0)
| p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X1))
| ~ p_LES_EQU_(n0,X2)
| ~ p_LES_EQU_(X2,f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__width_,n1))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(X1))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X1)) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV004-0.ax',axiom_33) ).
cnf(axiom_45,axiom,
( f__index_(fwork_DOTfifo_DOTrtl_DOTdata__out_(f_ADD_(X1,n1)),X2) = f__index_(f__index_(fwork_DOTfifo_DOTrtl_DOTmem_(X1),f_SUB_(f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,n1),fwork_DOTfifo_DOTrtl_DOTrd__level_(X1))),X2)
| p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTint__level_(X1),n0)
| p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X1))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X1))
| ~ p_LES_EQU_(n0,X2)
| ~ p_LES_EQU_(X2,f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__width_,n1))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(X1)) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV004-0.ax',axiom_45) ).
cnf(axiom_38,axiom,
( f__index_(fwork_DOTfifo_DOTrtl_DOTdata__out_(f_ADD_(X1,n1)),X2) = f__index_(fwork_DOTfifo_DOTrtl_DOTdata__out_(X1),X2)
| p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X1))
| ~ p_LES_EQU_(n0,X2)
| ~ p_LES_EQU_(X2,f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__width_,n1))
| ~ p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTint__level_(X1),n0)
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(X1))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X1)) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV004-0.ax',axiom_38) ).
cnf(axiom_50,axiom,
( f__index_(fwork_DOTfifo_DOTrtl_DOTdata__out_(f_ADD_(X1,n1)),X2) = f__index_(fwork_DOTfifo_DOTrtl_DOTdata__out_(X1),X2)
| p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X1))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X1))
| ~ p_LES_EQU_(n0,X2)
| ~ p_LES_EQU_(X2,f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__width_,n1))
| ~ p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTint__level_(X1),n0)
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(X1)) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV004-0.ax',axiom_50) ).
cnf(axiom_34,axiom,
( p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTint__level_(X1),n0)
| p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X1))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTrd__error_(f_ADD_(X1,n1)))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(X1))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X1)) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV004-0.ax',axiom_34) ).
cnf(axiom_46,axiom,
( p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTint__level_(X1),n0)
| p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X1))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X1))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTrd__error_(f_ADD_(X1,n1)))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(X1)) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV004-0.ax',axiom_46) ).
cnf(axiom_22,axiom,
( p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,fwork_DOTfifo_DOTrtl_DOTint__level_(X1))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(X1))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X1))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTwr__error_(f_ADD_(X1,n1)))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X1)) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV004-0.ax',axiom_22) ).
cnf(axiom_32,axiom,
( fwork_DOTfifo_DOTrtl_DOTrd__level_(f_ADD_(X1,n1)) = fstd_DOTstandard_DOTmod_(f_ADD_(fwork_DOTfifo_DOTrtl_DOTrd__level_(X1),n1),fwork_DOTfifo_DOTrtl_DOTfifo__length_)
| p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTint__level_(X1),n0)
| p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X1))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(X1))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X1)) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV004-0.ax',axiom_32) ).
cnf(axiom_44,axiom,
( fwork_DOTfifo_DOTrtl_DOTrd__level_(f_ADD_(X1,n1)) = fstd_DOTstandard_DOTmod_(f_ADD_(fwork_DOTfifo_DOTrtl_DOTrd__level_(X1),n1),fwork_DOTfifo_DOTrtl_DOTfifo__length_)
| p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTint__level_(X1),n0)
| p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X1))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X1))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(X1)) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV004-0.ax',axiom_44) ).
cnf(axiom_19,axiom,
( fwork_DOTfifo_DOTrtl_DOTwr__level_(f_ADD_(X1,n1)) = fstd_DOTstandard_DOTmod_(f_ADD_(fwork_DOTfifo_DOTrtl_DOTwr__level_(X1),n1),fwork_DOTfifo_DOTrtl_DOTfifo__length_)
| p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,fwork_DOTfifo_DOTrtl_DOTint__level_(X1))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(X1))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X1))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X1)) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV004-0.ax',axiom_19) ).
cnf(axiom_37,axiom,
( p__pred_(fwork_DOTfifo_DOTrtl_DOTrd__error_(f_ADD_(X1,n1)))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X1))
| ~ p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTint__level_(X1),n0)
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(X1))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X1)) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV004-0.ax',axiom_37) ).
cnf(axiom_49,axiom,
( p__pred_(fwork_DOTfifo_DOTrtl_DOTrd__error_(f_ADD_(X1,n1)))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X1))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X1))
| ~ p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTint__level_(X1),n0)
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(X1)) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV004-0.ax',axiom_49) ).
cnf(axiom_25,axiom,
( p__pred_(fwork_DOTfifo_DOTrtl_DOTwr__error_(f_ADD_(X1,n1)))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(X1))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X1))
| ~ p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,fwork_DOTfifo_DOTrtl_DOTint__level_(X1))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X1)) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV004-0.ax',axiom_25) ).
cnf(axiom_36,axiom,
( fwork_DOTfifo_DOTrtl_DOTint__level_(f_ADD_(X1,n1)) = f_ADD_(fwork_DOTfifo_DOTrtl_DOTint__level_(X1),n1)
| p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X1))
| ~ p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTint__level_(X1),n0)
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(X1))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X1)) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV004-0.ax',axiom_36) ).
cnf(axiom_35,axiom,
( fwork_DOTfifo_DOTrtl_DOTrd__level_(f_ADD_(X1,n1)) = fwork_DOTfifo_DOTrtl_DOTrd__level_(X1)
| p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X1))
| ~ p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTint__level_(X1),n0)
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(X1))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X1)) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV004-0.ax',axiom_35) ).
cnf(axiom_43,axiom,
( fwork_DOTfifo_DOTrtl_DOTint__level_(f_ADD_(X1,n1)) = f_SUB_(fwork_DOTfifo_DOTrtl_DOTint__level_(X1),n1)
| p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTint__level_(X1),n0)
| p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X1))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X1))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(X1)) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV004-0.ax',axiom_43) ).
cnf(axiom_18,axiom,
( fwork_DOTfifo_DOTrtl_DOTint__level_(f_ADD_(X1,n1)) = f_ADD_(fwork_DOTfifo_DOTrtl_DOTint__level_(X1),n1)
| p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,fwork_DOTfifo_DOTrtl_DOTint__level_(X1))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(X1))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X1))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X1)) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV004-0.ax',axiom_18) ).
cnf(axiom_48,axiom,
( fwork_DOTfifo_DOTrtl_DOTrd__level_(f_ADD_(X1,n1)) = fwork_DOTfifo_DOTrtl_DOTrd__level_(X1)
| p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X1))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X1))
| ~ p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTint__level_(X1),n0)
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(X1)) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV004-0.ax',axiom_48) ).
cnf(axiom_47,axiom,
( fwork_DOTfifo_DOTrtl_DOTint__level_(f_ADD_(X1,n1)) = fwork_DOTfifo_DOTrtl_DOTint__level_(X1)
| p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X1))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X1))
| ~ p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTint__level_(X1),n0)
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(X1)) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV004-0.ax',axiom_47) ).
cnf(axiom_24,axiom,
( fwork_DOTfifo_DOTrtl_DOTwr__level_(f_ADD_(X1,n1)) = fwork_DOTfifo_DOTrtl_DOTwr__level_(X1)
| p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(X1))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X1))
| ~ p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,fwork_DOTfifo_DOTrtl_DOTint__level_(X1))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X1)) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV004-0.ax',axiom_24) ).
cnf(axiom_23,axiom,
( fwork_DOTfifo_DOTrtl_DOTint__level_(f_ADD_(X1,n1)) = fwork_DOTfifo_DOTrtl_DOTint__level_(X1)
| p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(X1))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X1))
| ~ p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,fwork_DOTfifo_DOTrtl_DOTint__level_(X1))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X1)) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV004-0.ax',axiom_23) ).
cnf(axiom_31,axiom,
( fwork_DOTfifo_DOTrtl_DOTint__level_(f_ADD_(X1,n1)) = fwork_DOTfifo_DOTrtl_DOTint__level_(X1)
| p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTint__level_(X1),n0)
| p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X1))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(X1))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X1)) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV004-0.ax',axiom_31) ).
cnf(axiom_51,axiom,
( fwork_DOTfifo_DOTrtl_DOTint__level_(f_ADD_(X1,n1)) = fwork_DOTfifo_DOTrtl_DOTint__level_(X1)
| p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(X1))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X1))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X1)) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV004-0.ax',axiom_51) ).
cnf(axiom_12,axiom,
( fwork_DOTfifo_DOTrtl_DOTint__level_(f_ADD_(X1,n1)) = n0
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X1)) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV004-0.ax',axiom_12) ).
cnf(axiom_9,axiom,
( fwork_DOTfifo_DOTrtl_DOTint__level_(X1) = n0
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTempty_(X1)) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV004-0.ax',axiom_9) ).
cnf(axiom_7,axiom,
( fwork_DOTfifo_DOTrtl_DOTint__level_(X1) = fwork_DOTfifo_DOTrtl_DOTfifo__length_
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTfull_(X1)) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV004-0.ax',axiom_7) ).
cnf(axiom_8,axiom,
( p__pred_(fwork_DOTfifo_DOTrtl_DOTempty_(X1))
| fwork_DOTfifo_DOTrtl_DOTint__level_(X1) != n0 ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV004-0.ax',axiom_8) ).
cnf(axiom_6,axiom,
( p__pred_(fwork_DOTfifo_DOTrtl_DOTfull_(X1))
| fwork_DOTfifo_DOTrtl_DOTint__level_(X1) != fwork_DOTfifo_DOTrtl_DOTfifo__length_ ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV004-0.ax',axiom_6) ).
cnf(axiom_15,axiom,
( ~ p__pred_(f__index_(f__index_(fwork_DOTfifo_DOTrtl_DOTmem_(f_ADD_(X1,n1)),X2),X3))
| ~ p_LES_EQU_(n0,X3)
| ~ p_LES_EQU_(X3,f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__width_,n1))
| ~ p_LES_EQU_(n0,X2)
| ~ p_LES_EQU_(X2,f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,n1))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X1)) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV004-0.ax',axiom_15) ).
cnf(axiom_39,axiom,
( f__index_(f__index_(fwork_DOTfifo_DOTrtl_DOTmem_(f_ADD_(X1,n1)),f_SUB_(f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,n1),fwork_DOTfifo_DOTrtl_DOTwr__level_(X1))),X2) = f__index_(fwork_DOTfifo_DOTrtl_DOTdata__in_(X1),X2)
| p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X1))
| ~ p_LES_EQU_(n0,X2)
| ~ p_LES_EQU_(X2,f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__width_,n1))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(X1))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X1)) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV004-0.ax',axiom_39) ).
cnf(axiom_40,axiom,
( f__index_(f__index_(fwork_DOTfifo_DOTrtl_DOTmem_(f_ADD_(X1,n1)),X2),X3) = f__index_(f__index_(fwork_DOTfifo_DOTrtl_DOTmem_(X1),X2),X3)
| X2 = f_SUB_(f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,n1),fwork_DOTfifo_DOTrtl_DOTwr__level_(X1))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X1))
| ~ p_LES_EQU_(n0,X3)
| ~ p_LES_EQU_(X3,f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__width_,n1))
| ~ p_LES_EQU_(n0,X2)
| ~ p_LES_EQU_(X2,f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,n1))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(X1))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X1)) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV004-0.ax',axiom_40) ).
cnf(axiom_58,axiom,
( f__index_(f__index_(fwork_DOTfifo_DOTrtl_DOTmem_(f_ADD_(X1,n1)),X2),X3) = f__index_(f__index_(fwork_DOTfifo_DOTrtl_DOTmem_(X1),X2),X3)
| p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X1))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X1))
| ~ p_LES_EQU_(n0,X3)
| ~ p_LES_EQU_(X3,f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__width_,n1))
| ~ p_LES_EQU_(n0,X2)
| ~ p_LES_EQU_(X2,f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,n1)) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV004-0.ax',axiom_58) ).
cnf(axiom_16,axiom,
( ~ p__pred_(f__index_(fwork_DOTfifo_DOTrtl_DOTdata__out_(f_ADD_(X1,n1)),X2))
| ~ p_LES_EQU_(n0,X2)
| ~ p_LES_EQU_(X2,f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__width_,n1))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X1)) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV004-0.ax',axiom_16) ).
cnf(axiom_29,axiom,
( f__index_(fwork_DOTfifo_DOTrtl_DOTdata__out_(f_ADD_(X1,n1)),X2) = f__index_(fwork_DOTfifo_DOTrtl_DOTdata__out_(X1),X2)
| p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(X1))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X1))
| ~ p_LES_EQU_(n0,X2)
| ~ p_LES_EQU_(X2,f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__width_,n1))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X1)) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV004-0.ax',axiom_29) ).
cnf(axiom_55,axiom,
( f__index_(fwork_DOTfifo_DOTrtl_DOTdata__out_(f_ADD_(X1,n1)),X2) = f__index_(fwork_DOTfifo_DOTrtl_DOTdata__out_(X1),X2)
| p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(X1))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X1))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X1))
| ~ p_LES_EQU_(n0,X2)
| ~ p_LES_EQU_(X2,f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__width_,n1)) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV004-0.ax',axiom_55) ).
cnf(axiom_88,axiom,
f__index_(f__slice_(X1,X2,X3),X4) = f__index_(X1,f_ADD_(X4,X2)),
file('/export/starexec/sandbox/benchmark/Axioms/HWV004-0.ax',axiom_88) ).
cnf(axiom_82,axiom,
f__length_(f__slice_(X1,X2,X3)) = f_SUB_(X3,f_ADD_(X2,n1)),
file('/export/starexec/sandbox/benchmark/Axioms/HWV004-0.ax',axiom_82) ).
cnf(axiom_27,axiom,
( p__pred_(fwork_DOTfifo_DOTrtl_DOTrd__error_(X1))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(X1))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X1))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTrd__error_(f_ADD_(X1,n1)))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X1)) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV004-0.ax',axiom_27) ).
cnf(axiom_41,axiom,
( p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X1))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTwr__error_(f_ADD_(X1,n1)))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(X1))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X1)) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV004-0.ax',axiom_41) ).
cnf(axiom_53,axiom,
( p__pred_(fwork_DOTfifo_DOTrtl_DOTrd__error_(X1))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(X1))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X1))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X1))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTrd__error_(f_ADD_(X1,n1))) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV004-0.ax',axiom_53) ).
cnf(axiom_87,axiom,
( f__index_(f__concat_(X1,X3),X2) = f__index_(X3,f_SUB_(X2,length(X1)))
| ~ p_LES_EQU_(length(X1),X2) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV004-0.ax',axiom_87) ).
cnf(axiom_56,axiom,
( p__pred_(fwork_DOTfifo_DOTrtl_DOTwr__error_(X1))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X1))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X1))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTwr__error_(f_ADD_(X1,n1))) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV004-0.ax',axiom_56) ).
cnf(axiom_30,axiom,
( fwork_DOTfifo_DOTrtl_DOTwr__level_(f_ADD_(X1,n1)) = fstd_DOTstandard_DOTmod_(f_ADD_(fwork_DOTfifo_DOTrtl_DOTwr__level_(X1),n1),fwork_DOTfifo_DOTrtl_DOTfifo__length_)
| p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X1))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(X1))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X1)) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV004-0.ax',axiom_30) ).
cnf(axiom_28,axiom,
( p__pred_(fwork_DOTfifo_DOTrtl_DOTrd__error_(f_ADD_(X1,n1)))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(X1))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X1))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTrd__error_(X1))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X1)) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV004-0.ax',axiom_28) ).
cnf(axiom_66,axiom,
( p_LES_EQU_(X1,X2)
| ~ p_LES_EQU_(f_ADD_(X1,n1),f_ADD_(X2,n1)) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV004-0.ax',axiom_66) ).
cnf(axiom_94,axiom,
f__index_(f__xnor_(X1,X2),X3) = f__xnor_(f__index_(X1,X3),f__index_(X2,X3)),
file('/export/starexec/sandbox/benchmark/Axioms/HWV004-0.ax',axiom_94) ).
cnf(axiom_93,axiom,
f__index_(f__nor_(X1,X2),X3) = f__nor_(f__index_(X1,X3),f__index_(X2,X3)),
file('/export/starexec/sandbox/benchmark/Axioms/HWV004-0.ax',axiom_93) ).
cnf(axiom_92,axiom,
f__index_(f__nand_(X1,X2),X3) = f__nand_(f__index_(X1,X3),f__index_(X2,X3)),
file('/export/starexec/sandbox/benchmark/Axioms/HWV004-0.ax',axiom_92) ).
cnf(axiom_91,axiom,
f__index_(f__xor_(X1,X2),X3) = f__xor_(f__index_(X1,X3),f__index_(X2,X3)),
file('/export/starexec/sandbox/benchmark/Axioms/HWV004-0.ax',axiom_91) ).
cnf(axiom_90,axiom,
f__index_(f__or_(X1,X2),X3) = f__or_(f__index_(X1,X3),f__index_(X2,X3)),
file('/export/starexec/sandbox/benchmark/Axioms/HWV004-0.ax',axiom_90) ).
cnf(axiom_89,axiom,
f__index_(f__and_(X1,X2),X3) = f__and_(f__index_(X1,X3),f__index_(X2,X3)),
file('/export/starexec/sandbox/benchmark/Axioms/HWV004-0.ax',axiom_89) ).
cnf(axiom_14,axiom,
( ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTrd__error_(f_ADD_(X1,n1)))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X1)) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV004-0.ax',axiom_14) ).
cnf(axiom_13,axiom,
( ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTwr__error_(f_ADD_(X1,n1)))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X1)) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV004-0.ax',axiom_13) ).
cnf(axiom_54,axiom,
( p__pred_(fwork_DOTfifo_DOTrtl_DOTrd__error_(f_ADD_(X1,n1)))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(X1))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X1))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X1))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTrd__error_(X1)) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV004-0.ax',axiom_54) ).
cnf(axiom_57,axiom,
( p__pred_(fwork_DOTfifo_DOTrtl_DOTwr__error_(f_ADD_(X1,n1)))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X1))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X1))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTwr__error_(X1)) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV004-0.ax',axiom_57) ).
cnf(axiom_85,axiom,
( p_LES_EQU_(X1,n0)
| f__index_(f__cons_(X2,X3),X1) = f__index_(X3,f_SUB_(X1,n1)) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV004-0.ax',axiom_85) ).
cnf(axiom_72,axiom,
( f_ADD_(X1,n1) = X2
| p_LES_EQU_(X2,X1)
| ~ p_LES_EQU_(X2,f_ADD_(X1,n1)) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV004-0.ax',axiom_72) ).
cnf(axiom_67,axiom,
( p_LES_EQU_(f_ADD_(X1,n1),f_ADD_(X2,n1))
| ~ p_LES_EQU_(X1,X2) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV004-0.ax',axiom_67) ).
cnf(axiom_86,axiom,
( p_LES_EQU_(length(X1),X2)
| f__index_(f__concat_(X1,X3),X2) = f__index_(X1,X2) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV004-0.ax',axiom_86) ).
cnf(axiom_61,axiom,
( p_LES_EQU_(X1,n0)
| ~ p_LES_EQU_(X1,f_SUB_(X1,n1)) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV004-0.ax',axiom_61) ).
cnf(axiom_131,axiom,
( ~ p_LES_EQU_(X1,X2)
| ~ p__pred_(f__gt_(X1,X2)) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV004-0.ax',axiom_131) ).
cnf(axiom_127,axiom,
( ~ p_LES_EQU_(X1,X2)
| ~ p__pred_(f__lt_(X2,X1)) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV004-0.ax',axiom_127) ).
cnf(axiom_17,axiom,
( fwork_DOTfifo_DOTrtl_DOTrd__level_(f_ADD_(X1,n1)) = fwork_DOTfifo_DOTrtl_DOTrd__level_(X1)
| p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(X1))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X1))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X1)) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV004-0.ax',axiom_17) ).
cnf(axiom_52,axiom,
( fwork_DOTfifo_DOTrtl_DOTrd__level_(f_ADD_(X1,n1)) = fwork_DOTfifo_DOTrtl_DOTrd__level_(X1)
| p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(X1))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X1))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X1)) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV004-0.ax',axiom_52) ).
cnf(axiom_69,axiom,
( X1 = X2
| p_LES_EQU_(f_ADD_(X1,n1),X2)
| ~ p_LES_EQU_(X1,X2) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV004-0.ax',axiom_69) ).
cnf(axiom_68,axiom,
( X1 = X2
| p_LES_EQU_(f_ADD_(X2,n1),X1)
| ~ p_LES_EQU_(X2,X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV004-0.ax',axiom_68) ).
cnf(axiom_133,axiom,
( p_LES_EQU_(X1,X2)
| ~ p__pred_(f__geq_(X2,X1)) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV004-0.ax',axiom_133) ).
cnf(axiom_129,axiom,
( p_LES_EQU_(X1,X2)
| ~ p__pred_(f__leq_(X1,X2)) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV004-0.ax',axiom_129) ).
cnf(axiom_115,axiom,
( ~ p__pred_(X1)
| ~ p__pred_(X2)
| ~ p__pred_(f__nand_(X1,X2)) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV004-0.ax',axiom_115) ).
cnf(axiom_111,axiom,
( ~ p__pred_(X1)
| ~ p__pred_(X2)
| ~ p__pred_(f__xor_(X2,X1)) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV004-0.ax',axiom_111) ).
cnf(axiom_99,axiom,
( p__pred_(X1)
| ~ p__pred_(X2)
| ~ p__pred_(f__equiv_(X2,X1)) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV004-0.ax',axiom_99) ).
cnf(axiom_121,axiom,
( p__pred_(X1)
| ~ p__pred_(X2)
| ~ p__pred_(f__xnor_(X2,X1)) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV004-0.ax',axiom_121) ).
cnf(axiom_100,axiom,
( p__pred_(X2)
| ~ p__pred_(X1)
| ~ p__pred_(f__equiv_(X2,X1)) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV004-0.ax',axiom_100) ).
cnf(axiom_122,axiom,
( p__pred_(X2)
| ~ p__pred_(X1)
| ~ p__pred_(f__xnor_(X2,X1)) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV004-0.ax',axiom_122) ).
cnf(axiom_112,axiom,
( p__pred_(X1)
| p__pred_(X2)
| ~ p__pred_(f__xor_(X2,X1)) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV004-0.ax',axiom_112) ).
cnf(axiom_108,axiom,
( p__pred_(X1)
| p__pred_(X2)
| ~ p__pred_(f__or_(X1,X2)) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV004-0.ax',axiom_108) ).
cnf(axiom_81,axiom,
f__length_(f__concat_(X1,X2)) = f_ADD_(f__length_(X1),f__length_(X2)),
file('/export/starexec/sandbox/benchmark/Axioms/HWV004-0.ax',axiom_81) ).
cnf(axiom_60,axiom,
~ p_LES_EQU_(f_ADD_(X1,n1),n0),
file('/export/starexec/sandbox/benchmark/Axioms/HWV004-0.ax',axiom_60) ).
cnf(axiom_119,axiom,
( ~ p__pred_(X1)
| ~ p__pred_(f__nor_(X1,X2)) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV004-0.ax',axiom_119) ).
cnf(axiom_118,axiom,
( ~ p__pred_(X1)
| ~ p__pred_(f__nor_(X2,X1)) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV004-0.ax',axiom_118) ).
cnf(axiom_62,axiom,
( def_89(X1,X2)
| f_ADD_(X3,X1) = X2
| f_SUB_(X2,X1) != X3 ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV004-0.ax',axiom_62) ).
cnf(axiom_63,axiom,
( def_89(X1,X2)
| f_SUB_(X2,X1) = X3
| f_ADD_(X3,X1) != X2 ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV004-0.ax',axiom_63) ).
cnf(axiom_134,axiom,
( p__pred_(f__geq_(X2,X1))
| ~ p_LES_EQU_(X1,X2) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV004-0.ax',axiom_134) ).
cnf(axiom_130,axiom,
( p__pred_(f__leq_(X1,X2))
| ~ p_LES_EQU_(X1,X2) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV004-0.ax',axiom_130) ).
cnf(axiom_42,axiom,
( fwork_DOTfifo_DOTrtl_DOTwr__level_(f_ADD_(X1,n1)) = fwork_DOTfifo_DOTrtl_DOTwr__level_(X1)
| p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X1))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X1)) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV004-0.ax',axiom_42) ).
cnf(axiom_106,axiom,
( p__pred_(X1)
| ~ p__pred_(f__and_(X1,X2)) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV004-0.ax',axiom_106) ).
cnf(axiom_105,axiom,
( p__pred_(X1)
| ~ p__pred_(f__and_(X2,X1)) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV004-0.ax',axiom_105) ).
cnf(axiom_71,axiom,
( p_LES_EQU_(X3,X2)
| p_LES_EQU_(X1,X3)
| ~ p_LES_EQU_(X1,X2) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV004-0.ax',axiom_71) ).
cnf(quest_3,negated_conjecture,
p__pred_(fwork_DOTfifo_DOTrtl_DOTwr__error_(f_ADD_(t_206,n1))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',quest_3) ).
cnf(axiom_95,axiom,
f__index_(f__not_(X1),X2) = f__not_(f__index_(X1,X2)),
file('/export/starexec/sandbox/benchmark/Axioms/HWV004-0.ax',axiom_95) ).
cnf(axiom_103,axiom,
( X1 = X2
| ~ p__pred_(f__equal_(X1,X2)) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV004-0.ax',axiom_103) ).
cnf(axiom_79,axiom,
f__length_(f__cons_(X1,X2)) = f_ADD_(f__length_(X2),n1),
file('/export/starexec/sandbox/benchmark/Axioms/HWV004-0.ax',axiom_79) ).
cnf(axiom_70,axiom,
( X1 = X2
| ~ p_LES_EQU_(X1,X2)
| ~ p_LES_EQU_(X2,X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV004-0.ax',axiom_70) ).
cnf(axiom_132,axiom,
( p_LES_EQU_(X1,X2)
| p__pred_(f__gt_(X1,X2)) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV004-0.ax',axiom_132) ).
cnf(axiom_128,axiom,
( p_LES_EQU_(X1,X2)
| p__pred_(f__lt_(X2,X1)) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV004-0.ax',axiom_128) ).
cnf(axiom_101,axiom,
( p__pred_(f__equiv_(X2,X1))
| ~ p__pred_(X1)
| ~ p__pred_(X2) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV004-0.ax',axiom_101) ).
cnf(axiom_123,axiom,
( p__pred_(f__xnor_(X2,X1))
| ~ p__pred_(X1)
| ~ p__pred_(X2) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV004-0.ax',axiom_123) ).
cnf(axiom_107,axiom,
( p__pred_(f__and_(X1,X2))
| ~ p__pred_(X1)
| ~ p__pred_(X2) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV004-0.ax',axiom_107) ).
cnf(axiom_11,axiom,
( fwork_DOTfifo_DOTrtl_DOTwr__level_(f_ADD_(X1,n1)) = n0
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X1)) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV004-0.ax',axiom_11) ).
cnf(axiom_10,axiom,
( fwork_DOTfifo_DOTrtl_DOTrd__level_(f_ADD_(X1,n1)) = n0
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X1)) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV004-0.ax',axiom_10) ).
cnf(axiom_84,axiom,
( f__index_(f__cons_(X2,X3),X1) = X2
| X1 != n0 ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV004-0.ax',axiom_84) ).
cnf(axiom_4,axiom,
f__length_(fwork_DOTfifo_DOTrtl_DOTdata__in_(X1)) = f_ADD_(f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__width_,n1),n1),
file('/export/starexec/sandbox/benchmark/Axioms/HWV004-0.ax',axiom_4) ).
cnf(axiom_3,axiom,
f__length_(fwork_DOTfifo_DOTrtl_DOTdata__out_(X1)) = f_ADD_(f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__width_,n1),n1),
file('/export/starexec/sandbox/benchmark/Axioms/HWV004-0.ax',axiom_3) ).
cnf(axiom_2,axiom,
f__length_(fwork_DOTfifo_DOTrtl_DOTmem_(X1)) = f_ADD_(f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,n1),n1),
file('/export/starexec/sandbox/benchmark/Axioms/HWV004-0.ax',axiom_2) ).
cnf(axiom_113,axiom,
( p__pred_(X1)
| p__pred_(f__xor_(X2,X1))
| ~ p__pred_(X2) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV004-0.ax',axiom_113) ).
cnf(axiom_114,axiom,
( p__pred_(X2)
| p__pred_(f__xor_(X2,X1))
| ~ p__pred_(X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV004-0.ax',axiom_114) ).
cnf(axiom_76,axiom,
( X1 = X2
| f_ADD_(X1,n1) != f_ADD_(X2,n1) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV004-0.ax',axiom_76) ).
cnf(axiom_102,axiom,
( p__pred_(X1)
| p__pred_(X2)
| p__pred_(f__equiv_(X2,X1)) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV004-0.ax',axiom_102) ).
cnf(axiom_124,axiom,
( p__pred_(X1)
| p__pred_(X2)
| p__pred_(f__xnor_(X2,X1)) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV004-0.ax',axiom_124) ).
cnf(axiom_120,axiom,
( p__pred_(X1)
| p__pred_(X2)
| p__pred_(f__nor_(X1,X2)) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV004-0.ax',axiom_120) ).
cnf(axiom_110,axiom,
( p__pred_(f__or_(X1,X2))
| ~ p__pred_(X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV004-0.ax',axiom_110) ).
cnf(axiom_109,axiom,
( p__pred_(f__or_(X2,X1))
| ~ p__pred_(X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV004-0.ax',axiom_109) ).
cnf(axiom_65,axiom,
( p_LES_EQU_(X1,X2)
| ~ def_89(X2,X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV004-0.ax',axiom_65) ).
cnf(axiom_117,axiom,
( p__pred_(X1)
| p__pred_(f__nand_(X1,X2)) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV004-0.ax',axiom_117) ).
cnf(axiom_116,axiom,
( p__pred_(X1)
| p__pred_(f__nand_(X2,X1)) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV004-0.ax',axiom_116) ).
cnf(axiom_104,axiom,
( p__pred_(f__equal_(X1,X2))
| X1 != X2 ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV004-0.ax',axiom_104) ).
cnf(axiom_64,axiom,
( X1 != X2
| ~ def_89(X2,X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV004-0.ax',axiom_64) ).
cnf(axiom_125,axiom,
( ~ p__pred_(X1)
| ~ p__pred_(f__not_(X1)) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV004-0.ax',axiom_125) ).
cnf(axiom_73,axiom,
( X1 = n0
| ~ p_LES_EQU_(X1,n0) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV004-0.ax',axiom_73) ).
cnf(axiom_74,axiom,
( X1 = f_ADD_(y_105(X1),n1)
| X1 = n0 ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV004-0.ax',axiom_74) ).
cnf(axiom_83,axiom,
f__index_(f__others_(X1),X2) = X1,
file('/export/starexec/sandbox/benchmark/Axioms/HWV004-0.ax',axiom_83) ).
cnf(axiom_59,axiom,
f_ADD_(X1,n1) != n0,
file('/export/starexec/sandbox/benchmark/Axioms/HWV004-0.ax',axiom_59) ).
cnf(axiom_126,axiom,
( p__pred_(X1)
| p__pred_(f__not_(X1)) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV004-0.ax',axiom_126) ).
cnf(axiom_75,axiom,
p_LES_EQU_(X1,X1),
file('/export/starexec/sandbox/benchmark/Axioms/HWV004-0.ax',axiom_75) ).
cnf(axiom_77,axiom,
f_ADD_(n0,X1) = X1,
file('/export/starexec/sandbox/benchmark/Axioms/HWV004-0.ax',axiom_77) ).
cnf(quest_1,negated_conjecture,
~ p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(t_206)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',quest_1) ).
cnf(quest_4,negated_conjecture,
~ p__pred_(fwork_DOTfifo_DOTrtl_DOTwr__error_(t_206)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',quest_4) ).
cnf(quest_2,negated_conjecture,
~ p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(t_206)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',quest_2) ).
cnf(axiom_78,axiom,
n1 = f_ADD_(n0,n1),
file('/export/starexec/sandbox/benchmark/Axioms/HWV004-0.ax',axiom_78) ).
cnf(axiom_97,axiom,
~ p__pred_(f__false_),
file('/export/starexec/sandbox/benchmark/Axioms/HWV004-0.ax',axiom_97) ).
cnf(axiom_96,axiom,
p__pred_(f__true_),
file('/export/starexec/sandbox/benchmark/Axioms/HWV004-0.ax',axiom_96) ).
cnf(axiom_80,axiom,
f__length_(f__empty_) = n0,
file('/export/starexec/sandbox/benchmark/Axioms/HWV004-0.ax',axiom_80) ).
cnf(axiom_98,axiom,
f__false_ != f__true_,
file('/export/starexec/sandbox/benchmark/Axioms/HWV004-0.ax',axiom_98) ).
cnf(i_0_137,axiom,
( f__index_(f__index_(fwork_DOTfifo_DOTrtl_DOTmem_(f_ADD_(X1,n1)),f_SUB_(f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,n1),fwork_DOTfifo_DOTrtl_DOTwr__level_(X1))),X2) = f__index_(fwork_DOTfifo_DOTrtl_DOTdata__in_(X1),X2)
| p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,fwork_DOTfifo_DOTrtl_DOTint__level_(X1))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(X1))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X1))
| ~ p_LES_EQU_(n0,X2)
| ~ p_LES_EQU_(X2,f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__width_,n1))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X1)) ),
axiom_20 ).
cnf(i_0_138,axiom,
fwork_DOTfifo_DOTrtl_DOTlevel_(X1) = fwork_DOTfifo_DOTrtl_DOTint__level_(X1),
axiom_5 ).
cnf(i_0_139,axiom,
( f__index_(f__index_(fwork_DOTfifo_DOTrtl_DOTmem_(f_ADD_(X1,n1)),X2),X3) = f__index_(f__index_(fwork_DOTfifo_DOTrtl_DOTmem_(X1),X2),X3)
| X2 = f_SUB_(f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,n1),fwork_DOTfifo_DOTrtl_DOTwr__level_(X1))
| p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,fwork_DOTfifo_DOTrtl_DOTint__level_(X1))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(X1))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X1))
| ~ p_LES_EQU_(n0,X3)
| ~ p_LES_EQU_(X3,f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__width_,n1))
| ~ p_LES_EQU_(n0,X2)
| ~ p_LES_EQU_(X2,f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,n1))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X1)) ),
axiom_21 ).
cnf(i_0_140,axiom,
( f__index_(f__index_(fwork_DOTfifo_DOTrtl_DOTmem_(f_ADD_(X1,n1)),X2),X3) = f__index_(f__index_(fwork_DOTfifo_DOTrtl_DOTmem_(X1),X2),X3)
| p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(X1))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X1))
| ~ p_LES_EQU_(n0,X3)
| ~ p_LES_EQU_(X3,f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__width_,n1))
| ~ p_LES_EQU_(n0,X2)
| ~ p_LES_EQU_(X2,f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,n1))
| ~ p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,fwork_DOTfifo_DOTrtl_DOTint__level_(X1))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X1)) ),
axiom_26 ).
cnf(i_0_141,axiom,
( f__index_(fwork_DOTfifo_DOTrtl_DOTdata__out_(f_ADD_(X1,n1)),X2) = f__index_(f__index_(fwork_DOTfifo_DOTrtl_DOTmem_(X1),f_SUB_(f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,n1),fwork_DOTfifo_DOTrtl_DOTrd__level_(X1))),X2)
| p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTint__level_(X1),n0)
| p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X1))
| ~ p_LES_EQU_(n0,X2)
| ~ p_LES_EQU_(X2,f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__width_,n1))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(X1))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X1)) ),
axiom_33 ).
cnf(i_0_142,axiom,
( f__index_(fwork_DOTfifo_DOTrtl_DOTdata__out_(f_ADD_(X1,n1)),X2) = f__index_(f__index_(fwork_DOTfifo_DOTrtl_DOTmem_(X1),f_SUB_(f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,n1),fwork_DOTfifo_DOTrtl_DOTrd__level_(X1))),X2)
| p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTint__level_(X1),n0)
| p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X1))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X1))
| ~ p_LES_EQU_(n0,X2)
| ~ p_LES_EQU_(X2,f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__width_,n1))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(X1)) ),
axiom_45 ).
cnf(i_0_143,axiom,
( f__index_(fwork_DOTfifo_DOTrtl_DOTdata__out_(f_ADD_(X1,n1)),X2) = f__index_(fwork_DOTfifo_DOTrtl_DOTdata__out_(X1),X2)
| p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X1))
| ~ p_LES_EQU_(n0,X2)
| ~ p_LES_EQU_(X2,f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__width_,n1))
| ~ p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTint__level_(X1),n0)
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(X1))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X1)) ),
axiom_38 ).
cnf(i_0_144,axiom,
( f__index_(fwork_DOTfifo_DOTrtl_DOTdata__out_(f_ADD_(X1,n1)),X2) = f__index_(fwork_DOTfifo_DOTrtl_DOTdata__out_(X1),X2)
| p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X1))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X1))
| ~ p_LES_EQU_(n0,X2)
| ~ p_LES_EQU_(X2,f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__width_,n1))
| ~ p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTint__level_(X1),n0)
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(X1)) ),
axiom_50 ).
cnf(i_0_145,axiom,
( p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTint__level_(X1),n0)
| p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X1))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTrd__error_(f_ADD_(X1,n1)))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(X1))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X1)) ),
axiom_34 ).
cnf(i_0_146,axiom,
( p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTint__level_(X1),n0)
| p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X1))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X1))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTrd__error_(f_ADD_(X1,n1)))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(X1)) ),
axiom_46 ).
cnf(i_0_147,axiom,
( p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,fwork_DOTfifo_DOTrtl_DOTint__level_(X1))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(X1))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X1))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTwr__error_(f_ADD_(X1,n1)))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X1)) ),
axiom_22 ).
cnf(i_0_148,axiom,
( fwork_DOTfifo_DOTrtl_DOTrd__level_(f_ADD_(X1,n1)) = fstd_DOTstandard_DOTmod_(f_ADD_(fwork_DOTfifo_DOTrtl_DOTrd__level_(X1),n1),fwork_DOTfifo_DOTrtl_DOTfifo__length_)
| p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTint__level_(X1),n0)
| p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X1))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(X1))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X1)) ),
axiom_32 ).
cnf(i_0_149,axiom,
( fwork_DOTfifo_DOTrtl_DOTrd__level_(f_ADD_(X1,n1)) = fstd_DOTstandard_DOTmod_(f_ADD_(fwork_DOTfifo_DOTrtl_DOTrd__level_(X1),n1),fwork_DOTfifo_DOTrtl_DOTfifo__length_)
| p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTint__level_(X1),n0)
| p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X1))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X1))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(X1)) ),
axiom_44 ).
cnf(i_0_150,axiom,
( fwork_DOTfifo_DOTrtl_DOTwr__level_(f_ADD_(X1,n1)) = fstd_DOTstandard_DOTmod_(f_ADD_(fwork_DOTfifo_DOTrtl_DOTwr__level_(X1),n1),fwork_DOTfifo_DOTrtl_DOTfifo__length_)
| p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,fwork_DOTfifo_DOTrtl_DOTint__level_(X1))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(X1))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X1))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X1)) ),
axiom_19 ).
cnf(i_0_151,axiom,
( p__pred_(fwork_DOTfifo_DOTrtl_DOTrd__error_(f_ADD_(X1,n1)))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X1))
| ~ p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTint__level_(X1),n0)
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(X1))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X1)) ),
axiom_37 ).
cnf(i_0_152,axiom,
( p__pred_(fwork_DOTfifo_DOTrtl_DOTrd__error_(f_ADD_(X1,n1)))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X1))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X1))
| ~ p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTint__level_(X1),n0)
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(X1)) ),
axiom_49 ).
cnf(i_0_153,axiom,
( p__pred_(fwork_DOTfifo_DOTrtl_DOTwr__error_(f_ADD_(X1,n1)))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(X1))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X1))
| ~ p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,fwork_DOTfifo_DOTrtl_DOTint__level_(X1))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X1)) ),
axiom_25 ).
cnf(i_0_154,axiom,
( fwork_DOTfifo_DOTrtl_DOTint__level_(f_ADD_(X1,n1)) = f_ADD_(fwork_DOTfifo_DOTrtl_DOTint__level_(X1),n1)
| p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X1))
| ~ p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTint__level_(X1),n0)
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(X1))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X1)) ),
axiom_36 ).
cnf(i_0_155,axiom,
( fwork_DOTfifo_DOTrtl_DOTrd__level_(f_ADD_(X1,n1)) = fwork_DOTfifo_DOTrtl_DOTrd__level_(X1)
| p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X1))
| ~ p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTint__level_(X1),n0)
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(X1))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X1)) ),
axiom_35 ).
cnf(i_0_156,axiom,
( fwork_DOTfifo_DOTrtl_DOTint__level_(f_ADD_(X1,n1)) = f_SUB_(fwork_DOTfifo_DOTrtl_DOTint__level_(X1),n1)
| p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTint__level_(X1),n0)
| p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X1))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X1))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(X1)) ),
axiom_43 ).
cnf(i_0_157,axiom,
( fwork_DOTfifo_DOTrtl_DOTint__level_(f_ADD_(X1,n1)) = f_ADD_(fwork_DOTfifo_DOTrtl_DOTint__level_(X1),n1)
| p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,fwork_DOTfifo_DOTrtl_DOTint__level_(X1))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(X1))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X1))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X1)) ),
axiom_18 ).
cnf(i_0_158,axiom,
( fwork_DOTfifo_DOTrtl_DOTrd__level_(f_ADD_(X1,n1)) = fwork_DOTfifo_DOTrtl_DOTrd__level_(X1)
| p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X1))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X1))
| ~ p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTint__level_(X1),n0)
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(X1)) ),
axiom_48 ).
cnf(i_0_159,axiom,
( fwork_DOTfifo_DOTrtl_DOTint__level_(f_ADD_(X1,n1)) = fwork_DOTfifo_DOTrtl_DOTint__level_(X1)
| p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X1))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X1))
| ~ p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTint__level_(X1),n0)
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(X1)) ),
axiom_47 ).
cnf(i_0_160,axiom,
( fwork_DOTfifo_DOTrtl_DOTwr__level_(f_ADD_(X1,n1)) = fwork_DOTfifo_DOTrtl_DOTwr__level_(X1)
| p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(X1))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X1))
| ~ p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,fwork_DOTfifo_DOTrtl_DOTint__level_(X1))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X1)) ),
axiom_24 ).
cnf(i_0_161,axiom,
( fwork_DOTfifo_DOTrtl_DOTint__level_(f_ADD_(X1,n1)) = fwork_DOTfifo_DOTrtl_DOTint__level_(X1)
| p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(X1))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X1))
| ~ p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,fwork_DOTfifo_DOTrtl_DOTint__level_(X1))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X1)) ),
axiom_23 ).
cnf(i_0_162,axiom,
( fwork_DOTfifo_DOTrtl_DOTint__level_(f_ADD_(X1,n1)) = fwork_DOTfifo_DOTrtl_DOTint__level_(X1)
| p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTint__level_(X1),n0)
| p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X1))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(X1))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X1)) ),
axiom_31 ).
cnf(i_0_163,axiom,
( fwork_DOTfifo_DOTrtl_DOTint__level_(f_ADD_(X1,n1)) = fwork_DOTfifo_DOTrtl_DOTint__level_(X1)
| p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(X1))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X1))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X1)) ),
axiom_51 ).
cnf(i_0_164,axiom,
( fwork_DOTfifo_DOTrtl_DOTint__level_(f_ADD_(X1,n1)) = n0
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X1)) ),
axiom_12 ).
cnf(i_0_165,axiom,
( fwork_DOTfifo_DOTrtl_DOTint__level_(X1) = n0
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTempty_(X1)) ),
axiom_9 ).
cnf(i_0_166,axiom,
( fwork_DOTfifo_DOTrtl_DOTint__level_(X1) = fwork_DOTfifo_DOTrtl_DOTfifo__length_
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTfull_(X1)) ),
axiom_7 ).
cnf(i_0_167,axiom,
( p__pred_(fwork_DOTfifo_DOTrtl_DOTempty_(X1))
| fwork_DOTfifo_DOTrtl_DOTint__level_(X1) != n0 ),
axiom_8 ).
cnf(i_0_168,axiom,
( p__pred_(fwork_DOTfifo_DOTrtl_DOTfull_(X1))
| fwork_DOTfifo_DOTrtl_DOTint__level_(X1) != fwork_DOTfifo_DOTrtl_DOTfifo__length_ ),
axiom_6 ).
cnf(i_0_169,axiom,
( ~ p__pred_(f__index_(f__index_(fwork_DOTfifo_DOTrtl_DOTmem_(f_ADD_(X1,n1)),X2),X3))
| ~ p_LES_EQU_(n0,X3)
| ~ p_LES_EQU_(X3,f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__width_,n1))
| ~ p_LES_EQU_(n0,X2)
| ~ p_LES_EQU_(X2,f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,n1))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X1)) ),
axiom_15,
[final] ).
cnf(i_0_170,plain,
( f__index_(f__index_(fwork_DOTfifo_DOTrtl_DOTmem_(f_ADD_(X1,n1)),f_SUB_(f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,n1),fwork_DOTfifo_DOTrtl_DOTwr__level_(X1))),X2) = f__index_(fwork_DOTfifo_DOTrtl_DOTdata__in_(X1),X2)
| p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X1))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(X1))
| p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,fwork_DOTfifo_DOTrtl_DOTlevel_(X1))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X1))
| ~ p_LES_EQU_(n0,X2)
| ~ p_LES_EQU_(X2,f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__width_,n1)) ),
inference(rw,[status(thm)],[i_0_137,c_0_138]),
[final] ).
cnf(i_0_171,plain,
( X2 = f_SUB_(f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,n1),fwork_DOTfifo_DOTrtl_DOTwr__level_(X1))
| f__index_(f__index_(fwork_DOTfifo_DOTrtl_DOTmem_(f_ADD_(X1,n1)),X2),X3) = f__index_(f__index_(fwork_DOTfifo_DOTrtl_DOTmem_(X1),X2),X3)
| p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X1))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(X1))
| p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,fwork_DOTfifo_DOTrtl_DOTlevel_(X1))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X1))
| ~ p_LES_EQU_(n0,X3)
| ~ p_LES_EQU_(n0,X2)
| ~ p_LES_EQU_(X3,f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__width_,n1))
| ~ p_LES_EQU_(X2,f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,n1)) ),
inference(rw,[status(thm)],[i_0_139,c_0_138]),
[final] ).
cnf(i_0_172,axiom,
( f__index_(f__index_(fwork_DOTfifo_DOTrtl_DOTmem_(f_ADD_(X1,n1)),f_SUB_(f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,n1),fwork_DOTfifo_DOTrtl_DOTwr__level_(X1))),X2) = f__index_(fwork_DOTfifo_DOTrtl_DOTdata__in_(X1),X2)
| p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X1))
| ~ p_LES_EQU_(n0,X2)
| ~ p_LES_EQU_(X2,f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__width_,n1))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(X1))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X1)) ),
axiom_39,
[final] ).
cnf(i_0_173,axiom,
( f__index_(f__index_(fwork_DOTfifo_DOTrtl_DOTmem_(f_ADD_(X1,n1)),X2),X3) = f__index_(f__index_(fwork_DOTfifo_DOTrtl_DOTmem_(X1),X2),X3)
| X2 = f_SUB_(f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,n1),fwork_DOTfifo_DOTrtl_DOTwr__level_(X1))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X1))
| ~ p_LES_EQU_(n0,X3)
| ~ p_LES_EQU_(X3,f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__width_,n1))
| ~ p_LES_EQU_(n0,X2)
| ~ p_LES_EQU_(X2,f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,n1))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(X1))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X1)) ),
axiom_40,
[final] ).
cnf(i_0_174,plain,
( f__index_(f__index_(fwork_DOTfifo_DOTrtl_DOTmem_(f_ADD_(X1,n1)),X2),X3) = f__index_(f__index_(fwork_DOTfifo_DOTrtl_DOTmem_(X1),X2),X3)
| p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X1))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(X1))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X1))
| ~ p_LES_EQU_(n0,X3)
| ~ p_LES_EQU_(n0,X2)
| ~ p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,fwork_DOTfifo_DOTrtl_DOTlevel_(X1))
| ~ p_LES_EQU_(X3,f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__width_,n1))
| ~ p_LES_EQU_(X2,f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,n1)) ),
inference(rw,[status(thm)],[i_0_140,c_0_138]),
[final] ).
cnf(i_0_175,plain,
( f__index_(fwork_DOTfifo_DOTrtl_DOTdata__out_(f_ADD_(X1,n1)),X2) = f__index_(f__index_(fwork_DOTfifo_DOTrtl_DOTmem_(X1),f_SUB_(f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,n1),fwork_DOTfifo_DOTrtl_DOTrd__level_(X1))),X2)
| p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X1))
| p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTlevel_(X1),n0)
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(X1))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X1))
| ~ p_LES_EQU_(n0,X2)
| ~ p_LES_EQU_(X2,f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__width_,n1)) ),
inference(rw,[status(thm)],[i_0_141,c_0_138]),
[final] ).
cnf(i_0_176,plain,
( f__index_(fwork_DOTfifo_DOTrtl_DOTdata__out_(f_ADD_(X1,n1)),X2) = f__index_(f__index_(fwork_DOTfifo_DOTrtl_DOTmem_(X1),f_SUB_(f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,n1),fwork_DOTfifo_DOTrtl_DOTrd__level_(X1))),X2)
| p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X1))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X1))
| p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTlevel_(X1),n0)
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(X1))
| ~ p_LES_EQU_(n0,X2)
| ~ p_LES_EQU_(X2,f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__width_,n1)) ),
inference(rw,[status(thm)],[i_0_142,c_0_138]),
[final] ).
cnf(i_0_177,axiom,
( f__index_(f__index_(fwork_DOTfifo_DOTrtl_DOTmem_(f_ADD_(X1,n1)),X2),X3) = f__index_(f__index_(fwork_DOTfifo_DOTrtl_DOTmem_(X1),X2),X3)
| p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X1))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X1))
| ~ p_LES_EQU_(n0,X3)
| ~ p_LES_EQU_(X3,f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__width_,n1))
| ~ p_LES_EQU_(n0,X2)
| ~ p_LES_EQU_(X2,f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,n1)) ),
axiom_58,
[final] ).
cnf(i_0_178,axiom,
( ~ p__pred_(f__index_(fwork_DOTfifo_DOTrtl_DOTdata__out_(f_ADD_(X1,n1)),X2))
| ~ p_LES_EQU_(n0,X2)
| ~ p_LES_EQU_(X2,f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__width_,n1))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X1)) ),
axiom_16,
[final] ).
cnf(i_0_179,plain,
( f__index_(fwork_DOTfifo_DOTrtl_DOTdata__out_(f_ADD_(X1,n1)),X2) = f__index_(fwork_DOTfifo_DOTrtl_DOTdata__out_(X1),X2)
| p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X1))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(X1))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X1))
| ~ p_LES_EQU_(n0,X2)
| ~ p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTlevel_(X1),n0)
| ~ p_LES_EQU_(X2,f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__width_,n1)) ),
inference(rw,[status(thm)],[i_0_143,c_0_138]),
[final] ).
cnf(i_0_180,plain,
( f__index_(fwork_DOTfifo_DOTrtl_DOTdata__out_(f_ADD_(X1,n1)),X2) = f__index_(fwork_DOTfifo_DOTrtl_DOTdata__out_(X1),X2)
| p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X1))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X1))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(X1))
| ~ p_LES_EQU_(n0,X2)
| ~ p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTlevel_(X1),n0)
| ~ p_LES_EQU_(X2,f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__width_,n1)) ),
inference(rw,[status(thm)],[i_0_144,c_0_138]),
[final] ).
cnf(i_0_181,axiom,
( f__index_(fwork_DOTfifo_DOTrtl_DOTdata__out_(f_ADD_(X1,n1)),X2) = f__index_(fwork_DOTfifo_DOTrtl_DOTdata__out_(X1),X2)
| p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(X1))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X1))
| ~ p_LES_EQU_(n0,X2)
| ~ p_LES_EQU_(X2,f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__width_,n1))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X1)) ),
axiom_29,
[final] ).
cnf(i_0_182,axiom,
( f__index_(fwork_DOTfifo_DOTrtl_DOTdata__out_(f_ADD_(X1,n1)),X2) = f__index_(fwork_DOTfifo_DOTrtl_DOTdata__out_(X1),X2)
| p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(X1))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X1))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X1))
| ~ p_LES_EQU_(n0,X2)
| ~ p_LES_EQU_(X2,f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__width_,n1)) ),
axiom_55,
[final] ).
cnf(i_0_183,axiom,
f__index_(f__slice_(X1,X2,X3),X4) = f__index_(X1,f_ADD_(X4,X2)),
axiom_88,
[final] ).
cnf(i_0_184,plain,
( p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X1))
| p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTlevel_(X1),n0)
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(X1))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X1))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTrd__error_(f_ADD_(X1,n1))) ),
inference(rw,[status(thm)],[i_0_145,c_0_138]),
[final] ).
cnf(i_0_185,axiom,
f__length_(f__slice_(X1,X2,X3)) = f_SUB_(X3,f_ADD_(X2,n1)),
axiom_82,
[final] ).
cnf(i_0_186,plain,
( p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X1))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X1))
| p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTlevel_(X1),n0)
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(X1))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTrd__error_(f_ADD_(X1,n1))) ),
inference(rw,[status(thm)],[i_0_146,c_0_138]),
[final] ).
cnf(i_0_187,plain,
( p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X1))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(X1))
| p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,fwork_DOTfifo_DOTrtl_DOTlevel_(X1))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X1))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTwr__error_(f_ADD_(X1,n1))) ),
inference(rw,[status(thm)],[i_0_147,c_0_138]),
[final] ).
cnf(i_0_188,plain,
( fwork_DOTfifo_DOTrtl_DOTrd__level_(f_ADD_(X1,n1)) = fstd_DOTstandard_DOTmod_(f_ADD_(fwork_DOTfifo_DOTrtl_DOTrd__level_(X1),n1),fwork_DOTfifo_DOTrtl_DOTfifo__length_)
| p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X1))
| p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTlevel_(X1),n0)
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(X1))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X1)) ),
inference(rw,[status(thm)],[i_0_148,c_0_138]),
[final] ).
cnf(i_0_189,axiom,
( p__pred_(fwork_DOTfifo_DOTrtl_DOTrd__error_(X1))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(X1))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X1))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTrd__error_(f_ADD_(X1,n1)))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X1)) ),
axiom_27,
[final] ).
cnf(i_0_190,axiom,
( p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X1))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTwr__error_(f_ADD_(X1,n1)))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(X1))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X1)) ),
axiom_41,
[final] ).
cnf(i_0_191,plain,
( fwork_DOTfifo_DOTrtl_DOTrd__level_(f_ADD_(X1,n1)) = fstd_DOTstandard_DOTmod_(f_ADD_(fwork_DOTfifo_DOTrtl_DOTrd__level_(X1),n1),fwork_DOTfifo_DOTrtl_DOTfifo__length_)
| p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X1))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X1))
| p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTlevel_(X1),n0)
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(X1)) ),
inference(rw,[status(thm)],[i_0_149,c_0_138]),
[final] ).
cnf(i_0_192,plain,
( fwork_DOTfifo_DOTrtl_DOTwr__level_(f_ADD_(X1,n1)) = fstd_DOTstandard_DOTmod_(f_ADD_(fwork_DOTfifo_DOTrtl_DOTwr__level_(X1),n1),fwork_DOTfifo_DOTrtl_DOTfifo__length_)
| p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X1))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(X1))
| p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,fwork_DOTfifo_DOTrtl_DOTlevel_(X1))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X1)) ),
inference(rw,[status(thm)],[i_0_150,c_0_138]),
[final] ).
cnf(i_0_193,axiom,
( p__pred_(fwork_DOTfifo_DOTrtl_DOTrd__error_(X1))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(X1))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X1))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X1))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTrd__error_(f_ADD_(X1,n1))) ),
axiom_53,
[final] ).
cnf(i_0_194,plain,
( p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X1))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTrd__error_(f_ADD_(X1,n1)))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(X1))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X1))
| ~ p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTlevel_(X1),n0) ),
inference(rw,[status(thm)],[i_0_151,c_0_138]),
[final] ).
cnf(i_0_195,axiom,
( f__index_(f__concat_(X1,X3),X2) = f__index_(X3,f_SUB_(X2,length(X1)))
| ~ p_LES_EQU_(length(X1),X2) ),
axiom_87,
[final] ).
cnf(i_0_196,plain,
( p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X1))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X1))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTrd__error_(f_ADD_(X1,n1)))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(X1))
| ~ p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTlevel_(X1),n0) ),
inference(rw,[status(thm)],[i_0_152,c_0_138]),
[final] ).
cnf(i_0_197,plain,
( p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X1))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(X1))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTwr__error_(f_ADD_(X1,n1)))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X1))
| ~ p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,fwork_DOTfifo_DOTrtl_DOTlevel_(X1)) ),
inference(rw,[status(thm)],[i_0_153,c_0_138]),
[final] ).
cnf(i_0_198,axiom,
( p__pred_(fwork_DOTfifo_DOTrtl_DOTwr__error_(X1))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X1))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X1))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTwr__error_(f_ADD_(X1,n1))) ),
axiom_56,
[final] ).
cnf(i_0_199,plain,
( fwork_DOTfifo_DOTrtl_DOTlevel_(f_ADD_(X1,n1)) = f_ADD_(fwork_DOTfifo_DOTrtl_DOTlevel_(X1),n1)
| p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X1))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(X1))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X1))
| ~ p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTlevel_(X1),n0) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_154,c_0_138]),c_0_138]),c_0_138]),
[final] ).
cnf(i_0_200,axiom,
( fwork_DOTfifo_DOTrtl_DOTwr__level_(f_ADD_(X1,n1)) = fstd_DOTstandard_DOTmod_(f_ADD_(fwork_DOTfifo_DOTrtl_DOTwr__level_(X1),n1),fwork_DOTfifo_DOTrtl_DOTfifo__length_)
| p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X1))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(X1))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X1)) ),
axiom_30,
[final] ).
cnf(i_0_201,axiom,
( p__pred_(fwork_DOTfifo_DOTrtl_DOTrd__error_(f_ADD_(X1,n1)))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(X1))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X1))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTrd__error_(X1))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X1)) ),
axiom_28,
[final] ).
cnf(i_0_202,axiom,
( p_LES_EQU_(X1,X2)
| ~ p_LES_EQU_(f_ADD_(X1,n1),f_ADD_(X2,n1)) ),
axiom_66,
[final] ).
cnf(i_0_203,axiom,
f__index_(f__xnor_(X1,X2),X3) = f__xnor_(f__index_(X1,X3),f__index_(X2,X3)),
axiom_94,
[final] ).
cnf(i_0_204,axiom,
f__index_(f__nor_(X1,X2),X3) = f__nor_(f__index_(X1,X3),f__index_(X2,X3)),
axiom_93,
[final] ).
cnf(i_0_205,axiom,
f__index_(f__nand_(X1,X2),X3) = f__nand_(f__index_(X1,X3),f__index_(X2,X3)),
axiom_92,
[final] ).
cnf(i_0_206,axiom,
f__index_(f__xor_(X1,X2),X3) = f__xor_(f__index_(X1,X3),f__index_(X2,X3)),
axiom_91,
[final] ).
cnf(i_0_207,axiom,
f__index_(f__or_(X1,X2),X3) = f__or_(f__index_(X1,X3),f__index_(X2,X3)),
axiom_90,
[final] ).
cnf(i_0_208,axiom,
f__index_(f__and_(X1,X2),X3) = f__and_(f__index_(X1,X3),f__index_(X2,X3)),
axiom_89,
[final] ).
cnf(i_0_209,axiom,
( ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTrd__error_(f_ADD_(X1,n1)))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X1)) ),
axiom_14,
[final] ).
cnf(i_0_210,axiom,
( ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTwr__error_(f_ADD_(X1,n1)))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X1)) ),
axiom_13,
[final] ).
cnf(i_0_211,plain,
( fwork_DOTfifo_DOTrtl_DOTrd__level_(f_ADD_(X1,n1)) = fwork_DOTfifo_DOTrtl_DOTrd__level_(X1)
| p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X1))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(X1))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X1))
| ~ p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTlevel_(X1),n0) ),
inference(rw,[status(thm)],[i_0_155,c_0_138]),
[final] ).
cnf(i_0_212,axiom,
( p__pred_(fwork_DOTfifo_DOTrtl_DOTrd__error_(f_ADD_(X1,n1)))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(X1))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X1))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X1))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTrd__error_(X1)) ),
axiom_54,
[final] ).
cnf(i_0_213,plain,
( fwork_DOTfifo_DOTrtl_DOTlevel_(f_ADD_(X1,n1)) = f_SUB_(fwork_DOTfifo_DOTrtl_DOTlevel_(X1),n1)
| p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X1))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X1))
| p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTlevel_(X1),n0)
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(X1)) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_156,c_0_138]),c_0_138]),c_0_138]),
[final] ).
cnf(i_0_214,plain,
( fwork_DOTfifo_DOTrtl_DOTlevel_(f_ADD_(X1,n1)) = f_ADD_(fwork_DOTfifo_DOTrtl_DOTlevel_(X1),n1)
| p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X1))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(X1))
| p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,fwork_DOTfifo_DOTrtl_DOTlevel_(X1))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X1)) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_157,c_0_138]),c_0_138]),c_0_138]),
[final] ).
cnf(i_0_215,plain,
( fwork_DOTfifo_DOTrtl_DOTrd__level_(f_ADD_(X1,n1)) = fwork_DOTfifo_DOTrtl_DOTrd__level_(X1)
| p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X1))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X1))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(X1))
| ~ p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTlevel_(X1),n0) ),
inference(rw,[status(thm)],[i_0_158,c_0_138]),
[final] ).
cnf(i_0_216,plain,
( fwork_DOTfifo_DOTrtl_DOTlevel_(f_ADD_(X1,n1)) = fwork_DOTfifo_DOTrtl_DOTlevel_(X1)
| p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X1))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X1))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(X1))
| ~ p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTlevel_(X1),n0) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_159,c_0_138]),c_0_138]),c_0_138]),
[final] ).
cnf(i_0_217,plain,
( fwork_DOTfifo_DOTrtl_DOTwr__level_(f_ADD_(X1,n1)) = fwork_DOTfifo_DOTrtl_DOTwr__level_(X1)
| p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X1))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(X1))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X1))
| ~ p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,fwork_DOTfifo_DOTrtl_DOTlevel_(X1)) ),
inference(rw,[status(thm)],[i_0_160,c_0_138]),
[final] ).
cnf(i_0_218,plain,
( fwork_DOTfifo_DOTrtl_DOTlevel_(f_ADD_(X1,n1)) = fwork_DOTfifo_DOTrtl_DOTlevel_(X1)
| p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X1))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(X1))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X1))
| ~ p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,fwork_DOTfifo_DOTrtl_DOTlevel_(X1)) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_161,c_0_138]),c_0_138]),c_0_138]),
[final] ).
cnf(i_0_219,plain,
( fwork_DOTfifo_DOTrtl_DOTlevel_(f_ADD_(X1,n1)) = fwork_DOTfifo_DOTrtl_DOTlevel_(X1)
| p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X1))
| p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTlevel_(X1),n0)
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(X1))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X1)) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_162,c_0_138]),c_0_138]),c_0_138]),
[final] ).
cnf(i_0_220,axiom,
( p__pred_(fwork_DOTfifo_DOTrtl_DOTwr__error_(f_ADD_(X1,n1)))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X1))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X1))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTwr__error_(X1)) ),
axiom_57,
[final] ).
cnf(i_0_221,axiom,
( p_LES_EQU_(X1,n0)
| f__index_(f__cons_(X2,X3),X1) = f__index_(X3,f_SUB_(X1,n1)) ),
axiom_85,
[final] ).
cnf(i_0_222,axiom,
( f_ADD_(X1,n1) = X2
| p_LES_EQU_(X2,X1)
| ~ p_LES_EQU_(X2,f_ADD_(X1,n1)) ),
axiom_72,
[final] ).
cnf(i_0_223,axiom,
( p_LES_EQU_(f_ADD_(X1,n1),f_ADD_(X2,n1))
| ~ p_LES_EQU_(X1,X2) ),
axiom_67,
[final] ).
cnf(i_0_224,axiom,
( p_LES_EQU_(length(X1),X2)
| f__index_(f__concat_(X1,X3),X2) = f__index_(X1,X2) ),
axiom_86,
[final] ).
cnf(i_0_225,axiom,
( p_LES_EQU_(X1,n0)
| ~ p_LES_EQU_(X1,f_SUB_(X1,n1)) ),
axiom_61,
[final] ).
cnf(i_0_226,axiom,
( ~ p_LES_EQU_(X1,X2)
| ~ p__pred_(f__gt_(X1,X2)) ),
axiom_131,
[final] ).
cnf(i_0_227,axiom,
( ~ p_LES_EQU_(X1,X2)
| ~ p__pred_(f__lt_(X2,X1)) ),
axiom_127,
[final] ).
cnf(i_0_228,axiom,
( fwork_DOTfifo_DOTrtl_DOTrd__level_(f_ADD_(X1,n1)) = fwork_DOTfifo_DOTrtl_DOTrd__level_(X1)
| p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(X1))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X1))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X1)) ),
axiom_17,
[final] ).
cnf(i_0_229,axiom,
( fwork_DOTfifo_DOTrtl_DOTrd__level_(f_ADD_(X1,n1)) = fwork_DOTfifo_DOTrtl_DOTrd__level_(X1)
| p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(X1))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X1))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X1)) ),
axiom_52,
[final] ).
cnf(i_0_230,plain,
( fwork_DOTfifo_DOTrtl_DOTlevel_(f_ADD_(X1,n1)) = fwork_DOTfifo_DOTrtl_DOTlevel_(X1)
| p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X1))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(X1))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X1)) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_163,c_0_138]),c_0_138]),
[final] ).
cnf(i_0_231,axiom,
( X1 = X2
| p_LES_EQU_(f_ADD_(X1,n1),X2)
| ~ p_LES_EQU_(X1,X2) ),
axiom_69,
[final] ).
cnf(i_0_232,axiom,
( X1 = X2
| p_LES_EQU_(f_ADD_(X2,n1),X1)
| ~ p_LES_EQU_(X2,X1) ),
axiom_68,
[final] ).
cnf(i_0_233,axiom,
( p_LES_EQU_(X1,X2)
| ~ p__pred_(f__geq_(X2,X1)) ),
axiom_133,
[final] ).
cnf(i_0_234,axiom,
( p_LES_EQU_(X1,X2)
| ~ p__pred_(f__leq_(X1,X2)) ),
axiom_129,
[final] ).
cnf(i_0_235,axiom,
( ~ p__pred_(X1)
| ~ p__pred_(X2)
| ~ p__pred_(f__nand_(X1,X2)) ),
axiom_115,
[final] ).
cnf(i_0_236,axiom,
( ~ p__pred_(X1)
| ~ p__pred_(X2)
| ~ p__pred_(f__xor_(X2,X1)) ),
axiom_111,
[final] ).
cnf(i_0_237,axiom,
( p__pred_(X1)
| ~ p__pred_(X2)
| ~ p__pred_(f__equiv_(X2,X1)) ),
axiom_99,
[final] ).
cnf(i_0_238,axiom,
( p__pred_(X1)
| ~ p__pred_(X2)
| ~ p__pred_(f__xnor_(X2,X1)) ),
axiom_121,
[final] ).
cnf(i_0_239,axiom,
( p__pred_(X2)
| ~ p__pred_(X1)
| ~ p__pred_(f__equiv_(X2,X1)) ),
axiom_100,
[final] ).
cnf(i_0_240,axiom,
( p__pred_(X2)
| ~ p__pred_(X1)
| ~ p__pred_(f__xnor_(X2,X1)) ),
axiom_122,
[final] ).
cnf(i_0_241,axiom,
( p__pred_(X1)
| p__pred_(X2)
| ~ p__pred_(f__xor_(X2,X1)) ),
axiom_112,
[final] ).
cnf(i_0_242,axiom,
( p__pred_(X1)
| p__pred_(X2)
| ~ p__pred_(f__or_(X1,X2)) ),
axiom_108,
[final] ).
cnf(i_0_243,axiom,
f__length_(f__concat_(X1,X2)) = f_ADD_(f__length_(X1),f__length_(X2)),
axiom_81,
[final] ).
cnf(i_0_244,axiom,
~ p_LES_EQU_(f_ADD_(X1,n1),n0),
axiom_60,
[final] ).
cnf(i_0_245,axiom,
( ~ p__pred_(X1)
| ~ p__pred_(f__nor_(X1,X2)) ),
axiom_119,
[final] ).
cnf(i_0_246,axiom,
( ~ p__pred_(X1)
| ~ p__pred_(f__nor_(X2,X1)) ),
axiom_118,
[final] ).
cnf(i_0_247,axiom,
( def_89(X1,X2)
| f_ADD_(X3,X1) = X2
| f_SUB_(X2,X1) != X3 ),
axiom_62,
[final] ).
cnf(i_0_248,axiom,
( def_89(X1,X2)
| f_SUB_(X2,X1) = X3
| f_ADD_(X3,X1) != X2 ),
axiom_63,
[final] ).
cnf(i_0_249,axiom,
( p__pred_(f__geq_(X2,X1))
| ~ p_LES_EQU_(X1,X2) ),
axiom_134,
[final] ).
cnf(i_0_250,axiom,
( p__pred_(f__leq_(X1,X2))
| ~ p_LES_EQU_(X1,X2) ),
axiom_130,
[final] ).
cnf(i_0_251,axiom,
( fwork_DOTfifo_DOTrtl_DOTwr__level_(f_ADD_(X1,n1)) = fwork_DOTfifo_DOTrtl_DOTwr__level_(X1)
| p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X1))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X1)) ),
axiom_42,
[final] ).
cnf(i_0_252,axiom,
( p__pred_(X1)
| ~ p__pred_(f__and_(X1,X2)) ),
axiom_106,
[final] ).
cnf(i_0_253,axiom,
( p__pred_(X1)
| ~ p__pred_(f__and_(X2,X1)) ),
axiom_105,
[final] ).
cnf(i_0_254,axiom,
( p_LES_EQU_(X3,X2)
| p_LES_EQU_(X1,X3)
| ~ p_LES_EQU_(X1,X2) ),
axiom_71,
[final] ).
cnf(i_0_255,negated_conjecture,
p__pred_(fwork_DOTfifo_DOTrtl_DOTwr__error_(f_ADD_(t_206,n1))),
quest_3,
[final] ).
cnf(i_0_256,axiom,
f__index_(f__not_(X1),X2) = f__not_(f__index_(X1,X2)),
axiom_95,
[final] ).
cnf(i_0_257,axiom,
( X1 = X2
| ~ p__pred_(f__equal_(X1,X2)) ),
axiom_103,
[final] ).
cnf(i_0_258,axiom,
f__length_(f__cons_(X1,X2)) = f_ADD_(f__length_(X2),n1),
axiom_79,
[final] ).
cnf(i_0_259,axiom,
( X1 = X2
| ~ p_LES_EQU_(X1,X2)
| ~ p_LES_EQU_(X2,X1) ),
axiom_70,
[final] ).
cnf(i_0_260,axiom,
( p_LES_EQU_(X1,X2)
| p__pred_(f__gt_(X1,X2)) ),
axiom_132,
[final] ).
cnf(i_0_261,axiom,
( p_LES_EQU_(X1,X2)
| p__pred_(f__lt_(X2,X1)) ),
axiom_128,
[final] ).
cnf(i_0_262,axiom,
( p__pred_(f__equiv_(X2,X1))
| ~ p__pred_(X1)
| ~ p__pred_(X2) ),
axiom_101,
[final] ).
cnf(i_0_263,axiom,
( p__pred_(f__xnor_(X2,X1))
| ~ p__pred_(X1)
| ~ p__pred_(X2) ),
axiom_123,
[final] ).
cnf(i_0_264,axiom,
( p__pred_(f__and_(X1,X2))
| ~ p__pred_(X1)
| ~ p__pred_(X2) ),
axiom_107,
[final] ).
cnf(i_0_265,axiom,
( fwork_DOTfifo_DOTrtl_DOTwr__level_(f_ADD_(X1,n1)) = n0
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X1)) ),
axiom_11,
[final] ).
cnf(i_0_266,axiom,
( fwork_DOTfifo_DOTrtl_DOTrd__level_(f_ADD_(X1,n1)) = n0
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X1)) ),
axiom_10,
[final] ).
cnf(i_0_267,plain,
( fwork_DOTfifo_DOTrtl_DOTlevel_(f_ADD_(X1,n1)) = n0
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X1)) ),
inference(rw,[status(thm)],[i_0_164,c_0_138]),
[final] ).
cnf(i_0_268,axiom,
( f__index_(f__cons_(X2,X3),X1) = X2
| X1 != n0 ),
axiom_84,
[final] ).
cnf(i_0_269,axiom,
f__length_(fwork_DOTfifo_DOTrtl_DOTdata__in_(X1)) = f_ADD_(f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__width_,n1),n1),
axiom_4,
[final] ).
cnf(i_0_270,axiom,
f__length_(fwork_DOTfifo_DOTrtl_DOTdata__out_(X1)) = f_ADD_(f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__width_,n1),n1),
axiom_3,
[final] ).
cnf(i_0_271,axiom,
f__length_(fwork_DOTfifo_DOTrtl_DOTmem_(X1)) = f_ADD_(f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,n1),n1),
axiom_2,
[final] ).
cnf(i_0_272,axiom,
( p__pred_(X1)
| p__pred_(f__xor_(X2,X1))
| ~ p__pred_(X2) ),
axiom_113,
[final] ).
cnf(i_0_273,axiom,
( p__pred_(X2)
| p__pred_(f__xor_(X2,X1))
| ~ p__pred_(X1) ),
axiom_114,
[final] ).
cnf(i_0_274,axiom,
( X1 = X2
| f_ADD_(X1,n1) != f_ADD_(X2,n1) ),
axiom_76,
[final] ).
cnf(i_0_275,axiom,
( p__pred_(X1)
| p__pred_(X2)
| p__pred_(f__equiv_(X2,X1)) ),
axiom_102,
[final] ).
cnf(i_0_276,axiom,
( p__pred_(X1)
| p__pred_(X2)
| p__pred_(f__xnor_(X2,X1)) ),
axiom_124,
[final] ).
cnf(i_0_277,axiom,
( p__pred_(X1)
| p__pred_(X2)
| p__pred_(f__nor_(X1,X2)) ),
axiom_120,
[final] ).
cnf(i_0_278,axiom,
( p__pred_(f__or_(X1,X2))
| ~ p__pred_(X1) ),
axiom_110,
[final] ).
cnf(i_0_279,axiom,
( p__pred_(f__or_(X2,X1))
| ~ p__pred_(X1) ),
axiom_109,
[final] ).
cnf(i_0_280,axiom,
( p_LES_EQU_(X1,X2)
| ~ def_89(X2,X1) ),
axiom_65,
[final] ).
cnf(i_0_281,axiom,
( p__pred_(X1)
| p__pred_(f__nand_(X1,X2)) ),
axiom_117,
[final] ).
cnf(i_0_282,axiom,
( p__pred_(X1)
| p__pred_(f__nand_(X2,X1)) ),
axiom_116,
[final] ).
cnf(i_0_283,axiom,
( p__pred_(f__equal_(X1,X2))
| X1 != X2 ),
axiom_104,
[final] ).
cnf(i_0_284,axiom,
( X1 != X2
| ~ def_89(X2,X1) ),
axiom_64,
[final] ).
cnf(i_0_285,axiom,
( ~ p__pred_(X1)
| ~ p__pred_(f__not_(X1)) ),
axiom_125,
[final] ).
cnf(i_0_286,axiom,
( X1 = n0
| ~ p_LES_EQU_(X1,n0) ),
axiom_73,
[final] ).
cnf(i_0_287,plain,
( fwork_DOTfifo_DOTrtl_DOTlevel_(X1) = n0
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTempty_(X1)) ),
inference(rw,[status(thm)],[i_0_165,c_0_138]),
[final] ).
cnf(i_0_288,plain,
( fwork_DOTfifo_DOTrtl_DOTlevel_(X1) = fwork_DOTfifo_DOTrtl_DOTfifo__length_
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTfull_(X1)) ),
inference(rw,[status(thm)],[i_0_166,c_0_138]),
[final] ).
cnf(i_0_289,axiom,
( X1 = f_ADD_(y_105(X1),n1)
| X1 = n0 ),
axiom_74,
[final] ).
cnf(i_0_290,axiom,
f__index_(f__others_(X1),X2) = X1,
axiom_83,
[final] ).
cnf(i_0_291,axiom,
f_ADD_(X1,n1) != n0,
axiom_59,
[final] ).
cnf(i_0_292,plain,
( p__pred_(fwork_DOTfifo_DOTrtl_DOTempty_(X1))
| fwork_DOTfifo_DOTrtl_DOTlevel_(X1) != n0 ),
inference(rw,[status(thm)],[i_0_167,c_0_138]),
[final] ).
cnf(i_0_293,plain,
( p__pred_(fwork_DOTfifo_DOTrtl_DOTfull_(X1))
| fwork_DOTfifo_DOTrtl_DOTlevel_(X1) != fwork_DOTfifo_DOTrtl_DOTfifo__length_ ),
inference(rw,[status(thm)],[i_0_168,c_0_138]),
[final] ).
cnf(i_0_294,axiom,
( p__pred_(X1)
| p__pred_(f__not_(X1)) ),
axiom_126,
[final] ).
cnf(i_0_295,axiom,
p_LES_EQU_(X1,X1),
axiom_75,
[final] ).
cnf(i_0_296,axiom,
f_ADD_(n0,X1) = X1,
axiom_77,
[final] ).
cnf(i_0_297,negated_conjecture,
~ p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(t_206)),
quest_1,
[final] ).
cnf(i_0_298,negated_conjecture,
~ p__pred_(fwork_DOTfifo_DOTrtl_DOTwr__error_(t_206)),
quest_4,
[final] ).
cnf(i_0_299,negated_conjecture,
~ p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(t_206)),
quest_2,
[final] ).
cnf(i_0_300,axiom,
n1 = f_ADD_(n0,n1),
axiom_78,
[final] ).
cnf(i_0_301,axiom,
~ p__pred_(f__false_),
axiom_97,
[final] ).
cnf(i_0_302,axiom,
p__pred_(f__true_),
axiom_96,
[final] ).
cnf(i_0_303,axiom,
f__length_(f__empty_) = n0,
axiom_80,
[final] ).
cnf(i_0_304,axiom,
f__false_ != f__true_,
axiom_98,
[final] ).
cnf(i_0_305,axiom,
X1 = X1 ).
cnf(i_0_306,axiom,
( X1 = X2
| X2 != X1 ) ).
cnf(i_0_307,axiom,
( X1 = X2
| X1 != X3
| X3 != X2 ) ).
cnf(i_0_308,axiom,
( X1 != X2
| f__index_(X1,X3) = f__index_(X2,X3) ) ).
cnf(i_0_309,axiom,
( X1 != X2
| f__index_(X3,X1) = f__index_(X3,X2) ) ).
cnf(i_0_310,axiom,
( X1 != X2
| fwork_DOTfifo_DOTrtl_DOTrd__level_(X1) = fwork_DOTfifo_DOTrtl_DOTrd__level_(X2) ) ).
cnf(i_0_311,axiom,
( X1 != X2
| f__length_(X1) = f__length_(X2) ) ).
cnf(i_0_312,axiom,
( X1 != X2
| fstd_DOTstandard_DOTmod_(X1,X3) = fstd_DOTstandard_DOTmod_(X2,X3) ) ).
cnf(i_0_313,axiom,
( X1 != X2
| fstd_DOTstandard_DOTmod_(X3,X1) = fstd_DOTstandard_DOTmod_(X3,X2) ) ).
cnf(i_0_314,axiom,
( X1 != X2
| f__xnor_(X1,X3) = f__xnor_(X2,X3) ) ).
cnf(i_0_315,axiom,
( X1 != X2
| f__xnor_(X3,X1) = f__xnor_(X3,X2) ) ).
cnf(i_0_316,axiom,
( X1 != X2
| f__nor_(X1,X3) = f__nor_(X2,X3) ) ).
cnf(i_0_317,axiom,
( X1 != X2
| f__nor_(X3,X1) = f__nor_(X3,X2) ) ).
cnf(i_0_318,axiom,
( X1 != X2
| f__nand_(X1,X3) = f__nand_(X2,X3) ) ).
cnf(i_0_319,axiom,
( X1 != X2
| f__nand_(X3,X1) = f__nand_(X3,X2) ) ).
cnf(i_0_320,axiom,
( X1 != X2
| f__xor_(X1,X3) = f__xor_(X2,X3) ) ).
cnf(i_0_321,axiom,
( X1 != X2
| f__xor_(X3,X1) = f__xor_(X3,X2) ) ).
cnf(i_0_322,axiom,
( X1 != X2
| f__or_(X1,X3) = f__or_(X2,X3) ) ).
cnf(i_0_323,axiom,
( X1 != X2
| f__or_(X3,X1) = f__or_(X3,X2) ) ).
cnf(i_0_324,axiom,
( X1 != X2
| f__and_(X1,X3) = f__and_(X2,X3) ) ).
cnf(i_0_325,axiom,
( X1 != X2
| f__and_(X3,X1) = f__and_(X3,X2) ) ).
cnf(i_0_326,axiom,
( X1 != X2
| f_ADD_(X1,X3) = f_ADD_(X2,X3) ) ).
cnf(i_0_327,axiom,
( X1 != X2
| f_ADD_(X3,X1) = f_ADD_(X3,X2) ) ).
cnf(i_0_328,axiom,
( X1 != X2
| f__not_(X1) = f__not_(X2) ) ).
cnf(i_0_329,axiom,
( X1 != X2
| f_SUB_(X1,X3) = f_SUB_(X2,X3) ) ).
cnf(i_0_330,axiom,
( X1 != X2
| f_SUB_(X3,X1) = f_SUB_(X3,X2) ) ).
cnf(i_0_331,axiom,
( X1 != X2
| fwork_DOTfifo_DOTrtl_DOTwr__level_(X1) = fwork_DOTfifo_DOTrtl_DOTwr__level_(X2) ) ).
cnf(i_0_332,axiom,
( X1 != X2
| fwork_DOTfifo_DOTrtl_DOTlevel_(X1) = fwork_DOTfifo_DOTrtl_DOTlevel_(X2) ) ).
cnf(i_0_333,axiom,
( X1 != X2
| ~ p__pred_(X1)
| p__pred_(X2) ) ).
cnf(i_0_334,axiom,
( X1 != X2
| ~ p_LES_EQU_(X1,X3)
| p_LES_EQU_(X2,X3) ) ).
cnf(i_0_335,axiom,
( X1 != X2
| ~ p_LES_EQU_(X3,X1)
| p_LES_EQU_(X3,X2) ) ).
cnf(i_0_336,axiom,
( X1 != X2
| ~ def_89(X1,X3)
| def_89(X2,X3) ) ).
cnf(i_0_337,axiom,
( X1 != X2
| ~ def_89(X3,X1)
| def_89(X3,X2) ) ).
cnf(i_0_305_001,axiom,
X1 = X1 ).
cnf(i_0_306_002,axiom,
( X1 = X2
| X2 != X1 ) ).
cnf(i_0_307_003,axiom,
( X1 = X2
| X1 != X3
| X3 != X2 ) ).
cnf(i_0_308_004,axiom,
( X1 != X2
| f__index_(X1,X3) = f__index_(X2,X3) ) ).
cnf(i_0_309_005,axiom,
( X1 != X2
| f__index_(X3,X1) = f__index_(X3,X2) ) ).
cnf(i_0_310_006,axiom,
( X1 != X2
| fwork_DOTfifo_DOTrtl_DOTrd__level_(X1) = fwork_DOTfifo_DOTrtl_DOTrd__level_(X2) ) ).
cnf(i_0_311_007,axiom,
( X1 != X2
| f__length_(X1) = f__length_(X2) ) ).
cnf(i_0_312_008,axiom,
( X1 != X2
| fstd_DOTstandard_DOTmod_(X1,X3) = fstd_DOTstandard_DOTmod_(X2,X3) ) ).
cnf(i_0_313_009,axiom,
( X1 != X2
| fstd_DOTstandard_DOTmod_(X3,X1) = fstd_DOTstandard_DOTmod_(X3,X2) ) ).
cnf(i_0_314_010,axiom,
( X1 != X2
| f__xnor_(X1,X3) = f__xnor_(X2,X3) ) ).
cnf(i_0_315_011,axiom,
( X1 != X2
| f__xnor_(X3,X1) = f__xnor_(X3,X2) ) ).
cnf(i_0_316_012,axiom,
( X1 != X2
| f__nor_(X1,X3) = f__nor_(X2,X3) ) ).
cnf(i_0_317_013,axiom,
( X1 != X2
| f__nor_(X3,X1) = f__nor_(X3,X2) ) ).
cnf(i_0_318_014,axiom,
( X1 != X2
| f__nand_(X1,X3) = f__nand_(X2,X3) ) ).
cnf(i_0_319_015,axiom,
( X1 != X2
| f__nand_(X3,X1) = f__nand_(X3,X2) ) ).
cnf(i_0_320_016,axiom,
( X1 != X2
| f__xor_(X1,X3) = f__xor_(X2,X3) ) ).
cnf(i_0_321_017,axiom,
( X1 != X2
| f__xor_(X3,X1) = f__xor_(X3,X2) ) ).
cnf(i_0_322_018,axiom,
( X1 != X2
| f__or_(X1,X3) = f__or_(X2,X3) ) ).
cnf(i_0_323_019,axiom,
( X1 != X2
| f__or_(X3,X1) = f__or_(X3,X2) ) ).
cnf(i_0_324_020,axiom,
( X1 != X2
| f__and_(X1,X3) = f__and_(X2,X3) ) ).
cnf(i_0_325_021,axiom,
( X1 != X2
| f__and_(X3,X1) = f__and_(X3,X2) ) ).
cnf(i_0_326_022,axiom,
( X1 != X2
| f_ADD_(X1,X3) = f_ADD_(X2,X3) ) ).
cnf(i_0_327_023,axiom,
( X1 != X2
| f_ADD_(X3,X1) = f_ADD_(X3,X2) ) ).
cnf(i_0_328_024,axiom,
( X1 != X2
| f__not_(X1) = f__not_(X2) ) ).
cnf(i_0_329_025,axiom,
( X1 != X2
| f_SUB_(X1,X3) = f_SUB_(X2,X3) ) ).
cnf(i_0_330_026,axiom,
( X1 != X2
| f_SUB_(X3,X1) = f_SUB_(X3,X2) ) ).
cnf(i_0_331_027,axiom,
( X1 != X2
| fwork_DOTfifo_DOTrtl_DOTwr__level_(X1) = fwork_DOTfifo_DOTrtl_DOTwr__level_(X2) ) ).
cnf(i_0_332_028,axiom,
( X1 != X2
| fwork_DOTfifo_DOTrtl_DOTlevel_(X1) = fwork_DOTfifo_DOTrtl_DOTlevel_(X2) ) ).
cnf(i_0_333_029,axiom,
( X1 != X2
| ~ p__pred_(X1)
| p__pred_(X2) ) ).
cnf(i_0_334_030,axiom,
( X1 != X2
| ~ p_LES_EQU_(X1,X3)
| p_LES_EQU_(X2,X3) ) ).
cnf(i_0_335_031,axiom,
( X1 != X2
| ~ p_LES_EQU_(X3,X1)
| p_LES_EQU_(X3,X2) ) ).
cnf(i_0_336_032,axiom,
( X1 != X2
| ~ def_89(X1,X3)
| def_89(X2,X3) ) ).
cnf(i_0_337_033,axiom,
( X1 != X2
| ~ def_89(X3,X1)
| def_89(X3,X2) ) ).
cnf(i_0_338,plain,
( def_89(X1,X2)
| f_ADD_(f_SUB_(X2,X1),X1) = X2 ),
inference(equality_inference,[],[247]) ).
cnf(i_0_339,plain,
( def_89(X1,f_ADD_(X2,X1))
| f_SUB_(f_ADD_(X2,X1),X1) = X2 ),
inference(equality_inference,[],[248]) ).
cnf(i_0_340,plain,
f__index_(f__cons_(X1,X2),n0) = X1,
inference(equality_inference,[],[268]) ).
cnf(i_0_341,plain,
X1 = X1,
inference(equality_inference,[],[274]) ).
cnf(i_0_342,plain,
p__pred_(f__equal_(X1,X1)),
inference(equality_inference,[],[283]) ).
cnf(i_0_343,plain,
~ def_89(X1,X1),
inference(equality_inference,[],[284]) ).
cnf(i_0_344,plain,
$false,
inference(scs_inference,[],[i_0_298,i_0_297,i_0_299,i_0_255,i_0_198]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : HWV026-3 : TPTP v9.2.1. Released v2.5.0.
% 0.00/0.12 % Command : /export/starexec/sandbox/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox/solver/bin/cse --final-prover /export/starexec/sandbox/solver/bin/eprover --proof-time %d --global-time-limit %d
% 0.15/0.33 % Computer : n005.cluster.edu
% 0.15/0.33 % Model : x86_64 x86_64
% 0.15/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.33 % Memory : 8042.1875MB
% 0.15/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.34 % CPULimit : 300
% 0.15/0.34 % WCLimit : 300
% 0.15/0.34 % DateTime : Mon May 4 19:11:15 EDT 2026
% 0.15/0.34 % CPUTime :
% 0.15/0.35 % start to proof: theBenchmark
% 0.33/1.62 % Version : CSE_E---1.7
% 0.33/1.62 % Problem : theBenchmark.p
% 0.33/1.62 % SZS status Unsatisfiable for theBenchmark.p
% 0.33/1.62 % SZS output start CNFRefutation
% See solution above
% 0.33/1.65 % Total time : 1.272s
%------------------------------------------------------------------------------