%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWW217+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 : 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 03:08:49 PM UTC 2026
% Result : Theorem 0.40s 0.93s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SWW217+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.05 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.16/0.43 % Computer : n020.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:42:47 UTC 2026
% 0.16/0.43 % CPUTime :
% 0.29/0.63 % Drodi V4.1.1
% 0.40/0.93 % Refutation found
% 0.40/0.93 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.40/0.93 % SZS output start CNFRefutation for theBenchmark
% 0.40/0.93 fof(f5,axiom,(
% 0.40/0.93 c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),v_da____),v_m____),v_e) ),
% 0.40/0.93 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.40/0.93 fof(f8,axiom,(
% 0.40/0.93 c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_w____,v_z))),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_cs____),c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_w____,v_z)))),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),v_da____),v_m____)) ),
% 0.40/0.93 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.40/0.93 fof(f120,axiom,(
% 0.40/0.93 (! [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.40/0.93 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.40/0.93 fof(f121,axiom,(
% 0.40/0.93 (! [V_k,V_j,V_i] :( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_i,V_j)=> ( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_j,V_k)=> c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_i,V_k) ) ) )),
% 0.40/0.93 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.40/0.93 fof(f122,axiom,(
% 0.40/0.93 (! [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) ) )),
% 0.40/0.93 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.40/0.93 fof(f132,axiom,(
% 0.40/0.93 (! [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.40/0.93 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.40/0.93 fof(f1260,conjecture,(
% 0.40/0.93 c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_w____,v_z))),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_cs____),c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_w____,v_z)))),v_e) ),
% 0.40/0.93 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.40/0.93 fof(f1261,negated_conjecture,(
% 0.40/0.93 ~(c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_w____,v_z))),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_cs____),c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_w____,v_z)))),v_e) )),
% 0.40/0.93 inference(negated_conjecture,[status(cth)],[f1260])).
% 0.40/0.93 fof(f1268,plain,(
% 0.40/0.93 c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),v_da____),v_m____),v_e)),
% 0.40/0.93 inference(cnf_transformation,[status(thm)],[f5])).
% 0.40/0.93 fof(f1276,plain,(
% 0.40/0.93 c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_w____,v_z))),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_cs____),c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_w____,v_z)))),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),v_da____),v_m____))),
% 0.40/0.93 inference(cnf_transformation,[status(thm)],[f8])).
% 0.40/0.93 fof(f1599,plain,(
% 0.40/0.93 ![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.40/0.93 inference(pre_NNF_transformation,[status(thm)],[f120])).
% 0.40/0.93 fof(f1600,plain,(
% 0.40/0.93 ![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)),
% 0.40/0.93 inference(cnf_transformation,[status(thm)],[f1599])).
% 0.40/0.93 fof(f1601,plain,(
% 0.40/0.93 ![V_k,V_j,V_i]: (~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_i,V_j)|(~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_j,V_k)|c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_i,V_k)))),
% 0.40/0.93 inference(pre_NNF_transformation,[status(thm)],[f121])).
% 0.40/0.93 fof(f1602,plain,(
% 0.40/0.93 ![V_j,V_i]: (~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_i,V_j)|(![V_k]: (~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_j,V_k)|c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_i,V_k))))),
% 0.40/0.93 inference(miniscoping,[status(thm)],[f1601])).
% 0.40/0.93 fof(f1603,plain,(
% 0.40/0.93 ![X0,X1,X2]: (~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X0,X1)|~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X1,X2)|c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X0,X2))),
% 0.40/0.93 inference(cnf_transformation,[status(thm)],[f1602])).
% 0.40/0.93 fof(f1604,plain,(
% 0.40/0.93 ![X0,X1]: (c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X0,X1)|c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X1,X0))),
% 0.40/0.93 inference(cnf_transformation,[status(thm)],[f122])).
% 0.40/0.93 fof(f1630,plain,(
% 0.40/0.93 ![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)))),
% 0.40/0.93 inference(NNF_transformation,[status(thm)],[f132])).
% 0.40/0.93 fof(f1631,plain,(
% 0.40/0.93 (![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)))),
% 0.40/0.93 inference(miniscoping,[status(thm)],[f1630])).
% 0.40/0.93 fof(f1632,plain,(
% 0.40/0.93 ![X0,X1]: (~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X0,X1)|c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X0,X1))),
% 0.40/0.93 inference(cnf_transformation,[status(thm)],[f1631])).
% 0.40/0.93 fof(f1633,plain,(
% 0.40/0.93 ![X0,X1]: (~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X0,X1)|~X0=X1)),
% 0.40/0.93 inference(cnf_transformation,[status(thm)],[f1631])).
% 0.40/0.93 fof(f1634,plain,(
% 0.40/0.93 ![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)),
% 0.40/0.93 inference(cnf_transformation,[status(thm)],[f1631])).
% 0.40/0.93 fof(f4748,plain,(
% 0.40/0.93 ~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_w____,v_z))),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_cs____),c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_w____,v_z)))),v_e)),
% 0.40/0.93 inference(cnf_transformation,[status(thm)],[f1261])).
% 0.40/0.93 fof(f4836,plain,(
% 0.40/0.93 ![X0]: (~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X0,X0))),
% 0.40/0.93 inference(destructive_equality_resolution,[status(thm)],[f1633])).
% 0.40/0.93 fof(f4972,plain,(
% 0.40/0.93 c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),v_da____),v_m____),v_e)),
% 0.40/0.93 inference(resolution,[status(thm)],[f1632,f1268])).
% 0.40/0.93 fof(f5029,plain,(
% 0.40/0.93 ![X0,X1]: (c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X0,X1)|X0=X1|c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X1,X0))),
% 0.40/0.93 inference(resolution,[status(thm)],[f1634,f1604])).
% 0.40/0.93 fof(f5050,plain,(
% 0.40/0.93 hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_w____,v_z))),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_cs____),c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_w____,v_z))))=v_e|c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,v_e,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_w____,v_z))),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_cs____),c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_w____,v_z)))))),
% 0.40/0.93 inference(resolution,[status(thm)],[f5029,f4748])).
% 0.40/0.93 fof(f5064,plain,(
% 0.40/0.93 hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_w____,v_z))),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_cs____),c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_w____,v_z))))=v_e|~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_w____,v_z))),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_cs____),c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_w____,v_z)))),v_e)|hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_w____,v_z))),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_cs____),c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_w____,v_z))))=v_e),
% 0.40/0.93 inference(resolution,[status(thm)],[f5050,f1600])).
% 0.40/0.93 fof(f5066,plain,(
% 0.40/0.93 hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_w____,v_z))),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_cs____),c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_w____,v_z))))=v_e|~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_w____,v_z))),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_cs____),c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_w____,v_z)))),v_e)),
% 0.40/0.93 inference(duplicate_literals_removal,[status(thm)],[f5064])).
% 0.40/0.93 fof(f5082,plain,(
% 0.40/0.93 ![X0]: (~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_w____,v_z))),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_cs____),c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_w____,v_z)))),X0)|~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X0,v_e)|hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_w____,v_z))),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_cs____),c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_w____,v_z))))=v_e)),
% 0.40/0.93 inference(resolution,[status(thm)],[f1603,f5066])).
% 0.40/0.93 fof(f5188,plain,(
% 0.40/0.93 ~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),v_da____),v_m____),v_e)|hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_w____,v_z))),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_cs____),c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_w____,v_z))))=v_e),
% 0.40/0.93 inference(resolution,[status(thm)],[f5082,f1276])).
% 0.40/0.93 fof(f5960,plain,(
% 0.40/0.93 hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_w____,v_z))),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_cs____),c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_w____,v_z))))=v_e),
% 0.40/0.93 inference(backward_subsumption_resolution,[status(thm)],[f5188,f4972])).
% 0.40/0.93 fof(f6080,plain,(
% 0.40/0.93 c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,v_e,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),v_da____),v_m____))),
% 0.40/0.95 inference(backward_demodulation,[status(thm)],[f5960,f1276])).
% 0.40/0.95 fof(f6098,plain,(
% 0.40/0.95 ~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),v_da____),v_m____),v_e)|hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),v_da____),v_m____)=v_e),
% 0.40/0.95 inference(resolution,[status(thm)],[f6080,f1600])).
% 0.40/0.95 fof(f6101,plain,(
% 0.40/0.95 hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),v_da____),v_m____)=v_e),
% 0.40/0.95 inference(forward_subsumption_resolution,[status(thm)],[f6098,f4972])).
% 0.40/0.95 fof(f6104,plain,(
% 0.40/0.95 c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,v_e,v_e)),
% 0.40/0.95 inference(backward_demodulation,[status(thm)],[f6101,f1268])).
% 0.40/0.95 fof(f6120,plain,(
% 0.40/0.95 $false),
% 0.40/0.95 inference(forward_subsumption_resolution,[status(thm)],[f6104,f4836])).
% 0.40/0.95 % SZS output end CNFRefutation for theBenchmark.p
% 0.84/1.00 % Elapsed time: 0.545921 seconds
% 0.84/1.00 % CPU time: 2.497632 seconds
% 0.84/1.00 % Total memory used: 226.041 MB
% 0.84/1.00 % Net memory used: 224.039 MB
%------------------------------------------------------------------------------