%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : SEU148+1 : TPTP v8.1.2. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n004.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:22 EDT 2023
% Result : Theorem 0.33s 1.38s
% Output : Proof 0.33s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12 % Problem : SEU148+1 : TPTP v8.1.2. Released v3.3.0.
% 0.06/0.13 % Command : nanocop.sh %s %d
% 0.13/0.34 % Computer : n004.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Thu May 18 12:57:54 EDT 2023
% 0.13/0.34 % CPUTime :
% 0.33/1.38
% 0.33/1.38 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 0.33/1.38 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.33/1.38 %-----------------------------------------------------
% 0.33/1.38 ncf(matrix, plain, [(145 ^ _20062) ^ [] : [-(subset(singleton(142 ^ []), singleton(143 ^ [])))], (147 ^ _20062) ^ [] : [142 ^ [] = 143 ^ []], (58 ^ _20062) ^ [_21983, _21985] : [_21985 = _21983, -(singleton(_21985) = singleton(_21983))], (2 ^ _20062) ^ [_20206] : [-(_20206 = _20206)], (4 ^ _20062) ^ [_20313, _20315] : [_20315 = _20313, -(_20313 = _20315)], (10 ^ _20062) ^ [_20517, _20519, _20521] : [-(_20521 = _20517), _20521 = _20519, _20519 = _20517], (20 ^ _20062) ^ [_20858, _20860, _20862, _20864] : [-(in(_20862, _20858)), in(_20864, _20860), _20864 = _20862, _20860 = _20858], (34 ^ _20062) ^ [_21274, _21276] : [-(empty(_21274)), _21276 = _21274, empty(_21276)], (44 ^ _20062) ^ [_21577, _21579, _21581, _21583] : [-(subset(_21581, _21577)), subset(_21583, _21579), _21583 = _21581, _21579 = _21577], (64 ^ _20062) ^ [_22203, _22205] : [in(_22205, _22203), in(_22203, _22205)], (86 ^ _20062) ^ [_22964, _22966] : [-(_22964 = singleton(_22966)), 90 ^ _20062 : [(91 ^ _20062) ^ [] : [-(in(87 ^ [_22964, _22966], _22964))], (93 ^ _20062) ^ [] : [87 ^ [_22964, _22966] = _22966]], 94 ^ _20062 : [(95 ^ _20062) ^ [] : [-(87 ^ [_22964, _22966] = _22966)], (97 ^ _20062) ^ [] : [in(87 ^ [_22964, _22966], _22964)]]], (70 ^ _20062) ^ [_22443, _22445] : [_22443 = singleton(_22445), 73 ^ _20062 : [(74 ^ _20062) ^ [_22613] : [in(_22613, _22443), -(_22613 = _22445)], (80 ^ _20062) ^ [_22785] : [_22785 = _22445, -(in(_22785, _22443))]]], (101 ^ _20062) ^ [] : [true___, -(true___)], (107 ^ _20062) ^ [] : [true___, -(true___)], (113 ^ _20062) ^ [] : [-(empty(empty_set))], (115 ^ _20062) ^ [_23761] : [singleton(_23761) = empty_set], (136 ^ _20062) ^ [] : [-(empty(134 ^ []))], (139 ^ _20062) ^ [] : [empty(137 ^ [])], (141 ^ _20062) ^ [_24597, _24599] : [-(subset(_24599, _24599))], (127 ^ _20062) ^ [_24159, _24161] : [128 ^ _20062 : [(129 ^ _20062) ^ [] : [_24161 = empty_set], (131 ^ _20062) ^ [] : [_24161 = singleton(_24159)]], -(subset(_24161, singleton(_24159)))], (117 ^ _20062) ^ [_23899, _23901] : [subset(_23901, singleton(_23899)), -(_23901 = empty_set), -(_23901 = singleton(_23899))]], input).
% 0.33/1.38 ncf('1',plain,[142 ^ [] = 143 ^ []],start(147 ^ 0)).
% 0.33/1.38 ncf('1.1',plain,[-(142 ^ [] = 143 ^ []), 74 : in(142 ^ [], singleton(142 ^ [])), 74 : singleton(142 ^ []) = singleton(143 ^ [])],extension(70 ^ 1,bind([[_22443, _22445, _22613], [singleton(142 ^ []), 143 ^ [], 142 ^ []]]))).
% 0.33/1.38 ncf('1.1.1',plain,[-(in(142 ^ [], singleton(142 ^ []))), 80 : 142 ^ [] = 142 ^ [], 80 : singleton(142 ^ []) = singleton(142 ^ [])],extension(70 ^ 4,bind([[_22443, _22445, _22785], [singleton(142 ^ []), 142 ^ [], 142 ^ []]]))).
% 0.33/1.38 ncf('1.1.1.1',plain,[-(142 ^ [] = 142 ^ [])],extension(2 ^ 7,bind([[_20206], [142 ^ []]]))).
% 0.33/1.38 ncf('1.1.1.2',plain,[-(singleton(142 ^ []) = singleton(142 ^ []))],extension(2 ^ 5,bind([[_20206], [singleton(142 ^ [])]]))).
% 0.33/1.38 ncf('1.1.2',plain,[-(singleton(142 ^ []) = singleton(143 ^ [])), subset(singleton(142 ^ []), singleton(143 ^ [])), -(singleton(142 ^ []) = empty_set)],extension(117 ^ 2,bind([[_23899, _23901], [143 ^ [], singleton(142 ^ [])]]))).
% 0.33/1.38 ncf('1.1.2.1',plain,[-(subset(singleton(142 ^ []), singleton(143 ^ [])))],extension(145 ^ 3)).
% 0.33/1.38 ncf('1.1.2.2',plain,[singleton(142 ^ []) = empty_set],extension(115 ^ 3,bind([[_23761], [142 ^ []]]))).
% 0.33/1.38 %-----------------------------------------------------
% 0.33/1.38 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------