%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWW178+1 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n019.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:23 PM UTC 2026
% Result : Theorem 28.83s 4.32s
% Output : CNFRefutation 28.83s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 11
% Syntax : Number of formulae : 45 ( 20 unt; 0 def)
% Number of atoms : 74 ( 20 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 59 ( 30 ~; 23 |; 0 &)
% ( 0 <=>; 6 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 6 ( 4 usr; 1 prp; 0-3 aty)
% Number of functors : 8 ( 8 usr; 4 con; 0-3 aty)
% Number of variables : 79 ( 79 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f13,axiom,
! [V_w] : c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_w,V_w),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f29,axiom,
! [V_b,V_a,T_a] :
( class_Groups_Ogroup__add(T_a)
=> c_Groups_Oplus__class_Oplus(T_a,c_Groups_Ominus__class_Ominus(T_a,V_a,V_b),V_b) = V_a ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f30,axiom,
! [V_b,V_a,T_a] :
( class_Groups_Ogroup__add(T_a)
=> c_Groups_Oplus__class_Oplus(T_a,c_Groups_Ouminus__class_Ouminus(T_a,V_a),c_Groups_Oplus__class_Oplus(T_a,V_a,V_b)) = V_b ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f38,axiom,
! [V_b,V_a,T_a] :
( class_RealVector_Oreal__normed__vector(T_a)
=> c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(T_a,c_Groups_Ominus__class_Ominus(T_a,V_a,V_b)),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(T_a,V_a),c_RealVector_Onorm__class_Onorm(T_a,V_b))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f63,axiom,
! [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) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f89,axiom,
! [V_y,V_x] : c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,V_x,V_y) = c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex,V_x,c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,V_y)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f102,axiom,
! [V_c,V_a,T_a] :
( class_Rings_Ocomm__semiring__1(T_a)
=> c_Groups_Oplus__class_Oplus(T_a,V_a,V_c) = c_Groups_Oplus__class_Oplus(T_a,V_c,V_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f1169,axiom,
class_RealVector_Oreal__normed__vector(tc_Complex_Ocomplex),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f1180,axiom,
class_Rings_Ocomm__semiring__1(tc_Complex_Ocomplex),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f1189,axiom,
class_Groups_Ogroup__add(tc_Complex_Ocomplex),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f1200,conjecture,
c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_w),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex,v_w,v_z)),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_z))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f1201,negated_conjecture,
~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_w),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex,v_w,v_z)),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_z))),
inference(negated_conjecture,[status(cth)],[f1200]) ).
fof(f1240,plain,
! [X0] : c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X0,X0),
inference(cnf_transformation,[status(thm)],[f13]) ).
fof(f1302,plain,
! [V_b,V_a,T_a] :
( c_Groups_Oplus__class_Oplus(T_a,c_Groups_Ominus__class_Ominus(T_a,V_a,V_b),V_b) = V_a
| ~ class_Groups_Ogroup__add(T_a) ),
inference(pre_NNF_transformation,[status(thm)],[f29]) ).
fof(f1303,plain,
! [T_a] :
( ! [V_b,V_a] : c_Groups_Oplus__class_Oplus(T_a,c_Groups_Ominus__class_Ominus(T_a,V_a,V_b),V_b) = V_a
| ~ class_Groups_Ogroup__add(T_a) ),
inference(miniscoping,[status(thm)],[f1302]) ).
fof(f1304,plain,
! [X0,X1,X2] :
( c_Groups_Oplus__class_Oplus(X0,c_Groups_Ominus__class_Ominus(X0,X1,X2),X2) = X1
| ~ class_Groups_Ogroup__add(X0) ),
inference(cnf_transformation,[status(thm)],[f1303]) ).
fof(f1305,plain,
! [V_b,V_a,T_a] :
( c_Groups_Oplus__class_Oplus(T_a,c_Groups_Ouminus__class_Ouminus(T_a,V_a),c_Groups_Oplus__class_Oplus(T_a,V_a,V_b)) = V_b
| ~ class_Groups_Ogroup__add(T_a) ),
inference(pre_NNF_transformation,[status(thm)],[f30]) ).
fof(f1306,plain,
! [T_a] :
( ! [V_b,V_a] : c_Groups_Oplus__class_Oplus(T_a,c_Groups_Ouminus__class_Ouminus(T_a,V_a),c_Groups_Oplus__class_Oplus(T_a,V_a,V_b)) = V_b
| ~ class_Groups_Ogroup__add(T_a) ),
inference(miniscoping,[status(thm)],[f1305]) ).
fof(f1307,plain,
! [X0,X1,X2] :
( c_Groups_Oplus__class_Oplus(X0,c_Groups_Ouminus__class_Ouminus(X0,X1),c_Groups_Oplus__class_Oplus(X0,X1,X2)) = X2
| ~ class_Groups_Ogroup__add(X0) ),
inference(cnf_transformation,[status(thm)],[f1306]) ).
fof(f1329,plain,
! [V_b,V_a,T_a] :
( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(T_a,c_Groups_Ominus__class_Ominus(T_a,V_a,V_b)),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(T_a,V_a),c_RealVector_Onorm__class_Onorm(T_a,V_b)))
| ~ class_RealVector_Oreal__normed__vector(T_a) ),
inference(pre_NNF_transformation,[status(thm)],[f38]) ).
fof(f1330,plain,
! [T_a] :
( ! [V_b,V_a] : c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(T_a,c_Groups_Ominus__class_Ominus(T_a,V_a,V_b)),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(T_a,V_a),c_RealVector_Onorm__class_Onorm(T_a,V_b)))
| ~ class_RealVector_Oreal__normed__vector(T_a) ),
inference(miniscoping,[status(thm)],[f1329]) ).
fof(f1331,plain,
! [X0,X1,X2] :
( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(X0,c_Groups_Ominus__class_Ominus(X0,X1,X2)),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(X0,X1),c_RealVector_Onorm__class_Onorm(X0,X2)))
| ~ class_RealVector_Oreal__normed__vector(X0) ),
inference(cnf_transformation,[status(thm)],[f1330]) ).
fof(f1415,plain,
! [V_k,V_j,V_i] :
( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_i,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_j) ),
inference(pre_NNF_transformation,[status(thm)],[f63]) ).
fof(f1416,plain,
! [V_j,V_i] :
( ! [V_k] :
( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_i,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_j) ),
inference(miniscoping,[status(thm)],[f1415]) ).
fof(f1417,plain,
! [X0,X1,X2] :
( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X0,X2)
| ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X1,X2)
| ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X0,X1) ),
inference(cnf_transformation,[status(thm)],[f1416]) ).
fof(f1487,plain,
! [X0,X1] : c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,X0,X1) = c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex,X0,c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,X1)),
inference(cnf_transformation,[status(thm)],[f89]) ).
fof(f1523,plain,
! [V_c,V_a,T_a] :
( c_Groups_Oplus__class_Oplus(T_a,V_a,V_c) = c_Groups_Oplus__class_Oplus(T_a,V_c,V_a)
| ~ class_Rings_Ocomm__semiring__1(T_a) ),
inference(pre_NNF_transformation,[status(thm)],[f102]) ).
fof(f1524,plain,
! [T_a] :
( ! [V_c,V_a] : c_Groups_Oplus__class_Oplus(T_a,V_a,V_c) = c_Groups_Oplus__class_Oplus(T_a,V_c,V_a)
| ~ class_Rings_Ocomm__semiring__1(T_a) ),
inference(miniscoping,[status(thm)],[f1523]) ).
fof(f1525,plain,
! [X0,X1,X2] :
( c_Groups_Oplus__class_Oplus(X0,X1,X2) = c_Groups_Oplus__class_Oplus(X0,X2,X1)
| ~ class_Rings_Ocomm__semiring__1(X0) ),
inference(cnf_transformation,[status(thm)],[f1524]) ).
fof(f4466,plain,
class_RealVector_Oreal__normed__vector(tc_Complex_Ocomplex),
inference(cnf_transformation,[status(thm)],[f1169]) ).
fof(f4477,plain,
class_Rings_Ocomm__semiring__1(tc_Complex_Ocomplex),
inference(cnf_transformation,[status(thm)],[f1180]) ).
fof(f4486,plain,
class_Groups_Ogroup__add(tc_Complex_Ocomplex),
inference(cnf_transformation,[status(thm)],[f1189]) ).
fof(f4497,plain,
~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_w),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex,v_w,v_z)),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_z))),
inference(cnf_transformation,[status(thm)],[f1201]) ).
fof(f4672,plain,
! [X0] :
( ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X0,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex,v_w,v_z)),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_z)))
| ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_w),X0) ),
inference(resolution,[status(thm)],[f1417,f4497]) ).
fof(f5869,plain,
( ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_w),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex,v_w,v_z),v_z)))
| ~ class_RealVector_Oreal__normed__vector(tc_Complex_Ocomplex) ),
inference(resolution,[status(thm)],[f1331,f4672]) ).
fof(f7258,plain,
~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_w),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex,v_w,v_z),v_z))),
inference(backward_subsumption_resolution,[status(thm)],[f5869,f4466]) ).
fof(f12612,plain,
! [X0,X1] :
( c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,X0,X1) = c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex,c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,X1),X0)
| ~ class_Rings_Ocomm__semiring__1(tc_Complex_Ocomplex) ),
inference(paramodulation,[status(thm)],[f1487,f1525]) ).
fof(f12641,plain,
! [X0,X1] : c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,X0,X1) = c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex,c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,X1),X0),
inference(forward_subsumption_resolution,[status(thm)],[f12612,f4477]) ).
fof(f32638,plain,
! [X0,X1] :
( c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex,X0,X1),X0) = X1
| ~ class_Groups_Ogroup__add(tc_Complex_Ocomplex) ),
inference(paramodulation,[status(thm)],[f12641,f1307]) ).
fof(f32729,plain,
! [X0,X1] : c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex,X0,X1),X0) = X1,
inference(forward_subsumption_resolution,[status(thm)],[f32638,f4486]) ).
fof(f32971,plain,
! [X0,X1] :
( c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex,X0,X1) = c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex,X1,X0)
| ~ class_Groups_Ogroup__add(tc_Complex_Ocomplex) ),
inference(paramodulation,[status(thm)],[f32729,f1304]) ).
fof(f33007,plain,
! [X0,X1] : c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex,X0,X1) = c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex,X1,X0),
inference(forward_subsumption_resolution,[status(thm)],[f32971,f4486]) ).
fof(f33216,plain,
~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_w),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex,v_z,v_w),v_z))),
inference(paramodulation,[status(thm)],[f33007,f7258]) ).
fof(f33552,plain,
~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_w),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_w)),
inference(forward_demodulation,[status(thm)],[f32729,f33216]) ).
fof(f33553,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f33552,f1240]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWW178+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.36 % Computer : n019.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Mon Sep 21 09:40:34 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.15/0.46 % Drodi V4.1.1
% 28.83/4.32 % Refutation found
% 28.83/4.32 % SZS status Theorem for theBenchmark: Theorem is valid
% 28.83/4.32 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 2.89/5.18 % Elapsed time: 4.795304 seconds
% 2.89/5.18 % CPU time: 31.657597 seconds
% 2.89/5.18 % Total memory used: 374.950 MB
% 2.89/5.18 % Net memory used: 352.538 MB
%------------------------------------------------------------------------------