%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : SEU124+1 : TPTP v8.1.2. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n028.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:16 EDT 2023
% Result : Theorem 0.25s 1.38s
% Output : Proof 0.25s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SEU124+1 : TPTP v8.1.2. Released v3.3.0.
% 0.00/0.12 % Command : nanocop.sh %s %d
% 0.12/0.32 % Computer : n028.cluster.edu
% 0.12/0.32 % Model : x86_64 x86_64
% 0.12/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.32 % Memory : 8042.1875MB
% 0.12/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.32 % CPULimit : 300
% 0.12/0.32 % WCLimit : 300
% 0.12/0.32 % DateTime : Thu May 18 13:01:33 EDT 2023
% 0.12/0.33 % CPUTime :
% 0.25/1.38
% 0.25/1.38 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 0.25/1.38 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.25/1.38 %-----------------------------------------------------
% 0.25/1.38 ncf(matrix, plain, [(200 ^ _28301) ^ [] : [subset(197 ^ [], set_union2(197 ^ [], 198 ^ []))], (58 ^ _28301) ^ [_30250, _30252, _30254, _30256] : [-(set_union2(_30256, _30252) = set_union2(_30254, _30250)), _30256 = _30254, _30252 = _30250], (2 ^ _28301) ^ [_28445] : [-(_28445 = _28445)], (4 ^ _28301) ^ [_28552, _28554] : [_28554 = _28552, -(_28552 = _28554)], (10 ^ _28301) ^ [_28756, _28758, _28760] : [-(_28760 = _28756), _28760 = _28758, _28758 = _28756], (20 ^ _28301) ^ [_29097, _29099, _29101, _29103] : [-(in(_29101, _29097)), in(_29103, _29099), _29103 = _29101, _29099 = _29097], (34 ^ _28301) ^ [_29513, _29515] : [-(empty(_29513)), _29515 = _29513, empty(_29515)], (44 ^ _28301) ^ [_29816, _29818, _29820, _29822] : [-(subset(_29820, _29816)), subset(_29822, _29818), _29822 = _29820, _29818 = _29816], (68 ^ _28301) ^ [_30583, _30585] : [in(_30585, _30583), in(_30583, _30585)], (74 ^ _28301) ^ [_30779, _30781] : [-(set_union2(_30781, _30779) = set_union2(_30779, _30781))], (98 ^ _28301) ^ [_31662, _31664, _31666] : [-(_31662 = set_union2(_31666, _31664)), 102 ^ _28301 : [(103 ^ _28301) ^ [] : [-(in(99 ^ [_31662, _31664, _31666], _31662))], (105 ^ _28301) ^ [] : [in(99 ^ [_31662, _31664, _31666], _31666)], (107 ^ _28301) ^ [] : [in(99 ^ [_31662, _31664, _31666], _31664)]], 108 ^ _28301 : [(115 ^ _28301) ^ [] : [in(99 ^ [_31662, _31664, _31666], _31662)], (109 ^ _28301) ^ [] : [-(in(99 ^ [_31662, _31664, _31666], _31666)), -(in(99 ^ [_31662, _31664, _31666], _31664))]]], (76 ^ _28301) ^ [_30937, _30939, _30941] : [_30937 = set_union2(_30941, _30939), 79 ^ _28301 : [(90 ^ _28301) ^ [_31397] : [91 ^ _28301 : [(92 ^ _28301) ^ [] : [in(_31397, _30941)], (94 ^ _28301) ^ [] : [in(_31397, _30939)]], -(in(_31397, _30937))], (80 ^ _28301) ^ [_31119] : [in(_31119, _30937), -(in(_31119, _30941)), -(in(_31119, _30939))]]], (129 ^ _28301) ^ [_32756, _32758] : [131 ^ _28301 : [(132 ^ _28301) ^ [] : [-(in(130 ^ [_32756, _32758], _32758))], (134 ^ _28301) ^ [] : [in(130 ^ [_32756, _32758], _32756)]], -(subset(_32758, _32756))], (119 ^ _28301) ^ [_32442, _32444] : [subset(_32444, _32442), 122 ^ _28301 : [(123 ^ _28301) ^ [_32579] : [in(_32579, _32444), -(in(_32579, _32442))]]], (138 ^ _28301) ^ [] : [true___, -(true___)], (144 ^ _28301) ^ [] : [true___, -(true___)], (150 ^ _28301) ^ [] : [-(empty(empty_set))], (152 ^ _28301) ^ [_33404, _33406] : [-(empty(_33406)), empty(set_union2(_33406, _33404))], (158 ^ _28301) ^ [_33620, _33622] : [-(empty(_33622)), empty(set_union2(_33620, _33622))], (164 ^ _28301) ^ [_33821, _33823] : [-(set_union2(_33823, _33823) = _33823)], (167 ^ _28301) ^ [] : [-(empty(165 ^ []))], (170 ^ _28301) ^ [] : [empty(168 ^ [])], (172 ^ _28301) ^ [_34097, _34099] : [-(subset(_34099, _34099))], (174 ^ _28301) ^ [_34177] : [-(set_union2(_34177, empty_set) = _34177)], (176 ^ _28301) ^ [_34273] : [empty(_34273), -(_34273 = empty_set)], (182 ^ _28301) ^ [_34475, _34477] : [in(_34477, _34475), empty(_34475)], (188 ^ _28301) ^ [_34662, _34664] : [empty(_34664), -(_34664 = _34662), empty(_34662)]], input).
% 0.25/1.38 ncf('1',plain,[subset(197 ^ [], set_union2(197 ^ [], 198 ^ []))],start(200 ^ 0)).
% 0.25/1.38 ncf('1.1',plain,[-(subset(197 ^ [], set_union2(197 ^ [], 198 ^ []))), 134 : in(130 ^ [set_union2(197 ^ [], 198 ^ []), 197 ^ []], set_union2(197 ^ [], 198 ^ []))],extension(129 ^ 1,bind([[_32756, _32758], [set_union2(197 ^ [], 198 ^ []), 197 ^ []]]))).
% 0.25/1.38 ncf('1.1.1',plain,[-(in(130 ^ [set_union2(197 ^ [], 198 ^ []), 197 ^ []], set_union2(197 ^ [], 198 ^ []))), 92 : in(130 ^ [set_union2(197 ^ [], 198 ^ []), 197 ^ []], 197 ^ []), 90 : set_union2(197 ^ [], 198 ^ []) = set_union2(197 ^ [], 198 ^ [])],extension(76 ^ 4,bind([[_30937, _30939, _30941, _31397], [set_union2(197 ^ [], 198 ^ []), 198 ^ [], 197 ^ [], 130 ^ [set_union2(197 ^ [], 198 ^ []), 197 ^ []]]]))).
% 0.25/1.38 ncf('1.1.1.1',plain,[-(in(130 ^ [set_union2(197 ^ [], 198 ^ []), 197 ^ []], 197 ^ []))],extension(132 ^ 9)).
% 0.25/1.38 ncf('1.1.1.2',plain,[-(set_union2(197 ^ [], 198 ^ []) = set_union2(197 ^ [], 198 ^ []))],extension(2 ^ 5,bind([[_28445], [set_union2(197 ^ [], 198 ^ [])]]))).
% 0.25/1.38 %-----------------------------------------------------
% 0.25/1.38 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------