%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : HWV031-1 : TPTP v9.2.1. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox2/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox2/solver/bin/cse --final-prover /export/starexec/sandbox2/solver/bin/eprover --proof-time %d --global-time-limit %d
% Computer : n001.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 162.07s 110.40s
% Output : CNFRefutation 167.46s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named c_0_94)
% Comments :
%------------------------------------------------------------------------------
cnf(axiom_38,axiom,
( p_Reset(X1)
| p_Rd(X1)
| X2 = wr_level(X1)
| p_Mem(X2,X3,X1)
| ~ p_Wr(X1)
| ~ gt(fifo_length,int_level(X1))
| ~ p_Mem(X2,X3,plus(X1,n1)) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV003-0.ax',axiom_38) ).
cnf(axiom_21,axiom,
level(X1) = int_level(X1),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV003-0.ax',axiom_21) ).
cnf(axiom_39,axiom,
( p_Reset(X1)
| p_Rd(X1)
| X2 = wr_level(X1)
| p_Mem(X2,X3,plus(X1,n1))
| ~ p_Wr(X1)
| ~ gt(fifo_length,int_level(X1))
| ~ p_Mem(X2,X3,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV003-0.ax',axiom_39) ).
cnf(axiom_45,axiom,
( p_Reset(X1)
| p_Rd(X1)
| gt(fifo_length,int_level(X1))
| p_Mem(X2,X3,X1)
| ~ p_Wr(X1)
| ~ p_Mem(X2,X3,plus(X1,n1)) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV003-0.ax',axiom_45) ).
cnf(axiom_46,axiom,
( p_Reset(X1)
| p_Rd(X1)
| gt(fifo_length,int_level(X1))
| p_Mem(X2,X3,plus(X1,n1))
| ~ p_Wr(X1)
| ~ p_Mem(X2,X3,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV003-0.ax',axiom_46) ).
cnf(axiom_36,axiom,
( p_Reset(X1)
| p_Rd(X1)
| p_Data_in(X2,X1)
| ~ p_Wr(X1)
| ~ gt(fifo_length,int_level(X1))
| ~ p_Mem(wr_level(X1),X2,plus(X1,n1)) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV003-0.ax',axiom_36) ).
cnf(axiom_55,axiom,
( p_Reset(X1)
| p_Data_out(X2,plus(X1,n1))
| ~ p_Wr(X1)
| ~ p_Rd(X1)
| ~ gt(int_level(X1),n0)
| ~ p_Mem(rd_level(X1),X2,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV003-0.ax',axiom_55) ).
cnf(axiom_73,axiom,
( p_Reset(X1)
| p_Wr(X1)
| p_Data_out(X2,plus(X1,n1))
| ~ p_Rd(X1)
| ~ gt(int_level(X1),n0)
| ~ p_Mem(rd_level(X1),X2,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV003-0.ax',axiom_73) ).
cnf(axiom_54,axiom,
( p_Reset(X1)
| p_Mem(rd_level(X1),X2,X1)
| ~ p_Wr(X1)
| ~ p_Rd(X1)
| ~ gt(int_level(X1),n0)
| ~ p_Data_out(X2,plus(X1,n1)) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV003-0.ax',axiom_54) ).
cnf(axiom_72,axiom,
( p_Reset(X1)
| p_Wr(X1)
| p_Mem(rd_level(X1),X2,X1)
| ~ p_Rd(X1)
| ~ gt(int_level(X1),n0)
| ~ p_Data_out(X2,plus(X1,n1)) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV003-0.ax',axiom_72) ).
cnf(axiom_56,axiom,
( p_Reset(X1)
| rd_level(plus(X1,n1)) = plus(rd_level(X1),n1)
| ~ p_Wr(X1)
| ~ p_Rd(X1)
| ~ gt(int_level(X1),n0)
| ~ gt(minus(fifo_length,n1),rd_level(X1)) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV003-0.ax',axiom_56) ).
cnf(axiom_74,axiom,
( p_Reset(X1)
| p_Wr(X1)
| rd_level(plus(X1,n1)) = plus(rd_level(X1),n1)
| ~ p_Rd(X1)
| ~ gt(int_level(X1),n0)
| ~ gt(minus(fifo_length,n1),rd_level(X1)) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV003-0.ax',axiom_74) ).
cnf(axiom_40,axiom,
( p_Reset(X1)
| p_Rd(X1)
| wr_level(plus(X1,n1)) = plus(wr_level(X1),n1)
| ~ p_Wr(X1)
| ~ gt(fifo_length,int_level(X1))
| ~ gt(minus(fifo_length,n1),wr_level(X1)) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV003-0.ax',axiom_40) ).
cnf(axiom_37,axiom,
( p_Reset(X1)
| p_Rd(X1)
| p_Mem(wr_level(X1),X2,plus(X1,n1))
| ~ p_Wr(X1)
| ~ gt(fifo_length,int_level(X1))
| ~ p_Data_in(X2,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV003-0.ax',axiom_37) ).
cnf(axiom_57,axiom,
( p_Reset(X1)
| gt(minus(fifo_length,n1),rd_level(X1))
| rd_level(plus(X1,n1)) = n0
| ~ p_Wr(X1)
| ~ p_Rd(X1)
| ~ gt(int_level(X1),n0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV003-0.ax',axiom_57) ).
cnf(axiom_75,axiom,
( p_Reset(X1)
| p_Wr(X1)
| gt(minus(fifo_length,n1),rd_level(X1))
| rd_level(plus(X1,n1)) = n0
| ~ p_Rd(X1)
| ~ gt(int_level(X1),n0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV003-0.ax',axiom_75) ).
cnf(axiom_41,axiom,
( p_Reset(X1)
| p_Rd(X1)
| gt(minus(fifo_length,n1),wr_level(X1))
| wr_level(plus(X1,n1)) = n0
| ~ p_Wr(X1)
| ~ gt(fifo_length,int_level(X1)) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV003-0.ax',axiom_41) ).
cnf(axiom_61,axiom,
( p_Reset(X1)
| gt(int_level(X1),n0)
| p_Data_out(X2,X1)
| ~ p_Wr(X1)
| ~ p_Rd(X1)
| ~ p_Data_out(X2,plus(X1,n1)) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV003-0.ax',axiom_61) ).
cnf(axiom_79,axiom,
( p_Reset(X1)
| p_Wr(X1)
| gt(int_level(X1),n0)
| p_Data_out(X2,X1)
| ~ p_Rd(X1)
| ~ p_Data_out(X2,plus(X1,n1)) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV003-0.ax',axiom_79) ).
cnf(axiom_62,axiom,
( p_Reset(X1)
| gt(int_level(X1),n0)
| p_Data_out(X2,plus(X1,n1))
| ~ p_Wr(X1)
| ~ p_Rd(X1)
| ~ p_Data_out(X2,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV003-0.ax',axiom_62) ).
cnf(axiom_80,axiom,
( p_Reset(X1)
| p_Wr(X1)
| gt(int_level(X1),n0)
| p_Data_out(X2,plus(X1,n1))
| ~ p_Rd(X1)
| ~ p_Data_out(X2,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV003-0.ax',axiom_80) ).
cnf(axiom_52,axiom,
( p_Reset(X1)
| ~ p_Wr(X1)
| ~ p_Rd(X1)
| ~ gt(int_level(X1),n0)
| ~ p_Rd_error(plus(X1,n1)) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV003-0.ax',axiom_52) ).
cnf(axiom_71,axiom,
( p_Reset(X1)
| p_Wr(X1)
| int_level(plus(X1,n1)) = minus(int_level(X1),n1)
| ~ p_Rd(X1)
| ~ gt(int_level(X1),n0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV003-0.ax',axiom_71) ).
cnf(axiom_35,axiom,
( p_Reset(X1)
| p_Rd(X1)
| int_level(plus(X1,n1)) = plus(int_level(X1),n1)
| ~ p_Wr(X1)
| ~ gt(fifo_length,int_level(X1)) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV003-0.ax',axiom_35) ).
cnf(axiom_70,axiom,
( p_Reset(X1)
| p_Wr(X1)
| ~ p_Rd(X1)
| ~ gt(int_level(X1),n0)
| ~ p_Rd_error(plus(X1,n1)) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV003-0.ax',axiom_70) ).
cnf(axiom_34,axiom,
( p_Reset(X1)
| p_Rd(X1)
| ~ p_Wr(X1)
| ~ gt(fifo_length,int_level(X1))
| ~ p_Wr_error(plus(X1,n1)) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV003-0.ax',axiom_34) ).
cnf(axiom_59,axiom,
( p_Reset(X1)
| gt(int_level(X1),n0)
| int_level(plus(X1,n1)) = plus(int_level(X1),n1)
| ~ p_Wr(X1)
| ~ p_Rd(X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV003-0.ax',axiom_59) ).
cnf(axiom_53,axiom,
( p_Reset(X1)
| int_level(plus(X1,n1)) = int_level(X1)
| ~ p_Wr(X1)
| ~ p_Rd(X1)
| ~ gt(int_level(X1),n0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV003-0.ax',axiom_53) ).
cnf(axiom_60,axiom,
( p_Reset(X1)
| gt(int_level(X1),n0)
| rd_level(plus(X1,n1)) = rd_level(X1)
| ~ p_Wr(X1)
| ~ p_Rd(X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV003-0.ax',axiom_60) ).
cnf(axiom_77,axiom,
( p_Reset(X1)
| p_Wr(X1)
| gt(int_level(X1),n0)
| rd_level(plus(X1,n1)) = rd_level(X1)
| ~ p_Rd(X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV003-0.ax',axiom_77) ).
cnf(axiom_78,axiom,
( p_Reset(X1)
| p_Wr(X1)
| gt(int_level(X1),n0)
| int_level(plus(X1,n1)) = int_level(X1)
| ~ p_Rd(X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV003-0.ax',axiom_78) ).
cnf(axiom_43,axiom,
( p_Reset(X1)
| p_Rd(X1)
| gt(fifo_length,int_level(X1))
| wr_level(plus(X1,n1)) = wr_level(X1)
| ~ p_Wr(X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV003-0.ax',axiom_43) ).
cnf(axiom_44,axiom,
( p_Reset(X1)
| p_Rd(X1)
| gt(fifo_length,int_level(X1))
| int_level(plus(X1,n1)) = int_level(X1)
| ~ p_Wr(X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV003-0.ax',axiom_44) ).
cnf(axiom_58,axiom,
( p_Reset(X1)
| gt(int_level(X1),n0)
| p_Rd_error(plus(X1,n1))
| ~ p_Wr(X1)
| ~ p_Rd(X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV003-0.ax',axiom_58) ).
cnf(axiom_76,axiom,
( p_Reset(X1)
| p_Wr(X1)
| gt(int_level(X1),n0)
| p_Rd_error(plus(X1,n1))
| ~ p_Rd(X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV003-0.ax',axiom_76) ).
cnf(axiom_42,axiom,
( p_Reset(X1)
| p_Rd(X1)
| gt(fifo_length,int_level(X1))
| p_Wr_error(plus(X1,n1))
| ~ p_Wr(X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV003-0.ax',axiom_42) ).
cnf(axiom_82,axiom,
( p_Reset(X1)
| p_Wr(X1)
| p_Rd(X1)
| int_level(plus(X1,n1)) = int_level(X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV003-0.ax',axiom_82) ).
cnf(axiom_26,axiom,
( int_level(plus(X1,n1)) = n0
| ~ p_Reset(X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV003-0.ax',axiom_26) ).
cnf(axiom_24,axiom,
( p_Empty(X1)
| int_level(X1) != n0 ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV003-0.ax',axiom_24) ).
cnf(axiom_22,axiom,
( p_Full(X1)
| int_level(X1) != fifo_length ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV003-0.ax',axiom_22) ).
cnf(axiom_23,axiom,
( int_level(X1) = fifo_length
| ~ p_Full(X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV003-0.ax',axiom_23) ).
cnf(axiom_25,axiom,
( int_level(X1) = n0
| ~ p_Empty(X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV003-0.ax',axiom_25) ).
cnf(axiom_65,axiom,
( p_Reset(X1)
| X2 = wr_level(X1)
| p_Mem(X2,X3,X1)
| ~ p_Wr(X1)
| ~ p_Rd(X1)
| ~ p_Mem(X2,X3,plus(X1,n1)) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV003-0.ax',axiom_65) ).
cnf(axiom_66,axiom,
( p_Reset(X1)
| X2 = wr_level(X1)
| p_Mem(X2,X3,plus(X1,n1))
| ~ p_Wr(X1)
| ~ p_Rd(X1)
| ~ p_Mem(X2,X3,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV003-0.ax',axiom_66) ).
cnf(axiom_87,axiom,
( p_Reset(X1)
| p_Wr(X1)
| p_Mem(X2,X3,X1)
| ~ p_Mem(X2,X3,plus(X1,n1)) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV003-0.ax',axiom_87) ).
cnf(axiom_88,axiom,
( p_Reset(X1)
| p_Wr(X1)
| p_Mem(X2,X3,plus(X1,n1))
| ~ p_Mem(X2,X3,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV003-0.ax',axiom_88) ).
cnf(axiom_63,axiom,
( p_Reset(X1)
| p_Data_in(X2,X1)
| ~ p_Wr(X1)
| ~ p_Rd(X1)
| ~ p_Mem(wr_level(X1),X2,plus(X1,n1)) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV003-0.ax',axiom_63) ).
cnf(axiom_31,axiom,
( ~ p_Reset(X1)
| ~ p_Mem(X2,X3,plus(X1,n1)) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV003-0.ax',axiom_31) ).
cnf(axiom_67,axiom,
( p_Reset(X1)
| wr_level(plus(X1,n1)) = plus(wr_level(X1),n1)
| ~ p_Wr(X1)
| ~ p_Rd(X1)
| ~ gt(minus(fifo_length,n1),wr_level(X1)) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV003-0.ax',axiom_67) ).
cnf(quest_2,negated_conjecture,
gt(plus(wr_level(plus(x_139,n1)),n1),fifo_length),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',quest_2) ).
cnf(axiom_64,axiom,
( p_Reset(X1)
| p_Mem(wr_level(X1),X2,plus(X1,n1))
| ~ p_Wr(X1)
| ~ p_Rd(X1)
| ~ p_Data_in(X2,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV003-0.ax',axiom_64) ).
cnf(axiom_9,axiom,
( gt(X1,X2)
| ~ gt(plus(X1,n1),plus(X2,n1)) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV003-0.ax',axiom_9) ).
cnf(axiom_47,axiom,
( p_Reset(X1)
| p_Rd(X1)
| p_Data_out(X2,X1)
| ~ p_Wr(X1)
| ~ p_Data_out(X2,plus(X1,n1)) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV003-0.ax',axiom_47) ).
cnf(axiom_83,axiom,
( p_Reset(X1)
| p_Wr(X1)
| p_Rd(X1)
| p_Data_out(X2,X1)
| ~ p_Data_out(X2,plus(X1,n1)) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV003-0.ax',axiom_83) ).
cnf(axiom_68,axiom,
( p_Reset(X1)
| gt(minus(fifo_length,n1),wr_level(X1))
| wr_level(plus(X1,n1)) = n0
| ~ p_Wr(X1)
| ~ p_Rd(X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV003-0.ax',axiom_68) ).
cnf(axiom_8,axiom,
( gt(plus(X1,n1),plus(X2,n1))
| ~ gt(X1,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV003-0.ax',axiom_8) ).
cnf(axiom_48,axiom,
( p_Reset(X1)
| p_Rd(X1)
| p_Data_out(X2,plus(X1,n1))
| ~ p_Wr(X1)
| ~ p_Data_out(X2,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV003-0.ax',axiom_48) ).
cnf(axiom_11,axiom,
( gt(X1,X2)
| X1 = X2
| ~ gt(plus(X1,n1),X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV003-0.ax',axiom_11) ).
cnf(axiom_10,axiom,
( gt(X1,X2)
| X2 = X1
| ~ gt(plus(X1,n1),X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV003-0.ax',axiom_10) ).
cnf(axiom_84,axiom,
( p_Reset(X1)
| p_Wr(X1)
| p_Rd(X1)
| p_Data_out(X2,plus(X1,n1))
| ~ p_Data_out(X2,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV003-0.ax',axiom_84) ).
cnf(axiom_14,axiom,
( plus(X2,n1) = X1
| gt(X1,plus(X2,n1))
| ~ gt(X1,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV003-0.ax',axiom_14) ).
cnf(axiom_32,axiom,
( ~ p_Reset(X1)
| ~ p_Data_out(X2,plus(X1,n1)) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV003-0.ax',axiom_32) ).
cnf(quest_1,negated_conjecture,
~ gt(plus(wr_level(x_139),n1),fifo_length),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',quest_1) ).
cnf(axiom_49,axiom,
( p_Reset(X1)
| p_Rd(X1)
| p_Rd_error(X1)
| ~ p_Wr(X1)
| ~ p_Rd_error(plus(X1,n1)) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV003-0.ax',axiom_49) ).
cnf(axiom_51,axiom,
( p_Reset(X1)
| ~ p_Wr(X1)
| ~ p_Rd(X1)
| ~ p_Wr_error(plus(X1,n1)) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV003-0.ax',axiom_51) ).
cnf(axiom_85,axiom,
( p_Reset(X1)
| p_Wr(X1)
| p_Rd(X1)
| p_Rd_error(X1)
| ~ p_Rd_error(plus(X1,n1)) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV003-0.ax',axiom_85) ).
cnf(axiom_13,axiom,
( gt(X1,X3)
| ~ gt(X1,X2)
| ~ gt(X2,X3) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV003-0.ax',axiom_13) ).
cnf(axiom_3,axiom,
( gt(X1,minus(X1,n1))
| ~ gt(X1,n0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV003-0.ax',axiom_3) ).
cnf(axiom_89,axiom,
( p_Reset(X1)
| p_Wr(X1)
| p_Wr_error(X1)
| ~ p_Wr_error(plus(X1,n1)) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV003-0.ax',axiom_89) ).
cnf(axiom_5,axiom,
( minus(X1,X2) = X3
| def_10(X2,X1)
| plus(X3,X2) != X1 ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV003-0.ax',axiom_5) ).
cnf(axiom_4,axiom,
( plus(X3,X2) = X1
| def_10(X2,X1)
| minus(X1,X2) != X3 ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV003-0.ax',axiom_4) ).
cnf(axiom_50,axiom,
( p_Reset(X1)
| p_Rd(X1)
| p_Rd_error(plus(X1,n1))
| ~ p_Wr(X1)
| ~ p_Rd_error(X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV003-0.ax',axiom_50) ).
cnf(axiom_30,axiom,
( ~ p_Reset(X1)
| ~ p_Rd_error(plus(X1,n1)) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV003-0.ax',axiom_30) ).
cnf(axiom_29,axiom,
( ~ p_Reset(X1)
| ~ p_Wr_error(plus(X1,n1)) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV003-0.ax',axiom_29) ).
cnf(axiom_86,axiom,
( p_Reset(X1)
| p_Wr(X1)
| p_Rd(X1)
| p_Rd_error(plus(X1,n1))
| ~ p_Rd_error(X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV003-0.ax',axiom_86) ).
cnf(axiom_33,axiom,
( p_Reset(X1)
| p_Rd(X1)
| rd_level(plus(X1,n1)) = rd_level(X1)
| ~ p_Wr(X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV003-0.ax',axiom_33) ).
cnf(axiom_6,axiom,
( ~ def_10(X1,X2)
| ~ gt(X2,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV003-0.ax',axiom_6) ).
cnf(axiom_81,axiom,
( p_Reset(X1)
| p_Wr(X1)
| p_Rd(X1)
| rd_level(plus(X1,n1)) = rd_level(X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV003-0.ax',axiom_81) ).
cnf(axiom_90,axiom,
( p_Reset(X1)
| p_Wr(X1)
| p_Wr_error(plus(X1,n1))
| ~ p_Wr_error(X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV003-0.ax',axiom_90) ).
cnf(axiom_18,axiom,
( X1 = X2
| plus(X1,n1) != plus(X2,n1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV003-0.ax',axiom_18) ).
cnf(axiom_69,axiom,
( p_Reset(X1)
| p_Wr(X1)
| wr_level(plus(X1,n1)) = wr_level(X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV003-0.ax',axiom_69) ).
cnf(axiom_2,axiom,
gt(plus(X1,n1),n0),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV003-0.ax',axiom_2) ).
cnf(axiom_28,axiom,
( rd_level(plus(X1,n1)) = n0
| ~ p_Reset(X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV003-0.ax',axiom_28) ).
cnf(axiom_27,axiom,
( wr_level(plus(X1,n1)) = n0
| ~ p_Reset(X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV003-0.ax',axiom_27) ).
cnf(axiom_12,axiom,
( gt(X1,X2)
| X2 = X1
| gt(X2,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV003-0.ax',axiom_12) ).
cnf(axiom_7,axiom,
( ~ def_10(X1,X2)
| X2 != X1 ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV003-0.ax',axiom_7) ).
cnf(axiom_17,axiom,
~ gt(X1,X1),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV003-0.ax',axiom_17) ).
cnf(axiom_16,axiom,
( X1 = n0
| X1 = plus(y_27(X1),n1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV003-0.ax',axiom_16) ).
cnf(axiom_1,axiom,
plus(X1,n1) != n0,
file('/export/starexec/sandbox2/benchmark/Axioms/HWV003-0.ax',axiom_1) ).
cnf(axiom_15,axiom,
( X1 = n0
| gt(X1,n0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV003-0.ax',axiom_15) ).
cnf(axiom_19,axiom,
plus(n0,X1) = X1,
file('/export/starexec/sandbox2/benchmark/Axioms/HWV003-0.ax',axiom_19) ).
cnf(quest_3,negated_conjecture,
gt(fifo_length,n0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',quest_3) ).
cnf(axiom_20,axiom,
n1 = plus(n0,n1),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV003-0.ax',axiom_20) ).
cnf(i_0_93,axiom,
( p_Reset(X1)
| p_Rd(X1)
| X2 = wr_level(X1)
| p_Mem(X2,X3,X1)
| ~ p_Wr(X1)
| ~ gt(fifo_length,int_level(X1))
| ~ p_Mem(X2,X3,plus(X1,n1)) ),
axiom_38 ).
cnf(i_0_94,axiom,
level(X1) = int_level(X1),
axiom_21 ).
cnf(i_0_95,axiom,
( p_Reset(X1)
| p_Rd(X1)
| X2 = wr_level(X1)
| p_Mem(X2,X3,plus(X1,n1))
| ~ p_Wr(X1)
| ~ gt(fifo_length,int_level(X1))
| ~ p_Mem(X2,X3,X1) ),
axiom_39 ).
cnf(i_0_96,axiom,
( p_Reset(X1)
| p_Rd(X1)
| gt(fifo_length,int_level(X1))
| p_Mem(X2,X3,X1)
| ~ p_Wr(X1)
| ~ p_Mem(X2,X3,plus(X1,n1)) ),
axiom_45 ).
cnf(i_0_97,axiom,
( p_Reset(X1)
| p_Rd(X1)
| gt(fifo_length,int_level(X1))
| p_Mem(X2,X3,plus(X1,n1))
| ~ p_Wr(X1)
| ~ p_Mem(X2,X3,X1) ),
axiom_46 ).
cnf(i_0_98,axiom,
( p_Reset(X1)
| p_Rd(X1)
| p_Data_in(X2,X1)
| ~ p_Wr(X1)
| ~ gt(fifo_length,int_level(X1))
| ~ p_Mem(wr_level(X1),X2,plus(X1,n1)) ),
axiom_36 ).
cnf(i_0_99,axiom,
( p_Reset(X1)
| p_Data_out(X2,plus(X1,n1))
| ~ p_Wr(X1)
| ~ p_Rd(X1)
| ~ gt(int_level(X1),n0)
| ~ p_Mem(rd_level(X1),X2,X1) ),
axiom_55 ).
cnf(i_0_100,axiom,
( p_Reset(X1)
| p_Wr(X1)
| p_Data_out(X2,plus(X1,n1))
| ~ p_Rd(X1)
| ~ gt(int_level(X1),n0)
| ~ p_Mem(rd_level(X1),X2,X1) ),
axiom_73 ).
cnf(i_0_101,axiom,
( p_Reset(X1)
| p_Mem(rd_level(X1),X2,X1)
| ~ p_Wr(X1)
| ~ p_Rd(X1)
| ~ gt(int_level(X1),n0)
| ~ p_Data_out(X2,plus(X1,n1)) ),
axiom_54 ).
cnf(i_0_102,axiom,
( p_Reset(X1)
| p_Wr(X1)
| p_Mem(rd_level(X1),X2,X1)
| ~ p_Rd(X1)
| ~ gt(int_level(X1),n0)
| ~ p_Data_out(X2,plus(X1,n1)) ),
axiom_72 ).
cnf(i_0_103,axiom,
( p_Reset(X1)
| rd_level(plus(X1,n1)) = plus(rd_level(X1),n1)
| ~ p_Wr(X1)
| ~ p_Rd(X1)
| ~ gt(int_level(X1),n0)
| ~ gt(minus(fifo_length,n1),rd_level(X1)) ),
axiom_56 ).
cnf(i_0_104,axiom,
( p_Reset(X1)
| p_Wr(X1)
| rd_level(plus(X1,n1)) = plus(rd_level(X1),n1)
| ~ p_Rd(X1)
| ~ gt(int_level(X1),n0)
| ~ gt(minus(fifo_length,n1),rd_level(X1)) ),
axiom_74 ).
cnf(i_0_105,axiom,
( p_Reset(X1)
| p_Rd(X1)
| wr_level(plus(X1,n1)) = plus(wr_level(X1),n1)
| ~ p_Wr(X1)
| ~ gt(fifo_length,int_level(X1))
| ~ gt(minus(fifo_length,n1),wr_level(X1)) ),
axiom_40 ).
cnf(i_0_106,axiom,
( p_Reset(X1)
| p_Rd(X1)
| p_Mem(wr_level(X1),X2,plus(X1,n1))
| ~ p_Wr(X1)
| ~ gt(fifo_length,int_level(X1))
| ~ p_Data_in(X2,X1) ),
axiom_37 ).
cnf(i_0_107,axiom,
( p_Reset(X1)
| gt(minus(fifo_length,n1),rd_level(X1))
| rd_level(plus(X1,n1)) = n0
| ~ p_Wr(X1)
| ~ p_Rd(X1)
| ~ gt(int_level(X1),n0) ),
axiom_57 ).
cnf(i_0_108,axiom,
( p_Reset(X1)
| p_Wr(X1)
| gt(minus(fifo_length,n1),rd_level(X1))
| rd_level(plus(X1,n1)) = n0
| ~ p_Rd(X1)
| ~ gt(int_level(X1),n0) ),
axiom_75 ).
cnf(i_0_109,axiom,
( p_Reset(X1)
| p_Rd(X1)
| gt(minus(fifo_length,n1),wr_level(X1))
| wr_level(plus(X1,n1)) = n0
| ~ p_Wr(X1)
| ~ gt(fifo_length,int_level(X1)) ),
axiom_41 ).
cnf(i_0_110,axiom,
( p_Reset(X1)
| gt(int_level(X1),n0)
| p_Data_out(X2,X1)
| ~ p_Wr(X1)
| ~ p_Rd(X1)
| ~ p_Data_out(X2,plus(X1,n1)) ),
axiom_61 ).
cnf(i_0_111,axiom,
( p_Reset(X1)
| p_Wr(X1)
| gt(int_level(X1),n0)
| p_Data_out(X2,X1)
| ~ p_Rd(X1)
| ~ p_Data_out(X2,plus(X1,n1)) ),
axiom_79 ).
cnf(i_0_112,axiom,
( p_Reset(X1)
| gt(int_level(X1),n0)
| p_Data_out(X2,plus(X1,n1))
| ~ p_Wr(X1)
| ~ p_Rd(X1)
| ~ p_Data_out(X2,X1) ),
axiom_62 ).
cnf(i_0_113,axiom,
( p_Reset(X1)
| p_Wr(X1)
| gt(int_level(X1),n0)
| p_Data_out(X2,plus(X1,n1))
| ~ p_Rd(X1)
| ~ p_Data_out(X2,X1) ),
axiom_80 ).
cnf(i_0_114,axiom,
( p_Reset(X1)
| ~ p_Wr(X1)
| ~ p_Rd(X1)
| ~ gt(int_level(X1),n0)
| ~ p_Rd_error(plus(X1,n1)) ),
axiom_52 ).
cnf(i_0_115,axiom,
( p_Reset(X1)
| p_Wr(X1)
| int_level(plus(X1,n1)) = minus(int_level(X1),n1)
| ~ p_Rd(X1)
| ~ gt(int_level(X1),n0) ),
axiom_71 ).
cnf(i_0_116,axiom,
( p_Reset(X1)
| p_Rd(X1)
| int_level(plus(X1,n1)) = plus(int_level(X1),n1)
| ~ p_Wr(X1)
| ~ gt(fifo_length,int_level(X1)) ),
axiom_35 ).
cnf(i_0_117,axiom,
( p_Reset(X1)
| p_Wr(X1)
| ~ p_Rd(X1)
| ~ gt(int_level(X1),n0)
| ~ p_Rd_error(plus(X1,n1)) ),
axiom_70 ).
cnf(i_0_118,axiom,
( p_Reset(X1)
| p_Rd(X1)
| ~ p_Wr(X1)
| ~ gt(fifo_length,int_level(X1))
| ~ p_Wr_error(plus(X1,n1)) ),
axiom_34 ).
cnf(i_0_119,axiom,
( p_Reset(X1)
| gt(int_level(X1),n0)
| int_level(plus(X1,n1)) = plus(int_level(X1),n1)
| ~ p_Wr(X1)
| ~ p_Rd(X1) ),
axiom_59 ).
cnf(i_0_120,axiom,
( p_Reset(X1)
| int_level(plus(X1,n1)) = int_level(X1)
| ~ p_Wr(X1)
| ~ p_Rd(X1)
| ~ gt(int_level(X1),n0) ),
axiom_53 ).
cnf(i_0_121,axiom,
( p_Reset(X1)
| gt(int_level(X1),n0)
| rd_level(plus(X1,n1)) = rd_level(X1)
| ~ p_Wr(X1)
| ~ p_Rd(X1) ),
axiom_60 ).
cnf(i_0_122,axiom,
( p_Reset(X1)
| p_Wr(X1)
| gt(int_level(X1),n0)
| rd_level(plus(X1,n1)) = rd_level(X1)
| ~ p_Rd(X1) ),
axiom_77 ).
cnf(i_0_123,axiom,
( p_Reset(X1)
| p_Wr(X1)
| gt(int_level(X1),n0)
| int_level(plus(X1,n1)) = int_level(X1)
| ~ p_Rd(X1) ),
axiom_78 ).
cnf(i_0_124,axiom,
( p_Reset(X1)
| p_Rd(X1)
| gt(fifo_length,int_level(X1))
| wr_level(plus(X1,n1)) = wr_level(X1)
| ~ p_Wr(X1) ),
axiom_43 ).
cnf(i_0_125,axiom,
( p_Reset(X1)
| p_Rd(X1)
| gt(fifo_length,int_level(X1))
| int_level(plus(X1,n1)) = int_level(X1)
| ~ p_Wr(X1) ),
axiom_44 ).
cnf(i_0_126,axiom,
( p_Reset(X1)
| gt(int_level(X1),n0)
| p_Rd_error(plus(X1,n1))
| ~ p_Wr(X1)
| ~ p_Rd(X1) ),
axiom_58 ).
cnf(i_0_127,axiom,
( p_Reset(X1)
| p_Wr(X1)
| gt(int_level(X1),n0)
| p_Rd_error(plus(X1,n1))
| ~ p_Rd(X1) ),
axiom_76 ).
cnf(i_0_128,axiom,
( p_Reset(X1)
| p_Rd(X1)
| gt(fifo_length,int_level(X1))
| p_Wr_error(plus(X1,n1))
| ~ p_Wr(X1) ),
axiom_42 ).
cnf(i_0_129,axiom,
( p_Reset(X1)
| p_Wr(X1)
| p_Rd(X1)
| int_level(plus(X1,n1)) = int_level(X1) ),
axiom_82 ).
cnf(i_0_130,axiom,
( int_level(plus(X1,n1)) = n0
| ~ p_Reset(X1) ),
axiom_26 ).
cnf(i_0_131,axiom,
( p_Empty(X1)
| int_level(X1) != n0 ),
axiom_24 ).
cnf(i_0_132,axiom,
( p_Full(X1)
| int_level(X1) != fifo_length ),
axiom_22 ).
cnf(i_0_133,axiom,
( int_level(X1) = fifo_length
| ~ p_Full(X1) ),
axiom_23 ).
cnf(i_0_134,axiom,
( int_level(X1) = n0
| ~ p_Empty(X1) ),
axiom_25 ).
cnf(i_0_135,plain,
( X2 = wr_level(X1)
| p_Reset(X1)
| p_Rd(X1)
| p_Mem(X2,X3,X1)
| ~ p_Wr(X1)
| ~ gt(fifo_length,level(X1))
| ~ p_Mem(X2,X3,plus(X1,n1)) ),
inference(rw,[status(thm)],[i_0_93,c_0_94]),
[final] ).
cnf(i_0_136,plain,
( X2 = wr_level(X1)
| p_Reset(X1)
| p_Rd(X1)
| p_Mem(X2,X3,plus(X1,n1))
| ~ p_Wr(X1)
| ~ p_Mem(X2,X3,X1)
| ~ gt(fifo_length,level(X1)) ),
inference(rw,[status(thm)],[i_0_95,c_0_94]),
[final] ).
cnf(i_0_137,plain,
( p_Reset(X1)
| p_Rd(X1)
| p_Mem(X2,X3,X1)
| gt(fifo_length,level(X1))
| ~ p_Wr(X1)
| ~ p_Mem(X2,X3,plus(X1,n1)) ),
inference(rw,[status(thm)],[i_0_96,c_0_94]),
[final] ).
cnf(i_0_138,axiom,
( p_Reset(X1)
| X2 = wr_level(X1)
| p_Mem(X2,X3,X1)
| ~ p_Wr(X1)
| ~ p_Rd(X1)
| ~ p_Mem(X2,X3,plus(X1,n1)) ),
axiom_65,
[final] ).
cnf(i_0_139,plain,
( p_Reset(X1)
| p_Rd(X1)
| gt(fifo_length,level(X1))
| p_Mem(X2,X3,plus(X1,n1))
| ~ p_Wr(X1)
| ~ p_Mem(X2,X3,X1) ),
inference(rw,[status(thm)],[i_0_97,c_0_94]),
[final] ).
cnf(i_0_140,plain,
( p_Reset(X1)
| p_Rd(X1)
| p_Data_in(X2,X1)
| ~ p_Wr(X1)
| ~ gt(fifo_length,level(X1))
| ~ p_Mem(wr_level(X1),X2,plus(X1,n1)) ),
inference(rw,[status(thm)],[i_0_98,c_0_94]),
[final] ).
cnf(i_0_141,axiom,
( p_Reset(X1)
| X2 = wr_level(X1)
| p_Mem(X2,X3,plus(X1,n1))
| ~ p_Wr(X1)
| ~ p_Rd(X1)
| ~ p_Mem(X2,X3,X1) ),
axiom_66,
[final] ).
cnf(i_0_142,axiom,
( p_Reset(X1)
| p_Wr(X1)
| p_Mem(X2,X3,X1)
| ~ p_Mem(X2,X3,plus(X1,n1)) ),
axiom_87,
[final] ).
cnf(i_0_143,plain,
( p_Reset(X1)
| p_Data_out(X2,plus(X1,n1))
| ~ p_Wr(X1)
| ~ p_Rd(X1)
| ~ gt(level(X1),n0)
| ~ p_Mem(rd_level(X1),X2,X1) ),
inference(rw,[status(thm)],[i_0_99,c_0_94]),
[final] ).
cnf(i_0_144,plain,
( p_Reset(X1)
| p_Wr(X1)
| p_Data_out(X2,plus(X1,n1))
| ~ p_Rd(X1)
| ~ gt(level(X1),n0)
| ~ p_Mem(rd_level(X1),X2,X1) ),
inference(rw,[status(thm)],[i_0_100,c_0_94]),
[final] ).
cnf(i_0_145,axiom,
( p_Reset(X1)
| p_Wr(X1)
| p_Mem(X2,X3,plus(X1,n1))
| ~ p_Mem(X2,X3,X1) ),
axiom_88,
[final] ).
cnf(i_0_146,plain,
( p_Reset(X1)
| p_Mem(rd_level(X1),X2,X1)
| ~ p_Wr(X1)
| ~ p_Rd(X1)
| ~ gt(level(X1),n0)
| ~ p_Data_out(X2,plus(X1,n1)) ),
inference(rw,[status(thm)],[i_0_101,c_0_94]),
[final] ).
cnf(i_0_147,plain,
( p_Reset(X1)
| p_Wr(X1)
| p_Mem(rd_level(X1),X2,X1)
| ~ p_Rd(X1)
| ~ gt(level(X1),n0)
| ~ p_Data_out(X2,plus(X1,n1)) ),
inference(rw,[status(thm)],[i_0_102,c_0_94]),
[final] ).
cnf(i_0_148,axiom,
( p_Reset(X1)
| p_Data_in(X2,X1)
| ~ p_Wr(X1)
| ~ p_Rd(X1)
| ~ p_Mem(wr_level(X1),X2,plus(X1,n1)) ),
axiom_63,
[final] ).
cnf(i_0_149,plain,
( rd_level(plus(X1,n1)) = plus(rd_level(X1),n1)
| p_Reset(X1)
| ~ p_Wr(X1)
| ~ p_Rd(X1)
| ~ gt(level(X1),n0)
| ~ gt(minus(fifo_length,n1),rd_level(X1)) ),
inference(rw,[status(thm)],[i_0_103,c_0_94]),
[final] ).
cnf(i_0_150,plain,
( rd_level(plus(X1,n1)) = plus(rd_level(X1),n1)
| p_Reset(X1)
| p_Wr(X1)
| ~ p_Rd(X1)
| ~ gt(level(X1),n0)
| ~ gt(minus(fifo_length,n1),rd_level(X1)) ),
inference(rw,[status(thm)],[i_0_104,c_0_94]),
[final] ).
cnf(i_0_151,plain,
( wr_level(plus(X1,n1)) = plus(wr_level(X1),n1)
| p_Reset(X1)
| p_Rd(X1)
| ~ p_Wr(X1)
| ~ gt(fifo_length,level(X1))
| ~ gt(minus(fifo_length,n1),wr_level(X1)) ),
inference(rw,[status(thm)],[i_0_105,c_0_94]),
[final] ).
cnf(i_0_152,plain,
( p_Reset(X1)
| p_Rd(X1)
| p_Mem(wr_level(X1),X2,plus(X1,n1))
| ~ p_Wr(X1)
| ~ p_Data_in(X2,X1)
| ~ gt(fifo_length,level(X1)) ),
inference(rw,[status(thm)],[i_0_106,c_0_94]),
[final] ).
cnf(i_0_153,axiom,
( ~ p_Reset(X1)
| ~ p_Mem(X2,X3,plus(X1,n1)) ),
axiom_31,
[final] ).
cnf(i_0_154,axiom,
( p_Reset(X1)
| wr_level(plus(X1,n1)) = plus(wr_level(X1),n1)
| ~ p_Wr(X1)
| ~ p_Rd(X1)
| ~ gt(minus(fifo_length,n1),wr_level(X1)) ),
axiom_67,
[final] ).
cnf(i_0_155,negated_conjecture,
gt(plus(wr_level(plus(x_139,n1)),n1),fifo_length),
quest_2,
[final] ).
cnf(i_0_156,axiom,
( p_Reset(X1)
| p_Mem(wr_level(X1),X2,plus(X1,n1))
| ~ p_Wr(X1)
| ~ p_Rd(X1)
| ~ p_Data_in(X2,X1) ),
axiom_64,
[final] ).
cnf(i_0_157,plain,
( rd_level(plus(X1,n1)) = n0
| p_Reset(X1)
| gt(minus(fifo_length,n1),rd_level(X1))
| ~ p_Wr(X1)
| ~ p_Rd(X1)
| ~ gt(level(X1),n0) ),
inference(rw,[status(thm)],[i_0_107,c_0_94]),
[final] ).
cnf(i_0_158,plain,
( rd_level(plus(X1,n1)) = n0
| p_Reset(X1)
| p_Wr(X1)
| gt(minus(fifo_length,n1),rd_level(X1))
| ~ p_Rd(X1)
| ~ gt(level(X1),n0) ),
inference(rw,[status(thm)],[i_0_108,c_0_94]),
[final] ).
cnf(i_0_159,plain,
( wr_level(plus(X1,n1)) = n0
| p_Reset(X1)
| p_Rd(X1)
| gt(minus(fifo_length,n1),wr_level(X1))
| ~ p_Wr(X1)
| ~ gt(fifo_length,level(X1)) ),
inference(rw,[status(thm)],[i_0_109,c_0_94]),
[final] ).
cnf(i_0_160,plain,
( p_Reset(X1)
| p_Data_out(X2,X1)
| gt(level(X1),n0)
| ~ p_Wr(X1)
| ~ p_Rd(X1)
| ~ p_Data_out(X2,plus(X1,n1)) ),
inference(rw,[status(thm)],[i_0_110,c_0_94]),
[final] ).
cnf(i_0_161,axiom,
( gt(X1,X2)
| ~ gt(plus(X1,n1),plus(X2,n1)) ),
axiom_9,
[final] ).
cnf(i_0_162,plain,
( p_Reset(X1)
| p_Wr(X1)
| p_Data_out(X2,X1)
| gt(level(X1),n0)
| ~ p_Rd(X1)
| ~ p_Data_out(X2,plus(X1,n1)) ),
inference(rw,[status(thm)],[i_0_111,c_0_94]),
[final] ).
cnf(i_0_163,plain,
( p_Reset(X1)
| gt(level(X1),n0)
| p_Data_out(X2,plus(X1,n1))
| ~ p_Wr(X1)
| ~ p_Rd(X1)
| ~ p_Data_out(X2,X1) ),
inference(rw,[status(thm)],[i_0_112,c_0_94]),
[final] ).
cnf(i_0_164,plain,
( p_Reset(X1)
| p_Wr(X1)
| gt(level(X1),n0)
| p_Data_out(X2,plus(X1,n1))
| ~ p_Rd(X1)
| ~ p_Data_out(X2,X1) ),
inference(rw,[status(thm)],[i_0_113,c_0_94]),
[final] ).
cnf(i_0_165,plain,
( p_Reset(X1)
| ~ p_Wr(X1)
| ~ p_Rd(X1)
| ~ p_Rd_error(plus(X1,n1))
| ~ gt(level(X1),n0) ),
inference(rw,[status(thm)],[i_0_114,c_0_94]),
[final] ).
cnf(i_0_166,plain,
( level(plus(X1,n1)) = minus(level(X1),n1)
| p_Reset(X1)
| p_Wr(X1)
| ~ p_Rd(X1)
| ~ gt(level(X1),n0) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_115,c_0_94]),c_0_94]),c_0_94]),
[final] ).
cnf(i_0_167,plain,
( level(plus(X1,n1)) = plus(level(X1),n1)
| p_Reset(X1)
| p_Rd(X1)
| ~ p_Wr(X1)
| ~ gt(fifo_length,level(X1)) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_116,c_0_94]),c_0_94]),c_0_94]),
[final] ).
cnf(i_0_168,axiom,
( p_Reset(X1)
| p_Rd(X1)
| p_Data_out(X2,X1)
| ~ p_Wr(X1)
| ~ p_Data_out(X2,plus(X1,n1)) ),
axiom_47,
[final] ).
cnf(i_0_169,plain,
( p_Reset(X1)
| p_Wr(X1)
| ~ p_Rd(X1)
| ~ p_Rd_error(plus(X1,n1))
| ~ gt(level(X1),n0) ),
inference(rw,[status(thm)],[i_0_117,c_0_94]),
[final] ).
cnf(i_0_170,plain,
( p_Reset(X1)
| p_Rd(X1)
| ~ p_Wr(X1)
| ~ p_Wr_error(plus(X1,n1))
| ~ gt(fifo_length,level(X1)) ),
inference(rw,[status(thm)],[i_0_118,c_0_94]),
[final] ).
cnf(i_0_171,axiom,
( p_Reset(X1)
| p_Wr(X1)
| p_Rd(X1)
| p_Data_out(X2,X1)
| ~ p_Data_out(X2,plus(X1,n1)) ),
axiom_83,
[final] ).
cnf(i_0_172,axiom,
( p_Reset(X1)
| gt(minus(fifo_length,n1),wr_level(X1))
| wr_level(plus(X1,n1)) = n0
| ~ p_Wr(X1)
| ~ p_Rd(X1) ),
axiom_68,
[final] ).
cnf(i_0_173,plain,
( level(plus(X1,n1)) = plus(level(X1),n1)
| p_Reset(X1)
| gt(level(X1),n0)
| ~ p_Wr(X1)
| ~ p_Rd(X1) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_119,c_0_94]),c_0_94]),c_0_94]),
[final] ).
cnf(i_0_174,axiom,
( gt(plus(X1,n1),plus(X2,n1))
| ~ gt(X1,X2) ),
axiom_8,
[final] ).
cnf(i_0_175,plain,
( level(plus(X1,n1)) = level(X1)
| p_Reset(X1)
| ~ p_Wr(X1)
| ~ p_Rd(X1)
| ~ gt(level(X1),n0) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_120,c_0_94]),c_0_94]),c_0_94]),
[final] ).
cnf(i_0_176,axiom,
( p_Reset(X1)
| p_Rd(X1)
| p_Data_out(X2,plus(X1,n1))
| ~ p_Wr(X1)
| ~ p_Data_out(X2,X1) ),
axiom_48,
[final] ).
cnf(i_0_177,axiom,
( gt(X1,X2)
| X1 = X2
| ~ gt(plus(X1,n1),X2) ),
axiom_11,
[final] ).
cnf(i_0_178,axiom,
( gt(X1,X2)
| X2 = X1
| ~ gt(plus(X1,n1),X2) ),
axiom_10,
[final] ).
cnf(i_0_179,axiom,
( p_Reset(X1)
| p_Wr(X1)
| p_Rd(X1)
| p_Data_out(X2,plus(X1,n1))
| ~ p_Data_out(X2,X1) ),
axiom_84,
[final] ).
cnf(i_0_180,axiom,
( plus(X2,n1) = X1
| gt(X1,plus(X2,n1))
| ~ gt(X1,X2) ),
axiom_14,
[final] ).
cnf(i_0_181,plain,
( rd_level(plus(X1,n1)) = rd_level(X1)
| p_Reset(X1)
| gt(level(X1),n0)
| ~ p_Wr(X1)
| ~ p_Rd(X1) ),
inference(rw,[status(thm)],[i_0_121,c_0_94]),
[final] ).
cnf(i_0_182,plain,
( rd_level(plus(X1,n1)) = rd_level(X1)
| p_Reset(X1)
| p_Wr(X1)
| gt(level(X1),n0)
| ~ p_Rd(X1) ),
inference(rw,[status(thm)],[i_0_122,c_0_94]),
[final] ).
cnf(i_0_183,plain,
( level(plus(X1,n1)) = level(X1)
| p_Reset(X1)
| p_Wr(X1)
| gt(level(X1),n0)
| ~ p_Rd(X1) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_123,c_0_94]),c_0_94]),c_0_94]),
[final] ).
cnf(i_0_184,plain,
( wr_level(plus(X1,n1)) = wr_level(X1)
| p_Reset(X1)
| p_Rd(X1)
| gt(fifo_length,level(X1))
| ~ p_Wr(X1) ),
inference(rw,[status(thm)],[i_0_124,c_0_94]),
[final] ).
cnf(i_0_185,plain,
( level(plus(X1,n1)) = level(X1)
| p_Reset(X1)
| p_Rd(X1)
| gt(fifo_length,level(X1))
| ~ p_Wr(X1) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_125,c_0_94]),c_0_94]),c_0_94]),
[final] ).
cnf(i_0_186,axiom,
( ~ p_Reset(X1)
| ~ p_Data_out(X2,plus(X1,n1)) ),
axiom_32,
[final] ).
cnf(i_0_187,negated_conjecture,
~ gt(plus(wr_level(x_139),n1),fifo_length),
quest_1,
[final] ).
cnf(i_0_188,plain,
( p_Reset(X1)
| p_Rd_error(plus(X1,n1))
| gt(level(X1),n0)
| ~ p_Wr(X1)
| ~ p_Rd(X1) ),
inference(rw,[status(thm)],[i_0_126,c_0_94]),
[final] ).
cnf(i_0_189,axiom,
( p_Reset(X1)
| p_Rd(X1)
| p_Rd_error(X1)
| ~ p_Wr(X1)
| ~ p_Rd_error(plus(X1,n1)) ),
axiom_49,
[final] ).
cnf(i_0_190,plain,
( p_Reset(X1)
| p_Wr(X1)
| p_Rd_error(plus(X1,n1))
| gt(level(X1),n0)
| ~ p_Rd(X1) ),
inference(rw,[status(thm)],[i_0_127,c_0_94]),
[final] ).
cnf(i_0_191,plain,
( p_Reset(X1)
| p_Rd(X1)
| p_Wr_error(plus(X1,n1))
| gt(fifo_length,level(X1))
| ~ p_Wr(X1) ),
inference(rw,[status(thm)],[i_0_128,c_0_94]),
[final] ).
cnf(i_0_192,axiom,
( p_Reset(X1)
| ~ p_Wr(X1)
| ~ p_Rd(X1)
| ~ p_Wr_error(plus(X1,n1)) ),
axiom_51,
[final] ).
cnf(i_0_193,axiom,
( p_Reset(X1)
| p_Wr(X1)
| p_Rd(X1)
| p_Rd_error(X1)
| ~ p_Rd_error(plus(X1,n1)) ),
axiom_85,
[final] ).
cnf(i_0_194,axiom,
( gt(X1,X3)
| ~ gt(X1,X2)
| ~ gt(X2,X3) ),
axiom_13,
[final] ).
cnf(i_0_195,axiom,
( gt(X1,minus(X1,n1))
| ~ gt(X1,n0) ),
axiom_3,
[final] ).
cnf(i_0_196,axiom,
( p_Reset(X1)
| p_Wr(X1)
| p_Wr_error(X1)
| ~ p_Wr_error(plus(X1,n1)) ),
axiom_89,
[final] ).
cnf(i_0_197,axiom,
( minus(X1,X2) = X3
| def_10(X2,X1)
| plus(X3,X2) != X1 ),
axiom_5,
[final] ).
cnf(i_0_198,axiom,
( plus(X3,X2) = X1
| def_10(X2,X1)
| minus(X1,X2) != X3 ),
axiom_4,
[final] ).
cnf(i_0_199,axiom,
( p_Reset(X1)
| p_Rd(X1)
| p_Rd_error(plus(X1,n1))
| ~ p_Wr(X1)
| ~ p_Rd_error(X1) ),
axiom_50,
[final] ).
cnf(i_0_200,axiom,
( ~ p_Reset(X1)
| ~ p_Rd_error(plus(X1,n1)) ),
axiom_30,
[final] ).
cnf(i_0_201,axiom,
( ~ p_Reset(X1)
| ~ p_Wr_error(plus(X1,n1)) ),
axiom_29,
[final] ).
cnf(i_0_202,axiom,
( p_Reset(X1)
| p_Wr(X1)
| p_Rd(X1)
| p_Rd_error(plus(X1,n1))
| ~ p_Rd_error(X1) ),
axiom_86,
[final] ).
cnf(i_0_203,axiom,
( p_Reset(X1)
| p_Rd(X1)
| rd_level(plus(X1,n1)) = rd_level(X1)
| ~ p_Wr(X1) ),
axiom_33,
[final] ).
cnf(i_0_204,axiom,
( ~ def_10(X1,X2)
| ~ gt(X2,X1) ),
axiom_6,
[final] ).
cnf(i_0_205,axiom,
( p_Reset(X1)
| p_Wr(X1)
| p_Rd(X1)
| rd_level(plus(X1,n1)) = rd_level(X1) ),
axiom_81,
[final] ).
cnf(i_0_206,plain,
( level(plus(X1,n1)) = level(X1)
| p_Reset(X1)
| p_Wr(X1)
| p_Rd(X1) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_129,c_0_94]),c_0_94]),
[final] ).
cnf(i_0_207,axiom,
( p_Reset(X1)
| p_Wr(X1)
| p_Wr_error(plus(X1,n1))
| ~ p_Wr_error(X1) ),
axiom_90,
[final] ).
cnf(i_0_208,axiom,
( X1 = X2
| plus(X1,n1) != plus(X2,n1) ),
axiom_18,
[final] ).
cnf(i_0_209,axiom,
( p_Reset(X1)
| p_Wr(X1)
| wr_level(plus(X1,n1)) = wr_level(X1) ),
axiom_69,
[final] ).
cnf(i_0_210,axiom,
gt(plus(X1,n1),n0),
axiom_2,
[final] ).
cnf(i_0_211,axiom,
( rd_level(plus(X1,n1)) = n0
| ~ p_Reset(X1) ),
axiom_28,
[final] ).
cnf(i_0_212,axiom,
( wr_level(plus(X1,n1)) = n0
| ~ p_Reset(X1) ),
axiom_27,
[final] ).
cnf(i_0_213,plain,
( level(plus(X1,n1)) = n0
| ~ p_Reset(X1) ),
inference(rw,[status(thm)],[i_0_130,c_0_94]),
[final] ).
cnf(i_0_214,axiom,
( gt(X1,X2)
| X2 = X1
| gt(X2,X1) ),
axiom_12,
[final] ).
cnf(i_0_215,axiom,
( ~ def_10(X1,X2)
| X2 != X1 ),
axiom_7,
[final] ).
cnf(i_0_216,axiom,
~ gt(X1,X1),
axiom_17,
[final] ).
cnf(i_0_217,axiom,
( X1 = n0
| X1 = plus(y_27(X1),n1) ),
axiom_16,
[final] ).
cnf(i_0_218,axiom,
plus(X1,n1) != n0,
axiom_1,
[final] ).
cnf(i_0_219,axiom,
( X1 = n0
| gt(X1,n0) ),
axiom_15,
[final] ).
cnf(i_0_220,axiom,
plus(n0,X1) = X1,
axiom_19,
[final] ).
cnf(i_0_221,plain,
( p_Empty(X1)
| level(X1) != n0 ),
inference(rw,[status(thm)],[i_0_131,c_0_94]),
[final] ).
cnf(i_0_222,plain,
( p_Full(X1)
| level(X1) != fifo_length ),
inference(rw,[status(thm)],[i_0_132,c_0_94]),
[final] ).
cnf(i_0_223,plain,
( level(X1) = fifo_length
| ~ p_Full(X1) ),
inference(rw,[status(thm)],[i_0_133,c_0_94]),
[final] ).
cnf(i_0_224,plain,
( level(X1) = n0
| ~ p_Empty(X1) ),
inference(rw,[status(thm)],[i_0_134,c_0_94]),
[final] ).
cnf(i_0_225,negated_conjecture,
gt(fifo_length,n0),
quest_3,
[final] ).
cnf(i_0_226,axiom,
n1 = plus(n0,n1),
axiom_20,
[final] ).
cnf(i_0_227,axiom,
X1 = X1 ).
cnf(i_0_228,axiom,
( X1 = X2
| X2 != X1 ) ).
cnf(i_0_229,axiom,
( X1 = X2
| X1 != X3
| X3 != X2 ) ).
cnf(i_0_230,axiom,
( X1 != X2
| wr_level(X1) = wr_level(X2) ) ).
cnf(i_0_231,axiom,
( X1 != X2
| level(X1) = level(X2) ) ).
cnf(i_0_232,axiom,
( X1 != X2
| plus(X1,X3) = plus(X2,X3) ) ).
cnf(i_0_233,axiom,
( X1 != X2
| plus(X3,X1) = plus(X3,X2) ) ).
cnf(i_0_234,axiom,
( X1 != X2
| rd_level(X1) = rd_level(X2) ) ).
cnf(i_0_235,axiom,
( X1 != X2
| minus(X1,X3) = minus(X2,X3) ) ).
cnf(i_0_236,axiom,
( X1 != X2
| minus(X3,X1) = minus(X3,X2) ) ).
cnf(i_0_237,axiom,
( X1 != X2
| ~ p_Reset(X1)
| p_Reset(X2) ) ).
cnf(i_0_238,axiom,
( X1 != X2
| ~ def_10(X1,X3)
| def_10(X2,X3) ) ).
cnf(i_0_239,axiom,
( X1 != X2
| ~ def_10(X3,X1)
| def_10(X3,X2) ) ).
cnf(i_0_240,axiom,
( X1 != X2
| ~ p_Empty(X1)
| p_Empty(X2) ) ).
cnf(i_0_241,axiom,
( X1 != X2
| ~ p_Full(X1)
| p_Full(X2) ) ).
cnf(i_0_242,axiom,
( X1 != X2
| ~ p_Rd(X1)
| p_Rd(X2) ) ).
cnf(i_0_243,axiom,
( X1 != X2
| ~ p_Mem(X1,X3,X4)
| p_Mem(X2,X3,X4) ) ).
cnf(i_0_244,axiom,
( X1 != X2
| ~ p_Mem(X3,X1,X4)
| p_Mem(X3,X2,X4) ) ).
cnf(i_0_245,axiom,
( X1 != X2
| ~ p_Mem(X3,X4,X1)
| p_Mem(X3,X4,X2) ) ).
cnf(i_0_246,axiom,
( X1 != X2
| ~ p_Wr(X1)
| p_Wr(X2) ) ).
cnf(i_0_247,axiom,
( X1 != X2
| ~ gt(X1,X3)
| gt(X2,X3) ) ).
cnf(i_0_248,axiom,
( X1 != X2
| ~ gt(X3,X1)
| gt(X3,X2) ) ).
cnf(i_0_249,axiom,
( X1 != X2
| ~ p_Data_in(X1,X3)
| p_Data_in(X2,X3) ) ).
cnf(i_0_250,axiom,
( X1 != X2
| ~ p_Data_in(X3,X1)
| p_Data_in(X3,X2) ) ).
cnf(i_0_251,axiom,
( X1 != X2
| ~ p_Data_out(X1,X3)
| p_Data_out(X2,X3) ) ).
cnf(i_0_252,axiom,
( X1 != X2
| ~ p_Data_out(X3,X1)
| p_Data_out(X3,X2) ) ).
cnf(i_0_253,axiom,
( X1 != X2
| ~ p_Rd_error(X1)
| p_Rd_error(X2) ) ).
cnf(i_0_254,axiom,
( X1 != X2
| ~ p_Wr_error(X1)
| p_Wr_error(X2) ) ).
cnf(i_0_1567,plain,
plus(n0,n0) != plus(minus(plus(n0,n1),n1),n1),
inference(scs_inference,[],[i_0_1485,i_0_1503,i_0_1498,i_0_1517,i_0_1049,i_0_607,i_0_1468,i_0_917,i_0_1438,i_0_1444,i_0_1105,i_0_1409,i_0_1470,i_0_815,i_0_520,i_0_337,i_0_916,i_0_1557,i_0_348,i_0_401,i_0_875,i_0_395,i_0_161,i_0_208,i_0_174,i_0_256,i_0_230,i_0_231,i_0_232,i_0_234,i_0_235,i_0_236,i_0_233,i_0_228,i_0_198,i_0_197,i_0_194,i_0_178,i_0_177,i_0_229,i_0_247,i_0_248,i_0_239,i_0_238,i_0_217,i_0_219,i_0_215]) ).
cnf(i_0_1571,plain,
gt(minus(plus(n0,n1),n0),minus(minus(plus(n0,n1),n0),n1)),
inference(scs_inference,[],[i_0_1485,i_0_1503,i_0_1498,i_0_1517,i_0_1049,i_0_607,i_0_1468,i_0_917,i_0_1438,i_0_1444,i_0_1105,i_0_1409,i_0_1470,i_0_815,i_0_520,i_0_337,i_0_916,i_0_1557,i_0_348,i_0_401,i_0_875,i_0_395,i_0_161,i_0_208,i_0_174,i_0_256,i_0_230,i_0_231,i_0_232,i_0_234,i_0_235,i_0_236,i_0_233,i_0_228,i_0_198,i_0_197,i_0_194,i_0_178,i_0_177,i_0_229,i_0_247,i_0_248,i_0_239,i_0_238,i_0_217,i_0_219,i_0_215,i_0_214,i_0_195]) ).
cnf(i_0_1574,plain,
~ gt(plus(plus(n0,n1),n1),plus(plus(n1,minus(X1,X1)),n1)),
inference(scs_inference,[],[i_0_1549,i_0_161]) ).
cnf(i_0_1576,plain,
plus(minus(n1,n0),n1) != plus(minus(plus(n0,n1),n1),n1),
inference(scs_inference,[],[i_0_1494,i_0_1549,i_0_161,i_0_208]) ).
cnf(i_0_1578,plain,
gt(plus(minus(plus(n0,n1),n0),n1),plus(n0,n1)),
inference(scs_inference,[],[i_0_1494,i_0_1549,i_0_1565,i_0_161,i_0_208,i_0_174]) ).
cnf(i_0_1580,plain,
plus(minus(plus(n0,fifo_length),n0),n0) = plus(n0,fifo_length),
inference(scs_inference,[],[i_0_1494,i_0_1549,i_0_1565,i_0_330,i_0_161,i_0_208,i_0_174,i_0_256]) ).
cnf(i_0_1582,plain,
wr_level(minus(plus(n0,minus(X1,X1)),minus(X1,X1))) = wr_level(plus(n0,minus(X2,X2))),
inference(scs_inference,[],[i_0_1494,i_0_1549,i_0_1565,i_0_663,i_0_330,i_0_161,i_0_208,i_0_174,i_0_256,i_0_230]) ).
cnf(i_0_1583,plain,
level(minus(plus(n0,minus(X1,X1)),minus(X1,X1))) = level(plus(n0,minus(X2,X2))),
inference(scs_inference,[],[i_0_1494,i_0_1549,i_0_1565,i_0_663,i_0_330,i_0_161,i_0_208,i_0_174,i_0_256,i_0_230,i_0_231]) ).
cnf(i_0_1584,plain,
plus(minus(plus(n0,minus(X1,X1)),minus(X1,X1)),X2) = plus(plus(n0,minus(X3,X3)),X2),
inference(scs_inference,[],[i_0_1494,i_0_1549,i_0_1565,i_0_663,i_0_330,i_0_161,i_0_208,i_0_174,i_0_256,i_0_230,i_0_231,i_0_232]) ).
cnf(i_0_1585,plain,
rd_level(minus(plus(n0,minus(X1,X1)),minus(X1,X1))) = rd_level(plus(n0,minus(X2,X2))),
inference(scs_inference,[],[i_0_1494,i_0_1549,i_0_1565,i_0_663,i_0_330,i_0_161,i_0_208,i_0_174,i_0_256,i_0_230,i_0_231,i_0_232,i_0_234]) ).
cnf(i_0_1586,plain,
minus(minus(plus(n0,minus(X1,X1)),minus(X1,X1)),X2) = minus(plus(n0,minus(X3,X3)),X2),
inference(scs_inference,[],[i_0_1494,i_0_1549,i_0_1565,i_0_663,i_0_330,i_0_161,i_0_208,i_0_174,i_0_256,i_0_230,i_0_231,i_0_232,i_0_234,i_0_235]) ).
cnf(i_0_1587,plain,
minus(X1,minus(plus(n0,minus(X2,X2)),minus(X2,X2))) = minus(X1,plus(n0,minus(X3,X3))),
inference(scs_inference,[],[i_0_1494,i_0_1549,i_0_1565,i_0_663,i_0_330,i_0_161,i_0_208,i_0_174,i_0_256,i_0_230,i_0_231,i_0_232,i_0_234,i_0_235,i_0_236]) ).
cnf(i_0_1588,plain,
plus(X1,minus(plus(n0,minus(X2,X2)),minus(X2,X2))) = plus(X1,plus(n0,minus(X3,X3))),
inference(scs_inference,[],[i_0_1494,i_0_1549,i_0_1565,i_0_663,i_0_330,i_0_161,i_0_208,i_0_174,i_0_256,i_0_230,i_0_231,i_0_232,i_0_234,i_0_235,i_0_236,i_0_233]) ).
cnf(i_0_1589,plain,
n0 != minus(plus(n0,n1),n0),
inference(scs_inference,[],[i_0_1494,i_0_1549,i_0_1565,i_0_1540,i_0_663,i_0_330,i_0_161,i_0_208,i_0_174,i_0_256,i_0_230,i_0_231,i_0_232,i_0_234,i_0_235,i_0_236,i_0_233,i_0_228]) ).
cnf(i_0_1590,plain,
plus(minus(plus(X1,n1),plus(n0,n0)),minus(plus(n0,X2),X2)) = plus(X1,n1),
inference(scs_inference,[],[i_0_1494,i_0_1549,i_0_1565,i_0_1540,i_0_663,i_0_871,i_0_899,i_0_330,i_0_161,i_0_208,i_0_174,i_0_256,i_0_230,i_0_231,i_0_232,i_0_234,i_0_235,i_0_236,i_0_233,i_0_228,i_0_198]) ).
cnf(i_0_1594,plain,
plus(minus(plus(n0,n1),n1),n0) != n1,
inference(scs_inference,[],[i_0_1494,i_0_1549,i_0_1565,i_0_1540,i_0_663,i_0_871,i_0_899,i_0_330,i_0_323,i_0_161,i_0_208,i_0_174,i_0_256,i_0_230,i_0_231,i_0_232,i_0_234,i_0_235,i_0_236,i_0_233,i_0_228,i_0_198,i_0_197]) ).
cnf(i_0_1596,plain,
~ gt(minus(plus(plus(n0,n0),n1),n1),minus(plus(n0,n1),n0)),
inference(scs_inference,[],[i_0_1494,i_0_1549,i_0_1565,i_0_1540,i_0_663,i_0_871,i_0_899,i_0_330,i_0_1311,i_0_323,i_0_161,i_0_208,i_0_174,i_0_256,i_0_230,i_0_231,i_0_232,i_0_234,i_0_235,i_0_236,i_0_233,i_0_228,i_0_198,i_0_197,i_0_194]) ).
cnf(i_0_1598,plain,
gt(plus(plus(minus(n1,n0),n1),n1),plus(plus(n0,n1),n1)),
inference(scs_inference,[],[i_0_1494,i_0_1549,i_0_1565,i_0_1540,i_0_663,i_0_871,i_0_1432,i_0_1501,i_0_899,i_0_330,i_0_1311,i_0_323,i_0_161,i_0_208,i_0_174,i_0_256,i_0_230,i_0_231,i_0_232,i_0_234,i_0_235,i_0_236,i_0_233,i_0_228,i_0_198,i_0_197,i_0_194,i_0_214]) ).
cnf(i_0_1600,plain,
gt(plus(plus(n1,minus(plus(n0,n0),minus(X1,X1))),minus(X1,X1)),plus(n0,minus(X2,X2))),
inference(scs_inference,[],[i_0_1494,i_0_1549,i_0_1565,i_0_1540,i_0_663,i_0_871,i_0_1432,i_0_1501,i_0_1467,i_0_899,i_0_330,i_0_1311,i_0_323,i_0_511,i_0_161,i_0_208,i_0_174,i_0_256,i_0_230,i_0_231,i_0_232,i_0_234,i_0_235,i_0_236,i_0_233,i_0_228,i_0_198,i_0_197,i_0_194,i_0_214,i_0_177]) ).
cnf(i_0_1605,plain,
gt(plus(y_27(minus(n1,n0)),n1),minus(minus(n1,n0),n1)),
inference(scs_inference,[],[i_0_1494,i_0_1549,i_0_1565,i_0_1540,i_0_663,i_0_1258,i_0_871,i_0_1432,i_0_1501,i_0_1467,i_0_899,i_0_1271,i_0_330,i_0_1311,i_0_323,i_0_511,i_0_161,i_0_208,i_0_174,i_0_256,i_0_230,i_0_231,i_0_232,i_0_234,i_0_235,i_0_236,i_0_233,i_0_228,i_0_198,i_0_197,i_0_194,i_0_214,i_0_177,i_0_229,i_0_247]) ).
cnf(i_0_1606,plain,
~ gt(minus(plus(plus(n0,n0),n1),n1),minus(n1,n0)),
inference(scs_inference,[],[i_0_1494,i_0_1549,i_0_1565,i_0_1540,i_0_663,i_0_1258,i_0_871,i_0_1432,i_0_1501,i_0_1467,i_0_899,i_0_1271,i_0_772,i_0_330,i_0_1311,i_0_323,i_0_511,i_0_161,i_0_208,i_0_174,i_0_256,i_0_230,i_0_231,i_0_232,i_0_234,i_0_235,i_0_236,i_0_233,i_0_228,i_0_198,i_0_197,i_0_194,i_0_214,i_0_177,i_0_229,i_0_247,i_0_248]) ).
cnf(i_0_1608,plain,
~ def_10(minus(plus(n0,X1),X1),minus(n1,n0)),
inference(scs_inference,[],[i_0_1494,i_0_1549,i_0_1565,i_0_1540,i_0_663,i_0_1258,i_0_871,i_0_1432,i_0_1501,i_0_1467,i_0_899,i_0_1591,i_0_1271,i_0_772,i_0_330,i_0_1311,i_0_323,i_0_511,i_0_161,i_0_208,i_0_174,i_0_256,i_0_230,i_0_231,i_0_232,i_0_234,i_0_235,i_0_236,i_0_233,i_0_228,i_0_198,i_0_197,i_0_194,i_0_214,i_0_177,i_0_229,i_0_247,i_0_248,i_0_239]) ).
cnf(i_0_1610,plain,
~ def_10(plus(n0,n0),plus(n1,n0)),
inference(scs_inference,[],[i_0_1494,i_0_1549,i_0_1565,i_0_1540,i_0_663,i_0_1258,i_0_1461,i_0_871,i_0_1432,i_0_1501,i_0_1467,i_0_899,i_0_1591,i_0_1271,i_0_1417,i_0_772,i_0_330,i_0_1311,i_0_323,i_0_511,i_0_161,i_0_208,i_0_174,i_0_256,i_0_230,i_0_231,i_0_232,i_0_234,i_0_235,i_0_236,i_0_233,i_0_228,i_0_198,i_0_197,i_0_194,i_0_214,i_0_177,i_0_229,i_0_247,i_0_248,i_0_239,i_0_238]) ).
cnf(i_0_1617,plain,
~ gt(plus(minus(plus(plus(n0,n0),n1),n1),n1),plus(minus(n1,n0),n1)),
inference(scs_inference,[],[i_0_1606,i_0_161]) ).
cnf(i_0_1619,plain,
plus(plus(n0,plus(n0,n0)),n1) != plus(n1,n1),
inference(scs_inference,[],[i_0_1225,i_0_1606,i_0_161,i_0_208]) ).
cnf(i_0_1621,plain,
gt(plus(plus(wr_level(plus(x_139,n1)),n1),n1),plus(plus(n0,fifo_length),n1)),
inference(scs_inference,[],[i_0_1225,i_0_733,i_0_1606,i_0_161,i_0_208,i_0_174]) ).
cnf(i_0_1623,plain,
plus(minus(plus(n1,n0),plus(n0,n0)),plus(n0,n0)) = plus(n1,n0),
inference(scs_inference,[],[i_0_1610,i_0_1225,i_0_733,i_0_1606,i_0_161,i_0_208,i_0_174,i_0_256]) ).
cnf(i_0_1625,plain,
wr_level(plus(minus(plus(n0,fifo_length),n0),n0)) = wr_level(plus(n0,fifo_length)),
inference(scs_inference,[],[i_0_1610,i_0_1225,i_0_733,i_0_1606,i_0_1580,i_0_161,i_0_208,i_0_174,i_0_256,i_0_230]) ).
cnf(i_0_1626,plain,
level(plus(minus(plus(n0,fifo_length),n0),n0)) = level(plus(n0,fifo_length)),
inference(scs_inference,[],[i_0_1610,i_0_1225,i_0_733,i_0_1606,i_0_1580,i_0_161,i_0_208,i_0_174,i_0_256,i_0_230,i_0_231]) ).
cnf(i_0_1627,plain,
plus(plus(minus(plus(n0,fifo_length),n0),n0),X1) = plus(plus(n0,fifo_length),X1),
inference(scs_inference,[],[i_0_1610,i_0_1225,i_0_733,i_0_1606,i_0_1580,i_0_161,i_0_208,i_0_174,i_0_256,i_0_230,i_0_231,i_0_232]) ).
cnf(i_0_1628,plain,
rd_level(plus(minus(plus(n0,fifo_length),n0),n0)) = rd_level(plus(n0,fifo_length)),
inference(scs_inference,[],[i_0_1610,i_0_1225,i_0_733,i_0_1606,i_0_1580,i_0_161,i_0_208,i_0_174,i_0_256,i_0_230,i_0_231,i_0_232,i_0_234]) ).
cnf(i_0_1629,plain,
minus(plus(minus(plus(n0,fifo_length),n0),n0),X1) = minus(plus(n0,fifo_length),X1),
inference(scs_inference,[],[i_0_1610,i_0_1225,i_0_733,i_0_1606,i_0_1580,i_0_161,i_0_208,i_0_174,i_0_256,i_0_230,i_0_231,i_0_232,i_0_234,i_0_235]) ).
cnf(i_0_1630,plain,
minus(X1,plus(minus(plus(n0,fifo_length),n0),n0)) = minus(X1,plus(n0,fifo_length)),
inference(scs_inference,[],[i_0_1610,i_0_1225,i_0_733,i_0_1606,i_0_1580,i_0_161,i_0_208,i_0_174,i_0_256,i_0_230,i_0_231,i_0_232,i_0_234,i_0_235,i_0_236]) ).
cnf(i_0_1631,plain,
plus(X1,plus(minus(plus(n0,fifo_length),n0),n0)) = plus(X1,plus(n0,fifo_length)),
inference(scs_inference,[],[i_0_1610,i_0_1225,i_0_733,i_0_1606,i_0_1580,i_0_161,i_0_208,i_0_174,i_0_256,i_0_230,i_0_231,i_0_232,i_0_234,i_0_235,i_0_236,i_0_233]) ).
cnf(i_0_1632,plain,
plus(plus(n0,n1),n1) != plus(plus(n0,n0),n1),
inference(scs_inference,[],[i_0_1610,i_0_1225,i_0_1526,i_0_733,i_0_1606,i_0_1580,i_0_161,i_0_208,i_0_174,i_0_256,i_0_230,i_0_231,i_0_232,i_0_234,i_0_235,i_0_236,i_0_233,i_0_228]) ).
cnf(i_0_1633,plain,
minus(n1,plus(n0,n0)) != n0,
inference(scs_inference,[],[i_0_1610,i_0_1225,i_0_1526,i_0_733,i_0_1606,i_0_1580,i_0_654,i_0_161,i_0_208,i_0_174,i_0_256,i_0_230,i_0_231,i_0_232,i_0_234,i_0_235,i_0_236,i_0_233,i_0_228,i_0_198]) ).
cnf(i_0_1635,plain,
plus(plus(n1,minus(plus(n1,n0),plus(n0,n0))),plus(n0,n0)) != plus(n1,n0),
inference(scs_inference,[],[i_0_1610,i_0_1225,i_0_1526,i_0_733,i_0_1606,i_0_1580,i_0_654,i_0_875,i_0_161,i_0_208,i_0_174,i_0_256,i_0_230,i_0_231,i_0_232,i_0_234,i_0_235,i_0_236,i_0_233,i_0_228,i_0_198,i_0_197]) ).
cnf(i_0_1638,plain,
~ gt(minus(plus(n0,plus(n0,X1)),X1),plus(n0,plus(n0,plus(n0,n1)))),
inference(scs_inference,[],[i_0_1610,i_0_1225,i_0_1526,i_0_733,i_0_1606,i_0_1580,i_0_1465,i_0_654,i_0_427,i_0_875,i_0_161,i_0_208,i_0_174,i_0_256,i_0_230,i_0_231,i_0_232,i_0_234,i_0_235,i_0_236,i_0_233,i_0_228,i_0_198,i_0_197,i_0_194]) ).
cnf(i_0_1641,plain,
~ gt(plus(n0,plus(n0,n0)),y_27(plus(y_27(n1),n1))),
inference(scs_inference,[],[i_0_1610,i_0_1225,i_0_1526,i_0_733,i_0_1606,i_0_1580,i_0_1465,i_0_1367,i_0_654,i_0_355,i_0_427,i_0_875,i_0_161,i_0_208,i_0_174,i_0_256,i_0_230,i_0_231,i_0_232,i_0_234,i_0_235,i_0_236,i_0_233,i_0_228,i_0_198,i_0_197,i_0_194,i_0_180]) ).
cnf(i_0_1644,plain,
gt(plus(plus(n0,n1),n1),plus(plus(n0,n0),n1)),
inference(scs_inference,[],[i_0_1610,i_0_1225,i_0_1526,i_0_733,i_0_1606,i_0_1580,i_0_1465,i_0_1367,i_0_654,i_0_355,i_0_427,i_0_685,i_0_875,i_0_161,i_0_208,i_0_174,i_0_256,i_0_230,i_0_231,i_0_232,i_0_234,i_0_235,i_0_236,i_0_233,i_0_228,i_0_198,i_0_197,i_0_194,i_0_180,i_0_214]) ).
cnf(i_0_1647,plain,
~ gt(plus(n0,n1),minus(plus(n0,n1),n0)),
inference(scs_inference,[],[i_0_1610,i_0_1225,i_0_1589,i_0_1526,i_0_733,i_0_1606,i_0_1580,i_0_1465,i_0_1367,i_0_654,i_0_355,i_0_427,i_0_685,i_0_875,i_0_395,i_0_161,i_0_208,i_0_174,i_0_256,i_0_230,i_0_231,i_0_232,i_0_234,i_0_235,i_0_236,i_0_233,i_0_228,i_0_198,i_0_197,i_0_194,i_0_180,i_0_214,i_0_177]) ).
cnf(i_0_1650,plain,
plus(n0,minus(plus(n0,X1),X1)) != n1,
inference(scs_inference,[],[i_0_1610,i_0_1225,i_0_1589,i_0_1526,i_0_733,i_0_1606,i_0_1580,i_0_1465,i_0_817,i_0_1367,i_0_654,i_0_355,i_0_427,i_0_685,i_0_875,i_0_395,i_0_161,i_0_208,i_0_174,i_0_256,i_0_230,i_0_231,i_0_232,i_0_234,i_0_235,i_0_236,i_0_233,i_0_228,i_0_198,i_0_197,i_0_194,i_0_180,i_0_214,i_0_177,i_0_229]) ).
cnf(i_0_1652,plain,
gt(plus(n1,plus(n0,n0)),minus(X1,X1)),
inference(scs_inference,[],[i_0_1610,i_0_1225,i_0_1589,i_0_1526,i_0_733,i_0_1606,i_0_1580,i_0_1509,i_0_1465,i_0_1446,i_0_817,i_0_1367,i_0_654,i_0_355,i_0_427,i_0_685,i_0_875,i_0_395,i_0_161,i_0_208,i_0_174,i_0_256,i_0_230,i_0_231,i_0_232,i_0_234,i_0_235,i_0_236,i_0_233,i_0_228,i_0_198,i_0_197,i_0_194,i_0_180,i_0_214,i_0_177,i_0_229,i_0_247]) ).
cnf(i_0_1655,plain,
gt(plus(wr_level(plus(x_139,n1)),n1),plus(minus(plus(n0,n1),n1),fifo_length)),
inference(scs_inference,[],[i_0_1610,i_0_1225,i_0_1589,i_0_1526,i_0_733,i_0_1606,i_0_1580,i_0_1509,i_0_1465,i_0_1446,i_0_817,i_0_1367,i_0_654,i_0_916,i_0_355,i_0_427,i_0_685,i_0_875,i_0_395,i_0_161,i_0_208,i_0_174,i_0_256,i_0_230,i_0_231,i_0_232,i_0_234,i_0_235,i_0_236,i_0_233,i_0_228,i_0_198,i_0_197,i_0_194,i_0_180,i_0_214,i_0_177,i_0_229,i_0_247,i_0_248]) ).
cnf(i_0_1657,plain,
plus(n0,minus(X1,X1)) != plus(n0,plus(n0,plus(y_27(n1),n1))),
inference(scs_inference,[],[i_0_1610,i_0_1225,i_0_1589,i_0_1526,i_0_733,i_0_1606,i_0_1580,i_0_1509,i_0_1465,i_0_1446,i_0_817,i_0_1367,i_0_849,i_0_654,i_0_916,i_0_355,i_0_399,i_0_427,i_0_685,i_0_875,i_0_395,i_0_161,i_0_208,i_0_174,i_0_256,i_0_230,i_0_231,i_0_232,i_0_234,i_0_235,i_0_236,i_0_233,i_0_228,i_0_198,i_0_197,i_0_194,i_0_180,i_0_214,i_0_177,i_0_229,i_0_247,i_0_248,i_0_239]) ).
cnf(i_0_1659,plain,
def_10(plus(plus(n0,n0),n1),plus(n0,n0)),
inference(scs_inference,[],[i_0_1610,i_0_1225,i_0_1589,i_0_1526,i_0_733,i_0_1606,i_0_1580,i_0_1509,i_0_1465,i_0_868,i_0_1446,i_0_817,i_0_1561,i_0_1367,i_0_849,i_0_654,i_0_916,i_0_355,i_0_399,i_0_427,i_0_685,i_0_875,i_0_395,i_0_161,i_0_208,i_0_174,i_0_256,i_0_230,i_0_231,i_0_232,i_0_234,i_0_235,i_0_236,i_0_233,i_0_228,i_0_198,i_0_197,i_0_194,i_0_180,i_0_214,i_0_177,i_0_229,i_0_247,i_0_248,i_0_239,i_0_238]) ).
cnf(i_0_1661,plain,
minus(n1,plus(n0,n0)) = plus(y_27(minus(n1,plus(n0,n0))),n1),
inference(scs_inference,[],[i_0_1610,i_0_1225,i_0_1589,i_0_1526,i_0_733,i_0_1606,i_0_1580,i_0_1509,i_0_1465,i_0_868,i_0_1446,i_0_817,i_0_1561,i_0_1367,i_0_849,i_0_654,i_0_916,i_0_355,i_0_399,i_0_427,i_0_685,i_0_875,i_0_395,i_0_161,i_0_208,i_0_174,i_0_256,i_0_230,i_0_231,i_0_232,i_0_234,i_0_235,i_0_236,i_0_233,i_0_228,i_0_198,i_0_197,i_0_194,i_0_180,i_0_214,i_0_177,i_0_229,i_0_247,i_0_248,i_0_239,i_0_238,i_0_217]) ).
cnf(i_0_1663,plain,
gt(minus(n1,plus(n0,n0)),n0),
inference(scs_inference,[],[i_0_1610,i_0_1225,i_0_1589,i_0_1526,i_0_733,i_0_1606,i_0_1580,i_0_1509,i_0_1465,i_0_868,i_0_1446,i_0_817,i_0_1561,i_0_1367,i_0_849,i_0_654,i_0_916,i_0_355,i_0_399,i_0_427,i_0_685,i_0_875,i_0_395,i_0_161,i_0_208,i_0_174,i_0_256,i_0_230,i_0_231,i_0_232,i_0_234,i_0_235,i_0_236,i_0_233,i_0_228,i_0_198,i_0_197,i_0_194,i_0_180,i_0_214,i_0_177,i_0_229,i_0_247,i_0_248,i_0_239,i_0_238,i_0_217,i_0_219]) ).
cnf(i_0_1665,plain,
plus(n0,n0) != plus(plus(n0,n0),n1),
inference(scs_inference,[],[i_0_1610,i_0_1225,i_0_1589,i_0_1526,i_0_733,i_0_1606,i_0_1580,i_0_1509,i_0_1465,i_0_868,i_0_1446,i_0_817,i_0_1561,i_0_1367,i_0_849,i_0_654,i_0_916,i_0_355,i_0_399,i_0_427,i_0_685,i_0_875,i_0_395,i_0_161,i_0_208,i_0_174,i_0_256,i_0_230,i_0_231,i_0_232,i_0_234,i_0_235,i_0_236,i_0_233,i_0_228,i_0_198,i_0_197,i_0_194,i_0_180,i_0_214,i_0_177,i_0_229,i_0_247,i_0_248,i_0_239,i_0_238,i_0_217,i_0_219,i_0_215]) ).
cnf(i_0_1669,plain,
gt(minus(n1,plus(n0,n0)),minus(minus(n1,plus(n0,n0)),n1)),
inference(scs_inference,[],[i_0_1610,i_0_1225,i_0_1589,i_0_1526,i_0_733,i_0_1606,i_0_1580,i_0_1509,i_0_1465,i_0_868,i_0_1446,i_0_817,i_0_1561,i_0_1367,i_0_849,i_0_654,i_0_916,i_0_355,i_0_399,i_0_427,i_0_685,i_0_875,i_0_395,i_0_161,i_0_208,i_0_174,i_0_256,i_0_230,i_0_231,i_0_232,i_0_234,i_0_235,i_0_236,i_0_233,i_0_228,i_0_198,i_0_197,i_0_194,i_0_180,i_0_214,i_0_177,i_0_229,i_0_247,i_0_248,i_0_239,i_0_238,i_0_217,i_0_219,i_0_215,i_0_178,i_0_195]) ).
cnf(i_0_1689,plain,
~ def_10(minus(plus(n0,X1),X1),minus(n1,n0)),
inference(rename_variables,[],[i_0_1608]) ).
cnf(i_0_1690,plain,
minus(X1,minus(plus(n0,minus(X2,X2)),minus(X2,X2))) = minus(X1,plus(n0,minus(X3,X3))),
inference(rename_variables,[],[i_0_1587]) ).
cnf(i_0_1903,plain,
plus(minus(plus(X1,n1),plus(n0,n0)),minus(plus(n0,X2),X2)) = plus(X1,n1),
inference(rename_variables,[],[i_0_1590]) ).
cnf(i_0_1672,plain,
~ gt(plus(plus(n0,n1),n1),plus(minus(plus(n0,n1),n0),n1)),
inference(scs_inference,[],[i_0_1647,i_0_161]) ).
cnf(i_0_1674,plain,
plus(plus(n0,n0),n1) != plus(plus(plus(n0,n0),n1),n1),
inference(scs_inference,[],[i_0_1665,i_0_1647,i_0_161,i_0_208]) ).
cnf(i_0_1676,plain,
gt(plus(plus(n1,plus(n0,n0)),n1),plus(minus(X1,X1),n1)),
inference(scs_inference,[],[i_0_1652,i_0_1665,i_0_1647,i_0_161,i_0_208,i_0_174]) ).
cnf(i_0_1678,plain,
plus(minus(minus(n1,n0),minus(plus(n0,X1),X1)),minus(plus(n0,X1),X1)) = minus(n1,n0),
inference(scs_inference,[],[i_0_1652,i_0_1608,i_0_1665,i_0_1647,i_0_161,i_0_208,i_0_174,i_0_256]) ).
cnf(i_0_1680,plain,
wr_level(plus(minus(plus(n1,n0),plus(n0,n0)),plus(n0,n0))) = wr_level(plus(n1,n0)),
inference(scs_inference,[],[i_0_1652,i_0_1608,i_0_1665,i_0_1647,i_0_1623,i_0_161,i_0_208,i_0_174,i_0_256,i_0_230]) ).
cnf(i_0_1681,plain,
level(plus(minus(plus(n1,n0),plus(n0,n0)),plus(n0,n0))) = level(plus(n1,n0)),
inference(scs_inference,[],[i_0_1652,i_0_1608,i_0_1665,i_0_1647,i_0_1623,i_0_161,i_0_208,i_0_174,i_0_256,i_0_230,i_0_231]) ).
cnf(i_0_1682,plain,
plus(plus(minus(plus(n1,n0),plus(n0,n0)),plus(n0,n0)),X1) = plus(plus(n1,n0),X1),
inference(scs_inference,[],[i_0_1652,i_0_1608,i_0_1665,i_0_1647,i_0_1623,i_0_161,i_0_208,i_0_174,i_0_256,i_0_230,i_0_231,i_0_232]) ).
cnf(i_0_1683,plain,
rd_level(plus(minus(plus(n1,n0),plus(n0,n0)),plus(n0,n0))) = rd_level(plus(n1,n0)),
inference(scs_inference,[],[i_0_1652,i_0_1608,i_0_1665,i_0_1647,i_0_1623,i_0_161,i_0_208,i_0_174,i_0_256,i_0_230,i_0_231,i_0_232,i_0_234]) ).
cnf(i_0_1684,plain,
minus(plus(minus(plus(n1,n0),plus(n0,n0)),plus(n0,n0)),X1) = minus(plus(n1,n0),X1),
inference(scs_inference,[],[i_0_1652,i_0_1608,i_0_1665,i_0_1647,i_0_1623,i_0_161,i_0_208,i_0_174,i_0_256,i_0_230,i_0_231,i_0_232,i_0_234,i_0_235]) ).
cnf(i_0_1685,plain,
minus(X1,plus(minus(plus(n1,n0),plus(n0,n0)),plus(n0,n0))) = minus(X1,plus(n1,n0)),
inference(scs_inference,[],[i_0_1652,i_0_1608,i_0_1665,i_0_1647,i_0_1623,i_0_161,i_0_208,i_0_174,i_0_256,i_0_230,i_0_231,i_0_232,i_0_234,i_0_235,i_0_236]) ).
cnf(i_0_1686,plain,
plus(X1,plus(minus(plus(n1,n0),plus(n0,n0)),plus(n0,n0))) = plus(X1,plus(n1,n0)),
inference(scs_inference,[],[i_0_1652,i_0_1608,i_0_1665,i_0_1647,i_0_1623,i_0_161,i_0_208,i_0_174,i_0_256,i_0_230,i_0_231,i_0_232,i_0_234,i_0_235,i_0_236,i_0_233]) ).
cnf(i_0_1687,plain,
n0 != minus(n1,plus(n0,n0)),
inference(scs_inference,[],[i_0_1652,i_0_1608,i_0_1665,i_0_1647,i_0_1633,i_0_1623,i_0_161,i_0_208,i_0_174,i_0_256,i_0_230,i_0_231,i_0_232,i_0_234,i_0_235,i_0_236,i_0_233,i_0_228]) ).
cnf(i_0_1692,plain,
plus(plus(y_27(n1),n1),minus(X1,X1)) != minus(X1,X1),
inference(scs_inference,[],[i_0_1652,i_0_1608,i_0_1665,i_0_1647,i_0_1633,i_0_1623,i_0_1363,i_0_1587,i_0_398,i_0_161,i_0_208,i_0_174,i_0_256,i_0_230,i_0_231,i_0_232,i_0_234,i_0_235,i_0_236,i_0_233,i_0_228,i_0_198,i_0_197]) ).
cnf(i_0_1696,plain,
~ gt(plus(plus(n0,n0),n1),plus(n0,plus(plus(n1,n1),n1))),
inference(scs_inference,[],[i_0_1652,i_0_1608,i_0_1665,i_0_1647,i_0_1633,i_0_1623,i_0_1363,i_0_1644,i_0_1587,i_0_1240,i_0_398,i_0_161,i_0_208,i_0_174,i_0_256,i_0_230,i_0_231,i_0_232,i_0_234,i_0_235,i_0_236,i_0_233,i_0_228,i_0_198,i_0_197,i_0_194]) ).
cnf(i_0_1698,plain,
gt(plus(minus(n1,n0),n1),plus(plus(n0,minus(X1,X1)),n1)),
inference(scs_inference,[],[i_0_1652,i_0_1608,i_0_1665,i_0_1647,i_0_1633,i_0_1623,i_0_1363,i_0_1644,i_0_1506,i_0_1587,i_0_1240,i_0_398,i_0_511,i_0_161,i_0_208,i_0_174,i_0_256,i_0_230,i_0_231,i_0_232,i_0_234,i_0_235,i_0_236,i_0_233,i_0_228,i_0_198,i_0_197,i_0_194,i_0_180]) ).
cnf(i_0_1702,plain,
~ gt(plus(n0,n1),minus(n1,plus(n0,n0))),
inference(scs_inference,[],[i_0_1652,i_0_1608,i_0_1665,i_0_1647,i_0_1633,i_0_1623,i_0_1363,i_0_1644,i_0_1506,i_0_1587,i_0_1240,i_0_398,i_0_511,i_0_395,i_0_161,i_0_208,i_0_174,i_0_256,i_0_230,i_0_231,i_0_232,i_0_234,i_0_235,i_0_236,i_0_233,i_0_228,i_0_198,i_0_197,i_0_194,i_0_180,i_0_178]) ).
cnf(i_0_1705,plain,
~ gt(plus(plus(plus(n0,minus(X1,X1)),n1),n1),plus(minus(n1,n0),n1)),
inference(scs_inference,[],[i_0_1652,i_0_1608,i_0_1665,i_0_1647,i_0_1633,i_0_1623,i_0_1363,i_0_1644,i_0_1506,i_0_1699,i_0_1587,i_0_1240,i_0_398,i_0_634,i_0_511,i_0_395,i_0_161,i_0_208,i_0_174,i_0_256,i_0_230,i_0_231,i_0_232,i_0_234,i_0_235,i_0_236,i_0_233,i_0_228,i_0_198,i_0_197,i_0_194,i_0_180,i_0_178,i_0_177]) ).
cnf(i_0_1708,plain,
plus(minus(plus(n1,n0),plus(n0,n0)),plus(n0,n0)) = plus(y_27(plus(n1,n0)),n1),
inference(scs_inference,[],[i_0_1652,i_0_1608,i_0_1665,i_0_1647,i_0_1633,i_0_1623,i_0_1363,i_0_1644,i_0_1506,i_0_1699,i_0_1587,i_0_850,i_0_1240,i_0_398,i_0_634,i_0_511,i_0_395,i_0_161,i_0_208,i_0_174,i_0_256,i_0_230,i_0_231,i_0_232,i_0_234,i_0_235,i_0_236,i_0_233,i_0_228,i_0_198,i_0_197,i_0_194,i_0_180,i_0_178,i_0_177,i_0_229]) ).
cnf(i_0_1709,plain,
~ gt(plus(minus(plus(n1,n0),plus(n0,n0)),plus(n0,n0)),plus(n0,plus(n1,n0))),
inference(scs_inference,[],[i_0_1652,i_0_1608,i_0_1665,i_0_1647,i_0_1633,i_0_1623,i_0_1363,i_0_1644,i_0_1506,i_0_1699,i_0_1587,i_0_850,i_0_1240,i_0_398,i_0_634,i_0_511,i_0_307,i_0_395,i_0_161,i_0_208,i_0_174,i_0_256,i_0_230,i_0_231,i_0_232,i_0_234,i_0_235,i_0_236,i_0_233,i_0_228,i_0_198,i_0_197,i_0_194,i_0_180,i_0_178,i_0_177,i_0_229,i_0_247]) ).
cnf(i_0_1711,plain,
~ gt(plus(n0,plus(n1,n0)),plus(minus(plus(n1,n0),plus(n0,n0)),plus(n0,n0))),
inference(scs_inference,[],[i_0_1652,i_0_1608,i_0_1665,i_0_1647,i_0_1633,i_0_1623,i_0_1363,i_0_1644,i_0_1506,i_0_1699,i_0_1587,i_0_850,i_0_1240,i_0_398,i_0_634,i_0_511,i_0_307,i_0_309,i_0_395,i_0_161,i_0_208,i_0_174,i_0_256,i_0_230,i_0_231,i_0_232,i_0_234,i_0_235,i_0_236,i_0_233,i_0_228,i_0_198,i_0_197,i_0_194,i_0_180,i_0_178,i_0_177,i_0_229,i_0_247,i_0_248]) ).
cnf(i_0_1713,plain,
~ def_10(minus(plus(n0,X1),X1),minus(n1,plus(n0,minus(X2,X2)))),
inference(scs_inference,[],[i_0_1652,i_0_1608,i_0_1689,i_0_1665,i_0_1647,i_0_1633,i_0_1623,i_0_1363,i_0_1644,i_0_1506,i_0_1699,i_0_1587,i_0_609,i_0_850,i_0_1240,i_0_398,i_0_634,i_0_511,i_0_307,i_0_309,i_0_395,i_0_161,i_0_208,i_0_174,i_0_256,i_0_230,i_0_231,i_0_232,i_0_234,i_0_235,i_0_236,i_0_233,i_0_228,i_0_198,i_0_197,i_0_194,i_0_180,i_0_178,i_0_177,i_0_229,i_0_247,i_0_248,i_0_239]) ).
cnf(i_0_1715,plain,
~ def_10(plus(minus(plus(n1,n0),plus(n0,n0)),plus(n0,n0)),plus(n1,n0)),
inference(scs_inference,[],[i_0_1652,i_0_1608,i_0_1689,i_0_1665,i_0_1647,i_0_1633,i_0_1623,i_0_1363,i_0_1644,i_0_1506,i_0_1699,i_0_1587,i_0_609,i_0_850,i_0_1240,i_0_398,i_0_634,i_0_511,i_0_307,i_0_309,i_0_258,i_0_395,i_0_161,i_0_208,i_0_174,i_0_256,i_0_230,i_0_231,i_0_232,i_0_234,i_0_235,i_0_236,i_0_233,i_0_228,i_0_198,i_0_197,i_0_194,i_0_180,i_0_178,i_0_177,i_0_229,i_0_247,i_0_248,i_0_239,i_0_238]) ).
cnf(i_0_1864,plain,
plus(plus(plus(n0,n1),n1),n1) != plus(plus(plus(n0,n0),n1),n1),
inference(scs_inference,[],[i_0_1632,i_0_1351,i_0_161,i_0_208]) ).
cnf(i_0_1866,plain,
gt(plus(plus(plus(n1,minus(X1,X1)),n1),n1),plus(plus(n0,n1),n1)),
inference(scs_inference,[],[i_0_1632,i_0_1528,i_0_1351,i_0_161,i_0_208,i_0_174]) ).
cnf(i_0_1720,plain,
~ gt(plus(plus(n0,n1),n1),plus(minus(n1,plus(n0,n0)),n1)),
inference(scs_inference,[],[i_0_1702,i_0_161]) ).
cnf(i_0_1722,plain,
plus(n0,n1) != plus(minus(n1,plus(n0,n0)),n1),
inference(scs_inference,[],[i_0_1702,i_0_1687,i_0_161,i_0_208]) ).
cnf(i_0_1724,plain,
gt(plus(plus(plus(minus(n1,n0),minus(X1,X1)),n1),n1),plus(plus(n0,n1),n1)),
inference(scs_inference,[],[i_0_1702,i_0_1687,i_0_1434,i_0_161,i_0_208,i_0_174]) ).
cnf(i_0_1728,plain,
wr_level(minus(plus(plus(n0,n0),n1),n1)) = wr_level(n0),
inference(scs_inference,[],[i_0_1702,i_0_1687,i_0_1715,i_0_1434,i_0_1356,i_0_161,i_0_208,i_0_174,i_0_256,i_0_230]) ).
cnf(i_0_1729,plain,
level(minus(plus(plus(n0,n0),n1),n1)) = level(n0),
inference(scs_inference,[],[i_0_1702,i_0_1687,i_0_1715,i_0_1434,i_0_1356,i_0_161,i_0_208,i_0_174,i_0_256,i_0_230,i_0_231]) ).
cnf(i_0_1730,plain,
plus(minus(plus(plus(n0,n0),n1),n1),X1) = plus(n0,X1),
inference(scs_inference,[],[i_0_1702,i_0_1687,i_0_1715,i_0_1434,i_0_1356,i_0_161,i_0_208,i_0_174,i_0_256,i_0_230,i_0_231,i_0_232]) ).
cnf(i_0_1731,plain,
rd_level(minus(plus(plus(n0,n0),n1),n1)) = rd_level(n0),
inference(scs_inference,[],[i_0_1702,i_0_1687,i_0_1715,i_0_1434,i_0_1356,i_0_161,i_0_208,i_0_174,i_0_256,i_0_230,i_0_231,i_0_232,i_0_234]) ).
cnf(i_0_1732,plain,
minus(minus(plus(plus(n0,n0),n1),n1),X1) = minus(n0,X1),
inference(scs_inference,[],[i_0_1702,i_0_1687,i_0_1715,i_0_1434,i_0_1356,i_0_161,i_0_208,i_0_174,i_0_256,i_0_230,i_0_231,i_0_232,i_0_234,i_0_235]) ).
cnf(i_0_1733,plain,
minus(X1,minus(plus(plus(n0,n0),n1),n1)) = minus(X1,n0),
inference(scs_inference,[],[i_0_1702,i_0_1687,i_0_1715,i_0_1434,i_0_1356,i_0_161,i_0_208,i_0_174,i_0_256,i_0_230,i_0_231,i_0_232,i_0_234,i_0_235,i_0_236]) ).
cnf(i_0_1734,plain,
plus(X1,minus(plus(plus(n0,n0),n1),n1)) = plus(X1,n0),
inference(scs_inference,[],[i_0_1702,i_0_1687,i_0_1715,i_0_1434,i_0_1356,i_0_161,i_0_208,i_0_174,i_0_256,i_0_230,i_0_231,i_0_232,i_0_234,i_0_235,i_0_236,i_0_233]) ).
cnf(i_0_1735,plain,
minus(X1,X1) != plus(plus(y_27(n1),n1),minus(X1,X1)),
inference(scs_inference,[],[i_0_1702,i_0_1687,i_0_1715,i_0_1692,i_0_1434,i_0_1356,i_0_161,i_0_208,i_0_174,i_0_256,i_0_230,i_0_231,i_0_232,i_0_234,i_0_235,i_0_236,i_0_233,i_0_228]) ).
cnf(i_0_1736,plain,
minus(plus(y_27(n1),n1),plus(n0,n0)) != n0,
inference(scs_inference,[],[i_0_1702,i_0_1687,i_0_1715,i_0_1692,i_0_1282,i_0_1434,i_0_1356,i_0_657,i_0_161,i_0_208,i_0_174,i_0_256,i_0_230,i_0_231,i_0_232,i_0_234,i_0_235,i_0_236,i_0_233,i_0_228,i_0_198]) ).
cnf(i_0_1739,plain,
plus(plus(n1,minus(plus(n0,minus(X1,X1)),minus(X2,X2))),minus(X2,X2)) != plus(n0,minus(X1,X1)),
inference(scs_inference,[],[i_0_1702,i_0_1687,i_0_1715,i_0_1692,i_0_1282,i_0_1434,i_0_1356,i_0_487,i_0_657,i_0_875,i_0_161,i_0_208,i_0_174,i_0_256,i_0_230,i_0_231,i_0_232,i_0_234,i_0_235,i_0_236,i_0_233,i_0_228,i_0_198,i_0_197]) ).
cnf(i_0_1742,plain,
~ gt(plus(n0,minus(plus(n1,n0),n1)),plus(n0,plus(n0,plus(n1,n0)))),
inference(scs_inference,[],[i_0_1702,i_0_1687,i_0_1715,i_0_1692,i_0_1282,i_0_1434,i_0_1356,i_0_1051,i_0_487,i_0_657,i_0_401,i_0_875,i_0_161,i_0_208,i_0_174,i_0_256,i_0_230,i_0_231,i_0_232,i_0_234,i_0_235,i_0_236,i_0_233,i_0_228,i_0_198,i_0_197,i_0_194]) ).
cnf(i_0_1745,plain,
plus(n0,plus(n1,n0)) = plus(minus(plus(n1,n0),plus(n0,n0)),plus(n0,n0)),
inference(scs_inference,[],[i_0_1702,i_0_1687,i_0_1715,i_0_1692,i_0_1282,i_0_1434,i_0_1711,i_0_1709,i_0_1356,i_0_1051,i_0_487,i_0_657,i_0_401,i_0_875,i_0_161,i_0_208,i_0_174,i_0_256,i_0_230,i_0_231,i_0_232,i_0_234,i_0_235,i_0_236,i_0_233,i_0_228,i_0_198,i_0_197,i_0_194,i_0_214]) ).
cnf(i_0_1747,plain,
gt(plus(plus(y_27(n1),n1),minus(X1,X1)),minus(X1,X1)),
inference(scs_inference,[],[i_0_1702,i_0_1687,i_0_1715,i_0_1692,i_0_1282,i_0_1434,i_0_1711,i_0_1709,i_0_1356,i_0_1051,i_0_487,i_0_657,i_0_446,i_0_401,i_0_875,i_0_161,i_0_208,i_0_174,i_0_256,i_0_230,i_0_231,i_0_232,i_0_234,i_0_235,i_0_236,i_0_233,i_0_228,i_0_198,i_0_197,i_0_194,i_0_214,i_0_177]) ).
cnf(i_0_1750,plain,
minus(plus(n0,n1),n0) != minus(plus(plus(n0,n0),n1),n1),
inference(scs_inference,[],[i_0_1702,i_0_1687,i_0_1715,i_0_1692,i_0_1282,i_0_1434,i_0_1711,i_0_1709,i_0_1356,i_0_1051,i_0_1540,i_0_487,i_0_657,i_0_446,i_0_401,i_0_875,i_0_161,i_0_208,i_0_174,i_0_256,i_0_230,i_0_231,i_0_232,i_0_234,i_0_235,i_0_236,i_0_233,i_0_228,i_0_198,i_0_197,i_0_194,i_0_214,i_0_177,i_0_229]) ).
cnf(i_0_1751,plain,
gt(minus(plus(y_27(n1),n1),minus(plus(n0,n1),n1)),n0),
inference(scs_inference,[],[i_0_1702,i_0_1687,i_0_1715,i_0_1692,i_0_1282,i_0_1434,i_0_1711,i_0_1709,i_0_1056,i_0_1356,i_0_1051,i_0_919,i_0_1540,i_0_487,i_0_657,i_0_446,i_0_401,i_0_875,i_0_161,i_0_208,i_0_174,i_0_256,i_0_230,i_0_231,i_0_232,i_0_234,i_0_235,i_0_236,i_0_233,i_0_228,i_0_198,i_0_197,i_0_194,i_0_214,i_0_177,i_0_229,i_0_247]) ).
cnf(i_0_1753,plain,
gt(plus(plus(minus(n1,n0),minus(X1,X1)),n1),plus(plus(n0,minus(X2,X2)),n1)),
inference(scs_inference,[],[i_0_1702,i_0_1687,i_0_1715,i_0_1692,i_0_1282,i_0_1434,i_0_1711,i_0_1709,i_0_1056,i_0_1356,i_0_1051,i_0_919,i_0_1540,i_0_487,i_0_1043,i_0_657,i_0_446,i_0_401,i_0_875,i_0_161,i_0_208,i_0_174,i_0_256,i_0_230,i_0_231,i_0_232,i_0_234,i_0_235,i_0_236,i_0_233,i_0_228,i_0_198,i_0_197,i_0_194,i_0_214,i_0_177,i_0_229,i_0_247,i_0_248]) ).
cnf(i_0_1754,plain,
def_10(n1,minus(n0,minus(plus(n0,n1),n1))),
inference(scs_inference,[],[i_0_1702,i_0_1687,i_0_1715,i_0_1692,i_0_1282,i_0_1434,i_0_1711,i_0_1709,i_0_1056,i_0_1356,i_0_1051,i_0_919,i_0_1752,i_0_1540,i_0_487,i_0_1043,i_0_338,i_0_657,i_0_446,i_0_401,i_0_875,i_0_161,i_0_208,i_0_174,i_0_256,i_0_230,i_0_231,i_0_232,i_0_234,i_0_235,i_0_236,i_0_233,i_0_228,i_0_198,i_0_197,i_0_194,i_0_214,i_0_177,i_0_229,i_0_247,i_0_248,i_0_239]) ).
cnf(i_0_1757,plain,
def_10(plus(plus(n0,minus(X1,X1)),n1),plus(n0,n0)),
inference(scs_inference,[],[i_0_1702,i_0_1687,i_0_1715,i_0_1692,i_0_1282,i_0_1434,i_0_1711,i_0_1709,i_0_1056,i_0_1356,i_0_1051,i_0_919,i_0_1752,i_0_754,i_0_1659,i_0_1540,i_0_487,i_0_1043,i_0_338,i_0_657,i_0_446,i_0_401,i_0_875,i_0_161,i_0_208,i_0_174,i_0_256,i_0_230,i_0_231,i_0_232,i_0_234,i_0_235,i_0_236,i_0_233,i_0_228,i_0_198,i_0_197,i_0_194,i_0_214,i_0_177,i_0_229,i_0_247,i_0_248,i_0_239,i_0_238]) ).
cnf(i_0_1759,plain,
gt(minus(plus(y_27(n1),n1),plus(n0,n0)),n0),
inference(scs_inference,[],[i_0_1702,i_0_1687,i_0_1715,i_0_1692,i_0_1282,i_0_1434,i_0_1711,i_0_1709,i_0_1056,i_0_1356,i_0_1051,i_0_919,i_0_1752,i_0_754,i_0_1659,i_0_1540,i_0_487,i_0_1043,i_0_338,i_0_657,i_0_446,i_0_401,i_0_875,i_0_161,i_0_208,i_0_174,i_0_256,i_0_230,i_0_231,i_0_232,i_0_234,i_0_235,i_0_236,i_0_233,i_0_228,i_0_198,i_0_197,i_0_194,i_0_214,i_0_177,i_0_229,i_0_247,i_0_248,i_0_239,i_0_238,i_0_219]) ).
cnf(i_0_1761,plain,
~ gt(minus(n0,minus(plus(n0,n1),n1)),n1),
inference(scs_inference,[],[i_0_1702,i_0_1687,i_0_1715,i_0_1692,i_0_1282,i_0_1434,i_0_1711,i_0_1709,i_0_1056,i_0_1356,i_0_1051,i_0_919,i_0_1752,i_0_754,i_0_1659,i_0_1540,i_0_487,i_0_1043,i_0_338,i_0_657,i_0_446,i_0_401,i_0_875,i_0_161,i_0_208,i_0_174,i_0_256,i_0_230,i_0_231,i_0_232,i_0_234,i_0_235,i_0_236,i_0_233,i_0_228,i_0_198,i_0_197,i_0_194,i_0_214,i_0_177,i_0_229,i_0_247,i_0_248,i_0_239,i_0_238,i_0_219,i_0_204]) ).
cnf(i_0_1763,plain,
minus(n0,minus(plus(n0,n1),n1)) != n1,
inference(scs_inference,[],[i_0_1702,i_0_1687,i_0_1715,i_0_1692,i_0_1282,i_0_1434,i_0_1711,i_0_1709,i_0_1056,i_0_1356,i_0_1051,i_0_919,i_0_1752,i_0_754,i_0_1659,i_0_1540,i_0_487,i_0_1043,i_0_338,i_0_657,i_0_446,i_0_401,i_0_875,i_0_161,i_0_208,i_0_174,i_0_256,i_0_230,i_0_231,i_0_232,i_0_234,i_0_235,i_0_236,i_0_233,i_0_228,i_0_198,i_0_197,i_0_194,i_0_214,i_0_177,i_0_229,i_0_247,i_0_248,i_0_239,i_0_238,i_0_219,i_0_204,i_0_215]) ).
cnf(i_0_1767,plain,
~ gt(plus(minus(plus(plus(n0,n0),n1),n1),n1),minus(plus(n0,n1),n0)),
inference(scs_inference,[],[i_0_1702,i_0_1687,i_0_1715,i_0_1692,i_0_1282,i_0_1434,i_0_1711,i_0_1709,i_0_1056,i_0_1356,i_0_1051,i_0_919,i_0_1752,i_0_1596,i_0_754,i_0_1659,i_0_1540,i_0_487,i_0_1043,i_0_338,i_0_657,i_0_446,i_0_401,i_0_875,i_0_161,i_0_208,i_0_174,i_0_256,i_0_230,i_0_231,i_0_232,i_0_234,i_0_235,i_0_236,i_0_233,i_0_228,i_0_198,i_0_197,i_0_194,i_0_214,i_0_177,i_0_229,i_0_247,i_0_248,i_0_239,i_0_238,i_0_219,i_0_204,i_0_215,i_0_180,i_0_178]) ).
cnf(i_0_1769,plain,
gt(minus(plus(y_27(n1),n1),plus(n0,n0)),minus(minus(plus(y_27(n1),n1),plus(n0,n0)),n1)),
inference(scs_inference,[],[i_0_1702,i_0_1687,i_0_1715,i_0_1692,i_0_1282,i_0_1434,i_0_1711,i_0_1709,i_0_1056,i_0_1356,i_0_1051,i_0_919,i_0_1752,i_0_1596,i_0_754,i_0_1659,i_0_1540,i_0_487,i_0_1043,i_0_338,i_0_657,i_0_446,i_0_401,i_0_875,i_0_161,i_0_208,i_0_174,i_0_256,i_0_230,i_0_231,i_0_232,i_0_234,i_0_235,i_0_236,i_0_233,i_0_228,i_0_198,i_0_197,i_0_194,i_0_214,i_0_177,i_0_229,i_0_247,i_0_248,i_0_239,i_0_238,i_0_219,i_0_204,i_0_215,i_0_180,i_0_178,i_0_195]) ).
cnf(i_0_1850,plain,
~ def_10(minus(plus(n0,X1),X1),minus(n1,plus(n0,minus(X2,X2)))),
inference(rename_variables,[],[i_0_1713]) ).
cnf(i_0_1982,plain,
minus(X1,plus(minus(plus(n1,n0),plus(n0,n0)),plus(n0,n0))) = minus(X1,plus(n1,n0)),
inference(rename_variables,[],[i_0_1685]) ).
cnf(i_0_1776,plain,
gt(plus(plus(plus(y_27(n1),n1),minus(X1,X1)),n1),plus(minus(X1,X1),n1)),
inference(scs_inference,[],[i_0_1344,i_0_1747,i_0_1088,i_0_161,i_0_208,i_0_174]) ).
cnf(i_0_1778,plain,
plus(minus(plus(n0,fifo_length),minus(X1,X1)),minus(X1,X1)) = plus(n0,fifo_length),
inference(scs_inference,[],[i_0_1344,i_0_1747,i_0_1088,i_0_423,i_0_161,i_0_208,i_0_174,i_0_256]) ).
cnf(i_0_1780,plain,
plus(n0,n0) != plus(plus(n0,minus(X1,X1)),n1),
inference(scs_inference,[],[i_0_1344,i_0_1747,i_0_1757,i_0_1088,i_0_423,i_0_161,i_0_208,i_0_174,i_0_256,i_0_215]) ).
cnf(i_0_1782,plain,
wr_level(plus(n0,plus(n1,n0))) = wr_level(plus(minus(plus(n1,n0),plus(n0,n0)),plus(n0,n0))),
inference(scs_inference,[],[i_0_1344,i_0_1747,i_0_1757,i_0_1745,i_0_1088,i_0_423,i_0_161,i_0_208,i_0_174,i_0_256,i_0_215,i_0_230]) ).
cnf(i_0_1783,plain,
level(plus(n0,plus(n1,n0))) = level(plus(minus(plus(n1,n0),plus(n0,n0)),plus(n0,n0))),
inference(scs_inference,[],[i_0_1344,i_0_1747,i_0_1757,i_0_1745,i_0_1088,i_0_423,i_0_161,i_0_208,i_0_174,i_0_256,i_0_215,i_0_230,i_0_231]) ).
cnf(i_0_1784,plain,
plus(plus(n0,plus(n1,n0)),X1) = plus(plus(minus(plus(n1,n0),plus(n0,n0)),plus(n0,n0)),X1),
inference(scs_inference,[],[i_0_1344,i_0_1747,i_0_1757,i_0_1745,i_0_1088,i_0_423,i_0_161,i_0_208,i_0_174,i_0_256,i_0_215,i_0_230,i_0_231,i_0_232]) ).
cnf(i_0_1785,plain,
rd_level(plus(n0,plus(n1,n0))) = rd_level(plus(minus(plus(n1,n0),plus(n0,n0)),plus(n0,n0))),
inference(scs_inference,[],[i_0_1344,i_0_1747,i_0_1757,i_0_1745,i_0_1088,i_0_423,i_0_161,i_0_208,i_0_174,i_0_256,i_0_215,i_0_230,i_0_231,i_0_232,i_0_234]) ).
cnf(i_0_1786,plain,
minus(plus(n0,plus(n1,n0)),X1) = minus(plus(minus(plus(n1,n0),plus(n0,n0)),plus(n0,n0)),X1),
inference(scs_inference,[],[i_0_1344,i_0_1747,i_0_1757,i_0_1745,i_0_1088,i_0_423,i_0_161,i_0_208,i_0_174,i_0_256,i_0_215,i_0_230,i_0_231,i_0_232,i_0_234,i_0_235]) ).
cnf(i_0_1787,plain,
minus(X1,plus(n0,plus(n1,n0))) = minus(X1,plus(minus(plus(n1,n0),plus(n0,n0)),plus(n0,n0))),
inference(scs_inference,[],[i_0_1344,i_0_1747,i_0_1757,i_0_1745,i_0_1088,i_0_423,i_0_161,i_0_208,i_0_174,i_0_256,i_0_215,i_0_230,i_0_231,i_0_232,i_0_234,i_0_235,i_0_236]) ).
cnf(i_0_1788,plain,
plus(X1,plus(n0,plus(n1,n0))) = plus(X1,plus(minus(plus(n1,n0),plus(n0,n0)),plus(n0,n0))),
inference(scs_inference,[],[i_0_1344,i_0_1747,i_0_1757,i_0_1745,i_0_1088,i_0_423,i_0_161,i_0_208,i_0_174,i_0_256,i_0_215,i_0_230,i_0_231,i_0_232,i_0_234,i_0_235,i_0_236,i_0_233]) ).
cnf(i_0_1789,plain,
plus(n0,plus(n0,X1)) != plus(plus(n0,n1),X1),
inference(scs_inference,[],[i_0_1344,i_0_1747,i_0_1295,i_0_1757,i_0_1745,i_0_1088,i_0_423,i_0_161,i_0_208,i_0_174,i_0_256,i_0_215,i_0_230,i_0_231,i_0_232,i_0_234,i_0_235,i_0_236,i_0_233,i_0_228]) ).
cnf(i_0_1790,plain,
minus(n1,plus(n0,plus(n0,n0))) != n0,
inference(scs_inference,[],[i_0_1344,i_0_1747,i_0_1295,i_0_1757,i_0_1745,i_0_1088,i_0_738,i_0_630,i_0_423,i_0_161,i_0_208,i_0_174,i_0_256,i_0_215,i_0_230,i_0_231,i_0_232,i_0_234,i_0_235,i_0_236,i_0_233,i_0_228,i_0_198]) ).
cnf(i_0_1792,plain,
plus(plus(plus(y_27(n1),n1),minus(minus(X1,X1),minus(X1,X1))),minus(X1,X1)) != minus(X1,X1),
inference(scs_inference,[],[i_0_1344,i_0_1747,i_0_1735,i_0_1295,i_0_1757,i_0_1745,i_0_1088,i_0_738,i_0_630,i_0_423,i_0_398,i_0_161,i_0_208,i_0_174,i_0_256,i_0_215,i_0_230,i_0_231,i_0_232,i_0_234,i_0_235,i_0_236,i_0_233,i_0_228,i_0_198,i_0_197]) ).
cnf(i_0_1793,plain,
minus(X1,X1) != plus(plus(y_27(n1),n1),minus(X1,X1)),
inference(rename_variables,[],[i_0_1735]) ).
cnf(i_0_1796,plain,
~ gt(minus(plus(plus(n0,n0),n1),n1),minus(plus(y_27(n1),n1),plus(n0,n0))),
inference(scs_inference,[],[i_0_1344,i_0_1747,i_0_1735,i_0_1295,i_0_1759,i_0_1757,i_0_1745,i_0_1088,i_0_738,i_0_630,i_0_423,i_0_1311,i_0_398,i_0_161,i_0_208,i_0_174,i_0_256,i_0_215,i_0_230,i_0_231,i_0_232,i_0_234,i_0_235,i_0_236,i_0_233,i_0_228,i_0_198,i_0_197,i_0_194]) ).
cnf(i_0_1798,plain,
gt(n1,minus(n0,minus(plus(n0,n1),n1))),
inference(scs_inference,[],[i_0_1344,i_0_1747,i_0_1735,i_0_1295,i_0_1759,i_0_1757,i_0_1745,i_0_1088,i_0_1763,i_0_1761,i_0_738,i_0_630,i_0_423,i_0_1311,i_0_398,i_0_161,i_0_208,i_0_174,i_0_256,i_0_215,i_0_230,i_0_231,i_0_232,i_0_234,i_0_235,i_0_236,i_0_233,i_0_228,i_0_198,i_0_197,i_0_194,i_0_214]) ).
cnf(i_0_1800,plain,
~ gt(plus(n0,n1),minus(n1,minus(X1,X1))),
inference(scs_inference,[],[i_0_1344,i_0_1747,i_0_1735,i_0_1295,i_0_1759,i_0_1757,i_0_1745,i_0_1088,i_0_1763,i_0_1761,i_0_738,i_0_630,i_0_423,i_0_1311,i_0_398,i_0_395,i_0_161,i_0_208,i_0_174,i_0_256,i_0_215,i_0_230,i_0_231,i_0_232,i_0_234,i_0_235,i_0_236,i_0_233,i_0_228,i_0_198,i_0_197,i_0_194,i_0_214,i_0_177]) ).
cnf(i_0_1803,plain,
plus(y_27(n1),n1) != minus(plus(n0,n1),n1),
inference(scs_inference,[],[i_0_923,i_0_1344,i_0_1747,i_0_1735,i_0_1295,i_0_1759,i_0_1757,i_0_1745,i_0_1088,i_0_1763,i_0_1761,i_0_738,i_0_630,i_0_423,i_0_1311,i_0_398,i_0_610,i_0_395,i_0_161,i_0_208,i_0_174,i_0_256,i_0_215,i_0_230,i_0_231,i_0_232,i_0_234,i_0_235,i_0_236,i_0_233,i_0_228,i_0_198,i_0_197,i_0_194,i_0_214,i_0_177,i_0_229]) ).
cnf(i_0_1804,plain,
~ gt(minus(plus(n0,minus(X1,X1)),n0),plus(n0,plus(n0,plus(n0,n0)))),
inference(scs_inference,[],[i_0_923,i_0_1344,i_0_1747,i_0_1735,i_0_1295,i_0_1759,i_0_1757,i_0_1745,i_0_1088,i_0_1763,i_0_1761,i_0_769,i_0_738,i_0_630,i_0_423,i_0_1311,i_0_398,i_0_427,i_0_610,i_0_395,i_0_161,i_0_208,i_0_174,i_0_256,i_0_215,i_0_230,i_0_231,i_0_232,i_0_234,i_0_235,i_0_236,i_0_233,i_0_228,i_0_198,i_0_197,i_0_194,i_0_214,i_0_177,i_0_229,i_0_247]) ).
cnf(i_0_1806,plain,
~ gt(minus(plus(plus(n0,n0),n1),n1),minus(plus(n0,minus(X1,X1)),n0)),
inference(scs_inference,[],[i_0_923,i_0_1344,i_0_1747,i_0_1735,i_0_1295,i_0_1759,i_0_1757,i_0_1745,i_0_1088,i_0_1763,i_0_1761,i_0_769,i_0_738,i_0_630,i_0_423,i_0_1311,i_0_398,i_0_427,i_0_610,i_0_395,i_0_161,i_0_208,i_0_174,i_0_256,i_0_215,i_0_230,i_0_231,i_0_232,i_0_234,i_0_235,i_0_236,i_0_233,i_0_228,i_0_198,i_0_197,i_0_194,i_0_214,i_0_177,i_0_229,i_0_247,i_0_248]) ).
cnf(i_0_1807,plain,
minus(n0,minus(plus(n0,n1),n1)) != plus(n0,plus(n0,n1)),
inference(scs_inference,[],[i_0_923,i_0_1344,i_0_1747,i_0_1735,i_0_1295,i_0_1759,i_0_1757,i_0_1745,i_0_1088,i_0_1763,i_0_1761,i_0_1754,i_0_769,i_0_738,i_0_630,i_0_423,i_0_1311,i_0_398,i_0_399,i_0_427,i_0_610,i_0_395,i_0_161,i_0_208,i_0_174,i_0_256,i_0_215,i_0_230,i_0_231,i_0_232,i_0_234,i_0_235,i_0_236,i_0_233,i_0_228,i_0_198,i_0_197,i_0_194,i_0_214,i_0_177,i_0_229,i_0_247,i_0_248,i_0_239]) ).
cnf(i_0_1809,plain,
~ def_10(minus(plus(n0,minus(X1,X1)),n0),plus(n0,minus(n0,minus(X2,X2)))),
inference(scs_inference,[],[i_0_923,i_0_1344,i_0_1747,i_0_1735,i_0_1295,i_0_1759,i_0_1757,i_0_1745,i_0_1088,i_0_1763,i_0_1761,i_0_1754,i_0_769,i_0_557,i_0_738,i_0_630,i_0_423,i_0_1311,i_0_398,i_0_399,i_0_427,i_0_610,i_0_395,i_0_161,i_0_208,i_0_174,i_0_256,i_0_215,i_0_230,i_0_231,i_0_232,i_0_234,i_0_235,i_0_236,i_0_233,i_0_228,i_0_198,i_0_197,i_0_194,i_0_214,i_0_177,i_0_229,i_0_247,i_0_248,i_0_239,i_0_238]) ).
cnf(i_0_1810,plain,
gt(minus(n1,plus(n0,plus(n0,n0))),n0),
inference(scs_inference,[],[i_0_923,i_0_1344,i_0_1747,i_0_1735,i_0_1295,i_0_1759,i_0_1757,i_0_1745,i_0_1088,i_0_1763,i_0_1761,i_0_1754,i_0_769,i_0_557,i_0_738,i_0_630,i_0_423,i_0_1311,i_0_398,i_0_399,i_0_427,i_0_610,i_0_395,i_0_161,i_0_208,i_0_174,i_0_256,i_0_215,i_0_230,i_0_231,i_0_232,i_0_234,i_0_235,i_0_236,i_0_233,i_0_228,i_0_198,i_0_197,i_0_194,i_0_214,i_0_177,i_0_229,i_0_247,i_0_248,i_0_239,i_0_238,i_0_219]) ).
cnf(i_0_1815,plain,
~ gt(plus(plus(n0,n1),n1),plus(minus(n1,minus(X1,X1)),n1)),
inference(scs_inference,[],[i_0_1800,i_0_161]) ).
cnf(i_0_1817,plain,
plus(n0,n1) != plus(plus(n1,minus(X1,X1)),n1),
inference(scs_inference,[],[i_0_1800,i_0_1539,i_0_161,i_0_208]) ).
cnf(i_0_1819,plain,
gt(plus(plus(minus(plus(n0,n1),n0),n1),n1),plus(plus(n0,n1),n1)),
inference(scs_inference,[],[i_0_1800,i_0_1539,i_0_1578,i_0_161,i_0_208,i_0_174]) ).
cnf(i_0_1821,plain,
plus(minus(minus(X1,X1),n0),n0) = minus(X1,X1),
inference(scs_inference,[],[i_0_1800,i_0_1539,i_0_1578,i_0_293,i_0_161,i_0_208,i_0_174,i_0_256]) ).
cnf(i_0_1823,plain,
wr_level(plus(minus(plus(n0,fifo_length),minus(X1,X1)),minus(X1,X1))) = wr_level(plus(n0,fifo_length)),
inference(scs_inference,[],[i_0_1800,i_0_1539,i_0_1778,i_0_1578,i_0_293,i_0_161,i_0_208,i_0_174,i_0_256,i_0_230]) ).
cnf(i_0_1824,plain,
level(plus(minus(plus(n0,fifo_length),minus(X1,X1)),minus(X1,X1))) = level(plus(n0,fifo_length)),
inference(scs_inference,[],[i_0_1800,i_0_1539,i_0_1778,i_0_1578,i_0_293,i_0_161,i_0_208,i_0_174,i_0_256,i_0_230,i_0_231]) ).
cnf(i_0_1825,plain,
plus(plus(minus(plus(n0,fifo_length),minus(X1,X1)),minus(X1,X1)),X2) = plus(plus(n0,fifo_length),X2),
inference(scs_inference,[],[i_0_1800,i_0_1539,i_0_1778,i_0_1578,i_0_293,i_0_161,i_0_208,i_0_174,i_0_256,i_0_230,i_0_231,i_0_232]) ).
cnf(i_0_1826,plain,
rd_level(plus(minus(plus(n0,fifo_length),minus(X1,X1)),minus(X1,X1))) = rd_level(plus(n0,fifo_length)),
inference(scs_inference,[],[i_0_1800,i_0_1539,i_0_1778,i_0_1578,i_0_293,i_0_161,i_0_208,i_0_174,i_0_256,i_0_230,i_0_231,i_0_232,i_0_234]) ).
cnf(i_0_1827,plain,
minus(plus(minus(plus(n0,fifo_length),minus(X1,X1)),minus(X1,X1)),X2) = minus(plus(n0,fifo_length),X2),
inference(scs_inference,[],[i_0_1800,i_0_1539,i_0_1778,i_0_1578,i_0_293,i_0_161,i_0_208,i_0_174,i_0_256,i_0_230,i_0_231,i_0_232,i_0_234,i_0_235]) ).
cnf(i_0_1828,plain,
minus(X1,plus(minus(plus(n0,fifo_length),minus(X2,X2)),minus(X2,X2))) = minus(X1,plus(n0,fifo_length)),
inference(scs_inference,[],[i_0_1800,i_0_1539,i_0_1778,i_0_1578,i_0_293,i_0_161,i_0_208,i_0_174,i_0_256,i_0_230,i_0_231,i_0_232,i_0_234,i_0_235,i_0_236]) ).
cnf(i_0_1829,plain,
plus(X1,plus(minus(plus(n0,fifo_length),minus(X2,X2)),minus(X2,X2))) = plus(X1,plus(n0,fifo_length)),
inference(scs_inference,[],[i_0_1800,i_0_1539,i_0_1778,i_0_1578,i_0_293,i_0_161,i_0_208,i_0_174,i_0_256,i_0_230,i_0_231,i_0_232,i_0_234,i_0_235,i_0_236,i_0_233]) ).
cnf(i_0_1830,plain,
minus(plus(n0,n1),n1) != plus(y_27(n1),n1),
inference(scs_inference,[],[i_0_1800,i_0_1539,i_0_1778,i_0_1803,i_0_1578,i_0_293,i_0_161,i_0_208,i_0_174,i_0_256,i_0_230,i_0_231,i_0_232,i_0_234,i_0_235,i_0_236,i_0_233,i_0_228]) ).
cnf(i_0_1831,plain,
minus(plus(minus(plus(n0,n1),n1),n1),n0) != n0,
inference(scs_inference,[],[i_0_1800,i_0_1539,i_0_1778,i_0_1803,i_0_1578,i_0_1567,i_0_293,i_0_348,i_0_161,i_0_208,i_0_174,i_0_256,i_0_230,i_0_231,i_0_232,i_0_234,i_0_235,i_0_236,i_0_233,i_0_228,i_0_198]) ).
cnf(i_0_1834,plain,
plus(plus(n1,minus(minus(X1,X1),plus(n0,n0))),plus(n0,n0)) != minus(X1,X1),
inference(scs_inference,[],[i_0_1800,i_0_1539,i_0_1778,i_0_1803,i_0_1578,i_0_1567,i_0_293,i_0_464,i_0_348,i_0_875,i_0_161,i_0_208,i_0_174,i_0_256,i_0_230,i_0_231,i_0_232,i_0_234,i_0_235,i_0_236,i_0_233,i_0_228,i_0_198,i_0_197]) ).
cnf(i_0_1837,plain,
~ gt(plus(n0,n1),plus(n0,plus(minus(plus(n0,n1),n0),n1))),
inference(scs_inference,[],[i_0_1800,i_0_1539,i_0_1778,i_0_1803,i_0_1578,i_0_1567,i_0_293,i_0_464,i_0_348,i_0_307,i_0_875,i_0_161,i_0_208,i_0_174,i_0_256,i_0_230,i_0_231,i_0_232,i_0_234,i_0_235,i_0_236,i_0_233,i_0_228,i_0_198,i_0_197,i_0_194]) ).
cnf(i_0_1840,plain,
plus(minus(plus(n1,n0),plus(n0,n0)),plus(n0,n0)) = plus(n0,plus(n1,n0)),
inference(scs_inference,[],[i_0_1800,i_0_1539,i_0_1778,i_0_1803,i_0_1578,i_0_1567,i_0_1711,i_0_1709,i_0_293,i_0_464,i_0_348,i_0_307,i_0_875,i_0_161,i_0_208,i_0_174,i_0_256,i_0_230,i_0_231,i_0_232,i_0_234,i_0_235,i_0_236,i_0_233,i_0_228,i_0_198,i_0_197,i_0_194,i_0_214]) ).
cnf(i_0_1842,plain,
~ gt(plus(minus(n0,minus(plus(n0,n1),n1)),n1),n1),
inference(scs_inference,[],[i_0_1800,i_0_1539,i_0_1778,i_0_1803,i_0_1578,i_0_1567,i_0_1711,i_0_1709,i_0_1761,i_0_1763,i_0_293,i_0_464,i_0_348,i_0_307,i_0_875,i_0_161,i_0_208,i_0_174,i_0_256,i_0_230,i_0_231,i_0_232,i_0_234,i_0_235,i_0_236,i_0_233,i_0_228,i_0_198,i_0_197,i_0_194,i_0_214,i_0_177]) ).
cnf(i_0_1844,plain,
plus(minus(plus(n0,fifo_length),minus(X1,X1)),minus(X1,X1)) = plus(minus(plus(n0,n1),n1),fifo_length),
inference(scs_inference,[],[i_0_1800,i_0_1539,i_0_1778,i_0_1803,i_0_1578,i_0_1567,i_0_1711,i_0_1709,i_0_1761,i_0_1763,i_0_293,i_0_464,i_0_916,i_0_348,i_0_307,i_0_875,i_0_161,i_0_208,i_0_174,i_0_256,i_0_230,i_0_231,i_0_232,i_0_234,i_0_235,i_0_236,i_0_233,i_0_228,i_0_198,i_0_197,i_0_194,i_0_214,i_0_177,i_0_229]) ).
cnf(i_0_1846,plain,
gt(plus(y_27(plus(n1,n1)),n1),plus(plus(n0,plus(n0,n0)),n1)),
inference(scs_inference,[],[i_0_1800,i_0_1539,i_0_1778,i_0_1803,i_0_1578,i_0_1567,i_0_750,i_0_1711,i_0_1709,i_0_1761,i_0_1763,i_0_293,i_0_464,i_0_916,i_0_689,i_0_348,i_0_307,i_0_875,i_0_161,i_0_208,i_0_174,i_0_256,i_0_230,i_0_231,i_0_232,i_0_234,i_0_235,i_0_236,i_0_233,i_0_228,i_0_198,i_0_197,i_0_194,i_0_214,i_0_177,i_0_229,i_0_247]) ).
cnf(i_0_1848,plain,
gt(plus(minus(plus(n0,n1),n0),n1),plus(plus(n0,minus(X1,X1)),n1)),
inference(scs_inference,[],[i_0_1800,i_0_1539,i_0_1778,i_0_1803,i_0_1578,i_0_1567,i_0_750,i_0_1711,i_0_1709,i_0_1761,i_0_1763,i_0_293,i_0_464,i_0_1043,i_0_916,i_0_689,i_0_348,i_0_307,i_0_875,i_0_161,i_0_208,i_0_174,i_0_256,i_0_230,i_0_231,i_0_232,i_0_234,i_0_235,i_0_236,i_0_233,i_0_228,i_0_198,i_0_197,i_0_194,i_0_214,i_0_177,i_0_229,i_0_247,i_0_248]) ).
cnf(i_0_1849,plain,
~ def_10(minus(plus(n0,X1),X1),minus(n1,plus(n0,n0))),
inference(scs_inference,[],[i_0_1800,i_0_1539,i_0_1778,i_0_1803,i_0_1578,i_0_1567,i_0_750,i_0_757,i_0_1713,i_0_1711,i_0_1709,i_0_1761,i_0_1763,i_0_293,i_0_464,i_0_1043,i_0_916,i_0_689,i_0_348,i_0_307,i_0_875,i_0_161,i_0_208,i_0_174,i_0_256,i_0_230,i_0_231,i_0_232,i_0_234,i_0_235,i_0_236,i_0_233,i_0_228,i_0_198,i_0_197,i_0_194,i_0_214,i_0_177,i_0_229,i_0_247,i_0_248,i_0_239]) ).
cnf(i_0_1852,plain,
def_10(plus(y_27(n1),n1),minus(n0,minus(plus(n0,n1),n1))),
inference(scs_inference,[],[i_0_1800,i_0_1539,i_0_1778,i_0_1803,i_0_1578,i_0_1567,i_0_750,i_0_757,i_0_1713,i_0_1711,i_0_1709,i_0_1761,i_0_1763,i_0_1754,i_0_293,i_0_464,i_0_1043,i_0_916,i_0_689,i_0_348,i_0_307,i_0_610,i_0_875,i_0_161,i_0_208,i_0_174,i_0_256,i_0_230,i_0_231,i_0_232,i_0_234,i_0_235,i_0_236,i_0_233,i_0_228,i_0_198,i_0_197,i_0_194,i_0_214,i_0_177,i_0_229,i_0_247,i_0_248,i_0_239,i_0_238]) ).
cnf(i_0_1853,plain,
gt(minus(plus(minus(plus(n0,n1),n1),n1),n0),n0),
inference(scs_inference,[],[i_0_1800,i_0_1539,i_0_1778,i_0_1803,i_0_1578,i_0_1567,i_0_750,i_0_757,i_0_1713,i_0_1711,i_0_1709,i_0_1761,i_0_1763,i_0_1754,i_0_293,i_0_464,i_0_1043,i_0_916,i_0_689,i_0_348,i_0_307,i_0_610,i_0_875,i_0_161,i_0_208,i_0_174,i_0_256,i_0_230,i_0_231,i_0_232,i_0_234,i_0_235,i_0_236,i_0_233,i_0_228,i_0_198,i_0_197,i_0_194,i_0_214,i_0_177,i_0_229,i_0_247,i_0_248,i_0_239,i_0_238,i_0_219]) ).
cnf(i_0_1855,plain,
~ gt(minus(n0,minus(plus(n0,n1),n1)),plus(y_27(n1),n1)),
inference(scs_inference,[],[i_0_1800,i_0_1539,i_0_1778,i_0_1803,i_0_1578,i_0_1567,i_0_750,i_0_757,i_0_1713,i_0_1711,i_0_1709,i_0_1761,i_0_1763,i_0_1754,i_0_293,i_0_464,i_0_1043,i_0_916,i_0_689,i_0_348,i_0_307,i_0_610,i_0_875,i_0_161,i_0_208,i_0_174,i_0_256,i_0_230,i_0_231,i_0_232,i_0_234,i_0_235,i_0_236,i_0_233,i_0_228,i_0_198,i_0_197,i_0_194,i_0_214,i_0_177,i_0_229,i_0_247,i_0_248,i_0_239,i_0_238,i_0_219,i_0_204]) ).
cnf(i_0_1857,plain,
minus(n0,minus(plus(n0,n1),n1)) != plus(y_27(n1),n1),
inference(scs_inference,[],[i_0_1800,i_0_1539,i_0_1778,i_0_1803,i_0_1578,i_0_1567,i_0_750,i_0_757,i_0_1713,i_0_1711,i_0_1709,i_0_1761,i_0_1763,i_0_1754,i_0_293,i_0_464,i_0_1043,i_0_916,i_0_689,i_0_348,i_0_307,i_0_610,i_0_875,i_0_161,i_0_208,i_0_174,i_0_256,i_0_230,i_0_231,i_0_232,i_0_234,i_0_235,i_0_236,i_0_233,i_0_228,i_0_198,i_0_197,i_0_194,i_0_214,i_0_177,i_0_229,i_0_247,i_0_248,i_0_239,i_0_238,i_0_219,i_0_204,i_0_215]) ).
cnf(i_0_1868,plain,
plus(minus(minus(n1,plus(n0,n0)),minus(plus(n0,X1),X1)),minus(plus(n0,X1),X1)) = minus(n1,plus(n0,n0)),
inference(scs_inference,[],[i_0_1632,i_0_1849,i_0_1528,i_0_1351,i_0_161,i_0_208,i_0_174,i_0_256]) ).
cnf(i_0_1870,plain,
wr_level(plus(minus(minus(X1,X1),n0),n0)) = wr_level(minus(X1,X1)),
inference(scs_inference,[],[i_0_1632,i_0_1849,i_0_1821,i_0_1528,i_0_1351,i_0_161,i_0_208,i_0_174,i_0_256,i_0_230]) ).
cnf(i_0_1871,plain,
level(plus(minus(minus(X1,X1),n0),n0)) = level(minus(X1,X1)),
inference(scs_inference,[],[i_0_1632,i_0_1849,i_0_1821,i_0_1528,i_0_1351,i_0_161,i_0_208,i_0_174,i_0_256,i_0_230,i_0_231]) ).
cnf(i_0_1872,plain,
plus(plus(minus(minus(X1,X1),n0),n0),X2) = plus(minus(X1,X1),X2),
inference(scs_inference,[],[i_0_1632,i_0_1849,i_0_1821,i_0_1528,i_0_1351,i_0_161,i_0_208,i_0_174,i_0_256,i_0_230,i_0_231,i_0_232]) ).
cnf(i_0_1873,plain,
rd_level(plus(minus(minus(X1,X1),n0),n0)) = rd_level(minus(X1,X1)),
inference(scs_inference,[],[i_0_1632,i_0_1849,i_0_1821,i_0_1528,i_0_1351,i_0_161,i_0_208,i_0_174,i_0_256,i_0_230,i_0_231,i_0_232,i_0_234]) ).
cnf(i_0_1874,plain,
minus(plus(minus(minus(X1,X1),n0),n0),X2) = minus(minus(X1,X1),X2),
inference(scs_inference,[],[i_0_1632,i_0_1849,i_0_1821,i_0_1528,i_0_1351,i_0_161,i_0_208,i_0_174,i_0_256,i_0_230,i_0_231,i_0_232,i_0_234,i_0_235]) ).
cnf(i_0_1875,plain,
minus(X1,plus(minus(minus(X2,X2),n0),n0)) = minus(X1,minus(X2,X2)),
inference(scs_inference,[],[i_0_1632,i_0_1849,i_0_1821,i_0_1528,i_0_1351,i_0_161,i_0_208,i_0_174,i_0_256,i_0_230,i_0_231,i_0_232,i_0_234,i_0_235,i_0_236]) ).
cnf(i_0_1876,plain,
plus(X1,plus(minus(minus(X2,X2),n0),n0)) = plus(X1,minus(X2,X2)),
inference(scs_inference,[],[i_0_1632,i_0_1849,i_0_1821,i_0_1528,i_0_1351,i_0_161,i_0_208,i_0_174,i_0_256,i_0_230,i_0_231,i_0_232,i_0_234,i_0_235,i_0_236,i_0_233]) ).
cnf(i_0_1877,plain,
n0 != minus(plus(y_27(n1),n1),plus(n0,n0)),
inference(scs_inference,[],[i_0_1632,i_0_1849,i_0_1736,i_0_1821,i_0_1528,i_0_1351,i_0_161,i_0_208,i_0_174,i_0_256,i_0_230,i_0_231,i_0_232,i_0_234,i_0_235,i_0_236,i_0_233,i_0_228]) ).
cnf(i_0_1878,plain,
plus(minus(minus(n1,plus(n0,n0)),plus(n0,n0)),minus(plus(n0,X1),X1)) = minus(n1,plus(n0,n0)),
inference(scs_inference,[],[i_0_1632,i_0_1849,i_0_1736,i_0_1821,i_0_1528,i_0_1351,i_0_871,i_0_161,i_0_208,i_0_174,i_0_256,i_0_230,i_0_231,i_0_232,i_0_234,i_0_235,i_0_236,i_0_233,i_0_228,i_0_198]) ).
cnf(i_0_1879,plain,
~ def_10(minus(plus(n0,X1),X1),minus(n1,plus(n0,n0))),
inference(rename_variables,[],[i_0_1849]) ).
cnf(i_0_1882,plain,
plus(plus(y_27(n1),n1),n1) != plus(n0,n1),
inference(scs_inference,[],[i_0_1632,i_0_1830,i_0_1849,i_0_1736,i_0_1821,i_0_1528,i_0_1351,i_0_871,i_0_261,i_0_161,i_0_208,i_0_174,i_0_256,i_0_230,i_0_231,i_0_232,i_0_234,i_0_235,i_0_236,i_0_233,i_0_228,i_0_198,i_0_197]) ).
cnf(i_0_1885,plain,
~ gt(minus(plus(plus(n0,n0),n1),n1),minus(n1,plus(n0,plus(n0,n0)))),
inference(scs_inference,[],[i_0_1632,i_0_1830,i_0_1849,i_0_1736,i_0_1821,i_0_1528,i_0_1810,i_0_1351,i_0_871,i_0_1311,i_0_261,i_0_161,i_0_208,i_0_174,i_0_256,i_0_230,i_0_231,i_0_232,i_0_234,i_0_235,i_0_236,i_0_233,i_0_228,i_0_198,i_0_197,i_0_194]) ).
cnf(i_0_1887,plain,
~ gt(plus(n0,n1),minus(plus(y_27(n1),n1),plus(n0,n0))),
inference(scs_inference,[],[i_0_1632,i_0_1830,i_0_1849,i_0_1736,i_0_1821,i_0_1528,i_0_1810,i_0_1351,i_0_871,i_0_1311,i_0_261,i_0_395,i_0_161,i_0_208,i_0_174,i_0_256,i_0_230,i_0_231,i_0_232,i_0_234,i_0_235,i_0_236,i_0_233,i_0_228,i_0_198,i_0_197,i_0_194,i_0_178]) ).
cnf(i_0_1890,plain,
gt(plus(plus(n1,minus(minus(X1,X1),plus(n0,n0))),plus(n0,n0)),minus(X1,X1)),
inference(scs_inference,[],[i_0_1632,i_0_1830,i_0_1849,i_0_1736,i_0_1821,i_0_1528,i_0_1810,i_0_1351,i_0_1834,i_0_871,i_0_1311,i_0_261,i_0_441,i_0_395,i_0_161,i_0_208,i_0_174,i_0_256,i_0_230,i_0_231,i_0_232,i_0_234,i_0_235,i_0_236,i_0_233,i_0_228,i_0_198,i_0_197,i_0_194,i_0_178,i_0_214]) ).
cnf(i_0_1891,plain,
plus(plus(n1,minus(minus(X1,X1),plus(n0,n0))),plus(n0,n0)) != minus(X1,X1),
inference(rename_variables,[],[i_0_1834]) ).
cnf(i_0_1894,plain,
gt(plus(plus(n1,minus(plus(n0,minus(X1,X1)),minus(X2,X2))),minus(X2,X2)),plus(n0,minus(X1,X1))),
inference(scs_inference,[],[i_0_1632,i_0_1830,i_0_1849,i_0_1736,i_0_1821,i_0_1528,i_0_1810,i_0_1351,i_0_1834,i_0_1739,i_0_871,i_0_1311,i_0_511,i_0_261,i_0_441,i_0_395,i_0_161,i_0_208,i_0_174,i_0_256,i_0_230,i_0_231,i_0_232,i_0_234,i_0_235,i_0_236,i_0_233,i_0_228,i_0_198,i_0_197,i_0_194,i_0_178,i_0_214,i_0_177]) ).
cnf(i_0_1898,plain,
plus(minus(minus(X1,X1),n0),n0) = minus(X1,X1),
inference(rename_variables,[],[i_0_1821]) ).
cnf(i_0_1900,plain,
plus(minus(minus(X1,X1),n0),n0) = minus(X1,X1),
inference(rename_variables,[],[i_0_1821]) ).
cnf(i_0_1897,plain,
plus(plus(n1,minus(minus(X1,X1),plus(n0,n0))),plus(n0,n0)) != plus(minus(minus(X1,X1),n0),n0),
inference(scs_inference,[],[i_0_1632,i_0_1830,i_0_1849,i_0_1736,i_0_1821,i_0_1528,i_0_1810,i_0_1351,i_0_1834,i_0_1891,i_0_1739,i_0_871,i_0_1311,i_0_511,i_0_261,i_0_441,i_0_395,i_0_161,i_0_208,i_0_174,i_0_256,i_0_230,i_0_231,i_0_232,i_0_234,i_0_235,i_0_236,i_0_233,i_0_228,i_0_198,i_0_197,i_0_194,i_0_178,i_0_214,i_0_177,i_0_229]) ).
cnf(i_0_1899,plain,
~ gt(plus(minus(minus(X1,X1),n0),n0),X2),
inference(scs_inference,[],[i_0_1632,i_0_1830,i_0_1849,i_0_1736,i_0_1821,i_0_1898,i_0_1528,i_0_1810,i_0_1351,i_0_1834,i_0_1891,i_0_1739,i_0_871,i_0_1311,i_0_511,i_0_261,i_0_441,i_0_1892,i_0_395,i_0_161,i_0_208,i_0_174,i_0_256,i_0_230,i_0_231,i_0_232,i_0_234,i_0_235,i_0_236,i_0_233,i_0_228,i_0_198,i_0_197,i_0_194,i_0_178,i_0_214,i_0_177,i_0_229,i_0_247]) ).
cnf(i_0_1901,plain,
~ gt(minus(plus(n1,n0),n1),plus(minus(plus(n1,n0),plus(n0,n0)),plus(n0,n0))),
inference(scs_inference,[],[i_0_1632,i_0_1830,i_0_1849,i_0_1736,i_0_1821,i_0_1898,i_0_1528,i_0_1840,i_0_1810,i_0_1351,i_0_1834,i_0_1891,i_0_1739,i_0_1034,i_0_871,i_0_1311,i_0_511,i_0_261,i_0_441,i_0_1892,i_0_395,i_0_161,i_0_208,i_0_174,i_0_256,i_0_230,i_0_231,i_0_232,i_0_234,i_0_235,i_0_236,i_0_233,i_0_228,i_0_198,i_0_197,i_0_194,i_0_178,i_0_214,i_0_177,i_0_229,i_0_247,i_0_248]) ).
cnf(i_0_1902,plain,
~ def_10(plus(n0,minus(X1,X1)),plus(minus(plus(X2,n1),plus(n0,n0)),minus(plus(n0,X3),X3))),
inference(scs_inference,[],[i_0_1632,i_0_1830,i_0_1849,i_0_1736,i_0_1821,i_0_1898,i_0_1528,i_0_1840,i_0_1810,i_0_1351,i_0_1834,i_0_1891,i_0_1590,i_0_1739,i_0_1034,i_0_871,i_0_518,i_0_1311,i_0_511,i_0_261,i_0_441,i_0_1892,i_0_395,i_0_161,i_0_208,i_0_174,i_0_256,i_0_230,i_0_231,i_0_232,i_0_234,i_0_235,i_0_236,i_0_233,i_0_228,i_0_198,i_0_197,i_0_194,i_0_178,i_0_214,i_0_177,i_0_229,i_0_247,i_0_248,i_0_239]) ).
cnf(i_0_1904,plain,
~ def_10(level(n0),plus(n0,level(minus(plus(n0,n1),n1)))),
inference(scs_inference,[],[i_0_1632,i_0_1830,i_0_1849,i_0_1736,i_0_1821,i_0_1898,i_0_1528,i_0_1840,i_0_1810,i_0_1351,i_0_915,i_0_1834,i_0_1891,i_0_1590,i_0_1739,i_0_1034,i_0_871,i_0_518,i_0_1311,i_0_511,i_0_261,i_0_1883,i_0_441,i_0_1892,i_0_395,i_0_161,i_0_208,i_0_174,i_0_256,i_0_230,i_0_231,i_0_232,i_0_234,i_0_235,i_0_236,i_0_233,i_0_228,i_0_198,i_0_197,i_0_194,i_0_178,i_0_214,i_0_177,i_0_229,i_0_247,i_0_248,i_0_239,i_0_238]) ).
cnf(i_0_1909,plain,
~ gt(plus(plus(n0,n1),n1),plus(minus(plus(y_27(n1),n1),plus(n0,n0)),n1)),
inference(scs_inference,[],[i_0_1887,i_0_161]) ).
cnf(i_0_1911,plain,
plus(plus(plus(n0,n1),n1),n1) != plus(plus(plus(n1,n1),n1),n1),
inference(scs_inference,[],[i_0_1887,i_0_748,i_0_161,i_0_208]) ).
cnf(i_0_1913,plain,
gt(plus(plus(n1,n1),n1),plus(plus(plus(n0,minus(X1,X1)),n1),n1)),
inference(scs_inference,[],[i_0_1887,i_0_748,i_0_1119,i_0_161,i_0_208,i_0_174]) ).
cnf(i_0_1915,plain,
plus(minus(n1,minus(X1,X1)),minus(X1,X1)) = n1,
inference(scs_inference,[],[i_0_1887,i_0_748,i_0_1119,i_0_361,i_0_161,i_0_208,i_0_174,i_0_256]) ).
cnf(i_0_1917,plain,
wr_level(plus(plus(n0,minus(minus(X1,X1),plus(n0,n0))),plus(n0,n0))) = wr_level(minus(X1,X1)),
inference(scs_inference,[],[i_0_1887,i_0_748,i_0_1119,i_0_660,i_0_361,i_0_161,i_0_208,i_0_174,i_0_256,i_0_230]) ).
cnf(i_0_1918,plain,
level(plus(plus(n0,minus(minus(X1,X1),plus(n0,n0))),plus(n0,n0))) = level(minus(X1,X1)),
inference(scs_inference,[],[i_0_1887,i_0_748,i_0_1119,i_0_660,i_0_361,i_0_161,i_0_208,i_0_174,i_0_256,i_0_230,i_0_231]) ).
cnf(i_0_1919,plain,
plus(plus(plus(n0,minus(minus(X1,X1),plus(n0,n0))),plus(n0,n0)),X2) = plus(minus(X1,X1),X2),
inference(scs_inference,[],[i_0_1887,i_0_748,i_0_1119,i_0_660,i_0_361,i_0_161,i_0_208,i_0_174,i_0_256,i_0_230,i_0_231,i_0_232]) ).
cnf(i_0_1920,plain,
rd_level(plus(plus(n0,minus(minus(X1,X1),plus(n0,n0))),plus(n0,n0))) = rd_level(minus(X1,X1)),
inference(scs_inference,[],[i_0_1887,i_0_748,i_0_1119,i_0_660,i_0_361,i_0_161,i_0_208,i_0_174,i_0_256,i_0_230,i_0_231,i_0_232,i_0_234]) ).
cnf(i_0_1921,plain,
minus(plus(plus(n0,minus(minus(X1,X1),plus(n0,n0))),plus(n0,n0)),X2) = minus(minus(X1,X1),X2),
inference(scs_inference,[],[i_0_1887,i_0_748,i_0_1119,i_0_660,i_0_361,i_0_161,i_0_208,i_0_174,i_0_256,i_0_230,i_0_231,i_0_232,i_0_234,i_0_235]) ).
cnf(i_0_1922,plain,
minus(X1,plus(plus(n0,minus(minus(X2,X2),plus(n0,n0))),plus(n0,n0))) = minus(X1,minus(X2,X2)),
inference(scs_inference,[],[i_0_1887,i_0_748,i_0_1119,i_0_660,i_0_361,i_0_161,i_0_208,i_0_174,i_0_256,i_0_230,i_0_231,i_0_232,i_0_234,i_0_235,i_0_236]) ).
cnf(i_0_1923,plain,
plus(X1,plus(plus(n0,minus(minus(X2,X2),plus(n0,n0))),plus(n0,n0))) = plus(X1,minus(X2,X2)),
inference(scs_inference,[],[i_0_1887,i_0_748,i_0_1119,i_0_660,i_0_361,i_0_161,i_0_208,i_0_174,i_0_256,i_0_230,i_0_231,i_0_232,i_0_234,i_0_235,i_0_236,i_0_233]) ).
cnf(i_0_1924,plain,
plus(n1,n1) != plus(plus(n0,plus(n0,n0)),n1),
inference(scs_inference,[],[i_0_1887,i_0_748,i_0_1619,i_0_1119,i_0_660,i_0_361,i_0_161,i_0_208,i_0_174,i_0_256,i_0_230,i_0_231,i_0_232,i_0_234,i_0_235,i_0_236,i_0_233,i_0_228]) ).
cnf(i_0_1925,plain,
minus(plus(plus(n0,minus(X1,X1)),n1),n0) != n0,
inference(scs_inference,[],[i_0_1887,i_0_748,i_0_1619,i_0_1780,i_0_1119,i_0_660,i_0_361,i_0_348,i_0_161,i_0_208,i_0_174,i_0_256,i_0_230,i_0_231,i_0_232,i_0_234,i_0_235,i_0_236,i_0_233,i_0_228,i_0_198]) ).
cnf(i_0_1928,plain,
plus(plus(n0,plus(y_27(n1),n1)),plus(n0,minus(X1,X1))) != n0,
inference(scs_inference,[],[i_0_1887,i_0_748,i_0_1619,i_0_1780,i_0_1119,i_0_660,i_0_1208,i_0_361,i_0_508,i_0_348,i_0_161,i_0_208,i_0_174,i_0_256,i_0_230,i_0_231,i_0_232,i_0_234,i_0_235,i_0_236,i_0_233,i_0_228,i_0_198,i_0_197]) ).
cnf(i_0_1931,plain,
gt(plus(plus(plus(n0,n0),n1),n1),plus(plus(n0,n0),n1)),
inference(scs_inference,[],[i_0_1887,i_0_748,i_0_1619,i_0_1780,i_0_1119,i_0_660,i_0_1674,i_0_1208,i_0_361,i_0_508,i_0_655,i_0_348,i_0_161,i_0_208,i_0_174,i_0_256,i_0_230,i_0_231,i_0_232,i_0_234,i_0_235,i_0_236,i_0_233,i_0_228,i_0_198,i_0_197,i_0_180]) ).
cnf(i_0_1934,plain,
~ gt(plus(plus(n0,minus(X1,X1)),n1),plus(n0,plus(n0,plus(n1,n1)))),
inference(scs_inference,[],[i_0_1887,i_0_748,i_0_1619,i_0_1780,i_0_1119,i_0_660,i_0_1674,i_0_1208,i_0_361,i_0_508,i_0_655,i_0_348,i_0_401,i_0_161,i_0_208,i_0_174,i_0_256,i_0_230,i_0_231,i_0_232,i_0_234,i_0_235,i_0_236,i_0_233,i_0_228,i_0_198,i_0_197,i_0_180,i_0_194]) ).
cnf(i_0_2255,plain,
plus(plus(minus(minus(X1,X1),n0),n0),X2) = plus(minus(X1,X1),X2),
inference(rename_variables,[],[i_0_1872]) ).
cnf(i_0_1937,plain,
plus(n0,n0) = plus(minus(minus(X1,X1),n0),n0),
inference(scs_inference,[],[i_0_1887,i_0_748,i_0_1619,i_0_1780,i_0_1899,i_0_1119,i_0_660,i_0_1674,i_0_1208,i_0_361,i_0_508,i_0_655,i_0_1932,i_0_348,i_0_401,i_0_161,i_0_208,i_0_174,i_0_256,i_0_230,i_0_231,i_0_232,i_0_234,i_0_235,i_0_236,i_0_233,i_0_228,i_0_198,i_0_197,i_0_180,i_0_194,i_0_178]) ).
cnf(i_0_1938,plain,
~ gt(plus(minus(minus(X1,X1),n0),n0),X2),
inference(rename_variables,[],[i_0_1899]) ).
cnf(c_0_1969,plain,
plus(n0,n0) = plus(minus(minus(X1,X1),n0),n0),
i_0_1937 ).
cnf(c_0_1970,axiom,
plus(n0,X1) = X1,
i_0_220 ).
cnf(c_0_1971,plain,
~ gt(plus(minus(minus(X1,X1),n0),n0),X2),
i_0_1899 ).
cnf(c_0_1972,plain,
plus(minus(minus(X1,X1),n0),n0) = n0,
inference(rw,[status(thm)],[c_0_1969,c_0_1970]) ).
cnf(c_0_1973,axiom,
( gt(X1,X2)
| ~ gt(plus(X1,n1),plus(X2,n1)) ),
i_0_161 ).
cnf(c_0_1974,plain,
~ gt(n0,X1),
inference(rw,[status(thm)],[c_0_1971,c_0_1972]) ).
cnf(c_0_1975,plain,
~ gt(n1,plus(X1,n1)),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1973,c_0_1970]),c_0_1974]) ).
cnf(c_0_1976,axiom,
( X1 = n0
| X1 = plus(y_27(X1),n1) ),
i_0_217 ).
cnf(c_0_1977,plain,
( X1 = n0
| ~ gt(n1,X1) ),
inference(spm,[status(thm)],[c_0_1975,c_0_1976]) ).
cnf(c_0_1978,axiom,
( gt(X1,X2)
| X2 = X1
| gt(X2,X1) ),
i_0_214 ).
cnf(c_0_1979,plain,
( X1 = n0
| gt(X2,y_27(X1))
| ~ gt(plus(X2,n1),X1) ),
inference(spm,[status(thm)],[c_0_1973,c_0_1976]) ).
cnf(c_0_1980,axiom,
( gt(X1,X2)
| ~ gt(X1,X3)
| ~ gt(X3,X2) ),
i_0_194 ).
cnf(c_0_1981,plain,
( n1 = X1
| X1 = n0
| gt(X1,n1) ),
inference(spm,[status(thm)],[c_0_1977,c_0_1978]) ).
cnf(c_0_1982,negated_conjecture,
~ gt(plus(wr_level(x_139),n1),fifo_length),
i_0_187 ).
cnf(c_0_1983,plain,
( X1 = n0
| gt(y_27(X1),X2)
| ~ gt(X1,plus(X2,n1)) ),
inference(spm,[status(thm)],[c_0_1973,c_0_1976]) ).
cnf(c_0_1984,plain,
( y_27(X1) = n0
| X1 = n0
| ~ gt(plus(n1,n1),X1) ),
inference(spm,[status(thm)],[c_0_1977,c_0_1979]) ).
cnf(c_0_1985,plain,
( gt(X1,n0)
| ~ gt(plus(X1,n1),n1) ),
inference(spm,[status(thm)],[c_0_1973,c_0_1970]) ).
cnf(c_0_1986,plain,
gt(plus(plus(wr_level(plus(x_139,n1)),n1),n1),plus(plus(n0,fifo_length),n1)),
i_0_1621 ).
cnf(c_0_1987,axiom,
( gt(plus(X1,n1),plus(X2,n1))
| ~ gt(X1,X2) ),
i_0_174 ).
cnf(c_0_1988,plain,
( X1 = n0
| n1 = X1
| gt(X2,n1)
| ~ gt(X2,X1) ),
inference(spm,[status(thm)],[c_0_1980,c_0_1981]) ).
cnf(c_0_1989,negated_conjecture,
( plus(wr_level(x_139),n1) = fifo_length
| gt(fifo_length,plus(wr_level(x_139),n1)) ),
inference(spm,[status(thm)],[c_0_1982,c_0_1978]) ).
cnf(c_0_1990,axiom,
plus(X1,n1) != n0,
i_0_218 ).
cnf(c_0_1991,plain,
( X1 = n0
| ~ gt(plus(n1,n1),X1)
| ~ gt(X1,plus(X2,n1)) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1983,c_0_1984]),c_0_1974]) ).
cnf(c_0_1992,plain,
( X1 = n0
| gt(y_27(X1),n0)
| ~ gt(X1,n1) ),
inference(spm,[status(thm)],[c_0_1985,c_0_1976]) ).
cnf(c_0_1993,plain,
gt(plus(plus(wr_level(plus(x_139,n1)),n1),n1),plus(fifo_length,n1)),
inference(rw,[status(thm)],[c_0_1986,c_0_1970]) ).
cnf(c_0_1994,axiom,
( wr_level(plus(X1,n1)) = n0
| ~ p_Reset(X1) ),
i_0_212 ).
cnf(c_0_1995,plain,
( gt(plus(X1,n1),n1)
| ~ gt(X1,n0) ),
inference(spm,[status(thm)],[c_0_1987,c_0_1970]) ).
cnf(c_0_1996,negated_conjecture,
( plus(wr_level(x_139),n1) = fifo_length
| plus(wr_level(x_139),n1) = n1
| gt(fifo_length,n1) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1988,c_0_1989]),c_0_1990]) ).
cnf(c_0_1997,plain,
( plus(X1,n1) = n1
| gt(X1,n0) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1985,c_0_1978]),c_0_1975]) ).
cnf(c_0_1998,plain,
( ~ gt(plus(X1,n1),plus(X2,n1))
| ~ gt(n1,X1) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1991,c_0_1987]),c_0_1990]) ).
cnf(c_0_1999,plain,
gt(n1,minus(n0,minus(plus(n0,n1),n1))),
i_0_1798 ).
cnf(c_0_2000,plain,
plus(minus(minus(X1,X1),n0),n0) = minus(X1,X1),
i_0_1821 ).
cnf(c_0_2001,plain,
( X1 = n0
| ~ gt(plus(n1,n1),X1)
| ~ gt(X1,n1) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1992,c_0_1984]),c_0_1974]) ).
cnf(c_0_2002,plain,
( gt(plus(n1,n1),plus(fifo_length,n1))
| ~ p_Reset(x_139) ),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_1993,c_0_1994]),c_0_1970]) ).
cnf(c_0_2003,axiom,
( plus(X1,X2) = X3
| def_10(X2,X3)
| minus(X3,X2) != X1 ),
i_0_198 ).
cnf(c_0_2004,negated_conjecture,
( plus(wr_level(x_139),n1) = n1
| gt(fifo_length,n1) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_1995,c_0_1996]),c_0_1997]) ).
cnf(c_0_2005,axiom,
( gt(X1,X2)
| X1 = X2
| ~ gt(plus(X1,n1),X2) ),
i_0_177 ).
cnf(c_0_2006,axiom,
( gt(X1,minus(X1,n1))
| ~ gt(X1,n0) ),
i_0_195 ).
cnf(c_0_2007,axiom,
gt(plus(X1,n1),n0),
i_0_210 ).
cnf(c_0_2008,plain,
( X1 = n0
| ~ gt(X1,plus(X2,n1))
| ~ gt(n1,y_27(X1)) ),
inference(spm,[status(thm)],[c_0_1998,c_0_1976]) ).
cnf(c_0_2009,plain,
( X1 = n0
| gt(X1,plus(X2,n1))
| ~ gt(y_27(X1),X2) ),
inference(spm,[status(thm)],[c_0_1987,c_0_1976]) ).
cnf(c_0_2010,axiom,
( X1 = n0
| gt(X1,n0) ),
i_0_219 ).
cnf(c_0_2011,plain,
gt(n1,minus(n0,minus(n1,n1))),
inference(rw,[status(thm)],[c_0_1999,c_0_1970]) ).
cnf(c_0_2012,plain,
minus(X1,X1) = n0,
inference(rw,[status(thm)],[c_0_2000,c_0_1972]) ).
cnf(c_0_2013,axiom,
( p_Reset(X1)
| gt(minus(fifo_length,n1),wr_level(X1))
| wr_level(plus(X1,n1)) = n0
| ~ p_Wr(X1)
| ~ p_Rd(X1) ),
i_0_172 ).
cnf(c_0_2014,negated_conjecture,
gt(plus(wr_level(plus(x_139,n1)),n1),fifo_length),
i_0_155 ).
cnf(c_0_2015,axiom,
( p_Reset(X1)
| p_Wr(X1)
| wr_level(plus(X1,n1)) = wr_level(X1) ),
i_0_209 ).
cnf(c_0_2016,plain,
( ~ gt(plus(fifo_length,n1),n1)
| ~ p_Reset(x_139) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_2001,c_0_2002]),c_0_1990]) ).
cnf(c_0_2017,negated_conjecture,
gt(fifo_length,n0),
i_0_225 ).
cnf(c_0_2018,axiom,
( ~ def_10(X1,X2)
| ~ gt(X2,X1) ),
i_0_204 ).
cnf(c_0_2019,plain,
( plus(minus(X1,X2),X2) = X1
| def_10(X2,X1) ),
inference(er,[status(thm)],[c_0_2003]) ).
cnf(c_0_2020,negated_conjecture,
( gt(fifo_length,n1)
| ~ gt(wr_level(x_139),X1) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1987,c_0_2004]),c_0_1975]) ).
cnf(c_0_2021,plain,
( minus(plus(X1,n1),n1) = X1
| gt(X1,minus(plus(X1,n1),n1)) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_2005,c_0_2006]),c_0_2007])]) ).
cnf(c_0_2022,negated_conjecture,
( plus(wr_level(x_139),n1) = fifo_length
| fifo_length = n0
| ~ gt(n1,y_27(fifo_length)) ),
inference(spm,[status(thm)],[c_0_2008,c_0_1989]) ).
cnf(c_0_2023,plain,
( y_27(X1) = n0
| X1 = n0
| gt(X1,n1) ),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_2009,c_0_2010]),c_0_1970]) ).
cnf(c_0_2024,plain,
gt(n1,n0),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_2011,c_0_2012]),c_0_2012]) ).
cnf(c_0_2025,axiom,
( p_Reset(X1)
| wr_level(plus(X1,n1)) = plus(wr_level(X1),n1)
| ~ p_Wr(X1)
| ~ p_Rd(X1)
| ~ gt(minus(fifo_length,n1),wr_level(X1)) ),
i_0_154 ).
cnf(c_0_2026,plain,
( wr_level(plus(X1,n1)) = n0
| gt(minus(fifo_length,n1),wr_level(X1))
| ~ p_Wr(X1)
| ~ p_Rd(X1) ),
inference(csr,[status(thm)],[c_0_2013,c_0_1994]) ).
cnf(c_0_2027,negated_conjecture,
( p_Wr(x_139)
| p_Reset(x_139) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_2014,c_0_2015]),c_0_1982]) ).
cnf(c_0_2028,plain,
~ p_Reset(x_139),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_2016,c_0_1995]),c_0_2017])]) ).
cnf(c_0_2029,plain,
( plus(minus(X1,X2),X2) = X1
| ~ gt(X1,X2) ),
inference(spm,[status(thm)],[c_0_2018,c_0_2019]) ).
cnf(c_0_2030,negated_conjecture,
( minus(plus(wr_level(x_139),n1),n1) = wr_level(x_139)
| gt(fifo_length,n1) ),
inference(spm,[status(thm)],[c_0_2020,c_0_2021]) ).
cnf(c_0_2031,negated_conjecture,
( plus(wr_level(x_139),n1) = fifo_length
| fifo_length = n0
| gt(fifo_length,n1) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_2022,c_0_2023]),c_0_2024])]) ).
cnf(c_0_2032,negated_conjecture,
( wr_level(plus(x_139,n1)) = fifo_length
| gt(wr_level(plus(x_139,n1)),fifo_length) ),
inference(spm,[status(thm)],[c_0_2005,c_0_2014]) ).
cnf(c_0_2033,plain,
( wr_level(plus(X1,n1)) = plus(wr_level(X1),n1)
| wr_level(plus(X1,n1)) = n0
| ~ p_Wr(X1)
| ~ p_Rd(X1) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_2025,c_0_2026]),c_0_1994]) ).
cnf(c_0_2034,negated_conjecture,
p_Wr(x_139),
inference(sr,[status(thm)],[c_0_2027,c_0_2028]) ).
cnf(c_0_2035,negated_conjecture,
( plus(wr_level(x_139),n1) = n1
| gt(fifo_length,n1)
| fifo_length != n0 ),
inference(spm,[status(thm)],[c_0_1990,c_0_1996]) ).
cnf(c_0_2036,plain,
( ~ gt(n1,X1)
| ~ gt(X1,n1) ),
inference(spm,[status(thm)],[c_0_1975,c_0_2029]) ).
cnf(c_0_2037,negated_conjecture,
( wr_level(x_139) = minus(fifo_length,n1)
| fifo_length = n0
| gt(fifo_length,n1) ),
inference(spm,[status(thm)],[c_0_2030,c_0_2031]) ).
cnf(c_0_2038,negated_conjecture,
( wr_level(plus(x_139,n1)) = n0
| plus(wr_level(x_139),n1) = fifo_length
| ~ p_Rd(x_139) ),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_2032,c_0_2033]),c_0_2034])]),c_0_1982]) ).
cnf(c_0_2039,negated_conjecture,
~ gt(n1,fifo_length),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_1982,c_0_2035]),c_0_1977]),c_0_2036]) ).
cnf(c_0_2040,axiom,
( X1 = X2
| plus(X1,n1) != plus(X2,n1) ),
i_0_208 ).
cnf(c_0_2041,negated_conjecture,
( plus(minus(fifo_length,n1),n1) = fifo_length
| fifo_length = n0 ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_2031,c_0_2037]),c_0_2029]) ).
cnf(c_0_2042,negated_conjecture,
( plus(wr_level(x_139),n1) = fifo_length
| ~ p_Rd(x_139) ),
inference(sr,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_2014,c_0_2038]),c_0_1970]),c_0_2039]) ).
cnf(c_0_2043,plain,
( wr_level(plus(X1,n1)) = wr_level(X1)
| p_Reset(X1)
| p_Rd(X1)
| gt(fifo_length,level(X1))
| ~ p_Wr(X1) ),
i_0_184 ).
cnf(c_0_2044,negated_conjecture,
( X1 = minus(fifo_length,n1)
| fifo_length = n0
| plus(X1,n1) != fifo_length ),
inference(spm,[status(thm)],[c_0_2040,c_0_2041]) ).
cnf(c_0_2045,negated_conjecture,
( fifo_length != n0
| ~ p_Rd(x_139) ),
inference(spm,[status(thm)],[c_0_1990,c_0_2042]) ).
cnf(c_0_2046,plain,
( wr_level(plus(X1,n1)) = wr_level(X1)
| gt(fifo_length,level(X1))
| p_Rd(X1)
| p_Reset(X1) ),
inference(csr,[status(thm)],[c_0_2043,c_0_2015]) ).
cnf(c_0_2047,negated_conjecture,
( wr_level(x_139) = minus(fifo_length,n1)
| ~ p_Rd(x_139) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_2044,c_0_2042]),c_0_2045]) ).
cnf(c_0_2048,axiom,
~ gt(X1,X1),
i_0_216 ).
cnf(c_0_2049,plain,
( wr_level(plus(X1,n1)) = plus(wr_level(X1),n1)
| p_Reset(X1)
| p_Rd(X1)
| ~ p_Wr(X1)
| ~ gt(fifo_length,level(X1))
| ~ gt(minus(fifo_length,n1),wr_level(X1)) ),
i_0_151 ).
cnf(c_0_2050,plain,
( wr_level(plus(X1,n1)) = n0
| p_Reset(X1)
| p_Rd(X1)
| gt(minus(fifo_length,n1),wr_level(X1))
| ~ p_Wr(X1)
| ~ gt(fifo_length,level(X1)) ),
i_0_159 ).
cnf(c_0_2051,negated_conjecture,
( gt(fifo_length,level(x_139))
| p_Rd(x_139)
| p_Reset(x_139) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_2014,c_0_2046]),c_0_1982]) ).
cnf(c_0_2052,negated_conjecture,
( wr_level(plus(x_139,n1)) = n0
| ~ p_Rd(x_139) ),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_2026,c_0_2047]),c_0_2034])]),c_0_2048]) ).
cnf(c_0_2053,plain,
( wr_level(plus(X1,n1)) = plus(wr_level(X1),n1)
| p_Reset(X1)
| ~ gt(minus(fifo_length,n1),wr_level(X1))
| ~ gt(fifo_length,level(X1))
| ~ p_Wr(X1) ),
inference(csr,[status(thm)],[c_0_2049,c_0_2025]) ).
cnf(c_0_2054,plain,
( wr_level(plus(X1,n1)) = n0
| gt(minus(fifo_length,n1),wr_level(X1))
| ~ gt(fifo_length,level(X1))
| ~ p_Wr(X1) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[c_0_2050,c_0_1994]),c_0_2026]) ).
cnf(c_0_2055,negated_conjecture,
( gt(fifo_length,level(x_139))
| p_Rd(x_139) ),
inference(sr,[status(thm)],[c_0_2051,c_0_2028]) ).
cnf(c_0_2056,negated_conjecture,
~ p_Rd(x_139),
inference(sr,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_2014,c_0_2052]),c_0_1970]),c_0_2039]) ).
cnf(c_0_2057,plain,
( wr_level(plus(X1,n1)) = plus(wr_level(X1),n1)
| wr_level(plus(X1,n1)) = n0
| ~ gt(fifo_length,level(X1))
| ~ p_Wr(X1) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_2053,c_0_2054]),c_0_1994]) ).
cnf(c_0_2058,negated_conjecture,
gt(fifo_length,level(x_139)),
inference(sr,[status(thm)],[c_0_2055,c_0_2056]) ).
cnf(c_0_2059,negated_conjecture,
( wr_level(plus(x_139,n1)) = n0
| plus(wr_level(x_139),n1) = fifo_length ),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_2032,c_0_2057]),c_0_2058]),c_0_2034])]),c_0_1982]) ).
cnf(c_0_2060,plain,
( X1 = n0
| gt(X1,n1)
| ~ gt(X1,plus(X2,n1)) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1983,c_0_2023]),c_0_1974]) ).
cnf(c_0_2061,negated_conjecture,
( gt(X1,n0)
| ~ gt(X1,fifo_length) ),
inference(spm,[status(thm)],[c_0_1980,c_0_2017]) ).
cnf(c_0_2062,plain,
y_27(plus(X1,n1)) = X1,
inference(sr,[status(thm)],[inference(er,[status(thm)],[inference(spm,[status(thm)],[c_0_2040,c_0_1976])]),c_0_1990]) ).
cnf(c_0_2063,negated_conjecture,
plus(wr_level(x_139),n1) = fifo_length,
inference(sr,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_2014,c_0_2059]),c_0_1970]),c_0_2039]) ).
cnf(c_0_2064,plain,
( gt(plus(X1,n1),n1)
| ~ gt(X1,X2) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_2060,c_0_1987]),c_0_1990]) ).
cnf(c_0_2065,negated_conjecture,
( wr_level(plus(x_139,n1)) = fifo_length
| gt(wr_level(plus(x_139,n1)),n0) ),
inference(spm,[status(thm)],[c_0_2061,c_0_2032]) ).
cnf(c_0_2066,plain,
plus(n0,n0) != plus(plus(n0,n0),n1),
i_0_1665 ).
cnf(c_0_2067,negated_conjecture,
( y_27(fifo_length) = minus(fifo_length,n1)
| fifo_length = n0 ),
inference(spm,[status(thm)],[c_0_2062,c_0_2041]) ).
cnf(c_0_2068,negated_conjecture,
fifo_length != n0,
inference(spm,[status(thm)],[c_0_1990,c_0_2063]) ).
cnf(c_0_2069,negated_conjecture,
y_27(fifo_length) = wr_level(x_139),
inference(spm,[status(thm)],[c_0_2062,c_0_2063]) ).
cnf(c_0_2070,plain,
( X1 = n0
| ~ gt(plus(X2,n1),X1)
| ~ gt(n1,X2) ),
inference(spm,[status(thm)],[c_0_1998,c_0_1976]) ).
cnf(c_0_2071,negated_conjecture,
( wr_level(plus(x_139,n1)) = fifo_length
| gt(plus(wr_level(plus(x_139,n1)),n1),n1) ),
inference(spm,[status(thm)],[c_0_2064,c_0_2065]) ).
cnf(c_0_2072,plain,
n1 != n0,
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_2066,c_0_1970]),c_0_1970]),c_0_1970]) ).
cnf(c_0_2073,negated_conjecture,
wr_level(x_139) = minus(fifo_length,n1),
inference(rw,[status(thm)],[inference(sr,[status(thm)],[c_0_2067,c_0_2068]),c_0_2069]) ).
cnf(c_0_2074,negated_conjecture,
( wr_level(plus(x_139,n1)) = fifo_length
| ~ gt(n1,wr_level(plus(x_139,n1))) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_2070,c_0_2071]),c_0_2072]) ).
cnf(c_0_2075,plain,
wr_level(plus(x_139,n1)) = n0,
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_2054,c_0_2073]),c_0_2058]),c_0_2034])]),c_0_2048]) ).
cnf(c_0_2076,negated_conjecture,
$false,
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_2074,c_0_2075]),c_0_2075]),c_0_2024])]),c_0_2068]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.10 % Problem : HWV031-1 : TPTP v9.2.1. Released v2.5.0.
% 0.00/0.10 % Command : /export/starexec/sandbox2/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox2/solver/bin/cse --final-prover /export/starexec/sandbox2/solver/bin/eprover --proof-time %d --global-time-limit %d
% 0.13/0.30 % Computer : n001.cluster.edu
% 0.13/0.30 % Model : x86_64 x86_64
% 0.13/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.30 % Memory : 8042.1875MB
% 0.13/0.30 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.30 % CPULimit : 300
% 0.13/0.30 % WCLimit : 300
% 0.13/0.30 % DateTime : Mon May 4 19:12:33 EDT 2026
% 0.13/0.30 % CPUTime :
% 0.13/0.31 % start to proof: theBenchmark
% 162.07/110.40 % Version : CSE_E---1.7
% 162.07/110.40 % Problem : theBenchmark.p
% 162.07/110.40 % SZS status Unsatisfiable for theBenchmark.p
% 162.07/110.40 % SZS output start CNFRefutation
% See solution above
% 167.46/115.80 % Total time : 109.814s
%------------------------------------------------------------------------------