%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : SEU122+2 : TPTP v8.1.2. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n019.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:15 EDT 2023
% Result : Theorem 0.29s 1.36s
% Output : Proof 0.29s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : SEU122+2 : TPTP v8.1.2. Released v3.3.0.
% 0.11/0.13 % Command : nanocop.sh %s %d
% 0.12/0.32 % Computer : n019.cluster.edu
% 0.12/0.32 % Model : x86_64 x86_64
% 0.12/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.32 % Memory : 8042.1875MB
% 0.12/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.32 % CPULimit : 300
% 0.12/0.32 % WCLimit : 300
% 0.12/0.32 % DateTime : Thu May 18 13:42:27 EDT 2023
% 0.12/0.32 % CPUTime :
% 0.29/1.36
% 0.29/1.36 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 0.29/1.36 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.29/1.36 %-----------------------------------------------------
% 0.29/1.36 ncf(matrix, plain, [(272 ^ _37131) ^ [] : [subset(empty_set, 270 ^ [])], (72 ^ _37131) ^ [_39526, _39528, _39530, _39532] : [-(set_intersection2(_39532, _39528) = set_intersection2(_39530, _39526)), _39532 = _39530, _39528 = _39526], (2 ^ _37131) ^ [_37275] : [-(_37275 = _37275)], (4 ^ _37131) ^ [_37382, _37384] : [_37384 = _37382, -(_37382 = _37384)], (10 ^ _37131) ^ [_37586, _37588, _37590] : [-(_37590 = _37586), _37590 = _37588, _37588 = _37586], (20 ^ _37131) ^ [_37927, _37929, _37931, _37933] : [-(disjoint(_37931, _37927)), disjoint(_37933, _37929), _37933 = _37931, _37929 = _37927], (34 ^ _37131) ^ [_38371, _38373, _38375, _38377] : [-(in(_38375, _38371)), in(_38377, _38373), _38377 = _38375, _38373 = _38371], (48 ^ _37131) ^ [_38787, _38789] : [-(empty(_38787)), _38789 = _38787, empty(_38789)], (58 ^ _37131) ^ [_39090, _39092, _39094, _39096] : [-(subset(_39094, _39090)), subset(_39096, _39092), _39096 = _39094, _39092 = _39090], (82 ^ _37131) ^ [_39859, _39861] : [in(_39861, _39859), in(_39859, _39861)], (88 ^ _37131) ^ [_40055, _40057] : [-(set_intersection2(_40057, _40055) = set_intersection2(_40055, _40057))], (90 ^ _37131) ^ [_40185] : [_40185 = empty_set, 93 ^ _37131 : [(94 ^ _37131) ^ [_40298] : [in(_40298, _40185)]]], (96 ^ _37131) ^ [_40364] : [-(in(97 ^ [_40364], _40364)), -(_40364 = empty_set)], (113 ^ _37131) ^ [_40969, _40971] : [115 ^ _37131 : [(116 ^ _37131) ^ [] : [-(in(114 ^ [_40969, _40971], _40971))], (118 ^ _37131) ^ [] : [in(114 ^ [_40969, _40971], _40969)]], -(subset(_40971, _40969))], (103 ^ _37131) ^ [_40655, _40657] : [subset(_40657, _40655), 106 ^ _37131 : [(107 ^ _37131) ^ [_40792] : [in(_40792, _40657), -(in(_40792, _40655))]]], (144 ^ _37131) ^ [_42094, _42096, _42098] : [-(_42094 = set_intersection2(_42098, _42096)), 156 ^ _37131 : [(157 ^ _37131) ^ [] : [-(in(145 ^ [_42094, _42096, _42098], _42098))], (159 ^ _37131) ^ [] : [-(in(145 ^ [_42094, _42096, _42098], _42096))], (161 ^ _37131) ^ [] : [in(145 ^ [_42094, _42096, _42098], _42094)]], 148 ^ _37131 : [(149 ^ _37131) ^ [] : [-(in(145 ^ [_42094, _42096, _42098], _42094))], (151 ^ _37131) ^ [] : [in(145 ^ [_42094, _42096, _42098], _42098), in(145 ^ [_42094, _42096, _42098], _42096)]]], (122 ^ _37131) ^ [_41369, _41371, _41373] : [_41369 = set_intersection2(_41373, _41371), 125 ^ _37131 : [(126 ^ _37131) ^ [_41551] : [in(_41551, _41369), 129 ^ _37131 : [(130 ^ _37131) ^ [] : [-(in(_41551, _41373))], (132 ^ _37131) ^ [] : [-(in(_41551, _41371))]]], (134 ^ _37131) ^ [_41810] : [-(in(_41810, _41369)), in(_41810, _41373), in(_41810, _41371)]]], (165 ^ _37131) ^ [_42876, _42878] : [disjoint(_42878, _42876), -(set_intersection2(_42878, _42876) = empty_set)], (171 ^ _37131) ^ [_43044, _43046] : [set_intersection2(_43046, _43044) = empty_set, -(disjoint(_43046, _43044))], (177 ^ _37131) ^ [] : [true___, -(true___)], (183 ^ _37131) ^ [] : [true___, -(true___)], (189 ^ _37131) ^ [] : [-(empty(empty_set))], (191 ^ _37131) ^ [_43538, _43540] : [-(set_intersection2(_43540, _43540) = _43540)], (194 ^ _37131) ^ [] : [-(empty(192 ^ []))], (197 ^ _37131) ^ [] : [empty(195 ^ [])], (199 ^ _37131) ^ [_43814, _43816] : [-(subset(_43816, _43816))], (201 ^ _37131) ^ [_43923, _43925] : [disjoint(_43925, _43923), -(disjoint(_43923, _43925))], (207 ^ _37131) ^ [_44147, _44149, _44151] : [-(subset(_44151, _44147)), subset(_44151, _44149), subset(_44149, _44147)], (217 ^ _37131) ^ [_44476, _44478] : [-(disjoint(_44478, _44476)), 221 ^ _37131 : [(222 ^ _37131) ^ [] : [-(in(220 ^ [_44476, _44478], _44478))], (224 ^ _37131) ^ [] : [-(in(220 ^ [_44476, _44478], _44476))]]], (226 ^ _37131) ^ [_44790, _44792] : [disjoint(_44792, _44790), 227 ^ _37131 : [(228 ^ _37131) ^ [_44882] : [in(_44882, _44792), in(_44882, _44790)]]], (236 ^ _37131) ^ [_45173, _45175] : [-(disjoint(_45175, _45173)), -(in(239 ^ [_45173, _45175], set_intersection2(_45175, _45173)))], (243 ^ _37131) ^ [_45408, _45410] : [244 ^ _37131 : [(245 ^ _37131) ^ [_45481] : [in(_45481, set_intersection2(_45410, _45408))]], disjoint(_45410, _45408)], (249 ^ _37131) ^ [_45633] : [empty(_45633), -(_45633 = empty_set)], (255 ^ _37131) ^ [_45835, _45837] : [in(_45837, _45835), empty(_45835)], (261 ^ _37131) ^ [_46022, _46024] : [empty(_46024), -(_46024 = _46022), empty(_46022)]], input).
% 0.29/1.36 ncf('1',plain,[empty_set = empty_set, 94 : in(114 ^ [270 ^ [], empty_set], empty_set)],start(90 ^ 0,bind([[_40185, _40298], [empty_set, 114 ^ [270 ^ [], empty_set]]]))).
% 0.29/1.36 ncf('1.1',plain,[-(empty_set = empty_set)],extension(2 ^ 1,bind([[_37275], [empty_set]]))).
% 0.29/1.36 ncf('1.2',plain,[-(in(114 ^ [270 ^ [], empty_set], empty_set)), -(subset(empty_set, 270 ^ []))],extension(113 ^ 3,bind([[_40969, _40971], [270 ^ [], empty_set]]))).
% 0.29/1.36 ncf('1.2.1',plain,[subset(empty_set, 270 ^ [])],extension(272 ^ 4)).
% 0.29/1.36 %-----------------------------------------------------
% 0.29/1.36 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------