%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : HWV029-2 : 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 : n020.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:01 PM UTC 2026
% Result : Unsatisfiable 209.72s 135.78s
% Output : CNFRefutation 226.84s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named c_0_137)
% 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(quest_2,negated_conjecture,
~ p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTlevel_(f_ADD_(t_206,n1)),fwork_DOTfifo_DOTrtl_DOTfifo__length_),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',quest_2) ).
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(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(quest_3,negated_conjecture,
~ p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,n0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',quest_3) ).
cnf(quest_1,negated_conjecture,
p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTlevel_(t_206),fwork_DOTfifo_DOTrtl_DOTfifo__length_),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',quest_1) ).
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(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_136,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_137,axiom,
fwork_DOTfifo_DOTrtl_DOTlevel_(X1) = fwork_DOTfifo_DOTrtl_DOTint__level_(X1),
axiom_5 ).
cnf(i_0_138,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_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)
| 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_140,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_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_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_142,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_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_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_144,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_145,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_146,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_147,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_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_DOTwr_(X1))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X1))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(X1)) ),
axiom_44 ).
cnf(i_0_149,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_150,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_151,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_152,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_153,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_154,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_155,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_156,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_157,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_158,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_159,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_160,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_161,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_162,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_163,axiom,
( fwork_DOTfifo_DOTrtl_DOTint__level_(f_ADD_(X1,n1)) = n0
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X1)) ),
axiom_12 ).
cnf(i_0_164,axiom,
( fwork_DOTfifo_DOTrtl_DOTint__level_(X1) = n0
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTempty_(X1)) ),
axiom_9 ).
cnf(i_0_165,axiom,
( fwork_DOTfifo_DOTrtl_DOTint__level_(X1) = fwork_DOTfifo_DOTrtl_DOTfifo__length_
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTfull_(X1)) ),
axiom_7 ).
cnf(i_0_166,axiom,
( p__pred_(fwork_DOTfifo_DOTrtl_DOTempty_(X1))
| fwork_DOTfifo_DOTrtl_DOTint__level_(X1) != n0 ),
axiom_8 ).
cnf(i_0_167,axiom,
( p__pred_(fwork_DOTfifo_DOTrtl_DOTfull_(X1))
| fwork_DOTfifo_DOTrtl_DOTint__level_(X1) != fwork_DOTfifo_DOTrtl_DOTfifo__length_ ),
axiom_6 ).
cnf(i_0_168,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_169,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_136,c_0_137]),
[final] ).
cnf(i_0_170,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_138,c_0_137]),
[final] ).
cnf(i_0_171,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_172,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_173,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_139,c_0_137]),
[final] ).
cnf(i_0_174,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_140,c_0_137]),
[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__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_141,c_0_137]),
[final] ).
cnf(i_0_176,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_177,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_178,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_142,c_0_137]),
[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_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_143,c_0_137]),
[final] ).
cnf(i_0_180,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_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_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_182,axiom,
f__index_(f__slice_(X1,X2,X3),X4) = f__index_(X1,f_ADD_(X4,X2)),
axiom_88,
[final] ).
cnf(i_0_183,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_144,c_0_137]),
[final] ).
cnf(i_0_184,axiom,
f__length_(f__slice_(X1,X2,X3)) = f_SUB_(X3,f_ADD_(X2,n1)),
axiom_82,
[final] ).
cnf(i_0_185,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_145,c_0_137]),
[final] ).
cnf(i_0_186,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_146,c_0_137]),
[final] ).
cnf(i_0_187,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_147,c_0_137]),
[final] ).
cnf(i_0_188,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_189,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_190,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_148,c_0_137]),
[final] ).
cnf(i_0_191,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_149,c_0_137]),
[final] ).
cnf(i_0_192,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_193,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_150,c_0_137]),
[final] ).
cnf(i_0_194,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_195,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_151,c_0_137]),
[final] ).
cnf(i_0_196,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_152,c_0_137]),
[final] ).
cnf(i_0_197,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_198,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_153,c_0_137]),c_0_137]),c_0_137]),
[final] ).
cnf(i_0_199,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_200,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_201,axiom,
( p_LES_EQU_(X1,X2)
| ~ p_LES_EQU_(f_ADD_(X1,n1),f_ADD_(X2,n1)) ),
axiom_66,
[final] ).
cnf(i_0_202,axiom,
f__index_(f__xnor_(X1,X2),X3) = f__xnor_(f__index_(X1,X3),f__index_(X2,X3)),
axiom_94,
[final] ).
cnf(i_0_203,axiom,
f__index_(f__nor_(X1,X2),X3) = f__nor_(f__index_(X1,X3),f__index_(X2,X3)),
axiom_93,
[final] ).
cnf(i_0_204,axiom,
f__index_(f__nand_(X1,X2),X3) = f__nand_(f__index_(X1,X3),f__index_(X2,X3)),
axiom_92,
[final] ).
cnf(i_0_205,axiom,
f__index_(f__xor_(X1,X2),X3) = f__xor_(f__index_(X1,X3),f__index_(X2,X3)),
axiom_91,
[final] ).
cnf(i_0_206,axiom,
f__index_(f__or_(X1,X2),X3) = f__or_(f__index_(X1,X3),f__index_(X2,X3)),
axiom_90,
[final] ).
cnf(i_0_207,axiom,
f__index_(f__and_(X1,X2),X3) = f__and_(f__index_(X1,X3),f__index_(X2,X3)),
axiom_89,
[final] ).
cnf(i_0_208,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_209,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_210,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_154,c_0_137]),
[final] ).
cnf(i_0_211,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_212,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_155,c_0_137]),c_0_137]),c_0_137]),
[final] ).
cnf(i_0_213,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_156,c_0_137]),c_0_137]),c_0_137]),
[final] ).
cnf(i_0_214,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_157,c_0_137]),
[final] ).
cnf(i_0_215,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_158,c_0_137]),c_0_137]),c_0_137]),
[final] ).
cnf(i_0_216,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_159,c_0_137]),
[final] ).
cnf(i_0_217,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_160,c_0_137]),c_0_137]),c_0_137]),
[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_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_161,c_0_137]),c_0_137]),c_0_137]),
[final] ).
cnf(i_0_219,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_220,negated_conjecture,
~ p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTlevel_(f_ADD_(t_206,n1)),fwork_DOTfifo_DOTrtl_DOTfifo__length_),
quest_2,
[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_162,c_0_137]),c_0_137]),
[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,axiom,
f__index_(f__not_(X1),X2) = f__not_(f__index_(X1,X2)),
axiom_95,
[final] ).
cnf(i_0_256,axiom,
( X1 = X2
| ~ p__pred_(f__equal_(X1,X2)) ),
axiom_103,
[final] ).
cnf(i_0_257,axiom,
f__length_(f__cons_(X1,X2)) = f_ADD_(f__length_(X2),n1),
axiom_79,
[final] ).
cnf(i_0_258,axiom,
( X1 = X2
| ~ p_LES_EQU_(X1,X2)
| ~ p_LES_EQU_(X2,X1) ),
axiom_70,
[final] ).
cnf(i_0_259,axiom,
( p_LES_EQU_(X1,X2)
| p__pred_(f__gt_(X1,X2)) ),
axiom_132,
[final] ).
cnf(i_0_260,axiom,
( p_LES_EQU_(X1,X2)
| p__pred_(f__lt_(X2,X1)) ),
axiom_128,
[final] ).
cnf(i_0_261,axiom,
( p__pred_(f__equiv_(X2,X1))
| ~ p__pred_(X1)
| ~ p__pred_(X2) ),
axiom_101,
[final] ).
cnf(i_0_262,axiom,
( p__pred_(f__xnor_(X2,X1))
| ~ p__pred_(X1)
| ~ p__pred_(X2) ),
axiom_123,
[final] ).
cnf(i_0_263,axiom,
( p__pred_(f__and_(X1,X2))
| ~ p__pred_(X1)
| ~ p__pred_(X2) ),
axiom_107,
[final] ).
cnf(i_0_264,axiom,
( fwork_DOTfifo_DOTrtl_DOTwr__level_(f_ADD_(X1,n1)) = n0
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X1)) ),
axiom_11,
[final] ).
cnf(i_0_265,axiom,
( fwork_DOTfifo_DOTrtl_DOTrd__level_(f_ADD_(X1,n1)) = n0
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X1)) ),
axiom_10,
[final] ).
cnf(i_0_266,plain,
( fwork_DOTfifo_DOTrtl_DOTlevel_(f_ADD_(X1,n1)) = n0
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X1)) ),
inference(rw,[status(thm)],[i_0_163,c_0_137]),
[final] ).
cnf(i_0_267,axiom,
( f__index_(f__cons_(X2,X3),X1) = X2
| X1 != n0 ),
axiom_84,
[final] ).
cnf(i_0_268,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_269,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_270,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_271,axiom,
( p__pred_(X1)
| p__pred_(f__xor_(X2,X1))
| ~ p__pred_(X2) ),
axiom_113,
[final] ).
cnf(i_0_272,axiom,
( p__pred_(X2)
| p__pred_(f__xor_(X2,X1))
| ~ p__pred_(X1) ),
axiom_114,
[final] ).
cnf(i_0_273,axiom,
( X1 = X2
| f_ADD_(X1,n1) != f_ADD_(X2,n1) ),
axiom_76,
[final] ).
cnf(i_0_274,axiom,
( p__pred_(X1)
| p__pred_(X2)
| p__pred_(f__equiv_(X2,X1)) ),
axiom_102,
[final] ).
cnf(i_0_275,axiom,
( p__pred_(X1)
| p__pred_(X2)
| p__pred_(f__xnor_(X2,X1)) ),
axiom_124,
[final] ).
cnf(i_0_276,axiom,
( p__pred_(X1)
| p__pred_(X2)
| p__pred_(f__nor_(X1,X2)) ),
axiom_120,
[final] ).
cnf(i_0_277,axiom,
( p__pred_(f__or_(X1,X2))
| ~ p__pred_(X1) ),
axiom_110,
[final] ).
cnf(i_0_278,axiom,
( p__pred_(f__or_(X2,X1))
| ~ p__pred_(X1) ),
axiom_109,
[final] ).
cnf(i_0_279,axiom,
( p_LES_EQU_(X1,X2)
| ~ def_89(X2,X1) ),
axiom_65,
[final] ).
cnf(i_0_280,axiom,
( p__pred_(X1)
| p__pred_(f__nand_(X1,X2)) ),
axiom_117,
[final] ).
cnf(i_0_281,axiom,
( p__pred_(X1)
| p__pred_(f__nand_(X2,X1)) ),
axiom_116,
[final] ).
cnf(i_0_282,axiom,
( p__pred_(f__equal_(X1,X2))
| X1 != X2 ),
axiom_104,
[final] ).
cnf(i_0_283,axiom,
( X1 != X2
| ~ def_89(X2,X1) ),
axiom_64,
[final] ).
cnf(i_0_284,axiom,
( ~ p__pred_(X1)
| ~ p__pred_(f__not_(X1)) ),
axiom_125,
[final] ).
cnf(i_0_285,axiom,
( X1 = n0
| ~ p_LES_EQU_(X1,n0) ),
axiom_73,
[final] ).
cnf(i_0_286,plain,
( fwork_DOTfifo_DOTrtl_DOTlevel_(X1) = n0
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTempty_(X1)) ),
inference(rw,[status(thm)],[i_0_164,c_0_137]),
[final] ).
cnf(i_0_287,plain,
( fwork_DOTfifo_DOTrtl_DOTlevel_(X1) = fwork_DOTfifo_DOTrtl_DOTfifo__length_
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTfull_(X1)) ),
inference(rw,[status(thm)],[i_0_165,c_0_137]),
[final] ).
cnf(i_0_288,axiom,
( X1 = f_ADD_(y_105(X1),n1)
| X1 = n0 ),
axiom_74,
[final] ).
cnf(i_0_289,axiom,
f__index_(f__others_(X1),X2) = X1,
axiom_83,
[final] ).
cnf(i_0_290,axiom,
f_ADD_(X1,n1) != n0,
axiom_59,
[final] ).
cnf(i_0_291,negated_conjecture,
~ p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,n0),
quest_3,
[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_166,c_0_137]),
[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_167,c_0_137]),
[final] ).
cnf(i_0_294,negated_conjecture,
p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTlevel_(t_206),fwork_DOTfifo_DOTrtl_DOTfifo__length_),
quest_1,
[final] ).
cnf(i_0_295,axiom,
( p__pred_(X1)
| p__pred_(f__not_(X1)) ),
axiom_126,
[final] ).
cnf(i_0_296,axiom,
p_LES_EQU_(X1,X1),
axiom_75,
[final] ).
cnf(i_0_297,axiom,
f_ADD_(n0,X1) = X1,
axiom_77,
[final] ).
cnf(i_0_298,axiom,
n1 = f_ADD_(n0,n1),
axiom_78,
[final] ).
cnf(i_0_299,axiom,
~ p__pred_(f__false_),
axiom_97,
[final] ).
cnf(i_0_300,axiom,
p__pred_(f__true_),
axiom_96,
[final] ).
cnf(i_0_301,axiom,
f__length_(f__empty_) = n0,
axiom_80,
[final] ).
cnf(i_0_302,axiom,
f__false_ != f__true_,
axiom_98,
[final] ).
cnf(i_0_303,axiom,
X1 = X1 ).
cnf(i_0_304,axiom,
( X1 = X2
| X2 != X1 ) ).
cnf(i_0_305,axiom,
( X1 = X2
| X1 != X3
| X3 != X2 ) ).
cnf(i_0_306,axiom,
( X1 != X2
| f__index_(X1,X3) = f__index_(X2,X3) ) ).
cnf(i_0_307,axiom,
( X1 != X2
| f__index_(X3,X1) = f__index_(X3,X2) ) ).
cnf(i_0_308,axiom,
( X1 != X2
| fwork_DOTfifo_DOTrtl_DOTrd__level_(X1) = fwork_DOTfifo_DOTrtl_DOTrd__level_(X2) ) ).
cnf(i_0_309,axiom,
( X1 != X2
| f__length_(X1) = f__length_(X2) ) ).
cnf(i_0_310,axiom,
( X1 != X2
| fstd_DOTstandard_DOTmod_(X1,X3) = fstd_DOTstandard_DOTmod_(X2,X3) ) ).
cnf(i_0_311,axiom,
( X1 != X2
| fstd_DOTstandard_DOTmod_(X3,X1) = fstd_DOTstandard_DOTmod_(X3,X2) ) ).
cnf(i_0_312,axiom,
( X1 != X2
| f__xnor_(X1,X3) = f__xnor_(X2,X3) ) ).
cnf(i_0_313,axiom,
( X1 != X2
| f__xnor_(X3,X1) = f__xnor_(X3,X2) ) ).
cnf(i_0_314,axiom,
( X1 != X2
| f__nor_(X1,X3) = f__nor_(X2,X3) ) ).
cnf(i_0_315,axiom,
( X1 != X2
| f__nor_(X3,X1) = f__nor_(X3,X2) ) ).
cnf(i_0_316,axiom,
( X1 != X2
| f__nand_(X1,X3) = f__nand_(X2,X3) ) ).
cnf(i_0_317,axiom,
( X1 != X2
| f__nand_(X3,X1) = f__nand_(X3,X2) ) ).
cnf(i_0_318,axiom,
( X1 != X2
| f__xor_(X1,X3) = f__xor_(X2,X3) ) ).
cnf(i_0_319,axiom,
( X1 != X2
| f__xor_(X3,X1) = f__xor_(X3,X2) ) ).
cnf(i_0_320,axiom,
( X1 != X2
| f__or_(X1,X3) = f__or_(X2,X3) ) ).
cnf(i_0_321,axiom,
( X1 != X2
| f__or_(X3,X1) = f__or_(X3,X2) ) ).
cnf(i_0_322,axiom,
( X1 != X2
| f__and_(X1,X3) = f__and_(X2,X3) ) ).
cnf(i_0_323,axiom,
( X1 != X2
| f__and_(X3,X1) = f__and_(X3,X2) ) ).
cnf(i_0_324,axiom,
( X1 != X2
| f_ADD_(X1,X3) = f_ADD_(X2,X3) ) ).
cnf(i_0_325,axiom,
( X1 != X2
| f_ADD_(X3,X1) = f_ADD_(X3,X2) ) ).
cnf(i_0_326,axiom,
( X1 != X2
| f__not_(X1) = f__not_(X2) ) ).
cnf(i_0_327,axiom,
( X1 != X2
| f_SUB_(X1,X3) = f_SUB_(X2,X3) ) ).
cnf(i_0_328,axiom,
( X1 != X2
| f_SUB_(X3,X1) = f_SUB_(X3,X2) ) ).
cnf(i_0_329,axiom,
( X1 != X2
| fwork_DOTfifo_DOTrtl_DOTwr__level_(X1) = fwork_DOTfifo_DOTrtl_DOTwr__level_(X2) ) ).
cnf(i_0_330,axiom,
( X1 != X2
| fwork_DOTfifo_DOTrtl_DOTlevel_(X1) = fwork_DOTfifo_DOTrtl_DOTlevel_(X2) ) ).
cnf(i_0_331,axiom,
( X1 != X2
| ~ p__pred_(X1)
| p__pred_(X2) ) ).
cnf(i_0_332,axiom,
( X1 != X2
| ~ p_LES_EQU_(X1,X3)
| p_LES_EQU_(X2,X3) ) ).
cnf(i_0_333,axiom,
( X1 != X2
| ~ p_LES_EQU_(X3,X1)
| p_LES_EQU_(X3,X2) ) ).
cnf(i_0_334,axiom,
( X1 != X2
| ~ def_89(X1,X3)
| def_89(X2,X3) ) ).
cnf(i_0_335,axiom,
( X1 != X2
| ~ def_89(X3,X1)
| def_89(X3,X2) ) ).
cnf(i_0_821,plain,
~ p_LES_EQU_(f__index_(f__cons_(n1,X1),n0),f_SUB_(f_SUB_(X2,X2),f__index_(f__cons_(n0,X3),n0))),
inference(scs_inference,[],[i_0_681,i_0_405,i_0_811,i_0_465,i_0_304,i_0_248,i_0_332]) ).
cnf(i_0_823,plain,
f_ADD_(X1,n1) != f_ADD_(n0,f__index_(f__cons_(f_ADD_(n0,n0),X2),n0)),
inference(scs_inference,[],[i_0_681,i_0_535,i_0_405,i_0_506,i_0_811,i_0_465,i_0_304,i_0_248,i_0_332,i_0_305]) ).
cnf(i_0_825,plain,
n1 != f__index_(f__cons_(f_ADD_(n0,n0),X1),n0),
inference(scs_inference,[],[i_0_681,i_0_535,i_0_405,i_0_506,i_0_811,i_0_465,i_0_304,i_0_248,i_0_332,i_0_305,i_0_325]) ).
cnf(i_0_881,plain,
f_ADD_(f_ADD_(f_ADD_(n0,f__index_(f__cons_(n0,X1),n0)),n0),n0) = f_SUB_(X2,X2),
inference(rename_variables,[],[i_0_864]) ).
cnf(i_0_886,plain,
f_ADD_(f_ADD_(n0,f__index_(f__cons_(n0,X1),n0)),n0) = f_SUB_(f_SUB_(X2,X2),n0),
inference(scs_inference,[],[i_0_865,i_0_304]) ).
cnf(i_0_887,plain,
f_ADD_(X1,n1) != f__index_(f__cons_(f_ADD_(n0,n0),X2),n0),
inference(scs_inference,[],[i_0_535,i_0_865,i_0_338,i_0_304,i_0_305]) ).
cnf(i_0_889,plain,
def_89(n1,f__index_(f__cons_(f_ADD_(n0,n0),X1),n0)),
inference(scs_inference,[],[i_0_535,i_0_865,i_0_338,i_0_304,i_0_305,i_0_336]) ).
cnf(i_0_891,plain,
f__index_(f__cons_(f_ADD_(n0,n0),X1),n0) != n1,
inference(scs_inference,[],[i_0_535,i_0_865,i_0_338,i_0_304,i_0_305,i_0_336,i_0_283]) ).
cnf(i_0_893,plain,
p_LES_EQU_(f__index_(f__cons_(f_ADD_(n0,n0),X1),n0),n1),
inference(scs_inference,[],[i_0_535,i_0_865,i_0_338,i_0_304,i_0_305,i_0_336,i_0_283,i_0_279]) ).
cnf(i_0_895,plain,
~ p_LES_EQU_(n1,f__index_(f__cons_(f_ADD_(n0,n0),X1),n0)),
inference(scs_inference,[],[i_0_535,i_0_865,i_0_338,i_0_304,i_0_305,i_0_336,i_0_283,i_0_279,i_0_258]) ).
cnf(i_0_899,plain,
~ p_LES_EQU_(f_ADD_(n0,f__index_(f__cons_(n1,X1),n0)),f__index_(f__cons_(f_ADD_(n0,n0),X2),n0)),
inference(scs_inference,[],[i_0_659,i_0_535,i_0_506,i_0_865,i_0_338,i_0_304,i_0_305,i_0_336,i_0_283,i_0_279,i_0_258,i_0_254,i_0_332]) ).
cnf(i_0_1726,plain,
p_LES_EQU_(f_ADD_(f_ADD_(n0,f__index_(f__cons_(n0,X1),n0)),n0),n1),
inference(rename_variables,[],[i_0_1580]) ).
cnf(i_0_844,plain,
f_ADD_(f_ADD_(n0,n0),n0) = f_SUB_(f_ADD_(n0,n0),n0),
inference(scs_inference,[],[i_0_819,i_0_304]) ).
cnf(i_0_845,plain,
f_ADD_(X1,n1) != f_ADD_(f_ADD_(f_ADD_(n0,n0),n0),n0),
inference(scs_inference,[],[i_0_380,i_0_803,i_0_819,i_0_304,i_0_305]) ).
cnf(i_0_847,plain,
def_89(n1,f_ADD_(f_ADD_(f_ADD_(n0,n0),n0),n0)),
inference(scs_inference,[],[i_0_380,i_0_803,i_0_819,i_0_304,i_0_305,i_0_336]) ).
cnf(i_0_849,plain,
f_ADD_(f_ADD_(f_ADD_(n0,n0),n0),n0) != n1,
inference(scs_inference,[],[i_0_380,i_0_803,i_0_819,i_0_304,i_0_305,i_0_336,i_0_283]) ).
cnf(i_0_851,plain,
p_LES_EQU_(f_ADD_(f_ADD_(f_ADD_(n0,n0),n0),n0),n1),
inference(scs_inference,[],[i_0_380,i_0_803,i_0_819,i_0_304,i_0_305,i_0_336,i_0_283,i_0_279]) ).
cnf(i_0_855,plain,
~ p_LES_EQU_(n1,f_ADD_(f_ADD_(f_ADD_(n0,n0),n0),n0)),
inference(scs_inference,[],[i_0_380,i_0_803,i_0_819,i_0_823,i_0_304,i_0_305,i_0_336,i_0_283,i_0_279,i_0_222,i_0_258]) ).
cnf(i_0_1054,plain,
f_ADD_(f_ADD_(f_ADD_(f_ADD_(n0,n0),n0),n0),X1) = X1,
inference(rename_variables,[],[i_0_794]) ).
cnf(i_0_1729,plain,
p_LES_EQU_(f__index_(f__cons_(f_ADD_(n0,n0),X1),n0),n1),
inference(rename_variables,[],[i_0_893]) ).
cnf(i_0_2973,plain,
f_ADD_(f_ADD_(f_ADD_(f_ADD_(n0,n0),n0),n0),X1) = X1,
inference(rename_variables,[],[i_0_794]) ).
cnf(i_0_867,plain,
~ p_LES_EQU_(f_ADD_(n0,f__index_(f__cons_(n1,X1),n0)),f_ADD_(f_ADD_(f_ADD_(n0,n0),n0),n0)),
inference(scs_inference,[],[i_0_855,i_0_506,i_0_806,i_0_432,i_0_304,i_0_248,i_0_332]) ).
cnf(i_0_869,plain,
f_ADD_(n0,n0) = f_ADD_(f_ADD_(f_ADD_(n0,f__index_(f__cons_(n0,X1),n0)),n0),n0),
inference(scs_inference,[],[i_0_855,i_0_449,i_0_506,i_0_806,i_0_432,i_0_304,i_0_248,i_0_332,i_0_305]) ).
cnf(i_0_877,plain,
f_ADD_(f_ADD_(f_ADD_(n0,f__index_(f__cons_(n0,X1),n0)),n0),n0) = f_ADD_(n0,n0),
inference(scs_inference,[],[i_0_869,i_0_304]) ).
cnf(i_0_878,plain,
f_SUB_(f_ADD_(n0,n0),n0) = f_ADD_(f_ADD_(n0,f__index_(f__cons_(n0,X1),n0)),n0),
inference(scs_inference,[],[i_0_869,i_0_465,i_0_304,i_0_248]) ).
cnf(i_0_880,plain,
f_ADD_(X1,n1) != f_ADD_(f_ADD_(f_ADD_(n0,f__index_(f__cons_(n0,X2),n0)),n0),n0),
inference(scs_inference,[],[i_0_380,i_0_864,i_0_869,i_0_465,i_0_304,i_0_248,i_0_305]) ).
cnf(i_0_904,plain,
f_ADD_(f_ADD_(n0,f__index_(f__cons_(n0,X1),n0)),n0) = f_SUB_(f_ADD_(n0,n0),n0),
inference(scs_inference,[],[i_0_878,i_0_304]) ).
cnf(i_0_905,plain,
f_ADD_(X1,n1) != f_ADD_(n0,f_ADD_(n0,n0)),
inference(scs_inference,[],[i_0_535,i_0_878,i_0_297,i_0_304,i_0_305]) ).
cnf(i_0_907,plain,
n1 != f_ADD_(n0,n0),
inference(scs_inference,[],[i_0_535,i_0_878,i_0_297,i_0_304,i_0_305,i_0_325]) ).
cnf(i_0_916,plain,
def_89(n1,f_ADD_(n0,f_ADD_(n0,n0))),
inference(scs_inference,[],[i_0_905,i_0_336]) ).
cnf(i_0_917,plain,
f_ADD_(X1,n1) != f_ADD_(n0,f_ADD_(n0,n0)),
inference(rename_variables,[],[i_0_905]) ).
cnf(i_0_919,plain,
f_ADD_(n0,f_ADD_(n0,n0)) != n1,
inference(scs_inference,[],[i_0_905,i_0_336,i_0_283]) ).
cnf(i_0_921,plain,
p_LES_EQU_(f_ADD_(n0,f_ADD_(n0,n0)),n1),
inference(scs_inference,[],[i_0_905,i_0_336,i_0_283,i_0_279]) ).
cnf(i_0_923,plain,
X1 = f_ADD_(f_ADD_(f_ADD_(f_ADD_(n0,n0),n0),n0),X1),
inference(scs_inference,[],[i_0_905,i_0_794,i_0_336,i_0_283,i_0_279,i_0_304]) ).
cnf(i_0_924,plain,
~ p_LES_EQU_(n1,f_ADD_(n0,f_ADD_(n0,n0))),
inference(scs_inference,[],[i_0_905,i_0_794,i_0_336,i_0_283,i_0_279,i_0_304,i_0_258]) ).
cnf(i_0_926,plain,
~ p_LES_EQU_(f_ADD_(n0,f__index_(f__cons_(n1,X1),n0)),f_ADD_(n0,f_ADD_(n0,n0))),
inference(scs_inference,[],[i_0_506,i_0_905,i_0_794,i_0_336,i_0_283,i_0_279,i_0_304,i_0_258,i_0_332]) ).
cnf(i_0_928,plain,
f_ADD_(X1,n1) != f_ADD_(f_ADD_(n0,n0),f_ADD_(n0,n0)),
inference(scs_inference,[],[i_0_535,i_0_506,i_0_905,i_0_441,i_0_794,i_0_336,i_0_283,i_0_279,i_0_304,i_0_258,i_0_332,i_0_305]) ).
cnf(i_0_936,plain,
def_89(n1,f_ADD_(f_ADD_(n0,n0),f_ADD_(n0,n0))),
inference(scs_inference,[],[i_0_928,i_0_336]) ).
cnf(i_0_937,plain,
f_ADD_(X1,n1) != f_ADD_(f_ADD_(n0,n0),f_ADD_(n0,n0)),
inference(rename_variables,[],[i_0_928]) ).
cnf(i_0_939,plain,
f_ADD_(f_ADD_(n0,n0),f_ADD_(n0,n0)) != n1,
inference(scs_inference,[],[i_0_928,i_0_336,i_0_283]) ).
cnf(i_0_941,plain,
p_LES_EQU_(f_ADD_(f_ADD_(n0,n0),f_ADD_(n0,n0)),n1),
inference(scs_inference,[],[i_0_928,i_0_336,i_0_283,i_0_279]) ).
cnf(i_0_943,plain,
f__nor_(f__index_(X1,X2),f__index_(X3,X2)) = f__index_(f__nor_(X1,X3),X2),
inference(scs_inference,[],[i_0_928,i_0_203,i_0_336,i_0_283,i_0_279,i_0_304]) ).
cnf(i_0_944,plain,
~ p_LES_EQU_(n1,f_ADD_(f_ADD_(n0,n0),f_ADD_(n0,n0))),
inference(scs_inference,[],[i_0_928,i_0_203,i_0_336,i_0_283,i_0_279,i_0_304,i_0_258]) ).
cnf(i_0_946,plain,
~ p_LES_EQU_(f_ADD_(n0,f__index_(f__cons_(n1,X1),n0)),f_ADD_(f_ADD_(n0,n0),f_ADD_(n0,n0))),
inference(scs_inference,[],[i_0_506,i_0_928,i_0_203,i_0_336,i_0_283,i_0_279,i_0_304,i_0_258,i_0_332]) ).
cnf(i_0_948,plain,
f_SUB_(X1,X1) = f_ADD_(f_ADD_(f_ADD_(f_ADD_(n0,n0),n0),n0),n0),
inference(scs_inference,[],[i_0_352,i_0_506,i_0_923,i_0_928,i_0_203,i_0_336,i_0_283,i_0_279,i_0_304,i_0_258,i_0_332,i_0_305]) ).
cnf(i_0_949,plain,
X1 = f_ADD_(f_ADD_(f_ADD_(f_ADD_(n0,n0),n0),n0),X1),
inference(rename_variables,[],[i_0_923]) ).
cnf(i_0_950,plain,
f_ADD_(f_ADD_(f_ADD_(f_ADD_(f_ADD_(n0,n0),n0),n0),n0),X1) = X1,
inference(scs_inference,[],[i_0_341,i_0_352,i_0_506,i_0_923,i_0_928,i_0_203,i_0_336,i_0_283,i_0_279,i_0_304,i_0_258,i_0_332,i_0_305,i_0_247]) ).
cnf(i_0_1280,plain,
X1 = f_ADD_(f_ADD_(f_ADD_(f_ADD_(n0,n0),n0),n0),X1),
inference(rename_variables,[],[i_0_923]) ).
cnf(i_0_2468,plain,
X1 = f_ADD_(f_ADD_(f_ADD_(f_ADD_(n0,n0),n0),n0),X1),
inference(rename_variables,[],[i_0_923]) ).
cnf(i_0_3939,plain,
X1 = f_ADD_(f_ADD_(f_ADD_(f_ADD_(n0,n0),n0),n0),X1),
inference(rename_variables,[],[i_0_923]) ).
cnf(i_0_3944,plain,
X1 = f_ADD_(f_ADD_(f_ADD_(f_ADD_(n0,n0),n0),n0),X1),
inference(rename_variables,[],[i_0_923]) ).
cnf(i_0_958,plain,
f_ADD_(f_ADD_(f_ADD_(f_ADD_(n0,n0),n0),n0),n0) = f_SUB_(X1,X1),
inference(scs_inference,[],[i_0_948,i_0_304]) ).
cnf(i_0_959,plain,
f_SUB_(f_SUB_(X1,X1),n0) = f_ADD_(f_ADD_(f_ADD_(n0,n0),n0),n0),
inference(scs_inference,[],[i_0_948,i_0_432,i_0_304,i_0_248]) ).
cnf(i_0_961,plain,
f_ADD_(n0,n0) = f_ADD_(f_ADD_(f_ADD_(f_ADD_(n0,n0),n0),n0),n0),
inference(scs_inference,[],[i_0_449,i_0_948,i_0_432,i_0_304,i_0_248,i_0_305]) ).
cnf(i_0_962,plain,
f_SUB_(X1,X1) = f_ADD_(f_ADD_(f_ADD_(f_ADD_(n0,n0),n0),n0),n0),
inference(rename_variables,[],[i_0_948]) ).
cnf(i_0_1142,plain,
f_ADD_(X1,n1) != f_ADD_(f_ADD_(f_ADD_(f_ADD_(f_ADD_(n0,n0),n0),n0),n0),f_ADD_(n0,n0)),
inference(scs_inference,[],[i_0_1130,i_0_535,i_0_506,i_0_950,i_0_207,i_0_304,i_0_332,i_0_305]) ).
cnf(i_0_1143,plain,
f_ADD_(f_ADD_(f_ADD_(f_ADD_(f_ADD_(n0,n0),n0),n0),n0),X1) = X1,
inference(rename_variables,[],[i_0_950]) ).
cnf(i_0_2820,plain,
f_ADD_(f_ADD_(f_ADD_(f_ADD_(f_ADD_(n0,n0),n0),n0),n0),X1) = X1,
inference(rename_variables,[],[i_0_950]) ).
cnf(i_0_965,plain,
f_ADD_(f_ADD_(f_ADD_(f_ADD_(n0,n0),n0),n0),n0) = f_ADD_(n0,n0),
inference(scs_inference,[],[i_0_961,i_0_304]) ).
cnf(i_0_966,plain,
f_SUB_(f_ADD_(n0,n0),n0) = f_ADD_(f_ADD_(f_ADD_(n0,n0),n0),n0),
inference(scs_inference,[],[i_0_961,i_0_465,i_0_304,i_0_248]) ).
cnf(i_0_968,plain,
f_ADD_(X1,n1) != f_ADD_(f_ADD_(f_ADD_(f_ADD_(n0,n0),n0),n0),n0),
inference(scs_inference,[],[i_0_380,i_0_958,i_0_961,i_0_465,i_0_304,i_0_248,i_0_305]) ).
cnf(i_0_969,plain,
f_ADD_(f_ADD_(f_ADD_(f_ADD_(n0,n0),n0),n0),n0) = f_SUB_(X1,X1),
inference(rename_variables,[],[i_0_958]) ).
cnf(i_0_977,plain,
f_ADD_(f_ADD_(f_ADD_(n0,n0),n0),n0) = f_SUB_(f_SUB_(X1,X1),n0),
inference(scs_inference,[],[i_0_959,i_0_304]) ).
cnf(i_0_978,plain,
f_ADD_(X1,n1) != f_ADD_(f_ADD_(n0,f__index_(f__cons_(n0,X2),n0)),f_ADD_(n0,n0)),
inference(scs_inference,[],[i_0_535,i_0_959,i_0_522,i_0_304,i_0_305]) ).
cnf(i_0_1162,plain,
~ p_LES_EQU_(n1,f__index_(f__others_(f_ADD_(n0,n0)),X1)),
inference(scs_inference,[],[i_0_535,i_0_1142,i_0_243,i_0_289,i_0_304,i_0_305,i_0_336,i_0_283,i_0_279,i_0_222,i_0_258]) ).
cnf(i_0_3333,plain,
f_ADD_(X1,n1) != f_ADD_(f_ADD_(f_ADD_(f_ADD_(f_ADD_(n0,n0),n0),n0),n0),f_ADD_(n0,n0)),
inference(rename_variables,[],[i_0_1142]) ).
cnf(i_0_988,plain,
def_89(n1,f_ADD_(f_ADD_(n0,f__index_(f__cons_(n0,X1),n0)),f_ADD_(n0,n0))),
inference(scs_inference,[],[i_0_978,i_0_336]) ).
cnf(i_0_989,plain,
f_ADD_(X1,n1) != f_ADD_(f_ADD_(n0,f__index_(f__cons_(n0,X2),n0)),f_ADD_(n0,n0)),
inference(rename_variables,[],[i_0_978]) ).
cnf(i_0_991,plain,
f_ADD_(f_ADD_(n0,f__index_(f__cons_(n0,X1),n0)),f_ADD_(n0,n0)) != n1,
inference(scs_inference,[],[i_0_978,i_0_336,i_0_283]) ).
cnf(i_0_993,plain,
p_LES_EQU_(f_ADD_(f_ADD_(n0,f__index_(f__cons_(n0,X1),n0)),f_ADD_(n0,n0)),n1),
inference(scs_inference,[],[i_0_978,i_0_336,i_0_283,i_0_279]) ).
cnf(i_0_995,plain,
f_ADD_(f_ADD_(f_ADD_(n0,n0),n0),n0) = f_SUB_(f_ADD_(n0,n0),n0),
inference(scs_inference,[],[i_0_966,i_0_978,i_0_336,i_0_283,i_0_279,i_0_304]) ).
cnf(i_0_996,plain,
~ p_LES_EQU_(n1,f_ADD_(f_ADD_(n0,f__index_(f__cons_(n0,X1),n0)),f_ADD_(n0,n0))),
inference(scs_inference,[],[i_0_966,i_0_978,i_0_336,i_0_283,i_0_279,i_0_304,i_0_258]) ).
cnf(i_0_1000,plain,
f_ADD_(X1,n1) != f_ADD_(f_ADD_(f_ADD_(n0,n0),n0),f_ADD_(n0,n0)),
inference(scs_inference,[],[i_0_535,i_0_506,i_0_966,i_0_978,i_0_668,i_0_336,i_0_283,i_0_279,i_0_304,i_0_258,i_0_332,i_0_305]) ).
cnf(i_0_1172,plain,
~ p_LES_EQU_(f_ADD_(n0,f__index_(f__cons_(n1,X1),n0)),f__index_(f__others_(f_ADD_(n0,n0)),X2)),
inference(scs_inference,[],[i_0_1162,i_0_506,i_0_255,i_0_304,i_0_332]) ).
cnf(i_0_1174,plain,
f_ADD_(X1,n1) != f__index_(f__slice_(f__others_(f_ADD_(n0,n0)),X2,X3),X4),
inference(scs_inference,[],[i_0_1162,i_0_506,i_0_1152,i_0_255,i_0_182,i_0_304,i_0_332,i_0_305]) ).
cnf(i_0_1177,plain,
def_89(n1,f__index_(f__slice_(f__others_(f_ADD_(n0,n0)),X1,X2),X3)),
inference(scs_inference,[],[i_0_1162,i_0_506,i_0_1152,i_0_255,i_0_182,i_0_304,i_0_332,i_0_305,i_0_336]) ).
cnf(i_0_1179,plain,
f__index_(f__slice_(f__others_(f_ADD_(n0,n0)),X1,X2),X3) != n1,
inference(scs_inference,[],[i_0_1162,i_0_506,i_0_1152,i_0_255,i_0_182,i_0_304,i_0_332,i_0_305,i_0_336,i_0_283]) ).
cnf(i_0_1181,plain,
p_LES_EQU_(f__index_(f__slice_(f__others_(f_ADD_(n0,n0)),X1,X2),X3),n1),
inference(scs_inference,[],[i_0_1162,i_0_506,i_0_1152,i_0_255,i_0_182,i_0_304,i_0_332,i_0_305,i_0_336,i_0_283,i_0_279]) ).
cnf(i_0_1185,plain,
~ p_LES_EQU_(n1,f__index_(f__slice_(f__others_(f_ADD_(n0,n0)),X1,X2),X3)),
inference(scs_inference,[],[i_0_1162,i_0_506,i_0_1152,i_0_1176,i_0_255,i_0_182,i_0_304,i_0_332,i_0_305,i_0_336,i_0_283,i_0_279,i_0_222,i_0_258]) ).
cnf(i_0_3046,plain,
f_ADD_(X1,n1) != f_ADD_(f_ADD_(f_ADD_(f_ADD_(n0,n0),n0),n0),n0),
inference(rename_variables,[],[i_0_968]) ).
cnf(i_0_1008,plain,
def_89(n1,f_ADD_(f_ADD_(f_ADD_(n0,n0),n0),f_ADD_(n0,n0))),
inference(scs_inference,[],[i_0_1000,i_0_336]) ).
cnf(i_0_1009,plain,
f_ADD_(X1,n1) != f_ADD_(f_ADD_(f_ADD_(n0,n0),n0),f_ADD_(n0,n0)),
inference(rename_variables,[],[i_0_1000]) ).
cnf(i_0_1011,plain,
f_ADD_(f_ADD_(f_ADD_(n0,n0),n0),f_ADD_(n0,n0)) != n1,
inference(scs_inference,[],[i_0_1000,i_0_336,i_0_283]) ).
cnf(i_0_1013,plain,
p_LES_EQU_(f_ADD_(f_ADD_(f_ADD_(n0,n0),n0),f_ADD_(n0,n0)),n1),
inference(scs_inference,[],[i_0_1000,i_0_336,i_0_283,i_0_279]) ).
cnf(i_0_1015,plain,
X1 = f_ADD_(f_ADD_(f_ADD_(f_ADD_(f_ADD_(n0,n0),n0),n0),n0),X1),
inference(scs_inference,[],[i_0_1000,i_0_950,i_0_336,i_0_283,i_0_279,i_0_304]) ).
cnf(i_0_1016,plain,
~ p_LES_EQU_(n1,f_ADD_(f_ADD_(f_ADD_(n0,n0),n0),f_ADD_(n0,n0))),
inference(scs_inference,[],[i_0_1000,i_0_950,i_0_336,i_0_283,i_0_279,i_0_304,i_0_258]) ).
cnf(i_0_1018,plain,
~ p_LES_EQU_(f_ADD_(n0,f__index_(f__cons_(n1,X1),n0)),f_ADD_(f_ADD_(f_ADD_(n0,n0),n0),f_ADD_(n0,n0))),
inference(scs_inference,[],[i_0_506,i_0_1000,i_0_950,i_0_336,i_0_283,i_0_279,i_0_304,i_0_258,i_0_332]) ).
cnf(i_0_1020,plain,
f_ADD_(X1,n1) != f_ADD_(f_ADD_(f_ADD_(n0,f__index_(f__cons_(n0,X2),n0)),n0),f_ADD_(n0,n0)),
inference(scs_inference,[],[i_0_535,i_0_506,i_0_1000,i_0_683,i_0_950,i_0_336,i_0_283,i_0_279,i_0_304,i_0_258,i_0_332,i_0_305]) ).
cnf(i_0_1197,plain,
f_ADD_(X1,n1) != f__length_(f__slice_(X2,X3,f_ADD_(X3,n1))),
inference(scs_inference,[],[i_0_1185,i_0_341,i_0_380,i_0_506,i_0_184,i_0_304,i_0_247,i_0_332,i_0_305]) ).
cnf(i_0_1200,plain,
def_89(n1,f__length_(f__slice_(X1,X2,f_ADD_(X2,n1)))),
inference(scs_inference,[],[i_0_1185,i_0_341,i_0_380,i_0_506,i_0_184,i_0_304,i_0_247,i_0_332,i_0_305,i_0_336]) ).
cnf(i_0_1202,plain,
f__length_(f__slice_(X1,X2,f_ADD_(X2,n1))) != n1,
inference(scs_inference,[],[i_0_1185,i_0_341,i_0_380,i_0_506,i_0_184,i_0_304,i_0_247,i_0_332,i_0_305,i_0_336,i_0_283]) ).
cnf(i_0_1204,plain,
p_LES_EQU_(f__length_(f__slice_(X1,X2,f_ADD_(X2,n1))),n1),
inference(scs_inference,[],[i_0_1185,i_0_341,i_0_380,i_0_506,i_0_184,i_0_304,i_0_247,i_0_332,i_0_305,i_0_336,i_0_283,i_0_279]) ).
cnf(i_0_1208,plain,
~ p_LES_EQU_(n1,f__length_(f__slice_(X1,X2,f_ADD_(X2,n1)))),
inference(scs_inference,[],[i_0_1185,i_0_341,i_0_380,i_0_506,i_0_1174,i_0_184,i_0_304,i_0_247,i_0_332,i_0_305,i_0_336,i_0_283,i_0_279,i_0_222,i_0_258]) ).
cnf(i_0_3184,plain,
p_LES_EQU_(f__index_(f__slice_(f__others_(f_ADD_(n0,n0)),X1,X2),X3),n1),
inference(rename_variables,[],[i_0_1181]) ).
cnf(i_0_1029,plain,
f_SUB_(X1,X1) = f_ADD_(f_ADD_(f_ADD_(f_ADD_(f_ADD_(n0,n0),n0),n0),n0),n0),
inference(scs_inference,[],[i_0_352,i_0_1015,i_0_204,i_0_304,i_0_305]) ).
cnf(i_0_1030,plain,
X1 = f_ADD_(f_ADD_(f_ADD_(f_ADD_(f_ADD_(n0,n0),n0),n0),n0),X1),
inference(rename_variables,[],[i_0_1015]) ).
cnf(i_0_1215,plain,
~ p_LES_EQU_(f_ADD_(n0,f__index_(f__cons_(n1,X1),n0)),f__length_(f__slice_(X2,X3,f_ADD_(X3,n1)))),
inference(scs_inference,[],[i_0_1208,i_0_506,i_0_1192,i_0_304,i_0_332]) ).
cnf(i_0_1217,plain,
f_ADD_(X1,n1) != f__length_(f__empty_),
inference(scs_inference,[],[i_0_1208,i_0_290,i_0_506,i_0_1192,i_0_301,i_0_304,i_0_332,i_0_305]) ).
cnf(i_0_1218,plain,
def_89(n1,f__length_(f__empty_)),
inference(scs_inference,[],[i_0_1208,i_0_290,i_0_506,i_0_1192,i_0_301,i_0_304,i_0_332,i_0_305,i_0_336]) ).
cnf(i_0_1220,plain,
f__length_(f__empty_) != n1,
inference(scs_inference,[],[i_0_1208,i_0_290,i_0_506,i_0_1192,i_0_301,i_0_304,i_0_332,i_0_305,i_0_336,i_0_283]) ).
cnf(i_0_1222,plain,
p_LES_EQU_(f__length_(f__empty_),n1),
inference(scs_inference,[],[i_0_1208,i_0_290,i_0_506,i_0_1192,i_0_301,i_0_304,i_0_332,i_0_305,i_0_336,i_0_283,i_0_279]) ).
cnf(i_0_1226,plain,
~ p_LES_EQU_(n1,f__length_(f__empty_)),
inference(scs_inference,[],[i_0_1208,i_0_290,i_0_506,i_0_1197,i_0_1192,i_0_301,i_0_304,i_0_332,i_0_305,i_0_336,i_0_283,i_0_279,i_0_222,i_0_258]) ).
cnf(i_0_1287,plain,
X1 = f_ADD_(f_ADD_(f_ADD_(f_ADD_(f_ADD_(n0,n0),n0),n0),n0),X1),
inference(rename_variables,[],[i_0_1015]) ).
cnf(i_0_2321,plain,
X1 = f_ADD_(f_ADD_(f_ADD_(f_ADD_(f_ADD_(n0,n0),n0),n0),n0),X1),
inference(rename_variables,[],[i_0_1015]) ).
cnf(i_0_2757,plain,
f_ADD_(X1,n1) != f_ADD_(f_ADD_(f_ADD_(n0,f__index_(f__cons_(n0,X2),n0)),n0),f_ADD_(n0,n0)),
inference(rename_variables,[],[i_0_1020]) ).
cnf(i_0_2897,plain,
p_LES_EQU_(f__length_(f__slice_(X1,X2,f_ADD_(X2,n1))),n1),
inference(rename_variables,[],[i_0_1204]) ).
cnf(i_0_3639,plain,
X1 = f_ADD_(f_ADD_(f_ADD_(f_ADD_(f_ADD_(n0,n0),n0),n0),n0),X1),
inference(rename_variables,[],[i_0_1015]) ).
cnf(i_0_1036,plain,
f_ADD_(f_ADD_(f_ADD_(f_ADD_(f_ADD_(n0,n0),n0),n0),n0),n0) = f_SUB_(X1,X1),
inference(scs_inference,[],[i_0_1029,i_0_304]) ).
cnf(i_0_1037,plain,
f_SUB_(f_SUB_(X1,X1),n0) = f_ADD_(f_ADD_(f_ADD_(f_ADD_(n0,n0),n0),n0),n0),
inference(scs_inference,[],[i_0_1029,i_0_432,i_0_304,i_0_248]) ).
cnf(i_0_1039,plain,
f_ADD_(n0,n0) = f_ADD_(f_ADD_(f_ADD_(f_ADD_(f_ADD_(n0,n0),n0),n0),n0),n0),
inference(scs_inference,[],[i_0_449,i_0_1029,i_0_432,i_0_304,i_0_248,i_0_305]) ).
cnf(i_0_1040,plain,
f_SUB_(X1,X1) = f_ADD_(f_ADD_(f_ADD_(f_ADD_(f_ADD_(n0,n0),n0),n0),n0),n0),
inference(rename_variables,[],[i_0_1029]) ).
cnf(i_0_1236,plain,
~ p_LES_EQU_(n1,f_ADD_(n0,f__index_(f__cons_(f__length_(f__empty_),X1),n0))),
inference(scs_inference,[],[i_0_1226,i_0_506,i_0_269,i_0_304,i_0_333]) ).
cnf(i_0_1238,plain,
~ p_LES_EQU_(f_ADD_(n0,f__index_(f__cons_(n1,X1),n0)),f__length_(f__empty_)),
inference(scs_inference,[],[i_0_1226,i_0_506,i_0_1237,i_0_269,i_0_304,i_0_333,i_0_332]) ).
cnf(i_0_1240,plain,
n1 = f_ADD_(f__length_(f__slice_(X1,n0,f_ADD_(n0,n1))),f_ADD_(n0,n1)),
inference(scs_inference,[],[i_0_1226,i_0_405,i_0_506,i_0_1237,i_0_1214,i_0_269,i_0_304,i_0_333,i_0_332,i_0_305]) ).
cnf(i_0_1582,plain,
f_ADD_(f_ADD_(f_ADD_(f_ADD_(f_ADD_(f_ADD_(n0,n0),n0),n0),n0),n0),X1) = X1,
inference(scs_inference,[],[i_0_722,i_0_341,i_0_1029,i_0_336,i_0_283,i_0_279,i_0_247]) ).
cnf(i_0_1583,plain,
f_SUB_(X1,X1) = f_ADD_(f_ADD_(f_ADD_(f_ADD_(f_ADD_(n0,n0),n0),n0),n0),n0),
inference(rename_variables,[],[i_0_1029]) ).
cnf(i_0_1585,plain,
~ def_89(X1,f__index_(f__cons_(f__index_(f__cons_(f__index_(f__cons_(X1,X2),n0),X3),n0),X4),n0)),
inference(scs_inference,[],[i_0_722,i_0_342,i_0_341,i_0_1029,i_0_382,i_0_336,i_0_283,i_0_279,i_0_247,i_0_334]) ).
cnf(i_0_1587,plain,
~ def_89(f__index_(f__cons_(f__index_(f__cons_(f__index_(f__cons_(X1,X2),n0),X3),n0),X4),n0),X1),
inference(scs_inference,[],[i_0_722,i_0_342,i_0_341,i_0_1029,i_0_384,i_0_382,i_0_336,i_0_283,i_0_279,i_0_247,i_0_334,i_0_335]) ).
cnf(i_0_1589,plain,
~ p_LES_EQU_(n1,f_ADD_(f_ADD_(n0,f__index_(f__cons_(n0,X1),n0)),n0)),
inference(scs_inference,[],[i_0_722,i_0_342,i_0_341,i_0_1029,i_0_384,i_0_382,i_0_336,i_0_283,i_0_279,i_0_247,i_0_334,i_0_335,i_0_258]) ).
cnf(i_0_1597,plain,
X1 = f_ADD_(f_ADD_(f_ADD_(f_ADD_(f_ADD_(f_ADD_(n0,n0),n0),n0),n0),n0),X1),
inference(scs_inference,[],[i_0_350,i_0_641,i_0_722,i_0_342,i_0_341,i_0_1151,i_0_506,i_0_1592,i_0_1594,i_0_1029,i_0_384,i_0_382,i_0_336,i_0_283,i_0_279,i_0_247,i_0_334,i_0_335,i_0_258,i_0_333,i_0_332,i_0_305,i_0_304]) ).
cnf(i_0_1043,plain,
f_ADD_(f_ADD_(f_ADD_(f_ADD_(f_ADD_(n0,n0),n0),n0),n0),n0) = f_ADD_(n0,n0),
inference(scs_inference,[],[i_0_1039,i_0_304]) ).
cnf(i_0_1044,plain,
f_SUB_(f_ADD_(n0,n0),n0) = f_ADD_(f_ADD_(f_ADD_(f_ADD_(n0,n0),n0),n0),n0),
inference(scs_inference,[],[i_0_1039,i_0_465,i_0_304,i_0_248]) ).
cnf(i_0_1046,plain,
f_ADD_(X1,n1) != f_ADD_(f_ADD_(f_ADD_(f_ADD_(f_ADD_(n0,n0),n0),n0),n0),n0),
inference(scs_inference,[],[i_0_380,i_0_1036,i_0_1039,i_0_465,i_0_304,i_0_248,i_0_305]) ).
cnf(i_0_1047,plain,
f_ADD_(f_ADD_(f_ADD_(f_ADD_(f_ADD_(n0,n0),n0),n0),n0),n0) = f_SUB_(X1,X1),
inference(rename_variables,[],[i_0_1036]) ).
cnf(i_0_1052,plain,
f_ADD_(f_ADD_(f_ADD_(f_ADD_(n0,n0),n0),n0),n0) = f_SUB_(f_SUB_(X1,X1),n0),
inference(scs_inference,[],[i_0_1037,i_0_304]) ).
cnf(i_0_1053,plain,
f_ADD_(X1,n1) != f_ADD_(f_ADD_(f_ADD_(f_ADD_(n0,n0),n0),n0),f_ADD_(n0,n0)),
inference(scs_inference,[],[i_0_535,i_0_1037,i_0_794,i_0_304,i_0_305]) ).
cnf(i_0_1249,plain,
f_ADD_(f__length_(f__slice_(X1,n0,f_ADD_(n0,n1))),f_ADD_(n0,n1)) = n1,
inference(scs_inference,[],[i_0_1240,i_0_304]) ).
cnf(i_0_1626,plain,
~ p__pred_(f__not_(f__true_)),
inference(scs_inference,[],[i_0_1595,i_0_300,i_0_306,i_0_307,i_0_308,i_0_309,i_0_310,i_0_311,i_0_312,i_0_313,i_0_314,i_0_315,i_0_316,i_0_317,i_0_318,i_0_319,i_0_320,i_0_321,i_0_322,i_0_323,i_0_324,i_0_326,i_0_327,i_0_328,i_0_329,i_0_330,i_0_284]) ).
cnf(i_0_1628,plain,
p__pred_(f__not_(f__false_)),
inference(scs_inference,[],[i_0_1595,i_0_300,i_0_299,i_0_306,i_0_307,i_0_308,i_0_309,i_0_310,i_0_311,i_0_312,i_0_313,i_0_314,i_0_315,i_0_316,i_0_317,i_0_318,i_0_319,i_0_320,i_0_321,i_0_322,i_0_323,i_0_324,i_0_326,i_0_327,i_0_328,i_0_329,i_0_330,i_0_284,i_0_295]) ).
cnf(i_0_1630,plain,
~ p__pred_(f__nor_(f__true_,X1)),
inference(scs_inference,[],[i_0_1595,i_0_300,i_0_299,i_0_306,i_0_307,i_0_308,i_0_309,i_0_310,i_0_311,i_0_312,i_0_313,i_0_314,i_0_315,i_0_316,i_0_317,i_0_318,i_0_319,i_0_320,i_0_321,i_0_322,i_0_323,i_0_324,i_0_326,i_0_327,i_0_328,i_0_329,i_0_330,i_0_284,i_0_295,i_0_245]) ).
cnf(i_0_1632,plain,
~ p__pred_(f__nor_(X1,f__true_)),
inference(scs_inference,[],[i_0_1595,i_0_300,i_0_299,i_0_306,i_0_307,i_0_308,i_0_309,i_0_310,i_0_311,i_0_312,i_0_313,i_0_314,i_0_315,i_0_316,i_0_317,i_0_318,i_0_319,i_0_320,i_0_321,i_0_322,i_0_323,i_0_324,i_0_326,i_0_327,i_0_328,i_0_329,i_0_330,i_0_284,i_0_295,i_0_245,i_0_246]) ).
cnf(i_0_1634,plain,
~ p__pred_(f__and_(f__false_,X1)),
inference(scs_inference,[],[i_0_1595,i_0_300,i_0_299,i_0_306,i_0_307,i_0_308,i_0_309,i_0_310,i_0_311,i_0_312,i_0_313,i_0_314,i_0_315,i_0_316,i_0_317,i_0_318,i_0_319,i_0_320,i_0_321,i_0_322,i_0_323,i_0_324,i_0_326,i_0_327,i_0_328,i_0_329,i_0_330,i_0_284,i_0_295,i_0_245,i_0_246,i_0_252]) ).
cnf(i_0_1636,plain,
~ p__pred_(f__and_(X1,f__false_)),
inference(scs_inference,[],[i_0_1595,i_0_300,i_0_299,i_0_306,i_0_307,i_0_308,i_0_309,i_0_310,i_0_311,i_0_312,i_0_313,i_0_314,i_0_315,i_0_316,i_0_317,i_0_318,i_0_319,i_0_320,i_0_321,i_0_322,i_0_323,i_0_324,i_0_326,i_0_327,i_0_328,i_0_329,i_0_330,i_0_284,i_0_295,i_0_245,i_0_246,i_0_252,i_0_253]) ).
cnf(i_0_1638,plain,
p__pred_(f__or_(f__true_,X1)),
inference(scs_inference,[],[i_0_1595,i_0_300,i_0_299,i_0_306,i_0_307,i_0_308,i_0_309,i_0_310,i_0_311,i_0_312,i_0_313,i_0_314,i_0_315,i_0_316,i_0_317,i_0_318,i_0_319,i_0_320,i_0_321,i_0_322,i_0_323,i_0_324,i_0_326,i_0_327,i_0_328,i_0_329,i_0_330,i_0_284,i_0_295,i_0_245,i_0_246,i_0_252,i_0_253,i_0_277]) ).
cnf(i_0_1640,plain,
p__pred_(f__or_(X1,f__true_)),
inference(scs_inference,[],[i_0_1595,i_0_300,i_0_299,i_0_306,i_0_307,i_0_308,i_0_309,i_0_310,i_0_311,i_0_312,i_0_313,i_0_314,i_0_315,i_0_316,i_0_317,i_0_318,i_0_319,i_0_320,i_0_321,i_0_322,i_0_323,i_0_324,i_0_326,i_0_327,i_0_328,i_0_329,i_0_330,i_0_284,i_0_295,i_0_245,i_0_246,i_0_252,i_0_253,i_0_277,i_0_278]) ).
cnf(i_0_1642,plain,
p__pred_(f__nand_(f__false_,X1)),
inference(scs_inference,[],[i_0_1595,i_0_300,i_0_299,i_0_306,i_0_307,i_0_308,i_0_309,i_0_310,i_0_311,i_0_312,i_0_313,i_0_314,i_0_315,i_0_316,i_0_317,i_0_318,i_0_319,i_0_320,i_0_321,i_0_322,i_0_323,i_0_324,i_0_326,i_0_327,i_0_328,i_0_329,i_0_330,i_0_284,i_0_295,i_0_245,i_0_246,i_0_252,i_0_253,i_0_277,i_0_278,i_0_280]) ).
cnf(i_0_1644,plain,
p__pred_(f__nand_(X1,f__false_)),
inference(scs_inference,[],[i_0_1595,i_0_300,i_0_299,i_0_306,i_0_307,i_0_308,i_0_309,i_0_310,i_0_311,i_0_312,i_0_313,i_0_314,i_0_315,i_0_316,i_0_317,i_0_318,i_0_319,i_0_320,i_0_321,i_0_322,i_0_323,i_0_324,i_0_326,i_0_327,i_0_328,i_0_329,i_0_330,i_0_284,i_0_295,i_0_245,i_0_246,i_0_252,i_0_253,i_0_277,i_0_278,i_0_280,i_0_281]) ).
cnf(i_0_1646,plain,
~ p__pred_(f__gt_(f_ADD_(f_ADD_(n0,f__index_(f__cons_(n0,X1),n0)),n0),n1)),
inference(scs_inference,[],[i_0_1580,i_0_1595,i_0_300,i_0_299,i_0_306,i_0_307,i_0_308,i_0_309,i_0_310,i_0_311,i_0_312,i_0_313,i_0_314,i_0_315,i_0_316,i_0_317,i_0_318,i_0_319,i_0_320,i_0_321,i_0_322,i_0_323,i_0_324,i_0_326,i_0_327,i_0_328,i_0_329,i_0_330,i_0_284,i_0_295,i_0_245,i_0_246,i_0_252,i_0_253,i_0_277,i_0_278,i_0_280,i_0_281,i_0_226]) ).
cnf(i_0_1648,plain,
~ p__pred_(f__lt_(n1,f_ADD_(f_ADD_(n0,f__index_(f__cons_(n0,X1),n0)),n0))),
inference(scs_inference,[],[i_0_1580,i_0_1595,i_0_300,i_0_299,i_0_306,i_0_307,i_0_308,i_0_309,i_0_310,i_0_311,i_0_312,i_0_313,i_0_314,i_0_315,i_0_316,i_0_317,i_0_318,i_0_319,i_0_320,i_0_321,i_0_322,i_0_323,i_0_324,i_0_326,i_0_327,i_0_328,i_0_329,i_0_330,i_0_284,i_0_295,i_0_245,i_0_246,i_0_252,i_0_253,i_0_277,i_0_278,i_0_280,i_0_281,i_0_226,i_0_227]) ).
cnf(i_0_1654,plain,
p__pred_(f__geq_(n1,f_ADD_(f_ADD_(n0,f__index_(f__cons_(n0,X1),n0)),n0))),
inference(scs_inference,[],[i_0_220,i_0_1580,i_0_1595,i_0_300,i_0_299,i_0_306,i_0_307,i_0_308,i_0_309,i_0_310,i_0_311,i_0_312,i_0_313,i_0_314,i_0_315,i_0_316,i_0_317,i_0_318,i_0_319,i_0_320,i_0_321,i_0_322,i_0_323,i_0_324,i_0_326,i_0_327,i_0_328,i_0_329,i_0_330,i_0_284,i_0_295,i_0_245,i_0_246,i_0_252,i_0_253,i_0_277,i_0_278,i_0_280,i_0_281,i_0_226,i_0_227,i_0_233,i_0_234,i_0_249]) ).
cnf(i_0_1656,plain,
p__pred_(f__leq_(f_ADD_(f_ADD_(n0,f__index_(f__cons_(n0,X1),n0)),n0),n1)),
inference(scs_inference,[],[i_0_220,i_0_1580,i_0_1595,i_0_300,i_0_299,i_0_306,i_0_307,i_0_308,i_0_309,i_0_310,i_0_311,i_0_312,i_0_313,i_0_314,i_0_315,i_0_316,i_0_317,i_0_318,i_0_319,i_0_320,i_0_321,i_0_322,i_0_323,i_0_324,i_0_326,i_0_327,i_0_328,i_0_329,i_0_330,i_0_284,i_0_295,i_0_245,i_0_246,i_0_252,i_0_253,i_0_277,i_0_278,i_0_280,i_0_281,i_0_226,i_0_227,i_0_233,i_0_234,i_0_249,i_0_250]) ).
cnf(i_0_1658,plain,
~ p__pred_(f__equal_(f__true_,f__false_)),
inference(scs_inference,[],[i_0_220,i_0_381,i_0_1580,i_0_1595,i_0_300,i_0_299,i_0_306,i_0_307,i_0_308,i_0_309,i_0_310,i_0_311,i_0_312,i_0_313,i_0_314,i_0_315,i_0_316,i_0_317,i_0_318,i_0_319,i_0_320,i_0_321,i_0_322,i_0_323,i_0_324,i_0_326,i_0_327,i_0_328,i_0_329,i_0_330,i_0_284,i_0_295,i_0_245,i_0_246,i_0_252,i_0_253,i_0_277,i_0_278,i_0_280,i_0_281,i_0_226,i_0_227,i_0_233,i_0_234,i_0_249,i_0_250,i_0_256]) ).
cnf(i_0_1666,plain,
f__index_(f__cons_(X1,X2),f__length_(f__empty_)) = X1,
inference(scs_inference,[],[i_0_220,i_0_381,i_0_1580,i_0_1595,i_0_300,i_0_299,i_0_301,i_0_306,i_0_307,i_0_308,i_0_309,i_0_310,i_0_311,i_0_312,i_0_313,i_0_314,i_0_315,i_0_316,i_0_317,i_0_318,i_0_319,i_0_320,i_0_321,i_0_322,i_0_323,i_0_324,i_0_326,i_0_327,i_0_328,i_0_329,i_0_330,i_0_284,i_0_295,i_0_245,i_0_246,i_0_252,i_0_253,i_0_277,i_0_278,i_0_280,i_0_281,i_0_226,i_0_227,i_0_233,i_0_234,i_0_249,i_0_250,i_0_256,i_0_259,i_0_260,i_0_282,i_0_267]) ).
cnf(i_0_1668,plain,
n1 = f_ADD_(y_105(n1),n1),
inference(scs_inference,[],[i_0_220,i_0_381,i_0_541,i_0_1580,i_0_1595,i_0_300,i_0_299,i_0_301,i_0_306,i_0_307,i_0_308,i_0_309,i_0_310,i_0_311,i_0_312,i_0_313,i_0_314,i_0_315,i_0_316,i_0_317,i_0_318,i_0_319,i_0_320,i_0_321,i_0_322,i_0_323,i_0_324,i_0_326,i_0_327,i_0_328,i_0_329,i_0_330,i_0_284,i_0_295,i_0_245,i_0_246,i_0_252,i_0_253,i_0_277,i_0_278,i_0_280,i_0_281,i_0_226,i_0_227,i_0_233,i_0_234,i_0_249,i_0_250,i_0_256,i_0_259,i_0_260,i_0_282,i_0_267,i_0_288]) ).
cnf(i_0_1670,plain,
p_LES_EQU_(f_ADD_(f_ADD_(f_ADD_(n0,f__index_(f__cons_(n0,X1),n0)),n0),n1),f_ADD_(n1,n1)),
inference(scs_inference,[],[i_0_220,i_0_381,i_0_541,i_0_1580,i_0_1595,i_0_300,i_0_299,i_0_301,i_0_306,i_0_307,i_0_308,i_0_309,i_0_310,i_0_311,i_0_312,i_0_313,i_0_314,i_0_315,i_0_316,i_0_317,i_0_318,i_0_319,i_0_320,i_0_321,i_0_322,i_0_323,i_0_324,i_0_326,i_0_327,i_0_328,i_0_329,i_0_330,i_0_284,i_0_295,i_0_245,i_0_246,i_0_252,i_0_253,i_0_277,i_0_278,i_0_280,i_0_281,i_0_226,i_0_227,i_0_233,i_0_234,i_0_249,i_0_250,i_0_256,i_0_259,i_0_260,i_0_282,i_0_267,i_0_288,i_0_223]) ).
cnf(i_0_1672,plain,
f_ADD_(f__true_,n1) != f_ADD_(f__false_,n1),
inference(scs_inference,[],[i_0_220,i_0_381,i_0_541,i_0_1580,i_0_1595,i_0_300,i_0_299,i_0_301,i_0_306,i_0_307,i_0_308,i_0_309,i_0_310,i_0_311,i_0_312,i_0_313,i_0_314,i_0_315,i_0_316,i_0_317,i_0_318,i_0_319,i_0_320,i_0_321,i_0_322,i_0_323,i_0_324,i_0_326,i_0_327,i_0_328,i_0_329,i_0_330,i_0_284,i_0_295,i_0_245,i_0_246,i_0_252,i_0_253,i_0_277,i_0_278,i_0_280,i_0_281,i_0_226,i_0_227,i_0_233,i_0_234,i_0_249,i_0_250,i_0_256,i_0_259,i_0_260,i_0_282,i_0_267,i_0_288,i_0_223,i_0_273]) ).
cnf(i_0_1674,plain,
f_SUB_(f_ADD_(n0,n0),n0) = n0,
inference(scs_inference,[],[i_0_220,i_0_381,i_0_541,i_0_1580,i_0_1595,i_0_300,i_0_299,i_0_301,i_0_465,i_0_306,i_0_307,i_0_308,i_0_309,i_0_310,i_0_311,i_0_312,i_0_313,i_0_314,i_0_315,i_0_316,i_0_317,i_0_318,i_0_319,i_0_320,i_0_321,i_0_322,i_0_323,i_0_324,i_0_326,i_0_327,i_0_328,i_0_329,i_0_330,i_0_284,i_0_295,i_0_245,i_0_246,i_0_252,i_0_253,i_0_277,i_0_278,i_0_280,i_0_281,i_0_226,i_0_227,i_0_233,i_0_234,i_0_249,i_0_250,i_0_256,i_0_259,i_0_260,i_0_282,i_0_267,i_0_288,i_0_223,i_0_273,i_0_337]) ).
cnf(i_0_1732,plain,
f_ADD_(f_ADD_(f_ADD_(f_ADD_(f_ADD_(f_ADD_(n0,n0),n0),n0),n0),n0),X1) = X1,
inference(rename_variables,[],[i_0_1582]) ).
cnf(i_0_1747,plain,
X1 = f_ADD_(f_ADD_(f_ADD_(f_ADD_(f_ADD_(f_ADD_(n0,n0),n0),n0),n0),n0),X1),
inference(rename_variables,[],[i_0_1597]) ).
cnf(i_0_1749,plain,
X1 = f_ADD_(f_ADD_(f_ADD_(f_ADD_(f_ADD_(f_ADD_(n0,n0),n0),n0),n0),n0),X1),
inference(rename_variables,[],[i_0_1597]) ).
cnf(i_0_1894,plain,
X1 = f_ADD_(f_ADD_(f_ADD_(f_ADD_(f_ADD_(f_ADD_(n0,n0),n0),n0),n0),n0),X1),
inference(rename_variables,[],[i_0_1597]) ).
cnf(i_0_2034,plain,
~ def_89(f__index_(f__cons_(f__index_(f__cons_(f__index_(f__cons_(X1,X2),n0),X3),n0),X4),n0),X1),
inference(rename_variables,[],[i_0_1587]) ).
cnf(i_0_2044,plain,
X1 = f_ADD_(f_ADD_(f_ADD_(f_ADD_(f_ADD_(f_ADD_(n0,n0),n0),n0),n0),n0),X1),
inference(rename_variables,[],[i_0_1597]) ).
cnf(i_0_2326,plain,
~ def_89(X1,f__index_(f__cons_(f__index_(f__cons_(f__index_(f__cons_(X1,X2),n0),X3),n0),X4),n0)),
inference(rename_variables,[],[i_0_1585]) ).
cnf(i_0_2620,plain,
~ def_89(f__index_(f__cons_(f__index_(f__cons_(f__index_(f__cons_(X1,X2),n0),X3),n0),X4),n0),X1),
inference(rename_variables,[],[i_0_1587]) ).
cnf(i_0_2905,plain,
~ def_89(X1,f__index_(f__cons_(f__index_(f__cons_(f__index_(f__cons_(X1,X2),n0),X3),n0),X4),n0)),
inference(rename_variables,[],[i_0_1585]) ).
cnf(i_0_2907,plain,
~ def_89(f__index_(f__cons_(f__index_(f__cons_(f__index_(f__cons_(X1,X2),n0),X3),n0),X4),n0),X1),
inference(rename_variables,[],[i_0_1587]) ).
cnf(i_0_3187,plain,
X1 = f_ADD_(f_ADD_(f_ADD_(f_ADD_(f_ADD_(f_ADD_(n0,n0),n0),n0),n0),n0),X1),
inference(rename_variables,[],[i_0_1597]) ).
cnf(i_0_3798,plain,
~ def_89(X1,f__index_(f__cons_(f__index_(f__cons_(f__index_(f__cons_(X1,X2),n0),X3),n0),X4),n0)),
inference(rename_variables,[],[i_0_1585]) ).
cnf(i_0_3800,plain,
~ def_89(f__index_(f__cons_(f__index_(f__cons_(f__index_(f__cons_(X1,X2),n0),X3),n0),X4),n0),X1),
inference(rename_variables,[],[i_0_1587]) ).
cnf(i_0_1063,plain,
def_89(n1,f_ADD_(f_ADD_(f_ADD_(f_ADD_(n0,n0),n0),n0),f_ADD_(n0,n0))),
inference(scs_inference,[],[i_0_1053,i_0_336]) ).
cnf(i_0_1064,plain,
f_ADD_(X1,n1) != f_ADD_(f_ADD_(f_ADD_(f_ADD_(n0,n0),n0),n0),f_ADD_(n0,n0)),
inference(rename_variables,[],[i_0_1053]) ).
cnf(i_0_1066,plain,
f_ADD_(f_ADD_(f_ADD_(f_ADD_(n0,n0),n0),n0),f_ADD_(n0,n0)) != n1,
inference(scs_inference,[],[i_0_1053,i_0_336,i_0_283]) ).
cnf(i_0_1068,plain,
p_LES_EQU_(f_ADD_(f_ADD_(f_ADD_(f_ADD_(n0,n0),n0),n0),f_ADD_(n0,n0)),n1),
inference(scs_inference,[],[i_0_1053,i_0_336,i_0_283,i_0_279]) ).
cnf(i_0_1070,plain,
f_ADD_(f_ADD_(f_ADD_(f_ADD_(n0,n0),n0),n0),n0) = f_SUB_(f_ADD_(n0,n0),n0),
inference(scs_inference,[],[i_0_1044,i_0_1053,i_0_336,i_0_283,i_0_279,i_0_304]) ).
cnf(i_0_1071,plain,
~ p_LES_EQU_(n1,f_ADD_(f_ADD_(f_ADD_(f_ADD_(n0,n0),n0),n0),f_ADD_(n0,n0))),
inference(scs_inference,[],[i_0_1044,i_0_1053,i_0_336,i_0_283,i_0_279,i_0_304,i_0_258]) ).
cnf(i_0_1075,plain,
f_ADD_(X1,n1) != f__index_(f__cons_(f_ADD_(n0,f__index_(f__cons_(n0,X2),n0)),X3),n0),
inference(scs_inference,[],[i_0_602,i_0_506,i_0_1044,i_0_1053,i_0_338,i_0_336,i_0_283,i_0_279,i_0_304,i_0_258,i_0_332,i_0_305]) ).
cnf(i_0_1260,plain,
n0 != f_ADD_(f__length_(f__slice_(X1,n0,f_ADD_(n0,n1))),f_ADD_(n0,n1)),
inference(scs_inference,[],[i_0_364,i_0_1252,i_0_1249,i_0_304,i_0_305]) ).
cnf(i_0_1283,plain,
f_ADD_(n0,n0) != f_ADD_(f__length_(f__slice_(X1,n0,f_ADD_(n0,n1))),f_ADD_(n0,n1)),
inference(scs_inference,[],[i_0_553,i_0_1249,i_0_270,i_0_304,i_0_305]) ).
cnf(i_0_1305,plain,
f_ADD_(f_ADD_(n0,n0),n0) != f_ADD_(f__length_(f__slice_(X1,n0,f_ADD_(n0,n1))),f_ADD_(n0,n1)),
inference(scs_inference,[],[i_0_694,i_0_1249,i_0_301,i_0_304,i_0_305]) ).
cnf(i_0_1323,plain,
f_SUB_(f_ADD_(n0,n0),n0) != f_ADD_(f__length_(f__slice_(X1,n0,f_ADD_(n0,n1))),f_ADD_(n0,n1)),
inference(scs_inference,[],[i_0_1249,i_0_739,i_0_305]) ).
cnf(i_0_1333,plain,
f_ADD_(n0,f_ADD_(n0,n0)) != f_ADD_(f__length_(f__slice_(X1,n0,f_ADD_(n0,n1))),f_ADD_(n0,n1)),
inference(scs_inference,[],[i_0_1249,i_0_919,i_0_305]) ).
cnf(i_0_1359,plain,
f__length_(f__empty_) != f_ADD_(f__length_(f__slice_(X1,n0,f_ADD_(n0,n1))),f_ADD_(n0,n1)),
inference(scs_inference,[],[i_0_1249,i_0_1220,i_0_305]) ).
cnf(i_0_1367,plain,
f_SUB_(X1,X1) != f_ADD_(f__length_(f__slice_(X2,n0,f_ADD_(n0,n1))),f_ADD_(n0,n1)),
inference(scs_inference,[],[i_0_1249,i_0_403,i_0_305]) ).
cnf(i_0_1505,plain,
~ p_LES_EQU_(f_ADD_(f__length_(f__slice_(X1,n0,f_ADD_(n0,n1))),f_ADD_(n0,n1)),f_SUB_(X2,X2)),
inference(scs_inference,[],[i_0_408,i_0_1249,i_0_332]) ).
cnf(i_0_1755,plain,
~ p__pred_(f__not_(f__or_(f__true_,X1))),
inference(scs_inference,[],[i_0_1638,i_0_284]) ).
cnf(i_0_1757,plain,
p__pred_(f__not_(f__nor_(f__true_,X1))),
inference(scs_inference,[],[i_0_1630,i_0_1638,i_0_284,i_0_295]) ).
cnf(i_0_1759,plain,
~ p__pred_(f__nor_(f__or_(f__true_,X1),X2)),
inference(scs_inference,[],[i_0_1630,i_0_1638,i_0_284,i_0_295,i_0_245]) ).
cnf(i_0_1761,plain,
~ p__pred_(f__nor_(X1,f__or_(f__true_,X2))),
inference(scs_inference,[],[i_0_1630,i_0_1638,i_0_284,i_0_295,i_0_245,i_0_246]) ).
cnf(i_0_1763,plain,
~ p__pred_(f__and_(f__nor_(f__true_,X1),X2)),
inference(scs_inference,[],[i_0_1630,i_0_1638,i_0_284,i_0_295,i_0_245,i_0_246,i_0_252]) ).
cnf(i_0_1765,plain,
~ p__pred_(f__and_(X1,f__nor_(f__true_,X2))),
inference(scs_inference,[],[i_0_1630,i_0_1638,i_0_284,i_0_295,i_0_245,i_0_246,i_0_252,i_0_253]) ).
cnf(i_0_1767,plain,
p__pred_(f__or_(f__or_(f__true_,X1),X2)),
inference(scs_inference,[],[i_0_1630,i_0_1638,i_0_284,i_0_295,i_0_245,i_0_246,i_0_252,i_0_253,i_0_277]) ).
cnf(i_0_1769,plain,
p__pred_(f__or_(X1,f__or_(f__true_,X2))),
inference(scs_inference,[],[i_0_1630,i_0_1638,i_0_284,i_0_295,i_0_245,i_0_246,i_0_252,i_0_253,i_0_277,i_0_278]) ).
cnf(i_0_1771,plain,
p__pred_(f__nand_(f__nor_(f__true_,X1),X2)),
inference(scs_inference,[],[i_0_1630,i_0_1638,i_0_284,i_0_295,i_0_245,i_0_246,i_0_252,i_0_253,i_0_277,i_0_278,i_0_280]) ).
cnf(i_0_1773,plain,
p__pred_(f__nand_(X1,f__nor_(f__true_,X2))),
inference(scs_inference,[],[i_0_1630,i_0_1638,i_0_284,i_0_295,i_0_245,i_0_246,i_0_252,i_0_253,i_0_277,i_0_278,i_0_280,i_0_281]) ).
cnf(i_0_1796,plain,
f__index_(f__cons_(X1,X2),f__length_(f__empty_)) = X1,
inference(rename_variables,[],[i_0_1666]) ).
cnf(i_0_1881,plain,
f__index_(f__cons_(X1,X2),f__length_(f__empty_)) = X1,
inference(rename_variables,[],[i_0_1666]) ).
cnf(i_0_1897,plain,
f__index_(f__cons_(X1,X2),f__length_(f__empty_)) = X1,
inference(rename_variables,[],[i_0_1666]) ).
cnf(i_0_1902,plain,
~ p__pred_(f__not_(f__or_(X1,f__true_))),
inference(scs_inference,[],[i_0_1640,i_0_284]) ).
cnf(i_0_1904,plain,
p__pred_(f__not_(f__nor_(X1,f__true_))),
inference(scs_inference,[],[i_0_1632,i_0_1640,i_0_284,i_0_295]) ).
cnf(i_0_1906,plain,
~ p__pred_(f__nor_(f__or_(X1,f__true_),X2)),
inference(scs_inference,[],[i_0_1632,i_0_1640,i_0_284,i_0_295,i_0_245]) ).
cnf(i_0_1908,plain,
~ p__pred_(f__nor_(X1,f__or_(X2,f__true_))),
inference(scs_inference,[],[i_0_1632,i_0_1640,i_0_284,i_0_295,i_0_245,i_0_246]) ).
cnf(i_0_1910,plain,
~ p__pred_(f__and_(f__nor_(X1,f__true_),X2)),
inference(scs_inference,[],[i_0_1632,i_0_1640,i_0_284,i_0_295,i_0_245,i_0_246,i_0_252]) ).
cnf(i_0_1912,plain,
~ p__pred_(f__and_(X1,f__nor_(X2,f__true_))),
inference(scs_inference,[],[i_0_1632,i_0_1640,i_0_284,i_0_295,i_0_245,i_0_246,i_0_252,i_0_253]) ).
cnf(i_0_1914,plain,
p__pred_(f__or_(f__or_(X1,f__true_),X2)),
inference(scs_inference,[],[i_0_1632,i_0_1640,i_0_284,i_0_295,i_0_245,i_0_246,i_0_252,i_0_253,i_0_277]) ).
cnf(i_0_1916,plain,
p__pred_(f__or_(X1,f__or_(X2,f__true_))),
inference(scs_inference,[],[i_0_1632,i_0_1640,i_0_284,i_0_295,i_0_245,i_0_246,i_0_252,i_0_253,i_0_277,i_0_278]) ).
cnf(i_0_1918,plain,
p__pred_(f__nand_(f__nor_(X1,f__true_),X2)),
inference(scs_inference,[],[i_0_1632,i_0_1640,i_0_284,i_0_295,i_0_245,i_0_246,i_0_252,i_0_253,i_0_277,i_0_278,i_0_280]) ).
cnf(i_0_1920,plain,
p__pred_(f__nand_(X1,f__nor_(X2,f__true_))),
inference(scs_inference,[],[i_0_1632,i_0_1640,i_0_284,i_0_295,i_0_245,i_0_246,i_0_252,i_0_253,i_0_277,i_0_278,i_0_280,i_0_281]) ).
cnf(i_0_2029,plain,
~ p__pred_(f__and_(f__false_,X1)),
inference(rename_variables,[],[i_0_1634]) ).
cnf(i_0_2051,plain,
~ p__pred_(f__not_(f__nand_(f__false_,X1))),
inference(scs_inference,[],[i_0_1642,i_0_284]) ).
cnf(i_0_2053,plain,
p__pred_(f__not_(f__and_(X1,f__false_))),
inference(scs_inference,[],[i_0_1636,i_0_1642,i_0_284,i_0_295]) ).
cnf(i_0_2055,plain,
~ p__pred_(f__nor_(f__nand_(f__false_,X1),X2)),
inference(scs_inference,[],[i_0_1636,i_0_1642,i_0_284,i_0_295,i_0_245]) ).
cnf(i_0_2057,plain,
~ p__pred_(f__nor_(X1,f__nand_(f__false_,X2))),
inference(scs_inference,[],[i_0_1636,i_0_1642,i_0_284,i_0_295,i_0_245,i_0_246]) ).
cnf(i_0_2059,plain,
~ p__pred_(f__and_(f__and_(X1,f__false_),X2)),
inference(scs_inference,[],[i_0_1636,i_0_1642,i_0_284,i_0_295,i_0_245,i_0_246,i_0_252]) ).
cnf(i_0_2061,plain,
~ p__pred_(f__and_(X1,f__and_(X2,f__false_))),
inference(scs_inference,[],[i_0_1636,i_0_1642,i_0_284,i_0_295,i_0_245,i_0_246,i_0_252,i_0_253]) ).
cnf(i_0_2063,plain,
p__pred_(f__or_(f__nand_(f__false_,X1),X2)),
inference(scs_inference,[],[i_0_1636,i_0_1642,i_0_284,i_0_295,i_0_245,i_0_246,i_0_252,i_0_253,i_0_277]) ).
cnf(i_0_2065,plain,
p__pred_(f__or_(X1,f__nand_(f__false_,X2))),
inference(scs_inference,[],[i_0_1636,i_0_1642,i_0_284,i_0_295,i_0_245,i_0_246,i_0_252,i_0_253,i_0_277,i_0_278]) ).
cnf(i_0_2067,plain,
p__pred_(f__nand_(f__and_(X1,f__false_),X2)),
inference(scs_inference,[],[i_0_1636,i_0_1642,i_0_284,i_0_295,i_0_245,i_0_246,i_0_252,i_0_253,i_0_277,i_0_278,i_0_280]) ).
cnf(i_0_2069,plain,
p__pred_(f__nand_(X1,f__and_(X2,f__false_))),
inference(scs_inference,[],[i_0_1636,i_0_1642,i_0_284,i_0_295,i_0_245,i_0_246,i_0_252,i_0_253,i_0_277,i_0_278,i_0_280,i_0_281]) ).
cnf(i_0_2200,plain,
~ p__pred_(f__not_(f__nand_(X1,f__false_))),
inference(scs_inference,[],[i_0_1644,i_0_284]) ).
cnf(i_0_2202,plain,
p__pred_(f__not_(f__not_(f__true_))),
inference(scs_inference,[],[i_0_1644,i_0_1626,i_0_284,i_0_295]) ).
cnf(i_0_2204,plain,
~ p__pred_(f__nor_(f__nand_(X1,f__false_),X2)),
inference(scs_inference,[],[i_0_1644,i_0_1626,i_0_284,i_0_295,i_0_245]) ).
cnf(i_0_2206,plain,
~ p__pred_(f__nor_(X1,f__nand_(X2,f__false_))),
inference(scs_inference,[],[i_0_1644,i_0_1626,i_0_284,i_0_295,i_0_245,i_0_246]) ).
cnf(i_0_2208,plain,
~ p__pred_(f__and_(f__not_(f__true_),X1)),
inference(scs_inference,[],[i_0_1644,i_0_1626,i_0_284,i_0_295,i_0_245,i_0_246,i_0_252]) ).
cnf(i_0_2210,plain,
~ p__pred_(f__and_(X1,f__not_(f__true_))),
inference(scs_inference,[],[i_0_1644,i_0_1626,i_0_284,i_0_295,i_0_245,i_0_246,i_0_252,i_0_253]) ).
cnf(i_0_2212,plain,
p__pred_(f__or_(f__nand_(X1,f__false_),X2)),
inference(scs_inference,[],[i_0_1644,i_0_1626,i_0_284,i_0_295,i_0_245,i_0_246,i_0_252,i_0_253,i_0_277]) ).
cnf(i_0_2214,plain,
p__pred_(f__or_(X1,f__nand_(X2,f__false_))),
inference(scs_inference,[],[i_0_1644,i_0_1626,i_0_284,i_0_295,i_0_245,i_0_246,i_0_252,i_0_253,i_0_277,i_0_278]) ).
cnf(i_0_2216,plain,
p__pred_(f__nand_(f__not_(f__true_),X1)),
inference(scs_inference,[],[i_0_1644,i_0_1626,i_0_284,i_0_295,i_0_245,i_0_246,i_0_252,i_0_253,i_0_277,i_0_278,i_0_280]) ).
cnf(i_0_2218,plain,
p__pred_(f__nand_(X1,f__not_(f__true_))),
inference(scs_inference,[],[i_0_1644,i_0_1626,i_0_284,i_0_295,i_0_245,i_0_246,i_0_252,i_0_253,i_0_277,i_0_278,i_0_280,i_0_281]) ).
cnf(i_0_2347,plain,
~ p__pred_(f__not_(f__not_(f__false_))),
inference(scs_inference,[],[i_0_1628,i_0_284]) ).
cnf(i_0_2349,plain,
p__pred_(f__not_(f__equal_(f__true_,f__false_))),
inference(scs_inference,[],[i_0_1628,i_0_1658,i_0_284,i_0_295]) ).
cnf(i_0_2351,plain,
~ p__pred_(f__nor_(f__not_(f__false_),X1)),
inference(scs_inference,[],[i_0_1628,i_0_1658,i_0_284,i_0_295,i_0_245]) ).
cnf(i_0_2353,plain,
~ p__pred_(f__nor_(X1,f__not_(f__false_))),
inference(scs_inference,[],[i_0_1628,i_0_1658,i_0_284,i_0_295,i_0_245,i_0_246]) ).
cnf(i_0_2355,plain,
~ p__pred_(f__and_(f__equal_(f__true_,f__false_),X1)),
inference(scs_inference,[],[i_0_1628,i_0_1658,i_0_284,i_0_295,i_0_245,i_0_246,i_0_252]) ).
cnf(i_0_2357,plain,
~ p__pred_(f__and_(X1,f__equal_(f__true_,f__false_))),
inference(scs_inference,[],[i_0_1628,i_0_1658,i_0_284,i_0_295,i_0_245,i_0_246,i_0_252,i_0_253]) ).
cnf(i_0_2359,plain,
p__pred_(f__or_(f__not_(f__false_),X1)),
inference(scs_inference,[],[i_0_1628,i_0_1658,i_0_284,i_0_295,i_0_245,i_0_246,i_0_252,i_0_253,i_0_277]) ).
cnf(i_0_2361,plain,
p__pred_(f__or_(X1,f__not_(f__false_))),
inference(scs_inference,[],[i_0_1628,i_0_1658,i_0_284,i_0_295,i_0_245,i_0_246,i_0_252,i_0_253,i_0_277,i_0_278]) ).
cnf(i_0_2363,plain,
p__pred_(f__nand_(f__equal_(f__true_,f__false_),X1)),
inference(scs_inference,[],[i_0_1628,i_0_1658,i_0_284,i_0_295,i_0_245,i_0_246,i_0_252,i_0_253,i_0_277,i_0_278,i_0_280]) ).
cnf(i_0_2365,plain,
p__pred_(f__nand_(X1,f__equal_(f__true_,f__false_))),
inference(scs_inference,[],[i_0_1628,i_0_1658,i_0_284,i_0_295,i_0_245,i_0_246,i_0_252,i_0_253,i_0_277,i_0_278,i_0_280,i_0_281]) ).
cnf(i_0_2467,plain,
f_ADD_(X1,n1) != f_ADD_(f_ADD_(f_ADD_(f_ADD_(f_ADD_(n0,n0),n0),n0),n0),n0),
inference(rename_variables,[],[i_0_1046]) ).
cnf(i_0_1267,plain,
n0 != f_ADD_(n0,n1),
inference(scs_inference,[],[i_0_1260,i_0_1214,i_0_257,i_0_304,i_0_305]) ).
cnf(i_0_1275,plain,
n0 != f_ADD_(n0,f__index_(f__cons_(n1,X1),n0)),
inference(scs_inference,[],[i_0_1252,i_0_1260,i_0_268,i_0_304,i_0_305]) ).
cnf(i_0_1290,plain,
f_ADD_(n0,n0) != f_ADD_(n0,n1),
inference(scs_inference,[],[i_0_1283,i_0_1214,i_0_182,i_0_304,i_0_305]) ).
cnf(i_0_1297,plain,
f_ADD_(n0,n0) != f_ADD_(n0,f__index_(f__cons_(n1,X1),n0)),
inference(scs_inference,[],[i_0_1283,i_0_1252,i_0_289,i_0_304,i_0_305]) ).
cnf(i_0_1299,plain,
n0 != f__index_(f__cons_(n1,X1),n0),
inference(scs_inference,[],[i_0_1283,i_0_1252,i_0_289,i_0_304,i_0_305,i_0_325]) ).
cnf(i_0_1311,plain,
f_ADD_(f_ADD_(n0,n0),n0) != f_ADD_(n0,n1),
inference(scs_inference,[],[i_0_1305,i_0_1214,i_0_305]) ).
cnf(i_0_1317,plain,
f_ADD_(f_ADD_(n0,n0),n0) != f_ADD_(n0,f__index_(f__cons_(n1,X1),n0)),
inference(scs_inference,[],[i_0_1252,i_0_1305,i_0_305]) ).
cnf(i_0_1455,plain,
f_SUB_(X1,X1) != f_ADD_(n0,n1),
inference(scs_inference,[],[i_0_1214,i_0_1367,i_0_305]) ).
cnf(i_0_1464,plain,
f_SUB_(f_ADD_(n0,n0),n0) != f_ADD_(n0,f__index_(f__cons_(n1,X1),n0)),
inference(scs_inference,[],[i_0_1252,i_0_1323,i_0_305]) ).
cnf(i_0_1473,plain,
f_ADD_(f_ADD_(f_ADD_(n0,n0),n0),n0) != f_ADD_(n0,n1),
inference(scs_inference,[],[i_0_1214,i_0_1328,i_0_305]) ).
cnf(i_0_1475,plain,
f_ADD_(f_ADD_(n0,n0),f_ADD_(n0,n0)) != f_ADD_(n0,f__index_(f__cons_(n1,X1),n0)),
inference(scs_inference,[],[i_0_1252,i_0_1338,i_0_305]) ).
cnf(i_0_1477,plain,
f_ADD_(f_ADD_(f_ADD_(n0,n0),n0),f_ADD_(n0,n0)) != f_ADD_(n0,n1),
inference(scs_inference,[],[i_0_1214,i_0_1343,i_0_305]) ).
cnf(i_0_1481,plain,
f__index_(f__others_(f_ADD_(n0,n0)),X1) != f_ADD_(n0,n1),
inference(scs_inference,[],[i_0_1214,i_0_1375,i_0_305]) ).
cnf(i_0_1483,plain,
f__index_(f__slice_(f__others_(f_ADD_(n0,n0)),X1,X2),X3) != f_ADD_(n0,f__index_(f__cons_(n1,X4),n0)),
inference(scs_inference,[],[i_0_1252,i_0_1383,i_0_305]) ).
cnf(i_0_1485,plain,
f_ADD_(n0,f_ADD_(n0,n0)) != f_ADD_(n0,n1),
inference(scs_inference,[],[i_0_1214,i_0_1333,i_0_305]) ).
cnf(i_0_1487,plain,
f__length_(f__slice_(X1,X2,f_ADD_(X2,n1))) != f_ADD_(n0,f__index_(f__cons_(n1,X3),n0)),
inference(scs_inference,[],[i_0_1252,i_0_1391,i_0_305]) ).
cnf(i_0_1489,plain,
f_SUB_(X1,f__index_(f__cons_(X1,X2),n0)) != f_ADD_(n0,n1),
inference(scs_inference,[],[i_0_1214,i_0_1399,i_0_305]) ).
cnf(i_0_1491,plain,
f_SUB_(f_SUB_(X1,X1),f__index_(f__cons_(n0,X2),n0)) != f_ADD_(n0,f__index_(f__cons_(n1,X3),n0)),
inference(scs_inference,[],[i_0_1252,i_0_1407,i_0_305]) ).
cnf(i_0_1493,plain,
f_SUB_(f_ADD_(n0,n0),f__index_(f__cons_(n0,X1),n0)) != f_ADD_(n0,n1),
inference(scs_inference,[],[i_0_1214,i_0_1415,i_0_305]) ).
cnf(i_0_1497,plain,
f_ADD_(f_ADD_(n0,n0),f_ADD_(n0,f__index_(f__cons_(n0,X1),n0))) != f_ADD_(n0,n1),
inference(scs_inference,[],[i_0_1214,i_0_1431,i_0_305]) ).
cnf(i_0_1499,plain,
f__index_(f__cons_(f_SUB_(X1,X1),X2),n0) != f_ADD_(n0,f__index_(f__cons_(n1,X3),n0)),
inference(scs_inference,[],[i_0_1252,i_0_1439,i_0_305]) ).
cnf(i_0_1501,plain,
f__index_(f__cons_(f_ADD_(n0,n0),X1),n0) != f_ADD_(n0,n1),
inference(scs_inference,[],[i_0_1214,i_0_1447,i_0_305]) ).
cnf(i_0_1503,plain,
f__length_(f__empty_) != f_ADD_(n0,f__index_(f__cons_(n1,X1),n0)),
inference(scs_inference,[],[i_0_1252,i_0_1359,i_0_305]) ).
cnf(i_0_1506,plain,
f_SUB_(X1,X1) != f_ADD_(n0,f__index_(f__cons_(n1,X2),n0)),
inference(scs_inference,[],[i_0_408,i_0_1249,i_0_1252,i_0_1367,i_0_332,i_0_305]) ).
cnf(i_0_1508,plain,
~ p_LES_EQU_(f_ADD_(f__length_(f__slice_(X1,n0,f_ADD_(n0,n1))),f_ADD_(n0,n1)),f_ADD_(n0,n0)),
inference(scs_inference,[],[i_0_408,i_0_449,i_0_1249,i_0_1252,i_0_1367,i_0_332,i_0_305,i_0_333]) ).
cnf(i_0_1515,plain,
f_ADD_(f_ADD_(f_ADD_(n0,n0),n0),n0) != f_ADD_(n0,f__index_(f__cons_(n1,X1),n0)),
inference(scs_inference,[],[i_0_392,i_0_1249,i_0_1252,i_0_1328,i_0_332,i_0_305]) ).
cnf(i_0_1518,plain,
f_ADD_(f_ADD_(n0,n0),f_ADD_(n0,n0)) != f_ADD_(n0,n1),
inference(scs_inference,[],[i_0_509,i_0_1249,i_0_1214,i_0_1338,i_0_332,i_0_305]) ).
cnf(i_0_1521,plain,
f_ADD_(f_ADD_(f_ADD_(n0,n0),n0),f_ADD_(n0,n0)) != f_ADD_(n0,f__index_(f__cons_(n1,X1),n0)),
inference(scs_inference,[],[i_0_621,i_0_1249,i_0_1252,i_0_1343,i_0_332,i_0_305]) ).
cnf(i_0_1527,plain,
f__index_(f__others_(f_ADD_(n0,n0)),X1) != f_ADD_(n0,f__index_(f__cons_(n1,X2),n0)),
inference(scs_inference,[],[i_0_745,i_0_1249,i_0_1252,i_0_1375,i_0_332,i_0_305]) ).
cnf(c_0_1300,axiom,
( p_LES_EQU_(X1,X2)
| ~ p_LES_EQU_(f_ADD_(X1,n1),f_ADD_(X2,n1)) ),
i_0_201 ).
cnf(c_0_1301,axiom,
f_ADD_(n0,X1) = X1,
i_0_297 ).
cnf(c_0_1302,plain,
( p_LES_EQU_(X1,n0)
| ~ p_LES_EQU_(f_ADD_(X1,n1),n1) ),
inference(spm,[status(thm)],[c_0_1300,c_0_1301]) ).
cnf(c_0_1303,axiom,
( X1 = f_ADD_(y_105(X1),n1)
| X1 = n0 ),
i_0_288 ).
cnf(c_0_1304,axiom,
( X1 = X2
| f_ADD_(X1,n1) != f_ADD_(X2,n1) ),
i_0_273 ).
cnf(c_0_1305,axiom,
f_ADD_(X1,n1) != n0,
i_0_290 ).
cnf(c_0_1306,axiom,
( X1 = n0
| ~ p_LES_EQU_(X1,n0) ),
i_0_285 ).
cnf(c_0_1307,plain,
( X1 = n0
| p_LES_EQU_(y_105(X1),n0)
| ~ p_LES_EQU_(X1,n1) ),
inference(spm,[status(thm)],[c_0_1302,c_0_1303]) ).
cnf(c_0_1308,plain,
p_LES_EQU_(f__length_(f__empty_),n1),
i_0_1222 ).
cnf(c_0_1309,axiom,
f__length_(f__empty_) = n0,
i_0_301 ).
cnf(c_0_1310,plain,
y_105(f_ADD_(X1,n1)) = X1,
inference(sr,[status(thm)],[inference(er,[status(thm)],[inference(spm,[status(thm)],[c_0_1304,c_0_1303])]),c_0_1305]) ).
cnf(c_0_1311,plain,
( y_105(X1) = n0
| X1 = n0
| ~ p_LES_EQU_(X1,n1) ),
inference(spm,[status(thm)],[c_0_1306,c_0_1307]) ).
cnf(c_0_1312,axiom,
( p_LES_EQU_(X1,X2)
| p_LES_EQU_(X3,X1)
| ~ p_LES_EQU_(X3,X2) ),
i_0_254 ).
cnf(c_0_1313,plain,
p_LES_EQU_(n0,n1),
inference(rw,[status(thm)],[c_0_1308,c_0_1309]) ).
cnf(c_0_1314,plain,
( n0 = X1
| ~ p_LES_EQU_(f_ADD_(X1,n1),n1) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1310,c_0_1311]),c_0_1305]) ).
cnf(c_0_1315,plain,
( p_LES_EQU_(X1,n1)
| p_LES_EQU_(n0,X1) ),
inference(spm,[status(thm)],[c_0_1312,c_0_1313]) ).
cnf(c_0_1316,axiom,
( p_LES_EQU_(f_ADD_(X1,n1),f_ADD_(X2,n1))
| ~ p_LES_EQU_(X1,X2) ),
i_0_223 ).
cnf(c_0_1317,axiom,
( f_ADD_(X1,n1) = X2
| p_LES_EQU_(X2,X1)
| ~ p_LES_EQU_(X2,f_ADD_(X1,n1)) ),
i_0_222 ).
cnf(c_0_1318,plain,
( n0 = X1
| p_LES_EQU_(n0,f_ADD_(X1,n1)) ),
inference(spm,[status(thm)],[c_0_1314,c_0_1315]) ).
cnf(c_0_1319,negated_conjecture,
p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTlevel_(t_206),fwork_DOTfifo_DOTrtl_DOTfifo__length_),
i_0_294 ).
cnf(c_0_1320,plain,
( p_LES_EQU_(n1,f_ADD_(X1,n1))
| ~ p_LES_EQU_(n0,X1) ),
inference(spm,[status(thm)],[c_0_1316,c_0_1301]) ).
cnf(c_0_1321,plain,
( n0 = X1
| p_LES_EQU_(n0,X1) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1317,c_0_1318]),c_0_1305]) ).
cnf(c_0_1322,negated_conjecture,
( p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTlevel_(t_206),X1)
| p_LES_EQU_(X1,fwork_DOTfifo_DOTrtl_DOTfifo__length_) ),
inference(spm,[status(thm)],[c_0_1312,c_0_1319]) ).
cnf(c_0_1323,plain,
( X1 = n0
| p_LES_EQU_(n1,X1)
| ~ p_LES_EQU_(n0,y_105(X1)) ),
inference(spm,[status(thm)],[c_0_1320,c_0_1303]) ).
cnf(c_0_1324,plain,
p_LES_EQU_(n0,X1),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1317,c_0_1321]),c_0_1305]) ).
cnf(c_0_1325,negated_conjecture,
~ p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTlevel_(f_ADD_(t_206,n1)),fwork_DOTfifo_DOTrtl_DOTfifo__length_),
i_0_220 ).
cnf(c_0_1326,plain,
( fwork_DOTfifo_DOTrtl_DOTlevel_(f_ADD_(X1,n1)) = n0
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X1)) ),
i_0_266 ).
cnf(c_0_1327,negated_conjecture,
( fwork_DOTfifo_DOTrtl_DOTlevel_(t_206) = n0
| p_LES_EQU_(n0,fwork_DOTfifo_DOTrtl_DOTfifo__length_) ),
inference(spm,[status(thm)],[c_0_1306,c_0_1322]) ).
cnf(c_0_1328,plain,
( X1 = n0
| p_LES_EQU_(n1,X1) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1323,c_0_1324])]) ).
cnf(c_0_1329,negated_conjecture,
( ~ p_LES_EQU_(n0,fwork_DOTfifo_DOTrtl_DOTfifo__length_)
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(t_206)) ),
inference(spm,[status(thm)],[c_0_1325,c_0_1326]) ).
cnf(c_0_1330,negated_conjecture,
p_LES_EQU_(n0,fwork_DOTfifo_DOTrtl_DOTfifo__length_),
inference(spm,[status(thm)],[c_0_1319,c_0_1327]) ).
cnf(c_0_1331,plain,
( X1 = n0
| n1 = X1
| ~ p_LES_EQU_(X1,n1) ),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_1303,c_0_1311]),c_0_1301]) ).
cnf(c_0_1332,plain,
( p_LES_EQU_(f_ADD_(X1,n1),n1)
| ~ p_LES_EQU_(X1,n0) ),
inference(spm,[status(thm)],[c_0_1316,c_0_1301]) ).
cnf(c_0_1333,axiom,
( X1 = X2
| ~ p_LES_EQU_(X1,X2)
| ~ p_LES_EQU_(X2,X1) ),
i_0_258 ).
cnf(c_0_1334,plain,
( X1 = n0
| p_LES_EQU_(n1,X2)
| p_LES_EQU_(X2,X1) ),
inference(spm,[status(thm)],[c_0_1312,c_0_1328]) ).
cnf(c_0_1335,axiom,
( p_LES_EQU_(X1,n0)
| ~ p_LES_EQU_(X1,f_SUB_(X1,n1)) ),
i_0_225 ).
cnf(c_0_1336,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)) ),
i_0_230 ).
cnf(c_0_1337,negated_conjecture,
~ p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(t_206)),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1329,c_0_1330])]) ).
cnf(c_0_1338,plain,
( f_ADD_(X1,n1) = n1
| ~ p_LES_EQU_(X1,n0) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1331,c_0_1332]),c_0_1305]) ).
cnf(c_0_1339,plain,
( X1 = n0
| p_LES_EQU_(X1,f_ADD_(X2,n1))
| ~ p_LES_EQU_(y_105(X1),X2) ),
inference(spm,[status(thm)],[c_0_1316,c_0_1303]) ).
cnf(c_0_1340,plain,
( X1 = n0
| X1 = X2
| p_LES_EQU_(n1,X2)
| ~ p_LES_EQU_(X1,X2) ),
inference(spm,[status(thm)],[c_0_1333,c_0_1334]) ).
cnf(c_0_1341,axiom,
( X1 = X2
| p_LES_EQU_(f_ADD_(X2,n1),X1)
| ~ p_LES_EQU_(X2,X1) ),
i_0_232 ).
cnf(c_0_1342,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) ),
i_0_215 ).
cnf(c_0_1343,negated_conjecture,
( p_LES_EQU_(f_SUB_(fwork_DOTfifo_DOTrtl_DOTlevel_(t_206),n1),fwork_DOTfifo_DOTrtl_DOTfifo__length_)
| p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTlevel_(t_206),n0) ),
inference(spm,[status(thm)],[c_0_1335,c_0_1322]) ).
cnf(c_0_1344,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)) ),
i_0_212 ).
cnf(c_0_1345,negated_conjecture,
( p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(t_206))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(t_206)) ),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_1325,c_0_1336]),c_0_1319])]),c_0_1337]) ).
cnf(c_0_1346,plain,
( f_ADD_(y_105(X1),n1) = n1
| X1 = n0
| ~ p_LES_EQU_(X1,n1) ),
inference(spm,[status(thm)],[c_0_1338,c_0_1307]) ).
cnf(c_0_1347,plain,
p_LES_EQU_(n1,f_ADD_(X1,n1)),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1320,c_0_1324])]) ).
cnf(c_0_1348,plain,
( X1 = n0
| p_LES_EQU_(X1,f_ADD_(X2,n1))
| ~ p_LES_EQU_(X1,n1) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_1339,c_0_1311]),c_0_1324])]) ).
cnf(c_0_1349,plain,
( f_ADD_(X1,n1) = X2
| X2 = X1
| p_LES_EQU_(n1,X2)
| ~ p_LES_EQU_(X1,X2) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1340,c_0_1341]),c_0_1305]) ).
cnf(c_0_1350,plain,
( fwork_DOTfifo_DOTrtl_DOTlevel_(f_ADD_(X1,n1)) = fwork_DOTfifo_DOTrtl_DOTlevel_(X1)
| p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X1))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X1))
| ~ p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTlevel_(X1),n0) ),
inference(csr,[status(thm)],[c_0_1342,c_0_1336]) ).
cnf(c_0_1351,negated_conjecture,
( p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTlevel_(t_206),n0)
| p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(t_206)) ),
inference(csr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1343,c_0_1344]),c_0_1325]),c_0_1337]),c_0_1345]) ).
cnf(c_0_1352,plain,
( X1 = y_105(X2)
| X2 = n0
| p_LES_EQU_(X2,X1)
| ~ p_LES_EQU_(y_105(X2),X1) ),
inference(spm,[status(thm)],[c_0_1341,c_0_1303]) ).
cnf(c_0_1353,plain,
( X1 = n0
| p_LES_EQU_(y_105(X1),X2)
| ~ p_LES_EQU_(X1,n1) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_1300,c_0_1346]),c_0_1347])]) ).
cnf(c_0_1354,plain,
( X1 = n0
| X2 = n0
| p_LES_EQU_(X2,X1)
| ~ p_LES_EQU_(X2,n1) ),
inference(spm,[status(thm)],[c_0_1348,c_0_1303]) ).
cnf(c_0_1355,plain,
n0 != f_ADD_(n0,n1),
i_0_1267 ).
cnf(c_0_1356,axiom,
n1 = f_ADD_(n0,n1),
i_0_298 ).
cnf(c_0_1357,negated_conjecture,
( f_ADD_(fwork_DOTfifo_DOTrtl_DOTlevel_(t_206),n1) = fwork_DOTfifo_DOTrtl_DOTfifo__length_
| fwork_DOTfifo_DOTrtl_DOTlevel_(t_206) = fwork_DOTfifo_DOTrtl_DOTfifo__length_
| p_LES_EQU_(n1,fwork_DOTfifo_DOTrtl_DOTfifo__length_) ),
inference(spm,[status(thm)],[c_0_1349,c_0_1319]) ).
cnf(c_0_1358,plain,
( fwork_DOTfifo_DOTrtl_DOTlevel_(f_ADD_(t_206,n1)) = fwork_DOTfifo_DOTrtl_DOTlevel_(t_206)
| p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(t_206)) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1350,c_0_1351]),c_0_1337]) ).
cnf(c_0_1359,plain,
( X1 = y_105(X2)
| X2 = n0
| p_LES_EQU_(X2,X1)
| ~ p_LES_EQU_(X2,n1) ),
inference(spm,[status(thm)],[c_0_1352,c_0_1353]) ).
cnf(c_0_1360,plain,
( X1 = n0
| p_LES_EQU_(f_ADD_(X2,n1),X1)
| ~ p_LES_EQU_(X2,n0) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1354,c_0_1332]),c_0_1305]) ).
cnf(c_0_1361,plain,
n1 != n0,
inference(rw,[status(thm)],[c_0_1355,c_0_1356]) ).
cnf(c_0_1362,axiom,
( def_89(X1,X2)
| f_SUB_(X2,X1) = X3
| f_ADD_(X3,X1) != X2 ),
i_0_248 ).
cnf(c_0_1363,plain,
( X1 = n0
| p_LES_EQU_(f_ADD_(X2,n1),X1)
| ~ p_LES_EQU_(X2,y_105(X1)) ),
inference(spm,[status(thm)],[c_0_1316,c_0_1303]) ).
cnf(c_0_1364,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)) ),
i_0_218 ).
cnf(c_0_1365,negated_conjecture,
( fwork_DOTfifo_DOTrtl_DOTlevel_(t_206) = fwork_DOTfifo_DOTrtl_DOTfifo__length_
| p_LES_EQU_(n1,fwork_DOTfifo_DOTrtl_DOTfifo__length_) ),
inference(spm,[status(thm)],[c_0_1347,c_0_1357]) ).
cnf(c_0_1366,negated_conjecture,
p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(t_206)),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_1325,c_0_1358]),c_0_1319])]) ).
cnf(c_0_1367,negated_conjecture,
~ p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,n0),
i_0_291 ).
cnf(c_0_1368,plain,
( X1 = X2
| p_LES_EQU_(f_ADD_(X2,n1),X1)
| ~ p_LES_EQU_(X2,n0) ),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_1359,c_0_1360]),c_0_1310]),c_0_1305]),c_0_1361]) ).
cnf(c_0_1369,axiom,
~ p_LES_EQU_(f_ADD_(X1,n1),n0),
i_0_244 ).
cnf(c_0_1370,axiom,
( p_LES_EQU_(X1,X2)
| ~ def_89(X2,X1) ),
i_0_279 ).
cnf(c_0_1371,plain,
( f_SUB_(f_ADD_(X1,X2),X2) = X1
| def_89(X2,f_ADD_(X1,X2)) ),
inference(er,[status(thm)],[c_0_1362]) ).
cnf(c_0_1372,plain,
( y_105(X1) = n0
| X1 = n0
| p_LES_EQU_(f_ADD_(n1,n1),X1) ),
inference(spm,[status(thm)],[c_0_1363,c_0_1328]) ).
cnf(c_0_1373,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)) ),
i_0_217 ).
cnf(c_0_1374,plain,
( fwork_DOTfifo_DOTrtl_DOTlevel_(f_ADD_(t_206,n1)) = fwork_DOTfifo_DOTrtl_DOTfifo__length_
| p_LES_EQU_(n1,fwork_DOTfifo_DOTrtl_DOTfifo__length_)
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(t_206)) ),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_1364,c_0_1365]),c_0_1366])]),c_0_1367]),c_0_1337]) ).
cnf(c_0_1375,axiom,
p_LES_EQU_(X1,X1),
i_0_296 ).
cnf(c_0_1376,plain,
( f_SUB_(f_ADD_(X1,n1),n1) = X1
| ~ p_LES_EQU_(X1,n0) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1335,c_0_1368]),c_0_1369]) ).
cnf(c_0_1377,plain,
( f_SUB_(f_ADD_(X1,X2),X2) = X1
| p_LES_EQU_(f_ADD_(X1,X2),X2) ),
inference(spm,[status(thm)],[c_0_1370,c_0_1371]) ).
cnf(c_0_1378,negated_conjecture,
( X1 = fwork_DOTfifo_DOTrtl_DOTlevel_(t_206)
| p_LES_EQU_(X1,fwork_DOTfifo_DOTrtl_DOTfifo__length_)
| ~ p_LES_EQU_(X1,fwork_DOTfifo_DOTrtl_DOTlevel_(t_206)) ),
inference(spm,[status(thm)],[c_0_1333,c_0_1322]) ).
cnf(c_0_1379,plain,
( X1 = n0
| n1 = X1
| p_LES_EQU_(f_ADD_(n1,n1),X1) ),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_1303,c_0_1372]),c_0_1301]) ).
cnf(c_0_1380,plain,
( fwork_DOTfifo_DOTrtl_DOTlevel_(f_ADD_(X1,n1)) = fwork_DOTfifo_DOTrtl_DOTlevel_(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_DOTlevel_(X1)) ),
inference(csr,[status(thm)],[c_0_1373,c_0_1336]) ).
cnf(c_0_1381,negated_conjecture,
( p_LES_EQU_(n1,fwork_DOTfifo_DOTrtl_DOTfifo__length_)
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(t_206)) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_1325,c_0_1374]),c_0_1375])]) ).
cnf(c_0_1382,plain,
( ~ p_LES_EQU_(f_ADD_(X1,n1),X1)
| ~ p_LES_EQU_(X1,n0) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1335,c_0_1376]),c_0_1369]) ).
cnf(c_0_1383,plain,
( p_LES_EQU_(f_ADD_(X1,n1),n1)
| ~ p_LES_EQU_(f_ADD_(X1,n1),X1) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1335,c_0_1377]),c_0_1369]) ).
cnf(c_0_1384,negated_conjecture,
( fwork_DOTfifo_DOTrtl_DOTlevel_(t_206) = f_ADD_(n1,n1)
| fwork_DOTfifo_DOTrtl_DOTlevel_(t_206) = n1
| fwork_DOTfifo_DOTrtl_DOTlevel_(t_206) = n0
| p_LES_EQU_(f_ADD_(n1,n1),fwork_DOTfifo_DOTrtl_DOTfifo__length_) ),
inference(spm,[status(thm)],[c_0_1378,c_0_1379]) ).
cnf(c_0_1385,plain,
~ p_LES_EQU_(n1,f_ADD_(n0,f_ADD_(n0,n0))),
i_0_924 ).
cnf(c_0_1386,plain,
( fwork_DOTfifo_DOTrtl_DOTlevel_(f_ADD_(t_206,n1)) = fwork_DOTfifo_DOTrtl_DOTfifo__length_
| p_LES_EQU_(n1,fwork_DOTfifo_DOTrtl_DOTfifo__length_) ),
inference(csr,[status(thm)],[inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_1380,c_0_1365]),c_0_1375])]),c_0_1337]),c_0_1381]) ).
cnf(c_0_1387,plain,
( X1 = n0
| ~ p_LES_EQU_(y_105(X1),n0)
| ~ p_LES_EQU_(X1,y_105(X1)) ),
inference(spm,[status(thm)],[c_0_1382,c_0_1303]) ).
cnf(c_0_1388,plain,
( X1 = n0
| p_LES_EQU_(y_105(X1),X2)
| ~ p_LES_EQU_(X1,f_ADD_(X2,n1)) ),
inference(spm,[status(thm)],[c_0_1300,c_0_1303]) ).
cnf(c_0_1389,plain,
( X1 = n0
| p_LES_EQU_(X1,n1)
| ~ p_LES_EQU_(X1,y_105(X1)) ),
inference(spm,[status(thm)],[c_0_1383,c_0_1303]) ).
cnf(c_0_1390,negated_conjecture,
( fwork_DOTfifo_DOTrtl_DOTlevel_(t_206) = n0
| fwork_DOTfifo_DOTrtl_DOTlevel_(t_206) = n1
| p_LES_EQU_(f_ADD_(n1,n1),fwork_DOTfifo_DOTrtl_DOTfifo__length_) ),
inference(spm,[status(thm)],[c_0_1319,c_0_1384]) ).
cnf(c_0_1391,plain,
~ p_LES_EQU_(n1,n0),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_1385,c_0_1301]),c_0_1301]) ).
cnf(c_0_1392,plain,
( X1 = n0
| p_LES_EQU_(X1,n1)
| ~ p_LES_EQU_(y_105(X1),n0) ),
inference(spm,[status(thm)],[c_0_1332,c_0_1303]) ).
cnf(c_0_1393,plain,
( p_LES_EQU_(X1,f_ADD_(X2,n1))
| p_LES_EQU_(f_ADD_(X3,n1),X1)
| ~ p_LES_EQU_(X3,X2) ),
inference(spm,[status(thm)],[c_0_1312,c_0_1316]) ).
cnf(c_0_1394,negated_conjecture,
p_LES_EQU_(n1,fwork_DOTfifo_DOTrtl_DOTfifo__length_),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_1325,c_0_1386]),c_0_1375])]) ).
cnf(c_0_1395,plain,
( X1 = n0
| ~ p_LES_EQU_(X1,y_105(X1)) ),
inference(csr,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_1387,c_0_1388]),c_0_1301]),c_0_1389]) ).
cnf(c_0_1396,plain,
( fwork_DOTfifo_DOTrtl_DOTlevel_(f_ADD_(t_206,n1)) = n1
| fwork_DOTfifo_DOTrtl_DOTlevel_(t_206) = n0
| p_LES_EQU_(f_ADD_(n1,n1),fwork_DOTfifo_DOTrtl_DOTfifo__length_)
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(t_206)) ),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_1364,c_0_1390]),c_0_1366])]),c_0_1391]),c_0_1337]) ).
cnf(c_0_1397,plain,
( X1 = n0
| p_LES_EQU_(f_ADD_(n1,n1),X1)
| p_LES_EQU_(X1,n1) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_1392,c_0_1372]),c_0_1375])]) ).
cnf(c_0_1398,negated_conjecture,
( p_LES_EQU_(f_ADD_(n1,n1),X1)
| p_LES_EQU_(X1,f_ADD_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,n1)) ),
inference(spm,[status(thm)],[c_0_1393,c_0_1394]) ).
cnf(c_0_1399,plain,
~ p_LES_EQU_(f_ADD_(X1,n1),X1),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1395,c_0_1310]),c_0_1305]) ).
cnf(c_0_1400,negated_conjecture,
( fwork_DOTfifo_DOTrtl_DOTlevel_(t_206) = n0
| p_LES_EQU_(f_ADD_(n1,n1),fwork_DOTfifo_DOTrtl_DOTfifo__length_)
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(t_206)) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_1325,c_0_1396]),c_0_1394])]) ).
cnf(c_0_1401,plain,
( p_LES_EQU_(X1,X2)
| ~ p_LES_EQU_(f_ADD_(X1,n1),n1) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1300,c_0_1348]),c_0_1305]) ).
cnf(c_0_1402,plain,
( p_LES_EQU_(f_ADD_(X1,n1),n1)
| p_LES_EQU_(n1,X1) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1300,c_0_1397]),c_0_1305]) ).
cnf(c_0_1403,negated_conjecture,
( p_LES_EQU_(f_ADD_(n1,n1),f_ADD_(f_ADD_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,n1),n1))
| p_LES_EQU_(f_ADD_(f_ADD_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,n1),n1),n1) ),
inference(spm,[status(thm)],[c_0_1383,c_0_1398]) ).
cnf(c_0_1404,plain,
~ p_LES_EQU_(f_ADD_(f_ADD_(X1,n1),n1),n1),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1399,c_0_1348]),c_0_1305]) ).
cnf(c_0_1405,plain,
( fwork_DOTfifo_DOTrtl_DOTlevel_(f_ADD_(t_206,n1)) = n1
| fwork_DOTfifo_DOTrtl_DOTlevel_(t_206) = n0
| p_LES_EQU_(f_ADD_(n1,n1),fwork_DOTfifo_DOTrtl_DOTfifo__length_)
| ~ p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,n1) ),
inference(csr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1380,c_0_1390]),c_0_1337]),c_0_1400]) ).
cnf(c_0_1406,plain,
( f_SUB_(f_ADD_(X1,n1),n1) = X1
| ~ p_LES_EQU_(X1,f_SUB_(f_ADD_(X1,n1),n1)) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1335,c_0_1341]),c_0_1369]) ).
cnf(c_0_1407,plain,
( p_LES_EQU_(n1,X1)
| p_LES_EQU_(X1,X2) ),
inference(spm,[status(thm)],[c_0_1401,c_0_1402]) ).
cnf(c_0_1408,negated_conjecture,
p_LES_EQU_(f_ADD_(n1,n1),f_ADD_(f_ADD_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,n1),n1)),
inference(sr,[status(thm)],[c_0_1403,c_0_1404]) ).
cnf(c_0_1409,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) ),
i_0_198 ).
cnf(c_0_1410,negated_conjecture,
( fwork_DOTfifo_DOTrtl_DOTlevel_(t_206) = n0
| p_LES_EQU_(f_ADD_(n1,n1),fwork_DOTfifo_DOTrtl_DOTfifo__length_)
| ~ p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,n1) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_1325,c_0_1405]),c_0_1394])]) ).
cnf(c_0_1411,plain,
( f_SUB_(f_ADD_(X1,n1),n1) = X1
| p_LES_EQU_(n1,X1) ),
inference(spm,[status(thm)],[c_0_1406,c_0_1407]) ).
cnf(c_0_1412,negated_conjecture,
( f_ADD_(f_ADD_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,n1),n1) = f_ADD_(n1,n1)
| ~ p_LES_EQU_(f_ADD_(f_ADD_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,n1),n1),f_ADD_(n1,n1)) ),
inference(spm,[status(thm)],[c_0_1333,c_0_1408]) ).
cnf(c_0_1413,plain,
( f_ADD_(X1,n1) = f_ADD_(X2,n1)
| p_LES_EQU_(f_ADD_(X2,n1),X1)
| ~ p_LES_EQU_(X2,X1) ),
inference(spm,[status(thm)],[c_0_1317,c_0_1316]) ).
cnf(c_0_1414,plain,
( fwork_DOTfifo_DOTrtl_DOTlevel_(f_ADD_(t_206,n1)) = n1
| p_LES_EQU_(f_ADD_(n1,n1),fwork_DOTfifo_DOTrtl_DOTfifo__length_)
| ~ p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,n1)
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(t_206)) ),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_1409,c_0_1410]),c_0_1301]),c_0_1375]),c_0_1366])]),c_0_1337]) ).
cnf(c_0_1415,plain,
( p_LES_EQU_(n1,X1)
| ~ p_LES_EQU_(f_ADD_(X1,n1),X1) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1335,c_0_1411]),c_0_1369]) ).
cnf(c_0_1416,negated_conjecture,
( f_ADD_(f_ADD_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,n1),n1) = f_ADD_(f_ADD_(n1,n1),n1)
| f_ADD_(f_ADD_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,n1),n1) = f_ADD_(n1,n1)
| ~ p_LES_EQU_(f_ADD_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,n1),f_ADD_(n1,n1)) ),
inference(spm,[status(thm)],[c_0_1412,c_0_1413]) ).
cnf(c_0_1417,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)) ),
i_0_213 ).
cnf(c_0_1418,negated_conjecture,
( p_LES_EQU_(f_ADD_(n1,n1),fwork_DOTfifo_DOTrtl_DOTfifo__length_)
| ~ p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,n1)
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(t_206)) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_1325,c_0_1414]),c_0_1394])]) ).
cnf(c_0_1419,plain,
( X1 = n0
| p_LES_EQU_(n1,y_105(X1))
| ~ p_LES_EQU_(X1,y_105(X1)) ),
inference(spm,[status(thm)],[c_0_1415,c_0_1303]) ).
cnf(c_0_1420,plain,
( X1 = n0
| p_LES_EQU_(X2,y_105(X1))
| ~ p_LES_EQU_(f_ADD_(X2,n1),X1) ),
inference(spm,[status(thm)],[c_0_1300,c_0_1303]) ).
cnf(c_0_1421,negated_conjecture,
( f_ADD_(f_ADD_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,n1),n1) = f_ADD_(f_ADD_(n1,n1),n1)
| f_ADD_(f_ADD_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,n1),n1) = f_ADD_(n1,n1)
| ~ p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,n1) ),
inference(spm,[status(thm)],[c_0_1416,c_0_1316]) ).
cnf(c_0_1422,plain,
( fwork_DOTfifo_DOTrtl_DOTlevel_(f_ADD_(t_206,n1)) = n1
| p_LES_EQU_(f_ADD_(n1,n1),fwork_DOTfifo_DOTrtl_DOTfifo__length_)
| ~ p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,n1) ),
inference(csr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_1417,c_0_1410]),c_0_1301]),c_0_1366])]),c_0_1367]),c_0_1337]),c_0_1418]) ).
cnf(c_0_1423,plain,
( X1 = n0
| p_LES_EQU_(n1,y_105(X1))
| ~ p_LES_EQU_(f_ADD_(X1,n1),X1) ),
inference(spm,[status(thm)],[c_0_1419,c_0_1420]) ).
cnf(c_0_1424,negated_conjecture,
( f_ADD_(f_ADD_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,n1),n1) = f_ADD_(n1,n1)
| ~ p_LES_EQU_(f_ADD_(f_ADD_(n1,n1),n1),f_ADD_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,n1))
| ~ p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,n1) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1383,c_0_1421]),c_0_1404]) ).
cnf(c_0_1425,negated_conjecture,
( p_LES_EQU_(f_ADD_(n1,n1),fwork_DOTfifo_DOTrtl_DOTfifo__length_)
| ~ p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,n1) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_1325,c_0_1422]),c_0_1394])]) ).
cnf(c_0_1426,plain,
( p_LES_EQU_(n1,X1)
| ~ p_LES_EQU_(f_ADD_(f_ADD_(X1,n1),n1),n1) ),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_1423,c_0_1348]),c_0_1310]),c_0_1305]),c_0_1305]) ).
cnf(c_0_1427,negated_conjecture,
( f_ADD_(f_ADD_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,n1),n1) = f_ADD_(n1,n1)
| ~ p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,n1) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_1424,c_0_1316]),c_0_1425]) ).
cnf(c_0_1428,plain,
~ p_LES_EQU_(f_ADD_(n1,n1),n1),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1426,c_0_1301]),c_0_1391]) ).
cnf(c_0_1429,plain,
( fwork_DOTfifo_DOTrtl_DOTlevel_(f_ADD_(X1,n1)) = f_ADD_(fwork_DOTfifo_DOTrtl_DOTlevel_(X1),n1)
| 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(spm,[status(thm)],[c_0_1409,c_0_1364]) ).
cnf(c_0_1430,negated_conjecture,
( ~ p_LES_EQU_(f_ADD_(n1,n1),f_ADD_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,n1))
| ~ p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,n1) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1383,c_0_1427]),c_0_1428]) ).
cnf(c_0_1431,negated_conjecture,
( fwork_DOTfifo_DOTrtl_DOTlevel_(f_ADD_(t_206,n1)) = fwork_DOTfifo_DOTrtl_DOTlevel_(t_206)
| ~ p_LES_EQU_(f_ADD_(fwork_DOTfifo_DOTrtl_DOTlevel_(t_206),n1),fwork_DOTfifo_DOTrtl_DOTfifo__length_)
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(t_206)) ),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_1325,c_0_1429]),c_0_1366])]),c_0_1337]) ).
cnf(c_0_1432,plain,
( p_LES_EQU_(f_ADD_(X1,n1),X2)
| p_LES_EQU_(X2,n1)
| ~ p_LES_EQU_(X1,n0) ),
inference(spm,[status(thm)],[c_0_1312,c_0_1332]) ).
cnf(c_0_1433,negated_conjecture,
~ p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,n1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_1430,c_0_1316]),c_0_1394])]) ).
cnf(c_0_1434,negated_conjecture,
( fwork_DOTfifo_DOTrtl_DOTlevel_(f_ADD_(t_206,n1)) = fwork_DOTfifo_DOTrtl_DOTlevel_(t_206)
| ~ p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTlevel_(t_206),n0)
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(t_206)) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1431,c_0_1432]),c_0_1433]) ).
cnf(c_0_1435,negated_conjecture,
( fwork_DOTfifo_DOTrtl_DOTlevel_(t_206) = fwork_DOTfifo_DOTrtl_DOTfifo__length_
| ~ p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,fwork_DOTfifo_DOTrtl_DOTlevel_(t_206)) ),
inference(spm,[status(thm)],[c_0_1333,c_0_1319]) ).
cnf(c_0_1436,plain,
( fwork_DOTfifo_DOTrtl_DOTlevel_(f_ADD_(t_206,n1)) = fwork_DOTfifo_DOTrtl_DOTlevel_(t_206)
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(t_206)) ),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_1434,c_0_1364]),c_0_1366])]),c_0_1337]) ).
cnf(c_0_1437,negated_conjecture,
( fwork_DOTfifo_DOTrtl_DOTlevel_(f_ADD_(t_206,n1)) = f_ADD_(fwork_DOTfifo_DOTrtl_DOTlevel_(t_206),n1)
| fwork_DOTfifo_DOTrtl_DOTlevel_(t_206) = fwork_DOTfifo_DOTrtl_DOTfifo__length_
| p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(t_206)) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1435,c_0_1417]),c_0_1337]),c_0_1366])]) ).
cnf(c_0_1438,negated_conjecture,
~ p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(t_206)),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_1325,c_0_1436]),c_0_1319])]) ).
cnf(c_0_1439,negated_conjecture,
( fwork_DOTfifo_DOTrtl_DOTlevel_(f_ADD_(t_206,n1)) = f_ADD_(fwork_DOTfifo_DOTrtl_DOTlevel_(t_206),n1)
| fwork_DOTfifo_DOTrtl_DOTlevel_(t_206) = fwork_DOTfifo_DOTrtl_DOTfifo__length_ ),
inference(sr,[status(thm)],[c_0_1437,c_0_1438]) ).
cnf(c_0_1440,negated_conjecture,
( fwork_DOTfifo_DOTrtl_DOTlevel_(t_206) = fwork_DOTfifo_DOTrtl_DOTfifo__length_
| ~ p_LES_EQU_(f_ADD_(fwork_DOTfifo_DOTrtl_DOTlevel_(t_206),n1),fwork_DOTfifo_DOTrtl_DOTfifo__length_) ),
inference(spm,[status(thm)],[c_0_1325,c_0_1439]) ).
cnf(c_0_1441,negated_conjecture,
fwork_DOTfifo_DOTrtl_DOTlevel_(t_206) = fwork_DOTfifo_DOTrtl_DOTfifo__length_,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_1440,c_0_1341]),c_0_1319])]) ).
cnf(c_0_1442,plain,
fwork_DOTfifo_DOTrtl_DOTlevel_(f_ADD_(t_206,n1)) = fwork_DOTfifo_DOTrtl_DOTfifo__length_,
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_1380,c_0_1441]),c_0_1375])]),c_0_1337]),c_0_1438]) ).
cnf(c_0_1443,negated_conjecture,
$false,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_1325,c_0_1442]),c_0_1375])]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.08 % Problem : HWV029-2 : TPTP v9.2.1. Released v2.5.0.
% 0.00/0.08 % 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.09/0.27 % Computer : n020.cluster.edu
% 0.09/0.27 % Model : x86_64 x86_64
% 0.09/0.27 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.27 % Memory : 8042.1875MB
% 0.09/0.27 % OS : Linux 3.10.0-693.el7.x86_64
% 0.09/0.27 % CPULimit : 300
% 0.09/0.27 % WCLimit : 300
% 0.09/0.27 % DateTime : Mon May 4 19:11:19 EDT 2026
% 0.09/0.27 % CPUTime :
% 0.09/0.28 % start to proof: theBenchmark
% 209.72/135.78 % Version : CSE_E---1.7
% 209.72/135.78 % Problem : theBenchmark.p
% 209.72/135.78 % SZS status Unsatisfiable for theBenchmark.p
% 209.72/135.78 % SZS output start CNFRefutation
% See solution above
% 226.84/152.92 % Total time : 134.975s
%------------------------------------------------------------------------------