%------------------------------------------------------------------------------
% File : Gandalf---c-2.6
% Problem : GRP272-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 : art10.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 20.0s
% Output : Assurance 20.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/GRP272-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(Y,sk_c6),sk_c5) | -equal(inverse(Y),sk_c6) | -equal(multiply(sk_c6,sk_c7),sk_c5) | -equal(inverse(Z),sk_c7) | -equal(multiply(Z,sk_c6),sk_c7) | -equal(inverse(U),sk_c6) | -equal(multiply(U,sk_c5),sk_c6).
% was split for some strategies as:
% -equal(inverse(U),sk_c6) | -equal(multiply(U,sk_c5),sk_c6).
% -equal(inverse(Z),sk_c7) | -equal(multiply(Z,sk_c6),sk_c7).
% -equal(multiply(Y,sk_c6),sk_c5) | -equal(inverse(Y),sk_c6).
% -equal(multiply(X,sk_c7),sk_c6) | -equal(inverse(X),sk_c7).
% -equal(multiply(sk_c7,sk_c5),sk_c6).
% -equal(multiply(sk_c6,sk_c7),sk_c5).
%
% ********* EMPTY CLAUSE DERIVED *********
%
%
% timer checkpoints: c(30,40,0,65,0,1,538,50,4,573,0,4,1061,50,8,1096,0,8,1589,50,12,1624,0,12,2123,50,18,2158,0,18,2664,50,24,2699,0,24,3213,50,36,3248,0,36,3770,50,58,3805,0,59,4337,50,109,4372,0,109,4914,50,219,4949,0,219,5503,50,415,5538,0,415,6104,50,781,6104,40,781,6139,0,781,16847,3,1082,17554,4,1232,18192,5,1382,18193,1,1382,18193,50,1382,18193,40,1382,18228,0,1382,18396,3,1690,18404,4,1833,18412,5,1983,18412,1,1983,18412,50,1983,18412,40,1983,18447,0,1983)
%
%
% START OF PROOF
% 18283 [?] ?
% 18413 [] equal(X,X).
% 18414 [] equal(multiply(identity,X),X).
% 18415 [] equal(multiply(inverse(X),X),identity).
% 18416 [] equal(multiply(multiply(X,Y),Z),multiply(X,multiply(Y,Z))).
% 18418 [] equal(multiply(sk_c4,sk_c5),sk_c6) | equal(inverse(sk_c2),sk_c6).
% 18419 [] equal(inverse(sk_c2),sk_c6) | equal(inverse(sk_c4),sk_c6).
% 18420 [] equal(multiply(sk_c3,sk_c6),sk_c7) | equal(inverse(sk_c2),sk_c6).
% 18421 [] equal(inverse(sk_c2),sk_c6) | equal(inverse(sk_c3),sk_c7).
% 18422 [] equal(multiply(sk_c6,sk_c7),sk_c5) | equal(inverse(sk_c2),sk_c6).
% 18423 [] equal(multiply(sk_c2,sk_c6),sk_c5) | equal(multiply(sk_c4,sk_c5),sk_c6).
% 18424 [] equal(multiply(sk_c2,sk_c6),sk_c5) | equal(inverse(sk_c4),sk_c6).
% 18425 [] equal(multiply(sk_c2,sk_c6),sk_c5) | equal(multiply(sk_c3,sk_c6),sk_c7).
% 18426 [] equal(multiply(sk_c2,sk_c6),sk_c5) | equal(inverse(sk_c3),sk_c7).
% 18427 [] equal(multiply(sk_c2,sk_c6),sk_c5) | equal(multiply(sk_c6,sk_c7),sk_c5).
% 18428 [] equal(multiply(sk_c7,sk_c5),sk_c6) | equal(multiply(sk_c4,sk_c5),sk_c6).
% 18430 [] equal(multiply(sk_c7,sk_c5),sk_c6) | equal(multiply(sk_c3,sk_c6),sk_c7).
% 18431 [] equal(multiply(sk_c7,sk_c5),sk_c6) | equal(inverse(sk_c3),sk_c7).
% 18432 [] equal(multiply(sk_c7,sk_c5),sk_c6) | equal(multiply(sk_c6,sk_c7),sk_c5).
% 18433 [] equal(multiply(sk_c4,sk_c5),sk_c6) | equal(inverse(sk_c1),sk_c7).
% 18434 [] equal(inverse(sk_c1),sk_c7) | equal(inverse(sk_c4),sk_c6).
% 18435 [] equal(multiply(sk_c3,sk_c6),sk_c7) | equal(inverse(sk_c1),sk_c7).
% 18436 [] equal(inverse(sk_c1),sk_c7) | equal(inverse(sk_c3),sk_c7).
% 18437 [] equal(multiply(sk_c6,sk_c7),sk_c5) | equal(inverse(sk_c1),sk_c7).
% 18438 [] equal(multiply(sk_c1,sk_c7),sk_c6) | equal(multiply(sk_c4,sk_c5),sk_c6).
% 18439 [] equal(multiply(sk_c1,sk_c7),sk_c6) | equal(inverse(sk_c4),sk_c6).
% 18440 [] equal(multiply(sk_c1,sk_c7),sk_c6) | equal(multiply(sk_c3,sk_c6),sk_c7).
% 18441 [] equal(multiply(sk_c1,sk_c7),sk_c6) | equal(inverse(sk_c3),sk_c7).
% 18442 [] equal(multiply(sk_c1,sk_c7),sk_c6) | equal(multiply(sk_c6,sk_c7),sk_c5).
% 18443 [] -equal(multiply(sk_c7,sk_c5),sk_c6) | -equal(multiply(sk_c6,sk_c7),sk_c5) | $spltprd0($spltcnst13) | -equal(multiply(X,sk_c5),sk_c6) | -equal(inverse(X),sk_c6).
% 18444 [] $spltprd0($spltcnst14) | -equal(multiply(X,sk_c6),sk_c7) | -equal(inverse(X),sk_c7).
% 18445 [] $spltprd0($spltcnst15) | -equal(multiply(X,sk_c6),sk_c5) | -equal(inverse(X),sk_c6).
% 18446 [] $spltprd0($spltcnst16) | -equal(multiply(X,sk_c7),sk_c6) | -equal(inverse(X),sk_c7).
% 18447 [] -$spltprd0($spltcnst14) | -$spltprd0($spltcnst13) | -$spltprd0($spltcnst16) | -$spltprd0($spltcnst15).
% 18448 [input:18443,factor] -equal(multiply(sk_c7,sk_c5),sk_c6) | -equal(multiply(sk_c6,sk_c7),sk_c5) | -equal(inverse(sk_c7),sk_c6) | $spltprd0($spltcnst13).
% 18450 [para:18419.1.1,18415.1.1.1] equal(multiply(sk_c6,sk_c2),identity) | equal(inverse(sk_c4),sk_c6).
% 18451 [para:18419.2.1,18415.1.1.1] equal(multiply(sk_c6,sk_c4),identity) | equal(inverse(sk_c2),sk_c6).
% 18453 [para:18421.1.1,18415.1.1.1] equal(multiply(sk_c6,sk_c2),identity) | equal(inverse(sk_c3),sk_c7).
% 18454 [para:18421.2.1,18415.1.1.1] equal(multiply(sk_c7,sk_c3),identity) | equal(inverse(sk_c2),sk_c6).
% 18457 [para:18434.1.1,18415.1.1.1] equal(multiply(sk_c7,sk_c1),identity) | equal(inverse(sk_c4),sk_c6).
% 18458 [para:18434.2.1,18415.1.1.1] equal(multiply(sk_c6,sk_c4),identity) | equal(inverse(sk_c1),sk_c7).
% 18460 [para:18436.1.1,18415.1.1.1] equal(multiply(sk_c7,sk_c1),identity) | equal(inverse(sk_c3),sk_c7).
% 18461 [para:18436.2.1,18415.1.1.1] equal(multiply(sk_c7,sk_c3),identity) | equal(inverse(sk_c1),sk_c7).
% 18520 [para:18414.1.1,18444.2.1] -equal(inverse(identity),sk_c7) | -equal(sk_c6,sk_c7) | $spltprd0($spltcnst14).
% 18522 [para:18420.1.1,18444.2.1,cut:18413] -equal(inverse(sk_c3),sk_c7) | equal(inverse(sk_c2),sk_c6) | $spltprd0($spltcnst14).
% 18526 [para:18435.1.1,18444.2.1,cut:18413] -equal(inverse(sk_c3),sk_c7) | equal(inverse(sk_c1),sk_c7) | $spltprd0($spltcnst14).
% 18528 [para:18425.2.1,18444.2.1,cut:18413] equal(multiply(sk_c2,sk_c6),sk_c5) | -equal(inverse(sk_c3),sk_c7) | $spltprd0($spltcnst14).
% 18530 [para:18430.2.1,18444.2.1,cut:18413] equal(multiply(sk_c7,sk_c5),sk_c6) | -equal(inverse(sk_c3),sk_c7) | $spltprd0($spltcnst14).
% 18531 [para:18440.2.1,18444.2.1,cut:18413] equal(multiply(sk_c1,sk_c7),sk_c6) | -equal(inverse(sk_c3),sk_c7) | $spltprd0($spltcnst14).
% 18536 [para:18421.2.1,18522.1.1,cut:18413] equal(inverse(sk_c2),sk_c6) | $spltprd0($spltcnst14).
% 18538 [para:18536.1.1,18415.1.1.1] equal(multiply(sk_c6,sk_c2),identity) | $spltprd0($spltcnst14).
% 18547 [para:18424.1.1,18445.2.1,cut:18413,binarycut:18419] equal(inverse(sk_c4),sk_c6) | $spltprd0($spltcnst15).
% 18549 [para:18426.1.1,18445.2.1,cut:18413,binarycut:18421] equal(inverse(sk_c3),sk_c7) | $spltprd0($spltcnst15).
% 18550 [para:18423.1.1,18445.2.1,cut:18413] equal(multiply(sk_c4,sk_c5),sk_c6) | -equal(inverse(sk_c2),sk_c6) | $spltprd0($spltcnst15).
% 18552 [para:18425.1.1,18445.2.1,cut:18413] equal(multiply(sk_c3,sk_c6),sk_c7) | -equal(inverse(sk_c2),sk_c6) | $spltprd0($spltcnst15).
% 18554 [para:18427.1.1,18445.2.1,cut:18413] equal(multiply(sk_c6,sk_c7),sk_c5) | -equal(inverse(sk_c2),sk_c6) | $spltprd0($spltcnst15).
% 18559 [para:18547.1.1,18415.1.1.1] equal(multiply(sk_c6,sk_c4),identity) | $spltprd0($spltcnst15).
% 18561 [para:18549.1.1,18415.1.1.1] equal(multiply(sk_c7,sk_c3),identity) | $spltprd0($spltcnst15).
% 18566 [para:18414.1.1,18446.2.1] -equal(inverse(identity),sk_c7) | -equal(sk_c7,sk_c6) | $spltprd0($spltcnst16).
% 18571 [para:18439.1.1,18446.2.1,cut:18413,binarycut:18434] equal(inverse(sk_c4),sk_c6) | $spltprd0($spltcnst16).
% 18573 [para:18441.1.1,18446.2.1,cut:18413,binarycut:18436] equal(inverse(sk_c3),sk_c7) | $spltprd0($spltcnst16).
% 18576 [para:18438.1.1,18446.2.1,cut:18413] equal(multiply(sk_c4,sk_c5),sk_c6) | -equal(inverse(sk_c1),sk_c7) | $spltprd0($spltcnst16).
% 18577 [para:18440.1.1,18446.2.1,cut:18413] equal(multiply(sk_c3,sk_c6),sk_c7) | -equal(inverse(sk_c1),sk_c7) | $spltprd0($spltcnst16).
% 18578 [para:18442.1.1,18446.2.1,cut:18413] equal(multiply(sk_c6,sk_c7),sk_c5) | -equal(inverse(sk_c1),sk_c7) | $spltprd0($spltcnst16).
% 18581 [para:18571.1.1,18415.1.1.1] equal(multiply(sk_c6,sk_c4),identity) | $spltprd0($spltcnst16).
% 18583 [para:18573.1.1,18415.1.1.1] equal(multiply(sk_c7,sk_c3),identity) | $spltprd0($spltcnst16).
% 18587 [para:18415.1.1,18416.1.1.1,demod:18414] equal(X,multiply(inverse(Y),multiply(Y,X))).
% 18602 [para:18450.1.1,18416.1.1.1,demod:18414] equal(inverse(sk_c4),sk_c6) | equal(X,multiply(sk_c6,multiply(sk_c2,X))).
% 18605 [para:18451.1.1,18416.1.1.1,demod:18414] equal(inverse(sk_c2),sk_c6) | equal(X,multiply(sk_c6,multiply(sk_c4,X))).
% 18606 [para:18453.1.1,18416.1.1.1,demod:18414] equal(inverse(sk_c3),sk_c7) | equal(X,multiply(sk_c6,multiply(sk_c2,X))).
% 18607 [para:18454.1.1,18416.1.1.1,demod:18414] equal(inverse(sk_c2),sk_c6) | equal(X,multiply(sk_c7,multiply(sk_c3,X))).
% 18608 [para:18457.1.1,18416.1.1.1,demod:18414] equal(inverse(sk_c4),sk_c6) | equal(X,multiply(sk_c7,multiply(sk_c1,X))).
% 18609 [para:18458.1.1,18416.1.1.1,demod:18414] equal(inverse(sk_c1),sk_c7) | equal(X,multiply(sk_c6,multiply(sk_c4,X))).
% 18612 [para:18460.1.1,18416.1.1.1,demod:18414] equal(inverse(sk_c3),sk_c7) | equal(X,multiply(sk_c7,multiply(sk_c1,X))).
% 18641 [para:18422.1.1,18587.1.2.2] equal(sk_c7,multiply(inverse(sk_c6),sk_c5)) | equal(inverse(sk_c2),sk_c6).
% 18657 [para:18437.1.1,18587.1.2.2] equal(sk_c7,multiply(inverse(sk_c6),sk_c5)) | equal(inverse(sk_c1),sk_c7).
% 18675 [para:18458.1.1,18587.1.2.2] equal(sk_c4,multiply(inverse(sk_c6),identity)) | equal(inverse(sk_c1),sk_c7).
% 18678 [para:18427.2.1,18587.1.2.2] equal(sk_c7,multiply(inverse(sk_c6),sk_c5)) | equal(multiply(sk_c2,sk_c6),sk_c5).
% 18681 [para:18461.1.1,18587.1.2.2] equal(sk_c3,multiply(inverse(sk_c7),identity)) | equal(inverse(sk_c1),sk_c7).
% 18688 [para:18432.2.1,18587.1.2.2] equal(sk_c7,multiply(inverse(sk_c6),sk_c5)) | equal(multiply(sk_c7,sk_c5),sk_c6).
% 18694 [para:18442.2.1,18587.1.2.2] equal(sk_c7,multiply(inverse(sk_c6),sk_c5)) | equal(multiply(sk_c1,sk_c7),sk_c6).
% 18699 [para:18538.1.1,18587.1.2.2] equal(sk_c2,multiply(inverse(sk_c6),identity)) | $spltprd0($spltcnst14).
% 18700 [para:18559.1.1,18587.1.2.2] equal(sk_c4,multiply(inverse(sk_c6),identity)) | $spltprd0($spltcnst15).
% 18701 [para:18561.1.1,18587.1.2.2] equal(sk_c3,multiply(inverse(sk_c7),identity)) | $spltprd0($spltcnst15).
% 18702 [para:18581.1.1,18587.1.2.2] equal(sk_c4,multiply(inverse(sk_c6),identity)) | $spltprd0($spltcnst16).
% 18703 [para:18583.1.1,18587.1.2.2] equal(sk_c3,multiply(inverse(sk_c7),identity)) | $spltprd0($spltcnst16).
% 18709 [para:18699.1.2,18416.1.1.1,demod:18414] $spltprd0($spltcnst14) | equal(multiply(sk_c2,X),multiply(inverse(sk_c6),X)).
% 18711 [para:18700.1.2,18416.1.1.1,demod:18414] $spltprd0($spltcnst15) | equal(multiply(sk_c4,X),multiply(inverse(sk_c6),X)).
% 18725 [para:18701.1.2,18416.1.1.1,demod:18414] $spltprd0($spltcnst15) | equal(multiply(sk_c3,X),multiply(inverse(sk_c7),X)).
% 18727 [para:18702.1.2,18416.1.1.1,demod:18414] $spltprd0($spltcnst16) | equal(multiply(sk_c4,X),multiply(inverse(sk_c6),X)).
% 18742 [para:18703.1.2,18416.1.1.1,demod:18414] $spltprd0($spltcnst16) | equal(multiply(sk_c3,X),multiply(inverse(sk_c7),X)).
% 18786 [para:18709.2.2,18415.1.1] equal(multiply(sk_c2,sk_c6),identity) | $spltprd0($spltcnst14).
% 18968 [para:18711.2.2,18415.1.1] equal(multiply(sk_c4,sk_c6),identity) | $spltprd0($spltcnst15).
% 18972 [para:18711.2.2,18587.1.2] $spltprd0($spltcnst15) | equal(X,multiply(sk_c4,multiply(sk_c6,X))).
% 18979 [para:18968.1.1,18587.1.2.2] equal(sk_c6,multiply(inverse(sk_c4),identity)) | $spltprd0($spltcnst15).
% 18994 [para:18979.1.2,18416.1.1.1,demod:18414] $spltprd0($spltcnst15) | equal(multiply(sk_c6,X),multiply(inverse(sk_c4),X)).
% 19024 [para:18725.2.2,18415.1.1] equal(multiply(sk_c3,sk_c7),identity) | $spltprd0($spltcnst15).
% 19071 [para:18727.2.2,18587.1.2] $spltprd0($spltcnst16) | equal(X,multiply(sk_c4,multiply(sk_c6,X))).
% 19120 [para:18742.2.2,18415.1.1] equal(multiply(sk_c3,sk_c7),identity) | $spltprd0($spltcnst16).
% 19184 [para:18587.1.2,18994.2.2] $spltprd0($spltcnst15) | equal(multiply(sk_c6,multiply(sk_c4,X)),X).
% 19243 [para:18436.2.1,18526.1.1,cut:18413] equal(inverse(sk_c1),sk_c7) | $spltprd0($spltcnst14).
% 19247 [para:19243.1.1,18587.1.2.1] $spltprd0($spltcnst14) | equal(X,multiply(sk_c7,multiply(sk_c1,X))).
% 19304 [para:18426.2.1,18528.2.1,cut:18413] equal(multiply(sk_c2,sk_c6),sk_c5) | $spltprd0($spltcnst14).
% 19314 [para:19304.1.1,18786.1.1] equal(sk_c5,identity) | $spltprd0($spltcnst14).
% 19348 [para:18431.2.1,18530.2.1,cut:18413] equal(multiply(sk_c7,sk_c5),sk_c6) | $spltprd0($spltcnst14).
% 19357 [para:19314.1.1,19348.1.1.2] equal(multiply(sk_c7,identity),sk_c6) | $spltprd0($spltcnst14).
% 19402 [para:18441.2.1,18531.2.1,cut:18413] equal(multiply(sk_c1,sk_c7),sk_c6) | $spltprd0($spltcnst14).
% 19409 [para:19402.1.1,19247.2.2.2] equal(sk_c7,multiply(sk_c7,sk_c6)) | $spltprd0($spltcnst14).
% 19415 [para:19409.1.2,18587.1.2.2,demod:18415] equal(sk_c6,identity) | $spltprd0($spltcnst14).
% 19429 [para:19415.1.1,18538.1.1.1,demod:18414] equal(sk_c2,identity) | $spltprd0($spltcnst14).
% 19444 [para:19415.1.1,19409.1.2.2] equal(sk_c7,multiply(sk_c7,identity)) | $spltprd0($spltcnst14).
% 19458 [para:19429.1.1,18536.1.1.1] equal(inverse(identity),sk_c6) | $spltprd0($spltcnst14).
% 19528 [para:19458.1.1,18520.1.1] -equal(sk_c6,sk_c7) | $spltprd0($spltcnst14).
% 19646 [para:19444.1.2,19357.1.1] equal(sk_c7,sk_c6) | $spltprd0($spltcnst14).
% 19683 [para:19646.1.1,19528.1.2,cut:18413] $spltprd0($spltcnst14).
% 19684 [binary:18447,19683] -$spltprd0($spltcnst16) | -$spltprd0($spltcnst15) | -$spltprd0($spltcnst13).
% 19686 [para:18418.2.1,18550.2.1,cut:18413] equal(multiply(sk_c4,sk_c5),sk_c6) | $spltprd0($spltcnst15).
% 19737 [para:18420.2.1,18552.2.1,cut:18413] equal(multiply(sk_c3,sk_c6),sk_c7) | $spltprd0($spltcnst15).
% 19741 [para:18422.2.1,18554.2.1,cut:18413] equal(multiply(sk_c6,sk_c7),sk_c5) | $spltprd0($spltcnst15).
% 19746 [para:19686.1.1,19184.2.1.2] equal(multiply(sk_c6,sk_c6),sk_c5) | $spltprd0($spltcnst15).
% 19759 [para:19741.1.1,18972.2.2.2] equal(sk_c7,multiply(sk_c4,sk_c5)) | $spltprd0($spltcnst15).
% 19785 [para:19759.1.2,19686.1.1] equal(sk_c7,sk_c6) | $spltprd0($spltcnst15).
% 19801 [para:19785.1.1,19024.1.1.2] equal(multiply(sk_c3,sk_c6),identity) | $spltprd0($spltcnst15).
% 19847 [para:19801.1.1,19737.1.1] equal(identity,sk_c7) | $spltprd0($spltcnst15).
% 19871 [para:19847.1.2,19785.1.1] equal(identity,sk_c6) | $spltprd0($spltcnst15).
% 19911 [?] ?
% 19926 [para:19871.1.2,19746.1.1.1,demod:18414,binarycut:19911] $spltprd0($spltcnst15).
% 19931 [para:18433.2.1,18576.2.1,cut:18413] equal(multiply(sk_c4,sk_c5),sk_c6) | $spltprd0($spltcnst16).
% 19933 [para:18435.2.1,18577.2.1,cut:18413] equal(multiply(sk_c3,sk_c6),sk_c7) | $spltprd0($spltcnst16).
% 19935 [para:18437.2.1,18578.2.1,cut:18413] equal(multiply(sk_c6,sk_c7),sk_c5) | $spltprd0($spltcnst16).
% 19958 [para:19935.1.1,19071.2.2.2] equal(sk_c7,multiply(sk_c4,sk_c5)) | $spltprd0($spltcnst16).
% 20011 [para:19958.1.2,19931.1.1] equal(sk_c7,sk_c6) | $spltprd0($spltcnst16).
% 20027 [para:20011.1.1,19120.1.1.2] equal(multiply(sk_c3,sk_c6),identity) | $spltprd0($spltcnst16).
% 20111 [para:20027.1.1,19933.1.1] equal(identity,sk_c7) | $spltprd0($spltcnst16).
% 20126 [para:20111.1.2,18566.1.2,cut:18283,binarycut:20011] $spltprd0($spltcnst16).
% 20128 [binary:19684,20126,cut:19926] -$spltprd0($spltcnst13).
% 20163 [para:18424.1.1,18602.2.2.2] equal(sk_c6,multiply(sk_c6,sk_c5)) | equal(inverse(sk_c4),sk_c6).
% 20179 [para:18418.1.1,18605.2.2.2] equal(sk_c5,multiply(sk_c6,sk_c6)) | equal(inverse(sk_c2),sk_c6).
% 20184 [para:18426.1.1,18606.2.2.2] equal(sk_c6,multiply(sk_c6,sk_c5)) | equal(inverse(sk_c3),sk_c7).
% 20190 [para:18420.1.1,18607.2.2.2] equal(sk_c6,multiply(sk_c7,sk_c7)) | equal(inverse(sk_c2),sk_c6).
% 20195 [para:18439.1.1,18608.2.2.2] equal(sk_c7,multiply(sk_c7,sk_c6)) | equal(inverse(sk_c4),sk_c6).
% 20201 [para:18433.1.1,18609.2.2.2] equal(sk_c5,multiply(sk_c6,sk_c6)) | equal(inverse(sk_c1),sk_c7).
% 20217 [para:18441.1.1,18612.2.2.2] equal(sk_c7,multiply(sk_c7,sk_c6)) | equal(inverse(sk_c3),sk_c7).
% 20316 [para:20163.1.2,18587.1.2.2,demod:18415] equal(inverse(sk_c4),sk_c6) | equal(sk_c5,identity).
% 20357 [para:20179.1.2,18587.1.2.2] equal(sk_c6,multiply(inverse(sk_c6),sk_c5)) | equal(inverse(sk_c2),sk_c6).
% 20362 [para:20184.1.2,18587.1.2.2,demod:18415] equal(inverse(sk_c3),sk_c7) | equal(sk_c5,identity).
% 20370 [para:20362.2.1,18431.1.1.2] equal(multiply(sk_c7,identity),sk_c6) | equal(inverse(sk_c3),sk_c7).
% 20404 [para:20195.1.2,18587.1.2.2,demod:18415] equal(inverse(sk_c4),sk_c6) | equal(sk_c6,identity).
% 20411 [para:20404.2.1,18424.1.1.2] equal(multiply(sk_c2,identity),sk_c5) | equal(inverse(sk_c4),sk_c6).
% 20412 [para:20404.2.1,18450.1.1.1,demod:18414] equal(inverse(sk_c4),sk_c6) | equal(sk_c2,identity).
% 20426 [para:18602.2.1,20412.2.2.2.1,demod:18414] equal(inverse(sk_c4),sk_c6) | equal(X,multiply(sk_c6,X)).
% 20512 [para:20163.1.2,20426.2.2] equal(inverse(sk_c4),sk_c6) | equal(sk_c5,sk_c6).
% 20514 [para:20512.1.1,18415.1.1.1] equal(multiply(sk_c6,sk_c4),identity) | equal(sk_c5,sk_c6).
% 20516 [para:20316.2.1,20512.2.1] equal(inverse(sk_c4),sk_c6) | equal(identity,sk_c6).
% 20519 [para:20516.1.1,18415.1.1.1] equal(multiply(sk_c6,sk_c4),identity) | equal(identity,sk_c6).
% 20528 [para:20519.1.1,18587.1.2.2] equal(sk_c4,multiply(inverse(sk_c6),identity)) | equal(identity,sk_c6).
% 20544 [para:20217.1.2,18587.1.2.2,demod:18415] equal(inverse(sk_c3),sk_c7) | equal(sk_c6,identity).
% 20552 [para:20544.2.1,18426.1.1.2] equal(multiply(sk_c2,identity),sk_c5) | equal(inverse(sk_c3),sk_c7).
% 20553 [para:20544.2.1,18453.1.1.1,demod:18414] equal(inverse(sk_c3),sk_c7) | equal(sk_c2,identity).
% 20562 [para:20544.2.1,20217.1.2.2] equal(sk_c7,multiply(sk_c7,identity)) | equal(inverse(sk_c3),sk_c7).
% 20565 [para:20553.2.1,18421.1.1.1] equal(inverse(identity),sk_c6) | equal(inverse(sk_c3),sk_c7).
% 20569 [para:18606.2.1,20553.2.2.2.1,demod:18414] equal(inverse(sk_c3),sk_c7) | equal(X,multiply(sk_c6,X)).
% 20648 [para:20184.1.2,20569.2.2] equal(inverse(sk_c3),sk_c7) | equal(sk_c5,sk_c6).
% 20658 [para:20362.2.1,20648.2.1] equal(inverse(sk_c3),sk_c7) | equal(identity,sk_c6).
% 20660 [para:20658.1.1,18415.1.1.1] equal(multiply(sk_c7,sk_c3),identity) | equal(identity,sk_c6).
% 20668 [para:20660.1.1,18587.1.2.2] equal(sk_c3,multiply(inverse(sk_c7),identity)) | equal(identity,sk_c6).
% 20748 [para:20412.2.1,20411.1.1.1,demod:18414] equal(inverse(sk_c4),sk_c6) | equal(identity,sk_c5).
% 20754 [para:20748.1.1,18415.1.1.1] equal(multiply(sk_c6,sk_c4),identity) | equal(identity,sk_c5).
% 20762 [para:20754.1.1,18587.1.2.2] equal(sk_c4,multiply(inverse(sk_c6),identity)) | equal(identity,sk_c5).
% 20919 [para:20553.2.1,20552.1.1.1,demod:18414] equal(inverse(sk_c3),sk_c7) | equal(identity,sk_c5).
% 20921 [para:20919.1.1,18415.1.1.1] equal(multiply(sk_c7,sk_c3),identity) | equal(identity,sk_c5).
% 20924 [para:20921.1.1,18587.1.2.2] equal(sk_c3,multiply(inverse(sk_c7),identity)) | equal(identity,sk_c5).
% 20936 [para:20562.1.2,20370.1.1] equal(inverse(sk_c3),sk_c7) | equal(sk_c7,sk_c6).
% 20939 [para:20936.1.1,18415.1.1.1] equal(multiply(sk_c7,sk_c3),identity) | equal(sk_c7,sk_c6).
% 20945 [para:20936.2.1,18460.1.1.1] equal(multiply(sk_c6,sk_c1),identity) | equal(inverse(sk_c3),sk_c7).
% 20965 [para:20939.1.1,18587.1.2.2] equal(sk_c3,multiply(inverse(sk_c7),identity)) | equal(sk_c7,sk_c6).
% 21304 [para:20544.2.1,20945.1.1.1,demod:18414] equal(inverse(sk_c3),sk_c7) | equal(sk_c1,identity).
% 21307 [para:21304.2.1,18436.1.1.1] equal(inverse(identity),sk_c7) | equal(inverse(sk_c3),sk_c7).
% 21326 [para:20565.1.1,21307.1.1] equal(inverse(sk_c3),sk_c7) | equal(sk_c6,sk_c7).
% 22286 [para:20357.1.2,18641.1.2] equal(inverse(sk_c2),sk_c6) | equal(sk_c7,sk_c6).
% 22302 [para:22286.2.1,20190.1.2.1] equal(sk_c6,multiply(sk_c6,sk_c7)) | equal(inverse(sk_c2),sk_c6).
% 22404 [para:22302.1.2,18422.1.1] equal(inverse(sk_c2),sk_c6) | equal(sk_c6,sk_c5).
% 22406 [para:22302.1.2,18587.1.2.2,demod:18415] equal(inverse(sk_c2),sk_c6) | equal(sk_c7,identity).
% 22419 [para:22404.2.2,20357.1.2.2,demod:18415] equal(inverse(sk_c2),sk_c6) | equal(sk_c6,identity).
% 22438 [para:22419.2.1,18422.1.1.1,demod:18414] equal(inverse(sk_c2),sk_c6) | equal(sk_c7,sk_c5).
% 22439 [para:22419.2.1,18451.1.1.1,demod:18414] equal(inverse(sk_c2),sk_c6) | equal(sk_c4,identity).
% 22479 [para:22438.2.1,20190.1.2.2] equal(sk_c6,multiply(sk_c7,sk_c5)) | equal(inverse(sk_c2),sk_c6).
% 22492 [para:18419.2.1,22439.2.1.1] equal(inverse(identity),sk_c6) | equal(inverse(sk_c2),sk_c6).
% 23304 [para:22479.1.2,18448.1.1,cut:18413,cut:20128,binarycut:18422] -equal(inverse(sk_c7),sk_c6) | equal(inverse(sk_c2),sk_c6).
% 23309 [para:22406.2.1,23304.1.1.1,binarycut:22492] equal(inverse(sk_c2),sk_c6).
% 23310 [para:23309.1.1,18415.1.1.1] equal(multiply(sk_c6,sk_c2),identity).
% 23311 [para:23309.1.1,18587.1.2.1] equal(X,multiply(sk_c6,multiply(sk_c2,X))).
% 23312 [para:23310.1.1,18587.1.2.2] equal(sk_c2,multiply(inverse(sk_c6),identity)).
% 23350 [para:23312.1.2,18416.1.1.1,demod:18414] equal(multiply(sk_c2,X),multiply(inverse(sk_c6),X)).
% 23362 [para:23312.1.2,20762.1.2] equal(sk_c4,sk_c2) | equal(identity,sk_c5).
% 23374 [para:23312.1.2,18675.1.2] equal(inverse(sk_c1),sk_c7) | equal(sk_c4,sk_c2).
% 24180 [para:23350.1.2,18415.1.1] equal(multiply(sk_c2,sk_c6),identity).
% 24181 [para:23350.1.2,18587.1.2] equal(X,multiply(sk_c2,multiply(sk_c6,X))).
% 24199 [para:23350.1.2,18657.1.2] equal(sk_c7,multiply(sk_c2,sk_c5)) | equal(inverse(sk_c1),sk_c7).
% 24219 [para:23350.1.2,18678.1.2,demod:24180] equal(sk_c7,multiply(sk_c2,sk_c5)) | equal(identity,sk_c5).
% 24233 [para:23350.1.2,23312.1.2] equal(sk_c2,multiply(sk_c2,identity)).
% 24241 [para:24180.1.1,18587.1.2.2,demod:23309] equal(sk_c6,multiply(sk_c6,identity)).
% 24319 [para:20201.1.2,24181.1.2.2] equal(sk_c6,multiply(sk_c2,sk_c5)) | equal(inverse(sk_c1),sk_c7).
% 24864 [para:23362.1.2,24219.1.2.1] equal(sk_c7,multiply(sk_c4,sk_c5)) | equal(identity,sk_c5).
% 27068 [para:18423.1.2,24864.2.1,demod:24180] equal(sk_c7,sk_c6) | equal(identity,sk_c5).
% 27143 [para:27068.1.1,20924.1.2.1.1,demod:23312] equal(sk_c3,sk_c2) | equal(identity,sk_c5).
% 27201 [para:27143.1.2,24180.1.1.1] equal(multiply(sk_c3,sk_c6),identity) | equal(identity,sk_c5).
% 28445 [para:18425.1.1,27201.2.1,demod:24180] equal(identity,sk_c7) | equal(identity,sk_c5).
% 28522 [para:28445.1.2,27068.1.1] equal(identity,sk_c6) | equal(identity,sk_c5).
% 28683 [para:18427.1.2,28522.2.1.1,demod:24180,18414] equal(sk_c7,sk_c5) | equal(identity,sk_c5).
% 28824 [para:28683.1.1,28445.1.2] equal(identity,sk_c5).
% 28847 [para:28824.1.2,18657.1.2.2,demod:23312] equal(inverse(sk_c1),sk_c7) | equal(sk_c7,sk_c2).
% 28851 [para:28824.1.2,18688.1.2.2,demod:23312] equal(multiply(sk_c7,sk_c5),sk_c6) | equal(sk_c7,sk_c2).
% 28853 [para:28824.1.2,18694.1.2.2,demod:23312] equal(multiply(sk_c1,sk_c7),sk_c6) | equal(sk_c7,sk_c2).
% 28945 [para:28847.2.1,18681.1.2.1.1,demod:24241,23309] equal(inverse(sk_c1),sk_c7) | equal(sk_c3,sk_c6).
% 29815 [para:28824.1.2,28851.1.1.2] equal(multiply(sk_c7,identity),sk_c6) | equal(sk_c7,sk_c2).
% 31714 [para:28824.1.2,24319.1.2.2,demod:24233] equal(inverse(sk_c1),sk_c7) | equal(sk_c6,sk_c2).
% 31715 [para:24319.1.2,24199.1.2] equal(inverse(sk_c1),sk_c7) | equal(sk_c7,sk_c6).
% 31722 [para:31714.2.2,23309.1.1.1] equal(inverse(sk_c6),sk_c6) | equal(inverse(sk_c1),sk_c7).
% 31747 [para:23374.2.2,31714.2.2] equal(inverse(sk_c1),sk_c7) | equal(sk_c4,sk_c6).
% 31763 [para:31715.2.1,18443.1.1.1,cut:20128,binarycut:18437,factor:binarycut:31722] -equal(multiply(sk_c6,sk_c5),sk_c6) | equal(inverse(sk_c1),sk_c7).
% 31786 [para:31747.2.1,18433.1.1.1,binarycut:31763] equal(inverse(sk_c1),sk_c7).
% 31791 [para:31786.1.1,18415.1.1.1] equal(multiply(sk_c7,sk_c1),identity).
% 31792 [para:31786.1.1,18587.1.2.1] equal(X,multiply(sk_c7,multiply(sk_c1,X))).
% 31796 [para:31791.1.1,18587.1.2.2] equal(sk_c1,multiply(inverse(sk_c7),identity)).
% 31812 [para:31796.1.2,18416.1.1.1,demod:18414] equal(multiply(sk_c1,X),multiply(inverse(sk_c7),X)).
% 33203 [para:31812.1.2,18415.1.1] equal(multiply(sk_c1,sk_c7),identity).
% 33316 [para:33203.1.1,18438.1.1] equal(multiply(sk_c4,sk_c5),sk_c6) | equal(identity,sk_c6).
% 33320 [para:33203.1.1,18442.1.1] equal(multiply(sk_c6,sk_c7),sk_c5) | equal(identity,sk_c6).
% 33322 [para:33203.1.1,18587.1.2.2,demod:31786] equal(sk_c7,multiply(sk_c7,identity)).
% 33361 [para:33203.1.1,28853.1.1] equal(identity,sk_c6) | equal(sk_c7,sk_c2).
% 33418 [para:33322.1.2,29815.1.1] equal(sk_c7,sk_c6) | equal(sk_c7,sk_c2).
% 33455 [para:33361.2.1,20668.1.2.1.1,demod:24241,23309] equal(sk_c3,sk_c6) | equal(identity,sk_c6).
% 33705 [para:33418.2.1,20965.1.2.1.1,demod:24241,23309] equal(sk_c3,sk_c6) | equal(sk_c7,sk_c6).
% 33775 [para:18441.1.1,33455.2.1.1,demod:33203] equal(inverse(sk_c6),sk_c7) | equal(identity,sk_c6).
% 34243 [para:33705.2.1,31796.1.2.1.1,demod:23312] equal(sk_c1,sk_c2) | equal(sk_c3,sk_c6).
% 34802 [para:34243.1.1,28945.1.1.1,demod:23309] equal(sk_c6,sk_c7) | equal(sk_c3,sk_c6).
% 35162 [para:34802.2.1,21326.1.1.1] equal(inverse(sk_c6),sk_c7) | equal(sk_c6,sk_c7).
% 36185 [para:33775.1.1,20528.1.2.1,demod:33322] equal(sk_c4,sk_c7) | equal(identity,sk_c6).
% 36251 [para:36185.1.2,18448.1.1.1,cut:20128,binarycut:33320,binarycut:33316] -equal(inverse(sk_c7),sk_c6) | equal(identity,sk_c6).
% 37595 [para:28853.2.1,36251.1.1.1,demod:33203,23309,cut:18413] equal(identity,sk_c6).
% 37627 [para:37595.1.2,20514.1.1.1,demod:18414] equal(sk_c4,identity) | equal(sk_c5,sk_c6).
% 37676 [para:37595.1.2,23310.1.1.1,demod:18414] equal(sk_c2,identity).
% 37678 [para:37595.1.2,24241.1.2.1,demod:18414] equal(sk_c6,identity).
% 37733 [para:37676.1.1,23309.1.1.1] equal(inverse(identity),sk_c6).
% 37734 [para:37676.1.1,23311.1.2.2.1,demod:18414] equal(X,multiply(sk_c6,X)).
% 37793 [para:37678.1.1,23312.1.2.1.1,demod:24241,37733] equal(sk_c2,sk_c6).
% 37798 [para:37678.1.1,35162.1.1.1,demod:37733] equal(sk_c6,sk_c7).
% 37804 [para:37793.1.1,23309.1.1.1] equal(inverse(sk_c6),sk_c6).
% 37929 [para:37798.1.2,31791.1.1.1,demod:37734] equal(sk_c1,identity).
% 37960 [para:37929.1.1,31791.1.1.2,demod:33322] equal(sk_c7,identity).
% 37966 [para:37929.1.1,31792.1.2.2.1,demod:18414] equal(X,multiply(sk_c7,X)).
% 38067 [para:18428.1.1,37627.2.1.1,demod:37966,18414] equal(sk_c5,sk_c6).
% 38071 [para:38067.1.1,18448.1.1.2,demod:37734,37966,cut:18413,cut:20128] -equal(inverse(sk_c7),sk_c6) | -equal(sk_c7,sk_c5).
% 38764 [para:37798.1.2,38071.1.1.1,demod:37804,cut:18413] -equal(sk_c7,sk_c5).
% 38799 [para:28824.1.2,38764.1.2,cut:37960] 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
% clause length limited to 19
% clause depth limited to 3
% seconds given: 30
%
%
% ***GANDALF_FOUND_A_REFUTATION***
%
% Global statistics over all passes:
%
% given clauses: 5407
% derived clauses: 488562
% kept clauses: 28822
% kept size sum: 429069
% kept mid-nuclei: 3047
% kept new demods: 763
% forw unit-subs: 248978
% forw double-subs: 182497
% forw overdouble-subs: 16250
% backward subs: 1600
% fast unit cutoff: 1820
% full unit cutoff: 0
% dbl unit cutoff: 1573
% real runtime : 27.93
% process. runtime: 27.90
% specific non-discr-tree subsumption statistics:
% tried: 1422714
% length fails: 252103
% strength fails: 466356
% predlist fails: 2708
% aux str. fails: 272659
% by-lit fails: 140295
% full subs tried: 161191
% full subs fail: 152955
%
% ; 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/GRP272-1+eq_r.in")
%
%------------------------------------------------------------------------------