%------------------------------------------------------------------------------
% File : Gandalf---c-2.6
% Problem : COL076-1 : TPTP v3.4.2. Released v1.2.0.
% Transfm : add_equality:r
% Format : otter:hypothesis:set(auto),clear(print_given)
% Command : gandalf-wrapper -time %d %s
% Computer : art02.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 209.2s
% Output : Assurance 209.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/COL/COL076-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 4 3)
% (binary-unit 12 #f)
% (binary-unit-uniteq 12 #f)
% (binary-posweight-kb-big-order 60 #f 4 3)
% (binary-posweight-lex-big-order 30 #f 4 3)
% (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)
%
%
% **** EMPTY CLAUSE DERIVED ****
%
%
% timer checkpoints: c(13,40,1,26,0,1,6882,4,2253,20771,5,3002,20772,1,3002,20772,50,3004,20772,40,3004,20785,0,3004,34783,3,3605,36459,4,3905,37699,5,4205,37700,5,4205,37702,1,4205,37702,50,4206,37702,40,4206,37715,0,4206,63894,3,4810,76964,4,5108,83071,5,5407,83071,1,5407,83071,50,5410,83071,40,5410,83084,0,5410,159364,3,8413,160167,4,9911,161102,5,11412,161103,1,11413,161103,50,11418,161103,40,11418,161116,0,11418,199679,3,12920,200601,4,13670,202523,5,14419,202524,1,14419,202524,50,14421,202524,40,14421,202537,0,14421,278793,3,15943,279489,4,16673,291024,5,17422,291025,1,17423,291025,50,17425,291025,40,17425,291038,0,17425)
%
%
% START OF PROOF
% 291027 [] equal(apply(apply(k,X),Y),X).
% 291031 [] equal(apply(pair(X,Y),Z),pair(apply(X,Z),apply(Y,Z))).
% 291032 [] equal(apply(apply(apply(abstraction,X),Y),Z),apply(apply(X,apply(k,Z)),apply(Y,Z))).
% 291035 [] -equal(apply(X,n(X,Y)),apply(Y,n(X,Y))) | equal(X,Y).
% 291037 [] equal(apply(apply(f,X),Y),apply(X,X)).
% 291038 [] -equal(X,apply(eq,pair(apply(k,X),apply(k,projection2)))).
% 291040 [para:291037.1.2,291027.1.1] equal(apply(apply(f,apply(k,X)),Y),X).
% 291045 [para:291037.1.2,291037.1.2] equal(apply(apply(f,X),Y),apply(apply(f,X),Z)).
% 291050 [para:291027.1.1,291031.1.2.2] equal(apply(pair(X,apply(k,Y)),Z),pair(apply(X,Z),Y)).
% 291096 [para:291040.1.1,291032.1.2.1] equal(apply(apply(apply(abstraction,apply(f,apply(k,X))),Y),Z),apply(X,apply(Y,Z))).
% 291133 [para:291027.1.1,291035.1.1] -equal(X,apply(Y,n(apply(k,X),Y))) | equal(apply(k,X),Y).
% 291189 [para:291037.1.1,291045.1.1] equal(apply(X,X),apply(apply(f,X),Y)).
% 291373 [para:291050.1.1,291032.1.2.2] equal(apply(apply(apply(abstraction,X),pair(Y,apply(k,Z))),U),apply(apply(X,apply(k,U)),pair(apply(Y,U),Z))).
% 295546 [para:291096.1.1,291032.1.2,demod:291027] equal(apply(apply(apply(abstraction,apply(abstraction,apply(f,apply(k,X)))),Y),Z),apply(X,Z)).
% 301535 [binary:291189,291133] equal(apply(k,apply(X,X)),apply(f,X)).
% 301665 [para:301535.1.1,291038.1.2.2.1] -equal(apply(X,X),apply(eq,pair(apply(f,X),apply(k,projection2)))).
% 389273 [para:291373.1.1,301665.1.1,slowcut:295546] 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
% seconds given: 156
%
%
% old unit clauses discarded
%
% ***GANDALF_FOUND_A_REFUTATION***
%
% Global statistics over all passes:
%
% given clauses: 10093
% derived clauses: 3837837
% kept clauses: 312419
% kept size sum: 0
% kept mid-nuclei: 14575
% kept new demods: 56072
% forw unit-subs: 1650183
% forw double-subs: 320330
% forw overdouble-subs: 147003
% backward subs: 917
% fast unit cutoff: 54248
% full unit cutoff: 829
% dbl unit cutoff: 1182
% real runtime : 216.1
% process. runtime: 214.98
% specific non-discr-tree subsumption statistics:
% tried: 12135342
% length fails: 243205
% strength fails: 3400878
% predlist fails: 2599208
% aux str. fails: 1703083
% by-lit fails: 65327
% full subs tried: 4061141
% full subs fail: 3911757
%
% ; 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/COL/COL076-1+eq_r.in")
%
%------------------------------------------------------------------------------