%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : TOP022+1 : TPTP v8.1.2. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% 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 : Fri May 19 12:39:04 EDT 2023
% Result : Theorem 0.35s 1.40s
% Output : Proof 0.35s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.13 % Problem : TOP022+1 : TPTP v8.1.2. Released v3.1.0.
% 0.07/0.14 % Command : nanocop.sh %s %d
% 0.14/0.35 % Computer : n013.cluster.edu
% 0.14/0.35 % Model : x86_64 x86_64
% 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.35 % Memory : 8042.1875MB
% 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.35 % CPULimit : 300
% 0.14/0.35 % WCLimit : 300
% 0.14/0.35 % DateTime : Thu May 18 20:00:50 EDT 2023
% 0.14/0.35 % CPUTime :
% 0.35/1.40
% 0.35/1.40 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 0.35/1.40 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.35/1.40 %-----------------------------------------------------
% 0.35/1.40 ncf(matrix, plain, [(49 ^ _10795) ^ [] : [-(path_connected(45 ^ []))], (51 ^ _10795) ^ [] : [-(a_member_of(46 ^ [], 45 ^ []))], (53 ^ _10795) ^ [] : [-(a_member_of(47 ^ [], 45 ^ []))], (55 ^ _10795) ^ [] : [isomorphic_groups(first_homotop_grp(45 ^ [], 46 ^ []), first_homotop_grp(45 ^ [], 47 ^ []))], (2 ^ _10795) ^ [_10937, _10939] : [isomorphic_groups(_10939, _10937), -(a_group_isomorphism_from_to(5 ^ [_10937, _10939], _10939, _10937))], (9 ^ _10795) ^ [_11159, _11161] : [10 ^ _10795 : [(11 ^ _10795) ^ [_11230] : [a_group_isomorphism_from_to(_11230, _11161, _11159)]], -(isomorphic_groups(_11161, _11159))], (40 ^ _10795) ^ [_12263, _12265, _12267, _12269] : [a_path_from_to_in(_12269, _12267, _12265, _12263), -(a_group_isomorphism_from_to(alpha_hat(_12269), first_homotop_grp(_12263, _12267), first_homotop_grp(_12263, _12265)))], (30 ^ _10795) ^ [_11859, _11861, _11863] : [31 ^ _10795 : [(32 ^ _10795) ^ [] : [-(a_member_of(_11861, _11863))], (34 ^ _10795) ^ [] : [-(a_member_of(_11859, _11863))], (36 ^ _10795) ^ [_12082] : [a_path_from_to_in(_12082, _11861, _11859, _11863)]], -(path_connected(_11863))], (15 ^ _10795) ^ [_11438, _11440, _11442] : [path_connected(_11442), -(a_path_from_to_in(26 ^ [_11438, _11440, _11442], _11440, _11438, _11442)), a_member_of(_11440, _11442), a_member_of(_11438, _11442)]], input).
% 0.35/1.40 ncf('1',plain,[isomorphic_groups(first_homotop_grp(45 ^ [], 46 ^ []), first_homotop_grp(45 ^ [], 47 ^ []))],start(55 ^ 0)).
% 0.35/1.40 ncf('1.1',plain,[-(isomorphic_groups(first_homotop_grp(45 ^ [], 46 ^ []), first_homotop_grp(45 ^ [], 47 ^ []))), 11 : a_group_isomorphism_from_to(alpha_hat(26 ^ [47 ^ [], 46 ^ [], 45 ^ []]), first_homotop_grp(45 ^ [], 46 ^ []), first_homotop_grp(45 ^ [], 47 ^ []))],extension(9 ^ 1,bind([[_11159, _11161, _11230], [first_homotop_grp(45 ^ [], 47 ^ []), first_homotop_grp(45 ^ [], 46 ^ []), alpha_hat(26 ^ [47 ^ [], 46 ^ [], 45 ^ []])]]))).
% 0.35/1.40 ncf('1.1.1',plain,[-(a_group_isomorphism_from_to(alpha_hat(26 ^ [47 ^ [], 46 ^ [], 45 ^ []]), first_homotop_grp(45 ^ [], 46 ^ []), first_homotop_grp(45 ^ [], 47 ^ []))), a_path_from_to_in(26 ^ [47 ^ [], 46 ^ [], 45 ^ []], 46 ^ [], 47 ^ [], 45 ^ [])],extension(40 ^ 4,bind([[_12263, _12265, _12267, _12269], [45 ^ [], 47 ^ [], 46 ^ [], 26 ^ [47 ^ [], 46 ^ [], 45 ^ []]]]))).
% 0.35/1.40 ncf('1.1.1.1',plain,[-(a_path_from_to_in(26 ^ [47 ^ [], 46 ^ [], 45 ^ []], 46 ^ [], 47 ^ [], 45 ^ [])), path_connected(45 ^ []), a_member_of(46 ^ [], 45 ^ []), a_member_of(47 ^ [], 45 ^ [])],extension(15 ^ 5,bind([[_11438, _11440, _11442], [47 ^ [], 46 ^ [], 45 ^ []]]))).
% 0.35/1.40 ncf('1.1.1.1.1',plain,[-(path_connected(45 ^ []))],extension(49 ^ 6)).
% 0.35/1.40 ncf('1.1.1.1.2',plain,[-(a_member_of(46 ^ [], 45 ^ []))],extension(51 ^ 6)).
% 0.35/1.40 ncf('1.1.1.1.3',plain,[-(a_member_of(47 ^ [], 45 ^ []))],extension(53 ^ 6)).
% 0.35/1.40 %-----------------------------------------------------
% 0.35/1.40 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------