%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : SEU141+1 : TPTP v8.1.2. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n011.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:20 EDT 2023
% Result : Theorem 60.85s 59.38s
% Output : Proof 60.85s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SEU141+1 : TPTP v8.1.2. Released v3.3.0.
% 0.00/0.13 % Command : nanocop.sh %s %d
% 0.12/0.34 % Computer : n011.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 300
% 0.12/0.34 % DateTime : Thu May 18 12:46:32 EDT 2023
% 0.12/0.34 % CPUTime :
% 60.85/59.38
% 60.85/59.38 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 60.85/59.38 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 60.85/59.38 %-----------------------------------------------------
% 60.85/59.38 ncf(matrix, plain, [(314 ^ _63138) ^ [] : [315 ^ _63138 : [(318 ^ _63138) ^ [] : [set_difference(311 ^ [], 312 ^ []) = 311 ^ []], (316 ^ _63138) ^ [] : [-(disjoint(311 ^ [], 312 ^ []))]], 319 ^ _63138 : [(322 ^ _63138) ^ [] : [disjoint(311 ^ [], 312 ^ [])], (320 ^ _63138) ^ [] : [-(set_difference(311 ^ [], 312 ^ []) = 311 ^ [])]]], !, (128 ^ _52504) ^ [_56796, _56798] : [130 ^ _52504 : [(133 ^ _52504) ^ [] : [in(129 ^ [_56796, _56798], _56796)], (131 ^ _52504) ^ [] : [-(in(129 ^ [_56796, _56798], _56798))]], -(subset(_56798, _56796))], (72 ^ _52504) ^ [_54899, _54901, _54903, _54905] : [-(set_intersection2(_54905, _54901) = set_intersection2(_54903, _54899)), _54905 = _54903, _54901 = _54899], (263 ^ _52504) ^ [_61291, _61293] : [-(subset(_61293, _61293))], (277 ^ _52504) ^ [_61873, _61875] : [-(disjoint(_61875, _61873)), -(in(280 ^ [_61873, _61875], set_intersection2(_61875, _61873)))], (100 ^ _52504) ^ [_55915, _55917] : [_55917 = _55915, 103 ^ _52504 : [(106 ^ _52504) ^ [] : [-(subset(_55915, _55917))], (104 ^ _52504) ^ [] : [-(subset(_55917, _55915))]]], (34 ^ _52504) ^ [_53724, _53726, _53728, _53730] : [-(in(_53728, _53724)), in(_53730, _53726), _53730 = _53728, _53726 = _53724], (118 ^ _52504) ^ [_56482, _56484] : [subset(_56484, _56482), 121 ^ _52504 : [(122 ^ _52504) ^ [_56619] : [in(_56619, _56484), -(in(_56619, _56482))]]], (261 ^ _52504) ^ [] : [empty(259 ^ [])], (265 ^ _52504) ^ [_61400, _61402] : [disjoint(_61402, _61400), -(disjoint(_61400, _61402))], (273 ^ _52504) ^ [_61662] : [-(set_difference(_61662, empty_set) = _61662)], (284 ^ _52504) ^ [_62108, _62110] : [285 ^ _52504 : [(286 ^ _52504) ^ [_62181] : [in(_62181, set_intersection2(_62110, _62108))]], disjoint(_62110, _62108)], (271 ^ _52504) ^ [_61581] : [-(set_intersection2(_61581, empty_set) = empty_set)], (180 ^ _52504) ^ [_58717, _58719, _58721] : [_58717 = set_difference(_58721, _58719), 183 ^ _52504 : [(192 ^ _52504) ^ [_59161] : [-(in(_59161, _58717)), in(_59161, _58721), -(in(_59161, _58719))], (184 ^ _52504) ^ [_58901] : [in(_58901, _58717), 187 ^ _52504 : [(190 ^ _52504) ^ [] : [in(_58901, _58719)], (188 ^ _52504) ^ [] : [-(in(_58901, _58721))]]]]], (258 ^ _52504) ^ [] : [-(empty(256 ^ []))], (253 ^ _52504) ^ [] : [-(empty(empty_set))], (275 ^ _52504) ^ [_61743] : [-(set_difference(empty_set, _61743) = empty_set)], (290 ^ _52504) ^ [_62333] : [empty(_62333), -(_62333 = empty_set)], (82 ^ _52504) ^ [_55238, _55240, _55242, _55244] : [-(set_difference(_55244, _55240) = set_difference(_55242, _55238)), _55244 = _55242, _55240 = _55238], (137 ^ _52504) ^ [_57196, _57198, _57200] : [_57196 = set_intersection2(_57200, _57198), 140 ^ _52504 : [(149 ^ _52504) ^ [_57637] : [-(in(_57637, _57196)), in(_57637, _57200), in(_57637, _57198)], (141 ^ _52504) ^ [_57378] : [in(_57378, _57196), 144 ^ _52504 : [(147 ^ _52504) ^ [] : [-(in(_57378, _57198))], (145 ^ _52504) ^ [] : [-(in(_57378, _57200))]]]]], (296 ^ _52504) ^ [_62535, _62537] : [in(_62537, _62535), empty(_62535)], (48 ^ _52504) ^ [_54140, _54142] : [-(empty(_54140)), _54142 = _54140, empty(_54142)], (302 ^ _52504) ^ [_62722, _62724] : [empty(_62724), -(_62724 = _62722), empty(_62722)], (229 ^ _52504) ^ [_60402, _60404] : [set_intersection2(_60404, _60402) = empty_set, -(disjoint(_60404, _60402))], (98 ^ _52504) ^ [_55771, _55773] : [-(set_intersection2(_55773, _55771) = set_intersection2(_55771, _55773))], (10 ^ _52504) ^ [_52939, _52941, _52943] : [-(_52943 = _52939), _52943 = _52941, _52941 = _52939], (255 ^ _52504) ^ [_61015, _61017] : [-(set_intersection2(_61017, _61017) = _61017)], (223 ^ _52504) ^ [_60234, _60236] : [disjoint(_60236, _60234), -(set_intersection2(_60236, _60234) = empty_set)], (241 ^ _52504) ^ [] : [true___, -(true___)], (159 ^ _52504) ^ [_57921, _57923, _57925] : [-(_57921 = set_intersection2(_57925, _57923)), 171 ^ _52504 : [(176 ^ _52504) ^ [] : [in(160 ^ [_57921, _57923, _57925], _57921)], (174 ^ _52504) ^ [] : [-(in(160 ^ [_57921, _57923, _57925], _57923))], (172 ^ _52504) ^ [] : [-(in(160 ^ [_57921, _57923, _57925], _57925))]], 163 ^ _52504 : [(166 ^ _52504) ^ [] : [in(160 ^ [_57921, _57923, _57925], _57925), in(160 ^ [_57921, _57923, _57925], _57923)], (164 ^ _52504) ^ [] : [-(in(160 ^ [_57921, _57923, _57925], _57921))]]], (108 ^ _52504) ^ [_56152, _56154] : [-(_56154 = _56152), subset(_56154, _56152), subset(_56152, _56154)], (2 ^ _52504) ^ [_52628] : [-(_52628 = _52628)], (247 ^ _52504) ^ [] : [true___, -(true___)], (202 ^ _52504) ^ [_59448, _59450, _59452] : [-(_59448 = set_difference(_59452, _59450)), 214 ^ _52504 : [(219 ^ _52504) ^ [] : [in(203 ^ [_59448, _59450, _59452], _59448)], (217 ^ _52504) ^ [] : [in(203 ^ [_59448, _59450, _59452], _59450)], (215 ^ _52504) ^ [] : [-(in(203 ^ [_59448, _59450, _59452], _59452))]], 206 ^ _52504 : [(209 ^ _52504) ^ [] : [in(203 ^ [_59448, _59450, _59452], _59452), -(in(203 ^ [_59448, _59450, _59452], _59450))], (207 ^ _52504) ^ [] : [-(in(203 ^ [_59448, _59450, _59452], _59448))]]], (92 ^ _52504) ^ [_55575, _55577] : [in(_55577, _55575), in(_55575, _55577)], (20 ^ _52504) ^ [_53280, _53282, _53284, _53286] : [-(subset(_53284, _53280)), subset(_53286, _53282), _53286 = _53284, _53282 = _53280], (58 ^ _52504) ^ [_54443, _54445, _54447, _54449] : [-(disjoint(_54447, _54443)), disjoint(_54449, _54445), _54449 = _54447, _54445 = _54443], (4 ^ _52504) ^ [_52735, _52737] : [_52737 = _52735, -(_52735 = _52737)], (235 ^ _52504) ^ [] : [true___, -(true___)]], input).
% 60.85/59.38 ncf('1',plain,[316 : -(disjoint(311 ^ [], 312 ^ [])), 320 : -(set_difference(311 ^ [], 312 ^ []) = 311 ^ [])],start(314 ^ 0)).
% 60.85/59.38 ncf('1.1',plain,[disjoint(311 ^ [], 312 ^ []), -(set_intersection2(311 ^ [], 312 ^ []) = empty_set)],extension(223 ^ 3,bind([[_60234, _60236], [312 ^ [], 311 ^ []]]))).
% 60.85/59.38 ncf('1.1.1',plain,[set_intersection2(311 ^ [], 312 ^ []) = empty_set, -(empty_set = set_intersection2(311 ^ [], 312 ^ []))],extension(4 ^ 4,bind([[_52735, _52737], [empty_set, set_intersection2(311 ^ [], 312 ^ [])]]))).
% 60.85/59.38 ncf('1.1.1.1',plain,[empty_set = set_intersection2(311 ^ [], 312 ^ []), 141 : in(203 ^ [311 ^ [], 312 ^ [], 311 ^ []], empty_set), 147 : -(in(203 ^ [311 ^ [], 312 ^ [], 311 ^ []], 312 ^ []))],extension(137 ^ 5,bind([[_57196, _57198, _57200, _57378], [empty_set, 312 ^ [], 311 ^ [], 203 ^ [311 ^ [], 312 ^ [], 311 ^ []]]]))).
% 60.85/59.38 ncf('1.1.1.1.1',plain,[-(in(203 ^ [311 ^ [], 312 ^ [], 311 ^ []], empty_set)), in(203 ^ [311 ^ [], 312 ^ [], 311 ^ []], 311 ^ []), in(203 ^ [311 ^ [], 312 ^ [], 311 ^ []], 312 ^ [])],extension(149 ^ 8,bind([[_57637], [203 ^ [311 ^ [], 312 ^ [], 311 ^ []]]]))).
% 60.85/59.38 ncf('1.1.1.1.1.1',plain,[-(in(203 ^ [311 ^ [], 312 ^ [], 311 ^ []], 311 ^ [])), -(311 ^ [] = set_difference(311 ^ [], 312 ^ [])), 207 : -(in(203 ^ [311 ^ [], 312 ^ [], 311 ^ []], 311 ^ []))],extension(202 ^ 9,bind([[_59448, _59450, _59452], [311 ^ [], 312 ^ [], 311 ^ []]]))).
% 60.85/59.38 ncf('1.1.1.1.1.1.1',plain,[311 ^ [] = set_difference(311 ^ [], 312 ^ []), -(set_difference(311 ^ [], 312 ^ []) = 311 ^ [])],extension(4 ^ 10,bind([[_52735, _52737], [set_difference(311 ^ [], 312 ^ []), 311 ^ []]]))).
% 60.85/59.38 ncf('1.1.1.1.1.1.1.1',plain,[set_difference(311 ^ [], 312 ^ []) = 311 ^ []],extension(318 ^ 11)).
% 60.85/59.38 ncf('1.1.1.1.1.1.2',plain,[in(203 ^ [311 ^ [], 312 ^ [], 311 ^ []], 311 ^ [])],reduction('1.1.1.1.1')).
% 60.85/59.38 ncf('1.1.1.1.1.2',plain,[-(in(203 ^ [311 ^ [], 312 ^ [], 311 ^ []], 312 ^ [])), 209 : in(203 ^ [311 ^ [], 312 ^ [], 311 ^ []], 311 ^ []), 209 : -(311 ^ [] = set_difference(311 ^ [], 312 ^ [])), 219 : in(203 ^ [311 ^ [], 312 ^ [], 311 ^ []], 311 ^ [])],extension(202 ^ 9,bind([[_59448, _59450, _59452], [311 ^ [], 312 ^ [], 311 ^ []]]))).
% 60.85/59.38 ncf('1.1.1.1.1.2.1',plain,[-(in(203 ^ [311 ^ [], 312 ^ [], 311 ^ []], 311 ^ []))],lemmata('[1, 1, 1, 1].x')).
% 60.85/59.38 ncf('1.1.1.1.1.2.2',plain,[311 ^ [] = set_difference(311 ^ [], 312 ^ []), -(set_difference(311 ^ [], 312 ^ []) = 311 ^ [])],extension(4 ^ 10,bind([[_52735, _52737], [set_difference(311 ^ [], 312 ^ []), 311 ^ []]]))).
% 60.85/59.38 ncf('1.1.1.1.1.2.2.1',plain,[set_difference(311 ^ [], 312 ^ []) = 311 ^ []],extension(318 ^ 11)).
% 60.85/59.38 ncf('1.1.1.1.1.2.3',plain,[-(in(203 ^ [311 ^ [], 312 ^ [], 311 ^ []], 311 ^ []))],lemmata('[1, 1, 1, 1].x')).
% 60.85/59.38 ncf('1.1.1.1.2',plain,[in(203 ^ [311 ^ [], 312 ^ [], 311 ^ []], 312 ^ []), -(in(203 ^ [311 ^ [], 312 ^ [], 311 ^ []], empty_set)), in(203 ^ [311 ^ [], 312 ^ [], 311 ^ []], 311 ^ [])],extension(149 ^ 10,bind([[_57637], [203 ^ [311 ^ [], 312 ^ [], 311 ^ []]]]))).
% 60.85/59.38 ncf('1.1.1.1.2.1',plain,[in(203 ^ [311 ^ [], 312 ^ [], 311 ^ []], empty_set), -(in(203 ^ [311 ^ [], 312 ^ [], 311 ^ []], set_intersection2(311 ^ [], 312 ^ []))), 203 ^ [311 ^ [], 312 ^ [], 311 ^ []] = 203 ^ [311 ^ [], 312 ^ [], 311 ^ []], empty_set = set_intersection2(311 ^ [], 312 ^ [])],extension(34 ^ 11,bind([[_53724, _53726, _53728, _53730], [set_intersection2(311 ^ [], 312 ^ []), empty_set, 203 ^ [311 ^ [], 312 ^ [], 311 ^ []], 203 ^ [311 ^ [], 312 ^ [], 311 ^ []]]]))).
% 60.85/59.38 ncf('1.1.1.1.2.1.1',plain,[in(203 ^ [311 ^ [], 312 ^ [], 311 ^ []], set_intersection2(311 ^ [], 312 ^ [])), disjoint(311 ^ [], 312 ^ [])],extension(284 ^ 12,bind([[_62108, _62110, _62181], [312 ^ [], 311 ^ [], 203 ^ [311 ^ [], 312 ^ [], 311 ^ []]]]))).
% 60.85/59.38 ncf('1.1.1.1.2.1.1.1',plain,[-(disjoint(311 ^ [], 312 ^ []))],reduction('1')).
% 60.85/59.38 ncf('1.1.1.1.2.1.2',plain,[-(203 ^ [311 ^ [], 312 ^ [], 311 ^ []] = 203 ^ [311 ^ [], 312 ^ [], 311 ^ []])],extension(2 ^ 12,bind([[_52628], [203 ^ [311 ^ [], 312 ^ [], 311 ^ []]]]))).
% 60.85/59.38 ncf('1.1.1.1.2.1.3',plain,[-(empty_set = set_intersection2(311 ^ [], 312 ^ []))],reduction('1.1.1')).
% 60.85/59.38 ncf('1.1.1.1.2.2',plain,[-(in(203 ^ [311 ^ [], 312 ^ [], 311 ^ []], 311 ^ []))],extension(145 ^ 11)).
% 60.85/59.38 ncf('1.2',plain,[set_difference(311 ^ [], 312 ^ []) = 311 ^ [], 106 : -(subset(311 ^ [], set_difference(311 ^ [], 312 ^ [])))],extension(100 ^ 3,bind([[_55915, _55917], [311 ^ [], set_difference(311 ^ [], 312 ^ [])]]))).
% 60.85/59.38 ncf('1.2.1',plain,[subset(311 ^ [], set_difference(311 ^ [], 312 ^ [])), -(311 ^ [] = set_difference(311 ^ [], 312 ^ [])), subset(set_difference(311 ^ [], 312 ^ []), 311 ^ [])],extension(108 ^ 6,bind([[_56152, _56154], [set_difference(311 ^ [], 312 ^ []), 311 ^ []]]))).
% 60.85/59.38 ncf('1.2.1.1',plain,[311 ^ [] = set_difference(311 ^ [], 312 ^ []), 184 : in(280 ^ [312 ^ [], 311 ^ []], 311 ^ []), 190 : in(280 ^ [312 ^ [], 311 ^ []], 312 ^ [])],extension(180 ^ 7,bind([[_58717, _58719, _58721, _58901], [311 ^ [], 312 ^ [], 311 ^ [], 280 ^ [312 ^ [], 311 ^ []]]]))).
% 60.85/59.38 ncf('1.2.1.1.1',plain,[-(in(280 ^ [312 ^ [], 311 ^ []], 311 ^ [])), 141 : in(280 ^ [312 ^ [], 311 ^ []], set_intersection2(311 ^ [], 312 ^ [])), 141 : set_intersection2(311 ^ [], 312 ^ []) = set_intersection2(312 ^ [], 311 ^ [])],extension(137 ^ 10,bind([[_57196, _57198, _57200, _57378], [set_intersection2(311 ^ [], 312 ^ []), 311 ^ [], 312 ^ [], 280 ^ [312 ^ [], 311 ^ []]]]))).
% 60.85/59.38 ncf('1.2.1.1.1.1',plain,[-(in(280 ^ [312 ^ [], 311 ^ []], set_intersection2(311 ^ [], 312 ^ []))), -(disjoint(311 ^ [], 312 ^ []))],extension(277 ^ 13,bind([[_61873, _61875], [312 ^ [], 311 ^ []]]))).
% 60.85/59.38 ncf('1.2.1.1.1.1.1',plain,[disjoint(311 ^ [], 312 ^ [])],extension(322 ^ 14)).
% 60.85/59.38 ncf('1.2.1.1.1.2',plain,[-(set_intersection2(311 ^ [], 312 ^ []) = set_intersection2(312 ^ [], 311 ^ []))],extension(98 ^ 11,bind([[_55771, _55773], [312 ^ [], 311 ^ []]]))).
% 60.85/59.38 ncf('1.2.1.1.2',plain,[-(in(280 ^ [312 ^ [], 311 ^ []], 312 ^ [])), 141 : in(280 ^ [312 ^ [], 311 ^ []], set_intersection2(311 ^ [], 312 ^ [])), 141 : set_intersection2(311 ^ [], 312 ^ []) = set_intersection2(set_difference(311 ^ [], 312 ^ []), 312 ^ [])],extension(137 ^ 12,bind([[_57196, _57198, _57200, _57378], [set_intersection2(311 ^ [], 312 ^ []), 312 ^ [], set_difference(311 ^ [], 312 ^ []), 280 ^ [312 ^ [], 311 ^ []]]]))).
% 60.85/59.38 ncf('1.2.1.1.2.1',plain,[-(in(280 ^ [312 ^ [], 311 ^ []], set_intersection2(311 ^ [], 312 ^ []))), -(disjoint(311 ^ [], 312 ^ []))],extension(277 ^ 15,bind([[_61873, _61875], [312 ^ [], 311 ^ []]]))).
% 60.85/59.38 ncf('1.2.1.1.2.1.1',plain,[disjoint(311 ^ [], 312 ^ [])],extension(322 ^ 16)).
% 60.85/59.38 ncf('1.2.1.1.2.2',plain,[-(set_intersection2(311 ^ [], 312 ^ []) = set_intersection2(set_difference(311 ^ [], 312 ^ []), 312 ^ [])), 311 ^ [] = set_difference(311 ^ [], 312 ^ []), 312 ^ [] = 312 ^ []],extension(72 ^ 13,bind([[_54899, _54901, _54903, _54905], [312 ^ [], 312 ^ [], set_difference(311 ^ [], 312 ^ []), 311 ^ []]]))).
% 60.85/59.38 ncf('1.2.1.1.2.2.1',plain,[-(311 ^ [] = set_difference(311 ^ [], 312 ^ []))],reduction('1.2.1')).
% 60.85/59.38 ncf('1.2.1.1.2.2.2',plain,[-(312 ^ [] = 312 ^ [])],extension(2 ^ 14,bind([[_52628], [312 ^ []]]))).
% 60.85/59.38 ncf('1.2.1.2',plain,[-(subset(set_difference(311 ^ [], 312 ^ []), 311 ^ [])), 133 : in(129 ^ [311 ^ [], set_difference(311 ^ [], 312 ^ [])], 311 ^ [])],extension(128 ^ 7,bind([[_56796, _56798], [311 ^ [], set_difference(311 ^ [], 312 ^ [])]]))).
% 60.85/59.38 ncf('1.2.1.2.1',plain,[-(in(129 ^ [311 ^ [], set_difference(311 ^ [], 312 ^ [])], 311 ^ [])), in(129 ^ [311 ^ [], set_difference(311 ^ [], 312 ^ [])], set_difference(311 ^ [], 312 ^ [])), 129 ^ [311 ^ [], set_difference(311 ^ [], 312 ^ [])] = 129 ^ [311 ^ [], set_difference(311 ^ [], 312 ^ [])], set_difference(311 ^ [], 312 ^ []) = 311 ^ []],extension(34 ^ 10,bind([[_53724, _53726, _53728, _53730], [311 ^ [], set_difference(311 ^ [], 312 ^ []), 129 ^ [311 ^ [], set_difference(311 ^ [], 312 ^ [])], 129 ^ [311 ^ [], set_difference(311 ^ [], 312 ^ [])]]]))).
% 60.85/59.38 ncf('1.2.1.2.1.1',plain,[-(in(129 ^ [311 ^ [], set_difference(311 ^ [], 312 ^ [])], set_difference(311 ^ [], 312 ^ [])))],extension(131 ^ 11)).
% 60.85/59.38 ncf('1.2.1.2.1.2',plain,[-(129 ^ [311 ^ [], set_difference(311 ^ [], 312 ^ [])] = 129 ^ [311 ^ [], set_difference(311 ^ [], 312 ^ [])]), subset(129 ^ [311 ^ [], set_difference(311 ^ [], 312 ^ [])], 129 ^ [311 ^ [], set_difference(311 ^ [], 312 ^ [])]), subset(129 ^ [311 ^ [], set_difference(311 ^ [], 312 ^ [])], 129 ^ [311 ^ [], set_difference(311 ^ [], 312 ^ [])])],extension(108 ^ 11,bind([[_56152, _56154], [129 ^ [311 ^ [], set_difference(311 ^ [], 312 ^ [])], 129 ^ [311 ^ [], set_difference(311 ^ [], 312 ^ [])]]]))).
% 60.85/59.38 ncf('1.2.1.2.1.2.1',plain,[-(subset(129 ^ [311 ^ [], set_difference(311 ^ [], 312 ^ [])], 129 ^ [311 ^ [], set_difference(311 ^ [], 312 ^ [])]))],extension(263 ^ 12,bind([[_61291, _61293], [_42201, 129 ^ [311 ^ [], set_difference(311 ^ [], 312 ^ [])]]]))).
% 60.85/59.38 ncf('1.2.1.2.1.2.2',plain,[-(subset(129 ^ [311 ^ [], set_difference(311 ^ [], 312 ^ [])], 129 ^ [311 ^ [], set_difference(311 ^ [], 312 ^ [])]))],lemmata('[1, 2, 1, 2, 1].x')).
% 60.85/59.38 ncf('1.2.1.2.1.3',plain,[-(set_difference(311 ^ [], 312 ^ []) = 311 ^ [])],reduction('1')).
% 60.85/59.38 %-----------------------------------------------------
% 60.85/59.38 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------