%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SWV618-1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /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 : Sun Sep 27 09:08:50 AM UTC 2026
% Result : Unsatisfiable 111.40s 15.47s
% Output : CNFRefutation 111.40s
% Verified :
% SZS Type : Refutation
% Derivation depth : 18
% Number of leaves : 24
% Syntax : Number of formulae : 98 ( 50 unt; 0 def)
% Number of atoms : 166 ( 99 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 137 ( 69 ~; 68 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 3 avg)
% Maximal term depth : 9 ( 2 avg)
% Number of predicates : 9 ( 7 usr; 1 prp; 0-3 aty)
% Number of functors : 16 ( 16 usr; 4 con; 0-4 aty)
% Number of variables : 117 ( 10 sgn 32 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(cls_power__one_0,axiom,
! [VAR_0,VAR_1] :
( hAPP(c_Power_Opower__class_Opower(c_HOL_Oone__class_Oone(VAR_0),VAR_0),VAR_1) = c_HOL_Oone__class_Oone(VAR_0)
| ~ class_OrderedGroup_Omonoid__mult(VAR_0) ),
file('theBenchmark.p',cls_power__one_0) ).
cnf(c_17,plain,
( hAPP(c_Power_Opower__class_Opower(c_HOL_Oone__class_Oone(A),A),B) = c_HOL_Oone__class_Oone(A)
| ~ class_OrderedGroup_Omonoid__mult(A) ),
inference(clausify,[status(thm)],[cls_power__one_0]) ).
fof(clsarity_Complex__Ocomplex__OrderedGroup_Omonoid__mult,axiom,
class_OrderedGroup_Omonoid__mult(tc_Complex_Ocomplex),
file('theBenchmark.p',clsarity_Complex__Ocomplex__OrderedGroup_Omonoid__mult) ).
cnf(c_20,plain,
class_OrderedGroup_Omonoid__mult(tc_Complex_Ocomplex),
inference(clausify,[status(thm)],[clsarity_Complex__Ocomplex__OrderedGroup_Omonoid__mult]) ).
fof(cls_power__mult_0,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3] :
( hAPP(c_Power_Opower__class_Opower(VAR_1,VAR_0),c_HOL_Otimes__class_Otimes(VAR_2,VAR_3,tc_nat)) = hAPP(c_Power_Opower__class_Opower(hAPP(c_Power_Opower__class_Opower(VAR_1,VAR_0),VAR_2),VAR_0),VAR_3)
| ~ class_OrderedGroup_Omonoid__mult(VAR_0) ),
file('theBenchmark.p',cls_power__mult_0) ).
cnf(c_22,plain,
( hAPP(c_Power_Opower__class_Opower(B,A),c_HOL_Otimes__class_Otimes(C,D,tc_nat)) = hAPP(c_Power_Opower__class_Opower(hAPP(c_Power_Opower__class_Opower(B,A),C),A),D)
| ~ class_OrderedGroup_Omonoid__mult(A) ),
inference(clausify,[status(thm)],[cls_power__mult_0]) ).
fof(cls_class__semiring_Osemiring__rules_I9_J_0,axiom,
! [VAR_0,VAR_1] :
( c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(VAR_0),VAR_1,VAR_0) = c_HOL_Ozero__class_Ozero(VAR_0)
| ~ class_Ring__and__Field_Ocomm__semiring__1(VAR_0) ),
file('theBenchmark.p',cls_class__semiring_Osemiring__rules_I9_J_0) ).
cnf(c_47,plain,
( c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(A),B,A) = c_HOL_Ozero__class_Ozero(A)
| ~ class_Ring__and__Field_Ocomm__semiring__1(A) ),
inference(clausify,[status(thm)],[cls_class__semiring_Osemiring__rules_I9_J_0]) ).
fof(clsarity_Complex__Ocomplex__Ring__and__Field_Ocomm__semiring__1,axiom,
class_Ring__and__Field_Ocomm__semiring__1(tc_Complex_Ocomplex),
file('theBenchmark.p',clsarity_Complex__Ocomplex__Ring__and__Field_Ocomm__semiring__1) ).
cnf(c_66,plain,
class_Ring__and__Field_Ocomm__semiring__1(tc_Complex_Ocomplex),
inference(clausify,[status(thm)],[clsarity_Complex__Ocomplex__Ring__and__Field_Ocomm__semiring__1]) ).
fof(clsarity_Complex__Ocomplex__Ring__and__Field_Odivision__by__zero,axiom,
class_Ring__and__Field_Odivision__by__zero(tc_Complex_Ocomplex),
file('theBenchmark.p',clsarity_Complex__Ocomplex__Ring__and__Field_Odivision__by__zero) ).
cnf(c_67,plain,
class_Ring__and__Field_Odivision__by__zero(tc_Complex_Ocomplex),
inference(clausify,[status(thm)],[clsarity_Complex__Ocomplex__Ring__and__Field_Odivision__by__zero]) ).
fof(cls_eq__divide__eq_4,axiom,
! [VAR_0,VAR_1] :
( c_HOL_Ozero__class_Ozero(VAR_0) = c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(VAR_0),VAR_1,VAR_0),VAR_1,VAR_0)
| ~ class_Ring__and__Field_Odivision__by__zero(VAR_0)
| ~ class_Ring__and__Field_Ofield(VAR_0) ),
file('theBenchmark.p',cls_eq__divide__eq_4) ).
cnf(c_84,plain,
( c_HOL_Ozero__class_Ozero(A) = c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(A),B,A),B,A)
| ~ class_Ring__and__Field_Odivision__by__zero(A)
| ~ class_Ring__and__Field_Ofield(A) ),
inference(clausify,[status(thm)],[cls_eq__divide__eq_4]) ).
fof(cls_power__inverse_0,axiom,
! [VAR_0,VAR_1,VAR_2] :
( c_HOL_Oinverse__class_Oinverse(hAPP(c_Power_Opower__class_Opower(VAR_1,VAR_0),VAR_2),VAR_0) = hAPP(c_Power_Opower__class_Opower(c_HOL_Oinverse__class_Oinverse(VAR_1,VAR_0),VAR_0),VAR_2)
| ~ class_Ring__and__Field_Odivision__by__zero(VAR_0)
| ~ class_Ring__and__Field_Odivision__ring(VAR_0) ),
file('theBenchmark.p',cls_power__inverse_0) ).
cnf(c_94,plain,
( c_HOL_Oinverse__class_Oinverse(hAPP(c_Power_Opower__class_Opower(B,A),C),A) = hAPP(c_Power_Opower__class_Opower(c_HOL_Oinverse__class_Oinverse(B,A),A),C)
| ~ class_Ring__and__Field_Odivision__by__zero(A)
| ~ class_Ring__and__Field_Odivision__ring(A) ),
inference(clausify,[status(thm)],[cls_power__inverse_0]) ).
fof(cls_inverse__eq__1__iff_1,axiom,
! [VAR_0] :
( c_HOL_Oinverse__class_Oinverse(c_HOL_Oone__class_Oone(VAR_0),VAR_0) = c_HOL_Oone__class_Oone(VAR_0)
| ~ class_Ring__and__Field_Odivision__by__zero(VAR_0)
| ~ class_Ring__and__Field_Ofield(VAR_0) ),
file('theBenchmark.p',cls_inverse__eq__1__iff_1) ).
cnf(c_96,plain,
( c_HOL_Oinverse__class_Oinverse(c_HOL_Oone__class_Oone(A),A) = c_HOL_Oone__class_Oone(A)
| ~ class_Ring__and__Field_Odivision__by__zero(A)
| ~ class_Ring__and__Field_Ofield(A) ),
inference(clausify,[status(thm)],[cls_inverse__eq__1__iff_1]) ).
fof(cls_inverse__eq__iff__eq_0,axiom,
! [VAR_0,VAR_1,VAR_2] :
( VAR_1 = VAR_2
| c_HOL_Oinverse__class_Oinverse(VAR_1,VAR_0) != c_HOL_Oinverse__class_Oinverse(VAR_2,VAR_0)
| ~ class_Ring__and__Field_Odivision__by__zero(VAR_0)
| ~ class_Ring__and__Field_Odivision__ring(VAR_0) ),
file('theBenchmark.p',cls_inverse__eq__iff__eq_0) ).
cnf(c_114,plain,
( B = C
| c_HOL_Oinverse__class_Oinverse(B,A) != c_HOL_Oinverse__class_Oinverse(C,A)
| ~ class_Ring__and__Field_Odivision__by__zero(A)
| ~ class_Ring__and__Field_Odivision__ring(A) ),
inference(clausify,[status(thm)],[cls_inverse__eq__iff__eq_0]) ).
fof(cls_inverse__inverse__eq_0,axiom,
! [VAR_0,VAR_1] :
( c_HOL_Oinverse__class_Oinverse(c_HOL_Oinverse__class_Oinverse(VAR_1,VAR_0),VAR_0) = VAR_1
| ~ class_Ring__and__Field_Odivision__by__zero(VAR_0)
| ~ class_Ring__and__Field_Odivision__ring(VAR_0) ),
file('theBenchmark.p',cls_inverse__inverse__eq_0) ).
cnf(c_115,plain,
( c_HOL_Oinverse__class_Oinverse(c_HOL_Oinverse__class_Oinverse(B,A),A) = B
| ~ class_Ring__and__Field_Odivision__by__zero(A)
| ~ class_Ring__and__Field_Odivision__ring(A) ),
inference(clausify,[status(thm)],[cls_inverse__inverse__eq_0]) ).
fof(clsarity_Complex__Ocomplex__OrderedGroup_Oab__group__add,axiom,
class_OrderedGroup_Oab__group__add(tc_Complex_Ocomplex),
file('theBenchmark.p',clsarity_Complex__Ocomplex__OrderedGroup_Oab__group__add) ).
cnf(c_190,plain,
class_OrderedGroup_Oab__group__add(tc_Complex_Ocomplex),
inference(clausify,[status(thm)],[clsarity_Complex__Ocomplex__OrderedGroup_Oab__group__add]) ).
fof(cls_eq__iff__diff__eq__0_0,axiom,
! [VAR_0,VAR_1] :
( c_HOL_Ominus__class_Ominus(VAR_1,VAR_1,VAR_0) = c_HOL_Ozero__class_Ozero(VAR_0)
| ~ class_OrderedGroup_Oab__group__add(VAR_0) ),
file('theBenchmark.p',cls_eq__iff__diff__eq__0_0) ).
cnf(c_192,plain,
( c_HOL_Ominus__class_Ominus(B,B,A) = c_HOL_Ozero__class_Ozero(A)
| ~ class_OrderedGroup_Oab__group__add(A) ),
inference(clausify,[status(thm)],[cls_eq__iff__diff__eq__0_0]) ).
cnf(c_552,plain,
c_HOL_Ominus__class_Ominus(A,A,tc_Complex_Ocomplex) = c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),
inference(resolve,[status(thm)],[c_192,c_190]) ).
cnf(c_621,plain,
hAPP(c_Power_Opower__class_Opower(A,tc_Complex_Ocomplex),c_HOL_Otimes__class_Otimes(B,C,tc_nat)) = hAPP(c_Power_Opower__class_Opower(hAPP(c_Power_Opower__class_Opower(A,tc_Complex_Ocomplex),B),tc_Complex_Ocomplex),C),
inference(resolve,[status(thm)],[c_22,c_20]) ).
cnf(c_622,plain,
hAPP(c_Power_Opower__class_Opower(hAPP(c_Power_Opower__class_Opower(A,tc_Complex_Ocomplex),B),tc_Complex_Ocomplex),C) = hAPP(c_Power_Opower__class_Opower(A,tc_Complex_Ocomplex),c_HOL_Otimes__class_Otimes(B,C,tc_nat)),
inference(copy,[status(thm)],[c_621]) ).
cnf(c_631,plain,
hAPP(c_Power_Opower__class_Opower(c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),tc_Complex_Ocomplex),A) = c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),
inference(resolve,[status(thm)],[c_17,c_20]) ).
fof(cls_nat__mult__commute_0,axiom,
! [VAR_0,VAR_1] : c_HOL_Otimes__class_Otimes(VAR_0,VAR_1,tc_nat) = c_HOL_Otimes__class_Otimes(VAR_1,VAR_0,tc_nat),
file('theBenchmark.p',cls_nat__mult__commute_0) ).
cnf(c_637,plain,
c_HOL_Otimes__class_Otimes(A,B,tc_nat) = c_HOL_Otimes__class_Otimes(B,A,tc_nat),
inference(clausify,[status(thm)],[cls_nat__mult__commute_0]) ).
fof(cls_inverse__eq__divide_0,axiom,
! [VAR_0,VAR_1] :
( c_HOL_Oinverse__class_Oinverse(VAR_1,VAR_0) = c_HOL_Oinverse__class_Odivide(c_HOL_Oone__class_Oone(VAR_0),VAR_1,VAR_0)
| ~ class_Ring__and__Field_Ofield(VAR_0) ),
file('theBenchmark.p',cls_inverse__eq__divide_0) ).
cnf(c_782,plain,
( c_HOL_Oinverse__class_Oinverse(B,A) = c_HOL_Oinverse__class_Odivide(c_HOL_Oone__class_Oone(A),B,A)
| ~ class_Ring__and__Field_Ofield(A) ),
inference(clausify,[status(thm)],[cls_inverse__eq__divide_0]) ).
cnf(c_783,plain,
( c_HOL_Oinverse__class_Odivide(c_HOL_Oone__class_Oone(A),B,A) = c_HOL_Oinverse__class_Oinverse(B,A)
| ~ class_Ring__and__Field_Ofield(A) ),
inference(copy,[status(thm)],[c_782]) ).
fof(cls_atLeast0LessThan_0,axiom,
! [VAR_0] : c_SetInterval_Oord__class_OatLeastLessThan(c_HOL_Ozero__class_Ozero(tc_nat),VAR_0,tc_nat) = c_SetInterval_Oord__class_OlessThan(VAR_0,tc_nat),
file('theBenchmark.p',cls_atLeast0LessThan_0) ).
cnf(c_787,plain,
c_SetInterval_Oord__class_OatLeastLessThan(c_HOL_Ozero__class_Ozero(tc_nat),A,tc_nat) = c_SetInterval_Oord__class_OlessThan(A,tc_nat),
inference(clausify,[status(thm)],[cls_atLeast0LessThan_0]) ).
fof(cls_k_I1_J_0,axiom,
c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),v_k,tc_nat),
file('theBenchmark.p',cls_k_I1_J_0) ).
cnf(c_788,plain,
c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),v_k,tc_nat),
inference(clausify,[status(thm)],[cls_k_I1_J_0]) ).
fof(cls_k_I2_J_0,axiom,
c_HOL_Oord__class_Oless(v_k,v_n,tc_nat),
file('theBenchmark.p',cls_k_I2_J_0) ).
cnf(c_789,plain,
c_HOL_Oord__class_Oless(v_k,v_n,tc_nat),
inference(clausify,[status(thm)],[cls_k_I2_J_0]) ).
fof(cls_geometric__sum_0,axiom,
! [VAR_0,VAR_1,VAR_2] :
( VAR_1 = c_HOL_Oone__class_Oone(VAR_0)
| c_Finite__Set_Osetsum(c_Power_Opower__class_Opower(VAR_1,VAR_0),c_SetInterval_Oord__class_OatLeastLessThan(c_HOL_Ozero__class_Ozero(tc_nat),VAR_2,tc_nat),tc_nat,VAR_0) = c_HOL_Oinverse__class_Odivide(c_HOL_Ominus__class_Ominus(hAPP(c_Power_Opower__class_Opower(VAR_1,VAR_0),VAR_2),c_HOL_Oone__class_Oone(VAR_0),VAR_0),c_HOL_Ominus__class_Ominus(VAR_1,c_HOL_Oone__class_Oone(VAR_0),VAR_0),VAR_0)
| ~ class_Ring__and__Field_Ofield(VAR_0) ),
file('theBenchmark.p',cls_geometric__sum_0) ).
cnf(c_792,plain,
( B = c_HOL_Oone__class_Oone(A)
| c_Finite__Set_Osetsum(c_Power_Opower__class_Opower(B,A),c_SetInterval_Oord__class_OatLeastLessThan(c_HOL_Ozero__class_Ozero(tc_nat),C,tc_nat),tc_nat,A) = c_HOL_Oinverse__class_Odivide(c_HOL_Ominus__class_Ominus(hAPP(c_Power_Opower__class_Opower(B,A),C),c_HOL_Oone__class_Oone(A),A),c_HOL_Ominus__class_Ominus(B,c_HOL_Oone__class_Oone(A),A),A)
| ~ class_Ring__and__Field_Ofield(A) ),
inference(clausify,[status(thm)],[cls_geometric__sum_0]) ).
cnf(c_26495,plain,
( B = c_HOL_Oone__class_Oone(A)
| c_Finite__Set_Osetsum(c_Power_Opower__class_Opower(B,A),c_SetInterval_Oord__class_OlessThan(C,tc_nat),tc_nat,A) = c_HOL_Oinverse__class_Odivide(c_HOL_Ominus__class_Ominus(hAPP(c_Power_Opower__class_Opower(B,A),C),c_HOL_Oone__class_Oone(A),A),c_HOL_Ominus__class_Ominus(B,c_HOL_Oone__class_Oone(A),A),A)
| ~ class_Ring__and__Field_Ofield(A) ),
inference(paramod,[status(thm)],[c_787,c_792]) ).
cnf(c_793,plain,
( c_HOL_Oone__class_Oone(A) = B
| c_Finite__Set_Osetsum(c_Power_Opower__class_Opower(B,A),c_SetInterval_Oord__class_OlessThan(C,tc_nat),tc_nat,A) = c_HOL_Oinverse__class_Odivide(c_HOL_Ominus__class_Ominus(hAPP(c_Power_Opower__class_Opower(B,A),C),c_HOL_Oone__class_Oone(A),A),c_HOL_Ominus__class_Ominus(B,c_HOL_Oone__class_Oone(A),A),A)
| ~ class_Ring__and__Field_Ofield(A) ),
inference(copy,[status(thm)],[c_26495]) ).
fof(cls_root__summation_0,axiom,
! [VAR_0,VAR_1] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),VAR_1,tc_nat)
| ~ c_HOL_Oord__class_Oless(VAR_1,VAR_0,tc_nat)
| c_Finite__Set_Osetsum(c_Power_Opower__class_Opower(hAPP(c_Power_Opower__class_Opower(c_FFT__Mirabelle_Oroot(VAR_0),tc_Complex_Ocomplex),VAR_1),tc_Complex_Ocomplex),c_SetInterval_Oord__class_OatLeastLessThan(c_HOL_Ozero__class_Ozero(tc_nat),VAR_0,tc_nat),tc_nat,tc_Complex_Ocomplex) = c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) ),
file('theBenchmark.p',cls_root__summation_0) ).
cnf(c_794,plain,
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),B,tc_nat)
| ~ c_HOL_Oord__class_Oless(B,A,tc_nat)
| c_Finite__Set_Osetsum(c_Power_Opower__class_Opower(hAPP(c_Power_Opower__class_Opower(c_FFT__Mirabelle_Oroot(A),tc_Complex_Ocomplex),B),tc_Complex_Ocomplex),c_SetInterval_Oord__class_OatLeastLessThan(c_HOL_Ozero__class_Ozero(tc_nat),A,tc_nat),tc_nat,tc_Complex_Ocomplex) = c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) ),
inference(clausify,[status(thm)],[cls_root__summation_0]) ).
cnf(c_795,plain,
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),B,tc_nat)
| ~ c_HOL_Oord__class_Oless(B,A,tc_nat)
| c_Finite__Set_Osetsum(c_Power_Opower__class_Opower(hAPP(c_Power_Opower__class_Opower(c_FFT__Mirabelle_Oroot(A),tc_Complex_Ocomplex),B),tc_Complex_Ocomplex),c_SetInterval_Oord__class_OlessThan(A,tc_nat),tc_nat,tc_Complex_Ocomplex) = c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) ),
inference(paramod,[status(thm)],[c_787,c_794]) ).
fof(cls_root__unity_0,axiom,
! [VAR_0] : hAPP(c_Power_Opower__class_Opower(c_FFT__Mirabelle_Oroot(VAR_0),tc_Complex_Ocomplex),VAR_0) = c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),
file('theBenchmark.p',cls_root__unity_0) ).
cnf(c_803,plain,
hAPP(c_Power_Opower__class_Opower(c_FFT__Mirabelle_Oroot(A),tc_Complex_Ocomplex),A) = c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),
inference(clausify,[status(thm)],[cls_root__unity_0]) ).
fof(cls_conjecture_0,axiom,
c_Finite__Set_Osetsum(c_Power_Opower__class_Opower(hAPP(c_Power_Opower__class_Opower(c_HOL_Oinverse__class_Odivide(c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),c_FFT__Mirabelle_Oroot(v_n),tc_Complex_Ocomplex),tc_Complex_Ocomplex),v_k),tc_Complex_Ocomplex),c_SetInterval_Oord__class_OatLeastLessThan(c_HOL_Ozero__class_Ozero(tc_nat),v_n,tc_nat),tc_nat,tc_Complex_Ocomplex) != c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),
file('theBenchmark.p',cls_conjecture_0) ).
cnf(c_809,plain,
c_Finite__Set_Osetsum(c_Power_Opower__class_Opower(hAPP(c_Power_Opower__class_Opower(c_HOL_Oinverse__class_Odivide(c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),c_FFT__Mirabelle_Oroot(v_n),tc_Complex_Ocomplex),tc_Complex_Ocomplex),v_k),tc_Complex_Ocomplex),c_SetInterval_Oord__class_OatLeastLessThan(c_HOL_Ozero__class_Ozero(tc_nat),v_n,tc_nat),tc_nat,tc_Complex_Ocomplex) != c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),
inference(clausify,[status(thm)],[cls_conjecture_0]) ).
cnf(c_810,plain,
c_Finite__Set_Osetsum(c_Power_Opower__class_Opower(hAPP(c_Power_Opower__class_Opower(c_HOL_Oinverse__class_Odivide(c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),c_FFT__Mirabelle_Oroot(v_n),tc_Complex_Ocomplex),tc_Complex_Ocomplex),v_k),tc_Complex_Ocomplex),c_SetInterval_Oord__class_OlessThan(v_n,tc_nat),tc_nat,tc_Complex_Ocomplex) != c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),
inference(paramod,[status(thm)],[c_787,c_809]) ).
fof(clsarity_Complex__Ocomplex__Ring__and__Field_Odivision__ring,axiom,
class_Ring__and__Field_Odivision__ring(tc_Complex_Ocomplex),
file('theBenchmark.p',clsarity_Complex__Ocomplex__Ring__and__Field_Odivision__ring) ).
cnf(c_842,plain,
class_Ring__and__Field_Odivision__ring(tc_Complex_Ocomplex),
inference(clausify,[status(thm)],[clsarity_Complex__Ocomplex__Ring__and__Field_Odivision__ring]) ).
fof(clsarity_Complex__Ocomplex__Ring__and__Field_Ofield,axiom,
class_Ring__and__Field_Ofield(tc_Complex_Ocomplex),
file('theBenchmark.p',clsarity_Complex__Ocomplex__Ring__and__Field_Ofield) ).
cnf(c_846,plain,
class_Ring__and__Field_Ofield(tc_Complex_Ocomplex),
inference(clausify,[status(thm)],[clsarity_Complex__Ocomplex__Ring__and__Field_Ofield]) ).
cnf(c_979,plain,
c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),A,tc_Complex_Ocomplex) = c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),
inference(resolve,[status(thm)],[c_66,c_47]) ).
cnf(c_1014,plain,
( c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) = c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),A,tc_Complex_Ocomplex),A,tc_Complex_Ocomplex)
| ~ class_Ring__and__Field_Ofield(tc_Complex_Ocomplex) ),
inference(resolve,[status(thm)],[c_67,c_84]) ).
cnf(c_26496,plain,
( c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) = c_HOL_Oinverse__class_Odivide(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),A,tc_Complex_Ocomplex)
| ~ class_Ring__and__Field_Ofield(tc_Complex_Ocomplex) ),
inference(paramod,[status(thm)],[c_979,c_1014]) ).
cnf(c_26497,plain,
( c_HOL_Oinverse__class_Odivide(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),A,tc_Complex_Ocomplex) = c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)
| ~ class_Ring__and__Field_Ofield(tc_Complex_Ocomplex) ),
inference(copy,[status(thm)],[c_26496]) ).
cnf(c_1015,plain,
c_HOL_Oinverse__class_Odivide(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),A,tc_Complex_Ocomplex) = c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),
inference(resolve,[status(thm)],[c_846,c_26497]) ).
cnf(c_1031,plain,
( c_HOL_Oinverse__class_Oinverse(hAPP(c_Power_Opower__class_Opower(A,tc_Complex_Ocomplex),B),tc_Complex_Ocomplex) = hAPP(c_Power_Opower__class_Opower(c_HOL_Oinverse__class_Oinverse(A,tc_Complex_Ocomplex),tc_Complex_Ocomplex),B)
| ~ class_Ring__and__Field_Odivision__ring(tc_Complex_Ocomplex) ),
inference(resolve,[status(thm)],[c_67,c_94]) ).
cnf(c_26498,plain,
( hAPP(c_Power_Opower__class_Opower(c_HOL_Oinverse__class_Oinverse(A,tc_Complex_Ocomplex),tc_Complex_Ocomplex),B) = c_HOL_Oinverse__class_Oinverse(hAPP(c_Power_Opower__class_Opower(A,tc_Complex_Ocomplex),B),tc_Complex_Ocomplex)
| ~ class_Ring__and__Field_Odivision__ring(tc_Complex_Ocomplex) ),
inference(copy,[status(thm)],[c_1031]) ).
cnf(c_1032,plain,
hAPP(c_Power_Opower__class_Opower(c_HOL_Oinverse__class_Oinverse(A,tc_Complex_Ocomplex),tc_Complex_Ocomplex),B) = c_HOL_Oinverse__class_Oinverse(hAPP(c_Power_Opower__class_Opower(A,tc_Complex_Ocomplex),B),tc_Complex_Ocomplex),
inference(resolve,[status(thm)],[c_842,c_26498]) ).
cnf(c_1035,plain,
( c_HOL_Oinverse__class_Oinverse(c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),tc_Complex_Ocomplex) = c_HOL_Oone__class_Oone(tc_Complex_Ocomplex)
| ~ class_Ring__and__Field_Ofield(tc_Complex_Ocomplex) ),
inference(resolve,[status(thm)],[c_67,c_96]) ).
cnf(c_1036,plain,
c_HOL_Oinverse__class_Oinverse(c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),tc_Complex_Ocomplex) = c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),
inference(resolve,[status(thm)],[c_846,c_1035]) ).
cnf(c_1052,plain,
( A = B
| c_HOL_Oinverse__class_Oinverse(A,tc_Complex_Ocomplex) != c_HOL_Oinverse__class_Oinverse(B,tc_Complex_Ocomplex)
| ~ class_Ring__and__Field_Odivision__ring(tc_Complex_Ocomplex) ),
inference(resolve,[status(thm)],[c_67,c_114]) ).
cnf(c_1053,plain,
( A = B
| c_HOL_Oinverse__class_Oinverse(A,tc_Complex_Ocomplex) != c_HOL_Oinverse__class_Oinverse(B,tc_Complex_Ocomplex) ),
inference(resolve,[status(thm)],[c_842,c_1052]) ).
cnf(c_1054,plain,
( c_HOL_Oinverse__class_Oinverse(c_HOL_Oinverse__class_Oinverse(A,tc_Complex_Ocomplex),tc_Complex_Ocomplex) = A
| ~ class_Ring__and__Field_Odivision__ring(tc_Complex_Ocomplex) ),
inference(resolve,[status(thm)],[c_67,c_115]) ).
cnf(c_1055,plain,
c_HOL_Oinverse__class_Oinverse(c_HOL_Oinverse__class_Oinverse(A,tc_Complex_Ocomplex),tc_Complex_Ocomplex) = A,
inference(resolve,[status(thm)],[c_842,c_1054]) ).
cnf(c_1433,plain,
hAPP(c_Power_Opower__class_Opower(hAPP(c_Power_Opower__class_Opower(A,tc_Complex_Ocomplex),B),tc_Complex_Ocomplex),C) = hAPP(c_Power_Opower__class_Opower(A,tc_Complex_Ocomplex),c_HOL_Otimes__class_Otimes(C,B,tc_nat)),
inference(paramod,[status(thm)],[c_637,c_622]) ).
cnf(c_26499,plain,
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),v_k,tc_nat)
| c_Finite__Set_Osetsum(c_Power_Opower__class_Opower(hAPP(c_Power_Opower__class_Opower(c_FFT__Mirabelle_Oroot(v_n),tc_Complex_Ocomplex),v_k),tc_Complex_Ocomplex),c_SetInterval_Oord__class_OlessThan(v_n,tc_nat),tc_nat,tc_Complex_Ocomplex) = c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) ),
inference(resolve,[status(thm)],[c_795,c_789]) ).
cnf(c_1670,plain,
c_Finite__Set_Osetsum(c_Power_Opower__class_Opower(hAPP(c_Power_Opower__class_Opower(c_FFT__Mirabelle_Oroot(v_n),tc_Complex_Ocomplex),v_k),tc_Complex_Ocomplex),c_SetInterval_Oord__class_OlessThan(v_n,tc_nat),tc_nat,tc_Complex_Ocomplex) = c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),
inference(resolve,[status(thm)],[c_788,c_26499]) ).
cnf(c_26500,plain,
hAPP(c_Power_Opower__class_Opower(c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),tc_Complex_Ocomplex),A) = hAPP(c_Power_Opower__class_Opower(c_FFT__Mirabelle_Oroot(B),tc_Complex_Ocomplex),c_HOL_Otimes__class_Otimes(B,A,tc_nat)),
inference(paramod,[status(thm)],[c_803,c_622]) ).
cnf(c_26501,plain,
c_HOL_Oone__class_Oone(tc_Complex_Ocomplex) = hAPP(c_Power_Opower__class_Opower(c_FFT__Mirabelle_Oroot(B),tc_Complex_Ocomplex),c_HOL_Otimes__class_Otimes(B,A,tc_nat)),
inference(paramod,[status(thm)],[c_631,c_26500]) ).
cnf(c_1683,plain,
hAPP(c_Power_Opower__class_Opower(c_FFT__Mirabelle_Oroot(A),tc_Complex_Ocomplex),c_HOL_Otimes__class_Otimes(A,B,tc_nat)) = c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),
inference(copy,[status(thm)],[c_26501]) ).
cnf(c_1742,plain,
( c_HOL_Oone__class_Oone(tc_Complex_Ocomplex) = A
| c_Finite__Set_Osetsum(c_Power_Opower__class_Opower(A,tc_Complex_Ocomplex),c_SetInterval_Oord__class_OlessThan(B,tc_nat),tc_nat,tc_Complex_Ocomplex) = c_HOL_Oinverse__class_Odivide(c_HOL_Ominus__class_Ominus(hAPP(c_Power_Opower__class_Opower(A,tc_Complex_Ocomplex),B),c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_HOL_Ominus__class_Ominus(A,c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex) ),
inference(resolve,[status(thm)],[c_846,c_793]) ).
cnf(c_1743,plain,
c_HOL_Oinverse__class_Odivide(c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),A,tc_Complex_Ocomplex) = c_HOL_Oinverse__class_Oinverse(A,tc_Complex_Ocomplex),
inference(resolve,[status(thm)],[c_846,c_783]) ).
cnf(c_26502,plain,
c_Finite__Set_Osetsum(c_Power_Opower__class_Opower(hAPP(c_Power_Opower__class_Opower(c_HOL_Oinverse__class_Oinverse(c_FFT__Mirabelle_Oroot(v_n),tc_Complex_Ocomplex),tc_Complex_Ocomplex),v_k),tc_Complex_Ocomplex),c_SetInterval_Oord__class_OlessThan(v_n,tc_nat),tc_nat,tc_Complex_Ocomplex) != c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),
inference(paramod,[status(thm)],[c_1743,c_810]) ).
cnf(c_1748,plain,
c_Finite__Set_Osetsum(c_Power_Opower__class_Opower(c_HOL_Oinverse__class_Oinverse(hAPP(c_Power_Opower__class_Opower(c_FFT__Mirabelle_Oroot(v_n),tc_Complex_Ocomplex),v_k),tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_SetInterval_Oord__class_OlessThan(v_n,tc_nat),tc_nat,tc_Complex_Ocomplex) != c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),
inference(paramod,[status(thm)],[c_1032,c_26502]) ).
cnf(c_26503,plain,
( c_HOL_Oinverse__class_Oinverse(A,tc_Complex_Ocomplex) = B
| A != c_HOL_Oinverse__class_Oinverse(B,tc_Complex_Ocomplex) ),
inference(paramod,[status(thm)],[c_1055,c_1053]) ).
cnf(c_2385,plain,
( c_HOL_Oinverse__class_Oinverse(B,tc_Complex_Ocomplex) = A
| c_HOL_Oinverse__class_Oinverse(A,tc_Complex_Ocomplex) != B ),
inference(copy,[status(thm)],[c_26503]) ).
cnf(c_24651,plain,
hAPP(c_Power_Opower__class_Opower(hAPP(c_Power_Opower__class_Opower(c_FFT__Mirabelle_Oroot(A),tc_Complex_Ocomplex),B),tc_Complex_Ocomplex),A) = c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),
inference(paramod,[status(thm)],[c_1683,c_1433]) ).
cnf(c_26504,plain,
( c_HOL_Oinverse__class_Odivide(c_HOL_Ominus__class_Ominus(hAPP(c_Power_Opower__class_Opower(c_HOL_Oinverse__class_Oinverse(hAPP(c_Power_Opower__class_Opower(c_FFT__Mirabelle_Oroot(v_n),tc_Complex_Ocomplex),v_k),tc_Complex_Ocomplex),tc_Complex_Ocomplex),v_n),c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_HOL_Ominus__class_Ominus(c_HOL_Oinverse__class_Oinverse(hAPP(c_Power_Opower__class_Opower(c_FFT__Mirabelle_Oroot(v_n),tc_Complex_Ocomplex),v_k),tc_Complex_Ocomplex),c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex) != c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)
| c_HOL_Oone__class_Oone(tc_Complex_Ocomplex) = c_HOL_Oinverse__class_Oinverse(hAPP(c_Power_Opower__class_Opower(c_FFT__Mirabelle_Oroot(v_n),tc_Complex_Ocomplex),v_k),tc_Complex_Ocomplex) ),
inference(paramod,[status(thm)],[c_1742,c_1748]) ).
cnf(c_26505,plain,
( c_HOL_Oinverse__class_Odivide(c_HOL_Ominus__class_Ominus(c_HOL_Oinverse__class_Oinverse(hAPP(c_Power_Opower__class_Opower(hAPP(c_Power_Opower__class_Opower(c_FFT__Mirabelle_Oroot(v_n),tc_Complex_Ocomplex),v_k),tc_Complex_Ocomplex),v_n),tc_Complex_Ocomplex),c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_HOL_Ominus__class_Ominus(c_HOL_Oinverse__class_Oinverse(hAPP(c_Power_Opower__class_Opower(c_FFT__Mirabelle_Oroot(v_n),tc_Complex_Ocomplex),v_k),tc_Complex_Ocomplex),c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex) != c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)
| c_HOL_Oone__class_Oone(tc_Complex_Ocomplex) = c_HOL_Oinverse__class_Oinverse(hAPP(c_Power_Opower__class_Opower(c_FFT__Mirabelle_Oroot(v_n),tc_Complex_Ocomplex),v_k),tc_Complex_Ocomplex) ),
inference(paramod,[status(thm)],[c_1032,c_26504]) ).
cnf(c_26506,plain,
( c_HOL_Oinverse__class_Odivide(c_HOL_Ominus__class_Ominus(c_HOL_Oinverse__class_Oinverse(c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_HOL_Ominus__class_Ominus(c_HOL_Oinverse__class_Oinverse(hAPP(c_Power_Opower__class_Opower(c_FFT__Mirabelle_Oroot(v_n),tc_Complex_Ocomplex),v_k),tc_Complex_Ocomplex),c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex) != c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)
| c_HOL_Oone__class_Oone(tc_Complex_Ocomplex) = c_HOL_Oinverse__class_Oinverse(hAPP(c_Power_Opower__class_Opower(c_FFT__Mirabelle_Oroot(v_n),tc_Complex_Ocomplex),v_k),tc_Complex_Ocomplex) ),
inference(paramod,[status(thm)],[c_24651,c_26505]) ).
cnf(c_26507,plain,
( c_HOL_Oinverse__class_Odivide(c_HOL_Ominus__class_Ominus(c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_HOL_Ominus__class_Ominus(c_HOL_Oinverse__class_Oinverse(hAPP(c_Power_Opower__class_Opower(c_FFT__Mirabelle_Oroot(v_n),tc_Complex_Ocomplex),v_k),tc_Complex_Ocomplex),c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex) != c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)
| c_HOL_Oone__class_Oone(tc_Complex_Ocomplex) = c_HOL_Oinverse__class_Oinverse(hAPP(c_Power_Opower__class_Opower(c_FFT__Mirabelle_Oroot(v_n),tc_Complex_Ocomplex),v_k),tc_Complex_Ocomplex) ),
inference(paramod,[status(thm)],[c_1036,c_26506]) ).
cnf(c_26508,plain,
( c_HOL_Oinverse__class_Odivide(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),c_HOL_Ominus__class_Ominus(c_HOL_Oinverse__class_Oinverse(hAPP(c_Power_Opower__class_Opower(c_FFT__Mirabelle_Oroot(v_n),tc_Complex_Ocomplex),v_k),tc_Complex_Ocomplex),c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex) != c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)
| c_HOL_Oone__class_Oone(tc_Complex_Ocomplex) = c_HOL_Oinverse__class_Oinverse(hAPP(c_Power_Opower__class_Opower(c_FFT__Mirabelle_Oroot(v_n),tc_Complex_Ocomplex),v_k),tc_Complex_Ocomplex) ),
inference(paramod,[status(thm)],[c_552,c_26507]) ).
cnf(c_26509,plain,
( c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) != c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)
| c_HOL_Oone__class_Oone(tc_Complex_Ocomplex) = c_HOL_Oinverse__class_Oinverse(hAPP(c_Power_Opower__class_Opower(c_FFT__Mirabelle_Oroot(v_n),tc_Complex_Ocomplex),v_k),tc_Complex_Ocomplex) ),
inference(paramod,[status(thm)],[c_1015,c_26508]) ).
cnf(c_26510,plain,
( c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) != c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)
| c_HOL_Oinverse__class_Oinverse(hAPP(c_Power_Opower__class_Opower(c_FFT__Mirabelle_Oroot(v_n),tc_Complex_Ocomplex),v_k),tc_Complex_Ocomplex) = c_HOL_Oone__class_Oone(tc_Complex_Ocomplex) ),
inference(copy,[status(thm)],[c_26509]) ).
cnf(c_25876,plain,
c_HOL_Oinverse__class_Oinverse(hAPP(c_Power_Opower__class_Opower(c_FFT__Mirabelle_Oroot(v_n),tc_Complex_Ocomplex),v_k),tc_Complex_Ocomplex) = c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),
inference(copy,[status(thm)],[c_26510]) ).
cnf(c_25879,plain,
c_Finite__Set_Osetsum(c_Power_Opower__class_Opower(c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_SetInterval_Oord__class_OlessThan(v_n,tc_nat),tc_nat,tc_Complex_Ocomplex) != c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),
inference(paramod,[status(thm)],[c_25876,c_1748]) ).
cnf(c_26511,plain,
c_HOL_Oinverse__class_Oinverse(c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),tc_Complex_Ocomplex) = hAPP(c_Power_Opower__class_Opower(c_FFT__Mirabelle_Oroot(v_n),tc_Complex_Ocomplex),v_k),
inference(resolve,[status(thm)],[c_25876,c_2385]) ).
cnf(c_26512,plain,
c_HOL_Oone__class_Oone(tc_Complex_Ocomplex) = hAPP(c_Power_Opower__class_Opower(c_FFT__Mirabelle_Oroot(v_n),tc_Complex_Ocomplex),v_k),
inference(paramod,[status(thm)],[c_1036,c_26511]) ).
cnf(c_26493,plain,
hAPP(c_Power_Opower__class_Opower(c_FFT__Mirabelle_Oroot(v_n),tc_Complex_Ocomplex),v_k) = c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),
inference(copy,[status(thm)],[c_26512]) ).
cnf(c_26513,plain,
c_Finite__Set_Osetsum(c_Power_Opower__class_Opower(c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_SetInterval_Oord__class_OlessThan(v_n,tc_nat),tc_nat,tc_Complex_Ocomplex) = c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),
inference(paramod,[status(thm)],[c_26493,c_1670]) ).
cnf(c_26494,plain,
$false,
inference(resolve,[status(thm)],[c_25879,c_26513]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV618-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.38 % Computer : n020.cluster.edu
% 0.10/0.38 % Model : x86_64 x86_64
% 0.10/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.38 % Memory : 8046.5625MB
% 0.10/0.38 % OS : Linux 6.8.0-71-generic
% 0.10/0.38 % CPULimit : 300
% 0.10/0.38 % WCLimit : 300
% 0.10/0.38 % DateTime : Sat Sep 26 14:38:33 UTC 2026
% 0.10/0.38 % CPUTime :
% 0.10/0.38 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.10/0.38 % Process 1797195 was started by sandbox on n020,
% 0.10/0.38 % Sat Sep 26 14:38:33 2026
% 0.10/0.38 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.10/0.41
% 0.10/0.41 % From the command line: assign(max_seconds, 300).
% 111.40/15.47
% 111.40/15.47 % given #500 (I,wt=22): 1192 c_lessequals(c_HOL_Ozero__class_Ozero(tc_Int_Oint),c_HOL_Otimes__class_Otimes(A,B,tc_Int_Oint),tc_Int_Oint) | -c_lessequals(c_HOL_Ozero__class_Ozero(tc_Int_Oint),C,tc_Int_Oint) | -c_lessequals(c_HOL_Ozero__class_Ozero(tc_Int_Oint),A,tc_Int_Oint) | -c_lessequals(C,B,tc_Int_Oint). [factor(455,c,e),rewrite([946(4)])].
% 111.40/15.47
% 111.40/15.47 % given #1000 (F,wt=20): 6112 -c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(A,c_HOL_Ominus__class_Ominus(B,c_HOL_Ouminus__class_Ouminus(C,tc_Int_Oint),tc_Int_Oint),tc_Int_Oint),c_HOL_Otimes__class_Otimes(A,c_HOL_Ominus__class_Ominus(C,c_HOL_Ouminus__class_Ouminus(B,tc_Int_Oint),tc_Int_Oint),tc_Int_Oint),tc_Int_Oint). [para(1316(a,1),5493(a,1,1,2)),rewrite([489(8),501(10)])].
% 111.40/15.47
% 111.40/15.47 % given #1500 (T,wt=10): 5050 class_Orderings_Obot(tc_fun(A,tc_fun(B,tc_fun(C,tc_fun(D,tc_bool))))). [resolve(4052,a,815,b)].
% 111.40/15.47
% 111.40/15.47 % given #2000 (F,wt=20): 9876 -c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(A,c_HOL_Otimes__class_Otimes(c_Suc(v_k),c_HOL_Otimes__class_Otimes(B,C,tc_nat),tc_nat),tc_nat),c_HOL_Otimes__class_Otimes(A,c_HOL_Otimes__class_Otimes(C,B,tc_nat),tc_nat),tc_nat). [para(910(a,1),9719(a,2)),rewrite([637(6)])].
% 111.40/15.47
% 111.40/15.47 % given #2500 (T,wt=11): 8625 c_HOL_Oord__class_Oless(A,c_Suc(c_Suc(v_n)),tc_nat) | c_HOL_Oord__class_Oless(v_k,c_Suc(A),tc_nat). [resolve(1567,a,3635,b)].
% 111.40/15.47
% 111.40/15.47 % given #3000 (F,wt=11): 23056 -c_HOL_Oord__class_Oless(c_Suc(c_Suc(c_Suc(c_HOL_Otimes__class_Otimes(v_k,A,tc_nat)))),c_Suc(A),tc_nat). [para(637(a,1),23035(a,1,1,1,1))].
% 111.40/15.47
% 111.40/15.47 % given #3500 (T,wt=11): 20954 c_lessequals(A,c_Suc(c_Suc(v_n)),tc_nat) | -c_HOL_Oord__class_Oless(c_Suc(A),v_k,tc_nat). [resolve(10037,b,1064,a)].
% 111.40/15.47
% 111.40/15.47 % SZS status Unsatisfiable for theBenchmark
% 111.40/15.47
% 111.40/15.47 % Proof 1 at 11.53 (+ 3.26) seconds.
% 111.40/15.47 % Length of proof is 55.
% 111.40/15.47 % Level of proof is 7.
% 111.40/15.47 % Maximum clause weight is 32.000.
% 111.40/15.47 % Given clauses 3941.
% 111.40/15.47
% 111.40/15.47 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------