%------------------------------------------------------------------------------
% File : Otter---3.3
% Problem : GRP025-1 : TPTP v8.1.0. Bugfixed v1.2.1.
% Transfm : none
% Format : tptp:raw
% Command : otter-tptp-script %s
% Computer : n026.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:55:53 EDT 2022
% Result : Unsatisfiable 4.62s 4.80s
% Output : Refutation 4.62s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 22
% Syntax : Number of clauses : 73 ( 50 unt; 13 nHn; 66 RR)
% Number of literals : 107 ( 50 equ; 22 neg)
% Maximal clause size : 4 ( 1 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-4 aty)
% Number of functors : 13 ( 13 usr; 9 con; 0-3 aty)
% Number of variables : 40 ( 1 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(2,axiom,
( ~ group_member(A,B)
| ~ group_member(C,B)
| product(B,A,C,multiply(B,A,C)) ),
file('GRP025-1.p',unknown),
[] ).
cnf(4,axiom,
( ~ product(A,B,C,D)
| ~ product(A,B,C,E)
| E = D ),
file('GRP025-1.p',unknown),
[] ).
cnf(5,axiom,
( ~ product(A,B,C,D)
| ~ product(A,C,E,F)
| ~ product(A,D,E,G)
| product(A,B,F,G) ),
file('GRP025-1.p',unknown),
[] ).
cnf(6,axiom,
( ~ product(A,B,C,D)
| ~ product(A,C,E,F)
| ~ product(A,B,F,G)
| product(A,D,E,G) ),
file('GRP025-1.p',unknown),
[] ).
cnf(7,axiom,
( ~ group_member(A,g1)
| A = a
| A = b ),
file('GRP025-1.p',unknown),
[] ).
cnf(9,axiom,
~ product(g2,an_isomorphism(d1),an_isomorphism(d2),an_isomorphism(d3)),
file('GRP025-1.p',unknown),
[] ).
cnf(10,plain,
( ~ group_member(A,B)
| product(B,A,A,multiply(B,A,A)) ),
inference(factor,[status(thm)],[2]),
[iquote('factor,2.1.2')] ).
cnf(17,plain,
( ~ product(A,B,C,D)
| ~ product(A,C,E,C)
| product(A,D,E,D) ),
inference(factor,[status(thm)],[6]),
[iquote('factor,6.1.3')] ).
cnf(21,axiom,
product(A,identity_for(A),B,B),
file('GRP025-1.p',unknown),
[] ).
cnf(22,axiom,
product(A,B,identity_for(A),B),
file('GRP025-1.p',unknown),
[] ).
cnf(23,axiom,
product(A,inverse(A,B),B,identity_for(A)),
file('GRP025-1.p',unknown),
[] ).
cnf(25,axiom,
group_member(a,g1),
file('GRP025-1.p',unknown),
[] ).
cnf(26,axiom,
group_member(b,g1),
file('GRP025-1.p',unknown),
[] ).
cnf(29,axiom,
product(g1,a,a,a),
file('GRP025-1.p',unknown),
[] ).
cnf(31,axiom,
product(g1,b,a,b),
file('GRP025-1.p',unknown),
[] ).
cnf(32,axiom,
product(g1,b,b,a),
file('GRP025-1.p',unknown),
[] ).
cnf(35,axiom,
product(g2,d,c,d),
file('GRP025-1.p',unknown),
[] ).
cnf(36,axiom,
product(g2,d,d,c),
file('GRP025-1.p',unknown),
[] ).
cnf(38,axiom,
an_isomorphism(a) = c,
file('GRP025-1.p',unknown),
[] ).
cnf(40,axiom,
an_isomorphism(b) = d,
file('GRP025-1.p',unknown),
[] ).
cnf(41,axiom,
group_member(d1,g1),
file('GRP025-1.p',unknown),
[] ).
cnf(42,axiom,
group_member(d2,g1),
file('GRP025-1.p',unknown),
[] ).
cnf(43,axiom,
group_member(d3,g1),
file('GRP025-1.p',unknown),
[] ).
cnf(44,axiom,
product(g1,d1,d2,d3),
file('GRP025-1.p',unknown),
[] ).
cnf(46,plain,
product(g1,a,a,multiply(g1,a,a)),
inference(hyper,[status(thm)],[25,10]),
[iquote('hyper,25,10')] ).
cnf(57,plain,
product(g1,b,b,multiply(g1,b,b)),
inference(hyper,[status(thm)],[26,10]),
[iquote('hyper,26,10')] ).
cnf(125,plain,
( d1 = a
| d1 = b ),
inference(hyper,[status(thm)],[41,7]),
[iquote('hyper,41,7')] ).
cnf(136,plain,
product(g1,d1,a,multiply(g1,d1,a)),
inference(hyper,[status(thm)],[41,2,25]),
[iquote('hyper,41,2,25')] ).
cnf(149,plain,
( d2 = a
| d2 = b ),
inference(hyper,[status(thm)],[42,7]),
[iquote('hyper,42,7')] ).
cnf(158,plain,
product(g1,d1,d2,multiply(g1,d1,d2)),
inference(hyper,[status(thm)],[42,2,41]),
[iquote('hyper,42,2,41')] ).
cnf(160,plain,
product(g1,a,d2,multiply(g1,a,d2)),
inference(hyper,[status(thm)],[42,2,25]),
[iquote('hyper,42,2,25')] ).
cnf(177,plain,
( d3 = a
| d3 = b ),
inference(hyper,[status(thm)],[43,7]),
[iquote('hyper,43,7')] ).
cnf(190,plain,
product(g1,b,d3,multiply(g1,b,d3)),
inference(hyper,[status(thm)],[43,2,26]),
[iquote('hyper,43,2,26')] ).
cnf(321,plain,
product(g2,identity_for(g2),c,identity_for(g2)),
inference(hyper,[status(thm)],[23,17,35]),
[iquote('hyper,23,17,35')] ).
cnf(322,plain,
product(g1,identity_for(g1),a,identity_for(g1)),
inference(hyper,[status(thm)],[23,17,31]),
[iquote('hyper,23,17,31')] ).
cnf(331,plain,
product(g1,inverse(g1,b),a,b),
inference(hyper,[status(thm)],[23,5,32,21]),
[iquote('hyper,23,5,32,21')] ).
cnf(362,plain,
product(g1,inverse(g1,d1),d3,d2),
inference(hyper,[status(thm)],[44,5,23,21]),
[iquote('hyper,44,5,23,21')] ).
cnf(1040,plain,
multiply(g1,a,a) = a,
inference(hyper,[status(thm)],[46,4,29]),
[iquote('hyper,46,4,29')] ).
cnf(1345,plain,
( ~ product(g2,c,an_isomorphism(d2),an_isomorphism(d3))
| d1 = b ),
inference(demod,[status(thm),theory(equality)],[inference(para_from,[status(thm),theory(equality)],[125,9]),38]),
[iquote('para_from,125.1.1,9.1.2.1,demod,38')] ).
cnf(2726,plain,
( ~ product(g2,an_isomorphism(d1),an_isomorphism(d2),d)
| d3 = a ),
inference(demod,[status(thm),theory(equality)],[inference(para_from,[status(thm),theory(equality)],[177,9]),40]),
[iquote('para_from,177.2.1,9.1.4.1,demod,40')] ).
cnf(5047,plain,
multiply(g1,b,b) = a,
inference(hyper,[status(thm)],[57,4,32]),
[iquote('hyper,57,4,32')] ).
cnf(5880,plain,
product(g2,A,c,A),
inference(hyper,[status(thm)],[321,17,22]),
[iquote('hyper,321,17,22')] ).
cnf(5887,plain,
identity_for(g2) = c,
inference(hyper,[status(thm)],[321,4,21]),
[iquote('hyper,321,4,21')] ).
cnf(5892,plain,
product(g2,c,A,A),
inference(para_from,[status(thm),theory(equality)],[5887,21]),
[iquote('para_from,5887.1.1,21.1.2')] ).
cnf(5900,plain,
product(g1,A,a,A),
inference(hyper,[status(thm)],[322,17,22]),
[iquote('hyper,322,17,22')] ).
cnf(5907,plain,
identity_for(g1) = a,
inference(hyper,[status(thm)],[322,4,21]),
[iquote('hyper,322,4,21')] ).
cnf(5912,plain,
product(g1,a,A,A),
inference(para_from,[status(thm),theory(equality)],[5907,21]),
[iquote('para_from,5907.1.1,21.1.2')] ).
cnf(5924,plain,
inverse(g1,b) = b,
inference(flip,[status(thm),theory(equality)],[inference(hyper,[status(thm)],[331,4,5900])]),
[iquote('hyper,331,4,5900,flip.1')] ).
cnf(6008,plain,
multiply(g1,d1,a) = d1,
inference(hyper,[status(thm)],[136,4,5900]),
[iquote('hyper,136,4,5900')] ).
cnf(6013,plain,
multiply(g1,d1,d2) = d3,
inference(hyper,[status(thm)],[158,4,44]),
[iquote('hyper,158,4,44')] ).
cnf(6016,plain,
( multiply(g1,a,d2) = d3
| d1 = b ),
inference(para_into,[status(thm),theory(equality)],[6013,125]),
[iquote('para_into,6013.1.1.2,125.1.1')] ).
cnf(6017,plain,
( multiply(g1,d1,b) = d3
| d2 = a ),
inference(para_into,[status(thm),theory(equality)],[6013,149]),
[iquote('para_into,6013.1.1.3,149.2.1')] ).
cnf(6018,plain,
( d3 = d1
| d2 = b ),
inference(flip,[status(thm),theory(equality)],[inference(demod,[status(thm),theory(equality)],[inference(para_into,[status(thm),theory(equality)],[6013,149]),6008])]),
[iquote('para_into,6013.1.1.3,149.1.1,demod,6008,flip.1')] ).
cnf(6020,plain,
( d1 = a
| d2 = b
| d3 = b ),
inference(flip,[status(thm),theory(equality)],[inference(para_into,[status(thm),theory(equality)],[6018,177])]),
[iquote('para_into,6018.1.1,177.1.1,flip.1')] ).
cnf(6034,plain,
multiply(g1,a,d2) = d2,
inference(hyper,[status(thm)],[160,4,5912]),
[iquote('hyper,160,4,5912')] ).
cnf(6035,plain,
( d3 = d2
| d1 = b ),
inference(flip,[status(thm),theory(equality)],[inference(demod,[status(thm),theory(equality)],[inference(back_demod,[status(thm)],[6016]),6034])]),
[iquote('back_demod,6016,demod,6034,flip.1')] ).
cnf(6177,plain,
( d3 = d2
| d2 = b
| d3 = b ),
inference(flip,[status(thm),theory(equality)],[inference(demod,[status(thm),theory(equality)],[inference(para_from,[status(thm),theory(equality)],[6020,6013]),6034])]),
[iquote('para_from,6020.1.1,6013.1.1.2,demod,6034,flip.1')] ).
cnf(6205,plain,
( d2 = d1
| d2 = b
| d3 = b ),
inference(factor_simp,[status(thm)],[inference(para_into,[status(thm),theory(equality)],[6177,6018])]),
[iquote('para_into,6177.1.1,6018.1.1,factor_simp')] ).
cnf(6262,plain,
d1 = b,
inference(factor_simp,[status(thm)],[inference(unit_del,[status(thm)],[inference(para_into,[status(thm),theory(equality)],[1345,6035]),5892])]),
[iquote('para_into,1345.1.4.1,6035.1.1,unit_del,5892,factor_simp')] ).
cnf(6264,plain,
( d2 = b
| d3 = b ),
inference(factor_simp,[status(thm)],[inference(demod,[status(thm),theory(equality)],[inference(back_demod,[status(thm)],[6205]),6262])]),
[iquote('back_demod,6205,demod,6262,factor_simp')] ).
cnf(6276,plain,
( d3 = a
| d2 = a ),
inference(flip,[status(thm),theory(equality)],[inference(demod,[status(thm),theory(equality)],[inference(back_demod,[status(thm)],[6017]),6262,5047])]),
[iquote('back_demod,6017,demod,6262,5047,flip.1')] ).
cnf(6285,plain,
( ~ product(g2,d,an_isomorphism(d2),d)
| d3 = a ),
inference(demod,[status(thm),theory(equality)],[inference(back_demod,[status(thm)],[2726]),6262,40]),
[iquote('back_demod,2726,demod,6262,40')] ).
cnf(6294,plain,
product(g1,b,d3,d2),
inference(demod,[status(thm),theory(equality)],[inference(back_demod,[status(thm)],[362]),6262,5924]),
[iquote('back_demod,362,demod,6262,5924')] ).
cnf(6295,plain,
~ product(g2,d,an_isomorphism(d2),an_isomorphism(d3)),
inference(demod,[status(thm),theory(equality)],[inference(back_demod,[status(thm)],[9]),6262,40]),
[iquote('back_demod,9,demod,6262,40')] ).
cnf(6300,plain,
multiply(g1,b,d3) = d2,
inference(flip,[status(thm),theory(equality)],[inference(hyper,[status(thm)],[6294,4,190])]),
[iquote('hyper,6294,4,190,flip.1')] ).
cnf(6332,plain,
( ~ product(g2,d,d,an_isomorphism(d3))
| d3 = b ),
inference(demod,[status(thm),theory(equality)],[inference(para_into,[status(thm),theory(equality)],[6295,6264]),40]),
[iquote('para_into,6295.1.3.1,6264.1.1,demod,40')] ).
cnf(6385,plain,
d3 = a,
inference(factor_simp,[status(thm)],[inference(unit_del,[status(thm)],[inference(demod,[status(thm),theory(equality)],[inference(para_into,[status(thm),theory(equality)],[6285,6276]),38]),5880])]),
[iquote('para_into,6285.1.3.1,6276.2.1,demod,38,unit_del,5880,factor_simp')] ).
cnf(6396,plain,
b = a,
inference(flip,[status(thm),theory(equality)],[inference(unit_del,[status(thm)],[inference(demod,[status(thm),theory(equality)],[inference(back_demod,[status(thm)],[6332]),6385,38,6385]),36])]),
[iquote('back_demod,6332,demod,6385,38,6385,unit_del,36,flip.1')] ).
cnf(6400,plain,
d2 = a,
inference(flip,[status(thm),theory(equality)],[inference(demod,[status(thm),theory(equality)],[inference(back_demod,[status(thm)],[6300]),6396,6385,1040])]),
[iquote('back_demod,6300,demod,6396,6385,1040,flip.1')] ).
cnf(6401,plain,
~ product(g2,d,c,c),
inference(demod,[status(thm),theory(equality)],[inference(back_demod,[status(thm)],[6295]),6400,38,6385,38]),
[iquote('back_demod,6295,demod,6400,38,6385,38')] ).
cnf(6412,plain,
d = c,
inference(flip,[status(thm),theory(equality)],[inference(demod,[status(thm),theory(equality)],[inference(back_demod,[status(thm)],[40]),6396,38])]),
[iquote('back_demod,39,demod,6396,38,flip.1')] ).
cnf(6416,plain,
~ product(g2,c,c,c),
inference(demod,[status(thm),theory(equality)],[inference(back_demod,[status(thm)],[6401]),6412]),
[iquote('back_demod,6401,demod,6412')] ).
cnf(6417,plain,
$false,
inference(binary,[status(thm)],[6416,5892]),
[iquote('binary,6416.1,5892.1')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12 % Problem : GRP025-1 : TPTP v8.1.0. Bugfixed v1.2.1.
% 0.06/0.12 % Command : otter-tptp-script %s
% 0.12/0.33 % Computer : n026.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:11:09 EDT 2022
% 0.12/0.33 % CPUTime :
% 1.58/2.16 ----- Otter 3.3f, August 2004 -----
% 1.58/2.16 The process was started by sandbox on n026.cluster.edu,
% 1.58/2.16 Wed Jul 27 05:11:09 2022
% 1.58/2.16 The command was "./otter". The process ID is 14510.
% 1.58/2.16
% 1.58/2.16 set(prolog_style_variables).
% 1.58/2.16 set(auto).
% 1.58/2.16 dependent: set(auto1).
% 1.58/2.16 dependent: set(process_input).
% 1.58/2.16 dependent: clear(print_kept).
% 1.58/2.16 dependent: clear(print_new_demod).
% 1.58/2.16 dependent: clear(print_back_demod).
% 1.58/2.16 dependent: clear(print_back_sub).
% 1.58/2.16 dependent: set(control_memory).
% 1.58/2.16 dependent: assign(max_mem, 12000).
% 1.58/2.16 dependent: assign(pick_given_ratio, 4).
% 1.58/2.16 dependent: assign(stats_level, 1).
% 1.58/2.16 dependent: assign(max_seconds, 10800).
% 1.58/2.16 clear(print_given).
% 1.58/2.16
% 1.58/2.16 list(usable).
% 1.58/2.16 0 [] A=A.
% 1.58/2.16 0 [] group_member(identity_for(Xg),Xg).
% 1.58/2.16 0 [] product(Xg,identity_for(Xg),X,X).
% 1.58/2.16 0 [] product(Xg,X,identity_for(Xg),X).
% 1.58/2.16 0 [] -group_member(X,Xg)|group_member(inverse(Xg,X),Xg).
% 1.58/2.16 0 [] product(Xg,inverse(Xg,X),X,identity_for(Xg)).
% 1.58/2.16 0 [] product(Xg,X,inverse(Xg,X),identity_for(Xg)).
% 1.58/2.16 0 [] -group_member(X,Xg)| -group_member(Y,Xg)|product(Xg,X,Y,multiply(Xg,X,Y)).
% 1.58/2.16 0 [] -group_member(X,Xg)| -group_member(Y,Xg)|group_member(multiply(Xg,X,Y),Xg).
% 1.58/2.16 0 [] -product(Xg,X,Y,Z)| -product(Xg,X,Y,W)|W=Z.
% 1.58/2.16 0 [] -product(Xg,X,Y,Xy)| -product(Xg,Y,Z,Yz)| -product(Xg,Xy,Z,Xyz)|product(Xg,X,Yz,Xyz).
% 1.58/2.16 0 [] -product(Xg,X,Y,Xy)| -product(Xg,Y,Z,Yz)| -product(Xg,X,Yz,Xyz)|product(Xg,Xy,Z,Xyz).
% 1.58/2.16 0 [] group_member(a,g1).
% 1.58/2.16 0 [] group_member(b,g1).
% 1.58/2.16 0 [] group_member(c,g2).
% 1.58/2.16 0 [] group_member(d,g2).
% 1.58/2.16 0 [] -group_member(X,g1)|X=a|X=b.
% 1.58/2.16 0 [] -group_member(X,g2)|X=c|X=d.
% 1.58/2.16 0 [] product(g1,a,a,a).
% 1.58/2.16 0 [] product(g1,a,b,b).
% 1.58/2.16 0 [] product(g1,b,a,b).
% 1.58/2.16 0 [] product(g1,b,b,a).
% 1.58/2.16 0 [] product(g2,c,c,c).
% 1.58/2.16 0 [] product(g2,c,d,d).
% 1.58/2.16 0 [] product(g2,d,c,d).
% 1.58/2.16 0 [] product(g2,d,d,c).
% 1.58/2.16 0 [] an_isomorphism(a)=c.
% 1.58/2.16 0 [] an_isomorphism(b)=d.
% 1.58/2.16 0 [] group_member(d1,g1).
% 1.58/2.16 0 [] group_member(d2,g1).
% 1.58/2.16 0 [] group_member(d3,g1).
% 1.58/2.16 0 [] product(g1,d1,d2,d3).
% 1.58/2.16 0 [] -product(g2,an_isomorphism(d1),an_isomorphism(d2),an_isomorphism(d3)).
% 1.58/2.16 end_of_list.
% 1.58/2.16
% 1.58/2.16 SCAN INPUT: prop=0, horn=0, equality=1, symmetry=0, max_lits=4.
% 1.58/2.16
% 1.58/2.16 This ia a non-Horn set with equality. The strategy will be
% 1.58/2.16 Knuth-Bendix, ordered hyper_res, factoring, and unit
% 1.58/2.16 deletion, with positive clauses in sos and nonpositive
% 1.58/2.16 clauses in usable.
% 1.58/2.16
% 1.58/2.16 dependent: set(knuth_bendix).
% 1.58/2.16 dependent: set(anl_eq).
% 1.58/2.16 dependent: set(para_from).
% 1.58/2.16 dependent: set(para_into).
% 1.58/2.16 dependent: clear(para_from_right).
% 1.58/2.16 dependent: clear(para_into_right).
% 1.58/2.16 dependent: set(para_from_vars).
% 1.58/2.16 dependent: set(eq_units_both_ways).
% 1.58/2.16 dependent: set(dynamic_demod_all).
% 1.58/2.16 dependent: set(dynamic_demod).
% 1.58/2.16 dependent: set(order_eq).
% 1.58/2.16 dependent: set(back_demod).
% 1.58/2.16 dependent: set(lrpo).
% 1.58/2.16 dependent: set(hyper_res).
% 1.58/2.16 dependent: set(unit_deletion).
% 1.58/2.16 dependent: set(factor).
% 1.58/2.16
% 1.58/2.16 ------------> process usable:
% 1.58/2.16 ** KEPT (pick-wt=8): 1 [] -group_member(A,B)|group_member(inverse(B,A),B).
% 1.58/2.16 ** KEPT (pick-wt=14): 2 [] -group_member(A,B)| -group_member(C,B)|product(B,A,C,multiply(B,A,C)).
% 1.58/2.16 ** KEPT (pick-wt=12): 3 [] -group_member(A,B)| -group_member(C,B)|group_member(multiply(B,A,C),B).
% 1.58/2.16 ** KEPT (pick-wt=13): 4 [] -product(A,B,C,D)| -product(A,B,C,E)|E=D.
% 1.58/2.16 ** KEPT (pick-wt=20): 5 [] -product(A,B,C,D)| -product(A,C,E,F)| -product(A,D,E,G)|product(A,B,F,G).
% 1.58/2.16 ** KEPT (pick-wt=20): 6 [] -product(A,B,C,D)| -product(A,C,E,F)| -product(A,B,F,G)|product(A,D,E,G).
% 1.58/2.16 ** KEPT (pick-wt=9): 7 [] -group_member(A,g1)|A=a|A=b.
% 1.58/2.16 ** KEPT (pick-wt=9): 8 [] -group_member(A,g2)|A=c|A=d.
% 1.58/2.16 ** KEPT (pick-wt=8): 9 [] -product(g2,an_isomorphism(d1),an_isomorphism(d2),an_isomorphism(d3)).
% 1.58/2.16
% 1.58/2.16 ------------> process sos:
% 1.58/2.16 ** KEPT (pick-wt=3): 19 [] A=A.
% 1.58/2.16 ** KEPT (pick-wt=4): 20 [] group_member(identity_for(A),A).
% 1.58/2.16 ** KEPT (pick-wt=6): 21 [] product(A,identity_for(A),B,B).
% 1.58/2.16 ** KEPT (pick-wt=6): 22 [] product(A,B,identity_for(A),B).
% 1.58/2.16 ** KEPT (pick-wt=8): 23 [] product(A,inverse(A,B),B,identity_for(A)).
% 1.58/2.16 ** KEPT (pick-wt=8): 24 [] product(A,B,inverse(A,B),identity_for(A)).
% 1.58/2.16 ** KEPT (pick-wt=3): 25 [] group_member(a,g1).
% 1.58/2.16 ** KEPT (pick-wt=3): 26 [] group_member(b,g1).
% 1.58/2.16 ** KEPT (pick-wt=3): 27 [] group_member(c,g2).
% 1.58/2.16 ** KEPT (pick-wt=3): 28 [] group_member(d,g2).
% 1.58/2.16 ** KEPT (pick-wt=5): 29 [] product(g1,a,a,a).
% 4.62/4.80 ** KEPT (pick-wt=5): 30 [] product(g1,a,b,b).
% 4.62/4.80 ** KEPT (pick-wt=5): 31 [] product(g1,b,a,b).
% 4.62/4.80 ** KEPT (pick-wt=5): 32 [] product(g1,b,b,a).
% 4.62/4.80 ** KEPT (pick-wt=5): 33 [] product(g2,c,c,c).
% 4.62/4.80 ** KEPT (pick-wt=5): 34 [] product(g2,c,d,d).
% 4.62/4.80 ** KEPT (pick-wt=5): 35 [] product(g2,d,c,d).
% 4.62/4.80 ** KEPT (pick-wt=5): 36 [] product(g2,d,d,c).
% 4.62/4.80 ** KEPT (pick-wt=4): 37 [] an_isomorphism(a)=c.
% 4.62/4.80 ---> New Demodulator: 38 [new_demod,37] an_isomorphism(a)=c.
% 4.62/4.80 ** KEPT (pick-wt=4): 39 [] an_isomorphism(b)=d.
% 4.62/4.80 ---> New Demodulator: 40 [new_demod,39] an_isomorphism(b)=d.
% 4.62/4.80 ** KEPT (pick-wt=3): 41 [] group_member(d1,g1).
% 4.62/4.80 ** KEPT (pick-wt=3): 42 [] group_member(d2,g1).
% 4.62/4.80 ** KEPT (pick-wt=3): 43 [] group_member(d3,g1).
% 4.62/4.80 ** KEPT (pick-wt=5): 44 [] product(g1,d1,d2,d3).
% 4.62/4.80 Following clause subsumed by 19 during input processing: 0 [copy,19,flip.1] A=A.
% 4.62/4.80 19 back subsumes 12.
% 4.62/4.80 >>>> Starting back demodulation with 38.
% 4.62/4.80 >>>> Starting back demodulation with 40.
% 4.62/4.80
% 4.62/4.80 ======= end of input processing =======
% 4.62/4.80
% 4.62/4.80 =========== start of search ===========
% 4.62/4.80
% 4.62/4.80
% 4.62/4.80 Resetting weight limit to 9.
% 4.62/4.80
% 4.62/4.80
% 4.62/4.80 Resetting weight limit to 9.
% 4.62/4.80
% 4.62/4.80 sos_size=5305
% 4.62/4.80
% 4.62/4.80 -------- PROOF --------
% 4.62/4.80
% 4.62/4.80 ----> UNIT CONFLICT at 2.64 sec ----> 6417 [binary,6416.1,5892.1] $F.
% 4.62/4.80
% 4.62/4.80 Length of proof is 50. Level of proof is 14.
% 4.62/4.80
% 4.62/4.80 ---------------- PROOF ----------------
% 4.62/4.80 % SZS status Unsatisfiable
% 4.62/4.80 % SZS output start Refutation
% See solution above
% 4.62/4.80 ------------ end of proof -------------
% 4.62/4.80
% 4.62/4.80
% 4.62/4.80 Search stopped by max_proofs option.
% 4.62/4.80
% 4.62/4.80
% 4.62/4.80 Search stopped by max_proofs option.
% 4.62/4.80
% 4.62/4.80 ============ end of search ============
% 4.62/4.80
% 4.62/4.80 -------------- statistics -------------
% 4.62/4.80 clauses given 789
% 4.62/4.80 clauses generated 274446
% 4.62/4.80 clauses kept 6376
% 4.62/4.80 clauses forward subsumed 20477
% 4.62/4.80 clauses back subsumed 31
% 4.62/4.80 Kbytes malloced 4882
% 4.62/4.80
% 4.62/4.80 ----------- times (seconds) -----------
% 4.62/4.80 user CPU time 2.64 (0 hr, 0 min, 2 sec)
% 4.62/4.80 system CPU time 0.01 (0 hr, 0 min, 0 sec)
% 4.62/4.80 wall-clock time 4 (0 hr, 0 min, 4 sec)
% 4.62/4.80
% 4.62/4.80 That finishes the proof of the theorem.
% 4.62/4.80
% 4.62/4.80 Process 14510 finished Wed Jul 27 05:11:13 2022
% 4.62/4.80 Otter interrupted
% 4.62/4.80 PROOF FOUND
%------------------------------------------------------------------------------