%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : ALG417-1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 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 : Fri Sep 25 12:52:30 PM UTC 2026
% Result : Unsatisfiable 22.50s 3.34s
% Output : Proof 22.50s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 12
% Syntax : Number of formulae : 58 ( 38 unt; 0 def)
% Number of atoms : 82 ( 50 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 80 ( 56 ~; 24 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 2 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 8 ( 6 usr; 1 prp; 0-2 aty)
% Number of functors : 13 ( 13 usr; 6 con; 0-4 aty)
% Number of variables : 27 ( 2 sgn 12 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(f355,axiom,
v_s____ = c_Polynomial_OpCons(v_k____,c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Complex_Ocomplex),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_kpn_0) ).
fof(f355_nnf,plain,
v_s____ = c_Polynomial_OpCons(v_k____,c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Complex_Ocomplex),
inference(nnf_transformation,[status(thm)],[f355]) ).
cnf(c355,plain,
v_s____ = c_Polynomial_OpCons(v_k____,c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Complex_Ocomplex),
inference(cnf_transformation,[status(esa)],[f355_nnf]) ).
cnf(t35,plain,
c_Polynomial_OpCons(v_k____,c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Complex_Ocomplex) = v_s____,
inference(equality_encoding,[status(esa)],[c355]) ).
cnf(f226,axiom,
( c_Polynomial_OpCons(c_HOL_Ozero__class_Ozero(T_a),c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a)),T_a) = c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a))
| ~ class_HOL_Ozero(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_pCons__0__0_0) ).
fof(f226_nnf,plain,
! [T_a] :
( c_Polynomial_OpCons(c_HOL_Ozero__class_Ozero(T_a),c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a)),T_a) = c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a))
| ~ class_HOL_Ozero(T_a) ),
inference(nnf_transformation,[status(thm)],[f226]) ).
fof(f226_sk,plain,
! [T_a] :
( c_Polynomial_OpCons(c_HOL_Ozero__class_Ozero(T_a),c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a)),T_a) = c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a))
| ~ class_HOL_Ozero(T_a) ),
inference(skolemisation,[status(esa)],[f226_nnf]) ).
cnf(c226,plain,
( c_Polynomial_OpCons(c_HOL_Ozero__class_Ozero(X0),c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(X0)),X0) = c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(X0))
| ~ class_HOL_Ozero(X0) ),
inference(cnf_transformation,[status(esa)],[f226_sk]) ).
cnf(hi226,axiom,
ifeq(class_HOL_Ozero(X0),true,c_Polynomial_OpCons(c_HOL_Ozero__class_Ozero(X0),c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(X0)),X0),c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(X0))) = c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(X0)),
inference(equality_encoding,[status(esa)],[c226]) ).
cnf(f503,axiom,
class_HOL_Ozero(tc_Complex_Ocomplex),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clsarity_Complex__Ocomplex__HOL_Ozero) ).
fof(f503_nnf,plain,
class_HOL_Ozero(tc_Complex_Ocomplex),
inference(nnf_transformation,[status(thm)],[f503]) ).
cnf(c503,plain,
class_HOL_Ozero(tc_Complex_Ocomplex),
inference(cnf_transformation,[status(esa)],[f503_nnf]) ).
cnf(hi496,axiom,
class_HOL_Ozero(tc_Complex_Ocomplex) = true,
inference(equality_encoding,[status(esa)],[c503]) ).
cnf(t62,plain,
c_Polynomial_OpCons(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Complex_Ocomplex) = c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),
inference(hyper_resolution,[status(thm)],[hi226,hi496]) ).
cnf(f409,negated_conjecture,
v_k____ = c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_0) ).
fof(f409_nnf,plain,
v_k____ = c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),
inference(nnf_transformation,[status(thm)],[f409]) ).
cnf(c409,plain,
v_k____ = c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),
inference(cnf_transformation,[status(esa)],[f409_nnf]) ).
cnf(t0,plain,
c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) = v_k____,
inference(equality_encoding,[status(esa)],[c409]) ).
cnf(t1361,plain,
c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) = v_k____,
inference(orient,[status(thm)],[t0]) ).
cnf(t1606,plain,
c_Polynomial_OpCons(v_k____,c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Complex_Ocomplex) = c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),
inference(step,[status(thm)],[t62,t1361]) ).
cnf(t1413,plain,
c_Polynomial_OpCons(v_k____,c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Complex_Ocomplex) = c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),
inference(orient,[status(thm)],[t1606]) ).
cnf(t1609,plain,
c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)) = v_s____,
inference(step,[status(thm)],[t35,t1413]) ).
cnf(t1550,plain,
c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)) = v_s____,
inference(orient,[status(thm)],[t1609]) ).
cnf(t13,plain,
eq(X1,X1) = true,
introduced(definition) ).
cnf(t666,plain,
eq(X1,X1) = true,
inference(orient,[status(thm)],[t13]) ).
cnf(f298,axiom,
v_s____ != c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_sne_0) ).
fof(f298_nnf,plain,
v_s____ != c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),
inference(nnf_transformation,[status(thm)],[f298]) ).
fof(f298_sk,plain,
v_s____ != c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),
inference(skolemisation,[status(esa)],[f298_nnf]) ).
cnf(c298,plain,
v_s____ != c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),
inference(cnf_transformation,[status(esa)],[f298_sk]) ).
cnf(f314,axiom,
( ~ c_Int_Oiszero(c_HOL_Oone__class_Oone(T_a),T_a)
| ~ class_Ring__and__Field_Osemiring__1(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_not__iszero__1_0) ).
fof(f314_nnf,plain,
! [T_a] :
( ~ c_Int_Oiszero(c_HOL_Oone__class_Oone(T_a),T_a)
| ~ class_Ring__and__Field_Osemiring__1(T_a) ),
inference(nnf_transformation,[status(thm)],[f314]) ).
fof(f314_sk,plain,
! [T_a] :
( ~ c_Int_Oiszero(c_HOL_Oone__class_Oone(T_a),T_a)
| ~ class_Ring__and__Field_Osemiring__1(T_a) ),
inference(skolemisation,[status(esa)],[f314_nnf]) ).
cnf(c314,plain,
( ~ c_Int_Oiszero(c_HOL_Oone__class_Oone(X0),X0)
| ~ class_Ring__and__Field_Osemiring__1(X0) ),
inference(cnf_transformation,[status(esa)],[f314_sk]) ).
cnf(f329,axiom,
c_Complex_Oii != c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_complex__i__not__zero_0) ).
fof(f329_nnf,plain,
c_Complex_Oii != c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),
inference(nnf_transformation,[status(thm)],[f329]) ).
fof(f329_sk,plain,
c_Complex_Oii != c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),
inference(skolemisation,[status(esa)],[f329_nnf]) ).
cnf(c329,plain,
c_Complex_Oii != c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),
inference(cnf_transformation,[status(esa)],[f329_sk]) ).
cnf(f356,axiom,
( c_HOL_Ozero__class_Ozero(T_a) != c_HOL_Oone__class_Oone(T_a)
| ~ class_Ring__and__Field_Ozero__neq__one(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_zero__neq__one_0) ).
fof(f356_nnf,plain,
! [T_a] :
( c_HOL_Ozero__class_Ozero(T_a) != c_HOL_Oone__class_Oone(T_a)
| ~ class_Ring__and__Field_Ozero__neq__one(T_a) ),
inference(nnf_transformation,[status(thm)],[f356]) ).
fof(f356_sk,plain,
! [T_a] :
( c_HOL_Ozero__class_Ozero(T_a) != c_HOL_Oone__class_Oone(T_a)
| ~ class_Ring__and__Field_Ozero__neq__one(T_a) ),
inference(skolemisation,[status(esa)],[f356_nnf]) ).
cnf(c356,plain,
( c_HOL_Ozero__class_Ozero(X0) != c_HOL_Oone__class_Oone(X0)
| ~ class_Ring__and__Field_Ozero__neq__one(X0) ),
inference(cnf_transformation,[status(esa)],[f356_sk]) ).
cnf(f368,axiom,
( c_HOL_Oone__class_Oone(T_a) != c_HOL_Ozero__class_Ozero(T_a)
| ~ class_Ring__and__Field_Ozero__neq__one(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_one__neq__zero_0) ).
fof(f368_nnf,plain,
! [T_a] :
( c_HOL_Oone__class_Oone(T_a) != c_HOL_Ozero__class_Ozero(T_a)
| ~ class_Ring__and__Field_Ozero__neq__one(T_a) ),
inference(nnf_transformation,[status(thm)],[f368]) ).
fof(f368_sk,plain,
! [T_a] :
( c_HOL_Oone__class_Oone(T_a) != c_HOL_Ozero__class_Ozero(T_a)
| ~ class_Ring__and__Field_Ozero__neq__one(T_a) ),
inference(skolemisation,[status(esa)],[f368_nnf]) ).
cnf(c368,plain,
( c_HOL_Oone__class_Oone(X0) != c_HOL_Ozero__class_Ozero(X0)
| ~ class_Ring__and__Field_Ozero__neq__one(X0) ),
inference(cnf_transformation,[status(esa)],[f368_sk]) ).
cnf(f398,axiom,
( c_Transcendental_Oexp(V_x,T_a) != c_HOL_Ozero__class_Ozero(T_a)
| ~ class_RealVector_Oreal__normed__field(T_a)
| ~ class_SEQ_Obanach(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_exp__not__eq__zero_0) ).
fof(f398_nnf,plain,
! [T_a,V_x] :
( c_Transcendental_Oexp(V_x,T_a) != c_HOL_Ozero__class_Ozero(T_a)
| ~ class_RealVector_Oreal__normed__field(T_a)
| ~ class_SEQ_Obanach(T_a) ),
inference(nnf_transformation,[status(thm)],[f398]) ).
fof(f398_sk,plain,
! [T_a,V_x] :
( c_Transcendental_Oexp(V_x,T_a) != c_HOL_Ozero__class_Ozero(T_a)
| ~ class_RealVector_Oreal__normed__field(T_a)
| ~ class_SEQ_Obanach(T_a) ),
inference(skolemisation,[status(esa)],[f398_nnf]) ).
cnf(c398,plain,
( c_Transcendental_Oexp(X1,X0) != c_HOL_Ozero__class_Ozero(X0)
| ~ class_RealVector_Oreal__normed__field(X0)
| ~ class_SEQ_Obanach(X0) ),
inference(cnf_transformation,[status(esa)],[f398_sk]) ).
cnf(f408,axiom,
v_s____ != c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_CHAINED_0_01) ).
fof(f408_nnf,plain,
v_s____ != c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),
inference(nnf_transformation,[status(thm)],[f408]) ).
fof(f408_sk,plain,
v_s____ != c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),
inference(skolemisation,[status(esa)],[f408_nnf]) ).
cnf(c408,plain,
v_s____ != c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),
inference(cnf_transformation,[status(esa)],[f408_sk]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c298,c314,c329,c356,c368,c398,c408]) ).
cnf(g0_0,plain,
eq(v_s____,c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))) != false,
inference(rw,[status(thm)],[goal_0]) ).
cnf(g0_1,plain,
eq(v_s____,v_s____) != false,
inference(rw,[status(thm)],[g0_0,t1550]) ).
cnf(g0_2,plain,
true != false,
inference(rw,[status(thm)],[g0_1,t666]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_2]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG417-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.13/0.38 % Computer : n020.cluster.edu
% 0.13/0.38 % Model : x86_64 x86_64
% 0.13/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.38 % Memory : 8046.5625MB
% 0.13/0.38 % OS : Linux 6.8.0-71-generic
% 0.13/0.38 % CPULimit : 300
% 0.13/0.38 % WCLimit : 300
% 0.13/0.38 % DateTime : Fri Sep 25 05:37:03 UTC 2026
% 0.13/0.38 % CPUTime :
% 0.13/0.38 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 22.50/3.34 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 22.50/3.34 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------