%------------------------------------------------------------------------------
% File : Gandalf---c-2.6
% Problem : LAT155-1 : TPTP v3.4.2. Released v3.1.0.
% Transfm : add_equality:r
% Format : otter:hypothesis:set(auto),clear(print_given)
% Command : gandalf-wrapper -time %d %s
% Computer : art04.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 317.5s
% Output : Assurance 317.5s
% 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/LAT/LAT155-1+eq_r.in
% Using automatic strategy selection.
% Time limit in seconds: 600
%
% prove-all-passes started
%
% detected problem class: ueq
%
% strategies selected:
% (binary-posweight-kb-big-order 60 #f 7 1)
% (binary-posweight-lex-big-order 30 #f 7 1)
% (binary 30 #t)
% (binary-posweight-kb-big-order 180 #f)
% (binary-posweight-lex-big-order 120 #f)
% (binary-posweight-firstpref-order 60 #f)
% (binary-posweight-kb-small-order 60 #f)
% (binary-posweight-lex-small-order 60 #f)
%
%
% ********* EMPTY CLAUSE DERIVED *********
%
%
% timer checkpoints: c(11,40,1,22,0,1,39247,3,3010,53247,4,4514,63823,5,6002,63825,1,6002,63825,50,6006,63825,40,6006,63836,0,6006,91128,3,7515,100770,4,8279,109322,5,9007,109322,1,9007,109322,50,9010,109322,40,9010,109333,0,9010,110356,50,9051,110356,40,9051,110367,0,9065,247820,3,18074,322083,4,22632,410481,5,27066,410481,1,27066,410481,50,27071,410481,40,27071,410492,0,27071)
%
%
% START OF PROOF
% 410485 [] equal(meet(X,join(X,Y)),X).
% 410486 [] equal(join(X,meet(X,Y)),X).
% 410487 [] equal(meet(X,Y),meet(Y,X)).
% 410488 [] equal(join(X,Y),join(Y,X)).
% 410489 [] equal(meet(meet(X,Y),Z),meet(X,meet(Y,Z))).
% 410490 [] equal(join(join(X,Y),Z),join(X,join(Y,Z))).
% 410491 [] equal(meet(X,join(Y,meet(Z,join(X,U)))),meet(X,join(Y,join(meet(X,Z),meet(Z,join(Y,U)))))).
% 410492 [] -equal(meet(a,join(b,meet(a,c))),meet(a,join(b,meet(c,join(meet(a,join(b,c)),meet(b,c)))))).
% 410493 [para:410487.1.1,410485.1.1] equal(meet(join(X,Y),X),X).
% 410494 [para:410487.1.1,410486.1.1.2] equal(join(X,meet(Y,X)),X).
% 410501 [para:410488.1.1,410485.1.1.2] equal(meet(X,join(Y,X)),X).
% 410504 [para:410488.1.1,410492.1.2.2] -equal(meet(a,join(b,meet(a,c))),meet(a,join(meet(c,join(meet(a,join(b,c)),meet(b,c))),b))).
% 410507 [para:410493.1.1,410486.1.1.2,demod:410490] equal(join(X,join(Y,X)),join(X,Y)).
% 410508 [para:410488.1.1,410493.1.1.1] equal(meet(join(X,Y),Y),Y).
% 410509 [para:410494.1.1,410488.1.1] equal(X,join(meet(Y,X),X)).
% 410522 [para:410485.1.1,410489.1.1.1] equal(meet(X,Y),meet(X,meet(join(X,Z),Y))).
% 410524 [para:410489.1.1,410487.1.1] equal(meet(X,meet(Y,Z)),meet(Z,meet(X,Y))).
% 410526 [para:410487.1.1,410489.1.1.1,demod:410489] equal(meet(X,meet(Y,Z)),meet(Y,meet(X,Z))).
% 410528 [para:410489.1.1,410494.1.1.2] equal(join(X,meet(Y,meet(Z,X))),X).
% 410529 [para:410486.1.1,410501.1.1.2,demod:410489] equal(meet(X,meet(Y,X)),meet(X,Y)).
% 410531 [para:410501.1.1,410489.1.1.1] equal(meet(X,Y),meet(X,meet(join(Z,X),Y))).
% 410534 [para:410508.1.1,410489.1.1.1] equal(meet(X,Y),meet(join(Z,X),meet(X,Y))).
% 410535 [para:410489.1.1,410509.1.2.1] equal(X,join(meet(Y,meet(Z,X)),X)).
% 410536 [para:410507.1.1,410501.1.1.2] equal(meet(join(X,Y),join(Y,X)),join(X,Y)).
% 410538 [para:410490.1.1,410486.1.1] equal(join(X,join(Y,meet(join(X,Y),Z))),join(X,Y)).
% 410539 [para:410486.1.1,410490.1.1.1] equal(join(X,Y),join(X,join(meet(X,Z),Y))).
% 410540 [para:410490.1.1,410488.1.1] equal(join(X,join(Y,Z)),join(Z,join(X,Y))).
% 410545 [para:410494.1.1,410490.1.1.1] equal(join(X,Y),join(X,join(meet(Z,X),Y))).
% 410548 [para:410490.1.1,410508.1.1.1] equal(meet(join(X,join(Y,Z)),Z),Z).
% 410549 [para:410509.1.2,410490.1.1.1] equal(join(X,Y),join(meet(Z,X),join(X,Y))).
% 410554 [para:410485.1.1,410528.1.1.2.2,demod:410490] equal(join(X,join(Y,meet(Z,X))),join(X,Y)).
% 410555 [para:410487.1.1,410528.1.1.2,demod:410489] equal(join(X,meet(Y,meet(X,Z))),X).
% 410560 [para:410529.1.1,410494.1.1.2] equal(join(meet(X,Y),meet(Y,X)),meet(X,Y)).
% 410576 [para:410486.1.1,410491.1.2.2.2.2.2,demod:410554] equal(meet(X,join(Y,meet(Z,join(X,meet(Y,U))))),meet(X,join(Y,meet(X,Z)))).
% 410578 [para:410487.1.1,410491.1.2.2.2.1] equal(meet(X,join(Y,meet(Z,join(X,U)))),meet(X,join(Y,join(meet(Z,X),meet(Z,join(Y,U)))))).
% 410609 [para:410501.1.1,410535.1.2.1.2] equal(join(X,Y),join(meet(Z,Y),join(X,Y))).
% 410623 [para:410494.1.1,410548.1.1.1.2] equal(meet(join(X,Y),meet(Z,Y)),meet(Z,Y)).
% 410635 [para:410555.1.1,410548.1.1.1.2] equal(meet(join(X,Y),meet(Z,meet(Y,U))),meet(Z,meet(Y,U))).
% 410663 [para:410522.1.2,410487.1.1,demod:410489] equal(meet(X,Y),meet(join(X,Z),meet(Y,X))).
% 410673 [para:410522.1.2,410555.1.1.2,demod:410490] equal(join(X,join(Y,meet(X,Z))),join(X,Y)).
% 410739 [para:410531.1.2,410509.1.2.1] equal(meet(join(X,Y),Z),join(meet(Y,Z),meet(join(X,Y),Z))).
% 410740 [para:410507.1.1,410531.1.2.2.1] equal(meet(join(X,Y),Z),meet(join(X,Y),meet(join(Y,X),Z))).
% 410752 [para:410507.1.1,410534.1.2.1,demod:410740] equal(meet(join(X,Y),Z),meet(join(Y,X),Z)).
% 410761 [para:410536.1.1,410524.1.1.2] equal(meet(X,join(Y,Z)),meet(join(Z,Y),meet(X,join(Y,Z)))).
% 410762 [para:410536.1.1,410526.1.1.2,demod:410761] equal(meet(X,join(Y,Z)),meet(X,join(Z,Y))).
% 410771 [para:410539.1.2,410531.1.2.2.1] equal(meet(join(meet(X,Y),Z),U),meet(join(meet(X,Y),Z),meet(join(X,Z),U))).
% 410823 [para:410529.1.1,410545.1.2.2.1] equal(join(meet(X,Y),Z),join(meet(X,Y),join(meet(Y,X),Z))).
% 410853 [para:410529.1.1,410549.1.2.1,demod:410823] equal(join(meet(X,Y),Z),join(meet(Y,X),Z)).
% 410864 [para:410529.1.1,410554.1.1.2.2] equal(join(meet(X,Y),join(Z,meet(Y,X))),join(meet(X,Y),Z)).
% 410901 [para:410560.1.1,410540.1.1.2,demod:410864] equal(join(X,meet(Y,Z)),join(meet(Z,Y),X)).
% 411074 [para:410536.1.1,410663.1.2.2,demod:410490,410536] equal(join(X,Y),meet(join(X,join(Y,Z)),join(Y,X))).
% 411106 [para:410673.1.1,410609.1.2.2,demod:410673] equal(join(X,Y),join(meet(Z,join(Y,meet(X,U))),join(X,Y))).
% 411109 [para:410673.1.1,410623.1.1.1] equal(meet(join(X,Y),meet(Z,join(Y,meet(X,U)))),meet(Z,join(Y,meet(X,U)))).
% 411257 [para:410752.1.1,410853.1.1.1] equal(join(meet(join(X,Y),Z),U),join(meet(Z,join(Y,X)),U)).
% 411373 [para:410901.1.2,410762.1.1.2] equal(meet(X,join(Y,meet(Z,U))),meet(X,join(Y,meet(U,Z)))).
% 413247 [para:410487.1.1,410576.1.2.2.2] equal(meet(X,join(Y,meet(Z,join(X,meet(Y,U))))),meet(X,join(Y,meet(Z,X)))).
% 413704 [para:410522.1.2,410578.1.2.2.2.1,demod:410578,410489] equal(meet(join(X,Y),meet(Z,join(U,meet(X,join(meet(join(X,Y),Z),V))))),meet(join(X,Y),meet(Z,join(U,meet(X,join(Z,V)))))).
% 420712 [para:410538.1.1,410635.1.1.1] equal(meet(join(X,Y),meet(Z,meet(join(Y,meet(join(X,Y),U)),V))),meet(Z,meet(join(Y,meet(join(X,Y),U)),V))).
% 463877 [para:411106.1.2,411074.1.2.1] equal(join(meet(X,join(Y,meet(Z,U))),Z),meet(join(Z,Y),join(Z,meet(X,join(Y,meet(Z,U)))))).
% 485986 [para:410739.1.2,410771.1.2.1,demod:420712,410489,410739] equal(meet(join(X,Y),meet(Z,U)),meet(Z,meet(join(Y,meet(join(X,Y),Z)),U))).
% 502810 [para:411257.1.2,410504.1.2.2.1.2,demod:411109,413247,413704,485986,463877,cut:411373] 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 lex ordering for equality
% preferring bigger arities for lex ordering
% using clause demodulation
% seconds given: 120
%
%
% old unit clauses discarded
%
% ***GANDALF_FOUND_A_REFUTATION***
%
% Global statistics over all passes:
%
% given clauses: 3600
% derived clauses: 2970032
% kept clauses: 241005
% kept size sum: 0
% kept mid-nuclei: 0
% kept new demods: 169458
% forw unit-subs: 2362800
% forw double-subs: 0
% forw overdouble-subs: 0
% backward subs: 8
% fast unit cutoff: 1
% full unit cutoff: 0
% dbl unit cutoff: 0
% real runtime : 324.50
% process. runtime: 321.53
% specific non-discr-tree subsumption statistics:
% tried: 0
% length fails: 0
% strength fails: 0
% predlist fails: 0
% aux str. fails: 0
% by-lit fails: 0
% full subs tried: 0
% full subs fail: 0
%
% ; 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/LAT/LAT155-1+eq_r.in")
%
%------------------------------------------------------------------------------