%------------------------------------------------------------------------------ % File : cocATP---0.2.0 % Problem : CSR142^1 : TPTP v6.1.0. Released v4.1.0. % Transfm : none % Format : tptp:raw % Command : python CASC.py /export/starexec/sandbox/benchmark/theBenchmark.p % Computer : n180.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:21:05 EDT 2014 % Result : Theorem 0.75s % Output : Proof 0.75s % Verified : % SZS Type : None (Parsing solution fails) % Syntax : Number of formulae : 0 % Comments : %------------------------------------------------------------------------------ %----ERROR: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % % Problem : CSR142^1 : TPTP v6.1.0. Released v4.1.0. % % Command : python CASC.py /export/starexec/sandbox/benchmark/theBenchmark.p % % Computer : n180.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:07:51 CDT 2014 % % CPUTime : 0.75 % 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 0xcacf38>, <kernel.Type object at 0x11b9710>) of role type named numbers % Using role type % Declaring num:Type % FOF formula (<kernel.Constant object at 0xdde3f8>, <kernel.DependentProduct object at 0x11b9710>) of role type named husband_THFTYPE_IiioI % Using role type % Declaring husband_THFTYPE_IiioI:(fofType->(fofType->Prop)) % FOF formula (<kernel.Constant object at 0xdde3f8>, <kernel.Single object at 0xcacdd0>) of role type named lChris_THFTYPE_i % Using role type % Declaring lChris_THFTYPE_i:fofType % FOF formula (<kernel.Constant object at 0xdde3f8>, <kernel.Single object at 0xcacdd0>) of role type named lCorina_THFTYPE_i % Using role type % Declaring lCorina_THFTYPE_i:fofType % FOF formula (<kernel.Constant object at 0xcacf38>, <kernel.DependentProduct object at 0x11b9ea8>) of role type named wife_THFTYPE_IiioI % Using role type % Declaring wife_THFTYPE_IiioI:(fofType->(fofType->Prop)) % FOF formula (<kernel.Constant object at 0x11b9ea8>, <kernel.DependentProduct object at 0x11b9710>) of role type named inverse_THFTYPE_IIiioIIiioIoI % Using role type % Declaring inverse_THFTYPE_IIiioIIiioIoI:((fofType->(fofType->Prop))->((fofType->(fofType->Prop))->Prop)) % FOF formula ((inverse_THFTYPE_IIiioIIiioIoI husband_THFTYPE_IiioI) wife_THFTYPE_IiioI) of role axiom named ax % A new axiom: ((inverse_THFTYPE_IIiioIIiioIoI husband_THFTYPE_IiioI) wife_THFTYPE_IiioI) % FOF formula (forall (REL2:(fofType->(fofType->Prop))) (REL1:(fofType->(fofType->Prop))), (((inverse_THFTYPE_IIiioIIiioIoI REL1) REL2)->(forall (INST1:fofType) (INST2:fofType), ((iff ((REL1 INST1) INST2)) ((REL2 INST2) INST1))))) of role axiom named ax_001 % A new axiom: (forall (REL2:(fofType->(fofType->Prop))) (REL1:(fofType->(fofType->Prop))), (((inverse_THFTYPE_IIiioIIiioIoI REL1) REL2)->(forall (INST1:fofType) (INST2:fofType), ((iff ((REL1 INST1) INST2)) ((REL2 INST2) INST1))))) % FOF formula ((wife_THFTYPE_IiioI lCorina_THFTYPE_i) lChris_THFTYPE_i) of role axiom named ax_002 % A new axiom: ((wife_THFTYPE_IiioI lCorina_THFTYPE_i) lChris_THFTYPE_i) % FOF formula ((ex fofType) (fun (X:fofType)=> ((husband_THFTYPE_IiioI X) lCorina_THFTYPE_i))) of role conjecture named con % Conjecture to prove = ((ex fofType) (fun (X:fofType)=> ((husband_THFTYPE_IiioI X) lCorina_THFTYPE_i))):Prop % Parameter num_DUMMY:num. % We need to prove ['((ex fofType) (fun (X:fofType)=> ((husband_THFTYPE_IiioI X) lCorina_THFTYPE_i)))'] % Parameter num:Type. % Parameter fofType:Type. % Parameter husband_THFTYPE_IiioI:(fofType->(fofType->Prop)). % Parameter lChris_THFTYPE_i:fofType. % Parameter lCorina_THFTYPE_i:fofType. % Parameter wife_THFTYPE_IiioI:(fofType->(fofType->Prop)). % Parameter inverse_THFTYPE_IIiioIIiioIoI:((fofType->(fofType->Prop))->((fofType->(fofType->Prop))->Prop)). % Axiom ax:((inverse_THFTYPE_IIiioIIiioIoI husband_THFTYPE_IiioI) wife_THFTYPE_IiioI). % Axiom ax_001:(forall (REL2:(fofType->(fofType->Prop))) (REL1:(fofType->(fofType->Prop))), (((inverse_THFTYPE_IIiioIIiioIoI REL1) REL2)->(forall (INST1:fofType) (INST2:fofType), ((iff ((REL1 INST1) INST2)) ((REL2 INST2) INST1))))). % Axiom ax_002:((wife_THFTYPE_IiioI lCorina_THFTYPE_i) lChris_THFTYPE_i). % Trying to prove ((ex fofType) (fun (X:fofType)=> ((husband_THFTYPE_IiioI X) lCorina_THFTYPE_i))) % Found iff_sym:=(fun (A:Prop) (B:Prop) (H:((iff A) B))=> ((((conj (B->A)) (A->B)) (((proj2 (A->B)) (B->A)) H)) (((proj1 (A->B)) (B->A)) H))):(forall (A:Prop) (B:Prop), (((iff A) B)->((iff B) A))) % Found iff_sym as proof of (forall (A:Prop) (B:Prop), (((iff A) B)->((iff B) A))) % Found ax_002:((wife_THFTYPE_IiioI lCorina_THFTYPE_i) lChris_THFTYPE_i) % Found ax_002 as proof of ((wife_THFTYPE_IiioI lCorina_THFTYPE_i) lChris_THFTYPE_i) % Found iff_trans:=(fun (A:Prop) (B:Prop) (C:Prop) (AB:((iff A) B)) (BC:((iff B) C))=> ((((conj (A->C)) (C->A)) (fun (x:A)=> ((((proj1 (B->C)) (C->B)) BC) ((((proj1 (A->B)) (B->A)) AB) x)))) (fun (x:C)=> ((((proj2 (A->B)) (B->A)) AB) ((((proj2 (B->C)) (C->B)) BC) x))))):(forall (A:Prop) (B:Prop) (C:Prop), (((iff A) B)->(((iff B) C)->((iff A) C)))) % Found iff_trans as proof of (forall (A:Prop) (B:Prop) (C:Prop), (((iff A) B)->(((iff B) C)->((iff A) C)))) % Found ax_001:(forall (REL2:(fofType->(fofType->Prop))) (REL1:(fofType->(fofType->Prop))), (((inverse_THFTYPE_IIiioIIiioIoI REL1) REL2)->(forall (INST1:fofType) (INST2:fofType), ((iff ((REL1 INST1) INST2)) ((REL2 INST2) INST1))))) % Found ax_001 as proof of (forall (REL2:(fofType->(fofType->Prop))) (REL10:(fofType->(fofType->Prop))), (((inverse_THFTYPE_IIiioIIiioIoI REL10) REL2)->(forall (INST1:fofType) (INST2:fofType), ((iff ((REL10 INST1) INST2)) ((REL2 INST2) INST1))))) % Found iff_refl:=(fun (A:Prop)=> ((((conj (A->A)) (A->A)) (fun (H:A)=> H)) (fun (H:A)=> H))):(forall (P:Prop), ((iff P) P)) % Found iff_refl as proof of (forall (P:Prop), ((iff P) P)) % Found ax:((inverse_THFTYPE_IIiioIIiioIoI husband_THFTYPE_IiioI) wife_THFTYPE_IiioI) % Found ax as proof of ((inverse_THFTYPE_IIiioIIiioIoI husband_THFTYPE_IiioI) wife_THFTYPE_IiioI) % Found ax_001__proj10:=(ax_001__proj1 husband_THFTYPE_IiioI):(forall (REL1:(fofType->(fofType->Prop))), (((inverse_THFTYPE_IIiioIIiioIoI REL1) husband_THFTYPE_IiioI)->(forall (INST1:fofType) (INST2:fofType), (((REL1 INST1) INST2)->((husband_THFTYPE_IiioI INST2) INST1))))) % Found ax_001__proj10 as proof of (forall (REL10:(fofType->(fofType->Prop))), (((inverse_THFTYPE_IIiioIIiioIoI REL10) husband_THFTYPE_IiioI)->(forall (INST1:fofType) (INST2:fofType), (((REL10 INST1) INST2)->((husband_THFTYPE_IiioI INST2) INST1))))) % Found ax:((inverse_THFTYPE_IIiioIIiioIoI husband_THFTYPE_IiioI) wife_THFTYPE_IiioI) % Instantiate: REL2:=wife_THFTYPE_IiioI:(fofType->(fofType->Prop)) % Found ax as proof of ((inverse_THFTYPE_IIiioIIiioIoI husband_THFTYPE_IiioI) REL2) % Found ax_002:((wife_THFTYPE_IiioI lCorina_THFTYPE_i) lChris_THFTYPE_i) % Instantiate: x:=lChris_THFTYPE_i:fofType % Found ax_002 as proof of ((REL2 lCorina_THFTYPE_i) x) % Found ((ax_001__proj20000 ax) ax_002) as proof of ((husband_THFTYPE_IiioI x) lCorina_THFTYPE_i) % Found (((ax_001__proj2000 husband_THFTYPE_IiioI) ax) ax_002) as proof of ((husband_THFTYPE_IiioI x) lCorina_THFTYPE_i) % Found ((((ax_001__proj200 wife_THFTYPE_IiioI) husband_THFTYPE_IiioI) ax) ax_002) as proof of ((husband_THFTYPE_IiioI x) lCorina_THFTYPE_i) % Found (((((fun (REL2:(fofType->(fofType->Prop))) (REL1:(fofType->(fofType->Prop))) (x0:((inverse_THFTYPE_IIiioIIiioIoI REL1) REL2))=> ((((ax_001__proj20 REL2) REL1) x0) lCorina_THFTYPE_i)) wife_THFTYPE_IiioI) husband_THFTYPE_IiioI) ax) ax_002) as proof of ((husband_THFTYPE_IiioI x) lCorina_THFTYPE_i) % Found (((((fun (REL2:(fofType->(fofType->Prop))) (REL1:(fofType->(fofType->Prop))) (x0:((inverse_THFTYPE_IIiioIIiioIoI REL1) REL2))=> (((((fun (REL2:(fofType->(fofType->Prop))) (REL1:(fofType->(fofType->Prop))) (x0:((inverse_THFTYPE_IIiioIIiioIoI REL1) REL2))=> ((((ax_001__proj2 REL2) REL1) x0) x)) REL2) REL1) x0) lCorina_THFTYPE_i)) wife_THFTYPE_IiioI) husband_THFTYPE_IiioI) ax) ax_002) as proof of ((husband_THFTYPE_IiioI x) lCorina_THFTYPE_i) % Found (((((fun (REL2:(fofType->(fofType->Prop))) (REL1:(fofType->(fofType->Prop))) (x0:((inverse_THFTYPE_IIiioIIiioIoI REL1) REL2))=> (((((fun (REL2:(fofType->(fofType->Prop))) (REL1:(fofType->(fofType->Prop))) (x0:((inverse_THFTYPE_IIiioIIiioIoI REL1) REL2))=> ((((ax_001__proj2 REL2) REL1) x0) x)) REL2) REL1) x0) lCorina_THFTYPE_i)) wife_THFTYPE_IiioI) husband_THFTYPE_IiioI) ax) ax_002) as proof of ((husband_THFTYPE_IiioI x) lCorina_THFTYPE_i) % Found (ex_intro000 (((((fun (REL2:(fofType->(fofType->Prop))) (REL1:(fofType->(fofType->Prop))) (x0:((inverse_THFTYPE_IIiioIIiioIoI REL1) REL2))=> (((((fun (REL2:(fofType->(fofType->Prop))) (REL1:(fofType->(fofType->Prop))) (x0:((inverse_THFTYPE_IIiioIIiioIoI REL1) REL2))=> ((((ax_001__proj2 REL2) REL1) x0) x)) REL2) REL1) x0) lCorina_THFTYPE_i)) wife_THFTYPE_IiioI) husband_THFTYPE_IiioI) ax) ax_002)) as proof of ((ex fofType) (fun (X:fofType)=> ((husband_THFTYPE_IiioI X) lCorina_THFTYPE_i))) % Found ((ex_intro00 lChris_THFTYPE_i) (((((fun (REL2:(fofType->(fofType->Prop))) (REL1:(fofType->(fofType->Prop))) (x0:((inverse_THFTYPE_IIiioIIiioIoI REL1) REL2))=> (((((fun (REL2:(fofType->(fofType->Prop))) (REL1:(fofType->(fofType->Prop))) (x0:((inverse_THFTYPE_IIiioIIiioIoI REL1) REL2))=> ((((ax_001__proj2 REL2) REL1) x0) lChris_THFTYPE_i)) REL2) REL1) x0) lCorina_THFTYPE_i)) wife_THFTYPE_IiioI) husband_THFTYPE_IiioI) ax) ax_002)) as proof of ((ex fofType) (fun (X:fofType)=> ((husband_THFTYPE_IiioI X) lCorina_THFTYPE_i))) % Found (((ex_intro0 (fun (X:fofType)=> ((husband_THFTYPE_IiioI X) lCorina_THFTYPE_i))) lChris_THFTYPE_i) (((((fun (REL2:(fofType->(fofType->Prop))) (REL1:(fofType->(fofType->Prop))) (x0:((inverse_THFTYPE_IIiioIIiioIoI REL1) REL2))=> (((((fun (REL2:(fofType->(fofType->Prop))) (REL1:(fofType->(fofType->Prop))) (x0:((inverse_THFTYPE_IIiioIIiioIoI REL1) REL2))=> ((((ax_001__proj2 REL2) REL1) x0) lChris_THFTYPE_i)) REL2) REL1) x0) lCorina_THFTYPE_i)) wife_THFTYPE_IiioI) husband_THFTYPE_IiioI) ax) ax_002)) as proof of ((ex fofType) (fun (X:fofType)=> ((husband_THFTYPE_IiioI X) lCorina_THFTYPE_i))) % Found ((((ex_intro fofType) (fun (X:fofType)=> ((husband_THFTYPE_IiioI X) lCorina_THFTYPE_i))) lChris_THFTYPE_i) (((((fun (REL2:(fofType->(fofType->Prop))) (REL1:(fofType->(fofType->Prop))) (x0:((inverse_THFTYPE_IIiioIIiioIoI REL1) REL2))=> (((((fun (REL2:(fofType->(fofType->Prop))) (REL1:(fofType->(fofType->Prop))) (x0:((inverse_THFTYPE_IIiioIIiioIoI REL1) REL2))=> ((((ax_001__proj2 REL2) REL1) x0) lChris_THFTYPE_i)) REL2) REL1) x0) lCorina_THFTYPE_i)) wife_THFTYPE_IiioI) husband_THFTYPE_IiioI) ax) ax_002)) as proof of ((ex fofType) (fun (X:fofType)=> ((husband_THFTYPE_IiioI X) lCorina_THFTYPE_i))) % Found ((((ex_intro fofType) (fun (X:fofType)=> ((husband_THFTYPE_IiioI X) lCorina_THFTYPE_i))) lChris_THFTYPE_i) (((((fun (REL2:(fofType->(fofType->Prop))) (REL1:(fofType->(fofType->Prop))) (x0:((inverse_THFTYPE_IIiioIIiioIoI REL1) REL2))=> (((((fun (REL2:(fofType->(fofType->Prop))) (REL1:(fofType->(fofType->Prop))) (x0:((inverse_THFTYPE_IIiioIIiioIoI REL1) REL2))=> ((((ax_001__proj2 REL2) REL1) x0) lChris_THFTYPE_i)) REL2) REL1) x0) lCorina_THFTYPE_i)) wife_THFTYPE_IiioI) husband_THFTYPE_IiioI) ax) ax_002)) as proof of ((ex fofType) (fun (X:fofType)=> ((husband_THFTYPE_IiioI X) lCorina_THFTYPE_i))) % Got proof ((((ex_intro fofType) (fun (X:fofType)=> ((husband_THFTYPE_IiioI X) lCorina_THFTYPE_i))) lChris_THFTYPE_i) (((((fun (REL2:(fofType->(fofType->Prop))) (REL1:(fofType->(fofType->Prop))) (x0:((inverse_THFTYPE_IIiioIIiioIoI REL1) REL2))=> (((((fun (REL2:(fofType->(fofType->Prop))) (REL1:(fofType->(fofType->Prop))) (x0:((inverse_THFTYPE_IIiioIIiioIoI REL1) REL2))=> (((((fun (REL2:(fofType->(fofType->Prop))) (REL1:(fofType->(fofType->Prop))) (x:((inverse_THFTYPE_IIiioIIiioIoI REL1) REL2)) (INST1:fofType) (INST2:fofType)=> (((proj2 (((REL1 INST1) INST2)->((REL2 INST2) INST1))) (((REL2 INST2) INST1)->((REL1 INST1) INST2))) (((((ax_001 REL2) REL1) x) INST1) INST2))) REL2) REL1) x0) lChris_THFTYPE_i)) REL2) REL1) x0) lCorina_THFTYPE_i)) wife_THFTYPE_IiioI) husband_THFTYPE_IiioI) ax) ax_002)) % Time elapsed = 0.417484s % node=105 cost=1380.000000 depth=11 % :::::::::::::::::::::: % % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p % ((((ex_intro fofType) (fun (X:fofType)=> ((husband_THFTYPE_IiioI X) lCorina_THFTYPE_i))) lChris_THFTYPE_i) (((((fun (REL2:(fofType->(fofType->Prop))) (REL1:(fofType->(fofType->Prop))) (x0:((inverse_THFTYPE_IIiioIIiioIoI REL1) REL2))=> (((((fun (REL2:(fofType->(fofType->Prop))) (REL1:(fofType->(fofType->Prop))) (x0:((inverse_THFTYPE_IIiioIIiioIoI REL1) REL2))=> (((((fun (REL2:(fofType->(fofType->Prop))) (REL1:(fofType->(fofType->Prop))) (x:((inverse_THFTYPE_IIiioIIiioIoI REL1) REL2)) (INST1:fofType) (INST2:fofType)=> (((proj2 (((REL1 INST1) INST2)->((REL2 INST2) INST1))) (((REL2 INST2) INST1)->((REL1 INST1) INST2))) (((((ax_001 REL2) REL1) x) INST1) INST2))) REL2) REL1) x0) lChris_THFTYPE_i)) REL2) REL1) x0) lCorina_THFTYPE_i)) wife_THFTYPE_IiioI) husband_THFTYPE_IiioI) ax) ax_002)) % % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p % EOF %------------------------------------------------------------------------------