%------------------------------------------------------------------------------
% File : Gandalf---c-2.6
% Problem : GRP351-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 298.2s
% Output : Assurance 298.2s
% 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/GRP351-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_c6,sk_c5),sk_c7) | -equal(multiply(X,sk_c7),sk_c6) | -equal(inverse(X),sk_c7) | -equal(multiply(Y,sk_c6),sk_c5) | -equal(inverse(Y),sk_c6) | -equal(multiply(sk_c6,sk_c7),sk_c5) | -equal(multiply(Z,sk_c6),sk_c7) | -equal(inverse(Z),sk_c6) | -equal(inverse(U),sk_c5) | -equal(multiply(U,sk_c6),sk_c5).
% was split for some strategies as:
% -equal(inverse(U),sk_c5) | -equal(multiply(U,sk_c6),sk_c5).
% -equal(multiply(Z,sk_c6),sk_c7) | -equal(inverse(Z),sk_c6).
% -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_c6,sk_c5),sk_c7).
% -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_c6,sk_c5),sk_c7) | -equal(multiply(X,sk_c7),sk_c6) | -equal(inverse(X),sk_c7) | -equal(multiply(Y,sk_c6),sk_c5) | -equal(inverse(Y),sk_c6) | -equal(multiply(sk_c6,sk_c7),sk_c5) | -equal(multiply(Z,sk_c6),sk_c7) | -equal(inverse(Z),sk_c6) | -equal(inverse(U),sk_c5) | -equal(multiply(U,sk_c6),sk_c5).
% Split part used next: -equal(inverse(U),sk_c5) | -equal(multiply(U,sk_c6),sk_c5).
% END OF PROOFPART
% ********* EMPTY CLAUSE DERIVED *********
%
%
% timer checkpoints: c(30,40,1,65,0,1,519,50,4,554,0,4,1023,50,7,1058,0,7,1532,50,11,1567,0,11,2047,50,16,2082,0,16,2569,50,22,2604,0,22,3099,50,33,3134,0,33,3637,50,55,3672,0,55,4185,50,104,4220,0,104,4743,50,212,4778,0,212,5313,50,408,5348,0,408,5895,50,771,5895,40,771,5930,0,771,16716,3,1072,17467,4,1222,18152,1,1372,18152,50,1372,18152,40,1372,18187,0,1372,18338,3,1686,18346,4,1831,18354,5,1973,18354,1,1973,18354,50,1973,18354,40,1973,18389,0,1973,44006,3,3478,45143,4,4224,46268,5,4974,46269,1,4974,46269,50,4975,46269,40,4975,46304,0,4975,63171,3,5728,64067,4,6101,64801,5,6476,64802,1,6476,64802,50,6476,64802,40,6476,64837,0,6477,75444,3,7243,76060,4,7603,77274,5,7978,77275,1,7978,77275,50,7978,77275,40,7978,77310,0,7978,172762,3,11879,173805,4,13830,174159,5,15780,174160,1,15780,174160,50,15783,174160,40,15783,174195,0,15783,239953,3,18334,240754,4,19610,241000,1,20884,241000,50,20886,241000,40,20886,241035,0,20886,281631,3,22389,282338,4,23137,282975,5,23887,282976,1,23887,282976,50,23889,282976,40,23889,283011,0,23889,292016,3,24645,293092,4,25022,293351,5,25390,293351,1,25390,293351,50,25390,293351,40,25390,293386,0,25390,330042,3,26592,330466,4,27191,331012,1,27791,331012,50,27792,331012,40,27792,331047,0,27792,356307,3,28543,356815,4,28918,357232,5,29293,357233,1,29293,357233,50,29294,357233,40,29294,357233,40,29294,357263,0,29294)
%
%
% START OF PROOF
% 357235 [] equal(multiply(identity,X),X).
% 357236 [] equal(multiply(inverse(X),X),identity).
% 357237 [] equal(multiply(multiply(X,Y),Z),multiply(X,multiply(Y,Z))).
% 357238 [] -equal(multiply(X,sk_c6),sk_c5) | -equal(inverse(X),sk_c5).
% 357239 [?] ?
% 357240 [] equal(inverse(sk_c2),sk_c6) | equal(inverse(sk_c4),sk_c5).
% 357244 [] equal(multiply(sk_c2,sk_c6),sk_c5) | equal(multiply(sk_c4,sk_c6),sk_c5).
% 357245 [] equal(multiply(sk_c2,sk_c6),sk_c5) | equal(inverse(sk_c4),sk_c5).
% 357249 [?] ?
% 357250 [] equal(inverse(sk_c1),sk_c7) | equal(inverse(sk_c4),sk_c5).
% 357254 [] equal(multiply(sk_c1,sk_c7),sk_c6) | equal(multiply(sk_c4,sk_c6),sk_c5).
% 357255 [] equal(multiply(sk_c1,sk_c7),sk_c6) | equal(inverse(sk_c4),sk_c5).
% 357259 [] equal(multiply(sk_c6,sk_c5),sk_c7) | equal(multiply(sk_c4,sk_c6),sk_c5).
% 357260 [] equal(multiply(sk_c6,sk_c5),sk_c7) | equal(inverse(sk_c4),sk_c5).
% 357266 [hyper:357238,357240,binarycut:357239] equal(inverse(sk_c2),sk_c6).
% 357267 [para:357266.1.1,357236.1.1.1] equal(multiply(sk_c6,sk_c2),identity).
% 357276 [hyper:357238,357250,binarycut:357249] equal(inverse(sk_c1),sk_c7).
% 357277 [para:357276.1.1,357236.1.1.1] equal(multiply(sk_c7,sk_c1),identity).
% 357281 [hyper:357238,357245,357244] equal(multiply(sk_c2,sk_c6),sk_c5).
% 357290 [hyper:357238,357255,357254] equal(multiply(sk_c1,sk_c7),sk_c6).
% 357296 [hyper:357238,357260,357259] equal(multiply(sk_c6,sk_c5),sk_c7).
% 357297 [para:357236.1.1,357237.1.1.1,demod:357235] equal(X,multiply(inverse(Y),multiply(Y,X))).
% 357298 [para:357267.1.1,357237.1.1.1,demod:357235] equal(X,multiply(sk_c6,multiply(sk_c2,X))).
% 357303 [para:357281.1.1,357298.1.2.2,demod:357296] equal(sk_c6,sk_c7).
% 357304 [para:357303.1.1,357267.1.1.1] equal(multiply(sk_c7,sk_c2),identity).
% 357305 [para:357303.1.1,357281.1.1.2] equal(multiply(sk_c2,sk_c7),sk_c5).
% 357310 [para:357277.1.1,357297.1.2.2] equal(sk_c1,multiply(inverse(sk_c7),identity)).
% 357314 [para:357304.1.1,357297.1.2.2,demod:357310] equal(sk_c2,sk_c1).
% 357318 [para:357314.1.1,357281.1.1.1] equal(multiply(sk_c1,sk_c6),sk_c5).
% 357321 [para:357314.1.1,357305.1.1.1,demod:357290] equal(sk_c6,sk_c5).
% 357327 [para:357303.1.1,357321.1.1] equal(sk_c7,sk_c5).
% 357341 [hyper:357238,357318,demod:357276,cut:357327] 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 2 started.
%
% START OF PROOFPART
% Making new sos for split:
% Original clause to be split:
% -equal(multiply(sk_c6,sk_c5),sk_c7) | -equal(multiply(X,sk_c7),sk_c6) | -equal(inverse(X),sk_c7) | -equal(multiply(Y,sk_c6),sk_c5) | -equal(inverse(Y),sk_c6) | -equal(multiply(sk_c6,sk_c7),sk_c5) | -equal(multiply(Z,sk_c6),sk_c7) | -equal(inverse(Z),sk_c6) | -equal(inverse(U),sk_c5) | -equal(multiply(U,sk_c6),sk_c5).
% Split part used next: -equal(multiply(Z,sk_c6),sk_c7) | -equal(inverse(Z),sk_c6).
% 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,1,65,0,1,519,50,4,554,0,4,1023,50,7,1058,0,7,1532,50,11,1567,0,11,2047,50,16,2082,0,16,2569,50,22,2604,0,22,3099,50,33,3134,0,33,3637,50,55,3672,0,55,4185,50,104,4220,0,104,4743,50,212,4778,0,212,5313,50,408,5348,0,408,5895,50,771,5895,40,771,5930,0,771,16716,3,1072,17467,4,1222,18152,1,1372,18152,50,1372,18152,40,1372,18187,0,1372,18338,3,1686,18346,4,1831,18354,5,1973,18354,1,1973,18354,50,1973,18354,40,1973,18389,0,1973,44006,3,3478,45143,4,4224,46268,5,4974,46269,1,4974,46269,50,4975,46269,40,4975,46304,0,4975,63171,3,5728,64067,4,6101,64801,5,6476,64802,1,6476,64802,50,6476,64802,40,6476,64837,0,6477,75444,3,7243,76060,4,7603,77274,5,7978,77275,1,7978,77275,50,7978,77275,40,7978,77310,0,7978,172762,3,11879,173805,4,13830,174159,5,15780,174160,1,15780,174160,50,15783,174160,40,15783,174195,0,15783,239953,3,18334,240754,4,19610,241000,1,20884,241000,50,20886,241000,40,20886,241035,0,20886,281631,3,22389,282338,4,23137,282975,5,23887,282976,1,23887,282976,50,23889,282976,40,23889,283011,0,23889,292016,3,24645,293092,4,25022,293351,5,25390,293351,1,25390,293351,50,25390,293351,40,25390,293386,0,25390,330042,3,26592,330466,4,27191,331012,1,27791,331012,50,27792,331012,40,27792,331047,0,27792,356307,3,28543,356815,4,28918,357232,5,29293,357233,1,29293,357233,50,29294,357233,40,29294,357233,40,29294,357263,0,29294,357340,50,29294,357340,30,29294,357340,40,29294,357370,0,29294)
%
%
% START OF PROOF
% 357341 [] equal(X,X).
% 357342 [] equal(multiply(identity,X),X).
% 357343 [] equal(multiply(inverse(X),X),identity).
% 357344 [] equal(multiply(multiply(X,Y),Z),multiply(X,multiply(Y,Z))).
% 357345 [] -equal(multiply(X,sk_c6),sk_c7) | -equal(inverse(X),sk_c6).
% 357348 [] equal(inverse(sk_c2),sk_c6) | equal(inverse(sk_c3),sk_c6).
% 357349 [?] ?
% 357353 [] equal(multiply(sk_c2,sk_c6),sk_c5) | equal(inverse(sk_c3),sk_c6).
% 357354 [] equal(multiply(sk_c2,sk_c6),sk_c5) | equal(multiply(sk_c3,sk_c6),sk_c7).
% 357358 [] equal(inverse(sk_c1),sk_c7) | equal(inverse(sk_c3),sk_c6).
% 357359 [?] ?
% 357363 [] equal(multiply(sk_c1,sk_c7),sk_c6) | equal(inverse(sk_c3),sk_c6).
% 357364 [] equal(multiply(sk_c1,sk_c7),sk_c6) | equal(multiply(sk_c3,sk_c6),sk_c7).
% 357368 [] equal(multiply(sk_c6,sk_c5),sk_c7) | equal(inverse(sk_c3),sk_c6).
% 357369 [] equal(multiply(sk_c6,sk_c5),sk_c7) | equal(multiply(sk_c3,sk_c6),sk_c7).
% 357376 [hyper:357345,357348,binarycut:357349] equal(inverse(sk_c2),sk_c6).
% 357379 [para:357376.1.1,357343.1.1.1] equal(multiply(sk_c6,sk_c2),identity).
% 357385 [hyper:357345,357358,binarycut:357359] equal(inverse(sk_c1),sk_c7).
% 357386 [para:357385.1.1,357343.1.1.1] equal(multiply(sk_c7,sk_c1),identity).
% 357401 [hyper:357345,357354,357353] equal(multiply(sk_c2,sk_c6),sk_c5).
% 357405 [hyper:357345,357364,357363] equal(multiply(sk_c1,sk_c7),sk_c6).
% 357409 [hyper:357345,357369,357368] equal(multiply(sk_c6,sk_c5),sk_c7).
% 357410 [para:357343.1.1,357344.1.1.1,demod:357342] equal(X,multiply(inverse(Y),multiply(Y,X))).
% 357411 [para:357379.1.1,357344.1.1.1,demod:357342] equal(X,multiply(sk_c6,multiply(sk_c2,X))).
% 357413 [para:357401.1.1,357344.1.1.1] equal(multiply(sk_c5,X),multiply(sk_c2,multiply(sk_c6,X))).
% 357415 [para:357409.1.1,357344.1.1.1] equal(multiply(sk_c7,X),multiply(sk_c6,multiply(sk_c5,X))).
% 357416 [para:357401.1.1,357411.1.2.2,demod:357409] equal(sk_c6,sk_c7).
% 357417 [para:357416.1.1,357379.1.1.1] equal(multiply(sk_c7,sk_c2),identity).
% 357418 [para:357416.1.1,357401.1.1.2] equal(multiply(sk_c2,sk_c7),sk_c5).
% 357422 [para:357379.1.1,357410.1.2.2] equal(sk_c2,multiply(inverse(sk_c6),identity)).
% 357423 [para:357386.1.1,357410.1.2.2] equal(sk_c1,multiply(inverse(sk_c7),identity)).
% 357424 [para:357405.1.1,357410.1.2.2,demod:357385] equal(sk_c7,multiply(sk_c7,sk_c6)).
% 357425 [para:357409.1.1,357410.1.2.2] equal(sk_c5,multiply(inverse(sk_c6),sk_c7)).
% 357427 [para:357417.1.1,357410.1.2.2,demod:357423] equal(sk_c2,sk_c1).
% 357434 [para:357427.1.1,357418.1.1.1,demod:357405] equal(sk_c6,sk_c5).
% 357435 [para:357434.1.1,357379.1.1.1] equal(multiply(sk_c5,sk_c2),identity).
% 357438 [para:357434.1.1,357411.1.2.1] equal(X,multiply(sk_c5,multiply(sk_c2,X))).
% 357439 [para:357434.1.1,357416.1.1] equal(sk_c5,sk_c7).
% 357443 [para:357413.1.2,357411.1.2.2,demod:357415] equal(multiply(sk_c6,X),multiply(sk_c7,X)).
% 357444 [para:357411.1.2,357413.1.2.2,demod:357438] equal(X,multiply(sk_c2,X)).
% 357446 [para:357444.1.2,357411.1.2.2,demod:357443] equal(X,multiply(sk_c7,X)).
% 357454 [para:357435.1.1,357410.1.2.2] equal(sk_c2,multiply(inverse(sk_c5),identity)).
% 357456 [para:357454.1.2,357344.1.1.1,demod:357342,357444] equal(X,multiply(inverse(sk_c5),X)).
% 357457 [para:357456.1.2,357343.1.1] equal(sk_c5,identity).
% 357459 [para:357457.1.1,357409.1.1.2,demod:357446,357443] equal(identity,sk_c7).
% 357464 [para:357459.1.2,357425.1.2.2,demod:357422] equal(sk_c5,sk_c2).
% 357465 [para:357464.1.1,357439.1.1] equal(sk_c2,sk_c7).
% 357468 [para:357465.1.1,357376.1.1.1] equal(inverse(sk_c7),sk_c6).
% 357471 [hyper:357345,357468,demod:357424,cut:357341] 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_c6,sk_c5),sk_c7) | -equal(multiply(X,sk_c7),sk_c6) | -equal(inverse(X),sk_c7) | -equal(multiply(Y,sk_c6),sk_c5) | -equal(inverse(Y),sk_c6) | -equal(multiply(sk_c6,sk_c7),sk_c5) | -equal(multiply(Z,sk_c6),sk_c7) | -equal(inverse(Z),sk_c6) | -equal(inverse(U),sk_c5) | -equal(multiply(U,sk_c6),sk_c5).
% Split part used next: -equal(multiply(Y,sk_c6),sk_c5) | -equal(inverse(Y),sk_c6).
% 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,1,65,0,1,519,50,4,554,0,4,1023,50,7,1058,0,7,1532,50,11,1567,0,11,2047,50,16,2082,0,16,2569,50,22,2604,0,22,3099,50,33,3134,0,33,3637,50,55,3672,0,55,4185,50,104,4220,0,104,4743,50,212,4778,0,212,5313,50,408,5348,0,408,5895,50,771,5895,40,771,5930,0,771,16716,3,1072,17467,4,1222,18152,1,1372,18152,50,1372,18152,40,1372,18187,0,1372,18338,3,1686,18346,4,1831,18354,5,1973,18354,1,1973,18354,50,1973,18354,40,1973,18389,0,1973,44006,3,3478,45143,4,4224,46268,5,4974,46269,1,4974,46269,50,4975,46269,40,4975,46304,0,4975,63171,3,5728,64067,4,6101,64801,5,6476,64802,1,6476,64802,50,6476,64802,40,6476,64837,0,6477,75444,3,7243,76060,4,7603,77274,5,7978,77275,1,7978,77275,50,7978,77275,40,7978,77310,0,7978,172762,3,11879,173805,4,13830,174159,5,15780,174160,1,15780,174160,50,15783,174160,40,15783,174195,0,15783,239953,3,18334,240754,4,19610,241000,1,20884,241000,50,20886,241000,40,20886,241035,0,20886,281631,3,22389,282338,4,23137,282975,5,23887,282976,1,23887,282976,50,23889,282976,40,23889,283011,0,23889,292016,3,24645,293092,4,25022,293351,5,25390,293351,1,25390,293351,50,25390,293351,40,25390,293386,0,25390,330042,3,26592,330466,4,27191,331012,1,27791,331012,50,27792,331012,40,27792,331047,0,27792,356307,3,28543,356815,4,28918,357232,5,29293,357233,1,29293,357233,50,29294,357233,40,29294,357233,40,29294,357263,0,29294,357340,50,29294,357340,30,29294,357340,40,29294,357370,0,29294,357470,50,29294,357470,30,29294,357470,40,29294,357500,0,29299)
%
%
% START OF PROOF
% 357472 [] equal(multiply(identity,X),X).
% 357473 [] equal(multiply(inverse(X),X),identity).
% 357474 [] equal(multiply(multiply(X,Y),Z),multiply(X,multiply(Y,Z))).
% 357475 [] -equal(multiply(X,sk_c6),sk_c5) | -equal(inverse(X),sk_c6).
% 357476 [] equal(multiply(sk_c4,sk_c6),sk_c5) | equal(inverse(sk_c2),sk_c6).
% 357477 [] equal(inverse(sk_c2),sk_c6) | equal(inverse(sk_c4),sk_c5).
% 357478 [] equal(inverse(sk_c2),sk_c6) | equal(inverse(sk_c3),sk_c6).
% 357479 [] equal(multiply(sk_c3,sk_c6),sk_c7) | equal(inverse(sk_c2),sk_c6).
% 357480 [] equal(multiply(sk_c6,sk_c7),sk_c5) | equal(inverse(sk_c2),sk_c6).
% 357481 [?] ?
% 357482 [?] ?
% 357483 [?] ?
% 357484 [?] ?
% 357485 [?] ?
% 357503 [hyper:357475,357477,binarycut:357482] equal(inverse(sk_c4),sk_c5).
% 357504 [para:357503.1.1,357473.1.1.1] equal(multiply(sk_c5,sk_c4),identity).
% 357508 [hyper:357475,357478,binarycut:357483] equal(inverse(sk_c3),sk_c6).
% 357512 [para:357508.1.1,357473.1.1.1] equal(multiply(sk_c6,sk_c3),identity).
% 357517 [hyper:357475,357476,binarycut:357481] equal(multiply(sk_c4,sk_c6),sk_c5).
% 357521 [hyper:357475,357479,binarycut:357484] equal(multiply(sk_c3,sk_c6),sk_c7).
% 357526 [hyper:357475,357480,binarycut:357485] equal(multiply(sk_c6,sk_c7),sk_c5).
% 357527 [para:357473.1.1,357474.1.1.1,demod:357472] equal(X,multiply(inverse(Y),multiply(Y,X))).
% 357528 [para:357504.1.1,357474.1.1.1,demod:357472] equal(X,multiply(sk_c5,multiply(sk_c4,X))).
% 357529 [para:357512.1.1,357474.1.1.1,demod:357472] equal(X,multiply(sk_c6,multiply(sk_c3,X))).
% 357530 [para:357517.1.1,357474.1.1.1] equal(multiply(sk_c5,X),multiply(sk_c4,multiply(sk_c6,X))).
% 357531 [para:357521.1.1,357474.1.1.1] equal(multiply(sk_c7,X),multiply(sk_c3,multiply(sk_c6,X))).
% 357536 [para:357504.1.1,357527.1.2.2] equal(sk_c4,multiply(inverse(sk_c5),identity)).
% 357538 [para:357521.1.1,357527.1.2.2,demod:357526,357508] equal(sk_c6,sk_c5).
% 357541 [para:357538.1.1,357512.1.1.1] equal(multiply(sk_c5,sk_c3),identity).
% 357546 [para:357538.1.1,357529.1.2.1] equal(X,multiply(sk_c5,multiply(sk_c3,X))).
% 357547 [para:357541.1.1,357527.1.2.2,demod:357536] equal(sk_c3,sk_c4).
% 357557 [para:357529.1.2,357530.1.2.2,demod:357546] equal(X,multiply(sk_c4,X)).
% 357558 [para:357547.1.2,357530.1.2.1,demod:357531] equal(multiply(sk_c5,X),multiply(sk_c7,X)).
% 357559 [para:357557.1.2,357528.1.2.2,demod:357558] equal(X,multiply(sk_c7,X)).
% 357561 [para:357557.1.2,357530.1.2,demod:357559,357558] equal(X,multiply(sk_c6,X)).
% 357565 [para:357561.1.2,357512.1.1] equal(sk_c3,identity).
% 357566 [para:357565.1.1,357508.1.1.1] equal(inverse(identity),sk_c6).
% 357567 [hyper:357475,357566,demod:357472,cut:357538] 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_c6,sk_c5),sk_c7) | -equal(multiply(X,sk_c7),sk_c6) | -equal(inverse(X),sk_c7) | -equal(multiply(Y,sk_c6),sk_c5) | -equal(inverse(Y),sk_c6) | -equal(multiply(sk_c6,sk_c7),sk_c5) | -equal(multiply(Z,sk_c6),sk_c7) | -equal(inverse(Z),sk_c6) | -equal(inverse(U),sk_c5) | -equal(multiply(U,sk_c6),sk_c5).
% 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
%
%
% 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
%
%
% ********* EMPTY CLAUSE DERIVED *********
%
%
% timer checkpoints: c(30,40,1,65,0,1,519,50,4,554,0,4,1023,50,7,1058,0,7,1532,50,11,1567,0,11,2047,50,16,2082,0,16,2569,50,22,2604,0,22,3099,50,33,3134,0,33,3637,50,55,3672,0,55,4185,50,104,4220,0,104,4743,50,212,4778,0,212,5313,50,408,5348,0,408,5895,50,771,5895,40,771,5930,0,771,16716,3,1072,17467,4,1222,18152,1,1372,18152,50,1372,18152,40,1372,18187,0,1372,18338,3,1686,18346,4,1831,18354,5,1973,18354,1,1973,18354,50,1973,18354,40,1973,18389,0,1973,44006,3,3478,45143,4,4224,46268,5,4974,46269,1,4974,46269,50,4975,46269,40,4975,46304,0,4975,63171,3,5728,64067,4,6101,64801,5,6476,64802,1,6476,64802,50,6476,64802,40,6476,64837,0,6477,75444,3,7243,76060,4,7603,77274,5,7978,77275,1,7978,77275,50,7978,77275,40,7978,77310,0,7978,172762,3,11879,173805,4,13830,174159,5,15780,174160,1,15780,174160,50,15783,174160,40,15783,174195,0,15783,239953,3,18334,240754,4,19610,241000,1,20884,241000,50,20886,241000,40,20886,241035,0,20886,281631,3,22389,282338,4,23137,282975,5,23887,282976,1,23887,282976,50,23889,282976,40,23889,283011,0,23889,292016,3,24645,293092,4,25022,293351,5,25390,293351,1,25390,293351,50,25390,293351,40,25390,293386,0,25390,330042,3,26592,330466,4,27191,331012,1,27791,331012,50,27792,331012,40,27792,331047,0,27792,356307,3,28543,356815,4,28918,357232,5,29293,357233,1,29293,357233,50,29294,357233,40,29294,357233,40,29294,357263,0,29294,357340,50,29294,357340,30,29294,357340,40,29294,357370,0,29294,357470,50,29294,357470,30,29294,357470,40,29294,357500,0,29299,357566,50,29299,357566,30,29299,357566,40,29299,357596,0,29299,357671,50,29299,357701,0,29299,357825,50,29302,357855,0,29306,357989,50,29310,358019,0,29310)
%
%
% START OF PROOF
% 357991 [] equal(multiply(identity,X),X).
% 357992 [] equal(multiply(inverse(X),X),identity).
% 357993 [] equal(multiply(multiply(X,Y),Z),multiply(X,multiply(Y,Z))).
% 357994 [] -equal(multiply(X,sk_c7),sk_c6) | -equal(inverse(X),sk_c7).
% 358005 [] equal(multiply(sk_c4,sk_c6),sk_c5) | equal(inverse(sk_c1),sk_c7).
% 358006 [] equal(inverse(sk_c1),sk_c7) | equal(inverse(sk_c4),sk_c5).
% 358007 [] equal(inverse(sk_c1),sk_c7) | equal(inverse(sk_c3),sk_c6).
% 358008 [] equal(multiply(sk_c3,sk_c6),sk_c7) | equal(inverse(sk_c1),sk_c7).
% 358009 [] equal(multiply(sk_c6,sk_c7),sk_c5) | equal(inverse(sk_c1),sk_c7).
% 358010 [?] ?
% 358011 [?] ?
% 358012 [?] ?
% 358013 [?] ?
% 358014 [?] ?
% 358025 [hyper:357994,358006,binarycut:358011] equal(inverse(sk_c4),sk_c5).
% 358026 [para:358025.1.1,357992.1.1.1] equal(multiply(sk_c5,sk_c4),identity).
% 358029 [hyper:357994,358007,binarycut:358012] equal(inverse(sk_c3),sk_c6).
% 358030 [para:358029.1.1,357992.1.1.1] equal(multiply(sk_c6,sk_c3),identity).
% 358036 [hyper:357994,358005,binarycut:358010] equal(multiply(sk_c4,sk_c6),sk_c5).
% 358039 [hyper:357994,358008,binarycut:358013] equal(multiply(sk_c3,sk_c6),sk_c7).
% 358043 [hyper:357994,358009,binarycut:358014] equal(multiply(sk_c6,sk_c7),sk_c5).
% 358044 [para:357992.1.1,357993.1.1.1,demod:357991] equal(X,multiply(inverse(Y),multiply(Y,X))).
% 358045 [para:358026.1.1,357993.1.1.1,demod:357991] equal(X,multiply(sk_c5,multiply(sk_c4,X))).
% 358046 [para:358030.1.1,357993.1.1.1,demod:357991] equal(X,multiply(sk_c6,multiply(sk_c3,X))).
% 358047 [para:358036.1.1,357993.1.1.1] equal(multiply(sk_c5,X),multiply(sk_c4,multiply(sk_c6,X))).
% 358048 [para:358039.1.1,357993.1.1.1] equal(multiply(sk_c7,X),multiply(sk_c3,multiply(sk_c6,X))).
% 358050 [para:358036.1.1,358045.1.2.2] equal(sk_c6,multiply(sk_c5,sk_c5)).
% 358053 [para:357992.1.1,358044.1.2.2] equal(X,multiply(inverse(inverse(X)),identity)).
% 358054 [para:358026.1.1,358044.1.2.2] equal(sk_c4,multiply(inverse(sk_c5),identity)).
% 358055 [para:358030.1.1,358044.1.2.2] equal(sk_c3,multiply(inverse(sk_c6),identity)).
% 358056 [para:358039.1.1,358044.1.2.2,demod:358043,358029] equal(sk_c6,sk_c5).
% 358057 [para:357993.1.1,358044.1.2.2] equal(X,multiply(inverse(multiply(Y,Z)),multiply(Y,multiply(Z,X)))).
% 358058 [para:358043.1.1,358044.1.2.2] equal(sk_c7,multiply(inverse(sk_c6),sk_c5)).
% 358060 [para:358044.1.2,358044.1.2.2] equal(multiply(X,Y),multiply(inverse(inverse(X)),Y)).
% 358061 [para:358056.1.1,358030.1.1.1] equal(multiply(sk_c5,sk_c3),identity).
% 358062 [para:358056.1.1,358036.1.1.2] equal(multiply(sk_c4,sk_c5),sk_c5).
% 358066 [para:358056.1.1,358046.1.2.1] equal(X,multiply(sk_c5,multiply(sk_c3,X))).
% 358067 [para:358061.1.1,358044.1.2.2,demod:358054] equal(sk_c3,sk_c4).
% 358068 [para:358067.1.2,358036.1.1.1,demod:358039] equal(sk_c7,sk_c5).
% 358075 [para:358068.1.2,358062.1.1.2] equal(multiply(sk_c4,sk_c7),sk_c5).
% 358077 [para:358046.1.2,358047.1.2.2,demod:358066] equal(X,multiply(sk_c4,X)).
% 358078 [para:358067.1.2,358047.1.2.1,demod:358048] equal(multiply(sk_c5,X),multiply(sk_c7,X)).
% 358079 [para:358077.1.2,358045.1.2.2,demod:358078] equal(X,multiply(sk_c7,X)).
% 358080 [para:358067.1.2,358077.1.2.1] equal(X,multiply(sk_c3,X)).
% 358081 [para:358077.1.2,358047.1.2,demod:358079,358078] equal(X,multiply(sk_c6,X)).
% 358082 [para:358079.1.2,358044.1.2.2] equal(X,multiply(inverse(sk_c7),X)).
% 358088 [para:358075.1.1,358045.1.2.2,demod:358050] equal(sk_c7,sk_c6).
% 358089 [para:358082.1.2,357992.1.1] equal(sk_c7,identity).
% 358090 [para:358089.1.1,358043.1.1.2,demod:358081] equal(identity,sk_c5).
% 358096 [para:357992.1.1,358057.1.2.2] equal(X,multiply(inverse(multiply(inverse(multiply(Y,X)),Y)),identity)).
% 358097 [para:357992.1.1,358057.1.2.2.2] equal(X,multiply(inverse(multiply(Y,inverse(X))),multiply(Y,identity))).
% 358111 [para:358090.1.2,358058.1.2.2,demod:358055] equal(sk_c7,sk_c3).
% 358112 [para:358111.1.2,358029.1.1.1] equal(inverse(sk_c7),sk_c6).
% 358116 [para:358060.1.2,358053.1.2] equal(X,multiply(X,identity)).
% 358118 [para:358116.1.2,358053.1.2] equal(X,inverse(inverse(X))).
% 358119 [para:358116.1.2,358054.1.2] equal(sk_c4,inverse(sk_c5)).
% 358121 [para:358068.1.2,358119.1.2.1,demod:358112] equal(sk_c4,sk_c6).
% 358123 [para:358121.1.2,358039.1.1.2,demod:358080] equal(sk_c4,sk_c7).
% 358138 [para:358096.1.2,358116.1.2] equal(inverse(multiply(inverse(multiply(X,Y)),X)),Y).
% 358150 [para:358054.1.2,358097.1.2.2,demod:358118,358077,358119] equal(X,multiply(X,sk_c4)).
% 358153 [para:358123.1.1,358150.1.2.2] equal(X,multiply(X,sk_c7)).
% 358161 [hyper:357994,358138,demod:357991,357992,358153,cut:358088] 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 6
% seconds given: 4
%
%
% Split component 5 started.
%
% START OF PROOFPART
% Making new sos for split:
% Original clause to be split:
% -equal(multiply(sk_c6,sk_c5),sk_c7) | -equal(multiply(X,sk_c7),sk_c6) | -equal(inverse(X),sk_c7) | -equal(multiply(Y,sk_c6),sk_c5) | -equal(inverse(Y),sk_c6) | -equal(multiply(sk_c6,sk_c7),sk_c5) | -equal(multiply(Z,sk_c6),sk_c7) | -equal(inverse(Z),sk_c6) | -equal(inverse(U),sk_c5) | -equal(multiply(U,sk_c6),sk_c5).
% Split part used next: -equal(multiply(sk_c6,sk_c5),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
%
%
% 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,1,65,0,1,519,50,4,554,0,4,1023,50,7,1058,0,7,1532,50,11,1567,0,11,2047,50,16,2082,0,16,2569,50,22,2604,0,22,3099,50,33,3134,0,33,3637,50,55,3672,0,55,4185,50,104,4220,0,104,4743,50,212,4778,0,212,5313,50,408,5348,0,408,5895,50,771,5895,40,771,5930,0,771,16716,3,1072,17467,4,1222,18152,1,1372,18152,50,1372,18152,40,1372,18187,0,1372,18338,3,1686,18346,4,1831,18354,5,1973,18354,1,1973,18354,50,1973,18354,40,1973,18389,0,1973,44006,3,3478,45143,4,4224,46268,5,4974,46269,1,4974,46269,50,4975,46269,40,4975,46304,0,4975,63171,3,5728,64067,4,6101,64801,5,6476,64802,1,6476,64802,50,6476,64802,40,6476,64837,0,6477,75444,3,7243,76060,4,7603,77274,5,7978,77275,1,7978,77275,50,7978,77275,40,7978,77310,0,7978,172762,3,11879,173805,4,13830,174159,5,15780,174160,1,15780,174160,50,15783,174160,40,15783,174195,0,15783,239953,3,18334,240754,4,19610,241000,1,20884,241000,50,20886,241000,40,20886,241035,0,20886,281631,3,22389,282338,4,23137,282975,5,23887,282976,1,23887,282976,50,23889,282976,40,23889,283011,0,23889,292016,3,24645,293092,4,25022,293351,5,25390,293351,1,25390,293351,50,25390,293351,40,25390,293386,0,25390,330042,3,26592,330466,4,27191,331012,1,27791,331012,50,27792,331012,40,27792,331047,0,27792,356307,3,28543,356815,4,28918,357232,5,29293,357233,1,29293,357233,50,29294,357233,40,29294,357233,40,29294,357263,0,29294,357340,50,29294,357340,30,29294,357340,40,29294,357370,0,29294,357470,50,29294,357470,30,29294,357470,40,29294,357500,0,29299,357566,50,29299,357566,30,29299,357566,40,29299,357596,0,29299,357671,50,29299,357701,0,29299,357825,50,29302,357855,0,29306,357989,50,29310,358019,0,29310,358160,50,29311,358160,30,29311,358160,40,29311,358190,0,29316,358277,50,29316,358307,0,29316,358444,50,29318,358474,0,29318,358619,50,29321,358649,0,29325,358802,50,29331,358832,0,29331,358991,50,29339,359021,0,29343,359188,50,29358,359218,0,29358,359393,50,29386,359423,0,29386,359608,50,29446,359638,0,29446,359833,50,29560,359833,40,29560,359863,0,29561)
%
%
% START OF PROOF
% 359717 [?] ?
% 359835 [] equal(multiply(identity,X),X).
% 359836 [] equal(multiply(inverse(X),X),identity).
% 359837 [] equal(multiply(multiply(X,Y),Z),multiply(X,multiply(Y,Z))).
% 359838 [] -equal(multiply(sk_c6,sk_c5),sk_c7).
% 359859 [?] ?
% 359860 [?] ?
% 359861 [?] ?
% 359862 [?] ?
% 359863 [?] ?
% 359898 [input:359860,cut:359838] equal(inverse(sk_c4),sk_c5).
% 359899 [para:359898.1.1,359836.1.1.1] equal(multiply(sk_c5,sk_c4),identity).
% 359900 [input:359861,cut:359838] equal(inverse(sk_c3),sk_c6).
% 359901 [para:359900.1.1,359836.1.1.1] equal(multiply(sk_c6,sk_c3),identity).
% 359910 [input:359859,cut:359838] equal(multiply(sk_c4,sk_c6),sk_c5).
% 359911 [input:359862,cut:359838] equal(multiply(sk_c3,sk_c6),sk_c7).
% 359912 [input:359863,cut:359838] equal(multiply(sk_c6,sk_c7),sk_c5).
% 359928 [para:359899.1.1,359837.1.1.1,demod:359835] equal(X,multiply(sk_c5,multiply(sk_c4,X))).
% 359931 [para:359901.1.1,359837.1.1.1,demod:359835] equal(X,multiply(sk_c6,multiply(sk_c3,X))).
% 359949 [para:359910.1.1,359928.1.2.2] equal(sk_c6,multiply(sk_c5,sk_c5)).
% 359957 [para:359911.1.1,359931.1.2.2] equal(sk_c6,multiply(sk_c6,sk_c7)).
% 359962 [para:359957.1.2,359912.1.1] equal(sk_c6,sk_c5).
% 359964 [para:359962.1.1,359838.1.1.1,demod:359949,cut:359717] 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_c6,sk_c5),sk_c7) | -equal(multiply(X,sk_c7),sk_c6) | -equal(inverse(X),sk_c7) | -equal(multiply(Y,sk_c6),sk_c5) | -equal(inverse(Y),sk_c6) | -equal(multiply(sk_c6,sk_c7),sk_c5) | -equal(multiply(Z,sk_c6),sk_c7) | -equal(inverse(Z),sk_c6) | -equal(inverse(U),sk_c5) | -equal(multiply(U,sk_c6),sk_c5).
% 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,1,65,0,1,519,50,4,554,0,4,1023,50,7,1058,0,7,1532,50,11,1567,0,11,2047,50,16,2082,0,16,2569,50,22,2604,0,22,3099,50,33,3134,0,33,3637,50,55,3672,0,55,4185,50,104,4220,0,104,4743,50,212,4778,0,212,5313,50,408,5348,0,408,5895,50,771,5895,40,771,5930,0,771,16716,3,1072,17467,4,1222,18152,1,1372,18152,50,1372,18152,40,1372,18187,0,1372,18338,3,1686,18346,4,1831,18354,5,1973,18354,1,1973,18354,50,1973,18354,40,1973,18389,0,1973,44006,3,3478,45143,4,4224,46268,5,4974,46269,1,4974,46269,50,4975,46269,40,4975,46304,0,4975,63171,3,5728,64067,4,6101,64801,5,6476,64802,1,6476,64802,50,6476,64802,40,6476,64837,0,6477,75444,3,7243,76060,4,7603,77274,5,7978,77275,1,7978,77275,50,7978,77275,40,7978,77310,0,7978,172762,3,11879,173805,4,13830,174159,5,15780,174160,1,15780,174160,50,15783,174160,40,15783,174195,0,15783,239953,3,18334,240754,4,19610,241000,1,20884,241000,50,20886,241000,40,20886,241035,0,20886,281631,3,22389,282338,4,23137,282975,5,23887,282976,1,23887,282976,50,23889,282976,40,23889,283011,0,23889,292016,3,24645,293092,4,25022,293351,5,25390,293351,1,25390,293351,50,25390,293351,40,25390,293386,0,25390,330042,3,26592,330466,4,27191,331012,1,27791,331012,50,27792,331012,40,27792,331047,0,27792,356307,3,28543,356815,4,28918,357232,5,29293,357233,1,29293,357233,50,29294,357233,40,29294,357233,40,29294,357263,0,29294,357340,50,29294,357340,30,29294,357340,40,29294,357370,0,29294,357470,50,29294,357470,30,29294,357470,40,29294,357500,0,29299,357566,50,29299,357566,30,29299,357566,40,29299,357596,0,29299,357671,50,29299,357701,0,29299,357825,50,29302,357855,0,29306,357989,50,29310,358019,0,29310,358160,50,29311,358160,30,29311,358160,40,29311,358190,0,29316,358277,50,29316,358307,0,29316,358444,50,29318,358474,0,29318,358619,50,29321,358649,0,29325,358802,50,29331,358832,0,29331,358991,50,29339,359021,0,29343,359188,50,29358,359218,0,29358,359393,50,29386,359423,0,29386,359608,50,29446,359638,0,29446,359833,50,29560,359833,40,29560,359863,0,29561,359963,50,29561,359963,30,29561,359963,40,29561,359993,0,29561,360089,50,29561,360119,0,29566,360263,50,29569,360293,0,29569,360445,50,29572,360475,0,29572,360635,50,29577,360665,0,29581,360831,50,29590,360861,0,29590,361035,50,29605,361065,0,29610,361247,50,29638,361277,0,29638,361469,50,29700,361499,0,29700,361701,50,29815,361701,40,29815,361731,0,29815)
%
%
% START OF PROOF
% 361570 [?] ?
% 361703 [] equal(multiply(identity,X),X).
% 361704 [] equal(multiply(inverse(X),X),identity).
% 361705 [] equal(multiply(multiply(X,Y),Z),multiply(X,multiply(Y,Z))).
% 361706 [] -equal(multiply(sk_c6,sk_c7),sk_c5).
% 361711 [?] ?
% 361716 [?] ?
% 361721 [?] ?
% 361726 [?] ?
% 361731 [?] ?
% 361748 [input:361711,cut:361706] equal(inverse(sk_c2),sk_c6).
% 361749 [para:361748.1.1,361704.1.1.1] equal(multiply(sk_c6,sk_c2),identity).
% 361760 [input:361721,cut:361706] equal(inverse(sk_c1),sk_c7).
% 361761 [para:361760.1.1,361704.1.1.1] equal(multiply(sk_c7,sk_c1),identity).
% 361768 [input:361716,cut:361706] equal(multiply(sk_c2,sk_c6),sk_c5).
% 361777 [input:361726,cut:361706] equal(multiply(sk_c1,sk_c7),sk_c6).
% 361780 [input:361731,cut:361706] equal(multiply(sk_c6,sk_c5),sk_c7).
% 361786 [para:361749.1.1,361705.1.1.1,demod:361703] equal(X,multiply(sk_c6,multiply(sk_c2,X))).
% 361793 [para:361761.1.1,361705.1.1.1,demod:361703] equal(X,multiply(sk_c7,multiply(sk_c1,X))).
% 361817 [para:361768.1.1,361786.1.2.2] equal(sk_c6,multiply(sk_c6,sk_c5)).
% 361822 [para:361817.1.2,361780.1.1] equal(sk_c6,sk_c7).
% 361824 [para:361822.1.1,361706.1.1.1] -equal(multiply(sk_c7,sk_c7),sk_c5).
% 361854 [para:361777.1.1,361793.1.2.2] equal(sk_c7,multiply(sk_c7,sk_c6)).
% 361856 [para:361822.1.1,361854.1.2.2] equal(sk_c7,multiply(sk_c7,sk_c7)).
% 361857 [para:361856.1.2,361824.1.1,cut:361570] 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: 32173
% derived clauses: 5809002
% kept clauses: 307032
% kept size sum: 25612
% kept mid-nuclei: 3054
% kept new demods: 4162
% forw unit-subs: 1911040
% forw double-subs: 3186342
% forw overdouble-subs: 349150
% backward subs: 11342
% fast unit cutoff: 21321
% full unit cutoff: 0
% dbl unit cutoff: 5468
% real runtime : 300.30
% process. runtime: 298.14
% specific non-discr-tree subsumption statistics:
% tried: 36034104
% length fails: 3896266
% strength fails: 8463124
% predlist fails: 2462396
% aux str. fails: 4539213
% by-lit fails: 8727443
% full subs tried: 1356668
% full subs fail: 1245522
%
% ; 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/GRP351-1+eq_r.in")
%
%------------------------------------------------------------------------------