↑ Up

cocATP---0.2.0.THM-Prf.s

View TPTP
Problem Process solution in
SystemOnTSTP Download .tgz 
%------------------------------------------------------------------------------
% File     : cocATP---0.2.0
% Problem  : SEU821^2 : TPTP v6.1.0. Released v3.7.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : python CASC.py /export/starexec/sandbox/benchmark/theBenchmark.p

% Computer : n096.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:33:14 EDT 2014

% Result   : Theorem 2.05s
% Output   : Proof 2.05s
% Verified : 
% SZS Type : None (Parsing solution fails)
% Syntax   : Number of formulae    : 0

% Comments : 
%------------------------------------------------------------------------------
%----ERROR: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% % Problem  : SEU821^2 : TPTP v6.1.0. Released v3.7.0.
% % Command  : python CASC.py /export/starexec/sandbox/benchmark/theBenchmark.p
% % Computer : n096.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 11:34:16 CDT 2014
% % CPUTime  : 2.05 
% 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 0x24ae3f8>, <kernel.DependentProduct object at 0x24ce6c8>) of role type named in_type
% Using role type
% Declaring in:(fofType->(fofType->Prop))
% FOF formula (<kernel.Constant object at 0x2529c68>, <kernel.DependentProduct object at 0x24ce680>) of role type named powerset_type
% Using role type
% Declaring powerset:(fofType->fofType)
% FOF formula (<kernel.Constant object at 0x2529c68>, <kernel.DependentProduct object at 0x24ce6c8>) of role type named nonempty_type
% Using role type
% Declaring nonempty:(fofType->Prop)
% FOF formula (<kernel.Constant object at 0x24ae128>, <kernel.DependentProduct object at 0x24cea28>) of role type named transitiveset_type
% Using role type
% Declaring transitiveset:(fofType->Prop)
% FOF formula (<kernel.Constant object at 0x24ae3f8>, <kernel.DependentProduct object at 0x24ce7e8>) of role type named stricttotalorderedByIn_type
% Using role type
% Declaring stricttotalorderedByIn:(fofType->Prop)
% FOF formula (((eq (fofType->Prop)) stricttotalorderedByIn) (fun (A:fofType)=> ((and ((and (forall (Xx:fofType), (((in Xx) A)->(forall (X:fofType), (((in X) A)->(forall (Y:fofType), (((in Y) A)->(((and ((in Xx) X)) ((in X) Y))->((in Xx) Y))))))))) (forall (X:fofType), (((in X) A)->(forall (Y:fofType), (((in Y) A)->((or ((or (((eq fofType) X) Y)) ((in X) Y))) ((in Y) X)))))))) (forall (X:fofType), (((in X) A)->(((in X) X)->False)))))) of role definition named stricttotalorderedByIn
% A new definition: (((eq (fofType->Prop)) stricttotalorderedByIn) (fun (A:fofType)=> ((and ((and (forall (Xx:fofType), (((in Xx) A)->(forall (X:fofType), (((in X) A)->(forall (Y:fofType), (((in Y) A)->(((and ((in Xx) X)) ((in X) Y))->((in Xx) Y))))))))) (forall (X:fofType), (((in X) A)->(forall (Y:fofType), (((in Y) A)->((or ((or (((eq fofType) X) Y)) ((in X) Y))) ((in Y) X)))))))) (forall (X:fofType), (((in X) A)->(((in X) X)->False))))))
% Defined: stricttotalorderedByIn:=(fun (A:fofType)=> ((and ((and (forall (Xx:fofType), (((in Xx) A)->(forall (X:fofType), (((in X) A)->(forall (Y:fofType), (((in Y) A)->(((and ((in Xx) X)) ((in X) Y))->((in Xx) Y))))))))) (forall (X:fofType), (((in X) A)->(forall (Y:fofType), (((in Y) A)->((or ((or (((eq fofType) X) Y)) ((in X) Y))) ((in Y) X)))))))) (forall (X:fofType), (((in X) A)->(((in X) X)->False)))))
% FOF formula (<kernel.Constant object at 0x24ae128>, <kernel.DependentProduct object at 0x24ce320>) of role type named wellorderedByIn_type
% Using role type
% Declaring wellorderedByIn:(fofType->Prop)
% FOF formula (((eq (fofType->Prop)) wellorderedByIn) (fun (A:fofType)=> ((and (stricttotalorderedByIn A)) (forall (X:fofType), (((in X) (powerset A))->((nonempty X)->((ex fofType) (fun (Xx:fofType)=> ((and ((in Xx) X)) (forall (Y:fofType), (((in Y) X)->((or (((eq fofType) Xx) Y)) ((in Xx) Y))))))))))))) of role definition named wellorderedByIn
% A new definition: (((eq (fofType->Prop)) wellorderedByIn) (fun (A:fofType)=> ((and (stricttotalorderedByIn A)) (forall (X:fofType), (((in X) (powerset A))->((nonempty X)->((ex fofType) (fun (Xx:fofType)=> ((and ((in Xx) X)) (forall (Y:fofType), (((in Y) X)->((or (((eq fofType) Xx) Y)) ((in Xx) Y)))))))))))))
% Defined: wellorderedByIn:=(fun (A:fofType)=> ((and (stricttotalorderedByIn A)) (forall (X:fofType), (((in X) (powerset A))->((nonempty X)->((ex fofType) (fun (Xx:fofType)=> ((and ((in Xx) X)) (forall (Y:fofType), (((in Y) X)->((or (((eq fofType) Xx) Y)) ((in Xx) Y))))))))))))
% FOF formula (<kernel.Constant object at 0x24ce320>, <kernel.DependentProduct object at 0x24ce6c8>) of role type named ordinal_type
% Using role type
% Declaring ordinal:(fofType->Prop)
% FOF formula (((eq (fofType->Prop)) ordinal) (fun (Xx:fofType)=> ((and (transitiveset Xx)) (wellorderedByIn Xx)))) of role definition named ordinal
% A new definition: (((eq (fofType->Prop)) ordinal) (fun (Xx:fofType)=> ((and (transitiveset Xx)) (wellorderedByIn Xx))))
% Defined: ordinal:=(fun (Xx:fofType)=> ((and (transitiveset Xx)) (wellorderedByIn Xx)))
% FOF formula (forall (X:fofType), ((ordinal X)->(forall (A:fofType), (((in A) X)->(((in A) A)->False))))) of role conjecture named ordinalIrrefl
% Conjecture to prove = (forall (X:fofType), ((ordinal X)->(forall (A:fofType), (((in A) X)->(((in A) A)->False))))):Prop
% Parameter fofType_DUMMY:fofType.
% We need to prove ['(forall (X:fofType), ((ordinal X)->(forall (A:fofType), (((in A) X)->(((in A) A)->False)))))']
% Parameter fofType:Type.
% Parameter in:(fofType->(fofType->Prop)).
% Parameter powerset:(fofType->fofType).
% Parameter nonempty:(fofType->Prop).
% Parameter transitiveset:(fofType->Prop).
% Definition stricttotalorderedByIn:=(fun (A:fofType)=> ((and ((and (forall (Xx:fofType), (((in Xx) A)->(forall (X:fofType), (((in X) A)->(forall (Y:fofType), (((in Y) A)->(((and ((in Xx) X)) ((in X) Y))->((in Xx) Y))))))))) (forall (X:fofType), (((in X) A)->(forall (Y:fofType), (((in Y) A)->((or ((or (((eq fofType) X) Y)) ((in X) Y))) ((in Y) X)))))))) (forall (X:fofType), (((in X) A)->(((in X) X)->False))))):(fofType->Prop).
% Definition wellorderedByIn:=(fun (A:fofType)=> ((and (stricttotalorderedByIn A)) (forall (X:fofType), (((in X) (powerset A))->((nonempty X)->((ex fofType) (fun (Xx:fofType)=> ((and ((in Xx) X)) (forall (Y:fofType), (((in Y) X)->((or (((eq fofType) Xx) Y)) ((in Xx) Y)))))))))))):(fofType->Prop).
% Definition ordinal:=(fun (Xx:fofType)=> ((and (transitiveset Xx)) (wellorderedByIn Xx))):(fofType->Prop).
% Trying to prove (forall (X:fofType), ((ordinal X)->(forall (A:fofType), (((in A) X)->(((in A) A)->False)))))
% Found x600:=(x60 x0):(((in A) A)->False)
% Found (x60 x0) as proof of (not ((in A) A))
% Found ((x6 A) x0) as proof of (not ((in A) A))
% Found (fun (x6:(forall (X0:fofType), (((in X0) X)->(((in X0) X0)->False))))=> ((x6 A) x0)) as proof of (not ((in A) A))
% Found (fun (x5:((and (forall (Xx:fofType), (((in Xx) X)->(forall (X0:fofType), (((in X0) X)->(forall (Y:fofType), (((in Y) X)->(((and ((in Xx) X0)) ((in X0) Y))->((in Xx) Y))))))))) (forall (X0:fofType), (((in X0) X)->(forall (Y:fofType), (((in Y) X)->((or ((or (((eq fofType) X0) Y)) ((in X0) Y))) ((in Y) X0)))))))) (x6:(forall (X0:fofType), (((in X0) X)->(((in X0) X0)->False))))=> ((x6 A) x0)) as proof of ((forall (X0:fofType), (((in X0) X)->(((in X0) X0)->False)))->(not ((in A) A)))
% Found (fun (x5:((and (forall (Xx:fofType), (((in Xx) X)->(forall (X0:fofType), (((in X0) X)->(forall (Y:fofType), (((in Y) X)->(((and ((in Xx) X0)) ((in X0) Y))->((in Xx) Y))))))))) (forall (X0:fofType), (((in X0) X)->(forall (Y:fofType), (((in Y) X)->((or ((or (((eq fofType) X0) Y)) ((in X0) Y))) ((in Y) X0)))))))) (x6:(forall (X0:fofType), (((in X0) X)->(((in X0) X0)->False))))=> ((x6 A) x0)) as proof of (((and (forall (Xx:fofType), (((in Xx) X)->(forall (X0:fofType), (((in X0) X)->(forall (Y:fofType), (((in Y) X)->(((and ((in Xx) X0)) ((in X0) Y))->((in Xx) Y))))))))) (forall (X0:fofType), (((in X0) X)->(forall (Y:fofType), (((in Y) X)->((or ((or (((eq fofType) X0) Y)) ((in X0) Y))) ((in Y) X0)))))))->((forall (X0:fofType), (((in X0) X)->(((in X0) X0)->False)))->(not ((in A) A))))
% Found (and_rect20 (fun (x5:((and (forall (Xx:fofType), (((in Xx) X)->(forall (X0:fofType), (((in X0) X)->(forall (Y:fofType), (((in Y) X)->(((and ((in Xx) X0)) ((in X0) Y))->((in Xx) Y))))))))) (forall (X0:fofType), (((in X0) X)->(forall (Y:fofType), (((in Y) X)->((or ((or (((eq fofType) X0) Y)) ((in X0) Y))) ((in Y) X0)))))))) (x6:(forall (X0:fofType), (((in X0) X)->(((in X0) X0)->False))))=> ((x6 A) x0))) as proof of (not ((in A) A))
% Found ((and_rect2 (not ((in A) A))) (fun (x5:((and (forall (Xx:fofType), (((in Xx) X)->(forall (X0:fofType), (((in X0) X)->(forall (Y:fofType), (((in Y) X)->(((and ((in Xx) X0)) ((in X0) Y))->((in Xx) Y))))))))) (forall (X0:fofType), (((in X0) X)->(forall (Y:fofType), (((in Y) X)->((or ((or (((eq fofType) X0) Y)) ((in X0) Y))) ((in Y) X0)))))))) (x6:(forall (X0:fofType), (((in X0) X)->(((in X0) X0)->False))))=> ((x6 A) x0))) as proof of (not ((in A) A))
% Found (((fun (P:Type) (x5:(((and (forall (Xx:fofType), (((in Xx) X)->(forall (X0:fofType), (((in X0) X)->(forall (Y:fofType), (((in Y) X)->(((and ((in Xx) X0)) ((in X0) Y))->((in Xx) Y))))))))) (forall (X0:fofType), (((in X0) X)->(forall (Y:fofType), (((in Y) X)->((or ((or (((eq fofType) X0) Y)) ((in X0) Y))) ((in Y) X0)))))))->((forall (X0:fofType), (((in X0) X)->(((in X0) X0)->False)))->P)))=> (((((and_rect ((and (forall (Xx:fofType), (((in Xx) X)->(forall (X0:fofType), (((in X0) X)->(forall (Y:fofType), (((in Y) X)->(((and ((in Xx) X0)) ((in X0) Y))->((in Xx) Y))))))))) (forall (X0:fofType), (((in X0) X)->(forall (Y:fofType), (((in Y) X)->((or ((or (((eq fofType) X0) Y)) ((in X0) Y))) ((in Y) X0)))))))) (forall (X0:fofType), (((in X0) X)->(((in X0) X0)->False)))) P) x5) x3)) (not ((in A) A))) (fun (x5:((and (forall (Xx:fofType), (((in Xx) X)->(forall (X0:fofType), (((in X0) X)->(forall (Y:fofType), (((in Y) X)->(((and ((in Xx) X0)) ((in X0) Y))->((in Xx) Y))))))))) (forall (X0:fofType), (((in X0) X)->(forall (Y:fofType), (((in Y) X)->((or ((or (((eq fofType) X0) Y)) ((in X0) Y))) ((in Y) X0)))))))) (x6:(forall (X0:fofType), (((in X0) X)->(((in X0) X0)->False))))=> ((x6 A) x0))) as proof of (not ((in A) A))
% Found (fun (x4:(forall (X0:fofType), (((in X0) (powerset X))->((nonempty X0)->((ex fofType) (fun (Xx:fofType)=> ((and ((in Xx) X0)) (forall (Y:fofType), (((in Y) X0)->((or (((eq fofType) Xx) Y)) ((in Xx) Y)))))))))))=> (((fun (P:Type) (x5:(((and (forall (Xx:fofType), (((in Xx) X)->(forall (X0:fofType), (((in X0) X)->(forall (Y:fofType), (((in Y) X)->(((and ((in Xx) X0)) ((in X0) Y))->((in Xx) Y))))))))) (forall (X0:fofType), (((in X0) X)->(forall (Y:fofType), (((in Y) X)->((or ((or (((eq fofType) X0) Y)) ((in X0) Y))) ((in Y) X0)))))))->((forall (X0:fofType), (((in X0) X)->(((in X0) X0)->False)))->P)))=> (((((and_rect ((and (forall (Xx:fofType), (((in Xx) X)->(forall (X0:fofType), (((in X0) X)->(forall (Y:fofType), (((in Y) X)->(((and ((in Xx) X0)) ((in X0) Y))->((in Xx) Y))))))))) (forall (X0:fofType), (((in X0) X)->(forall (Y:fofType), (((in Y) X)->((or ((or (((eq fofType) X0) Y)) ((in X0) Y))) ((in Y) X0)))))))) (forall (X0:fofType), (((in X0) X)->(((in X0) X0)->False)))) P) x5) x3)) (not ((in A) A))) (fun (x5:((and (forall (Xx:fofType), (((in Xx) X)->(forall (X0:fofType), (((in X0) X)->(forall (Y:fofType), (((in Y) X)->(((and ((in Xx) X0)) ((in X0) Y))->((in Xx) Y))))))))) (forall (X0:fofType), (((in X0) X)->(forall (Y:fofType), (((in Y) X)->((or ((or (((eq fofType) X0) Y)) ((in X0) Y))) ((in Y) X0)))))))) (x6:(forall (X0:fofType), (((in X0) X)->(((in X0) X0)->False))))=> ((x6 A) x0)))) as proof of (not ((in A) A))
% Found (fun (x3:(stricttotalorderedByIn X)) (x4:(forall (X0:fofType), (((in X0) (powerset X))->((nonempty X0)->((ex fofType) (fun (Xx:fofType)=> ((and ((in Xx) X0)) (forall (Y:fofType), (((in Y) X0)->((or (((eq fofType) Xx) Y)) ((in Xx) Y)))))))))))=> (((fun (P:Type) (x5:(((and (forall (Xx:fofType), (((in Xx) X)->(forall (X0:fofType), (((in X0) X)->(forall (Y:fofType), (((in Y) X)->(((and ((in Xx) X0)) ((in X0) Y))->((in Xx) Y))))))))) (forall (X0:fofType), (((in X0) X)->(forall (Y:fofType), (((in Y) X)->((or ((or (((eq fofType) X0) Y)) ((in X0) Y))) ((in Y) X0)))))))->((forall (X0:fofType), (((in X0) X)->(((in X0) X0)->False)))->P)))=> (((((and_rect ((and (forall (Xx:fofType), (((in Xx) X)->(forall (X0:fofType), (((in X0) X)->(forall (Y:fofType), (((in Y) X)->(((and ((in Xx) X0)) ((in X0) Y))->((in Xx) Y))))))))) (forall (X0:fofType), (((in X0) X)->(forall (Y:fofType), (((in Y) X)->((or ((or (((eq fofType) X0) Y)) ((in X0) Y))) ((in Y) X0)))))))) (forall (X0:fofType), (((in X0) X)->(((in X0) X0)->False)))) P) x5) x3)) (not ((in A) A))) (fun (x5:((and (forall (Xx:fofType), (((in Xx) X)->(forall (X0:fofType), (((in X0) X)->(forall (Y:fofType), (((in Y) X)->(((and ((in Xx) X0)) ((in X0) Y))->((in Xx) Y))))))))) (forall (X0:fofType), (((in X0) X)->(forall (Y:fofType), (((in Y) X)->((or ((or (((eq fofType) X0) Y)) ((in X0) Y))) ((in Y) X0)))))))) (x6:(forall (X0:fofType), (((in X0) X)->(((in X0) X0)->False))))=> ((x6 A) x0)))) as proof of ((forall (X0:fofType), (((in X0) (powerset X))->((nonempty X0)->((ex fofType) (fun (Xx:fofType)=> ((and ((in Xx) X0)) (forall (Y:fofType), (((in Y) X0)->((or (((eq fofType) Xx) Y)) ((in Xx) Y))))))))))->(not ((in A) A)))
% Found (fun (x3:(stricttotalorderedByIn X)) (x4:(forall (X0:fofType), (((in X0) (powerset X))->((nonempty X0)->((ex fofType) (fun (Xx:fofType)=> ((and ((in Xx) X0)) (forall (Y:fofType), (((in Y) X0)->((or (((eq fofType) Xx) Y)) ((in Xx) Y)))))))))))=> (((fun (P:Type) (x5:(((and (forall (Xx:fofType), (((in Xx) X)->(forall (X0:fofType), (((in X0) X)->(forall (Y:fofType), (((in Y) X)->(((and ((in Xx) X0)) ((in X0) Y))->((in Xx) Y))))))))) (forall (X0:fofType), (((in X0) X)->(forall (Y:fofType), (((in Y) X)->((or ((or (((eq fofType) X0) Y)) ((in X0) Y))) ((in Y) X0)))))))->((forall (X0:fofType), (((in X0) X)->(((in X0) X0)->False)))->P)))=> (((((and_rect ((and (forall (Xx:fofType), (((in Xx) X)->(forall (X0:fofType), (((in X0) X)->(forall (Y:fofType), (((in Y) X)->(((and ((in Xx) X0)) ((in X0) Y))->((in Xx) Y))))))))) (forall (X0:fofType), (((in X0) X)->(forall (Y:fofType), (((in Y) X)->((or ((or (((eq fofType) X0) Y)) ((in X0) Y))) ((in Y) X0)))))))) (forall (X0:fofType), (((in X0) X)->(((in X0) X0)->False)))) P) x5) x3)) (not ((in A) A))) (fun (x5:((and (forall (Xx:fofType), (((in Xx) X)->(forall (X0:fofType), (((in X0) X)->(forall (Y:fofType), (((in Y) X)->(((and ((in Xx) X0)) ((in X0) Y))->((in Xx) Y))))))))) (forall (X0:fofType), (((in X0) X)->(forall (Y:fofType), (((in Y) X)->((or ((or (((eq fofType) X0) Y)) ((in X0) Y))) ((in Y) X0)))))))) (x6:(forall (X0:fofType), (((in X0) X)->(((in X0) X0)->False))))=> ((x6 A) x0)))) as proof of ((stricttotalorderedByIn X)->((forall (X0:fofType), (((in X0) (powerset X))->((nonempty X0)->((ex fofType) (fun (Xx:fofType)=> ((and ((in Xx) X0)) (forall (Y:fofType), (((in Y) X0)->((or (((eq fofType) Xx) Y)) ((in Xx) Y))))))))))->(not ((in A) A))))
% Found (and_rect10 (fun (x3:(stricttotalorderedByIn X)) (x4:(forall (X0:fofType), (((in X0) (powerset X))->((nonempty X0)->((ex fofType) (fun (Xx:fofType)=> ((and ((in Xx) X0)) (forall (Y:fofType), (((in Y) X0)->((or (((eq fofType) Xx) Y)) ((in Xx) Y)))))))))))=> (((fun (P:Type) (x5:(((and (forall (Xx:fofType), (((in Xx) X)->(forall (X0:fofType), (((in X0) X)->(forall (Y:fofType), (((in Y) X)->(((and ((in Xx) X0)) ((in X0) Y))->((in Xx) Y))))))))) (forall (X0:fofType), (((in X0) X)->(forall (Y:fofType), (((in Y) X)->((or ((or (((eq fofType) X0) Y)) ((in X0) Y))) ((in Y) X0)))))))->((forall (X0:fofType), (((in X0) X)->(((in X0) X0)->False)))->P)))=> (((((and_rect ((and (forall (Xx:fofType), (((in Xx) X)->(forall (X0:fofType), (((in X0) X)->(forall (Y:fofType), (((in Y) X)->(((and ((in Xx) X0)) ((in X0) Y))->((in Xx) Y))))))))) (forall (X0:fofType), (((in X0) X)->(forall (Y:fofType), (((in Y) X)->((or ((or (((eq fofType) X0) Y)) ((in X0) Y))) ((in Y) X0)))))))) (forall (X0:fofType), (((in X0) X)->(((in X0) X0)->False)))) P) x5) x3)) (not ((in A) A))) (fun (x5:((and (forall (Xx:fofType), (((in Xx) X)->(forall (X0:fofType), (((in X0) X)->(forall (Y:fofType), (((in Y) X)->(((and ((in Xx) X0)) ((in X0) Y))->((in Xx) Y))))))))) (forall (X0:fofType), (((in X0) X)->(forall (Y:fofType), (((in Y) X)->((or ((or (((eq fofType) X0) Y)) ((in X0) Y))) ((in Y) X0)))))))) (x6:(forall (X0:fofType), (((in X0) X)->(((in X0) X0)->False))))=> ((x6 A) x0))))) as proof of (not ((in A) A))
% Found ((and_rect1 (not ((in A) A))) (fun (x3:(stricttotalorderedByIn X)) (x4:(forall (X0:fofType), (((in X0) (powerset X))->((nonempty X0)->((ex fofType) (fun (Xx:fofType)=> ((and ((in Xx) X0)) (forall (Y:fofType), (((in Y) X0)->((or (((eq fofType) Xx) Y)) ((in Xx) Y)))))))))))=> (((fun (P:Type) (x5:(((and (forall (Xx:fofType), (((in Xx) X)->(forall (X0:fofType), (((in X0) X)->(forall (Y:fofType), (((in Y) X)->(((and ((in Xx) X0)) ((in X0) Y))->((in Xx) Y))))))))) (forall (X0:fofType), (((in X0) X)->(forall (Y:fofType), (((in Y) X)->((or ((or (((eq fofType) X0) Y)) ((in X0) Y))) ((in Y) X0)))))))->((forall (X0:fofType), (((in X0) X)->(((in X0) X0)->False)))->P)))=> (((((and_rect ((and (forall (Xx:fofType), (((in Xx) X)->(forall (X0:fofType), (((in X0) X)->(forall (Y:fofType), (((in Y) X)->(((and ((in Xx) X0)) ((in X0) Y))->((in Xx) Y))))))))) (forall (X0:fofType), (((in X0) X)->(forall (Y:fofType), (((in Y) X)->((or ((or (((eq fofType) X0) Y)) ((in X0) Y))) ((in Y) X0)))))))) (forall (X0:fofType), (((in X0) X)->(((in X0) X0)->False)))) P) x5) x3)) (not ((in A) A))) (fun (x5:((and (forall (Xx:fofType), (((in Xx) X)->(forall (X0:fofType), (((in X0) X)->(forall (Y:fofType), (((in Y) X)->(((and ((in Xx) X0)) ((in X0) Y))->((in Xx) Y))))))))) (forall (X0:fofType), (((in X0) X)->(forall (Y:fofType), (((in Y) X)->((or ((or (((eq fofType) X0) Y)) ((in X0) Y))) ((in Y) X0)))))))) (x6:(forall (X0:fofType), (((in X0) X)->(((in X0) X0)->False))))=> ((x6 A) x0))))) as proof of (not ((in A) A))
% Found (((fun (P:Type) (x3:((stricttotalorderedByIn X)->((forall (X0:fofType), (((in X0) (powerset X))->((nonempty X0)->((ex fofType) (fun (Xx:fofType)=> ((and ((in Xx) X0)) (forall (Y:fofType), (((in Y) X0)->((or (((eq fofType) Xx) Y)) ((in Xx) Y))))))))))->P)))=> (((((and_rect (stricttotalorderedByIn X)) (forall (X0:fofType), (((in X0) (powerset X))->((nonempty X0)->((ex fofType) (fun (Xx:fofType)=> ((and ((in Xx) X0)) (forall (Y:fofType), (((in Y) X0)->((or (((eq fofType) Xx) Y)) ((in Xx) Y))))))))))) P) x3) x2)) (not ((in A) A))) (fun (x3:(stricttotalorderedByIn X)) (x4:(forall (X0:fofType), (((in X0) (powerset X))->((nonempty X0)->((ex fofType) (fun (Xx:fofType)=> ((and ((in Xx) X0)) (forall (Y:fofType), (((in Y) X0)->((or (((eq fofType) Xx) Y)) ((in Xx) Y)))))))))))=> (((fun (P:Type) (x5:(((and (forall (Xx:fofType), (((in Xx) X)->(forall (X0:fofType), (((in X0) X)->(forall (Y:fofType), (((in Y) X)->(((and ((in Xx) X0)) ((in X0) Y))->((in Xx) Y))))))))) (forall (X0:fofType), (((in X0) X)->(forall (Y:fofType), (((in Y) X)->((or ((or (((eq fofType) X0) Y)) ((in X0) Y))) ((in Y) X0)))))))->((forall (X0:fofType), (((in X0) X)->(((in X0) X0)->False)))->P)))=> (((((and_rect ((and (forall (Xx:fofType), (((in Xx) X)->(forall (X0:fofType), (((in X0) X)->(forall (Y:fofType), (((in Y) X)->(((and ((in Xx) X0)) ((in X0) Y))->((in Xx) Y))))))))) (forall (X0:fofType), (((in X0) X)->(forall (Y:fofType), (((in Y) X)->((or ((or (((eq fofType) X0) Y)) ((in X0) Y))) ((in Y) X0)))))))) (forall (X0:fofType), (((in X0) X)->(((in X0) X0)->False)))) P) x5) x3)) (not ((in A) A))) (fun (x5:((and (forall (Xx:fofType), (((in Xx) X)->(forall (X0:fofType), (((in X0) X)->(forall (Y:fofType), (((in Y) X)->(((and ((in Xx) X0)) ((in X0) Y))->((in Xx) Y))))))))) (forall (X0:fofType), (((in X0) X)->(forall (Y:fofType), (((in Y) X)->((or ((or (((eq fofType) X0) Y)) ((in X0) Y))) ((in Y) X0)))))))) (x6:(forall (X0:fofType), (((in X0) X)->(((in X0) X0)->False))))=> ((x6 A) x0))))) as proof of (not ((in A) A))
% Found (fun (x2:(wellorderedByIn X))=> (((fun (P:Type) (x3:((stricttotalorderedByIn X)->((forall (X0:fofType), (((in X0) (powerset X))->((nonempty X0)->((ex fofType) (fun (Xx:fofType)=> ((and ((in Xx) X0)) (forall (Y:fofType), (((in Y) X0)->((or (((eq fofType) Xx) Y)) ((in Xx) Y))))))))))->P)))=> (((((and_rect (stricttotalorderedByIn X)) (forall (X0:fofType), (((in X0) (powerset X))->((nonempty X0)->((ex fofType) (fun (Xx:fofType)=> ((and ((in Xx) X0)) (forall (Y:fofType), (((in Y) X0)->((or (((eq fofType) Xx) Y)) ((in Xx) Y))))))))))) P) x3) x2)) (not ((in A) A))) (fun (x3:(stricttotalorderedByIn X)) (x4:(forall (X0:fofType), (((in X0) (powerset X))->((nonempty X0)->((ex fofType) (fun (Xx:fofType)=> ((and ((in Xx) X0)) (forall (Y:fofType), (((in Y) X0)->((or (((eq fofType) Xx) Y)) ((in Xx) Y)))))))))))=> (((fun (P:Type) (x5:(((and (forall (Xx:fofType), (((in Xx) X)->(forall (X0:fofType), (((in X0) X)->(forall (Y:fofType), (((in Y) X)->(((and ((in Xx) X0)) ((in X0) Y))->((in Xx) Y))))))))) (forall (X0:fofType), (((in X0) X)->(forall (Y:fofType), (((in Y) X)->((or ((or (((eq fofType) X0) Y)) ((in X0) Y))) ((in Y) X0)))))))->((forall (X0:fofType), (((in X0) X)->(((in X0) X0)->False)))->P)))=> (((((and_rect ((and (forall (Xx:fofType), (((in Xx) X)->(forall (X0:fofType), (((in X0) X)->(forall (Y:fofType), (((in Y) X)->(((and ((in Xx) X0)) ((in X0) Y))->((in Xx) Y))))))))) (forall (X0:fofType), (((in X0) X)->(forall (Y:fofType), (((in Y) X)->((or ((or (((eq fofType) X0) Y)) ((in X0) Y))) ((in Y) X0)))))))) (forall (X0:fofType), (((in X0) X)->(((in X0) X0)->False)))) P) x5) x3)) (not ((in A) A))) (fun (x5:((and (forall (Xx:fofType), (((in Xx) X)->(forall (X0:fofType), (((in X0) X)->(forall (Y:fofType), (((in Y) X)->(((and ((in Xx) X0)) ((in X0) Y))->((in Xx) Y))))))))) (forall (X0:fofType), (((in X0) X)->(forall (Y:fofType), (((in Y) X)->((or ((or (((eq fofType) X0) Y)) ((in X0) Y))) ((in Y) X0)))))))) (x6:(forall (X0:fofType), (((in X0) X)->(((in X0) X0)->False))))=> ((x6 A) x0)))))) as proof of (not ((in A) A))
% Found (fun (x1:(transitiveset X)) (x2:(wellorderedByIn X))=> (((fun (P:Type) (x3:((stricttotalorderedByIn X)->((forall (X0:fofType), (((in X0) (powerset X))->((nonempty X0)->((ex fofType) (fun (Xx:fofType)=> ((and ((in Xx) X0)) (forall (Y:fofType), (((in Y) X0)->((or (((eq fofType) Xx) Y)) ((in Xx) Y))))))))))->P)))=> (((((and_rect (stricttotalorderedByIn X)) (forall (X0:fofType), (((in X0) (powerset X))->((nonempty X0)->((ex fofType) (fun (Xx:fofType)=> ((and ((in Xx) X0)) (forall (Y:fofType), (((in Y) X0)->((or (((eq fofType) Xx) Y)) ((in Xx) Y))))))))))) P) x3) x2)) (not ((in A) A))) (fun (x3:(stricttotalorderedByIn X)) (x4:(forall (X0:fofType), (((in X0) (powerset X))->((nonempty X0)->((ex fofType) (fun (Xx:fofType)=> ((and ((in Xx) X0)) (forall (Y:fofType), (((in Y) X0)->((or (((eq fofType) Xx) Y)) ((in Xx) Y)))))))))))=> (((fun (P:Type) (x5:(((and (forall (Xx:fofType), (((in Xx) X)->(forall (X0:fofType), (((in X0) X)->(forall (Y:fofType), (((in Y) X)->(((and ((in Xx) X0)) ((in X0) Y))->((in Xx) Y))))))))) (forall (X0:fofType), (((in X0) X)->(forall (Y:fofType), (((in Y) X)->((or ((or (((eq fofType) X0) Y)) ((in X0) Y))) ((in Y) X0)))))))->((forall (X0:fofType), (((in X0) X)->(((in X0) X0)->False)))->P)))=> (((((and_rect ((and (forall (Xx:fofType), (((in Xx) X)->(forall (X0:fofType), (((in X0) X)->(forall (Y:fofType), (((in Y) X)->(((and ((in Xx) X0)) ((in X0) Y))->((in Xx) Y))))))))) (forall (X0:fofType), (((in X0) X)->(forall (Y:fofType), (((in Y) X)->((or ((or (((eq fofType) X0) Y)) ((in X0) Y))) ((in Y) X0)))))))) (forall (X0:fofType), (((in X0) X)->(((in X0) X0)->False)))) P) x5) x3)) (not ((in A) A))) (fun (x5:((and (forall (Xx:fofType), (((in Xx) X)->(forall (X0:fofType), (((in X0) X)->(forall (Y:fofType), (((in Y) X)->(((and ((in Xx) X0)) ((in X0) Y))->((in Xx) Y))))))))) (forall (X0:fofType), (((in X0) X)->(forall (Y:fofType), (((in Y) X)->((or ((or (((eq fofType) X0) Y)) ((in X0) Y))) ((in Y) X0)))))))) (x6:(forall (X0:fofType), (((in X0) X)->(((in X0) X0)->False))))=> ((x6 A) x0)))))) as proof of ((wellorderedByIn X)->(not ((in A) A)))
% Found (fun (x1:(transitiveset X)) (x2:(wellorderedByIn X))=> (((fun (P:Type) (x3:((stricttotalorderedByIn X)->((forall (X0:fofType), (((in X0) (powerset X))->((nonempty X0)->((ex fofType) (fun (Xx:fofType)=> ((and ((in Xx) X0)) (forall (Y:fofType), (((in Y) X0)->((or (((eq fofType) Xx) Y)) ((in Xx) Y))))))))))->P)))=> (((((and_rect (stricttotalorderedByIn X)) (forall (X0:fofType), (((in X0) (powerset X))->((nonempty X0)->((ex fofType) (fun (Xx:fofType)=> ((and ((in Xx) X0)) (forall (Y:fofType), (((in Y) X0)->((or (((eq fofType) Xx) Y)) ((in Xx) Y))))))))))) P) x3) x2)) (not ((in A) A))) (fun (x3:(stricttotalorderedByIn X)) (x4:(forall (X0:fofType), (((in X0) (powerset X))->((nonempty X0)->((ex fofType) (fun (Xx:fofType)=> ((and ((in Xx) X0)) (forall (Y:fofType), (((in Y) X0)->((or (((eq fofType) Xx) Y)) ((in Xx) Y)))))))))))=> (((fun (P:Type) (x5:(((and (forall (Xx:fofType), (((in Xx) X)->(forall (X0:fofType), (((in X0) X)->(forall (Y:fofType), (((in Y) X)->(((and ((in Xx) X0)) ((in X0) Y))->((in Xx) Y))))))))) (forall (X0:fofType), (((in X0) X)->(forall (Y:fofType), (((in Y) X)->((or ((or (((eq fofType) X0) Y)) ((in X0) Y))) ((in Y) X0)))))))->((forall (X0:fofType), (((in X0) X)->(((in X0) X0)->False)))->P)))=> (((((and_rect ((and (forall (Xx:fofType), (((in Xx) X)->(forall (X0:fofType), (((in X0) X)->(forall (Y:fofType), (((in Y) X)->(((and ((in Xx) X0)) ((in X0) Y))->((in Xx) Y))))))))) (forall (X0:fofType), (((in X0) X)->(forall (Y:fofType), (((in Y) X)->((or ((or (((eq fofType) X0) Y)) ((in X0) Y))) ((in Y) X0)))))))) (forall (X0:fofType), (((in X0) X)->(((in X0) X0)->False)))) P) x5) x3)) (not ((in A) A))) (fun (x5:((and (forall (Xx:fofType), (((in Xx) X)->(forall (X0:fofType), (((in X0) X)->(forall (Y:fofType), (((in Y) X)->(((and ((in Xx) X0)) ((in X0) Y))->((in Xx) Y))))))))) (forall (X0:fofType), (((in X0) X)->(forall (Y:fofType), (((in Y) X)->((or ((or (((eq fofType) X0) Y)) ((in X0) Y))) ((in Y) X0)))))))) (x6:(forall (X0:fofType), (((in X0) X)->(((in X0) X0)->False))))=> ((x6 A) x0)))))) as proof of ((transitiveset X)->((wellorderedByIn X)->(not ((in A) A))))
% Found (and_rect00 (fun (x1:(transitiveset X)) (x2:(wellorderedByIn X))=> (((fun (P:Type) (x3:((stricttotalorderedByIn X)->((forall (X0:fofType), (((in X0) (powerset X))->((nonempty X0)->((ex fofType) (fun (Xx:fofType)=> ((and ((in Xx) X0)) (forall (Y:fofType), (((in Y) X0)->((or (((eq fofType) Xx) Y)) ((in Xx) Y))))))))))->P)))=> (((((and_rect (stricttotalorderedByIn X)) (forall (X0:fofType), (((in X0) (powerset X))->((nonempty X0)->((ex fofType) (fun (Xx:fofType)=> ((and ((in Xx) X0)) (forall (Y:fofType), (((in Y) X0)->((or (((eq fofType) Xx) Y)) ((in Xx) Y))))))))))) P) x3) x2)) (not ((in A) A))) (fun (x3:(stricttotalorderedByIn X)) (x4:(forall (X0:fofType), (((in X0) (powerset X))->((nonempty X0)->((ex fofType) (fun (Xx:fofType)=> ((and ((in Xx) X0)) (forall (Y:fofType), (((in Y) X0)->((or (((eq fofType) Xx) Y)) ((in Xx) Y)))))))))))=> (((fun (P:Type) (x5:(((and (forall (Xx:fofType), (((in Xx) X)->(forall (X0:fofType), (((in X0) X)->(forall (Y:fofType), (((in Y) X)->(((and ((in Xx) X0)) ((in X0) Y))->((in Xx) Y))))))))) (forall (X0:fofType), (((in X0) X)->(forall (Y:fofType), (((in Y) X)->((or ((or (((eq fofType) X0) Y)) ((in X0) Y))) ((in Y) X0)))))))->((forall (X0:fofType), (((in X0) X)->(((in X0) X0)->False)))->P)))=> (((((and_rect ((and (forall (Xx:fofType), (((in Xx) X)->(forall (X0:fofType), (((in X0) X)->(forall (Y:fofType), (((in Y) X)->(((and ((in Xx) X0)) ((in X0) Y))->((in Xx) Y))))))))) (forall (X0:fofType), (((in X0) X)->(forall (Y:fofType), (((in Y) X)->((or ((or (((eq fofType) X0) Y)) ((in X0) Y))) ((in Y) X0)))))))) (forall (X0:fofType), (((in X0) X)->(((in X0) X0)->False)))) P) x5) x3)) (not ((in A) A))) (fun (x5:((and (forall (Xx:fofType), (((in Xx) X)->(forall (X0:fofType), (((in X0) X)->(forall (Y:fofType), (((in Y) X)->(((and ((in Xx) X0)) ((in X0) Y))->((in Xx) Y))))))))) (forall (X0:fofType), (((in X0) X)->(forall (Y:fofType), (((in Y) X)->((or ((or (((eq fofType) X0) Y)) ((in X0) Y))) ((in Y) X0)))))))) (x6:(forall (X0:fofType), (((in X0) X)->(((in X0) X0)->False))))=> ((x6 A) x0))))))) as proof of (not ((in A) A))
% Found ((and_rect0 (not ((in A) A))) (fun (x1:(transitiveset X)) (x2:(wellorderedByIn X))=> (((fun (P:Type) (x3:((stricttotalorderedByIn X)->((forall (X0:fofType), (((in X0) (powerset X))->((nonempty X0)->((ex fofType) (fun (Xx:fofType)=> ((and ((in Xx) X0)) (forall (Y:fofType), (((in Y) X0)->((or (((eq fofType) Xx) Y)) ((in Xx) Y))))))))))->P)))=> (((((and_rect (stricttotalorderedByIn X)) (forall (X0:fofType), (((in X0) (powerset X))->((nonempty X0)->((ex fofType) (fun (Xx:fofType)=> ((and ((in Xx) X0)) (forall (Y:fofType), (((in Y) X0)->((or (((eq fofType) Xx) Y)) ((in Xx) Y))))))))))) P) x3) x2)) (not ((in A) A))) (fun (x3:(stricttotalorderedByIn X)) (x4:(forall (X0:fofType), (((in X0) (powerset X))->((nonempty X0)->((ex fofType) (fun (Xx:fofType)=> ((and ((in Xx) X0)) (forall (Y:fofType), (((in Y) X0)->((or (((eq fofType) Xx) Y)) ((in Xx) Y)))))))))))=> (((fun (P:Type) (x5:(((and (forall (Xx:fofType), (((in Xx) X)->(forall (X0:fofType), (((in X0) X)->(forall (Y:fofType), (((in Y) X)->(((and ((in Xx) X0)) ((in X0) Y))->((in Xx) Y))))))))) (forall (X0:fofType), (((in X0) X)->(forall (Y:fofType), (((in Y) X)->((or ((or (((eq fofType) X0) Y)) ((in X0) Y))) ((in Y) X0)))))))->((forall (X0:fofType), (((in X0) X)->(((in X0) X0)->False)))->P)))=> (((((and_rect ((and (forall (Xx:fofType), (((in Xx) X)->(forall (X0:fofType), (((in X0) X)->(forall (Y:fofType), (((in Y) X)->(((and ((in Xx) X0)) ((in X0) Y))->((in Xx) Y))))))))) (forall (X0:fofType), (((in X0) X)->(forall (Y:fofType), (((in Y) X)->((or ((or (((eq fofType) X0) Y)) ((in X0) Y))) ((in Y) X0)))))))) (forall (X0:fofType), (((in X0) X)->(((in X0) X0)->False)))) P) x5) x3)) (not ((in A) A))) (fun (x5:((and (forall (Xx:fofType), (((in Xx) X)->(forall (X0:fofType), (((in X0) X)->(forall (Y:fofType), (((in Y) X)->(((and ((in Xx) X0)) ((in X0) Y))->((in Xx) Y))))))))) (forall (X0:fofType), (((in X0) X)->(forall (Y:fofType), (((in Y) X)->((or ((or (((eq fofType) X0) Y)) ((in X0) Y))) ((in Y) X0)))))))) (x6:(forall (X0:fofType), (((in X0) X)->(((in X0) X0)->False))))=> ((x6 A) x0))))))) as proof of (not ((in A) A))
% Found (((fun (P:Type) (x1:((transitiveset X)->((wellorderedByIn X)->P)))=> (((((and_rect (transitiveset X)) (wellorderedByIn X)) P) x1) x)) (not ((in A) A))) (fun (x1:(transitiveset X)) (x2:(wellorderedByIn X))=> (((fun (P:Type) (x3:((stricttotalorderedByIn X)->((forall (X0:fofType), (((in X0) (powerset X))->((nonempty X0)->((ex fofType) (fun (Xx:fofType)=> ((and ((in Xx) X0)) (forall (Y:fofType), (((in Y) X0)->((or (((eq fofType) Xx) Y)) ((in Xx) Y))))))))))->P)))=> (((((and_rect (stricttotalorderedByIn X)) (forall (X0:fofType), (((in X0) (powerset X))->((nonempty X0)->((ex fofType) (fun (Xx:fofType)=> ((and ((in Xx) X0)) (forall (Y:fofType), (((in Y) X0)->((or (((eq fofType) Xx) Y)) ((in Xx) Y))))))))))) P) x3) x2)) (not ((in A) A))) (fun (x3:(stricttotalorderedByIn X)) (x4:(forall (X0:fofType), (((in X0) (powerset X))->((nonempty X0)->((ex fofType) (fun (Xx:fofType)=> ((and ((in Xx) X0)) (forall (Y:fofType), (((in Y) X0)->((or (((eq fofType) Xx) Y)) ((in Xx) Y)))))))))))=> (((fun (P:Type) (x5:(((and (forall (Xx:fofType), (((in Xx) X)->(forall (X0:fofType), (((in X0) X)->(forall (Y:fofType), (((in Y) X)->(((and ((in Xx) X0)) ((in X0) Y))->((in Xx) Y))))))))) (forall (X0:fofType), (((in X0) X)->(forall (Y:fofType), (((in Y) X)->((or ((or (((eq fofType) X0) Y)) ((in X0) Y))) ((in Y) X0)))))))->((forall (X0:fofType), (((in X0) X)->(((in X0) X0)->False)))->P)))=> (((((and_rect ((and (forall (Xx:fofType), (((in Xx) X)->(forall (X0:fofType), (((in X0) X)->(forall (Y:fofType), (((in Y) X)->(((and ((in Xx) X0)) ((in X0) Y))->((in Xx) Y))))))))) (forall (X0:fofType), (((in X0) X)->(forall (Y:fofType), (((in Y) X)->((or ((or (((eq fofType) X0) Y)) ((in X0) Y))) ((in Y) X0)))))))) (forall (X0:fofType), (((in X0) X)->(((in X0) X0)->False)))) P) x5) x3)) (not ((in A) A))) (fun (x5:((and (forall (Xx:fofType), (((in Xx) X)->(forall (X0:fofType), (((in X0) X)->(forall (Y:fofType), (((in Y) X)->(((and ((in Xx) X0)) ((in X0) Y))->((in Xx) Y))))))))) (forall (X0:fofType), (((in X0) X)->(forall (Y:fofType), (((in Y) X)->((or ((or (((eq fofType) X0) Y)) ((in X0) Y))) ((in Y) X0)))))))) (x6:(forall (X0:fofType), (((in X0) X)->(((in X0) X0)->False))))=> ((x6 A) x0))))))) as proof of (not ((in A) A))
% Found (fun (x0:((in A) X))=> (((fun (P:Type) (x1:((transitiveset X)->((wellorderedByIn X)->P)))=> (((((and_rect (transitiveset X)) (wellorderedByIn X)) P) x1) x)) (not ((in A) A))) (fun (x1:(transitiveset X)) (x2:(wellorderedByIn X))=> (((fun (P:Type) (x3:((stricttotalorderedByIn X)->((forall (X0:fofType), (((in X0) (powerset X))->((nonempty X0)->((ex fofType) (fun (Xx:fofType)=> ((and ((in Xx) X0)) (forall (Y:fofType), (((in Y) X0)->((or (((eq fofType) Xx) Y)) ((in Xx) Y))))))))))->P)))=> (((((and_rect (stricttotalorderedByIn X)) (forall (X0:fofType), (((in X0) (powerset X))->((nonempty X0)->((ex fofType) (fun (Xx:fofType)=> ((and ((in Xx) X0)) (forall (Y:fofType), (((in Y) X0)->((or (((eq fofType) Xx) Y)) ((in Xx) Y))))))))))) P) x3) x2)) (not ((in A) A))) (fun (x3:(stricttotalorderedByIn X)) (x4:(forall (X0:fofType), (((in X0) (powerset X))->((nonempty X0)->((ex fofType) (fun (Xx:fofType)=> ((and ((in Xx) X0)) (forall (Y:fofType), (((in Y) X0)->((or (((eq fofType) Xx) Y)) ((in Xx) Y)))))))))))=> (((fun (P:Type) (x5:(((and (forall (Xx:fofType), (((in Xx) X)->(forall (X0:fofType), (((in X0) X)->(forall (Y:fofType), (((in Y) X)->(((and ((in Xx) X0)) ((in X0) Y))->((in Xx) Y))))))))) (forall (X0:fofType), (((in X0) X)->(forall (Y:fofType), (((in Y) X)->((or ((or (((eq fofType) X0) Y)) ((in X0) Y))) ((in Y) X0)))))))->((forall (X0:fofType), (((in X0) X)->(((in X0) X0)->False)))->P)))=> (((((and_rect ((and (forall (Xx:fofType), (((in Xx) X)->(forall (X0:fofType), (((in X0) X)->(forall (Y:fofType), (((in Y) X)->(((and ((in Xx) X0)) ((in X0) Y))->((in Xx) Y))))))))) (forall (X0:fofType), (((in X0) X)->(forall (Y:fofType), (((in Y) X)->((or ((or (((eq fofType) X0) Y)) ((in X0) Y))) ((in Y) X0)))))))) (forall (X0:fofType), (((in X0) X)->(((in X0) X0)->False)))) P) x5) x3)) (not ((in A) A))) (fun (x5:((and (forall (Xx:fofType), (((in Xx) X)->(forall (X0:fofType), (((in X0) X)->(forall (Y:fofType), (((in Y) X)->(((and ((in Xx) X0)) ((in X0) Y))->((in Xx) Y))))))))) (forall (X0:fofType), (((in X0) X)->(forall (Y:fofType), (((in Y) X)->((or ((or (((eq fofType) X0) Y)) ((in X0) Y))) ((in Y) X0)))))))) (x6:(forall (X0:fofType), (((in X0) X)->(((in X0) X0)->False))))=> ((x6 A) x0)))))))) as proof of (not ((in A) A))
% Found (fun (A:fofType) (x0:((in A) X))=> (((fun (P:Type) (x1:((transitiveset X)->((wellorderedByIn X)->P)))=> (((((and_rect (transitiveset X)) (wellorderedByIn X)) P) x1) x)) (not ((in A) A))) (fun (x1:(transitiveset X)) (x2:(wellorderedByIn X))=> (((fun (P:Type) (x3:((stricttotalorderedByIn X)->((forall (X0:fofType), (((in X0) (powerset X))->((nonempty X0)->((ex fofType) (fun (Xx:fofType)=> ((and ((in Xx) X0)) (forall (Y:fofType), (((in Y) X0)->((or (((eq fofType) Xx) Y)) ((in Xx) Y))))))))))->P)))=> (((((and_rect (stricttotalorderedByIn X)) (forall (X0:fofType), (((in X0) (powerset X))->((nonempty X0)->((ex fofType) (fun (Xx:fofType)=> ((and ((in Xx) X0)) (forall (Y:fofType), (((in Y) X0)->((or (((eq fofType) Xx) Y)) ((in Xx) Y))))))))))) P) x3) x2)) (not ((in A) A))) (fun (x3:(stricttotalorderedByIn X)) (x4:(forall (X0:fofType), (((in X0) (powerset X))->((nonempty X0)->((ex fofType) (fun (Xx:fofType)=> ((and ((in Xx) X0)) (forall (Y:fofType), (((in Y) X0)->((or (((eq fofType) Xx) Y)) ((in Xx) Y)))))))))))=> (((fun (P:Type) (x5:(((and (forall (Xx:fofType), (((in Xx) X)->(forall (X0:fofType), (((in X0) X)->(forall (Y:fofType), (((in Y) X)->(((and ((in Xx) X0)) ((in X0) Y))->((in Xx) Y))))))))) (forall (X0:fofType), (((in X0) X)->(forall (Y:fofType), (((in Y) X)->((or ((or (((eq fofType) X0) Y)) ((in X0) Y))) ((in Y) X0)))))))->((forall (X0:fofType), (((in X0) X)->(((in X0) X0)->False)))->P)))=> (((((and_rect ((and (forall (Xx:fofType), (((in Xx) X)->(forall (X0:fofType), (((in X0) X)->(forall (Y:fofType), (((in Y) X)->(((and ((in Xx) X0)) ((in X0) Y))->((in Xx) Y))))))))) (forall (X0:fofType), (((in X0) X)->(forall (Y:fofType), (((in Y) X)->((or ((or (((eq fofType) X0) Y)) ((in X0) Y))) ((in Y) X0)))))))) (forall (X0:fofType), (((in X0) X)->(((in X0) X0)->False)))) P) x5) x3)) (not ((in A) A))) (fun (x5:((and (forall (Xx:fofType), (((in Xx) X)->(forall (X0:fofType), (((in X0) X)->(forall (Y:fofType), (((in Y) X)->(((and ((in Xx) X0)) ((in X0) Y))->((in Xx) Y))))))))) (forall (X0:fofType), (((in X0) X)->(forall (Y:fofType), (((in Y) X)->((or ((or (((eq fofType) X0) Y)) ((in X0) Y))) ((in Y) X0)))))))) (x6:(forall (X0:fofType), (((in X0) X)->(((in X0) X0)->False))))=> ((x6 A) x0)))))))) as proof of (((in A) X)->(not ((in A) A)))
% Found (fun (x:(ordinal X)) (A:fofType) (x0:((in A) X))=> (((fun (P:Type) (x1:((transitiveset X)->((wellorderedByIn X)->P)))=> (((((and_rect (transitiveset X)) (wellorderedByIn X)) P) x1) x)) (not ((in A) A))) (fun (x1:(transitiveset X)) (x2:(wellorderedByIn X))=> (((fun (P:Type) (x3:((stricttotalorderedByIn X)->((forall (X0:fofType), (((in X0) (powerset X))->((nonempty X0)->((ex fofType) (fun (Xx:fofType)=> ((and ((in Xx) X0)) (forall (Y:fofType), (((in Y) X0)->((or (((eq fofType) Xx) Y)) ((in Xx) Y))))))))))->P)))=> (((((and_rect (stricttotalorderedByIn X)) (forall (X0:fofType), (((in X0) (powerset X))->((nonempty X0)->((ex fofType) (fun (Xx:fofType)=> ((and ((in Xx) X0)) (forall (Y:fofType), (((in Y) X0)->((or (((eq fofType) Xx) Y)) ((in Xx) Y))))))))))) P) x3) x2)) (not ((in A) A))) (fun (x3:(stricttotalorderedByIn X)) (x4:(forall (X0:fofType), (((in X0) (powerset X))->((nonempty X0)->((ex fofType) (fun (Xx:fofType)=> ((and ((in Xx) X0)) (forall (Y:fofType), (((in Y) X0)->((or (((eq fofType) Xx) Y)) ((in Xx) Y)))))))))))=> (((fun (P:Type) (x5:(((and (forall (Xx:fofType), (((in Xx) X)->(forall (X0:fofType), (((in X0) X)->(forall (Y:fofType), (((in Y) X)->(((and ((in Xx) X0)) ((in X0) Y))->((in Xx) Y))))))))) (forall (X0:fofType), (((in X0) X)->(forall (Y:fofType), (((in Y) X)->((or ((or (((eq fofType) X0) Y)) ((in X0) Y))) ((in Y) X0)))))))->((forall (X0:fofType), (((in X0) X)->(((in X0) X0)->False)))->P)))=> (((((and_rect ((and (forall (Xx:fofType), (((in Xx) X)->(forall (X0:fofType), (((in X0) X)->(forall (Y:fofType), (((in Y) X)->(((and ((in Xx) X0)) ((in X0) Y))->((in Xx) Y))))))))) (forall (X0:fofType), (((in X0) X)->(forall (Y:fofType), (((in Y) X)->((or ((or (((eq fofType) X0) Y)) ((in X0) Y))) ((in Y) X0)))))))) (forall (X0:fofType), (((in X0) X)->(((in X0) X0)->False)))) P) x5) x3)) (not ((in A) A))) (fun (x5:((and (forall (Xx:fofType), (((in Xx) X)->(forall (X0:fofType), (((in X0) X)->(forall (Y:fofType), (((in Y) X)->(((and ((in Xx) X0)) ((in X0) Y))->((in Xx) Y))))))))) (forall (X0:fofType), (((in X0) X)->(forall (Y:fofType), (((in Y) X)->((or ((or (((eq fofType) X0) Y)) ((in X0) Y))) ((in Y) X0)))))))) (x6:(forall (X0:fofType), (((in X0) X)->(((in X0) X0)->False))))=> ((x6 A) x0)))))))) as proof of (forall (A:fofType), (((in A) X)->(not ((in A) A))))
% Found (fun (X:fofType) (x:(ordinal X)) (A:fofType) (x0:((in A) X))=> (((fun (P:Type) (x1:((transitiveset X)->((wellorderedByIn X)->P)))=> (((((and_rect (transitiveset X)) (wellorderedByIn X)) P) x1) x)) (not ((in A) A))) (fun (x1:(transitiveset X)) (x2:(wellorderedByIn X))=> (((fun (P:Type) (x3:((stricttotalorderedByIn X)->((forall (X0:fofType), (((in X0) (powerset X))->((nonempty X0)->((ex fofType) (fun (Xx:fofType)=> ((and ((in Xx) X0)) (forall (Y:fofType), (((in Y) X0)->((or (((eq fofType) Xx) Y)) ((in Xx) Y))))))))))->P)))=> (((((and_rect (stricttotalorderedByIn X)) (forall (X0:fofType), (((in X0) (powerset X))->((nonempty X0)->((ex fofType) (fun (Xx:fofType)=> ((and ((in Xx) X0)) (forall (Y:fofType), (((in Y) X0)->((or (((eq fofType) Xx) Y)) ((in Xx) Y))))))))))) P) x3) x2)) (not ((in A) A))) (fun (x3:(stricttotalorderedByIn X)) (x4:(forall (X0:fofType), (((in X0) (powerset X))->((nonempty X0)->((ex fofType) (fun (Xx:fofType)=> ((and ((in Xx) X0)) (forall (Y:fofType), (((in Y) X0)->((or (((eq fofType) Xx) Y)) ((in Xx) Y)))))))))))=> (((fun (P:Type) (x5:(((and (forall (Xx:fofType), (((in Xx) X)->(forall (X0:fofType), (((in X0) X)->(forall (Y:fofType), (((in Y) X)->(((and ((in Xx) X0)) ((in X0) Y))->((in Xx) Y))))))))) (forall (X0:fofType), (((in X0) X)->(forall (Y:fofType), (((in Y) X)->((or ((or (((eq fofType) X0) Y)) ((in X0) Y))) ((in Y) X0)))))))->((forall (X0:fofType), (((in X0) X)->(((in X0) X0)->False)))->P)))=> (((((and_rect ((and (forall (Xx:fofType), (((in Xx) X)->(forall (X0:fofType), (((in X0) X)->(forall (Y:fofType), (((in Y) X)->(((and ((in Xx) X0)) ((in X0) Y))->((in Xx) Y))))))))) (forall (X0:fofType), (((in X0) X)->(forall (Y:fofType), (((in Y) X)->((or ((or (((eq fofType) X0) Y)) ((in X0) Y))) ((in Y) X0)))))))) (forall (X0:fofType), (((in X0) X)->(((in X0) X0)->False)))) P) x5) x3)) (not ((in A) A))) (fun (x5:((and (forall (Xx:fofType), (((in Xx) X)->(forall (X0:fofType), (((in X0) X)->(forall (Y:fofType), (((in Y) X)->(((and ((in Xx) X0)) ((in X0) Y))->((in Xx) Y))))))))) (forall (X0:fofType), (((in X0) X)->(forall (Y:fofType), (((in Y) X)->((or ((or (((eq fofType) X0) Y)) ((in X0) Y))) ((in Y) X0)))))))) (x6:(forall (X0:fofType), (((in X0) X)->(((in X0) X0)->False))))=> ((x6 A) x0)))))))) as proof of ((ordinal X)->(forall (A:fofType), (((in A) X)->(not ((in A) A)))))
% Found (fun (X:fofType) (x:(ordinal X)) (A:fofType) (x0:((in A) X))=> (((fun (P:Type) (x1:((transitiveset X)->((wellorderedByIn X)->P)))=> (((((and_rect (transitiveset X)) (wellorderedByIn X)) P) x1) x)) (not ((in A) A))) (fun (x1:(transitiveset X)) (x2:(wellorderedByIn X))=> (((fun (P:Type) (x3:((stricttotalorderedByIn X)->((forall (X0:fofType), (((in X0) (powerset X))->((nonempty X0)->((ex fofType) (fun (Xx:fofType)=> ((and ((in Xx) X0)) (forall (Y:fofType), (((in Y) X0)->((or (((eq fofType) Xx) Y)) ((in Xx) Y))))))))))->P)))=> (((((and_rect (stricttotalorderedByIn X)) (forall (X0:fofType), (((in X0) (powerset X))->((nonempty X0)->((ex fofType) (fun (Xx:fofType)=> ((and ((in Xx) X0)) (forall (Y:fofType), (((in Y) X0)->((or (((eq fofType) Xx) Y)) ((in Xx) Y))))))))))) P) x3) x2)) (not ((in A) A))) (fun (x3:(stricttotalorderedByIn X)) (x4:(forall (X0:fofType), (((in X0) (powerset X))->((nonempty X0)->((ex fofType) (fun (Xx:fofType)=> ((and ((in Xx) X0)) (forall (Y:fofType), (((in Y) X0)->((or (((eq fofType) Xx) Y)) ((in Xx) Y)))))))))))=> (((fun (P:Type) (x5:(((and (forall (Xx:fofType), (((in Xx) X)->(forall (X0:fofType), (((in X0) X)->(forall (Y:fofType), (((in Y) X)->(((and ((in Xx) X0)) ((in X0) Y))->((in Xx) Y))))))))) (forall (X0:fofType), (((in X0) X)->(forall (Y:fofType), (((in Y) X)->((or ((or (((eq fofType) X0) Y)) ((in X0) Y))) ((in Y) X0)))))))->((forall (X0:fofType), (((in X0) X)->(((in X0) X0)->False)))->P)))=> (((((and_rect ((and (forall (Xx:fofType), (((in Xx) X)->(forall (X0:fofType), (((in X0) X)->(forall (Y:fofType), (((in Y) X)->(((and ((in Xx) X0)) ((in X0) Y))->((in Xx) Y))))))))) (forall (X0:fofType), (((in X0) X)->(forall (Y:fofType), (((in Y) X)->((or ((or (((eq fofType) X0) Y)) ((in X0) Y))) ((in Y) X0)))))))) (forall (X0:fofType), (((in X0) X)->(((in X0) X0)->False)))) P) x5) x3)) (not ((in A) A))) (fun (x5:((and (forall (Xx:fofType), (((in Xx) X)->(forall (X0:fofType), (((in X0) X)->(forall (Y:fofType), (((in Y) X)->(((and ((in Xx) X0)) ((in X0) Y))->((in Xx) Y))))))))) (forall (X0:fofType), (((in X0) X)->(forall (Y:fofType), (((in Y) X)->((or ((or (((eq fofType) X0) Y)) ((in X0) Y))) ((in Y) X0)))))))) (x6:(forall (X0:fofType), (((in X0) X)->(((in X0) X0)->False))))=> ((x6 A) x0)))))))) as proof of (forall (X:fofType), ((ordinal X)->(forall (A:fofType), (((in A) X)->(not ((in A) A))))))
% Found (fun (X:fofType) (x:(ordinal X)) (A:fofType) (x0:((in A) X))=> (((fun (P:Type) (x1:((transitiveset X)->((wellorderedByIn X)->P)))=> (((((and_rect (transitiveset X)) (wellorderedByIn X)) P) x1) x)) (not ((in A) A))) (fun (x1:(transitiveset X)) (x2:(wellorderedByIn X))=> (((fun (P:Type) (x3:((stricttotalorderedByIn X)->((forall (X0:fofType), (((in X0) (powerset X))->((nonempty X0)->((ex fofType) (fun (Xx:fofType)=> ((and ((in Xx) X0)) (forall (Y:fofType), (((in Y) X0)->((or (((eq fofType) Xx) Y)) ((in Xx) Y))))))))))->P)))=> (((((and_rect (stricttotalorderedByIn X)) (forall (X0:fofType), (((in X0) (powerset X))->((nonempty X0)->((ex fofType) (fun (Xx:fofType)=> ((and ((in Xx) X0)) (forall (Y:fofType), (((in Y) X0)->((or (((eq fofType) Xx) Y)) ((in Xx) Y))))))))))) P) x3) x2)) (not ((in A) A))) (fun (x3:(stricttotalorderedByIn X)) (x4:(forall (X0:fofType), (((in X0) (powerset X))->((nonempty X0)->((ex fofType) (fun (Xx:fofType)=> ((and ((in Xx) X0)) (forall (Y:fofType), (((in Y) X0)->((or (((eq fofType) Xx) Y)) ((in Xx) Y)))))))))))=> (((fun (P:Type) (x5:(((and (forall (Xx:fofType), (((in Xx) X)->(forall (X0:fofType), (((in X0) X)->(forall (Y:fofType), (((in Y) X)->(((and ((in Xx) X0)) ((in X0) Y))->((in Xx) Y))))))))) (forall (X0:fofType), (((in X0) X)->(forall (Y:fofType), (((in Y) X)->((or ((or (((eq fofType) X0) Y)) ((in X0) Y))) ((in Y) X0)))))))->((forall (X0:fofType), (((in X0) X)->(((in X0) X0)->False)))->P)))=> (((((and_rect ((and (forall (Xx:fofType), (((in Xx) X)->(forall (X0:fofType), (((in X0) X)->(forall (Y:fofType), (((in Y) X)->(((and ((in Xx) X0)) ((in X0) Y))->((in Xx) Y))))))))) (forall (X0:fofType), (((in X0) X)->(forall (Y:fofType), (((in Y) X)->((or ((or (((eq fofType) X0) Y)) ((in X0) Y))) ((in Y) X0)))))))) (forall (X0:fofType), (((in X0) X)->(((in X0) X0)->False)))) P) x5) x3)) (not ((in A) A))) (fun (x5:((and (forall (Xx:fofType), (((in Xx) X)->(forall (X0:fofType), (((in X0) X)->(forall (Y:fofType), (((in Y) X)->(((and ((in Xx) X0)) ((in X0) Y))->((in Xx) Y))))))))) (forall (X0:fofType), (((in X0) X)->(forall (Y:fofType), (((in Y) X)->((or ((or (((eq fofType) X0) Y)) ((in X0) Y))) ((in Y) X0)))))))) (x6:(forall (X0:fofType), (((in X0) X)->(((in X0) X0)->False))))=> ((x6 A) x0)))))))) as proof of (forall (X:fofType), ((ordinal X)->(forall (A:fofType), (((in A) X)->(((in A) A)->False)))))
% Got proof (fun (X:fofType) (x:(ordinal X)) (A:fofType) (x0:((in A) X))=> (((fun (P:Type) (x1:((transitiveset X)->((wellorderedByIn X)->P)))=> (((((and_rect (transitiveset X)) (wellorderedByIn X)) P) x1) x)) (not ((in A) A))) (fun (x1:(transitiveset X)) (x2:(wellorderedByIn X))=> (((fun (P:Type) (x3:((stricttotalorderedByIn X)->((forall (X0:fofType), (((in X0) (powerset X))->((nonempty X0)->((ex fofType) (fun (Xx:fofType)=> ((and ((in Xx) X0)) (forall (Y:fofType), (((in Y) X0)->((or (((eq fofType) Xx) Y)) ((in Xx) Y))))))))))->P)))=> (((((and_rect (stricttotalorderedByIn X)) (forall (X0:fofType), (((in X0) (powerset X))->((nonempty X0)->((ex fofType) (fun (Xx:fofType)=> ((and ((in Xx) X0)) (forall (Y:fofType), (((in Y) X0)->((or (((eq fofType) Xx) Y)) ((in Xx) Y))))))))))) P) x3) x2)) (not ((in A) A))) (fun (x3:(stricttotalorderedByIn X)) (x4:(forall (X0:fofType), (((in X0) (powerset X))->((nonempty X0)->((ex fofType) (fun (Xx:fofType)=> ((and ((in Xx) X0)) (forall (Y:fofType), (((in Y) X0)->((or (((eq fofType) Xx) Y)) ((in Xx) Y)))))))))))=> (((fun (P:Type) (x5:(((and (forall (Xx:fofType), (((in Xx) X)->(forall (X0:fofType), (((in X0) X)->(forall (Y:fofType), (((in Y) X)->(((and ((in Xx) X0)) ((in X0) Y))->((in Xx) Y))))))))) (forall (X0:fofType), (((in X0) X)->(forall (Y:fofType), (((in Y) X)->((or ((or (((eq fofType) X0) Y)) ((in X0) Y))) ((in Y) X0)))))))->((forall (X0:fofType), (((in X0) X)->(((in X0) X0)->False)))->P)))=> (((((and_rect ((and (forall (Xx:fofType), (((in Xx) X)->(forall (X0:fofType), (((in X0) X)->(forall (Y:fofType), (((in Y) X)->(((and ((in Xx) X0)) ((in X0) Y))->((in Xx) Y))))))))) (forall (X0:fofType), (((in X0) X)->(forall (Y:fofType), (((in Y) X)->((or ((or (((eq fofType) X0) Y)) ((in X0) Y))) ((in Y) X0)))))))) (forall (X0:fofType), (((in X0) X)->(((in X0) X0)->False)))) P) x5) x3)) (not ((in A) A))) (fun (x5:((and (forall (Xx:fofType), (((in Xx) X)->(forall (X0:fofType), (((in X0) X)->(forall (Y:fofType), (((in Y) X)->(((and ((in Xx) X0)) ((in X0) Y))->((in Xx) Y))))))))) (forall (X0:fofType), (((in X0) X)->(forall (Y:fofType), (((in Y) X)->((or ((or (((eq fofType) X0) Y)) ((in X0) Y))) ((in Y) X0)))))))) (x6:(forall (X0:fofType), (((in X0) X)->(((in X0) X0)->False))))=> ((x6 A) x0))))))))
% Time elapsed = 1.706513s
% node=133 cost=535.000000 depth=25
% ::::::::::::::::::::::
% % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% (fun (X:fofType) (x:(ordinal X)) (A:fofType) (x0:((in A) X))=> (((fun (P:Type) (x1:((transitiveset X)->((wellorderedByIn X)->P)))=> (((((and_rect (transitiveset X)) (wellorderedByIn X)) P) x1) x)) (not ((in A) A))) (fun (x1:(transitiveset X)) (x2:(wellorderedByIn X))=> (((fun (P:Type) (x3:((stricttotalorderedByIn X)->((forall (X0:fofType), (((in X0) (powerset X))->((nonempty X0)->((ex fofType) (fun (Xx:fofType)=> ((and ((in Xx) X0)) (forall (Y:fofType), (((in Y) X0)->((or (((eq fofType) Xx) Y)) ((in Xx) Y))))))))))->P)))=> (((((and_rect (stricttotalorderedByIn X)) (forall (X0:fofType), (((in X0) (powerset X))->((nonempty X0)->((ex fofType) (fun (Xx:fofType)=> ((and ((in Xx) X0)) (forall (Y:fofType), (((in Y) X0)->((or (((eq fofType) Xx) Y)) ((in Xx) Y))))))))))) P) x3) x2)) (not ((in A) A))) (fun (x3:(stricttotalorderedByIn X)) (x4:(forall (X0:fofType), (((in X0) (powerset X))->((nonempty X0)->((ex fofType) (fun (Xx:fofType)=> ((and ((in Xx) X0)) (forall (Y:fofType), (((in Y) X0)->((or (((eq fofType) Xx) Y)) ((in Xx) Y)))))))))))=> (((fun (P:Type) (x5:(((and (forall (Xx:fofType), (((in Xx) X)->(forall (X0:fofType), (((in X0) X)->(forall (Y:fofType), (((in Y) X)->(((and ((in Xx) X0)) ((in X0) Y))->((in Xx) Y))))))))) (forall (X0:fofType), (((in X0) X)->(forall (Y:fofType), (((in Y) X)->((or ((or (((eq fofType) X0) Y)) ((in X0) Y))) ((in Y) X0)))))))->((forall (X0:fofType), (((in X0) X)->(((in X0) X0)->False)))->P)))=> (((((and_rect ((and (forall (Xx:fofType), (((in Xx) X)->(forall (X0:fofType), (((in X0) X)->(forall (Y:fofType), (((in Y) X)->(((and ((in Xx) X0)) ((in X0) Y))->((in Xx) Y))))))))) (forall (X0:fofType), (((in X0) X)->(forall (Y:fofType), (((in Y) X)->((or ((or (((eq fofType) X0) Y)) ((in X0) Y))) ((in Y) X0)))))))) (forall (X0:fofType), (((in X0) X)->(((in X0) X0)->False)))) P) x5) x3)) (not ((in A) A))) (fun (x5:((and (forall (Xx:fofType), (((in Xx) X)->(forall (X0:fofType), (((in X0) X)->(forall (Y:fofType), (((in Y) X)->(((and ((in Xx) X0)) ((in X0) Y))->((in Xx) Y))))))))) (forall (X0:fofType), (((in X0) X)->(forall (Y:fofType), (((in Y) X)->((or ((or (((eq fofType) X0) Y)) ((in X0) Y))) ((in Y) X0)))))))) (x6:(forall (X0:fofType), (((in X0) X)->(((in X0) X0)->False))))=> ((x6 A) x0))))))))
% % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% EOF
%------------------------------------------------------------------------------