%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : SET887+1 : TPTP v8.1.2. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n022.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 11:56:36 EDT 2023
% Result : Theorem 48.12s 46.86s
% Output : Proof 48.12s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12 % Problem : SET887+1 : TPTP v8.1.2. Released v3.2.0.
% 0.06/0.12 % Command : nanocop.sh %s %d
% 0.12/0.33 % Computer : n022.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Thu May 18 19:05:47 EDT 2023
% 0.12/0.33 % CPUTime :
% 48.12/46.86
% 48.12/46.86 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 48.12/46.86 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 48.12/46.86 %-----------------------------------------------------
% 48.12/46.86 ncf(matrix, plain, [(202 ^ _43969) ^ [] : [193 ^ [] = 196 ^ []], (200 ^ _43969) ^ [] : [193 ^ [] = 195 ^ []], (198 ^ _43969) ^ [] : [-(subset(unordered_pair(193 ^ [], 194 ^ []), unordered_pair(195 ^ [], 196 ^ [])))], !, (10 ^ _37074) ^ [_37509, _37511, _37513] : [-(_37513 = _37509), _37513 = _37511, _37511 = _37509], (188 ^ _37074) ^ [_43525, _43527, _43529] : [singleton(_43529) = unordered_pair(_43527, _43525), -(_43529 = _43527)], (58 ^ _37074) ^ [_38995, _38997] : [_38997 = _38995, -(singleton(_38997) = singleton(_38995))], (176 ^ _37074) ^ [_43058, _43060] : [-(subset(_43060, _43060))], (140 ^ _37074) ^ [_41940, _41942, _41944] : [subset(_41944, unordered_pair(_41942, _41940)), -(_41944 = empty_set), -(_41944 = singleton(_41942)), -(_41944 = singleton(_41940)), -(_41944 = unordered_pair(_41942, _41940))], (117 ^ _37074) ^ [_41093, _41095, _41097] : [-(_41093 = unordered_pair(_41097, _41095)), 121 ^ _37074 : [(126 ^ _37074) ^ [] : [118 ^ [_41093, _41095, _41097] = _41095], (124 ^ _37074) ^ [] : [118 ^ [_41093, _41095, _41097] = _41097], (122 ^ _37074) ^ [] : [-(in(118 ^ [_41093, _41095, _41097], _41093))]], 127 ^ _37074 : [(128 ^ _37074) ^ [] : [-(118 ^ [_41093, _41095, _41097] = _41097), -(118 ^ [_41093, _41095, _41097] = _41095)], (134 ^ _37074) ^ [] : [in(118 ^ [_41093, _41095, _41097], _41093)]]], (44 ^ _37074) ^ [_38569, _38571, _38573, _38575] : [-(subset(_38573, _38569)), subset(_38575, _38571), _38575 = _38573, _38571 = _38569], (88 ^ _37074) ^ [_40063] : [-(in(89 ^ [_40063], _40063)), -(_40063 = empty_set)], (138 ^ _37074) ^ [] : [-(empty(empty_set))], (95 ^ _37074) ^ [_40368, _40370, _40372] : [_40368 = unordered_pair(_40372, _40370), 98 ^ _37074 : [(99 ^ _37074) ^ [_40550] : [in(_40550, _40368), -(_40550 = _40372), -(_40550 = _40370)], (109 ^ _37074) ^ [_40828] : [110 ^ _37074 : [(113 ^ _37074) ^ [] : [_40828 = _40370], (111 ^ _37074) ^ [] : [_40828 = _40372]], -(in(_40828, _40368))]]], (82 ^ _37074) ^ [_39884] : [_39884 = empty_set, 85 ^ _37074 : [(86 ^ _37074) ^ [_39997] : [in(_39997, _39884)]]], (171 ^ _37074) ^ [] : [-(empty(169 ^ []))], (20 ^ _37074) ^ [_37850, _37852, _37854, _37856] : [-(in(_37854, _37850)), in(_37856, _37852), _37856 = _37854, _37852 = _37850], (34 ^ _37074) ^ [_38266, _38268] : [-(empty(_38266)), _38268 = _38266, empty(_38268)], (2 ^ _37074) ^ [_37198] : [-(_37198 = _37198)], (4 ^ _37074) ^ [_37305, _37307] : [_37307 = _37305, -(_37305 = _37307)], (178 ^ _37074) ^ [_43195, _43197, _43199, _43201] : [unordered_pair(_43201, _43199) = unordered_pair(_43197, _43195), -(_43201 = _43197), -(_43201 = _43195)], (74 ^ _37074) ^ [_39558, _39560] : [in(_39560, _39558), in(_39558, _39560)], (80 ^ _37074) ^ [_39754, _39756] : [-(unordered_pair(_39756, _39754) = unordered_pair(_39754, _39756))], (158 ^ _37074) ^ [_42420, _42422, _42424] : [159 ^ _37074 : [(162 ^ _37074) ^ [] : [_42424 = singleton(_42422)], (164 ^ _37074) ^ [] : [_42424 = singleton(_42420)], (166 ^ _37074) ^ [] : [_42424 = unordered_pair(_42422, _42420)], (160 ^ _37074) ^ [] : [_42424 = empty_set]], -(subset(_42424, unordered_pair(_42422, _42420)))], (174 ^ _37074) ^ [] : [empty(172 ^ [])], (64 ^ _37074) ^ [_39221, _39223, _39225, _39227] : [-(unordered_pair(_39227, _39223) = unordered_pair(_39225, _39221)), _39227 = _39225, _39223 = _39221]], input).
% 48.12/46.86 ncf('1',plain,[-(subset(unordered_pair(193 ^ [], 194 ^ []), unordered_pair(195 ^ [], 196 ^ [])))],start(198 ^ 0)).
% 48.12/46.86 ncf('1.1',plain,[subset(unordered_pair(193 ^ [], 194 ^ []), unordered_pair(195 ^ [], 196 ^ [])), -(unordered_pair(193 ^ [], 194 ^ []) = empty_set), -(unordered_pair(193 ^ [], 194 ^ []) = singleton(195 ^ [])), -(unordered_pair(193 ^ [], 194 ^ []) = singleton(196 ^ [])), -(unordered_pair(193 ^ [], 194 ^ []) = unordered_pair(195 ^ [], 196 ^ []))],extension(140 ^ 1,bind([[_41940, _41942, _41944], [196 ^ [], 195 ^ [], unordered_pair(193 ^ [], 194 ^ [])]]))).
% 48.12/46.86 ncf('1.1.1',plain,[unordered_pair(193 ^ [], 194 ^ []) = empty_set, 109 : -(in(unordered_pair(193 ^ [], 194 ^ []), unordered_pair(193 ^ [], 194 ^ []))), 109 : unordered_pair(193 ^ [], 194 ^ []) = unordered_pair(_23654, empty_set)],extension(95 ^ 2,bind([[_40368, _40370, _40372, _40828], [unordered_pair(193 ^ [], 194 ^ []), empty_set, _23654, unordered_pair(193 ^ [], 194 ^ [])]]))).
% 48.12/46.86 ncf('1.1.1.1',plain,[in(unordered_pair(193 ^ [], 194 ^ []), unordered_pair(193 ^ [], 194 ^ [])), unordered_pair(193 ^ [], 194 ^ []) = empty_set],extension(82 ^ 5,bind([[_39884, _39997], [unordered_pair(193 ^ [], 194 ^ []), unordered_pair(193 ^ [], 194 ^ [])]]))).
% 48.12/46.86 ncf('1.1.1.1.1',plain,[-(unordered_pair(193 ^ [], 194 ^ []) = empty_set)],reduction('1.1')).
% 48.12/46.86 ncf('1.1.1.2',plain,[-(unordered_pair(193 ^ [], 194 ^ []) = unordered_pair(_23654, empty_set)), unordered_pair(unordered_pair(193 ^ [], 194 ^ []), unordered_pair(_23654, empty_set)) = unordered_pair(unordered_pair(_23654, empty_set), unordered_pair(193 ^ [], 194 ^ [])), -(unordered_pair(193 ^ [], 194 ^ []) = unordered_pair(193 ^ [], 194 ^ []))],extension(178 ^ 3,bind([[_43195, _43197, _43199, _43201], [unordered_pair(193 ^ [], 194 ^ []), unordered_pair(_23654, empty_set), unordered_pair(_23654, empty_set), unordered_pair(193 ^ [], 194 ^ [])]]))).
% 48.12/46.86 ncf('1.1.1.2.1',plain,[-(unordered_pair(unordered_pair(193 ^ [], 194 ^ []), unordered_pair(_23654, empty_set)) = unordered_pair(unordered_pair(_23654, empty_set), unordered_pair(193 ^ [], 194 ^ []))), unordered_pair(unordered_pair(_23654, empty_set), unordered_pair(193 ^ [], 194 ^ [])) = unordered_pair(unordered_pair(193 ^ [], 194 ^ []), unordered_pair(_23654, empty_set))],extension(4 ^ 4,bind([[_37305, _37307], [unordered_pair(unordered_pair(193 ^ [], 194 ^ []), unordered_pair(_23654, empty_set)), unordered_pair(unordered_pair(_23654, empty_set), unordered_pair(193 ^ [], 194 ^ []))]]))).
% 48.12/46.86 ncf('1.1.1.2.1.1',plain,[-(unordered_pair(unordered_pair(_23654, empty_set), unordered_pair(193 ^ [], 194 ^ [])) = unordered_pair(unordered_pair(193 ^ [], 194 ^ []), unordered_pair(_23654, empty_set)))],extension(80 ^ 5,bind([[_39754, _39756], [unordered_pair(193 ^ [], 194 ^ []), unordered_pair(_23654, empty_set)]]))).
% 48.12/46.86 ncf('1.1.1.2.2',plain,[unordered_pair(193 ^ [], 194 ^ []) = unordered_pair(193 ^ [], 194 ^ []), 113 : 194 ^ [] = 194 ^ [], 113 : -(in(194 ^ [], unordered_pair(193 ^ [], 194 ^ [])))],extension(95 ^ 4,bind([[_40368, _40370, _40372, _40828], [unordered_pair(193 ^ [], 194 ^ []), 194 ^ [], 193 ^ [], 194 ^ []]]))).
% 48.12/46.86 ncf('1.1.1.2.2.1',plain,[-(194 ^ [] = 194 ^ [])],extension(2 ^ 9,bind([[_37198], [194 ^ []]]))).
% 48.12/46.86 ncf('1.1.1.2.2.2',plain,[in(194 ^ [], unordered_pair(193 ^ [], 194 ^ [])), unordered_pair(193 ^ [], 194 ^ []) = empty_set],extension(82 ^ 7,bind([[_39884, _39997], [unordered_pair(193 ^ [], 194 ^ []), 194 ^ []]]))).
% 48.12/46.86 ncf('1.1.1.2.2.2.1',plain,[-(unordered_pair(193 ^ [], 194 ^ []) = empty_set)],reduction('1.1')).
% 48.12/46.86 ncf('1.1.2',plain,[unordered_pair(193 ^ [], 194 ^ []) = singleton(195 ^ []), -(singleton(195 ^ []) = unordered_pair(193 ^ [], 194 ^ []))],extension(4 ^ 2,bind([[_37305, _37307], [singleton(195 ^ []), unordered_pair(193 ^ [], 194 ^ [])]]))).
% 48.12/46.86 ncf('1.1.2.1',plain,[singleton(195 ^ []) = unordered_pair(193 ^ [], 194 ^ []), -(singleton(195 ^ []) = unordered_pair(193 ^ [], 194 ^ [])), unordered_pair(193 ^ [], 194 ^ []) = unordered_pair(193 ^ [], 194 ^ [])],extension(10 ^ 3,bind([[_37509, _37511, _37513], [unordered_pair(193 ^ [], 194 ^ []), unordered_pair(193 ^ [], 194 ^ []), singleton(195 ^ [])]]))).
% 48.12/46.86 ncf('1.1.2.1.1',plain,[singleton(195 ^ []) = unordered_pair(193 ^ [], 194 ^ []), -(195 ^ [] = 193 ^ [])],extension(188 ^ 4,bind([[_43525, _43527, _43529], [194 ^ [], 193 ^ [], 195 ^ []]]))).
% 48.12/46.86 ncf('1.1.2.1.1.1',plain,[195 ^ [] = 193 ^ [], -(193 ^ [] = 195 ^ [])],extension(4 ^ 5,bind([[_37305, _37307], [193 ^ [], 195 ^ []]]))).
% 48.12/46.86 ncf('1.1.2.1.1.1.1',plain,[193 ^ [] = 195 ^ []],extension(200 ^ 6)).
% 48.12/46.86 ncf('1.1.2.1.2',plain,[-(unordered_pair(193 ^ [], 194 ^ []) = unordered_pair(193 ^ [], 194 ^ [])), unordered_pair(193 ^ [], 194 ^ []) = singleton(195 ^ []), singleton(195 ^ []) = unordered_pair(193 ^ [], 194 ^ [])],extension(10 ^ 4,bind([[_37509, _37511, _37513], [unordered_pair(193 ^ [], 194 ^ []), singleton(195 ^ []), unordered_pair(193 ^ [], 194 ^ [])]]))).
% 48.12/46.86 ncf('1.1.2.1.2.1',plain,[-(unordered_pair(193 ^ [], 194 ^ []) = singleton(195 ^ []))],reduction('1.1')).
% 48.12/46.86 ncf('1.1.2.1.2.2',plain,[-(singleton(195 ^ []) = unordered_pair(193 ^ [], 194 ^ []))],reduction('1.1.2')).
% 48.12/46.86 ncf('1.1.3',plain,[unordered_pair(193 ^ [], 194 ^ []) = singleton(196 ^ []), -(singleton(196 ^ []) = unordered_pair(193 ^ [], 194 ^ []))],extension(4 ^ 2,bind([[_37305, _37307], [singleton(196 ^ []), unordered_pair(193 ^ [], 194 ^ [])]]))).
% 48.12/46.86 ncf('1.1.3.1',plain,[singleton(196 ^ []) = unordered_pair(193 ^ [], 194 ^ []), -(singleton(196 ^ []) = unordered_pair(193 ^ [], 194 ^ [])), unordered_pair(193 ^ [], 194 ^ []) = unordered_pair(193 ^ [], 194 ^ [])],extension(10 ^ 3,bind([[_37509, _37511, _37513], [unordered_pair(193 ^ [], 194 ^ []), unordered_pair(193 ^ [], 194 ^ []), singleton(196 ^ [])]]))).
% 48.12/46.86 ncf('1.1.3.1.1',plain,[singleton(196 ^ []) = unordered_pair(193 ^ [], 194 ^ []), -(196 ^ [] = 193 ^ [])],extension(188 ^ 4,bind([[_43525, _43527, _43529], [194 ^ [], 193 ^ [], 196 ^ []]]))).
% 48.12/46.86 ncf('1.1.3.1.1.1',plain,[196 ^ [] = 193 ^ [], -(193 ^ [] = 196 ^ [])],extension(4 ^ 5,bind([[_37305, _37307], [193 ^ [], 196 ^ []]]))).
% 48.12/46.86 ncf('1.1.3.1.1.1.1',plain,[193 ^ [] = 196 ^ []],extension(202 ^ 6)).
% 48.12/46.86 ncf('1.1.3.1.2',plain,[-(unordered_pair(193 ^ [], 194 ^ []) = unordered_pair(193 ^ [], 194 ^ [])), unordered_pair(193 ^ [], 194 ^ []) = singleton(196 ^ []), singleton(196 ^ []) = unordered_pair(193 ^ [], 194 ^ [])],extension(10 ^ 4,bind([[_37509, _37511, _37513], [unordered_pair(193 ^ [], 194 ^ []), singleton(196 ^ []), unordered_pair(193 ^ [], 194 ^ [])]]))).
% 48.12/46.86 ncf('1.1.3.1.2.1',plain,[-(unordered_pair(193 ^ [], 194 ^ []) = singleton(196 ^ []))],reduction('1.1')).
% 48.12/46.86 ncf('1.1.3.1.2.2',plain,[-(singleton(196 ^ []) = unordered_pair(193 ^ [], 194 ^ []))],reduction('1.1.3')).
% 48.12/46.86 ncf('1.1.4',plain,[unordered_pair(193 ^ [], 194 ^ []) = unordered_pair(195 ^ [], 196 ^ []), -(196 ^ [] = unordered_pair(195 ^ [], 196 ^ [])), 196 ^ [] = unordered_pair(193 ^ [], 194 ^ [])],extension(10 ^ 2,bind([[_37509, _37511, _37513], [unordered_pair(195 ^ [], 196 ^ []), unordered_pair(193 ^ [], 194 ^ []), 196 ^ []]]))).
% 48.12/46.86 ncf('1.1.4.1',plain,[196 ^ [] = unordered_pair(195 ^ [], 196 ^ []), -(193 ^ [] = unordered_pair(195 ^ [], 196 ^ [])), 193 ^ [] = 196 ^ []],extension(10 ^ 3,bind([[_37509, _37511, _37513], [unordered_pair(195 ^ [], 196 ^ []), 196 ^ [], 193 ^ []]]))).
% 48.12/46.86 ncf('1.1.4.1.1',plain,[193 ^ [] = unordered_pair(195 ^ [], 196 ^ []), -(193 ^ [] = 196 ^ []), unordered_pair(195 ^ [], 196 ^ []) = 196 ^ []],extension(10 ^ 4,bind([[_37509, _37511, _37513], [196 ^ [], unordered_pair(195 ^ [], 196 ^ []), 193 ^ []]]))).
% 48.12/46.86 ncf('1.1.4.1.1.1',plain,[193 ^ [] = 196 ^ []],extension(202 ^ 5)).
% 48.12/46.86 ncf('1.1.4.1.1.2',plain,[-(unordered_pair(195 ^ [], 196 ^ []) = 196 ^ []), 196 ^ [] = unordered_pair(195 ^ [], 196 ^ [])],extension(4 ^ 5,bind([[_37305, _37307], [unordered_pair(195 ^ [], 196 ^ []), 196 ^ []]]))).
% 48.12/46.86 ncf('1.1.4.1.1.2.1',plain,[-(196 ^ [] = unordered_pair(195 ^ [], 196 ^ []))],reduction('1.1.4')).
% 48.12/46.86 ncf('1.1.4.1.2',plain,[-(193 ^ [] = 196 ^ []), unordered_pair(193 ^ [], 194 ^ []) = unordered_pair(195 ^ [], 196 ^ []), -(193 ^ [] = 195 ^ [])],extension(178 ^ 4,bind([[_43195, _43197, _43199, _43201], [196 ^ [], 195 ^ [], 194 ^ [], 193 ^ []]]))).
% 48.12/46.86 ncf('1.1.4.1.2.1',plain,[-(unordered_pair(193 ^ [], 194 ^ []) = unordered_pair(195 ^ [], 196 ^ []))],reduction('1.1')).
% 48.12/46.86 ncf('1.1.4.1.2.2',plain,[193 ^ [] = 195 ^ []],extension(200 ^ 5)).
% 48.12/46.86 ncf('1.1.4.2',plain,[-(196 ^ [] = unordered_pair(193 ^ [], 194 ^ [])), 99 : in(196 ^ [], unordered_pair(unordered_pair(193 ^ [], 194 ^ []), 196 ^ [])), 99 : -(196 ^ [] = 196 ^ []), 99 : unordered_pair(unordered_pair(193 ^ [], 194 ^ []), 196 ^ []) = unordered_pair(unordered_pair(193 ^ [], 194 ^ []), 196 ^ [])],extension(95 ^ 3,bind([[_40368, _40370, _40372, _40550], [unordered_pair(unordered_pair(193 ^ [], 194 ^ []), 196 ^ []), 196 ^ [], unordered_pair(193 ^ [], 194 ^ []), 196 ^ []]]))).
% 48.12/46.86 ncf('1.1.4.2.1',plain,[-(in(196 ^ [], unordered_pair(unordered_pair(193 ^ [], 194 ^ []), 196 ^ []))), 113 : 196 ^ [] = 196 ^ []],extension(109 ^ 6,bind([[_40828], [196 ^ []]]))).
% 48.12/46.86 ncf('1.1.4.2.1.1',plain,[-(196 ^ [] = 196 ^ [])],extension(2 ^ 9,bind([[_37198], [196 ^ []]]))).
% 48.12/46.86 ncf('1.1.4.2.2',plain,[196 ^ [] = 196 ^ [], -(193 ^ [] = 196 ^ []), 193 ^ [] = 196 ^ []],extension(10 ^ 6,bind([[_37509, _37511, _37513], [196 ^ [], 196 ^ [], 193 ^ []]]))).
% 48.12/46.86 ncf('1.1.4.2.2.1',plain,[193 ^ [] = 196 ^ []],extension(202 ^ 7)).
% 48.12/46.86 ncf('1.1.4.2.2.2',plain,[-(193 ^ [] = 196 ^ []), unordered_pair(193 ^ [], 194 ^ []) = unordered_pair(195 ^ [], 196 ^ []), -(193 ^ [] = 195 ^ [])],extension(178 ^ 7,bind([[_43195, _43197, _43199, _43201], [196 ^ [], 195 ^ [], 194 ^ [], 193 ^ []]]))).
% 48.12/46.86 ncf('1.1.4.2.2.2.1',plain,[-(unordered_pair(193 ^ [], 194 ^ []) = unordered_pair(195 ^ [], 196 ^ []))],reduction('1.1')).
% 48.12/46.86 ncf('1.1.4.2.2.2.2',plain,[193 ^ [] = 195 ^ []],extension(200 ^ 8)).
% 48.12/46.86 ncf('1.1.4.2.3',plain,[-(unordered_pair(unordered_pair(193 ^ [], 194 ^ []), 196 ^ []) = unordered_pair(unordered_pair(193 ^ [], 194 ^ []), 196 ^ []))],extension(2 ^ 4,bind([[_37198], [unordered_pair(unordered_pair(193 ^ [], 194 ^ []), 196 ^ [])]]))).
% 48.12/46.86 %-----------------------------------------------------
% 48.12/46.86 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------