%------------------------------------------------------------------------------ % File : cocATP---0.2.0 % Problem : DAT056^2 : TPTP v6.1.0. Released v5.4.0. % Transfm : none % Format : tptp:raw % Command : python CASC.py /export/starexec/sandbox/benchmark/theBenchmark.p % Computer : n096.star.cs.uiowa.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2609 0 2.40GHz % Memory : 32286.75MB % OS : Linux 2.6.32-431.20.3.el6.x86_64 % CPULimit : 300s % DateTime : Thu Jul 17 13:21:12 EDT 2014 % Result : Theorem 181.25s % Output : Proof 181.25s % Verified : % SZS Type : None (Parsing solution fails) % Syntax : Number of formulae : 0 % Comments : %------------------------------------------------------------------------------ %----ERROR: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % % Problem : DAT056^2 : TPTP v6.1.0. Released v5.4.0. % % Command : python CASC.py /export/starexec/sandbox/benchmark/theBenchmark.p % % Computer : n096.star.cs.uiowa.edu % % Model : x86_64 x86_64 % % CPU : Intel(R) Xeon(R) CPU E5-2609 0 @ 2.40GHz % % Memory : 32286.75MB % % OS : Linux 2.6.32-431.20.3.el6.x86_64 % % CPULimit : 300 % % DateTime : Thu Jul 17 07:47:26 CDT 2014 % % CPUTime : 181.25 % Python 2.7.5 % Using paths ['/home/cristobal/cocATP/CASC/TPTP/', '/export/starexec/sandbox/benchmark/', '/export/starexec/sandbox/benchmark/'] % FOF formula (<kernel.Constant object at 0x2177200>, <kernel.Type object at 0x2158560>) of role type named ty_n_tc__Foo__Olst_It__J % Using role type % Declaring lst:Type % FOF formula (<kernel.Constant object at 0x2177998>, <kernel.Type object at 0x2158368>) of role type named ty_n_t_ % Using role type % Declaring a:Type % FOF formula (<kernel.Constant object at 0x2177dd0>, <kernel.DependentProduct object at 0x2158440>) of role type named sy_c_Foo_Oap_001t_ % Using role type % Declaring ap:(lst->(lst->lst)) % FOF formula (<kernel.Constant object at 0x2177998>, <kernel.DependentProduct object at 0x21580e0>) of role type named sy_c_Foo_Olst_OCns_001t_ % Using role type % Declaring cns:(a->(lst->lst)) % FOF formula (<kernel.Constant object at 0x2177200>, <kernel.Constant object at 0x21580e0>) of role type named sy_c_Foo_Olst_ONl_001t_ % Using role type % Declaring nl:lst % FOF formula (<kernel.Constant object at 0x2177200>, <kernel.Constant object at 0x21580e0>) of role type named sy_v_xs % Using role type % Declaring xs:lst % FOF formula (forall (Lst:lst) (P:(lst->Prop)), ((P nl)->((forall (A:a) (Lst2:lst), ((P Lst2)->(P ((cns A) Lst2))))->(P Lst)))) of role axiom named fact_0_lst_Oinduct % A new axiom: (forall (Lst:lst) (P:(lst->Prop)), ((P nl)->((forall (A:a) (Lst2:lst), ((P Lst2)->(P ((cns A) Lst2))))->(P Lst)))) % FOF formula (forall (Ys2:lst) (Xs:lst) (X:a), (((eq lst) ((ap ((cns X) Xs)) Ys2)) ((cns X) ((ap Xs) Ys2)))) of role axiom named fact_1p_Osimps_I2_J % A new axiom: (forall (Ys2:lst) (Xs:lst) (X:a), (((eq lst) ((ap ((cns X) Xs)) Ys2)) ((cns X) ((ap Xs) Ys2)))) % FOF formula (forall (Ys2:lst), (((eq lst) ((ap nl) Ys2)) Ys2)) of role axiom named fact_2p_Osimps_I1_J % A new axiom: (forall (Ys2:lst), (((eq lst) ((ap nl) Ys2)) Ys2)) % FOF formula (forall (Ys:lst) (Zs:lst), (((eq lst) ((ap xs) ((ap Ys) Zs))) ((ap ((ap xs) Ys)) Zs))) of role conjecture named conj_0 % Conjecture to prove = (forall (Ys:lst) (Zs:lst), (((eq lst) ((ap xs) ((ap Ys) Zs))) ((ap ((ap xs) Ys)) Zs))):Prop % Parameter a_DUMMY:a. % We need to prove ['(forall (Ys:lst) (Zs:lst), (((eq lst) ((ap xs) ((ap Ys) Zs))) ((ap ((ap xs) Ys)) Zs)))'] % Parameter lst:Type. % Parameter a:Type. % Parameter ap:(lst->(lst->lst)). % Parameter cns:(a->(lst->lst)). % Parameter nl:lst. % Parameter xs:lst. % Axiom fact_0_lst_Oinduct:(forall (Lst:lst) (P:(lst->Prop)), ((P nl)->((forall (A:a) (Lst2:lst), ((P Lst2)->(P ((cns A) Lst2))))->(P Lst)))). % Axiom fact_1p_Osimps_I2_J:(forall (Ys2:lst) (Xs:lst) (X:a), (((eq lst) ((ap ((cns X) Xs)) Ys2)) ((cns X) ((ap Xs) Ys2)))). % Axiom fact_2p_Osimps_I1_J:(forall (Ys2:lst), (((eq lst) ((ap nl) Ys2)) Ys2)). % Trying to prove (forall (Ys:lst) (Zs:lst), (((eq lst) ((ap xs) ((ap Ys) Zs))) ((ap ((ap xs) Ys)) Zs))) % Found eq_ref000:=(eq_ref00 P):((P ((ap xs) ((ap Ys) Zs)))->(P ((ap xs) ((ap Ys) Zs)))) % Found (eq_ref00 P) as proof of (P0 ((ap xs) ((ap Ys) Zs))) % Found ((eq_ref0 ((ap xs) ((ap Ys) Zs))) P) as proof of (P0 ((ap xs) ((ap Ys) Zs))) % Found (((eq_ref lst) ((ap xs) ((ap Ys) Zs))) P) as proof of (P0 ((ap xs) ((ap Ys) Zs))) % Found (((eq_ref lst) ((ap xs) ((ap Ys) Zs))) P) as proof of (P0 ((ap xs) ((ap Ys) Zs))) % Found eq_ref00:=(eq_ref0 ((ap xs) ((ap Ys) Zs))):(((eq lst) ((ap xs) ((ap Ys) Zs))) ((ap xs) ((ap Ys) Zs))) % Found (eq_ref0 ((ap xs) ((ap Ys) Zs))) as proof of (((eq lst) ((ap xs) ((ap Ys) Zs))) b) % Found ((eq_ref lst) ((ap xs) ((ap Ys) Zs))) as proof of (((eq lst) ((ap xs) ((ap Ys) Zs))) b) % Found ((eq_ref lst) ((ap xs) ((ap Ys) Zs))) as proof of (((eq lst) ((ap xs) ((ap Ys) Zs))) b) % Found ((eq_ref lst) ((ap xs) ((ap Ys) Zs))) as proof of (((eq lst) ((ap xs) ((ap Ys) Zs))) b) % Found eq_ref00:=(eq_ref0 b):(((eq lst) b) b) % Found (eq_ref0 b) as proof of (((eq lst) b) ((ap ((ap xs) Ys)) Zs)) % Found ((eq_ref lst) b) as proof of (((eq lst) b) ((ap ((ap xs) Ys)) Zs)) % Found ((eq_ref lst) b) as proof of (((eq lst) b) ((ap ((ap xs) Ys)) Zs)) % Found ((eq_ref lst) b) as proof of (((eq lst) b) ((ap ((ap xs) Ys)) Zs)) % Found eq_ref00:=(eq_ref0 b):(((eq lst) b) b) % Found (eq_ref0 b) as proof of (((eq lst) b) ((ap xs) ((ap Ys) Zs))) % Found ((eq_ref lst) b) as proof of (((eq lst) b) ((ap xs) ((ap Ys) Zs))) % Found ((eq_ref lst) b) as proof of (((eq lst) b) ((ap xs) ((ap Ys) Zs))) % Found ((eq_ref lst) b) as proof of (((eq lst) b) ((ap xs) ((ap Ys) Zs))) % Found eq_ref00:=(eq_ref0 ((ap ((ap xs) Ys)) Zs)):(((eq lst) ((ap ((ap xs) Ys)) Zs)) ((ap ((ap xs) Ys)) Zs)) % Found (eq_ref0 ((ap ((ap xs) Ys)) Zs)) as proof of (((eq lst) ((ap ((ap xs) Ys)) Zs)) b) % Found ((eq_ref lst) ((ap ((ap xs) Ys)) Zs)) as proof of (((eq lst) ((ap ((ap xs) Ys)) Zs)) b) % Found ((eq_ref lst) ((ap ((ap xs) Ys)) Zs)) as proof of (((eq lst) ((ap ((ap xs) Ys)) Zs)) b) % Found ((eq_ref lst) ((ap ((ap xs) Ys)) Zs)) as proof of (((eq lst) ((ap ((ap xs) Ys)) Zs)) b) % Found fact_2p_Osimps_I1_J__eq_sym1:=(fact_2p_Osimps_I1_J__eq_sym ((ap Ys) Zs)):(((eq lst) ((ap Ys) Zs)) ((ap nl) ((ap Ys) Zs))) % Found (fact_2p_Osimps_I1_J__eq_sym ((ap Ys) Zs)) as proof of (((eq lst) ((ap Ys) Zs)) ((ap nl) ((ap Ys) Zs))) % Found (fact_2p_Osimps_I1_J__eq_sym ((ap Ys) Zs)) as proof of (((eq lst) ((ap Ys) Zs)) ((ap nl) ((ap Ys) Zs))) % Found (fact_2p_Osimps_I1_J__eq_sym00 (fact_2p_Osimps_I1_J__eq_sym ((ap Ys) Zs))) as proof of (((eq lst) ((ap ((ap nl) Ys)) Zs)) ((ap nl) ((ap Ys) Zs))) % Found ((fact_2p_Osimps_I1_J__eq_sym0 (fun (x0:lst)=> (((eq lst) ((ap x0) Zs)) ((ap nl) ((ap Ys) Zs))))) (fact_2p_Osimps_I1_J__eq_sym ((ap Ys) Zs))) as proof of (((eq lst) ((ap ((ap nl) Ys)) Zs)) ((ap nl) ((ap Ys) Zs))) % Found (((fact_2p_Osimps_I1_J__eq_sym Ys) (fun (x0:lst)=> (((eq lst) ((ap x0) Zs)) ((ap nl) ((ap Ys) Zs))))) (fact_2p_Osimps_I1_J__eq_sym ((ap Ys) Zs))) as proof of (((eq lst) ((ap ((ap nl) Ys)) Zs)) ((ap nl) ((ap Ys) Zs))) % Found (((fact_2p_Osimps_I1_J__eq_sym Ys) (fun (x0:lst)=> (((eq lst) ((ap x0) Zs)) ((ap nl) ((ap Ys) Zs))))) (fact_2p_Osimps_I1_J__eq_sym ((ap Ys) Zs))) as proof of (((eq lst) ((ap ((ap nl) Ys)) Zs)) ((ap nl) ((ap Ys) Zs))) % Found x0:=(x (fun (x0:lst)=> (P ((ap ((ap ((cns A) Lst2)) Ys)) Zs)))):((P ((ap ((ap ((cns A) Lst2)) Ys)) Zs))->(P ((ap ((ap ((cns A) Lst2)) Ys)) Zs))) % Found (x (fun (x0:lst)=> (P ((ap ((ap ((cns A) Lst2)) Ys)) Zs)))) as proof of (P0 ((ap ((ap ((cns A) Lst2)) Ys)) Zs)) % Found (x (fun (x0:lst)=> (P ((ap ((ap ((cns A) Lst2)) Ys)) Zs)))) as proof of (P0 ((ap ((ap ((cns A) Lst2)) Ys)) Zs)) % Found eq_ref000:=(eq_ref00 P):((P ((ap xs) ((ap Ys) nl)))->(P ((ap xs) ((ap Ys) nl)))) % Found (eq_ref00 P) as proof of (P0 ((ap xs) ((ap Ys) nl))) % Found ((eq_ref0 ((ap xs) ((ap Ys) nl))) P) as proof of (P0 ((ap xs) ((ap Ys) nl))) % Found (((eq_ref lst) ((ap xs) ((ap Ys) nl))) P) as proof of (P0 ((ap xs) ((ap Ys) nl))) % Found (((eq_ref lst) ((ap xs) ((ap Ys) nl))) P) as proof of (P0 ((ap xs) ((ap Ys) nl))) % Found fact_2p_Osimps_I1_J__eq_sym1:=(fact_2p_Osimps_I1_J__eq_sym ((ap Ys) Zs)):(((eq lst) ((ap Ys) Zs)) ((ap nl) ((ap Ys) Zs))) % Found (fact_2p_Osimps_I1_J__eq_sym ((ap Ys) Zs)) as proof of (((eq lst) ((ap Ys) Zs)) ((ap nl) ((ap Ys) Zs))) % Found (fact_2p_Osimps_I1_J__eq_sym ((ap Ys) Zs)) as proof of (((eq lst) ((ap Ys) Zs)) ((ap nl) ((ap Ys) Zs))) % Found (fact_2p_Osimps_I1_J__eq_sym00 (fact_2p_Osimps_I1_J__eq_sym ((ap Ys) Zs))) as proof of (((eq lst) ((ap ((ap nl) Ys)) Zs)) ((ap nl) ((ap Ys) Zs))) % Found ((fact_2p_Osimps_I1_J__eq_sym0 (fun (x0:lst)=> (((eq lst) ((ap x0) Zs)) ((ap nl) ((ap Ys) Zs))))) (fact_2p_Osimps_I1_J__eq_sym ((ap Ys) Zs))) as proof of (((eq lst) ((ap ((ap nl) Ys)) Zs)) ((ap nl) ((ap Ys) Zs))) % Found (((fact_2p_Osimps_I1_J__eq_sym Ys) (fun (x0:lst)=> (((eq lst) ((ap x0) Zs)) ((ap nl) ((ap Ys) Zs))))) (fact_2p_Osimps_I1_J__eq_sym ((ap Ys) Zs))) as proof of (((eq lst) ((ap ((ap nl) Ys)) Zs)) ((ap nl) ((ap Ys) Zs))) % Found (((fact_2p_Osimps_I1_J__eq_sym Ys) (fun (x0:lst)=> (((eq lst) ((ap x0) Zs)) ((ap nl) ((ap Ys) Zs))))) (fact_2p_Osimps_I1_J__eq_sym ((ap Ys) Zs))) as proof of (((eq lst) ((ap ((ap nl) Ys)) Zs)) ((ap nl) ((ap Ys) Zs))) % Found (eq_sym000 (((fact_2p_Osimps_I1_J__eq_sym Ys) (fun (x0:lst)=> (((eq lst) ((ap x0) Zs)) ((ap nl) ((ap Ys) Zs))))) (fact_2p_Osimps_I1_J__eq_sym ((ap Ys) Zs)))) as proof of (((eq lst) ((ap nl) ((ap Ys) Zs))) ((ap ((ap nl) Ys)) Zs)) % Found ((eq_sym00 ((ap nl) ((ap Ys) Zs))) (((fact_2p_Osimps_I1_J__eq_sym Ys) (fun (x0:lst)=> (((eq lst) ((ap x0) Zs)) ((ap nl) ((ap Ys) Zs))))) (fact_2p_Osimps_I1_J__eq_sym ((ap Ys) Zs)))) as proof of (((eq lst) ((ap nl) ((ap Ys) Zs))) ((ap ((ap nl) Ys)) Zs)) % Found (((eq_sym0 ((ap ((ap nl) Ys)) Zs)) ((ap nl) ((ap Ys) Zs))) (((fact_2p_Osimps_I1_J__eq_sym Ys) (fun (x0:lst)=> (((eq lst) ((ap x0) Zs)) ((ap nl) ((ap Ys) Zs))))) (fact_2p_Osimps_I1_J__eq_sym ((ap Ys) Zs)))) as proof of (((eq lst) ((ap nl) ((ap Ys) Zs))) ((ap ((ap nl) Ys)) Zs)) % Found ((((eq_sym lst) ((ap ((ap nl) Ys)) Zs)) ((ap nl) ((ap Ys) Zs))) (((fact_2p_Osimps_I1_J__eq_sym Ys) (fun (x0:lst)=> (((eq lst) ((ap x0) Zs)) ((ap nl) ((ap Ys) Zs))))) (fact_2p_Osimps_I1_J__eq_sym ((ap Ys) Zs)))) as proof of (((eq lst) ((ap nl) ((ap Ys) Zs))) ((ap ((ap nl) Ys)) Zs)) % Found ((((eq_sym lst) ((ap ((ap nl) Ys)) Zs)) ((ap nl) ((ap Ys) Zs))) (((fact_2p_Osimps_I1_J__eq_sym Ys) (fun (x0:lst)=> (((eq lst) ((ap x0) Zs)) ((ap nl) ((ap Ys) Zs))))) (fact_2p_Osimps_I1_J__eq_sym ((ap Ys) Zs)))) as proof of (((eq lst) ((ap nl) ((ap Ys) Zs))) ((ap ((ap nl) Ys)) Zs)) % Found x0:=(x (fun (x0:lst)=> (P ((ap ((cns A) Lst2)) ((ap Ys) Zs))))):((P ((ap ((cns A) Lst2)) ((ap Ys) Zs)))->(P ((ap ((cns A) Lst2)) ((ap Ys) Zs)))) % Found (x (fun (x0:lst)=> (P ((ap ((cns A) Lst2)) ((ap Ys) Zs))))) as proof of (P0 ((ap ((cns A) Lst2)) ((ap Ys) Zs))) % Found (x (fun (x0:lst)=> (P ((ap ((cns A) Lst2)) ((ap Ys) Zs))))) as proof of (P0 ((ap ((cns A) Lst2)) ((ap Ys) Zs))) % Found fact_1p_Osimps_I2_J000:=(fact_1p_Osimps_I2_J00 A):(((eq lst) ((ap ((cns A) Lst2)) ((ap Ys) Zs))) ((cns A) ((ap Lst2) ((ap Ys) Zs)))) % Found (fact_1p_Osimps_I2_J00 A) as proof of (((eq lst) ((ap ((cns A) Lst2)) ((ap Ys) Zs))) b) % Found ((fact_1p_Osimps_I2_J0 Lst2) A) as proof of (((eq lst) ((ap ((cns A) Lst2)) ((ap Ys) Zs))) b) % Found (((fact_1p_Osimps_I2_J ((ap Ys) Zs)) Lst2) A) as proof of (((eq lst) ((ap ((cns A) Lst2)) ((ap Ys) Zs))) b) % Found (((fact_1p_Osimps_I2_J ((ap Ys) Zs)) Lst2) A) as proof of (((eq lst) ((ap ((cns A) Lst2)) ((ap Ys) Zs))) b) % Found (((fact_1p_Osimps_I2_J ((ap Ys) Zs)) Lst2) A) as proof of (((eq lst) ((ap ((cns A) Lst2)) ((ap Ys) Zs))) b) % Found eq_ref00:=(eq_ref0 b):(((eq lst) b) b) % Found (eq_ref0 b) as proof of (((eq lst) b) ((ap ((ap ((cns A) Lst2)) Ys)) Zs)) % Found ((eq_ref lst) b) as proof of (((eq lst) b) ((ap ((ap ((cns A) Lst2)) Ys)) Zs)) % Found ((eq_ref lst) b) as proof of (((eq lst) b) ((ap ((ap ((cns A) Lst2)) Ys)) Zs)) % Found ((eq_ref lst) b) as proof of (((eq lst) b) ((ap ((ap ((cns A) Lst2)) Ys)) Zs)) % Found eq_ref000:=(eq_ref00 P):((P ((ap xs) ((ap nl) Zs)))->(P ((ap xs) ((ap nl) Zs)))) % Found (eq_ref00 P) as proof of (P0 ((ap xs) ((ap nl) Zs))) % Found ((eq_ref0 ((ap xs) ((ap nl) Zs))) P) as proof of (P0 ((ap xs) ((ap nl) Zs))) % Found (((eq_ref lst) ((ap xs) ((ap nl) Zs))) P) as proof of (P0 ((ap xs) ((ap nl) Zs))) % Found (((eq_ref lst) ((ap xs) ((ap nl) Zs))) P) as proof of (P0 ((ap xs) ((ap nl) Zs))) % Found eq_ref000:=(eq_ref00 P):((P ((cns A) ((ap Lst2) ((ap Ys) Zs))))->(P ((cns A) ((ap Lst2) ((ap Ys) Zs))))) % Found (eq_ref00 P) as proof of (P0 ((cns A) ((ap Lst2) ((ap Ys) Zs)))) % Found ((eq_ref0 ((cns A) ((ap Lst2) ((ap Ys) Zs)))) P) as proof of (P0 ((cns A) ((ap Lst2) ((ap Ys) Zs)))) % Found (((eq_ref lst) ((cns A) ((ap Lst2) ((ap Ys) Zs)))) P) as proof of (P0 ((cns A) ((ap Lst2) ((ap Ys) Zs)))) % Found (((eq_ref lst) ((cns A) ((ap Lst2) ((ap Ys) Zs)))) P) as proof of (P0 ((cns A) ((ap Lst2) ((ap Ys) Zs)))) % Found eq_ref00:=(eq_ref0 ((ap xs) ((ap Ys) nl))):(((eq lst) ((ap xs) ((ap Ys) nl))) ((ap xs) ((ap Ys) nl))) % Found (eq_ref0 ((ap xs) ((ap Ys) nl))) as proof of (((eq lst) ((ap xs) ((ap Ys) nl))) b) % Found ((eq_ref lst) ((ap xs) ((ap Ys) nl))) as proof of (((eq lst) ((ap xs) ((ap Ys) nl))) b) % Found ((eq_ref lst) ((ap xs) ((ap Ys) nl))) as proof of (((eq lst) ((ap xs) ((ap Ys) nl))) b) % Found ((eq_ref lst) ((ap xs) ((ap Ys) nl))) as proof of (((eq lst) ((ap xs) ((ap Ys) nl))) b) % Found eq_ref00:=(eq_ref0 b):(((eq lst) b) b) % Found (eq_ref0 b) as proof of (((eq lst) b) ((ap ((ap xs) Ys)) nl)) % Found ((eq_ref lst) b) as proof of (((eq lst) b) ((ap ((ap xs) Ys)) nl)) % Found ((eq_ref lst) b) as proof of (((eq lst) b) ((ap ((ap xs) Ys)) nl)) % Found ((eq_ref lst) b) as proof of (((eq lst) b) ((ap ((ap xs) Ys)) nl)) % Found eq_ref00:=(eq_ref0 ((ap xs) ((ap nl) Zs))):(((eq lst) ((ap xs) ((ap nl) Zs))) ((ap xs) ((ap nl) Zs))) % Found (eq_ref0 ((ap xs) ((ap nl) Zs))) as proof of (((eq lst) ((ap xs) ((ap nl) Zs))) b) % Found ((eq_ref lst) ((ap xs) ((ap nl) Zs))) as proof of (((eq lst) ((ap xs) ((ap nl) Zs))) b) % Found ((eq_ref lst) ((ap xs) ((ap nl) Zs))) as proof of (((eq lst) ((ap xs) ((ap nl) Zs))) b) % Found ((eq_ref lst) ((ap xs) ((ap nl) Zs))) as proof of (((eq lst) ((ap xs) ((ap nl) Zs))) b) % Found eq_ref00:=(eq_ref0 b):(((eq lst) b) b) % Found (eq_ref0 b) as proof of (((eq lst) b) ((ap ((ap xs) nl)) Zs)) % Found ((eq_ref lst) b) as proof of (((eq lst) b) ((ap ((ap xs) nl)) Zs)) % Found ((eq_ref lst) b) as proof of (((eq lst) b) ((ap ((ap xs) nl)) Zs)) % Found ((eq_ref lst) b) as proof of (((eq lst) b) ((ap ((ap xs) nl)) Zs)) % Found eq_ref00:=(eq_ref0 b):(((eq lst) b) b) % Found (eq_ref0 b) as proof of (((eq lst) b) ((ap ((cns A) Lst2)) ((ap Ys) Zs))) % Found ((eq_ref lst) b) as proof of (((eq lst) b) ((ap ((cns A) Lst2)) ((ap Ys) Zs))) % Found ((eq_ref lst) b) as proof of (((eq lst) b) ((ap ((cns A) Lst2)) ((ap Ys) Zs))) % Found ((eq_ref lst) b) as proof of (((eq lst) b) ((ap ((cns A) Lst2)) ((ap Ys) Zs))) % Found eq_ref00:=(eq_ref0 ((ap ((ap ((cns A) Lst2)) Ys)) Zs)):(((eq lst) ((ap ((ap ((cns A) Lst2)) Ys)) Zs)) ((ap ((ap ((cns A) Lst2)) Ys)) Zs)) % Found (eq_ref0 ((ap ((ap ((cns A) Lst2)) Ys)) Zs)) as proof of (((eq lst) ((ap ((ap ((cns A) Lst2)) Ys)) Zs)) b) % Found ((eq_ref lst) ((ap ((ap ((cns A) Lst2)) Ys)) Zs)) as proof of (((eq lst) ((ap ((ap ((cns A) Lst2)) Ys)) Zs)) b) % Found ((eq_ref lst) ((ap ((ap ((cns A) Lst2)) Ys)) Zs)) as proof of (((eq lst) ((ap ((ap ((cns A) Lst2)) Ys)) Zs)) b) % Found ((eq_ref lst) ((ap ((ap ((cns A) Lst2)) Ys)) Zs)) as proof of (((eq lst) ((ap ((ap ((cns A) Lst2)) Ys)) Zs)) b) % Found fact_2p_Osimps_I1_J__eq_sym1:=(fact_2p_Osimps_I1_J__eq_sym ((ap Ys) Zs)):(((eq lst) ((ap Ys) Zs)) ((ap nl) ((ap Ys) Zs))) % Found (fact_2p_Osimps_I1_J__eq_sym ((ap Ys) Zs)) as proof of (((eq lst) ((ap Ys) Zs)) ((ap nl) ((ap Ys) Zs))) % Found (fact_2p_Osimps_I1_J__eq_sym ((ap Ys) Zs)) as proof of (((eq lst) ((ap Ys) Zs)) ((ap nl) ((ap Ys) Zs))) % Found (fact_2p_Osimps_I1_J__eq_sym00 (fact_2p_Osimps_I1_J__eq_sym ((ap Ys) Zs))) as proof of (((eq lst) ((ap ((ap nl) Ys)) Zs)) ((ap nl) ((ap Ys) Zs))) % Found ((fact_2p_Osimps_I1_J__eq_sym0 (fun (x0:lst)=> (((eq lst) ((ap x0) Zs)) ((ap nl) ((ap Ys) Zs))))) (fact_2p_Osimps_I1_J__eq_sym ((ap Ys) Zs))) as proof of (((eq lst) ((ap ((ap nl) Ys)) Zs)) ((ap nl) ((ap Ys) Zs))) % Found (((fact_2p_Osimps_I1_J__eq_sym Ys) (fun (x0:lst)=> (((eq lst) ((ap x0) Zs)) ((ap nl) ((ap Ys) Zs))))) (fact_2p_Osimps_I1_J__eq_sym ((ap Ys) Zs))) as proof of (((eq lst) ((ap ((ap nl) Ys)) Zs)) ((ap nl) ((ap Ys) Zs))) % Found (((fact_2p_Osimps_I1_J__eq_sym Ys) (fun (x0:lst)=> (((eq lst) ((ap x0) Zs)) ((ap nl) ((ap Ys) Zs))))) (fact_2p_Osimps_I1_J__eq_sym ((ap Ys) Zs))) as proof of (((eq lst) ((ap ((ap nl) Ys)) Zs)) ((ap nl) ((ap Ys) Zs))) % Found fact_2p_Osimps_I1_J__eq_sym1:=(fact_2p_Osimps_I1_J__eq_sym ((ap Ys) Zs)):(((eq lst) ((ap Ys) Zs)) ((ap nl) ((ap Ys) Zs))) % Found (fact_2p_Osimps_I1_J__eq_sym ((ap Ys) Zs)) as proof of (((eq lst) ((ap Ys) Zs)) ((ap nl) ((ap Ys) Zs))) % Found (fact_2p_Osimps_I1_J__eq_sym ((ap Ys) Zs)) as proof of (((eq lst) ((ap Ys) Zs)) ((ap nl) ((ap Ys) Zs))) % Found (fact_2p_Osimps_I1_J__eq_sym00 (fact_2p_Osimps_I1_J__eq_sym ((ap Ys) Zs))) as proof of (((eq lst) ((ap ((ap nl) Ys)) Zs)) ((ap nl) ((ap Ys) Zs))) % Found ((fact_2p_Osimps_I1_J__eq_sym0 (fun (x0:lst)=> (((eq lst) ((ap x0) Zs)) ((ap nl) ((ap Ys) Zs))))) (fact_2p_Osimps_I1_J__eq_sym ((ap Ys) Zs))) as proof of (((eq lst) ((ap ((ap nl) Ys)) Zs)) ((ap nl) ((ap Ys) Zs))) % Found (((fact_2p_Osimps_I1_J__eq_sym Ys) (fun (x0:lst)=> (((eq lst) ((ap x0) Zs)) ((ap nl) ((ap Ys) Zs))))) (fact_2p_Osimps_I1_J__eq_sym ((ap Ys) Zs))) as proof of (((eq lst) ((ap ((ap nl) Ys)) Zs)) ((ap nl) ((ap Ys) Zs))) % Found (((fact_2p_Osimps_I1_J__eq_sym Ys) (fun (x0:lst)=> (((eq lst) ((ap x0) Zs)) ((ap nl) ((ap Ys) Zs))))) (fact_2p_Osimps_I1_J__eq_sym ((ap Ys) Zs))) as proof of (((eq lst) ((ap ((ap nl) Ys)) Zs)) ((ap nl) ((ap Ys) Zs))) % Found eq_ref000:=(eq_ref00 P):((P ((ap ((ap xs) Ys)) Lst2))->(P ((ap ((ap xs) Ys)) Lst2))) % Found (eq_ref00 P) as proof of (P0 ((ap ((ap xs) Ys)) Lst2)) % Found ((eq_ref0 ((ap ((ap xs) Ys)) Lst2)) P) as proof of (P0 ((ap ((ap xs) Ys)) Lst2)) % Found (((eq_ref lst) ((ap ((ap xs) Ys)) Lst2)) P) as proof of (P0 ((ap ((ap xs) Ys)) Lst2)) % Found (((eq_ref lst) ((ap ((ap xs) Ys)) Lst2)) P) as proof of (P0 ((ap ((ap xs) Ys)) Lst2)) % Found eq_ref000:=(eq_ref00 P):((P ((ap ((ap Lst2) Ys)) Zs))->(P ((ap ((ap Lst2) Ys)) Zs))) % Found (eq_ref00 P) as proof of (P0 ((ap ((ap Lst2) Ys)) Zs)) % Found ((eq_ref0 ((ap ((ap Lst2) Ys)) Zs)) P) as proof of (P0 ((ap ((ap Lst2) Ys)) Zs)) % Found (((eq_ref lst) ((ap ((ap Lst2) Ys)) Zs)) P) as proof of (P0 ((ap ((ap Lst2) Ys)) Zs)) % Found (((eq_ref lst) ((ap ((ap Lst2) Ys)) Zs)) P) as proof of (P0 ((ap ((ap Lst2) Ys)) Zs)) % Found eq_ref000:=(eq_ref00 P):((P ((ap ((ap xs) Lst2)) Zs))->(P ((ap ((ap xs) Lst2)) Zs))) % Found (eq_ref00 P) as proof of (P0 ((ap ((ap xs) Lst2)) Zs)) % Found ((eq_ref0 ((ap ((ap xs) Lst2)) Zs)) P) as proof of (P0 ((ap ((ap xs) Lst2)) Zs)) % Found (((eq_ref lst) ((ap ((ap xs) Lst2)) Zs)) P) as proof of (P0 ((ap ((ap xs) Lst2)) Zs)) % Found (((eq_ref lst) ((ap ((ap xs) Lst2)) Zs)) P) as proof of (P0 ((ap ((ap xs) Lst2)) Zs)) % Found eq_ref00:=(eq_ref0 b):(((eq lst) b) b) % Found (eq_ref0 b) as proof of (((eq lst) b) ((ap ((cns A) Lst2)) ((ap Ys) Zs))) % Found ((eq_ref lst) b) as proof of (((eq lst) b) ((ap ((cns A) Lst2)) ((ap Ys) Zs))) % Found ((eq_ref lst) b) as proof of (((eq lst) b) ((ap ((cns A) Lst2)) ((ap Ys) Zs))) % Found ((eq_ref lst) b) as proof of (((eq lst) b) ((ap ((cns A) Lst2)) ((ap Ys) Zs))) % Found eq_ref00:=(eq_ref0 ((ap ((ap ((cns A) Lst2)) Ys)) Zs)):(((eq lst) ((ap ((ap ((cns A) Lst2)) Ys)) Zs)) ((ap ((ap ((cns A) Lst2)) Ys)) Zs)) % Found (eq_ref0 ((ap ((ap ((cns A) Lst2)) Ys)) Zs)) as proof of (((eq lst) ((ap ((ap ((cns A) Lst2)) Ys)) Zs)) b) % Found ((eq_ref lst) ((ap ((ap ((cns A) Lst2)) Ys)) Zs)) as proof of (((eq lst) ((ap ((ap ((cns A) Lst2)) Ys)) Zs)) b) % Found ((eq_ref lst) ((ap ((ap ((cns A) Lst2)) Ys)) Zs)) as proof of (((eq lst) ((ap ((ap ((cns A) Lst2)) Ys)) Zs)) b) % Found ((eq_ref lst) ((ap ((ap ((cns A) Lst2)) Ys)) Zs)) as proof of (((eq lst) ((ap ((ap ((cns A) Lst2)) Ys)) Zs)) b) % Found x0:=(x (fun (x0:lst)=> (P ((ap xs) ((ap Ys) ((cns A) Lst2)))))):((P ((ap xs) ((ap Ys) ((cns A) Lst2))))->(P ((ap xs) ((ap Ys) ((cns A) Lst2))))) % Found (x (fun (x0:lst)=> (P ((ap xs) ((ap Ys) ((cns A) Lst2)))))) as proof of (P0 ((ap xs) ((ap Ys) ((cns A) Lst2)))) % Found (x (fun (x0:lst)=> (P ((ap xs) ((ap Ys) ((cns A) Lst2)))))) as proof of (P0 ((ap xs) ((ap Ys) ((cns A) Lst2)))) % Found x0:=(x (fun (x0:lst)=> (P ((ap xs) ((ap ((cns A) Lst2)) Zs))))):((P ((ap xs) ((ap ((cns A) Lst2)) Zs)))->(P ((ap xs) ((ap ((cns A) Lst2)) Zs)))) % Found (x (fun (x0:lst)=> (P ((ap xs) ((ap ((cns A) Lst2)) Zs))))) as proof of (P0 ((ap xs) ((ap ((cns A) Lst2)) Zs))) % Found (x (fun (x0:lst)=> (P ((ap xs) ((ap ((cns A) Lst2)) Zs))))) as proof of (P0 ((ap xs) ((ap ((cns A) Lst2)) Zs))) % Found eq_substitution00000:=(eq_substitution0000 (cns A)):((((eq lst) ((ap Lst2) ((ap Ys) Zs))) ((ap ((ap Lst2) Ys)) Zs))->(((eq lst) ((cns A) ((ap Lst2) ((ap Ys) Zs)))) ((cns A) ((ap ((ap Lst2) Ys)) Zs)))) % Found (eq_substitution0000 (cns A)) as proof of ((((eq lst) ((ap Lst2) ((ap Ys) Zs))) ((ap ((ap Lst2) Ys)) Zs))->(((eq lst) ((cns A) ((ap Lst2) ((ap Ys) Zs)))) ((cns A) ((ap ((ap Lst2) Ys)) Zs)))) % Found ((eq_substitution000 ((ap ((ap Lst2) Ys)) Zs)) (cns A)) as proof of ((((eq lst) ((ap Lst2) ((ap Ys) Zs))) ((ap ((ap Lst2) Ys)) Zs))->(((eq lst) ((cns A) ((ap Lst2) ((ap Ys) Zs)))) ((cns A) ((ap ((ap Lst2) Ys)) Zs)))) % Found (((eq_substitution00 ((ap Lst2) ((ap Ys) Zs))) ((ap ((ap Lst2) Ys)) Zs)) (cns A)) as proof of ((((eq lst) ((ap Lst2) ((ap Ys) Zs))) ((ap ((ap Lst2) Ys)) Zs))->(((eq lst) ((cns A) ((ap Lst2) ((ap Ys) Zs)))) ((cns A) ((ap ((ap Lst2) Ys)) Zs)))) % Found ((((eq_substitution0 lst) ((ap Lst2) ((ap Ys) Zs))) ((ap ((ap Lst2) Ys)) Zs)) (cns A)) as proof of ((((eq lst) ((ap Lst2) ((ap Ys) Zs))) ((ap ((ap Lst2) Ys)) Zs))->(((eq lst) ((cns A) ((ap Lst2) ((ap Ys) Zs)))) ((cns A) ((ap ((ap Lst2) Ys)) Zs)))) % Found (((((eq_substitution lst) lst) ((ap Lst2) ((ap Ys) Zs))) ((ap ((ap Lst2) Ys)) Zs)) (cns A)) as proof of ((((eq lst) ((ap Lst2) ((ap Ys) Zs))) ((ap ((ap Lst2) Ys)) Zs))->(((eq lst) ((cns A) ((ap Lst2) ((ap Ys) Zs)))) ((cns A) ((ap ((ap Lst2) Ys)) Zs)))) % Found (((((eq_substitution lst) lst) ((ap Lst2) ((ap Ys) Zs))) ((ap ((ap Lst2) Ys)) Zs)) (cns A)) as proof of ((((eq lst) ((ap Lst2) ((ap Ys) Zs))) ((ap ((ap Lst2) Ys)) Zs))->(((eq lst) ((cns A) ((ap Lst2) ((ap Ys) Zs)))) ((cns A) ((ap ((ap Lst2) Ys)) Zs)))) % Found (fact_1p_Osimps_I2_J__eq_sym2000 (((((eq_substitution lst) lst) ((ap Lst2) ((ap Ys) Zs))) ((ap ((ap Lst2) Ys)) Zs)) (cns A))) as proof of ((((eq lst) ((ap Lst2) ((ap Ys) Zs))) ((ap ((ap Lst2) Ys)) Zs))->(((eq lst) ((cns A) ((ap Lst2) ((ap Ys) Zs)))) ((ap ((cns A) ((ap Lst2) Ys))) Zs))) % Found ((fact_1p_Osimps_I2_J__eq_sym200 (fun (x0:lst)=> ((((eq lst) ((ap Lst2) ((ap Ys) Zs))) ((ap ((ap Lst2) Ys)) Zs))->(((eq lst) ((cns A) ((ap Lst2) ((ap Ys) Zs)))) x0)))) (((((eq_substitution lst) lst) ((ap Lst2) ((ap Ys) Zs))) ((ap ((ap Lst2) Ys)) Zs)) (cns A))) as proof of ((((eq lst) ((ap Lst2) ((ap Ys) Zs))) ((ap ((ap Lst2) Ys)) Zs))->(((eq lst) ((cns A) ((ap Lst2) ((ap Ys) Zs)))) ((ap ((cns A) ((ap Lst2) Ys))) Zs))) % Found (((fact_1p_Osimps_I2_J__eq_sym20 A) (fun (x0:lst)=> ((((eq lst) ((ap Lst2) ((ap Ys) Zs))) ((ap ((ap Lst2) Ys)) Zs))->(((eq lst) ((cns A) ((ap Lst2) ((ap Ys) Zs)))) x0)))) (((((eq_substitution lst) lst) ((ap Lst2) ((ap Ys) Zs))) ((ap ((ap Lst2) Ys)) Zs)) (cns A))) as proof of ((((eq lst) ((ap Lst2) ((ap Ys) Zs))) ((ap ((ap Lst2) Ys)) Zs))->(((eq lst) ((cns A) ((ap Lst2) ((ap Ys) Zs)))) ((ap ((cns A) ((ap Lst2) Ys))) Zs))) % Found ((((fact_1p_Osimps_I2_J__eq_sym2 ((ap Lst2) Ys)) A) (fun (x0:lst)=> ((((eq lst) ((ap Lst2) ((ap Ys) Zs))) ((ap ((ap Lst2) Ys)) Zs))->(((eq lst) ((cns A) ((ap Lst2) ((ap Ys) Zs)))) x0)))) (((((eq_substitution lst) lst) ((ap Lst2) ((ap Ys) Zs))) ((ap ((ap Lst2) Ys)) Zs)) (cns A))) as proof of ((((eq lst) ((ap Lst2) ((ap Ys) Zs))) ((ap ((ap Lst2) Ys)) Zs))->(((eq lst) ((cns A) ((ap Lst2) ((ap Ys) Zs)))) ((ap ((cns A) ((ap Lst2) Ys))) Zs))) % Found (((((fact_1p_Osimps_I2_J__eq_sym Zs) ((ap Lst2) Ys)) A) (fun (x0:lst)=> ((((eq lst) ((ap Lst2) ((ap Ys) Zs))) ((ap ((ap Lst2) Ys)) Zs))->(((eq lst) ((cns A) ((ap Lst2) ((ap Ys) Zs)))) x0)))) (((((eq_substitution lst) lst) ((ap Lst2) ((ap Ys) Zs))) ((ap ((ap Lst2) Ys)) Zs)) (cns A))) as proof of ((((eq lst) ((ap Lst2) ((ap Ys) Zs))) ((ap ((ap Lst2) Ys)) Zs))->(((eq lst) ((cns A) ((ap Lst2) ((ap Ys) Zs)))) ((ap ((cns A) ((ap Lst2) Ys))) Zs))) % Found (((((fact_1p_Osimps_I2_J__eq_sym Zs) ((ap Lst2) Ys)) A) (fun (x0:lst)=> ((((eq lst) ((ap Lst2) ((ap Ys) Zs))) ((ap ((ap Lst2) Ys)) Zs))->(((eq lst) ((cns A) ((ap Lst2) ((ap Ys) Zs)))) x0)))) (((((eq_substitution lst) lst) ((ap Lst2) ((ap Ys) Zs))) ((ap ((ap Lst2) Ys)) Zs)) (cns A))) as proof of ((((eq lst) ((ap Lst2) ((ap Ys) Zs))) ((ap ((ap Lst2) Ys)) Zs))->(((eq lst) ((cns A) ((ap Lst2) ((ap Ys) Zs)))) ((ap ((cns A) ((ap Lst2) Ys))) Zs))) % Found (fact_1p_Osimps_I2_J__eq_sym1000 (((((fact_1p_Osimps_I2_J__eq_sym Zs) ((ap Lst2) Ys)) A) (fun (x0:lst)=> ((((eq lst) ((ap Lst2) ((ap Ys) Zs))) ((ap ((ap Lst2) Ys)) Zs))->(((eq lst) ((cns A) ((ap Lst2) ((ap Ys) Zs)))) x0)))) (((((eq_substitution lst) lst) ((ap Lst2) ((ap Ys) Zs))) ((ap ((ap Lst2) Ys)) Zs)) (cns A)))) as proof of ((((eq lst) ((ap Lst2) ((ap Ys) Zs))) ((ap ((ap Lst2) Ys)) Zs))->(((eq lst) ((cns A) ((ap Lst2) ((ap Ys) Zs)))) ((ap ((ap ((cns A) Lst2)) Ys)) Zs))) % Found ((fact_1p_Osimps_I2_J__eq_sym100 (fun (x0:lst)=> ((((eq lst) ((ap Lst2) ((ap Ys) Zs))) ((ap ((ap Lst2) Ys)) Zs))->(((eq lst) ((cns A) ((ap Lst2) ((ap Ys) Zs)))) ((ap x0) Zs))))) (((((fact_1p_Osimps_I2_J__eq_sym Zs) ((ap Lst2) Ys)) A) (fun (x0:lst)=> ((((eq lst) ((ap Lst2) ((ap Ys) Zs))) ((ap ((ap Lst2) Ys)) Zs))->(((eq lst) ((cns A) ((ap Lst2) ((ap Ys) Zs)))) x0)))) (((((eq_substitution lst) lst) ((ap Lst2) ((ap Ys) Zs))) ((ap ((ap Lst2) Ys)) Zs)) (cns A)))) as proof of ((((eq lst) ((ap Lst2) ((ap Ys) Zs))) ((ap ((ap Lst2) Ys)) Zs))->(((eq lst) ((cns A) ((ap Lst2) ((ap Ys) Zs)))) ((ap ((ap ((cns A) Lst2)) Ys)) Zs))) % Found (((fact_1p_Osimps_I2_J__eq_sym10 A) (fun (x0:lst)=> ((((eq lst) ((ap Lst2) ((ap Ys) Zs))) ((ap ((ap Lst2) Ys)) Zs))->(((eq lst) ((cns A) ((ap Lst2) ((ap Ys) Zs)))) ((ap x0) Zs))))) (((((fact_1p_Osimps_I2_J__eq_sym Zs) ((ap Lst2) Ys)) A) (fun (x0:lst)=> ((((eq lst) ((ap Lst2) ((ap Ys) Zs))) ((ap ((ap Lst2) Ys)) Zs))->(((eq lst) ((cns A) ((ap Lst2) ((ap Ys) Zs)))) x0)))) (((((eq_substitution lst) lst) ((ap Lst2) ((ap Ys) Zs))) ((ap ((ap Lst2) Ys)) Zs)) (cns A)))) as proof of ((((eq lst) ((ap Lst2) ((ap Ys) Zs))) ((ap ((ap Lst2) Ys)) Zs))->(((eq lst) ((cns A) ((ap Lst2) ((ap Ys) Zs)))) ((ap ((ap ((cns A) Lst2)) Ys)) Zs))) % Found ((((fact_1p_Osimps_I2_J__eq_sym1 Lst2) A) (fun (x0:lst)=> ((((eq lst) ((ap Lst2) ((ap Ys) Zs))) ((ap ((ap Lst2) Ys)) Zs))->(((eq lst) ((cns A) ((ap Lst2) ((ap Ys) Zs)))) ((ap x0) Zs))))) (((((fact_1p_Osimps_I2_J__eq_sym Zs) ((ap Lst2) Ys)) A) (fun (x0:lst)=> ((((eq lst) ((ap Lst2) ((ap Ys) Zs))) ((ap ((ap Lst2) Ys)) Zs))->(((eq lst) ((cns A) ((ap Lst2) ((ap Ys) Zs)))) x0)))) (((((eq_substitution lst) lst) ((ap Lst2) ((ap Ys) Zs))) ((ap ((ap Lst2) Ys)) Zs)) (cns A)))) as proof of ((((eq lst) ((ap Lst2) ((ap Ys) Zs))) ((ap ((ap Lst2) Ys)) Zs))->(((eq lst) ((cns A) ((ap Lst2) ((ap Ys) Zs)))) ((ap ((ap ((cns A) Lst2)) Ys)) Zs))) % Found (((((fact_1p_Osimps_I2_J__eq_sym Ys) Lst2) A) (fun (x0:lst)=> ((((eq lst) ((ap Lst2) ((ap Ys) Zs))) ((ap ((ap Lst2) Ys)) Zs))->(((eq lst) ((cns A) ((ap Lst2) ((ap Ys) Zs)))) ((ap x0) Zs))))) (((((fact_1p_Osimps_I2_J__eq_sym Zs) ((ap Lst2) Ys)) A) (fun (x0:lst)=> ((((eq lst) ((ap Lst2) ((ap Ys) Zs))) ((ap ((ap Lst2) Ys)) Zs))->(((eq lst) ((cns A) ((ap Lst2) ((ap Ys) Zs)))) x0)))) (((((eq_substitution lst) lst) ((ap Lst2) ((ap Ys) Zs))) ((ap ((ap Lst2) Ys)) Zs)) (cns A)))) as proof of ((((eq lst) ((ap Lst2) ((ap Ys) Zs))) ((ap ((ap Lst2) Ys)) Zs))->(((eq lst) ((cns A) ((ap Lst2) ((ap Ys) Zs)))) ((ap ((ap ((cns A) Lst2)) Ys)) Zs))) % Found (((((fact_1p_Osimps_I2_J__eq_sym Ys) Lst2) A) (fun (x0:lst)=> ((((eq lst) ((ap Lst2) ((ap Ys) Zs))) ((ap ((ap Lst2) Ys)) Zs))->(((eq lst) ((cns A) ((ap Lst2) ((ap Ys) Zs)))) ((ap x0) Zs))))) (((((fact_1p_Osimps_I2_J__eq_sym Zs) ((ap Lst2) Ys)) A) (fun (x0:lst)=> ((((eq lst) ((ap Lst2) ((ap Ys) Zs))) ((ap ((ap Lst2) Ys)) Zs))->(((eq lst) ((cns A) ((ap Lst2) ((ap Ys) Zs)))) x0)))) (((((eq_substitution lst) lst) ((ap Lst2) ((ap Ys) Zs))) ((ap ((ap Lst2) Ys)) Zs)) (cns A)))) as proof of ((((eq lst) ((ap Lst2) ((ap Ys) Zs))) ((ap ((ap Lst2) Ys)) Zs))->(((eq lst) ((cns A) ((ap Lst2) ((ap Ys) Zs)))) ((ap ((ap ((cns A) Lst2)) Ys)) Zs))) % Found (fact_1p_Osimps_I2_J__eq_sym0000 (((((fact_1p_Osimps_I2_J__eq_sym Ys) Lst2) A) (fun (x0:lst)=> ((((eq lst) ((ap Lst2) ((ap Ys) Zs))) ((ap ((ap Lst2) Ys)) Zs))->(((eq lst) ((cns A) ((ap Lst2) ((ap Ys) Zs)))) ((ap x0) Zs))))) (((((fact_1p_Osimps_I2_J__eq_sym Zs) ((ap Lst2) Ys)) A) (fun (x0:lst)=> ((((eq lst) ((ap Lst2) ((ap Ys) Zs))) ((ap ((ap Lst2) Ys)) Zs))->(((eq lst) ((cns A) ((ap Lst2) ((ap Ys) Zs)))) x0)))) (((((eq_substitution lst) lst) ((ap Lst2) ((ap Ys) Zs))) ((ap ((ap Lst2) Ys)) Zs)) (cns A))))) as proof of ((((eq lst) ((ap Lst2) ((ap Ys) Zs))) ((ap ((ap Lst2) Ys)) Zs))->(((eq lst) ((ap ((cns A) Lst2)) ((ap Ys) Zs))) ((ap ((ap ((cns A) Lst2)) Ys)) Zs))) % Found ((fact_1p_Osimps_I2_J__eq_sym000 (fun (x0:lst)=> ((((eq lst) ((ap Lst2) ((ap Ys) Zs))) ((ap ((ap Lst2) Ys)) Zs))->(((eq lst) x0) ((ap ((ap ((cns A) Lst2)) Ys)) Zs))))) (((((fact_1p_Osimps_I2_J__eq_sym Ys) Lst2) A) (fun (x0:lst)=> ((((eq lst) ((ap Lst2) ((ap Ys) Zs))) ((ap ((ap Lst2) Ys)) Zs))->(((eq lst) ((cns A) ((ap Lst2) ((ap Ys) Zs)))) ((ap x0) Zs))))) (((((fact_1p_Osimps_I2_J__eq_sym Zs) ((ap Lst2) Ys)) A) (fun (x0:lst)=> ((((eq lst) ((ap Lst2) ((ap Ys) Zs))) ((ap ((ap Lst2) Ys)) Zs))->(((eq lst) ((cns A) ((ap Lst2) ((ap Ys) Zs)))) x0)))) (((((eq_substitution lst) lst) ((ap Lst2) ((ap Ys) Zs))) ((ap ((ap Lst2) Ys)) Zs)) (cns A))))) as proof of ((((eq lst) ((ap Lst2) ((ap Ys) Zs))) ((ap ((ap Lst2) Ys)) Zs))->(((eq lst) ((ap ((cns A) Lst2)) ((ap Ys) Zs))) ((ap ((ap ((cns A) Lst2)) Ys)) Zs))) % Found (((fact_1p_Osimps_I2_J__eq_sym00 A) (fun (x0:lst)=> ((((eq lst) ((ap Lst2) ((ap Ys) Zs))) ((ap ((ap Lst2) Ys)) Zs))->(((eq lst) x0) ((ap ((ap ((cns A) Lst2)) Ys)) Zs))))) (((((fact_1p_Osimps_I2_J__eq_sym Ys) Lst2) A) (fun (x0:lst)=> ((((eq lst) ((ap Lst2) ((ap Ys) Zs))) ((ap ((ap Lst2) Ys)) Zs))->(((eq lst) ((cns A) ((ap Lst2) ((ap Ys) Zs)))) ((ap x0) Zs))))) (((((fact_1p_Osimps_I2_J__eq_sym Zs) ((ap Lst2) Ys)) A) (fun (x0:lst)=> ((((eq lst) ((ap Lst2) ((ap Ys) Zs))) ((ap ((ap Lst2) Ys)) Zs))->(((eq lst) ((cns A) ((ap Lst2) ((ap Ys) Zs)))) x0)))) (((((eq_substitution lst) lst) ((ap Lst2) ((ap Ys) Zs))) ((ap ((ap Lst2) Ys)) Zs)) (cns A))))) as proof of ((((eq lst) ((ap Lst2) ((ap Ys) Zs))) ((ap ((ap Lst2) Ys)) Zs))->(((eq lst) ((ap ((cns A) Lst2)) ((ap Ys) Zs))) ((ap ((ap ((cns A) Lst2)) Ys)) Zs))) % Found ((((fact_1p_Osimps_I2_J__eq_sym0 Lst2) A) (fun (x0:lst)=> ((((eq lst) ((ap Lst2) ((ap Ys) Zs))) ((ap ((ap Lst2) Ys)) Zs))->(((eq lst) x0) ((ap ((ap ((cns A) Lst2)) Ys)) Zs))))) (((((fact_1p_Osimps_I2_J__eq_sym Ys) Lst2) A) (fun (x0:lst)=> ((((eq lst) ((ap Lst2) ((ap Ys) Zs))) ((ap ((ap Lst2) Ys)) Zs))->(((eq lst) ((cns A) ((ap Lst2) ((ap Ys) Zs)))) ((ap x0) Zs))))) (((((fact_1p_Osimps_I2_J__eq_sym Zs) ((ap Lst2) Ys)) A) (fun (x0:lst)=> ((((eq lst) ((ap Lst2) ((ap Ys) Zs))) ((ap ((ap Lst2) Ys)) Zs))->(((eq lst) ((cns A) ((ap Lst2) ((ap Ys) Zs)))) x0)))) (((((eq_substitution lst) lst) ((ap Lst2) ((ap Ys) Zs))) ((ap ((ap Lst2) Ys)) Zs)) (cns A))))) as proof of ((((eq lst) ((ap Lst2) ((ap Ys) Zs))) ((ap ((ap Lst2) Ys)) Zs))->(((eq lst) ((ap ((cns A) Lst2)) ((ap Ys) Zs))) ((ap ((ap ((cns A) Lst2)) Ys)) Zs))) % Found (((((fact_1p_Osimps_I2_J__eq_sym ((ap Ys) Zs)) Lst2) A) (fun (x0:lst)=> ((((eq lst) ((ap Lst2) ((ap Ys) Zs))) ((ap ((ap Lst2) Ys)) Zs))->(((eq lst) x0) ((ap ((ap ((cns A) Lst2)) Ys)) Zs))))) (((((fact_1p_Osimps_I2_J__eq_sym Ys) Lst2) A) (fun (x0:lst)=> ((((eq lst) ((ap Lst2) ((ap Ys) Zs))) ((ap ((ap Lst2) Ys)) Zs))->(((eq lst) ((cns A) ((ap Lst2) ((ap Ys) Zs)))) ((ap x0) Zs))))) (((((fact_1p_Osimps_I2_J__eq_sym Zs) ((ap Lst2) Ys)) A) (fun (x0:lst)=> ((((eq lst) ((ap Lst2) ((ap Ys) Zs))) ((ap ((ap Lst2) Ys)) Zs))->(((eq lst) ((cns A) ((ap Lst2) ((ap Ys) Zs)))) x0)))) (((((eq_substitution lst) lst) ((ap Lst2) ((ap Ys) Zs))) ((ap ((ap Lst2) Ys)) Zs)) (cns A))))) as proof of ((((eq lst) ((ap Lst2) ((ap Ys) Zs))) ((ap ((ap Lst2) Ys)) Zs))->(((eq lst) ((ap ((cns A) Lst2)) ((ap Ys) Zs))) ((ap ((ap ((cns A) Lst2)) Ys)) Zs))) % Found (fun (Lst2:lst)=> (((((fact_1p_Osimps_I2_J__eq_sym ((ap Ys) Zs)) Lst2) A) (fun (x0:lst)=> ((((eq lst) ((ap Lst2) ((ap Ys) Zs))) ((ap ((ap Lst2) Ys)) Zs))->(((eq lst) x0) ((ap ((ap ((cns A) Lst2)) Ys)) Zs))))) (((((fact_1p_Osimps_I2_J__eq_sym Ys) Lst2) A) (fun (x0:lst)=> ((((eq lst) ((ap Lst2) ((ap Ys) Zs))) ((ap ((ap Lst2) Ys)) Zs))->(((eq lst) ((cns A) ((ap Lst2) ((ap Ys) Zs)))) ((ap x0) Zs))))) (((((fact_1p_Osimps_I2_J__eq_sym Zs) ((ap Lst2) Ys)) A) (fun (x0:lst)=> ((((eq lst) ((ap Lst2) ((ap Ys) Zs))) ((ap ((ap Lst2) Ys)) Zs))->(((eq lst) ((cns A) ((ap Lst2) ((ap Ys) Zs)))) x0)))) (((((eq_substitution lst) lst) ((ap Lst2) ((ap Ys) Zs))) ((ap ((ap Lst2) Ys)) Zs)) (cns A)))))) as proof of ((((eq lst) ((ap Lst2) ((ap Ys) Zs))) ((ap ((ap Lst2) Ys)) Zs))->(((eq lst) ((ap ((cns A) Lst2)) ((ap Ys) Zs))) ((ap ((ap ((cns A) Lst2)) Ys)) Zs))) % Found (fun (A:a) (Lst2:lst)=> (((((fact_1p_Osimps_I2_J__eq_sym ((ap Ys) Zs)) Lst2) A) (fun (x0:lst)=> ((((eq lst) ((ap Lst2) ((ap Ys) Zs))) ((ap ((ap Lst2) Ys)) Zs))->(((eq lst) x0) ((ap ((ap ((cns A) Lst2)) Ys)) Zs))))) (((((fact_1p_Osimps_I2_J__eq_sym Ys) Lst2) A) (fun (x0:lst)=> ((((eq lst) ((ap Lst2) ((ap Ys) Zs))) ((ap ((ap Lst2) Ys)) Zs))->(((eq lst) ((cns A) ((ap Lst2) ((ap Ys) Zs)))) ((ap x0) Zs))))) (((((fact_1p_Osimps_I2_J__eq_sym Zs) ((ap Lst2) Ys)) A) (fun (x0:lst)=> ((((eq lst) ((ap Lst2) ((ap Ys) Zs))) ((ap ((ap Lst2) Ys)) Zs))->(((eq lst) ((cns A) ((ap Lst2) ((ap Ys) Zs)))) x0)))) (((((eq_substitution lst) lst) ((ap Lst2) ((ap Ys) Zs))) ((ap ((ap Lst2) Ys)) Zs)) (cns A)))))) as proof of (forall (Lst2:lst), ((((eq lst) ((ap Lst2) ((ap Ys) Zs))) ((ap ((ap Lst2) Ys)) Zs))->(((eq lst) ((ap ((cns A) Lst2)) ((ap Ys) Zs))) ((ap ((ap ((cns A) Lst2)) Ys)) Zs)))) % Found (fun (A:a) (Lst2:lst)=> (((((fact_1p_Osimps_I2_J__eq_sym ((ap Ys) Zs)) Lst2) A) (fun (x0:lst)=> ((((eq lst) ((ap Lst2) ((ap Ys) Zs))) ((ap ((ap Lst2) Ys)) Zs))->(((eq lst) x0) ((ap ((ap ((cns A) Lst2)) Ys)) Zs))))) (((((fact_1p_Osimps_I2_J__eq_sym Ys) Lst2) A) (fun (x0:lst)=> ((((eq lst) ((ap Lst2) ((ap Ys) Zs))) ((ap ((ap Lst2) Ys)) Zs))->(((eq lst) ((cns A) ((ap Lst2) ((ap Ys) Zs)))) ((ap x0) Zs))))) (((((fact_1p_Osimps_I2_J__eq_sym Zs) ((ap Lst2) Ys)) A) (fun (x0:lst)=> ((((eq lst) ((ap Lst2) ((ap Ys) Zs))) ((ap ((ap Lst2) Ys)) Zs))->(((eq lst) ((cns A) ((ap Lst2) ((ap Ys) Zs)))) x0)))) (((((eq_substitution lst) lst) ((ap Lst2) ((ap Ys) Zs))) ((ap ((ap Lst2) Ys)) Zs)) (cns A)))))) as proof of (forall (A:a) (Lst2:lst), ((((eq lst) ((ap Lst2) ((ap Ys) Zs))) ((ap ((ap Lst2) Ys)) Zs))->(((eq lst) ((ap ((cns A) Lst2)) ((ap Ys) Zs))) ((ap ((ap ((cns A) Lst2)) Ys)) Zs)))) % Found ((fact_0_lst_Oinduct00 ((((eq_sym lst) ((ap ((ap nl) Ys)) Zs)) ((ap nl) ((ap Ys) Zs))) (((fact_2p_Osimps_I1_J__eq_sym Ys) (fun (x0:lst)=> (((eq lst) ((ap x0) Zs)) ((ap nl) ((ap Ys) Zs))))) (fact_2p_Osimps_I1_J__eq_sym ((ap Ys) Zs))))) (fun (A:a) (Lst2:lst)=> (((((fact_1p_Osimps_I2_J__eq_sym ((ap Ys) Zs)) Lst2) A) (fun (x0:lst)=> ((((eq lst) ((ap Lst2) ((ap Ys) Zs))) ((ap ((ap Lst2) Ys)) Zs))->(((eq lst) x0) ((ap ((ap ((cns A) Lst2)) Ys)) Zs))))) (((((fact_1p_Osimps_I2_J__eq_sym Ys) Lst2) A) (fun (x0:lst)=> ((((eq lst) ((ap Lst2) ((ap Ys) Zs))) ((ap ((ap Lst2) Ys)) Zs))->(((eq lst) ((cns A) ((ap Lst2) ((ap Ys) Zs)))) ((ap x0) Zs))))) (((((fact_1p_Osimps_I2_J__eq_sym Zs) ((ap Lst2) Ys)) A) (fun (x0:lst)=> ((((eq lst) ((ap Lst2) ((ap Ys) Zs))) ((ap ((ap Lst2) Ys)) Zs))->(((eq lst) ((cns A) ((ap Lst2) ((ap Ys) Zs)))) x0)))) (((((eq_substitution lst) lst) ((ap Lst2) ((ap Ys) Zs))) ((ap ((ap Lst2) Ys)) Zs)) (cns A))))))) as proof of (((eq lst) ((ap xs) ((ap Ys) Zs))) ((ap ((ap xs) Ys)) Zs)) % Found (((fact_0_lst_Oinduct0 (fun (x1:lst)=> (((eq lst) ((ap x1) ((ap Ys) Zs))) ((ap ((ap x1) Ys)) Zs)))) ((((eq_sym lst) ((ap ((ap nl) Ys)) Zs)) ((ap nl) ((ap Ys) Zs))) (((fact_2p_Osimps_I1_J__eq_sym Ys) (fun (x0:lst)=> (((eq lst) ((ap x0) Zs)) ((ap nl) ((ap Ys) Zs))))) (fact_2p_Osimps_I1_J__eq_sym ((ap Ys) Zs))))) (fun (A:a) (Lst2:lst)=> (((((fact_1p_Osimps_I2_J__eq_sym ((ap Ys) Zs)) Lst2) A) (fun (x0:lst)=> ((((eq lst) ((ap Lst2) ((ap Ys) Zs))) ((ap ((ap Lst2) Ys)) Zs))->(((eq lst) x0) ((ap ((ap ((cns A) Lst2)) Ys)) Zs))))) (((((fact_1p_Osimps_I2_J__eq_sym Ys) Lst2) A) (fun (x0:lst)=> ((((eq lst) ((ap Lst2) ((ap Ys) Zs))) ((ap ((ap Lst2) Ys)) Zs))->(((eq lst) ((cns A) ((ap Lst2) ((ap Ys) Zs)))) ((ap x0) Zs))))) (((((fact_1p_Osimps_I2_J__eq_sym Zs) ((ap Lst2) Ys)) A) (fun (x0:lst)=> ((((eq lst) ((ap Lst2) ((ap Ys) Zs))) ((ap ((ap Lst2) Ys)) Zs))->(((eq lst) ((cns A) ((ap Lst2) ((ap Ys) Zs)))) x0)))) (((((eq_substitution lst) lst) ((ap Lst2) ((ap Ys) Zs))) ((ap ((ap Lst2) Ys)) Zs)) (cns A))))))) as proof of (((eq lst) ((ap xs) ((ap Ys) Zs))) ((ap ((ap xs) Ys)) Zs)) % Found ((((fact_0_lst_Oinduct xs) (fun (x1:lst)=> (((eq lst) ((ap x1) ((ap Ys) Zs))) ((ap ((ap x1) Ys)) Zs)))) ((((eq_sym lst) ((ap ((ap nl) Ys)) Zs)) ((ap nl) ((ap Ys) Zs))) (((fact_2p_Osimps_I1_J__eq_sym Ys) (fun (x0:lst)=> (((eq lst) ((ap x0) Zs)) ((ap nl) ((ap Ys) Zs))))) (fact_2p_Osimps_I1_J__eq_sym ((ap Ys) Zs))))) (fun (A:a) (Lst2:lst)=> (((((fact_1p_Osimps_I2_J__eq_sym ((ap Ys) Zs)) Lst2) A) (fun (x0:lst)=> ((((eq lst) ((ap Lst2) ((ap Ys) Zs))) ((ap ((ap Lst2) Ys)) Zs))->(((eq lst) x0) ((ap ((ap ((cns A) Lst2)) Ys)) Zs))))) (((((fact_1p_Osimps_I2_J__eq_sym Ys) Lst2) A) (fun (x0:lst)=> ((((eq lst) ((ap Lst2) ((ap Ys) Zs))) ((ap ((ap Lst2) Ys)) Zs))->(((eq lst) ((cns A) ((ap Lst2) ((ap Ys) Zs)))) ((ap x0) Zs))))) (((((fact_1p_Osimps_I2_J__eq_sym Zs) ((ap Lst2) Ys)) A) (fun (x0:lst)=> ((((eq lst) ((ap Lst2) ((ap Ys) Zs))) ((ap ((ap Lst2) Ys)) Zs))->(((eq lst) ((cns A) ((ap Lst2) ((ap Ys) Zs)))) x0)))) (((((eq_substitution lst) lst) ((ap Lst2) ((ap Ys) Zs))) ((ap ((ap Lst2) Ys)) Zs)) (cns A))))))) as proof of (((eq lst) ((ap xs) ((ap Ys) Zs))) ((ap ((ap xs) Ys)) Zs)) % Found (fun (Zs:lst)=> ((((fact_0_lst_Oinduct xs) (fun (x1:lst)=> (((eq lst) ((ap x1) ((ap Ys) Zs))) ((ap ((ap x1) Ys)) Zs)))) ((((eq_sym lst) ((ap ((ap nl) Ys)) Zs)) ((ap nl) ((ap Ys) Zs))) (((fact_2p_Osimps_I1_J__eq_sym Ys) (fun (x0:lst)=> (((eq lst) ((ap x0) Zs)) ((ap nl) ((ap Ys) Zs))))) (fact_2p_Osimps_I1_J__eq_sym ((ap Ys) Zs))))) (fun (A:a) (Lst2:lst)=> (((((fact_1p_Osimps_I2_J__eq_sym ((ap Ys) Zs)) Lst2) A) (fun (x0:lst)=> ((((eq lst) ((ap Lst2) ((ap Ys) Zs))) ((ap ((ap Lst2) Ys)) Zs))->(((eq lst) x0) ((ap ((ap ((cns A) Lst2)) Ys)) Zs))))) (((((fact_1p_Osimps_I2_J__eq_sym Ys) Lst2) A) (fun (x0:lst)=> ((((eq lst) ((ap Lst2) ((ap Ys) Zs))) ((ap ((ap Lst2) Ys)) Zs))->(((eq lst) ((cns A) ((ap Lst2) ((ap Ys) Zs)))) ((ap x0) Zs))))) (((((fact_1p_Osimps_I2_J__eq_sym Zs) ((ap Lst2) Ys)) A) (fun (x0:lst)=> ((((eq lst) ((ap Lst2) ((ap Ys) Zs))) ((ap ((ap Lst2) Ys)) Zs))->(((eq lst) ((cns A) ((ap Lst2) ((ap Ys) Zs)))) x0)))) (((((eq_substitution lst) lst) ((ap Lst2) ((ap Ys) Zs))) ((ap ((ap Lst2) Ys)) Zs)) (cns A)))))))) as proof of (((eq lst) ((ap xs) ((ap Ys) Zs))) ((ap ((ap xs) Ys)) Zs)) % Found (fun (Ys:lst) (Zs:lst)=> ((((fact_0_lst_Oinduct xs) (fun (x1:lst)=> (((eq lst) ((ap x1) ((ap Ys) Zs))) ((ap ((ap x1) Ys)) Zs)))) ((((eq_sym lst) ((ap ((ap nl) Ys)) Zs)) ((ap nl) ((ap Ys) Zs))) (((fact_2p_Osimps_I1_J__eq_sym Ys) (fun (x0:lst)=> (((eq lst) ((ap x0) Zs)) ((ap nl) ((ap Ys) Zs))))) (fact_2p_Osimps_I1_J__eq_sym ((ap Ys) Zs))))) (fun (A:a) (Lst2:lst)=> (((((fact_1p_Osimps_I2_J__eq_sym ((ap Ys) Zs)) Lst2) A) (fun (x0:lst)=> ((((eq lst) ((ap Lst2) ((ap Ys) Zs))) ((ap ((ap Lst2) Ys)) Zs))->(((eq lst) x0) ((ap ((ap ((cns A) Lst2)) Ys)) Zs))))) (((((fact_1p_Osimps_I2_J__eq_sym Ys) Lst2) A) (fun (x0:lst)=> ((((eq lst) ((ap Lst2) ((ap Ys) Zs))) ((ap ((ap Lst2) Ys)) Zs))->(((eq lst) ((cns A) ((ap Lst2) ((ap Ys) Zs)))) ((ap x0) Zs))))) (((((fact_1p_Osimps_I2_J__eq_sym Zs) ((ap Lst2) Ys)) A) (fun (x0:lst)=> ((((eq lst) ((ap Lst2) ((ap Ys) Zs))) ((ap ((ap Lst2) Ys)) Zs))->(((eq lst) ((cns A) ((ap Lst2) ((ap Ys) Zs)))) x0)))) (((((eq_substitution lst) lst) ((ap Lst2) ((ap Ys) Zs))) ((ap ((ap Lst2) Ys)) Zs)) (cns A)))))))) as proof of (forall (Zs:lst), (((eq lst) ((ap xs) ((ap Ys) Zs))) ((ap ((ap xs) Ys)) Zs))) % Found (fun (Ys:lst) (Zs:lst)=> ((((fact_0_lst_Oinduct xs) (fun (x1:lst)=> (((eq lst) ((ap x1) ((ap Ys) Zs))) ((ap ((ap x1) Ys)) Zs)))) ((((eq_sym lst) ((ap ((ap nl) Ys)) Zs)) ((ap nl) ((ap Ys) Zs))) (((fact_2p_Osimps_I1_J__eq_sym Ys) (fun (x0:lst)=> (((eq lst) ((ap x0) Zs)) ((ap nl) ((ap Ys) Zs))))) (fact_2p_Osimps_I1_J__eq_sym ((ap Ys) Zs))))) (fun (A:a) (Lst2:lst)=> (((((fact_1p_Osimps_I2_J__eq_sym ((ap Ys) Zs)) Lst2) A) (fun (x0:lst)=> ((((eq lst) ((ap Lst2) ((ap Ys) Zs))) ((ap ((ap Lst2) Ys)) Zs))->(((eq lst) x0) ((ap ((ap ((cns A) Lst2)) Ys)) Zs))))) (((((fact_1p_Osimps_I2_J__eq_sym Ys) Lst2) A) (fun (x0:lst)=> ((((eq lst) ((ap Lst2) ((ap Ys) Zs))) ((ap ((ap Lst2) Ys)) Zs))->(((eq lst) ((cns A) ((ap Lst2) ((ap Ys) Zs)))) ((ap x0) Zs))))) (((((fact_1p_Osimps_I2_J__eq_sym Zs) ((ap Lst2) Ys)) A) (fun (x0:lst)=> ((((eq lst) ((ap Lst2) ((ap Ys) Zs))) ((ap ((ap Lst2) Ys)) Zs))->(((eq lst) ((cns A) ((ap Lst2) ((ap Ys) Zs)))) x0)))) (((((eq_substitution lst) lst) ((ap Lst2) ((ap Ys) Zs))) ((ap ((ap Lst2) Ys)) Zs)) (cns A)))))))) as proof of (forall (Ys:lst) (Zs:lst), (((eq lst) ((ap xs) ((ap Ys) Zs))) ((ap ((ap xs) Ys)) Zs))) % Got proof (fun (Ys:lst) (Zs:lst)=> ((((fact_0_lst_Oinduct xs) (fun (x1:lst)=> (((eq lst) ((ap x1) ((ap Ys) Zs))) ((ap ((ap x1) Ys)) Zs)))) ((((eq_sym lst) ((ap ((ap nl) Ys)) Zs)) ((ap nl) ((ap Ys) Zs))) ((((fun (Ys2:lst)=> ((((eq_sym lst) ((ap nl) Ys2)) Ys2) (fact_2p_Osimps_I1_J Ys2))) Ys) (fun (x0:lst)=> (((eq lst) ((ap x0) Zs)) ((ap nl) ((ap Ys) Zs))))) ((fun (Ys2:lst)=> ((((eq_sym lst) ((ap nl) Ys2)) Ys2) (fact_2p_Osimps_I1_J Ys2))) ((ap Ys) Zs))))) (fun (A:a) (Lst2:lst)=> ((((((fun (Ys2:lst) (Xs:lst) (X:a)=> ((((eq_sym lst) ((ap ((cns X) Xs)) Ys2)) ((cns X) ((ap Xs) Ys2))) (((fact_1p_Osimps_I2_J Ys2) Xs) X))) ((ap Ys) Zs)) Lst2) A) (fun (x0:lst)=> ((((eq lst) ((ap Lst2) ((ap Ys) Zs))) ((ap ((ap Lst2) Ys)) Zs))->(((eq lst) x0) ((ap ((ap ((cns A) Lst2)) Ys)) Zs))))) ((((((fun (Ys2:lst) (Xs:lst) (X:a)=> ((((eq_sym lst) ((ap ((cns X) Xs)) Ys2)) ((cns X) ((ap Xs) Ys2))) (((fact_1p_Osimps_I2_J Ys2) Xs) X))) Ys) Lst2) A) (fun (x0:lst)=> ((((eq lst) ((ap Lst2) ((ap Ys) Zs))) ((ap ((ap Lst2) Ys)) Zs))->(((eq lst) ((cns A) ((ap Lst2) ((ap Ys) Zs)))) ((ap x0) Zs))))) ((((((fun (Ys2:lst) (Xs:lst) (X:a)=> ((((eq_sym lst) ((ap ((cns X) Xs)) Ys2)) ((cns X) ((ap Xs) Ys2))) (((fact_1p_Osimps_I2_J Ys2) Xs) X))) Zs) ((ap Lst2) Ys)) A) (fun (x0:lst)=> ((((eq lst) ((ap Lst2) ((ap Ys) Zs))) ((ap ((ap Lst2) Ys)) Zs))->(((eq lst) ((cns A) ((ap Lst2) ((ap Ys) Zs)))) x0)))) (((((eq_substitution lst) lst) ((ap Lst2) ((ap Ys) Zs))) ((ap ((ap Lst2) Ys)) Zs)) (cns A)))))))) % Time elapsed = 179.537165s % node=26072 cost=557.000000 depth=31 % :::::::::::::::::::::: % % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p % (fun (Ys:lst) (Zs:lst)=> ((((fact_0_lst_Oinduct xs) (fun (x1:lst)=> (((eq lst) ((ap x1) ((ap Ys) Zs))) ((ap ((ap x1) Ys)) Zs)))) ((((eq_sym lst) ((ap ((ap nl) Ys)) Zs)) ((ap nl) ((ap Ys) Zs))) ((((fun (Ys2:lst)=> ((((eq_sym lst) ((ap nl) Ys2)) Ys2) (fact_2p_Osimps_I1_J Ys2))) Ys) (fun (x0:lst)=> (((eq lst) ((ap x0) Zs)) ((ap nl) ((ap Ys) Zs))))) ((fun (Ys2:lst)=> ((((eq_sym lst) ((ap nl) Ys2)) Ys2) (fact_2p_Osimps_I1_J Ys2))) ((ap Ys) Zs))))) (fun (A:a) (Lst2:lst)=> ((((((fun (Ys2:lst) (Xs:lst) (X:a)=> ((((eq_sym lst) ((ap ((cns X) Xs)) Ys2)) ((cns X) ((ap Xs) Ys2))) (((fact_1p_Osimps_I2_J Ys2) Xs) X))) ((ap Ys) Zs)) Lst2) A) (fun (x0:lst)=> ((((eq lst) ((ap Lst2) ((ap Ys) Zs))) ((ap ((ap Lst2) Ys)) Zs))->(((eq lst) x0) ((ap ((ap ((cns A) Lst2)) Ys)) Zs))))) ((((((fun (Ys2:lst) (Xs:lst) (X:a)=> ((((eq_sym lst) ((ap ((cns X) Xs)) Ys2)) ((cns X) ((ap Xs) Ys2))) (((fact_1p_Osimps_I2_J Ys2) Xs) X))) Ys) Lst2) A) (fun (x0:lst)=> ((((eq lst) ((ap Lst2) ((ap Ys) Zs))) ((ap ((ap Lst2) Ys)) Zs))->(((eq lst) ((cns A) ((ap Lst2) ((ap Ys) Zs)))) ((ap x0) Zs))))) ((((((fun (Ys2:lst) (Xs:lst) (X:a)=> ((((eq_sym lst) ((ap ((cns X) Xs)) Ys2)) ((cns X) ((ap Xs) Ys2))) (((fact_1p_Osimps_I2_J Ys2) Xs) X))) Zs) ((ap Lst2) Ys)) A) (fun (x0:lst)=> ((((eq lst) ((ap Lst2) ((ap Ys) Zs))) ((ap ((ap Lst2) Ys)) Zs))->(((eq lst) ((cns A) ((ap Lst2) ((ap Ys) Zs)))) x0)))) (((((eq_substitution lst) lst) ((ap Lst2) ((ap Ys) Zs))) ((ap ((ap Lst2) Ys)) Zs)) (cns A)))))))) % % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p % EOF %------------------------------------------------------------------------------