%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : KRS078+1 : TPTP v8.1.2. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n016.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:26:13 EDT 2023
% Result : Unsatisfiable 0.35s 1.37s
% Output : Proof 0.35s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.11 % Problem : KRS078+1 : TPTP v8.1.2. Released v3.1.0.
% 0.07/0.12 % Command : nanocop.sh %s %d
% 0.12/0.33 % Computer : n016.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 23:32:12 EDT 2023
% 0.12/0.33 % CPUTime :
% 0.35/1.37
% 0.35/1.37 /export/starexec/sandbox2/benchmark/theBenchmark.p is Unsatisfiable
% 0.35/1.37 Start of proof for negated /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.35/1.37 %-----------------------------------------------------
% 0.35/1.37 ncf(matrix, plain, [(2 ^ _59246) ^ [_59350] : [-(_59350 = _59350)], (4 ^ _59246) ^ [_59457, _59459] : [_59459 = _59457, -(_59457 = _59459)], (10 ^ _59246) ^ [_59661, _59663, _59665] : [-(_59665 = _59661), _59665 = _59663, _59663 = _59661], (20 ^ _59246) ^ [_59974, _59976] : [-(cowlThing(_59974)), _59976 = _59974, cowlThing(_59976)], (30 ^ _59246) ^ [_60269, _60271] : [-(cowlNothing(_60269)), _60271 = _60269, cowlNothing(_60271)], (40 ^ _59246) ^ [_60564, _60566] : [-(xsd_string(_60564)), _60566 = _60564, xsd_string(_60566)], (50 ^ _59246) ^ [_60859, _60861] : [-(xsd_integer(_60859)), _60861 = _60859, xsd_integer(_60861)], (60 ^ _59246) ^ [_61182, _61184, _61186, _61188] : [-(rs(_61186, _61182)), rs(_61188, _61184), _61188 = _61186, _61184 = _61182], (74 ^ _59246) ^ [_61598, _61600] : [-(cq(_61598)), _61600 = _61598, cq(_61600)], (84 ^ _59246) ^ [_61893, _61895] : [-(cp(_61893)), _61895 = _61893, cp(_61895)], (94 ^ _59246) ^ [_62216, _62218, _62220, _62222] : [-(rinvR(_62220, _62216)), rinvR(_62222, _62218), _62222 = _62220, _62218 = _62216], (122 ^ _59246) ^ [_63056, _63058] : [-(cUnsatisfiable(_63056)), _63058 = _63056, cUnsatisfiable(_63058)], (108 ^ _59246) ^ [_62660, _62662, _62664, _62666] : [-(rr(_62664, _62660)), rr(_62666, _62662), _62666 = _62664, _62662 = _62660], (132 ^ _59246) ^ [_63375, _63377] : [-(cUnsatisfiable(_63375)), _63377 = _63375, cUnsatisfiable(_63377)], (142 ^ _59246) ^ [_63670, _63672] : [-(cowlNothing(_63670)), _63672 = _63670, cowlNothing(_63672)], (152 ^ _59246) ^ [_63965, _63967] : [-(cowlThing(_63965)), _63967 = _63965, cowlThing(_63967)], (162 ^ _59246) ^ [_64260, _64262] : [-(cp(_64260)), _64262 = _64260, cp(_64262)], (172 ^ _59246) ^ [_64555, _64557] : [-(cq(_64555)), _64557 = _64555, cq(_64557)], (182 ^ _59246) ^ [_64864, _64866, _64868] : [-(rinvR(_64866, _64864)), _64868 = _64866, rinvR(_64868, _64864)], (192 ^ _59246) ^ [_65187, _65189, _65191] : [-(rinvR(_65187, _65189)), _65191 = _65189, rinvR(_65187, _65191)], (202 ^ _59246) ^ [_65510, _65512, _65514] : [-(rr(_65512, _65510)), _65514 = _65512, rr(_65514, _65510)], (212 ^ _59246) ^ [_65833, _65835, _65837] : [-(rr(_65833, _65835)), _65837 = _65835, rr(_65833, _65837)], (222 ^ _59246) ^ [_66156, _66158, _66160] : [-(rs(_66158, _66156)), _66160 = _66158, rs(_66160, _66156)], (232 ^ _59246) ^ [_66479, _66481, _66483] : [-(rs(_66479, _66481)), _66483 = _66481, rs(_66479, _66483)], (242 ^ _59246) ^ [_66788, _66790] : [-(xsd_integer(_66788)), _66790 = _66788, xsd_integer(_66790)], (252 ^ _59246) ^ [_67083, _67085] : [-(xsd_string(_67083)), _67085 = _67083, xsd_string(_67085)], (262 ^ _59246) ^ [_67369] : [-(cowlThing(_67369))], (264 ^ _59246) ^ [_67411] : [cowlNothing(_67411)], (266 ^ _59246) ^ [_67534] : [xsd_string(_67534), xsd_integer(_67534)], (272 ^ _59246) ^ [_67687] : [-(xsd_integer(_67687)), -(xsd_string(_67687))], (362 ^ _59246) ^ [] : [-(cUnsatisfiable(i2003_11_14_17_19_13721))], (350 ^ _59246) ^ [_70680, _70682] : [rinvR(_70682, _70680), -(rr(_70680, _70682))], (356 ^ _59246) ^ [_70842, _70844] : [rr(_70842, _70844), -(rinvR(_70844, _70842))], (278 ^ _59246) ^ [_67907] : [cUnsatisfiable(_67907), 282 ^ _59246 : [(305 ^ _59246) ^ [] : [-(rs(_67907, 303 ^ [_67907]))], (307 ^ _59246) ^ [] : [cq(303 ^ [_67907])], (309 ^ _59246) ^ [] : [cp(303 ^ [_67907])], (283 ^ _59246) ^ [] : [-(rr(_67907, 281 ^ [_67907]))], (286 ^ _59246) ^ [] : [-(rinvR(281 ^ [_67907], 284 ^ [_67907]))], (288 ^ _59246) ^ [_68453] : [rs(284 ^ [_67907], _68453), -(cp(_68453))], (294 ^ _59246) ^ [_68655, _68657] : [-(_68657 = _68655), rinvR(281 ^ [_67907], _68657), rinvR(281 ^ [_67907], _68655)]]], (311 ^ _59246) ^ [_69197] : [-(cUnsatisfiable(_69197)), 337 ^ _59246 : [(338 ^ _59246) ^ [_70294] : [rs(_69197, _70294), -(cq(_70294)), -(cp(_70294))]], 314 ^ _59246 : [(315 ^ _59246) ^ [_69392] : [rr(_69197, _69392), 331 ^ _59246 : [(332 ^ _59246) ^ [] : [-(rinvR(_69392, 329 ^ [_69197, _69392]))], (334 ^ _59246) ^ [] : [-(rinvR(_69392, 330 ^ [_69197, _69392]))], (336 ^ _59246) ^ [] : [329 ^ [_69197, _69392] = 330 ^ [_69197, _69392]]], 320 ^ _59246 : [(321 ^ _59246) ^ [_69603] : [rinvR(_69392, _69603), 325 ^ _59246 : [(326 ^ _59246) ^ [] : [-(rs(_69603, 324 ^ [_69197, _69392, _69603]))], (328 ^ _59246) ^ [] : [cp(324 ^ [_69197, _69392, _69603])]]]]]]]], input).
% 0.35/1.37 ncf('1',plain,[cUnsatisfiable(i2003_11_14_17_19_13721), 307 : cq(303 ^ [i2003_11_14_17_19_13721])],start(278 ^ 0,bind([[_67907], [i2003_11_14_17_19_13721]]))).
% 0.35/1.37 ncf('1.1',plain,[-(cUnsatisfiable(i2003_11_14_17_19_13721))],extension(362 ^ 1)).
% 0.35/1.37 ncf('1.2',plain,[-(cq(303 ^ [i2003_11_14_17_19_13721])), 338 : rs(i2003_11_14_17_19_13721, 303 ^ [i2003_11_14_17_19_13721]), 338 : -(cp(303 ^ [i2003_11_14_17_19_13721])), 338 : -(cUnsatisfiable(i2003_11_14_17_19_13721)), 315 : rr(i2003_11_14_17_19_13721, 281 ^ [i2003_11_14_17_19_13721]), 332 : -(rinvR(281 ^ [i2003_11_14_17_19_13721], 329 ^ [i2003_11_14_17_19_13721, 281 ^ [i2003_11_14_17_19_13721]])), 321 : rinvR(281 ^ [i2003_11_14_17_19_13721], 284 ^ [i2003_11_14_17_19_13721]), 326 : -(rs(284 ^ [i2003_11_14_17_19_13721], 324 ^ [i2003_11_14_17_19_13721, 281 ^ [i2003_11_14_17_19_13721], 284 ^ [i2003_11_14_17_19_13721]]))],extension(311 ^ 3,bind([[_69197, _70294, _69392, _69603], [i2003_11_14_17_19_13721, 303 ^ [i2003_11_14_17_19_13721], 281 ^ [i2003_11_14_17_19_13721], 284 ^ [i2003_11_14_17_19_13721]]]))).
% 0.35/1.37 ncf('1.2.1',plain,[-(rs(i2003_11_14_17_19_13721, 303 ^ [i2003_11_14_17_19_13721])), rs(i2003_11_14_17_19_13721, 303 ^ [i2003_11_14_17_19_13721]), i2003_11_14_17_19_13721 = i2003_11_14_17_19_13721, 303 ^ [i2003_11_14_17_19_13721] = 303 ^ [i2003_11_14_17_19_13721]],extension(60 ^ 6,bind([[_61182, _61184, _61186, _61188], [303 ^ [i2003_11_14_17_19_13721], 303 ^ [i2003_11_14_17_19_13721], i2003_11_14_17_19_13721, i2003_11_14_17_19_13721]]))).
% 0.35/1.37 ncf('1.2.1.1',plain,[-(rs(i2003_11_14_17_19_13721, 303 ^ [i2003_11_14_17_19_13721])), rs(i2003_11_14_17_19_13721, 303 ^ [i2003_11_14_17_19_13721]), i2003_11_14_17_19_13721 = i2003_11_14_17_19_13721, 303 ^ [i2003_11_14_17_19_13721] = 303 ^ [i2003_11_14_17_19_13721]],extension(60 ^ 7,bind([[_61182, _61184, _61186, _61188], [303 ^ [i2003_11_14_17_19_13721], 303 ^ [i2003_11_14_17_19_13721], i2003_11_14_17_19_13721, i2003_11_14_17_19_13721]]))).
% 0.35/1.37 ncf('1.2.1.1.1',plain,[-(rs(i2003_11_14_17_19_13721, 303 ^ [i2003_11_14_17_19_13721])), rs(i2003_11_14_17_19_13721, 303 ^ [i2003_11_14_17_19_13721]), i2003_11_14_17_19_13721 = i2003_11_14_17_19_13721, 303 ^ [i2003_11_14_17_19_13721] = 303 ^ [i2003_11_14_17_19_13721]],extension(60 ^ 8,bind([[_61182, _61184, _61186, _61188], [303 ^ [i2003_11_14_17_19_13721], 303 ^ [i2003_11_14_17_19_13721], i2003_11_14_17_19_13721, i2003_11_14_17_19_13721]]))).
% 0.35/1.37 ncf('1.2.1.1.1.1',plain,[-(rs(i2003_11_14_17_19_13721, 303 ^ [i2003_11_14_17_19_13721]))],extension(305 ^ 9)).
% 0.35/1.37 ncf('1.2.1.1.1.2',plain,[-(i2003_11_14_17_19_13721 = i2003_11_14_17_19_13721)],extension(2 ^ 9,bind([[_59350], [i2003_11_14_17_19_13721]]))).
% 0.35/1.37 ncf('1.2.1.1.1.3',plain,[-(303 ^ [i2003_11_14_17_19_13721] = 303 ^ [i2003_11_14_17_19_13721])],extension(2 ^ 9,bind([[_59350], [303 ^ [i2003_11_14_17_19_13721]]]))).
% 0.35/1.37 ncf('1.2.1.1.2',plain,[-(i2003_11_14_17_19_13721 = i2003_11_14_17_19_13721)],extension(2 ^ 8,bind([[_59350], [i2003_11_14_17_19_13721]]))).
% 0.35/1.37 ncf('1.2.1.1.3',plain,[-(303 ^ [i2003_11_14_17_19_13721] = 303 ^ [i2003_11_14_17_19_13721])],extension(2 ^ 8,bind([[_59350], [303 ^ [i2003_11_14_17_19_13721]]]))).
% 0.35/1.37 ncf('1.2.1.2',plain,[-(i2003_11_14_17_19_13721 = i2003_11_14_17_19_13721)],extension(2 ^ 7,bind([[_59350], [i2003_11_14_17_19_13721]]))).
% 0.35/1.37 ncf('1.2.1.3',plain,[-(303 ^ [i2003_11_14_17_19_13721] = 303 ^ [i2003_11_14_17_19_13721])],extension(2 ^ 7,bind([[_59350], [303 ^ [i2003_11_14_17_19_13721]]]))).
% 0.35/1.37 ncf('1.2.2',plain,[cp(303 ^ [i2003_11_14_17_19_13721]), -(cp(303 ^ [i2003_11_14_17_19_13721])), 303 ^ [i2003_11_14_17_19_13721] = 303 ^ [i2003_11_14_17_19_13721]],extension(84 ^ 6,bind([[_61893, _61895], [303 ^ [i2003_11_14_17_19_13721], 303 ^ [i2003_11_14_17_19_13721]]]))).
% 0.35/1.37 ncf('1.2.2.1',plain,[cp(303 ^ [i2003_11_14_17_19_13721]), -(cp(303 ^ [i2003_11_14_17_19_13721])), 303 ^ [i2003_11_14_17_19_13721] = 303 ^ [i2003_11_14_17_19_13721]],extension(84 ^ 7,bind([[_61893, _61895], [303 ^ [i2003_11_14_17_19_13721], 303 ^ [i2003_11_14_17_19_13721]]]))).
% 0.35/1.37 ncf('1.2.2.1.1',plain,[cp(303 ^ [i2003_11_14_17_19_13721]), -(cp(303 ^ [i2003_11_14_17_19_13721])), 303 ^ [i2003_11_14_17_19_13721] = 303 ^ [i2003_11_14_17_19_13721]],extension(84 ^ 8,bind([[_61893, _61895], [303 ^ [i2003_11_14_17_19_13721], 303 ^ [i2003_11_14_17_19_13721]]]))).
% 0.35/1.37 ncf('1.2.2.1.1.1',plain,[cp(303 ^ [i2003_11_14_17_19_13721])],extension(309 ^ 9)).
% 0.35/1.37 ncf('1.2.2.1.1.2',plain,[-(303 ^ [i2003_11_14_17_19_13721] = 303 ^ [i2003_11_14_17_19_13721])],extension(2 ^ 9,bind([[_59350], [303 ^ [i2003_11_14_17_19_13721]]]))).
% 0.35/1.37 ncf('1.2.2.1.2',plain,[-(303 ^ [i2003_11_14_17_19_13721] = 303 ^ [i2003_11_14_17_19_13721])],extension(2 ^ 8,bind([[_59350], [303 ^ [i2003_11_14_17_19_13721]]]))).
% 0.35/1.37 ncf('1.2.2.2',plain,[-(303 ^ [i2003_11_14_17_19_13721] = 303 ^ [i2003_11_14_17_19_13721])],extension(2 ^ 7,bind([[_59350], [303 ^ [i2003_11_14_17_19_13721]]]))).
% 0.35/1.37 ncf('1.2.3',plain,[cUnsatisfiable(i2003_11_14_17_19_13721), -(cUnsatisfiable(284 ^ [i2003_11_14_17_19_13721])), i2003_11_14_17_19_13721 = 284 ^ [i2003_11_14_17_19_13721]],extension(122 ^ 4,bind([[_63056, _63058], [284 ^ [i2003_11_14_17_19_13721], i2003_11_14_17_19_13721]]))).
% 0.35/1.37 ncf('1.2.3.1',plain,[cUnsatisfiable(284 ^ [i2003_11_14_17_19_13721]), 305 : -(rs(284 ^ [i2003_11_14_17_19_13721], 303 ^ [284 ^ [i2003_11_14_17_19_13721]]))],extension(278 ^ 5,bind([[_67907], [284 ^ [i2003_11_14_17_19_13721]]]))).
% 0.35/1.37 ncf('1.2.3.1.1',plain,[rs(284 ^ [i2003_11_14_17_19_13721], 303 ^ [284 ^ [i2003_11_14_17_19_13721]]), 288 : -(cp(303 ^ [284 ^ [i2003_11_14_17_19_13721]])), 288 : cUnsatisfiable(i2003_11_14_17_19_13721)],extension(278 ^ 8,bind([[_67907, _68453], [i2003_11_14_17_19_13721, 303 ^ [284 ^ [i2003_11_14_17_19_13721]]]]))).
% 0.35/1.37 ncf('1.2.3.1.1.1',plain,[cp(303 ^ [284 ^ [i2003_11_14_17_19_13721]]), cUnsatisfiable(284 ^ [i2003_11_14_17_19_13721])],extension(278 ^ 11,bind([[_67907], [284 ^ [i2003_11_14_17_19_13721]]]))).
% 0.35/1.37 ncf('1.2.3.1.1.1.1',plain,[-(cUnsatisfiable(284 ^ [i2003_11_14_17_19_13721]))],reduction('1.2.3')).
% 0.35/1.37 ncf('1.2.3.1.1.2',plain,[-(cUnsatisfiable(i2003_11_14_17_19_13721))],reduction('1.2')).
% 0.35/1.37 ncf('1.2.3.2',plain,[-(i2003_11_14_17_19_13721 = 284 ^ [i2003_11_14_17_19_13721]), rinvR(281 ^ [i2003_11_14_17_19_13721], i2003_11_14_17_19_13721), rinvR(281 ^ [i2003_11_14_17_19_13721], 284 ^ [i2003_11_14_17_19_13721])],extension(294 ^ 5,bind([[_68655, _68657], [284 ^ [i2003_11_14_17_19_13721], i2003_11_14_17_19_13721]]))).
% 0.35/1.37 ncf('1.2.3.2.1',plain,[-(rinvR(281 ^ [i2003_11_14_17_19_13721], i2003_11_14_17_19_13721)), rr(i2003_11_14_17_19_13721, 281 ^ [i2003_11_14_17_19_13721])],extension(356 ^ 6,bind([[_70842, _70844], [i2003_11_14_17_19_13721, 281 ^ [i2003_11_14_17_19_13721]]]))).
% 0.35/1.37 ncf('1.2.3.2.1.1',plain,[-(rr(i2003_11_14_17_19_13721, 281 ^ [i2003_11_14_17_19_13721]))],extension(283 ^ 7)).
% 0.35/1.37 ncf('1.2.3.2.2',plain,[-(rinvR(281 ^ [i2003_11_14_17_19_13721], 284 ^ [i2003_11_14_17_19_13721])), rinvR(281 ^ [i2003_11_14_17_19_13721], 284 ^ [i2003_11_14_17_19_13721]), 281 ^ [i2003_11_14_17_19_13721] = 281 ^ [i2003_11_14_17_19_13721], 284 ^ [i2003_11_14_17_19_13721] = 284 ^ [i2003_11_14_17_19_13721]],extension(94 ^ 6,bind([[_62216, _62218, _62220, _62222], [284 ^ [i2003_11_14_17_19_13721], 284 ^ [i2003_11_14_17_19_13721], 281 ^ [i2003_11_14_17_19_13721], 281 ^ [i2003_11_14_17_19_13721]]]))).
% 0.35/1.37 ncf('1.2.3.2.2.1',plain,[-(rinvR(281 ^ [i2003_11_14_17_19_13721], 284 ^ [i2003_11_14_17_19_13721]))],extension(286 ^ 7)).
% 0.35/1.37 ncf('1.2.3.2.2.2',plain,[-(281 ^ [i2003_11_14_17_19_13721] = 281 ^ [i2003_11_14_17_19_13721])],extension(2 ^ 7,bind([[_59350], [281 ^ [i2003_11_14_17_19_13721]]]))).
% 0.35/1.37 ncf('1.2.3.2.2.3',plain,[-(284 ^ [i2003_11_14_17_19_13721] = 284 ^ [i2003_11_14_17_19_13721])],extension(2 ^ 7,bind([[_59350], [284 ^ [i2003_11_14_17_19_13721]]]))).
% 0.35/1.37 ncf('1.2.4',plain,[-(rr(i2003_11_14_17_19_13721, 281 ^ [i2003_11_14_17_19_13721])), rr(i2003_11_14_17_19_13721, 281 ^ [i2003_11_14_17_19_13721]), i2003_11_14_17_19_13721 = i2003_11_14_17_19_13721, 281 ^ [i2003_11_14_17_19_13721] = 281 ^ [i2003_11_14_17_19_13721]],extension(108 ^ 6,bind([[_62660, _62662, _62664, _62666], [281 ^ [i2003_11_14_17_19_13721], 281 ^ [i2003_11_14_17_19_13721], i2003_11_14_17_19_13721, i2003_11_14_17_19_13721]]))).
% 0.35/1.37 ncf('1.2.4.1',plain,[-(rr(i2003_11_14_17_19_13721, 281 ^ [i2003_11_14_17_19_13721])), rr(i2003_11_14_17_19_13721, 281 ^ [i2003_11_14_17_19_13721]), i2003_11_14_17_19_13721 = i2003_11_14_17_19_13721, 281 ^ [i2003_11_14_17_19_13721] = 281 ^ [i2003_11_14_17_19_13721]],extension(108 ^ 7,bind([[_62660, _62662, _62664, _62666], [281 ^ [i2003_11_14_17_19_13721], 281 ^ [i2003_11_14_17_19_13721], i2003_11_14_17_19_13721, i2003_11_14_17_19_13721]]))).
% 0.35/1.37 ncf('1.2.4.1.1',plain,[-(rr(i2003_11_14_17_19_13721, 281 ^ [i2003_11_14_17_19_13721])), rr(i2003_11_14_17_19_13721, 281 ^ [i2003_11_14_17_19_13721]), i2003_11_14_17_19_13721 = i2003_11_14_17_19_13721, 281 ^ [i2003_11_14_17_19_13721] = 281 ^ [i2003_11_14_17_19_13721]],extension(108 ^ 8,bind([[_62660, _62662, _62664, _62666], [281 ^ [i2003_11_14_17_19_13721], 281 ^ [i2003_11_14_17_19_13721], i2003_11_14_17_19_13721, i2003_11_14_17_19_13721]]))).
% 0.35/1.37 ncf('1.2.4.1.1.1',plain,[-(rr(i2003_11_14_17_19_13721, 281 ^ [i2003_11_14_17_19_13721]))],extension(283 ^ 9)).
% 0.35/1.37 ncf('1.2.4.1.1.2',plain,[-(i2003_11_14_17_19_13721 = i2003_11_14_17_19_13721)],extension(2 ^ 9,bind([[_59350], [i2003_11_14_17_19_13721]]))).
% 0.35/1.37 ncf('1.2.4.1.1.3',plain,[-(281 ^ [i2003_11_14_17_19_13721] = 281 ^ [i2003_11_14_17_19_13721])],extension(2 ^ 9,bind([[_59350], [281 ^ [i2003_11_14_17_19_13721]]]))).
% 0.35/1.37 ncf('1.2.4.1.2',plain,[-(i2003_11_14_17_19_13721 = i2003_11_14_17_19_13721)],extension(2 ^ 8,bind([[_59350], [i2003_11_14_17_19_13721]]))).
% 0.35/1.37 ncf('1.2.4.1.3',plain,[-(281 ^ [i2003_11_14_17_19_13721] = 281 ^ [i2003_11_14_17_19_13721])],extension(2 ^ 8,bind([[_59350], [281 ^ [i2003_11_14_17_19_13721]]]))).
% 0.35/1.37 ncf('1.2.4.2',plain,[-(i2003_11_14_17_19_13721 = i2003_11_14_17_19_13721)],extension(2 ^ 7,bind([[_59350], [i2003_11_14_17_19_13721]]))).
% 0.35/1.37 ncf('1.2.4.3',plain,[-(281 ^ [i2003_11_14_17_19_13721] = 281 ^ [i2003_11_14_17_19_13721])],extension(2 ^ 7,bind([[_59350], [281 ^ [i2003_11_14_17_19_13721]]]))).
% 0.35/1.37 ncf('1.2.5',plain,[rinvR(281 ^ [i2003_11_14_17_19_13721], 329 ^ [i2003_11_14_17_19_13721, 281 ^ [i2003_11_14_17_19_13721]]), -(rinvR(281 ^ [i2003_11_14_17_19_13721], 330 ^ [i2003_11_14_17_19_13721, 281 ^ [i2003_11_14_17_19_13721]])), 281 ^ [i2003_11_14_17_19_13721] = 281 ^ [i2003_11_14_17_19_13721], 329 ^ [i2003_11_14_17_19_13721, 281 ^ [i2003_11_14_17_19_13721]] = 330 ^ [i2003_11_14_17_19_13721, 281 ^ [i2003_11_14_17_19_13721]]],extension(94 ^ 8,bind([[_62216, _62218, _62220, _62222], [330 ^ [i2003_11_14_17_19_13721, 281 ^ [i2003_11_14_17_19_13721]], 329 ^ [i2003_11_14_17_19_13721, 281 ^ [i2003_11_14_17_19_13721]], 281 ^ [i2003_11_14_17_19_13721], 281 ^ [i2003_11_14_17_19_13721]]]))).
% 0.35/1.37 ncf('1.2.5.1',plain,[rinvR(281 ^ [i2003_11_14_17_19_13721], 330 ^ [i2003_11_14_17_19_13721, 281 ^ [i2003_11_14_17_19_13721]]), -(rinvR(281 ^ [i2003_11_14_17_19_13721], 329 ^ [i2003_11_14_17_19_13721, 281 ^ [i2003_11_14_17_19_13721]])), 281 ^ [i2003_11_14_17_19_13721] = 281 ^ [i2003_11_14_17_19_13721], 330 ^ [i2003_11_14_17_19_13721, 281 ^ [i2003_11_14_17_19_13721]] = 329 ^ [i2003_11_14_17_19_13721, 281 ^ [i2003_11_14_17_19_13721]]],extension(94 ^ 9,bind([[_62216, _62218, _62220, _62222], [329 ^ [i2003_11_14_17_19_13721, 281 ^ [i2003_11_14_17_19_13721]], 330 ^ [i2003_11_14_17_19_13721, 281 ^ [i2003_11_14_17_19_13721]], 281 ^ [i2003_11_14_17_19_13721], 281 ^ [i2003_11_14_17_19_13721]]]))).
% 0.35/1.37 ncf('1.2.5.1.1',plain,[rinvR(281 ^ [i2003_11_14_17_19_13721], 329 ^ [i2003_11_14_17_19_13721, 281 ^ [i2003_11_14_17_19_13721]]), -(329 ^ [i2003_11_14_17_19_13721, 281 ^ [i2003_11_14_17_19_13721]] = 330 ^ [i2003_11_14_17_19_13721, 281 ^ [i2003_11_14_17_19_13721]]), rinvR(281 ^ [i2003_11_14_17_19_13721], 330 ^ [i2003_11_14_17_19_13721, 281 ^ [i2003_11_14_17_19_13721]])],extension(294 ^ 10,bind([[_68655, _68657], [330 ^ [i2003_11_14_17_19_13721, 281 ^ [i2003_11_14_17_19_13721]], 329 ^ [i2003_11_14_17_19_13721, 281 ^ [i2003_11_14_17_19_13721]]]]))).
% 0.35/1.37 ncf('1.2.5.1.1.1',plain,[329 ^ [i2003_11_14_17_19_13721, 281 ^ [i2003_11_14_17_19_13721]] = 330 ^ [i2003_11_14_17_19_13721, 281 ^ [i2003_11_14_17_19_13721]]],extension(336 ^ 11)).
% 0.35/1.37 ncf('1.2.5.1.1.2',plain,[-(rinvR(281 ^ [i2003_11_14_17_19_13721], 330 ^ [i2003_11_14_17_19_13721, 281 ^ [i2003_11_14_17_19_13721]]))],reduction('1.2.5')).
% 0.35/1.37 ncf('1.2.5.1.2',plain,[-(281 ^ [i2003_11_14_17_19_13721] = 281 ^ [i2003_11_14_17_19_13721])],extension(2 ^ 10,bind([[_59350], [281 ^ [i2003_11_14_17_19_13721]]]))).
% 0.35/1.37 ncf('1.2.5.1.3',plain,[-(330 ^ [i2003_11_14_17_19_13721, 281 ^ [i2003_11_14_17_19_13721]] = 329 ^ [i2003_11_14_17_19_13721, 281 ^ [i2003_11_14_17_19_13721]]), 329 ^ [i2003_11_14_17_19_13721, 281 ^ [i2003_11_14_17_19_13721]] = 330 ^ [i2003_11_14_17_19_13721, 281 ^ [i2003_11_14_17_19_13721]]],extension(4 ^ 10,bind([[_59457, _59459], [330 ^ [i2003_11_14_17_19_13721, 281 ^ [i2003_11_14_17_19_13721]], 329 ^ [i2003_11_14_17_19_13721, 281 ^ [i2003_11_14_17_19_13721]]]]))).
% 0.35/1.37 ncf('1.2.5.1.3.1',plain,[-(329 ^ [i2003_11_14_17_19_13721, 281 ^ [i2003_11_14_17_19_13721]] = 330 ^ [i2003_11_14_17_19_13721, 281 ^ [i2003_11_14_17_19_13721]]), rinvR(281 ^ [i2003_11_14_17_19_13721], 329 ^ [i2003_11_14_17_19_13721, 281 ^ [i2003_11_14_17_19_13721]]), rinvR(281 ^ [i2003_11_14_17_19_13721], 330 ^ [i2003_11_14_17_19_13721, 281 ^ [i2003_11_14_17_19_13721]])],extension(294 ^ 11,bind([[_68655, _68657], [330 ^ [i2003_11_14_17_19_13721, 281 ^ [i2003_11_14_17_19_13721]], 329 ^ [i2003_11_14_17_19_13721, 281 ^ [i2003_11_14_17_19_13721]]]]))).
% 0.35/1.37 ncf('1.2.5.1.3.1.1',plain,[-(rinvR(281 ^ [i2003_11_14_17_19_13721], 329 ^ [i2003_11_14_17_19_13721, 281 ^ [i2003_11_14_17_19_13721]]))],reduction('1.2')).
% 0.35/1.37 ncf('1.2.5.1.3.1.2',plain,[-(rinvR(281 ^ [i2003_11_14_17_19_13721], 330 ^ [i2003_11_14_17_19_13721, 281 ^ [i2003_11_14_17_19_13721]]))],reduction('1.2.5')).
% 0.35/1.37 ncf('1.2.5.2',plain,[-(281 ^ [i2003_11_14_17_19_13721] = 281 ^ [i2003_11_14_17_19_13721])],extension(2 ^ 9,bind([[_59350], [281 ^ [i2003_11_14_17_19_13721]]]))).
% 0.35/1.37 ncf('1.2.5.3',plain,[-(329 ^ [i2003_11_14_17_19_13721, 281 ^ [i2003_11_14_17_19_13721]] = 330 ^ [i2003_11_14_17_19_13721, 281 ^ [i2003_11_14_17_19_13721]]), 330 ^ [i2003_11_14_17_19_13721, 281 ^ [i2003_11_14_17_19_13721]] = 329 ^ [i2003_11_14_17_19_13721, 281 ^ [i2003_11_14_17_19_13721]]],extension(4 ^ 9,bind([[_59457, _59459], [329 ^ [i2003_11_14_17_19_13721, 281 ^ [i2003_11_14_17_19_13721]], 330 ^ [i2003_11_14_17_19_13721, 281 ^ [i2003_11_14_17_19_13721]]]]))).
% 0.35/1.37 ncf('1.2.5.3.1',plain,[-(330 ^ [i2003_11_14_17_19_13721, 281 ^ [i2003_11_14_17_19_13721]] = 329 ^ [i2003_11_14_17_19_13721, 281 ^ [i2003_11_14_17_19_13721]]), rinvR(281 ^ [i2003_11_14_17_19_13721], 330 ^ [i2003_11_14_17_19_13721, 281 ^ [i2003_11_14_17_19_13721]]), rinvR(281 ^ [i2003_11_14_17_19_13721], 329 ^ [i2003_11_14_17_19_13721, 281 ^ [i2003_11_14_17_19_13721]])],extension(294 ^ 10,bind([[_68655, _68657], [329 ^ [i2003_11_14_17_19_13721, 281 ^ [i2003_11_14_17_19_13721]], 330 ^ [i2003_11_14_17_19_13721, 281 ^ [i2003_11_14_17_19_13721]]]]))).
% 0.35/1.37 ncf('1.2.5.3.1.1',plain,[-(rinvR(281 ^ [i2003_11_14_17_19_13721], 330 ^ [i2003_11_14_17_19_13721, 281 ^ [i2003_11_14_17_19_13721]]))],extension(334 ^ 11)).
% 0.35/1.37 ncf('1.2.5.3.1.2',plain,[-(rinvR(281 ^ [i2003_11_14_17_19_13721], 329 ^ [i2003_11_14_17_19_13721, 281 ^ [i2003_11_14_17_19_13721]]))],reduction('1.2')).
% 0.35/1.37 ncf('1.2.6',plain,[-(rinvR(281 ^ [i2003_11_14_17_19_13721], 284 ^ [i2003_11_14_17_19_13721])), rinvR(281 ^ [i2003_11_14_17_19_13721], 284 ^ [i2003_11_14_17_19_13721]), 281 ^ [i2003_11_14_17_19_13721] = 281 ^ [i2003_11_14_17_19_13721], 284 ^ [i2003_11_14_17_19_13721] = 284 ^ [i2003_11_14_17_19_13721]],extension(94 ^ 8,bind([[_62216, _62218, _62220, _62222], [284 ^ [i2003_11_14_17_19_13721], 284 ^ [i2003_11_14_17_19_13721], 281 ^ [i2003_11_14_17_19_13721], 281 ^ [i2003_11_14_17_19_13721]]]))).
% 0.35/1.37 ncf('1.2.6.1',plain,[-(rinvR(281 ^ [i2003_11_14_17_19_13721], 284 ^ [i2003_11_14_17_19_13721])), rinvR(281 ^ [i2003_11_14_17_19_13721], 284 ^ [i2003_11_14_17_19_13721]), 281 ^ [i2003_11_14_17_19_13721] = 281 ^ [i2003_11_14_17_19_13721], 284 ^ [i2003_11_14_17_19_13721] = 284 ^ [i2003_11_14_17_19_13721]],extension(94 ^ 9,bind([[_62216, _62218, _62220, _62222], [284 ^ [i2003_11_14_17_19_13721], 284 ^ [i2003_11_14_17_19_13721], 281 ^ [i2003_11_14_17_19_13721], 281 ^ [i2003_11_14_17_19_13721]]]))).
% 0.35/1.37 ncf('1.2.6.1.1',plain,[-(rinvR(281 ^ [i2003_11_14_17_19_13721], 284 ^ [i2003_11_14_17_19_13721])), rinvR(281 ^ [i2003_11_14_17_19_13721], 284 ^ [i2003_11_14_17_19_13721]), 281 ^ [i2003_11_14_17_19_13721] = 281 ^ [i2003_11_14_17_19_13721], 284 ^ [i2003_11_14_17_19_13721] = 284 ^ [i2003_11_14_17_19_13721]],extension(94 ^ 10,bind([[_62216, _62218, _62220, _62222], [284 ^ [i2003_11_14_17_19_13721], 284 ^ [i2003_11_14_17_19_13721], 281 ^ [i2003_11_14_17_19_13721], 281 ^ [i2003_11_14_17_19_13721]]]))).
% 0.35/1.37 ncf('1.2.6.1.1.1',plain,[-(rinvR(281 ^ [i2003_11_14_17_19_13721], 284 ^ [i2003_11_14_17_19_13721]))],extension(286 ^ 11)).
% 0.35/1.37 ncf('1.2.6.1.1.2',plain,[-(281 ^ [i2003_11_14_17_19_13721] = 281 ^ [i2003_11_14_17_19_13721])],extension(2 ^ 11,bind([[_59350], [281 ^ [i2003_11_14_17_19_13721]]]))).
% 0.35/1.37 ncf('1.2.6.1.1.3',plain,[-(284 ^ [i2003_11_14_17_19_13721] = 284 ^ [i2003_11_14_17_19_13721])],extension(2 ^ 11,bind([[_59350], [284 ^ [i2003_11_14_17_19_13721]]]))).
% 0.35/1.37 ncf('1.2.6.1.2',plain,[-(281 ^ [i2003_11_14_17_19_13721] = 281 ^ [i2003_11_14_17_19_13721])],extension(2 ^ 10,bind([[_59350], [281 ^ [i2003_11_14_17_19_13721]]]))).
% 0.35/1.37 ncf('1.2.6.1.3',plain,[-(284 ^ [i2003_11_14_17_19_13721] = 284 ^ [i2003_11_14_17_19_13721])],extension(2 ^ 10,bind([[_59350], [284 ^ [i2003_11_14_17_19_13721]]]))).
% 0.35/1.37 ncf('1.2.6.2',plain,[-(281 ^ [i2003_11_14_17_19_13721] = 281 ^ [i2003_11_14_17_19_13721])],extension(2 ^ 9,bind([[_59350], [281 ^ [i2003_11_14_17_19_13721]]]))).
% 0.35/1.37 ncf('1.2.6.3',plain,[-(284 ^ [i2003_11_14_17_19_13721] = 284 ^ [i2003_11_14_17_19_13721])],extension(2 ^ 9,bind([[_59350], [284 ^ [i2003_11_14_17_19_13721]]]))).
% 0.35/1.37 ncf('1.2.7',plain,[rs(284 ^ [i2003_11_14_17_19_13721], 324 ^ [i2003_11_14_17_19_13721, 281 ^ [i2003_11_14_17_19_13721], 284 ^ [i2003_11_14_17_19_13721]]), -(rs(284 ^ [i2003_11_14_17_19_13721], 324 ^ [i2003_11_14_17_19_13721, 281 ^ [i2003_11_14_17_19_13721], 284 ^ [i2003_11_14_17_19_13721]])), 284 ^ [i2003_11_14_17_19_13721] = 284 ^ [i2003_11_14_17_19_13721]],extension(222 ^ 10,bind([[_66156, _66158, _66160], [324 ^ [i2003_11_14_17_19_13721, 281 ^ [i2003_11_14_17_19_13721], 284 ^ [i2003_11_14_17_19_13721]], 284 ^ [i2003_11_14_17_19_13721], 284 ^ [i2003_11_14_17_19_13721]]]))).
% 0.35/1.37 ncf('1.2.7.1',plain,[rs(284 ^ [i2003_11_14_17_19_13721], 324 ^ [i2003_11_14_17_19_13721, 281 ^ [i2003_11_14_17_19_13721], 284 ^ [i2003_11_14_17_19_13721]]), -(rs(284 ^ [i2003_11_14_17_19_13721], 324 ^ [i2003_11_14_17_19_13721, 281 ^ [i2003_11_14_17_19_13721], 284 ^ [i2003_11_14_17_19_13721]])), 284 ^ [i2003_11_14_17_19_13721] = 284 ^ [i2003_11_14_17_19_13721]],extension(222 ^ 11,bind([[_66156, _66158, _66160], [324 ^ [i2003_11_14_17_19_13721, 281 ^ [i2003_11_14_17_19_13721], 284 ^ [i2003_11_14_17_19_13721]], 284 ^ [i2003_11_14_17_19_13721], 284 ^ [i2003_11_14_17_19_13721]]]))).
% 0.35/1.37 ncf('1.2.7.1.1',plain,[rs(284 ^ [i2003_11_14_17_19_13721], 324 ^ [i2003_11_14_17_19_13721, 281 ^ [i2003_11_14_17_19_13721], 284 ^ [i2003_11_14_17_19_13721]]), -(cp(324 ^ [i2003_11_14_17_19_13721, 281 ^ [i2003_11_14_17_19_13721], 284 ^ [i2003_11_14_17_19_13721]]))],extension(288 ^ 12,bind([[_68453], [324 ^ [i2003_11_14_17_19_13721, 281 ^ [i2003_11_14_17_19_13721], 284 ^ [i2003_11_14_17_19_13721]]]]))).
% 0.35/1.37 ncf('1.2.7.1.1.1',plain,[cp(324 ^ [i2003_11_14_17_19_13721, 281 ^ [i2003_11_14_17_19_13721], 284 ^ [i2003_11_14_17_19_13721]])],extension(328 ^ 13)).
% 0.35/1.37 ncf('1.2.7.1.2',plain,[-(284 ^ [i2003_11_14_17_19_13721] = 284 ^ [i2003_11_14_17_19_13721])],extension(2 ^ 12,bind([[_59350], [284 ^ [i2003_11_14_17_19_13721]]]))).
% 0.35/1.37 ncf('1.2.7.2',plain,[-(284 ^ [i2003_11_14_17_19_13721] = 284 ^ [i2003_11_14_17_19_13721])],extension(2 ^ 11,bind([[_59350], [284 ^ [i2003_11_14_17_19_13721]]]))).
% 0.35/1.37 %-----------------------------------------------------
% 0.35/1.37 End of proof for negated /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------