%------------------------------------------------------------------------------
% File : Gandalf---c-2.6
% Problem : BOO012-3 : TPTP v3.4.2. Bugfixed v1.2.1.
% 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 248.6s
% Output : Assurance 248.6s
% Verified :
% SZS Type : None (Parsing solution fails)
% Syntax : Number of formulae : 0
% Comments :
%------------------------------------------------------------------------------
%----NO SOLUTION OUTPUT BY SYSTEM
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
%
% Gandalf c-2.6 r1 starting to prove: /home/graph/tptp/TSTP/PreparedTPTP/otter:hypothesis:set(auto),clear(print_given)---add_equality:r/BOO/BOO012-3+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 3 9)
% (binary-posweight-order 29 #f 3 9)
% (binary-unit 29 #f 3 9)
% (binary-double 29 #f 3 9)
% (binary 29 #t 3 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(36,40,0,72,0,0,690880,4,4386,821982,5,5801,821985,1,5801,821985,50,5801,821985,40,5801,822021,0,5801,848928,3,7252,856128,4,7979,883013,5,8702,883014,5,8702,883014,1,8702,883014,50,8704,883014,40,8704,883050,0,8704,929854,3,10155,945500,4,10880,1005436,5,11605,1005438,5,11606,1005438,1,11606,1005438,50,11608,1005438,40,11608,1005474,0,11608,1053619,3,13060,1065594,4,13785,1098688,5,14515,1098689,5,14516,1098689,1,14516,1098689,50,14517,1098689,40,14517,1098725,0,14517,1131090,3,15968,1135735,4,16693,1141058,5,17418,1141059,5,17419,1141059,1,17419,1141059,50,17419,1141059,40,17419,1141095,0,17419,1141095,50,17419,1141095,40,17419,1141131,0,17420,1802181,4,25387)
%
%
% START OF PROOF
% 1141097 [] sum(X,Y,add(X,Y)).
% 1141101 [] sum(additive_identity,X,X).
% 1141102 [] sum(X,additive_identity,X).
% 1141109 [] -product(X,Y,Z) | -sum(U,Z,X1) | -sum(U,X,W) | -sum(U,Y,V) | product(W,V,X1).
% 1141111 [] -product(X,Y,Z) | -sum(Z,U,X1) | -sum(X,U,W) | -sum(Y,U,V) | product(W,V,X1).
% 1141114 [] sum(X,inverse(X),multiplicative_identity).
% 1141115 [] product(inverse(X),X,additive_identity).
% 1141116 [] product(X,inverse(X),additive_identity).
% 1141117 [] -sum(X,Y,U) | -sum(X,Y,Z) | equal(Z,U).
% 1141118 [] -product(X,Y,U) | -product(X,Y,Z) | equal(Z,U).
% 1141131 [] -equal(inverse(inverse(x)),x).
% 1143494 [hyper:1141117,1141097,1141101] equal(X,add(additive_identity,X)).
% 1143495 [hyper:1141117,1141097,1141102] equal(X,add(X,additive_identity)).
% 1147439 [hyper:1141109,1141115,1141097,1141097,1141114,demod:1143495] product(add(X,inverse(inverse(X))),multiplicative_identity,X).
% 1148579 [hyper:1141111,1141116,1141114,1141097,1141097,demod:1143494] product(add(X,inverse(inverse(X))),multiplicative_identity,inverse(inverse(X))).
% 1802182 [binary:1141118.3,1141131] -product(X,Y,inverse(inverse(x))) | -product(X,Y,x).
% 1802270 [binary:1148579,1802182,cut:1147439] contradiction
% END OF PROOF
%
% Proof found by the following strategy:
%
% using binary resolution
% not using sos strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% seconds given: 105
%
%
% ***GANDALF_FOUND_A_REFUTATION***
%
% Global statistics over all passes:
%
% given clauses: 7608
% derived clauses: 15079468
% kept clauses: 151342
% kept size sum: 26749
% kept mid-nuclei: 1591140
% kept new demods: 164
% forw unit-subs: 11844720
% forw double-subs: 318868
% forw overdouble-subs: 192677
% backward subs: 487
% fast unit cutoff: 19596
% full unit cutoff: 25927
% dbl unit cutoff: 302
% real runtime : 255.55
% process. runtime: 253.90
% specific non-discr-tree subsumption statistics:
% tried: 58665585
% length fails: 1827831
% strength fails: 19676783
% predlist fails: 18420880
% aux str. fails: 2689154
% by-lit fails: 543165
% full subs tried: 15145427
% full subs fail: 14936690
%
% ; 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/BOO/BOO012-3+eq_r.in")
%
%------------------------------------------------------------------------------