%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : TOP022+1 : TPTP v8.1.2. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n008.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 : Thu May 9 17:51:34 EDT 2024
% Result : Theorem 0.20s 0.53s
% Output : Refutation 0.20s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.13 % Problem : TOP022+1 : TPTP v8.1.2. Released v3.1.0.
% 0.11/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.34 % Computer : n008.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Wed May 8 20:48:23 EDT 2024
% 0.13/0.35 % CPUTime :
% 0.20/0.53 % Version: 1.5
% 0.20/0.53 % SZS status Theorem
% 0.20/0.53 % SZS output start CNFRefutation
% 0.20/0.53 fof(m_8_2_2,conjecture,(![X]:(![X0]:(![X1]:(((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/sandbox2/benchmark/theBenchmark.p', m_8_2_2)).
% 0.20/0.53 fof(c0,negated_conjecture,(~(![X]:(![X0]:(![X1]:(((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))))))),inference(assume_negation,[status(cth)],[m_8_2_2])).
% 0.20/0.53 fof(c1,negated_conjecture,(?[X]:(?[X0]:(?[X1]:(((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)))))),inference(fof_nnf,[status(thm)],[c0])).
% 0.20/0.53 fof(c2,negated_conjecture,(?[X2]:(?[X3]:(?[X4]:(((path_connected(X2)&a_member_of(X3,X2))&a_member_of(X4,X2))&~isomorphic_groups(first_homotop_grp(X2,X3),first_homotop_grp(X2,X4)))))),inference(variable_rename,[status(thm)],[c1])).
% 0.20/0.53 fof(c3,negated_conjecture,(((path_connected(skolem0001)&a_member_of(skolem0002,skolem0001))&a_member_of(skolem0003,skolem0001))&~isomorphic_groups(first_homotop_grp(skolem0001,skolem0002),first_homotop_grp(skolem0001,skolem0003))),inference(skolemize,[status(esa)],[c2])).
% 0.20/0.53 cnf(c7,negated_conjecture,~isomorphic_groups(first_homotop_grp(skolem0001,skolem0002),first_homotop_grp(skolem0001,skolem0003)),inference(split_conjunct,[status(thm)],[c3])).
% 0.20/0.53 fof(isomorphic_groups_defn,axiom,(![A]:(![B]:(isomorphic_groups(A,B)<=>(?[F]:a_group_isomorphism_from_to(F,A,B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', isomorphic_groups_defn)).
% 0.20/0.53 fof(c21,plain,(![A]:(![B]:((~isomorphic_groups(A,B)|(?[F]:a_group_isomorphism_from_to(F,A,B)))&((![F]:~a_group_isomorphism_from_to(F,A,B))|isomorphic_groups(A,B))))),inference(fof_nnf,[status(thm)],[isomorphic_groups_defn])).
% 0.20/0.53 fof(c22,plain,((![A]:(![B]:(~isomorphic_groups(A,B)|(?[F]:a_group_isomorphism_from_to(F,A,B)))))&(![A]:(![B]:((![F]:~a_group_isomorphism_from_to(F,A,B))|isomorphic_groups(A,B))))),inference(shift_quantors,[status(thm)],[c21])).
% 0.20/0.53 fof(c23,plain,((![X19]:(![X20]:(~isomorphic_groups(X19,X20)|(?[X21]:a_group_isomorphism_from_to(X21,X19,X20)))))&(![X22]:(![X23]:((![X24]:~a_group_isomorphism_from_to(X24,X22,X23))|isomorphic_groups(X22,X23))))),inference(variable_rename,[status(thm)],[c22])).
% 0.20/0.53 fof(c25,plain,(![X19]:(![X20]:(![X22]:(![X23]:(![X24]:((~isomorphic_groups(X19,X20)|a_group_isomorphism_from_to(skolem0005(X19,X20),X19,X20))&(~a_group_isomorphism_from_to(X24,X22,X23)|isomorphic_groups(X22,X23)))))))),inference(shift_quantors,[status(thm)],[fof(c24,plain,((![X19]:(![X20]:(~isomorphic_groups(X19,X20)|a_group_isomorphism_from_to(skolem0005(X19,X20),X19,X20))))&(![X22]:(![X23]:((![X24]:~a_group_isomorphism_from_to(X24,X22,X23))|isomorphic_groups(X22,X23))))),inference(skolemize,[status(esa)],[c23])).])).
% 0.20/0.53 cnf(c27,plain,~a_group_isomorphism_from_to(X35,X34,X33)|isomorphic_groups(X34,X33),inference(split_conjunct,[status(thm)],[c25])).
% 0.20/0.53 fof(m_8_2_1,axiom,(![A]:(![X0]:(![X1]:(![X]:(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/sandbox2/benchmark/theBenchmark.p', m_8_2_1)).
% 0.20/0.53 fof(c8,plain,(![A]:(![X0]:(![X1]:(![X]:(~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))))))),inference(fof_nnf,[status(thm)],[m_8_2_1])).
% 0.20/0.53 fof(c9,plain,(![X5]:(![X6]:(![X7]:(![X8]:(~a_path_from_to_in(X5,X6,X7,X8)|a_group_isomorphism_from_to(alpha_hat(X5),first_homotop_grp(X8,X6),first_homotop_grp(X8,X7))))))),inference(variable_rename,[status(thm)],[c8])).
% 0.20/0.53 cnf(c10,plain,~a_path_from_to_in(X40,X38,X41,X39)|a_group_isomorphism_from_to(alpha_hat(X40),first_homotop_grp(X39,X38),first_homotop_grp(X39,X41)),inference(split_conjunct,[status(thm)],[c9])).
% 0.20/0.53 cnf(c4,negated_conjecture,path_connected(skolem0001),inference(split_conjunct,[status(thm)],[c3])).
% 0.20/0.53 cnf(c5,negated_conjecture,a_member_of(skolem0002,skolem0001),inference(split_conjunct,[status(thm)],[c3])).
% 0.20/0.53 cnf(c6,negated_conjecture,a_member_of(skolem0003,skolem0001),inference(split_conjunct,[status(thm)],[c3])).
% 0.20/0.53 fof(path_connected_defn,axiom,(![X]:(![X0]:(![X1]:(path_connected(X)<=>((a_member_of(X0,X)&a_member_of(X1,X))=>(?[P]:a_path_from_to_in(P,X0,X1,X))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', path_connected_defn)).
% 0.20/0.53 fof(c11,plain,(![X]:(![X0]:(![X1]:((~path_connected(X)|((~a_member_of(X0,X)|~a_member_of(X1,X))|(?[P]:a_path_from_to_in(P,X0,X1,X))))&(((a_member_of(X0,X)&a_member_of(X1,X))&(![P]:~a_path_from_to_in(P,X0,X1,X)))|path_connected(X)))))),inference(fof_nnf,[status(thm)],[path_connected_defn])).
% 0.20/0.53 fof(c12,plain,((![X]:(~path_connected(X)|(![X0]:(![X1]:((~a_member_of(X0,X)|~a_member_of(X1,X))|(?[P]:a_path_from_to_in(P,X0,X1,X)))))))&(![X]:((((![X0]:a_member_of(X0,X))&(![X1]:a_member_of(X1,X)))&(![X0]:(![X1]:(![P]:~a_path_from_to_in(P,X0,X1,X)))))|path_connected(X)))),inference(shift_quantors,[status(thm)],[c11])).
% 0.20/0.53 fof(c13,plain,((![X9]:(~path_connected(X9)|(![X10]:(![X11]:((~a_member_of(X10,X9)|~a_member_of(X11,X9))|(?[X12]:a_path_from_to_in(X12,X10,X11,X9)))))))&(![X13]:((((![X14]:a_member_of(X14,X13))&(![X15]:a_member_of(X15,X13)))&(![X16]:(![X17]:(![X18]:~a_path_from_to_in(X18,X16,X17,X13)))))|path_connected(X13)))),inference(variable_rename,[status(thm)],[c12])).
% 0.20/0.53 fof(c15,plain,(![X9]:(![X10]:(![X11]:(![X13]:(![X14]:(![X15]:(![X16]:(![X17]:(![X18]:((~path_connected(X9)|((~a_member_of(X10,X9)|~a_member_of(X11,X9))|a_path_from_to_in(skolem0004(X9,X10,X11),X10,X11,X9)))&(((a_member_of(X14,X13)&a_member_of(X15,X13))&~a_path_from_to_in(X18,X16,X17,X13))|path_connected(X13)))))))))))),inference(shift_quantors,[status(thm)],[fof(c14,plain,((![X9]:(~path_connected(X9)|(![X10]:(![X11]:((~a_member_of(X10,X9)|~a_member_of(X11,X9))|a_path_from_to_in(skolem0004(X9,X10,X11),X10,X11,X9))))))&(![X13]:((((![X14]:a_member_of(X14,X13))&(![X15]:a_member_of(X15,X13)))&(![X16]:(![X17]:(![X18]:~a_path_from_to_in(X18,X16,X17,X13)))))|path_connected(X13)))),inference(skolemize,[status(esa)],[c13])).])).
% 0.20/0.53 fof(c16,plain,(![X9]:(![X10]:(![X11]:(![X13]:(![X14]:(![X15]:(![X16]:(![X17]:(![X18]:((~path_connected(X9)|((~a_member_of(X10,X9)|~a_member_of(X11,X9))|a_path_from_to_in(skolem0004(X9,X10,X11),X10,X11,X9)))&(((a_member_of(X14,X13)|path_connected(X13))&(a_member_of(X15,X13)|path_connected(X13)))&(~a_path_from_to_in(X18,X16,X17,X13)|path_connected(X13))))))))))))),inference(distribute,[status(thm)],[c15])).
% 0.20/0.53 cnf(c17,plain,~path_connected(X44)|~a_member_of(X42,X44)|~a_member_of(X43,X44)|a_path_from_to_in(skolem0004(X44,X42,X43),X42,X43,X44),inference(split_conjunct,[status(thm)],[c16])).
% 0.20/0.53 cnf(c30,plain,~path_connected(skolem0001)|~a_member_of(X53,skolem0001)|a_path_from_to_in(skolem0004(skolem0001,X53,skolem0003),X53,skolem0003,skolem0001),inference(resolution,[status(thm)],[c17, c6])).
% 0.20/0.53 cnf(c48,plain,~path_connected(skolem0001)|a_path_from_to_in(skolem0004(skolem0001,skolem0002,skolem0003),skolem0002,skolem0003,skolem0001),inference(resolution,[status(thm)],[c30, c5])).
% 0.20/0.53 cnf(c53,plain,a_path_from_to_in(skolem0004(skolem0001,skolem0002,skolem0003),skolem0002,skolem0003,skolem0001),inference(resolution,[status(thm)],[c48, c4])).
% 0.20/0.53 cnf(c55,plain,a_group_isomorphism_from_to(alpha_hat(skolem0004(skolem0001,skolem0002,skolem0003)),first_homotop_grp(skolem0001,skolem0002),first_homotop_grp(skolem0001,skolem0003)),inference(resolution,[status(thm)],[c53, c10])).
% 0.20/0.53 cnf(c62,plain,isomorphic_groups(first_homotop_grp(skolem0001,skolem0002),first_homotop_grp(skolem0001,skolem0003)),inference(resolution,[status(thm)],[c55, c27])).
% 0.20/0.53 cnf(c64,plain,$false,inference(resolution,[status(thm)],[c62, c7])).
% 0.20/0.53 % SZS output end CNFRefutation
% 0.20/0.53
% 0.20/0.53 % Initial clauses : 11
% 0.20/0.53 % Processed clauses : 29
% 0.20/0.53 % Factors computed : 1
% 0.20/0.53 % Resolvents computed: 37
% 0.20/0.53 % Tautologies deleted: 4
% 0.20/0.53 % Forward subsumed : 11
% 0.20/0.53 % Backward subsumed : 4
% 0.20/0.53 % -------- CPU Time ---------
% 0.20/0.53 % User time : 0.173 s
% 0.20/0.53 % System time : 0.013 s
% 0.20/0.53 % Total time : 0.186 s
%------------------------------------------------------------------------------