%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : MGT058-1 : TPTP v9.3.0. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 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 : Tue Sep 8 06:04:22 AM UTC 2026
% Result : Unsatisfiable 1.80s 2.09s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : MGT058-1 : TPTP v9.3.0. Released v2.4.0.
% 0.00/0.01 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 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 : Mon Sep 7 13:31:56 UTC 2026
% 0.04/0.30 % CPUTime :
% 0.09/0.39 start to proof:theBenchmark
% 1.80/2.09 %-------------------------------------------
% 1.80/2.09 % File :CSE---1.7
% 1.80/2.09 % Problem :theBenchmark
% 1.80/2.09 % Transform :cnf
% 1.80/2.09 % Format :tptp:raw
% 1.80/2.09 % Command :java -jar mcs_scs.jar %d %s
% 1.80/2.09
% 1.80/2.09 % Result :Theorem 1.706693s
% 1.80/2.09 % Output :CNFRefutation 1.706693s
% 1.80/2.09 %-------------------------------------------
% 1.80/2.09 %--------------------------------------------------------------------------
% 1.80/2.09 % File : MGT058-1 : TPTP v9.3.0. Released v2.4.0.
% 1.80/2.09 % Domain : Management (Organisation Theory)
% 1.80/2.09 % Problem : An organization's position cannot be both fragile and robust
% 1.80/2.09 % Version : [Han98] axioms.
% 1.80/2.09 % English :
% 1.80/2.09
% 1.80/2.09 % Refs : [Kam00] Kamps (2000), Email to G. Sutcliffe
% 1.80/2.09 % : [CH00] Carroll & Hannan (2000), The Demography of Corporation
% 1.80/2.09 % : [Han98] Hannan (1998), Rethinking Age Dependence in Organizati
% 1.80/2.09 % Source : [TPTP]
% 1.80/2.09 % Names :
% 1.80/2.09
% 1.80/2.09 % Status : Unsatisfiable
% 1.80/2.09 % Rating : 0.08 v9.3.0, 0.05 v9.0.0, 0.10 v8.1.0, 0.00 v7.5.0, 0.05 v7.4.0, 0.12 v7.3.0, 0.08 v7.1.0, 0.00 v7.0.0, 0.13 v6.4.0, 0.07 v6.3.0, 0.00 v6.2.0, 0.10 v6.1.0, 0.14 v6.0.0, 0.10 v5.5.0, 0.15 v5.3.0, 0.11 v5.2.0, 0.12 v5.0.0, 0.07 v4.1.0, 0.00 v4.0.1, 0.09 v4.0.0, 0.00 v3.4.0, 0.08 v3.3.0, 0.14 v3.2.0, 0.23 v3.1.0, 0.27 v2.7.0, 0.25 v2.6.0, 0.22 v2.5.0, 0.33 v2.4.0
% 1.80/2.09 % Syntax : Number of clauses : 29 ( 6 unt; 11 nHn; 24 RR)
% 1.80/2.09 % Number of literals : 68 ( 6 equ; 26 neg)
% 1.80/2.09 % Maximal clause size : 3 ( 2 avg)
% 1.80/2.09 % Maximal term depth : 3 ( 1 avg)
% 1.80/2.09 % Number of predicates : 9 ( 8 usr; 0 prp; 1-2 aty)
% 1.80/2.09 % Number of functors : 8 ( 8 usr; 5 con; 0-2 aty)
% 1.80/2.09 % Number of variables : 39 ( 0 sgn)
% 1.80/2.09 % SPC : CNF_UNS_RFO_SEQ_NHN
% 1.80/2.09
% 1.80/2.09 % Comments : See MGT042+1.p for the mnemonic names.
% 1.80/2.09 % : Created with tptp2X -f tptp -t clausify:otter MGT058+1.p
% 1.80/2.09 %--------------------------------------------------------------------------
% 1.80/2.09 include('Axioms/MGT001-0.ax').
% 1.80/2.09 %--------------------------------------------------------------------------
% 1.80/2.09 cnf(definition_3_30,axiom,
% 1.80/2.09 ( ~ fragile_position(A)
% 1.80/2.09 | ~ smaller_or_equal(age(A,B),sigma)
% 1.80/2.09 | positional_advantage(A,B) ) ).
% 1.80/2.09
% 1.80/2.09 cnf(definition_3_31,axiom,
% 1.80/2.09 ( ~ fragile_position(A)
% 1.80/2.09 | ~ greater(age(A,B),sigma)
% 1.80/2.09 | ~ positional_advantage(A,B) ) ).
% 1.80/2.09
% 1.80/2.09 cnf(definition_3_32,axiom,
% 1.80/2.09 ( smaller_or_equal(age(A,sk1(A)),sigma)
% 1.80/2.09 | greater(age(A,sk1(A)),sigma)
% 1.80/2.09 | fragile_position(A) ) ).
% 1.80/2.09
% 1.80/2.09 cnf(definition_3_33,axiom,
% 1.80/2.09 ( smaller_or_equal(age(A,sk1(A)),sigma)
% 1.80/2.09 | positional_advantage(A,sk1(A))
% 1.80/2.09 | fragile_position(A) ) ).
% 1.80/2.09
% 1.80/2.09 cnf(definition_3_34,axiom,
% 1.80/2.09 ( ~ positional_advantage(A,sk1(A))
% 1.80/2.09 | greater(age(A,sk1(A)),sigma)
% 1.80/2.09 | fragile_position(A) ) ).
% 1.80/2.09
% 1.80/2.09 cnf(definition_3_35,axiom,
% 1.80/2.09 ( ~ positional_advantage(A,sk1(A))
% 1.80/2.09 | positional_advantage(A,sk1(A))
% 1.80/2.09 | fragile_position(A) ) ).
% 1.80/2.09
% 1.80/2.09 cnf(definition_4_36,axiom,
% 1.80/2.09 ( ~ robust_position(A)
% 1.80/2.09 | ~ smaller_or_equal(age(A,B),tau)
% 1.80/2.09 | ~ positional_advantage(A,B) ) ).
% 1.80/2.09
% 1.80/2.09 cnf(definition_4_37,axiom,
% 1.80/2.09 ( ~ robust_position(A)
% 1.80/2.09 | ~ greater(age(A,B),tau)
% 1.80/2.09 | positional_advantage(A,B) ) ).
% 1.80/2.09
% 1.80/2.09 cnf(definition_4_38,axiom,
% 1.80/2.09 ( smaller_or_equal(age(A,sk2(A)),tau)
% 1.80/2.09 | greater(age(A,sk2(A)),tau)
% 1.80/2.09 | robust_position(A) ) ).
% 1.80/2.09
% 1.80/2.09 cnf(definition_4_39,axiom,
% 1.80/2.09 ( smaller_or_equal(age(A,sk2(A)),tau)
% 1.80/2.09 | ~ positional_advantage(A,sk2(A))
% 1.80/2.09 | robust_position(A) ) ).
% 1.80/2.09
% 1.80/2.09 cnf(definition_4_40,axiom,
% 1.80/2.09 ( positional_advantage(A,sk2(A))
% 1.80/2.09 | greater(age(A,sk2(A)),tau)
% 1.80/2.09 | robust_position(A) ) ).
% 1.80/2.09
% 1.80/2.09 cnf(definition_4_41,axiom,
% 1.80/2.09 ( positional_advantage(A,sk2(A))
% 1.80/2.09 | ~ positional_advantage(A,sk2(A))
% 1.80/2.09 | robust_position(A) ) ).
% 1.80/2.09
% 1.80/2.09 cnf(lemma_10_42,negated_conjecture,
% 1.80/2.09 organization(sk3) ).
% 1.80/2.09
% 1.80/2.09 cnf(lemma_10_43,negated_conjecture,
% 1.80/2.09 age(sk3,sk4) = zero ).
% 1.80/2.09
% 1.80/2.09 cnf(lemma_10_44,negated_conjecture,
% 1.80/2.09 greater_or_equal(sigma,zero) ).
% 1.80/2.09
% 1.80/2.09 cnf(lemma_10_45,negated_conjecture,
% 1.80/2.09 greater_or_equal(tau,zero) ).
% 1.80/2.09
% 1.80/2.09 cnf(lemma_10_46,negated_conjecture,
% 1.80/2.09 fragile_position(sk3) ).
% 1.80/2.09
% 1.80/2.09 cnf(lemma_10_47,negated_conjecture,
% 1.80/2.09 robust_position(sk3) ).
% 1.80/2.09
% 1.80/2.09 %--------------------------------------------------------------------------
% 1.80/2.09 %-------------------------------------------
% 1.80/2.09 % Proof found
% 1.80/2.09 % SZS status Theorem for theBenchmark
% 1.80/2.09 % SZS output start Proof
% 1.80/2.09 %ClaNum:47(EqnAxiom:20)
% 1.80/2.09 %VarNum:102(SingletonVarNum:37)
% 1.80/2.09 %MaxLitNum:3
% 1.80/2.09 %MaxfuncDepth:2
% 1.80/2.09 %SharedTerms:12
% 1.80/2.09 %goalClause: 21 22 23 24 25 26
% 1.80/2.09 %singleGoalClaCount:6
% 1.80/2.09 [21]P1(a1)
% 1.80/2.09 [22]P2(a1)
% 1.80/2.09 [23]P3(a1)
% 1.80/2.09 [25]P4(a3,a7)
% 1.80/2.09 [26]P4(a8,a7)
% 1.80/2.09 [24]E(f2(a1,a6),a7)
% 1.80/2.09 [27]~E(x271,x272)+P7(x271,x272)
% 1.80/2.09 [28]~E(x281,x282)+P4(x281,x282)
% 1.80/2.09 [30]~P8(x301,x302)+P7(x301,x302)
% 1.80/2.09 [31]~P5(x312,x311)+P8(x311,x312)
% 1.80/2.09 [32]~P5(x321,x322)+P4(x321,x322)
% 1.80/2.09 [33]~P8(x332,x331)+P5(x331,x332)
% 1.80/2.09 [36]~P5(x362,x361)+~P5(x361,x362)
% 1.80/2.09 [38]P1(x381)+P6(x381,f4(x381))+P7(f2(x381,f4(x381)),a3)
% 1.80/2.09 [39]P2(x391)+P6(x391,f5(x391))+P5(f2(x391,f5(x391)),a8)
% 1.80/2.09 [42]P1(x421)+~P6(x421,f4(x421))+P5(f2(x421,f4(x421)),a3)
% 1.80/2.09 [43]P2(x431)+~P6(x431,f5(x431))+P7(f2(x431,f5(x431)),a8)
% 1.80/2.09 [46]P1(x461)+P7(f2(x461,f4(x461)),a3)+P5(f2(x461,f4(x461)),a3)
% 1.80/2.09 [47]P2(x471)+P7(f2(x471,f5(x471)),a8)+P5(f2(x471,f5(x471)),a8)
% 1.80/2.09 [29]P8(x291,x292)+P5(x291,x292)+E(x291,x292)
% 1.80/2.09 [34]P8(x341,x342)+~P7(x341,x342)+E(x341,x342)
% 1.80/2.09 [35]P5(x351,x352)+~P4(x351,x352)+E(x351,x352)
% 1.80/2.09 [40]~P1(x401)+P6(x401,x402)+~P7(f2(x401,x402),a3)
% 1.80/2.09 [41]~P2(x411)+P6(x411,x412)+~P5(f2(x411,x412),a8)
% 1.80/2.09 [44]~P1(x441)+~P6(x441,x442)+~P5(f2(x441,x442),a3)
% 1.80/2.09 [45]~P2(x451)+~P6(x451,x452)+~P7(f2(x451,x452),a8)
% 1.80/2.09 [37]~P5(x371,x373)+P5(x371,x372)+~P5(x373,x372)
% 1.80/2.09 %EqnAxiom
% 1.80/2.09 [1]E(x11,x11)
% 1.80/2.09 [2]E(x22,x21)+~E(x21,x22)
% 1.80/2.09 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 1.80/2.09 [4]~E(x41,x42)+E(f2(x41,x43),f2(x42,x43))
% 1.80/2.09 [5]~E(x51,x52)+E(f2(x53,x51),f2(x53,x52))
% 1.80/2.09 [6]~E(x61,x62)+E(f4(x61),f4(x62))
% 1.80/2.09 [7]~E(x71,x72)+E(f5(x71),f5(x72))
% 1.80/2.09 [8]~P1(x81)+P1(x82)+~E(x81,x82)
% 1.80/2.09 [9]~P2(x91)+P2(x92)+~E(x91,x92)
% 1.80/2.09 [10]~P3(x101)+P3(x102)+~E(x101,x102)
% 1.80/2.09 [11]P4(x112,x113)+~E(x111,x112)+~P4(x111,x113)
% 1.80/2.09 [12]P4(x123,x122)+~E(x121,x122)+~P4(x123,x121)
% 1.80/2.09 [13]P6(x132,x133)+~E(x131,x132)+~P6(x131,x133)
% 1.80/2.09 [14]P6(x143,x142)+~E(x141,x142)+~P6(x143,x141)
% 1.80/2.09 [15]P7(x152,x153)+~E(x151,x152)+~P7(x151,x153)
% 1.80/2.09 [16]P7(x163,x162)+~E(x161,x162)+~P7(x163,x161)
% 1.80/2.09 [17]P5(x172,x173)+~E(x171,x172)+~P5(x171,x173)
% 1.80/2.09 [18]P5(x183,x182)+~E(x181,x182)+~P5(x183,x181)
% 1.80/2.09 [19]P8(x192,x193)+~E(x191,x192)+~P8(x191,x193)
% 1.80/2.09 [20]P8(x203,x202)+~E(x201,x202)+~P8(x203,x201)
% 1.80/2.09
% 1.80/2.09 %-------------------------------------------
% 1.80/2.09 cnf(48,plain,
% 1.80/2.09 (P7(x481,x481)),
% 1.80/2.09 inference(equality_inference,[],[27])).
% 1.80/2.09 cnf(49,plain,
% 1.80/2.09 (P4(x491,x491)),
% 1.80/2.09 inference(equality_inference,[],[28])).
% 1.80/2.09 cnf(50,plain,
% 1.80/2.09 (E(a7,f2(a1,a6))),
% 1.80/2.09 inference(scs_inference,[],[24,2])).
% 1.80/2.09 cnf(55,plain,
% 1.80/2.09 (P7(x551,x551)),
% 1.80/2.09 inference(rename_variables,[],[48])).
% 1.80/2.09 cnf(61,plain,
% 1.80/2.09 (E(a3,a7)+P5(a3,a7)),
% 1.80/2.09 inference(scs_inference,[],[25,24,48,55,49,2,11,12,15,16,8,9,10,35])).
% 1.80/2.09 cnf(63,plain,
% 1.80/2.09 (P4(a8,f2(a1,a6))),
% 1.80/2.09 inference(scs_inference,[],[26,50,12])).
% 1.80/2.09 cnf(76,plain,
% 1.80/2.09 (E(a8,f2(a1,a6))+P5(a8,f2(a1,a6))),
% 1.80/2.09 inference(scs_inference,[],[63,35])).
% 1.80/2.09 cnf(113,plain,
% 1.80/2.09 (~P5(a7,a3)+E(a3,a7)),
% 1.80/2.09 inference(scs_inference,[],[36,61])).
% 1.80/2.09 cnf(119,plain,
% 1.80/2.09 (P7(a7,a3)+~P5(a7,a3)),
% 1.80/2.09 inference(scs_inference,[],[48,113,15])).
% 1.80/2.09 cnf(122,plain,
% 1.80/2.09 (E(a7,a3)+P8(a7,a3)+~P5(a7,a3)),
% 1.80/2.09 inference(scs_inference,[],[119,34])).
% 1.80/2.09 cnf(175,plain,
% 1.80/2.09 (P5(a7,x1751)+~P8(x1751,f2(a1,a6))+~E(f2(a1,a6),a7)),
% 1.80/2.09 inference(scs_inference,[],[24,17,33])).
% 1.80/2.09 cnf(176,plain,
% 1.80/2.09 (~P8(x1761,f2(a1,a6))+P5(a7,x1761)),
% 1.80/2.09 inference(scs_inference,[],[24,175])).
% 1.80/2.09 cnf(177,plain,
% 1.80/2.09 (P5(a7,a7)+~P8(f2(a1,a6),f2(a1,a6))),
% 1.80/2.09 inference(scs_inference,[],[24,175,18])).
% 1.80/2.09 cnf(183,plain,
% 1.80/2.09 (~P5(f2(a1,a6),x1831)+P5(a7,x1831)),
% 1.80/2.09 inference(scs_inference,[],[176,31])).
% 1.80/2.09 cnf(191,plain,
% 1.80/2.09 (~P8(f2(a1,a6),a7)+P5(a7,a7)),
% 1.80/2.09 inference(scs_inference,[],[50,177,20])).
% 1.80/2.09 cnf(192,plain,
% 1.80/2.09 (~P8(f2(a1,a6),a7)),
% 1.80/2.09 inference(scs_inference,[],[191,36])).
% 1.80/2.09 cnf(195,plain,
% 1.80/2.09 (~P8(f2(a1,a6),f2(a1,a6))),
% 1.80/2.09 inference(scs_inference,[],[192,31,176])).
% 1.80/2.09 cnf(197,plain,
% 1.80/2.09 (~P5(f2(a1,a6),f2(a1,a6))),
% 1.80/2.09 inference(scs_inference,[],[192,31,176,183])).
% 1.80/2.09 cnf(199,plain,
% 1.80/2.09 (~P5(f2(a1,a6),a7)),
% 1.80/2.09 inference(scs_inference,[],[195,50,19,31])).
% 1.80/2.09 cnf(202,plain,
% 1.80/2.09 (~P5(x2021,f2(a1,a6))+~P5(a7,x2021)),
% 1.80/2.09 inference(scs_inference,[],[197,50,37,17])).
% 1.80/2.09 cnf(203,plain,
% 1.80/2.09 (~P5(x2031,f2(a1,a6))+~P8(x2031,f2(a1,a6))),
% 1.80/2.09 inference(scs_inference,[],[202,176])).
% 1.80/2.09 cnf(204,plain,
% 1.80/2.09 (~P8(x2041,a7)+~P5(x2041,f2(a1,a6))),
% 1.80/2.09 inference(scs_inference,[],[50,203,20])).
% 1.80/2.09 cnf(205,plain,
% 1.80/2.09 (E(a8,f2(a1,a6))+~P8(a8,a7)),
% 1.80/2.09 inference(scs_inference,[],[204,76])).
% 1.80/2.09 cnf(206,plain,
% 1.80/2.09 (E(a8,a7)+~P8(a8,a7)),
% 1.80/2.09 inference(scs_inference,[],[24,205,3])).
% 1.80/2.09 cnf(207,plain,
% 1.80/2.09 (~P5(f2(a1,a6),a8)+~P8(a8,a7)),
% 1.80/2.09 inference(scs_inference,[],[199,206,18])).
% 1.80/2.09 cnf(208,plain,
% 1.80/2.09 (~P8(a8,f2(a1,a6))+~P8(a8,a7)),
% 1.80/2.09 inference(scs_inference,[],[207,33])).
% 1.80/2.09 cnf(209,plain,
% 1.80/2.09 (~P8(a8,a7)),
% 1.80/2.09 inference(scs_inference,[],[50,208,20])).
% 1.80/2.09 cnf(216,plain,
% 1.80/2.09 (E(a7,a8)+P8(a7,a8)),
% 1.80/2.09 inference(scs_inference,[],[209,31,183,176,29])).
% 1.80/2.09 cnf(219,plain,
% 1.80/2.09 (P7(a7,a8)+E(a7,a8)),
% 1.80/2.09 inference(scs_inference,[],[216,30])).
% 1.80/2.09 cnf(228,plain,
% 1.80/2.09 (E(a8,a7)+P7(a7,a8)),
% 1.80/2.09 inference(scs_inference,[],[219,2])).
% 1.80/2.09 cnf(229,plain,
% 1.80/2.09 (P7(a7,a8)),
% 1.80/2.09 inference(scs_inference,[],[48,228,15])).
% 1.80/2.09 cnf(231,plain,
% 1.80/2.09 (~P6(a1,a6)),
% 1.80/2.09 inference(scs_inference,[],[22,50,229,15,45])).
% 1.80/2.09 cnf(254,plain,
% 1.80/2.09 (E(f2(a1,a6),a3)+P8(a7,a3)+~P5(a7,a3)),
% 1.80/2.09 inference(scs_inference,[],[24,122,3])).
% 1.80/2.10 cnf(585,plain,
% 1.80/2.10 (E(a3,f2(a1,a6))+P8(a7,a3)+~P5(a7,a3)),
% 1.80/2.10 inference(scs_inference,[],[2,254])).
% 1.80/2.10 cnf(586,plain,
% 1.80/2.10 (P7(f2(a1,a6),a3)+P8(a7,a3)+~P5(a7,a3)),
% 1.80/2.10 inference(scs_inference,[],[48,585,15])).
% 1.80/2.10 cnf(587,plain,
% 1.80/2.10 (P8(a7,a3)+~P5(a7,a3)),
% 1.80/2.10 inference(scs_inference,[],[21,231,586,40])).
% 1.80/2.10 cnf(588,plain,
% 1.80/2.10 (P5(a3,a7)+~P5(a7,a3)),
% 1.80/2.10 inference(scs_inference,[],[587,33])).
% 1.80/2.10 cnf(589,plain,
% 1.80/2.10 (~P5(a7,a3)),
% 1.80/2.10 inference(scs_inference,[],[588,36])).
% 1.80/2.10 cnf(590,plain,
% 1.80/2.10 (~P8(a3,a7)),
% 1.80/2.10 inference(scs_inference,[],[589,33])).
% 1.80/2.10 cnf(599,plain,
% 1.80/2.10 (E(a3,a7)+P8(a7,a3)),
% 1.80/2.10 inference(scs_inference,[],[24,589,33,176,183,29,3,2])).
% 1.80/2.10 cnf(608,plain,
% 1.80/2.10 (P7(a3,a7)+P8(a7,a3)),
% 1.80/2.10 inference(scs_inference,[],[48,599,16])).
% 1.80/2.10 cnf(610,plain,
% 1.80/2.10 (P7(a7,a3)+P7(a3,a7)),
% 1.80/2.10 inference(scs_inference,[],[608,30])).
% 1.80/2.10 cnf(611,plain,
% 1.80/2.10 (P7(f2(a1,a6),a3)+P7(a3,a7)),
% 1.80/2.10 inference(scs_inference,[],[50,610,15])).
% 1.80/2.10 cnf(613,plain,
% 1.80/2.10 (P7(a3,a7)),
% 1.80/2.10 inference(scs_inference,[],[21,231,611,40])).
% 1.80/2.10 cnf(614,plain,
% 1.80/2.10 (E(a3,a7)),
% 1.80/2.10 inference(scs_inference,[],[613,590,34])).
% 1.80/2.10 cnf(642,plain,
% 1.80/2.10 (P7(a7,a3)),
% 1.80/2.10 inference(scs_inference,[],[614,48,15])).
% 1.80/2.10 cnf(644,plain,
% 1.80/2.10 (P4(a7,a3)),
% 1.80/2.10 inference(scs_inference,[],[614,48,49,15,11])).
% 1.80/2.10 cnf(648,plain,
% 1.80/2.10 ($false),
% 1.80/2.10 inference(scs_inference,[],[21,50,642,644,231,15,11,40]),
% 1.80/2.10 ['proof']).
% 1.80/2.10 % SZS output end Proof
% 1.80/2.10 % Total time :1.706693s
%------------------------------------------------------------------------------