%------------------------------------------------------------------------------ % File : cocATP---0.2.0 % Problem : ITP209^3 : TPTP v7.6.0. Released v7.6.0. % Transfm : none % Format : tptp:raw % Command : python CASC.py /export/starexec/sandbox2/benchmark/theBenchmark.p % Computer : n027.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 17:47:30 EDT 2022 % Result : Theorem 3.17s 3.35s % Output : Proof 3.17s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.04/0.11 % Problem : ITP209^3 : TPTP v7.6.0. Released v7.6.0. % 0.04/0.12 % Command : python CASC.py /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.13/0.33 Computer : n027.cluster.edu % 0.13/0.33 Model : x86_64 x86_64 % 0.13/0.33 CPUModel : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.33 RAMPerCPU : 8042.1875MB % 0.13/0.33 OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.33 % CPULimit : 300 % 0.13/0.33 % DateTime : Fri Mar 18 09:24:34 EDT 2022 % 0.13/0.33 % CPUTime : % 0.13/0.34 ModuleCmd_Load.c(213):ERROR:105: Unable to locate a modulefile for 'python/python27' % 0.13/0.34 Python 2.7.5 % 0.40/0.61 Using paths ['/home/cristobal/cocATP/CASC/TPTP/', '/export/starexec/sandbox2/benchmark/', '/export/starexec/sandbox2/benchmark/'] % 0.40/0.61 FOF formula (<kernel.Constant object at 0x2375368>, <kernel.Type object at 0x2375098>) of role type named ty_n_tf__a % 0.40/0.61 Using role type % 0.40/0.61 Declaring a:Type % 0.40/0.61 FOF formula (<kernel.Constant object at 0x2375ea8>, <kernel.DependentProduct object at 0x2375758>) of role type named sy_c_Syntax__Match_Oac__operator_001tf__a % 0.40/0.61 Using role type % 0.40/0.61 Declaring syntax_ac_operator_a:((a->(a->a))->Prop) % 0.40/0.61 FOF formula (<kernel.Constant object at 0x2b5ac9efcea8>, <kernel.Constant object at 0x2375ea8>) of role type named sy_v_a % 0.40/0.61 Using role type % 0.40/0.61 Declaring a2:a % 0.40/0.61 FOF formula (<kernel.Constant object at 0x2b5ac9efc1b8>, <kernel.Constant object at 0x2375ea8>) of role type named sy_v_b % 0.40/0.61 Using role type % 0.40/0.61 Declaring b:a % 0.40/0.61 FOF formula (<kernel.Constant object at 0x2b5ac9efcea8>, <kernel.Constant object at 0x2375ea8>) of role type named sy_v_c % 0.40/0.61 Using role type % 0.40/0.61 Declaring c:a % 0.40/0.61 FOF formula (<kernel.Constant object at 0x2b5ac9efcea8>, <kernel.DependentProduct object at 0x2375128>) of role type named sy_v_f % 0.40/0.61 Using role type % 0.40/0.61 Declaring f:(a->(a->a)) % 0.40/0.61 FOF formula (syntax_ac_operator_a f) of role axiom named fact_0_ac__operator__axioms % 0.40/0.61 A new axiom: (syntax_ac_operator_a f) % 0.40/0.61 FOF formula (forall (A:a) (B:a), (((eq a) ((f A) B)) ((f B) A))) of role axiom named fact_1_commute % 0.40/0.61 A new axiom: (forall (A:a) (B:a), (((eq a) ((f A) B)) ((f B) A))) % 0.40/0.61 FOF formula (forall (A:a) (B:a) (C:a), (((eq a) ((f A) ((f B) C))) ((f B) ((f A) C)))) of role axiom named fact_2_left__commute % 0.40/0.61 A new axiom: (forall (A:a) (B:a) (C:a), (((eq a) ((f A) ((f B) C))) ((f B) ((f A) C)))) % 0.40/0.61 FOF formula (forall (A:a) (B:a) (C:a), (((eq a) ((f ((f A) B)) C)) ((f A) ((f B) C)))) of role axiom named fact_3_right__assoc % 0.40/0.61 A new axiom: (forall (A:a) (B:a) (C:a), (((eq a) ((f ((f A) B)) C)) ((f A) ((f B) C)))) % 0.40/0.61 FOF formula (forall (F:(a->(a->a))), ((forall (A2:a) (B2:a) (C2:a), (((eq a) ((F ((F A2) B2)) C2)) ((F A2) ((F B2) C2))))->((forall (A2:a) (B2:a), (((eq a) ((F A2) B2)) ((F B2) A2)))->(syntax_ac_operator_a F)))) of role axiom named fact_4_ac__operator_Ointro % 0.40/0.61 A new axiom: (forall (F:(a->(a->a))), ((forall (A2:a) (B2:a) (C2:a), (((eq a) ((F ((F A2) B2)) C2)) ((F A2) ((F B2) C2))))->((forall (A2:a) (B2:a), (((eq a) ((F A2) B2)) ((F B2) A2)))->(syntax_ac_operator_a F)))) % 0.40/0.61 FOF formula (forall (F:(a->(a->a))) (A:a) (B:a), ((syntax_ac_operator_a F)->(((eq a) ((F A) B)) ((F B) A)))) of role axiom named fact_5_ac__operator_Ocommute % 0.40/0.61 A new axiom: (forall (F:(a->(a->a))) (A:a) (B:a), ((syntax_ac_operator_a F)->(((eq a) ((F A) B)) ((F B) A)))) % 0.40/0.61 FOF formula (forall (F:(a->(a->a))) (A:a) (B:a) (C:a), ((syntax_ac_operator_a F)->(((eq a) ((F A) ((F B) C))) ((F ((F A) B)) C)))) of role axiom named fact_6_ac__operator_Oleft__assoc % 0.40/0.61 A new axiom: (forall (F:(a->(a->a))) (A:a) (B:a) (C:a), ((syntax_ac_operator_a F)->(((eq a) ((F A) ((F B) C))) ((F ((F A) B)) C)))) % 0.40/0.61 FOF formula (forall (F:(a->(a->a))) (A:a) (B:a) (C:a), ((syntax_ac_operator_a F)->(((eq a) ((F ((F A) B)) C)) ((F A) ((F B) C))))) of role axiom named fact_7_ac__operator_Oright__assoc % 0.40/0.61 A new axiom: (forall (F:(a->(a->a))) (A:a) (B:a) (C:a), ((syntax_ac_operator_a F)->(((eq a) ((F ((F A) B)) C)) ((F A) ((F B) C))))) % 0.40/0.61 FOF formula (forall (F:(a->(a->a))) (A:a) (B:a) (C:a), ((syntax_ac_operator_a F)->(((eq a) ((F A) ((F B) C))) ((F B) ((F A) C))))) of role axiom named fact_8_ac__operator_Oleft__commute % 0.40/0.61 A new axiom: (forall (F:(a->(a->a))) (A:a) (B:a) (C:a), ((syntax_ac_operator_a F)->(((eq a) ((F A) ((F B) C))) ((F B) ((F A) C))))) % 0.40/0.61 FOF formula (((eq ((a->(a->a))->Prop)) syntax_ac_operator_a) (fun (F2:(a->(a->a)))=> ((and (forall (A3:a) (B3:a) (C3:a), (((eq a) ((F2 ((F2 A3) B3)) C3)) ((F2 A3) ((F2 B3) C3))))) (forall (A3:a) (B3:a), (((eq a) ((F2 A3) B3)) ((F2 B3) A3)))))) of role axiom named fact_9_ac__operator__def % 0.40/0.61 A new axiom: (((eq ((a->(a->a))->Prop)) syntax_ac_operator_a) (fun (F2:(a->(a->a)))=> ((and (forall (A3:a) (B3:a) (C3:a), (((eq a) ((F2 ((F2 A3) B3)) C3)) ((F2 A3) ((F2 B3) C3))))) (forall (A3:a) (B3:a), (((eq a) ((F2 A3) B3)) ((F2 B3) A3)))))) % 0.40/0.61 FOF formula (((eq a) ((f ((f a2) b)) c)) ((f ((f a2) c)) b)) of role conjecture named conj_0 % 3.10/3.32 Conjecture to prove = (((eq a) ((f ((f a2) b)) c)) ((f ((f a2) c)) b)):Prop % 3.10/3.32 We need to prove ['(((eq a) ((f ((f a2) b)) c)) ((f ((f a2) c)) b))'] % 3.10/3.32 Parameter a:Type. % 3.10/3.32 Parameter syntax_ac_operator_a:((a->(a->a))->Prop). % 3.10/3.32 Parameter a2:a. % 3.10/3.32 Parameter b:a. % 3.10/3.32 Parameter c:a. % 3.10/3.32 Parameter f:(a->(a->a)). % 3.10/3.32 Axiom fact_0_ac__operator__axioms:(syntax_ac_operator_a f). % 3.10/3.32 Axiom fact_1_commute:(forall (A:a) (B:a), (((eq a) ((f A) B)) ((f B) A))). % 3.10/3.32 Axiom fact_2_left__commute:(forall (A:a) (B:a) (C:a), (((eq a) ((f A) ((f B) C))) ((f B) ((f A) C)))). % 3.10/3.32 Axiom fact_3_right__assoc:(forall (A:a) (B:a) (C:a), (((eq a) ((f ((f A) B)) C)) ((f A) ((f B) C)))). % 3.10/3.32 Axiom fact_4_ac__operator_Ointro:(forall (F:(a->(a->a))), ((forall (A2:a) (B2:a) (C2:a), (((eq a) ((F ((F A2) B2)) C2)) ((F A2) ((F B2) C2))))->((forall (A2:a) (B2:a), (((eq a) ((F A2) B2)) ((F B2) A2)))->(syntax_ac_operator_a F)))). % 3.10/3.32 Axiom fact_5_ac__operator_Ocommute:(forall (F:(a->(a->a))) (A:a) (B:a), ((syntax_ac_operator_a F)->(((eq a) ((F A) B)) ((F B) A)))). % 3.10/3.32 Axiom fact_6_ac__operator_Oleft__assoc:(forall (F:(a->(a->a))) (A:a) (B:a) (C:a), ((syntax_ac_operator_a F)->(((eq a) ((F A) ((F B) C))) ((F ((F A) B)) C)))). % 3.10/3.32 Axiom fact_7_ac__operator_Oright__assoc:(forall (F:(a->(a->a))) (A:a) (B:a) (C:a), ((syntax_ac_operator_a F)->(((eq a) ((F ((F A) B)) C)) ((F A) ((F B) C))))). % 3.10/3.32 Axiom fact_8_ac__operator_Oleft__commute:(forall (F:(a->(a->a))) (A:a) (B:a) (C:a), ((syntax_ac_operator_a F)->(((eq a) ((F A) ((F B) C))) ((F B) ((F A) C))))). % 3.10/3.32 Axiom fact_9_ac__operator__def:(((eq ((a->(a->a))->Prop)) syntax_ac_operator_a) (fun (F2:(a->(a->a)))=> ((and (forall (A3:a) (B3:a) (C3:a), (((eq a) ((F2 ((F2 A3) B3)) C3)) ((F2 A3) ((F2 B3) C3))))) (forall (A3:a) (B3:a), (((eq a) ((F2 A3) B3)) ((F2 B3) A3)))))). % 3.10/3.32 Trying to prove (((eq a) ((f ((f a2) b)) c)) ((f ((f a2) c)) b)) % 3.10/3.32 Found fact_3_right__assoc0000:=(fact_3_right__assoc000 P):((P ((f ((f a2) b)) c))->(P ((f a2) ((f b) c)))) % 3.10/3.32 Found (fact_3_right__assoc000 P) as proof of ((P ((f ((f a2) b)) c))->(P ((f a2) ((f b) c)))) % 3.10/3.32 Found ((fact_3_right__assoc00 c) P) as proof of ((P ((f ((f a2) b)) c))->(P ((f a2) ((f b) c)))) % 3.10/3.32 Found (((fact_3_right__assoc0 b) c) P) as proof of ((P ((f ((f a2) b)) c))->(P ((f a2) ((f b) c)))) % 3.10/3.32 Found ((((fact_3_right__assoc a2) b) c) P) as proof of ((P ((f ((f a2) b)) c))->(P ((f a2) ((f b) c)))) % 3.10/3.32 Found ((((fact_3_right__assoc a2) b) c) P) as proof of ((P ((f ((f a2) b)) c))->(P ((f a2) ((f b) c)))) % 3.10/3.32 Found (fact_2_left__commute0000 ((((fact_3_right__assoc a2) b) c) P)) as proof of ((P ((f ((f a2) b)) c))->(P ((f b) ((f a2) c)))) % 3.10/3.32 Found ((fact_2_left__commute000 (fun (x0:a)=> ((P ((f ((f a2) b)) c))->(P x0)))) ((((fact_3_right__assoc a2) b) c) P)) as proof of ((P ((f ((f a2) b)) c))->(P ((f b) ((f a2) c)))) % 3.10/3.32 Found (((fact_2_left__commute00 c) (fun (x0:a)=> ((P ((f ((f a2) b)) c))->(P x0)))) ((((fact_3_right__assoc a2) b) c) P)) as proof of ((P ((f ((f a2) b)) c))->(P ((f b) ((f a2) c)))) % 3.10/3.32 Found ((((fact_2_left__commute0 b) c) (fun (x0:a)=> ((P ((f ((f a2) b)) c))->(P x0)))) ((((fact_3_right__assoc a2) b) c) P)) as proof of ((P ((f ((f a2) b)) c))->(P ((f b) ((f a2) c)))) % 3.10/3.32 Found (((((fact_2_left__commute a2) b) c) (fun (x0:a)=> ((P ((f ((f a2) b)) c))->(P x0)))) ((((fact_3_right__assoc a2) b) c) P)) as proof of ((P ((f ((f a2) b)) c))->(P ((f b) ((f a2) c)))) % 3.10/3.32 Found (((((fact_2_left__commute a2) b) c) (fun (x0:a)=> ((P ((f ((f a2) b)) c))->(P x0)))) ((((fact_3_right__assoc a2) b) c) P)) as proof of ((P ((f ((f a2) b)) c))->(P ((f b) ((f a2) c)))) % 3.10/3.32 Found (fact_1_commute000 (((((fact_2_left__commute a2) b) c) (fun (x0:a)=> ((P ((f ((f a2) b)) c))->(P x0)))) ((((fact_3_right__assoc a2) b) c) P))) as proof of ((P ((f ((f a2) b)) c))->(P ((f ((f a2) c)) b))) % 3.10/3.32 Found ((fact_1_commute00 (fun (x0:a)=> ((P ((f ((f a2) b)) c))->(P x0)))) (((((fact_2_left__commute a2) b) c) (fun (x0:a)=> ((P ((f ((f a2) b)) c))->(P x0)))) ((((fact_3_right__assoc a2) b) c) P))) as proof of ((P ((f ((f a2) b)) c))->(P ((f ((f a2) c)) b))) % 3.10/3.32 Found (((fact_1_commute0 ((f a2) c)) (fun (x0:a)=> ((P ((f ((f a2) b)) c))->(P x0)))) (((((fact_2_left__commute a2) b) c) (fun (x0:a)=> ((P ((f ((f a2) b)) c))->(P x0)))) ((((fact_3_right__assoc a2) b) c) P))) as proof of ((P ((f ((f a2) b)) c))->(P ((f ((f a2) c)) b))) % 3.17/3.35 Found ((((fact_1_commute b) ((f a2) c)) (fun (x0:a)=> ((P ((f ((f a2) b)) c))->(P x0)))) (((((fact_2_left__commute a2) b) c) (fun (x0:a)=> ((P ((f ((f a2) b)) c))->(P x0)))) ((((fact_3_right__assoc a2) b) c) P))) as proof of ((P ((f ((f a2) b)) c))->(P ((f ((f a2) c)) b))) % 3.17/3.35 Found (fun (P:(a->Prop))=> ((((fact_1_commute b) ((f a2) c)) (fun (x0:a)=> ((P ((f ((f a2) b)) c))->(P x0)))) (((((fact_2_left__commute a2) b) c) (fun (x0:a)=> ((P ((f ((f a2) b)) c))->(P x0)))) ((((fact_3_right__assoc a2) b) c) P)))) as proof of ((P ((f ((f a2) b)) c))->(P ((f ((f a2) c)) b))) % 3.17/3.35 Found (fun (P:(a->Prop))=> ((((fact_1_commute b) ((f a2) c)) (fun (x0:a)=> ((P ((f ((f a2) b)) c))->(P x0)))) (((((fact_2_left__commute a2) b) c) (fun (x0:a)=> ((P ((f ((f a2) b)) c))->(P x0)))) ((((fact_3_right__assoc a2) b) c) P)))) as proof of (((eq a) ((f ((f a2) b)) c)) ((f ((f a2) c)) b)) % 3.17/3.35 Got proof (fun (P:(a->Prop))=> ((((fact_1_commute b) ((f a2) c)) (fun (x0:a)=> ((P ((f ((f a2) b)) c))->(P x0)))) (((((fact_2_left__commute a2) b) c) (fun (x0:a)=> ((P ((f ((f a2) b)) c))->(P x0)))) ((((fact_3_right__assoc a2) b) c) P)))) % 3.17/3.35 Time elapsed = 2.637226s % 3.17/3.35 node=671 cost=-103.000000 depth=16 % 3.17/3.35 :::::::::::::::::::::: % 3.17/3.35 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 3.17/3.35 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p % 3.17/3.35 (fun (P:(a->Prop))=> ((((fact_1_commute b) ((f a2) c)) (fun (x0:a)=> ((P ((f ((f a2) b)) c))->(P x0)))) (((((fact_2_left__commute a2) b) c) (fun (x0:a)=> ((P ((f ((f a2) b)) c))->(P x0)))) ((((fact_3_right__assoc a2) b) c) P)))) % 3.17/3.35 % SZS output end Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p %------------------------------------------------------------------------------