%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : ALG368-1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n003.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 : Sun Sep 27 06:50:05 AM UTC 2026
% Result : Unsatisfiable 18.21s 2.78s
% Output : CNFRefutation 18.21s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 10
% Syntax : Number of formulae : 33 ( 16 unt; 0 def)
% Number of atoms : 54 ( 10 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 50 ( 29 ~; 21 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 2 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 7 ( 5 usr; 1 prp; 0-3 aty)
% Number of functors : 12 ( 12 usr; 5 con; 0-3 aty)
% Number of variables : 30 ( 10 sgn 9 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(cls_zero__less__power_0,axiom,
! [VAR_0,VAR_1,VAR_2] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(VAR_0),VAR_1,VAR_0)
| c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(VAR_0),c_Power_Opower__class_Opower(VAR_1,VAR_2,VAR_0),VAR_0)
| ~ class_Ring__and__Field_Oordered__semidom(VAR_0) ),
file('theBenchmark.p',cls_zero__less__power_0) ).
cnf(c_106,plain,
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(A),B,A)
| c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(A),c_Power_Opower__class_Opower(B,C,A),A)
| ~ class_Ring__and__Field_Oordered__semidom(A) ),
inference(clausify,[status(thm)],[cls_zero__less__power_0]) ).
fof(clsarity_RealDef__Oreal__Ring__and__Field_Oordered__semidom,axiom,
class_Ring__and__Field_Oordered__semidom(tc_RealDef_Oreal),
file('theBenchmark.p',clsarity_RealDef__Oreal__Ring__and__Field_Oordered__semidom) ).
cnf(c_114,plain,
class_Ring__and__Field_Oordered__semidom(tc_RealDef_Oreal),
inference(clausify,[status(thm)],[clsarity_RealDef__Oreal__Ring__and__Field_Oordered__semidom]) ).
fof(clsarity_Complex__Ocomplex__RealVector_Oreal__normed__vector,axiom,
class_RealVector_Oreal__normed__vector(tc_Complex_Ocomplex),
file('theBenchmark.p',clsarity_Complex__Ocomplex__RealVector_Oreal__normed__vector) ).
cnf(c_139,plain,
class_RealVector_Oreal__normed__vector(tc_Complex_Ocomplex),
inference(clausify,[status(thm)],[clsarity_Complex__Ocomplex__RealVector_Oreal__normed__vector]) ).
fof(cls_norm__zero_0,axiom,
! [VAR_0] :
( c_RealVector_Onorm__class_Onorm(c_HOL_Ozero__class_Ozero(VAR_0),VAR_0) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)
| ~ class_RealVector_Oreal__normed__vector(VAR_0) ),
file('theBenchmark.p',cls_norm__zero_0) ).
cnf(c_144,plain,
( c_RealVector_Onorm__class_Onorm(c_HOL_Ozero__class_Ozero(A),A) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)
| ~ class_RealVector_Oreal__normed__vector(A) ),
inference(clausify,[status(thm)],[cls_norm__zero_0]) ).
fof(clsarity_Complex__Ocomplex__Int_Onumber__ring,axiom,
class_Int_Onumber__ring(tc_Complex_Ocomplex),
file('theBenchmark.p',clsarity_Complex__Ocomplex__Int_Onumber__ring) ).
cnf(c_292,plain,
class_Int_Onumber__ring(tc_Complex_Ocomplex),
inference(clausify,[status(thm)],[clsarity_Complex__Ocomplex__Int_Onumber__ring]) ).
fof(cls_class__ringb_Osubr0__iff_1,axiom,
! [VAR_0,VAR_1] :
( c_HOL_Ominus__class_Ominus(VAR_1,VAR_1,VAR_0) = c_HOL_Ozero__class_Ozero(VAR_0)
| ~ class_Int_Onumber__ring(VAR_0)
| ~ class_Ring__and__Field_Oidom(VAR_0) ),
file('theBenchmark.p',cls_class__ringb_Osubr0__iff_1) ).
cnf(c_294,plain,
( c_HOL_Ominus__class_Ominus(B,B,A) = c_HOL_Ozero__class_Ozero(A)
| ~ class_Int_Onumber__ring(A)
| ~ class_Ring__and__Field_Oidom(A) ),
inference(clausify,[status(thm)],[cls_class__ringb_Osubr0__iff_1]) ).
cnf(c_524,plain,
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),A,tc_RealDef_Oreal)
| c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_Power_Opower__class_Opower(A,B,tc_RealDef_Oreal),tc_RealDef_Oreal) ),
inference(resolve,[status(thm)],[c_114,c_106]) ).
fof(clsarity_Complex__Ocomplex__Ring__and__Field_Oidom,axiom,
class_Ring__and__Field_Oidom(tc_Complex_Ocomplex),
file('theBenchmark.p',clsarity_Complex__Ocomplex__Ring__and__Field_Oidom) ).
cnf(c_655,plain,
class_Ring__and__Field_Oidom(tc_Complex_Ocomplex),
inference(clausify,[status(thm)],[clsarity_Complex__Ocomplex__Ring__and__Field_Oidom]) ).
fof(cls_conjecture_2,axiom,
! [VAR_0] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),VAR_0,tc_RealDef_Oreal)
| ~ c_HOL_Oord__class_Oless(c_RealVector_Onorm__class_Onorm(c_HOL_Ominus__class_Ominus(c_Polynomial_Opoly(c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),c_HOL_Ominus__class_Ominus(hAPP(v_x,VAR_0),v_z,tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_Polynomial_Opoly(c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),c_HOL_Ominus__class_Ominus(v_z,v_z,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),v_e,tc_RealDef_Oreal) ),
file('theBenchmark.p',cls_conjecture_2) ).
cnf(c_728,plain,
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),A,tc_RealDef_Oreal)
| ~ c_HOL_Oord__class_Oless(c_RealVector_Onorm__class_Onorm(c_HOL_Ominus__class_Ominus(c_Polynomial_Opoly(c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),c_HOL_Ominus__class_Ominus(hAPP(v_x,A),v_z,tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_Polynomial_Opoly(c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),c_HOL_Ominus__class_Ominus(v_z,v_z,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),v_e,tc_RealDef_Oreal) ),
inference(clausify,[status(thm)],[cls_conjecture_2]) ).
fof(cls_CHAINED_0,axiom,
c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),v_e,tc_RealDef_Oreal),
file('theBenchmark.p',cls_CHAINED_0) ).
cnf(c_731,plain,
c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),v_e,tc_RealDef_Oreal),
inference(clausify,[status(thm)],[cls_CHAINED_0]) ).
fof(cls_order__root_1,axiom,
! [VAR_0,VAR_1] :
( c_Polynomial_Opoly(c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(VAR_0)),VAR_1,VAR_0) = c_HOL_Ozero__class_Ozero(VAR_0)
| ~ class_Ring__and__Field_Oidom(VAR_0) ),
file('theBenchmark.p',cls_order__root_1) ).
cnf(c_740,plain,
( c_Polynomial_Opoly(c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(A)),B,A) = c_HOL_Ozero__class_Ozero(A)
| ~ class_Ring__and__Field_Oidom(A) ),
inference(clausify,[status(thm)],[cls_order__root_1]) ).
cnf(c_1411,plain,
c_RealVector_Onorm__class_Onorm(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),
inference(resolve,[status(thm)],[c_144,c_139]) ).
cnf(c_1486,plain,
( c_HOL_Ominus__class_Ominus(A,A,tc_Complex_Ocomplex) = c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)
| ~ class_Ring__and__Field_Oidom(tc_Complex_Ocomplex) ),
inference(resolve,[status(thm)],[c_294,c_292]) ).
cnf(c_1487,plain,
c_HOL_Ominus__class_Ominus(A,A,tc_Complex_Ocomplex) = c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),
inference(resolve,[status(thm)],[c_655,c_1486]) ).
cnf(c_2148,plain,
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),A,tc_RealDef_Oreal)
| ~ c_HOL_Oord__class_Oless(c_RealVector_Onorm__class_Onorm(c_HOL_Ominus__class_Ominus(c_Polynomial_Opoly(c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),c_HOL_Ominus__class_Ominus(hAPP(v_x,A),v_z,tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_Polynomial_Opoly(c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),v_e,tc_RealDef_Oreal) ),
inference(paramod,[status(thm)],[c_1487,c_728]) ).
cnf(c_2446,plain,
c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_Power_Opower__class_Opower(v_e,A,tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(resolve,[status(thm)],[c_731,c_524]) ).
cnf(c_2472,plain,
c_Polynomial_Opoly(c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),A,tc_Complex_Ocomplex) = c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),
inference(resolve,[status(thm)],[c_740,c_655]) ).
cnf(c_2475,plain,
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),A,tc_RealDef_Oreal)
| ~ c_HOL_Oord__class_Oless(c_RealVector_Onorm__class_Onorm(c_HOL_Ominus__class_Ominus(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),c_Polynomial_Opoly(c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),v_e,tc_RealDef_Oreal) ),
inference(paramod,[status(thm)],[c_2472,c_2148]) ).
cnf(c_2476,plain,
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),A,tc_RealDef_Oreal)
| ~ c_HOL_Oord__class_Oless(c_RealVector_Onorm__class_Onorm(c_HOL_Ominus__class_Ominus(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),v_e,tc_RealDef_Oreal) ),
inference(paramod,[status(thm)],[c_2472,c_2475]) ).
cnf(c_2477,plain,
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),A,tc_RealDef_Oreal)
| ~ c_HOL_Oord__class_Oless(c_RealVector_Onorm__class_Onorm(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex),v_e,tc_RealDef_Oreal) ),
inference(paramod,[status(thm)],[c_1487,c_2476]) ).
cnf(c_2478,plain,
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),A,tc_RealDef_Oreal)
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),v_e,tc_RealDef_Oreal) ),
inference(paramod,[status(thm)],[c_1411,c_2477]) ).
cnf(c_2473,plain,
~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),A,tc_RealDef_Oreal),
inference(resolve,[status(thm)],[c_731,c_2478]) ).
cnf(c_2474,plain,
$false,
inference(resolve,[status(thm)],[c_2473,c_2446]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : ALG368-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.03 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n003.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Sat Sep 26 21:57:09 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.08/0.35 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.08/0.35 % Process 3846482 was started by sandbox2 on n003,
% 0.08/0.35 % Sat Sep 26 21:57:09 2026
% 0.08/0.35 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.13/0.41
% 0.13/0.41 % From the command line: assign(max_seconds, 300).
% 18.21/2.78
% 18.21/2.78 % SZS status Unsatisfiable for theBenchmark
% 18.21/2.78
% 18.21/2.78 % Proof 1 at 2.27 (+ 0.06) seconds.
% 18.21/2.78 % Length of proof is 19.
% 18.21/2.78 % Level of proof is 5.
% 18.21/2.78 % Maximum clause weight is 32.000.
% 18.21/2.78 % Given clauses 191.
% 18.21/2.78
% 18.21/2.78 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------