%------------------------------------------------------------------------------
% File : Gandalf---c-2.6
% Problem : RNG008-1 : TPTP v3.4.2. Released v1.0.0.
% Transfm : add_equality:r
% Format : otter:hypothesis:set(auto),clear(print_given)
% Command : gandalf-wrapper -time %d %s
% Computer : art09.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 60.0s
% Output : Assurance 60.0s
% 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/RNG/RNG008-1+eq_r.in
% Using automatic strategy selection.
% Time limit in seconds: 600
%
% prove-all-passes started
%
% detected problem class: heq
% detected subclass: medium
% detected subclass: long
%
% strategies selected:
% (hyper 58 #f 2 9)
% (binary-posweight-order 29 #f 2 9)
% (binary-unit 29 #f 2 9)
% (binary-double 29 #f 2 9)
% (binary 29 #t 2 9)
% (hyper 29 #t)
% (hyper 105 #f)
% (binary-unit-uniteq 17 #f)
% (binary-weightorder 23 #f)
% (binary-posweight-order 70 #f)
% (binary-posweight-lex-big-order 29 #f)
% (binary-posweight-lex-small-order 11 #f)
% (binary-order 29 #f)
% (binary-unit 46 #f)
% (binary 67 #t)
%
%
% ********* EMPTY CLAUSE DERIVED *********
%
%
% timer checkpoints: c(21,40,0,42,0,0,874944,4,4403,935438,5,5801,935441,1,5801,935441,50,5801,935441,40,5801,935462,0,5801)
%
%
% START OF PROOF
% 332237 [?] ?
% 334006 [?] ?
% 935443 [] sum(additive_identity,X,X).
% 935444 [] sum(X,additive_identity,X).
% 935445 [] product(X,Y,multiply(X,Y)).
% 935446 [] sum(X,Y,add(X,Y)).
% 935447 [] sum(additive_inverse(X),X,additive_identity).
% 935448 [] sum(X,additive_inverse(X),additive_identity).
% 935449 [] -sum(U,Y,V) | -sum(W,X,U) | -sum(X,Y,Z) | sum(W,Z,V).
% 935451 [] -sum(X,Y,Z) | sum(Y,X,Z).
% 935452 [] -product(U,Y,V) | -product(W,X,U) | -product(X,Y,Z) | product(W,Z,V).
% 935453 [] -product(U,Z,V) | -product(U,X,W) | -product(X,Y,Z) | product(W,Y,V).
% 935454 [] -product(X,U,V) | -product(X,W,X1) | -product(X,Y,Z) | -sum(W,Y,U) | sum(X1,Z,V).
% 935455 [] -product(X,Y,Z) | -product(X,U,V) | -sum(Z,V,X1) | -sum(Y,U,W) | product(X,W,X1).
% 935456 [] -product(U,Y,V) | -product(W,Y,X1) | -product(X,Y,Z) | -sum(W,X,U) | sum(X1,Z,V).
% 935457 [] -product(X,Y,Z) | -product(U,Y,V) | -sum(Z,V,X1) | -sum(X,U,W) | product(W,Y,X1).
% 935458 [] -sum(X,Y,U) | -sum(X,Y,Z) | equal(Z,U).
% 935459 [] -product(X,Y,U) | -product(X,Y,Z) | equal(Z,U).
% 935460 [] product(X,X,X).
% 935461 [] product(a,b,c).
% 935462 [] -product(b,a,c).
% 935468 [input:935452,factor:factor] -product(U,X,X) | -product(X,Y,Z) | product(U,Z,Z).
% 935469 [input:935453,factor] -product(Y,U,Y) | -product(X,Y,Z) | product(Z,U,Z).
% 935473 [input:935454,factor:factor:factor] -product(X,Y,Z) | -sum(Y,Y,Y) | sum(Z,Z,Z).
% 935474 [input:935455,factor] -product(X,Y,Z) | -sum(Y,Y,V) | -sum(Z,Z,U) | product(X,V,U).
% 935476 [input:935456,factor:factor] -product(X,Y,Z) | -product(U,Y,V) | -sum(U,X,X) | sum(V,Z,Z).
% 935484 [binary:935446,935451] sum(X,Y,add(Y,X)).
% 935486 [binary:935443,935449] -sum(X,Y,additive_identity) | -sum(Y,Z,U) | sum(X,U,Z).
% 935489 [binary:935448,935449] -sum(X,additive_inverse(Y),Z) | sum(U,Z,additive_identity) | -sum(U,X,Y).
% 935494 [binary:935444,935458] -sum(X,additive_identity,Y) | equal(Y,X).
% 935521 [binary:935460,935459] -product(X,X,Y) | equal(Y,X).
% 935523 [binary:935445,935459] equal(X,multiply(Y,Z)) | -product(Y,Z,X).
% 935525 [binary:935445,935521] equal(multiply(X,X),X).
% 935527 [binary:935460,935453] -product(Y,U,X) | -product(X,Y,Z) | product(Z,U,X).
% 935529 [binary:935445,935453] product(X,Y,multiply(Z,U)) | -product(V,Y,U) | -product(Z,V,X).
% 935550 [binary:935460,935455] -product(X,Y,Z) | -sum(X,Y,V) | -sum(X,Z,U) | product(X,V,U).
% 935552 [binary:935445,935455] -sum(multiply(X,Y),Z,U) | -product(X,V,Z) | -sum(Y,V,W) | product(X,W,U).
% 935565 [binary:935445,935527] -product(multiply(X,Y),X,Z) | product(Z,Y,multiply(X,Y)).
% 935580 [binary:935460,935457] -product(X,Y,Z) | -sum(Y,X,V) | -sum(Y,Z,U) | product(V,Y,U).
% 935582 [binary:935445,935457] -sum(multiply(X,Y),Z,U) | -product(V,Y,Z) | -sum(X,V,W) | product(W,Y,U).
% 935605 [binary:935460,935468] -product(X,Y,Z) | product(X,Z,Z).
% 935655 [binary:935460,935469] -product(X,Y,Z) | product(Z,Y,Z).
% 935742 [binary:935460,935474] -sum(X,X,Z) | -sum(X,X,Y) | product(X,Y,Z).
% 935743 [binary:935461,935474] -sum(c,c,Y) | -sum(b,b,X) | product(a,X,Y).
% 935877 [binary:935447,935486] sum(additive_inverse(X),Y,Z) | -sum(X,Z,Y).
% 935881 [binary:935446,935877.2] sum(additive_inverse(X),add(X,Y),Y).
% 935882 [binary:935484,935877.2] sum(additive_inverse(X),add(Y,X),Y).
% 935884 [binary:935451,935881] sum(add(X,Y),additive_inverse(X),Y).
% 935959 [binary:935448,935489] sum(X,additive_identity,additive_identity) | -sum(X,Y,Y).
% 936108 [binary:935461,935529.2] product(X,b,multiply(Y,c)) | -product(Y,a,X).
% 936152 [binary:935445,936108.2] product(multiply(X,a),b,multiply(X,c)).
% 936169 [binary:935565,936152] product(multiply(b,c),a,multiply(b,a)).
% 936295 [binary:935446,935742] product(X,Y,add(X,X)) | -sum(X,X,Y).
% 936297 [binary:935446,936295.2] product(X,add(X,X),add(X,X)).
% 936299 [binary:935461,935550] -sum(a,c,Y) | -sum(a,b,X) | product(a,X,Y).
% 936336 [binary:935476,936297] sum(X,add(Y,Y),add(Y,Y)) | -product(Z,add(Y,Y),X) | -sum(Z,Y,Y).
% 936400 [binary:935444,935552] product(X,Y,multiply(X,Z)) | -product(X,U,additive_identity) | -sum(Z,U,Y).
% 936753 [binary:935461,935580] -sum(b,c,Y) | -sum(b,a,X) | product(X,b,Y).
% 936860 [binary:935444,935582] product(X,Y,multiply(Z,Y)) | -product(U,Y,additive_identity) | -sum(Z,U,X).
% 937155 [binary:935446,935743] product(a,X,add(c,c)) | -sum(b,b,X).
% 937157 [binary:935446,937155.2] product(a,add(b,b),add(c,c)).
% 937170 [binary:935473,937157,cut:334006] sum(add(c,c),add(c,c),add(c,c)).
% 937237 [binary:935959.2,937170] sum(add(c,c),additive_identity,additive_identity).
% 937244 [binary:935494,937237] equal(additive_identity,add(c,c)).
% 937246 [para:937244.1.2,935881.1.2] sum(additive_inverse(c),additive_identity,c).
% 937272 [binary:935494,937246] equal(c,additive_inverse(c)).
% 938087 [binary:935446,936299] product(a,X,add(a,c)) | -sum(a,b,X).
% 938090 [binary:935446,938087.2] product(a,add(a,b),add(a,c)).
% 938117 [binary:935605,938090] product(a,add(a,c),add(a,c)).
% 938979 [binary:935446,936753] product(X,b,add(b,c)) | -sum(b,a,X).
% 938982 [binary:935446,938979.2] product(add(b,a),b,add(b,c)).
% 938995 [binary:935655,938982] product(add(b,c),b,add(b,c)).
% 942592 [binary:935460,936336.2,cut:332237] sum(add(X,X),add(X,X),add(X,X)).
% 942598 [binary:935959.2,942592] sum(add(X,X),additive_identity,additive_identity).
% 942618 [binary:935494,942598] equal(additive_identity,add(X,X)).
% 942620 [para:942618.1.2,935446.1.3] sum(X,X,additive_identity).
% 942621 [para:942618.1.2,935881.1.2] sum(additive_inverse(X),additive_identity,X).
% 942649 [binary:935552,942620] -product(X,Y,multiply(X,Z)) | product(X,U,additive_identity) | -sum(Z,Y,U).
% 942654 [binary:935582,942620] -product(X,Y,multiply(Z,Y)) | product(U,Y,additive_identity) | -sum(Z,X,U).
% 942696 [binary:935494,942621] equal(X,additive_inverse(X)).
% 942704 [para:942696.1.2,935884.1.2] sum(add(X,Y),X,Y).
% 943380 [para:935525.1.1,942649.1.3] product(X,Y,additive_identity) | -product(X,Z,X) | -sum(X,Z,Y).
% 943399 [binary:938995,943380.2] -sum(add(b,c),b,X) | product(add(b,c),X,additive_identity).
% 943451 [binary:942704,943399] product(add(b,c),c,additive_identity).
% 943482 [binary:936860.2,943451] -sum(X,add(b,c),Y) | product(Y,c,multiply(X,c)).
% 943610 [binary:935882,943482,demod:935525,937272] product(b,c,c).
% 943615 [binary:935523.2,943610] equal(c,multiply(b,c)).
% 943651 [para:943615.1.2,936169.1.1] product(c,a,multiply(b,a)).
% 943784 [binary:935523.2,943651] equal(multiply(b,a),multiply(c,a)).
% 943787 [para:943784.1.1,935445.1.3] product(b,a,multiply(c,a)).
% 944703 [para:935525.1.1,942654.1.3] product(X,Y,additive_identity) | -product(Z,Y,Y) | -sum(Y,Z,X).
% 945001 [binary:938117,944703.2] -sum(add(a,c),a,X) | product(X,add(a,c),additive_identity).
% 945151 [binary:942704,945001] product(c,add(a,c),additive_identity).
% 945182 [binary:936400.2,945151] -sum(X,add(a,c),Y) | product(c,Y,multiply(c,X)).
% 945317 [binary:935882,945182,demod:935525,937272] product(c,a,c).
% 945322 [binary:935523.2,945317] equal(c,multiply(c,a)).
% 945368 [para:945322.1.2,943787.1.3,cut:935462] contradiction
% END OF PROOF
%
% Proof found by the following strategy:
%
% using binary resolution
% using first neg lit preferred strategy
% not using sos strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% using clause demodulation
% clause length limited to 9
% clause depth limited to 2
% seconds given: 29
%
%
% ***GANDALF_FOUND_A_REFUTATION***
%
% Global statistics over all passes:
%
% given clauses: 3359
% derived clauses: 4816612
% kept clauses: 10609
% kept size sum: 175539
% kept mid-nuclei: 928324
% kept new demods: 27
% forw unit-subs: 3172169
% forw double-subs: 12391
% forw overdouble-subs: 7907
% backward subs: 461
% fast unit cutoff: 5529
% full unit cutoff: 2658
% dbl unit cutoff: 0
% real runtime : 65.3
% process. runtime: 64.65
% specific non-discr-tree subsumption statistics:
% tried: 11275398
% length fails: 1327788
% strength fails: 3528629
% predlist fails: 122348
% aux str. fails: 1695563
% by-lit fails: 479114
% full subs tried: 3677791
% full subs fail: 3667251
%
% ; 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/RNG/RNG008-1+eq_r.in")
%
%------------------------------------------------------------------------------