%------------------------------------------------------------------------------
% File : Gandalf---c-2.6
% Problem : GRP309-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 : art08.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 59.5s
% Output : Assurance 59.5s
% 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/GRP309-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(sk_c7,sk_c6),sk_c5) | -equal(inverse(sk_c7),sk_c5) | -equal(multiply(sk_c5,sk_c6),sk_c7) | -equal(multiply(sk_c7,X),sk_c6) | -equal(multiply(Y,sk_c7),X) | -equal(inverse(Y),sk_c7) | -equal(multiply(Z,sk_c7),sk_c6) | -equal(inverse(Z),sk_c7) | -equal(multiply(U,sk_c6),sk_c5) | -equal(inverse(U),sk_c6).
% was split for some strategies as:
% -equal(multiply(U,sk_c6),sk_c5) | -equal(inverse(U),sk_c6).
% -equal(multiply(Z,sk_c7),sk_c6) | -equal(inverse(Z),sk_c7).
% -equal(multiply(sk_c7,X),sk_c6) | -equal(multiply(Y,sk_c7),X) | -equal(inverse(Y),sk_c7).
% -equal(multiply(sk_c7,sk_c6),sk_c5).
% -equal(inverse(sk_c7),sk_c5).
% -equal(multiply(sk_c5,sk_c6),sk_c7).
%
% ********* EMPTY CLAUSE DERIVED *********
%
%
% timer checkpoints: c(26,40,0,56,0,0,2257,50,18,2287,0,18,4930,50,40,4960,0,40,8101,50,70,8131,0,70,11476,50,95,11506,0,95,15102,50,131,15132,0,131,18932,50,189,18962,0,190,23015,50,298,23045,0,298,27352,50,464,27382,0,464,31992,50,749,32022,0,749,36936,4,1294,40660,5,1450,40660,1,1452,40660,50,1452,40660,40,1452,40690,0,1452,51482,3,1753,52250,4,1903,52945,5,2053,52946,1,2053,52946,50,2053,52946,40,2053,52976,0,2053,53269,3,2354,53279,4,2520,53287,5,2654,53287,1,2654,53287,50,2654,53287,40,2654,53317,0,2654,65602,3,4155,65870,50,4245,65870,40,4245,65900,0,4245,94542,3,4996,94951,4,5371,95403,1,5746,95403,50,5747,95403,40,5747,95433,0,5747,99160,50,5891,99160,40,5891,99190,0,5891)
%
%
% START OF PROOF
% 64362 [?] ?
% 64364 [?] ?
% 65511 [?] ?
% 65555 [?] ?
% 98937 [?] ?
% 98948 [?] ?
% 99161 [] equal(X,X).
% 99162 [] equal(multiply(identity,X),X).
% 99163 [] equal(multiply(inverse(X),X),identity).
% 99164 [] equal(multiply(multiply(X,Y),Z),multiply(X,multiply(Y,Z))).
% 99167 [] equal(multiply(sk_c4,sk_c6),sk_c5) | equal(inverse(sk_c1),sk_c7).
% 99168 [] equal(inverse(sk_c1),sk_c7) | equal(inverse(sk_c3),sk_c7).
% 99169 [] equal(multiply(sk_c3,sk_c7),sk_c6) | equal(inverse(sk_c1),sk_c7).
% 99171 [] equal(multiply(sk_c1,sk_c7),sk_c2) | equal(multiply(sk_c4,sk_c6),sk_c5).
% 99172 [] equal(multiply(sk_c1,sk_c7),sk_c2) | equal(inverse(sk_c3),sk_c7).
% 99173 [] equal(multiply(sk_c1,sk_c7),sk_c2) | equal(multiply(sk_c3,sk_c7),sk_c6).
% 99174 [] equal(multiply(sk_c7,sk_c2),sk_c6) | equal(inverse(sk_c4),sk_c6).
% 99175 [] equal(multiply(sk_c7,sk_c2),sk_c6) | equal(multiply(sk_c4,sk_c6),sk_c5).
% 99176 [] equal(multiply(sk_c7,sk_c2),sk_c6) | equal(inverse(sk_c3),sk_c7).
% 99178 [] equal(multiply(sk_c5,sk_c6),sk_c7).
% 99179 [] equal(inverse(sk_c7),sk_c5) | equal(inverse(sk_c4),sk_c6).
% 99180 [] equal(multiply(sk_c4,sk_c6),sk_c5) | equal(inverse(sk_c7),sk_c5).
% 99181 [] equal(inverse(sk_c7),sk_c5) | equal(inverse(sk_c3),sk_c7).
% 99182 [] equal(multiply(sk_c3,sk_c7),sk_c6) | equal(inverse(sk_c7),sk_c5).
% 99183 [] equal(multiply(sk_c7,sk_c6),sk_c5) | equal(inverse(sk_c4),sk_c6).
% 99184 [] equal(multiply(sk_c7,sk_c6),sk_c5) | equal(multiply(sk_c4,sk_c6),sk_c5).
% 99185 [] equal(multiply(sk_c7,sk_c6),sk_c5) | equal(inverse(sk_c3),sk_c7).
% 99187 [?] ?
% 99188 [] $spltprd0($spltcnst20) | -equal(multiply(X,sk_c7),sk_c6) | -equal(inverse(X),sk_c7).
% 99189 [] $spltprd0($spltcnst21) | -equal(multiply(sk_c7,X),sk_c6) | -equal(multiply(Y,sk_c7),X) | -equal(inverse(Y),sk_c7).
% 99190 [] -$spltprd0($spltcnst20) | -$spltprd0($spltcnst19) | -$spltprd0($spltcnst21).
% 99207 [para:99167.2.1,99163.1.1.1] equal(multiply(sk_c7,sk_c1),identity) | equal(multiply(sk_c4,sk_c6),sk_c5).
% 99251 [input:99187,cut:99161] -equal(multiply(sk_c7,sk_c6),sk_c5) | -equal(inverse(sk_c7),sk_c5) | $spltprd0($spltcnst19) | -equal(multiply(X,sk_c6),sk_c5) | -equal(inverse(X),sk_c6).
% 99253 [para:99183.1.1,99251.1.1,cut:99161,binarycut:99179] equal(inverse(sk_c4),sk_c6) | $spltprd0($spltcnst19) | -equal(multiply(X,sk_c6),sk_c5) | -equal(inverse(X),sk_c6).
% 99255 [para:99185.1.1,99251.1.1,cut:99161,binarycut:99181] equal(inverse(sk_c3),sk_c7) | $spltprd0($spltcnst19) | -equal(multiply(X,sk_c6),sk_c5) | -equal(inverse(X),sk_c6).
% 99268 [para:99172.1.1,99188.2.1,cut:65511,binarycut:99168] equal(inverse(sk_c3),sk_c7) | $spltprd0($spltcnst20).
% 99274 [para:99173.2.1,99188.2.1,cut:99161,binarycut:99268] equal(multiply(sk_c1,sk_c7),sk_c2) | $spltprd0($spltcnst20).
% 99285 [para:99174.1.1,99189.2.1,cut:99161] equal(inverse(sk_c4),sk_c6) | $spltprd0($spltcnst21) | -equal(multiply(X,sk_c7),sk_c2) | -equal(inverse(X),sk_c7).
% 99286 [para:99176.1.1,99189.2.1,cut:99161] equal(inverse(sk_c3),sk_c7) | $spltprd0($spltcnst21) | -equal(multiply(X,sk_c7),sk_c2) | -equal(inverse(X),sk_c7).
% 99314 [para:99178.1.1,99164.1.1.1] equal(multiply(sk_c7,X),multiply(sk_c5,multiply(sk_c6,X))).
% 99315 [para:99163.1.1,99164.1.1.1,demod:99162] equal(X,multiply(inverse(Y),multiply(Y,X))).
% 99357 [para:99274.1.1,99188.2.1,cut:65511] -equal(inverse(sk_c1),sk_c7) | $spltprd0($spltcnst20).
% 99361 [para:99169.2.1,99357.1.1,cut:99161] equal(multiply(sk_c3,sk_c7),sk_c6) | $spltprd0($spltcnst20).
% 99395 [para:99361.1.1,99188.2.1,cut:99161,binarycut:99268] $spltprd0($spltcnst20).
% 99401 [binary:99190,99395] -$spltprd0($spltcnst19) | -$spltprd0($spltcnst21).
% 99405 [para:99163.1.1,99315.1.2.2] equal(X,multiply(inverse(inverse(X)),identity)).
% 99461 [para:99315.1.2,99315.1.2.2] equal(multiply(X,Y),multiply(inverse(inverse(X)),Y)).
% 99478 [para:99461.1.2,99163.1.1] equal(multiply(X,inverse(X)),identity).
% 99505 [para:99461.1.2,99315.1.2] equal(X,multiply(Y,multiply(inverse(Y),X))).
% 99506 [para:99461.1.2,99405.1.2] equal(X,multiply(X,identity)).
% 99511 [para:99506.1.2,99163.1.1] equal(inverse(identity),identity).
% 99512 [para:99506.1.2,99189.2.1,cut:98937] $spltprd0($spltcnst21) | -equal(multiply(X,sk_c7),identity) | -equal(inverse(X),sk_c7).
% 99513 [para:99506.1.2,99405.1.2] equal(X,inverse(inverse(X))).
% 99516 [para:99168.1.1,99513.1.2.1] equal(sk_c1,inverse(sk_c7)) | equal(inverse(sk_c3),sk_c7).
% 99661 [para:99516.1.2,99181.1.1] equal(inverse(sk_c3),sk_c7) | equal(sk_c1,sk_c5).
% 99671 [para:99661.2.1,99168.1.1.1] equal(inverse(sk_c5),sk_c7) | equal(inverse(sk_c3),sk_c7).
% 99898 [para:99162.1.1,99253.3.1,demod:99511,cut:98948,cut:64362] equal(inverse(sk_c4),sk_c6) | $spltprd0($spltcnst19).
% 99901 [binary:99401,99898.2] equal(inverse(sk_c4),sk_c6) | -$spltprd0($spltcnst21).
% 99916 [para:99162.1.1,99255.3.1,demod:99511,cut:98948,cut:64362] equal(inverse(sk_c3),sk_c7) | $spltprd0($spltcnst19).
% 99920 [binary:99401,99916.2] equal(inverse(sk_c3),sk_c7) | -$spltprd0($spltcnst21).
% 100069 [para:99478.1.1,99314.1.2.2,demod:99506] equal(multiply(sk_c7,inverse(sk_c6)),sk_c5).
% 100078 [para:100069.1.1,99315.1.2.2] equal(inverse(sk_c6),multiply(inverse(sk_c7),sk_c5)).
% 100117 [para:99162.1.1,99285.3.1,demod:99511,cut:65555,cut:64364] equal(inverse(sk_c4),sk_c6) | $spltprd0($spltcnst21).
% 100125 [binary:99901.2,100117.2] equal(inverse(sk_c4),sk_c6).
% 100126 [para:100125.1.1,99163.1.1.1] equal(multiply(sk_c6,sk_c4),identity).
% 100128 [para:100125.1.1,99405.1.2.1.1,demod:99506] equal(sk_c4,inverse(sk_c6)).
% 100129 [para:100125.1.1,99478.1.1.2] equal(multiply(sk_c4,sk_c6),identity).
% 100147 [para:99162.1.1,99286.3.1,demod:99511,cut:65555,cut:64364] equal(inverse(sk_c3),sk_c7) | $spltprd0($spltcnst21).
% 100157 [binary:99920.2,100147.2] equal(inverse(sk_c3),sk_c7).
% 100158 [para:100157.1.1,99163.1.1.1] equal(multiply(sk_c7,sk_c3),identity).
% 100160 [para:100157.1.1,99405.1.2.1.1,demod:99506] equal(sk_c3,inverse(sk_c7)).
% 100161 [para:100157.1.1,99478.1.1.2] equal(multiply(sk_c3,sk_c7),identity).
% 100162 [para:100157.1.1,99505.1.2.2.1] equal(X,multiply(sk_c3,multiply(sk_c7,X))).
% 100163 [para:99180.1.2,100160.2.1,demod:100129] equal(sk_c3,sk_c5) | equal(identity,sk_c5).
% 100164 [para:99182.1.2,100160.2.1,demod:100161] equal(sk_c3,sk_c5) | equal(identity,sk_c6).
% 100165 [para:100160.1.2,100078.1.2.1,demod:100128] equal(sk_c4,multiply(sk_c3,sk_c5)).
% 100197 [para:100163.2.2,100078.1.2.2,demod:99506,100160,100128] equal(sk_c4,sk_c3) | equal(sk_c3,sk_c5).
% 100203 [para:100164.2.2,99180.1.1.2,demod:100160,99506] equal(sk_c4,sk_c5) | equal(sk_c3,sk_c5).
% 100437 [para:100197.1.1,100203.1.1] equal(sk_c3,sk_c5).
% 100451 [para:99671.1.1,100437.2.1.1] equal(inverse(sk_c5),sk_c7).
% 100459 [para:100437.1.1,100158.1.1.2] equal(multiply(sk_c7,sk_c5),identity).
% 100460 [para:100437.1.1,100161.1.1.1] equal(multiply(sk_c5,sk_c7),identity).
% 100461 [para:100437.1.1,100165.1.2.1] equal(sk_c4,multiply(sk_c5,sk_c5)).
% 100465 [para:100451.1.1,99461.1.2.1.1,demod:100160] equal(multiply(sk_c5,X),multiply(sk_c3,X)).
% 100677 [para:99207.1.1,100162.1.2.2,demod:100129,99506,100465] equal(sk_c1,sk_c5) | equal(identity,sk_c5).
% 100804 [para:100677.1.1,99171.1.1.1,demod:100129,100460] equal(identity,sk_c2) | equal(identity,sk_c5).
% 101435 [para:100804.1.2,99175.1.1.2,demod:100129,99506] equal(sk_c7,sk_c6) | equal(identity,sk_c5).
% 102225 [para:101435.1.1,100069.1.1.1,demod:100126,100128] equal(identity,sk_c5).
% 102229 [para:102225.1.2,99178.1.1.1,demod:99162] equal(sk_c6,sk_c7).
% 102233 [para:102225.1.2,99314.1.2.1,demod:99162] equal(multiply(sk_c7,X),multiply(sk_c6,X)).
% 102235 [para:102225.1.2,100451.1.1.1,demod:99511] equal(identity,sk_c7).
% 102236 [para:102225.1.2,100459.1.1.2,demod:99506,102233] equal(sk_c6,identity).
% 102237 [para:102225.1.2,100460.1.1.1,demod:99162] equal(sk_c7,identity).
% 102251 [?] ?
% 102336 [para:102236.1.1,100128.1.2.1,demod:99511] equal(sk_c4,identity).
% 102350 [para:99184.1.1,102336.2.1.1,demod:102251,102233,99162] equal(sk_c6,sk_c5).
% 102351 [para:102350.1.1,99178.1.1.2,demod:100461] equal(sk_c4,sk_c7).
% 102381 [para:102229.1.2,102351.1.2] equal(sk_c4,sk_c6).
% 103172 [para:99162.1.1,99512.2.1,demod:99511,cut:102237,cut:102235] $spltprd0($spltcnst21).
% 103293 [para:102229.1.2,99251.1.1.1,demod:100160,cut:100437,factor:cut:102381] -equal(multiply(sk_c6,sk_c6),sk_c5) | $spltprd0($spltcnst19).
% 103294 [para:102225.1.2,103293.1.2,demod:102251,cut:102236] $spltprd0($spltcnst19).
% 103295 [binary:99401,103294,cut:103172] 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: 9341
% derived clauses: 1275984
% kept clauses: 58216
% kept size sum: 889645
% kept mid-nuclei: 28287
% kept new demods: 1327
% forw unit-subs: 784401
% forw double-subs: 319995
% forw overdouble-subs: 50993
% backward subs: 15813
% fast unit cutoff: 5784
% full unit cutoff: 0
% dbl unit cutoff: 7952
% real runtime : 61.3
% process. runtime: 60.50
% specific non-discr-tree subsumption statistics:
% tried: 4117914
% length fails: 604047
% strength fails: 1331523
% predlist fails: 152464
% aux str. fails: 500861
% by-lit fails: 381401
% full subs tried: 578879
% full subs fail: 559060
%
% ; 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/GRP309-1+eq_r.in")
%
%------------------------------------------------------------------------------