%------------------------------------------------------------------------------
% File : Gandalf---c-2.6
% Problem : GRP128-2.006 : 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 : art05.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 29.5s
% Output : Assurance 29.5s
% 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/GRP/GRP128-2.006+noeq.in
% Using automatic strategy selection.
% Time limit in seconds: 600
%
% prove-all-passes started
%
% detected problem class: nne
% detected subclass: medium
%
% strategies selected:
% (hyper 27 #f 1 15)
% (binary-unit 10 #f 1 15)
% (binary-double 16 #f 1 15)
% (binary 54 #t 1 15)
% (binary-order 27 #f 1 15)
% (binary-posweight-order 125 #f)
% (binary-order-sos 54 #t)
% (binary-unit-uniteq 27 #f)
% (binary-weightorder 54 #f)
% (binary-order 54 #f)
% (hyper-order 43 #f)
% (binary 109 #t)
%
%
% ********* EMPTY CLAUSE DERIVED *********
%
%
% timer checkpoints: c(62,40,0,124,0,0,35326,4,2027,43432,5,2701,43432,1,2701,43432,50,2702,43432,40,2702,43494,0,2702,43758,50,2703,43820,0,2703,44084,50,2705,44146,0,2706,44410,50,2708,44472,0,2708,44736,50,2709,44798,0,2709,45062,50,2710,45124,0,2711,45388,50,2712,45450,0,2712,45714,50,2713,45776,0,2715,46040,50,2716,46102,0,2716,46366,50,2717,46428,0,2717,46692,50,2718,46754,0,2720,47018,50,2721,47080,0,2721,47344,50,2722,47406,0,2724,47670,50,2725,47732,0,2725,47996,50,2726,48058,0,2726,48322,50,2727,48384,0,2728,48648,50,2729,48710,0,2729,48974,50,2731,49036,0,2732,49300,50,2734,49362,0,2734,49626,50,2735,49688,0,2735,49952,50,2736,50014,0,2738,50278,50,2739,50278,40,2739,50340,0,2739)
%
%
% START OF PROOF
% 50279 [] next(e_1,e_2).
% 50280 [] next(e_2,e_3).
% 50281 [] next(e_3,e_4).
% 50282 [] next(e_4,e_5).
% 50289 [] greater(e_3,e_2).
% 50290 [] greater(e_4,e_2).
% 50291 [] greater(e_5,e_2).
% 50292 [] greater(e_6,e_2).
% 50293 [] greater(e_4,e_3).
% 50294 [] greater(e_5,e_3).
% 50295 [] greater(e_6,e_3).
% 50296 [] greater(e_5,e_4).
% 50297 [] greater(e_6,e_4).
% 50298 [] greater(e_6,e_5).
% 50299 [] -product(X,e_1,Y) | -greater(Y,Z) | -next(X,Z).
% 50300 [] group_element(e_1).
% 50301 [] group_element(e_2).
% 50302 [] group_element(e_3).
% 50303 [] group_element(e_4).
% 50304 [] group_element(e_5).
% 50305 [] group_element(e_6).
% 50306 [] -equalish(e_1,e_2).
% 50307 [] -equalish(e_1,e_3).
% 50308 [] -equalish(e_1,e_4).
% 50309 [] -equalish(e_1,e_5).
% 50310 [] -equalish(e_1,e_6).
% 50311 [] -equalish(e_2,e_1).
% 50312 [] -equalish(e_2,e_3).
% 50313 [] -equalish(e_2,e_4).
% 50314 [] -equalish(e_2,e_5).
% 50315 [] -equalish(e_2,e_6).
% 50316 [] -equalish(e_3,e_1).
% 50318 [] -equalish(e_3,e_4).
% 50319 [] -equalish(e_3,e_5).
% 50320 [] -equalish(e_3,e_6).
% 50321 [] -equalish(e_4,e_1).
% 50324 [] -equalish(e_4,e_5).
% 50325 [] -equalish(e_4,e_6).
% 50326 [] -equalish(e_5,e_1).
% 50330 [] -equalish(e_5,e_6).
% 50331 [] -equalish(e_6,e_1).
% 50336 [] product(X,Y,e_5) | product(X,Y,e_6) | product(X,Y,e_3) | product(X,Y,e_4) | product(X,Y,e_1) | product(X,Y,e_2) | -group_element(X) | -group_element(Y).
% 50337 [] -product(X,Y,U) | -product(X,Y,Z) | equalish(Z,U).
% 50338 [] -product(X,U,Z) | -product(X,Y,Z) | equalish(Y,U).
% 50339 [] -product(U,Y,Z) | -product(X,Y,Z) | equalish(X,U).
% 50340 [] -product(Z,Y,U) | -product(X,Y,Z) | product(X,Z,U).
% 50348 [binary:50279,50299.3] -product(e_1,e_1,X) | -greater(X,e_2).
% 50349 [binary:50280,50299.3] -product(e_2,e_1,X) | -greater(X,e_3).
% 50350 [binary:50281,50299.3] -product(e_3,e_1,X) | -greater(X,e_4).
% 50351 [binary:50282,50299.3] -product(e_4,e_1,X) | -greater(X,e_5).
% 50370 [binary:50289,50348.2] -product(e_1,e_1,e_3).
% 50371 [binary:50290,50348.2] -product(e_1,e_1,e_4).
% 50373 [binary:50292,50348.2] -product(e_1,e_1,e_6).
% 50376 [binary:50300,50336.8] product(X,e_1,e_6) | product(X,e_1,e_5) | product(X,e_1,e_4) | product(X,e_1,e_3) | product(X,e_1,e_2) | product(X,e_1,e_1) | -group_element(X).
% 50377 [binary:50301,50336.7] product(e_2,X,e_5) | product(e_2,X,e_3) | product(e_2,X,e_6) | product(e_2,X,e_1) | product(e_2,X,e_4) | product(e_2,X,e_2) | -group_element(X).
% 50378 [binary:50301,50336.8] product(X,e_2,e_6) | product(X,e_2,e_5) | product(X,e_2,e_4) | product(X,e_2,e_3) | product(X,e_2,e_2) | product(X,e_2,e_1) | -group_element(X).
% 50379 [binary:50302,50336.7] product(e_3,X,e_5) | product(e_3,X,e_3) | product(e_3,X,e_6) | product(e_3,X,e_1) | product(e_3,X,e_4) | product(e_3,X,e_2) | -group_element(X).
% 50381 [binary:50303,50336.7] product(e_4,X,e_5) | product(e_4,X,e_3) | product(e_4,X,e_6) | product(e_4,X,e_1) | product(e_4,X,e_4) | product(e_4,X,e_2) | -group_element(X).
% 50382 [binary:50303,50336.8] product(X,e_4,e_6) | product(X,e_4,e_5) | product(X,e_4,e_4) | product(X,e_4,e_3) | product(X,e_4,e_2) | product(X,e_4,e_1) | -group_element(X).
% 50383 [binary:50304,50336.7] product(e_5,X,e_5) | product(e_5,X,e_3) | product(e_5,X,e_6) | product(e_5,X,e_1) | product(e_5,X,e_4) | product(e_5,X,e_2) | -group_element(X).
% 50385 [binary:50305,50336.7] product(e_6,X,e_5) | product(e_6,X,e_3) | product(e_6,X,e_6) | product(e_6,X,e_1) | product(e_6,X,e_4) | product(e_6,X,e_2) | -group_element(X).
% 50387 [binary:50348,50336,cut:50373,cut:50370,cut:50371,cut:50300,cut:50291] product(e_1,e_1,e_1) | product(e_1,e_1,e_2).
% 50399 [binary:50306,50337.3] -product(X,Y,e_1) | -product(X,Y,e_2).
% 50400 [binary:50307,50337.3] -product(X,Y,e_1) | -product(X,Y,e_3).
% 50401 [binary:50308,50337.3] -product(X,Y,e_1) | -product(X,Y,e_4).
% 50402 [binary:50309,50337.3] -product(X,Y,e_1) | -product(X,Y,e_5).
% 50403 [binary:50310,50337.3] -product(X,Y,e_1) | -product(X,Y,e_6).
% 50404 [binary:50312,50337.3] -product(X,Y,e_2) | -product(X,Y,e_3).
% 50405 [binary:50313,50337.3] -product(X,Y,e_2) | -product(X,Y,e_4).
% 50406 [binary:50314,50337.3] -product(X,Y,e_2) | -product(X,Y,e_5).
% 50407 [binary:50315,50337.3] -product(X,Y,e_2) | -product(X,Y,e_6).
% 50408 [binary:50318,50337.3] -product(X,Y,e_3) | -product(X,Y,e_4).
% 50409 [binary:50319,50337.3] -product(X,Y,e_3) | -product(X,Y,e_5).
% 50410 [binary:50320,50337.3] -product(X,Y,e_3) | -product(X,Y,e_6).
% 50411 [binary:50324,50337.3] -product(X,Y,e_4) | -product(X,Y,e_5).
% 50412 [binary:50325,50337.3] -product(X,Y,e_4) | -product(X,Y,e_6).
% 50413 [binary:50330,50337.3] -product(X,Y,e_5) | -product(X,Y,e_6).
% 50416 [binary:50293,50349.2] -product(e_2,e_1,e_4).
% 50417 [binary:50294,50349.2] -product(e_2,e_1,e_5).
% 50418 [binary:50295,50349.2] -product(e_2,e_1,e_6).
% 50428 [binary:50296,50350.2] -product(e_3,e_1,e_5).
% 50429 [binary:50297,50350.2] -product(e_3,e_1,e_6).
% 50436 [binary:50306,50338.3] -product(X,e_1,Y) | -product(X,e_2,Y).
% 50438 [binary:50308,50338.3] -product(X,e_1,Y) | -product(X,e_4,Y).
% 50439 [binary:50309,50338.3] -product(X,e_1,Y) | -product(X,e_5,Y).
% 50440 [binary:50310,50338.3] -product(X,e_1,Y) | -product(X,e_6,Y).
% 50441 [binary:50312,50338.3] -product(X,e_2,Y) | -product(X,e_3,Y).
% 50442 [binary:50313,50338.3] -product(X,e_2,Y) | -product(X,e_4,Y).
% 50447 [binary:50320,50338.3] -product(X,e_3,Y) | -product(X,e_6,Y).
% 50449 [binary:50325,50338.3] -product(X,e_4,Y) | -product(X,e_6,Y).
% 50450 [binary:50330,50338.3] -product(X,e_5,Y) | -product(X,e_6,Y).
% 50452 [binary:50340.3,50429] -product(e_3,X,e_1) | -product(e_1,X,e_6).
% 50455 [binary:50298,50351.2] -product(e_4,e_1,e_6).
% 50465 [binary:50307,50339.3] -product(e_1,X,Y) | -product(e_3,X,Y).
% 50466 [binary:50308,50339.3] -product(e_1,X,Y) | -product(e_4,X,Y).
% 50469 [binary:50312,50339.3] -product(e_2,X,Y) | -product(e_3,X,Y).
% 50470 [binary:50313,50339.3] -product(e_2,X,Y) | -product(e_4,X,Y).
% 50471 [binary:50314,50339.3] -product(e_2,X,Y) | -product(e_5,X,Y).
% 50472 [binary:50315,50339.3] -product(e_2,X,Y) | -product(e_6,X,Y).
% 50474 [binary:50319,50339.3] -product(e_3,X,Y) | -product(e_5,X,Y).
% 50475 [binary:50320,50339.3] -product(e_3,X,Y) | -product(e_6,X,Y).
% 50476 [binary:50324,50339.3] -product(e_4,X,Y) | -product(e_5,X,Y).
% 50477 [binary:50325,50339.3] -product(e_4,X,Y) | -product(e_6,X,Y).
% 50567 [binary:50340.3,50399] -product(Y,Z,e_1) | -product(X,Y,e_2) | -product(X,Z,Y).
% 50568 [binary:50340.3,50399,factor] -product(e_2,e_2,e_1) | -product(X,e_2,e_2).
% 50570 [binary:50340.3,50399.2,factor] -product(e_1,e_1,e_2) | -product(X,e_1,e_1).
% 50573 [binary:50340.3,50400,factor] -product(e_3,e_3,e_1) | -product(X,e_3,e_3).
% 50577 [binary:50340.3,50401,factor] -product(e_4,e_4,e_1) | -product(X,e_4,e_4).
% 50590 [binary:50340.3,50402,factor] -product(e_5,e_5,e_1) | -product(X,e_5,e_5).
% 50594 [binary:50340.3,50403,factor] -product(e_6,e_6,e_1) | -product(X,e_6,e_6).
% 50598 [binary:50340.3,50404,factor] -product(e_3,e_3,e_2) | -product(X,e_3,e_3).
% 50599 [binary:50340.3,50404.2] -product(Y,Z,e_3) | -product(X,Y,e_2) | -product(X,Z,Y).
% 50600 [binary:50340.3,50404.2,factor] -product(e_2,e_2,e_3) | -product(X,e_2,e_2).
% 50603 [binary:50340.3,50405,factor] -product(e_4,e_4,e_2) | -product(X,e_4,e_4).
% 50605 [binary:50340.3,50405.2,factor] -product(e_2,e_2,e_4) | -product(X,e_2,e_2).
% 50632 [binary:50340.3,50406,factor] -product(e_5,e_5,e_2) | -product(X,e_5,e_5).
% 50634 [binary:50340.3,50406.2,factor] -product(e_2,e_2,e_5) | -product(X,e_2,e_2).
% 50656 [binary:50340.3,50407,factor] -product(e_6,e_6,e_2) | -product(X,e_6,e_6).
% 50658 [binary:50340.3,50407.2,factor] -product(e_2,e_2,e_6) | -product(X,e_2,e_2).
% 50661 [binary:50340.3,50408,factor] -product(e_4,e_4,e_3) | -product(X,e_4,e_4).
% 50663 [binary:50340.3,50408.2,factor] -product(e_3,e_3,e_4) | -product(X,e_3,e_3).
% 50666 [binary:50340.3,50409,factor] -product(e_5,e_5,e_3) | -product(X,e_5,e_5).
% 50668 [binary:50340.3,50409.2,factor] -product(e_3,e_3,e_5) | -product(X,e_3,e_3).
% 50671 [binary:50340.3,50410,factor] -product(e_6,e_6,e_3) | -product(X,e_6,e_6).
% 50673 [binary:50340.3,50410.2,factor] -product(e_3,e_3,e_6) | -product(X,e_3,e_3).
% 50676 [binary:50340.3,50411,factor] -product(e_5,e_5,e_4) | -product(X,e_5,e_5).
% 50678 [binary:50340.3,50411.2,factor] -product(e_4,e_4,e_5) | -product(X,e_4,e_4).
% 50716 [binary:50340.3,50412,factor] -product(e_6,e_6,e_4) | -product(X,e_6,e_6).
% 50718 [binary:50340.3,50412.2,factor] -product(e_4,e_4,e_6) | -product(X,e_4,e_4).
% 50734 [binary:50340.3,50413,factor] -product(e_6,e_6,e_5) | -product(X,e_6,e_6).
% 50736 [binary:50340.3,50413.2,factor] -product(e_5,e_5,e_6) | -product(X,e_5,e_5).
% 50774 [binary:50377.6,50436.2,cut:50301,binarydemod:50568,50605,50658,50634,50600] -product(e_2,e_1,e_2) | -product(X,e_2,e_2).
% 50977 [binary:50340.3,50452.2] -product(e_3,X,e_1) | -product(e_1,Y,X) | -product(X,Y,e_6).
% 51146 [binary:50339,50387,binarycut:50570] -product(X,e_1,e_1) | equalish(X,e_1).
% 51152 [binary:50311,51146.2] -product(e_2,e_1,e_1).
% 51153 [binary:50316,51146.2] -product(e_3,e_1,e_1).
% 51154 [binary:50321,51146.2] -product(e_4,e_1,e_1).
% 51155 [binary:50326,51146.2] -product(e_5,e_1,e_1).
% 51156 [binary:50331,51146.2] -product(e_6,e_1,e_1).
% 51243 [binary:50381.5,50438.2,cut:50303,binarydemod:50718,50577,50661,50603,50678] -product(e_4,e_1,e_4) | -product(X,e_4,e_4).
% 51387 [binary:50383,50439.2,cut:50304,binarydemod:50736,50666,50590,50632,50676] -product(e_5,e_1,e_5) | -product(X,e_5,e_5).
% 51511 [binary:50385.3,50440.2,cut:50305,binarydemod:50734,50671,50594,50656,50716] -product(e_6,e_1,e_6) | -product(X,e_6,e_6).
% 51602 [binary:50377.6,50441,cut:50301,binarydemod:50568,50605,50658,50634,50600] -product(e_2,e_3,e_2) | -product(X,e_2,e_2).
% 51623 [binary:50379.2,50441.2,cut:50302,binarydemod:50673,50668,50573,50598,50663] -product(e_3,e_2,e_3) | -product(X,e_3,e_3).
% 51715 [binary:50377.6,50442,cut:50301,binarydemod:50568,50605,50658,50634,50600] -product(e_2,e_4,e_2) | -product(X,e_2,e_2).
% 52364 [binary:50379.2,50447,cut:50302,binarydemod:50673,50668,50573,50598,50663] -product(e_3,e_6,e_3) | -product(X,e_3,e_3).
% 52687 [binary:50385.3,50449.2,cut:50305,binarydemod:50734,50671,50594,50656,50716] -product(e_6,e_4,e_6) | -product(X,e_6,e_6).
% 52797 [binary:50383,50450,cut:50304,binarydemod:50736,50666,50590,50632,50676] -product(e_5,e_6,e_5) | -product(X,e_5,e_5).
% 53306 [binary:50382.3,50466.2,cut:50303,binarycut:50603,binarycut:50577,binarycut:50661,binarycut:50678,binarycut:50718] -product(e_1,e_4,e_4).
% 53671 [binary:50378.5,50469,cut:50301,binarycut:50658,binarycut:50568,binarycut:50634,binarycut:50600,binarycut:50605] -product(e_3,e_2,e_2).
% 53910 [binary:50382.3,50470.2,cut:50303,binarycut:50603,binarycut:50577,binarycut:50661,binarycut:50678,binarycut:50718] -product(e_2,e_4,e_4).
% 54980 [binary:50382.3,50477,cut:50303,binarycut:50603,binarycut:50577,binarycut:50661,binarycut:50678,binarycut:50718] -product(e_6,e_4,e_4).
% 56611 [binary:50387.2,50567.2] product(e_1,e_1,e_1) | -product(e_1,X,e_1).
% 56637 [binary:50438,56611,factor] -product(e_1,e_4,e_1).
% 56641 [binary:50440,56611,factor] -product(e_1,e_6,e_1).
% 56659 [binary:50340.3,56641] -product(e_1,X,e_6) | -product(e_6,X,e_1).
% 57468 [binary:50340.3,50774.2,factor:factor] -product(e_2,e_1,e_2).
% 57469 [binary:50336.6,57468,cut:51152,cut:50416,cut:50418,cut:50417,cut:50301,cut:50300] product(e_2,e_1,e_3).
% 57470 [binary:50340,57469] -product(X,e_1,e_2) | product(X,e_2,e_3).
% 57471 [binary:50340.2,57469] -product(e_3,e_1,X) | product(e_2,e_3,X).
% 57480 [binary:50438,57469] -product(e_2,e_4,e_3).
% 57483 [binary:50469,57469] -product(e_3,e_1,e_3).
% 57484 [binary:50470,57469] -product(e_4,e_1,e_3).
% 57485 [binary:50471,57469] -product(e_5,e_1,e_3).
% 57486 [binary:50472,57469] -product(e_6,e_1,e_3).
% 57533 [binary:50408,57470.2] -product(X,e_1,e_2) | -product(X,e_2,e_4).
% 57548 [binary:50442,57470.2] -product(X,e_1,e_2) | -product(X,e_4,e_3).
% 57568 [binary:50476.2,57470.2] -product(e_5,e_1,e_2) | -product(e_4,e_2,e_3).
% 57570 [binary:50477.2,57470.2] -product(e_6,e_1,e_2) | -product(e_4,e_2,e_3).
% 59649 [binary:50336.4,50436,cut:50300,binarycut:57533] -product(X,e_2,e_4) | product(X,e_1,e_6) | product(X,e_1,e_1) | product(X,e_1,e_3) | product(X,e_1,e_5) | -group_element(X).
% 59650 [binary:50302,59649.6,cut:50428,cut:57483,cut:51153,cut:50429] -product(e_3,e_2,e_4).
% 61303 [binary:50340.3,51243.2,factor:factor] -product(e_4,e_1,e_4).
% 61653 [binary:50340.3,51387.2,factor:factor] -product(e_5,e_1,e_5).
% 61683 [binary:50340.3,51511.2,factor:factor] -product(e_6,e_1,e_6).
% 61766 [binary:50340.3,51602.2,factor:factor] -product(e_2,e_3,e_2).
% 61771 [binary:57471.2,61766] -product(e_3,e_1,e_2).
% 61773 [binary:50336.6,61771,cut:51153,cut:57483,cut:50429,cut:50428,cut:50302,cut:50300] product(e_3,e_1,e_4).
% 61779 [binary:50340.2,61773] -product(e_4,e_1,X) | product(e_3,e_4,X).
% 61791 [binary:50474,61773] -product(e_5,e_1,e_4).
% 61792 [binary:50475,61773] -product(e_6,e_1,e_4).
% 63086 [binary:50442.2,61779.2] -product(e_4,e_1,X) | -product(e_3,e_2,X).
% 63090 [binary:50465.2,61779.2] -product(e_4,e_1,X) | -product(e_1,e_4,X).
% 63091 [binary:50469.2,61779.2] -product(e_4,e_1,X) | -product(e_2,e_4,X).
% 63093 [binary:50475,61779.2] -product(e_4,e_1,X) | -product(e_6,e_4,X).
% 63819 [binary:50336,63086,cut:50455,cut:57484,cut:61303,cut:51154,cut:50303,cut:50300] -product(e_3,e_2,e_5) | product(e_4,e_1,e_2).
% 63846 [binary:50336,63090,cut:50455,cut:57484,cut:61303,cut:51154,cut:50303,cut:50300] -product(e_1,e_4,e_5) | product(e_4,e_1,e_2).
% 63853 [binary:50336,63091,cut:50455,cut:57484,cut:61303,cut:51154,cut:50303,cut:50300] -product(e_2,e_4,e_5) | product(e_4,e_1,e_2).
% 63869 [binary:50336,63093,cut:50455,cut:57484,cut:61303,cut:51154,cut:50303,cut:50300] -product(e_6,e_4,e_5) | product(e_4,e_1,e_2).
% 64066 [binary:50340.3,51623.2,factor:factor] -product(e_3,e_2,e_3).
% 64111 [binary:50340.3,51715.2,factor:factor] -product(e_2,e_4,e_2).
% 64567 [binary:50340.3,52364.2,factor:factor] -product(e_3,e_6,e_3).
% 64568 [binary:50340.3,64567] -product(e_3,X,e_6) | -product(e_6,X,e_3).
% 64584 [binary:57470.2,64568.2] -product(e_3,e_2,e_6) | -product(e_6,e_1,e_2).
% 64693 [binary:50340.3,52687.2,factor:factor] -product(e_6,e_4,e_6).
% 64725 [binary:50340.3,52797.2,factor:factor] -product(e_5,e_6,e_5).
% 64726 [binary:50340.3,64725] -product(e_5,X,e_6) | -product(e_6,X,e_5).
% 64735 [binary:50376.2,64726.2,cut:61683,cut:61792,cut:57486,cut:51156,cut:50305] -product(e_5,e_1,e_6) | product(e_6,e_1,e_2).
% 67642 [binary:57570,64735.2] -product(e_5,e_1,e_6) | -product(e_4,e_2,e_3).
% 67744 [binary:50336.6,57568,cut:51155,cut:61791,cut:57485,cut:61653,cut:50304,cut:50300,binarycut:67642] -product(e_4,e_2,e_3).
% 67747 [binary:57470.2,67744] -product(e_4,e_1,e_2).
% 67749 [binary:50336.6,67747,cut:51154,cut:61303,cut:57484,cut:50455,cut:50303,cut:50300] product(e_4,e_1,e_5).
% 67752 [binary:63819.2,67747] -product(e_3,e_2,e_5).
% 67755 [binary:63846.2,67747] -product(e_1,e_4,e_5).
% 67756 [binary:63853.2,67747] -product(e_2,e_4,e_5).
% 67757 [binary:63869.2,67747] -product(e_6,e_4,e_5).
% 67769 [binary:50477,67749] -product(e_6,e_1,e_5).
% 67814 [binary:50336,67769,cut:61683,cut:57486,cut:61792,cut:51156,cut:50305,cut:50300] product(e_6,e_1,e_2).
% 67828 [binary:50438,67814] -product(e_6,e_4,e_2).
% 67839 [binary:57548,67814] -product(e_6,e_4,e_3).
% 67847 [binary:64584.2,67814] -product(e_3,e_2,e_6).
% 67849 [binary:50336.6,67828,cut:54980,cut:67839,cut:64693,cut:67757,cut:50305,cut:50303] product(e_6,e_4,e_1).
% 67879 [binary:50336.2,67847,cut:67752,cut:64066,cut:59650,cut:53671,cut:50302,cut:50301] product(e_3,e_2,e_1).
% 67891 [binary:50472.2,67849] -product(e_2,e_4,e_1).
% 67900 [binary:56659.2,67849] -product(e_1,e_4,e_6).
% 67901 [binary:50599.3,67849,cut:67814] -product(e_1,e_4,e_3).
% 67953 [binary:50336.5,67891,cut:53910,cut:57480,cut:67756,cut:64111,cut:50301,cut:50303] product(e_2,e_4,e_6).
% 67958 [binary:50336.2,67900,cut:67755,cut:67901,cut:53306,cut:56637,cut:50300,cut:50303] product(e_1,e_4,e_2).
% 68033 [binary:50977.3,67953,cut:67958,cut:67879] contradiction
% END OF PROOF
%
% Proof found by the following strategy:
%
% using binary resolution
% not using sos strategy
% using double strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% using clause demodulation
% clause length limited to 15
% clause depth limited to 1
% seconds given: 16
%
%
% old unit clauses discarded
%
% ***GANDALF_FOUND_A_REFUTATION***
%
% Global statistics over all passes:
%
% given clauses: 6485
% derived clauses: 406208
% kept clauses: 38091
% kept size sum: 0
% kept mid-nuclei: 22547
% kept new demods: 0
% forw unit-subs: 127911
% forw double-subs: 34970
% forw overdouble-subs: 172503
% backward subs: 2964
% fast unit cutoff: 147205
% full unit cutoff: 0
% dbl unit cutoff: 1008
% real runtime : 35.40
% process. runtime: 34.81
% specific non-discr-tree subsumption statistics:
% tried: 21561144
% length fails: 1162689
% strength fails: 4623178
% predlist fails: 3359765
% aux str. fails: 2775
% by-lit fails: 9877627
% full subs tried: 25908
% full subs fail: 20695
%
% ; 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/GRP/GRP128-2.006+noeq.in")
%
%------------------------------------------------------------------------------