%------------------------------------------------------------------------------
% File : LEO-II---2.3.1
% Problem : SWW342+1 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : leo --cores 7 --timeout 300 --proofoutput 1 --foatp e --atp e=/export/starexec/sandbox/solver/bin/eprover /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n012.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 : Wed Oct 7 11:01:16 AM UTC 2026
% Result : Theorem 42.41s 8.60s
% Output : CNFRefutation 42.41s
% Verified :
% SZS Type : Refutation
% Derivation depth : 22
% Number of leaves : 21
% Syntax : Number of formulae : 215 ( 177 unt; 0 typ; 0 def)
% Number of atoms : 843 ( 354 equ; 0 cnn)
% Maximal formula atoms : 3 ( 3 avg)
% Number of connectives : 2176 ( 334 ~; 132 |; 3 &;1676 @)
% ( 3 <=>; 28 =>; 0 <=; 0 <~>)
% Maximal formula depth : 15 ( 4 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of symbols : 542 ( 539 usr; 68 con; 0-10 aty)
% Number of variables : 887 ( 0 ^; 884 !; 3 ?; 887 :)
% Comments :
%------------------------------------------------------------------------------
thf(tp_c_Big__Operators_Ocomm__monoid__add__class_Osetsum,type,
c_Big__Operators_Ocomm__monoid__add__class_Osetsum: $i > $i > $i ).
thf(tp_c_Big__Operators_Ocomm__monoid__big,type,
c_Big__Operators_Ocomm__monoid__big: $i > $i > $i > $i > $i > $o ).
thf(tp_c_Big__Operators_Ocomm__monoid__mult__class_Osetprod,type,
c_Big__Operators_Ocomm__monoid__mult__class_Osetprod: $i > $i > $i ).
thf(tp_c_Big__Operators_Olattice_OInf__fin,type,
c_Big__Operators_Olattice_OInf__fin: $i > $i > $i > $i ).
thf(tp_c_Big__Operators_Olattice_OSup__fin,type,
c_Big__Operators_Olattice_OSup__fin: $i > $i > $i > $i ).
thf(tp_c_Big__Operators_Olattice__class_OInf__fin,type,
c_Big__Operators_Olattice__class_OInf__fin: $i > $i > $i ).
thf(tp_c_Big__Operators_Olattice__class_OSup__fin,type,
c_Big__Operators_Olattice__class_OSup__fin: $i > $i > $i ).
thf(tp_c_Big__Operators_Olinorder__class_OMax,type,
c_Big__Operators_Olinorder__class_OMax: $i > $i > $i ).
thf(tp_c_Big__Operators_Olinorder__class_OMin,type,
c_Big__Operators_Olinorder__class_OMin: $i > $i > $i ).
thf(tp_c_Big__Operators_Osemilattice__big,type,
c_Big__Operators_Osemilattice__big: $i > $i > $i > $o ).
thf(tp_c_COMBB,type,
c_COMBB: $i > $i > $i > $i ).
thf(tp_c_COMBC,type,
c_COMBC: $i > $i > $i > $i ).
thf(tp_c_COMBI,type,
c_COMBI: $i > $i ).
thf(tp_c_COMBK,type,
c_COMBK: $i > $i > $i ).
thf(tp_c_COMBS,type,
c_COMBS: $i > $i > $i > $i ).
thf(tp_c_Code__Numeral_OSuc__code__numeral,type,
c_Code__Numeral_OSuc__code__numeral: $i > $i ).
thf(tp_c_Code__Numeral_Ocode__numeral_Ocode__numeral__case,type,
c_Code__Numeral_Ocode__numeral_Ocode__numeral__case: $i > $i > $i > $i > $i ).
thf(tp_c_Code__Numeral_Ocode__numeral_Ocode__numeral__rec,type,
c_Code__Numeral_Ocode__numeral_Ocode__numeral__rec: $i > $i > $i > $i > $i ).
thf(tp_c_Code__Numeral_Ocode__numeral_Ocode__numeral__size,type,
c_Code__Numeral_Ocode__numeral_Ocode__numeral__size: $i > $i ).
thf(tp_c_Code__Numeral_Odiv__mod__code__numeral,type,
c_Code__Numeral_Odiv__mod__code__numeral: $i > $i > $i ).
thf(tp_c_Code__Numeral_Oint__of,type,
c_Code__Numeral_Oint__of: $i ).
thf(tp_c_Code__Numeral_Onat__of,type,
c_Code__Numeral_Onat__of: $i ).
thf(tp_c_Code__Numeral_Onat__of__aux,type,
c_Code__Numeral_Onat__of__aux: $i > $i > $i ).
thf(tp_c_Code__Numeral_Oof__nat,type,
c_Code__Numeral_Oof__nat: $i ).
thf(tp_c_Code__Numeral_Osubtract__code__numeral,type,
c_Code__Numeral_Osubtract__code__numeral: $i ).
thf(tp_c_Com_OArg,type,
c_Com_OArg: $i ).
thf(tp_c_Com_ORes,type,
c_Com_ORes: $i ).
thf(tp_c_Com_OWT,type,
c_Com_OWT: $i ).
thf(tp_c_Com_OWT__bodies,type,
c_Com_OWT__bodies: $o ).
thf(tp_c_Com_Obodies,type,
c_Com_Obodies: $i ).
thf(tp_c_Com_Obody,type,
c_Com_Obody: $i ).
thf(tp_c_Com_Ocom_OAss,type,
c_Com_Ocom_OAss: $i > $i > $i ).
thf(tp_c_Com_Ocom_OBODY,type,
c_Com_Ocom_OBODY: $i ).
thf(tp_c_Com_Ocom_OCall,type,
c_Com_Ocom_OCall: $i > $i > $i > $i ).
thf(tp_c_Com_Ocom_OCond,type,
c_Com_Ocom_OCond: $i > $i > $i > $i ).
thf(tp_c_Com_Ocom_OLocal,type,
c_Com_Ocom_OLocal: $i > $i > $i > $i ).
thf(tp_c_Com_Ocom_OSKIP,type,
c_Com_Ocom_OSKIP: $i ).
thf(tp_c_Com_Ocom_OSemi,type,
c_Com_Ocom_OSemi: $i > $i > $i ).
thf(tp_c_Com_Ocom_OWhile,type,
c_Com_Ocom_OWhile: $i > $i > $i ).
thf(tp_c_Com_Ocom_Ocom__case,type,
c_Com_Ocom_Ocom__case: $i > $i > $i > $i > $i > $i > $i > $i > $i > $i > $i ).
thf(tp_c_Com_Ocom_Ocom__rec,type,
c_Com_Ocom_Ocom__rec: $i > $i > $i > $i > $i > $i > $i > $i > $i > $i > $i ).
thf(tp_c_Com_Ocom_Ocom__size,type,
c_Com_Ocom_Ocom__size: $i > $i ).
thf(tp_c_Com_Ovname_OGlb,type,
c_Com_Ovname_OGlb: $i > $i ).
thf(tp_c_Com_Ovname_OLoc,type,
c_Com_Ovname_OLoc: $i > $i ).
thf(tp_c_Com_Ovname_Ovname__case,type,
c_Com_Ovname_Ovname__case: $i > $i > $i > $i > $i ).
thf(tp_c_Com_Ovname_Ovname__rec,type,
c_Com_Ovname_Ovname__rec: $i > $i > $i > $i > $i ).
thf(tp_c_Com_Ovname_Ovname__size,type,
c_Com_Ovname_Ovname__size: $i > $i ).
thf(tp_c_Complete__Lattice_OInf__class_OInf,type,
c_Complete__Lattice_OInf__class_OInf: $i > $i > $i ).
thf(tp_c_Complete__Lattice_OSup__class_OSup,type,
c_Complete__Lattice_OSup__class_OSup: $i > $i > $i ).
thf(tp_c_Complete__Lattice_Ocomplete__lattice__class_OINFI,type,
c_Complete__Lattice_Ocomplete__lattice__class_OINFI: $i > $i > $i ).
thf(tp_c_Complete__Lattice_Ocomplete__lattice__class_OSUPR,type,
c_Complete__Lattice_Ocomplete__lattice__class_OSUPR: $i > $i > $i ).
thf(tp_c_DSequence_Oempty,type,
c_DSequence_Oempty: $i > $i ).
thf(tp_c_DSequence_Osingle,type,
c_DSequence_Osingle: $i > $i ).
thf(tp_c_DSequence_Ounion,type,
c_DSequence_Ounion: $i > $i ).
thf(tp_c_Divides_Oadjust,type,
c_Divides_Oadjust: $i > $i ).
thf(tp_c_Divides_Odiv__class_Odiv,type,
c_Divides_Odiv__class_Odiv: $i > $i ).
thf(tp_c_Divides_Odiv__class_Omod,type,
c_Divides_Odiv__class_Omod: $i > $i > $i > $i ).
thf(tp_c_Divides_Odivmod__int,type,
c_Divides_Odivmod__int: $i > $i > $i ).
thf(tp_c_Divides_Odivmod__int__rel,type,
c_Divides_Odivmod__int__rel: $i > $i > $i ).
thf(tp_c_Divides_Odivmod__nat,type,
c_Divides_Odivmod__nat: $i > $i > $i ).
thf(tp_c_Divides_Odivmod__nat__rel,type,
c_Divides_Odivmod__nat__rel: $i > $i > $i ).
thf(tp_c_Divides_OnegDivAlg,type,
c_Divides_OnegDivAlg: $i > $i > $i ).
thf(tp_c_Divides_OnegDivAlg__rel,type,
c_Divides_OnegDivAlg__rel: $i ).
thf(tp_c_Divides_OnegateSnd,type,
c_Divides_OnegateSnd: $i ).
thf(tp_c_Divides_Opdivmod,type,
c_Divides_Opdivmod: $i > $i > $i ).
thf(tp_c_Divides_OposDivAlg,type,
c_Divides_OposDivAlg: $i > $i > $i ).
thf(tp_c_Divides_OposDivAlg__rel,type,
c_Divides_OposDivAlg__rel: $i ).
thf(tp_c_Equiv__Relations_Ocongruent,type,
c_Equiv__Relations_Ocongruent: $i > $i > $i > $i > $o ).
thf(tp_c_Equiv__Relations_Ocongruent2,type,
c_Equiv__Relations_Ocongruent2: $i > $i > $i > $i > $i > $i > $o ).
thf(tp_c_Equiv__Relations_Oequiv,type,
c_Equiv__Relations_Oequiv: $i > $i > $i > $o ).
thf(tp_c_Equiv__Relations_Oequivp,type,
c_Equiv__Relations_Oequivp: $i > $i > $o ).
thf(tp_c_Equiv__Relations_Oquotient,type,
c_Equiv__Relations_Oquotient: $i > $i ).
thf(tp_c_Finite__Set_Ocard,type,
c_Finite__Set_Ocard: $i > $i ).
thf(tp_c_Finite__Set_Ofinite,type,
c_Finite__Set_Ofinite: $i > $i ).
thf(tp_c_Finite__Set_Ofold,type,
c_Finite__Set_Ofold: $i > $i > $i > $i ).
thf(tp_c_Finite__Set_Ofold1,type,
c_Finite__Set_Ofold1: $i > $i > $i ).
thf(tp_c_Finite__Set_Ofold1Set,type,
c_Finite__Set_Ofold1Set: $i > $i > $i > $i ).
thf(tp_c_Finite__Set_Ofold__graph,type,
c_Finite__Set_Ofold__graph: $i > $i > $i > $i > $i > $i ).
thf(tp_c_Finite__Set_Ofold__image,type,
c_Finite__Set_Ofold__image: $i > $i > $i > $i ).
thf(tp_c_Finite__Set_Ofolding,type,
c_Finite__Set_Ofolding: $i > $i > $i > $i > $o ).
thf(tp_c_Finite__Set_Ofolding__idem,type,
c_Finite__Set_Ofolding__idem: $i > $i > $i > $i > $o ).
thf(tp_c_Finite__Set_Ofolding__image,type,
c_Finite__Set_Ofolding__image: $i > $i > $i > $i > $i > $o ).
thf(tp_c_Finite__Set_Ofolding__image__simple,type,
c_Finite__Set_Ofolding__image__simple: $i > $i > $i > $i > $i > $i > $o ).
thf(tp_c_Finite__Set_Ofolding__image__simple__idem,type,
c_Finite__Set_Ofolding__image__simple__idem: $i > $i > $i > $i > $i > $i > $o ).
thf(tp_c_Finite__Set_Ofolding__one,type,
c_Finite__Set_Ofolding__one: $i > $i > $i > $o ).
thf(tp_c_Finite__Set_Ofolding__one__idem,type,
c_Finite__Set_Ofolding__one__idem: $i > $i > $i > $o ).
thf(tp_c_Finite__Set_Ofun__left__comm,type,
c_Finite__Set_Ofun__left__comm: $i > $i > $i > $o ).
thf(tp_c_Finite__Set_Ofun__left__comm__idem,type,
c_Finite__Set_Ofun__left__comm__idem: $i > $i > $i > $o ).
thf(tp_c_FunDef_Oin__rel,type,
c_FunDef_Oin__rel: $i > $i > $i > $i ).
thf(tp_c_FunDef_Omax__strict,type,
c_FunDef_Omax__strict: $i ).
thf(tp_c_FunDef_Omax__weak,type,
c_FunDef_Omax__weak: $i ).
thf(tp_c_FunDef_Omin__strict,type,
c_FunDef_Omin__strict: $i ).
thf(tp_c_FunDef_Omin__weak,type,
c_FunDef_Omin__weak: $i ).
thf(tp_c_FunDef_Opair__leq,type,
c_FunDef_Opair__leq: $i ).
thf(tp_c_FunDef_Opair__less,type,
c_FunDef_Opair__less: $i ).
thf(tp_c_FunDef_Oreduction__pair,type,
c_FunDef_Oreduction__pair: $i > $i > $o ).
thf(tp_c_FunDef_Orp__inv__image,type,
c_FunDef_Orp__inv__image: $i > $i > $i ).
thf(tp_c_Fun_Ocomp,type,
c_Fun_Ocomp: $i > $i > $i > $i > $i ).
thf(tp_c_Fun_Ofun__upd,type,
c_Fun_Ofun__upd: $i > $i > $i ).
thf(tp_c_Fun_Oid,type,
c_Fun_Oid: $i > $i ).
thf(tp_c_Fun_Oinj__on,type,
c_Fun_Oinj__on: $i > $i > $i > $i > $o ).
thf(tp_c_Fun_Ooverride__on,type,
c_Fun_Ooverride__on: $i > $i > $i > $i > $i > $i ).
thf(tp_c_Fun_Othe__inv__into,type,
c_Fun_Othe__inv__into: $i > $i > $i > $i > $i ).
thf(tp_c_Groups_Oabs__class_Oabs,type,
c_Groups_Oabs__class_Oabs: $i > $i ).
thf(tp_c_Groups_Ominus__class_Ominus,type,
c_Groups_Ominus__class_Ominus: $i > $i ).
thf(tp_c_Groups_Oone__class_Oone,type,
c_Groups_Oone__class_Oone: $i > $i ).
thf(tp_c_Groups_Oplus__class_Oplus,type,
c_Groups_Oplus__class_Oplus: $i > $i ).
thf(tp_c_Groups_Osgn__class_Osgn,type,
c_Groups_Osgn__class_Osgn: $i > $i > $i ).
thf(tp_c_Groups_Otimes__class_Otimes,type,
c_Groups_Otimes__class_Otimes: $i > $i ).
thf(tp_c_Groups_Ouminus__class_Ouminus,type,
c_Groups_Ouminus__class_Ouminus: $i > $i ).
thf(tp_c_Groups_Ozero__class_Ozero,type,
c_Groups_Ozero__class_Ozero: $i > $i ).
thf(tp_c_HOL_OAll,type,
c_HOL_OAll: $i > $i ).
thf(tp_c_HOL_OEx,type,
c_HOL_OEx: $i > $i ).
thf(tp_c_HOL_OLet,type,
c_HOL_OLet: $i > $i > $i ).
thf(tp_c_HOL_OThe,type,
c_HOL_OThe: $i > $i > $i ).
thf(tp_c_HOL_Obool_Obool__size,type,
c_HOL_Obool_Obool__size: $i > $i ).
thf(tp_c_Hilbert__Choice_OEps,type,
c_Hilbert__Choice_OEps: $i > $i > $i ).
thf(tp_c_Hoare__Mirabelle_OMGT,type,
c_Hoare__Mirabelle_OMGT: $i > $i ).
thf(tp_c_Hoare__Mirabelle_Ohoare__derivs,type,
c_Hoare__Mirabelle_Ohoare__derivs: $i > $i > $i > $o ).
thf(tp_c_Hoare__Mirabelle_Ohoare__valids,type,
c_Hoare__Mirabelle_Ohoare__valids: $i > $i > $i > $o ).
thf(tp_c_Hoare__Mirabelle_Opeek__and,type,
c_Hoare__Mirabelle_Opeek__and: $i > $i > $i > $i ).
thf(tp_c_Hoare__Mirabelle_Otriple_Otriple,type,
c_Hoare__Mirabelle_Otriple_Otriple: $i > $i ).
thf(tp_c_Hoare__Mirabelle_Otriple_Otriple__case,type,
c_Hoare__Mirabelle_Otriple_Otriple__case: $i > $i > $i > $i > $i ).
thf(tp_c_Hoare__Mirabelle_Otriple_Otriple__rec,type,
c_Hoare__Mirabelle_Otriple_Otriple__rec: $i > $i > $i > $i > $i ).
thf(tp_c_Hoare__Mirabelle_Otriple_Otriple__size,type,
c_Hoare__Mirabelle_Otriple_Otriple__size: $i > $i > $i > $i ).
thf(tp_c_Hoare__Mirabelle_Otriple__valid,type,
c_Hoare__Mirabelle_Otriple__valid: $i > $i > $i > $o ).
thf(tp_c_If,type,
c_If: $i > $i ).
thf(tp_c_Int_OAbs__Integ,type,
c_Int_OAbs__Integ: $i ).
thf(tp_c_Int_OBit0,type,
c_Int_OBit0: $i > $i ).
thf(tp_c_Int_OBit1,type,
c_Int_OBit1: $i > $i ).
thf(tp_c_Int_OInteg,type,
c_Int_OInteg: $i ).
thf(tp_c_Int_OMin,type,
c_Int_OMin: $i ).
thf(tp_c_Int_OPls,type,
c_Int_OPls: $i ).
thf(tp_c_Int_ORep__Integ,type,
c_Int_ORep__Integ: $i ).
thf(tp_c_Int_Oint__ge__less__than,type,
c_Int_Oint__ge__less__than: $i > $i ).
thf(tp_c_Int_Oint__ge__less__than2,type,
c_Int_Oint__ge__less__than2: $i > $i ).
thf(tp_c_Int_Ointrel,type,
c_Int_Ointrel: $i ).
thf(tp_c_Int_Oiszero,type,
c_Int_Oiszero: $i > $i > $o ).
thf(tp_c_Int_Onat,type,
c_Int_Onat: $i ).
thf(tp_c_Int_Onat__aux,type,
c_Int_Onat__aux: $i > $i > $i ).
thf(tp_c_Int_Onumber__class_Onumber__of,type,
c_Int_Onumber__class_Onumber__of: $i > $i ).
thf(tp_c_Int_Opred,type,
c_Int_Opred: $i > $i ).
thf(tp_c_Int_Oring__1__class_OInts,type,
c_Int_Oring__1__class_OInts: $i > $i ).
thf(tp_c_Int_Oring__1__class_Oof__int,type,
c_Int_Oring__1__class_Oof__int: $i > $i ).
thf(tp_c_Int_Osucc,type,
c_Int_Osucc: $i > $i ).
thf(tp_c_Lattices_Osemilattice__inf__class_Oinf,type,
c_Lattices_Osemilattice__inf__class_Oinf: $i > $i ).
thf(tp_c_Lattices_Osemilattice__sup__class_Osup,type,
c_Lattices_Osemilattice__sup__class_Osup: $i > $i ).
thf(tp_c_Lazy__Sequence_Oanamorph,type,
c_Lazy__Sequence_Oanamorph: $i > $i > $i > $i > $i ).
thf(tp_c_Lazy__Sequence_Obind,type,
c_Lazy__Sequence_Obind: $i > $i > $i > $i > $i ).
thf(tp_c_Lazy__Sequence_Oempty,type,
c_Lazy__Sequence_Oempty: $i > $i ).
thf(tp_c_Lazy__Sequence_Ohb__bind,type,
c_Lazy__Sequence_Ohb__bind: $i > $i > $i > $i > $i ).
thf(tp_c_Lazy__Sequence_Ohb__not__seq,type,
c_Lazy__Sequence_Ohb__not__seq: $i > $i ).
thf(tp_c_Lazy__Sequence_Ohb__single,type,
c_Lazy__Sequence_Ohb__single: $i > $i > $i ).
thf(tp_c_Lazy__Sequence_Ohit__bound,type,
c_Lazy__Sequence_Ohit__bound: $i > $i ).
thf(tp_c_Lazy__Sequence_Osingle,type,
c_Lazy__Sequence_Osingle: $i > $i > $i ).
thf(tp_c_List_Oappend,type,
c_List_Oappend: $i > $i ).
thf(tp_c_List_Obutlast,type,
c_List_Obutlast: $i > $i > $i ).
thf(tp_c_List_Oconcat,type,
c_List_Oconcat: $i > $i > $i ).
thf(tp_c_List_Odistinct,type,
c_List_Odistinct: $i > $i ).
thf(tp_c_List_Odrop,type,
c_List_Odrop: $i > $i ).
thf(tp_c_List_Ofilter,type,
c_List_Ofilter: $i > $i > $i ).
thf(tp_c_List_Ofoldl,type,
c_List_Ofoldl: $i > $i > $i > $i > $i ).
thf(tp_c_List_Ofoldr,type,
c_List_Ofoldr: $i > $i > $i > $i > $i > $i ).
thf(tp_c_List_Ohd,type,
c_List_Ohd: $i > $i ).
thf(tp_c_List_Olast,type,
c_List_Olast: $i > $i > $i ).
thf(tp_c_List_Olenlex,type,
c_List_Olenlex: $i > $i > $i ).
thf(tp_c_List_Olex,type,
c_List_Olex: $i > $i > $i ).
thf(tp_c_List_Olexn,type,
c_List_Olexn: $i > $i > $i ).
thf(tp_c_List_Olexord,type,
c_List_Olexord: $i > $i > $i ).
thf(tp_c_List_Olinorder__class_Oinsort__insert__key,type,
c_List_Olinorder__class_Oinsort__insert__key: $i > $i > $i > $i > $i > $i ).
thf(tp_c_List_Olinorder__class_Oinsort__key,type,
c_List_Olinorder__class_Oinsort__key: $i > $i > $i > $i ).
thf(tp_c_List_Olinorder__class_Osorted,type,
c_List_Olinorder__class_Osorted: $i > $i > $o ).
thf(tp_c_List_Olinorder__class_Osorted__list__of__set,type,
c_List_Olinorder__class_Osorted__list__of__set: $i > $i > $i ).
thf(tp_c_List_Olist_OCons,type,
c_List_Olist_OCons: $i > $i ).
thf(tp_c_List_Olist_ONil,type,
c_List_Olist_ONil: $i > $i ).
thf(tp_c_List_Olist_Olist__case,type,
c_List_Olist_Olist__case: $i > $i > $i > $i > $i ).
thf(tp_c_List_Olist_Olist__size,type,
c_List_Olist_Olist__size: $i > $i > $i > $i ).
thf(tp_c_List_Olist__update,type,
c_List_Olist__update: $i > $i > $i ).
thf(tp_c_List_Olistrel,type,
c_List_Olistrel: $i > $i > $i ).
thf(tp_c_List_Olistrel1,type,
c_List_Olistrel1: $i > $i > $i ).
thf(tp_c_List_Olistrelp,type,
c_List_Olistrelp: $i > $i > $i > $i > $o ).
thf(tp_c_List_Olists,type,
c_List_Olists: $i > $i > $i ).
thf(tp_c_List_Olistset,type,
c_List_Olistset: $i > $i > $i ).
thf(tp_c_List_Omap,type,
c_List_Omap: $i > $i > $i ).
thf(tp_c_List_Omap__filter,type,
c_List_Omap__filter: $i > $i > $i > $i > $i ).
thf(tp_c_List_Omonoid__add__class_Olistsum,type,
c_List_Omonoid__add__class_Olistsum: $i > $i ).
thf(tp_c_List_Onat__list,type,
c_List_Onat__list: $i > $o ).
thf(tp_c_List_Onth,type,
c_List_Onth: $i > $i ).
thf(tp_c_List_Opartition,type,
c_List_Opartition: $i > $i > $i > $i ).
thf(tp_c_List_Oremove1,type,
c_List_Oremove1: $i > $i > $i > $i ).
thf(tp_c_List_Orev,type,
c_List_Orev: $i > $i ).
thf(tp_c_List_Orotate,type,
c_List_Orotate: $i > $i > $i ).
thf(tp_c_List_Orotate1,type,
c_List_Orotate1: $i > $i ).
thf(tp_c_List_Oset,type,
c_List_Oset: $i > $i ).
thf(tp_c_List_Oset__Cons,type,
c_List_Oset__Cons: $i > $i > $i > $i ).
thf(tp_c_List_Osublist,type,
c_List_Osublist: $i > $i > $i > $i ).
thf(tp_c_List_Otake,type,
c_List_Otake: $i > $i ).
thf(tp_c_List_Otl,type,
c_List_Otl: $i > $i > $i ).
thf(tp_c_List_Otranspose,type,
c_List_Otranspose: $i > $i > $i ).
thf(tp_c_List_Otranspose__rel,type,
c_List_Otranspose__rel: $i > $i ).
thf(tp_c_List_Oupt,type,
c_List_Oupt: $i > $i > $i ).
thf(tp_c_List_Oupto,type,
c_List_Oupto: $i > $i > $i ).
thf(tp_c_List_Oupto__rel,type,
c_List_Oupto__rel: $i ).
thf(tp_c_List_Ozip,type,
c_List_Ozip: $i > $i > $i ).
thf(tp_c_Map_Odom,type,
c_Map_Odom: $i > $i > $i > $i ).
thf(tp_c_Map_Omap__add,type,
c_Map_Omap__add: $i > $i > $i > $i > $i ).
thf(tp_c_Map_Omap__comp,type,
c_Map_Omap__comp: $i > $i > $i > $i > $i > $i > $i ).
thf(tp_c_Map_Omap__of,type,
c_Map_Omap__of: $i > $i > $i > $i ).
thf(tp_c_Map_Omap__upds,type,
c_Map_Omap__upds: $i > $i > $i > $i > $i > $i ).
thf(tp_c_Map_Oran,type,
c_Map_Oran: $i > $i > $i > $i ).
thf(tp_c_Map_Orestrict__map,type,
c_Map_Orestrict__map: $i > $i > $i > $i > $i ).
thf(tp_c_Nat_OSuc,type,
c_Nat_OSuc: $i ).
thf(tp_c_Nat_Ocompow,type,
c_Nat_Ocompow: $i > $i > $i ).
thf(tp_c_Nat_Ofunpow,type,
c_Nat_Ofunpow: $i > $i ).
thf(tp_c_Nat_Onat_Onat__case,type,
c_Nat_Onat_Onat__case: $i > $i > $i > $i > $i ).
thf(tp_c_Nat_Onat_Onat__rec,type,
c_Nat_Onat_Onat__rec: $i > $i > $i > $i ).
thf(tp_c_Nat_Onat_Onat__size,type,
c_Nat_Onat_Onat__size: $i > $i ).
thf(tp_c_Nat_Osemiring__1__class_ONats,type,
c_Nat_Osemiring__1__class_ONats: $i > $i ).
thf(tp_c_Nat_Osemiring__1__class_Oof__nat,type,
c_Nat_Osemiring__1__class_Oof__nat: $i > $i ).
thf(tp_c_Nat_Osemiring__1__class_Oof__nat__aux,type,
c_Nat_Osemiring__1__class_Oof__nat__aux: $i > $i > $i > $i > $i ).
thf(tp_c_Nat_Osize__class_Osize,type,
c_Nat_Osize__class_Osize: $i > $i ).
thf(tp_c_Nat__Numeral_Oneg,type,
c_Nat__Numeral_Oneg: $i ).
thf(tp_c_Nat__Transfer_Ois__nat,type,
c_Nat__Transfer_Ois__nat: $i > $o ).
thf(tp_c_Nat__Transfer_Onat__set,type,
c_Nat__Transfer_Onat__set: $i > $o ).
thf(tp_c_Nat__Transfer_Otransfer__morphism,type,
c_Nat__Transfer_Otransfer__morphism: $i > $i > $i > $i > $o ).
thf(tp_c_Nat__Transfer_Otsub,type,
c_Nat__Transfer_Otsub: $i > $i > $i ).
thf(tp_c_Natural_Oevalc,type,
c_Natural_Oevalc: $i > $i ).
thf(tp_c_Natural_Oevaln,type,
c_Natural_Oevaln: $i > $i > $i > $i > $o ).
thf(tp_c_Natural_Ogetlocs,type,
c_Natural_Ogetlocs: $i ).
thf(tp_c_Natural_Onewlocs,type,
c_Natural_Onewlocs: $i ).
thf(tp_c_Natural_Osetlocs,type,
c_Natural_Osetlocs: $i ).
thf(tp_c_Natural_Oupdate,type,
c_Natural_Oupdate: $i ).
thf(tp_c_New__DSequence_Oneg__bind,type,
c_New__DSequence_Oneg__bind: $i > $i > $i > $i > $i ).
thf(tp_c_New__DSequence_Oneg__decr__bind,type,
c_New__DSequence_Oneg__decr__bind: $i > $i > $i > $i > $i ).
thf(tp_c_New__DSequence_Oneg__single,type,
c_New__DSequence_Oneg__single: $i > $i > $i ).
thf(tp_c_New__DSequence_Opos__bind,type,
c_New__DSequence_Opos__bind: $i > $i > $i > $i > $i ).
thf(tp_c_New__DSequence_Opos__decr__bind,type,
c_New__DSequence_Opos__decr__bind: $i > $i > $i > $i > $i ).
thf(tp_c_New__DSequence_Opos__empty,type,
c_New__DSequence_Opos__empty: $i > $i ).
thf(tp_c_New__DSequence_Opos__not__seq,type,
c_New__DSequence_Opos__not__seq: $i > $i ).
thf(tp_c_New__DSequence_Opos__single,type,
c_New__DSequence_Opos__single: $i > $i > $i ).
thf(tp_c_New__Random__Sequence_Oneg__bind,type,
c_New__Random__Sequence_Oneg__bind: $i > $i > $i > $i > $i ).
thf(tp_c_New__Random__Sequence_Oneg__decr__bind,type,
c_New__Random__Sequence_Oneg__decr__bind: $i > $i > $i > $i > $i > $i > $i > $i ).
thf(tp_c_New__Random__Sequence_Oneg__map,type,
c_New__Random__Sequence_Oneg__map: $i > $i > $i > $i > $i ).
thf(tp_c_New__Random__Sequence_Oneg__single,type,
c_New__Random__Sequence_Oneg__single: $i > $i ).
thf(tp_c_New__Random__Sequence_Opos__bind,type,
c_New__Random__Sequence_Opos__bind: $i > $i > $i > $i > $i ).
thf(tp_c_New__Random__Sequence_Opos__decr__bind,type,
c_New__Random__Sequence_Opos__decr__bind: $i > $i > $i > $i > $i > $i > $i > $i ).
thf(tp_c_New__Random__Sequence_Opos__empty,type,
c_New__Random__Sequence_Opos__empty: $i > $i > $i > $i > $i ).
thf(tp_c_New__Random__Sequence_Opos__map,type,
c_New__Random__Sequence_Opos__map: $i > $i > $i > $i > $i ).
thf(tp_c_New__Random__Sequence_Opos__not__random__dseq,type,
c_New__Random__Sequence_Opos__not__random__dseq: $i > $i > $i > $i > $i ).
thf(tp_c_New__Random__Sequence_Opos__single,type,
c_New__Random__Sequence_Opos__single: $i > $i ).
thf(tp_c_Nitpick_OAbs__Frac,type,
c_Nitpick_OAbs__Frac: $i > $i > $i ).
thf(tp_c_Nitpick_OFrac,type,
c_Nitpick_OFrac: $i ).
thf(tp_c_Nitpick_ORep__Frac,type,
c_Nitpick_ORep__Frac: $i > $i ).
thf(tp_c_Nitpick_Ocard_H,type,
c_Nitpick_Ocard_H: $i > $i > $i ).
thf(tp_c_Nitpick_Odenom,type,
c_Nitpick_Odenom: $i > $i ).
thf(tp_c_Nitpick_Ofold__graph_H,type,
c_Nitpick_Ofold__graph_H: $i > $i > $i > $i > $i > $i > $o ).
thf(tp_c_Nitpick_Ofrac,type,
c_Nitpick_Ofrac: $i > $i ).
thf(tp_c_Nitpick_Oint__gcd,type,
c_Nitpick_Oint__gcd: $i ).
thf(tp_c_Nitpick_Oint__lcm,type,
c_Nitpick_Oint__lcm: $i > $i > $i ).
thf(tp_c_Nitpick_Oinverse__frac,type,
c_Nitpick_Oinverse__frac: $i > $i > $i ).
thf(tp_c_Nitpick_Oless__eq__frac,type,
c_Nitpick_Oless__eq__frac: $i > $i > $i > $o ).
thf(tp_c_Nitpick_Oless__frac,type,
c_Nitpick_Oless__frac: $i > $i > $i > $o ).
thf(tp_c_Nitpick_Onat__gcd,type,
c_Nitpick_Onat__gcd: $i > $i > $i ).
thf(tp_c_Nitpick_Onat__gcd__rel,type,
c_Nitpick_Onat__gcd__rel: $i ).
thf(tp_c_Nitpick_Onat__lcm,type,
c_Nitpick_Onat__lcm: $i > $i > $i ).
thf(tp_c_Nitpick_Onorm__frac,type,
c_Nitpick_Onorm__frac: $i > $i > $i ).
thf(tp_c_Nitpick_Onorm__frac__rel,type,
c_Nitpick_Onorm__frac__rel: $i ).
thf(tp_c_Nitpick_Onum,type,
c_Nitpick_Onum: $i > $i ).
thf(tp_c_Nitpick_Onumber__of__frac,type,
c_Nitpick_Onumber__of__frac: $i > $i > $i ).
thf(tp_c_Nitpick_Oof__frac,type,
c_Nitpick_Oof__frac: $i > $i > $i > $i ).
thf(tp_c_Nitpick_Oone__frac,type,
c_Nitpick_Oone__frac: $i > $i ).
thf(tp_c_Nitpick_Opair__box_OPairBox,type,
c_Nitpick_Opair__box_OPairBox: $i > $i > $i > $i > $i ).
thf(tp_c_Nitpick_Opair__box_Opair__box__case,type,
c_Nitpick_Opair__box_Opair__box__case: $i > $i > $i > $i > $i > $i ).
thf(tp_c_Nitpick_Opair__box_Opair__box__rec,type,
c_Nitpick_Opair__box_Opair__box__rec: $i > $i > $i > $i > $i > $i ).
thf(tp_c_Nitpick_Opair__box_Opair__box__size,type,
c_Nitpick_Opair__box_Opair__box__size: $i > $i > $i > $i > $i > $i ).
thf(tp_c_Nitpick_Oplus__frac,type,
c_Nitpick_Oplus__frac: $i > $i > $i > $i ).
thf(tp_c_Nitpick_Oprod,type,
c_Nitpick_Oprod: $i > $i > $i > $i > $i ).
thf(tp_c_Nitpick_Orefl_H,type,
c_Nitpick_Orefl_H: $i > $i > $o ).
thf(tp_c_Nitpick_Osetsum_H,type,
c_Nitpick_Osetsum_H: $i > $i > $i > $i > $i ).
thf(tp_c_Nitpick_Otimes__frac,type,
c_Nitpick_Otimes__frac: $i > $i > $i > $i ).
thf(tp_c_Nitpick_Ouminus__frac,type,
c_Nitpick_Ouminus__frac: $i > $i > $i ).
thf(tp_c_Nitpick_Ounknown,type,
c_Nitpick_Ounknown: $i > $o ).
thf(tp_c_Nitpick_Owf_H,type,
c_Nitpick_Owf_H: $i > $i > $o ).
thf(tp_c_Nitpick_Ozero__frac,type,
c_Nitpick_Ozero__frac: $i > $i ).
thf(tp_c_Option_Ois__none,type,
c_Option_Ois__none: $i > $i > $o ).
thf(tp_c_Option_Omap,type,
c_Option_Omap: $i > $i > $i ).
thf(tp_c_Option_Ooption_ONone,type,
c_Option_Ooption_ONone: $i > $i ).
thf(tp_c_Option_Ooption_OSome,type,
c_Option_Ooption_OSome: $i > $i ).
thf(tp_c_Option_Ooption_Ooption__case,type,
c_Option_Ooption_Ooption__case: $i > $i > $i > $i > $i ).
thf(tp_c_Option_Ooption_Ooption__rec,type,
c_Option_Ooption_Ooption__rec: $i > $i > $i > $i > $i > $i ).
thf(tp_c_Option_Ooption_Ooption__size,type,
c_Option_Ooption_Ooption__size: $i > $i > $i > $i ).
thf(tp_c_Option_Oset,type,
c_Option_Oset: $i > $i > $i ).
thf(tp_c_Option_Othe,type,
c_Option_Othe: $i > $i ).
thf(tp_c_Orderings_Obot__class_Obot,type,
c_Orderings_Obot__class_Obot: $i > $i ).
thf(tp_c_Orderings_Oord_Omax,type,
c_Orderings_Oord_Omax: $i > $i > $i ).
thf(tp_c_Orderings_Oord_Omin,type,
c_Orderings_Oord_Omin: $i > $i > $i ).
thf(tp_c_Orderings_Oord__class_Oless,type,
c_Orderings_Oord__class_Oless: $i > $i ).
thf(tp_c_Orderings_Oord__class_Oless__eq,type,
c_Orderings_Oord__class_Oless__eq: $i > $i ).
thf(tp_c_Orderings_Oord__class_Omax,type,
c_Orderings_Oord__class_Omax: $i > $i ).
thf(tp_c_Orderings_Oord__class_Omin,type,
c_Orderings_Oord__class_Omin: $i > $i ).
thf(tp_c_Orderings_Oorder_Omono,type,
c_Orderings_Oorder_Omono: $i > $i > $i > $i > $o ).
thf(tp_c_Orderings_Oorder_Ostrict__mono,type,
c_Orderings_Oorder_Ostrict__mono: $i > $i > $i > $i > $o ).
thf(tp_c_Orderings_Otop__class_Otop,type,
c_Orderings_Otop__class_Otop: $i > $i ).
thf(tp_c_Partial__Function_Oflat__lub,type,
c_Partial__Function_Oflat__lub: $i > $i > $i > $i ).
thf(tp_c_Power_Opower_Opower,type,
c_Power_Opower_Opower: $i > $i > $i > $i ).
thf(tp_c_Power_Opower__class_Opower,type,
c_Power_Opower__class_Opower: $i > $i ).
thf(tp_c_Predicate_ODomainP,type,
c_Predicate_ODomainP: $i > $i > $i > $i ).
thf(tp_c_Predicate_OPowp,type,
c_Predicate_OPowp: $i > $i > $i ).
thf(tp_c_Predicate_ORangeP,type,
c_Predicate_ORangeP: $i > $i > $i > $i ).
thf(tp_c_Predicate_Opred__comp,type,
c_Predicate_Opred__comp: $i > $i > $i > $i > $i > $i > $i > $o ).
thf(tp_c_Predicate_Oreflp,type,
c_Predicate_Oreflp: $i > $i > $o ).
thf(tp_c_Product__Type_OPair,type,
c_Product__Type_OPair: $i > $i > $i ).
thf(tp_c_Product__Type_OSigma,type,
c_Product__Type_OSigma: $i > $i > $i ).
thf(tp_c_Product__Type_Oapfst,type,
c_Product__Type_Oapfst: $i > $i > $i > $i > $i ).
thf(tp_c_Product__Type_Oapsnd,type,
c_Product__Type_Oapsnd: $i > $i > $i > $i > $i ).
thf(tp_c_Product__Type_Ocurry,type,
c_Product__Type_Ocurry: $i > $i > $i > $i > $i ).
thf(tp_c_Product__Type_Ofst,type,
c_Product__Type_Ofst: $i > $i > $i ).
thf(tp_c_Product__Type_Ointernal__split,type,
c_Product__Type_Ointernal__split: $i > $i > $i > $i ).
thf(tp_c_Product__Type_Omap__pair,type,
c_Product__Type_Omap__pair: $i > $i > $i > $i > $i > $i > $i ).
thf(tp_c_Product__Type_Oprod_Oprod__case,type,
c_Product__Type_Oprod_Oprod__case: $i > $i > $i > $i ).
thf(tp_c_Product__Type_Oprod_Oprod__rec,type,
c_Product__Type_Oprod_Oprod__rec: $i > $i > $i > $i > $i > $i ).
thf(tp_c_Product__Type_Oprod_Oprod__size,type,
c_Product__Type_Oprod_Oprod__size: $i > $i > $i > $i > $i > $i ).
thf(tp_c_Product__Type_Oscomp,type,
c_Product__Type_Oscomp: $i > $i > $i > $i > $i ).
thf(tp_c_Product__Type_Osnd,type,
c_Product__Type_Osnd: $i > $i > $i ).
thf(tp_c_Quickcheck_Obeyond,type,
c_Quickcheck_Obeyond: $i > $i > $i ).
thf(tp_c_Random_Oinc__shift,type,
c_Random_Oinc__shift: $i > $i > $i ).
thf(tp_c_Random_Oiterate,type,
c_Random_Oiterate: $i > $i > $i > $i > $i ).
thf(tp_c_Random_Olog,type,
c_Random_Olog: $i > $i > $i ).
thf(tp_c_Random_Ominus__shift,type,
c_Random_Ominus__shift: $i > $i > $i > $i ).
thf(tp_c_Random_Opick,type,
c_Random_Opick: $i > $i > $i ).
thf(tp_c_Random_Orange,type,
c_Random_Orange: $i > $i ).
thf(tp_c_Random_Oselect,type,
c_Random_Oselect: $i > $i > $i ).
thf(tp_c_Random_Oselect__weight,type,
c_Random_Oselect__weight: $i > $i > $i ).
thf(tp_c_Random__Sequence_ORandom,type,
c_Random__Sequence_ORandom: $i > $i > $i > $i > $i ).
thf(tp_c_Random__Sequence_Obind,type,
c_Random__Sequence_Obind: $i > $i > $i > $i > $i ).
thf(tp_c_Random__Sequence_Oempty,type,
c_Random__Sequence_Oempty: $i > $i > $i > $i ).
thf(tp_c_Random__Sequence_Omap,type,
c_Random__Sequence_Omap: $i > $i > $i > $i > $i ).
thf(tp_c_Random__Sequence_Osingle,type,
c_Random__Sequence_Osingle: $i > $i ).
thf(tp_c_Recdef_Osame__fst,type,
c_Recdef_Osame__fst: $i > $i > $i > $i > $i ).
thf(tp_c_Relation_ODomain,type,
c_Relation_ODomain: $i > $i > $i ).
thf(tp_c_Relation_OField,type,
c_Relation_OField: $i > $i ).
thf(tp_c_Relation_OId,type,
c_Relation_OId: $i > $i ).
thf(tp_c_Relation_OId__on,type,
c_Relation_OId__on: $i > $i > $i ).
thf(tp_c_Relation_OImage,type,
c_Relation_OImage: $i > $i > $i > $i ).
thf(tp_c_Relation_ORange,type,
c_Relation_ORange: $i > $i > $i ).
thf(tp_c_Relation_Oconverse,type,
c_Relation_Oconverse: $i > $i > $i ).
thf(tp_c_Relation_Oinv__image,type,
c_Relation_Oinv__image: $i > $i > $i ).
thf(tp_c_Relation_Oirrefl,type,
c_Relation_Oirrefl: $i > $i > $o ).
thf(tp_c_Relation_Orefl__on,type,
c_Relation_Orefl__on: $i > $i > $i > $o ).
thf(tp_c_Relation_Orel__comp,type,
c_Relation_Orel__comp: $i > $i > $i > $i ).
thf(tp_c_Relation_Osingle__valued,type,
c_Relation_Osingle__valued: $i > $i > $i > $o ).
thf(tp_c_Relation_Ototal__on,type,
c_Relation_Ototal__on: $i > $i > $i > $o ).
thf(tp_c_Rings_Odvd__class_Odvd,type,
c_Rings_Odvd__class_Odvd: $i > $i ).
thf(tp_c_Rings_Oinverse__class_Odivide,type,
c_Rings_Oinverse__class_Odivide: $i > $i ).
thf(tp_c_SMT_Oz3div,type,
c_SMT_Oz3div: $i > $i > $i ).
thf(tp_c_SMT_Oz3mod,type,
c_SMT_Oz3mod: $i > $i > $i ).
thf(tp_c_SetInterval_Oord_OatLeast,type,
c_SetInterval_Oord_OatLeast: $i > $i > $i > $i ).
thf(tp_c_SetInterval_Oord_OatLeastAtMost,type,
c_SetInterval_Oord_OatLeastAtMost: $i > $i > $i > $i > $i ).
thf(tp_c_SetInterval_Oord_OatLeastLessThan,type,
c_SetInterval_Oord_OatLeastLessThan: $i > $i > $i > $i > $i > $i ).
thf(tp_c_SetInterval_Oord_OatMost,type,
c_SetInterval_Oord_OatMost: $i > $i > $i > $i ).
thf(tp_c_SetInterval_Oord_OgreaterThan,type,
c_SetInterval_Oord_OgreaterThan: $i > $i > $i > $i ).
thf(tp_c_SetInterval_Oord_OgreaterThanAtMost,type,
c_SetInterval_Oord_OgreaterThanAtMost: $i > $i > $i > $i > $i > $i ).
thf(tp_c_SetInterval_Oord_OgreaterThanLessThan,type,
c_SetInterval_Oord_OgreaterThanLessThan: $i > $i > $i > $i > $i ).
thf(tp_c_SetInterval_Oord_OlessThan,type,
c_SetInterval_Oord_OlessThan: $i > $i > $i > $i ).
thf(tp_c_SetInterval_Oord__class_OatLeast,type,
c_SetInterval_Oord__class_OatLeast: $i > $i ).
thf(tp_c_SetInterval_Oord__class_OatLeastAtMost,type,
c_SetInterval_Oord__class_OatLeastAtMost: $i > $i > $i > $i ).
thf(tp_c_SetInterval_Oord__class_OatLeastLessThan,type,
c_SetInterval_Oord__class_OatLeastLessThan: $i > $i > $i ).
thf(tp_c_SetInterval_Oord__class_OatMost,type,
c_SetInterval_Oord__class_OatMost: $i > $i ).
thf(tp_c_SetInterval_Oord__class_OgreaterThan,type,
c_SetInterval_Oord__class_OgreaterThan: $i > $i ).
thf(tp_c_SetInterval_Oord__class_OgreaterThanAtMost,type,
c_SetInterval_Oord__class_OgreaterThanAtMost: $i > $i > $i > $i ).
thf(tp_c_SetInterval_Oord__class_OgreaterThanLessThan,type,
c_SetInterval_Oord__class_OgreaterThanLessThan: $i > $i > $i > $i ).
thf(tp_c_SetInterval_Oord__class_OlessThan,type,
c_SetInterval_Oord__class_OlessThan: $i > $i ).
thf(tp_c_Set_OBall,type,
c_Set_OBall: $i > $i ).
thf(tp_c_Set_OCollect,type,
c_Set_OCollect: $i > $i ).
thf(tp_c_Set_OPow,type,
c_Set_OPow: $i > $i ).
thf(tp_c_Set_Oimage,type,
c_Set_Oimage: $i > $i > $i > $i ).
thf(tp_c_Set_Oinsert,type,
c_Set_Oinsert: $i > $i ).
thf(tp_c_Set_Othe__elem,type,
c_Set_Othe__elem: $i > $i > $i ).
thf(tp_c_Set_Ovimage,type,
c_Set_Ovimage: $i > $i > $i > $i ).
thf(tp_c_Smallcheck_Ofull__small_H,type,
c_Smallcheck_Ofull__small_H: $i > $i > $i > $i ).
thf(tp_c_Smallcheck_Ofull__small__class_Ofull__small,type,
c_Smallcheck_Ofull__small__class_Ofull__small: $i > $i > $i > $i ).
thf(tp_c_Smallcheck_Oorelse,type,
c_Smallcheck_Oorelse: $i > $i > $i > $i ).
thf(tp_c_Smallcheck_Osmall_H,type,
c_Smallcheck_Osmall_H: $i > $i > $i > $i ).
thf(tp_c_Smallcheck_Osmall_H__rel,type,
c_Smallcheck_Osmall_H__rel: $i ).
thf(tp_c_Smallcheck_Osmall__class_Osmall,type,
c_Smallcheck_Osmall__class_Osmall: $i > $i ).
thf(tp_c_Sum__Type_OInl,type,
c_Sum__Type_OInl: $i > $i > $i ).
thf(tp_c_Sum__Type_OInr,type,
c_Sum__Type_OInr: $i > $i > $i ).
thf(tp_c_Sum__Type_OPlus,type,
c_Sum__Type_OPlus: $i > $i > $i > $i > $i ).
thf(tp_c_Sum__Type_OProjl,type,
c_Sum__Type_OProjl: $i > $i > $i > $i ).
thf(tp_c_Sum__Type_OProjr,type,
c_Sum__Type_OProjr: $i > $i > $i > $i ).
thf(tp_c_Sum__Type_OSuml,type,
c_Sum__Type_OSuml: $i > $i > $i > $i > $i ).
thf(tp_c_Sum__Type_OSumr,type,
c_Sum__Type_OSumr: $i > $i > $i > $i > $i ).
thf(tp_c_Sum__Type_Osum_Osum__case,type,
c_Sum__Type_Osum_Osum__case: $i > $i > $i > $i > $i > $i ).
thf(tp_c_Sum__Type_Osum_Osum__rec,type,
c_Sum__Type_Osum_Osum__rec: $i > $i > $i > $i > $i > $i > $i ).
thf(tp_c_Sum__Type_Osum_Osum__size,type,
c_Sum__Type_Osum_Osum__size: $i > $i > $i > $i > $i > $i ).
thf(tp_c_Transitive__Closure_Ortrancl,type,
c_Transitive__Closure_Ortrancl: $i > $i > $i ).
thf(tp_c_Transitive__Closure_Otrancl,type,
c_Transitive__Closure_Otrancl: $i > $i > $i ).
thf(tp_c_Typedef_Otype__definition,type,
c_Typedef_Otype__definition: $i > $i > $i > $i > $i > $o ).
thf(tp_c_Wellfounded_Oacc,type,
c_Wellfounded_Oacc: $i > $i > $i ).
thf(tp_c_Wellfounded_Oaccp,type,
c_Wellfounded_Oaccp: $i > $i > $i ).
thf(tp_c_Wellfounded_Oacyclic,type,
c_Wellfounded_Oacyclic: $i > $i > $o ).
thf(tp_c_Wellfounded_Ofinite__psubset,type,
c_Wellfounded_Ofinite__psubset: $i > $i ).
thf(tp_c_Wellfounded_Oless__than,type,
c_Wellfounded_Oless__than: $i ).
thf(tp_c_Wellfounded_Olex__prod,type,
c_Wellfounded_Olex__prod: $i > $i > $i > $i > $i ).
thf(tp_c_Wellfounded_Omax__ext,type,
c_Wellfounded_Omax__ext: $i > $i > $i ).
thf(tp_c_Wellfounded_Omax__extp,type,
c_Wellfounded_Omax__extp: $i > $i > $i > $i > $o ).
thf(tp_c_Wellfounded_Omeasure,type,
c_Wellfounded_Omeasure: $i > $i ).
thf(tp_c_Wellfounded_Omin__ext,type,
c_Wellfounded_Omin__ext: $i > $i > $i ).
thf(tp_c_Wellfounded_Omlex__prod,type,
c_Wellfounded_Omlex__prod: $i > $i > $i > $i ).
thf(tp_c_Wellfounded_Opred__nat,type,
c_Wellfounded_Opred__nat: $i ).
thf(tp_c_Wellfounded_Owf,type,
c_Wellfounded_Owf: $i > $i > $o ).
thf(tp_c_Wellfounded_OwfP,type,
c_Wellfounded_OwfP: $i > $i > $o ).
thf(tp_c_fFalse,type,
c_fFalse: $i ).
thf(tp_c_fNot,type,
c_fNot: $i ).
thf(tp_c_fTrue,type,
c_fTrue: $i ).
thf(tp_c_fconj,type,
c_fconj: $i ).
thf(tp_c_fdisj,type,
c_fdisj: $i ).
thf(tp_c_fequal,type,
c_fequal: $i ).
thf(tp_c_fimplies,type,
c_fimplies: $i ).
thf(tp_c_member,type,
c_member: $i > $i ).
thf(tp_class_Complete__Lattice_Ocomplete__lattice,type,
class_Complete__Lattice_Ocomplete__lattice: $i > $o ).
thf(tp_class_Divides_Oring__div,type,
class_Divides_Oring__div: $i > $o ).
thf(tp_class_Divides_Osemiring__div,type,
class_Divides_Osemiring__div: $i > $o ).
thf(tp_class_Fields_Ofield,type,
class_Fields_Ofield: $i > $o ).
thf(tp_class_Fields_Ofield__inverse__zero,type,
class_Fields_Ofield__inverse__zero: $i > $o ).
thf(tp_class_Fields_Olinordered__field,type,
class_Fields_Olinordered__field: $i > $o ).
thf(tp_class_Fields_Olinordered__field__inverse__zero,type,
class_Fields_Olinordered__field__inverse__zero: $i > $o ).
thf(tp_class_Finite__Set_Ofinite,type,
class_Finite__Set_Ofinite: $i > $o ).
thf(tp_class_Groups_Oab__group__add,type,
class_Groups_Oab__group__add: $i > $o ).
thf(tp_class_Groups_Oab__semigroup__add,type,
class_Groups_Oab__semigroup__add: $i > $o ).
thf(tp_class_Groups_Oab__semigroup__mult,type,
class_Groups_Oab__semigroup__mult: $i > $o ).
thf(tp_class_Groups_Oabs__if,type,
class_Groups_Oabs__if: $i > $o ).
thf(tp_class_Groups_Ocancel__ab__semigroup__add,type,
class_Groups_Ocancel__ab__semigroup__add: $i > $o ).
thf(tp_class_Groups_Ocancel__semigroup__add,type,
class_Groups_Ocancel__semigroup__add: $i > $o ).
thf(tp_class_Groups_Ocomm__monoid__add,type,
class_Groups_Ocomm__monoid__add: $i > $o ).
thf(tp_class_Groups_Ocomm__monoid__mult,type,
class_Groups_Ocomm__monoid__mult: $i > $o ).
thf(tp_class_Groups_Ogroup__add,type,
class_Groups_Ogroup__add: $i > $o ).
thf(tp_class_Groups_Olinordered__ab__group__add,type,
class_Groups_Olinordered__ab__group__add: $i > $o ).
thf(tp_class_Groups_Olinordered__ab__semigroup__add,type,
class_Groups_Olinordered__ab__semigroup__add: $i > $o ).
thf(tp_class_Groups_Ominus,type,
class_Groups_Ominus: $i > $o ).
thf(tp_class_Groups_Omonoid__add,type,
class_Groups_Omonoid__add: $i > $o ).
thf(tp_class_Groups_Omonoid__mult,type,
class_Groups_Omonoid__mult: $i > $o ).
thf(tp_class_Groups_Oone,type,
class_Groups_Oone: $i > $o ).
thf(tp_class_Groups_Oordered__ab__group__add,type,
class_Groups_Oordered__ab__group__add: $i > $o ).
thf(tp_class_Groups_Oordered__ab__group__add__abs,type,
class_Groups_Oordered__ab__group__add__abs: $i > $o ).
thf(tp_class_Groups_Oordered__ab__semigroup__add,type,
class_Groups_Oordered__ab__semigroup__add: $i > $o ).
thf(tp_class_Groups_Oordered__ab__semigroup__add__imp__le,type,
class_Groups_Oordered__ab__semigroup__add__imp__le: $i > $o ).
thf(tp_class_Groups_Oordered__cancel__ab__semigroup__add,type,
class_Groups_Oordered__cancel__ab__semigroup__add: $i > $o ).
thf(tp_class_Groups_Oordered__comm__monoid__add,type,
class_Groups_Oordered__comm__monoid__add: $i > $o ).
thf(tp_class_Groups_Osemigroup__add,type,
class_Groups_Osemigroup__add: $i > $o ).
thf(tp_class_Groups_Osgn__if,type,
class_Groups_Osgn__if: $i > $o ).
thf(tp_class_Groups_Ouminus,type,
class_Groups_Ouminus: $i > $o ).
thf(tp_class_Groups_Ozero,type,
class_Groups_Ozero: $i > $o ).
thf(tp_class_Int_Onumber,type,
class_Int_Onumber: $i > $o ).
thf(tp_class_Int_Onumber__ring,type,
class_Int_Onumber__ring: $i > $o ).
thf(tp_class_Int_Oring__char__0,type,
class_Int_Oring__char__0: $i > $o ).
thf(tp_class_Lattices_Oab__semigroup__idem__mult,type,
class_Lattices_Oab__semigroup__idem__mult: $i > $o ).
thf(tp_class_Lattices_Oboolean__algebra,type,
class_Lattices_Oboolean__algebra: $i > $o ).
thf(tp_class_Lattices_Obounded__lattice,type,
class_Lattices_Obounded__lattice: $i > $o ).
thf(tp_class_Lattices_Obounded__lattice__bot,type,
class_Lattices_Obounded__lattice__bot: $i > $o ).
thf(tp_class_Lattices_Obounded__lattice__top,type,
class_Lattices_Obounded__lattice__top: $i > $o ).
thf(tp_class_Lattices_Odistrib__lattice,type,
class_Lattices_Odistrib__lattice: $i > $o ).
thf(tp_class_Lattices_Olattice,type,
class_Lattices_Olattice: $i > $o ).
thf(tp_class_Lattices_Osemilattice__inf,type,
class_Lattices_Osemilattice__inf: $i > $o ).
thf(tp_class_Lattices_Osemilattice__sup,type,
class_Lattices_Osemilattice__sup: $i > $o ).
thf(tp_class_Nat_Osemiring__char__0,type,
class_Nat_Osemiring__char__0: $i > $o ).
thf(tp_class_Orderings_Obot,type,
class_Orderings_Obot: $i > $o ).
thf(tp_class_Orderings_Olinorder,type,
class_Orderings_Olinorder: $i > $o ).
thf(tp_class_Orderings_Oord,type,
class_Orderings_Oord: $i > $o ).
thf(tp_class_Orderings_Oorder,type,
class_Orderings_Oorder: $i > $o ).
thf(tp_class_Orderings_Opreorder,type,
class_Orderings_Opreorder: $i > $o ).
thf(tp_class_Orderings_Otop,type,
class_Orderings_Otop: $i > $o ).
thf(tp_class_Orderings_Owellorder,type,
class_Orderings_Owellorder: $i > $o ).
thf(tp_class_Power_Opower,type,
class_Power_Opower: $i > $o ).
thf(tp_class_Rings_Ocomm__ring,type,
class_Rings_Ocomm__ring: $i > $o ).
thf(tp_class_Rings_Ocomm__ring__1,type,
class_Rings_Ocomm__ring__1: $i > $o ).
thf(tp_class_Rings_Ocomm__semiring,type,
class_Rings_Ocomm__semiring: $i > $o ).
thf(tp_class_Rings_Ocomm__semiring__1,type,
class_Rings_Ocomm__semiring__1: $i > $o ).
thf(tp_class_Rings_Odivision__ring,type,
class_Rings_Odivision__ring: $i > $o ).
thf(tp_class_Rings_Odivision__ring__inverse__zero,type,
class_Rings_Odivision__ring__inverse__zero: $i > $o ).
thf(tp_class_Rings_Odvd,type,
class_Rings_Odvd: $i > $o ).
thf(tp_class_Rings_Oidom,type,
class_Rings_Oidom: $i > $o ).
thf(tp_class_Rings_Oinverse,type,
class_Rings_Oinverse: $i > $o ).
thf(tp_class_Rings_Olinordered__comm__semiring__strict,type,
class_Rings_Olinordered__comm__semiring__strict: $i > $o ).
thf(tp_class_Rings_Olinordered__idom,type,
class_Rings_Olinordered__idom: $i > $o ).
thf(tp_class_Rings_Olinordered__ring,type,
class_Rings_Olinordered__ring: $i > $o ).
thf(tp_class_Rings_Olinordered__ring__strict,type,
class_Rings_Olinordered__ring__strict: $i > $o ).
thf(tp_class_Rings_Olinordered__semidom,type,
class_Rings_Olinordered__semidom: $i > $o ).
thf(tp_class_Rings_Olinordered__semiring,type,
class_Rings_Olinordered__semiring: $i > $o ).
thf(tp_class_Rings_Olinordered__semiring__1,type,
class_Rings_Olinordered__semiring__1: $i > $o ).
thf(tp_class_Rings_Olinordered__semiring__1__strict,type,
class_Rings_Olinordered__semiring__1__strict: $i > $o ).
thf(tp_class_Rings_Olinordered__semiring__strict,type,
class_Rings_Olinordered__semiring__strict: $i > $o ).
thf(tp_class_Rings_Omult__zero,type,
class_Rings_Omult__zero: $i > $o ).
thf(tp_class_Rings_Ono__zero__divisors,type,
class_Rings_Ono__zero__divisors: $i > $o ).
thf(tp_class_Rings_Oordered__cancel__semiring,type,
class_Rings_Oordered__cancel__semiring: $i > $o ).
thf(tp_class_Rings_Oordered__comm__semiring,type,
class_Rings_Oordered__comm__semiring: $i > $o ).
thf(tp_class_Rings_Oordered__ring,type,
class_Rings_Oordered__ring: $i > $o ).
thf(tp_class_Rings_Oordered__ring__abs,type,
class_Rings_Oordered__ring__abs: $i > $o ).
thf(tp_class_Rings_Oordered__semiring,type,
class_Rings_Oordered__semiring: $i > $o ).
thf(tp_class_Rings_Oring,type,
class_Rings_Oring: $i > $o ).
thf(tp_class_Rings_Oring__1,type,
class_Rings_Oring__1: $i > $o ).
thf(tp_class_Rings_Oring__1__no__zero__divisors,type,
class_Rings_Oring__1__no__zero__divisors: $i > $o ).
thf(tp_class_Rings_Oring__no__zero__divisors,type,
class_Rings_Oring__no__zero__divisors: $i > $o ).
thf(tp_class_Rings_Osemiring,type,
class_Rings_Osemiring: $i > $o ).
thf(tp_class_Rings_Osemiring__0,type,
class_Rings_Osemiring__0: $i > $o ).
thf(tp_class_Rings_Osemiring__1,type,
class_Rings_Osemiring__1: $i > $o ).
thf(tp_class_Rings_Ozero__neq__one,type,
class_Rings_Ozero__neq__one: $i > $o ).
thf(tp_class_Semiring__Normalization_Ocomm__semiring__1__cancel__crossproduct,type,
class_Semiring__Normalization_Ocomm__semiring__1__cancel__crossproduct: $i > $o ).
thf(tp_class_Smallcheck_Osmall,type,
class_Smallcheck_Osmall: $i > $o ).
thf(tp_hAPP,type,
hAPP: $i > $i > $i ).
thf(tp_hBOOL,type,
hBOOL: $i > $o ).
thf(tp_sK1_B_Z,type,
sK1_B_Z: $i ).
thf(tp_sK2_SY76,type,
sK2_SY76: $i ).
thf(tp_sK3_SX0,type,
sK3_SX0: $i ).
thf(tp_sK4_SY215,type,
sK4_SY215: $i > $i > $i > $i > $i > $i ).
thf(tp_sK5_SY216,type,
sK5_SY216: $i > $i > $i > $i > $i > $i ).
thf(tp_t_a,type,
t_a: $i ).
thf(tp_tc_Code__Evaluation_Oterm,type,
tc_Code__Evaluation_Oterm: $i ).
thf(tp_tc_Code__Numeral_Ocode__numeral,type,
tc_Code__Numeral_Ocode__numeral: $i ).
thf(tp_tc_Com_Ocom,type,
tc_Com_Ocom: $i ).
thf(tp_tc_Com_Oloc,type,
tc_Com_Oloc: $i ).
thf(tp_tc_Com_Opname,type,
tc_Com_Opname: $i ).
thf(tp_tc_Com_Ostate,type,
tc_Com_Ostate: $i ).
thf(tp_tc_Com_Ovname,type,
tc_Com_Ovname: $i ).
thf(tp_tc_HOL_Obool,type,
tc_HOL_Obool: $i ).
thf(tp_tc_Hoare__Mirabelle_Otriple,type,
tc_Hoare__Mirabelle_Otriple: $i > $i ).
thf(tp_tc_Int_Oint,type,
tc_Int_Oint: $i ).
thf(tp_tc_Lazy__Sequence_Olazy__sequence,type,
tc_Lazy__Sequence_Olazy__sequence: $i > $i ).
thf(tp_tc_List_Olist,type,
tc_List_Olist: $i > $i ).
thf(tp_tc_Nat_Onat,type,
tc_Nat_Onat: $i ).
thf(tp_tc_Nitpick_Opair__box,type,
tc_Nitpick_Opair__box: $i > $i > $i ).
thf(tp_tc_Option_Ooption,type,
tc_Option_Ooption: $i > $i ).
thf(tp_tc_Product__Type_Ounit,type,
tc_Product__Type_Ounit: $i ).
thf(tp_tc_fun,type,
tc_fun: $i > $i > $i ).
thf(tp_tc_prod,type,
tc_prod: $i > $i > $i ).
thf(tp_tc_sum,type,
tc_sum: $i > $i > $i ).
thf(tp_v_G,type,
v_G: $i ).
thf(tp_v_P,type,
v_P: $i > $i > $o ).
thf(tp_v_n,type,
v_n: $i ).
thf(5076,axiom,
! [V_com_H_2: $i,V_fun_H_2: $i] :
( c_Com_Ocom_OSKIP
!= ( c_Com_Ocom_OWhile @ V_fun_H_2 @ V_com_H_2 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_com_Osimps_I16_J) ).
thf(5077,axiom,
! [V_com_H_2: $i,V_fun_H_2: $i] :
( ( c_Com_Ocom_OWhile @ V_fun_H_2 @ V_com_H_2 )
!= c_Com_Ocom_OSKIP ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_com_Osimps_I17_J) ).
thf(5125,axiom,
! [V_com_H_2: $i,V_fun_H_2: $i,V_loc_H_2: $i] :
( ( c_Com_Ocom_OLocal @ V_loc_H_2 @ V_fun_H_2 @ V_com_H_2 )
!= c_Com_Ocom_OSKIP ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_com_Osimps_I11_J) ).
thf(5126,axiom,
! [V_fun_H_2: $i,V_pname_H_2: $i,V_vname_H_2: $i] :
( ( c_Com_Ocom_OCall @ V_vname_H_2 @ V_pname_H_2 @ V_fun_H_2 )
!= c_Com_Ocom_OSKIP ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_com_Osimps_I21_J) ).
thf(5127,axiom,
! [V_com_H_2: $i,V_fun_H_2: $i,V_loc_H_2: $i] :
( c_Com_Ocom_OSKIP
!= ( c_Com_Ocom_OLocal @ V_loc_H_2 @ V_fun_H_2 @ V_com_H_2 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_com_Osimps_I10_J) ).
thf(5128,axiom,
! [V_fun_H_2: $i,V_pname_H_2: $i,V_vname_H_2: $i] :
( c_Com_Ocom_OSKIP
!= ( c_Com_Ocom_OCall @ V_vname_H_2 @ V_pname_H_2 @ V_fun_H_2 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_com_Osimps_I20_J) ).
thf(5133,axiom,
! [V_fun_H_2: $i,V_vname_H_2: $i] :
( ( c_Com_Ocom_OAss @ V_vname_H_2 @ V_fun_H_2 )
!= c_Com_Ocom_OSKIP ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_com_Osimps_I9_J) ).
thf(5134,axiom,
! [V_fun_H_2: $i,V_vname_H_2: $i] :
( c_Com_Ocom_OSKIP
!= ( c_Com_Ocom_OAss @ V_vname_H_2 @ V_fun_H_2 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_com_Osimps_I8_J) ).
thf(5163,axiom,
! [V_t: $i,V_n: $i,V_s: $i,V_c2: $i,V_c1: $i] :
( ( c_Natural_Oevaln @ ( c_Com_Ocom_OSemi @ V_c1 @ V_c2 ) @ V_s @ V_n @ V_t )
=> ~ ! [B_s1: $i] :
( ( c_Natural_Oevaln @ V_c1 @ V_s @ V_n @ B_s1 )
=> ~ ( c_Natural_Oevaln @ V_c2 @ B_s1 @ V_n @ V_t ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_evaln__elim__cases_I4_J) ).
thf(5166,axiom,
! [V_com2_H: $i,V_com1_H: $i] :
( c_Com_Ocom_OSKIP
!= ( c_Com_Ocom_OSemi @ V_com1_H @ V_com2_H ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_com_Osimps_I12_J) ).
thf(5167,axiom,
! [V_com2_H: $i,V_com1_H: $i] :
( ( c_Com_Ocom_OSemi @ V_com1_H @ V_com2_H )
!= c_Com_Ocom_OSKIP ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_com_Osimps_I13_J) ).
thf(5168,axiom,
! [V_com2_H_2: $i,V_com1_H_2: $i,V_fun_H_2: $i] :
( c_Com_Ocom_OSKIP
!= ( c_Com_Ocom_OCond @ V_fun_H_2 @ V_com1_H_2 @ V_com2_H_2 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_com_Osimps_I14_J) ).
thf(5169,axiom,
! [V_com2_H_2: $i,V_com1_H_2: $i,V_fun_H_2: $i] :
( ( c_Com_Ocom_OCond @ V_fun_H_2 @ V_com1_H_2 @ V_com2_H_2 )
!= c_Com_Ocom_OSKIP ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_com_Osimps_I15_J) ).
thf(5172,axiom,
! [V_a6_2: $i,V_a3_2: $i,V_a2_2: $i,V_a5_2: $i,V_a1_2: $i] :
( ( c_Natural_Oevaln @ ( c_Com_Ocom_OSemi @ V_a1_2 @ V_a5_2 ) @ V_a2_2 @ V_a3_2 @ V_a6_2 )
<=> ? [B_s1: $i] :
( ( c_Natural_Oevaln @ V_a1_2 @ V_a2_2 @ V_a3_2 @ B_s1 )
& ( c_Natural_Oevaln @ V_a5_2 @ B_s1 @ V_a3_2 @ V_a6_2 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_evaln_Oequations_I4_J) ).
thf(5195,axiom,
! [V_s2: $i,V_c1: $i,V_s1: $i,V_n: $i,V_s0: $i,V_c0: $i] :
( ( c_Natural_Oevaln @ V_c0 @ V_s0 @ V_n @ V_s1 )
=> ( ( c_Natural_Oevaln @ V_c1 @ V_s1 @ V_n @ V_s2 )
=> ( c_Natural_Oevaln @ ( c_Com_Ocom_OSemi @ V_c0 @ V_c1 ) @ V_s0 @ V_n @ V_s2 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_evaln_OSemi) ).
thf(5197,axiom,
! [V_f8_2: $i,V_f7_2: $i,V_f6_2: $i,V_f5_2: $i,V_f4_2: $i,V_f3_2: $i,V_f2_2: $i,V_f1_2: $i,T_b: $i] :
( ( c_Com_Ocom_Ocom__rec @ T_b @ V_f1_2 @ V_f2_2 @ V_f3_2 @ V_f4_2 @ V_f5_2 @ V_f6_2 @ V_f7_2 @ V_f8_2 @ c_Com_Ocom_OSKIP )
= V_f1_2 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_com_Orecs_I1_J) ).
thf(5198,axiom,
! [V_f8_2: $i,V_f7_2: $i,V_f6_2: $i,V_f5_2: $i,V_f4_2: $i,V_f3_2: $i,V_f2_2: $i,V_f1_2: $i,T_b: $i] :
( ( c_Com_Ocom_Ocom__case @ T_b @ V_f1_2 @ V_f2_2 @ V_f3_2 @ V_f4_2 @ V_f5_2 @ V_f6_2 @ V_f7_2 @ V_f8_2 @ c_Com_Ocom_OSKIP )
= V_f1_2 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_com_Osimps_I64_J) ).
thf(5201,axiom,
! [V_a2: $i,V_a1: $i] : ( c_Natural_Oevaln @ c_Com_Ocom_OSKIP @ V_a1 @ V_a2 @ V_a1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_evaln_Oequations_I1_J) ).
thf(5202,axiom,
! [V_t: $i,V_n: $i,V_s: $i] :
( ( c_Natural_Oevaln @ c_Com_Ocom_OSKIP @ V_s @ V_n @ V_t )
=> ( V_t = V_s ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_evaln__elim__cases_I1_J) ).
thf(5203,axiom,
! [V_n: $i,V_s: $i] : ( c_Natural_Oevaln @ c_Com_Ocom_OSKIP @ V_s @ V_n @ V_s ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_evaln_OSkip) ).
thf(5206,conjecture,
! [B_Z: $i,B_s: $i] :
( ( v_P @ B_Z @ B_s )
=> ! [B_s_H: $i] :
( ( c_Natural_Oevaln @ c_Com_Ocom_OSKIP @ B_s @ v_n @ B_s_H )
=> ( v_P @ B_Z @ B_s_H ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_1) ).
thf(5207,negated_conjecture,
( ( ! [B_Z: $i,B_s: $i] :
( ( v_P @ B_Z @ B_s )
=> ! [B_s_H: $i] :
( ( c_Natural_Oevaln @ c_Com_Ocom_OSKIP @ B_s @ v_n @ B_s_H )
=> ( v_P @ B_Z @ B_s_H ) ) ) )
= $false ),
inference(negate_conjecture,[status(cth)],[5206]) ).
thf(5208,plain,
( ( ! [B_Z: $i,B_s: $i] :
( ( v_P @ B_Z @ B_s )
=> ! [B_s_H: $i] :
( ( c_Natural_Oevaln @ c_Com_Ocom_OSKIP @ B_s @ v_n @ B_s_H )
=> ( v_P @ B_Z @ B_s_H ) ) ) )
= $false ),
inference(unfold_def,[status(thm)],[5207]) ).
thf(5209,plain,
( ( ! [V_com_H_2: $i,V_fun_H_2: $i] :
( c_Com_Ocom_OSKIP
!= ( c_Com_Ocom_OWhile @ V_fun_H_2 @ V_com_H_2 ) ) )
= $true ),
inference(unfold_def,[status(thm)],[5076]) ).
thf(5210,plain,
( ( ! [V_com_H_2: $i,V_fun_H_2: $i] :
( ( c_Com_Ocom_OWhile @ V_fun_H_2 @ V_com_H_2 )
!= c_Com_Ocom_OSKIP ) )
= $true ),
inference(unfold_def,[status(thm)],[5077]) ).
thf(5211,plain,
( ( ! [V_com_H_2: $i,V_fun_H_2: $i,V_loc_H_2: $i] :
( ( c_Com_Ocom_OLocal @ V_loc_H_2 @ V_fun_H_2 @ V_com_H_2 )
!= c_Com_Ocom_OSKIP ) )
= $true ),
inference(unfold_def,[status(thm)],[5125]) ).
thf(5212,plain,
( ( ! [V_fun_H_2: $i,V_pname_H_2: $i,V_vname_H_2: $i] :
( ( c_Com_Ocom_OCall @ V_vname_H_2 @ V_pname_H_2 @ V_fun_H_2 )
!= c_Com_Ocom_OSKIP ) )
= $true ),
inference(unfold_def,[status(thm)],[5126]) ).
thf(5213,plain,
( ( ! [V_com_H_2: $i,V_fun_H_2: $i,V_loc_H_2: $i] :
( c_Com_Ocom_OSKIP
!= ( c_Com_Ocom_OLocal @ V_loc_H_2 @ V_fun_H_2 @ V_com_H_2 ) ) )
= $true ),
inference(unfold_def,[status(thm)],[5127]) ).
thf(5214,plain,
( ( ! [V_fun_H_2: $i,V_pname_H_2: $i,V_vname_H_2: $i] :
( c_Com_Ocom_OSKIP
!= ( c_Com_Ocom_OCall @ V_vname_H_2 @ V_pname_H_2 @ V_fun_H_2 ) ) )
= $true ),
inference(unfold_def,[status(thm)],[5128]) ).
thf(5215,plain,
( ( ! [V_fun_H_2: $i,V_vname_H_2: $i] :
( ( c_Com_Ocom_OAss @ V_vname_H_2 @ V_fun_H_2 )
!= c_Com_Ocom_OSKIP ) )
= $true ),
inference(unfold_def,[status(thm)],[5133]) ).
thf(5216,plain,
( ( ! [V_fun_H_2: $i,V_vname_H_2: $i] :
( c_Com_Ocom_OSKIP
!= ( c_Com_Ocom_OAss @ V_vname_H_2 @ V_fun_H_2 ) ) )
= $true ),
inference(unfold_def,[status(thm)],[5134]) ).
thf(5217,plain,
( ( ! [V_t: $i,V_n: $i,V_s: $i,V_c2: $i,V_c1: $i] :
( ( c_Natural_Oevaln @ ( c_Com_Ocom_OSemi @ V_c1 @ V_c2 ) @ V_s @ V_n @ V_t )
=> ~ ! [B_s1: $i] :
( ( c_Natural_Oevaln @ V_c1 @ V_s @ V_n @ B_s1 )
=> ~ ( c_Natural_Oevaln @ V_c2 @ B_s1 @ V_n @ V_t ) ) ) )
= $true ),
inference(unfold_def,[status(thm)],[5163]) ).
thf(5218,plain,
( ( ! [V_com2_H: $i,V_com1_H: $i] :
( c_Com_Ocom_OSKIP
!= ( c_Com_Ocom_OSemi @ V_com1_H @ V_com2_H ) ) )
= $true ),
inference(unfold_def,[status(thm)],[5166]) ).
thf(5219,plain,
( ( ! [V_com2_H: $i,V_com1_H: $i] :
( ( c_Com_Ocom_OSemi @ V_com1_H @ V_com2_H )
!= c_Com_Ocom_OSKIP ) )
= $true ),
inference(unfold_def,[status(thm)],[5167]) ).
thf(5220,plain,
( ( ! [V_com2_H_2: $i,V_com1_H_2: $i,V_fun_H_2: $i] :
( c_Com_Ocom_OSKIP
!= ( c_Com_Ocom_OCond @ V_fun_H_2 @ V_com1_H_2 @ V_com2_H_2 ) ) )
= $true ),
inference(unfold_def,[status(thm)],[5168]) ).
thf(5221,plain,
( ( ! [V_com2_H_2: $i,V_com1_H_2: $i,V_fun_H_2: $i] :
( ( c_Com_Ocom_OCond @ V_fun_H_2 @ V_com1_H_2 @ V_com2_H_2 )
!= c_Com_Ocom_OSKIP ) )
= $true ),
inference(unfold_def,[status(thm)],[5169]) ).
thf(5222,plain,
( ( ! [V_a6_2: $i,V_a3_2: $i,V_a2_2: $i,V_a5_2: $i,V_a1_2: $i] :
( ( c_Natural_Oevaln @ ( c_Com_Ocom_OSemi @ V_a1_2 @ V_a5_2 ) @ V_a2_2 @ V_a3_2 @ V_a6_2 )
<=> ? [B_s1: $i] :
( ( c_Natural_Oevaln @ V_a1_2 @ V_a2_2 @ V_a3_2 @ B_s1 )
& ( c_Natural_Oevaln @ V_a5_2 @ B_s1 @ V_a3_2 @ V_a6_2 ) ) ) )
= $true ),
inference(unfold_def,[status(thm)],[5172]) ).
thf(5223,plain,
( ( ! [V_s2: $i,V_c1: $i,V_s1: $i,V_n: $i,V_s0: $i,V_c0: $i] :
( ( c_Natural_Oevaln @ V_c0 @ V_s0 @ V_n @ V_s1 )
=> ( ( c_Natural_Oevaln @ V_c1 @ V_s1 @ V_n @ V_s2 )
=> ( c_Natural_Oevaln @ ( c_Com_Ocom_OSemi @ V_c0 @ V_c1 ) @ V_s0 @ V_n @ V_s2 ) ) ) )
= $true ),
inference(unfold_def,[status(thm)],[5195]) ).
thf(5224,plain,
( ( ! [V_f8_2: $i,V_f7_2: $i,V_f6_2: $i,V_f5_2: $i,V_f4_2: $i,V_f3_2: $i,V_f2_2: $i,V_f1_2: $i,T_b: $i] :
( ( c_Com_Ocom_Ocom__rec @ T_b @ V_f1_2 @ V_f2_2 @ V_f3_2 @ V_f4_2 @ V_f5_2 @ V_f6_2 @ V_f7_2 @ V_f8_2 @ c_Com_Ocom_OSKIP )
= V_f1_2 ) )
= $true ),
inference(unfold_def,[status(thm)],[5197]) ).
thf(5225,plain,
( ( ! [V_f8_2: $i,V_f7_2: $i,V_f6_2: $i,V_f5_2: $i,V_f4_2: $i,V_f3_2: $i,V_f2_2: $i,V_f1_2: $i,T_b: $i] :
( ( c_Com_Ocom_Ocom__case @ T_b @ V_f1_2 @ V_f2_2 @ V_f3_2 @ V_f4_2 @ V_f5_2 @ V_f6_2 @ V_f7_2 @ V_f8_2 @ c_Com_Ocom_OSKIP )
= V_f1_2 ) )
= $true ),
inference(unfold_def,[status(thm)],[5198]) ).
thf(5226,plain,
( ( ! [V_a2: $i,V_a1: $i] : ( c_Natural_Oevaln @ c_Com_Ocom_OSKIP @ V_a1 @ V_a2 @ V_a1 ) )
= $true ),
inference(unfold_def,[status(thm)],[5201]) ).
thf(5227,plain,
( ( ! [V_t: $i,V_n: $i,V_s: $i] :
( ( c_Natural_Oevaln @ c_Com_Ocom_OSKIP @ V_s @ V_n @ V_t )
=> ( V_t = V_s ) ) )
= $true ),
inference(unfold_def,[status(thm)],[5202]) ).
thf(5228,plain,
( ( ! [V_n: $i,V_s: $i] : ( c_Natural_Oevaln @ c_Com_Ocom_OSKIP @ V_s @ V_n @ V_s ) )
= $true ),
inference(unfold_def,[status(thm)],[5203]) ).
thf(5229,plain,
( ( ! [SY76: $i] :
( ( v_P @ sK1_B_Z @ SY76 )
=> ! [SY77: $i] :
( ( c_Natural_Oevaln @ c_Com_Ocom_OSKIP @ SY76 @ v_n @ SY77 )
=> ( v_P @ sK1_B_Z @ SY77 ) ) ) )
= $false ),
inference(extcnf_forall_neg,[status(esa)],[5208]) ).
thf(5230,plain,
( ( ( v_P @ sK1_B_Z @ sK2_SY76 )
=> ! [SY78: $i] :
( ( c_Natural_Oevaln @ c_Com_Ocom_OSKIP @ sK2_SY76 @ v_n @ SY78 )
=> ( v_P @ sK1_B_Z @ SY78 ) ) )
= $false ),
inference(extcnf_forall_neg,[status(esa)],[5229]) ).
thf(5231,plain,
( ( v_P @ sK1_B_Z @ sK2_SY76 )
= $true ),
inference(standard_cnf,[status(thm)],[5230]) ).
thf(5232,plain,
( ( ! [SY78: $i] :
( ( c_Natural_Oevaln @ c_Com_Ocom_OSKIP @ sK2_SY76 @ v_n @ SY78 )
=> ( v_P @ sK1_B_Z @ SY78 ) ) )
= $false ),
inference(standard_cnf,[status(thm)],[5230]) ).
thf(5233,plain,
( ( ~ ! [SY78: $i] :
( ( c_Natural_Oevaln @ c_Com_Ocom_OSKIP @ sK2_SY76 @ v_n @ SY78 )
=> ( v_P @ sK1_B_Z @ SY78 ) ) )
= $true ),
inference(polarity_switch,[status(thm)],[5232]) ).
thf(5234,plain,
( ( ! [V_n: $i,V_s: $i] : ( c_Natural_Oevaln @ c_Com_Ocom_OSKIP @ V_s @ V_n @ V_s ) )
= $true ),
inference(copy,[status(thm)],[5228]) ).
thf(5235,plain,
( ( ! [V_t: $i,V_n: $i,V_s: $i] :
( ( c_Natural_Oevaln @ c_Com_Ocom_OSKIP @ V_s @ V_n @ V_t )
=> ( V_t = V_s ) ) )
= $true ),
inference(copy,[status(thm)],[5227]) ).
thf(5236,plain,
( ( ! [V_a2: $i,V_a1: $i] : ( c_Natural_Oevaln @ c_Com_Ocom_OSKIP @ V_a1 @ V_a2 @ V_a1 ) )
= $true ),
inference(copy,[status(thm)],[5226]) ).
thf(5237,plain,
( ( ! [V_f8_2: $i,V_f7_2: $i,V_f6_2: $i,V_f5_2: $i,V_f4_2: $i,V_f3_2: $i,V_f2_2: $i,V_f1_2: $i,T_b: $i] :
( ( c_Com_Ocom_Ocom__case @ T_b @ V_f1_2 @ V_f2_2 @ V_f3_2 @ V_f4_2 @ V_f5_2 @ V_f6_2 @ V_f7_2 @ V_f8_2 @ c_Com_Ocom_OSKIP )
= V_f1_2 ) )
= $true ),
inference(copy,[status(thm)],[5225]) ).
thf(5238,plain,
( ( ! [V_f8_2: $i,V_f7_2: $i,V_f6_2: $i,V_f5_2: $i,V_f4_2: $i,V_f3_2: $i,V_f2_2: $i,V_f1_2: $i,T_b: $i] :
( ( c_Com_Ocom_Ocom__rec @ T_b @ V_f1_2 @ V_f2_2 @ V_f3_2 @ V_f4_2 @ V_f5_2 @ V_f6_2 @ V_f7_2 @ V_f8_2 @ c_Com_Ocom_OSKIP )
= V_f1_2 ) )
= $true ),
inference(copy,[status(thm)],[5224]) ).
thf(5239,plain,
( ( ! [V_s2: $i,V_c1: $i,V_s1: $i,V_n: $i,V_s0: $i,V_c0: $i] :
( ( c_Natural_Oevaln @ V_c0 @ V_s0 @ V_n @ V_s1 )
=> ( ( c_Natural_Oevaln @ V_c1 @ V_s1 @ V_n @ V_s2 )
=> ( c_Natural_Oevaln @ ( c_Com_Ocom_OSemi @ V_c0 @ V_c1 ) @ V_s0 @ V_n @ V_s2 ) ) ) )
= $true ),
inference(copy,[status(thm)],[5223]) ).
thf(5240,plain,
( ( ! [V_a6_2: $i,V_a3_2: $i,V_a2_2: $i,V_a5_2: $i,V_a1_2: $i] :
( ( c_Natural_Oevaln @ ( c_Com_Ocom_OSemi @ V_a1_2 @ V_a5_2 ) @ V_a2_2 @ V_a3_2 @ V_a6_2 )
<=> ? [B_s1: $i] :
( ( c_Natural_Oevaln @ V_a1_2 @ V_a2_2 @ V_a3_2 @ B_s1 )
& ( c_Natural_Oevaln @ V_a5_2 @ B_s1 @ V_a3_2 @ V_a6_2 ) ) ) )
= $true ),
inference(copy,[status(thm)],[5222]) ).
thf(5241,plain,
( ( ! [V_com2_H_2: $i,V_com1_H_2: $i,V_fun_H_2: $i] :
( ( c_Com_Ocom_OCond @ V_fun_H_2 @ V_com1_H_2 @ V_com2_H_2 )
!= c_Com_Ocom_OSKIP ) )
= $true ),
inference(copy,[status(thm)],[5221]) ).
thf(5242,plain,
( ( ! [V_com2_H_2: $i,V_com1_H_2: $i,V_fun_H_2: $i] :
( c_Com_Ocom_OSKIP
!= ( c_Com_Ocom_OCond @ V_fun_H_2 @ V_com1_H_2 @ V_com2_H_2 ) ) )
= $true ),
inference(copy,[status(thm)],[5220]) ).
thf(5243,plain,
( ( ! [V_com2_H: $i,V_com1_H: $i] :
( ( c_Com_Ocom_OSemi @ V_com1_H @ V_com2_H )
!= c_Com_Ocom_OSKIP ) )
= $true ),
inference(copy,[status(thm)],[5219]) ).
thf(5244,plain,
( ( ! [V_com2_H: $i,V_com1_H: $i] :
( c_Com_Ocom_OSKIP
!= ( c_Com_Ocom_OSemi @ V_com1_H @ V_com2_H ) ) )
= $true ),
inference(copy,[status(thm)],[5218]) ).
thf(5245,plain,
( ( ! [V_t: $i,V_n: $i,V_s: $i,V_c2: $i,V_c1: $i] :
( ( c_Natural_Oevaln @ ( c_Com_Ocom_OSemi @ V_c1 @ V_c2 ) @ V_s @ V_n @ V_t )
=> ~ ! [B_s1: $i] :
( ( c_Natural_Oevaln @ V_c1 @ V_s @ V_n @ B_s1 )
=> ~ ( c_Natural_Oevaln @ V_c2 @ B_s1 @ V_n @ V_t ) ) ) )
= $true ),
inference(copy,[status(thm)],[5217]) ).
thf(5246,plain,
( ( ! [V_fun_H_2: $i,V_vname_H_2: $i] :
( c_Com_Ocom_OSKIP
!= ( c_Com_Ocom_OAss @ V_vname_H_2 @ V_fun_H_2 ) ) )
= $true ),
inference(copy,[status(thm)],[5216]) ).
thf(5247,plain,
( ( ! [V_fun_H_2: $i,V_vname_H_2: $i] :
( ( c_Com_Ocom_OAss @ V_vname_H_2 @ V_fun_H_2 )
!= c_Com_Ocom_OSKIP ) )
= $true ),
inference(copy,[status(thm)],[5215]) ).
thf(5248,plain,
( ( ! [V_fun_H_2: $i,V_pname_H_2: $i,V_vname_H_2: $i] :
( c_Com_Ocom_OSKIP
!= ( c_Com_Ocom_OCall @ V_vname_H_2 @ V_pname_H_2 @ V_fun_H_2 ) ) )
= $true ),
inference(copy,[status(thm)],[5214]) ).
thf(5249,plain,
( ( ! [V_com_H_2: $i,V_fun_H_2: $i,V_loc_H_2: $i] :
( c_Com_Ocom_OSKIP
!= ( c_Com_Ocom_OLocal @ V_loc_H_2 @ V_fun_H_2 @ V_com_H_2 ) ) )
= $true ),
inference(copy,[status(thm)],[5213]) ).
thf(5250,plain,
( ( ! [V_fun_H_2: $i,V_pname_H_2: $i,V_vname_H_2: $i] :
( ( c_Com_Ocom_OCall @ V_vname_H_2 @ V_pname_H_2 @ V_fun_H_2 )
!= c_Com_Ocom_OSKIP ) )
= $true ),
inference(copy,[status(thm)],[5212]) ).
thf(5251,plain,
( ( ! [V_com_H_2: $i,V_fun_H_2: $i,V_loc_H_2: $i] :
( ( c_Com_Ocom_OLocal @ V_loc_H_2 @ V_fun_H_2 @ V_com_H_2 )
!= c_Com_Ocom_OSKIP ) )
= $true ),
inference(copy,[status(thm)],[5211]) ).
thf(5252,plain,
( ( ! [V_com_H_2: $i,V_fun_H_2: $i] :
( ( c_Com_Ocom_OWhile @ V_fun_H_2 @ V_com_H_2 )
!= c_Com_Ocom_OSKIP ) )
= $true ),
inference(copy,[status(thm)],[5210]) ).
thf(5253,plain,
( ( ! [V_com_H_2: $i,V_fun_H_2: $i] :
( c_Com_Ocom_OSKIP
!= ( c_Com_Ocom_OWhile @ V_fun_H_2 @ V_com_H_2 ) ) )
= $true ),
inference(copy,[status(thm)],[5209]) ).
thf(5254,plain,
( ( v_P @ sK1_B_Z @ sK2_SY76 )
= $true ),
inference(copy,[status(thm)],[5231]) ).
thf(5255,plain,
( ( ~ ! [SY78: $i] :
( ( c_Natural_Oevaln @ c_Com_Ocom_OSKIP @ sK2_SY76 @ v_n @ SY78 )
=> ( v_P @ sK1_B_Z @ SY78 ) ) )
= $true ),
inference(copy,[status(thm)],[5233]) ).
thf(5256,plain,
( ( ! [SX0: $i,SX1: $i,SX2: $i] :
( ( c_Com_Ocom_OCond @ SX2 @ SX1 @ SX0 )
!= c_Com_Ocom_OSKIP ) )
= $true ),
inference(unfold_def,[status(thm)],[5241]) ).
thf(5257,plain,
( ( ! [SX0: $i,SX1: $i,SX2: $i,SX3: $i,SX4: $i,SX5: $i] :
( ~ ( c_Natural_Oevaln @ SX5 @ SX4 @ SX3 @ SX2 )
| ~ ( c_Natural_Oevaln @ SX1 @ SX2 @ SX3 @ SX0 )
| ( c_Natural_Oevaln @ ( c_Com_Ocom_OSemi @ SX5 @ SX1 ) @ SX4 @ SX3 @ SX0 ) ) )
= $true ),
inference(unfold_def,[status(thm)],[5239]) ).
thf(5258,plain,
( ( ! [SX0: $i,SX1: $i] :
( ( c_Com_Ocom_OAss @ SX1 @ SX0 )
!= c_Com_Ocom_OSKIP ) )
= $true ),
inference(unfold_def,[status(thm)],[5247]) ).
thf(5259,plain,
( ( ! [SX0: $i,SX1: $i] :
( ( c_Com_Ocom_OSemi @ SX1 @ SX0 )
!= c_Com_Ocom_OSKIP ) )
= $true ),
inference(unfold_def,[status(thm)],[5243]) ).
thf(5260,plain,
( ( ! [SX0: $i,SX1: $i] :
( c_Com_Ocom_OSKIP
!= ( c_Com_Ocom_OSemi @ SX1 @ SX0 ) ) )
= $true ),
inference(unfold_def,[status(thm)],[5244]) ).
thf(5261,plain,
( ( ! [SX0: $i,SX1: $i,SX2: $i] :
( c_Com_Ocom_OSKIP
!= ( c_Com_Ocom_OCond @ SX2 @ SX1 @ SX0 ) ) )
= $true ),
inference(unfold_def,[status(thm)],[5242]) ).
thf(5262,plain,
( ( ! [SX0: $i,SX1: $i,SX2: $i] :
( c_Com_Ocom_OSKIP
!= ( c_Com_Ocom_OLocal @ SX2 @ SX1 @ SX0 ) ) )
= $true ),
inference(unfold_def,[status(thm)],[5249]) ).
thf(5263,plain,
( ( ! [SX0: $i,SX1: $i,SX2: $i] :
( ~ ( c_Natural_Oevaln @ c_Com_Ocom_OSKIP @ SX2 @ SX1 @ SX0 )
| ( SX0 = SX2 ) ) )
= $true ),
inference(unfold_def,[status(thm)],[5235]) ).
thf(5264,plain,
( ( ! [SX0: $i,SX1: $i,SX2: $i,SX3: $i,SX4: $i] :
( ~ ( c_Natural_Oevaln @ ( c_Com_Ocom_OSemi @ SX4 @ SX3 ) @ SX2 @ SX1 @ SX0 )
| ~ ! [SX5: $i] :
( ~ ( c_Natural_Oevaln @ SX4 @ SX2 @ SX1 @ SX5 )
| ~ ( c_Natural_Oevaln @ SX3 @ SX5 @ SX1 @ SX0 ) ) ) )
= $true ),
inference(unfold_def,[status(thm)],[5245]) ).
thf(5265,plain,
( ( ! [SX0: $i,SX1: $i] :
( ( c_Com_Ocom_OWhile @ SX1 @ SX0 )
!= c_Com_Ocom_OSKIP ) )
= $true ),
inference(unfold_def,[status(thm)],[5252]) ).
thf(5266,plain,
( ( ! [SX0: $i,SX1: $i] :
( c_Com_Ocom_OSKIP
!= ( c_Com_Ocom_OWhile @ SX1 @ SX0 ) ) )
= $true ),
inference(unfold_def,[status(thm)],[5253]) ).
thf(5267,plain,
( ( ~ ! [SX0: $i] :
( ~ ( c_Natural_Oevaln @ c_Com_Ocom_OSKIP @ sK2_SY76 @ v_n @ SX0 )
| ( v_P @ sK1_B_Z @ SX0 ) ) )
= $true ),
inference(unfold_def,[status(thm)],[5255]) ).
thf(5268,plain,
( ( ! [SX0: $i,SX1: $i] :
( c_Com_Ocom_OSKIP
!= ( c_Com_Ocom_OAss @ SX1 @ SX0 ) ) )
= $true ),
inference(unfold_def,[status(thm)],[5246]) ).
thf(5269,plain,
( ( ! [SX0: $i,SX1: $i,SX2: $i] :
( ( c_Com_Ocom_OCall @ SX2 @ SX1 @ SX0 )
!= c_Com_Ocom_OSKIP ) )
= $true ),
inference(unfold_def,[status(thm)],[5250]) ).
thf(5270,plain,
( ( ! [SX0: $i,SX1: $i,SX2: $i] :
( c_Com_Ocom_OSKIP
!= ( c_Com_Ocom_OCall @ SX2 @ SX1 @ SX0 ) ) )
= $true ),
inference(unfold_def,[status(thm)],[5248]) ).
thf(5271,plain,
( ( ! [SX0: $i,SX1: $i,SX2: $i,SX3: $i,SX4: $i] :
~ ( ~ ( ~ ( c_Natural_Oevaln @ ( c_Com_Ocom_OSemi @ SX4 @ SX3 ) @ SX2 @ SX1 @ SX0 )
| ~ ! [SX5: $i] :
~ ~ ( ~ ( c_Natural_Oevaln @ SX4 @ SX2 @ SX1 @ SX5 )
| ~ ( c_Natural_Oevaln @ SX3 @ SX5 @ SX1 @ SX0 ) ) )
| ~ ( ~ ~ ! [SX5: $i] :
~ ~ ( ~ ( c_Natural_Oevaln @ SX4 @ SX2 @ SX1 @ SX5 )
| ~ ( c_Natural_Oevaln @ SX3 @ SX5 @ SX1 @ SX0 ) )
| ( c_Natural_Oevaln @ ( c_Com_Ocom_OSemi @ SX4 @ SX3 ) @ SX2 @ SX1 @ SX0 ) ) ) )
= $true ),
inference(unfold_def,[status(thm)],[5240]) ).
thf(5272,plain,
( ( ! [SX0: $i,SX1: $i,SX2: $i] :
( ( c_Com_Ocom_OLocal @ SX2 @ SX1 @ SX0 )
!= c_Com_Ocom_OSKIP ) )
= $true ),
inference(unfold_def,[status(thm)],[5251]) ).
thf(5273,plain,
! [SV1: $i] :
( ( ! [SY79: $i] : ( c_Natural_Oevaln @ c_Com_Ocom_OSKIP @ SY79 @ SV1 @ SY79 ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[5234]) ).
thf(5274,plain,
! [SV2: $i] :
( ( ! [SY80: $i] : ( c_Natural_Oevaln @ c_Com_Ocom_OSKIP @ SY80 @ SV2 @ SY80 ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[5236]) ).
thf(5275,plain,
! [SV3: $i] :
( ( ! [SY81: $i,SY82: $i,SY83: $i,SY84: $i,SY85: $i,SY86: $i,SY87: $i,SY88: $i] :
( ( c_Com_Ocom_Ocom__case @ SY88 @ SY87 @ SY86 @ SY85 @ SY84 @ SY83 @ SY82 @ SY81 @ SV3 @ c_Com_Ocom_OSKIP )
= SY87 ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[5237]) ).
thf(5276,plain,
! [SV4: $i] :
( ( ! [SY89: $i,SY90: $i,SY91: $i,SY92: $i,SY93: $i,SY94: $i,SY95: $i,SY96: $i] :
( ( c_Com_Ocom_Ocom__rec @ SY96 @ SY95 @ SY94 @ SY93 @ SY92 @ SY91 @ SY90 @ SY89 @ SV4 @ c_Com_Ocom_OSKIP )
= SY95 ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[5238]) ).
thf(5277,plain,
! [SV5: $i] :
( ( ! [SY97: $i,SY98: $i] :
( ( c_Com_Ocom_OCond @ SY98 @ SY97 @ SV5 )
!= c_Com_Ocom_OSKIP ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[5256]) ).
thf(5278,plain,
! [SV6: $i] :
( ( ! [SY99: $i,SY100: $i,SY101: $i,SY102: $i,SY103: $i] :
( ~ ( c_Natural_Oevaln @ SY103 @ SY102 @ SY101 @ SY100 )
| ~ ( c_Natural_Oevaln @ SY99 @ SY100 @ SY101 @ SV6 )
| ( c_Natural_Oevaln @ ( c_Com_Ocom_OSemi @ SY103 @ SY99 ) @ SY102 @ SY101 @ SV6 ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[5257]) ).
thf(5279,plain,
! [SV7: $i] :
( ( ! [SY104: $i] :
( ( c_Com_Ocom_OAss @ SY104 @ SV7 )
!= c_Com_Ocom_OSKIP ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[5258]) ).
thf(5280,plain,
! [SV8: $i] :
( ( ! [SY105: $i] :
( ( c_Com_Ocom_OSemi @ SY105 @ SV8 )
!= c_Com_Ocom_OSKIP ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[5259]) ).
thf(5281,plain,
! [SV9: $i] :
( ( ! [SY106: $i] :
( c_Com_Ocom_OSKIP
!= ( c_Com_Ocom_OSemi @ SY106 @ SV9 ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[5260]) ).
thf(5282,plain,
! [SV10: $i] :
( ( ! [SY107: $i,SY108: $i] :
( c_Com_Ocom_OSKIP
!= ( c_Com_Ocom_OCond @ SY108 @ SY107 @ SV10 ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[5261]) ).
thf(5283,plain,
! [SV11: $i] :
( ( ! [SY109: $i,SY110: $i] :
( c_Com_Ocom_OSKIP
!= ( c_Com_Ocom_OLocal @ SY110 @ SY109 @ SV11 ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[5262]) ).
thf(5284,plain,
! [SV12: $i] :
( ( ! [SY111: $i,SY112: $i] :
( ~ ( c_Natural_Oevaln @ c_Com_Ocom_OSKIP @ SY112 @ SY111 @ SV12 )
| ( SV12 = SY112 ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[5263]) ).
thf(5285,plain,
! [SV13: $i] :
( ( ! [SY113: $i,SY114: $i,SY115: $i,SY116: $i] :
( ~ ( c_Natural_Oevaln @ ( c_Com_Ocom_OSemi @ SY116 @ SY115 ) @ SY114 @ SY113 @ SV13 )
| ~ ! [SY117: $i] :
( ~ ( c_Natural_Oevaln @ SY116 @ SY114 @ SY113 @ SY117 )
| ~ ( c_Natural_Oevaln @ SY115 @ SY117 @ SY113 @ SV13 ) ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[5264]) ).
thf(5286,plain,
! [SV14: $i] :
( ( ! [SY118: $i] :
( ( c_Com_Ocom_OWhile @ SY118 @ SV14 )
!= c_Com_Ocom_OSKIP ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[5265]) ).
thf(5287,plain,
! [SV15: $i] :
( ( ! [SY119: $i] :
( c_Com_Ocom_OSKIP
!= ( c_Com_Ocom_OWhile @ SY119 @ SV15 ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[5266]) ).
thf(5288,plain,
( ( ! [SX0: $i] :
( ~ ( c_Natural_Oevaln @ c_Com_Ocom_OSKIP @ sK2_SY76 @ v_n @ SX0 )
| ( v_P @ sK1_B_Z @ SX0 ) ) )
= $false ),
inference(extcnf_not_pos,[status(thm)],[5267]) ).
thf(5289,plain,
! [SV16: $i] :
( ( ! [SY120: $i] :
( c_Com_Ocom_OSKIP
!= ( c_Com_Ocom_OAss @ SY120 @ SV16 ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[5268]) ).
thf(5290,plain,
! [SV17: $i] :
( ( ! [SY121: $i,SY122: $i] :
( ( c_Com_Ocom_OCall @ SY122 @ SY121 @ SV17 )
!= c_Com_Ocom_OSKIP ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[5269]) ).
thf(5291,plain,
! [SV18: $i] :
( ( ! [SY123: $i,SY124: $i] :
( c_Com_Ocom_OSKIP
!= ( c_Com_Ocom_OCall @ SY124 @ SY123 @ SV18 ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[5270]) ).
thf(5292,plain,
! [SV19: $i] :
( ( ! [SY125: $i,SY126: $i,SY127: $i,SY128: $i] :
~ ( ~ ( ~ ( c_Natural_Oevaln @ ( c_Com_Ocom_OSemi @ SY128 @ SY127 ) @ SY126 @ SY125 @ SV19 )
| ~ ! [SY129: $i] :
~ ~ ( ~ ( c_Natural_Oevaln @ SY128 @ SY126 @ SY125 @ SY129 )
| ~ ( c_Natural_Oevaln @ SY127 @ SY129 @ SY125 @ SV19 ) ) )
| ~ ( ~ ~ ! [SY130: $i] :
~ ~ ( ~ ( c_Natural_Oevaln @ SY128 @ SY126 @ SY125 @ SY130 )
| ~ ( c_Natural_Oevaln @ SY127 @ SY130 @ SY125 @ SV19 ) )
| ( c_Natural_Oevaln @ ( c_Com_Ocom_OSemi @ SY128 @ SY127 ) @ SY126 @ SY125 @ SV19 ) ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[5271]) ).
thf(5293,plain,
! [SV20: $i] :
( ( ! [SY131: $i,SY132: $i] :
( ( c_Com_Ocom_OLocal @ SY132 @ SY131 @ SV20 )
!= c_Com_Ocom_OSKIP ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[5272]) ).
thf(5294,plain,
! [SV1: $i,SV21: $i] :
( ( c_Natural_Oevaln @ c_Com_Ocom_OSKIP @ SV21 @ SV1 @ SV21 )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[5273]) ).
thf(5295,plain,
! [SV2: $i,SV22: $i] :
( ( c_Natural_Oevaln @ c_Com_Ocom_OSKIP @ SV22 @ SV2 @ SV22 )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[5274]) ).
thf(5296,plain,
! [SV3: $i,SV23: $i] :
( ( ! [SY133: $i,SY134: $i,SY135: $i,SY136: $i,SY137: $i,SY138: $i,SY139: $i] :
( ( c_Com_Ocom_Ocom__case @ SY139 @ SY138 @ SY137 @ SY136 @ SY135 @ SY134 @ SY133 @ SV23 @ SV3 @ c_Com_Ocom_OSKIP )
= SY138 ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[5275]) ).
thf(5297,plain,
! [SV4: $i,SV24: $i] :
( ( ! [SY140: $i,SY141: $i,SY142: $i,SY143: $i,SY144: $i,SY145: $i,SY146: $i] :
( ( c_Com_Ocom_Ocom__rec @ SY146 @ SY145 @ SY144 @ SY143 @ SY142 @ SY141 @ SY140 @ SV24 @ SV4 @ c_Com_Ocom_OSKIP )
= SY145 ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[5276]) ).
thf(5298,plain,
! [SV5: $i,SV25: $i] :
( ( ! [SY147: $i] :
( ( c_Com_Ocom_OCond @ SY147 @ SV25 @ SV5 )
!= c_Com_Ocom_OSKIP ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[5277]) ).
thf(5299,plain,
! [SV6: $i,SV26: $i] :
( ( ! [SY148: $i,SY149: $i,SY150: $i,SY151: $i] :
( ~ ( c_Natural_Oevaln @ SY151 @ SY150 @ SY149 @ SY148 )
| ~ ( c_Natural_Oevaln @ SV26 @ SY148 @ SY149 @ SV6 )
| ( c_Natural_Oevaln @ ( c_Com_Ocom_OSemi @ SY151 @ SV26 ) @ SY150 @ SY149 @ SV6 ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[5278]) ).
thf(5300,plain,
! [SV7: $i,SV27: $i] :
( ( ( c_Com_Ocom_OAss @ SV27 @ SV7 )
!= c_Com_Ocom_OSKIP )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[5279]) ).
thf(5301,plain,
! [SV8: $i,SV28: $i] :
( ( ( c_Com_Ocom_OSemi @ SV28 @ SV8 )
!= c_Com_Ocom_OSKIP )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[5280]) ).
thf(5302,plain,
! [SV9: $i,SV29: $i] :
( ( c_Com_Ocom_OSKIP
!= ( c_Com_Ocom_OSemi @ SV29 @ SV9 ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[5281]) ).
thf(5303,plain,
! [SV10: $i,SV30: $i] :
( ( ! [SY152: $i] :
( c_Com_Ocom_OSKIP
!= ( c_Com_Ocom_OCond @ SY152 @ SV30 @ SV10 ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[5282]) ).
thf(5304,plain,
! [SV11: $i,SV31: $i] :
( ( ! [SY153: $i] :
( c_Com_Ocom_OSKIP
!= ( c_Com_Ocom_OLocal @ SY153 @ SV31 @ SV11 ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[5283]) ).
thf(5305,plain,
! [SV12: $i,SV32: $i] :
( ( ! [SY154: $i] :
( ~ ( c_Natural_Oevaln @ c_Com_Ocom_OSKIP @ SY154 @ SV32 @ SV12 )
| ( SV12 = SY154 ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[5284]) ).
thf(5306,plain,
! [SV13: $i,SV33: $i] :
( ( ! [SY155: $i,SY156: $i,SY157: $i] :
( ~ ( c_Natural_Oevaln @ ( c_Com_Ocom_OSemi @ SY157 @ SY156 ) @ SY155 @ SV33 @ SV13 )
| ~ ! [SY158: $i] :
( ~ ( c_Natural_Oevaln @ SY157 @ SY155 @ SV33 @ SY158 )
| ~ ( c_Natural_Oevaln @ SY156 @ SY158 @ SV33 @ SV13 ) ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[5285]) ).
thf(5307,plain,
! [SV14: $i,SV34: $i] :
( ( ( c_Com_Ocom_OWhile @ SV34 @ SV14 )
!= c_Com_Ocom_OSKIP )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[5286]) ).
thf(5308,plain,
! [SV15: $i,SV35: $i] :
( ( c_Com_Ocom_OSKIP
!= ( c_Com_Ocom_OWhile @ SV35 @ SV15 ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[5287]) ).
thf(5309,plain,
( ( ~ ( c_Natural_Oevaln @ c_Com_Ocom_OSKIP @ sK2_SY76 @ v_n @ sK3_SX0 )
| ( v_P @ sK1_B_Z @ sK3_SX0 ) )
= $false ),
inference(extcnf_forall_neg,[status(esa)],[5288]) ).
thf(5310,plain,
! [SV16: $i,SV36: $i] :
( ( c_Com_Ocom_OSKIP
!= ( c_Com_Ocom_OAss @ SV36 @ SV16 ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[5289]) ).
thf(5311,plain,
! [SV17: $i,SV37: $i] :
( ( ! [SY159: $i] :
( ( c_Com_Ocom_OCall @ SY159 @ SV37 @ SV17 )
!= c_Com_Ocom_OSKIP ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[5290]) ).
thf(5312,plain,
! [SV18: $i,SV38: $i] :
( ( ! [SY160: $i] :
( c_Com_Ocom_OSKIP
!= ( c_Com_Ocom_OCall @ SY160 @ SV38 @ SV18 ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[5291]) ).
thf(5313,plain,
! [SV19: $i,SV39: $i] :
( ( ! [SY161: $i,SY162: $i,SY163: $i] :
~ ( ~ ( ~ ( c_Natural_Oevaln @ ( c_Com_Ocom_OSemi @ SY163 @ SY162 ) @ SY161 @ SV39 @ SV19 )
| ~ ! [SY164: $i] :
~ ~ ( ~ ( c_Natural_Oevaln @ SY163 @ SY161 @ SV39 @ SY164 )
| ~ ( c_Natural_Oevaln @ SY162 @ SY164 @ SV39 @ SV19 ) ) )
| ~ ( ~ ~ ! [SY165: $i] :
~ ~ ( ~ ( c_Natural_Oevaln @ SY163 @ SY161 @ SV39 @ SY165 )
| ~ ( c_Natural_Oevaln @ SY162 @ SY165 @ SV39 @ SV19 ) )
| ( c_Natural_Oevaln @ ( c_Com_Ocom_OSemi @ SY163 @ SY162 ) @ SY161 @ SV39 @ SV19 ) ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[5292]) ).
thf(5314,plain,
! [SV20: $i,SV40: $i] :
( ( ! [SY166: $i] :
( ( c_Com_Ocom_OLocal @ SY166 @ SV40 @ SV20 )
!= c_Com_Ocom_OSKIP ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[5293]) ).
thf(5315,plain,
! [SV3: $i,SV23: $i,SV41: $i] :
( ( ! [SY167: $i,SY168: $i,SY169: $i,SY170: $i,SY171: $i,SY172: $i] :
( ( c_Com_Ocom_Ocom__case @ SY172 @ SY171 @ SY170 @ SY169 @ SY168 @ SY167 @ SV41 @ SV23 @ SV3 @ c_Com_Ocom_OSKIP )
= SY171 ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[5296]) ).
thf(5316,plain,
! [SV4: $i,SV24: $i,SV42: $i] :
( ( ! [SY173: $i,SY174: $i,SY175: $i,SY176: $i,SY177: $i,SY178: $i] :
( ( c_Com_Ocom_Ocom__rec @ SY178 @ SY177 @ SY176 @ SY175 @ SY174 @ SY173 @ SV42 @ SV24 @ SV4 @ c_Com_Ocom_OSKIP )
= SY177 ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[5297]) ).
thf(5317,plain,
! [SV5: $i,SV25: $i,SV43: $i] :
( ( ( c_Com_Ocom_OCond @ SV43 @ SV25 @ SV5 )
!= c_Com_Ocom_OSKIP )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[5298]) ).
thf(5318,plain,
! [SV6: $i,SV26: $i,SV44: $i] :
( ( ! [SY179: $i,SY180: $i,SY181: $i] :
( ~ ( c_Natural_Oevaln @ SY181 @ SY180 @ SY179 @ SV44 )
| ~ ( c_Natural_Oevaln @ SV26 @ SV44 @ SY179 @ SV6 )
| ( c_Natural_Oevaln @ ( c_Com_Ocom_OSemi @ SY181 @ SV26 ) @ SY180 @ SY179 @ SV6 ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[5299]) ).
thf(5319,plain,
! [SV7: $i,SV27: $i] :
( ( ( c_Com_Ocom_OAss @ SV27 @ SV7 )
= c_Com_Ocom_OSKIP )
= $false ),
inference(extcnf_not_pos,[status(thm)],[5300]) ).
thf(5320,plain,
! [SV8: $i,SV28: $i] :
( ( ( c_Com_Ocom_OSemi @ SV28 @ SV8 )
= c_Com_Ocom_OSKIP )
= $false ),
inference(extcnf_not_pos,[status(thm)],[5301]) ).
thf(5321,plain,
! [SV9: $i,SV29: $i] :
( ( c_Com_Ocom_OSKIP
= ( c_Com_Ocom_OSemi @ SV29 @ SV9 ) )
= $false ),
inference(extcnf_not_pos,[status(thm)],[5302]) ).
thf(5322,plain,
! [SV10: $i,SV30: $i,SV45: $i] :
( ( c_Com_Ocom_OSKIP
!= ( c_Com_Ocom_OCond @ SV45 @ SV30 @ SV10 ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[5303]) ).
thf(5323,plain,
! [SV11: $i,SV31: $i,SV46: $i] :
( ( c_Com_Ocom_OSKIP
!= ( c_Com_Ocom_OLocal @ SV46 @ SV31 @ SV11 ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[5304]) ).
thf(5324,plain,
! [SV12: $i,SV32: $i,SV47: $i] :
( ( ~ ( c_Natural_Oevaln @ c_Com_Ocom_OSKIP @ SV47 @ SV32 @ SV12 )
| ( SV12 = SV47 ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[5305]) ).
thf(5325,plain,
! [SV13: $i,SV33: $i,SV48: $i] :
( ( ! [SY182: $i,SY183: $i] :
( ~ ( c_Natural_Oevaln @ ( c_Com_Ocom_OSemi @ SY183 @ SY182 ) @ SV48 @ SV33 @ SV13 )
| ~ ! [SY184: $i] :
( ~ ( c_Natural_Oevaln @ SY183 @ SV48 @ SV33 @ SY184 )
| ~ ( c_Natural_Oevaln @ SY182 @ SY184 @ SV33 @ SV13 ) ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[5306]) ).
thf(5326,plain,
! [SV14: $i,SV34: $i] :
( ( ( c_Com_Ocom_OWhile @ SV34 @ SV14 )
= c_Com_Ocom_OSKIP )
= $false ),
inference(extcnf_not_pos,[status(thm)],[5307]) ).
thf(5327,plain,
! [SV15: $i,SV35: $i] :
( ( c_Com_Ocom_OSKIP
= ( c_Com_Ocom_OWhile @ SV35 @ SV15 ) )
= $false ),
inference(extcnf_not_pos,[status(thm)],[5308]) ).
thf(5328,plain,
( ( ~ ( c_Natural_Oevaln @ c_Com_Ocom_OSKIP @ sK2_SY76 @ v_n @ sK3_SX0 ) )
= $false ),
inference(extcnf_or_neg,[status(thm)],[5309]) ).
thf(5329,plain,
( ( v_P @ sK1_B_Z @ sK3_SX0 )
= $false ),
inference(extcnf_or_neg,[status(thm)],[5309]) ).
thf(5330,plain,
! [SV16: $i,SV36: $i] :
( ( c_Com_Ocom_OSKIP
= ( c_Com_Ocom_OAss @ SV36 @ SV16 ) )
= $false ),
inference(extcnf_not_pos,[status(thm)],[5310]) ).
thf(5331,plain,
! [SV17: $i,SV37: $i,SV49: $i] :
( ( ( c_Com_Ocom_OCall @ SV49 @ SV37 @ SV17 )
!= c_Com_Ocom_OSKIP )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[5311]) ).
thf(5332,plain,
! [SV18: $i,SV38: $i,SV50: $i] :
( ( c_Com_Ocom_OSKIP
!= ( c_Com_Ocom_OCall @ SV50 @ SV38 @ SV18 ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[5312]) ).
thf(5333,plain,
! [SV19: $i,SV39: $i,SV51: $i] :
( ( ! [SY185: $i,SY186: $i] :
~ ( ~ ( ~ ( c_Natural_Oevaln @ ( c_Com_Ocom_OSemi @ SY186 @ SY185 ) @ SV51 @ SV39 @ SV19 )
| ~ ! [SY187: $i] :
~ ~ ( ~ ( c_Natural_Oevaln @ SY186 @ SV51 @ SV39 @ SY187 )
| ~ ( c_Natural_Oevaln @ SY185 @ SY187 @ SV39 @ SV19 ) ) )
| ~ ( ~ ~ ! [SY188: $i] :
~ ~ ( ~ ( c_Natural_Oevaln @ SY186 @ SV51 @ SV39 @ SY188 )
| ~ ( c_Natural_Oevaln @ SY185 @ SY188 @ SV39 @ SV19 ) )
| ( c_Natural_Oevaln @ ( c_Com_Ocom_OSemi @ SY186 @ SY185 ) @ SV51 @ SV39 @ SV19 ) ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[5313]) ).
thf(5334,plain,
! [SV20: $i,SV40: $i,SV52: $i] :
( ( ( c_Com_Ocom_OLocal @ SV52 @ SV40 @ SV20 )
!= c_Com_Ocom_OSKIP )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[5314]) ).
thf(5335,plain,
! [SV3: $i,SV23: $i,SV41: $i,SV53: $i] :
( ( ! [SY189: $i,SY190: $i,SY191: $i,SY192: $i,SY193: $i] :
( ( c_Com_Ocom_Ocom__case @ SY193 @ SY192 @ SY191 @ SY190 @ SY189 @ SV53 @ SV41 @ SV23 @ SV3 @ c_Com_Ocom_OSKIP )
= SY192 ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[5315]) ).
thf(5336,plain,
! [SV4: $i,SV24: $i,SV42: $i,SV54: $i] :
( ( ! [SY194: $i,SY195: $i,SY196: $i,SY197: $i,SY198: $i] :
( ( c_Com_Ocom_Ocom__rec @ SY198 @ SY197 @ SY196 @ SY195 @ SY194 @ SV54 @ SV42 @ SV24 @ SV4 @ c_Com_Ocom_OSKIP )
= SY197 ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[5316]) ).
thf(5337,plain,
! [SV5: $i,SV25: $i,SV43: $i] :
( ( ( c_Com_Ocom_OCond @ SV43 @ SV25 @ SV5 )
= c_Com_Ocom_OSKIP )
= $false ),
inference(extcnf_not_pos,[status(thm)],[5317]) ).
thf(5338,plain,
! [SV6: $i,SV26: $i,SV44: $i,SV55: $i] :
( ( ! [SY199: $i,SY200: $i] :
( ~ ( c_Natural_Oevaln @ SY200 @ SY199 @ SV55 @ SV44 )
| ~ ( c_Natural_Oevaln @ SV26 @ SV44 @ SV55 @ SV6 )
| ( c_Natural_Oevaln @ ( c_Com_Ocom_OSemi @ SY200 @ SV26 ) @ SY199 @ SV55 @ SV6 ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[5318]) ).
thf(5339,plain,
! [SV10: $i,SV30: $i,SV45: $i] :
( ( c_Com_Ocom_OSKIP
= ( c_Com_Ocom_OCond @ SV45 @ SV30 @ SV10 ) )
= $false ),
inference(extcnf_not_pos,[status(thm)],[5322]) ).
thf(5340,plain,
! [SV11: $i,SV31: $i,SV46: $i] :
( ( c_Com_Ocom_OSKIP
= ( c_Com_Ocom_OLocal @ SV46 @ SV31 @ SV11 ) )
= $false ),
inference(extcnf_not_pos,[status(thm)],[5323]) ).
thf(5341,plain,
! [SV12: $i,SV32: $i,SV47: $i] :
( ( ( ~ ( c_Natural_Oevaln @ c_Com_Ocom_OSKIP @ SV47 @ SV32 @ SV12 ) )
= $true )
| ( ( SV12 = SV47 )
= $true ) ),
inference(extcnf_or_pos,[status(thm)],[5324]) ).
thf(5342,plain,
! [SV13: $i,SV33: $i,SV48: $i,SV56: $i] :
( ( ! [SY201: $i] :
( ~ ( c_Natural_Oevaln @ ( c_Com_Ocom_OSemi @ SY201 @ SV56 ) @ SV48 @ SV33 @ SV13 )
| ~ ! [SY202: $i] :
( ~ ( c_Natural_Oevaln @ SY201 @ SV48 @ SV33 @ SY202 )
| ~ ( c_Natural_Oevaln @ SV56 @ SY202 @ SV33 @ SV13 ) ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[5325]) ).
thf(5343,plain,
( ( c_Natural_Oevaln @ c_Com_Ocom_OSKIP @ sK2_SY76 @ v_n @ sK3_SX0 )
= $true ),
inference(extcnf_not_neg,[status(thm)],[5328]) ).
thf(5344,plain,
! [SV17: $i,SV37: $i,SV49: $i] :
( ( ( c_Com_Ocom_OCall @ SV49 @ SV37 @ SV17 )
= c_Com_Ocom_OSKIP )
= $false ),
inference(extcnf_not_pos,[status(thm)],[5331]) ).
thf(5345,plain,
! [SV18: $i,SV38: $i,SV50: $i] :
( ( c_Com_Ocom_OSKIP
= ( c_Com_Ocom_OCall @ SV50 @ SV38 @ SV18 ) )
= $false ),
inference(extcnf_not_pos,[status(thm)],[5332]) ).
thf(5346,plain,
! [SV19: $i,SV39: $i,SV51: $i,SV57: $i] :
( ( ! [SY203: $i] :
~ ( ~ ( ~ ( c_Natural_Oevaln @ ( c_Com_Ocom_OSemi @ SY203 @ SV57 ) @ SV51 @ SV39 @ SV19 )
| ~ ! [SY204: $i] :
~ ~ ( ~ ( c_Natural_Oevaln @ SY203 @ SV51 @ SV39 @ SY204 )
| ~ ( c_Natural_Oevaln @ SV57 @ SY204 @ SV39 @ SV19 ) ) )
| ~ ( ~ ~ ! [SY205: $i] :
~ ~ ( ~ ( c_Natural_Oevaln @ SY203 @ SV51 @ SV39 @ SY205 )
| ~ ( c_Natural_Oevaln @ SV57 @ SY205 @ SV39 @ SV19 ) )
| ( c_Natural_Oevaln @ ( c_Com_Ocom_OSemi @ SY203 @ SV57 ) @ SV51 @ SV39 @ SV19 ) ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[5333]) ).
thf(5347,plain,
! [SV20: $i,SV40: $i,SV52: $i] :
( ( ( c_Com_Ocom_OLocal @ SV52 @ SV40 @ SV20 )
= c_Com_Ocom_OSKIP )
= $false ),
inference(extcnf_not_pos,[status(thm)],[5334]) ).
thf(5348,plain,
! [SV3: $i,SV23: $i,SV41: $i,SV53: $i,SV58: $i] :
( ( ! [SY206: $i,SY207: $i,SY208: $i,SY209: $i] :
( ( c_Com_Ocom_Ocom__case @ SY209 @ SY208 @ SY207 @ SY206 @ SV58 @ SV53 @ SV41 @ SV23 @ SV3 @ c_Com_Ocom_OSKIP )
= SY208 ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[5335]) ).
thf(5349,plain,
! [SV4: $i,SV24: $i,SV42: $i,SV54: $i,SV59: $i] :
( ( ! [SY210: $i,SY211: $i,SY212: $i,SY213: $i] :
( ( c_Com_Ocom_Ocom__rec @ SY213 @ SY212 @ SY211 @ SY210 @ SV59 @ SV54 @ SV42 @ SV24 @ SV4 @ c_Com_Ocom_OSKIP )
= SY212 ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[5336]) ).
thf(5350,plain,
! [SV6: $i,SV26: $i,SV44: $i,SV55: $i,SV60: $i] :
( ( ! [SY214: $i] :
( ~ ( c_Natural_Oevaln @ SY214 @ SV60 @ SV55 @ SV44 )
| ~ ( c_Natural_Oevaln @ SV26 @ SV44 @ SV55 @ SV6 )
| ( c_Natural_Oevaln @ ( c_Com_Ocom_OSemi @ SY214 @ SV26 ) @ SV60 @ SV55 @ SV6 ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[5338]) ).
thf(5351,plain,
! [SV12: $i,SV32: $i,SV47: $i] :
( ( ( c_Natural_Oevaln @ c_Com_Ocom_OSKIP @ SV47 @ SV32 @ SV12 )
= $false )
| ( ( SV12 = SV47 )
= $true ) ),
inference(extcnf_not_pos,[status(thm)],[5341]) ).
thf(5352,plain,
! [SV13: $i,SV33: $i,SV48: $i,SV56: $i,SV61: $i] :
( ( ~ ( c_Natural_Oevaln @ ( c_Com_Ocom_OSemi @ SV61 @ SV56 ) @ SV48 @ SV33 @ SV13 )
| ~ ! [SY215: $i] :
( ~ ( c_Natural_Oevaln @ SV61 @ SV48 @ SV33 @ SY215 )
| ~ ( c_Natural_Oevaln @ SV56 @ SY215 @ SV33 @ SV13 ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[5342]) ).
thf(5353,plain,
! [SV19: $i,SV39: $i,SV51: $i,SV57: $i,SV62: $i] :
( ( ~ ( ~ ( ~ ( c_Natural_Oevaln @ ( c_Com_Ocom_OSemi @ SV62 @ SV57 ) @ SV51 @ SV39 @ SV19 )
| ~ ! [SY216: $i] :
~ ~ ( ~ ( c_Natural_Oevaln @ SV62 @ SV51 @ SV39 @ SY216 )
| ~ ( c_Natural_Oevaln @ SV57 @ SY216 @ SV39 @ SV19 ) ) )
| ~ ( ~ ~ ! [SY217: $i] :
~ ~ ( ~ ( c_Natural_Oevaln @ SV62 @ SV51 @ SV39 @ SY217 )
| ~ ( c_Natural_Oevaln @ SV57 @ SY217 @ SV39 @ SV19 ) )
| ( c_Natural_Oevaln @ ( c_Com_Ocom_OSemi @ SV62 @ SV57 ) @ SV51 @ SV39 @ SV19 ) ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[5346]) ).
thf(5354,plain,
! [SV3: $i,SV23: $i,SV41: $i,SV53: $i,SV58: $i,SV63: $i] :
( ( ! [SY218: $i,SY219: $i,SY220: $i] :
( ( c_Com_Ocom_Ocom__case @ SY220 @ SY219 @ SY218 @ SV63 @ SV58 @ SV53 @ SV41 @ SV23 @ SV3 @ c_Com_Ocom_OSKIP )
= SY219 ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[5348]) ).
thf(5355,plain,
! [SV4: $i,SV24: $i,SV42: $i,SV54: $i,SV59: $i,SV64: $i] :
( ( ! [SY221: $i,SY222: $i,SY223: $i] :
( ( c_Com_Ocom_Ocom__rec @ SY223 @ SY222 @ SY221 @ SV64 @ SV59 @ SV54 @ SV42 @ SV24 @ SV4 @ c_Com_Ocom_OSKIP )
= SY222 ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[5349]) ).
thf(5356,plain,
! [SV6: $i,SV26: $i,SV44: $i,SV55: $i,SV60: $i,SV65: $i] :
( ( ~ ( c_Natural_Oevaln @ SV65 @ SV60 @ SV55 @ SV44 )
| ~ ( c_Natural_Oevaln @ SV26 @ SV44 @ SV55 @ SV6 )
| ( c_Natural_Oevaln @ ( c_Com_Ocom_OSemi @ SV65 @ SV26 ) @ SV60 @ SV55 @ SV6 ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[5350]) ).
thf(5357,plain,
! [SV13: $i,SV33: $i,SV48: $i,SV56: $i,SV61: $i] :
( ( ( ~ ( c_Natural_Oevaln @ ( c_Com_Ocom_OSemi @ SV61 @ SV56 ) @ SV48 @ SV33 @ SV13 ) )
= $true )
| ( ( ~ ! [SY215: $i] :
( ~ ( c_Natural_Oevaln @ SV61 @ SV48 @ SV33 @ SY215 )
| ~ ( c_Natural_Oevaln @ SV56 @ SY215 @ SV33 @ SV13 ) ) )
= $true ) ),
inference(extcnf_or_pos,[status(thm)],[5352]) ).
thf(5358,plain,
! [SV19: $i,SV39: $i,SV51: $i,SV57: $i,SV62: $i] :
( ( ~ ( ~ ( c_Natural_Oevaln @ ( c_Com_Ocom_OSemi @ SV62 @ SV57 ) @ SV51 @ SV39 @ SV19 )
| ~ ! [SY216: $i] :
~ ~ ( ~ ( c_Natural_Oevaln @ SV62 @ SV51 @ SV39 @ SY216 )
| ~ ( c_Natural_Oevaln @ SV57 @ SY216 @ SV39 @ SV19 ) ) )
| ~ ( ~ ~ ! [SY217: $i] :
~ ~ ( ~ ( c_Natural_Oevaln @ SV62 @ SV51 @ SV39 @ SY217 )
| ~ ( c_Natural_Oevaln @ SV57 @ SY217 @ SV39 @ SV19 ) )
| ( c_Natural_Oevaln @ ( c_Com_Ocom_OSemi @ SV62 @ SV57 ) @ SV51 @ SV39 @ SV19 ) ) )
= $false ),
inference(extcnf_not_pos,[status(thm)],[5353]) ).
thf(5359,plain,
! [SV3: $i,SV23: $i,SV41: $i,SV53: $i,SV58: $i,SV63: $i,SV66: $i] :
( ( ! [SY224: $i,SY225: $i] :
( ( c_Com_Ocom_Ocom__case @ SY225 @ SY224 @ SV66 @ SV63 @ SV58 @ SV53 @ SV41 @ SV23 @ SV3 @ c_Com_Ocom_OSKIP )
= SY224 ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[5354]) ).
thf(5360,plain,
! [SV4: $i,SV24: $i,SV42: $i,SV54: $i,SV59: $i,SV64: $i,SV67: $i] :
( ( ! [SY226: $i,SY227: $i] :
( ( c_Com_Ocom_Ocom__rec @ SY227 @ SY226 @ SV67 @ SV64 @ SV59 @ SV54 @ SV42 @ SV24 @ SV4 @ c_Com_Ocom_OSKIP )
= SY226 ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[5355]) ).
thf(5361,plain,
! [SV6: $i,SV26: $i,SV44: $i,SV55: $i,SV60: $i,SV65: $i] :
( ( ( ~ ( c_Natural_Oevaln @ SV65 @ SV60 @ SV55 @ SV44 ) )
= $true )
| ( ( ~ ( c_Natural_Oevaln @ SV26 @ SV44 @ SV55 @ SV6 )
| ( c_Natural_Oevaln @ ( c_Com_Ocom_OSemi @ SV65 @ SV26 ) @ SV60 @ SV55 @ SV6 ) )
= $true ) ),
inference(extcnf_or_pos,[status(thm)],[5356]) ).
thf(5362,plain,
! [SV13: $i,SV33: $i,SV48: $i,SV56: $i,SV61: $i] :
( ( ( c_Natural_Oevaln @ ( c_Com_Ocom_OSemi @ SV61 @ SV56 ) @ SV48 @ SV33 @ SV13 )
= $false )
| ( ( ~ ! [SY215: $i] :
( ~ ( c_Natural_Oevaln @ SV61 @ SV48 @ SV33 @ SY215 )
| ~ ( c_Natural_Oevaln @ SV56 @ SY215 @ SV33 @ SV13 ) ) )
= $true ) ),
inference(extcnf_not_pos,[status(thm)],[5357]) ).
thf(5363,plain,
! [SV19: $i,SV39: $i,SV51: $i,SV57: $i,SV62: $i] :
( ( ~ ( ~ ( c_Natural_Oevaln @ ( c_Com_Ocom_OSemi @ SV62 @ SV57 ) @ SV51 @ SV39 @ SV19 )
| ~ ! [SY216: $i] :
~ ~ ( ~ ( c_Natural_Oevaln @ SV62 @ SV51 @ SV39 @ SY216 )
| ~ ( c_Natural_Oevaln @ SV57 @ SY216 @ SV39 @ SV19 ) ) ) )
= $false ),
inference(extcnf_or_neg,[status(thm)],[5358]) ).
thf(5364,plain,
! [SV19: $i,SV57: $i,SV39: $i,SV51: $i,SV62: $i] :
( ( ~ ( ~ ~ ! [SY217: $i] :
~ ~ ( ~ ( c_Natural_Oevaln @ SV62 @ SV51 @ SV39 @ SY217 )
| ~ ( c_Natural_Oevaln @ SV57 @ SY217 @ SV39 @ SV19 ) )
| ( c_Natural_Oevaln @ ( c_Com_Ocom_OSemi @ SV62 @ SV57 ) @ SV51 @ SV39 @ SV19 ) ) )
= $false ),
inference(extcnf_or_neg,[status(thm)],[5358]) ).
thf(5365,plain,
! [SV3: $i,SV23: $i,SV41: $i,SV53: $i,SV58: $i,SV63: $i,SV66: $i,SV68: $i] :
( ( ! [SY228: $i] :
( ( c_Com_Ocom_Ocom__case @ SY228 @ SV68 @ SV66 @ SV63 @ SV58 @ SV53 @ SV41 @ SV23 @ SV3 @ c_Com_Ocom_OSKIP )
= SV68 ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[5359]) ).
thf(5366,plain,
! [SV4: $i,SV24: $i,SV42: $i,SV54: $i,SV59: $i,SV64: $i,SV67: $i,SV69: $i] :
( ( ! [SY229: $i] :
( ( c_Com_Ocom_Ocom__rec @ SY229 @ SV69 @ SV67 @ SV64 @ SV59 @ SV54 @ SV42 @ SV24 @ SV4 @ c_Com_Ocom_OSKIP )
= SV69 ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[5360]) ).
thf(5367,plain,
! [SV6: $i,SV26: $i,SV44: $i,SV55: $i,SV60: $i,SV65: $i] :
( ( ( c_Natural_Oevaln @ SV65 @ SV60 @ SV55 @ SV44 )
= $false )
| ( ( ~ ( c_Natural_Oevaln @ SV26 @ SV44 @ SV55 @ SV6 )
| ( c_Natural_Oevaln @ ( c_Com_Ocom_OSemi @ SV65 @ SV26 ) @ SV60 @ SV55 @ SV6 ) )
= $true ) ),
inference(extcnf_not_pos,[status(thm)],[5361]) ).
thf(5368,plain,
! [SV13: $i,SV56: $i,SV33: $i,SV48: $i,SV61: $i] :
( ( ( ! [SY215: $i] :
( ~ ( c_Natural_Oevaln @ SV61 @ SV48 @ SV33 @ SY215 )
| ~ ( c_Natural_Oevaln @ SV56 @ SY215 @ SV33 @ SV13 ) ) )
= $false )
| ( ( c_Natural_Oevaln @ ( c_Com_Ocom_OSemi @ SV61 @ SV56 ) @ SV48 @ SV33 @ SV13 )
= $false ) ),
inference(extcnf_not_pos,[status(thm)],[5362]) ).
thf(5369,plain,
! [SV19: $i,SV39: $i,SV51: $i,SV57: $i,SV62: $i] :
( ( ~ ( c_Natural_Oevaln @ ( c_Com_Ocom_OSemi @ SV62 @ SV57 ) @ SV51 @ SV39 @ SV19 )
| ~ ! [SY216: $i] :
~ ~ ( ~ ( c_Natural_Oevaln @ SV62 @ SV51 @ SV39 @ SY216 )
| ~ ( c_Natural_Oevaln @ SV57 @ SY216 @ SV39 @ SV19 ) ) )
= $true ),
inference(extcnf_not_neg,[status(thm)],[5363]) ).
thf(5370,plain,
! [SV19: $i,SV57: $i,SV39: $i,SV51: $i,SV62: $i] :
( ( ~ ~ ! [SY217: $i] :
~ ~ ( ~ ( c_Natural_Oevaln @ SV62 @ SV51 @ SV39 @ SY217 )
| ~ ( c_Natural_Oevaln @ SV57 @ SY217 @ SV39 @ SV19 ) )
| ( c_Natural_Oevaln @ ( c_Com_Ocom_OSemi @ SV62 @ SV57 ) @ SV51 @ SV39 @ SV19 ) )
= $true ),
inference(extcnf_not_neg,[status(thm)],[5364]) ).
thf(5371,plain,
! [SV3: $i,SV23: $i,SV41: $i,SV53: $i,SV58: $i,SV63: $i,SV66: $i,SV68: $i,SV70: $i] :
( ( ( c_Com_Ocom_Ocom__case @ SV70 @ SV68 @ SV66 @ SV63 @ SV58 @ SV53 @ SV41 @ SV23 @ SV3 @ c_Com_Ocom_OSKIP )
= SV68 )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[5365]) ).
thf(5372,plain,
! [SV4: $i,SV24: $i,SV42: $i,SV54: $i,SV59: $i,SV64: $i,SV67: $i,SV69: $i,SV71: $i] :
( ( ( c_Com_Ocom_Ocom__rec @ SV71 @ SV69 @ SV67 @ SV64 @ SV59 @ SV54 @ SV42 @ SV24 @ SV4 @ c_Com_Ocom_OSKIP )
= SV69 )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[5366]) ).
thf(5373,plain,
! [SV60: $i,SV65: $i,SV6: $i,SV55: $i,SV44: $i,SV26: $i] :
( ( ( ~ ( c_Natural_Oevaln @ SV26 @ SV44 @ SV55 @ SV6 ) )
= $true )
| ( ( c_Natural_Oevaln @ ( c_Com_Ocom_OSemi @ SV65 @ SV26 ) @ SV60 @ SV55 @ SV6 )
= $true )
| ( ( c_Natural_Oevaln @ SV65 @ SV60 @ SV55 @ SV44 )
= $false ) ),
inference(extcnf_or_pos,[status(thm)],[5367]) ).
thf(5374,plain,
! [SV56: $i,SV13: $i,SV33: $i,SV48: $i,SV61: $i] :
( ( ( ~ ( c_Natural_Oevaln @ SV61 @ SV48 @ SV33 @ ( sK4_SY215 @ SV13 @ SV56 @ SV33 @ SV48 @ SV61 ) )
| ~ ( c_Natural_Oevaln @ SV56 @ ( sK4_SY215 @ SV13 @ SV56 @ SV33 @ SV48 @ SV61 ) @ SV33 @ SV13 ) )
= $false )
| ( ( c_Natural_Oevaln @ ( c_Com_Ocom_OSemi @ SV61 @ SV56 ) @ SV48 @ SV33 @ SV13 )
= $false ) ),
inference(extcnf_forall_neg,[status(esa)],[5368]) ).
thf(5375,plain,
! [SV19: $i,SV39: $i,SV51: $i,SV57: $i,SV62: $i] :
( ( ( ~ ( c_Natural_Oevaln @ ( c_Com_Ocom_OSemi @ SV62 @ SV57 ) @ SV51 @ SV39 @ SV19 ) )
= $true )
| ( ( ~ ! [SY216: $i] :
~ ~ ( ~ ( c_Natural_Oevaln @ SV62 @ SV51 @ SV39 @ SY216 )
| ~ ( c_Natural_Oevaln @ SV57 @ SY216 @ SV39 @ SV19 ) ) )
= $true ) ),
inference(extcnf_or_pos,[status(thm)],[5369]) ).
thf(5376,plain,
! [SV19: $i,SV57: $i,SV39: $i,SV51: $i,SV62: $i] :
( ( ( ~ ~ ! [SY217: $i] :
~ ~ ( ~ ( c_Natural_Oevaln @ SV62 @ SV51 @ SV39 @ SY217 )
| ~ ( c_Natural_Oevaln @ SV57 @ SY217 @ SV39 @ SV19 ) ) )
= $true )
| ( ( c_Natural_Oevaln @ ( c_Com_Ocom_OSemi @ SV62 @ SV57 ) @ SV51 @ SV39 @ SV19 )
= $true ) ),
inference(extcnf_or_pos,[status(thm)],[5370]) ).
thf(5377,plain,
! [SV60: $i,SV65: $i,SV6: $i,SV55: $i,SV44: $i,SV26: $i] :
( ( ( c_Natural_Oevaln @ SV26 @ SV44 @ SV55 @ SV6 )
= $false )
| ( ( c_Natural_Oevaln @ ( c_Com_Ocom_OSemi @ SV65 @ SV26 ) @ SV60 @ SV55 @ SV6 )
= $true )
| ( ( c_Natural_Oevaln @ SV65 @ SV60 @ SV55 @ SV44 )
= $false ) ),
inference(extcnf_not_pos,[status(thm)],[5373]) ).
thf(5378,plain,
! [SV56: $i,SV13: $i,SV33: $i,SV48: $i,SV61: $i] :
( ( ( ~ ( c_Natural_Oevaln @ SV61 @ SV48 @ SV33 @ ( sK4_SY215 @ SV13 @ SV56 @ SV33 @ SV48 @ SV61 ) ) )
= $false )
| ( ( c_Natural_Oevaln @ ( c_Com_Ocom_OSemi @ SV61 @ SV56 ) @ SV48 @ SV33 @ SV13 )
= $false ) ),
inference(extcnf_or_neg,[status(thm)],[5374]) ).
thf(5379,plain,
! [SV61: $i,SV48: $i,SV33: $i,SV13: $i,SV56: $i] :
( ( ( ~ ( c_Natural_Oevaln @ SV56 @ ( sK4_SY215 @ SV13 @ SV56 @ SV33 @ SV48 @ SV61 ) @ SV33 @ SV13 ) )
= $false )
| ( ( c_Natural_Oevaln @ ( c_Com_Ocom_OSemi @ SV61 @ SV56 ) @ SV48 @ SV33 @ SV13 )
= $false ) ),
inference(extcnf_or_neg,[status(thm)],[5374]) ).
thf(5380,plain,
! [SV19: $i,SV39: $i,SV51: $i,SV57: $i,SV62: $i] :
( ( ( c_Natural_Oevaln @ ( c_Com_Ocom_OSemi @ SV62 @ SV57 ) @ SV51 @ SV39 @ SV19 )
= $false )
| ( ( ~ ! [SY216: $i] :
~ ~ ( ~ ( c_Natural_Oevaln @ SV62 @ SV51 @ SV39 @ SY216 )
| ~ ( c_Natural_Oevaln @ SV57 @ SY216 @ SV39 @ SV19 ) ) )
= $true ) ),
inference(extcnf_not_pos,[status(thm)],[5375]) ).
thf(5381,plain,
! [SV19: $i,SV57: $i,SV39: $i,SV51: $i,SV62: $i] :
( ( ( ~ ! [SY217: $i] :
~ ~ ( ~ ( c_Natural_Oevaln @ SV62 @ SV51 @ SV39 @ SY217 )
| ~ ( c_Natural_Oevaln @ SV57 @ SY217 @ SV39 @ SV19 ) ) )
= $false )
| ( ( c_Natural_Oevaln @ ( c_Com_Ocom_OSemi @ SV62 @ SV57 ) @ SV51 @ SV39 @ SV19 )
= $true ) ),
inference(extcnf_not_pos,[status(thm)],[5376]) ).
thf(5382,plain,
! [SV56: $i,SV13: $i,SV33: $i,SV48: $i,SV61: $i] :
( ( ( c_Natural_Oevaln @ SV61 @ SV48 @ SV33 @ ( sK4_SY215 @ SV13 @ SV56 @ SV33 @ SV48 @ SV61 ) )
= $true )
| ( ( c_Natural_Oevaln @ ( c_Com_Ocom_OSemi @ SV61 @ SV56 ) @ SV48 @ SV33 @ SV13 )
= $false ) ),
inference(extcnf_not_neg,[status(thm)],[5378]) ).
thf(5383,plain,
! [SV61: $i,SV48: $i,SV33: $i,SV13: $i,SV56: $i] :
( ( ( c_Natural_Oevaln @ SV56 @ ( sK4_SY215 @ SV13 @ SV56 @ SV33 @ SV48 @ SV61 ) @ SV33 @ SV13 )
= $true )
| ( ( c_Natural_Oevaln @ ( c_Com_Ocom_OSemi @ SV61 @ SV56 ) @ SV48 @ SV33 @ SV13 )
= $false ) ),
inference(extcnf_not_neg,[status(thm)],[5379]) ).
thf(5384,plain,
! [SV19: $i,SV57: $i,SV39: $i,SV51: $i,SV62: $i] :
( ( ( ! [SY216: $i] :
~ ~ ( ~ ( c_Natural_Oevaln @ SV62 @ SV51 @ SV39 @ SY216 )
| ~ ( c_Natural_Oevaln @ SV57 @ SY216 @ SV39 @ SV19 ) ) )
= $false )
| ( ( c_Natural_Oevaln @ ( c_Com_Ocom_OSemi @ SV62 @ SV57 ) @ SV51 @ SV39 @ SV19 )
= $false ) ),
inference(extcnf_not_pos,[status(thm)],[5380]) ).
thf(5385,plain,
! [SV19: $i,SV57: $i,SV39: $i,SV51: $i,SV62: $i] :
( ( ( ! [SY217: $i] :
~ ~ ( ~ ( c_Natural_Oevaln @ SV62 @ SV51 @ SV39 @ SY217 )
| ~ ( c_Natural_Oevaln @ SV57 @ SY217 @ SV39 @ SV19 ) ) )
= $true )
| ( ( c_Natural_Oevaln @ ( c_Com_Ocom_OSemi @ SV62 @ SV57 ) @ SV51 @ SV39 @ SV19 )
= $true ) ),
inference(extcnf_not_neg,[status(thm)],[5381]) ).
thf(5386,plain,
! [SV57: $i,SV19: $i,SV39: $i,SV51: $i,SV62: $i] :
( ( ( ~ ~ ( ~ ( c_Natural_Oevaln @ SV62 @ SV51 @ SV39 @ ( sK5_SY216 @ SV19 @ SV57 @ SV39 @ SV51 @ SV62 ) )
| ~ ( c_Natural_Oevaln @ SV57 @ ( sK5_SY216 @ SV19 @ SV57 @ SV39 @ SV51 @ SV62 ) @ SV39 @ SV19 ) ) )
= $false )
| ( ( c_Natural_Oevaln @ ( c_Com_Ocom_OSemi @ SV62 @ SV57 ) @ SV51 @ SV39 @ SV19 )
= $false ) ),
inference(extcnf_forall_neg,[status(esa)],[5384]) ).
thf(5387,plain,
! [SV19: $i,SV57: $i,SV72: $i,SV39: $i,SV51: $i,SV62: $i] :
( ( ( ~ ~ ( ~ ( c_Natural_Oevaln @ SV62 @ SV51 @ SV39 @ SV72 )
| ~ ( c_Natural_Oevaln @ SV57 @ SV72 @ SV39 @ SV19 ) ) )
= $true )
| ( ( c_Natural_Oevaln @ ( c_Com_Ocom_OSemi @ SV62 @ SV57 ) @ SV51 @ SV39 @ SV19 )
= $true ) ),
inference(extcnf_forall_pos,[status(thm)],[5385]) ).
thf(5388,plain,
! [SV57: $i,SV19: $i,SV39: $i,SV51: $i,SV62: $i] :
( ( ( ~ ( ~ ( c_Natural_Oevaln @ SV62 @ SV51 @ SV39 @ ( sK5_SY216 @ SV19 @ SV57 @ SV39 @ SV51 @ SV62 ) )
| ~ ( c_Natural_Oevaln @ SV57 @ ( sK5_SY216 @ SV19 @ SV57 @ SV39 @ SV51 @ SV62 ) @ SV39 @ SV19 ) ) )
= $true )
| ( ( c_Natural_Oevaln @ ( c_Com_Ocom_OSemi @ SV62 @ SV57 ) @ SV51 @ SV39 @ SV19 )
= $false ) ),
inference(extcnf_not_neg,[status(thm)],[5386]) ).
thf(5389,plain,
! [SV19: $i,SV57: $i,SV72: $i,SV39: $i,SV51: $i,SV62: $i] :
( ( ( ~ ( ~ ( c_Natural_Oevaln @ SV62 @ SV51 @ SV39 @ SV72 )
| ~ ( c_Natural_Oevaln @ SV57 @ SV72 @ SV39 @ SV19 ) ) )
= $false )
| ( ( c_Natural_Oevaln @ ( c_Com_Ocom_OSemi @ SV62 @ SV57 ) @ SV51 @ SV39 @ SV19 )
= $true ) ),
inference(extcnf_not_pos,[status(thm)],[5387]) ).
thf(5390,plain,
! [SV57: $i,SV19: $i,SV39: $i,SV51: $i,SV62: $i] :
( ( ( ~ ( c_Natural_Oevaln @ SV62 @ SV51 @ SV39 @ ( sK5_SY216 @ SV19 @ SV57 @ SV39 @ SV51 @ SV62 ) )
| ~ ( c_Natural_Oevaln @ SV57 @ ( sK5_SY216 @ SV19 @ SV57 @ SV39 @ SV51 @ SV62 ) @ SV39 @ SV19 ) )
= $false )
| ( ( c_Natural_Oevaln @ ( c_Com_Ocom_OSemi @ SV62 @ SV57 ) @ SV51 @ SV39 @ SV19 )
= $false ) ),
inference(extcnf_not_pos,[status(thm)],[5388]) ).
thf(5391,plain,
! [SV19: $i,SV57: $i,SV72: $i,SV39: $i,SV51: $i,SV62: $i] :
( ( ( ~ ( c_Natural_Oevaln @ SV62 @ SV51 @ SV39 @ SV72 )
| ~ ( c_Natural_Oevaln @ SV57 @ SV72 @ SV39 @ SV19 ) )
= $true )
| ( ( c_Natural_Oevaln @ ( c_Com_Ocom_OSemi @ SV62 @ SV57 ) @ SV51 @ SV39 @ SV19 )
= $true ) ),
inference(extcnf_not_neg,[status(thm)],[5389]) ).
thf(5392,plain,
! [SV57: $i,SV19: $i,SV39: $i,SV51: $i,SV62: $i] :
( ( ( ~ ( c_Natural_Oevaln @ SV62 @ SV51 @ SV39 @ ( sK5_SY216 @ SV19 @ SV57 @ SV39 @ SV51 @ SV62 ) ) )
= $false )
| ( ( c_Natural_Oevaln @ ( c_Com_Ocom_OSemi @ SV62 @ SV57 ) @ SV51 @ SV39 @ SV19 )
= $false ) ),
inference(extcnf_or_neg,[status(thm)],[5390]) ).
thf(5393,plain,
! [SV62: $i,SV51: $i,SV39: $i,SV19: $i,SV57: $i] :
( ( ( ~ ( c_Natural_Oevaln @ SV57 @ ( sK5_SY216 @ SV19 @ SV57 @ SV39 @ SV51 @ SV62 ) @ SV39 @ SV19 ) )
= $false )
| ( ( c_Natural_Oevaln @ ( c_Com_Ocom_OSemi @ SV62 @ SV57 ) @ SV51 @ SV39 @ SV19 )
= $false ) ),
inference(extcnf_or_neg,[status(thm)],[5390]) ).
thf(5394,plain,
! [SV19: $i,SV57: $i,SV72: $i,SV39: $i,SV51: $i,SV62: $i] :
( ( ( ~ ( c_Natural_Oevaln @ SV62 @ SV51 @ SV39 @ SV72 ) )
= $true )
| ( ( ~ ( c_Natural_Oevaln @ SV57 @ SV72 @ SV39 @ SV19 ) )
= $true )
| ( ( c_Natural_Oevaln @ ( c_Com_Ocom_OSemi @ SV62 @ SV57 ) @ SV51 @ SV39 @ SV19 )
= $true ) ),
inference(extcnf_or_pos,[status(thm)],[5391]) ).
thf(5395,plain,
! [SV57: $i,SV19: $i,SV39: $i,SV51: $i,SV62: $i] :
( ( ( c_Natural_Oevaln @ SV62 @ SV51 @ SV39 @ ( sK5_SY216 @ SV19 @ SV57 @ SV39 @ SV51 @ SV62 ) )
= $true )
| ( ( c_Natural_Oevaln @ ( c_Com_Ocom_OSemi @ SV62 @ SV57 ) @ SV51 @ SV39 @ SV19 )
= $false ) ),
inference(extcnf_not_neg,[status(thm)],[5392]) ).
thf(5396,plain,
! [SV62: $i,SV51: $i,SV39: $i,SV19: $i,SV57: $i] :
( ( ( c_Natural_Oevaln @ SV57 @ ( sK5_SY216 @ SV19 @ SV57 @ SV39 @ SV51 @ SV62 ) @ SV39 @ SV19 )
= $true )
| ( ( c_Natural_Oevaln @ ( c_Com_Ocom_OSemi @ SV62 @ SV57 ) @ SV51 @ SV39 @ SV19 )
= $false ) ),
inference(extcnf_not_neg,[status(thm)],[5393]) ).
thf(5397,plain,
! [SV19: $i,SV57: $i,SV72: $i,SV39: $i,SV51: $i,SV62: $i] :
( ( ( c_Natural_Oevaln @ SV62 @ SV51 @ SV39 @ SV72 )
= $false )
| ( ( ~ ( c_Natural_Oevaln @ SV57 @ SV72 @ SV39 @ SV19 ) )
= $true )
| ( ( c_Natural_Oevaln @ ( c_Com_Ocom_OSemi @ SV62 @ SV57 ) @ SV51 @ SV39 @ SV19 )
= $true ) ),
inference(extcnf_not_pos,[status(thm)],[5394]) ).
thf(5398,plain,
! [SV51: $i,SV62: $i,SV19: $i,SV39: $i,SV72: $i,SV57: $i] :
( ( ( c_Natural_Oevaln @ SV57 @ SV72 @ SV39 @ SV19 )
= $false )
| ( ( c_Natural_Oevaln @ SV62 @ SV51 @ SV39 @ SV72 )
= $false )
| ( ( c_Natural_Oevaln @ ( c_Com_Ocom_OSemi @ SV62 @ SV57 ) @ SV51 @ SV39 @ SV19 )
= $true ) ),
inference(extcnf_not_pos,[status(thm)],[5397]) ).
thf(5399,plain,
$false = $true,
inference(fo_atp_e,[status(thm)],[5254,5398,5396,5395,5383,5382,5377,5372,5371,5351,5347,5345,5344,5343,5340,5339,5337,5330,5329,5327,5326,5321,5320,5319,5295,5294]) ).
thf(5400,plain,
$false,
inference(solved_all_splits,[solved_all_splits(join,[])],[5399]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : SWW342+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.02 % Command : leo --cores 7 --timeout 300 --proofoutput 1 --foatp e --atp e=/export/starexec/sandbox/solver/bin/eprover /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.05/0.12 % Computer : n012.cluster.edu
% 0.05/0.12 % Model : x86_64 x86_64
% 0.05/0.12 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.05/0.12 % Memory : 8046.5625MB
% 0.05/0.12 % OS : Linux 6.8.0-71-generic
% 0.05/0.12 % CPULimit : 300
% 0.05/0.12 % WCLimit : 300
% 0.05/0.12 % DateTime : Tue Oct 6 16:54:17 UTC 2026
% 0.05/0.12 % CPUTime :
% 0.05/0.12 Running leo --cores 7 --timeout 300 --proofoutput 1 --foatp e --atp e=/export/starexec/sandbox/solver/bin/eprover /export/starexec/sandbox/benchmark/theBenchmark.p
% 42.41/8.60 ....................................
% 42.41/8.60
% 42.41/8.60 No.of.Axioms: 20
% 42.41/8.60
% 42.41/8.60 Length.of.Defs: 0
% 42.41/8.60
% 42.41/8.60 Contains.Choice.Funs: false
% 42.41/8.60 .............................................
% 42.41/8.60
% 42.41/8.60 ********************************
% 42.41/8.60 * All subproblems solved! *
% 42.41/8.60 ********************************
% 42.41/8.60 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p : (rf:1,axioms:21,ps:0,u:6,ude:true,rLeibEQ:true,rAndEQ:true,use_choice:true,use_extuni:true,use_extcnf_combined:false,expand_extuni:false,foatp:e,atp_timeout:296,atp_calls_frequency:5,ordering:none,proof_output:1,protocol_output:false,clause_count:5399,loop_count:0,foatp_calls:1,translation:fof_full)
% 42.41/8.60
% 42.41/8.60 %**** Beginning of derivation protocol ****
% 42.41/8.60 % SZS output start CNFRefutation
% See solution above
% 42.41/8.61
% 42.41/8.61 %**** End of derivation protocol ****
% 42.41/8.61 %**** no. of clauses in derivation: 215 ****
% 42.41/8.61 %**** clause counter: 5399 ****
% 42.41/8.61
% 42.41/8.61 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p : (rf:1,axioms:21,ps:0,u:6,ude:true,rLeibEQ:true,rAndEQ:true,use_choice:true,use_extuni:true,use_extcnf_combined:false,expand_extuni:false,foatp:e,atp_timeout:296,atp_calls_frequency:5,ordering:none,proof_output:1,protocol_output:false,clause_count:5399,loop_count:0,foatp_calls:1,translation:fof_full)
%------------------------------------------------------------------------------