%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : SET615+3 : TPTP v8.1.2. Released v2.2.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 11:56:08 EDT 2023
% Result : Theorem 4.06s 4.47s
% Output : Proof 4.06s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.11 % Problem : SET615+3 : TPTP v8.1.2. Released v2.2.0.
% 0.07/0.12 % Command : nanocop.sh %s %d
% 0.12/0.33 % Computer : n025.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:30:33 EDT 2023
% 0.12/0.33 % CPUTime :
% 4.06/4.47
% 4.06/4.47 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 4.06/4.47 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 4.06/4.47 %-----------------------------------------------------
% 4.06/4.47 ncf(matrix, plain, [(179 ^ _32828) ^ [] : [difference(union(175 ^ [], 176 ^ []), 177 ^ []) = union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ []))], (48 ^ _32828) ^ [_34500, _34502, _34504, _34506] : [-(union(_34506, _34502) = union(_34504, _34500)), _34506 = _34504, _34502 = _34500], (58 ^ _32828) ^ [_34839, _34841, _34843, _34845] : [-(difference(_34845, _34841) = difference(_34843, _34839)), _34845 = _34843, _34841 = _34839], (2 ^ _32828) ^ [_32972] : [-(_32972 = _32972)], (4 ^ _32828) ^ [_33079, _33081] : [_33081 = _33079, -(_33079 = _33081)], (10 ^ _32828) ^ [_33283, _33285, _33287] : [-(_33287 = _33283), _33287 = _33285, _33285 = _33283], (20 ^ _32828) ^ [_33624, _33626, _33628, _33630] : [-(subset(_33628, _33624)), subset(_33630, _33626), _33630 = _33628, _33626 = _33624], (34 ^ _32828) ^ [_34048, _34050, _34052, _34054] : [-(member(_34052, _34048)), member(_34054, _34050), _34054 = _34052, _34050 = _34048], (78 ^ _32828) ^ [_35487, _35489, _35491] : [79 ^ _32828 : [(80 ^ _32828) ^ [] : [member(_35487, _35491)], (82 ^ _32828) ^ [] : [member(_35487, _35489)]], -(member(_35487, union(_35491, _35489)))], (68 ^ _32828) ^ [_35219, _35221, _35223] : [member(_35219, union(_35223, _35221)), -(member(_35219, _35223)), -(member(_35219, _35221))], (86 ^ _32828) ^ [_35830, _35832, _35834] : [member(_35830, difference(_35834, _35832)), 89 ^ _32828 : [(90 ^ _32828) ^ [] : [-(member(_35830, _35834))], (92 ^ _32828) ^ [] : [member(_35830, _35832)]]], (94 ^ _32828) ^ [_36082, _36084, _36086] : [-(member(_36082, difference(_36086, _36084))), member(_36082, _36086), -(member(_36082, _36084))], (104 ^ _32828) ^ [_36431, _36433] : [_36433 = _36431, 107 ^ _32828 : [(108 ^ _32828) ^ [] : [-(subset(_36433, _36431))], (110 ^ _32828) ^ [] : [-(subset(_36431, _36433))]]], (112 ^ _32828) ^ [_36668, _36670] : [-(_36670 = _36668), subset(_36670, _36668), subset(_36668, _36670)], (122 ^ _32828) ^ [_36954, _36956] : [-(union(_36956, _36954) = union(_36954, _36956))], (134 ^ _32828) ^ [_37412, _37414] : [136 ^ _32828 : [(137 ^ _32828) ^ [] : [-(member(135 ^ [_37412, _37414], _37414))], (139 ^ _32828) ^ [] : [member(135 ^ [_37412, _37414], _37412)]], -(subset(_37414, _37412))], (124 ^ _32828) ^ [_37098, _37100] : [subset(_37100, _37098), 127 ^ _32828 : [(128 ^ _32828) ^ [_37235] : [member(_37235, _37100), -(member(_37235, _37098))]]], (143 ^ _32828) ^ [_37740] : [-(subset(_37740, _37740))], (161 ^ _32828) ^ [_38373, _38375] : [-(_38375 = _38373), 165 ^ _32828 : [(166 ^ _32828) ^ [] : [-(member(162 ^ [_38373, _38375], _38375))], (168 ^ _32828) ^ [] : [member(162 ^ [_38373, _38375], _38373)]], 169 ^ _32828 : [(170 ^ _32828) ^ [] : [-(member(162 ^ [_38373, _38375], _38373))], (172 ^ _32828) ^ [] : [member(162 ^ [_38373, _38375], _38375)]]], (145 ^ _32828) ^ [_37856, _37858] : [_37858 = _37856, 148 ^ _32828 : [(149 ^ _32828) ^ [_38022] : [member(_38022, _37858), -(member(_38022, _37856))], (155 ^ _32828) ^ [_38194] : [member(_38194, _37856), -(member(_38194, _37858))]]]], input).
% 4.06/4.47 ncf('1',plain,[member(162 ^ [union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])), difference(union(175 ^ [], 176 ^ []), 177 ^ [])], difference(union(175 ^ [], 176 ^ []), 177 ^ [])), 92 : member(162 ^ [union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])), difference(union(175 ^ [], 176 ^ []), 177 ^ [])], 177 ^ [])],start(86 ^ 0,bind([[_35830, _35832, _35834], [162 ^ [union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])), difference(union(175 ^ [], 176 ^ []), 177 ^ [])], 177 ^ [], union(175 ^ [], 176 ^ [])]]))).
% 4.06/4.47 ncf('1.1',plain,[-(member(162 ^ [union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])), difference(union(175 ^ [], 176 ^ []), 177 ^ [])], difference(union(175 ^ [], 176 ^ []), 177 ^ []))), member(162 ^ [union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])), difference(union(175 ^ [], 176 ^ []), 177 ^ [])], union(difference(union(175 ^ [], 176 ^ []), 177 ^ []), union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])))), -(member(162 ^ [union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])), difference(union(175 ^ [], 176 ^ []), 177 ^ [])], union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ []))))],extension(68 ^ 1,bind([[_35219, _35221, _35223], [162 ^ [union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])), difference(union(175 ^ [], 176 ^ []), 177 ^ [])], union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])), difference(union(175 ^ [], 176 ^ []), 177 ^ [])]]))).
% 4.06/4.47 ncf('1.1.1',plain,[-(member(162 ^ [union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])), difference(union(175 ^ [], 176 ^ []), 177 ^ [])], union(difference(union(175 ^ [], 176 ^ []), 177 ^ []), union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ []))))), 82 : member(162 ^ [union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])), difference(union(175 ^ [], 176 ^ []), 177 ^ [])], union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])))],extension(78 ^ 2,bind([[_35487, _35489, _35491], [162 ^ [union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])), difference(union(175 ^ [], 176 ^ []), 177 ^ [])], union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])), difference(union(175 ^ [], 176 ^ []), 177 ^ [])]]))).
% 4.06/4.47 ncf('1.1.1.1',plain,[-(member(162 ^ [union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])), difference(union(175 ^ [], 176 ^ []), 177 ^ [])], union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])))), member(162 ^ [union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])), difference(union(175 ^ [], 176 ^ []), 177 ^ [])], difference(union(175 ^ [], 176 ^ []), 177 ^ [])), 162 ^ [union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])), difference(union(175 ^ [], 176 ^ []), 177 ^ [])] = 162 ^ [union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])), difference(union(175 ^ [], 176 ^ []), 177 ^ [])], difference(union(175 ^ [], 176 ^ []), 177 ^ []) = union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ []))],extension(34 ^ 5,bind([[_34048, _34050, _34052, _34054], [union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])), difference(union(175 ^ [], 176 ^ []), 177 ^ []), 162 ^ [union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])), difference(union(175 ^ [], 176 ^ []), 177 ^ [])], 162 ^ [union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])), difference(union(175 ^ [], 176 ^ []), 177 ^ [])]]]))).
% 4.06/4.47 ncf('1.1.1.1.1',plain,[-(member(162 ^ [union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])), difference(union(175 ^ [], 176 ^ []), 177 ^ [])], difference(union(175 ^ [], 176 ^ []), 177 ^ []))), member(162 ^ [union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])), difference(union(175 ^ [], 176 ^ []), 177 ^ [])], union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ []))), 162 ^ [union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])), difference(union(175 ^ [], 176 ^ []), 177 ^ [])] = 162 ^ [union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])), difference(union(175 ^ [], 176 ^ []), 177 ^ [])], union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])) = difference(union(175 ^ [], 176 ^ []), 177 ^ [])],extension(34 ^ 6,bind([[_34048, _34050, _34052, _34054], [difference(union(175 ^ [], 176 ^ []), 177 ^ []), union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])), 162 ^ [union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])), difference(union(175 ^ [], 176 ^ []), 177 ^ [])], 162 ^ [union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])), difference(union(175 ^ [], 176 ^ []), 177 ^ [])]]]))).
% 4.06/4.47 ncf('1.1.1.1.1.1',plain,[-(member(162 ^ [union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])), difference(union(175 ^ [], 176 ^ []), 177 ^ [])], union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])))), member(162 ^ [union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])), difference(union(175 ^ [], 176 ^ []), 177 ^ [])], difference(union(175 ^ [], 176 ^ []), 177 ^ [])), 162 ^ [union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])), difference(union(175 ^ [], 176 ^ []), 177 ^ [])] = 162 ^ [union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])), difference(union(175 ^ [], 176 ^ []), 177 ^ [])], difference(union(175 ^ [], 176 ^ []), 177 ^ []) = union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ []))],extension(34 ^ 7,bind([[_34048, _34050, _34052, _34054], [union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])), difference(union(175 ^ [], 176 ^ []), 177 ^ []), 162 ^ [union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])), difference(union(175 ^ [], 176 ^ []), 177 ^ [])], 162 ^ [union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])), difference(union(175 ^ [], 176 ^ []), 177 ^ [])]]]))).
% 4.06/4.47 ncf('1.1.1.1.1.1.1',plain,[-(member(162 ^ [union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])), difference(union(175 ^ [], 176 ^ []), 177 ^ [])], difference(union(175 ^ [], 176 ^ []), 177 ^ []))), -(difference(union(175 ^ [], 176 ^ []), 177 ^ []) = union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ []))), 170 : -(member(162 ^ [union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])), difference(union(175 ^ [], 176 ^ []), 177 ^ [])], union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ []))))],extension(161 ^ 8,bind([[_38373, _38375], [union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])), difference(union(175 ^ [], 176 ^ []), 177 ^ [])]]))).
% 4.06/4.47 ncf('1.1.1.1.1.1.1.1',plain,[difference(union(175 ^ [], 176 ^ []), 177 ^ []) = union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ []))],extension(179 ^ 9)).
% 4.06/4.47 ncf('1.1.1.1.1.1.1.2',plain,[member(162 ^ [union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])), difference(union(175 ^ [], 176 ^ []), 177 ^ [])], union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])))],reduction('1.1.1.1.1')).
% 4.06/4.47 ncf('1.1.1.1.1.1.2',plain,[-(162 ^ [union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])), difference(union(175 ^ [], 176 ^ []), 177 ^ [])] = 162 ^ [union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])), difference(union(175 ^ [], 176 ^ []), 177 ^ [])])],extension(2 ^ 8,bind([[_32972], [162 ^ [union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])), difference(union(175 ^ [], 176 ^ []), 177 ^ [])]]]))).
% 4.06/4.47 ncf('1.1.1.1.1.1.3',plain,[-(difference(union(175 ^ [], 176 ^ []), 177 ^ []) = union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ []))), 166 : -(member(162 ^ [union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])), difference(union(175 ^ [], 176 ^ []), 177 ^ [])], difference(union(175 ^ [], 176 ^ []), 177 ^ []))), 170 : -(member(162 ^ [union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])), difference(union(175 ^ [], 176 ^ []), 177 ^ [])], union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ []))))],extension(161 ^ 8,bind([[_38373, _38375], [union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])), difference(union(175 ^ [], 176 ^ []), 177 ^ [])]]))).
% 4.06/4.47 ncf('1.1.1.1.1.1.3.1',plain,[member(162 ^ [union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])), difference(union(175 ^ [], 176 ^ []), 177 ^ [])], difference(union(175 ^ [], 176 ^ []), 177 ^ []))],reduction('1.1.1.1')).
% 4.06/4.47 ncf('1.1.1.1.1.1.3.2',plain,[member(162 ^ [union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])), difference(union(175 ^ [], 176 ^ []), 177 ^ [])], union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])))],reduction('1.1.1.1.1')).
% 4.06/4.47 ncf('1.1.1.1.1.2',plain,[-(162 ^ [union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])), difference(union(175 ^ [], 176 ^ []), 177 ^ [])] = 162 ^ [union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])), difference(union(175 ^ [], 176 ^ []), 177 ^ [])])],extension(2 ^ 7,bind([[_32972], [162 ^ [union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])), difference(union(175 ^ [], 176 ^ []), 177 ^ [])]]]))).
% 4.06/4.47 ncf('1.1.1.1.1.3',plain,[-(union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])) = difference(union(175 ^ [], 176 ^ []), 177 ^ [])), difference(union(175 ^ [], 176 ^ []), 177 ^ []) = union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ []))],extension(4 ^ 7,bind([[_33079, _33081], [union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])), difference(union(175 ^ [], 176 ^ []), 177 ^ [])]]))).
% 4.06/4.47 ncf('1.1.1.1.1.3.1',plain,[-(difference(union(175 ^ [], 176 ^ []), 177 ^ []) = union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ []))), 166 : -(member(162 ^ [union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])), difference(union(175 ^ [], 176 ^ []), 177 ^ [])], difference(union(175 ^ [], 176 ^ []), 177 ^ []))), 170 : -(member(162 ^ [union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])), difference(union(175 ^ [], 176 ^ []), 177 ^ [])], union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ []))))],extension(161 ^ 8,bind([[_38373, _38375], [union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])), difference(union(175 ^ [], 176 ^ []), 177 ^ [])]]))).
% 4.06/4.47 ncf('1.1.1.1.1.3.1.1',plain,[member(162 ^ [union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])), difference(union(175 ^ [], 176 ^ []), 177 ^ [])], difference(union(175 ^ [], 176 ^ []), 177 ^ []))],reduction('1.1.1.1')).
% 4.06/4.47 ncf('1.1.1.1.1.3.1.2',plain,[member(162 ^ [union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])), difference(union(175 ^ [], 176 ^ []), 177 ^ [])], union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])))],reduction('1.1.1')).
% 4.06/4.47 ncf('1.1.1.1.2',plain,[-(162 ^ [union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])), difference(union(175 ^ [], 176 ^ []), 177 ^ [])] = 162 ^ [union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])), difference(union(175 ^ [], 176 ^ []), 177 ^ [])])],extension(2 ^ 6,bind([[_32972], [162 ^ [union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])), difference(union(175 ^ [], 176 ^ []), 177 ^ [])]]]))).
% 4.06/4.47 ncf('1.1.1.1.3',plain,[-(difference(union(175 ^ [], 176 ^ []), 177 ^ []) = union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ []))), 166 : -(member(162 ^ [union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])), difference(union(175 ^ [], 176 ^ []), 177 ^ [])], difference(union(175 ^ [], 176 ^ []), 177 ^ []))), 170 : -(member(162 ^ [union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])), difference(union(175 ^ [], 176 ^ []), 177 ^ [])], union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ []))))],extension(161 ^ 6,bind([[_38373, _38375], [union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])), difference(union(175 ^ [], 176 ^ []), 177 ^ [])]]))).
% 4.06/4.47 ncf('1.1.1.1.3.1',plain,[member(162 ^ [union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])), difference(union(175 ^ [], 176 ^ []), 177 ^ [])], difference(union(175 ^ [], 176 ^ []), 177 ^ []))],reduction('1')).
% 4.06/4.47 ncf('1.1.1.1.3.2',plain,[member(162 ^ [union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])), difference(union(175 ^ [], 176 ^ []), 177 ^ [])], union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])))],reduction('1.1.1')).
% 4.06/4.47 ncf('1.1.2',plain,[member(162 ^ [union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])), difference(union(175 ^ [], 176 ^ []), 177 ^ [])], union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ []))), -(member(162 ^ [union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])), difference(union(175 ^ [], 176 ^ []), 177 ^ [])], difference(175 ^ [], 177 ^ []))), -(member(162 ^ [union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])), difference(union(175 ^ [], 176 ^ []), 177 ^ [])], difference(176 ^ [], 177 ^ [])))],extension(68 ^ 2,bind([[_35219, _35221, _35223], [162 ^ [union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])), difference(union(175 ^ [], 176 ^ []), 177 ^ [])], difference(176 ^ [], 177 ^ []), difference(175 ^ [], 177 ^ [])]]))).
% 4.06/4.47 ncf('1.1.2.1',plain,[member(162 ^ [union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])), difference(union(175 ^ [], 176 ^ []), 177 ^ [])], difference(175 ^ [], 177 ^ [])), 90 : -(member(162 ^ [union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])), difference(union(175 ^ [], 176 ^ []), 177 ^ [])], 175 ^ []))],extension(86 ^ 3,bind([[_35830, _35832, _35834], [162 ^ [union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])), difference(union(175 ^ [], 176 ^ []), 177 ^ [])], 177 ^ [], 175 ^ []]]))).
% 4.06/4.47 ncf('1.1.2.1.1',plain,[member(162 ^ [union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])), difference(union(175 ^ [], 176 ^ []), 177 ^ [])], 175 ^ []), -(member(162 ^ [union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])), difference(union(175 ^ [], 176 ^ []), 177 ^ [])], union(175 ^ [], 176 ^ [])))],extension(78 ^ 6,bind([[_35487, _35489, _35491], [162 ^ [union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])), difference(union(175 ^ [], 176 ^ []), 177 ^ [])], 176 ^ [], 175 ^ []]]))).
% 4.06/4.47 ncf('1.1.2.1.1.1',plain,[member(162 ^ [union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])), difference(union(175 ^ [], 176 ^ []), 177 ^ [])], union(175 ^ [], 176 ^ [])), -(member(162 ^ [union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])), difference(union(175 ^ [], 176 ^ []), 177 ^ [])], difference(union(175 ^ [], 176 ^ []), 177 ^ []))), -(member(162 ^ [union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])), difference(union(175 ^ [], 176 ^ []), 177 ^ [])], 177 ^ []))],extension(94 ^ 7,bind([[_36082, _36084, _36086], [162 ^ [union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])), difference(union(175 ^ [], 176 ^ []), 177 ^ [])], 177 ^ [], union(175 ^ [], 176 ^ [])]]))).
% 4.06/4.47 ncf('1.1.2.1.1.1.1',plain,[member(162 ^ [union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])), difference(union(175 ^ [], 176 ^ []), 177 ^ [])], difference(union(175 ^ [], 176 ^ []), 177 ^ []))],reduction('1')).
% 4.06/4.47 ncf('1.1.2.1.1.1.2',plain,[member(162 ^ [union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])), difference(union(175 ^ [], 176 ^ []), 177 ^ [])], 177 ^ [])],extension(92 ^ 8)).
% 4.06/4.47 ncf('1.1.2.2',plain,[member(162 ^ [union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])), difference(union(175 ^ [], 176 ^ []), 177 ^ [])], difference(176 ^ [], 177 ^ [])), 90 : -(member(162 ^ [union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])), difference(union(175 ^ [], 176 ^ []), 177 ^ [])], 176 ^ []))],extension(86 ^ 3,bind([[_35830, _35832, _35834], [162 ^ [union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])), difference(union(175 ^ [], 176 ^ []), 177 ^ [])], 177 ^ [], 176 ^ []]]))).
% 4.06/4.47 ncf('1.1.2.2.1',plain,[member(162 ^ [union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])), difference(union(175 ^ [], 176 ^ []), 177 ^ [])], 176 ^ []), -(member(162 ^ [union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])), difference(union(175 ^ [], 176 ^ []), 177 ^ [])], union(175 ^ [], 176 ^ [])))],extension(78 ^ 6,bind([[_35487, _35489, _35491], [162 ^ [union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])), difference(union(175 ^ [], 176 ^ []), 177 ^ [])], 176 ^ [], 175 ^ []]]))).
% 4.06/4.47 ncf('1.1.2.2.1.1',plain,[member(162 ^ [union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])), difference(union(175 ^ [], 176 ^ []), 177 ^ [])], union(175 ^ [], 176 ^ [])), -(member(162 ^ [union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])), difference(union(175 ^ [], 176 ^ []), 177 ^ [])], difference(union(175 ^ [], 176 ^ []), 177 ^ []))), -(member(162 ^ [union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])), difference(union(175 ^ [], 176 ^ []), 177 ^ [])], 177 ^ []))],extension(94 ^ 7,bind([[_36082, _36084, _36086], [162 ^ [union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])), difference(union(175 ^ [], 176 ^ []), 177 ^ [])], 177 ^ [], union(175 ^ [], 176 ^ [])]]))).
% 4.06/4.47 ncf('1.1.2.2.1.1.1',plain,[member(162 ^ [union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])), difference(union(175 ^ [], 176 ^ []), 177 ^ [])], difference(union(175 ^ [], 176 ^ []), 177 ^ []))],reduction('1')).
% 4.06/4.47 ncf('1.1.2.2.1.1.2',plain,[member(162 ^ [union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])), difference(union(175 ^ [], 176 ^ []), 177 ^ [])], 177 ^ [])],extension(92 ^ 8)).
% 4.06/4.47 ncf('1.2',plain,[-(member(162 ^ [union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])), difference(union(175 ^ [], 176 ^ []), 177 ^ [])], 177 ^ [])), member(162 ^ [union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])), difference(union(175 ^ [], 176 ^ []), 177 ^ [])], union(177 ^ [], union(175 ^ [], 176 ^ []))), -(member(162 ^ [union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])), difference(union(175 ^ [], 176 ^ []), 177 ^ [])], union(175 ^ [], 176 ^ [])))],extension(68 ^ 3,bind([[_35219, _35221, _35223], [162 ^ [union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])), difference(union(175 ^ [], 176 ^ []), 177 ^ [])], union(175 ^ [], 176 ^ []), 177 ^ []]]))).
% 4.06/4.47 ncf('1.2.1',plain,[-(member(162 ^ [union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])), difference(union(175 ^ [], 176 ^ []), 177 ^ [])], union(177 ^ [], union(175 ^ [], 176 ^ [])))), 82 : member(162 ^ [union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])), difference(union(175 ^ [], 176 ^ []), 177 ^ [])], union(175 ^ [], 176 ^ []))],extension(78 ^ 4,bind([[_35487, _35489, _35491], [162 ^ [union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])), difference(union(175 ^ [], 176 ^ []), 177 ^ [])], union(175 ^ [], 176 ^ []), 177 ^ []]]))).
% 4.06/4.47 ncf('1.2.1.1',plain,[-(member(162 ^ [union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])), difference(union(175 ^ [], 176 ^ []), 177 ^ [])], union(175 ^ [], 176 ^ []))), member(162 ^ [union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])), difference(union(175 ^ [], 176 ^ []), 177 ^ [])], union(175 ^ [], 176 ^ [])), 162 ^ [union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])), difference(union(175 ^ [], 176 ^ []), 177 ^ [])] = 162 ^ [union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])), difference(union(175 ^ [], 176 ^ []), 177 ^ [])], union(175 ^ [], 176 ^ []) = union(175 ^ [], 176 ^ [])],extension(34 ^ 7,bind([[_34048, _34050, _34052, _34054], [union(175 ^ [], 176 ^ []), union(175 ^ [], 176 ^ []), 162 ^ [union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])), difference(union(175 ^ [], 176 ^ []), 177 ^ [])], 162 ^ [union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])), difference(union(175 ^ [], 176 ^ []), 177 ^ [])]]]))).
% 4.06/4.47 ncf('1.2.1.1.1',plain,[-(member(162 ^ [union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])), difference(union(175 ^ [], 176 ^ []), 177 ^ [])], union(175 ^ [], 176 ^ []))), member(162 ^ [union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])), difference(union(175 ^ [], 176 ^ []), 177 ^ [])], union(175 ^ [], 176 ^ [])), 162 ^ [union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])), difference(union(175 ^ [], 176 ^ []), 177 ^ [])] = 162 ^ [union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])), difference(union(175 ^ [], 176 ^ []), 177 ^ [])], union(175 ^ [], 176 ^ []) = union(175 ^ [], 176 ^ [])],extension(34 ^ 8,bind([[_34048, _34050, _34052, _34054], [union(175 ^ [], 176 ^ []), union(175 ^ [], 176 ^ []), 162 ^ [union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])), difference(union(175 ^ [], 176 ^ []), 177 ^ [])], 162 ^ [union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])), difference(union(175 ^ [], 176 ^ []), 177 ^ [])]]]))).
% 4.06/4.47 ncf('1.2.1.1.1.1',plain,[-(member(162 ^ [union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])), difference(union(175 ^ [], 176 ^ []), 177 ^ [])], union(175 ^ [], 176 ^ []))), member(162 ^ [union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])), difference(union(175 ^ [], 176 ^ []), 177 ^ [])], union(175 ^ [], 176 ^ [])), 162 ^ [union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])), difference(union(175 ^ [], 176 ^ []), 177 ^ [])] = 162 ^ [union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])), difference(union(175 ^ [], 176 ^ []), 177 ^ [])], union(175 ^ [], 176 ^ []) = union(175 ^ [], 176 ^ [])],extension(34 ^ 9,bind([[_34048, _34050, _34052, _34054], [union(175 ^ [], 176 ^ []), union(175 ^ [], 176 ^ []), 162 ^ [union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])), difference(union(175 ^ [], 176 ^ []), 177 ^ [])], 162 ^ [union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])), difference(union(175 ^ [], 176 ^ []), 177 ^ [])]]]))).
% 4.06/4.47 ncf('1.2.1.1.1.1.1',plain,[-(member(162 ^ [union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])), difference(union(175 ^ [], 176 ^ []), 177 ^ [])], union(175 ^ [], 176 ^ [])))],extension(90 ^ 10)).
% 4.06/4.47 ncf('1.2.1.1.1.1.2',plain,[-(162 ^ [union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])), difference(union(175 ^ [], 176 ^ []), 177 ^ [])] = 162 ^ [union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])), difference(union(175 ^ [], 176 ^ []), 177 ^ [])])],extension(2 ^ 10,bind([[_32972], [162 ^ [union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])), difference(union(175 ^ [], 176 ^ []), 177 ^ [])]]]))).
% 4.06/4.47 ncf('1.2.1.1.1.1.3',plain,[-(union(175 ^ [], 176 ^ []) = union(175 ^ [], 176 ^ []))],extension(2 ^ 10,bind([[_32972], [union(175 ^ [], 176 ^ [])]]))).
% 4.06/4.47 ncf('1.2.1.1.1.2',plain,[-(162 ^ [union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])), difference(union(175 ^ [], 176 ^ []), 177 ^ [])] = 162 ^ [union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])), difference(union(175 ^ [], 176 ^ []), 177 ^ [])])],extension(2 ^ 9,bind([[_32972], [162 ^ [union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])), difference(union(175 ^ [], 176 ^ []), 177 ^ [])]]]))).
% 4.06/4.47 ncf('1.2.1.1.1.3',plain,[-(union(175 ^ [], 176 ^ []) = union(175 ^ [], 176 ^ [])), 175 ^ [] = 175 ^ [], 176 ^ [] = 176 ^ []],extension(48 ^ 9,bind([[_34500, _34502, _34504, _34506], [176 ^ [], 176 ^ [], 175 ^ [], 175 ^ []]]))).
% 4.06/4.47 ncf('1.2.1.1.1.3.1',plain,[-(175 ^ [] = 175 ^ [])],extension(2 ^ 10,bind([[_32972], [175 ^ []]]))).
% 4.06/4.47 ncf('1.2.1.1.1.3.2',plain,[-(176 ^ [] = 176 ^ [])],extension(2 ^ 10,bind([[_32972], [176 ^ []]]))).
% 4.06/4.47 ncf('1.2.1.1.2',plain,[-(162 ^ [union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])), difference(union(175 ^ [], 176 ^ []), 177 ^ [])] = 162 ^ [union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])), difference(union(175 ^ [], 176 ^ []), 177 ^ [])])],extension(2 ^ 8,bind([[_32972], [162 ^ [union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])), difference(union(175 ^ [], 176 ^ []), 177 ^ [])]]]))).
% 4.06/4.47 ncf('1.2.1.1.3',plain,[-(union(175 ^ [], 176 ^ []) = union(175 ^ [], 176 ^ [])), 175 ^ [] = 175 ^ [], 176 ^ [] = 176 ^ []],extension(48 ^ 8,bind([[_34500, _34502, _34504, _34506], [176 ^ [], 176 ^ [], 175 ^ [], 175 ^ []]]))).
% 4.06/4.47 ncf('1.2.1.1.3.1',plain,[-(175 ^ [] = 175 ^ [])],extension(2 ^ 9,bind([[_32972], [175 ^ []]]))).
% 4.06/4.47 ncf('1.2.1.1.3.2',plain,[-(176 ^ [] = 176 ^ [])],extension(2 ^ 9,bind([[_32972], [176 ^ []]]))).
% 4.06/4.47 ncf('1.2.2',plain,[member(162 ^ [union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])), difference(union(175 ^ [], 176 ^ []), 177 ^ [])], union(175 ^ [], 176 ^ [])), -(member(162 ^ [union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])), difference(union(175 ^ [], 176 ^ []), 177 ^ [])], 175 ^ [])), -(member(162 ^ [union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])), difference(union(175 ^ [], 176 ^ []), 177 ^ [])], 176 ^ []))],extension(68 ^ 4,bind([[_35219, _35221, _35223], [162 ^ [union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])), difference(union(175 ^ [], 176 ^ []), 177 ^ [])], 176 ^ [], 175 ^ []]]))).
% 4.06/4.47 ncf('1.2.2.1',plain,[member(162 ^ [union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])), difference(union(175 ^ [], 176 ^ []), 177 ^ [])], 175 ^ []), -(member(162 ^ [union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])), difference(union(175 ^ [], 176 ^ []), 177 ^ [])], difference(175 ^ [], 177 ^ []))), -(member(162 ^ [union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])), difference(union(175 ^ [], 176 ^ []), 177 ^ [])], 177 ^ []))],extension(94 ^ 5,bind([[_36082, _36084, _36086], [162 ^ [union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])), difference(union(175 ^ [], 176 ^ []), 177 ^ [])], 177 ^ [], 175 ^ []]]))).
% 4.06/4.47 ncf('1.2.2.1.1',plain,[member(162 ^ [union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])), difference(union(175 ^ [], 176 ^ []), 177 ^ [])], difference(175 ^ [], 177 ^ [])), -(member(162 ^ [union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])), difference(union(175 ^ [], 176 ^ []), 177 ^ [])], union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ []))))],extension(78 ^ 6,bind([[_35487, _35489, _35491], [162 ^ [union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])), difference(union(175 ^ [], 176 ^ []), 177 ^ [])], difference(176 ^ [], 177 ^ []), difference(175 ^ [], 177 ^ [])]]))).
% 4.06/4.47 ncf('1.2.2.1.1.1',plain,[member(162 ^ [union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])), difference(union(175 ^ [], 176 ^ []), 177 ^ [])], union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ []))), -(difference(union(175 ^ [], 176 ^ []), 177 ^ []) = union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ []))), 172 : member(162 ^ [union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])), difference(union(175 ^ [], 176 ^ []), 177 ^ [])], difference(union(175 ^ [], 176 ^ []), 177 ^ []))],extension(161 ^ 7,bind([[_38373, _38375], [union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])), difference(union(175 ^ [], 176 ^ []), 177 ^ [])]]))).
% 4.06/4.47 ncf('1.2.2.1.1.1.1',plain,[difference(union(175 ^ [], 176 ^ []), 177 ^ []) = union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ []))],extension(179 ^ 8)).
% 4.06/4.47 ncf('1.2.2.1.1.1.2',plain,[-(member(162 ^ [union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])), difference(union(175 ^ [], 176 ^ []), 177 ^ [])], difference(union(175 ^ [], 176 ^ []), 177 ^ [])))],lemmata('x')).
% 4.06/4.47 ncf('1.2.2.1.2',plain,[member(162 ^ [union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])), difference(union(175 ^ [], 176 ^ []), 177 ^ [])], 177 ^ [])],reduction('1')).
% 4.06/4.47 ncf('1.2.2.2',plain,[member(162 ^ [union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])), difference(union(175 ^ [], 176 ^ []), 177 ^ [])], 176 ^ []), -(member(162 ^ [union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])), difference(union(175 ^ [], 176 ^ []), 177 ^ [])], difference(176 ^ [], 177 ^ []))), -(member(162 ^ [union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])), difference(union(175 ^ [], 176 ^ []), 177 ^ [])], 177 ^ []))],extension(94 ^ 5,bind([[_36082, _36084, _36086], [162 ^ [union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])), difference(union(175 ^ [], 176 ^ []), 177 ^ [])], 177 ^ [], 176 ^ []]]))).
% 4.06/4.47 ncf('1.2.2.2.1',plain,[member(162 ^ [union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])), difference(union(175 ^ [], 176 ^ []), 177 ^ [])], difference(176 ^ [], 177 ^ [])), -(member(162 ^ [union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])), difference(union(175 ^ [], 176 ^ []), 177 ^ [])], union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ []))))],extension(78 ^ 6,bind([[_35487, _35489, _35491], [162 ^ [union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])), difference(union(175 ^ [], 176 ^ []), 177 ^ [])], difference(176 ^ [], 177 ^ []), difference(175 ^ [], 177 ^ [])]]))).
% 4.06/4.47 ncf('1.2.2.2.1.1',plain,[member(162 ^ [union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])), difference(union(175 ^ [], 176 ^ []), 177 ^ [])], union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ []))), -(difference(union(175 ^ [], 176 ^ []), 177 ^ []) = union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ []))), 172 : member(162 ^ [union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])), difference(union(175 ^ [], 176 ^ []), 177 ^ [])], difference(union(175 ^ [], 176 ^ []), 177 ^ []))],extension(161 ^ 7,bind([[_38373, _38375], [union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])), difference(union(175 ^ [], 176 ^ []), 177 ^ [])]]))).
% 4.06/4.47 ncf('1.2.2.2.1.1.1',plain,[difference(union(175 ^ [], 176 ^ []), 177 ^ []) = union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ []))],extension(179 ^ 8)).
% 4.06/4.47 ncf('1.2.2.2.1.1.2',plain,[-(member(162 ^ [union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])), difference(union(175 ^ [], 176 ^ []), 177 ^ [])], difference(union(175 ^ [], 176 ^ []), 177 ^ [])))],lemmata('x')).
% 4.06/4.47 ncf('1.2.2.2.2',plain,[member(162 ^ [union(difference(175 ^ [], 177 ^ []), difference(176 ^ [], 177 ^ [])), difference(union(175 ^ [], 176 ^ []), 177 ^ [])], 177 ^ [])],reduction('1')).
% 4.06/4.47 %-----------------------------------------------------
% 4.06/4.47 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------