%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : SET616+3 : TPTP v8.1.2. Released v2.2.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 11:56:08 EDT 2023
% Result : Theorem 24.87s 25.16s
% Output : Proof 24.87s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12 % Problem : SET616+3 : TPTP v8.1.2. Released v2.2.0.
% 0.06/0.12 % Command : nanocop.sh %s %d
% 0.12/0.33 % Computer : n028.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 19:31:18 EDT 2023
% 0.12/0.33 % CPUTime :
% 24.87/25.16
% 24.87/25.16 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 24.87/25.16 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 24.87/25.16 %-----------------------------------------------------
% 24.87/25.16 ncf(matrix, plain, [(163 ^ _24944) ^ [] : [-(difference(160 ^ [], 161 ^ []) = difference(161 ^ [], 160 ^ []))], (165 ^ _24944) ^ [] : [160 ^ [] = 161 ^ []], (48 ^ _24944) ^ [_26596, _26598, _26600, _26602] : [-(difference(_26602, _26598) = difference(_26600, _26596)), _26602 = _26600, _26598 = _26596], (2 ^ _24944) ^ [_25088] : [-(_25088 = _25088)], (4 ^ _24944) ^ [_25195, _25197] : [_25197 = _25195, -(_25195 = _25197)], (10 ^ _24944) ^ [_25399, _25401, _25403] : [-(_25403 = _25399), _25403 = _25401, _25401 = _25399], (20 ^ _24944) ^ [_25740, _25742, _25744, _25746] : [-(member(_25744, _25740)), member(_25746, _25742), _25746 = _25744, _25742 = _25740], (34 ^ _24944) ^ [_26164, _26166, _26168, _26170] : [-(subset(_26168, _26164)), subset(_26170, _26166), _26170 = _26168, _26166 = _26164], (58 ^ _24944) ^ [_26929, _26931] : [-(_26931 = _26929), 62 ^ _24944 : [(63 ^ _24944) ^ [] : [-(member(59 ^ [_26929, _26931], _26931))], (65 ^ _24944) ^ [] : [member(59 ^ [_26929, _26931], _26929)]], 66 ^ _24944 : [(67 ^ _24944) ^ [] : [-(member(59 ^ [_26929, _26931], _26929))], (69 ^ _24944) ^ [] : [member(59 ^ [_26929, _26931], _26931)]]], (73 ^ _24944) ^ [_27502, _27504, _27506] : [member(_27502, difference(_27506, _27504)), 76 ^ _24944 : [(77 ^ _24944) ^ [] : [-(member(_27502, _27506))], (79 ^ _24944) ^ [] : [member(_27502, _27504)]]], (81 ^ _24944) ^ [_27754, _27756, _27758] : [-(member(_27754, difference(_27758, _27756))), member(_27754, _27758), -(member(_27754, _27756))], (91 ^ _24944) ^ [_28103, _28105] : [_28105 = _28103, 94 ^ _24944 : [(95 ^ _24944) ^ [] : [-(subset(_28105, _28103))], (97 ^ _24944) ^ [] : [-(subset(_28103, _28105))]]], (99 ^ _24944) ^ [_28340, _28342] : [-(_28342 = _28340), subset(_28342, _28340), subset(_28340, _28342)], (159 ^ _24944) ^ [_30370] : [-(subset(_30370, _30370))], (150 ^ _24944) ^ [_30062, _30064] : [152 ^ _24944 : [(153 ^ _24944) ^ [] : [-(member(151 ^ [_30062, _30064], _30064))], (155 ^ _24944) ^ [] : [member(151 ^ [_30062, _30064], _30062)]], -(subset(_30064, _30062))], (140 ^ _24944) ^ [_29748, _29750] : [subset(_29750, _29748), 143 ^ _24944 : [(144 ^ _24944) ^ [_29885] : [member(_29885, _29750), -(member(_29885, _29748))]]], (125 ^ _24944) ^ [_29187, _29189] : [-(_29189 = _29187), 129 ^ _24944 : [(130 ^ _24944) ^ [] : [-(member(126 ^ [_29187, _29189], _29189))], (132 ^ _24944) ^ [] : [member(126 ^ [_29187, _29189], _29187)]], 133 ^ _24944 : [(134 ^ _24944) ^ [] : [-(member(126 ^ [_29187, _29189], _29187))], (136 ^ _24944) ^ [] : [member(126 ^ [_29187, _29189], _29189)]]], (109 ^ _24944) ^ [_28670, _28672] : [_28672 = _28670, 112 ^ _24944 : [(113 ^ _24944) ^ [_28836] : [member(_28836, _28672), -(member(_28836, _28670))], (119 ^ _24944) ^ [_29008] : [member(_29008, _28670), -(member(_29008, _28672))]]]], input).
% 24.87/25.16 ncf('1',plain,[member(59 ^ [161 ^ [], 160 ^ []], difference(161 ^ [], 160 ^ [])), 79 : member(59 ^ [161 ^ [], 160 ^ []], 160 ^ [])],start(73 ^ 0,bind([[_27502, _27504, _27506], [59 ^ [161 ^ [], 160 ^ []], 160 ^ [], 161 ^ []]]))).
% 24.87/25.16 ncf('1.1',plain,[-(member(59 ^ [161 ^ [], 160 ^ []], difference(161 ^ [], 160 ^ []))), member(59 ^ [161 ^ [], 160 ^ []], 161 ^ []), -(member(59 ^ [161 ^ [], 160 ^ []], 160 ^ []))],extension(81 ^ 1,bind([[_27754, _27756, _27758], [59 ^ [161 ^ [], 160 ^ []], 160 ^ [], 161 ^ []]]))).
% 24.87/25.16 ncf('1.1.1',plain,[-(member(59 ^ [161 ^ [], 160 ^ []], 161 ^ [])), -(member(59 ^ [161 ^ [], 160 ^ []], difference(160 ^ [], 161 ^ []))), member(59 ^ [161 ^ [], 160 ^ []], 160 ^ [])],extension(81 ^ 2,bind([[_27754, _27756, _27758], [59 ^ [161 ^ [], 160 ^ []], 161 ^ [], 160 ^ []]]))).
% 24.87/25.16 ncf('1.1.1.1',plain,[member(59 ^ [161 ^ [], 160 ^ []], difference(160 ^ [], 161 ^ [])), 113 : -(member(59 ^ [161 ^ [], 160 ^ []], difference(161 ^ [], 160 ^ []))), 113 : difference(160 ^ [], 161 ^ []) = difference(161 ^ [], 160 ^ [])],extension(109 ^ 3,bind([[_28670, _28672, _28836], [difference(161 ^ [], 160 ^ []), difference(160 ^ [], 161 ^ []), 59 ^ [161 ^ [], 160 ^ []]]]))).
% 24.87/25.16 ncf('1.1.1.1.1',plain,[member(59 ^ [161 ^ [], 160 ^ []], difference(161 ^ [], 160 ^ []))],reduction('1')).
% 24.87/25.16 ncf('1.1.1.1.2',plain,[-(difference(160 ^ [], 161 ^ []) = difference(161 ^ [], 160 ^ []))],extension(163 ^ 4)).
% 24.87/25.16 ncf('1.1.1.2',plain,[-(member(59 ^ [161 ^ [], 160 ^ []], 160 ^ [])), -(160 ^ [] = 161 ^ []), 67 : -(member(59 ^ [161 ^ [], 160 ^ []], 161 ^ []))],extension(58 ^ 3,bind([[_26929, _26931], [161 ^ [], 160 ^ []]]))).
% 24.87/25.16 ncf('1.1.1.2.1',plain,[160 ^ [] = 161 ^ []],extension(165 ^ 4)).
% 24.87/25.16 ncf('1.1.1.2.2',plain,[member(59 ^ [161 ^ [], 160 ^ []], 161 ^ [])],reduction('1.1')).
% 24.87/25.16 ncf('1.1.2',plain,[member(59 ^ [161 ^ [], 160 ^ []], 160 ^ []), -(member(59 ^ [161 ^ [], 160 ^ []], 161 ^ [])), 59 ^ [161 ^ [], 160 ^ []] = 59 ^ [161 ^ [], 160 ^ []], 160 ^ [] = 161 ^ []],extension(20 ^ 2,bind([[_25740, _25742, _25744, _25746], [161 ^ [], 160 ^ [], 59 ^ [161 ^ [], 160 ^ []], 59 ^ [161 ^ [], 160 ^ []]]]))).
% 24.87/25.16 ncf('1.1.2.1',plain,[member(59 ^ [161 ^ [], 160 ^ []], 161 ^ []), -(160 ^ [] = 161 ^ []), 69 : member(59 ^ [161 ^ [], 160 ^ []], 160 ^ [])],extension(58 ^ 3,bind([[_26929, _26931], [161 ^ [], 160 ^ []]]))).
% 24.87/25.16 ncf('1.1.2.1.1',plain,[160 ^ [] = 161 ^ []],extension(165 ^ 4)).
% 24.87/25.16 ncf('1.1.2.1.2',plain,[-(member(59 ^ [161 ^ [], 160 ^ []], 160 ^ []))],reduction('1.1')).
% 24.87/25.16 ncf('1.1.2.2',plain,[-(59 ^ [161 ^ [], 160 ^ []] = 59 ^ [161 ^ [], 160 ^ []])],extension(2 ^ 3,bind([[_25088], [59 ^ [161 ^ [], 160 ^ []]]]))).
% 24.87/25.16 ncf('1.1.2.3',plain,[-(160 ^ [] = 161 ^ []), 65 : member(59 ^ [161 ^ [], 160 ^ []], 161 ^ []), 67 : -(member(59 ^ [161 ^ [], 160 ^ []], 161 ^ []))],extension(58 ^ 3,bind([[_26929, _26931], [161 ^ [], 160 ^ []]]))).
% 24.87/25.16 ncf('1.1.2.3.1',plain,[-(member(59 ^ [161 ^ [], 160 ^ []], 161 ^ []))],lemmata('[1].x')).
% 24.87/25.16 ncf('1.1.2.3.2',plain,[member(59 ^ [161 ^ [], 160 ^ []], 161 ^ [])],lemmata('[1, 1].x')).
% 24.87/25.16 ncf('1.2',plain,[-(member(59 ^ [161 ^ [], 160 ^ []], 160 ^ [])), -(member(59 ^ [161 ^ [], 160 ^ []], difference(161 ^ [], 160 ^ []))), member(59 ^ [161 ^ [], 160 ^ []], 161 ^ [])],extension(81 ^ 3,bind([[_27754, _27756, _27758], [59 ^ [161 ^ [], 160 ^ []], 160 ^ [], 161 ^ []]]))).
% 24.87/25.16 ncf('1.2.1',plain,[member(59 ^ [161 ^ [], 160 ^ []], difference(161 ^ [], 160 ^ [])), -(member(59 ^ [161 ^ [], 160 ^ []], difference(160 ^ [], 161 ^ []))), 59 ^ [161 ^ [], 160 ^ []] = 59 ^ [161 ^ [], 160 ^ []], difference(161 ^ [], 160 ^ []) = difference(160 ^ [], 161 ^ [])],extension(20 ^ 4,bind([[_25740, _25742, _25744, _25746], [difference(160 ^ [], 161 ^ []), difference(161 ^ [], 160 ^ []), 59 ^ [161 ^ [], 160 ^ []], 59 ^ [161 ^ [], 160 ^ []]]]))).
% 24.87/25.16 ncf('1.2.1.1',plain,[member(59 ^ [161 ^ [], 160 ^ []], difference(160 ^ [], 161 ^ [])), 77 : -(member(59 ^ [161 ^ [], 160 ^ []], 160 ^ []))],extension(73 ^ 5,bind([[_27502, _27504, _27506], [59 ^ [161 ^ [], 160 ^ []], 161 ^ [], 160 ^ []]]))).
% 24.87/25.16 ncf('1.2.1.1.1',plain,[member(59 ^ [161 ^ [], 160 ^ []], 160 ^ [])],reduction('1')).
% 24.87/25.16 ncf('1.2.1.2',plain,[-(59 ^ [161 ^ [], 160 ^ []] = 59 ^ [161 ^ [], 160 ^ []])],extension(2 ^ 5,bind([[_25088], [59 ^ [161 ^ [], 160 ^ []]]]))).
% 24.87/25.16 ncf('1.2.1.3',plain,[-(difference(161 ^ [], 160 ^ []) = difference(160 ^ [], 161 ^ [])), difference(160 ^ [], 161 ^ []) = difference(161 ^ [], 160 ^ [])],extension(4 ^ 5,bind([[_25195, _25197], [difference(161 ^ [], 160 ^ []), difference(160 ^ [], 161 ^ [])]]))).
% 24.87/25.16 ncf('1.2.1.3.1',plain,[-(difference(160 ^ [], 161 ^ []) = difference(161 ^ [], 160 ^ []))],extension(163 ^ 6)).
% 24.87/25.16 ncf('1.2.2',plain,[-(member(59 ^ [161 ^ [], 160 ^ []], 161 ^ [])), member(59 ^ [161 ^ [], 160 ^ []], 160 ^ []), 59 ^ [161 ^ [], 160 ^ []] = 59 ^ [161 ^ [], 160 ^ []], 160 ^ [] = 161 ^ []],extension(20 ^ 4,bind([[_25740, _25742, _25744, _25746], [161 ^ [], 160 ^ [], 59 ^ [161 ^ [], 160 ^ []], 59 ^ [161 ^ [], 160 ^ []]]]))).
% 24.87/25.16 ncf('1.2.2.1',plain,[-(member(59 ^ [161 ^ [], 160 ^ []], 160 ^ [])), -(160 ^ [] = 161 ^ []), 67 : -(member(59 ^ [161 ^ [], 160 ^ []], 161 ^ []))],extension(58 ^ 5,bind([[_26929, _26931], [161 ^ [], 160 ^ []]]))).
% 24.87/25.16 ncf('1.2.2.1.1',plain,[160 ^ [] = 161 ^ []],extension(165 ^ 6)).
% 24.87/25.16 ncf('1.2.2.1.2',plain,[member(59 ^ [161 ^ [], 160 ^ []], 161 ^ [])],reduction('1.2')).
% 24.87/25.16 ncf('1.2.2.2',plain,[-(59 ^ [161 ^ [], 160 ^ []] = 59 ^ [161 ^ [], 160 ^ []])],extension(2 ^ 5,bind([[_25088], [59 ^ [161 ^ [], 160 ^ []]]]))).
% 24.87/25.16 ncf('1.2.2.3',plain,[-(160 ^ [] = 161 ^ []), 63 : -(member(59 ^ [161 ^ [], 160 ^ []], 160 ^ [])), 67 : -(member(59 ^ [161 ^ [], 160 ^ []], 161 ^ []))],extension(58 ^ 5,bind([[_26929, _26931], [161 ^ [], 160 ^ []]]))).
% 24.87/25.16 ncf('1.2.2.3.1',plain,[member(59 ^ [161 ^ [], 160 ^ []], 160 ^ [])],reduction('1')).
% 24.87/25.16 ncf('1.2.2.3.2',plain,[member(59 ^ [161 ^ [], 160 ^ []], 161 ^ [])],reduction('1.2')).
% 24.87/25.16 %-----------------------------------------------------
% 24.87/25.16 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------