%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWW256+1 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/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 03:08:52 PM UTC 2026
% Result : Theorem 67.01s 9.17s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SWW256+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.07 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.19/0.46 % Computer : n014.cluster.edu
% 0.19/0.46 % Model : x86_64 x86_64
% 0.19/0.46 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.19/0.46 % Memory : 8046.5625MB
% 0.19/0.46 % OS : Linux 6.8.0-71-generic
% 0.19/0.46 % CPULimit : 300
% 0.19/0.46 % WCLimit : 300
% 0.19/0.46 % DateTime : Mon Sep 21 09:44:19 UTC 2026
% 0.19/0.46 % CPUTime :
% 0.38/0.66 % Drodi V4.1.1
% 67.01/9.17 % Refutation found
% 67.01/9.17 % SZS status Theorem for theBenchmark: Theorem is valid
% 67.01/9.17 % SZS output start CNFRefutation for theBenchmark
% 67.01/9.17 fof(f2,axiom,(
% 67.01/9.17 v_k____ != c_Groups_Ozero__class_Ozero(tc_Nat_Onat) ),
% 67.01/9.17 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 67.01/9.17 fof(f5,axiom,(
% 67.01/9.17 (! [V_q,V_x,T_a] :( class_Rings_Ocomm__semiring__1(T_a)=> hAPP(hAPP(c_Power_Opower__class_Opower(T_a),V_x),c_Nat_OSuc(V_q)) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a),V_x),hAPP(hAPP(c_Power_Opower__class_Opower(T_a),V_x),V_q)) ) )),
% 67.01/9.17 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 67.01/9.17 fof(f73,axiom,(
% 67.01/9.17 (! [V_b,T_a] :( class_RealVector_Oreal__normed__algebra(T_a)=> hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a),c_Groups_Ozero__class_Ozero(T_a)),V_b) = c_Groups_Ozero__class_Ozero(T_a) ) )),
% 67.01/9.17 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 67.01/9.17 fof(f211,axiom,(
% 67.01/9.17 (! [V_n] : c_Nat_OSuc(V_n) = c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_Groups_Oone__class_Oone(tc_Nat_Onat),V_n) )),
% 67.01/9.17 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 67.01/9.17 fof(f214,axiom,(
% 67.01/9.17 (! [V_n,V_m] :( ~ c_Orderings_Oord__class_Oless(tc_Nat_Onat,V_m,V_n)=> c_Groups_Oplus__class_Oplus(tc_Nat_Onat,V_n,c_Groups_Ominus__class_Ominus(tc_Nat_Onat,V_m,V_n)) = V_m ) )),
% 67.01/9.17 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 67.01/9.17 fof(f429,axiom,(
% 67.01/9.17 (! [V_n_2] :( c_Orderings_Oord__class_Oless(tc_Nat_Onat,V_n_2,c_Nat_OSuc(c_Groups_Ozero__class_Ozero(tc_Nat_Onat)))<=> V_n_2 = c_Groups_Ozero__class_Ozero(tc_Nat_Onat) ) )),
% 67.01/9.17 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 67.01/9.17 fof(f445,axiom,(
% 67.01/9.17 c_Groups_Oone__class_Oone(tc_Nat_Onat) = c_Nat_OSuc(c_Groups_Ozero__class_Ozero(tc_Nat_Onat)) ),
% 67.01/9.17 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 67.01/9.17 fof(f667,axiom,(
% 67.01/9.17 hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_pa____),v_c____) = hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_q____),c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)) ),
% 67.01/9.17 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 67.01/9.17 fof(f764,axiom,(
% 67.01/9.17 hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_Osmult(tc_Complex_Ocomplex,c_Rings_Oinverse__class_Oinverse(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_q____),c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex))),v_q____)),c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)) = c_Groups_Oone__class_Oone(tc_Complex_Ocomplex) ),
% 67.01/9.17 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 67.01/9.17 fof(f767,axiom,(
% 67.01/9.17 (! [B_z] : hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_Osmult(tc_Complex_Ocomplex,c_Rings_Oinverse__class_Oinverse(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_q____),c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex))),v_q____)),B_z) = c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_Osmult(tc_Complex_Ocomplex,c_Rings_Oinverse__class_Oinverse(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_q____),c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex))),v_q____)),c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex),hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex),B_z),v_k____)),hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_OpCons(tc_Complex_Ocomplex,v_a____,v_s____)),B_z))) )),
% 67.01/9.17 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 67.01/9.17 fof(f803,axiom,(
% 67.01/9.17 ~ (! [B_x,B_y] : hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_Osmult(tc_Complex_Ocomplex,c_Rings_Oinverse__class_Oinverse(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_q____),c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex))),v_q____)),B_x) = hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_Osmult(tc_Complex_Ocomplex,c_Rings_Oinverse__class_Oinverse(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_q____),c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex))),v_q____)),B_y) )),
% 67.01/9.17 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 67.01/9.17 fof(f1185,axiom,(
% 67.01/9.17 class_RealVector_Oreal__normed__algebra(tc_Complex_Ocomplex) ),
% 67.01/9.17 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 67.01/9.17 fof(f1197,axiom,(
% 67.01/9.17 class_Rings_Ocomm__semiring__1(tc_Complex_Ocomplex) ),
% 67.01/9.17 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 67.01/9.17 fof(f1284,conjecture,(
% 67.01/9.17 (? [B_x,B_y] : hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex),B_x),hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex),B_x),c_Groups_Ominus__class_Ominus(tc_Nat_Onat,v_k____,c_Nat_OSuc(c_Groups_Ozero__class_Ozero(tc_Nat_Onat))))) != hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex),B_y),hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex),B_y),c_Groups_Ominus__class_Ominus(tc_Nat_Onat,v_k____,c_Nat_OSuc(c_Groups_Ozero__class_Ozero(tc_Nat_Onat))))) )),
% 67.01/9.17 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 67.01/9.17 fof(f1285,negated_conjecture,(
% 67.01/9.17 ~((? [B_x,B_y] : hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex),B_x),hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex),B_x),c_Groups_Ominus__class_Ominus(tc_Nat_Onat,v_k____,c_Nat_OSuc(c_Groups_Ozero__class_Ozero(tc_Nat_Onat))))) != hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex),B_y),hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex),B_y),c_Groups_Ominus__class_Ominus(tc_Nat_Onat,v_k____,c_Nat_OSuc(c_Groups_Ozero__class_Ozero(tc_Nat_Onat))))) ))),
% 67.01/9.17 inference(negated_conjecture,[status(cth)],[f1284])).
% 67.01/9.17 fof(f1289,plain,(
% 67.01/9.17 ~v_k____=c_Groups_Ozero__class_Ozero(tc_Nat_Onat)),
% 67.01/9.17 inference(cnf_transformation,[status(thm)],[f2])).
% 67.01/9.17 fof(f1294,plain,(
% 67.01/9.17 ![V_q,V_x,T_a]: (~class_Rings_Ocomm__semiring__1(T_a)|hAPP(hAPP(c_Power_Opower__class_Opower(T_a),V_x),c_Nat_OSuc(V_q))=hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a),V_x),hAPP(hAPP(c_Power_Opower__class_Opower(T_a),V_x),V_q)))),
% 67.01/9.17 inference(pre_NNF_transformation,[status(thm)],[f5])).
% 67.01/9.17 fof(f1295,plain,(
% 67.01/9.17 ![T_a]: (~class_Rings_Ocomm__semiring__1(T_a)|(![V_q,V_x]: hAPP(hAPP(c_Power_Opower__class_Opower(T_a),V_x),c_Nat_OSuc(V_q))=hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a),V_x),hAPP(hAPP(c_Power_Opower__class_Opower(T_a),V_x),V_q))))),
% 67.01/9.17 inference(miniscoping,[status(thm)],[f1294])).
% 67.01/9.17 fof(f1296,plain,(
% 67.01/9.17 ![X0,X1,X2]: (~class_Rings_Ocomm__semiring__1(X0)|hAPP(hAPP(c_Power_Opower__class_Opower(X0),X1),c_Nat_OSuc(X2))=hAPP(hAPP(c_Groups_Otimes__class_Otimes(X0),X1),hAPP(hAPP(c_Power_Opower__class_Opower(X0),X1),X2)))),
% 67.01/9.17 inference(cnf_transformation,[status(thm)],[f1295])).
% 67.01/9.17 fof(f1480,plain,(
% 67.01/9.17 ![V_b,T_a]: (~class_RealVector_Oreal__normed__algebra(T_a)|hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a),c_Groups_Ozero__class_Ozero(T_a)),V_b)=c_Groups_Ozero__class_Ozero(T_a))),
% 67.01/9.17 inference(pre_NNF_transformation,[status(thm)],[f73])).
% 67.01/9.17 fof(f1481,plain,(
% 67.01/9.17 ![T_a]: (~class_RealVector_Oreal__normed__algebra(T_a)|(![V_b]: hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a),c_Groups_Ozero__class_Ozero(T_a)),V_b)=c_Groups_Ozero__class_Ozero(T_a)))),
% 67.01/9.17 inference(miniscoping,[status(thm)],[f1480])).
% 67.01/9.17 fof(f1482,plain,(
% 67.01/9.17 ![X0,X1]: (~class_RealVector_Oreal__normed__algebra(X0)|hAPP(hAPP(c_Groups_Otimes__class_Otimes(X0),c_Groups_Ozero__class_Ozero(X0)),X1)=c_Groups_Ozero__class_Ozero(X0))),
% 67.01/9.17 inference(cnf_transformation,[status(thm)],[f1481])).
% 67.01/9.17 fof(f1907,plain,(
% 67.01/9.17 ![X0]: (c_Nat_OSuc(X0)=c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_Groups_Oone__class_Oone(tc_Nat_Onat),X0))),
% 67.01/9.17 inference(cnf_transformation,[status(thm)],[f211])).
% 67.01/9.17 fof(f1913,plain,(
% 67.01/9.17 ![V_n,V_m]: (c_Orderings_Oord__class_Oless(tc_Nat_Onat,V_m,V_n)|c_Groups_Oplus__class_Oplus(tc_Nat_Onat,V_n,c_Groups_Ominus__class_Ominus(tc_Nat_Onat,V_m,V_n))=V_m)),
% 67.01/9.17 inference(pre_NNF_transformation,[status(thm)],[f214])).
% 67.01/9.17 fof(f1914,plain,(
% 67.01/9.17 ![X0,X1]: (c_Orderings_Oord__class_Oless(tc_Nat_Onat,X0,X1)|c_Groups_Oplus__class_Oplus(tc_Nat_Onat,X1,c_Groups_Ominus__class_Ominus(tc_Nat_Onat,X0,X1))=X0)),
% 67.01/9.17 inference(cnf_transformation,[status(thm)],[f1913])).
% 67.01/9.17 fof(f2649,plain,(
% 67.01/9.17 ![V_n_2]: ((~c_Orderings_Oord__class_Oless(tc_Nat_Onat,V_n_2,c_Nat_OSuc(c_Groups_Ozero__class_Ozero(tc_Nat_Onat)))|V_n_2=c_Groups_Ozero__class_Ozero(tc_Nat_Onat))&(c_Orderings_Oord__class_Oless(tc_Nat_Onat,V_n_2,c_Nat_OSuc(c_Groups_Ozero__class_Ozero(tc_Nat_Onat)))|~V_n_2=c_Groups_Ozero__class_Ozero(tc_Nat_Onat)))),
% 67.01/9.17 inference(NNF_transformation,[status(thm)],[f429])).
% 67.01/9.17 fof(f2650,plain,(
% 67.01/9.17 (![V_n_2]: (~c_Orderings_Oord__class_Oless(tc_Nat_Onat,V_n_2,c_Nat_OSuc(c_Groups_Ozero__class_Ozero(tc_Nat_Onat)))|V_n_2=c_Groups_Ozero__class_Ozero(tc_Nat_Onat)))&(![V_n_2]: (c_Orderings_Oord__class_Oless(tc_Nat_Onat,V_n_2,c_Nat_OSuc(c_Groups_Ozero__class_Ozero(tc_Nat_Onat)))|~V_n_2=c_Groups_Ozero__class_Ozero(tc_Nat_Onat)))),
% 67.01/9.17 inference(miniscoping,[status(thm)],[f2649])).
% 67.01/9.17 fof(f2651,plain,(
% 67.01/9.17 ![X0]: (~c_Orderings_Oord__class_Oless(tc_Nat_Onat,X0,c_Nat_OSuc(c_Groups_Ozero__class_Ozero(tc_Nat_Onat)))|X0=c_Groups_Ozero__class_Ozero(tc_Nat_Onat))),
% 67.01/9.17 inference(cnf_transformation,[status(thm)],[f2650])).
% 67.01/9.17 fof(f2703,plain,(
% 67.01/9.17 c_Groups_Oone__class_Oone(tc_Nat_Onat)=c_Nat_OSuc(c_Groups_Ozero__class_Ozero(tc_Nat_Onat))),
% 67.01/9.17 inference(cnf_transformation,[status(thm)],[f445])).
% 67.01/9.17 fof(f3381,plain,(
% 67.01/9.17 hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_pa____),v_c____)=hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_q____),c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex))),
% 67.01/9.17 inference(cnf_transformation,[status(thm)],[f667])).
% 67.01/9.17 fof(f3686,plain,(
% 67.01/9.17 hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_Osmult(tc_Complex_Ocomplex,c_Rings_Oinverse__class_Oinverse(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_q____),c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex))),v_q____)),c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex))=c_Groups_Oone__class_Oone(tc_Complex_Ocomplex)),
% 67.01/9.17 inference(cnf_transformation,[status(thm)],[f764])).
% 67.01/9.17 fof(f3692,plain,(
% 67.01/9.17 ![X0]: (hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_Osmult(tc_Complex_Ocomplex,c_Rings_Oinverse__class_Oinverse(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_q____),c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex))),v_q____)),X0)=c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_Osmult(tc_Complex_Ocomplex,c_Rings_Oinverse__class_Oinverse(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_q____),c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex))),v_q____)),c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex),hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex),X0),v_k____)),hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_OpCons(tc_Complex_Ocomplex,v_a____,v_s____)),X0))))),
% 67.01/9.17 inference(cnf_transformation,[status(thm)],[f767])).
% 67.01/9.17 fof(f3803,plain,(
% 67.01/9.17 (?[B_x,B_y]: ~hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_Osmult(tc_Complex_Ocomplex,c_Rings_Oinverse__class_Oinverse(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_q____),c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex))),v_q____)),B_x)=hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_Osmult(tc_Complex_Ocomplex,c_Rings_Oinverse__class_Oinverse(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_q____),c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex))),v_q____)),B_y))),
% 67.01/9.17 inference(pre_NNF_transformation,[status(thm)],[f803])).
% 67.01/9.17 fof(f3804,plain,(
% 67.01/9.17 ~hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_Osmult(tc_Complex_Ocomplex,c_Rings_Oinverse__class_Oinverse(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_q____),c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex))),v_q____)),sK26_skl)=hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_Osmult(tc_Complex_Ocomplex,c_Rings_Oinverse__class_Oinverse(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_q____),c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex))),v_q____)),sK27_skl)),
% 67.01/9.17 inference(skolemize,[status(esa),new_symbols(skolem,[sK26_skl,sK27_skl]),skolemize(B_x,sK26_skl),skolemize(B_y,sK27_skl)],[f3803])).
% 67.01/9.17 fof(f3805,plain,(
% 67.01/9.17 ~hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_Osmult(tc_Complex_Ocomplex,c_Rings_Oinverse__class_Oinverse(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_q____),c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex))),v_q____)),sK26_skl)=hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_Osmult(tc_Complex_Ocomplex,c_Rings_Oinverse__class_Oinverse(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_q____),c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex))),v_q____)),sK27_skl)),
% 67.01/9.17 inference(cnf_transformation,[status(thm)],[f3804])).
% 67.01/9.17 fof(f4655,plain,(
% 67.01/9.17 class_RealVector_Oreal__normed__algebra(tc_Complex_Ocomplex)),
% 67.01/9.17 inference(cnf_transformation,[status(thm)],[f1185])).
% 67.01/9.17 fof(f4667,plain,(
% 67.01/9.17 class_Rings_Ocomm__semiring__1(tc_Complex_Ocomplex)),
% 67.01/9.17 inference(cnf_transformation,[status(thm)],[f1197])).
% 67.01/9.17 fof(f4814,plain,(
% 67.01/9.17 (![B_x,B_y]: hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex),B_x),hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex),B_x),c_Groups_Ominus__class_Ominus(tc_Nat_Onat,v_k____,c_Nat_OSuc(c_Groups_Ozero__class_Ozero(tc_Nat_Onat)))))=hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex),B_y),hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex),B_y),c_Groups_Ominus__class_Ominus(tc_Nat_Onat,v_k____,c_Nat_OSuc(c_Groups_Ozero__class_Ozero(tc_Nat_Onat))))))),
% 67.01/9.17 inference(pre_NNF_transformation,[status(thm)],[f1285])).
% 67.01/9.17 fof(f4815,plain,(
% 67.01/9.17 ![X0,X1]: (hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex),X0),hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex),X0),c_Groups_Ominus__class_Ominus(tc_Nat_Onat,v_k____,c_Nat_OSuc(c_Groups_Ozero__class_Ozero(tc_Nat_Onat)))))=hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex),X1),hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex),X1),c_Groups_Ominus__class_Ominus(tc_Nat_Onat,v_k____,c_Nat_OSuc(c_Groups_Ozero__class_Ozero(tc_Nat_Onat))))))),
% 67.01/9.17 inference(cnf_transformation,[status(thm)],[f4814])).
% 67.01/9.17 fof(f4938,plain,(
% 67.01/9.17 ![X0]: (~c_Orderings_Oord__class_Oless(tc_Nat_Onat,X0,c_Groups_Oone__class_Oone(tc_Nat_Onat))|X0=c_Groups_Ozero__class_Ozero(tc_Nat_Onat))),
% 67.01/9.17 inference(backward_demodulation,[status(thm)],[f2703,f2651])).
% 67.01/9.17 fof(f5046,plain,(
% 67.01/9.17 hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_Osmult(tc_Complex_Ocomplex,c_Rings_Oinverse__class_Oinverse(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_pa____),v_c____)),v_q____)),c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex))=c_Groups_Oone__class_Oone(tc_Complex_Ocomplex)),
% 67.01/9.17 inference(forward_demodulation,[status(thm)],[f3381,f3686])).
% 67.01/9.17 fof(f5052,plain,(
% 67.01/9.17 ![X0]: (hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_Osmult(tc_Complex_Ocomplex,c_Rings_Oinverse__class_Oinverse(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_pa____),v_c____)),v_q____)),X0)=c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_Osmult(tc_Complex_Ocomplex,c_Rings_Oinverse__class_Oinverse(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_q____),c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex))),v_q____)),c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex),hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex),X0),v_k____)),hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_OpCons(tc_Complex_Ocomplex,v_a____,v_s____)),X0))))),
% 67.01/9.17 inference(forward_demodulation,[status(thm)],[f3381,f3692])).
% 67.01/9.17 fof(f5053,plain,(
% 67.01/9.17 ![X0]: (hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_Osmult(tc_Complex_Ocomplex,c_Rings_Oinverse__class_Oinverse(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_pa____),v_c____)),v_q____)),X0)=c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_Osmult(tc_Complex_Ocomplex,c_Rings_Oinverse__class_Oinverse(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_pa____),v_c____)),v_q____)),c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex),hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex),X0),v_k____)),hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_OpCons(tc_Complex_Ocomplex,v_a____,v_s____)),X0))))),
% 67.01/9.17 inference(forward_demodulation,[status(thm)],[f3381,f5052])).
% 67.01/9.17 fof(f5054,plain,(
% 67.01/9.17 ![X0]: (hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_Osmult(tc_Complex_Ocomplex,c_Rings_Oinverse__class_Oinverse(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_pa____),v_c____)),v_q____)),X0)=c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex,c_Groups_Oone__class_Oone(tc_Complex_Ocomplex),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex),hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex),X0),v_k____)),hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_OpCons(tc_Complex_Ocomplex,v_a____,v_s____)),X0))))),
% 67.01/9.17 inference(forward_demodulation,[status(thm)],[f5046,f5053])).
% 67.01/9.17 fof(f5060,plain,(
% 67.01/9.17 ~hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_Osmult(tc_Complex_Ocomplex,c_Rings_Oinverse__class_Oinverse(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_pa____),v_c____)),v_q____)),sK26_skl)=hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_Osmult(tc_Complex_Ocomplex,c_Rings_Oinverse__class_Oinverse(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_q____),c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex))),v_q____)),sK27_skl)),
% 67.01/9.17 inference(forward_demodulation,[status(thm)],[f3381,f3805])).
% 67.01/9.17 fof(f5061,plain,(
% 67.01/9.17 ~hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_Osmult(tc_Complex_Ocomplex,c_Rings_Oinverse__class_Oinverse(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_pa____),v_c____)),v_q____)),sK26_skl)=hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_Osmult(tc_Complex_Ocomplex,c_Rings_Oinverse__class_Oinverse(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_pa____),v_c____)),v_q____)),sK27_skl)),
% 67.01/9.17 inference(forward_demodulation,[status(thm)],[f3381,f5060])).
% 67.01/9.17 fof(f5109,plain,(
% 67.01/9.17 ![X0,X1]: (hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex),X0),hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex),X0),c_Groups_Ominus__class_Ominus(tc_Nat_Onat,v_k____,c_Groups_Oone__class_Oone(tc_Nat_Onat))))=hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex),X1),hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex),X1),c_Groups_Ominus__class_Ominus(tc_Nat_Onat,v_k____,c_Nat_OSuc(c_Groups_Ozero__class_Ozero(tc_Nat_Onat))))))),
% 67.01/9.17 inference(forward_demodulation,[status(thm)],[f2703,f4815])).
% 67.01/9.17 fof(f5110,plain,(
% 67.01/9.17 ![X0,X1]: (hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex),X0),hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex),X0),c_Groups_Ominus__class_Ominus(tc_Nat_Onat,v_k____,c_Groups_Oone__class_Oone(tc_Nat_Onat))))=hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex),X1),hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex),X1),c_Groups_Ominus__class_Ominus(tc_Nat_Onat,v_k____,c_Groups_Oone__class_Oone(tc_Nat_Onat)))))),
% 67.01/9.17 inference(forward_demodulation,[status(thm)],[f2703,f5109])).
% 67.01/9.17 fof(f6053,plain,(
% 67.01/9.17 ![X0]: (c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_Groups_Oone__class_Oone(tc_Nat_Onat),c_Groups_Ominus__class_Ominus(tc_Nat_Onat,X0,c_Groups_Oone__class_Oone(tc_Nat_Onat)))=X0|X0=c_Groups_Ozero__class_Ozero(tc_Nat_Onat))),
% 67.01/9.17 inference(resolution,[status(thm)],[f1914,f4938])).
% 67.01/9.17 fof(f6062,plain,(
% 67.01/9.17 ![X0]: (c_Nat_OSuc(c_Groups_Ominus__class_Ominus(tc_Nat_Onat,X0,c_Groups_Oone__class_Oone(tc_Nat_Onat)))=X0|X0=c_Groups_Ozero__class_Ozero(tc_Nat_Onat))),
% 67.01/9.17 inference(forward_demodulation,[status(thm)],[f1907,f6053])).
% 67.01/9.17 fof(f14039,plain,(
% 67.01/9.17 ![X0]: (hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex),c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)),X0)=c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex))),
% 67.01/9.17 inference(resolution,[status(thm)],[f4655,f1482])).
% 67.01/9.17 fof(f14043,plain,(
% 67.01/9.17 ![X0]: (hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex),X0),hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex),X0),c_Groups_Ominus__class_Ominus(tc_Nat_Onat,v_k____,c_Groups_Oone__class_Oone(tc_Nat_Onat))))=c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex))),
% 67.01/9.17 inference(paramodulation,[status(thm)],[f5110,f14039])).
% 67.01/9.17 fof(f15514,plain,(
% 67.01/9.17 ![X0,X1]: (hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex),X0),c_Nat_OSuc(X1))=hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex),X0),hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex),X0),X1)))),
% 67.01/9.27 inference(resolution,[status(thm)],[f4667,f1296])).
% 67.01/9.27 fof(f15521,plain,(
% 67.01/9.27 ![X0]: (hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex),X0),c_Nat_OSuc(c_Groups_Ominus__class_Ominus(tc_Nat_Onat,v_k____,c_Groups_Oone__class_Oone(tc_Nat_Onat))))=c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex))),
% 67.01/9.27 inference(backward_demodulation,[status(thm)],[f15514,f14043])).
% 67.01/9.27 fof(f15713,plain,(
% 67.01/9.27 ![X0]: (hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex),X0),v_k____)=c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)|v_k____=c_Groups_Ozero__class_Ozero(tc_Nat_Onat))),
% 67.01/9.27 inference(paramodulation,[status(thm)],[f6062,f15521])).
% 67.01/9.27 fof(f15868,plain,(
% 67.01/9.27 ![X0]: (hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_Osmult(tc_Complex_Ocomplex,c_Rings_Oinverse__class_Oinverse(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_pa____),v_c____)),v_q____)),X0)=c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex,c_Groups_Oone__class_Oone(tc_Complex_Ocomplex),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex),c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)),hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_OpCons(tc_Complex_Ocomplex,v_a____,v_s____)),X0))))),
% 67.01/9.27 inference(backward_demodulation,[status(thm)],[f15869,f5054])).
% 67.01/9.27 fof(f15869,plain,(
% 67.01/9.27 ![X0]: (hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex),X0),v_k____)=c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex))),
% 67.01/9.27 inference(forward_subsumption_resolution,[status(thm)],[f15713,f1289])).
% 67.01/9.27 fof(f15905,plain,(
% 67.01/9.27 ~hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_Osmult(tc_Complex_Ocomplex,c_Rings_Oinverse__class_Oinverse(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_pa____),v_c____)),v_q____)),sK26_skl)=c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex,c_Groups_Oone__class_Oone(tc_Complex_Ocomplex),c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex))),
% 67.01/9.27 inference(backward_demodulation,[status(thm)],[f15911,f5061])).
% 67.01/9.27 fof(f15911,plain,(
% 67.01/9.27 ![X0]: (hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_Osmult(tc_Complex_Ocomplex,c_Rings_Oinverse__class_Oinverse(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_pa____),v_c____)),v_q____)),X0)=c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex,c_Groups_Oone__class_Oone(tc_Complex_Ocomplex),c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)))),
% 67.01/9.27 inference(forward_demodulation,[status(thm)],[f14039,f15868])).
% 67.01/9.27 fof(f15912,plain,(
% 67.01/9.27 ~c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex,c_Groups_Oone__class_Oone(tc_Complex_Ocomplex),c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex))=c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex,c_Groups_Oone__class_Oone(tc_Complex_Ocomplex),c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex))),
% 67.01/9.27 inference(forward_demodulation,[status(thm)],[f15911,f15905])).
% 67.01/9.27 fof(f15913,plain,(
% 67.01/9.27 $false),
% 67.01/9.27 inference(trivial_equality_resolution,[status(thm)],[f15912])).
% 67.01/9.27 % SZS output end CNFRefutation for theBenchmark.p
% 48.16/9.33 % Elapsed time: 8.835685 seconds
% 48.16/9.33 % CPU time: 67.914135 seconds
% 48.16/9.33 % Total memory used: 633.192 MB
% 48.16/9.33 % Net memory used: 612.416 MB
%------------------------------------------------------------------------------