%------------------------------------------------------------------------------
% File : Gandalf---c-2.6
% Problem : GRP479-1 : TPTP v3.4.2. Released v2.6.0.
% Transfm : add_equality:r
% Format : otter:hypothesis:set(auto),clear(print_given)
% Command : gandalf-wrapper -time %d %s
% Computer : art07.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 89.8s
% Output : Assurance 89.8s
% 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/GRP479-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 6 1)
% (binary-posweight-lex-big-order 30 #f 6 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(4,40,0,8,0,1,58547,3,3002,203986,4,4509,285239,5,6002,285239,1,6002,285239,50,6005,285239,40,6005,285243,0,6005,306332,3,7527,310766,4,8267,325022,5,9006,325022,1,9006,325022,50,9008,325022,40,9008,325026,0,9008,325026,50,9008,325026,40,9008,325030,0,9021)
%
%
% START OF PROOF
% 325027 [] equal(X,X).
% 325028 [] equal(divide(inverse(divide(divide(divide(X,X),Y),divide(Z,divide(Y,U)))),U),Z).
% 325029 [] equal(multiply(X,Y),divide(X,inverse(Y))).
% 325030 [] -equal(multiply(multiply(inverse(b2),b2),a2),a2).
% 325031 [para:325028.1.1,325029.1.2,demod:325029] equal(multiply(inverse(divide(divide(divide(X,X),Y),divide(Z,multiply(Y,U)))),U),Z).
% 325032 [para:325029.1.2,325028.1.1.1.1.1] equal(divide(inverse(divide(multiply(divide(X,X),Y),divide(Z,divide(inverse(Y),U)))),U),Z).
% 325033 [para:325029.1.2,325028.1.1.1.1.1.1] equal(divide(inverse(divide(divide(multiply(inverse(X),X),Y),divide(Z,divide(Y,U)))),U),Z).
% 325034 [para:325028.1.1,325028.1.1.1.1.2] equal(divide(inverse(divide(divide(divide(X,X),Y),Z)),U),inverse(divide(divide(divide(V,V),W),divide(Z,divide(W,divide(Y,U)))))).
% 325035 [para:325028.1.1,325028.1.1.1.1.2.2,demod:325029] equal(divide(inverse(divide(multiply(divide(X,X),divide(divide(divide(Y,Y),Z),divide(U,divide(Z,V)))),divide(W,U))),V),W).
% 325038 [para:325028.1.1,325031.1.1.1.1.2] equal(multiply(inverse(divide(divide(divide(X,X),Y),Z)),U),inverse(divide(divide(divide(V,V),W),divide(Z,divide(W,multiply(Y,U)))))).
% 325041 [para:325032.1.1,325028.1.1.1.1.2] equal(divide(inverse(divide(divide(divide(X,X),Y),Z)),U),inverse(divide(multiply(divide(V,V),W),divide(Z,divide(inverse(W),divide(Y,U)))))).
% 325043 [para:325028.1.1,325032.1.1.1.1.2] equal(divide(inverse(divide(multiply(divide(X,X),Y),Z)),U),inverse(divide(divide(divide(V,V),W),divide(Z,divide(W,divide(inverse(Y),U)))))).
% 325044 [para:325032.1.1,325031.1.1.1.1.2] equal(multiply(inverse(divide(divide(divide(X,X),Y),Z)),U),inverse(divide(multiply(divide(V,V),W),divide(Z,divide(inverse(W),multiply(Y,U)))))).
% 325045 [para:325032.1.1,325032.1.1.1.1.2] equal(divide(inverse(divide(multiply(divide(X,X),Y),Z)),U),inverse(divide(multiply(divide(V,V),W),divide(Z,divide(inverse(W),divide(inverse(Y),U)))))).
% 325046 [para:325033.1.1,325028.1.1.1.1.2] equal(divide(inverse(divide(divide(divide(X,X),Y),Z)),U),inverse(divide(divide(multiply(inverse(V),V),W),divide(Z,divide(W,divide(Y,U)))))).
% 325050 [para:325033.1.1,325031.1.1.1.1.2] equal(multiply(inverse(divide(divide(divide(X,X),Y),Z)),U),inverse(divide(divide(multiply(inverse(V),V),W),divide(Z,divide(W,multiply(Y,U)))))).
% 325051 [para:325033.1.1,325032.1.1.1.1.2] equal(divide(inverse(divide(multiply(divide(X,X),Y),Z)),U),inverse(divide(divide(multiply(inverse(V),V),W),divide(Z,divide(W,divide(inverse(Y),U)))))).
% 325052 [para:325032.1.1,325033.1.1.1.1.2] equal(divide(inverse(divide(divide(multiply(inverse(X),X),Y),Z)),U),inverse(divide(multiply(divide(V,V),W),divide(Z,divide(inverse(W),divide(Y,U)))))).
% 325054 [para:325033.1.1,325033.1.1.1.1.2] equal(divide(inverse(divide(divide(multiply(inverse(X),X),Y),Z)),U),inverse(divide(divide(multiply(inverse(V),V),W),divide(Z,divide(W,divide(Y,U)))))).
% 325089 [para:325034.1.2,325028.1.1.1] equal(divide(divide(inverse(divide(divide(divide(X,X),Y),Z)),U),divide(Y,U)),Z).
% 325131 [para:325029.1.2,325089.1.1.1,demod:325029] equal(divide(multiply(inverse(divide(divide(divide(X,X),Y),Z)),U),multiply(Y,U)),Z).
% 325132 [para:325029.1.2,325089.1.1.1.1.1] equal(divide(divide(inverse(multiply(divide(divide(X,X),Y),Z)),U),divide(Y,U)),inverse(Z)).
% 325133 [para:325029.1.2,325089.1.1.1.1.1.1] equal(divide(divide(inverse(divide(multiply(divide(X,X),Y),Z)),U),divide(inverse(Y),U)),Z).
% 325134 [para:325029.1.2,325089.1.1.1.1.1.1.1] equal(divide(divide(inverse(divide(divide(multiply(inverse(X),X),Y),Z)),U),divide(Y,U)),Z).
% 325135 [para:325089.1.1,325028.1.1.1.1.1,demod:325029] equal(divide(inverse(divide(X,divide(Y,divide(multiply(Z,divide(divide(divide(U,U),Z),X)),V)))),V),Y).
% 325148 [para:325089.1.1,325034.1.2.1.2,demod:325028] equal(inverse(divide(divide(divide(X,X),Y),Z)),inverse(divide(divide(divide(U,U),Y),Z))).
% 325151 [para:325034.1.2,325089.1.1.1.1] equal(divide(divide(divide(inverse(divide(divide(divide(X,X),Y),Z)),U),V),divide(W,V)),divide(Z,divide(W,divide(Y,U)))).
% 325154 [para:325089.1.1,325089.1.1.1.1.1.1,demod:325029] equal(divide(divide(inverse(divide(X,Y)),Z),divide(multiply(U,divide(divide(divide(V,V),U),X)),Z)),Y).
% 325158 [para:325029.1.2,325131.1.1.1.1.1.1.1] equal(divide(multiply(inverse(divide(divide(multiply(inverse(X),X),Y),Z)),U),multiply(Y,U)),Z).
% 325174 [para:325029.1.2,325132.1.1.1.1.1.1] equal(divide(divide(inverse(multiply(multiply(divide(X,X),Y),Z)),U),divide(inverse(Y),U)),inverse(Z)).
% 325190 [para:325132.1.1,325034.1.2.1.2,demod:325029,325028] equal(inverse(multiply(divide(divide(X,X),Y),Z)),inverse(multiply(divide(divide(U,U),Y),Z))).
% 325234 [para:325134.1.1,325034.1.2.1.2,demod:325028] equal(inverse(divide(divide(multiply(inverse(X),X),Y),Z)),inverse(divide(divide(divide(U,U),Y),Z))).
% 325300 [para:325148.1.1,325029.1.2.2,demod:325029] equal(multiply(X,divide(divide(divide(Y,Y),Z),U)),multiply(X,divide(divide(divide(V,V),Z),U))).
% 325371 [para:325190.1.1,325029.1.2.2,demod:325029] equal(multiply(X,multiply(divide(divide(Y,Y),Z),U)),multiply(X,multiply(divide(divide(V,V),Z),U))).
% 325639 [para:325234.1.1,325029.1.2.2,demod:325029] equal(multiply(X,divide(divide(multiply(inverse(Y),Y),Z),U)),multiply(X,divide(divide(divide(V,V),Z),U))).
% 326191 [para:325043.1.1,325035.1.1,demod:325028] equal(inverse(divide(divide(divide(X,X),Y),divide(divide(Z,U),divide(Y,U)))),Z).
% 326284 [para:325029.1.2,326191.1.1.1.1] equal(inverse(divide(multiply(divide(X,X),Y),divide(divide(Z,U),divide(inverse(Y),U)))),Z).
% 326286 [para:325029.1.2,326191.1.1.1.2.1,demod:325029] equal(inverse(divide(divide(divide(X,X),Y),divide(multiply(Z,U),multiply(Y,U)))),Z).
% 326299 [para:326191.1.1,325089.1.1.1.1] equal(divide(divide(X,Y),divide(Z,Y)),divide(divide(X,U),divide(Z,U))).
% 326300 [para:325089.1.1,326191.1.1.1.1,demod:325029] equal(inverse(divide(X,divide(divide(Y,Z),divide(multiply(U,divide(divide(divide(V,V),U),X)),Z)))),Y).
% 326302 [para:326191.1.1,325131.1.1.1.1] equal(divide(multiply(X,Y),multiply(Z,Y)),divide(divide(X,U),divide(Z,U))).
% 326346 [para:326299.1.1,325028.1.1.1.1.1] equal(divide(inverse(divide(divide(divide(X,Y),divide(Z,Y)),divide(U,divide(divide(Z,X),V)))),V),U).
% 326349 [para:325028.1.1,326299.1.1.2] equal(divide(divide(X,Y),Z),divide(divide(X,U),divide(inverse(divide(divide(divide(V,V),W),divide(Z,divide(W,Y)))),U))).
% 326350 [para:326299.1.1,325031.1.1.1.1.1] equal(multiply(inverse(divide(divide(divide(X,Y),divide(Z,Y)),divide(U,multiply(divide(Z,X),V)))),V),U).
% 326368 [para:326299.1.1,325089.1.1.1.1.1] equal(divide(divide(inverse(divide(divide(divide(X,X),Y),divide(Z,Y))),U),divide(V,U)),divide(Z,V)).
% 326371 [para:325089.1.1,326299.1.1.2] equal(divide(divide(X,divide(Y,Z)),U),divide(divide(X,V),divide(divide(inverse(divide(divide(divide(W,W),Y),U)),Z),V))).
% 326449 [para:325029.1.2,326302.1.2.1,demod:325029] equal(divide(multiply(X,Y),multiply(Z,Y)),divide(multiply(X,U),multiply(Z,U))).
% 326765 [para:326286.1.1,325029.1.2.2] equal(multiply(X,divide(divide(divide(Y,Y),Z),divide(multiply(U,V),multiply(Z,V)))),divide(X,U)).
% 326766 [para:325029.1.2,326286.1.1.1.1.1] equal(inverse(divide(divide(multiply(inverse(X),X),Y),divide(multiply(Z,U),multiply(Y,U)))),Z).
% 327334 [para:325089.1.1,325300.1.1.2.1,demod:325029] equal(multiply(X,divide(Y,Z)),multiply(X,divide(divide(divide(U,U),multiply(V,divide(divide(divide(W,W),V),Y))),Z))).
% 327620 [para:325132.1.1,325371.1.1.2.1,demod:325029] equal(multiply(X,multiply(inverse(Y),Z)),multiply(X,multiply(divide(divide(U,U),multiply(V,multiply(divide(divide(W,W),V),Y))),Z))).
% 331292 [para:326368.1.1,326299.1.1.1,demod:325151] equal(divide(divide(X,Y),divide(Z,divide(Y,U))),divide(divide(X,V),divide(Z,divide(V,U)))).
% 331293 [para:326368.1.1,326299.1.1.2,demod:326371] equal(divide(divide(X,divide(Y,Z)),divide(U,Y)),divide(divide(X,divide(V,Z)),divide(U,V))).
% 331368 [para:326368.1.1,325154.1.1] equal(divide(X,multiply(Y,divide(divide(divide(Z,Z),Y),divide(divide(U,U),V)))),divide(X,V)).
% 332277 [para:331368.1.1,325089.1.1.1.1.1,demod:325089] equal(X,multiply(Y,divide(divide(divide(Z,Z),Y),divide(divide(U,U),X)))).
% 332414 [para:326299.1.1,332277.1.2.2] equal(X,multiply(X,divide(divide(divide(Y,Y),Z),divide(divide(U,U),Z)))).
% 332499 [para:325034.1.1,332414.1.2.2.2.1,demod:327334,326349,325029] equal(X,multiply(X,divide(Y,Y))).
% 332503 [para:325132.1.1,332414.1.2.2.2,demod:327620,325029] equal(X,multiply(X,multiply(inverse(Y),Y))).
% 332511 [para:332414.1.2,325158.1.1.1,demod:332414] equal(divide(inverse(divide(divide(multiply(inverse(X),X),Y),Z)),Y),Z).
% 332537 [para:332414.1.2,326302.1.1.1,demod:332414] equal(divide(X,Y),divide(divide(X,Z),divide(Y,Z))).
% 332540 [para:326302.1.1,332414.1.2.2.1.1,demod:332537] equal(X,multiply(X,divide(divide(Y,Y),divide(Z,Z)))).
% 332542 [para:332414.1.2,326449.1.1.1,demod:332540,332537] equal(divide(X,Y),divide(multiply(X,Z),multiply(Y,Z))).
% 332545 [para:332414.1.2,326286.1.1.1.2.1,demod:332540,332537] equal(inverse(divide(divide(X,X),Y)),Y).
% 332546 [para:332414.1.2,326284.1.1.1.1,demod:332545,332537] equal(divide(X,divide(Y,Y)),X).
% 332548 [para:332414.1.2,326766.1.1.1.2.1,demod:332499,332546,332537] equal(inverse(divide(multiply(inverse(X),X),Y)),Y).
% 332573 [para:332414.1.2,326765.1.1.2.2.1,demod:332499,332546,332537] equal(multiply(X,divide(divide(Y,Y),Z)),divide(X,Z)).
% 332614 [para:332499.1.2,325174.1.1.1.1.1.1,demod:332499,325029,332537] equal(inverse(multiply(divide(X,X),Y)),inverse(Y)).
% 332632 [para:332499.1.2,325639.1.1,demod:332573,332537] equal(X,divide(X,multiply(inverse(Y),Y))).
% 332643 [para:332546.1.1,325089.1.1.1.1.1,demod:332537,332545] equal(divide(X,X),divide(Y,Y)).
% 332644 [para:332546.1.1,325133.1.1.1.1.1,demod:325029,332537,332614] equal(multiply(inverse(X),X),divide(Y,Y)).
% 332682 [para:332546.1.1,325135.1.1.1.1] equal(divide(inverse(X),Y),divide(multiply(Z,divide(divide(divide(U,U),Z),X)),Y)).
% 332685 [para:325135.1.1,332546.1.1,demod:325029,332546,332682] equal(X,inverse(divide(Y,multiply(X,Y)))).
% 332702 [para:332546.1.1,326300.1.1.1] equal(inverse(X),multiply(Y,divide(divide(divide(Z,Z),Y),X))).
% 332707 [para:332546.1.1,326346.1.1.1.1,demod:332537] equal(divide(inverse(divide(X,Y)),Z),divide(divide(Y,X),Z)).
% 332710 [para:332546.1.1,326350.1.1.1.1,demod:332537] equal(multiply(inverse(divide(X,Y)),Z),multiply(divide(Y,X),Z)).
% 332713 [para:332546.1.1,331292.1.1.2] equal(divide(divide(X,Y),Z),divide(divide(X,U),divide(Z,divide(U,Y)))).
% 332715 [para:332546.1.1,331293.1.1] equal(divide(X,divide(Y,Z)),divide(divide(X,divide(U,Z)),divide(Y,U))).
% 332716 [para:332546.1.1,331293.1.1.2,demod:332715] equal(divide(divide(X,divide(divide(Y,Y),Z)),U),divide(X,divide(U,Z))).
% 332766 [para:325089.1.1,325054.1.2.1.2.2,demod:332548,332715,332716,332707] equal(divide(divide(X,divide(multiply(inverse(Y),Y),Z)),U),divide(X,divide(U,Z))).
% 332776 [para:325054.1.2,325134.1.1.1.1,demod:332537,332766,332707] equal(divide(divide(X,divide(Y,Z)),U),divide(X,divide(U,divide(Z,Y)))).
% 332790 [para:325158.1.1,325054.1.1.1.1.1,demod:332548,332776,332713,332707] equal(divide(divide(X,Y),Z),divide(X,divide(Z,multiply(U,divide(divide(multiply(inverse(V),V),U),Y))))).
% 332838 [para:325054.1.1,325041.1.1.1.1.1.1,demod:332503,332776,332707,332546,332537,332790,325029] equal(divide(X,divide(Y,Z)),inverse(divide(multiply(divide(U,U),V),divide(X,divide(inverse(V),divide(Z,Y)))))).
% 332841 [para:325054.1.1,325041.1.2.1.2.2,demod:332548,332776,332713,332716,332707] equal(divide(X,divide(Y,Z)),inverse(divide(multiply(divide(U,U),divide(divide(multiply(inverse(V),V),W),X1)),divide(X,divide(X1,divide(divide(Z,Y),W)))))).
% 332868 [para:325054.1.1,325043.1.2.1.2.2,demod:332841,332548,332776,332713,325029,332707] equal(divide(divide(X,multiply(divide(Y,Y),Z)),U),divide(X,multiply(U,Z))).
% 332929 [para:325154.1.1,325054.1.2.1.2,demod:325029,332702,332511,332713,332707] equal(divide(X,Y),inverse(divide(multiply(multiply(inverse(Z),Z),Y),X))).
% 332943 [para:325054.1.2,325051.1.2,demod:332929,325029,332868,332707] equal(divide(X,multiply(Y,Z)),divide(divide(X,Z),Y)).
% 332977 [para:325054.1.1,325052.1.1,demod:332838,332548,332943] equal(multiply(divide(X,divide(Y,divide(Z,U))),Y),divide(X,divide(U,Z))).
% 332981 [para:325054.1.1,325052.1.2.1.2,demod:332838,332776,332977,332548,332943] equal(divide(multiply(multiply(X,Y),Z),U),divide(X,divide(U,multiply(Y,Z)))).
% 332984 [para:325054.1.1,325052.1.2.1.2.2.2,demod:332838,332977,332548,332943] equal(divide(multiply(X,multiply(Y,Z)),U),divide(X,divide(U,multiply(Y,Z)))).
% 332998 [para:325054.1.1,326368.1.1.1.1.1.2,demod:332715,332776,332984,332707,332548,332977,332943] equal(divide(X,divide(Y,divide(Z,multiply(divide(U,multiply(V,U)),V)))),divide(multiply(X,Z),Y)).
% 333001 [para:326368.1.1,325054.1.2.1.2.2.2,demod:332977,332537,332548,332998,332776,332984,332707,332943] equal(divide(multiply(X,Y),Z),divide(X,divide(Z,Y))).
% 333007 [para:331292.1.1,325054.1.1.1.1,demod:332632,332943,332707,332715,332776,333001] equal(divide(X,divide(Y,Z)),inverse(divide(inverse(U),divide(X,divide(U,divide(Z,Y)))))).
% 333035 [para:332546.1.1,325054.1.2.1,demod:332546,332632,332943,332707,332715,332776,333001] equal(X,inverse(divide(inverse(Y),divide(X,Y)))).
% 333036 [para:332546.1.1,325054.1.2.1.1,demod:333007,332632,332943,332707,332776,333001] equal(divide(X,divide(Y,Z)),divide(X,divide(U,multiply(divide(Z,Y),U)))).
% 333047 [para:332643.1.1,325032.1.1.1.1.2,demod:332685,332943,333001] equal(divide(X,multiply(Y,multiply(Z,X))),divide(inverse(Z),Y)).
% 333056 [para:332643.1.1,325034.1.2.1.2.2,demod:332546,333001,325029,332707,333047,332943] equal(divide(X,divide(Y,Z)),inverse(divide(Y,multiply(X,Z)))).
% 333076 [para:332643.1.1,325038.1.2.1.1,demod:333036,332981,332776,333056,325029,332710,333047,332943] equal(multiply(multiply(X,Y),Z),divide(X,divide(inverse(Z),Y))).
% 333113 [para:332643.1.1,326299.1.1.2,demod:332537,332943] equal(divide(X,multiply(divide(Y,Y),Z)),divide(X,Z)).
% 333115 [para:332643.1.1,325044.1.1.1.1.1,demod:333001,332542,333076,333113,332546,333056,332943] equal(multiply(X,Y),divide(X,divide(Z,multiply(Y,Z)))).
% 333116 [para:332643.1.1,325044.1.1.1.1.1.1,demod:333115,332984,333056,332542,333076,325029,332710,333047,332943] equal(multiply(multiply(X,Y),Z),multiply(X,multiply(Y,Z))).
% 333118 [para:332643.1.1,325045.1.1.1.1,demod:332546,333056,332542,325029,333047,333115,332984,333001,333116,333076,332943,332707] equal(divide(X,multiply(Y,X)),inverse(Y)).
% 333126 [para:332643.1.1,325046.1.2.1.1,demod:333047,333056,333116,333076,333001,325029,332707,333118,332943] equal(divide(X,divide(Y,Z)),multiply(X,multiply(divide(Z,multiply(U,Y)),U))).
% 333139 [para:332643.1.1,325050.1.1.1.1,demod:333035,333126,333116,333076,332715,332776,333118,332943,333001,332710] equal(multiply(divide(X,X),Y),Y).
% 333175 [para:332644.1.1,325030.1.1.1,demod:333139,cut:325027] 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: 180
%
%
% ***GANDALF_FOUND_A_REFUTATION***
%
% Global statistics over all passes:
%
% given clauses: 1523
% derived clauses: 6705033
% kept clauses: 82840
% kept size sum: 262588
% kept mid-nuclei: 0
% kept new demods: 4273
% forw unit-subs: 1161795
% forw double-subs: 0
% forw overdouble-subs: 0
% backward subs: 29
% fast unit cutoff: 1
% full unit cutoff: 0
% dbl unit cutoff: 0
% real runtime : 91.15
% process. runtime: 90.91
% 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/GRP/GRP479-1+eq_r.in")
%
%------------------------------------------------------------------------------