%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : SET613+3 : TPTP v8.1.2. Released v2.2.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n002.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:07 EDT 2023
% Result : Theorem 7.14s 7.58s
% Output : Proof 7.14s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : SET613+3 : TPTP v8.1.2. Released v2.2.0.
% 0.03/0.12 % Command : nanocop.sh %s %d
% 0.12/0.33 % Computer : n002.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:11:49 EDT 2023
% 0.12/0.33 % CPUTime :
% 7.14/7.58
% 7.14/7.58 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 7.14/7.58 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 7.14/7.58 %-----------------------------------------------------
% 7.14/7.58 ncf(matrix, plain, [(223 ^ _36919) ^ [] : [difference(union(220 ^ [], 221 ^ []), intersection(220 ^ [], 221 ^ [])) = union(difference(220 ^ [], 221 ^ []), difference(221 ^ [], 220 ^ []))], (48 ^ _36919) ^ [_38591, _38593, _38595, _38597] : [-(intersection(_38597, _38593) = intersection(_38595, _38591)), _38597 = _38595, _38593 = _38591], (58 ^ _36919) ^ [_38950, _38952, _38954, _38956] : [-(union(_38956, _38952) = union(_38954, _38950)), _38956 = _38954, _38952 = _38950], (68 ^ _36919) ^ [_39289, _39291, _39293, _39295] : [-(difference(_39295, _39291) = difference(_39293, _39289)), _39295 = _39293, _39291 = _39289], (2 ^ _36919) ^ [_37063] : [-(_37063 = _37063)], (4 ^ _36919) ^ [_37170, _37172] : [_37172 = _37170, -(_37170 = _37172)], (10 ^ _36919) ^ [_37374, _37376, _37378] : [-(_37378 = _37374), _37378 = _37376, _37376 = _37374], (20 ^ _36919) ^ [_37715, _37717, _37719, _37721] : [-(member(_37719, _37715)), member(_37721, _37717), _37721 = _37719, _37717 = _37715], (34 ^ _36919) ^ [_38139, _38141, _38143, _38145] : [-(subset(_38143, _38139)), subset(_38145, _38141), _38145 = _38143, _38141 = _38139], (78 ^ _36919) ^ [_39630, _39632] : [-(_39632 = _39630), 82 ^ _36919 : [(83 ^ _36919) ^ [] : [-(member(79 ^ [_39630, _39632], _39632))], (85 ^ _36919) ^ [] : [member(79 ^ [_39630, _39632], _39630)]], 86 ^ _36919 : [(87 ^ _36919) ^ [] : [-(member(79 ^ [_39630, _39632], _39630))], (89 ^ _36919) ^ [] : [member(79 ^ [_39630, _39632], _39632)]]], (103 ^ _36919) ^ [_40471, _40473, _40475] : [104 ^ _36919 : [(105 ^ _36919) ^ [] : [member(_40471, _40475)], (107 ^ _36919) ^ [] : [member(_40471, _40473)]], -(member(_40471, union(_40475, _40473)))], (93 ^ _36919) ^ [_40203, _40205, _40207] : [member(_40203, union(_40207, _40205)), -(member(_40203, _40207)), -(member(_40203, _40205))], (111 ^ _36919) ^ [_40814, _40816, _40818] : [member(_40814, intersection(_40818, _40816)), 114 ^ _36919 : [(115 ^ _36919) ^ [] : [-(member(_40814, _40818))], (117 ^ _36919) ^ [] : [-(member(_40814, _40816))]]], (119 ^ _36919) ^ [_41065, _41067, _41069] : [-(member(_41065, intersection(_41069, _41067))), member(_41065, _41069), member(_41065, _41067)], (129 ^ _36919) ^ [_41425, _41427, _41429] : [member(_41425, difference(_41429, _41427)), 132 ^ _36919 : [(133 ^ _36919) ^ [] : [-(member(_41425, _41429))], (135 ^ _36919) ^ [] : [member(_41425, _41427)]]], (137 ^ _36919) ^ [_41677, _41679, _41681] : [-(member(_41677, difference(_41681, _41679))), member(_41677, _41681), -(member(_41677, _41679))], (147 ^ _36919) ^ [_42026, _42028] : [_42028 = _42026, 150 ^ _36919 : [(151 ^ _36919) ^ [] : [-(subset(_42028, _42026))], (153 ^ _36919) ^ [] : [-(subset(_42026, _42028))]]], (155 ^ _36919) ^ [_42263, _42265] : [-(_42265 = _42263), subset(_42265, _42263), subset(_42263, _42265)], (165 ^ _36919) ^ [_42549, _42551] : [-(union(_42551, _42549) = union(_42549, _42551))], (167 ^ _36919) ^ [_42649, _42651] : [-(intersection(_42651, _42649) = intersection(_42649, _42651))], (219 ^ _36919) ^ [_44493] : [-(subset(_44493, _44493))], (210 ^ _36919) ^ [_44185, _44187] : [212 ^ _36919 : [(213 ^ _36919) ^ [] : [-(member(211 ^ [_44185, _44187], _44187))], (215 ^ _36919) ^ [] : [member(211 ^ [_44185, _44187], _44185)]], -(subset(_44187, _44185))], (200 ^ _36919) ^ [_43871, _43873] : [subset(_43873, _43871), 203 ^ _36919 : [(204 ^ _36919) ^ [_44008] : [member(_44008, _43873), -(member(_44008, _43871))]]], (185 ^ _36919) ^ [_43310, _43312] : [-(_43312 = _43310), 189 ^ _36919 : [(190 ^ _36919) ^ [] : [-(member(186 ^ [_43310, _43312], _43312))], (192 ^ _36919) ^ [] : [member(186 ^ [_43310, _43312], _43310)]], 193 ^ _36919 : [(194 ^ _36919) ^ [] : [-(member(186 ^ [_43310, _43312], _43310))], (196 ^ _36919) ^ [] : [member(186 ^ [_43310, _43312], _43312)]]], (169 ^ _36919) ^ [_42793, _42795] : [_42795 = _42793, 172 ^ _36919 : [(173 ^ _36919) ^ [_42959] : [member(_42959, _42795), -(member(_42959, _42793))], (179 ^ _36919) ^ [_43131] : [member(_43131, _42793), -(member(_43131, _42795))]]]], input).
% 7.14/7.58 ncf('1',plain,[difference(union(220 ^ [], 221 ^ []), intersection(220 ^ [], 221 ^ [])) = union(difference(220 ^ [], 221 ^ []), difference(221 ^ [], 220 ^ []))],start(223 ^ 0)).
% 7.14/7.58 ncf('1.1',plain,[-(difference(union(220 ^ [], 221 ^ []), intersection(220 ^ [], 221 ^ [])) = union(difference(220 ^ [], 221 ^ []), difference(221 ^ [], 220 ^ []))), 83 : -(member(79 ^ [union(difference(220 ^ [], 221 ^ []), difference(221 ^ [], 220 ^ [])), difference(union(220 ^ [], 221 ^ []), intersection(220 ^ [], 221 ^ []))], difference(union(220 ^ [], 221 ^ []), intersection(220 ^ [], 221 ^ [])))), 87 : -(member(79 ^ [union(difference(220 ^ [], 221 ^ []), difference(221 ^ [], 220 ^ [])), difference(union(220 ^ [], 221 ^ []), intersection(220 ^ [], 221 ^ []))], union(difference(220 ^ [], 221 ^ []), difference(221 ^ [], 220 ^ []))))],extension(78 ^ 1,bind([[_39630, _39632], [union(difference(220 ^ [], 221 ^ []), difference(221 ^ [], 220 ^ [])), difference(union(220 ^ [], 221 ^ []), intersection(220 ^ [], 221 ^ []))]]))).
% 7.14/7.58 ncf('1.1.1',plain,[member(79 ^ [union(difference(220 ^ [], 221 ^ []), difference(221 ^ [], 220 ^ [])), difference(union(220 ^ [], 221 ^ []), intersection(220 ^ [], 221 ^ []))], difference(union(220 ^ [], 221 ^ []), intersection(220 ^ [], 221 ^ []))), 133 : -(member(79 ^ [union(difference(220 ^ [], 221 ^ []), difference(221 ^ [], 220 ^ [])), difference(union(220 ^ [], 221 ^ []), intersection(220 ^ [], 221 ^ []))], union(220 ^ [], 221 ^ [])))],extension(129 ^ 4,bind([[_41425, _41427, _41429], [79 ^ [union(difference(220 ^ [], 221 ^ []), difference(221 ^ [], 220 ^ [])), difference(union(220 ^ [], 221 ^ []), intersection(220 ^ [], 221 ^ []))], intersection(220 ^ [], 221 ^ []), union(220 ^ [], 221 ^ [])]]))).
% 7.14/7.58 ncf('1.1.1.1',plain,[member(79 ^ [union(difference(220 ^ [], 221 ^ []), difference(221 ^ [], 220 ^ [])), difference(union(220 ^ [], 221 ^ []), intersection(220 ^ [], 221 ^ []))], union(220 ^ [], 221 ^ [])), -(member(79 ^ [union(difference(220 ^ [], 221 ^ []), difference(221 ^ [], 220 ^ [])), difference(union(220 ^ [], 221 ^ []), intersection(220 ^ [], 221 ^ []))], 220 ^ [])), -(member(79 ^ [union(difference(220 ^ [], 221 ^ []), difference(221 ^ [], 220 ^ [])), difference(union(220 ^ [], 221 ^ []), intersection(220 ^ [], 221 ^ []))], 221 ^ []))],extension(93 ^ 7,bind([[_40203, _40205, _40207], [79 ^ [union(difference(220 ^ [], 221 ^ []), difference(221 ^ [], 220 ^ [])), difference(union(220 ^ [], 221 ^ []), intersection(220 ^ [], 221 ^ []))], 221 ^ [], 220 ^ []]]))).
% 7.14/7.58 ncf('1.1.1.1.1',plain,[member(79 ^ [union(difference(220 ^ [], 221 ^ []), difference(221 ^ [], 220 ^ [])), difference(union(220 ^ [], 221 ^ []), intersection(220 ^ [], 221 ^ []))], 220 ^ []), -(member(79 ^ [union(difference(220 ^ [], 221 ^ []), difference(221 ^ [], 220 ^ [])), difference(union(220 ^ [], 221 ^ []), intersection(220 ^ [], 221 ^ []))], difference(220 ^ [], 221 ^ []))), -(member(79 ^ [union(difference(220 ^ [], 221 ^ []), difference(221 ^ [], 220 ^ [])), difference(union(220 ^ [], 221 ^ []), intersection(220 ^ [], 221 ^ []))], 221 ^ []))],extension(137 ^ 8,bind([[_41677, _41679, _41681], [79 ^ [union(difference(220 ^ [], 221 ^ []), difference(221 ^ [], 220 ^ [])), difference(union(220 ^ [], 221 ^ []), intersection(220 ^ [], 221 ^ []))], 221 ^ [], 220 ^ []]]))).
% 7.14/7.58 ncf('1.1.1.1.1.1',plain,[member(79 ^ [union(difference(220 ^ [], 221 ^ []), difference(221 ^ [], 220 ^ [])), difference(union(220 ^ [], 221 ^ []), intersection(220 ^ [], 221 ^ []))], difference(220 ^ [], 221 ^ [])), -(member(79 ^ [union(difference(220 ^ [], 221 ^ []), difference(221 ^ [], 220 ^ [])), difference(union(220 ^ [], 221 ^ []), intersection(220 ^ [], 221 ^ []))], union(difference(220 ^ [], 221 ^ []), difference(221 ^ [], 220 ^ []))))],extension(103 ^ 9,bind([[_40471, _40473, _40475], [79 ^ [union(difference(220 ^ [], 221 ^ []), difference(221 ^ [], 220 ^ [])), difference(union(220 ^ [], 221 ^ []), intersection(220 ^ [], 221 ^ []))], difference(221 ^ [], 220 ^ []), difference(220 ^ [], 221 ^ [])]]))).
% 7.14/7.58 ncf('1.1.1.1.1.1.1',plain,[member(79 ^ [union(difference(220 ^ [], 221 ^ []), difference(221 ^ [], 220 ^ [])), difference(union(220 ^ [], 221 ^ []), intersection(220 ^ [], 221 ^ []))], union(difference(220 ^ [], 221 ^ []), difference(221 ^ [], 220 ^ [])))],extension(85 ^ 10)).
% 7.14/7.58 ncf('1.1.1.1.1.2',plain,[member(79 ^ [union(difference(220 ^ [], 221 ^ []), difference(221 ^ [], 220 ^ [])), difference(union(220 ^ [], 221 ^ []), intersection(220 ^ [], 221 ^ []))], 221 ^ []), -(member(79 ^ [union(difference(220 ^ [], 221 ^ []), difference(221 ^ [], 220 ^ [])), difference(union(220 ^ [], 221 ^ []), intersection(220 ^ [], 221 ^ []))], intersection(220 ^ [], 221 ^ []))), member(79 ^ [union(difference(220 ^ [], 221 ^ []), difference(221 ^ [], 220 ^ [])), difference(union(220 ^ [], 221 ^ []), intersection(220 ^ [], 221 ^ []))], 220 ^ [])],extension(119 ^ 9,bind([[_41065, _41067, _41069], [79 ^ [union(difference(220 ^ [], 221 ^ []), difference(221 ^ [], 220 ^ [])), difference(union(220 ^ [], 221 ^ []), intersection(220 ^ [], 221 ^ []))], 221 ^ [], 220 ^ []]]))).
% 7.14/7.58 ncf('1.1.1.1.1.2.1',plain,[member(79 ^ [union(difference(220 ^ [], 221 ^ []), difference(221 ^ [], 220 ^ [])), difference(union(220 ^ [], 221 ^ []), intersection(220 ^ [], 221 ^ []))], intersection(220 ^ [], 221 ^ []))],extension(135 ^ 10)).
% 7.14/7.58 ncf('1.1.1.1.1.2.2',plain,[-(member(79 ^ [union(difference(220 ^ [], 221 ^ []), difference(221 ^ [], 220 ^ [])), difference(union(220 ^ [], 221 ^ []), intersection(220 ^ [], 221 ^ []))], 220 ^ []))],reduction('1.1.1.1')).
% 7.14/7.58 ncf('1.1.1.1.2',plain,[member(79 ^ [union(difference(220 ^ [], 221 ^ []), difference(221 ^ [], 220 ^ [])), difference(union(220 ^ [], 221 ^ []), intersection(220 ^ [], 221 ^ []))], 221 ^ []), -(member(79 ^ [union(difference(220 ^ [], 221 ^ []), difference(221 ^ [], 220 ^ [])), difference(union(220 ^ [], 221 ^ []), intersection(220 ^ [], 221 ^ []))], intersection(221 ^ [], union(difference(220 ^ [], 221 ^ []), difference(221 ^ [], 220 ^ []))))), member(79 ^ [union(difference(220 ^ [], 221 ^ []), difference(221 ^ [], 220 ^ [])), difference(union(220 ^ [], 221 ^ []), intersection(220 ^ [], 221 ^ []))], union(difference(220 ^ [], 221 ^ []), difference(221 ^ [], 220 ^ [])))],extension(119 ^ 8,bind([[_41065, _41067, _41069], [79 ^ [union(difference(220 ^ [], 221 ^ []), difference(221 ^ [], 220 ^ [])), difference(union(220 ^ [], 221 ^ []), intersection(220 ^ [], 221 ^ []))], union(difference(220 ^ [], 221 ^ []), difference(221 ^ [], 220 ^ [])), 221 ^ []]]))).
% 7.14/7.58 ncf('1.1.1.1.2.1',plain,[member(79 ^ [union(difference(220 ^ [], 221 ^ []), difference(221 ^ [], 220 ^ [])), difference(union(220 ^ [], 221 ^ []), intersection(220 ^ [], 221 ^ []))], intersection(221 ^ [], union(difference(220 ^ [], 221 ^ []), difference(221 ^ [], 220 ^ [])))), 117 : -(member(79 ^ [union(difference(220 ^ [], 221 ^ []), difference(221 ^ [], 220 ^ [])), difference(union(220 ^ [], 221 ^ []), intersection(220 ^ [], 221 ^ []))], union(difference(220 ^ [], 221 ^ []), difference(221 ^ [], 220 ^ []))))],extension(111 ^ 9,bind([[_40814, _40816, _40818], [79 ^ [union(difference(220 ^ [], 221 ^ []), difference(221 ^ [], 220 ^ [])), difference(union(220 ^ [], 221 ^ []), intersection(220 ^ [], 221 ^ []))], union(difference(220 ^ [], 221 ^ []), difference(221 ^ [], 220 ^ [])), 221 ^ []]]))).
% 7.14/7.58 ncf('1.1.1.1.2.1.1',plain,[member(79 ^ [union(difference(220 ^ [], 221 ^ []), difference(221 ^ [], 220 ^ [])), difference(union(220 ^ [], 221 ^ []), intersection(220 ^ [], 221 ^ []))], union(difference(220 ^ [], 221 ^ []), difference(221 ^ [], 220 ^ [])))],extension(85 ^ 12)).
% 7.14/7.58 ncf('1.1.1.1.2.2',plain,[-(member(79 ^ [union(difference(220 ^ [], 221 ^ []), difference(221 ^ [], 220 ^ [])), difference(union(220 ^ [], 221 ^ []), intersection(220 ^ [], 221 ^ []))], union(difference(220 ^ [], 221 ^ []), difference(221 ^ [], 220 ^ [])))), 107 : member(79 ^ [union(difference(220 ^ [], 221 ^ []), difference(221 ^ [], 220 ^ [])), difference(union(220 ^ [], 221 ^ []), intersection(220 ^ [], 221 ^ []))], difference(221 ^ [], 220 ^ []))],extension(103 ^ 9,bind([[_40471, _40473, _40475], [79 ^ [union(difference(220 ^ [], 221 ^ []), difference(221 ^ [], 220 ^ [])), difference(union(220 ^ [], 221 ^ []), intersection(220 ^ [], 221 ^ []))], difference(221 ^ [], 220 ^ []), difference(220 ^ [], 221 ^ [])]]))).
% 7.14/7.58 ncf('1.1.1.1.2.2.1',plain,[-(member(79 ^ [union(difference(220 ^ [], 221 ^ []), difference(221 ^ [], 220 ^ [])), difference(union(220 ^ [], 221 ^ []), intersection(220 ^ [], 221 ^ []))], difference(221 ^ [], 220 ^ []))), member(79 ^ [union(difference(220 ^ [], 221 ^ []), difference(221 ^ [], 220 ^ [])), difference(union(220 ^ [], 221 ^ []), intersection(220 ^ [], 221 ^ []))], 221 ^ []), -(member(79 ^ [union(difference(220 ^ [], 221 ^ []), difference(221 ^ [], 220 ^ [])), difference(union(220 ^ [], 221 ^ []), intersection(220 ^ [], 221 ^ []))], 220 ^ []))],extension(137 ^ 12,bind([[_41677, _41679, _41681], [79 ^ [union(difference(220 ^ [], 221 ^ []), difference(221 ^ [], 220 ^ [])), difference(union(220 ^ [], 221 ^ []), intersection(220 ^ [], 221 ^ []))], 220 ^ [], 221 ^ []]]))).
% 7.14/7.58 ncf('1.1.1.1.2.2.1.1',plain,[-(member(79 ^ [union(difference(220 ^ [], 221 ^ []), difference(221 ^ [], 220 ^ [])), difference(union(220 ^ [], 221 ^ []), intersection(220 ^ [], 221 ^ []))], 221 ^ []))],reduction('1.1.1.1')).
% 7.14/7.58 ncf('1.1.1.1.2.2.1.2',plain,[member(79 ^ [union(difference(220 ^ [], 221 ^ []), difference(221 ^ [], 220 ^ [])), difference(union(220 ^ [], 221 ^ []), intersection(220 ^ [], 221 ^ []))], 220 ^ [])],lemmata('[1, 1, 1].x')).
% 7.14/7.58 ncf('1.1.2',plain,[member(79 ^ [union(difference(220 ^ [], 221 ^ []), difference(221 ^ [], 220 ^ [])), difference(union(220 ^ [], 221 ^ []), intersection(220 ^ [], 221 ^ []))], union(difference(220 ^ [], 221 ^ []), difference(221 ^ [], 220 ^ []))), -(member(79 ^ [union(difference(220 ^ [], 221 ^ []), difference(221 ^ [], 220 ^ [])), difference(union(220 ^ [], 221 ^ []), intersection(220 ^ [], 221 ^ []))], difference(220 ^ [], 221 ^ []))), -(member(79 ^ [union(difference(220 ^ [], 221 ^ []), difference(221 ^ [], 220 ^ [])), difference(union(220 ^ [], 221 ^ []), intersection(220 ^ [], 221 ^ []))], difference(221 ^ [], 220 ^ [])))],extension(93 ^ 4,bind([[_40203, _40205, _40207], [79 ^ [union(difference(220 ^ [], 221 ^ []), difference(221 ^ [], 220 ^ [])), difference(union(220 ^ [], 221 ^ []), intersection(220 ^ [], 221 ^ []))], difference(221 ^ [], 220 ^ []), difference(220 ^ [], 221 ^ [])]]))).
% 7.14/7.58 ncf('1.1.2.1',plain,[member(79 ^ [union(difference(220 ^ [], 221 ^ []), difference(221 ^ [], 220 ^ [])), difference(union(220 ^ [], 221 ^ []), intersection(220 ^ [], 221 ^ []))], difference(220 ^ [], 221 ^ [])), -(member(79 ^ [union(difference(220 ^ [], 221 ^ []), difference(221 ^ [], 220 ^ [])), difference(union(220 ^ [], 221 ^ []), intersection(220 ^ [], 221 ^ []))], intersection(difference(220 ^ [], 221 ^ []), difference(union(220 ^ [], 221 ^ []), intersection(220 ^ [], 221 ^ []))))), member(79 ^ [union(difference(220 ^ [], 221 ^ []), difference(221 ^ [], 220 ^ [])), difference(union(220 ^ [], 221 ^ []), intersection(220 ^ [], 221 ^ []))], difference(union(220 ^ [], 221 ^ []), intersection(220 ^ [], 221 ^ [])))],extension(119 ^ 5,bind([[_41065, _41067, _41069], [79 ^ [union(difference(220 ^ [], 221 ^ []), difference(221 ^ [], 220 ^ [])), difference(union(220 ^ [], 221 ^ []), intersection(220 ^ [], 221 ^ []))], difference(union(220 ^ [], 221 ^ []), intersection(220 ^ [], 221 ^ [])), difference(220 ^ [], 221 ^ [])]]))).
% 7.14/7.58 ncf('1.1.2.1.1',plain,[member(79 ^ [union(difference(220 ^ [], 221 ^ []), difference(221 ^ [], 220 ^ [])), difference(union(220 ^ [], 221 ^ []), intersection(220 ^ [], 221 ^ []))], intersection(difference(220 ^ [], 221 ^ []), difference(union(220 ^ [], 221 ^ []), intersection(220 ^ [], 221 ^ [])))), 117 : -(member(79 ^ [union(difference(220 ^ [], 221 ^ []), difference(221 ^ [], 220 ^ [])), difference(union(220 ^ [], 221 ^ []), intersection(220 ^ [], 221 ^ []))], difference(union(220 ^ [], 221 ^ []), intersection(220 ^ [], 221 ^ []))))],extension(111 ^ 6,bind([[_40814, _40816, _40818], [79 ^ [union(difference(220 ^ [], 221 ^ []), difference(221 ^ [], 220 ^ [])), difference(union(220 ^ [], 221 ^ []), intersection(220 ^ [], 221 ^ []))], difference(union(220 ^ [], 221 ^ []), intersection(220 ^ [], 221 ^ [])), difference(220 ^ [], 221 ^ [])]]))).
% 7.14/7.58 ncf('1.1.2.1.1.1',plain,[member(79 ^ [union(difference(220 ^ [], 221 ^ []), difference(221 ^ [], 220 ^ [])), difference(union(220 ^ [], 221 ^ []), intersection(220 ^ [], 221 ^ []))], difference(union(220 ^ [], 221 ^ []), intersection(220 ^ [], 221 ^ [])))],extension(89 ^ 9)).
% 7.14/7.58 ncf('1.1.2.1.2',plain,[-(member(79 ^ [union(difference(220 ^ [], 221 ^ []), difference(221 ^ [], 220 ^ [])), difference(union(220 ^ [], 221 ^ []), intersection(220 ^ [], 221 ^ []))], difference(union(220 ^ [], 221 ^ []), intersection(220 ^ [], 221 ^ [])))), member(79 ^ [union(difference(220 ^ [], 221 ^ []), difference(221 ^ [], 220 ^ [])), difference(union(220 ^ [], 221 ^ []), intersection(220 ^ [], 221 ^ []))], union(220 ^ [], 221 ^ [])), -(member(79 ^ [union(difference(220 ^ [], 221 ^ []), difference(221 ^ [], 220 ^ [])), difference(union(220 ^ [], 221 ^ []), intersection(220 ^ [], 221 ^ []))], intersection(220 ^ [], 221 ^ [])))],extension(137 ^ 6,bind([[_41677, _41679, _41681], [79 ^ [union(difference(220 ^ [], 221 ^ []), difference(221 ^ [], 220 ^ [])), difference(union(220 ^ [], 221 ^ []), intersection(220 ^ [], 221 ^ []))], intersection(220 ^ [], 221 ^ []), union(220 ^ [], 221 ^ [])]]))).
% 7.14/7.58 ncf('1.1.2.1.2.1',plain,[-(member(79 ^ [union(difference(220 ^ [], 221 ^ []), difference(221 ^ [], 220 ^ [])), difference(union(220 ^ [], 221 ^ []), intersection(220 ^ [], 221 ^ []))], union(220 ^ [], 221 ^ []))), 105 : member(79 ^ [union(difference(220 ^ [], 221 ^ []), difference(221 ^ [], 220 ^ [])), difference(union(220 ^ [], 221 ^ []), intersection(220 ^ [], 221 ^ []))], 220 ^ [])],extension(103 ^ 7,bind([[_40471, _40473, _40475], [79 ^ [union(difference(220 ^ [], 221 ^ []), difference(221 ^ [], 220 ^ [])), difference(union(220 ^ [], 221 ^ []), intersection(220 ^ [], 221 ^ []))], 221 ^ [], 220 ^ []]]))).
% 7.14/7.58 ncf('1.1.2.1.2.1.1',plain,[-(member(79 ^ [union(difference(220 ^ [], 221 ^ []), difference(221 ^ [], 220 ^ [])), difference(union(220 ^ [], 221 ^ []), intersection(220 ^ [], 221 ^ []))], 220 ^ [])), member(79 ^ [union(difference(220 ^ [], 221 ^ []), difference(221 ^ [], 220 ^ [])), difference(union(220 ^ [], 221 ^ []), intersection(220 ^ [], 221 ^ []))], difference(220 ^ [], 221 ^ []))],extension(129 ^ 10,bind([[_41425, _41427, _41429], [79 ^ [union(difference(220 ^ [], 221 ^ []), difference(221 ^ [], 220 ^ [])), difference(union(220 ^ [], 221 ^ []), intersection(220 ^ [], 221 ^ []))], 221 ^ [], 220 ^ []]]))).
% 7.14/7.58 ncf('1.1.2.1.2.1.1.1',plain,[-(member(79 ^ [union(difference(220 ^ [], 221 ^ []), difference(221 ^ [], 220 ^ [])), difference(union(220 ^ [], 221 ^ []), intersection(220 ^ [], 221 ^ []))], difference(220 ^ [], 221 ^ [])))],reduction('1.1.2')).
% 7.14/7.58 ncf('1.1.2.1.2.2',plain,[member(79 ^ [union(difference(220 ^ [], 221 ^ []), difference(221 ^ [], 220 ^ [])), difference(union(220 ^ [], 221 ^ []), intersection(220 ^ [], 221 ^ []))], intersection(220 ^ [], 221 ^ [])), 117 : -(member(79 ^ [union(difference(220 ^ [], 221 ^ []), difference(221 ^ [], 220 ^ [])), difference(union(220 ^ [], 221 ^ []), intersection(220 ^ [], 221 ^ []))], 221 ^ []))],extension(111 ^ 7,bind([[_40814, _40816, _40818], [79 ^ [union(difference(220 ^ [], 221 ^ []), difference(221 ^ [], 220 ^ [])), difference(union(220 ^ [], 221 ^ []), intersection(220 ^ [], 221 ^ []))], 221 ^ [], 220 ^ []]]))).
% 7.14/7.58 ncf('1.1.2.1.2.2.1',plain,[member(79 ^ [union(difference(220 ^ [], 221 ^ []), difference(221 ^ [], 220 ^ [])), difference(union(220 ^ [], 221 ^ []), intersection(220 ^ [], 221 ^ []))], 221 ^ []), member(79 ^ [union(difference(220 ^ [], 221 ^ []), difference(221 ^ [], 220 ^ [])), difference(union(220 ^ [], 221 ^ []), intersection(220 ^ [], 221 ^ []))], difference(220 ^ [], 221 ^ []))],extension(129 ^ 10,bind([[_41425, _41427, _41429], [79 ^ [union(difference(220 ^ [], 221 ^ []), difference(221 ^ [], 220 ^ [])), difference(union(220 ^ [], 221 ^ []), intersection(220 ^ [], 221 ^ []))], 221 ^ [], 220 ^ []]]))).
% 7.14/7.58 ncf('1.1.2.1.2.2.1.1',plain,[-(member(79 ^ [union(difference(220 ^ [], 221 ^ []), difference(221 ^ [], 220 ^ [])), difference(union(220 ^ [], 221 ^ []), intersection(220 ^ [], 221 ^ []))], difference(220 ^ [], 221 ^ [])))],reduction('1.1.2')).
% 7.14/7.58 ncf('1.1.2.2',plain,[member(79 ^ [union(difference(220 ^ [], 221 ^ []), difference(221 ^ [], 220 ^ [])), difference(union(220 ^ [], 221 ^ []), intersection(220 ^ [], 221 ^ []))], difference(221 ^ [], 220 ^ [])), -(member(79 ^ [union(difference(220 ^ [], 221 ^ []), difference(221 ^ [], 220 ^ [])), difference(union(220 ^ [], 221 ^ []), intersection(220 ^ [], 221 ^ []))], intersection(difference(221 ^ [], 220 ^ []), difference(union(220 ^ [], 221 ^ []), intersection(220 ^ [], 221 ^ []))))), member(79 ^ [union(difference(220 ^ [], 221 ^ []), difference(221 ^ [], 220 ^ [])), difference(union(220 ^ [], 221 ^ []), intersection(220 ^ [], 221 ^ []))], difference(union(220 ^ [], 221 ^ []), intersection(220 ^ [], 221 ^ [])))],extension(119 ^ 5,bind([[_41065, _41067, _41069], [79 ^ [union(difference(220 ^ [], 221 ^ []), difference(221 ^ [], 220 ^ [])), difference(union(220 ^ [], 221 ^ []), intersection(220 ^ [], 221 ^ []))], difference(union(220 ^ [], 221 ^ []), intersection(220 ^ [], 221 ^ [])), difference(221 ^ [], 220 ^ [])]]))).
% 7.14/7.58 ncf('1.1.2.2.1',plain,[member(79 ^ [union(difference(220 ^ [], 221 ^ []), difference(221 ^ [], 220 ^ [])), difference(union(220 ^ [], 221 ^ []), intersection(220 ^ [], 221 ^ []))], intersection(difference(221 ^ [], 220 ^ []), difference(union(220 ^ [], 221 ^ []), intersection(220 ^ [], 221 ^ [])))), 117 : -(member(79 ^ [union(difference(220 ^ [], 221 ^ []), difference(221 ^ [], 220 ^ [])), difference(union(220 ^ [], 221 ^ []), intersection(220 ^ [], 221 ^ []))], difference(union(220 ^ [], 221 ^ []), intersection(220 ^ [], 221 ^ []))))],extension(111 ^ 6,bind([[_40814, _40816, _40818], [79 ^ [union(difference(220 ^ [], 221 ^ []), difference(221 ^ [], 220 ^ [])), difference(union(220 ^ [], 221 ^ []), intersection(220 ^ [], 221 ^ []))], difference(union(220 ^ [], 221 ^ []), intersection(220 ^ [], 221 ^ [])), difference(221 ^ [], 220 ^ [])]]))).
% 7.14/7.58 ncf('1.1.2.2.1.1',plain,[member(79 ^ [union(difference(220 ^ [], 221 ^ []), difference(221 ^ [], 220 ^ [])), difference(union(220 ^ [], 221 ^ []), intersection(220 ^ [], 221 ^ []))], difference(union(220 ^ [], 221 ^ []), intersection(220 ^ [], 221 ^ [])))],extension(89 ^ 9)).
% 7.14/7.58 ncf('1.1.2.2.2',plain,[-(member(79 ^ [union(difference(220 ^ [], 221 ^ []), difference(221 ^ [], 220 ^ [])), difference(union(220 ^ [], 221 ^ []), intersection(220 ^ [], 221 ^ []))], difference(union(220 ^ [], 221 ^ []), intersection(220 ^ [], 221 ^ [])))), member(79 ^ [union(difference(220 ^ [], 221 ^ []), difference(221 ^ [], 220 ^ [])), difference(union(220 ^ [], 221 ^ []), intersection(220 ^ [], 221 ^ []))], union(220 ^ [], 221 ^ [])), -(member(79 ^ [union(difference(220 ^ [], 221 ^ []), difference(221 ^ [], 220 ^ [])), difference(union(220 ^ [], 221 ^ []), intersection(220 ^ [], 221 ^ []))], intersection(220 ^ [], 221 ^ [])))],extension(137 ^ 6,bind([[_41677, _41679, _41681], [79 ^ [union(difference(220 ^ [], 221 ^ []), difference(221 ^ [], 220 ^ [])), difference(union(220 ^ [], 221 ^ []), intersection(220 ^ [], 221 ^ []))], intersection(220 ^ [], 221 ^ []), union(220 ^ [], 221 ^ [])]]))).
% 7.14/7.58 ncf('1.1.2.2.2.1',plain,[-(member(79 ^ [union(difference(220 ^ [], 221 ^ []), difference(221 ^ [], 220 ^ [])), difference(union(220 ^ [], 221 ^ []), intersection(220 ^ [], 221 ^ []))], union(220 ^ [], 221 ^ []))), 107 : member(79 ^ [union(difference(220 ^ [], 221 ^ []), difference(221 ^ [], 220 ^ [])), difference(union(220 ^ [], 221 ^ []), intersection(220 ^ [], 221 ^ []))], 221 ^ [])],extension(103 ^ 7,bind([[_40471, _40473, _40475], [79 ^ [union(difference(220 ^ [], 221 ^ []), difference(221 ^ [], 220 ^ [])), difference(union(220 ^ [], 221 ^ []), intersection(220 ^ [], 221 ^ []))], 221 ^ [], 220 ^ []]]))).
% 7.14/7.58 ncf('1.1.2.2.2.1.1',plain,[-(member(79 ^ [union(difference(220 ^ [], 221 ^ []), difference(221 ^ [], 220 ^ [])), difference(union(220 ^ [], 221 ^ []), intersection(220 ^ [], 221 ^ []))], 221 ^ [])), member(79 ^ [union(difference(220 ^ [], 221 ^ []), difference(221 ^ [], 220 ^ [])), difference(union(220 ^ [], 221 ^ []), intersection(220 ^ [], 221 ^ []))], difference(221 ^ [], 220 ^ []))],extension(129 ^ 10,bind([[_41425, _41427, _41429], [79 ^ [union(difference(220 ^ [], 221 ^ []), difference(221 ^ [], 220 ^ [])), difference(union(220 ^ [], 221 ^ []), intersection(220 ^ [], 221 ^ []))], 220 ^ [], 221 ^ []]]))).
% 7.14/7.58 ncf('1.1.2.2.2.1.1.1',plain,[-(member(79 ^ [union(difference(220 ^ [], 221 ^ []), difference(221 ^ [], 220 ^ [])), difference(union(220 ^ [], 221 ^ []), intersection(220 ^ [], 221 ^ []))], difference(221 ^ [], 220 ^ [])))],reduction('1.1.2')).
% 7.14/7.58 ncf('1.1.2.2.2.2',plain,[member(79 ^ [union(difference(220 ^ [], 221 ^ []), difference(221 ^ [], 220 ^ [])), difference(union(220 ^ [], 221 ^ []), intersection(220 ^ [], 221 ^ []))], intersection(220 ^ [], 221 ^ [])), 115 : -(member(79 ^ [union(difference(220 ^ [], 221 ^ []), difference(221 ^ [], 220 ^ [])), difference(union(220 ^ [], 221 ^ []), intersection(220 ^ [], 221 ^ []))], 220 ^ []))],extension(111 ^ 7,bind([[_40814, _40816, _40818], [79 ^ [union(difference(220 ^ [], 221 ^ []), difference(221 ^ [], 220 ^ [])), difference(union(220 ^ [], 221 ^ []), intersection(220 ^ [], 221 ^ []))], 221 ^ [], 220 ^ []]]))).
% 7.14/7.58 ncf('1.1.2.2.2.2.1',plain,[member(79 ^ [union(difference(220 ^ [], 221 ^ []), difference(221 ^ [], 220 ^ [])), difference(union(220 ^ [], 221 ^ []), intersection(220 ^ [], 221 ^ []))], 220 ^ []), member(79 ^ [union(difference(220 ^ [], 221 ^ []), difference(221 ^ [], 220 ^ [])), difference(union(220 ^ [], 221 ^ []), intersection(220 ^ [], 221 ^ []))], difference(221 ^ [], 220 ^ []))],extension(129 ^ 10,bind([[_41425, _41427, _41429], [79 ^ [union(difference(220 ^ [], 221 ^ []), difference(221 ^ [], 220 ^ [])), difference(union(220 ^ [], 221 ^ []), intersection(220 ^ [], 221 ^ []))], 220 ^ [], 221 ^ []]]))).
% 7.14/7.58 ncf('1.1.2.2.2.2.1.1',plain,[-(member(79 ^ [union(difference(220 ^ [], 221 ^ []), difference(221 ^ [], 220 ^ [])), difference(union(220 ^ [], 221 ^ []), intersection(220 ^ [], 221 ^ []))], difference(221 ^ [], 220 ^ [])))],reduction('1.1.2')).
% 7.14/7.58 %-----------------------------------------------------
% 7.14/7.58 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------