%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWW220+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 : 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:49 PM UTC 2026
% Result : Theorem 0.47s 1.01s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SWW220+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.17/0.42 % Computer : n026.cluster.edu
% 0.17/0.42 % Model : x86_64 x86_64
% 0.17/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.42 % Memory : 8046.5625MB
% 0.17/0.42 % OS : Linux 6.8.0-71-generic
% 0.17/0.42 % CPULimit : 300
% 0.17/0.42 % WCLimit : 300
% 0.17/0.42 % DateTime : Mon Sep 21 09:44:36 UTC 2026
% 0.17/0.43 % CPUTime :
% 0.24/0.60 % Drodi V4.1.1
% 0.47/1.01 % Refutation found
% 0.47/1.01 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.47/1.01 % SZS output start CNFRefutation for theBenchmark
% 0.47/1.01 fof(f3,axiom,(
% 0.47/1.01 (? [B_f] :( c_SEQ_Osubseq(B_f)& (? [B_z] :(! [B_e] :( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),B_e)=> (? [B_N] :(! [B_n] :( hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,B_N),B_n))=> c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_g____(hAPP(B_f,B_n)),B_z)),B_e) ) ))) ))) )),
% 0.47/1.01 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.47/1.01 fof(f1269,hypothesis,(
% 0.47/1.01 (! [B_f] :( c_SEQ_Osubseq(B_f)=> ( (? [B_z] :(! [B_e] :( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),B_e)=> (? [B_N] :(! [B_n] :( hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,B_N),B_n))=> c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_g____(hAPP(B_f,B_n)),B_z)),B_e) ) )))))=> v_thesis____ ) ) )),
% 0.47/1.01 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.47/1.01 fof(f1270,conjecture,(
% 0.47/1.01 v_thesis____ ),
% 0.47/1.01 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.47/1.01 fof(f1271,negated_conjecture,(
% 0.47/1.01 ~(v_thesis____ )),
% 0.47/1.01 inference(negated_conjecture,[status(cth)],[f1270])).
% 0.47/1.01 fof(f1280,plain,(
% 0.47/1.01 ?[B_f]: (c_SEQ_Osubseq(B_f)&(?[B_z]: ![B_e]: (~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),B_e)|(?[B_N]: ![B_n]: (~hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,B_N),B_n))|c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_g____(hAPP(B_f,B_n)),B_z)),B_e))))))),
% 0.47/1.01 inference(pre_NNF_transformation,[status(thm)],[f3])).
% 0.47/1.01 fof(f1281,plain,(
% 0.47/1.01 (c_SEQ_Osubseq(sK1_skl)&![B_e]: (~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),B_e)|![B_n]: (~hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,sK3_skl(B_e)),B_n))|c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_g____(hAPP(sK1_skl,B_n)),sK2_skl)),B_e))))),
% 0.47/1.01 inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl,sK2_skl,sK3_skl]),skolemize(B_f,sK1_skl),skolemize(B_z,sK2_skl),skolemize(B_N,sK3_skl(B_e))],[f1280])).
% 0.47/1.01 fof(f1282,plain,(
% 0.47/1.01 c_SEQ_Osubseq(sK1_skl)),
% 0.47/1.01 inference(cnf_transformation,[status(thm)],[f1281])).
% 0.47/1.01 fof(f1283,plain,(
% 0.47/1.01 ![X0,X1]: (~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),X0)|~hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,sK3_skl(X0)),X1))|c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_g____(hAPP(sK1_skl,X1)),sK2_skl)),X0))),
% 0.47/1.01 inference(cnf_transformation,[status(thm)],[f1281])).
% 0.47/1.01 fof(f4790,plain,(
% 0.47/1.01 ![B_f]: (~c_SEQ_Osubseq(B_f)|((![B_z]: ?[B_e]: (c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),B_e)&(![B_N]: ?[B_n]: (hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,B_N),B_n))&~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_g____(hAPP(B_f,B_n)),B_z)),B_e)))))|v_thesis____))),
% 0.47/1.01 inference(pre_NNF_transformation,[status(thm)],[f1269])).
% 0.47/1.01 fof(f4791,plain,(
% 0.47/1.01 ![B_f]: (~c_SEQ_Osubseq(B_f)|((![B_z]: (c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),sK78_skl(B_z,B_f))&(![B_N]: (hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,B_N),sK79_skl(B_N,B_z,B_f)))&~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_g____(hAPP(B_f,sK79_skl(B_N,B_z,B_f))),B_z)),sK78_skl(B_z,B_f))))))|v_thesis____))),
% 0.47/1.01 inference(skolemize,[status(esa),new_symbols(skolem,[sK78_skl,sK79_skl]),skolemize(B_e,sK78_skl(B_z,B_f)),skolemize(B_n,sK79_skl(B_N,B_z,B_f))],[f4790])).
% 0.47/1.04 fof(f4792,plain,(
% 0.47/1.04 ![X0,X1]: (~c_SEQ_Osubseq(X0)|c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),sK78_skl(X1,X0))|v_thesis____)),
% 0.47/1.04 inference(cnf_transformation,[status(thm)],[f4791])).
% 0.47/1.04 fof(f4793,plain,(
% 0.47/1.04 ![X0,X1,X2]: (~c_SEQ_Osubseq(X0)|hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,X1),sK79_skl(X1,X2,X0)))|v_thesis____)),
% 0.47/1.04 inference(cnf_transformation,[status(thm)],[f4791])).
% 0.47/1.04 fof(f4794,plain,(
% 0.47/1.04 ![X0,X1,X2]: (~c_SEQ_Osubseq(X0)|~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_g____(hAPP(X0,sK79_skl(X1,X2,X0))),X2)),sK78_skl(X2,X0))|v_thesis____)),
% 0.47/1.04 inference(cnf_transformation,[status(thm)],[f4791])).
% 0.47/1.04 fof(f4795,plain,(
% 0.47/1.04 ~v_thesis____),
% 0.47/1.04 inference(cnf_transformation,[status(thm)],[f1271])).
% 0.47/1.04 fof(f5191,plain,(
% 0.47/1.04 ![X0,X1,X2]: (~c_SEQ_Osubseq(X0)|~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_g____(hAPP(X0,sK79_skl(X1,X2,X0))),X2)),sK78_skl(X2,X0)))),
% 0.47/1.04 inference(backward_subsumption_resolution,[status(thm)],[f4794,f4795])).
% 0.47/1.04 fof(f5192,plain,(
% 0.47/1.04 ![X0,X1,X2]: (~c_SEQ_Osubseq(X0)|hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,X1),sK79_skl(X1,X2,X0))))),
% 0.47/1.04 inference(backward_subsumption_resolution,[status(thm)],[f4793,f4795])).
% 0.47/1.04 fof(f5193,plain,(
% 0.47/1.04 ![X0,X1]: (~c_SEQ_Osubseq(X0)|c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),sK78_skl(X1,X0)))),
% 0.47/1.04 inference(backward_subsumption_resolution,[status(thm)],[f4792,f4795])).
% 0.47/1.04 fof(f5217,plain,(
% 0.47/1.04 ![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(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_g____(hAPP(sK1_skl,sK79_skl(sK3_skl(X0),X1,X2))),sK2_skl)),X0)|~c_SEQ_Osubseq(X2))),
% 0.47/1.04 inference(resolution,[status(thm)],[f1283,f5192])).
% 0.47/1.04 fof(f5218,plain,(
% 0.47/1.04 ![X0,X1,X2,X3]: (c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_g____(hAPP(sK1_skl,sK79_skl(sK3_skl(sK78_skl(X0,X1)),X2,X3))),sK2_skl)),sK78_skl(X0,X1))|~c_SEQ_Osubseq(X3)|~c_SEQ_Osubseq(X1))),
% 0.47/1.04 inference(resolution,[status(thm)],[f5217,f5193])).
% 0.47/1.04 fof(f5219,plain,(
% 0.47/1.04 ~c_SEQ_Osubseq(sK1_skl)|~c_SEQ_Osubseq(sK1_skl)|~c_SEQ_Osubseq(sK1_skl)),
% 0.47/1.04 inference(resolution,[status(thm)],[f5218,f5191])).
% 0.47/1.04 fof(f5220,plain,(
% 0.47/1.04 ~c_SEQ_Osubseq(sK1_skl)),
% 0.47/1.04 inference(duplicate_literals_removal,[status(thm)],[f5219])).
% 0.47/1.04 fof(f5221,plain,(
% 0.47/1.04 $false),
% 0.47/1.04 inference(forward_subsumption_resolution,[status(thm)],[f5220,f1282])).
% 0.47/1.04 % SZS output end CNFRefutation for theBenchmark.p
% 0.47/1.07 % Elapsed time: 0.628754 seconds
% 0.47/1.07 % CPU time: 3.496392 seconds
% 0.47/1.07 % Total memory used: 238.981 MB
% 0.47/1.07 % Net memory used: 237.198 MB
%------------------------------------------------------------------------------