%------------------------------------------------------------------------------ % File : cocATP---0.2.0 % Problem : SEU729^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 : n116.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.68s % Output : Proof 0.68s % Verified : % SZS Type : None (Parsing solution fails) % Syntax : Number of formulae : 0 % Comments : %------------------------------------------------------------------------------ %----ERROR: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % % Problem : SEU729^2 : TPTP v6.1.0. Released v3.7.0. % % Command : python CASC.py /export/starexec/sandbox/benchmark/theBenchmark.p % % Computer : n116.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:46 CDT 2014 % % CPUTime : 0.68 % 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 0xe79b90>, <kernel.DependentProduct object at 0xe79758>) of role type named in_type % Using role type % Declaring in:(fofType->(fofType->Prop)) % FOF formula (<kernel.Constant object at 0xe79908>, <kernel.DependentProduct object at 0xe79cb0>) of role type named powerset_type % Using role type % Declaring powerset:(fofType->fofType) % FOF formula (<kernel.Constant object at 0xe79248>, <kernel.DependentProduct object at 0xe79680>) of role type named subset_type % Using role type % Declaring subset:(fofType->(fofType->Prop)) % FOF formula (<kernel.Constant object at 0xe79bd8>, <kernel.DependentProduct object at 0xe79cb0>) of role type named setminus_type % Using role type % Declaring setminus:(fofType->(fofType->fofType)) % FOF formula (<kernel.Constant object at 0xe79b90>, <kernel.Sort object at 0xb4b3f8>) 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 0xe79680>, <kernel.Sort object at 0xb4b3f8>) 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 0xe79248>, <kernel.Sort object at 0xb4b3f8>) of role type named doubleComplementI1_type % Using role type % Declaring doubleComplementI1:Prop % FOF formula (((eq Prop) doubleComplementI1) (forall (A:fofType) (X:fofType), (((in X) (powerset A))->(forall (Xx:fofType), (((in Xx) A)->(((in Xx) X)->((in Xx) ((setminus A) ((setminus A) X))))))))) of role definition named doubleComplementI1 % A new definition: (((eq Prop) doubleComplementI1) (forall (A:fofType) (X:fofType), (((in X) (powerset A))->(forall (Xx:fofType), (((in Xx) A)->(((in Xx) X)->((in Xx) ((setminus A) ((setminus A) X))))))))) % Defined: doubleComplementI1:=(forall (A:fofType) (X:fofType), (((in X) (powerset A))->(forall (Xx:fofType), (((in Xx) A)->(((in Xx) X)->((in Xx) ((setminus A) ((setminus A) X)))))))) % FOF formula (complementT_lem->(subsetTI->(doubleComplementI1->(forall (A:fofType) (X:fofType), (((in X) (powerset A))->((subset X) ((setminus A) ((setminus A) X)))))))) of role conjecture named doubleComplementSub1 % Conjecture to prove = (complementT_lem->(subsetTI->(doubleComplementI1->(forall (A:fofType) (X:fofType), (((in X) (powerset A))->((subset X) ((setminus A) ((setminus A) X)))))))):Prop % Parameter fofType_DUMMY:fofType. % We need to prove ['(complementT_lem->(subsetTI->(doubleComplementI1->(forall (A:fofType) (X:fofType), (((in X) (powerset A))->((subset X) ((setminus A) ((setminus A) 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 doubleComplementI1:=(forall (A:fofType) (X:fofType), (((in X) (powerset A))->(forall (Xx:fofType), (((in Xx) A)->(((in Xx) X)->((in Xx) ((setminus A) ((setminus A) X)))))))):Prop. % Trying to prove (complementT_lem->(subsetTI->(doubleComplementI1->(forall (A:fofType) (X:fofType), (((in X) (powerset A))->((subset X) ((setminus A) ((setminus A) 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) X)->((in Xx) ((setminus A) ((setminus A) X)))))) % Found (x100 x2) as proof of (forall (Xx:fofType), (((in Xx) A)->(((in Xx) X)->((in Xx) ((setminus A) ((setminus A) X)))))) % Found ((x10 X) x2) as proof of (forall (Xx:fofType), (((in Xx) A)->(((in Xx) X)->((in Xx) ((setminus A) ((setminus A) X)))))) % Found (((x1 A) X) x2) as proof of (forall (Xx:fofType), (((in Xx) A)->(((in Xx) X)->((in Xx) ((setminus A) ((setminus A) X)))))) % Found (((x1 A) X) x2) as proof of (forall (Xx:fofType), (((in Xx) A)->(((in Xx) X)->((in Xx) ((setminus A) ((setminus A) 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 x2) (((x A) ((setminus A) X)) (((x A) X) x2))) (((x1 A) X) x2)) as proof of ((subset X) ((setminus A) ((setminus A) X))) % Found ((((x000 A) x2) (((x A) ((setminus A) X)) (((x A) X) x2))) (((x1 A) X) x2)) as proof of ((subset X) ((setminus A) ((setminus A) X))) % Found (((((fun (A0:fofType) (x3:((in X) (powerset A0)))=> (((x00 A0) x3) ((setminus A) ((setminus A) X)))) A) x2) (((x A) ((setminus A) X)) (((x A) X) x2))) (((x1 A) X) x2)) as proof of ((subset X) ((setminus A) ((setminus A) X))) % Found (((((fun (A0:fofType) (x3:((in X) (powerset A0)))=> ((((fun (A0:fofType)=> ((x0 A0) X)) A0) x3) ((setminus A) ((setminus A) X)))) A) x2) (((x A) ((setminus A) X)) (((x A) X) x2))) (((x1 A) X) x2)) as proof of ((subset X) ((setminus A) ((setminus A) X))) % Found (fun (x2:((in X) (powerset A)))=> (((((fun (A0:fofType) (x3:((in X) (powerset A0)))=> ((((fun (A0:fofType)=> ((x0 A0) X)) A0) x3) ((setminus A) ((setminus A) X)))) A) x2) (((x A) ((setminus A) X)) (((x A) X) x2))) (((x1 A) X) x2))) as proof of ((subset X) ((setminus A) ((setminus A) X))) % Found (fun (X:fofType) (x2:((in X) (powerset A)))=> (((((fun (A0:fofType) (x3:((in X) (powerset A0)))=> ((((fun (A0:fofType)=> ((x0 A0) X)) A0) x3) ((setminus A) ((setminus A) X)))) A) x2) (((x A) ((setminus A) X)) (((x A) X) x2))) (((x1 A) X) x2))) as proof of (((in X) (powerset A))->((subset X) ((setminus A) ((setminus A) X)))) % Found (fun (A:fofType) (X:fofType) (x2:((in X) (powerset A)))=> (((((fun (A0:fofType) (x3:((in X) (powerset A0)))=> ((((fun (A0:fofType)=> ((x0 A0) X)) A0) x3) ((setminus A) ((setminus A) X)))) A) x2) (((x A) ((setminus A) X)) (((x A) X) x2))) (((x1 A) X) x2))) as proof of (forall (X:fofType), (((in X) (powerset A))->((subset X) ((setminus A) ((setminus A) X))))) % Found (fun (x1:doubleComplementI1) (A:fofType) (X:fofType) (x2:((in X) (powerset A)))=> (((((fun (A0:fofType) (x3:((in X) (powerset A0)))=> ((((fun (A0:fofType)=> ((x0 A0) X)) A0) x3) ((setminus A) ((setminus A) X)))) A) x2) (((x A) ((setminus A) X)) (((x A) X) x2))) (((x1 A) X) x2))) as proof of (forall (A:fofType) (X:fofType), (((in X) (powerset A))->((subset X) ((setminus A) ((setminus A) X))))) % Found (fun (x0:subsetTI) (x1:doubleComplementI1) (A:fofType) (X:fofType) (x2:((in X) (powerset A)))=> (((((fun (A0:fofType) (x3:((in X) (powerset A0)))=> ((((fun (A0:fofType)=> ((x0 A0) X)) A0) x3) ((setminus A) ((setminus A) X)))) A) x2) (((x A) ((setminus A) X)) (((x A) X) x2))) (((x1 A) X) x2))) as proof of (doubleComplementI1->(forall (A:fofType) (X:fofType), (((in X) (powerset A))->((subset X) ((setminus A) ((setminus A) X)))))) % Found (fun (x:complementT_lem) (x0:subsetTI) (x1:doubleComplementI1) (A:fofType) (X:fofType) (x2:((in X) (powerset A)))=> (((((fun (A0:fofType) (x3:((in X) (powerset A0)))=> ((((fun (A0:fofType)=> ((x0 A0) X)) A0) x3) ((setminus A) ((setminus A) X)))) A) x2) (((x A) ((setminus A) X)) (((x A) X) x2))) (((x1 A) X) x2))) as proof of (subsetTI->(doubleComplementI1->(forall (A:fofType) (X:fofType), (((in X) (powerset A))->((subset X) ((setminus A) ((setminus A) X))))))) % Found (fun (x:complementT_lem) (x0:subsetTI) (x1:doubleComplementI1) (A:fofType) (X:fofType) (x2:((in X) (powerset A)))=> (((((fun (A0:fofType) (x3:((in X) (powerset A0)))=> ((((fun (A0:fofType)=> ((x0 A0) X)) A0) x3) ((setminus A) ((setminus A) X)))) A) x2) (((x A) ((setminus A) X)) (((x A) X) x2))) (((x1 A) X) x2))) as proof of (complementT_lem->(subsetTI->(doubleComplementI1->(forall (A:fofType) (X:fofType), (((in X) (powerset A))->((subset X) ((setminus A) ((setminus A) X)))))))) % Got proof (fun (x:complementT_lem) (x0:subsetTI) (x1:doubleComplementI1) (A:fofType) (X:fofType) (x2:((in X) (powerset A)))=> (((((fun (A0:fofType) (x3:((in X) (powerset A0)))=> ((((fun (A0:fofType)=> ((x0 A0) X)) A0) x3) ((setminus A) ((setminus A) X)))) A) x2) (((x A) ((setminus A) X)) (((x A) X) x2))) (((x1 A) X) x2))) % Time elapsed = 0.349065s % node=58 cost=911.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:doubleComplementI1) (A:fofType) (X:fofType) (x2:((in X) (powerset A)))=> (((((fun (A0:fofType) (x3:((in X) (powerset A0)))=> ((((fun (A0:fofType)=> ((x0 A0) X)) A0) x3) ((setminus A) ((setminus A) X)))) A) x2) (((x A) ((setminus A) X)) (((x A) X) x2))) (((x1 A) X) x2))) % % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p % EOF %------------------------------------------------------------------------------