%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : HWV035-2 : TPTP v8.1.0. Bugfixed v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : bliksem %s
% Computer : n003.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 : 0s
% DateTime : Sat Jul 16 13:11:58 EDT 2022
% Result : Satisfiable 0.70s 1.09s
% Output : Saturation 0.70s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : HWV035-2 : TPTP v8.1.0. Bugfixed v2.7.0.
% 0.03/0.13 % Command : bliksem %s
% 0.13/0.34 % Computer : n003.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % DateTime : Fri Jun 17 01:27:57 EDT 2022
% 0.13/0.34 % CPUTime :
% 0.70/1.09 *** allocated 10000 integers for termspace/termends
% 0.70/1.09 *** allocated 10000 integers for clauses
% 0.70/1.09 *** allocated 10000 integers for justifications
% 0.70/1.09 Bliksem 1.12
% 0.70/1.09
% 0.70/1.09
% 0.70/1.09 Automatic Strategy Selection
% 0.70/1.09
% 0.70/1.09 Clauses:
% 0.70/1.09 [
% 0.70/1.09 [ ~( connection( X, Y ) ), ~( zero( X ) ), zero( Y ) ],
% 0.70/1.09 [ ~( connection( X, Y ) ), ~( one( X ) ), one( Y ) ],
% 0.70/1.09 [ ~( connection( X, Y ) ), ~( zero( Y ) ), zero( X ) ],
% 0.70/1.09 [ ~( connection( X, Y ) ), ~( one( Y ) ), one( X ) ],
% 0.70/1.09 [ ~( zero( X ) ), ~( one( X ) ) ],
% 0.70/1.09 [ ~( 'and_ok'( X ) ), ~( zero( in1( X ) ) ), zero( out1( X ) ) ],
% 0.70/1.09 [ ~( 'and_ok'( X ) ), ~( zero( in2( X ) ) ), zero( out1( X ) ) ],
% 0.70/1.09 [ ~( 'and_ok'( X ) ), ~( one( in1( X ) ) ), ~( one( in2( X ) ) ), one(
% 0.70/1.09 out1( X ) ) ],
% 0.70/1.09 [ ~( 'and_ok'( X ) ), ~( zero( out1( X ) ) ), zero( in1( X ) ), zero(
% 0.70/1.09 in2( X ) ) ],
% 0.70/1.09 [ ~( 'and_ok'( X ) ), ~( one( out1( X ) ) ), one( in1( X ) ) ],
% 0.70/1.09 [ ~( 'and_ok'( X ) ), ~( one( out1( X ) ) ), one( in2( X ) ) ],
% 0.70/1.09 [ ~( 'and_ok'( X ) ), ~( abnormal( X ) ) ],
% 0.70/1.09 [ ~( 'logic_and'( X ) ), 'and_ok'( X ), abnormal( X ) ],
% 0.70/1.09 [ ~( 'or_ok'( X ) ), ~( one( in1( X ) ) ), one( out1( X ) ) ],
% 0.70/1.09 [ ~( 'or_ok'( X ) ), ~( one( in2( X ) ) ), one( out1( X ) ) ],
% 0.70/1.09 [ ~( 'or_ok'( X ) ), ~( zero( in1( X ) ) ), ~( zero( in2( X ) ) ), zero(
% 0.70/1.09 out1( X ) ) ],
% 0.70/1.09 [ ~( 'or_ok'( X ) ), ~( one( out1( X ) ) ), one( in1( X ) ), one( in2( X
% 0.70/1.09 ) ) ],
% 0.70/1.09 [ ~( 'or_ok'( X ) ), ~( zero( out1( X ) ) ), zero( in1( X ) ) ],
% 0.70/1.09 [ ~( 'or_ok'( X ) ), ~( zero( out1( X ) ) ), zero( in2( X ) ) ],
% 0.70/1.09 [ ~( 'or_ok'( X ) ), ~( abnormal( X ) ) ],
% 0.70/1.09 [ ~( 'logic_or'( X ) ), 'or_ok'( X ), abnormal( X ) ],
% 0.70/1.09 [ ~( 'not_ok'( X ) ), ~( zero( in1( X ) ) ), one( out1( X ) ) ],
% 0.70/1.09 [ ~( 'not_ok'( X ) ), ~( one( in1( X ) ) ), zero( out1( X ) ) ],
% 0.70/1.09 [ ~( 'not_ok'( X ) ), ~( zero( out1( X ) ) ), one( in1( X ) ) ],
% 0.70/1.09 [ ~( 'not_ok'( X ) ), ~( one( out1( X ) ) ), zero( in1( X ) ) ],
% 0.70/1.09 [ ~( 'not_ok'( X ) ), ~( abnormal( X ) ) ],
% 0.70/1.09 [ ~( 'logic_not'( X ) ), 'not_ok'( X ), abnormal( X ) ],
% 0.70/1.09 [ ~( halfadder( X ) ), 'logic_and'( and1( X ) ) ],
% 0.70/1.09 [ ~( halfadder( X ) ), 'logic_and'( and2( X ) ) ],
% 0.70/1.09 [ ~( halfadder( X ) ), 'logic_not'( not1( X ) ) ],
% 0.70/1.09 [ ~( halfadder( X ) ), 'logic_or'( or1( X ) ) ],
% 0.70/1.09 [ ~( halfadder( X ) ), connection( in1( X ), in1( or1( X ) ) ) ],
% 0.70/1.09 [ ~( halfadder( X ) ), connection( in2( X ), in2( or1( X ) ) ) ],
% 0.70/1.09 [ ~( halfadder( X ) ), connection( in1( X ), in1( and2( X ) ) ) ],
% 0.70/1.09 [ ~( halfadder( X ) ), connection( in2( X ), in2( and2( X ) ) ) ],
% 0.70/1.09 [ ~( halfadder( X ) ), connection( outs( X ), out1( and1( X ) ) ) ],
% 0.70/1.09 [ ~( halfadder( X ) ), connection( outc( X ), out1( and2( X ) ) ) ],
% 0.70/1.09 [ ~( halfadder( X ) ), connection( out1( or1( X ) ), in1( and1( X ) ) )
% 0.70/1.09 ],
% 0.70/1.09 [ ~( halfadder( X ) ), connection( out1( and2( X ) ), in1( not1( X ) ) )
% 0.70/1.09 ],
% 0.70/1.09 [ ~( halfadder( X ) ), connection( out1( not1( X ) ), in2( and1( X ) ) )
% 0.70/1.09 ]
% 0.70/1.09 ] .
% 0.70/1.09
% 0.70/1.09
% 0.70/1.09 percentage equality = 0.000000, percentage horn = 0.875000
% 0.70/1.09 This a non-horn, non-equality problem
% 0.70/1.09
% 0.70/1.09
% 0.70/1.09 Options Used:
% 0.70/1.09
% 0.70/1.09 useres = 1
% 0.70/1.09 useparamod = 0
% 0.70/1.09 useeqrefl = 0
% 0.70/1.09 useeqfact = 0
% 0.70/1.09 usefactor = 1
% 0.70/1.09 usesimpsplitting = 0
% 0.70/1.09 usesimpdemod = 0
% 0.70/1.09 usesimpres = 3
% 0.70/1.09
% 0.70/1.09 resimpinuse = 1000
% 0.70/1.09 resimpclauses = 20000
% 0.70/1.09 substype = standard
% 0.70/1.09 backwardsubs = 1
% 0.70/1.09 selectoldest = 5
% 0.70/1.09
% 0.70/1.09 litorderings [0] = split
% 0.70/1.09 litorderings [1] = liftord
% 0.70/1.09
% 0.70/1.09 termordering = none
% 0.70/1.09
% 0.70/1.09 litapriori = 1
% 0.70/1.09 termapriori = 0
% 0.70/1.09 litaposteriori = 0
% 0.70/1.09 termaposteriori = 0
% 0.70/1.09 demodaposteriori = 0
% 0.70/1.09 ordereqreflfact = 0
% 0.70/1.09
% 0.70/1.09 litselect = none
% 0.70/1.09
% 0.70/1.09 maxweight = 15
% 0.70/1.09 maxdepth = 30000
% 0.70/1.09 maxlength = 115
% 0.70/1.09 maxnrvars = 195
% 0.70/1.09 excuselevel = 1
% 0.70/1.09 increasemaxweight = 1
% 0.70/1.09
% 0.70/1.09 maxselected = 10000000
% 0.70/1.09 maxnrclauses = 10000000
% 0.70/1.09
% 0.70/1.09 showgenerated = 0
% 0.70/1.09 showkept = 0
% 0.70/1.09 showselected = 0
% 0.70/1.09 showdeleted = 0
% 0.70/1.09 showresimp = 1
% 0.70/1.09 showstatus = 2000
% 0.70/1.09
% 0.70/1.09 prologoutput = 1
% 0.70/1.09 nrgoals = 5000000
% 0.70/1.09 totalproof = 1
% 0.70/1.09
% 0.70/1.09 Symbols occurring in the translation:
% 0.70/1.09
% 0.70/1.09 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 0.70/1.09 . [1, 2] (w:1, o:38, a:1, s:1, b:0),
% 0.70/1.09 ! [4, 1] (w:0, o:14, a:1, s:1, b:0),
% 0.70/1.09 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 0.70/1.09 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 0.70/1.09 connection [41, 2] (w:1, o:63, a:1, s:1, b:0),
% 0.70/1.09 zero [42, 1] (w:1, o:19, a:1, s:1, b:0),
% 0.70/1.09 one [43, 1] (w:1, o:22, a:1, s:1, b:0),
% 0.70/1.09 'and_ok' [46, 1] (w:1, o:23, a:1, s:1, b:0),
% 0.70/1.09 in1 [47, 1] (w:1, o:25, a:1, s:1, b:0),
% 0.70/1.09 out1 [48, 1] (w:1, o:26, a:1, s:1, b:0),
% 0.70/1.09 in2 [49, 1] (w:1, o:27, a:1, s:1, b:0),
% 0.70/1.09 abnormal [50, 1] (w:1, o:28, a:1, s:1, b:0),
% 0.70/1.09 'logic_and' [51, 1] (w:1, o:29, a:1, s:1, b:0),
% 0.70/1.09 'or_ok' [52, 1] (w:1, o:30, a:1, s:1, b:0),
% 0.70/1.09 'logic_or' [53, 1] (w:1, o:32, a:1, s:1, b:0),
% 0.70/1.09 'not_ok' [54, 1] (w:1, o:20, a:1, s:1, b:0),
% 0.70/1.09 'logic_not' [55, 1] (w:1, o:31, a:1, s:1, b:0),
% 0.70/1.09 halfadder [57, 1] (w:1, o:24, a:1, s:1, b:0),
% 0.70/1.09 and1 [58, 1] (w:1, o:33, a:1, s:1, b:0),
% 0.70/1.09 and2 [59, 1] (w:1, o:34, a:1, s:1, b:0),
% 0.70/1.09 not1 [60, 1] (w:1, o:21, a:1, s:1, b:0),
% 0.70/1.09 or1 [61, 1] (w:1, o:35, a:1, s:1, b:0),
% 0.70/1.09 outs [62, 1] (w:1, o:36, a:1, s:1, b:0),
% 0.70/1.09 outc [63, 1] (w:1, o:37, a:1, s:1, b:0).
% 0.70/1.09
% 0.70/1.09
% 0.70/1.09 Starting Search:
% 0.70/1.09
% 0.70/1.09 Resimplifying inuse:
% 0.70/1.09 Done
% 0.70/1.09
% 0.70/1.09 Failed to find proof!
% 0.70/1.09 maxweight = 15
% 0.70/1.09 maxnrclauses = 10000000
% 0.70/1.09 Generated: 105
% 0.70/1.09 Kept: 96
% 0.70/1.09
% 0.70/1.09
% 0.70/1.09 The strategy used was not complete!
% 0.70/1.09
% 0.70/1.09 Increased maxweight to 16
% 0.70/1.09
% 0.70/1.09 Starting Search:
% 0.70/1.09
% 0.70/1.09 Resimplifying inuse:
% 0.70/1.09 Done
% 0.70/1.09
% 0.70/1.09 Failed to find proof!
% 0.70/1.09 maxweight = 16
% 0.70/1.09 maxnrclauses = 10000000
% 0.70/1.09 Generated: 105
% 0.70/1.09 Kept: 96
% 0.70/1.09
% 0.70/1.09
% 0.70/1.09 The strategy used was not complete!
% 0.70/1.09
% 0.70/1.09 Increased maxweight to 17
% 0.70/1.09
% 0.70/1.09 Starting Search:
% 0.70/1.09
% 0.70/1.09 Resimplifying inuse:
% 0.70/1.09 Done
% 0.70/1.09
% 0.70/1.09
% 0.70/1.09
% 0.70/1.09 found a saturation!
% 0.70/1.09 % SZS status Satisfiable
% 0.70/1.09 % SZS output start Saturation
% 0.70/1.09
% 0.70/1.09 clause( 99, [ one( in1( or1( X ) ) ), ~( one( out1( or1( X ) ) ) ), one(
% 0.70/1.09 in2( or1( X ) ) ), ~( 'not_ok'( or1( X ) ) ), ~( halfadder( X ) ) ] )
% 0.70/1.09 .
% 0.70/1.09 clause( 92, [ zero( in1( or1( X ) ) ), ~( zero( out1( or1( X ) ) ) ), ~(
% 0.70/1.09 'and_ok'( or1( X ) ) ), ~( halfadder( X ) ) ] )
% 0.70/1.09 .
% 0.70/1.09 clause( 95, [ one( out1( or1( X ) ) ), ~( one( in2( or1( X ) ) ) ), ~(
% 0.70/1.09 'not_ok'( or1( X ) ) ), ~( halfadder( X ) ) ] )
% 0.70/1.09 .
% 0.70/1.09 clause( 90, [ ~( zero( out1( or1( X ) ) ) ), zero( in2( or1( X ) ) ), ~(
% 0.70/1.09 'and_ok'( or1( X ) ) ), ~( halfadder( X ) ) ] )
% 0.70/1.09 .
% 0.70/1.09 clause( 94, [ one( out1( or1( X ) ) ), ~( one( in2( or1( X ) ) ) ), ~(
% 0.70/1.09 'and_ok'( or1( X ) ) ), ~( halfadder( X ) ) ] )
% 0.70/1.09 .
% 0.70/1.09 clause( 97, [ ~( one( in1( or1( X ) ) ) ), one( out1( or1( X ) ) ), ~(
% 0.70/1.09 'not_ok'( or1( X ) ) ), ~( halfadder( X ) ) ] )
% 0.70/1.09 .
% 0.70/1.09 clause( 96, [ ~( one( in1( or1( X ) ) ) ), one( out1( or1( X ) ) ), ~(
% 0.70/1.09 'and_ok'( or1( X ) ) ), ~( halfadder( X ) ) ] )
% 0.70/1.09 .
% 0.70/1.09 clause( 98, [ ~( zero( in1( or1( X ) ) ) ), ~( zero( in2( or1( X ) ) ) ),
% 0.70/1.09 ~( 'not_ok'( or1( X ) ) ), ~( halfadder( X ) ) ] )
% 0.70/1.09 .
% 0.70/1.09 clause( 81, [ one( in1( or1( X ) ) ), ~( one( out1( or1( X ) ) ) ), one(
% 0.70/1.09 in2( or1( X ) ) ), ~( halfadder( X ) ), abnormal( or1( X ) ) ] )
% 0.70/1.09 .
% 0.70/1.09 clause( 80, [ ~( zero( out1( not1( X ) ) ) ), zero( in2( and1( X ) ) ), ~(
% 0.70/1.09 halfadder( X ) ) ] )
% 0.70/1.09 .
% 0.70/1.09 clause( 79, [ ~( one( out1( not1( X ) ) ) ), one( in2( and1( X ) ) ), ~(
% 0.70/1.09 halfadder( X ) ) ] )
% 0.70/1.09 .
% 0.70/1.09 clause( 78, [ ~( one( in2( and1( X ) ) ) ), one( out1( not1( X ) ) ), ~(
% 0.70/1.09 halfadder( X ) ) ] )
% 0.70/1.09 .
% 0.70/1.09 clause( 85, [ ~( zero( out1( and2( X ) ) ) ), zero( in1( not1( X ) ) ), ~(
% 0.70/1.09 halfadder( X ) ) ] )
% 0.70/1.09 .
% 0.70/1.09 clause( 77, [ ~( zero( in2( and1( X ) ) ) ), zero( out1( not1( X ) ) ), ~(
% 0.70/1.09 halfadder( X ) ) ] )
% 0.70/1.09 .
% 0.70/1.09 clause( 84, [ ~( one( out1( and2( X ) ) ) ), one( in1( not1( X ) ) ), ~(
% 0.70/1.09 halfadder( X ) ) ] )
% 0.70/1.09 .
% 0.70/1.09 clause( 83, [ ~( one( in1( not1( X ) ) ) ), one( out1( and2( X ) ) ), ~(
% 0.70/1.09 halfadder( X ) ) ] )
% 0.70/1.09 .
% 0.70/1.09 clause( 82, [ ~( zero( in1( not1( X ) ) ) ), zero( out1( and2( X ) ) ), ~(
% 0.70/1.09 halfadder( X ) ) ] )
% 0.70/1.09 .
% 0.70/1.09 clause( 89, [ ~( zero( out1( or1( X ) ) ) ), zero( in1( and1( X ) ) ), ~(
% 0.70/1.09 halfadder( X ) ) ] )
% 0.70/1.09 .
% 0.70/1.09 clause( 64, [ ~( zero( in1( or1( X ) ) ) ), zero( out1( or1( X ) ) ), ~(
% 0.70/1.09 zero( in2( or1( X ) ) ) ), ~( halfadder( X ) ), abnormal( or1( X ) ) ] )
% 0.70/1.09 .
% 0.70/1.09 clause( 88, [ ~( one( out1( or1( X ) ) ) ), one( in1( and1( X ) ) ), ~(
% 0.70/1.09 halfadder( X ) ) ] )
% 0.70/1.09 .
% 0.70/1.09 clause( 87, [ ~( one( in1( and1( X ) ) ) ), one( out1( or1( X ) ) ), ~(
% 0.70/1.09 halfadder( X ) ) ] )
% 0.70/1.09 .
% 0.70/1.09 clause( 86, [ ~( zero( in1( and1( X ) ) ) ), zero( out1( or1( X ) ) ), ~(
% 0.70/1.09 halfadder( X ) ) ] )
% 0.70/1.09 .
% 0.70/1.09 clause( 55, [ ~( zero( outc( X ) ) ), zero( out1( and2( X ) ) ), ~(
% 0.70/1.09 halfadder( X ) ) ] )
% 0.70/1.09 .
% 0.70/1.09 clause( 54, [ ~( one( outc( X ) ) ), one( out1( and2( X ) ) ), ~( halfadder(
% 0.70/1.09 X ) ) ] )
% 0.70/1.09 .
% 0.70/1.09 clause( 53, [ ~( one( out1( and2( X ) ) ) ), one( outc( X ) ), ~( halfadder(
% 0.70/1.09 X ) ) ] )
% 0.70/1.09 .
% 0.70/1.09 clause( 59, [ ~( zero( outs( X ) ) ), zero( out1( and1( X ) ) ), ~(
% 0.70/1.09 halfadder( X ) ) ] )
% 0.70/1.09 .
% 0.70/1.09 clause( 58, [ ~( one( outs( X ) ) ), one( out1( and1( X ) ) ), ~( halfadder(
% 0.70/1.09 X ) ) ] )
% 0.70/1.09 .
% 0.70/1.09 clause( 57, [ ~( one( out1( and1( X ) ) ) ), one( outs( X ) ), ~( halfadder(
% 0.70/1.09 X ) ) ] )
% 0.70/1.09 .
% 0.70/1.09 clause( 52, [ ~( zero( out1( and2( X ) ) ) ), zero( outc( X ) ), ~(
% 0.70/1.09 halfadder( X ) ) ] )
% 0.70/1.09 .
% 0.70/1.09 clause( 56, [ ~( zero( out1( and1( X ) ) ) ), zero( outs( X ) ), ~(
% 0.70/1.09 halfadder( X ) ) ] )
% 0.70/1.09 .
% 0.70/1.09 clause( 63, [ ~( zero( in2( X ) ) ), zero( in2( and2( X ) ) ), ~( halfadder(
% 0.70/1.09 X ) ) ] )
% 0.70/1.09 .
% 0.70/1.09 clause( 62, [ ~( one( in2( X ) ) ), one( in2( and2( X ) ) ), ~( halfadder(
% 0.70/1.09 X ) ) ] )
% 0.70/1.09 .
% 0.70/1.09 clause( 61, [ ~( one( in2( and2( X ) ) ) ), one( in2( X ) ), ~( halfadder(
% 0.70/1.09 X ) ) ] )
% 0.70/1.09 .
% 0.70/1.09 clause( 51, [ ~( one( in1( or1( X ) ) ) ), one( out1( or1( X ) ) ), ~(
% 0.70/1.09 halfadder( X ) ), abnormal( or1( X ) ) ] )
% 0.70/1.09 .
% 0.70/1.09 clause( 60, [ ~( zero( in2( and2( X ) ) ) ), zero( in2( X ) ), ~( halfadder(
% 0.70/1.09 X ) ) ] )
% 0.70/1.09 .
% 0.70/1.09 clause( 68, [ ~( zero( in1( X ) ) ), zero( in1( and2( X ) ) ), ~( halfadder(
% 0.70/1.09 X ) ) ] )
% 0.70/1.09 .
% 0.70/1.09 clause( 67, [ ~( one( in1( X ) ) ), one( in1( and2( X ) ) ), ~( halfadder(
% 0.70/1.09 X ) ) ] )
% 0.70/1.09 .
% 0.70/1.09 clause( 66, [ ~( one( in1( and2( X ) ) ) ), one( in1( X ) ), ~( halfadder(
% 0.70/1.09 X ) ) ] )
% 0.70/1.09 .
% 0.70/1.09 clause( 50, [ one( out1( or1( X ) ) ), ~( one( in2( or1( X ) ) ) ), ~(
% 0.70/1.09 halfadder( X ) ), abnormal( or1( X ) ) ] )
% 0.70/1.09 .
% 0.70/1.09 clause( 65, [ ~( zero( in1( and2( X ) ) ) ), zero( in1( X ) ), ~( halfadder(
% 0.70/1.09 X ) ) ] )
% 0.70/1.09 .
% 0.70/1.09 clause( 72, [ ~( zero( in2( X ) ) ), zero( in2( or1( X ) ) ), ~( halfadder(
% 0.70/1.09 X ) ) ] )
% 0.70/1.09 .
% 0.70/1.09 clause( 71, [ ~( one( in2( X ) ) ), one( in2( or1( X ) ) ), ~( halfadder( X
% 0.70/1.09 ) ) ] )
% 0.70/1.09 .
% 0.70/1.09 clause( 93, [ ~( zero( out1( or1( X ) ) ) ), ~( 'not_ok'( or1( X ) ) ), ~(
% 0.70/1.09 halfadder( X ) ) ] )
% 0.70/1.09 .
% 0.70/1.09 clause( 49, [ zero( in1( or1( X ) ) ), ~( zero( out1( or1( X ) ) ) ), ~(
% 0.70/1.09 halfadder( X ) ), abnormal( or1( X ) ) ] )
% 0.70/1.09 .
% 0.70/1.09 clause( 70, [ ~( one( in2( or1( X ) ) ) ), one( in2( X ) ), ~( halfadder( X
% 0.70/1.09 ) ) ] )
% 0.70/1.09 .
% 0.70/1.09 clause( 69, [ ~( zero( in2( or1( X ) ) ) ), zero( in2( X ) ), ~( halfadder(
% 0.70/1.09 X ) ) ] )
% 0.70/1.09 .
% 0.70/1.09 clause( 76, [ ~( zero( in1( X ) ) ), zero( in1( or1( X ) ) ), ~( halfadder(
% 0.70/1.09 X ) ) ] )
% 0.70/1.09 .
% 0.70/1.09 clause( 75, [ ~( one( in1( X ) ) ), one( in1( or1( X ) ) ), ~( halfadder( X
% 0.70/1.09 ) ) ] )
% 0.70/1.09 .
% 0.70/1.09 clause( 48, [ ~( zero( out1( or1( X ) ) ) ), zero( in2( or1( X ) ) ), ~(
% 0.70/1.09 halfadder( X ) ), abnormal( or1( X ) ) ] )
% 0.70/1.09 .
% 0.70/1.09 clause( 74, [ ~( one( in1( or1( X ) ) ) ), one( in1( X ) ), ~( halfadder( X
% 0.70/1.09 ) ) ] )
% 0.70/1.09 .
% 0.70/1.09 clause( 73, [ ~( zero( in1( or1( X ) ) ) ), zero( in1( X ) ), ~( halfadder(
% 0.70/1.09 X ) ) ] )
% 0.70/1.09 .
% 0.70/1.09 clause( 37, [ ~( halfadder( X ) ), connection( out1( or1( X ) ), in1( and1(
% 0.70/1.09 X ) ) ) ] )
% 0.70/1.09 .
% 0.70/1.09 clause( 38, [ ~( halfadder( X ) ), connection( out1( and2( X ) ), in1( not1(
% 0.70/1.09 X ) ) ) ] )
% 0.70/1.09 .
% 0.70/1.09 clause( 16, [ ~( one( out1( X ) ) ), one( in1( X ) ), one( in2( X ) ), ~(
% 0.70/1.09 'or_ok'( X ) ) ] )
% 0.70/1.09 .
% 0.70/1.09 clause( 39, [ ~( halfadder( X ) ), connection( out1( not1( X ) ), in2( and1(
% 0.70/1.09 X ) ) ) ] )
% 0.70/1.09 .
% 0.70/1.09 clause( 31, [ ~( halfadder( X ) ), connection( in1( X ), in1( or1( X ) ) )
% 0.70/1.09 ] )
% 0.70/1.09 .
% 0.70/1.09 clause( 32, [ ~( halfadder( X ) ), connection( in2( X ), in2( or1( X ) ) )
% 0.70/1.09 ] )
% 0.70/1.09 .
% 0.70/1.09 clause( 33, [ ~( halfadder( X ) ), connection( in1( X ), in1( and2( X ) ) )
% 0.70/1.09 ] )
% 0.70/1.09 .
% 0.70/1.09 clause( 15, [ ~( zero( in1( X ) ) ), ~( zero( in2( X ) ) ), zero( out1( X )
% 0.70/1.09 ), ~( 'or_ok'( X ) ) ] )
% 0.70/1.09 .
% 0.70/1.09 clause( 34, [ ~( halfadder( X ) ), connection( in2( X ), in2( and2( X ) ) )
% 0.70/1.09 ] )
% 0.70/1.09 .
% 0.70/1.09 clause( 35, [ ~( halfadder( X ) ), connection( outs( X ), out1( and1( X ) )
% 0.70/1.09 ) ] )
% 0.70/1.09 .
% 0.70/1.09 clause( 36, [ ~( halfadder( X ) ), connection( outc( X ), out1( and2( X ) )
% 0.70/1.09 ) ] )
% 0.70/1.09 .
% 0.70/1.09 clause( 10, [ ~( one( out1( X ) ) ), one( in2( X ) ), ~( 'and_ok'( X ) ) ]
% 0.70/1.09 )
% 0.70/1.09 .
% 0.70/1.09 clause( 9, [ ~( one( out1( X ) ) ), one( in1( X ) ), ~( 'and_ok'( X ) ) ]
% 0.70/1.09 )
% 0.70/1.09 .
% 0.70/1.09 clause( 13, [ ~( one( in1( X ) ) ), one( out1( X ) ), ~( 'or_ok'( X ) ) ]
% 0.70/1.09 )
% 0.70/1.09 .
% 0.70/1.09 clause( 14, [ ~( one( in2( X ) ) ), one( out1( X ) ), ~( 'or_ok'( X ) ) ]
% 0.70/1.09 )
% 0.70/1.09 .
% 0.70/1.09 clause( 17, [ ~( zero( out1( X ) ) ), zero( in1( X ) ), ~( 'or_ok'( X ) ) ]
% 0.70/1.09 )
% 0.70/1.09 .
% 0.70/1.09 clause( 18, [ ~( zero( out1( X ) ) ), zero( in2( X ) ), ~( 'or_ok'( X ) ) ]
% 0.70/1.09 )
% 0.70/1.09 .
% 0.70/1.09 clause( 8, [ ~( zero( out1( X ) ) ), zero( in1( X ) ), zero( in2( X ) ),
% 0.70/1.09 ~( 'and_ok'( X ) ) ] )
% 0.70/1.09 .
% 0.70/1.09 clause( 21, [ ~( zero( in1( X ) ) ), ~( 'not_ok'( X ) ), one( out1( X ) ) ]
% 0.70/1.09 )
% 0.70/1.09 .
% 0.70/1.09 clause( 22, [ ~( 'not_ok'( X ) ), zero( out1( X ) ), ~( one( in1( X ) ) ) ]
% 0.70/1.09 )
% 0.70/1.09 .
% 0.70/1.09 clause( 47, [ ~( zero( out1( X ) ) ), ~( zero( in1( X ) ) ), ~( 'not_ok'( X
% 0.70/1.09 ) ) ] )
% 0.70/1.09 .
% 0.70/1.09 clause( 23, [ ~( zero( out1( X ) ) ), ~( 'not_ok'( X ) ), one( in1( X ) ) ]
% 0.70/1.09 )
% 0.70/1.09 .
% 0.70/1.09 clause( 7, [ ~( one( in1( X ) ) ), ~( one( in2( X ) ) ), one( out1( X ) ),
% 0.70/1.09 ~( 'and_ok'( X ) ) ] )
% 0.70/1.09 .
% 0.70/1.09 clause( 24, [ ~( 'not_ok'( X ) ), zero( in1( X ) ), ~( one( out1( X ) ) ) ]
% 0.70/1.09 )
% 0.70/1.09 .
% 0.70/1.09 clause( 46, [ 'not_ok'( not1( X ) ), ~( 'and_ok'( not1( X ) ) ), ~(
% 0.70/1.09 halfadder( X ) ) ] )
% 0.70/1.09 .
% 0.70/1.09 clause( 40, [ 'not_ok'( not1( X ) ), ~( halfadder( X ) ), abnormal( not1( X
% 0.70/1.09 ) ) ] )
% 0.70/1.09 .
% 0.70/1.09 clause( 41, [ abnormal( or1( X ) ), ~( halfadder( X ) ), 'or_ok'( or1( X )
% 0.70/1.09 ) ] )
% 0.70/1.09 .
% 0.70/1.09 clause( 6, [ ~( zero( in2( X ) ) ), zero( out1( X ) ), ~( 'and_ok'( X ) ) ]
% 0.70/1.09 )
% 0.70/1.09 .
% 0.70/1.09 clause( 45, [ 'and_ok'( and2( X ) ), ~( 'not_ok'( and2( X ) ) ), ~(
% 0.70/1.09 halfadder( X ) ) ] )
% 0.70/1.09 .
% 0.70/1.09 clause( 43, [ 'and_ok'( and2( X ) ), ~( halfadder( X ) ), abnormal( and2( X
% 0.70/1.09 ) ) ] )
% 0.70/1.09 .
% 0.70/1.09 clause( 44, [ 'and_ok'( and1( X ) ), ~( 'not_ok'( and1( X ) ) ), ~(
% 0.70/1.09 halfadder( X ) ) ] )
% 0.70/1.09 .
% 0.70/1.09 clause( 42, [ 'and_ok'( and1( X ) ), ~( halfadder( X ) ), abnormal( and1( X
% 0.70/1.09 ) ) ] )
% 0.70/1.09 .
% 0.70/1.09 clause( 5, [ ~( zero( in1( X ) ) ), zero( out1( X ) ), ~( 'and_ok'( X ) ) ]
% 0.70/1.09 )
% 0.70/1.09 .
% 0.70/1.09 clause( 2, [ ~( zero( Y ) ), zero( X ), ~( connection( X, Y ) ) ] )
% 0.70/1.09 .
% 0.70/1.09 clause( 3, [ ~( one( Y ) ), one( X ), ~( connection( X, Y ) ) ] )
% 0.70/1.09 .
% 0.70/1.09 clause( 12, [ 'and_ok'( X ), abnormal( X ), ~( 'logic_and'( X ) ) ] )
% 0.70/1.09 .
% 0.70/1.09 clause( 20, [ 'or_ok'( X ), abnormal( X ), ~( 'logic_or'( X ) ) ] )
% 0.70/1.09 .
% 0.70/1.09 clause( 1, [ ~( one( X ) ), one( Y ), ~( connection( X, Y ) ) ] )
% 0.70/1.09 .
% 0.70/1.09 clause( 26, [ 'not_ok'( X ), abnormal( X ), ~( 'logic_not'( X ) ) ] )
% 0.70/1.09 .
% 0.70/1.09 clause( 27, [ ~( halfadder( X ) ), 'logic_and'( and1( X ) ) ] )
% 0.70/1.09 .
% 0.70/1.09 clause( 28, [ ~( halfadder( X ) ), 'logic_and'( and2( X ) ) ] )
% 0.70/1.09 .
% 0.70/1.09 clause( 29, [ ~( halfadder( X ) ), 'logic_not'( not1( X ) ) ] )
% 0.70/1.09 .
% 0.70/1.09 clause( 0, [ ~( zero( X ) ), zero( Y ), ~( connection( X, Y ) ) ] )
% 0.70/1.09 .
% 0.70/1.09 clause( 30, [ ~( halfadder( X ) ), 'logic_or'( or1( X ) ) ] )
% 0.70/1.09 .
% 0.70/1.09 clause( 4, [ ~( zero( X ) ), ~( one( X ) ) ] )
% 0.70/1.09 .
% 0.70/1.09 clause( 11, [ ~( 'and_ok'( X ) ), ~( abnormal( X ) ) ] )
% 0.70/1.09 .
% 0.70/1.09 clause( 19, [ ~( abnormal( X ) ), ~( 'or_ok'( X ) ) ] )
% 0.70/1.09 .
% 0.70/1.09 clause( 25, [ ~( 'not_ok'( X ) ), ~( abnormal( X ) ) ] )
% 0.70/1.09 .
% 0.70/1.09
% 0.70/1.09
% 0.70/1.09 % SZS output end Saturation
% 0.70/1.09 end of saturation!
% 0.70/1.09
% 0.70/1.09 Memory use:
% 0.70/1.09
% 0.70/1.09 space for terms: 2135
% 0.70/1.09 space for clauses: 5865
% 0.70/1.09
% 0.70/1.09
% 0.70/1.09 clauses generated: 109
% 0.70/1.09 clauses kept: 100
% 0.70/1.09 clauses selected: 99
% 0.70/1.09 clauses deleted: 1
% 0.70/1.09 clauses inuse deleted: 0
% 0.70/1.09
% 0.70/1.09 subsentry: 70
% 0.70/1.09 literals s-matched: 14
% 0.70/1.09 literals matched: 14
% 0.70/1.09 full subsumption: 0
% 0.70/1.09
% 0.70/1.09 checksum: 494750717
% 0.70/1.09
% 0.70/1.09
% 0.70/1.09 Bliksem ended
%------------------------------------------------------------------------------