%------------------------------------------------------------------------------ % File : cocATP---0.2.0 % Problem : SET014^4 : TPTP v6.1.0. Released v3.6.0. % Transfm : none % Format : tptp:raw % Command : python CASC.py /export/starexec/sandbox/benchmark/theBenchmark.p % Computer : n108.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:29:55 EDT 2014 % Result : Theorem 0.91s % Output : Proof 0.91s % Verified : % SZS Type : None (Parsing solution fails) % Syntax : Number of formulae : 0 % Comments : %------------------------------------------------------------------------------ %----ERROR: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % % Problem : SET014^4 : TPTP v6.1.0. Released v3.6.0. % % Command : python CASC.py /export/starexec/sandbox/benchmark/theBenchmark.p % % Computer : n108.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:38:26 CDT 2014 % % CPUTime : 0.91 % 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 0x1839368>, <kernel.DependentProduct object at 0x1839248>) 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 0x1839368>, <kernel.DependentProduct object at 0x1839e18>) 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 0x1839e18>, <kernel.DependentProduct object at 0x1839758>) 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 0x1839758>, <kernel.DependentProduct object at 0x1839560>) 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 0x1839560>, <kernel.DependentProduct object at 0x1839e60>) 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 0x1839e60>, <kernel.DependentProduct object at 0x18390e0>) 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 0x18390e0>, <kernel.DependentProduct object at 0x1839290>) 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 0x1818cb0>, <kernel.DependentProduct object at 0x18390e0>) 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 0x18390e0>, <kernel.DependentProduct object at 0x1839050>) 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 0x1839050>, <kernel.DependentProduct object at 0x1839128>) 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 0x1839128>, <kernel.DependentProduct object at 0x18397a0>) 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 0x151c050>, <kernel.DependentProduct object at 0x1839e60>) 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 0x151c488>, <kernel.DependentProduct object at 0x1839128>) 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 0x1839128>, <kernel.DependentProduct object at 0x1839368>) 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->Prop)) (Y:(fofType->Prop)) (A:(fofType->Prop)), (((and ((subset X) A)) ((subset Y) A))->((subset ((union X) Y)) A))) of role conjecture named thm % Conjecture to prove = (forall (X:(fofType->Prop)) (Y:(fofType->Prop)) (A:(fofType->Prop)), (((and ((subset X) A)) ((subset Y) A))->((subset ((union X) Y)) A))):Prop % Parameter fofType_DUMMY:fofType. % We need to prove ['(forall (X:(fofType->Prop)) (Y:(fofType->Prop)) (A:(fofType->Prop)), (((and ((subset X) A)) ((subset Y) A))->((subset ((union X) Y)) A)))'] % 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->Prop)) (Y:(fofType->Prop)) (A:(fofType->Prop)), (((and ((subset X) A)) ((subset Y) A))->((subset ((union X) Y)) A))) % Found x00:=(x0 U):((X U)->(A U)) % Found (x0 U) as proof of ((X U)->(A U)) % Found (x0 U) as proof of ((X U)->(A U)) % Found x10:=(x1 U):((Y U)->(A U)) % Found (x1 U) as proof of ((Y U)->(A U)) % Found (x1 U) as proof of ((Y U)->(A U)) % Found ((or_ind00 (x0 U)) (x1 U)) as proof of (A U) % Found (((or_ind0 (A U)) (x0 U)) (x1 U)) as proof of (A U) % Found ((((fun (P:Prop) (x3:((X U)->P)) (x4:((Y U)->P))=> ((((((or_ind (X U)) (Y U)) P) x3) x4) x2)) (A U)) (x0 U)) (x1 U)) as proof of (A U) % Found (fun (x2:(((union X) Y) U))=> ((((fun (P:Prop) (x3:((X U)->P)) (x4:((Y U)->P))=> ((((((or_ind (X U)) (Y U)) P) x3) x4) x2)) (A U)) (x0 U)) (x1 U))) as proof of (A U) % Found (fun (U:fofType) (x2:(((union X) Y) U))=> ((((fun (P:Prop) (x3:((X U)->P)) (x4:((Y U)->P))=> ((((((or_ind (X U)) (Y U)) P) x3) x4) x2)) (A U)) (x0 U)) (x1 U))) as proof of ((((union X) Y) U)->(A U)) % Found (fun (x1:((subset Y) A)) (U:fofType) (x2:(((union X) Y) U))=> ((((fun (P:Prop) (x3:((X U)->P)) (x4:((Y U)->P))=> ((((((or_ind (X U)) (Y U)) P) x3) x4) x2)) (A U)) (x0 U)) (x1 U))) as proof of ((subset ((union X) Y)) A) % Found (fun (x0:((subset X) A)) (x1:((subset Y) A)) (U:fofType) (x2:(((union X) Y) U))=> ((((fun (P:Prop) (x3:((X U)->P)) (x4:((Y U)->P))=> ((((((or_ind (X U)) (Y U)) P) x3) x4) x2)) (A U)) (x0 U)) (x1 U))) as proof of (((subset Y) A)->((subset ((union X) Y)) A)) % Found (fun (x0:((subset X) A)) (x1:((subset Y) A)) (U:fofType) (x2:(((union X) Y) U))=> ((((fun (P:Prop) (x3:((X U)->P)) (x4:((Y U)->P))=> ((((((or_ind (X U)) (Y U)) P) x3) x4) x2)) (A U)) (x0 U)) (x1 U))) as proof of (((subset X) A)->(((subset Y) A)->((subset ((union X) Y)) A))) % Found (and_rect00 (fun (x0:((subset X) A)) (x1:((subset Y) A)) (U:fofType) (x2:(((union X) Y) U))=> ((((fun (P:Prop) (x3:((X U)->P)) (x4:((Y U)->P))=> ((((((or_ind (X U)) (Y U)) P) x3) x4) x2)) (A U)) (x0 U)) (x1 U)))) as proof of ((subset ((union X) Y)) A) % Found ((and_rect0 ((subset ((union X) Y)) A)) (fun (x0:((subset X) A)) (x1:((subset Y) A)) (U:fofType) (x2:(((union X) Y) U))=> ((((fun (P:Prop) (x3:((X U)->P)) (x4:((Y U)->P))=> ((((((or_ind (X U)) (Y U)) P) x3) x4) x2)) (A U)) (x0 U)) (x1 U)))) as proof of ((subset ((union X) Y)) A) % Found (((fun (P:Type) (x0:(((subset X) A)->(((subset Y) A)->P)))=> (((((and_rect ((subset X) A)) ((subset Y) A)) P) x0) x)) ((subset ((union X) Y)) A)) (fun (x0:((subset X) A)) (x1:((subset Y) A)) (U:fofType) (x2:(((union X) Y) U))=> ((((fun (P:Prop) (x3:((X U)->P)) (x4:((Y U)->P))=> ((((((or_ind (X U)) (Y U)) P) x3) x4) x2)) (A U)) (x0 U)) (x1 U)))) as proof of ((subset ((union X) Y)) A) % Found (fun (x:((and ((subset X) A)) ((subset Y) A)))=> (((fun (P:Type) (x0:(((subset X) A)->(((subset Y) A)->P)))=> (((((and_rect ((subset X) A)) ((subset Y) A)) P) x0) x)) ((subset ((union X) Y)) A)) (fun (x0:((subset X) A)) (x1:((subset Y) A)) (U:fofType) (x2:(((union X) Y) U))=> ((((fun (P:Prop) (x3:((X U)->P)) (x4:((Y U)->P))=> ((((((or_ind (X U)) (Y U)) P) x3) x4) x2)) (A U)) (x0 U)) (x1 U))))) as proof of ((subset ((union X) Y)) A) % Found (fun (A:(fofType->Prop)) (x:((and ((subset X) A)) ((subset Y) A)))=> (((fun (P:Type) (x0:(((subset X) A)->(((subset Y) A)->P)))=> (((((and_rect ((subset X) A)) ((subset Y) A)) P) x0) x)) ((subset ((union X) Y)) A)) (fun (x0:((subset X) A)) (x1:((subset Y) A)) (U:fofType) (x2:(((union X) Y) U))=> ((((fun (P:Prop) (x3:((X U)->P)) (x4:((Y U)->P))=> ((((((or_ind (X U)) (Y U)) P) x3) x4) x2)) (A U)) (x0 U)) (x1 U))))) as proof of (((and ((subset X) A)) ((subset Y) A))->((subset ((union X) Y)) A)) % Found (fun (Y:(fofType->Prop)) (A:(fofType->Prop)) (x:((and ((subset X) A)) ((subset Y) A)))=> (((fun (P:Type) (x0:(((subset X) A)->(((subset Y) A)->P)))=> (((((and_rect ((subset X) A)) ((subset Y) A)) P) x0) x)) ((subset ((union X) Y)) A)) (fun (x0:((subset X) A)) (x1:((subset Y) A)) (U:fofType) (x2:(((union X) Y) U))=> ((((fun (P:Prop) (x3:((X U)->P)) (x4:((Y U)->P))=> ((((((or_ind (X U)) (Y U)) P) x3) x4) x2)) (A U)) (x0 U)) (x1 U))))) as proof of (forall (A:(fofType->Prop)), (((and ((subset X) A)) ((subset Y) A))->((subset ((union X) Y)) A))) % Found (fun (X:(fofType->Prop)) (Y:(fofType->Prop)) (A:(fofType->Prop)) (x:((and ((subset X) A)) ((subset Y) A)))=> (((fun (P:Type) (x0:(((subset X) A)->(((subset Y) A)->P)))=> (((((and_rect ((subset X) A)) ((subset Y) A)) P) x0) x)) ((subset ((union X) Y)) A)) (fun (x0:((subset X) A)) (x1:((subset Y) A)) (U:fofType) (x2:(((union X) Y) U))=> ((((fun (P:Prop) (x3:((X U)->P)) (x4:((Y U)->P))=> ((((((or_ind (X U)) (Y U)) P) x3) x4) x2)) (A U)) (x0 U)) (x1 U))))) as proof of (forall (Y:(fofType->Prop)) (A:(fofType->Prop)), (((and ((subset X) A)) ((subset Y) A))->((subset ((union X) Y)) A))) % Found (fun (X:(fofType->Prop)) (Y:(fofType->Prop)) (A:(fofType->Prop)) (x:((and ((subset X) A)) ((subset Y) A)))=> (((fun (P:Type) (x0:(((subset X) A)->(((subset Y) A)->P)))=> (((((and_rect ((subset X) A)) ((subset Y) A)) P) x0) x)) ((subset ((union X) Y)) A)) (fun (x0:((subset X) A)) (x1:((subset Y) A)) (U:fofType) (x2:(((union X) Y) U))=> ((((fun (P:Prop) (x3:((X U)->P)) (x4:((Y U)->P))=> ((((((or_ind (X U)) (Y U)) P) x3) x4) x2)) (A U)) (x0 U)) (x1 U))))) as proof of (forall (X:(fofType->Prop)) (Y:(fofType->Prop)) (A:(fofType->Prop)), (((and ((subset X) A)) ((subset Y) A))->((subset ((union X) Y)) A))) % Got proof (fun (X:(fofType->Prop)) (Y:(fofType->Prop)) (A:(fofType->Prop)) (x:((and ((subset X) A)) ((subset Y) A)))=> (((fun (P:Type) (x0:(((subset X) A)->(((subset Y) A)->P)))=> (((((and_rect ((subset X) A)) ((subset Y) A)) P) x0) x)) ((subset ((union X) Y)) A)) (fun (x0:((subset X) A)) (x1:((subset Y) A)) (U:fofType) (x2:(((union X) Y) U))=> ((((fun (P:Prop) (x3:((X U)->P)) (x4:((Y U)->P))=> ((((((or_ind (X U)) (Y U)) P) x3) x4) x2)) (A U)) (x0 U)) (x1 U))))) % Time elapsed = 0.538959s % node=66 cost=126.000000 depth=17 % :::::::::::::::::::::: % % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p % (fun (X:(fofType->Prop)) (Y:(fofType->Prop)) (A:(fofType->Prop)) (x:((and ((subset X) A)) ((subset Y) A)))=> (((fun (P:Type) (x0:(((subset X) A)->(((subset Y) A)->P)))=> (((((and_rect ((subset X) A)) ((subset Y) A)) P) x0) x)) ((subset ((union X) Y)) A)) (fun (x0:((subset X) A)) (x1:((subset Y) A)) (U:fofType) (x2:(((union X) Y) U))=> ((((fun (P:Prop) (x3:((X U)->P)) (x4:((Y U)->P))=> ((((((or_ind (X U)) (Y U)) P) x3) x4) x2)) (A U)) (x0 U)) (x1 U))))) % % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p % EOF %------------------------------------------------------------------------------