%------------------------------------------------------------------------------
% File : E---3.5.1
% Problem : HWV036-2 : TPTP v9.3.1. Bugfixed v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n012.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 12:47:27 PM UTC 2026
% Result : Satisfiable 0.07s 0.34s
% Output : Saturation 0.07s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named c_0_57ERROR: Could not build tree for root c_0_137ERROR: MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(c_0_79,plain,
( ~ logic_or(X1)
| abnormal(X1)
| or_ok(X1) ),
c_0_51,
[final] ).
cnf(c_0_80,plain,
( ~ fulladder(X1)
| logic_or(or1(X1)) ),
c_0_52,
[final] ).
cnf(c_0_81,plain,
( ~ halfadder(X1)
| logic_or(or1(X1)) ),
c_0_53,
[final] ).
cnf(c_0_83,plain,
( ~ logic_and(X1)
| abnormal(X1)
| and_ok(X1) ),
c_0_54,
[final] ).
cnf(c_0_84,plain,
( ~ halfadder(X1)
| logic_and(and2(X1)) ),
c_0_55,
[final] ).
cnf(c_0_85,plain,
( ~ halfadder(X1)
| logic_and(and1(X1)) ),
c_0_56,
[final] ).
cnf(c_0_88,plain,
( ~ one(X1)
| ~ connection(X1,X2)
| one(X2) ),
c_0_57,
[final] ).
cnf(c_0_89,plain,
( ~ fulladder(X1)
| connection(outc(h2(X1)),in1(or1(X1))) ),
c_0_58,
[final] ).
cnf(c_0_90,plain,
( ~ zero(X1)
| ~ connection(X1,X2)
| zero(X2) ),
c_0_59,
[final] ).
cnf(c_0_91,plain,
( ~ one(X2)
| ~ connection(X1,X2)
| one(X1) ),
c_0_60,
[final] ).
cnf(c_0_92,plain,
( ~ zero(X2)
| ~ connection(X1,X2)
| zero(X1) ),
c_0_61,
[final] ).
cnf(c_0_93,plain,
( ~ fulladder(X1)
| connection(outc(h1(X1)),in2(or1(X1))) ),
c_0_62,
[final] ).
cnf(c_0_94,plain,
( ~ fulladder(X1)
| connection(outs(h1(X1)),in2(h2(X1))) ),
c_0_63,
[final] ).
cnf(c_0_95,plain,
( ~ halfadder(X1)
| connection(out1(or1(X1)),in1(and1(X1))) ),
c_0_64,
[final] ).
cnf(c_0_96,plain,
( ~ halfadder(X1)
| connection(out1(not1(X1)),in2(and1(X1))) ),
c_0_65,
[final] ).
cnf(c_0_97,plain,
( ~ halfadder(X1)
| connection(out1(and2(X1)),in1(not1(X1))) ),
c_0_66,
[final] ).
cnf(c_0_98,plain,
( ~ fulladder(X1)
| connection(inc(X1),in2(h1(X1))) ),
c_0_67,
[final] ).
cnf(c_0_99,plain,
( ~ fulladder(X1)
| connection(outc(X1),out1(or1(X1))) ),
c_0_68,
[final] ).
cnf(c_0_100,plain,
( ~ halfadder(X1)
| connection(outc(X1),out1(and2(X1))) ),
c_0_69,
[final] ).
cnf(c_0_101,plain,
( ~ fulladder(X1)
| connection(outs(X1),outs(h2(X1))) ),
c_0_70,
[final] ).
cnf(c_0_102,plain,
( ~ halfadder(X1)
| connection(outs(X1),out1(and1(X1))) ),
c_0_71,
[final] ).
cnf(c_0_103,plain,
( ~ halfadder(X1)
| connection(in2(X1),in2(or1(X1))) ),
c_0_72,
[final] ).
cnf(c_0_104,plain,
( ~ halfadder(X1)
| connection(in2(X1),in2(and2(X1))) ),
c_0_73,
[final] ).
cnf(c_0_105,plain,
( ~ fulladder(X1)
| connection(in2(X1),in1(h1(X1))) ),
c_0_74,
[final] ).
cnf(c_0_106,plain,
( ~ fulladder(X1)
| connection(in1(X1),in1(h2(X1))) ),
c_0_75,
[final] ).
cnf(c_0_107,plain,
( ~ halfadder(X1)
| connection(in1(X1),in1(or1(X1))) ),
c_0_76,
[final] ).
cnf(c_0_108,plain,
( ~ halfadder(X1)
| connection(in1(X1),in1(and2(X1))) ),
c_0_77,
[final] ).
cnf(c_0_109,plain,
( ~ abnormal(X1)
| ~ and_ok(X1) ),
c_0_78,
[final] ).
cnf(c_0_110,plain,
( ~ fulladder(X1)
| abnormal(or1(X1))
| or_ok(or1(X1)) ),
inference(spm,[status(thm)],[c_0_79,c_0_80]),
[final] ).
cnf(c_0_111,plain,
( ~ halfadder(X1)
| abnormal(or1(X1))
| or_ok(or1(X1)) ),
inference(spm,[status(thm)],[c_0_79,c_0_81]),
[final] ).
cnf(c_0_112,plain,
( ~ abnormal(X1)
| ~ or_ok(X1) ),
c_0_82,
[final] ).
cnf(c_0_113,plain,
( ~ halfadder(X1)
| and_ok(and2(X1))
| abnormal(and2(X1)) ),
inference(spm,[status(thm)],[c_0_83,c_0_84]),
[final] ).
cnf(c_0_114,plain,
( ~ halfadder(X1)
| and_ok(and1(X1))
| abnormal(and1(X1)) ),
inference(spm,[status(thm)],[c_0_83,c_0_85]),
[final] ).
cnf(c_0_115,plain,
( ~ logic_not(X1)
| abnormal(X1)
| not_ok(X1) ),
c_0_86,
[final] ).
cnf(c_0_116,plain,
( ~ halfadder(X1)
| logic_not(not1(X1)) ),
c_0_87,
[final] ).
cnf(c_0_137,plain,
( ~ one(outc(h2(X1)))
| ~ fulladder(X1)
| one(in1(or1(X1))) ),
inference(spm,[status(thm)],[c_0_88,c_0_89]),
[final] ).
cnf(c_0_138,plain,
( ~ zero(outc(h2(X1)))
| ~ fulladder(X1)
| zero(in1(or1(X1))) ),
inference(spm,[status(thm)],[c_0_90,c_0_89]),
[final] ).
cnf(c_0_139,plain,
( ~ one(in1(or1(X1)))
| ~ fulladder(X1)
| one(outc(h2(X1))) ),
inference(spm,[status(thm)],[c_0_91,c_0_89]),
[final] ).
cnf(c_0_140,plain,
( ~ zero(in1(or1(X1)))
| ~ fulladder(X1)
| zero(outc(h2(X1))) ),
inference(spm,[status(thm)],[c_0_92,c_0_89]),
[final] ).
cnf(c_0_141,plain,
( ~ one(outc(h1(X1)))
| ~ fulladder(X1)
| one(in2(or1(X1))) ),
inference(spm,[status(thm)],[c_0_88,c_0_93]),
[final] ).
cnf(c_0_142,plain,
( ~ zero(outc(h1(X1)))
| ~ fulladder(X1)
| zero(in2(or1(X1))) ),
inference(spm,[status(thm)],[c_0_90,c_0_93]),
[final] ).
cnf(c_0_143,plain,
( ~ one(in2(or1(X1)))
| ~ fulladder(X1)
| one(outc(h1(X1))) ),
inference(spm,[status(thm)],[c_0_91,c_0_93]),
[final] ).
cnf(c_0_144,plain,
( ~ zero(in2(or1(X1)))
| ~ fulladder(X1)
| zero(outc(h1(X1))) ),
inference(spm,[status(thm)],[c_0_92,c_0_93]),
[final] ).
cnf(c_0_145,plain,
( ~ one(outs(h1(X1)))
| ~ fulladder(X1)
| one(in2(h2(X1))) ),
inference(spm,[status(thm)],[c_0_88,c_0_94]),
[final] ).
cnf(c_0_146,plain,
( ~ zero(outs(h1(X1)))
| ~ fulladder(X1)
| zero(in2(h2(X1))) ),
inference(spm,[status(thm)],[c_0_90,c_0_94]),
[final] ).
cnf(c_0_147,plain,
( ~ one(in2(h2(X1)))
| ~ fulladder(X1)
| one(outs(h1(X1))) ),
inference(spm,[status(thm)],[c_0_91,c_0_94]),
[final] ).
cnf(c_0_148,plain,
( ~ zero(in2(h2(X1)))
| ~ fulladder(X1)
| zero(outs(h1(X1))) ),
inference(spm,[status(thm)],[c_0_92,c_0_94]),
[final] ).
cnf(c_0_149,plain,
( ~ one(out1(or1(X1)))
| ~ halfadder(X1)
| one(in1(and1(X1))) ),
inference(spm,[status(thm)],[c_0_88,c_0_95]),
[final] ).
cnf(c_0_150,plain,
( ~ zero(out1(or1(X1)))
| ~ halfadder(X1)
| zero(in1(and1(X1))) ),
inference(spm,[status(thm)],[c_0_90,c_0_95]),
[final] ).
cnf(c_0_151,plain,
( ~ one(in1(and1(X1)))
| ~ halfadder(X1)
| one(out1(or1(X1))) ),
inference(spm,[status(thm)],[c_0_91,c_0_95]),
[final] ).
cnf(c_0_152,plain,
( ~ zero(in1(and1(X1)))
| ~ halfadder(X1)
| zero(out1(or1(X1))) ),
inference(spm,[status(thm)],[c_0_92,c_0_95]),
[final] ).
cnf(c_0_153,plain,
( ~ one(out1(not1(X1)))
| ~ halfadder(X1)
| one(in2(and1(X1))) ),
inference(spm,[status(thm)],[c_0_88,c_0_96]),
[final] ).
cnf(c_0_154,plain,
( ~ zero(out1(not1(X1)))
| ~ halfadder(X1)
| zero(in2(and1(X1))) ),
inference(spm,[status(thm)],[c_0_90,c_0_96]),
[final] ).
cnf(c_0_155,plain,
( ~ one(in2(and1(X1)))
| ~ halfadder(X1)
| one(out1(not1(X1))) ),
inference(spm,[status(thm)],[c_0_91,c_0_96]),
[final] ).
cnf(c_0_156,plain,
( ~ zero(in2(and1(X1)))
| ~ halfadder(X1)
| zero(out1(not1(X1))) ),
inference(spm,[status(thm)],[c_0_92,c_0_96]),
[final] ).
cnf(c_0_157,plain,
( ~ one(out1(and2(X1)))
| ~ halfadder(X1)
| one(in1(not1(X1))) ),
inference(spm,[status(thm)],[c_0_88,c_0_97]),
[final] ).
cnf(c_0_158,plain,
( ~ zero(out1(and2(X1)))
| ~ halfadder(X1)
| zero(in1(not1(X1))) ),
inference(spm,[status(thm)],[c_0_90,c_0_97]),
[final] ).
cnf(c_0_159,plain,
( ~ one(in1(not1(X1)))
| ~ halfadder(X1)
| one(out1(and2(X1))) ),
inference(spm,[status(thm)],[c_0_91,c_0_97]),
[final] ).
cnf(c_0_160,plain,
( ~ zero(in1(not1(X1)))
| ~ halfadder(X1)
| zero(out1(and2(X1))) ),
inference(spm,[status(thm)],[c_0_92,c_0_97]),
[final] ).
cnf(c_0_161,plain,
( ~ one(in2(h1(X1)))
| ~ fulladder(X1)
| one(inc(X1)) ),
inference(spm,[status(thm)],[c_0_91,c_0_98]),
[final] ).
cnf(c_0_162,plain,
( ~ zero(in2(h1(X1)))
| ~ fulladder(X1)
| zero(inc(X1)) ),
inference(spm,[status(thm)],[c_0_92,c_0_98]),
[final] ).
cnf(c_0_163,plain,
( ~ one(out1(or1(X1)))
| ~ fulladder(X1)
| one(outc(X1)) ),
inference(spm,[status(thm)],[c_0_91,c_0_99]),
[final] ).
cnf(c_0_164,plain,
( ~ zero(out1(or1(X1)))
| ~ fulladder(X1)
| zero(outc(X1)) ),
inference(spm,[status(thm)],[c_0_92,c_0_99]),
[final] ).
cnf(c_0_165,plain,
( ~ one(out1(and2(X1)))
| ~ halfadder(X1)
| one(outc(X1)) ),
inference(spm,[status(thm)],[c_0_91,c_0_100]),
[final] ).
cnf(c_0_166,plain,
( ~ zero(out1(and2(X1)))
| ~ halfadder(X1)
| zero(outc(X1)) ),
inference(spm,[status(thm)],[c_0_92,c_0_100]),
[final] ).
cnf(c_0_167,plain,
( ~ one(outs(h2(X1)))
| ~ fulladder(X1)
| one(outs(X1)) ),
inference(spm,[status(thm)],[c_0_91,c_0_101]),
[final] ).
cnf(c_0_168,plain,
( ~ zero(outs(h2(X1)))
| ~ fulladder(X1)
| zero(outs(X1)) ),
inference(spm,[status(thm)],[c_0_92,c_0_101]),
[final] ).
cnf(c_0_169,plain,
( ~ one(out1(and1(X1)))
| ~ halfadder(X1)
| one(outs(X1)) ),
inference(spm,[status(thm)],[c_0_91,c_0_102]),
[final] ).
cnf(c_0_170,plain,
( ~ zero(out1(and1(X1)))
| ~ halfadder(X1)
| zero(outs(X1)) ),
inference(spm,[status(thm)],[c_0_92,c_0_102]),
[final] ).
cnf(c_0_171,plain,
( ~ one(in2(or1(X1)))
| ~ halfadder(X1)
| one(in2(X1)) ),
inference(spm,[status(thm)],[c_0_91,c_0_103]),
[final] ).
cnf(c_0_172,plain,
( ~ zero(in2(or1(X1)))
| ~ halfadder(X1)
| zero(in2(X1)) ),
inference(spm,[status(thm)],[c_0_92,c_0_103]),
[final] ).
cnf(c_0_173,plain,
( ~ one(in2(and2(X1)))
| ~ halfadder(X1)
| one(in2(X1)) ),
inference(spm,[status(thm)],[c_0_91,c_0_104]),
[final] ).
cnf(c_0_174,plain,
( ~ zero(in2(and2(X1)))
| ~ halfadder(X1)
| zero(in2(X1)) ),
inference(spm,[status(thm)],[c_0_92,c_0_104]),
[final] ).
cnf(c_0_175,plain,
( ~ one(in1(h1(X1)))
| ~ fulladder(X1)
| one(in2(X1)) ),
inference(spm,[status(thm)],[c_0_91,c_0_105]),
[final] ).
cnf(c_0_176,plain,
( ~ one(inc(X1))
| ~ fulladder(X1)
| one(in2(h1(X1))) ),
inference(spm,[status(thm)],[c_0_88,c_0_98]),
[final] ).
cnf(c_0_177,plain,
( ~ zero(inc(X1))
| ~ fulladder(X1)
| zero(in2(h1(X1))) ),
inference(spm,[status(thm)],[c_0_90,c_0_98]),
[final] ).
cnf(c_0_178,plain,
( ~ one(outc(X1))
| ~ fulladder(X1)
| one(out1(or1(X1))) ),
inference(spm,[status(thm)],[c_0_88,c_0_99]),
[final] ).
cnf(c_0_179,plain,
( ~ zero(outc(X1))
| ~ fulladder(X1)
| zero(out1(or1(X1))) ),
inference(spm,[status(thm)],[c_0_90,c_0_99]),
[final] ).
cnf(c_0_180,plain,
( ~ one(outc(X1))
| ~ halfadder(X1)
| one(out1(and2(X1))) ),
inference(spm,[status(thm)],[c_0_88,c_0_100]),
[final] ).
cnf(c_0_181,plain,
( ~ zero(in1(h1(X1)))
| ~ fulladder(X1)
| zero(in2(X1)) ),
inference(spm,[status(thm)],[c_0_92,c_0_105]),
[final] ).
cnf(c_0_182,plain,
( ~ one(in1(h2(X1)))
| ~ fulladder(X1)
| one(in1(X1)) ),
inference(spm,[status(thm)],[c_0_91,c_0_106]),
[final] ).
cnf(c_0_183,plain,
( ~ zero(outc(X1))
| ~ halfadder(X1)
| zero(out1(and2(X1))) ),
inference(spm,[status(thm)],[c_0_90,c_0_100]),
[final] ).
cnf(c_0_184,plain,
( ~ one(outs(X1))
| ~ fulladder(X1)
| one(outs(h2(X1))) ),
inference(spm,[status(thm)],[c_0_88,c_0_101]),
[final] ).
cnf(c_0_185,plain,
( ~ zero(outs(X1))
| ~ fulladder(X1)
| zero(outs(h2(X1))) ),
inference(spm,[status(thm)],[c_0_90,c_0_101]),
[final] ).
cnf(c_0_186,plain,
( ~ one(outs(X1))
| ~ halfadder(X1)
| one(out1(and1(X1))) ),
inference(spm,[status(thm)],[c_0_88,c_0_102]),
[final] ).
cnf(c_0_187,plain,
( ~ zero(outs(X1))
| ~ halfadder(X1)
| zero(out1(and1(X1))) ),
inference(spm,[status(thm)],[c_0_90,c_0_102]),
[final] ).
cnf(c_0_188,plain,
( ~ one(in2(X1))
| ~ halfadder(X1)
| one(in2(or1(X1))) ),
inference(spm,[status(thm)],[c_0_88,c_0_103]),
[final] ).
cnf(c_0_189,plain,
( ~ zero(in2(X1))
| ~ halfadder(X1)
| zero(in2(or1(X1))) ),
inference(spm,[status(thm)],[c_0_90,c_0_103]),
[final] ).
cnf(c_0_190,plain,
( ~ zero(in1(h2(X1)))
| ~ fulladder(X1)
| zero(in1(X1)) ),
inference(spm,[status(thm)],[c_0_92,c_0_106]),
[final] ).
cnf(c_0_191,plain,
( ~ one(in1(or1(X1)))
| ~ halfadder(X1)
| one(in1(X1)) ),
inference(spm,[status(thm)],[c_0_91,c_0_107]),
[final] ).
cnf(c_0_192,plain,
( ~ one(in2(X1))
| ~ halfadder(X1)
| one(in2(and2(X1))) ),
inference(spm,[status(thm)],[c_0_88,c_0_104]),
[final] ).
cnf(c_0_193,plain,
( ~ zero(in2(X1))
| ~ halfadder(X1)
| zero(in2(and2(X1))) ),
inference(spm,[status(thm)],[c_0_90,c_0_104]),
[final] ).
cnf(c_0_194,plain,
( ~ one(in2(X1))
| ~ fulladder(X1)
| one(in1(h1(X1))) ),
inference(spm,[status(thm)],[c_0_88,c_0_105]),
[final] ).
cnf(c_0_195,plain,
( ~ zero(in2(X1))
| ~ fulladder(X1)
| zero(in1(h1(X1))) ),
inference(spm,[status(thm)],[c_0_90,c_0_105]),
[final] ).
cnf(c_0_196,plain,
( ~ one(in1(X1))
| ~ fulladder(X1)
| one(in1(h2(X1))) ),
inference(spm,[status(thm)],[c_0_88,c_0_106]),
[final] ).
cnf(c_0_197,plain,
( ~ zero(in1(X1))
| ~ fulladder(X1)
| zero(in1(h2(X1))) ),
inference(spm,[status(thm)],[c_0_90,c_0_106]),
[final] ).
cnf(c_0_198,plain,
( ~ one(in1(X1))
| ~ halfadder(X1)
| one(in1(or1(X1))) ),
inference(spm,[status(thm)],[c_0_88,c_0_107]),
[final] ).
cnf(c_0_199,plain,
( ~ zero(in1(or1(X1)))
| ~ halfadder(X1)
| zero(in1(X1)) ),
inference(spm,[status(thm)],[c_0_92,c_0_107]),
[final] ).
cnf(c_0_200,plain,
( ~ one(in1(and2(X1)))
| ~ halfadder(X1)
| one(in1(X1)) ),
inference(spm,[status(thm)],[c_0_91,c_0_108]),
[final] ).
cnf(c_0_201,plain,
( ~ zero(in1(X1))
| ~ halfadder(X1)
| zero(in1(or1(X1))) ),
inference(spm,[status(thm)],[c_0_90,c_0_107]),
[final] ).
cnf(c_0_202,plain,
( ~ one(in1(X1))
| ~ halfadder(X1)
| one(in1(and2(X1))) ),
inference(spm,[status(thm)],[c_0_88,c_0_108]),
[final] ).
cnf(c_0_203,plain,
( ~ zero(in1(X1))
| ~ halfadder(X1)
| zero(in1(and2(X1))) ),
inference(spm,[status(thm)],[c_0_90,c_0_108]),
[final] ).
cnf(c_0_204,plain,
( ~ and_ok(or1(X1))
| ~ fulladder(X1)
| or_ok(or1(X1)) ),
inference(spm,[status(thm)],[c_0_109,c_0_110]),
[final] ).
cnf(c_0_205,plain,
( ~ and_ok(or1(X1))
| ~ halfadder(X1)
| or_ok(or1(X1)) ),
inference(spm,[status(thm)],[c_0_109,c_0_111]),
[final] ).
cnf(c_0_206,plain,
( ~ or_ok(and2(X1))
| ~ halfadder(X1)
| and_ok(and2(X1)) ),
inference(spm,[status(thm)],[c_0_112,c_0_113]),
[final] ).
cnf(c_0_207,plain,
( ~ or_ok(and1(X1))
| ~ halfadder(X1)
| and_ok(and1(X1)) ),
inference(spm,[status(thm)],[c_0_112,c_0_114]),
[final] ).
cnf(c_0_208,plain,
( ~ zero(in1(and2(X1)))
| ~ halfadder(X1)
| zero(in1(X1)) ),
inference(spm,[status(thm)],[c_0_92,c_0_108]),
[final] ).
cnf(c_0_209,plain,
( ~ halfadder(X1)
| abnormal(not1(X1))
| not_ok(not1(X1)) ),
inference(spm,[status(thm)],[c_0_115,c_0_116]),
[final] ).
cnf(c_0_210,plain,
( ~ one(in2(X1))
| ~ one(in1(X1))
| ~ and_ok(X1)
| one(out1(X1)) ),
c_0_117,
[final] ).
cnf(c_0_211,plain,
( ~ zero(in2(X1))
| ~ zero(in1(X1))
| ~ or_ok(X1)
| zero(out1(X1)) ),
c_0_118,
[final] ).
cnf(c_0_212,plain,
( ~ one(out1(X1))
| ~ or_ok(X1)
| one(in2(X1))
| one(in1(X1)) ),
c_0_119,
[final] ).
cnf(c_0_213,plain,
( ~ zero(out1(X1))
| ~ and_ok(X1)
| zero(in2(X1))
| zero(in1(X1)) ),
c_0_120,
[final] ).
cnf(c_0_214,plain,
( ~ one(out1(X1))
| ~ and_ok(X1)
| one(in2(X1)) ),
c_0_121,
[final] ).
cnf(c_0_215,plain,
( ~ zero(in1(X1))
| ~ not_ok(X1)
| one(out1(X1)) ),
c_0_122,
[final] ).
cnf(c_0_216,plain,
( ~ one(in2(X1))
| ~ or_ok(X1)
| one(out1(X1)) ),
c_0_123,
[final] ).
cnf(c_0_217,plain,
( ~ one(in1(X1))
| ~ or_ok(X1)
| one(out1(X1)) ),
c_0_124,
[final] ).
cnf(c_0_218,plain,
( ~ zero(out1(X1))
| ~ not_ok(X1)
| one(in1(X1)) ),
c_0_125,
[final] ).
cnf(c_0_219,plain,
( ~ one(out1(X1))
| ~ and_ok(X1)
| one(in1(X1)) ),
c_0_126,
[final] ).
cnf(c_0_220,plain,
( ~ zero(out1(X1))
| ~ or_ok(X1)
| zero(in2(X1)) ),
c_0_127,
[final] ).
cnf(c_0_221,plain,
( ~ one(in1(X1))
| ~ not_ok(X1)
| zero(out1(X1)) ),
c_0_128,
[final] ).
cnf(c_0_222,plain,
( ~ zero(in2(X1))
| ~ and_ok(X1)
| zero(out1(X1)) ),
c_0_129,
[final] ).
cnf(c_0_223,plain,
( ~ zero(in1(X1))
| ~ and_ok(X1)
| zero(out1(X1)) ),
c_0_130,
[final] ).
cnf(c_0_224,plain,
( ~ one(out1(X1))
| ~ not_ok(X1)
| zero(in1(X1)) ),
c_0_131,
[final] ).
cnf(c_0_225,plain,
( ~ zero(out1(X1))
| ~ or_ok(X1)
| zero(in1(X1)) ),
c_0_132,
[final] ).
cnf(c_0_226,plain,
( ~ fulladder(X1)
| halfadder(h2(X1)) ),
c_0_133,
[final] ).
cnf(c_0_227,plain,
( ~ fulladder(X1)
| halfadder(h1(X1)) ),
c_0_134,
[final] ).
cnf(c_0_228,plain,
( ~ abnormal(X1)
| ~ not_ok(X1) ),
c_0_135,
[final] ).
cnf(c_0_229,plain,
( ~ one(X1)
| ~ zero(X1) ),
c_0_136,
[final] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : HWV036-2 : TPTP v9.3.1. Bugfixed v2.7.0.
% 0.00/0.02 % Command : run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.04/0.30 % Computer : n012.cluster.edu
% 0.04/0.30 % Model : x86_64 x86_64
% 0.04/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.04/0.30 % Memory : 8046.5625MB
% 0.04/0.30 % OS : Linux 6.8.0-71-generic
% 0.04/0.30 % CPULimit : 300
% 0.04/0.30 % WCLimit : 300
% 0.04/0.30 % DateTime : Sun Sep 20 20:49:21 UTC 2026
% 0.04/0.30 % CPUTime :
% 0.04/0.30 Running run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.07/0.32 Running first-order theorem proving
% 0.07/0.32 Running: /export/starexec/sandbox/solver/bin/eprover --delete-bad-limit=2000000000 --definitional-cnf=24 -s --print-statistics -R --print-version --proof-object --auto-schedule=8 --cpu-limit=300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.07/0.34 % Version: 3.5.1
% 0.07/0.34 % Preprocessing class: FSMSSMSSSSSNFFN.
% 0.07/0.34 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.07/0.34 % Starting G-E--_208_C18_F1_SE_CS_SOS_SP_PS_S5PRR_RG_S04AN with 1500s (5) cores
% 0.07/0.34 % Starting new_bool_3 with 300s (1) cores
% 0.07/0.34 % Starting new_bool_1 with 300s (1) cores
% 0.07/0.34 % Starting sh5l with 300s (1) cores
% 0.07/0.34 % G-E--_208_C18_F1_SE_CS_SOS_SP_PS_S5PRR_RG_S04AN with pid 840142 completed with status 1
% 0.07/0.34 % Result found by G-E--_208_C18_F1_SE_CS_SOS_SP_PS_S5PRR_RG_S04AN
% 0.07/0.34 % Preprocessing class: FSMSSMSSSSSNFFN.
% 0.07/0.34 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.07/0.34 % Starting G-E--_208_C18_F1_SE_CS_SOS_SP_PS_S5PRR_RG_S04AN with 1500s (5) cores
% 0.07/0.34 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 0.07/0.34 % No SInE strategy applied
% 0.07/0.34 % Search class: FGHNF-FFMF11-SFFFFFNN
% 0.07/0.34 % Scheduled 7 strats onto 5 cores with 1500 seconds (1500 total)
% 0.07/0.34 % Starting SubtermCWHack with 136s (1) cores
% 0.07/0.34 % Starting G-E--_208_C18_F1_SE_CS_SOS_SP_PS_S5PRR_RG_S04AN with 151s (1) cores
% 0.07/0.34 % Starting G-E--_107_C18_F1_PI_AE_Q4_CS_SP_PS_S4S with 136s (1) cores
% 0.07/0.34 % Starting G-E--_208_C02CMA_F1_SE_CS_SP_PS_S5PRR_RG_S04AN with 136s (1) cores
% 0.07/0.34 % Starting G-N--_023_B07_F1_SP_PI_Q7_CS_SP_CO_S5PRR_S0Y with 136s (1) cores
% 0.07/0.34 % G-E--_107_C18_F1_PI_AE_Q4_CS_SP_PS_S4S with pid 840151 completed with status 1
% 0.07/0.34 % Result found by G-E--_107_C18_F1_PI_AE_Q4_CS_SP_PS_S4S
% 0.07/0.34 % Preprocessing class: FSMSSMSSSSSNFFN.
% 0.07/0.34 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.07/0.34 % Starting G-E--_208_C18_F1_SE_CS_SOS_SP_PS_S5PRR_RG_S04AN with 1500s (5) cores
% 0.07/0.34 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 0.07/0.34 % No SInE strategy applied
% 0.07/0.34 % Search class: FGHNF-FFMF11-SFFFFFNN
% 0.07/0.34 % Scheduled 7 strats onto 5 cores with 1500 seconds (1500 total)
% 0.07/0.34 % Starting SubtermCWHack with 136s (1) cores
% 0.07/0.34 % Starting G-E--_208_C18_F1_SE_CS_SOS_SP_PS_S5PRR_RG_S04AN with 151s (1) cores
% 0.07/0.34 % Starting G-E--_107_C18_F1_PI_AE_Q4_CS_SP_PS_S4S with 136s (1) cores
% 0.07/0.34 % Preprocessing time : 0.001 s
% 0.07/0.34 % Presaturation interreduction done
% 0.07/0.34
% 0.07/0.34 % No proof found!
% 0.07/0.34 % SZS status Satisfiable
% 0.07/0.34 % SZS output start Saturation
% See solution above
% 0.07/0.34 % Parsed axioms : 51
% 0.07/0.34 % Removed by relevancy pruning/SinE : 0
% 0.07/0.34 % Initial clauses : 51
% 0.07/0.34 % Removed in clause preprocessing : 0
% 0.07/0.34 % Initial clauses in saturation : 51
% 0.07/0.34 % Processed clauses : 179
% 0.07/0.34 % ...of these trivial : 0
% 0.07/0.34 % ...subsumed : 0
% 0.07/0.34 % ...remaining for further processing : 179
% 0.07/0.34 % Other redundant clauses eliminated : 0
% 0.07/0.34 % Clauses deleted for lack of memory : 0
% 0.07/0.34 % Backward-subsumed : 0
% 0.07/0.34 % Backward-rewritten : 0
% 0.07/0.34 % Generated clauses : 82
% 0.07/0.34 % ...of the previous two non-redundant : 77
% 0.07/0.34 % ...aggressively subsumed : 0
% 0.07/0.34 % Contextual simplify-reflections : 0
% 0.07/0.34 % Paramodulations : 82
% 0.07/0.34 % Factorizations : 0
% 0.07/0.34 % NegExts : 0
% 0.07/0.34 % Equation resolutions : 0
% 0.07/0.34 % Disequality decompositions : 0
% 0.07/0.34 % Total rewrite steps : 0
% 0.07/0.34 % ...of those cached : 0
% 0.07/0.34 % Propositional unsat checks : 0
% 0.07/0.34 % Propositional check models : 0
% 0.07/0.34 % Propositional check unsatisfiable : 0
% 0.07/0.34 % Propositional clauses : 0
% 0.07/0.34 % Propositional clauses after purity: 0
% 0.07/0.34 % Propositional unsat core size : 0
% 0.07/0.34 % Propositional preprocessing time : 0.000
% 0.07/0.34 % Propositional encoding time : 0.000
% 0.07/0.34 % Propositional solver time : 0.000
% 0.07/0.34 % Success case prop preproc time : 0.000
% 0.07/0.34 % Success case prop encoding time : 0.000
% 0.07/0.34 % Success case prop solver time : 0.000
% 0.07/0.34 % Current number of processed clauses : 128
% 0.07/0.34 % Positive orientable unit clauses : 0
% 0.07/0.34 % Positive unorientable unit clauses: 0
% 0.07/0.34 % Negative unit clauses : 0
% 0.07/0.34 % Non-unit-clauses : 128
% 0.07/0.34 % Current number of unprocessed clauses: 0
% 0.07/0.34 % ...number of literals in the above : 0
% 0.07/0.34 % Current number of archived formulas : 0
% 0.07/0.34 % Current number of archived clauses : 51
% 0.07/0.34 % Clause-clause subsumption calls (NU) : 1970
% 0.07/0.34 % Rec. Clause-clause subsumption calls : 1712
% 0.07/0.34 % Non-unit clause-clause subsumptions : 0
% 0.07/0.34 % Unit Clause-clause subsumption calls : 0
% 0.07/0.34 % Rewrite failures with RHS unbound : 0
% 0.07/0.34 % BW rewrite match attempts : 0
% 0.07/0.34 % BW rewrite match successes : 0
% 0.07/0.34 % Condensation attempts : 0
% 0.07/0.34 % Condensation successes : 0
% 0.07/0.34 % Termbank termtop insertions : 4638
% 0.07/0.34 % Search garbage collected termcells : 97
% 0.07/0.34
% 0.07/0.34 % -------------------------------------------------
% 0.07/0.34 % User time : 0.006 s
% 0.07/0.34 % System time : 0.002 s
% 0.07/0.34 % Total time : 0.008 s
% 0.07/0.34 % Maximum resident set size: 3676 pages
% 0.07/0.34
% 0.07/0.34 % -------------------------------------------------
% 0.07/0.34 % User time : 0.029 s
% 0.07/0.34 % System time : 0.011 s
% 0.07/0.34 % Total time : 0.040 s
% 0.07/0.34 % Maximum resident set size: 4864 pages
% 0.07/0.34 % E exiting
%------------------------------------------------------------------------------