%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : HWV016-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 : n011.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:41 PM UTC 2026
% Result : Unsatisfiable 0.12s 0.45s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : HWV016-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 : n011.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:48:40 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.08/0.37 % Drodi V4.1.1
% 0.12/0.45 % Refutation found
% 0.12/0.45 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.12/0.45 % SZS output start CNFRefutation for theBenchmark
% 0.12/0.45 fof(f1,axiom,(
% 0.12/0.45 (![X_0]: (plus(X_0,n1) != n0 ))),
% 0.12/0.45 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.45 fof(f2,axiom,(
% 0.12/0.45 (![X_1]: (gt(plus(X_1,n1),n0) ))),
% 0.12/0.45 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.45 fof(f3,axiom,(
% 0.12/0.45 (![X_2]: (( ~ gt(X_2,n0)| gt(X_2,minus(X_2,n1)) ) ))),
% 0.12/0.45 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.45 fof(f5,axiom,(
% 0.12/0.45 (![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.45 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.45 fof(f7,axiom,(
% 0.12/0.45 (![Y_4,X_3]: (( ~ def_10(Y_4,X_3)| X_3 != Y_4 ) ))),
% 0.12/0.45 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.45 fof(f10,axiom,(
% 0.12/0.45 (![X_13,Y_14]: (( gt(X_13,Y_14)| ~ gt(plus(X_13,n1),Y_14)| Y_14 = X_13 ) ))),
% 0.12/0.45 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.45 fof(f12,axiom,(
% 0.12/0.45 (![Y_18,X_17]: (( gt(Y_18,X_17)| X_17 = Y_18| gt(X_17,Y_18) ) ))),
% 0.12/0.45 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.45 fof(f13,axiom,(
% 0.12/0.45 (![Z_21,Y_20,X_19]: (( ~ gt(Z_21,Y_20)| gt(Z_21,X_19)| ~ gt(Y_20,X_19) ) ))),
% 0.12/0.45 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.45 fof(f14,axiom,(
% 0.12/0.45 (![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.45 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.45 fof(f15,axiom,(
% 0.12/0.45 (![X_25]: (( X_25 = n0| gt(X_25,n0) ) ))),
% 0.12/0.45 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.45 fof(f16,axiom,(
% 0.12/0.45 (![X_26]: (( X_26 = n0| X_26 = plus(y_27(X_26),n1) ) ))),
% 0.12/0.45 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.45 fof(f17,axiom,(
% 0.12/0.45 (![X_28]: (~ gt(X_28,X_28) ))),
% 0.12/0.45 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.45 fof(f18,axiom,(
% 0.12/0.45 (![X_29,Y_30]: (( plus(X_29,n1) != plus(Y_30,n1)| X_29 = Y_30 ) ))),
% 0.12/0.45 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.45 fof(f19,axiom,(
% 0.12/0.45 (![X_31]: (plus(n0,X_31) = X_31 ))),
% 0.12/0.45 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.45 fof(f21,axiom,(
% 0.12/0.45 (![X_t_32]: (level(X_t_32) = int_level(X_t_32) ))),
% 0.12/0.45 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.45 fof(f25,axiom,(
% 0.12/0.45 (![X_t_36]: (( int_level(X_t_36) = n0| ~ p_Empty(X_t_36) ) ))),
% 0.12/0.45 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.45 fof(f35,axiom,(
% 0.12/0.45 (![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.45 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.45 fof(f44,axiom,(
% 0.12/0.45 (![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)) = int_level(X_t_42) ) ))),
% 0.12/0.45 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.45 fof(f53,axiom,(
% 0.12/0.45 (![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)| int_level(plus(X_t_42,n1)) = int_level(X_t_42) ) ))),
% 0.12/0.45 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.45 fof(f59,axiom,(
% 0.12/0.45 (![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)| int_level(plus(X_t_42,n1)) = plus(int_level(X_t_42),n1) ) ))),
% 0.12/0.45 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.45 fof(f92,negated_conjecture,(
% 0.12/0.45 p_Wr(t_139) ),
% 0.12/0.45 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.45 fof(f93,negated_conjecture,(
% 0.12/0.45 ~ p_Reset(t_139) ),
% 0.12/0.45 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.45 fof(f94,negated_conjecture,(
% 0.12/0.45 p_Empty(plus(t_139,n1)) ),
% 0.12/0.45 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.45 fof(f95,negated_conjecture,(
% 0.12/0.45 gt(fifo_length,n0) ),
% 0.12/0.45 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.45 fof(f96,plain,(
% 0.12/0.45 ![X0]: (~plus(X0,n1)=n0)),
% 0.12/0.45 inference(cnf_transformation,[status(thm)],[f1])).
% 0.12/0.45 fof(f97,plain,(
% 0.12/0.45 ![X0]: (gt(plus(X0,n1),n0))),
% 0.12/0.45 inference(cnf_transformation,[status(thm)],[f2])).
% 0.12/0.45 fof(f98,plain,(
% 0.12/0.45 ![X0]: (~gt(X0,n0)|gt(X0,minus(X0,n1)))),
% 0.12/0.45 inference(cnf_transformation,[status(thm)],[f3])).
% 0.12/0.45 fof(f101,plain,(
% 0.12/0.45 ![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.45 inference(miniscoping,[status(thm)],[f5])).
% 0.12/0.45 fof(f102,plain,(
% 0.12/0.45 ![X0,X1,X2]: (minus(X0,X1)=X2|~plus(X2,X1)=X0|def_10(X1,X0))),
% 0.12/0.45 inference(cnf_transformation,[status(thm)],[f101])).
% 0.12/0.45 fof(f104,plain,(
% 0.12/0.45 ![X0,X1]: (~def_10(X0,X1)|~X1=X0)),
% 0.12/0.45 inference(cnf_transformation,[status(thm)],[f7])).
% 0.12/0.45 fof(f107,plain,(
% 0.12/0.45 ![X0,X1]: (gt(X0,X1)|~gt(plus(X0,n1),X1)|X1=X0)),
% 0.12/0.45 inference(cnf_transformation,[status(thm)],[f10])).
% 0.12/0.45 fof(f109,plain,(
% 0.12/0.45 ![X0,X1]: (gt(X0,X1)|X1=X0|gt(X1,X0))),
% 0.12/0.45 inference(cnf_transformation,[status(thm)],[f12])).
% 0.12/0.45 fof(f110,plain,(
% 0.12/0.45 ![Y_20,X_19]: ((![Z_21]: (~gt(Z_21,Y_20)|gt(Z_21,X_19)))|~gt(Y_20,X_19))),
% 0.12/0.45 inference(miniscoping,[status(thm)],[f13])).
% 0.12/0.45 fof(f111,plain,(
% 0.12/0.45 ![X0,X1,X2]: (~gt(X0,X1)|gt(X0,X2)|~gt(X1,X2))),
% 0.12/0.45 inference(cnf_transformation,[status(thm)],[f110])).
% 0.12/0.45 fof(f112,plain,(
% 0.12/0.45 ![X0,X1]: (~gt(X0,X1)|plus(X1,n1)=X0|gt(X0,plus(X1,n1)))),
% 0.12/0.45 inference(cnf_transformation,[status(thm)],[f14])).
% 0.12/0.45 fof(f113,plain,(
% 0.12/0.45 ![X0]: (X0=n0|gt(X0,n0))),
% 0.12/0.45 inference(cnf_transformation,[status(thm)],[f15])).
% 0.12/0.45 fof(f114,plain,(
% 0.12/0.45 ![X0]: (X0=n0|X0=plus(y_27(X0),n1))),
% 0.12/0.45 inference(cnf_transformation,[status(thm)],[f16])).
% 0.12/0.45 fof(f115,plain,(
% 0.12/0.45 ![X0]: (~gt(X0,X0))),
% 0.12/0.45 inference(cnf_transformation,[status(thm)],[f17])).
% 0.12/0.45 fof(f116,plain,(
% 0.12/0.45 ![X0,X1]: (~plus(X0,n1)=plus(X1,n1)|X0=X1)),
% 0.12/0.45 inference(cnf_transformation,[status(thm)],[f18])).
% 0.12/0.45 fof(f117,plain,(
% 0.12/0.45 ![X0]: (plus(n0,X0)=X0)),
% 0.12/0.45 inference(cnf_transformation,[status(thm)],[f19])).
% 0.12/0.45 fof(f119,plain,(
% 0.12/0.45 ![X0]: (level(X0)=int_level(X0))),
% 0.12/0.45 inference(cnf_transformation,[status(thm)],[f21])).
% 0.12/0.45 fof(f123,plain,(
% 0.12/0.45 ![X0]: (int_level(X0)=n0|~p_Empty(X0))),
% 0.12/0.45 inference(cnf_transformation,[status(thm)],[f25])).
% 0.12/0.45 fof(f135,plain,(
% 0.12/0.45 ![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.45 inference(cnf_transformation,[status(thm)],[f35])).
% 0.12/0.45 fof(f144,plain,(
% 0.12/0.45 ![X0]: (p_Reset(X0)|~p_Wr(X0)|p_Rd(X0)|gt(fifo_length,int_level(X0))|int_level(plus(X0,n1))=int_level(X0))),
% 0.12/0.45 inference(cnf_transformation,[status(thm)],[f44])).
% 0.12/0.45 fof(f153,plain,(
% 0.12/0.45 ![X0]: (p_Reset(X0)|~p_Wr(X0)|~p_Rd(X0)|~gt(int_level(X0),n0)|int_level(plus(X0,n1))=int_level(X0))),
% 0.12/0.45 inference(cnf_transformation,[status(thm)],[f53])).
% 0.12/0.45 fof(f159,plain,(
% 0.12/0.45 ![X0]: (p_Reset(X0)|~p_Wr(X0)|~p_Rd(X0)|gt(int_level(X0),n0)|int_level(plus(X0,n1))=plus(int_level(X0),n1))),
% 0.12/0.45 inference(cnf_transformation,[status(thm)],[f59])).
% 0.12/0.45 fof(f192,plain,(
% 0.12/0.45 p_Wr(t_139)),
% 0.12/0.45 inference(cnf_transformation,[status(thm)],[f92])).
% 0.12/0.45 fof(f193,plain,(
% 0.12/0.45 ~p_Reset(t_139)),
% 0.12/0.45 inference(cnf_transformation,[status(thm)],[f93])).
% 0.12/0.45 fof(f194,plain,(
% 0.12/0.45 p_Empty(plus(t_139,n1))),
% 0.12/0.45 inference(cnf_transformation,[status(thm)],[f94])).
% 0.12/0.45 fof(f195,plain,(
% 0.12/0.45 gt(fifo_length,n0)),
% 0.12/0.45 inference(cnf_transformation,[status(thm)],[f95])).
% 0.12/0.45 fof(f197,plain,(
% 0.12/0.45 ![X0,X1]: (minus(plus(X0,X1),X1)=X0|def_10(X1,plus(X0,X1)))),
% 0.12/0.45 inference(destructive_equality_resolution,[status(thm)],[f102])).
% 0.12/0.45 fof(f198,plain,(
% 0.12/0.45 ![X0]: (~def_10(X0,X0))),
% 0.12/0.45 inference(destructive_equality_resolution,[status(thm)],[f104])).
% 0.12/0.45 fof(f199,plain,(
% 0.12/0.45 ~n1=n0),
% 0.12/0.45 inference(paramodulation,[status(thm)],[f117,f96])).
% 0.12/0.45 fof(f201,plain,(
% 0.12/0.45 gt(n1,n0)),
% 0.12/0.45 inference(paramodulation,[status(thm)],[f117,f97])).
% 0.12/0.45 fof(f209,plain,(
% 0.12/0.45 ![X0]: (level(X0)=n0|~p_Empty(X0))),
% 0.12/0.45 inference(forward_demodulation,[status(thm)],[f119,f123])).
% 0.12/0.45 fof(f211,plain,(
% 0.12/0.45 level(plus(t_139,n1))=n0),
% 0.12/0.45 inference(resolution,[status(thm)],[f194,f209])).
% 0.12/0.45 fof(f215,plain,(
% 0.12/0.45 ![X0]: (minus(plus(n0,X0),X0)=n0|def_10(X0,X0))),
% 0.12/0.45 inference(paramodulation,[status(thm)],[f117,f197])).
% 0.12/0.45 fof(f216,plain,(
% 0.12/0.45 ![X0]: (minus(X0,X0)=n0|def_10(X0,X0))),
% 0.12/0.45 inference(forward_demodulation,[status(thm)],[f117,f215])).
% 0.12/0.45 fof(f217,plain,(
% 0.12/0.45 ![X0]: (minus(X0,X0)=n0)),
% 0.12/0.45 inference(forward_subsumption_resolution,[status(thm)],[f216,f198])).
% 0.12/0.45 fof(f219,definition,(
% 0.12/0.45 sQ0_spl <=> (gt(n1,n0))),
% 0.12/0.45 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.12/0.45 fof(f231,definition,(
% 0.12/0.45 sQ2_spl <=> (gt(level(t_139),n0))),
% 0.12/0.45 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.12/0.45 fof(f232,plain,(
% 0.12/0.45 gt(level(t_139),n0)|~sQ2_spl),
% 0.12/0.45 inference(component_clause,[status(thm)],[f231])).
% 0.12/0.45 fof(f237,plain,(
% 0.12/0.45 ![X0,X1]: (~gt(X0,X1)|~gt(X1,X0))),
% 0.12/0.45 inference(resolution,[status(thm)],[f111,f115])).
% 0.12/0.45 fof(f238,plain,(
% 0.12/0.45 ~gt(n0,n1)),
% 0.12/0.45 inference(resolution,[status(thm)],[f237,f201])).
% 0.12/0.45 fof(f240,plain,(
% 0.12/0.45 ![X0]: (~gt(n0,plus(X0,n1)))),
% 0.12/0.45 inference(resolution,[status(thm)],[f237,f97])).
% 0.12/0.45 fof(f242,plain,(
% 0.12/0.45 ![X0]: (~gt(minus(X0,n1),X0)|~gt(X0,n0))),
% 0.12/0.45 inference(resolution,[status(thm)],[f237,f98])).
% 0.12/0.45 fof(f243,plain,(
% 0.12/0.45 ![X0]: (~gt(n0,X0)|X0=n0)),
% 0.12/0.45 inference(resolution,[status(thm)],[f237,f113])).
% 0.12/0.45 fof(f250,plain,(
% 0.12/0.45 gt(n1,n0)|n0=n1),
% 0.12/0.45 inference(resolution,[status(thm)],[f238,f109])).
% 0.12/0.45 fof(f252,definition,(
% 0.12/0.45 sQ3_spl <=> (n0=n1)),
% 0.12/0.45 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 0.12/0.45 fof(f253,plain,(
% 0.12/0.45 n0=n1|~sQ3_spl),
% 0.12/0.45 inference(component_clause,[status(thm)],[f252])).
% 0.12/0.45 fof(f255,plain,(
% 0.12/0.45 sQ0_spl|sQ3_spl),
% 0.12/0.45 inference(split_clause,[status(thm)],[f250,f219,f252])).
% 0.12/0.45 fof(f269,plain,(
% 0.12/0.45 n0=n0|n0=n0),
% 0.12/0.45 inference(resolution,[status(thm)],[f243,f113])).
% 0.12/0.45 fof(f282,definition,(
% 0.12/0.45 sQ8_spl <=> (n0=n0)),
% 0.12/0.45 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 0.12/0.45 fof(f285,plain,(
% 0.12/0.45 sQ8_spl),
% 0.12/0.45 inference(split_clause,[status(thm)],[f269,f282])).
% 0.12/0.45 fof(f309,plain,(
% 0.12/0.45 ![X0]: (gt(n0,X0)|~gt(n1,X0)|X0=n0)),
% 0.12/0.45 inference(paramodulation,[status(thm)],[f117,f107])).
% 0.12/0.45 fof(f311,plain,(
% 0.12/0.45 ![X0]: (~gt(n1,X0)|X0=n0)),
% 0.12/0.45 inference(forward_subsumption_resolution,[status(thm)],[f309,f243])).
% 0.12/0.45 fof(f314,plain,(
% 0.12/0.45 minus(n1,n1)=n0|~gt(n1,n0)),
% 0.12/0.45 inference(resolution,[status(thm)],[f311,f98])).
% 0.12/0.45 fof(f316,plain,(
% 0.12/0.45 ![X0,X1]: (X0=n0|~gt(n1,X1)|~gt(X1,X0))),
% 0.12/0.45 inference(resolution,[status(thm)],[f311,f111])).
% 0.12/0.45 fof(f317,plain,(
% 0.12/0.45 n1=n0|n1=n1),
% 0.12/0.45 inference(resolution,[status(thm)],[f311,f109])).
% 0.12/0.45 fof(f321,definition,(
% 0.12/0.45 sQ9_spl <=> (minus(n1,n1)=n0)),
% 0.12/0.45 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 0.12/0.45 fof(f324,plain,(
% 0.12/0.45 sQ9_spl|~sQ0_spl),
% 0.12/0.45 inference(split_clause,[status(thm)],[f314,f321,f219])).
% 0.12/0.45 fof(f326,definition,(
% 0.12/0.45 sQ10_spl <=> (n1=n1)),
% 0.12/0.45 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 0.12/0.45 fof(f329,plain,(
% 0.12/0.45 sQ3_spl|sQ10_spl),
% 0.12/0.45 inference(split_clause,[status(thm)],[f317,f252,f326])).
% 0.12/0.45 fof(f331,plain,(
% 0.12/0.45 $false|~sQ3_spl),
% 0.12/0.45 inference(forward_subsumption_resolution,[status(thm)],[f253,f199])).
% 0.12/0.45 fof(f332,plain,(
% 0.12/0.45 ~sQ3_spl),
% 0.12/0.45 inference(contradiction_clause,[status(thm)],[f331])).
% 0.12/0.45 fof(f342,definition,(
% 0.12/0.45 sQ11_spl <=> (gt(n0,n1))),
% 0.12/0.45 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 0.12/0.45 fof(f370,plain,(
% 0.12/0.45 ![X0]: (~gt(n1,X0)|plus(X0,n1)=n1|plus(X0,n1)=n0)),
% 0.12/0.45 inference(resolution,[status(thm)],[f112,f311])).
% 0.12/0.45 fof(f373,plain,(
% 0.12/0.45 ![X0]: (~gt(n0,X0)|plus(X0,n1)=n0)),
% 0.12/0.45 inference(resolution,[status(thm)],[f112,f240])).
% 0.12/0.45 fof(f379,plain,(
% 0.12/0.45 ![X0]: (~gt(n1,X0)|plus(X0,n1)=n1)),
% 0.12/0.45 inference(forward_subsumption_resolution,[status(thm)],[f370,f96])).
% 0.12/0.45 fof(f380,plain,(
% 0.12/0.45 ![X0]: (~gt(n0,X0))),
% 0.12/0.45 inference(forward_subsumption_resolution,[status(thm)],[f373,f96])).
% 0.12/0.45 fof(f384,plain,(
% 0.12/0.45 ![X0]: (X0=y_27(plus(X0,n1))|plus(X0,n1)=n0)),
% 0.12/0.45 inference(resolution,[status(thm)],[f116,f114])).
% 0.12/0.45 fof(f387,plain,(
% 0.12/0.45 ![X0]: (~n1=plus(X0,n1)|n0=X0)),
% 0.12/0.45 inference(paramodulation,[status(thm)],[f117,f116])).
% 0.12/0.45 fof(f391,plain,(
% 0.12/0.45 ![X0]: (X0=y_27(plus(X0,n1)))),
% 0.12/0.45 inference(forward_subsumption_resolution,[status(thm)],[f384,f96])).
% 0.12/0.45 fof(f445,plain,(
% 0.12/0.45 n0=y_27(n1)),
% 0.12/0.45 inference(paramodulation,[status(thm)],[f117,f391])).
% 0.12/0.45 fof(f447,plain,(
% 0.12/0.45 n1=n0|n1=plus(n0,n1)),
% 0.12/0.45 inference(paramodulation,[status(thm)],[f445,f114])).
% 0.12/0.45 fof(f448,definition,(
% 0.12/0.45 sQ19_spl <=> (n1=plus(n0,n1))),
% 0.12/0.45 introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition])).
% 0.12/0.45 fof(f451,plain,(
% 0.12/0.45 sQ3_spl|sQ19_spl),
% 0.12/0.45 inference(split_clause,[status(thm)],[f447,f252,f448])).
% 0.12/0.45 fof(f453,plain,(
% 0.12/0.45 ![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.45 inference(forward_demodulation,[status(thm)],[f119,f135])).
% 0.12/0.45 fof(f454,plain,(
% 0.12/0.45 ![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.45 inference(forward_demodulation,[status(thm)],[f119,f453])).
% 0.12/0.45 fof(f455,plain,(
% 0.12/0.45 ![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.45 inference(forward_demodulation,[status(thm)],[f119,f454])).
% 0.12/0.45 fof(f456,plain,(
% 0.12/0.45 p_Reset(t_139)|p_Rd(t_139)|~gt(fifo_length,level(t_139))|level(plus(t_139,n1))=plus(level(t_139),n1)),
% 0.12/0.45 inference(resolution,[status(thm)],[f455,f192])).
% 0.12/0.45 fof(f457,definition,(
% 0.12/0.45 sQ20_spl <=> (p_Reset(t_139))),
% 0.12/0.45 introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition])).
% 0.12/0.45 fof(f458,plain,(
% 0.12/0.45 p_Reset(t_139)|~sQ20_spl),
% 0.12/0.45 inference(component_clause,[status(thm)],[f457])).
% 0.12/0.45 fof(f460,definition,(
% 0.12/0.45 sQ21_spl <=> (p_Rd(t_139))),
% 0.12/0.45 introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition])).
% 0.12/0.45 fof(f463,definition,(
% 0.12/0.45 sQ22_spl <=> (gt(fifo_length,level(t_139)))),
% 0.12/0.45 introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition])).
% 0.12/0.45 fof(f465,plain,(
% 0.12/0.45 ~gt(fifo_length,level(t_139))|sQ22_spl),
% 0.12/0.45 inference(component_clause,[status(thm)],[f463])).
% 0.12/0.45 fof(f466,definition,(
% 0.12/0.45 sQ23_spl <=> (level(plus(t_139,n1))=plus(level(t_139),n1))),
% 0.12/0.45 introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition])).
% 0.12/0.45 fof(f467,plain,(
% 0.12/0.45 level(plus(t_139,n1))=plus(level(t_139),n1)|~sQ23_spl),
% 0.12/0.45 inference(component_clause,[status(thm)],[f466])).
% 0.12/0.45 fof(f469,plain,(
% 0.12/0.45 sQ20_spl|sQ21_spl|~sQ22_spl|sQ23_spl),
% 0.12/0.45 inference(split_clause,[status(thm)],[f456,f457,f460,f463,f466])).
% 0.12/0.45 fof(f470,plain,(
% 0.12/0.45 n0=plus(level(t_139),n1)|~sQ23_spl),
% 0.12/0.45 inference(forward_demodulation,[status(thm)],[f211,f467])).
% 0.12/0.45 fof(f499,plain,(
% 0.12/0.45 n0=y_27(n1)|n1=n0),
% 0.12/0.45 inference(resolution,[status(thm)],[f387,f114])).
% 0.12/0.45 fof(f503,definition,(
% 0.12/0.45 sQ26_spl <=> (n0=y_27(n1))),
% 0.12/0.45 introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition])).
% 0.12/0.45 fof(f506,plain,(
% 0.12/0.45 sQ26_spl|sQ3_spl),
% 0.12/0.45 inference(split_clause,[status(thm)],[f499,f503,f252])).
% 0.12/0.45 fof(f558,plain,(
% 0.12/0.45 ![X0]: (p_Reset(X0)|~p_Wr(X0)|p_Rd(X0)|gt(fifo_length,level(X0))|int_level(plus(X0,n1))=int_level(X0))),
% 0.12/0.45 inference(forward_demodulation,[status(thm)],[f119,f144])).
% 0.12/0.45 fof(f559,plain,(
% 0.12/0.45 ![X0]: (p_Reset(X0)|~p_Wr(X0)|p_Rd(X0)|gt(fifo_length,level(X0))|level(plus(X0,n1))=int_level(X0))),
% 0.12/0.45 inference(forward_demodulation,[status(thm)],[f119,f558])).
% 0.12/0.45 fof(f560,plain,(
% 0.12/0.45 ![X0]: (p_Reset(X0)|~p_Wr(X0)|p_Rd(X0)|gt(fifo_length,level(X0))|level(plus(X0,n1))=level(X0))),
% 0.12/0.45 inference(forward_demodulation,[status(thm)],[f119,f559])).
% 0.12/0.45 fof(f561,plain,(
% 0.12/0.45 p_Reset(t_139)|p_Rd(t_139)|gt(fifo_length,level(t_139))|level(plus(t_139,n1))=level(t_139)),
% 0.12/0.45 inference(resolution,[status(thm)],[f560,f192])).
% 0.12/0.45 fof(f562,definition,(
% 0.12/0.45 sQ28_spl <=> (level(plus(t_139,n1))=level(t_139))),
% 0.12/0.45 introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition])).
% 0.12/0.45 fof(f563,plain,(
% 0.12/0.45 level(plus(t_139,n1))=level(t_139)|~sQ28_spl),
% 0.12/0.45 inference(component_clause,[status(thm)],[f562])).
% 0.12/0.45 fof(f565,plain,(
% 0.12/0.45 sQ20_spl|sQ21_spl|sQ22_spl|sQ28_spl),
% 0.12/0.45 inference(split_clause,[status(thm)],[f561,f457,f460,f463,f562])).
% 0.12/0.45 fof(f599,plain,(
% 0.12/0.45 ![X0]: (X0=n0|~gt(minus(n1,n1),X0)|~gt(n1,n0))),
% 0.12/0.45 inference(resolution,[status(thm)],[f316,f98])).
% 0.12/0.45 fof(f600,plain,(
% 0.12/0.45 ![X0]: (X0=n0|~gt(n0,X0)|n1=n0)),
% 0.12/0.45 inference(resolution,[status(thm)],[f316,f113])).
% 0.12/0.45 fof(f610,definition,(
% 0.12/0.45 ![X0]: (sQ31_spl <=> (X0=n0|~gt(minus(n1,n1),X0)))),
% 0.12/0.45 introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition])).
% 0.12/0.45 fof(f613,plain,(
% 0.12/0.45 sQ31_spl|~sQ0_spl),
% 0.12/0.45 inference(split_clause,[status(thm)],[f599,f610,f219])).
% 0.12/0.45 fof(f614,definition,(
% 0.12/0.45 ![X0]: (sQ32_spl <=> (X0=n0|~gt(n0,X0)))),
% 0.12/0.45 introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition])).
% 0.12/0.45 fof(f617,plain,(
% 0.12/0.45 sQ32_spl|sQ3_spl),
% 0.12/0.45 inference(split_clause,[status(thm)],[f600,f614,f252])).
% 0.12/0.45 fof(f624,plain,(
% 0.12/0.45 plus(minus(n1,n1),n1)=n1|~gt(n1,n0)),
% 0.12/0.45 inference(resolution,[status(thm)],[f379,f98])).
% 0.12/0.45 fof(f631,definition,(
% 0.12/0.45 sQ33_spl <=> (plus(n1,n1)=n1)),
% 0.12/0.45 introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition])).
% 0.12/0.45 fof(f632,plain,(
% 0.12/0.45 plus(n1,n1)=n1|~sQ33_spl),
% 0.12/0.45 inference(component_clause,[status(thm)],[f631])).
% 0.12/0.45 fof(f635,definition,(
% 0.12/0.45 sQ34_spl <=> (plus(minus(n1,n1),n1)=n1)),
% 0.12/0.45 introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition])).
% 0.12/0.45 fof(f638,plain,(
% 0.12/0.45 sQ34_spl|~sQ0_spl),
% 0.12/0.45 inference(split_clause,[status(thm)],[f624,f635,f219])).
% 0.12/0.45 fof(f694,plain,(
% 0.12/0.45 $false|~sQ20_spl),
% 0.12/0.45 inference(forward_subsumption_resolution,[status(thm)],[f458,f193])).
% 0.12/0.45 fof(f695,plain,(
% 0.12/0.45 ~sQ20_spl),
% 0.12/0.45 inference(contradiction_clause,[status(thm)],[f694])).
% 0.12/0.45 fof(f701,plain,(
% 0.12/0.45 n1=y_27(n1)|~sQ33_spl),
% 0.12/0.45 inference(paramodulation,[status(thm)],[f632,f391])).
% 0.12/0.45 fof(f715,plain,(
% 0.12/0.45 n1=n0|~sQ33_spl),
% 0.12/0.45 inference(forward_demodulation,[status(thm)],[f445,f701])).
% 0.12/0.45 fof(f716,plain,(
% 0.12/0.45 $false|~sQ33_spl),
% 0.12/0.45 inference(forward_subsumption_resolution,[status(thm)],[f715,f199])).
% 0.12/0.45 fof(f717,plain,(
% 0.12/0.45 ~sQ33_spl),
% 0.12/0.45 inference(contradiction_clause,[status(thm)],[f716])).
% 0.12/0.45 fof(f726,plain,(
% 0.12/0.45 ![X0]: (p_Reset(X0)|~p_Wr(X0)|~p_Rd(X0)|~gt(level(X0),n0)|int_level(plus(X0,n1))=int_level(X0))),
% 0.12/0.45 inference(forward_demodulation,[status(thm)],[f119,f153])).
% 0.12/0.45 fof(f727,plain,(
% 0.12/0.45 ![X0]: (p_Reset(X0)|~p_Wr(X0)|~p_Rd(X0)|~gt(level(X0),n0)|level(plus(X0,n1))=int_level(X0))),
% 0.12/0.45 inference(forward_demodulation,[status(thm)],[f119,f726])).
% 0.12/0.45 fof(f728,plain,(
% 0.12/0.45 ![X0]: (p_Reset(X0)|~p_Wr(X0)|~p_Rd(X0)|~gt(level(X0),n0)|level(plus(X0,n1))=level(X0))),
% 0.12/0.45 inference(forward_demodulation,[status(thm)],[f119,f727])).
% 0.12/0.45 fof(f729,plain,(
% 0.12/0.45 p_Reset(t_139)|~p_Rd(t_139)|~gt(level(t_139),n0)|level(plus(t_139,n1))=level(t_139)),
% 0.12/0.45 inference(resolution,[status(thm)],[f728,f192])).
% 0.12/0.45 fof(f730,plain,(
% 0.12/0.45 sQ20_spl|~sQ21_spl|~sQ2_spl|sQ28_spl),
% 0.12/0.45 inference(split_clause,[status(thm)],[f729,f457,f460,f231,f562])).
% 0.12/0.45 fof(f731,plain,(
% 0.12/0.45 n0=level(t_139)|~sQ28_spl),
% 0.12/0.45 inference(forward_demodulation,[status(thm)],[f211,f563])).
% 0.12/0.45 fof(f768,plain,(
% 0.12/0.45 ~gt(n0,n1)|~gt(n1,n0)),
% 0.12/0.45 inference(paramodulation,[status(thm)],[f217,f242])).
% 0.12/0.45 fof(f775,plain,(
% 0.12/0.45 ~sQ11_spl|~sQ0_spl),
% 0.12/0.45 inference(split_clause,[status(thm)],[f768,f342,f219])).
% 0.12/0.45 fof(f796,plain,(
% 0.12/0.45 ![X0]: (p_Reset(X0)|~p_Wr(X0)|~p_Rd(X0)|gt(level(X0),n0)|int_level(plus(X0,n1))=plus(int_level(X0),n1))),
% 0.12/0.45 inference(forward_demodulation,[status(thm)],[f119,f159])).
% 0.12/0.45 fof(f797,plain,(
% 0.12/0.45 ![X0]: (p_Reset(X0)|~p_Wr(X0)|~p_Rd(X0)|gt(level(X0),n0)|level(plus(X0,n1))=plus(int_level(X0),n1))),
% 0.12/0.45 inference(forward_demodulation,[status(thm)],[f119,f796])).
% 0.12/0.45 fof(f798,plain,(
% 0.12/0.45 ![X0]: (p_Reset(X0)|~p_Wr(X0)|~p_Rd(X0)|gt(level(X0),n0)|level(plus(X0,n1))=plus(level(X0),n1))),
% 0.12/0.45 inference(forward_demodulation,[status(thm)],[f119,f797])).
% 0.12/0.45 fof(f799,plain,(
% 0.12/0.45 p_Reset(t_139)|~p_Rd(t_139)|gt(level(t_139),n0)|level(plus(t_139,n1))=plus(level(t_139),n1)),
% 0.12/0.45 inference(resolution,[status(thm)],[f798,f192])).
% 0.12/0.45 fof(f800,plain,(
% 0.12/0.45 sQ20_spl|~sQ21_spl|sQ2_spl|sQ23_spl),
% 0.12/0.45 inference(split_clause,[status(thm)],[f799,f457,f460,f231,f466])).
% 0.12/0.45 fof(f808,plain,(
% 0.12/0.45 gt(n0,n0)|~sQ28_spl|~sQ2_spl),
% 0.12/0.45 inference(forward_demodulation,[status(thm)],[f731,f232])).
% 0.12/0.45 fof(f809,plain,(
% 0.12/0.45 $false|~sQ28_spl|~sQ2_spl),
% 0.12/0.45 inference(forward_subsumption_resolution,[status(thm)],[f808,f380])).
% 0.12/0.45 fof(f810,plain,(
% 0.12/0.45 ~sQ28_spl|~sQ2_spl),
% 0.12/0.45 inference(contradiction_clause,[status(thm)],[f809])).
% 0.12/0.45 fof(f811,plain,(
% 0.12/0.45 ~gt(fifo_length,n0)|~sQ28_spl|sQ22_spl),
% 0.12/0.45 inference(forward_demodulation,[status(thm)],[f731,f465])).
% 0.12/0.45 fof(f812,plain,(
% 0.12/0.45 $false|~sQ28_spl|sQ22_spl),
% 0.12/0.45 inference(forward_subsumption_resolution,[status(thm)],[f811,f195])).
% 0.12/0.45 fof(f813,plain,(
% 0.12/0.45 ~sQ28_spl|sQ22_spl),
% 0.12/0.45 inference(contradiction_clause,[status(thm)],[f812])).
% 0.12/0.45 fof(f814,plain,(
% 0.12/0.45 $false|~sQ23_spl),
% 0.12/0.45 inference(forward_subsumption_resolution,[status(thm)],[f470,f96])).
% 0.12/0.45 fof(f815,plain,(
% 0.12/0.45 ~sQ23_spl),
% 0.12/0.45 inference(contradiction_clause,[status(thm)],[f814])).
% 0.12/0.45 fof(f816,plain,(
% 0.12/0.45 $false),
% 0.12/0.45 inference(sat_refutation,[status(thm)],[f255,f285,f324,f329,f332,f451,f469,f506,f565,f613,f617,f638,f695,f717,f730,f775,f800,f810,f813,f815])).
% 0.12/0.45 % SZS output end CNFRefutation for theBenchmark.p
% 0.12/0.47 % Elapsed time: 0.112359 seconds
% 0.12/0.47 % CPU time: 0.622976 seconds
% 0.12/0.47 % Total memory used: 113.131 MB
% 0.12/0.47 % Net memory used: 111.658 MB
%------------------------------------------------------------------------------