%------------------------------------------------------------------------------ % File : cocATP---0.2.0 % Problem : NUM637^2 : TPTP v7.0.0. Released v3.7.0. % Transfm : none % Format : tptp:raw % Command : python CASC.py /export/starexec/sandbox/benchmark/theBenchmark.p % Computer : n177.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:14 EST 2018 % Result : Timeout 300.08s % 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 : NUM637^2 : TPTP v7.0.0. Released v3.7.0. % 0.00/0.03 % Command : python CASC.py /export/starexec/sandbox/benchmark/theBenchmark.p % 0.02/0.23 % Computer : n177.star.cs.uiowa.edu % 0.02/0.23 % Model : x86_64 x86_64 % 0.02/0.23 % CPU : Intel(R) Xeon(R) CPU E5-2609 0 @ 2.40GHz % 0.02/0.23 % Memory : 32218.625MB % 0.02/0.23 % OS : Linux 3.10.0-693.2.2.el7.x86_64 % 0.02/0.23 % CPULimit : 300 % 0.02/0.23 % DateTime : Fri Jan 5 11:17:30 CST 2018 % 0.02/0.23 % CPUTime : % 0.07/0.31 Python 2.7.13 % 8.33/8.81 Using paths ['/home/cristobal/cocATP/CASC/TPTP/', '/export/starexec/sandbox/benchmark/', '/export/starexec/sandbox/benchmark/'] % 8.33/8.81 FOF formula (<kernel.Constant object at 0x2ba6491036c8>, <kernel.Constant object at 0x2ba649b807e8>) of role type named one_type % 8.33/8.81 Using role type % 8.33/8.81 Declaring one:fofType % 8.33/8.81 FOF formula (<kernel.Constant object at 0x2ba64910af80>, <kernel.DependentProduct object at 0x2ba649b80518>) of role type named succ_type % 8.33/8.81 Using role type % 8.33/8.81 Declaring succ:(fofType->fofType) % 8.33/8.81 FOF formula (forall (X:fofType), (not (((eq fofType) (succ X)) one))) of role axiom named one_is_first % 8.33/8.81 A new axiom: (forall (X:fofType), (not (((eq fofType) (succ X)) one))) % 8.33/8.81 FOF formula (forall (X:fofType) (Y:fofType), ((((eq fofType) (succ X)) (succ Y))->(((eq fofType) X) Y))) of role axiom named succ_injective % 8.33/8.81 A new axiom: (forall (X:fofType) (Y:fofType), ((((eq fofType) (succ X)) (succ Y))->(((eq fofType) X) Y))) % 8.33/8.81 FOF formula (forall (M:(fofType->Prop)), (((and (M one)) (forall (X:fofType), ((M X)->(M (succ X)))))->(forall (Y:fofType), (M Y)))) of role axiom named induction % 8.33/8.81 A new axiom: (forall (M:(fofType->Prop)), (((and (M one)) (forall (X:fofType), ((M X)->(M (succ X)))))->(forall (Y:fofType), (M Y)))) % 8.33/8.81 FOF formula (forall (X:fofType), ((not (((eq fofType) X) one))->((ex fofType) (fun (U:fofType)=> (((eq fofType) X) (succ U)))))) of role conjecture named satz3 % 8.33/8.81 Conjecture to prove = (forall (X:fofType), ((not (((eq fofType) X) one))->((ex fofType) (fun (U:fofType)=> (((eq fofType) X) (succ U)))))):Prop % 8.33/8.81 We need to prove ['(forall (X:fofType), ((not (((eq fofType) X) one))->((ex fofType) (fun (U:fofType)=> (((eq fofType) X) (succ U))))))'] % 8.33/8.81 Parameter fofType:Type. % 8.33/8.81 Parameter one:fofType. % 8.33/8.81 Parameter succ:(fofType->fofType). % 8.33/8.81 Axiom one_is_first:(forall (X:fofType), (not (((eq fofType) (succ X)) one))). % 8.33/8.81 Axiom succ_injective:(forall (X:fofType) (Y:fofType), ((((eq fofType) (succ X)) (succ Y))->(((eq fofType) X) Y))). % 8.33/8.81 Axiom induction:(forall (M:(fofType->Prop)), (((and (M one)) (forall (X:fofType), ((M X)->(M (succ X)))))->(forall (Y:fofType), (M Y)))). % 8.33/8.81 Trying to prove (forall (X:fofType), ((not (((eq fofType) X) one))->((ex fofType) (fun (U:fofType)=> (((eq fofType) X) (succ U)))))) % 8.33/8.81 Found eq_ref00:=(eq_ref0 (succ X0)):(((eq fofType) (succ X0)) (succ X0)) % 8.33/8.81 Found (eq_ref0 (succ X0)) as proof of (((eq fofType) (succ X0)) (succ x0)) % 8.33/8.81 Found ((eq_ref fofType) (succ X0)) as proof of (((eq fofType) (succ X0)) (succ x0)) % 8.33/8.81 Found ((eq_ref fofType) (succ X0)) as proof of (((eq fofType) (succ X0)) (succ x0)) % 8.33/8.81 Found (fun (x1:(((eq fofType) X0) (succ x0)))=> ((eq_ref fofType) (succ X0))) as proof of (((eq fofType) (succ X0)) (succ x0)) % 8.33/8.81 Found eq_ref000:=(eq_ref00 P):((P (succ X0))->(P (succ X0))) % 8.33/8.81 Found (eq_ref00 P) as proof of ((P (succ X0))->(P (succ x0))) % 8.33/8.81 Found ((eq_ref0 (succ X0)) P) as proof of ((P (succ X0))->(P (succ x0))) % 8.33/8.81 Found (((eq_ref fofType) (succ X0)) P) as proof of ((P (succ X0))->(P (succ x0))) % 8.33/8.81 Found (((eq_ref fofType) (succ X0)) P) as proof of ((P (succ X0))->(P (succ x0))) % 8.33/8.81 Found (fun (P:(fofType->Prop))=> (((eq_ref fofType) (succ X0)) P)) as proof of ((P (succ X0))->(P (succ x0))) % 8.33/8.81 Found (fun (x1:(((eq fofType) X0) (succ x0))) (P:(fofType->Prop))=> (((eq_ref fofType) (succ X0)) P)) as proof of (((eq fofType) (succ X0)) (succ x0)) % 8.33/8.81 Found x2:(P (succ X0)) % 8.33/8.81 Instantiate: x0:=X0:fofType % 8.33/8.81 Found (fun (x2:(P (succ X0)))=> x2) as proof of (P (succ x0)) % 8.33/8.81 Found (fun (P:(fofType->Prop)) (x2:(P (succ X0)))=> x2) as proof of ((P (succ X0))->(P (succ x0))) % 8.33/8.81 Found (fun (x1:(((eq fofType) X0) (succ x0))) (P:(fofType->Prop)) (x2:(P (succ X0)))=> x2) as proof of (((eq fofType) (succ X0)) (succ x0)) % 8.33/8.81 Found eq_ref00:=(eq_ref0 (succ X0)):(((eq fofType) (succ X0)) (succ X0)) % 8.33/8.81 Found (eq_ref0 (succ X0)) as proof of (((eq fofType) (succ X0)) (succ x1)) % 8.33/8.81 Found ((eq_ref fofType) (succ X0)) as proof of (((eq fofType) (succ X0)) (succ x1)) % 8.33/8.81 Found ((eq_ref fofType) (succ X0)) as proof of (((eq fofType) (succ X0)) (succ x1)) % 8.33/8.81 Found ((eq_ref fofType) (succ X0)) as proof of (((eq fofType) (succ X0)) (succ x1)) % 8.33/8.81 Found (ex_intro000 ((eq_ref fofType) (succ X0))) as proof of ((ex fofType) (fun (U:fofType)=> (((eq fofType) (succ X0)) (succ U)))) % 17.53/17.97 Found ((ex_intro00 X0) ((eq_ref fofType) (succ X0))) as proof of ((ex fofType) (fun (U:fofType)=> (((eq fofType) (succ X0)) (succ U)))) % 17.53/17.97 Found (((ex_intro0 (fun (U:fofType)=> (((eq fofType) (succ X0)) (succ U)))) X0) ((eq_ref fofType) (succ X0))) as proof of ((ex fofType) (fun (U:fofType)=> (((eq fofType) (succ X0)) (succ U)))) % 17.53/17.97 Found ((((ex_intro fofType) (fun (U:fofType)=> (((eq fofType) (succ X0)) (succ U)))) X0) ((eq_ref fofType) (succ X0))) as proof of ((ex fofType) (fun (U:fofType)=> (((eq fofType) (succ X0)) (succ U)))) % 17.53/17.97 Found (fun (x0:((ex fofType) (fun (U:fofType)=> (((eq fofType) X0) (succ U)))))=> ((((ex_intro fofType) (fun (U:fofType)=> (((eq fofType) (succ X0)) (succ U)))) X0) ((eq_ref fofType) (succ X0)))) as proof of ((ex fofType) (fun (U:fofType)=> (((eq fofType) (succ X0)) (succ U)))) % 17.53/17.97 Found (fun (X0:fofType) (x0:((ex fofType) (fun (U:fofType)=> (((eq fofType) X0) (succ U)))))=> ((((ex_intro fofType) (fun (U:fofType)=> (((eq fofType) (succ X0)) (succ U)))) X0) ((eq_ref fofType) (succ X0)))) as proof of (((ex fofType) (fun (U:fofType)=> (((eq fofType) X0) (succ U))))->((ex fofType) (fun (U:fofType)=> (((eq fofType) (succ X0)) (succ U))))) % 17.53/17.97 Found (fun (X0:fofType) (x0:((ex fofType) (fun (U:fofType)=> (((eq fofType) X0) (succ U)))))=> ((((ex_intro fofType) (fun (U:fofType)=> (((eq fofType) (succ X0)) (succ U)))) X0) ((eq_ref fofType) (succ X0)))) as proof of (forall (X:fofType), (((ex fofType) (fun (U:fofType)=> (((eq fofType) X) (succ U))))->((ex fofType) (fun (U:fofType)=> (((eq fofType) (succ X)) (succ U)))))) % 17.53/17.97 Found eq_ref00:=(eq_ref0 (succ (succ X0))):(((eq fofType) (succ (succ X0))) (succ (succ X0))) % 17.53/17.97 Found (eq_ref0 (succ (succ X0))) as proof of (((eq fofType) (succ (succ X0))) (succ (succ x0))) % 17.53/17.97 Found ((eq_ref fofType) (succ (succ X0))) as proof of (((eq fofType) (succ (succ X0))) (succ (succ x0))) % 17.53/17.97 Found ((eq_ref fofType) (succ (succ X0))) as proof of (((eq fofType) (succ (succ X0))) (succ (succ x0))) % 17.53/17.97 Found (fun (x1:(((eq fofType) (succ X0)) (succ (succ x0))))=> ((eq_ref fofType) (succ (succ X0)))) as proof of (((eq fofType) (succ (succ X0))) (succ (succ x0))) % 17.53/17.97 Found x2:(P (succ (succ X0))) % 17.53/17.97 Instantiate: x0:=X0:fofType % 17.53/17.97 Found (fun (x2:(P (succ (succ X0))))=> x2) as proof of (P (succ (succ x0))) % 17.53/17.97 Found (fun (P:(fofType->Prop)) (x2:(P (succ (succ X0))))=> x2) as proof of ((P (succ (succ X0)))->(P (succ (succ x0)))) % 17.53/17.97 Found (fun (x1:(((eq fofType) (succ X0)) (succ (succ x0)))) (P:(fofType->Prop)) (x2:(P (succ (succ X0))))=> x2) as proof of (((eq fofType) (succ (succ X0))) (succ (succ x0))) % 17.53/17.97 Found eq_ref000:=(eq_ref00 P):((P (succ (succ X0)))->(P (succ (succ X0)))) % 17.53/17.97 Found (eq_ref00 P) as proof of ((P (succ (succ X0)))->(P (succ (succ x0)))) % 17.53/17.97 Found ((eq_ref0 (succ (succ X0))) P) as proof of ((P (succ (succ X0)))->(P (succ (succ x0)))) % 17.53/17.97 Found (((eq_ref fofType) (succ (succ X0))) P) as proof of ((P (succ (succ X0)))->(P (succ (succ x0)))) % 17.53/17.97 Found (((eq_ref fofType) (succ (succ X0))) P) as proof of ((P (succ (succ X0)))->(P (succ (succ x0)))) % 17.53/17.97 Found (fun (P:(fofType->Prop))=> (((eq_ref fofType) (succ (succ X0))) P)) as proof of ((P (succ (succ X0)))->(P (succ (succ x0)))) % 17.53/17.97 Found (fun (x1:(((eq fofType) (succ X0)) (succ (succ x0)))) (P:(fofType->Prop))=> (((eq_ref fofType) (succ (succ X0))) P)) as proof of (((eq fofType) (succ (succ X0))) (succ (succ x0))) % 17.53/17.97 Found eq_ref00:=(eq_ref0 (fun (U:fofType)=> (((eq fofType) X) (succ U)))):(((eq (fofType->Prop)) (fun (U:fofType)=> (((eq fofType) X) (succ U)))) (fun (U:fofType)=> (((eq fofType) X) (succ U)))) % 17.53/17.97 Found (eq_ref0 (fun (U:fofType)=> (((eq fofType) X) (succ U)))) as proof of (((eq (fofType->Prop)) (fun (U:fofType)=> (((eq fofType) X) (succ U)))) b) % 17.53/17.97 Found ((eq_ref (fofType->Prop)) (fun (U:fofType)=> (((eq fofType) X) (succ U)))) as proof of (((eq (fofType->Prop)) (fun (U:fofType)=> (((eq fofType) X) (succ U)))) b) % 17.53/17.97 Found ((eq_ref (fofType->Prop)) (fun (U:fofType)=> (((eq fofType) X) (succ U)))) as proof of (((eq (fofType->Prop)) (fun (U:fofType)=> (((eq fofType) X) (succ U)))) b) % 17.53/17.97 Found ((eq_ref (fofType->Prop)) (fun (U:fofType)=> (((eq fofType) X) (succ U)))) as proof of (((eq (fofType->Prop)) (fun (U:fofType)=> (((eq fofType) X) (succ U)))) b) % 25.92/26.36 Found eq_ref00:=(eq_ref0 (succ (succ X0))):(((eq fofType) (succ (succ X0))) (succ (succ X0))) % 25.92/26.36 Found (eq_ref0 (succ (succ X0))) as proof of (((eq fofType) (succ (succ X0))) (succ (succ x0))) % 25.92/26.36 Found ((eq_ref fofType) (succ (succ X0))) as proof of (((eq fofType) (succ (succ X0))) (succ (succ x0))) % 25.92/26.36 Found ((eq_ref fofType) (succ (succ X0))) as proof of (((eq fofType) (succ (succ X0))) (succ (succ x0))) % 25.92/26.36 Found ((eq_ref fofType) (succ (succ X0))) as proof of (((eq fofType) (succ (succ X0))) (succ (succ x0))) % 25.92/26.36 Found (succ_injective00 ((eq_ref fofType) (succ (succ X0)))) as proof of (((eq fofType) (succ X0)) (succ x0)) % 25.92/26.36 Found ((succ_injective0 (succ x0)) ((eq_ref fofType) (succ (succ X0)))) as proof of (((eq fofType) (succ X0)) (succ x0)) % 25.92/26.36 Found (((succ_injective (succ X0)) (succ x0)) ((eq_ref fofType) (succ (succ X0)))) as proof of (((eq fofType) (succ X0)) (succ x0)) % 25.92/26.36 Found (fun (x1:(((eq fofType) X0) (succ x0)))=> (((succ_injective (succ X0)) (succ x0)) ((eq_ref fofType) (succ (succ X0))))) as proof of (((eq fofType) (succ X0)) (succ x0)) % 25.92/26.36 Found eq_ref00:=(eq_ref0 (succ x0)):(((eq fofType) (succ x0)) (succ x0)) % 25.92/26.36 Found (eq_ref0 (succ x0)) as proof of (((eq fofType) (succ x0)) (succ X0)) % 25.92/26.36 Found ((eq_ref fofType) (succ x0)) as proof of (((eq fofType) (succ x0)) (succ X0)) % 25.92/26.36 Found ((eq_ref fofType) (succ x0)) as proof of (((eq fofType) (succ x0)) (succ X0)) % 25.92/26.36 Found (fun (x1:(((eq fofType) (succ x0)) X0))=> ((eq_ref fofType) (succ x0))) as proof of (((eq fofType) (succ x0)) (succ X0)) % 25.92/26.36 Found eq_ref000:=(eq_ref00 P):((P X)->(P X)) % 25.92/26.36 Found (eq_ref00 P) as proof of (P0 X) % 25.92/26.36 Found ((eq_ref0 X) P) as proof of (P0 X) % 25.92/26.36 Found (((eq_ref fofType) X) P) as proof of (P0 X) % 25.92/26.36 Found (((eq_ref fofType) X) P) as proof of (P0 X) % 25.92/26.36 Found eq_ref00:=(eq_ref0 (f x0)):(((eq Prop) (f x0)) (f x0)) % 25.92/26.36 Found (eq_ref0 (f x0)) as proof of (((eq Prop) (f x0)) (((eq fofType) X) (succ x0))) % 25.92/26.36 Found ((eq_ref Prop) (f x0)) as proof of (((eq Prop) (f x0)) (((eq fofType) X) (succ x0))) % 25.92/26.36 Found ((eq_ref Prop) (f x0)) as proof of (((eq Prop) (f x0)) (((eq fofType) X) (succ x0))) % 25.92/26.36 Found (fun (x0:fofType)=> ((eq_ref Prop) (f x0))) as proof of (((eq Prop) (f x0)) (((eq fofType) X) (succ x0))) % 25.92/26.36 Found (fun (x0:fofType)=> ((eq_ref Prop) (f x0))) as proof of (forall (x:fofType), (((eq Prop) (f x)) (((eq fofType) X) (succ x)))) % 25.92/26.36 Found eq_ref00:=(eq_ref0 (f x0)):(((eq Prop) (f x0)) (f x0)) % 25.92/26.36 Found (eq_ref0 (f x0)) as proof of (((eq Prop) (f x0)) (((eq fofType) X) (succ x0))) % 25.92/26.36 Found ((eq_ref Prop) (f x0)) as proof of (((eq Prop) (f x0)) (((eq fofType) X) (succ x0))) % 25.92/26.36 Found ((eq_ref Prop) (f x0)) as proof of (((eq Prop) (f x0)) (((eq fofType) X) (succ x0))) % 25.92/26.36 Found (fun (x0:fofType)=> ((eq_ref Prop) (f x0))) as proof of (((eq Prop) (f x0)) (((eq fofType) X) (succ x0))) % 25.92/26.36 Found (fun (x0:fofType)=> ((eq_ref Prop) (f x0))) as proof of (forall (x:fofType), (((eq Prop) (f x)) (((eq fofType) X) (succ x)))) % 25.92/26.36 Found eq_ref00:=(eq_ref0 (fofType->(((ex fofType) (fun (U:fofType)=> (((eq fofType) X) (succ U))))->((ex fofType) (fun (U:fofType)=> (((eq fofType) X) (succ U))))))):(((eq Prop) (fofType->(((ex fofType) (fun (U:fofType)=> (((eq fofType) X) (succ U))))->((ex fofType) (fun (U:fofType)=> (((eq fofType) X) (succ U))))))) (fofType->(((ex fofType) (fun (U:fofType)=> (((eq fofType) X) (succ U))))->((ex fofType) (fun (U:fofType)=> (((eq fofType) X) (succ U))))))) % 25.92/26.36 Found (eq_ref0 (fofType->(((ex fofType) (fun (U:fofType)=> (((eq fofType) X) (succ U))))->((ex fofType) (fun (U:fofType)=> (((eq fofType) X) (succ U))))))) as proof of (((eq Prop) (fofType->(((ex fofType) (fun (U:fofType)=> (((eq fofType) X) (succ U))))->((ex fofType) (fun (U:fofType)=> (((eq fofType) X) (succ U))))))) b) % 25.92/26.36 Found ((eq_ref Prop) (fofType->(((ex fofType) (fun (U:fofType)=> (((eq fofType) X) (succ U))))->((ex fofType) (fun (U:fofType)=> (((eq fofType) X) (succ U))))))) as proof of (((eq Prop) (fofType->(((ex fofType) (fun (U:fofType)=> (((eq fofType) X) (succ U))))->((ex fofType) (fun (U:fofType)=> (((eq fofType) X) (succ U))))))) b) % 25.92/26.36 Found ((eq_ref Prop) (fofType->(((ex fofType) (fun (U:fofType)=> (((eq fofType) X) (succ U))))->((ex fofType) (fun (U:fofType)=> (((eq fofType) X) (succ U))))))) as proof of (((eq Prop) (fofType->(((ex fofType) (fun (U:fofType)=> (((eq fofType) X) (succ U))))->((ex fofType) (fun (U:fofType)=> (((eq fofType) X) (succ U))))))) b) % 34.63/35.07 Found ((eq_ref Prop) (fofType->(((ex fofType) (fun (U:fofType)=> (((eq fofType) X) (succ U))))->((ex fofType) (fun (U:fofType)=> (((eq fofType) X) (succ U))))))) as proof of (((eq Prop) (fofType->(((ex fofType) (fun (U:fofType)=> (((eq fofType) X) (succ U))))->((ex fofType) (fun (U:fofType)=> (((eq fofType) X) (succ U))))))) b) % 34.63/35.07 Found eq_ref00:=(eq_ref0 (forall (X:fofType), (((ex fofType) (fun (U:fofType)=> (((eq fofType) X) (succ U))))->((ex fofType) (fun (U:fofType)=> (((eq fofType) (succ X)) (succ U))))))):(((eq Prop) (forall (X:fofType), (((ex fofType) (fun (U:fofType)=> (((eq fofType) X) (succ U))))->((ex fofType) (fun (U:fofType)=> (((eq fofType) (succ X)) (succ U))))))) (forall (X:fofType), (((ex fofType) (fun (U:fofType)=> (((eq fofType) X) (succ U))))->((ex fofType) (fun (U:fofType)=> (((eq fofType) (succ X)) (succ U))))))) % 34.63/35.07 Found (eq_ref0 (forall (X:fofType), (((ex fofType) (fun (U:fofType)=> (((eq fofType) X) (succ U))))->((ex fofType) (fun (U:fofType)=> (((eq fofType) (succ X)) (succ U))))))) as proof of (((eq Prop) (forall (X:fofType), (((ex fofType) (fun (U:fofType)=> (((eq fofType) X) (succ U))))->((ex fofType) (fun (U:fofType)=> (((eq fofType) (succ X)) (succ U))))))) b) % 34.63/35.07 Found ((eq_ref Prop) (forall (X:fofType), (((ex fofType) (fun (U:fofType)=> (((eq fofType) X) (succ U))))->((ex fofType) (fun (U:fofType)=> (((eq fofType) (succ X)) (succ U))))))) as proof of (((eq Prop) (forall (X:fofType), (((ex fofType) (fun (U:fofType)=> (((eq fofType) X) (succ U))))->((ex fofType) (fun (U:fofType)=> (((eq fofType) (succ X)) (succ U))))))) b) % 34.63/35.07 Found ((eq_ref Prop) (forall (X:fofType), (((ex fofType) (fun (U:fofType)=> (((eq fofType) X) (succ U))))->((ex fofType) (fun (U:fofType)=> (((eq fofType) (succ X)) (succ U))))))) as proof of (((eq Prop) (forall (X:fofType), (((ex fofType) (fun (U:fofType)=> (((eq fofType) X) (succ U))))->((ex fofType) (fun (U:fofType)=> (((eq fofType) (succ X)) (succ U))))))) b) % 34.63/35.07 Found ((eq_ref Prop) (forall (X:fofType), (((ex fofType) (fun (U:fofType)=> (((eq fofType) X) (succ U))))->((ex fofType) (fun (U:fofType)=> (((eq fofType) (succ X)) (succ U))))))) as proof of (((eq Prop) (forall (X:fofType), (((ex fofType) (fun (U:fofType)=> (((eq fofType) X) (succ U))))->((ex fofType) (fun (U:fofType)=> (((eq fofType) (succ X)) (succ U))))))) b) % 34.63/35.07 Found eq_ref000:=(eq_ref00 P):((P (succ x0))->(P (succ x0))) % 34.63/35.07 Found (eq_ref00 P) as proof of ((P (succ x0))->(P (succ X0))) % 34.63/35.07 Found ((eq_ref0 (succ x0)) P) as proof of ((P (succ x0))->(P (succ X0))) % 34.63/35.07 Found (((eq_ref fofType) (succ x0)) P) as proof of ((P (succ x0))->(P (succ X0))) % 34.63/35.07 Found (((eq_ref fofType) (succ x0)) P) as proof of ((P (succ x0))->(P (succ X0))) % 34.63/35.07 Found (fun (P:(fofType->Prop))=> (((eq_ref fofType) (succ x0)) P)) as proof of ((P (succ x0))->(P (succ X0))) % 34.63/35.07 Found (fun (x1:(((eq fofType) (succ x0)) X0)) (P:(fofType->Prop))=> (((eq_ref fofType) (succ x0)) P)) as proof of (((eq fofType) (succ x0)) (succ X0)) % 34.63/35.07 Found x2:(P (succ x0)) % 34.63/35.07 Instantiate: x0:=X0:fofType % 34.63/35.07 Found (fun (x2:(P (succ x0)))=> x2) as proof of (P (succ X0)) % 34.63/35.07 Found (fun (P:(fofType->Prop)) (x2:(P (succ x0)))=> x2) as proof of ((P (succ x0))->(P (succ X0))) % 34.63/35.07 Found (fun (x1:(((eq fofType) (succ x0)) X0)) (P:(fofType->Prop)) (x2:(P (succ x0)))=> x2) as proof of (((eq fofType) (succ x0)) (succ X0)) % 34.63/35.07 Found eq_ref000:=(eq_ref00 P):((P X)->(P X)) % 34.63/35.07 Found (eq_ref00 P) as proof of (P0 X) % 34.63/35.07 Found ((eq_ref0 X) P) as proof of (P0 X) % 34.63/35.07 Found (((eq_ref fofType) X) P) as proof of (P0 X) % 34.63/35.07 Found (((eq_ref fofType) X) P) as proof of (P0 X) % 34.63/35.07 Found eq_ref00:=(eq_ref0 (succ x0)):(((eq fofType) (succ x0)) (succ x0)) % 34.63/35.07 Found (eq_ref0 (succ x0)) as proof of (((eq fofType) (succ x0)) (succ X0)) % 34.63/35.07 Found ((eq_ref fofType) (succ x0)) as proof of (((eq fofType) (succ x0)) (succ X0)) % 34.63/35.07 Found ((eq_ref fofType) (succ x0)) as proof of (((eq fofType) (succ x0)) (succ X0)) % 54.48/54.98 Found ((eq_ref fofType) (succ x0)) as proof of (((eq fofType) (succ x0)) (succ X0)) % 54.48/54.98 Found (eq_sym000 ((eq_ref fofType) (succ x0))) as proof of (((eq fofType) (succ X0)) (succ x0)) % 54.48/54.98 Found ((eq_sym00 (succ X0)) ((eq_ref fofType) (succ x0))) as proof of (((eq fofType) (succ X0)) (succ x0)) % 54.48/54.98 Found (((eq_sym0 (succ x0)) (succ X0)) ((eq_ref fofType) (succ x0))) as proof of (((eq fofType) (succ X0)) (succ x0)) % 54.48/54.98 Found ((((eq_sym fofType) (succ x0)) (succ X0)) ((eq_ref fofType) (succ x0))) as proof of (((eq fofType) (succ X0)) (succ x0)) % 54.48/54.98 Found (fun (x1:(((eq fofType) X0) (succ x0)))=> ((((eq_sym fofType) (succ x0)) (succ X0)) ((eq_ref fofType) (succ x0)))) as proof of (((eq fofType) (succ X0)) (succ x0)) % 54.48/54.98 Found x1:(P (succ x0)) % 54.48/54.98 Instantiate: x0:=X0:fofType % 54.48/54.98 Found x1 as proof of (P (succ X0)) % 54.48/54.98 Found (fun (x2:(P X0))=> x1) as proof of (P (succ X0)) % 54.48/54.98 Found x1:(P (succ x0)) % 54.48/54.98 Instantiate: x0:=X0:fofType % 54.48/54.98 Found x1 as proof of (P (succ X0)) % 54.48/54.98 Found (fun (x2:(P X0))=> x1) as proof of (P (succ X0)) % 54.48/54.98 Found x1:(P (succ x0)) % 54.48/54.98 Instantiate: x0:=X0:fofType % 54.48/54.98 Found x1 as proof of (P (succ X0)) % 54.48/54.98 Found (fun (x2:(P X0))=> x1) as proof of (P (succ X0)) % 54.48/54.98 Found x1:(P (succ x0)) % 54.48/54.98 Instantiate: x0:=X0:fofType % 54.48/54.98 Found x1 as proof of (P (succ X0)) % 54.48/54.98 Found (fun (x2:(P X0))=> x1) as proof of (P (succ X0)) % 54.48/54.98 Found one_is_first:(forall (X:fofType), (not (((eq fofType) (succ X)) one))) % 54.48/54.98 Instantiate: b:=(forall (X:fofType), (not (((eq fofType) (succ X)) one))):Prop % 54.48/54.98 Found one_is_first as proof of b % 54.48/54.98 Found eq_ref00:=(eq_ref0 (succ (succ x0))):(((eq fofType) (succ (succ x0))) (succ (succ x0))) % 54.48/54.98 Found (eq_ref0 (succ (succ x0))) as proof of (((eq fofType) (succ (succ x0))) (succ (succ X0))) % 54.48/54.98 Found ((eq_ref fofType) (succ (succ x0))) as proof of (((eq fofType) (succ (succ x0))) (succ (succ X0))) % 54.48/54.98 Found ((eq_ref fofType) (succ (succ x0))) as proof of (((eq fofType) (succ (succ x0))) (succ (succ X0))) % 54.48/54.98 Found (fun (x1:(((eq fofType) (succ (succ x0))) (succ X0)))=> ((eq_ref fofType) (succ (succ x0)))) as proof of (((eq fofType) (succ (succ x0))) (succ (succ X0))) % 54.48/54.98 Found eq_ref00:=(eq_ref0 (succ (succ x0))):(((eq fofType) (succ (succ x0))) (succ (succ x0))) % 54.48/54.98 Found (eq_ref0 (succ (succ x0))) as proof of (((eq fofType) (succ (succ x0))) (succ (succ X0))) % 54.48/54.98 Found ((eq_ref fofType) (succ (succ x0))) as proof of (((eq fofType) (succ (succ x0))) (succ (succ X0))) % 54.48/54.98 Found ((eq_ref fofType) (succ (succ x0))) as proof of (((eq fofType) (succ (succ x0))) (succ (succ X0))) % 54.48/54.98 Found (fun (x1:(((eq fofType) (succ (succ x0))) (succ X0)))=> ((eq_ref fofType) (succ (succ x0)))) as proof of (((eq fofType) (succ (succ x0))) (succ (succ X0))) % 54.48/54.98 Found eq_ref00:=(eq_ref0 (forall (X:fofType), (((and ((ex fofType) (fun (U:fofType)=> (((eq fofType) X) (succ U))))) (forall (X0:fofType), (((ex fofType) (fun (U:fofType)=> (((eq fofType) X0) (succ U))))->((ex fofType) (fun (U:fofType)=> (((eq fofType) (succ X0)) (succ U)))))))->((and ((ex fofType) (fun (U:fofType)=> (((eq fofType) (succ X)) (succ U))))) (forall (X0:fofType), (((ex fofType) (fun (U:fofType)=> (((eq fofType) X0) (succ U))))->((ex fofType) (fun (U:fofType)=> (((eq fofType) (succ X0)) (succ U)))))))))):(((eq Prop) (forall (X:fofType), (((and ((ex fofType) (fun (U:fofType)=> (((eq fofType) X) (succ U))))) (forall (X0:fofType), (((ex fofType) (fun (U:fofType)=> (((eq fofType) X0) (succ U))))->((ex fofType) (fun (U:fofType)=> (((eq fofType) (succ X0)) (succ U)))))))->((and ((ex fofType) (fun (U:fofType)=> (((eq fofType) (succ X)) (succ U))))) (forall (X0:fofType), (((ex fofType) (fun (U:fofType)=> (((eq fofType) X0) (succ U))))->((ex fofType) (fun (U:fofType)=> (((eq fofType) (succ X0)) (succ U)))))))))) (forall (X:fofType), (((and ((ex fofType) (fun (U:fofType)=> (((eq fofType) X) (succ U))))) (forall (X0:fofType), (((ex fofType) (fun (U:fofType)=> (((eq fofType) X0) (succ U))))->((ex fofType) (fun (U:fofType)=> (((eq fofType) (succ X0)) (succ U)))))))->((and ((ex fofType) (fun (U:fofType)=> (((eq fofType) (succ X)) (succ U))))) (forall (X0:fofType), (((ex fofType) (fun (U:fofType)=> (((eq fofType) X0) (succ U))))->((ex fofType) (fun (U:fofType)=> (((eq fofType) (succ X0)) (succ U)))))))))) % 54.48/54.99 Found (eq_ref0 (forall (X:fofType), (((and ((ex fofType) (fun (U:fofType)=> (((eq fofType) X) (succ U))))) (forall (X0:fofType), (((ex fofType) (fun (U:fofType)=> (((eq fofType) X0) (succ U))))->((ex fofType) (fun (U:fofType)=> (((eq fofType) (succ X0)) (succ U)))))))->((and ((ex fofType) (fun (U:fofType)=> (((eq fofType) (succ X)) (succ U))))) (forall (X0:fofType), (((ex fofType) (fun (U:fofType)=> (((eq fofType) X0) (succ U))))->((ex fofType) (fun (U:fofType)=> (((eq fofType) (succ X0)) (succ U)))))))))) as proof of (((eq Prop) (forall (X:fofType), (((and ((ex fofType) (fun (U:fofType)=> (((eq fofType) X) (succ U))))) (forall (X0:fofType), (((ex fofType) (fun (U:fofType)=> (((eq fofType) X0) (succ U))))->((ex fofType) (fun (U:fofType)=> (((eq fofType) (succ X0)) (succ U)))))))->((and ((ex fofType) (fun (U:fofType)=> (((eq fofType) (succ X)) (succ U))))) (forall (X0:fofType), (((ex fofType) (fun (U:fofType)=> (((eq fofType) X0) (succ U))))->((ex fofType) (fun (U:fofType)=> (((eq fofType) (succ X0)) (succ U)))))))))) b) % 54.48/54.99 Found ((eq_ref Prop) (forall (X:fofType), (((and ((ex fofType) (fun (U:fofType)=> (((eq fofType) X) (succ U))))) (forall (X0:fofType), (((ex fofType) (fun (U:fofType)=> (((eq fofType) X0) (succ U))))->((ex fofType) (fun (U:fofType)=> (((eq fofType) (succ X0)) (succ U)))))))->((and ((ex fofType) (fun (U:fofType)=> (((eq fofType) (succ X)) (succ U))))) (forall (X0:fofType), (((ex fofType) (fun (U:fofType)=> (((eq fofType) X0) (succ U))))->((ex fofType) (fun (U:fofType)=> (((eq fofType) (succ X0)) (succ U)))))))))) as proof of (((eq Prop) (forall (X:fofType), (((and ((ex fofType) (fun (U:fofType)=> (((eq fofType) X) (succ U))))) (forall (X0:fofType), (((ex fofType) (fun (U:fofType)=> (((eq fofType) X0) (succ U))))->((ex fofType) (fun (U:fofType)=> (((eq fofType) (succ X0)) (succ U)))))))->((and ((ex fofType) (fun (U:fofType)=> (((eq fofType) (succ X)) (succ U))))) (forall (X0:fofType), (((ex fofType) (fun (U:fofType)=> (((eq fofType) X0) (succ U))))->((ex fofType) (fun (U:fofType)=> (((eq fofType) (succ X0)) (succ U)))))))))) b) % 54.48/54.99 Found ((eq_ref Prop) (forall (X:fofType), (((and ((ex fofType) (fun (U:fofType)=> (((eq fofType) X) (succ U))))) (forall (X0:fofType), (((ex fofType) (fun (U:fofType)=> (((eq fofType) X0) (succ U))))->((ex fofType) (fun (U:fofType)=> (((eq fofType) (succ X0)) (succ U)))))))->((and ((ex fofType) (fun (U:fofType)=> (((eq fofType) (succ X)) (succ U))))) (forall (X0:fofType), (((ex fofType) (fun (U:fofType)=> (((eq fofType) X0) (succ U))))->((ex fofType) (fun (U:fofType)=> (((eq fofType) (succ X0)) (succ U)))))))))) as proof of (((eq Prop) (forall (X:fofType), (((and ((ex fofType) (fun (U:fofType)=> (((eq fofType) X) (succ U))))) (forall (X0:fofType), (((ex fofType) (fun (U:fofType)=> (((eq fofType) X0) (succ U))))->((ex fofType) (fun (U:fofType)=> (((eq fofType) (succ X0)) (succ U)))))))->((and ((ex fofType) (fun (U:fofType)=> (((eq fofType) (succ X)) (succ U))))) (forall (X0:fofType), (((ex fofType) (fun (U:fofType)=> (((eq fofType) X0) (succ U))))->((ex fofType) (fun (U:fofType)=> (((eq fofType) (succ X0)) (succ U)))))))))) b) % 54.48/54.99 Found ((eq_ref Prop) (forall (X:fofType), (((and ((ex fofType) (fun (U:fofType)=> (((eq fofType) X) (succ U))))) (forall (X0:fofType), (((ex fofType) (fun (U:fofType)=> (((eq fofType) X0) (succ U))))->((ex fofType) (fun (U:fofType)=> (((eq fofType) (succ X0)) (succ U)))))))->((and ((ex fofType) (fun (U:fofType)=> (((eq fofType) (succ X)) (succ U))))) (forall (X0:fofType), (((ex fofType) (fun (U:fofType)=> (((eq fofType) X0) (succ U))))->((ex fofType) (fun (U:fofType)=> (((eq fofType) (succ X0)) (succ U)))))))))) as proof of (((eq Prop) (forall (X:fofType), (((and ((ex fofType) (fun (U:fofType)=> (((eq fofType) X) (succ U))))) (forall (X0:fofType), (((ex fofType) (fun (U:fofType)=> (((eq fofType) X0) (succ U))))->((ex fofType) (fun (U:fofType)=> (((eq fofType) (succ X0)) (succ U)))))))->((and ((ex fofType) (fun (U:fofType)=> (((eq fofType) (succ X)) (succ U))))) (forall (X0:fofType), (((ex fofType) (fun (U:fofType)=> (((eq fofType) X0) (succ U))))->((ex fofType) (fun (U:fofType)=> (((eq fofType) (succ X0)) (succ U)))))))))) b) % 64.58/65.10 Found eq_ref00:=(eq_ref0 X):(((eq fofType) X) X) % 64.58/65.10 Found (eq_ref0 X) as proof of (((eq fofType) X) b) % 64.58/65.10 Found ((eq_ref fofType) X) as proof of (((eq fofType) X) b) % 64.58/65.10 Found ((eq_ref fofType) X) as proof of (((eq fofType) X) b) % 64.58/65.10 Found ((eq_ref fofType) X) as proof of (((eq fofType) X) b) % 64.58/65.10 Found eq_ref00:=(eq_ref0 b):(((eq fofType) b) b) % 64.58/65.10 Found (eq_ref0 b) as proof of (((eq fofType) b) (succ x0)) % 64.58/65.10 Found ((eq_ref fofType) b) as proof of (((eq fofType) b) (succ x0)) % 64.58/65.10 Found ((eq_ref fofType) b) as proof of (((eq fofType) b) (succ x0)) % 64.58/65.10 Found ((eq_ref fofType) b) as proof of (((eq fofType) b) (succ x0)) % 64.58/65.10 Found eq_ref000:=(eq_ref00 P):((P (succ X))->(P (succ X))) % 64.58/65.10 Found (eq_ref00 P) as proof of (P0 (succ X)) % 64.58/65.10 Found ((eq_ref0 (succ X)) P) as proof of (P0 (succ X)) % 64.58/65.10 Found (((eq_ref fofType) (succ X)) P) as proof of (P0 (succ X)) % 64.58/65.10 Found (((eq_ref fofType) (succ X)) P) as proof of (P0 (succ X)) % 64.58/65.10 Found eq_ref000:=(eq_ref00 P):((P (succ x0))->(P (succ x0))) % 64.58/65.10 Found (eq_ref00 P) as proof of (P0 (succ x0)) % 64.58/65.10 Found ((eq_ref0 (succ x0)) P) as proof of (P0 (succ x0)) % 64.58/65.10 Found (((eq_ref fofType) (succ x0)) P) as proof of (P0 (succ x0)) % 64.58/65.10 Found (((eq_ref fofType) (succ x0)) P) as proof of (P0 (succ x0)) % 64.58/65.10 Found x1:(((eq fofType) X0) (succ x0)) % 64.58/65.10 Instantiate: x0:=X0:fofType % 64.58/65.10 Found x1 as proof of (((eq fofType) X0) (succ X0)) % 64.58/65.10 Found (eq_sym000 x1) as proof of (((eq fofType) (succ X0)) X0) % 64.58/65.10 Found ((eq_sym00 (succ X0)) x1) as proof of (((eq fofType) (succ X0)) X0) % 64.58/65.10 Found (((eq_sym0 X0) (succ X0)) x1) as proof of (((eq fofType) (succ X0)) X0) % 64.58/65.10 Found ((((eq_sym fofType) X0) (succ X0)) x1) as proof of (((eq fofType) (succ X0)) X0) % 64.58/65.10 Found ((((eq_sym fofType) X0) (succ X0)) x1) as proof of (((eq fofType) (succ X0)) X0) % 64.58/65.10 Found (x10 ((((eq_sym fofType) X0) (succ X0)) x1)) as proof of (((eq fofType) (succ X0)) (succ x0)) % 64.58/65.10 Found ((x1 ((eq fofType) (succ X0))) ((((eq_sym fofType) X0) (succ X0)) x1)) as proof of (((eq fofType) (succ X0)) (succ x0)) % 64.58/65.10 Found (fun (x1:(((eq fofType) X0) (succ x0)))=> ((x1 ((eq fofType) (succ X0))) ((((eq_sym fofType) X0) (succ X0)) x1))) as proof of (((eq fofType) (succ X0)) (succ x0)) % 64.58/65.10 Found eta_expansion000:=(eta_expansion00 (fun (U:fofType)=> (((eq fofType) one) (succ U)))):(((eq (fofType->Prop)) (fun (U:fofType)=> (((eq fofType) one) (succ U)))) (fun (x:fofType)=> (((eq fofType) one) (succ x)))) % 64.58/65.10 Found (eta_expansion00 (fun (U:fofType)=> (((eq fofType) one) (succ U)))) as proof of (((eq (fofType->Prop)) (fun (U:fofType)=> (((eq fofType) one) (succ U)))) b) % 64.58/65.10 Found ((eta_expansion0 Prop) (fun (U:fofType)=> (((eq fofType) one) (succ U)))) as proof of (((eq (fofType->Prop)) (fun (U:fofType)=> (((eq fofType) one) (succ U)))) b) % 64.58/65.10 Found (((eta_expansion fofType) Prop) (fun (U:fofType)=> (((eq fofType) one) (succ U)))) as proof of (((eq (fofType->Prop)) (fun (U:fofType)=> (((eq fofType) one) (succ U)))) b) % 64.58/65.10 Found (((eta_expansion fofType) Prop) (fun (U:fofType)=> (((eq fofType) one) (succ U)))) as proof of (((eq (fofType->Prop)) (fun (U:fofType)=> (((eq fofType) one) (succ U)))) b) % 64.58/65.10 Found (((eta_expansion fofType) Prop) (fun (U:fofType)=> (((eq fofType) one) (succ U)))) as proof of (((eq (fofType->Prop)) (fun (U:fofType)=> (((eq fofType) one) (succ U)))) b) % 64.58/65.10 Found eq_ref00:=(eq_ref0 X0):(((eq fofType) X0) X0) % 64.58/65.10 Found (eq_ref0 X0) as proof of (((eq fofType) X0) x0) % 64.58/65.10 Found ((eq_ref fofType) X0) as proof of (((eq fofType) X0) x0) % 64.58/65.10 Found ((eq_ref fofType) X0) as proof of (((eq fofType) X0) x0) % 64.58/65.10 Found ((eq_ref fofType) X0) as proof of (((eq fofType) X0) x0) % 64.58/65.10 Found (eq_substitution00000 ((eq_ref fofType) X0)) as proof of (((eq fofType) (succ X0)) (succ x0)) % 64.58/65.10 Found ((eq_substitution0000 succ) ((eq_ref fofType) X0)) as proof of (((eq fofType) (succ X0)) (succ x0)) % 64.58/65.10 Found (((eq_substitution000 x0) succ) ((eq_ref fofType) X0)) as proof of (((eq fofType) (succ X0)) (succ x0)) % 64.58/65.10 Found ((((eq_substitution00 X0) x0) succ) ((eq_ref fofType) X0)) as proof of (((eq fofType) (succ X0)) (succ x0)) % 64.58/65.10 Found (((((eq_substitution0 fofType) X0) x0) succ) ((eq_ref fofType) X0)) as proof of (((eq fofType) (succ X0)) (succ x0)) % 74.19/74.72 Found ((((((eq_substitution fofType) fofType) X0) x0) succ) ((eq_ref fofType) X0)) as proof of (((eq fofType) (succ X0)) (succ x0)) % 74.19/74.72 Found (fun (x1:(((eq fofType) X0) (succ x0)))=> ((((((eq_substitution fofType) fofType) X0) x0) succ) ((eq_ref fofType) X0))) as proof of (((eq fofType) (succ X0)) (succ x0)) % 74.19/74.72 Found eq_ref00:=(eq_ref0 (succ (succ X0))):(((eq fofType) (succ (succ X0))) (succ (succ X0))) % 74.19/74.72 Found (eq_ref0 (succ (succ X0))) as proof of (((eq fofType) (succ (succ X0))) (succ (succ x0))) % 74.19/74.72 Found ((eq_ref fofType) (succ (succ X0))) as proof of (((eq fofType) (succ (succ X0))) (succ (succ x0))) % 74.19/74.72 Found ((eq_ref fofType) (succ (succ X0))) as proof of (((eq fofType) (succ (succ X0))) (succ (succ x0))) % 74.19/74.72 Found (fun (x1:(((eq fofType) (succ X0)) (succ (succ x0))))=> ((eq_ref fofType) (succ (succ X0)))) as proof of (((eq fofType) (succ (succ X0))) (succ (succ x0))) % 74.19/74.72 Found eq_ref000:=(eq_ref00 P):((P (succ (succ x0)))->(P (succ (succ x0)))) % 74.19/74.72 Found (eq_ref00 P) as proof of ((P (succ (succ x0)))->(P (succ (succ X0)))) % 74.19/74.72 Found ((eq_ref0 (succ (succ x0))) P) as proof of ((P (succ (succ x0)))->(P (succ (succ X0)))) % 74.19/74.72 Found (((eq_ref fofType) (succ (succ x0))) P) as proof of ((P (succ (succ x0)))->(P (succ (succ X0)))) % 74.19/74.72 Found (((eq_ref fofType) (succ (succ x0))) P) as proof of ((P (succ (succ x0)))->(P (succ (succ X0)))) % 74.19/74.72 Found (fun (P:(fofType->Prop))=> (((eq_ref fofType) (succ (succ x0))) P)) as proof of ((P (succ (succ x0)))->(P (succ (succ X0)))) % 74.19/74.72 Found (fun (x1:(((eq fofType) (succ (succ x0))) (succ X0))) (P:(fofType->Prop))=> (((eq_ref fofType) (succ (succ x0))) P)) as proof of (((eq fofType) (succ (succ x0))) (succ (succ X0))) % 74.19/74.72 Found x2:(P (succ (succ x0))) % 74.19/74.72 Instantiate: x0:=X0:fofType % 74.19/74.72 Found (fun (x2:(P (succ (succ x0))))=> x2) as proof of (P (succ (succ X0))) % 74.19/74.72 Found (fun (P:(fofType->Prop)) (x2:(P (succ (succ x0))))=> x2) as proof of ((P (succ (succ x0)))->(P (succ (succ X0)))) % 74.19/74.72 Found (fun (x1:(((eq fofType) (succ (succ x0))) (succ X0))) (P:(fofType->Prop)) (x2:(P (succ (succ x0))))=> x2) as proof of (((eq fofType) (succ (succ x0))) (succ (succ X0))) % 74.27/74.72 Found eq_ref000:=(eq_ref00 P):((P (succ (succ x0)))->(P (succ (succ x0)))) % 74.27/74.72 Found (eq_ref00 P) as proof of ((P (succ (succ x0)))->(P (succ (succ X0)))) % 74.27/74.72 Found ((eq_ref0 (succ (succ x0))) P) as proof of ((P (succ (succ x0)))->(P (succ (succ X0)))) % 74.27/74.72 Found (((eq_ref fofType) (succ (succ x0))) P) as proof of ((P (succ (succ x0)))->(P (succ (succ X0)))) % 74.27/74.72 Found (((eq_ref fofType) (succ (succ x0))) P) as proof of ((P (succ (succ x0)))->(P (succ (succ X0)))) % 74.27/74.72 Found (fun (P:(fofType->Prop))=> (((eq_ref fofType) (succ (succ x0))) P)) as proof of ((P (succ (succ x0)))->(P (succ (succ X0)))) % 74.27/74.72 Found (fun (x1:(((eq fofType) (succ (succ x0))) (succ X0))) (P:(fofType->Prop))=> (((eq_ref fofType) (succ (succ x0))) P)) as proof of (((eq fofType) (succ (succ x0))) (succ (succ X0))) % 74.27/74.72 Found x2:(P (succ (succ x0))) % 74.27/74.72 Instantiate: x0:=X0:fofType % 74.27/74.72 Found (fun (x2:(P (succ (succ x0))))=> x2) as proof of (P (succ (succ X0))) % 74.27/74.72 Found (fun (P:(fofType->Prop)) (x2:(P (succ (succ x0))))=> x2) as proof of ((P (succ (succ x0)))->(P (succ (succ X0)))) % 74.27/74.72 Found (fun (x1:(((eq fofType) (succ (succ x0))) (succ X0))) (P:(fofType->Prop)) (x2:(P (succ (succ x0))))=> x2) as proof of (((eq fofType) (succ (succ x0))) (succ (succ X0))) % 74.27/74.72 Found x1:(P (succ x0)) % 74.27/74.72 Instantiate: x0:=X0:fofType % 74.27/74.72 Found x1 as proof of (P (succ X0)) % 74.27/74.72 Found (fun (x2:(P X0))=> x1) as proof of (P (succ X0)) % 74.27/74.72 Found eq_ref00:=(eq_ref0 (succ (succ x0))):(((eq fofType) (succ (succ x0))) (succ (succ x0))) % 74.27/74.72 Found (eq_ref0 (succ (succ x0))) as proof of (((eq fofType) (succ (succ x0))) (succ (succ X0))) % 74.27/74.72 Found ((eq_ref fofType) (succ (succ x0))) as proof of (((eq fofType) (succ (succ x0))) (succ (succ X0))) % 74.27/74.72 Found ((eq_ref fofType) (succ (succ x0))) as proof of (((eq fofType) (succ (succ x0))) (succ (succ X0))) % 74.27/74.72 Found ((eq_ref fofType) (succ (succ x0))) as proof of (((eq fofType) (succ (succ x0))) (succ (succ X0))) % 74.27/74.72 Found (succ_injective00 ((eq_ref fofType) (succ (succ x0)))) as proof of (((eq fofType) (succ x0)) (succ X0)) % 74.27/74.72 Found ((succ_injective0 (succ X0)) ((eq_ref fofType) (succ (succ x0)))) as proof of (((eq fofType) (succ x0)) (succ X0)) % 80.23/80.72 Found (((succ_injective (succ x0)) (succ X0)) ((eq_ref fofType) (succ (succ x0)))) as proof of (((eq fofType) (succ x0)) (succ X0)) % 80.23/80.72 Found (fun (x1:(((eq fofType) (succ x0)) X0))=> (((succ_injective (succ x0)) (succ X0)) ((eq_ref fofType) (succ (succ x0))))) as proof of (((eq fofType) (succ x0)) (succ X0)) % 80.23/80.72 Found eq_ref000:=(eq_ref00 P):((P (succ x0))->(P (succ x0))) % 80.23/80.72 Found (eq_ref00 P) as proof of (P0 (succ x0)) % 80.23/80.72 Found ((eq_ref0 (succ x0)) P) as proof of (P0 (succ x0)) % 80.23/80.72 Found (((eq_ref fofType) (succ x0)) P) as proof of (P0 (succ x0)) % 80.23/80.72 Found (((eq_ref fofType) (succ x0)) P) as proof of (P0 (succ x0)) % 80.23/80.72 Found eq_ref00:=(eq_ref0 X0):(((eq fofType) X0) X0) % 80.23/80.72 Found (eq_ref0 X0) as proof of (((eq fofType) X0) x0) % 80.23/80.72 Found ((eq_ref fofType) X0) as proof of (((eq fofType) X0) x0) % 80.23/80.72 Found ((eq_ref fofType) X0) as proof of (((eq fofType) X0) x0) % 80.23/80.72 Found (eq_substitution00000 ((eq_ref fofType) X0)) as proof of (((eq fofType) (succ X0)) (succ x0)) % 80.23/80.72 Found (eq_substitution00000 ((eq_ref fofType) X0)) as proof of (((eq fofType) (succ X0)) (succ x0)) % 80.23/80.72 Found ((eq_substitution0000 (fun (x5:fofType)=> (succ X0))) ((eq_ref fofType) X0)) as proof of (((eq fofType) (succ X0)) (succ x0)) % 80.23/80.72 Found (((eq_substitution000 x0) (fun (x5:fofType)=> (succ X0))) ((eq_ref fofType) X0)) as proof of (((eq fofType) (succ X0)) (succ x0)) % 80.23/80.72 Found ((((eq_substitution00 X0) x0) (fun (x5:fofType)=> (succ X0))) ((eq_ref fofType) X0)) as proof of (((eq fofType) (succ X0)) (succ x0)) % 80.23/80.72 Found (((((eq_substitution0 fofType) X0) x0) (fun (x5:fofType)=> (succ X0))) ((eq_ref fofType) X0)) as proof of (((eq fofType) (succ X0)) (succ x0)) % 80.23/80.72 Found ((((((eq_substitution fofType) fofType) X0) x0) (fun (x5:fofType)=> (succ X0))) ((eq_ref fofType) X0)) as proof of (((eq fofType) (succ X0)) (succ x0)) % 80.23/80.72 Found (fun (x1:(((eq fofType) X0) (succ x0)))=> ((((((eq_substitution fofType) fofType) X0) x0) (fun (x5:fofType)=> (succ X0))) ((eq_ref fofType) X0))) as proof of (((eq fofType) (succ X0)) (succ x0)) % 80.23/80.72 Found eq_ref00:=(eq_ref0 (succ (succ x0))):(((eq fofType) (succ (succ x0))) (succ (succ x0))) % 80.23/80.72 Found (eq_ref0 (succ (succ x0))) as proof of (((eq fofType) (succ (succ x0))) (succ (succ X0))) % 80.23/80.72 Found ((eq_ref fofType) (succ (succ x0))) as proof of (((eq fofType) (succ (succ x0))) (succ (succ X0))) % 80.23/80.72 Found ((eq_ref fofType) (succ (succ x0))) as proof of (((eq fofType) (succ (succ x0))) (succ (succ X0))) % 80.23/80.72 Found ((eq_ref fofType) (succ (succ x0))) as proof of (((eq fofType) (succ (succ x0))) (succ (succ X0))) % 80.23/80.72 Found (eq_sym000 ((eq_ref fofType) (succ (succ x0)))) as proof of (((eq fofType) (succ (succ X0))) (succ (succ x0))) % 80.23/80.72 Found ((eq_sym00 (succ (succ X0))) ((eq_ref fofType) (succ (succ x0)))) as proof of (((eq fofType) (succ (succ X0))) (succ (succ x0))) % 80.23/80.72 Found (((eq_sym0 (succ (succ x0))) (succ (succ X0))) ((eq_ref fofType) (succ (succ x0)))) as proof of (((eq fofType) (succ (succ X0))) (succ (succ x0))) % 80.23/80.72 Found ((((eq_sym fofType) (succ (succ x0))) (succ (succ X0))) ((eq_ref fofType) (succ (succ x0)))) as proof of (((eq fofType) (succ (succ X0))) (succ (succ x0))) % 80.23/80.73 Found (fun (x1:(((eq fofType) (succ X0)) (succ (succ x0))))=> ((((eq_sym fofType) (succ (succ x0))) (succ (succ X0))) ((eq_ref fofType) (succ (succ x0))))) as proof of (((eq fofType) (succ (succ X0))) (succ (succ x0))) % 80.23/80.73 Found eq_ref00:=(eq_ref0 X0):(((eq fofType) X0) X0) % 80.23/80.73 Found (eq_ref0 X0) as proof of (((eq fofType) X0) x0) % 80.23/80.73 Found ((eq_ref fofType) X0) as proof of (((eq fofType) X0) x0) % 80.23/80.73 Found ((eq_ref fofType) X0) as proof of (((eq fofType) X0) x0) % 80.23/80.73 Found ((eq_ref fofType) X0) as proof of (((eq fofType) X0) x0) % 80.23/80.73 Found (eq_substitution00000 ((eq_ref fofType) X0)) as proof of (((eq fofType) (succ X0)) (succ x0)) % 80.23/80.73 Found ((eq_substitution0000 succ) ((eq_ref fofType) X0)) as proof of (((eq fofType) (succ X0)) (succ x0)) % 80.23/80.73 Found (((eq_substitution000 x0) succ) ((eq_ref fofType) X0)) as proof of (((eq fofType) (succ X0)) (succ x0)) % 80.23/80.73 Found ((((eq_substitution00 X0) x0) succ) ((eq_ref fofType) X0)) as proof of (((eq fofType) (succ X0)) (succ x0)) % 80.23/80.73 Found (((((eq_substitution0 fofType) X0) x0) succ) ((eq_ref fofType) X0)) as proof of (((eq fofType) (succ X0)) (succ x0)) % 98.85/99.33 Found ((((((eq_substitution fofType) fofType) X0) x0) succ) ((eq_ref fofType) X0)) as proof of (((eq fofType) (succ X0)) (succ x0)) % 98.85/99.33 Found (fun (x1:(((eq fofType) X0) (succ x0)))=> ((((((eq_substitution fofType) fofType) X0) x0) succ) ((eq_ref fofType) X0))) as proof of (((eq fofType) (succ X0)) (succ x0)) % 98.85/99.33 Found x1:(P (succ (succ x0))) % 98.85/99.33 Instantiate: x0:=X0:fofType % 98.85/99.33 Found x1 as proof of (P (succ (succ X0))) % 98.85/99.33 Found (fun (x2:(P (succ X0)))=> x1) as proof of (P (succ (succ X0))) % 98.85/99.33 Found eq_ref000:=(eq_ref00 P):((P one)->(P one)) % 98.85/99.33 Found (eq_ref00 P) as proof of (P0 one) % 98.85/99.33 Found ((eq_ref0 one) P) as proof of (P0 one) % 98.85/99.33 Found (((eq_ref fofType) one) P) as proof of (P0 one) % 98.85/99.33 Found (((eq_ref fofType) one) P) as proof of (P0 one) % 98.85/99.33 Found eq_ref00:=(eq_ref0 (f x0)):(((eq Prop) (f x0)) (f x0)) % 98.85/99.33 Found (eq_ref0 (f x0)) as proof of (((eq Prop) (f x0)) (((eq fofType) one) (succ x0))) % 98.85/99.33 Found ((eq_ref Prop) (f x0)) as proof of (((eq Prop) (f x0)) (((eq fofType) one) (succ x0))) % 98.85/99.33 Found ((eq_ref Prop) (f x0)) as proof of (((eq Prop) (f x0)) (((eq fofType) one) (succ x0))) % 98.85/99.33 Found (fun (x0:fofType)=> ((eq_ref Prop) (f x0))) as proof of (((eq Prop) (f x0)) (((eq fofType) one) (succ x0))) % 98.85/99.33 Found (fun (x0:fofType)=> ((eq_ref Prop) (f x0))) as proof of (forall (x:fofType), (((eq Prop) (f x)) (((eq fofType) one) (succ x)))) % 98.85/99.33 Found eq_ref00:=(eq_ref0 (f x0)):(((eq Prop) (f x0)) (f x0)) % 98.85/99.33 Found (eq_ref0 (f x0)) as proof of (((eq Prop) (f x0)) (((eq fofType) one) (succ x0))) % 98.85/99.33 Found ((eq_ref Prop) (f x0)) as proof of (((eq Prop) (f x0)) (((eq fofType) one) (succ x0))) % 98.85/99.33 Found ((eq_ref Prop) (f x0)) as proof of (((eq Prop) (f x0)) (((eq fofType) one) (succ x0))) % 98.85/99.33 Found (fun (x0:fofType)=> ((eq_ref Prop) (f x0))) as proof of (((eq Prop) (f x0)) (((eq fofType) one) (succ x0))) % 98.85/99.33 Found (fun (x0:fofType)=> ((eq_ref Prop) (f x0))) as proof of (forall (x:fofType), (((eq Prop) (f x)) (((eq fofType) one) (succ x)))) % 98.85/99.33 Found x1:(P (succ (succ x0))) % 98.85/99.33 Instantiate: x0:=X0:fofType % 98.85/99.33 Found x1 as proof of (P (succ (succ X0))) % 98.85/99.33 Found (fun (x2:(P (succ X0)))=> x1) as proof of (P (succ (succ X0))) % 98.85/99.33 Found eq_ref00:=(eq_ref0 (succ X)):(((eq fofType) (succ X)) (succ X)) % 98.85/99.33 Found (eq_ref0 (succ X)) as proof of (((eq fofType) (succ X)) b) % 98.85/99.33 Found ((eq_ref fofType) (succ X)) as proof of (((eq fofType) (succ X)) b) % 98.85/99.33 Found ((eq_ref fofType) (succ X)) as proof of (((eq fofType) (succ X)) b) % 98.85/99.33 Found ((eq_ref fofType) (succ X)) as proof of (((eq fofType) (succ X)) b) % 98.85/99.33 Found eq_ref00:=(eq_ref0 b):(((eq fofType) b) b) % 98.85/99.33 Found (eq_ref0 b) as proof of (((eq fofType) b) (succ (succ x0))) % 98.85/99.33 Found ((eq_ref fofType) b) as proof of (((eq fofType) b) (succ (succ x0))) % 98.85/99.33 Found ((eq_ref fofType) b) as proof of (((eq fofType) b) (succ (succ x0))) % 98.85/99.33 Found ((eq_ref fofType) b) as proof of (((eq fofType) b) (succ (succ x0))) % 98.85/99.33 Found x2:(P (succ (succ X0))) % 98.85/99.33 Instantiate: x0:=X0:fofType % 98.85/99.33 Found (fun (x2:(P (succ (succ X0))))=> x2) as proof of (P (succ (succ x0))) % 98.85/99.33 Found (fun (P:(fofType->Prop)) (x2:(P (succ (succ X0))))=> x2) as proof of ((P (succ (succ X0)))->(P (succ (succ x0)))) % 98.85/99.33 Found (fun (x1:(((eq fofType) (succ X0)) (succ (succ x0)))) (P:(fofType->Prop)) (x2:(P (succ (succ X0))))=> x2) as proof of (((eq fofType) (succ (succ X0))) (succ (succ x0))) % 98.85/99.33 Found eq_ref000:=(eq_ref00 P):((P (succ (succ X0)))->(P (succ (succ X0)))) % 98.85/99.33 Found (eq_ref00 P) as proof of ((P (succ (succ X0)))->(P (succ (succ x0)))) % 98.85/99.33 Found ((eq_ref0 (succ (succ X0))) P) as proof of ((P (succ (succ X0)))->(P (succ (succ x0)))) % 98.85/99.33 Found (((eq_ref fofType) (succ (succ X0))) P) as proof of ((P (succ (succ X0)))->(P (succ (succ x0)))) % 98.85/99.33 Found (((eq_ref fofType) (succ (succ X0))) P) as proof of ((P (succ (succ X0)))->(P (succ (succ x0)))) % 98.85/99.33 Found (fun (P:(fofType->Prop))=> (((eq_ref fofType) (succ (succ X0))) P)) as proof of ((P (succ (succ X0)))->(P (succ (succ x0)))) % 98.85/99.33 Found (fun (x1:(((eq fofType) (succ X0)) (succ (succ x0)))) (P:(fofType->Prop))=> (((eq_ref fofType) (succ (succ X0))) P)) as proof of (((eq fofType) (succ (succ X0))) (succ (succ x0))) % 98.85/99.33 Found x1:(P (succ x0)) % 98.85/99.33 Instantiate: x0:=X0:fofType % 98.85/99.33 Found x1 as proof of (P (succ X0)) % 98.85/99.33 Found (fun (x2:(P X0))=> x1) as proof of (P (succ X0)) % 114.34/114.81 Found eq_ref00:=(eq_ref0 (succ (succ X0))):(((eq fofType) (succ (succ X0))) (succ (succ X0))) % 114.34/114.81 Found (eq_ref0 (succ (succ X0))) as proof of (((eq fofType) (succ (succ X0))) (succ (succ x0))) % 114.34/114.81 Found ((eq_ref fofType) (succ (succ X0))) as proof of (((eq fofType) (succ (succ X0))) (succ (succ x0))) % 114.34/114.81 Found ((eq_ref fofType) (succ (succ X0))) as proof of (((eq fofType) (succ (succ X0))) (succ (succ x0))) % 114.34/114.81 Found ((eq_ref fofType) (succ (succ X0))) as proof of (((eq fofType) (succ (succ X0))) (succ (succ x0))) % 114.34/114.81 Found (succ_injective__eq_sym00 ((eq_ref fofType) (succ (succ X0)))) as proof of (((eq fofType) (succ x0)) (succ X0)) % 114.34/114.81 Found ((succ_injective__eq_sym0 (succ x0)) ((eq_ref fofType) (succ (succ X0)))) as proof of (((eq fofType) (succ x0)) (succ X0)) % 114.34/114.81 Found (((succ_injective__eq_sym (succ X0)) (succ x0)) ((eq_ref fofType) (succ (succ X0)))) as proof of (((eq fofType) (succ x0)) (succ X0)) % 114.34/114.81 Found (fun (x1:(((eq fofType) (succ x0)) X0))=> (((succ_injective__eq_sym (succ X0)) (succ x0)) ((eq_ref fofType) (succ (succ X0))))) as proof of (((eq fofType) (succ x0)) (succ X0)) % 114.34/114.81 Found eq_ref00:=(eq_ref0 (succ X0)):(((eq fofType) (succ X0)) (succ X0)) % 114.34/114.81 Found (eq_ref0 (succ X0)) as proof of (((eq fofType) (succ X0)) (succ x0)) % 114.34/114.81 Found ((eq_ref fofType) (succ X0)) as proof of (((eq fofType) (succ X0)) (succ x0)) % 114.34/114.81 Found ((eq_ref fofType) (succ X0)) as proof of (((eq fofType) (succ X0)) (succ x0)) % 114.34/114.81 Found ((eq_ref fofType) (succ X0)) as proof of (((eq fofType) (succ X0)) (succ x0)) % 114.34/114.81 Found (eq_sym010 ((eq_ref fofType) (succ X0))) as proof of (((eq fofType) (succ x0)) (succ X0)) % 114.34/114.81 Found ((eq_sym01 (succ x0)) ((eq_ref fofType) (succ X0))) as proof of (((eq fofType) (succ x0)) (succ X0)) % 114.34/114.81 Found (((eq_sym0 (succ X0)) (succ x0)) ((eq_ref fofType) (succ X0))) as proof of (((eq fofType) (succ x0)) (succ X0)) % 114.34/114.81 Found (fun (x1:(((eq fofType) (succ x0)) X0))=> (((eq_sym0 (succ X0)) (succ x0)) ((eq_ref fofType) (succ X0)))) as proof of (((eq fofType) (succ x0)) (succ X0)) % 114.34/114.81 Found eq_substitution00000:=(eq_substitution0000 succ):((((eq fofType) (succ X0)) (succ (succ X0)))->(((eq fofType) (succ (succ X0))) (succ (succ (succ X0))))) % 114.34/114.81 Found (eq_substitution0000 succ) as proof of ((((eq fofType) (succ X0)) (succ (succ X0)))->(((eq fofType) (succ (succ X0))) (succ (succ (succ X0))))) % 114.34/114.81 Found ((eq_substitution000 (succ (succ X0))) succ) as proof of ((((eq fofType) (succ X0)) (succ (succ X0)))->(((eq fofType) (succ (succ X0))) (succ (succ (succ X0))))) % 114.34/114.81 Found (((eq_substitution00 (succ X0)) (succ (succ X0))) succ) as proof of ((((eq fofType) (succ X0)) (succ (succ X0)))->(((eq fofType) (succ (succ X0))) (succ (succ (succ X0))))) % 114.34/114.81 Found ((((eq_substitution0 fofType) (succ X0)) (succ (succ X0))) succ) as proof of ((((eq fofType) (succ X0)) (succ (succ X0)))->(((eq fofType) (succ (succ X0))) (succ (succ (succ X0))))) % 114.34/114.81 Found (((((eq_substitution fofType) fofType) (succ X0)) (succ (succ X0))) succ) as proof of ((((eq fofType) (succ X0)) (succ (succ X0)))->(((eq fofType) (succ (succ X0))) (succ (succ (succ X0))))) % 114.34/114.81 Found (fun (X0:fofType)=> (((((eq_substitution fofType) fofType) (succ X0)) (succ (succ X0))) succ)) as proof of ((((eq fofType) (succ X0)) (succ (succ X0)))->(((eq fofType) (succ (succ X0))) (succ (succ (succ X0))))) % 114.34/114.81 Found (fun (X0:fofType)=> (((((eq_substitution fofType) fofType) (succ X0)) (succ (succ X0))) succ)) as proof of (forall (X:fofType), ((((eq fofType) (succ X)) (succ (succ X)))->(((eq fofType) (succ (succ X))) (succ (succ (succ X)))))) % 114.34/114.81 Found x1:(P (succ (succ x0))) % 114.34/114.81 Instantiate: x0:=X0:fofType % 114.34/114.81 Found x1 as proof of (P (succ (succ X0))) % 114.34/114.81 Found (fun (x2:(P (succ X0)))=> x1) as proof of (P (succ (succ X0))) % 114.34/114.81 Found x1:(P (succ (succ x0))) % 114.34/114.81 Instantiate: x0:=X0:fofType % 114.34/114.81 Found x1 as proof of (P (succ (succ X0))) % 114.34/114.81 Found (fun (x2:(P (succ X0)))=> x1) as proof of (P (succ (succ X0))) % 114.34/114.81 Found x1:(P (succ (succ x0))) % 114.34/114.81 Instantiate: x0:=X0:fofType % 114.34/114.81 Found x1 as proof of (P (succ (succ X0))) % 114.34/114.81 Found (fun (x2:(P (succ X0)))=> x1) as proof of (P (succ (succ X0))) % 114.34/114.81 Found x1:(P (succ (succ x0))) % 114.34/114.81 Instantiate: x0:=X0:fofType % 114.34/114.81 Found x1 as proof of (P (succ (succ X0))) % 147.88/148.40 Found (fun (x2:(P (succ X0)))=> x1) as proof of (P (succ (succ X0))) % 147.88/148.40 Found x1:(P (succ (succ x0))) % 147.88/148.40 Instantiate: x0:=X0:fofType % 147.88/148.40 Found x1 as proof of (P (succ (succ X0))) % 147.88/148.40 Found (fun (x2:(P (succ X0)))=> x1) as proof of (P (succ (succ X0))) % 147.88/148.40 Found x1:(P (succ (succ x0))) % 147.88/148.40 Instantiate: x0:=X0:fofType % 147.88/148.40 Found x1 as proof of (P (succ (succ X0))) % 147.88/148.40 Found (fun (x2:(P (succ X0)))=> x1) as proof of (P (succ (succ X0))) % 147.88/148.40 Found eq_substitution00000:=(eq_substitution0000 succ):((((eq fofType) (succ X0)) (succ (succ X0)))->(((eq fofType) (succ (succ X0))) (succ (succ (succ X0))))) % 147.88/148.40 Found (eq_substitution0000 succ) as proof of ((((eq fofType) (succ X0)) (succ (succ X0)))->(((eq fofType) (succ (succ X0))) (succ (succ (succ X0))))) % 147.88/148.40 Found ((eq_substitution000 (succ (succ X0))) succ) as proof of ((((eq fofType) (succ X0)) (succ (succ X0)))->(((eq fofType) (succ (succ X0))) (succ (succ (succ X0))))) % 147.88/148.40 Found (((eq_substitution00 (succ X0)) (succ (succ X0))) succ) as proof of ((((eq fofType) (succ X0)) (succ (succ X0)))->(((eq fofType) (succ (succ X0))) (succ (succ (succ X0))))) % 147.88/148.40 Found ((((eq_substitution0 fofType) (succ X0)) (succ (succ X0))) succ) as proof of ((((eq fofType) (succ X0)) (succ (succ X0)))->(((eq fofType) (succ (succ X0))) (succ (succ (succ X0))))) % 147.88/148.40 Found (((((eq_substitution fofType) fofType) (succ X0)) (succ (succ X0))) succ) as proof of ((((eq fofType) (succ X0)) (succ (succ X0)))->(((eq fofType) (succ (succ X0))) (succ (succ (succ X0))))) % 147.88/148.40 Found (fun (X0:fofType)=> (((((eq_substitution fofType) fofType) (succ X0)) (succ (succ X0))) succ)) as proof of ((((eq fofType) (succ X0)) (succ (succ X0)))->(((eq fofType) (succ (succ X0))) (succ (succ (succ X0))))) % 147.88/148.40 Found (fun (X0:fofType)=> (((((eq_substitution fofType) fofType) (succ X0)) (succ (succ X0))) succ)) as proof of (forall (X:fofType), ((((eq fofType) (succ X)) (succ (succ X)))->(((eq fofType) (succ (succ X))) (succ (succ (succ X)))))) % 147.88/148.40 Found eq_ref00:=(eq_ref0 (succ one)):(((eq fofType) (succ one)) (succ one)) % 147.88/148.40 Found (eq_ref0 (succ one)) as proof of (((eq fofType) (succ one)) (succ x0)) % 147.88/148.40 Found ((eq_ref fofType) (succ one)) as proof of (((eq fofType) (succ one)) (succ x0)) % 147.88/148.40 Found ((eq_ref fofType) (succ one)) as proof of (((eq fofType) (succ one)) (succ x0)) % 147.88/148.40 Found ((eq_ref fofType) (succ one)) as proof of (((eq fofType) (succ one)) (succ x0)) % 147.88/148.40 Found eq_ref000:=(eq_ref00 P):((P one)->(P one)) % 147.88/148.40 Found (eq_ref00 P) as proof of (P0 one) % 147.88/148.40 Found ((eq_ref0 one) P) as proof of (P0 one) % 147.88/148.40 Found (((eq_ref fofType) one) P) as proof of (P0 one) % 147.88/148.40 Found (((eq_ref fofType) one) P) as proof of (P0 one) % 147.88/148.40 Found x1:(P (succ x0)) % 147.88/148.40 Instantiate: x0:=X0:fofType % 147.88/148.40 Found x1 as proof of (P (succ X0)) % 147.88/148.40 Found (fun (x2:(P X0))=> x1) as proof of (P (succ X0)) % 147.88/148.40 Found eq_ref000:=(eq_ref00 P):((P (succ (succ x0)))->(P (succ (succ x0)))) % 147.88/148.40 Found (eq_ref00 P) as proof of (P0 (succ (succ x0))) % 147.88/148.40 Found ((eq_ref0 (succ (succ x0))) P) as proof of (P0 (succ (succ x0))) % 147.88/148.40 Found (((eq_ref fofType) (succ (succ x0))) P) as proof of (P0 (succ (succ x0))) % 147.88/148.40 Found (((eq_ref fofType) (succ (succ x0))) P) as proof of (P0 (succ (succ x0))) % 147.88/148.40 Found eq_ref000:=(eq_ref00 P):((P (succ (succ x0)))->(P (succ (succ x0)))) % 147.88/148.40 Found (eq_ref00 P) as proof of (P0 (succ (succ x0))) % 147.88/148.40 Found ((eq_ref0 (succ (succ x0))) P) as proof of (P0 (succ (succ x0))) % 147.88/148.40 Found (((eq_ref fofType) (succ (succ x0))) P) as proof of (P0 (succ (succ x0))) % 147.88/148.40 Found (((eq_ref fofType) (succ (succ x0))) P) as proof of (P0 (succ (succ x0))) % 147.88/148.40 Found eq_ref000:=(eq_ref00 P):((P (succ (succ x0)))->(P (succ (succ x0)))) % 147.88/148.40 Found (eq_ref00 P) as proof of (P0 (succ (succ x0))) % 147.88/148.40 Found ((eq_ref0 (succ (succ x0))) P) as proof of (P0 (succ (succ x0))) % 147.88/148.40 Found (((eq_ref fofType) (succ (succ x0))) P) as proof of (P0 (succ (succ x0))) % 147.88/148.40 Found (((eq_ref fofType) (succ (succ x0))) P) as proof of (P0 (succ (succ x0))) % 147.88/148.40 Found eq_ref000:=(eq_ref00 P):((P (succ X))->(P (succ X))) % 147.88/148.40 Found (eq_ref00 P) as proof of (P0 (succ X)) % 147.88/148.40 Found ((eq_ref0 (succ X)) P) as proof of (P0 (succ X)) % 147.88/148.40 Found (((eq_ref fofType) (succ X)) P) as proof of (P0 (succ X)) % 147.88/148.40 Found (((eq_ref fofType) (succ X)) P) as proof of (P0 (succ X)) % 147.88/148.40 Found eq_ref00:=(eq_ref0 (succ x0)):(((eq fofType) (succ x0)) (succ x0)) % 172.83/173.35 Found (eq_ref0 (succ x0)) as proof of (((eq fofType) (succ x0)) b) % 172.83/173.35 Found ((eq_ref fofType) (succ x0)) as proof of (((eq fofType) (succ x0)) b) % 172.83/173.35 Found ((eq_ref fofType) (succ x0)) as proof of (((eq fofType) (succ x0)) b) % 172.83/173.35 Found ((eq_ref fofType) (succ x0)) as proof of (((eq fofType) (succ x0)) b) % 172.83/173.35 Found eq_ref00:=(eq_ref0 b):(((eq fofType) b) b) % 172.83/173.35 Found (eq_ref0 b) as proof of (((eq fofType) b) X) % 172.83/173.35 Found ((eq_ref fofType) b) as proof of (((eq fofType) b) X) % 172.83/173.35 Found ((eq_ref fofType) b) as proof of (((eq fofType) b) X) % 172.83/173.35 Found ((eq_ref fofType) b) as proof of (((eq fofType) b) X) % 172.83/173.35 Found x1:(((eq fofType) (succ X0)) (succ (succ x0))) % 172.83/173.35 Instantiate: x0:=X0:fofType % 172.83/173.35 Found x1 as proof of (((eq fofType) (succ X0)) (succ (succ X0))) % 172.83/173.35 Found (eq_sym000 x1) as proof of (((eq fofType) (succ (succ X0))) (succ X0)) % 172.83/173.35 Found ((eq_sym00 (succ (succ X0))) x1) as proof of (((eq fofType) (succ (succ X0))) (succ X0)) % 172.83/173.35 Found (((eq_sym0 (succ X0)) (succ (succ X0))) x1) as proof of (((eq fofType) (succ (succ X0))) (succ X0)) % 172.83/173.35 Found ((((eq_sym fofType) (succ X0)) (succ (succ X0))) x1) as proof of (((eq fofType) (succ (succ X0))) (succ X0)) % 172.83/173.35 Found ((((eq_sym fofType) (succ X0)) (succ (succ X0))) x1) as proof of (((eq fofType) (succ (succ X0))) (succ X0)) % 172.83/173.35 Found (x10 ((((eq_sym fofType) (succ X0)) (succ (succ X0))) x1)) as proof of (((eq fofType) (succ (succ X0))) (succ (succ x0))) % 172.83/173.35 Found ((x1 ((eq fofType) (succ (succ X0)))) ((((eq_sym fofType) (succ X0)) (succ (succ X0))) x1)) as proof of (((eq fofType) (succ (succ X0))) (succ (succ x0))) % 172.83/173.35 Found (fun (x1:(((eq fofType) (succ X0)) (succ (succ x0))))=> ((x1 ((eq fofType) (succ (succ X0)))) ((((eq_sym fofType) (succ X0)) (succ (succ X0))) x1))) as proof of (((eq fofType) (succ (succ X0))) (succ (succ x0))) % 172.83/173.35 Found eq_ref00:=(eq_ref0 (succ (succ X1))):(((eq fofType) (succ (succ X1))) (succ (succ X1))) % 172.83/173.35 Found (eq_ref0 (succ (succ X1))) as proof of (((eq fofType) (succ (succ X1))) (succ x0)) % 172.83/173.35 Found ((eq_ref fofType) (succ (succ X1))) as proof of (((eq fofType) (succ (succ X1))) (succ x0)) % 172.83/173.35 Found ((eq_ref fofType) (succ (succ X1))) as proof of (((eq fofType) (succ (succ X1))) (succ x0)) % 172.83/173.35 Found (fun (x2:(((eq fofType) (succ X1)) (succ x0)))=> ((eq_ref fofType) (succ (succ X1)))) as proof of (((eq fofType) (succ (succ X1))) (succ x0)) % 172.83/173.35 Found x1:(((eq fofType) X0) (succ x0)) % 172.83/173.35 Found x1 as proof of (((eq fofType) X0) (succ x0)) % 172.83/173.35 Found eq_ref00:=(eq_ref0 (succ X0)):(((eq fofType) (succ X0)) (succ X0)) % 172.83/173.35 Found (eq_ref0 (succ X0)) as proof of (((eq fofType) (succ X0)) (succ x0)) % 172.83/173.35 Found ((eq_ref fofType) (succ X0)) as proof of (((eq fofType) (succ X0)) (succ x0)) % 172.83/173.35 Found ((eq_ref fofType) (succ X0)) as proof of (((eq fofType) (succ X0)) (succ x0)) % 172.83/173.35 Found ((eq_ref fofType) (succ X0)) as proof of (((eq fofType) (succ X0)) (succ x0)) % 172.83/173.35 Found (eq_substitution00000 ((eq_ref fofType) (succ X0))) as proof of (((eq fofType) (succ (succ X0))) (succ (succ x0))) % 172.83/173.35 Found ((eq_substitution0000 succ) ((eq_ref fofType) (succ X0))) as proof of (((eq fofType) (succ (succ X0))) (succ (succ x0))) % 172.83/173.35 Found (((eq_substitution000 (succ x0)) succ) ((eq_ref fofType) (succ X0))) as proof of (((eq fofType) (succ (succ X0))) (succ (succ x0))) % 172.83/173.35 Found ((((eq_substitution00 (succ X0)) (succ x0)) succ) ((eq_ref fofType) (succ X0))) as proof of (((eq fofType) (succ (succ X0))) (succ (succ x0))) % 172.83/173.35 Found (((((eq_substitution0 fofType) (succ X0)) (succ x0)) succ) ((eq_ref fofType) (succ X0))) as proof of (((eq fofType) (succ (succ X0))) (succ (succ x0))) % 172.83/173.35 Found ((((((eq_substitution fofType) fofType) (succ X0)) (succ x0)) succ) ((eq_ref fofType) (succ X0))) as proof of (((eq fofType) (succ (succ X0))) (succ (succ x0))) % 172.83/173.35 Found (fun (x1:(((eq fofType) (succ X0)) (succ (succ x0))))=> ((((((eq_substitution fofType) fofType) (succ X0)) (succ x0)) succ) ((eq_ref fofType) (succ X0)))) as proof of (((eq fofType) (succ (succ X0))) (succ (succ x0))) % 172.83/173.35 Found eq_ref00:=(eq_ref0 (succ (succ (succ X0)))):(((eq fofType) (succ (succ (succ X0)))) (succ (succ (succ X0)))) % 172.83/173.35 Found (eq_ref0 (succ (succ (succ X0)))) as proof of (((eq fofType) (succ (succ (succ X0)))) (succ (succ (succ x0)))) % 205.55/206.11 Found ((eq_ref fofType) (succ (succ (succ X0)))) as proof of (((eq fofType) (succ (succ (succ X0)))) (succ (succ (succ x0)))) % 205.55/206.11 Found ((eq_ref fofType) (succ (succ (succ X0)))) as proof of (((eq fofType) (succ (succ (succ X0)))) (succ (succ (succ x0)))) % 205.55/206.11 Found (fun (x1:(((eq fofType) (succ (succ X0))) (succ (succ (succ x0)))))=> ((eq_ref fofType) (succ (succ (succ X0))))) as proof of (((eq fofType) (succ (succ (succ X0)))) (succ (succ (succ x0)))) % 205.55/206.11 Found x1:(P (succ (succ x0))) % 205.55/206.11 Instantiate: x0:=X0:fofType % 205.55/206.11 Found x1 as proof of (P (succ (succ X0))) % 205.55/206.11 Found (fun (x2:(P (succ X0)))=> x1) as proof of (P (succ (succ X0))) % 205.55/206.11 Found eq_ref00:=(eq_ref0 (succ (succ (succ X0)))):(((eq fofType) (succ (succ (succ X0)))) (succ (succ (succ X0)))) % 205.55/206.11 Found (eq_ref0 (succ (succ (succ X0)))) as proof of (((eq fofType) (succ (succ (succ X0)))) (succ (succ (succ x0)))) % 205.55/206.11 Found ((eq_ref fofType) (succ (succ (succ X0)))) as proof of (((eq fofType) (succ (succ (succ X0)))) (succ (succ (succ x0)))) % 205.55/206.11 Found ((eq_ref fofType) (succ (succ (succ X0)))) as proof of (((eq fofType) (succ (succ (succ X0)))) (succ (succ (succ x0)))) % 205.55/206.11 Found (fun (x1:(((eq fofType) (succ (succ X0))) (succ (succ (succ x0)))))=> ((eq_ref fofType) (succ (succ (succ X0))))) as proof of (((eq fofType) (succ (succ (succ X0)))) (succ (succ (succ x0)))) % 205.55/206.11 Found x1:(P (succ (succ x0))) % 205.55/206.11 Instantiate: x0:=X0:fofType % 205.55/206.11 Found x1 as proof of (P (succ (succ X0))) % 205.55/206.11 Found (fun (x2:(P (succ X0)))=> x1) as proof of (P (succ (succ X0))) % 205.55/206.11 Found eq_ref00:=(eq_ref0 (succ (succ X0))):(((eq fofType) (succ (succ X0))) (succ (succ X0))) % 205.55/206.11 Found (eq_ref0 (succ (succ X0))) as proof of (((eq fofType) (succ (succ X0))) (succ (succ x0))) % 205.55/206.11 Found ((eq_ref fofType) (succ (succ X0))) as proof of (((eq fofType) (succ (succ X0))) (succ (succ x0))) % 205.55/206.11 Found ((eq_ref fofType) (succ (succ X0))) as proof of (((eq fofType) (succ (succ X0))) (succ (succ x0))) % 205.55/206.11 Found (fun (x1:(((eq fofType) (succ X0)) (succ (succ x0))))=> ((eq_ref fofType) (succ (succ X0)))) as proof of (((eq fofType) (succ (succ X0))) (succ (succ x0))) % 205.55/206.11 Found eq_ref00:=(eq_ref0 (succ (succ (succ X0)))):(((eq fofType) (succ (succ (succ X0)))) (succ (succ (succ X0)))) % 205.55/206.11 Found (eq_ref0 (succ (succ (succ X0)))) as proof of (((eq fofType) (succ (succ (succ X0)))) (succ (succ (succ x0)))) % 205.55/206.11 Found ((eq_ref fofType) (succ (succ (succ X0)))) as proof of (((eq fofType) (succ (succ (succ X0)))) (succ (succ (succ x0)))) % 205.55/206.11 Found ((eq_ref fofType) (succ (succ (succ X0)))) as proof of (((eq fofType) (succ (succ (succ X0)))) (succ (succ (succ x0)))) % 205.55/206.11 Found (fun (x1:(((eq fofType) (succ (succ X0))) (succ (succ (succ x0)))))=> ((eq_ref fofType) (succ (succ (succ X0))))) as proof of (((eq fofType) (succ (succ (succ X0)))) (succ (succ (succ x0)))) % 205.55/206.11 Found eq_ref000:=(eq_ref00 P):((P (succ X))->(P (succ X))) % 205.55/206.11 Found (eq_ref00 P) as proof of (P0 (succ X)) % 205.55/206.11 Found ((eq_ref0 (succ X)) P) as proof of (P0 (succ X)) % 205.55/206.11 Found (((eq_ref fofType) (succ X)) P) as proof of (P0 (succ X)) % 205.55/206.11 Found (((eq_ref fofType) (succ X)) P) as proof of (P0 (succ X)) % 205.55/206.11 Found eq_ref000:=(eq_ref00 P):((P (succ X))->(P (succ X))) % 205.55/206.11 Found (eq_ref00 P) as proof of (P0 (succ X)) % 205.55/206.11 Found ((eq_ref0 (succ X)) P) as proof of (P0 (succ X)) % 205.55/206.11 Found (((eq_ref fofType) (succ X)) P) as proof of (P0 (succ X)) % 205.55/206.11 Found (((eq_ref fofType) (succ X)) P) as proof of (P0 (succ X)) % 205.55/206.11 Found eq_ref00:=(eq_ref0 (succ (succ x0))):(((eq fofType) (succ (succ x0))) (succ (succ x0))) % 205.55/206.11 Found (eq_ref0 (succ (succ x0))) as proof of (((eq fofType) (succ (succ x0))) (succ (succ X))) % 205.55/206.11 Found ((eq_ref fofType) (succ (succ x0))) as proof of (((eq fofType) (succ (succ x0))) (succ (succ X))) % 205.55/206.11 Found ((eq_ref fofType) (succ (succ x0))) as proof of (((eq fofType) (succ (succ x0))) (succ (succ X))) % 205.55/206.11 Found ((eq_ref fofType) (succ (succ x0))) as proof of (((eq fofType) (succ (succ x0))) (succ (succ X))) % 205.55/206.11 Found eq_ref000:=(eq_ref00 P):((P (succ (succ X1)))->(P (succ (succ X1)))) % 205.55/206.11 Found (eq_ref00 P) as proof of ((P (succ (succ X1)))->(P (succ x0))) % 205.55/206.11 Found ((eq_ref0 (succ (succ X1))) P) as proof of ((P (succ (succ X1)))->(P (succ x0))) % 205.55/206.11 Found (((eq_ref fofType) (succ (succ X1))) P) as proof of ((P (succ (succ X1)))->(P (succ x0))) % 241.83/242.39 Found (((eq_ref fofType) (succ (succ X1))) P) as proof of ((P (succ (succ X1)))->(P (succ x0))) % 241.83/242.39 Found (fun (P:(fofType->Prop))=> (((eq_ref fofType) (succ (succ X1))) P)) as proof of ((P (succ (succ X1)))->(P (succ x0))) % 241.83/242.39 Found (fun (x2:(((eq fofType) (succ X1)) (succ x0))) (P:(fofType->Prop))=> (((eq_ref fofType) (succ (succ X1))) P)) as proof of (((eq fofType) (succ (succ X1))) (succ x0)) % 241.83/242.39 Found x10:=(x1 (fun (x3:fofType)=> (P (succ (succ X1))))):((P (succ (succ X1)))->(P (succ (succ X1)))) % 241.83/242.39 Found (x1 (fun (x3:fofType)=> (P (succ (succ X1))))) as proof of ((P (succ (succ X1)))->(P (succ x0))) % 241.83/242.39 Found (x1 (fun (x3:fofType)=> (P (succ (succ X1))))) as proof of ((P (succ (succ X1)))->(P (succ x0))) % 241.83/242.39 Found (fun (P:(fofType->Prop))=> (x1 (fun (x3:fofType)=> (P (succ (succ X1)))))) as proof of ((P (succ (succ X1)))->(P (succ x0))) % 241.83/242.39 Found (fun (x2:(((eq fofType) (succ X1)) (succ x0))) (P:(fofType->Prop))=> (x1 (fun (x3:fofType)=> (P (succ (succ X1)))))) as proof of (((eq fofType) (succ (succ X1))) (succ x0)) % 241.83/242.39 Found x3:(P (succ (succ X1))) % 241.83/242.39 Instantiate: x0:=(succ X1):fofType % 241.83/242.39 Found (fun (x3:(P (succ (succ X1))))=> x3) as proof of (P (succ x0)) % 241.83/242.39 Found (fun (P:(fofType->Prop)) (x3:(P (succ (succ X1))))=> x3) as proof of ((P (succ (succ X1)))->(P (succ x0))) % 241.83/242.39 Found (fun (x2:(((eq fofType) (succ X1)) (succ x0))) (P:(fofType->Prop)) (x3:(P (succ (succ X1))))=> x3) as proof of (((eq fofType) (succ (succ X1))) (succ x0)) % 241.83/242.39 Found eq_ref00:=(eq_ref0 one):(((eq fofType) one) one) % 241.83/242.39 Found (eq_ref0 one) as proof of (((eq fofType) one) b) % 241.83/242.39 Found ((eq_ref fofType) one) as proof of (((eq fofType) one) b) % 241.83/242.39 Found ((eq_ref fofType) one) as proof of (((eq fofType) one) b) % 241.83/242.39 Found ((eq_ref fofType) one) as proof of (((eq fofType) one) b) % 241.83/242.39 Found eq_ref00:=(eq_ref0 b):(((eq fofType) b) b) % 241.83/242.39 Found (eq_ref0 b) as proof of (((eq fofType) b) (succ x0)) % 241.83/242.39 Found ((eq_ref fofType) b) as proof of (((eq fofType) b) (succ x0)) % 241.83/242.39 Found ((eq_ref fofType) b) as proof of (((eq fofType) b) (succ x0)) % 241.83/242.39 Found ((eq_ref fofType) b) as proof of (((eq fofType) b) (succ x0)) % 241.83/242.39 Found eq_ref00:=(eq_ref0 (succ X0)):(((eq fofType) (succ X0)) (succ X0)) % 241.83/242.39 Found (eq_ref0 (succ X0)) as proof of (((eq fofType) (succ X0)) (succ x0)) % 241.83/242.39 Found ((eq_ref fofType) (succ X0)) as proof of (((eq fofType) (succ X0)) (succ x0)) % 241.83/242.39 Found ((eq_ref fofType) (succ X0)) as proof of (((eq fofType) (succ X0)) (succ x0)) % 241.83/242.39 Found (eq_substitution00000 ((eq_ref fofType) (succ X0))) as proof of (((eq fofType) (succ (succ X0))) (succ (succ x0))) % 241.83/242.39 Found (eq_substitution00000 ((eq_ref fofType) (succ X0))) as proof of (((eq fofType) (succ (succ X0))) (succ (succ x0))) % 241.83/242.39 Found ((eq_substitution0000 (fun (x5:fofType)=> (succ (succ X0)))) ((eq_ref fofType) (succ X0))) as proof of (((eq fofType) (succ (succ X0))) (succ (succ x0))) % 241.83/242.39 Found (((eq_substitution000 (succ x0)) (fun (x5:fofType)=> (succ (succ X0)))) ((eq_ref fofType) (succ X0))) as proof of (((eq fofType) (succ (succ X0))) (succ (succ x0))) % 241.83/242.39 Found ((((eq_substitution00 (succ X0)) (succ x0)) (fun (x5:fofType)=> (succ (succ X0)))) ((eq_ref fofType) (succ X0))) as proof of (((eq fofType) (succ (succ X0))) (succ (succ x0))) % 241.83/242.39 Found (((((eq_substitution0 fofType) (succ X0)) (succ x0)) (fun (x5:fofType)=> (succ (succ X0)))) ((eq_ref fofType) (succ X0))) as proof of (((eq fofType) (succ (succ X0))) (succ (succ x0))) % 241.83/242.39 Found ((((((eq_substitution fofType) fofType) (succ X0)) (succ x0)) (fun (x5:fofType)=> (succ (succ X0)))) ((eq_ref fofType) (succ X0))) as proof of (((eq fofType) (succ (succ X0))) (succ (succ x0))) % 241.83/242.39 Found (fun (x1:(((eq fofType) (succ X0)) (succ (succ x0))))=> ((((((eq_substitution fofType) fofType) (succ X0)) (succ x0)) (fun (x5:fofType)=> (succ (succ X0)))) ((eq_ref fofType) (succ X0)))) as proof of (((eq fofType) (succ (succ X0))) (succ (succ x0))) % 241.83/242.39 Found eq_ref00:=(eq_ref0 (succ (succ x0))):(((eq fofType) (succ (succ x0))) (succ (succ x0))) % 241.83/242.39 Found (eq_ref0 (succ (succ x0))) as proof of (((eq fofType) (succ (succ x0))) (succ (succ X0))) % 241.83/242.39 Found ((eq_ref fofType) (succ (succ x0))) as proof of (((eq fofType) (succ (succ x0))) (succ (succ X0))) % 241.83/242.39 Found ((eq_ref fofType) (succ (succ x0))) as proof of (((eq fofType) (succ (succ x0))) (succ (succ X0))) % 250.20/250.73 Found (fun (x1:(((eq fofType) (succ (succ x0))) (succ X0)))=> ((eq_ref fofType) (succ (succ x0)))) as proof of (((eq fofType) (succ (succ x0))) (succ (succ X0))) % 250.20/250.73 Found eq_ref00:=(eq_ref0 (succ (succ (succ x0)))):(((eq fofType) (succ (succ (succ x0)))) (succ (succ (succ x0)))) % 250.20/250.73 Found (eq_ref0 (succ (succ (succ x0)))) as proof of (((eq fofType) (succ (succ (succ x0)))) (succ (succ (succ X0)))) % 250.20/250.73 Found ((eq_ref fofType) (succ (succ (succ x0)))) as proof of (((eq fofType) (succ (succ (succ x0)))) (succ (succ (succ X0)))) % 250.20/250.73 Found ((eq_ref fofType) (succ (succ (succ x0)))) as proof of (((eq fofType) (succ (succ (succ x0)))) (succ (succ (succ X0)))) % 250.20/250.73 Found (fun (x1:(((eq fofType) (succ (succ (succ x0)))) (succ (succ X0))))=> ((eq_ref fofType) (succ (succ (succ x0))))) as proof of (((eq fofType) (succ (succ (succ x0)))) (succ (succ (succ X0)))) % 250.20/250.73 Found eq_ref000:=(eq_ref00 P):((P (succ (succ (succ X0))))->(P (succ (succ (succ X0))))) % 250.20/250.73 Found (eq_ref00 P) as proof of ((P (succ (succ (succ X0))))->(P (succ (succ (succ x0))))) % 250.20/250.73 Found ((eq_ref0 (succ (succ (succ X0)))) P) as proof of ((P (succ (succ (succ X0))))->(P (succ (succ (succ x0))))) % 250.20/250.73 Found (((eq_ref fofType) (succ (succ (succ X0)))) P) as proof of ((P (succ (succ (succ X0))))->(P (succ (succ (succ x0))))) % 250.20/250.73 Found (((eq_ref fofType) (succ (succ (succ X0)))) P) as proof of ((P (succ (succ (succ X0))))->(P (succ (succ (succ x0))))) % 250.20/250.73 Found (fun (P:(fofType->Prop))=> (((eq_ref fofType) (succ (succ (succ X0)))) P)) as proof of ((P (succ (succ (succ X0))))->(P (succ (succ (succ x0))))) % 250.20/250.73 Found (fun (x1:(((eq fofType) (succ (succ X0))) (succ (succ (succ x0))))) (P:(fofType->Prop))=> (((eq_ref fofType) (succ (succ (succ X0)))) P)) as proof of (((eq fofType) (succ (succ (succ X0)))) (succ (succ (succ x0)))) % 250.20/250.73 Found x2:(P (succ (succ (succ X0)))) % 250.20/250.73 Instantiate: x0:=X0:fofType % 250.20/250.73 Found (fun (x2:(P (succ (succ (succ X0)))))=> x2) as proof of (P (succ (succ (succ x0)))) % 250.20/250.73 Found (fun (P:(fofType->Prop)) (x2:(P (succ (succ (succ X0)))))=> x2) as proof of ((P (succ (succ (succ X0))))->(P (succ (succ (succ x0))))) % 250.20/250.73 Found (fun (x1:(((eq fofType) (succ (succ X0))) (succ (succ (succ x0))))) (P:(fofType->Prop)) (x2:(P (succ (succ (succ X0)))))=> x2) as proof of (((eq fofType) (succ (succ (succ X0)))) (succ (succ (succ x0)))) % 250.20/250.73 Found eq_ref000:=(eq_ref00 P):((P (succ (succ (succ X0))))->(P (succ (succ (succ X0))))) % 250.20/250.73 Found (eq_ref00 P) as proof of ((P (succ (succ (succ X0))))->(P (succ (succ (succ x0))))) % 250.20/250.73 Found ((eq_ref0 (succ (succ (succ X0)))) P) as proof of ((P (succ (succ (succ X0))))->(P (succ (succ (succ x0))))) % 250.20/250.73 Found (((eq_ref fofType) (succ (succ (succ X0)))) P) as proof of ((P (succ (succ (succ X0))))->(P (succ (succ (succ x0))))) % 250.20/250.73 Found (((eq_ref fofType) (succ (succ (succ X0)))) P) as proof of ((P (succ (succ (succ X0))))->(P (succ (succ (succ x0))))) % 250.20/250.73 Found (fun (P:(fofType->Prop))=> (((eq_ref fofType) (succ (succ (succ X0)))) P)) as proof of ((P (succ (succ (succ X0))))->(P (succ (succ (succ x0))))) % 250.20/250.73 Found (fun (x1:(((eq fofType) (succ (succ X0))) (succ (succ (succ x0))))) (P:(fofType->Prop))=> (((eq_ref fofType) (succ (succ (succ X0)))) P)) as proof of (((eq fofType) (succ (succ (succ X0)))) (succ (succ (succ x0)))) % 250.20/250.73 Found x2:(P (succ (succ (succ X0)))) % 250.20/250.73 Instantiate: x0:=X0:fofType % 250.20/250.73 Found (fun (x2:(P (succ (succ (succ X0)))))=> x2) as proof of (P (succ (succ (succ x0)))) % 250.20/250.73 Found (fun (P:(fofType->Prop)) (x2:(P (succ (succ (succ X0)))))=> x2) as proof of ((P (succ (succ (succ X0))))->(P (succ (succ (succ x0))))) % 250.20/250.73 Found (fun (x1:(((eq fofType) (succ (succ X0))) (succ (succ (succ x0))))) (P:(fofType->Prop)) (x2:(P (succ (succ (succ X0)))))=> x2) as proof of (((eq fofType) (succ (succ (succ X0)))) (succ (succ (succ x0)))) % 250.20/250.73 Found eq_ref000:=(eq_ref00 P):((P (succ (succ x0)))->(P (succ (succ x0)))) % 250.20/250.73 Found (eq_ref00 P) as proof of (P0 (succ (succ x0))) % 250.20/250.73 Found ((eq_ref0 (succ (succ x0))) P) as proof of (P0 (succ (succ x0))) % 250.20/250.73 Found (((eq_ref fofType) (succ (succ x0))) P) as proof of (P0 (succ (succ x0))) % 250.20/250.73 Found (((eq_ref fofType) (succ (succ x0))) P) as proof of (P0 (succ (succ x0))) % 253.01/253.55 Found eq_ref000:=(eq_ref00 P):((P (succ (succ x0)))->(P (succ (succ x0)))) % 253.01/253.55 Found (eq_ref00 P) as proof of (P0 (succ x0)) % 253.01/253.55 Found ((eq_ref0 (succ (succ x0))) P) as proof of (P0 (succ x0)) % 253.01/253.55 Found (((eq_ref fofType) (succ (succ x0))) P) as proof of (P0 (succ x0)) % 253.01/253.55 Found (((eq_ref fofType) (succ (succ x0))) P) as proof of (P0 (succ x0)) % 253.01/253.55 Found eq_ref000:=(eq_ref00 P):((P (succ (succ x0)))->(P (succ (succ x0)))) % 253.01/253.55 Found (eq_ref00 P) as proof of (P0 (succ (succ x0))) % 253.01/253.55 Found ((eq_ref0 (succ (succ x0))) P) as proof of (P0 (succ (succ x0))) % 253.01/253.55 Found (((eq_ref fofType) (succ (succ x0))) P) as proof of (P0 (succ (succ x0))) % 253.01/253.55 Found (((eq_ref fofType) (succ (succ x0))) P) as proof of (P0 (succ (succ x0))) % 253.01/253.55 Found eq_ref00:=(eq_ref0 (succ (succ (succ X0)))):(((eq fofType) (succ (succ (succ X0)))) (succ (succ (succ X0)))) % 253.01/253.55 Found (eq_ref0 (succ (succ (succ X0)))) as proof of (((eq fofType) (succ (succ (succ X0)))) (succ (succ (succ x0)))) % 253.01/253.55 Found ((eq_ref fofType) (succ (succ (succ X0)))) as proof of (((eq fofType) (succ (succ (succ X0)))) (succ (succ (succ x0)))) % 253.01/253.55 Found ((eq_ref fofType) (succ (succ (succ X0)))) as proof of (((eq fofType) (succ (succ (succ X0)))) (succ (succ (succ x0)))) % 253.01/253.55 Found ((eq_ref fofType) (succ (succ (succ X0)))) as proof of (((eq fofType) (succ (succ (succ X0)))) (succ (succ (succ x0)))) % 253.01/253.55 Found (succ_injective__eq_sym00 ((eq_ref fofType) (succ (succ (succ X0))))) as proof of (((eq fofType) (succ (succ x0))) (succ (succ X0))) % 253.01/253.55 Found ((succ_injective__eq_sym0 (succ (succ x0))) ((eq_ref fofType) (succ (succ (succ X0))))) as proof of (((eq fofType) (succ (succ x0))) (succ (succ X0))) % 253.01/253.55 Found (((succ_injective__eq_sym (succ (succ X0))) (succ (succ x0))) ((eq_ref fofType) (succ (succ (succ X0))))) as proof of (((eq fofType) (succ (succ x0))) (succ (succ X0))) % 253.01/253.55 Found (fun (x1:(((eq fofType) (succ (succ x0))) (succ X0)))=> (((succ_injective__eq_sym (succ (succ X0))) (succ (succ x0))) ((eq_ref fofType) (succ (succ (succ X0)))))) as proof of (((eq fofType) (succ (succ x0))) (succ (succ X0))) % 253.01/253.55 Found eq_ref00:=(eq_ref0 (succ (succ X0))):(((eq fofType) (succ (succ X0))) (succ (succ X0))) % 253.01/253.55 Found (eq_ref0 (succ (succ X0))) as proof of (((eq fofType) (succ (succ X0))) (succ (succ x0))) % 253.01/253.55 Found ((eq_ref fofType) (succ (succ X0))) as proof of (((eq fofType) (succ (succ X0))) (succ (succ x0))) % 253.01/253.55 Found ((eq_ref fofType) (succ (succ X0))) as proof of (((eq fofType) (succ (succ X0))) (succ (succ x0))) % 253.01/253.55 Found ((eq_ref fofType) (succ (succ X0))) as proof of (((eq fofType) (succ (succ X0))) (succ (succ x0))) % 253.01/253.55 Found (eq_sym010 ((eq_ref fofType) (succ (succ X0)))) as proof of (((eq fofType) (succ (succ x0))) (succ (succ X0))) % 253.01/253.55 Found ((eq_sym01 (succ (succ x0))) ((eq_ref fofType) (succ (succ X0)))) as proof of (((eq fofType) (succ (succ x0))) (succ (succ X0))) % 253.01/253.55 Found (((eq_sym0 (succ (succ X0))) (succ (succ x0))) ((eq_ref fofType) (succ (succ X0)))) as proof of (((eq fofType) (succ (succ x0))) (succ (succ X0))) % 253.01/253.55 Found (fun (x1:(((eq fofType) (succ (succ x0))) (succ X0)))=> (((eq_sym0 (succ (succ X0))) (succ (succ x0))) ((eq_ref fofType) (succ (succ X0))))) as proof of (((eq fofType) (succ (succ x0))) (succ (succ X0))) % 253.01/253.55 Found x2:(P (succ (succ X0))) % 253.01/253.55 Instantiate: x0:=X0:fofType % 253.01/253.55 Found (fun (x2:(P (succ (succ X0))))=> x2) as proof of (P (succ (succ x0))) % 253.01/253.55 Found (fun (P:(fofType->Prop)) (x2:(P (succ (succ X0))))=> x2) as proof of ((P (succ (succ X0)))->(P (succ (succ x0)))) % 253.01/253.55 Found (fun (x1:(((eq fofType) (succ X0)) (succ (succ x0)))) (P:(fofType->Prop)) (x2:(P (succ (succ X0))))=> x2) as proof of (((eq fofType) (succ (succ X0))) (succ (succ x0))) % 253.01/253.55 Found eq_ref000:=(eq_ref00 P):((P (succ (succ (succ X0))))->(P (succ (succ (succ X0))))) % 253.01/253.55 Found (eq_ref00 P) as proof of ((P (succ (succ (succ X0))))->(P (succ (succ (succ x0))))) % 253.01/253.55 Found ((eq_ref0 (succ (succ (succ X0)))) P) as proof of ((P (succ (succ (succ X0))))->(P (succ (succ (succ x0))))) % 253.01/253.55 Found (((eq_ref fofType) (succ (succ (succ X0)))) P) as proof of ((P (succ (succ (succ X0))))->(P (succ (succ (succ x0))))) % 253.01/253.55 Found (((eq_ref fofType) (succ (succ (succ X0)))) P) as proof of ((P (succ (succ (succ X0))))->(P (succ (succ (succ x0))))) % 257.43/257.96 Found (fun (P:(fofType->Prop))=> (((eq_ref fofType) (succ (succ (succ X0)))) P)) as proof of ((P (succ (succ (succ X0))))->(P (succ (succ (succ x0))))) % 257.43/257.96 Found (fun (x1:(((eq fofType) (succ (succ X0))) (succ (succ (succ x0))))) (P:(fofType->Prop))=> (((eq_ref fofType) (succ (succ (succ X0)))) P)) as proof of (((eq fofType) (succ (succ (succ X0)))) (succ (succ (succ x0)))) % 257.43/257.96 Found x2:(P (succ (succ (succ X0)))) % 257.43/257.96 Instantiate: x0:=X0:fofType % 257.43/257.96 Found (fun (x2:(P (succ (succ (succ X0)))))=> x2) as proof of (P (succ (succ (succ x0)))) % 257.43/257.96 Found (fun (P:(fofType->Prop)) (x2:(P (succ (succ (succ X0)))))=> x2) as proof of ((P (succ (succ (succ X0))))->(P (succ (succ (succ x0))))) % 257.43/257.96 Found (fun (x1:(((eq fofType) (succ (succ X0))) (succ (succ (succ x0))))) (P:(fofType->Prop)) (x2:(P (succ (succ (succ X0)))))=> x2) as proof of (((eq fofType) (succ (succ (succ X0)))) (succ (succ (succ x0)))) % 257.43/257.96 Found eq_ref00:=(eq_ref0 (succ X0)):(((eq fofType) (succ X0)) (succ X0)) % 257.43/257.96 Found (eq_ref0 (succ X0)) as proof of (((eq fofType) (succ X0)) (succ x0)) % 257.43/257.96 Found ((eq_ref fofType) (succ X0)) as proof of (((eq fofType) (succ X0)) (succ x0)) % 257.43/257.96 Found ((eq_ref fofType) (succ X0)) as proof of (((eq fofType) (succ X0)) (succ x0)) % 257.43/257.96 Found ((eq_ref fofType) (succ X0)) as proof of (((eq fofType) (succ X0)) (succ x0)) % 257.43/257.96 Found (eq_substitution00000 ((eq_ref fofType) (succ X0))) as proof of (((eq fofType) (succ (succ X0))) (succ (succ x0))) % 257.43/257.96 Found ((eq_substitution0000 succ) ((eq_ref fofType) (succ X0))) as proof of (((eq fofType) (succ (succ X0))) (succ (succ x0))) % 257.43/257.96 Found (((eq_substitution000 (succ x0)) succ) ((eq_ref fofType) (succ X0))) as proof of (((eq fofType) (succ (succ X0))) (succ (succ x0))) % 257.43/257.96 Found ((((eq_substitution00 (succ X0)) (succ x0)) succ) ((eq_ref fofType) (succ X0))) as proof of (((eq fofType) (succ (succ X0))) (succ (succ x0))) % 257.43/257.96 Found (((((eq_substitution0 fofType) (succ X0)) (succ x0)) succ) ((eq_ref fofType) (succ X0))) as proof of (((eq fofType) (succ (succ X0))) (succ (succ x0))) % 257.43/257.96 Found ((((((eq_substitution fofType) fofType) (succ X0)) (succ x0)) succ) ((eq_ref fofType) (succ X0))) as proof of (((eq fofType) (succ (succ X0))) (succ (succ x0))) % 257.43/257.96 Found (fun (x1:(((eq fofType) (succ X0)) (succ (succ x0))))=> ((((((eq_substitution fofType) fofType) (succ X0)) (succ x0)) succ) ((eq_ref fofType) (succ X0)))) as proof of (((eq fofType) (succ (succ X0))) (succ (succ x0))) % 257.43/257.96 Found eq_ref000:=(eq_ref00 P):((P (succ (succ X0)))->(P (succ (succ X0)))) % 257.43/257.96 Found (eq_ref00 P) as proof of ((P (succ (succ X0)))->(P (succ (succ x0)))) % 257.43/257.96 Found ((eq_ref0 (succ (succ X0))) P) as proof of ((P (succ (succ X0)))->(P (succ (succ x0)))) % 257.43/257.96 Found (((eq_ref fofType) (succ (succ X0))) P) as proof of ((P (succ (succ X0)))->(P (succ (succ x0)))) % 257.43/257.96 Found (((eq_ref fofType) (succ (succ X0))) P) as proof of ((P (succ (succ X0)))->(P (succ (succ x0)))) % 257.43/257.96 Found (fun (P:(fofType->Prop))=> (((eq_ref fofType) (succ (succ X0))) P)) as proof of ((P (succ (succ X0)))->(P (succ (succ x0)))) % 257.43/257.96 Found (fun (x1:(((eq fofType) (succ X0)) (succ (succ x0)))) (P:(fofType->Prop))=> (((eq_ref fofType) (succ (succ X0))) P)) as proof of (((eq fofType) (succ (succ X0))) (succ (succ x0))) % 257.43/257.96 Found eq_ref00:=(eq_ref0 (succ (succ x0))):(((eq fofType) (succ (succ x0))) (succ (succ x0))) % 257.43/257.96 Found (eq_ref0 (succ (succ x0))) as proof of (((eq fofType) (succ (succ x0))) b) % 257.43/257.96 Found ((eq_ref fofType) (succ (succ x0))) as proof of (((eq fofType) (succ (succ x0))) b) % 257.43/257.96 Found ((eq_ref fofType) (succ (succ x0))) as proof of (((eq fofType) (succ (succ x0))) b) % 257.43/257.96 Found ((eq_ref fofType) (succ (succ x0))) as proof of (((eq fofType) (succ (succ x0))) b) % 257.43/257.96 Found eq_ref00:=(eq_ref0 b):(((eq fofType) b) b) % 257.43/257.96 Found (eq_ref0 b) as proof of (((eq fofType) b) (succ X)) % 257.43/257.96 Found ((eq_ref fofType) b) as proof of (((eq fofType) b) (succ X)) % 257.43/257.96 Found ((eq_ref fofType) b) as proof of (((eq fofType) b) (succ X)) % 257.43/257.96 Found ((eq_ref fofType) b) as proof of (((eq fofType) b) (succ X)) % 257.43/257.96 Found eq_ref00:=(eq_ref0 (succ (succ (succ X0)))):(((eq fofType) (succ (succ (succ X0)))) (succ (succ (succ X0)))) % 257.43/257.96 Found (eq_ref0 (succ (succ (succ X0)))) as proof of (((eq fofType) (succ (succ (succ X0)))) (succ (succ (succ x0)))) % 263.09/263.63 Found ((eq_ref fofType) (succ (succ (succ X0)))) as proof of (((eq fofType) (succ (succ (succ X0)))) (succ (succ (succ x0)))) % 263.09/263.63 Found ((eq_ref fofType) (succ (succ (succ X0)))) as proof of (((eq fofType) (succ (succ (succ X0)))) (succ (succ (succ x0)))) % 263.09/263.63 Found ((eq_ref fofType) (succ (succ (succ X0)))) as proof of (((eq fofType) (succ (succ (succ X0)))) (succ (succ (succ x0)))) % 263.09/263.63 Found (succ_injective__eq_sym00 ((eq_ref fofType) (succ (succ (succ X0))))) as proof of (((eq fofType) (succ (succ x0))) (succ (succ X0))) % 263.09/263.63 Found ((succ_injective__eq_sym0 (succ (succ x0))) ((eq_ref fofType) (succ (succ (succ X0))))) as proof of (((eq fofType) (succ (succ x0))) (succ (succ X0))) % 263.09/263.63 Found (((succ_injective__eq_sym (succ (succ X0))) (succ (succ x0))) ((eq_ref fofType) (succ (succ (succ X0))))) as proof of (((eq fofType) (succ (succ x0))) (succ (succ X0))) % 263.09/263.63 Found (fun (x1:(((eq fofType) (succ (succ x0))) (succ X0)))=> (((succ_injective__eq_sym (succ (succ X0))) (succ (succ x0))) ((eq_ref fofType) (succ (succ (succ X0)))))) as proof of (((eq fofType) (succ (succ x0))) (succ (succ X0))) % 263.09/263.63 Found eq_ref00:=(eq_ref0 (succ (succ X0))):(((eq fofType) (succ (succ X0))) (succ (succ X0))) % 263.09/263.63 Found (eq_ref0 (succ (succ X0))) as proof of (((eq fofType) (succ (succ X0))) (succ (succ x0))) % 263.09/263.63 Found ((eq_ref fofType) (succ (succ X0))) as proof of (((eq fofType) (succ (succ X0))) (succ (succ x0))) % 263.09/263.63 Found ((eq_ref fofType) (succ (succ X0))) as proof of (((eq fofType) (succ (succ X0))) (succ (succ x0))) % 263.09/263.63 Found ((eq_ref fofType) (succ (succ X0))) as proof of (((eq fofType) (succ (succ X0))) (succ (succ x0))) % 263.09/263.63 Found (eq_sym010 ((eq_ref fofType) (succ (succ X0)))) as proof of (((eq fofType) (succ (succ x0))) (succ (succ X0))) % 263.09/263.63 Found ((eq_sym01 (succ (succ x0))) ((eq_ref fofType) (succ (succ X0)))) as proof of (((eq fofType) (succ (succ x0))) (succ (succ X0))) % 263.09/263.63 Found (((eq_sym0 (succ (succ X0))) (succ (succ x0))) ((eq_ref fofType) (succ (succ X0)))) as proof of (((eq fofType) (succ (succ x0))) (succ (succ X0))) % 263.09/263.63 Found (fun (x1:(((eq fofType) (succ (succ x0))) (succ X0)))=> (((eq_sym0 (succ (succ X0))) (succ (succ x0))) ((eq_ref fofType) (succ (succ X0))))) as proof of (((eq fofType) (succ (succ x0))) (succ (succ X0))) % 263.09/263.63 Found eq_ref000:=(eq_ref00 P):((P (succ one))->(P (succ one))) % 263.09/263.63 Found (eq_ref00 P) as proof of (P0 (succ one)) % 263.09/263.63 Found ((eq_ref0 (succ one)) P) as proof of (P0 (succ one)) % 263.09/263.63 Found (((eq_ref fofType) (succ one)) P) as proof of (P0 (succ one)) % 263.09/263.63 Found (((eq_ref fofType) (succ one)) P) as proof of (P0 (succ one)) % 263.09/263.63 Found eq_ref00:=(eq_ref0 (succ (succ x0))):(((eq fofType) (succ (succ x0))) (succ (succ x0))) % 263.09/263.63 Found (eq_ref0 (succ (succ x0))) as proof of (((eq fofType) (succ (succ x0))) b) % 263.09/263.63 Found ((eq_ref fofType) (succ (succ x0))) as proof of (((eq fofType) (succ (succ x0))) b) % 263.09/263.63 Found ((eq_ref fofType) (succ (succ x0))) as proof of (((eq fofType) (succ (succ x0))) b) % 263.09/263.63 Found ((eq_ref fofType) (succ (succ x0))) as proof of (((eq fofType) (succ (succ x0))) b) % 263.09/263.63 Found eq_ref00:=(eq_ref0 b):(((eq fofType) b) b) % 263.09/263.63 Found (eq_ref0 b) as proof of (((eq fofType) b) (succ X)) % 263.09/263.63 Found ((eq_ref fofType) b) as proof of (((eq fofType) b) (succ X)) % 263.09/263.63 Found ((eq_ref fofType) b) as proof of (((eq fofType) b) (succ X)) % 263.09/263.63 Found ((eq_ref fofType) b) as proof of (((eq fofType) b) (succ X)) % 263.09/263.63 Found eq_ref00:=(eq_ref0 (succ (succ (succ X0)))):(((eq fofType) (succ (succ (succ X0)))) (succ (succ (succ X0)))) % 263.09/263.63 Found (eq_ref0 (succ (succ (succ X0)))) as proof of (((eq fofType) (succ (succ (succ X0)))) (succ (succ (succ x0)))) % 263.09/263.63 Found ((eq_ref fofType) (succ (succ (succ X0)))) as proof of (((eq fofType) (succ (succ (succ X0)))) (succ (succ (succ x0)))) % 263.09/263.63 Found ((eq_ref fofType) (succ (succ (succ X0)))) as proof of (((eq fofType) (succ (succ (succ X0)))) (succ (succ (succ x0)))) % 263.09/263.63 Found ((eq_ref fofType) (succ (succ (succ X0)))) as proof of (((eq fofType) (succ (succ (succ X0)))) (succ (succ (succ x0)))) % 263.09/263.63 Found (succ_injective00 ((eq_ref fofType) (succ (succ (succ X0))))) as proof of (((eq fofType) (succ (succ X0))) (succ (succ x0))) % 263.09/263.63 Found ((succ_injective0 (succ (succ x0))) ( %------------------------------------------------------------------------------