%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : ALG380-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 11:50:06 AM UTC 2026
% Result : Unsatisfiable 16.89s 2.70s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG380-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.10/0.36 % Computer : n014.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.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Mon Sep 21 13:18:06 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.22/0.46 % Drodi V4.1.1
% 16.89/2.70 % Refutation found
% 16.89/2.70 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 16.89/2.70 % SZS output start CNFRefutation for theBenchmark
% 16.89/2.70 fof(f36,axiom,(
% 16.89/2.70 (![V_z,V_w]: (c_HOL_Otimes__class_Otimes(V_z,V_w,tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(V_w,V_z,tc_RealDef_Oreal) ))),
% 16.89/2.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 16.89/2.70 fof(f130,axiom,(
% 16.89/2.70 (![V_x]: (( c_NthRoot_Osqrt(V_x) != c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),V_x,tc_RealDef_Oreal) ) ))),
% 16.89/2.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 16.89/2.70 fof(f133,axiom,(
% 16.89/2.70 c_Transcendental_Osin(c_Transcendental_Opi) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) ),
% 16.89/2.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 16.89/2.70 fof(f215,axiom,(
% 16.89/2.70 (![T_a,V_a]: (( ~ class_OrderedGroup_Omonoid__add(T_a)| c_HOL_Oplus__class_Oplus(V_a,c_HOL_Ozero__class_Ozero(T_a),T_a) = V_a ) ))),
% 16.89/2.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 16.89/2.70 fof(f583,axiom,(
% 16.89/2.70 (![V_y,V_x]: (c_lessequals(V_y,c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_Power_Opower__class_Opower(V_x,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_nat),tc_RealDef_Oreal),c_Power_Opower__class_Opower(V_y,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_nat),tc_RealDef_Oreal),tc_RealDef_Oreal)),tc_RealDef_Oreal) ))),
% 16.89/2.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 16.89/2.70 fof(f590,axiom,(
% 16.89/2.70 (![V_y]: (( c_NthRoot_Osqrt(c_Power_Opower__class_Opower(V_y,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_nat),tc_RealDef_Oreal)) = V_y| ~ c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),V_y,tc_RealDef_Oreal) ) ))),
% 16.89/2.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 16.89/2.70 fof(f609,axiom,(
% 16.89/2.70 (![V_x,V_k]: (c_NthRoot_Osqrt(c_Power_Opower__class_Opower(V_x,V_k,tc_RealDef_Oreal)) = c_Power_Opower__class_Opower(c_NthRoot_Osqrt(V_x),V_k,tc_RealDef_Oreal) ))),
% 16.89/2.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 16.89/2.70 fof(f613,axiom,(
% 16.89/2.70 c_NthRoot_Osqrt(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) ),
% 16.89/2.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 16.89/2.70 fof(f615,axiom,(
% 16.89/2.70 (![V_x,V_y]: (c_NthRoot_Osqrt(c_HOL_Otimes__class_Otimes(V_x,V_y,tc_RealDef_Oreal)) = c_HOL_Otimes__class_Otimes(c_NthRoot_Osqrt(V_x),c_NthRoot_Osqrt(V_y),tc_RealDef_Oreal) ))),
% 16.89/2.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 16.89/2.70 fof(f620,axiom,(
% 16.89/2.70 (![V_r1,V_a,V_r2,V_b]: (c_HOL_Otimes__class_Otimes(c_Complex_Orcis(V_r1,V_a),c_Complex_Orcis(V_r2,V_b),tc_Complex_Ocomplex) = c_Complex_Orcis(c_HOL_Otimes__class_Otimes(V_r1,V_r2,tc_RealDef_Oreal),c_HOL_Oplus__class_Oplus(V_a,V_b,tc_RealDef_Oreal)) ))),
% 16.89/2.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 16.89/2.70 fof(f864,axiom,(
% 16.89/2.70 c_Transcendental_Otan(c_Transcendental_Opi) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) ),
% 16.89/2.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 16.89/2.70 fof(f867,axiom,(
% 16.89/2.70 (![V_r]: (( c_HOL_Oabs__class_Oabs(V_r,tc_RealDef_Oreal) = V_r| c_HOL_Oord__class_Oless(V_r,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal) ) ))),
% 16.89/2.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 16.89/2.70 fof(f946,axiom,(
% 16.89/2.70 (![V_x]: (c_NthRoot_Osqrt(c_HOL_Otimes__class_Otimes(V_x,V_x,tc_RealDef_Oreal)) = c_HOL_Oabs__class_Oabs(V_x,tc_RealDef_Oreal) ))),
% 16.89/2.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 16.89/2.70 fof(f965,axiom,(
% 16.89/2.70 (![V_x]: (c_NthRoot_Osqrt(c_Power_Opower__class_Opower(V_x,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_nat),tc_RealDef_Oreal)) = c_HOL_Oabs__class_Oabs(V_x,tc_RealDef_Oreal) ))),
% 16.89/2.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 16.89/2.70 fof(f995,axiom,(
% 16.89/2.70 (![V_x]: (c_HOL_Oplus__class_Oplus(c_HOL_Oinverse__class_Odivide(V_x,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(V_x,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal) = V_x ))),
% 16.89/2.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 16.89/2.70 fof(f1032,negated_conjecture,(
% 16.89/2.70 c_HOL_Otimes__class_Otimes(c_Complex_Orcis(c_NthRoot_Osqrt(c_HOL_Oabs__class_Oabs(v_r,tc_RealDef_Oreal)),c_HOL_Oinverse__class_Odivide(v_a,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal)),c_Complex_Orcis(c_NthRoot_Osqrt(c_HOL_Oabs__class_Oabs(v_r,tc_RealDef_Oreal)),c_HOL_Oinverse__class_Odivide(v_a,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal)),tc_Complex_Ocomplex) != c_Complex_Orcis(c_HOL_Oabs__class_Oabs(v_r,tc_RealDef_Oreal),v_a) ),
% 16.89/2.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 16.89/2.70 fof(f1165,axiom,(
% 16.89/2.70 class_OrderedGroup_Omonoid__add(tc_RealDef_Oreal) ),
% 16.89/2.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 16.89/2.70 fof(f1267,plain,(
% 16.89/2.70 ![X0,X1]: (c_HOL_Otimes__class_Otimes(X0,X1,tc_RealDef_Oreal)=c_HOL_Otimes__class_Otimes(X1,X0,tc_RealDef_Oreal))),
% 16.89/2.70 inference(cnf_transformation,[status(thm)],[f36])).
% 16.89/2.70 fof(f1401,plain,(
% 16.89/2.70 ![X0]: (~c_NthRoot_Osqrt(X0)=c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)|~c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X0,tc_RealDef_Oreal))),
% 16.89/2.70 inference(cnf_transformation,[status(thm)],[f130])).
% 16.89/2.70 fof(f1406,plain,(
% 16.89/2.70 c_Transcendental_Osin(c_Transcendental_Opi)=c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)),
% 16.89/2.70 inference(cnf_transformation,[status(thm)],[f133])).
% 16.89/2.70 fof(f1539,plain,(
% 16.89/2.70 ![T_a]: (~class_OrderedGroup_Omonoid__add(T_a)|(![V_a]: c_HOL_Oplus__class_Oplus(V_a,c_HOL_Ozero__class_Ozero(T_a),T_a)=V_a))),
% 16.89/2.70 inference(miniscoping,[status(thm)],[f215])).
% 16.89/2.70 fof(f1540,plain,(
% 16.89/2.70 ![X0,X1]: (~class_OrderedGroup_Omonoid__add(X0)|c_HOL_Oplus__class_Oplus(X1,c_HOL_Ozero__class_Ozero(X0),X0)=X1)),
% 16.89/2.70 inference(cnf_transformation,[status(thm)],[f1539])).
% 16.89/2.70 fof(f2141,plain,(
% 16.89/2.70 ![X0,X1]: (c_lessequals(X0,c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_Power_Opower__class_Opower(X1,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_nat),tc_RealDef_Oreal),c_Power_Opower__class_Opower(X0,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_nat),tc_RealDef_Oreal),tc_RealDef_Oreal)),tc_RealDef_Oreal))),
% 16.89/2.70 inference(cnf_transformation,[status(thm)],[f583])).
% 16.89/2.70 fof(f2150,plain,(
% 16.89/2.70 ![X0]: (c_NthRoot_Osqrt(c_Power_Opower__class_Opower(X0,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_nat),tc_RealDef_Oreal))=X0|~c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X0,tc_RealDef_Oreal))),
% 16.89/2.70 inference(cnf_transformation,[status(thm)],[f590])).
% 16.89/2.70 fof(f2177,plain,(
% 16.89/2.70 ![X0,X1]: (c_NthRoot_Osqrt(c_Power_Opower__class_Opower(X0,X1,tc_RealDef_Oreal))=c_Power_Opower__class_Opower(c_NthRoot_Osqrt(X0),X1,tc_RealDef_Oreal))),
% 16.89/2.70 inference(cnf_transformation,[status(thm)],[f609])).
% 16.89/2.70 fof(f2181,plain,(
% 16.89/2.70 c_NthRoot_Osqrt(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal))=c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)),
% 16.89/2.70 inference(cnf_transformation,[status(thm)],[f613])).
% 16.89/2.70 fof(f2183,plain,(
% 16.89/2.70 ![X0,X1]: (c_NthRoot_Osqrt(c_HOL_Otimes__class_Otimes(X0,X1,tc_RealDef_Oreal))=c_HOL_Otimes__class_Otimes(c_NthRoot_Osqrt(X0),c_NthRoot_Osqrt(X1),tc_RealDef_Oreal))),
% 16.89/2.70 inference(cnf_transformation,[status(thm)],[f615])).
% 16.89/2.70 fof(f2189,plain,(
% 16.89/2.70 ![X0,X1,X2,X3]: (c_HOL_Otimes__class_Otimes(c_Complex_Orcis(X0,X1),c_Complex_Orcis(X2,X3),tc_Complex_Ocomplex)=c_Complex_Orcis(c_HOL_Otimes__class_Otimes(X0,X2,tc_RealDef_Oreal),c_HOL_Oplus__class_Oplus(X1,X3,tc_RealDef_Oreal)))),
% 16.89/2.70 inference(cnf_transformation,[status(thm)],[f620])).
% 16.89/2.70 fof(f2529,plain,(
% 16.89/2.70 c_Transcendental_Otan(c_Transcendental_Opi)=c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)),
% 16.89/2.70 inference(cnf_transformation,[status(thm)],[f864])).
% 16.89/2.70 fof(f2532,plain,(
% 16.89/2.70 ![X0]: (c_HOL_Oabs__class_Oabs(X0,tc_RealDef_Oreal)=X0|c_HOL_Oord__class_Oless(X0,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal))),
% 16.89/2.70 inference(cnf_transformation,[status(thm)],[f867])).
% 16.89/2.70 fof(f2647,plain,(
% 16.89/2.70 ![X0]: (c_NthRoot_Osqrt(c_HOL_Otimes__class_Otimes(X0,X0,tc_RealDef_Oreal))=c_HOL_Oabs__class_Oabs(X0,tc_RealDef_Oreal))),
% 16.89/2.70 inference(cnf_transformation,[status(thm)],[f946])).
% 16.89/2.70 fof(f2667,plain,(
% 16.89/2.70 ![X0]: (c_NthRoot_Osqrt(c_Power_Opower__class_Opower(X0,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_nat),tc_RealDef_Oreal))=c_HOL_Oabs__class_Oabs(X0,tc_RealDef_Oreal))),
% 16.89/2.70 inference(cnf_transformation,[status(thm)],[f965])).
% 16.89/2.70 fof(f2713,plain,(
% 16.89/2.70 ![X0]: (c_HOL_Oplus__class_Oplus(c_HOL_Oinverse__class_Odivide(X0,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(X0,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal)=X0)),
% 16.89/2.70 inference(cnf_transformation,[status(thm)],[f995])).
% 16.89/2.70 fof(f2774,plain,(
% 16.89/2.70 ~c_HOL_Otimes__class_Otimes(c_Complex_Orcis(c_NthRoot_Osqrt(c_HOL_Oabs__class_Oabs(v_r,tc_RealDef_Oreal)),c_HOL_Oinverse__class_Odivide(v_a,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal)),c_Complex_Orcis(c_NthRoot_Osqrt(c_HOL_Oabs__class_Oabs(v_r,tc_RealDef_Oreal)),c_HOL_Oinverse__class_Odivide(v_a,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal)),tc_Complex_Ocomplex)=c_Complex_Orcis(c_HOL_Oabs__class_Oabs(v_r,tc_RealDef_Oreal),v_a)),
% 16.89/2.70 inference(cnf_transformation,[status(thm)],[f1032])).
% 16.89/2.70 fof(f2907,plain,(
% 16.89/2.70 class_OrderedGroup_Omonoid__add(tc_RealDef_Oreal)),
% 16.89/2.70 inference(cnf_transformation,[status(thm)],[f1165])).
% 16.89/2.70 fof(f2962,plain,(
% 16.89/2.70 ![X0]: (~c_NthRoot_Osqrt(X0)=c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)|~c_HOL_Oord__class_Oless(c_Transcendental_Osin(c_Transcendental_Opi),X0,tc_RealDef_Oreal))),
% 16.89/2.70 inference(backward_demodulation,[status(thm)],[f1406,f1401])).
% 16.89/2.70 fof(f3051,plain,(
% 16.89/2.70 ![X0]: (c_NthRoot_Osqrt(c_Power_Opower__class_Opower(X0,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_nat),tc_RealDef_Oreal))=X0|~c_lessequals(c_Transcendental_Osin(c_Transcendental_Opi),X0,tc_RealDef_Oreal))),
% 16.89/2.70 inference(forward_demodulation,[status(thm)],[f1406,f2150])).
% 16.89/2.70 fof(f3064,plain,(
% 16.89/2.70 c_NthRoot_Osqrt(c_Transcendental_Osin(c_Transcendental_Opi))=c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)),
% 16.89/2.70 inference(forward_demodulation,[status(thm)],[f1406,f2181])).
% 16.89/2.70 fof(f3065,plain,(
% 16.89/2.70 c_NthRoot_Osqrt(c_Transcendental_Osin(c_Transcendental_Opi))=c_Transcendental_Osin(c_Transcendental_Opi)),
% 16.89/2.70 inference(forward_demodulation,[status(thm)],[f1406,f3064])).
% 16.89/2.70 fof(f3113,plain,(
% 16.89/2.70 c_Transcendental_Osin(c_Transcendental_Opi)=c_Transcendental_Otan(c_Transcendental_Opi)),
% 16.89/2.70 inference(backward_demodulation,[status(thm)],[f2529,f1406])).
% 16.89/2.70 fof(f3114,plain,(
% 16.89/2.70 ![X0]: (c_HOL_Oabs__class_Oabs(X0,tc_RealDef_Oreal)=X0|c_HOL_Oord__class_Oless(X0,c_Transcendental_Otan(c_Transcendental_Opi),tc_RealDef_Oreal))),
% 16.89/2.70 inference(forward_demodulation,[status(thm)],[f2529,f2532])).
% 16.89/2.70 fof(f3136,plain,(
% 16.89/2.70 ![X0]: (c_HOL_Oabs__class_Oabs(X0,tc_RealDef_Oreal)=X0|~c_lessequals(c_Transcendental_Osin(c_Transcendental_Opi),X0,tc_RealDef_Oreal))),
% 16.89/2.70 inference(backward_demodulation,[status(thm)],[f2667,f3051])).
% 16.89/2.70 fof(f3140,plain,(
% 16.89/2.70 ![X0]: (~c_NthRoot_Osqrt(X0)=c_Transcendental_Otan(c_Transcendental_Opi)|~c_HOL_Oord__class_Oless(c_Transcendental_Osin(c_Transcendental_Opi),X0,tc_RealDef_Oreal))),
% 16.89/2.70 inference(forward_demodulation,[status(thm)],[f2529,f2962])).
% 16.89/2.70 fof(f3178,plain,(
% 16.89/2.70 ![X0]: (~c_NthRoot_Osqrt(X0)=c_Transcendental_Otan(c_Transcendental_Opi)|~c_HOL_Oord__class_Oless(c_Transcendental_Otan(c_Transcendental_Opi),X0,tc_RealDef_Oreal))),
% 16.89/2.70 inference(backward_demodulation,[status(thm)],[f3113,f3140])).
% 16.89/2.70 fof(f3207,plain,(
% 16.89/2.70 c_NthRoot_Osqrt(c_Transcendental_Osin(c_Transcendental_Opi))=c_Transcendental_Otan(c_Transcendental_Opi)),
% 16.89/2.70 inference(backward_demodulation,[status(thm)],[f3113,f3065])).
% 16.89/2.70 fof(f3252,plain,(
% 16.89/2.70 ![X0]: (c_HOL_Oabs__class_Oabs(X0,tc_RealDef_Oreal)=X0|~c_lessequals(c_Transcendental_Otan(c_Transcendental_Opi),X0,tc_RealDef_Oreal))),
% 16.89/2.70 inference(forward_demodulation,[status(thm)],[f3113,f3136])).
% 16.89/2.70 fof(f3272,plain,(
% 16.89/2.70 c_NthRoot_Osqrt(c_Transcendental_Otan(c_Transcendental_Opi))=c_Transcendental_Otan(c_Transcendental_Opi)),
% 16.89/2.70 inference(forward_demodulation,[status(thm)],[f3113,f3207])).
% 16.89/2.70 fof(f3350,plain,(
% 16.89/2.70 ![X0]: (c_NthRoot_Osqrt(c_Power_Opower__class_Opower(c_Transcendental_Otan(c_Transcendental_Opi),X0,tc_RealDef_Oreal))=c_Power_Opower__class_Opower(c_Transcendental_Otan(c_Transcendental_Opi),X0,tc_RealDef_Oreal))),
% 16.89/2.70 inference(paramodulation,[status(thm)],[f3272,f2177])).
% 16.89/2.70 fof(f3376,plain,(
% 16.89/2.70 ~c_NthRoot_Osqrt(c_Transcendental_Otan(c_Transcendental_Opi))=c_Transcendental_Otan(c_Transcendental_Opi)|c_HOL_Oabs__class_Oabs(c_Transcendental_Otan(c_Transcendental_Opi),tc_RealDef_Oreal)=c_Transcendental_Otan(c_Transcendental_Opi)),
% 16.89/2.70 inference(resolution,[status(thm)],[f3178,f3114])).
% 16.89/2.70 fof(f3377,plain,(
% 16.89/2.70 ~c_Transcendental_Otan(c_Transcendental_Opi)=c_Transcendental_Otan(c_Transcendental_Opi)|c_HOL_Oabs__class_Oabs(c_Transcendental_Otan(c_Transcendental_Opi),tc_RealDef_Oreal)=c_Transcendental_Otan(c_Transcendental_Opi)),
% 16.89/2.70 inference(forward_demodulation,[status(thm)],[f3272,f3376])).
% 16.89/2.70 fof(f3378,plain,(
% 16.89/2.70 c_HOL_Oabs__class_Oabs(c_Transcendental_Otan(c_Transcendental_Opi),tc_RealDef_Oreal)=c_Transcendental_Otan(c_Transcendental_Opi)),
% 16.89/2.70 inference(trivial_equality_resolution,[status(thm)],[f3377])).
% 16.89/2.70 fof(f3402,plain,(
% 16.89/2.70 ![X0,X1]: (c_NthRoot_Osqrt(c_HOL_Otimes__class_Otimes(X0,X1,tc_RealDef_Oreal))=c_HOL_Otimes__class_Otimes(c_NthRoot_Osqrt(X1),c_NthRoot_Osqrt(X0),tc_RealDef_Oreal))),
% 16.89/2.70 inference(paramodulation,[status(thm)],[f1267,f2183])).
% 16.89/2.70 fof(f3411,plain,(
% 16.89/2.70 ![X0]: (c_NthRoot_Osqrt(c_NthRoot_Osqrt(c_HOL_Otimes__class_Otimes(X0,X0,tc_RealDef_Oreal)))=c_HOL_Oabs__class_Oabs(c_NthRoot_Osqrt(X0),tc_RealDef_Oreal))),
% 16.89/2.70 inference(paramodulation,[status(thm)],[f2183,f2647])).
% 16.89/2.70 fof(f3420,plain,(
% 16.89/2.70 ![X0]: (c_NthRoot_Osqrt(c_HOL_Oabs__class_Oabs(X0,tc_RealDef_Oreal))=c_HOL_Oabs__class_Oabs(c_NthRoot_Osqrt(X0),tc_RealDef_Oreal))),
% 16.89/2.70 inference(forward_demodulation,[status(thm)],[f2647,f3411])).
% 16.89/2.70 fof(f3469,plain,(
% 16.89/2.70 ![X0]: (c_HOL_Oabs__class_Oabs(c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_Power_Opower__class_Opower(X0,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_nat),tc_RealDef_Oreal),c_Power_Opower__class_Opower(c_Transcendental_Otan(c_Transcendental_Opi),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_nat),tc_RealDef_Oreal),tc_RealDef_Oreal)),tc_RealDef_Oreal)=c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_Power_Opower__class_Opower(X0,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_nat),tc_RealDef_Oreal),c_Power_Opower__class_Opower(c_Transcendental_Otan(c_Transcendental_Opi),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_nat),tc_RealDef_Oreal),tc_RealDef_Oreal)))),
% 16.89/2.70 inference(resolution,[status(thm)],[f2141,f3252])).
% 16.89/2.70 fof(f3475,plain,(
% 16.89/2.70 ![X0]: (c_NthRoot_Osqrt(c_HOL_Oabs__class_Oabs(c_HOL_Oplus__class_Oplus(c_Power_Opower__class_Opower(X0,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_nat),tc_RealDef_Oreal),c_Power_Opower__class_Opower(c_Transcendental_Otan(c_Transcendental_Opi),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_nat),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal))=c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_Power_Opower__class_Opower(X0,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_nat),tc_RealDef_Oreal),c_Power_Opower__class_Opower(c_Transcendental_Otan(c_Transcendental_Opi),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_nat),tc_RealDef_Oreal),tc_RealDef_Oreal)))),
% 16.89/2.70 inference(forward_demodulation,[status(thm)],[f3420,f3469])).
% 16.89/2.70 fof(f3878,plain,(
% 16.89/2.70 ![X0,X1,X2,X3]: (c_HOL_Otimes__class_Otimes(c_Complex_Orcis(c_NthRoot_Osqrt(X0),X1),c_Complex_Orcis(c_NthRoot_Osqrt(X2),X3),tc_Complex_Ocomplex)=c_Complex_Orcis(c_NthRoot_Osqrt(c_HOL_Otimes__class_Otimes(X2,X0,tc_RealDef_Oreal)),c_HOL_Oplus__class_Oplus(X1,X3,tc_RealDef_Oreal)))),
% 16.89/2.70 inference(paramodulation,[status(thm)],[f3402,f2189])).
% 16.89/2.70 fof(f3886,plain,(
% 16.89/2.70 ~c_Complex_Orcis(c_NthRoot_Osqrt(c_HOL_Otimes__class_Otimes(c_HOL_Oabs__class_Oabs(v_r,tc_RealDef_Oreal),c_HOL_Oabs__class_Oabs(v_r,tc_RealDef_Oreal),tc_RealDef_Oreal)),c_HOL_Oplus__class_Oplus(c_HOL_Oinverse__class_Odivide(v_a,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(v_a,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal))=c_Complex_Orcis(c_HOL_Oabs__class_Oabs(v_r,tc_RealDef_Oreal),v_a)),
% 16.89/2.70 inference(backward_demodulation,[status(thm)],[f3878,f2774])).
% 16.89/2.70 fof(f3889,plain,(
% 16.89/2.70 ~c_Complex_Orcis(c_HOL_Oabs__class_Oabs(c_HOL_Oabs__class_Oabs(v_r,tc_RealDef_Oreal),tc_RealDef_Oreal),c_HOL_Oplus__class_Oplus(c_HOL_Oinverse__class_Odivide(v_a,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(v_a,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal))=c_Complex_Orcis(c_HOL_Oabs__class_Oabs(v_r,tc_RealDef_Oreal),v_a)),
% 16.89/2.70 inference(forward_demodulation,[status(thm)],[f2647,f3886])).
% 16.89/2.70 fof(f3890,plain,(
% 16.89/2.70 ~c_Complex_Orcis(c_HOL_Oabs__class_Oabs(c_HOL_Oabs__class_Oabs(v_r,tc_RealDef_Oreal),tc_RealDef_Oreal),v_a)=c_Complex_Orcis(c_HOL_Oabs__class_Oabs(v_r,tc_RealDef_Oreal),v_a)),
% 16.89/2.70 inference(forward_demodulation,[status(thm)],[f2713,f3889])).
% 16.89/2.70 fof(f4509,plain,(
% 16.89/2.70 c_Power_Opower__class_Opower(c_Transcendental_Otan(c_Transcendental_Opi),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_nat),tc_RealDef_Oreal)=c_HOL_Oabs__class_Oabs(c_Transcendental_Otan(c_Transcendental_Opi),tc_RealDef_Oreal)),
% 16.89/2.70 inference(paramodulation,[status(thm)],[f3350,f2667])).
% 16.89/2.70 fof(f4527,plain,(
% 16.89/2.70 ![X0]: (c_NthRoot_Osqrt(c_HOL_Oabs__class_Oabs(c_Power_Opower__class_Opower(X0,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_nat),tc_RealDef_Oreal),tc_RealDef_Oreal))=c_HOL_Oabs__class_Oabs(c_HOL_Oabs__class_Oabs(X0,tc_RealDef_Oreal),tc_RealDef_Oreal))),
% 16.89/2.70 inference(paramodulation,[status(thm)],[f2667,f3420])).
% 16.89/2.70 fof(f4553,plain,(
% 16.89/2.70 ![X0]: (c_NthRoot_Osqrt(c_HOL_Oabs__class_Oabs(c_HOL_Oplus__class_Oplus(c_Power_Opower__class_Opower(X0,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_nat),tc_RealDef_Oreal),c_Power_Opower__class_Opower(c_Transcendental_Otan(c_Transcendental_Opi),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_nat),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal))=c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_Power_Opower__class_Opower(X0,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_nat),tc_RealDef_Oreal),c_Transcendental_Otan(c_Transcendental_Opi),tc_RealDef_Oreal)))),
% 16.89/2.70 inference(backward_demodulation,[status(thm)],[f4555,f3475])).
% 16.89/2.70 fof(f4555,plain,(
% 16.89/2.70 c_Power_Opower__class_Opower(c_Transcendental_Otan(c_Transcendental_Opi),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_nat),tc_RealDef_Oreal)=c_Transcendental_Otan(c_Transcendental_Opi)),
% 16.89/2.70 inference(forward_demodulation,[status(thm)],[f3378,f4509])).
% 16.89/2.70 fof(f4560,plain,(
% 16.89/2.70 ![X0]: (c_NthRoot_Osqrt(c_HOL_Oabs__class_Oabs(c_HOL_Oplus__class_Oplus(c_Power_Opower__class_Opower(X0,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_nat),tc_RealDef_Oreal),c_Transcendental_Otan(c_Transcendental_Opi),tc_RealDef_Oreal),tc_RealDef_Oreal))=c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_Power_Opower__class_Opower(X0,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_nat),tc_RealDef_Oreal),c_Transcendental_Otan(c_Transcendental_Opi),tc_RealDef_Oreal)))),
% 16.89/2.70 inference(forward_demodulation,[status(thm)],[f4555,f4553])).
% 16.89/2.70 fof(f9274,plain,(
% 16.89/2.70 ![X0]: (c_HOL_Oplus__class_Oplus(X0,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)=X0)),
% 16.89/2.70 inference(resolution,[status(thm)],[f1540,f2907])).
% 16.89/2.70 fof(f9341,plain,(
% 16.89/2.70 ![X0]: (c_NthRoot_Osqrt(c_HOL_Oabs__class_Oabs(c_HOL_Oplus__class_Oplus(c_Power_Opower__class_Opower(X0,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_nat),tc_RealDef_Oreal),c_Transcendental_Otan(c_Transcendental_Opi),tc_RealDef_Oreal),tc_RealDef_Oreal))=c_NthRoot_Osqrt(c_Power_Opower__class_Opower(X0,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_nat),tc_RealDef_Oreal)))),
% 17.20/2.75 inference(backward_demodulation,[status(thm)],[f9361,f4560])).
% 17.20/2.75 fof(f9361,plain,(
% 17.20/2.75 ![X0]: (c_HOL_Oplus__class_Oplus(X0,c_Transcendental_Otan(c_Transcendental_Opi),tc_RealDef_Oreal)=X0)),
% 17.20/2.75 inference(forward_demodulation,[status(thm)],[f2529,f9274])).
% 17.20/2.75 fof(f9431,plain,(
% 17.20/2.75 ![X0]: (c_NthRoot_Osqrt(c_HOL_Oabs__class_Oabs(c_Power_Opower__class_Opower(X0,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_nat),tc_RealDef_Oreal),tc_RealDef_Oreal))=c_NthRoot_Osqrt(c_Power_Opower__class_Opower(X0,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_nat),tc_RealDef_Oreal)))),
% 17.20/2.75 inference(forward_demodulation,[status(thm)],[f9361,f9341])).
% 17.20/2.75 fof(f9432,plain,(
% 17.20/2.75 ![X0]: (c_HOL_Oabs__class_Oabs(c_HOL_Oabs__class_Oabs(X0,tc_RealDef_Oreal),tc_RealDef_Oreal)=c_NthRoot_Osqrt(c_Power_Opower__class_Opower(X0,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_nat),tc_RealDef_Oreal)))),
% 17.20/2.75 inference(forward_demodulation,[status(thm)],[f4527,f9431])).
% 17.20/2.75 fof(f9434,plain,(
% 17.20/2.75 ~c_Complex_Orcis(c_HOL_Oabs__class_Oabs(v_r,tc_RealDef_Oreal),v_a)=c_Complex_Orcis(c_HOL_Oabs__class_Oabs(v_r,tc_RealDef_Oreal),v_a)),
% 17.20/2.75 inference(backward_demodulation,[status(thm)],[f9542,f3890])).
% 17.20/2.75 fof(f9542,plain,(
% 17.20/2.75 ![X0]: (c_HOL_Oabs__class_Oabs(c_HOL_Oabs__class_Oabs(X0,tc_RealDef_Oreal),tc_RealDef_Oreal)=c_HOL_Oabs__class_Oabs(X0,tc_RealDef_Oreal))),
% 17.20/2.75 inference(forward_demodulation,[status(thm)],[f2667,f9432])).
% 17.20/2.75 fof(f9581,plain,(
% 17.20/2.75 $false),
% 17.20/2.75 inference(trivial_equality_resolution,[status(thm)],[f9434])).
% 17.20/2.75 % SZS output end CNFRefutation for theBenchmark.p
% 17.20/2.76 % Elapsed time: 2.374211 seconds
% 17.20/2.76 % CPU time: 17.973380 seconds
% 17.20/2.76 % Total memory used: 420.721 MB
% 17.20/2.76 % Net memory used: 414.061 MB
%------------------------------------------------------------------------------