%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : SEU195+1 : TPTP v8.1.2. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n015.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:02:36 EDT 2023
% Result : Theorem 0.52s 1.38s
% Output : Proof 0.52s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.12 % Problem : SEU195+1 : TPTP v8.1.2. Released v3.3.0.
% 0.08/0.12 % Command : nanocop.sh %s %d
% 0.13/0.34 % Computer : n015.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 : Thu May 18 13:05:37 EDT 2023
% 0.13/0.34 % CPUTime :
% 0.52/1.38
% 0.52/1.38 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 0.52/1.38 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.52/1.38 %-----------------------------------------------------
% 0.52/1.38 ncf(matrix, plain, [(393 ^ _59425) ^ [] : [-(relation(391 ^ []))], (395 ^ _59425) ^ [] : [relation_dom_restriction(391 ^ [], 390 ^ []) = relation_composition(identity_relation(390 ^ []), 391 ^ [])], (68 ^ _59425) ^ [_61663, _61665] : [_61665 = _61663, -(singleton(_61665) = singleton(_61663))], (74 ^ _59425) ^ [_61909, _61911, _61913, _61915] : [-(unordered_pair(_61915, _61911) = unordered_pair(_61913, _61909)), _61915 = _61913, _61911 = _61909], (84 ^ _59425) ^ [_62268, _62270, _62272, _62274] : [-(ordered_pair(_62274, _62270) = ordered_pair(_62272, _62268)), _62274 = _62272, _62270 = _62268], (94 ^ _59425) ^ [_62627, _62629, _62631, _62633] : [-(relation_dom_restriction(_62633, _62629) = relation_dom_restriction(_62631, _62627)), _62633 = _62631, _62629 = _62627], (114 ^ _59425) ^ [_63297, _63299] : [_63299 = _63297, -(identity_relation(_63299) = identity_relation(_63297))], (104 ^ _59425) ^ [_62986, _62988, _62990, _62992] : [-(relation_composition(_62992, _62988) = relation_composition(_62990, _62986)), _62992 = _62990, _62988 = _62986], (2 ^ _59425) ^ [_59569] : [-(_59569 = _59569)], (4 ^ _59425) ^ [_59676, _59678] : [_59678 = _59676, -(_59676 = _59678)], (10 ^ _59425) ^ [_59880, _59882, _59884] : [-(_59884 = _59880), _59884 = _59882, _59882 = _59880], (20 ^ _59425) ^ [_60221, _60223, _60225, _60227] : [-(element(_60225, _60221)), element(_60227, _60223), _60227 = _60225, _60223 = _60221], (34 ^ _59425) ^ [_60665, _60667, _60669, _60671] : [-(in(_60669, _60665)), in(_60671, _60667), _60671 = _60669, _60667 = _60665], (48 ^ _59425) ^ [_61081, _61083] : [-(empty(_61081)), _61083 = _61081, empty(_61083)], (58 ^ _59425) ^ [_61356, _61358] : [-(relation(_61356)), _61358 = _61356, relation(_61358)], (120 ^ _59425) ^ [_63537, _63539] : [in(_63539, _63537), in(_63537, _63539)], (126 ^ _59425) ^ [_63734] : [empty(_63734), -(relation(_63734))], (132 ^ _59425) ^ [_63919, _63921] : [-(unordered_pair(_63921, _63919) = unordered_pair(_63919, _63921))], (134 ^ _59425) ^ [_64020] : [relation(_64020), 137 ^ _59425 : [(138 ^ _59425) ^ [_64206, _64208] : [relation(_64206), 141 ^ _59425 : [(164 ^ _59425) ^ [] : [-(_64206 = relation_dom_restriction(_64020, _64208)), 177 ^ _59425 : [(178 ^ _59425) ^ [] : [-(in(165 ^ [_64020, _64206, _64208], _64208))], (180 ^ _59425) ^ [] : [-(in(ordered_pair(165 ^ [_64020, _64206, _64208], 166 ^ [_64020, _64206, _64208]), _64020))], (182 ^ _59425) ^ [] : [in(ordered_pair(165 ^ [_64020, _64206, _64208], 166 ^ [_64020, _64206, _64208]), _64206)]], 169 ^ _59425 : [(170 ^ _59425) ^ [] : [-(in(ordered_pair(165 ^ [_64020, _64206, _64208], 166 ^ [_64020, _64206, _64208]), _64206))], (172 ^ _59425) ^ [] : [in(165 ^ [_64020, _64206, _64208], _64208), in(ordered_pair(165 ^ [_64020, _64206, _64208], 166 ^ [_64020, _64206, _64208]), _64020)]]], (142 ^ _59425) ^ [] : [_64206 = relation_dom_restriction(_64020, _64208), 145 ^ _59425 : [(146 ^ _59425) ^ [_64531, _64533] : [in(ordered_pair(_64533, _64531), _64206), 149 ^ _59425 : [(150 ^ _59425) ^ [] : [-(in(_64533, _64208))], (152 ^ _59425) ^ [] : [-(in(ordered_pair(_64533, _64531), _64020))]]], (154 ^ _59425) ^ [_64810, _64812] : [-(in(ordered_pair(_64812, _64810), _64206)), in(_64812, _64208), in(ordered_pair(_64812, _64810), _64020)]]]]]]], (186 ^ _59425) ^ [_65965] : [relation(_65965), 189 ^ _59425 : [(190 ^ _59425) ^ [_66123] : [relation(_66123), 193 ^ _59425 : [(210 ^ _59425) ^ [] : [-(_65965 = _66123), 215 ^ _59425 : [(216 ^ _59425) ^ [] : [-(in(ordered_pair(211 ^ [_65965, _66123], 212 ^ [_65965, _66123]), _65965))], (218 ^ _59425) ^ [] : [in(ordered_pair(211 ^ [_65965, _66123], 212 ^ [_65965, _66123]), _66123)]], 219 ^ _59425 : [(220 ^ _59425) ^ [] : [-(in(ordered_pair(211 ^ [_65965, _66123], 212 ^ [_65965, _66123]), _66123))], (222 ^ _59425) ^ [] : [in(ordered_pair(211 ^ [_65965, _66123], 212 ^ [_65965, _66123]), _65965)]]], (194 ^ _59425) ^ [] : [_65965 = _66123, 197 ^ _59425 : [(198 ^ _59425) ^ [_66428, _66430] : [in(ordered_pair(_66430, _66428), _65965), -(in(ordered_pair(_66430, _66428), _66123))], (204 ^ _59425) ^ [_66618, _66620] : [in(ordered_pair(_66620, _66618), _66123), -(in(ordered_pair(_66620, _66618), _65965))]]]]]]], (226 ^ _59425) ^ [_67420, _67422] : [-(ordered_pair(_67422, _67420) = unordered_pair(unordered_pair(_67422, _67420), singleton(_67422)))], (228 ^ _59425) ^ [] : [true___, -(true___)], (234 ^ _59425) ^ [] : [true___, -(true___)], (240 ^ _59425) ^ [] : [true___, -(true___)], (246 ^ _59425) ^ [] : [true___, -(true___)], (252 ^ _59425) ^ [_68016, _68018] : [-(relation(relation_composition(_68018, _68016))), relation(_68018), relation(_68016)], (262 ^ _59425) ^ [_68286] : [-(relation(identity_relation(_68286)))], (264 ^ _59425) ^ [_68394, _68396] : [relation(_68396), -(relation(relation_dom_restriction(_68396, _68394)))], (270 ^ _59425) ^ [] : [true___, -(true___)], (277 ^ _59425) ^ [_68735] : [-(element(275 ^ [_68735], _68735))], (279 ^ _59425) ^ [_68847, _68849] : [286 ^ _59425 : [(287 ^ _59425) ^ [] : [-(empty(relation_composition(_68847, _68849)))], (289 ^ _59425) ^ [] : [-(relation(relation_composition(_68847, _68849)))]], empty(_68849), relation(_68847)], (291 ^ _59425) ^ [] : [-(empty(empty_set))], (293 ^ _59425) ^ [_69262, _69264] : [empty(ordered_pair(_69264, _69262))], (295 ^ _59425) ^ [_69343] : [empty(singleton(_69343))], (297 ^ _59425) ^ [_69435, _69437] : [empty(unordered_pair(_69437, _69435))], (299 ^ _59425) ^ [] : [-(empty(empty_set))], (301 ^ _59425) ^ [] : [-(relation(empty_set))], (303 ^ _59425) ^ [_69654, _69656] : [310 ^ _59425 : [(311 ^ _59425) ^ [] : [-(empty(relation_composition(_69656, _69654)))], (313 ^ _59425) ^ [] : [-(relation(relation_composition(_69656, _69654)))]], empty(_69656), relation(_69654)], (316 ^ _59425) ^ [] : [-(empty(314 ^ []))], (318 ^ _59425) ^ [] : [-(relation(314 ^ []))], (321 ^ _59425) ^ [] : [-(empty(319 ^ []))], (324 ^ _59425) ^ [] : [empty(322 ^ [])], (326 ^ _59425) ^ [] : [-(relation(322 ^ []))], (329 ^ _59425) ^ [] : [empty(327 ^ [])], (331 ^ _59425) ^ [_70510, _70512] : [in(_70512, _70510), -(element(_70512, _70510))], (337 ^ _59425) ^ [_70720, _70722] : [element(_70722, _70720), -(empty(_70720)), -(in(_70722, _70720))], (347 ^ _59425) ^ [_71004] : [empty(_71004), -(_71004 = empty_set)], (375 ^ _59425) ^ [_71927, _71929] : [in(_71929, _71927), empty(_71927)], (381 ^ _59425) ^ [_72114, _72116] : [empty(_72116), -(_72116 = _72114), empty(_72114)], (353 ^ _59425) ^ [_71234, _71236, _71238, _71240] : [relation(_71234), 356 ^ _59425 : [(357 ^ _59425) ^ [] : [in(ordered_pair(_71240, _71238), relation_composition(identity_relation(_71236), _71234)), 360 ^ _59425 : [(361 ^ _59425) ^ [] : [-(in(_71240, _71236))], (363 ^ _59425) ^ [] : [-(in(ordered_pair(_71240, _71238), _71234))]]], (365 ^ _59425) ^ [] : [-(in(ordered_pair(_71240, _71238), relation_composition(identity_relation(_71236), _71234))), in(_71240, _71236), in(ordered_pair(_71240, _71238), _71234)]]]], input).
% 0.52/1.38 ncf('1',plain,[relation_dom_restriction(391 ^ [], 390 ^ []) = relation_composition(identity_relation(390 ^ []), 391 ^ [])],start(395 ^ 0)).
% 0.52/1.38 ncf('1.1',plain,[-(relation_dom_restriction(391 ^ [], 390 ^ []) = relation_composition(identity_relation(390 ^ []), 391 ^ [])), relation_composition(identity_relation(390 ^ []), 391 ^ []) = relation_dom_restriction(391 ^ [], 390 ^ [])],extension(4 ^ 1,bind([[_59676, _59678], [relation_dom_restriction(391 ^ [], 390 ^ []), relation_composition(identity_relation(390 ^ []), 391 ^ [])]]))).
% 0.52/1.38 ncf('1.1.1',plain,[-(relation_composition(identity_relation(390 ^ []), 391 ^ []) = relation_dom_restriction(391 ^ [], 390 ^ [])), 178 : -(in(165 ^ [391 ^ [], relation_composition(identity_relation(390 ^ []), 391 ^ []), 390 ^ []], 390 ^ [])), 172 : in(165 ^ [391 ^ [], relation_composition(identity_relation(390 ^ []), 391 ^ []), 390 ^ []], 390 ^ []), 172 : in(ordered_pair(165 ^ [391 ^ [], relation_composition(identity_relation(390 ^ []), 391 ^ []), 390 ^ []], 166 ^ [391 ^ [], relation_composition(identity_relation(390 ^ []), 391 ^ []), 390 ^ []]), 391 ^ []), 164 : relation(relation_composition(identity_relation(390 ^ []), 391 ^ [])), 138 : relation(391 ^ [])],extension(134 ^ 2,bind([[_64020, _64206, _64208], [391 ^ [], relation_composition(identity_relation(390 ^ []), 391 ^ []), 390 ^ []]]))).
% 0.52/1.38 ncf('1.1.1.1',plain,[in(165 ^ [391 ^ [], relation_composition(identity_relation(390 ^ []), 391 ^ []), 390 ^ []], 390 ^ []), 365 : -(in(ordered_pair(165 ^ [391 ^ [], relation_composition(identity_relation(390 ^ []), 391 ^ []), 390 ^ []], 166 ^ [391 ^ [], relation_composition(identity_relation(390 ^ []), 391 ^ []), 390 ^ []]), relation_composition(identity_relation(390 ^ []), 391 ^ []))), 365 : in(ordered_pair(165 ^ [391 ^ [], relation_composition(identity_relation(390 ^ []), 391 ^ []), 390 ^ []], 166 ^ [391 ^ [], relation_composition(identity_relation(390 ^ []), 391 ^ []), 390 ^ []]), 391 ^ []), 365 : relation(391 ^ [])],extension(353 ^ 9,bind([[_71234, _71236, _71238, _71240], [391 ^ [], 390 ^ [], 166 ^ [391 ^ [], relation_composition(identity_relation(390 ^ []), 391 ^ []), 390 ^ []], 165 ^ [391 ^ [], relation_composition(identity_relation(390 ^ []), 391 ^ []), 390 ^ []]]]))).
% 0.52/1.38 ncf('1.1.1.1.1',plain,[in(ordered_pair(165 ^ [391 ^ [], relation_composition(identity_relation(390 ^ []), 391 ^ []), 390 ^ []], 166 ^ [391 ^ [], relation_composition(identity_relation(390 ^ []), 391 ^ []), 390 ^ []]), relation_composition(identity_relation(390 ^ []), 391 ^ []))],extension(182 ^ 12)).
% 0.52/1.38 ncf('1.1.1.1.2',plain,[-(in(ordered_pair(165 ^ [391 ^ [], relation_composition(identity_relation(390 ^ []), 391 ^ []), 390 ^ []], 166 ^ [391 ^ [], relation_composition(identity_relation(390 ^ []), 391 ^ []), 390 ^ []]), 391 ^ []))],extension(180 ^ 12)).
% 0.52/1.38 ncf('1.1.1.1.3',plain,[-(relation(391 ^ []))],extension(393 ^ 10)).
% 0.52/1.38 ncf('1.1.1.2',plain,[-(in(165 ^ [391 ^ [], relation_composition(identity_relation(390 ^ []), 391 ^ []), 390 ^ []], 390 ^ [])), 357 : in(ordered_pair(165 ^ [391 ^ [], relation_composition(identity_relation(390 ^ []), 391 ^ []), 390 ^ []], 166 ^ [391 ^ [], relation_composition(identity_relation(390 ^ []), 391 ^ []), 390 ^ []]), relation_composition(identity_relation(390 ^ []), 391 ^ [])), 357 : relation(391 ^ [])],extension(353 ^ 9,bind([[_71234, _71236, _71238, _71240], [391 ^ [], 390 ^ [], 166 ^ [391 ^ [], relation_composition(identity_relation(390 ^ []), 391 ^ []), 390 ^ []], 165 ^ [391 ^ [], relation_composition(identity_relation(390 ^ []), 391 ^ []), 390 ^ []]]]))).
% 0.52/1.38 ncf('1.1.1.2.1',plain,[-(in(ordered_pair(165 ^ [391 ^ [], relation_composition(identity_relation(390 ^ []), 391 ^ []), 390 ^ []], 166 ^ [391 ^ [], relation_composition(identity_relation(390 ^ []), 391 ^ []), 390 ^ []]), relation_composition(identity_relation(390 ^ []), 391 ^ [])))],extension(170 ^ 12)).
% 0.52/1.38 ncf('1.1.1.2.2',plain,[-(relation(391 ^ []))],extension(393 ^ 10)).
% 0.52/1.38 ncf('1.1.1.3',plain,[-(in(ordered_pair(165 ^ [391 ^ [], relation_composition(identity_relation(390 ^ []), 391 ^ []), 390 ^ []], 166 ^ [391 ^ [], relation_composition(identity_relation(390 ^ []), 391 ^ []), 390 ^ []]), 391 ^ [])), 357 : in(ordered_pair(165 ^ [391 ^ [], relation_composition(identity_relation(390 ^ []), 391 ^ []), 390 ^ []], 166 ^ [391 ^ [], relation_composition(identity_relation(390 ^ []), 391 ^ []), 390 ^ []]), relation_composition(identity_relation(390 ^ []), 391 ^ [])), 357 : relation(391 ^ [])],extension(353 ^ 9,bind([[_71234, _71236, _71238, _71240], [391 ^ [], 390 ^ [], 166 ^ [391 ^ [], relation_composition(identity_relation(390 ^ []), 391 ^ []), 390 ^ []], 165 ^ [391 ^ [], relation_composition(identity_relation(390 ^ []), 391 ^ []), 390 ^ []]]]))).
% 0.52/1.38 ncf('1.1.1.3.1',plain,[-(in(ordered_pair(165 ^ [391 ^ [], relation_composition(identity_relation(390 ^ []), 391 ^ []), 390 ^ []], 166 ^ [391 ^ [], relation_composition(identity_relation(390 ^ []), 391 ^ []), 390 ^ []]), relation_composition(identity_relation(390 ^ []), 391 ^ [])))],extension(170 ^ 12)).
% 0.52/1.38 ncf('1.1.1.3.2',plain,[-(relation(391 ^ []))],extension(393 ^ 10)).
% 0.52/1.38 ncf('1.1.1.4',plain,[-(relation(relation_composition(identity_relation(390 ^ []), 391 ^ []))), relation(identity_relation(390 ^ [])), relation(391 ^ [])],extension(252 ^ 5,bind([[_68016, _68018], [391 ^ [], identity_relation(390 ^ [])]]))).
% 0.52/1.38 ncf('1.1.1.4.1',plain,[-(relation(identity_relation(390 ^ [])))],extension(262 ^ 6,bind([[_68286], [390 ^ []]]))).
% 0.52/1.38 ncf('1.1.1.4.2',plain,[-(relation(391 ^ []))],extension(393 ^ 6)).
% 0.52/1.38 ncf('1.1.1.5',plain,[-(relation(391 ^ []))],extension(393 ^ 3)).
% 0.52/1.38 %-----------------------------------------------------
% 0.52/1.38 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------