%------------------------------------------------------------------------------
% File : SOS---2.0
% Problem : HWV007-2 : TPTP v8.1.0. Bugfixed v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : sos-script %s
% Computer : n008.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 19:12:32 EDT 2022
% Result : Unsatisfiable 1.23s 1.44s
% Output : Refutation 1.23s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : HWV007-2 : TPTP v8.1.0. Bugfixed v2.7.0.
% 0.03/0.12 % Command : sos-script %s
% 0.12/0.33 % Computer : n008.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 : 600
% 0.12/0.33 % DateTime : Fri Jun 17 02:41:52 EDT 2022
% 0.12/0.33 % CPUTime :
% 0.19/0.35 ----- Otter 3.2, August 2001 -----
% 0.19/0.35 The process was started by sandbox on n008.cluster.edu,
% 0.19/0.35 Fri Jun 17 02:41:52 2022
% 0.19/0.35 The command was "./sos". The process ID is 10825.
% 0.19/0.35
% 0.19/0.35 set(prolog_style_variables).
% 0.19/0.35 set(auto).
% 0.19/0.35 dependent: set(auto1).
% 0.19/0.35 dependent: set(process_input).
% 0.19/0.35 dependent: clear(print_kept).
% 0.19/0.35 dependent: clear(print_new_demod).
% 0.19/0.35 dependent: clear(print_back_demod).
% 0.19/0.35 dependent: clear(print_back_sub).
% 0.19/0.35 dependent: set(control_memory).
% 0.19/0.35 dependent: assign(max_mem, 12000).
% 0.19/0.35 dependent: assign(pick_given_ratio, 4).
% 0.19/0.35 dependent: assign(stats_level, 1).
% 0.19/0.35 dependent: assign(pick_semantic_ratio, 3).
% 0.19/0.35 dependent: assign(sos_limit, 5000).
% 0.19/0.35 dependent: assign(max_weight, 60).
% 0.19/0.35 clear(print_given).
% 0.19/0.35
% 0.19/0.35 list(usable).
% 0.19/0.35
% 0.19/0.35 SCAN INPUT: prop=0, horn=0, equality=0, symmetry=0, max_lits=4.
% 0.19/0.35
% 0.19/0.35 This is a non-Horn set without equality. The strategy
% 0.19/0.35 will be ordered hyper_res, ur_res, unit deletion, and
% 0.19/0.35 factoring, with satellites in sos and nuclei in usable.
% 0.19/0.35
% 0.19/0.35 dependent: set(hyper_res).
% 0.19/0.35 dependent: set(factor).
% 0.19/0.35 dependent: set(unit_deletion).
% 0.19/0.35
% 0.19/0.35 ------------> process usable:
% 0.19/0.35
% 0.19/0.35 ------------> process sos:
% 0.19/0.35
% 0.19/0.35 ======= end of input processing =======
% 0.19/0.39
% 0.19/0.39 Model 1 (0.00 seconds, 0 Inserts)
% 0.19/0.39
% 0.19/0.39 Stopped by limit on number of solutions
% 0.19/0.39
% 0.19/0.39
% 0.19/0.39 -------------- Softie stats --------------
% 0.19/0.39
% 0.19/0.39 UPDATE_STOP: 300
% 0.19/0.39 SFINDER_TIME_LIMIT: 2
% 0.19/0.39 SHORT_CLAUSE_CUTOFF: 4
% 0.19/0.39 number of clauses in intial UL: 56
% 0.19/0.39 number of clauses initially in problem: 62
% 0.19/0.39 percentage of clauses intially in UL: 90
% 0.19/0.39 percentage of distinct symbols occuring in initial UL: 100
% 0.19/0.39 percent of all initial clauses that are short: 100
% 0.19/0.39 absolute distinct symbol count: 25
% 0.19/0.39 distinct predicate count: 12
% 0.19/0.39 distinct function count: 12
% 0.19/0.39 distinct constant count: 1
% 0.19/0.39
% 0.19/0.39 ---------- no more Softie stats ----------
% 0.19/0.39
% 0.19/0.39
% 0.19/0.39
% 0.19/0.39 Model 2 (0.00 seconds, 0 Inserts)
% 0.19/0.39
% 0.19/0.39 Stopped by limit on number of solutions
% 0.19/0.39
% 0.19/0.39 =========== start of search ===========
% 1.23/1.44
% 1.23/1.44 -------- PROOF --------
% 1.23/1.44 % SZS status Unsatisfiable
% 1.23/1.44 % SZS output start Refutation
% 1.23/1.44
% 1.23/1.44 Model 3 (0.00 seconds, 0 Inserts)
% 1.23/1.44
% 1.23/1.44 Stopped by limit on number of solutions
% 1.23/1.44
% 1.23/1.44 Stopped by limit on insertions
% 1.23/1.44
% 1.23/1.44 Model 4 [ 2 1 1056 ] (0.00 seconds, 250000 Inserts)
% 1.23/1.44
% 1.23/1.44 Stopped by limit on insertions
% 1.23/1.44
% 1.23/1.44 Model 5 [ 2 0 1061 ] (0.00 seconds, 250000 Inserts)
% 1.23/1.44
% 1.23/1.44 Stopped by limit on insertions
% 1.23/1.44
% 1.23/1.44 Model 6 [ 3 0 1259 ] (0.00 seconds, 250000 Inserts)
% 1.23/1.44
% 1.23/1.44 Stopped by limit on insertions
% 1.23/1.44
% 1.23/1.44 Model 7 [ 3 1 263 ] (0.00 seconds, 250000 Inserts)
% 1.23/1.44
% 1.23/1.44 Stopped by limit on insertions
% 1.23/1.44
% 1.23/1.44 Model 8 [ 4 9 79515 ] (0.00 seconds, 250000 Inserts)
% 1.23/1.44
% 1.23/1.44 Stopped by limit on insertions
% 1.23/1.44
% 1.23/1.44 Model 9 [ 3 1 107 ] (0.00 seconds, 250000 Inserts)
% 1.23/1.44
% 1.23/1.44 Stopped by limit on insertions
% 1.23/1.44
% 1.23/1.44 Model 10 [ 6 0 2563 ] (0.00 seconds, 250000 Inserts)
% 1.23/1.44
% 1.23/1.44 Stopped by limit on insertions
% 1.23/1.44
% 1.23/1.44 Model 11 [ 8 0 106 ] (0.00 seconds, 250000 Inserts)
% 1.23/1.44
% 1.23/1.44 Stopped by limit on insertions
% 1.23/1.44
% 1.23/1.44 Model 12 [ 2 1 2097 ] (0.00 seconds, 250000 Inserts)
% 1.23/1.44
% 1.23/1.44 Stopped by limit on insertions
% 1.23/1.44
% 1.23/1.44 Model 13 [ 9 0 106 ] (0.00 seconds, 250000 Inserts)
% 1.23/1.44
% 1.23/1.44 Stopped by limit on insertions
% 1.23/1.44
% 1.23/1.44 Model 14 [ 9 1 439 ] (0.00 seconds, 250000 Inserts)
% 1.23/1.44
% 1.23/1.44 Stopped by limit on insertions
% 1.23/1.44
% 1.23/1.44 Model 15 [ 7 1 1109 ] (0.00 seconds, 250000 Inserts)
% 1.23/1.44
% 1.23/1.44 Stopped by limit on insertions
% 1.23/1.44
% 1.23/1.44 Model 16 [ 7 0 628 ] (0.00 seconds, 250000 Inserts)
% 1.23/1.44
% 1.23/1.44 Stopped by limit on insertions
% 1.23/1.44
% 1.23/1.44 Model 17 [ 8 1 1458 ] (0.00 seconds, 250000 Inserts)
% 1.23/1.44
% 1.23/1.44 Stopped by limit on insertions
% 1.23/1.44
% 1.23/1.44 Model 18 [ 10 0 992 ] (0.00 seconds, 250000 Inserts)
% 1.23/1.44
% 1.23/1.44 Stopped by limit on insertions
% 1.23/1.44
% 1.23/1.44 Model 19 [ 11 0 1368 ] (0.00 seconds, 250000 Inserts)
% 1.23/1.44
% 1.23/1.44 Stopped by limit on insertions
% 1.23/1.44
% 1.23/1.44 Model 20 [ 8 0 3240 ] (0.00 seconds, 250000 Inserts)
% 1.23/1.44
% 1.23/1.44 Stopped by limit on insertions
% 1.23/1.44
% 1.23/1.44 Model 21 [ 8 1 1158 ] (0.00 seconds, 250000 Inserts)
% 1.23/1.44
% 1.23/1.44 Stopped by limit on insertions
% 1.23/1.44
% 1.23/1.44 Model 22 [ 9 1 1119 ] (0.00 seconds, 250000 Inserts)
% 1.23/1.44
% 1.23/1.44 Stopped by limit on insertions
% 1.23/1.44
% 1.23/1.44 Model 23 [ 6 1 2025 ] (0.00 seconds, 250000 Inserts)
% 1.23/1.44
% 1.23/1.44 -----> EMPTY CLAUSE at 1.06 sec ----> 176 [hyper,174,53,131] {-} $F.
% 1.23/1.44
% 1.23/1.44 Length of proof is 60. Level of proof is 14.
% 1.23/1.44
% 1.23/1.44 ---------------- PROOF ----------------
% 1.23/1.44 % SZS status Unsatisfiable
% 1.23/1.44 % SZS output start Refutation
% 1.23/1.44
% 1.23/1.44 1 [] {+} -connection(A,B)| -zero(A)|zero(B).
% 1.23/1.44 2 [] {+} -connection(A,B)| -one(A)|one(B).
% 1.23/1.44 3 [] {+} -connection(A,B)| -zero(B)|zero(A).
% 1.23/1.44 4 [] {+} -connection(A,B)| -one(B)|one(A).
% 1.23/1.44 5 [] {+} -zero(A)| -one(A).
% 1.23/1.44 7 [] {+} -and_ok(A)| -zero(in2(A))|zero(out1(A)).
% 1.23/1.44 8 [] {+} -and_ok(A)| -one(in1(A))| -one(in2(A))|one(out1(A)).
% 1.23/1.44 10 [] {+} -and_ok(A)| -one(out1(A))|one(in1(A)).
% 1.23/1.44 13 [] {+} -logic_and(A)|and_ok(A)|abnormal(A).
% 1.23/1.44 17 [] {+} -or_ok(A)| -one(out1(A))|one(in1(A))|one(in2(A)).
% 1.23/1.44 19 [] {+} -or_ok(A)| -zero(out1(A))|zero(in2(A)).
% 1.23/1.44 21 [] {+} -logic_or(A)|or_ok(A)|abnormal(A).
% 1.23/1.44 23 [] {+} -not_ok(A)| -one(in1(A))|zero(out1(A)).
% 1.23/1.44 27 [] {+} -logic_not(A)|not_ok(A)|abnormal(A).
% 1.23/1.44 28 [] {+} -halfadder(A)|logic_and(and1(A)).
% 1.23/1.44 29 [] {+} -halfadder(A)|logic_and(and2(A)).
% 1.23/1.44 30 [] {+} -halfadder(A)|logic_not(not1(A)).
% 1.23/1.44 31 [] {+} -halfadder(A)|logic_or(or1(A)).
% 1.23/1.44 32 [] {+} -halfadder(A)|connection(in1(A),in1(or1(A))).
% 1.23/1.44 33 [] {+} -halfadder(A)|connection(in2(A),in2(or1(A))).
% 1.23/1.44 34 [] {+} -halfadder(A)|connection(in1(A),in1(and2(A))).
% 1.23/1.44 35 [] {+} -halfadder(A)|connection(in2(A),in2(and2(A))).
% 1.23/1.44 36 [] {+} -halfadder(A)|connection(outs(A),out1(and1(A))).
% 1.23/1.44 37 [] {+} -halfadder(A)|connection(outc(A),out1(and2(A))).
% 1.23/1.44 38 [] {+} -halfadder(A)|connection(out1(or1(A)),in1(and1(A))).
% 1.23/1.44 39 [] {+} -halfadder(A)|connection(out1(and2(A)),in1(not1(A))).
% 1.23/1.44 40 [] {+} -halfadder(A)|connection(out1(not1(A)),in2(and1(A))).
% 1.23/1.44 41 [] {+} -fulladder(A)|halfadder(h1(A)).
% 1.23/1.44 42 [] {+} -fulladder(A)|halfadder(h2(A)).
% 1.23/1.44 43 [] {+} -fulladder(A)|logic_or(or1(A)).
% 1.23/1.44 44 [] {+} -fulladder(A)|connection(outs(h1(A)),in2(h2(A))).
% 1.23/1.44 45 [] {+} -fulladder(A)|connection(outc(h1(A)),in2(or1(A))).
% 1.23/1.44 47 [] {+} -fulladder(A)|connection(in1(A),in1(h2(A))).
% 1.23/1.44 48 [] {+} -fulladder(A)|connection(in2(A),in1(h1(A))).
% 1.23/1.44 49 [] {+} -fulladder(A)|connection(inc(A),in2(h1(A))).
% 1.23/1.44 50 [] {+} -fulladder(A)|connection(outs(A),outs(h2(A))).
% 1.23/1.44 51 [] {+} -fulladder(A)|connection(outc(A),out1(or1(A))).
% 1.23/1.44 52 [] {+} -abnormal(and2(h1(f))).
% 1.23/1.44 53 [] {+} -abnormal(or1(f))| -abnormal(and1(h1(f))).
% 1.23/1.44 54 [] {+} -abnormal(or1(f))| -abnormal(not1(h1(f))).
% 1.23/1.44 55 [] {+} -abnormal(or1(f))| -abnormal(and1(h2(f))).
% 1.23/1.44 56 [] {+} -abnormal(or1(f))| -abnormal(or1(h2(f))).
% 1.23/1.44 57 [] {+} fulladder(f).
% 1.23/1.44 58 [] {+} zero(in1(f)).
% 1.23/1.44 59 [] {+} one(in2(f)).
% 1.23/1.44 60 [] {+} one(inc(f)).
% 1.23/1.44 61 [] {+} one(outs(f)).
% 1.23/1.44 62 [] {+} zero(outc(f)).
% 1.23/1.44 63 [hyper,57,51] {-} connection(outc(f),out1(or1(f))).
% 1.23/1.44 64 [hyper,57,50] {-} connection(outs(f),outs(h2(f))).
% 1.23/1.44 65 [hyper,57,49] {+} connection(inc(f),in2(h1(f))).
% 1.23/1.44 66 [hyper,57,48] {-} connection(in2(f),in1(h1(f))).
% 1.23/1.44 67 [hyper,57,47] {-} connection(in1(f),in1(h2(f))).
% 1.23/1.44 69 [hyper,57,45] {-} connection(outc(h1(f)),in2(or1(f))).
% 1.23/1.44 70 [hyper,57,44] {-} connection(outs(h1(f)),in2(h2(f))).
% 1.23/1.44 71 [hyper,57,43] {+} logic_or(or1(f)).
% 1.23/1.44 72 [hyper,57,42] {+} halfadder(h2(f)).
% 1.23/1.44 73 [hyper,57,41] {+} halfadder(h1(f)).
% 1.23/1.44 74 [hyper,71,21] {+} or_ok(or1(f))|abnormal(or1(f)).
% 1.23/1.44 75 [hyper,64,2,61] {+} one(outs(h2(f))).
% 1.23/1.44 78 [hyper,72,38] {+} connection(out1(or1(h2(f))),in1(and1(h2(f)))).
% 1.23/1.44 80 [hyper,72,36] {+} connection(outs(h2(f)),out1(and1(h2(f)))).
% 1.23/1.44 83 [hyper,72,33] {-} connection(in2(h2(f)),in2(or1(h2(f)))).
% 1.23/1.44 84 [hyper,72,32] {+} connection(in1(h2(f)),in1(or1(h2(f)))).
% 1.23/1.44 85 [hyper,72,31] {+} logic_or(or1(h2(f))).
% 1.23/1.44 88 [hyper,72,28] {+} logic_and(and1(h2(f))).
% 1.23/1.44 89 [hyper,63,1,62] {+} zero(out1(or1(f))).
% 1.23/1.44 90 [hyper,73,40] {-} connection(out1(not1(h1(f))),in2(and1(h1(f)))).
% 1.23/1.44 91 [hyper,73,39] {+} connection(out1(and2(h1(f))),in1(not1(h1(f)))).
% 1.23/1.44 93 [hyper,73,37] {+} connection(outc(h1(f)),out1(and2(h1(f)))).
% 1.23/1.44 94 [hyper,73,36] {-} connection(outs(h1(f)),out1(and1(h1(f)))).
% 1.23/1.44 95 [hyper,73,35] {-} connection(in2(h1(f)),in2(and2(h1(f)))).
% 1.23/1.44 96 [hyper,73,34] {-} connection(in1(h1(f)),in1(and2(h1(f)))).
% 1.23/1.44 100 [hyper,73,30] {+} logic_not(not1(h1(f))).
% 1.23/1.44 101 [hyper,73,29] {+} logic_and(and2(h1(f))).
% 1.23/1.44 102 [hyper,73,28] {+} logic_and(and1(h1(f))).
% 1.23/1.44 103 [hyper,85,21] {+} or_ok(or1(h2(f)))|abnormal(or1(h2(f))).
% 1.23/1.44 105 [hyper,65,2,60] {+} one(in2(h1(f))).
% 1.23/1.44 107 [hyper,88,13] {+} and_ok(and1(h2(f)))|abnormal(and1(h2(f))).
% 1.23/1.44 109 [hyper,100,27] {+} not_ok(not1(h1(f)))|abnormal(not1(h1(f))).
% 1.23/1.44 110 [hyper,66,2,59] {+} one(in1(h1(f))).
% 1.23/1.44 111 [hyper,102,13] {+} and_ok(and1(h1(f)))|abnormal(and1(h1(f))).
% 1.23/1.44 112 [hyper,67,1,58] {+} zero(in1(h2(f))).
% 1.23/1.44 113 [hyper,101,13,unit_del,52] {+} and_ok(and2(h1(f))).
% 1.23/1.44 114 [hyper,74,19,89] {-} abnormal(or1(f))|zero(in2(or1(f))).
% 1.23/1.44 116 [hyper,114,3,69] {-} abnormal(or1(f))|zero(outc(h1(f))).
% 1.23/1.44 118 [hyper,95,2,105] {+} one(in2(and2(h1(f)))).
% 1.23/1.44 119 [hyper,96,2,110] {+} one(in1(and2(h1(f)))).
% 1.23/1.44 122 [hyper,119,8,113,118] {+} one(out1(and2(h1(f)))).
% 1.23/1.44 125 [hyper,80,2,75] {+} one(out1(and1(h2(f)))).
% 1.23/1.44 127 [hyper,84,1,112] {-} zero(in1(or1(h2(f)))).
% 1.23/1.44 128 [hyper,91,2,122] {+} one(in1(not1(h1(f)))).
% 1.23/1.44 129 [hyper,93,4,122] {+} one(outc(h1(f))).
% 1.23/1.44 131 [hyper,129,5,116] {+} abnormal(or1(f)).
% 1.23/1.44 139 [hyper,107,10,125] {+} abnormal(and1(h2(f)))|one(in1(and1(h2(f)))).
% 1.23/1.44 141 [hyper,109,23,128] {+} abnormal(not1(h1(f)))|zero(out1(not1(h1(f)))).
% 1.23/1.44 144 [hyper,139,4,78] {+} abnormal(and1(h2(f)))|one(out1(or1(h2(f)))).
% 1.23/1.44 146 [hyper,141,1,90] {+} abnormal(not1(h1(f)))|zero(in2(and1(h1(f)))).
% 1.23/1.44 148 [hyper,144,17,103] {+} abnormal(and1(h2(f)))|one(in1(or1(h2(f))))|one(in2(or1(h2(f))))|abnormal(or1(h2(f))).
% 1.23/1.44 149 [hyper,146,7,111] {+} abnormal(not1(h1(f)))|zero(out1(and1(h1(f))))|abnormal(and1(h1(f))).
% 1.23/1.44 151 [hyper,148,5,127] {+} abnormal(and1(h2(f)))|one(in2(or1(h2(f))))|abnormal(or1(h2(f))).
% 1.23/1.44 153 [hyper,149,3,94] {+} abnormal(not1(h1(f)))|abnormal(and1(h1(f)))|zero(outs(h1(f))).
% 1.23/1.44 154 [hyper,153,1,70] {+} abnormal(not1(h1(f)))|abnormal(and1(h1(f)))|zero(in2(h2(f))).
% 1.23/1.44 158 [hyper,151,4,83] {+} abnormal(and1(h2(f)))|abnormal(or1(h2(f)))|one(in2(h2(f))).
% 1.23/1.44 160 [hyper,158,5,154] {+} abnormal(and1(h2(f)))|abnormal(or1(h2(f)))|abnormal(not1(h1(f)))|abnormal(and1(h1(f))).
% 1.23/1.44 167 [hyper,160,55,131] {+} abnormal(or1(h2(f)))|abnormal(not1(h1(f)))|abnormal(and1(h1(f))).
% 1.23/1.44 171 [hyper,167,56,131] {+} abnormal(not1(h1(f)))|abnormal(and1(h1(f))).
% 1.23/1.44 174 [hyper,171,54,131] {+} abnormal(and1(h1(f))).
% 1.23/1.44 176 [hyper,174,53,131] {-} $F.
% 1.23/1.44
% 1.23/1.44 % SZS output end Refutation
% 1.23/1.44 ------------ end of proof -------------
% 1.23/1.44
% 1.23/1.44
% 1.23/1.44 Search stopped by max_proofs option.
% 1.23/1.44
% 1.23/1.44
% 1.23/1.44 Search stopped by max_proofs option.
% 1.23/1.44
% 1.23/1.44 ============ end of search ============
% 1.23/1.44
% 1.23/1.44 ----------- soft-scott stats ----------
% 1.23/1.44
% 1.23/1.44 true clauses given 57 (52.8%)
% 1.23/1.44 false clauses given 51
% 1.23/1.44
% 1.23/1.44 FALSE TRUE
% 1.23/1.44 4 0 1
% 1.23/1.44 tot: 0 1 (100.0% true)
% 1.23/1.44
% 1.23/1.44
% 1.23/1.44 Model 23 [ 6 1 2025 ] (0.00 seconds, 250000 Inserts)
% 1.23/1.44
% 1.23/1.44 That finishes the proof of the theorem.
% 1.23/1.44
% 1.23/1.44 Process 10825 finished Fri Jun 17 02:41:53 2022
%------------------------------------------------------------------------------