%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : ALG409-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 : n020.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:09 AM UTC 2026
% Result : Unsatisfiable 145.19s 18.81s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG409-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.35 % Computer : n020.cluster.edu
% 0.10/0.35 % Model : x86_64 x86_64
% 0.10/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.35 % Memory : 8046.5625MB
% 0.10/0.35 % OS : Linux 6.8.0-71-generic
% 0.10/0.35 % CPULimit : 300
% 0.10/0.35 % WCLimit : 300
% 0.10/0.35 % DateTime : Mon Sep 21 13:20:32 UTC 2026
% 0.10/0.35 % CPUTime :
% 0.13/0.40 % Drodi V4.1.1
% 145.19/18.81 % Refutation found
% 145.19/18.81 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 145.19/18.81 % SZS output start CNFRefutation for theBenchmark
% 145.19/18.81 fof(f49,axiom,(
% 145.19/18.81 (![V_z]: (c_HOL_Otimes__class_Otimes(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),V_z,tc_RealDef_Oreal) = V_z ))),
% 145.19/18.81 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 145.19/18.81 fof(f51,axiom,(
% 145.19/18.81 (![V_n]: (c_Suc(V_n) = c_HOL_Oplus__class_Oplus(V_n,c_HOL_Oone__class_Oone(tc_nat),tc_nat) ))),
% 145.19/18.81 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 145.19/18.81 fof(f60,axiom,(
% 145.19/18.81 (![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) ))),
% 145.19/18.81 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 145.19/18.81 fof(f178,axiom,(
% 145.19/18.81 (![V_z1,V_z2,V_z3]: (c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(V_z1,V_z2,tc_RealDef_Oreal),V_z3,tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(V_z1,c_HOL_Otimes__class_Otimes(V_z2,V_z3,tc_RealDef_Oreal),tc_RealDef_Oreal) ))),
% 145.19/18.81 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 145.19/18.81 fof(f256,axiom,(
% 145.19/18.81 (![T_a,V_z,V_x,V_y]: (( ~ class_Orderings_Oorder(T_a)| c_HOL_Oord__class_Oless(V_z,V_x,T_a)| ~ c_lessequals(V_z,V_y,T_a)| ~ c_HOL_Oord__class_Oless(V_y,V_x,T_a) ) ))),
% 145.19/18.81 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 145.19/18.81 fof(f599,axiom,(
% 145.19/18.81 c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(v_t____,v_k____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_t____,c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(c_RealVector_Onorm__class_Onorm(v_w____,tc_Complex_Ocomplex),c_HOL_Oplus__class_Oplus(v_k____,c_HOL_Oone__class_Oone(tc_nat),tc_nat),tc_RealDef_Oreal),v_m____,tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(v_t____,v_k____,tc_RealDef_Oreal),c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal) ),
% 145.19/18.81 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 145.19/18.81 fof(f698,axiom,(
% 145.19/18.81 c_lessequals(c_RealVector_Onorm__class_Onorm(c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(c_HOL_Otimes__class_Otimes(c_RealVector_Oof__real(v_t____,tc_Complex_Ocomplex),v_w____,tc_Complex_Ocomplex),v_k____,tc_Complex_Ocomplex),c_HOL_Otimes__class_Otimes(c_RealVector_Oof__real(v_t____,tc_Complex_Ocomplex),v_w____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_Polynomial_Opoly(v_s____,c_HOL_Otimes__class_Otimes(c_RealVector_Oof__real(v_t____,tc_Complex_Ocomplex),v_w____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(v_t____,v_k____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_t____,c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(c_RealVector_Onorm__class_Onorm(v_w____,tc_Complex_Ocomplex),c_HOL_Oplus__class_Oplus(v_k____,c_HOL_Oone__class_Oone(tc_nat),tc_nat),tc_RealDef_Oreal),v_m____,tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal) ),
% 145.19/18.81 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 145.19/18.81 fof(f700,negated_conjecture,(
% 145.19/18.81 ~ c_HOL_Oord__class_Oless(c_RealVector_Onorm__class_Onorm(c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(c_HOL_Otimes__class_Otimes(c_RealVector_Oof__real(v_t____,tc_Complex_Ocomplex),v_w____,tc_Complex_Ocomplex),v_k____,tc_Complex_Ocomplex),c_HOL_Otimes__class_Otimes(c_RealVector_Oof__real(v_t____,tc_Complex_Ocomplex),v_w____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_Polynomial_Opoly(v_s____,c_HOL_Otimes__class_Otimes(c_RealVector_Oof__real(v_t____,tc_Complex_Ocomplex),v_w____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_Power_Opower__class_Opower(v_t____,v_k____,tc_RealDef_Oreal),tc_RealDef_Oreal) ),
% 145.19/18.81 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 145.19/18.81 fof(f802,axiom,(
% 145.19/18.81 class_Orderings_Oorder(tc_RealDef_Oreal) ),
% 145.19/18.81 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 145.19/18.81 fof(f964,plain,(
% 145.19/18.81 ![X0]: (c_HOL_Otimes__class_Otimes(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),X0,tc_RealDef_Oreal)=X0)),
% 145.19/18.81 inference(cnf_transformation,[status(thm)],[f49])).
% 145.19/18.81 fof(f966,plain,(
% 145.19/18.81 ![X0]: (c_Suc(X0)=c_HOL_Oplus__class_Oplus(X0,c_HOL_Oone__class_Oone(tc_nat),tc_nat))),
% 145.19/18.81 inference(cnf_transformation,[status(thm)],[f51])).
% 145.19/18.81 fof(f979,plain,(
% 145.19/18.81 ![X0,X1]: (c_HOL_Otimes__class_Otimes(X0,X1,tc_RealDef_Oreal)=c_HOL_Otimes__class_Otimes(X1,X0,tc_RealDef_Oreal))),
% 145.19/18.81 inference(cnf_transformation,[status(thm)],[f60])).
% 145.19/18.81 fof(f1181,plain,(
% 145.19/18.81 ![X0,X1,X2]: (c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(X0,X1,tc_RealDef_Oreal),X2,tc_RealDef_Oreal)=c_HOL_Otimes__class_Otimes(X0,c_HOL_Otimes__class_Otimes(X1,X2,tc_RealDef_Oreal),tc_RealDef_Oreal))),
% 145.19/18.81 inference(cnf_transformation,[status(thm)],[f178])).
% 145.19/18.81 fof(f1304,plain,(
% 145.19/18.81 ![T_a,V_x,V_y]: ((![V_z]: ((~class_Orderings_Oorder(T_a)|c_HOL_Oord__class_Oless(V_z,V_x,T_a))|~c_lessequals(V_z,V_y,T_a)))|~c_HOL_Oord__class_Oless(V_y,V_x,T_a))),
% 145.19/18.81 inference(miniscoping,[status(thm)],[f256])).
% 145.19/18.81 fof(f1305,plain,(
% 145.19/18.81 ![X0,X1,X2,X3]: (~class_Orderings_Oorder(X0)|c_HOL_Oord__class_Oless(X1,X2,X0)|~c_lessequals(X1,X3,X0)|~c_HOL_Oord__class_Oless(X3,X2,X0))),
% 145.19/18.81 inference(cnf_transformation,[status(thm)],[f1304])).
% 145.19/18.81 fof(f1848,plain,(
% 145.19/18.81 c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(v_t____,v_k____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_t____,c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(c_RealVector_Onorm__class_Onorm(v_w____,tc_Complex_Ocomplex),c_HOL_Oplus__class_Oplus(v_k____,c_HOL_Oone__class_Oone(tc_nat),tc_nat),tc_RealDef_Oreal),v_m____,tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(v_t____,v_k____,tc_RealDef_Oreal),c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal)),
% 145.19/18.81 inference(cnf_transformation,[status(thm)],[f599])).
% 145.19/18.81 fof(f2023,plain,(
% 145.19/18.81 c_lessequals(c_RealVector_Onorm__class_Onorm(c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(c_HOL_Otimes__class_Otimes(c_RealVector_Oof__real(v_t____,tc_Complex_Ocomplex),v_w____,tc_Complex_Ocomplex),v_k____,tc_Complex_Ocomplex),c_HOL_Otimes__class_Otimes(c_RealVector_Oof__real(v_t____,tc_Complex_Ocomplex),v_w____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_Polynomial_Opoly(v_s____,c_HOL_Otimes__class_Otimes(c_RealVector_Oof__real(v_t____,tc_Complex_Ocomplex),v_w____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(v_t____,v_k____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_t____,c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(c_RealVector_Onorm__class_Onorm(v_w____,tc_Complex_Ocomplex),c_HOL_Oplus__class_Oplus(v_k____,c_HOL_Oone__class_Oone(tc_nat),tc_nat),tc_RealDef_Oreal),v_m____,tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal)),
% 145.19/18.81 inference(cnf_transformation,[status(thm)],[f698])).
% 145.19/18.81 fof(f2025,plain,(
% 145.19/18.81 ~c_HOL_Oord__class_Oless(c_RealVector_Onorm__class_Onorm(c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(c_HOL_Otimes__class_Otimes(c_RealVector_Oof__real(v_t____,tc_Complex_Ocomplex),v_w____,tc_Complex_Ocomplex),v_k____,tc_Complex_Ocomplex),c_HOL_Otimes__class_Otimes(c_RealVector_Oof__real(v_t____,tc_Complex_Ocomplex),v_w____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_Polynomial_Opoly(v_s____,c_HOL_Otimes__class_Otimes(c_RealVector_Oof__real(v_t____,tc_Complex_Ocomplex),v_w____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_Power_Opower__class_Opower(v_t____,v_k____,tc_RealDef_Oreal),tc_RealDef_Oreal)),
% 145.19/18.81 inference(cnf_transformation,[status(thm)],[f700])).
% 145.19/18.81 fof(f2127,plain,(
% 145.19/18.81 class_Orderings_Oorder(tc_RealDef_Oreal)),
% 145.19/18.81 inference(cnf_transformation,[status(thm)],[f802])).
% 145.19/18.81 fof(f2239,plain,(
% 145.19/18.81 ![X0,X1,X2]: (c_HOL_Otimes__class_Otimes(X0,c_HOL_Otimes__class_Otimes(X1,X2,tc_RealDef_Oreal),tc_RealDef_Oreal)=c_HOL_Otimes__class_Otimes(X1,c_HOL_Otimes__class_Otimes(X2,X0,tc_RealDef_Oreal),tc_RealDef_Oreal))),
% 145.19/18.81 inference(paramodulation,[status(thm)],[f979,f1181])).
% 145.19/18.81 fof(f2242,plain,(
% 145.19/18.81 ![X0,X1,X2]: (c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(X0,X1,tc_RealDef_Oreal),X2,tc_RealDef_Oreal)=c_HOL_Otimes__class_Otimes(X1,c_HOL_Otimes__class_Otimes(X0,X2,tc_RealDef_Oreal),tc_RealDef_Oreal))),
% 145.19/18.81 inference(paramodulation,[status(thm)],[f979,f1181])).
% 145.19/18.81 fof(f2400,plain,(
% 145.19/18.81 c_lessequals(c_RealVector_Onorm__class_Onorm(c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(c_HOL_Otimes__class_Otimes(c_RealVector_Oof__real(v_t____,tc_Complex_Ocomplex),v_w____,tc_Complex_Ocomplex),v_k____,tc_Complex_Ocomplex),c_HOL_Otimes__class_Otimes(c_RealVector_Oof__real(v_t____,tc_Complex_Ocomplex),v_w____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_Polynomial_Opoly(v_s____,c_HOL_Otimes__class_Otimes(c_RealVector_Oof__real(v_t____,tc_Complex_Ocomplex),v_w____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(v_t____,v_k____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_t____,c_HOL_Otimes__class_Otimes(v_m____,c_Power_Opower__class_Opower(c_RealVector_Onorm__class_Onorm(v_w____,tc_Complex_Ocomplex),c_HOL_Oplus__class_Oplus(v_k____,c_HOL_Oone__class_Oone(tc_nat),tc_nat),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal)),
% 145.19/18.81 inference(forward_demodulation,[status(thm)],[f979,f2023])).
% 145.19/18.81 fof(f2550,plain,(
% 145.19/18.81 c_lessequals(c_RealVector_Onorm__class_Onorm(c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(c_HOL_Otimes__class_Otimes(c_RealVector_Oof__real(v_t____,tc_Complex_Ocomplex),v_w____,tc_Complex_Ocomplex),v_k____,tc_Complex_Ocomplex),c_HOL_Otimes__class_Otimes(c_RealVector_Oof__real(v_t____,tc_Complex_Ocomplex),v_w____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_Polynomial_Opoly(v_s____,c_HOL_Otimes__class_Otimes(c_RealVector_Oof__real(v_t____,tc_Complex_Ocomplex),v_w____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(v_t____,v_k____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_m____,c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(c_RealVector_Onorm__class_Onorm(v_w____,tc_Complex_Ocomplex),c_HOL_Oplus__class_Oplus(v_k____,c_HOL_Oone__class_Oone(tc_nat),tc_nat),tc_RealDef_Oreal),v_t____,tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal)),
% 145.19/18.81 inference(backward_demodulation,[status(thm)],[f2239,f2400])).
% 145.19/18.81 fof(f2635,plain,(
% 145.19/18.81 c_lessequals(c_RealVector_Onorm__class_Onorm(c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(c_HOL_Otimes__class_Otimes(c_RealVector_Oof__real(v_t____,tc_Complex_Ocomplex),v_w____,tc_Complex_Ocomplex),v_k____,tc_Complex_Ocomplex),c_HOL_Otimes__class_Otimes(c_RealVector_Oof__real(v_t____,tc_Complex_Ocomplex),v_w____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_Polynomial_Opoly(v_s____,c_HOL_Otimes__class_Otimes(c_RealVector_Oof__real(v_t____,tc_Complex_Ocomplex),v_w____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_HOL_Otimes__class_Otimes(v_m____,c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(c_RealVector_Onorm__class_Onorm(v_w____,tc_Complex_Ocomplex),c_HOL_Oplus__class_Oplus(v_k____,c_HOL_Oone__class_Oone(tc_nat),tc_nat),tc_RealDef_Oreal),v_t____,tc_RealDef_Oreal),c_Power_Opower__class_Opower(v_t____,v_k____,tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal)),
% 145.19/18.81 inference(forward_demodulation,[status(thm)],[f2239,f2550])).
% 145.19/18.81 fof(f2636,plain,(
% 145.19/18.81 c_lessequals(c_RealVector_Onorm__class_Onorm(c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(c_HOL_Otimes__class_Otimes(c_RealVector_Oof__real(v_t____,tc_Complex_Ocomplex),v_w____,tc_Complex_Ocomplex),v_k____,tc_Complex_Ocomplex),c_HOL_Otimes__class_Otimes(c_RealVector_Oof__real(v_t____,tc_Complex_Ocomplex),v_w____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_Polynomial_Opoly(v_s____,c_HOL_Otimes__class_Otimes(c_RealVector_Oof__real(v_t____,tc_Complex_Ocomplex),v_w____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_HOL_Otimes__class_Otimes(v_m____,c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(c_RealVector_Onorm__class_Onorm(v_w____,tc_Complex_Ocomplex),c_HOL_Oplus__class_Oplus(v_k____,c_HOL_Oone__class_Oone(tc_nat),tc_nat),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_t____,c_Power_Opower__class_Opower(v_t____,v_k____,tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal)),
% 145.19/18.81 inference(forward_demodulation,[status(thm)],[f1181,f2635])).
% 145.19/18.81 fof(f2637,plain,(
% 145.19/18.81 c_lessequals(c_RealVector_Onorm__class_Onorm(c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(c_HOL_Otimes__class_Otimes(c_RealVector_Oof__real(v_t____,tc_Complex_Ocomplex),v_w____,tc_Complex_Ocomplex),v_k____,tc_Complex_Ocomplex),c_HOL_Otimes__class_Otimes(c_RealVector_Oof__real(v_t____,tc_Complex_Ocomplex),v_w____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_Polynomial_Opoly(v_s____,c_HOL_Otimes__class_Otimes(c_RealVector_Oof__real(v_t____,tc_Complex_Ocomplex),v_w____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_HOL_Otimes__class_Otimes(v_m____,c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(v_t____,v_k____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(c_RealVector_Onorm__class_Onorm(v_w____,tc_Complex_Ocomplex),c_HOL_Oplus__class_Oplus(v_k____,c_HOL_Oone__class_Oone(tc_nat),tc_nat),tc_RealDef_Oreal),v_t____,tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal)),
% 145.19/18.81 inference(forward_demodulation,[status(thm)],[f2239,f2636])).
% 145.19/18.81 fof(f2638,plain,(
% 145.19/18.81 c_lessequals(c_RealVector_Onorm__class_Onorm(c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(c_HOL_Otimes__class_Otimes(c_RealVector_Oof__real(v_t____,tc_Complex_Ocomplex),v_w____,tc_Complex_Ocomplex),v_k____,tc_Complex_Ocomplex),c_HOL_Otimes__class_Otimes(c_RealVector_Oof__real(v_t____,tc_Complex_Ocomplex),v_w____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_Polynomial_Opoly(v_s____,c_HOL_Otimes__class_Otimes(c_RealVector_Oof__real(v_t____,tc_Complex_Ocomplex),v_w____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_HOL_Otimes__class_Otimes(v_m____,c_HOL_Otimes__class_Otimes(v_t____,c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(v_t____,v_k____,tc_RealDef_Oreal),c_Power_Opower__class_Opower(c_RealVector_Onorm__class_Onorm(v_w____,tc_Complex_Ocomplex),c_HOL_Oplus__class_Oplus(v_k____,c_HOL_Oone__class_Oone(tc_nat),tc_nat),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal)),
% 145.19/18.81 inference(forward_demodulation,[status(thm)],[f2239,f2637])).
% 145.19/18.81 fof(f2881,plain,(
% 145.19/18.81 ![X0]: (c_HOL_Otimes__class_Otimes(X0,c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal)=X0)),
% 145.19/18.81 inference(paramodulation,[status(thm)],[f979,f964])).
% 145.19/18.81 fof(f3049,plain,(
% 145.19/18.81 c_lessequals(c_RealVector_Onorm__class_Onorm(c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(c_HOL_Otimes__class_Otimes(c_RealVector_Oof__real(v_t____,tc_Complex_Ocomplex),v_w____,tc_Complex_Ocomplex),v_k____,tc_Complex_Ocomplex),c_HOL_Otimes__class_Otimes(c_RealVector_Oof__real(v_t____,tc_Complex_Ocomplex),v_w____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_Polynomial_Opoly(v_s____,c_HOL_Otimes__class_Otimes(c_RealVector_Oof__real(v_t____,tc_Complex_Ocomplex),v_w____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_HOL_Otimes__class_Otimes(v_m____,c_HOL_Otimes__class_Otimes(v_t____,c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(v_t____,v_k____,tc_RealDef_Oreal),c_Power_Opower__class_Opower(c_RealVector_Onorm__class_Onorm(v_w____,tc_Complex_Ocomplex),c_Suc(v_k____),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal)),
% 145.19/18.81 inference(backward_demodulation,[status(thm)],[f966,f2638])).
% 145.19/18.81 fof(f15020,plain,(
% 145.19/18.81 ![X0]: (~class_Orderings_Oorder(tc_RealDef_Oreal)|c_HOL_Oord__class_Oless(c_RealVector_Onorm__class_Onorm(c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(c_HOL_Otimes__class_Otimes(c_RealVector_Oof__real(v_t____,tc_Complex_Ocomplex),v_w____,tc_Complex_Ocomplex),v_k____,tc_Complex_Ocomplex),c_HOL_Otimes__class_Otimes(c_RealVector_Oof__real(v_t____,tc_Complex_Ocomplex),v_w____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_Polynomial_Opoly(v_s____,c_HOL_Otimes__class_Otimes(c_RealVector_Oof__real(v_t____,tc_Complex_Ocomplex),v_w____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),X0,tc_RealDef_Oreal)|~c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(v_m____,c_HOL_Otimes__class_Otimes(v_t____,c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(v_t____,v_k____,tc_RealDef_Oreal),c_Power_Opower__class_Opower(c_RealVector_Onorm__class_Onorm(v_w____,tc_Complex_Ocomplex),c_Suc(v_k____),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),X0,tc_RealDef_Oreal))),
% 145.19/18.81 inference(resolution,[status(thm)],[f1305,f3049])).
% 145.19/18.81 fof(f15102,plain,(
% 145.19/18.81 ![X0]: (c_HOL_Oord__class_Oless(c_RealVector_Onorm__class_Onorm(c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(c_HOL_Otimes__class_Otimes(c_RealVector_Oof__real(v_t____,tc_Complex_Ocomplex),v_w____,tc_Complex_Ocomplex),v_k____,tc_Complex_Ocomplex),c_HOL_Otimes__class_Otimes(c_RealVector_Oof__real(v_t____,tc_Complex_Ocomplex),v_w____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_Polynomial_Opoly(v_s____,c_HOL_Otimes__class_Otimes(c_RealVector_Oof__real(v_t____,tc_Complex_Ocomplex),v_w____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),X0,tc_RealDef_Oreal)|~c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(v_m____,c_HOL_Otimes__class_Otimes(v_t____,c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(v_t____,v_k____,tc_RealDef_Oreal),c_Power_Opower__class_Opower(c_RealVector_Onorm__class_Onorm(v_w____,tc_Complex_Ocomplex),c_Suc(v_k____),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),X0,tc_RealDef_Oreal))),
% 145.19/18.81 inference(forward_subsumption_resolution,[status(thm)],[f15020,f2127])).
% 145.19/18.81 fof(f69725,plain,(
% 145.19/18.81 c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(v_t____,c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(c_RealVector_Onorm__class_Onorm(v_w____,tc_Complex_Ocomplex),c_HOL_Oplus__class_Oplus(v_k____,c_HOL_Oone__class_Oone(tc_nat),tc_nat),tc_RealDef_Oreal),v_m____,tc_RealDef_Oreal),c_Power_Opower__class_Opower(v_t____,v_k____,tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(v_t____,v_k____,tc_RealDef_Oreal),c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal)),
% 145.19/18.81 inference(forward_demodulation,[status(thm)],[f2239,f1848])).
% 145.19/18.81 fof(f69726,plain,(
% 145.19/18.81 c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(v_t____,c_HOL_Otimes__class_Otimes(v_m____,c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(c_RealVector_Onorm__class_Onorm(v_w____,tc_Complex_Ocomplex),c_HOL_Oplus__class_Oplus(v_k____,c_HOL_Oone__class_Oone(tc_nat),tc_nat),tc_RealDef_Oreal),c_Power_Opower__class_Opower(v_t____,v_k____,tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(v_t____,v_k____,tc_RealDef_Oreal),c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal)),
% 145.19/18.81 inference(forward_demodulation,[status(thm)],[f2242,f69725])).
% 145.19/18.81 fof(f69727,plain,(
% 145.19/18.81 c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(v_m____,c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(c_RealVector_Onorm__class_Onorm(v_w____,tc_Complex_Ocomplex),c_HOL_Oplus__class_Oplus(v_k____,c_HOL_Oone__class_Oone(tc_nat),tc_nat),tc_RealDef_Oreal),c_Power_Opower__class_Opower(v_t____,v_k____,tc_RealDef_Oreal),tc_RealDef_Oreal),v_t____,tc_RealDef_Oreal),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(v_t____,v_k____,tc_RealDef_Oreal),c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal)),
% 145.19/18.81 inference(forward_demodulation,[status(thm)],[f2239,f69726])).
% 145.19/18.81 fof(f69728,plain,(
% 145.19/18.81 c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(v_m____,c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(v_t____,v_k____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(c_RealVector_Onorm__class_Onorm(v_w____,tc_Complex_Ocomplex),c_HOL_Oplus__class_Oplus(v_k____,c_HOL_Oone__class_Oone(tc_nat),tc_nat),tc_RealDef_Oreal),v_t____,tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(v_t____,v_k____,tc_RealDef_Oreal),c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal)),
% 145.19/18.87 inference(forward_demodulation,[status(thm)],[f2242,f69727])).
% 145.19/18.87 fof(f69729,plain,(
% 145.19/18.87 c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(v_m____,c_HOL_Otimes__class_Otimes(v_t____,c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(v_t____,v_k____,tc_RealDef_Oreal),c_Power_Opower__class_Opower(c_RealVector_Onorm__class_Onorm(v_w____,tc_Complex_Ocomplex),c_HOL_Oplus__class_Oplus(v_k____,c_HOL_Oone__class_Oone(tc_nat),tc_nat),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(v_t____,v_k____,tc_RealDef_Oreal),c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal)),
% 145.19/18.87 inference(forward_demodulation,[status(thm)],[f2239,f69728])).
% 145.19/18.87 fof(f69730,plain,(
% 145.19/18.87 c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(v_m____,c_HOL_Otimes__class_Otimes(v_t____,c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(v_t____,v_k____,tc_RealDef_Oreal),c_Power_Opower__class_Opower(c_RealVector_Onorm__class_Onorm(v_w____,tc_Complex_Ocomplex),c_Suc(v_k____),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(v_t____,v_k____,tc_RealDef_Oreal),c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal)),
% 145.19/18.87 inference(forward_demodulation,[status(thm)],[f966,f69729])).
% 145.19/18.87 fof(f69731,plain,(
% 145.19/18.87 c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(v_m____,c_HOL_Otimes__class_Otimes(v_t____,c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(v_t____,v_k____,tc_RealDef_Oreal),c_Power_Opower__class_Opower(c_RealVector_Onorm__class_Onorm(v_w____,tc_Complex_Ocomplex),c_Suc(v_k____),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),c_Power_Opower__class_Opower(v_t____,v_k____,tc_RealDef_Oreal),tc_RealDef_Oreal)),
% 145.19/18.87 inference(forward_demodulation,[status(thm)],[f2881,f69730])).
% 145.19/18.87 fof(f69732,plain,(
% 145.19/18.87 c_HOL_Oord__class_Oless(c_RealVector_Onorm__class_Onorm(c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(c_HOL_Otimes__class_Otimes(c_RealVector_Oof__real(v_t____,tc_Complex_Ocomplex),v_w____,tc_Complex_Ocomplex),v_k____,tc_Complex_Ocomplex),c_HOL_Otimes__class_Otimes(c_RealVector_Oof__real(v_t____,tc_Complex_Ocomplex),v_w____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_Polynomial_Opoly(v_s____,c_HOL_Otimes__class_Otimes(c_RealVector_Oof__real(v_t____,tc_Complex_Ocomplex),v_w____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_Power_Opower__class_Opower(v_t____,v_k____,tc_RealDef_Oreal),tc_RealDef_Oreal)),
% 145.19/18.87 inference(resolution,[status(thm)],[f69731,f15102])).
% 145.19/18.87 fof(f69812,plain,(
% 145.19/18.87 $false),
% 145.19/18.87 inference(forward_subsumption_resolution,[status(thm)],[f69732,f2025])).
% 145.19/18.87 % SZS output end CNFRefutation for theBenchmark.p
% 19.44/18.92 % Elapsed time: 18.559945 seconds
% 19.44/18.92 % CPU time: 145.888906 seconds
% 19.44/18.92 % Total memory used: 886.099 MB
% 19.44/18.92 % Net memory used: 867.744 MB
%------------------------------------------------------------------------------