%------------------------------------------------------------------------------ % File : cocATP---0.2.0 % Problem : SYN000^1 : TPTP v7.1.0. Released v3.7.0. % Transfm : none % Format : tptp:raw % Command : python CASC.py /export/starexec/sandbox/benchmark/theBenchmark.p % Computer : n120.star.cs.uiowa.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2609 0 2.40GHz % Memory : 32218.625MB % OS : Linux 3.10.0-693.2.2.el7.x86_64 % CPULimit : 300s % DateTime : Fri Jun 1 07:57:43 EDT 2018 % Result : Theorem 0.39s % Output : Proof 0.39s % Verified : % SZS Type : None (Parsing solution fails) % Syntax : Number of formulae : 0 % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SYN000^1 : TPTP v7.1.0. Released v3.7.0. % 0.00/0.04 % Command : python CASC.py /export/starexec/sandbox/benchmark/theBenchmark.p % 0.03/0.23 % Computer : n120.star.cs.uiowa.edu % 0.03/0.23 % Model : x86_64 x86_64 % 0.03/0.23 % CPU : Intel(R) Xeon(R) CPU E5-2609 0 @ 2.40GHz % 0.03/0.23 % Memory : 32218.625MB % 0.03/0.23 % OS : Linux 3.10.0-693.2.2.el7.x86_64 % 0.03/0.23 % CPULimit : 300 % 0.03/0.23 % DateTime : Fri Jun 1 00:57:28 CDT 2018 % 0.03/0.23 % CPUTime: % 0.08/0.43 Python 2.7.13 % 0.33/0.92 Using paths ['/home/cristobal/cocATP/CASC/TPTP/', '/export/starexec/sandbox/benchmark/', '/export/starexec/sandbox/benchmark/'] % 0.33/0.92 FOF formula (<kernel.Constant object at 0x2ab648db4098>, <kernel.Sort object at 0x2ab6415195f0>) of role type named p0_type % 0.33/0.92 Using role type % 0.33/0.92 Declaring p0:Prop % 0.33/0.92 FOF formula (<kernel.Constant object at 0x2ab648db46c8>, <kernel.Sort object at 0x2ab6415195f0>) of role type named q0_type % 0.33/0.92 Using role type % 0.33/0.92 Declaring q0:Prop % 0.33/0.92 FOF formula (<kernel.Constant object at 0x2ab648db4a70>, <kernel.Sort object at 0x2ab6415195f0>) of role type named r0_type % 0.33/0.92 Using role type % 0.33/0.92 Declaring r0:Prop % 0.33/0.92 FOF formula (<kernel.Constant object at 0x2ab648db4710>, <kernel.Sort object at 0x2ab6415195f0>) of role type named s0_type % 0.33/0.92 Using role type % 0.33/0.92 Declaring s0:Prop % 0.33/0.92 FOF formula (((and p0) (q0->False))->((or r0) (s0->False))) of role axiom named propositional % 0.33/0.92 A new axiom: (((and p0) (q0->False))->((or r0) (s0->False))) % 0.33/0.92 FOF formula (<kernel.Constant object at 0x2ab648db4368>, <kernel.Constant object at 0x2ab648db44d0>) of role type named a_type % 0.33/0.92 Using role type % 0.33/0.92 Declaring a:fofType % 0.33/0.92 FOF formula (<kernel.Constant object at 0x2ab648db4998>, <kernel.Single object at 0x2ab648db4a70>) of role type named b_type % 0.33/0.92 Using role type % 0.33/0.92 Declaring b:fofType % 0.33/0.92 FOF formula (<kernel.Constant object at 0x2ab648db47e8>, <kernel.Single object at 0x2ab648db4710>) of role type named h_type % 0.33/0.92 Using role type % 0.33/0.92 Declaring h:fofType % 0.33/0.92 FOF formula (<kernel.Constant object at 0x2ab648db4368>, <kernel.DependentProduct object at 0x2ab64988cc20>) of role type named f_type % 0.33/0.92 Using role type % 0.33/0.92 Declaring f:(fofType->fofType) % 0.33/0.92 FOF formula (<kernel.Constant object at 0x2ab648db47e8>, <kernel.DependentProduct object at 0x2ab64988cc20>) of role type named g_type % 0.33/0.92 Using role type % 0.33/0.92 Declaring g:(fofType->(fofType->(fofType->fofType))) % 0.33/0.92 FOF formula (<kernel.Constant object at 0x2ab648db4368>, <kernel.DependentProduct object at 0x2ab64988c170>) of role type named p_type % 0.33/0.92 Using role type % 0.33/0.92 Declaring p:(fofType->Prop) % 0.33/0.92 FOF formula (<kernel.Constant object at 0x2ab648db4710>, <kernel.DependentProduct object at 0x2ab64988c0e0>) of role type named q_type % 0.33/0.92 Using role type % 0.33/0.92 Declaring q:(fofType->(fofType->Prop)) % 0.33/0.92 FOF formula (<kernel.Constant object at 0x2ab648db4368>, <kernel.DependentProduct object at 0x2ab64988c830>) of role type named r_type % 0.33/0.92 Using role type % 0.33/0.92 Declaring r:(fofType->(fofType->(fofType->Prop))) % 0.33/0.92 FOF formula (<kernel.Constant object at 0x2ab648db4368>, <kernel.DependentProduct object at 0x2ab64988c170>) of role type named s_type % 0.33/0.92 Using role type % 0.33/0.92 Declaring s:(fofType->Prop) % 0.33/0.92 FOF formula (forall (X:fofType), (((or (p X)) (((q X) a)->False))->((ex fofType) (fun (Y:fofType)=> ((ex fofType) (fun (Z:fofType)=> ((and (((r X) (f Y)) (((g X) (f Y)) Z))) ((s (f (f (f b))))->False)))))))) of role axiom named first_order % 0.33/0.92 A new axiom: (forall (X:fofType), (((or (p X)) (((q X) a)->False))->((ex fofType) (fun (Y:fofType)=> ((ex fofType) (fun (Z:fofType)=> ((and (((r X) (f Y)) (((g X) (f Y)) Z))) ((s (f (f (f b))))->False)))))))) % 0.33/0.92 FOF formula ((ex fofType) (fun (Y:fofType)=> (forall (X:fofType) (Z:fofType), ((or ((or (((eq fofType) (f Y)) (((g X) (f Y)) Z))) (not (((eq fofType) (f (f (f b)))) a)))) (((eq fofType) X) (f Y)))))) of role axiom named equality % 0.33/0.92 A new axiom: ((ex fofType) (fun (Y:fofType)=> (forall (X:fofType) (Z:fofType), ((or ((or (((eq fofType) (f Y)) (((g X) (f Y)) Z))) (not (((eq fofType) (f (f (f b)))) a)))) (((eq fofType) X) (f Y)))))) % 0.33/0.92 FOF formula ((or True) False) of role axiom named true_false % 0.33/0.92 A new axiom: ((or True) False) % 0.33/0.92 FOF formula (<kernel.Constant object at 0x2ab64988c830>, <kernel.Sort object at 0x2ab6415195f0>) of role type named quoted_proposition_type % 0.33/0.92 Using role type % 0.33/0.92 Declaring A proposition:Prop % 0.33/0.92 FOF formula (<kernel.Constant object at 0x2ab64988cd40>, <kernel.DependentProduct object at 0x2ab64988c560>) of role type named quoted_predicate_type % 0.33/0.92 Using role type % 0.33/0.92 Declaring A predicate:(fofType->Prop) % 0.33/0.92 FOF formula (<kernel.Constant object at 0x2ab64988ccf8>, <kernel.Single object at 0x2ab64988c758>) of role type named quoted_constant_type % 0.33/0.92 Using role type % 0.33/0.92 Declaring A constant:fofType % 0.33/0.92 FOF formula (<kernel.Constant object at 0x2ab64988c830>, <kernel.DependentProduct object at 0x2ab64988c128>) of role type named quoted_function_type % 0.33/0.96 Using role type % 0.33/0.96 Declaring A function:(fofType->fofType) % 0.33/0.96 FOF formula (<kernel.Constant object at 0x2ab64988c9e0>, <kernel.Single object at 0x2ab64988c758>) of role type named quoted_escape_type % 0.33/0.96 Using role type % 0.33/0.96 Declaring A \'quoted \\ escape\':fofType % 0.33/0.96 FOF formula ((or ((or ((or ((or A proposition) (A predicate a))) (p A constant))) (p (A function a)))) (p A \'quoted \\ escape\')) of role axiom named single_quoted % 0.33/0.96 A new axiom: ((or ((or ((or ((or A proposition) (A predicate a))) (p A constant))) (p (A function a)))) (p A \'quoted \\ escape\')) % 0.33/0.96 FOF formula (forall (X:fofType), ((iff ((((q X) a)->False)->(p X))) ((ex fofType) (fun (Y:fofType)=> ((ex fofType) (fun (Z:fofType)=> (not ((iff (((r X) (f Y)) (((g X) (f Y)) Z))) ((s (f (f (f b))))->False))))))))) of role axiom named useful_connectives % 0.33/0.96 A new axiom: (forall (X:fofType), ((iff ((((q X) a)->False)->(p X))) ((ex fofType) (fun (Y:fofType)=> ((ex fofType) (fun (Z:fofType)=> (not ((iff (((r X) (f Y)) (((g X) (f Y)) Z))) ((s (f (f (f b))))->False))))))))) % 0.33/0.96 FOF formula (<kernel.Constant object at 0x2ab648d86e60>, <kernel.DependentProduct object at 0x2ab64988c248>) of role type named l1_type % 0.33/0.96 Using role type % 0.33/0.96 Declaring l1:(fofType->((fofType->Prop)->Prop)) % 0.33/0.96 FOF formula (<kernel.Constant object at 0x2ab648d86e18>, <kernel.DependentProduct object at 0x2ab64988c248>) of role type named l2_type % 0.33/0.96 Using role type % 0.33/0.96 Declaring l2:((fofType->((fofType->fofType)->fofType))->Prop) % 0.33/0.96 FOF formula (((eq (fofType->((fofType->Prop)->Prop))) l1) (fun (C:fofType) (P:(fofType->Prop))=> (P C))) of role axiom named lambda_defn % 0.33/0.96 A new axiom: (((eq (fofType->((fofType->Prop)->Prop))) l1) (fun (C:fofType) (P:(fofType->Prop))=> (P C))) % 0.33/0.96 FOF formula (l2 (fun (C:fofType) (F:(fofType->fofType))=> (F C))) of role axiom named lambda_use % 0.33/0.96 A new axiom: (l2 (fun (C:fofType) (F:(fofType->fofType))=> (F C))) % 0.33/0.96 FOF formula (<kernel.Constant object at 0x2ab64988c758>, <kernel.Type object at 0x2ab64988c1b8>) of role type named new_type % 0.33/0.96 Using role type % 0.33/0.96 Declaring new:Type % 0.33/0.96 FOF formula (<kernel.Constant object at 0x2ab64988c830>, <kernel.Constant object at 0x2ab64988c518>) of role type named newc_type % 0.33/0.96 Using role type % 0.33/0.96 Declaring newc:new % 0.33/0.96 FOF formula (<kernel.Constant object at 0x2ab64988cc20>, <kernel.DependentProduct object at 0x2ab64988c758>) of role type named newf_type % 0.33/0.96 Using role type % 0.33/0.96 Declaring newf:(new->(fofType->new)) % 0.33/0.96 FOF formula (<kernel.Constant object at 0x2ab64988cef0>, <kernel.DependentProduct object at 0x2ab64988c830>) of role type named newp_type % 0.33/0.96 Using role type % 0.33/0.96 Declaring newp:(new->(fofType->Prop)) % 0.33/0.96 FOF formula (new->((newp ((newf newc) a)) a)) of role axiom named new_axiom % 0.33/0.96 A new axiom: (new->((newp ((newf newc) a)) a)) % 0.33/0.96 FOF formula (forall (X:fofType), (((or (p X)) (((q X) a)->False))->((ex fofType) (fun (Y:fofType)=> ((ex fofType) (fun (Z:fofType)=> ((and (((r X) (f Y)) (((g X) (f Y)) Z))) ((s (f (f (f b))))->False)))))))) of role axiom named 123 % 0.33/0.96 A new axiom: (forall (X:fofType), (((or (p X)) (((q X) a)->False))->((ex fofType) (fun (Y:fofType)=> ((ex fofType) (fun (Z:fofType)=> ((and (((r X) (f Y)) (((g X) (f Y)) Z))) ((s (f (f (f b))))->False)))))))) % 0.33/0.96 FOF formula (p h) of role hypothesis named role_hypothesis % 0.33/0.96 A new axiom: (p h) % 0.33/0.96 FOF formula ((ex fofType) (fun (X:fofType)=> (p X))) of role conjecture named role_conjecture % 0.33/0.96 Conjecture to prove = ((ex fofType) (fun (X:fofType)=> (p X))):Prop % 0.33/0.96 Failed to open /home/cristobal/cocATP/CASC/TPTP/Axioms/SYN000^0.ax, trying next directory % 0.33/0.96 FOF formula (<kernel.Constant object at 0x2ab648db0170>, <kernel.Sort object at 0x2ab6415195f0>) of role type named ia1_type % 0.33/0.96 Using role type % 0.33/0.96 Declaring ia1:Prop % 0.33/0.96 FOF formula (<kernel.Constant object at 0x2ab648db0878>, <kernel.Sort object at 0x2ab6415195f0>) of role type named ia2_type % 0.33/0.96 Using role type % 0.33/0.96 Declaring ia2:Prop % 0.33/0.96 FOF formula (<kernel.Constant object at 0x2ab648db0170>, <kernel.Sort object at 0x2ab6415195f0>) of role type named ia3_type % 0.33/0.96 Using role type % 0.33/0.96 Declaring ia3:Prop % 0.33/0.96 FOF formula ia1 of role axiom named ia1 % 0.33/0.96 A new axiom: ia1 % 0.39/1.01 FOF formula ia2 of role axiom named ia2 % 0.39/1.01 A new axiom: ia2 % 0.39/1.01 FOF formula ia3 of role axiom named ia3 % 0.39/1.01 A new axiom: ia3 % 0.39/1.01 We need to prove ['((ex fofType) (fun (X:fofType)=> (p X)))'] % 0.39/1.01 Parameter p0:Prop. % 0.39/1.01 Parameter q0:Prop. % 0.39/1.01 Parameter r0:Prop. % 0.39/1.01 Parameter s0:Prop. % 0.39/1.01 Axiom propositional:(((and p0) (q0->False))->((or r0) (s0->False))). % 0.39/1.01 Parameter fofType:Type. % 0.39/1.01 Parameter a:fofType. % 0.39/1.01 Parameter b:fofType. % 0.39/1.01 Parameter h:fofType. % 0.39/1.01 Parameter f:(fofType->fofType). % 0.39/1.01 Parameter g:(fofType->(fofType->(fofType->fofType))). % 0.39/1.01 Parameter p:(fofType->Prop). % 0.39/1.01 Parameter q:(fofType->(fofType->Prop)). % 0.39/1.01 Parameter r:(fofType->(fofType->(fofType->Prop))). % 0.39/1.01 Parameter s:(fofType->Prop). % 0.39/1.01 Axiom first_order:(forall (X:fofType), (((or (p X)) (((q X) a)->False))->((ex fofType) (fun (Y:fofType)=> ((ex fofType) (fun (Z:fofType)=> ((and (((r X) (f Y)) (((g X) (f Y)) Z))) ((s (f (f (f b))))->False)))))))). % 0.39/1.01 Axiom equality:((ex fofType) (fun (Y:fofType)=> (forall (X:fofType) (Z:fofType), ((or ((or (((eq fofType) (f Y)) (((g X) (f Y)) Z))) (not (((eq fofType) (f (f (f b)))) a)))) (((eq fofType) X) (f Y)))))). % 0.39/1.01 Axiom true_false:((or True) False). % 0.39/1.01 Parameter A proposition:Prop. % 0.39/1.01 Parameter A predicate:(fofType->Prop). % 0.39/1.01 Parameter A constant:fofType. % 0.39/1.01 Parameter A function:(fofType->fofType). % 0.39/1.01 Parameter A \'quoted \\ escape\':fofType. % 0.39/1.01 Axiom single_quoted:((or ((or ((or ((or A proposition) (A predicate a))) (p A constant))) (p (A function a)))) (p A \'quoted \\ escape\')). % 0.39/1.01 Axiom useful_connectives:(forall (X:fofType), ((iff ((((q X) a)->False)->(p X))) ((ex fofType) (fun (Y:fofType)=> ((ex fofType) (fun (Z:fofType)=> (not ((iff (((r X) (f Y)) (((g X) (f Y)) Z))) ((s (f (f (f b))))->False))))))))). % 0.39/1.01 Parameter l1:(fofType->((fofType->Prop)->Prop)). % 0.39/1.01 Parameter l2:((fofType->((fofType->fofType)->fofType))->Prop). % 0.39/1.01 Axiom lambda_defn:(((eq (fofType->((fofType->Prop)->Prop))) l1) (fun (C:fofType) (P:(fofType->Prop))=> (P C))). % 0.39/1.01 Axiom lambda_use:(l2 (fun (C:fofType) (F:(fofType->fofType))=> (F C))). % 0.39/1.01 Parameter new:Type. % 0.39/1.01 Parameter newc:new. % 0.39/1.01 Parameter newf:(new->(fofType->new)). % 0.39/1.01 Parameter newp:(new->(fofType->Prop)). % 0.39/1.01 Axiom new_axiom:(new->((newp ((newf newc) a)) a)). % 0.39/1.01 Axiom 123:(forall (X:fofType), (((or (p X)) (((q X) a)->False))->((ex fofType) (fun (Y:fofType)=> ((ex fofType) (fun (Z:fofType)=> ((and (((r X) (f Y)) (((g X) (f Y)) Z))) ((s (f (f (f b))))->False)))))))). % 0.39/1.01 Axiom role_hypothesis:(p h). % 0.39/1.01 Parameter ia1:Prop. % 0.39/1.01 Parameter ia2:Prop. % 0.39/1.01 Parameter ia3:Prop. % 0.39/1.01 Axiom ia1_TPTP_next:ia1. % 0.39/1.01 Axiom ia2_TPTP_next:ia2. % 0.39/1.01 Axiom ia3_TPTP_next:ia3. % 0.39/1.01 Trying to prove ((ex fofType) (fun (X:fofType)=> (p X))) % 0.39/1.01 Found role_hypothesis:(p h) % 0.39/1.01 Instantiate: x:=h:fofType % 0.39/1.01 Found role_hypothesis as proof of (p x) % 0.39/1.01 Found (ex_intro000 role_hypothesis) as proof of ((ex fofType) (fun (X:fofType)=> (p X))) % 0.39/1.01 Found ((ex_intro00 h) role_hypothesis) as proof of ((ex fofType) (fun (X:fofType)=> (p X))) % 0.39/1.01 Found (((ex_intro0 (fun (X:fofType)=> (p X))) h) role_hypothesis) as proof of ((ex fofType) (fun (X:fofType)=> (p X))) % 0.39/1.01 Found ((((ex_intro fofType) (fun (X:fofType)=> (p X))) h) role_hypothesis) as proof of ((ex fofType) (fun (X:fofType)=> (p X))) % 0.39/1.01 Found ((((ex_intro fofType) (fun (X:fofType)=> (p X))) h) role_hypothesis) as proof of ((ex fofType) (fun (X:fofType)=> (p X))) % 0.39/1.01 Got proof ((((ex_intro fofType) (fun (X:fofType)=> (p X))) h) role_hypothesis) % 0.39/1.01 Time elapsed = 0.042980s % 0.39/1.01 node=8 cost=209.000000 depth=5 % 0.39/1.01:::::::::::::::::::::: % 0.39/1.01 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 0.39/1.01 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p % 0.39/1.01 ((((ex_intro fofType) (fun (X:fofType)=> (p X))) h) role_hypothesis) % 0.39/1.01 % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p %------------------------------------------------------------------------------