%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : TOP022+1 : TPTP v9.3.1. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n004.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 03:53:41 PM UTC 2026
% Result : Theorem 0.16s 5.41s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : TOP022+1 : TPTP v9.3.1. Released v3.1.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.12/5.38 % Computer : n004.cluster.edu
% 0.12/5.38 % Model : x86_64 x86_64
% 0.12/5.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/5.38 % Memory : 8046.5625MB
% 0.12/5.38 % OS : Linux 6.8.0-71-generic
% 0.12/5.38 % CPULimit : 300
% 0.12/5.38 % WCLimit : 300
% 0.12/5.38 % DateTime : Mon Sep 21 12:38:24 UTC 2026
% 0.12/5.38 % CPUTime :
% 0.12/5.39 % Drodi V4.1.1
% 0.16/5.41 % Refutation found
% 0.16/5.41 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.16/5.41 % SZS output start CNFRefutation for theBenchmark
% 0.16/5.41 fof(f1,axiom,(
% 0.16/5.41 (! [A,B] :( isomorphic_groups(A,B)<=> (? [F] : a_group_isomorphism_from_to(F,A,B) )) )),
% 0.16/5.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.16/5.41 fof(f2,axiom,(
% 0.16/5.41 (! [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) )) ) )),
% 0.16/5.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.16/5.41 fof(f3,axiom,(
% 0.16/5.41 (! [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)) ) )),
% 0.16/5.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.16/5.41 fof(f4,conjecture,(
% 0.16/5.41 (! [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)) ) )),
% 0.16/5.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.16/5.41 fof(f5,negated_conjecture,(
% 0.16/5.41 ~((! [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)) ) ))),
% 0.16/5.41 inference(negated_conjecture,[status(cth)],[f4])).
% 0.16/5.41 fof(f6,plain,(
% 0.16/5.41 ![A,B]: ((~isomorphic_groups(A,B)|(?[F]: a_group_isomorphism_from_to(F,A,B)))&(isomorphic_groups(A,B)|(![F]: ~a_group_isomorphism_from_to(F,A,B))))),
% 0.16/5.41 inference(NNF_transformation,[status(thm)],[f1])).
% 0.16/5.41 fof(f7,plain,(
% 0.16/5.41 (![A,B]: (~isomorphic_groups(A,B)|(?[F]: a_group_isomorphism_from_to(F,A,B))))&(![A,B]: (isomorphic_groups(A,B)|(![F]: ~a_group_isomorphism_from_to(F,A,B))))),
% 0.16/5.41 inference(miniscoping,[status(thm)],[f6])).
% 0.16/5.41 fof(f8,plain,(
% 0.16/5.41 (![A,B]: (~isomorphic_groups(A,B)|a_group_isomorphism_from_to(sK0_skl(B,A),A,B)))&(![A,B]: (isomorphic_groups(A,B)|(![F]: ~a_group_isomorphism_from_to(F,A,B))))),
% 0.16/5.41 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(F,sK0_skl(B,A))],[f7])).
% 0.16/5.41 fof(f10,plain,(
% 0.16/5.41 ![X0,X1,X2]: (isomorphic_groups(X0,X1)|~a_group_isomorphism_from_to(X2,X0,X1))),
% 0.16/5.41 inference(cnf_transformation,[status(thm)],[f8])).
% 0.16/5.41 fof(f11,plain,(
% 0.16/5.41 ![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))))),
% 0.16/5.41 inference(pre_NNF_transformation,[status(thm)],[f2])).
% 0.16/5.41 fof(f12,plain,(
% 0.16/5.41 ![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))))&(path_connected(X)|((a_member_of(X0,X)&a_member_of(X1,X))&(![P]: ~a_path_from_to_in(P,X0,X1,X)))))),
% 0.16/5.41 inference(NNF_transformation,[status(thm)],[f11])).
% 0.16/5.41 fof(f13,plain,(
% 0.16/5.41 (![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]: (path_connected(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)))))),
% 0.16/5.41 inference(miniscoping,[status(thm)],[f12])).
% 0.16/5.41 fof(f14,plain,(
% 0.16/5.41 (![X]: (~path_connected(X)|(![X0,X1]: ((~a_member_of(X0,X)|~a_member_of(X1,X))|a_path_from_to_in(sK1_skl(X1,X0,X),X0,X1,X)))))&(![X]: (path_connected(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)))))),
% 0.16/5.41 inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl]),skolemize(P,sK1_skl(X1,X0,X))],[f13])).
% 0.16/5.41 fof(f15,plain,(
% 0.16/5.41 ![X0,X1,X2]: (~path_connected(X0)|~a_member_of(X1,X0)|~a_member_of(X2,X0)|a_path_from_to_in(sK1_skl(X2,X1,X0),X1,X2,X0))),
% 0.16/5.41 inference(cnf_transformation,[status(thm)],[f14])).
% 0.16/5.41 fof(f19,plain,(
% 0.16/5.41 ![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)))),
% 0.16/5.41 inference(pre_NNF_transformation,[status(thm)],[f3])).
% 0.16/5.41 fof(f20,plain,(
% 0.16/5.41 ![X0,X1,X2,X3]: (~a_path_from_to_in(X0,X1,X2,X3)|a_group_isomorphism_from_to(alpha_hat(X0),first_homotop_grp(X3,X1),first_homotop_grp(X3,X2)))),
% 0.16/5.41 inference(cnf_transformation,[status(thm)],[f19])).
% 0.16/5.41 fof(f21,plain,(
% 0.16/5.41 (?[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))))),
% 0.16/5.41 inference(pre_NNF_transformation,[status(thm)],[f5])).
% 0.16/5.41 fof(f22,plain,(
% 0.16/5.41 (((path_connected(sK2_skl)&a_member_of(sK3_skl,sK2_skl))&a_member_of(sK4_skl,sK2_skl))&~isomorphic_groups(first_homotop_grp(sK2_skl,sK3_skl),first_homotop_grp(sK2_skl,sK4_skl)))),
% 0.16/5.41 inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl,sK3_skl,sK4_skl]),skolemize(X,sK2_skl),skolemize(X0,sK3_skl),skolemize(X1,sK4_skl)],[f21])).
% 0.16/5.41 fof(f23,plain,(
% 0.16/5.41 path_connected(sK2_skl)),
% 0.16/5.41 inference(cnf_transformation,[status(thm)],[f22])).
% 0.16/5.41 fof(f24,plain,(
% 0.16/5.41 a_member_of(sK3_skl,sK2_skl)),
% 0.16/5.41 inference(cnf_transformation,[status(thm)],[f22])).
% 0.16/5.41 fof(f25,plain,(
% 0.16/5.41 a_member_of(sK4_skl,sK2_skl)),
% 0.16/5.41 inference(cnf_transformation,[status(thm)],[f22])).
% 0.16/5.41 fof(f26,plain,(
% 0.16/5.41 ~isomorphic_groups(first_homotop_grp(sK2_skl,sK3_skl),first_homotop_grp(sK2_skl,sK4_skl))),
% 0.16/5.41 inference(cnf_transformation,[status(thm)],[f22])).
% 0.16/5.41 fof(f27,plain,(
% 0.16/5.41 ![X0,X1]: (~a_member_of(X0,sK2_skl)|~a_member_of(X1,sK2_skl)|a_path_from_to_in(sK1_skl(X1,X0,sK2_skl),X0,X1,sK2_skl))),
% 0.16/5.41 inference(resolution,[status(thm)],[f15,f23])).
% 0.16/5.41 fof(f28,plain,(
% 0.16/5.41 ![X0,X1]: (~a_member_of(X0,sK2_skl)|~a_member_of(X1,sK2_skl)|a_group_isomorphism_from_to(alpha_hat(sK1_skl(X1,X0,sK2_skl)),first_homotop_grp(sK2_skl,X0),first_homotop_grp(sK2_skl,X1)))),
% 0.16/5.41 inference(resolution,[status(thm)],[f27,f20])).
% 0.16/5.41 fof(f44,plain,(
% 0.16/5.41 ![X0,X1]: (~a_member_of(X0,sK2_skl)|~a_member_of(X1,sK2_skl)|isomorphic_groups(first_homotop_grp(sK2_skl,X0),first_homotop_grp(sK2_skl,X1)))),
% 0.16/5.41 inference(resolution,[status(thm)],[f28,f10])).
% 0.16/5.41 fof(f45,plain,(
% 0.16/5.41 ~a_member_of(sK3_skl,sK2_skl)|~a_member_of(sK4_skl,sK2_skl)),
% 0.16/5.41 inference(resolution,[status(thm)],[f44,f26])).
% 0.16/5.41 fof(f47,definition,(
% 0.16/5.41 sQ2_spl <=> (a_member_of(sK3_skl,sK2_skl))),
% 0.16/5.41 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.16/5.41 fof(f49,plain,(
% 0.16/5.41 ~a_member_of(sK3_skl,sK2_skl)|sQ2_spl),
% 0.16/5.41 inference(component_clause,[status(thm)],[f47])).
% 0.16/5.41 fof(f50,definition,(
% 0.16/5.41 sQ3_spl <=> (a_member_of(sK4_skl,sK2_skl))),
% 0.16/5.41 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 0.16/5.41 fof(f52,plain,(
% 0.16/5.41 ~a_member_of(sK4_skl,sK2_skl)|sQ3_spl),
% 0.16/5.41 inference(component_clause,[status(thm)],[f50])).
% 0.16/5.41 fof(f53,plain,(
% 0.16/5.41 ~sQ2_spl|~sQ3_spl),
% 0.16/5.41 inference(split_clause,[status(thm)],[f45,f47,f50])).
% 0.16/5.41 fof(f54,plain,(
% 0.16/5.41 $false|sQ2_spl),
% 0.16/5.41 inference(forward_subsumption_resolution,[status(thm)],[f49,f24])).
% 0.16/5.41 fof(f55,plain,(
% 0.16/5.41 sQ2_spl),
% 0.16/5.41 inference(contradiction_clause,[status(thm)],[f54])).
% 0.16/5.41 fof(f56,plain,(
% 0.16/5.41 $false|sQ3_spl),
% 0.16/5.41 inference(forward_subsumption_resolution,[status(thm)],[f52,f25])).
% 0.16/5.41 fof(f57,plain,(
% 0.16/5.41 sQ3_spl),
% 0.16/5.41 inference(contradiction_clause,[status(thm)],[f56])).
% 0.16/5.41 fof(f58,plain,(
% 0.16/5.41 $false),
% 0.16/5.41 inference(sat_refutation,[status(thm)],[f53,f55,f57])).
% 0.16/5.41 % SZS output end CNFRefutation for theBenchmark.p
% 0.16/5.45 % Elapsed time: 0.046466 seconds
% 0.16/5.45 % CPU time: 0.129075 seconds
% 0.16/5.45 % Total memory used: 16.862 MB
% 0.16/5.45 % Net memory used: 16.404 MB
%------------------------------------------------------------------------------