%------------------------------------------------------------------------------
% File : Gandalf---c-2.6
% Problem : HWV029-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 50.0s
% Output : Assurance 50.0s
% 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/HWV/HWV029-1+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 3 13)
% (binary-unit 9 #f 3 13)
% (binary-double 9 #f 3 13)
% (binary-double 15 #f)
% (binary-double 15 #t)
% (binary 50 #t 3 13)
% (binary-order 25 #f 3 13)
% (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)
%
%
% ********* EMPTY CLAUSE DERIVED *********
%
%
% timer checkpoints: c(94,40,1,188,0,1,40534,4,2003,57175,5,2502,57175,1,2502,57175,50,2503,57175,40,2503,57269,0,2503,71672,3,2954,72523,4,3179,73317,1,3404,73317,50,3404,73317,40,3404,73411,0,3405,99422,3,3856,104189,4,4081,114424,5,4306,114425,5,4306,114425,1,4306,114425,50,4307,114425,40,4307,114519,0,4307,150820,3,5059,161001,4,5445)
%
%
% START OF PROOF
% 73713 [?] ?
% 77232 [?] ?
% 79390 [?] ?
% 85370 [?] ?
% 87185 [?] ?
% 93406 [?] ?
% 95971 [?] ?
% 99210 [?] ?
% 114426 [] equal(X,X).
% 114427 [] -equal(plus(X,n1),n0).
% 114428 [] gt(plus(X,n1),n0).
% 114429 [] gt(X,minus(X,n1)) | -gt(X,n0).
% 114430 [] -equal(minus(X,Y),Z) | equal(plus(Z,Y),X) | def_10(Y,X).
% 114431 [] -equal(plus(X,Y),Z) | equal(minus(Z,Y),X) | def_10(Y,Z).
% 114432 [] -def_10(X,Y) | -gt(Y,X).
% 114433 [] -def_10(X,Y) | -equal(Y,X).
% 114434 [] gt(plus(X,n1),plus(Y,n1)) | -gt(X,Y).
% 114435 [] -gt(plus(X,n1),plus(Y,n1)) | gt(X,Y).
% 114437 [] -gt(plus(X,n1),Y) | gt(X,Y) | equal(X,Y).
% 114438 [] gt(Y,X) | gt(X,Y) | equal(Y,X).
% 114439 [] -gt(Y,Z) | -gt(X,Y) | gt(X,Z).
% 114440 [] gt(X,plus(Y,n1)) | equal(plus(Y,n1),X) | -gt(X,Y).
% 114441 [] gt(X,n0) | equal(X,n0).
% 114442 [] equal(X,plus(y_27(X),n1)) | equal(X,n0).
% 114443 [] -gt(X,X).
% 114444 [] -equal(plus(X,n1),plus(Y,n1)) | equal(X,Y).
% 114445 [] equal(plus(n0,X),X).
% 114448 [] -equal(level(X),fifo_length) | p_^full(X).
% 114449 [] equal(level(X),fifo_length) | -p_^full(X).
% 114450 [] -equal(level(X),n0) | p_^empty(X).
% 114451 [] equal(level(X),n0) | -p_^empty(X).
% 114452 [] equal(level(plus(X,n1)),n0) | -p_^reset(X).
% 114461 [] equal(level(plus(X,n1)),plus(level(X),n1)) | -gt(fifo_length,level(X)) | -p_^wr(X) | p_^rd(X) | p_^reset(X).
% 114470 [] equal(level(plus(X,n1)),level(X)) | gt(fifo_length,level(X)) | -p_^wr(X) | p_^rd(X) | p_^reset(X).
% 114479 [] equal(level(plus(X,n1)),level(X)) | -gt(level(X),n0) | -p_^rd(X) | -p_^wr(X) | p_^reset(X).
% 114497 [] equal(level(plus(X,n1)),minus(level(X),n1)) | -gt(level(X),n0) | -p_^rd(X) | p_^wr(X) | p_^reset(X).
% 114504 [] equal(level(plus(X,n1)),level(X)) | gt(level(X),n0) | -p_^rd(X) | p_^wr(X) | p_^reset(X).
% 114508 [] equal(level(plus(X,n1)),level(X)) | p_^rd(X) | p_^wr(X) | p_^reset(X).
% 114517 [] -gt(level(x_139),fifo_length).
% 114518 [] gt(level(plus(x_139,n1)),fifo_length).
% 114519 [] gt(fifo_length,n0).
% 114523 [binary:114519,114429.2] gt(fifo_length,minus(fifo_length,n1)).
% 114524 [binary:114428,114429.2] gt(plus(X,n1),minus(plus(X,n1),n1)).
% 114535 [binary:114426,114430] equal(plus(minus(X,Y),Y),X) | def_10(Y,X).
% 114540 [para:114430.2.1,114427.1.1,slowcut:114426] -equal(X,n0) | def_10(n1,X).
% 114558 [para:114431.2.1,114523.1.2,cut:77232] -equal(plus(X,n1),fifo_length) | gt(fifo_length,X).
% 114580 [binary:114519,114434.2,demod:114445] gt(plus(fifo_length,n1),n1).
% 114582 [para:114445.1.1,114434.1.1,cut:73713] -gt(n0,X).
% 114589 [para:114430.2.1,114434.1.1] -equal(minus(X,n1),Y) | gt(X,plus(Z,n1)) | def_10(n1,X) | -gt(Y,Z).
% 114606 [para:114445.1.1,114435.1.1,cut:114582] -gt(n1,plus(X,n1)).
% 114637 [binary:114517,114437.2] -gt(plus(level(x_139),n1),fifo_length) | equal(level(x_139),fifo_length).
% 114639 [para:114445.1.1,114437.1.1,cut:114582] -gt(n1,X) | equal(n0,X).
% 114646 [binary:114580,114437] gt(fifo_length,n1) | equal(fifo_length,n1).
% 114655 [binary:114437.3,114450,cut:114428] gt(level(X),n0) | p_^empty(X).
% 114660 [para:114451.1.1,114518.1.1,cut:114582] -p_^empty(plus(x_139,n1)).
% 114666 [binary:114450.2,114660] -equal(level(plus(x_139,n1)),n0).
% 114667 [binary:114450.2,114660,binarydemod:114452] -p_^reset(x_139).
% 114670 [binary:114517,114438,binarydemod:114448] gt(fifo_length,level(x_139)) | p_^full(x_139).
% 114699 [binary:114517,114439.3] -gt(level(x_139),X) | -gt(X,fifo_length).
% 114711 [binary:114434,114439,factor:cut:99210] -gt(X,plus(X,n1)).
% 114715 [?] ?
% 114722 [?] ?
% 114780 [para:114440.2.1,114580.1.1,binarycut:114715] -gt(X,fifo_length) | gt(X,n1).
% 114790 [para:114440.2.1,114606.1.2,binarycut:114722] -gt(n1,X) | -gt(X,Y).
% 114830 [para:114441.2.2,114519.1.2] gt(fifo_length,X) | gt(X,n0).
% 114872 [binary:114432,114540.2] -gt(X,n1) | -equal(X,n0).
% 114875 [binary:114433,114540.2] -equal(X,n0) | -equal(X,n1).
% 114876 [binary:114451,114540] def_10(n1,level(X)) | -p_^empty(X).
% 114879 [binary:114432,114876] -gt(level(X),n1) | -p_^empty(X).
% 114880 [binary:114433,114876] -equal(level(X),n1) | -p_^empty(X).
% 114881 [para:114449.1.1,114876.1.2,cut:77232] -p_^empty(X) | -p_^full(X).
% 114887 [binary:114427,114442.2,binarydemod:114444] equal(X,y_27(plus(X,n1))).
% 114935 [binary:114655.2,114881] gt(level(X),n0) | -p_^full(X).
% 114940 [binary:114437.2,114879,binarycut:114880] -gt(plus(level(X),n1),n1) | -p_^empty(X).
% 114942 [binary:114438,114879,binarycut:114880] gt(n1,level(X)) | -p_^empty(X).
% 115023 [binary:114518,114780] gt(level(plus(x_139,n1)),n1).
% 115074 [binary:114790,114942] -gt(level(X),Y) | -p_^empty(X).
% 115214 [para:114442.2.2,114830.2.2,factor:cut:114443] equal(fifo_length,plus(y_27(fifo_length),n1)).
% 115215 [binary:115074,114830.2] gt(fifo_length,level(X)) | -p_^empty(X).
% 115689 [binary:114438.3,114875.2,binarycut:114872] -equal(X,n0) | gt(n1,X).
% 116080 [binary:114790,115689.2] -equal(X,n0) | -gt(X,Y).
% 116088 [binary:114639,115689.2] -equal(X,n0) | equal(n0,X).
% 116362 [para:116088.2.1,114666.1.2] -equal(level(plus(x_139,n1)),X) | -equal(X,n0).
% 116497 [para:114479.1.1,114518.1.1,cut:114517,cut:79390,cut:114667] -p_^rd(x_139) | -p_^wr(x_139).
% 116631 [para:114461.1.1,115023.1.1,cut:114667,binarycut:116497,binarydemod:115215,114940] -p_^wr(x_139) | -p_^empty(x_139).
% 116633 [binary:114450.2,116631.2] -equal(level(x_139),n0) | -p_^wr(x_139).
% 116890 [para:115214.1.2,114711.1.2] -gt(y_27(fifo_length),fifo_length).
% 116923 [binary:114438,116890,cut:85370] gt(fifo_length,y_27(fifo_length)).
% 116997 [binary:114439.2,116923] -gt(y_27(fifo_length),X) | gt(fifo_length,X).
% 118317 [binary:114432.2,114646] -def_10(n1,fifo_length) | equal(fifo_length,n1).
% 118363 [binary:114433.2,118317.2] -def_10(n1,fifo_length).
% 118936 [para:114497.1.1,114518.1.1,cut:87185,cut:114667] -gt(level(x_139),n0) | -p_^rd(x_139) | p_^wr(x_139).
% 118937 [para:114497.1.1,114518.1.1,cut:87185,cut:114667,binarydemod:114935] -p_^rd(x_139) | -p_^full(x_139) | p_^wr(x_139).
% 119139 [binary:116497.2,118937.3] -p_^rd(x_139) | -p_^full(x_139).
% 119933 [para:114504.1.1,114518.1.1,cut:114517,cut:114667,binarydemod:115074,binarycut:116631] -p_^rd(x_139) | -p_^empty(x_139).
% 120666 [binary:116633.2,114508.3,cut:114667,binarycut:116362,binarydemod:114451,binarycut:119933] -p_^empty(x_139).
% 120714 [binary:114450.2,120666] -equal(level(x_139),n0).
% 120716 [binary:114655.2,120666] gt(level(x_139),n0).
% 120721 [binary:114442.2,120714] equal(level(x_139),plus(y_27(level(x_139)),n1)).
% 121423 [binary:114444,114535,cut:93406] equal(minus(plus(X,n1),n1),X).
% 122402 [para:121423.1.1,114430.1.1,cut:93406] equal(plus(X,n1),plus(Y,n1)) | -equal(Y,X).
% 122407 [para:115214.1.2,121423.1.1.1] equal(minus(fifo_length,n1),y_27(fifo_length)).
% 122408 [para:121423.1.1,114524.1.2] gt(plus(X,n1),X).
% 122414 [para:114442.1.2,122408.1.1] gt(X,y_27(X)) | equal(X,n0).
% 122679 [binary:114699,122414,cut:120714] -gt(y_27(level(x_139)),fifo_length).
% 122759 [binary:114438,122679,cut:95971] gt(fifo_length,y_27(level(x_139))).
% 122763 [binary:114434.2,122759,demod:120721] gt(plus(fifo_length,n1),level(x_139)).
% 123081 [binary:114439,122763] -gt(X,plus(fifo_length,n1)) | gt(X,level(x_139)).
% 123084 [para:114440.2.1,122763.1.1,binarycut:123081] gt(X,level(x_139)) | -gt(X,fifo_length).
% 123226 [binary:114430.2,114558,demod:122407,cut:118363] -equal(y_27(fifo_length),X) | gt(fifo_length,X).
% 124994 [binary:114438.3,123226,binarycut:116997] gt(X,y_27(fifo_length)) | gt(fifo_length,X).
% 125914 [binary:114443,114589.2,demod:121423,cut:93406] -gt(X,Y) | -equal(Y,X).
% 126063 [binary:114434,125914,binarydemod:122402] -gt(X,Y) | -equal(X,Y).
% 126065 [binary:114449,125914.2] -gt(fifo_length,level(X)) | -p_^full(X).
% 126620 [binary:114442,126063.2,binarycut:116080] -gt(X,plus(y_27(X),n1)).
% 126678 [binary:123084,126063] -equal(X,level(x_139)) | -gt(X,fifo_length).
% 126696 [binary:124994.2,126065] gt(level(X),y_27(fifo_length)) | -p_^full(X).
% 126725 [binary:114439.3,126620] -gt(X,plus(y_27(Y),n1)) | -gt(Y,X).
% 126728 [para:114440.2.1,126620.1.2,binarycut:126725] -gt(X,y_27(Y)) | -gt(Y,X).
% 127510 [binary:114518,126728.2] -gt(fifo_length,y_27(level(plus(x_139,n1)))).
% 128384 [binary:114434.2,126696,demod:115214] gt(plus(level(X),n1),fifo_length) | -p_^full(X).
% 130563 [binary:114518,126678.2] -equal(level(plus(x_139,n1)),level(x_139)).
% 132070 [para:114470.2.1,114637.2.2,cut:114443,cut:130563,cut:114667,binarycut:116497,binarydemod:128384] -p_^wr(x_139) | -p_^full(x_139).
% 132089 [binary:114508.3,132070,cut:130563,cut:114667,binarycut:119139] -p_^full(x_139).
% 132099 [binary:114670.2,132089] gt(fifo_length,level(x_139)).
% 142070 [para:114461.1.1,127510.1.2.1,demod:114887,cut:132099,cut:114667,binarycut:116497] -p_^wr(x_139).
% 142072 [para:114508.1.1,127510.1.2.1,cut:122759,cut:142070,cut:114667] p_^rd(x_139).
% 164574 [binary:120716,118936,cut:142072,cut:142070] 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: 15
%
%
% old unit clauses discarded
%
% ***GANDALF_FOUND_A_REFUTATION***
%
% Global statistics over all passes:
%
% given clauses: 6902
% derived clauses: 689763
% kept clauses: 125707
% kept size sum: 0
% kept mid-nuclei: 26081
% kept new demods: 144
% forw unit-subs: 248738
% forw double-subs: 130251
% forw overdouble-subs: 111722
% backward subs: 1330
% fast unit cutoff: 25798
% full unit cutoff: 159
% dbl unit cutoff: 2400
% real runtime : 55.60
% process. runtime: 55.57
% specific non-discr-tree subsumption statistics:
% tried: 12585677
% length fails: 960122
% strength fails: 1881977
% predlist fails: 3394206
% aux str. fails: 439737
% by-lit fails: 631827
% full subs tried: 5104495
% full subs fail: 5004010
%
% ; 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/HWV/HWV029-1+eq_r.in")
%
%------------------------------------------------------------------------------