%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : HWV008-1.001 : TPTP v8.2.0. Released v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% Computer : n020.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:06 EDT 2024
% Result : Unsatisfiable 220.70s 220.75s
% Output : CNFRefutation 221.67s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : HWV008-1.001 : TPTP v8.2.0. Released v2.1.0.
% 0.11/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.12/0.32 % Computer : n020.cluster.edu
% 0.12/0.32 % Model : x86_64 x86_64
% 0.12/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.32 % Memory : 8042.1875MB
% 0.12/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.32 % CPULimit : 300
% 0.12/0.32 % WCLimit : 300
% 0.12/0.32 % DateTime : Fri Jun 21 02:14:39 EDT 2024
% 0.12/0.32 % CPUTime :
% 0.19/0.54 start to proof:theBenchmark
% 220.70/220.70 %-------------------------------------------
% 220.70/220.70 % File :CSE---1.7
% 220.70/220.70 % Problem :theBenchmark
% 220.70/220.70 % Transform :cnf
% 220.70/220.70 % Format :tptp:raw
% 220.70/220.70 % Command :java -jar mcs_scs.jar %d %s
% 220.70/220.70
% 220.70/220.70 % Result :Theorem 220.080000s
% 220.70/220.70 % Output :CNFRefutation 220.080000s
% 220.70/220.70 %-------------------------------------------
% 220.70/220.74 %--------------------------------------------------------------------------
% 220.70/220.74 % File : HWV008-1.001 : TPTP v8.2.0. Released v2.1.0.
% 220.70/220.74 % Domain : Hardware Verification
% 220.70/220.74 % Problem : 1 bit ripple carry adder
% 220.70/220.74 % Version : [Gei96] axioms.
% 220.70/220.74 % English :
% 220.70/220.74
% 220.70/220.74 % Refs : [Gei96] Geisler (1996), Email to G. Sutcliffe
% 220.70/220.74 % Source : [Gei96]
% 220.70/220.74 % Names :
% 220.70/220.74
% 220.70/220.74 % Status : Unsatisfiable
% 220.70/220.74 % Rating : 0.08 v8.2.0, 0.14 v8.1.0, 0.00 v7.5.0, 0.17 v7.4.0, 0.00 v7.1.0, 0.17 v7.0.0, 0.38 v6.3.0, 0.14 v6.2.0, 0.11 v6.1.0, 0.00 v5.0.0, 0.14 v4.1.0, 0.12 v4.0.1, 0.20 v4.0.0, 0.14 v3.4.0, 0.25 v3.3.0, 0.00 v3.1.0, 0.17 v2.7.0, 0.12 v2.6.0, 0.00 v2.2.1, 0.33 v2.1.0
% 220.70/220.74 % Syntax : Number of clauses : 60 ( 11 unt; 3 nHn; 60 RR)
% 220.70/220.74 % Number of literals : 145 ( 0 equ; 88 neg)
% 220.70/220.74 % Maximal clause size : 5 ( 2 avg)
% 220.70/220.74 % Maximal term depth : 4 ( 1 avg)
% 220.70/220.74 % Number of predicates : 5 ( 5 usr; 0 prp; 2-2 aty)
% 220.70/220.74 % Number of functors : 25 ( 25 usr; 15 con; 0-2 aty)
% 220.70/220.74 % Number of variables : 58 ( 3 sgn)
% 220.70/220.74 % SPC : CNF_UNS_RFO_NEQ_NHN
% 220.70/220.74
% 220.70/220.74 % Comments :
% 220.70/220.74 %--------------------------------------------------------------------------
% 220.70/220.74 %----Include basic diagnosis axioms
% 220.70/220.74 include('Axioms/HWV001-0.ax').
% 220.70/220.74 %----Include model of halfadder
% 220.70/220.74 include('Axioms/HWV001-1.ax').
% 220.70/220.74 %----Include model of fulladder
% 220.70/220.74 include('Axioms/HWV001-2.ax').
% 220.70/220.74 %--------------------------------------------------------------------------
% 220.70/220.74 %----Composition of 1-bit adder
% 220.70/220.74 cnf(nbit_adder_fulladder1,axiom,
% 220.70/220.74 ( ~ type(X,nbit_adder(n1))
% 220.70/220.74 | type(v(n1,X),fulladder) ) ).
% 220.70/220.74
% 220.70/220.74 %----Connections of 1-bit adder
% 220.70/220.74 cnf(nbit_adder_connection_out1_out1v1,axiom,
% 220.70/220.74 ( ~ type(X,nbit_adder(n1))
% 220.70/220.74 | connection(out(n1,X),out(s,v(n1,X))) ) ).
% 220.70/220.74
% 220.70/220.74 cnf(nbit_adder_connection_outc_outcv1,axiom,
% 220.70/220.74 ( ~ type(X,nbit_adder(n1))
% 220.70/220.74 | connection(out(c,X),out(c,v(n1,X))) ) ).
% 220.70/220.74
% 220.70/220.74 cnf(nbit_adder_connection_ina1_in1v1,axiom,
% 220.70/220.74 ( ~ type(X,nbit_adder(n1))
% 220.70/220.74 | connection(in(a1,X),in(n1,v(n1,X))) ) ).
% 220.70/220.74
% 220.70/220.74 cnf(nbit_adder_connection_inb1_in2v1,axiom,
% 220.70/220.74 ( ~ type(X,nbit_adder(n1))
% 220.70/220.74 | connection(in(b1,X),in(n2,v(n1,X))) ) ).
% 220.70/220.74
% 220.70/220.74 cnf(nbit_adder_connection_inc_incv1,axiom,
% 220.70/220.74 ( ~ type(X,nbit_adder(n1))
% 220.70/220.74 | connection(in(c,X),in(c,v(n1,X))) ) ).
% 220.70/220.74
% 220.70/220.74 %----Observations
% 220.70/220.74 cnf(a_isa_1bit_adder,hypothesis,
% 220.70/220.74 type(a,nbit_adder(n1)) ).
% 220.70/220.74
% 220.70/220.74 cnf(ina1_0,hypothesis,
% 220.70/220.74 value(in(a1,a),n0) ).
% 220.70/220.74
% 220.70/220.74 cnf(inb1_0,hypothesis,
% 220.70/220.74 value(in(b1,a),n0) ).
% 220.70/220.74
% 220.70/220.74 cnf(inc_0,hypothesis,
% 220.70/220.74 value(in(c,a),n0) ).
% 220.70/220.75
% 220.70/220.75 cnf(out1_0,hypothesis,
% 220.70/220.75 value(out(n1,a),n0) ).
% 220.70/220.75
% 220.70/220.75 cnf(outc_0,hypothesis,
% 220.70/220.75 value(out(c,a),n1) ).
% 220.70/220.75
% 220.70/220.75 %----Minimal diagnosis
% 220.70/220.75 cnf(diagnosis_or1v1,negated_conjecture,
% 220.70/220.75 ~ mode(or1(v(n1,a)),abnormal) ).
% 220.70/220.75
% 220.70/220.75 cnf(diagnosis_and2h1v1,negated_conjecture,
% 220.70/220.75 ~ mode(and2(h1(v(n1,a))),abnormal) ).
% 220.70/220.75
% 220.70/220.75 cnf(diagnosis_and2h2v1,negated_conjecture,
% 220.70/220.75 ~ mode(and2(h2(v(n1,a))),abnormal) ).
% 220.70/220.75
% 220.70/220.75 %--------------------------------------------------------------------------
% 220.70/220.75 %-------------------------------------------
% 220.70/220.75 % Proof found
% 220.70/220.75 % SZS status Theorem for theBenchmark
% 220.70/220.75 % SZS output start Proof
% 220.79/220.78 %ClaNum:60(EqnAxiom:0)
% 220.79/220.78 %VarNum:168(SingletonVarNum:58)
% 220.79/220.78 %MaxLitNum:5
% 220.79/220.78 %MaxfuncDepth:3
% 220.79/220.78 %SharedTerms:38
% 220.79/220.78 %goalClause: 9 10 11
% 220.79/220.78 %singleGoalClaCount:3
% 220.79/220.78 [7]~P2(a15,a2)
% 220.79/220.78 [8]~P2(a2,a15)
% 220.79/220.78 [1]P1(a1,f16(a2))
% 220.79/220.78 [2]P5(f10(a3,a1),a15)
% 220.79/220.78 [3]P5(f10(a4,a1),a15)
% 220.79/220.78 [4]P5(f10(a5,a1),a15)
% 220.79/220.78 [5]P5(f18(a2,a1),a15)
% 220.79/220.78 [6]P5(f18(a3,a1),a2)
% 220.79/220.78 [9]~P4(f19(f24(a2,a1)),a6)
% 220.79/220.78 [10]~P4(f7(f11(f24(a2,a1))),a6)
% 220.79/220.78 [11]~P4(f7(f13(f24(a2,a1))),a6)
% 220.79/220.78 [19]~P4(x191,a6)+~P4(x191,a23)
% 220.79/220.78 [12]~P1(x121,a14)+P1(f8(x121),a9)
% 220.79/220.78 [13]~P1(x131,a14)+P1(f7(x131),a9)
% 220.79/220.78 [14]~P1(x141,a14)+P1(f20(x141),a21)
% 220.79/220.78 [15]~P1(x151,a14)+P1(f19(x151),a22)
% 220.79/220.78 [16]~P1(x161,a12)+P1(f19(x161),a22)
% 220.79/220.78 [17]~P1(x171,a12)+P1(f11(x171),a14)
% 220.79/220.78 [18]~P1(x181,a12)+P1(f13(x181),a14)
% 220.79/220.78 [24]~P1(x241,f16(a2))+P1(f24(a2,x241),a12)
% 220.79/220.78 [25]~P1(x251,a14)+P3(f10(a2,x251),f10(a2,f7(x251)))
% 220.79/220.78 [26]~P1(x261,a14)+P3(f10(a2,x261),f10(a2,f19(x261)))
% 220.79/220.78 [27]~P1(x271,a12)+P3(f10(a2,x271),f10(a2,f13(x271)))
% 220.79/220.78 [28]~P1(x281,a12)+P3(f10(a17,x281),f10(a2,f11(x281)))
% 220.79/220.78 [29]~P1(x291,a14)+P3(f10(a17,x291),f10(a17,f7(x291)))
% 220.79/220.78 [30]~P1(x301,a14)+P3(f10(a17,x301),f10(a17,f19(x301)))
% 220.79/220.78 [31]~P1(x311,a12)+P3(f10(a3,x311),f10(a17,f11(x311)))
% 220.79/220.78 [32]~P1(x321,a14)+P3(f18(a25,x321),f18(a2,f8(x321)))
% 220.79/220.78 [33]~P1(x331,a12)+P3(f18(a25,x331),f18(a25,f13(x331)))
% 220.79/220.78 [34]~P1(x341,a14)+P3(f18(a3,x341),f18(a2,f7(x341)))
% 220.79/220.78 [35]~P1(x351,a12)+P3(f18(a3,x351),f18(a2,f19(x351)))
% 220.79/220.78 [36]~P1(x361,a14)+P3(f18(a2,f7(x361)),f10(a2,f20(x361)))
% 220.79/220.78 [37]~P1(x371,a14)+P3(f18(a2,f20(x371)),f10(a17,f8(x371)))
% 220.79/220.78 [38]~P1(x381,a14)+P3(f18(a2,f19(x381)),f10(a2,f8(x381)))
% 220.79/220.78 [39]~P1(x391,a12)+P3(f18(a25,f11(x391)),f10(a17,f13(x391)))
% 220.79/220.78 [40]~P1(x401,a12)+P3(f18(a3,f11(x401)),f10(a17,f19(x401)))
% 220.79/220.78 [41]~P1(x411,a12)+P3(f18(a3,f13(x411)),f10(a2,f19(x411)))
% 220.79/220.78 [50]~P1(x501,f16(a2))+P3(f10(a3,x501),f10(a3,f24(a2,x501)))
% 220.79/220.78 [51]~P1(x511,f16(a2))+P3(f10(a4,x511),f10(a2,f24(a2,x511)))
% 220.79/220.78 [52]~P1(x521,f16(a2))+P3(f10(a5,x521),f10(a17,f24(a2,x521)))
% 220.79/220.78 [53]~P1(x531,f16(a2))+P3(f18(a2,x531),f18(a25,f24(a2,x531)))
% 220.79/220.78 [54]~P1(x541,f16(a2))+P3(f18(a3,x541),f18(a3,f24(a2,x541)))
% 220.79/220.78 [20]~P1(x201,x202)+P4(x201,a6)+P4(x201,a23)
% 220.79/220.79 [21]~P5(x213,x212)+P5(x211,x212)+~P3(x213,x211)
% 220.79/220.79 [22]~P5(x223,x222)+P5(x221,x222)+~P3(x221,x223)
% 220.79/220.79 [23]~P5(x233,x231)+P2(x231,x232)+~P5(x233,x232)
% 220.79/220.79 [42]~P4(x421,a23)+~P1(x421,a22)+~P5(f18(a2,x421),a15)+P5(f10(a2,x421),a15)
% 220.79/220.79 [43]~P4(x431,a23)+~P1(x431,a21)+~P5(f18(a2,x431),a2)+P5(f10(a2,x431),a15)
% 220.79/220.79 [44]~P4(x441,a23)+~P1(x441,a9)+~P5(f18(a2,x441),a2)+P5(f10(a2,x441),a2)
% 220.79/220.79 [45]~P4(x451,a23)+~P1(x451,a21)+~P5(f18(a2,x451),a15)+P5(f10(a2,x451),a2)
% 220.79/220.79 [46]~P4(x461,a23)+~P1(x461,a22)+~P5(f18(a2,x461),a15)+P5(f10(a17,x461),a15)
% 220.79/220.79 [47]~P4(x471,a23)+~P1(x471,a9)+~P5(f18(a2,x471),a2)+P5(f10(a17,x471),a2)
% 220.79/220.79 [48]~P4(x481,a23)+~P1(x481,a21)+~P5(f10(a2,x481),a2)+P5(f18(a2,x481),a15)
% 220.79/220.79 [49]~P4(x491,a23)+~P1(x491,a21)+~P5(f10(a2,x491),a15)+P5(f18(a2,x491),a2)
% 220.79/220.79 [55]~P4(x551,a23)+~P1(x551,a9)+~P5(f10(x552,x551),a15)+P5(f18(a2,x551),a15)
% 220.79/220.79 [56]~P4(x561,a23)+~P1(x561,a22)+~P5(f10(x562,x561),a2)+P5(f18(a2,x561),a2)
% 220.79/220.79 [57]~P4(x571,a23)+~P1(x571,a9)+P5(f10(a17,x571),a15)+~P5(f18(a2,x571),a15)+P5(f10(a2,x571),a15)
% 220.79/220.79 [58]~P4(x581,a23)+~P1(x581,a22)+P5(f10(a17,x581),a2)+~P5(f18(a2,x581),a2)+P5(f10(a2,x581),a2)
% 220.79/220.79 [59]~P4(x591,a23)+~P1(x591,a22)+~P5(f10(a2,x591),a15)+~P5(f10(a17,x591),a15)+P5(f18(a2,x591),a15)
% 220.79/220.79 [60]~P4(x601,a23)+~P1(x601,a9)+~P5(f10(a2,x601),a2)+~P5(f10(a17,x601),a2)+P5(f18(a2,x601),a2)
% 220.79/220.79 %EqnAxiom
% 220.79/220.79
% 220.79/220.79 %-------------------------------------------
% 221.31/221.29 cnf(63,plain,
% 221.31/221.29 (~P1(f19(f24(a2,a1)),x631)+P4(f19(f24(a2,a1)),a23)),
% 221.31/221.29 inference(scs_inference,[],[9,5,23,20])).
% 221.31/221.29 cnf(68,plain,
% 221.31/221.29 (~P1(f7(f13(f24(a2,a1))),x681)+P4(f7(f13(f24(a2,a1))),a23)),
% 221.31/221.29 inference(scs_inference,[],[11,5,23,20])).
% 221.31/221.29 cnf(73,plain,
% 221.31/221.29 (~P1(f7(f11(f24(a2,a1))),x731)+P4(f7(f11(f24(a2,a1))),a23)),
% 221.31/221.29 inference(scs_inference,[],[10,5,23,20])).
% 221.31/221.29 cnf(206,plain,
% 221.31/221.29 (~P1(x2061,a12)+P1(f8(f11(x2061)),a9)),
% 221.31/221.30 inference(scs_inference,[],[12,17])).
% 221.31/221.30 cnf(252,plain,
% 221.31/221.30 (~P1(x2521,a12)+P1(f7(f13(x2521)),a9)),
% 221.31/221.30 inference(scs_inference,[],[13,18])).
% 221.31/221.30 cnf(298,plain,
% 221.31/221.30 (~P1(x2981,a12)+P1(f20(f11(x2981)),a21)),
% 221.31/221.30 inference(scs_inference,[],[14,17])).
% 221.31/221.30 cnf(344,plain,
% 221.31/221.30 (~P1(x3441,a12)+P1(f19(f13(x3441)),a22)),
% 221.31/221.30 inference(scs_inference,[],[15,18])).
% 221.31/221.30 cnf(390,plain,
% 221.31/221.30 (P1(f19(f24(a2,a1)),a22)),
% 221.31/221.30 inference(scs_inference,[],[1,16,24])).
% 221.31/221.30 cnf(391,plain,
% 221.31/221.30 (P4(f19(f24(a2,a1)),a23)),
% 221.31/221.30 inference(scs_inference,[],[390,63])).
% 221.31/221.30 cnf(480,plain,
% 221.31/221.30 (P4(f7(f13(f24(a2,a1))),a23)+~P1(f24(a2,a1),a12)),
% 221.31/221.30 inference(scs_inference,[],[252,68])).
% 221.31/221.30 cnf(618,plain,
% 221.31/221.30 (~P1(x6181,a12)+P3(f10(a2,f11(x6181)),f10(a2,f7(f11(x6181))))),
% 221.31/221.30 inference(scs_inference,[],[25,17])).
% 221.31/221.30 cnf(664,plain,
% 221.31/221.30 (~P1(x6641,a12)+P3(f10(a2,f13(x6641)),f10(a2,f19(f13(x6641))))),
% 221.31/221.30 inference(scs_inference,[],[26,18])).
% 221.31/221.30 cnf(710,plain,
% 221.31/221.30 (P3(f10(a2,f24(a2,a1)),f10(a2,f13(f24(a2,a1))))),
% 221.31/221.30 inference(scs_inference,[],[1,27,24])).
% 221.31/221.30 cnf(720,plain,
% 221.31/221.30 (~P5(f10(a2,f13(f24(a2,a1))),x7201)+P5(f10(a2,f24(a2,a1)),x7201)),
% 221.31/221.30 inference(scs_inference,[],[710,5,23,22])).
% 221.31/221.30 cnf(764,plain,
% 221.31/221.30 (P3(f10(a17,f24(a2,a1)),f10(a2,f11(f24(a2,a1))))),
% 221.31/221.30 inference(scs_inference,[],[1,28,24])).
% 221.31/221.30 cnf(818,plain,
% 221.31/221.30 (~P1(x8181,a12)+P3(f10(a17,f11(x8181)),f10(a17,f7(f11(x8181))))),
% 221.31/221.30 inference(scs_inference,[],[29,17])).
% 221.31/221.30 cnf(864,plain,
% 221.31/221.30 (~P1(x8641,a12)+P3(f10(a17,f13(x8641)),f10(a17,f19(f13(x8641))))),
% 221.31/221.30 inference(scs_inference,[],[30,18])).
% 221.31/221.30 cnf(910,plain,
% 221.31/221.30 (P3(f10(a3,f24(a2,a1)),f10(a17,f11(f24(a2,a1))))),
% 221.31/221.30 inference(scs_inference,[],[1,31,24])).
% 221.31/221.30 cnf(964,plain,
% 221.31/221.30 (~P1(x9641,a12)+P3(f18(a25,f11(x9641)),f18(a2,f8(f11(x9641))))),
% 221.31/221.30 inference(scs_inference,[],[32,17])).
% 221.31/221.30 cnf(1064,plain,
% 221.31/221.30 (~P1(x10641,a12)+P3(f18(a3,f13(x10641)),f18(a2,f7(f13(x10641))))),
% 221.31/221.30 inference(scs_inference,[],[34,18])).
% 221.31/221.30 cnf(1110,plain,
% 221.31/221.30 (P3(f18(a3,f24(a2,a1)),f18(a2,f19(f24(a2,a1))))),
% 221.31/221.30 inference(scs_inference,[],[1,35,24])).
% 221.31/221.30 cnf(1122,plain,
% 221.31/221.30 (~P5(f18(a2,f19(f24(a2,a1))),x11221)+P5(f18(a3,f24(a2,a1)),x11221)),
% 221.31/221.30 inference(scs_inference,[],[1110,5,23,22])).
% 221.31/221.30 cnf(1168,plain,
% 221.31/221.30 (~P1(x11681,a12)+P3(f18(a2,f7(f11(x11681))),f10(a2,f20(f11(x11681))))),
% 221.31/221.30 inference(scs_inference,[],[36,17])).
% 221.31/221.30 cnf(1214,plain,
% 221.31/221.30 (~P1(x12141,a12)+P3(f18(a2,f20(f13(x12141))),f10(a17,f8(f13(x12141))))),
% 221.31/221.30 inference(scs_inference,[],[37,18])).
% 221.31/221.30 cnf(1260,plain,
% 221.31/221.30 (~P1(x12601,a12)+P3(f18(a2,f19(f11(x12601))),f10(a2,f8(f11(x12601))))),
% 221.31/221.30 inference(scs_inference,[],[38,17])).
% 221.31/221.30 cnf(1352,plain,
% 221.31/221.30 (P3(f18(a3,f11(f24(a2,a1))),f10(a17,f19(f24(a2,a1))))),
% 221.31/221.30 inference(scs_inference,[],[1,40,24])).
% 221.31/221.30 cnf(1398,plain,
% 221.31/221.30 (P3(f18(a3,f13(f24(a2,a1))),f10(a2,f19(f24(a2,a1))))),
% 221.31/221.30 inference(scs_inference,[],[1,41,24])).
% 221.31/221.30 cnf(1444,plain,
% 221.31/221.30 (P4(f7(f13(f24(a2,a1))),a23)),
% 221.31/221.30 inference(scs_inference,[],[1,480,24])).
% 221.31/221.30 cnf(1490,plain,
% 221.31/221.30 (P5(f10(a3,f24(a2,a1)),a15)),
% 221.31/221.30 inference(scs_inference,[],[1,2,50,21])).
% 221.31/221.30 cnf(1493,plain,
% 221.31/221.30 (P5(f10(a17,f11(f24(a2,a1))),a15)),
% 221.31/221.30 inference(scs_inference,[],[2,910,1490,23,21])).
% 221.31/221.30 cnf(1538,plain,
% 221.31/221.30 (P5(f10(a2,f24(a2,a1)),a15)),
% 221.31/221.30 inference(scs_inference,[],[1,3,51,21])).
% 221.31/221.30 cnf(1541,plain,
% 221.31/221.30 (P5(f10(a2,f13(f24(a2,a1))),a15)),
% 221.31/221.30 inference(scs_inference,[],[2,710,1538,23,21])).
% 221.31/221.30 cnf(1586,plain,
% 221.31/221.30 (P5(f10(a17,f24(a2,a1)),a15)),
% 221.31/221.30 inference(scs_inference,[],[1,4,52,21])).
% 221.31/221.30 cnf(1589,plain,
% 221.31/221.30 (P5(f10(a2,f11(f24(a2,a1))),a15)),
% 221.31/221.30 inference(scs_inference,[],[2,764,1586,23,21])).
% 221.31/221.30 cnf(1682,plain,
% 221.31/221.30 (P5(f18(a3,f24(a2,a1)),a2)),
% 221.31/221.30 inference(scs_inference,[],[1,6,54,21])).
% 221.31/221.30 cnf(1683,plain,
% 221.31/221.30 (P5(f18(a2,f19(f24(a2,a1))),a2)),
% 221.31/221.30 inference(scs_inference,[],[1110,1682,21])).
% 221.31/221.30 cnf(1806,plain,
% 221.31/221.30 (P5(f10(a2,f7(f11(f24(a2,a1)))),a15)+~P1(f24(a2,a1),a12)),
% 221.31/221.30 inference(scs_inference,[],[1589,618,21])).
% 221.31/221.30 cnf(1928,plain,
% 221.31/221.30 (P5(f10(a2,f19(f13(f24(a2,a1)))),a15)+~P1(f24(a2,a1),a12)),
% 221.31/221.30 inference(scs_inference,[],[1541,664,21])).
% 221.31/221.30 cnf(2028,plain,
% 221.31/221.30 (P5(f10(a17,f7(f11(f24(a2,a1)))),a15)+~P1(f24(a2,a1),a12)),
% 221.31/221.30 inference(scs_inference,[],[1493,818,21])).
% 221.31/221.30 cnf(2340,plain,
% 221.31/221.30 (~P5(f18(a2,f7(f13(x23401))),x23402)+P5(f18(a3,f13(x23401)),x23402)+~P1(x23401,a12)),
% 221.31/221.30 inference(scs_inference,[],[1064,22])).
% 221.31/221.30 cnf(2441,plain,
% 221.31/221.30 (P4(f7(f11(f24(a2,a1))),a23)+~P1(f11(f24(a2,a1)),a14)),
% 221.31/221.30 inference(scs_inference,[],[73,13])).
% 221.31/221.30 cnf(2542,plain,
% 221.31/221.30 (P4(f7(f11(f24(a2,a1))),a23)+~P1(f24(a2,a1),a12)),
% 221.31/221.30 inference(scs_inference,[],[2441,17])).
% 221.31/221.30 cnf(2643,plain,
% 221.31/221.30 (P4(f7(f11(f24(a2,a1))),a23)),
% 221.31/221.30 inference(scs_inference,[],[1,2542,24])).
% 221.31/221.30 cnf(6002,plain,
% 221.31/221.30 (~P5(f18(a3,f13(x60021)),a15)+~P5(f18(a2,f7(f13(x60021))),a2)+~P1(x60021,a12)),
% 221.31/221.30 inference(scs_inference,[],[8,2340,23])).
% 221.31/221.30 cnf(9292,plain,
% 221.31/221.30 (~P1(x92921,a12)+P1(f7(f11(x92921)),a9)),
% 221.31/221.30 inference(scs_inference,[],[13,17])).
% 221.31/221.30 cnf(9380,plain,
% 221.31/221.30 (~P1(f24(a2,a1),a12)+~P5(f18(a2,f7(f11(f24(a2,a1)))),a2)+P5(f10(a2,f7(f11(f24(a2,a1)))),a2)),
% 221.31/221.30 inference(scs_inference,[],[2643,9292,44])).
% 221.31/221.30 cnf(10777,plain,
% 221.31/221.30 (~P1(x107771,a12)+P1(f19(f11(x107771)),a22)),
% 221.31/221.30 inference(scs_inference,[],[15,17])).
% 221.31/221.30 cnf(145685,plain,
% 221.31/221.30 (P1(f24(a2,a1),a12)),
% 221.31/221.30 inference(scs_inference,[],[1,24])).
% 221.31/221.30 cnf(145697,plain,
% 221.31/221.30 (P5(f10(a2,f7(f11(f24(a2,a1)))),a15)),
% 221.31/221.30 inference(scs_inference,[],[1,24,50,51,52,53,54,1806])).
% 221.31/221.30 cnf(145698,plain,
% 221.31/221.30 (P5(f10(a2,f19(f13(f24(a2,a1)))),a15)),
% 221.31/221.30 inference(scs_inference,[],[1,24,50,51,52,53,54,1806,1928])).
% 221.31/221.30 cnf(145699,plain,
% 221.31/221.30 (P5(f10(a17,f7(f11(f24(a2,a1)))),a15)),
% 221.31/221.30 inference(scs_inference,[],[1,24,50,51,52,53,54,1806,1928,2028])).
% 221.31/221.30 cnf(145700,plain,
% 221.31/221.30 (~P5(f10(a17,f11(f24(a2,a1))),a2)),
% 221.31/221.30 inference(scs_inference,[],[8,1,1493,24,50,51,52,53,54,1806,1928,2028,23])).
% 221.31/221.30 cnf(145702,plain,
% 221.31/221.30 (P1(f11(f24(a2,a1)),a14)),
% 221.31/221.30 inference(scs_inference,[],[8,1,1493,24,50,51,52,53,54,1806,1928,2028,23,17])).
% 221.31/221.30 cnf(145704,plain,
% 221.31/221.30 (P1(f13(f24(a2,a1)),a14)),
% 221.31/221.30 inference(scs_inference,[],[8,1,1493,24,50,51,52,53,54,1806,1928,2028,23,17,18])).
% 221.31/221.30 cnf(145708,plain,
% 221.31/221.30 (P1(f7(f13(f24(a2,a1))),a9)),
% 221.31/221.30 inference(scs_inference,[],[8,1,1493,24,50,51,52,53,54,1806,1928,2028,23,17,18,206,252])).
% 221.31/221.30 cnf(145723,plain,
% 221.31/221.30 (P5(f18(a2,f7(f11(f24(a2,a1)))),a15)),
% 221.31/221.30 inference(scs_inference,[],[2643,8,1,1493,1682,24,50,51,52,53,54,1806,1928,2028,23,17,18,206,252,298,344,9292,10777,9380,21,22,55])).
% 221.31/221.30 cnf(145733,plain,
% 221.31/221.30 (~P5(f18(a3,f24(a2,a1)),a15)),
% 221.31/221.30 inference(scs_inference,[],[7,145700,1682,21,22,23])).
% 221.31/221.30 cnf(145735,plain,
% 221.31/221.30 (~P5(f18(a2,f19(f24(a2,a1))),a15)),
% 221.31/221.30 inference(scs_inference,[],[7,145700,1682,21,22,23,1122])).
% 221.31/221.30 cnf(145811,plain,
% 221.31/221.30 (~P5(f10(a2,f13(f24(a2,a1))),a2)),
% 221.31/221.30 inference(scs_inference,[],[145685,145700,8,1538,1682,22,21,20,23,720])).
% 221.31/221.30 cnf(145840,plain,
% 221.31/221.30 (~P5(f10(a3,a1),a2)),
% 221.31/221.30 inference(scs_inference,[],[145811,8,1,1682,2,22,21,20,23])).
% 221.31/221.30 cnf(145870,plain,
% 221.31/221.30 (~P5(f10(a4,a1),a2)),
% 221.31/221.30 inference(scs_inference,[],[145840,8,1682,3,22,21,23])).
% 221.31/221.30 cnf(145895,plain,
% 221.31/221.30 (~P5(f10(a5,a1),a2)),
% 221.31/221.30 inference(scs_inference,[],[145870,8,1682,4,22,21,23])).
% 221.31/221.30 cnf(145922,plain,
% 221.31/221.30 (~P5(f18(a3,a1),a15)),
% 221.31/221.30 inference(scs_inference,[],[7,145895,1682,6,22,21,23])).
% 221.31/221.30 cnf(193210,plain,
% 221.31/221.30 (P3(f18(a3,f13(f24(a2,a1))),f18(a2,f7(f13(f24(a2,a1)))))),
% 221.31/221.30 inference(scs_inference,[],[145685,618,664,818,864,964,1064])).
% 221.31/221.30 cnf(193222,plain,
% 221.31/221.30 (P5(f18(a3,f13(f24(a2,a1))),x1932221)+~P5(f18(a2,f7(f13(f24(a2,a1)))),x1932221)),
% 221.31/221.30 inference(scs_inference,[],[145698,8,145685,145922,618,664,818,864,964,1064,1168,1214,1260,21,23,2340])).
% 221.31/221.30 cnf(193224,plain,
% 221.31/221.30 (~P5(f18(a2,f7(f13(f24(a2,a1)))),a15)+~P5(f18(a2,f7(f13(f24(a2,a1)))),a2)),
% 221.31/221.30 inference(scs_inference,[],[145698,8,145685,145922,618,664,818,864,964,1064,1168,1214,1260,21,23,2340,6002])).
% 221.31/221.30 cnf(193229,plain,
% 221.31/221.30 (~P5(f18(a2,f7(f11(f24(a2,a1)))),a2)),
% 221.31/221.30 inference(scs_inference,[],[145698,145723,8,145733,21,23])).
% 221.31/221.30 cnf(193255,plain,
% 221.31/221.30 (~P5(f10(a2,f7(f11(f24(a2,a1)))),a2)),
% 221.31/221.30 inference(scs_inference,[],[145699,145697,8,145922,21,23])).
% 221.31/221.30 cnf(193263,plain,
% 221.31/221.30 (P5(f18(a3,f11(f24(a2,a1))),a2)+P5(f10(a2,f19(f24(a2,a1))),a2)),
% 221.31/221.30 inference(scs_inference,[],[145699,1352,145723,145697,390,8,391,1683,2643,145922,21,23,45,22,47,58])).
% 221.31/221.30 cnf(193270,plain,
% 221.31/221.30 (~P5(f10(a2,f19(f24(a2,a1))),x1932701)+P5(f18(a3,f13(f24(a2,a1))),x1932701)),
% 221.31/221.30 inference(scs_inference,[],[145699,1398,193255,145723,2643,145733,21,45,22])).
% 221.31/221.30 cnf(193604,plain,
% 221.31/221.30 (~P5(f18(a3,f13(f24(a2,a1))),x1936041)+P5(f10(a2,f19(f24(a2,a1))),x1936041)),
% 221.31/221.30 inference(scs_inference,[],[145735,2,193229,145697,2643,1398,22,49,21])).
% 221.31/221.30 cnf(193608,plain,
% 221.31/221.30 (~P5(f18(a3,f13(f24(a2,a1))),a15)+~P5(f10(a17,f19(f24(a2,a1))),a15)),
% 221.31/221.30 inference(scs_inference,[],[145735,391,2,390,193229,145697,2643,1398,22,49,21,55,59])).
% 221.31/221.30 cnf(193667,plain,
% 221.31/221.30 (~P5(f18(a2,f7(f13(f24(a2,a1)))),a15)+~P5(f18(a3,f13(f24(a2,a1))),a2)),
% 221.31/221.30 inference(scs_inference,[],[145735,2,8,193229,145697,2643,193210,22,49,21,23])).
% 221.31/221.30 cnf(194633,plain,
% 221.31/221.30 (~P5(f10(a17,f19(f24(a2,a1))),a15)+~P5(f18(a2,f7(f13(f24(a2,a1)))),a15)),
% 221.31/221.30 inference(scs_inference,[],[193608,193222])).
% 221.31/221.30 cnf(321997,plain,
% 221.31/221.30 (P3(f10(a2,f13(f24(a2,a1))),f10(a2,f7(f13(f24(a2,a1)))))),
% 221.31/221.30 inference(scs_inference,[],[145704,25])).
% 221.31/221.30 cnf(322007,plain,
% 221.31/221.30 (P3(f18(a3,f11(f24(a2,a1))),f18(a2,f7(f11(f24(a2,a1)))))),
% 221.31/221.30 inference(scs_inference,[],[145702,145704,25,26,29,30,32,34])).
% 221.31/221.30 cnf(322057,plain,
% 221.31/221.30 (P5(f18(a3,f11(f24(a2,a1))),a2)),
% 221.31/221.30 inference(scs_inference,[],[391,1444,1683,145735,2643,145723,390,193229,1541,145708,145697,7,321997,22,21,49,55,194633,193667,193224,193222,193270,23,44,46,45,58,193604,193263])).
% 221.31/221.30 cnf(322116,plain,
% 221.31/221.30 ($false),
% 221.31/221.30 inference(scs_inference,[],[145735,145723,193229,322007,322057,22,21]),
% 221.31/221.30 ['proof']).
% 221.67/221.60 % SZS output end Proof
% 221.67/221.60 % Total time :220.080000s
%------------------------------------------------------------------------------