%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : KRS108+1 : TPTP v8.1.2. Released v3.1.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 11:26:17 EDT 2023
% Result : Unsatisfiable 0.36s 1.37s
% Output : Proof 0.36s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : KRS108+1 : TPTP v8.1.2. Released v3.1.0.
% 0.11/0.12 % Command : nanocop.sh %s %d
% 0.12/0.33 % Computer : n011.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:00:03 EDT 2023
% 0.12/0.33 % CPUTime :
% 0.36/1.37
% 0.36/1.37 /export/starexec/sandbox2/benchmark/theBenchmark.p is Unsatisfiable
% 0.36/1.37 Start of proof for negated /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.36/1.37 %-----------------------------------------------------
% 0.36/1.37 ncf(matrix, plain, [(2 ^ _135354) ^ [_135458] : [-(_135458 = _135458)], (4 ^ _135354) ^ [_135565, _135567] : [_135567 = _135565, -(_135565 = _135567)], (10 ^ _135354) ^ [_135769, _135771, _135773] : [-(_135773 = _135769), _135773 = _135771, _135771 = _135769], (20 ^ _135354) ^ [_136082, _136084] : [-(cowlThing(_136082)), _136084 = _136082, cowlThing(_136084)], (30 ^ _135354) ^ [_136377, _136379] : [-(cowlNothing(_136377)), _136379 = _136377, cowlNothing(_136379)], (40 ^ _135354) ^ [_136672, _136674] : [-(xsd_string(_136672)), _136674 = _136672, xsd_string(_136674)], (50 ^ _135354) ^ [_136967, _136969] : [-(xsd_integer(_136967)), _136969 = _136967, xsd_integer(_136969)], (60 ^ _135354) ^ [_137262, _137264] : [-(cp2(_137262)), _137264 = _137262, cp2(_137264)], (70 ^ _135354) ^ [_137585, _137587, _137589, _137591] : [-(ra_Px5(_137589, _137585)), ra_Px5(_137591, _137587), _137591 = _137589, _137587 = _137585], (84 ^ _135354) ^ [_138001, _138003] : [-(cp3(_138001)), _138003 = _138001, cp3(_138003)], (94 ^ _135354) ^ [_138324, _138326, _138328, _138330] : [-(ra_Px6(_138328, _138324)), ra_Px6(_138330, _138326), _138330 = _138328, _138326 = _138324], (108 ^ _135354) ^ [_138740, _138742] : [-(cp4(_138740)), _138742 = _138740, cp4(_138742)], (118 ^ _135354) ^ [_139063, _139065, _139067, _139069] : [-(ra_Px7(_139067, _139063)), ra_Px7(_139069, _139065), _139069 = _139067, _139065 = _139063], (132 ^ _135354) ^ [_139479, _139481] : [-(cp5(_139479)), _139481 = _139479, cp5(_139481)], (142 ^ _135354) ^ [_139802, _139804, _139806, _139808] : [-(ra_Px4(_139806, _139802)), ra_Px4(_139808, _139804), _139808 = _139806, _139804 = _139802], (156 ^ _135354) ^ [_140218, _140220] : [-(ca_Ax14(_140218)), _140220 = _140218, ca_Ax14(_140220)], (166 ^ _135354) ^ [_140513, _140515] : [-(cp1(_140513)), _140515 = _140513, cp1(_140515)], (176 ^ _135354) ^ [_140808, _140810] : [-(cp2xcomp(_140808)), _140810 = _140808, cp2xcomp(_140810)], (186 ^ _135354) ^ [_141103, _141105] : [-(ca_Cx1(_141103)), _141105 = _141103, ca_Cx1(_141105)], (196 ^ _135354) ^ [_141398, _141400] : [-(ca_Cx1xcomp(_141398)), _141400 = _141398, ca_Cx1xcomp(_141400)], (206 ^ _135354) ^ [_141721, _141723, _141725, _141727] : [-(ra_Px1(_141725, _141721)), ra_Px1(_141727, _141723), _141727 = _141725, _141723 = _141721], (220 ^ _135354) ^ [_142137, _142139] : [-(cp3xcomp(_142137)), _142139 = _142137, cp3xcomp(_142139)], (230 ^ _135354) ^ [_142432, _142434] : [-(ca_Cx2(_142432)), _142434 = _142432, ca_Cx2(_142434)], (240 ^ _135354) ^ [_142727, _142729] : [-(ca_Cx2xcomp(_142727)), _142729 = _142727, ca_Cx2xcomp(_142729)], (250 ^ _135354) ^ [_143050, _143052, _143054, _143056] : [-(ra_Px2(_143054, _143050)), ra_Px2(_143056, _143052), _143056 = _143054, _143052 = _143050], (264 ^ _135354) ^ [_143466, _143468] : [-(ca_Cx3(_143466)), _143468 = _143466, ca_Cx3(_143468)], (274 ^ _135354) ^ [_143761, _143763] : [-(cp5xcomp(_143761)), _143763 = _143761, cp5xcomp(_143763)], (284 ^ _135354) ^ [_144056, _144058] : [-(cp4xcomp(_144056)), _144058 = _144056, cp4xcomp(_144058)], (294 ^ _135354) ^ [_144351, _144353] : [-(ca_Cx3xcomp(_144351)), _144353 = _144351, ca_Cx3xcomp(_144353)], (304 ^ _135354) ^ [_144674, _144676, _144678, _144680] : [-(ra_Px3(_144678, _144674)), ra_Px3(_144680, _144676), _144680 = _144678, _144676 = _144674], (318 ^ _135354) ^ [_145118, _145120, _145122, _145124] : [-(rinvR(_145122, _145118)), rinvR(_145124, _145120), _145124 = _145122, _145120 = _145118], (346 ^ _135354) ^ [_145958, _145960] : [-(cUnsatisfiable(_145958)), _145960 = _145958, cUnsatisfiable(_145960)], (332 ^ _135354) ^ [_145562, _145564, _145566, _145568] : [-(rr(_145566, _145562)), rr(_145568, _145564), _145568 = _145566, _145564 = _145562], (356 ^ _135354) ^ [_146397, _146399] : [-(cUnsatisfiable(_146397)), _146399 = _146397, cUnsatisfiable(_146399)], (366 ^ _135354) ^ [_146692, _146694] : [-(ca_Ax14(_146692)), _146694 = _146692, ca_Ax14(_146694)], (376 ^ _135354) ^ [_146987, _146989] : [-(ca_Cx1(_146987)), _146989 = _146987, ca_Cx1(_146989)], (386 ^ _135354) ^ [_147282, _147284] : [-(ca_Cx1xcomp(_147282)), _147284 = _147282, ca_Cx1xcomp(_147284)], (396 ^ _135354) ^ [_147577, _147579] : [-(ca_Cx2(_147577)), _147579 = _147577, ca_Cx2(_147579)], (406 ^ _135354) ^ [_147872, _147874] : [-(ca_Cx2xcomp(_147872)), _147874 = _147872, ca_Cx2xcomp(_147874)], (416 ^ _135354) ^ [_148167, _148169] : [-(ca_Cx3(_148167)), _148169 = _148167, ca_Cx3(_148169)], (426 ^ _135354) ^ [_148462, _148464] : [-(ca_Cx3xcomp(_148462)), _148464 = _148462, ca_Cx3xcomp(_148464)], (436 ^ _135354) ^ [_148757, _148759] : [-(cowlNothing(_148757)), _148759 = _148757, cowlNothing(_148759)], (446 ^ _135354) ^ [_149052, _149054] : [-(cowlThing(_149052)), _149054 = _149052, cowlThing(_149054)], (456 ^ _135354) ^ [_149347, _149349] : [-(cp1(_149347)), _149349 = _149347, cp1(_149349)], (466 ^ _135354) ^ [_149642, _149644] : [-(cp2(_149642)), _149644 = _149642, cp2(_149644)], (476 ^ _135354) ^ [_149937, _149939] : [-(cp2xcomp(_149937)), _149939 = _149937, cp2xcomp(_149939)], (486 ^ _135354) ^ [_150232, _150234] : [-(cp3(_150232)), _150234 = _150232, cp3(_150234)], (496 ^ _135354) ^ [_150527, _150529] : [-(cp3xcomp(_150527)), _150529 = _150527, cp3xcomp(_150529)], (506 ^ _135354) ^ [_150822, _150824] : [-(cp4(_150822)), _150824 = _150822, cp4(_150824)], (516 ^ _135354) ^ [_151117, _151119] : [-(cp4xcomp(_151117)), _151119 = _151117, cp4xcomp(_151119)], (526 ^ _135354) ^ [_151412, _151414] : [-(cp5(_151412)), _151414 = _151412, cp5(_151414)], (536 ^ _135354) ^ [_151707, _151709] : [-(cp5xcomp(_151707)), _151709 = _151707, cp5xcomp(_151709)], (546 ^ _135354) ^ [_152016, _152018, _152020] : [-(ra_Px1(_152018, _152016)), _152020 = _152018, ra_Px1(_152020, _152016)], (556 ^ _135354) ^ [_152339, _152341, _152343] : [-(ra_Px1(_152339, _152341)), _152343 = _152341, ra_Px1(_152339, _152343)], (566 ^ _135354) ^ [_152662, _152664, _152666] : [-(ra_Px2(_152664, _152662)), _152666 = _152664, ra_Px2(_152666, _152662)], (576 ^ _135354) ^ [_152985, _152987, _152989] : [-(ra_Px2(_152985, _152987)), _152989 = _152987, ra_Px2(_152985, _152989)], (586 ^ _135354) ^ [_153308, _153310, _153312] : [-(ra_Px3(_153310, _153308)), _153312 = _153310, ra_Px3(_153312, _153308)], (596 ^ _135354) ^ [_153631, _153633, _153635] : [-(ra_Px3(_153631, _153633)), _153635 = _153633, ra_Px3(_153631, _153635)], (606 ^ _135354) ^ [_153954, _153956, _153958] : [-(ra_Px4(_153956, _153954)), _153958 = _153956, ra_Px4(_153958, _153954)], (616 ^ _135354) ^ [_154277, _154279, _154281] : [-(ra_Px4(_154277, _154279)), _154281 = _154279, ra_Px4(_154277, _154281)], (626 ^ _135354) ^ [_154600, _154602, _154604] : [-(ra_Px5(_154602, _154600)), _154604 = _154602, ra_Px5(_154604, _154600)], (636 ^ _135354) ^ [_154923, _154925, _154927] : [-(ra_Px5(_154923, _154925)), _154927 = _154925, ra_Px5(_154923, _154927)], (646 ^ _135354) ^ [_155246, _155248, _155250] : [-(ra_Px6(_155248, _155246)), _155250 = _155248, ra_Px6(_155250, _155246)], (656 ^ _135354) ^ [_155569, _155571, _155573] : [-(ra_Px6(_155569, _155571)), _155573 = _155571, ra_Px6(_155569, _155573)], (666 ^ _135354) ^ [_155892, _155894, _155896] : [-(ra_Px7(_155894, _155892)), _155896 = _155894, ra_Px7(_155896, _155892)], (676 ^ _135354) ^ [_156215, _156217, _156219] : [-(ra_Px7(_156215, _156217)), _156219 = _156217, ra_Px7(_156215, _156219)], (686 ^ _135354) ^ [_156538, _156540, _156542] : [-(rinvR(_156540, _156538)), _156542 = _156540, rinvR(_156542, _156538)], (696 ^ _135354) ^ [_156861, _156863, _156865] : [-(rinvR(_156861, _156863)), _156865 = _156863, rinvR(_156861, _156865)], (706 ^ _135354) ^ [_157184, _157186, _157188] : [-(rr(_157186, _157184)), _157188 = _157186, rr(_157188, _157184)], (716 ^ _135354) ^ [_157507, _157509, _157511] : [-(rr(_157507, _157509)), _157511 = _157509, rr(_157507, _157511)], (726 ^ _135354) ^ [_157816, _157818] : [-(xsd_integer(_157816)), _157818 = _157816, xsd_integer(_157818)], (736 ^ _135354) ^ [_158111, _158113] : [-(xsd_string(_158111)), _158113 = _158111, xsd_string(_158113)], (746 ^ _135354) ^ [_158397] : [-(cowlThing(_158397))], (748 ^ _135354) ^ [_158439] : [cowlNothing(_158439)], (750 ^ _135354) ^ [_158562] : [xsd_string(_158562), xsd_integer(_158562)], (756 ^ _135354) ^ [_158715] : [-(xsd_integer(_158715)), -(xsd_string(_158715))], (762 ^ _135354) ^ [_158935] : [cUnsatisfiable(_158935), 766 ^ _135354 : [(767 ^ _135354) ^ [] : [-(rinvR(_158935, 765 ^ [_158935]))], (769 ^ _135354) ^ [] : [-(ca_Ax14(765 ^ [_158935]))], (771 ^ _135354) ^ [] : [-(cp2(_158935))]]], (773 ^ _135354) ^ [_159293] : [-(cUnsatisfiable(_159293)), cp2(_159293), 776 ^ _135354 : [(777 ^ _135354) ^ [_159418] : [rinvR(_159293, _159418), ca_Ax14(_159418)]]], (787 ^ _135354) ^ [_159709] : [cp1(_159709), -(ca_Cx1(_159709))], (793 ^ _135354) ^ [_159924] : [cp2(_159924), -(ra_Px5(_159924, 796 ^ [_159924]))], (800 ^ _135354) ^ [_160129] : [801 ^ _135354 : [(802 ^ _135354) ^ [_160196] : [ra_Px5(_160129, _160196)]], -(cp2(_160129))], (806 ^ _135354) ^ [_160341] : [cp2(_160341), -(ca_Cx2(_160341))], (812 ^ _135354) ^ [_160556] : [cp2xcomp(_160556), 815 ^ _135354 : [(816 ^ _135354) ^ [_160667] : [ra_Px5(_160556, _160667)]]], (818 ^ _135354) ^ [_160733] : [-(ra_Px5(_160733, 819 ^ [_160733])), -(cp2xcomp(_160733))], (825 ^ _135354) ^ [_161006] : [cp3(_161006), -(ra_Px6(_161006, 828 ^ [_161006]))], (832 ^ _135354) ^ [_161211] : [833 ^ _135354 : [(834 ^ _135354) ^ [_161278] : [ra_Px6(_161211, _161278)]], -(cp3(_161211))], (838 ^ _135354) ^ [_161423] : [cp3(_161423), -(ca_Cx3(_161423))], (844 ^ _135354) ^ [_161638] : [cp3xcomp(_161638), 847 ^ _135354 : [(848 ^ _135354) ^ [_161749] : [ra_Px6(_161638, _161749)]]], (850 ^ _135354) ^ [_161815] : [-(ra_Px6(_161815, 851 ^ [_161815])), -(cp3xcomp(_161815))], (857 ^ _135354) ^ [_162088] : [cp4(_162088), 860 ^ _135354 : [(861 ^ _135354) ^ [_162199] : [ra_Px7(_162088, _162199)]]], (863 ^ _135354) ^ [_162265] : [-(ra_Px7(_162265, 864 ^ [_162265])), -(cp4(_162265))], (870 ^ _135354) ^ [_162509] : [cp4(_162509), -(cp5xcomp(_162509))], (876 ^ _135354) ^ [_162724] : [cp4xcomp(_162724), -(ra_Px7(_162724, 879 ^ [_162724]))], (883 ^ _135354) ^ [_162929] : [884 ^ _135354 : [(885 ^ _135354) ^ [_162996] : [ra_Px7(_162929, _162996)]], -(cp4xcomp(_162929))], (889 ^ _135354) ^ [_163170] : [cp5(_163170), 892 ^ _135354 : [(893 ^ _135354) ^ [_163281] : [ra_Px4(_163170, _163281)]]], (895 ^ _135354) ^ [_163347] : [-(ra_Px4(_163347, 896 ^ [_163347])), -(cp5(_163347))], (902 ^ _135354) ^ [_163620] : [cp5xcomp(_163620), -(ra_Px4(_163620, 905 ^ [_163620]))], (909 ^ _135354) ^ [_163825] : [910 ^ _135354 : [(911 ^ _135354) ^ [_163892] : [ra_Px4(_163825, _163892)]], -(cp5xcomp(_163825))], (915 ^ _135354) ^ [_164066] : [ca_Ax14(_164066), 919 ^ _135354 : [(920 ^ _135354) ^ [] : [-(rr(_164066, 918 ^ [_164066]))], (922 ^ _135354) ^ [] : [-(cp1(918 ^ [_164066]))], (924 ^ _135354) ^ [_164423, _164425] : [-(_164425 = _164423), rr(_164066, _164425), rr(_164066, _164423)]]], (934 ^ _135354) ^ [_164695] : [-(ca_Ax14(_164695)), 945 ^ _135354 : [(946 ^ _135354) ^ [] : [-(rr(_164695, 943 ^ [_164695]))], (948 ^ _135354) ^ [] : [-(rr(_164695, 944 ^ [_164695]))], (950 ^ _135354) ^ [] : [943 ^ [_164695] = 944 ^ [_164695]]], 937 ^ _135354 : [(938 ^ _135354) ^ [_164843] : [rr(_164695, _164843), cp1(_164843)]]], (954 ^ _135354) ^ [_165440] : [ca_Cx1(_165440), 957 ^ _135354 : [(958 ^ _135354) ^ [] : [-(cp2xcomp(_165440))], (960 ^ _135354) ^ [] : [-(cp5xcomp(_165440))], (962 ^ _135354) ^ [] : [-(cp3xcomp(_165440))], (964 ^ _135354) ^ [] : [-(cp4xcomp(_165440))]]], (966 ^ _135354) ^ [_165803] : [-(ca_Cx1(_165803)), cp2xcomp(_165803), cp5xcomp(_165803), cp3xcomp(_165803), cp4xcomp(_165803)], (984 ^ _135354) ^ [_166269] : [ca_Cx1(_166269), -(ra_Px1(_166269, 987 ^ [_166269]))], (991 ^ _135354) ^ [_166474] : [992 ^ _135354 : [(993 ^ _135354) ^ [_166541] : [ra_Px1(_166474, _166541)]], -(ca_Cx1(_166474))], (997 ^ _135354) ^ [_166715] : [ca_Cx1xcomp(_166715), 1000 ^ _135354 : [(1001 ^ _135354) ^ [_166826] : [ra_Px1(_166715, _166826)]]], (1003 ^ _135354) ^ [_166892] : [-(ra_Px1(_166892, 1004 ^ [_166892])), -(ca_Cx1xcomp(_166892))], (1010 ^ _135354) ^ [_167165] : [ca_Cx2(_167165), 1013 ^ _135354 : [(1014 ^ _135354) ^ [] : [-(cp5xcomp(_167165))], (1016 ^ _135354) ^ [] : [-(cp3xcomp(_167165))], (1018 ^ _135354) ^ [] : [-(cp4xcomp(_167165))]]], (1020 ^ _135354) ^ [_167458] : [-(ca_Cx2(_167458)), cp5xcomp(_167458), cp3xcomp(_167458), cp4xcomp(_167458)], (1034 ^ _135354) ^ [_167841] : [ca_Cx2(_167841), 1037 ^ _135354 : [(1038 ^ _135354) ^ [_167952] : [ra_Px2(_167841, _167952)]]], (1040 ^ _135354) ^ [_168018] : [-(ra_Px2(_168018, 1041 ^ [_168018])), -(ca_Cx2(_168018))], (1047 ^ _135354) ^ [_168291] : [ca_Cx2xcomp(_168291), -(ra_Px2(_168291, 1050 ^ [_168291]))], (1054 ^ _135354) ^ [_168496] : [1055 ^ _135354 : [(1056 ^ _135354) ^ [_168563] : [ra_Px2(_168496, _168563)]], -(ca_Cx2xcomp(_168496))], (1060 ^ _135354) ^ [_168737] : [ca_Cx3(_168737), 1063 ^ _135354 : [(1064 ^ _135354) ^ [_168848] : [ra_Px3(_168737, _168848)]]], (1066 ^ _135354) ^ [_168914] : [-(ra_Px3(_168914, 1067 ^ [_168914])), -(ca_Cx3(_168914))], (1073 ^ _135354) ^ [_169187] : [ca_Cx3(_169187), 1076 ^ _135354 : [(1077 ^ _135354) ^ [] : [-(cp5xcomp(_169187))], (1079 ^ _135354) ^ [] : [-(cp4xcomp(_169187))]]], (1081 ^ _135354) ^ [_169410] : [-(ca_Cx3(_169410)), cp5xcomp(_169410), cp4xcomp(_169410)], (1091 ^ _135354) ^ [_169710] : [ca_Cx3xcomp(_169710), -(ra_Px3(_169710, 1094 ^ [_169710]))], (1098 ^ _135354) ^ [_169915] : [1099 ^ _135354 : [(1100 ^ _135354) ^ [_169982] : [ra_Px3(_169915, _169982)]], -(ca_Cx3xcomp(_169915))], (1116 ^ _135354) ^ [] : [-(cUnsatisfiable(i2003_11_14_17_21_04740))], (1104 ^ _135354) ^ [_170170, _170172] : [rinvR(_170172, _170170), -(rr(_170170, _170172))], (1110 ^ _135354) ^ [_170332, _170334] : [rr(_170332, _170334), -(rinvR(_170334, _170332))]], input).
% 0.36/1.37 ncf('1',plain,[cp2xcomp(918 ^ [765 ^ [i2003_11_14_17_21_04740]]), 816 : ra_Px5(918 ^ [765 ^ [i2003_11_14_17_21_04740]], 796 ^ [i2003_11_14_17_21_04740])],start(812 ^ 0,bind([[_160556, _160667], [918 ^ [765 ^ [i2003_11_14_17_21_04740]], 796 ^ [i2003_11_14_17_21_04740]]]))).
% 0.36/1.37 ncf('1.1',plain,[-(cp2xcomp(918 ^ [765 ^ [i2003_11_14_17_21_04740]])), ca_Cx1(918 ^ [765 ^ [i2003_11_14_17_21_04740]])],extension(954 ^ 1,bind([[_165440], [918 ^ [765 ^ [i2003_11_14_17_21_04740]]]]))).
% 0.36/1.38 ncf('1.1.1',plain,[-(ca_Cx1(918 ^ [765 ^ [i2003_11_14_17_21_04740]])), cp1(918 ^ [765 ^ [i2003_11_14_17_21_04740]])],extension(787 ^ 2,bind([[_159709], [918 ^ [765 ^ [i2003_11_14_17_21_04740]]]]))).
% 0.36/1.38 ncf('1.1.1.1',plain,[-(cp1(918 ^ [765 ^ [i2003_11_14_17_21_04740]])), ca_Ax14(765 ^ [i2003_11_14_17_21_04740])],extension(915 ^ 3,bind([[_164066], [765 ^ [i2003_11_14_17_21_04740]]]))).
% 0.36/1.38 ncf('1.1.1.1.1',plain,[-(ca_Ax14(765 ^ [i2003_11_14_17_21_04740])), cUnsatisfiable(i2003_11_14_17_21_04740)],extension(762 ^ 4,bind([[_158935], [i2003_11_14_17_21_04740]]))).
% 0.36/1.38 ncf('1.1.1.1.1.1',plain,[-(cUnsatisfiable(i2003_11_14_17_21_04740))],extension(1116 ^ 5)).
% 0.36/1.38 ncf('1.2',plain,[-(ra_Px5(918 ^ [765 ^ [i2003_11_14_17_21_04740]], 796 ^ [i2003_11_14_17_21_04740])), ra_Px5(i2003_11_14_17_21_04740, 796 ^ [i2003_11_14_17_21_04740]), i2003_11_14_17_21_04740 = 918 ^ [765 ^ [i2003_11_14_17_21_04740]], 796 ^ [i2003_11_14_17_21_04740] = 796 ^ [i2003_11_14_17_21_04740]],extension(70 ^ 3,bind([[_137585, _137587, _137589, _137591], [796 ^ [i2003_11_14_17_21_04740], 796 ^ [i2003_11_14_17_21_04740], 918 ^ [765 ^ [i2003_11_14_17_21_04740]], i2003_11_14_17_21_04740]]))).
% 0.36/1.38 ncf('1.2.1',plain,[-(ra_Px5(i2003_11_14_17_21_04740, 796 ^ [i2003_11_14_17_21_04740])), ra_Px5(i2003_11_14_17_21_04740, 796 ^ [i2003_11_14_17_21_04740]), i2003_11_14_17_21_04740 = i2003_11_14_17_21_04740, 796 ^ [i2003_11_14_17_21_04740] = 796 ^ [i2003_11_14_17_21_04740]],extension(70 ^ 4,bind([[_137585, _137587, _137589, _137591], [796 ^ [i2003_11_14_17_21_04740], 796 ^ [i2003_11_14_17_21_04740], i2003_11_14_17_21_04740, i2003_11_14_17_21_04740]]))).
% 0.36/1.38 ncf('1.2.1.1',plain,[-(ra_Px5(i2003_11_14_17_21_04740, 796 ^ [i2003_11_14_17_21_04740])), cp2(i2003_11_14_17_21_04740)],extension(793 ^ 5,bind([[_159924], [i2003_11_14_17_21_04740]]))).
% 0.36/1.38 ncf('1.2.1.1.1',plain,[-(cp2(i2003_11_14_17_21_04740)), cUnsatisfiable(i2003_11_14_17_21_04740)],extension(762 ^ 6,bind([[_158935], [i2003_11_14_17_21_04740]]))).
% 0.36/1.38 ncf('1.2.1.1.1.1',plain,[-(cUnsatisfiable(i2003_11_14_17_21_04740))],extension(1116 ^ 7)).
% 0.36/1.38 ncf('1.2.1.2',plain,[-(i2003_11_14_17_21_04740 = i2003_11_14_17_21_04740)],extension(2 ^ 5,bind([[_135458], [i2003_11_14_17_21_04740]]))).
% 0.36/1.38 ncf('1.2.1.3',plain,[-(796 ^ [i2003_11_14_17_21_04740] = 796 ^ [i2003_11_14_17_21_04740])],extension(2 ^ 5,bind([[_135458], [796 ^ [i2003_11_14_17_21_04740]]]))).
% 0.36/1.38 ncf('1.2.2',plain,[-(i2003_11_14_17_21_04740 = 918 ^ [765 ^ [i2003_11_14_17_21_04740]]), 924 : rr(765 ^ [i2003_11_14_17_21_04740], i2003_11_14_17_21_04740), 924 : rr(765 ^ [i2003_11_14_17_21_04740], 918 ^ [765 ^ [i2003_11_14_17_21_04740]]), 924 : ca_Ax14(765 ^ [i2003_11_14_17_21_04740])],extension(915 ^ 4,bind([[_164066, _164423, _164425], [765 ^ [i2003_11_14_17_21_04740], 918 ^ [765 ^ [i2003_11_14_17_21_04740]], i2003_11_14_17_21_04740]]))).
% 0.36/1.38 ncf('1.2.2.1',plain,[-(rr(765 ^ [i2003_11_14_17_21_04740], i2003_11_14_17_21_04740)), rinvR(i2003_11_14_17_21_04740, 765 ^ [i2003_11_14_17_21_04740])],extension(1104 ^ 7,bind([[_170170, _170172], [765 ^ [i2003_11_14_17_21_04740], i2003_11_14_17_21_04740]]))).
% 0.36/1.38 ncf('1.2.2.1.1',plain,[-(rinvR(i2003_11_14_17_21_04740, 765 ^ [i2003_11_14_17_21_04740])), cUnsatisfiable(i2003_11_14_17_21_04740)],extension(762 ^ 8,bind([[_158935], [i2003_11_14_17_21_04740]]))).
% 0.36/1.38 ncf('1.2.2.1.1.1',plain,[-(cUnsatisfiable(i2003_11_14_17_21_04740))],extension(1116 ^ 9)).
% 0.36/1.38 ncf('1.2.2.2',plain,[-(rr(765 ^ [i2003_11_14_17_21_04740], 918 ^ [765 ^ [i2003_11_14_17_21_04740]])), rr(765 ^ [i2003_11_14_17_21_04740], 918 ^ [765 ^ [i2003_11_14_17_21_04740]]), 765 ^ [i2003_11_14_17_21_04740] = 765 ^ [i2003_11_14_17_21_04740], 918 ^ [765 ^ [i2003_11_14_17_21_04740]] = 918 ^ [765 ^ [i2003_11_14_17_21_04740]]],extension(332 ^ 7,bind([[_145562, _145564, _145566, _145568], [918 ^ [765 ^ [i2003_11_14_17_21_04740]], 918 ^ [765 ^ [i2003_11_14_17_21_04740]], 765 ^ [i2003_11_14_17_21_04740], 765 ^ [i2003_11_14_17_21_04740]]]))).
% 0.36/1.38 ncf('1.2.2.2.1',plain,[-(rr(765 ^ [i2003_11_14_17_21_04740], 918 ^ [765 ^ [i2003_11_14_17_21_04740]]))],extension(920 ^ 8)).
% 0.36/1.38 ncf('1.2.2.2.2',plain,[-(765 ^ [i2003_11_14_17_21_04740] = 765 ^ [i2003_11_14_17_21_04740])],extension(2 ^ 8,bind([[_135458], [765 ^ [i2003_11_14_17_21_04740]]]))).
% 0.36/1.38 ncf('1.2.2.2.3',plain,[-(918 ^ [765 ^ [i2003_11_14_17_21_04740]] = 918 ^ [765 ^ [i2003_11_14_17_21_04740]])],extension(2 ^ 8,bind([[_135458], [918 ^ [765 ^ [i2003_11_14_17_21_04740]]]]))).
% 0.36/1.38 ncf('1.2.2.3',plain,[-(ca_Ax14(765 ^ [i2003_11_14_17_21_04740])), cUnsatisfiable(i2003_11_14_17_21_04740)],extension(762 ^ 5,bind([[_158935], [i2003_11_14_17_21_04740]]))).
% 0.36/1.38 ncf('1.2.2.3.1',plain,[-(cUnsatisfiable(i2003_11_14_17_21_04740))],extension(1116 ^ 6)).
% 0.36/1.38 ncf('1.2.3',plain,[-(796 ^ [i2003_11_14_17_21_04740] = 796 ^ [i2003_11_14_17_21_04740])],extension(2 ^ 4,bind([[_135458], [796 ^ [i2003_11_14_17_21_04740]]]))).
% 0.36/1.38 %-----------------------------------------------------
% 0.36/1.38 End of proof for negated /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------