%------------------------------------------------------------------------------ % File : cocATP---0.2.0 % Problem : NUM830^5 : TPTP v7.0.0. Bugfixed v5.3.0. % Transfm : none % Format : tptp:raw % Command : python CASC.py /export/starexec/sandbox/benchmark/theBenchmark.p % Computer : n078.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:51 EST 2018 % Result : Timeout 297.99s % 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 : NUM830^5 : TPTP v7.0.0. Bugfixed v5.3.0. % 0.00/0.03 % Command : python CASC.py /export/starexec/sandbox/benchmark/theBenchmark.p % 0.02/0.23 % Computer : n078.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 14:41:19 CST 2018 % 0.02/0.23 % CPUTime : % 0.02/0.27 Python 2.7.13 % 2.82/3.21 Using paths ['/home/cristobal/cocATP/CASC/TPTP/', '/export/starexec/sandbox/benchmark/', '/export/starexec/sandbox/benchmark/'] % 2.82/3.21 FOF formula (<kernel.Constant object at 0x2b8936660878>, <kernel.Type object at 0x2b8936660128>) of role type named n_type % 2.82/3.21 Using role type % 2.82/3.21 Declaring n:Type % 2.82/3.21 FOF formula (<kernel.Constant object at 0x2b8936655710>, <kernel.Constant object at 0x2b8936660560>) of role type named c0_type % 2.82/3.21 Using role type % 2.82/3.21 Declaring c0:n % 2.82/3.21 FOF formula (<kernel.Constant object at 0x2b8936660b48>, <kernel.DependentProduct object at 0x2b8935be5f38>) of role type named cS_type % 2.82/3.21 Using role type % 2.82/3.21 Declaring cS:(n->n) % 2.82/3.21 FOF formula (<kernel.Constant object at 0x2b8936660b90>, <kernel.DependentProduct object at 0x2b8935beaf80>) of role type named c_plus_type % 2.82/3.21 Using role type % 2.82/3.21 Declaring c_plus:(n->(n->n)) % 2.82/3.21 FOF formula (<kernel.Constant object at 0x2b8935beae18>, <kernel.DependentProduct object at 0x2b8936660b48>) of role type named c_star_type % 2.82/3.21 Using role type % 2.82/3.21 Declaring c_star:(n->(n->n)) % 2.82/3.21 FOF formula (<kernel.Constant object at 0x2b8935be5f38>, <kernel.Sort object at 0x2b892e2a7a70>) of role type named cPA_1_type % 2.82/3.21 Using role type % 2.82/3.21 Declaring cPA_1:Prop % 2.82/3.21 FOF formula (<kernel.Constant object at 0x2b8935be5f38>, <kernel.Sort object at 0x2b892e2a7a70>) of role type named cPA_2_type % 2.82/3.21 Using role type % 2.82/3.21 Declaring cPA_2:Prop % 2.82/3.21 FOF formula (<kernel.Constant object at 0x2b8936660bd8>, <kernel.Sort object at 0x2b892e2a7a70>) of role type named cPA_3_type % 2.82/3.21 Using role type % 2.82/3.21 Declaring cPA_3:Prop % 2.82/3.21 FOF formula (<kernel.Constant object at 0x2b89366604d0>, <kernel.Sort object at 0x2b892e2a7a70>) of role type named cPA_4_type % 2.82/3.21 Using role type % 2.82/3.21 Declaring cPA_4:Prop % 2.82/3.21 FOF formula (((eq Prop) cPA_1) (forall (Xx:n), (((eq n) ((c_plus Xx) c0)) Xx))) of role definition named cPA_1_def % 2.82/3.21 A new definition: (((eq Prop) cPA_1) (forall (Xx:n), (((eq n) ((c_plus Xx) c0)) Xx))) % 2.82/3.21 Defined: cPA_1:=(forall (Xx:n), (((eq n) ((c_plus Xx) c0)) Xx)) % 2.82/3.21 FOF formula (((eq Prop) cPA_2) (forall (Xx:n) (Xy:n), (((eq n) ((c_plus Xx) (cS Xy))) (cS ((c_plus Xx) Xy))))) of role definition named cPA_2_def % 2.82/3.21 A new definition: (((eq Prop) cPA_2) (forall (Xx:n) (Xy:n), (((eq n) ((c_plus Xx) (cS Xy))) (cS ((c_plus Xx) Xy))))) % 2.82/3.21 Defined: cPA_2:=(forall (Xx:n) (Xy:n), (((eq n) ((c_plus Xx) (cS Xy))) (cS ((c_plus Xx) Xy)))) % 2.82/3.21 FOF formula (((eq Prop) cPA_3) (forall (Xx:n), (((eq n) ((c_star Xx) c0)) c0))) of role definition named cPA_3_def % 2.82/3.21 A new definition: (((eq Prop) cPA_3) (forall (Xx:n), (((eq n) ((c_star Xx) c0)) c0))) % 2.82/3.21 Defined: cPA_3:=(forall (Xx:n), (((eq n) ((c_star Xx) c0)) c0)) % 2.82/3.21 FOF formula (((eq Prop) cPA_4) (forall (Xx:n) (Xy:n), (((eq n) ((c_star Xx) (cS Xy))) ((c_plus ((c_star Xx) Xy)) Xx)))) of role definition named cPA_4_def % 2.82/3.21 A new definition: (((eq Prop) cPA_4) (forall (Xx:n) (Xy:n), (((eq n) ((c_star Xx) (cS Xy))) ((c_plus ((c_star Xx) Xy)) Xx)))) % 2.82/3.21 Defined: cPA_4:=(forall (Xx:n) (Xy:n), (((eq n) ((c_star Xx) (cS Xy))) ((c_plus ((c_star Xx) Xy)) Xx))) % 2.82/3.21 FOF formula (((and ((and ((and cPA_1) cPA_2)) cPA_3)) cPA_4)->(((eq n) ((c_star (cS (cS c0))) (cS (cS c0)))) ((c_plus (cS (cS c0))) (cS (cS c0))))) of role conjecture named cPA_THM1 % 2.82/3.21 Conjecture to prove = (((and ((and ((and cPA_1) cPA_2)) cPA_3)) cPA_4)->(((eq n) ((c_star (cS (cS c0))) (cS (cS c0)))) ((c_plus (cS (cS c0))) (cS (cS c0))))):Prop % 2.82/3.21 We need to prove ['(((and ((and ((and cPA_1) cPA_2)) cPA_3)) cPA_4)->(((eq n) ((c_star (cS (cS c0))) (cS (cS c0)))) ((c_plus (cS (cS c0))) (cS (cS c0)))))'] % 2.82/3.21 Parameter n:Type. % 2.82/3.21 Parameter c0:n. % 2.82/3.21 Parameter cS:(n->n). % 2.82/3.21 Parameter c_plus:(n->(n->n)). % 2.82/3.21 Parameter c_star:(n->(n->n)). % 2.82/3.21 Definition cPA_1:=(forall (Xx:n), (((eq n) ((c_plus Xx) c0)) Xx)):Prop. % 2.82/3.21 Definition cPA_2:=(forall (Xx:n) (Xy:n), (((eq n) ((c_plus Xx) (cS Xy))) (cS ((c_plus Xx) Xy)))):Prop. % 2.82/3.21 Definition cPA_3:=(forall (Xx:n), (((eq n) ((c_star Xx) c0)) c0)):Prop. % 2.82/3.21 Definition cPA_4:=(forall (Xx:n) (Xy:n), (((eq n) ((c_star Xx) (cS Xy))) ((c_plus ((c_star Xx) Xy)) Xx))):Prop. % 2.82/3.21 Trying to prove (((and ((and ((and cPA_1) cPA_2)) cPA_3)) cPA_4)->(((eq n) ((c_star (cS (cS c0))) (cS (cS c0)))) ((c_plus (cS (cS c0))) (cS (cS c0))))) % 2.82/3.21 Found x00:(P ((c_star (cS (cS c0))) (cS (cS c0)))) % 2.82/3.21 Found (fun (x00:(P ((c_star (cS (cS c0))) (cS (cS c0)))))=> x00) as proof of (P ((c_star (cS (cS c0))) (cS (cS c0)))) % 16.54/16.98 Found (fun (x00:(P ((c_star (cS (cS c0))) (cS (cS c0)))))=> x00) as proof of (P0 ((c_star (cS (cS c0))) (cS (cS c0)))) % 16.54/16.98 Found eq_ref00:=(eq_ref0 ((c_star (cS (cS c0))) (cS (cS c0)))):(((eq n) ((c_star (cS (cS c0))) (cS (cS c0)))) ((c_star (cS (cS c0))) (cS (cS c0)))) % 16.54/16.98 Found (eq_ref0 ((c_star (cS (cS c0))) (cS (cS c0)))) as proof of (((eq n) ((c_star (cS (cS c0))) (cS (cS c0)))) b) % 16.54/16.98 Found ((eq_ref n) ((c_star (cS (cS c0))) (cS (cS c0)))) as proof of (((eq n) ((c_star (cS (cS c0))) (cS (cS c0)))) b) % 16.54/16.98 Found ((eq_ref n) ((c_star (cS (cS c0))) (cS (cS c0)))) as proof of (((eq n) ((c_star (cS (cS c0))) (cS (cS c0)))) b) % 16.54/16.98 Found ((eq_ref n) ((c_star (cS (cS c0))) (cS (cS c0)))) as proof of (((eq n) ((c_star (cS (cS c0))) (cS (cS c0)))) b) % 16.54/16.98 Found eq_ref00:=(eq_ref0 b):(((eq n) b) b) % 16.54/16.98 Found (eq_ref0 b) as proof of (((eq n) b) ((c_plus (cS (cS c0))) (cS (cS c0)))) % 16.54/16.98 Found ((eq_ref n) b) as proof of (((eq n) b) ((c_plus (cS (cS c0))) (cS (cS c0)))) % 16.54/16.98 Found ((eq_ref n) b) as proof of (((eq n) b) ((c_plus (cS (cS c0))) (cS (cS c0)))) % 16.54/16.98 Found ((eq_ref n) b) as proof of (((eq n) b) ((c_plus (cS (cS c0))) (cS (cS c0)))) % 16.54/16.98 Found x20:(P ((c_star (cS (cS c0))) (cS (cS c0)))) % 16.54/16.98 Found (fun (x20:(P ((c_star (cS (cS c0))) (cS (cS c0)))))=> x20) as proof of (P ((c_star (cS (cS c0))) (cS (cS c0)))) % 16.54/16.98 Found (fun (x20:(P ((c_star (cS (cS c0))) (cS (cS c0)))))=> x20) as proof of (P0 ((c_star (cS (cS c0))) (cS (cS c0)))) % 16.54/16.98 Found eq_ref00:=(eq_ref0 ((c_star (cS (cS c0))) (cS (cS c0)))):(((eq n) ((c_star (cS (cS c0))) (cS (cS c0)))) ((c_star (cS (cS c0))) (cS (cS c0)))) % 16.54/16.98 Found (eq_ref0 ((c_star (cS (cS c0))) (cS (cS c0)))) as proof of (((eq n) ((c_star (cS (cS c0))) (cS (cS c0)))) b) % 16.54/16.98 Found ((eq_ref n) ((c_star (cS (cS c0))) (cS (cS c0)))) as proof of (((eq n) ((c_star (cS (cS c0))) (cS (cS c0)))) b) % 16.54/16.98 Found ((eq_ref n) ((c_star (cS (cS c0))) (cS (cS c0)))) as proof of (((eq n) ((c_star (cS (cS c0))) (cS (cS c0)))) b) % 16.54/16.98 Found ((eq_ref n) ((c_star (cS (cS c0))) (cS (cS c0)))) as proof of (((eq n) ((c_star (cS (cS c0))) (cS (cS c0)))) b) % 16.54/16.98 Found eq_ref00:=(eq_ref0 b):(((eq n) b) b) % 16.54/16.98 Found (eq_ref0 b) as proof of (((eq n) b) ((c_plus (cS (cS c0))) (cS (cS c0)))) % 16.54/16.98 Found ((eq_ref n) b) as proof of (((eq n) b) ((c_plus (cS (cS c0))) (cS (cS c0)))) % 16.54/16.98 Found ((eq_ref n) b) as proof of (((eq n) b) ((c_plus (cS (cS c0))) (cS (cS c0)))) % 16.54/16.98 Found ((eq_ref n) b) as proof of (((eq n) b) ((c_plus (cS (cS c0))) (cS (cS c0)))) % 16.54/16.98 Found eq_ref00:=(eq_ref0 b):(((eq n) b) b) % 16.54/16.98 Found (eq_ref0 b) as proof of (((eq n) b) ((c_star (cS (cS c0))) (cS (cS c0)))) % 16.54/16.98 Found ((eq_ref n) b) as proof of (((eq n) b) ((c_star (cS (cS c0))) (cS (cS c0)))) % 16.54/16.98 Found ((eq_ref n) b) as proof of (((eq n) b) ((c_star (cS (cS c0))) (cS (cS c0)))) % 16.54/16.98 Found ((eq_ref n) b) as proof of (((eq n) b) ((c_star (cS (cS c0))) (cS (cS c0)))) % 16.54/16.98 Found eq_ref00:=(eq_ref0 ((c_plus (cS (cS c0))) (cS (cS c0)))):(((eq n) ((c_plus (cS (cS c0))) (cS (cS c0)))) ((c_plus (cS (cS c0))) (cS (cS c0)))) % 16.54/16.98 Found (eq_ref0 ((c_plus (cS (cS c0))) (cS (cS c0)))) as proof of (((eq n) ((c_plus (cS (cS c0))) (cS (cS c0)))) b) % 16.54/16.98 Found ((eq_ref n) ((c_plus (cS (cS c0))) (cS (cS c0)))) as proof of (((eq n) ((c_plus (cS (cS c0))) (cS (cS c0)))) b) % 16.54/16.98 Found ((eq_ref n) ((c_plus (cS (cS c0))) (cS (cS c0)))) as proof of (((eq n) ((c_plus (cS (cS c0))) (cS (cS c0)))) b) % 16.54/16.98 Found ((eq_ref n) ((c_plus (cS (cS c0))) (cS (cS c0)))) as proof of (((eq n) ((c_plus (cS (cS c0))) (cS (cS c0)))) b) % 16.54/16.98 Found x40:(P ((c_star (cS (cS c0))) (cS (cS c0)))) % 16.54/16.98 Found (fun (x40:(P ((c_star (cS (cS c0))) (cS (cS c0)))))=> x40) as proof of (P ((c_star (cS (cS c0))) (cS (cS c0)))) % 16.54/16.98 Found (fun (x40:(P ((c_star (cS (cS c0))) (cS (cS c0)))))=> x40) as proof of (P0 ((c_star (cS (cS c0))) (cS (cS c0)))) % 16.54/16.98 Found eq_ref00:=(eq_ref0 b):(((eq n) b) b) % 16.54/16.98 Found (eq_ref0 b) as proof of (((eq n) b) ((c_plus (cS (cS c0))) (cS (cS c0)))) % 16.54/16.98 Found ((eq_ref n) b) as proof of (((eq n) b) ((c_plus (cS (cS c0))) (cS (cS c0)))) % 16.54/16.98 Found ((eq_ref n) b) as proof of (((eq n) b) ((c_plus (cS (cS c0))) (cS (cS c0)))) % 16.54/16.98 Found ((eq_ref n) b) as proof of (((eq n) b) ((c_plus (cS (cS c0))) (cS (cS c0)))) % 44.94/45.33 Found eq_ref00:=(eq_ref0 ((c_star (cS (cS c0))) (cS (cS c0)))):(((eq n) ((c_star (cS (cS c0))) (cS (cS c0)))) ((c_star (cS (cS c0))) (cS (cS c0)))) % 44.94/45.33 Found (eq_ref0 ((c_star (cS (cS c0))) (cS (cS c0)))) as proof of (((eq n) ((c_star (cS (cS c0))) (cS (cS c0)))) b) % 44.94/45.33 Found ((eq_ref n) ((c_star (cS (cS c0))) (cS (cS c0)))) as proof of (((eq n) ((c_star (cS (cS c0))) (cS (cS c0)))) b) % 44.94/45.33 Found ((eq_ref n) ((c_star (cS (cS c0))) (cS (cS c0)))) as proof of (((eq n) ((c_star (cS (cS c0))) (cS (cS c0)))) b) % 44.94/45.33 Found ((eq_ref n) ((c_star (cS (cS c0))) (cS (cS c0)))) as proof of (((eq n) ((c_star (cS (cS c0))) (cS (cS c0)))) b) % 44.94/45.33 Found eq_ref00:=(eq_ref0 ((c_plus (cS (cS c0))) (cS (cS c0)))):(((eq n) ((c_plus (cS (cS c0))) (cS (cS c0)))) ((c_plus (cS (cS c0))) (cS (cS c0)))) % 44.94/45.33 Found (eq_ref0 ((c_plus (cS (cS c0))) (cS (cS c0)))) as proof of (((eq n) ((c_plus (cS (cS c0))) (cS (cS c0)))) b) % 44.94/45.33 Found ((eq_ref n) ((c_plus (cS (cS c0))) (cS (cS c0)))) as proof of (((eq n) ((c_plus (cS (cS c0))) (cS (cS c0)))) b) % 44.94/45.33 Found ((eq_ref n) ((c_plus (cS (cS c0))) (cS (cS c0)))) as proof of (((eq n) ((c_plus (cS (cS c0))) (cS (cS c0)))) b) % 44.94/45.33 Found ((eq_ref n) ((c_plus (cS (cS c0))) (cS (cS c0)))) as proof of (((eq n) ((c_plus (cS (cS c0))) (cS (cS c0)))) b) % 44.94/45.33 Found eq_ref00:=(eq_ref0 b):(((eq n) b) b) % 44.94/45.33 Found (eq_ref0 b) as proof of (((eq n) b) ((c_star (cS (cS c0))) (cS (cS c0)))) % 44.94/45.33 Found ((eq_ref n) b) as proof of (((eq n) b) ((c_star (cS (cS c0))) (cS (cS c0)))) % 44.94/45.33 Found ((eq_ref n) b) as proof of (((eq n) b) ((c_star (cS (cS c0))) (cS (cS c0)))) % 44.94/45.33 Found ((eq_ref n) b) as proof of (((eq n) b) ((c_star (cS (cS c0))) (cS (cS c0)))) % 44.94/45.33 Found eq_ref00:=(eq_ref0 b):(((eq n) b) b) % 44.94/45.33 Found (eq_ref0 b) as proof of (((eq n) b) ((c_star (cS (cS c0))) (cS (cS c0)))) % 44.94/45.33 Found ((eq_ref n) b) as proof of (((eq n) b) ((c_star (cS (cS c0))) (cS (cS c0)))) % 44.94/45.33 Found ((eq_ref n) b) as proof of (((eq n) b) ((c_star (cS (cS c0))) (cS (cS c0)))) % 44.94/45.33 Found ((eq_ref n) b) as proof of (((eq n) b) ((c_star (cS (cS c0))) (cS (cS c0)))) % 44.94/45.33 Found eq_ref00:=(eq_ref0 ((c_plus (cS (cS c0))) (cS (cS c0)))):(((eq n) ((c_plus (cS (cS c0))) (cS (cS c0)))) ((c_plus (cS (cS c0))) (cS (cS c0)))) % 44.94/45.33 Found (eq_ref0 ((c_plus (cS (cS c0))) (cS (cS c0)))) as proof of (((eq n) ((c_plus (cS (cS c0))) (cS (cS c0)))) b) % 44.94/45.33 Found ((eq_ref n) ((c_plus (cS (cS c0))) (cS (cS c0)))) as proof of (((eq n) ((c_plus (cS (cS c0))) (cS (cS c0)))) b) % 44.94/45.33 Found ((eq_ref n) ((c_plus (cS (cS c0))) (cS (cS c0)))) as proof of (((eq n) ((c_plus (cS (cS c0))) (cS (cS c0)))) b) % 44.94/45.33 Found ((eq_ref n) ((c_plus (cS (cS c0))) (cS (cS c0)))) as proof of (((eq n) ((c_plus (cS (cS c0))) (cS (cS c0)))) b) % 44.94/45.33 Found x60:(P ((c_star (cS (cS c0))) (cS (cS c0)))) % 44.94/45.33 Found (fun (x60:(P ((c_star (cS (cS c0))) (cS (cS c0)))))=> x60) as proof of (P ((c_star (cS (cS c0))) (cS (cS c0)))) % 44.94/45.33 Found (fun (x60:(P ((c_star (cS (cS c0))) (cS (cS c0)))))=> x60) as proof of (P0 ((c_star (cS (cS c0))) (cS (cS c0)))) % 44.94/45.33 Found eq_ref00:=(eq_ref0 b):(((eq n) b) b) % 44.94/45.33 Found (eq_ref0 b) as proof of (((eq n) b) ((c_plus (cS (cS c0))) (cS (cS c0)))) % 44.94/45.33 Found ((eq_ref n) b) as proof of (((eq n) b) ((c_plus (cS (cS c0))) (cS (cS c0)))) % 44.94/45.33 Found ((eq_ref n) b) as proof of (((eq n) b) ((c_plus (cS (cS c0))) (cS (cS c0)))) % 44.94/45.33 Found ((eq_ref n) b) as proof of (((eq n) b) ((c_plus (cS (cS c0))) (cS (cS c0)))) % 44.94/45.33 Found x100:=(x10 (cS c0)):(((eq n) ((c_star (cS (cS c0))) (cS (cS c0)))) ((c_plus ((c_star (cS (cS c0))) (cS c0))) (cS (cS c0)))) % 44.94/45.33 Found (x10 (cS c0)) as proof of (((eq n) ((c_star (cS (cS c0))) (cS (cS c0)))) b) % 44.94/45.33 Found ((x1 (cS (cS c0))) (cS c0)) as proof of (((eq n) ((c_star (cS (cS c0))) (cS (cS c0)))) b) % 44.94/45.33 Found ((x1 (cS (cS c0))) (cS c0)) as proof of (((eq n) ((c_star (cS (cS c0))) (cS (cS c0)))) b) % 44.94/45.33 Found ((x1 (cS (cS c0))) (cS c0)) as proof of (((eq n) ((c_star (cS (cS c0))) (cS (cS c0)))) b) % 44.94/45.33 Found eq_ref00:=(eq_ref0 b):(((eq n) b) b) % 44.94/45.33 Found (eq_ref0 b) as proof of (((eq n) b) ((c_star (cS (cS c0))) (cS (cS c0)))) % 44.94/45.33 Found ((eq_ref n) b) as proof of (((eq n) b) ((c_star (cS (cS c0))) (cS (cS c0)))) % 44.94/45.33 Found ((eq_ref n) b) as proof of (((eq n) b) ((c_star (cS (cS c0))) (cS (cS c0)))) % 69.40/69.78 Found ((eq_ref n) b) as proof of (((eq n) b) ((c_star (cS (cS c0))) (cS (cS c0)))) % 69.40/69.78 Found eq_ref00:=(eq_ref0 ((c_plus (cS (cS c0))) (cS (cS c0)))):(((eq n) ((c_plus (cS (cS c0))) (cS (cS c0)))) ((c_plus (cS (cS c0))) (cS (cS c0)))) % 69.40/69.78 Found (eq_ref0 ((c_plus (cS (cS c0))) (cS (cS c0)))) as proof of (((eq n) ((c_plus (cS (cS c0))) (cS (cS c0)))) b) % 69.40/69.78 Found ((eq_ref n) ((c_plus (cS (cS c0))) (cS (cS c0)))) as proof of (((eq n) ((c_plus (cS (cS c0))) (cS (cS c0)))) b) % 69.40/69.78 Found ((eq_ref n) ((c_plus (cS (cS c0))) (cS (cS c0)))) as proof of (((eq n) ((c_plus (cS (cS c0))) (cS (cS c0)))) b) % 69.40/69.78 Found ((eq_ref n) ((c_plus (cS (cS c0))) (cS (cS c0)))) as proof of (((eq n) ((c_plus (cS (cS c0))) (cS (cS c0)))) b) % 69.40/69.78 Found x0:(P ((c_star (cS (cS c0))) (cS (cS c0)))) % 69.40/69.78 Instantiate: b:=((c_star (cS (cS c0))) (cS (cS c0))):n % 69.40/69.78 Found x0 as proof of (P0 b) % 69.40/69.78 Found eq_ref00:=(eq_ref0 ((c_plus (cS (cS c0))) (cS (cS c0)))):(((eq n) ((c_plus (cS (cS c0))) (cS (cS c0)))) ((c_plus (cS (cS c0))) (cS (cS c0)))) % 69.40/69.78 Found (eq_ref0 ((c_plus (cS (cS c0))) (cS (cS c0)))) as proof of (((eq n) ((c_plus (cS (cS c0))) (cS (cS c0)))) b) % 69.40/69.78 Found ((eq_ref n) ((c_plus (cS (cS c0))) (cS (cS c0)))) as proof of (((eq n) ((c_plus (cS (cS c0))) (cS (cS c0)))) b) % 69.40/69.78 Found ((eq_ref n) ((c_plus (cS (cS c0))) (cS (cS c0)))) as proof of (((eq n) ((c_plus (cS (cS c0))) (cS (cS c0)))) b) % 69.40/69.78 Found ((eq_ref n) ((c_plus (cS (cS c0))) (cS (cS c0)))) as proof of (((eq n) ((c_plus (cS (cS c0))) (cS (cS c0)))) b) % 69.40/69.78 Found eq_ref00:=(eq_ref0 ((c_plus (cS (cS c0))) (cS (cS c0)))):(((eq n) ((c_plus (cS (cS c0))) (cS (cS c0)))) ((c_plus (cS (cS c0))) (cS (cS c0)))) % 69.40/69.78 Found (eq_ref0 ((c_plus (cS (cS c0))) (cS (cS c0)))) as proof of (((eq n) ((c_plus (cS (cS c0))) (cS (cS c0)))) b) % 69.40/69.78 Found ((eq_ref n) ((c_plus (cS (cS c0))) (cS (cS c0)))) as proof of (((eq n) ((c_plus (cS (cS c0))) (cS (cS c0)))) b) % 69.40/69.78 Found ((eq_ref n) ((c_plus (cS (cS c0))) (cS (cS c0)))) as proof of (((eq n) ((c_plus (cS (cS c0))) (cS (cS c0)))) b) % 69.40/69.78 Found ((eq_ref n) ((c_plus (cS (cS c0))) (cS (cS c0)))) as proof of (((eq n) ((c_plus (cS (cS c0))) (cS (cS c0)))) b) % 69.40/69.78 Found eq_ref00:=(eq_ref0 b):(((eq n) b) b) % 69.40/69.78 Found (eq_ref0 b) as proof of (((eq n) b) ((c_star (cS (cS c0))) (cS (cS c0)))) % 69.40/69.78 Found ((eq_ref n) b) as proof of (((eq n) b) ((c_star (cS (cS c0))) (cS (cS c0)))) % 69.40/69.78 Found ((eq_ref n) b) as proof of (((eq n) b) ((c_star (cS (cS c0))) (cS (cS c0)))) % 69.40/69.78 Found ((eq_ref n) b) as proof of (((eq n) b) ((c_star (cS (cS c0))) (cS (cS c0)))) % 69.40/69.78 Found eq_ref00:=(eq_ref0 ((c_plus (cS (cS c0))) (cS (cS c0)))):(((eq n) ((c_plus (cS (cS c0))) (cS (cS c0)))) ((c_plus (cS (cS c0))) (cS (cS c0)))) % 69.40/69.78 Found (eq_ref0 ((c_plus (cS (cS c0))) (cS (cS c0)))) as proof of (((eq n) ((c_plus (cS (cS c0))) (cS (cS c0)))) b) % 69.40/69.78 Found ((eq_ref n) ((c_plus (cS (cS c0))) (cS (cS c0)))) as proof of (((eq n) ((c_plus (cS (cS c0))) (cS (cS c0)))) b) % 69.40/69.78 Found ((eq_ref n) ((c_plus (cS (cS c0))) (cS (cS c0)))) as proof of (((eq n) ((c_plus (cS (cS c0))) (cS (cS c0)))) b) % 69.40/69.78 Found ((eq_ref n) ((c_plus (cS (cS c0))) (cS (cS c0)))) as proof of (((eq n) ((c_plus (cS (cS c0))) (cS (cS c0)))) b) % 69.40/69.78 Found eq_ref00:=(eq_ref0 b):(((eq n) b) b) % 69.40/69.78 Found (eq_ref0 b) as proof of (((eq n) b) ((c_star (cS (cS c0))) (cS (cS c0)))) % 69.40/69.78 Found ((eq_ref n) b) as proof of (((eq n) b) ((c_star (cS (cS c0))) (cS (cS c0)))) % 69.40/69.78 Found ((eq_ref n) b) as proof of (((eq n) b) ((c_star (cS (cS c0))) (cS (cS c0)))) % 69.40/69.78 Found ((eq_ref n) b) as proof of (((eq n) b) ((c_star (cS (cS c0))) (cS (cS c0)))) % 69.40/69.78 Found x2:(P ((c_star (cS (cS c0))) (cS (cS c0)))) % 69.40/69.78 Instantiate: b:=((c_star (cS (cS c0))) (cS (cS c0))):n % 69.40/69.78 Found x2 as proof of (P0 b) % 69.40/69.78 Found eq_ref00:=(eq_ref0 ((c_plus (cS (cS c0))) (cS (cS c0)))):(((eq n) ((c_plus (cS (cS c0))) (cS (cS c0)))) ((c_plus (cS (cS c0))) (cS (cS c0)))) % 69.40/69.78 Found (eq_ref0 ((c_plus (cS (cS c0))) (cS (cS c0)))) as proof of (((eq n) ((c_plus (cS (cS c0))) (cS (cS c0)))) b) % 69.40/69.78 Found ((eq_ref n) ((c_plus (cS (cS c0))) (cS (cS c0)))) as proof of (((eq n) ((c_plus (cS (cS c0))) (cS (cS c0)))) b) % 69.40/69.78 Found ((eq_ref n) ((c_plus (cS (cS c0))) (cS (cS c0)))) as proof of (((eq n) ((c_plus (cS (cS c0))) (cS (cS c0)))) b) % 69.40/69.78 Found ((eq_ref n) ((c_plus (cS (cS c0))) (cS (cS c0)))) as proof of (((eq n) ((c_plus (cS (cS c0))) (cS (cS c0)))) b) % 113.64/114.07 Found eq_ref00:=(eq_ref0 ((c_star (cS (cS c0))) (cS (cS c0)))):(((eq n) ((c_star (cS (cS c0))) (cS (cS c0)))) ((c_star (cS (cS c0))) (cS (cS c0)))) % 113.64/114.07 Found (eq_ref0 ((c_star (cS (cS c0))) (cS (cS c0)))) as proof of (((eq n) ((c_star (cS (cS c0))) (cS (cS c0)))) b) % 113.64/114.07 Found ((eq_ref n) ((c_star (cS (cS c0))) (cS (cS c0)))) as proof of (((eq n) ((c_star (cS (cS c0))) (cS (cS c0)))) b) % 113.64/114.07 Found ((eq_ref n) ((c_star (cS (cS c0))) (cS (cS c0)))) as proof of (((eq n) ((c_star (cS (cS c0))) (cS (cS c0)))) b) % 113.64/114.07 Found ((eq_ref n) ((c_star (cS (cS c0))) (cS (cS c0)))) as proof of (((eq n) ((c_star (cS (cS c0))) (cS (cS c0)))) b) % 113.64/114.07 Found eq_ref00:=(eq_ref0 b):(((eq n) b) b) % 113.64/114.07 Found (eq_ref0 b) as proof of (((eq n) b) ((c_plus (cS (cS c0))) (cS (cS c0)))) % 113.64/114.07 Found ((eq_ref n) b) as proof of (((eq n) b) ((c_plus (cS (cS c0))) (cS (cS c0)))) % 113.64/114.07 Found ((eq_ref n) b) as proof of (((eq n) b) ((c_plus (cS (cS c0))) (cS (cS c0)))) % 113.64/114.07 Found ((eq_ref n) b) as proof of (((eq n) b) ((c_plus (cS (cS c0))) (cS (cS c0)))) % 113.64/114.07 Found eq_ref00:=(eq_ref0 ((c_plus (cS (cS c0))) (cS (cS c0)))):(((eq n) ((c_plus (cS (cS c0))) (cS (cS c0)))) ((c_plus (cS (cS c0))) (cS (cS c0)))) % 113.64/114.07 Found (eq_ref0 ((c_plus (cS (cS c0))) (cS (cS c0)))) as proof of (((eq n) ((c_plus (cS (cS c0))) (cS (cS c0)))) b) % 113.64/114.07 Found ((eq_ref n) ((c_plus (cS (cS c0))) (cS (cS c0)))) as proof of (((eq n) ((c_plus (cS (cS c0))) (cS (cS c0)))) b) % 113.64/114.07 Found ((eq_ref n) ((c_plus (cS (cS c0))) (cS (cS c0)))) as proof of (((eq n) ((c_plus (cS (cS c0))) (cS (cS c0)))) b) % 113.64/114.07 Found ((eq_ref n) ((c_plus (cS (cS c0))) (cS (cS c0)))) as proof of (((eq n) ((c_plus (cS (cS c0))) (cS (cS c0)))) b) % 113.64/114.07 Found x0:(P0 b) % 113.64/114.07 Instantiate: b:=((c_star (cS (cS c0))) (cS (cS c0))):n % 113.64/114.07 Found (fun (x0:(P0 b))=> x0) as proof of (P0 ((c_star (cS (cS c0))) (cS (cS c0)))) % 113.64/114.07 Found (fun (P0:(n->Prop)) (x0:(P0 b))=> x0) as proof of ((P0 b)->(P0 ((c_star (cS (cS c0))) (cS (cS c0))))) % 113.64/114.07 Found (fun (P0:(n->Prop)) (x0:(P0 b))=> x0) as proof of (P b) % 113.64/114.07 Found x0:(P ((c_plus (cS (cS c0))) (cS (cS c0)))) % 113.64/114.07 Instantiate: b:=((c_plus (cS (cS c0))) (cS (cS c0))):n % 113.64/114.07 Found x0 as proof of (P0 b) % 113.64/114.07 Found eq_ref00:=(eq_ref0 ((c_star (cS (cS c0))) (cS (cS c0)))):(((eq n) ((c_star (cS (cS c0))) (cS (cS c0)))) ((c_star (cS (cS c0))) (cS (cS c0)))) % 113.64/114.07 Found (eq_ref0 ((c_star (cS (cS c0))) (cS (cS c0)))) as proof of (((eq n) ((c_star (cS (cS c0))) (cS (cS c0)))) b) % 113.64/114.07 Found ((eq_ref n) ((c_star (cS (cS c0))) (cS (cS c0)))) as proof of (((eq n) ((c_star (cS (cS c0))) (cS (cS c0)))) b) % 113.64/114.07 Found ((eq_ref n) ((c_star (cS (cS c0))) (cS (cS c0)))) as proof of (((eq n) ((c_star (cS (cS c0))) (cS (cS c0)))) b) % 113.64/114.07 Found ((eq_ref n) ((c_star (cS (cS c0))) (cS (cS c0)))) as proof of (((eq n) ((c_star (cS (cS c0))) (cS (cS c0)))) b) % 113.64/114.07 Found eq_ref00:=(eq_ref0 b):(((eq n) b) b) % 113.64/114.07 Found (eq_ref0 b) as proof of (((eq n) b) ((c_star (cS (cS c0))) (cS (cS c0)))) % 113.64/114.07 Found ((eq_ref n) b) as proof of (((eq n) b) ((c_star (cS (cS c0))) (cS (cS c0)))) % 113.64/114.07 Found ((eq_ref n) b) as proof of (((eq n) b) ((c_star (cS (cS c0))) (cS (cS c0)))) % 113.64/114.07 Found ((eq_ref n) b) as proof of (((eq n) b) ((c_star (cS (cS c0))) (cS (cS c0)))) % 113.64/114.07 Found eq_ref00:=(eq_ref0 ((c_plus (cS (cS c0))) (cS (cS c0)))):(((eq n) ((c_plus (cS (cS c0))) (cS (cS c0)))) ((c_plus (cS (cS c0))) (cS (cS c0)))) % 113.64/114.07 Found (eq_ref0 ((c_plus (cS (cS c0))) (cS (cS c0)))) as proof of (((eq n) ((c_plus (cS (cS c0))) (cS (cS c0)))) b) % 113.64/114.07 Found ((eq_ref n) ((c_plus (cS (cS c0))) (cS (cS c0)))) as proof of (((eq n) ((c_plus (cS (cS c0))) (cS (cS c0)))) b) % 113.64/114.07 Found ((eq_ref n) ((c_plus (cS (cS c0))) (cS (cS c0)))) as proof of (((eq n) ((c_plus (cS (cS c0))) (cS (cS c0)))) b) % 113.64/114.07 Found ((eq_ref n) ((c_plus (cS (cS c0))) (cS (cS c0)))) as proof of (((eq n) ((c_plus (cS (cS c0))) (cS (cS c0)))) b) % 113.64/114.07 Found x00:(P ((c_star (cS (cS c0))) (cS (cS c0)))) % 113.64/114.07 Found (fun (x00:(P ((c_star (cS (cS c0))) (cS (cS c0)))))=> x00) as proof of (P ((c_star (cS (cS c0))) (cS (cS c0)))) % 113.64/114.07 Found (fun (x00:(P ((c_star (cS (cS c0))) (cS (cS c0)))))=> x00) as proof of (P0 ((c_star (cS (cS c0))) (cS (cS c0)))) % 113.64/114.07 Found eq_ref00:=(eq_ref0 ((c_star (cS (cS c0))) (cS (cS c0)))):(((eq n) ((c_star (cS (cS c0))) (cS (cS c0)))) ((c_star (cS (cS c0))) (cS (cS c0)))) % 137.10/137.48 Found (eq_ref0 ((c_star (cS (cS c0))) (cS (cS c0)))) as proof of (((eq n) ((c_star (cS (cS c0))) (cS (cS c0)))) b) % 137.10/137.48 Found ((eq_ref n) ((c_star (cS (cS c0))) (cS (cS c0)))) as proof of (((eq n) ((c_star (cS (cS c0))) (cS (cS c0)))) b) % 137.10/137.48 Found ((eq_ref n) ((c_star (cS (cS c0))) (cS (cS c0)))) as proof of (((eq n) ((c_star (cS (cS c0))) (cS (cS c0)))) b) % 137.10/137.48 Found ((eq_ref n) ((c_star (cS (cS c0))) (cS (cS c0)))) as proof of (((eq n) ((c_star (cS (cS c0))) (cS (cS c0)))) b) % 137.10/137.48 Found eq_ref00:=(eq_ref0 b):(((eq n) b) b) % 137.10/137.48 Found (eq_ref0 b) as proof of (((eq n) b) ((c_plus (cS (cS c0))) (cS (cS c0)))) % 137.10/137.48 Found ((eq_ref n) b) as proof of (((eq n) b) ((c_plus (cS (cS c0))) (cS (cS c0)))) % 137.10/137.48 Found ((eq_ref n) b) as proof of (((eq n) b) ((c_plus (cS (cS c0))) (cS (cS c0)))) % 137.10/137.48 Found ((eq_ref n) b) as proof of (((eq n) b) ((c_plus (cS (cS c0))) (cS (cS c0)))) % 137.10/137.48 Found eq_ref00:=(eq_ref0 ((c_star (cS (cS c0))) (cS (cS c0)))):(((eq n) ((c_star (cS (cS c0))) (cS (cS c0)))) ((c_star (cS (cS c0))) (cS (cS c0)))) % 137.10/137.48 Found (eq_ref0 ((c_star (cS (cS c0))) (cS (cS c0)))) as proof of (((eq n) ((c_star (cS (cS c0))) (cS (cS c0)))) b0) % 137.10/137.48 Found ((eq_ref n) ((c_star (cS (cS c0))) (cS (cS c0)))) as proof of (((eq n) ((c_star (cS (cS c0))) (cS (cS c0)))) b0) % 137.10/137.48 Found ((eq_ref n) ((c_star (cS (cS c0))) (cS (cS c0)))) as proof of (((eq n) ((c_star (cS (cS c0))) (cS (cS c0)))) b0) % 137.10/137.48 Found ((eq_ref n) ((c_star (cS (cS c0))) (cS (cS c0)))) as proof of (((eq n) ((c_star (cS (cS c0))) (cS (cS c0)))) b0) % 137.10/137.48 Found eq_ref00:=(eq_ref0 b0):(((eq n) b0) b0) % 137.10/137.48 Found (eq_ref0 b0) as proof of (((eq n) b0) ((c_plus (cS (cS c0))) (cS (cS c0)))) % 137.10/137.48 Found ((eq_ref n) b0) as proof of (((eq n) b0) ((c_plus (cS (cS c0))) (cS (cS c0)))) % 137.10/137.48 Found ((eq_ref n) b0) as proof of (((eq n) b0) ((c_plus (cS (cS c0))) (cS (cS c0)))) % 137.10/137.48 Found ((eq_ref n) b0) as proof of (((eq n) b0) ((c_plus (cS (cS c0))) (cS (cS c0)))) % 137.10/137.48 Found eq_ref00:=(eq_ref0 a):(((eq n) a) a) % 137.10/137.48 Found (eq_ref0 a) as proof of (((eq n) a) (cS (cS c0))) % 137.10/137.48 Found ((eq_ref n) a) as proof of (((eq n) a) (cS (cS c0))) % 137.10/137.48 Found ((eq_ref n) a) as proof of (((eq n) a) (cS (cS c0))) % 137.10/137.48 Found ((eq_ref n) a) as proof of (((eq n) a) (cS (cS c0))) % 137.10/137.48 Found eq_ref00:=(eq_ref0 a):(((eq n) a) a) % 137.10/137.48 Found (eq_ref0 a) as proof of (((eq n) a) (cS (cS c0))) % 137.10/137.48 Found ((eq_ref n) a) as proof of (((eq n) a) (cS (cS c0))) % 137.10/137.48 Found ((eq_ref n) a) as proof of (((eq n) a) (cS (cS c0))) % 137.10/137.48 Found ((eq_ref n) a) as proof of (((eq n) a) (cS (cS c0))) % 137.10/137.48 Found eq_ref00:=(eq_ref0 a):(((eq n) a) a) % 137.10/137.48 Found (eq_ref0 a) as proof of (((eq n) a) (cS (cS c0))) % 137.10/137.48 Found ((eq_ref n) a) as proof of (((eq n) a) (cS (cS c0))) % 137.10/137.48 Found ((eq_ref n) a) as proof of (((eq n) a) (cS (cS c0))) % 137.10/137.48 Found ((eq_ref n) a) as proof of (((eq n) a) (cS (cS c0))) % 137.10/137.48 Found x100:=(x10 (cS c0)):(((eq n) ((c_star (cS (cS c0))) (cS (cS c0)))) ((c_plus ((c_star (cS (cS c0))) (cS c0))) (cS (cS c0)))) % 137.10/137.48 Found (x10 (cS c0)) as proof of (((eq n) ((c_star (cS (cS c0))) (cS (cS c0)))) b) % 137.10/137.48 Found ((x1 (cS (cS c0))) (cS c0)) as proof of (((eq n) ((c_star (cS (cS c0))) (cS (cS c0)))) b) % 137.10/137.48 Found ((x1 (cS (cS c0))) (cS c0)) as proof of (((eq n) ((c_star (cS (cS c0))) (cS (cS c0)))) b) % 137.10/137.48 Found ((x1 (cS (cS c0))) (cS c0)) as proof of (((eq n) ((c_star (cS (cS c0))) (cS (cS c0)))) b) % 137.10/137.48 Found eq_ref00:=(eq_ref0 b):(((eq n) b) b) % 137.10/137.48 Found (eq_ref0 b) as proof of (((eq n) b) ((c_plus (cS (cS c0))) (cS (cS c0)))) % 137.10/137.48 Found ((eq_ref n) b) as proof of (((eq n) b) ((c_plus (cS (cS c0))) (cS (cS c0)))) % 137.10/137.48 Found ((eq_ref n) b) as proof of (((eq n) b) ((c_plus (cS (cS c0))) (cS (cS c0)))) % 137.10/137.48 Found ((eq_ref n) b) as proof of (((eq n) b) ((c_plus (cS (cS c0))) (cS (cS c0)))) % 137.10/137.48 Found eq_ref00:=(eq_ref0 b):(((eq n) b) b) % 137.10/137.48 Found (eq_ref0 b) as proof of (((eq n) b) ((c_star (cS (cS c0))) (cS (cS c0)))) % 137.10/137.48 Found ((eq_ref n) b) as proof of (((eq n) b) ((c_star (cS (cS c0))) (cS (cS c0)))) % 137.10/137.48 Found ((eq_ref n) b) as proof of (((eq n) b) ((c_star (cS (cS c0))) (cS (cS c0)))) % 137.10/137.48 Found ((eq_ref n) b) as proof of (((eq n) b) ((c_star (cS (cS c0))) (cS (cS c0)))) % 137.10/137.48 Found x500:=(x50 (cS c0)):(((eq n) ((c_plus (cS (cS c0))) (cS (cS c0)))) (cS ((c_plus (cS (cS c0))) (cS c0)))) % 147.15/147.54 Found (x50 (cS c0)) as proof of (((eq n) ((c_plus (cS (cS c0))) (cS (cS c0)))) b) % 147.15/147.54 Found ((x5 (cS (cS c0))) (cS c0)) as proof of (((eq n) ((c_plus (cS (cS c0))) (cS (cS c0)))) b) % 147.15/147.54 Found ((x5 (cS (cS c0))) (cS c0)) as proof of (((eq n) ((c_plus (cS (cS c0))) (cS (cS c0)))) b) % 147.15/147.54 Found ((x5 (cS (cS c0))) (cS c0)) as proof of (((eq n) ((c_plus (cS (cS c0))) (cS (cS c0)))) b) % 147.15/147.54 Found eq_ref00:=(eq_ref0 b):(((eq n) b) b) % 147.15/147.54 Found (eq_ref0 b) as proof of (((eq n) b) ((c_star (cS (cS c0))) (cS (cS c0)))) % 147.15/147.54 Found ((eq_ref n) b) as proof of (((eq n) b) ((c_star (cS (cS c0))) (cS (cS c0)))) % 147.15/147.54 Found ((eq_ref n) b) as proof of (((eq n) b) ((c_star (cS (cS c0))) (cS (cS c0)))) % 147.15/147.54 Found ((eq_ref n) b) as proof of (((eq n) b) ((c_star (cS (cS c0))) (cS (cS c0)))) % 147.15/147.54 Found x500:=(x50 (cS c0)):(((eq n) ((c_plus (cS (cS c0))) (cS (cS c0)))) (cS ((c_plus (cS (cS c0))) (cS c0)))) % 147.15/147.54 Found (x50 (cS c0)) as proof of (((eq n) ((c_plus (cS (cS c0))) (cS (cS c0)))) b) % 147.15/147.54 Found ((x5 (cS (cS c0))) (cS c0)) as proof of (((eq n) ((c_plus (cS (cS c0))) (cS (cS c0)))) b) % 147.15/147.54 Found ((x5 (cS (cS c0))) (cS c0)) as proof of (((eq n) ((c_plus (cS (cS c0))) (cS (cS c0)))) b) % 147.15/147.54 Found ((x5 (cS (cS c0))) (cS c0)) as proof of (((eq n) ((c_plus (cS (cS c0))) (cS (cS c0)))) b) % 147.15/147.54 Found eq_ref00:=(eq_ref0 b):(((eq n) b) b) % 147.15/147.54 Found (eq_ref0 b) as proof of (((eq n) b) ((c_star (cS (cS c0))) (cS (cS c0)))) % 147.15/147.54 Found ((eq_ref n) b) as proof of (((eq n) b) ((c_star (cS (cS c0))) (cS (cS c0)))) % 147.15/147.54 Found ((eq_ref n) b) as proof of (((eq n) b) ((c_star (cS (cS c0))) (cS (cS c0)))) % 147.15/147.54 Found ((eq_ref n) b) as proof of (((eq n) b) ((c_star (cS (cS c0))) (cS (cS c0)))) % 147.15/147.54 Found x500:=(x50 (cS c0)):(((eq n) ((c_plus (cS (cS c0))) (cS (cS c0)))) (cS ((c_plus (cS (cS c0))) (cS c0)))) % 147.15/147.54 Found (x50 (cS c0)) as proof of (((eq n) ((c_plus (cS (cS c0))) (cS (cS c0)))) b) % 147.15/147.54 Found ((x5 (cS (cS c0))) (cS c0)) as proof of (((eq n) ((c_plus (cS (cS c0))) (cS (cS c0)))) b) % 147.15/147.54 Found ((x5 (cS (cS c0))) (cS c0)) as proof of (((eq n) ((c_plus (cS (cS c0))) (cS (cS c0)))) b) % 147.15/147.54 Found ((x5 (cS (cS c0))) (cS c0)) as proof of (((eq n) ((c_plus (cS (cS c0))) (cS (cS c0)))) b) % 147.15/147.54 Found eq_ref00:=(eq_ref0 ((c_plus (cS (cS c0))) (cS (cS c0)))):(((eq n) ((c_plus (cS (cS c0))) (cS (cS c0)))) ((c_plus (cS (cS c0))) (cS (cS c0)))) % 147.15/147.54 Found (eq_ref0 ((c_plus (cS (cS c0))) (cS (cS c0)))) as proof of (((eq n) ((c_plus (cS (cS c0))) (cS (cS c0)))) b) % 147.15/147.54 Found ((eq_ref n) ((c_plus (cS (cS c0))) (cS (cS c0)))) as proof of (((eq n) ((c_plus (cS (cS c0))) (cS (cS c0)))) b) % 147.15/147.54 Found ((eq_ref n) ((c_plus (cS (cS c0))) (cS (cS c0)))) as proof of (((eq n) ((c_plus (cS (cS c0))) (cS (cS c0)))) b) % 147.15/147.54 Found ((eq_ref n) ((c_plus (cS (cS c0))) (cS (cS c0)))) as proof of (((eq n) ((c_plus (cS (cS c0))) (cS (cS c0)))) b) % 147.15/147.54 Found x2:(P0 b) % 147.15/147.54 Instantiate: b:=((c_star (cS (cS c0))) (cS (cS c0))):n % 147.15/147.54 Found (fun (x2:(P0 b))=> x2) as proof of (P0 ((c_star (cS (cS c0))) (cS (cS c0)))) % 147.15/147.54 Found (fun (P0:(n->Prop)) (x2:(P0 b))=> x2) as proof of ((P0 b)->(P0 ((c_star (cS (cS c0))) (cS (cS c0))))) % 147.15/147.54 Found (fun (P0:(n->Prop)) (x2:(P0 b))=> x2) as proof of (P b) % 147.15/147.54 Found x4:(P ((c_star (cS (cS c0))) (cS (cS c0)))) % 147.15/147.54 Instantiate: b:=((c_star (cS (cS c0))) (cS (cS c0))):n % 147.15/147.54 Found x4 as proof of (P0 b) % 147.15/147.54 Found eq_ref00:=(eq_ref0 ((c_plus (cS (cS c0))) (cS (cS c0)))):(((eq n) ((c_plus (cS (cS c0))) (cS (cS c0)))) ((c_plus (cS (cS c0))) (cS (cS c0)))) % 147.15/147.54 Found (eq_ref0 ((c_plus (cS (cS c0))) (cS (cS c0)))) as proof of (((eq n) ((c_plus (cS (cS c0))) (cS (cS c0)))) b) % 147.15/147.54 Found ((eq_ref n) ((c_plus (cS (cS c0))) (cS (cS c0)))) as proof of (((eq n) ((c_plus (cS (cS c0))) (cS (cS c0)))) b) % 147.15/147.54 Found ((eq_ref n) ((c_plus (cS (cS c0))) (cS (cS c0)))) as proof of (((eq n) ((c_plus (cS (cS c0))) (cS (cS c0)))) b) % 147.15/147.54 Found ((eq_ref n) ((c_plus (cS (cS c0))) (cS (cS c0)))) as proof of (((eq n) ((c_plus (cS (cS c0))) (cS (cS c0)))) b) % 147.15/147.54 Found x2:(P ((c_plus (cS (cS c0))) (cS (cS c0)))) % 147.15/147.54 Instantiate: b:=((c_plus (cS (cS c0))) (cS (cS c0))):n % 147.15/147.54 Found x2 as proof of (P0 b) % 147.15/147.54 Found x100:=(x10 (cS c0)):(((eq n) ((c_star (cS (cS c0))) (cS (cS c0)))) ((c_plus ((c_star (cS (cS c0))) (cS c0))) (cS (cS c0)))) % 147.15/147.54 Found (x10 (cS c0)) as proof of (((eq n) ((c_star (cS (cS c0))) (cS (cS c0)))) b) % 175.96/176.33 Found ((x1 (cS (cS c0))) (cS c0)) as proof of (((eq n) ((c_star (cS (cS c0))) (cS (cS c0)))) b) % 175.96/176.33 Found ((x1 (cS (cS c0))) (cS c0)) as proof of (((eq n) ((c_star (cS (cS c0))) (cS (cS c0)))) b) % 175.96/176.33 Found ((x1 (cS (cS c0))) (cS c0)) as proof of (((eq n) ((c_star (cS (cS c0))) (cS (cS c0)))) b) % 175.96/176.33 Found eq_ref00:=(eq_ref0 b):(((eq n) b) b) % 175.96/176.33 Found (eq_ref0 b) as proof of (((eq n) b) ((c_star (cS (cS c0))) (cS (cS c0)))) % 175.96/176.33 Found ((eq_ref n) b) as proof of (((eq n) b) ((c_star (cS (cS c0))) (cS (cS c0)))) % 175.96/176.33 Found ((eq_ref n) b) as proof of (((eq n) b) ((c_star (cS (cS c0))) (cS (cS c0)))) % 175.96/176.33 Found ((eq_ref n) b) as proof of (((eq n) b) ((c_star (cS (cS c0))) (cS (cS c0)))) % 175.96/176.33 Found eq_ref00:=(eq_ref0 ((c_plus (cS (cS c0))) (cS (cS c0)))):(((eq n) ((c_plus (cS (cS c0))) (cS (cS c0)))) ((c_plus (cS (cS c0))) (cS (cS c0)))) % 175.96/176.33 Found (eq_ref0 ((c_plus (cS (cS c0))) (cS (cS c0)))) as proof of (((eq n) ((c_plus (cS (cS c0))) (cS (cS c0)))) b) % 175.96/176.33 Found ((eq_ref n) ((c_plus (cS (cS c0))) (cS (cS c0)))) as proof of (((eq n) ((c_plus (cS (cS c0))) (cS (cS c0)))) b) % 175.96/176.33 Found ((eq_ref n) ((c_plus (cS (cS c0))) (cS (cS c0)))) as proof of (((eq n) ((c_plus (cS (cS c0))) (cS (cS c0)))) b) % 175.96/176.33 Found ((eq_ref n) ((c_plus (cS (cS c0))) (cS (cS c0)))) as proof of (((eq n) ((c_plus (cS (cS c0))) (cS (cS c0)))) b) % 175.96/176.33 Found eq_ref00:=(eq_ref0 b):(((eq n) b) b) % 175.96/176.33 Found (eq_ref0 b) as proof of (((eq n) b) ((c_star (cS (cS c0))) (cS (cS c0)))) % 175.96/176.33 Found ((eq_ref n) b) as proof of (((eq n) b) ((c_star (cS (cS c0))) (cS (cS c0)))) % 175.96/176.33 Found ((eq_ref n) b) as proof of (((eq n) b) ((c_star (cS (cS c0))) (cS (cS c0)))) % 175.96/176.33 Found ((eq_ref n) b) as proof of (((eq n) b) ((c_star (cS (cS c0))) (cS (cS c0)))) % 175.96/176.33 Found eq_ref00:=(eq_ref0 ((c_plus (cS (cS c0))) (cS (cS c0)))):(((eq n) ((c_plus (cS (cS c0))) (cS (cS c0)))) ((c_plus (cS (cS c0))) (cS (cS c0)))) % 175.96/176.33 Found (eq_ref0 ((c_plus (cS (cS c0))) (cS (cS c0)))) as proof of (((eq n) ((c_plus (cS (cS c0))) (cS (cS c0)))) b) % 175.96/176.33 Found ((eq_ref n) ((c_plus (cS (cS c0))) (cS (cS c0)))) as proof of (((eq n) ((c_plus (cS (cS c0))) (cS (cS c0)))) b) % 175.96/176.33 Found ((eq_ref n) ((c_plus (cS (cS c0))) (cS (cS c0)))) as proof of (((eq n) ((c_plus (cS (cS c0))) (cS (cS c0)))) b) % 175.96/176.33 Found ((eq_ref n) ((c_plus (cS (cS c0))) (cS (cS c0)))) as proof of (((eq n) ((c_plus (cS (cS c0))) (cS (cS c0)))) b) % 175.96/176.33 Found eq_ref00:=(eq_ref0 ((c_plus (cS (cS c0))) (cS (cS c0)))):(((eq n) ((c_plus (cS (cS c0))) (cS (cS c0)))) ((c_plus (cS (cS c0))) (cS (cS c0)))) % 175.96/176.33 Found (eq_ref0 ((c_plus (cS (cS c0))) (cS (cS c0)))) as proof of (((eq n) ((c_plus (cS (cS c0))) (cS (cS c0)))) b) % 175.96/176.33 Found ((eq_ref n) ((c_plus (cS (cS c0))) (cS (cS c0)))) as proof of (((eq n) ((c_plus (cS (cS c0))) (cS (cS c0)))) b) % 175.96/176.33 Found ((eq_ref n) ((c_plus (cS (cS c0))) (cS (cS c0)))) as proof of (((eq n) ((c_plus (cS (cS c0))) (cS (cS c0)))) b) % 175.96/176.33 Found ((eq_ref n) ((c_plus (cS (cS c0))) (cS (cS c0)))) as proof of (((eq n) ((c_plus (cS (cS c0))) (cS (cS c0)))) b) % 175.96/176.33 Found eq_ref00:=(eq_ref0 b):(((eq n) b) b) % 175.96/176.33 Found (eq_ref0 b) as proof of (((eq n) b) ((c_star (cS (cS c0))) (cS (cS c0)))) % 175.96/176.33 Found ((eq_ref n) b) as proof of (((eq n) b) ((c_star (cS (cS c0))) (cS (cS c0)))) % 175.96/176.33 Found ((eq_ref n) b) as proof of (((eq n) b) ((c_star (cS (cS c0))) (cS (cS c0)))) % 175.96/176.33 Found ((eq_ref n) b) as proof of (((eq n) b) ((c_star (cS (cS c0))) (cS (cS c0)))) % 175.96/176.33 Found eq_ref00:=(eq_ref0 ((c_plus (cS (cS c0))) (cS (cS c0)))):(((eq n) ((c_plus (cS (cS c0))) (cS (cS c0)))) ((c_plus (cS (cS c0))) (cS (cS c0)))) % 175.96/176.33 Found (eq_ref0 ((c_plus (cS (cS c0))) (cS (cS c0)))) as proof of (((eq n) ((c_plus (cS (cS c0))) (cS (cS c0)))) b) % 175.96/176.33 Found ((eq_ref n) ((c_plus (cS (cS c0))) (cS (cS c0)))) as proof of (((eq n) ((c_plus (cS (cS c0))) (cS (cS c0)))) b) % 175.96/176.33 Found ((eq_ref n) ((c_plus (cS (cS c0))) (cS (cS c0)))) as proof of (((eq n) ((c_plus (cS (cS c0))) (cS (cS c0)))) b) % 175.96/176.33 Found ((eq_ref n) ((c_plus (cS (cS c0))) (cS (cS c0)))) as proof of (((eq n) ((c_plus (cS (cS c0))) (cS (cS c0)))) b) % 175.96/176.33 Found x2:(P0 b) % 175.96/176.33 Instantiate: b:=((c_star (cS (cS c0))) (cS (cS c0))):n % 175.96/176.33 Found (fun (x2:(P0 b))=> x2) as proof of (P0 ((c_star (cS (cS c0))) (cS (cS c0)))) % 175.96/176.33 Found (fun (P0:(n->Prop)) (x2:(P0 b))=> x2) as proof of ((P0 b)->(P0 ((c_star (cS (cS c0))) (cS (cS c0))))) % 244.13/244.58 Found (fun (P0:(n->Prop)) (x2:(P0 b))=> x2) as proof of (P b) % 244.13/244.58 Found x00:(P b) % 244.13/244.58 Found (fun (x00:(P b))=> x00) as proof of (P b) % 244.13/244.58 Found (fun (x00:(P b))=> x00) as proof of (P0 b) % 244.13/244.58 Found x2:(P ((c_plus (cS (cS c0))) (cS (cS c0)))) % 244.13/244.58 Instantiate: b:=((c_plus (cS (cS c0))) (cS (cS c0))):n % 244.13/244.58 Found x2 as proof of (P0 b) % 244.13/244.58 Found x100:=(x10 (cS c0)):(((eq n) ((c_star (cS (cS c0))) (cS (cS c0)))) ((c_plus ((c_star (cS (cS c0))) (cS c0))) (cS (cS c0)))) % 244.13/244.58 Found (x10 (cS c0)) as proof of (((eq n) ((c_star (cS (cS c0))) (cS (cS c0)))) b) % 244.13/244.58 Found ((x1 (cS (cS c0))) (cS c0)) as proof of (((eq n) ((c_star (cS (cS c0))) (cS (cS c0)))) b) % 244.13/244.58 Found ((x1 (cS (cS c0))) (cS c0)) as proof of (((eq n) ((c_star (cS (cS c0))) (cS (cS c0)))) b) % 244.13/244.58 Found ((x1 (cS (cS c0))) (cS c0)) as proof of (((eq n) ((c_star (cS (cS c0))) (cS (cS c0)))) b) % 244.13/244.58 Found x20:(P ((c_star (cS (cS c0))) (cS (cS c0)))) % 244.13/244.58 Found (fun (x20:(P ((c_star (cS (cS c0))) (cS (cS c0)))))=> x20) as proof of (P ((c_star (cS (cS c0))) (cS (cS c0)))) % 244.13/244.58 Found (fun (x20:(P ((c_star (cS (cS c0))) (cS (cS c0)))))=> x20) as proof of (P0 ((c_star (cS (cS c0))) (cS (cS c0)))) % 244.13/244.58 Found eq_ref00:=(eq_ref0 b):(((eq n) b) b) % 244.13/244.58 Found (eq_ref0 b) as proof of (((eq n) b) ((c_plus (cS (cS c0))) (cS (cS c0)))) % 244.13/244.58 Found ((eq_ref n) b) as proof of (((eq n) b) ((c_plus (cS (cS c0))) (cS (cS c0)))) % 244.13/244.58 Found ((eq_ref n) b) as proof of (((eq n) b) ((c_plus (cS (cS c0))) (cS (cS c0)))) % 244.13/244.58 Found ((eq_ref n) b) as proof of (((eq n) b) ((c_plus (cS (cS c0))) (cS (cS c0)))) % 244.13/244.58 Found x100:=(x10 (cS c0)):(((eq n) ((c_star (cS (cS c0))) (cS (cS c0)))) ((c_plus ((c_star (cS (cS c0))) (cS c0))) (cS (cS c0)))) % 244.13/244.58 Found (x10 (cS c0)) as proof of (((eq n) ((c_star (cS (cS c0))) (cS (cS c0)))) b) % 244.13/244.58 Found ((x1 (cS (cS c0))) (cS c0)) as proof of (((eq n) ((c_star (cS (cS c0))) (cS (cS c0)))) b) % 244.13/244.58 Found ((x1 (cS (cS c0))) (cS c0)) as proof of (((eq n) ((c_star (cS (cS c0))) (cS (cS c0)))) b) % 244.13/244.58 Found ((x1 (cS (cS c0))) (cS c0)) as proof of (((eq n) ((c_star (cS (cS c0))) (cS (cS c0)))) b) % 244.13/244.58 Found x100:=(x10 (cS c0)):(((eq n) ((c_star (cS (cS c0))) (cS (cS c0)))) ((c_plus ((c_star (cS (cS c0))) (cS c0))) (cS (cS c0)))) % 244.13/244.59 Found (x10 (cS c0)) as proof of (((eq n) ((c_star (cS (cS c0))) (cS (cS c0)))) b0) % 244.13/244.59 Found ((x1 (cS (cS c0))) (cS c0)) as proof of (((eq n) ((c_star (cS (cS c0))) (cS (cS c0)))) b0) % 244.13/244.59 Found ((x1 (cS (cS c0))) (cS c0)) as proof of (((eq n) ((c_star (cS (cS c0))) (cS (cS c0)))) b0) % 244.13/244.59 Found ((x1 (cS (cS c0))) (cS c0)) as proof of (((eq n) ((c_star (cS (cS c0))) (cS (cS c0)))) b0) % 244.13/244.59 Found eq_ref00:=(eq_ref0 b0):(((eq n) b0) b0) % 244.13/244.59 Found (eq_ref0 b0) as proof of (((eq n) b0) ((c_plus (cS (cS c0))) (cS (cS c0)))) % 244.13/244.59 Found ((eq_ref n) b0) as proof of (((eq n) b0) ((c_plus (cS (cS c0))) (cS (cS c0)))) % 244.13/244.59 Found ((eq_ref n) b0) as proof of (((eq n) b0) ((c_plus (cS (cS c0))) (cS (cS c0)))) % 244.13/244.59 Found ((eq_ref n) b0) as proof of (((eq n) b0) ((c_plus (cS (cS c0))) (cS (cS c0)))) % 244.13/244.59 Found eq_ref00:=(eq_ref0 a):(((eq n) a) a) % 244.13/244.59 Found (eq_ref0 a) as proof of (((eq n) a) (cS (cS c0))) % 244.13/244.59 Found ((eq_ref n) a) as proof of (((eq n) a) (cS (cS c0))) % 244.13/244.59 Found ((eq_ref n) a) as proof of (((eq n) a) (cS (cS c0))) % 244.13/244.59 Found ((eq_ref n) a) as proof of (((eq n) a) (cS (cS c0))) % 244.13/244.59 Found eq_ref00:=(eq_ref0 a):(((eq n) a) a) % 244.13/244.59 Found (eq_ref0 a) as proof of (((eq n) a) (cS (cS c0))) % 244.13/244.59 Found ((eq_ref n) a) as proof of (((eq n) a) (cS (cS c0))) % 244.13/244.59 Found ((eq_ref n) a) as proof of (((eq n) a) (cS (cS c0))) % 244.13/244.59 Found ((eq_ref n) a) as proof of (((eq n) a) (cS (cS c0))) % 244.13/244.59 Found eq_ref00:=(eq_ref0 a):(((eq n) a) a) % 244.13/244.59 Found (eq_ref0 a) as proof of (((eq n) a) (cS (cS c0))) % 244.13/244.59 Found ((eq_ref n) a) as proof of (((eq n) a) (cS (cS c0))) % 244.13/244.59 Found ((eq_ref n) a) as proof of (((eq n) a) (cS (cS c0))) % 244.13/244.59 Found ((eq_ref n) a) as proof of (((eq n) a) (cS (cS c0))) % 244.13/244.59 Found x00:(P ((c_plus (cS (cS c0))) (cS (cS c0)))) % 244.13/244.59 Found (fun (x00:(P ((c_plus (cS (cS c0))) (cS (cS c0)))))=> x00) as proof of (P ((c_plus (cS (cS c0))) (cS (cS c0)))) % 244.13/244.59 Found (fun (x00:(P ((c_plus (cS (cS c0))) (cS (cS c0)))))=> x00) as proof of (P0 ((c_plus (cS (cS c0))) (cS (cS c0)))) % 244.13/244.59 Found eq_ref00:=(eq_ref0 b):(((eq n) b) b) % 244.13/244.59 Found (eq_ref0 b) as proof of (((eq n) b) ((c_star (cS (cS c0))) (cS (cS c0)))) % 297.99/298.46 Found ((eq_ref n) b) as proof of (((eq n) b) ((c_star (cS (cS c0))) (cS (cS c0)))) % 297.99/298.46 Found ((eq_ref n) b) as proof of (((eq n) b) ((c_star (cS (cS c0))) (cS (cS c0)))) % 297.99/298.46 Found ((eq_ref n) b) as proof of (((eq n) b) ((c_star (cS (cS c0))) (cS (cS c0)))) % 297.99/298.46 Found eq_ref00:=(eq_ref0 ((c_plus (cS (cS c0))) (cS (cS c0)))):(((eq n) ((c_plus (cS (cS c0))) (cS (cS c0)))) ((c_plus (cS (cS c0))) (cS (cS c0)))) % 297.99/298.46 Found (eq_ref0 ((c_plus (cS (cS c0))) (cS (cS c0)))) as proof of (((eq n) ((c_plus (cS (cS c0))) (cS (cS c0)))) b) % 297.99/298.46 Found ((eq_ref n) ((c_plus (cS (cS c0))) (cS (cS c0)))) as proof of (((eq n) ((c_plus (cS (cS c0))) (cS (cS c0)))) b) % 297.99/298.46 Found ((eq_ref n) ((c_plus (cS (cS c0))) (cS (cS c0)))) as proof of (((eq n) ((c_plus (cS (cS c0))) (cS (cS c0)))) b) % 297.99/298.46 Found ((eq_ref n) ((c_plus (cS (cS c0))) (cS (cS c0)))) as proof of (((eq n) ((c_plus (cS (cS c0))) (cS (cS c0)))) b) % 297.99/298.46 Found eq_ref00:=(eq_ref0 b):(((eq n) b) b) % 297.99/298.46 Found (eq_ref0 b) as proof of (((eq n) b) ((c_plus (cS (cS c0))) (cS (cS c0)))) % 297.99/298.46 Found ((eq_ref n) b) as proof of (((eq n) b) ((c_plus (cS (cS c0))) (cS (cS c0)))) % 297.99/298.46 Found ((eq_ref n) b) as proof of (((eq n) b) ((c_plus (cS (cS c0))) (cS (cS c0)))) % 297.99/298.46 Found ((eq_ref n) b) as proof of (((eq n) b) ((c_plus (cS (cS c0))) (cS (cS c0)))) % 297.99/298.46 Found x100:=(x10 (cS c0)):(((eq n) ((c_star (cS (cS c0))) (cS (cS c0)))) ((c_plus ((c_star (cS (cS c0))) (cS c0))) (cS (cS c0)))) % 297.99/298.46 Found (x10 (cS c0)) as proof of (((eq n) ((c_star (cS (cS c0))) (cS (cS c0)))) b) % 297.99/298.46 Found ((x1 (cS (cS c0))) (cS c0)) as proof of (((eq n) ((c_star (cS (cS c0))) (cS (cS c0)))) b) % 297.99/298.46 Found ((x1 (cS (cS c0))) (cS c0)) as proof of (((eq n) ((c_star (cS (cS c0))) (cS (cS c0)))) b) % 297.99/298.46 Found ((x1 (cS (cS c0))) (cS c0)) as proof of (((eq n) ((c_star (cS (cS c0))) (cS (cS c0)))) b) % 297.99/298.46 Found eq_ref00:=(eq_ref0 b0):(((eq n) b0) b0) % 297.99/298.46 Found (eq_ref0 b0) as proof of (((eq n) b0) ((c_star (cS (cS c0))) (cS (cS c0)))) % 297.99/298.46 Found ((eq_ref n) b0) as proof of (((eq n) b0) ((c_star (cS (cS c0))) (cS (cS c0)))) % 297.99/298.46 Found ((eq_ref n) b0) as proof of (((eq n) b0) ((c_star (cS (cS c0))) (cS (cS c0)))) % 297.99/298.46 Found ((eq_ref n) b0) as proof of (((eq n) b0) ((c_star (cS (cS c0))) (cS (cS c0)))) % 297.99/298.46 Found eq_ref00:=(eq_ref0 ((c_plus (cS (cS c0))) (cS (cS c0)))):(((eq n) ((c_plus (cS (cS c0))) (cS (cS c0)))) ((c_plus (cS (cS c0))) (cS (cS c0)))) % 297.99/298.46 Found (eq_ref0 ((c_plus (cS (cS c0))) (cS (cS c0)))) as proof of (((eq n) ((c_plus (cS (cS c0))) (cS (cS c0)))) b0) % 297.99/298.46 Found ((eq_ref n) ((c_plus (cS (cS c0))) (cS (cS c0)))) as proof of (((eq n) ((c_plus (cS (cS c0))) (cS (cS c0)))) b0) % 297.99/298.46 Found ((eq_ref n) ((c_plus (cS (cS c0))) (cS (cS c0)))) as proof of (((eq n) ((c_plus (cS (cS c0))) (cS (cS c0)))) b0) % 297.99/298.46 Found ((eq_ref n) ((c_plus (cS (cS c0))) (cS (cS c0)))) as proof of (((eq n) ((c_plus (cS (cS c0))) (cS (cS c0)))) b0) % 297.99/298.46 Found eq_ref00:=(eq_ref0 b0):(((eq n) b0) b0) % 297.99/298.46 Found (eq_ref0 b0) as proof of (((eq n) b0) ((c_plus (cS (cS c0))) (cS (cS c0)))) % 297.99/298.46 Found ((eq_ref n) b0) as proof of (((eq n) b0) ((c_plus (cS (cS c0))) (cS (cS c0)))) % 297.99/298.46 Found ((eq_ref n) b0) as proof of (((eq n) b0) ((c_plus (cS (cS c0))) (cS (cS c0)))) % 297.99/298.46 Found ((eq_ref n) b0) as proof of (((eq n) b0) ((c_plus (cS (cS c0))) (cS (cS c0)))) % 297.99/298.46 Found x100:=(x10 (cS c0)):(((eq n) ((c_star (cS (cS c0))) (cS (cS c0)))) ((c_plus ((c_star (cS (cS c0))) (cS c0))) (cS (cS c0)))) % 297.99/298.46 Found (x10 (cS c0)) as proof of (((eq n) ((c_star (cS (cS c0))) (cS (cS c0)))) b0) % 297.99/298.46 Found ((x1 (cS (cS c0))) (cS c0)) as proof of (((eq n) ((c_star (cS (cS c0))) (cS (cS c0)))) b0) % 297.99/298.46 Found ((x1 (cS (cS c0))) (cS c0)) as proof of (((eq n) ((c_star (cS (cS c0))) (cS (cS c0)))) b0) % 297.99/298.46 Found ((x1 (cS (cS c0))) (cS c0)) as proof of (((eq n) ((c_star (cS (cS c0))) (cS (cS c0)))) b0) % 297.99/298.46 Found eq_ref00:=(eq_ref0 a):(((eq n) a) a) % 297.99/298.46 Found (eq_ref0 a) as proof of (((eq n) a) (cS (cS c0))) % 297.99/298.46 Found ((eq_ref n) a) as proof of (((eq n) a) (cS (cS c0))) % 297.99/298.46 Found ((eq_ref n) a) as proof of (((eq n) a) (cS (cS c0))) % 297.99/298.46 Found ((eq_ref n) a) as proof of (((eq n) a) (cS (cS c0))) % 297.99/298.46 Found eq_ref00:=(eq_ref0 a):(((eq n) a) a) % 297.99/298.46 Found (eq_ref0 a) as proof of (((eq n) a) (cS (cS c0))) % 297.99/298.46 Found ((eq_ref n %------------------------------------------------------------------------------