%------------------------------------------------------------------------------ % File : cocATP---0.2.0 % Problem : NUM770^1 : TPTP v7.0.0. Released v3.7.0. % Transfm : none % Format : tptp:raw % Command : python CASC.py /export/starexec/sandbox/benchmark/theBenchmark.p % Computer : n095.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 0.43s % Output : Proof 0.43s % 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.04 % Problem : NUM770^1 : TPTP v7.0.0. Released v3.7.0. % 0.00/0.04 % Command : python CASC.py /export/starexec/sandbox/benchmark/theBenchmark.p % 0.02/0.23 % Computer : n095.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:06:03 CST 2018 % 0.02/0.23 % CPUTime : % 0.02/0.25 Python 2.7.13 % 0.43/0.61 Using paths ['/home/cristobal/cocATP/CASC/TPTP/', '/export/starexec/sandbox/benchmark/', '/export/starexec/sandbox/benchmark/'] % 0.43/0.61 FOF formula (<kernel.Constant object at 0x2b953b5f6200>, <kernel.Type object at 0x2b953b5f67a0>) of role type named frac_type % 0.43/0.61 Using role type % 0.43/0.61 Declaring frac:Type % 0.43/0.61 FOF formula (<kernel.Constant object at 0x2b953af2ef38>, <kernel.Constant object at 0x2b953b5f6440>) of role type named x % 0.43/0.61 Using role type % 0.43/0.61 Declaring x:frac % 0.43/0.61 FOF formula (<kernel.Constant object at 0x2b953af2ef38>, <kernel.Constant object at 0x2b953b5f6440>) of role type named y % 0.43/0.61 Using role type % 0.43/0.61 Declaring y:frac % 0.43/0.61 FOF formula (<kernel.Constant object at 0x2b953b5f6200>, <kernel.Constant object at 0x2b953b5f6440>) of role type named v % 0.43/0.61 Using role type % 0.43/0.61 Declaring v:frac % 0.43/0.61 FOF formula (<kernel.Constant object at 0x2b953b5f6dd0>, <kernel.DependentProduct object at 0x2b953b5f6290>) of role type named moref % 0.43/0.61 Using role type % 0.43/0.61 Declaring moref:(frac->(frac->Prop)) % 0.43/0.61 FOF formula ((moref x) y) of role axiom named m % 0.43/0.61 A new axiom: ((moref x) y) % 0.43/0.61 FOF formula (<kernel.Constant object at 0x2b953b5f6440>, <kernel.DependentProduct object at 0x2b953b5f6200>) of role type named eq % 0.43/0.61 Using role type % 0.43/0.61 Declaring _TPTP_eq:(frac->(frac->Prop)) % 0.43/0.61 FOF formula (<kernel.Constant object at 0x2b953b5f64d0>, <kernel.DependentProduct object at 0x2b953b5f6dd0>) of role type named pf % 0.43/0.61 Using role type % 0.43/0.61 Declaring pf:(frac->(frac->frac)) % 0.43/0.61 FOF formula ((_TPTP_eq ((pf y) v)) x) of role axiom named e % 0.43/0.61 A new axiom: ((_TPTP_eq ((pf y) v)) x) % 0.43/0.61 FOF formula (<kernel.Constant object at 0x2b953b5f6200>, <kernel.DependentProduct object at 0x2b953b5f6830>) of role type named mf % 0.43/0.61 Using role type % 0.43/0.61 Declaring mf:(frac->(frac->frac)) % 0.43/0.61 FOF formula (forall (Xx:frac) (Xy:frac) (Xv:frac) (Xw:frac), (((_TPTP_eq ((pf Xy) Xv)) Xx)->(((_TPTP_eq ((pf Xy) Xw)) Xx)->((_TPTP_eq Xv) Xw)))) of role axiom named satz67b % 0.43/0.61 A new axiom: (forall (Xx:frac) (Xy:frac) (Xv:frac) (Xw:frac), (((_TPTP_eq ((pf Xy) Xv)) Xx)->(((_TPTP_eq ((pf Xy) Xw)) Xx)->((_TPTP_eq Xv) Xw)))) % 0.43/0.61 FOF formula (forall (Xx:frac) (Xy:frac), (((moref Xx) Xy)->((_TPTP_eq ((pf Xy) ((mf Xx) Xy))) Xx))) of role axiom named satz67c % 0.43/0.61 A new axiom: (forall (Xx:frac) (Xy:frac), (((moref Xx) Xy)->((_TPTP_eq ((pf Xy) ((mf Xx) Xy))) Xx))) % 0.43/0.61 FOF formula ((_TPTP_eq v) ((mf x) y)) of role conjecture named satz67e % 0.43/0.61 Conjecture to prove = ((_TPTP_eq v) ((mf x) y)):Prop % 0.43/0.61 We need to prove ['((_TPTP_eq v) ((mf x) y))'] % 0.43/0.61 Parameter frac:Type. % 0.43/0.61 Parameter x:frac. % 0.43/0.61 Parameter y:frac. % 0.43/0.61 Parameter v:frac. % 0.43/0.61 Parameter moref:(frac->(frac->Prop)). % 0.43/0.61 Axiom m:((moref x) y). % 0.43/0.61 Parameter _TPTP_eq:(frac->(frac->Prop)). % 0.43/0.61 Parameter pf:(frac->(frac->frac)). % 0.43/0.61 Axiom e:((_TPTP_eq ((pf y) v)) x). % 0.43/0.61 Parameter mf:(frac->(frac->frac)). % 0.43/0.61 Axiom satz67b:(forall (Xx:frac) (Xy:frac) (Xv:frac) (Xw:frac), (((_TPTP_eq ((pf Xy) Xv)) Xx)->(((_TPTP_eq ((pf Xy) Xw)) Xx)->((_TPTP_eq Xv) Xw)))). % 0.43/0.61 Axiom satz67c:(forall (Xx:frac) (Xy:frac), (((moref Xx) Xy)->((_TPTP_eq ((pf Xy) ((mf Xx) Xy))) Xx))). % 0.43/0.61 Trying to prove ((_TPTP_eq v) ((mf x) y)) % 0.43/0.61 Found e:((_TPTP_eq ((pf y) v)) x) % 0.43/0.61 Found e as proof of ((_TPTP_eq ((pf y) v)) x) % 0.43/0.61 Found m:((moref x) y) % 0.43/0.61 Found m as proof of ((moref x) y) % 0.43/0.61 Found (satz67c00 m) as proof of ((_TPTP_eq ((pf y) ((mf x) y))) x) % 0.43/0.61 Found ((satz67c0 y) m) as proof of ((_TPTP_eq ((pf y) ((mf x) y))) x) % 0.43/0.61 Found (((satz67c x) y) m) as proof of ((_TPTP_eq ((pf y) ((mf x) y))) x) % 0.43/0.61 Found (((satz67c x) y) m) as proof of ((_TPTP_eq ((pf y) ((mf x) y))) x) % 0.43/0.61 Found ((satz67b000 e) (((satz67c x) y) m)) as proof of ((_TPTP_eq v) ((mf x) y)) % 0.43/0.61 Found ((((satz67b00 x) y) e) (((satz67c x) y) m)) as proof of ((_TPTP_eq v) ((mf x) y)) % 0.43/0.61 Found (((((fun (Xx:frac) (Xy:frac)=> (((satz67b0 Xx) Xy) ((mf x) y))) x) y) e) (((satz67c x) y) m)) as proof of ((_TPTP_eq v) ((mf x) y)) % 0.43/0.61 Found (((((fun (Xx:frac) (Xy:frac)=> ((((fun (Xx:frac) (Xy:frac)=> (((satz67b Xx) Xy) v)) Xx) Xy) ((mf x) y))) x) y) e) (((satz67c x) y) m)) as proof of ((_TPTP_eq v) ((mf x) y)) % 0.43/0.61 Found (((((fun (Xx:frac) (Xy:frac)=> ((((fun (Xx:frac) (Xy:frac)=> (((satz67b Xx) Xy) v)) Xx) Xy) ((mf x) y))) x) y) e) (((satz67c x) y) m)) as proof of ((_TPTP_eq v) ((mf x) y)) % 0.43/0.61 Got proof (((((fun (Xx:frac) (Xy:frac)=> ((((fun (Xx:frac) (Xy:frac)=> (((satz67b Xx) Xy) v)) Xx) Xy) ((mf x) y))) x) y) e) (((satz67c x) y) m)) % 0.43/0.62 Time elapsed = 0.077581s % 0.43/0.62 node=19 cost=516.000000 depth=9 % 0.43/0.62:::::::::::::::::::::: % 0.43/0.62 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 0.43/0.62 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p % 0.43/0.62 (((((fun (Xx:frac) (Xy:frac)=> ((((fun (Xx:frac) (Xy:frac)=> (((satz67b Xx) Xy) v)) Xx) Xy) ((mf x) y))) x) y) e) (((satz67c x) y) m)) % 0.43/0.62 % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p %------------------------------------------------------------------------------