%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : KRS075+1 : TPTP v8.1.2. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n015.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.81s 1.37s
% Output : Proof 0.81s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12 % Problem : KRS075+1 : TPTP v8.1.2. Released v3.1.0.
% 0.06/0.12 % Command : nanocop.sh %s %d
% 0.12/0.33 % Computer : n015.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:22:22 EDT 2023
% 0.12/0.33 % CPUTime :
% 0.81/1.37
% 0.81/1.37 /export/starexec/sandbox/benchmark/theBenchmark.p is Unsatisfiable
% 0.81/1.37 Start of proof for negated /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.81/1.37 %-----------------------------------------------------
% 0.81/1.37 ncf(matrix, plain, [(2 ^ _73129) ^ [_73233] : [-(_73233 = _73233)], (4 ^ _73129) ^ [_73340, _73342] : [_73342 = _73340, -(_73340 = _73342)], (10 ^ _73129) ^ [_73544, _73546, _73548] : [-(_73548 = _73544), _73548 = _73546, _73546 = _73544], (20 ^ _73129) ^ [_73857, _73859] : [-(cowlNothing(_73857)), _73859 = _73857, cowlNothing(_73859)], (30 ^ _73129) ^ [_74152, _74154] : [-(xsd_string(_74152)), _74154 = _74152, xsd_string(_74154)], (40 ^ _73129) ^ [_74447, _74449] : [-(xsd_integer(_74447)), _74449 = _74447, xsd_integer(_74449)], (50 ^ _73129) ^ [_74742, _74744] : [-(cowlThing(_74742)), _74744 = _74742, cowlThing(_74744)], (60 ^ _73129) ^ [_75037, _75039] : [-(cp(_75037)), _75039 = _75037, cp(_75039)], (70 ^ _73129) ^ [_75360, _75362, _75364, _75366] : [-(rinvF(_75364, _75360)), rinvF(_75366, _75362), _75366 = _75364, _75362 = _75360], (84 ^ _73129) ^ [_75804, _75806, _75808, _75810] : [-(rinvF1(_75808, _75804)), rinvF1(_75810, _75806), _75810 = _75808, _75806 = _75804], (98 ^ _73129) ^ [_76248, _76250, _76252, _76254] : [-(rinvS(_76252, _76248)), rinvS(_76254, _76250), _76254 = _76252, _76250 = _76248], (112 ^ _73129) ^ [_76664, _76666] : [-(cUnsatisfiable(_76664)), _76666 = _76664, cUnsatisfiable(_76666)], (122 ^ _73129) ^ [_76987, _76989, _76991, _76993] : [-(rf1(_76991, _76987)), rf1(_76993, _76989), _76993 = _76991, _76989 = _76987], (136 ^ _73129) ^ [_77431, _77433, _77435, _77437] : [-(rs(_77435, _77431)), rs(_77437, _77433), _77437 = _77435, _77433 = _77431], (150 ^ _73129) ^ [_77855, _77857, _77859, _77861] : [-(rf(_77859, _77855)), rf(_77861, _77857), _77861 = _77859, _77857 = _77855], (164 ^ _73129) ^ [_78299, _78301] : [-(cUnsatisfiable(_78299)), _78301 = _78299, cUnsatisfiable(_78301)], (174 ^ _73129) ^ [_78594, _78596] : [-(cowlNothing(_78594)), _78596 = _78594, cowlNothing(_78596)], (184 ^ _73129) ^ [_78889, _78891] : [-(cowlThing(_78889)), _78891 = _78889, cowlThing(_78891)], (194 ^ _73129) ^ [_79184, _79186] : [-(cp(_79184)), _79186 = _79184, cp(_79186)], (204 ^ _73129) ^ [_79493, _79495, _79497] : [-(rf(_79495, _79493)), _79497 = _79495, rf(_79497, _79493)], (214 ^ _73129) ^ [_79816, _79818, _79820] : [-(rf(_79816, _79818)), _79820 = _79818, rf(_79816, _79820)], (224 ^ _73129) ^ [_80139, _80141, _80143] : [-(rf1(_80141, _80139)), _80143 = _80141, rf1(_80143, _80139)], (234 ^ _73129) ^ [_80462, _80464, _80466] : [-(rf1(_80462, _80464)), _80466 = _80464, rf1(_80462, _80466)], (244 ^ _73129) ^ [_80785, _80787, _80789] : [-(rinvF(_80787, _80785)), _80789 = _80787, rinvF(_80789, _80785)], (254 ^ _73129) ^ [_81108, _81110, _81112] : [-(rinvF(_81108, _81110)), _81112 = _81110, rinvF(_81108, _81112)], (264 ^ _73129) ^ [_81431, _81433, _81435] : [-(rinvF1(_81433, _81431)), _81435 = _81433, rinvF1(_81435, _81431)], (274 ^ _73129) ^ [_81754, _81756, _81758] : [-(rinvF1(_81754, _81756)), _81758 = _81756, rinvF1(_81754, _81758)], (284 ^ _73129) ^ [_82077, _82079, _82081] : [-(rinvS(_82079, _82077)), _82081 = _82079, rinvS(_82081, _82077)], (294 ^ _73129) ^ [_82400, _82402, _82404] : [-(rinvS(_82400, _82402)), _82404 = _82402, rinvS(_82400, _82404)], (304 ^ _73129) ^ [_82723, _82725, _82727] : [-(rs(_82725, _82723)), _82727 = _82725, rs(_82727, _82723)], (314 ^ _73129) ^ [_83046, _83048, _83050] : [-(rs(_83046, _83048)), _83050 = _83048, rs(_83046, _83050)], (324 ^ _73129) ^ [_83355, _83357] : [-(xsd_integer(_83355)), _83357 = _83355, xsd_integer(_83357)], (334 ^ _73129) ^ [_83650, _83652] : [-(xsd_string(_83650)), _83652 = _83650, xsd_string(_83652)], (344 ^ _73129) ^ [_83936] : [-(cowlThing(_83936))], (346 ^ _73129) ^ [_83978] : [cowlNothing(_83978)], (348 ^ _73129) ^ [_84101] : [xsd_string(_84101), xsd_integer(_84101)], (354 ^ _73129) ^ [_84254] : [-(xsd_integer(_84254)), -(xsd_string(_84254))], (360 ^ _73129) ^ [_84474] : [cUnsatisfiable(_84474), 364 ^ _73129 : [(365 ^ _73129) ^ [] : [-(rf1(_84474, 363 ^ [_84474]))], (367 ^ _73129) ^ [] : [cp(363 ^ [_84474])], (370 ^ _73129) ^ [] : [-(rs(_84474, 368 ^ [_84474]))], (372 ^ _73129) ^ [] : [-(cowlThing(368 ^ [_84474]))], (375 ^ _73129) ^ [] : [-(rf(_84474, 373 ^ [_84474]))], (377 ^ _73129) ^ [] : [-(cp(373 ^ [_84474]))]]], (379 ^ _73129) ^ [_85173] : [-(cUnsatisfiable(_85173)), 382 ^ _73129 : [(383 ^ _73129) ^ [_85327] : [rf1(_85173, _85327), -(cp(_85327))]], 390 ^ _73129 : [(391 ^ _73129) ^ [_85537] : [rs(_85173, _85537), cowlThing(_85537)]], 396 ^ _73129 : [(397 ^ _73129) ^ [_85712] : [rf(_85173, _85712), cp(_85712)]]], (405 ^ _73129) ^ [_85995, _85997, _85999] : [-(_85997 = _85995), rf(_85999, _85997), rf(_85999, _85995)], (415 ^ _73129) ^ [_86318, _86320, _86322] : [-(_86320 = _86318), rf1(_86322, _86320), rf1(_86322, _86318)], (425 ^ _73129) ^ [_86656, _86658] : [rinvF(_86658, _86656), -(rf(_86656, _86658))], (431 ^ _73129) ^ [_86818, _86820] : [rf(_86818, _86820), -(rinvF(_86820, _86818))], (437 ^ _73129) ^ [_87059, _87061] : [rinvF1(_87061, _87059), -(rf1(_87059, _87061))], (443 ^ _73129) ^ [_87221, _87223] : [rf1(_87221, _87223), -(rinvF1(_87223, _87221))], (449 ^ _73129) ^ [_87462, _87464] : [rinvS(_87464, _87462), -(rs(_87462, _87464))], (455 ^ _73129) ^ [_87624, _87626] : [rs(_87624, _87626), -(rinvS(_87626, _87624))], (461 ^ _73129) ^ [_87850, _87852, _87854] : [-(_87852 = _87850), rs(_87854, _87852), rs(_87854, _87850)], (471 ^ _73129) ^ [] : [-(cUnsatisfiable(i2003_11_14_17_19_02584))], (473 ^ _73129) ^ [_88212, _88214] : [rs(_88214, _88212), -(rf1(_88214, _88212))], (479 ^ _73129) ^ [_88402, _88404] : [rs(_88404, _88402), -(rf(_88404, _88402))]], input).
% 0.81/1.37 ncf('1',plain,[cUnsatisfiable(i2003_11_14_17_19_02584), 367 : cp(363 ^ [i2003_11_14_17_19_02584])],start(360 ^ 0,bind([[_84474], [i2003_11_14_17_19_02584]]))).
% 0.81/1.37 ncf('1.1',plain,[-(cUnsatisfiable(i2003_11_14_17_19_02584))],extension(471 ^ 1)).
% 0.81/1.37 ncf('1.2',plain,[-(cp(363 ^ [i2003_11_14_17_19_02584])), 383 : rf1(i2003_11_14_17_19_02584, 363 ^ [i2003_11_14_17_19_02584]), 383 : -(cUnsatisfiable(i2003_11_14_17_19_02584)), 391 : rs(i2003_11_14_17_19_02584, 368 ^ [i2003_11_14_17_19_02584]), 391 : cowlThing(368 ^ [i2003_11_14_17_19_02584]), 397 : rf(i2003_11_14_17_19_02584, 373 ^ [i2003_11_14_17_19_02584]), 397 : cp(373 ^ [i2003_11_14_17_19_02584])],extension(379 ^ 3,bind([[_85173, _85327, _85537, _85712], [i2003_11_14_17_19_02584, 363 ^ [i2003_11_14_17_19_02584], 368 ^ [i2003_11_14_17_19_02584], 373 ^ [i2003_11_14_17_19_02584]]]))).
% 0.81/1.37 ncf('1.2.1',plain,[-(rf1(i2003_11_14_17_19_02584, 363 ^ [i2003_11_14_17_19_02584])), rf1(i2003_11_14_17_19_02584, 363 ^ [i2003_11_14_17_19_02584]), i2003_11_14_17_19_02584 = i2003_11_14_17_19_02584, 363 ^ [i2003_11_14_17_19_02584] = 363 ^ [i2003_11_14_17_19_02584]],extension(122 ^ 6,bind([[_76987, _76989, _76991, _76993], [363 ^ [i2003_11_14_17_19_02584], 363 ^ [i2003_11_14_17_19_02584], i2003_11_14_17_19_02584, i2003_11_14_17_19_02584]]))).
% 0.81/1.37 ncf('1.2.1.1',plain,[-(rf1(i2003_11_14_17_19_02584, 363 ^ [i2003_11_14_17_19_02584])), rf1(i2003_11_14_17_19_02584, 363 ^ [i2003_11_14_17_19_02584]), i2003_11_14_17_19_02584 = i2003_11_14_17_19_02584, 363 ^ [i2003_11_14_17_19_02584] = 363 ^ [i2003_11_14_17_19_02584]],extension(122 ^ 7,bind([[_76987, _76989, _76991, _76993], [363 ^ [i2003_11_14_17_19_02584], 363 ^ [i2003_11_14_17_19_02584], i2003_11_14_17_19_02584, i2003_11_14_17_19_02584]]))).
% 0.81/1.37 ncf('1.2.1.1.1',plain,[-(rf1(i2003_11_14_17_19_02584, 363 ^ [i2003_11_14_17_19_02584])), rf1(i2003_11_14_17_19_02584, 363 ^ [i2003_11_14_17_19_02584]), i2003_11_14_17_19_02584 = i2003_11_14_17_19_02584, 363 ^ [i2003_11_14_17_19_02584] = 363 ^ [i2003_11_14_17_19_02584]],extension(122 ^ 8,bind([[_76987, _76989, _76991, _76993], [363 ^ [i2003_11_14_17_19_02584], 363 ^ [i2003_11_14_17_19_02584], i2003_11_14_17_19_02584, i2003_11_14_17_19_02584]]))).
% 0.81/1.37 ncf('1.2.1.1.1.1',plain,[-(rf1(i2003_11_14_17_19_02584, 363 ^ [i2003_11_14_17_19_02584])), rf1(i2003_11_14_17_19_02584, 363 ^ [i2003_11_14_17_19_02584]), i2003_11_14_17_19_02584 = i2003_11_14_17_19_02584, 363 ^ [i2003_11_14_17_19_02584] = 363 ^ [i2003_11_14_17_19_02584]],extension(122 ^ 9,bind([[_76987, _76989, _76991, _76993], [363 ^ [i2003_11_14_17_19_02584], 363 ^ [i2003_11_14_17_19_02584], i2003_11_14_17_19_02584, i2003_11_14_17_19_02584]]))).
% 0.81/1.37 ncf('1.2.1.1.1.1.1',plain,[-(rf1(i2003_11_14_17_19_02584, 363 ^ [i2003_11_14_17_19_02584])), rf1(i2003_11_14_17_19_02584, 363 ^ [i2003_11_14_17_19_02584]), i2003_11_14_17_19_02584 = i2003_11_14_17_19_02584, 363 ^ [i2003_11_14_17_19_02584] = 363 ^ [i2003_11_14_17_19_02584]],extension(122 ^ 10,bind([[_76987, _76989, _76991, _76993], [363 ^ [i2003_11_14_17_19_02584], 363 ^ [i2003_11_14_17_19_02584], i2003_11_14_17_19_02584, i2003_11_14_17_19_02584]]))).
% 0.81/1.37 ncf('1.2.1.1.1.1.1.1',plain,[-(rf1(i2003_11_14_17_19_02584, 363 ^ [i2003_11_14_17_19_02584]))],extension(365 ^ 11)).
% 0.81/1.37 ncf('1.2.1.1.1.1.1.2',plain,[-(i2003_11_14_17_19_02584 = i2003_11_14_17_19_02584)],extension(2 ^ 11,bind([[_73233], [i2003_11_14_17_19_02584]]))).
% 0.81/1.37 ncf('1.2.1.1.1.1.1.3',plain,[-(363 ^ [i2003_11_14_17_19_02584] = 363 ^ [i2003_11_14_17_19_02584])],extension(2 ^ 11,bind([[_73233], [363 ^ [i2003_11_14_17_19_02584]]]))).
% 0.81/1.37 ncf('1.2.1.1.1.1.2',plain,[-(i2003_11_14_17_19_02584 = i2003_11_14_17_19_02584)],extension(2 ^ 10,bind([[_73233], [i2003_11_14_17_19_02584]]))).
% 0.81/1.37 ncf('1.2.1.1.1.1.3',plain,[-(363 ^ [i2003_11_14_17_19_02584] = 363 ^ [i2003_11_14_17_19_02584])],extension(2 ^ 10,bind([[_73233], [363 ^ [i2003_11_14_17_19_02584]]]))).
% 0.81/1.37 ncf('1.2.1.1.1.2',plain,[-(i2003_11_14_17_19_02584 = i2003_11_14_17_19_02584)],extension(2 ^ 9,bind([[_73233], [i2003_11_14_17_19_02584]]))).
% 0.81/1.37 ncf('1.2.1.1.1.3',plain,[-(363 ^ [i2003_11_14_17_19_02584] = 363 ^ [i2003_11_14_17_19_02584])],extension(2 ^ 9,bind([[_73233], [363 ^ [i2003_11_14_17_19_02584]]]))).
% 0.81/1.37 ncf('1.2.1.1.2',plain,[-(i2003_11_14_17_19_02584 = i2003_11_14_17_19_02584)],extension(2 ^ 8,bind([[_73233], [i2003_11_14_17_19_02584]]))).
% 0.81/1.37 ncf('1.2.1.1.3',plain,[-(363 ^ [i2003_11_14_17_19_02584] = 363 ^ [i2003_11_14_17_19_02584])],extension(2 ^ 8,bind([[_73233], [363 ^ [i2003_11_14_17_19_02584]]]))).
% 0.81/1.37 ncf('1.2.1.2',plain,[-(i2003_11_14_17_19_02584 = i2003_11_14_17_19_02584)],extension(2 ^ 7,bind([[_73233], [i2003_11_14_17_19_02584]]))).
% 0.81/1.37 ncf('1.2.1.3',plain,[-(363 ^ [i2003_11_14_17_19_02584] = 363 ^ [i2003_11_14_17_19_02584])],extension(2 ^ 7,bind([[_73233], [363 ^ [i2003_11_14_17_19_02584]]]))).
% 0.81/1.37 ncf('1.2.2',plain,[cUnsatisfiable(i2003_11_14_17_19_02584), -(cUnsatisfiable(i2003_11_14_17_19_02584)), i2003_11_14_17_19_02584 = i2003_11_14_17_19_02584],extension(112 ^ 4,bind([[_76664, _76666], [i2003_11_14_17_19_02584, i2003_11_14_17_19_02584]]))).
% 0.81/1.37 ncf('1.2.2.1',plain,[cUnsatisfiable(i2003_11_14_17_19_02584), 370 : -(rs(i2003_11_14_17_19_02584, 368 ^ [i2003_11_14_17_19_02584]))],extension(360 ^ 5,bind([[_84474], [i2003_11_14_17_19_02584]]))).
% 0.81/1.37 ncf('1.2.2.1.1',plain,[rs(i2003_11_14_17_19_02584, 368 ^ [i2003_11_14_17_19_02584]), -(368 ^ [i2003_11_14_17_19_02584] = 363 ^ [i2003_11_14_17_19_02584]), rs(i2003_11_14_17_19_02584, 363 ^ [i2003_11_14_17_19_02584])],extension(461 ^ 8,bind([[_87850, _87852, _87854], [363 ^ [i2003_11_14_17_19_02584], 368 ^ [i2003_11_14_17_19_02584], i2003_11_14_17_19_02584]]))).
% 0.81/1.37 ncf('1.2.2.1.1.1',plain,[368 ^ [i2003_11_14_17_19_02584] = 363 ^ [i2003_11_14_17_19_02584], -(373 ^ [i2003_11_14_17_19_02584] = 363 ^ [i2003_11_14_17_19_02584]), 373 ^ [i2003_11_14_17_19_02584] = 368 ^ [i2003_11_14_17_19_02584]],extension(10 ^ 9,bind([[_73544, _73546, _73548], [363 ^ [i2003_11_14_17_19_02584], 368 ^ [i2003_11_14_17_19_02584], 373 ^ [i2003_11_14_17_19_02584]]]))).
% 0.81/1.37 ncf('1.2.2.1.1.1.1',plain,[373 ^ [i2003_11_14_17_19_02584] = 363 ^ [i2003_11_14_17_19_02584], -(cp(363 ^ [i2003_11_14_17_19_02584])), cp(373 ^ [i2003_11_14_17_19_02584])],extension(60 ^ 10,bind([[_75037, _75039], [363 ^ [i2003_11_14_17_19_02584], 373 ^ [i2003_11_14_17_19_02584]]]))).
% 0.81/1.37 ncf('1.2.2.1.1.1.1.1',plain,[cp(363 ^ [i2003_11_14_17_19_02584])],reduction('1')).
% 0.81/1.37 ncf('1.2.2.1.1.1.1.2',plain,[-(cp(373 ^ [i2003_11_14_17_19_02584]))],extension(377 ^ 11)).
% 0.81/1.37 ncf('1.2.2.1.1.1.2',plain,[-(373 ^ [i2003_11_14_17_19_02584] = 368 ^ [i2003_11_14_17_19_02584]), rf(i2003_11_14_17_19_02584, 373 ^ [i2003_11_14_17_19_02584]), rf(i2003_11_14_17_19_02584, 368 ^ [i2003_11_14_17_19_02584])],extension(405 ^ 10,bind([[_85995, _85997, _85999], [368 ^ [i2003_11_14_17_19_02584], 373 ^ [i2003_11_14_17_19_02584], i2003_11_14_17_19_02584]]))).
% 0.81/1.37 ncf('1.2.2.1.1.1.2.1',plain,[-(rf(i2003_11_14_17_19_02584, 373 ^ [i2003_11_14_17_19_02584]))],extension(375 ^ 11)).
% 0.81/1.37 ncf('1.2.2.1.1.1.2.2',plain,[-(rf(i2003_11_14_17_19_02584, 368 ^ [i2003_11_14_17_19_02584])), rs(i2003_11_14_17_19_02584, 368 ^ [i2003_11_14_17_19_02584])],extension(479 ^ 11,bind([[_88402, _88404], [368 ^ [i2003_11_14_17_19_02584], i2003_11_14_17_19_02584]]))).
% 0.81/1.37 ncf('1.2.2.1.1.1.2.2.1',plain,[-(rs(i2003_11_14_17_19_02584, 368 ^ [i2003_11_14_17_19_02584]))],reduction('1.2.2.1')).
% 0.81/1.37 ncf('1.2.2.1.1.2',plain,[-(rs(i2003_11_14_17_19_02584, 363 ^ [i2003_11_14_17_19_02584])), rs(i2003_11_14_17_19_02584, 368 ^ [i2003_11_14_17_19_02584]), i2003_11_14_17_19_02584 = i2003_11_14_17_19_02584, 368 ^ [i2003_11_14_17_19_02584] = 363 ^ [i2003_11_14_17_19_02584]],extension(136 ^ 9,bind([[_77431, _77433, _77435, _77437], [363 ^ [i2003_11_14_17_19_02584], 368 ^ [i2003_11_14_17_19_02584], i2003_11_14_17_19_02584, i2003_11_14_17_19_02584]]))).
% 0.81/1.38 ncf('1.2.2.1.1.2.1',plain,[-(rs(i2003_11_14_17_19_02584, 368 ^ [i2003_11_14_17_19_02584]))],reduction('1.2.2.1')).
% 0.81/1.38 ncf('1.2.2.1.1.2.2',plain,[-(i2003_11_14_17_19_02584 = i2003_11_14_17_19_02584)],extension(2 ^ 10,bind([[_73233], [i2003_11_14_17_19_02584]]))).
% 0.81/1.38 ncf('1.2.2.1.1.2.3',plain,[-(368 ^ [i2003_11_14_17_19_02584] = 363 ^ [i2003_11_14_17_19_02584]), rf1(i2003_11_14_17_19_02584, 368 ^ [i2003_11_14_17_19_02584]), rf1(i2003_11_14_17_19_02584, 363 ^ [i2003_11_14_17_19_02584])],extension(415 ^ 10,bind([[_86318, _86320, _86322], [363 ^ [i2003_11_14_17_19_02584], 368 ^ [i2003_11_14_17_19_02584], i2003_11_14_17_19_02584]]))).
% 0.81/1.38 ncf('1.2.2.1.1.2.3.1',plain,[-(rf1(i2003_11_14_17_19_02584, 368 ^ [i2003_11_14_17_19_02584])), rs(i2003_11_14_17_19_02584, 368 ^ [i2003_11_14_17_19_02584])],extension(473 ^ 11,bind([[_88212, _88214], [368 ^ [i2003_11_14_17_19_02584], i2003_11_14_17_19_02584]]))).
% 0.81/1.38 ncf('1.2.2.1.1.2.3.1.1',plain,[-(rs(i2003_11_14_17_19_02584, 368 ^ [i2003_11_14_17_19_02584]))],reduction('1.2.2.1')).
% 0.81/1.38 ncf('1.2.2.1.1.2.3.2',plain,[-(rf1(i2003_11_14_17_19_02584, 363 ^ [i2003_11_14_17_19_02584]))],extension(365 ^ 11)).
% 0.81/1.38 ncf('1.2.2.2',plain,[-(i2003_11_14_17_19_02584 = i2003_11_14_17_19_02584)],extension(2 ^ 5,bind([[_73233], [i2003_11_14_17_19_02584]]))).
% 0.81/1.38 ncf('1.2.3',plain,[-(rs(i2003_11_14_17_19_02584, 368 ^ [i2003_11_14_17_19_02584])), rs(i2003_11_14_17_19_02584, 368 ^ [i2003_11_14_17_19_02584]), i2003_11_14_17_19_02584 = i2003_11_14_17_19_02584, 368 ^ [i2003_11_14_17_19_02584] = 368 ^ [i2003_11_14_17_19_02584]],extension(136 ^ 6,bind([[_77431, _77433, _77435, _77437], [368 ^ [i2003_11_14_17_19_02584], 368 ^ [i2003_11_14_17_19_02584], i2003_11_14_17_19_02584, i2003_11_14_17_19_02584]]))).
% 0.81/1.38 ncf('1.2.3.1',plain,[-(rs(i2003_11_14_17_19_02584, 368 ^ [i2003_11_14_17_19_02584])), rs(i2003_11_14_17_19_02584, 368 ^ [i2003_11_14_17_19_02584]), i2003_11_14_17_19_02584 = i2003_11_14_17_19_02584, 368 ^ [i2003_11_14_17_19_02584] = 368 ^ [i2003_11_14_17_19_02584]],extension(136 ^ 7,bind([[_77431, _77433, _77435, _77437], [368 ^ [i2003_11_14_17_19_02584], 368 ^ [i2003_11_14_17_19_02584], i2003_11_14_17_19_02584, i2003_11_14_17_19_02584]]))).
% 0.81/1.38 ncf('1.2.3.1.1',plain,[-(rs(i2003_11_14_17_19_02584, 368 ^ [i2003_11_14_17_19_02584])), rs(i2003_11_14_17_19_02584, 368 ^ [i2003_11_14_17_19_02584]), i2003_11_14_17_19_02584 = i2003_11_14_17_19_02584, 368 ^ [i2003_11_14_17_19_02584] = 368 ^ [i2003_11_14_17_19_02584]],extension(136 ^ 8,bind([[_77431, _77433, _77435, _77437], [368 ^ [i2003_11_14_17_19_02584], 368 ^ [i2003_11_14_17_19_02584], i2003_11_14_17_19_02584, i2003_11_14_17_19_02584]]))).
% 0.81/1.38 ncf('1.2.3.1.1.1',plain,[-(rs(i2003_11_14_17_19_02584, 368 ^ [i2003_11_14_17_19_02584])), rs(i2003_11_14_17_19_02584, 368 ^ [i2003_11_14_17_19_02584]), i2003_11_14_17_19_02584 = i2003_11_14_17_19_02584, 368 ^ [i2003_11_14_17_19_02584] = 368 ^ [i2003_11_14_17_19_02584]],extension(136 ^ 9,bind([[_77431, _77433, _77435, _77437], [368 ^ [i2003_11_14_17_19_02584], 368 ^ [i2003_11_14_17_19_02584], i2003_11_14_17_19_02584, i2003_11_14_17_19_02584]]))).
% 0.81/1.38 ncf('1.2.3.1.1.1.1',plain,[-(rs(i2003_11_14_17_19_02584, 368 ^ [i2003_11_14_17_19_02584])), rs(i2003_11_14_17_19_02584, 368 ^ [i2003_11_14_17_19_02584]), i2003_11_14_17_19_02584 = i2003_11_14_17_19_02584, 368 ^ [i2003_11_14_17_19_02584] = 368 ^ [i2003_11_14_17_19_02584]],extension(136 ^ 10,bind([[_77431, _77433, _77435, _77437], [368 ^ [i2003_11_14_17_19_02584], 368 ^ [i2003_11_14_17_19_02584], i2003_11_14_17_19_02584, i2003_11_14_17_19_02584]]))).
% 0.81/1.38 ncf('1.2.3.1.1.1.1.1',plain,[-(rs(i2003_11_14_17_19_02584, 368 ^ [i2003_11_14_17_19_02584]))],extension(370 ^ 11)).
% 0.81/1.38 ncf('1.2.3.1.1.1.1.2',plain,[-(i2003_11_14_17_19_02584 = i2003_11_14_17_19_02584)],extension(2 ^ 11,bind([[_73233], [i2003_11_14_17_19_02584]]))).
% 0.81/1.38 ncf('1.2.3.1.1.1.1.3',plain,[-(368 ^ [i2003_11_14_17_19_02584] = 368 ^ [i2003_11_14_17_19_02584])],extension(2 ^ 11,bind([[_73233], [368 ^ [i2003_11_14_17_19_02584]]]))).
% 0.81/1.38 ncf('1.2.3.1.1.1.2',plain,[-(i2003_11_14_17_19_02584 = i2003_11_14_17_19_02584)],extension(2 ^ 10,bind([[_73233], [i2003_11_14_17_19_02584]]))).
% 0.81/1.38 ncf('1.2.3.1.1.1.3',plain,[-(368 ^ [i2003_11_14_17_19_02584] = 368 ^ [i2003_11_14_17_19_02584])],extension(2 ^ 10,bind([[_73233], [368 ^ [i2003_11_14_17_19_02584]]]))).
% 0.81/1.38 ncf('1.2.3.1.1.2',plain,[-(i2003_11_14_17_19_02584 = i2003_11_14_17_19_02584)],extension(2 ^ 9,bind([[_73233], [i2003_11_14_17_19_02584]]))).
% 0.81/1.38 ncf('1.2.3.1.1.3',plain,[-(368 ^ [i2003_11_14_17_19_02584] = 368 ^ [i2003_11_14_17_19_02584])],extension(2 ^ 9,bind([[_73233], [368 ^ [i2003_11_14_17_19_02584]]]))).
% 0.81/1.38 ncf('1.2.3.1.2',plain,[-(i2003_11_14_17_19_02584 = i2003_11_14_17_19_02584)],extension(2 ^ 8,bind([[_73233], [i2003_11_14_17_19_02584]]))).
% 0.81/1.38 ncf('1.2.3.1.3',plain,[-(368 ^ [i2003_11_14_17_19_02584] = 368 ^ [i2003_11_14_17_19_02584])],extension(2 ^ 8,bind([[_73233], [368 ^ [i2003_11_14_17_19_02584]]]))).
% 0.81/1.38 ncf('1.2.3.2',plain,[-(i2003_11_14_17_19_02584 = i2003_11_14_17_19_02584)],extension(2 ^ 7,bind([[_73233], [i2003_11_14_17_19_02584]]))).
% 0.81/1.38 ncf('1.2.3.3',plain,[-(368 ^ [i2003_11_14_17_19_02584] = 368 ^ [i2003_11_14_17_19_02584])],extension(2 ^ 7,bind([[_73233], [368 ^ [i2003_11_14_17_19_02584]]]))).
% 0.81/1.38 ncf('1.2.4',plain,[-(cowlThing(368 ^ [i2003_11_14_17_19_02584]))],extension(344 ^ 6,bind([[_83936], [368 ^ [i2003_11_14_17_19_02584]]]))).
% 0.81/1.38 ncf('1.2.5',plain,[-(rf(i2003_11_14_17_19_02584, 373 ^ [i2003_11_14_17_19_02584])), rf(i2003_11_14_17_19_02584, 373 ^ [i2003_11_14_17_19_02584]), i2003_11_14_17_19_02584 = i2003_11_14_17_19_02584, 373 ^ [i2003_11_14_17_19_02584] = 373 ^ [i2003_11_14_17_19_02584]],extension(150 ^ 6,bind([[_77855, _77857, _77859, _77861], [373 ^ [i2003_11_14_17_19_02584], 373 ^ [i2003_11_14_17_19_02584], i2003_11_14_17_19_02584, i2003_11_14_17_19_02584]]))).
% 0.81/1.38 ncf('1.2.5.1',plain,[-(rf(i2003_11_14_17_19_02584, 373 ^ [i2003_11_14_17_19_02584])), rf(i2003_11_14_17_19_02584, 373 ^ [i2003_11_14_17_19_02584]), i2003_11_14_17_19_02584 = i2003_11_14_17_19_02584, 373 ^ [i2003_11_14_17_19_02584] = 373 ^ [i2003_11_14_17_19_02584]],extension(150 ^ 7,bind([[_77855, _77857, _77859, _77861], [373 ^ [i2003_11_14_17_19_02584], 373 ^ [i2003_11_14_17_19_02584], i2003_11_14_17_19_02584, i2003_11_14_17_19_02584]]))).
% 0.81/1.38 ncf('1.2.5.1.1',plain,[-(rf(i2003_11_14_17_19_02584, 373 ^ [i2003_11_14_17_19_02584])), rf(i2003_11_14_17_19_02584, 373 ^ [i2003_11_14_17_19_02584]), i2003_11_14_17_19_02584 = i2003_11_14_17_19_02584, 373 ^ [i2003_11_14_17_19_02584] = 373 ^ [i2003_11_14_17_19_02584]],extension(150 ^ 8,bind([[_77855, _77857, _77859, _77861], [373 ^ [i2003_11_14_17_19_02584], 373 ^ [i2003_11_14_17_19_02584], i2003_11_14_17_19_02584, i2003_11_14_17_19_02584]]))).
% 0.81/1.38 ncf('1.2.5.1.1.1',plain,[-(rf(i2003_11_14_17_19_02584, 373 ^ [i2003_11_14_17_19_02584])), rf(i2003_11_14_17_19_02584, 373 ^ [i2003_11_14_17_19_02584]), i2003_11_14_17_19_02584 = i2003_11_14_17_19_02584, 373 ^ [i2003_11_14_17_19_02584] = 373 ^ [i2003_11_14_17_19_02584]],extension(150 ^ 9,bind([[_77855, _77857, _77859, _77861], [373 ^ [i2003_11_14_17_19_02584], 373 ^ [i2003_11_14_17_19_02584], i2003_11_14_17_19_02584, i2003_11_14_17_19_02584]]))).
% 0.81/1.38 ncf('1.2.5.1.1.1.1',plain,[-(rf(i2003_11_14_17_19_02584, 373 ^ [i2003_11_14_17_19_02584])), rf(i2003_11_14_17_19_02584, 373 ^ [i2003_11_14_17_19_02584]), i2003_11_14_17_19_02584 = i2003_11_14_17_19_02584, 373 ^ [i2003_11_14_17_19_02584] = 373 ^ [i2003_11_14_17_19_02584]],extension(150 ^ 10,bind([[_77855, _77857, _77859, _77861], [373 ^ [i2003_11_14_17_19_02584], 373 ^ [i2003_11_14_17_19_02584], i2003_11_14_17_19_02584, i2003_11_14_17_19_02584]]))).
% 0.81/1.38 ncf('1.2.5.1.1.1.1.1',plain,[-(rf(i2003_11_14_17_19_02584, 373 ^ [i2003_11_14_17_19_02584]))],extension(375 ^ 11)).
% 0.81/1.38 ncf('1.2.5.1.1.1.1.2',plain,[-(i2003_11_14_17_19_02584 = i2003_11_14_17_19_02584)],extension(2 ^ 11,bind([[_73233], [i2003_11_14_17_19_02584]]))).
% 0.81/1.38 ncf('1.2.5.1.1.1.1.3',plain,[-(373 ^ [i2003_11_14_17_19_02584] = 373 ^ [i2003_11_14_17_19_02584])],extension(2 ^ 11,bind([[_73233], [373 ^ [i2003_11_14_17_19_02584]]]))).
% 0.81/1.38 ncf('1.2.5.1.1.1.2',plain,[-(i2003_11_14_17_19_02584 = i2003_11_14_17_19_02584)],extension(2 ^ 10,bind([[_73233], [i2003_11_14_17_19_02584]]))).
% 0.81/1.38 ncf('1.2.5.1.1.1.3',plain,[-(373 ^ [i2003_11_14_17_19_02584] = 373 ^ [i2003_11_14_17_19_02584])],extension(2 ^ 10,bind([[_73233], [373 ^ [i2003_11_14_17_19_02584]]]))).
% 0.81/1.38 ncf('1.2.5.1.1.2',plain,[-(i2003_11_14_17_19_02584 = i2003_11_14_17_19_02584)],extension(2 ^ 9,bind([[_73233], [i2003_11_14_17_19_02584]]))).
% 0.81/1.38 ncf('1.2.5.1.1.3',plain,[-(373 ^ [i2003_11_14_17_19_02584] = 373 ^ [i2003_11_14_17_19_02584])],extension(2 ^ 9,bind([[_73233], [373 ^ [i2003_11_14_17_19_02584]]]))).
% 0.81/1.38 ncf('1.2.5.1.2',plain,[-(i2003_11_14_17_19_02584 = i2003_11_14_17_19_02584)],extension(2 ^ 8,bind([[_73233], [i2003_11_14_17_19_02584]]))).
% 0.81/1.38 ncf('1.2.5.1.3',plain,[-(373 ^ [i2003_11_14_17_19_02584] = 373 ^ [i2003_11_14_17_19_02584])],extension(2 ^ 8,bind([[_73233], [373 ^ [i2003_11_14_17_19_02584]]]))).
% 0.81/1.38 ncf('1.2.5.2',plain,[-(i2003_11_14_17_19_02584 = i2003_11_14_17_19_02584)],extension(2 ^ 7,bind([[_73233], [i2003_11_14_17_19_02584]]))).
% 0.81/1.38 ncf('1.2.5.3',plain,[-(373 ^ [i2003_11_14_17_19_02584] = 373 ^ [i2003_11_14_17_19_02584])],extension(2 ^ 7,bind([[_73233], [373 ^ [i2003_11_14_17_19_02584]]]))).
% 0.81/1.38 ncf('1.2.6',plain,[-(cp(373 ^ [i2003_11_14_17_19_02584]))],extension(377 ^ 6)).
% 0.81/1.38 %-----------------------------------------------------
% 0.81/1.38 End of proof for negated /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------