%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWV688-1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n010.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:01 PM UTC 2026
% Result : Unsatisfiable 154.79s 20.24s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SWV688-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.16/0.44 % Computer : n010.cluster.edu
% 0.16/0.44 % Model : x86_64 x86_64
% 0.16/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.44 % Memory : 8046.5625MB
% 0.16/0.44 % OS : Linux 6.8.0-71-generic
% 0.16/0.44 % CPULimit : 300
% 0.16/0.44 % WCLimit : 300
% 0.16/0.44 % DateTime : Mon Sep 21 09:19:55 UTC 2026
% 0.16/0.44 % CPUTime :
% 0.25/0.55 % Drodi V4.1.1
% 154.79/20.24 % Refutation found
% 154.79/20.24 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 154.79/20.24 % SZS output start CNFRefutation for theBenchmark
% 154.79/20.24 fof(f43,axiom,(
% 154.79/20.24 (![T_a,V_y,V_x]: (( ~ class_Orderings_Opreorder(T_a)| ~ hBOOL(hAPP(c_lessequals(V_y,T_a),V_x))| ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(V_x,T_a),V_y)) ) ))),
% 154.79/20.24 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 154.79/20.24 fof(f131,axiom,(
% 154.79/20.24 (![T_a,V_a]: (( ~ class_Ring__and__Field_Odivision__ring(T_a)| ~ class_Ring__and__Field_Odivision__by__zero(T_a)| hAPP(c_HOL_Oinverse__class_Oinverse(T_a),hAPP(c_HOL_Oinverse__class_Oinverse(T_a),V_a)) = V_a ) ))),
% 154.79/20.24 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 154.79/20.24 fof(f235,axiom,(
% 154.79/20.24 (![V_nat_H]: (hAPP(c_Suc,V_nat_H) != c_HOL_Ozero__class_Ozero(tc_nat) ))),
% 154.79/20.24 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 154.79/20.24 fof(f250,axiom,(
% 154.79/20.24 (![V_x,V_a]: (( V_x != hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_x),V_a)| V_a = c_HOL_Ozero__class_Ozero(tc_nat) ) ))),
% 154.79/20.24 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 154.79/20.24 fof(f338,axiom,(
% 154.79/20.24 (![V_m,V_n]: (hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),hAPP(c_Suc,V_m)),V_n) = hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_m),hAPP(c_Suc,V_n)) ))),
% 154.79/20.24 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 154.79/20.24 fof(f453,axiom,(
% 154.79/20.24 (![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 ))),
% 154.79/20.24 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 154.79/20.24 fof(f454,axiom,(
% 154.79/20.24 (![V_m,V_n]: (hAPP(hAPP(c_HOL_Ominus__class_Ominus(tc_nat),hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_m),V_n)),V_n) = V_m ))),
% 154.79/20.24 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 154.79/20.24 fof(f537,axiom,(
% 154.79/20.24 (![V_n,V_m]: (( hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_n),hAPP(hAPP(c_HOL_Ominus__class_Ominus(tc_nat),V_m),V_n)) = V_m| hBOOL(hAPP(c_HOL_Oord__class_Oless(V_m,tc_nat),V_n)) ) ))),
% 154.79/20.24 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 154.79/20.24 fof(f1213,axiom,(
% 154.79/20.24 (![V_P,V_Q,T_b,T_a,T_c,V_R]: (hAPP(c_COMBB(V_P,V_Q,T_b,T_a,T_c),V_R) = hAPP(V_P,hAPP(V_Q,V_R)) ))),
% 154.79/20.24 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 154.79/20.24 fof(f1214,axiom,(
% 154.79/20.24 (![V_P,T_b,T_c,T_a,V_Q,V_R]: (hAPP(hAPP(c_COMBC(V_P,T_b,T_c,T_a),V_Q),V_R) = hAPP(hAPP(V_P,V_R),V_Q) ))),
% 154.79/20.24 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 154.79/20.24 fof(f1215,axiom,(
% 154.79/20.24 (![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)) ))),
% 154.79/20.24 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 154.79/20.24 fof(f1233,axiom,(
% 154.79/20.24 (![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)) ))),
% 154.79/20.24 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 154.79/20.24 fof(f1292,axiom,(
% 154.79/20.24 class_Orderings_Opreorder(tc_nat) ),
% 154.79/20.24 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 154.79/20.24 fof(f1365,axiom,(
% 154.79/20.24 class_Ring__and__Field_Odivision__by__zero(tc_Complex_Ocomplex) ),
% 154.79/20.24 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 154.79/20.24 fof(f1373,axiom,(
% 154.79/20.24 class_Ring__and__Field_Odivision__ring(tc_Complex_Ocomplex) ),
% 154.79/20.24 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 154.79/20.24 fof(f1473,plain,(
% 154.79/20.24 ![X0,X1,X2]: (~class_Orderings_Opreorder(X0)|~hBOOL(hAPP(c_lessequals(X1,X0),X2))|~hBOOL(hAPP(c_HOL_Oord__class_Oless(X2,X0),X1)))),
% 154.79/20.24 inference(cnf_transformation,[status(thm)],[f43])).
% 154.79/20.24 fof(f1602,plain,(
% 154.79/20.24 ![T_a]: ((~class_Ring__and__Field_Odivision__ring(T_a)|~class_Ring__and__Field_Odivision__by__zero(T_a))|(![V_a]: hAPP(c_HOL_Oinverse__class_Oinverse(T_a),hAPP(c_HOL_Oinverse__class_Oinverse(T_a),V_a))=V_a))),
% 154.79/20.24 inference(miniscoping,[status(thm)],[f131])).
% 154.79/20.24 fof(f1603,plain,(
% 154.79/20.24 ![X0,X1]: (~class_Ring__and__Field_Odivision__ring(X0)|~class_Ring__and__Field_Odivision__by__zero(X0)|hAPP(c_HOL_Oinverse__class_Oinverse(X0),hAPP(c_HOL_Oinverse__class_Oinverse(X0),X1))=X1)),
% 154.79/20.24 inference(cnf_transformation,[status(thm)],[f1602])).
% 154.79/20.24 fof(f1778,plain,(
% 154.79/20.24 ![X0]: (~hAPP(c_Suc,X0)=c_HOL_Ozero__class_Ozero(tc_nat))),
% 154.79/20.24 inference(cnf_transformation,[status(thm)],[f235])).
% 154.79/20.24 fof(f1799,plain,(
% 154.79/20.24 ![V_a]: ((![V_x]: ~V_x=hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_x),V_a))|V_a=c_HOL_Ozero__class_Ozero(tc_nat))),
% 154.79/20.24 inference(miniscoping,[status(thm)],[f250])).
% 154.79/20.24 fof(f1800,plain,(
% 154.79/20.24 ![X0,X1]: (~X0=hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),X0),X1)|X1=c_HOL_Ozero__class_Ozero(tc_nat))),
% 154.79/20.24 inference(cnf_transformation,[status(thm)],[f1799])).
% 154.79/20.24 fof(f1933,plain,(
% 154.79/20.24 ![X0,X1]: (hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),hAPP(c_Suc,X0)),X1)=hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),X0),hAPP(c_Suc,X1)))),
% 154.79/20.24 inference(cnf_transformation,[status(thm)],[f338])).
% 154.79/20.24 fof(f2115,plain,(
% 154.79/20.24 ![X0,X1]: (hAPP(hAPP(c_HOL_Ominus__class_Ominus(tc_nat),hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),X0),X1)),X0)=X1)),
% 154.79/20.24 inference(cnf_transformation,[status(thm)],[f453])).
% 154.79/20.24 fof(f2116,plain,(
% 154.79/20.24 ![X0,X1]: (hAPP(hAPP(c_HOL_Ominus__class_Ominus(tc_nat),hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),X0),X1)),X1)=X0)),
% 154.79/20.24 inference(cnf_transformation,[status(thm)],[f454])).
% 154.79/20.24 fof(f2236,plain,(
% 154.79/20.24 ![X0,X1]: (hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),X0),hAPP(hAPP(c_HOL_Ominus__class_Ominus(tc_nat),X1),X0))=X1|hBOOL(hAPP(c_HOL_Oord__class_Oless(X1,tc_nat),X0)))),
% 154.79/20.24 inference(cnf_transformation,[status(thm)],[f537])).
% 154.79/20.24 fof(f3380,plain,(
% 154.79/20.24 ![X0,X1,X2,X3,X4,X5]: (hAPP(c_COMBB(X0,X1,X2,X3,X4),X5)=hAPP(X0,hAPP(X1,X5)))),
% 154.79/20.24 inference(cnf_transformation,[status(thm)],[f1213])).
% 154.79/20.24 fof(f3381,plain,(
% 154.79/20.24 ![X0,X1,X2,X3,X4,X5]: (hAPP(hAPP(c_COMBC(X0,X1,X2,X3),X4),X5)=hAPP(hAPP(X0,X5),X4))),
% 154.79/20.24 inference(cnf_transformation,[status(thm)],[f1214])).
% 154.79/20.24 fof(f3382,plain,(
% 154.79/20.24 ![X0,X1,X2,X3,X4,X5]: (hAPP(c_COMBS(X0,X1,X2,X3,X4),X5)=hAPP(hAPP(X0,X5),hAPP(X1,X5)))),
% 154.79/20.24 inference(cnf_transformation,[status(thm)],[f1215])).
% 154.79/20.24 fof(f3411,plain,(
% 154.79/20.24 ![X0,X1]: (hBOOL(hAPP(c_lessequals(hAPP(hAPP(c_HOL_Ominus__class_Ominus(tc_nat),X0),X1),tc_nat),X0)))),
% 154.79/20.24 inference(cnf_transformation,[status(thm)],[f1233])).
% 154.79/20.24 fof(f3493,plain,(
% 154.79/20.24 class_Orderings_Opreorder(tc_nat)),
% 154.79/20.24 inference(cnf_transformation,[status(thm)],[f1292])).
% 154.79/20.24 fof(f3566,plain,(
% 154.79/20.24 class_Ring__and__Field_Odivision__by__zero(tc_Complex_Ocomplex)),
% 154.79/20.24 inference(cnf_transformation,[status(thm)],[f1365])).
% 154.79/20.24 fof(f3574,plain,(
% 154.79/20.24 class_Ring__and__Field_Odivision__ring(tc_Complex_Ocomplex)),
% 154.79/20.24 inference(cnf_transformation,[status(thm)],[f1373])).
% 154.79/20.24 fof(f3665,plain,(
% 154.79/20.24 ![X0,X1]: (hBOOL(hAPP(c_lessequals(X0,tc_nat),hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),X1),X0))))),
% 154.79/20.24 inference(paramodulation,[status(thm)],[f2115,f3411])).
% 154.79/20.24 fof(f3693,plain,(
% 154.79/20.24 ![X0,X1,X2,X3,X4,X5,X6,X7,X8]: (hAPP(c_COMBS(c_COMBC(X0,X1,X2,X3),X4,X5,X6,X7),X8)=hAPP(hAPP(X0,hAPP(X4,X8)),X8))),
% 154.79/20.24 inference(paramodulation,[status(thm)],[f3381,f3382])).
% 154.79/20.24 fof(f3709,plain,(
% 154.79/20.24 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9]: (hAPP(c_COMBS(X0,c_COMBB(X1,X2,X3,X4,X5),X6,X7,X8),X9)=hAPP(hAPP(X0,X9),hAPP(X1,hAPP(X2,X9))))),
% 154.79/20.24 inference(paramodulation,[status(thm)],[f3380,f3382])).
% 154.79/20.24 fof(f9329,plain,(
% 154.79/20.24 ![X0,X1]: (~class_Orderings_Opreorder(tc_nat)|~hBOOL(hAPP(c_HOL_Oord__class_Oless(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),X0),X1),tc_nat),X1)))),
% 154.79/20.24 inference(resolution,[status(thm)],[f1473,f3665])).
% 154.79/20.24 fof(f9362,plain,(
% 154.79/20.24 ![X0,X1]: (~hBOOL(hAPP(c_HOL_Oord__class_Oless(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),X0),X1),tc_nat),X1)))),
% 154.79/20.24 inference(forward_subsumption_resolution,[status(thm)],[f9329,f3493])).
% 154.79/20.24 fof(f11531,plain,(
% 154.79/20.24 ![X0,X1]: (hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),X0),hAPP(hAPP(c_HOL_Ominus__class_Ominus(tc_nat),hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),X1),X0)),X0))=hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),X1),X0))),
% 154.79/20.24 inference(resolution,[status(thm)],[f2236,f9362])).
% 154.79/20.24 fof(f11586,plain,(
% 154.79/20.24 ![X0,X1]: (hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),X0),X1)=hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),X1),X0))),
% 154.79/20.24 inference(forward_demodulation,[status(thm)],[f2116,f11531])).
% 154.79/20.24 fof(f11692,plain,(
% 154.79/20.24 ![X0,X1]: (~X0=hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),X1),X0)|X1=c_HOL_Ozero__class_Ozero(tc_nat))),
% 154.79/20.24 inference(paramodulation,[status(thm)],[f11586,f1800])).
% 154.79/20.24 fof(f14396,plain,(
% 154.79/20.24 ![X0]: (~class_Ring__and__Field_Odivision__ring(tc_Complex_Ocomplex)|hAPP(c_HOL_Oinverse__class_Oinverse(tc_Complex_Ocomplex),hAPP(c_HOL_Oinverse__class_Oinverse(tc_Complex_Ocomplex),X0))=X0)),
% 141.68/20.39 inference(resolution,[status(thm)],[f1603,f3566])).
% 141.68/20.39 fof(f14397,plain,(
% 141.68/20.39 ![X0]: (hAPP(c_HOL_Oinverse__class_Oinverse(tc_Complex_Ocomplex),hAPP(c_HOL_Oinverse__class_Oinverse(tc_Complex_Ocomplex),X0))=X0)),
% 141.68/20.39 inference(forward_subsumption_resolution,[status(thm)],[f14396,f3574])).
% 141.68/20.39 fof(f14411,plain,(
% 141.68/20.39 ![X0,X1,X2,X3,X4,X5,X6]: (hAPP(c_COMBS(c_COMBC(c_HOL_Oinverse__class_Oinverse(tc_Complex_Ocomplex),X0,X1,X2),c_HOL_Oinverse__class_Oinverse(tc_Complex_Ocomplex),X3,X4,X5),X6)=hAPP(X6,X6))),
% 141.68/20.39 inference(paramodulation,[status(thm)],[f14397,f3693])).
% 141.68/20.39 fof(f77277,plain,(
% 141.68/20.39 ![X0,X1]: (~X0=hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),X1),hAPP(c_Suc,X0))|hAPP(c_Suc,X1)=c_HOL_Ozero__class_Ozero(tc_nat))),
% 141.68/20.39 inference(paramodulation,[status(thm)],[f1933,f11692])).
% 141.68/20.39 fof(f77408,plain,(
% 141.68/20.39 ![X0,X1]: (~X0=hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),X1),hAPP(c_Suc,X0)))),
% 141.68/20.39 inference(forward_subsumption_resolution,[status(thm)],[f77277,f1778])).
% 141.68/20.39 fof(f77444,plain,(
% 141.68/20.39 ![X0,X1,X2,X3,X4,X5,X6,X7]: (~hAPP(X0,X1)=hAPP(c_COMBS(c_HOL_Oplus__class_Oplus(tc_nat),c_COMBB(c_Suc,X0,X2,X3,X4),X5,X6,X7),X1))),
% 141.68/20.39 inference(paramodulation,[status(thm)],[f3709,f77408])).
% 141.68/20.39 fof(f78641,plain,(
% 141.68/20.39 $false),
% 141.68/20.39 inference(resolution,[status(thm)],[f77444,f14411])).
% 141.68/20.39 % SZS output end CNFRefutation for theBenchmark.p
% 141.68/20.46 % Elapsed time: 20.002281 seconds
% 141.68/20.46 % CPU time: 156.969234 seconds
% 141.68/20.46 % Total memory used: 1.009 GB
% 141.68/20.46 % Net memory used: 985.825 MB
%------------------------------------------------------------------------------