%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWV573-1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n020.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 02:52:51 PM UTC 2026
% Result : Unsatisfiable 24.96s 3.63s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWV573-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.34 % Computer : n020.cluster.edu
% 0.08/0.34 % Model : x86_64 x86_64
% 0.08/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.34 % Memory : 8046.5625MB
% 0.08/0.34 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Mon Sep 21 09:12:03 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.12/0.44 % Drodi V4.1.1
% 24.96/3.63 % Refutation found
% 24.96/3.63 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 24.96/3.63 % SZS output start CNFRefutation for theBenchmark
% 24.96/3.63 fof(f162,axiom,(
% 24.96/3.63 c_Complex_ORe(c_Complex_Oii) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) ),
% 24.96/3.63 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 24.96/3.63 fof(f760,axiom,(
% 24.96/3.63 (![V_z]: (c_Complex_Ocomplex_OComplex(c_Complex_ORe(V_z),c_Complex_OIm(V_z)) = V_z ))),
% 24.96/3.63 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 24.96/3.63 fof(f881,axiom,(
% 24.96/3.63 c_Transcendental_Otan(c_Transcendental_Opi) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) ),
% 24.96/3.63 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 24.96/3.63 fof(f1029,axiom,(
% 24.96/3.63 c_Complex_Oii = c_Complex_Ocomplex_OComplex(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Oone__class_Oone(tc_RealDef_Oreal)) ),
% 24.96/3.63 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 24.96/3.63 fof(f1034,axiom,(
% 24.96/3.63 (![V_x,V_y]: (c_Complex_ORe(c_Complex_Ocomplex_OComplex(V_x,V_y)) = V_x ))),
% 24.96/3.63 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 24.96/3.63 fof(f1054,axiom,(
% 24.96/3.64 (![V_x]: (c_Complex_Ocomplex_OComplex(V_x,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)) = c_RealVector_Oof__real(V_x,tc_Complex_Ocomplex) ))),
% 24.96/3.64 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 24.96/3.64 fof(f1063,axiom,(
% 24.96/3.64 (![V_n]: (c_Complex_OIm(c_Nat_Osemiring__1__class_Oof__nat(V_n,tc_Complex_Ocomplex)) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) ))),
% 24.96/3.64 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 24.96/3.64 fof(f1064,axiom,(
% 24.96/3.64 (![V_n]: (c_Complex_ORe(c_Nat_Osemiring__1__class_Oof__nat(V_n,tc_Complex_Ocomplex)) = c_Nat_Osemiring__1__class_Oof__nat(V_n,tc_RealDef_Oreal) ))),
% 24.96/3.64 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 24.96/3.64 fof(f1068,negated_conjecture,(
% 24.96/3.64 c_Nat_Osemiring__1__class_Oof__nat(v_n,tc_Complex_Ocomplex) != c_Complex_Ocomplex_OComplex(c_Nat_Osemiring__1__class_Oof__nat(v_n,tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)) ),
% 24.96/3.64 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 24.96/3.64 fof(f1533,plain,(
% 24.96/3.64 c_Complex_ORe(c_Complex_Oii)=c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)),
% 24.96/3.64 inference(cnf_transformation,[status(thm)],[f162])).
% 24.96/3.64 fof(f2458,plain,(
% 24.96/3.64 ![X0]: (c_Complex_Ocomplex_OComplex(c_Complex_ORe(X0),c_Complex_OIm(X0))=X0)),
% 24.96/3.64 inference(cnf_transformation,[status(thm)],[f760])).
% 24.96/3.64 fof(f2650,plain,(
% 24.96/3.64 c_Transcendental_Otan(c_Transcendental_Opi)=c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)),
% 24.96/3.64 inference(cnf_transformation,[status(thm)],[f881])).
% 24.96/3.64 fof(f2881,plain,(
% 24.96/3.64 c_Complex_Oii=c_Complex_Ocomplex_OComplex(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Oone__class_Oone(tc_RealDef_Oreal))),
% 24.96/3.64 inference(cnf_transformation,[status(thm)],[f1029])).
% 24.96/3.64 fof(f2886,plain,(
% 24.96/3.64 ![X0,X1]: (c_Complex_ORe(c_Complex_Ocomplex_OComplex(X0,X1))=X0)),
% 24.96/3.64 inference(cnf_transformation,[status(thm)],[f1034])).
% 24.96/3.64 fof(f2917,plain,(
% 24.96/3.64 ![X0]: (c_Complex_Ocomplex_OComplex(X0,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal))=c_RealVector_Oof__real(X0,tc_Complex_Ocomplex))),
% 24.96/3.64 inference(cnf_transformation,[status(thm)],[f1054])).
% 24.96/3.64 fof(f2932,plain,(
% 24.96/3.64 ![X0]: (c_Complex_OIm(c_Nat_Osemiring__1__class_Oof__nat(X0,tc_Complex_Ocomplex))=c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal))),
% 24.96/3.64 inference(cnf_transformation,[status(thm)],[f1063])).
% 24.96/3.64 fof(f2933,plain,(
% 24.96/3.64 ![X0]: (c_Complex_ORe(c_Nat_Osemiring__1__class_Oof__nat(X0,tc_Complex_Ocomplex))=c_Nat_Osemiring__1__class_Oof__nat(X0,tc_RealDef_Oreal))),
% 24.96/3.64 inference(cnf_transformation,[status(thm)],[f1064])).
% 24.96/3.64 fof(f2940,plain,(
% 24.96/3.64 ~c_Nat_Osemiring__1__class_Oof__nat(v_n,tc_Complex_Ocomplex)=c_Complex_Ocomplex_OComplex(c_Nat_Osemiring__1__class_Oof__nat(v_n,tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal))),
% 24.96/3.64 inference(cnf_transformation,[status(thm)],[f1068])).
% 24.96/3.64 fof(f3360,plain,(
% 24.96/3.64 ~c_Nat_Osemiring__1__class_Oof__nat(v_n,tc_Complex_Ocomplex)=c_RealVector_Oof__real(c_Nat_Osemiring__1__class_Oof__nat(v_n,tc_RealDef_Oreal),tc_Complex_Ocomplex)),
% 24.96/3.64 inference(backward_demodulation,[status(thm)],[f2917,f2940])).
% 24.96/3.64 fof(f7120,plain,(
% 24.96/3.64 c_Complex_ORe(c_Complex_Oii)=c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)),
% 24.96/3.64 inference(paramodulation,[status(thm)],[f2881,f2886])).
% 24.96/3.64 fof(f7133,plain,(
% 24.96/3.66 ![X0]: (c_Complex_Ocomplex_OComplex(X0,c_Complex_ORe(c_Complex_Oii))=c_RealVector_Oof__real(X0,tc_Complex_Ocomplex))),
% 24.96/3.66 inference(backward_demodulation,[status(thm)],[f1533,f2917])).
% 24.96/3.66 fof(f7614,plain,(
% 24.96/3.66 ![X0]: (c_Complex_Ocomplex_OComplex(X0,c_Transcendental_Otan(c_Transcendental_Opi))=c_RealVector_Oof__real(X0,tc_Complex_Ocomplex))),
% 24.96/3.66 inference(backward_demodulation,[status(thm)],[f7626,f7133])).
% 24.96/3.66 fof(f7626,plain,(
% 24.96/3.66 c_Complex_ORe(c_Complex_Oii)=c_Transcendental_Otan(c_Transcendental_Opi)),
% 24.96/3.66 inference(forward_demodulation,[status(thm)],[f2650,f7120])).
% 24.96/3.66 fof(f7660,plain,(
% 24.96/3.66 ![X0]: (c_Complex_Ocomplex_OComplex(c_Nat_Osemiring__1__class_Oof__nat(X0,tc_RealDef_Oreal),c_Complex_OIm(c_Nat_Osemiring__1__class_Oof__nat(X0,tc_Complex_Ocomplex)))=c_Nat_Osemiring__1__class_Oof__nat(X0,tc_Complex_Ocomplex))),
% 24.96/3.66 inference(paramodulation,[status(thm)],[f2933,f2458])).
% 24.96/3.66 fof(f11911,plain,(
% 24.96/3.66 ![X0]: (c_Complex_Ocomplex_OComplex(c_Nat_Osemiring__1__class_Oof__nat(X0,tc_RealDef_Oreal),c_Transcendental_Otan(c_Transcendental_Opi))=c_Nat_Osemiring__1__class_Oof__nat(X0,tc_Complex_Ocomplex))),
% 24.96/3.66 inference(backward_demodulation,[status(thm)],[f11912,f7660])).
% 24.96/3.66 fof(f11912,plain,(
% 24.96/3.66 ![X0]: (c_Complex_OIm(c_Nat_Osemiring__1__class_Oof__nat(X0,tc_Complex_Ocomplex))=c_Transcendental_Otan(c_Transcendental_Opi))),
% 24.96/3.66 inference(forward_demodulation,[status(thm)],[f2650,f2932])).
% 24.96/3.66 fof(f11924,plain,(
% 24.96/3.66 ![X0]: (c_RealVector_Oof__real(c_Nat_Osemiring__1__class_Oof__nat(X0,tc_RealDef_Oreal),tc_Complex_Ocomplex)=c_Nat_Osemiring__1__class_Oof__nat(X0,tc_Complex_Ocomplex))),
% 24.96/3.66 inference(forward_demodulation,[status(thm)],[f7614,f11911])).
% 24.96/3.66 fof(f11935,plain,(
% 24.96/3.66 ~c_Nat_Osemiring__1__class_Oof__nat(v_n,tc_Complex_Ocomplex)=c_Nat_Osemiring__1__class_Oof__nat(v_n,tc_Complex_Ocomplex)),
% 24.96/3.66 inference(backward_demodulation,[status(thm)],[f11924,f3360])).
% 24.96/3.66 fof(f11951,plain,(
% 24.96/3.66 $false),
% 24.96/3.66 inference(trivial_equality_resolution,[status(thm)],[f11935])).
% 24.96/3.66 % SZS output end CNFRefutation for theBenchmark.p
% 24.96/3.68 % Elapsed time: 3.319485 seconds
% 24.96/3.68 % CPU time: 25.542003 seconds
% 24.96/3.68 % Total memory used: 333.250 MB
% 24.96/3.68 % Net memory used: 322.669 MB
%------------------------------------------------------------------------------