%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : LCL069-1 : TPTP v9.3.1. Bugfixed v1.2.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% Computer : n005.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 : Mon Sep 7 11:18:35 AM UTC 2026
% Result : Unsatisfiable 182.77s 182.84s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LCL069-1 : TPTP v9.3.1. Bugfixed v1.2.0.
% 0.00/0.02 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.08/0.33 % Computer : n005.cluster.edu
% 0.08/0.33 % Model : x86_64 x86_64
% 0.08/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.33 % Memory : 8046.5625MB
% 0.08/0.33 % OS : Linux 6.8.0-71-generic
% 0.08/0.33 % CPULimit : 300
% 0.08/0.33 % WCLimit : 300
% 0.08/0.33 % DateTime : Sat Sep 5 03:54:50 UTC 2026
% 0.08/0.34 % CPUTime :
% 0.24/0.50 start to proof:theBenchmark
% 182.77/182.83 %-------------------------------------------
% 182.77/182.83 % File :CSE---1.7
% 182.77/182.83 % Problem :theBenchmark
% 182.77/182.83 % Transform :cnf
% 182.77/182.83 % Format :tptp:raw
% 182.77/182.84 % Command :java -jar mcs_scs.jar %d %s
% 182.77/182.84
% 182.77/182.84 % Result :Theorem 182.332841s
% 182.77/182.84 % Output :CNFRefutation 182.332841s
% 182.77/182.84 %-------------------------------------------
% 182.77/182.84 %--------------------------------------------------------------------------
% 182.77/182.84 % File : LCL069-1 : TPTP v9.3.1. Bugfixed v1.2.0.
% 182.77/182.84 % Domain : Logic Calculi (Implication/Negation 2 valued sentential)
% 182.77/182.84 % Problem : CN-3 depends on the second Lukasiewicz system
% 182.77/182.84 % Version : [McC92] axioms.
% 182.77/182.84 % English : Axiomatisations of the Implication/Negation 2 valued
% 182.77/182.84 % sentential calculus are {CN-1,CN-2,CN-3} by Lukasiewicz,
% 182.77/182.84 % {CN-18,CN-21,CN-35,CN-39,CN-39,CN-40,CN-46} by Frege,
% 182.77/182.84 % {CN-3,CN-18,CN-21,CN-22,CN-30,CN-54} by Hilbert, {CN-18,
% 182.77/182.84 % CN-35,CN-49} by Church, {CN-19,CN-37,CN-59} by Lukasiewicz,
% 182.77/182.84 % {CN-19,CN-37,CN-60} by Wos, and the single Meredith axiom.
% 182.77/182.84 % Show that CN-3 depends on the second Lukasiewicz system.
% 182.77/182.84
% 182.77/182.84 % Refs : [MW92] McCune & Wos (1992), Experiments in Automated Deductio
% 182.77/182.84 % : [McC92] McCune (1992), Email to G. Sutcliffe
% 182.77/182.84 % Source : [McC92]
% 182.77/182.84 % Names : CN-30 [MW92]
% 182.77/182.84
% 182.77/182.84 % Status : Unsatisfiable
% 182.77/182.84 % Rating : 0.00 v5.4.0, 0.06 v5.3.0, 0.15 v5.2.0, 0.08 v5.1.0, 0.06 v5.0.0, 0.07 v4.0.1, 0.00 v2.7.0, 0.12 v2.6.0, 0.00 v2.0.0
% 182.77/182.84 % Syntax : Number of clauses : 5 ( 4 unt; 0 nHn; 2 RR)
% 182.77/182.84 % Number of literals : 7 ( 0 equ; 3 neg)
% 182.77/182.84 % Maximal clause size : 3 ( 1 avg)
% 182.77/182.84 % Maximal term depth : 5 ( 2 avg)
% 182.77/182.84 % Number of predicates : 1 ( 1 usr; 0 prp; 1-1 aty)
% 182.77/182.84 % Number of functors : 4 ( 4 usr; 2 con; 0-2 aty)
% 182.77/182.84 % Number of variables : 11 ( 2 sgn)
% 182.77/182.84 % SPC : CNF_UNS_RFO_NEQ_HRN
% 182.77/182.84
% 182.77/182.84 % Comments :
% 182.77/182.84 % Bugfixes : v1.2.0 - Clause prove_cn_3 fixed.
% 182.77/182.84 %--------------------------------------------------------------------------
% 182.77/182.84 cnf(condensed_detachment,axiom,
% 182.77/182.84 ( ~ is_a_theorem(implies(X,Y))
% 182.77/182.84 | ~ is_a_theorem(X)
% 182.77/182.84 | is_a_theorem(Y) ) ).
% 182.77/182.84
% 182.77/182.84 cnf(cn_19,axiom,
% 182.77/182.84 is_a_theorem(implies(implies(implies(X,Y),Z),implies(Y,Z))) ).
% 182.77/182.84
% 182.77/182.84 cnf(cn_37,axiom,
% 182.77/182.84 is_a_theorem(implies(implies(implies(X,Y),Z),implies(not(X),Z))) ).
% 182.77/182.84
% 182.77/182.84 cnf(cn_59,axiom,
% 182.77/182.84 is_a_theorem(implies(implies(not(X),Z),implies(implies(Y,Z),implies(implies(X,Y),Z)))) ).
% 182.77/182.84
% 182.77/182.84 cnf(prove_cn_3,negated_conjecture,
% 182.77/182.84 ~ is_a_theorem(implies(a,implies(not(a),b))) ).
% 182.77/182.84
% 182.77/182.84 %--------------------------------------------------------------------------
% 182.77/182.84 %-------------------------------------------
% 182.77/182.84 % Proof found
% 182.77/182.84 % SZS status Theorem for theBenchmark
% 182.77/182.84 % SZS output start Proof
% 182.77/182.84 %ClaNum:5(EqnAxiom:0)
% 182.77/182.84 %VarNum:21(SingletonVarNum:11)
% 182.77/182.84 %MaxLitNum:3
% 182.77/182.84 %MaxfuncDepth:4
% 182.77/182.84 %SharedTerms:6
% 182.77/182.84 %goalClause: 4
% 182.77/182.84 %singleGoalClaCount:1
% 182.77/182.84 [4]~P1(f1(a2,f1(f4(a2),a3)))
% 182.77/182.84 [1]P1(f1(f1(f1(x11,x12),x13),f1(x12,x13)))
% 182.77/182.84 [2]P1(f1(f1(f1(x21,x22),x23),f1(f4(x21),x23)))
% 182.77/182.84 [3]P1(f1(f1(f4(x31),x32),f1(f1(x33,x32),f1(f1(x31,x33),x32))))
% 182.77/182.84 [5]P1(x51)+~P1(x52)+~P1(f1(x52,x51))
% 182.77/182.84 %EqnAxiom
% 182.77/182.84
% 182.77/182.84 %-------------------------------------------
% 182.77/182.85 cnf(6,plain,
% 182.77/182.85 (~P1(f1(f1(x61,a2),f1(f4(a2),a3)))),
% 182.77/182.85 inference(scs_inference,[],[4,1,5])).
% 182.77/182.85 cnf(9,plain,
% 182.77/182.85 (P1(f1(f4(f4(x91)),f1(f1(x92,x93),f1(f1(x91,x92),x93))))),
% 182.77/182.85 inference(scs_inference,[],[2,3,5])).
% 182.77/182.85 cnf(12,plain,
% 182.77/182.85 (P1(f1(f4(f1(x121,x122)),f1(x122,x123)))),
% 182.77/182.85 inference(scs_inference,[],[1,2,5])).
% 182.77/182.85 cnf(18,plain,
% 182.77/182.85 (P1(f1(f1(x181,x182),f1(f1(x183,x181),x182)))+~P1(f4(f4(x183)))),
% 182.77/182.85 inference(scs_inference,[],[9,5])).
% 182.77/182.85 cnf(20,plain,
% 182.77/182.85 (P1(f1(f1(x201,f1(x202,x203)),f1(f1(f1(x204,x202),x201),f1(x202,x203))))),
% 182.77/182.85 inference(scs_inference,[],[12,3,5])).
% 182.77/182.85 cnf(23,plain,
% 182.77/182.85 (P1(f1(f4(x231),f1(f1(f1(x232,x233),x231),f1(x233,x234))))),
% 182.77/182.85 inference(scs_inference,[],[20,2,5])).
% 182.77/182.85 cnf(26,plain,
% 182.77/182.85 (~P1(f4(a2))),
% 182.77/182.85 inference(scs_inference,[],[23,6,5])).
% 182.77/182.85 cnf(42,plain,
% 182.77/182.85 (P1(f1(f1(x421,f1(f1(f1(x422,x423),x424),f1(x423,x425))),f1(f1(x424,x421),f1(f1(f1(x422,x423),x424),f1(x423,x425)))))),
% 182.77/182.85 inference(scs_inference,[],[23,3,5])).
% 182.77/182.85 cnf(80,plain,
% 182.77/182.85 (P1(f1(f4(x801),f1(f1(x802,x801),f1(f1(f1(x803,x804),x802),f1(x804,x805)))))),
% 182.77/182.85 inference(scs_inference,[],[42,2,5])).
% 182.77/182.85 cnf(83,plain,
% 182.77/182.85 (P1(f1(f1(x831,x832),f1(f1(f1(x833,x834),x831),f1(x834,x835))))+~P1(f4(x832))),
% 182.77/182.85 inference(scs_inference,[],[80,5])).
% 182.77/182.85 cnf(152,plain,
% 182.77/182.85 (~P1(f1(f1(f1(f1(x1521,x1522),x1523),f1(x1522,x1523)),f4(a2)))),
% 182.77/182.85 inference(scs_inference,[],[1,26,5])).
% 182.77/182.85 cnf(280,plain,
% 182.77/182.85 (~P1(f1(f1(f4(x2801),f1(f1(f1(x2802,x2803),x2801),f1(x2803,x2804))),f1(a2,f1(f4(a2),a3))))),
% 182.77/182.85 inference(scs_inference,[],[4,23,5])).
% 182.77/182.85 cnf(350,plain,
% 182.77/182.85 (P1(f1(f1(f1(x3501,f4(x3502)),f1(f1(x3502,x3503),x3504)),f1(f4(x3502),x3504)))),
% 182.77/182.85 inference(scs_inference,[],[20,2,5])).
% 182.77/182.85 cnf(354,plain,
% 182.77/182.85 (P1(f1(f4(x3541),f1(f1(x3542,x3541),f4(x3541))))),
% 182.77/182.85 inference(scs_inference,[],[350,3,5])).
% 182.77/182.85 cnf(360,plain,
% 182.77/182.85 (P1(f1(f1(x3601,f1(f1(x3602,x3603),f4(x3603))),f1(f1(x3603,x3601),f1(f1(x3602,x3603),f4(x3603)))))),
% 182.77/182.85 inference(scs_inference,[],[354,3,5])).
% 182.77/182.85 cnf(368,plain,
% 182.77/182.85 (P1(f1(f1(f1(x3681,f4(x3682)),f1(f1(x3683,f4(x3682)),f1(f1(x3682,x3684),x3685))),f1(f4(x3682),x3685)))),
% 182.77/182.85 inference(scs_inference,[],[350,20,5])).
% 182.77/182.85 cnf(372,plain,
% 182.77/182.85 (P1(f1(f4(x3721),f4(x3721)))),
% 182.77/182.85 inference(scs_inference,[],[368,3,5])).
% 182.77/182.85 cnf(378,plain,
% 182.77/182.85 (P1(f1(f1(x3781,f4(x3782)),f1(f1(x3782,x3781),f4(x3782))))),
% 182.77/182.85 inference(scs_inference,[],[372,3,5])).
% 182.77/182.85 cnf(386,plain,
% 182.77/182.85 (P1(f1(f1(x3861,f1(x3861,f4(x3861))),f1(f1(x3861,x3861),f4(x3861))))),
% 182.77/182.85 inference(scs_inference,[],[360,378,5])).
% 182.77/182.85 cnf(406,plain,
% 182.77/182.85 (P1(f1(f1(x4061,f4(x4061)),f4(x4061)))),
% 182.77/182.85 inference(scs_inference,[],[372,378,5])).
% 182.77/182.85 cnf(416,plain,
% 182.77/182.85 (P1(f1(f1(x4161,f1(x4161,f4(x4161))),f4(x4161)))),
% 182.77/182.85 inference(scs_inference,[],[406,378,5])).
% 182.77/182.85 cnf(426,plain,
% 182.77/182.85 (P1(f1(f1(x4261,f1(x4261,f1(x4261,f4(x4261)))),f4(x4261)))),
% 182.77/182.85 inference(scs_inference,[],[416,378,5])).
% 182.77/182.85 cnf(436,plain,
% 182.77/182.85 (P1(f1(f1(x4361,f1(x4361,f1(x4361,f1(x4361,f4(x4361))))),f4(x4361)))),
% 182.77/182.85 inference(scs_inference,[],[426,378,5])).
% 182.77/182.85 cnf(444,plain,
% 182.77/182.85 (P1(f1(f1(x4441,f4(x4441)),f1(f1(x4442,x4441),f4(x4441))))),
% 182.77/182.85 inference(scs_inference,[],[354,360,5])).
% 182.77/182.85 cnf(503,plain,
% 182.77/182.85 (~P1(f1(f1(f1(x5031,f1(x5031,f4(x5031))),f1(f1(x5031,x5031),f4(x5031))),f1(f1(f1(f1(x5032,x5033),x5034),f1(x5033,x5034)),f4(a2))))),
% 182.77/182.85 inference(scs_inference,[],[386,152,5])).
% 182.77/182.85 cnf(588,plain,
% 182.77/182.85 (P1(f1(f4(x5881),f1(f1(x5882,x5881),f4(x5882))))),
% 182.77/182.85 inference(scs_inference,[],[2,378,5])).
% 182.77/182.85 cnf(608,plain,
% 182.77/182.85 (P1(f1(f1(f1(x6081,f1(x6082,x6083)),f4(f4(x6084))),f1(f1(x6082,x6083),f1(f1(x6084,x6082),x6083))))),
% 182.77/182.85 inference(scs_inference,[],[9,20,5])).
% 182.77/182.85 cnf(745,plain,
% 182.77/182.85 (P1(f1(f1(x7451,f1(x7451,f4(x7451))),f1(f1(x7452,x7451),f4(x7451))))),
% 182.77/182.85 inference(scs_inference,[],[360,444,5])).
% 182.77/182.85 cnf(755,plain,
% 182.77/182.85 (P1(f1(f1(x7551,f1(x7551,f1(x7551,f4(x7551)))),f1(f1(x7552,x7551),f4(x7551))))),
% 182.77/182.85 inference(scs_inference,[],[745,360,5])).
% 182.77/182.85 cnf(777,plain,
% 182.77/182.85 (P1(f1(f4(x7771),f1(f1(x7771,x7772),f4(x7771))))),
% 182.77/182.85 inference(scs_inference,[],[378,1,5])).
% 182.77/182.85 cnf(786,plain,
% 182.77/182.85 (P1(f1(f1(x7861,f1(f1(x7862,x7863),f4(x7862))),f1(f1(x7862,x7861),f1(f1(x7862,x7863),f4(x7862)))))),
% 182.77/182.85 inference(scs_inference,[],[777,3,5])).
% 182.77/182.85 cnf(857,plain,
% 182.77/182.85 (P1(f1(f1(x8571,f4(x8572)),f1(f1(x8571,x8572),f4(x8571))))),
% 182.77/182.85 inference(scs_inference,[],[588,786,5])).
% 182.77/182.85 cnf(865,plain,
% 182.77/182.85 (P1(f1(f1(f1(x8651,f4(x8651)),x8651),f4(f1(x8651,f4(x8651)))))),
% 182.77/182.85 inference(scs_inference,[],[857,406,5])).
% 182.77/182.85 cnf(874,plain,
% 182.77/182.85 (P1(f1(f1(f4(x8741),x8741),f4(f4(x8741))))),
% 182.77/182.85 inference(scs_inference,[],[857,372,5])).
% 182.77/182.85 cnf(881,plain,
% 182.77/182.85 (P1(f1(f1(x8811,x8812),f1(f1(f1(x8811,x8812),x8811),x8812)))),
% 182.77/182.85 inference(scs_inference,[],[874,608,5])).
% 182.77/182.85 cnf(890,plain,
% 182.77/182.85 (P1(f1(f1(f1(f1(f4(x8901),x8901),f4(f4(x8901))),f1(f4(x8901),x8901)),f4(f4(x8901))))),
% 182.77/182.85 inference(scs_inference,[],[881,874,5])).
% 182.77/182.85 cnf(897,plain,
% 182.77/182.85 (P1(f1(f1(f4(x8971),x8971),f1(f1(x8971,f4(x8971)),x8971)))),
% 182.77/182.85 inference(scs_inference,[],[890,608,5])).
% 182.77/182.85 cnf(906,plain,
% 182.77/182.85 (P1(f1(f1(f1(x9061,x9061),f4(f1(x9061,x9061))),f1(x9061,x9061)))),
% 182.77/182.85 inference(scs_inference,[],[897,12,5])).
% 182.77/182.85 cnf(918,plain,
% 182.77/182.85 (P1(f1(f1(x9181,f1(f1(x9182,x9182),f4(f1(x9182,x9182)))),f1(f1(f1(x9183,x9184),x9181),f1(x9184,x9185))))),
% 182.77/182.85 inference(scs_inference,[],[906,865,5,83])).
% 182.77/182.85 cnf(953,plain,
% 182.77/182.85 (P1(f1(f1(f1(f4(x9531),x9531),f4(x9531)),f4(f1(f4(x9531),x9531))))),
% 182.77/182.85 inference(scs_inference,[],[874,857,5])).
% 182.77/182.85 cnf(960,plain,
% 182.77/182.85 (P1(f1(f1(f1(x9601,x9602),f4(f1(x9603,f1(x9604,x9604)))),f1(x9602,x9605)))),
% 182.77/182.85 inference(scs_inference,[],[918,12,5])).
% 182.77/182.85 cnf(966,plain,
% 182.77/182.86 (P1(f1(f4(f1(x9661,x9661)),x9662))),
% 182.77/182.86 inference(scs_inference,[],[953,960,5])).
% 182.77/182.86 cnf(970,plain,
% 182.77/182.86 (~P1(f4(f1(x9701,x9701)))),
% 182.77/182.86 inference(scs_inference,[],[503,966,5])).
% 182.77/182.86 cnf(976,plain,
% 182.77/182.86 (~P1(f1(f1(x9761,x9761),f4(f1(x9761,x9761))))),
% 182.77/182.86 inference(scs_inference,[],[970,406,5])).
% 182.77/182.86 cnf(986,plain,
% 182.77/182.86 (P1(f1(f1(x9861,f4(f1(x9862,x9862))),f4(f4(f1(x9862,x9862)))))),
% 182.77/182.86 inference(scs_inference,[],[966,755,5])).
% 182.77/182.86 cnf(992,plain,
% 182.77/182.86 (P1(f4(f1(f4(f4(f1(x9921,x9921))),f4(f1(x9921,x9921)))))),
% 182.77/182.86 inference(scs_inference,[],[953,986,5])).
% 182.77/182.86 cnf(996,plain,
% 182.77/182.86 (P1(f4(f4(f1(x9961,x9961))))),
% 182.77/182.86 inference(scs_inference,[],[436,986,5])).
% 182.77/182.86 cnf(1002,plain,
% 182.77/182.86 (P1(f1(f1(x10021,f4(f1(x10022,x10022))),f1(f1(f1(x10023,x10024),x10021),f1(x10024,x10025))))),
% 182.77/182.86 inference(scs_inference,[],[976,996,5,83])).
% 182.77/182.86 cnf(1004,plain,
% 182.77/182.86 (P1(f1(f1(x10041,x10042),f1(f1(f1(x10043,x10043),x10041),x10042)))),
% 182.77/182.86 inference(scs_inference,[],[976,996,5,83,18])).
% 182.77/182.86 cnf(1006,plain,
% 182.77/182.86 (P1(f1(f1(f1(x10061,x10061),f1(x10062,f4(f1(x10063,x10063)))),f1(f1(f1(x10064,x10065),x10062),f1(x10065,x10066))))),
% 182.77/182.86 inference(scs_inference,[],[1004,1002,5])).
% 182.77/182.86 cnf(1115,plain,
% 182.77/182.86 (P1(f1(f1(f1(x11151,x11152),f1(f1(x11153,x11153),f4(f1(x11153,x11153)))),f1(x11152,x11154)))),
% 182.77/182.86 inference(scs_inference,[],[1006,378,5])).
% 182.77/182.86 cnf(1126,plain,
% 182.77/182.86 (P1(f1(f4(f1(x11261,f1(x11262,x11262))),x11263))),
% 182.77/182.86 inference(scs_inference,[],[1115,960,5])).
% 182.77/182.86 cnf(1135,plain,
% 182.77/182.86 (P1(f1(f1(x11351,f1(f4(f4(f1(x11352,x11352))),f4(f1(x11352,x11352)))),f4(x11351)))),
% 182.77/182.86 inference(scs_inference,[],[588,992,5])).
% 182.77/182.86 cnf(1144,plain,
% 182.77/182.86 (P1(f4(f4(f1(x11441,f1(x11442,x11442)))))),
% 182.77/182.86 inference(scs_inference,[],[1135,1126,5])).
% 182.77/182.86 cnf(1150,plain,
% 182.77/182.86 (P1(f1(f1(x11501,x11502),f1(f1(f1(x11503,f1(x11504,x11504)),x11501),x11502)))),
% 182.77/182.86 inference(scs_inference,[],[1144,83,18])).
% 182.77/182.86 cnf(1761,plain,
% 182.77/182.86 (P1(f1(f1(f1(x17611,f1(x17612,x17612)),f1(x17613,x17614)),f1(f1(f1(x17615,x17615),x17613),x17614)))),
% 182.77/182.86 inference(scs_inference,[],[1004,1150,5])).
% 182.77/182.86 cnf(1770,plain,
% 182.77/182.86 (P1(f1(f1(f1(x17701,x17701),f1(f1(x17702,f1(x17703,x17703)),f1(x17704,x17705))),f1(f1(f1(x17706,x17706),x17704),x17705)))),
% 182.77/182.86 inference(scs_inference,[],[1004,1761,5])).
% 182.77/182.86 cnf(1775,plain,
% 182.77/182.86 (P1(f1(f1(f1(x17751,x17751),x17752),x17752))),
% 182.77/182.86 inference(scs_inference,[],[1004,1770,5])).
% 182.77/182.86 cnf(1785,plain,
% 182.77/182.86 (P1(f1(f1(f1(x17851,x17851),f1(f1(x17852,x17852),x17853)),x17853))),
% 182.77/182.86 inference(scs_inference,[],[1004,1775,5])).
% 182.77/182.86 cnf(1804,plain,
% 182.77/182.86 (P1(f1(x18041,x18041))),
% 182.77/182.86 inference(scs_inference,[],[1785,1770,5])).
% 182.77/182.86 cnf(1967,plain,
% 182.77/182.86 (P1(f1(x19671,f1(x19672,x19671)))),
% 182.77/182.86 inference(scs_inference,[],[1,1804,5])).
% 182.77/182.86 cnf(2065,plain,
% 182.77/182.86 (P1(f1(f4(x20651),f1(x20652,f1(x20651,x20653))))),
% 182.77/182.86 inference(scs_inference,[],[2,1967,5])).
% 182.77/182.86 cnf(2172,plain,
% 182.77/182.86 (P1(f1(f1(x21721,f1(x21722,f1(x21723,x21724))),f1(f1(x21723,x21721),f1(x21722,f1(x21723,x21724)))))),
% 182.77/182.86 inference(scs_inference,[],[3,2065,5])).
% 182.77/182.86 cnf(2839,plain,
% 182.77/182.86 ($false),
% 182.77/182.86 inference(scs_inference,[],[1,280,2172,5]),
% 182.77/182.86 ['proof']).
% 182.77/182.86 % SZS output end Proof
% 182.77/182.86 % Total time :182.332841s
%------------------------------------------------------------------------------