%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SYN072+1 : TPTP v8.2.0. Released v2.0.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % Computer : n019.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 19:04:28 EDT 2024 % Result : Theorem 0.52s 0.95s % Output : CNFRefutation 0.52s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : SYN072+1 : TPTP v8.2.0. Released v2.0.0. % 0.03/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.12/0.33 % Computer : n019.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 : Sun Jun 23 22:06:54 EDT 2024 % 0.12/0.33 % CPUTime : % 0.42/0.61 start to proof:theBenchmark % 0.52/0.94 %------------------------------------------- % 0.52/0.94 % File :CSE---1.7 % 0.52/0.94 % Problem :theBenchmark % 0.52/0.94 % Transform :cnf % 0.52/0.94 % Format :tptp:raw % 0.52/0.94 % Command :java -jar mcs_scs.jar %d %s % 0.52/0.94 % 0.52/0.94 % Result :Theorem 0.300000s % 0.52/0.94 % Output :CNFRefutation 0.300000s % 0.52/0.94 %------------------------------------------- % 0.52/0.94 %-------------------------------------------------------------------------- % 0.52/0.94 % File : SYN072+1 : TPTP v8.2.0. Released v2.0.0. % 0.52/0.94 % Domain : Syntactic % 0.52/0.94 % Problem : Pelletier Problem 49 % 0.52/0.94 % Version : Especial. % 0.52/0.94 % English : % 0.52/0.94 % 0.52/0.94 % Refs : [Pel86] Pelletier (1986), Seventy-five Problems for Testing Au % 0.52/0.94 % : [Hah94] Haehnle (1994), Email to G. Sutcliffe % 0.52/0.94 % Source : [Hah94] % 0.52/0.94 % Names : Pelletier 49 [Pel86] % 0.52/0.94 % 0.52/0.94 % Status : Theorem % 0.52/0.94 % Rating : 0.00 v5.3.0, 0.18 v5.2.0, 0.25 v5.0.0, 0.00 v4.1.0, 0.13 v4.0.1, 0.09 v4.0.0, 0.08 v3.7.0, 0.00 v3.2.0, 0.11 v3.1.0, 0.17 v2.7.0, 0.00 v2.4.0, 0.00 v2.3.0, 0.33 v2.2.1, 0.00 v2.1.0 % 0.52/0.94 % Syntax : Number of formulae : 5 ( 4 unt; 0 def) % 0.52/0.94 % Number of atoms : 6 ( 3 equ) % 0.52/0.94 % Maximal formula atoms : 2 ( 1 avg) % 0.52/0.94 % Number of connectives : 2 ( 1 ~; 1 |; 0 &) % 0.52/0.94 % ( 0 <=>; 0 =>; 0 <=; 0 <~>) % 0.52/0.94 % Maximal formula depth : 5 ( 2 avg) % 0.52/0.94 % Maximal term depth : 1 ( 1 avg) % 0.52/0.94 % Number of predicates : 2 ( 1 usr; 0 prp; 1-2 aty) % 0.52/0.94 % Number of functors : 2 ( 2 usr; 2 con; 0-0 aty) % 0.52/0.94 % Number of variables : 4 ( 2 !; 2 ?) % 0.52/0.94 % SPC : FOF_THM_EPR_SEQ % 0.52/0.94 % 0.52/0.95 % Comments : % 0.52/0.95 %-------------------------------------------------------------------------- % 0.52/0.95 %----Problem axioms % 0.52/0.95 fof(pel49_1,axiom, % 0.52/0.95 ? [X,Y] : % 0.52/0.95 ! [Z] : % 0.52/0.95 ( Z = X % 0.52/0.95 | Z = Y ) ). % 0.52/0.95 % 0.52/0.95 fof(pel49_2,axiom, % 0.52/0.95 big_p(a) ). % 0.52/0.95 % 0.52/0.95 fof(pel49_3,axiom, % 0.52/0.95 big_p(b) ). % 0.52/0.95 % 0.52/0.95 fof(pel49_4,axiom, % 0.52/0.95 a != b ). % 0.52/0.95 % 0.52/0.95 fof(pel49,conjecture, % 0.52/0.95 ! [X] : big_p(X) ). % 0.52/0.95 % 0.52/0.95 %-------------------------------------------------------------------------- % 0.52/0.95 %------------------------------------------- % 0.52/0.95 % Proof found % 0.52/0.95 % SZS status Theorem for theBenchmark % 0.52/0.95 % SZS output start Proof % 0.52/0.95 %ClaNum:9(EqnAxiom:4) % 0.52/0.95 %VarNum:2(SingletonVarNum:1) % 0.52/0.95 %MaxLitNum:2 % 0.52/0.95 %MaxfuncDepth:0 % 0.52/0.95 %SharedTerms:9 % 0.52/0.95 %goalClause: 8 % 0.52/0.95 %singleGoalClaCount:1 % 0.52/0.95 [5]P1(a1) % 0.52/0.95 [6]P1(a2) % 0.52/0.95 [7]~E(a1,a2) % 0.52/0.95 [8]~P1(a3) % 0.52/0.95 [9]E(x91,a5)+E(x91,a4) % 0.52/0.95 %EqnAxiom % 0.52/0.95 [1]E(x11,x11) % 0.52/0.95 [2]E(x22,x21)+~E(x21,x22) % 0.52/0.95 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 0.52/0.95 [4]~P1(x41)+P1(x42)+~E(x41,x42) % 0.52/0.95 % 0.52/0.95 %------------------------------------------- % 0.52/0.95 cnf(10,plain, % 0.52/0.95 (E(a5,x101)+E(x101,a4)), % 0.52/0.95 inference(scs_inference,[],[2,9])). % 0.52/0.95 cnf(11,plain, % 0.52/0.95 (E(a4,x111)+E(a5,x111)), % 0.52/0.95 inference(scs_inference,[],[10,2])). % 0.52/0.95 cnf(12,plain, % 0.52/0.95 (E(x121,a5)+E(a4,x121)), % 0.52/0.95 inference(scs_inference,[],[11,2])). % 0.52/0.95 cnf(13,plain, % 0.52/0.95 (~E(a1,a4)+E(a2,a5)), % 0.52/0.95 inference(scs_inference,[],[7,12,3])). % 0.52/0.95 cnf(14,plain, % 0.52/0.95 (E(a1,a5)+E(a2,a5)), % 0.52/0.95 inference(scs_inference,[],[13,9])). % 0.52/0.95 cnf(18,plain, % 0.52/0.95 (~E(a3,a1)), % 0.52/0.95 inference(scs_inference,[],[5,8,4,2])). % 0.52/0.95 cnf(19,plain, % 0.52/0.95 (~E(x191,a3)+~E(x191,a1)), % 0.52/0.95 inference(scs_inference,[],[18,2,3])). % 0.52/0.95 cnf(20,plain, % 0.52/0.95 (E(a1,a4)+~E(a5,a3)), % 0.52/0.95 inference(scs_inference,[],[19,10])). % 0.52/0.95 cnf(21,plain, % 0.52/0.95 (~E(a5,a3)+E(a2,a5)), % 0.52/0.95 inference(scs_inference,[],[20,13])). % 0.52/0.95 cnf(22,plain, % 0.52/0.95 (E(a4,a3)+E(a2,a5)), % 0.52/0.95 inference(scs_inference,[],[21,11])). % 0.52/0.95 cnf(27,plain, % 0.52/0.95 (E(a5,a2)+E(a1,a5)), % 0.52/0.95 inference(scs_inference,[],[2,14])). % 0.52/0.95 cnf(28,plain, % 0.52/0.95 (E(a5,a1)+E(a5,a2)), % 0.52/0.95 inference(scs_inference,[],[27,2])). % 0.52/0.95 cnf(29,plain, % 0.52/0.95 (~E(a5,a3)+E(a5,a2)), % 0.52/0.95 inference(scs_inference,[],[28,19])). % 0.52/0.95 cnf(30,plain, % 0.52/0.95 (E(a3,a4)+E(a5,a2)), % 0.52/0.95 inference(scs_inference,[],[29,10])). % 0.52/0.95 cnf(31,plain, % 0.52/0.95 (E(a4,a3)+E(a5,a2)), % 0.52/0.95 inference(scs_inference,[],[30,2])). % 0.52/0.95 cnf(32,plain, % 0.52/0.95 (~E(a4,a1)+E(a5,a2)), % 0.52/0.95 inference(scs_inference,[],[31,19])). % 0.52/0.95 cnf(33,plain, % 0.52/0.95 (~E(a1,a4)+E(a5,a2)), % 0.52/0.95 inference(scs_inference,[],[32,2])). % 0.52/0.95 cnf(34,plain, % 0.52/0.95 (~E(x341,a4)+~E(a1,x341)+E(a5,a2)), % 0.52/0.95 inference(scs_inference,[],[33,3])). % 0.52/0.95 cnf(35,plain, % 0.52/0.95 (~E(a5,a4)+E(a5,a2)), % 0.52/0.95 inference(scs_inference,[],[34,27])). % 0.52/0.95 cnf(36,plain, % 0.52/0.95 (~E(a4,a5)+E(a5,a2)), % 0.52/0.95 inference(scs_inference,[],[35,2])). % 0.52/0.95 cnf(37,plain, % 0.52/0.95 (~E(x371,a5)+~E(a4,x371)+E(a5,a2)), % 0.52/0.95 inference(scs_inference,[],[36,3])). % 0.52/0.95 cnf(38,plain, % 0.52/0.95 (~E(a3,a5)+E(a5,a2)+E(a2,a5)), % 0.52/0.95 inference(scs_inference,[],[37,22])). % 0.52/0.95 cnf(39,plain, % 0.52/0.95 (~E(a1,a5)+~E(a3,a5)+E(a2,a5)), % 0.52/0.95 inference(scs_inference,[],[7,38,3])). % 0.52/0.95 cnf(40,plain, % 0.52/0.95 (E(a1,a4)+~E(a3,a5)+E(a2,a5)), % 0.52/0.95 inference(scs_inference,[],[39,9])). % 0.52/0.95 cnf(41,plain, % 0.52/0.95 (~E(a4,a2)+~E(a3,a5)+E(a2,a5)), % 0.52/0.95 inference(scs_inference,[],[7,40,3])). % 0.52/0.95 cnf(42,plain, % 0.52/0.95 (E(a2,a5)+~E(a3,a5)), % 0.52/0.95 inference(scs_inference,[],[41,12])). % 0.52/0.95 cnf(43,plain, % 0.52/0.95 (E(a5,a2)+~E(a3,a5)), % 0.52/0.95 inference(scs_inference,[],[42,2])). % 0.52/0.95 cnf(44,plain, % 0.52/0.95 (~E(a1,a5)+~E(a3,a5)), % 0.52/0.95 inference(scs_inference,[],[7,43,3])). % 0.52/0.95 cnf(45,plain, % 0.52/0.95 (E(a1,a4)+~E(a3,a5)), % 0.52/0.95 inference(scs_inference,[],[44,9])). % 0.52/0.95 cnf(46,plain, % 0.52/0.95 (E(a4,a1)+~E(a3,a5)), % 0.52/0.95 inference(scs_inference,[],[45,2])). % 0.52/0.95 cnf(47,plain, % 0.52/0.95 (~E(a4,a3)+~E(a3,a5)), % 0.52/0.95 inference(scs_inference,[],[46,19])). % 0.52/0.95 cnf(51,plain, % 0.52/0.96 (E(a4,a1)+~E(a5,a3)), % 0.52/0.96 inference(scs_inference,[],[2,20])). % 0.52/0.96 cnf(52,plain, % 0.52/0.96 (E(a4,a1)+E(a3,a4)), % 0.52/0.96 inference(scs_inference,[],[51,10])). % 0.52/0.96 cnf(55,plain, % 0.52/0.96 (~E(a3,a2)), % 0.52/0.96 inference(scs_inference,[],[6,8,2,4])). % 0.52/0.96 cnf(56,plain, % 0.52/0.96 (E(a3,a4)+E(a2,a5)), % 0.52/0.96 inference(scs_inference,[],[2,22])). % 0.52/0.96 cnf(57,plain, % 0.52/0.96 (E(a5,a2)+E(a2,a5)+~E(a1,a3)), % 0.52/0.96 inference(scs_inference,[],[56,34])). % 0.52/0.96 cnf(58,plain, % 0.52/0.96 (E(a2,a5)+~E(a1,a3)), % 0.52/0.96 inference(scs_inference,[],[57,2])). % 0.52/0.96 cnf(59,plain, % 0.52/0.96 (P1(a5)+~E(a1,a3)), % 0.52/0.96 inference(scs_inference,[],[6,58,4])). % 0.52/0.96 cnf(60,plain, % 0.52/0.96 (~E(x601,a3)+~E(a1,x601)+P1(a5)), % 0.52/0.96 inference(scs_inference,[],[59,3])). % 0.52/0.96 cnf(61,plain, % 0.52/0.96 (~E(a4,a3)+E(a1,a5)+P1(a5)), % 0.52/0.96 inference(scs_inference,[],[60,9])). % 0.52/0.96 cnf(62,plain, % 0.52/0.96 (~E(a5,a2)+~E(a4,a3)+P1(a5)), % 0.52/0.96 inference(scs_inference,[],[7,61,3])). % 0.52/0.96 cnf(63,plain, % 0.52/0.96 (E(a5,a3)+~E(a5,a2)+P1(a5)), % 0.52/0.96 inference(scs_inference,[],[62,11])). % 0.52/0.96 cnf(69,plain, % 0.52/0.96 (E(a2,a5)+~E(a5,a4)), % 0.52/0.96 inference(scs_inference,[],[2,35])). % 0.52/0.96 cnf(70,plain, % 0.52/0.96 (P1(a5)+~E(a5,a4)), % 0.52/0.96 inference(scs_inference,[],[6,69,4])). % 0.52/0.96 cnf(74,plain, % 0.52/0.96 (~E(x741,a4)+~E(a5,x741)+P1(a5)), % 0.52/0.96 inference(scs_inference,[],[70,3])). % 0.52/0.96 cnf(75,plain, % 0.52/0.96 (~E(a3,a4)+~E(a5,a2)+P1(a5)), % 0.52/0.96 inference(scs_inference,[],[74,63])). % 0.52/0.96 cnf(76,plain, % 0.52/0.96 (E(a3,a5)+~E(a5,a2)+P1(a5)), % 0.52/0.96 inference(scs_inference,[],[75,9])). % 0.52/0.96 cnf(84,plain, % 0.52/0.96 (~E(a4,x841)+~E(a5,x841)+P1(a5)), % 0.52/0.96 inference(scs_inference,[],[2,74])). % 0.52/0.96 cnf(85,plain, % 0.52/0.96 (~E(a5,a3)+~E(a5,x851)+~E(a4,x851)), % 0.52/0.96 inference(scs_inference,[],[8,84,4])). % 0.52/0.96 cnf(87,plain, % 0.52/0.96 (E(a2,a5)+~E(a4,a5)), % 0.52/0.96 inference(scs_inference,[],[2,36])). % 0.52/0.96 cnf(88,plain, % 0.52/0.96 (~E(x881,a5)+~E(a4,x881)+E(a2,a5)), % 0.52/0.96 inference(scs_inference,[],[87,3])). % 0.52/0.96 cnf(89,plain, % 0.52/0.96 (~E(x891,a4)+E(a2,a5)+~E(x891,a5)), % 0.52/0.96 inference(scs_inference,[],[88,2])). % 0.52/0.96 cnf(90,plain, % 0.52/0.96 (E(a5,a2)+~E(x901,a5)+~E(x901,a4)), % 0.52/0.96 inference(scs_inference,[],[89,2])). % 0.52/0.96 cnf(91,plain, % 0.52/0.96 (~E(a3,a5)+~E(x911,a4)+~E(x911,a5)), % 0.52/0.96 inference(scs_inference,[],[55,90,3])). % 0.52/0.96 cnf(93,plain, % 0.52/0.96 (~E(a5,a3)+~E(a3,a4)), % 0.52/0.96 inference(scs_inference,[],[2,91])). % 0.52/0.96 cnf(94,plain, % 0.52/0.96 (~E(x941,a3)+~E(a5,x941)+~E(a3,a4)), % 0.52/0.96 inference(scs_inference,[],[93,3])). % 0.52/0.96 cnf(95,plain, % 0.52/0.96 (~E(a5,x951)+~E(x951,a3)+E(a3,a5)), % 0.52/0.96 inference(scs_inference,[],[94,9])). % 0.52/0.96 cnf(96,plain, % 0.52/0.96 (~E(a5,a2)+~E(x961,a3)+~E(a5,x961)), % 0.52/0.96 inference(scs_inference,[],[55,95,3])). % 0.52/0.96 cnf(97,plain, % 0.52/0.96 (E(a2,a4)+~E(a2,a3)), % 0.52/0.96 inference(scs_inference,[],[96,10])). % 0.52/0.96 cnf(98,plain, % 0.52/0.96 (E(a4,a2)+~E(a2,a3)), % 0.52/0.96 inference(scs_inference,[],[97,2])). % 0.52/0.96 cnf(99,plain, % 0.52/0.96 (~E(a3,a4)+~E(a2,a3)), % 0.52/0.96 inference(scs_inference,[],[55,98,3])). % 0.52/0.96 cnf(106,plain, % 0.52/0.96 (E(a1,a4)+E(a3,a4)), % 0.52/0.96 inference(scs_inference,[],[2,52])). % 0.52/0.96 cnf(107,plain, % 0.52/0.96 (E(a1,a4)+~E(a2,a3)), % 0.52/0.96 inference(scs_inference,[],[106,99])). % 0.52/0.96 cnf(108,plain, % 0.52/0.96 (E(a4,a1)+~E(a2,a3)), % 0.52/0.96 inference(scs_inference,[],[107,2])). % 0.52/0.96 cnf(109,plain, % 0.52/0.96 (~E(a4,a3)+~E(a2,a3)), % 0.52/0.96 inference(scs_inference,[],[108,19])). % 0.52/0.96 cnf(110,plain, % 0.52/0.96 (E(a5,a3)+~E(a2,a3)), % 0.52/0.96 inference(scs_inference,[],[109,11])). % 0.52/0.96 cnf(115,plain, % 0.52/0.96 (~E(a2,a5)+~E(a2,a3)), % 0.52/0.96 inference(scs_inference,[],[2,96])). % 0.52/0.96 cnf(116,plain, % 0.52/0.96 (~E(x1161,a3)+~E(a2,x1161)+~E(a2,a5)), % 0.52/0.96 inference(scs_inference,[],[115,3])). % 0.52/0.96 cnf(117,plain, % 0.52/0.96 (~E(a5,a3)+~E(a2,a5)), % 0.52/0.96 inference(scs_inference,[],[116,21])). % 0.52/0.96 cnf(118,plain, % 0.52/0.96 (E(a3,a4)+~E(a2,a5)), % 0.52/0.96 inference(scs_inference,[],[117,10])). % 0.52/0.96 cnf(119,plain, % 0.52/0.96 (E(a4,a3)+~E(a2,a5)), % 0.52/0.96 inference(scs_inference,[],[118,2])). % 0.52/0.96 cnf(120,plain, % 0.52/0.96 (~E(a4,a1)+~E(a2,a5)), % 0.52/0.96 inference(scs_inference,[],[119,19])). % 0.52/0.96 cnf(121,plain, % 0.52/0.96 (E(a5,a1)+~E(a2,a5)), % 0.52/0.96 inference(scs_inference,[],[120,11])). % 0.52/0.96 cnf(122,plain, % 0.52/0.96 (E(a1,a5)+~E(a2,a5)), % 0.52/0.96 inference(scs_inference,[],[121,2])). % 0.52/0.96 cnf(123,plain, % 0.52/0.96 (~E(a3,a5)+~E(a2,a5)), % 0.52/0.96 inference(scs_inference,[],[122,44])). % 0.52/0.96 cnf(124,plain, % 0.52/0.96 (~E(a5,a2)+~E(a2,a5)+P1(a5)), % 0.52/0.96 inference(scs_inference,[],[123,76])). % 0.52/0.96 cnf(125,plain, % 0.52/0.96 (~E(a1,a4)+~E(a2,a5)+P1(a5)), % 0.52/0.96 inference(scs_inference,[],[124,33])). % 0.52/0.96 cnf(126,plain, % 0.52/0.96 (~E(a1,a4)+P1(a5)), % 0.52/0.96 inference(scs_inference,[],[125,13])). % 0.52/0.96 cnf(135,plain, % 0.52/0.96 (~E(a5,a3)+~E(a1,a4)), % 0.52/0.96 inference(scs_inference,[],[8,126,4])). % 0.52/0.96 cnf(136,plain, % 0.52/0.96 (~E(a1,a4)+~E(a2,a3)), % 0.52/0.96 inference(scs_inference,[],[135,110])). % 0.52/0.96 cnf(137,plain, % 0.52/0.96 (~E(a5,a3)+~E(a2,a3)), % 0.52/0.96 inference(scs_inference,[],[136,20])). % 0.52/0.96 cnf(138,plain, % 0.52/0.96 (~E(a2,a3)+E(a4,a3)), % 0.52/0.96 inference(scs_inference,[],[137,11])). % 0.52/0.96 cnf(139,plain, % 0.52/0.96 (~E(a3,a5)+~E(a2,a3)), % 0.52/0.96 inference(scs_inference,[],[138,47])). % 0.52/0.96 cnf(140,plain, % 0.52/0.96 (~E(a2,a3)+E(a3,a4)), % 0.52/0.96 inference(scs_inference,[],[139,9])). % 0.52/0.96 cnf(141,plain, % 0.52/0.96 (~E(a2,a3)), % 0.52/0.96 inference(scs_inference,[],[140,99])). % 0.52/0.96 cnf(142,plain, % 0.52/0.96 (E(a5,a1)+P1(a5)), % 0.52/0.96 inference(scs_inference,[],[126,10])). % 0.52/0.96 cnf(143,plain, % 0.52/0.96 (~E(a5,a3)+E(a5,a1)), % 0.52/0.96 inference(scs_inference,[],[8,142,4])). % 0.52/0.96 cnf(144,plain, % 0.52/0.96 (E(a5,a1)+E(a4,a3)), % 0.52/0.96 inference(scs_inference,[],[143,11])). % 0.52/0.96 cnf(145,plain, % 0.52/0.96 (E(a4,a3)+~E(a5,a3)), % 0.52/0.96 inference(scs_inference,[],[144,19])). % 0.52/0.96 cnf(146,plain, % 0.52/0.96 (~E(a3,a5)+E(a4,a3)), % 0.52/0.96 inference(scs_inference,[],[145,2])). % 0.52/0.96 cnf(147,plain, % 0.52/0.96 (~E(a3,a5)), % 0.52/0.96 inference(scs_inference,[],[146,47])). % 0.52/0.96 cnf(157,plain, % 0.52/0.96 (E(a4,a3)), % 0.52/0.96 inference(scs_inference,[],[147,2,9])). % 0.52/0.96 cnf(165,plain, % 0.52/0.96 (E(a5,a2)), % 0.52/0.96 inference(scs_inference,[],[8,157,141,2,4,85,3,9,10])). % 0.52/0.96 cnf(169,plain, % 0.52/0.96 (E(a1,a5)), % 0.52/0.96 inference(scs_inference,[],[8,157,141,2,4,85,3,9,10,120,121,122])). % 0.52/0.96 cnf(176,plain, % 0.52/0.96 ($false), % 0.52/0.96 inference(scs_inference,[],[7,165,169,3]), % 0.52/0.96 ['proof']). % 0.52/0.96 % SZS output end Proof % 0.52/0.96 % Total time :0.300000s %------------------------------------------------------------------------------