%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : HWV005-1 : TPTP v8.2.0. Released v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% Computer : n024.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 : Mon Jun 24 07:29:05 EDT 2024
% Result : Unsatisfiable 58.57s 58.85s
% Output : CNFRefutation 58.83s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : HWV005-1 : TPTP v8.2.0. Released v2.1.0.
% 0.03/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.12/0.33 % Computer : n024.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 : Fri Jun 21 01:12:09 EDT 2024
% 0.12/0.34 % CPUTime :
% 0.52/0.57 start to proof:theBenchmark
% 58.57/58.84 %-------------------------------------------
% 58.57/58.84 % File :CSE---1.7
% 58.57/58.84 % Problem :theBenchmark
% 58.57/58.84 % Transform :cnf
% 58.57/58.84 % Format :tptp:raw
% 58.57/58.84 % Command :java -jar mcs_scs.jar %d %s
% 58.57/58.84
% 58.57/58.84 % Result :Theorem 58.010000s
% 58.57/58.84 % Output :CNFRefutation 58.010000s
% 58.57/58.84 %-------------------------------------------
% 58.57/58.85 %--------------------------------------------------------------------------
% 58.57/58.85 % File : HWV005-1 : TPTP v8.2.0. Released v2.1.0.
% 58.57/58.85 % Domain : Hardware Verification
% 58.57/58.85 % Problem : A halfadder built from and, or and not gates
% 58.57/58.85 % Version : [Gei96] axioms.
% 58.57/58.85 % English :
% 58.57/58.85
% 58.57/58.85 % Refs : [Gei96] Geisler (1996), Email to G. Sutcliffe
% 58.57/58.85 % Source : [Gei96]
% 58.57/58.85 % Names :
% 58.57/58.85
% 58.57/58.85 % Status : Unsatisfiable
% 58.57/58.85 % Rating : 0.00 v7.1.0, 0.17 v7.0.0, 0.12 v6.3.0, 0.14 v6.2.0, 0.00 v2.1.0
% 58.57/58.85 % Syntax : Number of clauses : 42 ( 10 unt; 3 nHn; 42 RR)
% 58.57/58.85 % Number of literals : 110 ( 0 equ; 71 neg)
% 58.57/58.85 % Maximal clause size : 5 ( 2 avg)
% 58.57/58.85 % Maximal term depth : 3 ( 1 avg)
% 58.57/58.85 % Number of predicates : 5 ( 5 usr; 0 prp; 2-2 aty)
% 58.57/58.85 % Number of functors : 18 ( 18 usr; 12 con; 0-2 aty)
% 58.57/58.85 % Number of variables : 41 ( 3 sgn)
% 58.57/58.85 % SPC : CNF_UNS_RFO_NEQ_NHN
% 58.57/58.85
% 58.57/58.85 % Comments :
% 58.57/58.85 %--------------------------------------------------------------------------
% 58.57/58.85 %----Include basic diagnosis axioms
% 58.57/58.85 include('Axioms/HWV001-0.ax').
% 58.57/58.85 %----Include model of halfadder
% 58.57/58.85 include('Axioms/HWV001-1.ax').
% 58.57/58.85 %--------------------------------------------------------------------------
% 58.57/58.85 %----Observations
% 58.57/58.85 cnf(h_isa_halfadder,hypothesis,
% 58.57/58.85 type(h,halfadder) ).
% 58.57/58.85
% 58.57/58.85 cnf(in1_1,hypothesis,
% 58.57/58.85 value(in(n1,h),n1) ).
% 58.57/58.85
% 58.57/58.85 cnf(in2_0,hypothesis,
% 58.57/58.85 value(in(n2,h),n0) ).
% 58.57/58.85
% 58.57/58.85 cnf(outs_0,hypothesis,
% 58.57/58.85 value(out(s,h),n0) ).
% 58.57/58.85
% 58.57/58.85 cnf(outc_0,hypothesis,
% 58.57/58.85 value(out(c,h),n0) ).
% 58.57/58.85
% 58.57/58.85 cnf(diagnosis_and1,negated_conjecture,
% 58.57/58.85 ~ mode(and1(h),abnormal) ).
% 58.57/58.85
% 58.57/58.85 cnf(diagnosis_not1,negated_conjecture,
% 58.57/58.85 ~ mode(not1(h),abnormal) ).
% 58.57/58.85
% 58.57/58.85 cnf(diagnosis_or1,negated_conjecture,
% 58.57/58.85 ~ mode(or1(h),abnormal) ).
% 58.57/58.85
% 58.57/58.85 %--------------------------------------------------------------------------
% 58.57/58.85 %-------------------------------------------
% 58.57/58.85 % Proof found
% 58.57/58.85 % SZS status Theorem for theBenchmark
% 58.57/58.85 % SZS output start Proof
% 58.57/58.86 %ClaNum:42(EqnAxiom:0)
% 58.57/58.86 %VarNum:121(SingletonVarNum:41)
% 58.57/58.86 %MaxLitNum:5
% 58.57/58.86 %MaxfuncDepth:2
% 58.57/58.86 %SharedTerms:29
% 58.57/58.86 %goalClause: 8 9 10
% 58.57/58.86 %singleGoalClaCount:3
% 58.57/58.86 [1]P1(a1,a7)
% 58.57/58.86 [6]~P2(a10,a8)
% 58.57/58.86 [7]~P2(a8,a10)
% 58.57/58.86 [2]P5(f9(a8,a1),a8)
% 58.57/58.86 [3]P5(f9(a11,a1),a10)
% 58.57/58.86 [4]P5(f13(a12,a1),a10)
% 58.57/58.86 [5]P5(f13(a2,a1),a10)
% 58.57/58.86 [8]~P4(f3(a1),a4)
% 58.57/58.86 [9]~P4(f14(a1),a4)
% 58.57/58.86 [10]~P4(f16(a1),a4)
% 58.57/58.86 [15]~P4(x151,a4)+~P4(x151,a18)
% 58.57/58.86 [11]~P1(x111,a7)+P1(f3(x111),a5)
% 58.57/58.86 [12]~P1(x121,a7)+P1(f6(x121),a5)
% 58.65/58.86 [13]~P1(x131,a7)+P1(f14(x131),a15)
% 58.65/58.86 [14]~P1(x141,a7)+P1(f16(x141),a17)
% 58.65/58.86 [20]~P1(x201,a7)+P3(f9(a8,x201),f9(a8,f6(x201)))
% 58.65/58.86 [21]~P1(x211,a7)+P3(f9(a8,x211),f9(a8,f16(x211)))
% 58.65/58.86 [22]~P1(x221,a7)+P3(f9(a11,x221),f9(a11,f6(x221)))
% 58.65/58.86 [23]~P1(x231,a7)+P3(f9(a11,x231),f9(a11,f16(x231)))
% 58.65/58.86 [24]~P1(x241,a7)+P3(f13(a12,x241),f13(a8,f3(x241)))
% 58.65/58.86 [25]~P1(x251,a7)+P3(f13(a2,x251),f13(a8,f6(x251)))
% 58.65/58.86 [26]~P1(x261,a7)+P3(f13(a8,f6(x261)),f9(a8,f14(x261)))
% 58.65/58.86 [27]~P1(x271,a7)+P3(f13(a8,f14(x271)),f9(a11,f3(x271)))
% 58.65/58.86 [28]~P1(x281,a7)+P3(f13(a8,f16(x281)),f9(a8,f3(x281)))
% 58.65/58.86 [16]~P1(x161,x162)+P4(x161,a4)+P4(x161,a18)
% 58.65/58.86 [17]~P5(x173,x172)+P5(x171,x172)+~P3(x173,x171)
% 58.65/58.86 [18]~P5(x183,x182)+P5(x181,x182)+~P3(x181,x183)
% 58.65/58.86 [19]~P5(x193,x191)+P2(x191,x192)+~P5(x193,x192)
% 58.65/58.86 [29]~P4(x291,a18)+~P1(x291,a17)+~P5(f13(a8,x291),a10)+P5(f9(a8,x291),a10)
% 58.65/58.86 [30]~P4(x301,a18)+~P1(x301,a15)+~P5(f13(a8,x301),a8)+P5(f9(a8,x301),a10)
% 58.65/58.86 [31]~P4(x311,a18)+~P1(x311,a5)+~P5(f13(a8,x311),a8)+P5(f9(a8,x311),a8)
% 58.65/58.86 [32]~P4(x321,a18)+~P1(x321,a15)+~P5(f13(a8,x321),a10)+P5(f9(a8,x321),a8)
% 58.65/58.86 [33]~P4(x331,a18)+~P1(x331,a17)+~P5(f13(a8,x331),a10)+P5(f9(a11,x331),a10)
% 58.65/58.86 [34]~P4(x341,a18)+~P1(x341,a5)+~P5(f13(a8,x341),a8)+P5(f9(a11,x341),a8)
% 58.65/58.86 [35]~P4(x351,a18)+~P1(x351,a15)+~P5(f9(a8,x351),a8)+P5(f13(a8,x351),a10)
% 58.65/58.86 [36]~P4(x361,a18)+~P1(x361,a15)+~P5(f9(a8,x361),a10)+P5(f13(a8,x361),a8)
% 58.65/58.86 [37]~P4(x371,a18)+~P1(x371,a5)+~P5(f9(x372,x371),a10)+P5(f13(a8,x371),a10)
% 58.65/58.86 [38]~P4(x381,a18)+~P1(x381,a17)+~P5(f9(x382,x381),a8)+P5(f13(a8,x381),a8)
% 58.65/58.86 [39]~P4(x391,a18)+~P1(x391,a5)+P5(f9(a11,x391),a10)+~P5(f13(a8,x391),a10)+P5(f9(a8,x391),a10)
% 58.65/58.86 [40]~P4(x401,a18)+~P1(x401,a17)+P5(f9(a11,x401),a8)+~P5(f13(a8,x401),a8)+P5(f9(a8,x401),a8)
% 58.65/58.86 [41]~P4(x411,a18)+~P1(x411,a17)+~P5(f9(a8,x411),a10)+~P5(f9(a11,x411),a10)+P5(f13(a8,x411),a10)
% 58.65/58.86 [42]~P4(x421,a18)+~P1(x421,a5)+~P5(f9(a8,x421),a8)+~P5(f9(a11,x421),a8)+P5(f13(a8,x421),a8)
% 58.65/58.86 %EqnAxiom
% 58.65/58.86
% 58.65/58.86 %-------------------------------------------
% 58.74/58.99 cnf(45,plain,
% 58.74/58.99 (~P1(f3(a1),x451)+P4(f3(a1),a18)),
% 58.74/58.99 inference(scs_inference,[],[8,2,19,16])).
% 58.74/58.99 cnf(50,plain,
% 58.74/58.99 (~P1(f14(a1),x501)+P4(f14(a1),a18)),
% 58.74/58.99 inference(scs_inference,[],[9,3,19,16])).
% 58.74/58.99 cnf(55,plain,
% 58.74/58.99 (~P1(f16(a1),x551)+P4(f16(a1),a18)),
% 58.74/58.99 inference(scs_inference,[],[10,4,19,16])).
% 58.74/58.99 cnf(188,plain,
% 58.74/58.99 (P4(f3(a1),a18)),
% 58.74/58.99 inference(scs_inference,[],[1,11,45])).
% 58.74/58.99 cnf(280,plain,
% 58.74/58.99 (P4(f14(a1),a18)),
% 58.74/58.99 inference(scs_inference,[],[1,13,50])).
% 58.74/58.99 cnf(326,plain,
% 58.74/58.99 (P4(f16(a1),a18)),
% 58.74/58.99 inference(scs_inference,[],[1,14,55])).
% 58.74/58.99 cnf(509,plain,
% 58.74/58.99 (P5(f9(a8,f16(a1)),a8)),
% 58.74/58.99 inference(scs_inference,[],[1,2,21,17])).
% 58.74/58.99 cnf(661,plain,
% 58.74/58.99 (P5(f9(a11,f16(a1)),a10)),
% 58.74/58.99 inference(scs_inference,[],[1,3,23,17])).
% 58.74/58.99 cnf(737,plain,
% 58.74/58.99 (P5(f13(a8,f3(a1)),a10)),
% 58.74/58.99 inference(scs_inference,[],[1,4,24,17])).
% 58.74/58.99 cnf(873,plain,
% 58.74/58.99 (P5(f13(a8,f6(a1)),a10)),
% 58.74/58.99 inference(scs_inference,[],[1,5,25,17])).
% 58.74/58.99 cnf(963,plain,
% 58.74/58.99 (P5(f9(a8,f14(a1)),a10)),
% 58.74/58.99 inference(scs_inference,[],[1,873,26,17])).
% 58.74/58.99 cnf(966,plain,
% 58.74/58.99 (~P1(f14(a1),a15)+P5(f13(a8,f14(a1)),a8)),
% 58.74/58.99 inference(scs_inference,[],[280,963,19,36])).
% 58.74/58.99 cnf(1047,plain,
% 58.74/58.99 (P5(f13(a8,f14(a1)),a8)),
% 58.74/58.99 inference(scs_inference,[],[1,966,13])).
% 58.74/58.99 cnf(1165,plain,
% 58.74/58.99 (P5(f9(a11,f3(a1)),a8)),
% 58.74/58.99 inference(scs_inference,[],[1,1047,27,17])).
% 58.74/58.99 cnf(3372,plain,
% 58.74/58.99 (P5(f13(a8,f16(a1)),a8)),
% 58.74/58.99 inference(scs_inference,[],[1,509,326,14,38])).
% 58.74/58.99 cnf(204605,plain,
% 58.74/58.99 (P1(f3(a1),a5)),
% 58.74/58.99 inference(scs_inference,[],[1,11])).
% 58.74/58.99 cnf(204631,plain,
% 58.74/58.99 (P5(f9(a8,f3(a1)),a8)),
% 58.74/58.99 inference(scs_inference,[],[1,3372,11,12,13,14,20,21,22,23,24,25,26,27,28,17])).
% 58.74/58.99 cnf(204633,plain,
% 58.74/58.99 (~P5(f9(a11,f16(a1)),a8)),
% 58.74/58.99 inference(scs_inference,[],[7,661,1,3372,11,12,13,14,20,21,22,23,24,25,26,27,28,17,19])).
% 58.74/58.99 cnf(204637,plain,
% 58.74/58.99 (P5(f13(a8,f3(a1)),a8)),
% 58.74/58.99 inference(scs_inference,[],[7,661,1,188,326,3372,1165,11,12,13,14,20,21,22,23,24,25,26,27,28,17,19,34,42])).
% 58.74/58.99 cnf(204650,plain,
% 58.74/58.99 (~P5(f9(a8,f3(a1)),a10)),
% 58.74/58.99 inference(scs_inference,[],[6,204631,204633,17,18,19])).
% 58.74/58.99 cnf(204656,plain,
% 58.74/58.99 (P5(f9(a11,f3(a1)),a10)),
% 58.74/58.99 inference(scs_inference,[],[6,204605,204631,204637,204633,188,737,17,18,19,30,29,39])).
% 58.74/58.99 cnf(204668,plain,
% 58.74/58.99 ($false),
% 58.74/58.99 inference(scs_inference,[],[204656,204650,7,1165,17,18,19]),
% 58.74/58.99 ['proof']).
% 58.83/59.07 % SZS output end Proof
% 58.83/59.07 % Total time :58.010000s
%------------------------------------------------------------------------------