%------------------------------------------------------------------------------
% File : Gandalf---c-2.6
% Problem : PUZ016-2.005 : TPTP v3.4.2. Released v1.2.0.
% Transfm : add_equality:r
% Format : otter:hypothesis:set(auto),clear(print_given)
% Command : gandalf-wrapper -time %d %s
% Computer : art03.cs.miami.edu
% Model : i686 unknown
% CPU : Intel(R) Pentium(R) 4 CPU 2.80GHz @ 2793MHz
% Memory : 1000MB
% OS : Linux 2.4.22-21mdk-i686-up-4GB
% CPULimit : 600s
% Result : Unsatisfiable 0.0s
% Output : Assurance 0.0s
% Verified :
% SZS Type : None (Parsing solution fails)
% Syntax : Number of formulae : 0
% Comments :
%------------------------------------------------------------------------------
%----NO SOLUTION OUTPUT BY SYSTEM
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
%
% Gandalf c-2.6 r1 starting to prove: /home/graph/tptp/TSTP/PreparedTPTP/otter:hypothesis:set(auto),clear(print_given)---add_equality:r/PUZ/PUZ016-2.005+noeq.in
% Using automatic strategy selection.
% Time limit in seconds: 600
%
% prove-all-passes started
%
% detected problem class: nne
% detected subclass: big
%
% strategies selected:
% (hyper 30 #f 1 7)
% (binary-unit 30 #f 1 7)
% (binary-double 18 #f 1 7)
% (binary 90 #t 1 7)
% (binary-order 30 #f 1 7)
% (binary-posweight-order 54 #f)
% (binary-order-sos 30 #t)
% (binary-unit-uniteq 30 #f)
% (binary-weightorder 30 #f)
% (binary-weightorder-sos 30 #f)
% (binary-order 30 #f)
% (hyper-order 30 #f)
% (binary 168 #t)
%
%
% ********* EMPTY CLAUSE DERIVED *********
%
%
% timer checkpoints: c(117,40,1,234,0,1)
%
%
% START OF PROOF
% 118 [] horizontal_5_4(0) | vertical_4_5(0).
% 120 [] horizontal_5_3(0) | horizontal_5_2(0) | vertical_4_3(0).
% 122 [] horizontal_5_1(0) | vertical_4_1(0).
% 124 [] vertical_4_4(0) | horizontal_4_4(0) | horizontal_4_3(0) | vertical_3_4(0).
% 126 [] vertical_4_2(0) | horizontal_4_2(0) | horizontal_4_1(0) | vertical_3_2(0).
% 128 [] vertical_3_5(0) | horizontal_3_4(0) | vertical_2_5(0).
% 130 [] vertical_3_3(0) | horizontal_3_3(0) | horizontal_3_2(0) | vertical_2_3(0).
% 132 [] vertical_3_1(0) | horizontal_3_1(0) | vertical_2_1(0).
% 134 [] vertical_2_4(0) | horizontal_2_4(0) | horizontal_2_3(0) | vertical_1_4(0).
% 136 [?] ?
% 138 [] vertical_1_5(0) | horizontal_1_4(0).
% 140 [?] ?
% 143 [] -vertical_1_2(0).
% 145 [] -horizontal_1_1(0).
% 148 [] -vertical_1_4(0) | -horizontal_1_4(0).
% 153 [] -horizontal_2_1(0) | -vertical_1_1(0).
% 154 [] -vertical_2_1(0) | -vertical_1_1(0).
% 161 [] -vertical_2_3(0) | -horizontal_2_3(0).
% 162 [] -horizontal_2_3(0) | -horizontal_2_2(0).
% 164 [] -vertical_2_3(0) | -horizontal_2_2(0).
% 173 [] -vertical_2_5(0) | -horizontal_2_4(0).
% 174 [] -vertical_2_5(0) | -vertical_1_5(0).
% 176 [] -vertical_3_1(0) | -horizontal_3_1(0).
% 179 [] -vertical_3_2(0) | -horizontal_3_2(0).
% 180 [] -horizontal_3_2(0) | -horizontal_3_1(0).
% 181 [] -horizontal_3_2(0) | -vertical_2_2(0).
% 182 [] -vertical_3_2(0) | -horizontal_3_1(0).
% 183 [] -vertical_3_2(0) | -vertical_2_2(0).
% 184 [] -horizontal_3_1(0) | -vertical_2_2(0).
% 191 [] -vertical_3_4(0) | -horizontal_3_4(0).
% 192 [] -horizontal_3_4(0) | -horizontal_3_3(0).
% 194 [] -vertical_3_4(0) | -horizontal_3_3(0).
% 195 [] -vertical_3_4(0) | -vertical_2_4(0).
% 196 [] -horizontal_3_3(0) | -vertical_2_4(0).
% 197 [] -vertical_3_5(0) | -horizontal_3_4(0).
% 198 [] -vertical_3_5(0) | -vertical_2_5(0).
% 200 [] -vertical_4_1(0) | -horizontal_4_1(0).
% 201 [] -horizontal_4_1(0) | -vertical_3_1(0).
% 202 [] -vertical_4_1(0) | -vertical_3_1(0).
% 205 [] -horizontal_4_2(0) | -vertical_3_2(0).
% 209 [] -vertical_4_3(0) | -horizontal_4_3(0).
% 210 [] -horizontal_4_3(0) | -horizontal_4_2(0).
% 211 [] -horizontal_4_3(0) | -vertical_3_3(0).
% 212 [] -vertical_4_3(0) | -horizontal_4_2(0).
% 213 [] -vertical_4_3(0) | -vertical_3_3(0).
% 214 [] -horizontal_4_2(0) | -vertical_3_3(0).
% 221 [] -vertical_4_5(0) | -horizontal_4_4(0).
% 222 [] -vertical_4_5(0) | -vertical_3_5(0).
% 223 [] -horizontal_4_4(0) | -vertical_3_5(0).
% 224 [] -horizontal_5_1(0) | -vertical_4_1(0).
% 225 [] -horizontal_5_2(0) | -horizontal_5_1(0).
% 226 [] -horizontal_5_2(0) | -vertical_4_2(0).
% 227 [] -horizontal_5_1(0) | -vertical_4_2(0).
% 228 [] -horizontal_5_3(0) | -horizontal_5_2(0).
% 229 [] -horizontal_5_3(0) | -vertical_4_3(0).
% 231 [] -horizontal_5_4(0) | -horizontal_5_3(0).
% 232 [] -horizontal_5_4(0) | -vertical_4_4(0).
% 233 [] -horizontal_5_3(0) | -vertical_4_4(0).
% 234 [] -horizontal_5_4(0) | -vertical_4_5(0).
% 352 [input:140,cut:145] vertical_1_1(0).
% 362 [hyper:225,120,122] horizontal_5_3(0) | vertical_4_3(0) | vertical_4_1(0).
% 365 [hyper:231,120,118] horizontal_5_2(0) | vertical_4_5(0) | vertical_4_3(0).
% 419 [hyper:174,128,138] vertical_3_5(0) | horizontal_3_4(0) | horizontal_1_4(0).
% 424 [hyper:222,128,118] horizontal_5_4(0) | horizontal_3_4(0) | vertical_2_5(0).
% 436 [hyper:154,132,352] vertical_3_1(0) | horizontal_3_1(0).
% 456 [hyper:202,436,122] horizontal_5_1(0) | horizontal_3_1(0).
% 472 [hyper:225,456,120] horizontal_5_3(0) | vertical_4_3(0) | horizontal_3_1(0).
% 492 [hyper:221,124,118] horizontal_5_4(0) | vertical_4_4(0) | horizontal_4_3(0) | vertical_3_4(0).
% 496 [hyper:232,124,118] vertical_4_5(0) | horizontal_4_4(0) | horizontal_4_3(0) | vertical_3_4(0).
% 619 [hyper:225,365,456] vertical_4_5(0) | vertical_4_3(0) | horizontal_3_1(0).
% 644 [hyper:222,419,118] horizontal_5_4(0) | horizontal_3_4(0) | horizontal_1_4(0).
% 685 [hyper:182,126,456] horizontal_5_1(0) | vertical_4_2(0) | horizontal_4_2(0) | horizontal_4_1(0).
% 691 [hyper:201,126,436] vertical_4_2(0) | horizontal_4_2(0) | vertical_3_2(0) | horizontal_3_1(0).
% 804 [hyper:180,130,436] vertical_3_3(0) | horizontal_3_3(0) | vertical_3_1(0) | vertical_2_3(0).
% 810 [hyper:192,130,419] vertical_3_5(0) | vertical_3_3(0) | horizontal_3_2(0) | vertical_2_3(0) | horizontal_1_4(0).
% 811 [hyper:192,130,424] horizontal_5_4(0) | vertical_3_3(0) | horizontal_3_2(0) | vertical_2_5(0) | vertical_2_3(0).
% 1103 [input:136,cut:143] vertical_2_2(0) | horizontal_2_2(0) | horizontal_2_1(0).
% 1106 [hyper:153,1103,352] vertical_2_2(0) | horizontal_2_2(0).
% 1165 [hyper:181,1106,130] vertical_3_3(0) | horizontal_3_3(0) | vertical_2_3(0) | horizontal_2_2(0).
% 1169 [hyper:184,1106,436] vertical_3_1(0) | horizontal_2_2(0).
% 1171 [hyper:184,1106,472] horizontal_5_3(0) | vertical_4_3(0) | horizontal_2_2(0).
% 1172 [hyper:184,1106,619] vertical_4_5(0) | vertical_4_3(0) | horizontal_2_2(0).
% 1195 [hyper:162,1169,134] vertical_3_1(0) | vertical_2_4(0) | horizontal_2_4(0) | vertical_1_4(0).
% 1357 [hyper:191,492,424] horizontal_5_4(0) | vertical_4_4(0) | horizontal_4_3(0) | vertical_2_5(0).
% 1358 [hyper:191,492,644] horizontal_5_4(0) | vertical_4_4(0) | horizontal_4_3(0) | horizontal_1_4(0).
% 1686 [hyper:200,685,122] horizontal_5_1(0) | vertical_4_2(0) | horizontal_4_2(0).
% 1770 [hyper:224,1686,362] horizontal_5_3(0) | vertical_4_3(0) | vertical_4_2(0) | horizontal_4_2(0).
% 1823 [hyper:227,691,binarycut:456] horizontal_4_2(0) | vertical_3_2(0) | horizontal_3_1(0).
% 1837 [hyper:176,1823,1169] horizontal_4_2(0) | vertical_3_2(0) | horizontal_2_2(0).
% 1858 [hyper:212,1823,472] horizontal_5_3(0) | vertical_3_2(0) | horizontal_3_1(0).
% 1889 [hyper:183,1837,binarycut:1106] horizontal_4_2(0) | horizontal_2_2(0).
% 1970 [hyper:164,1889,130] horizontal_4_2(0) | vertical_3_3(0) | horizontal_3_3(0) | horizontal_3_2(0).
% 1975 [hyper:210,1889,124] vertical_4_4(0) | horizontal_4_4(0) | vertical_3_4(0) | horizontal_2_2(0).
% 1985 [hyper:212,1889,1171] horizontal_5_3(0) | horizontal_2_2(0).
% 1986 [hyper:212,1889,1172] vertical_4_5(0) | horizontal_2_2(0).
% 2006 [hyper:162,1985,134] horizontal_5_3(0) | vertical_2_4(0) | horizontal_2_4(0) | vertical_1_4(0).
% 2008 [hyper:164,1985,130] horizontal_5_3(0) | vertical_3_3(0) | horizontal_3_3(0) | horizontal_3_2(0).
% 2012 [hyper:231,1985,424] horizontal_3_4(0) | vertical_2_5(0) | horizontal_2_2(0).
% 2013 [hyper:231,1985,644] horizontal_3_4(0) | horizontal_2_2(0) | horizontal_1_4(0).
% 2425 [hyper:164,804,1169] vertical_3_3(0) | horizontal_3_3(0) | vertical_3_1(0).
% 2481 [hyper:176,2425,472] horizontal_5_3(0) | vertical_4_3(0) | vertical_3_3(0) | horizontal_3_3(0).
% 3079 [hyper:214,1165,binarycut:1889] horizontal_3_3(0) | vertical_2_3(0) | horizontal_2_2(0).
% 3591 [hyper:226,1770,120] horizontal_5_3(0) | vertical_4_3(0) | horizontal_4_2(0).
% 3636 [hyper:228,3591,365] vertical_4_5(0) | vertical_4_3(0) | horizontal_4_2(0).
% 4037 [hyper:221,1975,binarycut:1986] vertical_4_4(0) | vertical_3_4(0) | horizontal_2_2(0).
% 4078 [hyper:233,4037,binarycut:1985] vertical_3_4(0) | horizontal_2_2(0).
% 4140 [hyper:191,4078,2012] vertical_2_5(0) | horizontal_2_2(0).
% 4141 [hyper:191,4078,2013] horizontal_2_2(0) | horizontal_1_4(0).
% 4144 [hyper:194,4078,3079] vertical_2_3(0) | horizontal_2_2(0).
% 4719 [hyper:214,2481,3591] horizontal_5_3(0) | vertical_4_3(0) | horizontal_3_3(0).
% 4769 [hyper:213,4719,2425] horizontal_5_3(0) | horizontal_3_3(0) | vertical_3_1(0).
% 4772 [hyper:213,4719,2008] horizontal_5_3(0) | horizontal_3_3(0) | horizontal_3_2(0).
% 4774 [hyper:228,4719,365] vertical_4_5(0) | vertical_4_3(0) | horizontal_3_3(0).
% 4804 [hyper:176,4769,1858] horizontal_5_3(0) | horizontal_3_3(0) | vertical_3_2(0).
% 5073 [hyper:179,4804,4772] horizontal_5_3(0) | horizontal_3_3(0).
% 5139 [hyper:192,5073,128] horizontal_5_3(0) | vertical_3_5(0) | vertical_2_5(0).
% 5140 [hyper:192,5073,419] horizontal_5_3(0) | vertical_3_5(0) | horizontal_1_4(0).
% 5141 [hyper:192,5073,424] horizontal_5_4(0) | horizontal_5_3(0) | vertical_2_5(0).
% 5142 [hyper:192,5073,644] horizontal_5_4(0) | horizontal_5_3(0) | horizontal_1_4(0).
% 5158 [hyper:196,5073,2006] horizontal_5_3(0) | horizontal_2_4(0) | vertical_1_4(0).
% 5174 [hyper:229,5073,4774] vertical_4_5(0) | horizontal_3_3(0).
% 5246 [hyper:194,5174,496] vertical_4_5(0) | horizontal_4_4(0) | horizontal_4_3(0).
% 5451 [hyper:233,5141,1357] horizontal_5_4(0) | horizontal_4_3(0) | vertical_2_5(0).
% 5483 [hyper:233,5142,1358] horizontal_5_4(0) | horizontal_4_3(0) | horizontal_1_4(0).
% 5498 [hyper:148,5158,5140] horizontal_5_3(0) | vertical_3_5(0) | horizontal_2_4(0).
% 5941 [hyper:173,5498,5139] horizontal_5_3(0) | vertical_3_5(0).
% 5985 [hyper:198,5941,5141] horizontal_5_4(0) | horizontal_5_3(0).
% 6016 [hyper:231,5941,118] vertical_4_5(0) | vertical_3_5(0).
% 6102 [hyper:233,5985,492] horizontal_5_4(0) | horizontal_4_3(0) | vertical_3_4(0).
% 6118 [hyper:223,6016,5246] vertical_4_5(0) | horizontal_4_3(0).
% 6137 [hyper:164,810,binarycut:4141] vertical_3_5(0) | vertical_3_3(0) | horizontal_3_2(0) | horizontal_1_4(0).
% 6178 [hyper:209,6118,3636] vertical_4_5(0) | horizontal_4_2(0).
% 6194 [hyper:234,6118,5451] horizontal_4_3(0) | vertical_2_5(0).
% 6195 [hyper:234,6118,5483] horizontal_4_3(0) | horizontal_1_4(0).
% 6249 [hyper:211,811,binarycut:6194] horizontal_5_4(0) | horizontal_3_2(0) | vertical_2_5(0) | vertical_2_3(0).
% 6306 [hyper:210,6178,6118] vertical_4_5(0).
% 6320 [hyper:222,6306,419] horizontal_3_4(0) | horizontal_1_4(0).
% 6321 [hyper:222,6306,5941] horizontal_5_3(0).
% 6392 [hyper:197,6137,binarycut:6320] vertical_3_3(0) | horizontal_3_2(0) | horizontal_1_4(0).
% 6418 [hyper:210,6194,1823] vertical_3_2(0) | horizontal_3_1(0) | vertical_2_5(0).
% 6568 [hyper:211,6392,binarycut:6195] horizontal_3_2(0) | horizontal_1_4(0).
% 6603 [hyper:180,6568,436] vertical_3_1(0) | horizontal_1_4(0).
% 6623 [hyper:148,6603,1195] vertical_3_1(0) | vertical_2_4(0) | horizontal_2_4(0).
% 6719 [hyper:231,6249,cut:6321] horizontal_3_2(0) | vertical_2_5(0) | vertical_2_3(0).
% 6737 [hyper:164,6719,4140] horizontal_3_2(0) | vertical_2_5(0).
% 6779 [hyper:180,6737,436] vertical_3_1(0) | vertical_2_5(0).
% 6955 [hyper:231,6102,cut:6321] horizontal_4_3(0) | vertical_3_4(0).
% 7056 [hyper:176,6418,binarycut:6779] vertical_3_2(0) | vertical_2_5(0).
% 7075 [hyper:179,7056,binarycut:6737] vertical_2_5(0).
% 7084 [hyper:173,7075,134] vertical_2_4(0) | horizontal_2_3(0) | vertical_1_4(0).
% 7089 [hyper:174,7075,138] horizontal_1_4(0).
% 7107 [hyper:173,6623,cut:7075] vertical_3_1(0) | vertical_2_4(0).
% 7140 [hyper:195,7107,6955] horizontal_4_3(0) | vertical_3_1(0).
% 7143 [?] ?
% 7223 [hyper:211,7140,binarycut:7143] vertical_3_1(0).
% 7231 [hyper:176,7223,1823] horizontal_4_2(0) | vertical_3_2(0).
% 7250 [hyper:179,7231,1970] horizontal_4_2(0) | vertical_3_3(0) | horizontal_3_3(0).
% 7259 [hyper:210,7231,6955] vertical_3_4(0) | vertical_3_2(0).
% 7382 [hyper:148,7084,cut:7089] vertical_2_4(0) | horizontal_2_3(0).
% 7408 [hyper:161,7382,4144] vertical_2_4(0) | horizontal_2_2(0).
% 7440 [hyper:162,7408,7382] vertical_2_4(0).
% 7449 [hyper:195,7440,6955] horizontal_4_3(0).
% 7450 [hyper:195,7440,7259] vertical_3_2(0).
% 7499 [hyper:196,7250,cut:7440] horizontal_4_2(0) | vertical_3_3(0).
% 7510 [hyper:205,7499,cut:7450] vertical_3_3(0).
% 7515 [hyper:211,7510,cut:7449] contradiction
% END OF PROOF
%
% Proof found by the following strategy:
%
% using hyperresolution
% not using sos strategy
% using positive unit paramodulation strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% clause length limited to 7
% clause depth limited to 1
% seconds given: 30
%
%
% ***GANDALF_FOUND_A_REFUTATION***
%
% Global statistics over all passes:
%
% given clauses: 311
% derived clauses: 35368
% kept clauses: 2279
% kept size sum: 22348
% kept mid-nuclei: 4689
% kept new demods: 0
% forw unit-subs: 888
% forw double-subs: 5355
% forw overdouble-subs: 19184
% backward subs: 437
% fast unit cutoff: 45
% full unit cutoff: 0
% dbl unit cutoff: 18
% real runtime : 0.86
% process. runtime: 0.83
% specific non-discr-tree subsumption statistics:
% tried: 848887
% length fails: 0
% strength fails: 219738
% predlist fails: 332439
% aux str. fails: 0
% by-lit fails: 251925
% full subs tried: 0
% full subs fail: 0
%
% ; program args: ("/home/graph/tptp/Systems/Gandalf---c-2.6/gandalf" "-time" "600" "/home/graph/tptp/TSTP/PreparedTPTP/otter:hypothesis:set(auto),clear(print_given)---add_equality:r/PUZ/PUZ016-2.005+noeq.in")
%
%------------------------------------------------------------------------------