↑ Up

cocATP---0.2.0.THM-Prf.s

View TPTP
Problem Process solution in
SystemOnTSTP Download .tgz 
%------------------------------------------------------------------------------
% File     : cocATP---0.2.0
% Problem  : SEU644^2 : TPTP v6.1.0. Released v3.7.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : python CASC.py /export/starexec/sandbox/benchmark/theBenchmark.p

% Computer : n114.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:41 EDT 2014

% Result   : Theorem 14.42s
% Output   : Proof 14.42s
% Verified : 
% SZS Type : None (Parsing solution fails)
% Syntax   : Number of formulae    : 0

% Comments : 
%------------------------------------------------------------------------------
%----ERROR: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% % Problem  : SEU644^2 : TPTP v6.1.0. Released v3.7.0.
% % Command  : python CASC.py /export/starexec/sandbox/benchmark/theBenchmark.p
% % Computer : n114.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 11:00:56 CDT 2014
% % CPUTime  : 14.42 
% Python 2.7.5
% Using paths ['/home/cristobal/cocATP/CASC/TPTP/', '/export/starexec/sandbox/benchmark/', '/export/starexec/sandbox/benchmark/']
% FOF formula (<kernel.Constant object at 0x21407a0>, <kernel.DependentProduct object at 0x26b0248>) of role type named in_type
% Using role type
% Declaring in:(fofType->(fofType->Prop))
% FOF formula (<kernel.Constant object at 0x26a7440>, <kernel.Single object at 0x2140b48>) of role type named emptyset_type
% Using role type
% Declaring emptyset:fofType
% FOF formula (<kernel.Constant object at 0x26a7440>, <kernel.DependentProduct object at 0x26b0830>) of role type named setadjoin_type
% Using role type
% Declaring setadjoin:(fofType->(fofType->fofType))
% FOF formula (<kernel.Constant object at 0x2140b48>, <kernel.DependentProduct object at 0x213bf38>) of role type named setunion_type
% Using role type
% Declaring setunion:(fofType->fofType)
% FOF formula (<kernel.Constant object at 0x21407a0>, <kernel.Sort object at 0x213ec68>) of role type named eqinunit_type
% Using role type
% Declaring eqinunit:Prop
% FOF formula (((eq Prop) eqinunit) (forall (Xx:fofType) (Xy:fofType), ((((eq fofType) Xx) Xy)->((in Xx) ((setadjoin Xy) emptyset))))) of role definition named eqinunit
% A new definition: (((eq Prop) eqinunit) (forall (Xx:fofType) (Xy:fofType), ((((eq fofType) Xx) Xy)->((in Xx) ((setadjoin Xy) emptyset)))))
% Defined: eqinunit:=(forall (Xx:fofType) (Xy:fofType), ((((eq fofType) Xx) Xy)->((in Xx) ((setadjoin Xy) emptyset))))
% FOF formula (<kernel.Constant object at 0x2140b48>, <kernel.Sort object at 0x213ec68>) of role type named setunionsingleton_type
% Using role type
% Declaring setunionsingleton:Prop
% FOF formula (((eq Prop) setunionsingleton) (forall (Xx:fofType), (((eq fofType) (setunion ((setadjoin Xx) emptyset))) Xx))) of role definition named setunionsingleton
% A new definition: (((eq Prop) setunionsingleton) (forall (Xx:fofType), (((eq fofType) (setunion ((setadjoin Xx) emptyset))) Xx)))
% Defined: setunionsingleton:=(forall (Xx:fofType), (((eq fofType) (setunion ((setadjoin Xx) emptyset))) Xx))
% FOF formula (<kernel.Constant object at 0x26b05f0>, <kernel.DependentProduct object at 0x213bab8>) of role type named singleton_type
% Using role type
% Declaring singleton:(fofType->Prop)
% FOF formula (((eq (fofType->Prop)) singleton) (fun (A:fofType)=> ((ex fofType) (fun (Xx:fofType)=> ((and ((in Xx) A)) (((eq fofType) A) ((setadjoin Xx) emptyset))))))) of role definition named singleton
% A new definition: (((eq (fofType->Prop)) singleton) (fun (A:fofType)=> ((ex fofType) (fun (Xx:fofType)=> ((and ((in Xx) A)) (((eq fofType) A) ((setadjoin Xx) emptyset)))))))
% Defined: singleton:=(fun (A:fofType)=> ((ex fofType) (fun (Xx:fofType)=> ((and ((in Xx) A)) (((eq fofType) A) ((setadjoin Xx) emptyset))))))
% FOF formula (eqinunit->(setunionsingleton->(forall (X:fofType), ((singleton X)->((in (setunion X)) X))))) of role conjecture named theprop
% Conjecture to prove = (eqinunit->(setunionsingleton->(forall (X:fofType), ((singleton X)->((in (setunion X)) X))))):Prop
% We need to prove ['(eqinunit->(setunionsingleton->(forall (X:fofType), ((singleton X)->((in (setunion X)) X)))))']
% Parameter fofType:Type.
% Parameter in:(fofType->(fofType->Prop)).
% Parameter emptyset:fofType.
% Parameter setadjoin:(fofType->(fofType->fofType)).
% Parameter setunion:(fofType->fofType).
% Definition eqinunit:=(forall (Xx:fofType) (Xy:fofType), ((((eq fofType) Xx) Xy)->((in Xx) ((setadjoin Xy) emptyset)))):Prop.
% Definition setunionsingleton:=(forall (Xx:fofType), (((eq fofType) (setunion ((setadjoin Xx) emptyset))) Xx)):Prop.
% Definition singleton:=(fun (A:fofType)=> ((ex fofType) (fun (Xx:fofType)=> ((and ((in Xx) A)) (((eq fofType) A) ((setadjoin Xx) emptyset)))))):(fofType->Prop).
% Trying to prove (eqinunit->(setunionsingleton->(forall (X:fofType), ((singleton X)->((in (setunion X)) X)))))
% Found eq_ref00:=(eq_ref0 X):(((eq fofType) X) X)
% Found (eq_ref0 X) as proof of (((eq fofType) X) b)
% Found ((eq_ref fofType) X) as proof of (((eq fofType) X) b)
% Found ((eq_ref fofType) X) as proof of (((eq fofType) X) b)
% Found ((eq_ref fofType) X) as proof of (((eq fofType) X) b)
% Found x00:=(x0 X):(((eq fofType) (setunion ((setadjoin X) emptyset))) X)
% Instantiate: b:=X:fofType
% Found x00 as proof of (((eq fofType) (setunion ((setadjoin X) emptyset))) b)
% Found x00:=(x0 X):(((eq fofType) (setunion ((setadjoin X) emptyset))) X)
% Instantiate: b:=X:fofType
% Found x00 as proof of (((eq fofType) (setunion ((setadjoin X) emptyset))) b)
% Found x5:(((eq fofType) X) ((setadjoin x2) emptyset))
% Instantiate: b:=((setadjoin x2) emptyset):fofType
% Found x5 as proof of (((eq fofType) X) b)
% Found x00:=(x0 x2):(((eq fofType) (setunion ((setadjoin x2) emptyset))) x2)
% Found (x0 x2) as proof of (((eq fofType) (setunion b)) x2)
% Found (x0 x2) as proof of (((eq fofType) (setunion b)) x2)
% Found (x60 (x0 x2)) as proof of (P b)
% Found ((x6 x2) (x0 x2)) as proof of (P b)
% Found (((x (setunion b)) x2) (x0 x2)) as proof of (P b)
% Found (((x (setunion b)) x2) (x0 x2)) as proof of (P b)
% Found ((eq_sym0000 x5) (((x (setunion b)) x2) (x0 x2))) as proof of ((in (setunion X)) X)
% Found ((eq_sym0000 x5) (((x (setunion b)) x2) (x0 x2))) as proof of ((in (setunion X)) X)
% Found (((fun (x6:(((eq fofType) X) b))=> ((eq_sym000 x6) (fun (x8:fofType)=> ((in (setunion x8)) x8)))) x5) (((x (setunion b)) x2) (x0 x2))) as proof of ((in (setunion X)) X)
% Found (((fun (x6:(((eq fofType) X) ((setadjoin x2) emptyset)))=> (((eq_sym00 ((setadjoin x2) emptyset)) x6) (fun (x8:fofType)=> ((in (setunion x8)) x8)))) x5) (((x (setunion ((setadjoin x2) emptyset))) x2) (x0 x2))) as proof of ((in (setunion X)) X)
% Found (((fun (x6:(((eq fofType) X) ((setadjoin x2) emptyset)))=> ((((eq_sym0 X) ((setadjoin x2) emptyset)) x6) (fun (x8:fofType)=> ((in (setunion x8)) x8)))) x5) (((x (setunion ((setadjoin x2) emptyset))) x2) (x0 x2))) as proof of ((in (setunion X)) X)
% Found (((fun (x6:(((eq fofType) X) ((setadjoin x2) emptyset)))=> (((((eq_sym fofType) X) ((setadjoin x2) emptyset)) x6) (fun (x8:fofType)=> ((in (setunion x8)) x8)))) x5) (((x (setunion ((setadjoin x2) emptyset))) x2) (x0 x2))) as proof of ((in (setunion X)) X)
% Found (fun (x5:(((eq fofType) X) ((setadjoin x2) emptyset)))=> (((fun (x6:(((eq fofType) X) ((setadjoin x2) emptyset)))=> (((((eq_sym fofType) X) ((setadjoin x2) emptyset)) x6) (fun (x8:fofType)=> ((in (setunion x8)) x8)))) x5) (((x (setunion ((setadjoin x2) emptyset))) x2) (x0 x2)))) as proof of ((in (setunion X)) X)
% Found (fun (x4:((in x2) X)) (x5:(((eq fofType) X) ((setadjoin x2) emptyset)))=> (((fun (x6:(((eq fofType) X) ((setadjoin x2) emptyset)))=> (((((eq_sym fofType) X) ((setadjoin x2) emptyset)) x6) (fun (x8:fofType)=> ((in (setunion x8)) x8)))) x5) (((x (setunion ((setadjoin x2) emptyset))) x2) (x0 x2)))) as proof of ((((eq fofType) X) ((setadjoin x2) emptyset))->((in (setunion X)) X))
% Found (fun (x4:((in x2) X)) (x5:(((eq fofType) X) ((setadjoin x2) emptyset)))=> (((fun (x6:(((eq fofType) X) ((setadjoin x2) emptyset)))=> (((((eq_sym fofType) X) ((setadjoin x2) emptyset)) x6) (fun (x8:fofType)=> ((in (setunion x8)) x8)))) x5) (((x (setunion ((setadjoin x2) emptyset))) x2) (x0 x2)))) as proof of (((in x2) X)->((((eq fofType) X) ((setadjoin x2) emptyset))->((in (setunion X)) X)))
% Found (and_rect00 (fun (x4:((in x2) X)) (x5:(((eq fofType) X) ((setadjoin x2) emptyset)))=> (((fun (x6:(((eq fofType) X) ((setadjoin x2) emptyset)))=> (((((eq_sym fofType) X) ((setadjoin x2) emptyset)) x6) (fun (x8:fofType)=> ((in (setunion x8)) x8)))) x5) (((x (setunion ((setadjoin x2) emptyset))) x2) (x0 x2))))) as proof of ((in (setunion X)) X)
% Found ((and_rect0 ((in (setunion X)) X)) (fun (x4:((in x2) X)) (x5:(((eq fofType) X) ((setadjoin x2) emptyset)))=> (((fun (x6:(((eq fofType) X) ((setadjoin x2) emptyset)))=> (((((eq_sym fofType) X) ((setadjoin x2) emptyset)) x6) (fun (x8:fofType)=> ((in (setunion x8)) x8)))) x5) (((x (setunion ((setadjoin x2) emptyset))) x2) (x0 x2))))) as proof of ((in (setunion X)) X)
% Found (((fun (P:Type) (x4:(((in x2) X)->((((eq fofType) X) ((setadjoin x2) emptyset))->P)))=> (((((and_rect ((in x2) X)) (((eq fofType) X) ((setadjoin x2) emptyset))) P) x4) x3)) ((in (setunion X)) X)) (fun (x4:((in x2) X)) (x5:(((eq fofType) X) ((setadjoin x2) emptyset)))=> (((fun (x6:(((eq fofType) X) ((setadjoin x2) emptyset)))=> (((((eq_sym fofType) X) ((setadjoin x2) emptyset)) x6) (fun (x8:fofType)=> ((in (setunion x8)) x8)))) x5) (((x (setunion ((setadjoin x2) emptyset))) x2) (x0 x2))))) as proof of ((in (setunion X)) X)
% Found (fun (x3:((and ((in x2) X)) (((eq fofType) X) ((setadjoin x2) emptyset))))=> (((fun (P:Type) (x4:(((in x2) X)->((((eq fofType) X) ((setadjoin x2) emptyset))->P)))=> (((((and_rect ((in x2) X)) (((eq fofType) X) ((setadjoin x2) emptyset))) P) x4) x3)) ((in (setunion X)) X)) (fun (x4:((in x2) X)) (x5:(((eq fofType) X) ((setadjoin x2) emptyset)))=> (((fun (x6:(((eq fofType) X) ((setadjoin x2) emptyset)))=> (((((eq_sym fofType) X) ((setadjoin x2) emptyset)) x6) (fun (x8:fofType)=> ((in (setunion x8)) x8)))) x5) (((x (setunion ((setadjoin x2) emptyset))) x2) (x0 x2)))))) as proof of ((in (setunion X)) X)
% Found (fun (x2:fofType) (x3:((and ((in x2) X)) (((eq fofType) X) ((setadjoin x2) emptyset))))=> (((fun (P:Type) (x4:(((in x2) X)->((((eq fofType) X) ((setadjoin x2) emptyset))->P)))=> (((((and_rect ((in x2) X)) (((eq fofType) X) ((setadjoin x2) emptyset))) P) x4) x3)) ((in (setunion X)) X)) (fun (x4:((in x2) X)) (x5:(((eq fofType) X) ((setadjoin x2) emptyset)))=> (((fun (x6:(((eq fofType) X) ((setadjoin x2) emptyset)))=> (((((eq_sym fofType) X) ((setadjoin x2) emptyset)) x6) (fun (x8:fofType)=> ((in (setunion x8)) x8)))) x5) (((x (setunion ((setadjoin x2) emptyset))) x2) (x0 x2)))))) as proof of (((and ((in x2) X)) (((eq fofType) X) ((setadjoin x2) emptyset)))->((in (setunion X)) X))
% Found (fun (x2:fofType) (x3:((and ((in x2) X)) (((eq fofType) X) ((setadjoin x2) emptyset))))=> (((fun (P:Type) (x4:(((in x2) X)->((((eq fofType) X) ((setadjoin x2) emptyset))->P)))=> (((((and_rect ((in x2) X)) (((eq fofType) X) ((setadjoin x2) emptyset))) P) x4) x3)) ((in (setunion X)) X)) (fun (x4:((in x2) X)) (x5:(((eq fofType) X) ((setadjoin x2) emptyset)))=> (((fun (x6:(((eq fofType) X) ((setadjoin x2) emptyset)))=> (((((eq_sym fofType) X) ((setadjoin x2) emptyset)) x6) (fun (x8:fofType)=> ((in (setunion x8)) x8)))) x5) (((x (setunion ((setadjoin x2) emptyset))) x2) (x0 x2)))))) as proof of (forall (x:fofType), (((and ((in x) X)) (((eq fofType) X) ((setadjoin x) emptyset)))->((in (setunion X)) X)))
% Found (ex_ind00 (fun (x2:fofType) (x3:((and ((in x2) X)) (((eq fofType) X) ((setadjoin x2) emptyset))))=> (((fun (P:Type) (x4:(((in x2) X)->((((eq fofType) X) ((setadjoin x2) emptyset))->P)))=> (((((and_rect ((in x2) X)) (((eq fofType) X) ((setadjoin x2) emptyset))) P) x4) x3)) ((in (setunion X)) X)) (fun (x4:((in x2) X)) (x5:(((eq fofType) X) ((setadjoin x2) emptyset)))=> (((fun (x6:(((eq fofType) X) ((setadjoin x2) emptyset)))=> (((((eq_sym fofType) X) ((setadjoin x2) emptyset)) x6) (fun (x8:fofType)=> ((in (setunion x8)) x8)))) x5) (((x (setunion ((setadjoin x2) emptyset))) x2) (x0 x2))))))) as proof of ((in (setunion X)) X)
% Found ((ex_ind0 ((in (setunion X)) X)) (fun (x2:fofType) (x3:((and ((in x2) X)) (((eq fofType) X) ((setadjoin x2) emptyset))))=> (((fun (P:Type) (x4:(((in x2) X)->((((eq fofType) X) ((setadjoin x2) emptyset))->P)))=> (((((and_rect ((in x2) X)) (((eq fofType) X) ((setadjoin x2) emptyset))) P) x4) x3)) ((in (setunion X)) X)) (fun (x4:((in x2) X)) (x5:(((eq fofType) X) ((setadjoin x2) emptyset)))=> (((fun (x6:(((eq fofType) X) ((setadjoin x2) emptyset)))=> (((((eq_sym fofType) X) ((setadjoin x2) emptyset)) x6) (fun (x8:fofType)=> ((in (setunion x8)) x8)))) x5) (((x (setunion ((setadjoin x2) emptyset))) x2) (x0 x2))))))) as proof of ((in (setunion X)) X)
% Found (((fun (P:Prop) (x2:(forall (x:fofType), (((and ((in x) X)) (((eq fofType) X) ((setadjoin x) emptyset)))->P)))=> (((((ex_ind fofType) (fun (Xx:fofType)=> ((and ((in Xx) X)) (((eq fofType) X) ((setadjoin Xx) emptyset))))) P) x2) x1)) ((in (setunion X)) X)) (fun (x2:fofType) (x3:((and ((in x2) X)) (((eq fofType) X) ((setadjoin x2) emptyset))))=> (((fun (P:Type) (x4:(((in x2) X)->((((eq fofType) X) ((setadjoin x2) emptyset))->P)))=> (((((and_rect ((in x2) X)) (((eq fofType) X) ((setadjoin x2) emptyset))) P) x4) x3)) ((in (setunion X)) X)) (fun (x4:((in x2) X)) (x5:(((eq fofType) X) ((setadjoin x2) emptyset)))=> (((fun (x6:(((eq fofType) X) ((setadjoin x2) emptyset)))=> (((((eq_sym fofType) X) ((setadjoin x2) emptyset)) x6) (fun (x8:fofType)=> ((in (setunion x8)) x8)))) x5) (((x (setunion ((setadjoin x2) emptyset))) x2) (x0 x2))))))) as proof of ((in (setunion X)) X)
% Found (fun (x1:(singleton X))=> (((fun (P:Prop) (x2:(forall (x:fofType), (((and ((in x) X)) (((eq fofType) X) ((setadjoin x) emptyset)))->P)))=> (((((ex_ind fofType) (fun (Xx:fofType)=> ((and ((in Xx) X)) (((eq fofType) X) ((setadjoin Xx) emptyset))))) P) x2) x1)) ((in (setunion X)) X)) (fun (x2:fofType) (x3:((and ((in x2) X)) (((eq fofType) X) ((setadjoin x2) emptyset))))=> (((fun (P:Type) (x4:(((in x2) X)->((((eq fofType) X) ((setadjoin x2) emptyset))->P)))=> (((((and_rect ((in x2) X)) (((eq fofType) X) ((setadjoin x2) emptyset))) P) x4) x3)) ((in (setunion X)) X)) (fun (x4:((in x2) X)) (x5:(((eq fofType) X) ((setadjoin x2) emptyset)))=> (((fun (x6:(((eq fofType) X) ((setadjoin x2) emptyset)))=> (((((eq_sym fofType) X) ((setadjoin x2) emptyset)) x6) (fun (x8:fofType)=> ((in (setunion x8)) x8)))) x5) (((x (setunion ((setadjoin x2) emptyset))) x2) (x0 x2)))))))) as proof of ((in (setunion X)) X)
% Found (fun (X:fofType) (x1:(singleton X))=> (((fun (P:Prop) (x2:(forall (x:fofType), (((and ((in x) X)) (((eq fofType) X) ((setadjoin x) emptyset)))->P)))=> (((((ex_ind fofType) (fun (Xx:fofType)=> ((and ((in Xx) X)) (((eq fofType) X) ((setadjoin Xx) emptyset))))) P) x2) x1)) ((in (setunion X)) X)) (fun (x2:fofType) (x3:((and ((in x2) X)) (((eq fofType) X) ((setadjoin x2) emptyset))))=> (((fun (P:Type) (x4:(((in x2) X)->((((eq fofType) X) ((setadjoin x2) emptyset))->P)))=> (((((and_rect ((in x2) X)) (((eq fofType) X) ((setadjoin x2) emptyset))) P) x4) x3)) ((in (setunion X)) X)) (fun (x4:((in x2) X)) (x5:(((eq fofType) X) ((setadjoin x2) emptyset)))=> (((fun (x6:(((eq fofType) X) ((setadjoin x2) emptyset)))=> (((((eq_sym fofType) X) ((setadjoin x2) emptyset)) x6) (fun (x8:fofType)=> ((in (setunion x8)) x8)))) x5) (((x (setunion ((setadjoin x2) emptyset))) x2) (x0 x2)))))))) as proof of ((singleton X)->((in (setunion X)) X))
% Found (fun (x0:setunionsingleton) (X:fofType) (x1:(singleton X))=> (((fun (P:Prop) (x2:(forall (x:fofType), (((and ((in x) X)) (((eq fofType) X) ((setadjoin x) emptyset)))->P)))=> (((((ex_ind fofType) (fun (Xx:fofType)=> ((and ((in Xx) X)) (((eq fofType) X) ((setadjoin Xx) emptyset))))) P) x2) x1)) ((in (setunion X)) X)) (fun (x2:fofType) (x3:((and ((in x2) X)) (((eq fofType) X) ((setadjoin x2) emptyset))))=> (((fun (P:Type) (x4:(((in x2) X)->((((eq fofType) X) ((setadjoin x2) emptyset))->P)))=> (((((and_rect ((in x2) X)) (((eq fofType) X) ((setadjoin x2) emptyset))) P) x4) x3)) ((in (setunion X)) X)) (fun (x4:((in x2) X)) (x5:(((eq fofType) X) ((setadjoin x2) emptyset)))=> (((fun (x6:(((eq fofType) X) ((setadjoin x2) emptyset)))=> (((((eq_sym fofType) X) ((setadjoin x2) emptyset)) x6) (fun (x8:fofType)=> ((in (setunion x8)) x8)))) x5) (((x (setunion ((setadjoin x2) emptyset))) x2) (x0 x2)))))))) as proof of (forall (X:fofType), ((singleton X)->((in (setunion X)) X)))
% Found (fun (x:eqinunit) (x0:setunionsingleton) (X:fofType) (x1:(singleton X))=> (((fun (P:Prop) (x2:(forall (x:fofType), (((and ((in x) X)) (((eq fofType) X) ((setadjoin x) emptyset)))->P)))=> (((((ex_ind fofType) (fun (Xx:fofType)=> ((and ((in Xx) X)) (((eq fofType) X) ((setadjoin Xx) emptyset))))) P) x2) x1)) ((in (setunion X)) X)) (fun (x2:fofType) (x3:((and ((in x2) X)) (((eq fofType) X) ((setadjoin x2) emptyset))))=> (((fun (P:Type) (x4:(((in x2) X)->((((eq fofType) X) ((setadjoin x2) emptyset))->P)))=> (((((and_rect ((in x2) X)) (((eq fofType) X) ((setadjoin x2) emptyset))) P) x4) x3)) ((in (setunion X)) X)) (fun (x4:((in x2) X)) (x5:(((eq fofType) X) ((setadjoin x2) emptyset)))=> (((fun (x6:(((eq fofType) X) ((setadjoin x2) emptyset)))=> (((((eq_sym fofType) X) ((setadjoin x2) emptyset)) x6) (fun (x8:fofType)=> ((in (setunion x8)) x8)))) x5) (((x (setunion ((setadjoin x2) emptyset))) x2) (x0 x2)))))))) as proof of (setunionsingleton->(forall (X:fofType), ((singleton X)->((in (setunion X)) X))))
% Found (fun (x:eqinunit) (x0:setunionsingleton) (X:fofType) (x1:(singleton X))=> (((fun (P:Prop) (x2:(forall (x:fofType), (((and ((in x) X)) (((eq fofType) X) ((setadjoin x) emptyset)))->P)))=> (((((ex_ind fofType) (fun (Xx:fofType)=> ((and ((in Xx) X)) (((eq fofType) X) ((setadjoin Xx) emptyset))))) P) x2) x1)) ((in (setunion X)) X)) (fun (x2:fofType) (x3:((and ((in x2) X)) (((eq fofType) X) ((setadjoin x2) emptyset))))=> (((fun (P:Type) (x4:(((in x2) X)->((((eq fofType) X) ((setadjoin x2) emptyset))->P)))=> (((((and_rect ((in x2) X)) (((eq fofType) X) ((setadjoin x2) emptyset))) P) x4) x3)) ((in (setunion X)) X)) (fun (x4:((in x2) X)) (x5:(((eq fofType) X) ((setadjoin x2) emptyset)))=> (((fun (x6:(((eq fofType) X) ((setadjoin x2) emptyset)))=> (((((eq_sym fofType) X) ((setadjoin x2) emptyset)) x6) (fun (x8:fofType)=> ((in (setunion x8)) x8)))) x5) (((x (setunion ((setadjoin x2) emptyset))) x2) (x0 x2)))))))) as proof of (eqinunit->(setunionsingleton->(forall (X:fofType), ((singleton X)->((in (setunion X)) X)))))
% Got proof (fun (x:eqinunit) (x0:setunionsingleton) (X:fofType) (x1:(singleton X))=> (((fun (P:Prop) (x2:(forall (x:fofType), (((and ((in x) X)) (((eq fofType) X) ((setadjoin x) emptyset)))->P)))=> (((((ex_ind fofType) (fun (Xx:fofType)=> ((and ((in Xx) X)) (((eq fofType) X) ((setadjoin Xx) emptyset))))) P) x2) x1)) ((in (setunion X)) X)) (fun (x2:fofType) (x3:((and ((in x2) X)) (((eq fofType) X) ((setadjoin x2) emptyset))))=> (((fun (P:Type) (x4:(((in x2) X)->((((eq fofType) X) ((setadjoin x2) emptyset))->P)))=> (((((and_rect ((in x2) X)) (((eq fofType) X) ((setadjoin x2) emptyset))) P) x4) x3)) ((in (setunion X)) X)) (fun (x4:((in x2) X)) (x5:(((eq fofType) X) ((setadjoin x2) emptyset)))=> (((fun (x6:(((eq fofType) X) ((setadjoin x2) emptyset)))=> (((((eq_sym fofType) X) ((setadjoin x2) emptyset)) x6) (fun (x8:fofType)=> ((in (setunion x8)) x8)))) x5) (((x (setunion ((setadjoin x2) emptyset))) x2) (x0 x2))))))))
% Time elapsed = 13.983457s
% node=2989 cost=1239.000000 depth=28
% ::::::::::::::::::::::
% % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% (fun (x:eqinunit) (x0:setunionsingleton) (X:fofType) (x1:(singleton X))=> (((fun (P:Prop) (x2:(forall (x:fofType), (((and ((in x) X)) (((eq fofType) X) ((setadjoin x) emptyset)))->P)))=> (((((ex_ind fofType) (fun (Xx:fofType)=> ((and ((in Xx) X)) (((eq fofType) X) ((setadjoin Xx) emptyset))))) P) x2) x1)) ((in (setunion X)) X)) (fun (x2:fofType) (x3:((and ((in x2) X)) (((eq fofType) X) ((setadjoin x2) emptyset))))=> (((fun (P:Type) (x4:(((in x2) X)->((((eq fofType) X) ((setadjoin x2) emptyset))->P)))=> (((((and_rect ((in x2) X)) (((eq fofType) X) ((setadjoin x2) emptyset))) P) x4) x3)) ((in (setunion X)) X)) (fun (x4:((in x2) X)) (x5:(((eq fofType) X) ((setadjoin x2) emptyset)))=> (((fun (x6:(((eq fofType) X) ((setadjoin x2) emptyset)))=> (((((eq_sym fofType) X) ((setadjoin x2) emptyset)) x6) (fun (x8:fofType)=> ((in (setunion x8)) x8)))) x5) (((x (setunion ((setadjoin x2) emptyset))) x2) (x0 x2))))))))
% % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% EOF
%------------------------------------------------------------------------------