%------------------------------------------------------------------------------
% File : Gandalf---c-2.6
% Problem : SYN848-1 : TPTP v3.4.2. Released v2.5.0.
% Transfm : add_equality:r
% Format : otter:hypothesis:set(auto),clear(print_given)
% Command : gandalf-wrapper -time %d %s
% Computer : art02.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 239.5s
% Output : Assurance 239.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/SYN/SYN848-1+noeq.in
%
% Some predicates or functions were curried and renamed.
% 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 63)
% (binary-unit 30 #f 1 63)
% (binary-double 18 #f 1 63)
% (binary 90 #t 1 63)
% (binary-order 30 #f 1 63)
% (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(968,40,141,1936,0,162,35572,4,2413,41125,5,3163,41125,1,3163,41125,50,3163,41125,40,3163,42093,0,3176,43945,50,3277,44913,0,3287,46765,50,3384,47733,0,3401,49585,50,3500,50553,0,3511,52405,50,3621,53373,0,3631,55225,50,3737,56193,0,3755,58045,50,3864,59013,0,3874,60865,50,3996,61833,0,4007,63685,50,4121,64653,0,4139,66505,50,4258,67473,0,4268,69325,50,4400,70293,0,4410,72145,50,4534,73113,0,4552,74965,50,4681,74965,40,4681,75933,0,4692,84461,3,5593,85900,4,6043,87987,5,6493,87987,1,6493,87987,50,6493,87987,40,6493,88955,0,6505,114194,3,11008,118693,50,12659,118693,40,12659,119661,0,12736,127003,3,14237,132113,4,14987,136150,1,15737,136150,50,15737,136150,40,15737,137118,0,15755,147247,3,18476,153607,4,19806,156109,50,20511,156109,40,20511,157077,0,20573,178510,3,22074,179473,4,22824,180784,5,23574,180785,1,23574,180785,50,23575,180785,40,23575,181753,0,23599,189869,50,24087,189869,40,24087,190837,0,24100)
%
%
% START OF PROOF
% 181756 [?] ?
% 181777 [?] ?
% 181817 [?] ?
% 181868 [?] ?
% 181943 [?] ?
% 182018 [?] ?
% 182176 [?] ?
% 182362 [?] ?
% 182475 [?] ?
% 182681 [?] ?
% 182895 [?] ?
% 182898 [?] ?
% 183101 [?] ?
% 183297 [?] ?
% 183514 [?] ?
% 183800 [?] ?
% 184346 [?] ?
% 185361 [?] ?
% 186807 [?] ?
% 187363 [?] ?
% 187877 [?] ?
% 187959 [?] ?
% 188212 [?] ?
% 188600 [?] ?
% 189891 [?] ?
% 189895 [?] ?
% 190003 [?] ?
% 190006 [?] ?
% 190009 [?] ?
% 190036 [?] ?
% 190040 [?] ?
% 190043 [?] ?
% 190047 [?] ?
% 190109 [?] ?
% 190135 [?] ?
% 190154 [?] ?
% 190171 [?] ?
% 190279 [?] ?
% 190286 [?] ?
% 190297 [?] ?
% 190303 [?] ?
% 190348 [?] ?
% 190482 [?] ?
% 190486 [?] ?
% 190548 [?] ?
% 190555 [?] ?
% 190558 [?] ?
% 190564 [?] ?
% 190747 [?] ?
% 190761 [?] ?
% 190774 [?] ?
% 190808 [?] ?
% 190809 [] ss^nder1_0(0).
% 190811 [?] ?
% 190821 [?] ?
% 190828 [?] ?
% 190830 [?] ?
% 190834 [?] ?
% 190838 [input:190808,cut:190809] ss^nder1_1r1(X).
% 190847 [input:190811,cut:190809,cut:181777,cut:181756] -ss^pv24_5r1r1r1r1r1(X,Y,Z,U,skc47) | -ss^nder1_1r1(X).
% 190879 [input:190774,cut:190809,cut:181817,cut:181777,cut:181756] $ganappred6($ganc9,X,Y,Z,U,V,skc44) | -ss^nder1_1r1(X).
% 190880 [input:190821,cut:190809,cut:182895,cut:182681,cut:182475,cut:182362,cut:182176,cut:182018,cut:181943,cut:181868,cut:181817,cut:181777,cut:181756] -$ganappred14($ganc159,X,Y,Z,U,V,W,X1,X2,X3,X4,X5,X6,X7,skc37) | -ss^nder1_1r1(X).
% 190900 [input:190761,cut:190809,cut:181868,cut:181817,cut:181777,cut:181756] $ganappred7($ganc22,X,Y,Z,U,V,W,skc42) | -ss^nder1_1r1(X).
% 190908 [input:190828,cut:190809,cut:186807,cut:185361,cut:184346,cut:183800,cut:183514,cut:183297,cut:183101,cut:182895,cut:182681,cut:182475,cut:182362,cut:182176,cut:182018,cut:181943,cut:181868,cut:181817,cut:181777,cut:181756] -$ganappred21($ganc317,X,Y,Z,U,V,W,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,skc31) | -ss^nder1_1r1(X).
% 190914 [input:190830,cut:190809,cut:187363,cut:186807,cut:185361,cut:184346,cut:183800,cut:183514,cut:183297,cut:183101,cut:182895,cut:182681,cut:182475,cut:182362,cut:182176,cut:182018,cut:181943,cut:181868,cut:181817,cut:181777,cut:181756] -$ganappred22($ganc345,X,Y,Z,U,V,W,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,skc29) | -ss^nder1_1r1(X).
% 190921 [input:190747,cut:190809,cut:181943,cut:181868,cut:181817,cut:181777,cut:181756] $ganappred8($ganc35,X,Y,Z,U,V,W,X1,skc40) | -ss^nder1_1r1(X).
% 190926 [input:190834,cut:190809,cut:187877,cut:187363,cut:186807,cut:185361,cut:184346,cut:183800,cut:183514,cut:183297,cut:183101,cut:182895,cut:182681,cut:182475,cut:182362,cut:182176,cut:182018,cut:181943,cut:181868,cut:181817,cut:181777,cut:181756] -$ganappred24($ganc398,X,Y,Z,U,V,W,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,skc25) | -$ganappred21($ganc344,X,Y,Z,U,V,W,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15) | -ss^nder1_1r1(X).
% 191061 [input:189891,cut:190809,cut:188600,cut:188212,cut:187959,cut:187877,cut:187363,cut:186807,cut:185361,cut:184346,cut:183800,cut:183514,cut:183297,cut:183101,cut:182895,cut:182681,cut:182475,cut:182362,cut:182176,cut:182018,cut:181943,cut:181868,cut:181817,cut:181777,cut:181756] -$ganappred26($ganc488,X,Y,Z,U,V,W,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) | -$ganappred26($ganc536,X,Y,Z,U,V,W,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) | -$ganappred26($ganc504,X,Y,Z,U,V,W,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) | $ganappred26($ganc484,X,Y,Z,U,V,W,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) | -$ganappred21($ganc344,X,Y,Z,U,V,W,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15) | -ss^nder1_1r1(X).
% 191086 [input:189895,cut:190809,cut:188600,cut:188212,cut:187959,cut:187877,cut:187363,cut:186807,cut:185361,cut:184346,cut:183800,cut:183514,cut:183297,cut:183101,cut:182895,cut:182681,cut:182475,cut:182362,cut:182176,cut:182018,cut:181943,cut:181868,cut:181817,cut:181777,cut:181756] -$ganappred26($ganc490,X,Y,Z,U,V,W,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) | $ganappred26($ganc536,X,Y,Z,U,V,W,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) | $ganappred26($ganc505,X,Y,Z,U,V,W,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) | $ganappred26($ganc486,X,Y,Z,U,V,W,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) | -$ganappred21($ganc344,X,Y,Z,U,V,W,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15) | -ss^nder1_1r1(X).
% 191168 [input:190564,cut:190809,cut:183101,cut:182895,cut:182681,cut:182475,cut:182362,cut:182176,cut:182018,cut:181943,cut:181868,cut:181817,cut:181777,cut:181756] -$ganappred14($ganc188,X,Y,Z,U,V,W,X1,X2,X3,X4,X5,X6,X7,X8) | ss^pv26_3r1r1r1(X,Y,Z) | -ss^nder1_1r1(X).
% 191227 [input:190548,cut:190809,cut:183101,cut:182895,cut:182681,cut:182475,cut:182362,cut:182176,cut:182018,cut:181943,cut:181868,cut:181817,cut:181777,cut:181756] -$ganappred14($ganc198,X,Y,Z,U,V,W,X1,X2,X3,X4,X5,X6,X7,X8) | $ganappred9($ganc113,X,Y,Z,U,V,W,X1,X2,X3) | -ss^nder1_1r1(X).
% 191253 [input:190555,cut:190809,cut:183101,cut:182895,cut:182681,cut:182475,cut:182362,cut:182176,cut:182018,cut:181943,cut:181868,cut:181817,cut:181777,cut:181756] $ganappred14($ganc192,X,Y,Z,U,V,W,X1,X2,X3,X4,X5,X6,X7,X8) | -$ganappred7($ganc22,X,Y,Z,U,V,W,X1) | -ss^nder1_1r1(X).
% 191256 [input:190558,cut:190809,cut:183101,cut:182895,cut:182681,cut:182475,cut:182362,cut:182176,cut:182018,cut:181943,cut:181868,cut:181817,cut:181777,cut:181756] $ganappred14($ganc191,X,Y,Z,U,V,W,X1,X2,X3,X4,X5,X6,X7,X8) | -$ganappred6($ganc9,X,Y,Z,U,V,W) | -ss^nder1_1r1(X).
% 191413 [input:190482,cut:190809,cut:183101,cut:182895,cut:182681,cut:182475,cut:182362,cut:182176,cut:182018,cut:181943,cut:181868,cut:181817,cut:181777,cut:181756] -$ganappred14($ganc191,X,Y,Z,U,V,W,X1,X2,X3,X4,X5,X6,X7,X8) | -$ganappred14($ganc187,X,Y,Z,U,V,W,X1,X2,X3,X4,X5,X6,X7,X8) | $ganappred14($ganc198,X,Y,Z,U,V,W,X1,X2,X3,X4,X5,X6,X7,X8) | $ganappred14($ganc159,X,Y,Z,U,V,W,X1,X2,X3,X4,X5,X6,X7,X8) | -ss^nder1_1r1(X).
% 191414 [binary:191256,191413] -$ganappred14($ganc187,X,Y,Z,U,V,W,X1,X2,X3,X4,X5,X6,X7,X8) | $ganappred14($ganc159,X,Y,Z,U,V,W,X1,X2,X3,X4,X5,X6,X7,X8) | $ganappred14($ganc198,X,Y,Z,U,V,W,X1,X2,X3,X4,X5,X6,X7,X8) | -$ganappred6($ganc9,X,Y,Z,U,V,W) | -ss^nder1_1r1(X).
% 191441 [input:190486,cut:190809,cut:183101,cut:182895,cut:182681,cut:182475,cut:182362,cut:182176,cut:182018,cut:181943,cut:181868,cut:181817,cut:181777,cut:181756] -$ganappred14($ganc192,X,Y,Z,U,V,W,X1,X2,X3,X4,X5,X6,X7,X8) | $ganappred14($ganc159,X,Y,Z,U,V,W,X1,X2,X3,X4,X5,X6,X7,X8) | $ganappred14($ganc187,X,Y,Z,U,V,W,X1,X2,X3,X4,X5,X6,X7,X8) | $ganappred14($ganc188,X,Y,Z,U,V,W,X1,X2,X3,X4,X5,X6,X7,X8) | -ss^nder1_1r1(X).
% 191442 [binary:191253,191441] $ganappred14($ganc188,X,Y,Z,U,V,W,X1,X2,X3,X4,X5,X6,X7,X8) | $ganappred14($ganc159,X,Y,Z,U,V,W,X1,X2,X3,X4,X5,X6,X7,X8) | $ganappred14($ganc187,X,Y,Z,U,V,W,X1,X2,X3,X4,X5,X6,X7,X8) | -$ganappred7($ganc22,X,Y,Z,U,V,W,X1) | -ss^nder1_1r1(X).
% 191444 [binary:191168,191442] $ganappred14($ganc159,X,Y,Z,U,V,W,X1,X2,X3,X4,X5,X6,X7,X8) | $ganappred14($ganc187,X,Y,Z,U,V,W,X1,X2,X3,X4,X5,X6,X7,X8) | -$ganappred7($ganc22,X,Y,Z,U,V,W,X1) | ss^pv26_3r1r1r1(X,Y,Z) | -ss^nder1_1r1(X).
% 191446 [binary:190880,191444] $ganappred14($ganc187,X,Y,Z,U,V,W,X1,X2,X3,X4,X5,X6,X7,skc37) | -$ganappred7($ganc22,X,Y,Z,U,V,W,X1) | ss^pv26_3r1r1r1(X,Y,Z) | -ss^nder1_1r1(X).
% 191451 [binary:191414,191446,cut:182898] $ganappred14($ganc198,X,Y,Z,U,V,W,X1,X2,X3,X4,X5,X6,X7,skc37) | -$ganappred7($ganc22,X,Y,Z,U,V,W,X1) | -$ganappred6($ganc9,X,Y,Z,U,V,W) | ss^pv26_3r1r1r1(X,Y,Z) | -ss^nder1_1r1(X).
% 191457 [binary:191227,191451] $ganappred9($ganc113,X,Y,Z,U,V,W,X1,X2,X3) | -$ganappred7($ganc22,X,Y,Z,U,V,W,X1) | -$ganappred6($ganc9,X,Y,Z,U,V,W) | ss^pv26_3r1r1r1(X,Y,Z) | -ss^nder1_1r1(X).
% 191740 [input:190297,cut:190809,cut:187363,cut:186807,cut:185361,cut:184346,cut:183800,cut:183514,cut:183297,cut:183101,cut:182895,cut:182681,cut:182475,cut:182362,cut:182176,cut:182018,cut:181943,cut:181868,cut:181817,cut:181777,cut:181756] $ganappred21($ganc348,X,Y,Z,U,V,W,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15) | -ss^pv26_3r1r1r1(X,Y,Z) | -ss^nder1_1r1(X).
% 191746 [input:190303,cut:190809,cut:187363,cut:186807,cut:185361,cut:184346,cut:183800,cut:183514,cut:183297,cut:183101,cut:182895,cut:182681,cut:182475,cut:182362,cut:182176,cut:182018,cut:181943,cut:181868,cut:181817,cut:181777,cut:181756] $ganappred21($ganc344,X,Y,Z,U,V,W,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15) | -ss^nder1_1r1(X).
% 191783 [input:190003,cut:190809,cut:188600,cut:188212,cut:187959,cut:187877,cut:187363,cut:186807,cut:185361,cut:184346,cut:183800,cut:183514,cut:183297,cut:183101,cut:182895,cut:182681,cut:182475,cut:182362,cut:182176,cut:182018,cut:181943,cut:181868,cut:181817,cut:181777,cut:181756] -$ganappred26($ganc505,X,Y,Z,U,V,W,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) | $ganappred22($ganc345,X,Y,Z,U,V,W,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16) | -$ganappred21($ganc344,X,Y,Z,U,V,W,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15) | -ss^nder1_1r1(X).
% 191803 [input:190006,cut:190809,cut:188600,cut:188212,cut:187959,cut:187877,cut:187363,cut:186807,cut:185361,cut:184346,cut:183800,cut:183514,cut:183297,cut:183101,cut:182895,cut:182681,cut:182475,cut:182362,cut:182176,cut:182018,cut:181943,cut:181868,cut:181817,cut:181777,cut:181756] $ganappred26($ganc504,X,Y,Z,U,V,W,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) | -$ganappred21($ganc317,X,Y,Z,U,V,W,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15) | -$ganappred21($ganc344,X,Y,Z,U,V,W,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15) | -ss^nder1_1r1(X).
% 191819 [input:190009,cut:190809,cut:187959,cut:187877,cut:187363,cut:186807,cut:185361,cut:184346,cut:183800,cut:183514,cut:183297,cut:183101,cut:182895,cut:182681,cut:182475,cut:182362,cut:182176,cut:182018,cut:181943,cut:181868,cut:181817,cut:181777,cut:181756] -$ganappred24($ganc438,X,Y,Z,U,V,W,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18) | -$ganappred24($ganc429,X,Y,Z,U,V,W,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18) | $ganappred24($ganc451,X,Y,Z,U,V,W,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18) | $ganappred24($ganc398,X,Y,Z,U,V,W,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18) | -$ganappred21($ganc344,X,Y,Z,U,V,W,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15) | -ss^nder1_1r1(X).
% 191822 [input:190348,cut:190809,cut:186807,cut:185361,cut:184346,cut:183800,cut:183514,cut:183297,cut:183101,cut:182895,cut:182681,cut:182475,cut:182362,cut:182176,cut:182018,cut:181943,cut:181868,cut:181817,cut:181777,cut:181756] $ganappred21($ganc317,X,Y,Z,U,V,W,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,skc30) | -ss^nder1_1r1(X).
% 191863 [input:190279,cut:190809,cut:187363,cut:186807,cut:185361,cut:184346,cut:183800,cut:183514,cut:183297,cut:183101,cut:182895,cut:182681,cut:182475,cut:182362,cut:182176,cut:182018,cut:181943,cut:181868,cut:181817,cut:181777,cut:181756] -$ganappred21($ganc357,X,Y,Z,U,V,W,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15) | $ganappred12($ganc182,X,Y,Z,U,V,W,X1,X2,X3,X4,X5,X6) | -ss^nder1_1r1(X).
% 191872 [input:190286,cut:190809,cut:187363,cut:186807,cut:185361,cut:184346,cut:183800,cut:183514,cut:183297,cut:183101,cut:182895,cut:182681,cut:182475,cut:182362,cut:182176,cut:182018,cut:181943,cut:181868,cut:181817,cut:181777,cut:181756] $ganappred21($ganc353,X,Y,Z,U,V,W,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15) | -$ganappred8($ganc35,X,Y,Z,U,V,W,X1,X2) | -ss^nder1_1r1(X).
% 191959 [input:190154,cut:190809,cut:187959,cut:187877,cut:187363,cut:186807,cut:185361,cut:184346,cut:183800,cut:183514,cut:183297,cut:183101,cut:182895,cut:182681,cut:182475,cut:182362,cut:182176,cut:182018,cut:181943,cut:181868,cut:181817,cut:181777,cut:181756] $ganappred24($ganc429,X,Y,Z,U,V,W,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18) | -$ganappred21($ganc344,X,Y,Z,U,V,W,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15) | -ss^pv26_3r1r1r1(X,Y,Z) | -ss^nder1_1r1(X).
% 191968 [input:190036,cut:190809,cut:188600,cut:188212,cut:187959,cut:187877,cut:187363,cut:186807,cut:185361,cut:184346,cut:183800,cut:183514,cut:183297,cut:183101,cut:182895,cut:182681,cut:182475,cut:182362,cut:182176,cut:182018,cut:181943,cut:181868,cut:181817,cut:181777,cut:181756] $ganappred26($ganc490,X,Y,Z,U,V,W,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) | -$ganappred21($ganc344,X,Y,Z,U,V,W,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15) | -$ganappred9($ganc113,X,Y,Z,U,V,W,X1,X2,X3) | -ss^nder1_1r1(X).
% 191969 [binary:191086,191968] $ganappred26($ganc486,X,Y,Z,U,V,W,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) | $ganappred26($ganc536,X,Y,Z,U,V,W,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) | $ganappred26($ganc505,X,Y,Z,U,V,W,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) | -$ganappred21($ganc344,X,Y,Z,U,V,W,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15) | -$ganappred9($ganc113,X,Y,Z,U,V,W,X1,X2,X3) | -ss^nder1_1r1(X).
% 191982 [input:190171,cut:190809,cut:187363,cut:186807,cut:185361,cut:184346,cut:183800,cut:183514,cut:183297,cut:183101,cut:182895,cut:182681,cut:182475,cut:182362,cut:182176,cut:182018,cut:181943,cut:181868,cut:181817,cut:181777,cut:181756] -$ganappred21($ganc348,X,Y,Z,U,V,W,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15) | -$ganappred21($ganc353,X,Y,Z,U,V,W,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15) | $ganappred21($ganc357,X,Y,Z,U,V,W,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15) | $ganappred21($ganc317,X,Y,Z,U,V,W,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15) | -ss^nder1_1r1(X).
% 191983 [binary:191740,191982] -$ganappred21($ganc353,X,Y,Z,U,V,W,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15) | $ganappred21($ganc317,X,Y,Z,U,V,W,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15) | $ganappred21($ganc357,X,Y,Z,U,V,W,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15) | -ss^pv26_3r1r1r1(X,Y,Z) | -ss^nder1_1r1(X).
% 191985 [binary:191872,191983] $ganappred21($ganc317,X,Y,Z,U,V,W,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15) | $ganappred21($ganc357,X,Y,Z,U,V,W,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15) | -$ganappred8($ganc35,X,Y,Z,U,V,W,X1,X2) | -ss^pv26_3r1r1r1(X,Y,Z) | -ss^nder1_1r1(X).
% 191987 [binary:190908,191985] $ganappred21($ganc357,X,Y,Z,U,V,W,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,skc31) | -$ganappred8($ganc35,X,Y,Z,U,V,W,X1,X2) | -ss^pv26_3r1r1r1(X,Y,Z) | -ss^nder1_1r1(X).
% 191989 [binary:191863,191987] $ganappred12($ganc182,X,Y,Z,U,V,W,X1,X2,X3,X4,X5,X6) | -$ganappred8($ganc35,X,Y,Z,U,V,W,X1,X2) | -ss^pv26_3r1r1r1(X,Y,Z) | -ss^nder1_1r1(X).
% 191994 [input:190040,cut:190809,cut:188600,cut:188212,cut:187959,cut:187877,cut:187363,cut:186807,cut:185361,cut:184346,cut:183800,cut:183514,cut:183297,cut:183101,cut:182895,cut:182681,cut:182475,cut:182362,cut:182176,cut:182018,cut:181943,cut:181868,cut:181817,cut:181777,cut:181756] $ganappred26($ganc488,X,Y,Z,U,V,W,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) | -$ganappred21($ganc344,X,Y,Z,U,V,W,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15) | -$ganappred7($ganc22,X,Y,Z,U,V,W,X1) | -ss^nder1_1r1(X).
% 191995 [binary:191061,191994] -$ganappred26($ganc536,X,Y,Z,U,V,W,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) | -$ganappred26($ganc504,X,Y,Z,U,V,W,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) | $ganappred26($ganc484,X,Y,Z,U,V,W,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) | -$ganappred21($ganc344,X,Y,Z,U,V,W,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15) | -$ganappred7($ganc22,X,Y,Z,U,V,W,X1) | -ss^nder1_1r1(X).
% 192022 [input:190043,cut:190809,cut:188600,cut:188212,cut:187959,cut:187877,cut:187363,cut:186807,cut:185361,cut:184346,cut:183800,cut:183514,cut:183297,cut:183101,cut:182895,cut:182681,cut:182475,cut:182362,cut:182176,cut:182018,cut:181943,cut:181868,cut:181817,cut:181777,cut:181756] -$ganappred26($ganc486,X,Y,Z,U,V,W,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) | -$ganappred21($ganc344,X,Y,Z,U,V,W,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15) | ss^pv24_5r1r1r1r1r1(X,Y,Z,U,V) | -ss^nder1_1r1(X).
% 192023 [binary:191969,192022] $ganappred26($ganc536,X,Y,Z,U,V,W,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) | $ganappred26($ganc505,X,Y,Z,U,V,W,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) | -$ganappred21($ganc344,X,Y,Z,U,V,W,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15) | -$ganappred9($ganc113,X,Y,Z,U,V,W,X1,X2,X3) | ss^pv24_5r1r1r1r1r1(X,Y,Z,U,V) | -ss^nder1_1r1(X).
% 192025 [binary:191995,192023] -$ganappred26($ganc504,X,Y,Z,U,V,W,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) | $ganappred26($ganc484,X,Y,Z,U,V,W,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) | $ganappred26($ganc505,X,Y,Z,U,V,W,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) | -$ganappred21($ganc344,X,Y,Z,U,V,W,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15) | -$ganappred9($ganc113,X,Y,Z,U,V,W,X1,X2,X3) | -$ganappred7($ganc22,X,Y,Z,U,V,W,X1) | ss^pv24_5r1r1r1r1r1(X,Y,Z,U,V) | -ss^nder1_1r1(X).
% 192028 [binary:191803,192025] $ganappred26($ganc484,X,Y,Z,U,V,W,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) | $ganappred26($ganc505,X,Y,Z,U,V,W,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) | -$ganappred21($ganc344,X,Y,Z,U,V,W,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15) | -$ganappred21($ganc317,X,Y,Z,U,V,W,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15) | -$ganappred9($ganc113,X,Y,Z,U,V,W,X1,X2,X3) | -$ganappred7($ganc22,X,Y,Z,U,V,W,X1) | ss^pv24_5r1r1r1r1r1(X,Y,Z,U,V) | -ss^nder1_1r1(X).
% 192062 [input:190047,cut:190809,cut:188600,cut:188212,cut:187959,cut:187877,cut:187363,cut:186807,cut:185361,cut:184346,cut:183800,cut:183514,cut:183297,cut:183101,cut:182895,cut:182681,cut:182475,cut:182362,cut:182176,cut:182018,cut:181943,cut:181868,cut:181817,cut:181777,cut:181756] -$ganappred26($ganc484,X,Y,Z,U,V,W,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) | -$ganappred21($ganc344,X,Y,Z,U,V,W,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15) | ss^pv26_3r1r1r1(X,Y,Z) | -ss^nder1_1r1(X).
% 192064 [binary:192028,192062] $ganappred26($ganc505,X,Y,Z,U,V,W,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) | -$ganappred21($ganc344,X,Y,Z,U,V,W,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15) | -$ganappred21($ganc317,X,Y,Z,U,V,W,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15) | -$ganappred9($ganc113,X,Y,Z,U,V,W,X1,X2,X3) | -$ganappred7($ganc22,X,Y,Z,U,V,W,X1) | ss^pv24_5r1r1r1r1r1(X,Y,Z,U,V) | ss^pv26_3r1r1r1(X,Y,Z) | -ss^nder1_1r1(X).
% 192075 [binary:191783,192064] $ganappred22($ganc345,X,Y,Z,U,V,W,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16) | -$ganappred21($ganc344,X,Y,Z,U,V,W,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15) | -$ganappred21($ganc317,X,Y,Z,U,V,W,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15) | -$ganappred9($ganc113,X,Y,Z,U,V,W,X1,X2,X3) | -$ganappred7($ganc22,X,Y,Z,U,V,W,X1) | ss^pv24_5r1r1r1r1r1(X,Y,Z,U,V) | ss^pv26_3r1r1r1(X,Y,Z) | -ss^nder1_1r1(X).
% 192079 [binary:190914,192075] -$ganappred21($ganc317,X,Y,Z,U,V,W,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15) | -$ganappred21($ganc344,X,Y,Z,U,V,W,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15) | -$ganappred9($ganc113,X,Y,Z,U,V,W,X1,X2,X3) | -$ganappred7($ganc22,X,Y,Z,U,V,W,X1) | ss^pv24_5r1r1r1r1r1(X,Y,Z,U,V) | ss^pv26_3r1r1r1(X,Y,Z) | -ss^nder1_1r1(X).
% 192081 [binary:191822,192079] -$ganappred21($ganc344,X,Y,Z,U,V,W,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,skc30) | -$ganappred9($ganc113,X,Y,Z,U,V,W,X1,X2,X3) | -$ganappred7($ganc22,X,Y,Z,U,V,W,X1) | ss^pv24_5r1r1r1r1r1(X,Y,Z,U,V) | ss^pv26_3r1r1r1(X,Y,Z) | -ss^nder1_1r1(X).
% 192083 [binary:191746,192081] -$ganappred9($ganc113,X,Y,Z,U,V,W,X1,X2,X3) | -$ganappred7($ganc22,X,Y,Z,U,V,W,X1) | ss^pv24_5r1r1r1r1r1(X,Y,Z,U,V) | ss^pv26_3r1r1r1(X,Y,Z) | -ss^nder1_1r1(X).
% 192087 [binary:191457,192083] -$ganappred7($ganc22,X,Y,Z,U,V,W,X1) | -$ganappred6($ganc9,X,Y,Z,U,V,W) | ss^pv24_5r1r1r1r1r1(X,Y,Z,U,V) | ss^pv26_3r1r1r1(X,Y,Z) | -ss^nder1_1r1(X).
% 192094 [binary:190900,192087] -$ganappred6($ganc9,X,Y,Z,U,V,W) | ss^pv24_5r1r1r1r1r1(X,Y,Z,U,V) | ss^pv26_3r1r1r1(X,Y,Z) | -ss^nder1_1r1(X).
% 192096 [binary:190879,192094] ss^pv24_5r1r1r1r1r1(X,Y,Z,U,V) | ss^pv26_3r1r1r1(X,Y,Z) | -ss^nder1_1r1(X).
% 192098 [binary:190847,192096] ss^pv26_3r1r1r1(X,Y,Z) | -ss^nder1_1r1(X).
% 192297 [input:190109,cut:190809,cut:187959,cut:187877,cut:187363,cut:186807,cut:185361,cut:184346,cut:183800,cut:183514,cut:183297,cut:183101,cut:182895,cut:182681,cut:182475,cut:182362,cut:182176,cut:182018,cut:181943,cut:181868,cut:181817,cut:181777,cut:181756] -$ganappred24($ganc451,X,Y,Z,U,V,W,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18) | $ganappred22($ganc345,X,Y,Z,U,V,W,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16) | -$ganappred21($ganc344,X,Y,Z,U,V,W,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15) | -ss^nder1_1r1(X).
% 192453 [input:190135,cut:190809,cut:187959,cut:187877,cut:187363,cut:186807,cut:185361,cut:184346,cut:183800,cut:183514,cut:183297,cut:183101,cut:182895,cut:182681,cut:182475,cut:182362,cut:182176,cut:182018,cut:181943,cut:181868,cut:181817,cut:181777,cut:181756] $ganappred24($ganc438,X,Y,Z,U,V,W,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18) | -$ganappred21($ganc344,X,Y,Z,U,V,W,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15) | -$ganappred12($ganc182,X,Y,Z,U,V,W,X1,X2,X3,X4,X5,X6) | -ss^nder1_1r1(X).
% 192454 [binary:191819,192453] -$ganappred24($ganc429,X,Y,Z,U,V,W,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18) | $ganappred24($ganc398,X,Y,Z,U,V,W,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18) | $ganappred24($ganc451,X,Y,Z,U,V,W,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18) | -$ganappred21($ganc344,X,Y,Z,U,V,W,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15) | -$ganappred12($ganc182,X,Y,Z,U,V,W,X1,X2,X3,X4,X5,X6) | -ss^nder1_1r1(X).
% 192458 [binary:191959,192454,binarycut:192098] $ganappred24($ganc451,X,Y,Z,U,V,W,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18) | $ganappred24($ganc398,X,Y,Z,U,V,W,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18) | -$ganappred21($ganc344,X,Y,Z,U,V,W,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15) | -$ganappred12($ganc182,X,Y,Z,U,V,W,X1,X2,X3,X4,X5,X6) | -ss^nder1_1r1(X).
% 192461 [binary:192297,192458] $ganappred24($ganc398,X,Y,Z,U,V,W,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18) | $ganappred22($ganc345,X,Y,Z,U,V,W,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16) | -$ganappred21($ganc344,X,Y,Z,U,V,W,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15) | -$ganappred12($ganc182,X,Y,Z,U,V,W,X1,X2,X3,X4,X5,X6) | -ss^nder1_1r1(X).
% 192465 [binary:190926,192461] $ganappred22($ganc345,X,Y,Z,U,V,W,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16) | -$ganappred21($ganc344,X,Y,Z,U,V,W,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15) | -$ganappred12($ganc182,X,Y,Z,U,V,W,X1,X2,X3,X4,X5,X6) | -ss^nder1_1r1(X).
% 192467 [binary:190914,192465] -$ganappred21($ganc344,X,Y,Z,U,V,W,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15) | -$ganappred12($ganc182,X,Y,Z,U,V,W,X1,X2,X3,X4,X5,X6) | -ss^nder1_1r1(X).
% 192469 [binary:191746,192467] -$ganappred12($ganc182,X,Y,Z,U,V,W,X1,X2,X3,X4,X5,X6) | -ss^nder1_1r1(X).
% 192473 [binary:191989,192469,binarycut:192098] -$ganappred8($ganc35,X,Y,Z,U,V,W,X1,X2) | -ss^nder1_1r1(X).
% 192475 [binary:190921,192473] -ss^nder1_1r1(X).
% 192476 [binary:190838,192475] contradiction
% END OF PROOF
%
% Proof found by the following strategy:
%
% using binary resolution
% using weight-order strategy
% not using sos strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% using clause demodulation
% seconds given: 30
%
%
% ***GANDALF_FOUND_A_REFUTATION***
%
% Global statistics over all passes:
%
% given clauses: 60778
% derived clauses: 389450
% kept clauses: 75966
% kept size sum: 432848
% kept mid-nuclei: 26941
% kept new demods: 0
% forw unit-subs: 21586
% forw double-subs: 50002
% forw overdouble-subs: 144973
% backward subs: 27653
% fast unit cutoff: 81461
% full unit cutoff: 4
% dbl unit cutoff: 316
% real runtime: 241.94
% process. runtime: 241.29
% specific non-discr-tree subsumption statistics:
% tried: 28674938
% length fails: 408351
% strength fails: 3303230
% predlist fails: 664010
% aux str. fails: 436931
% by-lit fails: 19962707
% full subs tried: 1461654
% full subs fail: 1315875
%
% ; 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/SYN/SYN848-1+noeq.in")
%
%------------------------------------------------------------------------------