%------------------------------------------------------------------------------
% File : Gandalf---c-2.6
% Problem : GRP296-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 290.1s
% Output : Assurance 290.1s
% 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/GRP296-1+eq_r.in
% Using automatic strategy selection.
% Time limit in seconds: 600
%
% prove-all-passes started
%
% detected problem class: peq
%
% strategies selected:
% (hyper 30 #f 3 23)
% (binary-unit 12 #f)
% (binary-unit-uniteq 12 #f)
% (binary-posweight-kb-big-order 60 #f 3 23)
% (binary-posweight-lex-big-order 30 #f 3 23)
% (binary 30 #t)
% (binary-posweight-kb-big-order 156 #f)
% (binary-posweight-lex-big-order 102 #f)
% (binary-posweight-firstpref-order 60 #f)
% (binary-order 30 #f)
% (binary-posweight-kb-small-order 48 #f)
% (binary-posweight-lex-small-order 30 #f)
%
%
% SOS clause
% -equal(multiply(sk_c8,sk_c7),sk_c6) | -equal(multiply(X,sk_c8),sk_c7) | -equal(inverse(X),sk_c8) | -equal(multiply(sk_c8,sk_c6),sk_c7) | -equal(multiply(Y,sk_c8),sk_c6) | -equal(inverse(Y),sk_c8) | -equal(multiply(sk_c6,sk_c8),sk_c7) | -equal(multiply(sk_c8,Z),sk_c7) | -equal(multiply(U,sk_c8),Z) | -equal(inverse(U),sk_c8) | -equal(multiply(V,sk_c6),sk_c8) | -equal(inverse(V),sk_c6).
% was split for some strategies as:
% -equal(multiply(V,sk_c6),sk_c8) | -equal(inverse(V),sk_c6).
% -equal(multiply(sk_c8,Z),sk_c7) | -equal(multiply(U,sk_c8),Z) | -equal(inverse(U),sk_c8).
% -equal(multiply(Y,sk_c8),sk_c6) | -equal(inverse(Y),sk_c8).
% -equal(multiply(X,sk_c8),sk_c7) | -equal(inverse(X),sk_c8).
% -equal(multiply(sk_c8,sk_c7),sk_c6).
% -equal(multiply(sk_c8,sk_c6),sk_c7).
% -equal(multiply(sk_c6,sk_c8),sk_c7).
%
% Starting a split proof attempt with 7 components.
%
% Split component 1 started.
%
% START OF PROOFPART
% Making new sos for split:
% Original clause to be split:
% -equal(multiply(sk_c8,sk_c7),sk_c6) | -equal(multiply(X,sk_c8),sk_c7) | -equal(inverse(X),sk_c8) | -equal(multiply(sk_c8,sk_c6),sk_c7) | -equal(multiply(Y,sk_c8),sk_c6) | -equal(inverse(Y),sk_c8) | -equal(multiply(sk_c6,sk_c8),sk_c7) | -equal(multiply(sk_c8,Z),sk_c7) | -equal(multiply(U,sk_c8),Z) | -equal(inverse(U),sk_c8) | -equal(multiply(V,sk_c6),sk_c8) | -equal(inverse(V),sk_c6).
% Split part used next: -equal(multiply(V,sk_c6),sk_c8) | -equal(inverse(V),sk_c6).
% END OF PROOFPART
% ********* EMPTY CLAUSE DERIVED *********
%
%
% timer checkpoints: c(41,40,1,87,0,1,1074,50,9,1120,0,9,2458,50,26,2504,0,26,4147,50,49,4193,0,49,5969,50,69,6015,0,69,7966,50,96,8012,0,96,10097,50,134,10143,0,134,12405,50,193,12451,0,193,14891,50,295,14937,0,295,17598,50,470,17644,0,470,20527,50,725,20573,0,725,23721,50,1205,23721,40,1205,23767,0,1205,35720,3,1506,36368,4,1656,37048,5,1806,37049,1,1806,37049,50,1806,37049,40,1806,37095,0,1806,37277,3,2115,37285,4,2257,37293,5,2407,37293,1,2407,37293,50,2407,37293,40,2407,37339,0,2407,52269,3,3908,54591,50,4549,54591,40,4549,54637,0,4549,63892,3,5300,65376,50,5584,65376,40,5584,65422,0,5584,80959,3,6335,81520,4,6710,81778,1,7085,81778,50,7085,81778,40,7085,81824,0,7085,142250,3,11006,143417,4,12937,144181,5,14886,144182,1,14886,144182,50,14889,144182,40,14889,144228,0,14889,194336,3,17453,195129,4,18715,195714,1,19990,195714,50,19992,195714,40,19992,195760,0,19992,232421,3,21494,232969,4,22243,233676,5,22993,233677,1,22993,233677,50,22994,233677,40,22994,233723,0,22994,250824,3,23745,251367,4,24120,251914,5,24495,251915,1,24495,251915,50,24495,251915,40,24495,251961,0,24495,280523,3,25696,281156,4,26296,281881,5,26896,281882,1,26896,281882,50,26897,281882,40,26897,281928,0,26897,300224,3,27648,300643,4,28023,301250,1,28398,301250,50,28398,301250,40,28398,301250,40,28398,301291,0,28398,301392,50,28399,301433,0,28399)
%
%
% START OF PROOF
% 301394 [] equal(multiply(identity,X),X).
% 301395 [] equal(multiply(inverse(X),X),identity).
% 301396 [] equal(multiply(multiply(X,Y),Z),multiply(X,multiply(Y,Z))).
% 301397 [] -equal(multiply(X,sk_c6),sk_c8) | -equal(inverse(X),sk_c6).
% 301398 [] equal(inverse(sk_c2),sk_c8) | equal(inverse(sk_c5),sk_c6).
% 301399 [?] ?
% 301404 [] equal(multiply(sk_c2,sk_c8),sk_c6) | equal(inverse(sk_c5),sk_c6).
% 301405 [] equal(multiply(sk_c2,sk_c8),sk_c6) | equal(multiply(sk_c5,sk_c6),sk_c8).
% 301410 [] equal(multiply(sk_c8,sk_c6),sk_c7) | equal(inverse(sk_c5),sk_c6).
% 301411 [] equal(multiply(sk_c8,sk_c6),sk_c7) | equal(multiply(sk_c5,sk_c6),sk_c8).
% 301416 [] equal(inverse(sk_c1),sk_c8) | equal(inverse(sk_c5),sk_c6).
% 301417 [?] ?
% 301422 [] equal(multiply(sk_c1,sk_c8),sk_c7) | equal(inverse(sk_c5),sk_c6).
% 301423 [] equal(multiply(sk_c1,sk_c8),sk_c7) | equal(multiply(sk_c5,sk_c6),sk_c8).
% 301428 [] equal(multiply(sk_c8,sk_c7),sk_c6) | equal(inverse(sk_c5),sk_c6).
% 301429 [] equal(multiply(sk_c8,sk_c7),sk_c6) | equal(multiply(sk_c5,sk_c6),sk_c8).
% 301436 [hyper:301397,301398,binarycut:301399] equal(inverse(sk_c2),sk_c8).
% 301437 [para:301436.1.1,301395.1.1.1] equal(multiply(sk_c8,sk_c2),identity).
% 301444 [hyper:301397,301416,binarycut:301417] equal(inverse(sk_c1),sk_c8).
% 301445 [para:301444.1.1,301395.1.1.1] equal(multiply(sk_c8,sk_c1),identity).
% 301449 [hyper:301397,301405,301404] equal(multiply(sk_c2,sk_c8),sk_c6).
% 301455 [hyper:301397,301411,301410] equal(multiply(sk_c8,sk_c6),sk_c7).
% 301461 [hyper:301397,301423,301422] equal(multiply(sk_c1,sk_c8),sk_c7).
% 301468 [hyper:301397,301429,301428] equal(multiply(sk_c8,sk_c7),sk_c6).
% 301469 [para:301395.1.1,301396.1.1.1,demod:301394] equal(X,multiply(inverse(Y),multiply(Y,X))).
% 301470 [para:301437.1.1,301396.1.1.1,demod:301394] equal(X,multiply(sk_c8,multiply(sk_c2,X))).
% 301471 [para:301445.1.1,301396.1.1.1,demod:301394] equal(X,multiply(sk_c8,multiply(sk_c1,X))).
% 301472 [para:301449.1.1,301396.1.1.1] equal(multiply(sk_c6,X),multiply(sk_c2,multiply(sk_c8,X))).
% 301476 [para:301449.1.1,301470.1.2.2,demod:301455] equal(sk_c8,sk_c7).
% 301480 [para:301476.1.1,301455.1.1.1] equal(multiply(sk_c7,sk_c6),sk_c7).
% 301486 [para:301395.1.1,301469.1.2.2] equal(X,multiply(inverse(inverse(X)),identity)).
% 301487 [para:301437.1.1,301469.1.2.2] equal(sk_c2,multiply(inverse(sk_c8),identity)).
% 301488 [para:301445.1.1,301469.1.2.2,demod:301487] equal(sk_c1,sk_c2).
% 301490 [para:301461.1.1,301469.1.2.2,demod:301468,301444] equal(sk_c8,sk_c6).
% 301491 [para:301396.1.1,301469.1.2.2] equal(X,multiply(inverse(multiply(Y,Z)),multiply(Y,multiply(Z,X)))).
% 301492 [para:301468.1.1,301469.1.2.2] equal(sk_c7,multiply(inverse(sk_c8),sk_c6)).
% 301493 [para:301470.1.2,301469.1.2.2] equal(multiply(sk_c2,X),multiply(inverse(sk_c8),X)).
% 301495 [para:301469.1.2,301469.1.2.2] equal(multiply(X,Y),multiply(inverse(inverse(X)),Y)).
% 301496 [para:301488.1.2,301449.1.1.1,demod:301461] equal(sk_c7,sk_c6).
% 301506 [para:301471.1.2,301469.1.2.2,demod:301493] equal(multiply(sk_c1,X),multiply(sk_c2,X)).
% 301507 [para:301490.1.1,301471.1.2.1] equal(X,multiply(sk_c6,multiply(sk_c1,X))).
% 301509 [para:301480.1.1,301469.1.2.2,demod:301395] equal(sk_c6,identity).
% 301519 [para:301470.1.2,301472.1.2.2,demod:301507,301506] equal(X,multiply(sk_c1,X)).
% 301535 [para:301509.1.1,301492.1.2.2,demod:301487] equal(sk_c7,sk_c2).
% 301536 [para:301535.1.1,301496.1.1] equal(sk_c2,sk_c6).
% 301573 [para:301495.1.2,301395.1.1] equal(multiply(X,inverse(X)),identity).
% 301575 [para:301495.1.2,301486.1.2] equal(X,multiply(X,identity)).
% 301579 [para:301575.1.2,301487.1.2] equal(sk_c2,inverse(sk_c8)).
% 301580 [para:301575.1.2,301486.1.2] equal(X,inverse(inverse(X))).
% 301584 [para:301573.1.1,301491.1.2.2.2,demod:301575] equal(inverse(X),multiply(inverse(multiply(Y,X)),Y)).
% 301587 [para:301470.1.2,301584.1.2.1.1,demod:301519,301506] equal(inverse(X),multiply(inverse(X),sk_c8)).
% 301596 [para:301587.1.2,301495.1.2,demod:301580] equal(multiply(X,sk_c8),X).
% 301600 [para:301490.1.1,301596.1.1.2] equal(multiply(X,sk_c6),X).
% 301604 [hyper:301397,301600,demod:301579,cut:301536] 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 23
% 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_c8,sk_c7),sk_c6) | -equal(multiply(X,sk_c8),sk_c7) | -equal(inverse(X),sk_c8) | -equal(multiply(sk_c8,sk_c6),sk_c7) | -equal(multiply(Y,sk_c8),sk_c6) | -equal(inverse(Y),sk_c8) | -equal(multiply(sk_c6,sk_c8),sk_c7) | -equal(multiply(sk_c8,Z),sk_c7) | -equal(multiply(U,sk_c8),Z) | -equal(inverse(U),sk_c8) | -equal(multiply(V,sk_c6),sk_c8) | -equal(inverse(V),sk_c6).
% Split part used next: -equal(multiply(sk_c8,Z),sk_c7) | -equal(multiply(U,sk_c8),Z) | -equal(inverse(U),sk_c8).
% 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 23
% clause depth limited to 3
% seconds given: 4
%
%
% ********* EMPTY CLAUSE DERIVED *********
%
%
% timer checkpoints: c(41,40,1,87,0,1,1074,50,9,1120,0,9,2458,50,26,2504,0,26,4147,50,49,4193,0,49,5969,50,69,6015,0,69,7966,50,96,8012,0,96,10097,50,134,10143,0,134,12405,50,193,12451,0,193,14891,50,295,14937,0,295,17598,50,470,17644,0,470,20527,50,725,20573,0,725,23721,50,1205,23721,40,1205,23767,0,1205,35720,3,1506,36368,4,1656,37048,5,1806,37049,1,1806,37049,50,1806,37049,40,1806,37095,0,1806,37277,3,2115,37285,4,2257,37293,5,2407,37293,1,2407,37293,50,2407,37293,40,2407,37339,0,2407,52269,3,3908,54591,50,4549,54591,40,4549,54637,0,4549,63892,3,5300,65376,50,5584,65376,40,5584,65422,0,5584,80959,3,6335,81520,4,6710,81778,1,7085,81778,50,7085,81778,40,7085,81824,0,7085,142250,3,11006,143417,4,12937,144181,5,14886,144182,1,14886,144182,50,14889,144182,40,14889,144228,0,14889,194336,3,17453,195129,4,18715,195714,1,19990,195714,50,19992,195714,40,19992,195760,0,19992,232421,3,21494,232969,4,22243,233676,5,22993,233677,1,22993,233677,50,22994,233677,40,22994,233723,0,22994,250824,3,23745,251367,4,24120,251914,5,24495,251915,1,24495,251915,50,24495,251915,40,24495,251961,0,24495,280523,3,25696,281156,4,26296,281881,5,26896,281882,1,26896,281882,50,26897,281882,40,26897,281928,0,26897,300224,3,27648,300643,4,28023,301250,1,28398,301250,50,28398,301250,40,28398,301250,40,28398,301291,0,28398,301392,50,28399,301433,0,28399,301603,50,28400,301603,30,28400,301603,40,28400,301644,0,28405)
%
%
% START OF PROOF
% 301604 [] equal(X,X).
% 301608 [] -equal(multiply(sk_c8,X),sk_c7) | -equal(multiply(Y,sk_c8),X) | -equal(inverse(Y),sk_c8).
% 301611 [] equal(inverse(sk_c2),sk_c8) | equal(inverse(sk_c3),sk_c8).
% 301612 [] equal(multiply(sk_c3,sk_c8),sk_c4) | equal(inverse(sk_c2),sk_c8).
% 301613 [?] ?
% 301617 [] equal(multiply(sk_c2,sk_c8),sk_c6) | equal(inverse(sk_c3),sk_c8).
% 301618 [] equal(multiply(sk_c2,sk_c8),sk_c6) | equal(multiply(sk_c3,sk_c8),sk_c4).
% 301619 [] equal(multiply(sk_c2,sk_c8),sk_c6) | equal(multiply(sk_c8,sk_c4),sk_c7).
% 301623 [?] ?
% 301624 [?] ?
% 301625 [?] ?
% 301679 [hyper:301608,301612,301611,binarycut:301613] equal(inverse(sk_c2),sk_c8).
% 301698 [hyper:301608,301617,demod:301679,cut:301604,binarycut:301623] equal(inverse(sk_c3),sk_c8).
% 301717 [hyper:301608,301618,demod:301679,cut:301604,binarycut:301624] equal(multiply(sk_c3,sk_c8),sk_c4).
% 301729 [hyper:301608,301619,demod:301679,cut:301604,binarycut:301625] equal(multiply(sk_c8,sk_c4),sk_c7).
% 301733 [hyper:301608,301729,301717,demod:301698,cut:301604] 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 23
% 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_c8,sk_c7),sk_c6) | -equal(multiply(X,sk_c8),sk_c7) | -equal(inverse(X),sk_c8) | -equal(multiply(sk_c8,sk_c6),sk_c7) | -equal(multiply(Y,sk_c8),sk_c6) | -equal(inverse(Y),sk_c8) | -equal(multiply(sk_c6,sk_c8),sk_c7) | -equal(multiply(sk_c8,Z),sk_c7) | -equal(multiply(U,sk_c8),Z) | -equal(inverse(U),sk_c8) | -equal(multiply(V,sk_c6),sk_c8) | -equal(inverse(V),sk_c6).
% Split part used next: -equal(multiply(Y,sk_c8),sk_c6) | -equal(inverse(Y),sk_c8).
% 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 23
% clause depth limited to 3
% seconds given: 4
%
%
% ********* EMPTY CLAUSE DERIVED *********
%
%
% timer checkpoints: c(41,40,1,87,0,1,1074,50,9,1120,0,9,2458,50,26,2504,0,26,4147,50,49,4193,0,49,5969,50,69,6015,0,69,7966,50,96,8012,0,96,10097,50,134,10143,0,134,12405,50,193,12451,0,193,14891,50,295,14937,0,295,17598,50,470,17644,0,470,20527,50,725,20573,0,725,23721,50,1205,23721,40,1205,23767,0,1205,35720,3,1506,36368,4,1656,37048,5,1806,37049,1,1806,37049,50,1806,37049,40,1806,37095,0,1806,37277,3,2115,37285,4,2257,37293,5,2407,37293,1,2407,37293,50,2407,37293,40,2407,37339,0,2407,52269,3,3908,54591,50,4549,54591,40,4549,54637,0,4549,63892,3,5300,65376,50,5584,65376,40,5584,65422,0,5584,80959,3,6335,81520,4,6710,81778,1,7085,81778,50,7085,81778,40,7085,81824,0,7085,142250,3,11006,143417,4,12937,144181,5,14886,144182,1,14886,144182,50,14889,144182,40,14889,144228,0,14889,194336,3,17453,195129,4,18715,195714,1,19990,195714,50,19992,195714,40,19992,195760,0,19992,232421,3,21494,232969,4,22243,233676,5,22993,233677,1,22993,233677,50,22994,233677,40,22994,233723,0,22994,250824,3,23745,251367,4,24120,251914,5,24495,251915,1,24495,251915,50,24495,251915,40,24495,251961,0,24495,280523,3,25696,281156,4,26296,281881,5,26896,281882,1,26896,281882,50,26897,281882,40,26897,281928,0,26897,300224,3,27648,300643,4,28023,301250,1,28398,301250,50,28398,301250,40,28398,301250,40,28398,301291,0,28398,301392,50,28399,301433,0,28399,301603,50,28400,301603,30,28400,301603,40,28400,301644,0,28405,301732,50,28405,301732,30,28405,301732,40,28405,301773,0,28405)
%
%
% START OF PROOF
% 301734 [] equal(multiply(identity,X),X).
% 301735 [] equal(multiply(inverse(X),X),identity).
% 301736 [] equal(multiply(multiply(X,Y),Z),multiply(X,multiply(Y,Z))).
% 301737 [] -equal(multiply(X,sk_c8),sk_c6) | -equal(inverse(X),sk_c8).
% 301738 [] equal(inverse(sk_c2),sk_c8) | equal(inverse(sk_c5),sk_c6).
% 301739 [] equal(multiply(sk_c5,sk_c6),sk_c8) | equal(inverse(sk_c2),sk_c8).
% 301740 [] equal(inverse(sk_c2),sk_c8) | equal(inverse(sk_c3),sk_c8).
% 301741 [] equal(multiply(sk_c3,sk_c8),sk_c4) | equal(inverse(sk_c2),sk_c8).
% 301742 [] equal(multiply(sk_c8,sk_c4),sk_c7) | equal(inverse(sk_c2),sk_c8).
% 301743 [] equal(multiply(sk_c6,sk_c8),sk_c7) | equal(inverse(sk_c2),sk_c8).
% 301744 [?] ?
% 301745 [?] ?
% 301746 [?] ?
% 301747 [?] ?
% 301748 [?] ?
% 301749 [?] ?
% 301776 [hyper:301737,301738,binarycut:301744] equal(inverse(sk_c5),sk_c6).
% 301777 [para:301776.1.1,301735.1.1.1] equal(multiply(sk_c6,sk_c5),identity).
% 301781 [hyper:301737,301740,binarycut:301746] equal(inverse(sk_c3),sk_c8).
% 301785 [para:301781.1.1,301735.1.1.1] equal(multiply(sk_c8,sk_c3),identity).
% 301789 [hyper:301737,301739,binarycut:301745] equal(multiply(sk_c5,sk_c6),sk_c8).
% 301792 [hyper:301737,301741,binarycut:301747] equal(multiply(sk_c3,sk_c8),sk_c4).
% 301795 [hyper:301737,301742,binarycut:301748] equal(multiply(sk_c8,sk_c4),sk_c7).
% 301798 [hyper:301737,301743,binarycut:301749] equal(multiply(sk_c6,sk_c8),sk_c7).
% 301799 [para:301735.1.1,301736.1.1.1,demod:301734] equal(X,multiply(inverse(Y),multiply(Y,X))).
% 301800 [para:301777.1.1,301736.1.1.1,demod:301734] equal(X,multiply(sk_c6,multiply(sk_c5,X))).
% 301801 [para:301785.1.1,301736.1.1.1,demod:301734] equal(X,multiply(sk_c8,multiply(sk_c3,X))).
% 301802 [para:301789.1.1,301736.1.1.1] equal(multiply(sk_c8,X),multiply(sk_c5,multiply(sk_c6,X))).
% 301803 [para:301792.1.1,301736.1.1.1] equal(multiply(sk_c4,X),multiply(sk_c3,multiply(sk_c8,X))).
% 301804 [para:301795.1.1,301736.1.1.1] equal(multiply(sk_c7,X),multiply(sk_c8,multiply(sk_c4,X))).
% 301805 [para:301798.1.1,301736.1.1.1] equal(multiply(sk_c7,X),multiply(sk_c6,multiply(sk_c8,X))).
% 301806 [para:301789.1.1,301800.1.2.2,demod:301798] equal(sk_c6,sk_c7).
% 301807 [para:301792.1.1,301801.1.2.2,demod:301795] equal(sk_c8,sk_c7).
% 301808 [para:301807.1.1,301785.1.1.1] equal(multiply(sk_c7,sk_c3),identity).
% 301809 [para:301807.1.1,301792.1.1.2] equal(multiply(sk_c3,sk_c7),sk_c4).
% 301810 [para:301807.1.1,301795.1.1.1] equal(multiply(sk_c7,sk_c4),sk_c7).
% 301814 [para:301777.1.1,301799.1.2.2] equal(sk_c5,multiply(inverse(sk_c6),identity)).
% 301815 [para:301785.1.1,301799.1.2.2] equal(sk_c3,multiply(inverse(sk_c8),identity)).
% 301816 [para:301795.1.1,301799.1.2.2] equal(sk_c4,multiply(inverse(sk_c8),sk_c7)).
% 301820 [para:301806.1.2,301808.1.1.1] equal(multiply(sk_c6,sk_c3),identity).
% 301823 [para:301806.1.2,301809.1.1.2] equal(multiply(sk_c3,sk_c6),sk_c4).
% 301826 [para:301810.1.1,301799.1.2.2,demod:301735] equal(sk_c4,identity).
% 301834 [para:301802.1.2,301800.1.2.2,demod:301805] equal(multiply(sk_c6,X),multiply(sk_c7,X)).
% 301838 [para:301820.1.1,301799.1.2.2,demod:301814] equal(sk_c3,sk_c5).
% 301839 [?] ?
% 301840 [para:301838.1.2,301776.1.1.1,demod:301781] equal(sk_c8,sk_c6).
% 301841 [para:301838.1.2,301789.1.1.1,demod:301823] equal(sk_c4,sk_c8).
% 301842 [para:301838.1.2,301802.1.2.1] equal(multiply(sk_c8,X),multiply(sk_c3,multiply(sk_c6,X))).
% 301843 [para:301807.1.1,301840.1.1] equal(sk_c7,sk_c6).
% 301850 [para:301841.1.2,301840.1.1] equal(sk_c4,sk_c6).
% 301852 [para:301803.1.2,301801.1.2.2,demod:301834,301804] equal(multiply(sk_c8,X),multiply(sk_c6,X)).
% 301854 [para:301807.1.1,301803.1.2.2.1,demod:301852,301842,301834] equal(multiply(sk_c4,X),multiply(sk_c6,X)).
% 301857 [para:301850.1.1,301826.1.1] equal(sk_c6,identity).
% 301860 [para:301857.1.1,301789.1.1.2,demod:301839] equal(identity,sk_c8).
% 301861 [para:301857.1.1,301800.1.2.1,demod:301734] equal(X,multiply(sk_c5,X)).
% 301862 [para:301857.1.1,301802.1.2.2.1,demod:301861,301734,301852] equal(multiply(sk_c6,X),X).
% 301867 [para:301860.1.2,301798.1.1.2,demod:301862] equal(identity,sk_c7).
% 301875 [para:301867.1.2,301816.1.2.2,demod:301815] equal(sk_c4,sk_c3).
% 301876 [para:301875.1.2,301781.1.1.1] equal(inverse(sk_c4),sk_c8).
% 301877 [hyper:301737,301876,demod:301798,301854,cut:301843] 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 23
% 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_c8,sk_c7),sk_c6) | -equal(multiply(X,sk_c8),sk_c7) | -equal(inverse(X),sk_c8) | -equal(multiply(sk_c8,sk_c6),sk_c7) | -equal(multiply(Y,sk_c8),sk_c6) | -equal(inverse(Y),sk_c8) | -equal(multiply(sk_c6,sk_c8),sk_c7) | -equal(multiply(sk_c8,Z),sk_c7) | -equal(multiply(U,sk_c8),Z) | -equal(inverse(U),sk_c8) | -equal(multiply(V,sk_c6),sk_c8) | -equal(inverse(V),sk_c6).
% Split part used next: -equal(multiply(X,sk_c8),sk_c7) | -equal(inverse(X),sk_c8).
% 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 23
% clause depth limited to 3
% seconds given: 4
%
%
% ********* EMPTY CLAUSE DERIVED *********
%
%
% timer checkpoints: c(41,40,1,87,0,1,1074,50,9,1120,0,9,2458,50,26,2504,0,26,4147,50,49,4193,0,49,5969,50,69,6015,0,69,7966,50,96,8012,0,96,10097,50,134,10143,0,134,12405,50,193,12451,0,193,14891,50,295,14937,0,295,17598,50,470,17644,0,470,20527,50,725,20573,0,725,23721,50,1205,23721,40,1205,23767,0,1205,35720,3,1506,36368,4,1656,37048,5,1806,37049,1,1806,37049,50,1806,37049,40,1806,37095,0,1806,37277,3,2115,37285,4,2257,37293,5,2407,37293,1,2407,37293,50,2407,37293,40,2407,37339,0,2407,52269,3,3908,54591,50,4549,54591,40,4549,54637,0,4549,63892,3,5300,65376,50,5584,65376,40,5584,65422,0,5584,80959,3,6335,81520,4,6710,81778,1,7085,81778,50,7085,81778,40,7085,81824,0,7085,142250,3,11006,143417,4,12937,144181,5,14886,144182,1,14886,144182,50,14889,144182,40,14889,144228,0,14889,194336,3,17453,195129,4,18715,195714,1,19990,195714,50,19992,195714,40,19992,195760,0,19992,232421,3,21494,232969,4,22243,233676,5,22993,233677,1,22993,233677,50,22994,233677,40,22994,233723,0,22994,250824,3,23745,251367,4,24120,251914,5,24495,251915,1,24495,251915,50,24495,251915,40,24495,251961,0,24495,280523,3,25696,281156,4,26296,281881,5,26896,281882,1,26896,281882,50,26897,281882,40,26897,281928,0,26897,300224,3,27648,300643,4,28023,301250,1,28398,301250,50,28398,301250,40,28398,301250,40,28398,301291,0,28398,301392,50,28399,301433,0,28399,301603,50,28400,301603,30,28400,301603,40,28400,301644,0,28405,301732,50,28405,301732,30,28405,301732,40,28405,301773,0,28405,301876,50,28405,301876,30,28405,301876,40,28405,301917,0,28405)
%
%
% START OF PROOF
% 301877 [] equal(X,X).
% 301878 [] equal(multiply(identity,X),X).
% 301879 [] equal(multiply(inverse(X),X),identity).
% 301880 [] equal(multiply(multiply(X,Y),Z),multiply(X,multiply(Y,Z))).
% 301881 [] -equal(multiply(X,sk_c8),sk_c7) | -equal(inverse(X),sk_c8).
% 301900 [] equal(inverse(sk_c1),sk_c8) | equal(inverse(sk_c5),sk_c6).
% 301901 [] equal(multiply(sk_c5,sk_c6),sk_c8) | equal(inverse(sk_c1),sk_c8).
% 301902 [] equal(inverse(sk_c1),sk_c8) | equal(inverse(sk_c3),sk_c8).
% 301903 [] equal(multiply(sk_c3,sk_c8),sk_c4) | equal(inverse(sk_c1),sk_c8).
% 301904 [] equal(multiply(sk_c8,sk_c4),sk_c7) | equal(inverse(sk_c1),sk_c8).
% 301905 [] equal(multiply(sk_c6,sk_c8),sk_c7) | equal(inverse(sk_c1),sk_c8).
% 301906 [?] ?
% 301907 [?] ?
% 301908 [?] ?
% 301909 [?] ?
% 301910 [?] ?
% 301911 [?] ?
% 301926 [hyper:301881,301900,binarycut:301906] equal(inverse(sk_c5),sk_c6).
% 301927 [para:301926.1.1,301879.1.1.1] equal(multiply(sk_c6,sk_c5),identity).
% 301930 [hyper:301881,301902,binarycut:301908] equal(inverse(sk_c3),sk_c8).
% 301934 [para:301930.1.1,301879.1.1.1] equal(multiply(sk_c8,sk_c3),identity).
% 301953 [hyper:301881,301901,binarycut:301907] equal(multiply(sk_c5,sk_c6),sk_c8).
% 301956 [hyper:301881,301903,binarycut:301909] equal(multiply(sk_c3,sk_c8),sk_c4).
% 301960 [hyper:301881,301904,binarycut:301910] equal(multiply(sk_c8,sk_c4),sk_c7).
% 301964 [hyper:301881,301905,binarycut:301911] equal(multiply(sk_c6,sk_c8),sk_c7).
% 301966 [para:301879.1.1,301880.1.1.1,demod:301878] equal(X,multiply(inverse(Y),multiply(Y,X))).
% 301967 [para:301927.1.1,301880.1.1.1,demod:301878] equal(X,multiply(sk_c6,multiply(sk_c5,X))).
% 301968 [para:301934.1.1,301880.1.1.1,demod:301878] equal(X,multiply(sk_c8,multiply(sk_c3,X))).
% 301969 [para:301953.1.1,301880.1.1.1] equal(multiply(sk_c8,X),multiply(sk_c5,multiply(sk_c6,X))).
% 301970 [para:301956.1.1,301880.1.1.1] equal(multiply(sk_c4,X),multiply(sk_c3,multiply(sk_c8,X))).
% 301971 [para:301960.1.1,301880.1.1.1] equal(multiply(sk_c7,X),multiply(sk_c8,multiply(sk_c4,X))).
% 301974 [para:301964.1.1,301880.1.1.1] equal(multiply(sk_c7,X),multiply(sk_c6,multiply(sk_c8,X))).
% 301975 [para:301953.1.1,301967.1.2.2,demod:301964] equal(sk_c6,sk_c7).
% 301976 [para:301956.1.1,301968.1.2.2,demod:301960] equal(sk_c8,sk_c7).
% 301977 [para:301976.1.1,301934.1.1.1] equal(multiply(sk_c7,sk_c3),identity).
% 301978 [para:301976.1.1,301956.1.1.2] equal(multiply(sk_c3,sk_c7),sk_c4).
% 301979 [para:301976.1.1,301960.1.1.1] equal(multiply(sk_c7,sk_c4),sk_c7).
% 301983 [para:301927.1.1,301966.1.2.2] equal(sk_c5,multiply(inverse(sk_c6),identity)).
% 301984 [para:301934.1.1,301966.1.2.2] equal(sk_c3,multiply(inverse(sk_c8),identity)).
% 301985 [para:301960.1.1,301966.1.2.2] equal(sk_c4,multiply(inverse(sk_c8),sk_c7)).
% 301989 [para:301975.1.2,301977.1.1.1] equal(multiply(sk_c6,sk_c3),identity).
% 301992 [para:301975.1.2,301978.1.1.2] equal(multiply(sk_c3,sk_c6),sk_c4).
% 301995 [para:301979.1.1,301966.1.2.2,demod:301879] equal(sk_c4,identity).
% 302003 [para:301969.1.2,301967.1.2.2,demod:301974] equal(multiply(sk_c6,X),multiply(sk_c7,X)).
% 302007 [para:301989.1.1,301966.1.2.2,demod:301983] equal(sk_c3,sk_c5).
% 302008 [?] ?
% 302009 [para:302007.1.2,301926.1.1.1,demod:301930] equal(sk_c8,sk_c6).
% 302010 [para:302007.1.2,301953.1.1.1,demod:301992] equal(sk_c4,sk_c8).
% 302011 [para:302007.1.2,301969.1.2.1] equal(multiply(sk_c8,X),multiply(sk_c3,multiply(sk_c6,X))).
% 302019 [para:302010.1.2,302009.1.1] equal(sk_c4,sk_c6).
% 302021 [para:301970.1.2,301968.1.2.2,demod:302003,301971] equal(multiply(sk_c8,X),multiply(sk_c6,X)).
% 302023 [para:301976.1.1,301970.1.2.2.1,demod:302021,302011,302003] equal(multiply(sk_c4,X),multiply(sk_c6,X)).
% 302026 [para:302019.1.1,301995.1.1] equal(sk_c6,identity).
% 302029 [para:302026.1.1,301953.1.1.2,demod:302008] equal(identity,sk_c8).
% 302030 [para:302026.1.1,301967.1.2.1,demod:301878] equal(X,multiply(sk_c5,X)).
% 302031 [para:302026.1.1,301969.1.2.2.1,demod:302030,301878,302021] equal(multiply(sk_c6,X),X).
% 302036 [para:302029.1.2,301964.1.1.2,demod:302031] equal(identity,sk_c7).
% 302044 [para:302036.1.2,301985.1.2.2,demod:301984] equal(sk_c4,sk_c3).
% 302045 [para:302044.1.2,301930.1.1.1] equal(inverse(sk_c4),sk_c8).
% 302046 [hyper:301881,302045,demod:301964,302023,cut:301877] 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 23
% 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_c8,sk_c7),sk_c6) | -equal(multiply(X,sk_c8),sk_c7) | -equal(inverse(X),sk_c8) | -equal(multiply(sk_c8,sk_c6),sk_c7) | -equal(multiply(Y,sk_c8),sk_c6) | -equal(inverse(Y),sk_c8) | -equal(multiply(sk_c6,sk_c8),sk_c7) | -equal(multiply(sk_c8,Z),sk_c7) | -equal(multiply(U,sk_c8),Z) | -equal(inverse(U),sk_c8) | -equal(multiply(V,sk_c6),sk_c8) | -equal(inverse(V),sk_c6).
% Split part used next: -equal(multiply(sk_c8,sk_c7),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 23
% 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 23
% 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 23
% 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 23
% 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 23
% 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 23
% 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 23
% 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 23
% 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 23
% 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(41,40,1,87,0,1,1074,50,9,1120,0,9,2458,50,26,2504,0,26,4147,50,49,4193,0,49,5969,50,69,6015,0,69,7966,50,96,8012,0,96,10097,50,134,10143,0,134,12405,50,193,12451,0,193,14891,50,295,14937,0,295,17598,50,470,17644,0,470,20527,50,725,20573,0,725,23721,50,1205,23721,40,1205,23767,0,1205,35720,3,1506,36368,4,1656,37048,5,1806,37049,1,1806,37049,50,1806,37049,40,1806,37095,0,1806,37277,3,2115,37285,4,2257,37293,5,2407,37293,1,2407,37293,50,2407,37293,40,2407,37339,0,2407,52269,3,3908,54591,50,4549,54591,40,4549,54637,0,4549,63892,3,5300,65376,50,5584,65376,40,5584,65422,0,5584,80959,3,6335,81520,4,6710,81778,1,7085,81778,50,7085,81778,40,7085,81824,0,7085,142250,3,11006,143417,4,12937,144181,5,14886,144182,1,14886,144182,50,14889,144182,40,14889,144228,0,14889,194336,3,17453,195129,4,18715,195714,1,19990,195714,50,19992,195714,40,19992,195760,0,19992,232421,3,21494,232969,4,22243,233676,5,22993,233677,1,22993,233677,50,22994,233677,40,22994,233723,0,22994,250824,3,23745,251367,4,24120,251914,5,24495,251915,1,24495,251915,50,24495,251915,40,24495,251961,0,24495,280523,3,25696,281156,4,26296,281881,5,26896,281882,1,26896,281882,50,26897,281882,40,26897,281928,0,26897,300224,3,27648,300643,4,28023,301250,1,28398,301250,50,28398,301250,40,28398,301250,40,28398,301291,0,28398,301392,50,28399,301433,0,28399,301603,50,28400,301603,30,28400,301603,40,28400,301644,0,28405,301732,50,28405,301732,30,28405,301732,40,28405,301773,0,28405,301876,50,28405,301876,30,28405,301876,40,28405,301917,0,28405,302045,50,28405,302045,30,28405,302045,40,28405,302086,0,28409,302197,50,28409,302238,0,28409,302405,50,28412,302446,0,28417,302625,50,28421,302666,0,28421,302866,50,28429,302907,0,28429,303113,50,28440,303154,0,28445,303368,50,28464,303409,0,28464,303632,50,28498,303673,0,28503,303906,50,28570,303947,0,28570,304191,50,28707,304191,40,28707,304232,0,28707)
%
%
% START OF PROOF
% 304041 [?] ?
% 304129 [?] ?
% 304193 [] equal(multiply(identity,X),X).
% 304194 [] equal(multiply(inverse(X),X),identity).
% 304195 [] equal(multiply(multiply(X,Y),Z),multiply(X,multiply(Y,Z))).
% 304196 [] -equal(multiply(sk_c8,sk_c7),sk_c6).
% 304212 [] equal(multiply(sk_c8,sk_c6),sk_c7) | equal(multiply(sk_c3,sk_c8),sk_c4).
% 304213 [] equal(multiply(sk_c8,sk_c6),sk_c7) | equal(multiply(sk_c8,sk_c4),sk_c7).
% 304227 [?] ?
% 304228 [?] ?
% 304229 [?] ?
% 304232 [?] ?
% 304275 [input:304227,cut:304196] equal(inverse(sk_c5),sk_c6).
% 304276 [para:304275.1.1,304194.1.1.1] equal(multiply(sk_c6,sk_c5),identity).
% 304277 [input:304229,cut:304196] equal(inverse(sk_c3),sk_c8).
% 304278 [para:304277.1.1,304194.1.1.1] equal(multiply(sk_c8,sk_c3),identity).
% 304293 [input:304228,cut:304196] equal(multiply(sk_c5,sk_c6),sk_c8).
% 304296 [input:304232,cut:304196] equal(multiply(sk_c6,sk_c8),sk_c7).
% 304319 [para:304276.1.1,304195.1.1.1,demod:304193] equal(X,multiply(sk_c6,multiply(sk_c5,X))).
% 304320 [para:304278.1.1,304195.1.1.1,demod:304193] equal(X,multiply(sk_c8,multiply(sk_c3,X))).
% 304348 [para:304296.1.1,304195.1.1.1] equal(multiply(sk_c7,X),multiply(sk_c6,multiply(sk_c8,X))).
% 304357 [para:304293.1.1,304319.1.2.2] equal(sk_c6,multiply(sk_c6,sk_c8)).
% 304363 [para:304357.1.2,304296.1.1] equal(sk_c6,sk_c7).
% 304364 [para:304357.1.2,304195.1.1.1,demod:304348] equal(multiply(sk_c6,X),multiply(sk_c7,X)).
% 304365 [para:304363.1.2,304196.1.1.2] -equal(multiply(sk_c8,sk_c6),sk_c6).
% 304369 [para:304212.1.1,304365.1.1,cut:304041] equal(multiply(sk_c3,sk_c8),sk_c4).
% 304370 [para:304213.1.1,304365.1.1,cut:304041] equal(multiply(sk_c8,sk_c4),sk_c7).
% 304372 [para:304369.1.1,304320.1.2.2,demod:304370] equal(sk_c8,sk_c7).
% 304373 [para:304372.1.1,304196.1.1.1,demod:304364,cut:304129] 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_c8,sk_c7),sk_c6) | -equal(multiply(X,sk_c8),sk_c7) | -equal(inverse(X),sk_c8) | -equal(multiply(sk_c8,sk_c6),sk_c7) | -equal(multiply(Y,sk_c8),sk_c6) | -equal(inverse(Y),sk_c8) | -equal(multiply(sk_c6,sk_c8),sk_c7) | -equal(multiply(sk_c8,Z),sk_c7) | -equal(multiply(U,sk_c8),Z) | -equal(inverse(U),sk_c8) | -equal(multiply(V,sk_c6),sk_c8) | -equal(inverse(V),sk_c6).
% Split part used next: -equal(multiply(sk_c8,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 23
% 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 23
% 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 23
% 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 23
% 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 23
% 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 23
% 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 23
% 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 23
% 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 23
% 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(41,40,1,87,0,1,1074,50,9,1120,0,9,2458,50,26,2504,0,26,4147,50,49,4193,0,49,5969,50,69,6015,0,69,7966,50,96,8012,0,96,10097,50,134,10143,0,134,12405,50,193,12451,0,193,14891,50,295,14937,0,295,17598,50,470,17644,0,470,20527,50,725,20573,0,725,23721,50,1205,23721,40,1205,23767,0,1205,35720,3,1506,36368,4,1656,37048,5,1806,37049,1,1806,37049,50,1806,37049,40,1806,37095,0,1806,37277,3,2115,37285,4,2257,37293,5,2407,37293,1,2407,37293,50,2407,37293,40,2407,37339,0,2407,52269,3,3908,54591,50,4549,54591,40,4549,54637,0,4549,63892,3,5300,65376,50,5584,65376,40,5584,65422,0,5584,80959,3,6335,81520,4,6710,81778,1,7085,81778,50,7085,81778,40,7085,81824,0,7085,142250,3,11006,143417,4,12937,144181,5,14886,144182,1,14886,144182,50,14889,144182,40,14889,144228,0,14889,194336,3,17453,195129,4,18715,195714,1,19990,195714,50,19992,195714,40,19992,195760,0,19992,232421,3,21494,232969,4,22243,233676,5,22993,233677,1,22993,233677,50,22994,233677,40,22994,233723,0,22994,250824,3,23745,251367,4,24120,251914,5,24495,251915,1,24495,251915,50,24495,251915,40,24495,251961,0,24495,280523,3,25696,281156,4,26296,281881,5,26896,281882,1,26896,281882,50,26897,281882,40,26897,281928,0,26897,300224,3,27648,300643,4,28023,301250,1,28398,301250,50,28398,301250,40,28398,301250,40,28398,301291,0,28398,301392,50,28399,301433,0,28399,301603,50,28400,301603,30,28400,301603,40,28400,301644,0,28405,301732,50,28405,301732,30,28405,301732,40,28405,301773,0,28405,301876,50,28405,301876,30,28405,301876,40,28405,301917,0,28405,302045,50,28405,302045,30,28405,302045,40,28405,302086,0,28409,302197,50,28409,302238,0,28409,302405,50,28412,302446,0,28417,302625,50,28421,302666,0,28421,302866,50,28429,302907,0,28429,303113,50,28440,303154,0,28445,303368,50,28464,303409,0,28464,303632,50,28498,303673,0,28503,303906,50,28570,303947,0,28570,304191,50,28707,304191,40,28707,304232,0,28707,304372,50,28708,304372,30,28708,304372,40,28708,304413,0,28708,304524,50,28708,304565,0,28713,304732,50,28716,304773,0,28716,304952,50,28720,304993,0,28720,305193,50,28728,305234,0,28732,305440,50,28744,305481,0,28744,305695,50,28763,305736,0,28767,305959,50,28802,306000,0,28802,306233,50,28873,306274,0,28873,306518,50,29006,306518,40,29006,306559,0,29006)
%
%
% START OF PROOF
% 306357 [?] ?
% 306520 [] equal(multiply(identity,X),X).
% 306521 [] equal(multiply(inverse(X),X),identity).
% 306522 [] equal(multiply(multiply(X,Y),Z),multiply(X,multiply(Y,Z))).
% 306523 [] -equal(multiply(sk_c8,sk_c6),sk_c7).
% 306536 [?] ?
% 306537 [?] ?
% 306538 [?] ?
% 306541 [?] ?
% 306557 [] equal(multiply(sk_c8,sk_c7),sk_c6) | equal(multiply(sk_c3,sk_c8),sk_c4).
% 306558 [] equal(multiply(sk_c8,sk_c7),sk_c6) | equal(multiply(sk_c8,sk_c4),sk_c7).
% 306584 [input:306536,cut:306523] equal(inverse(sk_c5),sk_c6).
% 306585 [para:306584.1.1,306521.1.1.1] equal(multiply(sk_c6,sk_c5),identity).
% 306586 [input:306538,cut:306523] equal(inverse(sk_c3),sk_c8).
% 306587 [para:306586.1.1,306521.1.1.1] equal(multiply(sk_c8,sk_c3),identity).
% 306608 [input:306537,cut:306523] equal(multiply(sk_c5,sk_c6),sk_c8).
% 306611 [input:306541,cut:306523] equal(multiply(sk_c6,sk_c8),sk_c7).
% 306630 [para:306585.1.1,306522.1.1.1,demod:306520] equal(X,multiply(sk_c6,multiply(sk_c5,X))).
% 306633 [para:306587.1.1,306522.1.1.1,demod:306520] equal(X,multiply(sk_c8,multiply(sk_c3,X))).
% 306655 [para:306611.1.1,306522.1.1.1] equal(multiply(sk_c7,X),multiply(sk_c6,multiply(sk_c8,X))).
% 306670 [para:306608.1.1,306630.1.2.2] equal(sk_c6,multiply(sk_c6,sk_c8)).
% 306674 [para:306670.1.2,306611.1.1] equal(sk_c6,sk_c7).
% 306675 [para:306670.1.2,306522.1.1.1,demod:306655] equal(multiply(sk_c6,X),multiply(sk_c7,X)).
% 306676 [para:306674.1.2,306523.1.2] -equal(multiply(sk_c8,sk_c6),sk_c6).
% 306680 [para:306674.1.2,306557.1.1.2,cut:306676] equal(multiply(sk_c3,sk_c8),sk_c4).
% 306681 [para:306674.1.2,306558.1.1.2,cut:306676] equal(multiply(sk_c8,sk_c4),sk_c7).
% 306683 [para:306680.1.1,306633.1.2.2,demod:306681] equal(sk_c8,sk_c7).
% 306684 [para:306683.1.1,306523.1.1.1,demod:306675,cut:306357] 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 7 started.
%
% START OF PROOFPART
% Making new sos for split:
% Original clause to be split:
% -equal(multiply(sk_c8,sk_c7),sk_c6) | -equal(multiply(X,sk_c8),sk_c7) | -equal(inverse(X),sk_c8) | -equal(multiply(sk_c8,sk_c6),sk_c7) | -equal(multiply(Y,sk_c8),sk_c6) | -equal(inverse(Y),sk_c8) | -equal(multiply(sk_c6,sk_c8),sk_c7) | -equal(multiply(sk_c8,Z),sk_c7) | -equal(multiply(U,sk_c8),Z) | -equal(inverse(U),sk_c8) | -equal(multiply(V,sk_c6),sk_c8) | -equal(inverse(V),sk_c6).
% Split part used next: -equal(multiply(sk_c6,sk_c8),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 23
% 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 23
% 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 23
% 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 23
% 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 23
% 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 23
% 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 23
% 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 23
% 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 23
% 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(41,40,1,87,0,1,1074,50,9,1120,0,9,2458,50,26,2504,0,26,4147,50,49,4193,0,49,5969,50,69,6015,0,69,7966,50,96,8012,0,96,10097,50,134,10143,0,134,12405,50,193,12451,0,193,14891,50,295,14937,0,295,17598,50,470,17644,0,470,20527,50,725,20573,0,725,23721,50,1205,23721,40,1205,23767,0,1205,35720,3,1506,36368,4,1656,37048,5,1806,37049,1,1806,37049,50,1806,37049,40,1806,37095,0,1806,37277,3,2115,37285,4,2257,37293,5,2407,37293,1,2407,37293,50,2407,37293,40,2407,37339,0,2407,52269,3,3908,54591,50,4549,54591,40,4549,54637,0,4549,63892,3,5300,65376,50,5584,65376,40,5584,65422,0,5584,80959,3,6335,81520,4,6710,81778,1,7085,81778,50,7085,81778,40,7085,81824,0,7085,142250,3,11006,143417,4,12937,144181,5,14886,144182,1,14886,144182,50,14889,144182,40,14889,144228,0,14889,194336,3,17453,195129,4,18715,195714,1,19990,195714,50,19992,195714,40,19992,195760,0,19992,232421,3,21494,232969,4,22243,233676,5,22993,233677,1,22993,233677,50,22994,233677,40,22994,233723,0,22994,250824,3,23745,251367,4,24120,251914,5,24495,251915,1,24495,251915,50,24495,251915,40,24495,251961,0,24495,280523,3,25696,281156,4,26296,281881,5,26896,281882,1,26896,281882,50,26897,281882,40,26897,281928,0,26897,300224,3,27648,300643,4,28023,301250,1,28398,301250,50,28398,301250,40,28398,301250,40,28398,301291,0,28398,301392,50,28399,301433,0,28399,301603,50,28400,301603,30,28400,301603,40,28400,301644,0,28405,301732,50,28405,301732,30,28405,301732,40,28405,301773,0,28405,301876,50,28405,301876,30,28405,301876,40,28405,301917,0,28405,302045,50,28405,302045,30,28405,302045,40,28405,302086,0,28409,302197,50,28409,302238,0,28409,302405,50,28412,302446,0,28417,302625,50,28421,302666,0,28421,302866,50,28429,302907,0,28429,303113,50,28440,303154,0,28445,303368,50,28464,303409,0,28464,303632,50,28498,303673,0,28503,303906,50,28570,303947,0,28570,304191,50,28707,304191,40,28707,304232,0,28707,304372,50,28708,304372,30,28708,304372,40,28708,304413,0,28708,304524,50,28708,304565,0,28713,304732,50,28716,304773,0,28716,304952,50,28720,304993,0,28720,305193,50,28728,305234,0,28732,305440,50,28744,305481,0,28744,305695,50,28763,305736,0,28767,305959,50,28802,306000,0,28802,306233,50,28873,306274,0,28873,306518,50,29006,306518,40,29006,306559,0,29006,306683,50,29006,306683,30,29006,306683,40,29006,306724,0,29006,306833,50,29007,306874,0,29011,307031,50,29013,307072,0,29013,307237,50,29017,307278,0,29017,307451,50,29023,307492,0,29027,307671,50,29035,307712,0,29036,307899,50,29051,307940,0,29056,308135,50,29085,308176,0,29085,308381,50,29147,308422,0,29147,308637,50,29266,308637,40,29266,308678,0,29266)
%
%
% START OF PROOF
% 308513 [?] ?
% 308639 [] equal(multiply(identity,X),X).
% 308640 [] equal(multiply(inverse(X),X),identity).
% 308641 [] equal(multiply(multiply(X,Y),Z),multiply(X,multiply(Y,Z))).
% 308642 [] -equal(multiply(sk_c6,sk_c8),sk_c7).
% 308648 [?] ?
% 308654 [?] ?
% 308660 [?] ?
% 308697 [input:308648,cut:308642] equal(inverse(sk_c2),sk_c8).
% 308698 [para:308697.1.1,308640.1.1.1] equal(multiply(sk_c8,sk_c2),identity).
% 308729 [input:308654,cut:308642] equal(multiply(sk_c2,sk_c8),sk_c6).
% 308734 [input:308660,cut:308642] equal(multiply(sk_c8,sk_c6),sk_c7).
% 308747 [para:308698.1.1,308641.1.1.1,demod:308639] equal(X,multiply(sk_c8,multiply(sk_c2,X))).
% 308797 [para:308729.1.1,308747.1.2.2] equal(sk_c8,multiply(sk_c8,sk_c6)).
% 308803 [para:308797.1.2,308734.1.1] equal(sk_c8,sk_c7).
% 308805 [para:308803.1.1,308642.1.1.2,cut:308513] 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: 43645
% derived clauses: 4529883
% kept clauses: 240523
% kept size sum: 855358
% kept mid-nuclei: 14326
% kept new demods: 5744
% forw unit-subs: 1407335
% forw double-subs: 2639886
% forw overdouble-subs: 175149
% backward subs: 35108
% fast unit cutoff: 35519
% full unit cutoff: 0
% dbl unit cutoff: 13068
% real runtime : 292.84
% process. runtime: 292.66
% specific non-discr-tree subsumption statistics:
% tried: 20271356
% length fails: 1651555
% strength fails: 6346723
% predlist fails: 1198583
% aux str. fails: 4743085
% by-lit fails: 3231273
% full subs tried: 770688
% full subs fail: 692203
%
% ; 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/GRP296-1+eq_r.in")
%
%------------------------------------------------------------------------------