%------------------------------------------------------------------------------ % File : cocATP---0.2.0 % Problem : SET076^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 : n106.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:30:08 EDT 2014 % Result : Theorem 8.41s % Output : Proof 8.41s % Verified : % SZS Type : None (Parsing solution fails) % Syntax : Number of formulae : 0 % Comments : %------------------------------------------------------------------------------ %----ERROR: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % % Problem : SET076^1 : TPTP v6.1.0. Released v3.6.0. % % Command : python CASC.py /export/starexec/sandbox/benchmark/theBenchmark.p % % Computer : n106.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 08:36:51 CDT 2014 % % CPUTime : 8.41 % 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/SET008^0.ax, trying next directory % FOF formula (<kernel.Constant object at 0x1e24f38>, <kernel.DependentProduct object at 0x1b02e60>) of role type named in_decl % Using role type % Declaring in:(fofType->((fofType->Prop)->Prop)) % FOF formula (((eq (fofType->((fofType->Prop)->Prop))) in) (fun (X:fofType) (M:(fofType->Prop))=> (M X))) of role definition named in % A new definition: (((eq (fofType->((fofType->Prop)->Prop))) in) (fun (X:fofType) (M:(fofType->Prop))=> (M X))) % Defined: in:=(fun (X:fofType) (M:(fofType->Prop))=> (M X)) % FOF formula (<kernel.Constant object at 0x1e053f8>, <kernel.DependentProduct object at 0x1c34cb0>) of role type named is_a_decl % Using role type % Declaring is_a:(fofType->((fofType->Prop)->Prop)) % FOF formula (((eq (fofType->((fofType->Prop)->Prop))) is_a) (fun (X:fofType) (M:(fofType->Prop))=> (M X))) of role definition named is_a % A new definition: (((eq (fofType->((fofType->Prop)->Prop))) is_a) (fun (X:fofType) (M:(fofType->Prop))=> (M X))) % Defined: is_a:=(fun (X:fofType) (M:(fofType->Prop))=> (M X)) % FOF formula (<kernel.Constant object at 0x1e24128>, <kernel.DependentProduct object at 0x1c34c20>) of role type named emptyset_decl % Using role type % Declaring emptyset:(fofType->Prop) % FOF formula (((eq (fofType->Prop)) emptyset) (fun (X:fofType)=> False)) of role definition named emptyset % A new definition: (((eq (fofType->Prop)) emptyset) (fun (X:fofType)=> False)) % Defined: emptyset:=(fun (X:fofType)=> False) % FOF formula (<kernel.Constant object at 0x1e24710>, <kernel.DependentProduct object at 0x1c34f80>) of role type named unord_pair_decl % Using role type % Declaring unord_pair:(fofType->(fofType->(fofType->Prop))) % FOF formula (((eq (fofType->(fofType->(fofType->Prop)))) unord_pair) (fun (X:fofType) (Y:fofType) (U:fofType)=> ((or (((eq fofType) U) X)) (((eq fofType) U) Y)))) of role definition named unord_pair % A new definition: (((eq (fofType->(fofType->(fofType->Prop)))) unord_pair) (fun (X:fofType) (Y:fofType) (U:fofType)=> ((or (((eq fofType) U) X)) (((eq fofType) U) Y)))) % Defined: unord_pair:=(fun (X:fofType) (Y:fofType) (U:fofType)=> ((or (((eq fofType) U) X)) (((eq fofType) U) Y))) % FOF formula (<kernel.Constant object at 0x1e24710>, <kernel.DependentProduct object at 0x1c34c20>) of role type named singleton_decl % Using role type % Declaring singleton:(fofType->(fofType->Prop)) % FOF formula (((eq (fofType->(fofType->Prop))) singleton) (fun (X:fofType) (U:fofType)=> (((eq fofType) U) X))) of role definition named singleton % A new definition: (((eq (fofType->(fofType->Prop))) singleton) (fun (X:fofType) (U:fofType)=> (((eq fofType) U) X))) % Defined: singleton:=(fun (X:fofType) (U:fofType)=> (((eq fofType) U) X)) % FOF formula (<kernel.Constant object at 0x1e24f38>, <kernel.DependentProduct object at 0x1c34cb0>) of role type named union_decl % Using role type % Declaring union:((fofType->Prop)->((fofType->Prop)->(fofType->Prop))) % FOF formula (((eq ((fofType->Prop)->((fofType->Prop)->(fofType->Prop)))) union) (fun (X:(fofType->Prop)) (Y:(fofType->Prop)) (U:fofType)=> ((or (X U)) (Y U)))) of role definition named union % A new definition: (((eq ((fofType->Prop)->((fofType->Prop)->(fofType->Prop)))) union) (fun (X:(fofType->Prop)) (Y:(fofType->Prop)) (U:fofType)=> ((or (X U)) (Y U)))) % Defined: union:=(fun (X:(fofType->Prop)) (Y:(fofType->Prop)) (U:fofType)=> ((or (X U)) (Y U))) % FOF formula (<kernel.Constant object at 0x1c34cb0>, <kernel.DependentProduct object at 0x1c34c20>) of role type named excl_union_decl % Using role type % Declaring excl_union:((fofType->Prop)->((fofType->Prop)->(fofType->Prop))) % FOF formula (((eq ((fofType->Prop)->((fofType->Prop)->(fofType->Prop)))) excl_union) (fun (X:(fofType->Prop)) (Y:(fofType->Prop)) (U:fofType)=> ((or ((and (X U)) ((Y U)->False))) ((and ((X U)->False)) (Y U))))) of role definition named excl_union % A new definition: (((eq ((fofType->Prop)->((fofType->Prop)->(fofType->Prop)))) excl_union) (fun (X:(fofType->Prop)) (Y:(fofType->Prop)) (U:fofType)=> ((or ((and (X U)) ((Y U)->False))) ((and ((X U)->False)) (Y U))))) % Defined: excl_union:=(fun (X:(fofType->Prop)) (Y:(fofType->Prop)) (U:fofType)=> ((or ((and (X U)) ((Y U)->False))) ((and ((X U)->False)) (Y U)))) % FOF formula (<kernel.Constant object at 0x1c34c20>, <kernel.DependentProduct object at 0x1c349e0>) of role type named intersection_decl % Using role type % Declaring intersection:((fofType->Prop)->((fofType->Prop)->(fofType->Prop))) % FOF formula (((eq ((fofType->Prop)->((fofType->Prop)->(fofType->Prop)))) intersection) (fun (X:(fofType->Prop)) (Y:(fofType->Prop)) (U:fofType)=> ((and (X U)) (Y U)))) of role definition named intersection % A new definition: (((eq ((fofType->Prop)->((fofType->Prop)->(fofType->Prop)))) intersection) (fun (X:(fofType->Prop)) (Y:(fofType->Prop)) (U:fofType)=> ((and (X U)) (Y U)))) % Defined: intersection:=(fun (X:(fofType->Prop)) (Y:(fofType->Prop)) (U:fofType)=> ((and (X U)) (Y U))) % FOF formula (<kernel.Constant object at 0x1c349e0>, <kernel.DependentProduct object at 0x1c34440>) of role type named setminus_decl % Using role type % Declaring setminus:((fofType->Prop)->((fofType->Prop)->(fofType->Prop))) % FOF formula (((eq ((fofType->Prop)->((fofType->Prop)->(fofType->Prop)))) setminus) (fun (X:(fofType->Prop)) (Y:(fofType->Prop)) (U:fofType)=> ((and (X U)) ((Y U)->False)))) of role definition named setminus % A new definition: (((eq ((fofType->Prop)->((fofType->Prop)->(fofType->Prop)))) setminus) (fun (X:(fofType->Prop)) (Y:(fofType->Prop)) (U:fofType)=> ((and (X U)) ((Y U)->False)))) % Defined: setminus:=(fun (X:(fofType->Prop)) (Y:(fofType->Prop)) (U:fofType)=> ((and (X U)) ((Y U)->False))) % FOF formula (<kernel.Constant object at 0x1c34440>, <kernel.DependentProduct object at 0x1c34d40>) of role type named complement_decl % Using role type % Declaring complement:((fofType->Prop)->(fofType->Prop)) % FOF formula (((eq ((fofType->Prop)->(fofType->Prop))) complement) (fun (X:(fofType->Prop)) (U:fofType)=> ((X U)->False))) of role definition named complement % A new definition: (((eq ((fofType->Prop)->(fofType->Prop))) complement) (fun (X:(fofType->Prop)) (U:fofType)=> ((X U)->False))) % Defined: complement:=(fun (X:(fofType->Prop)) (U:fofType)=> ((X U)->False)) % FOF formula (<kernel.Constant object at 0x1c34d40>, <kernel.DependentProduct object at 0x1c34f80>) of role type named disjoint_decl % Using role type % Declaring disjoint:((fofType->Prop)->((fofType->Prop)->Prop)) % FOF formula (((eq ((fofType->Prop)->((fofType->Prop)->Prop))) disjoint) (fun (X:(fofType->Prop)) (Y:(fofType->Prop))=> (((eq (fofType->Prop)) ((intersection X) Y)) emptyset))) of role definition named disjoint % A new definition: (((eq ((fofType->Prop)->((fofType->Prop)->Prop))) disjoint) (fun (X:(fofType->Prop)) (Y:(fofType->Prop))=> (((eq (fofType->Prop)) ((intersection X) Y)) emptyset))) % Defined: disjoint:=(fun (X:(fofType->Prop)) (Y:(fofType->Prop))=> (((eq (fofType->Prop)) ((intersection X) Y)) emptyset)) % FOF formula (<kernel.Constant object at 0x1e25248>, <kernel.DependentProduct object at 0x1c34dd0>) of role type named subset_decl % Using role type % Declaring subset:((fofType->Prop)->((fofType->Prop)->Prop)) % FOF formula (((eq ((fofType->Prop)->((fofType->Prop)->Prop))) subset) (fun (X:(fofType->Prop)) (Y:(fofType->Prop))=> (forall (U:fofType), ((X U)->(Y U))))) of role definition named subset % A new definition: (((eq ((fofType->Prop)->((fofType->Prop)->Prop))) subset) (fun (X:(fofType->Prop)) (Y:(fofType->Prop))=> (forall (U:fofType), ((X U)->(Y U))))) % Defined: subset:=(fun (X:(fofType->Prop)) (Y:(fofType->Prop))=> (forall (U:fofType), ((X U)->(Y U)))) % FOF formula (<kernel.Constant object at 0x1e25290>, <kernel.DependentProduct object at 0x1c346c8>) of role type named meets_decl % Using role type % Declaring meets:((fofType->Prop)->((fofType->Prop)->Prop)) % FOF formula (((eq ((fofType->Prop)->((fofType->Prop)->Prop))) meets) (fun (X:(fofType->Prop)) (Y:(fofType->Prop))=> ((ex fofType) (fun (U:fofType)=> ((and (X U)) (Y U)))))) of role definition named meets % A new definition: (((eq ((fofType->Prop)->((fofType->Prop)->Prop))) meets) (fun (X:(fofType->Prop)) (Y:(fofType->Prop))=> ((ex fofType) (fun (U:fofType)=> ((and (X U)) (Y U)))))) % Defined: meets:=(fun (X:(fofType->Prop)) (Y:(fofType->Prop))=> ((ex fofType) (fun (U:fofType)=> ((and (X U)) (Y U))))) % FOF formula (<kernel.Constant object at 0x1e25ab8>, <kernel.DependentProduct object at 0x1c34830>) of role type named misses_decl % Using role type % Declaring misses:((fofType->Prop)->((fofType->Prop)->Prop)) % FOF formula (((eq ((fofType->Prop)->((fofType->Prop)->Prop))) misses) (fun (X:(fofType->Prop)) (Y:(fofType->Prop))=> (((ex fofType) (fun (U:fofType)=> ((and (X U)) (Y U))))->False))) of role definition named misses % A new definition: (((eq ((fofType->Prop)->((fofType->Prop)->Prop))) misses) (fun (X:(fofType->Prop)) (Y:(fofType->Prop))=> (((ex fofType) (fun (U:fofType)=> ((and (X U)) (Y U))))->False))) % Defined: misses:=(fun (X:(fofType->Prop)) (Y:(fofType->Prop))=> (((ex fofType) (fun (U:fofType)=> ((and (X U)) (Y U))))->False)) % FOF formula (forall (X:fofType) (Y:fofType) (Z:(fofType->Prop)), (((and (Z X)) (Z Y))->((subset ((unord_pair X) Y)) Z))) of role conjecture named thm % Conjecture to prove = (forall (X:fofType) (Y:fofType) (Z:(fofType->Prop)), (((and (Z X)) (Z Y))->((subset ((unord_pair X) Y)) Z))):Prop % Parameter fofType_DUMMY:fofType. % We need to prove ['(forall (X:fofType) (Y:fofType) (Z:(fofType->Prop)), (((and (Z X)) (Z Y))->((subset ((unord_pair X) Y)) Z)))'] % Parameter fofType:Type. % Definition in:=(fun (X:fofType) (M:(fofType->Prop))=> (M X)):(fofType->((fofType->Prop)->Prop)). % Definition is_a:=(fun (X:fofType) (M:(fofType->Prop))=> (M X)):(fofType->((fofType->Prop)->Prop)). % Definition emptyset:=(fun (X:fofType)=> False):(fofType->Prop). % Definition unord_pair:=(fun (X:fofType) (Y:fofType) (U:fofType)=> ((or (((eq fofType) U) X)) (((eq fofType) U) Y))):(fofType->(fofType->(fofType->Prop))). % Definition singleton:=(fun (X:fofType) (U:fofType)=> (((eq fofType) U) X)):(fofType->(fofType->Prop)). % Definition union:=(fun (X:(fofType->Prop)) (Y:(fofType->Prop)) (U:fofType)=> ((or (X U)) (Y U))):((fofType->Prop)->((fofType->Prop)->(fofType->Prop))). % Definition excl_union:=(fun (X:(fofType->Prop)) (Y:(fofType->Prop)) (U:fofType)=> ((or ((and (X U)) ((Y U)->False))) ((and ((X U)->False)) (Y U)))):((fofType->Prop)->((fofType->Prop)->(fofType->Prop))). % Definition intersection:=(fun (X:(fofType->Prop)) (Y:(fofType->Prop)) (U:fofType)=> ((and (X U)) (Y U))):((fofType->Prop)->((fofType->Prop)->(fofType->Prop))). % Definition setminus:=(fun (X:(fofType->Prop)) (Y:(fofType->Prop)) (U:fofType)=> ((and (X U)) ((Y U)->False))):((fofType->Prop)->((fofType->Prop)->(fofType->Prop))). % Definition complement:=(fun (X:(fofType->Prop)) (U:fofType)=> ((X U)->False)):((fofType->Prop)->(fofType->Prop)). % Definition disjoint:=(fun (X:(fofType->Prop)) (Y:(fofType->Prop))=> (((eq (fofType->Prop)) ((intersection X) Y)) emptyset)):((fofType->Prop)->((fofType->Prop)->Prop)). % Definition subset:=(fun (X:(fofType->Prop)) (Y:(fofType->Prop))=> (forall (U:fofType), ((X U)->(Y U)))):((fofType->Prop)->((fofType->Prop)->Prop)). % Definition meets:=(fun (X:(fofType->Prop)) (Y:(fofType->Prop))=> ((ex fofType) (fun (U:fofType)=> ((and (X U)) (Y U))))):((fofType->Prop)->((fofType->Prop)->Prop)). % Definition misses:=(fun (X:(fofType->Prop)) (Y:(fofType->Prop))=> (((ex fofType) (fun (U:fofType)=> ((and (X U)) (Y U))))->False)):((fofType->Prop)->((fofType->Prop)->Prop)). % Trying to prove (forall (X:fofType) (Y:fofType) (Z:(fofType->Prop)), (((and (Z X)) (Z Y))->((subset ((unord_pair X) Y)) Z))) % Found eq_sym00000:=(eq_sym0000 Z):((Z Y)->(Z U)) % Found (eq_sym0000 Z) as proof of ((Z Y)->(Z U)) % Found ((eq_sym000 x1) Z) as proof of ((Z Y)->(Z U)) % Found (((eq_sym00 Y) x1) Z) as proof of ((Z Y)->(Z U)) % Found ((((eq_sym0 U) Y) x1) Z) as proof of ((Z Y)->(Z U)) % Found (((((eq_sym fofType) U) Y) x1) Z) as proof of ((Z Y)->(Z U)) % Found (fun (x2:(Z X))=> (((((eq_sym fofType) U) Y) x1) Z)) as proof of ((Z Y)->(Z U)) % Found (fun (x2:(Z X))=> (((((eq_sym fofType) U) Y) x1) Z)) as proof of ((Z X)->((Z Y)->(Z U))) % Found (and_rect00 (fun (x2:(Z X))=> (((((eq_sym fofType) U) Y) x1) Z))) as proof of (Z U) % Found ((and_rect0 (Z U)) (fun (x2:(Z X))=> (((((eq_sym fofType) U) Y) x1) Z))) as proof of (Z U) % Found (((fun (P:Type) (x2:((Z X)->((Z Y)->P)))=> (((((and_rect (Z X)) (Z Y)) P) x2) x)) (Z U)) (fun (x2:(Z X))=> (((((eq_sym fofType) U) Y) x1) Z))) as proof of (Z U) % Found (fun (x1:(((eq fofType) U) Y))=> (((fun (P:Type) (x2:((Z X)->((Z Y)->P)))=> (((((and_rect (Z X)) (Z Y)) P) x2) x)) (Z U)) (fun (x2:(Z X))=> (((((eq_sym fofType) U) Y) x1) Z)))) as proof of (Z U) % Found (fun (x1:(((eq fofType) U) Y))=> (((fun (P:Type) (x2:((Z X)->((Z Y)->P)))=> (((((and_rect (Z X)) (Z Y)) P) x2) x)) (Z U)) (fun (x2:(Z X))=> (((((eq_sym fofType) U) Y) x1) Z)))) as proof of ((((eq fofType) U) Y)->(Z U)) % Found x10:=(x1 (fun (x3:fofType)=> (Z Y))):((Z Y)->(Z Y)) % Found (x1 (fun (x3:fofType)=> (Z Y))) as proof of (P Y) % Found (x1 (fun (x3:fofType)=> (Z Y))) as proof of (P Y) % Found eq_ref000:=(eq_ref00 (fun (x2:fofType)=> ((is_a x2) Z))):(((is_a Y) Z)->((is_a Y) Z)) % Found (eq_ref00 (fun (x2:fofType)=> ((is_a x2) Z))) as proof of (P Y) % Found ((eq_ref0 Y) (fun (x2:fofType)=> ((is_a x2) Z))) as proof of (P Y) % Found (((eq_ref fofType) Y) (fun (x2:fofType)=> ((is_a x2) Z))) as proof of (P Y) % Found (((eq_ref fofType) Y) (fun (x2:fofType)=> ((is_a x2) Z))) as proof of (P Y) % Found x1:(((eq fofType) U) X) % Instantiate: b:=X:fofType % Found x1 as proof of (((eq fofType) U) b) % Found eq_substitution00000:=(eq_substitution0000 (fun (x4:fofType)=> x4)):((((eq fofType) U) Y)->(((eq fofType) U) Y)) % Found (eq_substitution0000 (fun (x4:fofType)=> x4)) as proof of ((((eq fofType) U) Y)->(((eq fofType) U) Y)) % Found ((eq_substitution000 Y) (fun (x4:fofType)=> x4)) as proof of ((((eq fofType) U) Y)->(((eq fofType) U) Y)) % Found (((eq_substitution00 U) Y) (fun (x4:fofType)=> x4)) as proof of ((((eq fofType) U) Y)->(((eq fofType) U) Y)) % Found ((((eq_substitution0 fofType) U) Y) (fun (x4:fofType)=> x4)) as proof of ((((eq fofType) U) Y)->(((eq fofType) U) Y)) % Found (((((eq_substitution fofType) fofType) U) Y) (fun (x4:fofType)=> x4)) as proof of ((((eq fofType) U) Y)->(((eq fofType) U) Y)) % Found (((((eq_substitution fofType) fofType) U) Y) (fun (x4:fofType)=> x4)) as proof of ((((eq fofType) U) Y)->(((eq fofType) U) Y)) % Found eq_substitution00000:=(eq_substitution0000 (fun (x4:fofType)=> x4)):((((eq fofType) U) Y)->(((eq fofType) U) Y)) % Found (eq_substitution0000 (fun (x4:fofType)=> x4)) as proof of ((((eq fofType) U) Y)->(((eq fofType) U) Y)) % Found ((eq_substitution000 Y) (fun (x4:fofType)=> x4)) as proof of ((((eq fofType) U) Y)->(((eq fofType) U) Y)) % Found (((eq_substitution00 U) Y) (fun (x4:fofType)=> x4)) as proof of ((((eq fofType) U) Y)->(((eq fofType) U) Y)) % Found ((((eq_substitution0 fofType) U) Y) (fun (x4:fofType)=> x4)) as proof of ((((eq fofType) U) Y)->(((eq fofType) U) Y)) % Found (((((eq_substitution fofType) fofType) U) Y) (fun (x4:fofType)=> x4)) as proof of ((((eq fofType) U) Y)->(((eq fofType) U) Y)) % Found (((((eq_substitution fofType) fofType) U) Y) (fun (x4:fofType)=> x4)) as proof of ((((eq fofType) U) Y)->(((eq fofType) U) Y)) % Found eq_sym00000:=(eq_sym0000 (fun (x3:fofType)=> ((is_a x3) Z))):(((is_a Y) Z)->((is_a U) Z)) % Found (eq_sym0000 (fun (x3:fofType)=> ((is_a x3) Z))) as proof of (((is_a Y) Z)->(Z U)) % Found ((eq_sym000 x1) (fun (x3:fofType)=> ((is_a x3) Z))) as proof of (((is_a Y) Z)->(Z U)) % Found (((eq_sym00 Y) x1) (fun (x3:fofType)=> ((is_a x3) Z))) as proof of (((is_a Y) Z)->(Z U)) % Found ((((eq_sym0 U) Y) x1) (fun (x3:fofType)=> ((is_a x3) Z))) as proof of (((is_a Y) Z)->(Z U)) % Found (((((eq_sym fofType) U) Y) x1) (fun (x3:fofType)=> ((is_a x3) Z))) as proof of (((is_a Y) Z)->(Z U)) % Found (fun (x2:(Z X))=> (((((eq_sym fofType) U) Y) x1) (fun (x3:fofType)=> ((is_a x3) Z)))) as proof of (((is_a Y) Z)->(Z U)) % Found (fun (x2:(Z X))=> (((((eq_sym fofType) U) Y) x1) (fun (x3:fofType)=> ((is_a x3) Z)))) as proof of ((Z X)->(((is_a Y) Z)->(Z U))) % Found (and_rect00 (fun (x2:(Z X))=> (((((eq_sym fofType) U) Y) x1) (fun (x3:fofType)=> ((is_a x3) Z))))) as proof of (Z U) % Found ((and_rect0 (Z U)) (fun (x2:(Z X))=> (((((eq_sym fofType) U) Y) x1) (fun (x3:fofType)=> ((is_a x3) Z))))) as proof of (Z U) % Found (((fun (P:Type) (x2:((Z X)->(((is_a Y) Z)->P)))=> (((((and_rect (Z X)) ((is_a Y) Z)) P) x2) x)) (Z U)) (fun (x2:(Z X))=> (((((eq_sym fofType) U) Y) x1) (fun (x3:fofType)=> ((is_a x3) Z))))) as proof of (Z U) % Found (fun (x1:(((eq fofType) U) Y))=> (((fun (P:Type) (x2:((Z X)->(((is_a Y) Z)->P)))=> (((((and_rect (Z X)) ((is_a Y) Z)) P) x2) x)) (Z U)) (fun (x2:(Z X))=> (((((eq_sym fofType) U) Y) x1) (fun (x3:fofType)=> ((is_a x3) Z)))))) as proof of (Z U) % Found (fun (x1:(((eq fofType) U) Y))=> (((fun (P:Type) (x2:((Z X)->(((is_a Y) Z)->P)))=> (((((and_rect (Z X)) ((is_a Y) Z)) P) x2) x)) (Z U)) (fun (x2:(Z X))=> (((((eq_sym fofType) U) Y) x1) (fun (x3:fofType)=> ((is_a x3) Z)))))) as proof of ((((eq fofType) U) Y)->(Z U)) % Found x10:=(x1 (fun (x3:fofType)=> ((is_a Y) Z))):(((is_a Y) Z)->((is_a Y) Z)) % Found (x1 (fun (x3:fofType)=> ((is_a Y) Z))) as proof of (P Y) % Found (x1 (fun (x3:fofType)=> ((is_a Y) Z))) as proof of (P Y) % Found x1:(((eq fofType) U) X) % Found x1 as proof of (((eq fofType) U) X) % Found x1:(((eq fofType) U) X) % Found x1 as proof of (((eq fofType) U) X) % Found x1:(((eq fofType) U) X) % Instantiate: b:=X:fofType % Found x1 as proof of (((eq fofType) U) b) % Found x3:(Z Y) % Instantiate: b:=Y:fofType % Found x3 as proof of (P b) % Found x2:(Z X) % Found x2 as proof of (P b) % Found ((eq_sym0000 x1) x2) as proof of (Z U) % Found ((eq_sym0000 x1) x2) as proof of (Z U) % Found (((fun (x4:(((eq fofType) U) b))=> ((eq_sym000 x4) Z)) x1) x2) as proof of (Z U) % Found (((fun (x4:(((eq fofType) U) X))=> (((eq_sym00 X) x4) Z)) x1) x2) as proof of (Z U) % Found (((fun (x4:(((eq fofType) U) X))=> ((((eq_sym0 U) X) x4) Z)) x1) x2) as proof of (Z U) % Found (((fun (x4:(((eq fofType) U) X))=> (((((eq_sym fofType) U) X) x4) Z)) x1) x2) as proof of (Z U) % Found (fun (x3:(Z Y))=> (((fun (x4:(((eq fofType) U) X))=> (((((eq_sym fofType) U) X) x4) Z)) x1) x2)) as proof of (Z U) % Found (fun (x2:(Z X)) (x3:(Z Y))=> (((fun (x4:(((eq fofType) U) X))=> (((((eq_sym fofType) U) X) x4) Z)) x1) x2)) as proof of ((Z Y)->(Z U)) % Found (fun (x2:(Z X)) (x3:(Z Y))=> (((fun (x4:(((eq fofType) U) X))=> (((((eq_sym fofType) U) X) x4) Z)) x1) x2)) as proof of ((Z X)->((Z Y)->(Z U))) % Found (and_rect00 (fun (x2:(Z X)) (x3:(Z Y))=> (((fun (x4:(((eq fofType) U) X))=> (((((eq_sym fofType) U) X) x4) Z)) x1) x2))) as proof of (Z U) % Found ((and_rect0 (Z U)) (fun (x2:(Z X)) (x3:(Z Y))=> (((fun (x4:(((eq fofType) U) X))=> (((((eq_sym fofType) U) X) x4) Z)) x1) x2))) as proof of (Z U) % Found (((fun (P:Type) (x2:((Z X)->((Z Y)->P)))=> (((((and_rect (Z X)) (Z Y)) P) x2) x)) (Z U)) (fun (x2:(Z X)) (x3:(Z Y))=> (((fun (x4:(((eq fofType) U) X))=> (((((eq_sym fofType) U) X) x4) Z)) x1) x2))) as proof of (Z U) % Found (fun (x1:(((eq fofType) U) X))=> (((fun (P:Type) (x2:((Z X)->((Z Y)->P)))=> (((((and_rect (Z X)) (Z Y)) P) x2) x)) (Z U)) (fun (x2:(Z X)) (x3:(Z Y))=> (((fun (x4:(((eq fofType) U) X))=> (((((eq_sym fofType) U) X) x4) Z)) x1) x2)))) as proof of (Z U) % Found (fun (x1:(((eq fofType) U) X))=> (((fun (P:Type) (x2:((Z X)->((Z Y)->P)))=> (((((and_rect (Z X)) (Z Y)) P) x2) x)) (Z U)) (fun (x2:(Z X)) (x3:(Z Y))=> (((fun (x4:(((eq fofType) U) X))=> (((((eq_sym fofType) U) X) x4) Z)) x1) x2)))) as proof of ((((eq fofType) U) X)->(Z U)) % Found ((or_ind00 (fun (x1:(((eq fofType) U) X))=> (((fun (P:Type) (x2:((Z X)->((Z Y)->P)))=> (((((and_rect (Z X)) (Z Y)) P) x2) x)) (Z U)) (fun (x2:(Z X)) (x3:(Z Y))=> (((fun (x4:(((eq fofType) U) X))=> (((((eq_sym fofType) U) X) x4) Z)) x1) x2))))) (fun (x1:(((eq fofType) U) Y))=> (((fun (P:Type) (x2:((Z X)->((Z Y)->P)))=> (((((and_rect (Z X)) (Z Y)) P) x2) x)) (Z U)) (fun (x2:(Z X))=> (((((eq_sym fofType) U) Y) x1) Z))))) as proof of (Z U) % Found (((or_ind0 (Z U)) (fun (x1:(((eq fofType) U) X))=> (((fun (P:Type) (x2:((Z X)->((Z Y)->P)))=> (((((and_rect (Z X)) (Z Y)) P) x2) x)) (Z U)) (fun (x2:(Z X)) (x3:(Z Y))=> (((fun (x4:(((eq fofType) U) X))=> (((((eq_sym fofType) U) X) x4) Z)) x1) x2))))) (fun (x1:(((eq fofType) U) Y))=> (((fun (P:Type) (x2:((Z X)->((Z Y)->P)))=> (((((and_rect (Z X)) (Z Y)) P) x2) x)) (Z U)) (fun (x2:(Z X))=> (((((eq_sym fofType) U) Y) x1) Z))))) as proof of (Z U) % Found ((((fun (P:Prop) (x1:((((eq fofType) U) X)->P)) (x2:((((eq fofType) U) Y)->P))=> ((((((or_ind (((eq fofType) U) X)) (((eq fofType) U) Y)) P) x1) x2) x0)) (Z U)) (fun (x1:(((eq fofType) U) X))=> (((fun (P:Type) (x2:((Z X)->((Z Y)->P)))=> (((((and_rect (Z X)) (Z Y)) P) x2) x)) (Z U)) (fun (x2:(Z X)) (x3:(Z Y))=> (((fun (x4:(((eq fofType) U) X))=> (((((eq_sym fofType) U) X) x4) Z)) x1) x2))))) (fun (x1:(((eq fofType) U) Y))=> (((fun (P:Type) (x2:((Z X)->((Z Y)->P)))=> (((((and_rect (Z X)) (Z Y)) P) x2) x)) (Z U)) (fun (x2:(Z X))=> (((((eq_sym fofType) U) Y) x1) Z))))) as proof of (Z U) % Found (fun (x0:(((unord_pair X) Y) U))=> ((((fun (P:Prop) (x1:((((eq fofType) U) X)->P)) (x2:((((eq fofType) U) Y)->P))=> ((((((or_ind (((eq fofType) U) X)) (((eq fofType) U) Y)) P) x1) x2) x0)) (Z U)) (fun (x1:(((eq fofType) U) X))=> (((fun (P:Type) (x2:((Z X)->((Z Y)->P)))=> (((((and_rect (Z X)) (Z Y)) P) x2) x)) (Z U)) (fun (x2:(Z X)) (x3:(Z Y))=> (((fun (x4:(((eq fofType) U) X))=> (((((eq_sym fofType) U) X) x4) Z)) x1) x2))))) (fun (x1:(((eq fofType) U) Y))=> (((fun (P:Type) (x2:((Z X)->((Z Y)->P)))=> (((((and_rect (Z X)) (Z Y)) P) x2) x)) (Z U)) (fun (x2:(Z X))=> (((((eq_sym fofType) U) Y) x1) Z)))))) as proof of (Z U) % Found (fun (U:fofType) (x0:(((unord_pair X) Y) U))=> ((((fun (P:Prop) (x1:((((eq fofType) U) X)->P)) (x2:((((eq fofType) U) Y)->P))=> ((((((or_ind (((eq fofType) U) X)) (((eq fofType) U) Y)) P) x1) x2) x0)) (Z U)) (fun (x1:(((eq fofType) U) X))=> (((fun (P:Type) (x2:((Z X)->((Z Y)->P)))=> (((((and_rect (Z X)) (Z Y)) P) x2) x)) (Z U)) (fun (x2:(Z X)) (x3:(Z Y))=> (((fun (x4:(((eq fofType) U) X))=> (((((eq_sym fofType) U) X) x4) Z)) x1) x2))))) (fun (x1:(((eq fofType) U) Y))=> (((fun (P:Type) (x2:((Z X)->((Z Y)->P)))=> (((((and_rect (Z X)) (Z Y)) P) x2) x)) (Z U)) (fun (x2:(Z X))=> (((((eq_sym fofType) U) Y) x1) Z)))))) as proof of ((((unord_pair X) Y) U)->(Z U)) % Found (fun (x:((and (Z X)) (Z Y))) (U:fofType) (x0:(((unord_pair X) Y) U))=> ((((fun (P:Prop) (x1:((((eq fofType) U) X)->P)) (x2:((((eq fofType) U) Y)->P))=> ((((((or_ind (((eq fofType) U) X)) (((eq fofType) U) Y)) P) x1) x2) x0)) (Z U)) (fun (x1:(((eq fofType) U) X))=> (((fun (P:Type) (x2:((Z X)->((Z Y)->P)))=> (((((and_rect (Z X)) (Z Y)) P) x2) x)) (Z U)) (fun (x2:(Z X)) (x3:(Z Y))=> (((fun (x4:(((eq fofType) U) X))=> (((((eq_sym fofType) U) X) x4) Z)) x1) x2))))) (fun (x1:(((eq fofType) U) Y))=> (((fun (P:Type) (x2:((Z X)->((Z Y)->P)))=> (((((and_rect (Z X)) (Z Y)) P) x2) x)) (Z U)) (fun (x2:(Z X))=> (((((eq_sym fofType) U) Y) x1) Z)))))) as proof of ((subset ((unord_pair X) Y)) Z) % Found (fun (Z:(fofType->Prop)) (x:((and (Z X)) (Z Y))) (U:fofType) (x0:(((unord_pair X) Y) U))=> ((((fun (P:Prop) (x1:((((eq fofType) U) X)->P)) (x2:((((eq fofType) U) Y)->P))=> ((((((or_ind (((eq fofType) U) X)) (((eq fofType) U) Y)) P) x1) x2) x0)) (Z U)) (fun (x1:(((eq fofType) U) X))=> (((fun (P:Type) (x2:((Z X)->((Z Y)->P)))=> (((((and_rect (Z X)) (Z Y)) P) x2) x)) (Z U)) (fun (x2:(Z X)) (x3:(Z Y))=> (((fun (x4:(((eq fofType) U) X))=> (((((eq_sym fofType) U) X) x4) Z)) x1) x2))))) (fun (x1:(((eq fofType) U) Y))=> (((fun (P:Type) (x2:((Z X)->((Z Y)->P)))=> (((((and_rect (Z X)) (Z Y)) P) x2) x)) (Z U)) (fun (x2:(Z X))=> (((((eq_sym fofType) U) Y) x1) Z)))))) as proof of (((and (Z X)) (Z Y))->((subset ((unord_pair X) Y)) Z)) % Found (fun (Y:fofType) (Z:(fofType->Prop)) (x:((and (Z X)) (Z Y))) (U:fofType) (x0:(((unord_pair X) Y) U))=> ((((fun (P:Prop) (x1:((((eq fofType) U) X)->P)) (x2:((((eq fofType) U) Y)->P))=> ((((((or_ind (((eq fofType) U) X)) (((eq fofType) U) Y)) P) x1) x2) x0)) (Z U)) (fun (x1:(((eq fofType) U) X))=> (((fun (P:Type) (x2:((Z X)->((Z Y)->P)))=> (((((and_rect (Z X)) (Z Y)) P) x2) x)) (Z U)) (fun (x2:(Z X)) (x3:(Z Y))=> (((fun (x4:(((eq fofType) U) X))=> (((((eq_sym fofType) U) X) x4) Z)) x1) x2))))) (fun (x1:(((eq fofType) U) Y))=> (((fun (P:Type) (x2:((Z X)->((Z Y)->P)))=> (((((and_rect (Z X)) (Z Y)) P) x2) x)) (Z U)) (fun (x2:(Z X))=> (((((eq_sym fofType) U) Y) x1) Z)))))) as proof of (forall (Z:(fofType->Prop)), (((and (Z X)) (Z Y))->((subset ((unord_pair X) Y)) Z))) % Found (fun (X:fofType) (Y:fofType) (Z:(fofType->Prop)) (x:((and (Z X)) (Z Y))) (U:fofType) (x0:(((unord_pair X) Y) U))=> ((((fun (P:Prop) (x1:((((eq fofType) U) X)->P)) (x2:((((eq fofType) U) Y)->P))=> ((((((or_ind (((eq fofType) U) X)) (((eq fofType) U) Y)) P) x1) x2) x0)) (Z U)) (fun (x1:(((eq fofType) U) X))=> (((fun (P:Type) (x2:((Z X)->((Z Y)->P)))=> (((((and_rect (Z X)) (Z Y)) P) x2) x)) (Z U)) (fun (x2:(Z X)) (x3:(Z Y))=> (((fun (x4:(((eq fofType) U) X))=> (((((eq_sym fofType) U) X) x4) Z)) x1) x2))))) (fun (x1:(((eq fofType) U) Y))=> (((fun (P:Type) (x2:((Z X)->((Z Y)->P)))=> (((((and_rect (Z X)) (Z Y)) P) x2) x)) (Z U)) (fun (x2:(Z X))=> (((((eq_sym fofType) U) Y) x1) Z)))))) as proof of (forall (Y:fofType) (Z:(fofType->Prop)), (((and (Z X)) (Z Y))->((subset ((unord_pair X) Y)) Z))) % Found (fun (X:fofType) (Y:fofType) (Z:(fofType->Prop)) (x:((and (Z X)) (Z Y))) (U:fofType) (x0:(((unord_pair X) Y) U))=> ((((fun (P:Prop) (x1:((((eq fofType) U) X)->P)) (x2:((((eq fofType) U) Y)->P))=> ((((((or_ind (((eq fofType) U) X)) (((eq fofType) U) Y)) P) x1) x2) x0)) (Z U)) (fun (x1:(((eq fofType) U) X))=> (((fun (P:Type) (x2:((Z X)->((Z Y)->P)))=> (((((and_rect (Z X)) (Z Y)) P) x2) x)) (Z U)) (fun (x2:(Z X)) (x3:(Z Y))=> (((fun (x4:(((eq fofType) U) X))=> (((((eq_sym fofType) U) X) x4) Z)) x1) x2))))) (fun (x1:(((eq fofType) U) Y))=> (((fun (P:Type) (x2:((Z X)->((Z Y)->P)))=> (((((and_rect (Z X)) (Z Y)) P) x2) x)) (Z U)) (fun (x2:(Z X))=> (((((eq_sym fofType) U) Y) x1) Z)))))) as proof of (forall (X:fofType) (Y:fofType) (Z:(fofType->Prop)), (((and (Z X)) (Z Y))->((subset ((unord_pair X) Y)) Z))) % Got proof (fun (X:fofType) (Y:fofType) (Z:(fofType->Prop)) (x:((and (Z X)) (Z Y))) (U:fofType) (x0:(((unord_pair X) Y) U))=> ((((fun (P:Prop) (x1:((((eq fofType) U) X)->P)) (x2:((((eq fofType) U) Y)->P))=> ((((((or_ind (((eq fofType) U) X)) (((eq fofType) U) Y)) P) x1) x2) x0)) (Z U)) (fun (x1:(((eq fofType) U) X))=> (((fun (P:Type) (x2:((Z X)->((Z Y)->P)))=> (((((and_rect (Z X)) (Z Y)) P) x2) x)) (Z U)) (fun (x2:(Z X)) (x3:(Z Y))=> (((fun (x4:(((eq fofType) U) X))=> (((((eq_sym fofType) U) X) x4) Z)) x1) x2))))) (fun (x1:(((eq fofType) U) Y))=> (((fun (P:Type) (x2:((Z X)->((Z Y)->P)))=> (((((and_rect (Z X)) (Z Y)) P) x2) x)) (Z U)) (fun (x2:(Z X))=> (((((eq_sym fofType) U) Y) x1) Z)))))) % Time elapsed = 7.973528s % node=1138 cost=1257.000000 depth=24 % :::::::::::::::::::::: % % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p % (fun (X:fofType) (Y:fofType) (Z:(fofType->Prop)) (x:((and (Z X)) (Z Y))) (U:fofType) (x0:(((unord_pair X) Y) U))=> ((((fun (P:Prop) (x1:((((eq fofType) U) X)->P)) (x2:((((eq fofType) U) Y)->P))=> ((((((or_ind (((eq fofType) U) X)) (((eq fofType) U) Y)) P) x1) x2) x0)) (Z U)) (fun (x1:(((eq fofType) U) X))=> (((fun (P:Type) (x2:((Z X)->((Z Y)->P)))=> (((((and_rect (Z X)) (Z Y)) P) x2) x)) (Z U)) (fun (x2:(Z X)) (x3:(Z Y))=> (((fun (x4:(((eq fofType) U) X))=> (((((eq_sym fofType) U) X) x4) Z)) x1) x2))))) (fun (x1:(((eq fofType) U) Y))=> (((fun (P:Type) (x2:((Z X)->((Z Y)->P)))=> (((((and_rect (Z X)) (Z Y)) P) x2) x)) (Z U)) (fun (x2:(Z X))=> (((((eq_sym fofType) U) Y) x1) Z)))))) % % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p % EOF %------------------------------------------------------------------------------