%------------------------------------------------------------------------------ % File : cocATP---0.2.0 % Problem : CSR136^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 : n106.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:04 EDT 2014 % Result : Theorem 0.54s % Output : Proof 0.54s % Verified : % SZS Type : None (Parsing solution fails) % Syntax : Number of formulae : 0 % Comments : %------------------------------------------------------------------------------ %----ERROR: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % % Problem : CSR136^1 : TPTP v6.1.0. Released v4.1.0. % % Command : python CASC.py /export/starexec/sandbox/benchmark/theBenchmark.p % % Computer : n106.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:01 CDT 2014 % % CPUTime : 0.54 % 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 0x23f70e0>, <kernel.Type object at 0x23f7488>) of role type named numbers % Using role type % Declaring num:Type % FOF formula (<kernel.Constant object at 0x23f75f0>, <kernel.Constant object at 0x23f7248>) of role type named lAnna_THFTYPE_i % Using role type % Declaring lAnna_THFTYPE_i:fofType % FOF formula (<kernel.Constant object at 0x20ef6c8>, <kernel.Single object at 0x23f7368>) of role type named lBen_THFTYPE_i % Using role type % Declaring lBen_THFTYPE_i:fofType % FOF formula (<kernel.Constant object at 0x23f70e0>, <kernel.Single object at 0x23f73b0>) of role type named lBill_THFTYPE_i % Using role type % Declaring lBill_THFTYPE_i:fofType % FOF formula (<kernel.Constant object at 0x23f75f0>, <kernel.Single object at 0x23f7488>) of role type named lBob_THFTYPE_i % Using role type % Declaring lBob_THFTYPE_i:fofType % FOF formula (<kernel.Constant object at 0x23f7128>, <kernel.Single object at 0x23f71b8>) of role type named lMary_THFTYPE_i % Using role type % Declaring lMary_THFTYPE_i:fofType % FOF formula (<kernel.Constant object at 0x23f70e0>, <kernel.Single object at 0x23f7128>) of role type named lSue_THFTYPE_i % Using role type % Declaring lSue_THFTYPE_i:fofType % FOF formula (<kernel.Constant object at 0x23f4cb0>, <kernel.DependentProduct object at 0x2417a28>) of role type named likes_THFTYPE_IiioI % Using role type % Declaring likes_THFTYPE_IiioI:(fofType->(fofType->Prop)) % FOF formula (<kernel.Constant object at 0x23f7488>, <kernel.DependentProduct object at 0x2417a28>) of role type named parent_THFTYPE_IiioI % Using role type % Declaring parent_THFTYPE_IiioI:(fofType->(fofType->Prop)) % FOF formula ((likes_THFTYPE_IiioI lSue_THFTYPE_i) lBill_THFTYPE_i) of role axiom named ax % A new axiom: ((likes_THFTYPE_IiioI lSue_THFTYPE_i) lBill_THFTYPE_i) % FOF formula (not ((likes_THFTYPE_IiioI lSue_THFTYPE_i) lMary_THFTYPE_i)) of role axiom named ax_001 % A new axiom: (not ((likes_THFTYPE_IiioI lSue_THFTYPE_i) lMary_THFTYPE_i)) % FOF formula ((likes_THFTYPE_IiioI lMary_THFTYPE_i) lBill_THFTYPE_i) of role axiom named ax_002 % A new axiom: ((likes_THFTYPE_IiioI lMary_THFTYPE_i) lBill_THFTYPE_i) % FOF formula ((parent_THFTYPE_IiioI lMary_THFTYPE_i) lBen_THFTYPE_i) of role axiom named ax_003 % A new axiom: ((parent_THFTYPE_IiioI lMary_THFTYPE_i) lBen_THFTYPE_i) % FOF formula ((parent_THFTYPE_IiioI lSue_THFTYPE_i) lBen_THFTYPE_i) of role axiom named ax_004 % A new axiom: ((parent_THFTYPE_IiioI lSue_THFTYPE_i) lBen_THFTYPE_i) % FOF formula ((likes_THFTYPE_IiioI lBob_THFTYPE_i) lBill_THFTYPE_i) of role axiom named ax_005 % A new axiom: ((likes_THFTYPE_IiioI lBob_THFTYPE_i) lBill_THFTYPE_i) % FOF formula ((parent_THFTYPE_IiioI lSue_THFTYPE_i) lAnna_THFTYPE_i) of role axiom named ax_006 % A new axiom: ((parent_THFTYPE_IiioI lSue_THFTYPE_i) lAnna_THFTYPE_i) % FOF formula ((parent_THFTYPE_IiioI lMary_THFTYPE_i) lAnna_THFTYPE_i) of role axiom named ax_007 % A new axiom: ((parent_THFTYPE_IiioI lMary_THFTYPE_i) lAnna_THFTYPE_i) % FOF formula ((ex (fofType->(fofType->Prop))) (fun (R:(fofType->(fofType->Prop)))=> ((and ((and ((R lSue_THFTYPE_i) lBill_THFTYPE_i)) ((R lMary_THFTYPE_i) lBill_THFTYPE_i))) (not (forall (A:fofType) (B:fofType), ((R A) B)))))) of role conjecture named con % Conjecture to prove = ((ex (fofType->(fofType->Prop))) (fun (R:(fofType->(fofType->Prop)))=> ((and ((and ((R lSue_THFTYPE_i) lBill_THFTYPE_i)) ((R lMary_THFTYPE_i) lBill_THFTYPE_i))) (not (forall (A:fofType) (B:fofType), ((R A) B)))))):Prop % Parameter num_DUMMY:num. % We need to prove ['((ex (fofType->(fofType->Prop))) (fun (R:(fofType->(fofType->Prop)))=> ((and ((and ((R lSue_THFTYPE_i) lBill_THFTYPE_i)) ((R lMary_THFTYPE_i) lBill_THFTYPE_i))) (not (forall (A:fofType) (B:fofType), ((R A) B))))))'] % Parameter num:Type. % Parameter fofType:Type. % Parameter lAnna_THFTYPE_i:fofType. % Parameter lBen_THFTYPE_i:fofType. % Parameter lBill_THFTYPE_i:fofType. % Parameter lBob_THFTYPE_i:fofType. % Parameter lMary_THFTYPE_i:fofType. % Parameter lSue_THFTYPE_i:fofType. % Parameter likes_THFTYPE_IiioI:(fofType->(fofType->Prop)). % Parameter parent_THFTYPE_IiioI:(fofType->(fofType->Prop)). % Axiom ax:((likes_THFTYPE_IiioI lSue_THFTYPE_i) lBill_THFTYPE_i). % Axiom ax_001:(not ((likes_THFTYPE_IiioI lSue_THFTYPE_i) lMary_THFTYPE_i)). % Axiom ax_002:((likes_THFTYPE_IiioI lMary_THFTYPE_i) lBill_THFTYPE_i). % Axiom ax_003:((parent_THFTYPE_IiioI lMary_THFTYPE_i) lBen_THFTYPE_i). % Axiom ax_004:((parent_THFTYPE_IiioI lSue_THFTYPE_i) lBen_THFTYPE_i). % Axiom ax_005:((likes_THFTYPE_IiioI lBob_THFTYPE_i) lBill_THFTYPE_i). % Axiom ax_006:((parent_THFTYPE_IiioI lSue_THFTYPE_i) lAnna_THFTYPE_i). % Axiom ax_007:((parent_THFTYPE_IiioI lMary_THFTYPE_i) lAnna_THFTYPE_i). % Trying to prove ((ex (fofType->(fofType->Prop))) (fun (R:(fofType->(fofType->Prop)))=> ((and ((and ((R lSue_THFTYPE_i) lBill_THFTYPE_i)) ((R lMary_THFTYPE_i) lBill_THFTYPE_i))) (not (forall (A:fofType) (B:fofType), ((R A) B)))))) % Found x000:=(x00 lMary_THFTYPE_i):((x lSue_THFTYPE_i) lMary_THFTYPE_i) % Found (x00 lMary_THFTYPE_i) as proof of ((likes_THFTYPE_IiioI lSue_THFTYPE_i) lMary_THFTYPE_i) % Found ((x0 lSue_THFTYPE_i) lMary_THFTYPE_i) as proof of ((likes_THFTYPE_IiioI lSue_THFTYPE_i) lMary_THFTYPE_i) % Found ((x0 lSue_THFTYPE_i) lMary_THFTYPE_i) as proof of ((likes_THFTYPE_IiioI lSue_THFTYPE_i) lMary_THFTYPE_i) % Found ((x0 lSue_THFTYPE_i) lMary_THFTYPE_i) as proof of ((likes_THFTYPE_IiioI lSue_THFTYPE_i) lMary_THFTYPE_i) % Found (ax_001 ((x0 lSue_THFTYPE_i) lMary_THFTYPE_i)) as proof of False % Found (fun (x0:(forall (A:fofType) (B:fofType), ((x A) B)))=> (ax_001 ((x0 lSue_THFTYPE_i) lMary_THFTYPE_i))) as proof of False % Found (fun (x0:(forall (A:fofType) (B:fofType), ((x A) B)))=> (ax_001 ((x0 lSue_THFTYPE_i) lMary_THFTYPE_i))) as proof of (not (forall (A:fofType) (B:fofType), ((x A) B))) % Found conj1000:=(conj100 ax_002):((and ((x lSue_THFTYPE_i) lBill_THFTYPE_i)) ((x lMary_THFTYPE_i) lBill_THFTYPE_i)) % Found (conj100 ax_002) as proof of ((and ((x lSue_THFTYPE_i) lBill_THFTYPE_i)) ((x lMary_THFTYPE_i) lBill_THFTYPE_i)) % Found ((conj10 ((x lMary_THFTYPE_i) lBill_THFTYPE_i)) ax_002) as proof of ((and ((x lSue_THFTYPE_i) lBill_THFTYPE_i)) ((x lMary_THFTYPE_i) lBill_THFTYPE_i)) % Found (((fun (B:Prop)=> ((conj1 B) ax)) ((x lMary_THFTYPE_i) lBill_THFTYPE_i)) ax_002) as proof of ((and ((x lSue_THFTYPE_i) lBill_THFTYPE_i)) ((x lMary_THFTYPE_i) lBill_THFTYPE_i)) % Found (((fun (B:Prop)=> (((conj ((x lSue_THFTYPE_i) lBill_THFTYPE_i)) B) ax)) ((x lMary_THFTYPE_i) lBill_THFTYPE_i)) ax_002) as proof of ((and ((x lSue_THFTYPE_i) lBill_THFTYPE_i)) ((x lMary_THFTYPE_i) lBill_THFTYPE_i)) % Found (((fun (B:Prop)=> (((conj ((x lSue_THFTYPE_i) lBill_THFTYPE_i)) B) ax)) ((x lMary_THFTYPE_i) lBill_THFTYPE_i)) ax_002) as proof of ((and ((x lSue_THFTYPE_i) lBill_THFTYPE_i)) ((x lMary_THFTYPE_i) lBill_THFTYPE_i)) % Found ((conj00 (((fun (B:Prop)=> (((conj ((x lSue_THFTYPE_i) lBill_THFTYPE_i)) B) ax)) ((x lMary_THFTYPE_i) lBill_THFTYPE_i)) ax_002)) (fun (x0:(forall (A:fofType) (B:fofType), ((x A) B)))=> (ax_001 ((x0 lSue_THFTYPE_i) lMary_THFTYPE_i)))) as proof of ((and ((and ((x lSue_THFTYPE_i) lBill_THFTYPE_i)) ((x lMary_THFTYPE_i) lBill_THFTYPE_i))) (not (forall (A:fofType) (B:fofType), ((x A) B)))) % Found (((conj0 (not (forall (A:fofType) (B:fofType), ((x A) B)))) (((fun (B:Prop)=> (((conj ((x lSue_THFTYPE_i) lBill_THFTYPE_i)) B) ax)) ((x lMary_THFTYPE_i) lBill_THFTYPE_i)) ax_002)) (fun (x0:(forall (A:fofType) (B:fofType), ((x A) B)))=> (ax_001 ((x0 lSue_THFTYPE_i) lMary_THFTYPE_i)))) as proof of ((and ((and ((x lSue_THFTYPE_i) lBill_THFTYPE_i)) ((x lMary_THFTYPE_i) lBill_THFTYPE_i))) (not (forall (A:fofType) (B:fofType), ((x A) B)))) % Found ((((conj ((and ((x lSue_THFTYPE_i) lBill_THFTYPE_i)) ((x lMary_THFTYPE_i) lBill_THFTYPE_i))) (not (forall (A:fofType) (B:fofType), ((x A) B)))) (((fun (B:Prop)=> (((conj ((x lSue_THFTYPE_i) lBill_THFTYPE_i)) B) ax)) ((x lMary_THFTYPE_i) lBill_THFTYPE_i)) ax_002)) (fun (x0:(forall (A:fofType) (B:fofType), ((x A) B)))=> (ax_001 ((x0 lSue_THFTYPE_i) lMary_THFTYPE_i)))) as proof of ((and ((and ((x lSue_THFTYPE_i) lBill_THFTYPE_i)) ((x lMary_THFTYPE_i) lBill_THFTYPE_i))) (not (forall (A:fofType) (B:fofType), ((x A) B)))) % Found ((((conj ((and ((x lSue_THFTYPE_i) lBill_THFTYPE_i)) ((x lMary_THFTYPE_i) lBill_THFTYPE_i))) (not (forall (A:fofType) (B:fofType), ((x A) B)))) (((fun (B:Prop)=> (((conj ((x lSue_THFTYPE_i) lBill_THFTYPE_i)) B) ax)) ((x lMary_THFTYPE_i) lBill_THFTYPE_i)) ax_002)) (fun (x0:(forall (A:fofType) (B:fofType), ((x A) B)))=> (ax_001 ((x0 lSue_THFTYPE_i) lMary_THFTYPE_i)))) as proof of ((and ((and ((x lSue_THFTYPE_i) lBill_THFTYPE_i)) ((x lMary_THFTYPE_i) lBill_THFTYPE_i))) (not (forall (A:fofType) (B:fofType), ((x A) B)))) % Found (ex_intro000 ((((conj ((and ((x lSue_THFTYPE_i) lBill_THFTYPE_i)) ((x lMary_THFTYPE_i) lBill_THFTYPE_i))) (not (forall (A:fofType) (B:fofType), ((x A) B)))) (((fun (B:Prop)=> (((conj ((x lSue_THFTYPE_i) lBill_THFTYPE_i)) B) ax)) ((x lMary_THFTYPE_i) lBill_THFTYPE_i)) ax_002)) (fun (x0:(forall (A:fofType) (B:fofType), ((x A) B)))=> (ax_001 ((x0 lSue_THFTYPE_i) lMary_THFTYPE_i))))) as proof of ((ex (fofType->(fofType->Prop))) (fun (R:(fofType->(fofType->Prop)))=> ((and ((and ((R lSue_THFTYPE_i) lBill_THFTYPE_i)) ((R lMary_THFTYPE_i) lBill_THFTYPE_i))) (not (forall (A:fofType) (B:fofType), ((R A) B)))))) % Found ((ex_intro00 likes_THFTYPE_IiioI) ((((conj ((and ((likes_THFTYPE_IiioI lSue_THFTYPE_i) lBill_THFTYPE_i)) ((likes_THFTYPE_IiioI lMary_THFTYPE_i) lBill_THFTYPE_i))) (not (forall (A:fofType) (B:fofType), ((likes_THFTYPE_IiioI A) B)))) (((fun (B:Prop)=> (((conj ((likes_THFTYPE_IiioI lSue_THFTYPE_i) lBill_THFTYPE_i)) B) ax)) ((likes_THFTYPE_IiioI lMary_THFTYPE_i) lBill_THFTYPE_i)) ax_002)) (fun (x0:(forall (A:fofType) (B:fofType), ((likes_THFTYPE_IiioI A) B)))=> (ax_001 ((x0 lSue_THFTYPE_i) lMary_THFTYPE_i))))) as proof of ((ex (fofType->(fofType->Prop))) (fun (R:(fofType->(fofType->Prop)))=> ((and ((and ((R lSue_THFTYPE_i) lBill_THFTYPE_i)) ((R lMary_THFTYPE_i) lBill_THFTYPE_i))) (not (forall (A:fofType) (B:fofType), ((R A) B)))))) % Found (((ex_intro0 (fun (R:(fofType->(fofType->Prop)))=> ((and ((and ((R lSue_THFTYPE_i) lBill_THFTYPE_i)) ((R lMary_THFTYPE_i) lBill_THFTYPE_i))) (not (forall (A:fofType) (B:fofType), ((R A) B)))))) likes_THFTYPE_IiioI) ((((conj ((and ((likes_THFTYPE_IiioI lSue_THFTYPE_i) lBill_THFTYPE_i)) ((likes_THFTYPE_IiioI lMary_THFTYPE_i) lBill_THFTYPE_i))) (not (forall (A:fofType) (B:fofType), ((likes_THFTYPE_IiioI A) B)))) (((fun (B:Prop)=> (((conj ((likes_THFTYPE_IiioI lSue_THFTYPE_i) lBill_THFTYPE_i)) B) ax)) ((likes_THFTYPE_IiioI lMary_THFTYPE_i) lBill_THFTYPE_i)) ax_002)) (fun (x0:(forall (A:fofType) (B:fofType), ((likes_THFTYPE_IiioI A) B)))=> (ax_001 ((x0 lSue_THFTYPE_i) lMary_THFTYPE_i))))) as proof of ((ex (fofType->(fofType->Prop))) (fun (R:(fofType->(fofType->Prop)))=> ((and ((and ((R lSue_THFTYPE_i) lBill_THFTYPE_i)) ((R lMary_THFTYPE_i) lBill_THFTYPE_i))) (not (forall (A:fofType) (B:fofType), ((R A) B)))))) % Found ((((ex_intro (fofType->(fofType->Prop))) (fun (R:(fofType->(fofType->Prop)))=> ((and ((and ((R lSue_THFTYPE_i) lBill_THFTYPE_i)) ((R lMary_THFTYPE_i) lBill_THFTYPE_i))) (not (forall (A:fofType) (B:fofType), ((R A) B)))))) likes_THFTYPE_IiioI) ((((conj ((and ((likes_THFTYPE_IiioI lSue_THFTYPE_i) lBill_THFTYPE_i)) ((likes_THFTYPE_IiioI lMary_THFTYPE_i) lBill_THFTYPE_i))) (not (forall (A:fofType) (B:fofType), ((likes_THFTYPE_IiioI A) B)))) (((fun (B:Prop)=> (((conj ((likes_THFTYPE_IiioI lSue_THFTYPE_i) lBill_THFTYPE_i)) B) ax)) ((likes_THFTYPE_IiioI lMary_THFTYPE_i) lBill_THFTYPE_i)) ax_002)) (fun (x0:(forall (A:fofType) (B:fofType), ((likes_THFTYPE_IiioI A) B)))=> (ax_001 ((x0 lSue_THFTYPE_i) lMary_THFTYPE_i))))) as proof of ((ex (fofType->(fofType->Prop))) (fun (R:(fofType->(fofType->Prop)))=> ((and ((and ((R lSue_THFTYPE_i) lBill_THFTYPE_i)) ((R lMary_THFTYPE_i) lBill_THFTYPE_i))) (not (forall (A:fofType) (B:fofType), ((R A) B)))))) % Found ((((ex_intro (fofType->(fofType->Prop))) (fun (R:(fofType->(fofType->Prop)))=> ((and ((and ((R lSue_THFTYPE_i) lBill_THFTYPE_i)) ((R lMary_THFTYPE_i) lBill_THFTYPE_i))) (not (forall (A:fofType) (B:fofType), ((R A) B)))))) likes_THFTYPE_IiioI) ((((conj ((and ((likes_THFTYPE_IiioI lSue_THFTYPE_i) lBill_THFTYPE_i)) ((likes_THFTYPE_IiioI lMary_THFTYPE_i) lBill_THFTYPE_i))) (not (forall (A:fofType) (B:fofType), ((likes_THFTYPE_IiioI A) B)))) (((fun (B:Prop)=> (((conj ((likes_THFTYPE_IiioI lSue_THFTYPE_i) lBill_THFTYPE_i)) B) ax)) ((likes_THFTYPE_IiioI lMary_THFTYPE_i) lBill_THFTYPE_i)) ax_002)) (fun (x0:(forall (A:fofType) (B:fofType), ((likes_THFTYPE_IiioI A) B)))=> (ax_001 ((x0 lSue_THFTYPE_i) lMary_THFTYPE_i))))) as proof of ((ex (fofType->(fofType->Prop))) (fun (R:(fofType->(fofType->Prop)))=> ((and ((and ((R lSue_THFTYPE_i) lBill_THFTYPE_i)) ((R lMary_THFTYPE_i) lBill_THFTYPE_i))) (not (forall (A:fofType) (B:fofType), ((R A) B)))))) % Got proof ((((ex_intro (fofType->(fofType->Prop))) (fun (R:(fofType->(fofType->Prop)))=> ((and ((and ((R lSue_THFTYPE_i) lBill_THFTYPE_i)) ((R lMary_THFTYPE_i) lBill_THFTYPE_i))) (not (forall (A:fofType) (B:fofType), ((R A) B)))))) likes_THFTYPE_IiioI) ((((conj ((and ((likes_THFTYPE_IiioI lSue_THFTYPE_i) lBill_THFTYPE_i)) ((likes_THFTYPE_IiioI lMary_THFTYPE_i) lBill_THFTYPE_i))) (not (forall (A:fofType) (B:fofType), ((likes_THFTYPE_IiioI A) B)))) (((fun (B:Prop)=> (((conj ((likes_THFTYPE_IiioI lSue_THFTYPE_i) lBill_THFTYPE_i)) B) ax)) ((likes_THFTYPE_IiioI lMary_THFTYPE_i) lBill_THFTYPE_i)) ax_002)) (fun (x0:(forall (A:fofType) (B:fofType), ((likes_THFTYPE_IiioI A) B)))=> (ax_001 ((x0 lSue_THFTYPE_i) lMary_THFTYPE_i))))) % Time elapsed = 0.211911s % node=30 cost=511.000000 depth=13 % :::::::::::::::::::::: % % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p % ((((ex_intro (fofType->(fofType->Prop))) (fun (R:(fofType->(fofType->Prop)))=> ((and ((and ((R lSue_THFTYPE_i) lBill_THFTYPE_i)) ((R lMary_THFTYPE_i) lBill_THFTYPE_i))) (not (forall (A:fofType) (B:fofType), ((R A) B)))))) likes_THFTYPE_IiioI) ((((conj ((and ((likes_THFTYPE_IiioI lSue_THFTYPE_i) lBill_THFTYPE_i)) ((likes_THFTYPE_IiioI lMary_THFTYPE_i) lBill_THFTYPE_i))) (not (forall (A:fofType) (B:fofType), ((likes_THFTYPE_IiioI A) B)))) (((fun (B:Prop)=> (((conj ((likes_THFTYPE_IiioI lSue_THFTYPE_i) lBill_THFTYPE_i)) B) ax)) ((likes_THFTYPE_IiioI lMary_THFTYPE_i) lBill_THFTYPE_i)) ax_002)) (fun (x0:(forall (A:fofType) (B:fofType), ((likes_THFTYPE_IiioI A) B)))=> (ax_001 ((x0 lSue_THFTYPE_i) lMary_THFTYPE_i))))) % % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p % EOF %------------------------------------------------------------------------------