%------------------------------------------------------------------------------ % File : cocATP---0.2.0 % Problem : NUM771^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 : n157.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:42 EST 2018 % Result : Theorem 1.84s % Output : Proof 1.84s % 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 : NUM771^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 : n157.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 14:05:34 CST 2018 % 0.02/0.23 % CPUTime : % 0.02/0.26 Python 2.7.13 % 1.84/2.26 Using paths ['/home/cristobal/cocATP/CASC/TPTP/', '/export/starexec/sandbox2/benchmark/', '/export/starexec/sandbox2/benchmark/'] % 1.84/2.26 FOF formula (<kernel.Constant object at 0x2b61e6edae60>, <kernel.Type object at 0x2b61e6edaa70>) of role type named frac_type % 1.84/2.26 Using role type % 1.84/2.26 Declaring frac:Type % 1.84/2.26 FOF formula (<kernel.Constant object at 0x2b61e6eda050>, <kernel.Constant object at 0x2b61e6edacb0>) of role type named x % 1.84/2.26 Using role type % 1.84/2.26 Declaring x:frac % 1.84/2.26 FOF formula (<kernel.Constant object at 0x2b61e72a5d88>, <kernel.Constant object at 0x2b61e6edacb0>) of role type named y % 1.84/2.26 Using role type % 1.84/2.26 Declaring y:frac % 1.84/2.26 FOF formula (<kernel.Constant object at 0x2b61e6edae60>, <kernel.DependentProduct object at 0x2b61e6fb7488>) of role type named eq % 1.84/2.26 Using role type % 1.84/2.26 Declaring _TPTP_eq:(frac->(frac->Prop)) % 1.84/2.26 FOF formula (<kernel.Constant object at 0x2b61e6eda050>, <kernel.Type object at 0x2b61e6fb7488>) of role type named nat_type % 1.84/2.26 Using role type % 1.84/2.26 Declaring nat:Type % 1.84/2.26 FOF formula (<kernel.Constant object at 0x2b61e6edae60>, <kernel.DependentProduct object at 0x2b61e6fb70e0>) of role type named fr % 1.84/2.26 Using role type % 1.84/2.26 Declaring fr:(nat->(nat->frac)) % 1.84/2.26 FOF formula (<kernel.Constant object at 0x2b61e6edacb0>, <kernel.DependentProduct object at 0x2b61e6fb70e0>) of role type named ts % 1.84/2.26 Using role type % 1.84/2.26 Declaring ts:(nat->(nat->nat)) % 1.84/2.26 FOF formula (<kernel.Constant object at 0x2b61e6edae60>, <kernel.DependentProduct object at 0x2b61e6ed6ef0>) of role type named num % 1.84/2.26 Using role type % 1.84/2.26 Declaring num:(frac->nat) % 1.84/2.26 FOF formula (<kernel.Constant object at 0x2b61e6fb7e60>, <kernel.DependentProduct object at 0x2b61e6ed6440>) of role type named den % 1.84/2.26 Using role type % 1.84/2.26 Declaring den:(frac->nat) % 1.84/2.26 FOF formula (forall (Xx:frac), ((_TPTP_eq Xx) Xx)) of role axiom named satz37 % 1.84/2.26 A new axiom: (forall (Xx:frac), ((_TPTP_eq Xx) Xx)) % 1.84/2.26 FOF formula (forall (Xx:nat) (Xy:nat), (((eq nat) ((ts Xx) Xy)) ((ts Xy) Xx))) of role axiom named satz29 % 1.84/2.26 A new axiom: (forall (Xx:nat) (Xy:nat), (((eq nat) ((ts Xx) Xy)) ((ts Xy) Xx))) % 1.84/2.26 FOF formula ((_TPTP_eq ((fr ((ts (num x)) (num y))) ((ts (den x)) (den y)))) ((fr ((ts (num y)) (num x))) ((ts (den y)) (den x)))) of role conjecture named satz69 % 1.84/2.26 Conjecture to prove = ((_TPTP_eq ((fr ((ts (num x)) (num y))) ((ts (den x)) (den y)))) ((fr ((ts (num y)) (num x))) ((ts (den y)) (den x)))):Prop % 1.84/2.26 Parameter nat_DUMMY:nat. % 1.84/2.26 We need to prove ['((_TPTP_eq ((fr ((ts (num x)) (num y))) ((ts (den x)) (den y)))) ((fr ((ts (num y)) (num x))) ((ts (den y)) (den x))))'] % 1.84/2.26 Parameter frac:Type. % 1.84/2.26 Parameter x:frac. % 1.84/2.26 Parameter y:frac. % 1.84/2.26 Parameter _TPTP_eq:(frac->(frac->Prop)). % 1.84/2.26 Parameter nat:Type. % 1.84/2.26 Parameter fr:(nat->(nat->frac)). % 1.84/2.26 Parameter ts:(nat->(nat->nat)). % 1.84/2.26 Parameter num:(frac->nat). % 1.84/2.26 Parameter den:(frac->nat). % 1.84/2.26 Axiom satz37:(forall (Xx:frac), ((_TPTP_eq Xx) Xx)). % 1.84/2.26 Axiom satz29:(forall (Xx:nat) (Xy:nat), (((eq nat) ((ts Xx) Xy)) ((ts Xy) Xx))). % 1.84/2.26 Trying to prove ((_TPTP_eq ((fr ((ts (num x)) (num y))) ((ts (den x)) (den y)))) ((fr ((ts (num y)) (num x))) ((ts (den y)) (den x)))) % 1.84/2.26 Found satz370:=(satz37 ((fr ((ts (num y)) (num x))) ((ts (den x)) (den y)))):((_TPTP_eq ((fr ((ts (num y)) (num x))) ((ts (den x)) (den y)))) ((fr ((ts (num y)) (num x))) ((ts (den x)) (den y)))) % 1.84/2.26 Found (satz37 ((fr ((ts (num y)) (num x))) ((ts (den x)) (den y)))) as proof of ((_TPTP_eq ((fr ((ts (num y)) (num x))) ((ts (den x)) (den y)))) ((fr ((ts (num y)) (num x))) ((ts (den x)) (den y)))) % 1.84/2.26 Found (satz37 ((fr ((ts (num y)) (num x))) ((ts (den x)) (den y)))) as proof of ((_TPTP_eq ((fr ((ts (num y)) (num x))) ((ts (den x)) (den y)))) ((fr ((ts (num y)) (num x))) ((ts (den x)) (den y)))) % 1.84/2.26 Found (satz29000 (satz37 ((fr ((ts (num y)) (num x))) ((ts (den x)) (den y))))) as proof of ((_TPTP_eq ((fr ((ts (num y)) (num x))) ((ts (den x)) (den y)))) ((fr ((ts (num y)) (num x))) ((ts (den y)) (den x)))) % 1.84/2.26 Found ((satz2900 (fun (x1:nat)=> ((_TPTP_eq ((fr ((ts (num y)) (num x))) ((ts (den x)) (den y)))) ((fr ((ts (num y)) (num x))) x1)))) (satz37 ((fr ((ts (num y)) (num x))) ((ts (den x)) (den y))))) as proof of ((_TPTP_eq ((fr ((ts (num y)) (num x))) ((ts (den x)) (den y)))) ((fr ((ts (num y)) (num x))) ((ts (den y)) (den x)))) % 1.84/2.26 Found (((satz290 (den y)) (fun (x1:nat)=> ((_TPTP_eq ((fr ((ts (num y)) (num x))) ((ts (den x)) (den y)))) ((fr ((ts (num y)) (num x))) x1)))) (satz37 ((fr ((ts (num y)) (num x))) ((ts (den x)) (den y))))) as proof of ((_TPTP_eq ((fr ((ts (num y)) (num x))) ((ts (den x)) (den y)))) ((fr ((ts (num y)) (num x))) ((ts (den y)) (den x)))) % 1.84/2.27 Found ((((satz29 (den x)) (den y)) (fun (x1:nat)=> ((_TPTP_eq ((fr ((ts (num y)) (num x))) ((ts (den x)) (den y)))) ((fr ((ts (num y)) (num x))) x1)))) (satz37 ((fr ((ts (num y)) (num x))) ((ts (den x)) (den y))))) as proof of ((_TPTP_eq ((fr ((ts (num y)) (num x))) ((ts (den x)) (den y)))) ((fr ((ts (num y)) (num x))) ((ts (den y)) (den x)))) % 1.84/2.27 Found ((((satz29 (den x)) (den y)) (fun (x1:nat)=> ((_TPTP_eq ((fr ((ts (num y)) (num x))) ((ts (den x)) (den y)))) ((fr ((ts (num y)) (num x))) x1)))) (satz37 ((fr ((ts (num y)) (num x))) ((ts (den x)) (den y))))) as proof of ((_TPTP_eq ((fr ((ts (num y)) (num x))) ((ts (den x)) (den y)))) ((fr ((ts (num y)) (num x))) ((ts (den y)) (den x)))) % 1.84/2.27 Found (satz29__eq_sym000 ((((satz29 (den x)) (den y)) (fun (x1:nat)=> ((_TPTP_eq ((fr ((ts (num y)) (num x))) ((ts (den x)) (den y)))) ((fr ((ts (num y)) (num x))) x1)))) (satz37 ((fr ((ts (num y)) (num x))) ((ts (den x)) (den y)))))) as proof of ((_TPTP_eq ((fr ((ts (num x)) (num y))) ((ts (den x)) (den y)))) ((fr ((ts (num y)) (num x))) ((ts (den y)) (den x)))) % 1.84/2.27 Found ((satz29__eq_sym00 (fun (x1:nat)=> ((_TPTP_eq ((fr x1) ((ts (den x)) (den y)))) ((fr ((ts (num y)) (num x))) ((ts (den y)) (den x)))))) ((((satz29 (den x)) (den y)) (fun (x1:nat)=> ((_TPTP_eq ((fr ((ts (num y)) (num x))) ((ts (den x)) (den y)))) ((fr ((ts (num y)) (num x))) x1)))) (satz37 ((fr ((ts (num y)) (num x))) ((ts (den x)) (den y)))))) as proof of ((_TPTP_eq ((fr ((ts (num x)) (num y))) ((ts (den x)) (den y)))) ((fr ((ts (num y)) (num x))) ((ts (den y)) (den x)))) % 1.84/2.27 Found (((satz29__eq_sym0 (num y)) (fun (x1:nat)=> ((_TPTP_eq ((fr x1) ((ts (den x)) (den y)))) ((fr ((ts (num y)) (num x))) ((ts (den y)) (den x)))))) ((((satz29 (den x)) (den y)) (fun (x1:nat)=> ((_TPTP_eq ((fr ((ts (num y)) (num x))) ((ts (den x)) (den y)))) ((fr ((ts (num y)) (num x))) x1)))) (satz37 ((fr ((ts (num y)) (num x))) ((ts (den x)) (den y)))))) as proof of ((_TPTP_eq ((fr ((ts (num x)) (num y))) ((ts (den x)) (den y)))) ((fr ((ts (num y)) (num x))) ((ts (den y)) (den x)))) % 1.84/2.27 Found ((((satz29__eq_sym (num x)) (num y)) (fun (x1:nat)=> ((_TPTP_eq ((fr x1) ((ts (den x)) (den y)))) ((fr ((ts (num y)) (num x))) ((ts (den y)) (den x)))))) ((((satz29 (den x)) (den y)) (fun (x1:nat)=> ((_TPTP_eq ((fr ((ts (num y)) (num x))) ((ts (den x)) (den y)))) ((fr ((ts (num y)) (num x))) x1)))) (satz37 ((fr ((ts (num y)) (num x))) ((ts (den x)) (den y)))))) as proof of ((_TPTP_eq ((fr ((ts (num x)) (num y))) ((ts (den x)) (den y)))) ((fr ((ts (num y)) (num x))) ((ts (den y)) (den x)))) % 1.84/2.27 Found ((((satz29__eq_sym (num x)) (num y)) (fun (x1:nat)=> ((_TPTP_eq ((fr x1) ((ts (den x)) (den y)))) ((fr ((ts (num y)) (num x))) ((ts (den y)) (den x)))))) ((((satz29 (den x)) (den y)) (fun (x1:nat)=> ((_TPTP_eq ((fr ((ts (num y)) (num x))) ((ts (den x)) (den y)))) ((fr ((ts (num y)) (num x))) x1)))) (satz37 ((fr ((ts (num y)) (num x))) ((ts (den x)) (den y)))))) as proof of ((_TPTP_eq ((fr ((ts (num x)) (num y))) ((ts (den x)) (den y)))) ((fr ((ts (num y)) (num x))) ((ts (den y)) (den x)))) % 1.84/2.27 Got proof (((((fun (Xx:nat) (Xy:nat)=> ((((eq_sym nat) ((ts Xx) Xy)) ((ts Xy) Xx)) ((satz29 Xx) Xy))) (num x)) (num y)) (fun (x1:nat)=> ((_TPTP_eq ((fr x1) ((ts (den x)) (den y)))) ((fr ((ts (num y)) (num x))) ((ts (den y)) (den x)))))) ((((satz29 (den x)) (den y)) (fun (x1:nat)=> ((_TPTP_eq ((fr ((ts (num y)) (num x))) ((ts (den x)) (den y)))) ((fr ((ts (num y)) (num x))) x1)))) (satz37 ((fr ((ts (num y)) (num x))) ((ts (den x)) (den y)))))) % 1.84/2.27 Time elapsed = 1.546343s % 1.84/2.27 node=349 cost=883.000000 depth=11 % 1.84/2.27:::::::::::::::::::::: % 1.84/2.27 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 1.84/2.27 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p % 1.84/2.27 (((((fun (Xx:nat) (Xy:nat)=> ((((eq_sym nat) ((ts Xx) Xy)) ((ts Xy) Xx)) ((satz29 Xx) Xy))) (num x)) (num y)) (fun (x1:nat)=> ((_TPTP_eq ((fr x1) ((ts (den x)) (den y)))) ((fr ((ts (num y)) (num x))) ((ts (den y)) (den x)))))) ((((satz29 (den x)) (den y)) (fun (x1:nat)=> ((_TPTP_eq ((fr ((ts (num y)) (num x))) ((ts (den x)) (den y)))) ((fr ((ts (num y)) (num x))) x1)))) (satz37 ((fr ((ts (num y)) (num x))) ((ts (den x)) (den y)))))) % 1.84/2.28 % SZS output end Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p %------------------------------------------------------------------------------