%------------------------------------------------------------------------------
% File : Gandalf---c-2.6
% Problem : SWC252-1 : TPTP v3.4.2. Released v2.4.0.
% Transfm : add_equality:r
% Format : otter:hypothesis:set(auto),clear(print_given)
% Command : gandalf-wrapper -time %d %s
% Computer : art06.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 378.8s
% Output : Assurance 378.8s
% 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/SWC/SWC252-1+eq_r.in
% Using automatic strategy selection.
% Time limit in seconds: 600
%
% prove-all-passes started
%
% detected problem class: neq
% detected subclass: big
%
% strategies selected:
% (hyper 28 #f 5 19)
% (binary-unit 28 #f 5 19)
% (binary-double 11 #f 5 19)
% (binary-double 17 #f)
% (binary-double 17 #t)
% (binary 87 #t 5 19)
% (binary-order 28 #f 5 19)
% (binary-posweight-order 58 #f)
% (binary-posweight-lex-big-order 28 #f)
% (binary-posweight-lex-small-order 11 #f)
% (binary-order-sos 28 #t)
% (binary-unit-uniteq 28 #f)
% (binary-weightorder 28 #f)
% (binary-weightorder-sos 17 #f)
% (binary-order 28 #f)
% (hyper-order 17 #f)
% (binary 141 #t)
%
%
% ********* EMPTY CLAUSE DERIVED *********
%
%
% timer checkpoints: c(204,40,1,408,0,1,54251,4,2170,61750,5,2802,61751,1,2803,61751,50,2806,61751,40,2806,61955,0,2807,148500,3,4208,165158,4,4909,183269,5,5623,183269,5,5624,183269,1,5624,183269,50,5628,183269,40,5628,183473,0,5628,224870,3,6180,239587,4,6454,252304,5,6729,252304,5,6730,252305,1,6730,252305,50,6732,252305,40,6732,252509,0,6733,312693,3,7586,330275,4,8010,351284,62,8434,351285,5,8435,351286,1,8435,351286,50,8437,351286,40,8437,351490,0,8437,410742,3,9292,430585,4,9713,443404,5,10138,443404,5,10140,443405,1,10140,443405,50,10143,443405,40,10143,443609,0,10143,713330,3,14495,800600,4,16669,906285,5,18844,906285,5,18846,906286,1,18846,906286,50,18849,906286,40,18849,906490,0,18849,949964,3,20250,950956,4,20950,957123,5,21650,957124,1,21650,957124,50,21651,957124,40,21651,957328,0,21651,1176523,3,24553,1278495,4,26002,1335504,1,27452,1335504,50,27458,1335504,40,27458,1335708,0,27490,1490286,3,28891,1526933,4,29591,1573173,62,30291,1573173,5,30292,1573174,1,30292,1573174,50,30298,1573174,40,30298,1573378,0,30336,1623294,3,30905,1638532,4,31163,1683885,5,31437,1683885,1,31437,1683885,50,31442,1683885,40,31442,1684089,0,31443,1729446,3,32844,1731816,4,33544,1738938,1,34244,1738938,50,34245,1738938,40,34245,1739142,0,34245,1835181,3,35646,1905962,4,36346,1930553,5,37047,1930553,5,37048,1930553,1,37048,1930553,50,37050,1930553,40,37050,1930757,0,37050)
%
%
% START OF PROOF
% 1930554 [] equal(X,X).
% 1930562 [] ss^list(nil).
% 1930566 [] ss^item(skaf83(X)).
% 1930567 [] ss^list(skaf82(X)).
% 1930601 [] ss^item(skaf44(X)).
% 1930604 [] ss^list(skaf46(X,Y)).
% 1930605 [] ss^list(skaf45(X,Y)).
% 1930612 [] rearseg^p(X,nil) | -ss^list(X).
% 1930613 [] rearseg^p(X,X) | -ss^list(X).
% 1930614 [] frontseg^p(X,nil) | -ss^list(X).
% 1930615 [] frontseg^p(X,X) | -ss^list(X).
% 1930625 [] -member^p(nil,X) | -ss^item(X).
% 1930626 [] -ss^list(X) | ss^item(Y) | duplicatefree^p(X).
% 1930627 [] equal(app(X,nil),X) | -ss^list(X).
% 1930628 [] equal(app(nil,X),X) | -ss^list(X).
% 1930635 [] -equal(nil,X) | rearseg^p(nil,X) | -ss^list(X).
% 1930636 [] -rearseg^p(nil,X) | equal(nil,X) | -ss^list(X).
% 1930639 [] ss^list(app(X,Y)) | -ss^list(X) | -ss^list(Y).
% 1930640 [] ss^list(cons(X,Y)) | -ss^item(X) | -ss^list(Y).
% 1930650 [] equal(tl(cons(X,Y)),Y) | -ss^item(X) | -ss^list(Y).
% 1930651 [] equal(hd(cons(X,Y)),X) | -ss^item(X) | -ss^list(Y).
% 1930655 [] equal(cons(skaf44(X),nil),X) | -singleton^p(X) | -ss^list(X).
% 1930658 [] equal(cons(hd(X),tl(X)),X) | equal(nil,X) | -ss^list(X).
% 1930663 [] equal(cons(skaf83(X),skaf82(X)),X) | equal(nil,X) | -ss^list(X).
% 1930670 [] -equal(cons(X,nil),Y) | -ss^item(X) | -ss^list(Y) | singleton^p(Y).
% 1930674 [] equal(app(cons(X,nil),Y),cons(X,Y)) | -ss^item(X) | -ss^list(Y).
% 1930682 [] -rearseg^p(X,Y) | -rearseg^p(Y,X) | equal(Y,X) | -ss^list(Y) | -ss^list(X).
% 1930685 [] equal(app(skaf46(X,Y),Y),X) | -rearseg^p(X,Y) | -ss^list(X) | -ss^list(Y).
% 1930686 [] equal(app(X,skaf45(Y,X)),Y) | -frontseg^p(Y,X) | -ss^list(Y) | -ss^list(X).
% 1930687 [] equal(tl(app(X,Y)),app(tl(X),Y)) | equal(nil,X) | -ss^list(Y) | -ss^list(X).
% 1930690 [] rearseg^p(app(X,Y),Z) | -rearseg^p(Y,Z) | -ss^list(Y) | -ss^list(Z) | -ss^list(X).
% 1930691 [] frontseg^p(app(X,Y),Z) | -frontseg^p(X,Z) | -ss^list(X) | -ss^list(Z) | -ss^list(Y).
% 1930692 [] member^p(cons(X,Y),Z) | -equal(Z,X) | -ss^item(Z) | -ss^item(X) | -ss^list(Y).
% 1930694 [] member^p(app(X,Y),Z) | -member^p(X,Z) | -ss^item(Z) | -ss^list(X) | -ss^list(Y).
% 1930697 [] -equal(app(X,Y),Z) | rearseg^p(Z,Y) | -ss^list(Z) | -ss^list(Y) | -ss^list(X).
% 1930698 [] -equal(app(X,Y),Z) | frontseg^p(Z,X) | -ss^list(Z) | -ss^list(X) | -ss^list(Y).
% 1930699 [] equal(app(X,Y),nil) | -equal(nil,X) | -equal(nil,Y) | -ss^list(X) | -ss^list(Y).
% 1930704 [] -equal(app(X,Y),app(X,Z)) | equal(Y,Z) | -ss^list(Z) | -ss^list(X) | -ss^list(Y).
% 1930707 [] -rearseg^p(Y,Z) | -rearseg^p(X,Y) | rearseg^p(X,Z) | -ss^list(X) | -ss^list(Y) | -ss^list(Z).
% 1930708 [] -frontseg^p(Y,Z) | -frontseg^p(X,Y) | frontseg^p(X,Z) | -ss^list(X) | -ss^list(Y) | -ss^list(Z).
% 1930715 [] -member^p(cons(X,Y),Z) | member^p(Y,Z) | equal(Z,X) | -ss^item(Z) | -ss^item(X) | -ss^list(Y).
% 1930733 [] -equal(app(app(X,cons(Y,Z)),cons(Y,U)),V) | -ss^item(Y) | -ss^list(V) | -ss^list(X) | -ss^list(U) | -ss^list(Z) | -duplicatefree^p(V).
% 1930740 [] ss^list(sk1).
% 1930742 [] ss^list(sk3).
% 1930745 [] equal(sk1,sk3).
% 1930746 [] -equal(nil,sk1).
% 1930748 [] -equal(app(app(X,cons(Y,nil)),Z),sk1) | member^p(X,sk5(Z,X,Y)) | -ss^item(Y) | -ss^list(Z) | -ss^list(X).
% 1930753 [] equal(nil,sk3) | ss^item(sk6).
% 1930756 [] equal(cons(sk6,nil),sk3) | equal(nil,sk3).
% 1930763 [input:1930639,factor] ss^list(app(X,X)) | -ss^list(X).
% 1930785 [input:1930687,factor] equal(tl(app(X,X)),app(tl(X),X)) | equal(nil,X) | -ss^list(X).
% 1930787 [input:1930690,factor:binarycut:1930613] rearseg^p(app(X,Y),Y) | -ss^list(Y) | -ss^list(X).
% 1930791 [input:1930690,factor:factor:factor:factor:binarycut:1930613] rearseg^p(app(X,X),X) | -ss^list(X).
% 1930793 [input:1930691,factor:binarycut:1930615] frontseg^p(app(X,Y),X) | -ss^list(X) | -ss^list(Y).
% 1930797 [input:1930691,factor:factor:factor:factor:binarycut:1930615] frontseg^p(app(X,X),X) | -ss^list(X).
% 1930798 [input:1930692,factor:cut:1930554] member^p(cons(X,Y),X) | -ss^item(X) | -ss^list(Y).
% 1930800 [input:1930694,factor] member^p(app(X,X),Y) | -member^p(X,Y) | -ss^item(Y) | -ss^list(X).
% 1930890 [input:1930733,factor:factor:factor:factor:factor:factor:factor] -equal(app(app(X,cons(Y,X)),cons(Y,X)),Z) | -ss^item(Y) | -ss^list(Z) | -ss^list(X) | -duplicatefree^p(Z).
% 1931537 [para:1930745.1.2,1930753.1.2,cut:1930746] ss^item(sk6).
% 1931722 [binary:1930626,1930763] duplicatefree^p(app(X,X)) | -ss^list(X) | ss^item(Y).
% 1931766 [para:1930756.1.1,1930650.1.1.1,cut:1931537,cut:1930562] equal(tl(sk3),nil) | equal(nil,sk3).
% 1931772 [para:1930745.1.2,1931766.1.1.1] equal(tl(sk1),nil) | equal(nil,sk3).
% 1931822 [para:1930655.1.1,1930748.1.1.1.2,cut:1930601] -equal(app(app(X,Y),Z),sk1) | member^p(X,sk5(Z,X,skaf44(Y))) | -singleton^p(Y) | -ss^list(Z) | -ss^list(X) | -ss^list(Y).
% 1931843 [para:1930655.1.1,1930651.1.1.1,cut:1930601,cut:1930562] equal(hd(X),skaf44(X)) | -singleton^p(X) | -ss^list(X).
% 1931872 [para:1930655.1.1,1930798.1.1,cut:1930601,cut:1930562] member^p(X,skaf44(X)) | -singleton^p(X) | -ss^list(X).
% 1931885 [para:1931772.1.1,1930658.1.1.2,cut:1930746,cut:1930740] equal(cons(hd(sk1),nil),sk1) | equal(nil,sk3).
% 1931969 [para:1930663.1.1,1930650.1.1.1,cut:1930566,cut:1930567] equal(tl(X),skaf82(X)) | equal(nil,X) | -ss^list(X).
% 1931972 [para:1930663.1.1,1930798.1.1,cut:1930566,cut:1930567] member^p(X,skaf83(X)) | equal(nil,X) | -ss^list(X).
% 1932034 [binary:1930756,1930670,cut:1931537,cut:1930742] equal(nil,sk3) | singleton^p(sk3).
% 1932052 [para:1930745.1.2,1932034.1.2,cut:1930746] singleton^p(sk3).
% 1932053 [para:1930745.1.2,1932052.1.1] singleton^p(sk1).
% 1932105 [para:1931969.1.1,1931766.1.1,cut:1930742] equal(skaf82(sk3),nil) | equal(nil,sk3).
% 1932106 [para:1931766.1.1,1931969.1.1,cut:1930742] equal(nil,skaf82(sk3)) | equal(nil,sk3).
% 1932127 [para:1932105.1.1,1930663.1.1.2,cut:1930742] equal(cons(skaf83(sk3),nil),sk3) | equal(nil,sk3).
% 1932133 [binary:1930635,1932106,cut:1930567] rearseg^p(nil,skaf82(sk3)) | equal(nil,sk3).
% 1932235 [para:1932127.1.1,1930651.1.1.1,cut:1930566,cut:1930562] equal(hd(sk3),skaf83(sk3)) | equal(nil,sk3).
% 1932236 [para:1932127.1.1,1930798.1.1,cut:1930566,cut:1930562] member^p(sk3,skaf83(sk3)) | equal(nil,sk3).
% 1932240 [para:1930745.1.2,1932236.1.2.1] member^p(sk3,skaf83(sk1)) | equal(nil,sk3).
% 1932249 [para:1930745.1.2,1932235.1.1.1] equal(hd(sk1),skaf83(sk3)) | equal(nil,sk3).
% 1932286 [para:1930685.1.1,1930627.1.1,cut:1930562,cut:1930604,binarycut:1930612] equal(X,skaf46(X,nil)) | -ss^list(X).
% 1932288 [para:1930627.1.1,1930685.1.1,cut:1930562,cut:1930604,binarycut:1930612] equal(skaf46(X,nil),X) | -ss^list(X).
% 1932330 [para:1930686.1.1,1930628.1.1,cut:1930562,cut:1930605,binarycut:1930614] equal(X,skaf45(X,nil)) | -ss^list(X).
% 1932332 [para:1930628.1.1,1930686.1.1,cut:1930562,cut:1930605,binarycut:1930614] equal(skaf45(X,nil),X) | -ss^list(X).
% 1932375 [para:1932249.1.1,1931885.1.1.1] equal(cons(skaf83(sk3),nil),sk1) | equal(nil,sk3).
% 1932409 [para:1930627.1.1,1930690.1.1,cut:1930562] -rearseg^p(nil,X) | rearseg^p(Y,X) | -ss^list(X) | -ss^list(Y).
% 1932512 [binary:1932133,1932409,cut:1930567] equal(nil,sk3) | rearseg^p(X,skaf82(sk3)) | -ss^list(X).
% 1932517 [para:1930745.1.2,1932512.1.2,cut:1930746] rearseg^p(X,skaf82(sk3)) | -ss^list(X).
% 1932532 [binary:1930636,1932517,cut:1930562,cut:1930567] equal(nil,skaf82(sk3)).
% 1932533 [para:1930745.1.2,1932532.1.2.1] equal(nil,skaf82(sk1)).
% 1932534 [para:1932533.1.2,1930663.1.1.2,cut:1930746,cut:1930740] equal(cons(skaf83(sk1),nil),sk1).
% 1932553 [para:1932534.1.1,1930650.1.1.1,cut:1930566,cut:1930562] equal(tl(sk1),nil).
% 1932554 [para:1932534.1.1,1930651.1.1.1,cut:1930566,cut:1930562] equal(hd(sk1),skaf83(sk1)).
% 1932557 [para:1932534.1.1,1930674.1.1.1,cut:1930566] equal(app(sk1,X),cons(skaf83(sk1),X)) | -ss^list(X).
% 1932559 [para:1932554.1.1,1931843.1.1,cut:1932053,cut:1930740] equal(skaf83(sk1),skaf44(sk1)).
% 1932591 [para:1930628.1.1,1930697.1.1,cut:1930562] -equal(X,Y) | rearseg^p(Y,X) | -ss^list(Y) | -ss^list(X).
% 1932692 [binary:1930745,1932591,cut:1930742,cut:1930740] rearseg^p(sk3,sk1).
% 1932736 [binary:1932286,1932591,cut:1930604] rearseg^p(skaf46(X,nil),X) | -ss^list(X).
% 1932737 [binary:1932288,1932591,cut:1930604] rearseg^p(X,skaf46(X,nil)) | -ss^list(X).
% 1932741 [binary:1932330,1932591,cut:1930605] rearseg^p(skaf45(X,nil),X) | -ss^list(X).
% 1932742 [binary:1932332,1932591,cut:1930605] rearseg^p(X,skaf45(X,nil)) | -ss^list(X).
% 1933020 [para:1932557.1.2,1930640.1.1,cut:1930566] ss^list(app(sk1,X)) | -ss^list(X).
% 1933022 [para:1932557.1.2,1930650.1.1.1,cut:1930566] equal(tl(app(sk1,X)),X) | -ss^list(X).
% 1933026 [para:1932557.1.2,1930663.1.1,demod:1932533,cut:1930562,cut:1930746,cut:1930740] equal(app(sk1,nil),sk1).
% 1933071 [binary:1930686,1930704,cut:1930605,factor:binarycut:1930797,binarycut:1930763] equal(skaf45(app(X,X),X),X) | -ss^list(X).
% 1933099 [para:1933026.1.1,1930787.1.1,cut:1930562,cut:1930740] rearseg^p(sk1,nil).
% 1933102 [para:1933026.1.1,1930698.1.1,cut:1930740,cut:1930562] -equal(sk1,X) | frontseg^p(X,sk1) | -ss^list(X).
% 1933106 [binary:1930682,1933099,cut:1930746,cut:1930562,cut:1930740] -rearseg^p(nil,sk1).
% 1933205 [binary:1932692,1930707,cut:1930742,cut:1930740] -rearseg^p(X,sk3) | rearseg^p(X,sk1) | -ss^list(X).
% 1933265 [binary:1930745,1933102,cut:1930742] frontseg^p(sk3,sk1).
% 1933269 [binary:1930708,1933265,cut:1930742,cut:1930740] -frontseg^p(X,sk3) | frontseg^p(X,sk1) | -ss^list(X).
% 1933508 [binary:1930791,1933205,cut:1930742,binarydemod:1930763,cut:1930742] rearseg^p(app(sk3,sk3),sk1).
% 1933511 [binary:1932736,1933205,cut:1930604,cut:1930742] rearseg^p(skaf46(sk3,nil),sk1).
% 1933512 [binary:1932741,1933205,cut:1930605,cut:1930742] rearseg^p(skaf45(sk3,nil),sk1).
% 1933533 [para:1930699.1.1,1933508.1.1,cut:1933106,cut:1930742] -equal(nil,sk3).
% 1933539 [para:1930745.1.2,1933512.1.1.1] rearseg^p(skaf45(sk1,nil),sk1).
% 1933551 [para:1930756.1.1,1930715.1.1,cut:1931537,cut:1930562,cut:1933533,binarycut:1930625] -member^p(sk3,X) | equal(X,sk6) | -ss^item(X).
% 1933613 [binary:1930682,1933539,cut:1930740,cut:1930605,binarydemod:1932742,cut:1930740] equal(sk1,skaf45(sk1,nil)).
% 1933653 [para:1933613.1.2,1930686.1.1.2,cut:1930740,cut:1930562] equal(app(nil,sk1),sk1) | -frontseg^p(sk1,nil).
% 1933656 [binary:1930797,1933269,cut:1930742,binarydemod:1930763,cut:1930742] frontseg^p(app(sk3,sk3),sk1).
% 1933660 [binary:1931872,1933551,cut:1930601,cut:1932052,cut:1930742] equal(skaf44(sk3),sk6).
% 1933661 [binary:1931972,1933551,cut:1930566,cut:1933533,cut:1930742] equal(skaf83(sk3),sk6).
% 1933662 [binary:1932240,1933551,cut:1930566,cut:1933533] equal(skaf83(sk1),sk6).
% 1933663 [para:1933660.1.1,1930655.1.1.1,cut:1932052,cut:1930742] equal(cons(sk6,nil),sk3).
% 1933701 [para:1933661.1.1,1932375.1.1.1,demod:1933663,cut:1933533] equal(sk3,sk1).
% 1933702 [binary:1932591,1933701,cut:1930740,cut:1930742] rearseg^p(sk1,sk3).
% 1933703 [binary:1930707,1933702,cut:1930740,cut:1930742] -rearseg^p(X,sk1) | rearseg^p(X,sk3) | -ss^list(X).
% 1933740 [para:1933662.1.1,1932557.1.2.1] equal(app(sk1,X),cons(sk6,X)) | -ss^list(X).
% 1933742 [para:1930745.1.2,1933656.1.1.1] frontseg^p(app(sk1,sk3),sk1).
% 1933757 [para:1933663.1.1,1930674.1.1.1,cut:1931537] equal(app(sk3,X),cons(sk6,X)) | -ss^list(X).
% 1934044 [binary:1933511,1933703,cut:1930604] rearseg^p(skaf46(sk3,nil),sk3).
% 1934059 [binary:1930682,1934044,cut:1930742,cut:1930604,binarydemod:1932737,cut:1930742] equal(sk3,skaf46(sk3,nil)).
% 1934328 [para:1934059.1.2,1930685.1.1.1,cut:1930742,cut:1930562] equal(app(sk3,nil),sk3) | -rearseg^p(sk3,nil).
% 1937070 [para:1934328.1.1,1930793.1.1,cut:1930742,cut:1930562] -rearseg^p(sk3,nil) | frontseg^p(sk3,sk3).
% 1937082 [para:1930745.1.2,1937070.1.1,cut:1933099] frontseg^p(sk3,sk3).
% 1937083 [para:1930745.1.2,1937082.1.1] frontseg^p(sk1,sk3).
% 1937084 [binary:1930708,1937083,cut:1930740,cut:1930742] -frontseg^p(X,sk1) | frontseg^p(X,sk3) | -ss^list(X).
% 1937105 [binary:1930797,1937084,cut:1930740,binarydemod:1933020,cut:1930740] frontseg^p(app(sk1,sk1),sk3).
% 1937112 [binary:1933742,1937084,binarydemod:1933020,cut:1930742] frontseg^p(app(sk1,sk3),sk3).
% 1937330 [para:1930785.1.1,1933022.1.1,demod:1932553,cut:1930746,cut:1930740] equal(app(nil,sk1),sk1).
% 1937332 [para:1937330.1.1,1930793.1.1,cut:1930562,cut:1930740] frontseg^p(sk1,nil).
% 1941691 [para:1933740.1.1,1930763.1.1,cut:1930740] ss^list(cons(sk6,sk1)).
% 1941694 [para:1933740.1.1,1930797.1.1,cut:1930740] frontseg^p(cons(sk6,sk1),sk1).
% 1941695 [para:1933740.1.1,1931722.1.1,cut:1930740] duplicatefree^p(cons(sk6,sk1)) | ss^item(X).
% 1941764 [para:1933740.1.1,1937105.1.1,cut:1930740] frontseg^p(cons(sk6,sk1),sk3).
% 1941765 [para:1933740.1.1,1937112.1.1,cut:1930742] frontseg^p(cons(sk6,sk3),sk3).
% 1942023 [para:1931885.1.1,1930890.1.1.1.2,demod:1933663,1933662,1932554,1937330,cut:1931537,cut:1930562,cut:1933533] -equal(app(sk1,sk3),X) | -ss^list(X) | -duplicatefree^p(X).
% 1946604 [para:1933757.1.1,1930763.1.1,cut:1930742] ss^list(cons(sk6,sk3)).
% 1946642 [para:1933757.1.1,1933071.1.1.1,cut:1930742] equal(skaf45(cons(sk6,sk3),sk3),sk3).
% 1947028 [para:1930745.1.2,1946642.1.1.1.2] equal(skaf45(cons(sk6,sk1),sk3),sk3).
% 1947029 [para:1930745.1.2,1946642.1.1.2] equal(skaf45(cons(sk6,sk3),sk1),sk3).
% 1947030 [para:1946642.1.1,1930686.1.1.2,cut:1941765,cut:1946604,cut:1930742] equal(app(sk3,sk3),cons(sk6,sk3)).
% 1947361 [para:1947028.1.1,1930686.1.1.2,demod:1947030,cut:1941764,cut:1941691,cut:1930742] equal(cons(sk6,sk3),cons(sk6,sk1)).
% 1947362 [para:1947029.1.1,1930686.1.1.2,demod:1947361,cut:1941694,cut:1941691,cut:1930740] equal(app(sk1,sk3),cons(sk6,sk1)).
% 1950001 [binary:1930554,1942023,demod:1947362,cut:1941691,binarydemod:1941695] ss^item(X).
% 1956478 [para:1930699.1.1,1930800.1.1,binarycut:1930625,cut:1950001] -equal(nil,X) | -member^p(X,Y) | -ss^list(X).
% 1956479 [binary:1930554,1956478,cut:1930562] -member^p(nil,X).
% 1957366 [para:1933653.1.1,1931822.1.1.1,demod:1933662,1932559,cut:1956479,cut:1932053,cut:1930562,cut:1930740,cut:1937332] -equal(app(sk1,X),sk1) | -ss^list(X).
% 1957400 [para:1930627.1.1,1957366.1.1,cut:1930554,cut:1930562,cut:1930740] 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: 28
%
%
% ***GANDALF_FOUND_A_REFUTATION***
%
% Global statistics over all passes:
%
% given clauses: 27549
% derived clauses: 2834635
% kept clauses: 754050
% kept size sum: 522778
% kept mid-nuclei: 351891
% kept new demods: 75185
% forw unit-subs: 237227
% forw double-subs: 74954
% forw overdouble-subs: 98174
% backward subs: 1025
% fast unit cutoff: 285681
% full unit cutoff: 435
% dbl unit cutoff: 12301
% real runtime : 380.87
% process. runtime: 379.26
% specific non-discr-tree subsumption statistics:
% tried: 18182478
% length fails: 470650
% strength fails: 3590246
% predlist fails: 8352336
% aux str. fails: 256480
% by-lit fails: 436516
% full subs tried: 4860491
% full subs fail: 4728029
%
% ; 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/SWC/SWC252-1+eq_r.in")
%
%------------------------------------------------------------------------------