%------------------------------------------------------------------------------ % File : cocATP---0.2.0 % Problem : NUM635^2 : TPTP v7.0.0. Released v3.7.0. % Transfm : none % Format : tptp:raw % Command : python CASC.py /export/starexec/sandbox2/benchmark/theBenchmark.p % Computer : n046.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:13 EST 2018 % Result : Theorem 0.80s % Output : Proof 0.80s % 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.04 % Problem : NUM635^2 : 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.24 % Computer : n046.star.cs.uiowa.edu % 0.02/0.24 % Model : x86_64 x86_64 % 0.02/0.24 % CPU : Intel(R) Xeon(R) CPU E5-2609 0 @ 2.40GHz % 0.02/0.24 % Memory : 32218.625MB % 0.02/0.24 % OS : Linux 3.10.0-693.2.2.el7.x86_64 % 0.06/0.24 % CPULimit : 300 % 0.06/0.24 % DateTime : Fri Jan 5 11:14:00 CST 2018 % 0.06/0.24 % CPUTime : % 0.08/3.25 Python 2.7.13 % 0.80/16.74 Using paths ['/home/cristobal/cocATP/CASC/TPTP/', '/export/starexec/sandbox2/benchmark/', '/export/starexec/sandbox2/benchmark/'] % 0.80/16.74 FOF formula (<kernel.Constant object at 0x2af407bf0c68>, <kernel.Constant object at 0x2af407bf07a0>) of role type named one_type % 0.80/16.74 Using role type % 0.80/16.74 Declaring one:fofType % 0.80/16.74 FOF formula (<kernel.Constant object at 0x2af3fff84cb0>, <kernel.DependentProduct object at 0x2af407bf0d40>) of role type named succ_type % 0.80/16.74 Using role type % 0.80/16.74 Declaring succ:(fofType->fofType) % 0.80/16.74 FOF formula (forall (X:fofType), (not (((eq fofType) (succ X)) one))) of role axiom named one_is_first % 0.80/16.74 A new axiom: (forall (X:fofType), (not (((eq fofType) (succ X)) one))) % 0.80/16.74 FOF formula (forall (X:fofType) (Y:fofType), ((((eq fofType) (succ X)) (succ Y))->(((eq fofType) X) Y))) of role axiom named succ_injective % 0.80/16.74 A new axiom: (forall (X:fofType) (Y:fofType), ((((eq fofType) (succ X)) (succ Y))->(((eq fofType) X) Y))) % 0.80/16.74 FOF formula (forall (M:(fofType->Prop)), (((and (M one)) (forall (X:fofType), ((M X)->(M (succ X)))))->(forall (Y:fofType), (M Y)))) of role axiom named induction % 0.80/16.74 A new axiom: (forall (M:(fofType->Prop)), (((and (M one)) (forall (X:fofType), ((M X)->(M (succ X)))))->(forall (Y:fofType), (M Y)))) % 0.80/16.74 FOF formula (forall (X:fofType) (Y:fofType), ((not (((eq fofType) X) Y))->(not (((eq fofType) (succ X)) (succ Y))))) of role conjecture named satz1 % 0.80/16.74 Conjecture to prove = (forall (X:fofType) (Y:fofType), ((not (((eq fofType) X) Y))->(not (((eq fofType) (succ X)) (succ Y))))):Prop % 0.80/16.74 We need to prove ['(forall (X:fofType) (Y:fofType), ((not (((eq fofType) X) Y))->(not (((eq fofType) (succ X)) (succ Y)))))'] % 0.80/16.74 Parameter fofType:Type. % 0.80/16.74 Parameter one:fofType. % 0.80/16.74 Parameter succ:(fofType->fofType). % 0.80/16.74 Axiom one_is_first:(forall (X:fofType), (not (((eq fofType) (succ X)) one))). % 0.80/16.74 Axiom succ_injective:(forall (X:fofType) (Y:fofType), ((((eq fofType) (succ X)) (succ Y))->(((eq fofType) X) Y))). % 0.80/16.74 Axiom induction:(forall (M:(fofType->Prop)), (((and (M one)) (forall (X:fofType), ((M X)->(M (succ X)))))->(forall (Y:fofType), (M Y)))). % 0.80/16.74 Trying to prove (forall (X:fofType) (Y:fofType), ((not (((eq fofType) X) Y))->(not (((eq fofType) (succ X)) (succ Y))))) % 0.80/16.74 Found x0:(((eq fofType) (succ X)) (succ Y)) % 0.80/16.74 Found x0 as proof of (((eq fofType) (succ X)) (succ Y)) % 0.80/16.74 Found (succ_injective00 x0) as proof of (((eq fofType) X) Y) % 0.80/16.74 Found ((succ_injective0 Y) x0) as proof of (((eq fofType) X) Y) % 0.80/16.74 Found (((succ_injective X) Y) x0) as proof of (((eq fofType) X) Y) % 0.80/16.74 Found (((succ_injective X) Y) x0) as proof of (((eq fofType) X) Y) % 0.80/16.74 Found (x (((succ_injective X) Y) x0)) as proof of False % 0.80/16.74 Found (fun (x0:(((eq fofType) (succ X)) (succ Y)))=> (x (((succ_injective X) Y) x0))) as proof of False % 0.80/16.74 Found (fun (x:(not (((eq fofType) X) Y))) (x0:(((eq fofType) (succ X)) (succ Y)))=> (x (((succ_injective X) Y) x0))) as proof of (not (((eq fofType) (succ X)) (succ Y))) % 0.80/16.74 Found (fun (Y:fofType) (x:(not (((eq fofType) X) Y))) (x0:(((eq fofType) (succ X)) (succ Y)))=> (x (((succ_injective X) Y) x0))) as proof of ((not (((eq fofType) X) Y))->(not (((eq fofType) (succ X)) (succ Y)))) % 0.80/16.74 Found (fun (X:fofType) (Y:fofType) (x:(not (((eq fofType) X) Y))) (x0:(((eq fofType) (succ X)) (succ Y)))=> (x (((succ_injective X) Y) x0))) as proof of (forall (Y:fofType), ((not (((eq fofType) X) Y))->(not (((eq fofType) (succ X)) (succ Y))))) % 0.80/16.74 Found (fun (X:fofType) (Y:fofType) (x:(not (((eq fofType) X) Y))) (x0:(((eq fofType) (succ X)) (succ Y)))=> (x (((succ_injective X) Y) x0))) as proof of (forall (X:fofType) (Y:fofType), ((not (((eq fofType) X) Y))->(not (((eq fofType) (succ X)) (succ Y))))) % 0.80/16.74 Got proof (fun (X:fofType) (Y:fofType) (x:(not (((eq fofType) X) Y))) (x0:(((eq fofType) (succ X)) (succ Y)))=> (x (((succ_injective X) Y) x0))) % 0.80/16.74 Time elapsed = 0.476822s % 0.80/16.74 node=93 cost=112.000000 depth=10 % 0.80/16.74:::::::::::::::::::::: % 0.80/16.74 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.80/16.74 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.80/16.74 (fun (X:fofType) (Y:fofType) (x:(not (((eq fofType) X) Y))) (x0:(((eq fofType) (succ X)) (succ Y)))=> (x (((succ_injective X) Y) x0))) % 0.80/16.74 % SZS output end Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p %------------------------------------------------------------------------------