%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : SET872+1 : TPTP v8.1.2. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n006.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:35 EDT 2023
% Result : Theorem 1.73s 2.41s
% Output : Proof 1.73s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : SET872+1 : TPTP v8.1.2. Released v3.2.0.
% 0.11/0.12 % Command : nanocop.sh %s %d
% 0.12/0.33 % Computer : n006.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.34 % WCLimit : 300
% 0.12/0.34 % DateTime : Thu May 18 19:02:21 EDT 2023
% 0.12/0.34 % CPUTime :
% 1.73/2.41
% 1.73/2.41 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 1.73/2.41 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 1.73/2.41 %-----------------------------------------------------
% 1.73/2.41 ncf(matrix, plain, [(185 ^ _24804) ^ [] : [subset(singleton(182 ^ []), unordered_pair(182 ^ [], 183 ^ []))], (58 ^ _24804) ^ [_26745, _26747] : [_26747 = _26745, -(singleton(_26747) = singleton(_26745))], (64 ^ _24804) ^ [_26971, _26973, _26975, _26977] : [-(unordered_pair(_26977, _26973) = unordered_pair(_26975, _26971)), _26977 = _26975, _26973 = _26971], (2 ^ _24804) ^ [_24948] : [-(_24948 = _24948)], (4 ^ _24804) ^ [_25055, _25057] : [_25057 = _25055, -(_25055 = _25057)], (10 ^ _24804) ^ [_25259, _25261, _25263] : [-(_25263 = _25259), _25263 = _25261, _25261 = _25259], (20 ^ _24804) ^ [_25600, _25602, _25604, _25606] : [-(in(_25604, _25600)), in(_25606, _25602), _25606 = _25604, _25602 = _25600], (34 ^ _24804) ^ [_26016, _26018] : [-(empty(_26016)), _26018 = _26016, empty(_26018)], (44 ^ _24804) ^ [_26319, _26321, _26323, _26325] : [-(subset(_26323, _26319)), subset(_26325, _26321), _26325 = _26323, _26321 = _26319], (74 ^ _24804) ^ [_27308, _27310] : [in(_27310, _27308), in(_27308, _27310)], (80 ^ _24804) ^ [_27504, _27506] : [-(unordered_pair(_27506, _27504) = unordered_pair(_27504, _27506))], (98 ^ _24804) ^ [_28169, _28171] : [-(_28169 = singleton(_28171)), 102 ^ _24804 : [(103 ^ _24804) ^ [] : [-(in(99 ^ [_28169, _28171], _28169))], (105 ^ _24804) ^ [] : [99 ^ [_28169, _28171] = _28171]], 106 ^ _24804 : [(107 ^ _24804) ^ [] : [-(99 ^ [_28169, _28171] = _28171)], (109 ^ _24804) ^ [] : [in(99 ^ [_28169, _28171], _28169)]]], (82 ^ _24804) ^ [_27648, _27650] : [_27648 = singleton(_27650), 85 ^ _24804 : [(86 ^ _24804) ^ [_27818] : [in(_27818, _27648), -(_27818 = _27650)], (92 ^ _24804) ^ [_27990] : [_27990 = _27650, -(in(_27990, _27648))]]], (176 ^ _24804) ^ [] : [-(empty(174 ^ []))], (179 ^ _24804) ^ [] : [empty(177 ^ [])], (181 ^ _24804) ^ [_31068, _31070] : [-(subset(_31070, _31070))], (166 ^ _24804) ^ [_30567, _30569] : [168 ^ _24804 : [(169 ^ _24804) ^ [] : [-(in(167 ^ [_30567, _30569], _30569))], (171 ^ _24804) ^ [] : [in(167 ^ [_30567, _30569], _30567)]], -(subset(_30569, _30567))], (156 ^ _24804) ^ [_30253, _30255] : [subset(_30255, _30253), 159 ^ _24804 : [(160 ^ _24804) ^ [_30390] : [in(_30390, _30255), -(in(_30390, _30253))]]], (135 ^ _24804) ^ [_29473, _29475, _29477] : [-(_29473 = unordered_pair(_29477, _29475)), 139 ^ _24804 : [(140 ^ _24804) ^ [] : [-(in(136 ^ [_29473, _29475, _29477], _29473))], (142 ^ _24804) ^ [] : [136 ^ [_29473, _29475, _29477] = _29477], (144 ^ _24804) ^ [] : [136 ^ [_29473, _29475, _29477] = _29475]], 145 ^ _24804 : [(152 ^ _24804) ^ [] : [in(136 ^ [_29473, _29475, _29477], _29473)], (146 ^ _24804) ^ [] : [-(136 ^ [_29473, _29475, _29477] = _29477), -(136 ^ [_29473, _29475, _29477] = _29475)]]], (113 ^ _24804) ^ [_28748, _28750, _28752] : [_28748 = unordered_pair(_28752, _28750), 116 ^ _24804 : [(127 ^ _24804) ^ [_29208] : [128 ^ _24804 : [(129 ^ _24804) ^ [] : [_29208 = _28752], (131 ^ _24804) ^ [] : [_29208 = _28750]], -(in(_29208, _28748))], (117 ^ _24804) ^ [_28930] : [in(_28930, _28748), -(_28930 = _28752), -(_28930 = _28750)]]]], input).
% 1.73/2.41 ncf('1',plain,[subset(singleton(182 ^ []), unordered_pair(182 ^ [], 183 ^ []))],start(185 ^ 0)).
% 1.73/2.41 ncf('1.1',plain,[-(subset(singleton(182 ^ []), unordered_pair(182 ^ [], 183 ^ []))), 171 : in(167 ^ [unordered_pair(182 ^ [], 183 ^ []), singleton(182 ^ [])], unordered_pair(182 ^ [], 183 ^ []))],extension(166 ^ 1,bind([[_30567, _30569], [unordered_pair(182 ^ [], 183 ^ []), singleton(182 ^ [])]]))).
% 1.73/2.41 ncf('1.1.1',plain,[-(in(167 ^ [unordered_pair(182 ^ [], 183 ^ []), singleton(182 ^ [])], unordered_pair(182 ^ [], 183 ^ []))), 129 : 167 ^ [unordered_pair(182 ^ [], 183 ^ []), singleton(182 ^ [])] = 167 ^ [unordered_pair(182 ^ [], 183 ^ []), singleton(182 ^ [])], 127 : unordered_pair(182 ^ [], 183 ^ []) = unordered_pair(167 ^ [unordered_pair(182 ^ [], 183 ^ []), singleton(182 ^ [])], 183 ^ [])],extension(113 ^ 4,bind([[_28748, _28750, _28752, _29208], [unordered_pair(182 ^ [], 183 ^ []), 183 ^ [], 167 ^ [unordered_pair(182 ^ [], 183 ^ []), singleton(182 ^ [])], 167 ^ [unordered_pair(182 ^ [], 183 ^ []), singleton(182 ^ [])]]]))).
% 1.73/2.41 ncf('1.1.1.1',plain,[-(167 ^ [unordered_pair(182 ^ [], 183 ^ []), singleton(182 ^ [])] = 167 ^ [unordered_pair(182 ^ [], 183 ^ []), singleton(182 ^ [])])],extension(2 ^ 9,bind([[_24948], [167 ^ [unordered_pair(182 ^ [], 183 ^ []), singleton(182 ^ [])]]]))).
% 1.73/2.41 ncf('1.1.1.2',plain,[-(unordered_pair(182 ^ [], 183 ^ []) = unordered_pair(167 ^ [unordered_pair(182 ^ [], 183 ^ []), singleton(182 ^ [])], 183 ^ [])), 182 ^ [] = 167 ^ [unordered_pair(182 ^ [], 183 ^ []), singleton(182 ^ [])], 183 ^ [] = 183 ^ []],extension(64 ^ 5,bind([[_26971, _26973, _26975, _26977], [183 ^ [], 183 ^ [], 167 ^ [unordered_pair(182 ^ [], 183 ^ []), singleton(182 ^ [])], 182 ^ []]]))).
% 1.73/2.41 ncf('1.1.1.2.1',plain,[-(182 ^ [] = 167 ^ [unordered_pair(182 ^ [], 183 ^ []), singleton(182 ^ [])]), 167 ^ [unordered_pair(182 ^ [], 183 ^ []), singleton(182 ^ [])] = 182 ^ []],extension(4 ^ 6,bind([[_25055, _25057], [182 ^ [], 167 ^ [unordered_pair(182 ^ [], 183 ^ []), singleton(182 ^ [])]]]))).
% 1.73/2.41 ncf('1.1.1.2.1.1',plain,[-(167 ^ [unordered_pair(182 ^ [], 183 ^ []), singleton(182 ^ [])] = 182 ^ []), 86 : in(167 ^ [unordered_pair(182 ^ [], 183 ^ []), singleton(182 ^ [])], singleton(182 ^ [])), 86 : singleton(182 ^ []) = singleton(182 ^ [])],extension(82 ^ 7,bind([[_27648, _27650, _27818], [singleton(182 ^ []), 182 ^ [], 167 ^ [unordered_pair(182 ^ [], 183 ^ []), singleton(182 ^ [])]]]))).
% 1.73/2.41 ncf('1.1.1.2.1.1.1',plain,[-(in(167 ^ [unordered_pair(182 ^ [], 183 ^ []), singleton(182 ^ [])], singleton(182 ^ [])))],extension(169 ^ 10)).
% 1.73/2.41 ncf('1.1.1.2.1.1.2',plain,[-(singleton(182 ^ []) = singleton(182 ^ []))],extension(2 ^ 8,bind([[_24948], [singleton(182 ^ [])]]))).
% 1.73/2.41 ncf('1.1.1.2.2',plain,[-(183 ^ [] = 183 ^ [])],extension(2 ^ 6,bind([[_24948], [183 ^ []]]))).
% 1.73/2.41 %-----------------------------------------------------
% 1.73/2.41 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------