%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : HWV022-1 : TPTP v9.3.1. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n007.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 12:46:42 PM UTC 2026
% Result : Unsatisfiable 0.12s 0.46s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : HWV022-1 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n007.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Sun Sep 20 20:46:35 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.08/0.37 % Drodi V4.1.1
% 0.12/0.46 % Refutation found
% 0.12/0.46 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.12/0.46 % SZS output start CNFRefutation for theBenchmark
% 0.12/0.46 fof(f2,axiom,(
% 0.12/0.46 (![X_1]: (gt(plus(X_1,n1),n0) ))),
% 0.12/0.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.46 fof(f3,axiom,(
% 0.12/0.46 (![X_2]: (( ~ gt(X_2,n0)| gt(X_2,minus(X_2,n1)) ) ))),
% 0.12/0.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.46 fof(f5,axiom,(
% 0.12/0.46 (![X_3,Y_4,Z_5]: (( minus(X_3,Y_4) = Z_5| plus(Z_5,Y_4) != X_3| def_10(Y_4,X_3) ) ))),
% 0.12/0.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.46 fof(f6,axiom,(
% 0.12/0.46 (![Y_4,X_3]: (( ~ def_10(Y_4,X_3)| ~ gt(X_3,Y_4) ) ))),
% 0.12/0.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.46 fof(f14,axiom,(
% 0.12/0.46 (![Y_24,X_23]: (( ~ gt(Y_24,X_23)| plus(X_23,n1) = Y_24| gt(Y_24,plus(X_23,n1)) ) ))),
% 0.12/0.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.46 fof(f18,axiom,(
% 0.12/0.46 (![X_29,Y_30]: (( plus(X_29,n1) != plus(Y_30,n1)| X_29 = Y_30 ) ))),
% 0.12/0.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.46 fof(f19,axiom,(
% 0.12/0.46 (![X_31]: (plus(n0,X_31) = X_31 ))),
% 0.12/0.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.46 fof(f21,axiom,(
% 0.12/0.46 (![X_t_32]: (level(X_t_32) = int_level(X_t_32) ))),
% 0.12/0.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.46 fof(f24,axiom,(
% 0.12/0.46 (![X_t_35]: (( int_level(X_t_35) != n0| p_Empty(X_t_35) ) ))),
% 0.12/0.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.46 fof(f25,axiom,(
% 0.12/0.46 (![X_t_36]: (( int_level(X_t_36) = n0| ~ p_Empty(X_t_36) ) ))),
% 0.12/0.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.46 fof(f35,axiom,(
% 0.12/0.46 (![X_t_42]: (( p_Reset(X_t_42)| ~ p_Wr(X_t_42)| p_Rd(X_t_42)| ~ gt(fifo_length,int_level(X_t_42))| int_level(plus(X_t_42,n1)) = plus(int_level(X_t_42),n1) ) ))),
% 0.12/0.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.46 fof(f91,negated_conjecture,(
% 0.12/0.46 plus(level(t_139),n1) = fifo_length ),
% 0.12/0.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.46 fof(f92,negated_conjecture,(
% 0.12/0.46 ~ p_Rd(t_139) ),
% 0.12/0.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.46 fof(f93,negated_conjecture,(
% 0.12/0.46 p_Wr(t_139) ),
% 0.12/0.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.46 fof(f94,negated_conjecture,(
% 0.12/0.46 ~ p_Reset(t_139) ),
% 0.12/0.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.46 fof(f95,negated_conjecture,(
% 0.12/0.46 level(plus(t_139,n1)) != fifo_length ),
% 0.12/0.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.46 fof(f97,plain,(
% 0.12/0.46 ![X0]: (gt(plus(X0,n1),n0))),
% 0.12/0.46 inference(cnf_transformation,[status(thm)],[f2])).
% 0.12/0.46 fof(f98,plain,(
% 0.12/0.46 ![X0]: (~gt(X0,n0)|gt(X0,minus(X0,n1)))),
% 0.12/0.46 inference(cnf_transformation,[status(thm)],[f3])).
% 0.12/0.46 fof(f101,plain,(
% 0.12/0.46 ![X_3,Y_4]: ((![Z_5]: (minus(X_3,Y_4)=Z_5|~plus(Z_5,Y_4)=X_3))|def_10(Y_4,X_3))),
% 0.12/0.46 inference(miniscoping,[status(thm)],[f5])).
% 0.12/0.46 fof(f102,plain,(
% 0.12/0.46 ![X0,X1,X2]: (minus(X0,X1)=X2|~plus(X2,X1)=X0|def_10(X1,X0))),
% 0.12/0.46 inference(cnf_transformation,[status(thm)],[f101])).
% 0.12/0.46 fof(f103,plain,(
% 0.12/0.46 ![X0,X1]: (~def_10(X0,X1)|~gt(X1,X0))),
% 0.12/0.46 inference(cnf_transformation,[status(thm)],[f6])).
% 0.12/0.46 fof(f112,plain,(
% 0.12/0.46 ![X0,X1]: (~gt(X0,X1)|plus(X1,n1)=X0|gt(X0,plus(X1,n1)))),
% 0.12/0.46 inference(cnf_transformation,[status(thm)],[f14])).
% 0.12/0.46 fof(f116,plain,(
% 0.12/0.46 ![X0,X1]: (~plus(X0,n1)=plus(X1,n1)|X0=X1)),
% 0.12/0.46 inference(cnf_transformation,[status(thm)],[f18])).
% 0.12/0.46 fof(f117,plain,(
% 0.12/0.46 ![X0]: (plus(n0,X0)=X0)),
% 0.12/0.46 inference(cnf_transformation,[status(thm)],[f19])).
% 0.12/0.46 fof(f119,plain,(
% 0.12/0.46 ![X0]: (level(X0)=int_level(X0))),
% 0.12/0.46 inference(cnf_transformation,[status(thm)],[f21])).
% 0.12/0.46 fof(f122,plain,(
% 0.12/0.46 ![X0]: (~int_level(X0)=n0|p_Empty(X0))),
% 0.12/0.46 inference(cnf_transformation,[status(thm)],[f24])).
% 0.12/0.46 fof(f123,plain,(
% 0.12/0.46 ![X0]: (int_level(X0)=n0|~p_Empty(X0))),
% 0.12/0.46 inference(cnf_transformation,[status(thm)],[f25])).
% 0.12/0.46 fof(f135,plain,(
% 0.12/0.46 ![X0]: (p_Reset(X0)|~p_Wr(X0)|p_Rd(X0)|~gt(fifo_length,int_level(X0))|int_level(plus(X0,n1))=plus(int_level(X0),n1))),
% 0.12/0.46 inference(cnf_transformation,[status(thm)],[f35])).
% 0.12/0.46 fof(f191,plain,(
% 0.12/0.46 plus(level(t_139),n1)=fifo_length),
% 0.12/0.46 inference(cnf_transformation,[status(thm)],[f91])).
% 0.12/0.46 fof(f192,plain,(
% 0.12/0.46 ~p_Rd(t_139)),
% 0.12/0.46 inference(cnf_transformation,[status(thm)],[f92])).
% 0.12/0.46 fof(f193,plain,(
% 0.12/0.46 p_Wr(t_139)),
% 0.12/0.46 inference(cnf_transformation,[status(thm)],[f93])).
% 0.12/0.46 fof(f194,plain,(
% 0.12/0.46 ~p_Reset(t_139)),
% 0.12/0.46 inference(cnf_transformation,[status(thm)],[f94])).
% 0.12/0.46 fof(f195,plain,(
% 0.12/0.46 ~level(plus(t_139,n1))=fifo_length),
% 0.12/0.46 inference(cnf_transformation,[status(thm)],[f95])).
% 0.12/0.46 fof(f197,plain,(
% 0.12/0.46 ![X0,X1]: (minus(plus(X0,X1),X1)=X0|def_10(X1,plus(X0,X1)))),
% 0.12/0.46 inference(destructive_equality_resolution,[status(thm)],[f102])).
% 0.12/0.46 fof(f202,plain,(
% 0.12/0.46 ![X0]: (~plus(X0,n1)=n1|X0=n0)),
% 0.12/0.46 inference(paramodulation,[status(thm)],[f117,f116])).
% 0.12/0.46 fof(f206,plain,(
% 0.12/0.46 gt(n1,n0)),
% 0.12/0.46 inference(paramodulation,[status(thm)],[f117,f97])).
% 0.12/0.46 fof(f207,plain,(
% 0.12/0.46 gt(fifo_length,n0)),
% 0.12/0.46 inference(paramodulation,[status(thm)],[f191,f97])).
% 0.12/0.46 fof(f209,plain,(
% 0.12/0.46 gt(fifo_length,minus(fifo_length,n1))),
% 0.12/0.46 inference(resolution,[status(thm)],[f207,f98])).
% 0.12/0.46 fof(f211,plain,(
% 0.12/0.46 ~n1=n1|n0=n0),
% 0.12/0.46 inference(paramodulation,[status(thm)],[f117,f202])).
% 0.12/0.46 fof(f212,plain,(
% 0.12/0.46 ~fifo_length=n1|level(t_139)=n0),
% 0.12/0.46 inference(paramodulation,[status(thm)],[f191,f202])).
% 0.12/0.46 fof(f213,definition,(
% 0.12/0.46 sQ0_spl <=> (n1=n1)),
% 0.12/0.46 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.12/0.46 fof(f215,plain,(
% 0.12/0.46 ~n1=n1|sQ0_spl),
% 0.12/0.46 inference(component_clause,[status(thm)],[f213])).
% 0.12/0.46 fof(f216,definition,(
% 0.12/0.46 sQ1_spl <=> (n0=n0)),
% 0.12/0.46 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 0.12/0.46 fof(f219,plain,(
% 0.12/0.46 ~sQ0_spl|sQ1_spl),
% 0.12/0.46 inference(split_clause,[status(thm)],[f211,f213,f216])).
% 0.12/0.46 fof(f220,definition,(
% 0.12/0.46 sQ2_spl <=> (fifo_length=n1)),
% 0.12/0.46 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.12/0.46 fof(f222,plain,(
% 0.12/0.46 ~fifo_length=n1|sQ2_spl),
% 0.12/0.46 inference(component_clause,[status(thm)],[f220])).
% 0.12/0.46 fof(f223,definition,(
% 0.12/0.46 sQ3_spl <=> (level(t_139)=n0)),
% 0.12/0.46 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 0.12/0.46 fof(f224,plain,(
% 0.12/0.46 level(t_139)=n0|~sQ3_spl),
% 0.12/0.46 inference(component_clause,[status(thm)],[f223])).
% 0.12/0.46 fof(f226,plain,(
% 0.12/0.46 ~sQ2_spl|sQ3_spl),
% 0.12/0.46 inference(split_clause,[status(thm)],[f212,f220,f223])).
% 0.12/0.46 fof(f227,plain,(
% 0.12/0.46 $false|sQ0_spl),
% 0.12/0.46 inference(trivial_equality_resolution,[status(thm)],[f215])).
% 0.12/0.46 fof(f228,plain,(
% 0.12/0.46 sQ0_spl),
% 0.12/0.46 inference(contradiction_clause,[status(thm)],[f227])).
% 0.12/0.46 fof(f229,plain,(
% 0.12/0.46 ![X0]: (p_Reset(X0)|~p_Wr(X0)|p_Rd(X0)|~gt(fifo_length,level(X0))|int_level(plus(X0,n1))=plus(int_level(X0),n1))),
% 0.12/0.46 inference(forward_demodulation,[status(thm)],[f119,f135])).
% 0.12/0.46 fof(f230,plain,(
% 0.12/0.46 ![X0]: (p_Reset(X0)|~p_Wr(X0)|p_Rd(X0)|~gt(fifo_length,level(X0))|level(plus(X0,n1))=plus(int_level(X0),n1))),
% 0.12/0.46 inference(forward_demodulation,[status(thm)],[f119,f229])).
% 0.12/0.46 fof(f231,plain,(
% 0.12/0.46 ![X0]: (p_Reset(X0)|~p_Wr(X0)|p_Rd(X0)|~gt(fifo_length,level(X0))|level(plus(X0,n1))=plus(level(X0),n1))),
% 0.12/0.46 inference(forward_demodulation,[status(thm)],[f119,f230])).
% 0.12/0.46 fof(f236,definition,(
% 0.12/0.46 sQ4_spl <=> (p_Reset(t_139))),
% 0.12/0.46 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 0.12/0.46 fof(f237,plain,(
% 0.12/0.46 p_Reset(t_139)|~sQ4_spl),
% 0.12/0.46 inference(component_clause,[status(thm)],[f236])).
% 0.12/0.46 fof(f239,definition,(
% 0.12/0.46 sQ5_spl <=> (p_Rd(t_139))),
% 0.12/0.46 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 0.12/0.46 fof(f240,plain,(
% 0.12/0.46 p_Rd(t_139)|~sQ5_spl),
% 0.12/0.46 inference(component_clause,[status(thm)],[f239])).
% 0.12/0.46 fof(f252,plain,(
% 0.12/0.46 minus(plus(level(t_139),n1),n1)=level(t_139)|def_10(n1,fifo_length)),
% 0.12/0.46 inference(paramodulation,[status(thm)],[f191,f197])).
% 0.12/0.46 fof(f255,definition,(
% 0.12/0.46 sQ8_spl <=> (minus(plus(level(t_139),n1),n1)=level(t_139))),
% 0.12/0.46 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 0.12/0.46 fof(f256,plain,(
% 0.12/0.46 minus(plus(level(t_139),n1),n1)=level(t_139)|~sQ8_spl),
% 0.12/0.46 inference(component_clause,[status(thm)],[f255])).
% 0.12/0.46 fof(f258,definition,(
% 0.12/0.46 sQ9_spl <=> (def_10(n1,fifo_length))),
% 0.12/0.46 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 0.12/0.46 fof(f259,plain,(
% 0.12/0.46 def_10(n1,fifo_length)|~sQ9_spl),
% 0.12/0.46 inference(component_clause,[status(thm)],[f258])).
% 0.12/0.46 fof(f261,plain,(
% 0.12/0.46 sQ8_spl|sQ9_spl),
% 0.12/0.46 inference(split_clause,[status(thm)],[f252,f255,f258])).
% 0.12/0.46 fof(f262,plain,(
% 0.12/0.46 minus(fifo_length,n1)=level(t_139)|~sQ8_spl),
% 0.12/0.46 inference(forward_demodulation,[status(thm)],[f191,f256])).
% 0.12/0.46 fof(f265,plain,(
% 0.12/0.46 ~gt(fifo_length,n1)|~sQ9_spl),
% 0.12/0.46 inference(resolution,[status(thm)],[f259,f103])).
% 0.12/0.46 fof(f332,definition,(
% 0.12/0.46 sQ22_spl <=> (p_Wr(t_139))),
% 0.12/0.46 introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition])).
% 0.12/0.46 fof(f334,plain,(
% 0.12/0.46 ~p_Wr(t_139)|sQ22_spl),
% 0.12/0.46 inference(component_clause,[status(thm)],[f332])).
% 0.12/0.46 fof(f336,plain,(
% 0.12/0.46 $false|~sQ4_spl),
% 0.12/0.46 inference(forward_subsumption_resolution,[status(thm)],[f237,f194])).
% 0.12/0.46 fof(f337,plain,(
% 0.12/0.46 ~sQ4_spl),
% 0.12/0.46 inference(contradiction_clause,[status(thm)],[f336])).
% 0.12/0.46 fof(f399,plain,(
% 0.12/0.46 $false|~sQ5_spl),
% 0.12/0.46 inference(forward_subsumption_resolution,[status(thm)],[f240,f192])).
% 0.12/0.46 fof(f400,plain,(
% 0.12/0.46 ~sQ5_spl),
% 0.12/0.46 inference(contradiction_clause,[status(thm)],[f399])).
% 0.12/0.46 fof(f401,plain,(
% 0.12/0.46 gt(fifo_length,level(t_139))|~sQ8_spl),
% 0.12/0.46 inference(backward_demodulation,[status(thm)],[f262,f209])).
% 0.12/0.46 fof(f404,plain,(
% 0.12/0.46 ![X0]: (~level(X0)=n0|p_Empty(X0))),
% 0.12/0.46 inference(forward_demodulation,[status(thm)],[f119,f122])).
% 0.12/0.46 fof(f407,plain,(
% 0.12/0.46 plus(n0,n1)=fifo_length|gt(fifo_length,plus(n0,n1))),
% 0.12/0.46 inference(resolution,[status(thm)],[f112,f207])).
% 0.12/0.46 fof(f421,definition,(
% 0.12/0.46 sQ31_spl <=> (plus(n0,n1)=fifo_length)),
% 0.12/0.46 introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition])).
% 0.12/0.46 fof(f422,plain,(
% 0.12/0.46 plus(n0,n1)=fifo_length|~sQ31_spl),
% 0.12/0.46 inference(component_clause,[status(thm)],[f421])).
% 0.12/0.46 fof(f424,definition,(
% 0.12/0.46 sQ32_spl <=> (gt(fifo_length,plus(n0,n1)))),
% 0.12/0.46 introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition])).
% 0.12/0.46 fof(f425,plain,(
% 0.12/0.46 gt(fifo_length,plus(n0,n1))|~sQ32_spl),
% 0.12/0.46 inference(component_clause,[status(thm)],[f424])).
% 0.12/0.46 fof(f427,plain,(
% 0.12/0.46 sQ31_spl|sQ32_spl),
% 0.12/0.46 inference(split_clause,[status(thm)],[f407,f421,f424])).
% 0.12/0.46 fof(f432,plain,(
% 0.12/0.46 n1=fifo_length|~sQ31_spl),
% 0.12/0.46 inference(forward_demodulation,[status(thm)],[f117,f422])).
% 0.12/0.46 fof(f433,plain,(
% 0.12/0.46 $false|sQ2_spl|~sQ31_spl),
% 0.12/0.46 inference(forward_subsumption_resolution,[status(thm)],[f432,f222])).
% 0.12/0.46 fof(f434,plain,(
% 0.12/0.46 sQ2_spl|~sQ31_spl),
% 0.12/0.46 inference(contradiction_clause,[status(thm)],[f433])).
% 0.12/0.46 fof(f435,plain,(
% 0.12/0.46 gt(fifo_length,n1)|~sQ32_spl),
% 0.12/0.46 inference(forward_demodulation,[status(thm)],[f117,f425])).
% 0.12/0.46 fof(f484,plain,(
% 0.12/0.46 ![X0]: (level(X0)=n0|~p_Empty(X0))),
% 0.12/0.46 inference(forward_demodulation,[status(thm)],[f119,f123])).
% 0.12/0.46 fof(f507,plain,(
% 0.12/0.46 ~n0=n0|p_Empty(t_139)|~sQ3_spl),
% 0.12/0.46 inference(paramodulation,[status(thm)],[f224,f404])).
% 0.12/0.46 fof(f512,definition,(
% 0.12/0.46 sQ38_spl <=> (p_Empty(t_139))),
% 0.12/0.46 introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition])).
% 0.12/0.46 fof(f513,plain,(
% 0.12/0.46 p_Empty(t_139)|~sQ38_spl),
% 0.12/0.46 inference(component_clause,[status(thm)],[f512])).
% 0.12/0.46 fof(f515,plain,(
% 0.12/0.46 ~sQ1_spl|sQ38_spl|~sQ3_spl),
% 0.12/0.46 inference(split_clause,[status(thm)],[f507,f216,f512,f223])).
% 0.12/0.46 fof(f520,plain,(
% 0.12/0.46 level(t_139)=n0|~sQ38_spl),
% 0.12/0.46 inference(resolution,[status(thm)],[f513,f484])).
% 0.12/0.46 fof(f628,plain,(
% 0.12/0.46 p_Reset(t_139)|~p_Wr(t_139)|p_Rd(t_139)|~gt(fifo_length,n0)|level(plus(t_139,n1))=plus(level(t_139),n1)|~sQ38_spl),
% 0.12/0.46 inference(paramodulation,[status(thm)],[f520,f231])).
% 0.12/0.46 fof(f633,definition,(
% 0.12/0.46 sQ50_spl <=> (gt(fifo_length,n0))),
% 0.12/0.46 introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition])).
% 0.12/0.46 fof(f635,plain,(
% 0.12/0.46 ~gt(fifo_length,n0)|sQ50_spl),
% 0.12/0.46 inference(component_clause,[status(thm)],[f633])).
% 0.12/0.46 fof(f636,definition,(
% 0.12/0.46 sQ51_spl <=> (level(plus(t_139,n1))=plus(level(t_139),n1))),
% 0.12/0.46 introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition])).
% 0.12/0.46 fof(f637,plain,(
% 0.12/0.46 level(plus(t_139,n1))=plus(level(t_139),n1)|~sQ51_spl),
% 0.12/0.46 inference(component_clause,[status(thm)],[f636])).
% 0.12/0.46 fof(f639,plain,(
% 0.12/0.46 sQ4_spl|~sQ22_spl|sQ5_spl|~sQ50_spl|sQ51_spl|~sQ38_spl),
% 0.12/0.46 inference(split_clause,[status(thm)],[f628,f236,f332,f239,f633,f636,f512])).
% 0.12/0.46 fof(f690,plain,(
% 0.12/0.46 $false|sQ22_spl),
% 0.12/0.46 inference(forward_subsumption_resolution,[status(thm)],[f334,f193])).
% 0.12/0.46 fof(f691,plain,(
% 0.12/0.46 sQ22_spl),
% 0.12/0.46 inference(contradiction_clause,[status(thm)],[f690])).
% 0.12/0.46 fof(f696,plain,(
% 0.12/0.46 ~gt(n1,n0)|~sQ31_spl|sQ50_spl),
% 0.12/0.48 inference(forward_demodulation,[status(thm)],[f432,f635])).
% 0.12/0.48 fof(f697,plain,(
% 0.12/0.48 $false|~sQ31_spl|sQ50_spl),
% 0.12/0.48 inference(forward_subsumption_resolution,[status(thm)],[f696,f206])).
% 0.12/0.48 fof(f698,plain,(
% 0.12/0.48 ~sQ31_spl|sQ50_spl),
% 0.12/0.48 inference(contradiction_clause,[status(thm)],[f697])).
% 0.12/0.48 fof(f816,plain,(
% 0.12/0.48 p_Reset(t_139)|~p_Wr(t_139)|p_Rd(t_139)|level(plus(t_139,n1))=plus(level(t_139),n1)|~sQ8_spl),
% 0.12/0.48 inference(resolution,[status(thm)],[f401,f231])).
% 0.12/0.48 fof(f823,plain,(
% 0.12/0.48 sQ4_spl|~sQ22_spl|sQ5_spl|sQ51_spl|~sQ8_spl),
% 0.12/0.48 inference(split_clause,[status(thm)],[f816,f236,f332,f239,f636,f255])).
% 0.12/0.48 fof(f844,plain,(
% 0.12/0.48 $false|~sQ32_spl|~sQ9_spl),
% 0.12/0.48 inference(forward_subsumption_resolution,[status(thm)],[f265,f435])).
% 0.12/0.48 fof(f845,plain,(
% 0.12/0.48 ~sQ32_spl|~sQ9_spl),
% 0.12/0.48 inference(contradiction_clause,[status(thm)],[f844])).
% 0.12/0.48 fof(f846,plain,(
% 0.12/0.48 level(plus(t_139,n1))=fifo_length|~sQ51_spl),
% 0.12/0.48 inference(forward_demodulation,[status(thm)],[f191,f637])).
% 0.12/0.48 fof(f847,plain,(
% 0.12/0.48 $false|~sQ51_spl),
% 0.12/0.48 inference(forward_subsumption_resolution,[status(thm)],[f846,f195])).
% 0.12/0.48 fof(f848,plain,(
% 0.12/0.48 ~sQ51_spl),
% 0.12/0.48 inference(contradiction_clause,[status(thm)],[f847])).
% 0.12/0.48 fof(f849,plain,(
% 0.12/0.48 $false),
% 0.12/0.48 inference(sat_refutation,[status(thm)],[f219,f226,f228,f261,f337,f400,f427,f434,f515,f639,f691,f698,f823,f845,f848])).
% 0.12/0.48 % SZS output end CNFRefutation for theBenchmark.p
% 0.12/0.48 % Elapsed time: 0.124587 seconds
% 0.12/0.48 % CPU time: 0.616395 seconds
% 0.12/0.48 % Total memory used: 114.304 MB
% 0.12/0.48 % Net memory used: 112.935 MB
%------------------------------------------------------------------------------