%------------------------------------------------------------------------------
% File : Gandalf---c-2.6
% Problem : GRP249-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 : art05.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 179.6s
% Output : Assurance 179.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/GRP249-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 23)
% (binary-unit 12 #f)
% (binary-unit-uniteq 12 #f)
% (binary-posweight-kb-big-order 60 #f 3 23)
% (binary-posweight-lex-big-order 30 #f 3 23)
% (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_c9),sk_c8) | -equal(inverse(X),sk_c9) | -equal(multiply(Y,sk_c8),sk_c7) | -equal(inverse(Y),sk_c8) | -equal(inverse(Z),sk_c9) | -equal(multiply(Z,sk_c7),sk_c9) | -equal(inverse(sk_c8),sk_c7) | -equal(inverse(U),sk_c9) | -equal(multiply(U,sk_c8),sk_c9) | -equal(multiply(V,W),sk_c8) | -equal(inverse(V),W) | -equal(multiply(W,sk_c7),sk_c8).
% was split for some strategies as:
% -equal(multiply(V,W),sk_c8) | -equal(inverse(V),W) | -equal(multiply(W,sk_c7),sk_c8).
% -equal(inverse(U),sk_c9) | -equal(multiply(U,sk_c8),sk_c9).
% -equal(inverse(Z),sk_c9) | -equal(multiply(Z,sk_c7),sk_c9).
% -equal(multiply(Y,sk_c8),sk_c7) | -equal(inverse(Y),sk_c8).
% -equal(multiply(X,sk_c9),sk_c8) | -equal(inverse(X),sk_c9).
% -equal(inverse(sk_c8),sk_c7).
%
% ********* EMPTY CLAUSE DERIVED *********
%
%
% timer checkpoints: c(41,40,0,88,0,1,106267,5,1502,106269,1,1502,106269,50,1502,106269,40,1502,106316,0,1502,117701,3,1803,118377,4,1953,119005,1,2103,119005,50,2103,119005,40,2103,119052,0,2103,119350,3,2414,119359,4,2556,119373,5,2704,119373,1,2704,119373,50,2704,119373,40,2704,119420,0,2704,144906,3,4205,145985,4,4955,147053,5,5705,147054,1,5705,147054,50,5706,147054,40,5706,147101,0,5706,164760,3,6457,165565,4,6832,166301,5,7207,166302,1,7207,166302,50,7207,166302,40,7207,166349,0,7207,187507,3,7960,188012,4,8333,188659,5,8708,188660,1,8708,188660,50,8708,188660,40,8708,188707,0,8708,239028,3,12609,240284,4,14559,241098,5,16509,241099,1,16509,241099,50,16511,241099,40,16511,241146,0,16511)
%
%
% START OF PROOF
% 208448 [?] ?
% 228163 [?] ?
% 235383 [?] ?
% 241100 [] equal(X,X).
% 241101 [] equal(multiply(identity,X),X).
% 241102 [] equal(multiply(inverse(X),X),identity).
% 241103 [] equal(multiply(multiply(X,Y),Z),multiply(X,multiply(Y,Z))).
% 241106 [] equal(multiply(sk_c3,sk_c7),sk_c9) | equal(inverse(sk_c5),sk_c6).
% 241107 [] equal(multiply(sk_c3,sk_c7),sk_c9) | equal(multiply(sk_c5,sk_c6),sk_c8).
% 241108 [] equal(multiply(sk_c3,sk_c7),sk_c9) | equal(multiply(sk_c4,sk_c8),sk_c9).
% 241109 [] equal(multiply(sk_c3,sk_c7),sk_c9) | equal(inverse(sk_c4),sk_c9).
% 241110 [] equal(multiply(sk_c3,sk_c7),sk_c9) | equal(inverse(sk_c8),sk_c7).
% 241112 [] equal(inverse(sk_c3),sk_c9) | equal(inverse(sk_c5),sk_c6).
% 241113 [] equal(multiply(sk_c5,sk_c6),sk_c8) | equal(inverse(sk_c3),sk_c9).
% 241114 [] equal(multiply(sk_c4,sk_c8),sk_c9) | equal(inverse(sk_c3),sk_c9).
% 241115 [] equal(inverse(sk_c3),sk_c9) | equal(inverse(sk_c4),sk_c9).
% 241116 [] equal(inverse(sk_c3),sk_c9) | equal(inverse(sk_c8),sk_c7).
% 241118 [] equal(inverse(sk_c2),sk_c8) | equal(inverse(sk_c5),sk_c6).
% 241119 [] equal(multiply(sk_c5,sk_c6),sk_c8) | equal(inverse(sk_c2),sk_c8).
% 241120 [] equal(multiply(sk_c4,sk_c8),sk_c9) | equal(inverse(sk_c2),sk_c8).
% 241121 [] equal(inverse(sk_c2),sk_c8) | equal(inverse(sk_c4),sk_c9).
% 241122 [] equal(inverse(sk_c2),sk_c8) | equal(inverse(sk_c8),sk_c7).
% 241124 [] equal(multiply(sk_c2,sk_c8),sk_c7) | equal(inverse(sk_c5),sk_c6).
% 241125 [] equal(multiply(sk_c2,sk_c8),sk_c7) | equal(multiply(sk_c5,sk_c6),sk_c8).
% 241126 [] equal(multiply(sk_c2,sk_c8),sk_c7) | equal(multiply(sk_c4,sk_c8),sk_c9).
% 241127 [] equal(multiply(sk_c2,sk_c8),sk_c7) | equal(inverse(sk_c4),sk_c9).
% 241128 [] equal(multiply(sk_c2,sk_c8),sk_c7) | equal(inverse(sk_c8),sk_c7).
% 241132 [] equal(multiply(sk_c4,sk_c8),sk_c9) | equal(inverse(sk_c1),sk_c9).
% 241133 [] equal(inverse(sk_c1),sk_c9) | equal(inverse(sk_c4),sk_c9).
% 241134 [] equal(inverse(sk_c1),sk_c9) | equal(inverse(sk_c8),sk_c7).
% 241138 [] equal(multiply(sk_c1,sk_c9),sk_c8) | equal(multiply(sk_c4,sk_c8),sk_c9).
% 241139 [] equal(multiply(sk_c1,sk_c9),sk_c8) | equal(inverse(sk_c4),sk_c9).
% 241140 [] equal(multiply(sk_c1,sk_c9),sk_c8) | equal(inverse(sk_c8),sk_c7).
% 241141 [] -equal(inverse(sk_c8),sk_c7) | $spltprd0($spltcnst36) | -equal(multiply(X,sk_c7),sk_c8) | -equal(multiply(Y,X),sk_c8) | -equal(inverse(Y),X).
% 241142 [] $spltprd0($spltcnst37) | -equal(multiply(X,sk_c8),sk_c9) | -equal(inverse(X),sk_c9).
% 241143 [] $spltprd0($spltcnst38) | -equal(multiply(X,sk_c7),sk_c9) | -equal(inverse(X),sk_c9).
% 241144 [] $spltprd0($spltcnst39) | -equal(multiply(X,sk_c8),sk_c7) | -equal(inverse(X),sk_c8).
% 241145 [] $spltprd0($spltcnst40) | -equal(multiply(X,sk_c9),sk_c8) | -equal(inverse(X),sk_c9).
% 241146 [] -$spltprd0($spltcnst37) | -$spltprd0($spltcnst36) | -$spltprd0($spltcnst38) | -$spltprd0($spltcnst40) | -$spltprd0($spltcnst39).
% 241148 [input:241141,factor:cut:235383] -equal(multiply(sk_c7,sk_c7),sk_c8) | -equal(inverse(sk_c8),sk_c7) | $spltprd0($spltcnst36).
% 241179 [para:241134.2.1,241102.1.1.1] equal(multiply(sk_c7,sk_c8),identity) | equal(inverse(sk_c1),sk_c9).
% 241221 [para:241140.2.1,241102.1.1.1] equal(multiply(sk_c7,sk_c8),identity) | equal(multiply(sk_c1,sk_c9),sk_c8).
% 241277 [para:241114.1.1,241142.2.1,cut:241100] -equal(inverse(sk_c4),sk_c9) | equal(inverse(sk_c3),sk_c9) | $spltprd0($spltcnst37).
% 241278 [para:241108.2.1,241142.2.1,cut:241100] equal(multiply(sk_c3,sk_c7),sk_c9) | -equal(inverse(sk_c4),sk_c9) | $spltprd0($spltcnst37).
% 241279 [para:241120.1.1,241142.2.1,cut:241100] -equal(inverse(sk_c4),sk_c9) | equal(inverse(sk_c2),sk_c8) | $spltprd0($spltcnst37).
% 241284 [para:241132.1.1,241142.2.1,cut:241100] -equal(inverse(sk_c4),sk_c9) | equal(inverse(sk_c1),sk_c9) | $spltprd0($spltcnst37).
% 241287 [para:241126.2.1,241142.2.1,cut:241100] equal(multiply(sk_c2,sk_c8),sk_c7) | -equal(inverse(sk_c4),sk_c9) | $spltprd0($spltcnst37).
% 241290 [para:241138.2.1,241142.2.1,cut:241100] equal(multiply(sk_c1,sk_c9),sk_c8) | -equal(inverse(sk_c4),sk_c9) | $spltprd0($spltcnst37).
% 241301 [para:241115.2.1,241277.1.1,cut:241100] equal(inverse(sk_c3),sk_c9) | $spltprd0($spltcnst37).
% 241313 [para:241106.1.1,241143.2.1,cut:241100,binarycut:241112] equal(inverse(sk_c5),sk_c6) | $spltprd0($spltcnst38).
% 241315 [para:241109.1.1,241143.2.1,cut:241100,binarycut:241115] equal(inverse(sk_c4),sk_c9) | $spltprd0($spltcnst38).
% 241317 [para:241110.1.1,241143.2.1,cut:241100,binarycut:241116] equal(inverse(sk_c8),sk_c7) | $spltprd0($spltcnst38).
% 241318 [para:241107.1.1,241143.2.1,cut:241100] equal(multiply(sk_c5,sk_c6),sk_c8) | -equal(inverse(sk_c3),sk_c9) | $spltprd0($spltcnst38).
% 241321 [para:241108.1.1,241143.2.1,cut:241100] equal(multiply(sk_c4,sk_c8),sk_c9) | -equal(inverse(sk_c3),sk_c9) | $spltprd0($spltcnst38).
% 241341 [para:241102.1.1,241144.2.1,cut:208448] -equal(inverse(inverse(sk_c8)),sk_c8) | $spltprd0($spltcnst39).
% 241350 [para:241128.1.1,241144.2.1,cut:241100,binarycut:241122] equal(inverse(sk_c8),sk_c7) | $spltprd0($spltcnst39).
% 241364 [para:241102.1.1,241145.2.1,cut:228163] -equal(inverse(inverse(sk_c9)),sk_c9) | $spltprd0($spltcnst40).
% 241379 [para:241350.1.1,241102.1.1.1] equal(multiply(sk_c7,sk_c8),identity) | $spltprd0($spltcnst39).
% 241382 [para:241102.1.1,241103.1.1.1,demod:241101] equal(X,multiply(inverse(Y),multiply(Y,X))).
% 241469 [para:241350.1.1,241341.1.1.1] -equal(inverse(sk_c7),sk_c8) | $spltprd0($spltcnst39).
% 241489 [para:241102.1.1,241382.1.2.2] equal(X,multiply(inverse(inverse(X)),identity)).
% 241592 [para:241379.1.1,241382.1.2.2] equal(sk_c8,multiply(inverse(sk_c7),identity)) | $spltprd0($spltcnst39).
% 241596 [para:241382.1.2,241382.1.2.2] equal(multiply(X,Y),multiply(inverse(inverse(X)),Y)).
% 241734 [para:241596.1.2,241102.1.1] equal(multiply(X,inverse(X)),identity).
% 241795 [para:241596.1.2,241489.1.2] equal(X,multiply(X,identity)).
% 241803 [para:241795.1.2,241102.1.1] equal(inverse(identity),identity).
% 241804 [para:241795.1.2,241489.1.2] equal(X,inverse(inverse(X))).
% 241819 [para:241592.1.2,241795.1.2,binarycut:241469] $spltprd0($spltcnst39).
% 241851 [para:241122.1.1,241804.1.2.1] equal(sk_c2,inverse(sk_c8)) | equal(inverse(sk_c8),sk_c7).
% 241868 [para:241128.2.1,241804.1.2.1] equal(multiply(sk_c2,sk_c8),sk_c7) | equal(sk_c8,inverse(sk_c7)).
% 241893 [para:241804.1.2,241364.1.1,cut:241100] $spltprd0($spltcnst40).
% 241900 [para:241118.1.1,241734.1.1.2] equal(multiply(sk_c2,sk_c8),identity) | equal(inverse(sk_c5),sk_c6).
% 241901 [para:241118.2.1,241734.1.1.2] equal(multiply(sk_c5,sk_c6),identity) | equal(inverse(sk_c2),sk_c8).
% 241948 [para:241313.1.1,241734.1.1.2] equal(multiply(sk_c5,sk_c6),identity) | $spltprd0($spltcnst38).
% 242177 [para:241851.1.2,241489.1.2.1.1,demod:241795] equal(sk_c8,inverse(sk_c2)) | equal(inverse(sk_c8),sk_c7).
% 242499 [para:242177.2.1,241489.1.2.1.1,demod:241795] equal(sk_c8,inverse(sk_c7)) | equal(sk_c8,inverse(sk_c2)).
% 242867 [para:241109.2.1,241278.2.1,cut:241100] equal(multiply(sk_c3,sk_c7),sk_c9) | $spltprd0($spltcnst37).
% 242873 [para:242867.1.1,241382.1.2.2] equal(sk_c7,multiply(inverse(sk_c3),sk_c9)) | $spltprd0($spltcnst37).
% 242899 [para:241121.2.1,241279.1.1,cut:241100] equal(inverse(sk_c2),sk_c8) | $spltprd0($spltcnst37).
% 242906 [para:242899.1.1,241734.1.1.2] equal(multiply(sk_c2,sk_c8),identity) | $spltprd0($spltcnst37).
% 243055 [para:241133.2.1,241284.1.1,cut:241100] equal(inverse(sk_c1),sk_c9) | $spltprd0($spltcnst37).
% 243060 [para:243055.1.1,241489.1.2.1.1,demod:241795] equal(sk_c1,inverse(sk_c9)) | $spltprd0($spltcnst37).
% 243130 [para:241127.2.1,241287.2.1,cut:241100] equal(multiply(sk_c2,sk_c8),sk_c7) | $spltprd0($spltcnst37).
% 243137 [para:243130.1.1,242906.1.1] equal(sk_c7,identity) | $spltprd0($spltcnst37).
% 243156 [para:243137.1.1,242867.1.1.2,demod:241795] equal(sk_c3,sk_c9) | $spltprd0($spltcnst37).
% 243208 [para:243156.1.2,243060.1.2.1] equal(sk_c1,inverse(sk_c3)) | $spltprd0($spltcnst37).
% 243279 [para:243208.1.2,242873.1.2.1] equal(sk_c7,multiply(sk_c1,sk_c9)) | $spltprd0($spltcnst37).
% 243287 [para:241139.2.1,241290.2.1,cut:241100] equal(multiply(sk_c1,sk_c9),sk_c8) | $spltprd0($spltcnst37).
% 243347 [para:243287.1.1,243279.1.2] equal(sk_c7,sk_c8) | $spltprd0($spltcnst37).
% 243393 [para:243347.1.1,242867.1.1.2] equal(multiply(sk_c3,sk_c8),sk_c9) | $spltprd0($spltcnst37).
% 243571 [para:243393.1.1,241142.2.1,cut:241100,binarycut:241301] $spltprd0($spltcnst37).
% 243572 [binary:241146,243571,cut:241893,cut:241819] -$spltprd0($spltcnst36) | -$spltprd0($spltcnst38).
% 243580 [para:241113.2.1,241318.2.1,cut:241100] equal(multiply(sk_c5,sk_c6),sk_c8) | $spltprd0($spltcnst38).
% 243589 [para:243580.1.1,241948.1.1] equal(sk_c8,identity) | $spltprd0($spltcnst38).
% 243612 [para:243589.1.1,241317.1.1.1,demod:241803] equal(identity,sk_c7) | $spltprd0($spltcnst38).
% 243640 [para:243612.1.2,241143.2.1.2,demod:241795] $spltprd0($spltcnst38) | -equal(inverse(X),sk_c9) | -equal(X,sk_c9).
% 243744 [para:241114.2.1,241321.2.1,cut:241100] equal(multiply(sk_c4,sk_c8),sk_c9) | $spltprd0($spltcnst38).
% 244036 [para:243589.1.1,243744.1.1.2,demod:241795] equal(sk_c4,sk_c9) | $spltprd0($spltcnst38).
% 244643 [para:241315.1.1,243640.2.1,cut:241100,binarycut:244036] $spltprd0($spltcnst38).
% 249875 [para:241900.1.1,241124.1.1] equal(inverse(sk_c5),sk_c6) | equal(identity,sk_c7).
% 249899 [para:249875.1.1,241734.1.1.2] equal(multiply(sk_c5,sk_c6),identity) | equal(identity,sk_c7).
% 250819 [para:241901.1.1,241119.1.1] equal(inverse(sk_c2),sk_c8) | equal(identity,sk_c8).
% 250833 [para:241122.2.2,250819.2.1.1,demod:241803] equal(inverse(sk_c2),sk_c8) | equal(identity,sk_c7).
% 250840 [para:250819.1.1,241489.1.2.1.1,demod:241795] equal(sk_c2,inverse(sk_c8)) | equal(identity,sk_c8).
% 250876 [para:250833.1.1,241734.1.1.2] equal(multiply(sk_c2,sk_c8),identity) | equal(identity,sk_c7).
% 254610 [para:250876.1.1,241128.1.1] equal(inverse(sk_c8),sk_c7) | equal(identity,sk_c7).
% 254612 [para:250876.1.1,241125.1.1] equal(multiply(sk_c5,sk_c6),sk_c8) | equal(identity,sk_c7).
% 260437 [para:254612.1.1,249899.1.1] equal(sk_c8,identity) | equal(identity,sk_c7).
% 260465 [para:260437.2.2,241179.1.1.1,demod:241101] equal(inverse(sk_c1),sk_c9) | equal(sk_c8,identity).
% 260477 [para:260437.2.2,241221.1.1.1,demod:241101] equal(multiply(sk_c1,sk_c9),sk_c8) | equal(sk_c8,identity).
% 260507 [para:260437.1.1,254610.1.1.1,demod:241803] equal(identity,sk_c7).
% 261052 [para:260465.1.1,241734.1.1.2] equal(multiply(sk_c1,sk_c9),identity) | equal(sk_c8,identity).
% 280060 [para:260477.1.1,261052.1.1] equal(sk_c8,identity).
% 280102 [para:280060.1.1,241868.1.1.2,demod:241795] equal(sk_c8,inverse(sk_c7)) | equal(sk_c2,sk_c7).
% 280119 [para:280060.1.1,250840.1.2.1,demod:241803] equal(sk_c2,identity) | equal(identity,sk_c8).
% 280240 [para:280119.1.1,250819.1.1.1,demod:241803] equal(identity,sk_c8).
% 283539 [para:242499.2.1,280102.2.2.1] equal(sk_c8,inverse(sk_c7)).
% 283541 [para:283539.1.2,241382.1.2.1] equal(X,multiply(sk_c8,multiply(sk_c7,X))).
% 283542 [para:283539.1.2,241489.1.2.1.1,demod:241795] equal(sk_c7,inverse(sk_c8)).
% 284018 [para:280060.1.1,283541.1.2.1,demod:241101] equal(X,multiply(sk_c7,X)).
% 284035 [para:284018.1.2,241148.1.1,demod:283542,cut:241100] -equal(sk_c7,sk_c8) | $spltprd0($spltcnst36).
% 284050 [para:260507.1.2,284035.1.1,cut:280240] $spltprd0($spltcnst36).
% 284051 [binary:243572,284050,cut:244643] 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 lex ordering for equality
% preferring bigger arities for lex ordering
% using clause demodulation
% seconds given: 51
%
%
% old unit clauses discarded
%
% ***GANDALF_FOUND_A_REFUTATION***
%
% Global statistics over all passes:
%
% given clauses: 18636
% derived clauses: 4142690
% kept clauses: 155363
% kept size sum: 0
% kept mid-nuclei: 104232
% kept new demods: 278
% forw unit-subs: 1424260
% forw double-subs: 1946436
% forw overdouble-subs: 210271
% backward subs: 8177
% fast unit cutoff: 16536
% full unit cutoff: 0
% dbl unit cutoff: 4414
% real runtime : 188.40
% process. runtime: 187.85
% specific non-discr-tree subsumption statistics:
% tried: 9292946
% length fails: 732009
% strength fails: 2935461
% predlist fails: 178412
% aux str. fails: 1100419
% by-lit fails: 1719177
% full subs tried: 1502273
% full subs fail: 1363277
%
% ; 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/GRP249-1+eq_r.in")
%
%------------------------------------------------------------------------------