%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWW263+1 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n011.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 03:08:53 PM UTC 2026
% Result : Theorem 0.44s 1.41s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SWW263+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.19/0.45 % Computer : n011.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:44:26 UTC 2026
% 0.19/0.45 % CPUTime :
% 0.38/0.61 % Drodi V4.1.1
% 0.44/1.41 % Refutation found
% 0.44/1.41 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.44/1.41 % SZS output start CNFRefutation for theBenchmark
% 0.44/1.41 fof(f6,axiom,(
% 0.44/1.41 c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),hAPP(hAPP(c_Power_Opower__class_Opower(tc_RealDef_Oreal),v_t____),v_k____)) ),
% 0.44/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.44/1.41 fof(f7,axiom,(
% 0.44/1.41 c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),v_t____),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),hAPP(hAPP(c_Power_Opower__class_Opower(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_w____)),c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_k____,c_Groups_Oone__class_Oone(tc_Nat_Onat)))),v_m____)),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)) ),
% 0.44/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.44/1.41 fof(f172,axiom,(
% 0.44/1.41 (! [V_y_2,V_x_2,V_z_2] :( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),V_z_2)=> ( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),V_z_2),V_x_2),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),V_z_2),V_y_2))<=> c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_x_2,V_y_2) ) ) )),
% 0.44/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.44/1.41 fof(f212,axiom,(
% 0.44/1.41 (! [V_w,V_z] :( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_z,V_w)=> ( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_w,V_z)=> V_z = V_w ) ) )),
% 0.44/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.44/1.41 fof(f216,axiom,(
% 0.44/1.41 (! [V_w] : c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_w,V_w) )),
% 0.44/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.44/1.41 fof(f231,axiom,(
% 0.44/1.41 (! [V_w,V_z] : hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),V_z),V_w) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),V_w),V_z) )),
% 0.44/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.44/1.41 fof(f249,axiom,(
% 0.44/1.41 (! [V_y_2,V_x_2] :( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,V_x_2,V_y_2)<=> ( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_x_2,V_y_2)& V_x_2 != V_y_2 ) ) )),
% 0.44/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.44/1.41 fof(f271,axiom,(
% 0.44/1.41 (! [V_z] : hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)),V_z) = V_z )),
% 0.44/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.44/1.41 fof(f1288,conjecture,(
% 0.44/1.41 c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),hAPP(hAPP(c_Power_Opower__class_Opower(tc_RealDef_Oreal),v_t____),v_k____)),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),v_t____),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),hAPP(hAPP(c_Power_Opower__class_Opower(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_w____)),c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_k____,c_Groups_Oone__class_Oone(tc_Nat_Onat)))),v_m____))),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),hAPP(hAPP(c_Power_Opower__class_Opower(tc_RealDef_Oreal),v_t____),v_k____)),c_Groups_Oone__class_Oone(tc_RealDef_Oreal))) ),
% 0.44/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.44/1.41 fof(f1289,negated_conjecture,(
% 0.44/1.41 ~(c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),hAPP(hAPP(c_Power_Opower__class_Opower(tc_RealDef_Oreal),v_t____),v_k____)),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),v_t____),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),hAPP(hAPP(c_Power_Opower__class_Opower(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_w____)),c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_k____,c_Groups_Oone__class_Oone(tc_Nat_Onat)))),v_m____))),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),hAPP(hAPP(c_Power_Opower__class_Opower(tc_RealDef_Oreal),v_t____),v_k____)),c_Groups_Oone__class_Oone(tc_RealDef_Oreal))) )),
% 0.44/1.41 inference(negated_conjecture,[status(cth)],[f1288])).
% 0.44/1.41 fof(f1297,plain,(
% 0.44/1.41 c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),hAPP(hAPP(c_Power_Opower__class_Opower(tc_RealDef_Oreal),v_t____),v_k____))),
% 6.05/1.42 inference(cnf_transformation,[status(thm)],[f6])).
% 6.05/1.42 fof(f1298,plain,(
% 6.05/1.42 c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),v_t____),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),hAPP(hAPP(c_Power_Opower__class_Opower(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_w____)),c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_k____,c_Groups_Oone__class_Oone(tc_Nat_Onat)))),v_m____)),c_Groups_Oone__class_Oone(tc_RealDef_Oreal))),
% 6.05/1.42 inference(cnf_transformation,[status(thm)],[f7])).
% 6.05/1.42 fof(f1841,plain,(
% 6.05/1.42 ![V_y_2,V_x_2,V_z_2]: (~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),V_z_2)|(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),V_z_2),V_x_2),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),V_z_2),V_y_2))<=>c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_x_2,V_y_2)))),
% 6.05/1.42 inference(pre_NNF_transformation,[status(thm)],[f172])).
% 6.05/1.42 fof(f1842,plain,(
% 6.05/1.42 ![V_y_2,V_x_2,V_z_2]: (~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),V_z_2)|((~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),V_z_2),V_x_2),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),V_z_2),V_y_2))|c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_x_2,V_y_2))&(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),V_z_2),V_x_2),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),V_z_2),V_y_2))|~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_x_2,V_y_2))))),
% 6.05/1.42 inference(NNF_transformation,[status(thm)],[f1841])).
% 6.05/1.42 fof(f1843,plain,(
% 6.05/1.42 ![V_z_2]: (~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),V_z_2)|((![V_y_2,V_x_2]: (~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),V_z_2),V_x_2),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),V_z_2),V_y_2))|c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_x_2,V_y_2)))&(![V_y_2,V_x_2]: (c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),V_z_2),V_x_2),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),V_z_2),V_y_2))|~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_x_2,V_y_2)))))),
% 6.05/1.42 inference(miniscoping,[status(thm)],[f1842])).
% 6.05/1.42 fof(f1844,plain,(
% 6.05/1.42 ![X0,X1,X2]: (~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),X0)|~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),X0),X1),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),X0),X2))|c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X1,X2))),
% 6.05/1.42 inference(cnf_transformation,[status(thm)],[f1843])).
% 6.05/1.42 fof(f1845,plain,(
% 6.05/1.42 ![X0,X1,X2]: (~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),X0)|c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),X0),X1),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),X0),X2))|~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X1,X2))),
% 6.05/1.42 inference(cnf_transformation,[status(thm)],[f1843])).
% 6.05/1.42 fof(f1957,plain,(
% 6.05/1.42 ![V_w,V_z]: (~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_z,V_w)|(~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_w,V_z)|V_z=V_w))),
% 6.05/1.42 inference(pre_NNF_transformation,[status(thm)],[f212])).
% 6.05/1.42 fof(f1958,plain,(
% 6.05/1.42 ![X0,X1]: (~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X0,X1)|~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X1,X0)|X0=X1)),
% 6.05/1.42 inference(cnf_transformation,[status(thm)],[f1957])).
% 6.05/1.42 fof(f1966,plain,(
% 6.05/1.42 ![X0]: (c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X0,X0))),
% 6.05/1.42 inference(cnf_transformation,[status(thm)],[f216])).
% 6.05/1.42 fof(f2000,plain,(
% 6.05/1.42 ![X0,X1]: (hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),X0),X1)=hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),X1),X0))),
% 6.05/1.42 inference(cnf_transformation,[status(thm)],[f231])).
% 6.05/1.42 fof(f2049,plain,(
% 6.05/1.42 ![V_y_2,V_x_2]: ((~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,V_x_2,V_y_2)|(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_x_2,V_y_2)&~V_x_2=V_y_2))&(c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,V_x_2,V_y_2)|(~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_x_2,V_y_2)|V_x_2=V_y_2)))),
% 6.05/1.42 inference(NNF_transformation,[status(thm)],[f249])).
% 6.05/1.42 fof(f2050,plain,(
% 6.05/1.42 (![V_y_2,V_x_2]: (~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,V_x_2,V_y_2)|(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_x_2,V_y_2)&~V_x_2=V_y_2)))&(![V_y_2,V_x_2]: (c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,V_x_2,V_y_2)|(~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_x_2,V_y_2)|V_x_2=V_y_2)))),
% 6.05/1.42 inference(miniscoping,[status(thm)],[f2049])).
% 6.05/1.42 fof(f2051,plain,(
% 6.05/1.42 ![X0,X1]: (~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X0,X1)|c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X0,X1))),
% 6.05/1.42 inference(cnf_transformation,[status(thm)],[f2050])).
% 6.05/1.42 fof(f2052,plain,(
% 6.05/1.42 ![X0,X1]: (~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X0,X1)|~X0=X1)),
% 6.05/1.42 inference(cnf_transformation,[status(thm)],[f2050])).
% 6.05/1.42 fof(f2053,plain,(
% 6.05/1.42 ![X0,X1]: (c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X0,X1)|~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X0,X1)|X0=X1)),
% 6.05/1.42 inference(cnf_transformation,[status(thm)],[f2050])).
% 6.05/1.42 fof(f2119,plain,(
% 6.05/1.42 ![X0]: (hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)),X0)=X0)),
% 6.05/1.42 inference(cnf_transformation,[status(thm)],[f271])).
% 6.05/1.42 fof(f4786,plain,(
% 6.05/1.42 ~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),hAPP(hAPP(c_Power_Opower__class_Opower(tc_RealDef_Oreal),v_t____),v_k____)),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),v_t____),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),hAPP(hAPP(c_Power_Opower__class_Opower(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_w____)),c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_k____,c_Groups_Oone__class_Oone(tc_Nat_Onat)))),v_m____))),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),hAPP(hAPP(c_Power_Opower__class_Opower(tc_RealDef_Oreal),v_t____),v_k____)),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)))),
% 6.05/1.42 inference(cnf_transformation,[status(thm)],[f1289])).
% 6.05/1.42 fof(f4836,plain,(
% 6.05/1.42 ![X0]: (~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X0,X0))),
% 6.05/1.42 inference(destructive_equality_resolution,[status(thm)],[f2052])).
% 6.05/1.42 fof(f5046,plain,(
% 6.05/1.42 c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),v_t____),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),hAPP(hAPP(c_Power_Opower__class_Opower(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_w____)),c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_k____,c_Groups_Oone__class_Oone(tc_Nat_Onat)))),v_m____)),c_Groups_Oone__class_Oone(tc_RealDef_Oreal))),
% 6.05/1.42 inference(resolution,[status(thm)],[f2051,f1298])).
% 6.05/1.42 fof(f5140,plain,(
% 6.05/1.42 ~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),hAPP(hAPP(c_Power_Opower__class_Opower(tc_RealDef_Oreal),v_t____),v_k____)),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),v_t____),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),hAPP(hAPP(c_Power_Opower__class_Opower(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_w____)),c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_k____,c_Groups_Oone__class_Oone(tc_Nat_Onat)))),v_m____))),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),hAPP(hAPP(c_Power_Opower__class_Opower(tc_RealDef_Oreal),v_t____),v_k____)),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)))|hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),hAPP(hAPP(c_Power_Opower__class_Opower(tc_RealDef_Oreal),v_t____),v_k____)),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),v_t____),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),hAPP(hAPP(c_Power_Opower__class_Opower(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_w____)),c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_k____,c_Groups_Oone__class_Oone(tc_Nat_Onat)))),v_m____)))=hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),hAPP(hAPP(c_Power_Opower__class_Opower(tc_RealDef_Oreal),v_t____),v_k____)),c_Groups_Oone__class_Oone(tc_RealDef_Oreal))),
% 6.05/1.42 inference(resolution,[status(thm)],[f2053,f4786])).
% 6.05/1.42 fof(f5143,plain,(
% 6.05/1.42 hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),hAPP(hAPP(c_Power_Opower__class_Opower(tc_RealDef_Oreal),v_t____),v_k____)),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),v_t____),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),hAPP(hAPP(c_Power_Opower__class_Opower(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_w____)),c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_k____,c_Groups_Oone__class_Oone(tc_Nat_Onat)))),v_m____)))=hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),hAPP(hAPP(c_Power_Opower__class_Opower(tc_RealDef_Oreal),v_t____),v_k____)),c_Groups_Oone__class_Oone(tc_RealDef_Oreal))|~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),hAPP(hAPP(c_Power_Opower__class_Opower(tc_RealDef_Oreal),v_t____),v_k____))|~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),v_t____),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),hAPP(hAPP(c_Power_Opower__class_Opower(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_w____)),c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_k____,c_Groups_Oone__class_Oone(tc_Nat_Onat)))),v_m____)),c_Groups_Oone__class_Oone(tc_RealDef_Oreal))),
% 6.05/1.42 inference(resolution,[status(thm)],[f5140,f1845])).
% 6.05/1.42 fof(f5146,plain,(
% 6.05/1.42 hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),hAPP(hAPP(c_Power_Opower__class_Opower(tc_RealDef_Oreal),v_t____),v_k____)),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),v_t____),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),hAPP(hAPP(c_Power_Opower__class_Opower(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_w____)),c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_k____,c_Groups_Oone__class_Oone(tc_Nat_Onat)))),v_m____)))=hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),hAPP(hAPP(c_Power_Opower__class_Opower(tc_RealDef_Oreal),v_t____),v_k____)),c_Groups_Oone__class_Oone(tc_RealDef_Oreal))|~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),v_t____),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),hAPP(hAPP(c_Power_Opower__class_Opower(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_w____)),c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_k____,c_Groups_Oone__class_Oone(tc_Nat_Onat)))),v_m____)),c_Groups_Oone__class_Oone(tc_RealDef_Oreal))),
% 6.05/1.42 inference(forward_subsumption_resolution,[status(thm)],[f5143,f1297])).
% 6.05/1.42 fof(f5658,plain,(
% 6.05/1.42 ![X0]: (X0=hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),X0),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)))),
% 6.05/1.42 inference(paramodulation,[status(thm)],[f2119,f2000])).
% 6.05/1.42 fof(f5724,plain,(
% 6.05/1.42 hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),hAPP(hAPP(c_Power_Opower__class_Opower(tc_RealDef_Oreal),v_t____),v_k____)),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),v_t____),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),hAPP(hAPP(c_Power_Opower__class_Opower(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_w____)),c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_k____,c_Groups_Oone__class_Oone(tc_Nat_Onat)))),v_m____)))=hAPP(hAPP(c_Power_Opower__class_Opower(tc_RealDef_Oreal),v_t____),v_k____)|~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),v_t____),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),hAPP(hAPP(c_Power_Opower__class_Opower(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_w____)),c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_k____,c_Groups_Oone__class_Oone(tc_Nat_Onat)))),v_m____)),c_Groups_Oone__class_Oone(tc_RealDef_Oreal))),
% 6.05/1.42 inference(backward_demodulation,[status(thm)],[f5658,f5146])).
% 6.05/1.42 fof(f5813,plain,(
% 6.05/1.42 hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),hAPP(hAPP(c_Power_Opower__class_Opower(tc_RealDef_Oreal),v_t____),v_k____)),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),v_t____),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),hAPP(hAPP(c_Power_Opower__class_Opower(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_w____)),c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_k____,c_Groups_Oone__class_Oone(tc_Nat_Onat)))),v_m____)))=hAPP(hAPP(c_Power_Opower__class_Opower(tc_RealDef_Oreal),v_t____),v_k____)),
% 6.05/1.42 inference(forward_subsumption_resolution,[status(thm)],[f5724,f5046])).
% 6.05/1.42 fof(f6018,plain,(
% 6.05/1.42 ![X0]: (~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),hAPP(hAPP(c_Power_Opower__class_Opower(tc_RealDef_Oreal),v_t____),v_k____))|~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),hAPP(hAPP(c_Power_Opower__class_Opower(tc_RealDef_Oreal),v_t____),v_k____)),X0),hAPP(hAPP(c_Power_Opower__class_Opower(tc_RealDef_Oreal),v_t____),v_k____))|c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X0,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),v_t____),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),hAPP(hAPP(c_Power_Opower__class_Opower(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_w____)),c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_k____,c_Groups_Oone__class_Oone(tc_Nat_Onat)))),v_m____))))),
% 6.05/1.42 inference(paramodulation,[status(thm)],[f5813,f1844])).
% 6.05/1.42 fof(f6023,plain,(
% 6.05/1.42 ![X0]: (~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),hAPP(hAPP(c_Power_Opower__class_Opower(tc_RealDef_Oreal),v_t____),v_k____)),X0),hAPP(hAPP(c_Power_Opower__class_Opower(tc_RealDef_Oreal),v_t____),v_k____))|c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X0,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),v_t____),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),hAPP(hAPP(c_Power_Opower__class_Opower(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_w____)),c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_k____,c_Groups_Oone__class_Oone(tc_Nat_Onat)))),v_m____))))),
% 6.05/1.42 inference(forward_subsumption_resolution,[status(thm)],[f6018,f1297])).
% 6.05/1.42 fof(f6065,plain,(
% 6.05/1.42 ~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,hAPP(hAPP(c_Power_Opower__class_Opower(tc_RealDef_Oreal),v_t____),v_k____),hAPP(hAPP(c_Power_Opower__class_Opower(tc_RealDef_Oreal),v_t____),v_k____))|c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_RealDef_Oreal),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),v_t____),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),hAPP(hAPP(c_Power_Opower__class_Opower(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_w____)),c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_k____,c_Groups_Oone__class_Oone(tc_Nat_Onat)))),v_m____)))),
% 6.05/1.42 inference(paramodulation,[status(thm)],[f5658,f6023])).
% 6.05/1.42 fof(f6069,plain,(
% 6.05/1.42 c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_RealDef_Oreal),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),v_t____),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),hAPP(hAPP(c_Power_Opower__class_Opower(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_w____)),c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_k____,c_Groups_Oone__class_Oone(tc_Nat_Onat)))),v_m____)))),
% 6.05/1.42 inference(forward_subsumption_resolution,[status(thm)],[f6065,f1966])).
% 6.05/1.42 fof(f6262,plain,(
% 6.05/1.42 ~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),v_t____),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),hAPP(hAPP(c_Power_Opower__class_Opower(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_w____)),c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_k____,c_Groups_Oone__class_Oone(tc_Nat_Onat)))),v_m____)),c_Groups_Oone__class_Oone(tc_RealDef_Oreal))|hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),v_t____),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),hAPP(hAPP(c_Power_Opower__class_Opower(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_w____)),c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_k____,c_Groups_Oone__class_Oone(tc_Nat_Onat)))),v_m____))=c_Groups_Oone__class_Oone(tc_RealDef_Oreal)),
% 6.05/1.45 inference(resolution,[status(thm)],[f6069,f1958])).
% 6.05/1.45 fof(f6271,plain,(
% 6.05/1.45 c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_RealDef_Oreal),c_Groups_Oone__class_Oone(tc_RealDef_Oreal))),
% 6.05/1.45 inference(backward_demodulation,[status(thm)],[f6282,f1298])).
% 6.05/1.45 fof(f6282,plain,(
% 6.05/1.45 hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),v_t____),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),hAPP(hAPP(c_Power_Opower__class_Opower(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_w____)),c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_k____,c_Groups_Oone__class_Oone(tc_Nat_Onat)))),v_m____))=c_Groups_Oone__class_Oone(tc_RealDef_Oreal)),
% 6.05/1.45 inference(forward_subsumption_resolution,[status(thm)],[f6262,f5046])).
% 6.05/1.45 fof(f6283,plain,(
% 6.05/1.45 $false),
% 6.05/1.45 inference(forward_subsumption_resolution,[status(thm)],[f6271,f4836])).
% 6.05/1.45 % SZS output end CNFRefutation for theBenchmark.p
% 6.05/1.49 % Elapsed time: 1.014828 seconds
% 6.05/1.49 % CPU time: 6.631501 seconds
% 6.05/1.49 % Total memory used: 261.044 MB
% 6.05/1.49 % Net memory used: 257.519 MB
%------------------------------------------------------------------------------