%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWW212+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 : n007.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 62.04s 13.51s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SWW212+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.19/5.46 % Computer : n007.cluster.edu
% 0.19/5.46 % Model : x86_64 x86_64
% 0.19/5.46 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.19/5.46 % Memory : 8046.5625MB
% 0.19/5.46 % OS : Linux 6.8.0-71-generic
% 0.19/5.46 % CPULimit : 300
% 0.19/5.46 % WCLimit : 300
% 0.19/5.46 % DateTime : Mon Sep 21 09:38:56 UTC 2026
% 0.19/5.46 % CPUTime :
% 0.22/5.55 % Drodi V4.1.1
% 62.04/13.51 % Refutation found
% 62.04/13.51 % SZS status Theorem for theBenchmark: Theorem is valid
% 62.04/13.51 % SZS output start CNFRefutation for theBenchmark
% 62.04/13.51 fof(f17,axiom,(
% 62.04/13.51 c_SEQ_Osubseq(c_Fun_Ocomp(tc_Nat_Onat,tc_Nat_Onat,tc_Nat_Onat,v_f____,v_ga____)) ),
% 62.04/13.51 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 62.04/13.51 fof(f94,axiom,(
% 62.04/13.51 (! [V_e_2] :( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),V_e_2)=> (? [B_N] :(! [B_n] :( c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,B_N,B_n)=> c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,hAPP(c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex),hAPP(hAPP(c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex),hAPP(v_s,hAPP(c_Fun_Ocomp(tc_Nat_Onat,tc_Nat_Onat,tc_Nat_Onat,v_f____,v_ga____),B_n))),hAPP(hAPP(c_Complex_Ocomplex_OComplex,v_x____),v_y____))),V_e_2) ) ))) )),
% 62.04/13.51 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 62.04/13.51 fof(f1274,conjecture,(
% 62.04/13.51 (? [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] :( c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,B_N,B_n)=> c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,hAPP(c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex),hAPP(hAPP(c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex),hAPP(v_s,hAPP(B_f,B_n))),B_z)),B_e) ) ))) ))) )),
% 62.04/13.51 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 62.04/13.51 fof(f1275,negated_conjecture,(
% 62.04/13.51 ~((? [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] :( c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,B_N,B_n)=> c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,hAPP(c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex),hAPP(hAPP(c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex),hAPP(v_s,hAPP(B_f,B_n))),B_z)),B_e) ) ))) ))) ))),
% 62.04/13.51 inference(negated_conjecture,[status(cth)],[f1274])).
% 62.04/13.51 fof(f1327,plain,(
% 62.04/13.51 c_SEQ_Osubseq(c_Fun_Ocomp(tc_Nat_Onat,tc_Nat_Onat,tc_Nat_Onat,v_f____,v_ga____))),
% 62.04/13.51 inference(cnf_transformation,[status(thm)],[f17])).
% 62.04/13.51 fof(f1616,plain,(
% 62.04/13.51 ![V_e_2]: (~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),V_e_2)|(?[B_N]: ![B_n]: (~c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,B_N,B_n)|c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,hAPP(c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex),hAPP(hAPP(c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex),hAPP(v_s,hAPP(c_Fun_Ocomp(tc_Nat_Onat,tc_Nat_Onat,tc_Nat_Onat,v_f____,v_ga____),B_n))),hAPP(hAPP(c_Complex_Ocomplex_OComplex,v_x____),v_y____))),V_e_2))))),
% 62.04/13.51 inference(pre_NNF_transformation,[status(thm)],[f94])).
% 62.04/13.51 fof(f1617,plain,(
% 62.04/13.51 ![V_e_2]: (~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),V_e_2)|![B_n]: (~c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,sK10_skl(V_e_2),B_n)|c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,hAPP(c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex),hAPP(hAPP(c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex),hAPP(v_s,hAPP(c_Fun_Ocomp(tc_Nat_Onat,tc_Nat_Onat,tc_Nat_Onat,v_f____,v_ga____),B_n))),hAPP(hAPP(c_Complex_Ocomplex_OComplex,v_x____),v_y____))),V_e_2)))),
% 62.04/13.51 inference(skolemize,[status(esa),new_symbols(skolem,[sK10_skl]),skolemize(B_N,sK10_skl(V_e_2))],[f1616])).
% 62.04/13.51 fof(f1618,plain,(
% 62.04/13.51 ![X0,X1]: (~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),X0)|~c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,sK10_skl(X0),X1)|c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,hAPP(c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex),hAPP(hAPP(c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex),hAPP(v_s,hAPP(c_Fun_Ocomp(tc_Nat_Onat,tc_Nat_Onat,tc_Nat_Onat,v_f____,v_ga____),X1))),hAPP(hAPP(c_Complex_Ocomplex_OComplex,v_x____),v_y____))),X0))),
% 62.04/13.51 inference(cnf_transformation,[status(thm)],[f1617])).
% 62.04/13.51 fof(f4789,plain,(
% 62.04/13.51 (![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]: (c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,B_N,B_n)&~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,hAPP(c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex),hAPP(hAPP(c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex),hAPP(v_s,hAPP(B_f,B_n))),B_z)),B_e)))))))),
% 62.04/13.51 inference(pre_NNF_transformation,[status(thm)],[f1275])).
% 62.04/13.51 fof(f4790,plain,(
% 62.04/13.51 ![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),sK49_skl(B_z,B_f))&(![B_N]: (c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,B_N,sK50_skl(B_N,B_z,B_f))&~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,hAPP(c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex),hAPP(hAPP(c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex),hAPP(v_s,hAPP(B_f,sK50_skl(B_N,B_z,B_f)))),B_z)),sK49_skl(B_z,B_f)))))))),
% 62.04/13.51 inference(skolemize,[status(esa),new_symbols(skolem,[sK49_skl,sK50_skl]),skolemize(B_e,sK49_skl(B_z,B_f)),skolemize(B_n,sK50_skl(B_N,B_z,B_f))],[f4789])).
% 62.04/13.51 fof(f4791,plain,(
% 62.04/13.51 ![X0,X1]: (~c_SEQ_Osubseq(X0)|c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),sK49_skl(X1,X0)))),
% 62.04/13.51 inference(cnf_transformation,[status(thm)],[f4790])).
% 62.04/13.51 fof(f4792,plain,(
% 62.04/13.51 ![X0,X1,X2]: (~c_SEQ_Osubseq(X0)|c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,X1,sK50_skl(X1,X2,X0)))),
% 62.04/13.51 inference(cnf_transformation,[status(thm)],[f4790])).
% 62.04/13.51 fof(f4793,plain,(
% 62.04/13.51 ![X0,X1,X2]: (~c_SEQ_Osubseq(X0)|~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,hAPP(c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex),hAPP(hAPP(c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex),hAPP(v_s,hAPP(X0,sK50_skl(X1,X2,X0)))),X2)),sK49_skl(X2,X0)))),
% 62.04/13.51 inference(cnf_transformation,[status(thm)],[f4790])).
% 62.04/13.51 fof(f5265,plain,(
% 62.04/13.51 ![X0,X1]: (c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,X0,sK50_skl(X0,X1,c_Fun_Ocomp(tc_Nat_Onat,tc_Nat_Onat,tc_Nat_Onat,v_f____,v_ga____))))),
% 62.04/13.51 inference(resolution,[status(thm)],[f1327,f4792])).
% 62.04/13.51 fof(f10123,plain,(
% 62.04/13.51 ![X0]: (~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),sK49_skl(hAPP(hAPP(c_Complex_Ocomplex_OComplex,v_x____),v_y____),c_Fun_Ocomp(tc_Nat_Onat,tc_Nat_Onat,tc_Nat_Onat,v_f____,v_ga____)))|~c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,sK10_skl(sK49_skl(hAPP(hAPP(c_Complex_Ocomplex_OComplex,v_x____),v_y____),c_Fun_Ocomp(tc_Nat_Onat,tc_Nat_Onat,tc_Nat_Onat,v_f____,v_ga____))),sK50_skl(X0,hAPP(hAPP(c_Complex_Ocomplex_OComplex,v_x____),v_y____),c_Fun_Ocomp(tc_Nat_Onat,tc_Nat_Onat,tc_Nat_Onat,v_f____,v_ga____)))|~c_SEQ_Osubseq(c_Fun_Ocomp(tc_Nat_Onat,tc_Nat_Onat,tc_Nat_Onat,v_f____,v_ga____)))),
% 62.04/13.51 inference(resolution,[status(thm)],[f1618,f4793])).
% 62.04/13.51 fof(f10126,definition,(
% 62.04/13.51 sQ108_spl <=> (c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),sK49_skl(hAPP(hAPP(c_Complex_Ocomplex_OComplex,v_x____),v_y____),c_Fun_Ocomp(tc_Nat_Onat,tc_Nat_Onat,tc_Nat_Onat,v_f____,v_ga____))))),
% 62.04/13.51 introduced(definition,[new_symbols(definition,[sQ108_spl])],[split_symbol_definition])).
% 62.04/13.51 fof(f10128,plain,(
% 62.04/13.51 ~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),sK49_skl(hAPP(hAPP(c_Complex_Ocomplex_OComplex,v_x____),v_y____),c_Fun_Ocomp(tc_Nat_Onat,tc_Nat_Onat,tc_Nat_Onat,v_f____,v_ga____)))|sQ108_spl),
% 62.04/13.51 inference(component_clause,[status(thm)],[f10126])).
% 62.04/13.51 fof(f10129,definition,(
% 62.04/13.51 ![X0]: (sQ109_spl <=> (~c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,sK10_skl(sK49_skl(hAPP(hAPP(c_Complex_Ocomplex_OComplex,v_x____),v_y____),c_Fun_Ocomp(tc_Nat_Onat,tc_Nat_Onat,tc_Nat_Onat,v_f____,v_ga____))),sK50_skl(X0,hAPP(hAPP(c_Complex_Ocomplex_OComplex,v_x____),v_y____),c_Fun_Ocomp(tc_Nat_Onat,tc_Nat_Onat,tc_Nat_Onat,v_f____,v_ga____)))))),
% 62.04/13.51 introduced(definition,[new_symbols(definition,[sQ109_spl])],[split_symbol_definition])).
% 62.04/13.51 fof(f10130,plain,(
% 62.04/13.51 ![X0]: (~c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,sK10_skl(sK49_skl(hAPP(hAPP(c_Complex_Ocomplex_OComplex,v_x____),v_y____),c_Fun_Ocomp(tc_Nat_Onat,tc_Nat_Onat,tc_Nat_Onat,v_f____,v_ga____))),sK50_skl(X0,hAPP(hAPP(c_Complex_Ocomplex_OComplex,v_x____),v_y____),c_Fun_Ocomp(tc_Nat_Onat,tc_Nat_Onat,tc_Nat_Onat,v_f____,v_ga____)))|~sQ109_spl)),
% 62.85/13.59 inference(component_clause,[status(thm)],[f10129])).
% 62.85/13.59 fof(f10132,definition,(
% 62.85/13.59 sQ110_spl <=> (c_SEQ_Osubseq(c_Fun_Ocomp(tc_Nat_Onat,tc_Nat_Onat,tc_Nat_Onat,v_f____,v_ga____)))),
% 62.85/13.59 introduced(definition,[new_symbols(definition,[sQ110_spl])],[split_symbol_definition])).
% 62.85/13.59 fof(f10134,plain,(
% 62.85/13.59 ~c_SEQ_Osubseq(c_Fun_Ocomp(tc_Nat_Onat,tc_Nat_Onat,tc_Nat_Onat,v_f____,v_ga____))|sQ110_spl),
% 62.85/13.59 inference(component_clause,[status(thm)],[f10132])).
% 62.85/13.59 fof(f10135,plain,(
% 62.85/13.59 ~sQ108_spl|sQ109_spl|~sQ110_spl),
% 62.85/13.59 inference(split_clause,[status(thm)],[f10123,f10126,f10129,f10132])).
% 62.85/13.59 fof(f28189,plain,(
% 62.85/13.59 $false|sQ110_spl),
% 62.85/13.59 inference(forward_subsumption_resolution,[status(thm)],[f1327,f10134])).
% 62.85/13.59 fof(f28190,plain,(
% 62.85/13.59 sQ110_spl),
% 62.85/13.59 inference(contradiction_clause,[status(thm)],[f28189])).
% 62.85/13.59 fof(f28227,plain,(
% 62.85/13.59 ~c_SEQ_Osubseq(c_Fun_Ocomp(tc_Nat_Onat,tc_Nat_Onat,tc_Nat_Onat,v_f____,v_ga____))|sQ108_spl),
% 62.85/13.59 inference(resolution,[status(thm)],[f10128,f4791])).
% 62.85/13.59 fof(f28230,plain,(
% 62.85/13.59 ~sQ110_spl|sQ108_spl),
% 62.85/13.59 inference(split_clause,[status(thm)],[f28227,f10132,f10126])).
% 62.85/13.59 fof(f28376,plain,(
% 62.85/13.59 $false|~sQ109_spl),
% 62.85/13.59 inference(resolution,[status(thm)],[f10130,f5265])).
% 62.85/13.59 fof(f28381,plain,(
% 62.85/13.59 ~sQ109_spl),
% 62.85/13.59 inference(contradiction_clause,[status(thm)],[f28376])).
% 62.85/13.59 fof(f28382,plain,(
% 62.85/13.59 $false),
% 62.85/13.59 inference(sat_refutation,[status(thm)],[f10135,f28190,f28230,f28381])).
% 62.85/13.59 % SZS output end CNFRefutation for theBenchmark.p
% 15.31/13.64 % Elapsed time: 8.158108 seconds
% 15.31/13.64 % CPU time: 63.431908 seconds
% 15.31/13.64 % Total memory used: 599.947 MB
% 15.31/13.64 % Net memory used: 581.664 MB
%------------------------------------------------------------------------------