%------------------------------------------------------------------------------ % File : cocATP---0.2.0 % Problem : SYO236^5 : TPTP v7.5.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : python CASC.py /export/starexec/sandbox2/benchmark/theBenchmark.p % Computer : n014.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 0s % DateTime : Tue Mar 29 00:50:59 EDT 2022 % Result : Theorem 0.82s 1.04s % Output : Proof 0.82s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.08/0.11 % Problem : SYO236^5 : TPTP v7.5.0. Released v4.0.0. % 0.08/0.12 % Command : python CASC.py /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.12/0.33 % Computer : n014.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPUModel : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % RAMPerCPU : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % DateTime : Fri Mar 11 20:38:03 EST 2022 % 0.12/0.33 % CPUTime : % 0.12/0.34 ModuleCmd_Load.c(213):ERROR:105: Unable to locate a modulefile for 'python/python27' % 0.12/0.34 Python 2.7.5 % 0.82/1.03 Using paths ['/home/cristobal/cocATP/CASC/TPTP/', '/export/starexec/sandbox2/benchmark/', '/export/starexec/sandbox2/benchmark/'] % 0.82/1.03 FOF formula (<kernel.Constant object at 0x2b118097f758>, <kernel.Type object at 0x2b118097f290>) of role type named b_type % 0.82/1.03 Using role type % 0.82/1.03 Declaring b:Type % 0.82/1.03 FOF formula (<kernel.Constant object at 0x1e9dcb0>, <kernel.Type object at 0x2b118097f440>) of role type named a_type % 0.82/1.03 Using role type % 0.82/1.03 Declaring a:Type % 0.82/1.03 FOF formula (<kernel.Constant object at 0x2b118097f2d8>, <kernel.DependentProduct object at 0x2b118097fef0>) of role type named g % 0.82/1.03 Using role type % 0.82/1.03 Declaring g:(b->a) % 0.82/1.03 FOF formula (<kernel.Constant object at 0x2b118097f128>, <kernel.DependentProduct object at 0x2b118097f098>) of role type named f % 0.82/1.03 Using role type % 0.82/1.03 Declaring f:(b->a) % 0.82/1.03 FOF formula (((or (forall (Q:((b->a)->Prop)), ((Q f)->(Q g)))) (forall (Xx:b), (((eq a) (f Xx)) (g Xx))))->(((eq (b->a)) f) g)) of role conjecture named cTHM504 % 0.82/1.03 Conjecture to prove = (((or (forall (Q:((b->a)->Prop)), ((Q f)->(Q g)))) (forall (Xx:b), (((eq a) (f Xx)) (g Xx))))->(((eq (b->a)) f) g)):Prop % 0.82/1.03 Parameter b_DUMMY:b. % 0.82/1.03 Parameter a_DUMMY:a. % 0.82/1.03 We need to prove ['(((or (forall (Q:((b->a)->Prop)), ((Q f)->(Q g)))) (forall (Xx:b), (((eq a) (f Xx)) (g Xx))))->(((eq (b->a)) f) g))'] % 0.82/1.03 Parameter b:Type. % 0.82/1.03 Parameter a:Type. % 0.82/1.03 Parameter g:(b->a). % 0.82/1.03 Parameter f:(b->a). % 0.82/1.03 Trying to prove (((or (forall (Q:((b->a)->Prop)), ((Q f)->(Q g)))) (forall (Xx:b), (((eq a) (f Xx)) (g Xx))))->(((eq (b->a)) f) g)) % 0.82/1.03 Found eq_substitution00000:=(eq_substitution0000 (fun (x2:(b->a))=> x2)):((((eq (b->a)) f) g)->(((eq (b->a)) f) g)) % 0.82/1.03 Found (eq_substitution0000 (fun (x2:(b->a))=> x2)) as proof of ((forall (Q:((b->a)->Prop)), ((Q f)->(Q g)))->(((eq (b->a)) f) g)) % 0.82/1.03 Found ((eq_substitution000 g) (fun (x2:(b->a))=> x2)) as proof of ((forall (Q:((b->a)->Prop)), ((Q f)->(Q g)))->(((eq (b->a)) f) g)) % 0.82/1.03 Found (((eq_substitution00 f) g) (fun (x2:(b->a))=> x2)) as proof of ((forall (Q:((b->a)->Prop)), ((Q f)->(Q g)))->(((eq (b->a)) f) g)) % 0.82/1.03 Found ((((eq_substitution0 (b->a)) f) g) (fun (x2:(b->a))=> x2)) as proof of ((forall (Q:((b->a)->Prop)), ((Q f)->(Q g)))->(((eq (b->a)) f) g)) % 0.82/1.03 Found (((((eq_substitution (b->a)) (b->a)) f) g) (fun (x2:(b->a))=> x2)) as proof of ((forall (Q:((b->a)->Prop)), ((Q f)->(Q g)))->(((eq (b->a)) f) g)) % 0.82/1.03 Found (((((eq_substitution (b->a)) (b->a)) f) g) (fun (x2:(b->a))=> x2)) as proof of ((forall (Q:((b->a)->Prop)), ((Q f)->(Q g)))->(((eq (b->a)) f) g)) % 0.82/1.03 Found functional_extensionality0000:=(functional_extensionality000 g):((forall (x:b), (((eq a) (f x)) (g x)))->(((eq (b->a)) f) g)) % 0.82/1.03 Found (functional_extensionality000 g) as proof of ((forall (Xx:b), (((eq a) (f Xx)) (g Xx)))->(((eq (b->a)) f) g)) % 0.82/1.03 Found ((functional_extensionality00 f) g) as proof of ((forall (Xx:b), (((eq a) (f Xx)) (g Xx)))->(((eq (b->a)) f) g)) % 0.82/1.03 Found (((functional_extensionality0 a) f) g) as proof of ((forall (Xx:b), (((eq a) (f Xx)) (g Xx)))->(((eq (b->a)) f) g)) % 0.82/1.03 Found ((((functional_extensionality b) a) f) g) as proof of ((forall (Xx:b), (((eq a) (f Xx)) (g Xx)))->(((eq (b->a)) f) g)) % 0.82/1.03 Found ((((functional_extensionality b) a) f) g) as proof of ((forall (Xx:b), (((eq a) (f Xx)) (g Xx)))->(((eq (b->a)) f) g)) % 0.82/1.03 Found ((or_ind00 (((((eq_substitution (b->a)) (b->a)) f) g) (fun (x2:(b->a))=> x2))) ((((functional_extensionality b) a) f) g)) as proof of (((eq (b->a)) f) g) % 0.82/1.03 Found (((or_ind0 (((eq (b->a)) f) g)) (((((eq_substitution (b->a)) (b->a)) f) g) (fun (x2:(b->a))=> x2))) ((((functional_extensionality b) a) f) g)) as proof of (((eq (b->a)) f) g) % 0.82/1.03 Found ((((fun (P:Prop) (x0:((forall (Q:((b->a)->Prop)), ((Q f)->(Q g)))->P)) (x1:((forall (Xx:b), (((eq a) (f Xx)) (g Xx)))->P))=> ((((((or_ind (forall (Q:((b->a)->Prop)), ((Q f)->(Q g)))) (forall (Xx:b), (((eq a) (f Xx)) (g Xx)))) P) x0) x1) x)) (((eq (b->a)) f) g)) (((((eq_substitution (b->a)) (b->a)) f) g) (fun (x2:(b->a))=> x2))) ((((functional_extensionality b) a) f) g)) as proof of (((eq (b->a)) f) g) % 0.82/1.03 Found (fun (x:((or (forall (Q:((b->a)->Prop)), ((Q f)->(Q g)))) (forall (Xx:b), (((eq a) (f Xx)) (g Xx)))))=> ((((fun (P:Prop) (x0:((forall (Q:((b->a)->Prop)), ((Q f)->(Q g)))->P)) (x1:((forall (Xx:b), (((eq a) (f Xx)) (g Xx)))->P))=> ((((((or_ind (forall (Q:((b->a)->Prop)), ((Q f)->(Q g)))) (forall (Xx:b), (((eq a) (f Xx)) (g Xx)))) P) x0) x1) x)) (((eq (b->a)) f) g)) (((((eq_substitution (b->a)) (b->a)) f) g) (fun (x2:(b->a))=> x2))) ((((functional_extensionality b) a) f) g))) as proof of (((eq (b->a)) f) g) % 0.82/1.04 Found (fun (x:((or (forall (Q:((b->a)->Prop)), ((Q f)->(Q g)))) (forall (Xx:b), (((eq a) (f Xx)) (g Xx)))))=> ((((fun (P:Prop) (x0:((forall (Q:((b->a)->Prop)), ((Q f)->(Q g)))->P)) (x1:((forall (Xx:b), (((eq a) (f Xx)) (g Xx)))->P))=> ((((((or_ind (forall (Q:((b->a)->Prop)), ((Q f)->(Q g)))) (forall (Xx:b), (((eq a) (f Xx)) (g Xx)))) P) x0) x1) x)) (((eq (b->a)) f) g)) (((((eq_substitution (b->a)) (b->a)) f) g) (fun (x2:(b->a))=> x2))) ((((functional_extensionality b) a) f) g))) as proof of (((or (forall (Q:((b->a)->Prop)), ((Q f)->(Q g)))) (forall (Xx:b), (((eq a) (f Xx)) (g Xx))))->(((eq (b->a)) f) g)) % 0.82/1.04 Got proof (fun (x:((or (forall (Q:((b->a)->Prop)), ((Q f)->(Q g)))) (forall (Xx:b), (((eq a) (f Xx)) (g Xx)))))=> ((((fun (P:Prop) (x0:((forall (Q:((b->a)->Prop)), ((Q f)->(Q g)))->P)) (x1:((forall (Xx:b), (((eq a) (f Xx)) (g Xx)))->P))=> ((((((or_ind (forall (Q:((b->a)->Prop)), ((Q f)->(Q g)))) (forall (Xx:b), (((eq a) (f Xx)) (g Xx)))) P) x0) x1) x)) (((eq (b->a)) f) g)) (((((eq_substitution (b->a)) (b->a)) f) g) (fun (x2:(b->a))=> x2))) ((((functional_extensionality b) a) f) g))) % 0.82/1.04 Time elapsed = 0.409132s % 0.82/1.04 node=85 cost=-313.000000 depth=9 % 0.82/1.04 :::::::::::::::::::::: % 0.82/1.04 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.82/1.04 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.82/1.04 (fun (x:((or (forall (Q:((b->a)->Prop)), ((Q f)->(Q g)))) (forall (Xx:b), (((eq a) (f Xx)) (g Xx)))))=> ((((fun (P:Prop) (x0:((forall (Q:((b->a)->Prop)), ((Q f)->(Q g)))->P)) (x1:((forall (Xx:b), (((eq a) (f Xx)) (g Xx)))->P))=> ((((((or_ind (forall (Q:((b->a)->Prop)), ((Q f)->(Q g)))) (forall (Xx:b), (((eq a) (f Xx)) (g Xx)))) P) x0) x1) x)) (((eq (b->a)) f) g)) (((((eq_substitution (b->a)) (b->a)) f) g) (fun (x2:(b->a))=> x2))) ((((functional_extensionality b) a) f) g))) % 0.82/1.04 % SZS output end Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p %------------------------------------------------------------------------------