%------------------------------------------------------------------------------
% File : Otter---3.3
% Problem : HWV007-2 : TPTP v8.1.0. Bugfixed v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : otter-tptp-script %s
% Computer : n012.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:58:03 EDT 2022
% Result : Unsatisfiable 1.66s 1.87s
% Output : Refutation 1.66s
% Verified :
% SZS Type : Refutation
% Derivation depth : 16
% Number of leaves : 48
% Syntax : Number of clauses : 109 ( 48 unt; 24 nHn; 109 RR)
% Number of literals : 195 ( 0 equ; 58 neg)
% Maximal clause size : 4 ( 1 avg)
% Maximal term depth : 4 ( 2 avg)
% Number of predicates : 13 ( 12 usr; 1 prp; 0-2 aty)
% Number of functors : 13 ( 13 usr; 1 con; 0-1 aty)
% Number of variables : 41 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(1,axiom,
( ~ connection(A,B)
| ~ zero(A)
| zero(B) ),
file('HWV007-2.p',unknown),
[] ).
cnf(2,axiom,
( ~ connection(A,B)
| ~ one(A)
| one(B) ),
file('HWV007-2.p',unknown),
[] ).
cnf(3,axiom,
( ~ connection(A,B)
| ~ zero(B)
| zero(A) ),
file('HWV007-2.p',unknown),
[] ).
cnf(4,axiom,
( ~ connection(A,B)
| ~ one(B)
| one(A) ),
file('HWV007-2.p',unknown),
[] ).
cnf(5,axiom,
( ~ zero(A)
| ~ one(A) ),
file('HWV007-2.p',unknown),
[] ).
cnf(7,axiom,
( ~ and_ok(A)
| ~ zero(in2(A))
| zero(out1(A)) ),
file('HWV007-2.p',unknown),
[] ).
cnf(8,axiom,
( ~ and_ok(A)
| ~ one(in1(A))
| ~ one(in2(A))
| one(out1(A)) ),
file('HWV007-2.p',unknown),
[] ).
cnf(10,axiom,
( ~ and_ok(A)
| ~ one(out1(A))
| one(in1(A)) ),
file('HWV007-2.p',unknown),
[] ).
cnf(13,axiom,
( ~ logic_and(A)
| and_ok(A)
| abnormal(A) ),
file('HWV007-2.p',unknown),
[] ).
cnf(17,axiom,
( ~ or_ok(A)
| ~ one(out1(A))
| one(in1(A))
| one(in2(A)) ),
file('HWV007-2.p',unknown),
[] ).
cnf(19,axiom,
( ~ or_ok(A)
| ~ zero(out1(A))
| zero(in2(A)) ),
file('HWV007-2.p',unknown),
[] ).
cnf(21,axiom,
( ~ logic_or(A)
| or_ok(A)
| abnormal(A) ),
file('HWV007-2.p',unknown),
[] ).
cnf(23,axiom,
( ~ not_ok(A)
| ~ one(in1(A))
| zero(out1(A)) ),
file('HWV007-2.p',unknown),
[] ).
cnf(27,axiom,
( ~ logic_not(A)
| not_ok(A)
| abnormal(A) ),
file('HWV007-2.p',unknown),
[] ).
cnf(28,axiom,
( ~ halfadder(A)
| logic_and(and1(A)) ),
file('HWV007-2.p',unknown),
[] ).
cnf(29,axiom,
( ~ halfadder(A)
| logic_and(and2(A)) ),
file('HWV007-2.p',unknown),
[] ).
cnf(30,axiom,
( ~ halfadder(A)
| logic_not(not1(A)) ),
file('HWV007-2.p',unknown),
[] ).
cnf(31,axiom,
( ~ halfadder(A)
| logic_or(or1(A)) ),
file('HWV007-2.p',unknown),
[] ).
cnf(32,axiom,
( ~ halfadder(A)
| connection(in1(A),in1(or1(A))) ),
file('HWV007-2.p',unknown),
[] ).
cnf(33,axiom,
( ~ halfadder(A)
| connection(in2(A),in2(or1(A))) ),
file('HWV007-2.p',unknown),
[] ).
cnf(34,axiom,
( ~ halfadder(A)
| connection(in1(A),in1(and2(A))) ),
file('HWV007-2.p',unknown),
[] ).
cnf(35,axiom,
( ~ halfadder(A)
| connection(in2(A),in2(and2(A))) ),
file('HWV007-2.p',unknown),
[] ).
cnf(36,axiom,
( ~ halfadder(A)
| connection(outs(A),out1(and1(A))) ),
file('HWV007-2.p',unknown),
[] ).
cnf(37,axiom,
( ~ halfadder(A)
| connection(outc(A),out1(and2(A))) ),
file('HWV007-2.p',unknown),
[] ).
cnf(38,axiom,
( ~ halfadder(A)
| connection(out1(or1(A)),in1(and1(A))) ),
file('HWV007-2.p',unknown),
[] ).
cnf(39,axiom,
( ~ halfadder(A)
| connection(out1(and2(A)),in1(not1(A))) ),
file('HWV007-2.p',unknown),
[] ).
cnf(40,axiom,
( ~ halfadder(A)
| connection(out1(not1(A)),in2(and1(A))) ),
file('HWV007-2.p',unknown),
[] ).
cnf(41,axiom,
( ~ fulladder(A)
| halfadder(h1(A)) ),
file('HWV007-2.p',unknown),
[] ).
cnf(42,axiom,
( ~ fulladder(A)
| halfadder(h2(A)) ),
file('HWV007-2.p',unknown),
[] ).
cnf(43,axiom,
( ~ fulladder(A)
| logic_or(or1(A)) ),
file('HWV007-2.p',unknown),
[] ).
cnf(44,axiom,
( ~ fulladder(A)
| connection(outs(h1(A)),in2(h2(A))) ),
file('HWV007-2.p',unknown),
[] ).
cnf(45,axiom,
( ~ fulladder(A)
| connection(outc(h1(A)),in2(or1(A))) ),
file('HWV007-2.p',unknown),
[] ).
cnf(47,axiom,
( ~ fulladder(A)
| connection(in1(A),in1(h2(A))) ),
file('HWV007-2.p',unknown),
[] ).
cnf(48,axiom,
( ~ fulladder(A)
| connection(in2(A),in1(h1(A))) ),
file('HWV007-2.p',unknown),
[] ).
cnf(49,axiom,
( ~ fulladder(A)
| connection(inc(A),in2(h1(A))) ),
file('HWV007-2.p',unknown),
[] ).
cnf(50,axiom,
( ~ fulladder(A)
| connection(outs(A),outs(h2(A))) ),
file('HWV007-2.p',unknown),
[] ).
cnf(51,axiom,
( ~ fulladder(A)
| connection(outc(A),out1(or1(A))) ),
file('HWV007-2.p',unknown),
[] ).
cnf(52,axiom,
~ abnormal(and2(h1(f))),
file('HWV007-2.p',unknown),
[] ).
cnf(53,axiom,
( ~ abnormal(or1(f))
| ~ abnormal(and1(h1(f))) ),
file('HWV007-2.p',unknown),
[] ).
cnf(54,axiom,
( ~ abnormal(or1(f))
| ~ abnormal(not1(h1(f))) ),
file('HWV007-2.p',unknown),
[] ).
cnf(55,axiom,
( ~ abnormal(or1(f))
| ~ abnormal(and1(h2(f))) ),
file('HWV007-2.p',unknown),
[] ).
cnf(56,axiom,
( ~ abnormal(or1(f))
| ~ abnormal(or1(h2(f))) ),
file('HWV007-2.p',unknown),
[] ).
cnf(57,axiom,
fulladder(f),
file('HWV007-2.p',unknown),
[] ).
cnf(58,axiom,
zero(in1(f)),
file('HWV007-2.p',unknown),
[] ).
cnf(59,axiom,
one(in2(f)),
file('HWV007-2.p',unknown),
[] ).
cnf(60,axiom,
one(inc(f)),
file('HWV007-2.p',unknown),
[] ).
cnf(61,axiom,
one(outs(f)),
file('HWV007-2.p',unknown),
[] ).
cnf(62,axiom,
zero(outc(f)),
file('HWV007-2.p',unknown),
[] ).
cnf(63,plain,
connection(outc(f),out1(or1(f))),
inference(hyper,[status(thm)],[57,51]),
[iquote('hyper,57,51')] ).
cnf(64,plain,
connection(outs(f),outs(h2(f))),
inference(hyper,[status(thm)],[57,50]),
[iquote('hyper,57,50')] ).
cnf(65,plain,
connection(inc(f),in2(h1(f))),
inference(hyper,[status(thm)],[57,49]),
[iquote('hyper,57,49')] ).
cnf(66,plain,
connection(in2(f),in1(h1(f))),
inference(hyper,[status(thm)],[57,48]),
[iquote('hyper,57,48')] ).
cnf(67,plain,
connection(in1(f),in1(h2(f))),
inference(hyper,[status(thm)],[57,47]),
[iquote('hyper,57,47')] ).
cnf(69,plain,
connection(outc(h1(f)),in2(or1(f))),
inference(hyper,[status(thm)],[57,45]),
[iquote('hyper,57,45')] ).
cnf(70,plain,
connection(outs(h1(f)),in2(h2(f))),
inference(hyper,[status(thm)],[57,44]),
[iquote('hyper,57,44')] ).
cnf(71,plain,
logic_or(or1(f)),
inference(hyper,[status(thm)],[57,43]),
[iquote('hyper,57,43')] ).
cnf(72,plain,
halfadder(h2(f)),
inference(hyper,[status(thm)],[57,42]),
[iquote('hyper,57,42')] ).
cnf(73,plain,
halfadder(h1(f)),
inference(hyper,[status(thm)],[57,41]),
[iquote('hyper,57,41')] ).
cnf(74,plain,
( or_ok(or1(f))
| abnormal(or1(f)) ),
inference(hyper,[status(thm)],[71,21]),
[iquote('hyper,71,21')] ).
cnf(77,plain,
connection(out1(or1(h2(f))),in1(and1(h2(f)))),
inference(hyper,[status(thm)],[72,38]),
[iquote('hyper,72,38')] ).
cnf(79,plain,
connection(outs(h2(f)),out1(and1(h2(f)))),
inference(hyper,[status(thm)],[72,36]),
[iquote('hyper,72,36')] ).
cnf(82,plain,
connection(in2(h2(f)),in2(or1(h2(f)))),
inference(hyper,[status(thm)],[72,33]),
[iquote('hyper,72,33')] ).
cnf(83,plain,
connection(in1(h2(f)),in1(or1(h2(f)))),
inference(hyper,[status(thm)],[72,32]),
[iquote('hyper,72,32')] ).
cnf(84,plain,
logic_or(or1(h2(f))),
inference(hyper,[status(thm)],[72,31]),
[iquote('hyper,72,31')] ).
cnf(87,plain,
logic_and(and1(h2(f))),
inference(hyper,[status(thm)],[72,28]),
[iquote('hyper,72,28')] ).
cnf(88,plain,
connection(out1(not1(h1(f))),in2(and1(h1(f)))),
inference(hyper,[status(thm)],[73,40]),
[iquote('hyper,73,40')] ).
cnf(89,plain,
connection(out1(and2(h1(f))),in1(not1(h1(f)))),
inference(hyper,[status(thm)],[73,39]),
[iquote('hyper,73,39')] ).
cnf(91,plain,
connection(outc(h1(f)),out1(and2(h1(f)))),
inference(hyper,[status(thm)],[73,37]),
[iquote('hyper,73,37')] ).
cnf(92,plain,
connection(outs(h1(f)),out1(and1(h1(f)))),
inference(hyper,[status(thm)],[73,36]),
[iquote('hyper,73,36')] ).
cnf(93,plain,
connection(in2(h1(f)),in2(and2(h1(f)))),
inference(hyper,[status(thm)],[73,35]),
[iquote('hyper,73,35')] ).
cnf(94,plain,
connection(in1(h1(f)),in1(and2(h1(f)))),
inference(hyper,[status(thm)],[73,34]),
[iquote('hyper,73,34')] ).
cnf(98,plain,
logic_not(not1(h1(f))),
inference(hyper,[status(thm)],[73,30]),
[iquote('hyper,73,30')] ).
cnf(99,plain,
logic_and(and2(h1(f))),
inference(hyper,[status(thm)],[73,29]),
[iquote('hyper,73,29')] ).
cnf(100,plain,
logic_and(and1(h1(f))),
inference(hyper,[status(thm)],[73,28]),
[iquote('hyper,73,28')] ).
cnf(101,plain,
( or_ok(or1(h2(f)))
| abnormal(or1(h2(f))) ),
inference(hyper,[status(thm)],[84,21]),
[iquote('hyper,84,21')] ).
cnf(102,plain,
zero(out1(or1(f))),
inference(hyper,[status(thm)],[63,1,62]),
[iquote('hyper,63,1,62')] ).
cnf(105,plain,
( and_ok(and1(h2(f)))
| abnormal(and1(h2(f))) ),
inference(hyper,[status(thm)],[87,13]),
[iquote('hyper,87,13')] ).
cnf(107,plain,
one(outs(h2(f))),
inference(hyper,[status(thm)],[64,2,61]),
[iquote('hyper,64,2,61')] ).
cnf(108,plain,
( not_ok(not1(h1(f)))
| abnormal(not1(h1(f))) ),
inference(hyper,[status(thm)],[98,27]),
[iquote('hyper,98,27')] ).
cnf(109,plain,
and_ok(and2(h1(f))),
inference(unit_del,[status(thm)],[inference(hyper,[status(thm)],[99,13]),52]),
[iquote('hyper,99,13,unit_del,52')] ).
cnf(110,plain,
( and_ok(and1(h1(f)))
| abnormal(and1(h1(f))) ),
inference(hyper,[status(thm)],[100,13]),
[iquote('hyper,100,13')] ).
cnf(111,plain,
one(in2(h1(f))),
inference(hyper,[status(thm)],[65,2,60]),
[iquote('hyper,65,2,60')] ).
cnf(112,plain,
one(in1(h1(f))),
inference(hyper,[status(thm)],[66,2,59]),
[iquote('hyper,66,2,59')] ).
cnf(113,plain,
zero(in1(h2(f))),
inference(hyper,[status(thm)],[67,1,58]),
[iquote('hyper,67,1,58')] ).
cnf(114,plain,
( abnormal(or1(f))
| zero(in2(or1(f))) ),
inference(hyper,[status(thm)],[74,19,102]),
[iquote('hyper,74,19,102')] ).
cnf(116,plain,
( abnormal(or1(f))
| zero(outc(h1(f))) ),
inference(hyper,[status(thm)],[114,3,69]),
[iquote('hyper,114,3,69')] ).
cnf(119,plain,
one(out1(and1(h2(f)))),
inference(hyper,[status(thm)],[79,2,107]),
[iquote('hyper,79,2,107')] ).
cnf(121,plain,
zero(in1(or1(h2(f)))),
inference(hyper,[status(thm)],[83,1,113]),
[iquote('hyper,83,1,113')] ).
cnf(123,plain,
one(in2(and2(h1(f)))),
inference(hyper,[status(thm)],[93,2,111]),
[iquote('hyper,93,2,111')] ).
cnf(124,plain,
one(in1(and2(h1(f)))),
inference(hyper,[status(thm)],[94,2,112]),
[iquote('hyper,94,2,112')] ).
cnf(125,plain,
one(out1(and2(h1(f)))),
inference(hyper,[status(thm)],[124,8,109,123]),
[iquote('hyper,124,8,109,123')] ).
cnf(126,plain,
one(outc(h1(f))),
inference(hyper,[status(thm)],[125,4,91]),
[iquote('hyper,125,4,91')] ).
cnf(127,plain,
one(in1(not1(h1(f)))),
inference(hyper,[status(thm)],[125,2,89]),
[iquote('hyper,125,2,89')] ).
cnf(128,plain,
abnormal(or1(f)),
inference(hyper,[status(thm)],[126,5,116]),
[iquote('hyper,126,5,116')] ).
cnf(134,plain,
( abnormal(and1(h2(f)))
| one(in1(and1(h2(f)))) ),
inference(hyper,[status(thm)],[105,10,119]),
[iquote('hyper,105,10,119')] ).
cnf(136,plain,
( abnormal(not1(h1(f)))
| zero(out1(not1(h1(f)))) ),
inference(hyper,[status(thm)],[108,23,127]),
[iquote('hyper,108,23,127')] ).
cnf(141,plain,
( abnormal(and1(h2(f)))
| one(out1(or1(h2(f)))) ),
inference(hyper,[status(thm)],[134,4,77]),
[iquote('hyper,134,4,77')] ).
cnf(143,plain,
( abnormal(not1(h1(f)))
| zero(in2(and1(h1(f)))) ),
inference(hyper,[status(thm)],[136,1,88]),
[iquote('hyper,136,1,88')] ).
cnf(146,plain,
( abnormal(and1(h2(f)))
| one(in1(or1(h2(f))))
| one(in2(or1(h2(f))))
| abnormal(or1(h2(f))) ),
inference(hyper,[status(thm)],[141,17,101]),
[iquote('hyper,141,17,101')] ).
cnf(147,plain,
( abnormal(not1(h1(f)))
| zero(out1(and1(h1(f))))
| abnormal(and1(h1(f))) ),
inference(hyper,[status(thm)],[143,7,110]),
[iquote('hyper,143,7,110')] ).
cnf(150,plain,
( abnormal(not1(h1(f)))
| abnormal(and1(h1(f)))
| zero(outs(h1(f))) ),
inference(hyper,[status(thm)],[147,3,92]),
[iquote('hyper,147,3,92')] ).
cnf(151,plain,
( abnormal(not1(h1(f)))
| abnormal(and1(h1(f)))
| zero(in2(h2(f))) ),
inference(hyper,[status(thm)],[150,1,70]),
[iquote('hyper,150,1,70')] ).
cnf(152,plain,
( abnormal(not1(h1(f)))
| abnormal(and1(h1(f)))
| zero(in2(or1(h2(f)))) ),
inference(hyper,[status(thm)],[151,1,82]),
[iquote('hyper,151,1,82')] ).
cnf(154,plain,
( abnormal(and1(h2(f)))
| one(in2(or1(h2(f))))
| abnormal(or1(h2(f))) ),
inference(hyper,[status(thm)],[146,5,121]),
[iquote('hyper,146,5,121')] ).
cnf(159,plain,
( abnormal(and1(h2(f)))
| abnormal(or1(h2(f)))
| abnormal(not1(h1(f)))
| abnormal(and1(h1(f))) ),
inference(hyper,[status(thm)],[154,5,152]),
[iquote('hyper,154,5,152')] ).
cnf(167,plain,
( abnormal(or1(h2(f)))
| abnormal(not1(h1(f)))
| abnormal(and1(h1(f))) ),
inference(hyper,[status(thm)],[159,55,128]),
[iquote('hyper,159,55,128')] ).
cnf(171,plain,
( abnormal(not1(h1(f)))
| abnormal(and1(h1(f))) ),
inference(hyper,[status(thm)],[167,56,128]),
[iquote('hyper,167,56,128')] ).
cnf(174,plain,
abnormal(and1(h1(f))),
inference(hyper,[status(thm)],[171,54,128]),
[iquote('hyper,171,54,128')] ).
cnf(176,plain,
$false,
inference(hyper,[status(thm)],[174,53,128]),
[iquote('hyper,174,53,128')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.13 % Problem : HWV007-2 : TPTP v8.1.0. Bugfixed v2.7.0.
% 0.04/0.14 % Command : otter-tptp-script %s
% 0.13/0.35 % Computer : n012.cluster.edu
% 0.13/0.35 % Model : x86_64 x86_64
% 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.35 % Memory : 8042.1875MB
% 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.35 % CPULimit : 300
% 0.13/0.35 % WCLimit : 300
% 0.13/0.35 % DateTime : Wed Jul 27 06:42:51 EDT 2022
% 0.13/0.35 % CPUTime :
% 1.66/1.87 ----- Otter 3.3f, August 2004 -----
% 1.66/1.87 The process was started by sandbox on n012.cluster.edu,
% 1.66/1.87 Wed Jul 27 06:42:51 2022
% 1.66/1.87 The command was "./otter". The process ID is 26509.
% 1.66/1.87
% 1.66/1.87 set(prolog_style_variables).
% 1.66/1.87 set(auto).
% 1.66/1.87 dependent: set(auto1).
% 1.66/1.87 dependent: set(process_input).
% 1.66/1.87 dependent: clear(print_kept).
% 1.66/1.87 dependent: clear(print_new_demod).
% 1.66/1.87 dependent: clear(print_back_demod).
% 1.66/1.87 dependent: clear(print_back_sub).
% 1.66/1.87 dependent: set(control_memory).
% 1.66/1.87 dependent: assign(max_mem, 12000).
% 1.66/1.87 dependent: assign(pick_given_ratio, 4).
% 1.66/1.87 dependent: assign(stats_level, 1).
% 1.66/1.87 dependent: assign(max_seconds, 10800).
% 1.66/1.87 clear(print_given).
% 1.66/1.87
% 1.66/1.87 list(usable).
% 1.66/1.87 0 [] -connection(P1,P2)| -zero(P1)|zero(P2).
% 1.66/1.87 0 [] -connection(P1,P2)| -one(P1)|one(P2).
% 1.66/1.87 0 [] -connection(P1,P2)| -zero(P2)|zero(P1).
% 1.66/1.87 0 [] -connection(P1,P2)| -one(P2)|one(P1).
% 1.66/1.87 0 [] -zero(P)| -one(P).
% 1.66/1.87 0 [] -and_ok(K)| -zero(in1(K))|zero(out1(K)).
% 1.66/1.87 0 [] -and_ok(K)| -zero(in2(K))|zero(out1(K)).
% 1.66/1.87 0 [] -and_ok(K)| -one(in1(K))| -one(in2(K))|one(out1(K)).
% 1.66/1.87 0 [] -and_ok(K)| -zero(out1(K))|zero(in1(K))|zero(in2(K)).
% 1.66/1.87 0 [] -and_ok(K)| -one(out1(K))|one(in1(K)).
% 1.66/1.87 0 [] -and_ok(K)| -one(out1(K))|one(in2(K)).
% 1.66/1.87 0 [] -and_ok(K)| -abnormal(K).
% 1.66/1.87 0 [] -logic_and(K)|and_ok(K)|abnormal(K).
% 1.66/1.87 0 [] -or_ok(K)| -one(in1(K))|one(out1(K)).
% 1.66/1.87 0 [] -or_ok(K)| -one(in2(K))|one(out1(K)).
% 1.66/1.87 0 [] -or_ok(K)| -zero(in1(K))| -zero(in2(K))|zero(out1(K)).
% 1.66/1.87 0 [] -or_ok(K)| -one(out1(K))|one(in1(K))|one(in2(K)).
% 1.66/1.87 0 [] -or_ok(K)| -zero(out1(K))|zero(in1(K)).
% 1.66/1.87 0 [] -or_ok(K)| -zero(out1(K))|zero(in2(K)).
% 1.66/1.87 0 [] -or_ok(K)| -abnormal(K).
% 1.66/1.87 0 [] -logic_or(K)|or_ok(K)|abnormal(K).
% 1.66/1.87 0 [] -not_ok(K)| -zero(in1(K))|one(out1(K)).
% 1.66/1.87 0 [] -not_ok(K)| -one(in1(K))|zero(out1(K)).
% 1.66/1.87 0 [] -not_ok(K)| -zero(out1(K))|one(in1(K)).
% 1.66/1.87 0 [] -not_ok(K)| -one(out1(K))|zero(in1(K)).
% 1.66/1.87 0 [] -not_ok(K)| -abnormal(K).
% 1.66/1.87 0 [] -logic_not(K)|not_ok(K)|abnormal(K).
% 1.66/1.87 0 [] -halfadder(X)|logic_and(and1(X)).
% 1.66/1.87 0 [] -halfadder(X)|logic_and(and2(X)).
% 1.66/1.87 0 [] -halfadder(X)|logic_not(not1(X)).
% 1.66/1.87 0 [] -halfadder(X)|logic_or(or1(X)).
% 1.66/1.87 0 [] -halfadder(X)|connection(in1(X),in1(or1(X))).
% 1.66/1.87 0 [] -halfadder(X)|connection(in2(X),in2(or1(X))).
% 1.66/1.87 0 [] -halfadder(X)|connection(in1(X),in1(and2(X))).
% 1.66/1.87 0 [] -halfadder(X)|connection(in2(X),in2(and2(X))).
% 1.66/1.87 0 [] -halfadder(X)|connection(outs(X),out1(and1(X))).
% 1.66/1.87 0 [] -halfadder(X)|connection(outc(X),out1(and2(X))).
% 1.66/1.87 0 [] -halfadder(X)|connection(out1(or1(X)),in1(and1(X))).
% 1.66/1.87 0 [] -halfadder(X)|connection(out1(and2(X)),in1(not1(X))).
% 1.66/1.87 0 [] -halfadder(X)|connection(out1(not1(X)),in2(and1(X))).
% 1.66/1.87 0 [] -fulladder(X)|halfadder(h1(X)).
% 1.66/1.87 0 [] -fulladder(X)|halfadder(h2(X)).
% 1.66/1.87 0 [] -fulladder(X)|logic_or(or1(X)).
% 1.66/1.87 0 [] -fulladder(X)|connection(outs(h1(X)),in2(h2(X))).
% 1.66/1.87 0 [] -fulladder(X)|connection(outc(h1(X)),in2(or1(X))).
% 1.66/1.87 0 [] -fulladder(X)|connection(outc(h2(X)),in1(or1(X))).
% 1.66/1.87 0 [] -fulladder(X)|connection(in1(X),in1(h2(X))).
% 1.66/1.87 0 [] -fulladder(X)|connection(in2(X),in1(h1(X))).
% 1.66/1.87 0 [] -fulladder(X)|connection(inc(X),in2(h1(X))).
% 1.66/1.87 0 [] -fulladder(X)|connection(outs(X),outs(h2(X))).
% 1.66/1.87 0 [] -fulladder(X)|connection(outc(X),out1(or1(X))).
% 1.66/1.87 0 [] fulladder(f).
% 1.66/1.87 0 [] zero(in1(f)).
% 1.66/1.87 0 [] one(in2(f)).
% 1.66/1.87 0 [] one(inc(f)).
% 1.66/1.87 0 [] one(outs(f)).
% 1.66/1.87 0 [] zero(outc(f)).
% 1.66/1.87 0 [] -abnormal(and2(h1(f))).
% 1.66/1.87 0 [] -abnormal(or1(f))| -abnormal(and1(h1(f))).
% 1.66/1.87 0 [] -abnormal(or1(f))| -abnormal(not1(h1(f))).
% 1.66/1.87 0 [] -abnormal(or1(f))| -abnormal(and1(h2(f))).
% 1.66/1.87 0 [] -abnormal(or1(f))| -abnormal(or1(h2(f))).
% 1.66/1.87 end_of_list.
% 1.66/1.87
% 1.66/1.87 SCAN INPUT: prop=0, horn=0, equality=0, symmetry=0, max_lits=4.
% 1.66/1.87
% 1.66/1.87 This is a non-Horn set without equality. The strategy will
% 1.66/1.87 be ordered hyper_res, unit deletion, and factoring, with
% 1.66/1.87 satellites in sos and with nuclei in usable.
% 1.66/1.87
% 1.66/1.87 dependent: set(hyper_res).
% 1.66/1.87 dependent: set(factor).
% 1.66/1.87 dependent: set(unit_deletion).
% 1.66/1.87
% 1.66/1.87 ------------> process usable:
% 1.66/1.87 ** KEPT (pick-wt=7): 1 [] -connection(A,B)| -zero(A)|zero(B).
% 1.66/1.87 ** KEPT (pick-wt=7): 2 [] -connection(A,B)| -one(A)|one(B).
% 1.66/1.87 ** KEPT (pick-wt=7): 3 [] -connection(A,B)| -zero(B)|zero(A).
% 1.66/1.87 ** KEPT (pick-wt=7): 4 [] -connection(A,B)| -one(B)|one(A).
% 1.66/1.87 ** KEPT (pick-wt=4): 5 [] -zero(A)| -one(A).
% 1.66/1.87 ** KEPT (pick-wt=8): 6 [] -and_ok(A)| -zero(in1(A))|zero(out1(A)).
% 1.66/1.87 ** KEPT (pick-wt=8): 7 [] -and_ok(A)| -zero(in2(A))|zero(out1(A)).
% 1.66/1.87 ** KEPT (pick-wt=11): 8 [] -and_ok(A)| -one(in1(A))| -one(in2(A))|one(out1(A)).
% 1.66/1.87 ** KEPT (pick-wt=11): 9 [] -and_ok(A)| -zero(out1(A))|zero(in1(A))|zero(in2(A)).
% 1.66/1.87 ** KEPT (pick-wt=8): 10 [] -and_ok(A)| -one(out1(A))|one(in1(A)).
% 1.66/1.87 ** KEPT (pick-wt=8): 11 [] -and_ok(A)| -one(out1(A))|one(in2(A)).
% 1.66/1.87 ** KEPT (pick-wt=4): 12 [] -and_ok(A)| -abnormal(A).
% 1.66/1.87 ** KEPT (pick-wt=6): 13 [] -logic_and(A)|and_ok(A)|abnormal(A).
% 1.66/1.87 ** KEPT (pick-wt=8): 14 [] -or_ok(A)| -one(in1(A))|one(out1(A)).
% 1.66/1.87 ** KEPT (pick-wt=8): 15 [] -or_ok(A)| -one(in2(A))|one(out1(A)).
% 1.66/1.87 ** KEPT (pick-wt=11): 16 [] -or_ok(A)| -zero(in1(A))| -zero(in2(A))|zero(out1(A)).
% 1.66/1.87 ** KEPT (pick-wt=11): 17 [] -or_ok(A)| -one(out1(A))|one(in1(A))|one(in2(A)).
% 1.66/1.87 ** KEPT (pick-wt=8): 18 [] -or_ok(A)| -zero(out1(A))|zero(in1(A)).
% 1.66/1.87 ** KEPT (pick-wt=8): 19 [] -or_ok(A)| -zero(out1(A))|zero(in2(A)).
% 1.66/1.87 ** KEPT (pick-wt=4): 20 [] -or_ok(A)| -abnormal(A).
% 1.66/1.87 ** KEPT (pick-wt=6): 21 [] -logic_or(A)|or_ok(A)|abnormal(A).
% 1.66/1.87 ** KEPT (pick-wt=8): 22 [] -not_ok(A)| -zero(in1(A))|one(out1(A)).
% 1.66/1.87 ** KEPT (pick-wt=8): 23 [] -not_ok(A)| -one(in1(A))|zero(out1(A)).
% 1.66/1.87 ** KEPT (pick-wt=8): 24 [] -not_ok(A)| -zero(out1(A))|one(in1(A)).
% 1.66/1.87 ** KEPT (pick-wt=8): 25 [] -not_ok(A)| -one(out1(A))|zero(in1(A)).
% 1.66/1.87 ** KEPT (pick-wt=4): 26 [] -not_ok(A)| -abnormal(A).
% 1.66/1.87 ** KEPT (pick-wt=6): 27 [] -logic_not(A)|not_ok(A)|abnormal(A).
% 1.66/1.87 ** KEPT (pick-wt=5): 28 [] -halfadder(A)|logic_and(and1(A)).
% 1.66/1.87 ** KEPT (pick-wt=5): 29 [] -halfadder(A)|logic_and(and2(A)).
% 1.66/1.87 ** KEPT (pick-wt=5): 30 [] -halfadder(A)|logic_not(not1(A)).
% 1.66/1.87 ** KEPT (pick-wt=5): 31 [] -halfadder(A)|logic_or(or1(A)).
% 1.66/1.87 ** KEPT (pick-wt=8): 32 [] -halfadder(A)|connection(in1(A),in1(or1(A))).
% 1.66/1.87 ** KEPT (pick-wt=8): 33 [] -halfadder(A)|connection(in2(A),in2(or1(A))).
% 1.66/1.87 ** KEPT (pick-wt=8): 34 [] -halfadder(A)|connection(in1(A),in1(and2(A))).
% 1.66/1.87 ** KEPT (pick-wt=8): 35 [] -halfadder(A)|connection(in2(A),in2(and2(A))).
% 1.66/1.87 ** KEPT (pick-wt=8): 36 [] -halfadder(A)|connection(outs(A),out1(and1(A))).
% 1.66/1.87 ** KEPT (pick-wt=8): 37 [] -halfadder(A)|connection(outc(A),out1(and2(A))).
% 1.66/1.87 ** KEPT (pick-wt=9): 38 [] -halfadder(A)|connection(out1(or1(A)),in1(and1(A))).
% 1.66/1.87 ** KEPT (pick-wt=9): 39 [] -halfadder(A)|connection(out1(and2(A)),in1(not1(A))).
% 1.66/1.87 ** KEPT (pick-wt=9): 40 [] -halfadder(A)|connection(out1(not1(A)),in2(and1(A))).
% 1.66/1.87 ** KEPT (pick-wt=5): 41 [] -fulladder(A)|halfadder(h1(A)).
% 1.66/1.87 ** KEPT (pick-wt=5): 42 [] -fulladder(A)|halfadder(h2(A)).
% 1.66/1.87 ** KEPT (pick-wt=5): 43 [] -fulladder(A)|logic_or(or1(A)).
% 1.66/1.87 ** KEPT (pick-wt=9): 44 [] -fulladder(A)|connection(outs(h1(A)),in2(h2(A))).
% 1.66/1.87 ** KEPT (pick-wt=9): 45 [] -fulladder(A)|connection(outc(h1(A)),in2(or1(A))).
% 1.66/1.87 ** KEPT (pick-wt=9): 46 [] -fulladder(A)|connection(outc(h2(A)),in1(or1(A))).
% 1.66/1.87 ** KEPT (pick-wt=8): 47 [] -fulladder(A)|connection(in1(A),in1(h2(A))).
% 1.66/1.87 ** KEPT (pick-wt=8): 48 [] -fulladder(A)|connection(in2(A),in1(h1(A))).
% 1.66/1.87 ** KEPT (pick-wt=8): 49 [] -fulladder(A)|connection(inc(A),in2(h1(A))).
% 1.66/1.87 ** KEPT (pick-wt=8): 50 [] -fulladder(A)|connection(outs(A),outs(h2(A))).
% 1.66/1.87 ** KEPT (pick-wt=8): 51 [] -fulladder(A)|connection(outc(A),out1(or1(A))).
% 1.66/1.87 ** KEPT (pick-wt=4): 52 [] -abnormal(and2(h1(f))).
% 1.66/1.87 ** KEPT (pick-wt=7): 53 [] -abnormal(or1(f))| -abnormal(and1(h1(f))).
% 1.66/1.87 ** KEPT (pick-wt=7): 54 [] -abnormal(or1(f))| -abnormal(not1(h1(f))).
% 1.66/1.87 ** KEPT (pick-wt=7): 55 [] -abnormal(or1(f))| -abnormal(and1(h2(f))).
% 1.66/1.87 ** KEPT (pick-wt=7): 56 [] -abnormal(or1(f))| -abnormal(or1(h2(f))).
% 1.66/1.87
% 1.66/1.87 ------------> process sos:
% 1.66/1.87 ** KEPT (pick-wt=2): 57 [] fulladder(f).
% 1.66/1.87 ** KEPT (pick-wt=3): 58 [] zero(in1(f)).
% 1.66/1.87 ** KEPT (pick-wt=3): 59 [] one(in2(f)).
% 1.66/1.87 ** KEPT (pick-wt=3): 60 [] one(inc(f)).
% 1.66/1.87 ** KEPT (pick-wt=3): 61 [] one(outs(f)).
% 1.66/1.87 ** KEPT (pick-wt=3): 62 [] zero(outc(f)).
% 1.66/1.87
% 1.66/1.87 ======= end of input processing =======
% 1.66/1.87
% 1.66/1.87 =========== start of search ===========
% 1.66/1.87
% 1.66/1.87 -------- PROOF --------
% 1.66/1.87
% 1.66/1.87 -----> EMPTY CLAUSE at 0.01 sec ----> 176 [hyper,174,53,128] $F.
% 1.66/1.87
% 1.66/1.87 Length of proof is 60. Level of proof is 15.
% 1.66/1.87
% 1.66/1.87 ---------------- PROOF ----------------
% 1.66/1.87 % SZS status Unsatisfiable
% 1.66/1.87 % SZS output start Refutation
% See solution above
% 1.66/1.87 ------------ end of proof -------------
% 1.66/1.87
% 1.66/1.87
% 1.66/1.87 Search stopped by max_proofs option.
% 1.66/1.87
% 1.66/1.87
% 1.66/1.87 Search stopped by max_proofs option.
% 1.66/1.87
% 1.66/1.87 ============ end of search ============
% 1.66/1.87
% 1.66/1.87 -------------- statistics -------------
% 1.66/1.87 clauses given 107
% 1.66/1.87 clauses generated 184
% 1.66/1.87 clauses kept 175
% 1.66/1.87 clauses forward subsumed 70
% 1.66/1.87 clauses back subsumed 30
% 1.66/1.87 Kbytes malloced 1953
% 1.66/1.87
% 1.66/1.87 ----------- times (seconds) -----------
% 1.66/1.87 user CPU time 0.01 (0 hr, 0 min, 0 sec)
% 1.66/1.87 system CPU time 0.00 (0 hr, 0 min, 0 sec)
% 1.66/1.87 wall-clock time 1 (0 hr, 0 min, 1 sec)
% 1.66/1.87
% 1.66/1.87 That finishes the proof of the theorem.
% 1.66/1.87
% 1.66/1.87 Process 26509 finished Wed Jul 27 06:42:52 2022
% 1.66/1.88 Otter interrupted
% 1.66/1.88 PROOF FOUND
%------------------------------------------------------------------------------