%------------------------------------------------------------------------------
% File : Gandalf---c-2.6
% Problem : GRP002-1 : 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 0.0s
% Output : Assurance 0.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/GRP/GRP002-1+eq_r.in
% Using automatic strategy selection.
% Time limit in seconds: 600
%
% prove-all-passes started
%
% detected problem class: heq
% detected subclass: medium
% detected subclass: long
%
% strategies selected:
% (hyper 58 #f 2 7)
% (binary-posweight-order 29 #f 2 7)
% (binary-unit 29 #f 2 7)
% (binary-double 29 #f 2 7)
% (binary 29 #t 2 7)
% (hyper 29 #t)
% (hyper 105 #f)
% (binary-unit-uniteq 17 #f)
% (binary-weightorder 23 #f)
% (binary-posweight-order 70 #f)
% (binary-posweight-lex-big-order 29 #f)
% (binary-posweight-lex-small-order 11 #f)
% (binary-order 29 #f)
% (binary-unit 46 #f)
% (binary 67 #t)
%
%
% ********* EMPTY CLAUSE DERIVED *********
%
%
% timer checkpoints: c(17,40,0,34,0,0)
%
%
% START OF PROOF
% 19 [] product(identity,X,X).
% 20 [] product(X,identity,X).
% 21 [] product(inverse(X),X,identity).
% 22 [] product(X,inverse(X),identity).
% 23 [] product(X,Y,multiply(X,Y)).
% 24 [] -product(X,Y,U) | -product(X,Y,Z) | equal(Z,U).
% 25 [] -product(U,Y,V) | -product(W,X,U) | -product(X,Y,Z) | product(W,Z,V).
% 26 [] -product(U,Z,V) | -product(U,X,W) | -product(X,Y,Z) | product(W,Y,V).
% 27 [] product(X,Y,identity) | -product(X,X,Y).
% 28 [] product(X,Y,identity) | -product(Y,Y,X).
% 29 [] product(a,b,c).
% 30 [] product(c,inverse(a),d).
% 31 [] product(d,inverse(b),h).
% 32 [] product(h,b,j).
% 33 [] product(j,inverse(h),k).
% 34 [] -product(k,inverse(b),identity).
% 113 [hyper:24,21,20] equal(inverse(identity),identity).
% 125 [hyper:25,21,19,29] product(inverse(a),c,b).
% 177 [hyper:26,22,20,29] product(c,inverse(b),a).
% 178 [hyper:26,22,20,32] product(j,inverse(b),h).
% 210 [hyper:26,30,21,20] product(d,a,c).
% 230 [hyper:25,31,21,32] product(d,identity,j).
% 248 [hyper:26,31,21,20] product(h,b,d).
% 307 [hyper:25,230,30,20] product(c,inverse(a),j).
% 308 [hyper:25,230,19,20] product(identity,d,j).
% 341 [hyper:26,230,22,20,demod:113] product(j,identity,d).
% 343 [hyper:26,230,19,210] product(j,a,c).
% 373 [hyper:25,248,21,19] product(inverse(h),d,b).
% 398 [hyper:25,33,19,230] product(d,inverse(h),k).
% 421 [hyper:26,33,21,20] product(k,h,j).
% 567 [hyper:26,341,21,33] product(k,h,d).
% 629 [hyper:27,23] product(X,multiply(X,X),identity).
% 630 [hyper:28,23] product(multiply(X,X),X,identity).
% 632 [hyper:24,23,19] equal(X,multiply(identity,X)).
% 633 [hyper:24,23,20] equal(X,multiply(X,identity)).
% 636 [hyper:24,23,210] equal(c,multiply(d,a)).
% 664 [hyper:25,23,23,29] product(a,multiply(b,X),multiply(c,X)).
% 666 [hyper:25,23,23,21,demod:632] product(inverse(X),multiply(X,Y),Y).
% 668 [hyper:25,23,23,230,demod:632] product(d,X,multiply(j,X)).
% 669 [hyper:25,23,23,248] product(h,multiply(b,X),multiply(d,X)).
% 672 [hyper:25,23,23,341,demod:632] product(j,X,multiply(d,X)).
% 673 [hyper:25,23,23,343] product(j,multiply(a,X),multiply(c,X)).
% 674 [hyper:25,23,341,23,demod:633] product(X,d,multiply(X,j)).
% 681 [hyper:25,23,29,210] product(d,c,multiply(c,b)).
% 711 [hyper:25,23,343,32] product(h,multiply(b,a),c).
% 713 [hyper:25,23,308,21] product(inverse(X),multiply(X,d),j).
% 746 [hyper:26,23,23,29] product(multiply(X,a),b,multiply(X,c)).
% 748 [hyper:26,23,23,22,demod:633] product(multiply(X,Y),inverse(Y),X).
% 751 [hyper:26,23,23,210] product(multiply(X,d),a,multiply(X,c)).
% 817 [hyper:25,421,23,343] product(k,multiply(h,a),c).
% 819 [hyper:25,421,248,23] product(k,d,multiply(j,b)).
% 893 [hyper:25,567,21,19] product(inverse(k),d,h).
% 939 [hyper:25,125,23,23] product(inverse(a),multiply(c,X),multiply(b,X)).
% 1108 [hyper:26,177,23,23] product(multiply(X,c),inverse(b),multiply(X,a)).
% 1156 [hyper:26,629,23,23,demod:633] product(multiply(X,Y),multiply(Y,Y),X).
% 1159 [hyper:26,629,23,125,demod:633] product(b,multiply(c,c),inverse(a)).
% 1218 [hyper:26,178,23,23] product(multiply(X,j),inverse(b),multiply(X,h)).
% 1629 [hyper:26,307,23,23] product(multiply(X,c),inverse(a),multiply(X,j)).
% 2364 [hyper:25,373,23,23] product(inverse(h),multiply(d,X),multiply(b,X)).
% 2483 [hyper:25,630,23,23,demod:632] product(multiply(X,X),multiply(X,Y),Y).
% 2486 [hyper:25,630,23,177,demod:632] product(multiply(c,c),a,inverse(b)).
% 2587 [hyper:25,398,19,630] product(multiply(d,d),k,inverse(h)).
% 3299 [hyper:24,668,23] equal(multiply(d,X),multiply(j,X)).
% 3516 [hyper:25,672,630,19,demod:3299] product(multiply(d,j),multiply(d,X),X).
% 3659 [hyper:24,674,23] equal(multiply(X,d),multiply(X,j)).
% 5125 [hyper:26,666,630,20] product(X,X,inverse(X)).
% 5242 [hyper:24,5125,23] equal(multiply(X,X),inverse(X)).
% 5371 [hyper:25,5125,373,23] product(h,multiply(h,d),b).
% 5448 [hyper:25,5125,672,32] product(h,inverse(b),multiply(d,b)).
% 5451 [hyper:25,5125,23,21,demod:632] product(inverse(X),inverse(X),X).
% 5649 [hyper:26,5125,30,23] product(multiply(c,a),a,d).
% 11329 [hyper:24,681,23] equal(multiply(d,c),multiply(c,b)).
% 11384 [hyper:25,681,23,893] product(inverse(k),multiply(c,b),multiply(h,c)).
% 11772 [hyper:26,711,567,23] product(d,multiply(b,a),multiply(k,c)).
% 11773 [hyper:26,711,421,23] product(j,multiply(b,a),multiply(k,c)).
% 12254 [hyper:26,817,5125,23] product(inverse(k),multiply(h,a),multiply(k,c)).
% 12690 [hyper:26,819,23,210,demod:3299] product(multiply(d,b),a,multiply(k,c)).
% 21334 [hyper:25,5371,751,23] product(h,multiply(h,c),multiply(b,a)).
% 47535 [hyper:25,1218,177,1156,demod:3659] product(multiply(c,d),multiply(d,h),a).
% 49642 [hyper:25,1629,5451,1159,demod:3659] product(b,multiply(c,d),a).
% 49673 [hyper:26,1629,5125,2486,demod:3659] product(inverse(b),a,multiply(c,d)).
% 50016 [hyper:25,49642,939,748] product(multiply(b,a),multiply(b,d),a).
% 50017 [hyper:25,49642,713,748] product(multiply(b,c),j,a).
% 50116 [hyper:26,49642,672,23,demod:636,demod:3299] product(multiply(d,b),multiply(c,d),c).
% 50353 [hyper:26,50017,669,23,demod:11329] product(multiply(c,b),j,multiply(h,a)).
% 52792 [hyper:26,2364,5451,2587] product(multiply(b,d),k,h).
% 55019 [hyper:26,2483,1108,2486,demod:5242] product(multiply(c,a),multiply(b,a),inverse(b)).
% 67733 [hyper:25,49673,5125,23] product(b,multiply(b,a),multiply(c,d)).
% 82680 [hyper:25,11772,664,5649] product(multiply(c,a),multiply(c,a),multiply(k,c)).
% 83040 [hyper:25,12690,5448,49673] product(h,multiply(c,d),multiply(k,c)).
% 89447 [hyper:25,50016,52792,23] product(multiply(b,a),h,multiply(a,k)).
% 89823 [hyper:26,50116,12690,47535] product(c,multiply(d,h),multiply(k,c)).
% 91754 [hyper:26,50353,12254,11384] product(multiply(h,c),j,multiply(k,c)).
% 99315 [hyper:26,89447,673,11773] product(multiply(k,c),h,multiply(c,k)).
% 100632 [hyper:25,89823,3516,748,demod:5242,3659] product(multiply(c,d),h,multiply(k,c)).
% 101804 [hyper:25,91754,1108,178] product(multiply(h,c),h,multiply(k,a)).
% 104673 [hyper:25,100632,67733,89447] product(b,multiply(a,k),multiply(k,c)).
% 104732 [hyper:25,100632,83040,99315] product(h,multiply(k,c),multiply(c,k)).
% 105267 [hyper:25,101804,21334,89447] product(h,multiply(k,a),multiply(a,k)).
% 105898 [hyper:25,104673,2483,748,demod:5242] product(multiply(b,a),k,multiply(k,c)).
% 107135 [hyper:26,105267,746,104732] product(multiply(a,k),b,multiply(c,k)).
% 110212 [hyper:26,107135,2483,939,demod:5242] product(k,b,multiply(b,k)).
% 110859 [hyper:24,110212,23] equal(multiply(k,b),multiply(b,k)).
% 111281 [para:110859.1.2,666.1.2] product(inverse(b),multiply(k,b),k).
% 146392 [hyper:27,82680] product(multiply(c,a),multiply(k,c),identity).
% 146904 [hyper:26,146392,55019,105898] product(inverse(b),k,identity).
% 147388 [hyper:26,146904,1156,111281,demod:5242,cut:34] contradiction
% END OF PROOF
%
% Proof found by the following strategy:
%
% using hyperresolution
% not using sos strategy
% using positive unit paramodulation strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% clause length limited to 7
% clause depth limited to 2
% seconds given: 58
%
%
% ***GANDALF_FOUND_A_REFUTATION***
%
% Global statistics over all passes:
%
% given clauses: 554
% derived clauses: 434714
% kept clauses: 735
% kept size sum: 5818
% kept mid-nuclei: 146613
% kept new demods: 17
% forw unit-subs: 146174
% forw double-subs: 276
% forw overdouble-subs: 0
% backward subs: 6
% fast unit cutoff: 1
% full unit cutoff: 0
% dbl unit cutoff: 0
% real runtime : 7.89
% process. runtime: 7.88
% specific non-discr-tree subsumption statistics:
% tried: 2254
% length fails: 0
% strength fails: 59
% predlist fails: 46
% aux str. fails: 1045
% by-lit fails: 0
% full subs tried: 1104
% full subs fail: 1104
%
% ; 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/GRP/GRP002-1+eq_r.in")
%
%------------------------------------------------------------------------------