%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : SEU196+1 : TPTP v8.1.2. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n013.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:36 EDT 2023
% Result : Theorem 0.33s 1.37s
% Output : Proof 0.33s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : SEU196+1 : TPTP v8.1.2. Released v3.3.0.
% 0.11/0.12 % Command : nanocop.sh %s %d
% 0.12/0.33 % Computer : n013.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 13:10:05 EDT 2023
% 0.12/0.33 % CPUTime :
% 0.33/1.37
% 0.33/1.37 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 0.33/1.37 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.33/1.37 %-----------------------------------------------------
% 0.33/1.37 ncf(matrix, plain, [(331 ^ _47185) ^ [] : [-(relation(329 ^ []))], (333 ^ _47185) ^ [] : [subset(relation_rng(relation_dom_restriction(329 ^ [], 328 ^ [])), relation_rng(329 ^ []))], (82 ^ _47185) ^ [_49869, _49871] : [_49871 = _49869, -(relation_dom(_49871) = relation_dom(_49869))], (88 ^ _47185) ^ [_50087, _50089] : [_50089 = _50087, -(powerset(_50089) = powerset(_50087))], (104 ^ _47185) ^ [_50644, _50646] : [_50646 = _50644, -(relation_rng(_50646) = relation_rng(_50644))], (94 ^ _47185) ^ [_50333, _50335, _50337, _50339] : [-(relation_dom_restriction(_50339, _50335) = relation_dom_restriction(_50337, _50333)), _50339 = _50337, _50335 = _50333], (2 ^ _47185) ^ [_47329] : [-(_47329 = _47329)], (4 ^ _47185) ^ [_47436, _47438] : [_47438 = _47436, -(_47436 = _47438)], (10 ^ _47185) ^ [_47640, _47642, _47644] : [-(_47644 = _47640), _47644 = _47642, _47642 = _47640], (20 ^ _47185) ^ [_47981, _47983, _47985, _47987] : [-(element(_47985, _47981)), element(_47987, _47983), _47987 = _47985, _47983 = _47981], (34 ^ _47185) ^ [_48425, _48427, _48429, _48431] : [-(in(_48429, _48425)), in(_48431, _48427), _48431 = _48429, _48427 = _48425], (48 ^ _47185) ^ [_48841, _48843] : [-(empty(_48841)), _48843 = _48841, empty(_48843)], (58 ^ _47185) ^ [_49136, _49138] : [-(relation(_49136)), _49138 = _49136, relation(_49138)], (68 ^ _47185) ^ [_49439, _49441, _49443, _49445] : [-(subset(_49443, _49439)), subset(_49445, _49441), _49445 = _49443, _49441 = _49439], (110 ^ _47185) ^ [_50876, _50878] : [in(_50878, _50876), in(_50876, _50878)], (116 ^ _47185) ^ [_51073] : [empty(_51073), -(relation(_51073))], (122 ^ _47185) ^ [] : [true___, -(true___)], (128 ^ _47185) ^ [] : [true___, -(true___)], (134 ^ _47185) ^ [] : [true___, -(true___)], (140 ^ _47185) ^ [] : [true___, -(true___)], (146 ^ _47185) ^ [_51749, _51751] : [relation(_51751), -(relation(relation_dom_restriction(_51751, _51749)))], (152 ^ _47185) ^ [] : [true___, -(true___)], (159 ^ _47185) ^ [_52090] : [-(element(157 ^ [_52090], _52090))], (161 ^ _47185) ^ [_52172] : [empty(powerset(_52172))], (163 ^ _47185) ^ [] : [-(empty(empty_set))], (165 ^ _47185) ^ [] : [-(empty(empty_set))], (167 ^ _47185) ^ [] : [-(relation(empty_set))], (169 ^ _47185) ^ [_52427] : [empty(relation_dom(_52427)), -(empty(_52427)), relation(_52427)], (179 ^ _47185) ^ [_52704] : [empty(relation_rng(_52704)), -(empty(_52704)), relation(_52704)], (189 ^ _47185) ^ [_52981] : [empty(_52981), 192 ^ _47185 : [(193 ^ _47185) ^ [] : [-(empty(relation_dom(_52981)))], (195 ^ _47185) ^ [] : [-(relation(relation_dom(_52981)))]]], (197 ^ _47185) ^ [_53246] : [empty(_53246), 200 ^ _47185 : [(201 ^ _47185) ^ [] : [-(empty(relation_rng(_53246)))], (203 ^ _47185) ^ [] : [-(relation(relation_rng(_53246)))]]], (206 ^ _47185) ^ [] : [-(empty(204 ^ []))], (208 ^ _47185) ^ [] : [-(relation(204 ^ []))], (210 ^ _47185) ^ [_53660] : [-(empty(_53660)), 214 ^ _47185 : [(215 ^ _47185) ^ [] : [-(element(213 ^ [_53660], powerset(_53660)))], (217 ^ _47185) ^ [] : [empty(213 ^ [_53660])]]], (220 ^ _47185) ^ [] : [-(empty(218 ^ []))], (223 ^ _47185) ^ [] : [empty(221 ^ [])], (225 ^ _47185) ^ [] : [-(relation(221 ^ []))], (228 ^ _47185) ^ [_54282] : [-(element(226 ^ [_54282], powerset(_54282)))], (230 ^ _47185) ^ [_54333] : [-(empty(226 ^ [_54333]))], (233 ^ _47185) ^ [] : [empty(231 ^ [])], (235 ^ _47185) ^ [_54521, _54523] : [-(subset(_54523, _54523))], (237 ^ _47185) ^ [_54630, _54632] : [in(_54632, _54630), -(element(_54632, _54630))], (243 ^ _47185) ^ [_54826] : [relation(_54826), 246 ^ _47185 : [(247 ^ _47185) ^ [_54976] : [relation(_54976), subset(_54826, _54976), 254 ^ _47185 : [(255 ^ _47185) ^ [] : [-(subset(relation_dom(_54826), relation_dom(_54976)))], (257 ^ _47185) ^ [] : [-(subset(relation_rng(_54826), relation_rng(_54976)))]]]]], (259 ^ _47185) ^ [_55371, _55373] : [element(_55373, _55371), -(empty(_55371)), -(in(_55373, _55371))], (269 ^ _47185) ^ [_55698, _55700] : [element(_55700, powerset(_55698)), -(subset(_55700, _55698))], (275 ^ _47185) ^ [_55864, _55866] : [subset(_55866, _55864), -(element(_55866, powerset(_55864)))], (281 ^ _47185) ^ [_56094, _56096, _56098] : [-(element(_56098, _56094)), in(_56098, _56096), element(_56096, powerset(_56094))], (291 ^ _47185) ^ [_56421, _56423, _56425] : [in(_56425, _56423), element(_56423, powerset(_56421)), empty(_56421)], (301 ^ _47185) ^ [_56717] : [empty(_56717), -(_56717 = empty_set)], (307 ^ _47185) ^ [_56919, _56921] : [in(_56921, _56919), empty(_56919)], (313 ^ _47185) ^ [_57126, _57128] : [relation(_57126), -(subset(relation_dom_restriction(_57126, _57128), _57126))], (319 ^ _47185) ^ [_57320, _57322] : [empty(_57322), -(_57322 = _57320), empty(_57320)]], input).
% 0.33/1.37 ncf('1',plain,[subset(relation_rng(relation_dom_restriction(329 ^ [], 328 ^ [])), relation_rng(329 ^ []))],start(333 ^ 0)).
% 0.33/1.37 ncf('1.1',plain,[-(subset(relation_rng(relation_dom_restriction(329 ^ [], 328 ^ [])), relation_rng(329 ^ []))), 247 : relation(329 ^ []), 247 : subset(relation_dom_restriction(329 ^ [], 328 ^ []), 329 ^ []), 247 : relation(relation_dom_restriction(329 ^ [], 328 ^ []))],extension(243 ^ 1,bind([[_54826, _54976], [relation_dom_restriction(329 ^ [], 328 ^ []), 329 ^ []]]))).
% 0.33/1.37 ncf('1.1.1',plain,[-(relation(329 ^ []))],extension(331 ^ 4)).
% 0.33/1.37 ncf('1.1.2',plain,[-(subset(relation_dom_restriction(329 ^ [], 328 ^ []), 329 ^ [])), relation(329 ^ [])],extension(313 ^ 4,bind([[_57126, _57128], [329 ^ [], 328 ^ []]]))).
% 0.33/1.37 ncf('1.1.2.1',plain,[-(relation(329 ^ []))],lemmata('[1].x')).
% 0.33/1.37 ncf('1.1.3',plain,[-(relation(relation_dom_restriction(329 ^ [], 328 ^ []))), relation(329 ^ [])],extension(146 ^ 2,bind([[_51749, _51751], [328 ^ [], 329 ^ []]]))).
% 0.33/1.37 ncf('1.1.3.1',plain,[-(relation(329 ^ []))],extension(331 ^ 3)).
% 0.33/1.37 %-----------------------------------------------------
% 0.33/1.37 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------