↑ Up

cocATP---0.2.0.THM-Prf.s

View TPTP
Problem Process solution in
SystemOnTSTP Download .tgz 
%------------------------------------------------------------------------------
% File     : cocATP---0.2.0
% Problem  : SEU690^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 : n101.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:49 EDT 2014

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

% Comments : 
%------------------------------------------------------------------------------
%----ERROR: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% % Problem  : SEU690^2 : TPTP v6.1.0. Released v3.7.0.
% % Command  : python CASC.py /export/starexec/sandbox/benchmark/theBenchmark.p
% % Computer : n101.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:12:26 CDT 2014
% % CPUTime  : 3.84 
% 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 0x28f0290>, <kernel.DependentProduct object at 0x28f08c0>) of role type named in_type
% Using role type
% Declaring in:(fofType->(fofType->Prop))
% FOF formula (<kernel.Constant object at 0x294da28>, <kernel.DependentProduct object at 0x28f08c0>) of role type named subset_type
% Using role type
% Declaring subset:(fofType->(fofType->Prop))
% FOF formula (<kernel.Constant object at 0x28f0560>, <kernel.Sort object at 0x23d8488>) of role type named setextsub_type
% Using role type
% Declaring setextsub:Prop
% FOF formula (((eq Prop) setextsub) (forall (A:fofType) (B:fofType), (((subset A) B)->(((subset B) A)->(((eq fofType) A) B))))) of role definition named setextsub
% A new definition: (((eq Prop) setextsub) (forall (A:fofType) (B:fofType), (((subset A) B)->(((subset B) A)->(((eq fofType) A) B)))))
% Defined: setextsub:=(forall (A:fofType) (B:fofType), (((subset A) B)->(((subset B) A)->(((eq fofType) A) B))))
% FOF formula (<kernel.Constant object at 0x28f0878>, <kernel.DependentProduct object at 0x28f0050>) of role type named kpair_type
% Using role type
% Declaring kpair:(fofType->(fofType->fofType))
% FOF formula (<kernel.Constant object at 0x28f0170>, <kernel.DependentProduct object at 0x294bab8>) of role type named cartprod_type
% Using role type
% Declaring cartprod:(fofType->(fofType->fofType))
% FOF formula (<kernel.Constant object at 0x28f0290>, <kernel.DependentProduct object at 0x28f0878>) of role type named breln_type
% Using role type
% Declaring breln:(fofType->(fofType->(fofType->Prop)))
% FOF formula (((eq (fofType->(fofType->(fofType->Prop)))) breln) (fun (A:fofType) (B:fofType) (C:fofType)=> ((subset C) ((cartprod A) B)))) of role definition named breln
% A new definition: (((eq (fofType->(fofType->(fofType->Prop)))) breln) (fun (A:fofType) (B:fofType) (C:fofType)=> ((subset C) ((cartprod A) B))))
% Defined: breln:=(fun (A:fofType) (B:fofType) (C:fofType)=> ((subset C) ((cartprod A) B)))
% FOF formula (<kernel.Constant object at 0x28f0170>, <kernel.Sort object at 0x23d8488>) of role type named subbreln_type
% Using role type
% Declaring subbreln:Prop
% FOF formula (((eq Prop) subbreln) (forall (A:fofType) (B:fofType) (R:fofType), ((((breln A) B) R)->(forall (S:fofType), ((((breln A) B) S)->((forall (Xx:fofType), (((in Xx) A)->(forall (Xy:fofType), (((in Xy) B)->(((in ((kpair Xx) Xy)) R)->((in ((kpair Xx) Xy)) S))))))->((subset R) S))))))) of role definition named subbreln
% A new definition: (((eq Prop) subbreln) (forall (A:fofType) (B:fofType) (R:fofType), ((((breln A) B) R)->(forall (S:fofType), ((((breln A) B) S)->((forall (Xx:fofType), (((in Xx) A)->(forall (Xy:fofType), (((in Xy) B)->(((in ((kpair Xx) Xy)) R)->((in ((kpair Xx) Xy)) S))))))->((subset R) S)))))))
% Defined: subbreln:=(forall (A:fofType) (B:fofType) (R:fofType), ((((breln A) B) R)->(forall (S:fofType), ((((breln A) B) S)->((forall (Xx:fofType), (((in Xx) A)->(forall (Xy:fofType), (((in Xy) B)->(((in ((kpair Xx) Xy)) R)->((in ((kpair Xx) Xy)) S))))))->((subset R) S))))))
% FOF formula (setextsub->(subbreln->(forall (A:fofType) (B:fofType) (R:fofType), ((((breln A) B) R)->(forall (S:fofType), ((((breln A) B) S)->((forall (Xx:fofType), (((in Xx) A)->(forall (Xy:fofType), (((in Xy) B)->(((in ((kpair Xx) Xy)) R)->((in ((kpair Xx) Xy)) S))))))->((forall (Xx:fofType), (((in Xx) A)->(forall (Xy:fofType), (((in Xy) B)->(((in ((kpair Xx) Xy)) S)->((in ((kpair Xx) Xy)) R))))))->(((eq fofType) R) S))))))))) of role conjecture named eqbreln
% Conjecture to prove = (setextsub->(subbreln->(forall (A:fofType) (B:fofType) (R:fofType), ((((breln A) B) R)->(forall (S:fofType), ((((breln A) B) S)->((forall (Xx:fofType), (((in Xx) A)->(forall (Xy:fofType), (((in Xy) B)->(((in ((kpair Xx) Xy)) R)->((in ((kpair Xx) Xy)) S))))))->((forall (Xx:fofType), (((in Xx) A)->(forall (Xy:fofType), (((in Xy) B)->(((in ((kpair Xx) Xy)) S)->((in ((kpair Xx) Xy)) R))))))->(((eq fofType) R) S))))))))):Prop
% Parameter fofType_DUMMY:fofType.
% We need to prove ['(setextsub->(subbreln->(forall (A:fofType) (B:fofType) (R:fofType), ((((breln A) B) R)->(forall (S:fofType), ((((breln A) B) S)->((forall (Xx:fofType), (((in Xx) A)->(forall (Xy:fofType), (((in Xy) B)->(((in ((kpair Xx) Xy)) R)->((in ((kpair Xx) Xy)) S))))))->((forall (Xx:fofType), (((in Xx) A)->(forall (Xy:fofType), (((in Xy) B)->(((in ((kpair Xx) Xy)) S)->((in ((kpair Xx) Xy)) R))))))->(((eq fofType) R) S)))))))))']
% Parameter fofType:Type.
% Parameter in:(fofType->(fofType->Prop)).
% Parameter subset:(fofType->(fofType->Prop)).
% Definition setextsub:=(forall (A:fofType) (B:fofType), (((subset A) B)->(((subset B) A)->(((eq fofType) A) B)))):Prop.
% Parameter kpair:(fofType->(fofType->fofType)).
% Parameter cartprod:(fofType->(fofType->fofType)).
% Definition breln:=(fun (A:fofType) (B:fofType) (C:fofType)=> ((subset C) ((cartprod A) B))):(fofType->(fofType->(fofType->Prop))).
% Definition subbreln:=(forall (A:fofType) (B:fofType) (R:fofType), ((((breln A) B) R)->(forall (S:fofType), ((((breln A) B) S)->((forall (Xx:fofType), (((in Xx) A)->(forall (Xy:fofType), (((in Xy) B)->(((in ((kpair Xx) Xy)) R)->((in ((kpair Xx) Xy)) S))))))->((subset R) S)))))):Prop.
% Trying to prove (setextsub->(subbreln->(forall (A:fofType) (B:fofType) (R:fofType), ((((breln A) B) R)->(forall (S:fofType), ((((breln A) B) S)->((forall (Xx:fofType), (((in Xx) A)->(forall (Xy:fofType), (((in Xy) B)->(((in ((kpair Xx) Xy)) R)->((in ((kpair Xx) Xy)) S))))))->((forall (Xx:fofType), (((in Xx) A)->(forall (Xy:fofType), (((in Xy) B)->(((in ((kpair Xx) Xy)) S)->((in ((kpair Xx) Xy)) R))))))->(((eq fofType) R) S)))))))))
% Found x60:(P R)
% Found (fun (x60:(P R))=> x60) as proof of (P R)
% Found (fun (x60:(P R))=> x60) as proof of (P0 R)
% Found x50:(P R)
% Found (fun (x50:(P R))=> x50) as proof of (P R)
% Found (fun (x50:(P R))=> x50) as proof of (P0 R)
% Found eq_ref00:=(eq_ref0 R):(((eq fofType) R) R)
% Found (eq_ref0 R) as proof of (((eq fofType) R) b)
% Found ((eq_ref fofType) R) as proof of (((eq fofType) R) b)
% Found ((eq_ref fofType) R) as proof of (((eq fofType) R) b)
% Found ((eq_ref fofType) R) as proof of (((eq fofType) R) b)
% Found eq_ref00:=(eq_ref0 b):(((eq fofType) b) b)
% Found (eq_ref0 b) as proof of (((eq fofType) b) S)
% Found ((eq_ref fofType) b) as proof of (((eq fofType) b) S)
% Found ((eq_ref fofType) b) as proof of (((eq fofType) b) S)
% Found ((eq_ref fofType) b) as proof of (((eq fofType) b) S)
% Found x60:(P S)
% Found (fun (x60:(P S))=> x60) as proof of (P S)
% Found (fun (x60:(P S))=> x60) as proof of (P0 S)
% Found eq_ref00:=(eq_ref0 b):(((eq fofType) b) b)
% Found (eq_ref0 b) as proof of (((eq fofType) b) R)
% Found ((eq_ref fofType) b) as proof of (((eq fofType) b) R)
% Found ((eq_ref fofType) b) as proof of (((eq fofType) b) R)
% Found ((eq_ref fofType) b) as proof of (((eq fofType) b) R)
% Found eq_ref00:=(eq_ref0 S):(((eq fofType) S) S)
% Found (eq_ref0 S) as proof of (((eq fofType) S) b)
% Found ((eq_ref fofType) S) as proof of (((eq fofType) S) b)
% Found ((eq_ref fofType) S) as proof of (((eq fofType) S) b)
% Found ((eq_ref fofType) S) as proof of (((eq fofType) S) b)
% Found x0000000:=(x000000 x3):((subset R) S)
% Found (x000000 x3) as proof of ((subset R) S)
% Found ((x00000 x2) x3) as proof of ((subset R) S)
% Found (((x0000 x1) x2) x3) as proof of ((subset R) S)
% Found (((((x000 A) B) x1) x2) x3) as proof of ((subset R) S)
% Found ((((((fun (A0:fofType) (B0:fofType) (x6:(((breln A0) B0) R))=> ((((x00 A0) B0) x6) S)) A) B) x1) x2) x3) as proof of ((subset R) S)
% Found ((((((fun (A0:fofType) (B0:fofType) (x6:(((breln A0) B0) R))=> (((((fun (A0:fofType) (B0:fofType)=> (((x0 A0) B0) R)) A0) B0) x6) S)) A) B) x1) x2) x3) as proof of ((subset R) S)
% Found ((((((fun (A0:fofType) (B0:fofType) (x6:(((breln A0) B0) R))=> (((((fun (A0:fofType) (B0:fofType)=> (((x0 A0) B0) R)) A0) B0) x6) S)) A) B) x1) x2) x3) as proof of ((subset R) S)
% Found x0000000:=(x000000 x4):((subset S) R)
% Found (x000000 x4) as proof of ((subset S) R)
% Found ((x00000 x1) x4) as proof of ((subset S) R)
% Found (((x0000 x2) x1) x4) as proof of ((subset S) R)
% Found (((((x000 A) B) x2) x1) x4) as proof of ((subset S) R)
% Found ((((((fun (A0:fofType) (B0:fofType) (x6:(((breln A0) B0) S))=> ((((x00 A0) B0) x6) R)) A) B) x2) x1) x4) as proof of ((subset S) R)
% Found ((((((fun (A0:fofType) (B0:fofType) (x6:(((breln A0) B0) S))=> (((((fun (A0:fofType) (B0:fofType)=> (((x0 A0) B0) S)) A0) B0) x6) R)) A) B) x2) x1) x4) as proof of ((subset S) R)
% Found ((((((fun (A0:fofType) (B0:fofType) (x6:(((breln A0) B0) S))=> (((((fun (A0:fofType) (B0:fofType)=> (((x0 A0) B0) S)) A0) B0) x6) R)) A) B) x2) x1) x4) as proof of ((subset S) R)
% Found ((x50 ((((((fun (A0:fofType) (B0:fofType) (x6:(((breln A0) B0) R))=> (((((fun (A0:fofType) (B0:fofType)=> (((x0 A0) B0) R)) A0) B0) x6) S)) A) B) x1) x2) x3)) ((((((fun (A0:fofType) (B0:fofType) (x6:(((breln A0) B0) S))=> (((((fun (A0:fofType) (B0:fofType)=> (((x0 A0) B0) S)) A0) B0) x6) R)) A) B) x2) x1) x4)) as proof of (((eq fofType) R) S)
% Found (((x5 S) ((((((fun (A0:fofType) (B0:fofType) (x6:(((breln A0) B0) R))=> (((((fun (A0:fofType) (B0:fofType)=> (((x0 A0) B0) R)) A0) B0) x6) S)) A) B) x1) x2) x3)) ((((((fun (A0:fofType) (B0:fofType) (x6:(((breln A0) B0) S))=> (((((fun (A0:fofType) (B0:fofType)=> (((x0 A0) B0) S)) A0) B0) x6) R)) A) B) x2) x1) x4)) as proof of (((eq fofType) R) S)
% Found ((((x R) S) ((((((fun (A0:fofType) (B0:fofType) (x6:(((breln A0) B0) R))=> (((((fun (A0:fofType) (B0:fofType)=> (((x0 A0) B0) R)) A0) B0) x6) S)) A) B) x1) x2) x3)) ((((((fun (A0:fofType) (B0:fofType) (x6:(((breln A0) B0) S))=> (((((fun (A0:fofType) (B0:fofType)=> (((x0 A0) B0) S)) A0) B0) x6) R)) A) B) x2) x1) x4)) as proof of (((eq fofType) R) S)
% Found (fun (x4:(forall (Xx:fofType), (((in Xx) A)->(forall (Xy:fofType), (((in Xy) B)->(((in ((kpair Xx) Xy)) S)->((in ((kpair Xx) Xy)) R)))))))=> ((((x R) S) ((((((fun (A0:fofType) (B0:fofType) (x6:(((breln A0) B0) R))=> (((((fun (A0:fofType) (B0:fofType)=> (((x0 A0) B0) R)) A0) B0) x6) S)) A) B) x1) x2) x3)) ((((((fun (A0:fofType) (B0:fofType) (x6:(((breln A0) B0) S))=> (((((fun (A0:fofType) (B0:fofType)=> (((x0 A0) B0) S)) A0) B0) x6) R)) A) B) x2) x1) x4))) as proof of (((eq fofType) R) S)
% Found (fun (x3:(forall (Xx:fofType), (((in Xx) A)->(forall (Xy:fofType), (((in Xy) B)->(((in ((kpair Xx) Xy)) R)->((in ((kpair Xx) Xy)) S))))))) (x4:(forall (Xx:fofType), (((in Xx) A)->(forall (Xy:fofType), (((in Xy) B)->(((in ((kpair Xx) Xy)) S)->((in ((kpair Xx) Xy)) R)))))))=> ((((x R) S) ((((((fun (A0:fofType) (B0:fofType) (x6:(((breln A0) B0) R))=> (((((fun (A0:fofType) (B0:fofType)=> (((x0 A0) B0) R)) A0) B0) x6) S)) A) B) x1) x2) x3)) ((((((fun (A0:fofType) (B0:fofType) (x6:(((breln A0) B0) S))=> (((((fun (A0:fofType) (B0:fofType)=> (((x0 A0) B0) S)) A0) B0) x6) R)) A) B) x2) x1) x4))) as proof of ((forall (Xx:fofType), (((in Xx) A)->(forall (Xy:fofType), (((in Xy) B)->(((in ((kpair Xx) Xy)) S)->((in ((kpair Xx) Xy)) R))))))->(((eq fofType) R) S))
% Found (fun (x2:(((breln A) B) S)) (x3:(forall (Xx:fofType), (((in Xx) A)->(forall (Xy:fofType), (((in Xy) B)->(((in ((kpair Xx) Xy)) R)->((in ((kpair Xx) Xy)) S))))))) (x4:(forall (Xx:fofType), (((in Xx) A)->(forall (Xy:fofType), (((in Xy) B)->(((in ((kpair Xx) Xy)) S)->((in ((kpair Xx) Xy)) R)))))))=> ((((x R) S) ((((((fun (A0:fofType) (B0:fofType) (x6:(((breln A0) B0) R))=> (((((fun (A0:fofType) (B0:fofType)=> (((x0 A0) B0) R)) A0) B0) x6) S)) A) B) x1) x2) x3)) ((((((fun (A0:fofType) (B0:fofType) (x6:(((breln A0) B0) S))=> (((((fun (A0:fofType) (B0:fofType)=> (((x0 A0) B0) S)) A0) B0) x6) R)) A) B) x2) x1) x4))) as proof of ((forall (Xx:fofType), (((in Xx) A)->(forall (Xy:fofType), (((in Xy) B)->(((in ((kpair Xx) Xy)) R)->((in ((kpair Xx) Xy)) S))))))->((forall (Xx:fofType), (((in Xx) A)->(forall (Xy:fofType), (((in Xy) B)->(((in ((kpair Xx) Xy)) S)->((in ((kpair Xx) Xy)) R))))))->(((eq fofType) R) S)))
% Found (fun (S:fofType) (x2:(((breln A) B) S)) (x3:(forall (Xx:fofType), (((in Xx) A)->(forall (Xy:fofType), (((in Xy) B)->(((in ((kpair Xx) Xy)) R)->((in ((kpair Xx) Xy)) S))))))) (x4:(forall (Xx:fofType), (((in Xx) A)->(forall (Xy:fofType), (((in Xy) B)->(((in ((kpair Xx) Xy)) S)->((in ((kpair Xx) Xy)) R)))))))=> ((((x R) S) ((((((fun (A0:fofType) (B0:fofType) (x6:(((breln A0) B0) R))=> (((((fun (A0:fofType) (B0:fofType)=> (((x0 A0) B0) R)) A0) B0) x6) S)) A) B) x1) x2) x3)) ((((((fun (A0:fofType) (B0:fofType) (x6:(((breln A0) B0) S))=> (((((fun (A0:fofType) (B0:fofType)=> (((x0 A0) B0) S)) A0) B0) x6) R)) A) B) x2) x1) x4))) as proof of ((((breln A) B) S)->((forall (Xx:fofType), (((in Xx) A)->(forall (Xy:fofType), (((in Xy) B)->(((in ((kpair Xx) Xy)) R)->((in ((kpair Xx) Xy)) S))))))->((forall (Xx:fofType), (((in Xx) A)->(forall (Xy:fofType), (((in Xy) B)->(((in ((kpair Xx) Xy)) S)->((in ((kpair Xx) Xy)) R))))))->(((eq fofType) R) S))))
% Found (fun (x1:(((breln A) B) R)) (S:fofType) (x2:(((breln A) B) S)) (x3:(forall (Xx:fofType), (((in Xx) A)->(forall (Xy:fofType), (((in Xy) B)->(((in ((kpair Xx) Xy)) R)->((in ((kpair Xx) Xy)) S))))))) (x4:(forall (Xx:fofType), (((in Xx) A)->(forall (Xy:fofType), (((in Xy) B)->(((in ((kpair Xx) Xy)) S)->((in ((kpair Xx) Xy)) R)))))))=> ((((x R) S) ((((((fun (A0:fofType) (B0:fofType) (x6:(((breln A0) B0) R))=> (((((fun (A0:fofType) (B0:fofType)=> (((x0 A0) B0) R)) A0) B0) x6) S)) A) B) x1) x2) x3)) ((((((fun (A0:fofType) (B0:fofType) (x6:(((breln A0) B0) S))=> (((((fun (A0:fofType) (B0:fofType)=> (((x0 A0) B0) S)) A0) B0) x6) R)) A) B) x2) x1) x4))) as proof of (forall (S:fofType), ((((breln A) B) S)->((forall (Xx:fofType), (((in Xx) A)->(forall (Xy:fofType), (((in Xy) B)->(((in ((kpair Xx) Xy)) R)->((in ((kpair Xx) Xy)) S))))))->((forall (Xx:fofType), (((in Xx) A)->(forall (Xy:fofType), (((in Xy) B)->(((in ((kpair Xx) Xy)) S)->((in ((kpair Xx) Xy)) R))))))->(((eq fofType) R) S)))))
% Found (fun (R:fofType) (x1:(((breln A) B) R)) (S:fofType) (x2:(((breln A) B) S)) (x3:(forall (Xx:fofType), (((in Xx) A)->(forall (Xy:fofType), (((in Xy) B)->(((in ((kpair Xx) Xy)) R)->((in ((kpair Xx) Xy)) S))))))) (x4:(forall (Xx:fofType), (((in Xx) A)->(forall (Xy:fofType), (((in Xy) B)->(((in ((kpair Xx) Xy)) S)->((in ((kpair Xx) Xy)) R)))))))=> ((((x R) S) ((((((fun (A0:fofType) (B0:fofType) (x6:(((breln A0) B0) R))=> (((((fun (A0:fofType) (B0:fofType)=> (((x0 A0) B0) R)) A0) B0) x6) S)) A) B) x1) x2) x3)) ((((((fun (A0:fofType) (B0:fofType) (x6:(((breln A0) B0) S))=> (((((fun (A0:fofType) (B0:fofType)=> (((x0 A0) B0) S)) A0) B0) x6) R)) A) B) x2) x1) x4))) as proof of ((((breln A) B) R)->(forall (S:fofType), ((((breln A) B) S)->((forall (Xx:fofType), (((in Xx) A)->(forall (Xy:fofType), (((in Xy) B)->(((in ((kpair Xx) Xy)) R)->((in ((kpair Xx) Xy)) S))))))->((forall (Xx:fofType), (((in Xx) A)->(forall (Xy:fofType), (((in Xy) B)->(((in ((kpair Xx) Xy)) S)->((in ((kpair Xx) Xy)) R))))))->(((eq fofType) R) S))))))
% Found (fun (B:fofType) (R:fofType) (x1:(((breln A) B) R)) (S:fofType) (x2:(((breln A) B) S)) (x3:(forall (Xx:fofType), (((in Xx) A)->(forall (Xy:fofType), (((in Xy) B)->(((in ((kpair Xx) Xy)) R)->((in ((kpair Xx) Xy)) S))))))) (x4:(forall (Xx:fofType), (((in Xx) A)->(forall (Xy:fofType), (((in Xy) B)->(((in ((kpair Xx) Xy)) S)->((in ((kpair Xx) Xy)) R)))))))=> ((((x R) S) ((((((fun (A0:fofType) (B0:fofType) (x6:(((breln A0) B0) R))=> (((((fun (A0:fofType) (B0:fofType)=> (((x0 A0) B0) R)) A0) B0) x6) S)) A) B) x1) x2) x3)) ((((((fun (A0:fofType) (B0:fofType) (x6:(((breln A0) B0) S))=> (((((fun (A0:fofType) (B0:fofType)=> (((x0 A0) B0) S)) A0) B0) x6) R)) A) B) x2) x1) x4))) as proof of (forall (R:fofType), ((((breln A) B) R)->(forall (S:fofType), ((((breln A) B) S)->((forall (Xx:fofType), (((in Xx) A)->(forall (Xy:fofType), (((in Xy) B)->(((in ((kpair Xx) Xy)) R)->((in ((kpair Xx) Xy)) S))))))->((forall (Xx:fofType), (((in Xx) A)->(forall (Xy:fofType), (((in Xy) B)->(((in ((kpair Xx) Xy)) S)->((in ((kpair Xx) Xy)) R))))))->(((eq fofType) R) S)))))))
% Found (fun (A:fofType) (B:fofType) (R:fofType) (x1:(((breln A) B) R)) (S:fofType) (x2:(((breln A) B) S)) (x3:(forall (Xx:fofType), (((in Xx) A)->(forall (Xy:fofType), (((in Xy) B)->(((in ((kpair Xx) Xy)) R)->((in ((kpair Xx) Xy)) S))))))) (x4:(forall (Xx:fofType), (((in Xx) A)->(forall (Xy:fofType), (((in Xy) B)->(((in ((kpair Xx) Xy)) S)->((in ((kpair Xx) Xy)) R)))))))=> ((((x R) S) ((((((fun (A0:fofType) (B0:fofType) (x6:(((breln A0) B0) R))=> (((((fun (A0:fofType) (B0:fofType)=> (((x0 A0) B0) R)) A0) B0) x6) S)) A) B) x1) x2) x3)) ((((((fun (A0:fofType) (B0:fofType) (x6:(((breln A0) B0) S))=> (((((fun (A0:fofType) (B0:fofType)=> (((x0 A0) B0) S)) A0) B0) x6) R)) A) B) x2) x1) x4))) as proof of (forall (B:fofType) (R:fofType), ((((breln A) B) R)->(forall (S:fofType), ((((breln A) B) S)->((forall (Xx:fofType), (((in Xx) A)->(forall (Xy:fofType), (((in Xy) B)->(((in ((kpair Xx) Xy)) R)->((in ((kpair Xx) Xy)) S))))))->((forall (Xx:fofType), (((in Xx) A)->(forall (Xy:fofType), (((in Xy) B)->(((in ((kpair Xx) Xy)) S)->((in ((kpair Xx) Xy)) R))))))->(((eq fofType) R) S)))))))
% Found (fun (x0:subbreln) (A:fofType) (B:fofType) (R:fofType) (x1:(((breln A) B) R)) (S:fofType) (x2:(((breln A) B) S)) (x3:(forall (Xx:fofType), (((in Xx) A)->(forall (Xy:fofType), (((in Xy) B)->(((in ((kpair Xx) Xy)) R)->((in ((kpair Xx) Xy)) S))))))) (x4:(forall (Xx:fofType), (((in Xx) A)->(forall (Xy:fofType), (((in Xy) B)->(((in ((kpair Xx) Xy)) S)->((in ((kpair Xx) Xy)) R)))))))=> ((((x R) S) ((((((fun (A0:fofType) (B0:fofType) (x6:(((breln A0) B0) R))=> (((((fun (A0:fofType) (B0:fofType)=> (((x0 A0) B0) R)) A0) B0) x6) S)) A) B) x1) x2) x3)) ((((((fun (A0:fofType) (B0:fofType) (x6:(((breln A0) B0) S))=> (((((fun (A0:fofType) (B0:fofType)=> (((x0 A0) B0) S)) A0) B0) x6) R)) A) B) x2) x1) x4))) as proof of (forall (A:fofType) (B:fofType) (R:fofType), ((((breln A) B) R)->(forall (S:fofType), ((((breln A) B) S)->((forall (Xx:fofType), (((in Xx) A)->(forall (Xy:fofType), (((in Xy) B)->(((in ((kpair Xx) Xy)) R)->((in ((kpair Xx) Xy)) S))))))->((forall (Xx:fofType), (((in Xx) A)->(forall (Xy:fofType), (((in Xy) B)->(((in ((kpair Xx) Xy)) S)->((in ((kpair Xx) Xy)) R))))))->(((eq fofType) R) S)))))))
% Found (fun (x:setextsub) (x0:subbreln) (A:fofType) (B:fofType) (R:fofType) (x1:(((breln A) B) R)) (S:fofType) (x2:(((breln A) B) S)) (x3:(forall (Xx:fofType), (((in Xx) A)->(forall (Xy:fofType), (((in Xy) B)->(((in ((kpair Xx) Xy)) R)->((in ((kpair Xx) Xy)) S))))))) (x4:(forall (Xx:fofType), (((in Xx) A)->(forall (Xy:fofType), (((in Xy) B)->(((in ((kpair Xx) Xy)) S)->((in ((kpair Xx) Xy)) R)))))))=> ((((x R) S) ((((((fun (A0:fofType) (B0:fofType) (x6:(((breln A0) B0) R))=> (((((fun (A0:fofType) (B0:fofType)=> (((x0 A0) B0) R)) A0) B0) x6) S)) A) B) x1) x2) x3)) ((((((fun (A0:fofType) (B0:fofType) (x6:(((breln A0) B0) S))=> (((((fun (A0:fofType) (B0:fofType)=> (((x0 A0) B0) S)) A0) B0) x6) R)) A) B) x2) x1) x4))) as proof of (subbreln->(forall (A:fofType) (B:fofType) (R:fofType), ((((breln A) B) R)->(forall (S:fofType), ((((breln A) B) S)->((forall (Xx:fofType), (((in Xx) A)->(forall (Xy:fofType), (((in Xy) B)->(((in ((kpair Xx) Xy)) R)->((in ((kpair Xx) Xy)) S))))))->((forall (Xx:fofType), (((in Xx) A)->(forall (Xy:fofType), (((in Xy) B)->(((in ((kpair Xx) Xy)) S)->((in ((kpair Xx) Xy)) R))))))->(((eq fofType) R) S))))))))
% Found (fun (x:setextsub) (x0:subbreln) (A:fofType) (B:fofType) (R:fofType) (x1:(((breln A) B) R)) (S:fofType) (x2:(((breln A) B) S)) (x3:(forall (Xx:fofType), (((in Xx) A)->(forall (Xy:fofType), (((in Xy) B)->(((in ((kpair Xx) Xy)) R)->((in ((kpair Xx) Xy)) S))))))) (x4:(forall (Xx:fofType), (((in Xx) A)->(forall (Xy:fofType), (((in Xy) B)->(((in ((kpair Xx) Xy)) S)->((in ((kpair Xx) Xy)) R)))))))=> ((((x R) S) ((((((fun (A0:fofType) (B0:fofType) (x6:(((breln A0) B0) R))=> (((((fun (A0:fofType) (B0:fofType)=> (((x0 A0) B0) R)) A0) B0) x6) S)) A) B) x1) x2) x3)) ((((((fun (A0:fofType) (B0:fofType) (x6:(((breln A0) B0) S))=> (((((fun (A0:fofType) (B0:fofType)=> (((x0 A0) B0) S)) A0) B0) x6) R)) A) B) x2) x1) x4))) as proof of (setextsub->(subbreln->(forall (A:fofType) (B:fofType) (R:fofType), ((((breln A) B) R)->(forall (S:fofType), ((((breln A) B) S)->((forall (Xx:fofType), (((in Xx) A)->(forall (Xy:fofType), (((in Xy) B)->(((in ((kpair Xx) Xy)) R)->((in ((kpair Xx) Xy)) S))))))->((forall (Xx:fofType), (((in Xx) A)->(forall (Xy:fofType), (((in Xy) B)->(((in ((kpair Xx) Xy)) S)->((in ((kpair Xx) Xy)) R))))))->(((eq fofType) R) S)))))))))
% Got proof (fun (x:setextsub) (x0:subbreln) (A:fofType) (B:fofType) (R:fofType) (x1:(((breln A) B) R)) (S:fofType) (x2:(((breln A) B) S)) (x3:(forall (Xx:fofType), (((in Xx) A)->(forall (Xy:fofType), (((in Xy) B)->(((in ((kpair Xx) Xy)) R)->((in ((kpair Xx) Xy)) S))))))) (x4:(forall (Xx:fofType), (((in Xx) A)->(forall (Xy:fofType), (((in Xy) B)->(((in ((kpair Xx) Xy)) S)->((in ((kpair Xx) Xy)) R)))))))=> ((((x R) S) ((((((fun (A0:fofType) (B0:fofType) (x6:(((breln A0) B0) R))=> (((((fun (A0:fofType) (B0:fofType)=> (((x0 A0) B0) R)) A0) B0) x6) S)) A) B) x1) x2) x3)) ((((((fun (A0:fofType) (B0:fofType) (x6:(((breln A0) B0) S))=> (((((fun (A0:fofType) (B0:fofType)=> (((x0 A0) B0) S)) A0) B0) x6) R)) A) B) x2) x1) x4)))
% Time elapsed = 3.481852s
% node=589 cost=685.000000 depth=20
% ::::::::::::::::::::::
% % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% (fun (x:setextsub) (x0:subbreln) (A:fofType) (B:fofType) (R:fofType) (x1:(((breln A) B) R)) (S:fofType) (x2:(((breln A) B) S)) (x3:(forall (Xx:fofType), (((in Xx) A)->(forall (Xy:fofType), (((in Xy) B)->(((in ((kpair Xx) Xy)) R)->((in ((kpair Xx) Xy)) S))))))) (x4:(forall (Xx:fofType), (((in Xx) A)->(forall (Xy:fofType), (((in Xy) B)->(((in ((kpair Xx) Xy)) S)->((in ((kpair Xx) Xy)) R)))))))=> ((((x R) S) ((((((fun (A0:fofType) (B0:fofType) (x6:(((breln A0) B0) R))=> (((((fun (A0:fofType) (B0:fofType)=> (((x0 A0) B0) R)) A0) B0) x6) S)) A) B) x1) x2) x3)) ((((((fun (A0:fofType) (B0:fofType) (x6:(((breln A0) B0) S))=> (((((fun (A0:fofType) (B0:fofType)=> (((x0 A0) B0) S)) A0) B0) x6) R)) A) B) x2) x1) x4)))
% % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% EOF
%------------------------------------------------------------------------------