%------------------------------------------------------------------------------
% File : Gandalf---c-2.6
% Problem : FLD060-2 : TPTP v3.4.2. Bugfixed v2.1.0.
% Transfm : add_equality:r
% Format : otter:hypothesis:set(auto),clear(print_given)
% Command : gandalf-wrapper -time %d %s
% Computer : art03.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.3s
% Output : Assurance 79.3s
% 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/FLD/FLD060-2+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 3 7)
% (binary-unit 10 #f 3 7)
% (binary-double 16 #f 3 7)
% (binary 54 #t 3 7)
% (binary-order 27 #f 3 7)
% (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(35,40,0,70,0,0,766156,4,2026,766180,50,2055,766180,40,2055,766215,0,2055,803253,3,2556,809459,4,2806,830200,5,3056,830200,1,3056,830200,50,3060,830200,40,3060,830235,0,3060,857937,3,3861,863501,4,4261,932107,5,4661,932108,5,4661,932108,1,4661,932108,50,4665,932108,40,4665,932143,0,4665,1015976,3,7367,1036191,4,8716)
%
%
% START OF PROOF
% 932112 [] equalish(add(X,Y),add(Y,X)) | -defined(X) | -defined(Y).
% 932118 [] defined(add(X,Y)) | -defined(X) | -defined(Y).
% 932124 [] -less_or_equal(X,Y) | -less_or_equal(Y,X) | equalish(X,Y).
% 932125 [] -less_or_equal(X,Y) | -less_or_equal(Y,Z) | less_or_equal(X,Z).
% 932126 [] less_or_equal(X,Y) | less_or_equal(Y,X) | -defined(X) | -defined(Y).
% 932127 [] less_or_equal(add(X,Y),add(Z,Y)) | -less_or_equal(X,Z) | -defined(Y).
% 932129 [] equalish(X,X) | -defined(X).
% 932130 [] -equalish(X,Y) | equalish(Y,X).
% 932131 [] -equalish(X,Y) | -equalish(Y,Z) | equalish(X,Z).
% 932134 [] -less_or_equal(X,Y) | -equalish(X,Z) | less_or_equal(Z,Y).
% 932136 [] defined(a).
% 932137 [] defined(b).
% 932139 [] defined(v).
% 932140 [] equalish(add(a,a),u).
% 932141 [] equalish(add(b,b),v).
% 932142 [] less_or_equal(a,b).
% 932143 [] -less_or_equal(u,v).
% 932149 [binary:932112.2,932136] equalish(add(a,X),add(X,a)) | -defined(X).
% 932161 [binary:932118.2,932136] defined(add(a,X)) | -defined(X).
% 932196 [binary:932127.3,932137] less_or_equal(add(X,b),add(Y,b)) | -less_or_equal(X,Y).
% 932251 [binary:932126.3,932139] less_or_equal(v,X) | less_or_equal(X,v) | -defined(X).
% 932253 [binary:932129.2,932139] equalish(v,v).
% 932278 [binary:932134.2,932140] -less_or_equal(add(a,a),X) | less_or_equal(u,X).
% 932334 [binary:932127.2,932142] less_or_equal(add(a,X),add(b,X)) | -defined(X).
% 932336 [binary:932125.3,932143] -less_or_equal(X,v) | -less_or_equal(u,X).
% 932339 [binary:932130,932141] equalish(v,add(b,b)).
% 932478 [binary:932131,932339] -equalish(add(b,b),X) | equalish(v,X).
% 932482 [binary:932134.2,932339] less_or_equal(add(b,b),X) | -less_or_equal(v,X).
% 932491 [binary:932131.2,932149] -equalish(X,add(a,Y)) | equalish(X,add(Y,a)) | -defined(Y).
% 932496 [binary:932134.2,932149] -less_or_equal(add(a,X),Y) | less_or_equal(add(X,a),Y) | -defined(X).
% 932616 [binary:932137,932161.2] defined(add(a,b)).
% 935896 [binary:932142,932196.2] less_or_equal(add(a,b),add(b,b)).
% 939942 [binary:932134,932251,factor:cut:932253,cut:932139] less_or_equal(v,v).
% 940227 [binary:932134,939942] -equalish(v,X) | less_or_equal(X,v).
% 940250 [binary:932336,940227.2] -less_or_equal(u,X) | -equalish(v,X).
% 949255 [binary:932278,932334,cut:932136] less_or_equal(u,add(b,a)).
% 949267 [binary:932336.2,949255] -less_or_equal(add(b,a),v).
% 949271 [binary:940250,949255] -equalish(v,add(b,a)).
% 966179 [binary:949271,932491.2,cut:932137] -equalish(v,add(a,b)).
% 966236 [binary:932478.2,966179] -equalish(add(b,b),add(a,b)).
% 966753 [binary:949267,932496.2,cut:932137] -less_or_equal(add(a,b),v).
% 966781 [binary:932126,966753,cut:932616,cut:932139] less_or_equal(v,add(a,b)).
% 966806 [binary:932482.2,966781] less_or_equal(add(b,b),add(a,b)).
% 1036325 [binary:966806,932124,cut:935896,cut:966236] contradiction
% END OF PROOF
%
% Proof found by the following strategy:
%
% using binary resolution
% using sos strategy
% using unit paramodulation strategy
% using unit 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 7
% clause depth limited to 3
% seconds given: 54
%
%
% old unit clauses discarded
%
% ***GANDALF_FOUND_A_REFUTATION***
%
% Global statistics over all passes:
%
% given clauses: 8325
% derived clauses: 3646690
% kept clauses: 233281
% kept size sum: 0
% kept mid-nuclei: 93344
% kept new demods: 0
% forw unit-subs: 91593
% forw double-subs: 118668
% forw overdouble-subs: 11270
% backward subs: 186
% fast unit cutoff: 11957
% full unit cutoff: 0
% dbl unit cutoff: 240
% real runtime : 88.75
% process. runtime: 87.64
% specific non-discr-tree subsumption statistics:
% tried: 184648
% length fails: 494
% strength fails: 13342
% predlist fails: 101100
% aux str. fails: 404
% by-lit fails: 64
% full subs tried: 57155
% full subs fail: 50494
%
% ; 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/FLD/FLD060-2+noeq.in")
%
%------------------------------------------------------------------------------