%------------------------------------------------------------------------------ % File : cocATP---0.2.0 % Problem : NUM758^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 : n033.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:39 EST 2018 % Result : Theorem 0.51s % Output : Proof 0.51s % 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 : NUM758^1 : TPTP v7.0.0. Released v3.7.0. % 0.00/0.04 % Command : python CASC.py /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.02/0.24 % Computer : n033.star.cs.uiowa.edu % 0.02/0.24 % Model : x86_64 x86_64 % 0.02/0.24 % CPU : Intel(R) Xeon(R) CPU E5-2609 0 @ 2.40GHz % 0.02/0.24 % Memory : 32218.625MB % 0.02/0.24 % OS : Linux 3.10.0-693.2.2.el7.x86_64 % 0.02/0.24 % CPULimit : 300 % 0.02/0.24 % DateTime : Fri Jan 5 13:53:49 CST 2018 % 0.02/0.24 % CPUTime : % 0.02/0.26 Python 2.7.13 % 0.51/0.89 Using paths ['/home/cristobal/cocATP/CASC/TPTP/', '/export/starexec/sandbox2/benchmark/', '/export/starexec/sandbox2/benchmark/'] % 0.51/0.89 FOF formula (<kernel.Constant object at 0x2ac889ef35a8>, <kernel.Type object at 0x2ac889ef3368>) of role type named frac_type % 0.51/0.89 Using role type % 0.51/0.89 Declaring frac:Type % 0.51/0.89 FOF formula (<kernel.Constant object at 0x2ac889ec9f80>, <kernel.Constant object at 0x2ac889ef37e8>) of role type named x % 0.51/0.89 Using role type % 0.51/0.89 Declaring x:frac % 0.51/0.89 FOF formula (<kernel.Constant object at 0x2ac889ef3170>, <kernel.Constant object at 0x2ac889ef37e8>) of role type named y % 0.51/0.89 Using role type % 0.51/0.89 Declaring y:frac % 0.51/0.89 FOF formula (<kernel.Constant object at 0x2ac889ef35a8>, <kernel.Constant object at 0x2ac889ef37e8>) of role type named z % 0.51/0.89 Using role type % 0.51/0.89 Declaring z:frac % 0.51/0.89 FOF formula (<kernel.Constant object at 0x2ac889ef39e0>, <kernel.DependentProduct object at 0x2ac88a2bbcb0>) of role type named moref % 0.51/0.89 Using role type % 0.51/0.89 Declaring moref:(frac->(frac->Prop)) % 0.51/0.89 FOF formula (<kernel.Constant object at 0x2ac889ef37e8>, <kernel.DependentProduct object at 0x2ac88a2bb320>) of role type named pf % 0.51/0.89 Using role type % 0.51/0.89 Declaring pf:(frac->(frac->frac)) % 0.51/0.89 FOF formula ((moref ((pf z) x)) ((pf z) y)) of role axiom named m % 0.51/0.89 A new axiom: ((moref ((pf z) x)) ((pf z) y)) % 0.51/0.89 FOF formula (forall (Xx:frac) (Xy:frac) (Xz:frac), (((moref ((pf Xx) Xz)) ((pf Xy) Xz))->((moref Xx) Xy))) of role axiom named satz63a % 0.51/0.89 A new axiom: (forall (Xx:frac) (Xy:frac) (Xz:frac), (((moref ((pf Xx) Xz)) ((pf Xy) Xz))->((moref Xx) Xy))) % 0.51/0.89 FOF formula (<kernel.Constant object at 0x2ac889ef3368>, <kernel.DependentProduct object at 0x2ac88a2bbf38>) of role type named eq % 0.51/0.89 Using role type % 0.51/0.89 Declaring _TPTP_eq:(frac->(frac->Prop)) % 0.51/0.89 FOF formula (forall (Xx:frac) (Xy:frac) (Xz:frac) (Xu:frac), (((moref Xx) Xy)->(((_TPTP_eq Xx) Xz)->(((_TPTP_eq Xy) Xu)->((moref Xz) Xu))))) of role axiom named satz44 % 0.51/0.89 A new axiom: (forall (Xx:frac) (Xy:frac) (Xz:frac) (Xu:frac), (((moref Xx) Xy)->(((_TPTP_eq Xx) Xz)->(((_TPTP_eq Xy) Xu)->((moref Xz) Xu))))) % 0.51/0.89 FOF formula (forall (Xx:frac) (Xy:frac), ((_TPTP_eq ((pf Xx) Xy)) ((pf Xy) Xx))) of role axiom named satz58 % 0.51/0.89 A new axiom: (forall (Xx:frac) (Xy:frac), ((_TPTP_eq ((pf Xx) Xy)) ((pf Xy) Xx))) % 0.51/0.89 FOF formula ((moref x) y) of role conjecture named satz63d % 0.51/0.89 Conjecture to prove = ((moref x) y):Prop % 0.51/0.89 We need to prove ['((moref x) y)'] % 0.51/0.89 Parameter frac:Type. % 0.51/0.89 Parameter x:frac. % 0.51/0.89 Parameter y:frac. % 0.51/0.89 Parameter z:frac. % 0.51/0.89 Parameter moref:(frac->(frac->Prop)). % 0.51/0.89 Parameter pf:(frac->(frac->frac)). % 0.51/0.89 Axiom m:((moref ((pf z) x)) ((pf z) y)). % 0.51/0.89 Axiom satz63a:(forall (Xx:frac) (Xy:frac) (Xz:frac), (((moref ((pf Xx) Xz)) ((pf Xy) Xz))->((moref Xx) Xy))). % 0.51/0.89 Parameter _TPTP_eq:(frac->(frac->Prop)). % 0.51/0.89 Axiom satz44:(forall (Xx:frac) (Xy:frac) (Xz:frac) (Xu:frac), (((moref Xx) Xy)->(((_TPTP_eq Xx) Xz)->(((_TPTP_eq Xy) Xu)->((moref Xz) Xu))))). % 0.51/0.89 Axiom satz58:(forall (Xx:frac) (Xy:frac), ((_TPTP_eq ((pf Xx) Xy)) ((pf Xy) Xx))). % 0.51/0.89 Trying to prove ((moref x) y) % 0.51/0.89 Found m:((moref ((pf z) x)) ((pf z) y)) % 0.51/0.89 Found m as proof of ((moref ((pf z) x)) ((pf z) y)) % 0.51/0.89 Found m:((moref ((pf z) x)) ((pf z) y)) % 0.51/0.89 Found m as proof of ((moref ((pf z) x)) ((pf z) y)) % 0.51/0.89 Found satz5800:=(satz580 y):((_TPTP_eq ((pf z) y)) ((pf y) z)) % 0.51/0.89 Found (satz580 y) as proof of ((_TPTP_eq ((pf z) y)) ((pf y) Xz)) % 0.51/0.89 Found ((satz58 z) y) as proof of ((_TPTP_eq ((pf z) y)) ((pf y) Xz)) % 0.51/0.89 Found ((satz58 z) y) as proof of ((_TPTP_eq ((pf z) y)) ((pf y) Xz)) % 0.51/0.89 Found ((satz58 z) y) as proof of ((_TPTP_eq ((pf z) y)) ((pf y) Xz)) % 0.51/0.89 Found satz5800:=(satz580 x):((_TPTP_eq ((pf z) x)) ((pf x) z)) % 0.51/0.89 Found (satz580 x) as proof of ((_TPTP_eq ((pf z) x)) ((pf x) Xz)) % 0.51/0.89 Found ((satz58 z) x) as proof of ((_TPTP_eq ((pf z) x)) ((pf x) Xz)) % 0.51/0.89 Found ((satz58 z) x) as proof of ((_TPTP_eq ((pf z) x)) ((pf x) Xz)) % 0.51/0.89 Found ((satz58 z) x) as proof of ((_TPTP_eq ((pf z) x)) ((pf x) Xz)) % 0.51/0.89 Found (((satz44000 m) ((satz58 z) x)) ((satz58 z) y)) as proof of ((moref ((pf x) Xz)) ((pf y) Xz)) % 0.51/0.89 Found (((((satz4400 ((pf z) x)) ((pf z) y)) m) ((satz58 z) x)) ((satz58 z) y)) as proof of ((moref ((pf x) Xz)) ((pf y) Xz)) % 0.51/0.89 Found ((((((fun (Xx:frac) (Xy:frac)=> (((satz440 Xx) Xy) ((pf y) Xz))) ((pf z) x)) ((pf z) y)) m) ((satz58 z) x)) ((satz58 z) y)) as proof of ((moref ((pf x) Xz)) ((pf y) Xz)) % 0.51/0.90 Found ((((((fun (Xx:frac) (Xy:frac)=> ((((fun (Xx:frac) (Xy:frac)=> (((satz44 Xx) Xy) ((pf x) Xz))) Xx) Xy) ((pf y) Xz))) ((pf z) x)) ((pf z) y)) m) ((satz58 z) x)) ((satz58 z) y)) as proof of ((moref ((pf x) Xz)) ((pf y) Xz)) % 0.51/0.90 Found ((((((fun (Xx:frac) (Xy:frac)=> ((((fun (Xx:frac) (Xy:frac)=> (((satz44 Xx) Xy) ((pf x) Xz))) Xx) Xy) ((pf y) Xz))) ((pf z) x)) ((pf z) y)) m) ((satz58 z) x)) ((satz58 z) y)) as proof of ((moref ((pf x) Xz)) ((pf y) Xz)) % 0.51/0.90 Found (satz63a000 ((((((fun (Xx:frac) (Xy:frac)=> ((((fun (Xx:frac) (Xy:frac)=> (((satz44 Xx) Xy) ((pf x) Xz))) Xx) Xy) ((pf y) Xz))) ((pf z) x)) ((pf z) y)) m) ((satz58 z) x)) ((satz58 z) y))) as proof of ((moref x) y) % 0.51/0.90 Found ((satz63a00 z) ((((((fun (Xx:frac) (Xy:frac)=> ((((fun (Xx:frac) (Xy:frac)=> (((satz44 Xx) Xy) ((pf x) z))) Xx) Xy) ((pf y) z))) ((pf z) x)) ((pf z) y)) m) ((satz58 z) x)) ((satz58 z) y))) as proof of ((moref x) y) % 0.51/0.90 Found (((satz63a0 y) z) ((((((fun (Xx:frac) (Xy:frac)=> ((((fun (Xx:frac) (Xy:frac)=> (((satz44 Xx) Xy) ((pf x) z))) Xx) Xy) ((pf y) z))) ((pf z) x)) ((pf z) y)) m) ((satz58 z) x)) ((satz58 z) y))) as proof of ((moref x) y) % 0.51/0.90 Found ((((satz63a x) y) z) ((((((fun (Xx:frac) (Xy:frac)=> ((((fun (Xx:frac) (Xy:frac)=> (((satz44 Xx) Xy) ((pf x) z))) Xx) Xy) ((pf y) z))) ((pf z) x)) ((pf z) y)) m) ((satz58 z) x)) ((satz58 z) y))) as proof of ((moref x) y) % 0.51/0.90 Found ((((satz63a x) y) z) ((((((fun (Xx:frac) (Xy:frac)=> ((((fun (Xx:frac) (Xy:frac)=> (((satz44 Xx) Xy) ((pf x) z))) Xx) Xy) ((pf y) z))) ((pf z) x)) ((pf z) y)) m) ((satz58 z) x)) ((satz58 z) y))) as proof of ((moref x) y) % 0.51/0.90 Got proof ((((satz63a x) y) z) ((((((fun (Xx:frac) (Xy:frac)=> ((((fun (Xx:frac) (Xy:frac)=> (((satz44 Xx) Xy) ((pf x) z))) Xx) Xy) ((pf y) z))) ((pf z) x)) ((pf z) y)) m) ((satz58 z) x)) ((satz58 z) y))) % 0.51/0.90 Time elapsed = 0.160619s % 0.51/0.90 node=40 cost=615.000000 depth=13 % 0.51/0.90:::::::::::::::::::::: % 0.51/0.90 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.51/0.90 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.51/0.90 ((((satz63a x) y) z) ((((((fun (Xx:frac) (Xy:frac)=> ((((fun (Xx:frac) (Xy:frac)=> (((satz44 Xx) Xy) ((pf x) z))) Xx) Xy) ((pf y) z))) ((pf z) x)) ((pf z) y)) m) ((satz58 z) x)) ((satz58 z) y))) % 0.51/0.90 % SZS output end Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p %------------------------------------------------------------------------------