%------------------------------------------------------------------------------ % File : cocATP---0.2.0 % Problem : NUM636^3 : TPTP v7.0.0. Released v3.7.0. % Transfm : none % Format : tptp:raw % Command : python CASC.py /export/starexec/sandbox2/benchmark/theBenchmark.p % Computer : n131.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 : Mon Jan 8 13:11:14 EST 2018 % Result : Theorem 1.57s % Output : Proof 1.57s % 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 : NUM636^3 : TPTP v7.0.0. Released v3.7.0. % 0.00/0.03 % Command : python CASC.py /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.02/0.23 % Computer : n131.star.cs.uiowa.edu % 0.02/0.23 % Model : x86_64 x86_64 % 0.02/0.23 % CPU : Intel(R) Xeon(R) CPU E5-2609 0 @ 2.40GHz % 0.02/0.23 % Memory : 32218.625MB % 0.02/0.23 % OS : Linux 3.10.0-693.2.2.el7.x86_64 % 0.02/0.23 % CPULimit : 300 % 0.02/0.23 % DateTime : Fri Jan 5 11:15:59 CST 2018 % 0.02/0.23 % CPUTime : % 0.08/0.27 Python 2.7.13 % 1.50/1.97 Using paths ['/home/cristobal/cocATP/CASC/TPTP/', '/export/starexec/sandbox2/benchmark/', '/export/starexec/sandbox2/benchmark/'] % 1.50/1.97 FOF formula (<kernel.Constant object at 0x2b151da4e998>, <kernel.Constant object at 0x2b151da4eea8>) of role type named one_type % 1.50/1.97 Using role type % 1.50/1.97 Declaring one:fofType % 1.50/1.97 FOF formula (<kernel.Constant object at 0x2b151da4ee18>, <kernel.DependentProduct object at 0x2b151d761dd0>) of role type named succ_type % 1.50/1.97 Using role type % 1.50/1.97 Declaring succ:(fofType->fofType) % 1.50/1.97 FOF formula (forall (X:fofType), (not (((eq fofType) (succ X)) one))) of role axiom named one_is_first % 1.50/1.97 A new axiom: (forall (X:fofType), (not (((eq fofType) (succ X)) one))) % 1.50/1.97 FOF formula (forall (X:fofType) (Y:fofType), ((((eq fofType) (succ X)) (succ Y))->(((eq fofType) X) Y))) of role axiom named succ_injective % 1.50/1.97 A new axiom: (forall (X:fofType) (Y:fofType), ((((eq fofType) (succ X)) (succ Y))->(((eq fofType) X) Y))) % 1.50/1.97 FOF formula (forall (M:(fofType->Prop)), (((and (M one)) (forall (X:fofType), ((M X)->(M (succ X)))))->(forall (Y:fofType), (M Y)))) of role axiom named induction % 1.50/1.97 A new axiom: (forall (M:(fofType->Prop)), (((and (M one)) (forall (X:fofType), ((M X)->(M (succ X)))))->(forall (Y:fofType), (M Y)))) % 1.50/1.97 FOF formula (<kernel.Constant object at 0x2b151da4ee18>, <kernel.DependentProduct object at 0x2b151d7617a0>) of role type named m_type % 1.50/1.97 Using role type % 1.50/1.97 Declaring m:(fofType->Prop) % 1.50/1.97 FOF formula (((eq (fofType->Prop)) m) (fun (E:fofType)=> (not (((eq fofType) (succ E)) E)))) of role definition named m_defn % 1.50/1.97 A new definition: (((eq (fofType->Prop)) m) (fun (E:fofType)=> (not (((eq fofType) (succ E)) E)))) % 1.50/1.97 Defined: m:=(fun (E:fofType)=> (not (((eq fofType) (succ E)) E))) % 1.50/1.97 FOF formula (m one) of role lemma named m_is_one % 1.50/1.97 A new axiom: (m one) % 1.50/1.97 FOF formula (forall (X:fofType), ((m X)->(m (succ X)))) of role lemma named m_is_next % 1.50/1.97 A new axiom: (forall (X:fofType), ((m X)->(m (succ X)))) % 1.50/1.97 FOF formula (forall (X:fofType), (m X)) of role conjecture named m_is_all % 1.50/1.97 Conjecture to prove = (forall (X:fofType), (m X)):Prop % 1.50/1.97 We need to prove ['(forall (X:fofType), (m X))'] % 1.50/1.97 Parameter fofType:Type. % 1.50/1.97 Parameter one:fofType. % 1.50/1.97 Parameter succ:(fofType->fofType). % 1.50/1.97 Axiom one_is_first:(forall (X:fofType), (not (((eq fofType) (succ X)) one))). % 1.50/1.97 Axiom succ_injective:(forall (X:fofType) (Y:fofType), ((((eq fofType) (succ X)) (succ Y))->(((eq fofType) X) Y))). % 1.50/1.97 Axiom induction:(forall (M:(fofType->Prop)), (((and (M one)) (forall (X:fofType), ((M X)->(M (succ X)))))->(forall (Y:fofType), (M Y)))). % 1.50/1.97 Definition m:=(fun (E:fofType)=> (not (((eq fofType) (succ E)) E))):(fofType->Prop). % 1.50/1.97 Axiom m_is_one:(m one). % 1.50/1.97 Axiom m_is_next:(forall (X:fofType), ((m X)->(m (succ X)))). % 1.50/1.97 Trying to prove (forall (X:fofType), (m X)) % 1.50/1.97 Found m_is_next:(forall (X:fofType), ((m X)->(m (succ X)))) % 1.50/1.97 Found m_is_next as proof of (forall (X:fofType), ((m X)->(m (succ X)))) % 1.50/1.97 Found (conj000 m_is_next) as proof of ((and (m one)) (forall (X:fofType), ((m X)->(m (succ X))))) % 1.50/1.97 Found ((conj00 (forall (X:fofType), ((m X)->(m (succ X))))) m_is_next) as proof of ((and (m one)) (forall (X:fofType), ((m X)->(m (succ X))))) % 1.50/1.97 Found (((fun (B:Prop)=> ((conj0 B) m_is_one)) (forall (X:fofType), ((m X)->(m (succ X))))) m_is_next) as proof of ((and (m one)) (forall (X:fofType), ((m X)->(m (succ X))))) % 1.50/1.97 Found (((fun (B:Prop)=> (((conj (m one)) B) m_is_one)) (forall (X:fofType), ((m X)->(m (succ X))))) m_is_next) as proof of ((and (m one)) (forall (X:fofType), ((m X)->(m (succ X))))) % 1.50/1.97 Found (((fun (B:Prop)=> (((conj (m one)) B) m_is_one)) (forall (X:fofType), ((m X)->(m (succ X))))) m_is_next) as proof of ((and (m one)) (forall (X:fofType), ((m X)->(m (succ X))))) % 1.50/1.97 Found (induction00 (((fun (B:Prop)=> (((conj (m one)) B) m_is_one)) (forall (X:fofType), ((m X)->(m (succ X))))) m_is_next)) as proof of (m X) % 1.50/1.97 Found ((induction0 m) (((fun (B:Prop)=> (((conj (m one)) B) m_is_one)) (forall (X:fofType), ((m X)->(m (succ X))))) m_is_next)) as proof of (m X) % 1.50/1.97 Found (((fun (M:(fofType->Prop)) (x:((and (M one)) (forall (X:fofType), ((M X)->(M (succ X))))))=> (((induction M) x) X)) m) (((fun (B:Prop)=> (((conj (m one)) B) m_is_one)) (forall (X0:fofType), ((m X0)->(m (succ X0))))) m_is_next)) as proof of (m X) % 1.57/1.99 Found (fun (X:fofType)=> (((fun (M:(fofType->Prop)) (x:((and (M one)) (forall (X:fofType), ((M X)->(M (succ X))))))=> (((induction M) x) X)) m) (((fun (B:Prop)=> (((conj (m one)) B) m_is_one)) (forall (X0:fofType), ((m X0)->(m (succ X0))))) m_is_next))) as proof of (m X) % 1.57/1.99 Found (fun (X:fofType)=> (((fun (M:(fofType->Prop)) (x:((and (M one)) (forall (X:fofType), ((M X)->(M (succ X))))))=> (((induction M) x) X)) m) (((fun (B:Prop)=> (((conj (m one)) B) m_is_one)) (forall (X0:fofType), ((m X0)->(m (succ X0))))) m_is_next))) as proof of (forall (X:fofType), (m X)) % 1.57/1.99 Got proof (fun (X:fofType)=> (((fun (M:(fofType->Prop)) (x:((and (M one)) (forall (X:fofType), ((M X)->(M (succ X))))))=> (((induction M) x) X)) m) (((fun (B:Prop)=> (((conj (m one)) B) m_is_one)) (forall (X0:fofType), ((m X0)->(m (succ X0))))) m_is_next))) % 1.57/1.99 Time elapsed = 1.200482s % 1.57/1.99 node=288 cost=197.000000 depth=10 % 1.57/1.99:::::::::::::::::::::: % 1.57/1.99 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 1.57/1.99 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p % 1.57/1.99 (fun (X:fofType)=> (((fun (M:(fofType->Prop)) (x:((and (M one)) (forall (X:fofType), ((M X)->(M (succ X))))))=> (((induction M) x) X)) m) (((fun (B:Prop)=> (((conj (m one)) B) m_is_one)) (forall (X0:fofType), ((m X0)->(m (succ X0))))) m_is_next))) % 1.57/1.99 % SZS output end Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p %------------------------------------------------------------------------------