%------------------------------------------------------------------------------ % File : cocATP---0.2.0 % Problem : NUM767^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 : n072.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:41 EST 2018 % Result : Theorem 0.78s % Output : Proof 0.78s % 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 : NUM767^1 : TPTP v7.0.0. Released v3.7.0. % 0.00/0.03 % Command : python CASC.py /export/starexec/sandbox/benchmark/theBenchmark.p % 0.02/0.22 % Computer : n072.star.cs.uiowa.edu % 0.02/0.22 % Model : x86_64 x86_64 % 0.02/0.22 % CPU : Intel(R) Xeon(R) CPU E5-2609 0 @ 2.40GHz % 0.02/0.22 % Memory : 32218.625MB % 0.02/0.22 % OS : Linux 3.10.0-693.2.2.el7.x86_64 % 0.02/0.22 % CPULimit : 300 % 0.02/0.22 % DateTime : Fri Jan 5 14:02:18 CST 2018 % 0.02/0.23 % CPUTime : % 0.07/0.24 Python 2.7.13 % 0.78/0.97 Using paths ['/home/cristobal/cocATP/CASC/TPTP/', '/export/starexec/sandbox/benchmark/', '/export/starexec/sandbox/benchmark/'] % 0.78/0.97 FOF formula (<kernel.Constant object at 0x2ae32458c950>, <kernel.Type object at 0x2ae325009560>) of role type named frac_type % 0.78/0.97 Using role type % 0.78/0.97 Declaring frac:Type % 0.78/0.97 FOF formula (<kernel.Constant object at 0x2ae31cc51170>, <kernel.Constant object at 0x2ae325009050>) of role type named x % 0.78/0.97 Using role type % 0.78/0.97 Declaring x:frac % 0.78/0.97 FOF formula (<kernel.Constant object at 0x2ae32458c200>, <kernel.Constant object at 0x2ae325009a70>) of role type named y % 0.78/0.97 Using role type % 0.78/0.97 Declaring y:frac % 0.78/0.97 FOF formula (<kernel.Constant object at 0x2ae32458c950>, <kernel.Constant object at 0x2ae325009a70>) of role type named v % 0.78/0.97 Using role type % 0.78/0.97 Declaring v:frac % 0.78/0.97 FOF formula (<kernel.Constant object at 0x2ae32458c950>, <kernel.Constant object at 0x2ae325009a70>) of role type named w % 0.78/0.97 Using role type % 0.78/0.97 Declaring w:frac % 0.78/0.97 FOF formula (<kernel.Constant object at 0x2ae3250093b0>, <kernel.DependentProduct object at 0x2ae3248e5d88>) of role type named eq % 0.78/0.97 Using role type % 0.78/0.97 Declaring _TPTP_eq:(frac->(frac->Prop)) % 0.78/0.97 FOF formula (<kernel.Constant object at 0x2ae325009200>, <kernel.DependentProduct object at 0x2ae3250099e0>) of role type named pf % 0.78/0.97 Using role type % 0.78/0.97 Declaring pf:(frac->(frac->frac)) % 0.78/0.97 FOF formula ((_TPTP_eq ((pf y) v)) x) of role axiom named e % 0.78/0.97 A new axiom: ((_TPTP_eq ((pf y) v)) x) % 0.78/0.97 FOF formula ((_TPTP_eq ((pf y) w)) x) of role axiom named f % 0.78/0.97 A new axiom: ((_TPTP_eq ((pf y) w)) x) % 0.78/0.97 FOF formula (forall (Xx:frac) (Xy:frac) (Xz:frac), (((_TPTP_eq ((pf Xz) Xx)) ((pf Xz) Xy))->((_TPTP_eq Xx) Xy))) of role axiom named satz63e % 0.78/0.97 A new axiom: (forall (Xx:frac) (Xy:frac) (Xz:frac), (((_TPTP_eq ((pf Xz) Xx)) ((pf Xz) Xy))->((_TPTP_eq Xx) Xy))) % 0.78/0.97 FOF formula (forall (Xx:frac) (Xy:frac) (Xz:frac), (((_TPTP_eq Xx) Xy)->(((_TPTP_eq Xy) Xz)->((_TPTP_eq Xx) Xz)))) of role axiom named satz39 % 0.78/0.97 A new axiom: (forall (Xx:frac) (Xy:frac) (Xz:frac), (((_TPTP_eq Xx) Xy)->(((_TPTP_eq Xy) Xz)->((_TPTP_eq Xx) Xz)))) % 0.78/0.97 FOF formula (forall (Xx:frac) (Xy:frac), (((_TPTP_eq Xx) Xy)->((_TPTP_eq Xy) Xx))) of role axiom named satz38 % 0.78/0.97 A new axiom: (forall (Xx:frac) (Xy:frac), (((_TPTP_eq Xx) Xy)->((_TPTP_eq Xy) Xx))) % 0.78/0.97 FOF formula ((_TPTP_eq v) w) of role conjecture named satz67b % 0.78/0.97 Conjecture to prove = ((_TPTP_eq v) w):Prop % 0.78/0.97 We need to prove ['((_TPTP_eq v) w)'] % 0.78/0.97 Parameter frac:Type. % 0.78/0.97 Parameter x:frac. % 0.78/0.97 Parameter y:frac. % 0.78/0.97 Parameter v:frac. % 0.78/0.97 Parameter w:frac. % 0.78/0.97 Parameter _TPTP_eq:(frac->(frac->Prop)). % 0.78/0.97 Parameter pf:(frac->(frac->frac)). % 0.78/0.97 Axiom e:((_TPTP_eq ((pf y) v)) x). % 0.78/0.97 Axiom f:((_TPTP_eq ((pf y) w)) x). % 0.78/0.97 Axiom satz63e:(forall (Xx:frac) (Xy:frac) (Xz:frac), (((_TPTP_eq ((pf Xz) Xx)) ((pf Xz) Xy))->((_TPTP_eq Xx) Xy))). % 0.78/0.97 Axiom satz39:(forall (Xx:frac) (Xy:frac) (Xz:frac), (((_TPTP_eq Xx) Xy)->(((_TPTP_eq Xy) Xz)->((_TPTP_eq Xx) Xz)))). % 0.78/0.97 Axiom satz38:(forall (Xx:frac) (Xy:frac), (((_TPTP_eq Xx) Xy)->((_TPTP_eq Xy) Xx))). % 0.78/0.97 Trying to prove ((_TPTP_eq v) w) % 0.78/0.97 Found e:((_TPTP_eq ((pf y) v)) x) % 0.78/0.97 Instantiate: Xz:=y:frac;Xy:=x:frac % 0.78/0.97 Found e as proof of ((_TPTP_eq ((pf Xz) v)) Xy) % 0.78/0.97 Found f:((_TPTP_eq ((pf y) w)) x) % 0.78/0.97 Instantiate: Xz:=y:frac;Xy:=x:frac % 0.78/0.97 Found f as proof of ((_TPTP_eq ((pf Xz) w)) Xy) % 0.78/0.97 Found (satz3800 f) as proof of ((_TPTP_eq Xy) ((pf Xz) w)) % 0.78/0.97 Found ((satz380 Xy) f) as proof of ((_TPTP_eq Xy) ((pf Xz) w)) % 0.78/0.97 Found (((satz38 ((pf Xz) w)) Xy) f) as proof of ((_TPTP_eq Xy) ((pf Xz) w)) % 0.78/0.97 Found (((satz38 ((pf Xz) w)) Xy) f) as proof of ((_TPTP_eq Xy) ((pf Xz) w)) % 0.78/0.97 Found ((satz39000 e) (((satz38 ((pf Xz) w)) Xy) f)) as proof of ((_TPTP_eq ((pf Xz) v)) ((pf Xz) w)) % 0.78/0.97 Found (((satz3900 x) e) (((satz38 ((pf Xz) w)) x) f)) as proof of ((_TPTP_eq ((pf Xz) v)) ((pf Xz) w)) % 0.78/0.97 Found ((((fun (Xy:frac)=> ((satz390 Xy) ((pf Xz) w))) x) e) (((satz38 ((pf Xz) w)) x) f)) as proof of ((_TPTP_eq ((pf Xz) v)) ((pf Xz) w)) % 0.78/0.97 Found ((((fun (Xy:frac)=> (((satz39 ((pf Xz) v)) Xy) ((pf Xz) w))) x) e) (((satz38 ((pf Xz) w)) x) f)) as proof of ((_TPTP_eq ((pf Xz) v)) ((pf Xz) w)) % 0.78/0.97 Found ((((fun (Xy:frac)=> (((satz39 ((pf Xz) v)) Xy) ((pf Xz) w))) x) e) (((satz38 ((pf Xz) w)) x) f)) as proof of ((_TPTP_eq ((pf Xz) v)) ((pf Xz) w)) % 0.78/0.97 Found (satz63e000 ((((fun (Xy:frac)=> (((satz39 ((pf Xz) v)) Xy) ((pf Xz) w))) x) e) (((satz38 ((pf Xz) w)) x) f))) as proof of ((_TPTP_eq v) w) % 0.78/0.98 Found ((satz63e00 y) ((((fun (Xy:frac)=> (((satz39 ((pf y) v)) Xy) ((pf y) w))) x) e) (((satz38 ((pf y) w)) x) f))) as proof of ((_TPTP_eq v) w) % 0.78/0.98 Found (((satz63e0 w) y) ((((fun (Xy:frac)=> (((satz39 ((pf y) v)) Xy) ((pf y) w))) x) e) (((satz38 ((pf y) w)) x) f))) as proof of ((_TPTP_eq v) w) % 0.78/0.98 Found ((((satz63e v) w) y) ((((fun (Xy:frac)=> (((satz39 ((pf y) v)) Xy) ((pf y) w))) x) e) (((satz38 ((pf y) w)) x) f))) as proof of ((_TPTP_eq v) w) % 0.78/0.98 Found ((((satz63e v) w) y) ((((fun (Xy:frac)=> (((satz39 ((pf y) v)) Xy) ((pf y) w))) x) e) (((satz38 ((pf y) w)) x) f))) as proof of ((_TPTP_eq v) w) % 0.78/0.98 Got proof ((((satz63e v) w) y) ((((fun (Xy:frac)=> (((satz39 ((pf y) v)) Xy) ((pf y) w))) x) e) (((satz38 ((pf y) w)) x) f))) % 0.78/0.98 Time elapsed = 0.448533s % 0.78/0.98 node=111 cost=981.000000 depth=14 % 0.78/0.98:::::::::::::::::::::: % 0.78/0.98 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 0.78/0.98 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p % 0.78/0.98 ((((satz63e v) w) y) ((((fun (Xy:frac)=> (((satz39 ((pf y) v)) Xy) ((pf y) w))) x) e) (((satz38 ((pf y) w)) x) f))) % 0.78/0.98 % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p %------------------------------------------------------------------------------