%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : SYO604+1 : TPTP v8.1.2. Released v7.0.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n003.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:15 EDT 2023
% Result : Theorem 3.91s 4.48s
% Output : Proof 3.91s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : SYO604+1 : TPTP v8.1.2. Released v7.0.0.
% 0.03/0.13 % Command : nanocop.sh %s %d
% 0.13/0.34 % Computer : n003.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Thu May 18 18:43:30 EDT 2023
% 0.13/0.34 % CPUTime :
% 3.91/4.48
% 3.91/4.48 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 3.91/4.48 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 3.91/4.48 %-----------------------------------------------------
% 3.91/4.48 ncf(matrix, plain, [(2 ^ _88597) ^ [_88739, _88741] : [g_true_only(_88741, _88739), 5 ^ _88597 : [(6 ^ _88597) ^ [] : [-(g_true(_88741, _88739))], (8 ^ _88597) ^ [] : [g_false(_88741, _88739)]]], (10 ^ _88597) ^ [_88977, _88979] : [-(g_true_only(_88979, _88977)), g_true(_88979, _88977), -(g_false(_88979, _88977))], (20 ^ _88597) ^ [_89310, _89312] : [g_both(_89312, _89310), 23 ^ _88597 : [(24 ^ _88597) ^ [] : [-(g_true(_89312, _89310))], (26 ^ _88597) ^ [] : [-(g_false(_89312, _89310))]]], (28 ^ _88597) ^ [_89547, _89549] : [-(g_both(_89549, _89547)), g_true(_89549, _89547), g_false(_89549, _89547)], (56 ^ _88597) ^ [_90399, _90401] : [-(g_true_only(_90401, _90399)), -(g_both(_90401, _90399)), -(g_false_only(_90401, _90399))], (38 ^ _88597) ^ [_89877, _89879] : [g_false_only(_89879, _89877), 41 ^ _88597 : [(42 ^ _88597) ^ [] : [-(g_false(_89879, _89877))], (44 ^ _88597) ^ [] : [g_true(_89879, _89877)]]], (46 ^ _88597) ^ [_90115, _90117] : [-(g_false_only(_90117, _90115)), g_false(_90117, _90115), -(g_true(_90117, _90115))], (139 ^ _88597) ^ [] : [239 ^ _88597 : [(240 ^ _88597) ^ [_97133] : [249 ^ _88597 : [(250 ^ _88597) ^ [] : [-(g_false_only(_97133, 238 ^ []))], (253 ^ _88597) ^ [] : [-(g_true_only(_97133, 251 ^ [_97133]))], (255 ^ _88597) ^ [] : [-(g_true_only(251 ^ [_97133], _97133))]], 241 ^ _88597 : [(242 ^ _88597) ^ [] : [-(g_true_only(_97133, 238 ^ []))], (244 ^ _88597) ^ [_97310] : [-(g_false_only(_97133, _97310)), -(g_false_only(_97310, _97133))]]]], 140 ^ _88597 : [(141 ^ _88597) ^ [_93359] : [142 ^ _88597 : [(143 ^ _88597) ^ [_93686] : [g_both(_93686, _93359), 161 ^ _88597 : [(162 ^ _88597) ^ [] : [-(g_true_only(_93686, 160 ^ [_93359, _93686]))], (164 ^ _88597) ^ [] : [-(g_true_only(160 ^ [_93359, _93686], _93686))]], 148 ^ _88597 : [(149 ^ _88597) ^ [_93894] : [150 ^ _88597 : [(151 ^ _88597) ^ [] : [g_both(_93686, _93894)], (153 ^ _88597) ^ [] : [g_both(_93894, _93686)]], -(g_false_only(_93686, _93894)), -(g_false_only(_93894, _93686))]]]], 168 ^ _88597 : [(169 ^ _88597) ^ [] : [-(g_true_only(165 ^ [_93359], _93359))], (171 ^ _88597) ^ [] : [190 ^ _88597 : [(191 ^ _88597) ^ [] : [-(g_true_only(165 ^ [_93359], 189 ^ [_93359]))], (193 ^ _88597) ^ [] : [-(g_true_only(189 ^ [_93359], 165 ^ [_93359]))]], 173 ^ _88597 : [(180 ^ _88597) ^ [] : [g_false_only(165 ^ [_93359], 172 ^ [_93359])], (182 ^ _88597) ^ [] : [g_false_only(172 ^ [_93359], 165 ^ [_93359])], (174 ^ _88597) ^ [] : [-(g_both(165 ^ [_93359], 172 ^ [_93359])), -(g_both(172 ^ [_93359], 165 ^ [_93359]))], (184 ^ _88597) ^ [_95200] : [g_true_only(165 ^ [_93359], _95200), g_true_only(_95200, 165 ^ [_93359])]]]], 196 ^ _88597 : [(197 ^ _88597) ^ [] : [-(g_both(165 ^ [_93359], _93359))], (199 ^ _88597) ^ [] : [207 ^ _88597 : [(208 ^ _88597) ^ [] : [-(g_true_only(165 ^ [_93359], 206 ^ [_93359]))], (210 ^ _88597) ^ [] : [-(g_true_only(206 ^ [_93359], 165 ^ [_93359]))]], 200 ^ _88597 : [(201 ^ _88597) ^ [_95731] : [-(g_false_only(165 ^ [_93359], _95731)), -(g_false_only(_95731, 165 ^ [_93359]))]]]], 211 ^ _88597 : [(212 ^ _88597) ^ [] : [-(g_false_only(165 ^ [_93359], _93359))], (214 ^ _88597) ^ [] : [215 ^ _88597 : [(216 ^ _88597) ^ [_96226] : [-(g_false_only(165 ^ [_93359], _96226)), -(g_false_only(_96226, 165 ^ [_93359]))]], 222 ^ _88597 : [(229 ^ _88597) ^ [] : [g_false_only(165 ^ [_93359], 221 ^ [_93359])], (231 ^ _88597) ^ [] : [g_false_only(221 ^ [_93359], 165 ^ [_93359])], (223 ^ _88597) ^ [] : [-(g_both(165 ^ [_93359], 221 ^ [_93359])), -(g_both(221 ^ [_93359], 165 ^ [_93359]))], (233 ^ _88597) ^ [_96824] : [g_true_only(165 ^ [_93359], _96824), g_true_only(_96824, 165 ^ [_93359])]]]]]]], (67 ^ _88597) ^ [_90942] : [g_true_only(_90942, 65 ^ []), 70 ^ _88597 : [(90 ^ _88597) ^ [_91698] : [g_true_only(_90942, _91698), g_true_only(_91698, _90942)], (71 ^ _88597) ^ [] : [85 ^ _88597 : [(86 ^ _88597) ^ [] : [-(g_true_only(_90942, 84 ^ [_90942]))], (88 ^ _88597) ^ [] : [-(g_true_only(84 ^ [_90942], _90942))]], 72 ^ _88597 : [(73 ^ _88597) ^ [_91179] : [74 ^ _88597 : [(75 ^ _88597) ^ [] : [g_both(_90942, _91179)], (77 ^ _88597) ^ [] : [g_both(_91179, _90942)]], -(g_false_only(_90942, _91179)), -(g_false_only(_91179, _90942))]]]]], (96 ^ _88597) ^ [_91888] : [g_both(_91888, 65 ^ []), 100 ^ _88597 : [(101 ^ _88597) ^ [] : [g_false_only(_91888, 99 ^ [_91888])], (103 ^ _88597) ^ [] : [g_false_only(99 ^ [_91888], _91888)], (105 ^ _88597) ^ [_92223] : [g_true_only(_91888, _92223), g_true_only(_92223, _91888)]]], (111 ^ _88597) ^ [_92395] : [g_false_only(_92395, 65 ^ []), 115 ^ _88597 : [(116 ^ _88597) ^ [] : [g_false_only(_92395, 114 ^ [_92395])], (118 ^ _88597) ^ [] : [g_false_only(114 ^ [_92395], _92395)], (120 ^ _88597) ^ [] : [134 ^ _88597 : [(135 ^ _88597) ^ [] : [-(g_true_only(_92395, 133 ^ [_92395]))], (137 ^ _88597) ^ [] : [-(g_true_only(133 ^ [_92395], _92395))]], 121 ^ _88597 : [(122 ^ _88597) ^ [_92797] : [123 ^ _88597 : [(124 ^ _88597) ^ [] : [g_both(_92395, _92797)], (126 ^ _88597) ^ [] : [g_both(_92797, _92395)]], -(g_false_only(_92395, _92797)), -(g_false_only(_92797, _92395))]]]]]], input).
% 3.91/4.48 ncf('1',plain,[g_false_only(65 ^ [], 65 ^ []), 116 : g_false_only(65 ^ [], 114 ^ [65 ^ []])],start(111 ^ 0,bind([[_92395], [65 ^ []]]))).
% 3.91/4.48 ncf('1.1',plain,[-(g_false_only(65 ^ [], 65 ^ [])), -(g_true_only(65 ^ [], 65 ^ [])), -(g_both(65 ^ [], 65 ^ []))],extension(56 ^ 1,bind([[_90399, _90401], [65 ^ [], 65 ^ []]]))).
% 3.91/4.48 ncf('1.1.1',plain,[g_true_only(65 ^ [], 65 ^ []), 90 : g_true_only(65 ^ [], 65 ^ []), 90 : g_true_only(65 ^ [], 65 ^ [])],extension(67 ^ 2,bind([[_90942, _91698], [65 ^ [], 65 ^ []]]))).
% 3.91/4.48 ncf('1.1.1.1',plain,[-(g_true_only(65 ^ [], 65 ^ []))],reduction('1.1')).
% 3.91/4.48 ncf('1.1.1.2',plain,[-(g_true_only(65 ^ [], 65 ^ []))],reduction('1.1')).
% 3.91/4.48 ncf('1.1.2',plain,[g_both(65 ^ [], 65 ^ []), 162 : -(g_true_only(65 ^ [], 160 ^ [65 ^ [], 65 ^ []])), 151 : g_both(65 ^ [], 65 ^ []), 151 : -(g_false_only(65 ^ [], 65 ^ [])), 151 : -(g_false_only(65 ^ [], 65 ^ [])), 191 : -(g_true_only(165 ^ [65 ^ []], 189 ^ [65 ^ []])), 180 : g_false_only(165 ^ [65 ^ []], 172 ^ [65 ^ []]), 197 : -(g_both(165 ^ [65 ^ []], 65 ^ [])), 212 : -(g_false_only(165 ^ [65 ^ []], 65 ^ [])), 253 : -(g_true_only(251 ^ [65 ^ []], 251 ^ [251 ^ [65 ^ []]])), 244 : -(g_false_only(251 ^ [65 ^ []], 65 ^ [])), 244 : -(g_false_only(65 ^ [], 251 ^ [65 ^ []]))],extension(139 ^ 2,bind([[_93359, _93686, _93894, _97133, _97310], [65 ^ [], 65 ^ [], 65 ^ [], 251 ^ [65 ^ []], 65 ^ []]]))).
% 3.91/4.48 ncf('1.1.2.1',plain,[g_true_only(65 ^ [], 160 ^ [65 ^ [], 65 ^ []]), 90 : g_true_only(160 ^ [65 ^ [], 65 ^ []], 65 ^ []), 90 : g_true_only(160 ^ [65 ^ [], 65 ^ []], 65 ^ [])],extension(67 ^ 9,bind([[_90942, _91698], [160 ^ [65 ^ [], 65 ^ []], 65 ^ []]]))).
% 3.91/4.48 ncf('1.1.2.1.1',plain,[-(g_true_only(160 ^ [65 ^ [], 65 ^ []], 65 ^ []))],extension(164 ^ 12)).
% 3.91/4.48 ncf('1.1.2.1.2',plain,[-(g_true_only(160 ^ [65 ^ [], 65 ^ []], 65 ^ []))],extension(164 ^ 10)).
% 3.91/4.48 ncf('1.1.2.2',plain,[-(g_both(65 ^ [], 65 ^ []))],reduction('1.1')).
% 3.91/4.48 ncf('1.1.2.3',plain,[g_false_only(65 ^ [], 65 ^ [])],reduction('1')).
% 3.91/4.48 ncf('1.1.2.4',plain,[g_false_only(65 ^ [], 65 ^ [])],lemmata('[1, 1].x')).
% 3.91/4.48 ncf('1.1.2.5',plain,[g_true_only(165 ^ [65 ^ []], 189 ^ [65 ^ []]), 90 : g_true_only(189 ^ [65 ^ []], 165 ^ [65 ^ []]), 90 : g_true_only(165 ^ [65 ^ []], 65 ^ [])],extension(67 ^ 9,bind([[_90942, _91698], [165 ^ [65 ^ []], 189 ^ [65 ^ []]]]))).
% 3.91/4.48 ncf('1.1.2.5.1',plain,[-(g_true_only(189 ^ [65 ^ []], 165 ^ [65 ^ []]))],extension(193 ^ 12)).
% 3.91/4.48 ncf('1.1.2.5.2',plain,[-(g_true_only(165 ^ [65 ^ []], 65 ^ []))],extension(169 ^ 10)).
% 3.91/4.48 ncf('1.1.2.6',plain,[-(g_false_only(165 ^ [65 ^ []], 172 ^ [65 ^ []])), 75 : g_both(165 ^ [65 ^ []], 172 ^ [65 ^ []]), 75 : -(g_false_only(172 ^ [65 ^ []], 165 ^ [65 ^ []])), 86 : -(g_true_only(165 ^ [65 ^ []], 84 ^ [165 ^ [65 ^ []]])), 71 : g_true_only(165 ^ [65 ^ []], 65 ^ [])],extension(67 ^ 9,bind([[_90942, _91179], [165 ^ [65 ^ []], 172 ^ [65 ^ []]]]))).
% 3.91/4.48 ncf('1.1.2.6.1',plain,[-(g_both(165 ^ [65 ^ []], 172 ^ [65 ^ []])), -(g_both(172 ^ [65 ^ []], 165 ^ [65 ^ []]))],extension(174 ^ 16)).
% 3.91/4.48 ncf('1.1.2.6.1.1',plain,[g_both(172 ^ [65 ^ []], 165 ^ [65 ^ []])],extension(77 ^ 17)).
% 3.91/4.48 ncf('1.1.2.6.2',plain,[g_false_only(172 ^ [65 ^ []], 165 ^ [65 ^ []])],extension(182 ^ 14)).
% 3.91/4.48 ncf('1.1.2.6.3',plain,[g_true_only(165 ^ [65 ^ []], 84 ^ [165 ^ [65 ^ []]]), g_true_only(84 ^ [165 ^ [65 ^ []]], 165 ^ [65 ^ []])],extension(184 ^ 14,bind([[_95200], [84 ^ [165 ^ [65 ^ []]]]]))).
% 3.91/4.48 ncf('1.1.2.6.3.1',plain,[-(g_true_only(84 ^ [165 ^ [65 ^ []]], 165 ^ [65 ^ []]))],extension(88 ^ 15)).
% 3.91/4.48 ncf('1.1.2.6.4',plain,[-(g_true_only(165 ^ [65 ^ []], 65 ^ []))],extension(169 ^ 10)).
% 3.91/4.48 ncf('1.1.2.7',plain,[g_both(165 ^ [65 ^ []], 65 ^ []), 105 : g_true_only(165 ^ [65 ^ []], 206 ^ [65 ^ []]), 105 : g_true_only(206 ^ [65 ^ []], 165 ^ [65 ^ []])],extension(96 ^ 7,bind([[_91888, _92223], [165 ^ [65 ^ []], 206 ^ [65 ^ []]]]))).
% 3.91/4.48 ncf('1.1.2.7.1',plain,[-(g_true_only(165 ^ [65 ^ []], 206 ^ [65 ^ []])), 201 : -(g_false_only(165 ^ [65 ^ []], 99 ^ [165 ^ [65 ^ []]])), 201 : -(g_false_only(99 ^ [165 ^ [65 ^ []]], 165 ^ [65 ^ []]))],extension(199 ^ 10,bind([[_95731], [99 ^ [165 ^ [65 ^ []]]]]))).
% 3.91/4.48 ncf('1.1.2.7.1.1',plain,[g_false_only(165 ^ [65 ^ []], 99 ^ [165 ^ [65 ^ []]])],extension(101 ^ 13)).
% 3.91/4.48 ncf('1.1.2.7.1.2',plain,[g_false_only(99 ^ [165 ^ [65 ^ []]], 165 ^ [65 ^ []])],extension(103 ^ 13)).
% 3.91/4.48 ncf('1.1.2.7.2',plain,[-(g_true_only(206 ^ [65 ^ []], 165 ^ [65 ^ []])), 201 : -(g_false_only(165 ^ [65 ^ []], 99 ^ [165 ^ [65 ^ []]])), 201 : -(g_false_only(99 ^ [165 ^ [65 ^ []]], 165 ^ [65 ^ []]))],extension(199 ^ 10,bind([[_95731], [99 ^ [165 ^ [65 ^ []]]]]))).
% 3.91/4.48 ncf('1.1.2.7.2.1',plain,[g_false_only(165 ^ [65 ^ []], 99 ^ [165 ^ [65 ^ []]])],extension(101 ^ 13)).
% 3.91/4.48 ncf('1.1.2.7.2.2',plain,[g_false_only(99 ^ [165 ^ [65 ^ []]], 165 ^ [65 ^ []])],extension(103 ^ 13)).
% 3.91/4.48 ncf('1.1.2.8',plain,[g_false_only(165 ^ [65 ^ []], 65 ^ []), 135 : -(g_true_only(165 ^ [65 ^ []], 133 ^ [165 ^ [65 ^ []]])), 124 : g_both(165 ^ [65 ^ []], 221 ^ [65 ^ []]), 124 : -(g_false_only(165 ^ [65 ^ []], 221 ^ [65 ^ []])), 124 : -(g_false_only(221 ^ [65 ^ []], 165 ^ [65 ^ []]))],extension(111 ^ 7,bind([[_92395, _92797], [165 ^ [65 ^ []], 221 ^ [65 ^ []]]]))).
% 3.91/4.48 ncf('1.1.2.8.1',plain,[g_true_only(165 ^ [65 ^ []], 133 ^ [165 ^ [65 ^ []]]), 233 : g_true_only(133 ^ [165 ^ [65 ^ []]], 165 ^ [65 ^ []]), 216 : -(g_false_only(165 ^ [65 ^ []], 114 ^ [165 ^ [65 ^ []]])), 216 : -(g_false_only(114 ^ [165 ^ [65 ^ []]], 165 ^ [65 ^ []]))],extension(214 ^ 12,bind([[_96824, _96226], [133 ^ [165 ^ [65 ^ []]], 114 ^ [165 ^ [65 ^ []]]]]))).
% 3.91/4.48 ncf('1.1.2.8.1.1',plain,[-(g_true_only(133 ^ [165 ^ [65 ^ []]], 165 ^ [65 ^ []]))],extension(137 ^ 15)).
% 3.91/4.48 ncf('1.1.2.8.1.2',plain,[g_false_only(165 ^ [65 ^ []], 114 ^ [165 ^ [65 ^ []]])],extension(116 ^ 15)).
% 3.91/4.48 ncf('1.1.2.8.1.3',plain,[g_false_only(114 ^ [165 ^ [65 ^ []]], 165 ^ [65 ^ []])],extension(118 ^ 15)).
% 3.91/4.48 ncf('1.1.2.8.2',plain,[-(g_both(165 ^ [65 ^ []], 221 ^ [65 ^ []])), 223 : -(g_both(221 ^ [65 ^ []], 165 ^ [65 ^ []])), 216 : -(g_false_only(165 ^ [65 ^ []], 114 ^ [165 ^ [65 ^ []]])), 216 : -(g_false_only(114 ^ [165 ^ [65 ^ []]], 165 ^ [65 ^ []]))],extension(214 ^ 14,bind([[_96226], [114 ^ [165 ^ [65 ^ []]]]]))).
% 3.91/4.48 ncf('1.1.2.8.2.1',plain,[g_both(221 ^ [65 ^ []], 165 ^ [65 ^ []])],extension(126 ^ 17)).
% 3.91/4.48 ncf('1.1.2.8.2.2',plain,[g_false_only(165 ^ [65 ^ []], 114 ^ [165 ^ [65 ^ []]])],extension(116 ^ 17)).
% 3.91/4.48 ncf('1.1.2.8.2.3',plain,[g_false_only(114 ^ [165 ^ [65 ^ []]], 165 ^ [65 ^ []])],extension(118 ^ 17)).
% 3.91/4.48 ncf('1.1.2.8.3',plain,[g_false_only(165 ^ [65 ^ []], 221 ^ [65 ^ []]), 216 : -(g_false_only(165 ^ [65 ^ []], 114 ^ [165 ^ [65 ^ []]])), 216 : -(g_false_only(114 ^ [165 ^ [65 ^ []]], 165 ^ [65 ^ []]))],extension(214 ^ 12,bind([[_96226], [114 ^ [165 ^ [65 ^ []]]]]))).
% 3.91/4.48 ncf('1.1.2.8.3.1',plain,[g_false_only(165 ^ [65 ^ []], 114 ^ [165 ^ [65 ^ []]])],extension(116 ^ 15)).
% 3.91/4.48 ncf('1.1.2.8.3.2',plain,[g_false_only(114 ^ [165 ^ [65 ^ []]], 165 ^ [65 ^ []])],extension(118 ^ 15)).
% 3.91/4.48 ncf('1.1.2.8.4',plain,[g_false_only(221 ^ [65 ^ []], 165 ^ [65 ^ []]), 216 : -(g_false_only(165 ^ [65 ^ []], 114 ^ [165 ^ [65 ^ []]])), 216 : -(g_false_only(114 ^ [165 ^ [65 ^ []]], 165 ^ [65 ^ []]))],extension(214 ^ 12,bind([[_96226], [114 ^ [165 ^ [65 ^ []]]]]))).
% 3.91/4.48 ncf('1.1.2.8.4.1',plain,[g_false_only(165 ^ [65 ^ []], 114 ^ [165 ^ [65 ^ []]])],extension(116 ^ 15)).
% 3.91/4.48 ncf('1.1.2.8.4.2',plain,[g_false_only(114 ^ [165 ^ [65 ^ []]], 165 ^ [65 ^ []])],extension(118 ^ 15)).
% 3.91/4.48 ncf('1.1.2.9',plain,[g_true_only(251 ^ [65 ^ []], 251 ^ [251 ^ [65 ^ []]]), 90 : g_true_only(251 ^ [251 ^ [65 ^ []]], 251 ^ [65 ^ []]), 90 : g_true_only(251 ^ [65 ^ []], 65 ^ [])],extension(67 ^ 7,bind([[_90942, _91698], [251 ^ [65 ^ []], 251 ^ [251 ^ [65 ^ []]]]]))).
% 3.91/4.48 ncf('1.1.2.9.1',plain,[-(g_true_only(251 ^ [251 ^ [65 ^ []]], 251 ^ [65 ^ []]))],extension(255 ^ 10)).
% 3.91/4.48 ncf('1.1.2.9.2',plain,[-(g_true_only(251 ^ [65 ^ []], 65 ^ [])), 244 : -(g_false_only(65 ^ [], 65 ^ [])), 244 : -(g_false_only(65 ^ [], 65 ^ []))],extension(240 ^ 8,bind([[_97133, _97310], [65 ^ [], 65 ^ []]]))).
% 3.91/4.48 ncf('1.1.2.9.2.1',plain,[g_false_only(65 ^ [], 65 ^ [])],reduction('1')).
% 3.91/4.48 ncf('1.1.2.9.2.2',plain,[g_false_only(65 ^ [], 65 ^ [])],lemmata('[9, 2, 1, 1].x')).
% 3.91/4.48 ncf('1.1.2.10',plain,[g_false_only(251 ^ [65 ^ []], 65 ^ []), 42 : -(g_false(251 ^ [65 ^ []], 65 ^ []))],extension(38 ^ 7,bind([[_89877, _89879], [65 ^ [], 251 ^ [65 ^ []]]]))).
% 3.91/4.48 ncf('1.1.2.10.1',plain,[g_false(251 ^ [65 ^ []], 65 ^ []), g_true_only(251 ^ [65 ^ []], 65 ^ [])],extension(2 ^ 10,bind([[_88739, _88741], [65 ^ [], 251 ^ [65 ^ []]]]))).
% 3.91/4.48 ncf('1.1.2.10.1.1',plain,[-(g_true_only(251 ^ [65 ^ []], 65 ^ [])), 244 : -(g_false_only(65 ^ [], 65 ^ [])), 244 : -(g_false_only(65 ^ [], 65 ^ []))],extension(240 ^ 11,bind([[_97133, _97310], [65 ^ [], 65 ^ []]]))).
% 3.91/4.48 ncf('1.1.2.10.1.1.1',plain,[g_false_only(65 ^ [], 65 ^ [])],reduction('1')).
% 3.91/4.48 ncf('1.1.2.10.1.1.2',plain,[g_false_only(65 ^ [], 65 ^ [])],lemmata('[1, 10, 2, 1, 1].x')).
% 3.91/4.48 ncf('1.1.2.11',plain,[g_false_only(65 ^ [], 251 ^ [65 ^ []]), 42 : -(g_false(65 ^ [], 251 ^ [65 ^ []]))],extension(38 ^ 7,bind([[_89877, _89879], [251 ^ [65 ^ []], 65 ^ []]]))).
% 3.91/4.48 ncf('1.1.2.11.1',plain,[g_false(65 ^ [], 251 ^ [65 ^ []]), g_true_only(65 ^ [], 251 ^ [65 ^ []])],extension(2 ^ 10,bind([[_88739, _88741], [251 ^ [65 ^ []], 65 ^ []]]))).
% 3.91/4.48 ncf('1.1.2.11.1.1',plain,[-(g_true_only(65 ^ [], 251 ^ [65 ^ []])), 244 : -(g_false_only(65 ^ [], 65 ^ [])), 244 : -(g_false_only(65 ^ [], 65 ^ []))],extension(240 ^ 11,bind([[_97133, _97310], [65 ^ [], 65 ^ []]]))).
% 3.91/4.48 ncf('1.1.2.11.1.1.1',plain,[g_false_only(65 ^ [], 65 ^ [])],reduction('1')).
% 3.91/4.48 ncf('1.1.2.11.1.1.2',plain,[g_false_only(65 ^ [], 65 ^ [])],lemmata('[1, 11, 2, 1, 1].x')).
% 3.91/4.48 ncf('1.2',plain,[-(g_false_only(65 ^ [], 114 ^ [65 ^ []])), 75 : g_both(114 ^ [65 ^ []], 65 ^ []), 75 : -(g_false_only(114 ^ [65 ^ []], 65 ^ [])), 86 : -(g_true_only(114 ^ [65 ^ []], 84 ^ [114 ^ [65 ^ []]])), 71 : g_true_only(114 ^ [65 ^ []], 65 ^ [])],extension(67 ^ 3,bind([[_90942, _91179], [114 ^ [65 ^ []], 65 ^ []]]))).
% 3.91/4.48 ncf('1.2.1',plain,[-(g_both(114 ^ [65 ^ []], 65 ^ [])), -(g_true_only(114 ^ [65 ^ []], 65 ^ [])), -(g_false_only(114 ^ [65 ^ []], 65 ^ []))],extension(56 ^ 10,bind([[_90399, _90401], [65 ^ [], 114 ^ [65 ^ []]]]))).
% 3.91/4.48 ncf('1.2.1.1',plain,[g_true_only(114 ^ [65 ^ []], 65 ^ []), g_true_only(65 ^ [], 114 ^ [65 ^ []])],extension(90 ^ 11,bind([[_91698], [65 ^ []]]))).
% 3.91/4.48 ncf('1.2.1.1.1',plain,[-(g_true_only(65 ^ [], 114 ^ [65 ^ []])), -(g_both(65 ^ [], 114 ^ [65 ^ []])), -(g_false_only(65 ^ [], 114 ^ [65 ^ []]))],extension(56 ^ 12,bind([[_90399, _90401], [114 ^ [65 ^ []], 65 ^ []]]))).
% 3.91/4.48 ncf('1.2.1.1.1.1',plain,[g_both(65 ^ [], 114 ^ [65 ^ []])],extension(77 ^ 13)).
% 3.91/4.48 ncf('1.2.1.1.1.2',plain,[g_false_only(65 ^ [], 114 ^ [65 ^ []])],reduction('1')).
% 3.91/4.48 ncf('1.2.1.2',plain,[g_false_only(114 ^ [65 ^ []], 65 ^ [])],extension(118 ^ 11)).
% 3.91/4.48 ncf('1.2.2',plain,[g_false_only(114 ^ [65 ^ []], 65 ^ [])],extension(118 ^ 8)).
% 3.91/4.48 ncf('1.2.3',plain,[g_true_only(114 ^ [65 ^ []], 84 ^ [114 ^ [65 ^ []]]), g_true_only(84 ^ [114 ^ [65 ^ []]], 114 ^ [65 ^ []])],extension(90 ^ 8,bind([[_91698], [84 ^ [114 ^ [65 ^ []]]]]))).
% 3.91/4.48 ncf('1.2.3.1',plain,[-(g_true_only(84 ^ [114 ^ [65 ^ []]], 114 ^ [65 ^ []]))],extension(88 ^ 9)).
% 3.91/4.48 ncf('1.2.4',plain,[-(g_true_only(114 ^ [65 ^ []], 65 ^ [])), -(g_both(114 ^ [65 ^ []], 65 ^ [])), -(g_false_only(114 ^ [65 ^ []], 65 ^ []))],extension(56 ^ 4,bind([[_90399, _90401], [65 ^ [], 114 ^ [65 ^ []]]]))).
% 3.91/4.48 ncf('1.2.4.1',plain,[g_both(114 ^ [65 ^ []], 65 ^ []), 122 : -(g_false_only(65 ^ [], 114 ^ [65 ^ []])), 122 : -(g_false_only(114 ^ [65 ^ []], 65 ^ [])), 135 : -(g_true_only(65 ^ [], 133 ^ [65 ^ []]))],extension(120 ^ 5,bind([[_92797], [114 ^ [65 ^ []]]]))).
% 3.91/4.48 ncf('1.2.4.1.1',plain,[g_false_only(65 ^ [], 114 ^ [65 ^ []])],reduction('1')).
% 3.91/4.48 ncf('1.2.4.1.2',plain,[g_false_only(114 ^ [65 ^ []], 65 ^ []), 44 : g_true(114 ^ [65 ^ []], 65 ^ [])],extension(38 ^ 8,bind([[_89877, _89879], [65 ^ [], 114 ^ [65 ^ []]]]))).
% 3.91/4.48 ncf('1.2.4.1.2.1',plain,[-(g_true(114 ^ [65 ^ []], 65 ^ [])), g_both(114 ^ [65 ^ []], 65 ^ [])],extension(20 ^ 11,bind([[_89310, _89312], [65 ^ [], 114 ^ [65 ^ []]]]))).
% 3.91/4.48 ncf('1.2.4.1.2.1.1',plain,[-(g_both(114 ^ [65 ^ []], 65 ^ []))],reduction('1.2.4')).
% 3.91/4.48 ncf('1.2.4.1.3',plain,[g_true_only(65 ^ [], 133 ^ [65 ^ []]), 90 : g_true_only(133 ^ [65 ^ []], 65 ^ []), 90 : g_true_only(133 ^ [65 ^ []], 65 ^ [])],extension(67 ^ 8,bind([[_90942, _91698], [133 ^ [65 ^ []], 65 ^ []]]))).
% 3.91/4.48 ncf('1.2.4.1.3.1',plain,[-(g_true_only(133 ^ [65 ^ []], 65 ^ []))],extension(137 ^ 11)).
% 3.91/4.48 ncf('1.2.4.1.3.2',plain,[-(g_true_only(133 ^ [65 ^ []], 65 ^ []))],extension(137 ^ 9)).
% 3.91/4.48 ncf('1.2.4.2',plain,[g_false_only(114 ^ [65 ^ []], 65 ^ [])],extension(118 ^ 5)).
% 3.91/4.48 %-----------------------------------------------------
% 3.91/4.48 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------