%------------------------------------------------------------------------------ % File : cocATP---0.2.0 % Problem : SEU730^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 : n092.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:57 EDT 2014 % Result : Theorem 0.71s % Output : Proof 0.71s % Verified : % SZS Type : None (Parsing solution fails) % Syntax : Number of formulae : 0 % Comments : %------------------------------------------------------------------------------ %----ERROR: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % % Problem : SEU730^2 : TPTP v6.1.0. Released v3.7.0. % % Command : python CASC.py /export/starexec/sandbox/benchmark/theBenchmark.p % % Computer : n092.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:19:56 CDT 2014 % % CPUTime : 0.71 % 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 0x19a9d88>, <kernel.DependentProduct object at 0x1f1b248>) of role type named in_type % Using role type % Declaring in:(fofType->(fofType->Prop)) % FOF formula (<kernel.Constant object at 0x19ac200>, <kernel.DependentProduct object at 0x1f1bcf8>) of role type named powerset_type % Using role type % Declaring powerset:(fofType->fofType) % FOF formula (<kernel.Constant object at 0x1ca1cb0>, <kernel.DependentProduct object at 0x1f1b200>) of role type named subset_type % Using role type % Declaring subset:(fofType->(fofType->Prop)) % FOF formula (<kernel.Constant object at 0x19ac200>, <kernel.DependentProduct object at 0x1f1be60>) of role type named setminus_type % Using role type % Declaring setminus:(fofType->(fofType->fofType)) % FOF formula (<kernel.Constant object at 0x19ac200>, <kernel.Sort object at 0x1d74fc8>) of role type named complementT_lem_type % Using role type % Declaring complementT_lem:Prop % FOF formula (((eq Prop) complementT_lem) (forall (A:fofType) (X:fofType), (((in X) (powerset A))->((in ((setminus A) X)) (powerset A))))) of role definition named complementT_lem % A new definition: (((eq Prop) complementT_lem) (forall (A:fofType) (X:fofType), (((in X) (powerset A))->((in ((setminus A) X)) (powerset A))))) % Defined: complementT_lem:=(forall (A:fofType) (X:fofType), (((in X) (powerset A))->((in ((setminus A) X)) (powerset A)))) % FOF formula (<kernel.Constant object at 0x1f19c20>, <kernel.Sort object at 0x1d74fc8>) of role type named subsetTI_type % Using role type % Declaring subsetTI:Prop % FOF formula (((eq Prop) subsetTI) (forall (A:fofType) (X:fofType), (((in X) (powerset A))->(forall (Y:fofType), (((in Y) (powerset A))->((forall (Xx:fofType), (((in Xx) A)->(((in Xx) X)->((in Xx) Y))))->((subset X) Y))))))) of role definition named subsetTI % A new definition: (((eq Prop) subsetTI) (forall (A:fofType) (X:fofType), (((in X) (powerset A))->(forall (Y:fofType), (((in Y) (powerset A))->((forall (Xx:fofType), (((in Xx) A)->(((in Xx) X)->((in Xx) Y))))->((subset X) Y))))))) % Defined: subsetTI:=(forall (A:fofType) (X:fofType), (((in X) (powerset A))->(forall (Y:fofType), (((in Y) (powerset A))->((forall (Xx:fofType), (((in Xx) A)->(((in Xx) X)->((in Xx) Y))))->((subset X) Y)))))) % FOF formula (<kernel.Constant object at 0x1f19c20>, <kernel.Sort object at 0x1d74fc8>) of role type named doubleComplementE1_type % Using role type % Declaring doubleComplementE1:Prop % FOF formula (((eq Prop) doubleComplementE1) (forall (A:fofType) (X:fofType), (((in X) (powerset A))->(forall (Xx:fofType), (((in Xx) A)->(((in Xx) ((setminus A) ((setminus A) X)))->((in Xx) X))))))) of role definition named doubleComplementE1 % A new definition: (((eq Prop) doubleComplementE1) (forall (A:fofType) (X:fofType), (((in X) (powerset A))->(forall (Xx:fofType), (((in Xx) A)->(((in Xx) ((setminus A) ((setminus A) X)))->((in Xx) X))))))) % Defined: doubleComplementE1:=(forall (A:fofType) (X:fofType), (((in X) (powerset A))->(forall (Xx:fofType), (((in Xx) A)->(((in Xx) ((setminus A) ((setminus A) X)))->((in Xx) X)))))) % FOF formula (complementT_lem->(subsetTI->(doubleComplementE1->(forall (A:fofType) (X:fofType), (((in X) (powerset A))->((subset ((setminus A) ((setminus A) X))) X)))))) of role conjecture named doubleComplementSub2 % Conjecture to prove = (complementT_lem->(subsetTI->(doubleComplementE1->(forall (A:fofType) (X:fofType), (((in X) (powerset A))->((subset ((setminus A) ((setminus A) X))) X)))))):Prop % Parameter fofType_DUMMY:fofType. % We need to prove ['(complementT_lem->(subsetTI->(doubleComplementE1->(forall (A:fofType) (X:fofType), (((in X) (powerset A))->((subset ((setminus A) ((setminus A) X))) X))))))'] % Parameter fofType:Type. % Parameter in:(fofType->(fofType->Prop)). % Parameter powerset:(fofType->fofType). % Parameter subset:(fofType->(fofType->Prop)). % Parameter setminus:(fofType->(fofType->fofType)). % Definition complementT_lem:=(forall (A:fofType) (X:fofType), (((in X) (powerset A))->((in ((setminus A) X)) (powerset A)))):Prop. % Definition subsetTI:=(forall (A:fofType) (X:fofType), (((in X) (powerset A))->(forall (Y:fofType), (((in Y) (powerset A))->((forall (Xx:fofType), (((in Xx) A)->(((in Xx) X)->((in Xx) Y))))->((subset X) Y)))))):Prop. % Definition doubleComplementE1:=(forall (A:fofType) (X:fofType), (((in X) (powerset A))->(forall (Xx:fofType), (((in Xx) A)->(((in Xx) ((setminus A) ((setminus A) X)))->((in Xx) X)))))):Prop. % Trying to prove (complementT_lem->(subsetTI->(doubleComplementE1->(forall (A:fofType) (X:fofType), (((in X) (powerset A))->((subset ((setminus A) ((setminus A) X))) X)))))) % Found x2:((in X) (powerset A)) % Found x2 as proof of ((in X) (powerset A)) % Found x1000:=(x100 x2):(forall (Xx:fofType), (((in Xx) A)->(((in Xx) ((setminus A) ((setminus A) X)))->((in Xx) X)))) % Found (x100 x2) as proof of (forall (Xx:fofType), (((in Xx) A)->(((in Xx) ((setminus A) ((setminus A) X)))->((in Xx) X)))) % Found ((x10 X) x2) as proof of (forall (Xx:fofType), (((in Xx) A)->(((in Xx) ((setminus A) ((setminus A) X)))->((in Xx) X)))) % Found (((x1 A) X) x2) as proof of (forall (Xx:fofType), (((in Xx) A)->(((in Xx) ((setminus A) ((setminus A) X)))->((in Xx) X)))) % Found (((x1 A) X) x2) as proof of (forall (Xx:fofType), (((in Xx) A)->(((in Xx) ((setminus A) ((setminus A) X)))->((in Xx) X)))) % Found x310:=(x31 x2):((in ((setminus A) X)) (powerset A)) % Found (x31 x2) as proof of ((in ((setminus A) X)) (powerset A)) % Found ((x3 X) x2) as proof of ((in ((setminus A) X)) (powerset A)) % Found ((x3 X) x2) as proof of ((in ((setminus A) X)) (powerset A)) % Found (x30 ((x3 X) x2)) as proof of ((in ((setminus A) ((setminus A) X))) (powerset A)) % Found ((x3 ((setminus A) X)) ((x3 X) x2)) as proof of ((in ((setminus A) ((setminus A) X))) (powerset A)) % Found (((x A) ((setminus A) X)) (((x A) X) x2)) as proof of ((in ((setminus A) ((setminus A) X))) (powerset A)) % Found (((x A) ((setminus A) X)) (((x A) X) x2)) as proof of ((in ((setminus A) ((setminus A) X))) (powerset A)) % Found (((x0000 (((x A) ((setminus A) X)) (((x A) X) x2))) x2) (((x1 A) X) x2)) as proof of ((subset ((setminus A) ((setminus A) X))) X) % Found ((((x000 A) (((x A) ((setminus A) X)) (((x A) X) x2))) x2) (((x1 A) X) x2)) as proof of ((subset ((setminus A) ((setminus A) X))) X) % Found (((((fun (A0:fofType) (x3:((in ((setminus A) ((setminus A) X))) (powerset A0)))=> (((x00 A0) x3) X)) A) (((x A) ((setminus A) X)) (((x A) X) x2))) x2) (((x1 A) X) x2)) as proof of ((subset ((setminus A) ((setminus A) X))) X) % Found (((((fun (A0:fofType) (x3:((in ((setminus A) ((setminus A) X))) (powerset A0)))=> ((((fun (A0:fofType)=> ((x0 A0) ((setminus A) ((setminus A) X)))) A0) x3) X)) A) (((x A) ((setminus A) X)) (((x A) X) x2))) x2) (((x1 A) X) x2)) as proof of ((subset ((setminus A) ((setminus A) X))) X) % Found (fun (x2:((in X) (powerset A)))=> (((((fun (A0:fofType) (x3:((in ((setminus A) ((setminus A) X))) (powerset A0)))=> ((((fun (A0:fofType)=> ((x0 A0) ((setminus A) ((setminus A) X)))) A0) x3) X)) A) (((x A) ((setminus A) X)) (((x A) X) x2))) x2) (((x1 A) X) x2))) as proof of ((subset ((setminus A) ((setminus A) X))) X) % Found (fun (X:fofType) (x2:((in X) (powerset A)))=> (((((fun (A0:fofType) (x3:((in ((setminus A) ((setminus A) X))) (powerset A0)))=> ((((fun (A0:fofType)=> ((x0 A0) ((setminus A) ((setminus A) X)))) A0) x3) X)) A) (((x A) ((setminus A) X)) (((x A) X) x2))) x2) (((x1 A) X) x2))) as proof of (((in X) (powerset A))->((subset ((setminus A) ((setminus A) X))) X)) % Found (fun (A:fofType) (X:fofType) (x2:((in X) (powerset A)))=> (((((fun (A0:fofType) (x3:((in ((setminus A) ((setminus A) X))) (powerset A0)))=> ((((fun (A0:fofType)=> ((x0 A0) ((setminus A) ((setminus A) X)))) A0) x3) X)) A) (((x A) ((setminus A) X)) (((x A) X) x2))) x2) (((x1 A) X) x2))) as proof of (forall (X:fofType), (((in X) (powerset A))->((subset ((setminus A) ((setminus A) X))) X))) % Found (fun (x1:doubleComplementE1) (A:fofType) (X:fofType) (x2:((in X) (powerset A)))=> (((((fun (A0:fofType) (x3:((in ((setminus A) ((setminus A) X))) (powerset A0)))=> ((((fun (A0:fofType)=> ((x0 A0) ((setminus A) ((setminus A) X)))) A0) x3) X)) A) (((x A) ((setminus A) X)) (((x A) X) x2))) x2) (((x1 A) X) x2))) as proof of (forall (A:fofType) (X:fofType), (((in X) (powerset A))->((subset ((setminus A) ((setminus A) X))) X))) % Found (fun (x0:subsetTI) (x1:doubleComplementE1) (A:fofType) (X:fofType) (x2:((in X) (powerset A)))=> (((((fun (A0:fofType) (x3:((in ((setminus A) ((setminus A) X))) (powerset A0)))=> ((((fun (A0:fofType)=> ((x0 A0) ((setminus A) ((setminus A) X)))) A0) x3) X)) A) (((x A) ((setminus A) X)) (((x A) X) x2))) x2) (((x1 A) X) x2))) as proof of (doubleComplementE1->(forall (A:fofType) (X:fofType), (((in X) (powerset A))->((subset ((setminus A) ((setminus A) X))) X)))) % Found (fun (x:complementT_lem) (x0:subsetTI) (x1:doubleComplementE1) (A:fofType) (X:fofType) (x2:((in X) (powerset A)))=> (((((fun (A0:fofType) (x3:((in ((setminus A) ((setminus A) X))) (powerset A0)))=> ((((fun (A0:fofType)=> ((x0 A0) ((setminus A) ((setminus A) X)))) A0) x3) X)) A) (((x A) ((setminus A) X)) (((x A) X) x2))) x2) (((x1 A) X) x2))) as proof of (subsetTI->(doubleComplementE1->(forall (A:fofType) (X:fofType), (((in X) (powerset A))->((subset ((setminus A) ((setminus A) X))) X))))) % Found (fun (x:complementT_lem) (x0:subsetTI) (x1:doubleComplementE1) (A:fofType) (X:fofType) (x2:((in X) (powerset A)))=> (((((fun (A0:fofType) (x3:((in ((setminus A) ((setminus A) X))) (powerset A0)))=> ((((fun (A0:fofType)=> ((x0 A0) ((setminus A) ((setminus A) X)))) A0) x3) X)) A) (((x A) ((setminus A) X)) (((x A) X) x2))) x2) (((x1 A) X) x2))) as proof of (complementT_lem->(subsetTI->(doubleComplementE1->(forall (A:fofType) (X:fofType), (((in X) (powerset A))->((subset ((setminus A) ((setminus A) X))) X)))))) % Got proof (fun (x:complementT_lem) (x0:subsetTI) (x1:doubleComplementE1) (A:fofType) (X:fofType) (x2:((in X) (powerset A)))=> (((((fun (A0:fofType) (x3:((in ((setminus A) ((setminus A) X))) (powerset A0)))=> ((((fun (A0:fofType)=> ((x0 A0) ((setminus A) ((setminus A) X)))) A0) x3) X)) A) (((x A) ((setminus A) X)) (((x A) X) x2))) x2) (((x1 A) X) x2))) % Time elapsed = 0.374154s % node=65 cost=764.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:complementT_lem) (x0:subsetTI) (x1:doubleComplementE1) (A:fofType) (X:fofType) (x2:((in X) (powerset A)))=> (((((fun (A0:fofType) (x3:((in ((setminus A) ((setminus A) X))) (powerset A0)))=> ((((fun (A0:fofType)=> ((x0 A0) ((setminus A) ((setminus A) X)))) A0) x3) X)) A) (((x A) ((setminus A) X)) (((x A) X) x2))) x2) (((x1 A) X) x2))) % % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p % EOF %------------------------------------------------------------------------------