%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : HWV025-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 : n008.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:43 PM UTC 2026
% Result : Unsatisfiable 0.14s 0.39s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : HWV025-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.09/0.35 % Computer : n008.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Sun Sep 20 20:49:39 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.14/0.37 % Drodi V4.1.1
% 0.14/0.39 % Refutation found
% 0.14/0.39 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.14/0.39 % SZS output start CNFRefutation for theBenchmark
% 0.14/0.39 fof(f15,axiom,(
% 0.14/0.39 (![X_25]: (( X_25 = n0| gt(X_25,n0) ) ))),
% 0.14/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.39 fof(f18,axiom,(
% 0.14/0.39 (![X_29,Y_30]: (( plus(X_29,n1) != plus(Y_30,n1)| X_29 = Y_30 ) ))),
% 0.14/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.39 fof(f19,axiom,(
% 0.14/0.39 (![X_31]: (plus(n0,X_31) = X_31 ))),
% 0.14/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.39 fof(f22,axiom,(
% 0.14/0.39 (![X_t_33]: (( int_level(X_t_33) != fifo_length| p_Full(X_t_33) ) ))),
% 0.14/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.39 fof(f23,axiom,(
% 0.14/0.39 (![X_t_34]: (( int_level(X_t_34) = fifo_length| ~ p_Full(X_t_34) ) ))),
% 0.14/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.39 fof(f24,axiom,(
% 0.14/0.39 (![X_t_35]: (( int_level(X_t_35) != n0| p_Empty(X_t_35) ) ))),
% 0.14/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.39 fof(f30,axiom,(
% 0.14/0.39 (![X_t_37]: (( ~ p_Reset(X_t_37)| ~ p_Rd_error(plus(X_t_37,n1)) ) ))),
% 0.14/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.39 fof(f49,axiom,(
% 0.14/0.39 (![X_t_42]: (( p_Reset(X_t_42)| ~ p_Wr(X_t_42)| p_Rd(X_t_42)| ~ p_Rd_error(plus(X_t_42,n1))| p_Rd_error(X_t_42) ) ))),
% 0.14/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.39 fof(f50,axiom,(
% 0.14/0.39 (![X_t_42]: (( p_Reset(X_t_42)| ~ p_Wr(X_t_42)| p_Rd(X_t_42)| p_Rd_error(plus(X_t_42,n1))| ~ p_Rd_error(X_t_42) ) ))),
% 0.14/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.39 fof(f52,axiom,(
% 0.14/0.39 (![X_t_42]: (( p_Reset(X_t_42)| ~ p_Wr(X_t_42)| ~ p_Rd(X_t_42)| ~ gt(int_level(X_t_42),n0)| ~ p_Rd_error(plus(X_t_42,n1)) ) ))),
% 0.14/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.39 fof(f58,axiom,(
% 0.14/0.39 (![X_t_42]: (( p_Reset(X_t_42)| ~ p_Wr(X_t_42)| ~ p_Rd(X_t_42)| gt(int_level(X_t_42),n0)| p_Rd_error(plus(X_t_42,n1)) ) ))),
% 0.14/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.39 fof(f70,axiom,(
% 0.14/0.39 (![X_t_42]: (( p_Reset(X_t_42)| p_Wr(X_t_42)| ~ p_Rd(X_t_42)| ~ gt(int_level(X_t_42),n0)| ~ p_Rd_error(plus(X_t_42,n1)) ) ))),
% 0.14/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.39 fof(f76,axiom,(
% 0.14/0.39 (![X_t_42]: (( p_Reset(X_t_42)| p_Wr(X_t_42)| ~ p_Rd(X_t_42)| gt(int_level(X_t_42),n0)| p_Rd_error(plus(X_t_42,n1)) ) ))),
% 0.14/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.39 fof(f82,axiom,(
% 0.14/0.39 (![X_t_42]: (( p_Reset(X_t_42)| p_Wr(X_t_42)| p_Rd(X_t_42)| int_level(plus(X_t_42,n1)) = int_level(X_t_42) ) ))),
% 0.14/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.39 fof(f85,axiom,(
% 0.14/0.39 (![X_t_42]: (( p_Reset(X_t_42)| p_Wr(X_t_42)| p_Rd(X_t_42)| ~ p_Rd_error(plus(X_t_42,n1))| p_Rd_error(X_t_42) ) ))),
% 0.14/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.39 fof(f86,axiom,(
% 0.14/0.39 (![X_t_42]: (( p_Reset(X_t_42)| p_Wr(X_t_42)| p_Rd(X_t_42)| p_Rd_error(plus(X_t_42,n1))| ~ p_Rd_error(X_t_42) ) ))),
% 0.14/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.39 fof(f91,negated_conjecture,(
% 0.14/0.39 ~ p_Rd(t_139) ),
% 0.14/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.39 fof(f92,negated_conjecture,(
% 0.14/0.39 ~ p_Reset(t_139) ),
% 0.14/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.39 fof(f93,negated_conjecture,(
% 0.14/0.39 ( ~ p_Rd_error(t_139)| ~ p_Rd_error(plus(t_139,n1)) ) ),
% 0.14/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.39 fof(f94,negated_conjecture,(
% 0.14/0.39 ( p_Rd_error(t_139)| p_Rd_error(plus(t_139,n1)) ) ),
% 0.14/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.39 fof(f112,plain,(
% 0.14/0.39 ![X0]: (X0=n0|gt(X0,n0))),
% 0.14/0.39 inference(cnf_transformation,[status(thm)],[f15])).
% 0.14/0.39 fof(f115,plain,(
% 0.14/0.39 ![X0,X1]: (~plus(X0,n1)=plus(X1,n1)|X0=X1)),
% 0.14/0.39 inference(cnf_transformation,[status(thm)],[f18])).
% 0.14/0.39 fof(f116,plain,(
% 0.14/0.39 ![X0]: (plus(n0,X0)=X0)),
% 0.14/0.39 inference(cnf_transformation,[status(thm)],[f19])).
% 0.14/0.39 fof(f119,plain,(
% 0.14/0.39 ![X0]: (~int_level(X0)=fifo_length|p_Full(X0))),
% 0.14/0.39 inference(cnf_transformation,[status(thm)],[f22])).
% 0.14/0.39 fof(f120,plain,(
% 0.14/0.39 ![X0]: (int_level(X0)=fifo_length|~p_Full(X0))),
% 0.14/0.39 inference(cnf_transformation,[status(thm)],[f23])).
% 0.14/0.39 fof(f121,plain,(
% 0.14/0.39 ![X0]: (~int_level(X0)=n0|p_Empty(X0))),
% 0.14/0.39 inference(cnf_transformation,[status(thm)],[f24])).
% 0.14/0.39 fof(f127,plain,(
% 0.14/0.39 ![X0]: (~p_Reset(X0)|~p_Rd_error(plus(X0,n1)))),
% 0.14/0.39 inference(cnf_transformation,[status(thm)],[f30])).
% 0.14/0.39 fof(f148,plain,(
% 0.14/0.39 ![X0]: (p_Reset(X0)|~p_Wr(X0)|p_Rd(X0)|~p_Rd_error(plus(X0,n1))|p_Rd_error(X0))),
% 0.14/0.39 inference(cnf_transformation,[status(thm)],[f49])).
% 0.14/0.39 fof(f149,plain,(
% 0.14/0.39 ![X0]: (p_Reset(X0)|~p_Wr(X0)|p_Rd(X0)|p_Rd_error(plus(X0,n1))|~p_Rd_error(X0))),
% 0.14/0.39 inference(cnf_transformation,[status(thm)],[f50])).
% 0.14/0.39 fof(f151,plain,(
% 0.14/0.39 ![X0]: (p_Reset(X0)|~p_Wr(X0)|~p_Rd(X0)|~gt(int_level(X0),n0)|~p_Rd_error(plus(X0,n1)))),
% 0.14/0.39 inference(cnf_transformation,[status(thm)],[f52])).
% 0.14/0.39 fof(f157,plain,(
% 0.14/0.39 ![X0]: (p_Reset(X0)|~p_Wr(X0)|~p_Rd(X0)|gt(int_level(X0),n0)|p_Rd_error(plus(X0,n1)))),
% 0.14/0.39 inference(cnf_transformation,[status(thm)],[f58])).
% 0.14/0.39 fof(f169,plain,(
% 0.14/0.39 ![X0]: (p_Reset(X0)|p_Wr(X0)|~p_Rd(X0)|~gt(int_level(X0),n0)|~p_Rd_error(plus(X0,n1)))),
% 0.14/0.39 inference(cnf_transformation,[status(thm)],[f70])).
% 0.14/0.39 fof(f175,plain,(
% 0.14/0.39 ![X0]: (p_Reset(X0)|p_Wr(X0)|~p_Rd(X0)|gt(int_level(X0),n0)|p_Rd_error(plus(X0,n1)))),
% 0.14/0.39 inference(cnf_transformation,[status(thm)],[f76])).
% 0.14/0.39 fof(f181,plain,(
% 0.14/0.39 ![X0]: (p_Reset(X0)|p_Wr(X0)|p_Rd(X0)|int_level(plus(X0,n1))=int_level(X0))),
% 0.14/0.39 inference(cnf_transformation,[status(thm)],[f82])).
% 0.14/0.39 fof(f184,plain,(
% 0.14/0.39 ![X0]: (p_Reset(X0)|p_Wr(X0)|p_Rd(X0)|~p_Rd_error(plus(X0,n1))|p_Rd_error(X0))),
% 0.14/0.39 inference(cnf_transformation,[status(thm)],[f85])).
% 0.14/0.39 fof(f185,plain,(
% 0.14/0.39 ![X0]: (p_Reset(X0)|p_Wr(X0)|p_Rd(X0)|p_Rd_error(plus(X0,n1))|~p_Rd_error(X0))),
% 0.14/0.39 inference(cnf_transformation,[status(thm)],[f86])).
% 0.14/0.39 fof(f190,plain,(
% 0.14/0.39 ~p_Rd(t_139)),
% 0.14/0.39 inference(cnf_transformation,[status(thm)],[f91])).
% 0.14/0.39 fof(f191,plain,(
% 0.14/0.39 ~p_Reset(t_139)),
% 0.14/0.39 inference(cnf_transformation,[status(thm)],[f92])).
% 0.14/0.39 fof(f192,plain,(
% 0.14/0.39 ~p_Rd_error(t_139)|~p_Rd_error(plus(t_139,n1))),
% 0.14/0.39 inference(cnf_transformation,[status(thm)],[f93])).
% 0.14/0.39 fof(f193,plain,(
% 0.14/0.39 p_Rd_error(t_139)|p_Rd_error(plus(t_139,n1))),
% 0.14/0.39 inference(cnf_transformation,[status(thm)],[f94])).
% 0.14/0.39 fof(f194,definition,(
% 0.14/0.39 sQ0_spl <=> (p_Rd_error(t_139))),
% 0.14/0.39 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.14/0.39 fof(f195,plain,(
% 0.14/0.39 p_Rd_error(t_139)|~sQ0_spl),
% 0.14/0.39 inference(component_clause,[status(thm)],[f194])).
% 0.14/0.39 fof(f197,definition,(
% 0.14/0.39 sQ1_spl <=> (p_Rd_error(plus(t_139,n1)))),
% 0.14/0.39 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 0.14/0.39 fof(f198,plain,(
% 0.14/0.39 p_Rd_error(plus(t_139,n1))|~sQ1_spl),
% 0.14/0.39 inference(component_clause,[status(thm)],[f197])).
% 0.14/0.39 fof(f200,plain,(
% 0.14/0.39 ~sQ0_spl|~sQ1_spl),
% 0.14/0.39 inference(split_clause,[status(thm)],[f192,f194,f197])).
% 0.14/0.39 fof(f201,plain,(
% 0.14/0.39 sQ0_spl|sQ1_spl),
% 0.14/0.39 inference(split_clause,[status(thm)],[f193,f194,f197])).
% 0.14/0.39 fof(f206,plain,(
% 0.14/0.39 ![X0]: (~p_Wr(X0)|p_Rd(X0)|~p_Rd_error(plus(X0,n1))|p_Rd_error(X0))),
% 0.14/0.39 inference(forward_subsumption_resolution,[status(thm)],[f148,f127])).
% 0.14/0.39 fof(f208,definition,(
% 0.14/0.39 sQ2_spl <=> (p_Reset(t_139))),
% 0.14/0.39 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.14/0.39 fof(f209,plain,(
% 0.14/0.39 p_Reset(t_139)|~sQ2_spl),
% 0.14/0.39 inference(component_clause,[status(thm)],[f208])).
% 0.14/0.40 fof(f211,definition,(
% 0.14/0.40 sQ3_spl <=> (p_Wr(t_139))),
% 0.14/0.40 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 0.14/0.40 fof(f214,definition,(
% 0.14/0.40 sQ4_spl <=> (p_Rd(t_139))),
% 0.14/0.40 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 0.14/0.40 fof(f215,plain,(
% 0.14/0.40 p_Rd(t_139)|~sQ4_spl),
% 0.14/0.40 inference(component_clause,[status(thm)],[f214])).
% 0.14/0.40 fof(f218,plain,(
% 0.14/0.40 ~p_Wr(t_139)|p_Rd(t_139)|p_Rd_error(t_139)|~sQ1_spl),
% 0.14/0.40 inference(resolution,[status(thm)],[f198,f206])).
% 0.14/0.40 fof(f221,plain,(
% 0.14/0.40 ~sQ3_spl|sQ4_spl|sQ0_spl|~sQ1_spl),
% 0.14/0.40 inference(split_clause,[status(thm)],[f218,f211,f214,f194,f197])).
% 0.14/0.40 fof(f228,definition,(
% 0.14/0.40 sQ7_spl <=> (p_Rd(plus(t_139,n1)))),
% 0.14/0.40 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 0.14/0.40 fof(f231,definition,(
% 0.14/0.40 sQ8_spl <=> (p_Rd_error(plus(plus(t_139,n1),n1)))),
% 0.14/0.40 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 0.14/0.40 fof(f235,plain,(
% 0.14/0.40 $false|~sQ4_spl),
% 0.14/0.40 inference(forward_subsumption_resolution,[status(thm)],[f215,f190])).
% 0.14/0.40 fof(f236,plain,(
% 0.14/0.40 ~sQ4_spl),
% 0.14/0.40 inference(contradiction_clause,[status(thm)],[f235])).
% 0.14/0.40 fof(f239,plain,(
% 0.14/0.40 p_Wr(t_139)|p_Rd(t_139)|int_level(plus(t_139,n1))=int_level(t_139)),
% 0.14/0.40 inference(resolution,[status(thm)],[f181,f191])).
% 0.14/0.40 fof(f240,definition,(
% 0.14/0.40 sQ9_spl <=> (int_level(plus(t_139,n1))=int_level(t_139))),
% 0.14/0.40 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 0.14/0.40 fof(f241,plain,(
% 0.14/0.40 int_level(plus(t_139,n1))=int_level(t_139)|~sQ9_spl),
% 0.14/0.40 inference(component_clause,[status(thm)],[f240])).
% 0.14/0.40 fof(f243,plain,(
% 0.14/0.40 sQ3_spl|sQ4_spl|sQ9_spl),
% 0.14/0.40 inference(split_clause,[status(thm)],[f239,f211,f214,f240])).
% 0.14/0.40 fof(f244,plain,(
% 0.14/0.40 $false|~sQ2_spl),
% 0.14/0.40 inference(forward_subsumption_resolution,[status(thm)],[f209,f191])).
% 0.14/0.40 fof(f245,plain,(
% 0.14/0.40 ~sQ2_spl),
% 0.14/0.40 inference(contradiction_clause,[status(thm)],[f244])).
% 0.14/0.40 fof(f246,plain,(
% 0.14/0.40 ![X0]: (~p_Wr(X0)|~p_Rd(X0)|~gt(int_level(X0),n0)|~p_Rd_error(plus(X0,n1)))),
% 0.14/0.40 inference(forward_subsumption_resolution,[status(thm)],[f151,f127])).
% 0.14/0.40 fof(f248,definition,(
% 0.14/0.40 sQ10_spl <=> (gt(int_level(t_139),n0))),
% 0.14/0.40 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 0.14/0.40 fof(f249,plain,(
% 0.14/0.40 gt(int_level(t_139),n0)|~sQ10_spl),
% 0.14/0.40 inference(component_clause,[status(thm)],[f248])).
% 0.14/0.40 fof(f250,plain,(
% 0.14/0.40 ~gt(int_level(t_139),n0)|sQ10_spl),
% 0.14/0.40 inference(component_clause,[status(thm)],[f248])).
% 0.14/0.40 fof(f252,plain,(
% 0.14/0.40 ~p_Wr(n0)|p_Rd(n0)|~p_Rd_error(n1)|p_Rd_error(n0)),
% 0.14/0.40 inference(paramodulation,[status(thm)],[f116,f206])).
% 0.14/0.40 fof(f253,plain,(
% 0.14/0.40 ![X0]: (~plus(X0,n1)=n1|X0=n0)),
% 0.14/0.40 inference(paramodulation,[status(thm)],[f116,f115])).
% 0.14/0.40 fof(f255,plain,(
% 0.14/0.40 ~p_Reset(n0)|~p_Rd_error(n1)),
% 0.14/0.40 inference(paramodulation,[status(thm)],[f116,f127])).
% 0.14/0.40 fof(f256,definition,(
% 0.14/0.40 sQ11_spl <=> (p_Wr(n0))),
% 0.14/0.40 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 0.14/0.40 fof(f257,plain,(
% 0.14/0.40 p_Wr(n0)|~sQ11_spl),
% 0.14/0.40 inference(component_clause,[status(thm)],[f256])).
% 0.14/0.40 fof(f259,definition,(
% 0.14/0.40 sQ12_spl <=> (p_Rd(n0))),
% 0.14/0.40 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 0.14/0.40 fof(f260,plain,(
% 0.14/0.40 p_Rd(n0)|~sQ12_spl),
% 0.14/0.40 inference(component_clause,[status(thm)],[f259])).
% 0.14/0.40 fof(f262,definition,(
% 0.14/0.40 sQ13_spl <=> (p_Rd_error(n1))),
% 0.14/0.40 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 0.14/0.40 fof(f264,plain,(
% 0.14/0.40 ~p_Rd_error(n1)|sQ13_spl),
% 0.14/0.40 inference(component_clause,[status(thm)],[f262])).
% 0.14/0.40 fof(f265,definition,(
% 0.14/0.40 sQ14_spl <=> (p_Rd_error(n0))),
% 0.14/0.40 introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 0.14/0.40 fof(f266,plain,(
% 0.14/0.40 p_Rd_error(n0)|~sQ14_spl),
% 0.14/0.40 inference(component_clause,[status(thm)],[f265])).
% 0.14/0.40 fof(f268,plain,(
% 0.14/0.40 ~sQ11_spl|sQ12_spl|~sQ13_spl|sQ14_spl),
% 0.14/0.40 inference(split_clause,[status(thm)],[f252,f256,f259,f262,f265])).
% 0.14/0.40 fof(f269,definition,(
% 0.14/0.40 sQ15_spl <=> (p_Reset(n0))),
% 0.14/0.40 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 0.14/0.40 fof(f271,plain,(
% 0.14/0.40 ~p_Reset(n0)|sQ15_spl),
% 0.14/0.40 inference(component_clause,[status(thm)],[f269])).
% 0.14/0.40 fof(f272,plain,(
% 0.14/0.40 ~sQ15_spl|~sQ13_spl),
% 0.14/0.40 inference(split_clause,[status(thm)],[f255,f269,f262])).
% 0.14/0.40 fof(f274,plain,(
% 0.14/0.40 ![X0]: (int_level(X0)=n0|~p_Wr(X0)|~p_Rd(X0)|~p_Rd_error(plus(X0,n1)))),
% 0.14/0.40 inference(resolution,[status(thm)],[f112,f246])).
% 0.14/0.40 fof(f277,plain,(
% 0.14/0.40 ~int_level(t_139)=fifo_length|p_Full(plus(t_139,n1))|~sQ9_spl),
% 0.14/0.40 inference(paramodulation,[status(thm)],[f241,f119])).
% 0.14/0.40 fof(f278,definition,(
% 0.14/0.40 sQ16_spl <=> (int_level(t_139)=fifo_length)),
% 0.14/0.40 introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition])).
% 0.14/0.40 fof(f280,plain,(
% 0.14/0.40 ~int_level(t_139)=fifo_length|sQ16_spl),
% 0.14/0.40 inference(component_clause,[status(thm)],[f278])).
% 0.14/0.40 fof(f281,definition,(
% 0.14/0.40 sQ17_spl <=> (p_Full(plus(t_139,n1)))),
% 0.14/0.40 introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 0.14/0.40 fof(f284,plain,(
% 0.14/0.40 ~sQ16_spl|sQ17_spl|~sQ9_spl),
% 0.14/0.40 inference(split_clause,[status(thm)],[f277,f278,f281,f240])).
% 0.14/0.40 fof(f285,plain,(
% 0.14/0.40 ~int_level(t_139)=n0|p_Empty(plus(t_139,n1))|~sQ9_spl),
% 0.14/0.40 inference(paramodulation,[status(thm)],[f241,f121])).
% 0.14/0.40 fof(f286,definition,(
% 0.14/0.40 sQ18_spl <=> (int_level(t_139)=n0)),
% 0.14/0.40 introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition])).
% 0.14/0.40 fof(f287,plain,(
% 0.14/0.40 int_level(t_139)=n0|~sQ18_spl),
% 0.14/0.40 inference(component_clause,[status(thm)],[f286])).
% 0.14/0.40 fof(f288,plain,(
% 0.14/0.40 ~int_level(t_139)=n0|sQ18_spl),
% 0.14/0.40 inference(component_clause,[status(thm)],[f286])).
% 0.14/0.40 fof(f289,definition,(
% 0.14/0.40 sQ19_spl <=> (p_Empty(plus(t_139,n1)))),
% 0.14/0.40 introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition])).
% 0.14/0.40 fof(f292,plain,(
% 0.14/0.40 ~sQ18_spl|sQ19_spl|~sQ9_spl),
% 0.14/0.40 inference(split_clause,[status(thm)],[f285,f286,f289,f240])).
% 0.14/0.40 fof(f299,plain,(
% 0.14/0.40 ~n1=n1|n0=n0),
% 0.14/0.40 inference(paramodulation,[status(thm)],[f116,f253])).
% 0.14/0.40 fof(f300,definition,(
% 0.14/0.40 sQ20_spl <=> (n1=n1)),
% 0.14/0.40 introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition])).
% 0.14/0.40 fof(f302,plain,(
% 0.14/0.40 ~n1=n1|sQ20_spl),
% 0.14/0.40 inference(component_clause,[status(thm)],[f300])).
% 0.14/0.40 fof(f303,definition,(
% 0.14/0.40 sQ21_spl <=> (n0=n0)),
% 0.14/0.40 introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition])).
% 0.14/0.40 fof(f306,plain,(
% 0.14/0.40 ~sQ20_spl|sQ21_spl),
% 0.14/0.40 inference(split_clause,[status(thm)],[f299,f300,f303])).
% 0.14/0.40 fof(f307,plain,(
% 0.14/0.40 $false|sQ20_spl),
% 0.14/0.40 inference(trivial_equality_resolution,[status(thm)],[f302])).
% 0.14/0.40 fof(f308,plain,(
% 0.14/0.40 sQ20_spl),
% 0.14/0.40 inference(contradiction_clause,[status(thm)],[f307])).
% 0.14/0.40 fof(f309,plain,(
% 0.14/0.40 int_level(n0)=n0|~p_Wr(n0)|~p_Rd(n0)|~p_Rd_error(n1)),
% 0.14/0.40 inference(paramodulation,[status(thm)],[f116,f274])).
% 0.14/0.40 fof(f310,definition,(
% 0.14/0.40 sQ22_spl <=> (int_level(n0)=n0)),
% 0.14/0.40 introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition])).
% 0.14/0.40 fof(f311,plain,(
% 0.14/0.40 int_level(n0)=n0|~sQ22_spl),
% 0.14/0.40 inference(component_clause,[status(thm)],[f310])).
% 0.14/0.40 fof(f313,plain,(
% 0.14/0.40 sQ22_spl|~sQ11_spl|~sQ12_spl|~sQ13_spl),
% 0.14/0.40 inference(split_clause,[status(thm)],[f309,f310,f256,f259,f262])).
% 0.14/0.40 fof(f314,plain,(
% 0.14/0.40 ![X0]: (~p_Rd(X0)|~gt(int_level(X0),n0)|~p_Rd_error(plus(X0,n1)))),
% 0.14/0.40 inference(backward_subsumption_resolution,[status(thm)],[f246,f315])).
% 0.14/0.40 fof(f315,plain,(
% 0.14/0.40 ![X0]: (p_Wr(X0)|~p_Rd(X0)|~gt(int_level(X0),n0)|~p_Rd_error(plus(X0,n1)))),
% 0.14/0.40 inference(forward_subsumption_resolution,[status(thm)],[f169,f127])).
% 0.14/0.40 fof(f320,plain,(
% 0.14/0.40 int_level(t_139)=n0|sQ10_spl),
% 0.14/0.40 inference(resolution,[status(thm)],[f250,f112])).
% 0.14/0.40 fof(f321,plain,(
% 0.14/0.40 $false|sQ18_spl|sQ10_spl),
% 0.14/0.40 inference(forward_subsumption_resolution,[status(thm)],[f320,f288])).
% 0.14/0.40 fof(f322,plain,(
% 0.14/0.40 sQ18_spl|sQ10_spl),
% 0.14/0.40 inference(contradiction_clause,[status(thm)],[f321])).
% 0.14/0.40 fof(f323,plain,(
% 0.14/0.40 p_Wr(n0)|p_Rd(n0)|int_level(plus(n0,n1))=int_level(n0)|sQ15_spl),
% 0.14/0.40 inference(resolution,[status(thm)],[f271,f181])).
% 0.14/0.40 fof(f324,definition,(
% 0.14/0.40 sQ23_spl <=> (int_level(plus(n0,n1))=int_level(n0))),
% 0.14/0.40 introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition])).
% 0.14/0.40 fof(f327,plain,(
% 0.14/0.40 sQ11_spl|sQ12_spl|sQ23_spl|sQ15_spl),
% 0.14/0.40 inference(split_clause,[status(thm)],[f323,f256,f259,f324,f269])).
% 0.14/0.40 fof(f329,plain,(
% 0.14/0.40 p_Reset(n0)|~p_Wr(n0)|p_Rd(n0)|p_Rd_error(plus(n0,n1))|~sQ14_spl),
% 0.14/0.40 inference(resolution,[status(thm)],[f266,f149])).
% 0.14/0.40 fof(f330,definition,(
% 0.14/0.40 sQ24_spl <=> (p_Rd_error(plus(n0,n1)))),
% 0.14/0.40 introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition])).
% 0.14/0.40 fof(f331,plain,(
% 0.14/0.40 p_Rd_error(plus(n0,n1))|~sQ24_spl),
% 0.14/0.40 inference(component_clause,[status(thm)],[f330])).
% 0.14/0.40 fof(f333,plain,(
% 0.14/0.40 sQ15_spl|~sQ11_spl|sQ12_spl|sQ24_spl|~sQ14_spl),
% 0.14/0.40 inference(split_clause,[status(thm)],[f329,f269,f256,f259,f330,f265])).
% 0.14/0.40 fof(f334,plain,(
% 0.14/0.40 p_Rd_error(n1)|~sQ24_spl),
% 0.14/0.40 inference(forward_demodulation,[status(thm)],[f116,f331])).
% 0.14/0.40 fof(f335,plain,(
% 0.14/0.40 $false|sQ13_spl|~sQ24_spl),
% 0.14/0.40 inference(forward_subsumption_resolution,[status(thm)],[f334,f264])).
% 0.14/0.40 fof(f336,plain,(
% 0.14/0.40 sQ13_spl|~sQ24_spl),
% 0.14/0.40 inference(contradiction_clause,[status(thm)],[f335])).
% 0.14/0.40 fof(f352,plain,(
% 0.14/0.40 ![X0]: (p_Reset(X0)|~p_Rd(X0)|gt(int_level(X0),n0)|p_Rd_error(plus(X0,n1)))),
% 0.14/0.40 inference(forward_subsumption_resolution,[status(thm)],[f175,f157])).
% 0.14/0.40 fof(f354,plain,(
% 0.14/0.40 p_Reset(n0)|gt(int_level(n0),n0)|p_Rd_error(plus(n0,n1))|~sQ12_spl),
% 0.14/0.40 inference(resolution,[status(thm)],[f352,f260])).
% 0.14/0.40 fof(f359,definition,(
% 0.14/0.40 sQ30_spl <=> (gt(int_level(n0),n0))),
% 0.14/0.40 introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition])).
% 0.14/0.40 fof(f362,plain,(
% 0.14/0.40 sQ15_spl|sQ30_spl|sQ24_spl|~sQ12_spl),
% 0.14/0.40 inference(split_clause,[status(thm)],[f354,f269,f359,f330,f259])).
% 0.14/0.40 fof(f364,plain,(
% 0.14/0.40 ![X0]: (p_Wr(X0)|p_Rd(X0)|~p_Rd_error(plus(X0,n1))|p_Rd_error(X0))),
% 0.14/0.40 inference(forward_subsumption_resolution,[status(thm)],[f184,f127])).
% 0.14/0.40 fof(f365,plain,(
% 0.14/0.40 p_Wr(n0)|p_Rd(n0)|~p_Rd_error(n1)|p_Rd_error(n0)),
% 0.14/0.40 inference(paramodulation,[status(thm)],[f116,f364])).
% 0.14/0.40 fof(f366,plain,(
% 0.14/0.40 sQ11_spl|sQ12_spl|~sQ13_spl|sQ14_spl),
% 0.14/0.40 inference(split_clause,[status(thm)],[f365,f256,f259,f262,f265])).
% 0.14/0.40 fof(f372,plain,(
% 0.14/0.40 p_Wr(n0)|~p_Rd(n0)|~gt(n0,n0)|~p_Rd_error(plus(n0,n1))|~sQ22_spl),
% 0.14/0.40 inference(paramodulation,[status(thm)],[f311,f315])).
% 0.14/0.40 fof(f373,plain,(
% 0.14/0.40 ~n0=n0|p_Empty(n0)|~sQ22_spl),
% 0.14/0.40 inference(paramodulation,[status(thm)],[f311,f121])).
% 0.14/0.40 fof(f374,plain,(
% 0.14/0.40 ~n0=fifo_length|p_Full(n0)|~sQ22_spl),
% 0.14/0.40 inference(paramodulation,[status(thm)],[f311,f119])).
% 0.14/0.40 fof(f375,definition,(
% 0.14/0.40 sQ31_spl <=> (gt(n0,n0))),
% 0.14/0.40 introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition])).
% 0.14/0.40 fof(f378,plain,(
% 0.14/0.40 sQ11_spl|~sQ12_spl|~sQ31_spl|~sQ24_spl|~sQ22_spl),
% 0.14/0.40 inference(split_clause,[status(thm)],[f372,f256,f259,f375,f330,f310])).
% 0.14/0.40 fof(f379,definition,(
% 0.14/0.40 sQ32_spl <=> (p_Empty(n0))),
% 0.14/0.40 introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition])).
% 0.14/0.40 fof(f382,plain,(
% 0.14/0.40 ~sQ21_spl|sQ32_spl|~sQ22_spl),
% 0.14/0.40 inference(split_clause,[status(thm)],[f373,f303,f379,f310])).
% 0.14/0.40 fof(f383,definition,(
% 0.14/0.40 sQ33_spl <=> (n0=fifo_length)),
% 0.14/0.40 introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition])).
% 0.14/0.40 fof(f384,plain,(
% 0.14/0.40 n0=fifo_length|~sQ33_spl),
% 0.14/0.40 inference(component_clause,[status(thm)],[f383])).
% 0.14/0.40 fof(f385,plain,(
% 0.14/0.40 ~n0=fifo_length|sQ33_spl),
% 0.14/0.40 inference(component_clause,[status(thm)],[f383])).
% 0.14/0.40 fof(f386,definition,(
% 0.14/0.40 sQ34_spl <=> (p_Full(n0))),
% 0.14/0.40 introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition])).
% 0.14/0.40 fof(f387,plain,(
% 0.14/0.40 p_Full(n0)|~sQ34_spl),
% 0.14/0.40 inference(component_clause,[status(thm)],[f386])).
% 0.14/0.40 fof(f389,plain,(
% 0.14/0.40 ~sQ33_spl|sQ34_spl|~sQ22_spl),
% 0.14/0.40 inference(split_clause,[status(thm)],[f374,f383,f386,f310])).
% 0.14/0.40 fof(f390,plain,(
% 0.14/0.40 int_level(n0)=fifo_length|~sQ34_spl),
% 0.14/0.40 inference(resolution,[status(thm)],[f387,f120])).
% 0.14/0.40 fof(f394,plain,(
% 0.14/0.40 p_Wr(n0)|~p_Rd(n0)|~gt(fifo_length,n0)|~p_Rd_error(plus(n0,n1))|~sQ34_spl),
% 0.14/0.40 inference(paramodulation,[status(thm)],[f390,f315])).
% 0.14/0.40 fof(f395,plain,(
% 0.14/0.40 ~fifo_length=n0|p_Empty(n0)|~sQ34_spl),
% 0.14/0.40 inference(paramodulation,[status(thm)],[f390,f121])).
% 0.14/0.40 fof(f397,definition,(
% 0.14/0.40 sQ35_spl <=> (gt(fifo_length,n0))),
% 0.14/0.40 introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition])).
% 0.14/0.40 fof(f399,plain,(
% 0.14/0.40 ~gt(fifo_length,n0)|sQ35_spl),
% 0.14/0.40 inference(component_clause,[status(thm)],[f397])).
% 0.14/0.40 fof(f400,plain,(
% 0.14/0.40 sQ11_spl|~sQ12_spl|~sQ35_spl|~sQ24_spl|~sQ34_spl),
% 0.14/0.40 inference(split_clause,[status(thm)],[f394,f256,f259,f397,f330,f386])).
% 0.14/0.40 fof(f401,plain,(
% 0.14/0.40 ~sQ33_spl|sQ32_spl|~sQ34_spl),
% 0.14/0.40 inference(split_clause,[status(thm)],[f395,f383,f379,f386])).
% 0.14/0.40 fof(f402,definition,(
% 0.14/0.40 sQ36_spl <=> (fifo_length=fifo_length)),
% 0.14/0.40 introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition])).
% 0.14/0.40 fof(f404,plain,(
% 0.14/0.40 ~fifo_length=fifo_length|sQ36_spl),
% 0.14/0.40 inference(component_clause,[status(thm)],[f402])).
% 0.14/0.40 fof(f406,plain,(
% 0.14/0.40 fifo_length=n0|sQ35_spl),
% 0.14/0.40 inference(resolution,[status(thm)],[f399,f112])).
% 0.14/0.40 fof(f407,plain,(
% 0.14/0.40 $false|sQ33_spl|sQ35_spl),
% 0.14/0.40 inference(forward_subsumption_resolution,[status(thm)],[f406,f385])).
% 0.14/0.40 fof(f408,plain,(
% 0.14/0.40 sQ33_spl|sQ35_spl),
% 0.14/0.40 inference(contradiction_clause,[status(thm)],[f407])).
% 0.14/0.40 fof(f409,plain,(
% 0.14/0.40 p_Wr(fifo_length)|~sQ33_spl|~sQ11_spl),
% 0.14/0.40 inference(backward_demodulation,[status(thm)],[f384,f257])).
% 0.14/0.40 fof(f414,plain,(
% 0.14/0.40 p_Rd_error(fifo_length)|~sQ33_spl|~sQ14_spl),
% 0.14/0.40 inference(backward_demodulation,[status(thm)],[f384,f266])).
% 0.14/0.40 fof(f426,plain,(
% 0.14/0.40 ![X0]: (plus(fifo_length,X0)=X0|~sQ33_spl)),
% 0.14/0.40 inference(backward_demodulation,[status(thm)],[f384,f116])).
% 0.14/0.40 fof(f429,plain,(
% 0.14/0.40 gt(int_level(t_139),fifo_length)|~sQ33_spl|~sQ10_spl),
% 0.14/0.40 inference(forward_demodulation,[status(thm)],[f384,f249])).
% 0.14/0.40 fof(f433,plain,(
% 0.14/0.40 p_Reset(fifo_length)|~p_Wr(fifo_length)|p_Rd(fifo_length)|p_Rd_error(plus(fifo_length,n1))|~sQ33_spl|~sQ14_spl),
% 0.14/0.40 inference(resolution,[status(thm)],[f414,f149])).
% 0.14/0.40 fof(f434,definition,(
% 0.14/0.40 sQ37_spl <=> (p_Reset(fifo_length))),
% 0.14/0.40 introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition])).
% 0.14/0.40 fof(f437,definition,(
% 0.14/0.40 sQ38_spl <=> (p_Wr(fifo_length))),
% 0.14/0.40 introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition])).
% 0.14/0.40 fof(f439,plain,(
% 0.14/0.40 ~p_Wr(fifo_length)|sQ38_spl),
% 0.14/0.40 inference(component_clause,[status(thm)],[f437])).
% 0.14/0.40 fof(f440,definition,(
% 0.14/0.40 sQ39_spl <=> (p_Rd(fifo_length))),
% 0.14/0.40 introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition])).
% 0.14/0.40 fof(f443,definition,(
% 0.14/0.40 sQ40_spl <=> (p_Rd_error(plus(fifo_length,n1)))),
% 0.14/0.40 introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition])).
% 0.14/0.40 fof(f446,plain,(
% 0.14/0.40 sQ37_spl|~sQ38_spl|sQ39_spl|sQ40_spl|~sQ33_spl|~sQ14_spl),
% 0.14/0.40 inference(split_clause,[status(thm)],[f433,f434,f437,f440,f443,f383,f265])).
% 0.14/0.40 fof(f447,plain,(
% 0.14/0.40 $false|~sQ33_spl|~sQ11_spl|sQ38_spl),
% 0.14/0.40 inference(forward_subsumption_resolution,[status(thm)],[f439,f409])).
% 0.14/0.40 fof(f448,plain,(
% 0.14/0.40 ~sQ33_spl|~sQ11_spl|sQ38_spl),
% 0.14/0.40 inference(contradiction_clause,[status(thm)],[f447])).
% 0.14/0.40 fof(f452,plain,(
% 0.14/0.40 ![X0]: (p_Reset(X0)|p_Rd(X0)|p_Rd_error(plus(X0,n1))|~p_Rd_error(X0))),
% 0.14/0.40 inference(forward_subsumption_resolution,[status(thm)],[f185,f149])).
% 0.14/0.40 fof(f453,plain,(
% 0.14/0.40 p_Reset(t_139)|p_Rd(t_139)|p_Rd_error(plus(t_139,n1))|~sQ0_spl),
% 0.14/0.40 inference(resolution,[status(thm)],[f452,f195])).
% 0.14/0.40 fof(f454,plain,(
% 0.14/0.40 sQ2_spl|sQ4_spl|sQ1_spl|~sQ0_spl),
% 0.14/0.40 inference(split_clause,[status(thm)],[f453,f208,f214,f197,f194])).
% 0.14/0.40 fof(f455,plain,(
% 0.14/0.40 ![X0]: (~p_Rd(X0)|~gt(int_level(X0),fifo_length)|~p_Rd_error(plus(X0,n1))|~sQ33_spl)),
% 0.14/0.40 inference(forward_demodulation,[status(thm)],[f384,f314])).
% 0.14/0.40 fof(f457,plain,(
% 0.14/0.40 ~p_Rd(plus(t_139,n1))|~gt(int_level(t_139),fifo_length)|~p_Rd_error(plus(plus(t_139,n1),n1))|~sQ33_spl|~sQ9_spl),
% 0.14/0.40 inference(paramodulation,[status(thm)],[f241,f455])).
% 0.14/0.40 fof(f459,definition,(
% 0.14/0.40 sQ41_spl <=> (gt(int_level(t_139),fifo_length))),
% 0.14/0.40 introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition])).
% 0.14/0.40 fof(f461,plain,(
% 0.14/0.40 ~gt(int_level(t_139),fifo_length)|sQ41_spl),
% 0.14/0.40 inference(component_clause,[status(thm)],[f459])).
% 0.14/0.40 fof(f462,plain,(
% 0.14/0.40 ~sQ7_spl|~sQ41_spl|~sQ8_spl|~sQ33_spl|~sQ9_spl),
% 0.14/0.40 inference(split_clause,[status(thm)],[f457,f228,f459,f231,f383,f240])).
% 0.14/0.40 fof(f463,plain,(
% 0.14/0.40 $false|~sQ33_spl|~sQ10_spl|sQ41_spl),
% 0.14/0.40 inference(forward_subsumption_resolution,[status(thm)],[f461,f429])).
% 0.14/0.40 fof(f464,plain,(
% 0.14/0.40 ~sQ33_spl|~sQ10_spl|sQ41_spl),
% 0.14/0.40 inference(contradiction_clause,[status(thm)],[f463])).
% 0.14/0.40 fof(f466,plain,(
% 0.14/0.40 int_level(t_139)=fifo_length|~sQ33_spl|sQ10_spl),
% 0.14/0.40 inference(forward_demodulation,[status(thm)],[f384,f320])).
% 0.14/0.40 fof(f467,plain,(
% 0.14/0.40 $false|sQ16_spl|~sQ33_spl|sQ10_spl),
% 0.14/0.40 inference(forward_subsumption_resolution,[status(thm)],[f466,f280])).
% 0.14/0.40 fof(f468,plain,(
% 0.14/0.40 sQ16_spl|~sQ33_spl|sQ10_spl),
% 0.14/0.40 inference(contradiction_clause,[status(thm)],[f467])).
% 0.14/0.40 fof(f469,plain,(
% 0.14/0.40 int_level(t_139)=fifo_length|~sQ33_spl|~sQ18_spl),
% 0.14/0.40 inference(forward_demodulation,[status(thm)],[f384,f287])).
% 0.14/0.40 fof(f475,plain,(
% 0.14/0.40 p_Wr(fifo_length)|p_Rd(fifo_length)|~p_Rd_error(n1)|p_Rd_error(fifo_length)|~sQ33_spl),
% 0.14/0.40 inference(paramodulation,[status(thm)],[f426,f364])).
% 0.14/0.40 fof(f478,plain,(
% 0.14/0.40 ~p_Reset(fifo_length)|~p_Rd_error(n1)|~sQ33_spl),
% 0.14/0.40 inference(paramodulation,[status(thm)],[f426,f127])).
% 0.14/0.40 fof(f480,definition,(
% 0.14/0.40 sQ42_spl <=> (p_Rd_error(fifo_length))),
% 0.14/0.40 introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition])).
% 0.14/0.40 fof(f481,plain,(
% 0.14/0.40 p_Rd_error(fifo_length)|~sQ42_spl),
% 0.14/0.40 inference(component_clause,[status(thm)],[f480])).
% 0.14/0.40 fof(f483,plain,(
% 0.14/0.40 sQ38_spl|sQ39_spl|~sQ13_spl|sQ42_spl|~sQ33_spl),
% 0.14/0.40 inference(split_clause,[status(thm)],[f475,f437,f440,f262,f480,f383])).
% 0.14/0.40 fof(f484,plain,(
% 0.14/0.40 ~sQ37_spl|~sQ13_spl|~sQ33_spl),
% 0.14/0.40 inference(split_clause,[status(thm)],[f478,f434,f262,f383])).
% 0.14/0.40 fof(f487,plain,(
% 0.14/0.40 p_Reset(fifo_length)|p_Rd(fifo_length)|p_Rd_error(plus(fifo_length,n1))|~sQ42_spl),
% 0.14/0.40 inference(resolution,[status(thm)],[f481,f452])).
% 0.14/0.40 fof(f488,plain,(
% 0.14/0.40 sQ37_spl|sQ39_spl|sQ40_spl|~sQ42_spl),
% 0.14/0.40 inference(split_clause,[status(thm)],[f487,f434,f440,f443,f480])).
% 0.14/0.40 fof(f492,plain,(
% 0.14/0.40 ~fifo_length=fifo_length|p_Full(t_139)|~sQ33_spl|~sQ18_spl),
% 0.14/0.40 inference(paramodulation,[status(thm)],[f469,f119])).
% 0.14/0.40 fof(f497,definition,(
% 0.14/0.40 sQ44_spl <=> (p_Full(t_139))),
% 0.14/0.40 introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition])).
% 0.14/0.40 fof(f500,plain,(
% 0.14/0.40 ~sQ36_spl|sQ44_spl|~sQ33_spl|~sQ18_spl),
% 0.14/0.40 inference(split_clause,[status(thm)],[f492,f402,f497,f383,f286])).
% 0.14/0.40 fof(f501,plain,(
% 0.14/0.40 $false|sQ36_spl),
% 0.14/0.40 inference(trivial_equality_resolution,[status(thm)],[f404])).
% 0.14/0.40 fof(f502,plain,(
% 0.14/0.40 sQ36_spl),
% 0.14/0.40 inference(contradiction_clause,[status(thm)],[f501])).
% 0.14/0.40 fof(f523,plain,(
% 0.14/0.40 p_Wr(t_139)|p_Rd(t_139)|p_Rd_error(t_139)|~sQ1_spl),
% 0.14/0.40 inference(resolution,[status(thm)],[f198,f364])).
% 0.14/0.40 fof(f526,plain,(
% 0.14/0.40 sQ3_spl|sQ4_spl|sQ0_spl|~sQ1_spl),
% 0.14/0.40 inference(split_clause,[status(thm)],[f523,f211,f214,f194,f197])).
% 0.14/0.40 fof(f528,plain,(
% 0.14/0.40 $false),
% 0.14/0.40 inference(sat_refutation,[status(thm)],[f200,f201,f221,f236,f243,f245,f268,f272,f284,f292,f306,f308,f313,f322,f327,f333,f336,f362,f366,f378,f382,f389,f400,f401,f408,f446,f448,f454,f462,f464,f468,f483,f484,f488,f500,f502,f526])).
% 0.14/0.40 % SZS output end CNFRefutation for theBenchmark.p
% 0.14/0.42 % Elapsed time: 0.060255 seconds
% 0.14/0.42 % CPU time: 0.201294 seconds
% 0.14/0.42 % Total memory used: 82.257 MB
% 0.14/0.42 % Net memory used: 82.168 MB
%------------------------------------------------------------------------------