%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : SET596+3 : TPTP v8.1.2. Released v2.2.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n026.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:04 EDT 2023
% Result : Theorem 0.36s 1.38s
% Output : Proof 0.36s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : SET596+3 : TPTP v8.1.2. Released v2.2.0.
% 0.07/0.12 % Command : nanocop.sh %s %d
% 0.12/0.33 % Computer : n026.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:25:35 EDT 2023
% 0.12/0.33 % CPUTime :
% 0.36/1.38
% 0.36/1.38 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 0.36/1.38 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.36/1.38 %-----------------------------------------------------
% 0.36/1.38 ncf(matrix, plain, [(188 ^ _26910) ^ [] : [-(subset(184 ^ [], 185 ^ []))], (190 ^ _26910) ^ [] : [-(intersection(185 ^ [], 186 ^ []) = empty_set)], (192 ^ _26910) ^ [] : [intersection(184 ^ [], 186 ^ []) = empty_set], (58 ^ _26910) ^ [_28859, _28861, _28863, _28865] : [-(intersection(_28865, _28861) = intersection(_28863, _28859)), _28865 = _28863, _28861 = _28859], (2 ^ _26910) ^ [_27054] : [-(_27054 = _27054)], (4 ^ _26910) ^ [_27161, _27163] : [_27163 = _27161, -(_27161 = _27163)], (10 ^ _26910) ^ [_27365, _27367, _27369] : [-(_27369 = _27365), _27369 = _27367, _27367 = _27365], (20 ^ _26910) ^ [_27678, _27680] : [-(empty(_27678)), _27680 = _27678, empty(_27680)], (30 ^ _26910) ^ [_28001, _28003, _28005, _28007] : [-(member(_28005, _28001)), member(_28007, _28003), _28007 = _28005, _28003 = _28001], (44 ^ _26910) ^ [_28425, _28427, _28429, _28431] : [-(subset(_28429, _28425)), subset(_28431, _28427), _28431 = _28429, _28427 = _28425], (68 ^ _26910) ^ [_29178] : [subset(_29178, empty_set), -(_29178 = empty_set)], (74 ^ _26910) ^ [_29396, _29398, _29400] : [subset(_29400, _29398), -(subset(intersection(_29400, _29396), intersection(_29398, _29396)))], (80 ^ _26910) ^ [_29594] : [member(_29594, empty_set)], (82 ^ _26910) ^ [_29744, _29746, _29748] : [member(_29744, intersection(_29748, _29746)), 85 ^ _26910 : [(86 ^ _26910) ^ [] : [-(member(_29744, _29748))], (88 ^ _26910) ^ [] : [-(member(_29744, _29746))]]], (90 ^ _26910) ^ [_29995, _29997, _29999] : [-(member(_29995, intersection(_29999, _29997))), member(_29995, _29999), member(_29995, _29997)], (110 ^ _26910) ^ [_30655, _30657] : [112 ^ _26910 : [(113 ^ _26910) ^ [] : [-(member(111 ^ [_30655, _30657], _30657))], (115 ^ _26910) ^ [] : [member(111 ^ [_30655, _30657], _30655)]], -(subset(_30657, _30655))], (100 ^ _26910) ^ [_30341, _30343] : [subset(_30343, _30341), 103 ^ _26910 : [(104 ^ _26910) ^ [_30478] : [member(_30478, _30343), -(member(_30478, _30341))]]], (119 ^ _26910) ^ [_31041, _31043] : [_31043 = _31041, 122 ^ _26910 : [(123 ^ _26910) ^ [] : [-(subset(_31043, _31041))], (125 ^ _26910) ^ [] : [-(subset(_31041, _31043))]]], (127 ^ _26910) ^ [_31278, _31280] : [-(_31280 = _31278), subset(_31280, _31278), subset(_31278, _31280)], (137 ^ _26910) ^ [_31564, _31566] : [-(intersection(_31566, _31564) = intersection(_31564, _31566))], (139 ^ _26910) ^ [_31650] : [-(subset(_31650, _31650))], (141 ^ _26910) ^ [_31772] : [empty(_31772), 144 ^ _26910 : [(145 ^ _26910) ^ [_31883] : [member(_31883, _31772)]]], (147 ^ _26910) ^ [_31949] : [-(member(148 ^ [_31949], _31949)), -(empty(_31949))], (170 ^ _26910) ^ [_32735, _32737] : [-(_32737 = _32735), 174 ^ _26910 : [(175 ^ _26910) ^ [] : [-(member(171 ^ [_32735, _32737], _32737))], (177 ^ _26910) ^ [] : [member(171 ^ [_32735, _32737], _32735)]], 178 ^ _26910 : [(179 ^ _26910) ^ [] : [-(member(171 ^ [_32735, _32737], _32735))], (181 ^ _26910) ^ [] : [member(171 ^ [_32735, _32737], _32737)]]], (154 ^ _26910) ^ [_32218, _32220] : [_32220 = _32218, 157 ^ _26910 : [(158 ^ _26910) ^ [_32384] : [member(_32384, _32220), -(member(_32384, _32218))], (164 ^ _26910) ^ [_32556] : [member(_32556, _32218), -(member(_32556, _32220))]]]], input).
% 0.36/1.38 ncf('1',plain,[empty(intersection(185 ^ [], 186 ^ [])), 145 : member(111 ^ [intersection(184 ^ [], 186 ^ []), intersection(185 ^ [], 186 ^ [])], intersection(185 ^ [], 186 ^ []))],start(141 ^ 0,bind([[_31772, _31883], [intersection(185 ^ [], 186 ^ []), 111 ^ [intersection(184 ^ [], 186 ^ []), intersection(185 ^ [], 186 ^ [])]]]))).
% 0.36/1.38 ncf('1.1',plain,[-(empty(intersection(185 ^ [], 186 ^ []))), -(member(148 ^ [intersection(185 ^ [], 186 ^ [])], intersection(185 ^ [], 186 ^ [])))],extension(147 ^ 1,bind([[_31949], [intersection(185 ^ [], 186 ^ [])]]))).
% 0.36/1.38 ncf('1.1.1',plain,[member(148 ^ [intersection(185 ^ [], 186 ^ [])], intersection(185 ^ [], 186 ^ [])), -(member(148 ^ [intersection(185 ^ [], 186 ^ [])], empty_set)), 148 ^ [intersection(185 ^ [], 186 ^ [])] = 148 ^ [intersection(185 ^ [], 186 ^ [])], intersection(185 ^ [], 186 ^ []) = empty_set],extension(30 ^ 2,bind([[_28001, _28003, _28005, _28007], [empty_set, intersection(185 ^ [], 186 ^ []), 148 ^ [intersection(185 ^ [], 186 ^ [])], 148 ^ [intersection(185 ^ [], 186 ^ [])]]]))).
% 0.36/1.38 ncf('1.1.1.1',plain,[member(148 ^ [intersection(185 ^ [], 186 ^ [])], empty_set)],extension(80 ^ 3,bind([[_29594], [148 ^ [intersection(185 ^ [], 186 ^ [])]]]))).
% 0.36/1.38 ncf('1.1.1.2',plain,[-(148 ^ [intersection(185 ^ [], 186 ^ [])] = 148 ^ [intersection(185 ^ [], 186 ^ [])])],extension(2 ^ 3,bind([[_27054], [148 ^ [intersection(185 ^ [], 186 ^ [])]]]))).
% 0.36/1.38 ncf('1.1.1.3',plain,[-(intersection(185 ^ [], 186 ^ []) = empty_set)],extension(190 ^ 3)).
% 0.36/1.38 ncf('1.2',plain,[-(member(111 ^ [intersection(184 ^ [], 186 ^ []), intersection(185 ^ [], 186 ^ [])], intersection(185 ^ [], 186 ^ []))), -(subset(intersection(185 ^ [], 186 ^ []), intersection(184 ^ [], 186 ^ [])))],extension(110 ^ 3,bind([[_30655, _30657], [intersection(184 ^ [], 186 ^ []), intersection(185 ^ [], 186 ^ [])]]))).
% 0.36/1.38 ncf('1.2.1',plain,[subset(intersection(185 ^ [], 186 ^ []), intersection(184 ^ [], 186 ^ [])), -(intersection(184 ^ [], 186 ^ []) = intersection(185 ^ [], 186 ^ [])), subset(intersection(184 ^ [], 186 ^ []), intersection(185 ^ [], 186 ^ []))],extension(127 ^ 4,bind([[_31278, _31280], [intersection(185 ^ [], 186 ^ []), intersection(184 ^ [], 186 ^ [])]]))).
% 0.36/1.38 ncf('1.2.1.1',plain,[intersection(184 ^ [], 186 ^ []) = intersection(185 ^ [], 186 ^ []), -(intersection(184 ^ [], 186 ^ []) = empty_set), intersection(185 ^ [], 186 ^ []) = empty_set],extension(10 ^ 5,bind([[_27365, _27367, _27369], [empty_set, intersection(185 ^ [], 186 ^ []), intersection(184 ^ [], 186 ^ [])]]))).
% 0.36/1.38 ncf('1.2.1.1.1',plain,[intersection(184 ^ [], 186 ^ []) = empty_set],extension(192 ^ 6)).
% 0.36/1.38 ncf('1.2.1.1.2',plain,[-(intersection(185 ^ [], 186 ^ []) = empty_set)],extension(190 ^ 6)).
% 0.36/1.38 ncf('1.2.1.2',plain,[-(subset(intersection(184 ^ [], 186 ^ []), intersection(185 ^ [], 186 ^ []))), subset(184 ^ [], 185 ^ [])],extension(74 ^ 5,bind([[_29396, _29398, _29400], [186 ^ [], 185 ^ [], 184 ^ []]]))).
% 0.36/1.38 ncf('1.2.1.2.1',plain,[-(subset(184 ^ [], 185 ^ []))],extension(188 ^ 6)).
% 0.36/1.38 %-----------------------------------------------------
% 0.36/1.38 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------