%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWW259+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:53 PM UTC 2026
% Result : Theorem 19.32s 3.12s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWW259+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.05 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.16/0.43 % Computer : n014.cluster.edu
% 0.16/0.43 % Model : x86_64 x86_64
% 0.16/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.43 % Memory : 8046.5625MB
% 0.16/0.43 % OS : Linux 6.8.0-71-generic
% 0.16/0.43 % CPULimit : 300
% 0.16/0.43 % WCLimit : 300
% 0.16/0.43 % DateTime : Mon Sep 21 09:44:34 UTC 2026
% 0.16/0.43 % CPUTime :
% 0.26/0.56 % Drodi V4.1.1
% 19.32/3.12 % Refutation found
% 19.32/3.12 % SZS status Theorem for theBenchmark: Theorem is valid
% 19.32/3.12 % SZS output start CNFRefutation for theBenchmark
% 19.32/3.12 fof(f2,axiom,(
% 19.32/3.12 (! [V_d2] :( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),V_d2)=> (? [B_e] :( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),B_e)& c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,B_e,c_Groups_Oone__class_Oone(tc_RealDef_Oreal))& c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,B_e,V_d2) ) )) )),
% 19.32/3.12 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 19.32/3.12 fof(f4,axiom,(
% 19.32/3.12 c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_Rings_Oinverse__class_Oinverse(tc_RealDef_Oreal,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____))) ),
% 19.32/3.12 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 19.32/3.12 fof(f121,axiom,(
% 19.32/3.12 (! [V_n,V_x,T_a] :( class_RealVector_Oreal__normed__div__algebra(T_a)=> c_RealVector_Onorm__class_Onorm(T_a,hAPP(hAPP(c_Power_Opower__class_Opower(T_a),V_x),V_n)) = hAPP(hAPP(c_Power_Opower__class_Opower(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(T_a,V_x)),V_n) ) )),
% 19.32/3.12 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 19.32/3.12 fof(f609,axiom,(
% 19.32/3.12 (! [V_n] : c_Nat_OSuc(V_n) = c_Groups_Oplus__class_Oplus(tc_Nat_Onat,V_n,c_Groups_Oone__class_Oone(tc_Nat_Onat)) )),
% 19.32/3.12 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 19.32/3.12 fof(f1164,axiom,(
% 19.32/3.12 class_RealVector_Oreal__normed__div__algebra(tc_Complex_Ocomplex) ),
% 19.32/3.12 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 19.32/3.12 fof(f1257,hypothesis,(
% 19.32/3.12 (! [B_t] :( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),B_t)=> ( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,B_t,c_Groups_Oone__class_Oone(tc_RealDef_Oreal))=> ( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,B_t,c_Rings_Oinverse__class_Oinverse(tc_RealDef_Oreal,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____)))=> v_thesis____ ) ) ) )),
% 19.32/3.12 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 19.32/3.12 fof(f1258,conjecture,(
% 19.32/3.12 v_thesis____ ),
% 19.32/3.12 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 19.32/3.12 fof(f1259,negated_conjecture,(
% 19.32/3.12 ~(v_thesis____ )),
% 19.32/3.12 inference(negated_conjecture,[status(cth)],[f1258])).
% 19.32/3.12 fof(f1263,plain,(
% 19.32/3.12 ![V_d2]: (~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),V_d2)|(?[B_e]: ((c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),B_e)&c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,B_e,c_Groups_Oone__class_Oone(tc_RealDef_Oreal)))&c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,B_e,V_d2))))),
% 19.32/3.12 inference(pre_NNF_transformation,[status(thm)],[f2])).
% 19.32/3.12 fof(f1264,plain,(
% 19.32/3.12 ![V_d2]: (~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),V_d2)|((c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),sK1_skl(V_d2))&c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,sK1_skl(V_d2),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)))&c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,sK1_skl(V_d2),V_d2)))),
% 19.32/3.12 inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl]),skolemize(B_e,sK1_skl(V_d2))],[f1263])).
% 19.32/3.12 fof(f1265,plain,(
% 19.32/3.12 ![X0]: (~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),X0)|c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),sK1_skl(X0)))),
% 19.32/3.12 inference(cnf_transformation,[status(thm)],[f1264])).
% 19.32/3.12 fof(f1266,plain,(
% 19.32/3.12 ![X0]: (~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),X0)|c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,sK1_skl(X0),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)))),
% 19.32/3.12 inference(cnf_transformation,[status(thm)],[f1264])).
% 19.32/3.12 fof(f1267,plain,(
% 19.32/3.12 ![X0]: (~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),X0)|c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,sK1_skl(X0),X0))),
% 19.32/3.12 inference(cnf_transformation,[status(thm)],[f1264])).
% 19.32/3.12 fof(f1269,plain,(
% 19.32/3.12 c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_Rings_Oinverse__class_Oinverse(tc_RealDef_Oreal,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____)))),
% 19.32/3.12 inference(cnf_transformation,[status(thm)],[f4])).
% 19.32/3.12 fof(f1644,plain,(
% 19.32/3.12 ![V_n,V_x,T_a]: (~class_RealVector_Oreal__normed__div__algebra(T_a)|c_RealVector_Onorm__class_Onorm(T_a,hAPP(hAPP(c_Power_Opower__class_Opower(T_a),V_x),V_n))=hAPP(hAPP(c_Power_Opower__class_Opower(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(T_a,V_x)),V_n))),
% 19.32/3.12 inference(pre_NNF_transformation,[status(thm)],[f121])).
% 19.32/3.12 fof(f1645,plain,(
% 19.32/3.12 ![T_a]: (~class_RealVector_Oreal__normed__div__algebra(T_a)|(![V_n,V_x]: c_RealVector_Onorm__class_Onorm(T_a,hAPP(hAPP(c_Power_Opower__class_Opower(T_a),V_x),V_n))=hAPP(hAPP(c_Power_Opower__class_Opower(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(T_a,V_x)),V_n)))),
% 19.32/3.12 inference(miniscoping,[status(thm)],[f1644])).
% 19.32/3.12 fof(f1646,plain,(
% 19.32/3.12 ![X0,X1,X2]: (~class_RealVector_Oreal__normed__div__algebra(X0)|c_RealVector_Onorm__class_Onorm(X0,hAPP(hAPP(c_Power_Opower__class_Opower(X0),X1),X2))=hAPP(hAPP(c_Power_Opower__class_Opower(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(X0,X1)),X2))),
% 19.32/3.12 inference(cnf_transformation,[status(thm)],[f1645])).
% 19.32/3.12 fof(f3114,plain,(
% 19.32/3.12 ![X0]: (c_Nat_OSuc(X0)=c_Groups_Oplus__class_Oplus(tc_Nat_Onat,X0,c_Groups_Oone__class_Oone(tc_Nat_Onat)))),
% 19.32/3.12 inference(cnf_transformation,[status(thm)],[f609])).
% 19.32/3.12 fof(f4565,plain,(
% 19.32/3.12 class_RealVector_Oreal__normed__div__algebra(tc_Complex_Ocomplex)),
% 19.32/3.12 inference(cnf_transformation,[status(thm)],[f1164])).
% 19.32/3.12 fof(f4713,plain,(
% 19.32/3.12 ![B_t]: (~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),B_t)|(~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,B_t,c_Groups_Oone__class_Oone(tc_RealDef_Oreal))|(~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,B_t,c_Rings_Oinverse__class_Oinverse(tc_RealDef_Oreal,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____)))|v_thesis____)))),
% 19.32/3.12 inference(pre_NNF_transformation,[status(thm)],[f1257])).
% 19.32/3.12 fof(f4714,plain,(
% 19.32/3.12 ![X0]: (~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),X0)|~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X0,c_Groups_Oone__class_Oone(tc_RealDef_Oreal))|~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X0,c_Rings_Oinverse__class_Oinverse(tc_RealDef_Oreal,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____)))|v_thesis____)),
% 19.32/3.12 inference(cnf_transformation,[status(thm)],[f4713])).
% 19.32/3.12 fof(f4715,plain,(
% 19.32/3.12 ~v_thesis____),
% 19.32/3.12 inference(cnf_transformation,[status(thm)],[f1259])).
% 19.32/3.12 fof(f4853,plain,(
% 19.32/3.12 c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_Rings_Oinverse__class_Oinverse(tc_RealDef_Oreal,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_Nat_OSuc(v_k____))),v_m____)))),
% 19.32/3.12 inference(backward_demodulation,[status(thm)],[f3114,f1269])).
% 19.32/3.12 fof(f4971,plain,(
% 19.32/3.12 ![X0]: (~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),X0)|~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X0,c_Groups_Oone__class_Oone(tc_RealDef_Oreal))|~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X0,c_Rings_Oinverse__class_Oinverse(tc_RealDef_Oreal,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_Nat_OSuc(v_k____))),v_m____)))|v_thesis____)),
% 19.32/3.12 inference(forward_demodulation,[status(thm)],[f3114,f4714])).
% 19.32/3.12 fof(f4972,plain,(
% 19.32/3.12 ![X0]: (~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),X0)|~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X0,c_Groups_Oone__class_Oone(tc_RealDef_Oreal))|~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X0,c_Rings_Oinverse__class_Oinverse(tc_RealDef_Oreal,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_Nat_OSuc(v_k____))),v_m____))))),
% 19.32/3.12 inference(backward_subsumption_resolution,[status(thm)],[f4971,f4715])).
% 19.32/3.12 fof(f6349,plain,(
% 19.32/3.12 ![X0,X1]: (c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex),X0),X1))=hAPP(hAPP(c_Power_Opower__class_Opower(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,X0)),X1))),
% 19.32/3.12 inference(resolution,[status(thm)],[f1646,f4565])).
% 19.32/3.12 fof(f6360,plain,(
% 19.32/3.12 ![X0]: (~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),X0)|~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X0,c_Groups_Oone__class_Oone(tc_RealDef_Oreal))|~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X0,c_Rings_Oinverse__class_Oinverse(tc_RealDef_Oreal,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex),v_w____),c_Nat_OSuc(v_k____)))),v_m____))))),
% 19.32/3.12 inference(backward_demodulation,[status(thm)],[f6349,f4972])).
% 19.32/3.12 fof(f6361,plain,(
% 19.32/3.12 c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_Rings_Oinverse__class_Oinverse(tc_RealDef_Oreal,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex),v_w____),c_Nat_OSuc(v_k____)))),v_m____)))),
% 19.32/3.12 inference(backward_demodulation,[status(thm)],[f6349,f4853])).
% 19.32/3.12 fof(f6369,plain,(
% 19.32/3.12 ![X0]: (~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),sK1_skl(X0))|~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,sK1_skl(X0),c_Rings_Oinverse__class_Oinverse(tc_RealDef_Oreal,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex),v_w____),c_Nat_OSuc(v_k____)))),v_m____)))|~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),X0))),
% 19.32/3.12 inference(resolution,[status(thm)],[f6360,f1266])).
% 19.32/3.12 fof(f6371,plain,(
% 19.32/3.12 ![X0]: (~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,sK1_skl(X0),c_Rings_Oinverse__class_Oinverse(tc_RealDef_Oreal,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex),v_w____),c_Nat_OSuc(v_k____)))),v_m____)))|~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),X0))),
% 19.32/3.12 inference(forward_subsumption_resolution,[status(thm)],[f6369,f1265])).
% 19.32/3.12 fof(f6549,plain,(
% 19.32/3.12 ~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_Rings_Oinverse__class_Oinverse(tc_RealDef_Oreal,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex),v_w____),c_Nat_OSuc(v_k____)))),v_m____)))|~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_Rings_Oinverse__class_Oinverse(tc_RealDef_Oreal,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex),v_w____),c_Nat_OSuc(v_k____)))),v_m____)))),
% 20.16/3.18 inference(resolution,[status(thm)],[f6371,f1267])).
% 20.16/3.18 fof(f6553,plain,(
% 20.16/3.18 ~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_Rings_Oinverse__class_Oinverse(tc_RealDef_Oreal,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex),v_w____),c_Nat_OSuc(v_k____)))),v_m____)))),
% 20.16/3.18 inference(duplicate_literals_removal,[status(thm)],[f6549])).
% 20.16/3.18 fof(f6554,plain,(
% 20.16/3.18 $false),
% 20.16/3.18 inference(forward_subsumption_resolution,[status(thm)],[f6553,f6361])).
% 20.16/3.18 % SZS output end CNFRefutation for theBenchmark.p
% 20.16/3.20 % Elapsed time: 2.747130 seconds
% 20.16/3.20 % CPU time: 20.414188 seconds
% 20.16/3.20 % Total memory used: 397.687 MB
% 20.16/3.20 % Net memory used: 391.877 MB
%------------------------------------------------------------------------------