%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWV682-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 52.33s 12.08s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SWV682-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.07 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.19/0.45 % Computer : n014.cluster.edu
% 0.19/0.45 % Model : x86_64 x86_64
% 0.19/0.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.19/0.45 % Memory : 8046.5625MB
% 0.19/0.45 % OS : Linux 6.8.0-71-generic
% 0.19/0.45 % CPULimit : 300
% 0.19/0.45 % WCLimit : 300
% 0.19/0.45 % DateTime : Mon Sep 21 09:19:04 UTC 2026
% 0.19/0.46 % CPUTime :
% 0.24/0.60 % Drodi V4.1.1
% 52.33/12.08 % Refutation found
% 52.33/12.08 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 52.33/12.08 % SZS output start CNFRefutation for theBenchmark
% 52.33/12.08 fof(f150,axiom,(
% 52.33/12.08 (![V_n]: (~ hBOOL(hAPP(c_lessequals(hAPP(c_Suc,V_n),tc_nat),V_n)) ))),
% 52.33/12.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 52.33/12.08 fof(f161,axiom,(
% 52.33/12.08 (![V_x]: (hBOOL(hAPP(c_lessequals(V_x,tc_nat),V_x)) ))),
% 52.33/12.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 52.33/12.08 fof(f272,axiom,(
% 52.33/12.08 (![V_n]: (hAPP(hAPP(c_HOL_Otimes__class_Otimes(tc_nat),c_HOL_Oone__class_Oone(tc_nat)),V_n) = V_n ))),
% 52.33/12.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 52.33/12.08 fof(f873,axiom,(
% 52.33/12.08 (![T_b,T_a,T_c,V_P,V_Q,V_R]: (hAPP(hAPP(hAPP(c_COMBB(T_b,T_a,T_c),V_P),V_Q),V_R) = hAPP(V_P,hAPP(V_Q,V_R)) ))),
% 52.33/12.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 52.33/12.08 fof(f875,axiom,(
% 52.33/12.08 (![T_b,T_c,T_a,V_P,V_Q,V_R]: (hAPP(hAPP(hAPP(c_COMBS(T_b,T_c,T_a),V_P),V_Q),V_R) = hAPP(hAPP(V_P,V_R),hAPP(V_Q,V_R)) ))),
% 52.33/12.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 52.33/12.08 fof(f1203,plain,(
% 52.33/12.08 ![X0]: (~hBOOL(hAPP(c_lessequals(hAPP(c_Suc,X0),tc_nat),X0)))),
% 52.33/12.08 inference(cnf_transformation,[status(thm)],[f150])).
% 52.33/12.08 fof(f1222,plain,(
% 52.33/12.08 ![X0]: (hBOOL(hAPP(c_lessequals(X0,tc_nat),X0)))),
% 52.33/12.08 inference(cnf_transformation,[status(thm)],[f161])).
% 52.33/12.08 fof(f1415,plain,(
% 52.33/12.08 ![X0]: (hAPP(hAPP(c_HOL_Otimes__class_Otimes(tc_nat),c_HOL_Oone__class_Oone(tc_nat)),X0)=X0)),
% 52.33/12.08 inference(cnf_transformation,[status(thm)],[f272])).
% 52.33/12.08 fof(f2426,plain,(
% 52.33/12.08 ![X0,X1,X2,X3,X4,X5]: (hAPP(hAPP(hAPP(c_COMBB(X0,X1,X2),X3),X4),X5)=hAPP(X3,hAPP(X4,X5)))),
% 52.33/12.08 inference(cnf_transformation,[status(thm)],[f873])).
% 52.33/12.08 fof(f2428,plain,(
% 52.33/12.08 ![X0,X1,X2,X3,X4,X5]: (hAPP(hAPP(hAPP(c_COMBS(X0,X1,X2),X3),X4),X5)=hAPP(hAPP(X3,X5),hAPP(X4,X5)))),
% 52.33/12.08 inference(cnf_transformation,[status(thm)],[f875])).
% 52.33/12.08 fof(f2612,plain,(
% 52.33/12.08 ![X0,X1,X2,X3,X4,X5,X6,X7,X8]: (hAPP(hAPP(hAPP(c_COMBS(X0,X1,X2),hAPP(c_COMBB(X3,X4,X5),X6)),X7),X8)=hAPP(X6,hAPP(X8,hAPP(X7,X8))))),
% 52.33/12.08 inference(paramodulation,[status(thm)],[f2426,f2428])).
% 52.33/12.08 fof(f2830,plain,(
% 52.33/12.08 ![X0,X1,X2,X3,X4,X5,X6,X7]: (~hBOOL(hAPP(c_lessequals(hAPP(hAPP(hAPP(c_COMBS(X0,X1,X2),hAPP(c_COMBB(X3,X4,X5),c_Suc)),X6),X7),tc_nat),hAPP(X7,hAPP(X6,X7)))))),
% 52.33/12.08 inference(paramodulation,[status(thm)],[f2612,f1203])).
% 52.33/12.08 fof(f10716,plain,(
% 52.33/12.08 ![X0,X1,X2,X3,X4,X5,X6]: (~hBOOL(hAPP(c_lessequals(hAPP(hAPP(hAPP(c_COMBS(X0,X1,X2),hAPP(c_COMBB(X3,X4,X5),c_Suc)),hAPP(c_HOL_Otimes__class_Otimes(tc_nat),c_HOL_Oone__class_Oone(tc_nat))),X6),tc_nat),hAPP(X6,X6))))),
% 52.33/12.08 inference(paramodulation,[status(thm)],[f1415,f2830])).
% 52.33/12.08 fof(f11063,plain,(
% 52.33/12.08 $false),
% 52.33/12.08 inference(resolution,[status(thm)],[f10716,f1222])).
% 52.33/12.08 % SZS output end CNFRefutation for theBenchmark.p
% 52.33/12.08 % Elapsed time: 11.602328 seconds
% 52.33/12.08 % CPU time: 90.573327 seconds
% 52.33/12.08 % Total memory used: 843.988 MB
% 52.33/12.08 % Net memory used: 828.095 MB
%------------------------------------------------------------------------------