%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : SEU131+1 : 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:18 EDT 2023
% Result : Theorem 43.47s 42.85s
% Output : Proof 43.47s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SEU131+1 : TPTP v8.1.2. Released v3.3.0.
% 0.00/0.12 % Command : nanocop.sh %s %d
% 0.12/0.33 % Computer : n019.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 12:53:42 EDT 2023
% 0.12/0.33 % CPUTime :
% 43.47/42.85
% 43.47/42.85 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 43.47/42.85 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 43.47/42.85 %-----------------------------------------------------
% 43.47/42.85 ncf(matrix, plain, [(201 ^ _40047) ^ [] : [202 ^ _40047 : [(205 ^ _40047) ^ [] : [subset(198 ^ [], 199 ^ [])], (203 ^ _40047) ^ [] : [-(set_difference(198 ^ [], 199 ^ []) = empty_set)]], 206 ^ _40047 : [(209 ^ _40047) ^ [] : [set_difference(198 ^ [], 199 ^ []) = empty_set], (207 ^ _40047) ^ [] : [-(subset(198 ^ [], 199 ^ []))]]], !, (93 ^ _33356) ^ [_36572, _36574, _36576] : [_36572 = set_difference(_36576, _36574), 96 ^ _33356 : [(105 ^ _33356) ^ [_37016] : [-(in(_37016, _36572)), in(_37016, _36576), -(in(_37016, _36574))], (97 ^ _33356) ^ [_36756] : [in(_36756, _36572), 100 ^ _33356 : [(103 ^ _33356) ^ [] : [in(_36756, _36574)], (101 ^ _33356) ^ [] : [-(in(_36756, _36576))]]]]], (58 ^ _33356) ^ [_35285, _35287, _35289, _35291] : [-(set_difference(_35291, _35287) = set_difference(_35289, _35285)), _35291 = _35289, _35287 = _35285], (44 ^ _33356) ^ [_34851, _34853, _34855, _34857] : [-(subset(_34855, _34851)), subset(_34857, _34853), _34857 = _34855, _34853 = _34851], (173 ^ _33356) ^ [_39125] : [-(set_difference(_39125, empty_set) = _39125)], (175 ^ _33356) ^ [_39206] : [-(set_difference(empty_set, _39206) = empty_set)], (68 ^ _33356) ^ [_35618, _35620] : [in(_35620, _35618), in(_35618, _35620)], (34 ^ _33356) ^ [_34548, _34550] : [-(empty(_34548)), _34550 = _34548, empty(_34550)], (136 ^ _33356) ^ [] : [true___, -(true___)], (115 ^ _33356) ^ [_37303, _37305, _37307] : [-(_37303 = set_difference(_37307, _37305)), 127 ^ _33356 : [(132 ^ _33356) ^ [] : [in(116 ^ [_37303, _37305, _37307], _37303)], (130 ^ _33356) ^ [] : [in(116 ^ [_37303, _37305, _37307], _37305)], (128 ^ _33356) ^ [] : [-(in(116 ^ [_37303, _37305, _37307], _37307))]], 119 ^ _33356 : [(122 ^ _33356) ^ [] : [in(116 ^ [_37303, _37305, _37307], _37307), -(in(116 ^ [_37303, _37305, _37307], _37305))], (120 ^ _33356) ^ [] : [-(in(116 ^ [_37303, _37305, _37307], _37303))]]], (177 ^ _33356) ^ [_39302] : [empty(_39302), -(_39302 = empty_set)], (154 ^ _33356) ^ [] : [empty(152 ^ [])], (2 ^ _33356) ^ [_33480] : [-(_33480 = _33480)], (84 ^ _33356) ^ [_36172, _36174] : [86 ^ _33356 : [(89 ^ _33356) ^ [] : [in(85 ^ [_36172, _36174], _36172)], (87 ^ _33356) ^ [] : [-(in(85 ^ [_36172, _36174], _36174))]], -(subset(_36174, _36172))], (189 ^ _33356) ^ [_39691, _39693] : [empty(_39693), -(_39693 = _39691), empty(_39691)], (148 ^ _33356) ^ [] : [-(empty(empty_set))], (20 ^ _33356) ^ [_34132, _34134, _34136, _34138] : [-(in(_34136, _34132)), in(_34138, _34134), _34138 = _34136, _34134 = _34132], (4 ^ _33356) ^ [_33587, _33589] : [_33589 = _33587, -(_33587 = _33589)], (74 ^ _33356) ^ [_35858, _35860] : [subset(_35860, _35858), 77 ^ _33356 : [(78 ^ _33356) ^ [_35995] : [in(_35995, _35860), -(in(_35995, _35858))]]], (158 ^ _33356) ^ [_38624, _38626] : [-(_38626 = _38624), 162 ^ _33356 : [(165 ^ _33356) ^ [] : [in(159 ^ [_38624, _38626], _38624)], (163 ^ _33356) ^ [] : [-(in(159 ^ [_38624, _38626], _38626))]], 166 ^ _33356 : [(169 ^ _33356) ^ [] : [in(159 ^ [_38624, _38626], _38626)], (167 ^ _33356) ^ [] : [-(in(159 ^ [_38624, _38626], _38624))]]], (142 ^ _33356) ^ [] : [true___, -(true___)], (183 ^ _33356) ^ [_39504, _39506] : [in(_39506, _39504), empty(_39504)], (156 ^ _33356) ^ [_38515, _38517] : [-(subset(_38517, _38517))], (10 ^ _33356) ^ [_33791, _33793, _33795] : [-(_33795 = _33791), _33795 = _33793, _33793 = _33791], (151 ^ _33356) ^ [] : [-(empty(149 ^ []))]], input).
% 43.47/42.85 ncf('1',plain,[203 : -(set_difference(198 ^ [], 199 ^ []) = empty_set), 209 : set_difference(198 ^ [], 199 ^ []) = empty_set],start(201 ^ 0)).
% 43.47/42.85 ncf('1.1',plain,[set_difference(198 ^ [], 199 ^ []) = empty_set, -(empty_set = set_difference(198 ^ [], 199 ^ []))],extension(4 ^ 3,bind([[_33587, _33589], [empty_set, set_difference(198 ^ [], 199 ^ [])]]))).
% 43.47/42.85 ncf('1.1.1',plain,[empty_set = set_difference(198 ^ [], 199 ^ []), 97 : in(85 ^ [199 ^ [], 198 ^ []], empty_set), 103 : in(85 ^ [199 ^ [], 198 ^ []], 199 ^ [])],extension(93 ^ 4,bind([[_36572, _36574, _36576, _36756], [empty_set, 199 ^ [], 198 ^ [], 85 ^ [199 ^ [], 198 ^ []]]]))).
% 43.47/42.85 ncf('1.1.1.1',plain,[-(in(85 ^ [199 ^ [], 198 ^ []], empty_set)), in(85 ^ [199 ^ [], 198 ^ []], 198 ^ []), -(in(85 ^ [199 ^ [], 198 ^ []], 199 ^ []))],extension(105 ^ 7,bind([[_37016], [85 ^ [199 ^ [], 198 ^ []]]]))).
% 43.47/42.85 ncf('1.1.1.1.1',plain,[-(in(85 ^ [199 ^ [], 198 ^ []], 198 ^ [])), -(subset(198 ^ [], 199 ^ []))],extension(84 ^ 8,bind([[_36172, _36174], [199 ^ [], 198 ^ []]]))).
% 43.47/42.85 ncf('1.1.1.1.1.1',plain,[subset(198 ^ [], 199 ^ [])],extension(205 ^ 9)).
% 43.47/42.85 ncf('1.1.1.1.2',plain,[in(85 ^ [199 ^ [], 198 ^ []], 199 ^ []), -(subset(198 ^ [], 199 ^ []))],extension(84 ^ 8,bind([[_36172, _36174], [199 ^ [], 198 ^ []]]))).
% 43.47/42.85 ncf('1.1.1.1.2.1',plain,[subset(198 ^ [], 199 ^ [])],extension(205 ^ 9)).
% 43.47/42.85 ncf('1.1.1.2',plain,[-(in(85 ^ [199 ^ [], 198 ^ []], 199 ^ [])), -(in(85 ^ [199 ^ [], 198 ^ []], empty_set)), in(85 ^ [199 ^ [], 198 ^ []], 198 ^ [])],extension(105 ^ 9,bind([[_37016], [85 ^ [199 ^ [], 198 ^ []]]]))).
% 43.47/42.85 ncf('1.1.1.2.1',plain,[in(85 ^ [199 ^ [], 198 ^ []], empty_set), empty(empty_set)],extension(183 ^ 10,bind([[_39504, _39506], [empty_set, 85 ^ [199 ^ [], 198 ^ []]]]))).
% 43.47/42.85 ncf('1.1.1.2.1.1',plain,[-(empty(empty_set))],extension(148 ^ 11)).
% 43.47/42.85 ncf('1.1.1.2.2',plain,[-(in(85 ^ [199 ^ [], 198 ^ []], 198 ^ []))],extension(101 ^ 10)).
% 43.47/42.85 ncf('1.2',plain,[-(set_difference(198 ^ [], 199 ^ []) = empty_set), empty_set = set_difference(198 ^ [], 199 ^ [])],extension(4 ^ 3,bind([[_33587, _33589], [set_difference(198 ^ [], 199 ^ []), empty_set]]))).
% 43.47/42.85 ncf('1.2.1',plain,[-(empty_set = set_difference(198 ^ [], 199 ^ [])), 130 : in(116 ^ [empty_set, 199 ^ [], 198 ^ []], 199 ^ []), 120 : -(in(116 ^ [empty_set, 199 ^ [], 198 ^ []], empty_set))],extension(115 ^ 4,bind([[_37303, _37305, _37307], [empty_set, 199 ^ [], 198 ^ []]]))).
% 43.47/42.85 ncf('1.2.1.1',plain,[-(in(116 ^ [empty_set, 199 ^ [], 198 ^ []], 199 ^ [])), 78 : in(116 ^ [empty_set, 199 ^ [], 198 ^ []], 198 ^ []), 78 : subset(198 ^ [], 199 ^ [])],extension(74 ^ 7,bind([[_35858, _35860, _35995], [199 ^ [], 198 ^ [], 116 ^ [empty_set, 199 ^ [], 198 ^ []]]]))).
% 43.47/42.85 ncf('1.2.1.1.1',plain,[-(in(116 ^ [empty_set, 199 ^ [], 198 ^ []], 198 ^ []))],extension(128 ^ 10)).
% 43.47/42.85 ncf('1.2.1.1.2',plain,[-(subset(198 ^ [], 199 ^ []))],extension(207 ^ 8)).
% 43.47/42.85 ncf('1.2.1.2',plain,[in(116 ^ [empty_set, 199 ^ [], 198 ^ []], empty_set), empty(empty_set)],extension(183 ^ 7,bind([[_39504, _39506], [empty_set, 116 ^ [empty_set, 199 ^ [], 198 ^ []]]]))).
% 43.47/42.85 ncf('1.2.1.2.1',plain,[-(empty(empty_set))],extension(148 ^ 8)).
% 43.47/42.85 %-----------------------------------------------------
% 43.47/42.85 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------