%------------------------------------------------------------------------------
% File : Gandalf---c-2.6
% Problem : GRP284-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 : art03.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 288.6s
% Output : Assurance 288.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/GRP284-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(multiply(X,sk_c7),sk_c6) | -equal(inverse(X),sk_c7) | -equal(multiply(Y,sk_c7),sk_c5) | -equal(inverse(Y),sk_c7) | -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_c7),sk_c5) | -equal(inverse(Y),sk_c7).
% -equal(multiply(X,sk_c7),sk_c6) | -equal(inverse(X),sk_c7).
% -equal(multiply(sk_c7,sk_c6),sk_c5).
% -equal(multiply(sk_c6,sk_c7),sk_c5).
%
% Starting a split proof attempt with 6 components.
%
% Split component 1 started.
%
% START OF PROOFPART
% Making new sos for split:
% Original clause to be split:
% -equal(multiply(sk_c7,sk_c6),sk_c5) | -equal(multiply(X,sk_c7),sk_c6) | -equal(inverse(X),sk_c7) | -equal(multiply(Y,sk_c7),sk_c5) | -equal(inverse(Y),sk_c7) | -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).
% Split part used next: -equal(inverse(U),sk_c6) | -equal(multiply(U,sk_c5),sk_c6).
% END OF PROOFPART
% ********* EMPTY CLAUSE DERIVED *********
%
%
% timer checkpoints: c(30,40,0,65,0,0,574,50,4,609,0,4,1133,50,7,1168,0,7,1697,50,11,1732,0,11,2267,50,17,2302,0,17,2844,50,23,2879,0,23,3429,50,34,3464,0,34,4022,50,57,4057,0,57,4625,50,108,4660,0,108,5238,50,218,5273,0,218,5863,50,412,5898,0,412,6500,50,778,6500,40,778,6535,0,778,17409,3,1079,18124,4,1229,18808,5,1379,18809,1,1379,18809,50,1379,18809,40,1379,18844,0,1381,19016,3,1686,19026,4,1854,19033,5,1982,19033,1,1982,19033,50,1982,19033,40,1982,19068,0,1982,41376,3,3483,42304,4,4233,42791,1,4983,42791,50,4984,42791,40,4984,42826,0,4984,60518,3,5735,61107,4,6110,61607,1,6485,61607,50,6485,61607,40,6485,61642,0,6485,73179,3,7246,73920,4,7611,75001,5,7986,75002,1,7986,75002,50,7986,75002,40,7986,75037,0,7986,114408,3,11898,116404,4,13837,117846,1,15787,117846,50,15789,117846,40,15789,117881,0,15789,153301,3,18348,154765,4,19615,155843,1,20890,155843,50,20891,155843,40,20891,155878,0,20891,184736,3,22393,185966,4,23142,187239,5,23892,187240,1,23892,187240,50,23893,187240,40,23893,187275,0,23893,196691,3,24662,197755,4,25026,198068,5,25394,198068,1,25394,198068,50,25394,198068,40,25394,198103,0,25394,224080,3,26595,225113,4,27195,225841,5,27795,225842,1,27795,225842,50,27796,225842,40,27796,225877,0,27796,243528,3,28548,244429,4,28922,245119,5,29297,245120,1,29297,245120,50,29297,245120,40,29297,245120,40,29297,245150,0,29297,245229,50,29298,245259,0,29298)
%
%
% START OF PROOF
% 245231 [] equal(multiply(identity,X),X).
% 245232 [] equal(multiply(inverse(X),X),identity).
% 245233 [] equal(multiply(multiply(X,Y),Z),multiply(X,multiply(Y,Z))).
% 245234 [] -equal(multiply(X,sk_c5),sk_c6) | -equal(inverse(X),sk_c6).
% 245235 [?] ?
% 245236 [] equal(inverse(sk_c2),sk_c7) | equal(inverse(sk_c4),sk_c6).
% 245240 [] equal(multiply(sk_c2,sk_c7),sk_c5) | equal(multiply(sk_c4,sk_c5),sk_c6).
% 245241 [] equal(multiply(sk_c2,sk_c7),sk_c5) | equal(inverse(sk_c4),sk_c6).
% 245245 [?] ?
% 245246 [] equal(inverse(sk_c1),sk_c7) | equal(inverse(sk_c4),sk_c6).
% 245250 [] equal(multiply(sk_c1,sk_c7),sk_c6) | equal(multiply(sk_c4,sk_c5),sk_c6).
% 245251 [] equal(multiply(sk_c1,sk_c7),sk_c6) | equal(inverse(sk_c4),sk_c6).
% 245255 [] equal(multiply(sk_c7,sk_c6),sk_c5) | equal(multiply(sk_c4,sk_c5),sk_c6).
% 245256 [] equal(multiply(sk_c7,sk_c6),sk_c5) | equal(inverse(sk_c4),sk_c6).
% 245262 [hyper:245234,245236,binarycut:245235] equal(inverse(sk_c2),sk_c7).
% 245263 [para:245262.1.1,245232.1.1.1] equal(multiply(sk_c7,sk_c2),identity).
% 245270 [hyper:245234,245246,binarycut:245245] equal(inverse(sk_c1),sk_c7).
% 245271 [para:245270.1.1,245232.1.1.1] equal(multiply(sk_c7,sk_c1),identity).
% 245274 [hyper:245234,245241,245240] equal(multiply(sk_c2,sk_c7),sk_c5).
% 245280 [hyper:245234,245251,245250] equal(multiply(sk_c1,sk_c7),sk_c6).
% 245286 [hyper:245234,245256,245255] equal(multiply(sk_c7,sk_c6),sk_c5).
% 245287 [para:245232.1.1,245233.1.1.1,demod:245231] equal(X,multiply(inverse(Y),multiply(Y,X))).
% 245288 [para:245263.1.1,245233.1.1.1,demod:245231] equal(X,multiply(sk_c7,multiply(sk_c2,X))).
% 245289 [para:245271.1.1,245233.1.1.1,demod:245231] equal(X,multiply(sk_c7,multiply(sk_c1,X))).
% 245290 [para:245274.1.1,245233.1.1.1] equal(multiply(sk_c5,X),multiply(sk_c2,multiply(sk_c7,X))).
% 245293 [para:245274.1.1,245288.1.2.2] equal(sk_c7,multiply(sk_c7,sk_c5)).
% 245296 [para:245232.1.1,245287.1.2.2] equal(X,multiply(inverse(inverse(X)),identity)).
% 245299 [para:245280.1.1,245287.1.2.2,demod:245286,245270] equal(sk_c7,sk_c5).
% 245300 [para:245233.1.1,245287.1.2.2] equal(X,multiply(inverse(multiply(Y,Z)),multiply(Y,multiply(Z,X)))).
% 245302 [para:245288.1.2,245287.1.2.2] equal(multiply(sk_c2,X),multiply(inverse(sk_c7),X)).
% 245303 [para:245287.1.2,245287.1.2.2] equal(multiply(X,Y),multiply(inverse(inverse(X)),Y)).
% 245305 [para:245289.1.2,245287.1.2.2,demod:245302] equal(multiply(sk_c1,X),multiply(sk_c2,X)).
% 245311 [para:245299.1.1,245288.1.2.1,demod:245305] equal(X,multiply(sk_c5,multiply(sk_c1,X))).
% 245314 [?] ?
% 245315 [para:245288.1.2,245290.1.2.2,demod:245311,245305] equal(X,multiply(sk_c1,X)).
% 245317 [para:245289.1.2,245290.1.2.2,demod:245305,245315] equal(multiply(sk_c5,X),X).
% 245319 [para:245315.1.2,245287.1.2.2,demod:245270] equal(X,multiply(sk_c7,X)).
% 245320 [para:245317.1.1,245287.1.2.2] equal(X,multiply(inverse(sk_c5),X)).
% 245327 [para:245320.1.2,245232.1.1] equal(sk_c5,identity).
% 245328 [para:245327.1.1,245293.1.2.2,demod:245319] equal(sk_c7,identity).
% 245330 [para:245328.1.1,245280.1.1.2,demod:245314] equal(identity,sk_c6).
% 245344 [para:245280.1.1,245300.1.2.1.1,demod:245315,245319] equal(X,multiply(inverse(sk_c6),X)).
% 245352 [para:245303.1.2,245232.1.1] equal(multiply(X,inverse(X)),identity).
% 245354 [para:245303.1.2,245296.1.2] equal(X,multiply(X,identity)).
% 245357 [para:245354.1.2,245296.1.2] equal(X,inverse(inverse(X))).
% 245358 [para:245354.1.2,245344.1.2] equal(identity,inverse(sk_c6)).
% 245363 [para:245352.1.1,245300.1.2.2.2,demod:245354] equal(inverse(X),multiply(inverse(multiply(Y,X)),Y)).
% 245366 [para:245288.1.2,245363.1.2.1.1,demod:245315,245305] equal(inverse(X),multiply(inverse(X),sk_c7)).
% 245374 [para:245366.1.2,245303.1.2,demod:245357] equal(multiply(X,sk_c7),X).
% 245377 [para:245299.1.1,245374.1.1.2] equal(multiply(X,sk_c5),X).
% 245382 [hyper:245234,245377,demod:245358,cut:245330] 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 19
% clause depth limited to 4
% seconds given: 4
%
%
% Split component 2 started.
%
% START OF PROOFPART
% Making new sos for split:
% Original clause to be split:
% -equal(multiply(sk_c7,sk_c6),sk_c5) | -equal(multiply(X,sk_c7),sk_c6) | -equal(inverse(X),sk_c7) | -equal(multiply(Y,sk_c7),sk_c5) | -equal(inverse(Y),sk_c7) | -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).
% Split part used next: -equal(inverse(Z),sk_c7) | -equal(multiply(Z,sk_c6),sk_c7).
% END OF PROOFPART
% 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 19
% clause depth limited to 3
% seconds given: 4
%
%
% ********* EMPTY CLAUSE DERIVED *********
%
%
% timer checkpoints: c(30,40,0,65,0,0,574,50,4,609,0,4,1133,50,7,1168,0,7,1697,50,11,1732,0,11,2267,50,17,2302,0,17,2844,50,23,2879,0,23,3429,50,34,3464,0,34,4022,50,57,4057,0,57,4625,50,108,4660,0,108,5238,50,218,5273,0,218,5863,50,412,5898,0,412,6500,50,778,6500,40,778,6535,0,778,17409,3,1079,18124,4,1229,18808,5,1379,18809,1,1379,18809,50,1379,18809,40,1379,18844,0,1381,19016,3,1686,19026,4,1854,19033,5,1982,19033,1,1982,19033,50,1982,19033,40,1982,19068,0,1982,41376,3,3483,42304,4,4233,42791,1,4983,42791,50,4984,42791,40,4984,42826,0,4984,60518,3,5735,61107,4,6110,61607,1,6485,61607,50,6485,61607,40,6485,61642,0,6485,73179,3,7246,73920,4,7611,75001,5,7986,75002,1,7986,75002,50,7986,75002,40,7986,75037,0,7986,114408,3,11898,116404,4,13837,117846,1,15787,117846,50,15789,117846,40,15789,117881,0,15789,153301,3,18348,154765,4,19615,155843,1,20890,155843,50,20891,155843,40,20891,155878,0,20891,184736,3,22393,185966,4,23142,187239,5,23892,187240,1,23892,187240,50,23893,187240,40,23893,187275,0,23893,196691,3,24662,197755,4,25026,198068,5,25394,198068,1,25394,198068,50,25394,198068,40,25394,198103,0,25394,224080,3,26595,225113,4,27195,225841,5,27795,225842,1,27795,225842,50,27796,225842,40,27796,225877,0,27796,243528,3,28548,244429,4,28922,245119,5,29297,245120,1,29297,245120,50,29297,245120,40,29297,245120,40,29297,245150,0,29297,245229,50,29298,245259,0,29298,245381,50,29299,245381,30,29299,245381,40,29299,245411,0,29301)
%
%
% START OF PROOF
% 245383 [] equal(multiply(identity,X),X).
% 245384 [] equal(multiply(inverse(X),X),identity).
% 245385 [] equal(multiply(multiply(X,Y),Z),multiply(X,multiply(Y,Z))).
% 245386 [] -equal(multiply(X,sk_c6),sk_c7) | -equal(inverse(X),sk_c7).
% 245389 [?] ?
% 245390 [] equal(inverse(sk_c2),sk_c7) | equal(inverse(sk_c3),sk_c7).
% 245394 [] equal(multiply(sk_c2,sk_c7),sk_c5) | equal(multiply(sk_c3,sk_c6),sk_c7).
% 245395 [] equal(multiply(sk_c2,sk_c7),sk_c5) | equal(inverse(sk_c3),sk_c7).
% 245399 [?] ?
% 245400 [] equal(inverse(sk_c1),sk_c7) | equal(inverse(sk_c3),sk_c7).
% 245404 [] equal(multiply(sk_c1,sk_c7),sk_c6) | equal(multiply(sk_c3,sk_c6),sk_c7).
% 245405 [] equal(multiply(sk_c1,sk_c7),sk_c6) | equal(inverse(sk_c3),sk_c7).
% 245409 [] equal(multiply(sk_c7,sk_c6),sk_c5) | equal(multiply(sk_c3,sk_c6),sk_c7).
% 245410 [] equal(multiply(sk_c7,sk_c6),sk_c5) | equal(inverse(sk_c3),sk_c7).
% 245417 [hyper:245386,245390,binarycut:245389] equal(inverse(sk_c2),sk_c7).
% 245420 [para:245417.1.1,245384.1.1.1] equal(multiply(sk_c7,sk_c2),identity).
% 245429 [hyper:245386,245400,binarycut:245399] equal(inverse(sk_c1),sk_c7).
% 245432 [para:245429.1.1,245384.1.1.1] equal(multiply(sk_c7,sk_c1),identity).
% 245440 [hyper:245386,245395,245394] equal(multiply(sk_c2,sk_c7),sk_c5).
% 245452 [hyper:245386,245404,245405] equal(multiply(sk_c1,sk_c7),sk_c6).
% 245456 [hyper:245386,245409,245410] equal(multiply(sk_c7,sk_c6),sk_c5).
% 245457 [para:245384.1.1,245385.1.1.1,demod:245383] equal(X,multiply(inverse(Y),multiply(Y,X))).
% 245458 [para:245420.1.1,245385.1.1.1,demod:245383] equal(X,multiply(sk_c7,multiply(sk_c2,X))).
% 245459 [para:245432.1.1,245385.1.1.1,demod:245383] equal(X,multiply(sk_c7,multiply(sk_c1,X))).
% 245460 [para:245440.1.1,245385.1.1.1] equal(multiply(sk_c5,X),multiply(sk_c2,multiply(sk_c7,X))).
% 245463 [para:245440.1.1,245458.1.2.2] equal(sk_c7,multiply(sk_c7,sk_c5)).
% 245466 [para:245420.1.1,245457.1.2.2] equal(sk_c2,multiply(inverse(sk_c7),identity)).
% 245467 [para:245432.1.1,245457.1.2.2,demod:245466] equal(sk_c1,sk_c2).
% 245468 [para:245452.1.1,245457.1.2.2,demod:245456,245429] equal(sk_c7,sk_c5).
% 245469 [para:245456.1.1,245457.1.2.2] equal(sk_c6,multiply(inverse(sk_c7),sk_c5)).
% 245470 [para:245458.1.2,245457.1.2.2] equal(multiply(sk_c2,X),multiply(inverse(sk_c7),X)).
% 245471 [para:245467.1.2,245440.1.1.1,demod:245452] equal(sk_c6,sk_c5).
% 245472 [para:245459.1.2,245457.1.2.2,demod:245470] equal(multiply(sk_c1,X),multiply(sk_c2,X)).
% 245477 [para:245468.1.1,245456.1.1.1] equal(multiply(sk_c5,sk_c6),sk_c5).
% 245478 [para:245468.1.1,245458.1.2.1,demod:245472] equal(X,multiply(sk_c5,multiply(sk_c1,X))).
% 245482 [para:245458.1.2,245460.1.2.2,demod:245478,245472] equal(X,multiply(sk_c1,X)).
% 245484 [para:245459.1.2,245460.1.2.2,demod:245472,245482] equal(multiply(sk_c5,X),X).
% 245486 [para:245482.1.2,245457.1.2.2,demod:245429] equal(X,multiply(sk_c7,X)).
% 245487 [para:245484.1.1,245457.1.2.2] equal(X,multiply(inverse(sk_c5),X)).
% 245495 [para:245463.1.2,245486.1.2] equal(sk_c5,sk_c7).
% 245496 [para:245487.1.2,245384.1.1] equal(sk_c5,identity).
% 245503 [para:245496.1.1,245469.1.2.2,demod:245466] equal(sk_c6,sk_c2).
% 245505 [para:245503.1.1,245471.1.1] equal(sk_c2,sk_c5).
% 245507 [para:245505.1.1,245417.1.1.1] equal(inverse(sk_c5),sk_c7).
% 245511 [hyper:245386,245507,demod:245477,cut:245495] 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 19
% clause depth limited to 3
% seconds given: 4
%
%
% Split component 3 started.
%
% START OF PROOFPART
% Making new sos for split:
% Original clause to be split:
% -equal(multiply(sk_c7,sk_c6),sk_c5) | -equal(multiply(X,sk_c7),sk_c6) | -equal(inverse(X),sk_c7) | -equal(multiply(Y,sk_c7),sk_c5) | -equal(inverse(Y),sk_c7) | -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).
% Split part used next: -equal(multiply(Y,sk_c7),sk_c5) | -equal(inverse(Y),sk_c7).
% END OF PROOFPART
% 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 19
% clause depth limited to 3
% seconds given: 4
%
%
% ********* EMPTY CLAUSE DERIVED *********
%
%
% timer checkpoints: c(30,40,0,65,0,0,574,50,4,609,0,4,1133,50,7,1168,0,7,1697,50,11,1732,0,11,2267,50,17,2302,0,17,2844,50,23,2879,0,23,3429,50,34,3464,0,34,4022,50,57,4057,0,57,4625,50,108,4660,0,108,5238,50,218,5273,0,218,5863,50,412,5898,0,412,6500,50,778,6500,40,778,6535,0,778,17409,3,1079,18124,4,1229,18808,5,1379,18809,1,1379,18809,50,1379,18809,40,1379,18844,0,1381,19016,3,1686,19026,4,1854,19033,5,1982,19033,1,1982,19033,50,1982,19033,40,1982,19068,0,1982,41376,3,3483,42304,4,4233,42791,1,4983,42791,50,4984,42791,40,4984,42826,0,4984,60518,3,5735,61107,4,6110,61607,1,6485,61607,50,6485,61607,40,6485,61642,0,6485,73179,3,7246,73920,4,7611,75001,5,7986,75002,1,7986,75002,50,7986,75002,40,7986,75037,0,7986,114408,3,11898,116404,4,13837,117846,1,15787,117846,50,15789,117846,40,15789,117881,0,15789,153301,3,18348,154765,4,19615,155843,1,20890,155843,50,20891,155843,40,20891,155878,0,20891,184736,3,22393,185966,4,23142,187239,5,23892,187240,1,23892,187240,50,23893,187240,40,23893,187275,0,23893,196691,3,24662,197755,4,25026,198068,5,25394,198068,1,25394,198068,50,25394,198068,40,25394,198103,0,25394,224080,3,26595,225113,4,27195,225841,5,27795,225842,1,27795,225842,50,27796,225842,40,27796,225877,0,27796,243528,3,28548,244429,4,28922,245119,5,29297,245120,1,29297,245120,50,29297,245120,40,29297,245120,40,29297,245150,0,29297,245229,50,29298,245259,0,29298,245381,50,29299,245381,30,29299,245381,40,29299,245411,0,29301,245510,50,29301,245510,30,29301,245510,40,29301,245540,0,29301)
%
%
% START OF PROOF
% 245512 [] equal(multiply(identity,X),X).
% 245513 [] equal(multiply(inverse(X),X),identity).
% 245514 [] equal(multiply(multiply(X,Y),Z),multiply(X,multiply(Y,Z))).
% 245515 [] -equal(multiply(X,sk_c7),sk_c5) | -equal(inverse(X),sk_c7).
% 245516 [] equal(multiply(sk_c4,sk_c5),sk_c6) | equal(inverse(sk_c2),sk_c7).
% 245517 [] equal(inverse(sk_c2),sk_c7) | equal(inverse(sk_c4),sk_c6).
% 245518 [] equal(multiply(sk_c3,sk_c6),sk_c7) | equal(inverse(sk_c2),sk_c7).
% 245519 [] equal(inverse(sk_c2),sk_c7) | equal(inverse(sk_c3),sk_c7).
% 245520 [] equal(multiply(sk_c6,sk_c7),sk_c5) | equal(inverse(sk_c2),sk_c7).
% 245521 [?] ?
% 245522 [?] ?
% 245523 [?] ?
% 245524 [?] ?
% 245525 [?] ?
% 245543 [hyper:245515,245517,binarycut:245522] equal(inverse(sk_c4),sk_c6).
% 245544 [para:245543.1.1,245513.1.1.1] equal(multiply(sk_c6,sk_c4),identity).
% 245548 [hyper:245515,245519,binarycut:245524] equal(inverse(sk_c3),sk_c7).
% 245552 [para:245548.1.1,245513.1.1.1] equal(multiply(sk_c7,sk_c3),identity).
% 245556 [hyper:245515,245516,binarycut:245521] equal(multiply(sk_c4,sk_c5),sk_c6).
% 245559 [hyper:245515,245518,binarycut:245523] equal(multiply(sk_c3,sk_c6),sk_c7).
% 245563 [hyper:245515,245520,binarycut:245525] equal(multiply(sk_c6,sk_c7),sk_c5).
% 245565 [para:245513.1.1,245514.1.1.1,demod:245512] equal(X,multiply(inverse(Y),multiply(Y,X))).
% 245566 [para:245544.1.1,245514.1.1.1,demod:245512] equal(X,multiply(sk_c6,multiply(sk_c4,X))).
% 245573 [para:245556.1.1,245566.1.2.2] equal(sk_c5,multiply(sk_c6,sk_c6)).
% 245578 [para:245559.1.1,245565.1.2.2,demod:245548] equal(sk_c6,multiply(sk_c7,sk_c7)).
% 245579 [para:245563.1.1,245565.1.2.2] equal(sk_c7,multiply(inverse(sk_c6),sk_c5)).
% 245581 [para:245573.1.2,245565.1.2.2,demod:245579] equal(sk_c6,sk_c7).
% 245586 [para:245581.1.2,245578.1.2.1,demod:245563] equal(sk_c6,sk_c5).
% 245590 [para:245586.1.1,245563.1.1.1] equal(multiply(sk_c5,sk_c7),sk_c5).
% 245607 [para:245590.1.1,245565.1.2.2,demod:245513] equal(sk_c7,identity).
% 245610 [para:245607.1.1,245552.1.1.1,demod:245512] equal(sk_c3,identity).
% 245612 [para:245607.1.1,245581.1.2] equal(sk_c6,identity).
% 245615 [para:245610.1.1,245548.1.1.1] equal(inverse(identity),sk_c7).
% 245621 [para:245612.1.1,245563.1.1.1,demod:245512] equal(sk_c7,sk_c5).
% 245626 [hyper:245515,245615,demod:245512,cut:245621] 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 19
% clause depth limited to 3
% seconds given: 4
%
%
% Split component 4 started.
%
% START OF PROOFPART
% Making new sos for split:
% Original clause to be split:
% -equal(multiply(sk_c7,sk_c6),sk_c5) | -equal(multiply(X,sk_c7),sk_c6) | -equal(inverse(X),sk_c7) | -equal(multiply(Y,sk_c7),sk_c5) | -equal(inverse(Y),sk_c7) | -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).
% Split part used next: -equal(multiply(X,sk_c7),sk_c6) | -equal(inverse(X),sk_c7).
% END OF PROOFPART
% 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 19
% clause depth limited to 3
% seconds given: 4
%
%
% ********* EMPTY CLAUSE DERIVED *********
%
%
% timer checkpoints: c(30,40,0,65,0,0,574,50,4,609,0,4,1133,50,7,1168,0,7,1697,50,11,1732,0,11,2267,50,17,2302,0,17,2844,50,23,2879,0,23,3429,50,34,3464,0,34,4022,50,57,4057,0,57,4625,50,108,4660,0,108,5238,50,218,5273,0,218,5863,50,412,5898,0,412,6500,50,778,6500,40,778,6535,0,778,17409,3,1079,18124,4,1229,18808,5,1379,18809,1,1379,18809,50,1379,18809,40,1379,18844,0,1381,19016,3,1686,19026,4,1854,19033,5,1982,19033,1,1982,19033,50,1982,19033,40,1982,19068,0,1982,41376,3,3483,42304,4,4233,42791,1,4983,42791,50,4984,42791,40,4984,42826,0,4984,60518,3,5735,61107,4,6110,61607,1,6485,61607,50,6485,61607,40,6485,61642,0,6485,73179,3,7246,73920,4,7611,75001,5,7986,75002,1,7986,75002,50,7986,75002,40,7986,75037,0,7986,114408,3,11898,116404,4,13837,117846,1,15787,117846,50,15789,117846,40,15789,117881,0,15789,153301,3,18348,154765,4,19615,155843,1,20890,155843,50,20891,155843,40,20891,155878,0,20891,184736,3,22393,185966,4,23142,187239,5,23892,187240,1,23892,187240,50,23893,187240,40,23893,187275,0,23893,196691,3,24662,197755,4,25026,198068,5,25394,198068,1,25394,198068,50,25394,198068,40,25394,198103,0,25394,224080,3,26595,225113,4,27195,225841,5,27795,225842,1,27795,225842,50,27796,225842,40,27796,225877,0,27796,243528,3,28548,244429,4,28922,245119,5,29297,245120,1,29297,245120,50,29297,245120,40,29297,245120,40,29297,245150,0,29297,245229,50,29298,245259,0,29298,245381,50,29299,245381,30,29299,245381,40,29299,245411,0,29301,245510,50,29301,245510,30,29301,245510,40,29301,245540,0,29301,245625,50,29302,245625,30,29302,245625,40,29302,245655,0,29302)
%
%
% START OF PROOF
% 245627 [] equal(multiply(identity,X),X).
% 245628 [] equal(multiply(inverse(X),X),identity).
% 245629 [] equal(multiply(multiply(X,Y),Z),multiply(X,multiply(Y,Z))).
% 245630 [] -equal(multiply(X,sk_c7),sk_c6) | -equal(inverse(X),sk_c7).
% 245641 [] equal(multiply(sk_c4,sk_c5),sk_c6) | equal(inverse(sk_c1),sk_c7).
% 245642 [] equal(inverse(sk_c1),sk_c7) | equal(inverse(sk_c4),sk_c6).
% 245643 [] equal(multiply(sk_c3,sk_c6),sk_c7) | equal(inverse(sk_c1),sk_c7).
% 245644 [] equal(inverse(sk_c1),sk_c7) | equal(inverse(sk_c3),sk_c7).
% 245645 [] equal(multiply(sk_c6,sk_c7),sk_c5) | equal(inverse(sk_c1),sk_c7).
% 245646 [?] ?
% 245647 [?] ?
% 245648 [?] ?
% 245649 [?] ?
% 245650 [?] ?
% 245664 [hyper:245630,245642,binarycut:245647] equal(inverse(sk_c4),sk_c6).
% 245665 [para:245664.1.1,245628.1.1.1] equal(multiply(sk_c6,sk_c4),identity).
% 245668 [hyper:245630,245644,binarycut:245649] equal(inverse(sk_c3),sk_c7).
% 245672 [para:245668.1.1,245628.1.1.1] equal(multiply(sk_c7,sk_c3),identity).
% 245685 [hyper:245630,245641,binarycut:245646] equal(multiply(sk_c4,sk_c5),sk_c6).
% 245688 [hyper:245630,245643,binarycut:245648] equal(multiply(sk_c3,sk_c6),sk_c7).
% 245692 [hyper:245630,245645,binarycut:245650] equal(multiply(sk_c6,sk_c7),sk_c5).
% 245693 [para:245628.1.1,245629.1.1.1,demod:245627] equal(X,multiply(inverse(Y),multiply(Y,X))).
% 245694 [para:245665.1.1,245629.1.1.1,demod:245627] equal(X,multiply(sk_c6,multiply(sk_c4,X))).
% 245699 [para:245685.1.1,245694.1.2.2] equal(sk_c5,multiply(sk_c6,sk_c6)).
% 245702 [para:245665.1.1,245693.1.2.2] equal(sk_c4,multiply(inverse(sk_c6),identity)).
% 245704 [para:245688.1.1,245693.1.2.2,demod:245668] equal(sk_c6,multiply(sk_c7,sk_c7)).
% 245705 [para:245692.1.1,245693.1.2.2] equal(sk_c7,multiply(inverse(sk_c6),sk_c5)).
% 245707 [para:245699.1.2,245693.1.2.2,demod:245705] equal(sk_c6,sk_c7).
% 245708 [para:245707.1.2,245672.1.1.1] equal(multiply(sk_c6,sk_c3),identity).
% 245712 [para:245707.1.2,245704.1.2.1,demod:245692] equal(sk_c6,sk_c5).
% 245716 [para:245712.1.1,245692.1.1.1] equal(multiply(sk_c5,sk_c7),sk_c5).
% 245720 [para:245708.1.1,245693.1.2.2,demod:245702] equal(sk_c3,sk_c4).
% 245722 [para:245720.1.2,245664.1.1.1,demod:245668] equal(sk_c7,sk_c6).
% 245731 [para:245716.1.1,245693.1.2.2,demod:245628] equal(sk_c7,identity).
% 245734 [para:245731.1.1,245672.1.1.1,demod:245627] equal(sk_c3,identity).
% 245739 [para:245734.1.1,245668.1.1.1] equal(inverse(identity),sk_c7).
% 245750 [hyper:245630,245739,demod:245627,cut:245722] 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 19
% clause depth limited to 3
% seconds given: 4
%
%
% Split component 5 started.
%
% START OF PROOFPART
% Making new sos for split:
% Original clause to be split:
% -equal(multiply(sk_c7,sk_c6),sk_c5) | -equal(multiply(X,sk_c7),sk_c6) | -equal(inverse(X),sk_c7) | -equal(multiply(Y,sk_c7),sk_c5) | -equal(inverse(Y),sk_c7) | -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).
% Split part used next: -equal(multiply(sk_c7,sk_c6),sk_c5).
% END OF PROOFPART
% 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 19
% clause depth limited to 3
% seconds given: 4
%
%
% proof attempt stopped: sos exhausted
%
% 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 19
% clause depth limited to 4
% seconds given: 4
%
%
% proof attempt stopped: sos exhausted
%
% 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 19
% clause depth limited to 5
% seconds given: 4
%
%
% proof attempt stopped: sos exhausted
%
% 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 19
% clause depth limited to 6
% seconds given: 4
%
%
% proof attempt stopped: sos exhausted
%
% 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 19
% clause depth limited to 7
% seconds given: 4
%
%
% proof attempt stopped: sos exhausted
%
% 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 19
% clause depth limited to 8
% seconds given: 4
%
%
% proof attempt stopped: sos exhausted
%
% 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 19
% clause depth limited to 9
% seconds given: 4
%
%
% proof attempt stopped: sos exhausted
%
% 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 19
% clause depth limited to 10
% seconds given: 4
%
%
% proof attempt stopped: sos exhausted
%
% 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 19
% clause depth limited to 11
% seconds given: 4
%
%
% proof attempt stopped: sos exhausted
%
% using binary resolution
% not using sos strategy
% using unit strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% using clause demodulation
% seconds given: 2
%
%
% ********* EMPTY CLAUSE DERIVED *********
%
%
% timer checkpoints: c(30,40,0,65,0,0,574,50,4,609,0,4,1133,50,7,1168,0,7,1697,50,11,1732,0,11,2267,50,17,2302,0,17,2844,50,23,2879,0,23,3429,50,34,3464,0,34,4022,50,57,4057,0,57,4625,50,108,4660,0,108,5238,50,218,5273,0,218,5863,50,412,5898,0,412,6500,50,778,6500,40,778,6535,0,778,17409,3,1079,18124,4,1229,18808,5,1379,18809,1,1379,18809,50,1379,18809,40,1379,18844,0,1381,19016,3,1686,19026,4,1854,19033,5,1982,19033,1,1982,19033,50,1982,19033,40,1982,19068,0,1982,41376,3,3483,42304,4,4233,42791,1,4983,42791,50,4984,42791,40,4984,42826,0,4984,60518,3,5735,61107,4,6110,61607,1,6485,61607,50,6485,61607,40,6485,61642,0,6485,73179,3,7246,73920,4,7611,75001,5,7986,75002,1,7986,75002,50,7986,75002,40,7986,75037,0,7986,114408,3,11898,116404,4,13837,117846,1,15787,117846,50,15789,117846,40,15789,117881,0,15789,153301,3,18348,154765,4,19615,155843,1,20890,155843,50,20891,155843,40,20891,155878,0,20891,184736,3,22393,185966,4,23142,187239,5,23892,187240,1,23892,187240,50,23893,187240,40,23893,187275,0,23893,196691,3,24662,197755,4,25026,198068,5,25394,198068,1,25394,198068,50,25394,198068,40,25394,198103,0,25394,224080,3,26595,225113,4,27195,225841,5,27795,225842,1,27795,225842,50,27796,225842,40,27796,225877,0,27796,243528,3,28548,244429,4,28922,245119,5,29297,245120,1,29297,245120,50,29297,245120,40,29297,245120,40,29297,245150,0,29297,245229,50,29298,245259,0,29298,245381,50,29299,245381,30,29299,245381,40,29299,245411,0,29301,245510,50,29301,245510,30,29301,245510,40,29301,245540,0,29301,245625,50,29302,245625,30,29302,245625,40,29302,245655,0,29302,245749,50,29302,245749,30,29302,245749,40,29302,245779,0,29304,245881,50,29304,245911,0,29305,246073,50,29306,246103,0,29308,246282,50,29311,246312,0,29311,246504,50,29316,246534,0,29316,246732,50,29323,246762,0,29325,246968,50,29338,246998,0,29338,247212,50,29365,247242,0,29365,247466,50,29422,247496,0,29422,247730,50,29533,247730,40,29533,247760,0,29533)
%
%
% START OF PROOF
% 247731 [] equal(X,X).
% 247732 [] equal(multiply(identity,X),X).
% 247733 [] equal(multiply(inverse(X),X),identity).
% 247734 [] equal(multiply(multiply(X,Y),Z),multiply(X,multiply(Y,Z))).
% 247735 [] -equal(multiply(sk_c7,sk_c6),sk_c5).
% 247756 [?] ?
% 247757 [?] ?
% 247760 [?] ?
% 247795 [input:247757,cut:247735] equal(inverse(sk_c4),sk_c6).
% 247796 [para:247795.1.1,247733.1.1.1] equal(multiply(sk_c6,sk_c4),identity).
% 247807 [input:247756,cut:247735] equal(multiply(sk_c4,sk_c5),sk_c6).
% 247809 [input:247760,cut:247735] equal(multiply(sk_c6,sk_c7),sk_c5).
% 247810 [para:247733.1.1,247734.1.1.1,demod:247732] equal(X,multiply(inverse(Y),multiply(Y,X))).
% 247825 [para:247796.1.1,247734.1.1.1,demod:247732] equal(X,multiply(sk_c6,multiply(sk_c4,X))).
% 247846 [para:247807.1.1,247825.1.2.2] equal(sk_c5,multiply(sk_c6,sk_c6)).
% 247893 [para:247809.1.1,247810.1.2.2] equal(sk_c7,multiply(inverse(sk_c6),sk_c5)).
% 247897 [para:247846.1.2,247810.1.2.2,demod:247893] equal(sk_c6,sk_c7).
% 247901 [para:247897.1.2,247735.1.1.1,demod:247846,cut:247731] contradiction
% END OF PROOF
%
% Proof found by the following strategy:
%
% using binary resolution
% not using sos strategy
% using unit strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% using clause demodulation
% seconds given: 2
%
%
% Split component 6 started.
%
% START OF PROOFPART
% Making new sos for split:
% Original clause to be split:
% -equal(multiply(sk_c7,sk_c6),sk_c5) | -equal(multiply(X,sk_c7),sk_c6) | -equal(inverse(X),sk_c7) | -equal(multiply(Y,sk_c7),sk_c5) | -equal(inverse(Y),sk_c7) | -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).
% Split part used next: -equal(multiply(sk_c6,sk_c7),sk_c5).
% END OF PROOFPART
% 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 19
% clause depth limited to 3
% seconds given: 4
%
%
% proof attempt stopped: sos exhausted
%
% 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 19
% clause depth limited to 4
% seconds given: 4
%
%
% proof attempt stopped: sos exhausted
%
% 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 19
% clause depth limited to 5
% seconds given: 4
%
%
% proof attempt stopped: sos exhausted
%
% 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 19
% clause depth limited to 6
% seconds given: 4
%
%
% proof attempt stopped: sos exhausted
%
% 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 19
% clause depth limited to 7
% seconds given: 4
%
%
% proof attempt stopped: sos exhausted
%
% 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 19
% clause depth limited to 8
% seconds given: 4
%
%
% proof attempt stopped: sos exhausted
%
% 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 19
% clause depth limited to 9
% seconds given: 4
%
%
% proof attempt stopped: sos exhausted
%
% 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 19
% clause depth limited to 10
% seconds given: 4
%
%
% proof attempt stopped: sos exhausted
%
% 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 19
% clause depth limited to 11
% seconds given: 4
%
%
% proof attempt stopped: sos exhausted
%
% using binary resolution
% not using sos strategy
% using unit strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% using clause demodulation
% seconds given: 2
%
%
% ********* EMPTY CLAUSE DERIVED *********
%
%
% timer checkpoints: c(30,40,0,65,0,0,574,50,4,609,0,4,1133,50,7,1168,0,7,1697,50,11,1732,0,11,2267,50,17,2302,0,17,2844,50,23,2879,0,23,3429,50,34,3464,0,34,4022,50,57,4057,0,57,4625,50,108,4660,0,108,5238,50,218,5273,0,218,5863,50,412,5898,0,412,6500,50,778,6500,40,778,6535,0,778,17409,3,1079,18124,4,1229,18808,5,1379,18809,1,1379,18809,50,1379,18809,40,1379,18844,0,1381,19016,3,1686,19026,4,1854,19033,5,1982,19033,1,1982,19033,50,1982,19033,40,1982,19068,0,1982,41376,3,3483,42304,4,4233,42791,1,4983,42791,50,4984,42791,40,4984,42826,0,4984,60518,3,5735,61107,4,6110,61607,1,6485,61607,50,6485,61607,40,6485,61642,0,6485,73179,3,7246,73920,4,7611,75001,5,7986,75002,1,7986,75002,50,7986,75002,40,7986,75037,0,7986,114408,3,11898,116404,4,13837,117846,1,15787,117846,50,15789,117846,40,15789,117881,0,15789,153301,3,18348,154765,4,19615,155843,1,20890,155843,50,20891,155843,40,20891,155878,0,20891,184736,3,22393,185966,4,23142,187239,5,23892,187240,1,23892,187240,50,23893,187240,40,23893,187275,0,23893,196691,3,24662,197755,4,25026,198068,5,25394,198068,1,25394,198068,50,25394,198068,40,25394,198103,0,25394,224080,3,26595,225113,4,27195,225841,5,27795,225842,1,27795,225842,50,27796,225842,40,27796,225877,0,27796,243528,3,28548,244429,4,28922,245119,5,29297,245120,1,29297,245120,50,29297,245120,40,29297,245120,40,29297,245150,0,29297,245229,50,29298,245259,0,29298,245381,50,29299,245381,30,29299,245381,40,29299,245411,0,29301,245510,50,29301,245510,30,29301,245510,40,29301,245540,0,29301,245625,50,29302,245625,30,29302,245625,40,29302,245655,0,29302,245749,50,29302,245749,30,29302,245749,40,29302,245779,0,29304,245881,50,29304,245911,0,29305,246073,50,29306,246103,0,29308,246282,50,29311,246312,0,29311,246504,50,29316,246534,0,29316,246732,50,29323,246762,0,29325,246968,50,29338,246998,0,29338,247212,50,29365,247242,0,29365,247466,50,29422,247496,0,29422,247730,50,29533,247730,40,29533,247760,0,29533,247900,50,29534,247900,30,29534,247900,40,29534,247930,0,29534,248019,50,29534,248049,0,29536,248184,50,29538,248214,0,29538,248357,50,29541,248387,0,29541,248538,50,29546,248568,0,29547,248725,50,29556,248755,0,29556,248920,50,29572,248950,0,29572,249123,50,29601,249153,0,29601,249336,50,29660,249366,0,29660,249559,50,29775,249559,40,29775,249589,0,29775)
%
%
% START OF PROOF
% 249437 [?] ?
% 249561 [] equal(multiply(identity,X),X).
% 249562 [] equal(multiply(inverse(X),X),identity).
% 249563 [] equal(multiply(multiply(X,Y),Z),multiply(X,multiply(Y,Z))).
% 249564 [] -equal(multiply(sk_c6,sk_c7),sk_c5).
% 249579 [?] ?
% 249584 [?] ?
% 249589 [?] ?
% 249618 [input:249579,cut:249564] equal(inverse(sk_c1),sk_c7).
% 249619 [para:249618.1.1,249562.1.1.1] equal(multiply(sk_c7,sk_c1),identity).
% 249635 [input:249584,cut:249564] equal(multiply(sk_c1,sk_c7),sk_c6).
% 249638 [input:249589,cut:249564] equal(multiply(sk_c7,sk_c6),sk_c5).
% 249651 [para:249619.1.1,249563.1.1.1,demod:249561] equal(X,multiply(sk_c7,multiply(sk_c1,X))).
% 249681 [para:249635.1.1,249651.1.2.2] equal(sk_c7,multiply(sk_c7,sk_c6)).
% 249686 [para:249681.1.2,249638.1.1] equal(sk_c7,sk_c5).
% 249688 [para:249686.1.1,249564.1.1.2,cut:249437] contradiction
% END OF PROOF
%
% Proof found by the following strategy:
%
% using binary resolution
% not using sos strategy
% using unit strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% using clause demodulation
% seconds given: 2
%
%
% Split attempt finished with SUCCESS.
%
% ***GANDALF_FOUND_A_REFUTATION***
%
% Global statistics over all passes:
%
% given clauses: 36059
% derived clauses: 5934730
% kept clauses: 205881
% kept size sum: 885920
% kept mid-nuclei: 3626
% kept new demods: 3990
% forw unit-subs: 2276992
% forw double-subs: 3187438
% forw overdouble-subs: 221442
% backward subs: 11880
% fast unit cutoff: 26797
% full unit cutoff: 0
% dbl unit cutoff: 5431
% real runtime : 299.49
% process. runtime: 297.75
% specific non-discr-tree subsumption statistics:
% tried: 33911615
% length fails: 3846068
% strength fails: 8443927
% predlist fails: 3530427
% aux str. fails: 4659636
% by-lit fails: 7855995
% full subs tried: 1288021
% full subs fail: 1197504
%
% ; 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/GRP284-1+eq_r.in")
%
%------------------------------------------------------------------------------