%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : SET011+3 : TPTP v8.1.2. Released v2.2.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n019.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:55:03 EDT 2023
% Result : Theorem 14.36s 14.82s
% Output : Proof 14.36s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : SET011+3 : TPTP v8.1.2. Released v2.2.0.
% 0.07/0.13 % Command : nanocop.sh %s %d
% 0.13/0.34 % Computer : n019.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 19:00:12 EDT 2023
% 0.13/0.34 % CPUTime :
% 14.36/14.82
% 14.36/14.82 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 14.36/14.82 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 14.36/14.82 %-----------------------------------------------------
% 14.36/14.82 ncf(matrix, plain, [(178 ^ _32307) ^ [] : [difference(175 ^ [], difference(175 ^ [], 176 ^ [])) = intersection(175 ^ [], 176 ^ [])], (48 ^ _32307) ^ [_33979, _33981, _33983, _33985] : [-(difference(_33985, _33981) = difference(_33983, _33979)), _33985 = _33983, _33981 = _33979], (58 ^ _32307) ^ [_34318, _34320, _34322, _34324] : [-(intersection(_34324, _34320) = intersection(_34322, _34318)), _34324 = _34322, _34320 = _34318], (2 ^ _32307) ^ [_32451] : [-(_32451 = _32451)], (4 ^ _32307) ^ [_32558, _32560] : [_32560 = _32558, -(_32558 = _32560)], (10 ^ _32307) ^ [_32762, _32764, _32766] : [-(_32766 = _32762), _32766 = _32764, _32764 = _32762], (20 ^ _32307) ^ [_33103, _33105, _33107, _33109] : [-(subset(_33107, _33103)), subset(_33109, _33105), _33109 = _33107, _33105 = _33103], (34 ^ _32307) ^ [_33527, _33529, _33531, _33533] : [-(member(_33531, _33527)), member(_33533, _33529), _33533 = _33531, _33529 = _33527], (68 ^ _32307) ^ [_34698, _34700, _34702] : [member(_34698, intersection(_34702, _34700)), 71 ^ _32307 : [(72 ^ _32307) ^ [] : [-(member(_34698, _34702))], (74 ^ _32307) ^ [] : [-(member(_34698, _34700))]]], (76 ^ _32307) ^ [_34949, _34951, _34953] : [-(member(_34949, intersection(_34953, _34951))), member(_34949, _34953), member(_34949, _34951)], (86 ^ _32307) ^ [_35309, _35311, _35313] : [member(_35309, difference(_35313, _35311)), 89 ^ _32307 : [(90 ^ _32307) ^ [] : [-(member(_35309, _35313))], (92 ^ _32307) ^ [] : [member(_35309, _35311)]]], (94 ^ _32307) ^ [_35561, _35563, _35565] : [-(member(_35561, difference(_35565, _35563))), member(_35561, _35565), -(member(_35561, _35563))], (104 ^ _32307) ^ [_35910, _35912] : [_35912 = _35910, 107 ^ _32307 : [(108 ^ _32307) ^ [] : [-(subset(_35912, _35910))], (110 ^ _32307) ^ [] : [-(subset(_35910, _35912))]]], (112 ^ _32307) ^ [_36147, _36149] : [-(_36149 = _36147), subset(_36149, _36147), subset(_36147, _36149)], (122 ^ _32307) ^ [_36433, _36435] : [-(intersection(_36435, _36433) = intersection(_36433, _36435))], (134 ^ _32307) ^ [_36891, _36893] : [136 ^ _32307 : [(137 ^ _32307) ^ [] : [-(member(135 ^ [_36891, _36893], _36893))], (139 ^ _32307) ^ [] : [member(135 ^ [_36891, _36893], _36891)]], -(subset(_36893, _36891))], (124 ^ _32307) ^ [_36577, _36579] : [subset(_36579, _36577), 127 ^ _32307 : [(128 ^ _32307) ^ [_36714] : [member(_36714, _36579), -(member(_36714, _36577))]]], (143 ^ _32307) ^ [_37219] : [-(subset(_37219, _37219))], (161 ^ _32307) ^ [_37852, _37854] : [-(_37854 = _37852), 165 ^ _32307 : [(166 ^ _32307) ^ [] : [-(member(162 ^ [_37852, _37854], _37854))], (168 ^ _32307) ^ [] : [member(162 ^ [_37852, _37854], _37852)]], 169 ^ _32307 : [(170 ^ _32307) ^ [] : [-(member(162 ^ [_37852, _37854], _37852))], (172 ^ _32307) ^ [] : [member(162 ^ [_37852, _37854], _37854)]]], (145 ^ _32307) ^ [_37335, _37337] : [_37337 = _37335, 148 ^ _32307 : [(149 ^ _32307) ^ [_37501] : [member(_37501, _37337), -(member(_37501, _37335))], (155 ^ _32307) ^ [_37673] : [member(_37673, _37335), -(member(_37673, _37337))]]]], input).
% 14.36/14.82 ncf('1',plain,[difference(175 ^ [], difference(175 ^ [], 176 ^ [])) = intersection(175 ^ [], 176 ^ [])],start(178 ^ 0)).
% 14.36/14.82 ncf('1.1',plain,[-(difference(175 ^ [], difference(175 ^ [], 176 ^ [])) = intersection(175 ^ [], 176 ^ [])), 168 : member(162 ^ [intersection(175 ^ [], 176 ^ []), difference(175 ^ [], difference(175 ^ [], 176 ^ []))], intersection(175 ^ [], 176 ^ [])), 172 : member(162 ^ [intersection(175 ^ [], 176 ^ []), difference(175 ^ [], difference(175 ^ [], 176 ^ []))], difference(175 ^ [], difference(175 ^ [], 176 ^ [])))],extension(161 ^ 1,bind([[_37852, _37854], [intersection(175 ^ [], 176 ^ []), difference(175 ^ [], difference(175 ^ [], 176 ^ []))]]))).
% 14.36/14.82 ncf('1.1.1',plain,[-(member(162 ^ [intersection(175 ^ [], 176 ^ []), difference(175 ^ [], difference(175 ^ [], 176 ^ []))], intersection(175 ^ [], 176 ^ []))), member(162 ^ [intersection(175 ^ [], 176 ^ []), difference(175 ^ [], difference(175 ^ [], 176 ^ []))], 175 ^ []), member(162 ^ [intersection(175 ^ [], 176 ^ []), difference(175 ^ [], difference(175 ^ [], 176 ^ []))], 176 ^ [])],extension(76 ^ 4,bind([[_34949, _34951, _34953], [162 ^ [intersection(175 ^ [], 176 ^ []), difference(175 ^ [], difference(175 ^ [], 176 ^ []))], 176 ^ [], 175 ^ []]]))).
% 14.36/14.82 ncf('1.1.1.1',plain,[-(member(162 ^ [intersection(175 ^ [], 176 ^ []), difference(175 ^ [], difference(175 ^ [], 176 ^ []))], 175 ^ [])), member(162 ^ [intersection(175 ^ [], 176 ^ []), difference(175 ^ [], difference(175 ^ [], 176 ^ []))], intersection(175 ^ [], 176 ^ []))],extension(68 ^ 5,bind([[_34698, _34700, _34702], [162 ^ [intersection(175 ^ [], 176 ^ []), difference(175 ^ [], difference(175 ^ [], 176 ^ []))], 176 ^ [], 175 ^ []]]))).
% 14.36/14.82 ncf('1.1.1.1.1',plain,[-(member(162 ^ [intersection(175 ^ [], 176 ^ []), difference(175 ^ [], difference(175 ^ [], 176 ^ []))], intersection(175 ^ [], 176 ^ []))), member(162 ^ [intersection(175 ^ [], 176 ^ []), difference(175 ^ [], difference(175 ^ [], 176 ^ []))], difference(175 ^ [], difference(175 ^ [], 176 ^ []))), 162 ^ [intersection(175 ^ [], 176 ^ []), difference(175 ^ [], difference(175 ^ [], 176 ^ []))] = 162 ^ [intersection(175 ^ [], 176 ^ []), difference(175 ^ [], difference(175 ^ [], 176 ^ []))], difference(175 ^ [], difference(175 ^ [], 176 ^ [])) = intersection(175 ^ [], 176 ^ [])],extension(34 ^ 6,bind([[_33527, _33529, _33531, _33533], [intersection(175 ^ [], 176 ^ []), difference(175 ^ [], difference(175 ^ [], 176 ^ [])), 162 ^ [intersection(175 ^ [], 176 ^ []), difference(175 ^ [], difference(175 ^ [], 176 ^ []))], 162 ^ [intersection(175 ^ [], 176 ^ []), difference(175 ^ [], difference(175 ^ [], 176 ^ []))]]]))).
% 14.36/14.82 ncf('1.1.1.1.1.1',plain,[-(member(162 ^ [intersection(175 ^ [], 176 ^ []), difference(175 ^ [], difference(175 ^ [], 176 ^ []))], difference(175 ^ [], difference(175 ^ [], 176 ^ [])))), member(162 ^ [intersection(175 ^ [], 176 ^ []), difference(175 ^ [], difference(175 ^ [], 176 ^ []))], difference(175 ^ [], difference(175 ^ [], 176 ^ []))), 162 ^ [intersection(175 ^ [], 176 ^ []), difference(175 ^ [], difference(175 ^ [], 176 ^ []))] = 162 ^ [intersection(175 ^ [], 176 ^ []), difference(175 ^ [], difference(175 ^ [], 176 ^ []))], difference(175 ^ [], difference(175 ^ [], 176 ^ [])) = difference(175 ^ [], difference(175 ^ [], 176 ^ []))],extension(34 ^ 7,bind([[_33527, _33529, _33531, _33533], [difference(175 ^ [], difference(175 ^ [], 176 ^ [])), difference(175 ^ [], difference(175 ^ [], 176 ^ [])), 162 ^ [intersection(175 ^ [], 176 ^ []), difference(175 ^ [], difference(175 ^ [], 176 ^ []))], 162 ^ [intersection(175 ^ [], 176 ^ []), difference(175 ^ [], difference(175 ^ [], 176 ^ []))]]]))).
% 14.36/14.82 ncf('1.1.1.1.1.1.1',plain,[-(member(162 ^ [intersection(175 ^ [], 176 ^ []), difference(175 ^ [], difference(175 ^ [], 176 ^ []))], difference(175 ^ [], difference(175 ^ [], 176 ^ [])))), member(162 ^ [intersection(175 ^ [], 176 ^ []), difference(175 ^ [], difference(175 ^ [], 176 ^ []))], difference(175 ^ [], difference(175 ^ [], 176 ^ []))), 162 ^ [intersection(175 ^ [], 176 ^ []), difference(175 ^ [], difference(175 ^ [], 176 ^ []))] = 162 ^ [intersection(175 ^ [], 176 ^ []), difference(175 ^ [], difference(175 ^ [], 176 ^ []))], difference(175 ^ [], difference(175 ^ [], 176 ^ [])) = difference(175 ^ [], difference(175 ^ [], 176 ^ []))],extension(34 ^ 8,bind([[_33527, _33529, _33531, _33533], [difference(175 ^ [], difference(175 ^ [], 176 ^ [])), difference(175 ^ [], difference(175 ^ [], 176 ^ [])), 162 ^ [intersection(175 ^ [], 176 ^ []), difference(175 ^ [], difference(175 ^ [], 176 ^ []))], 162 ^ [intersection(175 ^ [], 176 ^ []), difference(175 ^ [], difference(175 ^ [], 176 ^ []))]]]))).
% 14.36/14.82 ncf('1.1.1.1.1.1.1.1',plain,[-(member(162 ^ [intersection(175 ^ [], 176 ^ []), difference(175 ^ [], difference(175 ^ [], 176 ^ []))], difference(175 ^ [], difference(175 ^ [], 176 ^ []))))],extension(166 ^ 9)).
% 14.36/14.82 ncf('1.1.1.1.1.1.1.2',plain,[-(162 ^ [intersection(175 ^ [], 176 ^ []), difference(175 ^ [], difference(175 ^ [], 176 ^ []))] = 162 ^ [intersection(175 ^ [], 176 ^ []), difference(175 ^ [], difference(175 ^ [], 176 ^ []))])],extension(2 ^ 9,bind([[_32451], [162 ^ [intersection(175 ^ [], 176 ^ []), difference(175 ^ [], difference(175 ^ [], 176 ^ []))]]]))).
% 14.36/14.82 ncf('1.1.1.1.1.1.1.3',plain,[-(difference(175 ^ [], difference(175 ^ [], 176 ^ [])) = difference(175 ^ [], difference(175 ^ [], 176 ^ [])))],extension(2 ^ 9,bind([[_32451], [difference(175 ^ [], difference(175 ^ [], 176 ^ []))]]))).
% 14.36/14.82 ncf('1.1.1.1.1.1.2',plain,[-(162 ^ [intersection(175 ^ [], 176 ^ []), difference(175 ^ [], difference(175 ^ [], 176 ^ []))] = 162 ^ [intersection(175 ^ [], 176 ^ []), difference(175 ^ [], difference(175 ^ [], 176 ^ []))])],extension(2 ^ 8,bind([[_32451], [162 ^ [intersection(175 ^ [], 176 ^ []), difference(175 ^ [], difference(175 ^ [], 176 ^ []))]]]))).
% 14.36/14.82 ncf('1.1.1.1.1.1.3',plain,[-(difference(175 ^ [], difference(175 ^ [], 176 ^ [])) = difference(175 ^ [], difference(175 ^ [], 176 ^ []))), 175 ^ [] = 175 ^ [], difference(175 ^ [], 176 ^ []) = difference(175 ^ [], 176 ^ [])],extension(48 ^ 8,bind([[_33979, _33981, _33983, _33985], [difference(175 ^ [], 176 ^ []), difference(175 ^ [], 176 ^ []), 175 ^ [], 175 ^ []]]))).
% 14.36/14.82 ncf('1.1.1.1.1.1.3.1',plain,[-(175 ^ [] = 175 ^ [])],extension(2 ^ 9,bind([[_32451], [175 ^ []]]))).
% 14.36/14.82 ncf('1.1.1.1.1.1.3.2',plain,[-(difference(175 ^ [], 176 ^ []) = difference(175 ^ [], 176 ^ []))],extension(2 ^ 9,bind([[_32451], [difference(175 ^ [], 176 ^ [])]]))).
% 14.36/14.82 ncf('1.1.1.1.1.2',plain,[-(162 ^ [intersection(175 ^ [], 176 ^ []), difference(175 ^ [], difference(175 ^ [], 176 ^ []))] = 162 ^ [intersection(175 ^ [], 176 ^ []), difference(175 ^ [], difference(175 ^ [], 176 ^ []))])],extension(2 ^ 7,bind([[_32451], [162 ^ [intersection(175 ^ [], 176 ^ []), difference(175 ^ [], difference(175 ^ [], 176 ^ []))]]]))).
% 14.36/14.82 ncf('1.1.1.1.1.3',plain,[-(difference(175 ^ [], difference(175 ^ [], 176 ^ [])) = intersection(175 ^ [], 176 ^ [])), 166 : -(member(162 ^ [intersection(175 ^ [], 176 ^ []), difference(175 ^ [], difference(175 ^ [], 176 ^ []))], difference(175 ^ [], difference(175 ^ [], 176 ^ [])))), 170 : -(member(162 ^ [intersection(175 ^ [], 176 ^ []), difference(175 ^ [], difference(175 ^ [], 176 ^ []))], intersection(175 ^ [], 176 ^ [])))],extension(161 ^ 7,bind([[_37852, _37854], [intersection(175 ^ [], 176 ^ []), difference(175 ^ [], difference(175 ^ [], 176 ^ []))]]))).
% 14.36/14.82 ncf('1.1.1.1.1.3.1',plain,[member(162 ^ [intersection(175 ^ [], 176 ^ []), difference(175 ^ [], difference(175 ^ [], 176 ^ []))], difference(175 ^ [], difference(175 ^ [], 176 ^ []))), 90 : -(member(162 ^ [intersection(175 ^ [], 176 ^ []), difference(175 ^ [], difference(175 ^ [], 176 ^ []))], 175 ^ []))],extension(86 ^ 10,bind([[_35309, _35311, _35313], [162 ^ [intersection(175 ^ [], 176 ^ []), difference(175 ^ [], difference(175 ^ [], 176 ^ []))], difference(175 ^ [], 176 ^ []), 175 ^ []]]))).
% 14.36/14.82 ncf('1.1.1.1.1.3.1.1',plain,[member(162 ^ [intersection(175 ^ [], 176 ^ []), difference(175 ^ [], difference(175 ^ [], 176 ^ []))], 175 ^ [])],reduction('1.1.1')).
% 14.36/14.82 ncf('1.1.1.1.1.3.2',plain,[member(162 ^ [intersection(175 ^ [], 176 ^ []), difference(175 ^ [], difference(175 ^ [], 176 ^ []))], intersection(175 ^ [], 176 ^ []))],reduction('1.1.1.1')).
% 14.36/14.82 ncf('1.1.1.2',plain,[-(member(162 ^ [intersection(175 ^ [], 176 ^ []), difference(175 ^ [], difference(175 ^ [], 176 ^ []))], 176 ^ [])), 128 : member(162 ^ [intersection(175 ^ [], 176 ^ []), difference(175 ^ [], difference(175 ^ [], 176 ^ []))], difference(175 ^ [], difference(175 ^ [], 176 ^ []))), 128 : subset(difference(175 ^ [], difference(175 ^ [], 176 ^ [])), 176 ^ [])],extension(124 ^ 5,bind([[_36577, _36579, _36714], [176 ^ [], difference(175 ^ [], difference(175 ^ [], 176 ^ [])), 162 ^ [intersection(175 ^ [], 176 ^ []), difference(175 ^ [], difference(175 ^ [], 176 ^ []))]]]))).
% 14.36/14.82 ncf('1.1.1.2.1',plain,[-(member(162 ^ [intersection(175 ^ [], 176 ^ []), difference(175 ^ [], difference(175 ^ [], 176 ^ []))], difference(175 ^ [], difference(175 ^ [], 176 ^ [])))), member(162 ^ [intersection(175 ^ [], 176 ^ []), difference(175 ^ [], difference(175 ^ [], 176 ^ []))], difference(175 ^ [], difference(175 ^ [], 176 ^ []))), 162 ^ [intersection(175 ^ [], 176 ^ []), difference(175 ^ [], difference(175 ^ [], 176 ^ []))] = 162 ^ [intersection(175 ^ [], 176 ^ []), difference(175 ^ [], difference(175 ^ [], 176 ^ []))], difference(175 ^ [], difference(175 ^ [], 176 ^ [])) = difference(175 ^ [], difference(175 ^ [], 176 ^ []))],extension(34 ^ 8,bind([[_33527, _33529, _33531, _33533], [difference(175 ^ [], difference(175 ^ [], 176 ^ [])), difference(175 ^ [], difference(175 ^ [], 176 ^ [])), 162 ^ [intersection(175 ^ [], 176 ^ []), difference(175 ^ [], difference(175 ^ [], 176 ^ []))], 162 ^ [intersection(175 ^ [], 176 ^ []), difference(175 ^ [], difference(175 ^ [], 176 ^ []))]]]))).
% 14.36/14.82 ncf('1.1.1.2.1.1',plain,[-(member(162 ^ [intersection(175 ^ [], 176 ^ []), difference(175 ^ [], difference(175 ^ [], 176 ^ []))], difference(175 ^ [], difference(175 ^ [], 176 ^ [])))), member(162 ^ [intersection(175 ^ [], 176 ^ []), difference(175 ^ [], difference(175 ^ [], 176 ^ []))], difference(175 ^ [], difference(175 ^ [], 176 ^ []))), 162 ^ [intersection(175 ^ [], 176 ^ []), difference(175 ^ [], difference(175 ^ [], 176 ^ []))] = 162 ^ [intersection(175 ^ [], 176 ^ []), difference(175 ^ [], difference(175 ^ [], 176 ^ []))], difference(175 ^ [], difference(175 ^ [], 176 ^ [])) = difference(175 ^ [], difference(175 ^ [], 176 ^ []))],extension(34 ^ 9,bind([[_33527, _33529, _33531, _33533], [difference(175 ^ [], difference(175 ^ [], 176 ^ [])), difference(175 ^ [], difference(175 ^ [], 176 ^ [])), 162 ^ [intersection(175 ^ [], 176 ^ []), difference(175 ^ [], difference(175 ^ [], 176 ^ []))], 162 ^ [intersection(175 ^ [], 176 ^ []), difference(175 ^ [], difference(175 ^ [], 176 ^ []))]]]))).
% 14.36/14.82 ncf('1.1.1.2.1.1.1',plain,[-(member(162 ^ [intersection(175 ^ [], 176 ^ []), difference(175 ^ [], difference(175 ^ [], 176 ^ []))], difference(175 ^ [], difference(175 ^ [], 176 ^ [])))), member(162 ^ [intersection(175 ^ [], 176 ^ []), difference(175 ^ [], difference(175 ^ [], 176 ^ []))], difference(175 ^ [], difference(175 ^ [], 176 ^ []))), 162 ^ [intersection(175 ^ [], 176 ^ []), difference(175 ^ [], difference(175 ^ [], 176 ^ []))] = 162 ^ [intersection(175 ^ [], 176 ^ []), difference(175 ^ [], difference(175 ^ [], 176 ^ []))], difference(175 ^ [], difference(175 ^ [], 176 ^ [])) = difference(175 ^ [], difference(175 ^ [], 176 ^ []))],extension(34 ^ 10,bind([[_33527, _33529, _33531, _33533], [difference(175 ^ [], difference(175 ^ [], 176 ^ [])), difference(175 ^ [], difference(175 ^ [], 176 ^ [])), 162 ^ [intersection(175 ^ [], 176 ^ []), difference(175 ^ [], difference(175 ^ [], 176 ^ []))], 162 ^ [intersection(175 ^ [], 176 ^ []), difference(175 ^ [], difference(175 ^ [], 176 ^ []))]]]))).
% 14.36/14.82 ncf('1.1.1.2.1.1.1.1',plain,[-(member(162 ^ [intersection(175 ^ [], 176 ^ []), difference(175 ^ [], difference(175 ^ [], 176 ^ []))], difference(175 ^ [], difference(175 ^ [], 176 ^ []))))],extension(166 ^ 11)).
% 14.36/14.82 ncf('1.1.1.2.1.1.1.2',plain,[-(162 ^ [intersection(175 ^ [], 176 ^ []), difference(175 ^ [], difference(175 ^ [], 176 ^ []))] = 162 ^ [intersection(175 ^ [], 176 ^ []), difference(175 ^ [], difference(175 ^ [], 176 ^ []))])],extension(2 ^ 11,bind([[_32451], [162 ^ [intersection(175 ^ [], 176 ^ []), difference(175 ^ [], difference(175 ^ [], 176 ^ []))]]]))).
% 14.36/14.82 ncf('1.1.1.2.1.1.1.3',plain,[-(difference(175 ^ [], difference(175 ^ [], 176 ^ [])) = difference(175 ^ [], difference(175 ^ [], 176 ^ [])))],extension(2 ^ 11,bind([[_32451], [difference(175 ^ [], difference(175 ^ [], 176 ^ []))]]))).
% 14.36/14.82 ncf('1.1.1.2.1.1.2',plain,[-(162 ^ [intersection(175 ^ [], 176 ^ []), difference(175 ^ [], difference(175 ^ [], 176 ^ []))] = 162 ^ [intersection(175 ^ [], 176 ^ []), difference(175 ^ [], difference(175 ^ [], 176 ^ []))])],extension(2 ^ 10,bind([[_32451], [162 ^ [intersection(175 ^ [], 176 ^ []), difference(175 ^ [], difference(175 ^ [], 176 ^ []))]]]))).
% 14.36/14.82 ncf('1.1.1.2.1.1.3',plain,[-(difference(175 ^ [], difference(175 ^ [], 176 ^ [])) = difference(175 ^ [], difference(175 ^ [], 176 ^ []))), 175 ^ [] = 175 ^ [], difference(175 ^ [], 176 ^ []) = difference(175 ^ [], 176 ^ [])],extension(48 ^ 10,bind([[_33979, _33981, _33983, _33985], [difference(175 ^ [], 176 ^ []), difference(175 ^ [], 176 ^ []), 175 ^ [], 175 ^ []]]))).
% 14.36/14.82 ncf('1.1.1.2.1.1.3.1',plain,[-(175 ^ [] = 175 ^ [])],extension(2 ^ 11,bind([[_32451], [175 ^ []]]))).
% 14.36/14.82 ncf('1.1.1.2.1.1.3.2',plain,[-(difference(175 ^ [], 176 ^ []) = difference(175 ^ [], 176 ^ []))],extension(2 ^ 11,bind([[_32451], [difference(175 ^ [], 176 ^ [])]]))).
% 14.36/14.82 ncf('1.1.1.2.1.2',plain,[-(162 ^ [intersection(175 ^ [], 176 ^ []), difference(175 ^ [], difference(175 ^ [], 176 ^ []))] = 162 ^ [intersection(175 ^ [], 176 ^ []), difference(175 ^ [], difference(175 ^ [], 176 ^ []))])],extension(2 ^ 9,bind([[_32451], [162 ^ [intersection(175 ^ [], 176 ^ []), difference(175 ^ [], difference(175 ^ [], 176 ^ []))]]]))).
% 14.36/14.82 ncf('1.1.1.2.1.3',plain,[-(difference(175 ^ [], difference(175 ^ [], 176 ^ [])) = difference(175 ^ [], difference(175 ^ [], 176 ^ []))), 175 ^ [] = 175 ^ [], difference(175 ^ [], 176 ^ []) = difference(175 ^ [], 176 ^ [])],extension(48 ^ 9,bind([[_33979, _33981, _33983, _33985], [difference(175 ^ [], 176 ^ []), difference(175 ^ [], 176 ^ []), 175 ^ [], 175 ^ []]]))).
% 14.36/14.82 ncf('1.1.1.2.1.3.1',plain,[-(175 ^ [] = 175 ^ [])],extension(2 ^ 10,bind([[_32451], [175 ^ []]]))).
% 14.36/14.82 ncf('1.1.1.2.1.3.2',plain,[-(difference(175 ^ [], 176 ^ []) = difference(175 ^ [], 176 ^ [])), 175 ^ [] = 175 ^ [], 176 ^ [] = 176 ^ []],extension(48 ^ 10,bind([[_33979, _33981, _33983, _33985], [176 ^ [], 176 ^ [], 175 ^ [], 175 ^ []]]))).
% 14.36/14.82 ncf('1.1.1.2.1.3.2.1',plain,[-(175 ^ [] = 175 ^ [])],extension(2 ^ 11,bind([[_32451], [175 ^ []]]))).
% 14.36/14.82 ncf('1.1.1.2.1.3.2.2',plain,[-(176 ^ [] = 176 ^ [])],extension(2 ^ 11,bind([[_32451], [176 ^ []]]))).
% 14.36/14.82 ncf('1.1.1.2.2',plain,[-(subset(difference(175 ^ [], difference(175 ^ [], 176 ^ [])), 176 ^ [])), 137 : -(member(135 ^ [176 ^ [], difference(175 ^ [], difference(175 ^ [], 176 ^ []))], difference(175 ^ [], difference(175 ^ [], 176 ^ []))))],extension(134 ^ 6,bind([[_36891, _36893], [176 ^ [], difference(175 ^ [], difference(175 ^ [], 176 ^ []))]]))).
% 14.36/14.82 ncf('1.1.1.2.2.1',plain,[member(135 ^ [176 ^ [], difference(175 ^ [], difference(175 ^ [], 176 ^ []))], difference(175 ^ [], difference(175 ^ [], 176 ^ []))), 92 : member(135 ^ [176 ^ [], difference(175 ^ [], difference(175 ^ [], 176 ^ []))], difference(175 ^ [], 176 ^ []))],extension(86 ^ 9,bind([[_35309, _35311, _35313], [135 ^ [176 ^ [], difference(175 ^ [], difference(175 ^ [], 176 ^ []))], difference(175 ^ [], 176 ^ []), 175 ^ []]]))).
% 14.36/14.82 ncf('1.1.1.2.2.1.1',plain,[-(member(135 ^ [176 ^ [], difference(175 ^ [], difference(175 ^ [], 176 ^ []))], difference(175 ^ [], 176 ^ []))), member(135 ^ [176 ^ [], difference(175 ^ [], difference(175 ^ [], 176 ^ []))], 175 ^ []), -(member(135 ^ [176 ^ [], difference(175 ^ [], difference(175 ^ [], 176 ^ []))], 176 ^ []))],extension(94 ^ 12,bind([[_35561, _35563, _35565], [135 ^ [176 ^ [], difference(175 ^ [], difference(175 ^ [], 176 ^ []))], 176 ^ [], 175 ^ []]]))).
% 14.36/14.82 ncf('1.1.1.2.2.1.1.1',plain,[-(member(135 ^ [176 ^ [], difference(175 ^ [], difference(175 ^ [], 176 ^ []))], 175 ^ []))],extension(90 ^ 13)).
% 14.36/14.82 ncf('1.1.1.2.2.1.1.2',plain,[member(135 ^ [176 ^ [], difference(175 ^ [], difference(175 ^ [], 176 ^ []))], 176 ^ [])],extension(139 ^ 13)).
% 14.36/14.82 ncf('1.1.2',plain,[-(member(162 ^ [intersection(175 ^ [], 176 ^ []), difference(175 ^ [], difference(175 ^ [], 176 ^ []))], difference(175 ^ [], difference(175 ^ [], 176 ^ [])))), member(162 ^ [intersection(175 ^ [], 176 ^ []), difference(175 ^ [], difference(175 ^ [], 176 ^ []))], 175 ^ []), -(member(162 ^ [intersection(175 ^ [], 176 ^ []), difference(175 ^ [], difference(175 ^ [], 176 ^ []))], difference(175 ^ [], 176 ^ [])))],extension(94 ^ 4,bind([[_35561, _35563, _35565], [162 ^ [intersection(175 ^ [], 176 ^ []), difference(175 ^ [], difference(175 ^ [], 176 ^ []))], difference(175 ^ [], 176 ^ []), 175 ^ []]]))).
% 14.36/14.82 ncf('1.1.2.1',plain,[-(member(162 ^ [intersection(175 ^ [], 176 ^ []), difference(175 ^ [], difference(175 ^ [], 176 ^ []))], 175 ^ [])), member(162 ^ [intersection(175 ^ [], 176 ^ []), difference(175 ^ [], difference(175 ^ [], 176 ^ []))], 175 ^ []), 162 ^ [intersection(175 ^ [], 176 ^ []), difference(175 ^ [], difference(175 ^ [], 176 ^ []))] = 162 ^ [intersection(175 ^ [], 176 ^ []), difference(175 ^ [], difference(175 ^ [], 176 ^ []))], 175 ^ [] = 175 ^ []],extension(34 ^ 5,bind([[_33527, _33529, _33531, _33533], [175 ^ [], 175 ^ [], 162 ^ [intersection(175 ^ [], 176 ^ []), difference(175 ^ [], difference(175 ^ [], 176 ^ []))], 162 ^ [intersection(175 ^ [], 176 ^ []), difference(175 ^ [], difference(175 ^ [], 176 ^ []))]]]))).
% 14.36/14.82 ncf('1.1.2.1.1',plain,[-(member(162 ^ [intersection(175 ^ [], 176 ^ []), difference(175 ^ [], difference(175 ^ [], 176 ^ []))], 175 ^ [])), member(162 ^ [intersection(175 ^ [], 176 ^ []), difference(175 ^ [], difference(175 ^ [], 176 ^ []))], 175 ^ []), 162 ^ [intersection(175 ^ [], 176 ^ []), difference(175 ^ [], difference(175 ^ [], 176 ^ []))] = 162 ^ [intersection(175 ^ [], 176 ^ []), difference(175 ^ [], difference(175 ^ [], 176 ^ []))], 175 ^ [] = 175 ^ []],extension(34 ^ 6,bind([[_33527, _33529, _33531, _33533], [175 ^ [], 175 ^ [], 162 ^ [intersection(175 ^ [], 176 ^ []), difference(175 ^ [], difference(175 ^ [], 176 ^ []))], 162 ^ [intersection(175 ^ [], 176 ^ []), difference(175 ^ [], difference(175 ^ [], 176 ^ []))]]]))).
% 14.36/14.82 ncf('1.1.2.1.1.1',plain,[-(member(162 ^ [intersection(175 ^ [], 176 ^ []), difference(175 ^ [], difference(175 ^ [], 176 ^ []))], 175 ^ [])), member(162 ^ [intersection(175 ^ [], 176 ^ []), difference(175 ^ [], difference(175 ^ [], 176 ^ []))], 175 ^ []), 162 ^ [intersection(175 ^ [], 176 ^ []), difference(175 ^ [], difference(175 ^ [], 176 ^ []))] = 162 ^ [intersection(175 ^ [], 176 ^ []), difference(175 ^ [], difference(175 ^ [], 176 ^ []))], 175 ^ [] = 175 ^ []],extension(34 ^ 7,bind([[_33527, _33529, _33531, _33533], [175 ^ [], 175 ^ [], 162 ^ [intersection(175 ^ [], 176 ^ []), difference(175 ^ [], difference(175 ^ [], 176 ^ []))], 162 ^ [intersection(175 ^ [], 176 ^ []), difference(175 ^ [], difference(175 ^ [], 176 ^ []))]]]))).
% 14.36/14.82 ncf('1.1.2.1.1.1.1',plain,[-(member(162 ^ [intersection(175 ^ [], 176 ^ []), difference(175 ^ [], difference(175 ^ [], 176 ^ []))], 175 ^ [])), member(162 ^ [intersection(175 ^ [], 176 ^ []), difference(175 ^ [], difference(175 ^ [], 176 ^ []))], intersection(175 ^ [], 176 ^ []))],extension(68 ^ 8,bind([[_34698, _34700, _34702], [162 ^ [intersection(175 ^ [], 176 ^ []), difference(175 ^ [], difference(175 ^ [], 176 ^ []))], 176 ^ [], 175 ^ []]]))).
% 14.36/14.82 ncf('1.1.2.1.1.1.1.1',plain,[-(member(162 ^ [intersection(175 ^ [], 176 ^ []), difference(175 ^ [], difference(175 ^ [], 176 ^ []))], intersection(175 ^ [], 176 ^ [])))],extension(170 ^ 9)).
% 14.36/14.82 ncf('1.1.2.1.1.1.2',plain,[-(162 ^ [intersection(175 ^ [], 176 ^ []), difference(175 ^ [], difference(175 ^ [], 176 ^ []))] = 162 ^ [intersection(175 ^ [], 176 ^ []), difference(175 ^ [], difference(175 ^ [], 176 ^ []))])],extension(2 ^ 8,bind([[_32451], [162 ^ [intersection(175 ^ [], 176 ^ []), difference(175 ^ [], difference(175 ^ [], 176 ^ []))]]]))).
% 14.36/14.82 ncf('1.1.2.1.1.1.3',plain,[-(175 ^ [] = 175 ^ [])],extension(2 ^ 8,bind([[_32451], [175 ^ []]]))).
% 14.36/14.82 ncf('1.1.2.1.1.2',plain,[-(162 ^ [intersection(175 ^ [], 176 ^ []), difference(175 ^ [], difference(175 ^ [], 176 ^ []))] = 162 ^ [intersection(175 ^ [], 176 ^ []), difference(175 ^ [], difference(175 ^ [], 176 ^ []))])],extension(2 ^ 7,bind([[_32451], [162 ^ [intersection(175 ^ [], 176 ^ []), difference(175 ^ [], difference(175 ^ [], 176 ^ []))]]]))).
% 14.36/14.82 ncf('1.1.2.1.1.3',plain,[-(175 ^ [] = 175 ^ [])],extension(2 ^ 7,bind([[_32451], [175 ^ []]]))).
% 14.36/14.82 ncf('1.1.2.1.2',plain,[-(162 ^ [intersection(175 ^ [], 176 ^ []), difference(175 ^ [], difference(175 ^ [], 176 ^ []))] = 162 ^ [intersection(175 ^ [], 176 ^ []), difference(175 ^ [], difference(175 ^ [], 176 ^ []))])],extension(2 ^ 6,bind([[_32451], [162 ^ [intersection(175 ^ [], 176 ^ []), difference(175 ^ [], difference(175 ^ [], 176 ^ []))]]]))).
% 14.36/14.82 ncf('1.1.2.1.3',plain,[-(175 ^ [] = 175 ^ [])],extension(2 ^ 6,bind([[_32451], [175 ^ []]]))).
% 14.36/14.82 ncf('1.1.2.2',plain,[member(162 ^ [intersection(175 ^ [], 176 ^ []), difference(175 ^ [], difference(175 ^ [], 176 ^ []))], difference(175 ^ [], 176 ^ [])), 92 : member(162 ^ [intersection(175 ^ [], 176 ^ []), difference(175 ^ [], difference(175 ^ [], 176 ^ []))], 176 ^ [])],extension(86 ^ 5,bind([[_35309, _35311, _35313], [162 ^ [intersection(175 ^ [], 176 ^ []), difference(175 ^ [], difference(175 ^ [], 176 ^ []))], 176 ^ [], 175 ^ []]]))).
% 14.36/14.82 ncf('1.1.2.2.1',plain,[-(member(162 ^ [intersection(175 ^ [], 176 ^ []), difference(175 ^ [], difference(175 ^ [], 176 ^ []))], 176 ^ [])), member(162 ^ [intersection(175 ^ [], 176 ^ []), difference(175 ^ [], difference(175 ^ [], 176 ^ []))], intersection(175 ^ [], 176 ^ []))],extension(68 ^ 8,bind([[_34698, _34700, _34702], [162 ^ [intersection(175 ^ [], 176 ^ []), difference(175 ^ [], difference(175 ^ [], 176 ^ []))], 176 ^ [], 175 ^ []]]))).
% 14.36/14.82 ncf('1.1.2.2.1.1',plain,[-(member(162 ^ [intersection(175 ^ [], 176 ^ []), difference(175 ^ [], difference(175 ^ [], 176 ^ []))], intersection(175 ^ [], 176 ^ [])))],extension(170 ^ 9)).
% 14.36/14.82 %-----------------------------------------------------
% 14.36/14.82 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------