%------------------------------------------------------------------------------
% File : Gandalf---c-2.6
% Problem : GRP277-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 119.6s
% Output : Assurance 119.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/GRP/GRP277-1+eq_r.in
% Using automatic strategy selection.
% Time limit in seconds: 600
%
% prove-all-passes started
%
% detected problem class: peq
%
% strategies selected:
% (hyper 30 #f 3 19)
% (binary-unit 12 #f)
% (binary-unit-uniteq 12 #f)
% (binary-posweight-kb-big-order 60 #f 3 19)
% (binary-posweight-lex-big-order 30 #f 3 19)
% (binary 30 #t)
% (binary-posweight-kb-big-order 156 #f)
% (binary-posweight-lex-big-order 102 #f)
% (binary-posweight-firstpref-order 60 #f)
% (binary-order 30 #f)
% (binary-posweight-kb-small-order 48 #f)
% (binary-posweight-lex-small-order 30 #f)
%
%
% SOS clause
% -equal(multiply(X,sk_c7),sk_c6) | -equal(inverse(X),sk_c7) | -equal(multiply(sk_c7,sk_c5),sk_c6) | -equal(multiply(sk_c5,sk_c6),sk_c7) | -equal(multiply(sk_c6,sk_c7),sk_c5) | -equal(inverse(Y),sk_c7) | -equal(multiply(Y,sk_c6),sk_c7) | -equal(multiply(Z,U),sk_c6) | -equal(inverse(Z),U) | -equal(multiply(U,sk_c7),sk_c6).
% was split for some strategies as:
% -equal(multiply(Z,U),sk_c6) | -equal(inverse(Z),U) | -equal(multiply(U,sk_c7),sk_c6).
% -equal(inverse(Y),sk_c7) | -equal(multiply(Y,sk_c6),sk_c7).
% -equal(multiply(X,sk_c7),sk_c6) | -equal(inverse(X),sk_c7).
% -equal(multiply(sk_c7,sk_c5),sk_c6).
% -equal(multiply(sk_c5,sk_c6),sk_c7).
% -equal(multiply(sk_c6,sk_c7),sk_c5).
%
% ********* EMPTY CLAUSE DERIVED *********
%
%
% timer checkpoints: c(29,40,2,62,0,2,761,50,7,794,0,7,2102,50,19,2135,0,19,3724,50,38,3757,0,38,5515,50,57,5548,0,57,7475,50,77,7508,0,77,9659,50,108,9692,0,108,12068,50,156,12101,0,157,14757,50,245,14790,0,245,17727,50,416,17760,0,416,21033,50,678,21066,0,678,24676,50,1137,24676,40,1137,24709,0,1137,34160,3,1438,34967,4,1588,35731,5,1738,35732,1,1738,35732,50,1738,35732,40,1738,35765,0,1738,36081,3,2051,36089,4,2192,36100,5,2339,36100,1,2339,36100,50,2339,36100,40,2339,36133,0,2339,64393,3,3840,65346,4,4590,66320,5,5340,66321,1,5340,66321,50,5341,66321,40,5341,66354,0,5341,85204,3,6093,85972,4,6467,86708,1,6842,86708,50,6842,86708,40,6842,86741,0,6842,97333,3,7598,98583,4,7968,100307,5,8343,100308,1,8343,100308,50,8343,100308,40,8343,100341,0,8343)
%
%
% START OF PROOF
% 100309 [] equal(X,X).
% 100310 [] equal(multiply(identity,X),X).
% 100311 [] equal(multiply(inverse(X),X),identity).
% 100312 [] equal(multiply(multiply(X,Y),Z),multiply(X,multiply(Y,Z))).
% 100313 [] -equal(multiply(sk_c5,sk_c6),sk_c7) | -equal(multiply(sk_c6,sk_c7),sk_c5) | -equal(multiply(sk_c7,sk_c5),sk_c6) | -equal(multiply(Y,sk_c7),sk_c6) | -equal(multiply(Z,sk_c6),sk_c7) | -equal(multiply(X,sk_c7),sk_c6) | -equal(multiply(U,Y),sk_c6) | -equal(inverse(Z),sk_c7) | -equal(inverse(X),sk_c7) | -equal(inverse(U),Y).
% 100316 [] equal(multiply(sk_c5,sk_c6),sk_c7) | equal(multiply(sk_c3,sk_c4),sk_c6).
% 100317 [] equal(multiply(sk_c5,sk_c6),sk_c7) | equal(multiply(sk_c2,sk_c6),sk_c7).
% 100318 [] equal(multiply(sk_c5,sk_c6),sk_c7) | equal(inverse(sk_c2),sk_c7).
% 100319 [] equal(multiply(sk_c5,sk_c6),sk_c7) | equal(multiply(sk_c6,sk_c7),sk_c5).
% 100322 [] equal(multiply(sk_c7,sk_c5),sk_c6) | equal(multiply(sk_c3,sk_c4),sk_c6).
% 100323 [] equal(multiply(sk_c7,sk_c5),sk_c6) | equal(multiply(sk_c2,sk_c6),sk_c7).
% 100324 [] equal(multiply(sk_c7,sk_c5),sk_c6) | equal(inverse(sk_c2),sk_c7).
% 100327 [] equal(inverse(sk_c1),sk_c7) | equal(inverse(sk_c3),sk_c4).
% 100328 [] equal(multiply(sk_c3,sk_c4),sk_c6) | equal(inverse(sk_c1),sk_c7).
% 100330 [] equal(inverse(sk_c1),sk_c7) | equal(inverse(sk_c2),sk_c7).
% 100331 [] equal(multiply(sk_c6,sk_c7),sk_c5) | equal(inverse(sk_c1),sk_c7).
% 100333 [] equal(multiply(sk_c1,sk_c7),sk_c6) | equal(inverse(sk_c3),sk_c4).
% 100334 [] equal(multiply(sk_c1,sk_c7),sk_c6) | equal(multiply(sk_c3,sk_c4),sk_c6).
% 100342 [input:100313,factor] -equal(multiply(sk_c7,sk_c5),sk_c6) | -equal(multiply(sk_c5,sk_c6),sk_c7) | -equal(multiply(sk_c6,sk_c7),sk_c5) | -equal(inverse(sk_c5),sk_c7) | -equal(multiply(X,sk_c7),sk_c6) | -equal(multiply(Y,sk_c7),sk_c6) | -equal(multiply(Z,Y),sk_c6) | -equal(inverse(X),sk_c7) | -equal(inverse(Z),Y).
% 100464 [para:100311.1.1,100312.1.1.1,demod:100310] equal(X,multiply(inverse(Y),multiply(Y,X))).
% 100468 [para:100324.1.1,100312.1.1.1] equal(inverse(sk_c2),sk_c7) | equal(multiply(sk_c6,X),multiply(sk_c7,multiply(sk_c5,X))).
% 100518 [para:100311.1.1,100464.1.2.2] equal(X,multiply(inverse(inverse(X)),identity)).
% 100578 [para:100312.1.1,100464.1.2.2] equal(X,multiply(inverse(multiply(Y,Z)),multiply(Y,multiply(Z,X)))).
% 100579 [para:100464.1.2,100464.1.2.2] equal(multiply(X,Y),multiply(inverse(inverse(X)),Y)).
% 100602 [para:100579.1.2,100311.1.1] equal(multiply(X,inverse(X)),identity).
% 100624 [para:100579.1.2,100518.1.2] equal(X,multiply(X,identity)).
% 100626 [para:100624.1.2,100518.1.2] equal(X,inverse(inverse(X))).
% 100635 [para:100330.1.1,100626.1.2.1] equal(sk_c1,inverse(sk_c7)) | equal(inverse(sk_c2),sk_c7).
% 100636 [para:100330.2.1,100626.1.2.1] equal(sk_c2,inverse(sk_c7)) | equal(inverse(sk_c1),sk_c7).
% 100642 [para:100328.2.1,100626.1.2.1] equal(multiply(sk_c3,sk_c4),sk_c6) | equal(sk_c1,inverse(sk_c7)).
% 100644 [para:100331.2.1,100626.1.2.1] equal(multiply(sk_c6,sk_c7),sk_c5) | equal(sk_c1,inverse(sk_c7)).
% 100651 [para:100327.1.1,100602.1.1.2] equal(multiply(sk_c1,sk_c7),identity) | equal(inverse(sk_c3),sk_c4).
% 100748 [para:100635.2.1,100518.1.2.1.1,demod:100624] equal(sk_c2,inverse(sk_c7)) | equal(sk_c1,inverse(sk_c7)).
% 100948 [para:100651.1.1,100333.1.1] equal(inverse(sk_c3),sk_c4) | equal(identity,sk_c6).
% 100961 [para:100948.1.1,100602.1.1.2] equal(multiply(sk_c3,sk_c4),identity) | equal(identity,sk_c6).
% 101173 [para:100961.1.1,100328.1.1] equal(inverse(sk_c1),sk_c7) | equal(identity,sk_c6).
% 101174 [para:100316.1.1,100961.2.1] equal(multiply(sk_c5,sk_c6),sk_c7) | equal(identity,sk_c6).
% 101175 [para:100322.1.1,100961.2.1] equal(multiply(sk_c7,sk_c5),sk_c6) | equal(identity,sk_c6).
% 101176 [para:100334.1.1,100961.2.1] equal(multiply(sk_c1,sk_c7),sk_c6) | equal(identity,sk_c6).
% 101186 [para:100961.1.1,100642.1.1] equal(sk_c1,inverse(sk_c7)) | equal(identity,sk_c6).
% 101195 [para:101173.2.2,100331.1.1.1,demod:100310] equal(inverse(sk_c1),sk_c7) | equal(sk_c7,sk_c5).
% 101203 [para:101173.1.1,100602.1.1.2] equal(multiply(sk_c1,sk_c7),identity) | equal(identity,sk_c6).
% 101237 [para:101186.2.2,100644.1.1.1,demod:100310] equal(sk_c1,inverse(sk_c7)) | equal(sk_c7,sk_c5).
% 101281 [para:101195.2.1,100636.1.2.1] equal(sk_c2,inverse(sk_c5)) | equal(inverse(sk_c1),sk_c7).
% 101354 [para:101237.1.2,100518.1.2.1.1,demod:100624] equal(sk_c7,inverse(sk_c1)) | equal(sk_c7,sk_c5).
% 101362 [para:101237.2.1,100748.1.2.1] equal(sk_c2,inverse(sk_c5)) | equal(sk_c1,inverse(sk_c7)).
% 101518 [para:101281.1.2,100518.1.2.1.1,demod:100624] equal(sk_c5,inverse(sk_c2)) | equal(inverse(sk_c1),sk_c7).
% 101540 [para:101362.1.2,100518.1.2.1.1,demod:100624] equal(sk_c5,inverse(sk_c2)) | equal(sk_c1,inverse(sk_c7)).
% 101674 [para:100330.1.2,101518.2.1] equal(inverse(sk_c1),sk_c7) | equal(sk_c5,sk_c7).
% 101684 [para:101674.1.1,100518.1.2.1.1,demod:100624] equal(sk_c1,inverse(sk_c7)) | equal(sk_c5,sk_c7).
% 102045 [para:100317.2.2,101174.2.1.2,demod:100624] equal(multiply(sk_c5,sk_c6),sk_c7) | equal(sk_c2,sk_c7).
% 102046 [para:100319.2.2,101174.2.1.1,demod:100310] equal(multiply(sk_c5,sk_c6),sk_c7) | equal(sk_c7,sk_c5).
% 102054 [para:100323.2.2,101175.2.1.2,demod:100624] equal(multiply(sk_c7,sk_c5),sk_c6) | equal(sk_c2,sk_c7).
% 102085 [para:101203.1.1,101176.1.1] equal(identity,sk_c6).
% 102087 [para:102085.1.2,100318.1.1.2,demod:100624] equal(inverse(sk_c2),sk_c7) | equal(sk_c5,sk_c7).
% 102116 [para:102087.2.2,100635.1.2.1] equal(sk_c1,inverse(sk_c5)) | equal(inverse(sk_c2),sk_c7).
% 103782 [para:102085.1.2,102046.1.1.2,demod:100624] equal(sk_c5,sk_c7) | equal(sk_c7,sk_c5).
% 103790 [para:102045.2.1,102046.2.2] equal(multiply(sk_c5,sk_c6),sk_c7) | equal(sk_c2,sk_c5).
% 103835 [para:103782.1.2,101237.1.2.1] equal(sk_c1,inverse(sk_c5)) | equal(sk_c7,sk_c5).
% 103841 [para:103782.2.1,101684.1.2.1] equal(sk_c1,inverse(sk_c5)) | equal(sk_c5,sk_c7).
% 103997 [para:103835.1.2,100518.1.2.1.1,demod:100624] equal(sk_c5,inverse(sk_c1)) | equal(sk_c7,sk_c5).
% 104018 [para:101540.2.1,103835.2.2.1] equal(sk_c1,inverse(sk_c5)) | equal(sk_c5,inverse(sk_c2)).
% 104024 [para:103841.1.2,100518.1.2.1.1,demod:100624] equal(sk_c5,inverse(sk_c1)) | equal(sk_c5,sk_c7).
% 104234 [para:103997.1.2,101354.1.2] equal(sk_c7,sk_c5).
% 104282 [para:104024.1.2,101674.1.1] equal(sk_c5,sk_c7).
% 104332 [para:104018.1.2,100518.1.2.1.1,demod:100624] equal(sk_c5,inverse(sk_c1)) | equal(sk_c5,inverse(sk_c2)).
% 104455 [para:102054.2.2,104234.1.1] equal(multiply(sk_c7,sk_c5),sk_c6) | equal(sk_c2,sk_c5).
% 104693 [para:100317.2.1,103790.2.1.1] equal(multiply(sk_c5,sk_c6),sk_c7).
% 104700 [para:104693.1.1,100312.1.1.1] equal(multiply(sk_c7,X),multiply(sk_c5,multiply(sk_c6,X))).
% 104701 [para:104693.1.1,100464.1.2.2] equal(sk_c6,multiply(inverse(sk_c5),sk_c7)).
% 105153 [para:100602.1.1,104700.1.2.2,demod:100624] equal(multiply(sk_c7,inverse(sk_c6)),sk_c5).
% 105157 [para:102085.1.2,104700.1.2.2.1,demod:100310] equal(multiply(sk_c7,X),multiply(sk_c5,X)).
% 105178 [para:104234.1.1,105153.1.1.1] equal(multiply(sk_c5,inverse(sk_c6)),sk_c5).
% 105194 [para:105178.1.1,100464.1.2.2,demod:100311] equal(inverse(sk_c6),identity).
% 105201 [para:105194.1.1,100464.1.2.1,demod:100310] equal(X,multiply(sk_c6,X)).
% 105224 [para:105157.1.1,100602.1.1] equal(multiply(sk_c5,inverse(sk_c7)),identity).
% 105293 [para:105224.1.1,100464.1.2.2,demod:100624] equal(inverse(sk_c7),inverse(sk_c5)).
% 105300 [para:100468.1.1,105224.2.2.2,demod:100624,105157,105201,105293] equal(inverse(sk_c5),sk_c5) | equal(inverse(sk_c2),sk_c7).
% 105538 [para:105300.1.1,102116.1.2] equal(inverse(sk_c2),sk_c7) | equal(sk_c1,sk_c5).
% 105576 [para:105538.1.1,100518.1.2.1.1,demod:100624,105293] equal(sk_c2,inverse(sk_c5)) | equal(sk_c1,sk_c5).
% 105599 [para:105576.1.2,100518.1.2.1.1,demod:100624] equal(sk_c5,inverse(sk_c2)) | equal(sk_c1,sk_c5).
% 105684 [para:105599.2.1,104332.1.2.1] equal(sk_c5,inverse(sk_c5)) | equal(sk_c5,inverse(sk_c2)).
% 110941 [para:100311.1.1,100578.1.2.2,demod:100624] equal(X,inverse(multiply(inverse(multiply(Y,X)),Y))).
% 110942 [para:100311.1.1,100578.1.2.2.2,demod:100624] equal(X,multiply(inverse(multiply(Y,inverse(X))),Y)).
% 112234 [para:104455.1.1,110941.1.2.1.1.1,demod:105293,100310,105194] equal(sk_c5,inverse(sk_c5)) | equal(sk_c2,sk_c5).
% 112279 [para:110941.1.2,110941.1.2.1.1] equal(X,inverse(multiply(Y,inverse(multiply(X,Y))))).
% 112602 [para:105684.2.1,112234.2.2.1] equal(sk_c5,inverse(sk_c5)).
% 112603 [para:112602.1.2,100311.1.1.1] equal(multiply(sk_c5,sk_c5),identity).
% 112609 [para:112602.1.2,104701.1.2.1] equal(sk_c6,multiply(sk_c5,sk_c7)).
% 114857 [para:105157.1.1,110942.1.2.1.1] equal(X,multiply(inverse(multiply(sk_c5,inverse(X))),sk_c7)).
% 114887 [para:112279.1.2,114857.1.2.1] equal(multiply(X,sk_c5),multiply(X,sk_c7)).
% 116565 [para:104234.1.1,100342.1.1.1,factor:cut:104693] -equal(multiply(sk_c6,sk_c7),sk_c5) | -equal(multiply(sk_c5,sk_c5),sk_c6) | -equal(multiply(sk_c5,sk_c7),sk_c6) | -equal(inverse(sk_c5),sk_c5) | -equal(inverse(sk_c5),sk_c7) | -equal(multiply(X,sk_c7),sk_c6) | -equal(inverse(X),sk_c7).
% 116566 [para:102085.1.2,116565.1.1.1,demod:114887,112602,112609,112603,100310,cut:104234,cut:102085,cut:100309,cut:100309,cut:104282] -equal(multiply(X,sk_c5),sk_c6) | -equal(inverse(X),sk_c7).
% 116569 [para:100311.1.1,116566.1.1,demod:112602,cut:102085,cut:104282] 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: 78
%
%
% ***GANDALF_FOUND_A_REFUTATION***
%
% Global statistics over all passes:
%
% given clauses: 15413
% derived clauses: 2989134
% kept clauses: 74657
% kept size sum: 179869
% kept mid-nuclei: 14553
% kept new demods: 942
% forw unit-subs: 1938937
% forw double-subs: 696504
% forw overdouble-subs: 238914
% backward subs: 11340
% fast unit cutoff: 10387
% full unit cutoff: 0
% dbl unit cutoff: 11305
% real runtime : 120.77
% process. runtime: 120.23
% specific non-discr-tree subsumption statistics:
% tried: 20592995
% length fails: 1234049
% strength fails: 5923134
% predlist fails: 1969625
% aux str. fails: 4197153
% by-lit fails: 4778857
% full subs tried: 516370
% full subs fail: 473806
%
% ; 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/GRP277-1+eq_r.in")
%
%------------------------------------------------------------------------------