%------------------------------------------------------------------------------ % File : cocATP---0.2.0 % Problem : NUM747^1 : TPTP v7.0.0. Released v3.7.0. % Transfm : none % Format : tptp:raw % Command : python CASC.py /export/starexec/sandbox2/benchmark/theBenchmark.p % Computer : n061.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:36 EST 2018 % Result : Theorem 0.08s % Output : Proof 0.08s % 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 : NUM747^1 : 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 : n061.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 13:35:48 CST 2018 % 0.02/0.23 % CPUTime : % 0.02/0.25 Python 2.7.13 % 0.08/0.58 Using paths ['/home/cristobal/cocATP/CASC/TPTP/', '/export/starexec/sandbox2/benchmark/', '/export/starexec/sandbox2/benchmark/'] % 0.08/0.58 FOF formula (<kernel.Constant object at 0x2b3bf9b80950>, <kernel.Type object at 0x2b3bf9b802d8>) of role type named nat_type % 0.08/0.58 Using role type % 0.08/0.58 Declaring nat:Type % 0.08/0.58 FOF formula (<kernel.Constant object at 0x2b3bf9b88ef0>, <kernel.Constant object at 0x2b3bf9b80fc8>) of role type named x1 % 0.08/0.58 Using role type % 0.08/0.58 Declaring x1:nat % 0.08/0.58 FOF formula (<kernel.Constant object at 0x2b3bf9b80b48>, <kernel.Constant object at 0x2b3bf9b80fc8>) of role type named x2 % 0.08/0.58 Using role type % 0.08/0.58 Declaring x2:nat % 0.08/0.58 FOF formula (<kernel.Constant object at 0x2b3bf9b80950>, <kernel.Constant object at 0x2b3bf9b80fc8>) of role type named n % 0.08/0.58 Using role type % 0.08/0.58 Declaring n:nat % 0.08/0.58 FOF formula (<kernel.Constant object at 0x2b3bf9b80e60>, <kernel.Type object at 0x2b3bf9b80b48>) of role type named frac_type % 0.08/0.58 Using role type % 0.08/0.58 Declaring frac:Type % 0.08/0.58 FOF formula (<kernel.Constant object at 0x2b3bf9b80908>, <kernel.DependentProduct object at 0x2b3bf9aa4fc8>) of role type named eq % 0.08/0.58 Using role type % 0.08/0.58 Declaring _TPTP_eq:(frac->(frac->Prop)) % 0.08/0.58 FOF formula (<kernel.Constant object at 0x2b3bf9b80950>, <kernel.DependentProduct object at 0x2b3bf9aa4e18>) of role type named fr % 0.08/0.58 Using role type % 0.08/0.58 Declaring fr:(nat->(nat->frac)) % 0.08/0.58 FOF formula (<kernel.Constant object at 0x2b3bf9b80e60>, <kernel.DependentProduct object at 0x2b3bf9aa4fc8>) of role type named pl % 0.08/0.58 Using role type % 0.08/0.58 Declaring pl:(nat->(nat->nat)) % 0.08/0.58 FOF formula (<kernel.Constant object at 0x2b3bf9b80950>, <kernel.DependentProduct object at 0x2b3bf9aa4fc8>) of role type named pf % 0.08/0.58 Using role type % 0.08/0.58 Declaring pf:(frac->(frac->frac)) % 0.08/0.58 FOF formula (forall (Xx:frac) (Xy:frac), (((_TPTP_eq Xx) Xy)->((_TPTP_eq Xy) Xx))) of role axiom named satz38 % 0.08/0.58 A new axiom: (forall (Xx:frac) (Xy:frac), (((_TPTP_eq Xx) Xy)->((_TPTP_eq Xy) Xx))) % 0.08/0.58 FOF formula (forall (Xx1:nat) (Xx2:nat) (Xn:nat), ((_TPTP_eq ((pf ((fr Xx1) Xn)) ((fr Xx2) Xn))) ((fr ((pl Xx1) Xx2)) Xn))) of role axiom named satz57 % 0.08/0.58 A new axiom: (forall (Xx1:nat) (Xx2:nat) (Xn:nat), ((_TPTP_eq ((pf ((fr Xx1) Xn)) ((fr Xx2) Xn))) ((fr ((pl Xx1) Xx2)) Xn))) % 0.08/0.58 FOF formula ((_TPTP_eq ((fr ((pl x1) x2)) n)) ((pf ((fr x1) n)) ((fr x2) n))) of role conjecture named satz57a % 0.08/0.58 Conjecture to prove = ((_TPTP_eq ((fr ((pl x1) x2)) n)) ((pf ((fr x1) n)) ((fr x2) n))):Prop % 0.08/0.58 Parameter frac_DUMMY:frac. % 0.08/0.58 We need to prove ['((_TPTP_eq ((fr ((pl x1) x2)) n)) ((pf ((fr x1) n)) ((fr x2) n)))'] % 0.08/0.58 Parameter nat:Type. % 0.08/0.58 Parameter x1:nat. % 0.08/0.58 Parameter x2:nat. % 0.08/0.58 Parameter n:nat. % 0.08/0.58 Parameter frac:Type. % 0.08/0.58 Parameter _TPTP_eq:(frac->(frac->Prop)). % 0.08/0.58 Parameter fr:(nat->(nat->frac)). % 0.08/0.58 Parameter pl:(nat->(nat->nat)). % 0.08/0.58 Parameter pf:(frac->(frac->frac)). % 0.08/0.58 Axiom satz38:(forall (Xx:frac) (Xy:frac), (((_TPTP_eq Xx) Xy)->((_TPTP_eq Xy) Xx))). % 0.08/0.58 Axiom satz57:(forall (Xx1:nat) (Xx2:nat) (Xn:nat), ((_TPTP_eq ((pf ((fr Xx1) Xn)) ((fr Xx2) Xn))) ((fr ((pl Xx1) Xx2)) Xn))). % 0.08/0.58 Trying to prove ((_TPTP_eq ((fr ((pl x1) x2)) n)) ((pf ((fr x1) n)) ((fr x2) n))) % 0.08/0.58 Found satz57000:=(satz5700 n):((_TPTP_eq ((pf ((fr x1) n)) ((fr x2) n))) ((fr ((pl x1) x2)) n)) % 0.08/0.58 Found (satz5700 n) as proof of ((_TPTP_eq ((pf ((fr x1) n)) ((fr x2) n))) ((fr ((pl x1) x2)) n)) % 0.08/0.58 Found ((satz570 x2) n) as proof of ((_TPTP_eq ((pf ((fr x1) n)) ((fr x2) n))) ((fr ((pl x1) x2)) n)) % 0.08/0.58 Found (((satz57 x1) x2) n) as proof of ((_TPTP_eq ((pf ((fr x1) n)) ((fr x2) n))) ((fr ((pl x1) x2)) n)) % 0.08/0.58 Found (((satz57 x1) x2) n) as proof of ((_TPTP_eq ((pf ((fr x1) n)) ((fr x2) n))) ((fr ((pl x1) x2)) n)) % 0.08/0.58 Found (satz3800 (((satz57 x1) x2) n)) as proof of ((_TPTP_eq ((fr ((pl x1) x2)) n)) ((pf ((fr x1) n)) ((fr x2) n))) % 0.08/0.58 Found ((satz380 ((fr ((pl x1) x2)) n)) (((satz57 x1) x2) n)) as proof of ((_TPTP_eq ((fr ((pl x1) x2)) n)) ((pf ((fr x1) n)) ((fr x2) n))) % 0.08/0.58 Found (((satz38 ((pf ((fr x1) n)) ((fr x2) n))) ((fr ((pl x1) x2)) n)) (((satz57 x1) x2) n)) as proof of ((_TPTP_eq ((fr ((pl x1) x2)) n)) ((pf ((fr x1) n)) ((fr x2) n))) % 0.08/0.58 Found (((satz38 ((pf ((fr x1) n)) ((fr x2) n))) ((fr ((pl x1) x2)) n)) (((satz57 x1) x2) n)) as proof of ((_TPTP_eq ((fr ((pl x1) x2)) n)) ((pf ((fr x1) n)) ((fr x2) n))) % 0.08/0.58 Got proof (((satz38 ((pf ((fr x1) n)) ((fr x2) n))) ((fr ((pl x1) x2)) n)) (((satz57 x1) x2) n)) % 0.08/0.59 Time elapsed = 0.057763s % 0.08/0.59 node=7 cost=-239.000000 depth=7 % 0.08/0.59:::::::::::::::::::::: % 0.08/0.59 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.08/0.59 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.08/0.59 (((satz38 ((pf ((fr x1) n)) ((fr x2) n))) ((fr ((pl x1) x2)) n)) (((satz57 x1) x2) n)) % 0.08/0.59 % SZS output end Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p %------------------------------------------------------------------------------