%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWW192+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 : n015.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:24 PM UTC 2026
% Result : Theorem 238.44s 30.75s
% Output : CNFRefutation 238.44s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 8
% Syntax : Number of formulae : 33 ( 25 unt; 0 def)
% Number of atoms : 49 ( 48 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 35 ( 19 ~; 10 |; 4 &)
% ( 2 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 2 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 19 ( 19 usr; 7 con; 0-3 aty)
% Number of variables : 23 ( 23 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f2,axiom,
c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_z) = c_Groups_Oone__class_Oone(tc_RealDef_Oreal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f3,axiom,
v_z = c_Complex_Ocomplex_OComplex(v_x____,v_y____),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f53,axiom,
! [V_y,V_x] : c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Complex_Ocomplex_OComplex(V_x,V_y)) = c_NthRoot_Osqrt(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,hAPP(hAPP(c_Power_Opower__class_Opower(tc_RealDef_Oreal),V_x),c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))),hAPP(hAPP(c_Power_Opower__class_Opower(tc_RealDef_Oreal),V_y),c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f186,axiom,
! [V_ya_2,V_xa_2] :
( c_NthRoot_Osqrt(V_xa_2) = c_NthRoot_Osqrt(V_ya_2)
<=> V_xa_2 = V_ya_2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f203,axiom,
! [V_xa_2] :
( c_NthRoot_Osqrt(V_xa_2) = c_Groups_Oone__class_Oone(tc_RealDef_Oreal)
<=> V_xa_2 = c_Groups_Oone__class_Oone(tc_RealDef_Oreal) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f489,axiom,
c_Groups_Oone__class_Oone(tc_Nat_Onat) = c_Nat_OSuc(c_Groups_Ozero__class_Ozero(tc_Nat_Onat)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f525,axiom,
c_Nat_OSuc(c_Nat_OSuc(c_Groups_Ozero__class_Ozero(tc_Nat_Onat))) = c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f1231,conjecture,
c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,hAPP(hAPP(c_Power_Opower__class_Opower(tc_RealDef_Oreal),v_x____),c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))),hAPP(hAPP(c_Power_Opower__class_Opower(tc_RealDef_Oreal),v_y____),c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Int_OBit0(c_Int_OBit1(c_Int_OPls))))) = c_Groups_Oone__class_Oone(tc_RealDef_Oreal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f1232,negated_conjecture,
c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,hAPP(hAPP(c_Power_Opower__class_Opower(tc_RealDef_Oreal),v_x____),c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))),hAPP(hAPP(c_Power_Opower__class_Opower(tc_RealDef_Oreal),v_y____),c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Int_OBit0(c_Int_OBit1(c_Int_OPls))))) != c_Groups_Oone__class_Oone(tc_RealDef_Oreal),
inference(negated_conjecture,[status(cth)],[f1231]) ).
fof(f1236,plain,
c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_z) = c_Groups_Oone__class_Oone(tc_RealDef_Oreal),
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f1237,plain,
v_z = c_Complex_Ocomplex_OComplex(v_x____,v_y____),
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f1348,plain,
! [X0,X1] : c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Complex_Ocomplex_OComplex(X0,X1)) = c_NthRoot_Osqrt(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,hAPP(hAPP(c_Power_Opower__class_Opower(tc_RealDef_Oreal),X0),c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))),hAPP(hAPP(c_Power_Opower__class_Opower(tc_RealDef_Oreal),X1),c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))))),
inference(cnf_transformation,[status(thm)],[f53]) ).
fof(f1685,plain,
! [V_ya_2,V_xa_2] :
( ( V_xa_2 != V_ya_2
| c_NthRoot_Osqrt(V_xa_2) = c_NthRoot_Osqrt(V_ya_2) )
& ( V_xa_2 = V_ya_2
| c_NthRoot_Osqrt(V_xa_2) != c_NthRoot_Osqrt(V_ya_2) ) ),
inference(NNF_transformation,[status(thm)],[f186]) ).
fof(f1686,plain,
( ! [V_ya_2,V_xa_2] :
( V_xa_2 != V_ya_2
| c_NthRoot_Osqrt(V_xa_2) = c_NthRoot_Osqrt(V_ya_2) )
& ! [V_ya_2,V_xa_2] :
( V_xa_2 = V_ya_2
| c_NthRoot_Osqrt(V_xa_2) != c_NthRoot_Osqrt(V_ya_2) ) ),
inference(miniscoping,[status(thm)],[f1685]) ).
fof(f1687,plain,
! [X0,X1] :
( X0 = X1
| c_NthRoot_Osqrt(X0) != c_NthRoot_Osqrt(X1) ),
inference(cnf_transformation,[status(thm)],[f1686]) ).
fof(f1743,plain,
! [V_xa_2] :
( ( V_xa_2 != c_Groups_Oone__class_Oone(tc_RealDef_Oreal)
| c_NthRoot_Osqrt(V_xa_2) = c_Groups_Oone__class_Oone(tc_RealDef_Oreal) )
& ( V_xa_2 = c_Groups_Oone__class_Oone(tc_RealDef_Oreal)
| c_NthRoot_Osqrt(V_xa_2) != c_Groups_Oone__class_Oone(tc_RealDef_Oreal) ) ),
inference(NNF_transformation,[status(thm)],[f203]) ).
fof(f1744,plain,
( ! [V_xa_2] :
( V_xa_2 != c_Groups_Oone__class_Oone(tc_RealDef_Oreal)
| c_NthRoot_Osqrt(V_xa_2) = c_Groups_Oone__class_Oone(tc_RealDef_Oreal) )
& ! [V_xa_2] :
( V_xa_2 = c_Groups_Oone__class_Oone(tc_RealDef_Oreal)
| c_NthRoot_Osqrt(V_xa_2) != c_Groups_Oone__class_Oone(tc_RealDef_Oreal) ) ),
inference(miniscoping,[status(thm)],[f1743]) ).
fof(f1746,plain,
! [X0] :
( X0 != c_Groups_Oone__class_Oone(tc_RealDef_Oreal)
| c_NthRoot_Osqrt(X0) = c_Groups_Oone__class_Oone(tc_RealDef_Oreal) ),
inference(cnf_transformation,[status(thm)],[f1744]) ).
fof(f2637,plain,
c_Groups_Oone__class_Oone(tc_Nat_Onat) = c_Nat_OSuc(c_Groups_Ozero__class_Ozero(tc_Nat_Onat)),
inference(cnf_transformation,[status(thm)],[f489]) ).
fof(f2749,plain,
c_Nat_OSuc(c_Nat_OSuc(c_Groups_Ozero__class_Ozero(tc_Nat_Onat))) = c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),
inference(cnf_transformation,[status(thm)],[f525]) ).
fof(f4654,plain,
c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,hAPP(hAPP(c_Power_Opower__class_Opower(tc_RealDef_Oreal),v_x____),c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))),hAPP(hAPP(c_Power_Opower__class_Opower(tc_RealDef_Oreal),v_y____),c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Int_OBit0(c_Int_OBit1(c_Int_OPls))))) != c_Groups_Oone__class_Oone(tc_RealDef_Oreal),
inference(cnf_transformation,[status(thm)],[f1232]) ).
fof(f4802,plain,
c_NthRoot_Osqrt(c_Groups_Oone__class_Oone(tc_RealDef_Oreal)) = c_Groups_Oone__class_Oone(tc_RealDef_Oreal),
inference(destructive_equality_resolution,[status(thm)],[f1746]) ).
fof(f4932,plain,
! [X0,X1] : c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Complex_Ocomplex_OComplex(X0,X1)) = c_NthRoot_Osqrt(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,hAPP(hAPP(c_Power_Opower__class_Opower(tc_RealDef_Oreal),X0),c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))),hAPP(hAPP(c_Power_Opower__class_Opower(tc_RealDef_Oreal),X1),c_Nat_OSuc(c_Groups_Oone__class_Oone(tc_Nat_Onat))))),
inference(backward_demodulation,[status(thm)],[f4942,f1348]) ).
fof(f4942,plain,
c_Nat_OSuc(c_Groups_Oone__class_Oone(tc_Nat_Onat)) = c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),
inference(forward_demodulation,[status(thm)],[f2637,f2749]) ).
fof(f5160,plain,
c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,hAPP(hAPP(c_Power_Opower__class_Opower(tc_RealDef_Oreal),v_x____),c_Nat_OSuc(c_Groups_Oone__class_Oone(tc_Nat_Onat))),hAPP(hAPP(c_Power_Opower__class_Opower(tc_RealDef_Oreal),v_y____),c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Int_OBit0(c_Int_OBit1(c_Int_OPls))))) != c_Groups_Oone__class_Oone(tc_RealDef_Oreal),
inference(forward_demodulation,[status(thm)],[f4942,f4654]) ).
fof(f5161,plain,
c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,hAPP(hAPP(c_Power_Opower__class_Opower(tc_RealDef_Oreal),v_x____),c_Nat_OSuc(c_Groups_Oone__class_Oone(tc_Nat_Onat))),hAPP(hAPP(c_Power_Opower__class_Opower(tc_RealDef_Oreal),v_y____),c_Nat_OSuc(c_Groups_Oone__class_Oone(tc_Nat_Onat)))) != c_Groups_Oone__class_Oone(tc_RealDef_Oreal),
inference(forward_demodulation,[status(thm)],[f4942,f5160]) ).
fof(f5262,plain,
! [X0,X1] : c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Complex_Ocomplex_OComplex(X0,X1)) = c_NthRoot_Osqrt(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,hAPP(hAPP(c_Power_Opower__class_Opower(tc_RealDef_Oreal),X0),c_Nat_OSuc(c_Groups_Oone__class_Oone(tc_Nat_Onat))),hAPP(hAPP(c_Power_Opower__class_Opower(tc_RealDef_Oreal),X1),c_Nat_OSuc(c_Groups_Oone__class_Oone(tc_Nat_Onat))))),
inference(forward_demodulation,[status(thm)],[f4942,f4932]) ).
fof(f10682,plain,
c_NthRoot_Osqrt(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,hAPP(hAPP(c_Power_Opower__class_Opower(tc_RealDef_Oreal),v_x____),c_Nat_OSuc(c_Groups_Oone__class_Oone(tc_Nat_Onat))),hAPP(hAPP(c_Power_Opower__class_Opower(tc_RealDef_Oreal),v_y____),c_Nat_OSuc(c_Groups_Oone__class_Oone(tc_Nat_Onat))))) != c_NthRoot_Osqrt(c_Groups_Oone__class_Oone(tc_RealDef_Oreal)),
inference(resolution,[status(thm)],[f1687,f5161]) ).
fof(f10759,plain,
c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Complex_Ocomplex_OComplex(v_x____,v_y____)) != c_NthRoot_Osqrt(c_Groups_Oone__class_Oone(tc_RealDef_Oreal)),
inference(forward_demodulation,[status(thm)],[f5262,f10682]) ).
fof(f10760,plain,
c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_z) != c_NthRoot_Osqrt(c_Groups_Oone__class_Oone(tc_RealDef_Oreal)),
inference(forward_demodulation,[status(thm)],[f1237,f10759]) ).
fof(f10761,plain,
c_Groups_Oone__class_Oone(tc_RealDef_Oreal) != c_NthRoot_Osqrt(c_Groups_Oone__class_Oone(tc_RealDef_Oreal)),
inference(forward_demodulation,[status(thm)],[f1236,f10760]) ).
fof(f10762,plain,
c_Groups_Oone__class_Oone(tc_RealDef_Oreal) != c_Groups_Oone__class_Oone(tc_RealDef_Oreal),
inference(forward_demodulation,[status(thm)],[f4802,f10761]) ).
fof(f10763,plain,
$false,
inference(trivial_equality_resolution,[status(thm)],[f10762]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SWW192+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.07 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.18/0.43 % Computer : n015.cluster.edu
% 0.18/0.43 % Model : x86_64 x86_64
% 0.18/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.43 % Memory : 8046.5625MB
% 0.18/0.43 % OS : Linux 6.8.0-71-generic
% 0.18/0.43 % CPULimit : 300
% 0.18/0.43 % WCLimit : 300
% 0.18/0.43 % DateTime : Mon Sep 21 09:44:08 UTC 2026
% 0.18/0.44 % CPUTime :
% 0.27/0.60 % Drodi V4.1.1
% 238.44/30.75 % Refutation found
% 238.44/30.75 % SZS status Theorem for theBenchmark: Theorem is valid
% 238.44/30.75 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 16.50/31.77 % Elapsed time: 31.310717 seconds
% 16.50/31.77 % CPU time: 241.728982 seconds
% 16.50/31.77 % Total memory used: 963.393 MB
% 16.50/31.77 % Net memory used: 905.252 MB
%------------------------------------------------------------------------------