%------------------------------------------------------------------------------
% File : Z3---4.15.1
% Problem : TOP022+1 : TPTP v9.0.0. Released v3.1.0.
% Transfm : none
% Format : tptp
% Command : run_E %s %d THM
% Computer : n013.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 : 300s
% DateTime : Sat Jun 21 05:42:37 AM UTC 2025
% Result : Theorem 0.17s 0.36s
% Output : Proof 0.17s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.10/0.11 % Problem : TOP022+1 : TPTP v9.0.0. Released v3.1.0.
% 0.10/0.11 % Command : run_E %s %d THM
% 0.10/0.32 % Computer : n013.cluster.edu
% 0.10/0.32 % Model : x86_64 x86_64
% 0.10/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.32 % Memory : 8042.1875MB
% 0.10/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.10/0.32 % CPULimit : 300
% 0.10/0.32 % WCLimit : 300
% 0.10/0.32 % DateTime : Fri Jun 20 13:52:23 EDT 2025
% 0.10/0.32 % CPUTime :
% 0.17/0.36 % SZS status Theorem
% 0.17/0.36 % SZS output start Proof
% 0.17/0.36 tff(a_group_isomorphism_from_to_type, type, (
% 0.17/0.36 a_group_isomorphism_from_to: ( $i * $i * $i ) > $o)).
% 0.17/0.36 tff(first_homotop_grp_type, type, (
% 0.17/0.36 first_homotop_grp: ( $i * $i ) > $i)).
% 0.17/0.36 tff(tptp_fun_X1_2_type, type, (
% 0.17/0.36 tptp_fun_X1_2: $i)).
% 0.17/0.36 tff(tptp_fun_X_4_type, type, (
% 0.17/0.36 tptp_fun_X_4: $i)).
% 0.17/0.36 tff(tptp_fun_X0_3_type, type, (
% 0.17/0.36 tptp_fun_X0_3: $i)).
% 0.17/0.36 tff(alpha_hat_type, type, (
% 0.17/0.36 alpha_hat: $i > $i)).
% 0.17/0.36 tff(tptp_fun_P_1_type, type, (
% 0.17/0.36 tptp_fun_P_1: ( $i * $i * $i ) > $i)).
% 0.17/0.36 tff(a_path_from_to_in_type, type, (
% 0.17/0.36 a_path_from_to_in: ( $i * $i * $i * $i ) > $o)).
% 0.17/0.36 tff(a_member_of_type, type, (
% 0.17/0.36 a_member_of: ( $i * $i ) > $o)).
% 0.17/0.36 tff(path_connected_type, type, (
% 0.17/0.36 path_connected: $i > $o)).
% 0.17/0.36 tff(isomorphic_groups_type, type, (
% 0.17/0.36 isomorphic_groups: ( $i * $i ) > $o)).
% 0.17/0.36 tff(tptp_fun_F_0_type, type, (
% 0.17/0.36 tptp_fun_F_0: ( $i * $i ) > $i)).
% 0.17/0.36 tff(1,plain,
% 0.17/0.36 (^[X: $i, X0: $i, X1: $i] : refl((~((~((~path_connected(X)) | a_path_from_to_in(tptp_fun_P_1(X1, X0, X), X0, X1, X) | (~a_member_of(X0, X)) | (~a_member_of(X1, X)))) | (~(path_connected(X) | (~((~a_member_of(X0, X)) | (~a_member_of(X1, X)) | (~![P: $i] : (~a_path_from_to_in(P, X0, X1, X))))))))) <=> (~((~((~path_connected(X)) | a_path_from_to_in(tptp_fun_P_1(X1, X0, X), X0, X1, X) | (~a_member_of(X0, X)) | (~a_member_of(X1, X)))) | (~(path_connected(X) | (~((~a_member_of(X0, X)) | (~a_member_of(X1, X)) | (~![P: $i] : (~a_path_from_to_in(P, X0, X1, X))))))))))),
% 0.17/0.36 inference(bind,[status(th)],[])).
% 0.17/0.36 tff(2,plain,
% 0.17/0.36 (![X: $i, X0: $i, X1: $i] : (~((~((~path_connected(X)) | a_path_from_to_in(tptp_fun_P_1(X1, X0, X), X0, X1, X) | (~a_member_of(X0, X)) | (~a_member_of(X1, X)))) | (~(path_connected(X) | (~((~a_member_of(X0, X)) | (~a_member_of(X1, X)) | (~![P: $i] : (~a_path_from_to_in(P, X0, X1, X))))))))) <=> ![X: $i, X0: $i, X1: $i] : (~((~((~path_connected(X)) | a_path_from_to_in(tptp_fun_P_1(X1, X0, X), X0, X1, X) | (~a_member_of(X0, X)) | (~a_member_of(X1, X)))) | (~(path_connected(X) | (~((~a_member_of(X0, X)) | (~a_member_of(X1, X)) | (~![P: $i] : (~a_path_from_to_in(P, X0, X1, X)))))))))),
% 0.17/0.36 inference(quant_intro,[status(thm)],[1])).
% 0.17/0.36 tff(3,plain,
% 0.17/0.36 (^[X: $i, X0: $i, X1: $i] : rewrite((~((~((~path_connected(X)) | a_path_from_to_in(tptp_fun_P_1(X1, X0, X), X0, X1, X) | (~a_member_of(X0, X)) | (~a_member_of(X1, X)))) | (~(path_connected(X) | (~((~a_member_of(X0, X)) | (~a_member_of(X1, X)) | (~![P: $i] : (~a_path_from_to_in(P, X0, X1, X))))))))) <=> (~((~((~path_connected(X)) | a_path_from_to_in(tptp_fun_P_1(X1, X0, X), X0, X1, X) | (~a_member_of(X0, X)) | (~a_member_of(X1, X)))) | (~(path_connected(X) | (~((~a_member_of(X0, X)) | (~a_member_of(X1, X)) | (~![P: $i] : (~a_path_from_to_in(P, X0, X1, X))))))))))),
% 0.17/0.36 inference(bind,[status(th)],[])).
% 0.17/0.36 tff(4,plain,
% 0.17/0.36 (![X: $i, X0: $i, X1: $i] : (~((~((~path_connected(X)) | a_path_from_to_in(tptp_fun_P_1(X1, X0, X), X0, X1, X) | (~a_member_of(X0, X)) | (~a_member_of(X1, X)))) | (~(path_connected(X) | (~((~a_member_of(X0, X)) | (~a_member_of(X1, X)) | (~![P: $i] : (~a_path_from_to_in(P, X0, X1, X))))))))) <=> ![X: $i, X0: $i, X1: $i] : (~((~((~path_connected(X)) | a_path_from_to_in(tptp_fun_P_1(X1, X0, X), X0, X1, X) | (~a_member_of(X0, X)) | (~a_member_of(X1, X)))) | (~(path_connected(X) | (~((~a_member_of(X0, X)) | (~a_member_of(X1, X)) | (~![P: $i] : (~a_path_from_to_in(P, X0, X1, X)))))))))),
% 0.17/0.36 inference(quant_intro,[status(thm)],[3])).
% 0.17/0.36 tff(5,plain,
% 0.17/0.36 (![X: $i, X0: $i, X1: $i] : (~((~((~path_connected(X)) | a_path_from_to_in(tptp_fun_P_1(X1, X0, X), X0, X1, X) | (~a_member_of(X0, X)) | (~a_member_of(X1, X)))) | (~(path_connected(X) | (~((~a_member_of(X0, X)) | (~a_member_of(X1, X)) | (~![P: $i] : (~a_path_from_to_in(P, X0, X1, X))))))))) <=> ![X: $i, X0: $i, X1: $i] : (~((~((~path_connected(X)) | a_path_from_to_in(tptp_fun_P_1(X1, X0, X), X0, X1, X) | (~a_member_of(X0, X)) | (~a_member_of(X1, X)))) | (~(path_connected(X) | (~((~a_member_of(X0, X)) | (~a_member_of(X1, X)) | (~![P: $i] : (~a_path_from_to_in(P, X0, X1, X)))))))))),
% 0.17/0.36 inference(transitivity,[status(thm)],[4, 2])).
% 0.17/0.36 tff(6,plain,
% 0.17/0.36 (^[X: $i, X0: $i, X1: $i] : trans(monotonicity(trans(monotonicity(trans(monotonicity(rewrite((a_member_of(X0, X) & a_member_of(X1, X)) <=> (~((~a_member_of(X0, X)) | (~a_member_of(X1, X))))), ((~(a_member_of(X0, X) & a_member_of(X1, X))) <=> (~(~((~a_member_of(X0, X)) | (~a_member_of(X1, X))))))), rewrite((~(~((~a_member_of(X0, X)) | (~a_member_of(X1, X))))) <=> ((~a_member_of(X0, X)) | (~a_member_of(X1, X)))), ((~(a_member_of(X0, X) & a_member_of(X1, X))) <=> ((~a_member_of(X0, X)) | (~a_member_of(X1, X))))), (((~(a_member_of(X0, X) & a_member_of(X1, X))) | (~path_connected(X)) | a_path_from_to_in(tptp_fun_P_1(X1, X0, X), X0, X1, X)) <=> (((~a_member_of(X0, X)) | (~a_member_of(X1, X))) | (~path_connected(X)) | a_path_from_to_in(tptp_fun_P_1(X1, X0, X), X0, X1, X)))), rewrite((((~a_member_of(X0, X)) | (~a_member_of(X1, X))) | (~path_connected(X)) | a_path_from_to_in(tptp_fun_P_1(X1, X0, X), X0, X1, X)) <=> ((~path_connected(X)) | a_path_from_to_in(tptp_fun_P_1(X1, X0, X), X0, X1, X) | (~a_member_of(X0, X)) | (~a_member_of(X1, X)))), (((~(a_member_of(X0, X) & a_member_of(X1, X))) | (~path_connected(X)) | a_path_from_to_in(tptp_fun_P_1(X1, X0, X), X0, X1, X)) <=> ((~path_connected(X)) | a_path_from_to_in(tptp_fun_P_1(X1, X0, X), X0, X1, X) | (~a_member_of(X0, X)) | (~a_member_of(X1, X))))), rewrite((path_connected(X) | (a_member_of(X0, X) & a_member_of(X1, X) & ![P: $i] : (~a_path_from_to_in(P, X0, X1, X)))) <=> (path_connected(X) | (~((~a_member_of(X0, X)) | (~a_member_of(X1, X)) | (~![P: $i] : (~a_path_from_to_in(P, X0, X1, X))))))), ((((~(a_member_of(X0, X) & a_member_of(X1, X))) | (~path_connected(X)) | a_path_from_to_in(tptp_fun_P_1(X1, X0, X), X0, X1, X)) & (path_connected(X) | (a_member_of(X0, X) & a_member_of(X1, X) & ![P: $i] : (~a_path_from_to_in(P, X0, X1, X))))) <=> (((~path_connected(X)) | a_path_from_to_in(tptp_fun_P_1(X1, X0, X), X0, X1, X) | (~a_member_of(X0, X)) | (~a_member_of(X1, X))) & (path_connected(X) | (~((~a_member_of(X0, X)) | (~a_member_of(X1, X)) | (~![P: $i] : (~a_path_from_to_in(P, X0, X1, X))))))))), rewrite((((~path_connected(X)) | a_path_from_to_in(tptp_fun_P_1(X1, X0, X), X0, X1, X) | (~a_member_of(X0, X)) | (~a_member_of(X1, X))) & (path_connected(X) | (~((~a_member_of(X0, X)) | (~a_member_of(X1, X)) | (~![P: $i] : (~a_path_from_to_in(P, X0, X1, X))))))) <=> (~((~((~path_connected(X)) | a_path_from_to_in(tptp_fun_P_1(X1, X0, X), X0, X1, X) | (~a_member_of(X0, X)) | (~a_member_of(X1, X)))) | (~(path_connected(X) | (~((~a_member_of(X0, X)) | (~a_member_of(X1, X)) | (~![P: $i] : (~a_path_from_to_in(P, X0, X1, X)))))))))), ((((~(a_member_of(X0, X) & a_member_of(X1, X))) | (~path_connected(X)) | a_path_from_to_in(tptp_fun_P_1(X1, X0, X), X0, X1, X)) & (path_connected(X) | (a_member_of(X0, X) & a_member_of(X1, X) & ![P: $i] : (~a_path_from_to_in(P, X0, X1, X))))) <=> (~((~((~path_connected(X)) | a_path_from_to_in(tptp_fun_P_1(X1, X0, X), X0, X1, X) | (~a_member_of(X0, X)) | (~a_member_of(X1, X)))) | (~(path_connected(X) | (~((~a_member_of(X0, X)) | (~a_member_of(X1, X)) | (~![P: $i] : (~a_path_from_to_in(P, X0, X1, X)))))))))))),
% 0.17/0.36 inference(bind,[status(th)],[])).
% 0.17/0.36 tff(7,plain,
% 0.17/0.36 (![X: $i, X0: $i, X1: $i] : (((~(a_member_of(X0, X) & a_member_of(X1, X))) | (~path_connected(X)) | a_path_from_to_in(tptp_fun_P_1(X1, X0, X), X0, X1, X)) & (path_connected(X) | (a_member_of(X0, X) & a_member_of(X1, X) & ![P: $i] : (~a_path_from_to_in(P, X0, X1, X))))) <=> ![X: $i, X0: $i, X1: $i] : (~((~((~path_connected(X)) | a_path_from_to_in(tptp_fun_P_1(X1, X0, X), X0, X1, X) | (~a_member_of(X0, X)) | (~a_member_of(X1, X)))) | (~(path_connected(X) | (~((~a_member_of(X0, X)) | (~a_member_of(X1, X)) | (~![P: $i] : (~a_path_from_to_in(P, X0, X1, X)))))))))),
% 0.17/0.36 inference(quant_intro,[status(thm)],[6])).
% 0.17/0.36 tff(8,plain,
% 0.17/0.36 (^[X: $i, X0: $i, X1: $i] : rewrite((((~path_connected(X)) | ((~(a_member_of(X0, X) & a_member_of(X1, X))) | a_path_from_to_in(tptp_fun_P_1(X1, X0, X), X0, X1, X))) & (path_connected(X) | ((a_member_of(X0, X) & a_member_of(X1, X)) & ![P: $i] : (~a_path_from_to_in(P, X0, X1, X))))) <=> (((~(a_member_of(X0, X) & a_member_of(X1, X))) | (~path_connected(X)) | a_path_from_to_in(tptp_fun_P_1(X1, X0, X), X0, X1, X)) & (path_connected(X) | (a_member_of(X0, X) & a_member_of(X1, X) & ![P: $i] : (~a_path_from_to_in(P, X0, X1, X))))))),
% 0.17/0.36 inference(bind,[status(th)],[])).
% 0.17/0.36 tff(9,plain,
% 0.17/0.36 (![X: $i, X0: $i, X1: $i] : (((~path_connected(X)) | ((~(a_member_of(X0, X) & a_member_of(X1, X))) | a_path_from_to_in(tptp_fun_P_1(X1, X0, X), X0, X1, X))) & (path_connected(X) | ((a_member_of(X0, X) & a_member_of(X1, X)) & ![P: $i] : (~a_path_from_to_in(P, X0, X1, X))))) <=> ![X: $i, X0: $i, X1: $i] : (((~(a_member_of(X0, X) & a_member_of(X1, X))) | (~path_connected(X)) | a_path_from_to_in(tptp_fun_P_1(X1, X0, X), X0, X1, X)) & (path_connected(X) | (a_member_of(X0, X) & a_member_of(X1, X) & ![P: $i] : (~a_path_from_to_in(P, X0, X1, X)))))),
% 0.17/0.36 inference(quant_intro,[status(thm)],[8])).
% 0.17/0.36 tff(10,plain,
% 0.17/0.36 (![X: $i, X0: $i, X1: $i] : (path_connected(X) <=> ((~(a_member_of(X0, X) & a_member_of(X1, X))) | ?[P: $i] : a_path_from_to_in(P, X0, X1, X))) <=> ![X: $i, X0: $i, X1: $i] : (path_connected(X) <=> ((~(a_member_of(X0, X) & a_member_of(X1, X))) | ?[P: $i] : a_path_from_to_in(P, X0, X1, X)))),
% 0.17/0.36 inference(rewrite,[status(thm)],[])).
% 0.17/0.36 tff(11,plain,
% 0.17/0.36 (^[X: $i, X0: $i, X1: $i] : rewrite((path_connected(X) <=> ((a_member_of(X0, X) & a_member_of(X1, X)) => ?[P: $i] : a_path_from_to_in(P, X0, X1, X))) <=> (path_connected(X) <=> ((~(a_member_of(X0, X) & a_member_of(X1, X))) | ?[P: $i] : a_path_from_to_in(P, X0, X1, X))))),
% 0.17/0.36 inference(bind,[status(th)],[])).
% 0.17/0.36 tff(12,plain,
% 0.17/0.36 (![X: $i, X0: $i, X1: $i] : (path_connected(X) <=> ((a_member_of(X0, X) & a_member_of(X1, X)) => ?[P: $i] : a_path_from_to_in(P, X0, X1, X))) <=> ![X: $i, X0: $i, X1: $i] : (path_connected(X) <=> ((~(a_member_of(X0, X) & a_member_of(X1, X))) | ?[P: $i] : a_path_from_to_in(P, X0, X1, X)))),
% 0.17/0.36 inference(quant_intro,[status(thm)],[11])).
% 0.17/0.36 tff(13,axiom,(![X: $i, X0: $i, X1: $i] : (path_connected(X) <=> ((a_member_of(X0, X) & a_member_of(X1, X)) => ?[P: $i] : a_path_from_to_in(P, X0, X1, X)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','path_connected_defn')).
% 0.17/0.36 tff(14,plain,
% 0.17/0.36 (![X: $i, X0: $i, X1: $i] : (path_connected(X) <=> ((~(a_member_of(X0, X) & a_member_of(X1, X))) | ?[P: $i] : a_path_from_to_in(P, X0, X1, X)))),
% 0.17/0.36 inference(modus_ponens,[status(thm)],[13, 12])).
% 0.17/0.36 tff(15,plain,
% 0.17/0.36 (![X: $i, X0: $i, X1: $i] : (path_connected(X) <=> ((~(a_member_of(X0, X) & a_member_of(X1, X))) | ?[P: $i] : a_path_from_to_in(P, X0, X1, X)))),
% 0.17/0.36 inference(modus_ponens,[status(thm)],[14, 10])).
% 0.17/0.36 tff(16,plain,(
% 0.17/0.36 ![X: $i, X0: $i, X1: $i] : (((~path_connected(X)) | ((~(a_member_of(X0, X) & a_member_of(X1, X))) | a_path_from_to_in(tptp_fun_P_1(X1, X0, X), X0, X1, X))) & (path_connected(X) | ((a_member_of(X0, X) & a_member_of(X1, X)) & ![P: $i] : (~a_path_from_to_in(P, X0, X1, X)))))),
% 0.17/0.36 inference(skolemize,[status(sab)],[15])).
% 0.17/0.36 tff(17,plain,
% 0.17/0.36 (![X: $i, X0: $i, X1: $i] : (((~(a_member_of(X0, X) & a_member_of(X1, X))) | (~path_connected(X)) | a_path_from_to_in(tptp_fun_P_1(X1, X0, X), X0, X1, X)) & (path_connected(X) | (a_member_of(X0, X) & a_member_of(X1, X) & ![P: $i] : (~a_path_from_to_in(P, X0, X1, X)))))),
% 0.17/0.36 inference(modus_ponens,[status(thm)],[16, 9])).
% 0.17/0.36 tff(18,plain,
% 0.17/0.36 (![X: $i, X0: $i, X1: $i] : (~((~((~path_connected(X)) | a_path_from_to_in(tptp_fun_P_1(X1, X0, X), X0, X1, X) | (~a_member_of(X0, X)) | (~a_member_of(X1, X)))) | (~(path_connected(X) | (~((~a_member_of(X0, X)) | (~a_member_of(X1, X)) | (~![P: $i] : (~a_path_from_to_in(P, X0, X1, X)))))))))),
% 0.17/0.36 inference(modus_ponens,[status(thm)],[17, 7])).
% 0.17/0.36 tff(19,plain,
% 0.17/0.36 (![X: $i, X0: $i, X1: $i] : (~((~((~path_connected(X)) | a_path_from_to_in(tptp_fun_P_1(X1, X0, X), X0, X1, X) | (~a_member_of(X0, X)) | (~a_member_of(X1, X)))) | (~(path_connected(X) | (~((~a_member_of(X0, X)) | (~a_member_of(X1, X)) | (~![P: $i] : (~a_path_from_to_in(P, X0, X1, X)))))))))),
% 0.17/0.36 inference(modus_ponens,[status(thm)],[18, 5])).
% 0.17/0.36 tff(20,plain,
% 0.17/0.36 (((~![X: $i, X0: $i, X1: $i] : (~((~((~path_connected(X)) | a_path_from_to_in(tptp_fun_P_1(X1, X0, X), X0, X1, X) | (~a_member_of(X0, X)) | (~a_member_of(X1, X)))) | (~(path_connected(X) | (~((~a_member_of(X0, X)) | (~a_member_of(X1, X)) | (~![P: $i] : (~a_path_from_to_in(P, X0, X1, X)))))))))) | (~((~((~a_member_of(X0!3, X!4)) | (~path_connected(X!4)) | (~a_member_of(X1!2, X!4)) | a_path_from_to_in(tptp_fun_P_1(X1!2, X0!3, X!4), X0!3, X1!2, X!4))) | (~(path_connected(X!4) | (~((~a_member_of(X0!3, X!4)) | (~a_member_of(X1!2, X!4)) | (~![P: $i] : (~a_path_from_to_in(P, X0!3, X1!2, X!4)))))))))) <=> ((~![X: $i, X0: $i, X1: $i] : (~((~((~path_connected(X)) | a_path_from_to_in(tptp_fun_P_1(X1, X0, X), X0, X1, X) | (~a_member_of(X0, X)) | (~a_member_of(X1, X)))) | (~(path_connected(X) | (~((~a_member_of(X0, X)) | (~a_member_of(X1, X)) | (~![P: $i] : (~a_path_from_to_in(P, X0, X1, X)))))))))) | (~((~((~a_member_of(X0!3, X!4)) | (~path_connected(X!4)) | (~a_member_of(X1!2, X!4)) | a_path_from_to_in(tptp_fun_P_1(X1!2, X0!3, X!4), X0!3, X1!2, X!4))) | (~(path_connected(X!4) | (~((~a_member_of(X0!3, X!4)) | (~a_member_of(X1!2, X!4)) | (~![P: $i] : (~a_path_from_to_in(P, X0!3, X1!2, X!4))))))))))),
% 0.17/0.36 inference(rewrite,[status(thm)],[])).
% 0.17/0.36 tff(21,plain,
% 0.17/0.36 ((~((~((~path_connected(X!4)) | a_path_from_to_in(tptp_fun_P_1(X1!2, X0!3, X!4), X0!3, X1!2, X!4) | (~a_member_of(X0!3, X!4)) | (~a_member_of(X1!2, X!4)))) | (~(path_connected(X!4) | (~((~a_member_of(X0!3, X!4)) | (~a_member_of(X1!2, X!4)) | (~![P: $i] : (~a_path_from_to_in(P, X0!3, X1!2, X!4))))))))) <=> (~((~((~a_member_of(X0!3, X!4)) | (~path_connected(X!4)) | (~a_member_of(X1!2, X!4)) | a_path_from_to_in(tptp_fun_P_1(X1!2, X0!3, X!4), X0!3, X1!2, X!4))) | (~(path_connected(X!4) | (~((~a_member_of(X0!3, X!4)) | (~a_member_of(X1!2, X!4)) | (~![P: $i] : (~a_path_from_to_in(P, X0!3, X1!2, X!4)))))))))),
% 0.17/0.36 inference(rewrite,[status(thm)],[])).
% 0.17/0.36 tff(22,plain,
% 0.17/0.36 (((~![X: $i, X0: $i, X1: $i] : (~((~((~path_connected(X)) | a_path_from_to_in(tptp_fun_P_1(X1, X0, X), X0, X1, X) | (~a_member_of(X0, X)) | (~a_member_of(X1, X)))) | (~(path_connected(X) | (~((~a_member_of(X0, X)) | (~a_member_of(X1, X)) | (~![P: $i] : (~a_path_from_to_in(P, X0, X1, X)))))))))) | (~((~((~path_connected(X!4)) | a_path_from_to_in(tptp_fun_P_1(X1!2, X0!3, X!4), X0!3, X1!2, X!4) | (~a_member_of(X0!3, X!4)) | (~a_member_of(X1!2, X!4)))) | (~(path_connected(X!4) | (~((~a_member_of(X0!3, X!4)) | (~a_member_of(X1!2, X!4)) | (~![P: $i] : (~a_path_from_to_in(P, X0!3, X1!2, X!4)))))))))) <=> ((~![X: $i, X0: $i, X1: $i] : (~((~((~path_connected(X)) | a_path_from_to_in(tptp_fun_P_1(X1, X0, X), X0, X1, X) | (~a_member_of(X0, X)) | (~a_member_of(X1, X)))) | (~(path_connected(X) | (~((~a_member_of(X0, X)) | (~a_member_of(X1, X)) | (~![P: $i] : (~a_path_from_to_in(P, X0, X1, X)))))))))) | (~((~((~a_member_of(X0!3, X!4)) | (~path_connected(X!4)) | (~a_member_of(X1!2, X!4)) | a_path_from_to_in(tptp_fun_P_1(X1!2, X0!3, X!4), X0!3, X1!2, X!4))) | (~(path_connected(X!4) | (~((~a_member_of(X0!3, X!4)) | (~a_member_of(X1!2, X!4)) | (~![P: $i] : (~a_path_from_to_in(P, X0!3, X1!2, X!4))))))))))),
% 0.17/0.36 inference(monotonicity,[status(thm)],[21])).
% 0.17/0.36 tff(23,plain,
% 0.17/0.36 (((~![X: $i, X0: $i, X1: $i] : (~((~((~path_connected(X)) | a_path_from_to_in(tptp_fun_P_1(X1, X0, X), X0, X1, X) | (~a_member_of(X0, X)) | (~a_member_of(X1, X)))) | (~(path_connected(X) | (~((~a_member_of(X0, X)) | (~a_member_of(X1, X)) | (~![P: $i] : (~a_path_from_to_in(P, X0, X1, X)))))))))) | (~((~((~path_connected(X!4)) | a_path_from_to_in(tptp_fun_P_1(X1!2, X0!3, X!4), X0!3, X1!2, X!4) | (~a_member_of(X0!3, X!4)) | (~a_member_of(X1!2, X!4)))) | (~(path_connected(X!4) | (~((~a_member_of(X0!3, X!4)) | (~a_member_of(X1!2, X!4)) | (~![P: $i] : (~a_path_from_to_in(P, X0!3, X1!2, X!4)))))))))) <=> ((~![X: $i, X0: $i, X1: $i] : (~((~((~path_connected(X)) | a_path_from_to_in(tptp_fun_P_1(X1, X0, X), X0, X1, X) | (~a_member_of(X0, X)) | (~a_member_of(X1, X)))) | (~(path_connected(X) | (~((~a_member_of(X0, X)) | (~a_member_of(X1, X)) | (~![P: $i] : (~a_path_from_to_in(P, X0, X1, X)))))))))) | (~((~((~a_member_of(X0!3, X!4)) | (~path_connected(X!4)) | (~a_member_of(X1!2, X!4)) | a_path_from_to_in(tptp_fun_P_1(X1!2, X0!3, X!4), X0!3, X1!2, X!4))) | (~(path_connected(X!4) | (~((~a_member_of(X0!3, X!4)) | (~a_member_of(X1!2, X!4)) | (~![P: $i] : (~a_path_from_to_in(P, X0!3, X1!2, X!4))))))))))),
% 0.17/0.36 inference(transitivity,[status(thm)],[22, 20])).
% 0.17/0.36 tff(24,plain,
% 0.17/0.36 ((~![X: $i, X0: $i, X1: $i] : (~((~((~path_connected(X)) | a_path_from_to_in(tptp_fun_P_1(X1, X0, X), X0, X1, X) | (~a_member_of(X0, X)) | (~a_member_of(X1, X)))) | (~(path_connected(X) | (~((~a_member_of(X0, X)) | (~a_member_of(X1, X)) | (~![P: $i] : (~a_path_from_to_in(P, X0, X1, X)))))))))) | (~((~((~path_connected(X!4)) | a_path_from_to_in(tptp_fun_P_1(X1!2, X0!3, X!4), X0!3, X1!2, X!4) | (~a_member_of(X0!3, X!4)) | (~a_member_of(X1!2, X!4)))) | (~(path_connected(X!4) | (~((~a_member_of(X0!3, X!4)) | (~a_member_of(X1!2, X!4)) | (~![P: $i] : (~a_path_from_to_in(P, X0!3, X1!2, X!4)))))))))),
% 0.17/0.36 inference(quant_inst,[status(thm)],[])).
% 0.17/0.36 tff(25,plain,
% 0.17/0.36 ((~![X: $i, X0: $i, X1: $i] : (~((~((~path_connected(X)) | a_path_from_to_in(tptp_fun_P_1(X1, X0, X), X0, X1, X) | (~a_member_of(X0, X)) | (~a_member_of(X1, X)))) | (~(path_connected(X) | (~((~a_member_of(X0, X)) | (~a_member_of(X1, X)) | (~![P: $i] : (~a_path_from_to_in(P, X0, X1, X)))))))))) | (~((~((~a_member_of(X0!3, X!4)) | (~path_connected(X!4)) | (~a_member_of(X1!2, X!4)) | a_path_from_to_in(tptp_fun_P_1(X1!2, X0!3, X!4), X0!3, X1!2, X!4))) | (~(path_connected(X!4) | (~((~a_member_of(X0!3, X!4)) | (~a_member_of(X1!2, X!4)) | (~![P: $i] : (~a_path_from_to_in(P, X0!3, X1!2, X!4)))))))))),
% 0.17/0.36 inference(modus_ponens,[status(thm)],[24, 23])).
% 0.17/0.36 tff(26,plain,
% 0.17/0.36 (~((~((~a_member_of(X0!3, X!4)) | (~path_connected(X!4)) | (~a_member_of(X1!2, X!4)) | a_path_from_to_in(tptp_fun_P_1(X1!2, X0!3, X!4), X0!3, X1!2, X!4))) | (~(path_connected(X!4) | (~((~a_member_of(X0!3, X!4)) | (~a_member_of(X1!2, X!4)) | (~![P: $i] : (~a_path_from_to_in(P, X0!3, X1!2, X!4))))))))),
% 0.17/0.36 inference(unit_resolution,[status(thm)],[25, 19])).
% 0.17/0.36 tff(27,plain,
% 0.17/0.36 (((~((~a_member_of(X0!3, X!4)) | (~path_connected(X!4)) | (~a_member_of(X1!2, X!4)) | a_path_from_to_in(tptp_fun_P_1(X1!2, X0!3, X!4), X0!3, X1!2, X!4))) | (~(path_connected(X!4) | (~((~a_member_of(X0!3, X!4)) | (~a_member_of(X1!2, X!4)) | (~![P: $i] : (~a_path_from_to_in(P, X0!3, X1!2, X!4)))))))) | ((~a_member_of(X0!3, X!4)) | (~path_connected(X!4)) | (~a_member_of(X1!2, X!4)) | a_path_from_to_in(tptp_fun_P_1(X1!2, X0!3, X!4), X0!3, X1!2, X!4))),
% 0.17/0.36 inference(tautology,[status(thm)],[])).
% 0.17/0.36 tff(28,plain,
% 0.17/0.36 ((~a_member_of(X0!3, X!4)) | (~path_connected(X!4)) | (~a_member_of(X1!2, X!4)) | a_path_from_to_in(tptp_fun_P_1(X1!2, X0!3, X!4), X0!3, X1!2, X!4)),
% 0.17/0.36 inference(unit_resolution,[status(thm)],[27, 26])).
% 0.17/0.36 tff(29,plain,
% 0.17/0.36 ((~![X: $i, X0: $i, X1: $i] : ((~(path_connected(X) & a_member_of(X0, X) & a_member_of(X1, X))) | isomorphic_groups(first_homotop_grp(X, X0), first_homotop_grp(X, X1)))) <=> (~![X: $i, X0: $i, X1: $i] : ((~(path_connected(X) & a_member_of(X0, X) & a_member_of(X1, X))) | isomorphic_groups(first_homotop_grp(X, X0), first_homotop_grp(X, X1))))),
% 0.17/0.36 inference(rewrite,[status(thm)],[])).
% 0.17/0.36 tff(30,plain,
% 0.17/0.36 ((~![X: $i, X0: $i, X1: $i] : (((path_connected(X) & a_member_of(X0, X)) & a_member_of(X1, X)) => isomorphic_groups(first_homotop_grp(X, X0), first_homotop_grp(X, X1)))) <=> (~![X: $i, X0: $i, X1: $i] : ((~(path_connected(X) & a_member_of(X0, X) & a_member_of(X1, X))) | isomorphic_groups(first_homotop_grp(X, X0), first_homotop_grp(X, X1))))),
% 0.17/0.36 inference(rewrite,[status(thm)],[])).
% 0.17/0.36 tff(31,axiom,(~![X: $i, X0: $i, X1: $i] : (((path_connected(X) & a_member_of(X0, X)) & a_member_of(X1, X)) => isomorphic_groups(first_homotop_grp(X, X0), first_homotop_grp(X, X1)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','m_8_2_2')).
% 0.17/0.36 tff(32,plain,
% 0.17/0.36 (~![X: $i, X0: $i, X1: $i] : ((~(path_connected(X) & a_member_of(X0, X) & a_member_of(X1, X))) | isomorphic_groups(first_homotop_grp(X, X0), first_homotop_grp(X, X1)))),
% 0.17/0.36 inference(modus_ponens,[status(thm)],[31, 30])).
% 0.17/0.36 tff(33,plain,
% 0.17/0.36 (~![X: $i, X0: $i, X1: $i] : ((~(path_connected(X) & a_member_of(X0, X) & a_member_of(X1, X))) | isomorphic_groups(first_homotop_grp(X, X0), first_homotop_grp(X, X1)))),
% 0.17/0.37 inference(modus_ponens,[status(thm)],[32, 29])).
% 0.17/0.37 tff(34,plain,
% 0.17/0.37 (~![X: $i, X0: $i, X1: $i] : ((~(path_connected(X) & a_member_of(X0, X) & a_member_of(X1, X))) | isomorphic_groups(first_homotop_grp(X, X0), first_homotop_grp(X, X1)))),
% 0.17/0.37 inference(modus_ponens,[status(thm)],[33, 29])).
% 0.17/0.37 tff(35,plain,
% 0.17/0.37 (~![X: $i, X0: $i, X1: $i] : ((~(path_connected(X) & a_member_of(X0, X) & a_member_of(X1, X))) | isomorphic_groups(first_homotop_grp(X, X0), first_homotop_grp(X, X1)))),
% 0.17/0.37 inference(modus_ponens,[status(thm)],[34, 29])).
% 0.17/0.37 tff(36,plain,(
% 0.17/0.37 ~((~(path_connected(X!4) & a_member_of(X0!3, X!4) & a_member_of(X1!2, X!4))) | isomorphic_groups(first_homotop_grp(X!4, X0!3), first_homotop_grp(X!4, X1!2)))),
% 0.17/0.37 inference(skolemize,[status(sab)],[35])).
% 0.17/0.37 tff(37,plain,
% 0.17/0.37 (path_connected(X!4) & a_member_of(X0!3, X!4) & a_member_of(X1!2, X!4)),
% 0.17/0.37 inference(or_elim,[status(thm)],[36])).
% 0.17/0.37 tff(38,plain,
% 0.17/0.37 (a_member_of(X1!2, X!4)),
% 0.17/0.37 inference(and_elim,[status(thm)],[37])).
% 0.17/0.37 tff(39,plain,
% 0.17/0.37 (a_member_of(X0!3, X!4)),
% 0.17/0.37 inference(and_elim,[status(thm)],[37])).
% 0.17/0.37 tff(40,plain,
% 0.17/0.37 (path_connected(X!4)),
% 0.17/0.37 inference(and_elim,[status(thm)],[37])).
% 0.17/0.37 tff(41,plain,
% 0.17/0.37 ((~((~a_member_of(X0!3, X!4)) | (~path_connected(X!4)) | (~a_member_of(X1!2, X!4)) | a_path_from_to_in(tptp_fun_P_1(X1!2, X0!3, X!4), X0!3, X1!2, X!4))) | (~a_member_of(X0!3, X!4)) | (~path_connected(X!4)) | (~a_member_of(X1!2, X!4)) | a_path_from_to_in(tptp_fun_P_1(X1!2, X0!3, X!4), X0!3, X1!2, X!4)),
% 0.17/0.37 inference(tautology,[status(thm)],[])).
% 0.17/0.37 tff(42,plain,
% 0.17/0.37 ((~((~a_member_of(X0!3, X!4)) | (~path_connected(X!4)) | (~a_member_of(X1!2, X!4)) | a_path_from_to_in(tptp_fun_P_1(X1!2, X0!3, X!4), X0!3, X1!2, X!4))) | a_path_from_to_in(tptp_fun_P_1(X1!2, X0!3, X!4), X0!3, X1!2, X!4)),
% 0.17/0.37 inference(unit_resolution,[status(thm)],[41, 40, 39, 38])).
% 0.17/0.37 tff(43,plain,
% 0.17/0.37 (a_path_from_to_in(tptp_fun_P_1(X1!2, X0!3, X!4), X0!3, X1!2, X!4)),
% 0.17/0.37 inference(unit_resolution,[status(thm)],[42, 28])).
% 0.17/0.37 tff(44,plain,
% 0.17/0.37 (^[A: $i, X0: $i, X1: $i, X: $i] : refl(((~a_path_from_to_in(A, X0, X1, X)) | a_group_isomorphism_from_to(alpha_hat(A), first_homotop_grp(X, X0), first_homotop_grp(X, X1))) <=> ((~a_path_from_to_in(A, X0, X1, X)) | a_group_isomorphism_from_to(alpha_hat(A), first_homotop_grp(X, X0), first_homotop_grp(X, X1))))),
% 0.17/0.37 inference(bind,[status(th)],[])).
% 0.17/0.37 tff(45,plain,
% 0.17/0.37 (![A: $i, X0: $i, X1: $i, X: $i] : ((~a_path_from_to_in(A, X0, X1, X)) | a_group_isomorphism_from_to(alpha_hat(A), first_homotop_grp(X, X0), first_homotop_grp(X, X1))) <=> ![A: $i, X0: $i, X1: $i, X: $i] : ((~a_path_from_to_in(A, X0, X1, X)) | a_group_isomorphism_from_to(alpha_hat(A), first_homotop_grp(X, X0), first_homotop_grp(X, X1)))),
% 0.17/0.37 inference(quant_intro,[status(thm)],[44])).
% 0.17/0.37 tff(46,plain,
% 0.17/0.37 (![A: $i, X0: $i, X1: $i, X: $i] : ((~a_path_from_to_in(A, X0, X1, X)) | a_group_isomorphism_from_to(alpha_hat(A), first_homotop_grp(X, X0), first_homotop_grp(X, X1))) <=> ![A: $i, X0: $i, X1: $i, X: $i] : ((~a_path_from_to_in(A, X0, X1, X)) | a_group_isomorphism_from_to(alpha_hat(A), first_homotop_grp(X, X0), first_homotop_grp(X, X1)))),
% 0.17/0.37 inference(rewrite,[status(thm)],[])).
% 0.17/0.37 tff(47,plain,
% 0.17/0.37 (^[A: $i, X0: $i, X1: $i, X: $i] : rewrite((a_path_from_to_in(A, X0, X1, X) => a_group_isomorphism_from_to(alpha_hat(A), first_homotop_grp(X, X0), first_homotop_grp(X, X1))) <=> ((~a_path_from_to_in(A, X0, X1, X)) | a_group_isomorphism_from_to(alpha_hat(A), first_homotop_grp(X, X0), first_homotop_grp(X, X1))))),
% 0.17/0.37 inference(bind,[status(th)],[])).
% 0.17/0.37 tff(48,plain,
% 0.17/0.37 (![A: $i, X0: $i, X1: $i, X: $i] : (a_path_from_to_in(A, X0, X1, X) => a_group_isomorphism_from_to(alpha_hat(A), first_homotop_grp(X, X0), first_homotop_grp(X, X1))) <=> ![A: $i, X0: $i, X1: $i, X: $i] : ((~a_path_from_to_in(A, X0, X1, X)) | a_group_isomorphism_from_to(alpha_hat(A), first_homotop_grp(X, X0), first_homotop_grp(X, X1)))),
% 0.17/0.37 inference(quant_intro,[status(thm)],[47])).
% 0.17/0.37 tff(49,axiom,(![A: $i, X0: $i, X1: $i, X: $i] : (a_path_from_to_in(A, X0, X1, X) => a_group_isomorphism_from_to(alpha_hat(A), first_homotop_grp(X, X0), first_homotop_grp(X, X1)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','m_8_2_1')).
% 0.17/0.37 tff(50,plain,
% 0.17/0.37 (![A: $i, X0: $i, X1: $i, X: $i] : ((~a_path_from_to_in(A, X0, X1, X)) | a_group_isomorphism_from_to(alpha_hat(A), first_homotop_grp(X, X0), first_homotop_grp(X, X1)))),
% 0.17/0.37 inference(modus_ponens,[status(thm)],[49, 48])).
% 0.17/0.37 tff(51,plain,
% 0.17/0.37 (![A: $i, X0: $i, X1: $i, X: $i] : ((~a_path_from_to_in(A, X0, X1, X)) | a_group_isomorphism_from_to(alpha_hat(A), first_homotop_grp(X, X0), first_homotop_grp(X, X1)))),
% 0.17/0.37 inference(modus_ponens,[status(thm)],[50, 46])).
% 0.17/0.37 tff(52,plain,(
% 0.17/0.37 ![A: $i, X0: $i, X1: $i, X: $i] : ((~a_path_from_to_in(A, X0, X1, X)) | a_group_isomorphism_from_to(alpha_hat(A), first_homotop_grp(X, X0), first_homotop_grp(X, X1)))),
% 0.17/0.37 inference(skolemize,[status(sab)],[51])).
% 0.17/0.37 tff(53,plain,
% 0.17/0.37 (![A: $i, X0: $i, X1: $i, X: $i] : ((~a_path_from_to_in(A, X0, X1, X)) | a_group_isomorphism_from_to(alpha_hat(A), first_homotop_grp(X, X0), first_homotop_grp(X, X1)))),
% 0.17/0.37 inference(modus_ponens,[status(thm)],[52, 45])).
% 0.17/0.37 tff(54,plain,
% 0.17/0.37 (((~![A: $i, X0: $i, X1: $i, X: $i] : ((~a_path_from_to_in(A, X0, X1, X)) | a_group_isomorphism_from_to(alpha_hat(A), first_homotop_grp(X, X0), first_homotop_grp(X, X1)))) | ((~a_path_from_to_in(tptp_fun_P_1(X1!2, X0!3, X!4), X0!3, X1!2, X!4)) | a_group_isomorphism_from_to(alpha_hat(tptp_fun_P_1(X1!2, X0!3, X!4)), first_homotop_grp(X!4, X0!3), first_homotop_grp(X!4, X1!2)))) <=> ((~![A: $i, X0: $i, X1: $i, X: $i] : ((~a_path_from_to_in(A, X0, X1, X)) | a_group_isomorphism_from_to(alpha_hat(A), first_homotop_grp(X, X0), first_homotop_grp(X, X1)))) | (~a_path_from_to_in(tptp_fun_P_1(X1!2, X0!3, X!4), X0!3, X1!2, X!4)) | a_group_isomorphism_from_to(alpha_hat(tptp_fun_P_1(X1!2, X0!3, X!4)), first_homotop_grp(X!4, X0!3), first_homotop_grp(X!4, X1!2)))),
% 0.17/0.37 inference(rewrite,[status(thm)],[])).
% 0.17/0.37 tff(55,plain,
% 0.17/0.37 ((~![A: $i, X0: $i, X1: $i, X: $i] : ((~a_path_from_to_in(A, X0, X1, X)) | a_group_isomorphism_from_to(alpha_hat(A), first_homotop_grp(X, X0), first_homotop_grp(X, X1)))) | ((~a_path_from_to_in(tptp_fun_P_1(X1!2, X0!3, X!4), X0!3, X1!2, X!4)) | a_group_isomorphism_from_to(alpha_hat(tptp_fun_P_1(X1!2, X0!3, X!4)), first_homotop_grp(X!4, X0!3), first_homotop_grp(X!4, X1!2)))),
% 0.17/0.37 inference(quant_inst,[status(thm)],[])).
% 0.17/0.37 tff(56,plain,
% 0.17/0.37 ((~![A: $i, X0: $i, X1: $i, X: $i] : ((~a_path_from_to_in(A, X0, X1, X)) | a_group_isomorphism_from_to(alpha_hat(A), first_homotop_grp(X, X0), first_homotop_grp(X, X1)))) | (~a_path_from_to_in(tptp_fun_P_1(X1!2, X0!3, X!4), X0!3, X1!2, X!4)) | a_group_isomorphism_from_to(alpha_hat(tptp_fun_P_1(X1!2, X0!3, X!4)), first_homotop_grp(X!4, X0!3), first_homotop_grp(X!4, X1!2))),
% 0.17/0.37 inference(modus_ponens,[status(thm)],[55, 54])).
% 0.17/0.37 tff(57,plain,
% 0.17/0.37 (a_group_isomorphism_from_to(alpha_hat(tptp_fun_P_1(X1!2, X0!3, X!4)), first_homotop_grp(X!4, X0!3), first_homotop_grp(X!4, X1!2))),
% 0.17/0.37 inference(unit_resolution,[status(thm)],[56, 53, 43])).
% 0.17/0.37 tff(58,plain,
% 0.17/0.37 (^[A: $i, B: $i] : refl((~((~((~isomorphic_groups(A, B)) | a_group_isomorphism_from_to(tptp_fun_F_0(B, A), A, B))) | (~(isomorphic_groups(A, B) | ![F: $i] : (~a_group_isomorphism_from_to(F, A, B)))))) <=> (~((~((~isomorphic_groups(A, B)) | a_group_isomorphism_from_to(tptp_fun_F_0(B, A), A, B))) | (~(isomorphic_groups(A, B) | ![F: $i] : (~a_group_isomorphism_from_to(F, A, B)))))))),
% 0.17/0.37 inference(bind,[status(th)],[])).
% 0.17/0.37 tff(59,plain,
% 0.17/0.37 (![A: $i, B: $i] : (~((~((~isomorphic_groups(A, B)) | a_group_isomorphism_from_to(tptp_fun_F_0(B, A), A, B))) | (~(isomorphic_groups(A, B) | ![F: $i] : (~a_group_isomorphism_from_to(F, A, B)))))) <=> ![A: $i, B: $i] : (~((~((~isomorphic_groups(A, B)) | a_group_isomorphism_from_to(tptp_fun_F_0(B, A), A, B))) | (~(isomorphic_groups(A, B) | ![F: $i] : (~a_group_isomorphism_from_to(F, A, B))))))),
% 0.17/0.37 inference(quant_intro,[status(thm)],[58])).
% 0.17/0.37 tff(60,plain,
% 0.17/0.37 (^[A: $i, B: $i] : rewrite((~((~((~isomorphic_groups(A, B)) | a_group_isomorphism_from_to(tptp_fun_F_0(B, A), A, B))) | (~(isomorphic_groups(A, B) | ![F: $i] : (~a_group_isomorphism_from_to(F, A, B)))))) <=> (~((~((~isomorphic_groups(A, B)) | a_group_isomorphism_from_to(tptp_fun_F_0(B, A), A, B))) | (~(isomorphic_groups(A, B) | ![F: $i] : (~a_group_isomorphism_from_to(F, A, B)))))))),
% 0.17/0.37 inference(bind,[status(th)],[])).
% 0.17/0.37 tff(61,plain,
% 0.17/0.37 (![A: $i, B: $i] : (~((~((~isomorphic_groups(A, B)) | a_group_isomorphism_from_to(tptp_fun_F_0(B, A), A, B))) | (~(isomorphic_groups(A, B) | ![F: $i] : (~a_group_isomorphism_from_to(F, A, B)))))) <=> ![A: $i, B: $i] : (~((~((~isomorphic_groups(A, B)) | a_group_isomorphism_from_to(tptp_fun_F_0(B, A), A, B))) | (~(isomorphic_groups(A, B) | ![F: $i] : (~a_group_isomorphism_from_to(F, A, B))))))),
% 0.17/0.37 inference(quant_intro,[status(thm)],[60])).
% 0.17/0.37 tff(62,plain,
% 0.17/0.37 (![A: $i, B: $i] : (~((~((~isomorphic_groups(A, B)) | a_group_isomorphism_from_to(tptp_fun_F_0(B, A), A, B))) | (~(isomorphic_groups(A, B) | ![F: $i] : (~a_group_isomorphism_from_to(F, A, B)))))) <=> ![A: $i, B: $i] : (~((~((~isomorphic_groups(A, B)) | a_group_isomorphism_from_to(tptp_fun_F_0(B, A), A, B))) | (~(isomorphic_groups(A, B) | ![F: $i] : (~a_group_isomorphism_from_to(F, A, B))))))),
% 0.17/0.37 inference(transitivity,[status(thm)],[61, 59])).
% 0.17/0.37 tff(63,plain,
% 0.17/0.37 (^[A: $i, B: $i] : trans(monotonicity(rewrite((isomorphic_groups(A, B) | ![F: $i] : (~a_group_isomorphism_from_to(F, A, B))) <=> (isomorphic_groups(A, B) | ![F: $i] : (~a_group_isomorphism_from_to(F, A, B)))), ((((~isomorphic_groups(A, B)) | a_group_isomorphism_from_to(tptp_fun_F_0(B, A), A, B)) & (isomorphic_groups(A, B) | ![F: $i] : (~a_group_isomorphism_from_to(F, A, B)))) <=> (((~isomorphic_groups(A, B)) | a_group_isomorphism_from_to(tptp_fun_F_0(B, A), A, B)) & (isomorphic_groups(A, B) | ![F: $i] : (~a_group_isomorphism_from_to(F, A, B)))))), rewrite((((~isomorphic_groups(A, B)) | a_group_isomorphism_from_to(tptp_fun_F_0(B, A), A, B)) & (isomorphic_groups(A, B) | ![F: $i] : (~a_group_isomorphism_from_to(F, A, B)))) <=> (~((~((~isomorphic_groups(A, B)) | a_group_isomorphism_from_to(tptp_fun_F_0(B, A), A, B))) | (~(isomorphic_groups(A, B) | ![F: $i] : (~a_group_isomorphism_from_to(F, A, B))))))), ((((~isomorphic_groups(A, B)) | a_group_isomorphism_from_to(tptp_fun_F_0(B, A), A, B)) & (isomorphic_groups(A, B) | ![F: $i] : (~a_group_isomorphism_from_to(F, A, B)))) <=> (~((~((~isomorphic_groups(A, B)) | a_group_isomorphism_from_to(tptp_fun_F_0(B, A), A, B))) | (~(isomorphic_groups(A, B) | ![F: $i] : (~a_group_isomorphism_from_to(F, A, B))))))))),
% 0.17/0.37 inference(bind,[status(th)],[])).
% 0.17/0.37 tff(64,plain,
% 0.17/0.37 (![A: $i, B: $i] : (((~isomorphic_groups(A, B)) | a_group_isomorphism_from_to(tptp_fun_F_0(B, A), A, B)) & (isomorphic_groups(A, B) | ![F: $i] : (~a_group_isomorphism_from_to(F, A, B)))) <=> ![A: $i, B: $i] : (~((~((~isomorphic_groups(A, B)) | a_group_isomorphism_from_to(tptp_fun_F_0(B, A), A, B))) | (~(isomorphic_groups(A, B) | ![F: $i] : (~a_group_isomorphism_from_to(F, A, B))))))),
% 0.17/0.37 inference(quant_intro,[status(thm)],[63])).
% 0.17/0.37 tff(65,plain,
% 0.17/0.37 (![A: $i, B: $i] : (isomorphic_groups(A, B) <=> ?[F: $i] : a_group_isomorphism_from_to(F, A, B)) <=> ![A: $i, B: $i] : (isomorphic_groups(A, B) <=> ?[F: $i] : a_group_isomorphism_from_to(F, A, B))),
% 0.17/0.37 inference(rewrite,[status(thm)],[])).
% 0.17/0.37 tff(66,axiom,(![A: $i, B: $i] : (isomorphic_groups(A, B) <=> ?[F: $i] : a_group_isomorphism_from_to(F, A, B))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','isomorphic_groups_defn')).
% 0.17/0.37 tff(67,plain,
% 0.17/0.37 (![A: $i, B: $i] : (isomorphic_groups(A, B) <=> ?[F: $i] : a_group_isomorphism_from_to(F, A, B))),
% 0.17/0.37 inference(modus_ponens,[status(thm)],[66, 65])).
% 0.17/0.37 tff(68,plain,(
% 0.17/0.37 ![A: $i, B: $i] : (((~isomorphic_groups(A, B)) | a_group_isomorphism_from_to(tptp_fun_F_0(B, A), A, B)) & (isomorphic_groups(A, B) | ![F: $i] : (~a_group_isomorphism_from_to(F, A, B))))),
% 0.17/0.37 inference(skolemize,[status(sab)],[67])).
% 0.17/0.37 tff(69,plain,
% 0.17/0.37 (![A: $i, B: $i] : (~((~((~isomorphic_groups(A, B)) | a_group_isomorphism_from_to(tptp_fun_F_0(B, A), A, B))) | (~(isomorphic_groups(A, B) | ![F: $i] : (~a_group_isomorphism_from_to(F, A, B))))))),
% 0.17/0.37 inference(modus_ponens,[status(thm)],[68, 64])).
% 0.17/0.37 tff(70,plain,
% 0.17/0.37 (![A: $i, B: $i] : (~((~((~isomorphic_groups(A, B)) | a_group_isomorphism_from_to(tptp_fun_F_0(B, A), A, B))) | (~(isomorphic_groups(A, B) | ![F: $i] : (~a_group_isomorphism_from_to(F, A, B))))))),
% 0.17/0.37 inference(modus_ponens,[status(thm)],[69, 62])).
% 0.17/0.37 tff(71,plain,
% 0.17/0.37 ((~![A: $i, B: $i] : (~((~((~isomorphic_groups(A, B)) | a_group_isomorphism_from_to(tptp_fun_F_0(B, A), A, B))) | (~(isomorphic_groups(A, B) | ![F: $i] : (~a_group_isomorphism_from_to(F, A, B))))))) | (~((~((~isomorphic_groups(first_homotop_grp(X!4, X0!3), first_homotop_grp(X!4, X1!2))) | a_group_isomorphism_from_to(tptp_fun_F_0(first_homotop_grp(X!4, X1!2), first_homotop_grp(X!4, X0!3)), first_homotop_grp(X!4, X0!3), first_homotop_grp(X!4, X1!2)))) | (~(isomorphic_groups(first_homotop_grp(X!4, X0!3), first_homotop_grp(X!4, X1!2)) | ![F: $i] : (~a_group_isomorphism_from_to(F, first_homotop_grp(X!4, X0!3), first_homotop_grp(X!4, X1!2)))))))),
% 0.17/0.37 inference(quant_inst,[status(thm)],[])).
% 0.17/0.37 tff(72,plain,
% 0.17/0.37 (~((~((~isomorphic_groups(first_homotop_grp(X!4, X0!3), first_homotop_grp(X!4, X1!2))) | a_group_isomorphism_from_to(tptp_fun_F_0(first_homotop_grp(X!4, X1!2), first_homotop_grp(X!4, X0!3)), first_homotop_grp(X!4, X0!3), first_homotop_grp(X!4, X1!2)))) | (~(isomorphic_groups(first_homotop_grp(X!4, X0!3), first_homotop_grp(X!4, X1!2)) | ![F: $i] : (~a_group_isomorphism_from_to(F, first_homotop_grp(X!4, X0!3), first_homotop_grp(X!4, X1!2))))))),
% 0.17/0.37 inference(unit_resolution,[status(thm)],[71, 70])).
% 0.17/0.37 tff(73,plain,
% 0.17/0.37 (((~((~isomorphic_groups(first_homotop_grp(X!4, X0!3), first_homotop_grp(X!4, X1!2))) | a_group_isomorphism_from_to(tptp_fun_F_0(first_homotop_grp(X!4, X1!2), first_homotop_grp(X!4, X0!3)), first_homotop_grp(X!4, X0!3), first_homotop_grp(X!4, X1!2)))) | (~(isomorphic_groups(first_homotop_grp(X!4, X0!3), first_homotop_grp(X!4, X1!2)) | ![F: $i] : (~a_group_isomorphism_from_to(F, first_homotop_grp(X!4, X0!3), first_homotop_grp(X!4, X1!2)))))) | (isomorphic_groups(first_homotop_grp(X!4, X0!3), first_homotop_grp(X!4, X1!2)) | ![F: $i] : (~a_group_isomorphism_from_to(F, first_homotop_grp(X!4, X0!3), first_homotop_grp(X!4, X1!2))))),
% 0.17/0.37 inference(tautology,[status(thm)],[])).
% 0.17/0.37 tff(74,plain,
% 0.17/0.37 (isomorphic_groups(first_homotop_grp(X!4, X0!3), first_homotop_grp(X!4, X1!2)) | ![F: $i] : (~a_group_isomorphism_from_to(F, first_homotop_grp(X!4, X0!3), first_homotop_grp(X!4, X1!2)))),
% 0.17/0.37 inference(unit_resolution,[status(thm)],[73, 72])).
% 0.17/0.37 tff(75,plain,
% 0.17/0.37 (~isomorphic_groups(first_homotop_grp(X!4, X0!3), first_homotop_grp(X!4, X1!2))),
% 0.17/0.37 inference(or_elim,[status(thm)],[36])).
% 0.17/0.37 tff(76,plain,
% 0.17/0.37 ((~(isomorphic_groups(first_homotop_grp(X!4, X0!3), first_homotop_grp(X!4, X1!2)) | ![F: $i] : (~a_group_isomorphism_from_to(F, first_homotop_grp(X!4, X0!3), first_homotop_grp(X!4, X1!2))))) | isomorphic_groups(first_homotop_grp(X!4, X0!3), first_homotop_grp(X!4, X1!2)) | ![F: $i] : (~a_group_isomorphism_from_to(F, first_homotop_grp(X!4, X0!3), first_homotop_grp(X!4, X1!2)))),
% 0.17/0.37 inference(tautology,[status(thm)],[])).
% 0.17/0.37 tff(77,plain,
% 0.17/0.37 ((~(isomorphic_groups(first_homotop_grp(X!4, X0!3), first_homotop_grp(X!4, X1!2)) | ![F: $i] : (~a_group_isomorphism_from_to(F, first_homotop_grp(X!4, X0!3), first_homotop_grp(X!4, X1!2))))) | ![F: $i] : (~a_group_isomorphism_from_to(F, first_homotop_grp(X!4, X0!3), first_homotop_grp(X!4, X1!2)))),
% 0.17/0.37 inference(unit_resolution,[status(thm)],[76, 75])).
% 0.17/0.37 tff(78,plain,
% 0.17/0.37 (![F: $i] : (~a_group_isomorphism_from_to(F, first_homotop_grp(X!4, X0!3), first_homotop_grp(X!4, X1!2)))),
% 0.17/0.37 inference(unit_resolution,[status(thm)],[77, 74])).
% 0.17/0.37 tff(79,plain,
% 0.17/0.37 ((~![F: $i] : (~a_group_isomorphism_from_to(F, first_homotop_grp(X!4, X0!3), first_homotop_grp(X!4, X1!2)))) | (~a_group_isomorphism_from_to(alpha_hat(tptp_fun_P_1(X1!2, X0!3, X!4)), first_homotop_grp(X!4, X0!3), first_homotop_grp(X!4, X1!2)))),
% 0.17/0.37 inference(quant_inst,[status(thm)],[])).
% 0.17/0.37 tff(80,plain,
% 0.17/0.37 ($false),
% 0.17/0.37 inference(unit_resolution,[status(thm)],[79, 78, 57])).
% 0.17/0.37 % SZS output end Proof
% 0.17/0.38 % E exiting
%------------------------------------------------------------------------------