%------------------------------------------------------------------------------ % File : cocATP---0.2.0 % Problem : NUM729^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 : n082.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:34 EST 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 : NUM729^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 : n082.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:19:21 CST 2018 % 0.02/0.23 % CPUTime : % 0.06/0.27 Python 2.7.13 % 0.39/0.75 Using paths ['/home/cristobal/cocATP/CASC/TPTP/', '/export/starexec/sandbox2/benchmark/', '/export/starexec/sandbox2/benchmark/'] % 0.39/0.75 FOF formula (<kernel.Constant object at 0x2b716e20d560>, <kernel.Type object at 0x2b716de45518>) of role type named nat_type % 0.39/0.75 Using role type % 0.39/0.75 Declaring nat:Type % 0.39/0.75 FOF formula (<kernel.Constant object at 0x2b716df7fdd0>, <kernel.Constant object at 0x2b716de45128>) of role type named x1 % 0.39/0.75 Using role type % 0.39/0.75 Declaring x1:nat % 0.39/0.75 FOF formula (<kernel.Constant object at 0x2b716e20d560>, <kernel.Constant object at 0x2b716de454d0>) of role type named x2 % 0.39/0.75 Using role type % 0.39/0.75 Declaring x2:nat % 0.39/0.75 FOF formula (<kernel.Constant object at 0x2b716e20de60>, <kernel.Constant object at 0x2b716de459e0>) of role type named n % 0.39/0.75 Using role type % 0.39/0.75 Declaring n:nat % 0.39/0.75 FOF formula (<kernel.Constant object at 0x2b716e20d368>, <kernel.Type object at 0x2b716de45128>) of role type named frac_type % 0.39/0.75 Using role type % 0.39/0.75 Declaring frac:Type % 0.39/0.75 FOF formula (<kernel.Constant object at 0x2b716e20d368>, <kernel.DependentProduct object at 0x2b716de45560>) of role type named eq % 0.39/0.75 Using role type % 0.39/0.75 Declaring _TPTP_eq:(frac->(frac->Prop)) % 0.39/0.75 FOF formula (<kernel.Constant object at 0x2b716de45518>, <kernel.DependentProduct object at 0x2b716de45908>) of role type named fr % 0.39/0.75 Using role type % 0.39/0.75 Declaring fr:(nat->(nat->frac)) % 0.39/0.75 FOF formula (<kernel.Constant object at 0x2b716de45a28>, <kernel.DependentProduct object at 0x2b716de45050>) of role type named ts % 0.39/0.75 Using role type % 0.39/0.75 Declaring ts:(nat->(nat->nat)) % 0.39/0.75 FOF formula (forall (Xx:frac) (Xy:frac), (((_TPTP_eq Xx) Xy)->((_TPTP_eq Xy) Xx))) of role axiom named satz38 % 0.39/0.75 A new axiom: (forall (Xx:frac) (Xy:frac), (((_TPTP_eq Xx) Xy)->((_TPTP_eq Xy) Xx))) % 0.39/0.75 FOF formula (forall (Xx1:nat) (Xx2:nat) (Xn:nat), ((_TPTP_eq ((fr Xx1) Xx2)) ((fr ((ts Xx1) Xn)) ((ts Xx2) Xn)))) of role axiom named satz40b % 0.39/0.75 A new axiom: (forall (Xx1:nat) (Xx2:nat) (Xn:nat), ((_TPTP_eq ((fr Xx1) Xx2)) ((fr ((ts Xx1) Xn)) ((ts Xx2) Xn)))) % 0.39/0.75 FOF formula ((_TPTP_eq ((fr ((ts x1) n)) ((ts x2) n))) ((fr x1) x2)) of role conjecture named satz40c % 0.39/0.75 Conjecture to prove = ((_TPTP_eq ((fr ((ts x1) n)) ((ts x2) n))) ((fr x1) x2)):Prop % 0.39/0.75 Parameter frac_DUMMY:frac. % 0.39/0.75 We need to prove ['((_TPTP_eq ((fr ((ts x1) n)) ((ts x2) n))) ((fr x1) x2))'] % 0.39/0.75 Parameter nat:Type. % 0.39/0.75 Parameter x1:nat. % 0.39/0.75 Parameter x2:nat. % 0.39/0.75 Parameter n:nat. % 0.39/0.75 Parameter frac:Type. % 0.39/0.75 Parameter _TPTP_eq:(frac->(frac->Prop)). % 0.39/0.75 Parameter fr:(nat->(nat->frac)). % 0.39/0.75 Parameter ts:(nat->(nat->nat)). % 0.39/0.75 Axiom satz38:(forall (Xx:frac) (Xy:frac), (((_TPTP_eq Xx) Xy)->((_TPTP_eq Xy) Xx))). % 0.39/0.75 Axiom satz40b:(forall (Xx1:nat) (Xx2:nat) (Xn:nat), ((_TPTP_eq ((fr Xx1) Xx2)) ((fr ((ts Xx1) Xn)) ((ts Xx2) Xn)))). % 0.39/0.75 Trying to prove ((_TPTP_eq ((fr ((ts x1) n)) ((ts x2) n))) ((fr x1) x2)) % 0.39/0.75 Found satz40b000:=(satz40b00 n):((_TPTP_eq ((fr x1) x2)) ((fr ((ts x1) n)) ((ts x2) n))) % 0.39/0.75 Found (satz40b00 n) as proof of ((_TPTP_eq ((fr x1) x2)) ((fr ((ts x1) n)) ((ts x2) n))) % 0.39/0.75 Found ((satz40b0 x2) n) as proof of ((_TPTP_eq ((fr x1) x2)) ((fr ((ts x1) n)) ((ts x2) n))) % 0.39/0.75 Found (((satz40b x1) x2) n) as proof of ((_TPTP_eq ((fr x1) x2)) ((fr ((ts x1) n)) ((ts x2) n))) % 0.39/0.75 Found (((satz40b x1) x2) n) as proof of ((_TPTP_eq ((fr x1) x2)) ((fr ((ts x1) n)) ((ts x2) n))) % 0.39/0.75 Found (satz3800 (((satz40b x1) x2) n)) as proof of ((_TPTP_eq ((fr ((ts x1) n)) ((ts x2) n))) ((fr x1) x2)) % 0.39/0.75 Found ((satz380 ((fr ((ts x1) n)) ((ts x2) n))) (((satz40b x1) x2) n)) as proof of ((_TPTP_eq ((fr ((ts x1) n)) ((ts x2) n))) ((fr x1) x2)) % 0.39/0.75 Found (((satz38 ((fr x1) x2)) ((fr ((ts x1) n)) ((ts x2) n))) (((satz40b x1) x2) n)) as proof of ((_TPTP_eq ((fr ((ts x1) n)) ((ts x2) n))) ((fr x1) x2)) % 0.39/0.75 Found (((satz38 ((fr x1) x2)) ((fr ((ts x1) n)) ((ts x2) n))) (((satz40b x1) x2) n)) as proof of ((_TPTP_eq ((fr ((ts x1) n)) ((ts x2) n))) ((fr x1) x2)) % 0.39/0.75 Got proof (((satz38 ((fr x1) x2)) ((fr ((ts x1) n)) ((ts x2) n))) (((satz40b x1) x2) n)) % 0.39/0.75 Time elapsed = 0.050663s % 0.39/0.75 node=7 cost=-239.000000 depth=7 % 0.39/0.75:::::::::::::::::::::: % 0.39/0.75 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.39/0.75 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.39/0.75 (((satz38 ((fr x1) x2)) ((fr ((ts x1) n)) ((ts x2) n))) (((satz40b x1) x2) n)) % 0.39/0.76 % SZS output end Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p %------------------------------------------------------------------------------