%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : SET200+3 : TPTP v8.1.2. Released v2.2.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n008.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:35 EDT 2023
% Result : Theorem 1.57s 2.41s
% Output : Proof 1.57s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : SET200+3 : TPTP v8.1.2. Released v2.2.0.
% 0.11/0.12 % Command : nanocop.sh %s %d
% 0.12/0.33 % Computer : n008.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:16:09 EDT 2023
% 0.18/0.33 % CPUTime :
% 1.57/2.41
% 1.57/2.41 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 1.57/2.41 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 1.57/2.41 %-----------------------------------------------------
% 1.57/2.41 ncf(matrix, plain, [(134 ^ _25450) ^ [] : [-(subset(129 ^ [], 130 ^ []))], (136 ^ _25450) ^ [] : [-(subset(131 ^ [], 132 ^ []))], (138 ^ _25450) ^ [] : [subset(union(129 ^ [], 131 ^ []), union(130 ^ [], 132 ^ []))], (48 ^ _25450) ^ [_27102, _27104, _27106, _27108] : [-(union(_27108, _27104) = union(_27106, _27102)), _27108 = _27106, _27104 = _27102], (2 ^ _25450) ^ [_25594] : [-(_25594 = _25594)], (4 ^ _25450) ^ [_25701, _25703] : [_25703 = _25701, -(_25701 = _25703)], (10 ^ _25450) ^ [_25905, _25907, _25909] : [-(_25909 = _25905), _25909 = _25907, _25907 = _25905], (20 ^ _25450) ^ [_26246, _26248, _26250, _26252] : [-(member(_26250, _26246)), member(_26252, _26248), _26252 = _26250, _26248 = _26246], (34 ^ _25450) ^ [_26670, _26672, _26674, _26676] : [-(subset(_26674, _26670)), subset(_26676, _26672), _26676 = _26674, _26672 = _26670], (68 ^ _25450) ^ [_27746, _27748, _27750] : [69 ^ _25450 : [(70 ^ _25450) ^ [] : [member(_27746, _27750)], (72 ^ _25450) ^ [] : [member(_27746, _27748)]], -(member(_27746, union(_27750, _27748)))], (58 ^ _25450) ^ [_27478, _27480, _27482] : [member(_27478, union(_27482, _27480)), -(member(_27478, _27482)), -(member(_27478, _27480))], (86 ^ _25450) ^ [_28389, _28391] : [88 ^ _25450 : [(89 ^ _25450) ^ [] : [-(member(87 ^ [_28389, _28391], _28391))], (91 ^ _25450) ^ [] : [member(87 ^ [_28389, _28391], _28389)]], -(subset(_28391, _28389))], (76 ^ _25450) ^ [_28075, _28077] : [subset(_28077, _28075), 79 ^ _25450 : [(80 ^ _25450) ^ [_28212] : [member(_28212, _28077), -(member(_28212, _28075))]]], (95 ^ _25450) ^ [_28731, _28733] : [-(union(_28733, _28731) = union(_28731, _28733))], (97 ^ _25450) ^ [_28817] : [-(subset(_28817, _28817))], (115 ^ _25450) ^ [_29450, _29452] : [-(_29452 = _29450), 119 ^ _25450 : [(120 ^ _25450) ^ [] : [-(member(116 ^ [_29450, _29452], _29452))], (122 ^ _25450) ^ [] : [member(116 ^ [_29450, _29452], _29450)]], 123 ^ _25450 : [(124 ^ _25450) ^ [] : [-(member(116 ^ [_29450, _29452], _29450))], (126 ^ _25450) ^ [] : [member(116 ^ [_29450, _29452], _29452)]]], (99 ^ _25450) ^ [_28933, _28935] : [_28935 = _28933, 102 ^ _25450 : [(103 ^ _25450) ^ [_29099] : [member(_29099, _28935), -(member(_29099, _28933))], (109 ^ _25450) ^ [_29271] : [member(_29271, _28933), -(member(_29271, _28935))]]]], input).
% 1.57/2.41 ncf('1',plain,[subset(union(129 ^ [], 131 ^ []), union(130 ^ [], 132 ^ []))],start(138 ^ 0)).
% 1.57/2.41 ncf('1.1',plain,[-(subset(union(129 ^ [], 131 ^ []), union(130 ^ [], 132 ^ []))), 89 : -(member(87 ^ [union(130 ^ [], 132 ^ []), union(129 ^ [], 131 ^ [])], union(129 ^ [], 131 ^ [])))],extension(86 ^ 1,bind([[_28389, _28391], [union(130 ^ [], 132 ^ []), union(129 ^ [], 131 ^ [])]]))).
% 1.57/2.41 ncf('1.1.1',plain,[member(87 ^ [union(130 ^ [], 132 ^ []), union(129 ^ [], 131 ^ [])], union(129 ^ [], 131 ^ [])), -(member(87 ^ [union(130 ^ [], 132 ^ []), union(129 ^ [], 131 ^ [])], 129 ^ [])), -(member(87 ^ [union(130 ^ [], 132 ^ []), union(129 ^ [], 131 ^ [])], 131 ^ []))],extension(58 ^ 4,bind([[_27478, _27480, _27482], [87 ^ [union(130 ^ [], 132 ^ []), union(129 ^ [], 131 ^ [])], 131 ^ [], 129 ^ []]]))).
% 1.57/2.41 ncf('1.1.1.1',plain,[member(87 ^ [union(130 ^ [], 132 ^ []), union(129 ^ [], 131 ^ [])], 129 ^ []), 80 : -(member(87 ^ [union(130 ^ [], 132 ^ []), union(129 ^ [], 131 ^ [])], union(130 ^ [], 132 ^ []))), 80 : subset(129 ^ [], union(130 ^ [], 132 ^ []))],extension(76 ^ 5,bind([[_28075, _28077, _28212], [union(130 ^ [], 132 ^ []), 129 ^ [], 87 ^ [union(130 ^ [], 132 ^ []), union(129 ^ [], 131 ^ [])]]]))).
% 1.57/2.41 ncf('1.1.1.1.1',plain,[member(87 ^ [union(130 ^ [], 132 ^ []), union(129 ^ [], 131 ^ [])], union(130 ^ [], 132 ^ [])), -(member(87 ^ [union(130 ^ [], 132 ^ []), union(129 ^ [], 131 ^ [])], union(130 ^ [], 132 ^ []))), 87 ^ [union(130 ^ [], 132 ^ []), union(129 ^ [], 131 ^ [])] = 87 ^ [union(130 ^ [], 132 ^ []), union(129 ^ [], 131 ^ [])], union(130 ^ [], 132 ^ []) = union(130 ^ [], 132 ^ [])],extension(20 ^ 8,bind([[_26246, _26248, _26250, _26252], [union(130 ^ [], 132 ^ []), union(130 ^ [], 132 ^ []), 87 ^ [union(130 ^ [], 132 ^ []), union(129 ^ [], 131 ^ [])], 87 ^ [union(130 ^ [], 132 ^ []), union(129 ^ [], 131 ^ [])]]]))).
% 1.57/2.41 ncf('1.1.1.1.1.1',plain,[member(87 ^ [union(130 ^ [], 132 ^ []), union(129 ^ [], 131 ^ [])], union(130 ^ [], 132 ^ [])), -(member(87 ^ [union(130 ^ [], 132 ^ []), union(129 ^ [], 131 ^ [])], union(130 ^ [], 132 ^ []))), 87 ^ [union(130 ^ [], 132 ^ []), union(129 ^ [], 131 ^ [])] = 87 ^ [union(130 ^ [], 132 ^ []), union(129 ^ [], 131 ^ [])], union(130 ^ [], 132 ^ []) = union(130 ^ [], 132 ^ [])],extension(20 ^ 9,bind([[_26246, _26248, _26250, _26252], [union(130 ^ [], 132 ^ []), union(130 ^ [], 132 ^ []), 87 ^ [union(130 ^ [], 132 ^ []), union(129 ^ [], 131 ^ [])], 87 ^ [union(130 ^ [], 132 ^ []), union(129 ^ [], 131 ^ [])]]]))).
% 1.57/2.41 ncf('1.1.1.1.1.1.1',plain,[member(87 ^ [union(130 ^ [], 132 ^ []), union(129 ^ [], 131 ^ [])], union(130 ^ [], 132 ^ [])), -(member(87 ^ [union(130 ^ [], 132 ^ []), union(129 ^ [], 131 ^ [])], union(130 ^ [], 132 ^ []))), 87 ^ [union(130 ^ [], 132 ^ []), union(129 ^ [], 131 ^ [])] = 87 ^ [union(130 ^ [], 132 ^ []), union(129 ^ [], 131 ^ [])], union(130 ^ [], 132 ^ []) = union(130 ^ [], 132 ^ [])],extension(20 ^ 10,bind([[_26246, _26248, _26250, _26252], [union(130 ^ [], 132 ^ []), union(130 ^ [], 132 ^ []), 87 ^ [union(130 ^ [], 132 ^ []), union(129 ^ [], 131 ^ [])], 87 ^ [union(130 ^ [], 132 ^ []), union(129 ^ [], 131 ^ [])]]]))).
% 1.57/2.41 ncf('1.1.1.1.1.1.1.1',plain,[member(87 ^ [union(130 ^ [], 132 ^ []), union(129 ^ [], 131 ^ [])], union(130 ^ [], 132 ^ []))],extension(91 ^ 11)).
% 1.57/2.41 ncf('1.1.1.1.1.1.1.2',plain,[-(87 ^ [union(130 ^ [], 132 ^ []), union(129 ^ [], 131 ^ [])] = 87 ^ [union(130 ^ [], 132 ^ []), union(129 ^ [], 131 ^ [])])],extension(2 ^ 11,bind([[_25594], [87 ^ [union(130 ^ [], 132 ^ []), union(129 ^ [], 131 ^ [])]]]))).
% 1.57/2.41 ncf('1.1.1.1.1.1.1.3',plain,[-(union(130 ^ [], 132 ^ []) = union(130 ^ [], 132 ^ []))],extension(2 ^ 11,bind([[_25594], [union(130 ^ [], 132 ^ [])]]))).
% 1.57/2.41 ncf('1.1.1.1.1.1.2',plain,[-(87 ^ [union(130 ^ [], 132 ^ []), union(129 ^ [], 131 ^ [])] = 87 ^ [union(130 ^ [], 132 ^ []), union(129 ^ [], 131 ^ [])])],extension(2 ^ 10,bind([[_25594], [87 ^ [union(130 ^ [], 132 ^ []), union(129 ^ [], 131 ^ [])]]]))).
% 1.57/2.41 ncf('1.1.1.1.1.1.3',plain,[-(union(130 ^ [], 132 ^ []) = union(130 ^ [], 132 ^ [])), 130 ^ [] = 130 ^ [], 132 ^ [] = 132 ^ []],extension(48 ^ 10,bind([[_27102, _27104, _27106, _27108], [132 ^ [], 132 ^ [], 130 ^ [], 130 ^ []]]))).
% 1.57/2.41 ncf('1.1.1.1.1.1.3.1',plain,[-(130 ^ [] = 130 ^ [])],extension(2 ^ 11,bind([[_25594], [130 ^ []]]))).
% 1.57/2.41 ncf('1.1.1.1.1.1.3.2',plain,[-(132 ^ [] = 132 ^ [])],extension(2 ^ 11,bind([[_25594], [132 ^ []]]))).
% 1.57/2.41 ncf('1.1.1.1.1.2',plain,[-(87 ^ [union(130 ^ [], 132 ^ []), union(129 ^ [], 131 ^ [])] = 87 ^ [union(130 ^ [], 132 ^ []), union(129 ^ [], 131 ^ [])])],extension(2 ^ 9,bind([[_25594], [87 ^ [union(130 ^ [], 132 ^ []), union(129 ^ [], 131 ^ [])]]]))).
% 1.57/2.41 ncf('1.1.1.1.1.3',plain,[-(union(130 ^ [], 132 ^ []) = union(130 ^ [], 132 ^ [])), 130 ^ [] = 130 ^ [], 132 ^ [] = 132 ^ []],extension(48 ^ 9,bind([[_27102, _27104, _27106, _27108], [132 ^ [], 132 ^ [], 130 ^ [], 130 ^ []]]))).
% 1.57/2.41 ncf('1.1.1.1.1.3.1',plain,[-(130 ^ [] = 130 ^ [])],extension(2 ^ 10,bind([[_25594], [130 ^ []]]))).
% 1.57/2.41 ncf('1.1.1.1.1.3.2',plain,[-(132 ^ [] = 132 ^ [])],extension(2 ^ 10,bind([[_25594], [132 ^ []]]))).
% 1.57/2.41 ncf('1.1.1.1.2',plain,[-(subset(129 ^ [], union(130 ^ [], 132 ^ []))), 91 : member(87 ^ [union(130 ^ [], 132 ^ []), 129 ^ []], union(130 ^ [], 132 ^ []))],extension(86 ^ 6,bind([[_28389, _28391], [union(130 ^ [], 132 ^ []), 129 ^ []]]))).
% 1.57/2.41 ncf('1.1.1.1.2.1',plain,[-(member(87 ^ [union(130 ^ [], 132 ^ []), 129 ^ []], union(130 ^ [], 132 ^ []))), 70 : member(87 ^ [union(130 ^ [], 132 ^ []), 129 ^ []], 130 ^ [])],extension(68 ^ 9,bind([[_27746, _27748, _27750], [87 ^ [union(130 ^ [], 132 ^ []), 129 ^ []], 132 ^ [], 130 ^ []]]))).
% 1.57/2.41 ncf('1.1.1.1.2.1.1',plain,[-(member(87 ^ [union(130 ^ [], 132 ^ []), 129 ^ []], 130 ^ [])), 80 : member(87 ^ [union(130 ^ [], 132 ^ []), 129 ^ []], 129 ^ []), 80 : subset(129 ^ [], 130 ^ [])],extension(76 ^ 12,bind([[_28075, _28077, _28212], [130 ^ [], 129 ^ [], 87 ^ [union(130 ^ [], 132 ^ []), 129 ^ []]]]))).
% 1.57/2.41 ncf('1.1.1.1.2.1.1.1',plain,[-(member(87 ^ [union(130 ^ [], 132 ^ []), 129 ^ []], 129 ^ []))],extension(89 ^ 15)).
% 1.57/2.41 ncf('1.1.1.1.2.1.1.2',plain,[-(subset(129 ^ [], 130 ^ []))],extension(134 ^ 13)).
% 1.57/2.41 ncf('1.1.1.2',plain,[member(87 ^ [union(130 ^ [], 132 ^ []), union(129 ^ [], 131 ^ [])], 131 ^ []), 80 : -(member(87 ^ [union(130 ^ [], 132 ^ []), union(129 ^ [], 131 ^ [])], union(130 ^ [], 132 ^ []))), 80 : subset(131 ^ [], union(130 ^ [], 132 ^ []))],extension(76 ^ 5,bind([[_28075, _28077, _28212], [union(130 ^ [], 132 ^ []), 131 ^ [], 87 ^ [union(130 ^ [], 132 ^ []), union(129 ^ [], 131 ^ [])]]]))).
% 1.57/2.41 ncf('1.1.1.2.1',plain,[member(87 ^ [union(130 ^ [], 132 ^ []), union(129 ^ [], 131 ^ [])], union(130 ^ [], 132 ^ [])), -(member(87 ^ [union(130 ^ [], 132 ^ []), union(129 ^ [], 131 ^ [])], union(130 ^ [], 132 ^ []))), 87 ^ [union(130 ^ [], 132 ^ []), union(129 ^ [], 131 ^ [])] = 87 ^ [union(130 ^ [], 132 ^ []), union(129 ^ [], 131 ^ [])], union(130 ^ [], 132 ^ []) = union(130 ^ [], 132 ^ [])],extension(20 ^ 8,bind([[_26246, _26248, _26250, _26252], [union(130 ^ [], 132 ^ []), union(130 ^ [], 132 ^ []), 87 ^ [union(130 ^ [], 132 ^ []), union(129 ^ [], 131 ^ [])], 87 ^ [union(130 ^ [], 132 ^ []), union(129 ^ [], 131 ^ [])]]]))).
% 1.57/2.41 ncf('1.1.1.2.1.1',plain,[member(87 ^ [union(130 ^ [], 132 ^ []), union(129 ^ [], 131 ^ [])], union(130 ^ [], 132 ^ [])), -(member(87 ^ [union(130 ^ [], 132 ^ []), union(129 ^ [], 131 ^ [])], union(130 ^ [], 132 ^ []))), 87 ^ [union(130 ^ [], 132 ^ []), union(129 ^ [], 131 ^ [])] = 87 ^ [union(130 ^ [], 132 ^ []), union(129 ^ [], 131 ^ [])], union(130 ^ [], 132 ^ []) = union(130 ^ [], 132 ^ [])],extension(20 ^ 9,bind([[_26246, _26248, _26250, _26252], [union(130 ^ [], 132 ^ []), union(130 ^ [], 132 ^ []), 87 ^ [union(130 ^ [], 132 ^ []), union(129 ^ [], 131 ^ [])], 87 ^ [union(130 ^ [], 132 ^ []), union(129 ^ [], 131 ^ [])]]]))).
% 1.57/2.41 ncf('1.1.1.2.1.1.1',plain,[member(87 ^ [union(130 ^ [], 132 ^ []), union(129 ^ [], 131 ^ [])], union(130 ^ [], 132 ^ [])), -(member(87 ^ [union(130 ^ [], 132 ^ []), union(129 ^ [], 131 ^ [])], union(130 ^ [], 132 ^ []))), 87 ^ [union(130 ^ [], 132 ^ []), union(129 ^ [], 131 ^ [])] = 87 ^ [union(130 ^ [], 132 ^ []), union(129 ^ [], 131 ^ [])], union(130 ^ [], 132 ^ []) = union(130 ^ [], 132 ^ [])],extension(20 ^ 10,bind([[_26246, _26248, _26250, _26252], [union(130 ^ [], 132 ^ []), union(130 ^ [], 132 ^ []), 87 ^ [union(130 ^ [], 132 ^ []), union(129 ^ [], 131 ^ [])], 87 ^ [union(130 ^ [], 132 ^ []), union(129 ^ [], 131 ^ [])]]]))).
% 1.57/2.41 ncf('1.1.1.2.1.1.1.1',plain,[member(87 ^ [union(130 ^ [], 132 ^ []), union(129 ^ [], 131 ^ [])], union(130 ^ [], 132 ^ []))],extension(91 ^ 11)).
% 1.57/2.41 ncf('1.1.1.2.1.1.1.2',plain,[-(87 ^ [union(130 ^ [], 132 ^ []), union(129 ^ [], 131 ^ [])] = 87 ^ [union(130 ^ [], 132 ^ []), union(129 ^ [], 131 ^ [])])],extension(2 ^ 11,bind([[_25594], [87 ^ [union(130 ^ [], 132 ^ []), union(129 ^ [], 131 ^ [])]]]))).
% 1.57/2.41 ncf('1.1.1.2.1.1.1.3',plain,[-(union(130 ^ [], 132 ^ []) = union(130 ^ [], 132 ^ []))],extension(2 ^ 11,bind([[_25594], [union(130 ^ [], 132 ^ [])]]))).
% 1.57/2.41 ncf('1.1.1.2.1.1.2',plain,[-(87 ^ [union(130 ^ [], 132 ^ []), union(129 ^ [], 131 ^ [])] = 87 ^ [union(130 ^ [], 132 ^ []), union(129 ^ [], 131 ^ [])])],extension(2 ^ 10,bind([[_25594], [87 ^ [union(130 ^ [], 132 ^ []), union(129 ^ [], 131 ^ [])]]]))).
% 1.57/2.41 ncf('1.1.1.2.1.1.3',plain,[-(union(130 ^ [], 132 ^ []) = union(130 ^ [], 132 ^ [])), 130 ^ [] = 130 ^ [], 132 ^ [] = 132 ^ []],extension(48 ^ 10,bind([[_27102, _27104, _27106, _27108], [132 ^ [], 132 ^ [], 130 ^ [], 130 ^ []]]))).
% 1.57/2.41 ncf('1.1.1.2.1.1.3.1',plain,[-(130 ^ [] = 130 ^ [])],extension(2 ^ 11,bind([[_25594], [130 ^ []]]))).
% 1.57/2.41 ncf('1.1.1.2.1.1.3.2',plain,[-(132 ^ [] = 132 ^ [])],extension(2 ^ 11,bind([[_25594], [132 ^ []]]))).
% 1.57/2.41 ncf('1.1.1.2.1.2',plain,[-(87 ^ [union(130 ^ [], 132 ^ []), union(129 ^ [], 131 ^ [])] = 87 ^ [union(130 ^ [], 132 ^ []), union(129 ^ [], 131 ^ [])])],extension(2 ^ 9,bind([[_25594], [87 ^ [union(130 ^ [], 132 ^ []), union(129 ^ [], 131 ^ [])]]]))).
% 1.57/2.41 ncf('1.1.1.2.1.3',plain,[-(union(130 ^ [], 132 ^ []) = union(130 ^ [], 132 ^ [])), 130 ^ [] = 130 ^ [], 132 ^ [] = 132 ^ []],extension(48 ^ 9,bind([[_27102, _27104, _27106, _27108], [132 ^ [], 132 ^ [], 130 ^ [], 130 ^ []]]))).
% 1.57/2.41 ncf('1.1.1.2.1.3.1',plain,[-(130 ^ [] = 130 ^ [])],extension(2 ^ 10,bind([[_25594], [130 ^ []]]))).
% 1.57/2.41 ncf('1.1.1.2.1.3.2',plain,[-(132 ^ [] = 132 ^ [])],extension(2 ^ 10,bind([[_25594], [132 ^ []]]))).
% 1.57/2.41 ncf('1.1.1.2.2',plain,[-(subset(131 ^ [], union(130 ^ [], 132 ^ []))), 91 : member(87 ^ [union(130 ^ [], 132 ^ []), 131 ^ []], union(130 ^ [], 132 ^ []))],extension(86 ^ 6,bind([[_28389, _28391], [union(130 ^ [], 132 ^ []), 131 ^ []]]))).
% 1.57/2.41 ncf('1.1.1.2.2.1',plain,[-(member(87 ^ [union(130 ^ [], 132 ^ []), 131 ^ []], union(130 ^ [], 132 ^ []))), 72 : member(87 ^ [union(130 ^ [], 132 ^ []), 131 ^ []], 132 ^ [])],extension(68 ^ 9,bind([[_27746, _27748, _27750], [87 ^ [union(130 ^ [], 132 ^ []), 131 ^ []], 132 ^ [], 130 ^ []]]))).
% 1.57/2.41 ncf('1.1.1.2.2.1.1',plain,[-(member(87 ^ [union(130 ^ [], 132 ^ []), 131 ^ []], 132 ^ [])), 80 : member(87 ^ [union(130 ^ [], 132 ^ []), 131 ^ []], 131 ^ []), 80 : subset(131 ^ [], 132 ^ [])],extension(76 ^ 12,bind([[_28075, _28077, _28212], [132 ^ [], 131 ^ [], 87 ^ [union(130 ^ [], 132 ^ []), 131 ^ []]]]))).
% 1.57/2.41 ncf('1.1.1.2.2.1.1.1',plain,[-(member(87 ^ [union(130 ^ [], 132 ^ []), 131 ^ []], 131 ^ []))],extension(89 ^ 15)).
% 1.57/2.41 ncf('1.1.1.2.2.1.1.2',plain,[-(subset(131 ^ [], 132 ^ []))],extension(136 ^ 13)).
% 1.57/2.41 %-----------------------------------------------------
% 1.57/2.41 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------