%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : SYO605+1 : TPTP v8.1.2. Released v7.0.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n011.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 12:38:16 EDT 2023
% Result : Theorem 2.16s 2.41s
% Output : Proof 2.16s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : SYO605+1 : TPTP v8.1.2. Released v7.0.0.
% 0.07/0.13 % Command : nanocop.sh %s %d
% 0.12/0.34 % Computer : n011.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 300
% 0.12/0.34 % DateTime : Thu May 18 18:17:03 EDT 2023
% 0.12/0.34 % CPUTime :
% 2.16/2.41
% 2.16/2.41 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 2.16/2.41 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 2.16/2.41 %-----------------------------------------------------
% 2.16/2.41 ncf(matrix, plain, [(2 ^ _85462) ^ [_85604, _85606] : [g_true_only(_85606, _85604), 5 ^ _85462 : [(6 ^ _85462) ^ [] : [-(g_true(_85606, _85604))], (8 ^ _85462) ^ [] : [g_false(_85606, _85604)]]], (10 ^ _85462) ^ [_85842, _85844] : [-(g_true_only(_85844, _85842)), g_true(_85844, _85842), -(g_false(_85844, _85842))], (20 ^ _85462) ^ [_86175, _86177] : [g_both(_86177, _86175), 23 ^ _85462 : [(24 ^ _85462) ^ [] : [-(g_true(_86177, _86175))], (26 ^ _85462) ^ [] : [-(g_false(_86177, _86175))]]], (28 ^ _85462) ^ [_86412, _86414] : [-(g_both(_86414, _86412)), g_true(_86414, _86412), g_false(_86414, _86412)], (56 ^ _85462) ^ [_87264, _87266] : [-(g_true_only(_87266, _87264)), -(g_both(_87266, _87264)), -(g_false_only(_87266, _87264))], (38 ^ _85462) ^ [_86742, _86744] : [g_false_only(_86744, _86742), 41 ^ _85462 : [(42 ^ _85462) ^ [] : [-(g_false(_86744, _86742))], (44 ^ _85462) ^ [] : [g_true(_86744, _86742)]]], (46 ^ _85462) ^ [_86980, _86982] : [-(g_false_only(_86982, _86980)), g_false(_86982, _86980), -(g_true(_86982, _86980))], (67 ^ _85462) ^ [_87671] : [g_true_only(_87671, 65 ^ []), 70 ^ _85462 : [(71 ^ _85462) ^ [] : [g_both(_87671, _87671)], (73 ^ _85462) ^ [] : [g_false_only(_87671, _87671)]]], (75 ^ _85462) ^ [_87918] : [g_both(_87918, 65 ^ []), 78 ^ _85462 : [(79 ^ _85462) ^ [] : [g_true_only(_87918, _87918)], (81 ^ _85462) ^ [] : [g_false_only(_87918, _87918)]]], (83 ^ _85462) ^ [_88145] : [g_false_only(_88145, 65 ^ []), 86 ^ _85462 : [(87 ^ _85462) ^ [] : [g_true_only(_88145, _88145)], (89 ^ _85462) ^ [] : [g_both(_88145, _88145)]]], (92 ^ _85462) ^ [_88536, _88538] : [g_true_only(_88536, 90 ^ [_88538]), 95 ^ _85462 : [(96 ^ _85462) ^ [] : [g_both(_88536, _88538)], (98 ^ _85462) ^ [] : [g_true_only(_88536, _88538)]]], (100 ^ _85462) ^ [_88801, _88803] : [g_both(_88801, 90 ^ [_88803]), 103 ^ _85462 : [(104 ^ _85462) ^ [] : [g_false_only(_88801, _88803)], (106 ^ _85462) ^ [] : [g_true_only(_88801, _88803)]]], (108 ^ _85462) ^ [_89046, _89048] : [g_false_only(_89046, 90 ^ [_89048]), 111 ^ _85462 : [(112 ^ _85462) ^ [] : [g_false_only(_89046, _89048)], (114 ^ _85462) ^ [] : [g_both(_89046, _89048)]]], (116 ^ _85462) ^ [] : [117 ^ _85462 : [(118 ^ _85462) ^ [_89339] : [119 ^ _85462 : [(120 ^ _85462) ^ [_89484] : [g_both(_89484, _89339), g_both(_89484, _89484)]], 128 ^ _85462 : [(129 ^ _85462) ^ [] : [-(g_true_only(125 ^ [_89339], _89339))], (131 ^ _85462) ^ [] : [-(g_both(125 ^ [_89339], 125 ^ [_89339])), -(g_false_only(125 ^ [_89339], 125 ^ [_89339]))]], 138 ^ _85462 : [(139 ^ _85462) ^ [] : [-(g_both(125 ^ [_89339], _89339))], (141 ^ _85462) ^ [] : [-(g_true_only(125 ^ [_89339], 125 ^ [_89339])), -(g_false_only(125 ^ [_89339], 125 ^ [_89339]))]], 146 ^ _85462 : [(147 ^ _85462) ^ [] : [-(g_false_only(125 ^ [_89339], _89339))], (149 ^ _85462) ^ [] : [-(g_true_only(125 ^ [_89339], 125 ^ [_89339])), -(g_both(125 ^ [_89339], 125 ^ [_89339]))]]]], 157 ^ _85462 : [(158 ^ _85462) ^ [_90565] : [159 ^ _85462 : [(160 ^ _85462) ^ [] : [-(g_true_only(_90565, 156 ^ []))], (162 ^ _85462) ^ [] : [-(g_true_only(_90565, _90565))]], 163 ^ _85462 : [(164 ^ _85462) ^ [] : [-(g_false_only(_90565, 156 ^ []))], (166 ^ _85462) ^ [] : [-(g_false_only(_90565, _90565))]]]], 221 ^ _85462 : [(222 ^ _85462) ^ [_92867] : [223 ^ _85462 : [(224 ^ _85462) ^ [] : [-(g_true_only(220 ^ [_92867], _92867))], (226 ^ _85462) ^ [] : [-(g_both(220 ^ [_92867], 219 ^ [])), -(g_true_only(220 ^ [_92867], 219 ^ []))]], 233 ^ _85462 : [(234 ^ _85462) ^ [] : [-(g_both(220 ^ [_92867], _92867))], (236 ^ _85462) ^ [] : [-(g_false_only(220 ^ [_92867], 219 ^ [])), -(g_true_only(220 ^ [_92867], 219 ^ []))]], 241 ^ _85462 : [(242 ^ _85462) ^ [] : [-(g_false_only(220 ^ [_92867], _92867))], (244 ^ _85462) ^ [] : [-(g_false_only(220 ^ [_92867], 219 ^ [])), -(g_both(220 ^ [_92867], 219 ^ []))]]]], 169 ^ _85462 : [(170 ^ _85462) ^ [_90912] : [209 ^ _85462 : [(210 ^ _85462) ^ [_92330] : [211 ^ _85462 : [(212 ^ _85462) ^ [] : [-(g_true_only(_92330, 208 ^ [_90912]))], (214 ^ _85462) ^ [] : [-(g_false_only(_92330, _90912))]], 215 ^ _85462 : [(216 ^ _85462) ^ [] : [-(g_false_only(_92330, 208 ^ [_90912]))], (218 ^ _85462) ^ [] : [-(g_true_only(_92330, _90912))]]]], 171 ^ _85462 : [(172 ^ _85462) ^ [_91098] : [173 ^ _85462 : [(174 ^ _85462) ^ [_91247] : [g_both(_91247, _91098), g_both(_91247, _90912)]], 182 ^ _85462 : [(183 ^ _85462) ^ [] : [-(g_true_only(179 ^ [_90912, _91098], _91098))], (185 ^ _85462) ^ [] : [-(g_both(179 ^ [_90912, _91098], _90912)), -(g_true_only(179 ^ [_90912, _91098], _90912))]], 192 ^ _85462 : [(193 ^ _85462) ^ [] : [-(g_both(179 ^ [_90912, _91098], _91098))], (195 ^ _85462) ^ [] : [-(g_false_only(179 ^ [_90912, _91098], _90912)), -(g_true_only(179 ^ [_90912, _91098], _90912))]], 200 ^ _85462 : [(201 ^ _85462) ^ [] : [-(g_false_only(179 ^ [_90912, _91098], _91098))], (203 ^ _85462) ^ [] : [-(g_false_only(179 ^ [_90912, _91098], _90912)), -(g_both(179 ^ [_90912, _91098], _90912))]]]]]]]], input).
% 2.16/2.41 ncf('1',plain,[g_false_only(90 ^ [65 ^ []], 65 ^ []), 44 : g_true(90 ^ [65 ^ []], 65 ^ [])],start(38 ^ 0,bind([[_86742, _86744], [65 ^ [], 90 ^ [65 ^ []]]]))).
% 2.16/2.41 ncf('1.1',plain,[-(g_false_only(90 ^ [65 ^ []], 65 ^ [])), -(g_true_only(90 ^ [65 ^ []], 65 ^ [])), -(g_both(90 ^ [65 ^ []], 65 ^ []))],extension(56 ^ 1,bind([[_87264, _87266], [65 ^ [], 90 ^ [65 ^ []]]]))).
% 2.16/2.41 ncf('1.1.1',plain,[g_true_only(90 ^ [65 ^ []], 65 ^ []), 71 : g_both(90 ^ [65 ^ []], 90 ^ [65 ^ []])],extension(67 ^ 2,bind([[_87671], [90 ^ [65 ^ []]]]))).
% 2.16/2.41 ncf('1.1.1.1',plain,[-(g_both(90 ^ [65 ^ []], 90 ^ [65 ^ []])), -(g_true_only(90 ^ [65 ^ []], 90 ^ [65 ^ []])), -(g_false_only(90 ^ [65 ^ []], 90 ^ [65 ^ []]))],extension(56 ^ 5,bind([[_87264, _87266], [90 ^ [65 ^ []], 90 ^ [65 ^ []]]]))).
% 2.16/2.41 ncf('1.1.1.1.1',plain,[g_true_only(90 ^ [65 ^ []], 90 ^ [65 ^ []]), 98 : g_true_only(90 ^ [65 ^ []], 65 ^ [])],extension(92 ^ 6,bind([[_88536, _88538], [90 ^ [65 ^ []], 65 ^ []]]))).
% 2.16/2.41 ncf('1.1.1.1.1.1',plain,[-(g_true_only(90 ^ [65 ^ []], 65 ^ []))],reduction('1.1')).
% 2.16/2.41 ncf('1.1.1.1.2',plain,[g_false_only(90 ^ [65 ^ []], 90 ^ [65 ^ []])],extension(73 ^ 6)).
% 2.16/2.41 ncf('1.1.2',plain,[g_both(90 ^ [65 ^ []], 65 ^ []), 79 : g_true_only(90 ^ [65 ^ []], 90 ^ [65 ^ []])],extension(75 ^ 2,bind([[_87918], [90 ^ [65 ^ []]]]))).
% 2.16/2.41 ncf('1.1.2.1',plain,[-(g_true_only(90 ^ [65 ^ []], 90 ^ [65 ^ []])), 214 : -(g_false_only(90 ^ [65 ^ []], 90 ^ [65 ^ []])), 174 : g_both(90 ^ [65 ^ []], 65 ^ []), 174 : g_both(90 ^ [65 ^ []], 90 ^ [65 ^ []]), 185 : -(g_both(179 ^ [90 ^ [65 ^ []], 65 ^ []], 90 ^ [65 ^ []])), 185 : -(g_true_only(179 ^ [90 ^ [65 ^ []], 65 ^ []], 90 ^ [65 ^ []])), 195 : -(g_false_only(179 ^ [90 ^ [65 ^ []], 65 ^ []], 90 ^ [65 ^ []])), 195 : -(g_true_only(179 ^ [90 ^ [65 ^ []], 65 ^ []], 90 ^ [65 ^ []])), 203 : -(g_false_only(179 ^ [90 ^ [65 ^ []], 65 ^ []], 90 ^ [65 ^ []])), 203 : -(g_both(179 ^ [90 ^ [65 ^ []], 65 ^ []], 90 ^ [65 ^ []])), 120 : g_both(90 ^ [65 ^ []], 65 ^ []), 120 : g_both(90 ^ [65 ^ []], 90 ^ [65 ^ []]), 131 : -(g_both(125 ^ [65 ^ []], 125 ^ [65 ^ []])), 131 : -(g_false_only(125 ^ [65 ^ []], 125 ^ [65 ^ []])), 141 : -(g_true_only(125 ^ [65 ^ []], 125 ^ [65 ^ []])), 141 : -(g_false_only(125 ^ [65 ^ []], 125 ^ [65 ^ []])), 149 : -(g_true_only(125 ^ [65 ^ []], 125 ^ [65 ^ []])), 149 : -(g_both(125 ^ [65 ^ []], 125 ^ [65 ^ []])), 160 : -(g_true_only(90 ^ [156 ^ []], 156 ^ [])), 164 : -(g_false_only(90 ^ [156 ^ []], 156 ^ [])), 226 : -(g_both(220 ^ [90 ^ [219 ^ []]], 219 ^ [])), 226 : -(g_true_only(220 ^ [90 ^ [219 ^ []]], 219 ^ [])), 236 : -(g_false_only(220 ^ [90 ^ [219 ^ []]], 219 ^ [])), 236 : -(g_true_only(220 ^ [90 ^ [219 ^ []]], 219 ^ [])), 244 : -(g_false_only(220 ^ [90 ^ [219 ^ []]], 219 ^ [])), 244 : -(g_both(220 ^ [90 ^ [219 ^ []]], 219 ^ []))],extension(116 ^ 5,bind([[_90912, _92330, _91098, _91247, _89339, _89484, _90565, _92867], [90 ^ [65 ^ []], 90 ^ [65 ^ []], 65 ^ [], 90 ^ [65 ^ []], 65 ^ [], 90 ^ [65 ^ []], 90 ^ [156 ^ []], 90 ^ [219 ^ []]]]))).
% 2.16/2.41 ncf('1.1.2.1.1',plain,[g_false_only(90 ^ [65 ^ []], 90 ^ [65 ^ []])],extension(81 ^ 12)).
% 2.16/2.41 ncf('1.1.2.1.2',plain,[-(g_both(90 ^ [65 ^ []], 65 ^ []))],reduction('1.1')).
% 2.16/2.41 ncf('1.1.2.1.3',plain,[-(g_both(90 ^ [65 ^ []], 90 ^ [65 ^ []])), -(g_true_only(90 ^ [65 ^ []], 90 ^ [65 ^ []])), -(g_false_only(90 ^ [65 ^ []], 90 ^ [65 ^ []]))],extension(56 ^ 12,bind([[_87264, _87266], [90 ^ [65 ^ []], 90 ^ [65 ^ []]]]))).
% 2.16/2.41 ncf('1.1.2.1.3.1',plain,[g_true_only(90 ^ [65 ^ []], 90 ^ [65 ^ []])],reduction('1.1.2')).
% 2.16/2.41 ncf('1.1.2.1.3.2',plain,[g_false_only(90 ^ [65 ^ []], 90 ^ [65 ^ []])],extension(81 ^ 13)).
% 2.16/2.41 ncf('1.1.2.1.4',plain,[g_both(179 ^ [90 ^ [65 ^ []], 65 ^ []], 90 ^ [65 ^ []]), 106 : g_true_only(179 ^ [90 ^ [65 ^ []], 65 ^ []], 65 ^ [])],extension(100 ^ 12,bind([[_88801, _88803], [179 ^ [90 ^ [65 ^ []], 65 ^ []], 65 ^ []]]))).
% 2.16/2.41 ncf('1.1.2.1.4.1',plain,[-(g_true_only(179 ^ [90 ^ [65 ^ []], 65 ^ []], 65 ^ []))],extension(183 ^ 15)).
% 2.16/2.41 ncf('1.1.2.1.5',plain,[g_true_only(179 ^ [90 ^ [65 ^ []], 65 ^ []], 90 ^ [65 ^ []]), 98 : g_true_only(179 ^ [90 ^ [65 ^ []], 65 ^ []], 65 ^ [])],extension(92 ^ 12,bind([[_88536, _88538], [179 ^ [90 ^ [65 ^ []], 65 ^ []], 65 ^ []]]))).
% 2.16/2.41 ncf('1.1.2.1.5.1',plain,[-(g_true_only(179 ^ [90 ^ [65 ^ []], 65 ^ []], 65 ^ []))],extension(183 ^ 15)).
% 2.16/2.41 ncf('1.1.2.1.6',plain,[g_false_only(179 ^ [90 ^ [65 ^ []], 65 ^ []], 90 ^ [65 ^ []]), 114 : g_both(179 ^ [90 ^ [65 ^ []], 65 ^ []], 65 ^ [])],extension(108 ^ 12,bind([[_89046, _89048], [179 ^ [90 ^ [65 ^ []], 65 ^ []], 65 ^ []]]))).
% 2.16/2.41 ncf('1.1.2.1.6.1',plain,[-(g_both(179 ^ [90 ^ [65 ^ []], 65 ^ []], 65 ^ []))],extension(193 ^ 15)).
% 2.16/2.41 ncf('1.1.2.1.7',plain,[g_true_only(179 ^ [90 ^ [65 ^ []], 65 ^ []], 90 ^ [65 ^ []]), 96 : g_both(179 ^ [90 ^ [65 ^ []], 65 ^ []], 65 ^ [])],extension(92 ^ 12,bind([[_88536, _88538], [179 ^ [90 ^ [65 ^ []], 65 ^ []], 65 ^ []]]))).
% 2.16/2.41 ncf('1.1.2.1.7.1',plain,[-(g_both(179 ^ [90 ^ [65 ^ []], 65 ^ []], 65 ^ []))],extension(193 ^ 15)).
% 2.16/2.41 ncf('1.1.2.1.8',plain,[g_false_only(179 ^ [90 ^ [65 ^ []], 65 ^ []], 90 ^ [65 ^ []]), 112 : g_false_only(179 ^ [90 ^ [65 ^ []], 65 ^ []], 65 ^ [])],extension(108 ^ 12,bind([[_89046, _89048], [179 ^ [90 ^ [65 ^ []], 65 ^ []], 65 ^ []]]))).
% 2.16/2.41 ncf('1.1.2.1.8.1',plain,[-(g_false_only(179 ^ [90 ^ [65 ^ []], 65 ^ []], 65 ^ []))],extension(201 ^ 15)).
% 2.16/2.41 ncf('1.1.2.1.9',plain,[g_both(179 ^ [90 ^ [65 ^ []], 65 ^ []], 90 ^ [65 ^ []]), 104 : g_false_only(179 ^ [90 ^ [65 ^ []], 65 ^ []], 65 ^ [])],extension(100 ^ 12,bind([[_88801, _88803], [179 ^ [90 ^ [65 ^ []], 65 ^ []], 65 ^ []]]))).
% 2.16/2.41 ncf('1.1.2.1.9.1',plain,[-(g_false_only(179 ^ [90 ^ [65 ^ []], 65 ^ []], 65 ^ []))],extension(201 ^ 15)).
% 2.16/2.41 ncf('1.1.2.1.10',plain,[-(g_both(90 ^ [65 ^ []], 65 ^ []))],reduction('1.1')).
% 2.16/2.41 ncf('1.1.2.1.11',plain,[-(g_both(90 ^ [65 ^ []], 90 ^ [65 ^ []])), -(g_true_only(90 ^ [65 ^ []], 90 ^ [65 ^ []])), -(g_false_only(90 ^ [65 ^ []], 90 ^ [65 ^ []]))],extension(56 ^ 10,bind([[_87264, _87266], [90 ^ [65 ^ []], 90 ^ [65 ^ []]]]))).
% 2.16/2.41 ncf('1.1.2.1.11.1',plain,[g_true_only(90 ^ [65 ^ []], 90 ^ [65 ^ []])],reduction('1.1.2')).
% 2.16/2.41 ncf('1.1.2.1.11.2',plain,[g_false_only(90 ^ [65 ^ []], 90 ^ [65 ^ []])],extension(81 ^ 11)).
% 2.16/2.41 ncf('1.1.2.1.12',plain,[g_both(125 ^ [65 ^ []], 125 ^ [65 ^ []]), g_true_only(125 ^ [65 ^ []], 65 ^ [])],extension(67 ^ 10,bind([[_87671], [125 ^ [65 ^ []]]]))).
% 2.16/2.41 ncf('1.1.2.1.12.1',plain,[-(g_true_only(125 ^ [65 ^ []], 65 ^ []))],extension(129 ^ 11)).
% 2.16/2.41 ncf('1.1.2.1.13',plain,[g_false_only(125 ^ [65 ^ []], 125 ^ [65 ^ []]), g_true_only(125 ^ [65 ^ []], 65 ^ [])],extension(67 ^ 10,bind([[_87671], [125 ^ [65 ^ []]]]))).
% 2.16/2.41 ncf('1.1.2.1.13.1',plain,[-(g_true_only(125 ^ [65 ^ []], 65 ^ []))],extension(129 ^ 11)).
% 2.16/2.41 ncf('1.1.2.1.14',plain,[g_true_only(125 ^ [65 ^ []], 125 ^ [65 ^ []]), g_both(125 ^ [65 ^ []], 65 ^ [])],extension(75 ^ 10,bind([[_87918], [125 ^ [65 ^ []]]]))).
% 2.16/2.41 ncf('1.1.2.1.14.1',plain,[-(g_both(125 ^ [65 ^ []], 65 ^ []))],extension(139 ^ 11)).
% 2.16/2.41 ncf('1.1.2.1.15',plain,[g_false_only(125 ^ [65 ^ []], 125 ^ [65 ^ []]), g_both(125 ^ [65 ^ []], 65 ^ [])],extension(75 ^ 10,bind([[_87918], [125 ^ [65 ^ []]]]))).
% 2.16/2.41 ncf('1.1.2.1.15.1',plain,[-(g_both(125 ^ [65 ^ []], 65 ^ []))],extension(139 ^ 11)).
% 2.16/2.41 ncf('1.1.2.1.16',plain,[g_true_only(125 ^ [65 ^ []], 125 ^ [65 ^ []]), g_false_only(125 ^ [65 ^ []], 65 ^ [])],extension(83 ^ 10,bind([[_88145], [125 ^ [65 ^ []]]]))).
% 2.16/2.41 ncf('1.1.2.1.16.1',plain,[-(g_false_only(125 ^ [65 ^ []], 65 ^ []))],extension(147 ^ 11)).
% 2.16/2.41 ncf('1.1.2.1.17',plain,[g_both(125 ^ [65 ^ []], 125 ^ [65 ^ []]), g_false_only(125 ^ [65 ^ []], 65 ^ [])],extension(83 ^ 10,bind([[_88145], [125 ^ [65 ^ []]]]))).
% 2.16/2.41 ncf('1.1.2.1.17.1',plain,[-(g_false_only(125 ^ [65 ^ []], 65 ^ []))],extension(147 ^ 11)).
% 2.16/2.41 ncf('1.1.2.1.18',plain,[g_true_only(90 ^ [156 ^ []], 156 ^ []), g_true_only(90 ^ [156 ^ []], 90 ^ [156 ^ []])],extension(92 ^ 10,bind([[_88536, _88538], [90 ^ [156 ^ []], 156 ^ []]]))).
% 2.16/2.41 ncf('1.1.2.1.18.1',plain,[-(g_true_only(90 ^ [156 ^ []], 90 ^ [156 ^ []]))],extension(162 ^ 11)).
% 2.16/2.41 ncf('1.1.2.1.19',plain,[g_false_only(90 ^ [156 ^ []], 156 ^ []), g_false_only(90 ^ [156 ^ []], 90 ^ [156 ^ []])],extension(108 ^ 10,bind([[_89046, _89048], [90 ^ [156 ^ []], 156 ^ []]]))).
% 2.16/2.41 ncf('1.1.2.1.19.1',plain,[-(g_false_only(90 ^ [156 ^ []], 90 ^ [156 ^ []]))],extension(166 ^ 11)).
% 2.16/2.41 ncf('1.1.2.1.20',plain,[g_both(220 ^ [90 ^ [219 ^ []]], 219 ^ []), g_true_only(220 ^ [90 ^ [219 ^ []]], 90 ^ [219 ^ []])],extension(92 ^ 10,bind([[_88536, _88538], [220 ^ [90 ^ [219 ^ []]], 219 ^ []]]))).
% 2.16/2.41 ncf('1.1.2.1.20.1',plain,[-(g_true_only(220 ^ [90 ^ [219 ^ []]], 90 ^ [219 ^ []]))],extension(224 ^ 11)).
% 2.16/2.41 ncf('1.1.2.1.21',plain,[g_true_only(220 ^ [90 ^ [219 ^ []]], 219 ^ []), g_true_only(220 ^ [90 ^ [219 ^ []]], 90 ^ [219 ^ []])],extension(92 ^ 10,bind([[_88536, _88538], [220 ^ [90 ^ [219 ^ []]], 219 ^ []]]))).
% 2.16/2.41 ncf('1.1.2.1.21.1',plain,[-(g_true_only(220 ^ [90 ^ [219 ^ []]], 90 ^ [219 ^ []]))],extension(224 ^ 11)).
% 2.16/2.41 ncf('1.1.2.1.22',plain,[g_false_only(220 ^ [90 ^ [219 ^ []]], 219 ^ []), g_both(220 ^ [90 ^ [219 ^ []]], 90 ^ [219 ^ []])],extension(100 ^ 10,bind([[_88801, _88803], [220 ^ [90 ^ [219 ^ []]], 219 ^ []]]))).
% 2.16/2.41 ncf('1.1.2.1.22.1',plain,[-(g_both(220 ^ [90 ^ [219 ^ []]], 90 ^ [219 ^ []]))],extension(234 ^ 11)).
% 2.16/2.41 ncf('1.1.2.1.23',plain,[g_true_only(220 ^ [90 ^ [219 ^ []]], 219 ^ []), g_both(220 ^ [90 ^ [219 ^ []]], 90 ^ [219 ^ []])],extension(100 ^ 10,bind([[_88801, _88803], [220 ^ [90 ^ [219 ^ []]], 219 ^ []]]))).
% 2.16/2.41 ncf('1.1.2.1.23.1',plain,[-(g_both(220 ^ [90 ^ [219 ^ []]], 90 ^ [219 ^ []]))],extension(234 ^ 11)).
% 2.16/2.41 ncf('1.1.2.1.24',plain,[g_false_only(220 ^ [90 ^ [219 ^ []]], 219 ^ []), g_false_only(220 ^ [90 ^ [219 ^ []]], 90 ^ [219 ^ []])],extension(108 ^ 10,bind([[_89046, _89048], [220 ^ [90 ^ [219 ^ []]], 219 ^ []]]))).
% 2.16/2.41 ncf('1.1.2.1.24.1',plain,[-(g_false_only(220 ^ [90 ^ [219 ^ []]], 90 ^ [219 ^ []]))],extension(242 ^ 11)).
% 2.16/2.41 ncf('1.1.2.1.25',plain,[g_both(220 ^ [90 ^ [219 ^ []]], 219 ^ []), g_false_only(220 ^ [90 ^ [219 ^ []]], 90 ^ [219 ^ []])],extension(108 ^ 10,bind([[_89046, _89048], [220 ^ [90 ^ [219 ^ []]], 219 ^ []]]))).
% 2.16/2.41 ncf('1.1.2.1.25.1',plain,[-(g_false_only(220 ^ [90 ^ [219 ^ []]], 90 ^ [219 ^ []]))],extension(242 ^ 11)).
% 2.16/2.41 ncf('1.2',plain,[-(g_true(90 ^ [65 ^ []], 65 ^ [])), g_true_only(90 ^ [65 ^ []], 65 ^ [])],extension(2 ^ 3,bind([[_85604, _85606], [65 ^ [], 90 ^ [65 ^ []]]]))).
% 2.16/2.41 ncf('1.2.1',plain,[-(g_true_only(90 ^ [65 ^ []], 65 ^ [])), -(g_both(90 ^ [65 ^ []], 65 ^ [])), -(g_false_only(90 ^ [65 ^ []], 65 ^ []))],extension(56 ^ 4,bind([[_87264, _87266], [65 ^ [], 90 ^ [65 ^ []]]]))).
% 2.16/2.41 ncf('1.2.1.1',plain,[g_both(90 ^ [65 ^ []], 65 ^ []), 24 : -(g_true(90 ^ [65 ^ []], 65 ^ []))],extension(20 ^ 5,bind([[_86175, _86177], [65 ^ [], 90 ^ [65 ^ []]]]))).
% 2.16/2.41 ncf('1.2.1.1.1',plain,[g_true(90 ^ [65 ^ []], 65 ^ [])],reduction('1')).
% 2.16/2.41 ncf('1.2.1.2',plain,[g_false_only(90 ^ [65 ^ []], 65 ^ []), 87 : g_true_only(90 ^ [65 ^ []], 90 ^ [65 ^ []])],extension(83 ^ 5,bind([[_88145], [90 ^ [65 ^ []]]]))).
% 2.16/2.41 ncf('1.2.1.2.1',plain,[-(g_true_only(90 ^ [65 ^ []], 90 ^ [65 ^ []])), -(g_both(90 ^ [65 ^ []], 90 ^ [65 ^ []])), -(g_false_only(90 ^ [65 ^ []], 90 ^ [65 ^ []]))],extension(56 ^ 8,bind([[_87264, _87266], [90 ^ [65 ^ []], 90 ^ [65 ^ []]]]))).
% 2.16/2.41 ncf('1.2.1.2.1.1',plain,[g_both(90 ^ [65 ^ []], 90 ^ [65 ^ []])],extension(89 ^ 9)).
% 2.16/2.41 ncf('1.2.1.2.1.2',plain,[g_false_only(90 ^ [65 ^ []], 90 ^ [65 ^ []]), 112 : g_false_only(90 ^ [65 ^ []], 65 ^ [])],extension(108 ^ 9,bind([[_89046, _89048], [90 ^ [65 ^ []], 65 ^ []]]))).
% 2.16/2.41 ncf('1.2.1.2.1.2.1',plain,[-(g_false_only(90 ^ [65 ^ []], 65 ^ []))],lemmata('x')).
% 2.16/2.41 %-----------------------------------------------------
% 2.16/2.41 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------