%------------------------------------------------------------------------------
% File : Gandalf---c-2.6
% Problem : GEO006-2 : TPTP v3.4.2. Released v1.0.0.
% Transfm : add_equality:r
% Format : otter:hypothesis:set(auto),clear(print_given)
% Command : gandalf-wrapper -time %d %s
% Computer : art01.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 69.1s
% Output : Assurance 69.1s
% 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/GEO/GEO006-2+eq_r.in
% Using automatic strategy selection.
% Time limit in seconds: 600
%
% prove-all-passes started
%
% detected problem class: neq
% detected subclass: medium
%
% strategies selected:
% (hyper 25 #f 2 15)
% (binary-unit 9 #f 2 15)
% (binary-double 9 #f 2 15)
% (binary-double 15 #f)
% (binary-double 15 #t)
% (binary 50 #t 2 15)
% (binary-order 25 #f 2 15)
% (binary-posweight-order 101 #f)
% (binary-posweight-lex-big-order 25 #f)
% (binary-posweight-lex-small-order 9 #f)
% (binary-order-sos 50 #t)
% (binary-unit-uniteq 25 #f)
% (binary-weightorder 50 #f)
% (binary-order 50 #f)
% (hyper-order 30 #f)
% (binary 112 #t)
%
%
% SOS clause
% between(c,a,d) | between(a,d,c).
% was split for some strategies as:
% between(c,a,d).
% between(a,d,c).
%
% ********* EMPTY CLAUSE DERIVED *********
%
%
% timer checkpoints: c(24,40,0,48,0,0,124480,4,927,136814,5,1201,136814,1,1201,136814,50,1201,136814,40,1201,136838,0,1201,148105,3,1402,149466,4,1502,155031,5,1602,155032,1,1602,155032,50,1602,155032,40,1602,155056,0,1602,164214,3,1807,165795,4,1903,168034,5,2006,168036,5,2006,168036,1,2006,168036,50,2007,168036,40,2007,168060,0,2007,182075,3,2364,184756,4,2533,187865,5,2712,187866,5,2713,187866,1,2713,187866,50,2713,187866,40,2713,187890,0,2713,209926,3,3064,214356,4,3239,220415,5,3414,220416,5,3414,220416,1,3414,220416,50,3415,220416,40,3415,220440,0,3415,255441,3,5660,255441,4,5660,258161,5,5817,258163,5,5817,258163,1,5817,258163,50,5818,258163,40,5818,258187,0,5818,265241,3,6456,269019,4,6719,270623,5,7019,270624,5,7019,270624,1,7019,270624,50,7019,270624,40,7019,270648,0,7019)
%
%
% START OF PROOF
% 224096 [?] ?
% 270628 [] -equidistant(X,Y,Z,Z) | equal(X,Y).
% 270629 [] between(X,Y,extension(X,Y,Z,U)).
% 270630 [] equidistant(X,extension(Y,X,Z,U),Z,U).
% 270632 [] -between(X,Y,X) | equal(X,Y).
% 270633 [] between(X,inner_pasch(Y,X,Z,U,V),V) | -between(V,U,Z) | -between(Y,X,Z).
% 270634 [] between(X,inner_pasch(Y,Z,U,X,V),Y) | -between(V,X,U) | -between(Y,Z,U).
% 270646 [] -equal(c,d).
% 270647 [] between(a,c,d).
% 270648 [] between(c,a,d) | between(a,d,c).
% 270666 [binary:270628,270630] equal(X,extension(Y,X,Z,Z)).
% 270667 [para:270666.1.2,270629.1.3] between(X,Y,Y).
% 270686 [binary:270647,270633.2] between(X,inner_pasch(Y,X,d,c,a),a) | -between(Y,X,d).
% 270690 [binary:270667,270633.2] between(X,inner_pasch(Y,X,Z,Z,U),U) | -between(Y,X,Z).
% 270704 [binary:270647,270634.2] between(c,inner_pasch(X,Y,d,c,a),X) | -between(X,Y,d).
% 270708 [binary:270667,270634.2] between(X,inner_pasch(Y,Z,X,X,U),Y) | -between(Y,Z,X).
% 270716 [binary:270667,270686.2] between(d,inner_pasch(X,d,d,c,a),a).
% 270728 [binary:270648,270690.2] between(a,d,c) | between(a,inner_pasch(c,a,d,d,X),X).
% 270766 [binary:270667,270704.2] between(c,inner_pasch(X,d,d,c,a),X).
% 270769 [binary:270632,270766] equal(c,inner_pasch(c,d,d,c,a)).
% 270777 [para:270769.1.2,270716.1.2] between(d,c,a).
% 270778 [binary:270633.2,270777] between(X,inner_pasch(Y,X,a,c,d),d) | -between(Y,X,a).
% 270779 [binary:270634.2,270777] between(c,inner_pasch(X,Y,a,c,d),X) | -between(X,Y,a).
% 270806 [binary:270648,270708.2] between(a,d,c) | between(d,inner_pasch(c,a,d,d,X),c).
% 271993 [binary:270632,270728.2] equal(a,inner_pasch(c,a,d,d,a)) | between(a,d,c).
% 272255 [para:271993.1.2,270806.2.2,cut:224096] between(a,d,c).
% 272259 [binary:270690.2,272255] between(d,inner_pasch(a,d,c,c,X),X).
% 272263 [binary:270708.2,272255] between(c,inner_pasch(a,d,c,c,X),a).
% 272315 [binary:270632,272259] equal(d,inner_pasch(a,d,c,c,d)).
% 272340 [para:272315.1.2,272263.1.2] between(c,d,a).
% 272350 [binary:270778.2,272340] between(d,inner_pasch(c,d,a,c,d),d).
% 272351 [binary:270779.2,272340] between(c,inner_pasch(c,d,a,c,d),c).
% 272417 [binary:270632,272350] equal(d,inner_pasch(c,d,a,c,d)).
% 272418 [binary:270632,272351,demod:272417,cut:270646] contradiction
% END OF PROOF
%
% Proof found by the following strategy:
%
% using binary resolution
% using first neg lit preferred 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: 50
%
%
% old unit clauses discarded
%
% ***GANDALF_FOUND_A_REFUTATION***
%
% Global statistics over all passes:
%
% given clauses: 3883
% derived clauses: 939561
% kept clauses: 99891
% kept size sum: 0
% kept mid-nuclei: 147733
% kept new demods: 357
% forw unit-subs: 281160
% forw double-subs: 154041
% forw overdouble-subs: 71267
% backward subs: 213
% fast unit cutoff: 70132
% full unit cutoff: 376
% dbl unit cutoff: 455
% real runtime : 71.18
% process. runtime: 70.27
% specific non-discr-tree subsumption statistics:
% tried: 29274526
% length fails: 2684152
% strength fails: 9442518
% predlist fails: 4980297
% aux str. fails: 3099233
% by-lit fails: 1622158
% full subs tried: 6834158
% full subs fail: 6757391
%
% ; 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/GEO/GEO006-2+eq_r.in")
%
%------------------------------------------------------------------------------