%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : ALG380-1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n001.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 11:49:18 AM UTC 2026
% Result : Unsatisfiable 6.16s 1.27s
% Output : CNFRefutation 6.16s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 11
% Syntax : Number of formulae : 40 ( 30 unt; 0 def)
% Number of atoms : 50 ( 30 equ)
% Maximal formula atoms : 2 ( 1 avg)
% Number of connectives : 27 ( 17 ~; 10 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 3 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-3 aty)
% Number of functors : 17 ( 17 usr; 5 con; 0-3 aty)
% Number of variables : 47 ( 47 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f39,axiom,
! [V_x] :
( ~ c_HOL_Oord__class_Oless(V_x,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)
| c_HOL_Oord__class_Oless(c_NthRoot_Osqrt(V_x),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f48,axiom,
! [T_a,V_x] :
( ~ c_HOL_Oord__class_Oless(c_RealVector_Onorm__class_Onorm(V_x,T_a),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ class_RealVector_Oreal__normed__vector(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f126,axiom,
! [V_r] : c_Complex_Orcis(V_r,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)) = c_RealVector_Oof__real(V_r,tc_Complex_Ocomplex),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f615,axiom,
! [V_x,V_y] : c_NthRoot_Osqrt(c_HOL_Otimes__class_Otimes(V_x,V_y,tc_RealDef_Oreal)) = c_HOL_Otimes__class_Otimes(c_NthRoot_Osqrt(V_x),c_NthRoot_Osqrt(V_y),tc_RealDef_Oreal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f620,axiom,
! [V_r1,V_a,V_r2,V_b] : c_HOL_Otimes__class_Otimes(c_Complex_Orcis(V_r1,V_a),c_Complex_Orcis(V_r2,V_b),tc_Complex_Ocomplex) = c_Complex_Orcis(c_HOL_Otimes__class_Otimes(V_r1,V_r2,tc_RealDef_Oreal),c_HOL_Oplus__class_Oplus(V_a,V_b,tc_RealDef_Oreal)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f867,axiom,
! [V_r] :
( c_HOL_Oord__class_Oless(V_r,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)
| c_HOL_Oabs__class_Oabs(V_r,tc_RealDef_Oreal) = V_r ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f946,axiom,
! [V_x] : c_NthRoot_Osqrt(c_HOL_Otimes__class_Otimes(V_x,V_x,tc_RealDef_Oreal)) = c_HOL_Oabs__class_Oabs(V_x,tc_RealDef_Oreal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f947,axiom,
! [V_r,V_a] : c_RealVector_Onorm__class_Onorm(c_Complex_Orcis(V_r,V_a),tc_Complex_Ocomplex) = c_HOL_Oabs__class_Oabs(V_r,tc_RealDef_Oreal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f995,axiom,
! [V_x] : c_HOL_Oplus__class_Oplus(c_HOL_Oinverse__class_Odivide(V_x,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(V_x,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal) = V_x,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1032,negated_conjecture,
c_HOL_Otimes__class_Otimes(c_Complex_Orcis(c_NthRoot_Osqrt(c_HOL_Oabs__class_Oabs(v_r,tc_RealDef_Oreal)),c_HOL_Oinverse__class_Odivide(v_a,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal)),c_Complex_Orcis(c_NthRoot_Osqrt(c_HOL_Oabs__class_Oabs(v_r,tc_RealDef_Oreal)),c_HOL_Oinverse__class_Odivide(v_a,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal)),tc_Complex_Ocomplex) != c_Complex_Orcis(c_HOL_Oabs__class_Oabs(v_r,tc_RealDef_Oreal),v_a),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1192,axiom,
class_RealVector_Oreal__normed__vector(tc_Complex_Ocomplex),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1270,plain,
! [X0] :
( ~ c_HOL_Oord__class_Oless(X0,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)
| c_HOL_Oord__class_Oless(c_NthRoot_Osqrt(X0),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal) ),
inference(cnf_transformation,[status(thm)],[f39]) ).
fof(f1284,plain,
! [T_a] :
( ! [V_x] : ~ c_HOL_Oord__class_Oless(c_RealVector_Onorm__class_Onorm(V_x,T_a),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ class_RealVector_Oreal__normed__vector(T_a) ),
inference(miniscoping,[status(thm)],[f48]) ).
fof(f1285,plain,
! [X0,X1] :
( ~ c_HOL_Oord__class_Oless(c_RealVector_Onorm__class_Onorm(X1,X0),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ class_RealVector_Oreal__normed__vector(X0) ),
inference(cnf_transformation,[status(thm)],[f1284]) ).
fof(f1397,plain,
! [X0] : c_Complex_Orcis(X0,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)) = c_RealVector_Oof__real(X0,tc_Complex_Ocomplex),
inference(cnf_transformation,[status(thm)],[f126]) ).
fof(f2183,plain,
! [X0,X1] : c_NthRoot_Osqrt(c_HOL_Otimes__class_Otimes(X0,X1,tc_RealDef_Oreal)) = c_HOL_Otimes__class_Otimes(c_NthRoot_Osqrt(X0),c_NthRoot_Osqrt(X1),tc_RealDef_Oreal),
inference(cnf_transformation,[status(thm)],[f615]) ).
fof(f2189,plain,
! [X0,X1,X2,X3] : c_HOL_Otimes__class_Otimes(c_Complex_Orcis(X0,X1),c_Complex_Orcis(X2,X3),tc_Complex_Ocomplex) = c_Complex_Orcis(c_HOL_Otimes__class_Otimes(X0,X2,tc_RealDef_Oreal),c_HOL_Oplus__class_Oplus(X1,X3,tc_RealDef_Oreal)),
inference(cnf_transformation,[status(thm)],[f620]) ).
fof(f2532,plain,
! [X0] :
( c_HOL_Oord__class_Oless(X0,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)
| c_HOL_Oabs__class_Oabs(X0,tc_RealDef_Oreal) = X0 ),
inference(cnf_transformation,[status(thm)],[f867]) ).
fof(f2647,plain,
! [X0] : c_NthRoot_Osqrt(c_HOL_Otimes__class_Otimes(X0,X0,tc_RealDef_Oreal)) = c_HOL_Oabs__class_Oabs(X0,tc_RealDef_Oreal),
inference(cnf_transformation,[status(thm)],[f946]) ).
fof(f2648,plain,
! [X0,X1] : c_RealVector_Onorm__class_Onorm(c_Complex_Orcis(X0,X1),tc_Complex_Ocomplex) = c_HOL_Oabs__class_Oabs(X0,tc_RealDef_Oreal),
inference(cnf_transformation,[status(thm)],[f947]) ).
fof(f2713,plain,
! [X0] : c_HOL_Oplus__class_Oplus(c_HOL_Oinverse__class_Odivide(X0,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(X0,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal) = X0,
inference(cnf_transformation,[status(thm)],[f995]) ).
fof(f2774,plain,
c_HOL_Otimes__class_Otimes(c_Complex_Orcis(c_NthRoot_Osqrt(c_HOL_Oabs__class_Oabs(v_r,tc_RealDef_Oreal)),c_HOL_Oinverse__class_Odivide(v_a,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal)),c_Complex_Orcis(c_NthRoot_Osqrt(c_HOL_Oabs__class_Oabs(v_r,tc_RealDef_Oreal)),c_HOL_Oinverse__class_Odivide(v_a,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal)),tc_Complex_Ocomplex) != c_Complex_Orcis(c_HOL_Oabs__class_Oabs(v_r,tc_RealDef_Oreal),v_a),
inference(cnf_transformation,[status(thm)],[f1032]) ).
fof(f2934,plain,
class_RealVector_Oreal__normed__vector(tc_Complex_Ocomplex),
inference(cnf_transformation,[status(thm)],[f1192]) ).
fof(f3008,plain,
! [X0] : c_RealVector_Onorm__class_Onorm(c_RealVector_Oof__real(X0,tc_Complex_Ocomplex),tc_Complex_Ocomplex) = c_HOL_Oabs__class_Oabs(X0,tc_RealDef_Oreal),
inference(paramodulation,[status(thm)],[f1397,f2648]) ).
fof(f3019,plain,
! [X0] :
( c_HOL_Oord__class_Oless(c_NthRoot_Osqrt(X0),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)
| c_HOL_Oabs__class_Oabs(X0,tc_RealDef_Oreal) = X0 ),
inference(resolution,[status(thm)],[f2532,f1270]) ).
fof(f3098,plain,
! [X0] :
( c_HOL_Oord__class_Oless(c_HOL_Oabs__class_Oabs(X0,tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)
| c_HOL_Oabs__class_Oabs(c_HOL_Otimes__class_Otimes(X0,X0,tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(X0,X0,tc_RealDef_Oreal) ),
inference(paramodulation,[status(thm)],[f2647,f3019]) ).
fof(f3119,plain,
! [X0] : c_NthRoot_Osqrt(c_NthRoot_Osqrt(c_HOL_Otimes__class_Otimes(X0,X0,tc_RealDef_Oreal))) = c_HOL_Oabs__class_Oabs(c_NthRoot_Osqrt(X0),tc_RealDef_Oreal),
inference(paramodulation,[status(thm)],[f2183,f2647]) ).
fof(f3129,plain,
! [X0] : c_NthRoot_Osqrt(c_HOL_Oabs__class_Oabs(X0,tc_RealDef_Oreal)) = c_HOL_Oabs__class_Oabs(c_NthRoot_Osqrt(X0),tc_RealDef_Oreal),
inference(forward_demodulation,[status(thm)],[f2647,f3119]) ).
fof(f3139,plain,
! [X0] : c_NthRoot_Osqrt(c_HOL_Oabs__class_Oabs(c_HOL_Otimes__class_Otimes(X0,X0,tc_RealDef_Oreal),tc_RealDef_Oreal)) = c_HOL_Oabs__class_Oabs(c_HOL_Oabs__class_Oabs(X0,tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(paramodulation,[status(thm)],[f2647,f3129]) ).
fof(f3851,plain,
! [X0,X1,X2,X3] : c_HOL_Otimes__class_Otimes(c_Complex_Orcis(c_NthRoot_Osqrt(X0),X1),c_Complex_Orcis(c_NthRoot_Osqrt(X2),X3),tc_Complex_Ocomplex) = c_Complex_Orcis(c_NthRoot_Osqrt(c_HOL_Otimes__class_Otimes(X0,X2,tc_RealDef_Oreal)),c_HOL_Oplus__class_Oplus(X1,X3,tc_RealDef_Oreal)),
inference(paramodulation,[status(thm)],[f2183,f2189]) ).
fof(f3859,plain,
c_Complex_Orcis(c_NthRoot_Osqrt(c_HOL_Otimes__class_Otimes(c_HOL_Oabs__class_Oabs(v_r,tc_RealDef_Oreal),c_HOL_Oabs__class_Oabs(v_r,tc_RealDef_Oreal),tc_RealDef_Oreal)),c_HOL_Oplus__class_Oplus(c_HOL_Oinverse__class_Odivide(v_a,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(v_a,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal)) != c_Complex_Orcis(c_HOL_Oabs__class_Oabs(v_r,tc_RealDef_Oreal),v_a),
inference(backward_demodulation,[status(thm)],[f3851,f2774]) ).
fof(f3864,plain,
c_Complex_Orcis(c_HOL_Oabs__class_Oabs(c_HOL_Oabs__class_Oabs(v_r,tc_RealDef_Oreal),tc_RealDef_Oreal),c_HOL_Oplus__class_Oplus(c_HOL_Oinverse__class_Odivide(v_a,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(v_a,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal)) != c_Complex_Orcis(c_HOL_Oabs__class_Oabs(v_r,tc_RealDef_Oreal),v_a),
inference(forward_demodulation,[status(thm)],[f2647,f3859]) ).
fof(f3865,plain,
c_Complex_Orcis(c_HOL_Oabs__class_Oabs(c_HOL_Oabs__class_Oabs(v_r,tc_RealDef_Oreal),tc_RealDef_Oreal),v_a) != c_Complex_Orcis(c_HOL_Oabs__class_Oabs(v_r,tc_RealDef_Oreal),v_a),
inference(forward_demodulation,[status(thm)],[f2713,f3864]) ).
fof(f3883,plain,
! [X0] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Oabs__class_Oabs(X0,tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ class_RealVector_Oreal__normed__vector(tc_Complex_Ocomplex) ),
inference(paramodulation,[status(thm)],[f3008,f1285]) ).
fof(f3885,plain,
! [X0] : c_HOL_Oabs__class_Oabs(c_HOL_Otimes__class_Otimes(X0,X0,tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(X0,X0,tc_RealDef_Oreal),
inference(backward_subsumption_resolution,[status(thm)],[f3098,f3886]) ).
fof(f3886,plain,
! [X0] : ~ c_HOL_Oord__class_Oless(c_HOL_Oabs__class_Oabs(X0,tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(forward_subsumption_resolution,[status(thm)],[f3883,f2934]) ).
fof(f3890,plain,
! [X0] : c_NthRoot_Osqrt(c_HOL_Otimes__class_Otimes(X0,X0,tc_RealDef_Oreal)) = c_HOL_Oabs__class_Oabs(c_HOL_Oabs__class_Oabs(X0,tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(backward_demodulation,[status(thm)],[f3885,f3139]) ).
fof(f3892,plain,
c_Complex_Orcis(c_HOL_Oabs__class_Oabs(v_r,tc_RealDef_Oreal),v_a) != c_Complex_Orcis(c_HOL_Oabs__class_Oabs(v_r,tc_RealDef_Oreal),v_a),
inference(backward_demodulation,[status(thm)],[f3894,f3865]) ).
fof(f3894,plain,
! [X0] : c_HOL_Oabs__class_Oabs(X0,tc_RealDef_Oreal) = c_HOL_Oabs__class_Oabs(c_HOL_Oabs__class_Oabs(X0,tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(forward_demodulation,[status(thm)],[f2647,f3890]) ).
fof(f3895,plain,
$false,
inference(trivial_equality_resolution,[status(thm)],[f3892]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG380-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.36 % Computer : n001.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 13:23:45 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.13/0.40 % Drodi V4.1.1
% 6.16/1.27 % Refutation found
% 6.16/1.27 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 6.16/1.27 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 6.16/1.31 % Elapsed time: 0.944073 seconds
% 6.16/1.31 % CPU time: 6.921743 seconds
% 6.16/1.31 % Total memory used: 271.148 MB
% 6.16/1.31 % Net memory used: 267.981 MB
%------------------------------------------------------------------------------