%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SWV629-1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/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 03:13:49 PM UTC 2026
% Result : Unsatisfiable 8.68s 1.67s
% Output : Proof 8.68s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 16
% Syntax : Number of formulae : 74 ( 50 unt; 0 def)
% Number of atoms : 110 ( 62 equ)
% Maximal formula atoms : 5 ( 1 avg)
% Number of connectives : 120 ( 84 ~; 36 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 3 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 11 ( 9 usr; 1 prp; 0-2 aty)
% Number of functors : 13 ( 13 usr; 5 con; 0-4 aty)
% Number of variables : 62 ( 10 sgn 24 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(f311,axiom,
( c_Power_Opower__class_Opower(V_x,c_HOL_Oone__class_Oone(tc_nat),T_a) = V_x
| ~ class_Ring__and__Field_Ocomm__semiring__1(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_class__semiring_Osemiring__rules_I33_J_0) ).
fof(f311_nnf,plain,
! [T_a,V_x] :
( c_Power_Opower__class_Opower(V_x,c_HOL_Oone__class_Oone(tc_nat),T_a) = V_x
| ~ class_Ring__and__Field_Ocomm__semiring__1(T_a) ),
inference(nnf_transformation,[status(thm)],[f311]) ).
fof(f311_sk,plain,
! [T_a,V_x] :
( c_Power_Opower__class_Opower(V_x,c_HOL_Oone__class_Oone(tc_nat),T_a) = V_x
| ~ class_Ring__and__Field_Ocomm__semiring__1(T_a) ),
inference(skolemisation,[status(esa)],[f311_nnf]) ).
cnf(c311,plain,
( c_Power_Opower__class_Opower(X1,c_HOL_Oone__class_Oone(tc_nat),X0) = X1
| ~ class_Ring__and__Field_Ocomm__semiring__1(X0) ),
inference(cnf_transformation,[status(esa)],[f311_sk]) ).
cnf(t70,plain,
ifeq(class_Ring__and__Field_Ocomm__semiring__1(X1),true,c_Power_Opower__class_Opower(X2,c_HOL_Oone__class_Oone(tc_nat),X1),X2) = X2,
inference(equality_encoding,[status(esa)],[c311]) ).
cnf(t251,plain,
ifeq(class_Ring__and__Field_Ocomm__semiring__1(X1),true,c_Power_Opower__class_Opower(X2,c_HOL_Oone__class_Oone(tc_nat),X1),X2) = X2,
inference(orient,[status(thm)],[t70]) ).
cnf(f333,axiom,
c_Power_Opower__class_Opower(c_FFT__Mirabelle_Oroot(V_n),V_n,tc_Complex_Ocomplex) = c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_root__unity_0) ).
fof(f333_nnf,plain,
! [V_n] : c_Power_Opower__class_Opower(c_FFT__Mirabelle_Oroot(V_n),V_n,tc_Complex_Ocomplex) = c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),
inference(nnf_transformation,[status(thm)],[f333]) ).
fof(f333_sk,plain,
! [V_n] : c_Power_Opower__class_Opower(c_FFT__Mirabelle_Oroot(V_n),V_n,tc_Complex_Ocomplex) = c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),
inference(skolemisation,[status(esa)],[f333_nnf]) ).
cnf(c333,plain,
c_Power_Opower__class_Opower(c_FFT__Mirabelle_Oroot(X0),X0,tc_Complex_Ocomplex) = c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),
inference(cnf_transformation,[status(esa)],[f333_sk]) ).
cnf(t32,plain,
c_Power_Opower__class_Opower(c_FFT__Mirabelle_Oroot(X1),X1,tc_Complex_Ocomplex) = c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),
inference(equality_encoding,[status(esa)],[c333]) ).
cnf(t2503,plain,
c_Power_Opower__class_Opower(c_FFT__Mirabelle_Oroot(X1),X1,tc_Complex_Ocomplex) = c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),
inference(orient,[status(thm)],[t32]) ).
cnf(t2508,plain,
c_FFT__Mirabelle_Oroot(c_HOL_Oone__class_Oone(tc_nat)) = ifeq(class_Ring__and__Field_Ocomm__semiring__1(tc_Complex_Ocomplex),true,c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),c_FFT__Mirabelle_Oroot(c_HOL_Oone__class_Oone(tc_nat))),
inference(cp,[status(thm)],[t251,t2503]) ).
cnf(f371,axiom,
class_Ring__and__Field_Ocomm__semiring__1(tc_Complex_Ocomplex),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clsarity_Complex__Ocomplex__Ring__and__Field_Ocomm__semiring__1) ).
fof(f371_nnf,plain,
class_Ring__and__Field_Ocomm__semiring__1(tc_Complex_Ocomplex),
inference(nnf_transformation,[status(thm)],[f371]) ).
cnf(c371,plain,
class_Ring__and__Field_Ocomm__semiring__1(tc_Complex_Ocomplex),
inference(cnf_transformation,[status(esa)],[f371_nnf]) ).
cnf(t0,plain,
class_Ring__and__Field_Ocomm__semiring__1(tc_Complex_Ocomplex) = true,
inference(equality_encoding,[status(esa)],[c371]) ).
cnf(t1663,plain,
class_Ring__and__Field_Ocomm__semiring__1(tc_Complex_Ocomplex) = true,
inference(orient,[status(thm)],[t0]) ).
cnf(t2839,plain,
c_FFT__Mirabelle_Oroot(c_HOL_Oone__class_Oone(tc_nat)) = ifeq(true,true,c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),c_FFT__Mirabelle_Oroot(c_HOL_Oone__class_Oone(tc_nat))),
inference(step,[status(thm)],[t2508,t1663]) ).
cnf(t22,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t241,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t22]) ).
cnf(t2840,plain,
c_FFT__Mirabelle_Oroot(c_HOL_Oone__class_Oone(tc_nat)) = c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),
inference(step,[status(thm)],[t2839,t241]) ).
cnf(t2830,plain,
c_FFT__Mirabelle_Oroot(c_HOL_Oone__class_Oone(tc_nat)) = c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),
inference(orient,[status(thm)],[t2840]) ).
cnf(t4,plain,
eq(X1,X1) = true,
introduced(definition) ).
cnf(t1615,plain,
eq(X1,X1) = true,
inference(orient,[status(thm)],[t4]) ).
cnf(f100,axiom,
c_Fact_Ofact__class_Ofact(V_n,tc_nat) != c_HOL_Ozero__class_Ozero(tc_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_fact__nonzero__nat_0) ).
fof(f100_nnf,plain,
! [V_n] : c_Fact_Ofact__class_Ofact(V_n,tc_nat) != c_HOL_Ozero__class_Ozero(tc_nat),
inference(nnf_transformation,[status(thm)],[f100]) ).
fof(f100_sk,plain,
! [V_n] : c_Fact_Ofact__class_Ofact(V_n,tc_nat) != c_HOL_Ozero__class_Ozero(tc_nat),
inference(skolemisation,[status(esa)],[f100_nnf]) ).
cnf(c100,plain,
c_Fact_Ofact__class_Ofact(X0,tc_nat) != c_HOL_Ozero__class_Ozero(tc_nat),
inference(cnf_transformation,[status(esa)],[f100_sk]) ).
cnf(f156,axiom,
( c_Power_Opower__class_Opower(V_a,c_HOL_Ozero__class_Ozero(tc_nat),T_a) != c_HOL_Ozero__class_Ozero(T_a)
| ~ class_Power_Opower(T_a)
| ~ class_Ring__and__Field_Omult__zero(T_a)
| ~ class_Ring__and__Field_Ono__zero__divisors(T_a)
| ~ class_Ring__and__Field_Ozero__neq__one(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_power__eq__0__iff_1) ).
fof(f156_nnf,plain,
! [T_a,V_a] :
( c_Power_Opower__class_Opower(V_a,c_HOL_Ozero__class_Ozero(tc_nat),T_a) != c_HOL_Ozero__class_Ozero(T_a)
| ~ class_Power_Opower(T_a)
| ~ class_Ring__and__Field_Omult__zero(T_a)
| ~ class_Ring__and__Field_Ono__zero__divisors(T_a)
| ~ class_Ring__and__Field_Ozero__neq__one(T_a) ),
inference(nnf_transformation,[status(thm)],[f156]) ).
fof(f156_sk,plain,
! [T_a,V_a] :
( c_Power_Opower__class_Opower(V_a,c_HOL_Ozero__class_Ozero(tc_nat),T_a) != c_HOL_Ozero__class_Ozero(T_a)
| ~ class_Power_Opower(T_a)
| ~ class_Ring__and__Field_Omult__zero(T_a)
| ~ class_Ring__and__Field_Ono__zero__divisors(T_a)
| ~ class_Ring__and__Field_Ozero__neq__one(T_a) ),
inference(skolemisation,[status(esa)],[f156_nnf]) ).
cnf(c156,plain,
( c_Power_Opower__class_Opower(X1,c_HOL_Ozero__class_Ozero(tc_nat),X0) != c_HOL_Ozero__class_Ozero(X0)
| ~ class_Power_Opower(X0)
| ~ class_Ring__and__Field_Omult__zero(X0)
| ~ class_Ring__and__Field_Ono__zero__divisors(X0)
| ~ class_Ring__and__Field_Ozero__neq__one(X0) ),
inference(cnf_transformation,[status(esa)],[f156_sk]) ).
cnf(f181,axiom,
( c_Nat_Osemiring__1__class_Oof__nat(c_Fact_Ofact__class_Ofact(V_n,tc_nat),T_a) != c_HOL_Ozero__class_Ozero(T_a)
| ~ class_Nat_Osemiring__char__0(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_of__nat__fact__not__zero_0) ).
fof(f181_nnf,plain,
! [T_a,V_n] :
( c_Nat_Osemiring__1__class_Oof__nat(c_Fact_Ofact__class_Ofact(V_n,tc_nat),T_a) != c_HOL_Ozero__class_Ozero(T_a)
| ~ class_Nat_Osemiring__char__0(T_a) ),
inference(nnf_transformation,[status(thm)],[f181]) ).
fof(f181_sk,plain,
! [T_a,V_n] :
( c_Nat_Osemiring__1__class_Oof__nat(c_Fact_Ofact__class_Ofact(V_n,tc_nat),T_a) != c_HOL_Ozero__class_Ozero(T_a)
| ~ class_Nat_Osemiring__char__0(T_a) ),
inference(skolemisation,[status(esa)],[f181_nnf]) ).
cnf(c181,plain,
( c_Nat_Osemiring__1__class_Oof__nat(c_Fact_Ofact__class_Ofact(X1,tc_nat),X0) != c_HOL_Ozero__class_Ozero(X0)
| ~ class_Nat_Osemiring__char__0(X0) ),
inference(cnf_transformation,[status(esa)],[f181_sk]) ).
cnf(f273,axiom,
c_Complex_Oii != c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_complex__i__not__zero_0) ).
fof(f273_nnf,plain,
c_Complex_Oii != c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),
inference(nnf_transformation,[status(thm)],[f273]) ).
fof(f273_sk,plain,
c_Complex_Oii != c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),
inference(skolemisation,[status(esa)],[f273_nnf]) ).
cnf(c273,plain,
c_Complex_Oii != c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),
inference(cnf_transformation,[status(esa)],[f273_sk]) ).
cnf(f304,axiom,
c_FFT__Mirabelle_Oroot(V_n) != c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_root__nonzero_0) ).
fof(f304_nnf,plain,
! [V_n] : c_FFT__Mirabelle_Oroot(V_n) != c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),
inference(nnf_transformation,[status(thm)],[f304]) ).
fof(f304_sk,plain,
! [V_n] : c_FFT__Mirabelle_Oroot(V_n) != c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),
inference(skolemisation,[status(esa)],[f304_nnf]) ).
cnf(c304,plain,
c_FFT__Mirabelle_Oroot(X0) != c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),
inference(cnf_transformation,[status(esa)],[f304_sk]) ).
cnf(f305,axiom,
( ~ c_Int_Oiszero(c_HOL_Oone__class_Oone(T_a),T_a)
| ~ class_Ring__and__Field_Osemiring__1(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_not__iszero__1_0) ).
fof(f305_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)],[f305]) ).
fof(f305_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)],[f305_nnf]) ).
cnf(c305,plain,
( ~ c_Int_Oiszero(c_HOL_Oone__class_Oone(X0),X0)
| ~ class_Ring__and__Field_Osemiring__1(X0) ),
inference(cnf_transformation,[status(esa)],[f305_sk]) ).
cnf(f312,axiom,
c_Complex_Oii != c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_complex__i__not__one_0) ).
fof(f312_nnf,plain,
c_Complex_Oii != c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),
inference(nnf_transformation,[status(thm)],[f312]) ).
fof(f312_sk,plain,
c_Complex_Oii != c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),
inference(skolemisation,[status(esa)],[f312_nnf]) ).
cnf(c312,plain,
c_Complex_Oii != c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),
inference(cnf_transformation,[status(esa)],[f312_sk]) ).
cnf(f321,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/sandbox/benchmark/theBenchmark.p',cls_zero__neq__one_0) ).
fof(f321_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)],[f321]) ).
fof(f321_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)],[f321_nnf]) ).
cnf(c321,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)],[f321_sk]) ).
cnf(f325,axiom,
~ c_Parity_Oeven__odd__class_Oeven(c_HOL_Oone__class_Oone(tc_nat),tc_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_odd__1__nat_0) ).
fof(f325_nnf,plain,
~ c_Parity_Oeven__odd__class_Oeven(c_HOL_Oone__class_Oone(tc_nat),tc_nat),
inference(nnf_transformation,[status(thm)],[f325]) ).
fof(f325_sk,plain,
~ c_Parity_Oeven__odd__class_Oeven(c_HOL_Oone__class_Oone(tc_nat),tc_nat),
inference(skolemisation,[status(esa)],[f325_nnf]) ).
cnf(c325,plain,
~ c_Parity_Oeven__odd__class_Oeven(c_HOL_Oone__class_Oone(tc_nat),tc_nat),
inference(cnf_transformation,[status(esa)],[f325_sk]) ).
cnf(f334,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/sandbox/benchmark/theBenchmark.p',cls_one__neq__zero_0) ).
fof(f334_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)],[f334]) ).
fof(f334_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)],[f334_nnf]) ).
cnf(c334,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)],[f334_sk]) ).
cnf(f351,negated_conjecture,
c_FFT__Mirabelle_Oroot(c_HOL_Oone__class_Oone(tc_nat)) != c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_0) ).
fof(f351_nnf,plain,
c_FFT__Mirabelle_Oroot(c_HOL_Oone__class_Oone(tc_nat)) != c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),
inference(nnf_transformation,[status(thm)],[f351]) ).
fof(f351_sk,plain,
c_FFT__Mirabelle_Oroot(c_HOL_Oone__class_Oone(tc_nat)) != c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),
inference(skolemisation,[status(esa)],[f351_nnf]) ).
cnf(c351,plain,
c_FFT__Mirabelle_Oroot(c_HOL_Oone__class_Oone(tc_nat)) != c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),
inference(cnf_transformation,[status(esa)],[f351_sk]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c100,c156,c181,c273,c304,c305,c312,c321,c325,c334,c351]) ).
cnf(g0_0,plain,
eq(c_FFT__Mirabelle_Oroot(c_HOL_Oone__class_Oone(tc_nat)),c_HOL_Oone__class_Oone(tc_Complex_Ocomplex)) != false,
inference(rw,[status(thm)],[goal_0]) ).
cnf(g0_1,plain,
eq(c_FFT__Mirabelle_Oroot(c_HOL_Oone__class_Oone(tc_nat)),c_FFT__Mirabelle_Oroot(c_HOL_Oone__class_Oone(tc_nat))) != false,
inference(rw,[status(thm)],[g0_0,t2830]) ).
cnf(g0_2,plain,
true != false,
inference(rw,[status(thm)],[g0_1,t1615]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_2]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV629-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.08/0.35 % Computer : n020.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 : Thu Sep 24 20:46:33 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.08/0.36 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 8.68/1.67 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 8.68/1.67 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------