%------------------------------------------------------------------------------ % File : cocATP---0.2.0 % Problem : NUM740^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 : n038.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 0.43s % Output : Proof 0.43s % 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 : NUM740^1 : TPTP v7.0.0. Released v3.7.0. % 0.00/0.04 % Command : python CASC.py /export/starexec/sandbox/benchmark/theBenchmark.p % 0.02/0.23 % Computer : n038.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:22:21 CST 2018 % 0.02/0.23 % CPUTime : % 0.08/0.25 Python 2.7.13 % 0.43/0.62 Using paths ['/home/cristobal/cocATP/CASC/TPTP/', '/export/starexec/sandbox/benchmark/', '/export/starexec/sandbox/benchmark/'] % 0.43/0.62 FOF formula (<kernel.Constant object at 0x2b6d3cd81f80>, <kernel.Type object at 0x2b6d3cd81638>) of role type named frac_type % 0.43/0.62 Using role type % 0.43/0.62 Declaring frac:Type % 0.43/0.62 FOF formula (<kernel.Constant object at 0x2b6d3ca20638>, <kernel.Constant object at 0x2b6d3cd81440>) of role type named x % 0.43/0.62 Using role type % 0.43/0.62 Declaring x:frac % 0.43/0.62 FOF formula (<kernel.Constant object at 0x2b6d3cd81b90>, <kernel.Constant object at 0x2b6d3cd81440>) of role type named y % 0.43/0.62 Using role type % 0.43/0.62 Declaring y:frac % 0.43/0.62 FOF formula (<kernel.Constant object at 0x2b6d3cd81f80>, <kernel.DependentProduct object at 0x2b6d3cd81fc8>) of role type named moref % 0.43/0.62 Using role type % 0.43/0.62 Declaring moref:(frac->(frac->Prop)) % 0.43/0.62 FOF formula (<kernel.Constant object at 0x2b6d3cd81488>, <kernel.DependentProduct object at 0x2b6d3cd81d88>) of role type named eq % 0.43/0.62 Using role type % 0.43/0.62 Declaring _TPTP_eq:(frac->(frac->Prop)) % 0.43/0.62 FOF formula ((((moref x) y)->False)->((_TPTP_eq x) y)) of role axiom named m % 0.43/0.62 A new axiom: ((((moref x) y)->False)->((_TPTP_eq x) y)) % 0.43/0.62 FOF formula (<kernel.Constant object at 0x2b6d3cd819e0>, <kernel.DependentProduct object at 0x2b6d3cd81b90>) of role type named lessf % 0.43/0.62 Using role type % 0.43/0.62 Declaring lessf:(frac->(frac->Prop)) % 0.43/0.62 FOF formula (forall (Xx:frac) (Xy:frac), (((_TPTP_eq Xx) Xy)->((_TPTP_eq Xy) Xx))) of role axiom named satz38 % 0.43/0.62 A new axiom: (forall (Xx:frac) (Xy:frac), (((_TPTP_eq Xx) Xy)->((_TPTP_eq Xy) Xx))) % 0.43/0.62 FOF formula (forall (Xx:frac) (Xy:frac), (((moref Xx) Xy)->((lessf Xy) Xx))) of role axiom named satz42 % 0.43/0.62 A new axiom: (forall (Xx:frac) (Xy:frac), (((moref Xx) Xy)->((lessf Xy) Xx))) % 0.43/0.62 FOF formula ((((lessf y) x)->False)->((_TPTP_eq y) x)) of role conjecture named satz48 % 0.43/0.62 Conjecture to prove = ((((lessf y) x)->False)->((_TPTP_eq y) x)):Prop % 0.43/0.62 We need to prove ['((((lessf y) x)->False)->((_TPTP_eq y) x))'] % 0.43/0.62 Parameter frac:Type. % 0.43/0.62 Parameter x:frac. % 0.43/0.62 Parameter y:frac. % 0.43/0.62 Parameter moref:(frac->(frac->Prop)). % 0.43/0.62 Parameter _TPTP_eq:(frac->(frac->Prop)). % 0.43/0.62 Axiom m:((((moref x) y)->False)->((_TPTP_eq x) y)). % 0.43/0.62 Parameter lessf:(frac->(frac->Prop)). % 0.43/0.62 Axiom satz38:(forall (Xx:frac) (Xy:frac), (((_TPTP_eq Xx) Xy)->((_TPTP_eq Xy) Xx))). % 0.43/0.62 Axiom satz42:(forall (Xx:frac) (Xy:frac), (((moref Xx) Xy)->((lessf Xy) Xx))). % 0.43/0.62 Trying to prove ((((lessf y) x)->False)->((_TPTP_eq y) x)) % 0.43/0.62 Found satz42000:=(satz4200 x1):((lessf y) x) % 0.43/0.62 Found (satz4200 x1) as proof of ((lessf y) x) % 0.43/0.62 Found ((satz420 y) x1) as proof of ((lessf y) x) % 0.43/0.62 Found (((satz42 x) y) x1) as proof of ((lessf y) x) % 0.43/0.62 Found (((satz42 x) y) x1) as proof of ((lessf y) x) % 0.43/0.62 Found (x0 (((satz42 x) y) x1)) as proof of False % 0.43/0.62 Found (fun (x1:((moref x) y))=> (x0 (((satz42 x) y) x1))) as proof of False % 0.43/0.62 Found (fun (x1:((moref x) y))=> (x0 (((satz42 x) y) x1))) as proof of (((moref x) y)->False) % 0.43/0.62 Found (m (fun (x1:((moref x) y))=> (x0 (((satz42 x) y) x1)))) as proof of ((_TPTP_eq x) y) % 0.43/0.62 Found (m (fun (x1:((moref x) y))=> (x0 (((satz42 x) y) x1)))) as proof of ((_TPTP_eq x) y) % 0.43/0.62 Found (satz3800 (m (fun (x1:((moref x) y))=> (x0 (((satz42 x) y) x1))))) as proof of ((_TPTP_eq y) x) % 0.43/0.62 Found ((satz380 y) (m (fun (x1:((moref x) y))=> (x0 (((satz42 x) y) x1))))) as proof of ((_TPTP_eq y) x) % 0.43/0.62 Found (((satz38 x) y) (m (fun (x1:((moref x) y))=> (x0 (((satz42 x) y) x1))))) as proof of ((_TPTP_eq y) x) % 0.43/0.62 Found (fun (x0:(((lessf y) x)->False))=> (((satz38 x) y) (m (fun (x1:((moref x) y))=> (x0 (((satz42 x) y) x1)))))) as proof of ((_TPTP_eq y) x) % 0.43/0.62 Found (fun (x0:(((lessf y) x)->False))=> (((satz38 x) y) (m (fun (x1:((moref x) y))=> (x0 (((satz42 x) y) x1)))))) as proof of ((((lessf y) x)->False)->((_TPTP_eq y) x)) % 0.43/0.62 Got proof (fun (x0:(((lessf y) x)->False))=> (((satz38 x) y) (m (fun (x1:((moref x) y))=> (x0 (((satz42 x) y) x1)))))) % 0.43/0.62 Time elapsed = 0.095124s % 0.43/0.62 node=31 cost=179.000000 depth=13 % 0.43/0.62:::::::::::::::::::::: % 0.43/0.62 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 0.43/0.62 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p % 0.43/0.62 (fun (x0:(((lessf y) x)->False))=> (((satz38 x) y) (m (fun (x1:((moref x) y))=> (x0 (((satz42 x) y) x1)))))) % 0.43/0.62 % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p %------------------------------------------------------------------------------