%------------------------------------------------------------------------------ % File : cocATP---0.2.0 % Problem : SEU520^1 : TPTP v6.1.0. Released v3.7.0. % Transfm : none % Format : tptp:raw % Command : python CASC.py /export/starexec/sandbox/benchmark/theBenchmark.p % Computer : n095.star.cs.uiowa.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2609 0 2.40GHz % Memory : 32286.75MB % OS : Linux 2.6.32-431.20.3.el6.x86_64 % CPULimit : 300s % DateTime : Thu Jul 17 13:32:21 EDT 2014 % Result : Theorem 43.98s % Output : Proof 43.98s % Verified : % SZS Type : None (Parsing solution fails) % Syntax : Number of formulae : 0 % Comments : %------------------------------------------------------------------------------ %----ERROR: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % % Problem : SEU520^1 : TPTP v6.1.0. Released v3.7.0. % % Command : python CASC.py /export/starexec/sandbox/benchmark/theBenchmark.p % % Computer : n095.star.cs.uiowa.edu % % Model : x86_64 x86_64 % % CPU : Intel(R) Xeon(R) CPU E5-2609 0 @ 2.40GHz % % Memory : 32286.75MB % % OS : Linux 2.6.32-431.20.3.el6.x86_64 % % CPULimit : 300 % % DateTime : Thu Jul 17 10:29:41 CDT 2014 % % CPUTime : 43.98 % Python 2.7.5 % Using paths ['/home/cristobal/cocATP/CASC/TPTP/', '/export/starexec/sandbox/benchmark/', '/export/starexec/sandbox/benchmark/'] % FOF formula (<kernel.Constant object at 0x1dfed40>, <kernel.DependentProduct object at 0x2238e60>) of role type named in_type % Using role type % Declaring in:(fofType->(fofType->Prop)) % FOF formula (<kernel.Constant object at 0x21bb8c0>, <kernel.DependentProduct object at 0x2238e60>) of role type named exu_type % Using role type % Declaring exu:((fofType->Prop)->Prop) % FOF formula (((eq ((fofType->Prop)->Prop)) exu) (fun (Xphi:(fofType->Prop))=> ((ex fofType) (fun (Xx:fofType)=> ((and (Xphi Xx)) (forall (Xy:fofType), ((Xphi Xy)->(((eq fofType) Xx) Xy)))))))) of role definition named exu % A new definition: (((eq ((fofType->Prop)->Prop)) exu) (fun (Xphi:(fofType->Prop))=> ((ex fofType) (fun (Xx:fofType)=> ((and (Xphi Xx)) (forall (Xy:fofType), ((Xphi Xy)->(((eq fofType) Xx) Xy)))))))) % Defined: exu:=(fun (Xphi:(fofType->Prop))=> ((ex fofType) (fun (Xx:fofType)=> ((and (Xphi Xx)) (forall (Xy:fofType), ((Xphi Xy)->(((eq fofType) Xx) Xy))))))) % FOF formula (<kernel.Constant object at 0x1dfee60>, <kernel.Sort object at 0x1cc8998>) of role type named setextAx_type % Using role type % Declaring setextAx:Prop % FOF formula (((eq Prop) setextAx) (forall (A:fofType) (B:fofType), ((forall (Xx:fofType), ((iff ((in Xx) A)) ((in Xx) B)))->(((eq fofType) A) B)))) of role definition named setextAx % A new definition: (((eq Prop) setextAx) (forall (A:fofType) (B:fofType), ((forall (Xx:fofType), ((iff ((in Xx) A)) ((in Xx) B)))->(((eq fofType) A) B)))) % Defined: setextAx:=(forall (A:fofType) (B:fofType), ((forall (Xx:fofType), ((iff ((in Xx) A)) ((in Xx) B)))->(((eq fofType) A) B))) % FOF formula (<kernel.Constant object at 0x1dfee60>, <kernel.Single object at 0x1dfec68>) of role type named emptyset_type % Using role type % Declaring emptyset:fofType % FOF formula (<kernel.Constant object at 0x1dfebd8>, <kernel.Sort object at 0x1cc8998>) of role type named emptysetAx_type % Using role type % Declaring emptysetAx:Prop % FOF formula (((eq Prop) emptysetAx) (forall (Xx:fofType), (((in Xx) emptyset)->False))) of role definition named emptysetAx % A new definition: (((eq Prop) emptysetAx) (forall (Xx:fofType), (((in Xx) emptyset)->False))) % Defined: emptysetAx:=(forall (Xx:fofType), (((in Xx) emptyset)->False)) % FOF formula (<kernel.Constant object at 0x1dfec68>, <kernel.DependentProduct object at 0x1cc4ef0>) of role type named setadjoin_type % Using role type % Declaring setadjoin:(fofType->(fofType->fofType)) % FOF formula (<kernel.Constant object at 0x2091680>, <kernel.Sort object at 0x1cc8998>) of role type named setadjoinAx_type % Using role type % Declaring setadjoinAx:Prop % FOF formula (((eq Prop) setadjoinAx) (forall (Xx:fofType) (A:fofType) (Xy:fofType), ((iff ((in Xy) ((setadjoin Xx) A))) ((or (((eq fofType) Xy) Xx)) ((in Xy) A))))) of role definition named setadjoinAx % A new definition: (((eq Prop) setadjoinAx) (forall (Xx:fofType) (A:fofType) (Xy:fofType), ((iff ((in Xy) ((setadjoin Xx) A))) ((or (((eq fofType) Xy) Xx)) ((in Xy) A))))) % Defined: setadjoinAx:=(forall (Xx:fofType) (A:fofType) (Xy:fofType), ((iff ((in Xy) ((setadjoin Xx) A))) ((or (((eq fofType) Xy) Xx)) ((in Xy) A)))) % FOF formula (<kernel.Constant object at 0x2091f38>, <kernel.DependentProduct object at 0x2238e60>) of role type named powerset_type % Using role type % Declaring powerset:(fofType->fofType) % FOF formula (<kernel.Constant object at 0x1cc4ef0>, <kernel.Sort object at 0x1cc8998>) of role type named powersetAx_type % Using role type % Declaring powersetAx:Prop % FOF formula (((eq Prop) powersetAx) (forall (A:fofType) (B:fofType), ((iff ((in B) (powerset A))) (forall (Xx:fofType), (((in Xx) B)->((in Xx) A)))))) of role definition named powersetAx % A new definition: (((eq Prop) powersetAx) (forall (A:fofType) (B:fofType), ((iff ((in B) (powerset A))) (forall (Xx:fofType), (((in Xx) B)->((in Xx) A)))))) % Defined: powersetAx:=(forall (A:fofType) (B:fofType), ((iff ((in B) (powerset A))) (forall (Xx:fofType), (((in Xx) B)->((in Xx) A))))) % FOF formula (<kernel.Constant object at 0x1cc4ef0>, <kernel.DependentProduct object at 0x21db128>) of role type named setunion_type % Using role type % Declaring setunion:(fofType->fofType) % FOF formula (<kernel.Constant object at 0x1cc4f80>, <kernel.Sort object at 0x1cc8998>) of role type named setunionAx_type % Using role type % Declaring setunionAx:Prop % FOF formula (((eq Prop) setunionAx) (forall (A:fofType) (Xx:fofType), ((iff ((in Xx) (setunion A))) ((ex fofType) (fun (B:fofType)=> ((and ((in Xx) B)) ((in B) A))))))) of role definition named setunionAx % A new definition: (((eq Prop) setunionAx) (forall (A:fofType) (Xx:fofType), ((iff ((in Xx) (setunion A))) ((ex fofType) (fun (B:fofType)=> ((and ((in Xx) B)) ((in B) A))))))) % Defined: setunionAx:=(forall (A:fofType) (Xx:fofType), ((iff ((in Xx) (setunion A))) ((ex fofType) (fun (B:fofType)=> ((and ((in Xx) B)) ((in B) A)))))) % FOF formula (<kernel.Constant object at 0x21db440>, <kernel.Single object at 0x21dba28>) of role type named omega_type % Using role type % Declaring omega:fofType % FOF formula (<kernel.Constant object at 0x21dbc20>, <kernel.Sort object at 0x1cc8998>) of role type named omega0Ax_type % Using role type % Declaring omega0Ax:Prop % FOF formula (((eq Prop) omega0Ax) ((in emptyset) omega)) of role definition named omega0Ax % A new definition: (((eq Prop) omega0Ax) ((in emptyset) omega)) % Defined: omega0Ax:=((in emptyset) omega) % FOF formula (<kernel.Constant object at 0x21db830>, <kernel.Sort object at 0x1cc8998>) of role type named omegaSAx_type % Using role type % Declaring omegaSAx:Prop % FOF formula (((eq Prop) omegaSAx) (forall (Xx:fofType), (((in Xx) omega)->((in ((setadjoin Xx) Xx)) omega)))) of role definition named omegaSAx % A new definition: (((eq Prop) omegaSAx) (forall (Xx:fofType), (((in Xx) omega)->((in ((setadjoin Xx) Xx)) omega)))) % Defined: omegaSAx:=(forall (Xx:fofType), (((in Xx) omega)->((in ((setadjoin Xx) Xx)) omega))) % FOF formula (<kernel.Constant object at 0x21db830>, <kernel.Sort object at 0x1cc8998>) of role type named omegaIndAx_type % Using role type % Declaring omegaIndAx:Prop % FOF formula (((eq Prop) omegaIndAx) (forall (A:fofType), (((and ((in emptyset) A)) (forall (Xx:fofType), (((and ((in Xx) omega)) ((in Xx) A))->((in ((setadjoin Xx) Xx)) A))))->(forall (Xx:fofType), (((in Xx) omega)->((in Xx) A)))))) of role definition named omegaIndAx % A new definition: (((eq Prop) omegaIndAx) (forall (A:fofType), (((and ((in emptyset) A)) (forall (Xx:fofType), (((and ((in Xx) omega)) ((in Xx) A))->((in ((setadjoin Xx) Xx)) A))))->(forall (Xx:fofType), (((in Xx) omega)->((in Xx) A)))))) % Defined: omegaIndAx:=(forall (A:fofType), (((and ((in emptyset) A)) (forall (Xx:fofType), (((and ((in Xx) omega)) ((in Xx) A))->((in ((setadjoin Xx) Xx)) A))))->(forall (Xx:fofType), (((in Xx) omega)->((in Xx) A))))) % FOF formula (<kernel.Constant object at 0x21db440>, <kernel.Sort object at 0x1cc8998>) of role type named replAx_type % Using role type % Declaring replAx:Prop % FOF formula (((eq Prop) replAx) (forall (Xphi:(fofType->(fofType->Prop))) (A:fofType), ((forall (Xx:fofType), (((in Xx) A)->(exu (fun (Xy:fofType)=> ((Xphi Xx) Xy)))))->((ex fofType) (fun (B:fofType)=> (forall (Xx:fofType), ((iff ((in Xx) B)) ((ex fofType) (fun (Xy:fofType)=> ((and ((in Xy) A)) ((Xphi Xy) Xx))))))))))) of role definition named replAx % A new definition: (((eq Prop) replAx) (forall (Xphi:(fofType->(fofType->Prop))) (A:fofType), ((forall (Xx:fofType), (((in Xx) A)->(exu (fun (Xy:fofType)=> ((Xphi Xx) Xy)))))->((ex fofType) (fun (B:fofType)=> (forall (Xx:fofType), ((iff ((in Xx) B)) ((ex fofType) (fun (Xy:fofType)=> ((and ((in Xy) A)) ((Xphi Xy) Xx))))))))))) % Defined: replAx:=(forall (Xphi:(fofType->(fofType->Prop))) (A:fofType), ((forall (Xx:fofType), (((in Xx) A)->(exu (fun (Xy:fofType)=> ((Xphi Xx) Xy)))))->((ex fofType) (fun (B:fofType)=> (forall (Xx:fofType), ((iff ((in Xx) B)) ((ex fofType) (fun (Xy:fofType)=> ((and ((in Xy) A)) ((Xphi Xy) Xx)))))))))) % FOF formula (<kernel.Constant object at 0x22389e0>, <kernel.Sort object at 0x1cc8998>) of role type named foundationAx_type % Using role type % Declaring foundationAx:Prop % FOF formula (((eq Prop) foundationAx) (forall (A:fofType), (((ex fofType) (fun (Xx:fofType)=> ((in Xx) A)))->((ex fofType) (fun (B:fofType)=> ((and ((in B) A)) (((ex fofType) (fun (Xx:fofType)=> ((and ((in Xx) B)) ((in Xx) A))))->False))))))) of role definition named foundationAx % A new definition: (((eq Prop) foundationAx) (forall (A:fofType), (((ex fofType) (fun (Xx:fofType)=> ((in Xx) A)))->((ex fofType) (fun (B:fofType)=> ((and ((in B) A)) (((ex fofType) (fun (Xx:fofType)=> ((and ((in Xx) B)) ((in Xx) A))))->False))))))) % Defined: foundationAx:=(forall (A:fofType), (((ex fofType) (fun (Xx:fofType)=> ((in Xx) A)))->((ex fofType) (fun (B:fofType)=> ((and ((in B) A)) (((ex fofType) (fun (Xx:fofType)=> ((and ((in Xx) B)) ((in Xx) A))))->False)))))) % FOF formula (<kernel.Constant object at 0x22389e0>, <kernel.Sort object at 0x1cc8998>) of role type named wellorderingAx_type % Using role type % Declaring wellorderingAx:Prop % FOF formula (((eq Prop) wellorderingAx) (forall (A:fofType), ((ex fofType) (fun (B:fofType)=> ((and ((and ((and (forall (C:fofType), (((in C) B)->(forall (Xx:fofType), (((in Xx) C)->((in Xx) A)))))) (forall (Xx:fofType) (Xy:fofType), (((and ((in Xx) A)) ((in Xy) A))->((forall (C:fofType), (((in C) B)->((iff ((in Xx) C)) ((in Xy) C))))->(((eq fofType) Xx) Xy)))))) (forall (C:fofType) (D:fofType), (((and ((in C) B)) ((in D) B))->((or (forall (Xx:fofType), (((in Xx) C)->((in Xx) D)))) (forall (Xx:fofType), (((in Xx) D)->((in Xx) C)))))))) (forall (C:fofType), (((and (forall (Xx:fofType), (((in Xx) C)->((in Xx) A)))) ((ex fofType) (fun (Xx:fofType)=> ((in Xx) C))))->((ex fofType) (fun (D:fofType)=> ((ex fofType) (fun (Xx:fofType)=> ((and ((and ((and ((in D) B)) ((in Xx) C))) (((ex fofType) (fun (Xy:fofType)=> ((and ((in Xy) D)) ((in Xy) C))))->False))) (forall (E:fofType), (((in E) B)->((or (forall (Xy:fofType), (((in Xy) E)->((in Xy) D)))) ((in Xx) E)))))))))))))))) of role definition named wellorderingAx % A new definition: (((eq Prop) wellorderingAx) (forall (A:fofType), ((ex fofType) (fun (B:fofType)=> ((and ((and ((and (forall (C:fofType), (((in C) B)->(forall (Xx:fofType), (((in Xx) C)->((in Xx) A)))))) (forall (Xx:fofType) (Xy:fofType), (((and ((in Xx) A)) ((in Xy) A))->((forall (C:fofType), (((in C) B)->((iff ((in Xx) C)) ((in Xy) C))))->(((eq fofType) Xx) Xy)))))) (forall (C:fofType) (D:fofType), (((and ((in C) B)) ((in D) B))->((or (forall (Xx:fofType), (((in Xx) C)->((in Xx) D)))) (forall (Xx:fofType), (((in Xx) D)->((in Xx) C)))))))) (forall (C:fofType), (((and (forall (Xx:fofType), (((in Xx) C)->((in Xx) A)))) ((ex fofType) (fun (Xx:fofType)=> ((in Xx) C))))->((ex fofType) (fun (D:fofType)=> ((ex fofType) (fun (Xx:fofType)=> ((and ((and ((and ((in D) B)) ((in Xx) C))) (((ex fofType) (fun (Xy:fofType)=> ((and ((in Xy) D)) ((in Xy) C))))->False))) (forall (E:fofType), (((in E) B)->((or (forall (Xy:fofType), (((in Xy) E)->((in Xy) D)))) ((in Xx) E)))))))))))))))) % Defined: wellorderingAx:=(forall (A:fofType), ((ex fofType) (fun (B:fofType)=> ((and ((and ((and (forall (C:fofType), (((in C) B)->(forall (Xx:fofType), (((in Xx) C)->((in Xx) A)))))) (forall (Xx:fofType) (Xy:fofType), (((and ((in Xx) A)) ((in Xy) A))->((forall (C:fofType), (((in C) B)->((iff ((in Xx) C)) ((in Xy) C))))->(((eq fofType) Xx) Xy)))))) (forall (C:fofType) (D:fofType), (((and ((in C) B)) ((in D) B))->((or (forall (Xx:fofType), (((in Xx) C)->((in Xx) D)))) (forall (Xx:fofType), (((in Xx) D)->((in Xx) C)))))))) (forall (C:fofType), (((and (forall (Xx:fofType), (((in Xx) C)->((in Xx) A)))) ((ex fofType) (fun (Xx:fofType)=> ((in Xx) C))))->((ex fofType) (fun (D:fofType)=> ((ex fofType) (fun (Xx:fofType)=> ((and ((and ((and ((in D) B)) ((in Xx) C))) (((ex fofType) (fun (Xy:fofType)=> ((and ((in Xy) D)) ((in Xy) C))))->False))) (forall (E:fofType), (((in E) B)->((or (forall (Xy:fofType), (((in Xy) E)->((in Xy) D)))) ((in Xx) E))))))))))))))) % FOF formula (<kernel.Constant object at 0x22389e0>, <kernel.DependentProduct object at 0x21d9cb0>) of role type named descr_type % Using role type % Declaring descr:((fofType->Prop)->fofType) % FOF formula (<kernel.Constant object at 0x2238ea8>, <kernel.Sort object at 0x1cc8998>) of role type named descrp_type % Using role type % Declaring descrp:Prop % FOF formula (((eq Prop) descrp) (forall (Xphi:(fofType->Prop)), ((exu (fun (Xx:fofType)=> (Xphi Xx)))->(Xphi (descr (fun (Xx:fofType)=> (Xphi Xx))))))) of role definition named descrp % A new definition: (((eq Prop) descrp) (forall (Xphi:(fofType->Prop)), ((exu (fun (Xx:fofType)=> (Xphi Xx)))->(Xphi (descr (fun (Xx:fofType)=> (Xphi Xx))))))) % Defined: descrp:=(forall (Xphi:(fofType->Prop)), ((exu (fun (Xx:fofType)=> (Xphi Xx)))->(Xphi (descr (fun (Xx:fofType)=> (Xphi Xx)))))) % FOF formula (<kernel.Constant object at 0x22389e0>, <kernel.DependentProduct object at 0x21d9710>) of role type named dsetconstr_type % Using role type % Declaring dsetconstr:(fofType->((fofType->Prop)->fofType)) % FOF formula (<kernel.Constant object at 0x22363b0>, <kernel.Sort object at 0x1cc8998>) of role type named dsetconstrI_type % Using role type % Declaring dsetconstrI:Prop % FOF formula (((eq Prop) dsetconstrI) (forall (A:fofType) (Xphi:(fofType->Prop)) (Xx:fofType), (((in Xx) A)->((Xphi Xx)->((in Xx) ((dsetconstr A) (fun (Xy:fofType)=> (Xphi Xy)))))))) of role definition named dsetconstrI % A new definition: (((eq Prop) dsetconstrI) (forall (A:fofType) (Xphi:(fofType->Prop)) (Xx:fofType), (((in Xx) A)->((Xphi Xx)->((in Xx) ((dsetconstr A) (fun (Xy:fofType)=> (Xphi Xy)))))))) % Defined: dsetconstrI:=(forall (A:fofType) (Xphi:(fofType->Prop)) (Xx:fofType), (((in Xx) A)->((Xphi Xx)->((in Xx) ((dsetconstr A) (fun (Xy:fofType)=> (Xphi Xy))))))) % FOF formula (<kernel.Constant object at 0x22363b0>, <kernel.Sort object at 0x1cc8998>) of role type named dsetconstrEL_type % Using role type % Declaring dsetconstrEL:Prop % FOF formula (((eq Prop) dsetconstrEL) (forall (A:fofType) (Xphi:(fofType->Prop)) (Xx:fofType), (((in Xx) ((dsetconstr A) (fun (Xy:fofType)=> (Xphi Xy))))->((in Xx) A)))) of role definition named dsetconstrEL % A new definition: (((eq Prop) dsetconstrEL) (forall (A:fofType) (Xphi:(fofType->Prop)) (Xx:fofType), (((in Xx) ((dsetconstr A) (fun (Xy:fofType)=> (Xphi Xy))))->((in Xx) A)))) % Defined: dsetconstrEL:=(forall (A:fofType) (Xphi:(fofType->Prop)) (Xx:fofType), (((in Xx) ((dsetconstr A) (fun (Xy:fofType)=> (Xphi Xy))))->((in Xx) A))) % FOF formula (<kernel.Constant object at 0x2236680>, <kernel.Sort object at 0x1cc8998>) of role type named dsetconstrER_type % Using role type % Declaring dsetconstrER:Prop % FOF formula (((eq Prop) dsetconstrER) (forall (A:fofType) (Xphi:(fofType->Prop)) (Xx:fofType), (((in Xx) ((dsetconstr A) (fun (Xy:fofType)=> (Xphi Xy))))->(Xphi Xx)))) of role definition named dsetconstrER % A new definition: (((eq Prop) dsetconstrER) (forall (A:fofType) (Xphi:(fofType->Prop)) (Xx:fofType), (((in Xx) ((dsetconstr A) (fun (Xy:fofType)=> (Xphi Xy))))->(Xphi Xx)))) % Defined: dsetconstrER:=(forall (A:fofType) (Xphi:(fofType->Prop)) (Xx:fofType), (((in Xx) ((dsetconstr A) (fun (Xy:fofType)=> (Xphi Xy))))->(Xphi Xx))) % FOF formula (<kernel.Constant object at 0x21d9050>, <kernel.Sort object at 0x1cc8998>) of role type named exuE1_type % Using role type % Declaring exuE1:Prop % FOF formula (((eq Prop) exuE1) (forall (Xphi:(fofType->Prop)), ((exu (fun (Xx:fofType)=> (Xphi Xx)))->((ex fofType) (fun (Xx:fofType)=> ((and (Xphi Xx)) (forall (Xy:fofType), ((Xphi Xy)->(((eq fofType) Xx) Xy))))))))) of role definition named exuE1 % A new definition: (((eq Prop) exuE1) (forall (Xphi:(fofType->Prop)), ((exu (fun (Xx:fofType)=> (Xphi Xx)))->((ex fofType) (fun (Xx:fofType)=> ((and (Xphi Xx)) (forall (Xy:fofType), ((Xphi Xy)->(((eq fofType) Xx) Xy))))))))) % Defined: exuE1:=(forall (Xphi:(fofType->Prop)), ((exu (fun (Xx:fofType)=> (Xphi Xx)))->((ex fofType) (fun (Xx:fofType)=> ((and (Xphi Xx)) (forall (Xy:fofType), ((Xphi Xy)->(((eq fofType) Xx) Xy)))))))) % FOF formula (<kernel.Constant object at 0x21d9b90>, <kernel.DependentProduct object at 0x21d95f0>) of role type named prop2set_type % Using role type % Declaring prop2set:(Prop->fofType) % FOF formula (((eq (Prop->fofType)) prop2set) (fun (Xphi:Prop)=> ((dsetconstr (powerset emptyset)) (fun (Xx:fofType)=> Xphi)))) of role definition named prop2set % A new definition: (((eq (Prop->fofType)) prop2set) (fun (Xphi:Prop)=> ((dsetconstr (powerset emptyset)) (fun (Xx:fofType)=> Xphi)))) % Defined: prop2set:=(fun (Xphi:Prop)=> ((dsetconstr (powerset emptyset)) (fun (Xx:fofType)=> Xphi))) % FOF formula (<kernel.Constant object at 0x21d95f0>, <kernel.Sort object at 0x1cc8998>) of role type named prop2setE_type % Using role type % Declaring prop2setE:Prop % FOF formula (((eq Prop) prop2setE) (forall (Xphi:Prop) (Xx:fofType), (((in Xx) (prop2set Xphi))->Xphi))) of role definition named prop2setE % A new definition: (((eq Prop) prop2setE) (forall (Xphi:Prop) (Xx:fofType), (((in Xx) (prop2set Xphi))->Xphi))) % Defined: prop2setE:=(forall (Xphi:Prop) (Xx:fofType), (((in Xx) (prop2set Xphi))->Xphi)) % FOF formula (<kernel.Constant object at 0x21d9878>, <kernel.Sort object at 0x1cc8998>) of role type named emptysetE_type % Using role type % Declaring emptysetE:Prop % FOF formula (((eq Prop) emptysetE) (forall (Xx:fofType), (((in Xx) emptyset)->(forall (Xphi:Prop), Xphi)))) of role definition named emptysetE % A new definition: (((eq Prop) emptysetE) (forall (Xx:fofType), (((in Xx) emptyset)->(forall (Xphi:Prop), Xphi)))) % Defined: emptysetE:=(forall (Xx:fofType), (((in Xx) emptyset)->(forall (Xphi:Prop), Xphi))) % FOF formula (<kernel.Constant object at 0x21d9f38>, <kernel.Sort object at 0x1cc8998>) of role type named emptysetimpfalse_type % Using role type % Declaring emptysetimpfalse:Prop % FOF formula (((eq Prop) emptysetimpfalse) (forall (Xx:fofType), (((in Xx) emptyset)->False))) of role definition named emptysetimpfalse % A new definition: (((eq Prop) emptysetimpfalse) (forall (Xx:fofType), (((in Xx) emptyset)->False))) % Defined: emptysetimpfalse:=(forall (Xx:fofType), (((in Xx) emptyset)->False)) % FOF formula (<kernel.Constant object at 0x21d9998>, <kernel.Sort object at 0x1cc8998>) of role type named notinemptyset_type % Using role type % Declaring notinemptyset:Prop % FOF formula (((eq Prop) notinemptyset) (forall (Xx:fofType), (((in Xx) emptyset)->False))) of role definition named notinemptyset % A new definition: (((eq Prop) notinemptyset) (forall (Xx:fofType), (((in Xx) emptyset)->False))) % Defined: notinemptyset:=(forall (Xx:fofType), (((in Xx) emptyset)->False)) % FOF formula (<kernel.Constant object at 0x21d9170>, <kernel.Sort object at 0x1cc8998>) of role type named exuE3e_type % Using role type % Declaring exuE3e:Prop % FOF formula (((eq Prop) exuE3e) (forall (Xphi:(fofType->Prop)), ((exu (fun (Xx:fofType)=> (Xphi Xx)))->((ex fofType) (fun (Xx:fofType)=> (Xphi Xx)))))) of role definition named exuE3e % A new definition: (((eq Prop) exuE3e) (forall (Xphi:(fofType->Prop)), ((exu (fun (Xx:fofType)=> (Xphi Xx)))->((ex fofType) (fun (Xx:fofType)=> (Xphi Xx)))))) % Defined: exuE3e:=(forall (Xphi:(fofType->Prop)), ((exu (fun (Xx:fofType)=> (Xphi Xx)))->((ex fofType) (fun (Xx:fofType)=> (Xphi Xx))))) % FOF formula (<kernel.Constant object at 0x21d9638>, <kernel.Sort object at 0x1cc8998>) of role type named setext_type % Using role type % Declaring setext:Prop % FOF formula (((eq Prop) setext) (forall (A:fofType) (B:fofType), ((forall (Xx:fofType), (((in Xx) A)->((in Xx) B)))->((forall (Xx:fofType), (((in Xx) B)->((in Xx) A)))->(((eq fofType) A) B))))) of role definition named setext % A new definition: (((eq Prop) setext) (forall (A:fofType) (B:fofType), ((forall (Xx:fofType), (((in Xx) A)->((in Xx) B)))->((forall (Xx:fofType), (((in Xx) B)->((in Xx) A)))->(((eq fofType) A) B))))) % Defined: setext:=(forall (A:fofType) (B:fofType), ((forall (Xx:fofType), (((in Xx) A)->((in Xx) B)))->((forall (Xx:fofType), (((in Xx) B)->((in Xx) A)))->(((eq fofType) A) B)))) % FOF formula (<kernel.Constant object at 0x21d99e0>, <kernel.Sort object at 0x1cc8998>) of role type named emptyI_type % Using role type % Declaring emptyI:Prop % FOF formula (((eq Prop) emptyI) (forall (A:fofType), ((forall (Xx:fofType), (((in Xx) A)->False))->(((eq fofType) A) emptyset)))) of role definition named emptyI % A new definition: (((eq Prop) emptyI) (forall (A:fofType), ((forall (Xx:fofType), (((in Xx) A)->False))->(((eq fofType) A) emptyset)))) % Defined: emptyI:=(forall (A:fofType), ((forall (Xx:fofType), (((in Xx) A)->False))->(((eq fofType) A) emptyset))) % FOF formula (<kernel.Constant object at 0x21d9fc8>, <kernel.Sort object at 0x1cc8998>) of role type named noeltsimpempty_type % Using role type % Declaring noeltsimpempty:Prop % FOF formula (((eq Prop) noeltsimpempty) (forall (A:fofType), ((forall (Xx:fofType), (((in Xx) A)->False))->(((eq fofType) A) emptyset)))) of role definition named noeltsimpempty % A new definition: (((eq Prop) noeltsimpempty) (forall (A:fofType), ((forall (Xx:fofType), (((in Xx) A)->False))->(((eq fofType) A) emptyset)))) % Defined: noeltsimpempty:=(forall (A:fofType), ((forall (Xx:fofType), (((in Xx) A)->False))->(((eq fofType) A) emptyset))) % FOF formula (<kernel.Constant object at 0x21d9710>, <kernel.Sort object at 0x1cc8998>) of role type named setbeta_type % Using role type % Declaring setbeta:Prop % FOF formula (((eq Prop) setbeta) (forall (A:fofType) (Xphi:(fofType->Prop)) (Xx:fofType), (((in Xx) A)->((iff ((in Xx) ((dsetconstr A) (fun (Xy:fofType)=> (Xphi Xy))))) (Xphi Xx))))) of role definition named setbeta % A new definition: (((eq Prop) setbeta) (forall (A:fofType) (Xphi:(fofType->Prop)) (Xx:fofType), (((in Xx) A)->((iff ((in Xx) ((dsetconstr A) (fun (Xy:fofType)=> (Xphi Xy))))) (Xphi Xx))))) % Defined: setbeta:=(forall (A:fofType) (Xphi:(fofType->Prop)) (Xx:fofType), (((in Xx) A)->((iff ((in Xx) ((dsetconstr A) (fun (Xy:fofType)=> (Xphi Xy))))) (Xphi Xx)))) % FOF formula (<kernel.Constant object at 0x21d9050>, <kernel.DependentProduct object at 0x21d9758>) of role type named nonempty_type % Using role type % Declaring nonempty:(fofType->Prop) % FOF formula (((eq (fofType->Prop)) nonempty) (fun (Xx:fofType)=> (not (((eq fofType) Xx) emptyset)))) of role definition named nonempty % A new definition: (((eq (fofType->Prop)) nonempty) (fun (Xx:fofType)=> (not (((eq fofType) Xx) emptyset)))) % Defined: nonempty:=(fun (Xx:fofType)=> (not (((eq fofType) Xx) emptyset))) % FOF formula (<kernel.Constant object at 0x21d9758>, <kernel.Sort object at 0x1cc8998>) of role type named nonemptyE1_type % Using role type % Declaring nonemptyE1:Prop % FOF formula (((eq Prop) nonemptyE1) (forall (A:fofType), ((nonempty A)->((ex fofType) (fun (Xx:fofType)=> ((in Xx) A)))))) of role definition named nonemptyE1 % A new definition: (((eq Prop) nonemptyE1) (forall (A:fofType), ((nonempty A)->((ex fofType) (fun (Xx:fofType)=> ((in Xx) A)))))) % Defined: nonemptyE1:=(forall (A:fofType), ((nonempty A)->((ex fofType) (fun (Xx:fofType)=> ((in Xx) A))))) % FOF formula (<kernel.Constant object at 0x21d97a0>, <kernel.Sort object at 0x1cc8998>) of role type named nonemptyI_type % Using role type % Declaring nonemptyI:Prop % FOF formula (((eq Prop) nonemptyI) (forall (A:fofType) (Xphi:(fofType->Prop)) (Xx:fofType), (((in Xx) A)->((Xphi Xx)->(nonempty ((dsetconstr A) (fun (Xy:fofType)=> (Xphi Xy)))))))) of role definition named nonemptyI % A new definition: (((eq Prop) nonemptyI) (forall (A:fofType) (Xphi:(fofType->Prop)) (Xx:fofType), (((in Xx) A)->((Xphi Xx)->(nonempty ((dsetconstr A) (fun (Xy:fofType)=> (Xphi Xy)))))))) % Defined: nonemptyI:=(forall (A:fofType) (Xphi:(fofType->Prop)) (Xx:fofType), (((in Xx) A)->((Xphi Xx)->(nonempty ((dsetconstr A) (fun (Xy:fofType)=> (Xphi Xy))))))) % FOF formula (<kernel.Constant object at 0x21dacb0>, <kernel.Sort object at 0x1cc8998>) of role type named nonemptyI1_type % Using role type % Declaring nonemptyI1:Prop % FOF formula (((eq Prop) nonemptyI1) (forall (A:fofType), (((ex fofType) (fun (Xx:fofType)=> ((in Xx) A)))->(nonempty A)))) of role definition named nonemptyI1 % A new definition: (((eq Prop) nonemptyI1) (forall (A:fofType), (((ex fofType) (fun (Xx:fofType)=> ((in Xx) A)))->(nonempty A)))) % Defined: nonemptyI1:=(forall (A:fofType), (((ex fofType) (fun (Xx:fofType)=> ((in Xx) A)))->(nonempty A))) % FOF formula (<kernel.Constant object at 0x21da998>, <kernel.Sort object at 0x1cc8998>) of role type named setadjoinIL_type % Using role type % Declaring setadjoinIL:Prop % FOF formula (((eq Prop) setadjoinIL) (forall (Xx:fofType) (Xy:fofType), ((in Xx) ((setadjoin Xx) Xy)))) of role definition named setadjoinIL % A new definition: (((eq Prop) setadjoinIL) (forall (Xx:fofType) (Xy:fofType), ((in Xx) ((setadjoin Xx) Xy)))) % Defined: setadjoinIL:=(forall (Xx:fofType) (Xy:fofType), ((in Xx) ((setadjoin Xx) Xy))) % FOF formula (<kernel.Constant object at 0x21da998>, <kernel.Sort object at 0x1cc8998>) of role type named emptyinunitempty_type % Using role type % Declaring emptyinunitempty:Prop % FOF formula (((eq Prop) emptyinunitempty) ((in emptyset) ((setadjoin emptyset) emptyset))) of role definition named emptyinunitempty % A new definition: (((eq Prop) emptyinunitempty) ((in emptyset) ((setadjoin emptyset) emptyset))) % Defined: emptyinunitempty:=((in emptyset) ((setadjoin emptyset) emptyset)) % FOF formula (<kernel.Constant object at 0x21da908>, <kernel.Sort object at 0x1cc8998>) of role type named setadjoinIR_type % Using role type % Declaring setadjoinIR:Prop % FOF formula (((eq Prop) setadjoinIR) (forall (Xx:fofType) (A:fofType) (Xy:fofType), (((in Xy) A)->((in Xy) ((setadjoin Xx) A))))) of role definition named setadjoinIR % A new definition: (((eq Prop) setadjoinIR) (forall (Xx:fofType) (A:fofType) (Xy:fofType), (((in Xy) A)->((in Xy) ((setadjoin Xx) A))))) % Defined: setadjoinIR:=(forall (Xx:fofType) (A:fofType) (Xy:fofType), (((in Xy) A)->((in Xy) ((setadjoin Xx) A)))) % FOF formula (<kernel.Constant object at 0x21d9758>, <kernel.Sort object at 0x1cc8998>) of role type named setadjoinE_type % Using role type % Declaring setadjoinE:Prop % FOF formula (((eq Prop) setadjoinE) (forall (Xx:fofType) (A:fofType) (Xy:fofType), (((in Xy) ((setadjoin Xx) A))->(forall (Xphi:Prop), (((((eq fofType) Xy) Xx)->Xphi)->((((in Xy) A)->Xphi)->Xphi)))))) of role definition named setadjoinE % A new definition: (((eq Prop) setadjoinE) (forall (Xx:fofType) (A:fofType) (Xy:fofType), (((in Xy) ((setadjoin Xx) A))->(forall (Xphi:Prop), (((((eq fofType) Xy) Xx)->Xphi)->((((in Xy) A)->Xphi)->Xphi)))))) % Defined: setadjoinE:=(forall (Xx:fofType) (A:fofType) (Xy:fofType), (((in Xy) ((setadjoin Xx) A))->(forall (Xphi:Prop), (((((eq fofType) Xy) Xx)->Xphi)->((((in Xy) A)->Xphi)->Xphi))))) % FOF formula (<kernel.Constant object at 0x21d9b48>, <kernel.Sort object at 0x1cc8998>) of role type named setadjoinOr_type % Using role type % Declaring setadjoinOr:Prop % FOF formula (((eq Prop) setadjoinOr) (forall (Xx:fofType) (A:fofType) (Xy:fofType), (((in Xy) ((setadjoin Xx) A))->((or (((eq fofType) Xy) Xx)) ((in Xy) A))))) of role definition named setadjoinOr % A new definition: (((eq Prop) setadjoinOr) (forall (Xx:fofType) (A:fofType) (Xy:fofType), (((in Xy) ((setadjoin Xx) A))->((or (((eq fofType) Xy) Xx)) ((in Xy) A))))) % Defined: setadjoinOr:=(forall (Xx:fofType) (A:fofType) (Xy:fofType), (((in Xy) ((setadjoin Xx) A))->((or (((eq fofType) Xy) Xx)) ((in Xy) A)))) % FOF formula (<kernel.Constant object at 0x21d93f8>, <kernel.Sort object at 0x1cc8998>) of role type named setoftrueEq_type % Using role type % Declaring setoftrueEq:Prop % FOF formula (((eq Prop) setoftrueEq) (forall (A:fofType), (((eq fofType) ((dsetconstr A) (fun (Xx:fofType)=> True))) A))) of role definition named setoftrueEq % A new definition: (((eq Prop) setoftrueEq) (forall (A:fofType), (((eq fofType) ((dsetconstr A) (fun (Xx:fofType)=> True))) A))) % Defined: setoftrueEq:=(forall (A:fofType), (((eq fofType) ((dsetconstr A) (fun (Xx:fofType)=> True))) A)) % FOF formula (<kernel.Constant object at 0x21d95a8>, <kernel.Sort object at 0x1cc8998>) of role type named powersetI_type % Using role type % Declaring powersetI:Prop % FOF formula (((eq Prop) powersetI) (forall (A:fofType) (B:fofType), ((forall (Xx:fofType), (((in Xx) B)->((in Xx) A)))->((in B) (powerset A))))) of role definition named powersetI % A new definition: (((eq Prop) powersetI) (forall (A:fofType) (B:fofType), ((forall (Xx:fofType), (((in Xx) B)->((in Xx) A)))->((in B) (powerset A))))) % Defined: powersetI:=(forall (A:fofType) (B:fofType), ((forall (Xx:fofType), (((in Xx) B)->((in Xx) A)))->((in B) (powerset A)))) % FOF formula (<kernel.Constant object at 0x21d9950>, <kernel.Sort object at 0x1cc8998>) of role type named emptyinPowerset_type % Using role type % Declaring emptyinPowerset:Prop % FOF formula (((eq Prop) emptyinPowerset) (forall (A:fofType), ((in emptyset) (powerset A)))) of role definition named emptyinPowerset % A new definition: (((eq Prop) emptyinPowerset) (forall (A:fofType), ((in emptyset) (powerset A)))) % Defined: emptyinPowerset:=(forall (A:fofType), ((in emptyset) (powerset A))) % FOF formula (setextAx->(emptysetAx->(setadjoinAx->(powersetAx->(setunionAx->(omega0Ax->(omegaSAx->(omegaIndAx->(replAx->(foundationAx->(wellorderingAx->(descrp->(dsetconstrI->(dsetconstrEL->(dsetconstrER->(exuE1->(prop2setE->(emptysetE->(emptysetimpfalse->(notinemptyset->(exuE3e->(setext->(emptyI->(noeltsimpempty->(setbeta->(nonemptyE1->(nonemptyI->(nonemptyI1->(setadjoinIL->(emptyinunitempty->(setadjoinIR->(setadjoinE->(setadjoinOr->(setoftrueEq->(powersetI->(emptyinPowerset->(forall (A:fofType), ((in emptyset) (powerset A))))))))))))))))))))))))))))))))))))))) of role conjecture named emptyInPowerset % Conjecture to prove = (setextAx->(emptysetAx->(setadjoinAx->(powersetAx->(setunionAx->(omega0Ax->(omegaSAx->(omegaIndAx->(replAx->(foundationAx->(wellorderingAx->(descrp->(dsetconstrI->(dsetconstrEL->(dsetconstrER->(exuE1->(prop2setE->(emptysetE->(emptysetimpfalse->(notinemptyset->(exuE3e->(setext->(emptyI->(noeltsimpempty->(setbeta->(nonemptyE1->(nonemptyI->(nonemptyI1->(setadjoinIL->(emptyinunitempty->(setadjoinIR->(setadjoinE->(setadjoinOr->(setoftrueEq->(powersetI->(emptyinPowerset->(forall (A:fofType), ((in emptyset) (powerset A))))))))))))))))))))))))))))))))))))))):Prop % We need to prove ['(setextAx->(emptysetAx->(setadjoinAx->(powersetAx->(setunionAx->(omega0Ax->(omegaSAx->(omegaIndAx->(replAx->(foundationAx->(wellorderingAx->(descrp->(dsetconstrI->(dsetconstrEL->(dsetconstrER->(exuE1->(prop2setE->(emptysetE->(emptysetimpfalse->(notinemptyset->(exuE3e->(setext->(emptyI->(noeltsimpempty->(setbeta->(nonemptyE1->(nonemptyI->(nonemptyI1->(setadjoinIL->(emptyinunitempty->(setadjoinIR->(setadjoinE->(setadjoinOr->(setoftrueEq->(powersetI->(emptyinPowerset->(forall (A:fofType), ((in emptyset) (powerset A)))))))))))))))))))))))))))))))))))))))'] % Parameter fofType:Type. % Parameter in:(fofType->(fofType->Prop)). % Definition exu:=(fun (Xphi:(fofType->Prop))=> ((ex fofType) (fun (Xx:fofType)=> ((and (Xphi Xx)) (forall (Xy:fofType), ((Xphi Xy)->(((eq fofType) Xx) Xy))))))):((fofType->Prop)->Prop). % Definition setextAx:=(forall (A:fofType) (B:fofType), ((forall (Xx:fofType), ((iff ((in Xx) A)) ((in Xx) B)))->(((eq fofType) A) B))):Prop. % Parameter emptyset:fofType. % Definition emptysetAx:=(forall (Xx:fofType), (((in Xx) emptyset)->False)):Prop. % Parameter setadjoin:(fofType->(fofType->fofType)). % Definition setadjoinAx:=(forall (Xx:fofType) (A:fofType) (Xy:fofType), ((iff ((in Xy) ((setadjoin Xx) A))) ((or (((eq fofType) Xy) Xx)) ((in Xy) A)))):Prop. % Parameter powerset:(fofType->fofType). % Definition powersetAx:=(forall (A:fofType) (B:fofType), ((iff ((in B) (powerset A))) (forall (Xx:fofType), (((in Xx) B)->((in Xx) A))))):Prop. % Parameter setunion:(fofType->fofType). % Definition setunionAx:=(forall (A:fofType) (Xx:fofType), ((iff ((in Xx) (setunion A))) ((ex fofType) (fun (B:fofType)=> ((and ((in Xx) B)) ((in B) A)))))):Prop. % Parameter omega:fofType. % Definition omega0Ax:=((in emptyset) omega):Prop. % Definition omegaSAx:=(forall (Xx:fofType), (((in Xx) omega)->((in ((setadjoin Xx) Xx)) omega))):Prop. % Definition omegaIndAx:=(forall (A:fofType), (((and ((in emptyset) A)) (forall (Xx:fofType), (((and ((in Xx) omega)) ((in Xx) A))->((in ((setadjoin Xx) Xx)) A))))->(forall (Xx:fofType), (((in Xx) omega)->((in Xx) A))))):Prop. % Definition replAx:=(forall (Xphi:(fofType->(fofType->Prop))) (A:fofType), ((forall (Xx:fofType), (((in Xx) A)->(exu (fun (Xy:fofType)=> ((Xphi Xx) Xy)))))->((ex fofType) (fun (B:fofType)=> (forall (Xx:fofType), ((iff ((in Xx) B)) ((ex fofType) (fun (Xy:fofType)=> ((and ((in Xy) A)) ((Xphi Xy) Xx)))))))))):Prop. % Definition foundationAx:=(forall (A:fofType), (((ex fofType) (fun (Xx:fofType)=> ((in Xx) A)))->((ex fofType) (fun (B:fofType)=> ((and ((in B) A)) (((ex fofType) (fun (Xx:fofType)=> ((and ((in Xx) B)) ((in Xx) A))))->False)))))):Prop. % Definition wellorderingAx:=(forall (A:fofType), ((ex fofType) (fun (B:fofType)=> ((and ((and ((and (forall (C:fofType), (((in C) B)->(forall (Xx:fofType), (((in Xx) C)->((in Xx) A)))))) (forall (Xx:fofType) (Xy:fofType), (((and ((in Xx) A)) ((in Xy) A))->((forall (C:fofType), (((in C) B)->((iff ((in Xx) C)) ((in Xy) C))))->(((eq fofType) Xx) Xy)))))) (forall (C:fofType) (D:fofType), (((and ((in C) B)) ((in D) B))->((or (forall (Xx:fofType), (((in Xx) C)->((in Xx) D)))) (forall (Xx:fofType), (((in Xx) D)->((in Xx) C)))))))) (forall (C:fofType), (((and (forall (Xx:fofType), (((in Xx) C)->((in Xx) A)))) ((ex fofType) (fun (Xx:fofType)=> ((in Xx) C))))->((ex fofType) (fun (D:fofType)=> ((ex fofType) (fun (Xx:fofType)=> ((and ((and ((and ((in D) B)) ((in Xx) C))) (((ex fofType) (fun (Xy:fofType)=> ((and ((in Xy) D)) ((in Xy) C))))->False))) (forall (E:fofType), (((in E) B)->((or (forall (Xy:fofType), (((in Xy) E)->((in Xy) D)))) ((in Xx) E))))))))))))))):Prop. % Parameter descr:((fofType->Prop)->fofType). % Definition descrp:=(forall (Xphi:(fofType->Prop)), ((exu (fun (Xx:fofType)=> (Xphi Xx)))->(Xphi (descr (fun (Xx:fofType)=> (Xphi Xx)))))):Prop. % Parameter dsetconstr:(fofType->((fofType->Prop)->fofType)). % Definition dsetconstrI:=(forall (A:fofType) (Xphi:(fofType->Prop)) (Xx:fofType), (((in Xx) A)->((Xphi Xx)->((in Xx) ((dsetconstr A) (fun (Xy:fofType)=> (Xphi Xy))))))):Prop. % Definition dsetconstrEL:=(forall (A:fofType) (Xphi:(fofType->Prop)) (Xx:fofType), (((in Xx) ((dsetconstr A) (fun (Xy:fofType)=> (Xphi Xy))))->((in Xx) A))):Prop. % Definition dsetconstrER:=(forall (A:fofType) (Xphi:(fofType->Prop)) (Xx:fofType), (((in Xx) ((dsetconstr A) (fun (Xy:fofType)=> (Xphi Xy))))->(Xphi Xx))):Prop. % Definition exuE1:=(forall (Xphi:(fofType->Prop)), ((exu (fun (Xx:fofType)=> (Xphi Xx)))->((ex fofType) (fun (Xx:fofType)=> ((and (Xphi Xx)) (forall (Xy:fofType), ((Xphi Xy)->(((eq fofType) Xx) Xy)))))))):Prop. % Definition prop2set:=(fun (Xphi:Prop)=> ((dsetconstr (powerset emptyset)) (fun (Xx:fofType)=> Xphi))):(Prop->fofType). % Definition prop2setE:=(forall (Xphi:Prop) (Xx:fofType), (((in Xx) (prop2set Xphi))->Xphi)):Prop. % Definition emptysetE:=(forall (Xx:fofType), (((in Xx) emptyset)->(forall (Xphi:Prop), Xphi))):Prop. % Definition emptysetimpfalse:=(forall (Xx:fofType), (((in Xx) emptyset)->False)):Prop. % Definition notinemptyset:=(forall (Xx:fofType), (((in Xx) emptyset)->False)):Prop. % Definition exuE3e:=(forall (Xphi:(fofType->Prop)), ((exu (fun (Xx:fofType)=> (Xphi Xx)))->((ex fofType) (fun (Xx:fofType)=> (Xphi Xx))))):Prop. % Definition setext:=(forall (A:fofType) (B:fofType), ((forall (Xx:fofType), (((in Xx) A)->((in Xx) B)))->((forall (Xx:fofType), (((in Xx) B)->((in Xx) A)))->(((eq fofType) A) B)))):Prop. % Definition emptyI:=(forall (A:fofType), ((forall (Xx:fofType), (((in Xx) A)->False))->(((eq fofType) A) emptyset))):Prop. % Definition noeltsimpempty:=(forall (A:fofType), ((forall (Xx:fofType), (((in Xx) A)->False))->(((eq fofType) A) emptyset))):Prop. % Definition setbeta:=(forall (A:fofType) (Xphi:(fofType->Prop)) (Xx:fofType), (((in Xx) A)->((iff ((in Xx) ((dsetconstr A) (fun (Xy:fofType)=> (Xphi Xy))))) (Xphi Xx)))):Prop. % Definition nonempty:=(fun (Xx:fofType)=> (not (((eq fofType) Xx) emptyset))):(fofType->Prop). % Definition nonemptyE1:=(forall (A:fofType), ((nonempty A)->((ex fofType) (fun (Xx:fofType)=> ((in Xx) A))))):Prop. % Definition nonemptyI:=(forall (A:fofType) (Xphi:(fofType->Prop)) (Xx:fofType), (((in Xx) A)->((Xphi Xx)->(nonempty ((dsetconstr A) (fun (Xy:fofType)=> (Xphi Xy))))))):Prop. % Definition nonemptyI1:=(forall (A:fofType), (((ex fofType) (fun (Xx:fofType)=> ((in Xx) A)))->(nonempty A))):Prop. % Definition setadjoinIL:=(forall (Xx:fofType) (Xy:fofType), ((in Xx) ((setadjoin Xx) Xy))):Prop. % Definition emptyinunitempty:=((in emptyset) ((setadjoin emptyset) emptyset)):Prop. % Definition setadjoinIR:=(forall (Xx:fofType) (A:fofType) (Xy:fofType), (((in Xy) A)->((in Xy) ((setadjoin Xx) A)))):Prop. % Definition setadjoinE:=(forall (Xx:fofType) (A:fofType) (Xy:fofType), (((in Xy) ((setadjoin Xx) A))->(forall (Xphi:Prop), (((((eq fofType) Xy) Xx)->Xphi)->((((in Xy) A)->Xphi)->Xphi))))):Prop. % Definition setadjoinOr:=(forall (Xx:fofType) (A:fofType) (Xy:fofType), (((in Xy) ((setadjoin Xx) A))->((or (((eq fofType) Xy) Xx)) ((in Xy) A)))):Prop. % Definition setoftrueEq:=(forall (A:fofType), (((eq fofType) ((dsetconstr A) (fun (Xx:fofType)=> True))) A)):Prop. % Definition powersetI:=(forall (A:fofType) (B:fofType), ((forall (Xx:fofType), (((in Xx) B)->((in Xx) A)))->((in B) (powerset A)))):Prop. % Definition emptyinPowerset:=(forall (A:fofType), ((in emptyset) (powerset A))):Prop. % Trying to prove (setextAx->(emptysetAx->(setadjoinAx->(powersetAx->(setunionAx->(omega0Ax->(omegaSAx->(omegaIndAx->(replAx->(foundationAx->(wellorderingAx->(descrp->(dsetconstrI->(dsetconstrEL->(dsetconstrER->(exuE1->(prop2setE->(emptysetE->(emptysetimpfalse->(notinemptyset->(exuE3e->(setext->(emptyI->(noeltsimpempty->(setbeta->(nonemptyE1->(nonemptyI->(nonemptyI1->(setadjoinIL->(emptyinunitempty->(setadjoinIR->(setadjoinE->(setadjoinOr->(setoftrueEq->(powersetI->(emptyinPowerset->(forall (A:fofType), ((in emptyset) (powerset A))))))))))))))))))))))))))))))))))))))) % Found x4:omega0Ax % Instantiate: Xx:=emptyset:fofType % Found x4 as proof of ((in Xx) omega) % Found x34:emptyinPowerset % Found (fun (x34:emptyinPowerset)=> x34) as proof of (forall (A:fofType), ((in emptyset) (powerset A))) % Found (fun (x33:powersetI) (x34:emptyinPowerset)=> x34) as proof of (emptyinPowerset->(forall (A:fofType), ((in emptyset) (powerset A)))) % Found (fun (x32:setoftrueEq) (x33:powersetI) (x34:emptyinPowerset)=> x34) as proof of (powersetI->(emptyinPowerset->(forall (A:fofType), ((in emptyset) (powerset A))))) % Found (fun (x31:setadjoinOr) (x32:setoftrueEq) (x33:powersetI) (x34:emptyinPowerset)=> x34) as proof of (setoftrueEq->(powersetI->(emptyinPowerset->(forall (A:fofType), ((in emptyset) (powerset A)))))) % Found (fun (x30:setadjoinE) (x31:setadjoinOr) (x32:setoftrueEq) (x33:powersetI) (x34:emptyinPowerset)=> x34) as proof of (setadjoinOr->(setoftrueEq->(powersetI->(emptyinPowerset->(forall (A:fofType), ((in emptyset) (powerset A))))))) % Found (fun (x29:setadjoinIR) (x30:setadjoinE) (x31:setadjoinOr) (x32:setoftrueEq) (x33:powersetI) (x34:emptyinPowerset)=> x34) as proof of (setadjoinE->(setadjoinOr->(setoftrueEq->(powersetI->(emptyinPowerset->(forall (A:fofType), ((in emptyset) (powerset A)))))))) % Found (fun (x28:emptyinunitempty) (x29:setadjoinIR) (x30:setadjoinE) (x31:setadjoinOr) (x32:setoftrueEq) (x33:powersetI) (x34:emptyinPowerset)=> x34) as proof of (setadjoinIR->(setadjoinE->(setadjoinOr->(setoftrueEq->(powersetI->(emptyinPowerset->(forall (A:fofType), ((in emptyset) (powerset A))))))))) % Found (fun (x27:setadjoinIL) (x28:emptyinunitempty) (x29:setadjoinIR) (x30:setadjoinE) (x31:setadjoinOr) (x32:setoftrueEq) (x33:powersetI) (x34:emptyinPowerset)=> x34) as proof of (emptyinunitempty->(setadjoinIR->(setadjoinE->(setadjoinOr->(setoftrueEq->(powersetI->(emptyinPowerset->(forall (A:fofType), ((in emptyset) (powerset A)))))))))) % Found (fun (x26:nonemptyI1) (x27:setadjoinIL) (x28:emptyinunitempty) (x29:setadjoinIR) (x30:setadjoinE) (x31:setadjoinOr) (x32:setoftrueEq) (x33:powersetI) (x34:emptyinPowerset)=> x34) as proof of (setadjoinIL->(emptyinunitempty->(setadjoinIR->(setadjoinE->(setadjoinOr->(setoftrueEq->(powersetI->(emptyinPowerset->(forall (A:fofType), ((in emptyset) (powerset A))))))))))) % Found (fun (x25:nonemptyI) (x26:nonemptyI1) (x27:setadjoinIL) (x28:emptyinunitempty) (x29:setadjoinIR) (x30:setadjoinE) (x31:setadjoinOr) (x32:setoftrueEq) (x33:powersetI) (x34:emptyinPowerset)=> x34) as proof of (nonemptyI1->(setadjoinIL->(emptyinunitempty->(setadjoinIR->(setadjoinE->(setadjoinOr->(setoftrueEq->(powersetI->(emptyinPowerset->(forall (A:fofType), ((in emptyset) (powerset A)))))))))))) % Found (fun (x24:nonemptyE1) (x25:nonemptyI) (x26:nonemptyI1) (x27:setadjoinIL) (x28:emptyinunitempty) (x29:setadjoinIR) (x30:setadjoinE) (x31:setadjoinOr) (x32:setoftrueEq) (x33:powersetI) (x34:emptyinPowerset)=> x34) as proof of (nonemptyI->(nonemptyI1->(setadjoinIL->(emptyinunitempty->(setadjoinIR->(setadjoinE->(setadjoinOr->(setoftrueEq->(powersetI->(emptyinPowerset->(forall (A:fofType), ((in emptyset) (powerset A))))))))))))) % Found (fun (x23:setbeta) (x24:nonemptyE1) (x25:nonemptyI) (x26:nonemptyI1) (x27:setadjoinIL) (x28:emptyinunitempty) (x29:setadjoinIR) (x30:setadjoinE) (x31:setadjoinOr) (x32:setoftrueEq) (x33:powersetI) (x34:emptyinPowerset)=> x34) as proof of (nonemptyE1->(nonemptyI->(nonemptyI1->(setadjoinIL->(emptyinunitempty->(setadjoinIR->(setadjoinE->(setadjoinOr->(setoftrueEq->(powersetI->(emptyinPowerset->(forall (A:fofType), ((in emptyset) (powerset A)))))))))))))) % Found (fun (x22:noeltsimpempty) (x23:setbeta) (x24:nonemptyE1) (x25:nonemptyI) (x26:nonemptyI1) (x27:setadjoinIL) (x28:emptyinunitempty) (x29:setadjoinIR) (x30:setadjoinE) (x31:setadjoinOr) (x32:setoftrueEq) (x33:powersetI) (x34:emptyinPowerset)=> x34) as proof of (setbeta->(nonemptyE1->(nonemptyI->(nonemptyI1->(setadjoinIL->(emptyinunitempty->(setadjoinIR->(setadjoinE->(setadjoinOr->(setoftrueEq->(powersetI->(emptyinPowerset->(forall (A:fofType), ((in emptyset) (powerset A))))))))))))))) % Found (fun (x21:emptyI) (x22:noeltsimpempty) (x23:setbeta) (x24:nonemptyE1) (x25:nonemptyI) (x26:nonemptyI1) (x27:setadjoinIL) (x28:emptyinunitempty) (x29:setadjoinIR) (x30:setadjoinE) (x31:setadjoinOr) (x32:setoftrueEq) (x33:powersetI) (x34:emptyinPowerset)=> x34) as proof of (noeltsimpempty->(setbeta->(nonemptyE1->(nonemptyI->(nonemptyI1->(setadjoinIL->(emptyinunitempty->(setadjoinIR->(setadjoinE->(setadjoinOr->(setoftrueEq->(powersetI->(emptyinPowerset->(forall (A:fofType), ((in emptyset) (powerset A)))))))))))))))) % Found (fun (x20:setext) (x21:emptyI) (x22:noeltsimpempty) (x23:setbeta) (x24:nonemptyE1) (x25:nonemptyI) (x26:nonemptyI1) (x27:setadjoinIL) (x28:emptyinunitempty) (x29:setadjoinIR) (x30:setadjoinE) (x31:setadjoinOr) (x32:setoftrueEq) (x33:powersetI) (x34:emptyinPowerset)=> x34) as proof of (emptyI->(noeltsimpempty->(setbeta->(nonemptyE1->(nonemptyI->(nonemptyI1->(setadjoinIL->(emptyinunitempty->(setadjoinIR->(setadjoinE->(setadjoinOr->(setoftrueEq->(powersetI->(emptyinPowerset->(forall (A:fofType), ((in emptyset) (powerset A))))))))))))))))) % Found (fun (x19:exuE3e) (x20:setext) (x21:emptyI) (x22:noeltsimpempty) (x23:setbeta) (x24:nonemptyE1) (x25:nonemptyI) (x26:nonemptyI1) (x27:setadjoinIL) (x28:emptyinunitempty) (x29:setadjoinIR) (x30:setadjoinE) (x31:setadjoinOr) (x32:setoftrueEq) (x33:powersetI) (x34:emptyinPowerset)=> x34) as proof of (setext->(emptyI->(noeltsimpempty->(setbeta->(nonemptyE1->(nonemptyI->(nonemptyI1->(setadjoinIL->(emptyinunitempty->(setadjoinIR->(setadjoinE->(setadjoinOr->(setoftrueEq->(powersetI->(emptyinPowerset->(forall (A:fofType), ((in emptyset) (powerset A)))))))))))))))))) % Found (fun (x18:notinemptyset) (x19:exuE3e) (x20:setext) (x21:emptyI) (x22:noeltsimpempty) (x23:setbeta) (x24:nonemptyE1) (x25:nonemptyI) (x26:nonemptyI1) (x27:setadjoinIL) (x28:emptyinunitempty) (x29:setadjoinIR) (x30:setadjoinE) (x31:setadjoinOr) (x32:setoftrueEq) (x33:powersetI) (x34:emptyinPowerset)=> x34) as proof of (exuE3e->(setext->(emptyI->(noeltsimpempty->(setbeta->(nonemptyE1->(nonemptyI->(nonemptyI1->(setadjoinIL->(emptyinunitempty->(setadjoinIR->(setadjoinE->(setadjoinOr->(setoftrueEq->(powersetI->(emptyinPowerset->(forall (A:fofType), ((in emptyset) (powerset A))))))))))))))))))) % Found (fun (x17:emptysetimpfalse) (x18:notinemptyset) (x19:exuE3e) (x20:setext) (x21:emptyI) (x22:noeltsimpempty) (x23:setbeta) (x24:nonemptyE1) (x25:nonemptyI) (x26:nonemptyI1) (x27:setadjoinIL) (x28:emptyinunitempty) (x29:setadjoinIR) (x30:setadjoinE) (x31:setadjoinOr) (x32:setoftrueEq) (x33:powersetI) (x34:emptyinPowerset)=> x34) as proof of (notinemptyset->(exuE3e->(setext->(emptyI->(noeltsimpempty->(setbeta->(nonemptyE1->(nonemptyI->(nonemptyI1->(setadjoinIL->(emptyinunitempty->(setadjoinIR->(setadjoinE->(setadjoinOr->(setoftrueEq->(powersetI->(emptyinPowerset->(forall (A:fofType), ((in emptyset) (powerset A)))))))))))))))))))) % Found (fun (x16:emptysetE) (x17:emptysetimpfalse) (x18:notinemptyset) (x19:exuE3e) (x20:setext) (x21:emptyI) (x22:noeltsimpempty) (x23:setbeta) (x24:nonemptyE1) (x25:nonemptyI) (x26:nonemptyI1) (x27:setadjoinIL) (x28:emptyinunitempty) (x29:setadjoinIR) (x30:setadjoinE) (x31:setadjoinOr) (x32:setoftrueEq) (x33:powersetI) (x34:emptyinPowerset)=> x34) as proof of (emptysetimpfalse->(notinemptyset->(exuE3e->(setext->(emptyI->(noeltsimpempty->(setbeta->(nonemptyE1->(nonemptyI->(nonemptyI1->(setadjoinIL->(emptyinunitempty->(setadjoinIR->(setadjoinE->(setadjoinOr->(setoftrueEq->(powersetI->(emptyinPowerset->(forall (A:fofType), ((in emptyset) (powerset A))))))))))))))))))))) % Found (fun (x15:prop2setE) (x16:emptysetE) (x17:emptysetimpfalse) (x18:notinemptyset) (x19:exuE3e) (x20:setext) (x21:emptyI) (x22:noeltsimpempty) (x23:setbeta) (x24:nonemptyE1) (x25:nonemptyI) (x26:nonemptyI1) (x27:setadjoinIL) (x28:emptyinunitempty) (x29:setadjoinIR) (x30:setadjoinE) (x31:setadjoinOr) (x32:setoftrueEq) (x33:powersetI) (x34:emptyinPowerset)=> x34) as proof of (emptysetE->(emptysetimpfalse->(notinemptyset->(exuE3e->(setext->(emptyI->(noeltsimpempty->(setbeta->(nonemptyE1->(nonemptyI->(nonemptyI1->(setadjoinIL->(emptyinunitempty->(setadjoinIR->(setadjoinE->(setadjoinOr->(setoftrueEq->(powersetI->(emptyinPowerset->(forall (A:fofType), ((in emptyset) (powerset A)))))))))))))))))))))) % Found (fun (x14:exuE1) (x15:prop2setE) (x16:emptysetE) (x17:emptysetimpfalse) (x18:notinemptyset) (x19:exuE3e) (x20:setext) (x21:emptyI) (x22:noeltsimpempty) (x23:setbeta) (x24:nonemptyE1) (x25:nonemptyI) (x26:nonemptyI1) (x27:setadjoinIL) (x28:emptyinunitempty) (x29:setadjoinIR) (x30:setadjoinE) (x31:setadjoinOr) (x32:setoftrueEq) (x33:powersetI) (x34:emptyinPowerset)=> x34) as proof of (prop2setE->(emptysetE->(emptysetimpfalse->(notinemptyset->(exuE3e->(setext->(emptyI->(noeltsimpempty->(setbeta->(nonemptyE1->(nonemptyI->(nonemptyI1->(setadjoinIL->(emptyinunitempty->(setadjoinIR->(setadjoinE->(setadjoinOr->(setoftrueEq->(powersetI->(emptyinPowerset->(forall (A:fofType), ((in emptyset) (powerset A))))))))))))))))))))))) % Found (fun (x13:dsetconstrER) (x14:exuE1) (x15:prop2setE) (x16:emptysetE) (x17:emptysetimpfalse) (x18:notinemptyset) (x19:exuE3e) (x20:setext) (x21:emptyI) (x22:noeltsimpempty) (x23:setbeta) (x24:nonemptyE1) (x25:nonemptyI) (x26:nonemptyI1) (x27:setadjoinIL) (x28:emptyinunitempty) (x29:setadjoinIR) (x30:setadjoinE) (x31:setadjoinOr) (x32:setoftrueEq) (x33:powersetI) (x34:emptyinPowerset)=> x34) as proof of (exuE1->(prop2setE->(emptysetE->(emptysetimpfalse->(notinemptyset->(exuE3e->(setext->(emptyI->(noeltsimpempty->(setbeta->(nonemptyE1->(nonemptyI->(nonemptyI1->(setadjoinIL->(emptyinunitempty->(setadjoinIR->(setadjoinE->(setadjoinOr->(setoftrueEq->(powersetI->(emptyinPowerset->(forall (A:fofType), ((in emptyset) (powerset A)))))))))))))))))))))))) % Found (fun (x12:dsetconstrEL) (x13:dsetconstrER) (x14:exuE1) (x15:prop2setE) (x16:emptysetE) (x17:emptysetimpfalse) (x18:notinemptyset) (x19:exuE3e) (x20:setext) (x21:emptyI) (x22:noeltsimpempty) (x23:setbeta) (x24:nonemptyE1) (x25:nonemptyI) (x26:nonemptyI1) (x27:setadjoinIL) (x28:emptyinunitempty) (x29:setadjoinIR) (x30:setadjoinE) (x31:setadjoinOr) (x32:setoftrueEq) (x33:powersetI) (x34:emptyinPowerset)=> x34) as proof of (dsetconstrER->(exuE1->(prop2setE->(emptysetE->(emptysetimpfalse->(notinemptyset->(exuE3e->(setext->(emptyI->(noeltsimpempty->(setbeta->(nonemptyE1->(nonemptyI->(nonemptyI1->(setadjoinIL->(emptyinunitempty->(setadjoinIR->(setadjoinE->(setadjoinOr->(setoftrueEq->(powersetI->(emptyinPowerset->(forall (A:fofType), ((in emptyset) (powerset A))))))))))))))))))))))))) % Found (fun (x11:dsetconstrI) (x12:dsetconstrEL) (x13:dsetconstrER) (x14:exuE1) (x15:prop2setE) (x16:emptysetE) (x17:emptysetimpfalse) (x18:notinemptyset) (x19:exuE3e) (x20:setext) (x21:emptyI) (x22:noeltsimpempty) (x23:setbeta) (x24:nonemptyE1) (x25:nonemptyI) (x26:nonemptyI1) (x27:setadjoinIL) (x28:emptyinunitempty) (x29:setadjoinIR) (x30:setadjoinE) (x31:setadjoinOr) (x32:setoftrueEq) (x33:powersetI) (x34:emptyinPowerset)=> x34) as proof of (dsetconstrEL->(dsetconstrER->(exuE1->(prop2setE->(emptysetE->(emptysetimpfalse->(notinemptyset->(exuE3e->(setext->(emptyI->(noeltsimpempty->(setbeta->(nonemptyE1->(nonemptyI->(nonemptyI1->(setadjoinIL->(emptyinunitempty->(setadjoinIR->(setadjoinE->(setadjoinOr->(setoftrueEq->(powersetI->(emptyinPowerset->(forall (A:fofType), ((in emptyset) (powerset A)))))))))))))))))))))))))) % Found (fun (x10:descrp) (x11:dsetconstrI) (x12:dsetconstrEL) (x13:dsetconstrER) (x14:exuE1) (x15:prop2setE) (x16:emptysetE) (x17:emptysetimpfalse) (x18:notinemptyset) (x19:exuE3e) (x20:setext) (x21:emptyI) (x22:noeltsimpempty) (x23:setbeta) (x24:nonemptyE1) (x25:nonemptyI) (x26:nonemptyI1) (x27:setadjoinIL) (x28:emptyinunitempty) (x29:setadjoinIR) (x30:setadjoinE) (x31:setadjoinOr) (x32:setoftrueEq) (x33:powersetI) (x34:emptyinPowerset)=> x34) as proof of (dsetconstrI->(dsetconstrEL->(dsetconstrER->(exuE1->(prop2setE->(emptysetE->(emptysetimpfalse->(notinemptyset->(exuE3e->(setext->(emptyI->(noeltsimpempty->(setbeta->(nonemptyE1->(nonemptyI->(nonemptyI1->(setadjoinIL->(emptyinunitempty->(setadjoinIR->(setadjoinE->(setadjoinOr->(setoftrueEq->(powersetI->(emptyinPowerset->(forall (A:fofType), ((in emptyset) (powerset A))))))))))))))))))))))))))) % Found (fun (x9:wellorderingAx) (x10:descrp) (x11:dsetconstrI) (x12:dsetconstrEL) (x13:dsetconstrER) (x14:exuE1) (x15:prop2setE) (x16:emptysetE) (x17:emptysetimpfalse) (x18:notinemptyset) (x19:exuE3e) (x20:setext) (x21:emptyI) (x22:noeltsimpempty) (x23:setbeta) (x24:nonemptyE1) (x25:nonemptyI) (x26:nonemptyI1) (x27:setadjoinIL) (x28:emptyinunitempty) (x29:setadjoinIR) (x30:setadjoinE) (x31:setadjoinOr) (x32:setoftrueEq) (x33:powersetI) (x34:emptyinPowerset)=> x34) as proof of (descrp->(dsetconstrI->(dsetconstrEL->(dsetconstrER->(exuE1->(prop2setE->(emptysetE->(emptysetimpfalse->(notinemptyset->(exuE3e->(setext->(emptyI->(noeltsimpempty->(setbeta->(nonemptyE1->(nonemptyI->(nonemptyI1->(setadjoinIL->(emptyinunitempty->(setadjoinIR->(setadjoinE->(setadjoinOr->(setoftrueEq->(powersetI->(emptyinPowerset->(forall (A:fofType), ((in emptyset) (powerset A)))))))))))))))))))))))))))) % Found (fun (x8:foundationAx) (x9:wellorderingAx) (x10:descrp) (x11:dsetconstrI) (x12:dsetconstrEL) (x13:dsetconstrER) (x14:exuE1) (x15:prop2setE) (x16:emptysetE) (x17:emptysetimpfalse) (x18:notinemptyset) (x19:exuE3e) (x20:setext) (x21:emptyI) (x22:noeltsimpempty) (x23:setbeta) (x24:nonemptyE1) (x25:nonemptyI) (x26:nonemptyI1) (x27:setadjoinIL) (x28:emptyinunitempty) (x29:setadjoinIR) (x30:setadjoinE) (x31:setadjoinOr) (x32:setoftrueEq) (x33:powersetI) (x34:emptyinPowerset)=> x34) as proof of (wellorderingAx->(descrp->(dsetconstrI->(dsetconstrEL->(dsetconstrER->(exuE1->(prop2setE->(emptysetE->(emptysetimpfalse->(notinemptyset->(exuE3e->(setext->(emptyI->(noeltsimpempty->(setbeta->(nonemptyE1->(nonemptyI->(nonemptyI1->(setadjoinIL->(emptyinunitempty->(setadjoinIR->(setadjoinE->(setadjoinOr->(setoftrueEq->(powersetI->(emptyinPowerset->(forall (A:fofType), ((in emptyset) (powerset A))))))))))))))))))))))))))))) % Found (fun (x7:replAx) (x8:foundationAx) (x9:wellorderingAx) (x10:descrp) (x11:dsetconstrI) (x12:dsetconstrEL) (x13:dsetconstrER) (x14:exuE1) (x15:prop2setE) (x16:emptysetE) (x17:emptysetimpfalse) (x18:notinemptyset) (x19:exuE3e) (x20:setext) (x21:emptyI) (x22:noeltsimpempty) (x23:setbeta) (x24:nonemptyE1) (x25:nonemptyI) (x26:nonemptyI1) (x27:setadjoinIL) (x28:emptyinunitempty) (x29:setadjoinIR) (x30:setadjoinE) (x31:setadjoinOr) (x32:setoftrueEq) (x33:powersetI) (x34:emptyinPowerset)=> x34) as proof of (foundationAx->(wellorderingAx->(descrp->(dsetconstrI->(dsetconstrEL->(dsetconstrER->(exuE1->(prop2setE->(emptysetE->(emptysetimpfalse->(notinemptyset->(exuE3e->(setext->(emptyI->(noeltsimpempty->(setbeta->(nonemptyE1->(nonemptyI->(nonemptyI1->(setadjoinIL->(emptyinunitempty->(setadjoinIR->(setadjoinE->(setadjoinOr->(setoftrueEq->(powersetI->(emptyinPowerset->(forall (A:fofType), ((in emptyset) (powerset A)))))))))))))))))))))))))))))) % Found (fun (x6:omegaIndAx) (x7:replAx) (x8:foundationAx) (x9:wellorderingAx) (x10:descrp) (x11:dsetconstrI) (x12:dsetconstrEL) (x13:dsetconstrER) (x14:exuE1) (x15:prop2setE) (x16:emptysetE) (x17:emptysetimpfalse) (x18:notinemptyset) (x19:exuE3e) (x20:setext) (x21:emptyI) (x22:noeltsimpempty) (x23:setbeta) (x24:nonemptyE1) (x25:nonemptyI) (x26:nonemptyI1) (x27:setadjoinIL) (x28:emptyinunitempty) (x29:setadjoinIR) (x30:setadjoinE) (x31:setadjoinOr) (x32:setoftrueEq) (x33:powersetI) (x34:emptyinPowerset)=> x34) as proof of (replAx->(foundationAx->(wellorderingAx->(descrp->(dsetconstrI->(dsetconstrEL->(dsetconstrER->(exuE1->(prop2setE->(emptysetE->(emptysetimpfalse->(notinemptyset->(exuE3e->(setext->(emptyI->(noeltsimpempty->(setbeta->(nonemptyE1->(nonemptyI->(nonemptyI1->(setadjoinIL->(emptyinunitempty->(setadjoinIR->(setadjoinE->(setadjoinOr->(setoftrueEq->(powersetI->(emptyinPowerset->(forall (A:fofType), ((in emptyset) (powerset A))))))))))))))))))))))))))))))) % Found (fun (x5:omegaSAx) (x6:omegaIndAx) (x7:replAx) (x8:foundationAx) (x9:wellorderingAx) (x10:descrp) (x11:dsetconstrI) (x12:dsetconstrEL) (x13:dsetconstrER) (x14:exuE1) (x15:prop2setE) (x16:emptysetE) (x17:emptysetimpfalse) (x18:notinemptyset) (x19:exuE3e) (x20:setext) (x21:emptyI) (x22:noeltsimpempty) (x23:setbeta) (x24:nonemptyE1) (x25:nonemptyI) (x26:nonemptyI1) (x27:setadjoinIL) (x28:emptyinunitempty) (x29:setadjoinIR) (x30:setadjoinE) (x31:setadjoinOr) (x32:setoftrueEq) (x33:powersetI) (x34:emptyinPowerset)=> x34) as proof of (omegaIndAx->(replAx->(foundationAx->(wellorderingAx->(descrp->(dsetconstrI->(dsetconstrEL->(dsetconstrER->(exuE1->(prop2setE->(emptysetE->(emptysetimpfalse->(notinemptyset->(exuE3e->(setext->(emptyI->(noeltsimpempty->(setbeta->(nonemptyE1->(nonemptyI->(nonemptyI1->(setadjoinIL->(emptyinunitempty->(setadjoinIR->(setadjoinE->(setadjoinOr->(setoftrueEq->(powersetI->(emptyinPowerset->(forall (A:fofType), ((in emptyset) (powerset A)))))))))))))))))))))))))))))))) % Found (fun (x4:omega0Ax) (x5:omegaSAx) (x6:omegaIndAx) (x7:replAx) (x8:foundationAx) (x9:wellorderingAx) (x10:descrp) (x11:dsetconstrI) (x12:dsetconstrEL) (x13:dsetconstrER) (x14:exuE1) (x15:prop2setE) (x16:emptysetE) (x17:emptysetimpfalse) (x18:notinemptyset) (x19:exuE3e) (x20:setext) (x21:emptyI) (x22:noeltsimpempty) (x23:setbeta) (x24:nonemptyE1) (x25:nonemptyI) (x26:nonemptyI1) (x27:setadjoinIL) (x28:emptyinunitempty) (x29:setadjoinIR) (x30:setadjoinE) (x31:setadjoinOr) (x32:setoftrueEq) (x33:powersetI) (x34:emptyinPowerset)=> x34) as proof of (omegaSAx->(omegaIndAx->(replAx->(foundationAx->(wellorderingAx->(descrp->(dsetconstrI->(dsetconstrEL->(dsetconstrER->(exuE1->(prop2setE->(emptysetE->(emptysetimpfalse->(notinemptyset->(exuE3e->(setext->(emptyI->(noeltsimpempty->(setbeta->(nonemptyE1->(nonemptyI->(nonemptyI1->(setadjoinIL->(emptyinunitempty->(setadjoinIR->(setadjoinE->(setadjoinOr->(setoftrueEq->(powersetI->(emptyinPowerset->(forall (A:fofType), ((in emptyset) (powerset A))))))))))))))))))))))))))))))))) % Found (fun (x3:setunionAx) (x4:omega0Ax) (x5:omegaSAx) (x6:omegaIndAx) (x7:replAx) (x8:foundationAx) (x9:wellorderingAx) (x10:descrp) (x11:dsetconstrI) (x12:dsetconstrEL) (x13:dsetconstrER) (x14:exuE1) (x15:prop2setE) (x16:emptysetE) (x17:emptysetimpfalse) (x18:notinemptyset) (x19:exuE3e) (x20:setext) (x21:emptyI) (x22:noeltsimpempty) (x23:setbeta) (x24:nonemptyE1) (x25:nonemptyI) (x26:nonemptyI1) (x27:setadjoinIL) (x28:emptyinunitempty) (x29:setadjoinIR) (x30:setadjoinE) (x31:setadjoinOr) (x32:setoftrueEq) (x33:powersetI) (x34:emptyinPowerset)=> x34) as proof of (omega0Ax->(omegaSAx->(omegaIndAx->(replAx->(foundationAx->(wellorderingAx->(descrp->(dsetconstrI->(dsetconstrEL->(dsetconstrER->(exuE1->(prop2setE->(emptysetE->(emptysetimpfalse->(notinemptyset->(exuE3e->(setext->(emptyI->(noeltsimpempty->(setbeta->(nonemptyE1->(nonemptyI->(nonemptyI1->(setadjoinIL->(emptyinunitempty->(setadjoinIR->(setadjoinE->(setadjoinOr->(setoftrueEq->(powersetI->(emptyinPowerset->(forall (A:fofType), ((in emptyset) (powerset A)))))))))))))))))))))))))))))))))) % Found (fun (x2:powersetAx) (x3:setunionAx) (x4:omega0Ax) (x5:omegaSAx) (x6:omegaIndAx) (x7:replAx) (x8:foundationAx) (x9:wellorderingAx) (x10:descrp) (x11:dsetconstrI) (x12:dsetconstrEL) (x13:dsetconstrER) (x14:exuE1) (x15:prop2setE) (x16:emptysetE) (x17:emptysetimpfalse) (x18:notinemptyset) (x19:exuE3e) (x20:setext) (x21:emptyI) (x22:noeltsimpempty) (x23:setbeta) (x24:nonemptyE1) (x25:nonemptyI) (x26:nonemptyI1) (x27:setadjoinIL) (x28:emptyinunitempty) (x29:setadjoinIR) (x30:setadjoinE) (x31:setadjoinOr) (x32:setoftrueEq) (x33:powersetI) (x34:emptyinPowerset)=> x34) as proof of (setunionAx->(omega0Ax->(omegaSAx->(omegaIndAx->(replAx->(foundationAx->(wellorderingAx->(descrp->(dsetconstrI->(dsetconstrEL->(dsetconstrER->(exuE1->(prop2setE->(emptysetE->(emptysetimpfalse->(notinemptyset->(exuE3e->(setext->(emptyI->(noeltsimpempty->(setbeta->(nonemptyE1->(nonemptyI->(nonemptyI1->(setadjoinIL->(emptyinunitempty->(setadjoinIR->(setadjoinE->(setadjoinOr->(setoftrueEq->(powersetI->(emptyinPowerset->(forall (A:fofType), ((in emptyset) (powerset A))))))))))))))))))))))))))))))))))) % Found (fun (x1:setadjoinAx) (x2:powersetAx) (x3:setunionAx) (x4:omega0Ax) (x5:omegaSAx) (x6:omegaIndAx) (x7:replAx) (x8:foundationAx) (x9:wellorderingAx) (x10:descrp) (x11:dsetconstrI) (x12:dsetconstrEL) (x13:dsetconstrER) (x14:exuE1) (x15:prop2setE) (x16:emptysetE) (x17:emptysetimpfalse) (x18:notinemptyset) (x19:exuE3e) (x20:setext) (x21:emptyI) (x22:noeltsimpempty) (x23:setbeta) (x24:nonemptyE1) (x25:nonemptyI) (x26:nonemptyI1) (x27:setadjoinIL) (x28:emptyinunitempty) (x29:setadjoinIR) (x30:setadjoinE) (x31:setadjoinOr) (x32:setoftrueEq) (x33:powersetI) (x34:emptyinPowerset)=> x34) as proof of (powersetAx->(setunionAx->(omega0Ax->(omegaSAx->(omegaIndAx->(replAx->(foundationAx->(wellorderingAx->(descrp->(dsetconstrI->(dsetconstrEL->(dsetconstrER->(exuE1->(prop2setE->(emptysetE->(emptysetimpfalse->(notinemptyset->(exuE3e->(setext->(emptyI->(noeltsimpempty->(setbeta->(nonemptyE1->(nonemptyI->(nonemptyI1->(setadjoinIL->(emptyinunitempty->(setadjoinIR->(setadjoinE->(setadjoinOr->(setoftrueEq->(powersetI->(emptyinPowerset->(forall (A:fofType), ((in emptyset) (powerset A)))))))))))))))))))))))))))))))))))) % Found (fun (x0:emptysetAx) (x1:setadjoinAx) (x2:powersetAx) (x3:setunionAx) (x4:omega0Ax) (x5:omegaSAx) (x6:omegaIndAx) (x7:replAx) (x8:foundationAx) (x9:wellorderingAx) (x10:descrp) (x11:dsetconstrI) (x12:dsetconstrEL) (x13:dsetconstrER) (x14:exuE1) (x15:prop2setE) (x16:emptysetE) (x17:emptysetimpfalse) (x18:notinemptyset) (x19:exuE3e) (x20:setext) (x21:emptyI) (x22:noeltsimpempty) (x23:setbeta) (x24:nonemptyE1) (x25:nonemptyI) (x26:nonemptyI1) (x27:setadjoinIL) (x28:emptyinunitempty) (x29:setadjoinIR) (x30:setadjoinE) (x31:setadjoinOr) (x32:setoftrueEq) (x33:powersetI) (x34:emptyinPowerset)=> x34) as proof of (setadjoinAx->(powersetAx->(setunionAx->(omega0Ax->(omegaSAx->(omegaIndAx->(replAx->(foundationAx->(wellorderingAx->(descrp->(dsetconstrI->(dsetconstrEL->(dsetconstrER->(exuE1->(prop2setE->(emptysetE->(emptysetimpfalse->(notinemptyset->(exuE3e->(setext->(emptyI->(noeltsimpempty->(setbeta->(nonemptyE1->(nonemptyI->(nonemptyI1->(setadjoinIL->(emptyinunitempty->(setadjoinIR->(setadjoinE->(setadjoinOr->(setoftrueEq->(powersetI->(emptyinPowerset->(forall (A:fofType), ((in emptyset) (powerset A))))))))))))))))))))))))))))))))))))) % Found (fun (x:setextAx) (x0:emptysetAx) (x1:setadjoinAx) (x2:powersetAx) (x3:setunionAx) (x4:omega0Ax) (x5:omegaSAx) (x6:omegaIndAx) (x7:replAx) (x8:foundationAx) (x9:wellorderingAx) (x10:descrp) (x11:dsetconstrI) (x12:dsetconstrEL) (x13:dsetconstrER) (x14:exuE1) (x15:prop2setE) (x16:emptysetE) (x17:emptysetimpfalse) (x18:notinemptyset) (x19:exuE3e) (x20:setext) (x21:emptyI) (x22:noeltsimpempty) (x23:setbeta) (x24:nonemptyE1) (x25:nonemptyI) (x26:nonemptyI1) (x27:setadjoinIL) (x28:emptyinunitempty) (x29:setadjoinIR) (x30:setadjoinE) (x31:setadjoinOr) (x32:setoftrueEq) (x33:powersetI) (x34:emptyinPowerset)=> x34) as proof of (emptysetAx->(setadjoinAx->(powersetAx->(setunionAx->(omega0Ax->(omegaSAx->(omegaIndAx->(replAx->(foundationAx->(wellorderingAx->(descrp->(dsetconstrI->(dsetconstrEL->(dsetconstrER->(exuE1->(prop2setE->(emptysetE->(emptysetimpfalse->(notinemptyset->(exuE3e->(setext->(emptyI->(noeltsimpempty->(setbeta->(nonemptyE1->(nonemptyI->(nonemptyI1->(setadjoinIL->(emptyinunitempty->(setadjoinIR->(setadjoinE->(setadjoinOr->(setoftrueEq->(powersetI->(emptyinPowerset->(forall (A:fofType), ((in emptyset) (powerset A)))))))))))))))))))))))))))))))))))))) % Found (fun (x:setextAx) (x0:emptysetAx) (x1:setadjoinAx) (x2:powersetAx) (x3:setunionAx) (x4:omega0Ax) (x5:omegaSAx) (x6:omegaIndAx) (x7:replAx) (x8:foundationAx) (x9:wellorderingAx) (x10:descrp) (x11:dsetconstrI) (x12:dsetconstrEL) (x13:dsetconstrER) (x14:exuE1) (x15:prop2setE) (x16:emptysetE) (x17:emptysetimpfalse) (x18:notinemptyset) (x19:exuE3e) (x20:setext) (x21:emptyI) (x22:noeltsimpempty) (x23:setbeta) (x24:nonemptyE1) (x25:nonemptyI) (x26:nonemptyI1) (x27:setadjoinIL) (x28:emptyinunitempty) (x29:setadjoinIR) (x30:setadjoinE) (x31:setadjoinOr) (x32:setoftrueEq) (x33:powersetI) (x34:emptyinPowerset)=> x34) as proof of (setextAx->(emptysetAx->(setadjoinAx->(powersetAx->(setunionAx->(omega0Ax->(omegaSAx->(omegaIndAx->(replAx->(foundationAx->(wellorderingAx->(descrp->(dsetconstrI->(dsetconstrEL->(dsetconstrER->(exuE1->(prop2setE->(emptysetE->(emptysetimpfalse->(notinemptyset->(exuE3e->(setext->(emptyI->(noeltsimpempty->(setbeta->(nonemptyE1->(nonemptyI->(nonemptyI1->(setadjoinIL->(emptyinunitempty->(setadjoinIR->(setadjoinE->(setadjoinOr->(setoftrueEq->(powersetI->(emptyinPowerset->(forall (A:fofType), ((in emptyset) (powerset A))))))))))))))))))))))))))))))))))))))) % Got proof (fun (x:setextAx) (x0:emptysetAx) (x1:setadjoinAx) (x2:powersetAx) (x3:setunionAx) (x4:omega0Ax) (x5:omegaSAx) (x6:omegaIndAx) (x7:replAx) (x8:foundationAx) (x9:wellorderingAx) (x10:descrp) (x11:dsetconstrI) (x12:dsetconstrEL) (x13:dsetconstrER) (x14:exuE1) (x15:prop2setE) (x16:emptysetE) (x17:emptysetimpfalse) (x18:notinemptyset) (x19:exuE3e) (x20:setext) (x21:emptyI) (x22:noeltsimpempty) (x23:setbeta) (x24:nonemptyE1) (x25:nonemptyI) (x26:nonemptyI1) (x27:setadjoinIL) (x28:emptyinunitempty) (x29:setadjoinIR) (x30:setadjoinE) (x31:setadjoinOr) (x32:setoftrueEq) (x33:powersetI) (x34:emptyinPowerset)=> x34) % Time elapsed = 43.363584s % node=2375 cost=742.000000 depth=36 % :::::::::::::::::::::: % % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p % (fun (x:setextAx) (x0:emptysetAx) (x1:setadjoinAx) (x2:powersetAx) (x3:setunionAx) (x4:omega0Ax) (x5:omegaSAx) (x6:omegaIndAx) (x7:replAx) (x8:foundationAx) (x9:wellorderingAx) (x10:descrp) (x11:dsetconstrI) (x12:dsetconstrEL) (x13:dsetconstrER) (x14:exuE1) (x15:prop2setE) (x16:emptysetE) (x17:emptysetimpfalse) (x18:notinemptyset) (x19:exuE3e) (x20:setext) (x21:emptyI) (x22:noeltsimpempty) (x23:setbeta) (x24:nonemptyE1) (x25:nonemptyI) (x26:nonemptyI1) (x27:setadjoinIL) (x28:emptyinunitempty) (x29:setadjoinIR) (x30:setadjoinE) (x31:setadjoinOr) (x32:setoftrueEq) (x33:powersetI) (x34:emptyinPowerset)=> x34) % % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p % EOF %------------------------------------------------------------------------------