%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWW262+1 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -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:07:32 PM UTC 2026
% Result : Theorem 125.51s 16.36s
% Output : CNFRefutation 97.17s
% Verified :
% SZS Type : Refutation
% Derivation depth : 6
% Number of leaves : 10
% Syntax : Number of formulae : 36 ( 13 unt; 4 def)
% Number of atoms : 69 ( 0 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 59 ( 26 ~; 25 |; 0 &)
% ( 4 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 3 avg)
% Maximal term depth : 8 ( 2 avg)
% Number of predicates : 7 ( 6 usr; 5 prp; 0-3 aty)
% Number of functors : 14 ( 14 usr; 7 con; 0-3 aty)
% Number of variables : 24 ( 24 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f4,axiom,
c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),v_t____),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____)),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f6,axiom,
c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),v_t____),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f60,axiom,
! [V_n,V_a,T_a] :
( class_Rings_Olinordered__semidom(T_a)
=> ( c_Orderings_Oord__class_Oless(T_a,c_Groups_Ozero__class_Ozero(T_a),V_a)
=> c_Orderings_Oord__class_Oless(T_a,c_Groups_Ozero__class_Ozero(T_a),hAPP(hAPP(c_Power_Opower__class_Opower(T_a),V_a),V_n)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f296,axiom,
! [V_y,V_x,V_z] :
( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),V_z)
=> ( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,V_x,V_y)
=> c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),V_z),V_x),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),V_z),V_y)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1142,axiom,
class_Rings_Olinordered__semidom(tc_RealDef_Oreal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1288,conjecture,
c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),hAPP(hAPP(c_Power_Opower__class_Opower(tc_RealDef_Oreal),v_t____),v_k____)),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),v_t____),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____))),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),hAPP(hAPP(c_Power_Opower__class_Opower(tc_RealDef_Oreal),v_t____),v_k____)),c_Groups_Oone__class_Oone(tc_RealDef_Oreal))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1289,negated_conjecture,
~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),hAPP(hAPP(c_Power_Opower__class_Opower(tc_RealDef_Oreal),v_t____),v_k____)),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),v_t____),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____))),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),hAPP(hAPP(c_Power_Opower__class_Opower(tc_RealDef_Oreal),v_t____),v_k____)),c_Groups_Oone__class_Oone(tc_RealDef_Oreal))),
inference(negated_conjecture,[status(cth)],[f1288]) ).
fof(f1295,plain,
c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),v_t____),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____)),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f1297,plain,
c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),v_t____),
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f1465,plain,
! [V_n,V_a,T_a] :
( c_Orderings_Oord__class_Oless(T_a,c_Groups_Ozero__class_Ozero(T_a),hAPP(hAPP(c_Power_Opower__class_Opower(T_a),V_a),V_n))
| ~ c_Orderings_Oord__class_Oless(T_a,c_Groups_Ozero__class_Ozero(T_a),V_a)
| ~ class_Rings_Olinordered__semidom(T_a) ),
inference(pre_NNF_transformation,[status(thm)],[f60]) ).
fof(f1466,plain,
! [T_a] :
( ! [V_a] :
( ! [V_n] : c_Orderings_Oord__class_Oless(T_a,c_Groups_Ozero__class_Ozero(T_a),hAPP(hAPP(c_Power_Opower__class_Opower(T_a),V_a),V_n))
| ~ c_Orderings_Oord__class_Oless(T_a,c_Groups_Ozero__class_Ozero(T_a),V_a) )
| ~ class_Rings_Olinordered__semidom(T_a) ),
inference(miniscoping,[status(thm)],[f1465]) ).
fof(f1467,plain,
! [X0,X1,X2] :
( c_Orderings_Oord__class_Oless(X0,c_Groups_Ozero__class_Ozero(X0),hAPP(hAPP(c_Power_Opower__class_Opower(X0),X1),X2))
| ~ c_Orderings_Oord__class_Oless(X0,c_Groups_Ozero__class_Ozero(X0),X1)
| ~ class_Rings_Olinordered__semidom(X0) ),
inference(cnf_transformation,[status(thm)],[f1466]) ).
fof(f2194,plain,
! [V_y,V_x,V_z] :
( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),V_z),V_x),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),V_z),V_y))
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,V_x,V_y)
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),V_z) ),
inference(pre_NNF_transformation,[status(thm)],[f296]) ).
fof(f2195,plain,
! [V_z] :
( ! [V_y,V_x] :
( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),V_z),V_x),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),V_z),V_y))
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,V_x,V_y) )
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),V_z) ),
inference(miniscoping,[status(thm)],[f2194]) ).
fof(f2196,plain,
! [X0,X1,X2] :
( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),X0),X1),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),X0),X2))
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X1,X2)
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),X0) ),
inference(cnf_transformation,[status(thm)],[f2195]) ).
fof(f4573,plain,
class_Rings_Olinordered__semidom(tc_RealDef_Oreal),
inference(cnf_transformation,[status(thm)],[f1142]) ).
fof(f4779,plain,
~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),hAPP(hAPP(c_Power_Opower__class_Opower(tc_RealDef_Oreal),v_t____),v_k____)),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),v_t____),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____))),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),hAPP(hAPP(c_Power_Opower__class_Opower(tc_RealDef_Oreal),v_t____),v_k____)),c_Groups_Oone__class_Oone(tc_RealDef_Oreal))),
inference(cnf_transformation,[status(thm)],[f1289]) ).
fof(f5096,definition,
( sQ29_spl
<=> class_Rings_Olinordered__semidom(tc_RealDef_Oreal) ),
introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition]) ).
fof(f5098,plain,
( sQ29_spl
| ~ class_Rings_Olinordered__semidom(tc_RealDef_Oreal) ),
inference(component_clause,[status(thm)],[f5096]) ).
fof(f7325,plain,
( sQ29_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4573,f5098]) ).
fof(f7326,plain,
sQ29_spl,
inference(contradiction_clause,[status(thm)],[f7325]) ).
fof(f10815,plain,
( ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),v_t____),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____)),c_Groups_Oone__class_Oone(tc_RealDef_Oreal))
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),hAPP(hAPP(c_Power_Opower__class_Opower(tc_RealDef_Oreal),v_t____),v_k____)) ),
inference(resolution,[status(thm)],[f2196,f4779]) ).
fof(f10828,definition,
( sQ586_spl
<=> c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),hAPP(hAPP(c_Power_Opower__class_Opower(tc_RealDef_Oreal),v_t____),v_k____)) ),
introduced(definition,[new_symbols(definition,[sQ586_spl])],[split_symbol_definition]) ).
fof(f10830,plain,
( sQ586_spl
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),hAPP(hAPP(c_Power_Opower__class_Opower(tc_RealDef_Oreal),v_t____),v_k____)) ),
inference(component_clause,[status(thm)],[f10828]) ).
fof(f10855,definition,
( sQ593_spl
<=> c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),v_t____),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____)),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)) ),
introduced(definition,[new_symbols(definition,[sQ593_spl])],[split_symbol_definition]) ).
fof(f10857,plain,
( sQ593_spl
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),v_t____),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____)),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)) ),
inference(component_clause,[status(thm)],[f10855]) ).
fof(f10858,plain,
( ~ sQ593_spl
| ~ sQ586_spl ),
inference(split_clause,[status(thm)],[f10815,f10828,f10855]) ).
fof(f10961,plain,
( sQ586_spl
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),v_t____)
| ~ class_Rings_Olinordered__semidom(tc_RealDef_Oreal) ),
inference(resolution,[status(thm)],[f10830,f1467]) ).
fof(f10962,definition,
( sQ611_spl
<=> c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),v_t____) ),
introduced(definition,[new_symbols(definition,[sQ611_spl])],[split_symbol_definition]) ).
fof(f10964,plain,
( sQ611_spl
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),v_t____) ),
inference(component_clause,[status(thm)],[f10962]) ).
fof(f10965,plain,
( sQ586_spl
| ~ sQ611_spl
| ~ sQ29_spl ),
inference(split_clause,[status(thm)],[f10961,f5096,f10962,f10828]) ).
fof(f10971,plain,
( sQ611_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1297,f10964]) ).
fof(f10972,plain,
sQ611_spl,
inference(contradiction_clause,[status(thm)],[f10971]) ).
fof(f19099,plain,
( sQ593_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f10857,f1295]) ).
fof(f19100,plain,
sQ593_spl,
inference(contradiction_clause,[status(thm)],[f19099]) ).
fof(f19101,plain,
$false,
inference(sat_refutation,[status(thm)],[f7326,f10858,f10965,f10972,f19100]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWW262+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n007.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Mon Sep 21 09:42:21 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.14/0.46 % Drodi V4.1.1
% 125.51/16.36 % Refutation found
% 125.51/16.36 % SZS status Theorem for theBenchmark: Theorem is valid
% 125.51/16.36 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 8.22/16.74 % Elapsed time: 16.373128 seconds
% 8.22/16.74 % CPU time: 127.057359 seconds
% 8.22/16.74 % Total memory used: 746.190 MB
% 8.22/16.74 % Net memory used: 704.460 MB
%------------------------------------------------------------------------------