%------------------------------------------------------------------------------
% File : EQP---0.9e
% Problem : GRP434-1 : TPTP v8.1.0. Released v2.6.0.
% Transfm : none
% Format : tptp:raw
% Command : tptp2X_and_run_eqp %s
% Computer : n015.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 600s
% DateTime : Sat Jul 16 08:47:09 EDT 2022
% Result : Unsatisfiable 0.82s 1.19s
% Output : Refutation 0.82s
% Verified :
% SZS Type : Refutation
% Derivation depth : 27
% Number of leaves : 2
% Syntax : Number of clauses : 63 ( 63 unt; 0 nHn; 2 RR)
% Number of literals : 63 ( 0 equ; 1 neg)
% Maximal clause size : 1 ( 1 avg)
% Maximal term depth : 15 ( 3 avg)
% Number of predicates : 2 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 4 ( 4 usr; 2 con; 0-2 aty)
% Number of variables : 241 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(1,plain,
equal(inverse(multiply(multiply(multiply(inverse(multiply(multiply(A,B),C)),A),B),multiply(D,inverse(D)))),C),
file('GRP434-1.p',unknown),
[] ).
cnf(2,plain,
~ equal(multiply(multiply(inverse(b2),b2),a2),a2),
file('GRP434-1.p',unknown),
[] ).
cnf(3,plain,
equal(inverse(multiply(multiply(multiply(A,multiply(inverse(multiply(multiply(B,C),A)),B)),C),multiply(D,inverse(D)))),multiply(E,inverse(E))),
inference(para,[status(thm),theory(equality)],[1,1]),
[iquote('para(1,1)')] ).
cnf(4,plain,
equal(multiply(A,inverse(A)),inverse(multiply(multiply(multiply(B,multiply(inverse(multiply(multiply(C,D),B)),C)),D),multiply(E,inverse(E))))),
inference(flip,[status(thm),theory(equality)],[3]),
[iquote('flip(3)')] ).
cnf(6,plain,
equal(inverse(multiply(multiply(multiply(multiply(A,inverse(A)),multiply(B,multiply(inverse(multiply(multiply(C,D),B)),C))),D),multiply(E,inverse(E)))),multiply(F,inverse(F))),
inference(para,[status(thm),theory(equality)],[3,1]),
[iquote('para(3,1)')] ).
cnf(7,plain,
equal(multiply(A,inverse(A)),inverse(multiply(multiply(multiply(multiply(B,inverse(B)),multiply(C,multiply(inverse(multiply(multiply(D,E),C)),D))),E),multiply(F,inverse(F))))),
inference(flip,[status(thm),theory(equality)],[6]),
[iquote('flip(6)')] ).
cnf(13,plain,
equal(multiply(A,inverse(A)),multiply(B,inverse(B))),
inference(para,[status(thm),theory(equality)],[3,3]),
[iquote('para(3,3)')] ).
cnf(14,plain,
equal(inverse(multiply(multiply(multiply(inverse(multiply(multiply(A,inverse(A)),B)),C),inverse(C)),multiply(D,inverse(D)))),B),
inference(para,[status(thm),theory(equality)],[13,1]),
[iquote('para(13,1)')] ).
cnf(15,plain,
equal(inverse(multiply(multiply(multiply(inverse(multiply(A,inverse(A))),B),C),multiply(D,inverse(D)))),inverse(multiply(B,C))),
inference(para,[status(thm),theory(equality)],[13,1]),
[iquote('para(13,1)')] ).
cnf(16,plain,
equal(inverse(multiply(multiply(multiply(inverse(multiply(inverse(multiply(multiply(multiply(A,multiply(inverse(multiply(multiply(B,C),A)),B)),C),multiply(D,inverse(D)))),E)),F),inverse(F)),multiply(G,inverse(G)))),E),
inference(para,[status(thm),theory(equality)],[4,1]),
[iquote('para(4,1)')] ).
cnf(18,plain,
equal(inverse(multiply(multiply(multiply(inverse(multiply(multiply(A,B),C)),A),B),inverse(multiply(multiply(multiply(D,multiply(inverse(multiply(multiply(E,F),D)),E)),F),multiply(G,inverse(G)))))),C),
inference(para,[status(thm),theory(equality)],[4,1]),
[iquote('para(4,1)')] ).
cnf(20,plain,
equal(inverse(multiply(multiply(multiply(A,inverse(A)),B),multiply(C,inverse(C)))),inverse(multiply(inverse(inverse(multiply(D,inverse(D)))),B))),
inference(para,[status(thm),theory(equality)],[13,15]),
[iquote('para(13,15)')] ).
cnf(21,plain,
equal(inverse(multiply(inverse(inverse(multiply(A,inverse(A)))),B)),inverse(multiply(multiply(multiply(C,inverse(C)),B),multiply(D,inverse(D))))),
inference(flip,[status(thm),theory(equality)],[20]),
[iquote('flip(20)')] ).
cnf(22,plain,
equal(inverse(multiply(multiply(A,inverse(A)),multiply(B,inverse(B)))),inverse(multiply(C,inverse(multiply(inverse(multiply(D,inverse(D))),C))))),
inference(para,[status(thm),theory(equality)],[13,15]),
[iquote('para(13,15)')] ).
cnf(23,plain,
equal(inverse(multiply(A,inverse(multiply(inverse(multiply(B,inverse(B))),A)))),inverse(multiply(multiply(C,inverse(C)),multiply(D,inverse(D))))),
inference(flip,[status(thm),theory(equality)],[22]),
[iquote('flip(22)')] ).
cnf(97,plain,
equal(inverse(multiply(multiply(multiply(inverse(multiply(multiply(A,inverse(A)),B)),C),inverse(C)),inverse(multiply(multiply(multiply(D,multiply(inverse(multiply(multiply(E,F),D)),E)),F),multiply(G,inverse(G)))))),B),
inference(para,[status(thm),theory(equality)],[13,18]),
[iquote('para(13,18)')] ).
cnf(121,plain,
equal(inverse(multiply(multiply(multiply(inverse(multiply(inverse(inverse(multiply(A,inverse(A)))),inverse(multiply(B,inverse(B))))),C),inverse(C)),multiply(D,inverse(D)))),multiply(E,inverse(E))),
inference(para,[status(thm),theory(equality)],[20,14]),
[iquote('para(20,14)')] ).
cnf(130,plain,
equal(inverse(multiply(multiply(multiply(A,inverse(A)),inverse(inverse(inverse(multiply(inverse(inverse(multiply(B,inverse(B)))),inverse(multiply(C,inverse(C)))))))),multiply(D,inverse(D)))),multiply(E,inverse(E))),
inference(para,[status(thm),theory(equality)],[13,121]),
[iquote('para(13,121)')] ).
cnf(131,plain,
equal(multiply(A,inverse(A)),inverse(multiply(multiply(multiply(B,inverse(B)),inverse(inverse(inverse(multiply(inverse(inverse(multiply(C,inverse(C)))),inverse(multiply(D,inverse(D)))))))),multiply(E,inverse(E))))),
inference(flip,[status(thm),theory(equality)],[130]),
[iquote('flip(130)')] ).
cnf(163,plain,
equal(multiply(A,inverse(A)),inverse(multiply(inverse(multiply(B,inverse(B))),multiply(C,inverse(C))))),
inference(demod,[status(thm),theory(equality)],[inference(para,[status(thm),theory(equality)],[23,14]),14]),
[iquote('para(23,14),demod([14])')] ).
cnf(175,plain,
equal(inverse(multiply(multiply(multiply(inverse(multiply(multiply(A,B),C)),A),B),inverse(multiply(inverse(multiply(D,inverse(D))),multiply(E,inverse(E)))))),C),
inference(para,[status(thm),theory(equality)],[163,1]),
[iquote('para(163,1)')] ).
cnf(180,plain,
equal(inverse(multiply(multiply(multiply(inverse(multiply(A,inverse(A))),B),C),inverse(multiply(inverse(multiply(D,inverse(D))),multiply(E,inverse(E)))))),inverse(multiply(B,C))),
inference(para,[status(thm),theory(equality)],[13,175]),
[iquote('para(13,175)')] ).
cnf(207,plain,
equal(inverse(multiply(multiply(multiply(A,inverse(A)),B),inverse(multiply(inverse(multiply(C,inverse(C))),multiply(D,inverse(D)))))),inverse(multiply(inverse(inverse(multiply(E,inverse(E)))),B))),
inference(para,[status(thm),theory(equality)],[13,180]),
[iquote('para(13,180)')] ).
cnf(208,plain,
equal(inverse(multiply(inverse(inverse(multiply(A,inverse(A)))),B)),inverse(multiply(multiply(multiply(C,inverse(C)),B),inverse(multiply(inverse(multiply(D,inverse(D))),multiply(E,inverse(E))))))),
inference(flip,[status(thm),theory(equality)],[207]),
[iquote('flip(207)')] ).
cnf(316,plain,
equal(inverse(multiply(multiply(inverse(multiply(multiply(multiply(A,multiply(inverse(multiply(multiply(B,C),A)),B)),C),multiply(D,inverse(D)))),inverse(inverse(inverse(multiply(multiply(E,inverse(E)),F))))),multiply(G,inverse(G)))),F),
inference(para,[status(thm),theory(equality)],[4,14]),
[iquote('para(4,14)')] ).
cnf(340,plain,
equal(inverse(multiply(multiply(inverse(multiply(multiply(A,B),inverse(multiply(C,inverse(C))))),A),B)),multiply(D,inverse(D))),
inference(para,[status(thm),theory(equality)],[15,3]),
[iquote('para(15,3)')] ).
cnf(342,plain,
equal(inverse(multiply(multiply(inverse(multiply(multiply(multiply(A,multiply(inverse(multiply(multiply(B,C),A)),B)),C),multiply(D,inverse(D)))),E),multiply(F,inverse(F)))),inverse(multiply(inverse(inverse(multiply(G,inverse(G)))),E))),
inference(para,[status(thm),theory(equality)],[4,15]),
[iquote('para(4,15)')] ).
cnf(343,plain,
equal(inverse(multiply(inverse(inverse(multiply(A,inverse(A)))),B)),inverse(multiply(multiply(inverse(multiply(multiply(multiply(C,multiply(inverse(multiply(multiply(D,E),C)),D)),E),multiply(F,inverse(F)))),B),multiply(G,inverse(G))))),
inference(flip,[status(thm),theory(equality)],[342]),
[iquote('flip(342)')] ).
cnf(356,plain,
equal(inverse(multiply(multiply(multiply(multiply(A,inverse(A)),inverse(multiply(multiply(B,C),inverse(multiply(D,inverse(D)))))),B),multiply(E,inverse(E)))),C),
inference(para,[status(thm),theory(equality)],[340,1]),
[iquote('para(340,1)')] ).
cnf(358,plain,
equal(inverse(multiply(multiply(multiply(A,inverse(A)),B),multiply(C,inverse(C)))),inverse(B)),
inference(para,[status(thm),theory(equality)],[13,356]),
[iquote('para(13,356)')] ).
cnf(372,plain,
equal(multiply(A,inverse(A)),inverse(inverse(inverse(inverse(multiply(inverse(inverse(multiply(B,inverse(B)))),inverse(multiply(C,inverse(C))))))))),
inference(demod,[status(thm),theory(equality)],[inference(demod,[status(thm),theory(equality)],[131]),358]),
[iquote('back_demod(131),demod([358])')] ).
cnf(373,plain,
equal(inverse(inverse(inverse(inverse(multiply(inverse(inverse(multiply(A,inverse(A)))),inverse(multiply(B,inverse(B)))))))),multiply(C,inverse(C))),
inference(flip,[status(thm),theory(equality)],[372]),
[iquote('flip(372)')] ).
cnf(378,plain,
equal(inverse(multiply(inverse(inverse(multiply(A,inverse(A)))),B)),inverse(B)),
inference(demod,[status(thm),theory(equality)],[inference(demod,[status(thm),theory(equality)],[21]),358]),
[iquote('back_demod(21),demod([358])')] ).
cnf(379,plain,
equal(inverse(inverse(inverse(inverse(inverse(multiply(A,inverse(A))))))),multiply(B,inverse(B))),
inference(demod,[status(thm),theory(equality)],[inference(demod,[status(thm),theory(equality)],[373]),378]),
[iquote('back_demod(373),demod([378])')] ).
cnf(381,plain,
equal(inverse(multiply(multiply(inverse(multiply(multiply(multiply(A,multiply(inverse(multiply(multiply(B,C),A)),B)),C),multiply(D,inverse(D)))),E),multiply(F,inverse(F)))),inverse(E)),
inference(flip,[status(thm),theory(equality)],[inference(demod,[status(thm),theory(equality)],[inference(demod,[status(thm),theory(equality)],[343]),378]),1]),
[iquote('back_demod(343),demod([378]),flip(1)')] ).
cnf(382,plain,
equal(inverse(inverse(inverse(inverse(multiply(multiply(A,inverse(A)),B))))),B),
inference(demod,[status(thm),theory(equality)],[inference(demod,[status(thm),theory(equality)],[316]),381]),
[iquote('back_demod(316),demod([381])')] ).
cnf(399,plain,
equal(inverse(multiply(multiply(multiply(A,inverse(A)),B),inverse(multiply(inverse(multiply(C,inverse(C))),multiply(D,inverse(D)))))),inverse(B)),
inference(flip,[status(thm),theory(equality)],[inference(demod,[status(thm),theory(equality)],[inference(demod,[status(thm),theory(equality)],[208]),378]),1]),
[iquote('back_demod(208),demod([378]),flip(1)')] ).
cnf(415,plain,
equal(inverse(multiply(multiply(multiply(inverse(multiply(A,inverse(A))),B),C),inverse(multiply(multiply(multiply(multiply(D,inverse(D)),multiply(E,multiply(inverse(multiply(multiply(F,G),E)),F))),G),multiply(H,inverse(H)))))),inverse(multiply(B,C))),
inference(para,[status(thm),theory(equality)],[7,15]),
[iquote('para(7,15)')] ).
cnf(439,plain,
equal(inverse(inverse(multiply(A,inverse(A)))),multiply(B,inverse(B))),
inference(para,[status(thm),theory(equality)],[382,379]),
[iquote('para(382,379)')] ).
cnf(440,plain,
equal(multiply(A,inverse(A)),inverse(inverse(multiply(B,inverse(B))))),
inference(flip,[status(thm),theory(equality)],[439]),
[iquote('flip(439)')] ).
cnf(449,plain,
equal(inverse(multiply(multiply(multiply(inverse(multiply(inverse(multiply(multiply(multiply(A,multiply(inverse(multiply(multiply(B,C),A)),B)),C),multiply(D,inverse(D)))),E)),F),inverse(F)),inverse(multiply(multiply(multiply(G,multiply(inverse(multiply(multiply(H,I),G)),H)),I),multiply(J,inverse(J)))))),E),
inference(para,[status(thm),theory(equality)],[4,16]),
[iquote('para(4,16)')] ).
cnf(450,plain,
equal(inverse(inverse(inverse(inverse(multiply(multiply(inverse(multiply(A,inverse(A))),multiply(B,inverse(B))),C))))),C),
inference(para,[status(thm),theory(equality)],[439,382]),
[iquote('para(439,382)')] ).
cnf(451,plain,
equal(inverse(inverse(multiply(A,inverse(A)))),inverse(multiply(B,inverse(B)))),
inference(para,[status(thm),theory(equality)],[439,382]),
[iquote('para(439,382)')] ).
cnf(457,plain,
equal(inverse(multiply(A,inverse(A))),multiply(B,inverse(B))),
inference(para,[status(thm),theory(equality)],[451,439]),
[iquote('para(451,439)')] ).
cnf(458,plain,
equal(multiply(A,inverse(A)),inverse(multiply(B,inverse(B)))),
inference(flip,[status(thm),theory(equality)],[457]),
[iquote('flip(457)')] ).
cnf(472,plain,
equal(inverse(inverse(inverse(inverse(multiply(inverse(multiply(A,inverse(A))),B))))),B),
inference(para,[status(thm),theory(equality)],[458,382]),
[iquote('para(458,382)')] ).
cnf(479,plain,
equal(inverse(inverse(inverse(inverse(A)))),A),
inference(demod,[status(thm),theory(equality)],[inference(para,[status(thm),theory(equality)],[440,382]),378]),
[iquote('para(440,382),demod([378])')] ).
cnf(480,plain,
equal(multiply(inverse(multiply(A,inverse(A))),B),B),
inference(demod,[status(thm),theory(equality)],[inference(demod,[status(thm),theory(equality)],[472]),479]),
[iquote('back_demod(472),demod([479])')] ).
cnf(481,plain,
equal(multiply(multiply(A,inverse(A)),B),B),
inference(demod,[status(thm),theory(equality)],[inference(demod,[status(thm),theory(equality)],[450]),480,479]),
[iquote('back_demod(450),demod([480,479])')] ).
cnf(485,plain,
equal(inverse(multiply(multiply(A,B),inverse(multiply(multiply(multiply(C,multiply(inverse(multiply(multiply(D,E),C)),D)),E),multiply(F,inverse(F)))))),inverse(multiply(A,B))),
inference(demod,[status(thm),theory(equality)],[inference(demod,[status(thm),theory(equality)],[415]),480,481]),
[iquote('back_demod(415),demod([480,481])')] ).
cnf(486,plain,
equal(inverse(multiply(multiply(inverse(multiply(inverse(multiply(multiply(multiply(A,multiply(inverse(multiply(multiply(B,C),A)),B)),C),multiply(D,inverse(D)))),E)),F),inverse(F))),E),
inference(demod,[status(thm),theory(equality)],[inference(demod,[status(thm),theory(equality)],[449]),485]),
[iquote('back_demod(449),demod([485])')] ).
cnf(488,plain,
equal(inverse(multiply(multiply(inverse(A),B),inverse(B))),A),
inference(demod,[status(thm),theory(equality)],[inference(demod,[status(thm),theory(equality)],[97]),481,485]),
[iquote('back_demod(97),demod([481,485])')] ).
cnf(489,plain,
equal(multiply(inverse(multiply(multiply(multiply(A,multiply(inverse(multiply(multiply(B,C),A)),B)),C),multiply(D,inverse(D)))),E),E),
inference(demod,[status(thm),theory(equality)],[inference(demod,[status(thm),theory(equality)],[486]),488]),
[iquote('back_demod(486),demod([488])')] ).
cnf(504,plain,
equal(inverse(multiply(A,multiply(B,inverse(B)))),inverse(A)),
inference(demod,[status(thm),theory(equality)],[inference(demod,[status(thm),theory(equality)],[381]),489]),
[iquote('back_demod(381),demod([489])')] ).
cnf(520,plain,
equal(inverse(multiply(A,inverse(multiply(B,inverse(B))))),inverse(A)),
inference(demod,[status(thm),theory(equality)],[inference(demod,[status(thm),theory(equality)],[399]),481,480]),
[iquote('back_demod(399),demod([481,480])')] ).
cnf(522,plain,
equal(inverse(multiply(inverse(multiply(A,B)),A)),B),
inference(demod,[status(thm),theory(equality)],[inference(demod,[status(thm),theory(equality)],[356]),520,481,504]),
[iquote('back_demod(356),demod([520,481,504])')] ).
cnf(598,plain,
equal(inverse(inverse(inverse(A))),multiply(inverse(multiply(B,A)),B)),
inference(para,[status(thm),theory(equality)],[522,479]),
[iquote('para(522,479)')] ).
cnf(599,plain,
equal(multiply(inverse(multiply(A,B)),A),inverse(inverse(inverse(B)))),
inference(flip,[status(thm),theory(equality)],[598]),
[iquote('flip(598)')] ).
cnf(604,plain,
equal(multiply(multiply(multiply(inverse(multiply(A,B)),A),B),C),C),
inference(para,[status(thm),theory(equality)],[522,481]),
[iquote('para(522,481)')] ).
cnf(605,plain,
equal(inverse(inverse(A)),A),
inference(demod,[status(thm),theory(equality)],[inference(para,[status(thm),theory(equality)],[481,522]),504]),
[iquote('para(481,522),demod([504])')] ).
cnf(609,plain,
equal(multiply(inverse(multiply(A,B)),A),inverse(B)),
inference(demod,[status(thm),theory(equality)],[inference(demod,[status(thm),theory(equality)],[599]),605]),
[iquote('back_demod(599),demod([605])')] ).
cnf(610,plain,
equal(multiply(multiply(inverse(A),A),B),B),
inference(demod,[status(thm),theory(equality)],[inference(demod,[status(thm),theory(equality)],[604]),609]),
[iquote('back_demod(604),demod([609])')] ).
cnf(611,plain,
$false,
inference(conflict,[status(thm)],[610,2]),
[iquote('conflict(610,2)')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.12 % Problem : GRP434-1 : TPTP v8.1.0. Released v2.6.0.
% 0.12/0.13 % Command : tptp2X_and_run_eqp %s
% 0.13/0.34 % Computer : n015.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 600
% 0.13/0.34 % DateTime : Mon Jun 13 21:54:08 EDT 2022
% 0.13/0.34 % CPUTime :
% 0.82/1.19 ----- EQP 0.9e, May 2009 -----
% 0.82/1.19 The job began on n015.cluster.edu, Mon Jun 13 21:54:09 2022
% 0.82/1.19 The command was "./eqp09e".
% 0.82/1.19
% 0.82/1.19 set(prolog_style_variables).
% 0.82/1.19 set(lrpo).
% 0.82/1.19 set(basic_paramod).
% 0.82/1.19 set(functional_subsume).
% 0.82/1.19 set(ordered_paramod).
% 0.82/1.19 set(prime_paramod).
% 0.82/1.19 set(para_pairs).
% 0.82/1.19 assign(pick_given_ratio,4).
% 0.82/1.19 clear(print_kept).
% 0.82/1.19 clear(print_new_demod).
% 0.82/1.19 clear(print_back_demod).
% 0.82/1.19 clear(print_given).
% 0.82/1.19 assign(max_mem,64000).
% 0.82/1.19 end_of_commands.
% 0.82/1.19
% 0.82/1.19 Usable:
% 0.82/1.19 end_of_list.
% 0.82/1.19
% 0.82/1.19 Sos:
% 0.82/1.19 0 (wt=-1) [] inverse(multiply(multiply(multiply(inverse(multiply(multiply(A,B),C)),A),B),multiply(D,inverse(D)))) = C.
% 0.82/1.19 0 (wt=-1) [] -(multiply(multiply(inverse(b2),b2),a2) = a2).
% 0.82/1.19 end_of_list.
% 0.82/1.19
% 0.82/1.19 Demodulators:
% 0.82/1.19 end_of_list.
% 0.82/1.19
% 0.82/1.19 Passive:
% 0.82/1.19 end_of_list.
% 0.82/1.19
% 0.82/1.19 Starting to process input.
% 0.82/1.19
% 0.82/1.19 ** KEPT: 1 (wt=18) [] inverse(multiply(multiply(multiply(inverse(multiply(multiply(A,B),C)),A),B),multiply(D,inverse(D)))) = C.
% 0.82/1.19 1 is a new demodulator.
% 0.82/1.19
% 0.82/1.19 ** KEPT: 2 (wt=8) [] -(multiply(multiply(inverse(b2),b2),a2) = a2).
% 0.82/1.19 ---------------- PROOF FOUND ----------------
% 0.82/1.19 % SZS status Unsatisfiable
% 0.82/1.19
% 0.82/1.19
% 0.82/1.19 After processing input:
% 0.82/1.19
% 0.82/1.19 Usable:
% 0.82/1.19 end_of_list.
% 0.82/1.19
% 0.82/1.19 Sos:
% 0.82/1.19 2 (wt=8) [] -(multiply(multiply(inverse(b2),b2),a2) = a2).
% 0.82/1.19 1 (wt=18) [] inverse(multiply(multiply(multiply(inverse(multiply(multiply(A,B),C)),A),B),multiply(D,inverse(D)))) = C.
% 0.82/1.19 end_of_list.
% 0.82/1.19
% 0.82/1.19 Demodulators:
% 0.82/1.19 1 (wt=18) [] inverse(multiply(multiply(multiply(inverse(multiply(multiply(A,B),C)),A),B),multiply(D,inverse(D)))) = C.
% 0.82/1.19 end_of_list.
% 0.82/1.19
% 0.82/1.19 Passive:
% 0.82/1.19 end_of_list.
% 0.82/1.19
% 0.82/1.19 UNIT CONFLICT from 610 and 2 at 0.06 seconds.
% 0.82/1.19
% 0.82/1.19 ---------------- PROOF ----------------
% 0.82/1.19 % SZS output start Refutation
% See solution above
% 0.82/1.19 ------------ end of proof -------------
% 0.82/1.19
% 0.82/1.19
% 0.82/1.19 ------------- memory usage ------------
% 0.82/1.19 Memory dynamically allocated (tp_alloc): 1953.
% 0.82/1.19 type (bytes each) gets frees in use avail bytes
% 0.82/1.19 sym_ent ( 96) 56 0 56 0 5.2 K
% 0.82/1.19 term ( 16) 63251 42601 20650 51 401.9 K
% 0.82/1.19 gen_ptr ( 8) 154390 30598 123792 62 967.6 K
% 0.82/1.19 context ( 808) 40370 40368 2 3 3.9 K
% 0.82/1.19 trail ( 12) 5565 5565 0 15 0.2 K
% 0.82/1.19 bt_node ( 68) 5954 5951 3 33 2.4 K
% 0.82/1.19 ac_position (285432) 0 0 0 0 0.0 K
% 0.82/1.19 ac_match_pos (14044) 0 0 0 0 0.0 K
% 0.82/1.19 ac_match_free_vars_pos (4020)
% 0.82/1.19 0 0 0 0 0.0 K
% 0.82/1.19 discrim ( 12) 13261 12090 1171 8118 108.9 K
% 0.82/1.19 flat ( 40) 129961 129961 0 64 2.5 K
% 0.82/1.19 discrim_pos ( 12) 1701 1701 0 1 0.0 K
% 0.82/1.19 fpa_head ( 12) 3305 0 3305 0 38.7 K
% 0.82/1.19 fpa_tree ( 28) 1514 1514 0 15 0.4 K
% 0.82/1.19 fpa_pos ( 36) 839 839 0 1 0.0 K
% 0.82/1.19 literal ( 12) 2759 2149 610 1 7.2 K
% 0.82/1.19 clause ( 24) 2759 2149 610 1 14.3 K
% 0.82/1.19 list ( 12) 288 230 58 9 0.8 K
% 0.82/1.19 list_pos ( 20) 3453 2624 829 1129 38.2 K
% 0.82/1.19 pair_index ( 40) 2 0 2 0 0.1 K
% 0.82/1.19
% 0.82/1.19 -------------- statistics -------------
% 0.82/1.19 Clauses input 2
% 0.82/1.19 Usable input 0
% 0.82/1.19 Sos input 2
% 0.82/1.19 Demodulators input 0
% 0.82/1.19 Passive input 0
% 0.82/1.19
% 0.82/1.19 Processed BS (before search) 2
% 0.82/1.19 Forward subsumed BS 0
% 0.82/1.19 Kept BS 2
% 0.82/1.19 New demodulators BS 1
% 0.82/1.19 Back demodulated BS 0
% 0.82/1.19
% 0.82/1.19 Clauses or pairs given 542
% 0.82/1.19 Clauses generated 1351
% 0.82/1.19 Forward subsumed 743
% 0.82/1.19 Deleted by weight 0
% 0.82/1.19 Deleted by variable count 0
% 0.82/1.19 Kept 608
% 0.82/1.19 New demodulators 228
% 0.82/1.19 Back demodulated 526
% 0.82/1.19 Ordered paramod prunes 0
% 0.82/1.19 Basic paramod prunes 3261
% 0.82/1.19 Prime paramod prunes 0
% 0.82/1.19 Semantic prunes 0
% 0.82/1.19
% 0.82/1.19 Rewrite attmepts 28848
% 0.82/1.19 Rewrites 1181
% 0.82/1.19
% 0.82/1.19 FPA overloads 0
% 0.82/1.19 FPA underloads 0
% 0.82/1.19
% 0.82/1.19 Usable size 0
% 0.82/1.19 Sos size 83
% 0.82/1.19 Demodulators size 28
% 0.82/1.19 Passive size 0
% 0.82/1.19 Disabled size 526
% 0.82/1.19
% 0.82/1.19 Proofs found 1
% 0.82/1.19
% 0.82/1.19 ----------- times (seconds) ----------- Mon Jun 13 21:54:09 2022
% 0.82/1.19
% 0.82/1.19 user CPU time 0.06 (0 hr, 0 min, 0 sec)
% 0.82/1.19 system CPU time 0.03 (0 hr, 0 min, 0 sec)
% 0.82/1.19 wall-clock time 0 (0 hr, 0 min, 0 sec)
% 0.82/1.19 input time 0.00
% 0.82/1.19 paramodulation time 0.00
% 0.82/1.19 demodulation time 0.01
% 0.82/1.19 orient time 0.01
% 0.82/1.19 weigh time 0.00
% 0.82/1.19 forward subsume time 0.00
% 0.82/1.19 back demod find time 0.01
% 0.82/1.19 conflict time 0.00
% 0.82/1.19 LRPO time 0.00
% 0.82/1.19 store clause time 0.02
% 0.82/1.19 disable clause time 0.00
% 0.82/1.19 prime paramod time 0.00
% 0.82/1.19 semantics time 0.00
% 0.82/1.19
% 0.82/1.19 EQP interrupted
%------------------------------------------------------------------------------