%------------------------------------------------------------------------------ % File : cocATP---0.2.0 % Problem : NUM705^1 : TPTP v7.0.0. Released v3.7.0. % Transfm : none % Format : tptp:raw % Command : python CASC.py /export/starexec/sandbox/benchmark/theBenchmark.p % Computer : n098.star.cs.uiowa.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2609 0 2.40GHz % Memory : 32218.625MB % OS : Linux 3.10.0-693.2.2.el7.x86_64 % CPULimit : 300s % DateTime : Mon Jan 8 13:11:31 EST 2018 % Result : Timeout 293.16s % Output : None % Verified : % SZS Type : None (Parsing solution fails) % Syntax : Number of formulae : 0 % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : NUM705^1 : TPTP v7.0.0. Released v3.7.0. % 0.00/0.04 % Command : python CASC.py /export/starexec/sandbox/benchmark/theBenchmark.p % 0.03/0.23 % Computer : n098.star.cs.uiowa.edu % 0.03/0.23 % Model : x86_64 x86_64 % 0.03/0.23 % CPU : Intel(R) Xeon(R) CPU E5-2609 0 @ 2.40GHz % 0.03/0.23 % Memory : 32218.625MB % 0.03/0.23 % OS : Linux 3.10.0-693.2.2.el7.x86_64 % 0.03/0.23 % CPULimit : 300 % 0.03/0.23 % DateTime : Fri Jan 5 13:11:21 CST 2018 % 0.03/0.23 % CPUTime : % 0.03/0.27 Python 2.7.13 % 0.84/1.23 Using paths ['/home/cristobal/cocATP/CASC/TPTP/', '/export/starexec/sandbox/benchmark/', '/export/starexec/sandbox/benchmark/'] % 0.84/1.23 FOF formula (<kernel.Constant object at 0x2b389f9321b8>, <kernel.Type object at 0x2b389fc8b200>) of role type named nat_type % 0.84/1.23 Using role type % 0.84/1.23 Declaring nat:Type % 0.84/1.23 FOF formula (<kernel.Constant object at 0x2b389f932638>, <kernel.DependentProduct object at 0x2b389fc8bb90>) of role type named p % 0.84/1.23 Using role type % 0.84/1.23 Declaring p:(nat->Prop) % 0.84/1.23 FOF formula (<kernel.Constant object at 0x2b389f9320e0>, <kernel.DependentProduct object at 0x2b389fc8bf80>) of role type named some % 0.84/1.23 Using role type % 0.84/1.23 Declaring some:((nat->Prop)->Prop) % 0.84/1.23 FOF formula (some p) of role axiom named s % 0.84/1.23 A new axiom: (some p) % 0.84/1.23 FOF formula (<kernel.Constant object at 0x2b389f9321b8>, <kernel.DependentProduct object at 0x2b389fc8bfc8>) of role type named lessis % 0.84/1.23 Using role type % 0.84/1.23 Declaring lessis:(nat->(nat->Prop)) % 0.84/1.23 FOF formula (<kernel.Constant object at 0x2b389f9321b8>, <kernel.DependentProduct object at 0x2b389fc8bbd8>) of role type named more % 0.84/1.23 Using role type % 0.84/1.23 Declaring more:(nat->(nat->Prop)) % 0.84/1.23 FOF formula (forall (Xx:nat) (Xy:nat), (((lessis Xx) Xy)->((((more Xy) Xx)->False)->(((eq nat) Xy) Xx)))) of role axiom named satz14 % 0.84/1.23 A new axiom: (forall (Xx:nat) (Xy:nat), (((lessis Xx) Xy)->((((more Xy) Xx)->False)->(((eq nat) Xy) Xx)))) % 0.84/1.23 FOF formula (forall (Xa:Prop), (((Xa->False)->False)->Xa)) of role axiom named et % 0.84/1.23 A new axiom: (forall (Xa:Prop), (((Xa->False)->False)->Xa)) % 0.84/1.23 FOF formula (forall (Xx:nat) (Xy:nat), (((lessis Xx) Xy)->(((more Xx) Xy)->False))) of role axiom named satz10d % 0.84/1.23 A new axiom: (forall (Xx:nat) (Xy:nat), (((lessis Xx) Xy)->(((more Xx) Xy)->False))) % 0.84/1.23 FOF formula (forall (Xp:(nat->Prop)), ((some Xp)->(some (fun (Xx:nat)=> (((forall (Xx_0:nat), ((Xp Xx_0)->((lessis Xx) Xx_0)))->((Xp Xx)->False))->False))))) of role axiom named satz27 % 0.84/1.23 A new axiom: (forall (Xp:(nat->Prop)), ((some Xp)->(some (fun (Xx:nat)=> (((forall (Xx_0:nat), ((Xp Xx_0)->((lessis Xx) Xx_0)))->((Xp Xx)->False))->False))))) % 0.84/1.23 FOF formula (((forall (Xx:nat) (Xy:nat), ((((forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))->((p Xx)->False))->False)->((((forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))->((p Xy)->False))->False)->(((eq nat) Xx) Xy))))->((some (fun (Xx:nat)=> (((forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))->((p Xx)->False))->False)))->False))->False) of role conjecture named satz27a % 0.84/1.23 Conjecture to prove = (((forall (Xx:nat) (Xy:nat), ((((forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))->((p Xx)->False))->False)->((((forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))->((p Xy)->False))->False)->(((eq nat) Xx) Xy))))->((some (fun (Xx:nat)=> (((forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))->((p Xx)->False))->False)))->False))->False):Prop % 0.84/1.23 Parameter nat_DUMMY:nat. % 0.84/1.23 We need to prove ['(((forall (Xx:nat) (Xy:nat), ((((forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))->((p Xx)->False))->False)->((((forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))->((p Xy)->False))->False)->(((eq nat) Xx) Xy))))->((some (fun (Xx:nat)=> (((forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))->((p Xx)->False))->False)))->False))->False)'] % 0.84/1.23 Parameter nat:Type. % 0.84/1.23 Parameter p:(nat->Prop). % 0.84/1.23 Parameter some:((nat->Prop)->Prop). % 0.84/1.23 Axiom s:(some p). % 0.84/1.23 Parameter lessis:(nat->(nat->Prop)). % 0.84/1.23 Parameter more:(nat->(nat->Prop)). % 0.84/1.23 Axiom satz14:(forall (Xx:nat) (Xy:nat), (((lessis Xx) Xy)->((((more Xy) Xx)->False)->(((eq nat) Xy) Xx)))). % 0.84/1.23 Axiom et:(forall (Xa:Prop), (((Xa->False)->False)->Xa)). % 0.84/1.23 Axiom satz10d:(forall (Xx:nat) (Xy:nat), (((lessis Xx) Xy)->(((more Xx) Xy)->False))). % 0.84/1.23 Axiom satz27:(forall (Xp:(nat->Prop)), ((some Xp)->(some (fun (Xx:nat)=> (((forall (Xx_0:nat), ((Xp Xx_0)->((lessis Xx) Xx_0)))->((Xp Xx)->False))->False))))). % 0.84/1.23 Trying to prove (((forall (Xx:nat) (Xy:nat), ((((forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))->((p Xx)->False))->False)->((((forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))->((p Xy)->False))->False)->(((eq nat) Xx) Xy))))->((some (fun (Xx:nat)=> (((forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))->((p Xx)->False))->False)))->False))->False) % 0.84/1.23 Found satz2700:=(satz270 s):(some (fun (Xx:nat)=> (((forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))->((p Xx)->False))->False))) % 19.14/19.56 Found (satz270 s) as proof of (some (fun (Xx:nat)=> (((forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))->((p Xx)->False))->False))) % 19.14/19.56 Found ((satz27 p) s) as proof of (some (fun (Xx:nat)=> (((forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))->((p Xx)->False))->False))) % 19.14/19.56 Found ((satz27 p) s) as proof of (some (fun (Xx:nat)=> (((forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))->((p Xx)->False))->False))) % 19.14/19.56 Found satz2700:=(satz270 s):(some (fun (Xx:nat)=> (((forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))->((p Xx)->False))->False))) % 19.14/19.56 Found (satz270 s) as proof of (some (fun (Xx:nat)=> (((forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))->((p Xx)->False))->False))) % 19.14/19.56 Found ((satz27 p) s) as proof of (some (fun (Xx:nat)=> (((forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))->((p Xx)->False))->False))) % 19.14/19.56 Found ((satz27 p) s) as proof of (some (fun (Xx:nat)=> (((forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))->((p Xx)->False))->False))) % 19.14/19.56 Found eq_ref000:=(eq_ref00 P):((P Xx)->(P Xx)) % 19.14/19.56 Found (eq_ref00 P) as proof of (P0 Xx) % 19.14/19.56 Found ((eq_ref0 Xx) P) as proof of (P0 Xx) % 19.14/19.56 Found (((eq_ref nat) Xx) P) as proof of (P0 Xx) % 19.14/19.56 Found (((eq_ref nat) Xx) P) as proof of (P0 Xx) % 19.14/19.56 Found eq_ref000:=(eq_ref00 P):((P Xx)->(P Xx)) % 19.14/19.56 Found (eq_ref00 P) as proof of (P0 Xx) % 19.14/19.56 Found ((eq_ref0 Xx) P) as proof of (P0 Xx) % 19.14/19.56 Found (((eq_ref nat) Xx) P) as proof of (P0 Xx) % 19.14/19.56 Found (((eq_ref nat) Xx) P) as proof of (P0 Xx) % 19.14/19.56 Found eq_ref000:=(eq_ref00 P):((P Xx)->(P Xx)) % 19.14/19.56 Found (eq_ref00 P) as proof of (P0 Xx) % 19.14/19.56 Found ((eq_ref0 Xx) P) as proof of (P0 Xx) % 19.14/19.56 Found (((eq_ref nat) Xx) P) as proof of (P0 Xx) % 19.14/19.56 Found (((eq_ref nat) Xx) P) as proof of (P0 Xx) % 19.14/19.56 Found eq_ref000:=(eq_ref00 P):((P Xx)->(P Xx)) % 19.14/19.56 Found (eq_ref00 P) as proof of (P0 Xx) % 19.14/19.56 Found ((eq_ref0 Xx) P) as proof of (P0 Xx) % 19.14/19.56 Found (((eq_ref nat) Xx) P) as proof of (P0 Xx) % 19.14/19.56 Found (((eq_ref nat) Xx) P) as proof of (P0 Xx) % 19.14/19.56 Found eq_ref00:=(eq_ref0 Xx):(((eq nat) Xx) Xx) % 19.14/19.56 Found (eq_ref0 Xx) as proof of (((eq nat) Xx) b) % 19.14/19.56 Found ((eq_ref nat) Xx) as proof of (((eq nat) Xx) b) % 19.14/19.56 Found ((eq_ref nat) Xx) as proof of (((eq nat) Xx) b) % 19.14/19.56 Found ((eq_ref nat) Xx) as proof of (((eq nat) Xx) b) % 19.14/19.56 Found eq_ref00:=(eq_ref0 b):(((eq nat) b) b) % 19.14/19.56 Found (eq_ref0 b) as proof of (((eq nat) b) Xy) % 19.14/19.56 Found ((eq_ref nat) b) as proof of (((eq nat) b) Xy) % 19.14/19.56 Found ((eq_ref nat) b) as proof of (((eq nat) b) Xy) % 19.14/19.56 Found ((eq_ref nat) b) as proof of (((eq nat) b) Xy) % 19.14/19.56 Found eq_ref000:=(eq_ref00 P):((P Xy)->(P Xy)) % 19.14/19.56 Found (eq_ref00 P) as proof of (P0 Xy) % 19.14/19.56 Found ((eq_ref0 Xy) P) as proof of (P0 Xy) % 19.14/19.56 Found (((eq_ref nat) Xy) P) as proof of (P0 Xy) % 19.14/19.56 Found (((eq_ref nat) Xy) P) as proof of (P0 Xy) % 19.14/19.56 Found eq_ref00:=(eq_ref0 Xx):(((eq nat) Xx) Xx) % 19.14/19.56 Found (eq_ref0 Xx) as proof of (((eq nat) Xx) b) % 19.14/19.56 Found ((eq_ref nat) Xx) as proof of (((eq nat) Xx) b) % 19.14/19.56 Found ((eq_ref nat) Xx) as proof of (((eq nat) Xx) b) % 19.14/19.56 Found ((eq_ref nat) Xx) as proof of (((eq nat) Xx) b) % 19.14/19.56 Found eq_ref00:=(eq_ref0 b):(((eq nat) b) b) % 19.14/19.56 Found (eq_ref0 b) as proof of (((eq nat) b) Xy) % 19.14/19.56 Found ((eq_ref nat) b) as proof of (((eq nat) b) Xy) % 19.14/19.56 Found ((eq_ref nat) b) as proof of (((eq nat) b) Xy) % 19.14/19.56 Found ((eq_ref nat) b) as proof of (((eq nat) b) Xy) % 19.14/19.56 Found x2:((more Xx) Xy) % 19.14/19.56 Found x2 as proof of ((more Xx) Xy) % 19.14/19.56 Found x00:False % 19.14/19.56 Found (fun (x1:(((((forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))->((p Xy)->False))->False)->(((eq nat) Xx) Xy))->False))=> x00) as proof of False % 19.14/19.56 Found (fun (x1:(((((forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))->((p Xy)->False))->False)->(((eq nat) Xx) Xy))->False))=> x00) as proof of ((((((forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))->((p Xy)->False))->False)->(((eq nat) Xx) Xy))->False)->False) % 19.14/19.56 Found x10:False % 19.14/19.56 Found (fun (x2:((((eq nat) Xx) Xy)->False))=> x10) as proof of False % 19.14/19.56 Found (fun (x2:((((eq nat) Xx) Xy)->False))=> x10) as proof of (((((eq nat) Xx) Xy)->False)->False) % 19.14/19.56 Found x00:False % 19.14/19.56 Found (fun (x2:((((eq nat) Xx) Xy)->False))=> x00) as proof of False % 19.14/19.56 Found (fun (x2:((((eq nat) Xx) Xy)->False))=> x00) as proof of (((((eq nat) Xx) Xy)->False)->False) % 19.14/19.56 Found eq_ref000:=(eq_ref00 P):((P Xy)->(P Xy)) % 30.44/30.82 Found (eq_ref00 P) as proof of (P0 Xy) % 30.44/30.82 Found ((eq_ref0 Xy) P) as proof of (P0 Xy) % 30.44/30.82 Found (((eq_ref nat) Xy) P) as proof of (P0 Xy) % 30.44/30.82 Found (((eq_ref nat) Xy) P) as proof of (P0 Xy) % 30.44/30.82 Found x00:False % 30.44/30.82 Found (fun (x2:(((P Xx)->(P Xy))->False))=> x00) as proof of False % 30.44/30.82 Found (fun (x2:(((P Xx)->(P Xy))->False))=> x00) as proof of ((((P Xx)->(P Xy))->False)->False) % 30.44/30.82 Found x10:False % 30.44/30.82 Found (fun (x2:(((P Xx)->(P Xy))->False))=> x10) as proof of False % 30.44/30.82 Found (fun (x2:(((P Xx)->(P Xy))->False))=> x10) as proof of ((((P Xx)->(P Xy))->False)->False) % 30.44/30.82 Found x3:((more Xx) Xy) % 30.44/30.82 Found x3 as proof of ((more Xx) Xy) % 30.44/30.82 Found eq_ref00:=(eq_ref0 b):(((eq nat) b) b) % 30.44/30.82 Found (eq_ref0 b) as proof of (((eq nat) b) Xx) % 30.44/30.82 Found ((eq_ref nat) b) as proof of (((eq nat) b) Xx) % 30.44/30.82 Found ((eq_ref nat) b) as proof of (((eq nat) b) Xx) % 30.44/30.82 Found ((eq_ref nat) b) as proof of (((eq nat) b) Xx) % 30.44/30.82 Found eq_ref00:=(eq_ref0 Xy):(((eq nat) Xy) Xy) % 30.44/30.82 Found (eq_ref0 Xy) as proof of (((eq nat) Xy) b) % 30.44/30.82 Found ((eq_ref nat) Xy) as proof of (((eq nat) Xy) b) % 30.44/30.82 Found ((eq_ref nat) Xy) as proof of (((eq nat) Xy) b) % 30.44/30.82 Found ((eq_ref nat) Xy) as proof of (((eq nat) Xy) b) % 30.44/30.82 Found x00:False % 30.44/30.82 Found (fun (x3:((P Xy)->False))=> x00) as proof of False % 30.44/30.82 Found (fun (x3:((P Xy)->False))=> x00) as proof of (((P Xy)->False)->False) % 30.44/30.82 Found x10:False % 30.44/30.82 Found (fun (x3:((P Xy)->False))=> x10) as proof of False % 30.44/30.82 Found (fun (x3:((P Xy)->False))=> x10) as proof of (((P Xy)->False)->False) % 30.44/30.82 Found x00:False % 30.44/30.82 Found (fun (x1:(((((forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))->((p Xy)->False))->False)->(((eq nat) Xx) Xy))->False))=> x00) as proof of False % 30.44/30.82 Found (fun (x1:(((((forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))->((p Xy)->False))->False)->(((eq nat) Xx) Xy))->False))=> x00) as proof of ((((((forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))->((p Xy)->False))->False)->(((eq nat) Xx) Xy))->False)->False) % 30.44/30.82 Found (et0 (fun (x1:(((((forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))->((p Xy)->False))->False)->(((eq nat) Xx) Xy))->False))=> x00)) as proof of ((((forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))->((p Xy)->False))->False)->(((eq nat) Xx) Xy)) % 30.44/30.82 Found ((et ((((forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))->((p Xy)->False))->False)->(((eq nat) Xx) Xy))) (fun (x1:(((((forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))->((p Xy)->False))->False)->(((eq nat) Xx) Xy))->False))=> x00)) as proof of ((((forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))->((p Xy)->False))->False)->(((eq nat) Xx) Xy)) % 30.44/30.82 Found ((et ((((forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))->((p Xy)->False))->False)->(((eq nat) Xx) Xy))) (fun (x1:(((((forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))->((p Xy)->False))->False)->(((eq nat) Xx) Xy))->False))=> x00)) as proof of ((((forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))->((p Xy)->False))->False)->(((eq nat) Xx) Xy)) % 30.44/30.82 Found x10:False % 30.44/30.82 Found (fun (x4:(p Xx))=> x10) as proof of False % 30.44/30.82 Found (fun (x4:(p Xx))=> x10) as proof of ((p Xx)->False) % 30.44/30.82 Found x00:False % 30.44/30.82 Found (fun (x4:(p Xy))=> x00) as proof of False % 30.44/30.82 Found (fun (x4:(p Xy))=> x00) as proof of ((p Xy)->False) % 30.44/30.82 Found x00:False % 30.44/30.82 Found (fun (x2:((((eq nat) Xx) Xy)->False))=> x00) as proof of False % 30.44/30.82 Found (fun (x2:((((eq nat) Xx) Xy)->False))=> x00) as proof of (((((eq nat) Xx) Xy)->False)->False) % 30.44/30.82 Found (et0 (fun (x2:((((eq nat) Xx) Xy)->False))=> x00)) as proof of (((eq nat) Xx) Xy) % 30.44/30.82 Found ((et (((eq nat) Xx) Xy)) (fun (x2:((((eq nat) Xx) Xy)->False))=> x00)) as proof of (((eq nat) Xx) Xy) % 30.44/30.82 Found ((et (((eq nat) Xx) Xy)) (fun (x2:((((eq nat) Xx) Xy)->False))=> x00)) as proof of (((eq nat) Xx) Xy) % 30.44/30.82 Found x10:False % 30.44/30.82 Found (fun (x2:((((eq nat) Xx) Xy)->False))=> x10) as proof of False % 30.44/30.82 Found (fun (x2:((((eq nat) Xx) Xy)->False))=> x10) as proof of (((((eq nat) Xx) Xy)->False)->False) % 30.44/30.82 Found (et0 (fun (x2:((((eq nat) Xx) Xy)->False))=> x10)) as proof of (((eq nat) Xx) Xy) % 30.44/30.82 Found ((et (((eq nat) Xx) Xy)) (fun (x2:((((eq nat) Xx) Xy)->False))=> x10)) as proof of (((eq nat) Xx) Xy) % 30.44/30.82 Found ((et (((eq nat) Xx) Xy)) (fun (x2:((((eq nat) Xx) Xy)->False))=> x10)) as proof of (((eq nat) Xx) Xy) % 30.44/30.82 Found x00:False % 30.44/30.82 Found (fun (x4:(p Xy))=> x00) as proof of False % 37.83/38.25 Found (fun (x4:(p Xy))=> x00) as proof of ((p Xy)->False) % 37.83/38.25 Found x10:False % 37.83/38.25 Found (fun (x4:(p Xx))=> x10) as proof of False % 37.83/38.25 Found (fun (x4:(p Xx))=> x10) as proof of ((p Xx)->False) % 37.83/38.25 Found x10:False % 37.83/38.25 Found (fun (x4:(p Xx))=> x10) as proof of False % 37.83/38.25 Found (fun (x3:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))) (x4:(p Xx))=> x10) as proof of ((p Xx)->False) % 37.83/38.25 Found (fun (x3:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))) (x4:(p Xx))=> x10) as proof of ((forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))->((p Xx)->False)) % 37.83/38.25 Found x00:False % 37.83/38.25 Found (fun (x4:(p Xy))=> x00) as proof of False % 37.83/38.25 Found (fun (x3:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))) (x4:(p Xy))=> x00) as proof of ((p Xy)->False) % 37.83/38.25 Found (fun (x3:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))) (x4:(p Xy))=> x00) as proof of ((forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))->((p Xy)->False)) % 37.83/38.25 Found x2:((more Xx) Xy) % 37.83/38.25 Found x2 as proof of ((more Xx) Xy) % 37.83/38.25 Found x2:((more Xx) Xy) % 37.83/38.25 Found x2 as proof of ((more Xx) Xy) % 37.83/38.25 Found x00:False % 37.83/38.25 Found (fun (x2:(((P Xx)->(P Xy))->False))=> x00) as proof of False % 37.83/38.25 Found (fun (x2:(((P Xx)->(P Xy))->False))=> x00) as proof of ((((P Xx)->(P Xy))->False)->False) % 37.83/38.25 Found (et0 (fun (x2:(((P Xx)->(P Xy))->False))=> x00)) as proof of ((P Xx)->(P Xy)) % 37.83/38.25 Found ((et ((P Xx)->(P Xy))) (fun (x2:(((P Xx)->(P Xy))->False))=> x00)) as proof of ((P Xx)->(P Xy)) % 37.83/38.25 Found ((et ((P Xx)->(P Xy))) (fun (x2:(((P Xx)->(P Xy))->False))=> x00)) as proof of ((P Xx)->(P Xy)) % 37.83/38.25 Found x10:False % 37.83/38.25 Found (fun (x2:(((P Xx)->(P Xy))->False))=> x10) as proof of False % 37.83/38.25 Found (fun (x2:(((P Xx)->(P Xy))->False))=> x10) as proof of ((((P Xx)->(P Xy))->False)->False) % 37.83/38.25 Found (et0 (fun (x2:(((P Xx)->(P Xy))->False))=> x10)) as proof of ((P Xx)->(P Xy)) % 37.83/38.25 Found ((et ((P Xx)->(P Xy))) (fun (x2:(((P Xx)->(P Xy))->False))=> x10)) as proof of ((P Xx)->(P Xy)) % 37.83/38.25 Found ((et ((P Xx)->(P Xy))) (fun (x2:(((P Xx)->(P Xy))->False))=> x10)) as proof of ((P Xx)->(P Xy)) % 37.83/38.25 Found x10:False % 37.83/38.25 Found (fun (x5:(p Xx))=> x10) as proof of False % 37.83/38.25 Found (fun (x5:(p Xx))=> x10) as proof of ((p Xx)->False) % 37.83/38.25 Found x00:False % 37.83/38.25 Found (fun (x5:(p Xy))=> x00) as proof of False % 37.83/38.25 Found (fun (x5:(p Xy))=> x00) as proof of ((p Xy)->False) % 37.83/38.25 Found x00:False % 37.83/38.25 Found (fun (x4:(p Xy))=> x00) as proof of False % 37.83/38.25 Found (fun (x3:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))) (x4:(p Xy))=> x00) as proof of ((p Xy)->False) % 37.83/38.25 Found (fun (x3:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))) (x4:(p Xy))=> x00) as proof of ((forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))->((p Xy)->False)) % 37.83/38.25 Found x10:False % 37.83/38.25 Found (fun (x4:(p Xx))=> x10) as proof of False % 37.83/38.25 Found (fun (x3:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))) (x4:(p Xx))=> x10) as proof of ((p Xx)->False) % 37.83/38.25 Found (fun (x3:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))) (x4:(p Xx))=> x10) as proof of ((forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))->((p Xx)->False)) % 37.83/38.25 Found x10:False % 37.83/38.25 Found (fun (x3:((P Xy)->False))=> x10) as proof of False % 37.83/38.25 Found (fun (x3:((P Xy)->False))=> x10) as proof of (((P Xy)->False)->False) % 37.83/38.25 Found (et0 (fun (x3:((P Xy)->False))=> x10)) as proof of (P Xy) % 37.83/38.25 Found ((et (P Xy)) (fun (x3:((P Xy)->False))=> x10)) as proof of (P Xy) % 37.83/38.25 Found ((et (P Xy)) (fun (x3:((P Xy)->False))=> x10)) as proof of (P Xy) % 37.83/38.25 Found x00:False % 37.83/38.25 Found (fun (x3:((P Xy)->False))=> x00) as proof of False % 37.83/38.25 Found (fun (x3:((P Xy)->False))=> x00) as proof of (((P Xy)->False)->False) % 37.83/38.25 Found (et0 (fun (x3:((P Xy)->False))=> x00)) as proof of (P Xy) % 37.83/38.25 Found ((et (P Xy)) (fun (x3:((P Xy)->False))=> x00)) as proof of (P Xy) % 37.83/38.25 Found ((et (P Xy)) (fun (x3:((P Xy)->False))=> x00)) as proof of (P Xy) % 37.83/38.25 Found eq_ref00:=(eq_ref0 Xy):(((eq nat) Xy) Xy) % 37.83/38.25 Found (eq_ref0 Xy) as proof of (((eq nat) Xy) b) % 37.83/38.25 Found ((eq_ref nat) Xy) as proof of (((eq nat) Xy) b) % 37.83/38.25 Found ((eq_ref nat) Xy) as proof of (((eq nat) Xy) b) % 37.83/38.25 Found ((eq_ref nat) Xy) as proof of (((eq nat) Xy) b) % 37.83/38.25 Found eq_ref00:=(eq_ref0 b):(((eq nat) b) b) % 37.83/38.25 Found (eq_ref0 b) as proof of (((eq nat) b) Xx) % 37.83/38.25 Found ((eq_ref nat) b) as proof of (((eq nat) b) Xx) % 37.83/38.25 Found ((eq_ref nat) b) as proof of (((eq nat) b) Xx) % 37.83/38.25 Found ((eq_ref nat) b) as proof of (((eq nat) b) Xx) % 59.61/60.08 Found x00:False % 59.61/60.08 Found (fun (x5:(p Xy))=> x00) as proof of False % 59.61/60.08 Found (fun (x4:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))) (x5:(p Xy))=> x00) as proof of ((p Xy)->False) % 59.61/60.08 Found (fun (x4:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))) (x5:(p Xy))=> x00) as proof of ((forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))->((p Xy)->False)) % 59.61/60.08 Found x10:False % 59.61/60.08 Found (fun (x5:(p Xx))=> x10) as proof of False % 59.61/60.08 Found (fun (x4:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))) (x5:(p Xx))=> x10) as proof of ((p Xx)->False) % 59.61/60.08 Found (fun (x4:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))) (x5:(p Xx))=> x10) as proof of ((forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))->((p Xx)->False)) % 59.61/60.08 Found x2:((more Xx) Xy) % 59.61/60.08 Found x2 as proof of ((more Xx) Xy) % 59.61/60.08 Found x2:((more Xx) Xy) % 59.61/60.08 Found x2 as proof of ((more Xx) Xy) % 59.61/60.08 Found x2:((more Xy) Xx) % 59.61/60.08 Found x2 as proof of ((more Xy) Xx) % 59.61/60.08 Found x2:((more Xx) Xy) % 59.61/60.08 Found x2 as proof of ((more Xx) Xy) % 59.61/60.08 Found x00:False % 59.61/60.08 Found (fun (x2:((more Xx) Xy))=> x00) as proof of False % 59.61/60.08 Found (fun (x2:((more Xx) Xy))=> x00) as proof of (((more Xx) Xy)->False) % 59.61/60.08 Found x10:False % 59.61/60.08 Found (fun (x2:((more Xx) Xy))=> x10) as proof of False % 59.61/60.08 Found (fun (x2:((more Xx) Xy))=> x10) as proof of (((more Xx) Xy)->False) % 59.61/60.08 Found x10:False % 59.61/60.08 Found (fun (x2:((((eq nat) Xy) Xx)->False))=> x10) as proof of False % 59.61/60.08 Found (fun (x2:((((eq nat) Xy) Xx)->False))=> x10) as proof of (((((eq nat) Xy) Xx)->False)->False) % 59.61/60.08 Found x00:False % 59.61/60.08 Found (fun (x2:((((eq nat) Xy) Xx)->False))=> x00) as proof of False % 59.61/60.08 Found (fun (x2:((((eq nat) Xy) Xx)->False))=> x00) as proof of (((((eq nat) Xy) Xx)->False)->False) % 59.61/60.08 Found x3:((more Xx) Xy) % 59.61/60.08 Found x3 as proof of ((more Xx) Xy) % 59.61/60.08 Found x3:((more Xx) Xy) % 59.61/60.08 Found x3 as proof of ((more Xx) Xy) % 59.61/60.08 Found x00:False % 59.61/60.08 Found (fun (x2:(((P Xy)->(P Xx))->False))=> x00) as proof of False % 59.61/60.08 Found (fun (x2:(((P Xy)->(P Xx))->False))=> x00) as proof of ((((P Xy)->(P Xx))->False)->False) % 59.61/60.08 Found x10:False % 59.61/60.08 Found (fun (x2:(((P Xy)->(P Xx))->False))=> x10) as proof of False % 59.61/60.08 Found (fun (x2:(((P Xy)->(P Xx))->False))=> x10) as proof of ((((P Xy)->(P Xx))->False)->False) % 59.61/60.08 Found satz2700:=(satz270 s):(some (fun (Xx:nat)=> (((forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))->((p Xx)->False))->False))) % 59.61/60.08 Found (satz270 s) as proof of (some (fun (Xx:nat)=> (((forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))->((p Xx)->False))->False))) % 59.61/60.08 Found ((satz27 p) s) as proof of (some (fun (Xx:nat)=> (((forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))->((p Xx)->False))->False))) % 59.61/60.08 Found ((satz27 p) s) as proof of (some (fun (Xx:nat)=> (((forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))->((p Xx)->False))->False))) % 59.61/60.08 Found x00:False % 59.61/60.08 Found (fun (x3:((P Xx)->False))=> x00) as proof of False % 59.61/60.08 Found (fun (x3:((P Xx)->False))=> x00) as proof of (((P Xx)->False)->False) % 59.61/60.08 Found x10:False % 59.61/60.08 Found (fun (x3:((P Xx)->False))=> x10) as proof of False % 59.61/60.08 Found (fun (x3:((P Xx)->False))=> x10) as proof of (((P Xx)->False)->False) % 59.61/60.08 Found x3:((more Xx) Xy) % 59.61/60.08 Found x3 as proof of ((more Xx) Xy) % 59.61/60.08 Found x3:((more Xx) Xy) % 59.61/60.08 Found x3 as proof of ((more Xx) Xy) % 59.61/60.08 Found x3:((more Xy) Xx) % 59.61/60.08 Found x3 as proof of ((more Xy) Xx) % 59.61/60.08 Found x10:False % 59.61/60.08 Found (fun (x3:((more Xx) Xy))=> x10) as proof of False % 59.61/60.08 Found (fun (x3:((more Xx) Xy))=> x10) as proof of (((more Xx) Xy)->False) % 59.61/60.08 Found x20:False % 59.61/60.08 Found (fun (x3:((more Xx) Xy))=> x20) as proof of False % 59.61/60.08 Found (fun (x3:((more Xx) Xy))=> x20) as proof of (((more Xx) Xy)->False) % 59.61/60.08 Found x2:((more Xx) Xy) % 59.61/60.08 Found x2 as proof of ((more Xx) Xy) % 59.61/60.08 Found x2:((more Xx) Xy) % 59.61/60.08 Found x2 as proof of ((more Xx) Xy) % 59.61/60.08 Found x00:False % 59.61/60.08 Found (fun (x4:(p Xy))=> x00) as proof of False % 59.61/60.08 Found (fun (x4:(p Xy))=> x00) as proof of ((p Xy)->False) % 59.61/60.08 Found x10:False % 59.61/60.08 Found (fun (x4:(p Xx))=> x10) as proof of False % 59.61/60.08 Found (fun (x4:(p Xx))=> x10) as proof of ((p Xx)->False) % 59.61/60.08 Found x10:False % 59.61/60.08 Found (fun (x2:((((eq nat) Xy) Xx)->False))=> x10) as proof of False % 59.61/60.08 Found (fun (x2:((((eq nat) Xy) Xx)->False))=> x10) as proof of (((((eq nat) Xy) Xx)->False)->False) % 59.61/60.08 Found (et0 (fun (x2:((((eq nat) Xy) Xx)->False))=> x10)) as proof of (((eq nat) Xy) Xx) % 59.61/60.08 Found ((et (((eq nat) Xy) Xx)) (fun (x2:((((eq nat) Xy) Xx)->False))=> x10)) as proof of (((eq nat) Xy) Xx) % 73.24/73.68 Found ((et (((eq nat) Xy) Xx)) (fun (x2:((((eq nat) Xy) Xx)->False))=> x10)) as proof of (((eq nat) Xy) Xx) % 73.24/73.68 Found x00:False % 73.24/73.68 Found (fun (x2:((((eq nat) Xy) Xx)->False))=> x00) as proof of False % 73.24/73.68 Found (fun (x2:((((eq nat) Xy) Xx)->False))=> x00) as proof of (((((eq nat) Xy) Xx)->False)->False) % 73.24/73.68 Found (et0 (fun (x2:((((eq nat) Xy) Xx)->False))=> x00)) as proof of (((eq nat) Xy) Xx) % 73.24/73.68 Found ((et (((eq nat) Xy) Xx)) (fun (x2:((((eq nat) Xy) Xx)->False))=> x00)) as proof of (((eq nat) Xy) Xx) % 73.24/73.68 Found ((et (((eq nat) Xy) Xx)) (fun (x2:((((eq nat) Xy) Xx)->False))=> x00)) as proof of (((eq nat) Xy) Xx) % 73.24/73.68 Found x10:False % 73.24/73.68 Found (fun (x2:(((P Xy)->(P Xx))->False))=> x10) as proof of False % 73.24/73.68 Found (fun (x2:(((P Xy)->(P Xx))->False))=> x10) as proof of ((((P Xy)->(P Xx))->False)->False) % 73.24/73.68 Found (et0 (fun (x2:(((P Xy)->(P Xx))->False))=> x10)) as proof of ((P Xy)->(P Xx)) % 73.24/73.68 Found ((et ((P Xy)->(P Xx))) (fun (x2:(((P Xy)->(P Xx))->False))=> x10)) as proof of ((P Xy)->(P Xx)) % 73.24/73.68 Found ((et ((P Xy)->(P Xx))) (fun (x2:(((P Xy)->(P Xx))->False))=> x10)) as proof of ((P Xy)->(P Xx)) % 73.24/73.68 Found x00:False % 73.24/73.68 Found (fun (x2:(((P Xy)->(P Xx))->False))=> x00) as proof of False % 73.24/73.68 Found (fun (x2:(((P Xy)->(P Xx))->False))=> x00) as proof of ((((P Xy)->(P Xx))->False)->False) % 73.24/73.68 Found (et0 (fun (x2:(((P Xy)->(P Xx))->False))=> x00)) as proof of ((P Xy)->(P Xx)) % 73.24/73.68 Found ((et ((P Xy)->(P Xx))) (fun (x2:(((P Xy)->(P Xx))->False))=> x00)) as proof of ((P Xy)->(P Xx)) % 73.24/73.68 Found ((et ((P Xy)->(P Xx))) (fun (x2:(((P Xy)->(P Xx))->False))=> x00)) as proof of ((P Xy)->(P Xx)) % 73.24/73.68 Found x10:False % 73.24/73.68 Found (fun (x4:(p Xx))=> x10) as proof of False % 73.24/73.68 Found (fun (x4:(p Xx))=> x10) as proof of ((p Xx)->False) % 73.24/73.68 Found x00:False % 73.24/73.68 Found (fun (x4:(p Xy))=> x00) as proof of False % 73.24/73.68 Found (fun (x4:(p Xy))=> x00) as proof of ((p Xy)->False) % 73.24/73.68 Found x00:False % 73.24/73.68 Found (fun (x4:(p Xy))=> x00) as proof of False % 73.24/73.68 Found (fun (x3:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))) (x4:(p Xy))=> x00) as proof of ((p Xy)->False) % 73.24/73.68 Found (fun (x3:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))) (x4:(p Xy))=> x00) as proof of ((forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))->((p Xy)->False)) % 73.24/73.68 Found x10:False % 73.24/73.68 Found (fun (x4:(p Xx))=> x10) as proof of False % 73.24/73.68 Found (fun (x3:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))) (x4:(p Xx))=> x10) as proof of ((p Xx)->False) % 73.24/73.68 Found (fun (x3:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))) (x4:(p Xx))=> x10) as proof of ((forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))->((p Xx)->False)) % 73.24/73.68 Found x2:(P Xx) % 73.24/73.68 Instantiate: Xy0:=Xx:nat % 73.24/73.68 Found x2 as proof of (P0 Xy0) % 73.24/73.68 Found x20:False % 73.24/73.68 Found (fun (x3:((more Xx) Xy))=> x20) as proof of False % 73.24/73.68 Found (fun (x3:((more Xx) Xy))=> x20) as proof of (((more Xx) Xy)->False) % 73.24/73.68 Found x10:False % 73.24/73.68 Found (fun (x3:((more Xx) Xy))=> x10) as proof of False % 73.24/73.68 Found (fun (x3:((more Xx) Xy))=> x10) as proof of (((more Xx) Xy)->False) % 73.24/73.68 Found x2:((more Xx) Xy) % 73.24/73.68 Found x2 as proof of ((more Xx) Xy) % 73.24/73.68 Found x2:((more Xx) Xy) % 73.24/73.68 Found x2 as proof of ((more Xx) Xy) % 73.24/73.68 Found x2:((more Xx) Xy) % 73.24/73.68 Found x2 as proof of ((more Xx) Xy) % 73.24/73.68 Found x2:((more Xx) Xy) % 73.24/73.68 Found x2 as proof of ((more Xx) Xy) % 73.24/73.68 Found x2:((more Xx) Xy) % 73.24/73.68 Found x2 as proof of ((more Xx) Xy) % 73.24/73.68 Found x2:((more Xx) Xy) % 73.24/73.68 Found x2 as proof of ((more Xx) Xy) % 73.24/73.68 Found x2:((more Xy) Xx) % 73.24/73.68 Found x2 as proof of ((more Xy) Xx) % 73.24/73.68 Found x2:((more Xy) Xx) % 73.24/73.68 Found x2 as proof of ((more Xy) Xx) % 73.24/73.68 Found x2:((more Xy) Xx) % 73.24/73.68 Found x2 as proof of ((more Xy) Xx) % 73.24/73.68 Found x2:((more Xy) Xx) % 73.24/73.68 Found x2 as proof of ((more Xy) Xx) % 73.24/73.68 Found x00:False % 73.24/73.68 Found (fun (x2:((((more Xx) Xy)->False)->False))=> x00) as proof of False % 73.24/73.68 Found (fun (x2:((((more Xx) Xy)->False)->False))=> x00) as proof of (((((more Xx) Xy)->False)->False)->False) % 73.24/73.68 Found x10:False % 73.24/73.68 Found (fun (x2:((((more Xx) Xy)->False)->False))=> x10) as proof of False % 73.24/73.68 Found (fun (x2:((((more Xx) Xy)->False)->False))=> x10) as proof of (((((more Xx) Xy)->False)->False)->False) % 73.24/73.68 Found x00:False % 73.24/73.68 Found (fun (x2:(((lessis Xy) Xx)->False))=> x00) as proof of False % 73.24/73.68 Found (fun (x2:(((lessis Xy) Xx)->False))=> x00) as proof of ((((lessis Xy) Xx)->False)->False) % 73.24/73.68 Found x10:False % 73.24/73.68 Found (fun (x2:(((lessis Xy) Xx)->False))=> x10) as proof of False % 83.71/84.14 Found (fun (x2:(((lessis Xy) Xx)->False))=> x10) as proof of ((((lessis Xy) Xx)->False)->False) % 83.71/84.14 Found x2:((more Xx) Xy) % 83.71/84.14 Found x2 as proof of ((more Xx) Xy) % 83.71/84.14 Found x2:((more Xx) Xy) % 83.71/84.14 Found x2 as proof of ((more Xx) Xy) % 83.71/84.14 Found x10:False % 83.71/84.14 Found (fun (x2:((more Xx) Xy))=> x10) as proof of False % 83.71/84.14 Found (fun (x2:((more Xx) Xy))=> x10) as proof of (((more Xx) Xy)->False) % 83.71/84.14 Found x00:False % 83.71/84.14 Found (fun (x2:((more Xx) Xy))=> x00) as proof of False % 83.71/84.14 Found (fun (x2:((more Xx) Xy))=> x00) as proof of (((more Xx) Xy)->False) % 83.71/84.14 Found x00:False % 83.71/84.14 Found (fun (x2:((more Xx) Xy))=> x00) as proof of False % 83.71/84.14 Found (fun (x2:((more Xx) Xy))=> x00) as proof of (((more Xx) Xy)->False) % 83.71/84.14 Found x10:False % 83.71/84.14 Found (fun (x2:((more Xx) Xy))=> x10) as proof of False % 83.71/84.14 Found (fun (x2:((more Xx) Xy))=> x10) as proof of (((more Xx) Xy)->False) % 83.71/84.14 Found x00:False % 83.71/84.14 Found (fun (x3:((P Xx)->False))=> x00) as proof of False % 83.71/84.14 Found (fun (x3:((P Xx)->False))=> x00) as proof of (((P Xx)->False)->False) % 83.71/84.14 Found (et0 (fun (x3:((P Xx)->False))=> x00)) as proof of (P Xx) % 83.71/84.14 Found ((et (P Xx)) (fun (x3:((P Xx)->False))=> x00)) as proof of (P Xx) % 83.71/84.14 Found ((et (P Xx)) (fun (x3:((P Xx)->False))=> x00)) as proof of (P Xx) % 83.71/84.14 Found x10:False % 83.71/84.14 Found (fun (x3:((P Xx)->False))=> x10) as proof of False % 83.71/84.14 Found (fun (x3:((P Xx)->False))=> x10) as proof of (((P Xx)->False)->False) % 83.71/84.14 Found (et0 (fun (x3:((P Xx)->False))=> x10)) as proof of (P Xx) % 83.71/84.14 Found ((et (P Xx)) (fun (x3:((P Xx)->False))=> x10)) as proof of (P Xx) % 83.71/84.14 Found ((et (P Xx)) (fun (x3:((P Xx)->False))=> x10)) as proof of (P Xx) % 83.71/84.14 Found x10:False % 83.71/84.14 Found (fun (x4:(p Xx))=> x10) as proof of False % 83.71/84.14 Found (fun (x3:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))) (x4:(p Xx))=> x10) as proof of ((p Xx)->False) % 83.71/84.14 Found (fun (x3:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))) (x4:(p Xx))=> x10) as proof of ((forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))->((p Xx)->False)) % 83.71/84.14 Found x00:False % 83.71/84.14 Found (fun (x4:(p Xy))=> x00) as proof of False % 83.71/84.14 Found (fun (x3:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))) (x4:(p Xy))=> x00) as proof of ((p Xy)->False) % 83.71/84.14 Found (fun (x3:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))) (x4:(p Xy))=> x00) as proof of ((forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))->((p Xy)->False)) % 83.71/84.14 Found x2:(P Xx) % 83.71/84.14 Instantiate: b:=Xx:nat % 83.71/84.14 Found x2 as proof of (P0 b) % 83.71/84.14 Found eq_ref00:=(eq_ref0 Xy):(((eq nat) Xy) Xy) % 83.71/84.14 Found (eq_ref0 Xy) as proof of (((eq nat) Xy) b) % 83.71/84.14 Found ((eq_ref nat) Xy) as proof of (((eq nat) Xy) b) % 83.71/84.14 Found ((eq_ref nat) Xy) as proof of (((eq nat) Xy) b) % 83.71/84.14 Found ((eq_ref nat) Xy) as proof of (((eq nat) Xy) b) % 83.71/84.14 Found x00:False % 83.71/84.14 Found (fun (x5:(p Xy))=> x00) as proof of False % 83.71/84.14 Found (fun (x5:(p Xy))=> x00) as proof of ((p Xy)->False) % 83.71/84.14 Found x10:False % 83.71/84.14 Found (fun (x5:(p Xx))=> x10) as proof of False % 83.71/84.14 Found (fun (x5:(p Xx))=> x10) as proof of ((p Xx)->False) % 83.71/84.14 Found x10:False % 83.71/84.14 Found (fun (x3:((more Xx) Xy))=> x10) as proof of False % 83.71/84.14 Found (fun (x3:((more Xx) Xy))=> x10) as proof of (((more Xx) Xy)->False) % 83.71/84.14 Found x10:False % 83.71/84.14 Found (fun (x2:((((eq nat) Xy) Xx)->False))=> x10) as proof of False % 83.71/84.14 Found (fun (x2:((((eq nat) Xy) Xx)->False))=> x10) as proof of (((((eq nat) Xy) Xx)->False)->False) % 83.71/84.14 Found x00:False % 83.71/84.14 Found (fun (x2:((((eq nat) Xy) Xx)->False))=> x00) as proof of False % 83.71/84.14 Found (fun (x2:((((eq nat) Xy) Xx)->False))=> x00) as proof of (((((eq nat) Xy) Xx)->False)->False) % 83.71/84.14 Found x00:False % 83.71/84.14 Found (fun (x2:((((eq nat) Xy) Xx)->False))=> x00) as proof of False % 83.71/84.14 Found (fun (x2:((((eq nat) Xy) Xx)->False))=> x00) as proof of (((((eq nat) Xy) Xx)->False)->False) % 83.71/84.14 Found x10:False % 83.71/84.14 Found (fun (x2:((((eq nat) Xy) Xx)->False))=> x10) as proof of False % 83.71/84.14 Found (fun (x2:((((eq nat) Xy) Xx)->False))=> x10) as proof of (((((eq nat) Xy) Xx)->False)->False) % 83.71/84.14 Found x2:((more Xx) Xy) % 83.71/84.14 Found x2 as proof of ((more Xx) Xy) % 83.71/84.14 Found x2:((more Xx) Xy) % 83.71/84.14 Found x2 as proof of ((more Xx) Xy) % 83.71/84.14 Found x2:((more b) Xy) % 83.71/84.14 Found x2 as proof of ((more b) Xy) % 83.71/84.14 Found x10:False % 83.71/84.14 Found (fun (x5:(p Xx))=> x10) as proof of False % 83.71/84.14 Found (fun (x4:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))) (x5:(p Xx))=> x10) as proof of ((p Xx)->False) % 83.71/84.14 Found (fun (x4:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))) (x5:(p Xx))=> x10) as proof of ((forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))->((p Xx)->False)) % 97.70/98.08 Found x00:False % 97.70/98.08 Found (fun (x5:(p Xy))=> x00) as proof of False % 97.70/98.08 Found (fun (x4:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))) (x5:(p Xy))=> x00) as proof of ((p Xy)->False) % 97.70/98.08 Found (fun (x4:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))) (x5:(p Xy))=> x00) as proof of ((forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))->((p Xy)->False)) % 97.70/98.08 Found x10:False % 97.70/98.08 Found (fun (x2:((more Xy) Xx))=> x10) as proof of False % 97.70/98.08 Found (fun (x2:((more Xy) Xx))=> x10) as proof of (((more Xy) Xx)->False) % 97.70/98.08 Found x00:False % 97.70/98.08 Found (fun (x2:((more Xy) Xx))=> x00) as proof of False % 97.70/98.08 Found (fun (x2:((more Xy) Xx))=> x00) as proof of (((more Xy) Xx)->False) % 97.70/98.08 Found x00:False % 97.70/98.08 Found (fun (x4:(p Xy))=> x00) as proof of False % 97.70/98.08 Found (fun (x4:(p Xy))=> x00) as proof of ((p Xy)->False) % 97.70/98.08 Found x10:False % 97.70/98.08 Found (fun (x4:(p Xx))=> x10) as proof of False % 97.70/98.08 Found (fun (x4:(p Xx))=> x10) as proof of ((p Xx)->False) % 97.70/98.08 Found x2:((more Xx) Xy) % 97.70/98.08 Found x2 as proof of ((more Xx) Xy) % 97.70/98.08 Found x2:((more Xy) Xx) % 97.70/98.08 Found x2 as proof of ((more Xy) Xx) % 97.70/98.08 Found x2:((more Xy) Xx) % 97.70/98.08 Found x2 as proof of ((more Xy) Xx) % 97.70/98.08 Found x2:((more Xx) Xy) % 97.70/98.08 Found x2 as proof of ((more Xx) Xy) % 97.70/98.08 Found x2:((more Xx) Xy) % 97.70/98.08 Found x2 as proof of ((more Xx) Xy) % 97.70/98.08 Found x2:((more Xx) Xy) % 97.70/98.08 Found x2 as proof of ((more Xx) Xy) % 97.70/98.08 Found eq_ref000:=(eq_ref00 P):((P Xy)->(P Xy)) % 97.70/98.08 Found (eq_ref00 P) as proof of (P0 Xy) % 97.70/98.08 Found ((eq_ref0 Xy) P) as proof of (P0 Xy) % 97.70/98.08 Found (((eq_ref nat) Xy) P) as proof of (P0 Xy) % 97.70/98.08 Found (((eq_ref nat) Xy) P) as proof of (P0 Xy) % 97.70/98.08 Found x10:False % 97.70/98.08 Found (fun (x3:(False->False))=> x10) as proof of False % 97.70/98.08 Found (fun (x3:(False->False))=> x10) as proof of ((False->False)->False) % 97.70/98.08 Found x00:False % 97.70/98.08 Found (fun (x3:(False->False))=> x00) as proof of False % 97.70/98.08 Found (fun (x3:(False->False))=> x00) as proof of ((False->False)->False) % 97.70/98.08 Found x10:False % 97.70/98.08 Found (fun (x2:(((P1 Xy)->(P1 Xx))->False))=> x10) as proof of False % 97.70/98.08 Found (fun (x2:(((P1 Xy)->(P1 Xx))->False))=> x10) as proof of ((((P1 Xy)->(P1 Xx))->False)->False) % 97.70/98.09 Found x10:False % 97.70/98.09 Found (fun (x2:(((P1 Xy)->(P1 Xx))->False))=> x10) as proof of False % 97.70/98.09 Found (fun (x2:(((P1 Xy)->(P1 Xx))->False))=> x10) as proof of ((((P1 Xy)->(P1 Xx))->False)->False) % 97.70/98.09 Found x00:False % 97.70/98.09 Found (fun (x2:(((P1 Xy)->(P1 Xx))->False))=> x00) as proof of False % 97.70/98.09 Found (fun (x2:(((P1 Xy)->(P1 Xx))->False))=> x00) as proof of ((((P1 Xy)->(P1 Xx))->False)->False) % 97.70/98.09 Found x00:False % 97.70/98.09 Found (fun (x2:(((P1 Xy)->(P1 Xx))->False))=> x00) as proof of False % 97.70/98.09 Found (fun (x2:(((P1 Xy)->(P1 Xx))->False))=> x00) as proof of ((((P1 Xy)->(P1 Xx))->False)->False) % 97.70/98.09 Found x2:((more Xy) Xx) % 97.70/98.09 Found x2 as proof of ((more Xy) Xx) % 97.70/98.09 Found x3:(P Xx) % 97.70/98.09 Instantiate: Xy0:=Xx:nat % 97.70/98.09 Found x3 as proof of (P0 Xy0) % 97.70/98.09 Found x10:False % 97.70/98.09 Found (fun (x2:((((eq nat) b) Xy)->False))=> x10) as proof of False % 97.70/98.09 Found (fun (x2:((((eq nat) b) Xy)->False))=> x10) as proof of (((((eq nat) b) Xy)->False)->False) % 97.70/98.09 Found x00:False % 97.70/98.09 Found (fun (x2:((((eq nat) b) Xy)->False))=> x00) as proof of False % 97.70/98.09 Found (fun (x2:((((eq nat) b) Xy)->False))=> x00) as proof of (((((eq nat) b) Xy)->False)->False) % 97.70/98.09 Found x10:False % 97.70/98.09 Found (fun (x4:(p Xx))=> x10) as proof of False % 97.70/98.09 Found (fun (x3:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))) (x4:(p Xx))=> x10) as proof of ((p Xx)->False) % 97.70/98.09 Found (fun (x3:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))) (x4:(p Xx))=> x10) as proof of ((forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))->((p Xx)->False)) % 97.70/98.09 Found x00:False % 97.70/98.09 Found (fun (x4:(p Xy))=> x00) as proof of False % 97.70/98.09 Found (fun (x3:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))) (x4:(p Xy))=> x00) as proof of ((p Xy)->False) % 97.70/98.09 Found (fun (x3:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))) (x4:(p Xy))=> x00) as proof of ((forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))->((p Xy)->False)) % 97.70/98.09 Found x00:False % 97.70/98.09 Found (fun (x3:((P1 Xx)->False))=> x00) as proof of False % 97.70/98.09 Found (fun (x3:((P1 Xx)->False))=> x00) as proof of (((P1 Xx)->False)->False) % 97.70/98.09 Found x00:False % 97.70/98.09 Found (fun (x3:((P1 Xx)->False))=> x00) as proof of False % 97.70/98.09 Found (fun (x3:((P1 Xx)->False))=> x00) as proof of (((P1 Xx)->False)->False) % 110.70/111.09 Found x10:False % 110.70/111.09 Found (fun (x3:((P1 Xx)->False))=> x10) as proof of False % 110.70/111.09 Found (fun (x3:((P1 Xx)->False))=> x10) as proof of (((P1 Xx)->False)->False) % 110.70/111.09 Found x10:False % 110.70/111.09 Found (fun (x3:((P1 Xx)->False))=> x10) as proof of False % 110.70/111.09 Found (fun (x3:((P1 Xx)->False))=> x10) as proof of (((P1 Xx)->False)->False) % 110.70/111.09 Found x10:False % 110.70/111.09 Found (fun (x3:((more Xx) Xy))=> x10) as proof of False % 110.70/111.09 Found (fun (x3:((more Xx) Xy))=> x10) as proof of (((more Xx) Xy)->False) % 110.70/111.09 Found x20:False % 110.70/111.09 Found (fun (x3:((more Xx) Xy))=> x20) as proof of False % 110.70/111.09 Found (fun (x3:((more Xx) Xy))=> x20) as proof of (((more Xx) Xy)->False) % 110.70/111.09 Found x20:False % 110.70/111.09 Found (fun (x3:((more Xx) Xy))=> x20) as proof of False % 110.70/111.09 Found (fun (x3:((more Xx) Xy))=> x20) as proof of (((more Xx) Xy)->False) % 110.70/111.09 Found x10:False % 110.70/111.09 Found (fun (x3:((more Xx) Xy))=> x10) as proof of False % 110.70/111.09 Found (fun (x3:((more Xx) Xy))=> x10) as proof of (((more Xx) Xy)->False) % 110.70/111.09 Found x10:False % 110.70/111.09 Found (fun (x2:(((lessis Xy) Xx)->False))=> x10) as proof of False % 110.70/111.09 Found (fun (x2:(((lessis Xy) Xx)->False))=> x10) as proof of ((((lessis Xy) Xx)->False)->False) % 110.70/111.09 Found (et0 (fun (x2:(((lessis Xy) Xx)->False))=> x10)) as proof of ((lessis Xy) Xx) % 110.70/111.09 Found ((et ((lessis Xy) Xx)) (fun (x2:(((lessis Xy) Xx)->False))=> x10)) as proof of ((lessis Xy) Xx) % 110.70/111.09 Found ((et ((lessis Xy) Xx)) (fun (x2:(((lessis Xy) Xx)->False))=> x10)) as proof of ((lessis Xy) Xx) % 110.70/111.09 Found x00:False % 110.70/111.09 Found (fun (x2:(((lessis Xy) Xx)->False))=> x00) as proof of False % 110.70/111.09 Found (fun (x2:(((lessis Xy) Xx)->False))=> x00) as proof of ((((lessis Xy) Xx)->False)->False) % 110.70/111.09 Found (et0 (fun (x2:(((lessis Xy) Xx)->False))=> x00)) as proof of ((lessis Xy) Xx) % 110.70/111.09 Found ((et ((lessis Xy) Xx)) (fun (x2:(((lessis Xy) Xx)->False))=> x00)) as proof of ((lessis Xy) Xx) % 110.70/111.09 Found ((et ((lessis Xy) Xx)) (fun (x2:(((lessis Xy) Xx)->False))=> x00)) as proof of ((lessis Xy) Xx) % 110.70/111.09 Found x3:(P Xx) % 110.70/111.09 Instantiate: b:=Xx:nat % 110.70/111.09 Found x3 as proof of (P0 b) % 110.70/111.09 Found eq_ref00:=(eq_ref0 Xy):(((eq nat) Xy) Xy) % 110.70/111.09 Found (eq_ref0 Xy) as proof of (((eq nat) Xy) b) % 110.70/111.09 Found ((eq_ref nat) Xy) as proof of (((eq nat) Xy) b) % 110.70/111.09 Found ((eq_ref nat) Xy) as proof of (((eq nat) Xy) b) % 110.70/111.09 Found ((eq_ref nat) Xy) as proof of (((eq nat) Xy) b) % 110.70/111.09 Found x10:False % 110.70/111.09 Found (fun (x2:(((P b)->(P Xy))->False))=> x10) as proof of False % 110.70/111.09 Found (fun (x2:(((P b)->(P Xy))->False))=> x10) as proof of ((((P b)->(P Xy))->False)->False) % 110.70/111.09 Found x00:False % 110.70/111.09 Found (fun (x2:(((P b)->(P Xy))->False))=> x00) as proof of False % 110.70/111.09 Found (fun (x2:(((P b)->(P Xy))->False))=> x00) as proof of ((((P b)->(P Xy))->False)->False) % 110.70/111.09 Found x3:((more Xx) Xy) % 110.70/111.09 Found x3 as proof of ((more Xx) Xy) % 110.70/111.09 Found x3:((more Xx) Xy) % 110.70/111.09 Found x3 as proof of ((more Xx) Xy) % 110.70/111.09 Found x3:((more Xx) Xy) % 110.70/111.09 Found x3 as proof of ((more Xx) Xy) % 110.70/111.09 Found x3:((more Xx) Xy) % 110.70/111.09 Found x3 as proof of ((more Xx) Xy) % 110.70/111.09 Found x10:False % 110.70/111.09 Found (fun (x3:(p Xx))=> x10) as proof of False % 110.70/111.09 Found (fun (x3:(p Xx))=> x10) as proof of ((p Xx)->False) % 110.70/111.09 Found x00:False % 110.70/111.09 Found (fun (x3:(p Xy))=> x00) as proof of False % 110.70/111.09 Found (fun (x3:(p Xy))=> x00) as proof of ((p Xy)->False) % 110.70/111.09 Found x3:((more Xy) Xx) % 110.70/111.09 Found x3 as proof of ((more Xy) Xx) % 110.70/111.09 Found x3:((more Xy) Xx) % 110.70/111.09 Found x3 as proof of ((more Xy) Xx) % 110.70/111.09 Found x3:((more Xy) Xx) % 110.70/111.09 Found x3 as proof of ((more Xy) Xx) % 110.70/111.09 Found x3:((more Xy) Xx) % 110.70/111.09 Found x3 as proof of ((more Xy) Xx) % 110.70/111.09 Found x2:((more Xx) Xy) % 110.70/111.09 Found x2 as proof of ((more Xx) Xy) % 110.70/111.09 Found x2:((more Xx) Xy) % 110.70/111.09 Found x2 as proof of ((more Xx) Xy) % 110.70/111.09 Found x2:((more Xx) Xy) % 110.70/111.09 Found x2 as proof of ((more Xx) Xy) % 110.70/111.09 Found x2:((more Xx) Xy) % 110.70/111.09 Found x2 as proof of ((more Xx) Xy) % 110.70/111.09 Found x300:=(x30 x6):((lessis Xx) Xy) % 110.70/111.09 Found (x30 x6) as proof of ((lessis Xx) Xy) % 110.70/111.09 Found ((x3 Xy) x6) as proof of ((lessis Xx) Xy) % 110.70/111.09 Found ((x3 Xy) x6) as proof of ((lessis Xx) Xy) % 110.70/111.09 Found ((satz10d0 ((x3 Xy) x6)) x2) as proof of False % 110.70/111.09 Found ((((satz10d Xx) Xy) ((x3 Xy) x6)) x2) as proof of False % 110.70/111.09 Found (fun (x6:(p Xy))=> ((((satz10d Xx) Xy) ((x3 Xy) x6)) x2)) as proof of False % 110.70/111.09 Found (fun (x5:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))) (x6:(p Xy))=> ((((satz10d Xx) Xy) ((x3 Xy) x6)) x2)) as proof of ((p Xy)->False) % 110.70/111.09 Found (fun (x5:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))) (x6:(p Xy))=> ((((satz10d Xx) Xy) ((x3 Xy) x6)) x2)) as proof of ((forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))->((p Xy)->False)) % 115.02/115.47 Found (x1 (fun (x5:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))) (x6:(p Xy))=> ((((satz10d Xx) Xy) ((x3 Xy) x6)) x2))) as proof of False % 115.02/115.47 Found (fun (x4:(p Xx))=> (x1 (fun (x5:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))) (x6:(p Xy))=> ((((satz10d Xx) Xy) ((x3 Xy) x6)) x2)))) as proof of False % 115.02/115.47 Found (fun (x3:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))) (x4:(p Xx))=> (x1 (fun (x5:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))) (x6:(p Xy))=> ((((satz10d Xx) Xy) ((x3 Xy) x6)) x2)))) as proof of ((p Xx)->False) % 115.02/115.47 Found (fun (x3:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))) (x4:(p Xx))=> (x1 (fun (x5:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))) (x6:(p Xy))=> ((((satz10d Xx) Xy) ((x3 Xy) x6)) x2)))) as proof of ((forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))->((p Xx)->False)) % 115.02/115.47 Found (x0 (fun (x3:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))) (x4:(p Xx))=> (x1 (fun (x5:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))) (x6:(p Xy))=> ((((satz10d Xx) Xy) ((x3 Xy) x6)) x2))))) as proof of False % 115.02/115.47 Found (fun (x2:((more Xx) Xy))=> (x0 (fun (x3:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))) (x4:(p Xx))=> (x1 (fun (x5:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))) (x6:(p Xy))=> ((((satz10d Xx) Xy) ((x3 Xy) x6)) x2)))))) as proof of False % 115.02/115.47 Found (fun (x2:((more Xx) Xy))=> (x0 (fun (x3:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))) (x4:(p Xx))=> (x1 (fun (x5:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))) (x6:(p Xy))=> ((((satz10d Xx) Xy) ((x3 Xy) x6)) x2)))))) as proof of (((more Xx) Xy)->False) % 115.02/115.47 Found x10:False % 115.02/115.47 Found (fun (x4:(p Xx))=> x10) as proof of False % 115.02/115.47 Found (fun (x4:(p Xx))=> x10) as proof of ((p Xx)->False) % 115.02/115.47 Found x00:False % 115.02/115.47 Found (fun (x4:(p Xy))=> x00) as proof of False % 115.02/115.47 Found (fun (x4:(p Xy))=> x00) as proof of ((p Xy)->False) % 115.02/115.47 Found x00:False % 115.02/115.47 Found (fun (x4:(p Xy))=> x00) as proof of False % 115.02/115.47 Found (fun (x3:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))) (x4:(p Xy))=> x00) as proof of ((p Xy)->False) % 115.02/115.47 Found (fun (x3:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))) (x4:(p Xy))=> x00) as proof of ((forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))->((p Xy)->False)) % 115.02/115.47 Found x10:False % 115.02/115.47 Found (fun (x4:(p Xx))=> x10) as proof of False % 115.02/115.47 Found (fun (x3:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))) (x4:(p Xx))=> x10) as proof of ((p Xx)->False) % 115.02/115.47 Found (fun (x3:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))) (x4:(p Xx))=> x10) as proof of ((forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))->((p Xx)->False)) % 115.02/115.47 Found x10:False % 115.02/115.47 Found (fun (x3:(p Xx))=> x10) as proof of False % 115.02/115.47 Found (fun (x3:(p Xx))=> x10) as proof of ((p Xx)->False) % 115.02/115.47 Found x00:False % 115.02/115.47 Found (fun (x3:(p Xy))=> x00) as proof of False % 115.02/115.47 Found (fun (x3:(p Xy))=> x00) as proof of ((p Xy)->False) % 115.02/115.47 Found x10:False % 115.02/115.47 Found (fun (x2:((((eq nat) Xy) Xx)->False))=> x10) as proof of False % 115.02/115.47 Found (fun (x2:((((eq nat) Xy) Xx)->False))=> x10) as proof of (((((eq nat) Xy) Xx)->False)->False) % 115.02/115.47 Found (et0 (fun (x2:((((eq nat) Xy) Xx)->False))=> x10)) as proof of (((eq nat) Xy) Xx) % 115.02/115.47 Found ((et (((eq nat) Xy) Xx)) (fun (x2:((((eq nat) Xy) Xx)->False))=> x10)) as proof of (((eq nat) Xy) Xx) % 115.02/115.47 Found ((et (((eq nat) Xy) Xx)) (fun (x2:((((eq nat) Xy) Xx)->False))=> x10)) as proof of (((eq nat) Xy) Xx) % 115.02/115.47 Found x00:False % 115.02/115.47 Found (fun (x2:((((eq nat) Xy) Xx)->False))=> x00) as proof of False % 115.02/115.47 Found (fun (x2:((((eq nat) Xy) Xx)->False))=> x00) as proof of (((((eq nat) Xy) Xx)->False)->False) % 115.02/115.47 Found (et0 (fun (x2:((((eq nat) Xy) Xx)->False))=> x00)) as proof of (((eq nat) Xy) Xx) % 115.02/115.47 Found ((et (((eq nat) Xy) Xx)) (fun (x2:((((eq nat) Xy) Xx)->False))=> x00)) as proof of (((eq nat) Xy) Xx) % 115.02/115.47 Found ((et (((eq nat) Xy) Xx)) (fun (x2:((((eq nat) Xy) Xx)->False))=> x00)) as proof of (((eq nat) Xy) Xx) % 115.02/115.47 Found x10:False % 115.02/115.47 Found (fun (x2:((((eq nat) Xy) Xx)->False))=> x10) as proof of False % 115.02/115.47 Found (fun (x2:((((eq nat) Xy) Xx)->False))=> x10) as proof of (((((eq nat) Xy) Xx)->False)->False) % 115.02/115.47 Found (et0 (fun (x2:((((eq nat) Xy) Xx)->False))=> x10)) as proof of (((eq nat) Xy) Xx) % 120.60/120.99 Found ((et (((eq nat) Xy) Xx)) (fun (x2:((((eq nat) Xy) Xx)->False))=> x10)) as proof of (((eq nat) Xy) Xx) % 120.60/120.99 Found ((et (((eq nat) Xy) Xx)) (fun (x2:((((eq nat) Xy) Xx)->False))=> x10)) as proof of (((eq nat) Xy) Xx) % 120.60/120.99 Found x00:False % 120.60/120.99 Found (fun (x2:((((eq nat) Xy) Xx)->False))=> x00) as proof of False % 120.60/120.99 Found (fun (x2:((((eq nat) Xy) Xx)->False))=> x00) as proof of (((((eq nat) Xy) Xx)->False)->False) % 120.60/120.99 Found (et0 (fun (x2:((((eq nat) Xy) Xx)->False))=> x00)) as proof of (((eq nat) Xy) Xx) % 120.60/120.99 Found ((et (((eq nat) Xy) Xx)) (fun (x2:((((eq nat) Xy) Xx)->False))=> x00)) as proof of (((eq nat) Xy) Xx) % 120.60/120.99 Found ((et (((eq nat) Xy) Xx)) (fun (x2:((((eq nat) Xy) Xx)->False))=> x00)) as proof of (((eq nat) Xy) Xx) % 120.60/120.99 Found x00:False % 120.60/120.99 Found (fun (x3:((P Xy)->False))=> x00) as proof of False % 120.60/120.99 Found (fun (x3:((P Xy)->False))=> x00) as proof of (((P Xy)->False)->False) % 120.60/120.99 Found x10:False % 120.60/120.99 Found (fun (x3:((P Xy)->False))=> x10) as proof of False % 120.60/120.99 Found (fun (x3:((P Xy)->False))=> x10) as proof of (((P Xy)->False)->False) % 120.60/120.99 Found False_rect00:=(False_rect0 ((lessis Xy) Xx)):((lessis Xy) Xx) % 120.60/120.99 Found (False_rect0 ((lessis Xy) Xx)) as proof of ((lessis Xy) Xx) % 120.60/120.99 Found ((fun (P:Type)=> ((False_rect P) x10)) ((lessis Xy) Xx)) as proof of ((lessis Xy) Xx) % 120.60/120.99 Found ((fun (P:Type)=> ((False_rect P) x10)) ((lessis Xy) Xx)) as proof of ((lessis Xy) Xx) % 120.60/120.99 Found ((satz1400 ((fun (P:Type)=> ((False_rect P) x10)) ((lessis Xy) Xx))) (fun (x3:((more Xx) Xy))=> x10)) as proof of (((eq nat) Xx) Xy) % 120.60/120.99 Found (((satz140 Xx) ((fun (P:Type)=> ((False_rect P) x10)) ((lessis Xy) Xx))) (fun (x3:((more Xx) Xy))=> x10)) as proof of (((eq nat) Xx) Xy) % 120.60/120.99 Found ((((satz14 Xy) Xx) ((fun (P:Type)=> ((False_rect P) x10)) ((lessis Xy) Xx))) (fun (x3:((more Xx) Xy))=> x10)) as proof of (((eq nat) Xx) Xy) % 120.60/120.99 Found ((((satz14 Xy) Xx) ((fun (P:Type)=> ((False_rect P) x10)) ((lessis Xy) Xx))) (fun (x3:((more Xx) Xy))=> x10)) as proof of (((eq nat) Xx) Xy) % 120.60/120.99 Found False_rect00:=(False_rect0 ((lessis Xy) Xx)):((lessis Xy) Xx) % 120.60/120.99 Found (False_rect0 ((lessis Xy) Xx)) as proof of ((lessis Xy) Xx) % 120.60/120.99 Found ((fun (P:Type)=> ((False_rect P) x20)) ((lessis Xy) Xx)) as proof of ((lessis Xy) Xx) % 120.60/120.99 Found ((fun (P:Type)=> ((False_rect P) x20)) ((lessis Xy) Xx)) as proof of ((lessis Xy) Xx) % 120.60/120.99 Found ((satz1400 ((fun (P:Type)=> ((False_rect P) x20)) ((lessis Xy) Xx))) (fun (x3:((more Xx) Xy))=> x20)) as proof of (((eq nat) Xx) Xy) % 120.60/120.99 Found (((satz140 Xx) ((fun (P:Type)=> ((False_rect P) x20)) ((lessis Xy) Xx))) (fun (x3:((more Xx) Xy))=> x20)) as proof of (((eq nat) Xx) Xy) % 120.60/120.99 Found ((((satz14 Xy) Xx) ((fun (P:Type)=> ((False_rect P) x20)) ((lessis Xy) Xx))) (fun (x3:((more Xx) Xy))=> x20)) as proof of (((eq nat) Xx) Xy) % 120.60/120.99 Found ((((satz14 Xy) Xx) ((fun (P:Type)=> ((False_rect P) x20)) ((lessis Xy) Xx))) (fun (x3:((more Xx) Xy))=> x20)) as proof of (((eq nat) Xx) Xy) % 120.60/120.99 Found x10:False % 120.60/120.99 Found (fun (x3:(p Xx))=> x10) as proof of False % 120.60/120.99 Found (fun (x2:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))) (x3:(p Xx))=> x10) as proof of ((p Xx)->False) % 120.60/120.99 Found (fun (x2:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))) (x3:(p Xx))=> x10) as proof of ((forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))->((p Xx)->False)) % 120.60/120.99 Found x00:False % 120.60/120.99 Found (fun (x3:(p Xy))=> x00) as proof of False % 120.60/120.99 Found (fun (x2:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))) (x3:(p Xy))=> x00) as proof of ((p Xy)->False) % 120.60/120.99 Found (fun (x2:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))) (x3:(p Xy))=> x00) as proof of ((forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))->((p Xy)->False)) % 120.60/120.99 Found x00:False % 120.60/120.99 Found (fun (x4:(p Xy))=> x00) as proof of False % 120.60/120.99 Found (fun (x4:(p Xy))=> x00) as proof of ((p Xy)->False) % 120.60/120.99 Found x10:False % 120.60/120.99 Found (fun (x4:(p Xx))=> x10) as proof of False % 120.60/120.99 Found (fun (x4:(p Xx))=> x10) as proof of ((p Xx)->False) % 120.60/120.99 Found x10:False % 120.60/120.99 Found (fun (x4:(p Xx))=> x10) as proof of False % 120.60/120.99 Found (fun (x4:(p Xx))=> x10) as proof of ((p Xx)->False) % 120.60/120.99 Found x00:False % 120.60/120.99 Found (fun (x4:(p Xy))=> x00) as proof of False % 120.60/120.99 Found (fun (x4:(p Xy))=> x00) as proof of ((p Xy)->False) % 120.60/120.99 Found eq_ref00:=(eq_ref0 Xx):(((eq nat) Xx) Xx) % 120.60/120.99 Found (eq_ref0 Xx) as proof of (((eq nat) Xx) b) % 130.39/130.78 Found ((eq_ref nat) Xx) as proof of (((eq nat) Xx) b) % 130.39/130.78 Found ((eq_ref nat) Xx) as proof of (((eq nat) Xx) b) % 130.39/130.78 Found ((eq_ref nat) Xx) as proof of (((eq nat) Xx) b) % 130.39/130.78 Found x10:False % 130.39/130.78 Found (fun (x5:(p Xy))=> x10) as proof of False % 130.39/130.78 Found (fun (x5:(p Xy))=> x10) as proof of ((p Xy)->False) % 130.39/130.78 Found x20:False % 130.39/130.78 Found (fun (x5:(p Xx))=> x20) as proof of False % 130.39/130.78 Found (fun (x5:(p Xx))=> x20) as proof of ((p Xx)->False) % 130.39/130.78 Found x20:False % 130.39/130.78 Found (fun (x3:((more Xy) Xx))=> x20) as proof of False % 130.39/130.78 Found (fun (x3:((more Xy) Xx))=> x20) as proof of (((more Xy) Xx)->False) % 130.39/130.78 Found x10:False % 130.39/130.78 Found (fun (x3:((more Xy) Xx))=> x10) as proof of False % 130.39/130.78 Found (fun (x3:((more Xy) Xx))=> x10) as proof of (((more Xy) Xx)->False) % 130.39/130.78 Found x00:False % 130.39/130.78 Found (fun (x4:(p Xy))=> x00) as proof of False % 130.39/130.78 Found (fun (x4:(p Xy))=> x00) as proof of ((p Xy)->False) % 130.39/130.78 Found x10:False % 130.39/130.78 Found (fun (x4:(p Xx))=> x10) as proof of False % 130.39/130.78 Found (fun (x4:(p Xx))=> x10) as proof of ((p Xx)->False) % 130.39/130.78 Found x3:((more Xx) Xy) % 130.39/130.78 Found x3 as proof of ((more Xx) Xy) % 130.39/130.78 Found x00:False % 130.39/130.78 Found (fun (x2:(((forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))->((p Xy)->False))->False))=> x00) as proof of False % 130.39/130.78 Found (fun (x2:(((forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))->((p Xy)->False))->False))=> x00) as proof of ((((forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))->((p Xy)->False))->False)->False) % 130.39/130.78 Found x3:((more b) Xy) % 130.39/130.78 Found x3 as proof of ((more b) Xy) % 130.39/130.78 Found x10:False % 130.39/130.78 Found (fun (x2:(((forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))->((p Xx)->False))->False))=> x10) as proof of False % 130.39/130.78 Found (fun (x2:(((forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))->((p Xx)->False))->False))=> x10) as proof of ((((forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))->((p Xx)->False))->False)->False) % 130.39/130.78 Found x3:((more Xx) Xy) % 130.39/130.78 Found x3 as proof of ((more Xx) Xy) % 130.39/130.78 Found x10:False % 130.39/130.78 Found (fun (x2:(((P1 Xy)->(P1 Xx))->False))=> x10) as proof of False % 130.39/130.78 Found (fun (x2:(((P1 Xy)->(P1 Xx))->False))=> x10) as proof of ((((P1 Xy)->(P1 Xx))->False)->False) % 130.39/130.78 Found (et0 (fun (x2:(((P1 Xy)->(P1 Xx))->False))=> x10)) as proof of ((P1 Xy)->(P1 Xx)) % 130.39/130.78 Found ((et ((P1 Xy)->(P1 Xx))) (fun (x2:(((P1 Xy)->(P1 Xx))->False))=> x10)) as proof of ((P1 Xy)->(P1 Xx)) % 130.39/130.78 Found ((et ((P1 Xy)->(P1 Xx))) (fun (x2:(((P1 Xy)->(P1 Xx))->False))=> x10)) as proof of ((P1 Xy)->(P1 Xx)) % 130.39/130.78 Found x00:False % 130.39/130.78 Found (fun (x2:(((P1 Xy)->(P1 Xx))->False))=> x00) as proof of False % 130.39/130.78 Found (fun (x2:(((P1 Xy)->(P1 Xx))->False))=> x00) as proof of ((((P1 Xy)->(P1 Xx))->False)->False) % 130.39/130.78 Found (et0 (fun (x2:(((P1 Xy)->(P1 Xx))->False))=> x00)) as proof of ((P1 Xy)->(P1 Xx)) % 130.39/130.78 Found ((et ((P1 Xy)->(P1 Xx))) (fun (x2:(((P1 Xy)->(P1 Xx))->False))=> x00)) as proof of ((P1 Xy)->(P1 Xx)) % 130.39/130.78 Found ((et ((P1 Xy)->(P1 Xx))) (fun (x2:(((P1 Xy)->(P1 Xx))->False))=> x00)) as proof of ((P1 Xy)->(P1 Xx)) % 130.39/130.78 Found x10:False % 130.39/130.78 Found (fun (x2:(((P1 Xy)->(P1 Xx))->False))=> x10) as proof of False % 130.39/130.78 Found (fun (x2:(((P1 Xy)->(P1 Xx))->False))=> x10) as proof of ((((P1 Xy)->(P1 Xx))->False)->False) % 130.39/130.78 Found (et0 (fun (x2:(((P1 Xy)->(P1 Xx))->False))=> x10)) as proof of ((P1 Xy)->(P1 Xx)) % 130.39/130.78 Found ((et ((P1 Xy)->(P1 Xx))) (fun (x2:(((P1 Xy)->(P1 Xx))->False))=> x10)) as proof of ((P1 Xy)->(P1 Xx)) % 130.39/130.78 Found ((et ((P1 Xy)->(P1 Xx))) (fun (x2:(((P1 Xy)->(P1 Xx))->False))=> x10)) as proof of ((P1 Xy)->(P1 Xx)) % 130.39/130.78 Found x00:False % 130.39/130.78 Found (fun (x2:(((P1 Xy)->(P1 Xx))->False))=> x00) as proof of False % 130.39/130.78 Found (fun (x2:(((P1 Xy)->(P1 Xx))->False))=> x00) as proof of ((((P1 Xy)->(P1 Xx))->False)->False) % 130.39/130.78 Found (et0 (fun (x2:(((P1 Xy)->(P1 Xx))->False))=> x00)) as proof of ((P1 Xy)->(P1 Xx)) % 130.39/130.78 Found ((et ((P1 Xy)->(P1 Xx))) (fun (x2:(((P1 Xy)->(P1 Xx))->False))=> x00)) as proof of ((P1 Xy)->(P1 Xx)) % 130.39/130.78 Found ((et ((P1 Xy)->(P1 Xx))) (fun (x2:(((P1 Xy)->(P1 Xx))->False))=> x00)) as proof of ((P1 Xy)->(P1 Xx)) % 130.39/130.78 Found eq_ref000:=(eq_ref00 P):((P Xy)->(P Xy)) % 130.39/130.78 Found (eq_ref00 P) as proof of (P0 Xy) % 130.39/130.78 Found ((eq_ref0 Xy) P) as proof of (P0 Xy) % 130.39/130.78 Found (((eq_ref nat) Xy) P) as proof of (P0 Xy) % 130.39/130.78 Found (((eq_ref nat) Xy) P) as proof of (P0 Xy) % 130.39/130.78 Found x10:False % 130.39/130.78 Found (fun (x3:(p Xx))=> x10) as proof of False % 130.39/130.78 Found (fun (x2:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))) (x3:(p Xx))=> x10) as proof of ((p Xx)->False) % 135.02/135.48 Found (fun (x2:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))) (x3:(p Xx))=> x10) as proof of ((forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))->((p Xx)->False)) % 135.02/135.48 Found x00:False % 135.02/135.48 Found (fun (x3:(p Xy))=> x00) as proof of False % 135.02/135.48 Found (fun (x2:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))) (x3:(p Xy))=> x00) as proof of ((p Xy)->False) % 135.02/135.48 Found (fun (x2:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))) (x3:(p Xy))=> x00) as proof of ((forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))->((p Xy)->False)) % 135.02/135.48 Found False_rect00:=(False_rect0 ((lessis Xy) Xx)):((lessis Xy) Xx) % 135.02/135.48 Found (False_rect0 ((lessis Xy) Xx)) as proof of ((lessis Xy) Xx) % 135.02/135.48 Found ((fun (P:Type)=> ((False_rect P) x10)) ((lessis Xy) Xx)) as proof of ((lessis Xy) Xx) % 135.02/135.48 Found ((fun (P:Type)=> ((False_rect P) x10)) ((lessis Xy) Xx)) as proof of ((lessis Xy) Xx) % 135.02/135.48 Found ((satz1400 ((fun (P:Type)=> ((False_rect P) x10)) ((lessis Xy) Xx))) (fun (x3:((more Xx) Xy))=> x10)) as proof of (((eq nat) Xx) Xy) % 135.02/135.48 Found (((satz140 Xx) ((fun (P:Type)=> ((False_rect P) x10)) ((lessis Xy) Xx))) (fun (x3:((more Xx) Xy))=> x10)) as proof of (((eq nat) Xx) Xy) % 135.02/135.48 Found ((((satz14 Xy) Xx) ((fun (P:Type)=> ((False_rect P) x10)) ((lessis Xy) Xx))) (fun (x3:((more Xx) Xy))=> x10)) as proof of (((eq nat) Xx) Xy) % 135.02/135.48 Found (fun (x2:(((forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))->((p Xy)->False))->False))=> ((((satz14 Xy) Xx) ((fun (P:Type)=> ((False_rect P) x10)) ((lessis Xy) Xx))) (fun (x3:((more Xx) Xy))=> x10))) as proof of (((eq nat) Xx) Xy) % 135.02/135.48 Found (fun (x2:(((forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))->((p Xy)->False))->False))=> ((((satz14 Xy) Xx) ((fun (P:Type)=> ((False_rect P) x10)) ((lessis Xy) Xx))) (fun (x3:((more Xx) Xy))=> x10))) as proof of ((((forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))->((p Xy)->False))->False)->(((eq nat) Xx) Xy)) % 135.02/135.48 Found eq_ref00:=(eq_ref0 Xx):(((eq nat) Xx) Xx) % 135.02/135.48 Found (eq_ref0 Xx) as proof of (((eq nat) Xx) b) % 135.02/135.48 Found ((eq_ref nat) Xx) as proof of (((eq nat) Xx) b) % 135.02/135.48 Found ((eq_ref nat) Xx) as proof of (((eq nat) Xx) b) % 135.02/135.48 Found ((eq_ref nat) Xx) as proof of (((eq nat) Xx) b) % 135.02/135.48 Found eq_ref00:=(eq_ref0 b):(((eq nat) b) b) % 135.02/135.48 Found (eq_ref0 b) as proof of (((eq nat) b) Xy) % 135.02/135.48 Found ((eq_ref nat) b) as proof of (((eq nat) b) Xy) % 135.02/135.48 Found ((eq_ref nat) b) as proof of (((eq nat) b) Xy) % 135.02/135.48 Found ((eq_ref nat) b) as proof of (((eq nat) b) Xy) % 135.02/135.48 Found eq_ref000:=(eq_ref00 P):((P Xx)->(P Xx)) % 135.02/135.48 Found (eq_ref00 P) as proof of (P0 Xx) % 135.02/135.48 Found ((eq_ref0 Xx) P) as proof of (P0 Xx) % 135.02/135.48 Found (((eq_ref nat) Xx) P) as proof of (P0 Xx) % 135.02/135.48 Found (((eq_ref nat) Xx) P) as proof of (P0 Xx) % 135.02/135.48 Found eq_ref00:=(eq_ref0 Xx):(((eq nat) Xx) Xx) % 135.02/135.48 Found (eq_ref0 Xx) as proof of (((eq nat) Xx) b) % 135.02/135.48 Found ((eq_ref nat) Xx) as proof of (((eq nat) Xx) b) % 135.02/135.48 Found ((eq_ref nat) Xx) as proof of (((eq nat) Xx) b) % 135.02/135.48 Found ((eq_ref nat) Xx) as proof of (((eq nat) Xx) b) % 135.02/135.48 Found eq_ref00:=(eq_ref0 b):(((eq nat) b) b) % 135.02/135.48 Found (eq_ref0 b) as proof of (((eq nat) b) Xy) % 135.02/135.48 Found ((eq_ref nat) b) as proof of (((eq nat) b) Xy) % 135.02/135.48 Found ((eq_ref nat) b) as proof of (((eq nat) b) Xy) % 135.02/135.48 Found ((eq_ref nat) b) as proof of (((eq nat) b) Xy) % 135.02/135.48 Found x3:((more Xy) Xx) % 135.02/135.48 Found x3 as proof of ((more Xy) Xx) % 135.02/135.48 Found x3:((more Xy) Xx) % 135.02/135.48 Found x3 as proof of ((more Xy) Xx) % 135.02/135.48 Found x10:False % 135.02/135.48 Found (fun (x3:(p Xx))=> x10) as proof of False % 135.02/135.48 Found (fun (x3:(p Xx))=> x10) as proof of ((p Xx)->False) % 135.02/135.48 Found x00:False % 135.02/135.48 Found (fun (x4:(p Xy))=> x00) as proof of False % 135.02/135.48 Found (fun (x3:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))) (x4:(p Xy))=> x00) as proof of ((p Xy)->False) % 135.02/135.48 Found (fun (x3:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))) (x4:(p Xy))=> x00) as proof of ((forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))->((p Xy)->False)) % 135.02/135.48 Found x00:False % 135.02/135.48 Found (fun (x3:(p Xy))=> x00) as proof of False % 135.02/135.48 Found (fun (x3:(p Xy))=> x00) as proof of ((p Xy)->False) % 135.02/135.48 Found x10:False % 135.02/135.48 Found (fun (x4:(p Xx))=> x10) as proof of False % 135.02/135.48 Found (fun (x3:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))) (x4:(p Xx))=> x10) as proof of ((p Xx)->False) % 135.02/135.48 Found (fun (x3:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))) (x4:(p Xx))=> x10) as proof of ((forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))->((p Xx)->False)) % 138.34/138.74 Found x10:False % 138.34/138.74 Found (fun (x4:(p Xx))=> x10) as proof of False % 138.34/138.74 Found (fun (x3:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))) (x4:(p Xx))=> x10) as proof of ((p Xx)->False) % 138.34/138.74 Found (fun (x3:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))) (x4:(p Xx))=> x10) as proof of ((forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))->((p Xx)->False)) % 138.34/138.74 Found x00:False % 138.34/138.74 Found (fun (x4:(p Xy))=> x00) as proof of False % 138.34/138.74 Found (fun (x3:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))) (x4:(p Xy))=> x00) as proof of ((p Xy)->False) % 138.34/138.74 Found (fun (x3:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))) (x4:(p Xy))=> x00) as proof of ((forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))->((p Xy)->False)) % 138.34/138.74 Found x10:False % 138.34/138.74 Found (fun (x3:(((p Xx)->False)->False))=> x10) as proof of False % 138.34/138.74 Found (fun (x3:(((p Xx)->False)->False))=> x10) as proof of ((((p Xx)->False)->False)->False) % 138.34/138.74 Found x00:False % 138.34/138.74 Found (fun (x3:(((p Xy)->False)->False))=> x00) as proof of False % 138.34/138.74 Found (fun (x3:(((p Xy)->False)->False))=> x00) as proof of ((((p Xy)->False)->False)->False) % 138.34/138.74 Found x00:False % 138.34/138.74 Found (fun (x4:(p Xy))=> x00) as proof of False % 138.34/138.74 Found (fun (x4:(p Xy))=> x00) as proof of ((p Xy)->False) % 138.34/138.74 Found x10:False % 138.34/138.74 Found (fun (x4:(p Xx))=> x10) as proof of False % 138.34/138.74 Found (fun (x4:(p Xx))=> x10) as proof of ((p Xx)->False) % 138.34/138.74 Found x10:False % 138.34/138.74 Found (fun (x4:(p Xx))=> x10) as proof of False % 138.34/138.74 Found (fun (x4:(p Xx))=> x10) as proof of ((p Xx)->False) % 138.34/138.74 Found x00:False % 138.34/138.74 Found (fun (x4:(p Xy))=> x00) as proof of False % 138.34/138.74 Found (fun (x4:(p Xy))=> x00) as proof of ((p Xy)->False) % 138.34/138.74 Found eq_ref00:=(eq_ref0 b):(((eq nat) b) b) % 138.34/138.74 Found (eq_ref0 b) as proof of (P b) % 138.34/138.74 Found ((eq_ref nat) b) as proof of (P b) % 138.34/138.74 Found ((eq_ref nat) b) as proof of (P b) % 138.34/138.74 Found ((eq_ref nat) b) as proof of (P b) % 138.34/138.74 Found eq_ref00:=(eq_ref0 Xy):(((eq nat) Xy) Xy) % 138.34/138.74 Found (eq_ref0 Xy) as proof of (((eq nat) Xy) b) % 138.34/138.74 Found ((eq_ref nat) Xy) as proof of (((eq nat) Xy) b) % 138.34/138.74 Found ((eq_ref nat) Xy) as proof of (((eq nat) Xy) b) % 138.34/138.74 Found ((eq_ref nat) Xy) as proof of (((eq nat) Xy) b) % 138.34/138.74 Found x10:False % 138.34/138.74 Found (fun (x5:(p Xy))=> x10) as proof of False % 138.34/138.74 Found (fun (x4:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))) (x5:(p Xy))=> x10) as proof of ((p Xy)->False) % 138.34/138.74 Found (fun (x4:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))) (x5:(p Xy))=> x10) as proof of ((forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))->((p Xy)->False)) % 138.34/138.74 Found x20:False % 138.34/138.74 Found (fun (x5:(p Xx))=> x20) as proof of False % 138.34/138.74 Found (fun (x4:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))) (x5:(p Xx))=> x20) as proof of ((p Xx)->False) % 138.34/138.74 Found (fun (x4:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))) (x5:(p Xx))=> x20) as proof of ((forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))->((p Xx)->False)) % 138.34/138.74 Found x00:False % 138.34/138.74 Found (fun (x2:(((forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))->((p Xy)->False))->False))=> x00) as proof of False % 138.34/138.74 Found (fun (x2:(((forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))->((p Xy)->False))->False))=> x00) as proof of ((((forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))->((p Xy)->False))->False)->False) % 138.34/138.74 Found x10:False % 138.34/138.74 Found (fun (x2:((((more Xx) Xy)->False)->False))=> x10) as proof of False % 138.34/138.74 Found (fun (x2:((((more Xx) Xy)->False)->False))=> x10) as proof of (((((more Xx) Xy)->False)->False)->False) % 138.34/138.74 Found x10:False % 138.34/138.74 Found (fun (x2:(((forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))->((p Xx)->False))->False))=> x10) as proof of False % 138.34/138.74 Found (fun (x2:(((forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))->((p Xx)->False))->False))=> x10) as proof of ((((forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))->((p Xx)->False))->False)->False) % 138.34/138.74 Found x00:False % 138.34/138.74 Found (fun (x2:((((more Xx) Xy)->False)->False))=> x00) as proof of False % 138.34/138.74 Found (fun (x2:((((more Xx) Xy)->False)->False))=> x00) as proof of (((((more Xx) Xy)->False)->False)->False) % 138.34/138.74 Found x00:False % 138.34/138.74 Found (fun (x2:((((more Xx) Xy)->False)->False))=> x00) as proof of False % 138.34/138.74 Found (fun (x2:((((more Xx) Xy)->False)->False))=> x00) as proof of (((((more Xx) Xy)->False)->False)->False) % 147.36/147.81 Found x10:False % 147.36/147.81 Found (fun (x2:((((more Xx) Xy)->False)->False))=> x10) as proof of False % 147.36/147.81 Found (fun (x2:((((more Xx) Xy)->False)->False))=> x10) as proof of (((((more Xx) Xy)->False)->False)->False) % 147.36/147.81 Found x00:False % 147.36/147.81 Found (fun (x2:((((eq nat) b) Xy)->False))=> x00) as proof of False % 147.36/147.81 Found (fun (x2:((((eq nat) b) Xy)->False))=> x00) as proof of (((((eq nat) b) Xy)->False)->False) % 147.36/147.81 Found (et0 (fun (x2:((((eq nat) b) Xy)->False))=> x00)) as proof of (((eq nat) b) Xy) % 147.36/147.81 Found ((et (((eq nat) b) Xy)) (fun (x2:((((eq nat) b) Xy)->False))=> x00)) as proof of (((eq nat) b) Xy) % 147.36/147.81 Found ((et (((eq nat) b) Xy)) (fun (x2:((((eq nat) b) Xy)->False))=> x00)) as proof of (((eq nat) b) Xy) % 147.36/147.81 Found x10:False % 147.36/147.81 Found (fun (x2:((((eq nat) b) Xy)->False))=> x10) as proof of False % 147.36/147.81 Found (fun (x2:((((eq nat) b) Xy)->False))=> x10) as proof of (((((eq nat) b) Xy)->False)->False) % 147.36/147.81 Found (et0 (fun (x2:((((eq nat) b) Xy)->False))=> x10)) as proof of (((eq nat) b) Xy) % 147.36/147.81 Found ((et (((eq nat) b) Xy)) (fun (x2:((((eq nat) b) Xy)->False))=> x10)) as proof of (((eq nat) b) Xy) % 147.36/147.81 Found ((et (((eq nat) b) Xy)) (fun (x2:((((eq nat) b) Xy)->False))=> x10)) as proof of (((eq nat) b) Xy) % 147.36/147.81 Found x00:False % 147.36/147.81 Found (fun (x2:(((lessis Xy) Xx)->False))=> x00) as proof of False % 147.36/147.81 Found (fun (x2:(((lessis Xy) Xx)->False))=> x00) as proof of ((((lessis Xy) Xx)->False)->False) % 147.36/147.81 Found x10:False % 147.36/147.81 Found (fun (x2:(((lessis Xy) Xx)->False))=> x10) as proof of False % 147.36/147.81 Found (fun (x2:(((lessis Xy) Xx)->False))=> x10) as proof of ((((lessis Xy) Xx)->False)->False) % 147.36/147.81 Found x10:False % 147.36/147.81 Found (fun (x2:(((lessis Xy) Xx)->False))=> x10) as proof of False % 147.36/147.81 Found (fun (x2:(((lessis Xy) Xx)->False))=> x10) as proof of ((((lessis Xy) Xx)->False)->False) % 147.36/147.81 Found x00:False % 147.36/147.81 Found (fun (x2:(((lessis Xy) Xx)->False))=> x00) as proof of False % 147.36/147.81 Found (fun (x2:(((lessis Xy) Xx)->False))=> x00) as proof of ((((lessis Xy) Xx)->False)->False) % 147.36/147.81 Found x10:False % 147.36/147.81 Found (fun (x4:(p Xx))=> x10) as proof of False % 147.36/147.81 Found (fun (x4:(p Xx))=> x10) as proof of ((p Xx)->False) % 147.36/147.81 Found x00:False % 147.36/147.81 Found (fun (x4:(p Xy))=> x00) as proof of False % 147.36/147.81 Found (fun (x4:(p Xy))=> x00) as proof of ((p Xy)->False) % 147.36/147.81 Found x2:((more Xx) Xy) % 147.36/147.81 Found x2 as proof of ((more Xx) Xy) % 147.36/147.81 Found x2:((more Xx) Xy) % 147.36/147.81 Found x2 as proof of ((more Xx) Xy) % 147.36/147.81 Found x2:((more Xy) Xx) % 147.36/147.81 Found x2 as proof of ((more Xy) Xx) % 147.36/147.81 Found x2:((more Xx) Xy) % 147.36/147.81 Found x2 as proof of ((more Xx) Xy) % 147.36/147.81 Found x2:((more Xx) Xy) % 147.36/147.81 Found x2 as proof of ((more Xx) Xy) % 147.36/147.81 Found x2:((more Xy) Xx) % 147.36/147.81 Found x2 as proof of ((more Xy) Xx) % 147.36/147.81 Found x00:False % 147.36/147.81 Found (fun (x4:(p Xy))=> x00) as proof of False % 147.36/147.81 Found (fun (x3:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))) (x4:(p Xy))=> x00) as proof of ((p Xy)->False) % 147.36/147.81 Found (fun (x3:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))) (x4:(p Xy))=> x00) as proof of ((forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))->((p Xy)->False)) % 147.36/147.81 Found x10:False % 147.36/147.81 Found (fun (x4:(p Xx))=> x10) as proof of False % 147.36/147.81 Found (fun (x3:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))) (x4:(p Xx))=> x10) as proof of ((p Xx)->False) % 147.36/147.81 Found (fun (x3:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))) (x4:(p Xx))=> x10) as proof of ((forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))->((p Xx)->False)) % 147.36/147.81 Found x10:False % 147.36/147.81 Found (fun (x4:(p Xy))=> x10) as proof of False % 147.36/147.81 Found (fun (x4:(p Xy))=> x10) as proof of ((p Xy)->False) % 147.36/147.81 Found x20:False % 147.36/147.81 Found (fun (x4:(p Xx))=> x20) as proof of False % 147.36/147.81 Found (fun (x4:(p Xx))=> x20) as proof of ((p Xx)->False) % 147.36/147.81 Found x00:False % 147.36/147.81 Found (fun (x4:(False->False))=> x00) as proof of False % 147.36/147.81 Found (fun (x4:(False->False))=> x00) as proof of ((False->False)->False) % 147.36/147.81 Found x10:False % 147.36/147.81 Found (fun (x4:(False->False))=> x10) as proof of False % 147.36/147.81 Found (fun (x4:(False->False))=> x10) as proof of ((False->False)->False) % 147.36/147.81 Found x10:False % 147.36/147.81 Found (fun (x3:((P1 Xx)->False))=> x10) as proof of False % 147.36/147.81 Found (fun (x3:((P1 Xx)->False))=> x10) as proof of (((P1 Xx)->False)->False) % 147.36/147.81 Found (et0 (fun (x3:((P1 Xx)->False))=> x10)) as proof of (P1 Xx) % 147.36/147.81 Found ((et (P1 Xx)) (fun (x3:((P1 Xx)->False))=> x10)) as proof of (P1 Xx) % 147.36/147.81 Found ((et (P1 Xx)) (fun (x3:((P1 Xx)->False))=> x10)) as proof of (P1 Xx) % 155.74/156.15 Found x00:False % 155.74/156.15 Found (fun (x3:((P1 Xx)->False))=> x00) as proof of False % 155.74/156.15 Found (fun (x3:((P1 Xx)->False))=> x00) as proof of (((P1 Xx)->False)->False) % 155.74/156.15 Found (et0 (fun (x3:((P1 Xx)->False))=> x00)) as proof of (P1 Xx) % 155.74/156.15 Found ((et (P1 Xx)) (fun (x3:((P1 Xx)->False))=> x00)) as proof of (P1 Xx) % 155.74/156.15 Found ((et (P1 Xx)) (fun (x3:((P1 Xx)->False))=> x00)) as proof of (P1 Xx) % 155.74/156.15 Found x10:False % 155.74/156.15 Found (fun (x3:((P1 Xx)->False))=> x10) as proof of False % 155.74/156.15 Found (fun (x3:((P1 Xx)->False))=> x10) as proof of (((P1 Xx)->False)->False) % 155.74/156.15 Found (et0 (fun (x3:((P1 Xx)->False))=> x10)) as proof of (P1 Xx) % 155.74/156.15 Found ((et (P1 Xx)) (fun (x3:((P1 Xx)->False))=> x10)) as proof of (P1 Xx) % 155.74/156.15 Found ((et (P1 Xx)) (fun (x3:((P1 Xx)->False))=> x10)) as proof of (P1 Xx) % 155.74/156.15 Found x00:False % 155.74/156.15 Found (fun (x3:((P1 Xx)->False))=> x00) as proof of False % 155.74/156.15 Found (fun (x3:((P1 Xx)->False))=> x00) as proof of (((P1 Xx)->False)->False) % 155.74/156.15 Found (et0 (fun (x3:((P1 Xx)->False))=> x00)) as proof of (P1 Xx) % 155.74/156.15 Found ((et (P1 Xx)) (fun (x3:((P1 Xx)->False))=> x00)) as proof of (P1 Xx) % 155.74/156.15 Found ((et (P1 Xx)) (fun (x3:((P1 Xx)->False))=> x00)) as proof of (P1 Xx) % 155.74/156.15 Found x2:(P Xy) % 155.74/156.15 Instantiate: b:=Xy:nat % 155.74/156.15 Found x2 as proof of (P0 b) % 155.74/156.15 Found eq_ref00:=(eq_ref0 Xx):(((eq nat) Xx) Xx) % 155.74/156.15 Found (eq_ref0 Xx) as proof of (((eq nat) Xx) b) % 155.74/156.15 Found ((eq_ref nat) Xx) as proof of (((eq nat) Xx) b) % 155.74/156.15 Found ((eq_ref nat) Xx) as proof of (((eq nat) Xx) b) % 155.74/156.15 Found ((eq_ref nat) Xx) as proof of (((eq nat) Xx) b) % 155.74/156.15 Found x10:False % 155.74/156.15 Found (fun (x3:(p Xx))=> x10) as proof of False % 155.74/156.15 Found (fun (x3:(p Xx))=> x10) as proof of ((p Xx)->False) % 155.74/156.15 Found x2:(P Xy) % 155.74/156.15 Instantiate: Xy0:=Xy:nat % 155.74/156.15 Found x2 as proof of (P0 Xy0) % 155.74/156.15 Found x00:False % 155.74/156.15 Found (fun (x3:(p Xy))=> x00) as proof of False % 155.74/156.15 Found (fun (x3:(p Xy))=> x00) as proof of ((p Xy)->False) % 155.74/156.15 Found x10:False % 155.74/156.15 Found (fun (x3:(((p Xx)->False)->False))=> x10) as proof of False % 155.74/156.15 Found (fun (x3:(((p Xx)->False)->False))=> x10) as proof of ((((p Xx)->False)->False)->False) % 155.74/156.15 Found x00:False % 155.74/156.15 Found (fun (x3:(((p Xy)->False)->False))=> x00) as proof of False % 155.74/156.15 Found (fun (x3:(((p Xy)->False)->False))=> x00) as proof of ((((p Xy)->False)->False)->False) % 155.74/156.15 Found x00:False % 155.74/156.15 Found (fun (x3:(((forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))->((p Xy)->False))->False))=> x00) as proof of False % 155.74/156.15 Found (fun (x3:(((forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))->((p Xy)->False))->False))=> x00) as proof of ((((forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))->((p Xy)->False))->False)->False) % 155.74/156.15 Found x3:(p Xx) % 155.74/156.15 Instantiate: Xy0:=Xx:nat % 155.74/156.15 Found x3 as proof of (p Xy0) % 155.74/156.15 Found (x20 x3) as proof of ((lessis Xx0) Xy0) % 155.74/156.15 Found ((x2 Xy0) x3) as proof of ((lessis Xx0) Xy0) % 155.74/156.15 Found ((x2 Xy0) x3) as proof of ((lessis Xx0) Xy0) % 155.74/156.15 Found ((x2 Xy0) x3) as proof of ((lessis Xx0) Xy0) % 155.74/156.15 Found x10:False % 155.74/156.15 Found (fun (x3:(((forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))->((p Xx)->False))->False))=> x10) as proof of False % 155.74/156.15 Found (fun (x3:(((forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))->((p Xx)->False))->False))=> x10) as proof of ((((forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))->((p Xx)->False))->False)->False) % 155.74/156.15 Found x10:False % 155.74/156.15 Found (fun (x2:(((P b)->(P Xy))->False))=> x10) as proof of False % 155.74/156.15 Found (fun (x2:(((P b)->(P Xy))->False))=> x10) as proof of ((((P b)->(P Xy))->False)->False) % 155.74/156.15 Found (et0 (fun (x2:(((P b)->(P Xy))->False))=> x10)) as proof of ((P b)->(P Xy)) % 155.74/156.15 Found ((et ((P b)->(P Xy))) (fun (x2:(((P b)->(P Xy))->False))=> x10)) as proof of ((P b)->(P Xy)) % 155.74/156.15 Found ((et ((P b)->(P Xy))) (fun (x2:(((P b)->(P Xy))->False))=> x10)) as proof of ((P b)->(P Xy)) % 155.74/156.15 Found x00:False % 155.74/156.15 Found (fun (x2:(((P b)->(P Xy))->False))=> x00) as proof of False % 155.74/156.15 Found (fun (x2:(((P b)->(P Xy))->False))=> x00) as proof of ((((P b)->(P Xy))->False)->False) % 155.74/156.15 Found (et0 (fun (x2:(((P b)->(P Xy))->False))=> x00)) as proof of ((P b)->(P Xy)) % 155.74/156.15 Found ((et ((P b)->(P Xy))) (fun (x2:(((P b)->(P Xy))->False))=> x00)) as proof of ((P b)->(P Xy)) % 155.74/156.15 Found ((et ((P b)->(P Xy))) (fun (x2:(((P b)->(P Xy))->False))=> x00)) as proof of ((P b)->(P Xy)) % 155.74/156.15 Found x10:False % 155.74/156.15 Found (fun (x3:(p Xx))=> x10) as proof of False % 155.74/156.15 Found (fun (x2:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))) (x3:(p Xx))=> x10) as proof of ((p Xx)->False) % 159.35/159.74 Found (fun (x2:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))) (x3:(p Xx))=> x10) as proof of ((forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))->((p Xx)->False)) % 159.35/159.74 Found x00:False % 159.35/159.74 Found (fun (x3:(p Xy))=> x00) as proof of False % 159.35/159.74 Found (fun (x2:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))) (x3:(p Xy))=> x00) as proof of ((p Xy)->False) % 159.35/159.74 Found (fun (x2:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))) (x3:(p Xy))=> x00) as proof of ((forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))->((p Xy)->False)) % 159.35/159.74 Found x10:False % 159.35/159.74 Found (fun (x4:(p Xx))=> x10) as proof of False % 159.35/159.74 Found (fun (x3:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))) (x4:(p Xx))=> x10) as proof of ((p Xx)->False) % 159.35/159.74 Found (fun (x3:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))) (x4:(p Xx))=> x10) as proof of ((forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))->((p Xx)->False)) % 159.35/159.74 Found x00:False % 159.35/159.74 Found (fun (x4:(p Xy))=> x00) as proof of False % 159.35/159.74 Found (fun (x3:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))) (x4:(p Xy))=> x00) as proof of ((p Xy)->False) % 159.35/159.74 Found (fun (x3:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))) (x4:(p Xy))=> x00) as proof of ((forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))->((p Xy)->False)) % 159.35/159.74 Found x00:False % 159.35/159.74 Found (fun (x4:(p Xy))=> x00) as proof of False % 159.35/159.74 Found (fun (x3:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))) (x4:(p Xy))=> x00) as proof of ((p Xy)->False) % 159.35/159.74 Found (fun (x3:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))) (x4:(p Xy))=> x00) as proof of ((forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))->((p Xy)->False)) % 159.35/159.74 Found x10:False % 159.35/159.74 Found (fun (x4:(p Xx))=> x10) as proof of False % 159.35/159.74 Found (fun (x3:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))) (x4:(p Xx))=> x10) as proof of ((p Xx)->False) % 159.35/159.74 Found (fun (x3:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))) (x4:(p Xx))=> x10) as proof of ((forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))->((p Xx)->False)) % 159.35/159.74 Found x00:False % 159.35/159.74 Found (fun (x3:(p Xy))=> x00) as proof of False % 159.35/159.74 Found (fun (x3:(p Xy))=> x00) as proof of ((p Xy)->False) % 159.35/159.74 Found x10:False % 159.35/159.74 Found (fun (x3:(p Xx))=> x10) as proof of False % 159.35/159.74 Found (fun (x3:(p Xx))=> x10) as proof of ((p Xx)->False) % 159.35/159.74 Found x10:False % 159.35/159.74 Found (fun (x5:(p Xx))=> x10) as proof of False % 159.35/159.74 Found (fun (x5:(p Xx))=> x10) as proof of ((p Xx)->False) % 159.35/159.74 Found x10:False % 159.35/159.74 Found (fun (x5:(p Xx))=> x10) as proof of False % 159.35/159.74 Found (fun (x5:(p Xx))=> x10) as proof of ((p Xx)->False) % 159.35/159.74 Found x10:False % 159.35/159.74 Found (fun (x4:(p Xx))=> x10) as proof of False % 159.35/159.74 Found (fun (x3:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))) (x4:(p Xx))=> x10) as proof of ((p Xx)->False) % 159.35/159.74 Found (fun (x3:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))) (x4:(p Xx))=> x10) as proof of ((forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))->((p Xx)->False)) % 159.35/159.74 Found x00:False % 159.35/159.74 Found (fun (x4:(p Xy))=> x00) as proof of False % 159.35/159.74 Found (fun (x3:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))) (x4:(p Xy))=> x00) as proof of ((p Xy)->False) % 159.35/159.74 Found (fun (x3:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))) (x4:(p Xy))=> x00) as proof of ((forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))->((p Xy)->False)) % 159.35/159.74 Found x00:False % 159.35/159.74 Found (fun (x4:(p Xy))=> x00) as proof of False % 159.35/159.74 Found (fun (x4:(p Xy))=> x00) as proof of ((p Xy)->False) % 159.35/159.74 Found x00:False % 159.35/159.74 Found (fun (x5:(p Xy))=> x00) as proof of False % 159.35/159.74 Found (fun (x5:(p Xy))=> x00) as proof of ((p Xy)->False) % 159.35/159.74 Found x10:False % 159.35/159.74 Found (fun (x4:(p Xx))=> x10) as proof of False % 159.35/159.74 Found (fun (x4:(p Xx))=> x10) as proof of ((p Xx)->False) % 159.35/159.74 Found x00:False % 159.35/159.74 Found (fun (x5:(p Xy))=> x00) as proof of False % 159.35/159.74 Found (fun (x5:(p Xy))=> x00) as proof of ((p Xy)->False) % 159.35/159.74 Found x10:False % 159.35/159.74 Found (fun (x4:(p Xy))=> x10) as proof of False % 159.35/159.74 Found (fun (x3:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))) (x4:(p Xy))=> x10) as proof of ((p Xy)->False) % 159.35/159.74 Found (fun (x3:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))) (x4:(p Xy))=> x10) as proof of ((forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))->((p Xy)->False)) % 159.35/159.74 Found x20:False % 159.35/159.74 Found (fun (x4:(p Xx))=> x20) as proof of False % 159.35/159.74 Found (fun (x3:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))) (x4:(p Xx))=> x20) as proof of ((p Xx)->False) % 163.72/164.12 Found (fun (x3:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))) (x4:(p Xx))=> x20) as proof of ((forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))->((p Xx)->False)) % 163.72/164.12 Found x20:False % 163.72/164.12 Found (fun (x3:((more Xy) Xx))=> x20) as proof of False % 163.72/164.12 Found (fun (x3:((more Xy) Xx))=> x20) as proof of (((more Xy) Xx)->False) % 163.72/164.12 Found x10:False % 163.72/164.12 Found (fun (x3:((more Xy) Xx))=> x10) as proof of False % 163.72/164.12 Found (fun (x3:((more Xy) Xx))=> x10) as proof of (((more Xy) Xx)->False) % 163.72/164.12 Found x10:False % 163.72/164.12 Found (fun (x4:(False->False))=> x10) as proof of False % 163.72/164.12 Found (fun (x4:(False->False))=> x10) as proof of ((False->False)->False) % 163.72/164.12 Found x00:False % 163.72/164.12 Found (fun (x4:(False->False))=> x00) as proof of False % 163.72/164.12 Found (fun (x4:(False->False))=> x00) as proof of ((False->False)->False) % 163.72/164.12 Found x10:False % 163.72/164.12 Found (fun (x4:(p Xx))=> x10) as proof of False % 163.72/164.12 Found (fun (x4:(p Xx))=> x10) as proof of ((p Xx)->False) % 163.72/164.12 Found x00:False % 163.72/164.12 Found (fun (x4:(p Xy))=> x00) as proof of False % 163.72/164.12 Found (fun (x4:(p Xy))=> x00) as proof of ((p Xy)->False) % 163.72/164.12 Found x00:False % 163.72/164.12 Found (fun (x4:(((p Xy)->False)->False))=> x00) as proof of False % 163.72/164.12 Found (fun (x4:(((p Xy)->False)->False))=> x00) as proof of ((((p Xy)->False)->False)->False) % 163.72/164.12 Found x10:False % 163.72/164.12 Found (fun (x4:(((p Xx)->False)->False))=> x10) as proof of False % 163.72/164.12 Found (fun (x4:(((p Xx)->False)->False))=> x10) as proof of ((((p Xx)->False)->False)->False) % 163.72/164.12 Found x00:False % 163.72/164.12 Found (fun (x2:((((more Xy) Xx)->False)->False))=> x00) as proof of False % 163.72/164.12 Found (fun (x2:((((more Xy) Xx)->False)->False))=> x00) as proof of (((((more Xy) Xx)->False)->False)->False) % 163.72/164.12 Found x10:False % 163.72/164.12 Found (fun (x2:((((more Xy) Xx)->False)->False))=> x10) as proof of False % 163.72/164.12 Found (fun (x2:((((more Xy) Xx)->False)->False))=> x10) as proof of (((((more Xy) Xx)->False)->False)->False) % 163.72/164.12 Found x00:False % 163.72/164.12 Found (fun (x4:(p Xy))=> x00) as proof of False % 163.72/164.12 Found (fun (x4:(p Xy))=> x00) as proof of ((p Xy)->False) % 163.72/164.12 Found x10:False % 163.72/164.12 Found (fun (x4:(p Xx))=> x10) as proof of False % 163.72/164.12 Found (fun (x4:(p Xx))=> x10) as proof of ((p Xx)->False) % 163.72/164.12 Found x10:False % 163.72/164.12 Found (fun (x4:(p Xx))=> x10) as proof of False % 163.72/164.12 Found (fun (x4:(p Xx))=> x10) as proof of ((p Xx)->False) % 163.72/164.12 Found x00:False % 163.72/164.12 Found (fun (x4:(p Xy))=> x00) as proof of False % 163.72/164.12 Found (fun (x4:(p Xy))=> x00) as proof of ((p Xy)->False) % 163.72/164.12 Found x00:False % 163.72/164.12 Found (fun (x2:(((lessis Xx) Xy)->False))=> x00) as proof of False % 163.72/164.12 Found (fun (x2:(((lessis Xx) Xy)->False))=> x00) as proof of ((((lessis Xx) Xy)->False)->False) % 163.72/164.12 Found x20:False % 163.72/164.12 Found (fun (x3:((more Xx) Xy))=> x20) as proof of False % 163.72/164.12 Found (fun (x3:((more Xx) Xy))=> x20) as proof of (((more Xx) Xy)->False) % 163.72/164.12 Found x10:False % 163.72/164.12 Found (fun (x3:((more Xx) Xy))=> x10) as proof of False % 163.72/164.12 Found (fun (x3:((more Xx) Xy))=> x10) as proof of (((more Xx) Xy)->False) % 163.72/164.12 Found x10:False % 163.72/164.12 Found (fun (x2:(((lessis Xx) Xy)->False))=> x10) as proof of False % 163.72/164.12 Found (fun (x2:(((lessis Xx) Xy)->False))=> x10) as proof of ((((lessis Xx) Xy)->False)->False) % 163.72/164.12 Found x00:False % 163.72/164.12 Found (fun (x3:(p Xy))=> x00) as proof of False % 163.72/164.12 Found (fun (x2:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))) (x3:(p Xy))=> x00) as proof of ((p Xy)->False) % 163.72/164.12 Found (fun (x2:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))) (x3:(p Xy))=> x00) as proof of ((forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))->((p Xy)->False)) % 163.72/164.12 Found x10:False % 163.72/164.12 Found (fun (x3:(p Xx))=> x10) as proof of False % 163.72/164.12 Found (fun (x2:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))) (x3:(p Xx))=> x10) as proof of ((p Xx)->False) % 163.72/164.12 Found (fun (x2:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))) (x3:(p Xx))=> x10) as proof of ((forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))->((p Xx)->False)) % 163.72/164.12 Found x00:False % 163.72/164.12 Found (fun (x2:((more Xy) Xx))=> x00) as proof of False % 163.72/164.12 Found (fun (x2:((more Xy) Xx))=> x00) as proof of (((more Xy) Xx)->False) % 163.72/164.12 Found x10:False % 163.72/164.12 Found (fun (x2:((more Xy) Xx))=> x10) as proof of False % 163.72/164.12 Found (fun (x2:((more Xy) Xx))=> x10) as proof of (((more Xy) Xx)->False) % 163.72/164.12 Found x10:False % 163.72/164.12 Found (fun (x2:((more Xy) Xx))=> x10) as proof of False % 163.72/164.12 Found (fun (x2:((more Xy) Xx))=> x10) as proof of (((more Xy) Xx)->False) % 171.14/171.58 Found x00:False % 171.14/171.58 Found (fun (x2:((more Xy) Xx))=> x00) as proof of False % 171.14/171.58 Found (fun (x2:((more Xy) Xx))=> x00) as proof of (((more Xy) Xx)->False) % 171.14/171.58 Found x00:False % 171.14/171.58 Found (fun (x2:((more Xy) Xx))=> x00) as proof of False % 171.14/171.58 Found (fun (x2:((more Xy) Xx))=> x00) as proof of (((more Xy) Xx)->False) % 171.14/171.58 Found x10:False % 171.14/171.58 Found (fun (x2:((more Xy) Xx))=> x10) as proof of False % 171.14/171.58 Found (fun (x2:((more Xy) Xx))=> x10) as proof of (((more Xy) Xx)->False) % 171.14/171.58 Found x00:False % 171.14/171.58 Found (fun (x2:((more Xy) Xx))=> x00) as proof of False % 171.14/171.58 Found (fun (x2:((more Xy) Xx))=> x00) as proof of (((more Xy) Xx)->False) % 171.14/171.58 Found x10:False % 171.14/171.58 Found (fun (x2:((more Xy) Xx))=> x10) as proof of False % 171.14/171.58 Found (fun (x2:((more Xy) Xx))=> x10) as proof of (((more Xy) Xx)->False) % 171.14/171.58 Found x2:((more Xx) Xy) % 171.14/171.58 Found x2 as proof of ((more Xx) Xy) % 171.14/171.58 Found x2:((more Xx) Xy) % 171.14/171.58 Found x2 as proof of ((more Xx) Xy) % 171.14/171.58 Found x2:((more Xx) Xy) % 171.14/171.58 Found x2 as proof of ((more Xx) Xy) % 171.14/171.58 Found x2:((more Xx) Xy) % 171.14/171.58 Found x2 as proof of ((more Xx) Xy) % 171.14/171.58 Found x00:False % 171.14/171.58 Found (fun (x3:((P Xy)->False))=> x00) as proof of False % 171.14/171.58 Found (fun (x3:((P Xy)->False))=> x00) as proof of (((P Xy)->False)->False) % 171.14/171.58 Found (et0 (fun (x3:((P Xy)->False))=> x00)) as proof of (P Xy) % 171.14/171.58 Found ((et (P Xy)) (fun (x3:((P Xy)->False))=> x00)) as proof of (P Xy) % 171.14/171.58 Found ((et (P Xy)) (fun (x3:((P Xy)->False))=> x00)) as proof of (P Xy) % 171.14/171.58 Found x10:False % 171.14/171.58 Found (fun (x3:((P Xy)->False))=> x10) as proof of False % 171.14/171.58 Found (fun (x3:((P Xy)->False))=> x10) as proof of (((P Xy)->False)->False) % 171.14/171.58 Found (et0 (fun (x3:((P Xy)->False))=> x10)) as proof of (P Xy) % 171.14/171.58 Found ((et (P Xy)) (fun (x3:((P Xy)->False))=> x10)) as proof of (P Xy) % 171.14/171.58 Found ((et (P Xy)) (fun (x3:((P Xy)->False))=> x10)) as proof of (P Xy) % 171.14/171.58 Found x00:False % 171.14/171.58 Found (fun (x3:(False->False))=> x00) as proof of False % 171.14/171.58 Found (fun (x3:(False->False))=> x00) as proof of ((False->False)->False) % 171.14/171.58 Found x10:False % 171.14/171.58 Found (fun (x3:(False->False))=> x10) as proof of False % 171.14/171.58 Found (fun (x3:(False->False))=> x10) as proof of ((False->False)->False) % 171.14/171.58 Found x00:False % 171.14/171.58 Found (fun (x3:(False->False))=> x00) as proof of False % 171.14/171.58 Found (fun (x3:(False->False))=> x00) as proof of ((False->False)->False) % 171.14/171.58 Found x10:False % 171.14/171.58 Found (fun (x3:(False->False))=> x10) as proof of False % 171.14/171.58 Found (fun (x3:(False->False))=> x10) as proof of ((False->False)->False) % 171.14/171.58 Found x4:(p Xx) % 171.14/171.58 Instantiate: Xy0:=Xx:nat % 171.14/171.58 Found x4 as proof of (p Xy0) % 171.14/171.58 Found (x30 x4) as proof of ((lessis Xx0) Xy0) % 171.14/171.58 Found ((x3 Xy0) x4) as proof of ((lessis Xx0) Xy0) % 171.14/171.58 Found ((x3 Xy0) x4) as proof of ((lessis Xx0) Xy0) % 171.14/171.58 Found ((x3 Xy0) x4) as proof of ((lessis Xx0) Xy0) % 171.14/171.58 Found x4:(p Xy) % 171.14/171.58 Instantiate: Xy0:=Xy:nat % 171.14/171.58 Found x4 as proof of (p Xy0) % 171.14/171.58 Found (x30 x4) as proof of ((lessis Xx0) Xy0) % 171.14/171.58 Found ((x3 Xy0) x4) as proof of ((lessis Xx0) Xy0) % 171.14/171.58 Found ((x3 Xy0) x4) as proof of ((lessis Xx0) Xy0) % 171.14/171.58 Found ((x3 Xy0) x4) as proof of ((lessis Xx0) Xy0) % 171.14/171.58 Found x10:False % 171.14/171.58 Found (fun (x3:(p Xx))=> x10) as proof of False % 171.14/171.58 Found (fun (x2:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))) (x3:(p Xx))=> x10) as proof of ((p Xx)->False) % 171.14/171.58 Found (fun (x2:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))) (x3:(p Xx))=> x10) as proof of ((forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))->((p Xx)->False)) % 171.14/171.58 Found x00:False % 171.14/171.58 Found (fun (x3:(p Xy))=> x00) as proof of False % 171.14/171.58 Found (fun (x2:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))) (x3:(p Xy))=> x00) as proof of ((p Xy)->False) % 171.14/171.58 Found (fun (x2:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))) (x3:(p Xy))=> x00) as proof of ((forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))->((p Xy)->False)) % 171.14/171.58 Found x10:False % 171.14/171.58 Found (fun (x4:(p Xx))=> x10) as proof of False % 171.14/171.58 Found (fun (x3:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))) (x4:(p Xx))=> x10) as proof of ((p Xx)->False) % 171.14/171.58 Found (fun (x3:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))) (x4:(p Xx))=> x10) as proof of ((forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))->((p Xx)->False)) % 171.14/171.58 Found x00:False % 171.14/171.58 Found (fun (x4:(p Xy))=> x00) as proof of False % 171.14/171.58 Found (fun (x3:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))) (x4:(p Xy))=> x00) as proof of ((p Xy)->False) % 171.14/171.58 Found (fun (x3:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))) (x4:(p Xy))=> x00) as proof of ((forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))->((p Xy)->False)) % 174.21/174.66 Found x00:False % 174.21/174.66 Found (fun (x5:(p Xy))=> x00) as proof of False % 174.21/174.66 Found (fun (x4:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))) (x5:(p Xy))=> x00) as proof of ((p Xy)->False) % 174.21/174.66 Found (fun (x4:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))) (x5:(p Xy))=> x00) as proof of ((forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))->((p Xy)->False)) % 174.21/174.66 Found x10:False % 174.21/174.66 Found (fun (x5:(p Xx))=> x10) as proof of False % 174.21/174.66 Found (fun (x4:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))) (x5:(p Xx))=> x10) as proof of ((p Xx)->False) % 174.21/174.66 Found (fun (x4:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))) (x5:(p Xx))=> x10) as proof of ((forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))->((p Xx)->False)) % 174.21/174.66 Found x00:False % 174.21/174.66 Found (fun (x5:(p Xy))=> x00) as proof of False % 174.21/174.66 Found (fun (x4:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))) (x5:(p Xy))=> x00) as proof of ((p Xy)->False) % 174.21/174.66 Found (fun (x4:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))) (x5:(p Xy))=> x00) as proof of ((forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))->((p Xy)->False)) % 174.21/174.66 Found x10:False % 174.21/174.66 Found (fun (x5:(p Xx))=> x10) as proof of False % 174.21/174.66 Found (fun (x4:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))) (x5:(p Xx))=> x10) as proof of ((p Xx)->False) % 174.21/174.66 Found (fun (x4:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))) (x5:(p Xx))=> x10) as proof of ((forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))->((p Xx)->False)) % 174.21/174.66 Found x2:((more Xx) Xy) % 174.21/174.66 Found x2 as proof of ((more Xx) Xy) % 174.21/174.66 Found x2:((more Xx) Xy) % 174.21/174.66 Found x2 as proof of ((more Xx) Xy) % 174.21/174.66 Found x2:((more Xy) Xx) % 174.21/174.66 Found x2 as proof of ((more Xy) Xx) % 174.21/174.66 Found x00:False % 174.21/174.66 Found (fun (x5:(p Xy))=> x00) as proof of False % 174.21/174.66 Found (fun (x5:(p Xy))=> x00) as proof of ((p Xy)->False) % 174.21/174.66 Found x10:False % 174.21/174.66 Found (fun (x5:(p Xx))=> x10) as proof of False % 174.21/174.66 Found (fun (x5:(p Xx))=> x10) as proof of ((p Xx)->False) % 174.21/174.66 Found x2:((more Xx) Xy) % 174.21/174.66 Found x2 as proof of ((more Xx) Xy) % 174.21/174.66 Found x2:((more Xx) Xy) % 174.21/174.66 Found x2 as proof of ((more Xx) Xy) % 174.21/174.66 Found x2:((more Xy) Xx) % 174.21/174.66 Found x2 as proof of ((more Xy) Xx) % 174.21/174.66 Found x2:((more Xx) Xy) % 174.21/174.66 Found x2 as proof of ((more Xx) Xy) % 174.21/174.66 Found x2:((more Xx) Xy) % 174.21/174.66 Found x2 as proof of ((more Xx) Xy) % 174.21/174.66 Found x2:((more Xx) Xy) % 174.21/174.66 Found x2 as proof of ((more Xx) Xy) % 174.21/174.66 Found x2:((more Xx) Xy) % 174.21/174.66 Found x2 as proof of ((more Xx) Xy) % 174.21/174.66 Found x00:False % 174.21/174.66 Found (fun (x5:(False->False))=> x00) as proof of False % 174.21/174.66 Found (fun (x5:(False->False))=> x00) as proof of ((False->False)->False) % 174.21/174.66 Found x10:False % 174.21/174.66 Found (fun (x5:(False->False))=> x10) as proof of False % 174.21/174.66 Found (fun (x5:(False->False))=> x10) as proof of ((False->False)->False) % 174.21/174.66 Found x2:((more Xy) Xx) % 174.21/174.66 Found x2 as proof of ((more Xy) Xx) % 174.21/174.66 Found x2:((more Xy) Xx) % 174.21/174.66 Found x2 as proof of ((more Xy) Xx) % 174.21/174.66 Found x2:((more Xy) Xx) % 174.21/174.66 Found x2 as proof of ((more Xy) Xx) % 174.21/174.66 Found x2:((more Xy) Xx) % 174.21/174.66 Found x2 as proof of ((more Xy) Xx) % 174.21/174.66 Found x2:((more Xy) Xx) % 174.21/174.66 Found x2 as proof of ((more Xy) Xx) % 174.21/174.66 Found x2:((more Xy) Xx) % 174.21/174.66 Found x2 as proof of ((more Xy) Xx) % 174.21/174.66 Found x2:((more Xy) Xx) % 174.21/174.66 Found x2 as proof of ((more Xy) Xx) % 174.21/174.66 Found x2:((more Xy) Xx) % 174.21/174.66 Found x2 as proof of ((more Xy) Xx) % 174.21/174.66 Found x600:=(x60 x5):((lessis Xx) Xy) % 174.21/174.66 Found (x60 x5) as proof of ((lessis Xx) Xy) % 174.21/174.66 Found ((x6 Xy) x5) as proof of ((lessis Xx) Xy) % 174.21/174.66 Found ((x6 Xy) x5) as proof of ((lessis Xx) Xy) % 174.21/174.66 Found ((satz10d0 ((x6 Xy) x5)) x3) as proof of False % 174.21/174.66 Found ((((satz10d Xx) Xy) ((x6 Xy) x5)) x3) as proof of False % 174.21/174.66 Found (fun (x7:(p Xx))=> ((((satz10d Xx) Xy) ((x6 Xy) x5)) x3)) as proof of False % 174.21/174.66 Found (fun (x6:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))) (x7:(p Xx))=> ((((satz10d Xx) Xy) ((x6 Xy) x5)) x3)) as proof of ((p Xx)->False) % 174.21/174.66 Found (fun (x6:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))) (x7:(p Xx))=> ((((satz10d Xx) Xy) ((x6 Xy) x5)) x3)) as proof of ((forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))->((p Xx)->False)) % 174.21/174.66 Found (x1 (fun (x6:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))) (x7:(p Xx))=> ((((satz10d Xx) Xy) ((x6 Xy) x5)) x3))) as proof of False % 174.21/174.66 Found (fun (x5:(p Xy))=> (x1 (fun (x6:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))) (x7:(p Xx))=> ((((satz10d Xx) Xy) ((x6 Xy) x5)) x3)))) as proof of False % 180.81/181.26 Found (fun (x4:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))) (x5:(p Xy))=> (x1 (fun (x6:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))) (x7:(p Xx))=> ((((satz10d Xx) Xy) ((x6 Xy) x5)) x3)))) as proof of ((p Xy)->False) % 180.81/181.26 Found (fun (x4:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))) (x5:(p Xy))=> (x1 (fun (x6:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))) (x7:(p Xx))=> ((((satz10d Xx) Xy) ((x6 Xy) x5)) x3)))) as proof of ((forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))->((p Xy)->False)) % 180.81/181.26 Found (x2 (fun (x4:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))) (x5:(p Xy))=> (x1 (fun (x6:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))) (x7:(p Xx))=> ((((satz10d Xx) Xy) ((x6 Xy) x5)) x3))))) as proof of False % 180.81/181.26 Found (fun (x3:((more Xx) Xy))=> (x2 (fun (x4:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))) (x5:(p Xy))=> (x1 (fun (x6:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))) (x7:(p Xx))=> ((((satz10d Xx) Xy) ((x6 Xy) x5)) x3)))))) as proof of False % 180.81/181.26 Found (fun (x3:((more Xx) Xy))=> (x2 (fun (x4:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))) (x5:(p Xy))=> (x1 (fun (x6:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))) (x7:(p Xx))=> ((((satz10d Xx) Xy) ((x6 Xy) x5)) x3)))))) as proof of (((more Xx) Xy)->False) % 180.81/181.26 Found eq_ref00:=(eq_ref0 Xx):(((eq nat) Xx) Xx) % 180.81/181.26 Found (eq_ref0 Xx) as proof of (((eq nat) Xx) b) % 180.81/181.26 Found ((eq_ref nat) Xx) as proof of (((eq nat) Xx) b) % 180.81/181.26 Found ((eq_ref nat) Xx) as proof of (((eq nat) Xx) b) % 180.81/181.26 Found ((eq_ref nat) Xx) as proof of (((eq nat) Xx) b) % 180.81/181.26 Found x00:False % 180.81/181.26 Found (fun (x4:(p Xy))=> x00) as proof of False % 180.81/181.26 Found (fun (x3:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))) (x4:(p Xy))=> x00) as proof of ((p Xy)->False) % 180.81/181.26 Found (fun (x3:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))) (x4:(p Xy))=> x00) as proof of ((forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))->((p Xy)->False)) % 180.81/181.26 Found x10:False % 180.81/181.26 Found (fun (x4:(p Xx))=> x10) as proof of False % 180.81/181.26 Found (fun (x3:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))) (x4:(p Xx))=> x10) as proof of ((p Xx)->False) % 180.81/181.26 Found (fun (x3:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))) (x4:(p Xx))=> x10) as proof of ((forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))->((p Xx)->False)) % 180.81/181.26 Found eq_ref000:=(eq_ref00 P):((P Xx)->(P Xx)) % 180.81/181.26 Found (eq_ref00 P) as proof of (P0 Xx) % 180.81/181.26 Found ((eq_ref0 Xx) P) as proof of (P0 Xx) % 180.81/181.26 Found (((eq_ref nat) Xx) P) as proof of (P0 Xx) % 180.81/181.26 Found (((eq_ref nat) Xx) P) as proof of (P0 Xx) % 180.81/181.26 Found x20:False % 180.81/181.26 Found (fun (x3:((more Xx) Xy))=> x20) as proof of False % 180.81/181.26 Found (fun (x3:((more Xx) Xy))=> x20) as proof of (((more Xx) Xy)->False) % 180.81/181.26 Found eq_ref000:=(eq_ref00 P):((P Xx)->(P Xx)) % 180.81/181.26 Found (eq_ref00 P) as proof of (P0 Xx) % 180.81/181.26 Found ((eq_ref0 Xx) P) as proof of (P0 Xx) % 180.81/181.26 Found (((eq_ref nat) Xx) P) as proof of (P0 Xx) % 180.81/181.26 Found (((eq_ref nat) Xx) P) as proof of (P0 Xx) % 180.81/181.26 Found x10:False % 180.81/181.26 Found (fun (x3:((more Xx) Xy))=> x10) as proof of False % 180.81/181.26 Found (fun (x3:((more Xx) Xy))=> x10) as proof of (((more Xx) Xy)->False) % 180.81/181.26 Found x2:((more Xy) Xx) % 180.81/181.26 Found x2 as proof of ((more Xy) Xx) % 180.81/181.26 Found x2:((more Xy) Xx) % 180.81/181.26 Found x2 as proof of ((more Xy) Xx) % 180.81/181.26 Found x10:False % 180.81/181.26 Found (fun (x4:(p Xx))=> x10) as proof of False % 180.81/181.26 Found (fun (x3:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))) (x4:(p Xx))=> x10) as proof of ((p Xx)->False) % 180.81/181.26 Found (fun (x3:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))) (x4:(p Xx))=> x10) as proof of ((forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))->((p Xx)->False)) % 180.81/181.26 Found x2:((more Xy) Xx) % 180.81/181.26 Found x2 as proof of ((more Xy) Xx) % 180.81/181.26 Found x10:False % 180.81/181.26 Found (fun (x4:(p Xx))=> x10) as proof of False % 180.81/181.26 Found (fun (x3:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))) (x4:(p Xx))=> x10) as proof of ((p Xx)->False) % 180.81/181.26 Found (fun (x3:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))) (x4:(p Xx))=> x10) as proof of ((forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))->((p Xx)->False)) % 180.81/181.26 Found x00:False % 180.81/181.26 Found (fun (x4:(p Xy))=> x00) as proof of False % 180.81/181.26 Found (fun (x3:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))) (x4:(p Xy))=> x00) as proof of ((p Xy)->False) % 189.35/189.73 Found (fun (x3:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))) (x4:(p Xy))=> x00) as proof of ((forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))->((p Xy)->False)) % 189.35/189.73 Found x00:False % 189.35/189.73 Found (fun (x4:(p Xy))=> x00) as proof of False % 189.35/189.73 Found (fun (x3:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))) (x4:(p Xy))=> x00) as proof of ((p Xy)->False) % 189.35/189.73 Found (fun (x3:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))) (x4:(p Xy))=> x00) as proof of ((forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))->((p Xy)->False)) % 189.35/189.73 Found x2:((more Xy) Xx) % 189.35/189.73 Found x2 as proof of ((more Xy) Xx) % 189.35/189.73 Found eq_ref000:=(eq_ref00 P1):((P1 Xy)->(P1 Xy)) % 189.35/189.73 Found (eq_ref00 P1) as proof of (P2 Xy) % 189.35/189.73 Found ((eq_ref0 Xy) P1) as proof of (P2 Xy) % 189.35/189.73 Found (((eq_ref nat) Xy) P1) as proof of (P2 Xy) % 189.35/189.73 Found (((eq_ref nat) Xy) P1) as proof of (P2 Xy) % 189.35/189.73 Found eq_ref000:=(eq_ref00 P1):((P1 Xy)->(P1 Xy)) % 189.35/189.73 Found (eq_ref00 P1) as proof of (P2 Xy) % 189.35/189.73 Found ((eq_ref0 Xy) P1) as proof of (P2 Xy) % 189.35/189.73 Found (((eq_ref nat) Xy) P1) as proof of (P2 Xy) % 189.35/189.73 Found (((eq_ref nat) Xy) P1) as proof of (P2 Xy) % 189.35/189.73 Found eq_ref000:=(eq_ref00 P):((P Xx)->(P Xx)) % 189.35/189.73 Found (eq_ref00 P) as proof of (P0 Xx) % 189.35/189.73 Found ((eq_ref0 Xx) P) as proof of (P0 Xx) % 189.35/189.73 Found (((eq_ref nat) Xx) P) as proof of (P0 Xx) % 189.35/189.73 Found (((eq_ref nat) Xx) P) as proof of (P0 Xx) % 189.35/189.73 Found eq_ref00:=(eq_ref0 Xx):(((eq nat) Xx) Xx) % 189.35/189.73 Found (eq_ref0 Xx) as proof of (((eq nat) Xx) b) % 189.35/189.73 Found ((eq_ref nat) Xx) as proof of (((eq nat) Xx) b) % 189.35/189.73 Found ((eq_ref nat) Xx) as proof of (((eq nat) Xx) b) % 189.35/189.73 Found ((eq_ref nat) Xx) as proof of (((eq nat) Xx) b) % 189.35/189.73 Found eq_ref00:=(eq_ref0 b):(((eq nat) b) b) % 189.35/189.73 Found (eq_ref0 b) as proof of (((eq nat) b) Xy) % 189.35/189.73 Found ((eq_ref nat) b) as proof of (((eq nat) b) Xy) % 189.35/189.73 Found ((eq_ref nat) b) as proof of (((eq nat) b) Xy) % 189.35/189.73 Found ((eq_ref nat) b) as proof of (((eq nat) b) Xy) % 189.35/189.73 Found eq_ref00:=(eq_ref0 Xx):(((eq nat) Xx) Xx) % 189.35/189.73 Found (eq_ref0 Xx) as proof of (((eq nat) Xx) b) % 189.35/189.73 Found ((eq_ref nat) Xx) as proof of (((eq nat) Xx) b) % 189.35/189.73 Found ((eq_ref nat) Xx) as proof of (((eq nat) Xx) b) % 189.35/189.73 Found ((eq_ref nat) Xx) as proof of (((eq nat) Xx) b) % 189.35/189.73 Found eq_ref00:=(eq_ref0 b):(((eq nat) b) b) % 189.35/189.73 Found (eq_ref0 b) as proof of (((eq nat) b) Xy) % 189.35/189.73 Found ((eq_ref nat) b) as proof of (((eq nat) b) Xy) % 189.35/189.73 Found ((eq_ref nat) b) as proof of (((eq nat) b) Xy) % 189.35/189.73 Found ((eq_ref nat) b) as proof of (((eq nat) b) Xy) % 189.35/189.73 Found x10:False % 189.35/189.73 Found (fun (x2:(((forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))->((p Xx)->False))->False))=> x10) as proof of False % 189.35/189.73 Found (fun (x2:(((forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))->((p Xx)->False))->False))=> x10) as proof of ((((forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))->((p Xx)->False))->False)->False) % 189.35/189.73 Found x00:False % 189.35/189.73 Found (fun (x2:(((forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))->((p Xy)->False))->False))=> x00) as proof of False % 189.35/189.73 Found (fun (x2:(((forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))->((p Xy)->False))->False))=> x00) as proof of ((((forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))->((p Xy)->False))->False)->False) % 189.35/189.73 Found eq_ref000:=(eq_ref00 P):((P Xx)->(P Xx)) % 189.35/189.73 Found (eq_ref00 P) as proof of (P0 Xx) % 189.35/189.73 Found ((eq_ref0 Xx) P) as proof of (P0 Xx) % 189.35/189.73 Found (((eq_ref nat) Xx) P) as proof of (P0 Xx) % 189.35/189.73 Found (((eq_ref nat) Xx) P) as proof of (P0 Xx) % 189.35/189.73 Found eq_ref000:=(eq_ref00 P):((P Xx)->(P Xx)) % 189.35/189.73 Found (eq_ref00 P) as proof of (P0 Xx) % 189.35/189.73 Found ((eq_ref0 Xx) P) as proof of (P0 Xx) % 189.35/189.73 Found (((eq_ref nat) Xx) P) as proof of (P0 Xx) % 189.35/189.73 Found (((eq_ref nat) Xx) P) as proof of (P0 Xx) % 189.35/189.73 Found x4:(p Xy) % 189.35/189.73 Instantiate: Xy0:=Xy:nat % 189.35/189.73 Found x4 as proof of (p Xy0) % 189.35/189.73 Found (x30 x4) as proof of ((lessis Xx0) Xy0) % 189.35/189.73 Found ((x3 Xy0) x4) as proof of ((lessis Xx0) Xy0) % 189.35/189.73 Found ((x3 Xy0) x4) as proof of ((lessis Xx0) Xy0) % 189.35/189.73 Found ((x3 Xy0) x4) as proof of ((lessis Xx0) Xy0) % 189.35/189.73 Found x4:(p Xx) % 189.35/189.73 Instantiate: Xy0:=Xx:nat % 189.35/189.73 Found x4 as proof of (p Xy0) % 189.35/189.73 Found (x30 x4) as proof of ((lessis Xx0) Xy0) % 189.35/189.73 Found ((x3 Xy0) x4) as proof of ((lessis Xx0) Xy0) % 189.35/189.73 Found ((x3 Xy0) x4) as proof of ((lessis Xx0) Xy0) % 189.35/189.73 Found ((x3 Xy0) x4) as proof of ((lessis Xx0) Xy0) % 189.35/189.73 Found eq_ref00:=(eq_ref0 b):(((eq nat) b) b) % 189.35/189.73 Found (eq_ref0 b) as proof of (P b) % 189.35/189.73 Found ((eq_ref nat) b) as proof of (P b) % 189.35/189.73 Found ((eq_ref nat) b) as proof of (P b) % 194.53/194.95 Found ((eq_ref nat) b) as proof of (P b) % 194.53/194.95 Found eq_ref00:=(eq_ref0 Xy):(((eq nat) Xy) Xy) % 194.53/194.95 Found (eq_ref0 Xy) as proof of (((eq nat) Xy) b) % 194.53/194.95 Found ((eq_ref nat) Xy) as proof of (((eq nat) Xy) b) % 194.53/194.95 Found ((eq_ref nat) Xy) as proof of (((eq nat) Xy) b) % 194.53/194.95 Found ((eq_ref nat) Xy) as proof of (((eq nat) Xy) b) % 194.53/194.95 Found x10:False % 194.53/194.95 Found (fun (x2:((more b) Xy))=> x10) as proof of False % 194.53/194.95 Found (fun (x2:((more b) Xy))=> x10) as proof of (((more b) Xy)->False) % 194.53/194.95 Found x00:False % 194.53/194.95 Found (fun (x2:((more b) Xy))=> x00) as proof of False % 194.53/194.95 Found (fun (x2:((more b) Xy))=> x00) as proof of (((more b) Xy)->False) % 194.53/194.95 Found x10:False % 194.53/194.95 Found (fun (x5:(p Xx))=> x10) as proof of False % 194.53/194.95 Found (fun (x4:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))) (x5:(p Xx))=> x10) as proof of ((p Xx)->False) % 194.53/194.95 Found (fun (x4:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))) (x5:(p Xx))=> x10) as proof of ((forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))->((p Xx)->False)) % 194.53/194.95 Found x00:False % 194.53/194.95 Found (fun (x5:(p Xy))=> x00) as proof of False % 194.53/194.96 Found (fun (x4:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))) (x5:(p Xy))=> x00) as proof of ((p Xy)->False) % 194.53/194.96 Found (fun (x4:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))) (x5:(p Xy))=> x00) as proof of ((forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))->((p Xy)->False)) % 194.53/194.96 Found x10:False % 194.53/194.96 Found (fun (x4:(p Xx))=> x10) as proof of False % 194.53/194.96 Found (fun (x4:(p Xx))=> x10) as proof of ((p Xx)->False) % 194.53/194.96 Found x00:False % 194.53/194.96 Found (fun (x2:(((lessis Xy) Xx)->False))=> x00) as proof of False % 194.53/194.96 Found (fun (x2:(((lessis Xy) Xx)->False))=> x00) as proof of ((((lessis Xy) Xx)->False)->False) % 194.53/194.96 Found (et0 (fun (x2:(((lessis Xy) Xx)->False))=> x00)) as proof of ((lessis Xy) Xx) % 194.53/194.96 Found ((et ((lessis Xy) Xx)) (fun (x2:(((lessis Xy) Xx)->False))=> x00)) as proof of ((lessis Xy) Xx) % 194.53/194.96 Found ((et ((lessis Xy) Xx)) (fun (x2:(((lessis Xy) Xx)->False))=> x00)) as proof of ((lessis Xy) Xx) % 194.53/194.96 Found x00:False % 194.53/194.96 Found (fun (x4:(p Xy))=> x00) as proof of False % 194.53/194.96 Found (fun (x4:(p Xy))=> x00) as proof of ((p Xy)->False) % 194.53/194.96 Found x10:False % 194.53/194.96 Found (fun (x2:(((lessis Xy) Xx)->False))=> x10) as proof of False % 194.53/194.96 Found (fun (x2:(((lessis Xy) Xx)->False))=> x10) as proof of ((((lessis Xy) Xx)->False)->False) % 194.53/194.96 Found (et0 (fun (x2:(((lessis Xy) Xx)->False))=> x10)) as proof of ((lessis Xy) Xx) % 194.53/194.96 Found ((et ((lessis Xy) Xx)) (fun (x2:(((lessis Xy) Xx)->False))=> x10)) as proof of ((lessis Xy) Xx) % 194.53/194.96 Found ((et ((lessis Xy) Xx)) (fun (x2:(((lessis Xy) Xx)->False))=> x10)) as proof of ((lessis Xy) Xx) % 194.53/194.96 Found x10:False % 194.53/194.96 Found (fun (x2:(((lessis Xy) Xx)->False))=> x10) as proof of False % 194.53/194.96 Found (fun (x2:(((lessis Xy) Xx)->False))=> x10) as proof of ((((lessis Xy) Xx)->False)->False) % 194.53/194.96 Found (et0 (fun (x2:(((lessis Xy) Xx)->False))=> x10)) as proof of ((lessis Xy) Xx) % 194.53/194.96 Found ((et ((lessis Xy) Xx)) (fun (x2:(((lessis Xy) Xx)->False))=> x10)) as proof of ((lessis Xy) Xx) % 194.53/194.96 Found ((et ((lessis Xy) Xx)) (fun (x2:(((lessis Xy) Xx)->False))=> x10)) as proof of ((lessis Xy) Xx) % 194.53/194.96 Found x00:False % 194.53/194.96 Found (fun (x2:(((lessis Xy) Xx)->False))=> x00) as proof of False % 194.53/194.96 Found (fun (x2:(((lessis Xy) Xx)->False))=> x00) as proof of ((((lessis Xy) Xx)->False)->False) % 194.53/194.96 Found (et0 (fun (x2:(((lessis Xy) Xx)->False))=> x00)) as proof of ((lessis Xy) Xx) % 194.53/194.96 Found ((et ((lessis Xy) Xx)) (fun (x2:(((lessis Xy) Xx)->False))=> x00)) as proof of ((lessis Xy) Xx) % 194.53/194.96 Found ((et ((lessis Xy) Xx)) (fun (x2:(((lessis Xy) Xx)->False))=> x00)) as proof of ((lessis Xy) Xx) % 194.53/194.96 Found x2:((more b) Xy) % 194.53/194.96 Found x2 as proof of ((more b) Xy) % 194.53/194.96 Found x2:((more b) Xy) % 194.53/194.96 Found x2 as proof of ((more b) Xy) % 194.53/194.96 Found x10:False % 194.53/194.96 Found (fun (x3:(p Xx))=> x10) as proof of False % 194.53/194.96 Found (fun (x3:(p Xx))=> x10) as proof of ((p Xx)->False) % 194.53/194.96 Found x00:False % 194.53/194.96 Found (fun (x3:(p Xy))=> x00) as proof of False % 194.53/194.96 Found (fun (x3:(p Xy))=> x00) as proof of ((p Xy)->False) % 194.53/194.96 Found satz2700:=(satz270 s):(some (fun (Xx:nat)=> (((forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))->((p Xx)->False))->False))) % 194.53/194.96 Found (satz270 s) as proof of (some (fun (Xx:nat)=> (((forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))->((p Xx)->False))->False))) % 194.53/194.96 Found ((satz27 p) s) as proof of (some (fun (Xx:nat)=> (((forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))->((p Xx)->False))->False))) % 206.00/206.45 Found ((satz27 p) s) as proof of (some (fun (Xx:nat)=> (((forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))->((p Xx)->False))->False))) % 206.00/206.45 Found x10:False % 206.00/206.45 Found (fun (x3:(((p Xx)->False)->False))=> x10) as proof of False % 206.00/206.45 Found (fun (x3:(((p Xx)->False)->False))=> x10) as proof of ((((p Xx)->False)->False)->False) % 206.00/206.45 Found x00:False % 206.00/206.45 Found (fun (x3:(((p Xy)->False)->False))=> x00) as proof of False % 206.00/206.45 Found (fun (x3:(((p Xy)->False)->False))=> x00) as proof of ((((p Xy)->False)->False)->False) % 206.00/206.45 Found satz2700:=(satz270 s):(some (fun (Xx:nat)=> (((forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))->((p Xx)->False))->False))) % 206.00/206.45 Found (satz270 s) as proof of (some (fun (Xx:nat)=> (((forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))->((p Xx)->False))->False))) % 206.00/206.45 Found ((satz27 p) s) as proof of (some (fun (Xx:nat)=> (((forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))->((p Xx)->False))->False))) % 206.00/206.45 Found ((satz27 p) s) as proof of (some (fun (Xx:nat)=> (((forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))->((p Xx)->False))->False))) % 206.00/206.45 Found x10:False % 206.00/206.45 Found (fun (x3:(False->False))=> x10) as proof of False % 206.00/206.45 Found (fun (x3:(False->False))=> x10) as proof of ((False->False)->False) % 206.00/206.45 Found x00:False % 206.00/206.45 Found (fun (x3:(False->False))=> x00) as proof of False % 206.00/206.45 Found (fun (x3:(False->False))=> x00) as proof of ((False->False)->False) % 206.00/206.45 Found x2:((more Xy) b) % 206.00/206.45 Found x2 as proof of ((more Xy) b) % 206.00/206.45 Found x2:((more Xy) b) % 206.00/206.45 Found x2 as proof of ((more Xy) b) % 206.00/206.45 Found x2:((more b) Xy) % 206.00/206.45 Found x2 as proof of ((more b) Xy) % 206.00/206.45 Found x2:((more Xy) Xx) % 206.00/206.45 Found x2 as proof of ((more Xy) Xx) % 206.00/206.45 Found x2:((more Xy) Xx) % 206.00/206.45 Found x2 as proof of ((more Xy) Xx) % 206.00/206.45 Found x5:(p Xy) % 206.00/206.45 Instantiate: Xy0:=Xy:nat % 206.00/206.45 Found x5 as proof of (p Xy0) % 206.00/206.45 Found (x40 x5) as proof of ((lessis Xx0) Xy0) % 206.00/206.45 Found ((x4 Xy0) x5) as proof of ((lessis Xx0) Xy0) % 206.00/206.45 Found ((x4 Xy0) x5) as proof of ((lessis Xx0) Xy0) % 206.00/206.45 Found ((x4 Xy0) x5) as proof of ((lessis Xx0) Xy0) % 206.00/206.45 Found x3:(P Xy) % 206.00/206.45 Instantiate: b:=Xy:nat % 206.00/206.45 Found x3 as proof of (P0 b) % 206.00/206.45 Found eq_ref00:=(eq_ref0 Xx):(((eq nat) Xx) Xx) % 206.00/206.45 Found (eq_ref0 Xx) as proof of (((eq nat) Xx) b) % 206.00/206.45 Found ((eq_ref nat) Xx) as proof of (((eq nat) Xx) b) % 206.00/206.45 Found ((eq_ref nat) Xx) as proof of (((eq nat) Xx) b) % 206.00/206.45 Found ((eq_ref nat) Xx) as proof of (((eq nat) Xx) b) % 206.00/206.45 Found x5:(p Xx) % 206.00/206.45 Instantiate: Xy0:=Xx:nat % 206.00/206.45 Found x5 as proof of (p Xy0) % 206.00/206.45 Found (x40 x5) as proof of ((lessis Xx0) Xy0) % 206.00/206.45 Found ((x4 Xy0) x5) as proof of ((lessis Xx0) Xy0) % 206.00/206.45 Found ((x4 Xy0) x5) as proof of ((lessis Xx0) Xy0) % 206.00/206.45 Found ((x4 Xy0) x5) as proof of ((lessis Xx0) Xy0) % 206.00/206.45 Found x3:(P Xy) % 206.00/206.45 Instantiate: Xy0:=Xy:nat % 206.00/206.45 Found x3 as proof of (P0 Xy0) % 206.00/206.45 Found eq_ref000:=(eq_ref00 P):((P b)->(P b)) % 206.00/206.45 Found (eq_ref00 P) as proof of (P0 b) % 206.00/206.45 Found ((eq_ref0 b) P) as proof of (P0 b) % 206.00/206.45 Found (((eq_ref nat) b) P) as proof of (P0 b) % 206.00/206.45 Found (((eq_ref nat) b) P) as proof of (P0 b) % 206.00/206.45 Found x00:False % 206.00/206.45 Found (fun (x3:(p Xy))=> x00) as proof of False % 206.00/206.45 Found (fun (x3:(p Xy))=> x00) as proof of ((p Xy)->False) % 206.00/206.45 Found x10:False % 206.00/206.45 Found (fun (x3:(p Xx))=> x10) as proof of False % 206.00/206.45 Found (fun (x3:(p Xx))=> x10) as proof of ((p Xx)->False) % 206.00/206.45 Found x10:False % 206.00/206.45 Found (fun (x4:(p Xx))=> x10) as proof of False % 206.00/206.45 Found (fun (x3:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))) (x4:(p Xx))=> x10) as proof of ((p Xx)->False) % 206.00/206.45 Found (fun (x3:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))) (x4:(p Xx))=> x10) as proof of ((forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))->((p Xx)->False)) % 206.00/206.45 Found x00:False % 206.00/206.45 Found (fun (x4:(p Xy))=> x00) as proof of False % 206.00/206.45 Found (fun (x3:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))) (x4:(p Xy))=> x00) as proof of ((p Xy)->False) % 206.00/206.45 Found (fun (x3:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))) (x4:(p Xy))=> x00) as proof of ((forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))->((p Xy)->False)) % 206.00/206.45 Found x2:((more Xy) Xx) % 206.00/206.45 Found x2 as proof of ((more Xy) Xx) % 206.00/206.45 Found x2:((more Xy) Xx) % 206.00/206.45 Found x2 as proof of ((more Xy) Xx) % 206.00/206.45 Found x2:((more Xy) Xx) % 206.00/206.45 Found x2 as proof of ((more Xy) Xx) % 206.00/206.45 Found x2:((more Xy) Xx) % 206.00/206.45 Found x2 as proof of ((more Xy) Xx) % 206.00/206.45 Found x10:False % 206.00/206.45 Found (fun (x4:(False->False))=> x10) as proof of False % 219.23/219.63 Found (fun (x4:(False->False))=> x10) as proof of ((False->False)->False) % 219.23/219.63 Found x00:False % 219.23/219.63 Found (fun (x2:((((eq nat) Xy) b)->False))=> x00) as proof of False % 219.23/219.63 Found (fun (x2:((((eq nat) Xy) b)->False))=> x00) as proof of (((((eq nat) Xy) b)->False)->False) % 219.23/219.63 Found x10:False % 219.23/219.63 Found (fun (x2:((((eq nat) Xy) b)->False))=> x10) as proof of False % 219.23/219.63 Found (fun (x2:((((eq nat) Xy) b)->False))=> x10) as proof of (((((eq nat) Xy) b)->False)->False) % 219.23/219.63 Found x00:False % 219.23/219.63 Found (fun (x4:(False->False))=> x00) as proof of False % 219.23/219.63 Found (fun (x4:(False->False))=> x00) as proof of ((False->False)->False) % 219.23/219.63 Found x00:False % 219.23/219.63 Found (fun (x2:((((eq nat) Xy) b)->False))=> x00) as proof of False % 219.23/219.63 Found (fun (x2:((((eq nat) Xy) b)->False))=> x00) as proof of (((((eq nat) Xy) b)->False)->False) % 219.23/219.63 Found x10:False % 219.23/219.63 Found (fun (x2:((((eq nat) Xy) b)->False))=> x10) as proof of False % 219.23/219.63 Found (fun (x2:((((eq nat) Xy) b)->False))=> x10) as proof of (((((eq nat) Xy) b)->False)->False) % 219.23/219.63 Found x2:((more Xx) Xy) % 219.23/219.63 Found x2 as proof of ((more Xx) Xy) % 219.23/219.63 Found x00:False % 219.23/219.63 Found (fun (x3:(p Xy))=> x00) as proof of False % 219.23/219.63 Found (fun (x2:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))) (x3:(p Xy))=> x00) as proof of ((p Xy)->False) % 219.23/219.63 Found (fun (x2:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))) (x3:(p Xy))=> x00) as proof of ((forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))->((p Xy)->False)) % 219.23/219.63 Found x10:False % 219.23/219.63 Found (fun (x3:(p Xx))=> x10) as proof of False % 219.23/219.63 Found (fun (x2:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))) (x3:(p Xx))=> x10) as proof of ((p Xx)->False) % 219.23/219.63 Found (fun (x2:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))) (x3:(p Xx))=> x10) as proof of ((forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))->((p Xx)->False)) % 219.23/219.63 Found eq_ref00:=(eq_ref0 Xx):(((eq nat) Xx) Xx) % 219.23/219.63 Found (eq_ref0 Xx) as proof of (((eq nat) Xx) b0) % 219.23/219.63 Found ((eq_ref nat) Xx) as proof of (((eq nat) Xx) b0) % 219.23/219.63 Found ((eq_ref nat) Xx) as proof of (((eq nat) Xx) b0) % 219.23/219.63 Found ((eq_ref nat) Xx) as proof of (((eq nat) Xx) b0) % 219.23/219.63 Found eq_ref00:=(eq_ref0 b0):(((eq nat) b0) b0) % 219.23/219.63 Found (eq_ref0 b0) as proof of (((eq nat) b0) Xy) % 219.23/219.63 Found ((eq_ref nat) b0) as proof of (((eq nat) b0) Xy) % 219.23/219.63 Found ((eq_ref nat) b0) as proof of (((eq nat) b0) Xy) % 219.23/219.63 Found ((eq_ref nat) b0) as proof of (((eq nat) b0) Xy) % 219.23/219.63 Found x10:False % 219.23/219.63 Found (fun (x2:(((lessis Xx) Xy)->False))=> x10) as proof of False % 219.23/219.63 Found (fun (x2:(((lessis Xx) Xy)->False))=> x10) as proof of ((((lessis Xx) Xy)->False)->False) % 219.23/219.63 Found (et0 (fun (x2:(((lessis Xx) Xy)->False))=> x10)) as proof of ((lessis Xx) Xy) % 219.23/219.63 Found ((et ((lessis Xx) Xy)) (fun (x2:(((lessis Xx) Xy)->False))=> x10)) as proof of ((lessis Xx) Xy) % 219.23/219.63 Found ((et ((lessis Xx) Xy)) (fun (x2:(((lessis Xx) Xy)->False))=> x10)) as proof of ((lessis Xx) Xy) % 219.23/219.63 Found x00:False % 219.23/219.63 Found (fun (x2:(((lessis Xx) Xy)->False))=> x00) as proof of False % 219.23/219.63 Found (fun (x2:(((lessis Xx) Xy)->False))=> x00) as proof of ((((lessis Xx) Xy)->False)->False) % 219.23/219.63 Found (et0 (fun (x2:(((lessis Xx) Xy)->False))=> x00)) as proof of ((lessis Xx) Xy) % 219.23/219.63 Found ((et ((lessis Xx) Xy)) (fun (x2:(((lessis Xx) Xy)->False))=> x00)) as proof of ((lessis Xx) Xy) % 219.23/219.63 Found ((et ((lessis Xx) Xy)) (fun (x2:(((lessis Xx) Xy)->False))=> x00)) as proof of ((lessis Xx) Xy) % 219.23/219.63 Found x500:=(x50 x4):((lessis Xx) Xy) % 219.23/219.63 Found (x50 x4) as proof of ((lessis Xx) Xy) % 219.23/219.63 Found ((x5 Xy) x4) as proof of ((lessis Xx) Xy) % 219.23/219.63 Found ((x5 Xy) x4) as proof of ((lessis Xx) Xy) % 219.23/219.63 Found ((satz10d0 ((x5 Xy) x4)) x2) as proof of False % 219.23/219.63 Found ((((satz10d Xx) Xy) ((x5 Xy) x4)) x2) as proof of False % 219.23/219.63 Found (fun (x6:(p Xx))=> ((((satz10d Xx) Xy) ((x5 Xy) x4)) x2)) as proof of False % 219.23/219.63 Found (fun (x5:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))) (x6:(p Xx))=> ((((satz10d Xx) Xy) ((x5 Xy) x4)) x2)) as proof of ((p Xx)->False) % 219.23/219.63 Found (fun (x5:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))) (x6:(p Xx))=> ((((satz10d Xx) Xy) ((x5 Xy) x4)) x2)) as proof of ((forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))->((p Xx)->False)) % 219.23/219.63 Found (x0 (fun (x5:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))) (x6:(p Xx))=> ((((satz10d Xx) Xy) ((x5 Xy) x4)) x2))) as proof of False % 219.23/219.63 Found (fun (x4:(p Xy))=> (x0 (fun (x5:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))) (x6:(p Xx))=> ((((satz10d Xx) Xy) ((x5 Xy) x4)) x2)))) as proof of False % 220.06/220.51 Found (fun (x3:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))) (x4:(p Xy))=> (x0 (fun (x5:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))) (x6:(p Xx))=> ((((satz10d Xx) Xy) ((x5 Xy) x4)) x2)))) as proof of ((p Xy)->False) % 220.06/220.51 Found (fun (x3:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))) (x4:(p Xy))=> (x0 (fun (x5:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))) (x6:(p Xx))=> ((((satz10d Xx) Xy) ((x5 Xy) x4)) x2)))) as proof of ((forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))->((p Xy)->False)) % 220.06/220.51 Found (x1 (fun (x3:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))) (x4:(p Xy))=> (x0 (fun (x5:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))) (x6:(p Xx))=> ((((satz10d Xx) Xy) ((x5 Xy) x4)) x2))))) as proof of False % 220.06/220.51 Found (fun (x2:((more Xx) Xy))=> (x1 (fun (x3:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))) (x4:(p Xy))=> (x0 (fun (x5:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))) (x6:(p Xx))=> ((((satz10d Xx) Xy) ((x5 Xy) x4)) x2)))))) as proof of False % 220.06/220.51 Found (fun (x2:((more Xx) Xy))=> (x1 (fun (x3:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))) (x4:(p Xy))=> (x0 (fun (x5:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))) (x6:(p Xx))=> ((((satz10d Xx) Xy) ((x5 Xy) x4)) x2)))))) as proof of (((more Xx) Xy)->False) % 220.06/220.51 Found x10:False % 220.06/220.51 Found (fun (x4:(p Xx))=> x10) as proof of False % 220.06/220.51 Found (fun (x4:(p Xx))=> x10) as proof of ((p Xx)->False) % 220.06/220.51 Found x00:False % 220.06/220.51 Found (fun (x4:(p Xy))=> x00) as proof of False % 220.06/220.51 Found (fun (x4:(p Xy))=> x00) as proof of ((p Xy)->False) % 220.06/220.51 Found x10:False % 220.06/220.51 Found (fun (x4:(p Xx))=> x10) as proof of False % 220.06/220.51 Found (fun (x3:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))) (x4:(p Xx))=> x10) as proof of ((p Xx)->False) % 220.06/220.51 Found (fun (x3:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))) (x4:(p Xx))=> x10) as proof of ((forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))->((p Xx)->False)) % 220.06/220.51 Found x00:False % 220.06/220.51 Found (fun (x4:(p Xy))=> x00) as proof of False % 220.13/220.51 Found (fun (x3:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))) (x4:(p Xy))=> x00) as proof of ((p Xy)->False) % 220.13/220.51 Found (fun (x3:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))) (x4:(p Xy))=> x00) as proof of ((forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))->((p Xy)->False)) % 220.13/220.51 Found x500:=(x50 x4):((lessis Xx) Xy) % 220.13/220.51 Found (x50 x4) as proof of ((lessis Xx) Xy) % 220.13/220.51 Found ((x5 Xy) x4) as proof of ((lessis Xx) Xy) % 220.13/220.51 Found ((x5 Xy) x4) as proof of ((lessis Xx) Xy) % 220.13/220.51 Found ((satz10d0 ((x5 Xy) x4)) x2) as proof of False % 220.13/220.51 Found ((((satz10d Xx) Xy) ((x5 Xy) x4)) x2) as proof of False % 220.13/220.51 Found (fun (x6:(p Xx))=> ((((satz10d Xx) Xy) ((x5 Xy) x4)) x2)) as proof of False % 220.13/220.51 Found (fun (x5:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))) (x6:(p Xx))=> ((((satz10d Xx) Xy) ((x5 Xy) x4)) x2)) as proof of ((p Xx)->False) % 220.13/220.51 Found (fun (x5:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))) (x6:(p Xx))=> ((((satz10d Xx) Xy) ((x5 Xy) x4)) x2)) as proof of ((forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))->((p Xx)->False)) % 220.13/220.51 Found (x0 (fun (x5:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))) (x6:(p Xx))=> ((((satz10d Xx) Xy) ((x5 Xy) x4)) x2))) as proof of False % 220.13/220.51 Found (fun (x4:(p Xy))=> (x0 (fun (x5:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))) (x6:(p Xx))=> ((((satz10d Xx) Xy) ((x5 Xy) x4)) x2)))) as proof of False % 220.13/220.51 Found (fun (x3:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))) (x4:(p Xy))=> (x0 (fun (x5:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))) (x6:(p Xx))=> ((((satz10d Xx) Xy) ((x5 Xy) x4)) x2)))) as proof of ((p Xy)->False) % 220.13/220.51 Found (fun (x3:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))) (x4:(p Xy))=> (x0 (fun (x5:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))) (x6:(p Xx))=> ((((satz10d Xx) Xy) ((x5 Xy) x4)) x2)))) as proof of ((forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))->((p Xy)->False)) % 220.13/220.51 Found (x1 (fun (x3:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))) (x4:(p Xy))=> (x0 (fun (x5:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))) (x6:(p Xx))=> ((((satz10d Xx) Xy) ((x5 Xy) x4)) x2))))) as proof of False % 227.06/227.50 Found (fun (x2:((more Xx) Xy))=> (x1 (fun (x3:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))) (x4:(p Xy))=> (x0 (fun (x5:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))) (x6:(p Xx))=> ((((satz10d Xx) Xy) ((x5 Xy) x4)) x2)))))) as proof of False % 227.06/227.50 Found (fun (x2:((more Xx) Xy))=> (x1 (fun (x3:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))) (x4:(p Xy))=> (x0 (fun (x5:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))) (x6:(p Xx))=> ((((satz10d Xx) Xy) ((x5 Xy) x4)) x2)))))) as proof of (((more Xx) Xy)->False) % 227.06/227.50 Found x10:False % 227.06/227.50 Found (fun (x4:(p Xx))=> x10) as proof of False % 227.06/227.50 Found (fun (x4:(p Xx))=> x10) as proof of ((p Xx)->False) % 227.06/227.50 Found x00:False % 227.06/227.50 Found (fun (x4:(p Xy))=> x00) as proof of False % 227.06/227.50 Found (fun (x4:(p Xy))=> x00) as proof of ((p Xy)->False) % 227.06/227.50 Found x10:False % 227.06/227.50 Found (fun (x4:(p Xx))=> x10) as proof of False % 227.06/227.50 Found (fun (x3:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))) (x4:(p Xx))=> x10) as proof of ((p Xx)->False) % 227.06/227.50 Found (fun (x3:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))) (x4:(p Xx))=> x10) as proof of ((forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))->((p Xx)->False)) % 227.06/227.50 Found x00:False % 227.06/227.50 Found (fun (x4:(p Xy))=> x00) as proof of False % 227.06/227.50 Found (fun (x3:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))) (x4:(p Xy))=> x00) as proof of ((p Xy)->False) % 227.06/227.50 Found (fun (x3:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))) (x4:(p Xy))=> x00) as proof of ((forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))->((p Xy)->False)) % 227.06/227.50 Found eq_ref000:=(eq_ref00 P):((P Xx)->(P Xx)) % 227.06/227.50 Found (eq_ref00 P) as proof of (P0 Xx) % 227.06/227.50 Found ((eq_ref0 Xx) P) as proof of (P0 Xx) % 227.06/227.50 Found (((eq_ref nat) Xx) P) as proof of (P0 Xx) % 227.06/227.50 Found (((eq_ref nat) Xx) P) as proof of (P0 Xx) % 227.06/227.50 Found x20:False % 227.06/227.50 Found (fun (x5:(p Xx))=> x20) as proof of False % 227.06/227.50 Found (fun (x5:(p Xx))=> x20) as proof of ((p Xx)->False) % 227.06/227.50 Found x10:False % 227.06/227.50 Found (fun (x5:(p Xy))=> x10) as proof of False % 227.06/227.50 Found (fun (x5:(p Xy))=> x10) as proof of ((p Xy)->False) % 227.06/227.50 Found x20:False % 227.06/227.50 Found (fun (x5:(p Xx))=> x20) as proof of False % 227.06/227.50 Found (fun (x5:(p Xx))=> x20) as proof of ((p Xx)->False) % 227.06/227.50 Found x10:False % 227.06/227.50 Found (fun (x5:(p Xy))=> x10) as proof of False % 227.06/227.50 Found (fun (x5:(p Xy))=> x10) as proof of ((p Xy)->False) % 227.06/227.50 Found x10:False % 227.06/227.50 Found (fun (x3:(p Xx))=> x10) as proof of False % 227.06/227.50 Found (fun (x3:(p Xx))=> x10) as proof of ((p Xx)->False) % 227.06/227.50 Found x00:False % 227.06/227.50 Found (fun (x3:(p Xy))=> x00) as proof of False % 227.06/227.50 Found (fun (x3:(p Xy))=> x00) as proof of ((p Xy)->False) % 227.06/227.50 Found eq_ref000:=(eq_ref00 P):((P b)->(P b)) % 227.06/227.50 Found (eq_ref00 P) as proof of (P0 b) % 227.06/227.50 Found ((eq_ref0 b) P) as proof of (P0 b) % 227.06/227.50 Found (((eq_ref nat) b) P) as proof of (P0 b) % 227.06/227.50 Found (((eq_ref nat) b) P) as proof of (P0 b) % 227.06/227.50 Found x10:False % 227.06/227.50 Found (fun (x3:(p Xx))=> x10) as proof of False % 227.06/227.50 Found (fun (x2:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))) (x3:(p Xx))=> x10) as proof of ((p Xx)->False) % 227.06/227.50 Found (fun (x2:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))) (x3:(p Xx))=> x10) as proof of ((forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))->((p Xx)->False)) % 227.06/227.50 Found x00:False % 227.06/227.50 Found (fun (x3:(p Xy))=> x00) as proof of False % 227.06/227.50 Found (fun (x2:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))) (x3:(p Xy))=> x00) as proof of ((p Xy)->False) % 227.06/227.50 Found (fun (x2:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))) (x3:(p Xy))=> x00) as proof of ((forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))->((p Xy)->False)) % 227.06/227.50 Found x10:False % 227.06/227.50 Found (fun (x3:((more Xy) Xx))=> x10) as proof of False % 227.06/227.50 Found (fun (x3:((more Xy) Xx))=> x10) as proof of (((more Xy) Xx)->False) % 227.06/227.50 Found x10:False % 227.06/227.50 Found (fun (x3:((more Xy) Xx))=> x10) as proof of False % 227.06/227.50 Found (fun (x3:((more Xy) Xx))=> x10) as proof of (((more Xy) Xx)->False) % 227.06/227.50 Found x10:False % 227.06/227.50 Found (fun (x3:((more Xy) Xx))=> x10) as proof of False % 227.06/227.50 Found (fun (x3:((more Xy) Xx))=> x10) as proof of (((more Xy) Xx)->False) % 227.06/227.50 Found x20:False % 227.06/227.50 Found (fun (x3:((more Xy) Xx))=> x20) as proof of False % 227.06/227.50 Found (fun (x3:((more Xy) Xx))=> x20) as proof of (((more Xy) Xx)->False) % 227.06/227.50 Found x20:False % 227.06/227.50 Found (fun (x3:((more Xy) Xx))=> x20) as proof of False % 227.06/227.50 Found (fun (x3:((more Xy) Xx))=> x20) as proof of (((more Xy) Xx)->False) % 227.06/227.50 Found x20:False % 238.87/239.29 Found (fun (x3:((more Xy) Xx))=> x20) as proof of False % 238.87/239.29 Found (fun (x3:((more Xy) Xx))=> x20) as proof of (((more Xy) Xx)->False) % 238.87/239.29 Found x20:False % 238.87/239.29 Found (fun (x3:((more Xy) Xx))=> x20) as proof of False % 238.87/239.29 Found (fun (x3:((more Xy) Xx))=> x20) as proof of (((more Xy) Xx)->False) % 238.87/239.29 Found x10:False % 238.87/239.29 Found (fun (x3:((more Xy) Xx))=> x10) as proof of False % 238.87/239.29 Found (fun (x3:((more Xy) Xx))=> x10) as proof of (((more Xy) Xx)->False) % 238.87/239.29 Found x10:False % 238.87/239.29 Found (fun (x2:(((P Xy)->(P b))->False))=> x10) as proof of False % 238.87/239.29 Found (fun (x2:(((P Xy)->(P b))->False))=> x10) as proof of ((((P Xy)->(P b))->False)->False) % 238.87/239.29 Found x10:False % 238.87/239.29 Found (fun (x2:(((P Xy)->(P b))->False))=> x10) as proof of False % 238.87/239.29 Found (fun (x2:(((P Xy)->(P b))->False))=> x10) as proof of ((((P Xy)->(P b))->False)->False) % 238.87/239.29 Found x00:False % 238.87/239.29 Found (fun (x2:(((P Xy)->(P b))->False))=> x00) as proof of False % 238.87/239.29 Found (fun (x2:(((P Xy)->(P b))->False))=> x00) as proof of ((((P Xy)->(P b))->False)->False) % 238.87/239.29 Found x00:False % 238.87/239.29 Found (fun (x2:(((P Xy)->(P b))->False))=> x00) as proof of False % 238.87/239.29 Found (fun (x2:(((P Xy)->(P b))->False))=> x00) as proof of ((((P Xy)->(P b))->False)->False) % 238.87/239.29 Found eq_ref000:=(eq_ref00 P):((P Xx)->(P Xx)) % 238.87/239.29 Found (eq_ref00 P) as proof of (P0 Xx) % 238.87/239.29 Found ((eq_ref0 Xx) P) as proof of (P0 Xx) % 238.87/239.29 Found (((eq_ref nat) Xx) P) as proof of (P0 Xx) % 238.87/239.29 Found (((eq_ref nat) Xx) P) as proof of (P0 Xx) % 238.87/239.29 Found x6:(p Xx) % 238.87/239.29 Instantiate: Xy0:=Xx:nat % 238.87/239.29 Found x6 as proof of (p Xy0) % 238.87/239.29 Found (x50 x6) as proof of ((lessis Xx0) Xy0) % 238.87/239.29 Found ((x5 Xy0) x6) as proof of ((lessis Xx0) Xy0) % 238.87/239.29 Found ((x5 Xy0) x6) as proof of ((lessis Xx0) Xy0) % 238.87/239.29 Found ((x5 Xy0) x6) as proof of ((lessis Xx0) Xy0) % 238.87/239.29 Found x6:(p Xy) % 238.87/239.29 Instantiate: Xy0:=Xy:nat % 238.87/239.29 Found x6 as proof of (p Xy0) % 238.87/239.29 Found (x30 x6) as proof of ((lessis Xx0) Xy0) % 238.87/239.29 Found ((x3 Xy0) x6) as proof of ((lessis Xx0) Xy0) % 238.87/239.29 Found ((x3 Xy0) x6) as proof of ((lessis Xx0) Xy0) % 238.87/239.29 Found ((x3 Xy0) x6) as proof of ((lessis Xx0) Xy0) % 238.87/239.29 Found x3:((more Xx) Xy) % 238.87/239.29 Found x3 as proof of ((more Xx) Xy) % 238.87/239.29 Found x3:((more Xx) Xy) % 238.87/239.29 Found x3 as proof of ((more Xx) Xy) % 238.87/239.29 Found x3:((more Xx) Xy) % 238.87/239.29 Found x3 as proof of ((more Xx) Xy) % 238.87/239.29 Found x3:((more Xx) Xy) % 238.87/239.29 Found x3 as proof of ((more Xx) Xy) % 238.87/239.29 Found x00:False % 238.87/239.29 Found (fun (x2:(((forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))->((p Xy)->False))->False))=> x00) as proof of False % 238.87/239.29 Found (fun (x2:(((forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))->((p Xy)->False))->False))=> x00) as proof of ((((forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))->((p Xy)->False))->False)->False) % 238.87/239.29 Found x10:False % 238.87/239.29 Found (fun (x4:(p Xx))=> x10) as proof of False % 238.87/239.29 Found (fun (x4:(p Xx))=> x10) as proof of ((p Xx)->False) % 238.87/239.29 Found x00:False % 238.87/239.29 Found (fun (x4:(p Xy))=> x00) as proof of False % 238.87/239.29 Found (fun (x4:(p Xy))=> x00) as proof of ((p Xy)->False) % 238.87/239.29 Found x10:False % 238.87/239.29 Found (fun (x5:(p Xy))=> x10) as proof of False % 238.87/239.29 Found (fun (x4:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))) (x5:(p Xy))=> x10) as proof of ((p Xy)->False) % 238.87/239.29 Found (fun (x4:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))) (x5:(p Xy))=> x10) as proof of ((forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))->((p Xy)->False)) % 238.87/239.29 Found x20:False % 238.87/239.29 Found (fun (x5:(p Xx))=> x20) as proof of False % 238.87/239.29 Found (fun (x4:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))) (x5:(p Xx))=> x20) as proof of ((p Xx)->False) % 238.87/239.29 Found (fun (x4:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))) (x5:(p Xx))=> x20) as proof of ((forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))->((p Xx)->False)) % 238.87/239.29 Found x10:False % 238.87/239.29 Found (fun (x5:(p Xy))=> x10) as proof of False % 238.87/239.29 Found (fun (x4:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))) (x5:(p Xy))=> x10) as proof of ((p Xy)->False) % 238.87/239.29 Found (fun (x4:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))) (x5:(p Xy))=> x10) as proof of ((forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))->((p Xy)->False)) % 238.87/239.29 Found x10:False % 238.87/239.29 Found (fun (x2:(((forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))->((p Xx)->False))->False))=> x10) as proof of False % 238.87/239.29 Found (fun (x2:(((forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))->((p Xx)->False))->False))=> x10) as proof of ((((forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))->((p Xx)->False))->False)->False) % 251.31/251.70 Found x20:False % 251.31/251.70 Found (fun (x5:(p Xx))=> x20) as proof of False % 251.31/251.70 Found (fun (x4:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))) (x5:(p Xx))=> x20) as proof of ((p Xx)->False) % 251.31/251.70 Found (fun (x4:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))) (x5:(p Xx))=> x20) as proof of ((forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))->((p Xx)->False)) % 251.31/251.70 Found x10:False % 251.31/251.70 Found (fun (x3:(p Xx))=> x10) as proof of False % 251.31/251.70 Found (fun (x2:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))) (x3:(p Xx))=> x10) as proof of ((p Xx)->False) % 251.31/251.70 Found (fun (x2:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))) (x3:(p Xx))=> x10) as proof of ((forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))->((p Xx)->False)) % 251.31/251.70 Found x00:False % 251.31/251.70 Found (fun (x3:(p Xy))=> x00) as proof of False % 251.31/251.70 Found (fun (x2:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))) (x3:(p Xy))=> x00) as proof of ((p Xy)->False) % 251.31/251.70 Found (fun (x2:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))) (x3:(p Xy))=> x00) as proof of ((forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))->((p Xy)->False)) % 251.31/251.70 Found eq_ref000:=(eq_ref00 P1):((P1 Xy)->(P1 Xy)) % 251.31/251.70 Found (eq_ref00 P1) as proof of (P2 Xy) % 251.31/251.70 Found ((eq_ref0 Xy) P1) as proof of (P2 Xy) % 251.31/251.70 Found (((eq_ref nat) Xy) P1) as proof of (P2 Xy) % 251.31/251.70 Found (((eq_ref nat) Xy) P1) as proof of (P2 Xy) % 251.31/251.70 Found eq_ref000:=(eq_ref00 P1):((P1 Xy)->(P1 Xy)) % 251.31/251.70 Found (eq_ref00 P1) as proof of (P2 Xy) % 251.31/251.70 Found ((eq_ref0 Xy) P1) as proof of (P2 Xy) % 251.31/251.70 Found (((eq_ref nat) Xy) P1) as proof of (P2 Xy) % 251.31/251.70 Found (((eq_ref nat) Xy) P1) as proof of (P2 Xy) % 251.31/251.70 Found x3:((more Xy) Xx) % 251.31/251.70 Found x3 as proof of ((more Xy) Xx) % 251.31/251.70 Found x3:((more Xy) Xx) % 251.31/251.70 Found x3 as proof of ((more Xy) Xx) % 251.31/251.70 Found x3:((more Xy) Xx) % 251.31/251.70 Found x3 as proof of ((more Xy) Xx) % 251.31/251.70 Found x3:((more Xy) Xx) % 251.31/251.70 Found x3 as proof of ((more Xy) Xx) % 251.31/251.70 Found x3:((more Xy) Xx) % 251.31/251.70 Found x3 as proof of ((more Xy) Xx) % 251.31/251.70 Found x3:((more Xy) Xx) % 251.31/251.70 Found x3 as proof of ((more Xy) Xx) % 251.31/251.70 Found x3:((more Xy) Xx) % 251.31/251.70 Found x3 as proof of ((more Xy) Xx) % 251.31/251.70 Found x3:((more Xy) Xx) % 251.31/251.70 Found x3 as proof of ((more Xy) Xx) % 251.31/251.70 Found x10:False % 251.31/251.70 Found (fun (x3:((more b) Xy))=> x10) as proof of False % 251.31/251.70 Found (fun (x3:((more b) Xy))=> x10) as proof of (((more b) Xy)->False) % 251.31/251.70 Found x20:False % 251.31/251.70 Found (fun (x3:((more b) Xy))=> x20) as proof of False % 251.31/251.70 Found (fun (x3:((more b) Xy))=> x20) as proof of (((more b) Xy)->False) % 251.31/251.70 Found x00:False % 251.31/251.70 Found (fun (x3:(p Xy))=> x00) as proof of False % 251.31/251.70 Found (fun (x3:(p Xy))=> x00) as proof of ((p Xy)->False) % 251.31/251.70 Found x2:((more Xy) Xx) % 251.31/251.70 Found x2 as proof of ((more Xy) Xx) % 251.31/251.70 Found x10:False % 251.31/251.70 Found (fun (x3:(p Xx))=> x10) as proof of False % 251.31/251.70 Found (fun (x3:(p Xx))=> x10) as proof of ((p Xx)->False) % 251.31/251.70 Found eq_ref000:=(eq_ref00 P):((P Xy)->(P Xy)) % 251.31/251.70 Found (eq_ref00 P) as proof of (P0 Xy) % 251.31/251.70 Found ((eq_ref0 Xy) P) as proof of (P0 Xy) % 251.31/251.70 Found (((eq_ref nat) Xy) P) as proof of (P0 Xy) % 251.31/251.70 Found (((eq_ref nat) Xy) P) as proof of (P0 Xy) % 251.31/251.70 Found x00:False % 251.31/251.70 Found (fun (x3:(p Xy))=> x00) as proof of False % 251.31/251.70 Found (fun (x3:(p Xy))=> x00) as proof of ((p Xy)->False) % 251.31/251.70 Found x4:(p Xy) % 251.31/251.70 Instantiate: Xy0:=Xy:nat % 251.31/251.70 Found x4 as proof of (p Xy0) % 251.31/251.70 Found (x30 x4) as proof of ((lessis Xx0) Xy0) % 251.31/251.70 Found ((x3 Xy0) x4) as proof of ((lessis Xx0) Xy0) % 251.31/251.70 Found ((x3 Xy0) x4) as proof of ((lessis Xx0) Xy0) % 251.31/251.70 Found ((x3 Xy0) x4) as proof of ((lessis Xx0) Xy0) % 251.31/251.70 Found x2:((more Xy) Xx) % 251.31/251.70 Found x2 as proof of ((more Xy) Xx) % 251.31/251.70 Found x2:((more Xy) Xx) % 251.31/251.70 Found x2 as proof of ((more Xy) Xx) % 251.31/251.70 Found x2:((more Xy) Xx) % 251.31/251.70 Found x2 as proof of ((more Xy) Xx) % 251.31/251.70 Found x2:((more Xy) Xx) % 251.31/251.70 Found x2 as proof of ((more Xy) Xx) % 251.31/251.70 Found x2:((more Xy) Xx) % 251.31/251.70 Found x2 as proof of ((more Xy) Xx) % 251.31/251.70 Found x10:False % 251.31/251.70 Found (fun (x3:(p Xx))=> x10) as proof of False % 251.31/251.70 Found (fun (x3:(p Xx))=> x10) as proof of ((p Xx)->False) % 251.31/251.70 Found x2:((more Xy) Xx) % 251.31/251.70 Found x2 as proof of ((more Xy) Xx) % 251.31/251.70 Found x2:((more Xy) Xx) % 251.31/251.70 Found x2 as proof of ((more Xy) Xx) % 251.31/251.70 Found x4:(p Xx) % 251.31/251.70 Instantiate: Xy0:=Xx:nat % 251.31/251.70 Found x4 as proof of (p Xy0) % 251.31/251.70 Found (x30 x4) as proof of ((lessis Xx0) Xy0) % 251.31/251.70 Found ((x3 Xy0) x4) as proof of ((lessis Xx0) Xy0) % 251.31/251.70 Found ((x3 Xy0) x4) as proof of ((lessis Xx0) Xy0) % 251.31/251.70 Found ((x3 Xy0) x4) as proof of ((lessis Xx0) Xy0) % 251.31/251.70 Found x00:False % 251.31/251.70 Found (fun (x3:((P b)->False))=> x00) as proof of False % 251.31/251.70 Found (fun (x3:((P b)->False))=> x00) as proof of (((P b)->False)->False) % 257.22/257.65 Found x10:False % 257.22/257.65 Found (fun (x3:((P b)->False))=> x10) as proof of False % 257.22/257.65 Found (fun (x3:((P b)->False))=> x10) as proof of (((P b)->False)->False) % 257.22/257.65 Found x10:False % 257.22/257.65 Found (fun (x3:((P b)->False))=> x10) as proof of False % 257.22/257.65 Found (fun (x3:((P b)->False))=> x10) as proof of (((P b)->False)->False) % 257.22/257.65 Found x00:False % 257.22/257.65 Found (fun (x3:((P b)->False))=> x00) as proof of False % 257.22/257.65 Found (fun (x3:((P b)->False))=> x00) as proof of (((P b)->False)->False) % 257.22/257.65 Found x4:(p Xx) % 257.22/257.65 Instantiate: Xy0:=Xx:nat % 257.22/257.65 Found x4 as proof of (p Xy0) % 257.22/257.65 Found (x50 x4) as proof of ((lessis Xx0) Xy0) % 257.22/257.65 Found ((x5 Xy0) x4) as proof of ((lessis Xx0) Xy0) % 257.22/257.65 Found ((x5 Xy0) x4) as proof of ((lessis Xx0) Xy0) % 257.22/257.65 Found ((x5 Xy0) x4) as proof of ((lessis Xx0) Xy0) % 257.22/257.65 Found x4:(p Xy) % 257.22/257.65 Instantiate: Xy0:=Xy:nat % 257.22/257.65 Found x4 as proof of (p Xy0) % 257.22/257.65 Found (x30 x4) as proof of ((lessis Xx0) Xy0) % 257.22/257.65 Found ((x3 Xy0) x4) as proof of ((lessis Xx0) Xy0) % 257.22/257.65 Found ((x3 Xy0) x4) as proof of ((lessis Xx0) Xy0) % 257.22/257.65 Found ((x3 Xy0) x4) as proof of ((lessis Xx0) Xy0) % 257.22/257.65 Found x00:False % 257.22/257.65 Found (fun (x3:(p Xy))=> x00) as proof of False % 257.22/257.65 Found (fun (x3:(p Xy))=> x00) as proof of ((p Xy)->False) % 257.22/257.65 Found x10:False % 257.22/257.65 Found (fun (x3:(p Xx))=> x10) as proof of False % 257.22/257.65 Found (fun (x3:(p Xx))=> x10) as proof of ((p Xx)->False) % 257.22/257.65 Found x10:False % 257.22/257.65 Found (fun (x3:(((p Xx)->False)->False))=> x10) as proof of False % 257.22/257.65 Found (fun (x3:(((p Xx)->False)->False))=> x10) as proof of ((((p Xx)->False)->False)->False) % 257.22/257.65 Found x00:False % 257.22/257.65 Found (fun (x3:(((p Xy)->False)->False))=> x00) as proof of False % 257.22/257.65 Found (fun (x3:(((p Xy)->False)->False))=> x00) as proof of ((((p Xy)->False)->False)->False) % 257.22/257.65 Found eq_ref00:=(eq_ref0 b):(((eq nat) b) b) % 257.22/257.65 Found (eq_ref0 b) as proof of (((eq nat) b) Xx) % 257.22/257.65 Found ((eq_ref nat) b) as proof of (((eq nat) b) Xx) % 257.22/257.65 Found ((eq_ref nat) b) as proof of (((eq nat) b) Xx) % 257.22/257.65 Found ((eq_ref nat) b) as proof of (((eq nat) b) Xx) % 257.22/257.65 Found eq_ref00:=(eq_ref0 Xy):(((eq nat) Xy) Xy) % 257.22/257.65 Found (eq_ref0 Xy) as proof of (((eq nat) Xy) b) % 257.22/257.65 Found ((eq_ref nat) Xy) as proof of (((eq nat) Xy) b) % 257.22/257.65 Found ((eq_ref nat) Xy) as proof of (((eq nat) Xy) b) % 257.22/257.65 Found ((eq_ref nat) Xy) as proof of (((eq nat) Xy) b) % 257.22/257.65 Found eq_ref00:=(eq_ref0 b):(((eq nat) b) b) % 257.22/257.65 Found (eq_ref0 b) as proof of (((eq nat) b) Xx) % 257.22/257.65 Found ((eq_ref nat) b) as proof of (((eq nat) b) Xx) % 257.22/257.65 Found ((eq_ref nat) b) as proof of (((eq nat) b) Xx) % 257.22/257.65 Found ((eq_ref nat) b) as proof of (((eq nat) b) Xx) % 257.22/257.65 Found eq_ref00:=(eq_ref0 Xy):(((eq nat) Xy) Xy) % 257.22/257.65 Found (eq_ref0 Xy) as proof of (((eq nat) Xy) b) % 257.22/257.65 Found ((eq_ref nat) Xy) as proof of (((eq nat) Xy) b) % 257.22/257.65 Found ((eq_ref nat) Xy) as proof of (((eq nat) Xy) b) % 257.22/257.65 Found ((eq_ref nat) Xy) as proof of (((eq nat) Xy) b) % 257.22/257.65 Found eq_ref00:=(eq_ref0 b):(((eq nat) b) b) % 257.22/257.65 Found (eq_ref0 b) as proof of (((eq nat) b) Xx) % 257.22/257.65 Found ((eq_ref nat) b) as proof of (((eq nat) b) Xx) % 257.22/257.65 Found ((eq_ref nat) b) as proof of (((eq nat) b) Xx) % 257.22/257.65 Found ((eq_ref nat) b) as proof of (((eq nat) b) Xx) % 257.22/257.65 Found eq_ref00:=(eq_ref0 Xy):(((eq nat) Xy) Xy) % 257.22/257.65 Found (eq_ref0 Xy) as proof of (((eq nat) Xy) b) % 257.22/257.65 Found ((eq_ref nat) Xy) as proof of (((eq nat) Xy) b) % 257.22/257.65 Found ((eq_ref nat) Xy) as proof of (((eq nat) Xy) b) % 257.22/257.65 Found ((eq_ref nat) Xy) as proof of (((eq nat) Xy) b) % 257.22/257.65 Found eq_ref00:=(eq_ref0 b):(((eq nat) b) b) % 257.22/257.65 Found (eq_ref0 b) as proof of (((eq nat) b) Xx) % 257.22/257.65 Found ((eq_ref nat) b) as proof of (((eq nat) b) Xx) % 257.22/257.65 Found ((eq_ref nat) b) as proof of (((eq nat) b) Xx) % 257.22/257.65 Found ((eq_ref nat) b) as proof of (((eq nat) b) Xx) % 257.22/257.65 Found eq_ref00:=(eq_ref0 Xy):(((eq nat) Xy) Xy) % 257.22/257.65 Found (eq_ref0 Xy) as proof of (((eq nat) Xy) b) % 257.22/257.65 Found ((eq_ref nat) Xy) as proof of (((eq nat) Xy) b) % 257.22/257.65 Found ((eq_ref nat) Xy) as proof of (((eq nat) Xy) b) % 257.22/257.65 Found ((eq_ref nat) Xy) as proof of (((eq nat) Xy) b) % 257.22/257.65 Found x00:False % 257.22/257.65 Found (fun (x2:(((forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))->((p Xy)->False))->False))=> x00) as proof of False % 257.22/257.65 Found (fun (x2:(((forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))->((p Xy)->False))->False))=> x00) as proof of ((((forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))->((p Xy)->False))->False)->False) % 257.22/257.65 Found x10:False % 257.22/257.65 Found (fun (x2:(((forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))->((p Xx)->False))->False))=> x10) as proof of False % 261.74/262.16 Found (fun (x2:(((forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))->((p Xx)->False))->False))=> x10) as proof of ((((forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))->((p Xx)->False))->False)->False) % 261.74/262.16 Found x20:False % 261.74/262.16 Found (fun (x5:(p Xx))=> x20) as proof of False % 261.74/262.16 Found (fun (x5:(p Xx))=> x20) as proof of ((p Xx)->False) % 261.74/262.16 Found x10:False % 261.74/262.16 Found (fun (x5:(p Xy))=> x10) as proof of False % 261.74/262.16 Found (fun (x5:(p Xy))=> x10) as proof of ((p Xy)->False) % 261.74/262.16 Found x10:False % 261.74/262.16 Found (fun (x4:(p Xx))=> x10) as proof of False % 261.74/262.16 Found (fun (x3:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))) (x4:(p Xx))=> x10) as proof of ((p Xx)->False) % 261.74/262.16 Found (fun (x3:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))) (x4:(p Xx))=> x10) as proof of ((forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))->((p Xx)->False)) % 261.74/262.16 Found x00:False % 261.74/262.16 Found (fun (x4:(p Xy))=> x00) as proof of False % 261.74/262.16 Found (fun (x3:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))) (x4:(p Xy))=> x00) as proof of ((p Xy)->False) % 261.74/262.16 Found (fun (x3:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))) (x4:(p Xy))=> x00) as proof of ((forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))->((p Xy)->False)) % 261.74/262.16 Found x10:False % 261.74/262.16 Found (fun (x4:(p Xy))=> x10) as proof of False % 261.74/262.16 Found (fun (x4:(p Xy))=> x10) as proof of ((p Xy)->False) % 261.74/262.16 Found x20:False % 261.74/262.16 Found (fun (x4:(p Xx))=> x20) as proof of False % 261.74/262.16 Found (fun (x4:(p Xx))=> x20) as proof of ((p Xx)->False) % 261.74/262.16 Found x300:=(x30 x6):((lessis Xy) Xx) % 261.74/262.16 Found (x30 x6) as proof of ((lessis Xy) Xx) % 261.74/262.16 Found ((x3 Xx) x6) as proof of ((lessis Xy) Xx) % 261.74/262.16 Found ((x3 Xx) x6) as proof of ((lessis Xy) Xx) % 261.74/262.16 Found ((satz10d0 ((x3 Xx) x6)) x2) as proof of False % 261.74/262.16 Found ((((satz10d Xy) Xx) ((x3 Xx) x6)) x2) as proof of False % 261.74/262.16 Found (fun (x6:(p Xx))=> ((((satz10d Xy) Xx) ((x3 Xx) x6)) x2)) as proof of False % 261.74/262.16 Found (fun (x5:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))) (x6:(p Xx))=> ((((satz10d Xy) Xx) ((x3 Xx) x6)) x2)) as proof of ((p Xx)->False) % 261.74/262.16 Found (fun (x5:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))) (x6:(p Xx))=> ((((satz10d Xy) Xx) ((x3 Xx) x6)) x2)) as proof of ((forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))->((p Xx)->False)) % 261.74/262.16 Found (x0 (fun (x5:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))) (x6:(p Xx))=> ((((satz10d Xy) Xx) ((x3 Xx) x6)) x2))) as proof of False % 261.74/262.16 Found (fun (x4:(p Xy))=> (x0 (fun (x5:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))) (x6:(p Xx))=> ((((satz10d Xy) Xx) ((x3 Xx) x6)) x2)))) as proof of False % 261.74/262.16 Found (fun (x3:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))) (x4:(p Xy))=> (x0 (fun (x5:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))) (x6:(p Xx))=> ((((satz10d Xy) Xx) ((x3 Xx) x6)) x2)))) as proof of ((p Xy)->False) % 261.74/262.16 Found (fun (x3:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))) (x4:(p Xy))=> (x0 (fun (x5:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))) (x6:(p Xx))=> ((((satz10d Xy) Xx) ((x3 Xx) x6)) x2)))) as proof of ((forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))->((p Xy)->False)) % 261.74/262.16 Found (x1 (fun (x3:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))) (x4:(p Xy))=> (x0 (fun (x5:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))) (x6:(p Xx))=> ((((satz10d Xy) Xx) ((x3 Xx) x6)) x2))))) as proof of False % 261.74/262.16 Found (fun (x2:((more Xy) Xx))=> (x1 (fun (x3:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))) (x4:(p Xy))=> (x0 (fun (x5:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))) (x6:(p Xx))=> ((((satz10d Xy) Xx) ((x3 Xx) x6)) x2)))))) as proof of False % 261.74/262.16 Found (fun (x2:((more Xy) Xx))=> (x1 (fun (x3:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))) (x4:(p Xy))=> (x0 (fun (x5:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))) (x6:(p Xx))=> ((((satz10d Xy) Xx) ((x3 Xx) x6)) x2)))))) as proof of (((more Xy) Xx)->False) % 261.74/262.16 Found x00:False % 261.74/262.16 Found (fun (x4:(p Xy))=> x00) as proof of False % 261.74/262.16 Found (fun (x4:(p Xy))=> x00) as proof of ((p Xy)->False) % 261.74/262.16 Found x10:False % 261.74/262.16 Found (fun (x4:(p Xx))=> x10) as proof of False % 261.74/262.16 Found (fun (x4:(p Xx))=> x10) as proof of ((p Xx)->False) % 261.74/262.16 Found x10:False % 261.74/262.16 Found (fun (x4:(p Xx))=> x10) as proof of False % 261.74/262.16 Found (fun (x3:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))) (x4:(p Xx))=> x10) as proof of ((p Xx)->False) % 266.98/267.40 Found (fun (x3:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))) (x4:(p Xx))=> x10) as proof of ((forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))->((p Xx)->False)) % 266.98/267.40 Found x00:False % 266.98/267.40 Found (fun (x4:(p Xy))=> x00) as proof of False % 266.98/267.40 Found (fun (x3:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))) (x4:(p Xy))=> x00) as proof of ((p Xy)->False) % 266.98/267.40 Found (fun (x3:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))) (x4:(p Xy))=> x00) as proof of ((forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))->((p Xy)->False)) % 266.98/267.40 Found x3:((more b) Xy) % 266.98/267.40 Found x3 as proof of ((more b) Xy) % 266.98/267.40 Found x3:((more b) Xy) % 266.98/267.40 Found x3 as proof of ((more b) Xy) % 266.98/267.40 Found False_rect00:=(False_rect0 ((lessis Xy) Xx)):((lessis Xy) Xx) % 266.98/267.40 Found (False_rect0 ((lessis Xy) Xx)) as proof of ((lessis Xy) Xx) % 266.98/267.40 Found ((fun (P1:Type)=> ((False_rect P1) x20)) ((lessis Xy) Xx)) as proof of ((lessis Xy) Xx) % 266.98/267.40 Found ((fun (P1:Type)=> ((False_rect P1) x20)) ((lessis Xy) Xx)) as proof of ((lessis Xy) Xx) % 266.98/267.40 Found (((satz14000 ((fun (P1:Type)=> ((False_rect P1) x20)) ((lessis Xy) Xx))) (fun (x3:((more Xx) Xy))=> x20)) (((eq_ref nat) Xx) P)) as proof of ((P Xx)->(P Xy)) % 266.98/267.40 Found (((satz14000 ((fun (P1:Type)=> ((False_rect P1) x20)) ((lessis Xy) Xx))) (fun (x3:((more Xx) Xy))=> x20)) (((eq_ref nat) Xx) P)) as proof of ((P Xx)->(P Xy)) % 266.98/267.40 Found ((((fun (x3:((lessis Xy) Xx)) (x4:(((more Xx) Xy)->False))=> (((satz1400 x3) x4) (fun (x6:nat)=> ((P Xx)->(P x6))))) ((fun (P1:Type)=> ((False_rect P1) x20)) ((lessis Xy) Xx))) (fun (x3:((more Xx) Xy))=> x20)) (((eq_ref nat) Xx) P)) as proof of ((P Xx)->(P Xy)) % 266.98/267.40 Found ((((fun (x3:((lessis Xy) Xx)) (x4:(((more Xx) Xy)->False))=> ((((satz140 Xx) x3) x4) (fun (x6:nat)=> ((P Xx)->(P x6))))) ((fun (P1:Type)=> ((False_rect P1) x20)) ((lessis Xy) Xx))) (fun (x3:((more Xx) Xy))=> x20)) (((eq_ref nat) Xx) P)) as proof of ((P Xx)->(P Xy)) % 266.98/267.40 Found ((((fun (x3:((lessis Xy) Xx)) (x4:(((more Xx) Xy)->False))=> (((((satz14 Xy) Xx) x3) x4) (fun (x6:nat)=> ((P Xx)->(P x6))))) ((fun (P1:Type)=> ((False_rect P1) x20)) ((lessis Xy) Xx))) (fun (x3:((more Xx) Xy))=> x20)) (((eq_ref nat) Xx) P)) as proof of ((P Xx)->(P Xy)) % 266.98/267.40 Found ((((fun (x3:((lessis Xy) Xx)) (x4:(((more Xx) Xy)->False))=> (((((satz14 Xy) Xx) x3) x4) (fun (x6:nat)=> ((P Xx)->(P x6))))) ((fun (P1:Type)=> ((False_rect P1) x20)) ((lessis Xy) Xx))) (fun (x3:((more Xx) Xy))=> x20)) (((eq_ref nat) Xx) P)) as proof of ((P Xx)->(P Xy)) % 266.98/267.40 Found x10:False % 266.98/267.40 Found (fun (x4:(p Xy))=> x10) as proof of False % 266.98/267.40 Found (fun (x3:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))) (x4:(p Xy))=> x10) as proof of ((p Xy)->False) % 266.98/267.40 Found (fun (x3:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))) (x4:(p Xy))=> x10) as proof of ((forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))->((p Xy)->False)) % 266.98/267.40 Found False_rect00:=(False_rect0 ((lessis Xy) Xx)):((lessis Xy) Xx) % 266.98/267.40 Found (False_rect0 ((lessis Xy) Xx)) as proof of ((lessis Xy) Xx) % 266.98/267.40 Found ((fun (P1:Type)=> ((False_rect P1) x10)) ((lessis Xy) Xx)) as proof of ((lessis Xy) Xx) % 266.98/267.40 Found ((fun (P1:Type)=> ((False_rect P1) x10)) ((lessis Xy) Xx)) as proof of ((lessis Xy) Xx) % 266.98/267.40 Found (((satz14000 ((fun (P1:Type)=> ((False_rect P1) x10)) ((lessis Xy) Xx))) (fun (x3:((more Xx) Xy))=> x10)) (((eq_ref nat) Xx) P)) as proof of ((P Xx)->(P Xy)) % 266.98/267.40 Found (((satz14000 ((fun (P1:Type)=> ((False_rect P1) x10)) ((lessis Xy) Xx))) (fun (x3:((more Xx) Xy))=> x10)) (((eq_ref nat) Xx) P)) as proof of ((P Xx)->(P Xy)) % 266.98/267.40 Found ((((fun (x3:((lessis Xy) Xx)) (x4:(((more Xx) Xy)->False))=> (((satz1400 x3) x4) (fun (x6:nat)=> ((P Xx)->(P x6))))) ((fun (P1:Type)=> ((False_rect P1) x10)) ((lessis Xy) Xx))) (fun (x3:((more Xx) Xy))=> x10)) (((eq_ref nat) Xx) P)) as proof of ((P Xx)->(P Xy)) % 266.98/267.40 Found ((((fun (x3:((lessis Xy) Xx)) (x4:(((more Xx) Xy)->False))=> ((((satz140 Xx) x3) x4) (fun (x6:nat)=> ((P Xx)->(P x6))))) ((fun (P1:Type)=> ((False_rect P1) x10)) ((lessis Xy) Xx))) (fun (x3:((more Xx) Xy))=> x10)) (((eq_ref nat) Xx) P)) as proof of ((P Xx)->(P Xy)) % 266.98/267.40 Found ((((fun (x3:((lessis Xy) Xx)) (x4:(((more Xx) Xy)->False))=> (((((satz14 Xy) Xx) x3) x4) (fun (x6:nat)=> ((P Xx)->(P x6))))) ((fun (P1:Type)=> ((False_rect P1) x10)) ((lessis Xy) Xx))) (fun (x3:((more Xx) Xy))=> x10)) (((eq_ref nat) Xx) P)) as proof of ((P Xx)->(P Xy)) % 273.89/274.29 Found ((((fun (x3:((lessis Xy) Xx)) (x4:(((more Xx) Xy)->False))=> (((((satz14 Xy) Xx) x3) x4) (fun (x6:nat)=> ((P Xx)->(P x6))))) ((fun (P1:Type)=> ((False_rect P1) x10)) ((lessis Xy) Xx))) (fun (x3:((more Xx) Xy))=> x10)) (((eq_ref nat) Xx) P)) as proof of ((P Xx)->(P Xy)) % 273.89/274.29 Found x20:False % 273.89/274.29 Found (fun (x4:(p Xx))=> x20) as proof of False % 273.89/274.29 Found (fun (x3:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))) (x4:(p Xx))=> x20) as proof of ((p Xx)->False) % 273.89/274.29 Found (fun (x3:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))) (x4:(p Xx))=> x20) as proof of ((forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))->((p Xx)->False)) % 273.89/274.29 Found x3:((more Xy0) Xy) % 273.89/274.29 Found x3 as proof of ((more Xy0) Xy) % 273.89/274.29 Found eq_ref000:=(eq_ref00 P):((P b)->(P b)) % 273.89/274.29 Found (eq_ref00 P) as proof of (P0 b) % 273.89/274.29 Found ((eq_ref0 b) P) as proof of (P0 b) % 273.89/274.29 Found (((eq_ref nat) b) P) as proof of (P0 b) % 273.89/274.29 Found (((eq_ref nat) b) P) as proof of (P0 b) % 273.89/274.29 Found x20:False % 273.89/274.29 Found (fun (x3:((more Xy) Xx))=> x20) as proof of False % 273.89/274.29 Found (fun (x3:((more Xy) Xx))=> x20) as proof of (((more Xy) Xx)->False) % 273.89/274.29 Found x20:False % 273.89/274.29 Found (fun (x3:((more Xy) Xx))=> x20) as proof of False % 273.89/274.29 Found (fun (x3:((more Xy) Xx))=> x20) as proof of (((more Xy) Xx)->False) % 273.89/274.29 Found x10:False % 273.89/274.29 Found (fun (x3:((more Xy) Xx))=> x10) as proof of False % 273.89/274.29 Found (fun (x3:((more Xy) Xx))=> x10) as proof of (((more Xy) Xx)->False) % 273.89/274.29 Found x10:False % 273.89/274.29 Found (fun (x3:((more Xy) Xx))=> x10) as proof of False % 273.89/274.29 Found (fun (x3:((more Xy) Xx))=> x10) as proof of (((more Xy) Xx)->False) % 273.89/274.29 Found x00:False % 273.89/274.29 Found (fun (x3:(p Xy))=> x00) as proof of False % 273.89/274.29 Found (fun (x2:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))) (x3:(p Xy))=> x00) as proof of ((p Xy)->False) % 273.89/274.29 Found (fun (x2:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))) (x3:(p Xy))=> x00) as proof of ((forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))->((p Xy)->False)) % 273.89/274.29 Found eq_ref00:=(eq_ref0 Xx):(((eq nat) Xx) Xx) % 273.89/274.29 Found (eq_ref0 Xx) as proof of (((eq nat) Xx) b0) % 273.89/274.29 Found ((eq_ref nat) Xx) as proof of (((eq nat) Xx) b0) % 273.89/274.29 Found ((eq_ref nat) Xx) as proof of (((eq nat) Xx) b0) % 273.89/274.29 Found ((eq_ref nat) Xx) as proof of (((eq nat) Xx) b0) % 273.89/274.29 Found eq_ref00:=(eq_ref0 b0):(((eq nat) b0) b0) % 273.89/274.29 Found (eq_ref0 b0) as proof of (((eq nat) b0) Xy) % 273.89/274.29 Found ((eq_ref nat) b0) as proof of (((eq nat) b0) Xy) % 273.89/274.29 Found ((eq_ref nat) b0) as proof of (((eq nat) b0) Xy) % 273.89/274.29 Found ((eq_ref nat) b0) as proof of (((eq nat) b0) Xy) % 273.89/274.29 Found x10:False % 273.89/274.29 Found (fun (x2:((((more Xy) Xx)->False)->False))=> x10) as proof of False % 273.89/274.29 Found (fun (x2:((((more Xy) Xx)->False)->False))=> x10) as proof of (((((more Xy) Xx)->False)->False)->False) % 273.89/274.29 Found x10:False % 273.89/274.29 Found (fun (x2:((((more Xy) Xx)->False)->False))=> x10) as proof of False % 273.89/274.29 Found (fun (x2:((((more Xy) Xx)->False)->False))=> x10) as proof of (((((more Xy) Xx)->False)->False)->False) % 273.89/274.29 Found x00:False % 273.89/274.29 Found (fun (x2:((((more Xy) Xx)->False)->False))=> x00) as proof of False % 273.89/274.29 Found (fun (x2:((((more Xy) Xx)->False)->False))=> x00) as proof of (((((more Xy) Xx)->False)->False)->False) % 273.89/274.29 Found x10:False % 273.89/274.29 Found (fun (x2:((((more Xy) Xx)->False)->False))=> x10) as proof of False % 273.89/274.29 Found (fun (x2:((((more Xy) Xx)->False)->False))=> x10) as proof of (((((more Xy) Xx)->False)->False)->False) % 273.89/274.29 Found x00:False % 273.89/274.29 Found (fun (x2:((((more Xy) Xx)->False)->False))=> x00) as proof of False % 273.89/274.29 Found (fun (x2:((((more Xy) Xx)->False)->False))=> x00) as proof of (((((more Xy) Xx)->False)->False)->False) % 273.89/274.29 Found x10:False % 273.89/274.29 Found (fun (x3:(p Xx))=> x10) as proof of False % 273.89/274.29 Found (fun (x2:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))) (x3:(p Xx))=> x10) as proof of ((p Xx)->False) % 273.89/274.29 Found (fun (x2:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))) (x3:(p Xx))=> x10) as proof of ((forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))->((p Xx)->False)) % 273.89/274.29 Found x2:((more b) Xy) % 273.89/274.29 Found x2 as proof of ((more b) Xy) % 273.89/274.29 Found x00:False % 273.89/274.29 Found (fun (x3:(p Xy))=> x00) as proof of False % 273.89/274.29 Found (fun (x2:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))) (x3:(p Xy))=> x00) as proof of ((p Xy)->False) % 279.56/279.97 Found (fun (x2:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))) (x3:(p Xy))=> x00) as proof of ((forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))->((p Xy)->False)) % 279.56/279.97 Found x00:False % 279.56/279.97 Found (fun (x2:((((more Xy) Xx)->False)->False))=> x00) as proof of False % 279.56/279.97 Found (fun (x2:((((more Xy) Xx)->False)->False))=> x00) as proof of (((((more Xy) Xx)->False)->False)->False) % 279.56/279.97 Found x2:((more b) Xy) % 279.56/279.97 Found x2 as proof of ((more b) Xy) % 279.56/279.97 Found x10:False % 279.56/279.97 Found (fun (x3:(p Xx))=> x10) as proof of False % 279.56/279.97 Found (fun (x2:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))) (x3:(p Xx))=> x10) as proof of ((p Xx)->False) % 279.56/279.97 Found (fun (x2:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))) (x3:(p Xx))=> x10) as proof of ((forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))->((p Xx)->False)) % 279.56/279.97 Found x00:False % 279.56/279.97 Found (fun (x2:((((more Xy) Xx)->False)->False))=> x00) as proof of False % 279.56/279.97 Found (fun (x2:((((more Xy) Xx)->False)->False))=> x00) as proof of (((((more Xy) Xx)->False)->False)->False) % 279.56/279.97 Found x10:False % 279.56/279.97 Found (fun (x2:((((more Xy) Xx)->False)->False))=> x10) as proof of False % 279.56/279.97 Found (fun (x2:((((more Xy) Xx)->False)->False))=> x10) as proof of (((((more Xy) Xx)->False)->False)->False) % 279.56/279.97 Found eq_ref000:=(eq_ref00 P):((P Xx)->(P Xx)) % 279.56/279.97 Found (eq_ref00 P) as proof of (P0 Xx) % 279.56/279.97 Found ((eq_ref0 Xx) P) as proof of (P0 Xx) % 279.56/279.97 Found (((eq_ref nat) Xx) P) as proof of (P0 Xx) % 279.56/279.97 Found (((eq_ref nat) Xx) P) as proof of (P0 Xx) % 279.56/279.97 Found x00:False % 279.56/279.97 Found (fun (x2:((((eq nat) Xy) b)->False))=> x00) as proof of False % 279.56/279.97 Found (fun (x2:((((eq nat) Xy) b)->False))=> x00) as proof of (((((eq nat) Xy) b)->False)->False) % 279.56/279.97 Found (et0 (fun (x2:((((eq nat) Xy) b)->False))=> x00)) as proof of (((eq nat) Xy) b) % 279.56/279.97 Found ((et (((eq nat) Xy) b)) (fun (x2:((((eq nat) Xy) b)->False))=> x00)) as proof of (((eq nat) Xy) b) % 279.56/279.97 Found ((et (((eq nat) Xy) b)) (fun (x2:((((eq nat) Xy) b)->False))=> x00)) as proof of (((eq nat) Xy) b) % 279.56/279.97 Found x10:False % 279.56/279.97 Found (fun (x4:(False->False))=> x10) as proof of False % 279.56/279.97 Found (fun (x4:(False->False))=> x10) as proof of ((False->False)->False) % 279.56/279.97 Found x10:False % 279.56/279.97 Found (fun (x2:((((eq nat) Xy) b)->False))=> x10) as proof of False % 279.56/279.97 Found (fun (x2:((((eq nat) Xy) b)->False))=> x10) as proof of (((((eq nat) Xy) b)->False)->False) % 279.56/279.97 Found (et0 (fun (x2:((((eq nat) Xy) b)->False))=> x10)) as proof of (((eq nat) Xy) b) % 279.56/279.97 Found ((et (((eq nat) Xy) b)) (fun (x2:((((eq nat) Xy) b)->False))=> x10)) as proof of (((eq nat) Xy) b) % 279.56/279.97 Found ((et (((eq nat) Xy) b)) (fun (x2:((((eq nat) Xy) b)->False))=> x10)) as proof of (((eq nat) Xy) b) % 279.56/279.97 Found x10:False % 279.56/279.97 Found (fun (x2:((((eq nat) Xy) b)->False))=> x10) as proof of False % 279.56/279.97 Found (fun (x2:((((eq nat) Xy) b)->False))=> x10) as proof of (((((eq nat) Xy) b)->False)->False) % 279.56/279.97 Found (et0 (fun (x2:((((eq nat) Xy) b)->False))=> x10)) as proof of (((eq nat) Xy) b) % 279.56/279.97 Found ((et (((eq nat) Xy) b)) (fun (x2:((((eq nat) Xy) b)->False))=> x10)) as proof of (((eq nat) Xy) b) % 279.56/279.97 Found ((et (((eq nat) Xy) b)) (fun (x2:((((eq nat) Xy) b)->False))=> x10)) as proof of (((eq nat) Xy) b) % 279.56/279.97 Found x00:False % 279.56/279.97 Found (fun (x2:((((eq nat) Xy) b)->False))=> x00) as proof of False % 279.56/279.97 Found (fun (x2:((((eq nat) Xy) b)->False))=> x00) as proof of (((((eq nat) Xy) b)->False)->False) % 279.56/279.97 Found (et0 (fun (x2:((((eq nat) Xy) b)->False))=> x00)) as proof of (((eq nat) Xy) b) % 279.56/279.97 Found ((et (((eq nat) Xy) b)) (fun (x2:((((eq nat) Xy) b)->False))=> x00)) as proof of (((eq nat) Xy) b) % 279.56/279.97 Found ((et (((eq nat) Xy) b)) (fun (x2:((((eq nat) Xy) b)->False))=> x00)) as proof of (((eq nat) Xy) b) % 279.56/279.97 Found eq_ref00:=(eq_ref0 Xx):(((eq nat) Xx) Xx) % 279.56/279.97 Found (eq_ref0 Xx) as proof of (((eq nat) Xx) b) % 279.56/279.97 Found ((eq_ref nat) Xx) as proof of (((eq nat) Xx) b) % 279.56/279.97 Found ((eq_ref nat) Xx) as proof of (((eq nat) Xx) b) % 279.56/279.97 Found ((eq_ref nat) Xx) as proof of (((eq nat) Xx) b) % 279.56/279.97 Found eq_ref00:=(eq_ref0 b):(((eq nat) b) b) % 279.56/279.97 Found (eq_ref0 b) as proof of (((eq nat) b) Xy) % 279.56/279.97 Found ((eq_ref nat) b) as proof of (((eq nat) b) Xy) % 279.56/279.97 Found ((eq_ref nat) b) as proof of (((eq nat) b) Xy) % 279.56/279.97 Found ((eq_ref nat) b) as proof of (((eq nat) b) Xy) % 279.56/279.97 Found x00:False % 279.56/279.97 Found (fun (x4:(False->False))=> x00) as proof of False % 279.56/279.97 Found (fun (x4:(False->False))=> x00) as proof of ((False->False)->False) % 282.41/282.84 Found x10:False % 282.41/282.84 Found (fun (x3:(p Xx))=> x10) as proof of False % 282.41/282.84 Found (fun (x3:(p Xx))=> x10) as proof of ((p Xx)->False) % 282.41/282.84 Found x00:False % 282.41/282.84 Found (fun (x3:(p Xy))=> x00) as proof of False % 282.41/282.84 Found (fun (x3:(p Xy))=> x00) as proof of ((p Xy)->False) % 282.41/282.84 Found x10:False % 282.41/282.84 Found (fun (x2:(((lessis Xx) Xy)->False))=> x10) as proof of False % 282.41/282.84 Found (fun (x2:(((lessis Xx) Xy)->False))=> x10) as proof of ((((lessis Xx) Xy)->False)->False) % 282.41/282.84 Found x00:False % 282.41/282.84 Found (fun (x2:(((lessis Xx) Xy)->False))=> x00) as proof of False % 282.41/282.84 Found (fun (x2:(((lessis Xx) Xy)->False))=> x00) as proof of ((((lessis Xx) Xy)->False)->False) % 282.41/282.84 Found x10:False % 282.41/282.84 Found (fun (x2:(((lessis Xx) Xy)->False))=> x10) as proof of False % 282.41/282.84 Found (fun (x2:(((lessis Xx) Xy)->False))=> x10) as proof of ((((lessis Xx) Xy)->False)->False) % 282.41/282.84 Found x10:False % 282.41/282.84 Found (fun (x2:(((lessis Xx) Xy)->False))=> x10) as proof of False % 282.41/282.84 Found (fun (x2:(((lessis Xx) Xy)->False))=> x10) as proof of ((((lessis Xx) Xy)->False)->False) % 282.41/282.84 Found x10:False % 282.41/282.84 Found (fun (x2:(((lessis Xx) Xy)->False))=> x10) as proof of False % 282.41/282.84 Found (fun (x2:(((lessis Xx) Xy)->False))=> x10) as proof of ((((lessis Xx) Xy)->False)->False) % 282.41/282.84 Found x00:False % 282.41/282.84 Found (fun (x2:(((lessis Xx) Xy)->False))=> x00) as proof of False % 282.41/282.84 Found (fun (x2:(((lessis Xx) Xy)->False))=> x00) as proof of ((((lessis Xx) Xy)->False)->False) % 282.41/282.84 Found x00:False % 282.41/282.84 Found (fun (x2:(((lessis Xx) Xy)->False))=> x00) as proof of False % 282.41/282.84 Found (fun (x2:(((lessis Xx) Xy)->False))=> x00) as proof of ((((lessis Xx) Xy)->False)->False) % 282.41/282.84 Found x00:False % 282.41/282.84 Found (fun (x2:(((lessis Xx) Xy)->False))=> x00) as proof of False % 282.41/282.84 Found (fun (x2:(((lessis Xx) Xy)->False))=> x00) as proof of ((((lessis Xx) Xy)->False)->False) % 282.41/282.84 Found x10:False % 282.41/282.84 Found (fun (x3:(p Xx))=> x10) as proof of False % 282.41/282.84 Found (fun (x2:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))) (x3:(p Xx))=> x10) as proof of ((p Xx)->False) % 282.41/282.84 Found (fun (x2:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))) (x3:(p Xx))=> x10) as proof of ((forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))->((p Xx)->False)) % 282.41/282.84 Found x10:False % 282.41/282.84 Found (fun (x3:(((p Xx)->False)->False))=> x10) as proof of False % 282.41/282.84 Found (fun (x3:(((p Xx)->False)->False))=> x10) as proof of ((((p Xx)->False)->False)->False) % 282.41/282.84 Found x00:False % 282.41/282.84 Found (fun (x3:(((p Xy)->False)->False))=> x00) as proof of False % 282.41/282.84 Found (fun (x3:(((p Xy)->False)->False))=> x00) as proof of ((((p Xy)->False)->False)->False) % 282.41/282.84 Found x3:((more Xy) b) % 282.41/282.84 Found x3 as proof of ((more Xy) b) % 282.41/282.84 Found x00:False % 282.41/282.84 Found (fun (x3:(p Xy))=> x00) as proof of False % 282.41/282.84 Found (fun (x2:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))) (x3:(p Xy))=> x00) as proof of ((p Xy)->False) % 282.41/282.84 Found (fun (x2:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))) (x3:(p Xy))=> x00) as proof of ((forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))->((p Xy)->False)) % 282.41/282.84 Found False_rect00:=(False_rect0 ((lessis Xx) Xy)):((lessis Xx) Xy) % 282.41/282.84 Found (False_rect0 ((lessis Xx) Xy)) as proof of ((lessis Xx) Xy) % 282.41/282.84 Found ((fun (P:Type)=> ((False_rect P) x20)) ((lessis Xx) Xy)) as proof of ((lessis Xx) Xy) % 282.41/282.84 Found ((fun (P:Type)=> ((False_rect P) x20)) ((lessis Xx) Xy)) as proof of ((lessis Xx) Xy) % 282.41/282.84 Found ((satz1400 ((fun (P:Type)=> ((False_rect P) x20)) ((lessis Xx) Xy))) (fun (x3:((more Xy) Xx))=> x20)) as proof of (((eq nat) Xy) Xx) % 282.41/282.84 Found (((satz140 Xy) ((fun (P:Type)=> ((False_rect P) x20)) ((lessis Xx) Xy))) (fun (x3:((more Xy) Xx))=> x20)) as proof of (((eq nat) Xy) Xx) % 282.41/282.84 Found ((((satz14 Xx) Xy) ((fun (P:Type)=> ((False_rect P) x20)) ((lessis Xx) Xy))) (fun (x3:((more Xy) Xx))=> x20)) as proof of (((eq nat) Xy) Xx) % 282.41/282.84 Found ((((satz14 Xx) Xy) ((fun (P:Type)=> ((False_rect P) x20)) ((lessis Xx) Xy))) (fun (x3:((more Xy) Xx))=> x20)) as proof of (((eq nat) Xy) Xx) % 282.41/282.84 Found x10:False % 282.41/282.84 Found (fun (x4:(p Xy))=> x10) as proof of False % 282.41/282.84 Found (fun (x4:(p Xy))=> x10) as proof of ((p Xy)->False) % 282.41/282.84 Found x3:((more b) Xx) % 282.41/282.84 Found x3 as proof of ((more b) Xx) % 282.41/282.84 Found x3:((more Xx) Xy) % 282.41/282.84 Found x3 as proof of ((more Xx) Xy) % 282.41/282.84 Found False_rect00:=(False_rect0 ((lessis Xx) Xy)):((lessis Xx) Xy) % 282.41/282.84 Found (False_rect0 ((lessis Xx) Xy)) as proof of ((lessis Xx) Xy) % 293.16/293.61 Found ((fun (P:Type)=> ((False_rect P) x10)) ((lessis Xx) Xy)) as proof of ((lessis Xx) Xy) % 293.16/293.61 Found ((fun (P:Type)=> ((False_rect P) x10)) ((lessis Xx) Xy)) as proof of ((lessis Xx) Xy) % 293.16/293.61 Found ((satz1400 ((fun (P:Type)=> ((False_rect P) x10)) ((lessis Xx) Xy))) (fun (x3:((more Xy) Xx))=> x10)) as proof of (((eq nat) Xy) Xx) % 293.16/293.61 Found (((satz140 Xy) ((fun (P:Type)=> ((False_rect P) x10)) ((lessis Xx) Xy))) (fun (x3:((more Xy) Xx))=> x10)) as proof of (((eq nat) Xy) Xx) % 293.16/293.61 Found ((((satz14 Xx) Xy) ((fun (P:Type)=> ((False_rect P) x10)) ((lessis Xx) Xy))) (fun (x3:((more Xy) Xx))=> x10)) as proof of (((eq nat) Xy) Xx) % 293.16/293.61 Found ((((satz14 Xx) Xy) ((fun (P:Type)=> ((False_rect P) x10)) ((lessis Xx) Xy))) (fun (x3:((more Xy) Xx))=> x10)) as proof of (((eq nat) Xy) Xx) % 293.16/293.61 Found x20:False % 293.16/293.61 Found (fun (x4:(p Xx))=> x20) as proof of False % 293.16/293.61 Found (fun (x4:(p Xx))=> x20) as proof of ((p Xx)->False) % 293.16/293.61 Found x5:(p Xy) % 293.16/293.61 Instantiate: Xy0:=Xy:nat % 293.16/293.61 Found x5 as proof of (p Xy0) % 293.16/293.61 Found (x60 x5) as proof of ((lessis Xx0) Xy0) % 293.16/293.61 Found ((x6 Xy0) x5) as proof of ((lessis Xx0) Xy0) % 293.16/293.61 Found ((x6 Xy0) x5) as proof of ((lessis Xx0) Xy0) % 293.16/293.61 Found ((x6 Xy0) x5) as proof of ((lessis Xx0) Xy0) % 293.16/293.61 Found x5:(p Xx) % 293.16/293.61 Instantiate: Xy0:=Xx:nat % 293.16/293.61 Found x5 as proof of (p Xy0) % 293.16/293.61 Found (x60 x5) as proof of ((lessis Xx0) Xy0) % 293.16/293.61 Found ((x6 Xy0) x5) as proof of ((lessis Xx0) Xy0) % 293.16/293.61 Found ((x6 Xy0) x5) as proof of ((lessis Xx0) Xy0) % 293.16/293.61 Found ((x6 Xy0) x5) as proof of ((lessis Xx0) Xy0) % 293.16/293.61 Found x10:False % 293.16/293.61 Found (fun (x3:(((forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))->((p Xx)->False))->False))=> x10) as proof of False % 293.16/293.61 Found (fun (x3:(((forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))->((p Xx)->False))->False))=> x10) as proof of ((((forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))->((p Xx)->False))->False)->False) % 293.16/293.61 Found x10:False % 293.16/293.61 Found (fun (x5:(p Xy))=> x10) as proof of False % 293.16/293.61 Found (fun (x5:(p Xy))=> x10) as proof of ((p Xy)->False) % 293.16/293.61 Found x20:False % 293.16/293.61 Found (fun (x5:(p Xx))=> x20) as proof of False % 293.16/293.61 Found (fun (x5:(p Xx))=> x20) as proof of ((p Xx)->False) % 293.16/293.61 Found x00:False % 293.16/293.61 Found (fun (x3:(((forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))->((p Xy)->False))->False))=> x00) as proof of False % 293.16/293.61 Found (fun (x3:(((forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))->((p Xy)->False))->False))=> x00) as proof of ((((forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))->((p Xy)->False))->False)->False) % 293.16/293.61 Found x10:False % 293.16/293.61 Found (fun (x5:(p Xy))=> x10) as proof of False % 293.16/293.61 Found (fun (x4:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))) (x5:(p Xy))=> x10) as proof of ((p Xy)->False) % 293.16/293.61 Found (fun (x4:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))) (x5:(p Xy))=> x10) as proof of ((forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))->((p Xy)->False)) % 293.16/293.61 Found x20:False % 293.16/293.61 Found (fun (x5:(p Xx))=> x20) as proof of False % 293.16/293.61 Found (fun (x4:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))) (x5:(p Xx))=> x20) as proof of ((p Xx)->False) % 293.16/293.61 Found (fun (x4:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))) (x5:(p Xx))=> x20) as proof of ((forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))->((p Xx)->False)) % 293.16/293.61 Found x3:((more Xy0) Xy) % 293.16/293.61 Found x3 as proof of ((more Xy0) Xy) % 293.16/293.61 Found x3:((more Xy) Xx) % 293.16/293.61 Found x3 as proof of ((more Xy) Xx) % 293.16/293.61 Found x00:False % 293.16/293.61 Found (fun (x3:(p Xy))=> x00) as proof of False % 293.16/293.61 Found (fun (x3:(p Xy))=> x00) as proof of ((p Xy)->False) % 293.16/293.61 Found x3:((more Xy) Xx) % 293.16/293.61 Found x3 as proof of ((more Xy) Xx) % 293.16/293.61 Found x10:False % 293.16/293.61 Found (fun (x3:(p Xx))=> x10) as proof of False % 293.16/293.61 Found (fun (x3:(p Xx))=> x10) as proof of ((p Xx)->False) % 293.16/293.61 Found x20:False % 293.16/293.61 Found (fun (x4:(p Xx))=> x20) as proof of False % 293.16/293.61 Found (fun (x3:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))) (x4:(p Xx))=> x20) as proof of ((p Xx)->False) % 293.16/293.61 Found (fun (x3:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))) (x4:(p Xx))=> x20) as proof of ((forall (Xx_0:nat), ((p Xx_0)->((lessis Xx) Xx_0)))->((p Xx)->False)) % 293.16/293.61 Found x10:False % 293.16/293.61 Found (fun (x4:(p Xy))=> x10) as proof of False % 293.16/293.61 Found (fun (x3:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))) (x4:(p Xy))=> x10) as proof of ((p Xy)->False) % 293.16/293.61 Found (fun (x3:(forall (Xx_0:nat), ((p Xx_0)->((lessis Xy) Xx_0)))) (x4:(p Xy))=> x1 %------------------------------------------------------------------------------