%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : SEU217+1 : TPTP v8.1.2. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n025.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:42 EDT 2023
% Result : Theorem 0.32s 1.37s
% Output : Proof 0.32s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : SEU217+1 : TPTP v8.1.2. Released v3.3.0.
% 0.11/0.12 % Command : nanocop.sh %s %d
% 0.13/0.33 % Computer : n025.cluster.edu
% 0.13/0.33 % Model : x86_64 x86_64
% 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.33 % Memory : 8042.1875MB
% 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.33 % CPULimit : 300
% 0.13/0.33 % WCLimit : 300
% 0.13/0.33 % DateTime : Thu May 18 13:56:33 EDT 2023
% 0.13/0.33 % CPUTime :
% 0.32/1.37
% 0.32/1.37 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 0.32/1.37 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.32/1.37 %-----------------------------------------------------
% 0.32/1.37 ncf(matrix, plain, [(290 ^ _38903) ^ [] : [-(in(288 ^ [], 287 ^ []))], (292 ^ _38903) ^ [] : [apply(identity_relation(287 ^ []), 288 ^ []) = 288 ^ []], (88 ^ _38903) ^ [_41735, _41737] : [_41737 = _41735, -(relation_dom(_41737) = relation_dom(_41735))], (104 ^ _38903) ^ [_42292, _42294] : [_42294 = _42292, -(identity_relation(_42294) = identity_relation(_42292))], (94 ^ _38903) ^ [_41981, _41983, _41985, _41987] : [-(apply(_41987, _41983) = apply(_41985, _41981)), _41987 = _41985, _41983 = _41981], (2 ^ _38903) ^ [_39047] : [-(_39047 = _39047)], (4 ^ _38903) ^ [_39154, _39156] : [_39156 = _39154, -(_39154 = _39156)], (10 ^ _38903) ^ [_39358, _39360, _39362] : [-(_39362 = _39358), _39362 = _39360, _39360 = _39358], (20 ^ _38903) ^ [_39671, _39673] : [-(relation_empty_yielding(_39671)), _39673 = _39671, relation_empty_yielding(_39673)], (30 ^ _38903) ^ [_39994, _39996, _39998, _40000] : [-(element(_39998, _39994)), element(_40000, _39996), _40000 = _39998, _39996 = _39994], (44 ^ _38903) ^ [_40410, _40412] : [-(empty(_40410)), _40412 = _40410, empty(_40412)], (54 ^ _38903) ^ [_40705, _40707] : [-(relation(_40705)), _40707 = _40705, relation(_40707)], (64 ^ _38903) ^ [_41000, _41002] : [-(function(_41000)), _41002 = _41000, function(_41002)], (74 ^ _38903) ^ [_41303, _41305, _41307, _41309] : [-(in(_41307, _41303)), in(_41309, _41305), _41309 = _41307, _41305 = _41303], (111 ^ _38903) ^ [] : [-(relation(109 ^ []))], (113 ^ _38903) ^ [] : [-(relation_empty_yielding(109 ^ []))], (115 ^ _38903) ^ [] : [true___, -(true___)], (121 ^ _38903) ^ [] : [-(empty(empty_set))], (123 ^ _38903) ^ [] : [-(relation(empty_set))], (125 ^ _38903) ^ [] : [-(empty(empty_set))], (127 ^ _38903) ^ [] : [-(relation(empty_set))], (129 ^ _38903) ^ [] : [-(relation_empty_yielding(empty_set))], (131 ^ _38903) ^ [] : [-(empty(empty_set))], (134 ^ _38903) ^ [_43122] : [-(element(132 ^ [_43122], _43122))], (136 ^ _38903) ^ [] : [true___, -(true___)], (142 ^ _38903) ^ [_43339] : [empty(_43339), -(function(_43339))], (149 ^ _38903) ^ [] : [-(empty(147 ^ []))], (151 ^ _38903) ^ [] : [-(relation(147 ^ []))], (153 ^ _38903) ^ [_43674] : [empty(_43674), -(relation(_43674))], (160 ^ _38903) ^ [] : [empty(158 ^ [])], (162 ^ _38903) ^ [] : [-(relation(158 ^ []))], (164 ^ _38903) ^ [_44010] : [empty(relation_dom(_44010)), -(empty(_44010)), relation(_44010)], (174 ^ _38903) ^ [_44287] : [empty(_44287), 177 ^ _38903 : [(178 ^ _38903) ^ [] : [-(empty(relation_dom(_44287)))], (180 ^ _38903) ^ [] : [-(relation(relation_dom(_44287)))]]], (183 ^ _38903) ^ [] : [-(empty(181 ^ []))], (186 ^ _38903) ^ [] : [empty(184 ^ [])], (188 ^ _38903) ^ [_44745, _44747] : [element(_44747, _44745), -(empty(_44745)), -(in(_44747, _44745))], (198 ^ _38903) ^ [_45029] : [empty(_45029), -(_45029 = empty_set)], (204 ^ _38903) ^ [_45231, _45233] : [empty(_45233), -(_45233 = _45231), empty(_45231)], (214 ^ _38903) ^ [_45528, _45530] : [in(_45530, _45528), in(_45528, _45530)], (220 ^ _38903) ^ [] : [true___, -(true___)], (226 ^ _38903) ^ [] : [true___, -(true___)], (232 ^ _38903) ^ [_45948] : [-(relation(identity_relation(_45948)))], (235 ^ _38903) ^ [] : [-(relation(233 ^ []))], (237 ^ _38903) ^ [] : [-(function(233 ^ []))], (239 ^ _38903) ^ [_46196] : [-(relation(identity_relation(_46196)))], (241 ^ _38903) ^ [_46241] : [-(function(identity_relation(_46241)))], (243 ^ _38903) ^ [_46351, _46353] : [in(_46353, _46351), -(element(_46353, _46351))], (249 ^ _38903) ^ [_46561, _46563] : [in(_46563, _46561), empty(_46561)], (255 ^ _38903) ^ [_46748, _46750] : [relation(_46748), function(_46748), 262 ^ _38903 : [(263 ^ _38903) ^ [] : [_46748 = identity_relation(_46750), 266 ^ _38903 : [(267 ^ _38903) ^ [] : [-(relation_dom(_46748) = _46750)], (269 ^ _38903) ^ [_47167] : [in(_47167, _46750), -(apply(_46748, _47167) = _47167)]]], (275 ^ _38903) ^ [] : [-(_46748 = identity_relation(_46750)), relation_dom(_46748) = _46750, 281 ^ _38903 : [(282 ^ _38903) ^ [] : [-(in(280 ^ [_46748, _46750], _46750))], (284 ^ _38903) ^ [] : [apply(_46748, 280 ^ [_46748, _46750]) = 280 ^ [_46748, _46750]]]]]]], input).
% 0.32/1.37 ncf('1',plain,[apply(identity_relation(287 ^ []), 288 ^ []) = 288 ^ []],start(292 ^ 0)).
% 0.32/1.37 ncf('1.1',plain,[-(apply(identity_relation(287 ^ []), 288 ^ []) = 288 ^ []), 269 : in(288 ^ [], 287 ^ []), 269 : identity_relation(287 ^ []) = identity_relation(287 ^ []), 263 : relation(identity_relation(287 ^ [])), 263 : function(identity_relation(287 ^ []))],extension(255 ^ 1,bind([[_46748, _46750, _47167], [identity_relation(287 ^ []), 287 ^ [], 288 ^ []]]))).
% 0.32/1.37 ncf('1.1.1',plain,[-(in(288 ^ [], 287 ^ []))],extension(290 ^ 6)).
% 0.32/1.37 ncf('1.1.2',plain,[-(identity_relation(287 ^ []) = identity_relation(287 ^ []))],extension(2 ^ 4,bind([[_39047], [identity_relation(287 ^ [])]]))).
% 0.32/1.37 ncf('1.1.3',plain,[-(relation(identity_relation(287 ^ [])))],extension(232 ^ 2,bind([[_45948], [287 ^ []]]))).
% 0.32/1.37 ncf('1.1.4',plain,[-(function(identity_relation(287 ^ [])))],extension(241 ^ 2,bind([[_46241], [287 ^ []]]))).
% 0.32/1.37 %-----------------------------------------------------
% 0.32/1.37 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------