↑ Up

cocATP---0.2.0.THM-Prf.s

View TPTP
Problem Process solution in
SystemOnTSTP Download .tgz 
%------------------------------------------------------------------------------
% File     : cocATP---0.2.0
% Problem  : SET747^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 : n091.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:31:02 EDT 2014

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

% Comments : 
%------------------------------------------------------------------------------
%----ERROR: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% % Problem  : SET747^4 : TPTP v6.1.0. Released v3.6.0.
% % Command  : python CASC.py /export/starexec/sandbox/benchmark/theBenchmark.p
% % Computer : n091.star.cs.uiowa.edu
% % Model    : x86_64 x86_64
% % CPU      : Intel(R) Xeon(R) CPU E5-2609 0 @ 2.40GHz
% % Memory   : 32286.75MB
% % OS       : Linux 2.6.32-431.20.3.el6.x86_64
% % CPULimit : 300
% % DateTime : Thu Jul 17 10:48:31 CDT 2014
% % CPUTime  : 0.78 
% 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^1.ax, trying next directory
% FOF formula (<kernel.Constant object at 0x2959ef0>, <kernel.DependentProduct object at 0x2959c68>) of role type named fun_image_decl
% Using role type
% Declaring fun_image:((fofType->fofType)->((fofType->Prop)->(fofType->Prop)))
% FOF formula (((eq ((fofType->fofType)->((fofType->Prop)->(fofType->Prop)))) fun_image) (fun (F:(fofType->fofType)) (A:(fofType->Prop)) (Y:fofType)=> ((ex fofType) (fun (X:fofType)=> ((and (A X)) (((eq fofType) Y) (F X))))))) of role definition named fun_image
% A new definition: (((eq ((fofType->fofType)->((fofType->Prop)->(fofType->Prop)))) fun_image) (fun (F:(fofType->fofType)) (A:(fofType->Prop)) (Y:fofType)=> ((ex fofType) (fun (X:fofType)=> ((and (A X)) (((eq fofType) Y) (F X)))))))
% Defined: fun_image:=(fun (F:(fofType->fofType)) (A:(fofType->Prop)) (Y:fofType)=> ((ex fofType) (fun (X:fofType)=> ((and (A X)) (((eq fofType) Y) (F X))))))
% FOF formula (<kernel.Constant object at 0x23f3950>, <kernel.DependentProduct object at 0x2959f80>) of role type named fun_composition_decl
% Using role type
% Declaring fun_composition:((fofType->fofType)->((fofType->fofType)->(fofType->fofType)))
% FOF formula (((eq ((fofType->fofType)->((fofType->fofType)->(fofType->fofType)))) fun_composition) (fun (F:(fofType->fofType)) (G:(fofType->fofType)) (X:fofType)=> (G (F X)))) of role definition named fun_composition
% A new definition: (((eq ((fofType->fofType)->((fofType->fofType)->(fofType->fofType)))) fun_composition) (fun (F:(fofType->fofType)) (G:(fofType->fofType)) (X:fofType)=> (G (F X))))
% Defined: fun_composition:=(fun (F:(fofType->fofType)) (G:(fofType->fofType)) (X:fofType)=> (G (F X)))
% FOF formula (<kernel.Constant object at 0x28e2d40>, <kernel.DependentProduct object at 0x2959758>) of role type named fun_inv_image_decl
% Using role type
% Declaring fun_inv_image:((fofType->fofType)->((fofType->Prop)->(fofType->Prop)))
% FOF formula (((eq ((fofType->fofType)->((fofType->Prop)->(fofType->Prop)))) fun_inv_image) (fun (F:(fofType->fofType)) (B:(fofType->Prop)) (X:fofType)=> ((ex fofType) (fun (Y:fofType)=> ((and (B Y)) (((eq fofType) Y) (F X))))))) of role definition named fun_inv_image
% A new definition: (((eq ((fofType->fofType)->((fofType->Prop)->(fofType->Prop)))) fun_inv_image) (fun (F:(fofType->fofType)) (B:(fofType->Prop)) (X:fofType)=> ((ex fofType) (fun (Y:fofType)=> ((and (B Y)) (((eq fofType) Y) (F X)))))))
% Defined: fun_inv_image:=(fun (F:(fofType->fofType)) (B:(fofType->Prop)) (X:fofType)=> ((ex fofType) (fun (Y:fofType)=> ((and (B Y)) (((eq fofType) Y) (F X))))))
% FOF formula (<kernel.Constant object at 0x2959758>, <kernel.DependentProduct object at 0x2959710>) of role type named fun_injective_decl
% Using role type
% Declaring fun_injective:((fofType->fofType)->Prop)
% FOF formula (((eq ((fofType->fofType)->Prop)) fun_injective) (fun (F:(fofType->fofType))=> (forall (X:fofType) (Y:fofType), ((((eq fofType) (F X)) (F Y))->(((eq fofType) X) Y))))) of role definition named fun_injective
% A new definition: (((eq ((fofType->fofType)->Prop)) fun_injective) (fun (F:(fofType->fofType))=> (forall (X:fofType) (Y:fofType), ((((eq fofType) (F X)) (F Y))->(((eq fofType) X) Y)))))
% Defined: fun_injective:=(fun (F:(fofType->fofType))=> (forall (X:fofType) (Y:fofType), ((((eq fofType) (F X)) (F Y))->(((eq fofType) X) Y))))
% FOF formula (<kernel.Constant object at 0x2959fc8>, <kernel.DependentProduct object at 0x2959b00>) of role type named fun_surjective_decl
% Using role type
% Declaring fun_surjective:((fofType->fofType)->Prop)
% FOF formula (((eq ((fofType->fofType)->Prop)) fun_surjective) (fun (F:(fofType->fofType))=> (forall (Y:fofType), ((ex fofType) (fun (X:fofType)=> (((eq fofType) Y) (F X))))))) of role definition named fun_surjective
% A new definition: (((eq ((fofType->fofType)->Prop)) fun_surjective) (fun (F:(fofType->fofType))=> (forall (Y:fofType), ((ex fofType) (fun (X:fofType)=> (((eq fofType) Y) (F X)))))))
% Defined: fun_surjective:=(fun (F:(fofType->fofType))=> (forall (Y:fofType), ((ex fofType) (fun (X:fofType)=> (((eq fofType) Y) (F X))))))
% FOF formula (<kernel.Constant object at 0x2959d88>, <kernel.DependentProduct object at 0x2959758>) of role type named fun_bijective_decl
% Using role type
% Declaring fun_bijective:((fofType->fofType)->Prop)
% FOF formula (((eq ((fofType->fofType)->Prop)) fun_bijective) (fun (F:(fofType->fofType))=> ((and (fun_injective F)) (fun_surjective F)))) of role definition named fun_bijective
% A new definition: (((eq ((fofType->fofType)->Prop)) fun_bijective) (fun (F:(fofType->fofType))=> ((and (fun_injective F)) (fun_surjective F))))
% Defined: fun_bijective:=(fun (F:(fofType->fofType))=> ((and (fun_injective F)) (fun_surjective F)))
% FOF formula (<kernel.Constant object at 0x2959b00>, <kernel.DependentProduct object at 0x2903710>) of role type named fun_decreasing_decl
% Using role type
% Declaring fun_decreasing:((fofType->fofType)->((fofType->(fofType->Prop))->Prop))
% FOF formula (((eq ((fofType->fofType)->((fofType->(fofType->Prop))->Prop))) fun_decreasing) (fun (F:(fofType->fofType)) (SMALLER:(fofType->(fofType->Prop)))=> (forall (X:fofType) (Y:fofType), (((SMALLER X) Y)->((SMALLER (F Y)) (F X)))))) of role definition named fun_decreasing
% A new definition: (((eq ((fofType->fofType)->((fofType->(fofType->Prop))->Prop))) fun_decreasing) (fun (F:(fofType->fofType)) (SMALLER:(fofType->(fofType->Prop)))=> (forall (X:fofType) (Y:fofType), (((SMALLER X) Y)->((SMALLER (F Y)) (F X))))))
% Defined: fun_decreasing:=(fun (F:(fofType->fofType)) (SMALLER:(fofType->(fofType->Prop)))=> (forall (X:fofType) (Y:fofType), (((SMALLER X) Y)->((SMALLER (F Y)) (F X)))))
% FOF formula (<kernel.Constant object at 0x2959fc8>, <kernel.DependentProduct object at 0x29037e8>) of role type named fun_increasing_decl
% Using role type
% Declaring fun_increasing:((fofType->fofType)->((fofType->(fofType->Prop))->Prop))
% FOF formula (((eq ((fofType->fofType)->((fofType->(fofType->Prop))->Prop))) fun_increasing) (fun (F:(fofType->fofType)) (SMALLER:(fofType->(fofType->Prop)))=> (forall (X:fofType) (Y:fofType), (((SMALLER X) Y)->((SMALLER (F X)) (F Y)))))) of role definition named fun_increasing
% A new definition: (((eq ((fofType->fofType)->((fofType->(fofType->Prop))->Prop))) fun_increasing) (fun (F:(fofType->fofType)) (SMALLER:(fofType->(fofType->Prop)))=> (forall (X:fofType) (Y:fofType), (((SMALLER X) Y)->((SMALLER (F X)) (F Y))))))
% Defined: fun_increasing:=(fun (F:(fofType->fofType)) (SMALLER:(fofType->(fofType->Prop)))=> (forall (X:fofType) (Y:fofType), (((SMALLER X) Y)->((SMALLER (F X)) (F Y)))))
% FOF formula (forall (F:(fofType->fofType)) (G:(fofType->fofType)) (LESS:(fofType->(fofType->Prop))), (((and ((fun_increasing F) LESS)) ((fun_decreasing G) LESS))->((fun_decreasing ((fun_composition F) G)) LESS))) of role conjecture named thm
% Conjecture to prove = (forall (F:(fofType->fofType)) (G:(fofType->fofType)) (LESS:(fofType->(fofType->Prop))), (((and ((fun_increasing F) LESS)) ((fun_decreasing G) LESS))->((fun_decreasing ((fun_composition F) G)) LESS))):Prop
% Parameter fofType_DUMMY:fofType.
% We need to prove ['(forall (F:(fofType->fofType)) (G:(fofType->fofType)) (LESS:(fofType->(fofType->Prop))), (((and ((fun_increasing F) LESS)) ((fun_decreasing G) LESS))->((fun_decreasing ((fun_composition F) G)) LESS)))']
% Parameter fofType:Type.
% Definition fun_image:=(fun (F:(fofType->fofType)) (A:(fofType->Prop)) (Y:fofType)=> ((ex fofType) (fun (X:fofType)=> ((and (A X)) (((eq fofType) Y) (F X)))))):((fofType->fofType)->((fofType->Prop)->(fofType->Prop))).
% Definition fun_composition:=(fun (F:(fofType->fofType)) (G:(fofType->fofType)) (X:fofType)=> (G (F X))):((fofType->fofType)->((fofType->fofType)->(fofType->fofType))).
% Definition fun_inv_image:=(fun (F:(fofType->fofType)) (B:(fofType->Prop)) (X:fofType)=> ((ex fofType) (fun (Y:fofType)=> ((and (B Y)) (((eq fofType) Y) (F X)))))):((fofType->fofType)->((fofType->Prop)->(fofType->Prop))).
% Definition fun_injective:=(fun (F:(fofType->fofType))=> (forall (X:fofType) (Y:fofType), ((((eq fofType) (F X)) (F Y))->(((eq fofType) X) Y)))):((fofType->fofType)->Prop).
% Definition fun_surjective:=(fun (F:(fofType->fofType))=> (forall (Y:fofType), ((ex fofType) (fun (X:fofType)=> (((eq fofType) Y) (F X)))))):((fofType->fofType)->Prop).
% Definition fun_bijective:=(fun (F:(fofType->fofType))=> ((and (fun_injective F)) (fun_surjective F))):((fofType->fofType)->Prop).
% Definition fun_decreasing:=(fun (F:(fofType->fofType)) (SMALLER:(fofType->(fofType->Prop)))=> (forall (X:fofType) (Y:fofType), (((SMALLER X) Y)->((SMALLER (F Y)) (F X))))):((fofType->fofType)->((fofType->(fofType->Prop))->Prop)).
% Definition fun_increasing:=(fun (F:(fofType->fofType)) (SMALLER:(fofType->(fofType->Prop)))=> (forall (X:fofType) (Y:fofType), (((SMALLER X) Y)->((SMALLER (F X)) (F Y))))):((fofType->fofType)->((fofType->(fofType->Prop))->Prop)).
% Trying to prove (forall (F:(fofType->fofType)) (G:(fofType->fofType)) (LESS:(fofType->(fofType->Prop))), (((and ((fun_increasing F) LESS)) ((fun_decreasing G) LESS))->((fun_decreasing ((fun_composition F) G)) LESS)))
% Found x0000:=(x000 x2):((LESS (F X)) (F Y))
% Found (x000 x2) as proof of ((LESS (F X)) (F Y))
% Found ((x00 Y) x2) as proof of ((LESS (F X)) (F Y))
% Found (((x0 X) Y) x2) as proof of ((LESS (F X)) (F Y))
% Found (((x0 X) Y) x2) as proof of ((LESS (F X)) (F Y))
% Found (x100 (((x0 X) Y) x2)) as proof of ((LESS (((fun_composition F) G) Y)) (((fun_composition F) G) X))
% Found ((x10 (F Y)) (((x0 X) Y) x2)) as proof of ((LESS (((fun_composition F) G) Y)) (((fun_composition F) G) X))
% Found (((x1 (F X)) (F Y)) (((x0 X) Y) x2)) as proof of ((LESS (((fun_composition F) G) Y)) (((fun_composition F) G) X))
% Found (fun (x2:((LESS X) Y))=> (((x1 (F X)) (F Y)) (((x0 X) Y) x2))) as proof of ((LESS (((fun_composition F) G) Y)) (((fun_composition F) G) X))
% Found (fun (Y:fofType) (x2:((LESS X) Y))=> (((x1 (F X)) (F Y)) (((x0 X) Y) x2))) as proof of (((LESS X) Y)->((LESS (((fun_composition F) G) Y)) (((fun_composition F) G) X)))
% Found (fun (X:fofType) (Y:fofType) (x2:((LESS X) Y))=> (((x1 (F X)) (F Y)) (((x0 X) Y) x2))) as proof of (forall (Y:fofType), (((LESS X) Y)->((LESS (((fun_composition F) G) Y)) (((fun_composition F) G) X))))
% Found (fun (x1:((fun_decreasing G) LESS)) (X:fofType) (Y:fofType) (x2:((LESS X) Y))=> (((x1 (F X)) (F Y)) (((x0 X) Y) x2))) as proof of ((fun_decreasing ((fun_composition F) G)) LESS)
% Found (fun (x0:((fun_increasing F) LESS)) (x1:((fun_decreasing G) LESS)) (X:fofType) (Y:fofType) (x2:((LESS X) Y))=> (((x1 (F X)) (F Y)) (((x0 X) Y) x2))) as proof of (((fun_decreasing G) LESS)->((fun_decreasing ((fun_composition F) G)) LESS))
% Found (fun (x0:((fun_increasing F) LESS)) (x1:((fun_decreasing G) LESS)) (X:fofType) (Y:fofType) (x2:((LESS X) Y))=> (((x1 (F X)) (F Y)) (((x0 X) Y) x2))) as proof of (((fun_increasing F) LESS)->(((fun_decreasing G) LESS)->((fun_decreasing ((fun_composition F) G)) LESS)))
% Found (and_rect00 (fun (x0:((fun_increasing F) LESS)) (x1:((fun_decreasing G) LESS)) (X:fofType) (Y:fofType) (x2:((LESS X) Y))=> (((x1 (F X)) (F Y)) (((x0 X) Y) x2)))) as proof of ((fun_decreasing ((fun_composition F) G)) LESS)
% Found ((and_rect0 ((fun_decreasing ((fun_composition F) G)) LESS)) (fun (x0:((fun_increasing F) LESS)) (x1:((fun_decreasing G) LESS)) (X:fofType) (Y:fofType) (x2:((LESS X) Y))=> (((x1 (F X)) (F Y)) (((x0 X) Y) x2)))) as proof of ((fun_decreasing ((fun_composition F) G)) LESS)
% Found (((fun (P:Type) (x0:(((fun_increasing F) LESS)->(((fun_decreasing G) LESS)->P)))=> (((((and_rect ((fun_increasing F) LESS)) ((fun_decreasing G) LESS)) P) x0) x)) ((fun_decreasing ((fun_composition F) G)) LESS)) (fun (x0:((fun_increasing F) LESS)) (x1:((fun_decreasing G) LESS)) (X:fofType) (Y:fofType) (x2:((LESS X) Y))=> (((x1 (F X)) (F Y)) (((x0 X) Y) x2)))) as proof of ((fun_decreasing ((fun_composition F) G)) LESS)
% Found (fun (x:((and ((fun_increasing F) LESS)) ((fun_decreasing G) LESS)))=> (((fun (P:Type) (x0:(((fun_increasing F) LESS)->(((fun_decreasing G) LESS)->P)))=> (((((and_rect ((fun_increasing F) LESS)) ((fun_decreasing G) LESS)) P) x0) x)) ((fun_decreasing ((fun_composition F) G)) LESS)) (fun (x0:((fun_increasing F) LESS)) (x1:((fun_decreasing G) LESS)) (X:fofType) (Y:fofType) (x2:((LESS X) Y))=> (((x1 (F X)) (F Y)) (((x0 X) Y) x2))))) as proof of ((fun_decreasing ((fun_composition F) G)) LESS)
% Found (fun (LESS:(fofType->(fofType->Prop))) (x:((and ((fun_increasing F) LESS)) ((fun_decreasing G) LESS)))=> (((fun (P:Type) (x0:(((fun_increasing F) LESS)->(((fun_decreasing G) LESS)->P)))=> (((((and_rect ((fun_increasing F) LESS)) ((fun_decreasing G) LESS)) P) x0) x)) ((fun_decreasing ((fun_composition F) G)) LESS)) (fun (x0:((fun_increasing F) LESS)) (x1:((fun_decreasing G) LESS)) (X:fofType) (Y:fofType) (x2:((LESS X) Y))=> (((x1 (F X)) (F Y)) (((x0 X) Y) x2))))) as proof of (((and ((fun_increasing F) LESS)) ((fun_decreasing G) LESS))->((fun_decreasing ((fun_composition F) G)) LESS))
% Found (fun (G:(fofType->fofType)) (LESS:(fofType->(fofType->Prop))) (x:((and ((fun_increasing F) LESS)) ((fun_decreasing G) LESS)))=> (((fun (P:Type) (x0:(((fun_increasing F) LESS)->(((fun_decreasing G) LESS)->P)))=> (((((and_rect ((fun_increasing F) LESS)) ((fun_decreasing G) LESS)) P) x0) x)) ((fun_decreasing ((fun_composition F) G)) LESS)) (fun (x0:((fun_increasing F) LESS)) (x1:((fun_decreasing G) LESS)) (X:fofType) (Y:fofType) (x2:((LESS X) Y))=> (((x1 (F X)) (F Y)) (((x0 X) Y) x2))))) as proof of (forall (LESS:(fofType->(fofType->Prop))), (((and ((fun_increasing F) LESS)) ((fun_decreasing G) LESS))->((fun_decreasing ((fun_composition F) G)) LESS)))
% Found (fun (F:(fofType->fofType)) (G:(fofType->fofType)) (LESS:(fofType->(fofType->Prop))) (x:((and ((fun_increasing F) LESS)) ((fun_decreasing G) LESS)))=> (((fun (P:Type) (x0:(((fun_increasing F) LESS)->(((fun_decreasing G) LESS)->P)))=> (((((and_rect ((fun_increasing F) LESS)) ((fun_decreasing G) LESS)) P) x0) x)) ((fun_decreasing ((fun_composition F) G)) LESS)) (fun (x0:((fun_increasing F) LESS)) (x1:((fun_decreasing G) LESS)) (X:fofType) (Y:fofType) (x2:((LESS X) Y))=> (((x1 (F X)) (F Y)) (((x0 X) Y) x2))))) as proof of (forall (G:(fofType->fofType)) (LESS:(fofType->(fofType->Prop))), (((and ((fun_increasing F) LESS)) ((fun_decreasing G) LESS))->((fun_decreasing ((fun_composition F) G)) LESS)))
% Found (fun (F:(fofType->fofType)) (G:(fofType->fofType)) (LESS:(fofType->(fofType->Prop))) (x:((and ((fun_increasing F) LESS)) ((fun_decreasing G) LESS)))=> (((fun (P:Type) (x0:(((fun_increasing F) LESS)->(((fun_decreasing G) LESS)->P)))=> (((((and_rect ((fun_increasing F) LESS)) ((fun_decreasing G) LESS)) P) x0) x)) ((fun_decreasing ((fun_composition F) G)) LESS)) (fun (x0:((fun_increasing F) LESS)) (x1:((fun_decreasing G) LESS)) (X:fofType) (Y:fofType) (x2:((LESS X) Y))=> (((x1 (F X)) (F Y)) (((x0 X) Y) x2))))) as proof of (forall (F:(fofType->fofType)) (G:(fofType->fofType)) (LESS:(fofType->(fofType->Prop))), (((and ((fun_increasing F) LESS)) ((fun_decreasing G) LESS))->((fun_decreasing ((fun_composition F) G)) LESS)))
% Got proof (fun (F:(fofType->fofType)) (G:(fofType->fofType)) (LESS:(fofType->(fofType->Prop))) (x:((and ((fun_increasing F) LESS)) ((fun_decreasing G) LESS)))=> (((fun (P:Type) (x0:(((fun_increasing F) LESS)->(((fun_decreasing G) LESS)->P)))=> (((((and_rect ((fun_increasing F) LESS)) ((fun_decreasing G) LESS)) P) x0) x)) ((fun_decreasing ((fun_composition F) G)) LESS)) (fun (x0:((fun_increasing F) LESS)) (x1:((fun_decreasing G) LESS)) (X:fofType) (Y:fofType) (x2:((LESS X) Y))=> (((x1 (F X)) (F Y)) (((x0 X) Y) x2)))))
% Time elapsed = 0.433032s
% node=43 cost=325.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 (F:(fofType->fofType)) (G:(fofType->fofType)) (LESS:(fofType->(fofType->Prop))) (x:((and ((fun_increasing F) LESS)) ((fun_decreasing G) LESS)))=> (((fun (P:Type) (x0:(((fun_increasing F) LESS)->(((fun_decreasing G) LESS)->P)))=> (((((and_rect ((fun_increasing F) LESS)) ((fun_decreasing G) LESS)) P) x0) x)) ((fun_decreasing ((fun_composition F) G)) LESS)) (fun (x0:((fun_increasing F) LESS)) (x1:((fun_decreasing G) LESS)) (X:fofType) (Y:fofType) (x2:((LESS X) Y))=> (((x1 (F X)) (F Y)) (((x0 X) Y) x2)))))
% % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% EOF
%------------------------------------------------------------------------------