%------------------------------------------------------------------------------
% File : Otter---3.3
% Problem : GRP125-3.005 : TPTP v8.1.0. Released v1.2.0.
% Transfm : none
% Format : tptp:raw
% Command : otter-tptp-script %s
% Computer : n013.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 : 300s
% DateTime : Wed Jul 27 12:56:10 EDT 2022
% Result : Unsatisfiable 2.13s 2.37s
% Output : Refutation 2.13s
% Verified :
% SZS Type : Refutation
% Derivation depth : 43
% Number of leaves : 50
% Syntax : Number of clauses : 156 ( 54 unt; 93 nHn; 155 RR)
% Number of literals : 401 ( 0 equ; 51 neg)
% Maximal clause size : 7 ( 2 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 7 ( 6 usr; 1 prp; 0-3 aty)
% Number of functors : 6 ( 6 usr; 6 con; 0-0 aty)
% Number of variables : 39 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(2,axiom,
( ~ group_element(A)
| cycle(A,e_0)
| cycle(A,e_1)
| cycle(A,e_2)
| cycle(A,e_3)
| cycle(A,e_4) ),
file('GRP125-3.005.p',unknown),
[] ).
cnf(3,axiom,
( ~ cycle(A,B)
| ~ cycle(C,D)
| ~ next(A,C)
| ~ greater(B,e_0)
| ~ next(D,E)
| e_qualish(B,E) ),
file('GRP125-3.005.p',unknown),
[] ).
cnf(4,axiom,
( ~ cycle(A,B)
| ~ cycle(C,e_0)
| ~ cycle(D,E)
| ~ next(C,D)
| ~ greater(C,A)
| ~ greater(B,E) ),
file('GRP125-3.005.p',unknown),
[] ).
cnf(5,axiom,
( ~ cycle(A,e_0)
| ~ product(A,e_1,B)
| ~ greater(B,A) ),
file('GRP125-3.005.p',unknown),
[] ).
cnf(6,axiom,
( ~ cycle(A,B)
| ~ product(A,e_1,C)
| ~ greater(B,e_0)
| ~ next(A,D)
| e_qualish(C,D) ),
file('GRP125-3.005.p',unknown),
[] ).
cnf(7,axiom,
~ e_qualish(e_1,e_2),
file('GRP125-3.005.p',unknown),
[] ).
cnf(8,axiom,
~ e_qualish(e_1,e_3),
file('GRP125-3.005.p',unknown),
[] ).
cnf(9,axiom,
~ e_qualish(e_1,e_4),
file('GRP125-3.005.p',unknown),
[] ).
cnf(11,axiom,
~ e_qualish(e_2,e_1),
file('GRP125-3.005.p',unknown),
[] ).
cnf(12,axiom,
~ e_qualish(e_2,e_3),
file('GRP125-3.005.p',unknown),
[] ).
cnf(13,axiom,
~ e_qualish(e_2,e_4),
file('GRP125-3.005.p',unknown),
[] ).
cnf(14,axiom,
~ e_qualish(e_2,e_5),
file('GRP125-3.005.p',unknown),
[] ).
cnf(15,axiom,
~ e_qualish(e_3,e_1),
file('GRP125-3.005.p',unknown),
[] ).
cnf(16,axiom,
~ e_qualish(e_3,e_2),
file('GRP125-3.005.p',unknown),
[] ).
cnf(17,axiom,
~ e_qualish(e_3,e_4),
file('GRP125-3.005.p',unknown),
[] ).
cnf(19,axiom,
~ e_qualish(e_4,e_1),
file('GRP125-3.005.p',unknown),
[] ).
cnf(20,axiom,
~ e_qualish(e_4,e_2),
file('GRP125-3.005.p',unknown),
[] ).
cnf(21,axiom,
~ e_qualish(e_4,e_3),
file('GRP125-3.005.p',unknown),
[] ).
cnf(22,axiom,
~ e_qualish(e_4,e_5),
file('GRP125-3.005.p',unknown),
[] ).
cnf(23,axiom,
~ e_qualish(e_5,e_1),
file('GRP125-3.005.p',unknown),
[] ).
cnf(24,axiom,
~ e_qualish(e_5,e_2),
file('GRP125-3.005.p',unknown),
[] ).
cnf(25,axiom,
~ e_qualish(e_5,e_3),
file('GRP125-3.005.p',unknown),
[] ).
cnf(26,axiom,
~ e_qualish(e_5,e_4),
file('GRP125-3.005.p',unknown),
[] ).
cnf(27,axiom,
( ~ group_element(A)
| ~ group_element(B)
| product(A,B,e_1)
| product(A,B,e_2)
| product(A,B,e_3)
| product(A,B,e_4)
| product(A,B,e_5) ),
file('GRP125-3.005.p',unknown),
[] ).
cnf(28,axiom,
( ~ product(A,B,C)
| ~ product(A,B,D)
| e_qualish(C,D) ),
file('GRP125-3.005.p',unknown),
[] ).
cnf(29,axiom,
( ~ product(A,B,C)
| ~ product(A,D,C)
| e_qualish(B,D) ),
file('GRP125-3.005.p',unknown),
[] ).
cnf(30,axiom,
( ~ product(A,B,C)
| ~ product(D,B,C)
| e_qualish(A,D) ),
file('GRP125-3.005.p',unknown),
[] ).
cnf(31,axiom,
( ~ product(A,B,C)
| ~ product(B,A,D)
| product(C,D,A) ),
file('GRP125-3.005.p',unknown),
[] ).
cnf(34,plain,
( ~ cycle(A,B)
| ~ cycle(C,A)
| ~ next(A,C)
| ~ greater(B,e_0)
| e_qualish(B,C) ),
inference(factor,[status(thm)],[3]),
[iquote('factor,3.3.5')] ).
cnf(49,axiom,
next(e_0,e_1),
file('GRP125-3.005.p',unknown),
[] ).
cnf(50,axiom,
next(e_1,e_2),
file('GRP125-3.005.p',unknown),
[] ).
cnf(51,axiom,
next(e_2,e_3),
file('GRP125-3.005.p',unknown),
[] ).
cnf(52,axiom,
next(e_3,e_4),
file('GRP125-3.005.p',unknown),
[] ).
cnf(53,axiom,
next(e_4,e_5),
file('GRP125-3.005.p',unknown),
[] ).
cnf(54,axiom,
greater(e_1,e_0),
file('GRP125-3.005.p',unknown),
[] ).
cnf(55,axiom,
greater(e_2,e_0),
file('GRP125-3.005.p',unknown),
[] ).
cnf(56,axiom,
greater(e_3,e_0),
file('GRP125-3.005.p',unknown),
[] ).
cnf(57,axiom,
greater(e_4,e_0),
file('GRP125-3.005.p',unknown),
[] ).
cnf(59,axiom,
greater(e_2,e_1),
file('GRP125-3.005.p',unknown),
[] ).
cnf(60,axiom,
greater(e_3,e_1),
file('GRP125-3.005.p',unknown),
[] ).
cnf(63,axiom,
greater(e_3,e_2),
file('GRP125-3.005.p',unknown),
[] ).
cnf(64,axiom,
greater(e_4,e_2),
file('GRP125-3.005.p',unknown),
[] ).
cnf(65,axiom,
greater(e_5,e_2),
file('GRP125-3.005.p',unknown),
[] ).
cnf(66,axiom,
greater(e_4,e_3),
file('GRP125-3.005.p',unknown),
[] ).
cnf(67,axiom,
greater(e_5,e_3),
file('GRP125-3.005.p',unknown),
[] ).
cnf(69,axiom,
cycle(e_5,e_0),
file('GRP125-3.005.p',unknown),
[] ).
cnf(70,axiom,
group_element(e_1),
file('GRP125-3.005.p',unknown),
[] ).
cnf(71,axiom,
group_element(e_2),
file('GRP125-3.005.p',unknown),
[] ).
cnf(72,axiom,
group_element(e_3),
file('GRP125-3.005.p',unknown),
[] ).
cnf(73,axiom,
group_element(e_4),
file('GRP125-3.005.p',unknown),
[] ).
cnf(75,axiom,
product(A,A,A),
file('GRP125-3.005.p',unknown),
[] ).
cnf(77,plain,
( product(e_1,e_2,e_1)
| product(e_1,e_2,e_2)
| product(e_1,e_2,e_3)
| product(e_1,e_2,e_4)
| product(e_1,e_2,e_5) ),
inference(hyper,[status(thm)],[71,27,70]),
[iquote('hyper,71,27,70')] ).
cnf(78,plain,
( product(e_2,e_1,e_1)
| product(e_2,e_1,e_2)
| product(e_2,e_1,e_3)
| product(e_2,e_1,e_4)
| product(e_2,e_1,e_5) ),
inference(hyper,[status(thm)],[71,27,70]),
[iquote('hyper,71,27,70')] ).
cnf(79,plain,
( cycle(e_2,e_0)
| cycle(e_2,e_1)
| cycle(e_2,e_2)
| cycle(e_2,e_3)
| cycle(e_2,e_4) ),
inference(hyper,[status(thm)],[71,2]),
[iquote('hyper,71,2')] ).
cnf(80,plain,
( product(e_2,e_3,e_1)
| product(e_2,e_3,e_2)
| product(e_2,e_3,e_3)
| product(e_2,e_3,e_4)
| product(e_2,e_3,e_5) ),
inference(hyper,[status(thm)],[72,27,71]),
[iquote('hyper,72,27,71')] ).
cnf(81,plain,
( product(e_1,e_3,e_1)
| product(e_1,e_3,e_2)
| product(e_1,e_3,e_3)
| product(e_1,e_3,e_4)
| product(e_1,e_3,e_5) ),
inference(hyper,[status(thm)],[72,27,70]),
[iquote('hyper,72,27,70')] ).
cnf(82,plain,
( product(e_3,e_2,e_1)
| product(e_3,e_2,e_2)
| product(e_3,e_2,e_3)
| product(e_3,e_2,e_4)
| product(e_3,e_2,e_5) ),
inference(hyper,[status(thm)],[72,27,71]),
[iquote('hyper,72,27,71')] ).
cnf(83,plain,
( product(e_3,e_1,e_1)
| product(e_3,e_1,e_2)
| product(e_3,e_1,e_3)
| product(e_3,e_1,e_4)
| product(e_3,e_1,e_5) ),
inference(hyper,[status(thm)],[72,27,70]),
[iquote('hyper,72,27,70')] ).
cnf(84,plain,
( cycle(e_3,e_0)
| cycle(e_3,e_1)
| cycle(e_3,e_2)
| cycle(e_3,e_3)
| cycle(e_3,e_4) ),
inference(hyper,[status(thm)],[72,2]),
[iquote('hyper,72,2')] ).
cnf(85,plain,
( product(e_3,e_4,e_1)
| product(e_3,e_4,e_2)
| product(e_3,e_4,e_3)
| product(e_3,e_4,e_4)
| product(e_3,e_4,e_5) ),
inference(hyper,[status(thm)],[73,27,72]),
[iquote('hyper,73,27,72')] ).
cnf(86,plain,
( product(e_2,e_4,e_1)
| product(e_2,e_4,e_2)
| product(e_2,e_4,e_3)
| product(e_2,e_4,e_4)
| product(e_2,e_4,e_5) ),
inference(hyper,[status(thm)],[73,27,71]),
[iquote('hyper,73,27,71')] ).
cnf(87,plain,
( product(e_1,e_4,e_1)
| product(e_1,e_4,e_2)
| product(e_1,e_4,e_3)
| product(e_1,e_4,e_4)
| product(e_1,e_4,e_5) ),
inference(hyper,[status(thm)],[73,27,70]),
[iquote('hyper,73,27,70')] ).
cnf(88,plain,
( product(e_4,e_3,e_1)
| product(e_4,e_3,e_2)
| product(e_4,e_3,e_3)
| product(e_4,e_3,e_4)
| product(e_4,e_3,e_5) ),
inference(hyper,[status(thm)],[73,27,72]),
[iquote('hyper,73,27,72')] ).
cnf(90,plain,
( product(e_4,e_1,e_1)
| product(e_4,e_1,e_2)
| product(e_4,e_1,e_3)
| product(e_4,e_1,e_4)
| product(e_4,e_1,e_5) ),
inference(hyper,[status(thm)],[73,27,70]),
[iquote('hyper,73,27,70')] ).
cnf(91,plain,
( cycle(e_4,e_0)
| cycle(e_4,e_1)
| cycle(e_4,e_2)
| cycle(e_4,e_3)
| cycle(e_4,e_4) ),
inference(hyper,[status(thm)],[73,2]),
[iquote('hyper,73,2')] ).
cnf(106,plain,
( product(e_1,e_2,e_2)
| product(e_1,e_2,e_3)
| product(e_1,e_2,e_4)
| product(e_1,e_2,e_5) ),
inference(unit_del,[status(thm)],[inference(hyper,[status(thm)],[77,29,75]),7]),
[iquote('hyper,77,29,75,unit_del,7')] ).
cnf(114,plain,
( product(e_2,e_1,e_2)
| product(e_2,e_1,e_3)
| product(e_2,e_1,e_4)
| product(e_2,e_1,e_5) ),
inference(unit_del,[status(thm)],[inference(hyper,[status(thm)],[78,30,75]),7]),
[iquote('hyper,78,30,75,unit_del,7')] ).
cnf(147,plain,
( cycle(e_4,e_0)
| cycle(e_4,e_1)
| cycle(e_4,e_3)
| cycle(e_4,e_4) ),
inference(unit_del,[status(thm)],[inference(hyper,[status(thm)],[91,3,69,53,55,49]),11]),
[iquote('hyper,91,3,69,53,55,49,unit_del,11')] ).
cnf(172,plain,
( cycle(e_4,e_0)
| cycle(e_4,e_1)
| cycle(e_4,e_4) ),
inference(unit_del,[status(thm)],[inference(hyper,[status(thm)],[147,3,69,53,56,49]),15]),
[iquote('hyper,147,3,69,53,56,49,unit_del,15')] ).
cnf(178,plain,
( product(e_2,e_3,e_1)
| product(e_2,e_3,e_3)
| product(e_2,e_3,e_4)
| product(e_2,e_3,e_5) ),
inference(unit_del,[status(thm)],[inference(hyper,[status(thm)],[80,29,75]),12]),
[iquote('hyper,80,29,75,unit_del,12')] ).
cnf(196,plain,
( cycle(e_4,e_0)
| cycle(e_4,e_1) ),
inference(unit_del,[status(thm)],[inference(hyper,[status(thm)],[172,3,69,53,57,49]),19]),
[iquote('hyper,172,3,69,53,57,49,unit_del,19')] ).
cnf(198,plain,
( cycle(e_4,e_1)
| cycle(e_3,e_0)
| cycle(e_3,e_1)
| cycle(e_3,e_2)
| cycle(e_3,e_3) ),
inference(hyper,[status(thm)],[196,4,84,69,53,66,57]),
[iquote('hyper,196,4,84,69,53,66,57')] ).
cnf(202,plain,
( cycle(e_4,e_1)
| cycle(e_2,e_0)
| cycle(e_2,e_1)
| cycle(e_2,e_2)
| cycle(e_2,e_3) ),
inference(hyper,[status(thm)],[196,4,79,69,53,64,57]),
[iquote('hyper,196,4,79,69,53,64,57')] ).
cnf(209,plain,
( cycle(e_3,e_0)
| cycle(e_3,e_1)
| cycle(e_3,e_2)
| cycle(e_3,e_3) ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(unit_del,[status(thm)],[inference(hyper,[status(thm)],[198,3,84,52,57,50]),20])])])])]),
[iquote('hyper,198,3,84,52,57,50,unit_del,20,factor_simp,factor_simp,factor_simp,factor_simp')] ).
cnf(210,plain,
( cycle(e_4,e_1)
| cycle(e_3,e_0)
| cycle(e_3,e_2)
| cycle(e_3,e_3) ),
inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[198,4,196,69,53,66,54])]),
[iquote('hyper,198,4,196,69,53,66,54,factor_simp')] ).
cnf(230,plain,
( product(e_1,e_3,e_2)
| product(e_1,e_3,e_3)
| product(e_1,e_3,e_4)
| product(e_1,e_3,e_5) ),
inference(unit_del,[status(thm)],[inference(hyper,[status(thm)],[81,29,75]),8]),
[iquote('hyper,81,29,75,unit_del,8')] ).
cnf(232,plain,
( cycle(e_3,e_0)
| cycle(e_3,e_2)
| cycle(e_3,e_3) ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(unit_del,[status(thm)],[inference(hyper,[status(thm)],[210,3,209,52,54,50]),7])])])]),
[iquote('hyper,210,3,209,52,54,50,unit_del,7,factor_simp,factor_simp,factor_simp')] ).
cnf(233,plain,
( cycle(e_4,e_1)
| cycle(e_3,e_0)
| cycle(e_3,e_3) ),
inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[210,4,196,69,53,66,55])]),
[iquote('hyper,210,4,196,69,53,66,55,factor_simp')] ).
cnf(248,plain,
( cycle(e_4,e_1)
| cycle(e_3,e_0) ),
inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[233,4,196,69,53,66,56])]),
[iquote('hyper,233,4,196,69,53,66,56,factor_simp')] ).
cnf(249,plain,
( cycle(e_3,e_0)
| cycle(e_3,e_2) ),
inference(factor_simp,[status(thm)],[inference(unit_del,[status(thm)],[inference(hyper,[status(thm)],[248,3,232,52,56,50]),16])]),
[iquote('hyper,248,3,232,52,56,50,unit_del,16,factor_simp')] ).
cnf(250,plain,
( product(e_3,e_2,e_1)
| product(e_3,e_2,e_3)
| product(e_3,e_2,e_4)
| product(e_3,e_2,e_5) ),
inference(unit_del,[status(thm)],[inference(hyper,[status(thm)],[82,30,75]),12]),
[iquote('hyper,82,30,75,unit_del,12')] ).
cnf(255,plain,
( cycle(e_3,e_2)
| cycle(e_2,e_0)
| cycle(e_2,e_1)
| cycle(e_2,e_2)
| cycle(e_2,e_3) ),
inference(unit_del,[status(thm)],[inference(hyper,[status(thm)],[249,3,79,51,57,49]),19]),
[iquote('hyper,249,3,79,51,57,49,unit_del,19')] ).
cnf(262,plain,
( cycle(e_4,e_1)
| cycle(e_2,e_0)
| cycle(e_2,e_2)
| cycle(e_2,e_3) ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[202,4,248,196,52,63,54])])]),
[iquote('hyper,202,4,248,196,52,63,54,factor_simp,factor_simp')] ).
cnf(268,plain,
( cycle(e_4,e_1)
| cycle(e_2,e_0)
| cycle(e_2,e_3) ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[262,4,248,196,52,63,55])])]),
[iquote('hyper,262,4,248,196,52,63,55,factor_simp,factor_simp')] ).
cnf(272,plain,
( cycle(e_4,e_1)
| cycle(e_2,e_0) ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[268,4,248,196,52,63,56])])]),
[iquote('hyper,268,4,248,196,52,63,56,factor_simp,factor_simp')] ).
cnf(273,plain,
( product(e_3,e_1,e_2)
| product(e_3,e_1,e_3)
| product(e_3,e_1,e_4)
| product(e_3,e_1,e_5) ),
inference(unit_del,[status(thm)],[inference(hyper,[status(thm)],[83,30,75]),8]),
[iquote('hyper,83,30,75,unit_del,8')] ).
cnf(281,plain,
( cycle(e_2,e_0)
| cycle(e_2,e_1)
| cycle(e_2,e_2)
| cycle(e_2,e_3) ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(unit_del,[status(thm)],[inference(hyper,[status(thm)],[255,34,79,51,57]),21])])])])]),
[iquote('hyper,255,34,79,51,57,unit_del,21,factor_simp,factor_simp,factor_simp,factor_simp')] ).
cnf(282,plain,
( cycle(e_3,e_2)
| cycle(e_2,e_0)
| cycle(e_2,e_1)
| cycle(e_2,e_3) ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[255,4,249,272,52,63,59])])]),
[iquote('hyper,255,4,249,272,52,63,59,factor_simp,factor_simp')] ).
cnf(286,plain,
( cycle(e_2,e_0)
| cycle(e_2,e_1)
| cycle(e_2,e_3) ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(unit_del,[status(thm)],[inference(hyper,[status(thm)],[282,34,281,51,55]),12])])])]),
[iquote('hyper,282,34,281,51,55,unit_del,12,factor_simp,factor_simp,factor_simp')] ).
cnf(287,plain,
( cycle(e_3,e_2)
| cycle(e_2,e_0)
| cycle(e_2,e_1) ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[282,4,249,272,52,63,60])])]),
[iquote('hyper,282,4,249,272,52,63,60,factor_simp,factor_simp')] ).
cnf(288,plain,
( product(e_3,e_4,e_1)
| product(e_3,e_4,e_2)
| product(e_3,e_4,e_4)
| product(e_3,e_4,e_5) ),
inference(unit_del,[status(thm)],[inference(hyper,[status(thm)],[85,29,75]),17]),
[iquote('hyper,85,29,75,unit_del,17')] ).
cnf(291,plain,
( product(e_1,e_2,e_3)
| product(e_1,e_2,e_4)
| product(e_1,e_2,e_5) ),
inference(unit_del,[status(thm)],[inference(hyper,[status(thm)],[106,30,75]),11]),
[iquote('hyper,106,30,75,unit_del,11')] ).
cnf(292,plain,
( product(e_2,e_4,e_1)
| product(e_2,e_4,e_3)
| product(e_2,e_4,e_4)
| product(e_2,e_4,e_5) ),
inference(unit_del,[status(thm)],[inference(hyper,[status(thm)],[86,29,75]),13]),
[iquote('hyper,86,29,75,unit_del,13')] ).
cnf(300,plain,
( product(e_2,e_1,e_3)
| product(e_2,e_1,e_4)
| product(e_2,e_1,e_5) ),
inference(unit_del,[status(thm)],[inference(hyper,[status(thm)],[114,29,75]),11]),
[iquote('hyper,114,29,75,unit_del,11')] ).
cnf(356,plain,
( product(e_2,e_1,e_3)
| product(e_2,e_1,e_5)
| cycle(e_3,e_2)
| cycle(e_2,e_0) ),
inference(unit_del,[status(thm)],[inference(hyper,[status(thm)],[300,6,287,54,51]),21]),
[iquote('hyper,300,6,287,54,51,unit_del,21')] ).
cnf(357,plain,
( product(e_2,e_1,e_3)
| product(e_2,e_1,e_5)
| cycle(e_2,e_0)
| cycle(e_2,e_1) ),
inference(unit_del,[status(thm)],[inference(hyper,[status(thm)],[300,6,286,56,51]),21]),
[iquote('hyper,300,6,286,56,51,unit_del,21')] ).
cnf(377,plain,
( product(e_1,e_4,e_2)
| product(e_1,e_4,e_3)
| product(e_1,e_4,e_4)
| product(e_1,e_4,e_5) ),
inference(unit_del,[status(thm)],[inference(hyper,[status(thm)],[87,29,75]),9]),
[iquote('hyper,87,29,75,unit_del,9')] ).
cnf(381,plain,
( product(e_4,e_3,e_1)
| product(e_4,e_3,e_2)
| product(e_4,e_3,e_4)
| product(e_4,e_3,e_5) ),
inference(unit_del,[status(thm)],[inference(hyper,[status(thm)],[88,30,75]),17]),
[iquote('hyper,88,30,75,unit_del,17')] ).
cnf(386,plain,
( product(e_2,e_1,e_3)
| product(e_2,e_1,e_5)
| cycle(e_3,e_2) ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[356,5,300,64])])]),
[iquote('hyper,356,5,300,64,factor_simp,factor_simp')] ).
cnf(394,plain,
( product(e_2,e_1,e_3)
| product(e_2,e_1,e_5)
| cycle(e_2,e_1) ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[357,5,300,64])])]),
[iquote('hyper,357,5,300,64,factor_simp,factor_simp')] ).
cnf(396,plain,
( product(e_4,e_1,e_2)
| product(e_4,e_1,e_3)
| product(e_4,e_1,e_4)
| product(e_4,e_1,e_5) ),
inference(unit_del,[status(thm)],[inference(hyper,[status(thm)],[90,30,75]),9]),
[iquote('hyper,90,30,75,unit_del,9')] ).
cnf(413,plain,
( product(e_2,e_1,e_3)
| product(e_2,e_1,e_5) ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(unit_del,[status(thm)],[inference(hyper,[status(thm)],[394,34,386,51,54]),8])])]),
[iquote('hyper,394,34,386,51,54,unit_del,8,factor_simp,factor_simp')] ).
cnf(431,plain,
( product(e_2,e_1,e_3)
| cycle(e_3,e_2)
| cycle(e_2,e_0) ),
inference(unit_del,[status(thm)],[inference(hyper,[status(thm)],[413,6,287,54,51]),25]),
[iquote('hyper,413,6,287,54,51,unit_del,25')] ).
cnf(432,plain,
( product(e_2,e_1,e_3)
| cycle(e_2,e_0)
| cycle(e_2,e_1) ),
inference(unit_del,[status(thm)],[inference(hyper,[status(thm)],[413,6,286,56,51]),25]),
[iquote('hyper,413,6,286,56,51,unit_del,25')] ).
cnf(445,plain,
( product(e_2,e_1,e_3)
| cycle(e_3,e_2) ),
inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[431,5,413,65])]),
[iquote('hyper,431,5,413,65,factor_simp')] ).
cnf(451,plain,
( product(e_2,e_1,e_3)
| cycle(e_2,e_1) ),
inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[432,5,413,65])]),
[iquote('hyper,432,5,413,65,factor_simp')] ).
cnf(453,plain,
product(e_2,e_1,e_3),
inference(factor_simp,[status(thm)],[inference(unit_del,[status(thm)],[inference(hyper,[status(thm)],[451,34,445,51,54]),8])]),
[iquote('hyper,451,34,445,51,54,unit_del,8,factor_simp')] ).
cnf(456,plain,
( product(e_3,e_3,e_1)
| product(e_1,e_2,e_4)
| product(e_1,e_2,e_5) ),
inference(hyper,[status(thm)],[453,31,291]),
[iquote('hyper,453,31,291')] ).
cnf(463,plain,
cycle(e_4,e_1),
inference(hyper,[status(thm)],[453,5,272,63]),
[iquote('hyper,453,5,272,63')] ).
cnf(480,plain,
( product(e_1,e_2,e_4)
| product(e_1,e_2,e_5) ),
inference(unit_del,[status(thm)],[inference(hyper,[status(thm)],[456,28,75]),15]),
[iquote('hyper,456,28,75,unit_del,15')] ).
cnf(483,plain,
( product(e_1,e_2,e_5)
| product(e_3,e_4,e_2) ),
inference(hyper,[status(thm)],[480,31,453]),
[iquote('hyper,480,31,453')] ).
cnf(484,plain,
( product(e_1,e_2,e_5)
| product(e_4,e_3,e_1) ),
inference(hyper,[status(thm)],[480,31,453]),
[iquote('hyper,480,31,453')] ).
cnf(490,plain,
( product(e_3,e_4,e_2)
| product(e_5,e_3,e_1) ),
inference(hyper,[status(thm)],[483,31,453]),
[iquote('hyper,483,31,453')] ).
cnf(491,plain,
( product(e_4,e_3,e_1)
| product(e_3,e_5,e_2) ),
inference(hyper,[status(thm)],[484,31,453]),
[iquote('hyper,484,31,453')] ).
cnf(492,plain,
( product(e_4,e_3,e_1)
| product(e_5,e_3,e_1) ),
inference(hyper,[status(thm)],[484,31,453]),
[iquote('hyper,484,31,453')] ).
cnf(511,plain,
( product(e_2,e_3,e_1)
| product(e_2,e_3,e_4)
| product(e_2,e_3,e_5) ),
inference(unit_del,[status(thm)],[inference(hyper,[status(thm)],[178,30,75]),16]),
[iquote('hyper,178,30,75,unit_del,16')] ).
cnf(512,plain,
( product(e_2,e_3,e_4)
| product(e_2,e_3,e_5)
| product(e_4,e_3,e_1) ),
inference(unit_del,[status(thm)],[inference(hyper,[status(thm)],[511,30,492]),24]),
[iquote('hyper,511,30,492,unit_del,24')] ).
cnf(518,plain,
( product(e_2,e_3,e_4)
| product(e_2,e_3,e_5) ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(unit_del,[status(thm)],[inference(hyper,[status(thm)],[512,30,511]),13])])]),
[iquote('hyper,512,30,511,unit_del,13,factor_simp,factor_simp')] ).
cnf(519,plain,
( product(e_1,e_3,e_2)
| product(e_1,e_3,e_4)
| product(e_1,e_3,e_5) ),
inference(unit_del,[status(thm)],[inference(hyper,[status(thm)],[230,30,75]),15]),
[iquote('hyper,230,30,75,unit_del,15')] ).
cnf(533,plain,
( product(e_1,e_3,e_2)
| product(e_1,e_3,e_4)
| product(e_4,e_3,e_1) ),
inference(unit_del,[status(thm)],[inference(hyper,[status(thm)],[519,29,484]),12]),
[iquote('hyper,519,29,484,unit_del,12')] ).
cnf(553,plain,
( product(e_3,e_2,e_1)
| product(e_3,e_2,e_4)
| product(e_3,e_2,e_5) ),
inference(unit_del,[status(thm)],[inference(hyper,[status(thm)],[250,29,75]),16]),
[iquote('hyper,250,29,75,unit_del,16')] ).
cnf(645,plain,
( product(e_3,e_1,e_2)
| product(e_3,e_1,e_4)
| product(e_3,e_1,e_5) ),
inference(unit_del,[status(thm)],[inference(hyper,[status(thm)],[273,30,453]),12]),
[iquote('hyper,273,30,453,unit_del,12')] ).
cnf(723,plain,
( product(e_3,e_4,e_1)
| product(e_3,e_4,e_2)
| product(e_3,e_4,e_5) ),
inference(unit_del,[status(thm)],[inference(hyper,[status(thm)],[288,30,75]),21]),
[iquote('hyper,288,30,75,unit_del,21')] ).
cnf(792,plain,
( product(e_2,e_4,e_1)
| product(e_2,e_4,e_4)
| product(e_2,e_4,e_5) ),
inference(unit_del,[status(thm)],[inference(hyper,[status(thm)],[292,29,453]),9]),
[iquote('hyper,292,29,453,unit_del,9')] ).
cnf(966,plain,
( product(e_3,e_1,e_2)
| product(e_3,e_1,e_4)
| cycle(e_3,e_0) ),
inference(unit_del,[status(thm)],[inference(hyper,[status(thm)],[645,6,249,55,52]),26]),
[iquote('hyper,645,6,249,55,52,unit_del,26')] ).
cnf(983,plain,
( product(e_1,e_4,e_2)
| product(e_1,e_4,e_3)
| product(e_1,e_4,e_5) ),
inference(unit_del,[status(thm)],[inference(hyper,[status(thm)],[377,30,75]),19]),
[iquote('hyper,377,30,75,unit_del,19')] ).
cnf(994,plain,
( product(e_3,e_1,e_2)
| product(e_3,e_1,e_4) ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[966,5,645,67])])]),
[iquote('hyper,966,5,645,67,factor_simp,factor_simp')] ).
cnf(1049,plain,
( product(e_3,e_1,e_4)
| product(e_4,e_3,e_1) ),
inference(unit_del,[status(thm)],[inference(hyper,[status(thm)],[994,29,491]),23]),
[iquote('hyper,994,29,491,unit_del,23')] ).
cnf(1050,plain,
( product(e_3,e_1,e_4)
| product(e_5,e_3,e_1) ),
inference(unit_del,[status(thm)],[inference(hyper,[status(thm)],[994,29,490]),19]),
[iquote('hyper,994,29,490,unit_del,19')] ).
cnf(1124,plain,
( product(e_4,e_3,e_1)
| product(e_4,e_3,e_2)
| product(e_4,e_3,e_5) ),
inference(unit_del,[status(thm)],[inference(hyper,[status(thm)],[381,29,75]),21]),
[iquote('hyper,381,29,75,unit_del,21')] ).
cnf(1155,plain,
( product(e_4,e_3,e_1)
| product(e_4,e_4,e_1)
| product(e_1,e_3,e_2) ),
inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[1049,31,533])]),
[iquote('hyper,1049,31,533,factor_simp')] ).
cnf(1189,plain,
product(e_3,e_1,e_4),
inference(factor_simp,[status(thm)],[inference(unit_del,[status(thm)],[inference(hyper,[status(thm)],[1050,30,1049]),22])]),
[iquote('hyper,1050,30,1049,unit_del,22,factor_simp')] ).
cnf(1190,plain,
( product(e_4,e_1,e_3)
| product(e_4,e_1,e_4)
| product(e_4,e_1,e_5) ),
inference(unit_del,[status(thm)],[inference(hyper,[status(thm)],[396,6,463,54,53]),14]),
[iquote('hyper,396,6,463,54,53,unit_del,14')] ).
cnf(1231,plain,
( product(e_3,e_2,e_1)
| product(e_3,e_2,e_5) ),
inference(unit_del,[status(thm)],[inference(hyper,[status(thm)],[1189,29,553]),11]),
[iquote('hyper,1189,29,553,unit_del,11')] ).
cnf(1277,plain,
( product(e_3,e_2,e_1)
| product(e_3,e_4,e_2) ),
inference(unit_del,[status(thm)],[inference(hyper,[status(thm)],[1231,30,483]),8]),
[iquote('hyper,1231,30,483,unit_del,8')] ).
cnf(1313,plain,
( product(e_3,e_4,e_2)
| product(e_3,e_4,e_5) ),
inference(factor_simp,[status(thm)],[inference(unit_del,[status(thm)],[inference(hyper,[status(thm)],[723,29,1277]),13])]),
[iquote('hyper,723,29,1277,unit_del,13,factor_simp')] ).
cnf(1328,plain,
( product(e_3,e_4,e_5)
| product(e_4,e_3,e_1) ),
inference(unit_del,[status(thm)],[inference(hyper,[status(thm)],[1313,29,491]),26]),
[iquote('hyper,1313,29,491,unit_del,26')] ).
cnf(1330,plain,
( product(e_2,e_4,e_1)
| product(e_2,e_4,e_5) ),
inference(unit_del,[status(thm)],[inference(hyper,[status(thm)],[792,30,75]),20]),
[iquote('hyper,792,30,75,unit_del,20')] ).
cnf(1344,plain,
( product(e_2,e_4,e_1)
| product(e_4,e_3,e_1) ),
inference(unit_del,[status(thm)],[inference(hyper,[status(thm)],[1330,30,1328]),16]),
[iquote('hyper,1330,30,1328,unit_del,16')] ).
cnf(1504,plain,
( product(e_4,e_3,e_1)
| product(e_1,e_3,e_2) ),
inference(factor_simp,[status(thm)],[inference(unit_del,[status(thm)],[inference(hyper,[status(thm)],[1155,30,1344]),13])]),
[iquote('hyper,1155,30,1344,unit_del,13,factor_simp')] ).
cnf(1518,plain,
( product(e_4,e_3,e_1)
| product(e_4,e_3,e_5) ),
inference(factor_simp,[status(thm)],[inference(unit_del,[status(thm)],[inference(hyper,[status(thm)],[1504,30,1124]),19])]),
[iquote('hyper,1504,30,1124,unit_del,19,factor_simp')] ).
cnf(1559,plain,
( product(e_4,e_3,e_1)
| product(e_5,e_5,e_3) ),
inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[1518,31,1328])]),
[iquote('hyper,1518,31,1328,factor_simp')] ).
cnf(1624,plain,
product(e_4,e_3,e_1),
inference(unit_del,[status(thm)],[inference(hyper,[status(thm)],[1559,28,75]),25]),
[iquote('hyper,1559,28,75,unit_del,25')] ).
cnf(1629,plain,
product(e_3,e_4,e_2),
inference(unit_del,[status(thm)],[inference(hyper,[status(thm)],[1624,30,490]),26]),
[iquote('hyper,1624,30,490,unit_del,26')] ).
cnf(1637,plain,
( product(e_4,e_1,e_4)
| product(e_4,e_1,e_5) ),
inference(unit_del,[status(thm)],[inference(hyper,[status(thm)],[1190,30,453]),13]),
[iquote('hyper,1190,30,453,unit_del,13')] ).
cnf(1651,plain,
( product(e_1,e_4,e_3)
| product(e_1,e_4,e_5) ),
inference(unit_del,[status(thm)],[inference(hyper,[status(thm)],[1629,30,983]),8]),
[iquote('hyper,1629,30,983,unit_del,8')] ).
cnf(1680,plain,
product(e_4,e_1,e_5),
inference(unit_del,[status(thm)],[inference(hyper,[status(thm)],[1637,30,1189]),17]),
[iquote('hyper,1637,30,1189,unit_del,17')] ).
cnf(1692,plain,
( product(e_1,e_4,e_3)
| product(e_5,e_5,e_4) ),
inference(hyper,[status(thm)],[1651,31,1680]),
[iquote('hyper,1651,31,1680')] ).
cnf(1713,plain,
product(e_1,e_4,e_3),
inference(unit_del,[status(thm)],[inference(hyper,[status(thm)],[1692,28,75]),26]),
[iquote('hyper,1692,28,75,unit_del,26')] ).
cnf(1714,plain,
product(e_5,e_3,e_4),
inference(hyper,[status(thm)],[1713,31,1680]),
[iquote('hyper,1713,31,1680')] ).
cnf(1715,plain,
product(e_3,e_5,e_1),
inference(hyper,[status(thm)],[1713,31,1680]),
[iquote('hyper,1713,31,1680')] ).
cnf(1719,plain,
product(e_2,e_3,e_5),
inference(unit_del,[status(thm)],[inference(hyper,[status(thm)],[1714,30,518]),14]),
[iquote('hyper,1714,30,518,unit_del,14')] ).
cnf(1720,plain,
product(e_3,e_2,e_5),
inference(unit_del,[status(thm)],[inference(hyper,[status(thm)],[1715,29,1231]),14]),
[iquote('hyper,1715,29,1231,unit_del,14')] ).
cnf(1721,plain,
product(e_5,e_5,e_2),
inference(hyper,[status(thm)],[1720,31,1719]),
[iquote('hyper,1720,31,1719')] ).
cnf(1728,plain,
e_qualish(e_5,e_2),
inference(hyper,[status(thm)],[1721,28,75]),
[iquote('hyper,1721,28,75')] ).
cnf(1729,plain,
$false,
inference(binary,[status(thm)],[1728,24]),
[iquote('binary,1728.1,24.1')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : GRP125-3.005 : TPTP v8.1.0. Released v1.2.0.
% 0.12/0.12 % Command : otter-tptp-script %s
% 0.12/0.33 % Computer : n013.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Wed Jul 27 05:04:45 EDT 2022
% 0.12/0.33 % CPUTime :
% 1.84/2.08 ----- Otter 3.3f, August 2004 -----
% 1.84/2.08 The process was started by sandbox2 on n013.cluster.edu,
% 1.84/2.08 Wed Jul 27 05:04:45 2022
% 1.84/2.08 The command was "./otter". The process ID is 21527.
% 1.84/2.08
% 1.84/2.08 set(prolog_style_variables).
% 1.84/2.08 set(auto).
% 1.84/2.08 dependent: set(auto1).
% 1.84/2.08 dependent: set(process_input).
% 1.84/2.08 dependent: clear(print_kept).
% 1.84/2.08 dependent: clear(print_new_demod).
% 1.84/2.08 dependent: clear(print_back_demod).
% 1.84/2.08 dependent: clear(print_back_sub).
% 1.84/2.08 dependent: set(control_memory).
% 1.84/2.08 dependent: assign(max_mem, 12000).
% 1.84/2.08 dependent: assign(pick_given_ratio, 4).
% 1.84/2.08 dependent: assign(stats_level, 1).
% 1.84/2.08 dependent: assign(max_seconds, 10800).
% 1.84/2.08 clear(print_given).
% 1.84/2.08
% 1.84/2.08 list(usable).
% 1.84/2.08 0 [] next(e_0,e_1).
% 1.84/2.08 0 [] next(e_1,e_2).
% 1.84/2.08 0 [] next(e_2,e_3).
% 1.84/2.08 0 [] next(e_3,e_4).
% 1.84/2.08 0 [] next(e_4,e_5).
% 1.84/2.08 0 [] greater(e_1,e_0).
% 1.84/2.08 0 [] greater(e_2,e_0).
% 1.84/2.08 0 [] greater(e_3,e_0).
% 1.84/2.08 0 [] greater(e_4,e_0).
% 1.84/2.08 0 [] greater(e_5,e_0).
% 1.84/2.08 0 [] greater(e_2,e_1).
% 1.84/2.08 0 [] greater(e_3,e_1).
% 1.84/2.08 0 [] greater(e_4,e_1).
% 1.84/2.08 0 [] greater(e_5,e_1).
% 1.84/2.08 0 [] greater(e_3,e_2).
% 1.84/2.08 0 [] greater(e_4,e_2).
% 1.84/2.08 0 [] greater(e_5,e_2).
% 1.84/2.08 0 [] greater(e_4,e_3).
% 1.84/2.08 0 [] greater(e_5,e_3).
% 1.84/2.08 0 [] greater(e_5,e_4).
% 1.84/2.08 0 [] -cycle(X,Y)| -cycle(X,Z)|e_qualish(Y,Z).
% 1.84/2.08 0 [] -group_element(X)|cycle(X,e_0)|cycle(X,e_1)|cycle(X,e_2)|cycle(X,e_3)|cycle(X,e_4).
% 1.84/2.08 0 [] cycle(e_5,e_0).
% 1.84/2.08 0 [] -cycle(X,Y)| -cycle(W,Z)| -next(X,W)| -greater(Y,e_0)| -next(Z,Z1)|e_qualish(Y,Z1).
% 1.84/2.08 0 [] -cycle(X,Z1)| -cycle(Y,e_0)| -cycle(W,Z2)| -next(Y,W)| -greater(Y,X)| -greater(Z1,Z2).
% 1.84/2.08 0 [] -cycle(X,e_0)| -product(X,e_1,Y)| -greater(Y,X).
% 1.84/2.08 0 [] -cycle(X,Y)| -product(X,e_1,Z)| -greater(Y,e_0)| -next(X,X1)|e_qualish(Z,X1).
% 1.84/2.08 0 [] group_element(e_1).
% 1.84/2.08 0 [] group_element(e_2).
% 1.84/2.08 0 [] group_element(e_3).
% 1.84/2.08 0 [] group_element(e_4).
% 1.84/2.08 0 [] group_element(e_5).
% 1.84/2.08 0 [] -e_qualish(e_1,e_2).
% 1.84/2.08 0 [] -e_qualish(e_1,e_3).
% 1.84/2.08 0 [] -e_qualish(e_1,e_4).
% 1.84/2.08 0 [] -e_qualish(e_1,e_5).
% 1.84/2.08 0 [] -e_qualish(e_2,e_1).
% 1.84/2.08 0 [] -e_qualish(e_2,e_3).
% 1.84/2.08 0 [] -e_qualish(e_2,e_4).
% 1.84/2.08 0 [] -e_qualish(e_2,e_5).
% 1.84/2.08 0 [] -e_qualish(e_3,e_1).
% 1.84/2.08 0 [] -e_qualish(e_3,e_2).
% 1.84/2.08 0 [] -e_qualish(e_3,e_4).
% 1.84/2.08 0 [] -e_qualish(e_3,e_5).
% 1.84/2.08 0 [] -e_qualish(e_4,e_1).
% 1.84/2.08 0 [] -e_qualish(e_4,e_2).
% 1.84/2.08 0 [] -e_qualish(e_4,e_3).
% 1.84/2.08 0 [] -e_qualish(e_4,e_5).
% 1.84/2.08 0 [] -e_qualish(e_5,e_1).
% 1.84/2.08 0 [] -e_qualish(e_5,e_2).
% 1.84/2.08 0 [] -e_qualish(e_5,e_3).
% 1.84/2.08 0 [] -e_qualish(e_5,e_4).
% 1.84/2.08 0 [] -group_element(X)| -group_element(Y)|product(X,Y,e_1)|product(X,Y,e_2)|product(X,Y,e_3)|product(X,Y,e_4)|product(X,Y,e_5).
% 1.84/2.08 0 [] -product(X,Y,W)| -product(X,Y,Z)|e_qualish(W,Z).
% 1.84/2.08 0 [] -product(X,W,Y)| -product(X,Z,Y)|e_qualish(W,Z).
% 1.84/2.08 0 [] -product(W,Y,X)| -product(Z,Y,X)|e_qualish(W,Z).
% 1.84/2.08 0 [] product(X,X,X).
% 1.84/2.08 0 [] -product(X,Y,Z1)| -product(Y,X,Z2)|product(Z1,Z2,X).
% 1.84/2.08 end_of_list.
% 1.84/2.08
% 1.84/2.08 SCAN INPUT: prop=0, horn=0, equality=0, symmetry=0, max_lits=7.
% 1.84/2.08
% 1.84/2.08 This is a non-Horn set without equality. The strategy will
% 1.84/2.08 be ordered hyper_res, unit deletion, and factoring, with
% 1.84/2.08 satellites in sos and with nuclei in usable.
% 1.84/2.08
% 1.84/2.08 dependent: set(hyper_res).
% 1.84/2.08 dependent: set(factor).
% 1.84/2.08 dependent: set(unit_deletion).
% 1.84/2.08
% 1.84/2.08 ------------> process usable:
% 1.84/2.08 ** KEPT (pick-wt=9): 1 [] -cycle(A,B)| -cycle(A,C)|e_qualish(B,C).
% 1.84/2.08 ** KEPT (pick-wt=17): 2 [] -group_element(A)|cycle(A,e_0)|cycle(A,e_1)|cycle(A,e_2)|cycle(A,e_3)|cycle(A,e_4).
% 1.84/2.08 ** KEPT (pick-wt=18): 3 [] -cycle(A,B)| -cycle(C,D)| -next(A,C)| -greater(B,e_0)| -next(D,E)|e_qualish(B,E).
% 1.84/2.08 ** KEPT (pick-wt=18): 4 [] -cycle(A,B)| -cycle(C,e_0)| -cycle(D,E)| -next(C,D)| -greater(C,A)| -greater(B,E).
% 1.84/2.08 ** KEPT (pick-wt=10): 5 [] -cycle(A,e_0)| -product(A,e_1,B)| -greater(B,A).
% 1.84/2.08 ** KEPT (pick-wt=16): 6 [] -cycle(A,B)| -product(A,e_1,C)| -greater(B,e_0)| -next(A,D)|e_qualish(C,D).
% 1.84/2.08 ** KEPT (pick-wt=3): 7 [] -e_qualish(e_1,e_2).
% 1.84/2.08 ** KEPT (pick-wt=3): 8 [] -e_qualish(e_1,e_3).
% 1.84/2.08 ** KEPT (pick-wt=3): 9 [] -e_qualish(e_1,e_4).
% 1.84/2.08 ** KEPT (pick-wt=3): 10 [] -e_qualish(e_1,e_5).
% 1.84/2.08 ** KEPT (pick-wt=3): 11 [] -e_qualish(e_2,e_1).
% 1.84/2.08 ** KEPT (pick-wt=3): 12 [] -e_qualish(e_2,e_3).
% 1.84/2.08 ** KEPT (pick-wt=3): 13 [] -e_qualish(e_2,e_4).
% 1.84/2.08 ** KEPT (pick-wt=3): 14 [] -e_qualish(e_2,e_5).
% 1.84/2.08 ** KEPT (pick-wt=3): 15 [] -e_qualish(e_3,e_1).
% 1.84/2.08 ** KEPT (pick-wt=3): 16 [] -e_qualish(e_3,e_2).
% 1.84/2.08 ** KEPT (pick-wt=3): 17 [] -e_qualish(e_3,e_4).
% 1.84/2.08 ** KEPT (pick-wt=3): 18 [] -e_qualish(e_3,e_5).
% 2.13/2.37 ** KEPT (pick-wt=3): 19 [] -e_qualish(e_4,e_1).
% 2.13/2.37 ** KEPT (pick-wt=3): 20 [] -e_qualish(e_4,e_2).
% 2.13/2.37 ** KEPT (pick-wt=3): 21 [] -e_qualish(e_4,e_3).
% 2.13/2.37 ** KEPT (pick-wt=3): 22 [] -e_qualish(e_4,e_5).
% 2.13/2.37 ** KEPT (pick-wt=3): 23 [] -e_qualish(e_5,e_1).
% 2.13/2.37 ** KEPT (pick-wt=3): 24 [] -e_qualish(e_5,e_2).
% 2.13/2.37 ** KEPT (pick-wt=3): 25 [] -e_qualish(e_5,e_3).
% 2.13/2.37 ** KEPT (pick-wt=3): 26 [] -e_qualish(e_5,e_4).
% 2.13/2.37 ** KEPT (pick-wt=24): 27 [] -group_element(A)| -group_element(B)|product(A,B,e_1)|product(A,B,e_2)|product(A,B,e_3)|product(A,B,e_4)|product(A,B,e_5).
% 2.13/2.37 ** KEPT (pick-wt=11): 28 [] -product(A,B,C)| -product(A,B,D)|e_qualish(C,D).
% 2.13/2.37 ** KEPT (pick-wt=11): 29 [] -product(A,B,C)| -product(A,D,C)|e_qualish(B,D).
% 2.13/2.37 ** KEPT (pick-wt=11): 30 [] -product(A,B,C)| -product(D,B,C)|e_qualish(A,D).
% 2.13/2.37 ** KEPT (pick-wt=12): 31 [] -product(A,B,C)| -product(B,A,D)|product(C,D,A).
% 2.13/2.37
% 2.13/2.37 ------------> process sos:
% 2.13/2.37 ** KEPT (pick-wt=3): 49 [] next(e_0,e_1).
% 2.13/2.37 ** KEPT (pick-wt=3): 50 [] next(e_1,e_2).
% 2.13/2.37 ** KEPT (pick-wt=3): 51 [] next(e_2,e_3).
% 2.13/2.37 ** KEPT (pick-wt=3): 52 [] next(e_3,e_4).
% 2.13/2.37 ** KEPT (pick-wt=3): 53 [] next(e_4,e_5).
% 2.13/2.37 ** KEPT (pick-wt=3): 54 [] greater(e_1,e_0).
% 2.13/2.37 ** KEPT (pick-wt=3): 55 [] greater(e_2,e_0).
% 2.13/2.37 ** KEPT (pick-wt=3): 56 [] greater(e_3,e_0).
% 2.13/2.37 ** KEPT (pick-wt=3): 57 [] greater(e_4,e_0).
% 2.13/2.37 ** KEPT (pick-wt=3): 58 [] greater(e_5,e_0).
% 2.13/2.37 ** KEPT (pick-wt=3): 59 [] greater(e_2,e_1).
% 2.13/2.37 ** KEPT (pick-wt=3): 60 [] greater(e_3,e_1).
% 2.13/2.37 ** KEPT (pick-wt=3): 61 [] greater(e_4,e_1).
% 2.13/2.37 ** KEPT (pick-wt=3): 62 [] greater(e_5,e_1).
% 2.13/2.37 ** KEPT (pick-wt=3): 63 [] greater(e_3,e_2).
% 2.13/2.37 ** KEPT (pick-wt=3): 64 [] greater(e_4,e_2).
% 2.13/2.37 ** KEPT (pick-wt=3): 65 [] greater(e_5,e_2).
% 2.13/2.37 ** KEPT (pick-wt=3): 66 [] greater(e_4,e_3).
% 2.13/2.37 ** KEPT (pick-wt=3): 67 [] greater(e_5,e_3).
% 2.13/2.37 ** KEPT (pick-wt=3): 68 [] greater(e_5,e_4).
% 2.13/2.37 ** KEPT (pick-wt=3): 69 [] cycle(e_5,e_0).
% 2.13/2.37 ** KEPT (pick-wt=2): 70 [] group_element(e_1).
% 2.13/2.37 ** KEPT (pick-wt=2): 71 [] group_element(e_2).
% 2.13/2.37 ** KEPT (pick-wt=2): 72 [] group_element(e_3).
% 2.13/2.37 ** KEPT (pick-wt=2): 73 [] group_element(e_4).
% 2.13/2.37 ** KEPT (pick-wt=2): 74 [] group_element(e_5).
% 2.13/2.37 ** KEPT (pick-wt=4): 75 [] product(A,A,A).
% 2.13/2.37
% 2.13/2.37 ======= end of input processing =======
% 2.13/2.37
% 2.13/2.37 =========== start of search ===========
% 2.13/2.37
% 2.13/2.37 -------- PROOF --------
% 2.13/2.37
% 2.13/2.37 ----> UNIT CONFLICT at 0.29 sec ----> 1729 [binary,1728.1,24.1] $F.
% 2.13/2.37
% 2.13/2.37 Length of proof is 105. Level of proof is 42.
% 2.13/2.37
% 2.13/2.37 ---------------- PROOF ----------------
% 2.13/2.37 % SZS status Unsatisfiable
% 2.13/2.37 % SZS output start Refutation
% See solution above
% 2.13/2.37 ------------ end of proof -------------
% 2.13/2.37
% 2.13/2.37
% 2.13/2.37 Search stopped by max_proofs option.
% 2.13/2.37
% 2.13/2.37
% 2.13/2.37 Search stopped by max_proofs option.
% 2.13/2.37
% 2.13/2.37 ============ end of search ============
% 2.13/2.37
% 2.13/2.37 -------------- statistics -------------
% 2.13/2.37 clauses given 252
% 2.13/2.37 clauses generated 16393
% 2.13/2.37 clauses kept 1728
% 2.13/2.37 clauses forward subsumed 14723
% 2.13/2.37 clauses back subsumed 1592
% 2.13/2.37 Kbytes malloced 1953
% 2.13/2.37
% 2.13/2.37 ----------- times (seconds) -----------
% 2.13/2.37 user CPU time 0.29 (0 hr, 0 min, 0 sec)
% 2.13/2.37 system CPU time 0.00 (0 hr, 0 min, 0 sec)
% 2.13/2.37 wall-clock time 2 (0 hr, 0 min, 2 sec)
% 2.13/2.37
% 2.13/2.37 That finishes the proof of the theorem.
% 2.13/2.37
% 2.13/2.37 Process 21527 finished Wed Jul 27 05:04:47 2022
% 2.13/2.37 Otter interrupted
% 2.13/2.37 PROOF FOUND
%------------------------------------------------------------------------------