%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : SET612+3 : TPTP v8.1.2. Released v2.2.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n006.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 10.42s 10.69s
% Output : Proof 10.42s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : SET612+3 : TPTP v8.1.2. Released v2.2.0.
% 0.11/0.12 % Command : nanocop.sh %s %d
% 0.13/0.33 % Computer : n006.cluster.edu
% 0.13/0.33 % Model : x86_64 x86_64
% 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.33 % Memory : 8042.1875MB
% 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.33 % CPULimit : 300
% 0.13/0.33 % WCLimit : 300
% 0.13/0.34 % DateTime : Thu May 18 19:16:51 EDT 2023
% 0.13/0.34 % CPUTime :
% 10.42/10.69
% 10.42/10.69 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 10.42/10.69 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 10.42/10.69 %-----------------------------------------------------
% 10.42/10.69 ncf(matrix, plain, [(227 ^ _40325) ^ [] : [difference(223 ^ [], union(224 ^ [], 225 ^ [])) = intersection(difference(223 ^ [], 224 ^ []), difference(223 ^ [], 225 ^ []))], (48 ^ _40325) ^ [_41997, _41999, _42001, _42003] : [-(union(_42003, _41999) = union(_42001, _41997)), _42003 = _42001, _41999 = _41997], (58 ^ _40325) ^ [_42356, _42358, _42360, _42362] : [-(intersection(_42362, _42358) = intersection(_42360, _42356)), _42362 = _42360, _42358 = _42356], (68 ^ _40325) ^ [_42695, _42697, _42699, _42701] : [-(difference(_42701, _42697) = difference(_42699, _42695)), _42701 = _42699, _42697 = _42695], (2 ^ _40325) ^ [_40469] : [-(_40469 = _40469)], (4 ^ _40325) ^ [_40576, _40578] : [_40578 = _40576, -(_40576 = _40578)], (10 ^ _40325) ^ [_40780, _40782, _40784] : [-(_40784 = _40780), _40784 = _40782, _40782 = _40780], (20 ^ _40325) ^ [_41121, _41123, _41125, _41127] : [-(subset(_41125, _41121)), subset(_41127, _41123), _41127 = _41125, _41123 = _41121], (34 ^ _40325) ^ [_41545, _41547, _41549, _41551] : [-(member(_41549, _41545)), member(_41551, _41547), _41551 = _41549, _41547 = _41545], (88 ^ _40325) ^ [_43347, _43349, _43351] : [89 ^ _40325 : [(90 ^ _40325) ^ [] : [member(_43347, _43351)], (92 ^ _40325) ^ [] : [member(_43347, _43349)]], -(member(_43347, union(_43351, _43349)))], (78 ^ _40325) ^ [_43079, _43081, _43083] : [member(_43079, union(_43083, _43081)), -(member(_43079, _43083)), -(member(_43079, _43081))], (96 ^ _40325) ^ [_43690, _43692, _43694] : [member(_43690, intersection(_43694, _43692)), 99 ^ _40325 : [(100 ^ _40325) ^ [] : [-(member(_43690, _43694))], (102 ^ _40325) ^ [] : [-(member(_43690, _43692))]]], (104 ^ _40325) ^ [_43941, _43943, _43945] : [-(member(_43941, intersection(_43945, _43943))), member(_43941, _43945), member(_43941, _43943)], (114 ^ _40325) ^ [_44301, _44303, _44305] : [member(_44301, difference(_44305, _44303)), 117 ^ _40325 : [(118 ^ _40325) ^ [] : [-(member(_44301, _44305))], (120 ^ _40325) ^ [] : [member(_44301, _44303)]]], (122 ^ _40325) ^ [_44553, _44555, _44557] : [-(member(_44553, difference(_44557, _44555))), member(_44553, _44557), -(member(_44553, _44555))], (132 ^ _40325) ^ [_44858, _44860] : [-(subset(_44860, union(_44860, _44858)))], (134 ^ _40325) ^ [_44984, _44986, _44988] : [-(subset(_44988, intersection(_44986, _44984))), subset(_44988, _44986), subset(_44988, _44984)], (144 ^ _40325) ^ [_45313, _45315, _45317] : [subset(_45317, _45315), -(subset(difference(_45313, _45315), difference(_45313, _45317)))], (150 ^ _40325) ^ [_45570, _45572] : [_45572 = _45570, 153 ^ _40325 : [(154 ^ _40325) ^ [] : [-(subset(_45572, _45570))], (156 ^ _40325) ^ [] : [-(subset(_45570, _45572))]]], (158 ^ _40325) ^ [_45807, _45809] : [-(_45809 = _45807), subset(_45809, _45807), subset(_45807, _45809)], (168 ^ _40325) ^ [_46093, _46095] : [-(union(_46095, _46093) = union(_46093, _46095))], (170 ^ _40325) ^ [_46193, _46195] : [-(intersection(_46195, _46193) = intersection(_46193, _46195))], (182 ^ _40325) ^ [_46651, _46653] : [184 ^ _40325 : [(185 ^ _40325) ^ [] : [-(member(183 ^ [_46651, _46653], _46653))], (187 ^ _40325) ^ [] : [member(183 ^ [_46651, _46653], _46651)]], -(subset(_46653, _46651))], (172 ^ _40325) ^ [_46337, _46339] : [subset(_46339, _46337), 175 ^ _40325 : [(176 ^ _40325) ^ [_46474] : [member(_46474, _46339), -(member(_46474, _46337))]]], (191 ^ _40325) ^ [_46979] : [-(subset(_46979, _46979))], (209 ^ _40325) ^ [_47612, _47614] : [-(_47614 = _47612), 213 ^ _40325 : [(214 ^ _40325) ^ [] : [-(member(210 ^ [_47612, _47614], _47614))], (216 ^ _40325) ^ [] : [member(210 ^ [_47612, _47614], _47612)]], 217 ^ _40325 : [(218 ^ _40325) ^ [] : [-(member(210 ^ [_47612, _47614], _47612))], (220 ^ _40325) ^ [] : [member(210 ^ [_47612, _47614], _47614)]]], (193 ^ _40325) ^ [_47095, _47097] : [_47097 = _47095, 196 ^ _40325 : [(197 ^ _40325) ^ [_47261] : [member(_47261, _47097), -(member(_47261, _47095))], (203 ^ _40325) ^ [_47433] : [member(_47433, _47095), -(member(_47433, _47097))]]]], input).
% 10.42/10.69 ncf('1',plain,[difference(223 ^ [], union(224 ^ [], 225 ^ [])) = intersection(difference(223 ^ [], 224 ^ []), difference(223 ^ [], 225 ^ []))],start(227 ^ 0)).
% 10.42/10.69 ncf('1.1',plain,[-(difference(223 ^ [], union(224 ^ [], 225 ^ [])) = intersection(difference(223 ^ [], 224 ^ []), difference(223 ^ [], 225 ^ []))), 216 : member(210 ^ [intersection(difference(223 ^ [], 224 ^ []), difference(223 ^ [], 225 ^ [])), difference(223 ^ [], union(224 ^ [], 225 ^ []))], intersection(difference(223 ^ [], 224 ^ []), difference(223 ^ [], 225 ^ []))), 220 : member(210 ^ [intersection(difference(223 ^ [], 224 ^ []), difference(223 ^ [], 225 ^ [])), difference(223 ^ [], union(224 ^ [], 225 ^ []))], difference(223 ^ [], union(224 ^ [], 225 ^ [])))],extension(209 ^ 1,bind([[_47612, _47614], [intersection(difference(223 ^ [], 224 ^ []), difference(223 ^ [], 225 ^ [])), difference(223 ^ [], union(224 ^ [], 225 ^ []))]]))).
% 10.42/10.69 ncf('1.1.1',plain,[-(member(210 ^ [intersection(difference(223 ^ [], 224 ^ []), difference(223 ^ [], 225 ^ [])), difference(223 ^ [], union(224 ^ [], 225 ^ []))], intersection(difference(223 ^ [], 224 ^ []), difference(223 ^ [], 225 ^ [])))), member(210 ^ [intersection(difference(223 ^ [], 224 ^ []), difference(223 ^ [], 225 ^ [])), difference(223 ^ [], union(224 ^ [], 225 ^ []))], difference(223 ^ [], 224 ^ [])), member(210 ^ [intersection(difference(223 ^ [], 224 ^ []), difference(223 ^ [], 225 ^ [])), difference(223 ^ [], union(224 ^ [], 225 ^ []))], difference(223 ^ [], 225 ^ []))],extension(104 ^ 4,bind([[_43941, _43943, _43945], [210 ^ [intersection(difference(223 ^ [], 224 ^ []), difference(223 ^ [], 225 ^ [])), difference(223 ^ [], union(224 ^ [], 225 ^ []))], difference(223 ^ [], 225 ^ []), difference(223 ^ [], 224 ^ [])]]))).
% 10.42/10.69 ncf('1.1.1.1',plain,[-(member(210 ^ [intersection(difference(223 ^ [], 224 ^ []), difference(223 ^ [], 225 ^ [])), difference(223 ^ [], union(224 ^ [], 225 ^ []))], difference(223 ^ [], 224 ^ []))), member(210 ^ [intersection(difference(223 ^ [], 224 ^ []), difference(223 ^ [], 225 ^ [])), difference(223 ^ [], union(224 ^ [], 225 ^ []))], union(difference(223 ^ [], 224 ^ []), difference(223 ^ [], union(224 ^ [], 225 ^ [])))), -(member(210 ^ [intersection(difference(223 ^ [], 224 ^ []), difference(223 ^ [], 225 ^ [])), difference(223 ^ [], union(224 ^ [], 225 ^ []))], difference(223 ^ [], union(224 ^ [], 225 ^ []))))],extension(78 ^ 5,bind([[_43079, _43081, _43083], [210 ^ [intersection(difference(223 ^ [], 224 ^ []), difference(223 ^ [], 225 ^ [])), difference(223 ^ [], union(224 ^ [], 225 ^ []))], difference(223 ^ [], union(224 ^ [], 225 ^ [])), difference(223 ^ [], 224 ^ [])]]))).
% 10.42/10.69 ncf('1.1.1.1.1',plain,[-(member(210 ^ [intersection(difference(223 ^ [], 224 ^ []), difference(223 ^ [], 225 ^ [])), difference(223 ^ [], union(224 ^ [], 225 ^ []))], union(difference(223 ^ [], 224 ^ []), difference(223 ^ [], union(224 ^ [], 225 ^ []))))), 92 : member(210 ^ [intersection(difference(223 ^ [], 224 ^ []), difference(223 ^ [], 225 ^ [])), difference(223 ^ [], union(224 ^ [], 225 ^ []))], difference(223 ^ [], union(224 ^ [], 225 ^ [])))],extension(88 ^ 6,bind([[_43347, _43349, _43351], [210 ^ [intersection(difference(223 ^ [], 224 ^ []), difference(223 ^ [], 225 ^ [])), difference(223 ^ [], union(224 ^ [], 225 ^ []))], difference(223 ^ [], union(224 ^ [], 225 ^ [])), difference(223 ^ [], 224 ^ [])]]))).
% 10.42/10.69 ncf('1.1.1.1.1.1',plain,[-(member(210 ^ [intersection(difference(223 ^ [], 224 ^ []), difference(223 ^ [], 225 ^ [])), difference(223 ^ [], union(224 ^ [], 225 ^ []))], difference(223 ^ [], union(224 ^ [], 225 ^ [])))), member(210 ^ [intersection(difference(223 ^ [], 224 ^ []), difference(223 ^ [], 225 ^ [])), difference(223 ^ [], union(224 ^ [], 225 ^ []))], difference(223 ^ [], union(224 ^ [], 225 ^ []))), 210 ^ [intersection(difference(223 ^ [], 224 ^ []), difference(223 ^ [], 225 ^ [])), difference(223 ^ [], union(224 ^ [], 225 ^ []))] = 210 ^ [intersection(difference(223 ^ [], 224 ^ []), difference(223 ^ [], 225 ^ [])), difference(223 ^ [], union(224 ^ [], 225 ^ []))], difference(223 ^ [], union(224 ^ [], 225 ^ [])) = difference(223 ^ [], union(224 ^ [], 225 ^ []))],extension(34 ^ 9,bind([[_41545, _41547, _41549, _41551], [difference(223 ^ [], union(224 ^ [], 225 ^ [])), difference(223 ^ [], union(224 ^ [], 225 ^ [])), 210 ^ [intersection(difference(223 ^ [], 224 ^ []), difference(223 ^ [], 225 ^ [])), difference(223 ^ [], union(224 ^ [], 225 ^ []))], 210 ^ [intersection(difference(223 ^ [], 224 ^ []), difference(223 ^ [], 225 ^ [])), difference(223 ^ [], union(224 ^ [], 225 ^ []))]]]))).
% 10.42/10.69 ncf('1.1.1.1.1.1.1',plain,[-(member(210 ^ [intersection(difference(223 ^ [], 224 ^ []), difference(223 ^ [], 225 ^ [])), difference(223 ^ [], union(224 ^ [], 225 ^ []))], difference(223 ^ [], union(224 ^ [], 225 ^ []))))],extension(214 ^ 10)).
% 10.42/10.69 ncf('1.1.1.1.1.1.2',plain,[-(210 ^ [intersection(difference(223 ^ [], 224 ^ []), difference(223 ^ [], 225 ^ [])), difference(223 ^ [], union(224 ^ [], 225 ^ []))] = 210 ^ [intersection(difference(223 ^ [], 224 ^ []), difference(223 ^ [], 225 ^ [])), difference(223 ^ [], union(224 ^ [], 225 ^ []))])],extension(2 ^ 10,bind([[_40469], [210 ^ [intersection(difference(223 ^ [], 224 ^ []), difference(223 ^ [], 225 ^ [])), difference(223 ^ [], union(224 ^ [], 225 ^ []))]]]))).
% 10.42/10.69 ncf('1.1.1.1.1.1.3',plain,[-(difference(223 ^ [], union(224 ^ [], 225 ^ [])) = difference(223 ^ [], union(224 ^ [], 225 ^ [])))],extension(2 ^ 10,bind([[_40469], [difference(223 ^ [], union(224 ^ [], 225 ^ []))]]))).
% 10.42/10.69 ncf('1.1.1.1.2',plain,[member(210 ^ [intersection(difference(223 ^ [], 224 ^ []), difference(223 ^ [], 225 ^ [])), difference(223 ^ [], union(224 ^ [], 225 ^ []))], difference(223 ^ [], union(224 ^ [], 225 ^ []))), 176 : -(member(210 ^ [intersection(difference(223 ^ [], 224 ^ []), difference(223 ^ [], 225 ^ [])), difference(223 ^ [], union(224 ^ [], 225 ^ []))], difference(223 ^ [], 224 ^ []))), 176 : subset(difference(223 ^ [], union(224 ^ [], 225 ^ [])), difference(223 ^ [], 224 ^ []))],extension(172 ^ 6,bind([[_46337, _46339, _46474], [difference(223 ^ [], 224 ^ []), difference(223 ^ [], union(224 ^ [], 225 ^ [])), 210 ^ [intersection(difference(223 ^ [], 224 ^ []), difference(223 ^ [], 225 ^ [])), difference(223 ^ [], union(224 ^ [], 225 ^ []))]]]))).
% 10.42/10.69 ncf('1.1.1.1.2.1',plain,[member(210 ^ [intersection(difference(223 ^ [], 224 ^ []), difference(223 ^ [], 225 ^ [])), difference(223 ^ [], union(224 ^ [], 225 ^ []))], difference(223 ^ [], 224 ^ []))],reduction('1.1.1')).
% 10.42/10.69 ncf('1.1.1.1.2.2',plain,[-(subset(difference(223 ^ [], union(224 ^ [], 225 ^ [])), difference(223 ^ [], 224 ^ []))), subset(224 ^ [], union(224 ^ [], 225 ^ []))],extension(144 ^ 7,bind([[_45313, _45315, _45317], [223 ^ [], union(224 ^ [], 225 ^ []), 224 ^ []]]))).
% 10.42/10.69 ncf('1.1.1.1.2.2.1',plain,[-(subset(224 ^ [], union(224 ^ [], 225 ^ [])))],extension(132 ^ 8,bind([[_44858, _44860], [225 ^ [], 224 ^ []]]))).
% 10.42/10.69 ncf('1.1.1.2',plain,[-(member(210 ^ [intersection(difference(223 ^ [], 224 ^ []), difference(223 ^ [], 225 ^ [])), difference(223 ^ [], union(224 ^ [], 225 ^ []))], difference(223 ^ [], 225 ^ []))), member(210 ^ [intersection(difference(223 ^ [], 224 ^ []), difference(223 ^ [], 225 ^ [])), difference(223 ^ [], union(224 ^ [], 225 ^ []))], 223 ^ []), -(member(210 ^ [intersection(difference(223 ^ [], 224 ^ []), difference(223 ^ [], 225 ^ [])), difference(223 ^ [], union(224 ^ [], 225 ^ []))], 225 ^ []))],extension(122 ^ 5,bind([[_44553, _44555, _44557], [210 ^ [intersection(difference(223 ^ [], 224 ^ []), difference(223 ^ [], 225 ^ [])), difference(223 ^ [], union(224 ^ [], 225 ^ []))], 225 ^ [], 223 ^ []]]))).
% 10.42/10.69 ncf('1.1.1.2.1',plain,[-(member(210 ^ [intersection(difference(223 ^ [], 224 ^ []), difference(223 ^ [], 225 ^ [])), difference(223 ^ [], union(224 ^ [], 225 ^ []))], 223 ^ [])), member(210 ^ [intersection(difference(223 ^ [], 224 ^ []), difference(223 ^ [], 225 ^ [])), difference(223 ^ [], union(224 ^ [], 225 ^ []))], union(223 ^ [], difference(223 ^ [], union(224 ^ [], 225 ^ [])))), -(member(210 ^ [intersection(difference(223 ^ [], 224 ^ []), difference(223 ^ [], 225 ^ [])), difference(223 ^ [], union(224 ^ [], 225 ^ []))], difference(223 ^ [], union(224 ^ [], 225 ^ []))))],extension(78 ^ 6,bind([[_43079, _43081, _43083], [210 ^ [intersection(difference(223 ^ [], 224 ^ []), difference(223 ^ [], 225 ^ [])), difference(223 ^ [], union(224 ^ [], 225 ^ []))], difference(223 ^ [], union(224 ^ [], 225 ^ [])), 223 ^ []]]))).
% 10.42/10.69 ncf('1.1.1.2.1.1',plain,[-(member(210 ^ [intersection(difference(223 ^ [], 224 ^ []), difference(223 ^ [], 225 ^ [])), difference(223 ^ [], union(224 ^ [], 225 ^ []))], union(223 ^ [], difference(223 ^ [], union(224 ^ [], 225 ^ []))))), 92 : member(210 ^ [intersection(difference(223 ^ [], 224 ^ []), difference(223 ^ [], 225 ^ [])), difference(223 ^ [], union(224 ^ [], 225 ^ []))], difference(223 ^ [], union(224 ^ [], 225 ^ [])))],extension(88 ^ 7,bind([[_43347, _43349, _43351], [210 ^ [intersection(difference(223 ^ [], 224 ^ []), difference(223 ^ [], 225 ^ [])), difference(223 ^ [], union(224 ^ [], 225 ^ []))], difference(223 ^ [], union(224 ^ [], 225 ^ [])), 223 ^ []]]))).
% 10.42/10.69 ncf('1.1.1.2.1.1.1',plain,[-(member(210 ^ [intersection(difference(223 ^ [], 224 ^ []), difference(223 ^ [], 225 ^ [])), difference(223 ^ [], union(224 ^ [], 225 ^ []))], difference(223 ^ [], union(224 ^ [], 225 ^ []))))],extension(214 ^ 10)).
% 10.42/10.69 ncf('1.1.1.2.1.2',plain,[member(210 ^ [intersection(difference(223 ^ [], 224 ^ []), difference(223 ^ [], 225 ^ [])), difference(223 ^ [], union(224 ^ [], 225 ^ []))], difference(223 ^ [], union(224 ^ [], 225 ^ []))), 118 : -(member(210 ^ [intersection(difference(223 ^ [], 224 ^ []), difference(223 ^ [], 225 ^ [])), difference(223 ^ [], union(224 ^ [], 225 ^ []))], 223 ^ []))],extension(114 ^ 7,bind([[_44301, _44303, _44305], [210 ^ [intersection(difference(223 ^ [], 224 ^ []), difference(223 ^ [], 225 ^ [])), difference(223 ^ [], union(224 ^ [], 225 ^ []))], union(224 ^ [], 225 ^ []), 223 ^ []]]))).
% 10.42/10.69 ncf('1.1.1.2.1.2.1',plain,[member(210 ^ [intersection(difference(223 ^ [], 224 ^ []), difference(223 ^ [], 225 ^ [])), difference(223 ^ [], union(224 ^ [], 225 ^ []))], 223 ^ [])],reduction('1.1.1.2')).
% 10.42/10.69 ncf('1.1.1.2.2',plain,[member(210 ^ [intersection(difference(223 ^ [], 224 ^ []), difference(223 ^ [], 225 ^ [])), difference(223 ^ [], union(224 ^ [], 225 ^ []))], 225 ^ []), -(member(210 ^ [intersection(difference(223 ^ [], 224 ^ []), difference(223 ^ [], 225 ^ [])), difference(223 ^ [], union(224 ^ [], 225 ^ []))], union(224 ^ [], 225 ^ [])))],extension(88 ^ 6,bind([[_43347, _43349, _43351], [210 ^ [intersection(difference(223 ^ [], 224 ^ []), difference(223 ^ [], 225 ^ [])), difference(223 ^ [], union(224 ^ [], 225 ^ []))], 225 ^ [], 224 ^ []]]))).
% 10.42/10.69 ncf('1.1.1.2.2.1',plain,[member(210 ^ [intersection(difference(223 ^ [], 224 ^ []), difference(223 ^ [], 225 ^ [])), difference(223 ^ [], union(224 ^ [], 225 ^ []))], union(224 ^ [], 225 ^ [])), member(210 ^ [intersection(difference(223 ^ [], 224 ^ []), difference(223 ^ [], 225 ^ [])), difference(223 ^ [], union(224 ^ [], 225 ^ []))], difference(223 ^ [], union(224 ^ [], 225 ^ [])))],extension(114 ^ 7,bind([[_44301, _44303, _44305], [210 ^ [intersection(difference(223 ^ [], 224 ^ []), difference(223 ^ [], 225 ^ [])), difference(223 ^ [], union(224 ^ [], 225 ^ []))], union(224 ^ [], 225 ^ []), 223 ^ []]]))).
% 10.42/10.69 ncf('1.1.1.2.2.1.1',plain,[-(member(210 ^ [intersection(difference(223 ^ [], 224 ^ []), difference(223 ^ [], 225 ^ [])), difference(223 ^ [], union(224 ^ [], 225 ^ []))], difference(223 ^ [], union(224 ^ [], 225 ^ []))))],extension(214 ^ 8)).
% 10.42/10.69 ncf('1.1.2',plain,[-(member(210 ^ [intersection(difference(223 ^ [], 224 ^ []), difference(223 ^ [], 225 ^ [])), difference(223 ^ [], union(224 ^ [], 225 ^ []))], difference(223 ^ [], union(224 ^ [], 225 ^ [])))), member(210 ^ [intersection(difference(223 ^ [], 224 ^ []), difference(223 ^ [], 225 ^ [])), difference(223 ^ [], union(224 ^ [], 225 ^ []))], 223 ^ []), -(member(210 ^ [intersection(difference(223 ^ [], 224 ^ []), difference(223 ^ [], 225 ^ [])), difference(223 ^ [], union(224 ^ [], 225 ^ []))], union(224 ^ [], 225 ^ [])))],extension(122 ^ 4,bind([[_44553, _44555, _44557], [210 ^ [intersection(difference(223 ^ [], 224 ^ []), difference(223 ^ [], 225 ^ [])), difference(223 ^ [], union(224 ^ [], 225 ^ []))], union(224 ^ [], 225 ^ []), 223 ^ []]]))).
% 10.42/10.69 ncf('1.1.2.1',plain,[-(member(210 ^ [intersection(difference(223 ^ [], 224 ^ []), difference(223 ^ [], 225 ^ [])), difference(223 ^ [], union(224 ^ [], 225 ^ []))], 223 ^ [])), member(210 ^ [intersection(difference(223 ^ [], 224 ^ []), difference(223 ^ [], 225 ^ [])), difference(223 ^ [], union(224 ^ [], 225 ^ []))], union(223 ^ [], intersection(difference(223 ^ [], 224 ^ []), difference(223 ^ [], 225 ^ [])))), -(member(210 ^ [intersection(difference(223 ^ [], 224 ^ []), difference(223 ^ [], 225 ^ [])), difference(223 ^ [], union(224 ^ [], 225 ^ []))], intersection(difference(223 ^ [], 224 ^ []), difference(223 ^ [], 225 ^ []))))],extension(78 ^ 5,bind([[_43079, _43081, _43083], [210 ^ [intersection(difference(223 ^ [], 224 ^ []), difference(223 ^ [], 225 ^ [])), difference(223 ^ [], union(224 ^ [], 225 ^ []))], intersection(difference(223 ^ [], 224 ^ []), difference(223 ^ [], 225 ^ [])), 223 ^ []]]))).
% 10.42/10.69 ncf('1.1.2.1.1',plain,[-(member(210 ^ [intersection(difference(223 ^ [], 224 ^ []), difference(223 ^ [], 225 ^ [])), difference(223 ^ [], union(224 ^ [], 225 ^ []))], union(223 ^ [], intersection(difference(223 ^ [], 224 ^ []), difference(223 ^ [], 225 ^ []))))), member(210 ^ [intersection(difference(223 ^ [], 224 ^ []), difference(223 ^ [], 225 ^ [])), difference(223 ^ [], union(224 ^ [], 225 ^ []))], union(intersection(difference(223 ^ [], 224 ^ []), difference(223 ^ [], 225 ^ [])), 223 ^ [])), 210 ^ [intersection(difference(223 ^ [], 224 ^ []), difference(223 ^ [], 225 ^ [])), difference(223 ^ [], union(224 ^ [], 225 ^ []))] = 210 ^ [intersection(difference(223 ^ [], 224 ^ []), difference(223 ^ [], 225 ^ [])), difference(223 ^ [], union(224 ^ [], 225 ^ []))], union(intersection(difference(223 ^ [], 224 ^ []), difference(223 ^ [], 225 ^ [])), 223 ^ []) = union(223 ^ [], intersection(difference(223 ^ [], 224 ^ []), difference(223 ^ [], 225 ^ [])))],extension(34 ^ 6,bind([[_41545, _41547, _41549, _41551], [union(223 ^ [], intersection(difference(223 ^ [], 224 ^ []), difference(223 ^ [], 225 ^ []))), union(intersection(difference(223 ^ [], 224 ^ []), difference(223 ^ [], 225 ^ [])), 223 ^ []), 210 ^ [intersection(difference(223 ^ [], 224 ^ []), difference(223 ^ [], 225 ^ [])), difference(223 ^ [], union(224 ^ [], 225 ^ []))], 210 ^ [intersection(difference(223 ^ [], 224 ^ []), difference(223 ^ [], 225 ^ [])), difference(223 ^ [], union(224 ^ [], 225 ^ []))]]]))).
% 10.42/10.69 ncf('1.1.2.1.1.1',plain,[-(member(210 ^ [intersection(difference(223 ^ [], 224 ^ []), difference(223 ^ [], 225 ^ [])), difference(223 ^ [], union(224 ^ [], 225 ^ []))], union(intersection(difference(223 ^ [], 224 ^ []), difference(223 ^ [], 225 ^ [])), 223 ^ []))), 90 : member(210 ^ [intersection(difference(223 ^ [], 224 ^ []), difference(223 ^ [], 225 ^ [])), difference(223 ^ [], union(224 ^ [], 225 ^ []))], intersection(difference(223 ^ [], 224 ^ []), difference(223 ^ [], 225 ^ [])))],extension(88 ^ 7,bind([[_43347, _43349, _43351], [210 ^ [intersection(difference(223 ^ [], 224 ^ []), difference(223 ^ [], 225 ^ [])), difference(223 ^ [], union(224 ^ [], 225 ^ []))], 223 ^ [], intersection(difference(223 ^ [], 224 ^ []), difference(223 ^ [], 225 ^ []))]]))).
% 10.42/10.69 ncf('1.1.2.1.1.1.1',plain,[-(member(210 ^ [intersection(difference(223 ^ [], 224 ^ []), difference(223 ^ [], 225 ^ [])), difference(223 ^ [], union(224 ^ [], 225 ^ []))], intersection(difference(223 ^ [], 224 ^ []), difference(223 ^ [], 225 ^ []))))],extension(218 ^ 10)).
% 10.42/10.69 ncf('1.1.2.1.1.2',plain,[-(210 ^ [intersection(difference(223 ^ [], 224 ^ []), difference(223 ^ [], 225 ^ [])), difference(223 ^ [], union(224 ^ [], 225 ^ []))] = 210 ^ [intersection(difference(223 ^ [], 224 ^ []), difference(223 ^ [], 225 ^ [])), difference(223 ^ [], union(224 ^ [], 225 ^ []))])],extension(2 ^ 7,bind([[_40469], [210 ^ [intersection(difference(223 ^ [], 224 ^ []), difference(223 ^ [], 225 ^ [])), difference(223 ^ [], union(224 ^ [], 225 ^ []))]]]))).
% 10.42/10.69 ncf('1.1.2.1.1.3',plain,[-(union(intersection(difference(223 ^ [], 224 ^ []), difference(223 ^ [], 225 ^ [])), 223 ^ []) = union(223 ^ [], intersection(difference(223 ^ [], 224 ^ []), difference(223 ^ [], 225 ^ [])))), union(223 ^ [], intersection(difference(223 ^ [], 224 ^ []), difference(223 ^ [], 225 ^ []))) = union(intersection(difference(223 ^ [], 224 ^ []), difference(223 ^ [], 225 ^ [])), 223 ^ [])],extension(4 ^ 7,bind([[_40576, _40578], [union(intersection(difference(223 ^ [], 224 ^ []), difference(223 ^ [], 225 ^ [])), 223 ^ []), union(223 ^ [], intersection(difference(223 ^ [], 224 ^ []), difference(223 ^ [], 225 ^ [])))]]))).
% 10.42/10.69 ncf('1.1.2.1.1.3.1',plain,[-(union(223 ^ [], intersection(difference(223 ^ [], 224 ^ []), difference(223 ^ [], 225 ^ []))) = union(intersection(difference(223 ^ [], 224 ^ []), difference(223 ^ [], 225 ^ [])), 223 ^ []))],extension(168 ^ 8,bind([[_46093, _46095], [intersection(difference(223 ^ [], 224 ^ []), difference(223 ^ [], 225 ^ [])), 223 ^ []]]))).
% 10.42/10.69 ncf('1.1.2.1.2',plain,[member(210 ^ [intersection(difference(223 ^ [], 224 ^ []), difference(223 ^ [], 225 ^ [])), difference(223 ^ [], union(224 ^ [], 225 ^ []))], intersection(difference(223 ^ [], 224 ^ []), difference(223 ^ [], 225 ^ []))), 100 : -(member(210 ^ [intersection(difference(223 ^ [], 224 ^ []), difference(223 ^ [], 225 ^ [])), difference(223 ^ [], union(224 ^ [], 225 ^ []))], difference(223 ^ [], 224 ^ [])))],extension(96 ^ 6,bind([[_43690, _43692, _43694], [210 ^ [intersection(difference(223 ^ [], 224 ^ []), difference(223 ^ [], 225 ^ [])), difference(223 ^ [], union(224 ^ [], 225 ^ []))], difference(223 ^ [], 225 ^ []), difference(223 ^ [], 224 ^ [])]]))).
% 10.42/10.69 ncf('1.1.2.1.2.1',plain,[member(210 ^ [intersection(difference(223 ^ [], 224 ^ []), difference(223 ^ [], 225 ^ [])), difference(223 ^ [], union(224 ^ [], 225 ^ []))], difference(223 ^ [], 224 ^ [])), 118 : -(member(210 ^ [intersection(difference(223 ^ [], 224 ^ []), difference(223 ^ [], 225 ^ [])), difference(223 ^ [], union(224 ^ [], 225 ^ []))], 223 ^ []))],extension(114 ^ 9,bind([[_44301, _44303, _44305], [210 ^ [intersection(difference(223 ^ [], 224 ^ []), difference(223 ^ [], 225 ^ [])), difference(223 ^ [], union(224 ^ [], 225 ^ []))], 224 ^ [], 223 ^ []]]))).
% 10.42/10.69 ncf('1.1.2.1.2.1.1',plain,[member(210 ^ [intersection(difference(223 ^ [], 224 ^ []), difference(223 ^ [], 225 ^ [])), difference(223 ^ [], union(224 ^ [], 225 ^ []))], 223 ^ [])],reduction('1.1.2')).
% 10.42/10.69 ncf('1.1.2.2',plain,[member(210 ^ [intersection(difference(223 ^ [], 224 ^ []), difference(223 ^ [], 225 ^ [])), difference(223 ^ [], union(224 ^ [], 225 ^ []))], union(224 ^ [], 225 ^ [])), -(member(210 ^ [intersection(difference(223 ^ [], 224 ^ []), difference(223 ^ [], 225 ^ [])), difference(223 ^ [], union(224 ^ [], 225 ^ []))], 224 ^ [])), -(member(210 ^ [intersection(difference(223 ^ [], 224 ^ []), difference(223 ^ [], 225 ^ [])), difference(223 ^ [], union(224 ^ [], 225 ^ []))], 225 ^ []))],extension(78 ^ 5,bind([[_43079, _43081, _43083], [210 ^ [intersection(difference(223 ^ [], 224 ^ []), difference(223 ^ [], 225 ^ [])), difference(223 ^ [], union(224 ^ [], 225 ^ []))], 225 ^ [], 224 ^ []]]))).
% 10.42/10.69 ncf('1.1.2.2.1',plain,[member(210 ^ [intersection(difference(223 ^ [], 224 ^ []), difference(223 ^ [], 225 ^ [])), difference(223 ^ [], union(224 ^ [], 225 ^ []))], 224 ^ []), member(210 ^ [intersection(difference(223 ^ [], 224 ^ []), difference(223 ^ [], 225 ^ [])), difference(223 ^ [], union(224 ^ [], 225 ^ []))], difference(223 ^ [], 224 ^ []))],extension(114 ^ 6,bind([[_44301, _44303, _44305], [210 ^ [intersection(difference(223 ^ [], 224 ^ []), difference(223 ^ [], 225 ^ [])), difference(223 ^ [], union(224 ^ [], 225 ^ []))], 224 ^ [], 223 ^ []]]))).
% 10.42/10.69 ncf('1.1.2.2.1.1',plain,[-(member(210 ^ [intersection(difference(223 ^ [], 224 ^ []), difference(223 ^ [], 225 ^ [])), difference(223 ^ [], union(224 ^ [], 225 ^ []))], difference(223 ^ [], 224 ^ []))), member(210 ^ [intersection(difference(223 ^ [], 224 ^ []), difference(223 ^ [], 225 ^ [])), difference(223 ^ [], union(224 ^ [], 225 ^ []))], intersection(difference(223 ^ [], 224 ^ []), difference(223 ^ [], 225 ^ [])))],extension(96 ^ 7,bind([[_43690, _43692, _43694], [210 ^ [intersection(difference(223 ^ [], 224 ^ []), difference(223 ^ [], 225 ^ [])), difference(223 ^ [], union(224 ^ [], 225 ^ []))], difference(223 ^ [], 225 ^ []), difference(223 ^ [], 224 ^ [])]]))).
% 10.42/10.69 ncf('1.1.2.2.1.1.1',plain,[-(member(210 ^ [intersection(difference(223 ^ [], 224 ^ []), difference(223 ^ [], 225 ^ [])), difference(223 ^ [], union(224 ^ [], 225 ^ []))], intersection(difference(223 ^ [], 224 ^ []), difference(223 ^ [], 225 ^ []))))],extension(218 ^ 8)).
% 10.42/10.69 ncf('1.1.2.2.2',plain,[member(210 ^ [intersection(difference(223 ^ [], 224 ^ []), difference(223 ^ [], 225 ^ [])), difference(223 ^ [], union(224 ^ [], 225 ^ []))], 225 ^ []), member(210 ^ [intersection(difference(223 ^ [], 224 ^ []), difference(223 ^ [], 225 ^ [])), difference(223 ^ [], union(224 ^ [], 225 ^ []))], difference(223 ^ [], 225 ^ []))],extension(114 ^ 6,bind([[_44301, _44303, _44305], [210 ^ [intersection(difference(223 ^ [], 224 ^ []), difference(223 ^ [], 225 ^ [])), difference(223 ^ [], union(224 ^ [], 225 ^ []))], 225 ^ [], 223 ^ []]]))).
% 10.42/10.69 ncf('1.1.2.2.2.1',plain,[-(member(210 ^ [intersection(difference(223 ^ [], 224 ^ []), difference(223 ^ [], 225 ^ [])), difference(223 ^ [], union(224 ^ [], 225 ^ []))], difference(223 ^ [], 225 ^ []))), member(210 ^ [intersection(difference(223 ^ [], 224 ^ []), difference(223 ^ [], 225 ^ [])), difference(223 ^ [], union(224 ^ [], 225 ^ []))], intersection(difference(223 ^ [], 224 ^ []), difference(223 ^ [], 225 ^ [])))],extension(96 ^ 7,bind([[_43690, _43692, _43694], [210 ^ [intersection(difference(223 ^ [], 224 ^ []), difference(223 ^ [], 225 ^ [])), difference(223 ^ [], union(224 ^ [], 225 ^ []))], difference(223 ^ [], 225 ^ []), difference(223 ^ [], 224 ^ [])]]))).
% 10.42/10.69 ncf('1.1.2.2.2.1.1',plain,[-(member(210 ^ [intersection(difference(223 ^ [], 224 ^ []), difference(223 ^ [], 225 ^ [])), difference(223 ^ [], union(224 ^ [], 225 ^ []))], intersection(difference(223 ^ [], 224 ^ []), difference(223 ^ [], 225 ^ []))))],extension(218 ^ 8)).
% 10.42/10.69 %-----------------------------------------------------
% 10.42/10.69 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------