%------------------------------------------------------------------------------ % File : cocATP---0.2.0 % Problem : NUM746^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 : n106.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:36 EST 2018 % Result : Theorem 7.59s % Output : Proof 7.59s % 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 : NUM746^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.23 % Computer : n106.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 13:28:34 CST 2018 % 0.02/0.23 % CPUTime : % 0.02/0.25 Python 2.7.13 % 2.35/2.54 Using paths ['/home/cristobal/cocATP/CASC/TPTP/', '/export/starexec/sandbox/benchmark/', '/export/starexec/sandbox/benchmark/'] % 2.35/2.54 FOF formula (<kernel.Constant object at 0x2b74d67764d0>, <kernel.Type object at 0x2b74d67767e8>) of role type named frac_type % 2.35/2.54 Using role type % 2.35/2.54 Declaring frac:Type % 2.35/2.54 FOF formula (<kernel.Constant object at 0x2b74d641d998>, <kernel.Constant object at 0x2b74d6776680>) of role type named x % 2.35/2.54 Using role type % 2.35/2.54 Declaring x:frac % 2.35/2.54 FOF formula (<kernel.Constant object at 0x2b74d6776518>, <kernel.Constant object at 0x2b74d6776680>) of role type named y % 2.35/2.54 Using role type % 2.35/2.54 Declaring y:frac % 2.35/2.54 FOF formula (<kernel.Constant object at 0x2b74d67764d0>, <kernel.Constant object at 0x2b74d6776680>) of role type named z % 2.35/2.54 Using role type % 2.35/2.54 Declaring z:frac % 2.35/2.54 FOF formula (<kernel.Constant object at 0x2b74d6776ea8>, <kernel.DependentProduct object at 0x2b74ceadfef0>) of role type named lessf % 2.35/2.54 Using role type % 2.35/2.54 Declaring lessf:(frac->(frac->Prop)) % 2.35/2.54 FOF formula (<kernel.Constant object at 0x2b74d6776518>, <kernel.DependentProduct object at 0x2b74ceadf3b0>) of role type named eq % 2.35/2.54 Using role type % 2.35/2.54 Declaring _TPTP_eq:(frac->(frac->Prop)) % 2.35/2.54 FOF formula ((((lessf x) y)->False)->((_TPTP_eq x) y)) of role axiom named l % 2.35/2.54 A new axiom: ((((lessf x) y)->False)->((_TPTP_eq x) y)) % 2.35/2.54 FOF formula ((((lessf y) z)->False)->((_TPTP_eq y) z)) of role axiom named k % 2.35/2.54 A new axiom: ((((lessf y) z)->False)->((_TPTP_eq y) z)) % 2.35/2.54 FOF formula (forall (Xa:Prop), (((Xa->False)->False)->Xa)) of role axiom named et % 2.35/2.54 A new axiom: (forall (Xa:Prop), (((Xa->False)->False)->Xa)) % 2.35/2.54 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 % 2.35/2.54 A new axiom: (forall (Xx:frac) (Xy:frac) (Xz:frac), (((_TPTP_eq Xx) Xy)->(((_TPTP_eq Xy) Xz)->((_TPTP_eq Xx) Xz)))) % 2.35/2.54 FOF formula (forall (Xx:frac) (Xy:frac) (Xz:frac), (((lessf Xx) Xy)->(((((lessf Xy) Xz)->False)->((_TPTP_eq Xy) Xz))->((lessf Xx) Xz)))) of role axiom named satz51b % 2.35/2.54 A new axiom: (forall (Xx:frac) (Xy:frac) (Xz:frac), (((lessf Xx) Xy)->(((((lessf Xy) Xz)->False)->((_TPTP_eq Xy) Xz))->((lessf Xx) Xz)))) % 2.35/2.54 FOF formula (forall (Xx:frac) (Xy:frac) (Xz:frac), (((((lessf Xx) Xy)->False)->((_TPTP_eq Xx) Xy))->(((lessf Xy) Xz)->((lessf Xx) Xz)))) of role axiom named satz51a % 2.35/2.54 A new axiom: (forall (Xx:frac) (Xy:frac) (Xz:frac), (((((lessf Xx) Xy)->False)->((_TPTP_eq Xx) Xy))->(((lessf Xy) Xz)->((lessf Xx) Xz)))) % 2.35/2.54 FOF formula ((((lessf x) z)->False)->((_TPTP_eq x) z)) of role conjecture named satz52 % 2.35/2.54 Conjecture to prove = ((((lessf x) z)->False)->((_TPTP_eq x) z)):Prop % 2.35/2.54 We need to prove ['((((lessf x) z)->False)->((_TPTP_eq x) z))'] % 2.35/2.54 Parameter frac:Type. % 2.35/2.54 Parameter x:frac. % 2.35/2.54 Parameter y:frac. % 2.35/2.54 Parameter z:frac. % 2.35/2.54 Parameter lessf:(frac->(frac->Prop)). % 2.35/2.54 Parameter _TPTP_eq:(frac->(frac->Prop)). % 2.35/2.54 Axiom l:((((lessf x) y)->False)->((_TPTP_eq x) y)). % 2.35/2.54 Axiom k:((((lessf y) z)->False)->((_TPTP_eq y) z)). % 2.35/2.54 Axiom et:(forall (Xa:Prop), (((Xa->False)->False)->Xa)). % 2.35/2.54 Axiom satz39:(forall (Xx:frac) (Xy:frac) (Xz:frac), (((_TPTP_eq Xx) Xy)->(((_TPTP_eq Xy) Xz)->((_TPTP_eq Xx) Xz)))). % 2.35/2.54 Axiom satz51b:(forall (Xx:frac) (Xy:frac) (Xz:frac), (((lessf Xx) Xy)->(((((lessf Xy) Xz)->False)->((_TPTP_eq Xy) Xz))->((lessf Xx) Xz)))). % 2.35/2.54 Axiom satz51a:(forall (Xx:frac) (Xy:frac) (Xz:frac), (((((lessf Xx) Xy)->False)->((_TPTP_eq Xx) Xy))->(((lessf Xy) Xz)->((lessf Xx) Xz)))). % 2.35/2.54 Trying to prove ((((lessf x) z)->False)->((_TPTP_eq x) z)) % 2.35/2.54 Found k:((((lessf y) z)->False)->((_TPTP_eq y) z)) % 2.35/2.54 Found k as proof of ((((lessf y) z)->False)->((_TPTP_eq y) z)) % 2.35/2.54 Found l:((((lessf x) y)->False)->((_TPTP_eq x) y)) % 2.35/2.54 Found l as proof of ((((lessf x) y)->False)->((_TPTP_eq x) y)) % 2.35/2.54 Found k:((((lessf y) z)->False)->((_TPTP_eq y) z)) % 2.35/2.54 Found k as proof of ((((lessf y) z)->False)->((_TPTP_eq y) z)) % 2.35/2.54 Found l:((((lessf x) y)->False)->((_TPTP_eq x) y)) % 2.35/2.54 Found l as proof of ((((lessf x) y)->False)->((_TPTP_eq x) y)) % 2.35/2.54 Found x00:False % 2.35/2.54 Found (fun (x01:(((_TPTP_eq x) z)->False))=> x00) as proof of False % 2.35/2.54 Found (fun (x01:(((_TPTP_eq x) z)->False))=> x00) as proof of ((((_TPTP_eq x) z)->False)->False) % 2.35/2.54 Found x00:False % 2.35/2.54 Found (fun (x01:(((_TPTP_eq x) z)->False))=> x00) as proof of False % 7.29/7.47 Found (fun (x01:(((_TPTP_eq x) z)->False))=> x00) as proof of ((((_TPTP_eq x) z)->False)->False) % 7.29/7.47 Found (et0 (fun (x01:(((_TPTP_eq x) z)->False))=> x00)) as proof of ((_TPTP_eq x) z) % 7.29/7.47 Found ((et ((_TPTP_eq x) z)) (fun (x01:(((_TPTP_eq x) z)->False))=> x00)) as proof of ((_TPTP_eq x) z) % 7.29/7.47 Found ((et ((_TPTP_eq x) z)) (fun (x01:(((_TPTP_eq x) z)->False))=> x00)) as proof of ((_TPTP_eq x) z) % 7.29/7.47 Found k:((((lessf y) z)->False)->((_TPTP_eq y) z)) % 7.29/7.47 Found k as proof of ((((lessf y) z)->False)->((_TPTP_eq y) z)) % 7.29/7.47 Found k0:((_TPTP_eq y) z) % 7.29/7.47 Instantiate: Xy:=y:frac % 7.29/7.47 Found k0 as proof of ((_TPTP_eq Xy) z) % 7.29/7.47 Found l0:((_TPTP_eq x) y) % 7.29/7.47 Instantiate: Xy:=y:frac % 7.29/7.47 Found l0 as proof of ((_TPTP_eq x) Xy) % 7.29/7.47 Found k:((((lessf y) z)->False)->((_TPTP_eq y) z)) % 7.29/7.47 Found k as proof of ((((lessf y) z)->False)->((_TPTP_eq y) z)) % 7.29/7.47 Found l:((((lessf x) y)->False)->((_TPTP_eq x) y)) % 7.29/7.47 Found l as proof of ((((lessf x) y)->False)->((_TPTP_eq x) y)) % 7.29/7.47 Found k:((((lessf y) z)->False)->((_TPTP_eq y) z)) % 7.29/7.47 Found k as proof of ((((lessf y) z)->False)->((_TPTP_eq y) z)) % 7.29/7.47 Found l:((((lessf x) y)->False)->((_TPTP_eq x) y)) % 7.29/7.47 Found l as proof of ((((lessf x) y)->False)->((_TPTP_eq x) y)) % 7.29/7.47 Found k0:((_TPTP_eq y) z) % 7.29/7.47 Instantiate: Xy:=y:frac % 7.29/7.47 Found k0 as proof of ((_TPTP_eq Xy) z) % 7.29/7.47 Found l0:((_TPTP_eq x) y) % 7.29/7.47 Instantiate: Xy:=y:frac % 7.29/7.47 Found l0 as proof of ((_TPTP_eq x) Xy) % 7.29/7.47 Found k:((((lessf y) z)->False)->((_TPTP_eq y) z)) % 7.29/7.47 Found k as proof of ((((lessf y) z)->False)->((_TPTP_eq y) z)) % 7.29/7.47 Found l:((((lessf x) y)->False)->((_TPTP_eq x) y)) % 7.29/7.47 Found l as proof of ((((lessf x) y)->False)->((_TPTP_eq x) y)) % 7.29/7.47 Found l:((((lessf x) y)->False)->((_TPTP_eq x) y)) % 7.29/7.47 Found l as proof of ((((lessf x) y)->False)->((_TPTP_eq x) y)) % 7.29/7.47 Found l0:((_TPTP_eq x) y) % 7.29/7.47 Instantiate: Xy:=y:frac % 7.29/7.47 Found l0 as proof of ((_TPTP_eq x) Xy) % 7.29/7.47 Found k0:((_TPTP_eq y) z) % 7.29/7.47 Instantiate: Xy:=y:frac % 7.29/7.47 Found k0 as proof of ((_TPTP_eq Xy) z) % 7.29/7.47 Found k:((((lessf y) z)->False)->((_TPTP_eq y) z)) % 7.29/7.47 Found k as proof of ((((lessf y) z)->False)->((_TPTP_eq y) z)) % 7.29/7.47 Found l:((((lessf x) y)->False)->((_TPTP_eq x) y)) % 7.29/7.47 Found l as proof of ((((lessf x) y)->False)->((_TPTP_eq x) y)) % 7.29/7.47 Found k0:((_TPTP_eq y) z) % 7.29/7.47 Instantiate: Xy:=y:frac % 7.29/7.47 Found k0 as proof of ((_TPTP_eq Xy) z) % 7.29/7.47 Found l0:((_TPTP_eq x) y) % 7.29/7.47 Instantiate: Xy:=y:frac % 7.29/7.47 Found l0 as proof of ((_TPTP_eq x) Xy) % 7.29/7.47 Found k:((((lessf y) z)->False)->((_TPTP_eq y) z)) % 7.29/7.47 Found k as proof of ((((lessf y) z)->False)->((_TPTP_eq y) z)) % 7.29/7.47 Found l:((((lessf x) y)->False)->((_TPTP_eq x) y)) % 7.29/7.47 Found l as proof of ((((lessf x) y)->False)->((_TPTP_eq x) y)) % 7.29/7.47 Found k0:((_TPTP_eq y) z) % 7.29/7.47 Instantiate: Xy:=y:frac % 7.29/7.47 Found k0 as proof of ((_TPTP_eq Xy) z) % 7.29/7.47 Found l0:((_TPTP_eq x) y) % 7.29/7.47 Instantiate: Xy:=y:frac % 7.29/7.47 Found l0 as proof of ((_TPTP_eq x) Xy) % 7.29/7.47 Found l0:((_TPTP_eq x) y) % 7.29/7.47 Instantiate: Xy:=y:frac % 7.29/7.47 Found l0 as proof of ((_TPTP_eq x) Xy) % 7.29/7.47 Found k0:((_TPTP_eq y) z) % 7.29/7.47 Instantiate: Xy:=y:frac % 7.29/7.47 Found k0 as proof of ((_TPTP_eq Xy) z) % 7.29/7.47 Found x00:False % 7.29/7.47 Found (fun (x1:((lessf y) z))=> x00) as proof of False % 7.29/7.47 Found (fun (x1:((lessf y) z))=> x00) as proof of (((lessf y) z)->False) % 7.29/7.47 Found x00:False % 7.29/7.47 Found (fun (x1:((lessf x) y))=> x00) as proof of False % 7.29/7.47 Found (fun (x1:((lessf x) y))=> x00) as proof of (((lessf x) y)->False) % 7.29/7.47 Found x00:False % 7.29/7.47 Found (fun (x1:(((_TPTP_eq Xy) z)->False))=> x00) as proof of False % 7.29/7.47 Found (fun (x1:(((_TPTP_eq Xy) z)->False))=> x00) as proof of ((((_TPTP_eq Xy) z)->False)->False) % 7.29/7.47 Found x00:False % 7.29/7.47 Found (fun (x01:(((_TPTP_eq x) Xy)->False))=> x00) as proof of False % 7.29/7.47 Found (fun (x01:(((_TPTP_eq x) Xy)->False))=> x00) as proof of ((((_TPTP_eq x) Xy)->False)->False) % 7.29/7.47 Found satz51a00000:=(satz51a0000 x1):((lessf x) z) % 7.29/7.47 Found (satz51a0000 x1) as proof of ((lessf x) z) % 7.29/7.47 Found ((satz51a000 l) x1) as proof of ((lessf x) z) % 7.29/7.47 Found (((satz51a00 y) l) x1) as proof of ((lessf x) z) % 7.29/7.47 Found ((((fun (Xy0:frac)=> ((satz51a0 Xy0) z)) y) l) x1) as proof of ((lessf x) z) % 7.29/7.47 Found ((((fun (Xy0:frac)=> (((satz51a x) Xy0) z)) y) l) x1) as proof of ((lessf x) z) % 7.29/7.47 Found ((((fun (Xy0:frac)=> (((satz51a x) Xy0) z)) y) l) x1) as proof of ((lessf x) z) % 7.29/7.47 Found (x0 ((((fun (Xy0:frac)=> (((satz51a x) Xy0) z)) y) l) x1)) as proof of False % 7.29/7.47 Found (fun (x1:((lessf y) z))=> (x0 ((((fun (Xy0:frac)=> (((satz51a x) Xy0) z)) y) l) x1))) as proof of False % 7.59/7.78 Found (fun (x1:((lessf y) z))=> (x0 ((((fun (Xy0:frac)=> (((satz51a x) Xy0) z)) y) l) x1))) as proof of (((lessf y) z)->False) % 7.59/7.78 Found (k (fun (x1:((lessf y) z))=> (x0 ((((fun (Xy0:frac)=> (((satz51a x) Xy0) z)) y) l) x1)))) as proof of ((_TPTP_eq Xy) z) % 7.59/7.78 Found (k (fun (x1:((lessf y) z))=> (x0 ((((fun (Xy0:frac)=> (((satz51a x) Xy0) z)) y) l) x1)))) as proof of ((_TPTP_eq Xy) z) % 7.59/7.78 Found (k (fun (x1:((lessf y) z))=> (x0 ((((fun (Xy0:frac)=> (((satz51a x) Xy0) z)) y) l) x1)))) as proof of ((_TPTP_eq Xy) z) % 7.59/7.78 Found satz51b00000:=(satz51b0000 k):((lessf x) z) % 7.59/7.78 Found (satz51b0000 k) as proof of ((lessf x) z) % 7.59/7.78 Found ((satz51b000 x1) k) as proof of ((lessf x) z) % 7.59/7.78 Found (((satz51b00 y) x1) k) as proof of ((lessf x) z) % 7.59/7.78 Found ((((fun (Xy0:frac)=> ((satz51b0 Xy0) z)) y) x1) k) as proof of ((lessf x) z) % 7.59/7.78 Found ((((fun (Xy0:frac)=> (((satz51b x) Xy0) z)) y) x1) k) as proof of ((lessf x) z) % 7.59/7.78 Found ((((fun (Xy0:frac)=> (((satz51b x) Xy0) z)) y) x1) k) as proof of ((lessf x) z) % 7.59/7.78 Found (x0 ((((fun (Xy0:frac)=> (((satz51b x) Xy0) z)) y) x1) k)) as proof of False % 7.59/7.78 Found (fun (x1:((lessf x) y))=> (x0 ((((fun (Xy0:frac)=> (((satz51b x) Xy0) z)) y) x1) k))) as proof of False % 7.59/7.78 Found (fun (x1:((lessf x) y))=> (x0 ((((fun (Xy0:frac)=> (((satz51b x) Xy0) z)) y) x1) k))) as proof of (((lessf x) y)->False) % 7.59/7.78 Found (l (fun (x1:((lessf x) y))=> (x0 ((((fun (Xy0:frac)=> (((satz51b x) Xy0) z)) y) x1) k)))) as proof of ((_TPTP_eq x) Xy) % 7.59/7.78 Found (l (fun (x1:((lessf x) y))=> (x0 ((((fun (Xy0:frac)=> (((satz51b x) Xy0) z)) y) x1) k)))) as proof of ((_TPTP_eq x) Xy) % 7.59/7.78 Found (l (fun (x1:((lessf x) y))=> (x0 ((((fun (Xy0:frac)=> (((satz51b x) Xy0) z)) y) x1) k)))) as proof of ((_TPTP_eq x) Xy) % 7.59/7.78 Found ((satz39000 (l (fun (x1:((lessf x) y))=> (x0 ((((fun (Xy0:frac)=> (((satz51b x) Xy0) z)) y) x1) k))))) (k (fun (x1:((lessf y) z))=> (x0 ((((fun (Xy0:frac)=> (((satz51a x) Xy0) z)) y) l) x1))))) as proof of ((_TPTP_eq x) z) % 7.59/7.78 Found (((satz3900 y) (l (fun (x1:((lessf x) y))=> (x0 ((((fun (Xy0:frac)=> (((satz51b x) Xy0) z)) y) x1) k))))) (k (fun (x1:((lessf y) z))=> (x0 ((((fun (Xy0:frac)=> (((satz51a x) Xy0) z)) y) l) x1))))) as proof of ((_TPTP_eq x) z) % 7.59/7.78 Found ((((fun (Xy:frac)=> ((satz390 Xy) z)) y) (l (fun (x1:((lessf x) y))=> (x0 ((((fun (Xy0:frac)=> (((satz51b x) Xy0) z)) y) x1) k))))) (k (fun (x1:((lessf y) z))=> (x0 ((((fun (Xy0:frac)=> (((satz51a x) Xy0) z)) y) l) x1))))) as proof of ((_TPTP_eq x) z) % 7.59/7.78 Found ((((fun (Xy:frac)=> (((satz39 x) Xy) z)) y) (l (fun (x1:((lessf x) y))=> (x0 ((((fun (Xy0:frac)=> (((satz51b x) Xy0) z)) y) x1) k))))) (k (fun (x1:((lessf y) z))=> (x0 ((((fun (Xy0:frac)=> (((satz51a x) Xy0) z)) y) l) x1))))) as proof of ((_TPTP_eq x) z) % 7.59/7.78 Found (fun (x0:(((lessf x) z)->False))=> ((((fun (Xy:frac)=> (((satz39 x) Xy) z)) y) (l (fun (x1:((lessf x) y))=> (x0 ((((fun (Xy0:frac)=> (((satz51b x) Xy0) z)) y) x1) k))))) (k (fun (x1:((lessf y) z))=> (x0 ((((fun (Xy0:frac)=> (((satz51a x) Xy0) z)) y) l) x1)))))) as proof of ((_TPTP_eq x) z) % 7.59/7.78 Found (fun (x0:(((lessf x) z)->False))=> ((((fun (Xy:frac)=> (((satz39 x) Xy) z)) y) (l (fun (x1:((lessf x) y))=> (x0 ((((fun (Xy0:frac)=> (((satz51b x) Xy0) z)) y) x1) k))))) (k (fun (x1:((lessf y) z))=> (x0 ((((fun (Xy0:frac)=> (((satz51a x) Xy0) z)) y) l) x1)))))) as proof of ((((lessf x) z)->False)->((_TPTP_eq x) z)) % 7.59/7.78 Got proof (fun (x0:(((lessf x) z)->False))=> ((((fun (Xy:frac)=> (((satz39 x) Xy) z)) y) (l (fun (x1:((lessf x) y))=> (x0 ((((fun (Xy0:frac)=> (((satz51b x) Xy0) z)) y) x1) k))))) (k (fun (x1:((lessf y) z))=> (x0 ((((fun (Xy0:frac)=> (((satz51a x) Xy0) z)) y) l) x1)))))) % 7.59/7.78 Time elapsed = 7.236759s % 7.59/7.78 node=2293 cost=733.000000 depth=17 % 7.59/7.78:::::::::::::::::::::: % 7.59/7.78 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 7.59/7.78 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p % 7.59/7.78 (fun (x0:(((lessf x) z)->False))=> ((((fun (Xy:frac)=> (((satz39 x) Xy) z)) y) (l (fun (x1:((lessf x) y))=> (x0 ((((fun (Xy0:frac)=> (((satz51b x) Xy0) z)) y) x1) k))))) (k (fun (x1:((lessf y) z))=> (x0 ((((fun (Xy0:frac)=> (((satz51a x) Xy0) z)) y) l) x1)))))) % 7.59/7.78 % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p %------------------------------------------------------------------------------