%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWV691-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 : 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 02:53:01 PM UTC 2026
% Result : Unsatisfiable 74.46s 10.13s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SWV691-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.07 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.18/0.46 % Computer : n017.cluster.edu
% 0.18/0.46 % Model : x86_64 x86_64
% 0.18/0.46 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.46 % Memory : 8046.5625MB
% 0.18/0.46 % OS : Linux 6.8.0-71-generic
% 0.18/0.46 % CPULimit : 300
% 0.18/0.46 % WCLimit : 300
% 0.18/0.46 % DateTime : Mon Sep 21 09:14:43 UTC 2026
% 0.18/0.47 % CPUTime :
% 0.37/0.63 % Drodi V4.1.1
% 74.46/10.13 % Refutation found
% 74.46/10.13 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 74.46/10.13 % SZS output start CNFRefutation for theBenchmark
% 74.46/10.13 fof(f4,axiom,(
% 74.46/10.13 (![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 ) ))),
% 74.46/10.13 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 74.46/10.13 fof(f5,axiom,(
% 74.46/10.13 (![V_m,V_n]: (hAPP(hAPP(c_HOL_Otimes__class_Otimes(tc_nat),V_m),V_n) = hAPP(hAPP(c_HOL_Otimes__class_Otimes(tc_nat),V_n),V_m) ))),
% 74.46/10.13 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 74.46/10.13 fof(f14,axiom,(
% 74.46/10.13 (![V_k,V_m,V_n]: (( hAPP(hAPP(c_HOL_Otimes__class_Otimes(tc_nat),V_k),V_m) != hAPP(hAPP(c_HOL_Otimes__class_Otimes(tc_nat),V_k),V_n)| ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),V_k))| V_m = V_n ) ))),
% 74.46/10.13 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 74.46/10.13 fof(f53,axiom,(
% 74.46/10.13 (![V_m,V_n]: (hAPP(hAPP(c_HOL_Otimes__class_Otimes(tc_nat),hAPP(c_Suc,V_m)),V_n) = hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_n),hAPP(hAPP(c_HOL_Otimes__class_Otimes(tc_nat),V_m),V_n)) ))),
% 74.46/10.13 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 74.46/10.13 fof(f197,axiom,(
% 74.46/10.13 (![V_n]: (( hBOOL(hAPP(c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),V_n))| V_n = c_HOL_Ozero__class_Ozero(tc_nat) ) ))),
% 74.46/10.13 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 74.46/10.13 fof(f198,axiom,(
% 74.46/10.13 (![V_n]: (hAPP(hAPP(c_HOL_Otimes__class_Otimes(tc_nat),c_HOL_Ozero__class_Ozero(tc_nat)),V_n) = c_HOL_Ozero__class_Ozero(tc_nat) ))),
% 74.46/10.13 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 74.46/10.13 fof(f199,axiom,(
% 74.46/10.13 (![V_m]: (hAPP(hAPP(c_HOL_Otimes__class_Otimes(tc_nat),V_m),c_HOL_Ozero__class_Ozero(tc_nat)) = c_HOL_Ozero__class_Ozero(tc_nat) ))),
% 74.46/10.13 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 74.46/10.13 fof(f211,axiom,(
% 74.46/10.13 (![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) ) ))),
% 74.46/10.13 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 74.46/10.13 fof(f214,axiom,(
% 74.46/10.13 (![V_x]: (V_x = hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_x),c_HOL_Ozero__class_Ozero(tc_nat)) ))),
% 74.46/10.13 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 74.46/10.13 fof(f216,axiom,(
% 74.46/10.13 (![V_n]: (hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),c_HOL_Ozero__class_Ozero(tc_nat)),V_n) = V_n ))),
% 74.46/10.13 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 74.46/10.13 fof(f249,axiom,(
% 74.46/10.13 (![V_m,V_n]: (hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_m),V_n) = hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_n),V_m) ))),
% 74.46/10.13 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 74.46/10.13 fof(f282,axiom,(
% 74.46/10.13 (![V_j,V_i]: (~ hBOOL(hAPP(c_HOL_Oord__class_Oless(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_j),V_i),tc_nat),V_i)) ))),
% 74.46/10.13 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 74.46/10.13 fof(f285,axiom,(
% 74.46/10.13 (![V_i,V_k,V_j]: (( hBOOL(hAPP(c_HOL_Oord__class_Oless(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_i),V_k),tc_nat),V_j))| ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(V_i,tc_nat),hAPP(hAPP(c_HOL_Ominus__class_Ominus(tc_nat),V_j),V_k))) ) ))),
% 74.46/10.13 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 74.46/10.13 fof(f386,axiom,(
% 74.46/10.13 (![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 ))),
% 74.46/10.13 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 74.46/10.13 fof(f600,axiom,(
% 74.46/10.13 (![V_k]: (hBOOL(hAPP(c_HOL_Oord__class_Oless(hAPP(hAPP(c_HOL_Ominus__class_Ominus(tc_nat),v_i),V_k),tc_nat),v_n)) ))),
% 74.46/10.13 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 74.46/10.13 fof(f666,axiom,(
% 74.46/10.13 (![V_m]: (c_HOL_Ozero__class_Ozero(tc_nat) != hAPP(c_Suc,V_m) ))),
% 74.46/10.13 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 74.46/10.13 fof(f889,axiom,(
% 74.46/10.13 (![V_m]: (hAPP(hAPP(c_HOL_Ominus__class_Ominus(tc_nat),V_m),V_m) = c_HOL_Ozero__class_Ozero(tc_nat) ))),
% 74.46/10.13 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 74.46/10.13 fof(f929,axiom,(
% 74.46/10.13 (![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) ))),
% 74.46/10.13 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 74.46/10.13 fof(f930,axiom,(
% 74.46/10.13 (![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)) ))),
% 74.46/10.13 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 74.46/10.13 fof(f1034,axiom,(
% 74.46/10.13 class_Ring__and__Field_Odivision__by__zero(tc_Complex_Ocomplex) ),
% 74.46/10.13 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 74.46/10.13 fof(f1042,axiom,(
% 74.46/10.13 class_Ring__and__Field_Odivision__ring(tc_Complex_Ocomplex) ),
% 74.46/10.13 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 74.46/10.13 fof(f1073,plain,(
% 74.46/10.13 ![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))),
% 74.46/10.13 inference(miniscoping,[status(thm)],[f4])).
% 74.46/10.13 fof(f1074,plain,(
% 74.46/10.13 ![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)),
% 74.46/10.13 inference(cnf_transformation,[status(thm)],[f1073])).
% 74.46/10.13 fof(f1075,plain,(
% 74.46/10.13 ![X0,X1]: (hAPP(hAPP(c_HOL_Otimes__class_Otimes(tc_nat),X0),X1)=hAPP(hAPP(c_HOL_Otimes__class_Otimes(tc_nat),X1),X0))),
% 74.46/10.13 inference(cnf_transformation,[status(thm)],[f5])).
% 74.46/10.13 fof(f1089,plain,(
% 74.46/10.13 ![V_m,V_n]: ((![V_k]: (~hAPP(hAPP(c_HOL_Otimes__class_Otimes(tc_nat),V_k),V_m)=hAPP(hAPP(c_HOL_Otimes__class_Otimes(tc_nat),V_k),V_n)|~hBOOL(hAPP(c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),V_k))))|V_m=V_n)),
% 74.46/10.13 inference(miniscoping,[status(thm)],[f14])).
% 74.46/10.13 fof(f1090,plain,(
% 74.46/10.13 ![X0,X1,X2]: (~hAPP(hAPP(c_HOL_Otimes__class_Otimes(tc_nat),X0),X1)=hAPP(hAPP(c_HOL_Otimes__class_Otimes(tc_nat),X0),X2)|~hBOOL(hAPP(c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),X0))|X1=X2)),
% 74.46/10.13 inference(cnf_transformation,[status(thm)],[f1089])).
% 74.46/10.13 fof(f1149,plain,(
% 74.46/10.13 ![X0,X1]: (hAPP(hAPP(c_HOL_Otimes__class_Otimes(tc_nat),hAPP(c_Suc,X0)),X1)=hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),X1),hAPP(hAPP(c_HOL_Otimes__class_Otimes(tc_nat),X0),X1)))),
% 74.46/10.13 inference(cnf_transformation,[status(thm)],[f53])).
% 74.46/10.13 fof(f1382,plain,(
% 74.46/10.13 ![X0]: (hBOOL(hAPP(c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),X0))|X0=c_HOL_Ozero__class_Ozero(tc_nat))),
% 74.46/10.13 inference(cnf_transformation,[status(thm)],[f197])).
% 74.46/10.13 fof(f1383,plain,(
% 74.46/10.13 ![X0]: (hAPP(hAPP(c_HOL_Otimes__class_Otimes(tc_nat),c_HOL_Ozero__class_Ozero(tc_nat)),X0)=c_HOL_Ozero__class_Ozero(tc_nat))),
% 74.46/10.13 inference(cnf_transformation,[status(thm)],[f198])).
% 74.46/10.13 fof(f1384,plain,(
% 74.46/10.13 ![X0]: (hAPP(hAPP(c_HOL_Otimes__class_Otimes(tc_nat),X0),c_HOL_Ozero__class_Ozero(tc_nat))=c_HOL_Ozero__class_Ozero(tc_nat))),
% 74.46/10.13 inference(cnf_transformation,[status(thm)],[f199])).
% 74.46/10.13 fof(f1403,plain,(
% 74.46/10.13 ![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))),
% 74.46/10.13 inference(miniscoping,[status(thm)],[f211])).
% 74.46/10.13 fof(f1404,plain,(
% 74.46/10.13 ![X0,X1]: (~X0=hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),X0),X1)|X1=c_HOL_Ozero__class_Ozero(tc_nat))),
% 74.46/10.13 inference(cnf_transformation,[status(thm)],[f1403])).
% 74.46/10.13 fof(f1408,plain,(
% 74.46/10.13 ![X0]: (X0=hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),X0),c_HOL_Ozero__class_Ozero(tc_nat)))),
% 74.46/10.13 inference(cnf_transformation,[status(thm)],[f214])).
% 74.46/10.13 fof(f1410,plain,(
% 74.46/10.13 ![X0]: (hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),c_HOL_Ozero__class_Ozero(tc_nat)),X0)=X0)),
% 74.46/10.13 inference(cnf_transformation,[status(thm)],[f216])).
% 74.46/10.13 fof(f1462,plain,(
% 74.46/10.13 ![X0,X1]: (hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),X0),X1)=hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),X1),X0))),
% 74.46/10.13 inference(cnf_transformation,[status(thm)],[f249])).
% 74.46/10.13 fof(f1512,plain,(
% 74.46/10.13 ![X0,X1]: (~hBOOL(hAPP(c_HOL_Oord__class_Oless(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),X0),X1),tc_nat),X1)))),
% 74.46/10.13 inference(cnf_transformation,[status(thm)],[f282])).
% 74.46/10.13 fof(f1515,plain,(
% 74.46/10.13 ![X0,X1,X2]: (hBOOL(hAPP(c_HOL_Oord__class_Oless(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),X0),X1),tc_nat),X2))|~hBOOL(hAPP(c_HOL_Oord__class_Oless(X0,tc_nat),hAPP(hAPP(c_HOL_Ominus__class_Ominus(tc_nat),X2),X1))))),
% 74.46/10.13 inference(cnf_transformation,[status(thm)],[f285])).
% 74.46/10.13 fof(f1678,plain,(
% 74.46/10.13 ![X0,X1]: (hAPP(hAPP(c_HOL_Ominus__class_Ominus(tc_nat),hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),X0),X1)),X1)=X0)),
% 74.46/10.13 inference(cnf_transformation,[status(thm)],[f386])).
% 74.46/10.13 fof(f2028,plain,(
% 74.46/10.13 ![X0]: (hBOOL(hAPP(c_HOL_Oord__class_Oless(hAPP(hAPP(c_HOL_Ominus__class_Ominus(tc_nat),v_i),X0),tc_nat),v_n)))),
% 74.46/10.13 inference(cnf_transformation,[status(thm)],[f600])).
% 74.46/10.13 fof(f2130,plain,(
% 74.46/10.13 ![X0]: (~c_HOL_Ozero__class_Ozero(tc_nat)=hAPP(c_Suc,X0))),
% 74.46/10.13 inference(cnf_transformation,[status(thm)],[f666])).
% 74.46/10.13 fof(f2523,plain,(
% 74.46/10.13 ![X0]: (hAPP(hAPP(c_HOL_Ominus__class_Ominus(tc_nat),X0),X0)=c_HOL_Ozero__class_Ozero(tc_nat))),
% 74.46/10.13 inference(cnf_transformation,[status(thm)],[f889])).
% 74.46/10.13 fof(f2592,plain,(
% 74.46/10.13 ![X0,X1,X2,X3,X4,X5]: (hAPP(hAPP(c_COMBC(X0,X1,X2,X3),X4),X5)=hAPP(hAPP(X0,X5),X4))),
% 74.46/10.13 inference(cnf_transformation,[status(thm)],[f929])).
% 74.46/10.13 fof(f2593,plain,(
% 74.46/10.13 ![X0,X1,X2,X3,X4,X5]: (hAPP(c_COMBS(X0,X1,X2,X3,X4),X5)=hAPP(hAPP(X0,X5),hAPP(X1,X5)))),
% 74.46/10.13 inference(cnf_transformation,[status(thm)],[f930])).
% 74.46/10.13 fof(f2744,plain,(
% 74.46/10.13 class_Ring__and__Field_Odivision__by__zero(tc_Complex_Ocomplex)),
% 74.46/10.13 inference(cnf_transformation,[status(thm)],[f1034])).
% 74.46/10.13 fof(f2752,plain,(
% 74.46/10.13 class_Ring__and__Field_Odivision__ring(tc_Complex_Ocomplex)),
% 74.46/10.13 inference(cnf_transformation,[status(thm)],[f1042])).
% 74.46/10.13 fof(f2950,plain,(
% 74.46/10.13 ![X0,X1]: (~X0=hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),X1),X0)|X1=c_HOL_Ozero__class_Ozero(tc_nat))),
% 74.46/10.13 inference(paramodulation,[status(thm)],[f1462,f1404])).
% 74.46/10.13 fof(f3012,plain,(
% 74.46/10.13 ![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))),
% 74.46/10.13 inference(paramodulation,[status(thm)],[f2592,f2593])).
% 74.46/10.13 fof(f3063,plain,(
% 74.46/10.13 ![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)),hAPP(X0,X4))=X4)),
% 74.46/10.13 inference(paramodulation,[status(thm)],[f2593,f1678])).
% 74.46/10.13 fof(f3065,plain,(
% 74.46/10.13 ![X0,X1,X2,X3,X4]: (~hAPP(X0,X1)=hAPP(c_COMBS(c_HOL_Oplus__class_Oplus(tc_nat),X0,X2,X3,X4),X1)|X1=c_HOL_Ozero__class_Ozero(tc_nat))),
% 74.46/10.13 inference(paramodulation,[status(thm)],[f2593,f2950])).
% 74.46/10.13 fof(f3067,plain,(
% 74.46/10.13 ![X0,X1,X2,X3,X4]: (~hBOOL(hAPP(c_HOL_Oord__class_Oless(hAPP(c_COMBS(c_HOL_Oplus__class_Oplus(tc_nat),X0,X1,X2,X3),X4),tc_nat),hAPP(X0,X4))))),
% 74.46/10.13 inference(paramodulation,[status(thm)],[f2593,f1512])).
% 74.46/10.13 fof(f3189,plain,(
% 74.46/10.13 hBOOL(hAPP(c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),v_n))),
% 74.46/10.13 inference(paramodulation,[status(thm)],[f2523,f2028])).
% 74.46/10.13 fof(f3191,plain,(
% 74.46/10.13 ![X0,X1]: (~hAPP(hAPP(c_HOL_Otimes__class_Otimes(tc_nat),v_n),X0)=hAPP(hAPP(c_HOL_Otimes__class_Otimes(tc_nat),v_n),X1)|X0=X1)),
% 74.46/10.13 inference(resolution,[status(thm)],[f3189,f1090])).
% 74.46/10.13 fof(f3535,plain,(
% 74.46/10.13 ![X0]: (~class_Ring__and__Field_Odivision__by__zero(tc_Complex_Ocomplex)|hAPP(c_HOL_Oinverse__class_Oinverse(tc_Complex_Ocomplex),hAPP(c_HOL_Oinverse__class_Oinverse(tc_Complex_Ocomplex),X0))=X0)),
% 74.46/10.13 inference(resolution,[status(thm)],[f2752,f1074])).
% 74.46/10.13 fof(f3536,plain,(
% 74.46/10.13 ![X0]: (hAPP(c_HOL_Oinverse__class_Oinverse(tc_Complex_Ocomplex),hAPP(c_HOL_Oinverse__class_Oinverse(tc_Complex_Ocomplex),X0))=X0)),
% 74.46/10.13 inference(forward_subsumption_resolution,[status(thm)],[f3535,f2744])).
% 74.46/10.13 fof(f3644,plain,(
% 74.46/10.13 ![X0]: (~c_HOL_Ozero__class_Ozero(tc_nat)=hAPP(hAPP(c_HOL_Otimes__class_Otimes(tc_nat),v_n),X0)|c_HOL_Ozero__class_Ozero(tc_nat)=X0)),
% 74.46/10.13 inference(paramodulation,[status(thm)],[f1384,f3191])).
% 74.46/10.13 fof(f3653,plain,(
% 74.46/10.13 ![X0]: (~c_HOL_Ozero__class_Ozero(tc_nat)=hAPP(hAPP(c_HOL_Otimes__class_Otimes(tc_nat),X0),v_n)|c_HOL_Ozero__class_Ozero(tc_nat)=X0)),
% 74.46/10.13 inference(paramodulation,[status(thm)],[f1075,f3644])).
% 74.46/10.13 fof(f4524,plain,(
% 74.46/10.13 ![X0]: (hAPP(hAPP(c_HOL_Otimes__class_Otimes(tc_nat),hAPP(c_Suc,c_HOL_Ozero__class_Ozero(tc_nat))),X0)=hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),X0),c_HOL_Ozero__class_Ozero(tc_nat)))),
% 74.46/10.13 inference(paramodulation,[status(thm)],[f1383,f1149])).
% 74.46/10.13 fof(f4579,plain,(
% 74.46/10.13 ![X0]: (hAPP(hAPP(c_HOL_Otimes__class_Otimes(tc_nat),hAPP(c_Suc,c_HOL_Ozero__class_Ozero(tc_nat))),X0)=X0)),
% 74.46/10.13 inference(forward_demodulation,[status(thm)],[f1408,f4524])).
% 74.46/10.13 fof(f4680,plain,(
% 74.46/10.13 ~c_HOL_Ozero__class_Ozero(tc_nat)=v_n|c_HOL_Ozero__class_Ozero(tc_nat)=hAPP(c_Suc,c_HOL_Ozero__class_Ozero(tc_nat))),
% 75.30/10.24 inference(paramodulation,[status(thm)],[f4579,f3653])).
% 75.30/10.24 fof(f4715,plain,(
% 75.30/10.24 ~c_HOL_Ozero__class_Ozero(tc_nat)=v_n),
% 75.30/10.24 inference(forward_subsumption_resolution,[status(thm)],[f4680,f2130])).
% 75.30/10.24 fof(f4922,plain,(
% 75.30/10.24 ![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))),
% 75.30/10.24 inference(paramodulation,[status(thm)],[f3536,f3012])).
% 75.30/10.24 fof(f7541,plain,(
% 75.30/10.24 ![X0,X1]: (hAPP(hAPP(c_HOL_Ominus__class_Ominus(tc_nat),X0),X1)=c_HOL_Ozero__class_Ozero(tc_nat)|hBOOL(hAPP(c_HOL_Oord__class_Oless(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),c_HOL_Ozero__class_Ozero(tc_nat)),X1),tc_nat),X0)))),
% 75.30/10.24 inference(resolution,[status(thm)],[f1382,f1515])).
% 75.30/10.24 fof(f7563,plain,(
% 75.30/10.24 ![X0,X1]: (hAPP(hAPP(c_HOL_Ominus__class_Ominus(tc_nat),X0),X1)=c_HOL_Ozero__class_Ozero(tc_nat)|hBOOL(hAPP(c_HOL_Oord__class_Oless(X1,tc_nat),X0)))),
% 75.30/10.24 inference(forward_demodulation,[status(thm)],[f1410,f7541])).
% 75.30/10.24 fof(f9379,plain,(
% 75.30/10.24 ![X0,X1,X2,X3,X4,X5,X6,X7,X8]: (c_COMBS(c_HOL_Oplus__class_Oplus(tc_nat),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,X7,X8)=c_HOL_Ozero__class_Ozero(tc_nat))),
% 75.30/10.24 inference(resolution,[status(thm)],[f4922,f3065])).
% 75.30/10.24 fof(f9403,plain,(
% 75.30/10.24 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9]: (~hBOOL(hAPP(c_HOL_Oord__class_Oless(hAPP(c_COMBS(c_HOL_Oplus__class_Oplus(tc_nat),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,X7,X8),X9),tc_nat),hAPP(X9,X9))))),
% 75.30/10.24 inference(paramodulation,[status(thm)],[f4922,f3067])).
% 75.30/10.24 fof(f9595,plain,(
% 75.30/10.24 ![X0]: (~hBOOL(hAPP(c_HOL_Oord__class_Oless(hAPP(c_HOL_Ozero__class_Ozero(tc_nat),X0),tc_nat),hAPP(X0,X0))))),
% 75.30/10.24 inference(forward_demodulation,[status(thm)],[f9379,f9403])).
% 75.30/10.24 fof(f9597,plain,(
% 75.30/10.24 ![X0]: (hAPP(hAPP(c_HOL_Ominus__class_Ominus(tc_nat),hAPP(X0,X0)),hAPP(c_HOL_Ozero__class_Ozero(tc_nat),X0))=c_HOL_Ozero__class_Ozero(tc_nat))),
% 75.30/10.24 inference(resolution,[status(thm)],[f9595,f7563])).
% 75.30/10.24 fof(f14546,plain,(
% 75.30/10.24 ![X0,X1,X2]: (c_HOL_Ozero__class_Ozero(tc_nat)=c_COMBS(c_HOL_Oplus__class_Oplus(tc_nat),c_HOL_Ozero__class_Ozero(tc_nat),X0,X1,X2))),
% 75.30/10.24 inference(paramodulation,[status(thm)],[f9597,f3063])).
% 75.30/10.24 fof(f14806,plain,(
% 75.30/10.24 ![X0]: (hAPP(hAPP(c_HOL_Ominus__class_Ominus(tc_nat),hAPP(c_HOL_Ozero__class_Ozero(tc_nat),X0)),hAPP(c_HOL_Ozero__class_Ozero(tc_nat),X0))=X0)),
% 75.30/10.24 inference(paramodulation,[status(thm)],[f14546,f3063])).
% 75.30/10.24 fof(f14819,plain,(
% 75.30/10.24 ![X0]: (c_HOL_Ozero__class_Ozero(tc_nat)=X0)),
% 75.30/10.24 inference(forward_demodulation,[status(thm)],[f2523,f14806])).
% 75.30/10.24 fof(f14820,plain,(
% 75.30/10.24 $false),
% 75.30/10.24 inference(backward_subsumption_resolution,[status(thm)],[f4715,f14819])).
% 75.30/10.24 % SZS output end CNFRefutation for theBenchmark.p
% 32.08/10.29 % Elapsed time: 9.809844 seconds
% 32.08/10.29 % CPU time: 76.002806 seconds
% 32.08/10.29 % Total memory used: 577.601 MB
% 32.08/10.29 % Net memory used: 562.515 MB
%------------------------------------------------------------------------------