%------------------------------------------------------------------------------ % File : cocATP---0.2.0 % Problem : NUM739^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 : n119.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:35 EST 2018 % Result : Theorem 18.63s % Output : Proof 18.63s % 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 : NUM739^1 : TPTP v7.0.0. Released v3.7.0. % 0.00/0.03 % Command : python CASC.py /export/starexec/sandbox/benchmark/theBenchmark.p % 0.03/0.23 % Computer : n119.star.cs.uiowa.edu % 0.03/0.23 % Model : x86_64 x86_64 % 0.03/0.23 % CPU : Intel(R) Xeon(R) CPU E5-2609 0 @ 2.40GHz % 0.03/0.23 % Memory : 32218.625MB % 0.03/0.23 % OS : Linux 3.10.0-693.2.2.el7.x86_64 % 0.03/0.23 % CPULimit : 300 % 0.03/0.23 % DateTime : Fri Jan 5 13:21:34 CST 2018 % 0.03/0.23 % CPUTime : % 0.03/0.25 Python 2.7.13 % 2.05/2.22 Using paths ['/home/cristobal/cocATP/CASC/TPTP/', '/export/starexec/sandbox/benchmark/', '/export/starexec/sandbox/benchmark/'] % 2.05/2.22 FOF formula (<kernel.Constant object at 0x2b02a2b58758>, <kernel.Type object at 0x2b02a2b58ab8>) of role type named frac_type % 2.05/2.22 Using role type % 2.05/2.22 Declaring frac:Type % 2.05/2.22 FOF formula (<kernel.Constant object at 0x2b02a20d40e0>, <kernel.Constant object at 0x2b02a2b58098>) of role type named x % 2.05/2.22 Using role type % 2.05/2.22 Declaring x:frac % 2.05/2.22 FOF formula (<kernel.Constant object at 0x2b02a2b58908>, <kernel.Constant object at 0x2b02a2b58098>) of role type named y % 2.05/2.22 Using role type % 2.05/2.22 Declaring y:frac % 2.05/2.22 FOF formula (<kernel.Constant object at 0x2b02a2b58758>, <kernel.Constant object at 0x2b02a2b58098>) of role type named z % 2.05/2.22 Using role type % 2.05/2.22 Declaring z:frac % 2.05/2.22 FOF formula (<kernel.Constant object at 0x2b02a2b587e8>, <kernel.Constant object at 0x2b02a2b58098>) of role type named u % 2.05/2.22 Using role type % 2.05/2.22 Declaring u:frac % 2.05/2.22 FOF formula (<kernel.Constant object at 0x2b02a2b58908>, <kernel.DependentProduct object at 0x2b02a2b535a8>) of role type named moref % 2.05/2.22 Using role type % 2.05/2.22 Declaring moref:(frac->(frac->Prop)) % 2.05/2.22 FOF formula (<kernel.Constant object at 0x2b02a2b58098>, <kernel.DependentProduct object at 0x2b02a2b53518>) of role type named eq % 2.05/2.22 Using role type % 2.05/2.22 Declaring _TPTP_eq:(frac->(frac->Prop)) % 2.05/2.22 FOF formula ((((moref x) y)->False)->((_TPTP_eq x) y)) of role axiom named m % 2.05/2.22 A new axiom: ((((moref x) y)->False)->((_TPTP_eq x) y)) % 2.05/2.22 FOF formula ((_TPTP_eq x) z) of role axiom named e % 2.05/2.22 A new axiom: ((_TPTP_eq x) z) % 2.05/2.22 FOF formula ((_TPTP_eq y) u) of role axiom named f % 2.05/2.22 A new axiom: ((_TPTP_eq y) u) % 2.05/2.22 FOF formula (forall (Xa:Prop), (((Xa->False)->False)->Xa)) of role axiom named et % 2.05/2.22 A new axiom: (forall (Xa:Prop), (((Xa->False)->False)->Xa)) % 2.05/2.22 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.05/2.22 A new axiom: (forall (Xx:frac) (Xy:frac) (Xz:frac), (((_TPTP_eq Xx) Xy)->(((_TPTP_eq Xy) Xz)->((_TPTP_eq Xx) Xz)))) % 2.05/2.22 FOF formula (forall (Xx:frac) (Xy:frac), (((_TPTP_eq Xx) Xy)->((_TPTP_eq Xy) Xx))) of role axiom named satz38 % 2.05/2.23 A new axiom: (forall (Xx:frac) (Xy:frac), (((_TPTP_eq Xx) Xy)->((_TPTP_eq Xy) Xx))) % 2.05/2.23 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 % 2.05/2.23 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))))) % 2.05/2.23 FOF formula ((((moref z) u)->False)->((_TPTP_eq z) u)) of role conjecture named satz46 % 2.05/2.23 Conjecture to prove = ((((moref z) u)->False)->((_TPTP_eq z) u)):Prop % 2.05/2.23 We need to prove ['((((moref z) u)->False)->((_TPTP_eq z) u))'] % 2.05/2.23 Parameter frac:Type. % 2.05/2.23 Parameter x:frac. % 2.05/2.23 Parameter y:frac. % 2.05/2.23 Parameter z:frac. % 2.05/2.23 Parameter u:frac. % 2.05/2.23 Parameter moref:(frac->(frac->Prop)). % 2.05/2.23 Parameter _TPTP_eq:(frac->(frac->Prop)). % 2.05/2.23 Axiom m:((((moref x) y)->False)->((_TPTP_eq x) y)). % 2.05/2.23 Axiom e:((_TPTP_eq x) z). % 2.05/2.23 Axiom f:((_TPTP_eq y) u). % 2.05/2.23 Axiom et:(forall (Xa:Prop), (((Xa->False)->False)->Xa)). % 2.05/2.23 Axiom satz39:(forall (Xx:frac) (Xy:frac) (Xz:frac), (((_TPTP_eq Xx) Xy)->(((_TPTP_eq Xy) Xz)->((_TPTP_eq Xx) Xz)))). % 2.05/2.23 Axiom satz38:(forall (Xx:frac) (Xy:frac), (((_TPTP_eq Xx) Xy)->((_TPTP_eq Xy) Xx))). % 2.05/2.23 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))))). % 2.05/2.23 Trying to prove ((((moref z) u)->False)->((_TPTP_eq z) u)) % 2.05/2.23 Found f:((_TPTP_eq y) u) % 2.05/2.23 Found f as proof of ((_TPTP_eq y) u) % 2.05/2.23 Found f:((_TPTP_eq y) u) % 2.05/2.23 Found f as proof of ((_TPTP_eq y) u) % 2.05/2.23 Found e:((_TPTP_eq x) z) % 2.05/2.23 Found e as proof of ((_TPTP_eq x) z) % 2.05/2.23 Found e:((_TPTP_eq x) z) % 2.05/2.23 Found e as proof of ((_TPTP_eq x) z) % 2.05/2.23 Found x00:False % 2.05/2.23 Found (fun (x1:(((_TPTP_eq z) u)->False))=> x00) as proof of False % 2.05/2.23 Found (fun (x1:(((_TPTP_eq z) u)->False))=> x00) as proof of ((((_TPTP_eq z) u)->False)->False) % 2.05/2.23 Found x00:False % 2.05/2.23 Found (fun (x1:(((_TPTP_eq u) z)->False))=> x00) as proof of False % 2.05/2.23 Found (fun (x1:(((_TPTP_eq u) z)->False))=> x00) as proof of ((((_TPTP_eq u) z)->False)->False) % 2.05/2.23 Found x00:False % 2.05/2.23 Found (fun (x1:(((_TPTP_eq z) u)->False))=> x00) as proof of False % 5.95/6.14 Found (fun (x1:(((_TPTP_eq z) u)->False))=> x00) as proof of ((((_TPTP_eq z) u)->False)->False) % 5.95/6.14 Found (et0 (fun (x1:(((_TPTP_eq z) u)->False))=> x00)) as proof of ((_TPTP_eq z) u) % 5.95/6.14 Found ((et ((_TPTP_eq z) u)) (fun (x1:(((_TPTP_eq z) u)->False))=> x00)) as proof of ((_TPTP_eq z) u) % 5.95/6.14 Found ((et ((_TPTP_eq z) u)) (fun (x1:(((_TPTP_eq z) u)->False))=> x00)) as proof of ((_TPTP_eq z) u) % 5.95/6.14 Found x00:False % 5.95/6.14 Found (fun (x1:(((_TPTP_eq u) z)->False))=> x00) as proof of False % 5.95/6.14 Found (fun (x1:(((_TPTP_eq u) z)->False))=> x00) as proof of ((((_TPTP_eq u) z)->False)->False) % 5.95/6.14 Found (et0 (fun (x1:(((_TPTP_eq u) z)->False))=> x00)) as proof of ((_TPTP_eq u) z) % 5.95/6.14 Found ((et ((_TPTP_eq u) z)) (fun (x1:(((_TPTP_eq u) z)->False))=> x00)) as proof of ((_TPTP_eq u) z) % 5.95/6.14 Found ((et ((_TPTP_eq u) z)) (fun (x1:(((_TPTP_eq u) z)->False))=> x00)) as proof of ((_TPTP_eq u) z) % 5.95/6.14 Found e:((_TPTP_eq x) z) % 5.95/6.14 Found e as proof of ((_TPTP_eq x) z) % 5.95/6.14 Found e:((_TPTP_eq x) z) % 5.95/6.14 Found e as proof of ((_TPTP_eq x) z) % 5.95/6.14 Found e:((_TPTP_eq x) z) % 5.95/6.14 Found e as proof of ((_TPTP_eq x) z) % 5.95/6.14 Found e:((_TPTP_eq x) z) % 5.95/6.14 Found e as proof of ((_TPTP_eq x) z) % 5.95/6.14 Found x00:False % 5.95/6.14 Found (fun (x1:(((_TPTP_eq z) y)->False))=> x00) as proof of False % 5.95/6.14 Found (fun (x1:(((_TPTP_eq z) y)->False))=> x00) as proof of ((((_TPTP_eq z) y)->False)->False) % 5.95/6.14 Found x00:False % 5.95/6.14 Found (fun (x1:(((_TPTP_eq z) y)->False))=> x00) as proof of False % 5.95/6.14 Found (fun (x1:(((_TPTP_eq z) y)->False))=> x00) as proof of ((((_TPTP_eq z) y)->False)->False) % 5.95/6.14 Found f:((_TPTP_eq y) u) % 5.95/6.14 Instantiate: Xy:=u:frac % 5.95/6.14 Found f as proof of ((_TPTP_eq y) Xy) % 5.95/6.14 Found (satz3800 f) as proof of ((_TPTP_eq Xy) y) % 5.95/6.14 Found ((satz380 Xy) f) as proof of ((_TPTP_eq Xy) y) % 5.95/6.14 Found (((satz38 y) Xy) f) as proof of ((_TPTP_eq Xy) y) % 5.95/6.14 Found (((satz38 y) Xy) f) as proof of ((_TPTP_eq Xy) y) % 5.95/6.14 Found e:((_TPTP_eq x) z) % 5.95/6.14 Instantiate: Xy:=x:frac % 5.95/6.14 Found e as proof of ((_TPTP_eq Xy) z) % 5.95/6.14 Found (satz3800 e) as proof of ((_TPTP_eq z) Xy) % 5.95/6.14 Found ((satz380 z) e) as proof of ((_TPTP_eq z) Xy) % 5.95/6.14 Found (((satz38 Xy) z) e) as proof of ((_TPTP_eq z) Xy) % 5.95/6.14 Found (((satz38 Xy) z) e) as proof of ((_TPTP_eq z) Xy) % 5.95/6.14 Found f:((_TPTP_eq y) u) % 5.95/6.14 Instantiate: Xy:=u:frac % 5.95/6.14 Found f as proof of ((_TPTP_eq y) Xy) % 5.95/6.14 Found (satz3800 f) as proof of ((_TPTP_eq Xy) y) % 5.95/6.14 Found ((satz380 Xy) f) as proof of ((_TPTP_eq Xy) y) % 5.95/6.14 Found (((satz38 y) Xy) f) as proof of ((_TPTP_eq Xy) y) % 5.95/6.14 Found (((satz38 y) Xy) f) as proof of ((_TPTP_eq Xy) y) % 5.95/6.14 Found e:((_TPTP_eq x) z) % 5.95/6.14 Instantiate: Xy:=x:frac % 5.95/6.14 Found e as proof of ((_TPTP_eq Xy) z) % 5.95/6.14 Found (satz3800 e) as proof of ((_TPTP_eq z) Xy) % 5.95/6.14 Found ((satz380 z) e) as proof of ((_TPTP_eq z) Xy) % 5.95/6.14 Found (((satz38 Xy) z) e) as proof of ((_TPTP_eq z) Xy) % 5.95/6.14 Found (((satz38 Xy) z) e) as proof of ((_TPTP_eq z) Xy) % 5.95/6.14 Found x00:False % 5.95/6.14 Found (fun (x1:(((_TPTP_eq y) z)->False))=> x00) as proof of False % 5.95/6.14 Found (fun (x1:(((_TPTP_eq y) z)->False))=> x00) as proof of ((((_TPTP_eq y) z)->False)->False) % 5.95/6.14 Found x00:False % 5.95/6.14 Found (fun (x01:(((_TPTP_eq u) x)->False))=> x00) as proof of False % 5.95/6.14 Found (fun (x01:(((_TPTP_eq u) x)->False))=> x00) as proof of ((((_TPTP_eq u) x)->False)->False) % 5.95/6.14 Found f:((_TPTP_eq y) u) % 5.95/6.14 Instantiate: Xy:=u:frac % 5.95/6.14 Found f as proof of ((_TPTP_eq y) Xy) % 5.95/6.14 Found (satz3800 f) as proof of ((_TPTP_eq Xy) y) % 5.95/6.14 Found ((satz380 Xy) f) as proof of ((_TPTP_eq Xy) y) % 5.95/6.14 Found (((satz38 y) Xy) f) as proof of ((_TPTP_eq Xy) y) % 5.95/6.14 Found (((satz38 y) Xy) f) as proof of ((_TPTP_eq Xy) y) % 5.95/6.14 Found e:((_TPTP_eq x) z) % 5.95/6.14 Instantiate: Xy:=x:frac % 5.95/6.14 Found e as proof of ((_TPTP_eq Xy) z) % 5.95/6.14 Found (satz3800 e) as proof of ((_TPTP_eq z) Xy) % 5.95/6.14 Found ((satz380 z) e) as proof of ((_TPTP_eq z) Xy) % 5.95/6.14 Found (((satz38 Xy) z) e) as proof of ((_TPTP_eq z) Xy) % 5.95/6.14 Found (((satz38 Xy) z) e) as proof of ((_TPTP_eq z) Xy) % 5.95/6.14 Found x00:False % 5.95/6.14 Found (fun (x1:(((_TPTP_eq z) y)->False))=> x00) as proof of False % 5.95/6.14 Found (fun (x1:(((_TPTP_eq z) y)->False))=> x00) as proof of ((((_TPTP_eq z) y)->False)->False) % 5.95/6.14 Found (et0 (fun (x1:(((_TPTP_eq z) y)->False))=> x00)) as proof of ((_TPTP_eq z) y) % 5.95/6.14 Found ((et ((_TPTP_eq z) y)) (fun (x1:(((_TPTP_eq z) y)->False))=> x00)) as proof of ((_TPTP_eq z) y) % 5.95/6.14 Found ((et ((_TPTP_eq z) y)) (fun (x1:(((_TPTP_eq z) y)->False))=> x00)) as proof of ((_TPTP_eq z) y) % 9.33/9.51 Found f:((_TPTP_eq y) u) % 9.33/9.51 Found f as proof of ((_TPTP_eq y) u) % 9.33/9.51 Found x00:False % 9.33/9.51 Found (fun (x1:(((_TPTP_eq z) y)->False))=> x00) as proof of False % 9.33/9.51 Found (fun (x1:(((_TPTP_eq z) y)->False))=> x00) as proof of ((((_TPTP_eq z) y)->False)->False) % 9.33/9.51 Found (et0 (fun (x1:(((_TPTP_eq z) y)->False))=> x00)) as proof of ((_TPTP_eq z) y) % 9.33/9.51 Found ((et ((_TPTP_eq z) y)) (fun (x1:(((_TPTP_eq z) y)->False))=> x00)) as proof of ((_TPTP_eq z) y) % 9.33/9.51 Found ((et ((_TPTP_eq z) y)) (fun (x1:(((_TPTP_eq z) y)->False))=> x00)) as proof of ((_TPTP_eq z) y) % 9.33/9.51 Found x00:False % 9.33/9.51 Found (fun (x1:(((_TPTP_eq y) z)->False))=> x00) as proof of False % 9.33/9.51 Found (fun (x1:(((_TPTP_eq y) z)->False))=> x00) as proof of ((((_TPTP_eq y) z)->False)->False) % 9.33/9.51 Found x00:False % 9.33/9.51 Found (fun (x01:(((_TPTP_eq u) x)->False))=> x00) as proof of False % 9.33/9.51 Found (fun (x01:(((_TPTP_eq u) x)->False))=> x00) as proof of ((((_TPTP_eq u) x)->False)->False) % 9.33/9.51 Found f:((_TPTP_eq y) u) % 9.33/9.51 Instantiate: Xy:=u:frac % 9.33/9.51 Found f as proof of ((_TPTP_eq y) Xy) % 9.33/9.51 Found (satz3800 f) as proof of ((_TPTP_eq Xy) y) % 9.33/9.51 Found ((satz380 Xy) f) as proof of ((_TPTP_eq Xy) y) % 9.33/9.51 Found (((satz38 y) Xy) f) as proof of ((_TPTP_eq Xy) y) % 9.33/9.51 Found (((satz38 y) Xy) f) as proof of ((_TPTP_eq Xy) y) % 9.33/9.51 Found e:((_TPTP_eq x) z) % 9.33/9.51 Instantiate: Xy:=x:frac % 9.33/9.51 Found e as proof of ((_TPTP_eq Xy) z) % 9.33/9.51 Found (satz3800 e) as proof of ((_TPTP_eq z) Xy) % 9.33/9.51 Found ((satz380 z) e) as proof of ((_TPTP_eq z) Xy) % 9.33/9.51 Found (((satz38 Xy) z) e) as proof of ((_TPTP_eq z) Xy) % 9.33/9.51 Found (((satz38 Xy) z) e) as proof of ((_TPTP_eq z) Xy) % 9.33/9.51 Found f:((_TPTP_eq y) u) % 9.33/9.51 Found f as proof of ((_TPTP_eq y) u) % 9.33/9.51 Found x00:False % 9.33/9.51 Found (fun (x1:(((_TPTP_eq y) z)->False))=> x00) as proof of False % 9.33/9.51 Found (fun (x1:(((_TPTP_eq y) z)->False))=> x00) as proof of ((((_TPTP_eq y) z)->False)->False) % 9.33/9.51 Found (et0 (fun (x1:(((_TPTP_eq y) z)->False))=> x00)) as proof of ((_TPTP_eq y) z) % 9.33/9.51 Found ((et ((_TPTP_eq y) z)) (fun (x1:(((_TPTP_eq y) z)->False))=> x00)) as proof of ((_TPTP_eq y) z) % 9.33/9.51 Found ((et ((_TPTP_eq y) z)) (fun (x1:(((_TPTP_eq y) z)->False))=> x00)) as proof of ((_TPTP_eq y) z) % 9.33/9.51 Found x00:False % 9.33/9.51 Found (fun (x01:(((_TPTP_eq u) x)->False))=> x00) as proof of False % 9.33/9.51 Found (fun (x01:(((_TPTP_eq u) x)->False))=> x00) as proof of ((((_TPTP_eq u) x)->False)->False) % 9.33/9.51 Found (et0 (fun (x01:(((_TPTP_eq u) x)->False))=> x00)) as proof of ((_TPTP_eq u) x) % 9.33/9.51 Found ((et ((_TPTP_eq u) x)) (fun (x01:(((_TPTP_eq u) x)->False))=> x00)) as proof of ((_TPTP_eq u) x) % 9.33/9.51 Found ((et ((_TPTP_eq u) x)) (fun (x01:(((_TPTP_eq u) x)->False))=> x00)) as proof of ((_TPTP_eq u) x) % 9.33/9.51 Found e:((_TPTP_eq x) z) % 9.33/9.51 Found e as proof of ((_TPTP_eq x) z) % 9.33/9.51 Found x00:False % 9.33/9.51 Found (fun (x1:(((_TPTP_eq y) z)->False))=> x00) as proof of False % 9.33/9.51 Found (fun (x1:(((_TPTP_eq y) z)->False))=> x00) as proof of ((((_TPTP_eq y) z)->False)->False) % 9.33/9.51 Found (et0 (fun (x1:(((_TPTP_eq y) z)->False))=> x00)) as proof of ((_TPTP_eq y) z) % 9.33/9.51 Found ((et ((_TPTP_eq y) z)) (fun (x1:(((_TPTP_eq y) z)->False))=> x00)) as proof of ((_TPTP_eq y) z) % 9.33/9.51 Found ((et ((_TPTP_eq y) z)) (fun (x1:(((_TPTP_eq y) z)->False))=> x00)) as proof of ((_TPTP_eq y) z) % 9.33/9.51 Found x00:False % 9.33/9.51 Found (fun (x01:(((_TPTP_eq u) x)->False))=> x00) as proof of False % 9.33/9.51 Found (fun (x01:(((_TPTP_eq u) x)->False))=> x00) as proof of ((((_TPTP_eq u) x)->False)->False) % 9.33/9.51 Found (et0 (fun (x01:(((_TPTP_eq u) x)->False))=> x00)) as proof of ((_TPTP_eq u) x) % 9.33/9.51 Found ((et ((_TPTP_eq u) x)) (fun (x01:(((_TPTP_eq u) x)->False))=> x00)) as proof of ((_TPTP_eq u) x) % 9.33/9.51 Found ((et ((_TPTP_eq u) x)) (fun (x01:(((_TPTP_eq u) x)->False))=> x00)) as proof of ((_TPTP_eq u) x) % 9.33/9.51 Found x00:False % 9.33/9.51 Found (fun (x1:((moref x) y))=> x00) as proof of False % 9.33/9.51 Found (fun (x1:((moref x) y))=> x00) as proof of (((moref x) y)->False) % 9.33/9.51 Found e:((_TPTP_eq x) z) % 9.33/9.51 Found e as proof of ((_TPTP_eq x) z) % 9.33/9.51 Found e:((_TPTP_eq x) z) % 9.33/9.51 Found e as proof of ((_TPTP_eq x) z) % 9.33/9.51 Found e:((_TPTP_eq x) z) % 9.33/9.51 Found e as proof of ((_TPTP_eq x) z) % 9.33/9.51 Found x00:False % 9.33/9.51 Found (fun (x1:((moref x) y))=> x00) as proof of False % 9.33/9.51 Found (fun (x1:((moref x) y))=> x00) as proof of (((moref x) y)->False) % 9.33/9.51 Found x00:False % 9.33/9.51 Found (fun (x1:(((_TPTP_eq z) u)->False))=> x00) as proof of False % 9.33/9.51 Found (fun (x1:(((_TPTP_eq z) u)->False))=> x00) as proof of ((((_TPTP_eq z) u)->False)->False) % 15.54/15.73 Found x00:False % 15.54/15.73 Found (fun (x2:((moref x) y))=> x00) as proof of False % 15.54/15.73 Found (fun (x2:((moref x) y))=> x00) as proof of (((moref x) y)->False) % 15.54/15.73 Found e:((_TPTP_eq x) z) % 15.54/15.73 Found e as proof of ((_TPTP_eq x) z) % 15.54/15.73 Found e:((_TPTP_eq x) z) % 15.54/15.73 Found e as proof of ((_TPTP_eq x) z) % 15.54/15.73 Found x00:False % 15.54/15.73 Found (fun (x1:((moref x) y))=> x00) as proof of False % 15.54/15.73 Found (fun (x1:((moref x) y))=> x00) as proof of (((moref x) y)->False) % 15.54/15.73 Found e:((_TPTP_eq x) z) % 15.54/15.73 Found e as proof of ((_TPTP_eq x) z) % 15.54/15.73 Found e:((_TPTP_eq x) z) % 15.54/15.73 Found e as proof of ((_TPTP_eq x) z) % 15.54/15.73 Found e:((_TPTP_eq x) z) % 15.54/15.73 Found e as proof of ((_TPTP_eq x) z) % 15.54/15.73 Found x00:False % 15.54/15.73 Found (fun (x1:((moref x) y))=> x00) as proof of False % 15.54/15.73 Found (fun (x1:((moref x) y))=> x00) as proof of (((moref x) y)->False) % 15.54/15.73 Found e:((_TPTP_eq x) z) % 15.54/15.73 Found e as proof of ((_TPTP_eq x) z) % 15.54/15.73 Found x00:False % 15.54/15.73 Found (fun (x1:(((_TPTP_eq u) z)->False))=> x00) as proof of False % 15.54/15.73 Found (fun (x1:(((_TPTP_eq u) z)->False))=> x00) as proof of ((((_TPTP_eq u) z)->False)->False) % 15.54/15.73 Found x00:False % 15.54/15.73 Found (fun (x01:((((moref x) y)->False)->False))=> x00) as proof of False % 15.54/15.73 Found (fun (x01:((((moref x) y)->False)->False))=> x00) as proof of (((((moref x) y)->False)->False)->False) % 15.54/15.73 Found x00:False % 15.54/15.73 Found (fun (x1:(((_TPTP_eq z) u)->False))=> x00) as proof of False % 15.54/15.73 Found (fun (x1:(((_TPTP_eq z) u)->False))=> x00) as proof of ((((_TPTP_eq z) u)->False)->False) % 15.54/15.73 Found x00:False % 15.54/15.73 Found (fun (x2:((moref x) y))=> x00) as proof of False % 15.54/15.73 Found (fun (x2:((moref x) y))=> x00) as proof of (((moref x) y)->False) % 15.54/15.73 Found e:((_TPTP_eq x) z) % 15.54/15.73 Found e as proof of ((_TPTP_eq x) z) % 15.54/15.73 Found e:((_TPTP_eq x) z) % 15.54/15.73 Found e as proof of ((_TPTP_eq x) z) % 15.54/15.73 Found e:((_TPTP_eq x) z) % 15.54/15.73 Found e as proof of ((_TPTP_eq x) z) % 15.54/15.73 Found e:((_TPTP_eq x) z) % 15.54/15.73 Found e as proof of ((_TPTP_eq x) z) % 15.54/15.73 Found x00:False % 15.54/15.73 Found (fun (x2:(False->False))=> x00) as proof of False % 15.54/15.73 Found (fun (x2:(False->False))=> x00) as proof of ((False->False)->False) % 15.54/15.73 Found e:((_TPTP_eq x) z) % 15.54/15.73 Found e as proof of ((_TPTP_eq x) z) % 15.54/15.73 Found e:((_TPTP_eq x) z) % 15.54/15.73 Found e as proof of ((_TPTP_eq x) z) % 15.54/15.73 Found e:((_TPTP_eq x) z) % 15.54/15.73 Found e as proof of ((_TPTP_eq x) z) % 15.54/15.73 Found e:((_TPTP_eq x) z) % 15.54/15.73 Found e as proof of ((_TPTP_eq x) z) % 15.54/15.73 Found x00:False % 15.54/15.73 Found (fun (x01:((((moref x) y)->False)->False))=> x00) as proof of False % 15.54/15.73 Found (fun (x01:((((moref x) y)->False)->False))=> x00) as proof of (((((moref x) y)->False)->False)->False) % 15.54/15.73 Found x00:False % 15.54/15.73 Found (fun (x1:(((_TPTP_eq u) z)->False))=> x00) as proof of False % 15.54/15.73 Found (fun (x1:(((_TPTP_eq u) z)->False))=> x00) as proof of ((((_TPTP_eq u) z)->False)->False) % 15.54/15.73 Found x00:False % 15.54/15.73 Found (fun (x1:(((_TPTP_eq z) Xy)->False))=> x00) as proof of False % 15.54/15.73 Found (fun (x1:(((_TPTP_eq z) Xy)->False))=> x00) as proof of ((((_TPTP_eq z) Xy)->False)->False) % 15.54/15.73 Found x00:False % 15.54/15.73 Found (fun (x1:(((_TPTP_eq z) u)->False))=> x00) as proof of False % 15.54/15.73 Found (fun (x1:(((_TPTP_eq z) u)->False))=> x00) as proof of ((((_TPTP_eq z) u)->False)->False) % 15.54/15.73 Found (et0 (fun (x1:(((_TPTP_eq z) u)->False))=> x00)) as proof of ((_TPTP_eq z) u) % 15.54/15.73 Found ((et ((_TPTP_eq z) u)) (fun (x1:(((_TPTP_eq z) u)->False))=> x00)) as proof of ((_TPTP_eq z) u) % 15.54/15.73 Found ((et ((_TPTP_eq z) u)) (fun (x1:(((_TPTP_eq z) u)->False))=> x00)) as proof of ((_TPTP_eq z) u) % 15.54/15.73 Found e:((_TPTP_eq x) z) % 15.54/15.73 Found e as proof of ((_TPTP_eq x) z) % 15.54/15.73 Found e:((_TPTP_eq x) z) % 15.54/15.73 Found e as proof of ((_TPTP_eq x) z) % 15.54/15.73 Found x00:False % 15.54/15.73 Found (fun (x1:(((_TPTP_eq z) Xy)->False))=> x00) as proof of False % 15.54/15.73 Found (fun (x1:(((_TPTP_eq z) Xy)->False))=> x00) as proof of ((((_TPTP_eq z) Xy)->False)->False) % 15.54/15.73 Found x00:False % 15.54/15.73 Found (fun (x2:(False->False))=> x00) as proof of False % 15.54/15.73 Found (fun (x2:(False->False))=> x00) as proof of ((False->False)->False) % 15.54/15.73 Found x00:False % 15.54/15.73 Found (fun (x1:(((_TPTP_eq u) z)->False))=> x00) as proof of False % 15.54/15.73 Found (fun (x1:(((_TPTP_eq u) z)->False))=> x00) as proof of ((((_TPTP_eq u) z)->False)->False) % 15.54/15.73 Found (et0 (fun (x1:(((_TPTP_eq u) z)->False))=> x00)) as proof of ((_TPTP_eq u) z) % 15.54/15.73 Found ((et ((_TPTP_eq u) z)) (fun (x1:(((_TPTP_eq u) z)->False))=> x00)) as proof of ((_TPTP_eq u) z) % 15.54/15.73 Found ((et ((_TPTP_eq u) z)) (fun (x1:(((_TPTP_eq u) z)->False))=> x00)) as proof of ((_TPTP_eq u) z) % 18.03/18.26 Found x00:False % 18.03/18.26 Found (fun (x1:(((_TPTP_eq z) Xy)->False))=> x00) as proof of False % 18.03/18.26 Found (fun (x1:(((_TPTP_eq z) Xy)->False))=> x00) as proof of ((((_TPTP_eq z) Xy)->False)->False) % 18.03/18.26 Found (et0 (fun (x1:(((_TPTP_eq z) Xy)->False))=> x00)) as proof of ((_TPTP_eq z) Xy) % 18.03/18.26 Found ((et ((_TPTP_eq z) Xy)) (fun (x1:(((_TPTP_eq z) Xy)->False))=> x00)) as proof of ((_TPTP_eq z) Xy) % 18.03/18.26 Found ((et ((_TPTP_eq z) Xy)) (fun (x1:(((_TPTP_eq z) Xy)->False))=> x00)) as proof of ((_TPTP_eq z) Xy) % 18.03/18.26 Found x00:False % 18.03/18.26 Found (fun (x1:(((_TPTP_eq Xy) z)->False))=> x00) as proof of False % 18.03/18.26 Found (fun (x1:(((_TPTP_eq Xy) z)->False))=> x00) as proof of ((((_TPTP_eq Xy) z)->False)->False) % 18.03/18.26 Found x00:False % 18.03/18.26 Found (fun (x1:(((_TPTP_eq u) z)->False))=> x00) as proof of False % 18.03/18.26 Found (fun (x1:(((_TPTP_eq u) z)->False))=> x00) as proof of ((((_TPTP_eq u) z)->False)->False) % 18.03/18.26 Found x00:False % 18.03/18.26 Found (fun (x1:(((_TPTP_eq z) Xy)->False))=> x00) as proof of False % 18.03/18.26 Found (fun (x1:(((_TPTP_eq z) Xy)->False))=> x00) as proof of ((((_TPTP_eq z) Xy)->False)->False) % 18.03/18.26 Found (et0 (fun (x1:(((_TPTP_eq z) Xy)->False))=> x00)) as proof of ((_TPTP_eq z) Xy) % 18.03/18.26 Found ((et ((_TPTP_eq z) Xy)) (fun (x1:(((_TPTP_eq z) Xy)->False))=> x00)) as proof of ((_TPTP_eq z) Xy) % 18.03/18.26 Found ((et ((_TPTP_eq z) Xy)) (fun (x1:(((_TPTP_eq z) Xy)->False))=> x00)) as proof of ((_TPTP_eq z) Xy) % 18.03/18.26 Found x00:False % 18.03/18.26 Found (fun (x1:((moref x) y))=> x00) as proof of False % 18.03/18.26 Found (fun (x1:((moref x) y))=> x00) as proof of (((moref x) y)->False) % 18.03/18.26 Found x00:False % 18.03/18.26 Found (fun (x1:(((_TPTP_eq Xy) z)->False))=> x00) as proof of False % 18.03/18.26 Found (fun (x1:(((_TPTP_eq Xy) z)->False))=> x00) as proof of ((((_TPTP_eq Xy) z)->False)->False) % 18.03/18.26 Found satz440000000:=(satz44000000 e):((moref z) u) % 18.03/18.26 Found (satz44000000 e) as proof of ((moref z) u) % 18.03/18.26 Found ((satz4400000 x1) e) as proof of ((moref z) u) % 18.03/18.26 Found (((satz440000 x) x1) e) as proof of ((moref z) u) % 18.03/18.26 Found ((((fun (Xx:frac) (x2:((moref Xx) y)) (x3:((_TPTP_eq Xx) z))=> ((((satz44000 Xx) x2) x3) f)) x) x1) e) as proof of ((moref z) u) % 18.03/18.26 Found ((((fun (Xx:frac) (x2:((moref Xx) y)) (x3:((_TPTP_eq Xx) z))=> (((((fun (Xx:frac)=> ((satz4400 Xx) y)) Xx) x2) x3) f)) x) x1) e) as proof of ((moref z) u) % 18.03/18.26 Found ((((fun (Xx:frac) (x2:((moref Xx) y)) (x3:((_TPTP_eq Xx) z))=> (((((fun (Xx:frac)=> (((fun (Xx:frac) (Xy:frac)=> (((satz440 Xx) Xy) u)) Xx) y)) Xx) x2) x3) f)) x) x1) e) as proof of ((moref z) u) % 18.03/18.26 Found ((((fun (Xx:frac) (x2:((moref Xx) y)) (x3:((_TPTP_eq Xx) z))=> (((((fun (Xx:frac)=> (((fun (Xx:frac) (Xy:frac)=> ((((fun (Xx:frac) (Xy:frac)=> (((satz44 Xx) Xy) z)) Xx) Xy) u)) Xx) y)) Xx) x2) x3) f)) x) x1) e) as proof of ((moref z) u) % 18.03/18.26 Found ((((fun (Xx:frac) (x2:((moref Xx) y)) (x3:((_TPTP_eq Xx) z))=> (((((fun (Xx:frac)=> (((fun (Xx:frac) (Xy:frac)=> ((((fun (Xx:frac) (Xy:frac)=> (((satz44 Xx) Xy) z)) Xx) Xy) u)) Xx) y)) Xx) x2) x3) f)) x) x1) e) as proof of ((moref z) u) % 18.03/18.26 Found (x0 ((((fun (Xx:frac) (x2:((moref Xx) y)) (x3:((_TPTP_eq Xx) z))=> (((((fun (Xx:frac)=> (((fun (Xx:frac) (Xy:frac)=> ((((fun (Xx:frac) (Xy:frac)=> (((satz44 Xx) Xy) z)) Xx) Xy) u)) Xx) y)) Xx) x2) x3) f)) x) x1) e)) as proof of False % 18.03/18.26 Found (fun (x1:((moref x) y))=> (x0 ((((fun (Xx:frac) (x2:((moref Xx) y)) (x3:((_TPTP_eq Xx) z))=> (((((fun (Xx:frac)=> (((fun (Xx:frac) (Xy:frac)=> ((((fun (Xx:frac) (Xy:frac)=> (((satz44 Xx) Xy) z)) Xx) Xy) u)) Xx) y)) Xx) x2) x3) f)) x) x1) e))) as proof of False % 18.03/18.26 Found (fun (x1:((moref x) y))=> (x0 ((((fun (Xx:frac) (x2:((moref Xx) y)) (x3:((_TPTP_eq Xx) z))=> (((((fun (Xx:frac)=> (((fun (Xx:frac) (Xy:frac)=> ((((fun (Xx:frac) (Xy:frac)=> (((satz44 Xx) Xy) z)) Xx) Xy) u)) Xx) y)) Xx) x2) x3) f)) x) x1) e))) as proof of (((moref x) y)->False) % 18.03/18.26 Found x00:False % 18.03/18.26 Found (fun (x1:(((_TPTP_eq u) z)->False))=> x00) as proof of False % 18.03/18.26 Found (fun (x1:(((_TPTP_eq u) z)->False))=> x00) as proof of ((((_TPTP_eq u) z)->False)->False) % 18.03/18.26 Found (et0 (fun (x1:(((_TPTP_eq u) z)->False))=> x00)) as proof of ((_TPTP_eq u) z) % 18.03/18.26 Found ((et ((_TPTP_eq u) z)) (fun (x1:(((_TPTP_eq u) z)->False))=> x00)) as proof of ((_TPTP_eq u) z) % 18.03/18.26 Found ((et ((_TPTP_eq u) z)) (fun (x1:(((_TPTP_eq u) z)->False))=> x00)) as proof of ((_TPTP_eq u) z) % 18.63/18.81 Found m0:((_TPTP_eq x) y) % 18.63/18.81 Instantiate: Xy:=x:frac % 18.63/18.81 Found m0 as proof of ((_TPTP_eq Xy) y) % 18.63/18.81 Found e:((_TPTP_eq x) z) % 18.63/18.81 Found e as proof of ((_TPTP_eq x) z) % 18.63/18.81 Found m0:((_TPTP_eq x) y) % 18.63/18.81 Instantiate: Xy:=x:frac % 18.63/18.81 Found m0 as proof of ((_TPTP_eq Xy) y) % 18.63/18.81 Found e:((_TPTP_eq x) z) % 18.63/18.81 Instantiate: Xy:=x:frac % 18.63/18.81 Found e as proof of ((_TPTP_eq Xy) z) % 18.63/18.81 Found (satz3800 e) as proof of ((_TPTP_eq z) Xy) % 18.63/18.81 Found ((satz380 z) e) as proof of ((_TPTP_eq z) Xy) % 18.63/18.81 Found (((satz38 Xy) z) e) as proof of ((_TPTP_eq z) Xy) % 18.63/18.81 Found (((satz38 Xy) z) e) as proof of ((_TPTP_eq z) Xy) % 18.63/18.81 Found ((satz39010 (((satz38 Xy) z) e)) m0) as proof of ((_TPTP_eq z) y) % 18.63/18.81 Found (((satz3901 x) (((satz38 x) z) e)) m0) as proof of ((_TPTP_eq z) y) % 18.63/18.81 Found ((((fun (Xy:frac)=> ((satz390 Xy) y)) x) (((satz38 x) z) e)) m0) as proof of ((_TPTP_eq z) y) % 18.63/18.81 Found ((((fun (Xy:frac)=> ((satz390 Xy) y)) x) (((satz38 x) z) e)) m0) as proof of ((_TPTP_eq z) y) % 18.63/18.81 Found ((satz39000 ((((fun (Xy:frac)=> ((satz390 Xy) y)) x) (((satz38 x) z) e)) m0)) f) as proof of ((_TPTP_eq z) u) % 18.63/18.81 Found (((satz3900 y) ((((fun (Xy:frac)=> ((satz390 Xy) y)) x) (((satz38 x) z) e)) m0)) f) as proof of ((_TPTP_eq z) u) % 18.63/18.81 Found ((((fun (Xy:frac)=> ((satz390 Xy) u)) y) ((((fun (Xy:frac)=> ((satz390 Xy) y)) x) (((satz38 x) z) e)) m0)) f) as proof of ((_TPTP_eq z) u) % 18.63/18.81 Found ((((fun (Xy:frac)=> (((satz39 z) Xy) u)) y) ((((fun (Xy:frac)=> (((satz39 z) Xy) y)) x) (((satz38 x) z) e)) m0)) f) as proof of ((_TPTP_eq z) u) % 18.63/18.81 Found ((((fun (Xy:frac)=> (((satz39 z) Xy) u)) y) ((((fun (Xy:frac)=> (((satz39 z) Xy) y)) x) (((satz38 x) z) e)) m0)) f) as proof of ((_TPTP_eq z) u) % 18.63/18.81 Found ((((fun (Xy:frac)=> (((satz39 z) Xy) u)) y) ((((fun (Xy:frac)=> (((satz39 z) Xy) y)) x) (((satz38 x) z) e)) (m (fun (x1:((moref x) y))=> (x0 ((((fun (Xx:frac) (x2:((moref Xx) y)) (x3:((_TPTP_eq Xx) z))=> (((((fun (Xx:frac)=> (((fun (Xx:frac) (Xy:frac)=> ((((fun (Xx:frac) (Xy:frac)=> (((satz44 Xx) Xy) z)) Xx) Xy) u)) Xx) y)) Xx) x2) x3) f)) x) x1) e)))))) f) as proof of ((_TPTP_eq z) u) % 18.63/18.81 Found (fun (x0:(((moref z) u)->False))=> ((((fun (Xy:frac)=> (((satz39 z) Xy) u)) y) ((((fun (Xy:frac)=> (((satz39 z) Xy) y)) x) (((satz38 x) z) e)) (m (fun (x1:((moref x) y))=> (x0 ((((fun (Xx:frac) (x2:((moref Xx) y)) (x3:((_TPTP_eq Xx) z))=> (((((fun (Xx:frac)=> (((fun (Xx:frac) (Xy:frac)=> ((((fun (Xx:frac) (Xy:frac)=> (((satz44 Xx) Xy) z)) Xx) Xy) u)) Xx) y)) Xx) x2) x3) f)) x) x1) e)))))) f)) as proof of ((_TPTP_eq z) u) % 18.63/18.81 Found (fun (x0:(((moref z) u)->False))=> ((((fun (Xy:frac)=> (((satz39 z) Xy) u)) y) ((((fun (Xy:frac)=> (((satz39 z) Xy) y)) x) (((satz38 x) z) e)) (m (fun (x1:((moref x) y))=> (x0 ((((fun (Xx:frac) (x2:((moref Xx) y)) (x3:((_TPTP_eq Xx) z))=> (((((fun (Xx:frac)=> (((fun (Xx:frac) (Xy:frac)=> ((((fun (Xx:frac) (Xy:frac)=> (((satz44 Xx) Xy) z)) Xx) Xy) u)) Xx) y)) Xx) x2) x3) f)) x) x1) e)))))) f)) as proof of ((((moref z) u)->False)->((_TPTP_eq z) u)) % 18.63/18.81 Got proof (fun (x0:(((moref z) u)->False))=> ((((fun (Xy:frac)=> (((satz39 z) Xy) u)) y) ((((fun (Xy:frac)=> (((satz39 z) Xy) y)) x) (((satz38 x) z) e)) (m (fun (x1:((moref x) y))=> (x0 ((((fun (Xx:frac) (x2:((moref Xx) y)) (x3:((_TPTP_eq Xx) z))=> (((((fun (Xx:frac)=> (((fun (Xx:frac) (Xy:frac)=> ((((fun (Xx:frac) (Xy:frac)=> (((satz44 Xx) Xy) z)) Xx) Xy) u)) Xx) y)) Xx) x2) x3) f)) x) x1) e)))))) f)) % 18.63/18.81 Time elapsed = 18.021060s % 18.63/18.81 node=5862 cost=1307.000000 depth=16 % 18.63/18.81:::::::::::::::::::::: % 18.63/18.81 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 18.63/18.81 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p % 18.63/18.81 (fun (x0:(((moref z) u)->False))=> ((((fun (Xy:frac)=> (((satz39 z) Xy) u)) y) ((((fun (Xy:frac)=> (((satz39 z) Xy) y)) x) (((satz38 x) z) e)) (m (fun (x1:((moref x) y))=> (x0 ((((fun (Xx:frac) (x2:((moref Xx) y)) (x3:((_TPTP_eq Xx) z))=> (((((fun (Xx:frac)=> (((fun (Xx:frac) (Xy:frac)=> ((((fun (Xx:frac) (Xy:frac)=> (((satz44 Xx) Xy) z)) Xx) Xy) u)) Xx) y)) Xx) x2) x3) f)) x) x1) e)))))) f)) % 18.63/18.81 % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p %------------------------------------------------------------------------------