%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWV687-1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n014.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 02:53:00 PM UTC 2026
% Result : Unsatisfiable 57.84s 7.91s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWV687-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.35 % Computer : n014.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 : Mon Sep 21 09:19:20 UTC 2026
% 0.12/0.36 % CPUTime :
% 0.21/0.49 % Drodi V4.1.1
% 57.84/7.91 % Refutation found
% 57.84/7.91 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 57.84/7.91 % SZS output start CNFRefutation for theBenchmark
% 57.84/7.91 fof(f357,axiom,(
% 57.84/7.91 (![V_n]: (hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),c_HOL_Ozero__class_Ozero(tc_nat)),V_n) = V_n ))),
% 57.84/7.91 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 57.84/7.91 fof(f392,axiom,(
% 57.84/7.91 (![V_n]: (~ hBOOL(hAPP(c_lessequals(hAPP(c_Suc,V_n),tc_nat),V_n)) ))),
% 57.84/7.91 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 57.84/7.91 fof(f453,axiom,(
% 57.84/7.91 (![V_n,V_m]: (hAPP(hAPP(c_HOL_Ominus__class_Ominus(tc_nat),hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_n),V_m)),V_n) = V_m ))),
% 57.84/7.91 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 57.84/7.91 fof(f1213,axiom,(
% 57.84/7.91 (![V_P,T_b,T_a,T_c,V_Q,V_R]: (hAPP(hAPP(c_COMBB(V_P,T_b,T_a,T_c),V_Q),V_R) = hAPP(V_P,hAPP(V_Q,V_R)) ))),
% 57.84/7.91 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 57.84/7.91 fof(f1215,axiom,(
% 57.84/7.91 (![V_P,V_Q,T_b,T_c,T_a,V_R]: (hAPP(c_COMBS(V_P,V_Q,T_b,T_c,T_a),V_R) = hAPP(hAPP(V_P,V_R),hAPP(V_Q,V_R)) ))),
% 57.84/7.91 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 57.84/7.91 fof(f1233,axiom,(
% 57.84/7.91 (![V_m,V_n]: (hBOOL(hAPP(c_lessequals(hAPP(hAPP(c_HOL_Ominus__class_Ominus(tc_nat),V_m),V_n),tc_nat),V_m)) ))),
% 57.84/7.91 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 57.84/7.91 fof(f1959,plain,(
% 57.84/7.91 ![X0]: (hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),c_HOL_Ozero__class_Ozero(tc_nat)),X0)=X0)),
% 57.84/7.91 inference(cnf_transformation,[status(thm)],[f357])).
% 57.84/7.91 fof(f2021,plain,(
% 57.84/7.91 ![X0]: (~hBOOL(hAPP(c_lessequals(hAPP(c_Suc,X0),tc_nat),X0)))),
% 57.84/7.91 inference(cnf_transformation,[status(thm)],[f392])).
% 57.84/7.91 fof(f2115,plain,(
% 57.84/7.91 ![X0,X1]: (hAPP(hAPP(c_HOL_Ominus__class_Ominus(tc_nat),hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),X0),X1)),X0)=X1)),
% 57.84/7.91 inference(cnf_transformation,[status(thm)],[f453])).
% 57.84/7.91 fof(f3380,plain,(
% 57.84/7.91 ![X0,X1,X2,X3,X4,X5]: (hAPP(hAPP(c_COMBB(X0,X1,X2,X3),X4),X5)=hAPP(X0,hAPP(X4,X5)))),
% 57.84/7.91 inference(cnf_transformation,[status(thm)],[f1213])).
% 57.84/7.91 fof(f3382,plain,(
% 57.84/7.91 ![X0,X1,X2,X3,X4,X5]: (hAPP(c_COMBS(X0,X1,X2,X3,X4),X5)=hAPP(hAPP(X0,X5),hAPP(X1,X5)))),
% 57.84/7.91 inference(cnf_transformation,[status(thm)],[f1215])).
% 57.84/7.92 fof(f3411,plain,(
% 57.84/7.92 ![X0,X1]: (hBOOL(hAPP(c_lessequals(hAPP(hAPP(c_HOL_Ominus__class_Ominus(tc_nat),X0),X1),tc_nat),X0)))),
% 57.84/7.92 inference(cnf_transformation,[status(thm)],[f1233])).
% 57.84/7.92 fof(f3693,plain,(
% 57.84/7.92 ![X0,X1,X2,X3,X4,X5,X6,X7,X8]: (hAPP(c_COMBS(c_COMBB(X0,X1,X2,X3),X4,X5,X6,X7),X8)=hAPP(X0,hAPP(X8,hAPP(X4,X8))))),
% 57.84/7.92 inference(paramodulation,[status(thm)],[f3380,f3382])).
% 57.84/7.92 fof(f3718,plain,(
% 57.84/7.92 ![X0,X1,X2,X3,X4]: (hAPP(hAPP(c_HOL_Ominus__class_Ominus(tc_nat),hAPP(c_COMBS(c_HOL_Oplus__class_Oplus(tc_nat),X0,X1,X2,X3),X4)),X4)=hAPP(X0,X4))),
% 57.84/7.92 inference(paramodulation,[status(thm)],[f3382,f2115])).
% 57.84/7.92 fof(f4052,plain,(
% 57.84/7.92 ![X0,X1,X2,X3,X4,X5,X6,X7]: (~hBOOL(hAPP(c_lessequals(hAPP(c_COMBS(c_COMBB(c_Suc,X0,X1,X2),X3,X4,X5,X6),X7),tc_nat),hAPP(X7,hAPP(X3,X7)))))),
% 57.84/7.92 inference(paramodulation,[status(thm)],[f3693,f2021])).
% 57.84/7.92 fof(f4499,plain,(
% 57.84/7.92 ![X0,X1,X2,X3,X4]: (hBOOL(hAPP(c_lessequals(hAPP(X0,X1),tc_nat),hAPP(c_COMBS(c_HOL_Oplus__class_Oplus(tc_nat),X0,X2,X3,X4),X1))))),
% 57.84/7.92 inference(paramodulation,[status(thm)],[f3718,f3411])).
% 57.84/7.92 fof(f11277,plain,(
% 57.84/7.92 ![X0,X1,X2,X3,X4,X5,X6]: (~hBOOL(hAPP(c_lessequals(hAPP(c_COMBS(c_COMBB(c_Suc,X0,X1,X2),hAPP(c_HOL_Oplus__class_Oplus(tc_nat),c_HOL_Ozero__class_Ozero(tc_nat)),X3,X4,X5),X6),tc_nat),hAPP(X6,X6))))),
% 57.84/7.92 inference(paramodulation,[status(thm)],[f1959,f4052])).
% 57.84/7.92 fof(f11286,plain,(
% 57.84/7.92 $false),
% 57.84/7.92 inference(resolution,[status(thm)],[f11277,f4499])).
% 57.84/7.92 % SZS output end CNFRefutation for theBenchmark.p
% 8.75/7.94 % Elapsed time: 7.564030 seconds
% 8.75/7.94 % CPU time: 58.494683 seconds
% 8.75/7.94 % Total memory used: 621.162 MB
% 8.75/7.94 % Net memory used: 608.643 MB
%------------------------------------------------------------------------------