%------------------------------------------------------------------------------ % File : cocATP---0.2.0 % Problem : SEU493^1 : TPTP v6.1.0. Released v3.6.0. % Transfm : none % Format : tptp:raw % Command : python CASC.py /export/starexec/sandbox/benchmark/theBenchmark.p % Computer : n185.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:32:17 EDT 2014 % Result : Theorem 17.65s % Output : Proof 17.65s % Verified : % SZS Type : None (Parsing solution fails) % Syntax : Number of formulae : 0 % Comments : %------------------------------------------------------------------------------ %----ERROR: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % % Problem : SEU493^1 : TPTP v6.1.0. Released v3.6.0. % % Command : python CASC.py /export/starexec/sandbox/benchmark/theBenchmark.p % % Computer : n185.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 10:22:46 CDT 2014 % % CPUTime : 17.65 % Python 2.7.5 % Using paths ['/home/cristobal/cocATP/CASC/TPTP/', '/export/starexec/sandbox/benchmark/', '/export/starexec/sandbox/benchmark/'] % Failed to open /home/cristobal/cocATP/CASC/TPTP/Axioms/SET009^0.ax, trying next directory % FOF formula (<kernel.Constant object at 0x1618290>, <kernel.DependentProduct object at 0x1436cf8>) of role type named subrel_type % Using role type % Declaring subrel:((fofType->(fofType->Prop))->((fofType->(fofType->Prop))->Prop)) % FOF formula (((eq ((fofType->(fofType->Prop))->((fofType->(fofType->Prop))->Prop))) subrel) (fun (R:(fofType->(fofType->Prop))) (S:(fofType->(fofType->Prop)))=> (forall (X:fofType) (Y:fofType), (((R X) Y)->((S X) Y))))) of role definition named subrel % A new definition: (((eq ((fofType->(fofType->Prop))->((fofType->(fofType->Prop))->Prop))) subrel) (fun (R:(fofType->(fofType->Prop))) (S:(fofType->(fofType->Prop)))=> (forall (X:fofType) (Y:fofType), (((R X) Y)->((S X) Y))))) % Defined: subrel:=(fun (R:(fofType->(fofType->Prop))) (S:(fofType->(fofType->Prop)))=> (forall (X:fofType) (Y:fofType), (((R X) Y)->((S X) Y)))) % FOF formula (<kernel.Constant object at 0x1867170>, <kernel.DependentProduct object at 0x1436cf8>) of role type named inv_type % Using role type % Declaring inv:((fofType->(fofType->Prop))->(fofType->(fofType->Prop))) % FOF formula (((eq ((fofType->(fofType->Prop))->(fofType->(fofType->Prop)))) inv) (fun (R:(fofType->(fofType->Prop))) (X:fofType) (Y:fofType)=> ((R Y) X))) of role definition named inverse % A new definition: (((eq ((fofType->(fofType->Prop))->(fofType->(fofType->Prop)))) inv) (fun (R:(fofType->(fofType->Prop))) (X:fofType) (Y:fofType)=> ((R Y) X))) % Defined: inv:=(fun (R:(fofType->(fofType->Prop))) (X:fofType) (Y:fofType)=> ((R Y) X)) % FOF formula (<kernel.Constant object at 0x1436cf8>, <kernel.DependentProduct object at 0x1436a28>) of role type named idem_type % Using role type % Declaring idem:(((fofType->(fofType->Prop))->(fofType->(fofType->Prop)))->Prop) % FOF formula (((eq (((fofType->(fofType->Prop))->(fofType->(fofType->Prop)))->Prop)) idem) (fun (F:((fofType->(fofType->Prop))->(fofType->(fofType->Prop))))=> (forall (R:(fofType->(fofType->Prop))), (((eq (fofType->(fofType->Prop))) (F (F R))) (F R))))) of role definition named idempotent % A new definition: (((eq (((fofType->(fofType->Prop))->(fofType->(fofType->Prop)))->Prop)) idem) (fun (F:((fofType->(fofType->Prop))->(fofType->(fofType->Prop))))=> (forall (R:(fofType->(fofType->Prop))), (((eq (fofType->(fofType->Prop))) (F (F R))) (F R))))) % Defined: idem:=(fun (F:((fofType->(fofType->Prop))->(fofType->(fofType->Prop))))=> (forall (R:(fofType->(fofType->Prop))), (((eq (fofType->(fofType->Prop))) (F (F R))) (F R)))) % FOF formula (<kernel.Constant object at 0x1436d88>, <kernel.DependentProduct object at 0x1436ab8>) of role type named infl_type % Using role type % Declaring infl:(((fofType->(fofType->Prop))->(fofType->(fofType->Prop)))->Prop) % FOF formula (((eq (((fofType->(fofType->Prop))->(fofType->(fofType->Prop)))->Prop)) infl) (fun (F:((fofType->(fofType->Prop))->(fofType->(fofType->Prop))))=> (forall (R:(fofType->(fofType->Prop))), ((subrel R) (F R))))) of role definition named inflationary % A new definition: (((eq (((fofType->(fofType->Prop))->(fofType->(fofType->Prop)))->Prop)) infl) (fun (F:((fofType->(fofType->Prop))->(fofType->(fofType->Prop))))=> (forall (R:(fofType->(fofType->Prop))), ((subrel R) (F R))))) % Defined: infl:=(fun (F:((fofType->(fofType->Prop))->(fofType->(fofType->Prop))))=> (forall (R:(fofType->(fofType->Prop))), ((subrel R) (F R)))) % FOF formula (<kernel.Constant object at 0x1436cf8>, <kernel.DependentProduct object at 0x1436488>) of role type named mono_type % Using role type % Declaring mono:(((fofType->(fofType->Prop))->(fofType->(fofType->Prop)))->Prop) % FOF formula (((eq (((fofType->(fofType->Prop))->(fofType->(fofType->Prop)))->Prop)) mono) (fun (F:((fofType->(fofType->Prop))->(fofType->(fofType->Prop))))=> (forall (R:(fofType->(fofType->Prop))) (S:(fofType->(fofType->Prop))), (((subrel R) S)->((subrel (F R)) (F S)))))) of role definition named monotonic % A new definition: (((eq (((fofType->(fofType->Prop))->(fofType->(fofType->Prop)))->Prop)) mono) (fun (F:((fofType->(fofType->Prop))->(fofType->(fofType->Prop))))=> (forall (R:(fofType->(fofType->Prop))) (S:(fofType->(fofType->Prop))), (((subrel R) S)->((subrel (F R)) (F S)))))) % Defined: mono:=(fun (F:((fofType->(fofType->Prop))->(fofType->(fofType->Prop))))=> (forall (R:(fofType->(fofType->Prop))) (S:(fofType->(fofType->Prop))), (((subrel R) S)->((subrel (F R)) (F S))))) % FOF formula (<kernel.Constant object at 0x1436cf8>, <kernel.DependentProduct object at 0x14365f0>) of role type named refl_type % Using role type % Declaring refl:((fofType->(fofType->Prop))->Prop) % FOF formula (((eq ((fofType->(fofType->Prop))->Prop)) refl) (fun (R:(fofType->(fofType->Prop)))=> (forall (X:fofType), ((R X) X)))) of role definition named reflexive % A new definition: (((eq ((fofType->(fofType->Prop))->Prop)) refl) (fun (R:(fofType->(fofType->Prop)))=> (forall (X:fofType), ((R X) X)))) % Defined: refl:=(fun (R:(fofType->(fofType->Prop)))=> (forall (X:fofType), ((R X) X))) % FOF formula (<kernel.Constant object at 0x1436b48>, <kernel.DependentProduct object at 0x1436f80>) of role type named irrefl_type % Using role type % Declaring irrefl:((fofType->(fofType->Prop))->Prop) % FOF formula (((eq ((fofType->(fofType->Prop))->Prop)) irrefl) (fun (R:(fofType->(fofType->Prop)))=> (forall (X:fofType), (((R X) X)->False)))) of role definition named irreflexive % A new definition: (((eq ((fofType->(fofType->Prop))->Prop)) irrefl) (fun (R:(fofType->(fofType->Prop)))=> (forall (X:fofType), (((R X) X)->False)))) % Defined: irrefl:=(fun (R:(fofType->(fofType->Prop)))=> (forall (X:fofType), (((R X) X)->False))) % FOF formula (<kernel.Constant object at 0x1436cf8>, <kernel.DependentProduct object at 0x1436f80>) of role type named rc_type % Using role type % Declaring rc:((fofType->(fofType->Prop))->(fofType->(fofType->Prop))) % FOF formula (((eq ((fofType->(fofType->Prop))->(fofType->(fofType->Prop)))) rc) (fun (R:(fofType->(fofType->Prop))) (X:fofType) (Y:fofType)=> ((or (((eq fofType) X) Y)) ((R X) Y)))) of role definition named reflexive_closure % A new definition: (((eq ((fofType->(fofType->Prop))->(fofType->(fofType->Prop)))) rc) (fun (R:(fofType->(fofType->Prop))) (X:fofType) (Y:fofType)=> ((or (((eq fofType) X) Y)) ((R X) Y)))) % Defined: rc:=(fun (R:(fofType->(fofType->Prop))) (X:fofType) (Y:fofType)=> ((or (((eq fofType) X) Y)) ((R X) Y))) % FOF formula (<kernel.Constant object at 0x1436cf8>, <kernel.DependentProduct object at 0x1619170>) of role type named symm_type % Using role type % Declaring symm:((fofType->(fofType->Prop))->Prop) % FOF formula (((eq ((fofType->(fofType->Prop))->Prop)) symm) (fun (R:(fofType->(fofType->Prop)))=> (forall (X:fofType) (Y:fofType), (((R X) Y)->((R Y) X))))) of role definition named symmetric % A new definition: (((eq ((fofType->(fofType->Prop))->Prop)) symm) (fun (R:(fofType->(fofType->Prop)))=> (forall (X:fofType) (Y:fofType), (((R X) Y)->((R Y) X))))) % Defined: symm:=(fun (R:(fofType->(fofType->Prop)))=> (forall (X:fofType) (Y:fofType), (((R X) Y)->((R Y) X)))) % FOF formula (<kernel.Constant object at 0x16190e0>, <kernel.DependentProduct object at 0x16195f0>) of role type named antisymm_type % Using role type % Declaring antisymm:((fofType->(fofType->Prop))->Prop) % FOF formula (((eq ((fofType->(fofType->Prop))->Prop)) antisymm) (fun (R:(fofType->(fofType->Prop)))=> (forall (X:fofType) (Y:fofType), (((and ((R X) Y)) ((R Y) X))->(((eq fofType) X) Y))))) of role definition named antisymmetric % A new definition: (((eq ((fofType->(fofType->Prop))->Prop)) antisymm) (fun (R:(fofType->(fofType->Prop)))=> (forall (X:fofType) (Y:fofType), (((and ((R X) Y)) ((R Y) X))->(((eq fofType) X) Y))))) % Defined: antisymm:=(fun (R:(fofType->(fofType->Prop)))=> (forall (X:fofType) (Y:fofType), (((and ((R X) Y)) ((R Y) X))->(((eq fofType) X) Y)))) % FOF formula (<kernel.Constant object at 0x1619170>, <kernel.DependentProduct object at 0x142c680>) of role type named asymm_type % Using role type % Declaring asymm:((fofType->(fofType->Prop))->Prop) % FOF formula (((eq ((fofType->(fofType->Prop))->Prop)) asymm) (fun (R:(fofType->(fofType->Prop)))=> (forall (X:fofType) (Y:fofType), (((R X) Y)->(((R Y) X)->False))))) of role definition named asymmetric % A new definition: (((eq ((fofType->(fofType->Prop))->Prop)) asymm) (fun (R:(fofType->(fofType->Prop)))=> (forall (X:fofType) (Y:fofType), (((R X) Y)->(((R Y) X)->False))))) % Defined: asymm:=(fun (R:(fofType->(fofType->Prop)))=> (forall (X:fofType) (Y:fofType), (((R X) Y)->(((R Y) X)->False)))) % FOF formula (<kernel.Constant object at 0x16190e0>, <kernel.DependentProduct object at 0x142c248>) of role type named sc_type % Using role type % Declaring sc:((fofType->(fofType->Prop))->(fofType->(fofType->Prop))) % FOF formula (((eq ((fofType->(fofType->Prop))->(fofType->(fofType->Prop)))) sc) (fun (R:(fofType->(fofType->Prop))) (X:fofType) (Y:fofType)=> ((or ((R Y) X)) ((R X) Y)))) of role definition named symmetric_closure % A new definition: (((eq ((fofType->(fofType->Prop))->(fofType->(fofType->Prop)))) sc) (fun (R:(fofType->(fofType->Prop))) (X:fofType) (Y:fofType)=> ((or ((R Y) X)) ((R X) Y)))) % Defined: sc:=(fun (R:(fofType->(fofType->Prop))) (X:fofType) (Y:fofType)=> ((or ((R Y) X)) ((R X) Y))) % FOF formula (<kernel.Constant object at 0x142c7e8>, <kernel.DependentProduct object at 0x142c488>) of role type named trans_type % Using role type % Declaring trans:((fofType->(fofType->Prop))->Prop) % FOF formula (((eq ((fofType->(fofType->Prop))->Prop)) trans) (fun (R:(fofType->(fofType->Prop)))=> (forall (X:fofType) (Y:fofType) (Z:fofType), (((and ((R X) Y)) ((R Y) Z))->((R X) Z))))) of role definition named transitive % A new definition: (((eq ((fofType->(fofType->Prop))->Prop)) trans) (fun (R:(fofType->(fofType->Prop)))=> (forall (X:fofType) (Y:fofType) (Z:fofType), (((and ((R X) Y)) ((R Y) Z))->((R X) Z))))) % Defined: trans:=(fun (R:(fofType->(fofType->Prop)))=> (forall (X:fofType) (Y:fofType) (Z:fofType), (((and ((R X) Y)) ((R Y) Z))->((R X) Z)))) % FOF formula (<kernel.Constant object at 0x142c518>, <kernel.DependentProduct object at 0x142c908>) of role type named tc_type % Using role type % Declaring tc:((fofType->(fofType->Prop))->(fofType->(fofType->Prop))) % FOF formula (((eq ((fofType->(fofType->Prop))->(fofType->(fofType->Prop)))) tc) (fun (R:(fofType->(fofType->Prop))) (X:fofType) (Y:fofType)=> (forall (S:(fofType->(fofType->Prop))), (((and (trans S)) ((subrel R) S))->((S X) Y))))) of role definition named transitive_closure % A new definition: (((eq ((fofType->(fofType->Prop))->(fofType->(fofType->Prop)))) tc) (fun (R:(fofType->(fofType->Prop))) (X:fofType) (Y:fofType)=> (forall (S:(fofType->(fofType->Prop))), (((and (trans S)) ((subrel R) S))->((S X) Y))))) % Defined: tc:=(fun (R:(fofType->(fofType->Prop))) (X:fofType) (Y:fofType)=> (forall (S:(fofType->(fofType->Prop))), (((and (trans S)) ((subrel R) S))->((S X) Y)))) % FOF formula (<kernel.Constant object at 0x142c710>, <kernel.DependentProduct object at 0x142c440>) of role type named trc_type % Using role type % Declaring trc:((fofType->(fofType->Prop))->(fofType->(fofType->Prop))) % FOF formula (((eq ((fofType->(fofType->Prop))->(fofType->(fofType->Prop)))) trc) (fun (R:(fofType->(fofType->Prop)))=> (rc (tc R)))) of role definition named transitive_reflexive_closure % A new definition: (((eq ((fofType->(fofType->Prop))->(fofType->(fofType->Prop)))) trc) (fun (R:(fofType->(fofType->Prop)))=> (rc (tc R)))) % Defined: trc:=(fun (R:(fofType->(fofType->Prop)))=> (rc (tc R))) % FOF formula (<kernel.Constant object at 0x142c0e0>, <kernel.DependentProduct object at 0x142c9e0>) of role type named trsc_type % Using role type % Declaring trsc:((fofType->(fofType->Prop))->(fofType->(fofType->Prop))) % FOF formula (((eq ((fofType->(fofType->Prop))->(fofType->(fofType->Prop)))) trsc) (fun (R:(fofType->(fofType->Prop)))=> (sc (rc (tc R))))) of role definition named transitive_reflexive_symmetric_closure % A new definition: (((eq ((fofType->(fofType->Prop))->(fofType->(fofType->Prop)))) trsc) (fun (R:(fofType->(fofType->Prop)))=> (sc (rc (tc R))))) % Defined: trsc:=(fun (R:(fofType->(fofType->Prop)))=> (sc (rc (tc R)))) % FOF formula (<kernel.Constant object at 0x142c0e0>, <kernel.DependentProduct object at 0x142c5f0>) of role type named po_type % Using role type % Declaring po:((fofType->(fofType->Prop))->Prop) % FOF formula (((eq ((fofType->(fofType->Prop))->Prop)) po) (fun (R:(fofType->(fofType->Prop)))=> ((and ((and (refl R)) (antisymm R))) (trans R)))) of role definition named partial_order % A new definition: (((eq ((fofType->(fofType->Prop))->Prop)) po) (fun (R:(fofType->(fofType->Prop)))=> ((and ((and (refl R)) (antisymm R))) (trans R)))) % Defined: po:=(fun (R:(fofType->(fofType->Prop)))=> ((and ((and (refl R)) (antisymm R))) (trans R))) % FOF formula (<kernel.Constant object at 0x142c200>, <kernel.DependentProduct object at 0x142c5a8>) of role type named so_type % Using role type % Declaring so:((fofType->(fofType->Prop))->Prop) % FOF formula (((eq ((fofType->(fofType->Prop))->Prop)) so) (fun (R:(fofType->(fofType->Prop)))=> ((and (asymm R)) (trans R)))) of role definition named strict_order % A new definition: (((eq ((fofType->(fofType->Prop))->Prop)) so) (fun (R:(fofType->(fofType->Prop)))=> ((and (asymm R)) (trans R)))) % Defined: so:=(fun (R:(fofType->(fofType->Prop)))=> ((and (asymm R)) (trans R))) % FOF formula (<kernel.Constant object at 0x142c5f0>, <kernel.DependentProduct object at 0x142c4d0>) of role type named total_type % Using role type % Declaring total:((fofType->(fofType->Prop))->Prop) % FOF formula (((eq ((fofType->(fofType->Prop))->Prop)) total) (fun (R:(fofType->(fofType->Prop)))=> (forall (X:fofType) (Y:fofType), ((or ((or (((eq fofType) X) Y)) ((R X) Y))) ((R Y) X))))) of role definition named total % A new definition: (((eq ((fofType->(fofType->Prop))->Prop)) total) (fun (R:(fofType->(fofType->Prop)))=> (forall (X:fofType) (Y:fofType), ((or ((or (((eq fofType) X) Y)) ((R X) Y))) ((R Y) X))))) % Defined: total:=(fun (R:(fofType->(fofType->Prop)))=> (forall (X:fofType) (Y:fofType), ((or ((or (((eq fofType) X) Y)) ((R X) Y))) ((R Y) X)))) % FOF formula (<kernel.Constant object at 0x142c4d0>, <kernel.DependentProduct object at 0x142cb48>) of role type named term_type % Using role type % Declaring term:((fofType->(fofType->Prop))->Prop) % FOF formula (((eq ((fofType->(fofType->Prop))->Prop)) term) (fun (R:(fofType->(fofType->Prop)))=> (forall (A:(fofType->Prop)), (((ex fofType) (fun (X:fofType)=> (A X)))->((ex fofType) (fun (X:fofType)=> ((and (A X)) (forall (Y:fofType), ((A Y)->(((R X) Y)->False)))))))))) of role definition named terminating % A new definition: (((eq ((fofType->(fofType->Prop))->Prop)) term) (fun (R:(fofType->(fofType->Prop)))=> (forall (A:(fofType->Prop)), (((ex fofType) (fun (X:fofType)=> (A X)))->((ex fofType) (fun (X:fofType)=> ((and (A X)) (forall (Y:fofType), ((A Y)->(((R X) Y)->False)))))))))) % Defined: term:=(fun (R:(fofType->(fofType->Prop)))=> (forall (A:(fofType->Prop)), (((ex fofType) (fun (X:fofType)=> (A X)))->((ex fofType) (fun (X:fofType)=> ((and (A X)) (forall (Y:fofType), ((A Y)->(((R X) Y)->False))))))))) % FOF formula (<kernel.Constant object at 0x142cbd8>, <kernel.DependentProduct object at 0x142ccf8>) of role type named ind_type % Using role type % Declaring ind:((fofType->(fofType->Prop))->Prop) % FOF formula (((eq ((fofType->(fofType->Prop))->Prop)) ind) (fun (R:(fofType->(fofType->Prop)))=> (forall (P:(fofType->Prop)), ((forall (X:fofType), ((forall (Y:fofType), ((((tc R) X) Y)->(P Y)))->(P X)))->(forall (X:fofType), (P X)))))) of role definition named satisfying_the_induction_principle % A new definition: (((eq ((fofType->(fofType->Prop))->Prop)) ind) (fun (R:(fofType->(fofType->Prop)))=> (forall (P:(fofType->Prop)), ((forall (X:fofType), ((forall (Y:fofType), ((((tc R) X) Y)->(P Y)))->(P X)))->(forall (X:fofType), (P X)))))) % Defined: ind:=(fun (R:(fofType->(fofType->Prop)))=> (forall (P:(fofType->Prop)), ((forall (X:fofType), ((forall (Y:fofType), ((((tc R) X) Y)->(P Y)))->(P X)))->(forall (X:fofType), (P X))))) % FOF formula (<kernel.Constant object at 0x142c1b8>, <kernel.DependentProduct object at 0x142cbd8>) of role type named innf_type % Using role type % Declaring innf:((fofType->(fofType->Prop))->(fofType->Prop)) % FOF formula (((eq ((fofType->(fofType->Prop))->(fofType->Prop))) innf) (fun (R:(fofType->(fofType->Prop))) (X:fofType)=> (((ex fofType) (fun (Y:fofType)=> ((R X) Y)))->False))) of role definition named in_normal_form % A new definition: (((eq ((fofType->(fofType->Prop))->(fofType->Prop))) innf) (fun (R:(fofType->(fofType->Prop))) (X:fofType)=> (((ex fofType) (fun (Y:fofType)=> ((R X) Y)))->False))) % Defined: innf:=(fun (R:(fofType->(fofType->Prop))) (X:fofType)=> (((ex fofType) (fun (Y:fofType)=> ((R X) Y)))->False)) % FOF formula (<kernel.Constant object at 0x142ccf8>, <kernel.DependentProduct object at 0x142c0e0>) of role type named nfof_type % Using role type % Declaring nfof:((fofType->(fofType->Prop))->(fofType->(fofType->Prop))) % FOF formula (((eq ((fofType->(fofType->Prop))->(fofType->(fofType->Prop)))) nfof) (fun (R:(fofType->(fofType->Prop))) (X:fofType) (Y:fofType)=> ((and (((trc R) Y) X)) ((innf R) X)))) of role definition named normal_form_of % A new definition: (((eq ((fofType->(fofType->Prop))->(fofType->(fofType->Prop)))) nfof) (fun (R:(fofType->(fofType->Prop))) (X:fofType) (Y:fofType)=> ((and (((trc R) Y) X)) ((innf R) X)))) % Defined: nfof:=(fun (R:(fofType->(fofType->Prop))) (X:fofType) (Y:fofType)=> ((and (((trc R) Y) X)) ((innf R) X))) % FOF formula (<kernel.Constant object at 0x142c1b8>, <kernel.DependentProduct object at 0x142cd88>) of role type named norm_type % Using role type % Declaring norm:((fofType->(fofType->Prop))->Prop) % FOF formula (((eq ((fofType->(fofType->Prop))->Prop)) norm) (fun (R:(fofType->(fofType->Prop)))=> (forall (X:fofType), ((ex fofType) (fun (Y:fofType)=> (((nfof R) Y) X)))))) of role definition named normalizing % A new definition: (((eq ((fofType->(fofType->Prop))->Prop)) norm) (fun (R:(fofType->(fofType->Prop)))=> (forall (X:fofType), ((ex fofType) (fun (Y:fofType)=> (((nfof R) Y) X)))))) % Defined: norm:=(fun (R:(fofType->(fofType->Prop)))=> (forall (X:fofType), ((ex fofType) (fun (Y:fofType)=> (((nfof R) Y) X))))) % FOF formula (<kernel.Constant object at 0x142c1b8>, <kernel.DependentProduct object at 0x142cf80>) of role type named join_type % Using role type % Declaring join:((fofType->(fofType->Prop))->(fofType->(fofType->Prop))) % FOF formula (((eq ((fofType->(fofType->Prop))->(fofType->(fofType->Prop)))) join) (fun (R:(fofType->(fofType->Prop))) (X:fofType) (Y:fofType)=> ((ex fofType) (fun (Z:fofType)=> ((and (((trc R) X) Z)) (((trc R) Y) Z)))))) of role definition named joinable % A new definition: (((eq ((fofType->(fofType->Prop))->(fofType->(fofType->Prop)))) join) (fun (R:(fofType->(fofType->Prop))) (X:fofType) (Y:fofType)=> ((ex fofType) (fun (Z:fofType)=> ((and (((trc R) X) Z)) (((trc R) Y) Z)))))) % Defined: join:=(fun (R:(fofType->(fofType->Prop))) (X:fofType) (Y:fofType)=> ((ex fofType) (fun (Z:fofType)=> ((and (((trc R) X) Z)) (((trc R) Y) Z))))) % FOF formula (<kernel.Constant object at 0x142c680>, <kernel.DependentProduct object at 0x16063f8>) of role type named lconfl_type % Using role type % Declaring lconfl:((fofType->(fofType->Prop))->Prop) % FOF formula (((eq ((fofType->(fofType->Prop))->Prop)) lconfl) (fun (R:(fofType->(fofType->Prop)))=> (forall (X:fofType) (Y:fofType) (Z:fofType), (((and ((R X) Z)) ((R X) Y))->(((join R) Z) Y))))) of role definition named locally_confluent % A new definition: (((eq ((fofType->(fofType->Prop))->Prop)) lconfl) (fun (R:(fofType->(fofType->Prop)))=> (forall (X:fofType) (Y:fofType) (Z:fofType), (((and ((R X) Z)) ((R X) Y))->(((join R) Z) Y))))) % Defined: lconfl:=(fun (R:(fofType->(fofType->Prop)))=> (forall (X:fofType) (Y:fofType) (Z:fofType), (((and ((R X) Z)) ((R X) Y))->(((join R) Z) Y)))) % FOF formula (<kernel.Constant object at 0x142c1b8>, <kernel.DependentProduct object at 0x1606050>) of role type named sconfl_type % Using role type % Declaring sconfl:((fofType->(fofType->Prop))->Prop) % FOF formula (((eq ((fofType->(fofType->Prop))->Prop)) sconfl) (fun (R:(fofType->(fofType->Prop)))=> (forall (X:fofType) (Y:fofType) (Z:fofType), (((and ((R X) Z)) (((trc R) X) Y))->(((join R) Z) Y))))) of role definition named semi_confluent % A new definition: (((eq ((fofType->(fofType->Prop))->Prop)) sconfl) (fun (R:(fofType->(fofType->Prop)))=> (forall (X:fofType) (Y:fofType) (Z:fofType), (((and ((R X) Z)) (((trc R) X) Y))->(((join R) Z) Y))))) % Defined: sconfl:=(fun (R:(fofType->(fofType->Prop)))=> (forall (X:fofType) (Y:fofType) (Z:fofType), (((and ((R X) Z)) (((trc R) X) Y))->(((join R) Z) Y)))) % FOF formula (<kernel.Constant object at 0x16063f8>, <kernel.DependentProduct object at 0x1606440>) of role type named confl_type % Using role type % Declaring confl:((fofType->(fofType->Prop))->Prop) % FOF formula (((eq ((fofType->(fofType->Prop))->Prop)) confl) (fun (R:(fofType->(fofType->Prop)))=> (forall (X:fofType) (Y:fofType) (Z:fofType), (((and (((trc R) X) Z)) (((trc R) X) Y))->(((join R) Z) Y))))) of role definition named confluent % A new definition: (((eq ((fofType->(fofType->Prop))->Prop)) confl) (fun (R:(fofType->(fofType->Prop)))=> (forall (X:fofType) (Y:fofType) (Z:fofType), (((and (((trc R) X) Z)) (((trc R) X) Y))->(((join R) Z) Y))))) % Defined: confl:=(fun (R:(fofType->(fofType->Prop)))=> (forall (X:fofType) (Y:fofType) (Z:fofType), (((and (((trc R) X) Z)) (((trc R) X) Y))->(((join R) Z) Y)))) % FOF formula (<kernel.Constant object at 0x1606050>, <kernel.DependentProduct object at 0x1606320>) of role type named cr_type % Using role type % Declaring cr:((fofType->(fofType->Prop))->Prop) % FOF formula (((eq ((fofType->(fofType->Prop))->Prop)) cr) (fun (R:(fofType->(fofType->Prop)))=> (forall (X:fofType) (Y:fofType), ((((trsc R) X) Y)->(((join R) X) Y))))) of role definition named church_rosser % A new definition: (((eq ((fofType->(fofType->Prop))->Prop)) cr) (fun (R:(fofType->(fofType->Prop)))=> (forall (X:fofType) (Y:fofType), ((((trsc R) X) Y)->(((join R) X) Y))))) % Defined: cr:=(fun (R:(fofType->(fofType->Prop)))=> (forall (X:fofType) (Y:fofType), ((((trsc R) X) Y)->(((join R) X) Y)))) % FOF formula (forall (R:(fofType->(fofType->Prop))), ((po R)->(po (inv R)))) of role conjecture named inverse_of_partial_order_is_partial_order % Conjecture to prove = (forall (R:(fofType->(fofType->Prop))), ((po R)->(po (inv R)))):Prop % Parameter fofType_DUMMY:fofType. % We need to prove ['(forall (R:(fofType->(fofType->Prop))), ((po R)->(po (inv R))))'] % Parameter fofType:Type. % Definition subrel:=(fun (R:(fofType->(fofType->Prop))) (S:(fofType->(fofType->Prop)))=> (forall (X:fofType) (Y:fofType), (((R X) Y)->((S X) Y)))):((fofType->(fofType->Prop))->((fofType->(fofType->Prop))->Prop)). % Definition inv:=(fun (R:(fofType->(fofType->Prop))) (X:fofType) (Y:fofType)=> ((R Y) X)):((fofType->(fofType->Prop))->(fofType->(fofType->Prop))). % Definition idem:=(fun (F:((fofType->(fofType->Prop))->(fofType->(fofType->Prop))))=> (forall (R:(fofType->(fofType->Prop))), (((eq (fofType->(fofType->Prop))) (F (F R))) (F R)))):(((fofType->(fofType->Prop))->(fofType->(fofType->Prop)))->Prop). % Definition infl:=(fun (F:((fofType->(fofType->Prop))->(fofType->(fofType->Prop))))=> (forall (R:(fofType->(fofType->Prop))), ((subrel R) (F R)))):(((fofType->(fofType->Prop))->(fofType->(fofType->Prop)))->Prop). % Definition mono:=(fun (F:((fofType->(fofType->Prop))->(fofType->(fofType->Prop))))=> (forall (R:(fofType->(fofType->Prop))) (S:(fofType->(fofType->Prop))), (((subrel R) S)->((subrel (F R)) (F S))))):(((fofType->(fofType->Prop))->(fofType->(fofType->Prop)))->Prop). % Definition refl:=(fun (R:(fofType->(fofType->Prop)))=> (forall (X:fofType), ((R X) X))):((fofType->(fofType->Prop))->Prop). % Definition irrefl:=(fun (R:(fofType->(fofType->Prop)))=> (forall (X:fofType), (((R X) X)->False))):((fofType->(fofType->Prop))->Prop). % Definition rc:=(fun (R:(fofType->(fofType->Prop))) (X:fofType) (Y:fofType)=> ((or (((eq fofType) X) Y)) ((R X) Y))):((fofType->(fofType->Prop))->(fofType->(fofType->Prop))). % Definition symm:=(fun (R:(fofType->(fofType->Prop)))=> (forall (X:fofType) (Y:fofType), (((R X) Y)->((R Y) X)))):((fofType->(fofType->Prop))->Prop). % Definition antisymm:=(fun (R:(fofType->(fofType->Prop)))=> (forall (X:fofType) (Y:fofType), (((and ((R X) Y)) ((R Y) X))->(((eq fofType) X) Y)))):((fofType->(fofType->Prop))->Prop). % Definition asymm:=(fun (R:(fofType->(fofType->Prop)))=> (forall (X:fofType) (Y:fofType), (((R X) Y)->(((R Y) X)->False)))):((fofType->(fofType->Prop))->Prop). % Definition sc:=(fun (R:(fofType->(fofType->Prop))) (X:fofType) (Y:fofType)=> ((or ((R Y) X)) ((R X) Y))):((fofType->(fofType->Prop))->(fofType->(fofType->Prop))). % Definition trans:=(fun (R:(fofType->(fofType->Prop)))=> (forall (X:fofType) (Y:fofType) (Z:fofType), (((and ((R X) Y)) ((R Y) Z))->((R X) Z)))):((fofType->(fofType->Prop))->Prop). % Definition tc:=(fun (R:(fofType->(fofType->Prop))) (X:fofType) (Y:fofType)=> (forall (S:(fofType->(fofType->Prop))), (((and (trans S)) ((subrel R) S))->((S X) Y)))):((fofType->(fofType->Prop))->(fofType->(fofType->Prop))). % Definition trc:=(fun (R:(fofType->(fofType->Prop)))=> (rc (tc R))):((fofType->(fofType->Prop))->(fofType->(fofType->Prop))). % Definition trsc:=(fun (R:(fofType->(fofType->Prop)))=> (sc (rc (tc R)))):((fofType->(fofType->Prop))->(fofType->(fofType->Prop))). % Definition po:=(fun (R:(fofType->(fofType->Prop)))=> ((and ((and (refl R)) (antisymm R))) (trans R))):((fofType->(fofType->Prop))->Prop). % Definition so:=(fun (R:(fofType->(fofType->Prop)))=> ((and (asymm R)) (trans R))):((fofType->(fofType->Prop))->Prop). % Definition total:=(fun (R:(fofType->(fofType->Prop)))=> (forall (X:fofType) (Y:fofType), ((or ((or (((eq fofType) X) Y)) ((R X) Y))) ((R Y) X)))):((fofType->(fofType->Prop))->Prop). % Definition term:=(fun (R:(fofType->(fofType->Prop)))=> (forall (A:(fofType->Prop)), (((ex fofType) (fun (X:fofType)=> (A X)))->((ex fofType) (fun (X:fofType)=> ((and (A X)) (forall (Y:fofType), ((A Y)->(((R X) Y)->False))))))))):((fofType->(fofType->Prop))->Prop). % Definition ind:=(fun (R:(fofType->(fofType->Prop)))=> (forall (P:(fofType->Prop)), ((forall (X:fofType), ((forall (Y:fofType), ((((tc R) X) Y)->(P Y)))->(P X)))->(forall (X:fofType), (P X))))):((fofType->(fofType->Prop))->Prop). % Definition innf:=(fun (R:(fofType->(fofType->Prop))) (X:fofType)=> (((ex fofType) (fun (Y:fofType)=> ((R X) Y)))->False)):((fofType->(fofType->Prop))->(fofType->Prop)). % Definition nfof:=(fun (R:(fofType->(fofType->Prop))) (X:fofType) (Y:fofType)=> ((and (((trc R) Y) X)) ((innf R) X))):((fofType->(fofType->Prop))->(fofType->(fofType->Prop))). % Definition norm:=(fun (R:(fofType->(fofType->Prop)))=> (forall (X:fofType), ((ex fofType) (fun (Y:fofType)=> (((nfof R) Y) X))))):((fofType->(fofType->Prop))->Prop). % Definition join:=(fun (R:(fofType->(fofType->Prop))) (X:fofType) (Y:fofType)=> ((ex fofType) (fun (Z:fofType)=> ((and (((trc R) X) Z)) (((trc R) Y) Z))))):((fofType->(fofType->Prop))->(fofType->(fofType->Prop))). % Definition lconfl:=(fun (R:(fofType->(fofType->Prop)))=> (forall (X:fofType) (Y:fofType) (Z:fofType), (((and ((R X) Z)) ((R X) Y))->(((join R) Z) Y)))):((fofType->(fofType->Prop))->Prop). % Definition sconfl:=(fun (R:(fofType->(fofType->Prop)))=> (forall (X:fofType) (Y:fofType) (Z:fofType), (((and ((R X) Z)) (((trc R) X) Y))->(((join R) Z) Y)))):((fofType->(fofType->Prop))->Prop). % Definition confl:=(fun (R:(fofType->(fofType->Prop)))=> (forall (X:fofType) (Y:fofType) (Z:fofType), (((and (((trc R) X) Z)) (((trc R) X) Y))->(((join R) Z) Y)))):((fofType->(fofType->Prop))->Prop). % Definition cr:=(fun (R:(fofType->(fofType->Prop)))=> (forall (X:fofType) (Y:fofType), ((((trsc R) X) Y)->(((join R) X) Y)))):((fofType->(fofType->Prop))->Prop). % Trying to prove (forall (R:(fofType->(fofType->Prop))), ((po R)->(po (inv R)))) % Found x2:(refl R) % Found x2 as proof of (refl (inv R)) % Found x2:(refl R) % Found x2 as proof of (refl (inv R)) % Found x2:(refl R) % Found (fun (x3:(antisymm R))=> x2) as proof of (refl (inv R)) % Found (fun (x2:(refl R)) (x3:(antisymm R))=> x2) as proof of ((antisymm R)->(refl (inv R))) % Found (fun (x2:(refl R)) (x3:(antisymm R))=> x2) as proof of ((refl R)->((antisymm R)->(refl (inv R)))) % Found (and_rect10 (fun (x2:(refl R)) (x3:(antisymm R))=> x2)) as proof of (refl (inv R)) % Found ((and_rect1 (refl (inv R))) (fun (x2:(refl R)) (x3:(antisymm R))=> x2)) as proof of (refl (inv R)) % Found (((fun (P:Type) (x2:((refl R)->((antisymm R)->P)))=> (((((and_rect (refl R)) (antisymm R)) P) x2) x0)) (refl (inv R))) (fun (x2:(refl R)) (x3:(antisymm R))=> x2)) as proof of (refl (inv R)) % Found (((fun (P:Type) (x2:((refl R)->((antisymm R)->P)))=> (((((and_rect (refl R)) (antisymm R)) P) x2) x0)) (refl (inv R))) (fun (x2:(refl R)) (x3:(antisymm R))=> x2)) as proof of (refl (inv R)) % Found x60:(((inv R) Y) Z) % Found (fun (x60:(((inv R) Y) Z))=> x60) as proof of (((inv R) Y) Z) % Found (fun (x60:(((inv R) Y) Z))=> x60) as proof of (P Y) % Found x50:(P X) % Found (fun (x50:(P X))=> x50) as proof of (P X) % Found (fun (x50:(P X))=> x50) as proof of (P0 X) % Found x20:=(x2 Y0):((R Y0) Y0) % Found (x2 Y0) as proof of ((R Y0) X) % Found (x2 Y0) as proof of ((R Y0) X) % Found (x2 Y0) as proof of ((R Y0) X) % Found x20:=(x2 Z):((R Z) Z) % Found (x2 Z) as proof of ((R Z) Y0) % Found (x2 Z) as proof of ((R Z) Y0) % Found (x2 Z) as proof of ((R Z) Y0) % Found x50:(P X) % Found (fun (x50:(P X))=> x50) as proof of (P X) % Found (fun (x50:(P X))=> x50) as proof of (P0 X) % Found x50:(P X) % Found (fun (x50:(P X))=> x50) as proof of (P X) % Found (fun (x50:(P X))=> x50) as proof of (P0 X) % Found x4:(((inv R) Y) Z) % Instantiate: Y0:=Y:fofType % Found x4 as proof of ((R Z) Y0) % Found x3:(((inv R) X) Y) % Instantiate: Y0:=Y:fofType % Found x3 as proof of ((R Y0) X) % Found ((conj10 x4) x3) as proof of ((and ((R Z) Y0)) ((R Y0) X)) % Found (((conj1 ((R Y0) X)) x4) x3) as proof of ((and ((R Z) Y0)) ((R Y0) X)) % Found ((((conj ((R Z) Y0)) ((R Y0) X)) x4) x3) as proof of ((and ((R Z) Y0)) ((R Y0) X)) % Found ((((conj ((R Z) Y0)) ((R Y0) X)) x4) x3) as proof of ((and ((R Z) Y0)) ((R Y0) X)) % Found (x1000 ((((conj ((R Z) Y0)) ((R Y0) X)) x4) x3)) as proof of (((inv R) X) Z) % Found ((x100 Y) ((((conj ((R Z) Y)) ((R Y) X)) x4) x3)) as proof of (((inv R) X) Z) % Found (((fun (Y0:fofType)=> ((x10 Y0) X)) Y) ((((conj ((R Z) Y)) ((R Y) X)) x4) x3)) as proof of (((inv R) X) Z) % Found (((fun (Y0:fofType)=> (((x1 Z) Y0) X)) Y) ((((conj ((R Z) Y)) ((R Y) X)) x4) x3)) as proof of (((inv R) X) Z) % Found (fun (x4:(((inv R) Y) Z))=> (((fun (Y0:fofType)=> (((x1 Z) Y0) X)) Y) ((((conj ((R Z) Y)) ((R Y) X)) x4) x3))) as proof of (((inv R) X) Z) % Found (fun (x3:(((inv R) X) Y)) (x4:(((inv R) Y) Z))=> (((fun (Y0:fofType)=> (((x1 Z) Y0) X)) Y) ((((conj ((R Z) Y)) ((R Y) X)) x4) x3))) as proof of ((((inv R) Y) Z)->(((inv R) X) Z)) % Found (fun (x3:(((inv R) X) Y)) (x4:(((inv R) Y) Z))=> (((fun (Y0:fofType)=> (((x1 Z) Y0) X)) Y) ((((conj ((R Z) Y)) ((R Y) X)) x4) x3))) as proof of ((((inv R) X) Y)->((((inv R) Y) Z)->(((inv R) X) Z))) % Found (and_rect10 (fun (x3:(((inv R) X) Y)) (x4:(((inv R) Y) Z))=> (((fun (Y0:fofType)=> (((x1 Z) Y0) X)) Y) ((((conj ((R Z) Y)) ((R Y) X)) x4) x3)))) as proof of (((inv R) X) Z) % Found ((and_rect1 (((inv R) X) Z)) (fun (x3:(((inv R) X) Y)) (x4:(((inv R) Y) Z))=> (((fun (Y0:fofType)=> (((x1 Z) Y0) X)) Y) ((((conj ((R Z) Y)) ((R Y) X)) x4) x3)))) as proof of (((inv R) X) Z) % Found (((fun (P:Type) (x3:((((inv R) X) Y)->((((inv R) Y) Z)->P)))=> (((((and_rect (((inv R) X) Y)) (((inv R) Y) Z)) P) x3) x2)) (((inv R) X) Z)) (fun (x3:(((inv R) X) Y)) (x4:(((inv R) Y) Z))=> (((fun (Y0:fofType)=> (((x1 Z) Y0) X)) Y) ((((conj ((R Z) Y)) ((R Y) X)) x4) x3)))) as proof of (((inv R) X) Z) % Found (fun (x2:((and (((inv R) X) Y)) (((inv R) Y) Z)))=> (((fun (P:Type) (x3:((((inv R) X) Y)->((((inv R) Y) Z)->P)))=> (((((and_rect (((inv R) X) Y)) (((inv R) Y) Z)) P) x3) x2)) (((inv R) X) Z)) (fun (x3:(((inv R) X) Y)) (x4:(((inv R) Y) Z))=> (((fun (Y0:fofType)=> (((x1 Z) Y0) X)) Y) ((((conj ((R Z) Y)) ((R Y) X)) x4) x3))))) as proof of (((inv R) X) Z) % Found (fun (Z:fofType) (x2:((and (((inv R) X) Y)) (((inv R) Y) Z)))=> (((fun (P:Type) (x3:((((inv R) X) Y)->((((inv R) Y) Z)->P)))=> (((((and_rect (((inv R) X) Y)) (((inv R) Y) Z)) P) x3) x2)) (((inv R) X) Z)) (fun (x3:(((inv R) X) Y)) (x4:(((inv R) Y) Z))=> (((fun (Y0:fofType)=> (((x1 Z) Y0) X)) Y) ((((conj ((R Z) Y)) ((R Y) X)) x4) x3))))) as proof of (((and (((inv R) X) Y)) (((inv R) Y) Z))->(((inv R) X) Z)) % Found (fun (Y:fofType) (Z:fofType) (x2:((and (((inv R) X) Y)) (((inv R) Y) Z)))=> (((fun (P:Type) (x3:((((inv R) X) Y)->((((inv R) Y) Z)->P)))=> (((((and_rect (((inv R) X) Y)) (((inv R) Y) Z)) P) x3) x2)) (((inv R) X) Z)) (fun (x3:(((inv R) X) Y)) (x4:(((inv R) Y) Z))=> (((fun (Y0:fofType)=> (((x1 Z) Y0) X)) Y) ((((conj ((R Z) Y)) ((R Y) X)) x4) x3))))) as proof of (forall (Z:fofType), (((and (((inv R) X) Y)) (((inv R) Y) Z))->(((inv R) X) Z))) % Found (fun (X:fofType) (Y:fofType) (Z:fofType) (x2:((and (((inv R) X) Y)) (((inv R) Y) Z)))=> (((fun (P:Type) (x3:((((inv R) X) Y)->((((inv R) Y) Z)->P)))=> (((((and_rect (((inv R) X) Y)) (((inv R) Y) Z)) P) x3) x2)) (((inv R) X) Z)) (fun (x3:(((inv R) X) Y)) (x4:(((inv R) Y) Z))=> (((fun (Y0:fofType)=> (((x1 Z) Y0) X)) Y) ((((conj ((R Z) Y)) ((R Y) X)) x4) x3))))) as proof of (forall (Y:fofType) (Z:fofType), (((and (((inv R) X) Y)) (((inv R) Y) Z))->(((inv R) X) Z))) % Found (fun (X:fofType) (Y:fofType) (Z:fofType) (x2:((and (((inv R) X) Y)) (((inv R) Y) Z)))=> (((fun (P:Type) (x3:((((inv R) X) Y)->((((inv R) Y) Z)->P)))=> (((((and_rect (((inv R) X) Y)) (((inv R) Y) Z)) P) x3) x2)) (((inv R) X) Z)) (fun (x3:(((inv R) X) Y)) (x4:(((inv R) Y) Z))=> (((fun (Y0:fofType)=> (((x1 Z) Y0) X)) Y) ((((conj ((R Z) Y)) ((R Y) X)) x4) x3))))) as proof of (trans (inv R)) % Found x4000:=(x400 x2):(((eq fofType) Y) X) % Found (x400 x2) as proof of (((eq fofType) Y) X) % Found ((x40 X) x2) as proof of (((eq fofType) Y) X) % Found (((x4 Y) X) x2) as proof of (((eq fofType) Y) X) % Found (((x4 Y) X) x2) as proof of (((eq fofType) Y) X) % Found (eq_sym000 (((x4 Y) X) x2)) as proof of (((eq fofType) X) Y) % Found ((eq_sym00 X) (((x4 Y) X) x2)) as proof of (((eq fofType) X) Y) % Found (((eq_sym0 Y) X) (((x4 Y) X) x2)) as proof of (((eq fofType) X) Y) % Found ((((eq_sym fofType) Y) X) (((x4 Y) X) x2)) as proof of (((eq fofType) X) Y) % Found (fun (x4:(antisymm R))=> ((((eq_sym fofType) Y) X) (((x4 Y) X) x2))) as proof of (((eq fofType) X) Y) % Found (fun (x3:(refl R)) (x4:(antisymm R))=> ((((eq_sym fofType) Y) X) (((x4 Y) X) x2))) as proof of ((antisymm R)->(((eq fofType) X) Y)) % Found (fun (x3:(refl R)) (x4:(antisymm R))=> ((((eq_sym fofType) Y) X) (((x4 Y) X) x2))) as proof of ((refl R)->((antisymm R)->(((eq fofType) X) Y))) % Found (and_rect10 (fun (x3:(refl R)) (x4:(antisymm R))=> ((((eq_sym fofType) Y) X) (((x4 Y) X) x2)))) as proof of (((eq fofType) X) Y) % Found ((and_rect1 (((eq fofType) X) Y)) (fun (x3:(refl R)) (x4:(antisymm R))=> ((((eq_sym fofType) Y) X) (((x4 Y) X) x2)))) as proof of (((eq fofType) X) Y) % Found (((fun (P:Type) (x3:((refl R)->((antisymm R)->P)))=> (((((and_rect (refl R)) (antisymm R)) P) x3) x0)) (((eq fofType) X) Y)) (fun (x3:(refl R)) (x4:(antisymm R))=> ((((eq_sym fofType) Y) X) (((x4 Y) X) x2)))) as proof of (((eq fofType) X) Y) % Found (fun (x2:((and (((inv R) X) Y)) (((inv R) Y) X)))=> (((fun (P:Type) (x3:((refl R)->((antisymm R)->P)))=> (((((and_rect (refl R)) (antisymm R)) P) x3) x0)) (((eq fofType) X) Y)) (fun (x3:(refl R)) (x4:(antisymm R))=> ((((eq_sym fofType) Y) X) (((x4 Y) X) x2))))) as proof of (((eq fofType) X) Y) % Found (fun (Y:fofType) (x2:((and (((inv R) X) Y)) (((inv R) Y) X)))=> (((fun (P:Type) (x3:((refl R)->((antisymm R)->P)))=> (((((and_rect (refl R)) (antisymm R)) P) x3) x0)) (((eq fofType) X) Y)) (fun (x3:(refl R)) (x4:(antisymm R))=> ((((eq_sym fofType) Y) X) (((x4 Y) X) x2))))) as proof of (((and (((inv R) X) Y)) (((inv R) Y) X))->(((eq fofType) X) Y)) % Found (fun (X:fofType) (Y:fofType) (x2:((and (((inv R) X) Y)) (((inv R) Y) X)))=> (((fun (P:Type) (x3:((refl R)->((antisymm R)->P)))=> (((((and_rect (refl R)) (antisymm R)) P) x3) x0)) (((eq fofType) X) Y)) (fun (x3:(refl R)) (x4:(antisymm R))=> ((((eq_sym fofType) Y) X) (((x4 Y) X) x2))))) as proof of (forall (Y:fofType), (((and (((inv R) X) Y)) (((inv R) Y) X))->(((eq fofType) X) Y))) % Found (fun (X:fofType) (Y:fofType) (x2:((and (((inv R) X) Y)) (((inv R) Y) X)))=> (((fun (P:Type) (x3:((refl R)->((antisymm R)->P)))=> (((((and_rect (refl R)) (antisymm R)) P) x3) x0)) (((eq fofType) X) Y)) (fun (x3:(refl R)) (x4:(antisymm R))=> ((((eq_sym fofType) Y) X) (((x4 Y) X) x2))))) as proof of (antisymm (inv R)) % Found ((conj10 (((fun (P:Type) (x2:((refl R)->((antisymm R)->P)))=> (((((and_rect (refl R)) (antisymm R)) P) x2) x0)) (refl (inv R))) (fun (x2:(refl R)) (x3:(antisymm R))=> x2))) (fun (X:fofType) (Y:fofType) (x2:((and (((inv R) X) Y)) (((inv R) Y) X)))=> (((fun (P:Type) (x3:((refl R)->((antisymm R)->P)))=> (((((and_rect (refl R)) (antisymm R)) P) x3) x0)) (((eq fofType) X) Y)) (fun (x3:(refl R)) (x4:(antisymm R))=> ((((eq_sym fofType) Y) X) (((x4 Y) X) x2)))))) as proof of ((and (refl (inv R))) (antisymm (inv R))) % Found (((conj1 (antisymm (inv R))) (((fun (P:Type) (x2:((refl R)->((antisymm R)->P)))=> (((((and_rect (refl R)) (antisymm R)) P) x2) x0)) (refl (inv R))) (fun (x2:(refl R)) (x3:(antisymm R))=> x2))) (fun (X:fofType) (Y:fofType) (x2:((and (((inv R) X) Y)) (((inv R) Y) X)))=> (((fun (P:Type) (x3:((refl R)->((antisymm R)->P)))=> (((((and_rect (refl R)) (antisymm R)) P) x3) x0)) (((eq fofType) X) Y)) (fun (x3:(refl R)) (x4:(antisymm R))=> ((((eq_sym fofType) Y) X) (((x4 Y) X) x2)))))) as proof of ((and (refl (inv R))) (antisymm (inv R))) % Found ((((conj (refl (inv R))) (antisymm (inv R))) (((fun (P:Type) (x2:((refl R)->((antisymm R)->P)))=> (((((and_rect (refl R)) (antisymm R)) P) x2) x0)) (refl (inv R))) (fun (x2:(refl R)) (x3:(antisymm R))=> x2))) (fun (X:fofType) (Y:fofType) (x2:((and (((inv R) X) Y)) (((inv R) Y) X)))=> (((fun (P:Type) (x3:((refl R)->((antisymm R)->P)))=> (((((and_rect (refl R)) (antisymm R)) P) x3) x0)) (((eq fofType) X) Y)) (fun (x3:(refl R)) (x4:(antisymm R))=> ((((eq_sym fofType) Y) X) (((x4 Y) X) x2)))))) as proof of ((and (refl (inv R))) (antisymm (inv R))) % Found ((((conj (refl (inv R))) (antisymm (inv R))) (((fun (P:Type) (x2:((refl R)->((antisymm R)->P)))=> (((((and_rect (refl R)) (antisymm R)) P) x2) x0)) (refl (inv R))) (fun (x2:(refl R)) (x3:(antisymm R))=> x2))) (fun (X:fofType) (Y:fofType) (x2:((and (((inv R) X) Y)) (((inv R) Y) X)))=> (((fun (P:Type) (x3:((refl R)->((antisymm R)->P)))=> (((((and_rect (refl R)) (antisymm R)) P) x3) x0)) (((eq fofType) X) Y)) (fun (x3:(refl R)) (x4:(antisymm R))=> ((((eq_sym fofType) Y) X) (((x4 Y) X) x2)))))) as proof of ((and (refl (inv R))) (antisymm (inv R))) % Found ((conj00 ((((conj (refl (inv R))) (antisymm (inv R))) (((fun (P:Type) (x2:((refl R)->((antisymm R)->P)))=> (((((and_rect (refl R)) (antisymm R)) P) x2) x0)) (refl (inv R))) (fun (x2:(refl R)) (x3:(antisymm R))=> x2))) (fun (X:fofType) (Y:fofType) (x2:((and (((inv R) X) Y)) (((inv R) Y) X)))=> (((fun (P:Type) (x3:((refl R)->((antisymm R)->P)))=> (((((and_rect (refl R)) (antisymm R)) P) x3) x0)) (((eq fofType) X) Y)) (fun (x3:(refl R)) (x4:(antisymm R))=> ((((eq_sym fofType) Y) X) (((x4 Y) X) x2))))))) (fun (X:fofType) (Y:fofType) (Z:fofType) (x2:((and (((inv R) X) Y)) (((inv R) Y) Z)))=> (((fun (P:Type) (x3:((((inv R) X) Y)->((((inv R) Y) Z)->P)))=> (((((and_rect (((inv R) X) Y)) (((inv R) Y) Z)) P) x3) x2)) (((inv R) X) Z)) (fun (x3:(((inv R) X) Y)) (x4:(((inv R) Y) Z))=> (((fun (Y0:fofType)=> (((x1 Z) Y0) X)) Y) ((((conj ((R Z) Y)) ((R Y) X)) x4) x3)))))) as proof of (po (inv R)) % Found (((conj0 (trans (inv R))) ((((conj (refl (inv R))) (antisymm (inv R))) (((fun (P:Type) (x2:((refl R)->((antisymm R)->P)))=> (((((and_rect (refl R)) (antisymm R)) P) x2) x0)) (refl (inv R))) (fun (x2:(refl R)) (x3:(antisymm R))=> x2))) (fun (X:fofType) (Y:fofType) (x2:((and (((inv R) X) Y)) (((inv R) Y) X)))=> (((fun (P:Type) (x3:((refl R)->((antisymm R)->P)))=> (((((and_rect (refl R)) (antisymm R)) P) x3) x0)) (((eq fofType) X) Y)) (fun (x3:(refl R)) (x4:(antisymm R))=> ((((eq_sym fofType) Y) X) (((x4 Y) X) x2))))))) (fun (X:fofType) (Y:fofType) (Z:fofType) (x2:((and (((inv R) X) Y)) (((inv R) Y) Z)))=> (((fun (P:Type) (x3:((((inv R) X) Y)->((((inv R) Y) Z)->P)))=> (((((and_rect (((inv R) X) Y)) (((inv R) Y) Z)) P) x3) x2)) (((inv R) X) Z)) (fun (x3:(((inv R) X) Y)) (x4:(((inv R) Y) Z))=> (((fun (Y0:fofType)=> (((x1 Z) Y0) X)) Y) ((((conj ((R Z) Y)) ((R Y) X)) x4) x3)))))) as proof of (po (inv R)) % Found ((((conj ((and (refl (inv R))) (antisymm (inv R)))) (trans (inv R))) ((((conj (refl (inv R))) (antisymm (inv R))) (((fun (P:Type) (x2:((refl R)->((antisymm R)->P)))=> (((((and_rect (refl R)) (antisymm R)) P) x2) x0)) (refl (inv R))) (fun (x2:(refl R)) (x3:(antisymm R))=> x2))) (fun (X:fofType) (Y:fofType) (x2:((and (((inv R) X) Y)) (((inv R) Y) X)))=> (((fun (P:Type) (x3:((refl R)->((antisymm R)->P)))=> (((((and_rect (refl R)) (antisymm R)) P) x3) x0)) (((eq fofType) X) Y)) (fun (x3:(refl R)) (x4:(antisymm R))=> ((((eq_sym fofType) Y) X) (((x4 Y) X) x2))))))) (fun (X:fofType) (Y:fofType) (Z:fofType) (x2:((and (((inv R) X) Y)) (((inv R) Y) Z)))=> (((fun (P:Type) (x3:((((inv R) X) Y)->((((inv R) Y) Z)->P)))=> (((((and_rect (((inv R) X) Y)) (((inv R) Y) Z)) P) x3) x2)) (((inv R) X) Z)) (fun (x3:(((inv R) X) Y)) (x4:(((inv R) Y) Z))=> (((fun (Y0:fofType)=> (((x1 Z) Y0) X)) Y) ((((conj ((R Z) Y)) ((R Y) X)) x4) x3)))))) as proof of (po (inv R)) % Found (fun (x1:(trans R))=> ((((conj ((and (refl (inv R))) (antisymm (inv R)))) (trans (inv R))) ((((conj (refl (inv R))) (antisymm (inv R))) (((fun (P:Type) (x2:((refl R)->((antisymm R)->P)))=> (((((and_rect (refl R)) (antisymm R)) P) x2) x0)) (refl (inv R))) (fun (x2:(refl R)) (x3:(antisymm R))=> x2))) (fun (X:fofType) (Y:fofType) (x2:((and (((inv R) X) Y)) (((inv R) Y) X)))=> (((fun (P:Type) (x3:((refl R)->((antisymm R)->P)))=> (((((and_rect (refl R)) (antisymm R)) P) x3) x0)) (((eq fofType) X) Y)) (fun (x3:(refl R)) (x4:(antisymm R))=> ((((eq_sym fofType) Y) X) (((x4 Y) X) x2))))))) (fun (X:fofType) (Y:fofType) (Z:fofType) (x2:((and (((inv R) X) Y)) (((inv R) Y) Z)))=> (((fun (P:Type) (x3:((((inv R) X) Y)->((((inv R) Y) Z)->P)))=> (((((and_rect (((inv R) X) Y)) (((inv R) Y) Z)) P) x3) x2)) (((inv R) X) Z)) (fun (x3:(((inv R) X) Y)) (x4:(((inv R) Y) Z))=> (((fun (Y0:fofType)=> (((x1 Z) Y0) X)) Y) ((((conj ((R Z) Y)) ((R Y) X)) x4) x3))))))) as proof of (po (inv R)) % Found (fun (x0:((and (refl R)) (antisymm R))) (x1:(trans R))=> ((((conj ((and (refl (inv R))) (antisymm (inv R)))) (trans (inv R))) ((((conj (refl (inv R))) (antisymm (inv R))) (((fun (P:Type) (x2:((refl R)->((antisymm R)->P)))=> (((((and_rect (refl R)) (antisymm R)) P) x2) x0)) (refl (inv R))) (fun (x2:(refl R)) (x3:(antisymm R))=> x2))) (fun (X:fofType) (Y:fofType) (x2:((and (((inv R) X) Y)) (((inv R) Y) X)))=> (((fun (P:Type) (x3:((refl R)->((antisymm R)->P)))=> (((((and_rect (refl R)) (antisymm R)) P) x3) x0)) (((eq fofType) X) Y)) (fun (x3:(refl R)) (x4:(antisymm R))=> ((((eq_sym fofType) Y) X) (((x4 Y) X) x2))))))) (fun (X:fofType) (Y:fofType) (Z:fofType) (x2:((and (((inv R) X) Y)) (((inv R) Y) Z)))=> (((fun (P:Type) (x3:((((inv R) X) Y)->((((inv R) Y) Z)->P)))=> (((((and_rect (((inv R) X) Y)) (((inv R) Y) Z)) P) x3) x2)) (((inv R) X) Z)) (fun (x3:(((inv R) X) Y)) (x4:(((inv R) Y) Z))=> (((fun (Y0:fofType)=> (((x1 Z) Y0) X)) Y) ((((conj ((R Z) Y)) ((R Y) X)) x4) x3))))))) as proof of ((trans R)->(po (inv R))) % Found (fun (x0:((and (refl R)) (antisymm R))) (x1:(trans R))=> ((((conj ((and (refl (inv R))) (antisymm (inv R)))) (trans (inv R))) ((((conj (refl (inv R))) (antisymm (inv R))) (((fun (P:Type) (x2:((refl R)->((antisymm R)->P)))=> (((((and_rect (refl R)) (antisymm R)) P) x2) x0)) (refl (inv R))) (fun (x2:(refl R)) (x3:(antisymm R))=> x2))) (fun (X:fofType) (Y:fofType) (x2:((and (((inv R) X) Y)) (((inv R) Y) X)))=> (((fun (P:Type) (x3:((refl R)->((antisymm R)->P)))=> (((((and_rect (refl R)) (antisymm R)) P) x3) x0)) (((eq fofType) X) Y)) (fun (x3:(refl R)) (x4:(antisymm R))=> ((((eq_sym fofType) Y) X) (((x4 Y) X) x2))))))) (fun (X:fofType) (Y:fofType) (Z:fofType) (x2:((and (((inv R) X) Y)) (((inv R) Y) Z)))=> (((fun (P:Type) (x3:((((inv R) X) Y)->((((inv R) Y) Z)->P)))=> (((((and_rect (((inv R) X) Y)) (((inv R) Y) Z)) P) x3) x2)) (((inv R) X) Z)) (fun (x3:(((inv R) X) Y)) (x4:(((inv R) Y) Z))=> (((fun (Y0:fofType)=> (((x1 Z) Y0) X)) Y) ((((conj ((R Z) Y)) ((R Y) X)) x4) x3))))))) as proof of (((and (refl R)) (antisymm R))->((trans R)->(po (inv R)))) % Found (and_rect00 (fun (x0:((and (refl R)) (antisymm R))) (x1:(trans R))=> ((((conj ((and (refl (inv R))) (antisymm (inv R)))) (trans (inv R))) ((((conj (refl (inv R))) (antisymm (inv R))) (((fun (P:Type) (x2:((refl R)->((antisymm R)->P)))=> (((((and_rect (refl R)) (antisymm R)) P) x2) x0)) (refl (inv R))) (fun (x2:(refl R)) (x3:(antisymm R))=> x2))) (fun (X:fofType) (Y:fofType) (x2:((and (((inv R) X) Y)) (((inv R) Y) X)))=> (((fun (P:Type) (x3:((refl R)->((antisymm R)->P)))=> (((((and_rect (refl R)) (antisymm R)) P) x3) x0)) (((eq fofType) X) Y)) (fun (x3:(refl R)) (x4:(antisymm R))=> ((((eq_sym fofType) Y) X) (((x4 Y) X) x2))))))) (fun (X:fofType) (Y:fofType) (Z:fofType) (x2:((and (((inv R) X) Y)) (((inv R) Y) Z)))=> (((fun (P:Type) (x3:((((inv R) X) Y)->((((inv R) Y) Z)->P)))=> (((((and_rect (((inv R) X) Y)) (((inv R) Y) Z)) P) x3) x2)) (((inv R) X) Z)) (fun (x3:(((inv R) X) Y)) (x4:(((inv R) Y) Z))=> (((fun (Y0:fofType)=> (((x1 Z) Y0) X)) Y) ((((conj ((R Z) Y)) ((R Y) X)) x4) x3)))))))) as proof of (po (inv R)) % Found ((and_rect0 (po (inv R))) (fun (x0:((and (refl R)) (antisymm R))) (x1:(trans R))=> ((((conj ((and (refl (inv R))) (antisymm (inv R)))) (trans (inv R))) ((((conj (refl (inv R))) (antisymm (inv R))) (((fun (P:Type) (x2:((refl R)->((antisymm R)->P)))=> (((((and_rect (refl R)) (antisymm R)) P) x2) x0)) (refl (inv R))) (fun (x2:(refl R)) (x3:(antisymm R))=> x2))) (fun (X:fofType) (Y:fofType) (x2:((and (((inv R) X) Y)) (((inv R) Y) X)))=> (((fun (P:Type) (x3:((refl R)->((antisymm R)->P)))=> (((((and_rect (refl R)) (antisymm R)) P) x3) x0)) (((eq fofType) X) Y)) (fun (x3:(refl R)) (x4:(antisymm R))=> ((((eq_sym fofType) Y) X) (((x4 Y) X) x2))))))) (fun (X:fofType) (Y:fofType) (Z:fofType) (x2:((and (((inv R) X) Y)) (((inv R) Y) Z)))=> (((fun (P:Type) (x3:((((inv R) X) Y)->((((inv R) Y) Z)->P)))=> (((((and_rect (((inv R) X) Y)) (((inv R) Y) Z)) P) x3) x2)) (((inv R) X) Z)) (fun (x3:(((inv R) X) Y)) (x4:(((inv R) Y) Z))=> (((fun (Y0:fofType)=> (((x1 Z) Y0) X)) Y) ((((conj ((R Z) Y)) ((R Y) X)) x4) x3)))))))) as proof of (po (inv R)) % Found (((fun (P:Type) (x0:(((and (refl R)) (antisymm R))->((trans R)->P)))=> (((((and_rect ((and (refl R)) (antisymm R))) (trans R)) P) x0) x)) (po (inv R))) (fun (x0:((and (refl R)) (antisymm R))) (x1:(trans R))=> ((((conj ((and (refl (inv R))) (antisymm (inv R)))) (trans (inv R))) ((((conj (refl (inv R))) (antisymm (inv R))) (((fun (P:Type) (x2:((refl R)->((antisymm R)->P)))=> (((((and_rect (refl R)) (antisymm R)) P) x2) x0)) (refl (inv R))) (fun (x2:(refl R)) (x3:(antisymm R))=> x2))) (fun (X:fofType) (Y:fofType) (x2:((and (((inv R) X) Y)) (((inv R) Y) X)))=> (((fun (P:Type) (x3:((refl R)->((antisymm R)->P)))=> (((((and_rect (refl R)) (antisymm R)) P) x3) x0)) (((eq fofType) X) Y)) (fun (x3:(refl R)) (x4:(antisymm R))=> ((((eq_sym fofType) Y) X) (((x4 Y) X) x2))))))) (fun (X:fofType) (Y:fofType) (Z:fofType) (x2:((and (((inv R) X) Y)) (((inv R) Y) Z)))=> (((fun (P:Type) (x3:((((inv R) X) Y)->((((inv R) Y) Z)->P)))=> (((((and_rect (((inv R) X) Y)) (((inv R) Y) Z)) P) x3) x2)) (((inv R) X) Z)) (fun (x3:(((inv R) X) Y)) (x4:(((inv R) Y) Z))=> (((fun (Y0:fofType)=> (((x1 Z) Y0) X)) Y) ((((conj ((R Z) Y)) ((R Y) X)) x4) x3)))))))) as proof of (po (inv R)) % Found (fun (x:(po R))=> (((fun (P:Type) (x0:(((and (refl R)) (antisymm R))->((trans R)->P)))=> (((((and_rect ((and (refl R)) (antisymm R))) (trans R)) P) x0) x)) (po (inv R))) (fun (x0:((and (refl R)) (antisymm R))) (x1:(trans R))=> ((((conj ((and (refl (inv R))) (antisymm (inv R)))) (trans (inv R))) ((((conj (refl (inv R))) (antisymm (inv R))) (((fun (P:Type) (x2:((refl R)->((antisymm R)->P)))=> (((((and_rect (refl R)) (antisymm R)) P) x2) x0)) (refl (inv R))) (fun (x2:(refl R)) (x3:(antisymm R))=> x2))) (fun (X:fofType) (Y:fofType) (x2:((and (((inv R) X) Y)) (((inv R) Y) X)))=> (((fun (P:Type) (x3:((refl R)->((antisymm R)->P)))=> (((((and_rect (refl R)) (antisymm R)) P) x3) x0)) (((eq fofType) X) Y)) (fun (x3:(refl R)) (x4:(antisymm R))=> ((((eq_sym fofType) Y) X) (((x4 Y) X) x2))))))) (fun (X:fofType) (Y:fofType) (Z:fofType) (x2:((and (((inv R) X) Y)) (((inv R) Y) Z)))=> (((fun (P:Type) (x3:((((inv R) X) Y)->((((inv R) Y) Z)->P)))=> (((((and_rect (((inv R) X) Y)) (((inv R) Y) Z)) P) x3) x2)) (((inv R) X) Z)) (fun (x3:(((inv R) X) Y)) (x4:(((inv R) Y) Z))=> (((fun (Y0:fofType)=> (((x1 Z) Y0) X)) Y) ((((conj ((R Z) Y)) ((R Y) X)) x4) x3))))))))) as proof of (po (inv R)) % Found (fun (R:(fofType->(fofType->Prop))) (x:(po R))=> (((fun (P:Type) (x0:(((and (refl R)) (antisymm R))->((trans R)->P)))=> (((((and_rect ((and (refl R)) (antisymm R))) (trans R)) P) x0) x)) (po (inv R))) (fun (x0:((and (refl R)) (antisymm R))) (x1:(trans R))=> ((((conj ((and (refl (inv R))) (antisymm (inv R)))) (trans (inv R))) ((((conj (refl (inv R))) (antisymm (inv R))) (((fun (P:Type) (x2:((refl R)->((antisymm R)->P)))=> (((((and_rect (refl R)) (antisymm R)) P) x2) x0)) (refl (inv R))) (fun (x2:(refl R)) (x3:(antisymm R))=> x2))) (fun (X:fofType) (Y:fofType) (x2:((and (((inv R) X) Y)) (((inv R) Y) X)))=> (((fun (P:Type) (x3:((refl R)->((antisymm R)->P)))=> (((((and_rect (refl R)) (antisymm R)) P) x3) x0)) (((eq fofType) X) Y)) (fun (x3:(refl R)) (x4:(antisymm R))=> ((((eq_sym fofType) Y) X) (((x4 Y) X) x2))))))) (fun (X:fofType) (Y:fofType) (Z:fofType) (x2:((and (((inv R) X) Y)) (((inv R) Y) Z)))=> (((fun (P:Type) (x3:((((inv R) X) Y)->((((inv R) Y) Z)->P)))=> (((((and_rect (((inv R) X) Y)) (((inv R) Y) Z)) P) x3) x2)) (((inv R) X) Z)) (fun (x3:(((inv R) X) Y)) (x4:(((inv R) Y) Z))=> (((fun (Y0:fofType)=> (((x1 Z) Y0) X)) Y) ((((conj ((R Z) Y)) ((R Y) X)) x4) x3))))))))) as proof of ((po R)->(po (inv R))) % Found (fun (R:(fofType->(fofType->Prop))) (x:(po R))=> (((fun (P:Type) (x0:(((and (refl R)) (antisymm R))->((trans R)->P)))=> (((((and_rect ((and (refl R)) (antisymm R))) (trans R)) P) x0) x)) (po (inv R))) (fun (x0:((and (refl R)) (antisymm R))) (x1:(trans R))=> ((((conj ((and (refl (inv R))) (antisymm (inv R)))) (trans (inv R))) ((((conj (refl (inv R))) (antisymm (inv R))) (((fun (P:Type) (x2:((refl R)->((antisymm R)->P)))=> (((((and_rect (refl R)) (antisymm R)) P) x2) x0)) (refl (inv R))) (fun (x2:(refl R)) (x3:(antisymm R))=> x2))) (fun (X:fofType) (Y:fofType) (x2:((and (((inv R) X) Y)) (((inv R) Y) X)))=> (((fun (P:Type) (x3:((refl R)->((antisymm R)->P)))=> (((((and_rect (refl R)) (antisymm R)) P) x3) x0)) (((eq fofType) X) Y)) (fun (x3:(refl R)) (x4:(antisymm R))=> ((((eq_sym fofType) Y) X) (((x4 Y) X) x2))))))) (fun (X:fofType) (Y:fofType) (Z:fofType) (x2:((and (((inv R) X) Y)) (((inv R) Y) Z)))=> (((fun (P:Type) (x3:((((inv R) X) Y)->((((inv R) Y) Z)->P)))=> (((((and_rect (((inv R) X) Y)) (((inv R) Y) Z)) P) x3) x2)) (((inv R) X) Z)) (fun (x3:(((inv R) X) Y)) (x4:(((inv R) Y) Z))=> (((fun (Y0:fofType)=> (((x1 Z) Y0) X)) Y) ((((conj ((R Z) Y)) ((R Y) X)) x4) x3))))))))) as proof of (forall (R:(fofType->(fofType->Prop))), ((po R)->(po (inv R)))) % Got proof (fun (R:(fofType->(fofType->Prop))) (x:(po R))=> (((fun (P:Type) (x0:(((and (refl R)) (antisymm R))->((trans R)->P)))=> (((((and_rect ((and (refl R)) (antisymm R))) (trans R)) P) x0) x)) (po (inv R))) (fun (x0:((and (refl R)) (antisymm R))) (x1:(trans R))=> ((((conj ((and (refl (inv R))) (antisymm (inv R)))) (trans (inv R))) ((((conj (refl (inv R))) (antisymm (inv R))) (((fun (P:Type) (x2:((refl R)->((antisymm R)->P)))=> (((((and_rect (refl R)) (antisymm R)) P) x2) x0)) (refl (inv R))) (fun (x2:(refl R)) (x3:(antisymm R))=> x2))) (fun (X:fofType) (Y:fofType) (x2:((and (((inv R) X) Y)) (((inv R) Y) X)))=> (((fun (P:Type) (x3:((refl R)->((antisymm R)->P)))=> (((((and_rect (refl R)) (antisymm R)) P) x3) x0)) (((eq fofType) X) Y)) (fun (x3:(refl R)) (x4:(antisymm R))=> ((((eq_sym fofType) Y) X) (((x4 Y) X) x2))))))) (fun (X:fofType) (Y:fofType) (Z:fofType) (x2:((and (((inv R) X) Y)) (((inv R) Y) Z)))=> (((fun (P:Type) (x3:((((inv R) X) Y)->((((inv R) Y) Z)->P)))=> (((((and_rect (((inv R) X) Y)) (((inv R) Y) Z)) P) x3) x2)) (((inv R) X) Z)) (fun (x3:(((inv R) X) Y)) (x4:(((inv R) Y) Z))=> (((fun (Y0:fofType)=> (((x1 Z) Y0) X)) Y) ((((conj ((R Z) Y)) ((R Y) X)) x4) x3))))))))) % Time elapsed = 17.097581s % node=1756 cost=1096.000000 depth=33 % :::::::::::::::::::::: % % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p % (fun (R:(fofType->(fofType->Prop))) (x:(po R))=> (((fun (P:Type) (x0:(((and (refl R)) (antisymm R))->((trans R)->P)))=> (((((and_rect ((and (refl R)) (antisymm R))) (trans R)) P) x0) x)) (po (inv R))) (fun (x0:((and (refl R)) (antisymm R))) (x1:(trans R))=> ((((conj ((and (refl (inv R))) (antisymm (inv R)))) (trans (inv R))) ((((conj (refl (inv R))) (antisymm (inv R))) (((fun (P:Type) (x2:((refl R)->((antisymm R)->P)))=> (((((and_rect (refl R)) (antisymm R)) P) x2) x0)) (refl (inv R))) (fun (x2:(refl R)) (x3:(antisymm R))=> x2))) (fun (X:fofType) (Y:fofType) (x2:((and (((inv R) X) Y)) (((inv R) Y) X)))=> (((fun (P:Type) (x3:((refl R)->((antisymm R)->P)))=> (((((and_rect (refl R)) (antisymm R)) P) x3) x0)) (((eq fofType) X) Y)) (fun (x3:(refl R)) (x4:(antisymm R))=> ((((eq_sym fofType) Y) X) (((x4 Y) X) x2))))))) (fun (X:fofType) (Y:fofType) (Z:fofType) (x2:((and (((inv R) X) Y)) (((inv R) Y) Z)))=> (((fun (P:Type) (x3:((((inv R) X) Y)->((((inv R) Y) Z)->P)))=> (((((and_rect (((inv R) X) Y)) (((inv R) Y) Z)) P) x3) x2)) (((inv R) X) Z)) (fun (x3:(((inv R) X) Y)) (x4:(((inv R) Y) Z))=> (((fun (Y0:fofType)=> (((x1 Z) Y0) X)) Y) ((((conj ((R Z) Y)) ((R Y) X)) x4) x3))))))))) % % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p % EOF %------------------------------------------------------------------------------