%------------------------------------------------------------------------------ % File : cocATP---0.2.0 % Problem : NUM765^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 : n089.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 4.76s % Output : Proof 4.76s % 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 : NUM765^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.23 % Computer : n089.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:01:48 CST 2018 % 0.02/0.23 % CPUTime : % 0.07/0.28 Python 2.7.13 % 0.31/0.75 Using paths ['/home/cristobal/cocATP/CASC/TPTP/', '/export/starexec/sandbox2/benchmark/', '/export/starexec/sandbox2/benchmark/'] % 0.31/0.75 FOF formula (<kernel.Constant object at 0x2b08af5266c8>, <kernel.Type object at 0x2b08af526248>) of role type named frac_type % 0.31/0.75 Using role type % 0.31/0.75 Declaring frac:Type % 0.31/0.75 FOF formula (<kernel.Constant object at 0x2b08af4fcf80>, <kernel.Constant object at 0x2b08af5262d8>) of role type named x % 0.31/0.75 Using role type % 0.31/0.75 Declaring x:frac % 0.31/0.75 FOF formula (<kernel.Constant object at 0x2b08af526758>, <kernel.Constant object at 0x2b08af5262d8>) of role type named y % 0.31/0.75 Using role type % 0.31/0.75 Declaring y:frac % 0.31/0.75 FOF formula (<kernel.Constant object at 0x2b08af5266c8>, <kernel.Constant object at 0x2b08af5262d8>) of role type named z % 0.31/0.75 Using role type % 0.31/0.75 Declaring z:frac % 0.31/0.75 FOF formula (<kernel.Constant object at 0x2b08af526320>, <kernel.Constant object at 0x2b08af5262d8>) of role type named u % 0.31/0.75 Using role type % 0.31/0.75 Declaring u:frac % 0.31/0.75 FOF formula (<kernel.Constant object at 0x2b08af526758>, <kernel.DependentProduct object at 0x2b08af51f488>) of role type named moref % 0.31/0.75 Using role type % 0.31/0.75 Declaring moref:(frac->(frac->Prop)) % 0.31/0.75 FOF formula (<kernel.Constant object at 0x2b08af526170>, <kernel.DependentProduct object at 0x2b08af51f098>) of role type named eq % 0.31/0.75 Using role type % 0.31/0.75 Declaring _TPTP_eq:(frac->(frac->Prop)) % 0.31/0.75 FOF formula ((((moref x) y)->False)->((_TPTP_eq x) y)) of role axiom named m % 0.31/0.75 A new axiom: ((((moref x) y)->False)->((_TPTP_eq x) y)) % 0.31/0.75 FOF formula ((((moref z) u)->False)->((_TPTP_eq z) u)) of role axiom named n % 0.31/0.75 A new axiom: ((((moref z) u)->False)->((_TPTP_eq z) u)) % 0.31/0.75 FOF formula (<kernel.Constant object at 0x2b08af5266c8>, <kernel.DependentProduct object at 0x2b08af51f878>) of role type named pf % 0.31/0.75 Using role type % 0.31/0.75 Declaring pf:(frac->(frac->frac)) % 0.31/0.75 FOF formula (forall (Xa:Prop), (((Xa->False)->False)->Xa)) of role axiom named et % 0.31/0.75 A new axiom: (forall (Xa:Prop), (((Xa->False)->False)->Xa)) % 0.31/0.75 FOF formula (forall (Xx:frac) (Xy:frac) (Xz:frac) (Xu:frac), (((_TPTP_eq Xx) Xy)->(((_TPTP_eq Xz) Xu)->((_TPTP_eq ((pf Xx) Xz)) ((pf Xy) Xu))))) of role axiom named satz56 % 0.31/0.75 A new axiom: (forall (Xx:frac) (Xy:frac) (Xz:frac) (Xu:frac), (((_TPTP_eq Xx) Xy)->(((_TPTP_eq Xz) Xu)->((_TPTP_eq ((pf Xx) Xz)) ((pf Xy) Xu))))) % 0.31/0.75 FOF formula (forall (Xx:frac) (Xy:frac) (Xz:frac) (Xu:frac), (((moref Xx) Xy)->(((((moref Xz) Xu)->False)->((_TPTP_eq Xz) Xu))->((moref ((pf Xx) Xz)) ((pf Xy) Xu))))) of role axiom named satz65b % 0.31/0.75 A new axiom: (forall (Xx:frac) (Xy:frac) (Xz:frac) (Xu:frac), (((moref Xx) Xy)->(((((moref Xz) Xu)->False)->((_TPTP_eq Xz) Xu))->((moref ((pf Xx) Xz)) ((pf Xy) Xu))))) % 0.31/0.75 FOF formula (forall (Xx:frac) (Xy:frac) (Xz:frac) (Xu:frac), (((((moref Xx) Xy)->False)->((_TPTP_eq Xx) Xy))->(((moref Xz) Xu)->((moref ((pf Xx) Xz)) ((pf Xy) Xu))))) of role axiom named satz65a % 0.31/0.75 A new axiom: (forall (Xx:frac) (Xy:frac) (Xz:frac) (Xu:frac), (((((moref Xx) Xy)->False)->((_TPTP_eq Xx) Xy))->(((moref Xz) Xu)->((moref ((pf Xx) Xz)) ((pf Xy) Xu))))) % 0.31/0.75 FOF formula ((((moref ((pf x) z)) ((pf y) u))->False)->((_TPTP_eq ((pf x) z)) ((pf y) u))) of role conjecture named satz66 % 0.31/0.75 Conjecture to prove = ((((moref ((pf x) z)) ((pf y) u))->False)->((_TPTP_eq ((pf x) z)) ((pf y) u))):Prop % 0.31/0.75 We need to prove ['((((moref ((pf x) z)) ((pf y) u))->False)->((_TPTP_eq ((pf x) z)) ((pf y) u)))'] % 0.31/0.75 Parameter frac:Type. % 0.31/0.75 Parameter x:frac. % 0.31/0.75 Parameter y:frac. % 0.31/0.75 Parameter z:frac. % 0.31/0.75 Parameter u:frac. % 0.31/0.75 Parameter moref:(frac->(frac->Prop)). % 0.31/0.75 Parameter _TPTP_eq:(frac->(frac->Prop)). % 0.31/0.75 Axiom m:((((moref x) y)->False)->((_TPTP_eq x) y)). % 0.31/0.75 Axiom n:((((moref z) u)->False)->((_TPTP_eq z) u)). % 0.31/0.75 Parameter pf:(frac->(frac->frac)). % 0.31/0.75 Axiom et:(forall (Xa:Prop), (((Xa->False)->False)->Xa)). % 0.31/0.75 Axiom satz56:(forall (Xx:frac) (Xy:frac) (Xz:frac) (Xu:frac), (((_TPTP_eq Xx) Xy)->(((_TPTP_eq Xz) Xu)->((_TPTP_eq ((pf Xx) Xz)) ((pf Xy) Xu))))). % 0.31/0.75 Axiom satz65b:(forall (Xx:frac) (Xy:frac) (Xz:frac) (Xu:frac), (((moref Xx) Xy)->(((((moref Xz) Xu)->False)->((_TPTP_eq Xz) Xu))->((moref ((pf Xx) Xz)) ((pf Xy) Xu))))). % 0.31/0.75 Axiom satz65a:(forall (Xx:frac) (Xy:frac) (Xz:frac) (Xu:frac), (((((moref Xx) Xy)->False)->((_TPTP_eq Xx) Xy))->(((moref Xz) Xu)->((moref ((pf Xx) Xz)) ((pf Xy) Xu))))). % 4.68/5.09 Trying to prove ((((moref ((pf x) z)) ((pf y) u))->False)->((_TPTP_eq ((pf x) z)) ((pf y) u))) % 4.68/5.09 Found n:((((moref z) u)->False)->((_TPTP_eq z) u)) % 4.68/5.09 Found n as proof of ((((moref z) u)->False)->((_TPTP_eq z) u)) % 4.68/5.09 Found m:((((moref x) y)->False)->((_TPTP_eq x) y)) % 4.68/5.09 Found m as proof of ((((moref x) y)->False)->((_TPTP_eq x) y)) % 4.68/5.09 Found n:((((moref z) u)->False)->((_TPTP_eq z) u)) % 4.68/5.09 Found n as proof of ((((moref z) u)->False)->((_TPTP_eq z) u)) % 4.68/5.09 Found m:((((moref x) y)->False)->((_TPTP_eq x) y)) % 4.68/5.09 Found m as proof of ((((moref x) y)->False)->((_TPTP_eq x) y)) % 4.68/5.09 Found x00:False % 4.68/5.09 Found (fun (x01:(((_TPTP_eq ((pf x) z)) ((pf y) u))->False))=> x00) as proof of False % 4.68/5.09 Found (fun (x01:(((_TPTP_eq ((pf x) z)) ((pf y) u))->False))=> x00) as proof of ((((_TPTP_eq ((pf x) z)) ((pf y) u))->False)->False) % 4.68/5.09 Found n:((((moref z) u)->False)->((_TPTP_eq z) u)) % 4.68/5.09 Found n as proof of ((((moref z) u)->False)->((_TPTP_eq z) u)) % 4.68/5.09 Found m:((((moref x) y)->False)->((_TPTP_eq x) y)) % 4.68/5.09 Found m as proof of ((((moref x) y)->False)->((_TPTP_eq x) y)) % 4.68/5.09 Found x00:False % 4.68/5.09 Found (fun (x01:(((_TPTP_eq ((pf x) z)) ((pf y) u))->False))=> x00) as proof of False % 4.68/5.09 Found (fun (x01:(((_TPTP_eq ((pf x) z)) ((pf y) u))->False))=> x00) as proof of ((((_TPTP_eq ((pf x) z)) ((pf y) u))->False)->False) % 4.68/5.09 Found (et0 (fun (x01:(((_TPTP_eq ((pf x) z)) ((pf y) u))->False))=> x00)) as proof of ((_TPTP_eq ((pf x) z)) ((pf y) u)) % 4.68/5.09 Found ((et ((_TPTP_eq ((pf x) z)) ((pf y) u))) (fun (x01:(((_TPTP_eq ((pf x) z)) ((pf y) u))->False))=> x00)) as proof of ((_TPTP_eq ((pf x) z)) ((pf y) u)) % 4.68/5.09 Found ((et ((_TPTP_eq ((pf x) z)) ((pf y) u))) (fun (x01:(((_TPTP_eq ((pf x) z)) ((pf y) u))->False))=> x00)) as proof of ((_TPTP_eq ((pf x) z)) ((pf y) u)) % 4.68/5.09 Found n:((((moref z) u)->False)->((_TPTP_eq z) u)) % 4.68/5.09 Found n as proof of ((((moref z) u)->False)->((_TPTP_eq z) u)) % 4.68/5.09 Found m:((((moref x) y)->False)->((_TPTP_eq x) y)) % 4.68/5.09 Found m as proof of ((((moref x) y)->False)->((_TPTP_eq x) y)) % 4.68/5.09 Found satz65a000000:=(satz65a00000 x1):((moref ((pf x) z)) ((pf y) u)) % 4.68/5.09 Found (satz65a00000 x1) as proof of ((moref ((pf x) z)) ((pf y) u)) % 4.68/5.09 Found ((satz65a0000 u) x1) as proof of ((moref ((pf x) z)) ((pf y) u)) % 4.68/5.09 Found (((satz65a000 z) u) x1) as proof of ((moref ((pf x) z)) ((pf y) u)) % 4.68/5.09 Found ((((fun (Xz:frac) (Xu:frac)=> (((satz65a00 Xz) Xu) m)) z) u) x1) as proof of ((moref ((pf x) z)) ((pf y) u)) % 4.68/5.09 Found ((((fun (Xz:frac) (Xu:frac)=> ((((satz65a0 y) Xz) Xu) m)) z) u) x1) as proof of ((moref ((pf x) z)) ((pf y) u)) % 4.68/5.09 Found ((((fun (Xz:frac) (Xu:frac)=> (((((satz65a x) y) Xz) Xu) m)) z) u) x1) as proof of ((moref ((pf x) z)) ((pf y) u)) % 4.68/5.09 Found ((((fun (Xz:frac) (Xu:frac)=> (((((satz65a x) y) Xz) Xu) m)) z) u) x1) as proof of ((moref ((pf x) z)) ((pf y) u)) % 4.68/5.09 Found (x0 ((((fun (Xz:frac) (Xu:frac)=> (((((satz65a x) y) Xz) Xu) m)) z) u) x1)) as proof of False % 4.68/5.09 Found (fun (x1:((moref z) u))=> (x0 ((((fun (Xz:frac) (Xu:frac)=> (((((satz65a x) y) Xz) Xu) m)) z) u) x1))) as proof of False % 4.68/5.09 Found (fun (x1:((moref z) u))=> (x0 ((((fun (Xz:frac) (Xu:frac)=> (((((satz65a x) y) Xz) Xu) m)) z) u) x1))) as proof of (((moref z) u)->False) % 4.68/5.09 Found (n (fun (x1:((moref z) u))=> (x0 ((((fun (Xz:frac) (Xu:frac)=> (((((satz65a x) y) Xz) Xu) m)) z) u) x1)))) as proof of ((_TPTP_eq z) u) % 4.68/5.09 Found (n (fun (x1:((moref z) u))=> (x0 ((((fun (Xz:frac) (Xu:frac)=> (((((satz65a x) y) Xz) Xu) m)) z) u) x1)))) as proof of ((_TPTP_eq z) u) % 4.68/5.09 Found satz65b000000:=(satz65b00000 n):((moref ((pf x) z)) ((pf y) u)) % 4.68/5.09 Found (satz65b00000 n) as proof of ((moref ((pf x) z)) ((pf y) u)) % 4.68/5.09 Found ((satz65b0000 u) n) as proof of ((moref ((pf x) z)) ((pf y) u)) % 4.68/5.09 Found (((satz65b000 z) u) n) as proof of ((moref ((pf x) z)) ((pf y) u)) % 4.68/5.09 Found ((((fun (Xz:frac) (Xu:frac)=> (((satz65b00 Xz) Xu) x1)) z) u) n) as proof of ((moref ((pf x) z)) ((pf y) u)) % 4.68/5.09 Found ((((fun (Xz:frac) (Xu:frac)=> ((((satz65b0 y) Xz) Xu) x1)) z) u) n) as proof of ((moref ((pf x) z)) ((pf y) u)) % 4.68/5.09 Found ((((fun (Xz:frac) (Xu:frac)=> (((((satz65b x) y) Xz) Xu) x1)) z) u) n) as proof of ((moref ((pf x) z)) ((pf y) u)) % 4.68/5.09 Found ((((fun (Xz:frac) (Xu:frac)=> (((((satz65b x) y) Xz) Xu) x1)) z) u) n) as proof of ((moref ((pf x) z)) ((pf y) u)) % 4.68/5.09 Found (x0 ((((fun (Xz:frac) (Xu:frac)=> (((((satz65b x) y) Xz) Xu) x1)) z) u) n)) as proof of False % 4.76/5.17 Found (fun (x1:((moref x) y))=> (x0 ((((fun (Xz:frac) (Xu:frac)=> (((((satz65b x) y) Xz) Xu) x1)) z) u) n))) as proof of False % 4.76/5.17 Found (fun (x1:((moref x) y))=> (x0 ((((fun (Xz:frac) (Xu:frac)=> (((((satz65b x) y) Xz) Xu) x1)) z) u) n))) as proof of (((moref x) y)->False) % 4.76/5.17 Found (m (fun (x1:((moref x) y))=> (x0 ((((fun (Xz:frac) (Xu:frac)=> (((((satz65b x) y) Xz) Xu) x1)) z) u) n)))) as proof of ((_TPTP_eq x) y) % 4.76/5.17 Found (m (fun (x1:((moref x) y))=> (x0 ((((fun (Xz:frac) (Xu:frac)=> (((((satz65b x) y) Xz) Xu) x1)) z) u) n)))) as proof of ((_TPTP_eq x) y) % 4.76/5.17 Found ((satz560000 (m (fun (x1:((moref x) y))=> (x0 ((((fun (Xz:frac) (Xu:frac)=> (((((satz65b x) y) Xz) Xu) x1)) z) u) n))))) (n (fun (x1:((moref z) u))=> (x0 ((((fun (Xz:frac) (Xu:frac)=> (((((satz65a x) y) Xz) Xu) m)) z) u) x1))))) as proof of ((_TPTP_eq ((pf x) z)) ((pf y) u)) % 4.76/5.17 Found (((satz56000 u) (m (fun (x1:((moref x) y))=> (x0 ((((fun (Xz:frac) (Xu:frac)=> (((((satz65b x) y) Xz) Xu) x1)) z) u) n))))) (n (fun (x1:((moref z) u))=> (x0 ((((fun (Xz:frac) (Xu:frac)=> (((((satz65a x) y) Xz) Xu) m)) z) u) x1))))) as proof of ((_TPTP_eq ((pf x) z)) ((pf y) u)) % 4.76/5.17 Found ((((satz5600 z) u) (m (fun (x1:((moref x) y))=> (x0 ((((fun (Xz:frac) (Xu:frac)=> (((((satz65b x) y) Xz) Xu) x1)) z) u) n))))) (n (fun (x1:((moref z) u))=> (x0 ((((fun (Xz:frac) (Xu:frac)=> (((((satz65a x) y) Xz) Xu) m)) z) u) x1))))) as proof of ((_TPTP_eq ((pf x) z)) ((pf y) u)) % 4.76/5.17 Found (((((satz560 y) z) u) (m (fun (x1:((moref x) y))=> (x0 ((((fun (Xz:frac) (Xu:frac)=> (((((satz65b x) y) Xz) Xu) x1)) z) u) n))))) (n (fun (x1:((moref z) u))=> (x0 ((((fun (Xz:frac) (Xu:frac)=> (((((satz65a x) y) Xz) Xu) m)) z) u) x1))))) as proof of ((_TPTP_eq ((pf x) z)) ((pf y) u)) % 4.76/5.17 Found ((((((satz56 x) y) z) u) (m (fun (x1:((moref x) y))=> (x0 ((((fun (Xz:frac) (Xu:frac)=> (((((satz65b x) y) Xz) Xu) x1)) z) u) n))))) (n (fun (x1:((moref z) u))=> (x0 ((((fun (Xz:frac) (Xu:frac)=> (((((satz65a x) y) Xz) Xu) m)) z) u) x1))))) as proof of ((_TPTP_eq ((pf x) z)) ((pf y) u)) % 4.76/5.17 Found (fun (x0:(((moref ((pf x) z)) ((pf y) u))->False))=> ((((((satz56 x) y) z) u) (m (fun (x1:((moref x) y))=> (x0 ((((fun (Xz:frac) (Xu:frac)=> (((((satz65b x) y) Xz) Xu) x1)) z) u) n))))) (n (fun (x1:((moref z) u))=> (x0 ((((fun (Xz:frac) (Xu:frac)=> (((((satz65a x) y) Xz) Xu) m)) z) u) x1)))))) as proof of ((_TPTP_eq ((pf x) z)) ((pf y) u)) % 4.76/5.17 Found (fun (x0:(((moref ((pf x) z)) ((pf y) u))->False))=> ((((((satz56 x) y) z) u) (m (fun (x1:((moref x) y))=> (x0 ((((fun (Xz:frac) (Xu:frac)=> (((((satz65b x) y) Xz) Xu) x1)) z) u) n))))) (n (fun (x1:((moref z) u))=> (x0 ((((fun (Xz:frac) (Xu:frac)=> (((((satz65a x) y) Xz) Xu) m)) z) u) x1)))))) as proof of ((((moref ((pf x) z)) ((pf y) u))->False)->((_TPTP_eq ((pf x) z)) ((pf y) u))) % 4.76/5.17 Got proof (fun (x0:(((moref ((pf x) z)) ((pf y) u))->False))=> ((((((satz56 x) y) z) u) (m (fun (x1:((moref x) y))=> (x0 ((((fun (Xz:frac) (Xu:frac)=> (((((satz65b x) y) Xz) Xu) x1)) z) u) n))))) (n (fun (x1:((moref z) u))=> (x0 ((((fun (Xz:frac) (Xu:frac)=> (((((satz65a x) y) Xz) Xu) m)) z) u) x1)))))) % 4.76/5.17 Time elapsed = 4.318228s % 4.76/5.17 node=982 cost=340.000000 depth=18 % 4.76/5.17:::::::::::::::::::::: % 4.76/5.17 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 4.76/5.17 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p % 4.76/5.17 (fun (x0:(((moref ((pf x) z)) ((pf y) u))->False))=> ((((((satz56 x) y) z) u) (m (fun (x1:((moref x) y))=> (x0 ((((fun (Xz:frac) (Xu:frac)=> (((((satz65b x) y) Xz) Xu) x1)) z) u) n))))) (n (fun (x1:((moref z) u))=> (x0 ((((fun (Xz:frac) (Xu:frac)=> (((((satz65a x) y) Xz) Xu) m)) z) u) x1)))))) % 4.76/5.17 % SZS output end Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p %------------------------------------------------------------------------------