%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : HWV014-1 : TPTP v9.2.1. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox/solver/bin/cse --final-prover /export/starexec/sandbox/solver/bin/eprover --proof-time %d --global-time-limit %d
% Computer : 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:28:56 PM UTC 2026
% Result : Unsatisfiable 0.33s 1.62s
% Output : CNFRefutation 0.33s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named c_0_96)
% 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/sandbox/benchmark/Axioms/HWV003-0.ax',axiom_38) ).
cnf(axiom_21,axiom,
level(X1) = int_level(X1),
file('/export/starexec/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/benchmark/Axioms/HWV003-0.ax',axiom_82) ).
cnf(axiom_26,axiom,
( int_level(plus(X1,n1)) = n0
| ~ p_Reset(X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV003-0.ax',axiom_26) ).
cnf(axiom_24,axiom,
( p_Empty(X1)
| int_level(X1) != n0 ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV003-0.ax',axiom_24) ).
cnf(axiom_22,axiom,
( p_Full(X1)
| int_level(X1) != fifo_length ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV003-0.ax',axiom_22) ).
cnf(axiom_23,axiom,
( int_level(X1) = fifo_length
| ~ p_Full(X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV003-0.ax',axiom_23) ).
cnf(axiom_25,axiom,
( int_level(X1) = n0
| ~ p_Empty(X1) ),
file('/export/starexec/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/benchmark/Axioms/HWV003-0.ax',axiom_63) ).
cnf(axiom_31,axiom,
( ~ p_Reset(X1)
| ~ p_Mem(X2,X3,plus(X1,n1)) ),
file('/export/starexec/sandbox/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/sandbox/benchmark/Axioms/HWV003-0.ax',axiom_67) ).
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/sandbox/benchmark/Axioms/HWV003-0.ax',axiom_64) ).
cnf(axiom_9,axiom,
( gt(X1,X2)
| ~ gt(plus(X1,n1),plus(X2,n1)) ),
file('/export/starexec/sandbox/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/sandbox/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/sandbox/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/sandbox/benchmark/Axioms/HWV003-0.ax',axiom_68) ).
cnf(axiom_8,axiom,
( gt(plus(X1,n1),plus(X2,n1))
| ~ gt(X1,X2) ),
file('/export/starexec/sandbox/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/sandbox/benchmark/Axioms/HWV003-0.ax',axiom_48) ).
cnf(axiom_11,axiom,
( gt(X1,X2)
| X1 = X2
| ~ gt(plus(X1,n1),X2) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV003-0.ax',axiom_11) ).
cnf(axiom_10,axiom,
( gt(X1,X2)
| X2 = X1
| ~ gt(plus(X1,n1),X2) ),
file('/export/starexec/sandbox/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/sandbox/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/sandbox/benchmark/Axioms/HWV003-0.ax',axiom_14) ).
cnf(axiom_32,axiom,
( ~ p_Reset(X1)
| ~ p_Data_out(X2,plus(X1,n1)) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV003-0.ax',axiom_32) ).
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/sandbox/benchmark/Axioms/HWV003-0.ax',axiom_49) ).
cnf(quest_5,negated_conjecture,
level(plus(x_139,n1)) != minus(level(x_139),n1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',quest_5) ).
cnf(axiom_51,axiom,
( p_Reset(X1)
| ~ p_Wr(X1)
| ~ p_Rd(X1)
| ~ p_Wr_error(plus(X1,n1)) ),
file('/export/starexec/sandbox/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/sandbox/benchmark/Axioms/HWV003-0.ax',axiom_85) ).
cnf(axiom_13,axiom,
( gt(X1,X3)
| ~ gt(X1,X2)
| ~ gt(X2,X3) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV003-0.ax',axiom_13) ).
cnf(axiom_3,axiom,
( gt(X1,minus(X1,n1))
| ~ gt(X1,n0) ),
file('/export/starexec/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/benchmark/Axioms/HWV003-0.ax',axiom_50) ).
cnf(axiom_30,axiom,
( ~ p_Reset(X1)
| ~ p_Rd_error(plus(X1,n1)) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV003-0.ax',axiom_30) ).
cnf(axiom_29,axiom,
( ~ p_Reset(X1)
| ~ p_Wr_error(plus(X1,n1)) ),
file('/export/starexec/sandbox/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/sandbox/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/sandbox/benchmark/Axioms/HWV003-0.ax',axiom_33) ).
cnf(axiom_6,axiom,
( ~ def_10(X1,X2)
| ~ gt(X2,X1) ),
file('/export/starexec/sandbox/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/sandbox/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/sandbox/benchmark/Axioms/HWV003-0.ax',axiom_90) ).
cnf(axiom_18,axiom,
( X1 = X2
| plus(X1,n1) != plus(X2,n1) ),
file('/export/starexec/sandbox/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/sandbox/benchmark/Axioms/HWV003-0.ax',axiom_69) ).
cnf(axiom_2,axiom,
gt(plus(X1,n1),n0),
file('/export/starexec/sandbox/benchmark/Axioms/HWV003-0.ax',axiom_2) ).
cnf(axiom_28,axiom,
( rd_level(plus(X1,n1)) = n0
| ~ p_Reset(X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV003-0.ax',axiom_28) ).
cnf(axiom_27,axiom,
( wr_level(plus(X1,n1)) = n0
| ~ p_Reset(X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV003-0.ax',axiom_27) ).
cnf(axiom_12,axiom,
( gt(X1,X2)
| X2 = X1
| gt(X2,X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV003-0.ax',axiom_12) ).
cnf(axiom_7,axiom,
( ~ def_10(X1,X2)
| X2 != X1 ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV003-0.ax',axiom_7) ).
cnf(axiom_17,axiom,
~ gt(X1,X1),
file('/export/starexec/sandbox/benchmark/Axioms/HWV003-0.ax',axiom_17) ).
cnf(axiom_16,axiom,
( X1 = n0
| X1 = plus(y_27(X1),n1) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV003-0.ax',axiom_16) ).
cnf(axiom_1,axiom,
plus(X1,n1) != n0,
file('/export/starexec/sandbox/benchmark/Axioms/HWV003-0.ax',axiom_1) ).
cnf(quest_1,negated_conjecture,
gt(level(x_139),n0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',quest_1) ).
cnf(axiom_15,axiom,
( X1 = n0
| gt(X1,n0) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV003-0.ax',axiom_15) ).
cnf(axiom_19,axiom,
plus(n0,X1) = X1,
file('/export/starexec/sandbox/benchmark/Axioms/HWV003-0.ax',axiom_19) ).
cnf(axiom_20,axiom,
n1 = plus(n0,n1),
file('/export/starexec/sandbox/benchmark/Axioms/HWV003-0.ax',axiom_20) ).
cnf(quest_3,negated_conjecture,
~ p_Wr(x_139),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',quest_3) ).
cnf(quest_4,negated_conjecture,
~ p_Reset(x_139),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',quest_4) ).
cnf(quest_2,negated_conjecture,
p_Rd(x_139),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',quest_2) ).
cnf(i_0_95,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_96,axiom,
level(X1) = int_level(X1),
axiom_21 ).
cnf(i_0_97,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_98,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_99,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_100,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_101,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_102,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_103,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_104,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_105,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_106,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_107,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_108,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_109,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_110,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_111,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_112,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_113,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_114,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_115,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_116,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_117,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_118,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_119,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_120,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_121,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_122,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_123,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_124,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_125,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_126,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_127,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_128,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_129,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_130,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_131,axiom,
( p_Reset(X1)
| p_Wr(X1)
| p_Rd(X1)
| int_level(plus(X1,n1)) = int_level(X1) ),
axiom_82 ).
cnf(i_0_132,axiom,
( int_level(plus(X1,n1)) = n0
| ~ p_Reset(X1) ),
axiom_26 ).
cnf(i_0_133,axiom,
( p_Empty(X1)
| int_level(X1) != n0 ),
axiom_24 ).
cnf(i_0_134,axiom,
( p_Full(X1)
| int_level(X1) != fifo_length ),
axiom_22 ).
cnf(i_0_135,axiom,
( int_level(X1) = fifo_length
| ~ p_Full(X1) ),
axiom_23 ).
cnf(i_0_136,axiom,
( int_level(X1) = n0
| ~ p_Empty(X1) ),
axiom_25 ).
cnf(i_0_137,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_95,c_0_96]),
[final] ).
cnf(i_0_138,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_97,c_0_96]),
[final] ).
cnf(i_0_139,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_98,c_0_96]),
[final] ).
cnf(i_0_140,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_141,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_99,c_0_96]),
[final] ).
cnf(i_0_142,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_100,c_0_96]),
[final] ).
cnf(i_0_143,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_144,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_145,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_101,c_0_96]),
[final] ).
cnf(i_0_146,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_102,c_0_96]),
[final] ).
cnf(i_0_147,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_148,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_103,c_0_96]),
[final] ).
cnf(i_0_149,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_104,c_0_96]),
[final] ).
cnf(i_0_150,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_151,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_105,c_0_96]),
[final] ).
cnf(i_0_152,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_106,c_0_96]),
[final] ).
cnf(i_0_153,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_107,c_0_96]),
[final] ).
cnf(i_0_154,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_108,c_0_96]),
[final] ).
cnf(i_0_155,axiom,
( ~ p_Reset(X1)
| ~ p_Mem(X2,X3,plus(X1,n1)) ),
axiom_31,
[final] ).
cnf(i_0_156,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_157,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_158,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_109,c_0_96]),
[final] ).
cnf(i_0_159,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_110,c_0_96]),
[final] ).
cnf(i_0_160,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_111,c_0_96]),
[final] ).
cnf(i_0_161,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_112,c_0_96]),
[final] ).
cnf(i_0_162,axiom,
( gt(X1,X2)
| ~ gt(plus(X1,n1),plus(X2,n1)) ),
axiom_9,
[final] ).
cnf(i_0_163,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_113,c_0_96]),
[final] ).
cnf(i_0_164,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_114,c_0_96]),
[final] ).
cnf(i_0_165,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_115,c_0_96]),
[final] ).
cnf(i_0_166,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_116,c_0_96]),
[final] ).
cnf(i_0_167,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_117,c_0_96]),c_0_96]),c_0_96]),
[final] ).
cnf(i_0_168,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_118,c_0_96]),c_0_96]),c_0_96]),
[final] ).
cnf(i_0_169,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_170,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_119,c_0_96]),
[final] ).
cnf(i_0_171,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_120,c_0_96]),
[final] ).
cnf(i_0_172,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_173,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_174,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_121,c_0_96]),c_0_96]),c_0_96]),
[final] ).
cnf(i_0_175,axiom,
( gt(plus(X1,n1),plus(X2,n1))
| ~ gt(X1,X2) ),
axiom_8,
[final] ).
cnf(i_0_176,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_122,c_0_96]),c_0_96]),c_0_96]),
[final] ).
cnf(i_0_177,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_178,axiom,
( gt(X1,X2)
| X1 = X2
| ~ gt(plus(X1,n1),X2) ),
axiom_11,
[final] ).
cnf(i_0_179,axiom,
( gt(X1,X2)
| X2 = X1
| ~ gt(plus(X1,n1),X2) ),
axiom_10,
[final] ).
cnf(i_0_180,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_181,axiom,
( plus(X2,n1) = X1
| gt(X1,plus(X2,n1))
| ~ gt(X1,X2) ),
axiom_14,
[final] ).
cnf(i_0_182,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_123,c_0_96]),
[final] ).
cnf(i_0_183,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_124,c_0_96]),
[final] ).
cnf(i_0_184,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_125,c_0_96]),c_0_96]),c_0_96]),
[final] ).
cnf(i_0_185,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_126,c_0_96]),
[final] ).
cnf(i_0_186,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_127,c_0_96]),c_0_96]),c_0_96]),
[final] ).
cnf(i_0_187,axiom,
( ~ p_Reset(X1)
| ~ p_Data_out(X2,plus(X1,n1)) ),
axiom_32,
[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_128,c_0_96]),
[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_129,c_0_96]),
[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_130,c_0_96]),
[final] ).
cnf(i_0_192,negated_conjecture,
level(plus(x_139,n1)) != minus(level(x_139),n1),
quest_5,
[final] ).
cnf(i_0_193,axiom,
( p_Reset(X1)
| ~ p_Wr(X1)
| ~ p_Rd(X1)
| ~ p_Wr_error(plus(X1,n1)) ),
axiom_51,
[final] ).
cnf(i_0_194,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_195,axiom,
( gt(X1,X3)
| ~ gt(X1,X2)
| ~ gt(X2,X3) ),
axiom_13,
[final] ).
cnf(i_0_196,axiom,
( gt(X1,minus(X1,n1))
| ~ gt(X1,n0) ),
axiom_3,
[final] ).
cnf(i_0_197,axiom,
( p_Reset(X1)
| p_Wr(X1)
| p_Wr_error(X1)
| ~ p_Wr_error(plus(X1,n1)) ),
axiom_89,
[final] ).
cnf(i_0_198,axiom,
( minus(X1,X2) = X3
| def_10(X2,X1)
| plus(X3,X2) != X1 ),
axiom_5,
[final] ).
cnf(i_0_199,axiom,
( plus(X3,X2) = X1
| def_10(X2,X1)
| minus(X1,X2) != X3 ),
axiom_4,
[final] ).
cnf(i_0_200,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_201,axiom,
( ~ p_Reset(X1)
| ~ p_Rd_error(plus(X1,n1)) ),
axiom_30,
[final] ).
cnf(i_0_202,axiom,
( ~ p_Reset(X1)
| ~ p_Wr_error(plus(X1,n1)) ),
axiom_29,
[final] ).
cnf(i_0_203,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_204,axiom,
( p_Reset(X1)
| p_Rd(X1)
| rd_level(plus(X1,n1)) = rd_level(X1)
| ~ p_Wr(X1) ),
axiom_33,
[final] ).
cnf(i_0_205,axiom,
( ~ def_10(X1,X2)
| ~ gt(X2,X1) ),
axiom_6,
[final] ).
cnf(i_0_206,axiom,
( p_Reset(X1)
| p_Wr(X1)
| p_Rd(X1)
| rd_level(plus(X1,n1)) = rd_level(X1) ),
axiom_81,
[final] ).
cnf(i_0_207,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_131,c_0_96]),c_0_96]),
[final] ).
cnf(i_0_208,axiom,
( p_Reset(X1)
| p_Wr(X1)
| p_Wr_error(plus(X1,n1))
| ~ p_Wr_error(X1) ),
axiom_90,
[final] ).
cnf(i_0_209,axiom,
( X1 = X2
| plus(X1,n1) != plus(X2,n1) ),
axiom_18,
[final] ).
cnf(i_0_210,axiom,
( p_Reset(X1)
| p_Wr(X1)
| wr_level(plus(X1,n1)) = wr_level(X1) ),
axiom_69,
[final] ).
cnf(i_0_211,axiom,
gt(plus(X1,n1),n0),
axiom_2,
[final] ).
cnf(i_0_212,axiom,
( rd_level(plus(X1,n1)) = n0
| ~ p_Reset(X1) ),
axiom_28,
[final] ).
cnf(i_0_213,axiom,
( wr_level(plus(X1,n1)) = n0
| ~ p_Reset(X1) ),
axiom_27,
[final] ).
cnf(i_0_214,plain,
( level(plus(X1,n1)) = n0
| ~ p_Reset(X1) ),
inference(rw,[status(thm)],[i_0_132,c_0_96]),
[final] ).
cnf(i_0_215,axiom,
( gt(X1,X2)
| X2 = X1
| gt(X2,X1) ),
axiom_12,
[final] ).
cnf(i_0_216,axiom,
( ~ def_10(X1,X2)
| X2 != X1 ),
axiom_7,
[final] ).
cnf(i_0_217,axiom,
~ gt(X1,X1),
axiom_17,
[final] ).
cnf(i_0_218,axiom,
( X1 = n0
| X1 = plus(y_27(X1),n1) ),
axiom_16,
[final] ).
cnf(i_0_219,axiom,
plus(X1,n1) != n0,
axiom_1,
[final] ).
cnf(i_0_220,negated_conjecture,
gt(level(x_139),n0),
quest_1,
[final] ).
cnf(i_0_221,axiom,
( X1 = n0
| gt(X1,n0) ),
axiom_15,
[final] ).
cnf(i_0_222,axiom,
plus(n0,X1) = X1,
axiom_19,
[final] ).
cnf(i_0_223,plain,
( p_Empty(X1)
| level(X1) != n0 ),
inference(rw,[status(thm)],[i_0_133,c_0_96]),
[final] ).
cnf(i_0_224,plain,
( p_Full(X1)
| level(X1) != fifo_length ),
inference(rw,[status(thm)],[i_0_134,c_0_96]),
[final] ).
cnf(i_0_225,plain,
( level(X1) = fifo_length
| ~ p_Full(X1) ),
inference(rw,[status(thm)],[i_0_135,c_0_96]),
[final] ).
cnf(i_0_226,plain,
( level(X1) = n0
| ~ p_Empty(X1) ),
inference(rw,[status(thm)],[i_0_136,c_0_96]),
[final] ).
cnf(i_0_227,axiom,
n1 = plus(n0,n1),
axiom_20,
[final] ).
cnf(i_0_228,negated_conjecture,
~ p_Wr(x_139),
quest_3,
[final] ).
cnf(i_0_229,negated_conjecture,
~ p_Reset(x_139),
quest_4,
[final] ).
cnf(i_0_230,negated_conjecture,
p_Rd(x_139),
quest_2,
[final] ).
cnf(i_0_231,axiom,
X1 = X1 ).
cnf(i_0_232,axiom,
( X1 = X2
| X2 != X1 ) ).
cnf(i_0_233,axiom,
( X1 = X2
| X1 != X3
| X3 != X2 ) ).
cnf(i_0_234,axiom,
( X1 != X2
| wr_level(X1) = wr_level(X2) ) ).
cnf(i_0_235,axiom,
( X1 != X2
| level(X1) = level(X2) ) ).
cnf(i_0_236,axiom,
( X1 != X2
| plus(X1,X3) = plus(X2,X3) ) ).
cnf(i_0_237,axiom,
( X1 != X2
| plus(X3,X1) = plus(X3,X2) ) ).
cnf(i_0_238,axiom,
( X1 != X2
| rd_level(X1) = rd_level(X2) ) ).
cnf(i_0_239,axiom,
( X1 != X2
| minus(X1,X3) = minus(X2,X3) ) ).
cnf(i_0_240,axiom,
( X1 != X2
| minus(X3,X1) = minus(X3,X2) ) ).
cnf(i_0_241,axiom,
( X1 != X2
| ~ p_Reset(X1)
| p_Reset(X2) ) ).
cnf(i_0_242,axiom,
( X1 != X2
| ~ def_10(X1,X3)
| def_10(X2,X3) ) ).
cnf(i_0_243,axiom,
( X1 != X2
| ~ def_10(X3,X1)
| def_10(X3,X2) ) ).
cnf(i_0_244,axiom,
( X1 != X2
| ~ p_Empty(X1)
| p_Empty(X2) ) ).
cnf(i_0_245,axiom,
( X1 != X2
| ~ p_Full(X1)
| p_Full(X2) ) ).
cnf(i_0_246,axiom,
( X1 != X2
| ~ p_Rd(X1)
| p_Rd(X2) ) ).
cnf(i_0_247,axiom,
( X1 != X2
| ~ p_Mem(X1,X3,X4)
| p_Mem(X2,X3,X4) ) ).
cnf(i_0_248,axiom,
( X1 != X2
| ~ p_Mem(X3,X1,X4)
| p_Mem(X3,X2,X4) ) ).
cnf(i_0_249,axiom,
( X1 != X2
| ~ p_Mem(X3,X4,X1)
| p_Mem(X3,X4,X2) ) ).
cnf(i_0_250,axiom,
( X1 != X2
| ~ p_Wr(X1)
| p_Wr(X2) ) ).
cnf(i_0_251,axiom,
( X1 != X2
| ~ gt(X1,X3)
| gt(X2,X3) ) ).
cnf(i_0_252,axiom,
( X1 != X2
| ~ gt(X3,X1)
| gt(X3,X2) ) ).
cnf(i_0_253,axiom,
( X1 != X2
| ~ p_Data_in(X1,X3)
| p_Data_in(X2,X3) ) ).
cnf(i_0_254,axiom,
( X1 != X2
| ~ p_Data_in(X3,X1)
| p_Data_in(X3,X2) ) ).
cnf(i_0_255,axiom,
( X1 != X2
| ~ p_Data_out(X1,X3)
| p_Data_out(X2,X3) ) ).
cnf(i_0_256,axiom,
( X1 != X2
| ~ p_Data_out(X3,X1)
| p_Data_out(X3,X2) ) ).
cnf(i_0_257,axiom,
( X1 != X2
| ~ p_Rd_error(X1)
| p_Rd_error(X2) ) ).
cnf(i_0_258,axiom,
( X1 != X2
| ~ p_Wr_error(X1)
| p_Wr_error(X2) ) ).
cnf(i_0_231_001,axiom,
X1 = X1 ).
cnf(i_0_232_002,axiom,
( X1 = X2
| X2 != X1 ) ).
cnf(i_0_233_003,axiom,
( X1 = X2
| X1 != X3
| X3 != X2 ) ).
cnf(i_0_234_004,axiom,
( X1 != X2
| wr_level(X1) = wr_level(X2) ) ).
cnf(i_0_235_005,axiom,
( X1 != X2
| level(X1) = level(X2) ) ).
cnf(i_0_236_006,axiom,
( X1 != X2
| plus(X1,X3) = plus(X2,X3) ) ).
cnf(i_0_237_007,axiom,
( X1 != X2
| plus(X3,X1) = plus(X3,X2) ) ).
cnf(i_0_238_008,axiom,
( X1 != X2
| rd_level(X1) = rd_level(X2) ) ).
cnf(i_0_239_009,axiom,
( X1 != X2
| minus(X1,X3) = minus(X2,X3) ) ).
cnf(i_0_240_010,axiom,
( X1 != X2
| minus(X3,X1) = minus(X3,X2) ) ).
cnf(i_0_241_011,axiom,
( X1 != X2
| ~ p_Reset(X1)
| p_Reset(X2) ) ).
cnf(i_0_242_012,axiom,
( X1 != X2
| ~ def_10(X1,X3)
| def_10(X2,X3) ) ).
cnf(i_0_243_013,axiom,
( X1 != X2
| ~ def_10(X3,X1)
| def_10(X3,X2) ) ).
cnf(i_0_244_014,axiom,
( X1 != X2
| ~ p_Empty(X1)
| p_Empty(X2) ) ).
cnf(i_0_245_015,axiom,
( X1 != X2
| ~ p_Full(X1)
| p_Full(X2) ) ).
cnf(i_0_246_016,axiom,
( X1 != X2
| ~ p_Rd(X1)
| p_Rd(X2) ) ).
cnf(i_0_247_017,axiom,
( X1 != X2
| ~ p_Mem(X1,X3,X4)
| p_Mem(X2,X3,X4) ) ).
cnf(i_0_248_018,axiom,
( X1 != X2
| ~ p_Mem(X3,X1,X4)
| p_Mem(X3,X2,X4) ) ).
cnf(i_0_249_019,axiom,
( X1 != X2
| ~ p_Mem(X3,X4,X1)
| p_Mem(X3,X4,X2) ) ).
cnf(i_0_250_020,axiom,
( X1 != X2
| ~ p_Wr(X1)
| p_Wr(X2) ) ).
cnf(i_0_251_021,axiom,
( X1 != X2
| ~ gt(X1,X3)
| gt(X2,X3) ) ).
cnf(i_0_252_022,axiom,
( X1 != X2
| ~ gt(X3,X1)
| gt(X3,X2) ) ).
cnf(i_0_253_023,axiom,
( X1 != X2
| ~ p_Data_in(X1,X3)
| p_Data_in(X2,X3) ) ).
cnf(i_0_254_024,axiom,
( X1 != X2
| ~ p_Data_in(X3,X1)
| p_Data_in(X3,X2) ) ).
cnf(i_0_255_025,axiom,
( X1 != X2
| ~ p_Data_out(X1,X3)
| p_Data_out(X2,X3) ) ).
cnf(i_0_256_026,axiom,
( X1 != X2
| ~ p_Data_out(X3,X1)
| p_Data_out(X3,X2) ) ).
cnf(i_0_257_027,axiom,
( X1 != X2
| ~ p_Rd_error(X1)
| p_Rd_error(X2) ) ).
cnf(i_0_258_028,axiom,
( X1 != X2
| ~ p_Wr_error(X1)
| p_Wr_error(X2) ) ).
cnf(i_0_259,plain,
( def_10(X1,plus(X2,X1))
| minus(plus(X2,X1),X1) = X2 ),
inference(equality_inference,[],[198]) ).
cnf(i_0_260,plain,
( def_10(X1,X2)
| plus(minus(X2,X1),X1) = X2 ),
inference(equality_inference,[],[199]) ).
cnf(i_0_261,plain,
X1 = X1,
inference(equality_inference,[],[209]) ).
cnf(i_0_262,plain,
~ def_10(X1,X1),
inference(equality_inference,[],[216]) ).
cnf(i_0_263,plain,
$false,
inference(scs_inference,[],[i_0_192,i_0_229,i_0_228,i_0_230,i_0_220,i_0_167]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : HWV014-1 : TPTP v9.2.1. Released v2.5.0.
% 0.00/0.12 % Command : /export/starexec/sandbox/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox/solver/bin/cse --final-prover /export/starexec/sandbox/solver/bin/eprover --proof-time %d --global-time-limit %d
% 0.15/0.33 % Computer : n001.cluster.edu
% 0.15/0.33 % Model : x86_64 x86_64
% 0.15/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.33 % Memory : 8042.1875MB
% 0.15/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.33 % CPULimit : 300
% 0.15/0.33 % WCLimit : 300
% 0.15/0.33 % DateTime : Mon May 4 19:11:48 EDT 2026
% 0.15/0.34 % CPUTime :
% 0.15/0.35 % start to proof: theBenchmark
% 0.33/1.62 % Version : CSE_E---1.7
% 0.33/1.62 % Problem : theBenchmark.p
% 0.33/1.62 % SZS status Unsatisfiable for theBenchmark.p
% 0.33/1.62 % SZS output start CNFRefutation
% See solution above
% 0.33/1.65 % Total time : 1.272s
%------------------------------------------------------------------------------