%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : LCL686+1.010 : TPTP v9.3.1. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % Computer : n027.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:19:39 AM UTC 2026 % Result : Theorem 5.54s 5.75s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : LCL686+1.010 : TPTP v9.3.1. Released v4.0.0. % 0.00/0.03 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.08/0.35 % Computer : n027.cluster.edu % 0.08/0.35 % Model : x86_64 x86_64 % 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.08/0.35 % Memory : 8046.5625MB % 0.08/0.35 % OS : Linux 6.8.0-71-generic % 0.08/0.35 % CPULimit : 300 % 0.08/0.35 % WCLimit : 300 % 0.08/0.35 % DateTime : Sat Sep 5 16:27:43 UTC 2026 % 0.08/0.35 % CPUTime : % 0.24/0.52 start to proof:theBenchmark % 5.54/5.73 %------------------------------------------- % 5.54/5.73 % File :CSE---1.7 % 5.54/5.73 % Problem :theBenchmark % 5.54/5.73 % Transform :cnf % 5.54/5.73 % Format :tptp:raw % 5.54/5.73 % Command :java -jar mcs_scs.jar %d %s % 5.54/5.73 % 5.54/5.73 % Result :Theorem 5.199230s % 5.54/5.73 % Output :CNFRefutation 5.199230s % 5.54/5.73 %------------------------------------------- % 5.54/5.73 %------------------------------------------------------------------------------ % 5.54/5.73 % File : LCL686+1.010 : TPTP v9.3.1. Released v4.0.0. % 5.54/5.73 % Domain : Logic Calculi (Modal Logic) % 5.54/5.73 % Problem : In S4, formula provable in S5 embedding, size 10 % 5.54/5.73 % Version : Especial. % 5.54/5.73 % English : % 5.54/5.73 % 5.54/5.73 % Refs : [BHS00] Balsiger et al. (2000), A Benchmark Method for the Pro % 5.54/5.73 % : [Kam08] Kaminski (2008), Email to G. Sutcliffe % 5.54/5.73 % Source : [Kam08] % 5.54/5.73 % Names : s4_s5_p [BHS00] % 5.54/5.73 % 5.54/5.73 % Status : Theorem % 5.54/5.73 % Rating : 0.00 v9.3.0, 0.05 v9.1.0, 0.13 v9.0.0, 0.06 v8.2.0, 0.07 v8.1.0, 0.00 v7.5.0, 0.10 v7.4.0, 0.06 v7.3.0, 0.14 v7.2.0, 0.00 v6.3.0, 0.08 v6.2.0, 0.09 v6.1.0, 0.12 v6.0.0, 0.25 v5.5.0, 0.17 v5.3.0, 0.26 v5.2.0, 0.14 v5.0.0, 0.15 v4.1.0, 0.17 v4.0.1, 0.21 v4.0.0 % 5.54/5.73 % Syntax : Number of formulae : 3 ( 1 unt; 0 def) % 5.54/5.73 % Number of atoms : 294 ( 0 equ) % 5.54/5.73 % Maximal formula atoms : 290 ( 98 avg) % 5.54/5.73 % Number of connectives : 527 ( 236 ~; 177 |; 113 &) % 5.54/5.73 % ( 0 <=>; 1 =>; 0 <=; 0 <~>) % 5.54/5.74 % Maximal formula depth : 100 ( 36 avg) % 5.54/5.74 % Maximal term depth : 1 ( 1 avg) % 5.54/5.74 % Number of predicates : 32 ( 31 usr; 1 prp; 0-2 aty) % 5.54/5.74 % Number of functors : 0 ( 0 usr; 0 con; --- aty) % 5.54/5.74 % Number of variables : 67 ( 66 !; 1 ?) % 5.54/5.74 % SPC : FOF_THM_RFO_NEQ % 5.54/5.74 % 5.54/5.74 % Comments : A naive relational encoding of the modal logic problem into % 5.54/5.74 % first-order logic. % 5.54/5.74 %------------------------------------------------------------------------------ % 5.54/5.74 fof(reflexivity,axiom, % 5.54/5.74 ! [X] : r1(X,X) ). % 5.54/5.74 % 5.54/5.74 fof(transitivity,axiom, % 5.54/5.74 ! [X,Y,Z] : % 5.54/5.74 ( ( r1(X,Y) % 5.54/5.74 & r1(Y,Z) ) % 5.54/5.74 => r1(X,Z) ) ). % 5.54/5.74 % 5.54/5.74 fof(main,conjecture, % 5.54/5.74 ~ ? [X] : % 5.54/5.74 ~ ( ! [Y] : % 5.54/5.74 ( ~ r1(X,Y) % 5.54/5.74 | ~ p30(Y) % 5.54/5.74 | ! [X] : % 5.54/5.74 ( ~ r1(Y,X) % 5.54/5.74 | ~ p1(X) ) ) % 5.54/5.74 | ! [Y] : % 5.54/5.74 ( ~ r1(X,Y) % 5.54/5.74 | ~ ! [X] : % 5.54/5.74 ( ~ r1(Y,X) % 5.54/5.74 | ~ ( ! [Y] : % 5.54/5.74 ( ~ r1(X,Y) % 5.54/5.74 | ! [X] : % 5.54/5.74 ( ~ r1(Y,X) % 5.54/5.74 | ! [Y] : % 5.54/5.74 ( ~ r1(X,Y) % 5.54/5.74 | ! [X] : % 5.54/5.74 ( ~ r1(Y,X) % 5.54/5.74 | ! [Y] : % 5.54/5.74 ( ~ r1(X,Y) % 5.54/5.74 | ! [X] : % 5.54/5.74 ( ~ r1(Y,X) % 5.54/5.74 | ! [Y] : % 5.54/5.74 ( ~ r1(X,Y) % 5.54/5.74 | ! [X] : % 5.54/5.74 ( ~ r1(Y,X) % 5.54/5.74 | ! [Y] : % 5.54/5.74 ( ~ r1(X,Y) % 5.54/5.74 | ! [X] : % 5.54/5.74 ( ~ r1(Y,X) % 5.54/5.74 | ! [Y] : % 5.54/5.74 ( ~ r1(X,Y) % 5.54/5.74 | ! [X] : % 5.54/5.74 ( ~ r1(Y,X) % 5.54/5.74 | ! [Y] : % 5.54/5.74 ( ~ r1(X,Y) % 5.54/5.74 | ! [X] : % 5.54/5.74 ( ~ r1(Y,X) % 5.54/5.74 | ! [Y] : % 5.54/5.74 ( ~ r1(X,Y) % 5.54/5.74 | ! [X] : % 5.54/5.74 ( ~ r1(Y,X) % 5.54/5.74 | ! [Y] : % 5.54/5.74 ( ~ r1(X,Y) % 5.54/5.74 | ! [X] : % 5.54/5.74 ( ~ r1(Y,X) % 5.54/5.74 | ! [Y] : % 5.54/5.74 ( ~ r1(X,Y) % 5.54/5.74 | ! [X] : % 5.54/5.74 ( ~ r1(Y,X) % 5.54/5.74 | ! [Y] : % 5.54/5.74 ( ~ r1(X,Y) % 5.54/5.74 | ! [X] : % 5.54/5.74 ( ~ r1(Y,X) % 5.54/5.74 | ! [Y] : % 5.54/5.74 ( ~ r1(X,Y) % 5.54/5.74 | ! [X] : % 5.54/5.74 ( ~ r1(Y,X) % 5.54/5.74 | ! [Y] : % 5.54/5.74 ( ~ r1(X,Y) % 5.54/5.74 | ! [X] : % 5.54/5.74 ( ~ r1(Y,X) % 5.54/5.74 | ! [Y] : % 5.54/5.74 ( ~ r1(X,Y) % 5.54/5.74 | ! [X] : % 5.54/5.74 ( ~ r1(Y,X) % 5.54/5.74 | $false ) % 5.54/5.74 | ~ ! [X] : % 5.54/5.74 ( ~ r1(Y,X) % 5.54/5.74 | ~ ( ( p29(X) % 5.54/5.74 & ~ p28(X) ) % 5.54/5.74 | ( ~ p29(X) % 5.54/5.74 & p28(X) ) ) ) ) % 5.54/5.74 | ~ ! [Y] : % 5.54/5.74 ( ~ r1(X,Y) % 5.54/5.74 | ~ ( ( p28(Y) % 5.54/5.74 & ~ p27(Y) ) % 5.54/5.74 | ( ~ p28(Y) % 5.54/5.74 & p27(Y) ) ) ) ) % 5.54/5.74 | ~ ! [X] : % 5.54/5.74 ( ~ r1(Y,X) % 5.54/5.74 | ~ ( ( p27(X) % 5.54/5.74 & ~ p26(X) ) % 5.54/5.74 | ( ~ p27(X) % 5.54/5.74 & p26(X) ) ) ) ) % 5.54/5.74 | ~ ! [Y] : % 5.54/5.74 ( ~ r1(X,Y) % 5.54/5.74 | ~ ( ( p26(Y) % 5.54/5.74 & ~ p25(Y) ) % 5.54/5.74 | ( ~ p26(Y) % 5.54/5.74 & p25(Y) ) ) ) ) % 5.54/5.74 | ~ ! [X] : % 5.54/5.74 ( ~ r1(Y,X) % 5.54/5.74 | ~ ( ( p25(X) % 5.54/5.74 & ~ p24(X) ) % 5.54/5.74 | ( ~ p25(X) % 5.54/5.74 & p24(X) ) ) ) ) % 5.54/5.74 | ~ ! [Y] : % 5.54/5.74 ( ~ r1(X,Y) % 5.54/5.74 | ~ ( ( p24(Y) % 5.54/5.74 & ~ p23(Y) ) % 5.54/5.74 | ( ~ p24(Y) % 5.54/5.74 & p23(Y) ) ) ) ) % 5.54/5.74 | ~ ! [X] : % 5.54/5.74 ( ~ r1(Y,X) % 5.54/5.74 | ~ ( ( p23(X) % 5.54/5.74 & ~ p22(X) ) % 5.54/5.74 | ( ~ p23(X) % 5.54/5.74 & p22(X) ) ) ) ) % 5.54/5.74 | ~ ! [Y] : % 5.54/5.74 ( ~ r1(X,Y) % 5.54/5.74 | ~ ( ( p22(Y) % 5.54/5.74 & ~ p21(Y) ) % 5.54/5.74 | ( ~ p22(Y) % 5.54/5.74 & p21(Y) ) ) ) ) % 5.54/5.74 | ~ ! [X] : % 5.54/5.74 ( ~ r1(Y,X) % 5.54/5.74 | ~ ( ( p21(X) % 5.54/5.74 & ~ p20(X) ) % 5.54/5.74 | ( ~ p21(X) % 5.54/5.74 & p20(X) ) ) ) ) % 5.54/5.75 | ~ ! [Y] : % 5.54/5.75 ( ~ r1(X,Y) % 5.54/5.75 | ~ ( ( p20(Y) % 5.54/5.75 & ~ p19(Y) ) % 5.54/5.75 | ( ~ p20(Y) % 5.54/5.75 & p19(Y) ) ) ) ) % 5.54/5.75 | ~ ! [X] : % 5.54/5.75 ( ~ r1(Y,X) % 5.54/5.75 | ~ ( ( p19(X) % 5.54/5.75 & ~ p18(X) ) % 5.54/5.75 | ( ~ p19(X) % 5.54/5.75 & p18(X) ) ) ) ) % 5.54/5.75 | ~ ! [Y] : % 5.54/5.75 ( ~ r1(X,Y) % 5.54/5.75 | ~ ( ( p18(Y) % 5.54/5.75 & ~ p17(Y) ) % 5.54/5.75 | ( ~ p18(Y) % 5.54/5.75 & p17(Y) ) ) ) ) % 5.54/5.75 | ~ ! [X] : % 5.54/5.75 ( ~ r1(Y,X) % 5.54/5.75 | ~ ( ( p17(X) % 5.54/5.75 & ~ p16(X) ) % 5.54/5.75 | ( ~ p17(X) % 5.54/5.75 & p16(X) ) ) ) ) % 5.54/5.75 | ~ ! [Y] : % 5.54/5.75 ( ~ r1(X,Y) % 5.54/5.75 | ~ ( ( p16(Y) % 5.54/5.75 & ~ p15(Y) ) % 5.54/5.75 | ( ~ p16(Y) % 5.54/5.75 & p15(Y) ) ) ) ) % 5.54/5.75 | ~ ! [X] : % 5.54/5.75 ( ~ r1(Y,X) % 5.54/5.75 | ~ ( ( p15(X) % 5.54/5.75 & ~ p14(X) ) % 5.54/5.75 | ( ~ p15(X) % 5.54/5.75 & p14(X) ) ) ) ) % 5.54/5.75 | ~ ! [Y] : % 5.54/5.75 ( ~ r1(X,Y) % 5.54/5.75 | ~ ( ( p14(Y) % 5.54/5.75 & ~ p13(Y) ) % 5.54/5.75 | ( ~ p14(Y) % 5.54/5.75 & p13(Y) ) ) ) ) % 5.54/5.75 | ~ ! [X] : % 5.54/5.75 ( ~ r1(Y,X) % 5.54/5.75 | ~ ( ( p13(X) % 5.54/5.75 & ~ p12(X) ) % 5.54/5.75 | ( ~ p13(X) % 5.54/5.75 & p12(X) ) ) ) ) % 5.54/5.75 | ~ ! [Y] : % 5.54/5.75 ( ~ r1(X,Y) % 5.54/5.75 | ~ ( ( p12(Y) % 5.54/5.75 & ~ p11(Y) ) % 5.54/5.75 | ( ~ p12(Y) % 5.54/5.75 & p11(Y) ) ) ) ) % 5.54/5.75 | ~ ! [X] : % 5.54/5.75 ( ~ r1(Y,X) % 5.54/5.75 | ~ ( ( p11(X) % 5.54/5.75 & ~ p10(X) ) % 5.54/5.75 | ( ~ p11(X) % 5.54/5.75 & p10(X) ) ) ) ) % 5.54/5.75 | ~ ! [Y] : % 5.54/5.75 ( ~ r1(X,Y) % 5.54/5.75 | ~ ( ( p10(Y) % 5.54/5.75 & ~ p9(Y) ) % 5.54/5.75 | ( ~ p10(Y) % 5.54/5.75 & p9(Y) ) ) ) ) % 5.54/5.75 | ~ ! [X] : % 5.54/5.75 ( ~ r1(Y,X) % 5.54/5.75 | ~ ( ( p9(X) % 5.54/5.75 & ~ p8(X) ) % 5.54/5.75 | ( ~ p9(X) % 5.54/5.75 & p8(X) ) ) ) ) % 5.54/5.75 | ~ ! [Y] : % 5.54/5.75 ( ~ r1(X,Y) % 5.54/5.75 | ~ ( ( p8(Y) % 5.54/5.75 & ~ p7(Y) ) % 5.54/5.75 | ( ~ p8(Y) % 5.54/5.75 & p7(Y) ) ) ) ) % 5.54/5.75 | ~ ! [X] : % 5.54/5.75 ( ~ r1(Y,X) % 5.54/5.75 | ~ ( ( p7(X) % 5.54/5.75 & ~ p6(X) ) % 5.54/5.75 | ( ~ p7(X) % 5.54/5.75 & p6(X) ) ) ) ) % 5.54/5.75 | ~ ! [Y] : % 5.54/5.75 ( ~ r1(X,Y) % 5.54/5.75 | ~ ( ( p6(Y) % 5.54/5.75 & ~ p5(Y) ) % 5.54/5.75 | ( ~ p6(Y) % 5.54/5.75 & p5(Y) ) ) ) ) % 5.54/5.75 | ~ ! [X] : % 5.54/5.75 ( ~ r1(Y,X) % 5.54/5.75 | ~ ( ( p5(X) % 5.54/5.75 & ~ p4(X) ) % 5.54/5.75 | ( ~ p5(X) % 5.54/5.75 & p4(X) ) ) ) ) % 5.54/5.75 | ~ ! [Y] : % 5.54/5.75 ( ~ r1(X,Y) % 5.54/5.75 | ~ ( ( p4(Y) % 5.54/5.75 & ~ p3(Y) ) % 5.54/5.75 | ( ~ p4(Y) % 5.54/5.75 & p3(Y) ) ) ) ) % 5.54/5.75 | ~ ! [X] : % 5.54/5.75 ( ~ r1(Y,X) % 5.54/5.75 | ~ ( ( p3(X) % 5.54/5.75 & ~ p2(X) ) % 5.54/5.75 | ( ~ p3(X) % 5.54/5.75 & p2(X) ) ) ) ) % 5.54/5.75 | ~ ! [Y] : % 5.54/5.75 ( ~ r1(X,Y) % 5.54/5.75 | ~ ( ( p2(Y) % 5.54/5.75 & ~ p1(Y) ) % 5.54/5.75 | ( ~ p2(Y) % 5.54/5.75 & p1(Y) ) ) ) % 5.54/5.75 | ! [Y] : % 5.54/5.75 ( ~ r1(X,Y) % 5.54/5.75 | p30(Y) ) % 5.54/5.75 | ! [Y] : % 5.54/5.75 ( ~ r1(X,Y) % 5.54/5.75 | ( ~ p28(Y) % 5.54/5.75 & ~ p29(Y) ) % 5.54/5.75 | ( p29(Y) % 5.54/5.75 & p28(Y) ) % 5.54/5.75 | ( ~ p27(Y) % 5.54/5.75 & ~ p28(Y) ) % 5.54/5.75 | ( p28(Y) % 5.54/5.75 & p27(Y) ) % 5.54/5.75 | ( ~ p26(Y) % 5.54/5.75 & ~ p27(Y) ) % 5.54/5.75 | ( p27(Y) % 5.54/5.75 & p26(Y) ) % 5.54/5.75 | ( ~ p25(Y) % 5.54/5.75 & ~ p26(Y) ) % 5.54/5.75 | ( p26(Y) % 5.54/5.75 & p25(Y) ) % 5.54/5.75 | ( ~ p24(Y) % 5.54/5.75 & ~ p25(Y) ) % 5.54/5.75 | ( p25(Y) % 5.54/5.75 & p24(Y) ) % 5.54/5.75 | ( ~ p23(Y) % 5.54/5.75 & ~ p24(Y) ) % 5.54/5.75 | ( p24(Y) % 5.54/5.75 & p23(Y) ) % 5.54/5.75 | ( ~ p22(Y) % 5.54/5.75 & ~ p23(Y) ) % 5.54/5.75 | ( p23(Y) % 5.54/5.75 & p22(Y) ) % 5.54/5.75 | ( ~ p21(Y) % 5.54/5.75 & ~ p22(Y) ) % 5.54/5.75 | ( p22(Y) % 5.54/5.75 & p21(Y) ) % 5.54/5.75 | ( ~ p20(Y) % 5.54/5.75 & ~ p21(Y) ) % 5.54/5.75 | ( p21(Y) % 5.54/5.75 & p20(Y) ) % 5.54/5.75 | ( ~ p19(Y) % 5.54/5.75 & ~ p20(Y) ) % 5.54/5.75 | ( p20(Y) % 5.54/5.75 & p19(Y) ) % 5.54/5.75 | ( ~ p18(Y) % 5.54/5.75 & ~ p19(Y) ) % 5.54/5.75 | ( p19(Y) % 5.54/5.75 & p18(Y) ) % 5.54/5.75 | ( ~ p17(Y) % 5.54/5.75 & ~ p18(Y) ) % 5.54/5.75 | ( p18(Y) % 5.54/5.75 & p17(Y) ) % 5.54/5.75 | ( ~ p16(Y) % 5.54/5.75 & ~ p17(Y) ) % 5.54/5.75 | ( p17(Y) % 5.54/5.75 & p16(Y) ) % 5.54/5.75 | ( ~ p15(Y) % 5.54/5.75 & ~ p16(Y) ) % 5.54/5.75 | ( p16(Y) % 5.54/5.75 & p15(Y) ) % 5.54/5.75 | ( ~ p14(Y) % 5.54/5.75 & ~ p15(Y) ) % 5.54/5.75 | ( p15(Y) % 5.54/5.75 & p14(Y) ) % 5.54/5.75 | ( ~ p13(Y) % 5.54/5.75 & ~ p14(Y) ) % 5.54/5.75 | ( p14(Y) % 5.54/5.75 & p13(Y) ) % 5.54/5.75 | ( ~ p12(Y) % 5.54/5.75 & ~ p13(Y) ) % 5.54/5.75 | ( p13(Y) % 5.54/5.75 & p12(Y) ) % 5.54/5.75 | ( ~ p11(Y) % 5.54/5.75 & ~ p12(Y) ) % 5.54/5.75 | ( p12(Y) % 5.54/5.75 & p11(Y) ) % 5.54/5.75 | ( ~ p10(Y) % 5.54/5.75 & ~ p11(Y) ) % 5.54/5.75 | ( p11(Y) % 5.54/5.75 & p10(Y) ) % 5.54/5.75 | ( ~ p9(Y) % 5.54/5.75 & ~ p10(Y) ) % 5.54/5.75 | ( p10(Y) % 5.54/5.75 & p9(Y) ) % 5.54/5.75 | ( ~ p8(Y) % 5.54/5.75 & ~ p9(Y) ) % 5.54/5.75 | ( p9(Y) % 5.54/5.75 & p8(Y) ) % 5.54/5.75 | ( ~ p7(Y) % 5.54/5.75 & ~ p8(Y) ) % 5.54/5.75 | ( p8(Y) % 5.54/5.75 & p7(Y) ) % 5.54/5.75 | ( ~ p6(Y) % 5.54/5.75 & ~ p7(Y) ) % 5.54/5.75 | ( p7(Y) % 5.54/5.75 & p6(Y) ) % 5.54/5.75 | ( ~ p5(Y) % 5.54/5.75 & ~ p6(Y) ) % 5.54/5.75 | ( p6(Y) % 5.54/5.75 & p5(Y) ) % 5.54/5.75 | ( ~ p4(Y) % 5.54/5.75 & ~ p5(Y) ) % 5.54/5.75 | ( p5(Y) % 5.54/5.75 & p4(Y) ) % 5.54/5.75 | ( ~ p3(Y) % 5.54/5.75 & ~ p4(Y) ) % 5.54/5.75 | ( p4(Y) % 5.54/5.75 & p3(Y) ) % 5.54/5.75 | ( ~ p2(Y) % 5.54/5.75 & ~ p3(Y) ) % 5.54/5.75 | ( p3(Y) % 5.54/5.75 & p2(Y) ) % 5.54/5.75 | ( ~ p1(Y) % 5.54/5.75 & ~ p2(Y) ) % 5.54/5.75 | ( p2(Y) % 5.54/5.75 & p1(Y) ) ) ) ) ) ) ). % 5.54/5.75 % 5.54/5.75 %------------------------------------------------------------------------------ % 5.54/5.75 %------------------------------------------- % 5.54/5.75 % Proof found % 5.54/5.75 % SZS status Theorem for theBenchmark % 5.54/5.75 % SZS output start Proof % 5.54/5.75 %ClaNum:151(EqnAxiom:0) % 5.54/5.75 %VarNum:550(SingletonVarNum:204) % 5.54/5.75 %MaxLitNum:4 % 5.54/5.75 %MaxfuncDepth:1 % 5.54/5.75 %SharedTerms:9 % 5.54/5.75 %goalClause: 1 2 3 4 5 8 % 5.54/5.76 %singleGoalClaCount:5 % 5.54/5.76 [1]P1(a1) % 5.54/5.76 [2]P2(a23) % 5.54/5.76 [3]P26(a2,a1) % 5.54/5.76 [4]P26(a2,a29) % 5.54/5.76 [5]P26(a1,a23) % 5.54/5.76 [6]P26(x61,x61) % 5.54/5.76 [8]P3(x81)+~P26(a29,x81) % 5.54/5.76 [7]~P3(x71)+~P1(f24(x71)) % 5.54/5.76 [9]~P3(x91)+P26(x91,f30(x91)) % 5.54/5.76 [10]~P3(x101)+P26(x101,f24(x101)) % 5.54/5.76 [11]~P3(x111)+P26(x111,f28(x111)) % 5.54/5.76 [40]~P3(x401)+P26(f30(x401),f31(x401)) % 5.54/5.76 [41]~P3(x411)+P26(f31(x411),f32(x411)) % 5.54/5.76 [42]~P3(x421)+P26(f32(x421),f33(x421)) % 5.54/5.76 [43]~P3(x431)+P26(f33(x431),f34(x431)) % 5.54/5.76 [44]~P3(x441)+P26(f34(x441),f3(x441)) % 5.54/5.76 [45]~P3(x451)+P26(f3(x451),f4(x451)) % 5.54/5.76 [46]~P3(x461)+P26(f4(x461),f5(x461)) % 5.54/5.76 [47]~P3(x471)+P26(f5(x471),f6(x471)) % 5.54/5.76 [48]~P3(x481)+P26(f6(x481),f7(x481)) % 5.54/5.76 [49]~P3(x491)+P26(f7(x491),f8(x491)) % 5.54/5.76 [50]~P3(x501)+P26(f8(x501),f9(x501)) % 5.54/5.76 [51]~P3(x511)+P26(f9(x511),f10(x511)) % 5.54/5.76 [52]~P3(x521)+P26(f10(x521),f11(x521)) % 5.54/5.76 [53]~P3(x531)+P26(f11(x531),f12(x531)) % 5.54/5.76 [54]~P3(x541)+P26(f12(x541),f13(x541)) % 5.54/5.76 [55]~P3(x551)+P26(f13(x551),f14(x551)) % 5.54/5.76 [56]~P3(x561)+P26(f14(x561),f15(x561)) % 5.54/5.76 [57]~P3(x571)+P26(f15(x571),f16(x571)) % 5.54/5.76 [58]~P3(x581)+P26(f16(x581),f17(x581)) % 5.54/5.76 [59]~P3(x591)+P26(f17(x591),f18(x591)) % 5.54/5.76 [60]~P3(x601)+P26(f18(x601),f19(x601)) % 5.54/5.76 [61]~P3(x611)+P26(f19(x611),f20(x611)) % 5.54/5.76 [62]~P3(x621)+P26(f20(x621),f21(x621)) % 5.54/5.76 [63]~P3(x631)+P26(f21(x631),f22(x631)) % 5.54/5.76 [64]~P3(x641)+P26(f22(x641),f25(x641)) % 5.54/5.76 [65]~P3(x651)+P26(f25(x651),f26(x651)) % 5.54/5.76 [66]~P3(x661)+P26(f26(x661),f27(x661)) % 5.54/5.76 [12]~P3(x121)+P2(f28(x121))+P4(f28(x121)) % 5.54/5.76 [13]~P3(x131)+P15(f28(x131))+P16(f28(x131)) % 5.54/5.76 [14]~P3(x141)+P16(f28(x141))+P17(f28(x141)) % 5.54/5.76 [15]~P3(x151)+P17(f28(x151))+P18(f28(x151)) % 5.54/5.76 [16]~P3(x161)+P18(f28(x161))+P19(f28(x161)) % 5.54/5.76 [17]~P3(x171)+P19(f28(x171))+P20(f28(x171)) % 5.54/5.76 [18]~P3(x181)+P20(f28(x181))+P21(f28(x181)) % 5.54/5.76 [19]~P3(x191)+P21(f28(x191))+P22(f28(x191)) % 5.54/5.76 [20]~P3(x201)+P22(f28(x201))+P23(f28(x201)) % 5.54/5.76 [21]~P3(x211)+P23(f28(x211))+P24(f28(x211)) % 5.54/5.76 [22]~P3(x221)+P24(f28(x221))+P5(f28(x221)) % 5.54/5.76 [23]~P3(x231)+P5(f28(x231))+P6(f28(x231)) % 5.54/5.76 [24]~P3(x241)+P6(f28(x241))+P7(f28(x241)) % 5.54/5.76 [25]~P3(x251)+P7(f28(x251))+P8(f28(x251)) % 5.54/5.76 [26]~P3(x261)+P8(f28(x261))+P9(f28(x261)) % 5.54/5.76 [27]~P3(x271)+P9(f28(x271))+P10(f28(x271)) % 5.54/5.76 [28]~P3(x281)+P10(f28(x281))+P11(f28(x281)) % 5.54/5.76 [29]~P3(x291)+P11(f28(x291))+P12(f28(x291)) % 5.54/5.76 [30]~P3(x301)+P12(f28(x301))+P13(f28(x301)) % 5.54/5.76 [31]~P3(x311)+P13(f28(x311))+P14(f28(x311)) % 5.54/5.76 [32]~P3(x321)+P14(f28(x321))+P27(f28(x321)) % 5.54/5.76 [33]~P3(x331)+P27(f28(x331))+P28(f28(x331)) % 5.54/5.76 [34]~P3(x341)+P28(f28(x341))+P29(f28(x341)) % 5.54/5.76 [35]~P3(x351)+P29(f28(x351))+P30(f28(x351)) % 5.54/5.76 [36]~P3(x361)+P30(f28(x361))+P31(f28(x361)) % 5.54/5.76 [37]~P3(x371)+P31(f28(x371))+P32(f28(x371)) % 5.54/5.76 [38]~P3(x381)+P32(f28(x381))+P25(f28(x381)) % 5.54/5.76 [39]~P3(x391)+P25(f28(x391))+P4(f28(x391)) % 5.54/5.76 [67]~P3(x671)+~P2(f28(x671))+~P4(f28(x671)) % 5.54/5.76 [68]~P3(x681)+~P15(f28(x681))+~P16(f28(x681)) % 5.54/5.76 [69]~P3(x691)+~P16(f28(x691))+~P17(f28(x691)) % 5.54/5.76 [70]~P3(x701)+~P17(f28(x701))+~P18(f28(x701)) % 5.54/5.76 [71]~P3(x711)+~P18(f28(x711))+~P19(f28(x711)) % 5.54/5.76 [72]~P3(x721)+~P19(f28(x721))+~P20(f28(x721)) % 5.54/5.76 [73]~P3(x731)+~P20(f28(x731))+~P21(f28(x731)) % 5.54/5.76 [74]~P3(x741)+~P21(f28(x741))+~P22(f28(x741)) % 5.54/5.76 [75]~P3(x751)+~P22(f28(x751))+~P23(f28(x751)) % 5.54/5.76 [76]~P3(x761)+~P23(f28(x761))+~P24(f28(x761)) % 5.54/5.76 [77]~P3(x771)+~P24(f28(x771))+~P5(f28(x771)) % 5.54/5.76 [78]~P3(x781)+~P5(f28(x781))+~P6(f28(x781)) % 5.54/5.76 [79]~P3(x791)+~P6(f28(x791))+~P7(f28(x791)) % 5.54/5.76 [80]~P3(x801)+~P7(f28(x801))+~P8(f28(x801)) % 5.54/5.76 [81]~P3(x811)+~P8(f28(x811))+~P9(f28(x811)) % 5.54/5.76 [82]~P3(x821)+~P9(f28(x821))+~P10(f28(x821)) % 5.54/5.76 [83]~P3(x831)+~P10(f28(x831))+~P11(f28(x831)) % 5.54/5.76 [84]~P3(x841)+~P11(f28(x841))+~P12(f28(x841)) % 5.54/5.76 [85]~P3(x851)+~P12(f28(x851))+~P13(f28(x851)) % 5.54/5.76 [86]~P3(x861)+~P13(f28(x861))+~P14(f28(x861)) % 5.54/5.76 [87]~P3(x871)+~P14(f28(x871))+~P27(f28(x871)) % 5.54/5.76 [88]~P3(x881)+~P27(f28(x881))+~P28(f28(x881)) % 5.54/5.76 [89]~P3(x891)+~P28(f28(x891))+~P29(f28(x891)) % 5.54/5.76 [90]~P3(x901)+~P29(f28(x901))+~P30(f28(x901)) % 5.54/5.76 [91]~P3(x911)+~P30(f28(x911))+~P31(f28(x911)) % 5.54/5.76 [92]~P3(x921)+~P31(f28(x921))+~P32(f28(x921)) % 5.54/5.76 [93]~P3(x931)+~P32(f28(x931))+~P25(f28(x931)) % 5.54/5.76 [94]~P3(x941)+~P25(f28(x941))+~P4(f28(x941)) % 5.54/5.76 [151]~P26(x1511,x1513)+P26(x1511,x1512)+~P26(x1513,x1512) % 5.54/5.76 [95]~P4(x951)+~P26(x952,x951)+P2(x951)+~P3(x952) % 5.54/5.76 [96]~P2(x961)+~P26(x962,x961)+P4(x961)+~P3(x962) % 5.54/5.76 [97]~P16(x971)+P15(x971)+~P3(x972)+~P26(f26(x972),x971) % 5.54/5.76 [98]~P15(x981)+P16(x981)+~P3(x982)+~P26(f26(x982),x981) % 5.54/5.76 [99]~P17(x991)+P16(x991)+~P3(x992)+~P26(f25(x992),x991) % 5.54/5.76 [100]~P16(x1001)+P17(x1001)+~P3(x1002)+~P26(f25(x1002),x1001) % 5.54/5.76 [101]~P18(x1011)+P17(x1011)+~P3(x1012)+~P26(f22(x1012),x1011) % 5.54/5.76 [102]~P17(x1021)+P18(x1021)+~P3(x1022)+~P26(f22(x1022),x1021) % 5.54/5.76 [103]~P19(x1031)+P18(x1031)+~P3(x1032)+~P26(f21(x1032),x1031) % 5.54/5.76 [104]~P18(x1041)+P19(x1041)+~P3(x1042)+~P26(f21(x1042),x1041) % 5.54/5.76 [105]~P20(x1051)+P19(x1051)+~P3(x1052)+~P26(f20(x1052),x1051) % 5.54/5.76 [106]~P19(x1061)+P20(x1061)+~P3(x1062)+~P26(f20(x1062),x1061) % 5.54/5.76 [107]~P21(x1071)+P20(x1071)+~P3(x1072)+~P26(f19(x1072),x1071) % 5.54/5.76 [108]~P20(x1081)+P21(x1081)+~P3(x1082)+~P26(f19(x1082),x1081) % 5.54/5.76 [109]~P22(x1091)+P21(x1091)+~P3(x1092)+~P26(f18(x1092),x1091) % 5.54/5.76 [110]~P21(x1101)+P22(x1101)+~P3(x1102)+~P26(f18(x1102),x1101) % 5.54/5.76 [111]~P23(x1111)+P22(x1111)+~P3(x1112)+~P26(f17(x1112),x1111) % 5.54/5.76 [112]~P22(x1121)+P23(x1121)+~P3(x1122)+~P26(f17(x1122),x1121) % 5.54/5.76 [113]~P24(x1131)+P23(x1131)+~P3(x1132)+~P26(f16(x1132),x1131) % 5.54/5.76 [114]~P23(x1141)+P24(x1141)+~P3(x1142)+~P26(f16(x1142),x1141) % 5.54/5.76 [115]~P5(x1151)+P24(x1151)+~P3(x1152)+~P26(f15(x1152),x1151) % 5.54/5.76 [116]~P24(x1161)+P5(x1161)+~P3(x1162)+~P26(f15(x1162),x1161) % 5.54/5.76 [117]~P6(x1171)+P5(x1171)+~P3(x1172)+~P26(f14(x1172),x1171) % 5.54/5.76 [118]~P5(x1181)+P6(x1181)+~P3(x1182)+~P26(f14(x1182),x1181) % 5.54/5.76 [119]~P7(x1191)+P6(x1191)+~P3(x1192)+~P26(f13(x1192),x1191) % 5.54/5.76 [120]~P6(x1201)+P7(x1201)+~P3(x1202)+~P26(f13(x1202),x1201) % 5.54/5.76 [121]~P8(x1211)+P7(x1211)+~P3(x1212)+~P26(f12(x1212),x1211) % 5.54/5.76 [122]~P7(x1221)+P8(x1221)+~P3(x1222)+~P26(f12(x1222),x1221) % 5.54/5.76 [123]~P9(x1231)+P8(x1231)+~P3(x1232)+~P26(f11(x1232),x1231) % 5.54/5.76 [124]~P8(x1241)+P9(x1241)+~P3(x1242)+~P26(f11(x1242),x1241) % 5.54/5.76 [125]~P10(x1251)+P9(x1251)+~P3(x1252)+~P26(f10(x1252),x1251) % 5.54/5.76 [126]~P9(x1261)+P10(x1261)+~P3(x1262)+~P26(f10(x1262),x1261) % 5.54/5.76 [127]~P11(x1271)+P10(x1271)+~P3(x1272)+~P26(f9(x1272),x1271) % 5.54/5.76 [128]~P10(x1281)+P11(x1281)+~P3(x1282)+~P26(f9(x1282),x1281) % 5.54/5.76 [129]~P12(x1291)+P11(x1291)+~P3(x1292)+~P26(f8(x1292),x1291) % 5.54/5.76 [130]~P11(x1301)+P12(x1301)+~P3(x1302)+~P26(f8(x1302),x1301) % 5.54/5.76 [131]~P13(x1311)+P12(x1311)+~P3(x1312)+~P26(f7(x1312),x1311) % 5.54/5.76 [132]~P12(x1321)+P13(x1321)+~P3(x1322)+~P26(f7(x1322),x1321) % 5.54/5.76 [133]~P14(x1331)+P13(x1331)+~P3(x1332)+~P26(f6(x1332),x1331) % 5.54/5.76 [134]~P13(x1341)+P14(x1341)+~P3(x1342)+~P26(f6(x1342),x1341) % 5.54/5.76 [135]~P27(x1351)+P14(x1351)+~P3(x1352)+~P26(f5(x1352),x1351) % 5.54/5.76 [136]~P14(x1361)+P27(x1361)+~P3(x1362)+~P26(f5(x1362),x1361) % 5.54/5.76 [137]~P28(x1371)+P27(x1371)+~P3(x1372)+~P26(f4(x1372),x1371) % 5.54/5.76 [138]~P27(x1381)+P28(x1381)+~P3(x1382)+~P26(f4(x1382),x1381) % 5.54/5.76 [139]~P29(x1391)+P28(x1391)+~P3(x1392)+~P26(f3(x1392),x1391) % 5.54/5.76 [140]~P28(x1401)+P29(x1401)+~P3(x1402)+~P26(f3(x1402),x1401) % 5.54/5.76 [141]~P30(x1411)+P29(x1411)+~P3(x1412)+~P26(f34(x1412),x1411) % 5.54/5.76 [142]~P29(x1421)+P30(x1421)+~P3(x1422)+~P26(f34(x1422),x1421) % 5.54/5.76 [143]~P31(x1431)+P30(x1431)+~P3(x1432)+~P26(f33(x1432),x1431) % 5.54/5.76 [144]~P30(x1441)+P31(x1441)+~P3(x1442)+~P26(f33(x1442),x1441) % 5.54/5.76 [145]~P32(x1451)+P31(x1451)+~P3(x1452)+~P26(f32(x1452),x1451) % 5.54/5.76 [146]~P31(x1461)+P32(x1461)+~P3(x1462)+~P26(f32(x1462),x1461) % 5.54/5.76 [147]~P25(x1471)+P32(x1471)+~P3(x1472)+~P26(f31(x1472),x1471) % 5.54/5.76 [148]~P32(x1481)+P25(x1481)+~P3(x1482)+~P26(f31(x1482),x1481) % 5.54/5.76 [149]~P4(x1491)+P25(x1491)+~P3(x1492)+~P26(f30(x1492),x1491) % 5.54/5.76 [150]~P25(x1501)+P4(x1501)+~P3(x1502)+~P26(f30(x1502),x1501) % 5.54/5.76 %EqnAxiom % 5.54/5.76 % 5.54/5.76 %------------------------------------------- % 5.54/5.76 cnf(152,plain, % 5.54/5.76 (P3(a29)), % 5.54/5.76 inference(scs_inference,[],[6,8])). % 5.54/5.76 cnf(372,plain, % 5.54/5.76 (P26(a29,f30(a29))), % 5.54/5.76 inference(scs_inference,[],[6,9,8])). % 5.54/5.76 cnf(373,plain, % 5.54/5.76 (P3(f30(a29))), % 5.54/5.76 inference(scs_inference,[],[372,8])). % 5.54/5.76 cnf(2192,plain, % 5.54/5.76 (P23(f28(f30(a29)))+P24(f28(f30(a29)))), % 5.54/5.76 inference(scs_inference,[],[372,21,8])). % 5.54/5.76 cnf(2193,plain, % 5.54/5.76 (P24(f28(f30(a29)))+~P22(f28(f30(a29)))), % 5.54/5.76 inference(scs_inference,[],[373,2192,75])). % 5.54/5.76 cnf(2263,plain, % 5.54/5.76 (P32(f28(f30(a29)))+P25(f28(f30(a29)))), % 5.54/5.76 inference(scs_inference,[],[372,38,8])). % 5.54/5.76 cnf(2264,plain, % 5.54/5.76 (P25(f28(f30(a29)))+~P31(f28(f30(a29)))), % 5.54/5.76 inference(scs_inference,[],[373,2263,92])). % 5.54/5.76 cnf(2265,plain, % 5.54/5.76 (~P31(f28(f30(a29)))+~P32(f28(f30(a29)))), % 5.54/5.76 inference(scs_inference,[],[373,2264,93])). % 5.54/5.76 cnf(2266,plain, % 5.54/5.76 (~P32(f28(f30(a29)))+P30(f28(f30(a29)))), % 5.54/5.76 inference(scs_inference,[],[373,2265,36])). % 5.54/5.76 cnf(2267,plain, % 5.54/5.76 (P30(f28(f30(a29)))+P25(f28(f30(a29)))), % 5.54/5.76 inference(scs_inference,[],[2266,2263])). % 5.54/5.76 cnf(2268,plain, % 5.54/5.76 (P25(f28(f30(a29)))+~P29(f28(f30(a29)))), % 5.54/5.76 inference(scs_inference,[],[373,2267,90])). % 5.54/5.76 cnf(2269,plain, % 5.54/5.76 (~P29(f28(f30(a29)))+~P4(f28(f30(a29)))), % 5.54/5.76 inference(scs_inference,[],[373,2268,94])). % 5.54/5.76 cnf(2270,plain, % 5.54/5.76 (~P4(f28(f30(a29)))+P28(f28(f30(a29)))), % 5.54/5.76 inference(scs_inference,[],[373,2269,34])). % 5.54/5.76 cnf(2271,plain, % 5.54/5.76 (P28(f28(f30(a29)))+P2(f28(f30(a29)))), % 5.54/5.76 inference(scs_inference,[],[373,2270,12])). % 5.54/5.76 cnf(2272,plain, % 5.54/5.76 (P2(f28(f30(a29)))+~P27(f28(f30(a29)))), % 5.54/5.76 inference(scs_inference,[],[373,2271,88])). % 5.54/5.76 cnf(2273,plain, % 5.54/5.76 (~P27(f28(f30(a29)))+~P4(f28(f30(a29)))), % 5.54/5.76 inference(scs_inference,[],[373,2272,67])). % 5.54/5.76 cnf(2274,plain, % 5.54/5.76 (~P4(f28(f30(a29)))+P14(f28(f30(a29)))), % 5.54/5.76 inference(scs_inference,[],[373,2273,32])). % 5.54/5.76 cnf(2275,plain, % 5.54/5.76 (P14(f28(f30(a29)))+P25(f28(f30(a29)))), % 5.54/5.76 inference(scs_inference,[],[373,2274,39])). % 5.54/5.76 cnf(2276,plain, % 5.54/5.76 (P25(f28(f30(a29)))+~P13(f28(f30(a29)))), % 5.54/5.76 inference(scs_inference,[],[373,2275,86])). % 5.54/5.76 cnf(2277,plain, % 5.54/5.76 (~P13(f28(f30(a29)))+~P32(f28(f30(a29)))), % 5.54/5.76 inference(scs_inference,[],[373,2276,93])). % 5.54/5.76 cnf(2278,plain, % 5.54/5.76 (~P32(f28(f30(a29)))+P12(f28(f30(a29)))), % 5.54/5.76 inference(scs_inference,[],[373,2277,30])). % 5.54/5.76 cnf(2279,plain, % 5.54/5.76 (P12(f28(f30(a29)))+P25(f28(f30(a29)))), % 5.54/5.76 inference(scs_inference,[],[2278,2263])). % 5.54/5.76 cnf(2280,plain, % 5.54/5.76 (P25(f28(f30(a29)))+~P11(f28(f30(a29)))), % 5.54/5.76 inference(scs_inference,[],[373,2279,84])). % 5.54/5.76 cnf(2281,plain, % 5.54/5.76 (~P11(f28(f30(a29)))+~P4(f28(f30(a29)))), % 5.54/5.76 inference(scs_inference,[],[373,2280,94])). % 5.54/5.76 cnf(2282,plain, % 5.54/5.76 (~P4(f28(f30(a29)))+P10(f28(f30(a29)))), % 5.54/5.76 inference(scs_inference,[],[373,2281,28])). % 5.54/5.76 cnf(2283,plain, % 5.54/5.76 (P10(f28(f30(a29)))+P2(f28(f30(a29)))), % 5.54/5.76 inference(scs_inference,[],[373,2282,12])). % 5.54/5.76 cnf(2284,plain, % 5.54/5.76 (P2(f28(f30(a29)))+~P9(f28(f30(a29)))), % 5.54/5.76 inference(scs_inference,[],[373,2283,82])). % 5.54/5.76 cnf(2285,plain, % 5.54/5.76 (~P9(f28(f30(a29)))+~P4(f28(f30(a29)))), % 5.54/5.76 inference(scs_inference,[],[373,2284,67])). % 5.54/5.76 cnf(2286,plain, % 5.54/5.76 (~P4(f28(f30(a29)))+P8(f28(f30(a29)))), % 5.54/5.76 inference(scs_inference,[],[373,2285,26])). % 5.54/5.76 cnf(2287,plain, % 5.54/5.76 (P8(f28(f30(a29)))+P25(f28(f30(a29)))), % 5.54/5.76 inference(scs_inference,[],[373,2286,39])). % 5.54/5.76 cnf(2288,plain, % 5.54/5.76 (P25(f28(f30(a29)))+~P7(f28(f30(a29)))), % 5.54/5.76 inference(scs_inference,[],[373,2287,80])). % 5.54/5.76 cnf(2289,plain, % 5.54/5.76 (~P7(f28(f30(a29)))+~P32(f28(f30(a29)))), % 5.54/5.76 inference(scs_inference,[],[373,2288,93])). % 5.54/5.76 cnf(2290,plain, % 5.54/5.76 (~P32(f28(f30(a29)))+P6(f28(f30(a29)))), % 5.54/5.76 inference(scs_inference,[],[373,2289,24])). % 5.54/5.76 cnf(2291,plain, % 5.54/5.76 (P6(f28(f30(a29)))+P25(f28(f30(a29)))), % 5.54/5.76 inference(scs_inference,[],[2290,2263])). % 5.54/5.76 cnf(2292,plain, % 5.54/5.76 (P25(f28(f30(a29)))+~P5(f28(f30(a29)))), % 5.54/5.76 inference(scs_inference,[],[373,2291,78])). % 5.54/5.76 cnf(2293,plain, % 5.54/5.76 (~P5(f28(f30(a29)))+~P4(f28(f30(a29)))), % 5.54/5.76 inference(scs_inference,[],[373,2292,94])). % 5.54/5.76 cnf(2294,plain, % 5.54/5.76 (~P4(f28(f30(a29)))+P24(f28(f30(a29)))), % 5.54/5.76 inference(scs_inference,[],[373,2293,22])). % 5.54/5.76 cnf(2295,plain, % 5.54/5.76 (P24(f28(f30(a29)))+P2(f28(f30(a29)))), % 5.54/5.76 inference(scs_inference,[],[373,2294,12])). % 5.54/5.76 cnf(2296,plain, % 5.54/5.76 (P2(f28(f30(a29)))+~P23(f28(f30(a29)))), % 5.54/5.76 inference(scs_inference,[],[373,2295,76])). % 5.54/5.76 cnf(2297,plain, % 5.54/5.76 (~P23(f28(f30(a29)))+~P4(f28(f30(a29)))), % 5.54/5.76 inference(scs_inference,[],[373,2296,67])). % 5.54/5.76 cnf(2298,plain, % 5.54/5.76 (~P4(f28(f30(a29)))+P22(f28(f30(a29)))), % 5.54/5.76 inference(scs_inference,[],[373,2297,20])). % 5.54/5.76 cnf(2299,plain, % 5.54/5.76 (P22(f28(f30(a29)))+P25(f28(f30(a29)))), % 5.54/5.76 inference(scs_inference,[],[373,2298,39])). % 5.54/5.76 cnf(2300,plain, % 5.54/5.76 (P25(f28(f30(a29)))+P24(f28(f30(a29)))), % 5.54/5.76 inference(scs_inference,[],[2299,2193])). % 5.54/5.76 cnf(2301,plain, % 5.54/5.76 (P24(f28(f30(a29)))+~P32(f28(f30(a29)))), % 5.54/5.76 inference(scs_inference,[],[373,2300,93])). % 5.54/5.76 cnf(2302,plain, % 5.54/5.76 (~P32(f28(f30(a29)))+~P5(f28(f30(a29)))), % 5.54/5.76 inference(scs_inference,[],[373,2301,77])). % 5.54/5.76 cnf(2303,plain, % 5.54/5.76 (~P5(f28(f30(a29)))+P31(f28(f30(a29)))), % 5.54/5.76 inference(scs_inference,[],[373,2302,37])). % 5.54/5.76 cnf(2304,plain, % 5.54/5.76 (P31(f28(f30(a29)))+P6(f28(f30(a29)))), % 5.54/5.76 inference(scs_inference,[],[373,2303,23])). % 5.54/5.76 cnf(2305,plain, % 5.54/5.76 (P6(f28(f30(a29)))+~P30(f28(f30(a29)))), % 5.54/5.76 inference(scs_inference,[],[373,2304,91])). % 5.54/5.76 cnf(2306,plain, % 5.54/5.76 (~P30(f28(f30(a29)))+~P7(f28(f30(a29)))), % 5.54/5.76 inference(scs_inference,[],[373,2305,79])). % 5.54/5.76 cnf(2307,plain, % 5.54/5.76 (~P7(f28(f30(a29)))+P29(f28(f30(a29)))), % 5.54/5.76 inference(scs_inference,[],[373,2306,35])). % 5.54/5.76 cnf(2308,plain, % 5.54/5.76 (P29(f28(f30(a29)))+P8(f28(f30(a29)))), % 5.54/5.76 inference(scs_inference,[],[373,2307,25])). % 5.54/5.76 cnf(2309,plain, % 5.54/5.76 (P8(f28(f30(a29)))+~P28(f28(f30(a29)))), % 5.54/5.76 inference(scs_inference,[],[373,2308,89])). % 5.54/5.76 cnf(2310,plain, % 5.54/5.76 (~P28(f28(f30(a29)))+~P9(f28(f30(a29)))), % 5.54/5.77 inference(scs_inference,[],[373,2309,81])). % 5.54/5.77 cnf(2311,plain, % 5.54/5.77 (~P9(f28(f30(a29)))+P27(f28(f30(a29)))), % 5.54/5.77 inference(scs_inference,[],[373,2310,33])). % 5.54/5.77 cnf(2312,plain, % 5.54/5.77 (P27(f28(f30(a29)))+P10(f28(f30(a29)))), % 5.54/5.77 inference(scs_inference,[],[373,2311,27])). % 5.54/5.77 cnf(2313,plain, % 5.54/5.77 (P10(f28(f30(a29)))+~P14(f28(f30(a29)))), % 5.54/5.77 inference(scs_inference,[],[373,2312,87])). % 5.54/5.77 cnf(2314,plain, % 5.54/5.77 (~P14(f28(f30(a29)))+~P11(f28(f30(a29)))), % 5.54/5.77 inference(scs_inference,[],[373,2313,83])). % 5.54/5.77 cnf(2315,plain, % 5.54/5.77 (~P11(f28(f30(a29)))+P13(f28(f30(a29)))), % 5.54/5.77 inference(scs_inference,[],[373,2314,31])). % 5.54/5.77 cnf(2316,plain, % 5.54/5.77 (P13(f28(f30(a29)))+P12(f28(f30(a29)))), % 5.54/5.77 inference(scs_inference,[],[373,2315,29])). % 5.54/5.77 cnf(2336,plain, % 5.54/5.77 (P26(f30(a29),f28(f30(a29)))), % 5.54/5.77 inference(scs_inference,[],[372,8,11])). % 5.54/5.77 cnf(2337,plain, % 5.54/5.77 (P26(a29,f28(f30(a29)))), % 5.54/5.77 inference(scs_inference,[],[372,2336,151])). % 5.54/5.77 cnf(2341,plain, % 5.54/5.77 (P4(f28(f30(a29)))+~P25(f28(f30(a29)))), % 5.54/5.77 inference(scs_inference,[],[372,152,2336,151,8,150])). % 5.54/5.77 cnf(2363,plain, % 5.54/5.77 (P4(f28(f30(a29)))+~P27(f28(f30(a29)))), % 5.54/5.77 inference(scs_inference,[],[372,152,373,2336,151,8,150,149,2264,2268,2276,2280,2288,2292,2300,2304,2308,2316,31,35,37,39,81,87])). % 5.54/5.77 cnf(2415,plain, % 5.54/5.77 (~P4(f28(f30(a29)))), % 5.54/5.77 inference(scs_inference,[],[4,152,373,2337,2336,151,149,94])). % 5.54/5.77 cnf(2469,plain, % 5.54/5.77 (~P25(f28(f30(a29)))), % 5.54/5.77 inference(scs_inference,[],[2415,2341])). % 5.54/5.77 cnf(2484,plain, % 5.54/5.77 (~P27(f28(f30(a29)))), % 5.54/5.77 inference(scs_inference,[],[2415,2363])). % 5.54/5.77 cnf(2568,plain, % 5.54/5.77 ($false), % 5.54/5.77 inference(scs_inference,[],[373,2469,2484,2415,33,39]), % 5.54/5.77 ['proof']). % 5.54/5.77 % SZS output end Proof % 5.54/5.77 % Total time :5.199230s %------------------------------------------------------------------------------