%------------------------------------------------------------------------------
% File : Gandalf---c-2.6
% Problem : SWC336-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 : art09.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 79.6s
% Output : Assurance 79.6s
% 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/SWC336-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(207,40,1,414,0,1,80538,4,2316,103487,5,2802,103488,1,2803,103488,50,2808,103488,40,2808,103695,0,2808,196211,3,4211,220542,4,4909,237535,5,5609,237537,1,5610,237537,50,5613,237537,40,5613,237744,0,5613,274801,3,6164,286282,4,6440,301765,5,6714,301767,5,6715,301768,1,6715,301768,50,6717,301768,40,6717,301975,0,6717,350704,3,7570,367634,4,7994)
%
%
% START OF PROOF
% 301773 [] totalordered^p(nil).
% 301777 [] ss^list(nil).
% 301780 [] -singleton^p(nil).
% 301825 [] segment^p(X,nil) | -ss^list(X).
% 301826 [] segment^p(X,X) | -ss^list(X).
% 301836 [] totalordered^p(cons(X,nil)) | -ss^item(X).
% 301848 [] -equal(nil,X) | segment^p(nil,X) | -ss^list(X).
% 301867 [] -equal(cons(X,Y),nil) | -ss^item(X) | -ss^list(Y).
% 301885 [] -equal(cons(X,nil),Y) | -ss^item(X) | -ss^list(Y) | singleton^p(Y).
% 301896 [] -segment^p(X,Y) | -segment^p(Y,X) | equal(Y,X) | -ss^list(Y) | -ss^list(X).
% 301942 [] -equal(app(app(X,Y),Z),U) | segment^p(U,Y) | -ss^list(U) | -ss^list(Y) | -ss^list(Z) | -ss^list(X).
% 301955 [] ss^list(sk1).
% 301956 [] ss^list(sk2).
% 301957 [] ss^list(sk3).
% 301958 [] ss^list(sk4).
% 301959 [] equal(sk2,sk4).
% 301960 [] equal(sk1,sk3).
% 301962 [] equal(nil,sk3) | ss^item(sk5).
% 301963 [] equal(nil,sk4) | ss^list(sk6).
% 301964 [] equal(nil,sk4) | ss^list(sk7).
% 301965 [] equal(cons(sk5,nil),sk3) | equal(nil,sk4).
% 301969 [] equal(nil,sk3) | ss^list(sk6).
% 301970 [] equal(nil,sk3) | ss^list(sk7).
% 301971 [] equal(cons(sk5,nil),sk3) | equal(nil,sk3).
% 301972 [] equal(app(app(sk6,sk3),sk7),sk4) | equal(nil,sk3).
% 301975 [] -segment^p(sk2,sk1) | -totalordered^p(sk1).
% 302307 [para:301962.1.2,301960.1.2] equal(sk1,nil) | ss^item(sk5).
% 302310 [para:301963.1.2,301959.1.2] equal(sk2,nil) | ss^list(sk6).
% 302313 [para:301964.1.2,301959.1.2] equal(sk2,nil) | ss^list(sk7).
% 302316 [para:301965.2.2,301959.1.2] equal(cons(sk5,nil),sk3) | equal(sk2,nil).
% 302319 [para:301969.1.2,301960.1.2] equal(sk1,nil) | ss^list(sk6).
% 302350 [para:301970.1.2,301960.1.2] equal(sk1,nil) | ss^list(sk7).
% 302362 [para:301960.1.2,301972.1.1.1.2] equal(app(app(sk6,sk1),sk7),sk4) | equal(nil,sk3).
% 302447 [binary:301956,301825.2] segment^p(sk2,nil).
% 302448 [binary:301957,301825.2] segment^p(sk3,nil).
% 302486 [binary:301958,301826.2] segment^p(sk4,sk4).
% 302565 [para:301959.1.2,302486.1.1] segment^p(sk2,sk4).
% 302566 [para:301959.1.2,302486.1.2] segment^p(sk4,sk2).
% 302611 [?] ?
% 302612 [?] ?
% 302877 [para:302307.1.1,301975.1.2,cut:302447] -totalordered^p(sk1) | ss^item(sk5).
% 302942 [para:302307.1.1,302877.1.1,cut:301773] ss^item(sk5).
% 302951 [binary:301836.2,302942] totalordered^p(cons(sk5,nil)).
% 304042 [para:301971.1.1,302951.1.1] equal(nil,sk3) | totalordered^p(sk3).
% 307329 [para:302310.1.1,301975.1.1,binarycut:302611] -totalordered^p(sk1) | ss^list(sk6).
% 308010 [binary:302565,301896,cut:302566,cut:301958,cut:301956] equal(sk4,sk2).
% 310747 [para:302313.1.1,301975.1.1,binarycut:302612] -totalordered^p(sk1) | ss^list(sk7).
% 311778 [para:302319.1.1,307329.1.1,cut:301773] ss^list(sk6).
% 314748 [para:302350.1.1,310747.1.1,cut:301773] ss^list(sk7).
% 319718 [para:302316.1.1,301836.1.1,cut:302942] equal(sk2,nil) | totalordered^p(sk3).
% 319735 [binary:301885,302316,cut:302942,cut:301957] equal(sk2,nil) | singleton^p(sk3).
% 320581 [para:304042.1.2,301960.1.2] equal(sk1,nil) | totalordered^p(sk3).
% 320585 [?] ?
% 320677 [?] ?
% 321248 [para:319718.1.1,301975.1.1,binarycut:320585] -totalordered^p(sk1) | totalordered^p(sk3).
% 321338 [para:319735.1.1,301975.1.1,binarycut:320677] -totalordered^p(sk1) | singleton^p(sk3).
% 322152 [para:302362.1.1,301942.1.1,cut:301955,cut:314748,cut:311778] equal(nil,sk3) | -equal(sk4,X) | segment^p(X,sk1) | -ss^list(X).
% 323431 [para:320581.1.1,321248.1.1,cut:301773] totalordered^p(sk3).
% 323432 [para:301960.1.2,323431.1.1] totalordered^p(sk1).
% 323434 [binary:301975.2,323432] -segment^p(sk2,sk1).
% 323438 [binary:321338,323432] singleton^p(sk3).
% 323485 [para:301971.2.2,323438.1.1,cut:301780] equal(cons(sk5,nil),sk3).
% 323838 [para:323485.1.1,301867.1.1,cut:302942,cut:301777] -equal(sk3,nil).
% 323892 [binary:301896.3,323838,cut:302448,cut:301957,cut:301777] -segment^p(nil,sk3).
% 323948 [binary:301848.2,323892,cut:301957] -equal(nil,sk3).
% 378959 [binary:308010,322152.2,cut:323948,cut:323434,cut:301956] contradiction
% END OF PROOF
%
% Proof found by the following strategy:
%
% using binary resolution
% not using sos strategy
% using unit paramodulation strategy
% using unit strategy
% using double strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% using clause demodulation
% seconds given: 17
%
%
% old unit clauses discarded
%
% ***GANDALF_FOUND_A_REFUTATION***
%
% Global statistics over all passes:
%
% given clauses: 4158
% derived clauses: 599811
% kept clauses: 255108
% kept size sum: 0
% kept mid-nuclei: 62246
% kept new demods: 27061
% forw unit-subs: 68876
% forw double-subs: 34173
% forw overdouble-subs: 11767
% backward subs: 1130
% fast unit cutoff: 46740
% full unit cutoff: 0
% dbl unit cutoff: 949
% real runtime : 83.53
% process. runtime: 83.8
% specific non-discr-tree subsumption statistics:
% tried: 2678198
% length fails: 41197
% strength fails: 268112
% predlist fails: 1767032
% aux str. fails: 91485
% by-lit fails: 94071
% full subs tried: 350995
% full subs fail: 338346
%
% ; 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/SWC336-1+eq_r.in")
%
%------------------------------------------------------------------------------