%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : HWV023-1 : TPTP v9.3.1. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n017.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.41s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : HWV023-1 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.36 % Computer : n017.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Sun Sep 20 20:43:56 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.14/0.38 % Drodi V4.1.1
% 0.14/0.41 % Refutation found
% 0.14/0.41 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.14/0.41 % SZS output start CNFRefutation for theBenchmark
% 0.14/0.41 fof(f2,axiom,(
% 0.14/0.41 (![X_1]: (gt(plus(X_1,n1),n0) ))),
% 0.14/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.41 fof(f5,axiom,(
% 0.14/0.41 (![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.14/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.41 fof(f7,axiom,(
% 0.14/0.41 (![Y_4,X_3]: (( ~ def_10(Y_4,X_3)| X_3 != Y_4 ) ))),
% 0.14/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.41 fof(f19,axiom,(
% 0.14/0.41 (![X_31]: (plus(n0,X_31) = X_31 ))),
% 0.14/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.41 fof(f21,axiom,(
% 0.14/0.41 (![X_t_32]: (level(X_t_32) = int_level(X_t_32) ))),
% 0.14/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.41 fof(f24,axiom,(
% 0.14/0.41 (![X_t_35]: (( int_level(X_t_35) != n0| p_Empty(X_t_35) ) ))),
% 0.14/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.41 fof(f71,axiom,(
% 0.14/0.41 (![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)) = minus(int_level(X_t_42),n1) ) ))),
% 0.14/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.42 fof(f91,negated_conjecture,(
% 0.14/0.42 level(t_139) = n1 ),
% 0.14/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.42 fof(f92,negated_conjecture,(
% 0.14/0.42 ~ p_Wr(t_139) ),
% 0.14/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.42 fof(f93,negated_conjecture,(
% 0.14/0.42 p_Rd(t_139) ),
% 0.14/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.42 fof(f94,negated_conjecture,(
% 0.14/0.42 ~ p_Reset(t_139) ),
% 0.14/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.42 fof(f95,negated_conjecture,(
% 0.14/0.42 ~ p_Empty(plus(t_139,n1)) ),
% 0.14/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.42 fof(f97,plain,(
% 0.14/0.42 ![X0]: (gt(plus(X0,n1),n0))),
% 0.14/0.42 inference(cnf_transformation,[status(thm)],[f2])).
% 0.14/0.42 fof(f101,plain,(
% 0.14/0.42 ![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.14/0.42 inference(miniscoping,[status(thm)],[f5])).
% 0.14/0.42 fof(f102,plain,(
% 0.14/0.42 ![X0,X1,X2]: (minus(X0,X1)=X2|~plus(X2,X1)=X0|def_10(X1,X0))),
% 0.14/0.42 inference(cnf_transformation,[status(thm)],[f101])).
% 0.14/0.42 fof(f104,plain,(
% 0.14/0.42 ![X0,X1]: (~def_10(X0,X1)|~X1=X0)),
% 0.14/0.42 inference(cnf_transformation,[status(thm)],[f7])).
% 0.14/0.42 fof(f117,plain,(
% 0.14/0.42 ![X0]: (plus(n0,X0)=X0)),
% 0.14/0.42 inference(cnf_transformation,[status(thm)],[f19])).
% 0.14/0.42 fof(f119,plain,(
% 0.14/0.42 ![X0]: (level(X0)=int_level(X0))),
% 0.14/0.42 inference(cnf_transformation,[status(thm)],[f21])).
% 0.14/0.42 fof(f122,plain,(
% 0.14/0.42 ![X0]: (~int_level(X0)=n0|p_Empty(X0))),
% 0.14/0.42 inference(cnf_transformation,[status(thm)],[f24])).
% 0.14/0.42 fof(f171,plain,(
% 0.14/0.42 ![X0]: (p_Reset(X0)|p_Wr(X0)|~p_Rd(X0)|~gt(int_level(X0),n0)|int_level(plus(X0,n1))=minus(int_level(X0),n1))),
% 0.14/0.42 inference(cnf_transformation,[status(thm)],[f71])).
% 0.14/0.42 fof(f191,plain,(
% 0.14/0.42 level(t_139)=n1),
% 0.14/0.42 inference(cnf_transformation,[status(thm)],[f91])).
% 0.14/0.42 fof(f192,plain,(
% 0.14/0.42 ~p_Wr(t_139)),
% 0.14/0.42 inference(cnf_transformation,[status(thm)],[f92])).
% 0.14/0.42 fof(f193,plain,(
% 0.14/0.42 p_Rd(t_139)),
% 0.14/0.42 inference(cnf_transformation,[status(thm)],[f93])).
% 0.14/0.42 fof(f194,plain,(
% 0.14/0.42 ~p_Reset(t_139)),
% 0.14/0.42 inference(cnf_transformation,[status(thm)],[f94])).
% 0.14/0.42 fof(f195,plain,(
% 0.14/0.42 ~p_Empty(plus(t_139,n1))),
% 0.14/0.42 inference(cnf_transformation,[status(thm)],[f95])).
% 0.14/0.42 fof(f197,plain,(
% 0.14/0.42 ![X0,X1]: (minus(plus(X0,X1),X1)=X0|def_10(X1,plus(X0,X1)))),
% 0.14/0.42 inference(destructive_equality_resolution,[status(thm)],[f102])).
% 0.14/0.42 fof(f198,plain,(
% 0.14/0.42 ![X0]: (~def_10(X0,X0))),
% 0.14/0.42 inference(destructive_equality_resolution,[status(thm)],[f104])).
% 0.14/0.42 fof(f201,plain,(
% 0.14/0.42 ![X0]: (~level(X0)=n0|p_Empty(X0))),
% 0.14/0.42 inference(forward_demodulation,[status(thm)],[f119,f122])).
% 0.14/0.42 fof(f264,plain,(
% 0.14/0.42 ![X0]: (p_Reset(X0)|p_Wr(X0)|~p_Rd(X0)|~gt(level(X0),n0)|int_level(plus(X0,n1))=minus(int_level(X0),n1))),
% 0.14/0.42 inference(forward_demodulation,[status(thm)],[f119,f171])).
% 0.14/0.42 fof(f265,plain,(
% 0.14/0.42 ![X0]: (p_Reset(X0)|p_Wr(X0)|~p_Rd(X0)|~gt(level(X0),n0)|level(plus(X0,n1))=minus(int_level(X0),n1))),
% 0.14/0.42 inference(forward_demodulation,[status(thm)],[f119,f264])).
% 0.14/0.42 fof(f266,plain,(
% 0.14/0.42 ![X0]: (p_Reset(X0)|p_Wr(X0)|~p_Rd(X0)|~gt(level(X0),n0)|level(plus(X0,n1))=minus(level(X0),n1))),
% 0.14/0.42 inference(forward_demodulation,[status(thm)],[f119,f265])).
% 0.14/0.42 fof(f319,plain,(
% 0.14/0.42 gt(n1,n0)),
% 0.14/0.42 inference(paramodulation,[status(thm)],[f117,f97])).
% 0.14/0.42 fof(f322,plain,(
% 0.14/0.42 ~level(plus(t_139,n1))=n0),
% 0.14/0.42 inference(resolution,[status(thm)],[f195,f201])).
% 0.14/0.42 fof(f347,plain,(
% 0.14/0.42 ![X0]: (minus(plus(n0,X0),X0)=n0|def_10(X0,X0))),
% 0.14/0.42 inference(paramodulation,[status(thm)],[f117,f197])).
% 0.14/0.42 fof(f348,plain,(
% 0.14/0.42 ![X0]: (minus(X0,X0)=n0|def_10(X0,X0))),
% 0.14/0.42 inference(forward_demodulation,[status(thm)],[f117,f347])).
% 0.14/0.42 fof(f351,plain,(
% 0.14/0.42 ![X0]: (minus(X0,X0)=n0)),
% 0.14/0.42 inference(forward_subsumption_resolution,[status(thm)],[f348,f198])).
% 0.14/0.42 fof(f366,plain,(
% 0.14/0.42 p_Reset(t_139)|p_Wr(t_139)|~gt(level(t_139),n0)|level(plus(t_139,n1))=minus(level(t_139),n1)),
% 0.14/0.42 inference(resolution,[status(thm)],[f266,f193])).
% 0.14/0.42 fof(f368,plain,(
% 0.14/0.42 p_Reset(t_139)|p_Wr(t_139)|~gt(n1,n0)|level(plus(t_139,n1))=minus(level(t_139),n1)),
% 0.14/0.42 inference(forward_demodulation,[status(thm)],[f191,f366])).
% 0.14/0.42 fof(f369,plain,(
% 0.14/0.42 p_Reset(t_139)|p_Wr(t_139)|~gt(n1,n0)|level(plus(t_139,n1))=minus(n1,n1)),
% 0.14/0.42 inference(forward_demodulation,[status(thm)],[f191,f368])).
% 0.14/0.42 fof(f370,plain,(
% 0.14/0.42 p_Reset(t_139)|p_Wr(t_139)|~gt(n1,n0)|level(plus(t_139,n1))=n0),
% 0.14/0.42 inference(forward_demodulation,[status(thm)],[f351,f369])).
% 0.14/0.42 fof(f371,plain,(
% 0.14/0.42 p_Wr(t_139)|~gt(n1,n0)|level(plus(t_139,n1))=n0),
% 0.14/0.42 inference(forward_subsumption_resolution,[status(thm)],[f370,f194])).
% 0.14/0.42 fof(f421,plain,(
% 0.14/0.42 p_Wr(t_139)|level(plus(t_139,n1))=n0),
% 0.14/0.42 inference(resolution,[status(thm)],[f371,f319])).
% 0.14/0.42 fof(f427,plain,(
% 0.14/0.42 ~n0=n0),
% 0.14/0.42 inference(backward_demodulation,[status(thm)],[f428,f322])).
% 0.14/0.42 fof(f428,plain,(
% 0.14/0.42 level(plus(t_139,n1))=n0),
% 0.14/0.42 inference(forward_subsumption_resolution,[status(thm)],[f421,f192])).
% 0.14/0.42 fof(f429,plain,(
% 0.14/0.42 $false),
% 0.14/0.42 inference(trivial_equality_resolution,[status(thm)],[f427])).
% 0.14/0.42 % SZS output end CNFRefutation for theBenchmark.p
% 0.14/0.45 % Elapsed time: 0.069535 seconds
% 0.14/0.45 % CPU time: 0.233889 seconds
% 0.14/0.45 % Total memory used: 106.267 MB
% 0.14/0.45 % Net memory used: 105.996 MB
%------------------------------------------------------------------------------