%------------------------------------------------------------------------------ % File : cocATP---0.2.0 % Problem : SET716^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 : n189.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:01 EDT 2014 % Result : Theorem 2.14s % Output : Proof 2.14s % Verified : % SZS Type : None (Parsing solution fails) % Syntax : Number of formulae : 0 % Comments : %------------------------------------------------------------------------------ %----ERROR: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % % Problem : SET716^4 : TPTP v6.1.0. Released v3.6.0. % % Command : python CASC.py /export/starexec/sandbox/benchmark/theBenchmark.p % % Computer : n189.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:44:56 CDT 2014 % % CPUTime : 2.14 % 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 0x26fa950>, <kernel.DependentProduct object at 0x26faef0>) 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 0x26d8d40>, <kernel.DependentProduct object at 0x26fa320>) 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 0x26fa560>, <kernel.DependentProduct object at 0x26faf80>) 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 0x26faf80>, <kernel.DependentProduct object at 0x26fa170>) 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 0x26fa050>, <kernel.DependentProduct object at 0x26fad88>) 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 0x26fa560>, <kernel.DependentProduct object at 0x26faf80>) 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 0x26fad88>, <kernel.DependentProduct object at 0x231ecb0>) 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 0x26fa050>, <kernel.DependentProduct object at 0x231ef80>) 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)), (((and (fun_injective F)) (fun_injective G))->(fun_injective ((fun_composition F) G)))) of role conjecture named thm % Conjecture to prove = (forall (F:(fofType->fofType)) (G:(fofType->fofType)), (((and (fun_injective F)) (fun_injective G))->(fun_injective ((fun_composition F) G)))):Prop % Parameter fofType_DUMMY:fofType. % We need to prove ['(forall (F:(fofType->fofType)) (G:(fofType->fofType)), (((and (fun_injective F)) (fun_injective G))->(fun_injective ((fun_composition F) G))))'] % 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)), (((and (fun_injective F)) (fun_injective G))->(fun_injective ((fun_composition F) G)))) % Found x1000:=(x100 x2):(((eq fofType) (F X)) (F Y)) % Found (x100 x2) as proof of (((eq fofType) (F X)) (F Y)) % Found ((x10 (F Y)) x2) as proof of (((eq fofType) (F X)) (F Y)) % Found (((x1 (F X)) (F Y)) x2) as proof of (((eq fofType) (F X)) (F Y)) % Found (((x1 (F X)) (F Y)) x2) as proof of (((eq fofType) (F X)) (F Y)) % Found (x000 (((x1 (F X)) (F Y)) x2)) as proof of (((eq fofType) X) Y) % Found ((x00 Y) (((x1 (F X)) (F Y)) x2)) as proof of (((eq fofType) X) Y) % Found (((x0 X) Y) (((x1 (F X)) (F Y)) x2)) as proof of (((eq fofType) X) Y) % Found (fun (x2:(((eq fofType) (((fun_composition F) G) X)) (((fun_composition F) G) Y)))=> (((x0 X) Y) (((x1 (F X)) (F Y)) x2))) as proof of (((eq fofType) X) Y) % Found (fun (Y:fofType) (x2:(((eq fofType) (((fun_composition F) G) X)) (((fun_composition F) G) Y)))=> (((x0 X) Y) (((x1 (F X)) (F Y)) x2))) as proof of ((((eq fofType) (((fun_composition F) G) X)) (((fun_composition F) G) Y))->(((eq fofType) X) Y)) % Found (fun (X:fofType) (Y:fofType) (x2:(((eq fofType) (((fun_composition F) G) X)) (((fun_composition F) G) Y)))=> (((x0 X) Y) (((x1 (F X)) (F Y)) x2))) as proof of (forall (Y:fofType), ((((eq fofType) (((fun_composition F) G) X)) (((fun_composition F) G) Y))->(((eq fofType) X) Y))) % Found (fun (x1:(fun_injective G)) (X:fofType) (Y:fofType) (x2:(((eq fofType) (((fun_composition F) G) X)) (((fun_composition F) G) Y)))=> (((x0 X) Y) (((x1 (F X)) (F Y)) x2))) as proof of (fun_injective ((fun_composition F) G)) % Found (fun (x0:(fun_injective F)) (x1:(fun_injective G)) (X:fofType) (Y:fofType) (x2:(((eq fofType) (((fun_composition F) G) X)) (((fun_composition F) G) Y)))=> (((x0 X) Y) (((x1 (F X)) (F Y)) x2))) as proof of ((fun_injective G)->(fun_injective ((fun_composition F) G))) % Found (fun (x0:(fun_injective F)) (x1:(fun_injective G)) (X:fofType) (Y:fofType) (x2:(((eq fofType) (((fun_composition F) G) X)) (((fun_composition F) G) Y)))=> (((x0 X) Y) (((x1 (F X)) (F Y)) x2))) as proof of ((fun_injective F)->((fun_injective G)->(fun_injective ((fun_composition F) G)))) % Found (and_rect00 (fun (x0:(fun_injective F)) (x1:(fun_injective G)) (X:fofType) (Y:fofType) (x2:(((eq fofType) (((fun_composition F) G) X)) (((fun_composition F) G) Y)))=> (((x0 X) Y) (((x1 (F X)) (F Y)) x2)))) as proof of (fun_injective ((fun_composition F) G)) % Found ((and_rect0 (fun_injective ((fun_composition F) G))) (fun (x0:(fun_injective F)) (x1:(fun_injective G)) (X:fofType) (Y:fofType) (x2:(((eq fofType) (((fun_composition F) G) X)) (((fun_composition F) G) Y)))=> (((x0 X) Y) (((x1 (F X)) (F Y)) x2)))) as proof of (fun_injective ((fun_composition F) G)) % Found (((fun (P:Type) (x0:((fun_injective F)->((fun_injective G)->P)))=> (((((and_rect (fun_injective F)) (fun_injective G)) P) x0) x)) (fun_injective ((fun_composition F) G))) (fun (x0:(fun_injective F)) (x1:(fun_injective G)) (X:fofType) (Y:fofType) (x2:(((eq fofType) (((fun_composition F) G) X)) (((fun_composition F) G) Y)))=> (((x0 X) Y) (((x1 (F X)) (F Y)) x2)))) as proof of (fun_injective ((fun_composition F) G)) % Found (fun (x:((and (fun_injective F)) (fun_injective G)))=> (((fun (P:Type) (x0:((fun_injective F)->((fun_injective G)->P)))=> (((((and_rect (fun_injective F)) (fun_injective G)) P) x0) x)) (fun_injective ((fun_composition F) G))) (fun (x0:(fun_injective F)) (x1:(fun_injective G)) (X:fofType) (Y:fofType) (x2:(((eq fofType) (((fun_composition F) G) X)) (((fun_composition F) G) Y)))=> (((x0 X) Y) (((x1 (F X)) (F Y)) x2))))) as proof of (fun_injective ((fun_composition F) G)) % Found (fun (G:(fofType->fofType)) (x:((and (fun_injective F)) (fun_injective G)))=> (((fun (P:Type) (x0:((fun_injective F)->((fun_injective G)->P)))=> (((((and_rect (fun_injective F)) (fun_injective G)) P) x0) x)) (fun_injective ((fun_composition F) G))) (fun (x0:(fun_injective F)) (x1:(fun_injective G)) (X:fofType) (Y:fofType) (x2:(((eq fofType) (((fun_composition F) G) X)) (((fun_composition F) G) Y)))=> (((x0 X) Y) (((x1 (F X)) (F Y)) x2))))) as proof of (((and (fun_injective F)) (fun_injective G))->(fun_injective ((fun_composition F) G))) % Found (fun (F:(fofType->fofType)) (G:(fofType->fofType)) (x:((and (fun_injective F)) (fun_injective G)))=> (((fun (P:Type) (x0:((fun_injective F)->((fun_injective G)->P)))=> (((((and_rect (fun_injective F)) (fun_injective G)) P) x0) x)) (fun_injective ((fun_composition F) G))) (fun (x0:(fun_injective F)) (x1:(fun_injective G)) (X:fofType) (Y:fofType) (x2:(((eq fofType) (((fun_composition F) G) X)) (((fun_composition F) G) Y)))=> (((x0 X) Y) (((x1 (F X)) (F Y)) x2))))) as proof of (forall (G:(fofType->fofType)), (((and (fun_injective F)) (fun_injective G))->(fun_injective ((fun_composition F) G)))) % Found (fun (F:(fofType->fofType)) (G:(fofType->fofType)) (x:((and (fun_injective F)) (fun_injective G)))=> (((fun (P:Type) (x0:((fun_injective F)->((fun_injective G)->P)))=> (((((and_rect (fun_injective F)) (fun_injective G)) P) x0) x)) (fun_injective ((fun_composition F) G))) (fun (x0:(fun_injective F)) (x1:(fun_injective G)) (X:fofType) (Y:fofType) (x2:(((eq fofType) (((fun_composition F) G) X)) (((fun_composition F) G) Y)))=> (((x0 X) Y) (((x1 (F X)) (F Y)) x2))))) as proof of (forall (F:(fofType->fofType)) (G:(fofType->fofType)), (((and (fun_injective F)) (fun_injective G))->(fun_injective ((fun_composition F) G)))) % Got proof (fun (F:(fofType->fofType)) (G:(fofType->fofType)) (x:((and (fun_injective F)) (fun_injective G)))=> (((fun (P:Type) (x0:((fun_injective F)->((fun_injective G)->P)))=> (((((and_rect (fun_injective F)) (fun_injective G)) P) x0) x)) (fun_injective ((fun_composition F) G))) (fun (x0:(fun_injective F)) (x1:(fun_injective G)) (X:fofType) (Y:fofType) (x2:(((eq fofType) (((fun_composition F) G) X)) (((fun_composition F) G) Y)))=> (((x0 X) Y) (((x1 (F X)) (F Y)) x2))))) % Time elapsed = 1.779414s % node=213 cost=316.000000 depth=19 % :::::::::::::::::::::: % % 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)) (x:((and (fun_injective F)) (fun_injective G)))=> (((fun (P:Type) (x0:((fun_injective F)->((fun_injective G)->P)))=> (((((and_rect (fun_injective F)) (fun_injective G)) P) x0) x)) (fun_injective ((fun_composition F) G))) (fun (x0:(fun_injective F)) (x1:(fun_injective G)) (X:fofType) (Y:fofType) (x2:(((eq fofType) (((fun_composition F) G) X)) (((fun_composition F) G) Y)))=> (((x0 X) Y) (((x1 (F X)) (F Y)) x2))))) % % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p % EOF %------------------------------------------------------------------------------