%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWW192+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 : n026.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:47 PM UTC 2026
% Result : Theorem 139.78s 33.29s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWW192+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.03/15.40 % Computer : n026.cluster.edu
% 0.03/15.40 % Model : x86_64 x86_64
% 0.03/15.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.03/15.40 % Memory : 8046.5625MB
% 0.03/15.40 % OS : Linux 6.8.0-71-generic
% 0.03/15.40 % CPULimit : 300
% 0.03/15.40 % WCLimit : 300
% 0.03/15.40 % DateTime : Mon Sep 21 09:43:54 UTC 2026
% 0.03/15.40 % CPUTime :
% 0.17/15.56 % Drodi V4.1.1
% 139.78/33.29 % Refutation found
% 139.78/33.29 % SZS status Theorem for theBenchmark: Theorem is valid
% 139.78/33.29 % SZS output start CNFRefutation for theBenchmark
% 139.78/33.29 fof(f2,axiom,(
% 139.78/33.29 c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_z) = c_Groups_Oone__class_Oone(tc_RealDef_Oreal) ),
% 139.78/33.29 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 139.78/33.29 fof(f3,axiom,(
% 139.78/33.29 v_z = c_Complex_Ocomplex_OComplex(v_x____,v_y____) ),
% 139.78/33.29 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 139.78/33.29 fof(f25,axiom,(
% 139.78/33.29 c_Groups_Oone__class_Oone(tc_Int_Oint) = c_Int_Onumber__class_Onumber__of(tc_Int_Oint,c_Int_OBit1(c_Int_OPls)) ),
% 139.78/33.29 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 139.78/33.29 fof(f28,axiom,(
% 139.78/33.29 c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_Groups_Oone__class_Oone(tc_Nat_Onat),c_Groups_Oone__class_Oone(tc_Nat_Onat)) = c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Int_OBit0(c_Int_OBit1(c_Int_OPls))) ),
% 139.78/33.29 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 139.78/33.29 fof(f53,axiom,(
% 139.78/33.29 (! [V_y,V_x] : c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Complex_Ocomplex_OComplex(V_x,V_y)) = c_NthRoot_Osqrt(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,hAPP(hAPP(c_Power_Opower__class_Opower(tc_RealDef_Oreal),V_x),c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))),hAPP(hAPP(c_Power_Opower__class_Opower(tc_RealDef_Oreal),V_y),c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))))) )),
% 139.78/33.29 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 139.78/33.29 fof(f57,axiom,(
% 139.78/33.29 (! [V_k] : c_Int_Onumber__class_Onumber__of(tc_Int_Oint,V_k) = V_k )),
% 139.78/33.29 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 139.78/33.29 fof(f203,axiom,(
% 139.78/33.29 (! [V_xa_2] :( c_NthRoot_Osqrt(V_xa_2) = c_Groups_Oone__class_Oone(tc_RealDef_Oreal)<=> V_xa_2 = c_Groups_Oone__class_Oone(tc_RealDef_Oreal) ) )),
% 139.78/33.29 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 139.78/33.29 fof(f497,axiom,(
% 139.78/33.29 (! [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) )),
% 139.78/33.29 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 139.78/33.29 fof(f1231,conjecture,(
% 139.78/33.29 c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,hAPP(hAPP(c_Power_Opower__class_Opower(tc_RealDef_Oreal),v_x____),c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))),hAPP(hAPP(c_Power_Opower__class_Opower(tc_RealDef_Oreal),v_y____),c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Int_OBit0(c_Int_OBit1(c_Int_OPls))))) = c_Groups_Oone__class_Oone(tc_RealDef_Oreal) ),
% 139.78/33.29 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 139.78/33.29 fof(f1232,negated_conjecture,(
% 139.78/33.29 ~(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,hAPP(hAPP(c_Power_Opower__class_Opower(tc_RealDef_Oreal),v_x____),c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))),hAPP(hAPP(c_Power_Opower__class_Opower(tc_RealDef_Oreal),v_y____),c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Int_OBit0(c_Int_OBit1(c_Int_OPls))))) = c_Groups_Oone__class_Oone(tc_RealDef_Oreal) )),
% 139.78/33.29 inference(negated_conjecture,[status(cth)],[f1231])).
% 139.78/33.29 fof(f1236,plain,(
% 139.78/33.29 c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_z)=c_Groups_Oone__class_Oone(tc_RealDef_Oreal)),
% 139.78/33.29 inference(cnf_transformation,[status(thm)],[f2])).
% 139.78/33.29 fof(f1237,plain,(
% 139.78/33.29 v_z=c_Complex_Ocomplex_OComplex(v_x____,v_y____)),
% 139.78/33.29 inference(cnf_transformation,[status(thm)],[f3])).
% 139.78/33.29 fof(f1279,plain,(
% 139.78/33.29 c_Groups_Oone__class_Oone(tc_Int_Oint)=c_Int_Onumber__class_Onumber__of(tc_Int_Oint,c_Int_OBit1(c_Int_OPls))),
% 139.78/33.29 inference(cnf_transformation,[status(thm)],[f25])).
% 139.78/33.29 fof(f1282,plain,(
% 139.78/33.29 c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_Groups_Oone__class_Oone(tc_Nat_Onat),c_Groups_Oone__class_Oone(tc_Nat_Onat))=c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))),
% 139.78/33.29 inference(cnf_transformation,[status(thm)],[f28])).
% 139.78/33.29 fof(f1348,plain,(
% 139.78/33.29 ![X0,X1]: (c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Complex_Ocomplex_OComplex(X0,X1))=c_NthRoot_Osqrt(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,hAPP(hAPP(c_Power_Opower__class_Opower(tc_RealDef_Oreal),X0),c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))),hAPP(hAPP(c_Power_Opower__class_Opower(tc_RealDef_Oreal),X1),c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))))))),
% 139.78/33.29 inference(cnf_transformation,[status(thm)],[f53])).
% 139.78/33.29 fof(f1353,plain,(
% 139.78/33.29 ![X0]: (c_Int_Onumber__class_Onumber__of(tc_Int_Oint,X0)=X0)),
% 139.78/33.29 inference(cnf_transformation,[status(thm)],[f57])).
% 139.78/33.29 fof(f1743,plain,(
% 139.78/33.29 ![V_xa_2]: ((~c_NthRoot_Osqrt(V_xa_2)=c_Groups_Oone__class_Oone(tc_RealDef_Oreal)|V_xa_2=c_Groups_Oone__class_Oone(tc_RealDef_Oreal))&(c_NthRoot_Osqrt(V_xa_2)=c_Groups_Oone__class_Oone(tc_RealDef_Oreal)|~V_xa_2=c_Groups_Oone__class_Oone(tc_RealDef_Oreal)))),
% 139.78/33.29 inference(NNF_transformation,[status(thm)],[f203])).
% 139.78/33.29 fof(f1744,plain,(
% 139.78/33.29 (![V_xa_2]: (~c_NthRoot_Osqrt(V_xa_2)=c_Groups_Oone__class_Oone(tc_RealDef_Oreal)|V_xa_2=c_Groups_Oone__class_Oone(tc_RealDef_Oreal)))&(![V_xa_2]: (c_NthRoot_Osqrt(V_xa_2)=c_Groups_Oone__class_Oone(tc_RealDef_Oreal)|~V_xa_2=c_Groups_Oone__class_Oone(tc_RealDef_Oreal)))),
% 139.78/33.29 inference(miniscoping,[status(thm)],[f1743])).
% 139.78/33.29 fof(f1745,plain,(
% 139.78/33.29 ![X0]: (~c_NthRoot_Osqrt(X0)=c_Groups_Oone__class_Oone(tc_RealDef_Oreal)|X0=c_Groups_Oone__class_Oone(tc_RealDef_Oreal))),
% 139.78/33.29 inference(cnf_transformation,[status(thm)],[f1744])).
% 139.78/33.29 fof(f2660,plain,(
% 139.78/33.29 ![X0]: (c_Nat_OSuc(X0)=c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_Groups_Oone__class_Oone(tc_Nat_Onat),X0))),
% 139.78/33.29 inference(cnf_transformation,[status(thm)],[f497])).
% 139.78/33.29 fof(f4654,plain,(
% 139.78/33.29 ~c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,hAPP(hAPP(c_Power_Opower__class_Opower(tc_RealDef_Oreal),v_x____),c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))),hAPP(hAPP(c_Power_Opower__class_Opower(tc_RealDef_Oreal),v_y____),c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))))=c_Groups_Oone__class_Oone(tc_RealDef_Oreal)),
% 139.78/33.29 inference(cnf_transformation,[status(thm)],[f1232])).
% 139.78/33.29 fof(f5056,plain,(
% 139.78/33.29 ~c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,hAPP(hAPP(c_Power_Opower__class_Opower(tc_RealDef_Oreal),v_x____),c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))),hAPP(hAPP(c_Power_Opower__class_Opower(tc_RealDef_Oreal),v_y____),c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Int_OBit0(c_Groups_Oone__class_Oone(tc_Int_Oint)))))=c_Groups_Oone__class_Oone(tc_RealDef_Oreal)),
% 139.78/33.29 inference(backward_demodulation,[status(thm)],[f5057,f4654])).
% 139.78/33.29 fof(f5057,plain,(
% 139.78/33.29 c_Groups_Oone__class_Oone(tc_Int_Oint)=c_Int_OBit1(c_Int_OPls)),
% 139.78/33.29 inference(forward_demodulation,[status(thm)],[f1353,f1279])).
% 139.78/33.29 fof(f5059,plain,(
% 139.78/33.29 ~c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,hAPP(hAPP(c_Power_Opower__class_Opower(tc_RealDef_Oreal),v_x____),c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Int_OBit0(c_Groups_Oone__class_Oone(tc_Int_Oint)))),hAPP(hAPP(c_Power_Opower__class_Opower(tc_RealDef_Oreal),v_y____),c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Int_OBit0(c_Groups_Oone__class_Oone(tc_Int_Oint)))))=c_Groups_Oone__class_Oone(tc_RealDef_Oreal)),
% 139.78/33.29 inference(forward_demodulation,[status(thm)],[f5057,f5056])).
% 139.78/33.29 fof(f5082,plain,(
% 139.78/33.29 c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_Groups_Oone__class_Oone(tc_Nat_Onat),c_Groups_Oone__class_Oone(tc_Nat_Onat))=c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Int_OBit0(c_Groups_Oone__class_Oone(tc_Int_Oint)))),
% 139.78/33.29 inference(forward_demodulation,[status(thm)],[f5057,f1282])).
% 139.78/33.29 fof(f5234,plain,(
% 139.78/33.29 ![X0,X1]: (c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Complex_Ocomplex_OComplex(X0,X1))=c_NthRoot_Osqrt(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,hAPP(hAPP(c_Power_Opower__class_Opower(tc_RealDef_Oreal),X0),c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Int_OBit0(c_Groups_Oone__class_Oone(tc_Int_Oint)))),hAPP(hAPP(c_Power_Opower__class_Opower(tc_RealDef_Oreal),X1),c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))))))),
% 139.78/33.29 inference(forward_demodulation,[status(thm)],[f5057,f1348])).
% 139.78/33.29 fof(f5235,plain,(
% 139.78/33.29 ![X0,X1]: (c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Complex_Ocomplex_OComplex(X0,X1))=c_NthRoot_Osqrt(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,hAPP(hAPP(c_Power_Opower__class_Opower(tc_RealDef_Oreal),X0),c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Int_OBit0(c_Groups_Oone__class_Oone(tc_Int_Oint)))),hAPP(hAPP(c_Power_Opower__class_Opower(tc_RealDef_Oreal),X1),c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Int_OBit0(c_Groups_Oone__class_Oone(tc_Int_Oint)))))))),
% 139.78/33.29 inference(forward_demodulation,[status(thm)],[f5057,f5234])).
% 139.78/33.29 fof(f6863,plain,(
% 139.78/33.29 ![X0,X1]: (~c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Complex_Ocomplex_OComplex(X0,X1))=c_Groups_Oone__class_Oone(tc_RealDef_Oreal)|c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,hAPP(hAPP(c_Power_Opower__class_Opower(tc_RealDef_Oreal),X0),c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Int_OBit0(c_Groups_Oone__class_Oone(tc_Int_Oint)))),hAPP(hAPP(c_Power_Opower__class_Opower(tc_RealDef_Oreal),X1),c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Int_OBit0(c_Groups_Oone__class_Oone(tc_Int_Oint)))))=c_Groups_Oone__class_Oone(tc_RealDef_Oreal))),
% 139.78/33.29 inference(paramodulation,[status(thm)],[f5235,f1745])).
% 139.78/33.29 fof(f23732,plain,(
% 139.78/33.29 c_Nat_OSuc(c_Groups_Oone__class_Oone(tc_Nat_Onat))=c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Int_OBit0(c_Groups_Oone__class_Oone(tc_Int_Oint)))),
% 139.78/33.29 inference(backward_demodulation,[status(thm)],[f2660,f5082])).
% 139.78/33.29 fof(f24251,plain,(
% 139.78/33.29 ~c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,hAPP(hAPP(c_Power_Opower__class_Opower(tc_RealDef_Oreal),v_x____),c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Int_OBit0(c_Groups_Oone__class_Oone(tc_Int_Oint)))),hAPP(hAPP(c_Power_Opower__class_Opower(tc_RealDef_Oreal),v_y____),c_Nat_OSuc(c_Groups_Oone__class_Oone(tc_Nat_Onat))))=c_Groups_Oone__class_Oone(tc_RealDef_Oreal)),
% 139.78/33.29 inference(backward_demodulation,[status(thm)],[f23732,f5059])).
% 139.78/33.29 fof(f24309,plain,(
% 139.78/33.29 ~c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,hAPP(hAPP(c_Power_Opower__class_Opower(tc_RealDef_Oreal),v_x____),c_Nat_OSuc(c_Groups_Oone__class_Oone(tc_Nat_Onat))),hAPP(hAPP(c_Power_Opower__class_Opower(tc_RealDef_Oreal),v_y____),c_Nat_OSuc(c_Groups_Oone__class_Oone(tc_Nat_Onat))))=c_Groups_Oone__class_Oone(tc_RealDef_Oreal)),
% 139.78/33.29 inference(forward_demodulation,[status(thm)],[f23732,f24251])).
% 139.78/33.29 fof(f56762,plain,(
% 139.78/33.29 ![X0,X1]: (~c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Complex_Ocomplex_OComplex(X0,X1))=c_Groups_Oone__class_Oone(tc_RealDef_Oreal)|c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,hAPP(hAPP(c_Power_Opower__class_Opower(tc_RealDef_Oreal),X0),c_Nat_OSuc(c_Groups_Oone__class_Oone(tc_Nat_Onat))),hAPP(hAPP(c_Power_Opower__class_Opower(tc_RealDef_Oreal),X1),c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Int_OBit0(c_Groups_Oone__class_Oone(tc_Int_Oint)))))=c_Groups_Oone__class_Oone(tc_RealDef_Oreal))),
% 139.78/33.29 inference(forward_demodulation,[status(thm)],[f23732,f6863])).
% 139.78/33.29 fof(f56763,plain,(
% 139.78/33.29 ![X0,X1]: (~c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Complex_Ocomplex_OComplex(X0,X1))=c_Groups_Oone__class_Oone(tc_RealDef_Oreal)|c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,hAPP(hAPP(c_Power_Opower__class_Opower(tc_RealDef_Oreal),X0),c_Nat_OSuc(c_Groups_Oone__class_Oone(tc_Nat_Onat))),hAPP(hAPP(c_Power_Opower__class_Opower(tc_RealDef_Oreal),X1),c_Nat_OSuc(c_Groups_Oone__class_Oone(tc_Nat_Onat))))=c_Groups_Oone__class_Oone(tc_RealDef_Oreal))),
% 139.78/33.29 inference(forward_demodulation,[status(thm)],[f23732,f56762])).
% 139.78/33.29 fof(f56770,plain,(
% 139.78/33.29 ~c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_z)=c_Groups_Oone__class_Oone(tc_RealDef_Oreal)|c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,hAPP(hAPP(c_Power_Opower__class_Opower(tc_RealDef_Oreal),v_x____),c_Nat_OSuc(c_Groups_Oone__class_Oone(tc_Nat_Onat))),hAPP(hAPP(c_Power_Opower__class_Opower(tc_RealDef_Oreal),v_y____),c_Nat_OSuc(c_Groups_Oone__class_Oone(tc_Nat_Onat))))=c_Groups_Oone__class_Oone(tc_RealDef_Oreal)),
% 139.78/33.29 inference(paramodulation,[status(thm)],[f1237,f56763])).
% 139.78/33.29 fof(f56774,plain,(
% 139.78/33.29 ~c_Groups_Oone__class_Oone(tc_RealDef_Oreal)=c_Groups_Oone__class_Oone(tc_RealDef_Oreal)|c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,hAPP(hAPP(c_Power_Opower__class_Opower(tc_RealDef_Oreal),v_x____),c_Nat_OSuc(c_Groups_Oone__class_Oone(tc_Nat_Onat))),hAPP(hAPP(c_Power_Opower__class_Opower(tc_RealDef_Oreal),v_y____),c_Nat_OSuc(c_Groups_Oone__class_Oone(tc_Nat_Onat))))=c_Groups_Oone__class_Oone(tc_RealDef_Oreal)),
% 57.80/33.51 inference(forward_demodulation,[status(thm)],[f1236,f56770])).
% 57.80/33.51 fof(f56775,plain,(
% 57.80/33.51 c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,hAPP(hAPP(c_Power_Opower__class_Opower(tc_RealDef_Oreal),v_x____),c_Nat_OSuc(c_Groups_Oone__class_Oone(tc_Nat_Onat))),hAPP(hAPP(c_Power_Opower__class_Opower(tc_RealDef_Oreal),v_y____),c_Nat_OSuc(c_Groups_Oone__class_Oone(tc_Nat_Onat))))=c_Groups_Oone__class_Oone(tc_RealDef_Oreal)),
% 57.80/33.51 inference(trivial_equality_resolution,[status(thm)],[f56774])).
% 57.80/33.51 fof(f56776,plain,(
% 57.80/33.51 $false),
% 57.80/33.51 inference(forward_subsumption_resolution,[status(thm)],[f56775,f24309])).
% 57.80/33.51 % SZS output end CNFRefutation for theBenchmark.p
% 57.80/33.51 % Elapsed time: 18.072548 seconds
% 57.80/33.51 % CPU time: 141.467838 seconds
% 57.80/33.51 % Total memory used: 1.007 GB
% 57.80/33.51 % Net memory used: 969.652 MB
%------------------------------------------------------------------------------