%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : SEU319+1 : TPTP v8.1.2. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n023.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:03:07 EDT 2023
% Result : Theorem 0.28s 1.36s
% Output : Proof 0.28s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.10 % Problem : SEU319+1 : TPTP v8.1.2. Released v3.3.0.
% 0.10/0.11 % Command : nanocop.sh %s %d
% 0.11/0.31 % Computer : n023.cluster.edu
% 0.11/0.31 % Model : x86_64 x86_64
% 0.11/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.31 % Memory : 8042.1875MB
% 0.11/0.31 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.31 % CPULimit : 300
% 0.11/0.31 % WCLimit : 300
% 0.11/0.31 % DateTime : Thu May 18 13:56:59 EDT 2023
% 0.11/0.32 % CPUTime :
% 0.28/1.36
% 0.28/1.36 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 0.28/1.36 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.28/1.36 %-----------------------------------------------------
% 0.28/1.36 ncf(matrix, plain, [(276 ^ _45365) ^ [] : [-(top_str(274 ^ []))], (279 ^ _45365) ^ [] : [-(element(277 ^ [], powerset(the_carrier(274 ^ []))))], (281 ^ _45365) ^ [] : [282 ^ _45365 : [(283 ^ _45365) ^ [] : [-(closed_subset(277 ^ [], 274 ^ []))], (285 ^ _45365) ^ [] : [open_subset(subset_complement(the_carrier(274 ^ []), 277 ^ []), 274 ^ [])]], 286 ^ _45365 : [(287 ^ _45365) ^ [] : [-(open_subset(subset_complement(the_carrier(274 ^ []), 277 ^ []), 274 ^ []))], (289 ^ _45365) ^ [] : [closed_subset(277 ^ [], 274 ^ [])]]], (148 ^ _45365) ^ [_50371] : [top_str(_50371), 151 ^ _45365 : [(152 ^ _45365) ^ [_50520] : [element(_50520, powerset(the_carrier(_50371))), 155 ^ _45365 : [(156 ^ _45365) ^ [] : [closed_subset(_50520, _50371), -(open_subset(subset_difference(the_carrier(_50371), cast_as_carrier_subset(_50371), _50520), _50371))], (162 ^ _45365) ^ [] : [open_subset(subset_difference(the_carrier(_50371), cast_as_carrier_subset(_50371), _50520), _50371), -(closed_subset(_50520, _50371))]]]]], (168 ^ _45365) ^ [] : [true___, -(true___)], (174 ^ _45365) ^ [_51124] : [one_sorted_str(_51124), -(element(cast_as_carrier_subset(_51124), powerset(the_carrier(_51124))))], (180 ^ _45365) ^ [_51338, _51340] : [element(_51338, powerset(_51340)), -(element(subset_complement(_51340, _51338), powerset(_51340)))], (186 ^ _45365) ^ [] : [true___, -(true___)], (192 ^ _45365) ^ [_51695, _51697, _51699] : [-(element(subset_difference(_51699, _51697, _51695), powerset(_51699))), element(_51697, powerset(_51699)), element(_51695, powerset(_51699))], (202 ^ _45365) ^ [_52010] : [top_str(_52010), -(one_sorted_str(_52010))], (208 ^ _45365) ^ [] : [true___, -(true___)], (214 ^ _45365) ^ [] : [true___, -(true___)], (220 ^ _45365) ^ [] : [true___, -(true___)], (227 ^ _45365) ^ [] : [-(top_str(225 ^ []))], (230 ^ _45365) ^ [] : [-(one_sorted_str(228 ^ []))], (233 ^ _45365) ^ [_52755] : [-(element(231 ^ [_52755], _52755))], (235 ^ _45365) ^ [_52867, _52869] : [element(_52867, powerset(_52869)), -(subset_complement(_52869, subset_complement(_52869, _52867)) = _52867)], (241 ^ _45365) ^ [_53107, _53109, _53111] : [-(subset_difference(_53111, _53109, _53107) = set_difference(_53109, _53107)), element(_53109, powerset(_53111)), element(_53107, powerset(_53111))], (251 ^ _45365) ^ [_53423, _53425] : [-(subset(_53425, _53425))], (253 ^ _45365) ^ [_53518] : [one_sorted_str(_53518), 256 ^ _45365 : [(257 ^ _45365) ^ [_53666] : [element(_53666, powerset(the_carrier(_53518))), -(subset_complement(the_carrier(_53518), _53666) = subset_difference(the_carrier(_53518), cast_as_carrier_subset(_53518), _53666))]]], (263 ^ _45365) ^ [_53926, _53928] : [element(_53928, powerset(_53926)), -(subset(_53928, _53926))], (269 ^ _45365) ^ [_54092, _54094] : [subset(_54094, _54092), -(element(_54094, powerset(_54092)))], (96 ^ _45365) ^ [_48523, _48525, _48527, _48529] : [-(set_difference(_48529, _48525) = set_difference(_48527, _48523)), _48529 = _48527, _48525 = _48523], (106 ^ _45365) ^ [_48910, _48912, _48914, _48916, _48918, _48920] : [-(subset_difference(_48920, _48916, _48912) = subset_difference(_48918, _48914, _48910)), _48920 = _48918, _48916 = _48914, _48912 = _48910], (120 ^ _45365) ^ [_49370, _49372] : [_49372 = _49370, -(cast_as_carrier_subset(_49372) = cast_as_carrier_subset(_49370))], (126 ^ _45365) ^ [_49588, _49590] : [_49590 = _49588, -(powerset(_49590) = powerset(_49588))], (142 ^ _45365) ^ [_50145, _50147] : [_50147 = _50145, -(the_carrier(_50147) = the_carrier(_50145))], (132 ^ _45365) ^ [_49834, _49836, _49838, _49840] : [-(subset_complement(_49840, _49836) = subset_complement(_49838, _49834)), _49840 = _49838, _49836 = _49834], (2 ^ _45365) ^ [_45509] : [-(_45509 = _45509)], (4 ^ _45365) ^ [_45616, _45618] : [_45618 = _45616, -(_45616 = _45618)], (10 ^ _45365) ^ [_45820, _45822, _45824] : [-(_45824 = _45820), _45824 = _45822, _45822 = _45820], (20 ^ _45365) ^ [_46133, _46135] : [-(one_sorted_str(_46133)), _46135 = _46133, one_sorted_str(_46135)], (30 ^ _45365) ^ [_46456, _46458, _46460, _46462] : [-(subset(_46460, _46456)), subset(_46462, _46458), _46462 = _46460, _46458 = _46456], (44 ^ _45365) ^ [_46872, _46874] : [-(top_str(_46872)), _46874 = _46872, top_str(_46874)], (54 ^ _45365) ^ [_47195, _47197, _47199, _47201] : [-(element(_47199, _47195)), element(_47201, _47197), _47201 = _47199, _47197 = _47195], (68 ^ _45365) ^ [_47639, _47641, _47643, _47645] : [-(closed_subset(_47643, _47639)), closed_subset(_47645, _47641), _47645 = _47643, _47641 = _47639], (82 ^ _45365) ^ [_48063, _48065, _48067, _48069] : [-(open_subset(_48067, _48063)), open_subset(_48069, _48065), _48069 = _48067, _48065 = _48063]], input).
% 0.28/1.36 ncf('1',plain,[285 : open_subset(subset_complement(the_carrier(274 ^ []), 277 ^ []), 274 ^ []), 289 : closed_subset(277 ^ [], 274 ^ [])],start(281 ^ 0)).
% 0.28/1.36 ncf('1.1',plain,[-(open_subset(subset_complement(the_carrier(274 ^ []), 277 ^ []), 274 ^ [])), open_subset(subset_difference(the_carrier(274 ^ []), cast_as_carrier_subset(274 ^ []), 277 ^ []), 274 ^ []), subset_difference(the_carrier(274 ^ []), cast_as_carrier_subset(274 ^ []), 277 ^ []) = subset_complement(the_carrier(274 ^ []), 277 ^ []), 274 ^ [] = 274 ^ []],extension(82 ^ 3,bind([[_48063, _48065, _48067, _48069], [274 ^ [], 274 ^ [], subset_complement(the_carrier(274 ^ []), 277 ^ []), subset_difference(the_carrier(274 ^ []), cast_as_carrier_subset(274 ^ []), 277 ^ [])]]))).
% 0.28/1.36 ncf('1.1.1',plain,[-(open_subset(subset_difference(the_carrier(274 ^ []), cast_as_carrier_subset(274 ^ []), 277 ^ []), 274 ^ [])), 156 : closed_subset(277 ^ [], 274 ^ []), 156 : element(277 ^ [], powerset(the_carrier(274 ^ []))), 152 : top_str(274 ^ [])],extension(148 ^ 4,bind([[_50371, _50520], [274 ^ [], 277 ^ []]]))).
% 0.28/1.36 ncf('1.1.1.1',plain,[-(closed_subset(277 ^ [], 274 ^ []))],extension(283 ^ 9)).
% 0.28/1.36 ncf('1.1.1.2',plain,[-(element(277 ^ [], powerset(the_carrier(274 ^ []))))],extension(279 ^ 7)).
% 0.28/1.36 ncf('1.1.1.3',plain,[-(top_str(274 ^ []))],extension(276 ^ 5)).
% 0.28/1.36 ncf('1.1.2',plain,[-(subset_difference(the_carrier(274 ^ []), cast_as_carrier_subset(274 ^ []), 277 ^ []) = subset_complement(the_carrier(274 ^ []), 277 ^ [])), subset_complement(the_carrier(274 ^ []), 277 ^ []) = subset_difference(the_carrier(274 ^ []), cast_as_carrier_subset(274 ^ []), 277 ^ [])],extension(4 ^ 4,bind([[_45616, _45618], [subset_difference(the_carrier(274 ^ []), cast_as_carrier_subset(274 ^ []), 277 ^ []), subset_complement(the_carrier(274 ^ []), 277 ^ [])]]))).
% 0.28/1.36 ncf('1.1.2.1',plain,[-(subset_complement(the_carrier(274 ^ []), 277 ^ []) = subset_difference(the_carrier(274 ^ []), cast_as_carrier_subset(274 ^ []), 277 ^ [])), 257 : element(277 ^ [], powerset(the_carrier(274 ^ []))), 257 : one_sorted_str(274 ^ [])],extension(253 ^ 5,bind([[_53518, _53666], [274 ^ [], 277 ^ []]]))).
% 0.28/1.36 ncf('1.1.2.1.1',plain,[-(element(277 ^ [], powerset(the_carrier(274 ^ []))))],extension(279 ^ 8)).
% 0.28/1.36 ncf('1.1.2.1.2',plain,[-(one_sorted_str(274 ^ [])), top_str(274 ^ [])],extension(202 ^ 6,bind([[_52010], [274 ^ []]]))).
% 0.28/1.36 ncf('1.1.2.1.2.1',plain,[-(top_str(274 ^ []))],extension(276 ^ 7)).
% 0.28/1.36 ncf('1.1.3',plain,[-(274 ^ [] = 274 ^ [])],extension(2 ^ 4,bind([[_45509], [274 ^ []]]))).
% 0.28/1.36 ncf('1.2',plain,[-(closed_subset(277 ^ [], 274 ^ [])), 162 : open_subset(subset_difference(the_carrier(274 ^ []), cast_as_carrier_subset(274 ^ []), 277 ^ []), 274 ^ []), 162 : element(277 ^ [], powerset(the_carrier(274 ^ []))), 152 : top_str(274 ^ [])],extension(148 ^ 3,bind([[_50371, _50520], [274 ^ [], 277 ^ []]]))).
% 0.28/1.36 ncf('1.2.1',plain,[-(open_subset(subset_difference(the_carrier(274 ^ []), cast_as_carrier_subset(274 ^ []), 277 ^ []), 274 ^ [])), open_subset(subset_complement(the_carrier(274 ^ []), 277 ^ []), 274 ^ []), subset_complement(the_carrier(274 ^ []), 277 ^ []) = subset_difference(the_carrier(274 ^ []), cast_as_carrier_subset(274 ^ []), 277 ^ []), 274 ^ [] = 274 ^ []],extension(82 ^ 8,bind([[_48063, _48065, _48067, _48069], [274 ^ [], 274 ^ [], subset_difference(the_carrier(274 ^ []), cast_as_carrier_subset(274 ^ []), 277 ^ []), subset_complement(the_carrier(274 ^ []), 277 ^ [])]]))).
% 0.28/1.36 ncf('1.2.1.1',plain,[-(open_subset(subset_complement(the_carrier(274 ^ []), 277 ^ []), 274 ^ []))],extension(287 ^ 9)).
% 0.28/1.36 ncf('1.2.1.2',plain,[-(subset_complement(the_carrier(274 ^ []), 277 ^ []) = subset_difference(the_carrier(274 ^ []), cast_as_carrier_subset(274 ^ []), 277 ^ [])), 257 : element(277 ^ [], powerset(the_carrier(274 ^ []))), 257 : one_sorted_str(274 ^ [])],extension(253 ^ 9,bind([[_53518, _53666], [274 ^ [], 277 ^ []]]))).
% 0.28/1.36 ncf('1.2.1.2.1',plain,[-(element(277 ^ [], powerset(the_carrier(274 ^ []))))],extension(279 ^ 12)).
% 0.28/1.36 ncf('1.2.1.2.2',plain,[-(one_sorted_str(274 ^ [])), top_str(274 ^ [])],extension(202 ^ 10,bind([[_52010], [274 ^ []]]))).
% 0.28/1.36 ncf('1.2.1.2.2.1',plain,[-(top_str(274 ^ []))],extension(276 ^ 11)).
% 0.28/1.36 ncf('1.2.1.3',plain,[-(274 ^ [] = 274 ^ [])],extension(2 ^ 9,bind([[_45509], [274 ^ []]]))).
% 0.28/1.36 ncf('1.2.2',plain,[-(element(277 ^ [], powerset(the_carrier(274 ^ []))))],extension(279 ^ 6)).
% 0.28/1.36 ncf('1.2.3',plain,[-(top_str(274 ^ []))],extension(276 ^ 4)).
% 0.28/1.36 %-----------------------------------------------------
% 0.28/1.36 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------