%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : LCL686+1.015 : 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 : n017.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 25.35s 25.56s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : LCL686+1.015 : 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 : n017.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 : Fri Sep 4 19:11:06 UTC 2026 % 0.08/0.35 % CPUTime : % 0.22/0.51 start to proof:theBenchmark % 25.35/25.52 %------------------------------------------- % 25.35/25.52 % File :CSE---1.7 % 25.35/25.52 % Problem :theBenchmark % 25.35/25.52 % Transform :cnf % 25.35/25.52 % Format :tptp:raw % 25.35/25.52 % Command :java -jar mcs_scs.jar %d %s % 25.35/25.52 % 25.35/25.52 % Result :Theorem 24.973443s % 25.35/25.52 % Output :CNFRefutation 24.973443s % 25.35/25.52 %------------------------------------------- % 25.35/25.53 %------------------------------------------------------------------------------ % 25.35/25.53 % File : LCL686+1.015 : TPTP v9.3.1. Released v4.0.0. % 25.35/25.53 % Domain : Logic Calculi (Modal Logic) % 25.35/25.53 % Problem : In S4, formula provable in S5 embedding, size 15 % 25.35/25.53 % Version : Especial. % 25.35/25.53 % English : % 25.35/25.53 % 25.35/25.53 % Refs : [BHS00] Balsiger et al. (2000), A Benchmark Method for the Pro % 25.35/25.53 % : [Kam08] Kaminski (2008), Email to G. Sutcliffe % 25.35/25.53 % Source : [Kam08] % 25.35/25.53 % Names : s4_s5_p [BHS00] % 25.35/25.53 % 25.35/25.53 % Status : Theorem % 25.35/25.53 % Rating : 0.00 v9.1.0, 0.07 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.2.0, 0.09 v6.1.0, 0.16 v6.0.0, 0.25 v5.5.0, 0.17 v5.4.0, 0.22 v5.2.0, 0.14 v5.0.0, 0.15 v4.1.0, 0.17 v4.0.1, 0.21 v4.0.0 % 25.35/25.53 % Syntax : Number of formulae : 3 ( 1 unt; 0 def) % 25.35/25.53 % Number of atoms : 444 ( 0 equ) % 25.35/25.53 % Maximal formula atoms : 440 ( 148 avg) % 25.35/25.53 % Number of connectives : 797 ( 356 ~; 267 |; 173 &) % 25.35/25.53 % ( 0 <=>; 1 =>; 0 <=; 0 <~>) % 25.35/25.53 % Maximal formula depth : 145 ( 51 avg) % 25.35/25.53 % Maximal term depth : 1 ( 1 avg) % 25.35/25.53 % Number of predicates : 47 ( 46 usr; 1 prp; 0-2 aty) % 25.35/25.53 % Number of functors : 0 ( 0 usr; 0 con; --- aty) % 25.35/25.53 % Number of variables : 97 ( 96 !; 1 ?) % 25.35/25.53 % SPC : FOF_THM_RFO_NEQ % 25.35/25.53 % 25.35/25.53 % Comments : A naive relational encoding of the modal logic problem into % 25.35/25.53 % first-order logic. % 25.35/25.53 %------------------------------------------------------------------------------ % 25.35/25.53 fof(reflexivity,axiom, % 25.35/25.53 ! [X] : r1(X,X) ). % 25.35/25.53 % 25.35/25.53 fof(transitivity,axiom, % 25.35/25.53 ! [X,Y,Z] : % 25.35/25.53 ( ( r1(X,Y) % 25.35/25.53 & r1(Y,Z) ) % 25.35/25.53 => r1(X,Z) ) ). % 25.35/25.53 % 25.35/25.53 fof(main,conjecture, % 25.35/25.53 ~ ? [X] : % 25.35/25.53 ~ ( ! [Y] : % 25.35/25.53 ( ~ r1(X,Y) % 25.35/25.53 | ~ p45(Y) % 25.35/25.53 | ! [X] : % 25.35/25.53 ( ~ r1(Y,X) % 25.35/25.53 | ~ p1(X) ) ) % 25.35/25.53 | ! [Y] : % 25.35/25.53 ( ~ r1(X,Y) % 25.35/25.53 | ~ ! [X] : % 25.35/25.53 ( ~ r1(Y,X) % 25.35/25.53 | ~ ( ! [Y] : % 25.35/25.53 ( ~ r1(X,Y) % 25.35/25.53 | ! [X] : % 25.35/25.53 ( ~ r1(Y,X) % 25.35/25.53 | ! [Y] : % 25.35/25.53 ( ~ r1(X,Y) % 25.35/25.53 | ! [X] : % 25.35/25.53 ( ~ r1(Y,X) % 25.35/25.53 | ! [Y] : % 25.35/25.53 ( ~ r1(X,Y) % 25.35/25.53 | ! [X] : % 25.35/25.53 ( ~ r1(Y,X) % 25.35/25.53 | ! [Y] : % 25.35/25.53 ( ~ r1(X,Y) % 25.35/25.53 | ! [X] : % 25.35/25.53 ( ~ r1(Y,X) % 25.35/25.53 | ! [Y] : % 25.35/25.53 ( ~ r1(X,Y) % 25.35/25.53 | ! [X] : % 25.35/25.53 ( ~ r1(Y,X) % 25.35/25.53 | ! [Y] : % 25.35/25.53 ( ~ r1(X,Y) % 25.35/25.53 | ! [X] : % 25.35/25.53 ( ~ r1(Y,X) % 25.35/25.53 | ! [Y] : % 25.35/25.53 ( ~ r1(X,Y) % 25.35/25.53 | ! [X] : % 25.35/25.53 ( ~ r1(Y,X) % 25.35/25.53 | ! [Y] : % 25.35/25.53 ( ~ r1(X,Y) % 25.35/25.53 | ! [X] : % 25.35/25.53 ( ~ r1(Y,X) % 25.35/25.53 | ! [Y] : % 25.35/25.53 ( ~ r1(X,Y) % 25.35/25.53 | ! [X] : % 25.35/25.53 ( ~ r1(Y,X) % 25.35/25.53 | ! [Y] : % 25.35/25.53 ( ~ r1(X,Y) % 25.35/25.53 | ! [X] : % 25.35/25.53 ( ~ r1(Y,X) % 25.35/25.53 | ! [Y] : % 25.35/25.53 ( ~ r1(X,Y) % 25.35/25.53 | ! [X] : % 25.35/25.53 ( ~ r1(Y,X) % 25.35/25.53 | ! [Y] : % 25.35/25.53 ( ~ r1(X,Y) % 25.35/25.53 | ! [X] : % 25.35/25.53 ( ~ r1(Y,X) % 25.35/25.53 | ! [Y] : % 25.35/25.53 ( ~ r1(X,Y) % 25.35/25.53 | ! [X] : % 25.35/25.53 ( ~ r1(Y,X) % 25.35/25.53 | ! [Y] : % 25.35/25.53 ( ~ r1(X,Y) % 25.35/25.53 | ! [X] : % 25.35/25.53 ( ~ r1(Y,X) % 25.35/25.53 | ! [Y] : % 25.35/25.53 ( ~ r1(X,Y) % 25.35/25.54 | ! [X] : % 25.35/25.54 ( ~ r1(Y,X) % 25.35/25.54 | ! [Y] : % 25.35/25.54 ( ~ r1(X,Y) % 25.35/25.54 | ! [X] : % 25.35/25.54 ( ~ r1(Y,X) % 25.35/25.54 | ! [Y] : % 25.35/25.54 ( ~ r1(X,Y) % 25.35/25.54 | ! [X] : % 25.35/25.54 ( ~ r1(Y,X) % 25.35/25.54 | ! [Y] : % 25.35/25.54 ( ~ r1(X,Y) % 25.35/25.54 | ! [X] : % 25.35/25.54 ( ~ r1(Y,X) % 25.35/25.54 | ! [Y] : % 25.35/25.54 ( ~ r1(X,Y) % 25.35/25.54 | ! [X] : % 25.35/25.54 ( ~ r1(Y,X) % 25.35/25.54 | ! [Y] : % 25.35/25.54 ( ~ r1(X,Y) % 25.35/25.54 | ! [X] : % 25.35/25.54 ( ~ r1(Y,X) % 25.35/25.54 | ! [Y] : % 25.35/25.54 ( ~ r1(X,Y) % 25.35/25.54 | ! [X] : % 25.35/25.54 ( ~ r1(Y,X) % 25.35/25.54 | ! [Y] : % 25.35/25.54 ( ~ r1(X,Y) % 25.35/25.54 | $false ) % 25.35/25.54 | ~ ! [Y] : % 25.35/25.54 ( ~ r1(X,Y) % 25.35/25.54 | ~ ( ( p44(Y) % 25.35/25.54 & ~ p43(Y) ) % 25.35/25.54 | ( ~ p44(Y) % 25.35/25.54 & p43(Y) ) ) ) ) % 25.35/25.54 | ~ ! [X] : % 25.35/25.54 ( ~ r1(Y,X) % 25.35/25.54 | ~ ( ( p43(X) % 25.35/25.54 & ~ p42(X) ) % 25.35/25.54 | ( ~ p43(X) % 25.35/25.54 & p42(X) ) ) ) ) % 25.35/25.54 | ~ ! [Y] : % 25.35/25.54 ( ~ r1(X,Y) % 25.35/25.54 | ~ ( ( p42(Y) % 25.35/25.54 & ~ p41(Y) ) % 25.35/25.54 | ( ~ p42(Y) % 25.35/25.54 & p41(Y) ) ) ) ) % 25.35/25.54 | ~ ! [X] : % 25.35/25.54 ( ~ r1(Y,X) % 25.35/25.54 | ~ ( ( p41(X) % 25.35/25.54 & ~ p40(X) ) % 25.35/25.54 | ( ~ p41(X) % 25.35/25.54 & p40(X) ) ) ) ) % 25.35/25.54 | ~ ! [Y] : % 25.35/25.54 ( ~ r1(X,Y) % 25.35/25.54 | ~ ( ( p40(Y) % 25.35/25.54 & ~ p39(Y) ) % 25.35/25.54 | ( ~ p40(Y) % 25.35/25.54 & p39(Y) ) ) ) ) % 25.35/25.54 | ~ ! [X] : % 25.35/25.54 ( ~ r1(Y,X) % 25.35/25.54 | ~ ( ( p39(X) % 25.35/25.54 & ~ p38(X) ) % 25.35/25.54 | ( ~ p39(X) % 25.35/25.54 & p38(X) ) ) ) ) % 25.35/25.54 | ~ ! [Y] : % 25.35/25.54 ( ~ r1(X,Y) % 25.35/25.54 | ~ ( ( p38(Y) % 25.35/25.54 & ~ p37(Y) ) % 25.35/25.54 | ( ~ p38(Y) % 25.35/25.54 & p37(Y) ) ) ) ) % 25.35/25.54 | ~ ! [X] : % 25.35/25.54 ( ~ r1(Y,X) % 25.35/25.54 | ~ ( ( p37(X) % 25.35/25.54 & ~ p36(X) ) % 25.35/25.54 | ( ~ p37(X) % 25.35/25.54 & p36(X) ) ) ) ) % 25.35/25.54 | ~ ! [Y] : % 25.35/25.54 ( ~ r1(X,Y) % 25.35/25.54 | ~ ( ( p36(Y) % 25.35/25.54 & ~ p35(Y) ) % 25.35/25.54 | ( ~ p36(Y) % 25.35/25.54 & p35(Y) ) ) ) ) % 25.35/25.54 | ~ ! [X] : % 25.35/25.54 ( ~ r1(Y,X) % 25.35/25.54 | ~ ( ( p35(X) % 25.35/25.54 & ~ p34(X) ) % 25.35/25.54 | ( ~ p35(X) % 25.35/25.54 & p34(X) ) ) ) ) % 25.35/25.54 | ~ ! [Y] : % 25.35/25.54 ( ~ r1(X,Y) % 25.35/25.54 | ~ ( ( p34(Y) % 25.35/25.54 & ~ p33(Y) ) % 25.35/25.54 | ( ~ p34(Y) % 25.35/25.54 & p33(Y) ) ) ) ) % 25.35/25.54 | ~ ! [X] : % 25.35/25.54 ( ~ r1(Y,X) % 25.35/25.54 | ~ ( ( p33(X) % 25.35/25.54 & ~ p32(X) ) % 25.35/25.54 | ( ~ p33(X) % 25.35/25.54 & p32(X) ) ) ) ) % 25.35/25.54 | ~ ! [Y] : % 25.35/25.54 ( ~ r1(X,Y) % 25.35/25.54 | ~ ( ( p32(Y) % 25.35/25.54 & ~ p31(Y) ) % 25.35/25.54 | ( ~ p32(Y) % 25.35/25.54 & p31(Y) ) ) ) ) % 25.35/25.54 | ~ ! [X] : % 25.35/25.54 ( ~ r1(Y,X) % 25.35/25.54 | ~ ( ( p31(X) % 25.35/25.54 & ~ p30(X) ) % 25.35/25.54 | ( ~ p31(X) % 25.35/25.54 & p30(X) ) ) ) ) % 25.35/25.54 | ~ ! [Y] : % 25.35/25.54 ( ~ r1(X,Y) % 25.35/25.54 | ~ ( ( p30(Y) % 25.35/25.54 & ~ p29(Y) ) % 25.35/25.54 | ( ~ p30(Y) % 25.35/25.54 & p29(Y) ) ) ) ) % 25.35/25.54 | ~ ! [X] : % 25.35/25.54 ( ~ r1(Y,X) % 25.35/25.54 | ~ ( ( p29(X) % 25.35/25.54 & ~ p28(X) ) % 25.35/25.54 | ( ~ p29(X) % 25.35/25.54 & p28(X) ) ) ) ) % 25.35/25.54 | ~ ! [Y] : % 25.35/25.54 ( ~ r1(X,Y) % 25.35/25.54 | ~ ( ( p28(Y) % 25.35/25.54 & ~ p27(Y) ) % 25.35/25.54 | ( ~ p28(Y) % 25.35/25.54 & p27(Y) ) ) ) ) % 25.35/25.54 | ~ ! [X] : % 25.35/25.54 ( ~ r1(Y,X) % 25.35/25.54 | ~ ( ( p27(X) % 25.35/25.54 & ~ p26(X) ) % 25.35/25.54 | ( ~ p27(X) % 25.35/25.54 & p26(X) ) ) ) ) % 25.35/25.54 | ~ ! [Y] : % 25.35/25.54 ( ~ r1(X,Y) % 25.35/25.54 | ~ ( ( p26(Y) % 25.35/25.54 & ~ p25(Y) ) % 25.35/25.54 | ( ~ p26(Y) % 25.35/25.54 & p25(Y) ) ) ) ) % 25.35/25.54 | ~ ! [X] : % 25.35/25.54 ( ~ r1(Y,X) % 25.35/25.54 | ~ ( ( p25(X) % 25.35/25.54 & ~ p24(X) ) % 25.35/25.54 | ( ~ p25(X) % 25.35/25.54 & p24(X) ) ) ) ) % 25.35/25.54 | ~ ! [Y] : % 25.35/25.54 ( ~ r1(X,Y) % 25.35/25.54 | ~ ( ( p24(Y) % 25.35/25.54 & ~ p23(Y) ) % 25.35/25.54 | ( ~ p24(Y) % 25.35/25.54 & p23(Y) ) ) ) ) % 25.35/25.54 | ~ ! [X] : % 25.35/25.54 ( ~ r1(Y,X) % 25.35/25.54 | ~ ( ( p23(X) % 25.35/25.54 & ~ p22(X) ) % 25.35/25.54 | ( ~ p23(X) % 25.35/25.54 & p22(X) ) ) ) ) % 25.35/25.54 | ~ ! [Y] : % 25.35/25.54 ( ~ r1(X,Y) % 25.35/25.54 | ~ ( ( p22(Y) % 25.35/25.54 & ~ p21(Y) ) % 25.35/25.54 | ( ~ p22(Y) % 25.35/25.54 & p21(Y) ) ) ) ) % 25.35/25.54 | ~ ! [X] : % 25.35/25.54 ( ~ r1(Y,X) % 25.35/25.54 | ~ ( ( p21(X) % 25.35/25.54 & ~ p20(X) ) % 25.35/25.54 | ( ~ p21(X) % 25.35/25.54 & p20(X) ) ) ) ) % 25.35/25.54 | ~ ! [Y] : % 25.35/25.54 ( ~ r1(X,Y) % 25.35/25.54 | ~ ( ( p20(Y) % 25.35/25.54 & ~ p19(Y) ) % 25.35/25.54 | ( ~ p20(Y) % 25.35/25.54 & p19(Y) ) ) ) ) % 25.35/25.54 | ~ ! [X] : % 25.35/25.54 ( ~ r1(Y,X) % 25.35/25.55 | ~ ( ( p19(X) % 25.35/25.55 & ~ p18(X) ) % 25.35/25.55 | ( ~ p19(X) % 25.35/25.55 & p18(X) ) ) ) ) % 25.35/25.55 | ~ ! [Y] : % 25.35/25.55 ( ~ r1(X,Y) % 25.35/25.55 | ~ ( ( p18(Y) % 25.35/25.55 & ~ p17(Y) ) % 25.35/25.55 | ( ~ p18(Y) % 25.35/25.55 & p17(Y) ) ) ) ) % 25.35/25.55 | ~ ! [X] : % 25.35/25.55 ( ~ r1(Y,X) % 25.35/25.55 | ~ ( ( p17(X) % 25.35/25.55 & ~ p16(X) ) % 25.35/25.55 | ( ~ p17(X) % 25.35/25.55 & p16(X) ) ) ) ) % 25.35/25.55 | ~ ! [Y] : % 25.35/25.55 ( ~ r1(X,Y) % 25.35/25.55 | ~ ( ( p16(Y) % 25.35/25.55 & ~ p15(Y) ) % 25.35/25.55 | ( ~ p16(Y) % 25.35/25.55 & p15(Y) ) ) ) ) % 25.35/25.55 | ~ ! [X] : % 25.35/25.55 ( ~ r1(Y,X) % 25.35/25.55 | ~ ( ( p15(X) % 25.35/25.55 & ~ p14(X) ) % 25.35/25.55 | ( ~ p15(X) % 25.35/25.55 & p14(X) ) ) ) ) % 25.35/25.55 | ~ ! [Y] : % 25.35/25.55 ( ~ r1(X,Y) % 25.35/25.55 | ~ ( ( p14(Y) % 25.35/25.55 & ~ p13(Y) ) % 25.35/25.55 | ( ~ p14(Y) % 25.35/25.55 & p13(Y) ) ) ) ) % 25.35/25.55 | ~ ! [X] : % 25.35/25.55 ( ~ r1(Y,X) % 25.35/25.55 | ~ ( ( p13(X) % 25.35/25.55 & ~ p12(X) ) % 25.35/25.55 | ( ~ p13(X) % 25.35/25.55 & p12(X) ) ) ) ) % 25.35/25.55 | ~ ! [Y] : % 25.35/25.55 ( ~ r1(X,Y) % 25.35/25.55 | ~ ( ( p12(Y) % 25.35/25.55 & ~ p11(Y) ) % 25.35/25.55 | ( ~ p12(Y) % 25.35/25.55 & p11(Y) ) ) ) ) % 25.35/25.55 | ~ ! [X] : % 25.35/25.55 ( ~ r1(Y,X) % 25.35/25.55 | ~ ( ( p11(X) % 25.35/25.55 & ~ p10(X) ) % 25.35/25.55 | ( ~ p11(X) % 25.35/25.55 & p10(X) ) ) ) ) % 25.35/25.55 | ~ ! [Y] : % 25.35/25.55 ( ~ r1(X,Y) % 25.35/25.55 | ~ ( ( p10(Y) % 25.35/25.55 & ~ p9(Y) ) % 25.35/25.55 | ( ~ p10(Y) % 25.35/25.55 & p9(Y) ) ) ) ) % 25.35/25.55 | ~ ! [X] : % 25.35/25.55 ( ~ r1(Y,X) % 25.35/25.55 | ~ ( ( p9(X) % 25.35/25.55 & ~ p8(X) ) % 25.35/25.55 | ( ~ p9(X) % 25.35/25.55 & p8(X) ) ) ) ) % 25.35/25.55 | ~ ! [Y] : % 25.35/25.55 ( ~ r1(X,Y) % 25.35/25.55 | ~ ( ( p8(Y) % 25.35/25.55 & ~ p7(Y) ) % 25.35/25.55 | ( ~ p8(Y) % 25.35/25.55 & p7(Y) ) ) ) ) % 25.35/25.55 | ~ ! [X] : % 25.35/25.55 ( ~ r1(Y,X) % 25.35/25.55 | ~ ( ( p7(X) % 25.35/25.55 & ~ p6(X) ) % 25.35/25.55 | ( ~ p7(X) % 25.35/25.55 & p6(X) ) ) ) ) % 25.35/25.55 | ~ ! [Y] : % 25.35/25.55 ( ~ r1(X,Y) % 25.35/25.55 | ~ ( ( p6(Y) % 25.35/25.55 & ~ p5(Y) ) % 25.35/25.55 | ( ~ p6(Y) % 25.35/25.55 & p5(Y) ) ) ) ) % 25.35/25.55 | ~ ! [X] : % 25.35/25.55 ( ~ r1(Y,X) % 25.35/25.55 | ~ ( ( p5(X) % 25.35/25.55 & ~ p4(X) ) % 25.35/25.55 | ( ~ p5(X) % 25.35/25.55 & p4(X) ) ) ) ) % 25.35/25.55 | ~ ! [Y] : % 25.35/25.55 ( ~ r1(X,Y) % 25.35/25.55 | ~ ( ( p4(Y) % 25.35/25.55 & ~ p3(Y) ) % 25.35/25.55 | ( ~ p4(Y) % 25.35/25.55 & p3(Y) ) ) ) ) % 25.35/25.55 | ~ ! [X] : % 25.35/25.55 ( ~ r1(Y,X) % 25.35/25.55 | ~ ( ( p3(X) % 25.35/25.55 & ~ p2(X) ) % 25.35/25.55 | ( ~ p3(X) % 25.35/25.55 & p2(X) ) ) ) ) % 25.35/25.55 | ~ ! [Y] : % 25.35/25.55 ( ~ r1(X,Y) % 25.35/25.55 | ~ ( ( p2(Y) % 25.35/25.55 & ~ p1(Y) ) % 25.35/25.55 | ( ~ p2(Y) % 25.35/25.55 & p1(Y) ) ) ) % 25.35/25.55 | ! [Y] : % 25.35/25.55 ( ~ r1(X,Y) % 25.35/25.55 | p45(Y) ) % 25.35/25.55 | ! [Y] : % 25.35/25.55 ( ~ r1(X,Y) % 25.35/25.55 | ( ~ p43(Y) % 25.35/25.55 & ~ p44(Y) ) % 25.35/25.55 | ( p44(Y) % 25.35/25.55 & p43(Y) ) % 25.35/25.55 | ( ~ p42(Y) % 25.35/25.55 & ~ p43(Y) ) % 25.35/25.55 | ( p43(Y) % 25.35/25.55 & p42(Y) ) % 25.35/25.55 | ( ~ p41(Y) % 25.35/25.55 & ~ p42(Y) ) % 25.35/25.55 | ( p42(Y) % 25.35/25.55 & p41(Y) ) % 25.35/25.55 | ( ~ p40(Y) % 25.35/25.55 & ~ p41(Y) ) % 25.35/25.55 | ( p41(Y) % 25.35/25.55 & p40(Y) ) % 25.35/25.55 | ( ~ p39(Y) % 25.35/25.55 & ~ p40(Y) ) % 25.35/25.55 | ( p40(Y) % 25.35/25.55 & p39(Y) ) % 25.35/25.55 | ( ~ p38(Y) % 25.35/25.55 & ~ p39(Y) ) % 25.35/25.55 | ( p39(Y) % 25.35/25.55 & p38(Y) ) % 25.35/25.55 | ( ~ p37(Y) % 25.35/25.55 & ~ p38(Y) ) % 25.35/25.55 | ( p38(Y) % 25.35/25.55 & p37(Y) ) % 25.35/25.55 | ( ~ p36(Y) % 25.35/25.55 & ~ p37(Y) ) % 25.35/25.55 | ( p37(Y) % 25.35/25.55 & p36(Y) ) % 25.35/25.55 | ( ~ p35(Y) % 25.35/25.55 & ~ p36(Y) ) % 25.35/25.55 | ( p36(Y) % 25.35/25.55 & p35(Y) ) % 25.35/25.55 | ( ~ p34(Y) % 25.35/25.55 & ~ p35(Y) ) % 25.35/25.55 | ( p35(Y) % 25.35/25.55 & p34(Y) ) % 25.35/25.55 | ( ~ p33(Y) % 25.35/25.55 & ~ p34(Y) ) % 25.35/25.55 | ( p34(Y) % 25.35/25.55 & p33(Y) ) % 25.35/25.55 | ( ~ p32(Y) % 25.35/25.55 & ~ p33(Y) ) % 25.35/25.55 | ( p33(Y) % 25.35/25.55 & p32(Y) ) % 25.35/25.55 | ( ~ p31(Y) % 25.35/25.55 & ~ p32(Y) ) % 25.35/25.55 | ( p32(Y) % 25.35/25.55 & p31(Y) ) % 25.35/25.55 | ( ~ p30(Y) % 25.35/25.55 & ~ p31(Y) ) % 25.35/25.55 | ( p31(Y) % 25.35/25.55 & p30(Y) ) % 25.35/25.55 | ( ~ p29(Y) % 25.35/25.55 & ~ p30(Y) ) % 25.35/25.55 | ( p30(Y) % 25.35/25.55 & p29(Y) ) % 25.35/25.55 | ( ~ p28(Y) % 25.35/25.55 & ~ p29(Y) ) % 25.35/25.55 | ( p29(Y) % 25.35/25.55 & p28(Y) ) % 25.35/25.55 | ( ~ p27(Y) % 25.35/25.55 & ~ p28(Y) ) % 25.35/25.55 | ( p28(Y) % 25.35/25.55 & p27(Y) ) % 25.35/25.55 | ( ~ p26(Y) % 25.35/25.55 & ~ p27(Y) ) % 25.35/25.55 | ( p27(Y) % 25.35/25.55 & p26(Y) ) % 25.35/25.55 | ( ~ p25(Y) % 25.35/25.55 & ~ p26(Y) ) % 25.35/25.55 | ( p26(Y) % 25.35/25.55 & p25(Y) ) % 25.35/25.55 | ( ~ p24(Y) % 25.35/25.55 & ~ p25(Y) ) % 25.35/25.55 | ( p25(Y) % 25.35/25.55 & p24(Y) ) % 25.35/25.55 | ( ~ p23(Y) % 25.35/25.55 & ~ p24(Y) ) % 25.35/25.55 | ( p24(Y) % 25.35/25.55 & p23(Y) ) % 25.35/25.55 | ( ~ p22(Y) % 25.35/25.55 & ~ p23(Y) ) % 25.35/25.55 | ( p23(Y) % 25.35/25.55 & p22(Y) ) % 25.35/25.55 | ( ~ p21(Y) % 25.35/25.55 & ~ p22(Y) ) % 25.35/25.55 | ( p22(Y) % 25.35/25.55 & p21(Y) ) % 25.35/25.55 | ( ~ p20(Y) % 25.35/25.55 & ~ p21(Y) ) % 25.35/25.55 | ( p21(Y) % 25.35/25.55 & p20(Y) ) % 25.35/25.55 | ( ~ p19(Y) % 25.35/25.55 & ~ p20(Y) ) % 25.35/25.55 | ( p20(Y) % 25.35/25.55 & p19(Y) ) % 25.35/25.55 | ( ~ p18(Y) % 25.35/25.55 & ~ p19(Y) ) % 25.35/25.55 | ( p19(Y) % 25.35/25.55 & p18(Y) ) % 25.35/25.55 | ( ~ p17(Y) % 25.35/25.55 & ~ p18(Y) ) % 25.35/25.55 | ( p18(Y) % 25.35/25.55 & p17(Y) ) % 25.35/25.55 | ( ~ p16(Y) % 25.35/25.55 & ~ p17(Y) ) % 25.35/25.55 | ( p17(Y) % 25.35/25.55 & p16(Y) ) % 25.35/25.55 | ( ~ p15(Y) % 25.35/25.55 & ~ p16(Y) ) % 25.35/25.55 | ( p16(Y) % 25.35/25.55 & p15(Y) ) % 25.35/25.55 | ( ~ p14(Y) % 25.35/25.55 & ~ p15(Y) ) % 25.35/25.55 | ( p15(Y) % 25.35/25.55 & p14(Y) ) % 25.35/25.55 | ( ~ p13(Y) % 25.35/25.55 & ~ p14(Y) ) % 25.35/25.55 | ( p14(Y) % 25.35/25.55 & p13(Y) ) % 25.35/25.55 | ( ~ p12(Y) % 25.35/25.55 & ~ p13(Y) ) % 25.35/25.55 | ( p13(Y) % 25.35/25.55 & p12(Y) ) % 25.35/25.55 | ( ~ p11(Y) % 25.35/25.55 & ~ p12(Y) ) % 25.35/25.55 | ( p12(Y) % 25.35/25.55 & p11(Y) ) % 25.35/25.55 | ( ~ p10(Y) % 25.35/25.55 & ~ p11(Y) ) % 25.35/25.55 | ( p11(Y) % 25.35/25.55 & p10(Y) ) % 25.35/25.55 | ( ~ p9(Y) % 25.35/25.55 & ~ p10(Y) ) % 25.35/25.55 | ( p10(Y) % 25.35/25.55 & p9(Y) ) % 25.35/25.55 | ( ~ p8(Y) % 25.35/25.55 & ~ p9(Y) ) % 25.35/25.55 | ( p9(Y) % 25.35/25.55 & p8(Y) ) % 25.35/25.55 | ( ~ p7(Y) % 25.35/25.55 & ~ p8(Y) ) % 25.35/25.55 | ( p8(Y) % 25.35/25.55 & p7(Y) ) % 25.35/25.55 | ( ~ p6(Y) % 25.35/25.55 & ~ p7(Y) ) % 25.35/25.55 | ( p7(Y) % 25.35/25.55 & p6(Y) ) % 25.35/25.55 | ( ~ p5(Y) % 25.35/25.55 & ~ p6(Y) ) % 25.35/25.55 | ( p6(Y) % 25.35/25.55 & p5(Y) ) % 25.35/25.55 | ( ~ p4(Y) % 25.35/25.55 & ~ p5(Y) ) % 25.35/25.55 | ( p5(Y) % 25.35/25.55 & p4(Y) ) % 25.35/25.55 | ( ~ p3(Y) % 25.35/25.55 & ~ p4(Y) ) % 25.35/25.55 | ( p4(Y) % 25.35/25.55 & p3(Y) ) % 25.35/25.56 | ( ~ p2(Y) % 25.35/25.56 & ~ p3(Y) ) % 25.35/25.56 | ( p3(Y) % 25.35/25.56 & p2(Y) ) % 25.35/25.56 | ( ~ p1(Y) % 25.35/25.56 & ~ p2(Y) ) % 25.35/25.56 | ( p2(Y) % 25.35/25.56 & p1(Y) ) ) ) ) ) ) ). % 25.35/25.56 % 25.35/25.56 %------------------------------------------------------------------------------ % 25.35/25.56 %------------------------------------------- % 25.35/25.56 % Proof found % 25.35/25.56 % SZS status Theorem for theBenchmark % 25.35/25.56 % SZS output start Proof % 25.35/25.56 %ClaNum:226(EqnAxiom:0) % 25.35/25.56 %VarNum:835(SingletonVarNum:309) % 25.35/25.56 %MaxLitNum:4 % 25.35/25.56 %MaxfuncDepth:1 % 25.35/25.56 %SharedTerms:9 % 25.35/25.56 %goalClause: 1 2 3 4 5 8 % 25.35/25.56 %singleGoalClaCount:5 % 25.35/25.56 [1]P1(a1) % 25.35/25.56 [2]P2(a23) % 25.35/25.56 [3]P42(a2,a1) % 25.35/25.56 [4]P42(a2,a34) % 25.35/25.56 [5]P42(a1,a23) % 25.35/25.56 [6]P42(x61,x61) % 25.35/25.56 [8]P3(x81)+~P42(a34,x81) % 25.35/25.56 [7]~P3(x71)+~P1(f35(x71)) % 25.35/25.56 [9]~P3(x91)+P42(x91,f45(x91)) % 25.35/25.56 [10]~P3(x101)+P42(x101,f35(x101)) % 25.35/25.56 [11]~P3(x111)+P42(x111,f44(x111)) % 25.35/25.56 [55]~P3(x551)+P42(f45(x551),f46(x551)) % 25.35/25.56 [56]~P3(x561)+P42(f46(x561),f47(x561)) % 25.35/25.56 [57]~P3(x571)+P42(f47(x571),f48(x571)) % 25.35/25.56 [58]~P3(x581)+P42(f48(x581),f49(x581)) % 25.35/25.56 [59]~P3(x591)+P42(f49(x591),f3(x591)) % 25.35/25.56 [60]~P3(x601)+P42(f3(x601),f4(x601)) % 25.35/25.56 [61]~P3(x611)+P42(f4(x611),f5(x611)) % 25.35/25.56 [62]~P3(x621)+P42(f5(x621),f6(x621)) % 25.35/25.56 [63]~P3(x631)+P42(f6(x631),f7(x631)) % 25.35/25.56 [64]~P3(x641)+P42(f7(x641),f8(x641)) % 25.35/25.56 [65]~P3(x651)+P42(f8(x651),f9(x651)) % 25.35/25.56 [66]~P3(x661)+P42(f9(x661),f10(x661)) % 25.35/25.56 [67]~P3(x671)+P42(f10(x671),f11(x671)) % 25.35/25.56 [68]~P3(x681)+P42(f11(x681),f12(x681)) % 25.35/25.56 [69]~P3(x691)+P42(f12(x691),f13(x691)) % 25.35/25.56 [70]~P3(x701)+P42(f13(x701),f14(x701)) % 25.35/25.56 [71]~P3(x711)+P42(f14(x711),f15(x711)) % 25.35/25.56 [72]~P3(x721)+P42(f15(x721),f16(x721)) % 25.35/25.56 [73]~P3(x731)+P42(f16(x731),f17(x731)) % 25.35/25.56 [74]~P3(x741)+P42(f17(x741),f18(x741)) % 25.35/25.56 [75]~P3(x751)+P42(f18(x751),f19(x751)) % 25.35/25.56 [76]~P3(x761)+P42(f19(x761),f20(x761)) % 25.35/25.56 [77]~P3(x771)+P42(f20(x771),f21(x771)) % 25.35/25.56 [78]~P3(x781)+P42(f21(x781),f22(x781)) % 25.35/25.56 [79]~P3(x791)+P42(f22(x791),f24(x791)) % 25.35/25.56 [80]~P3(x801)+P42(f24(x801),f25(x801)) % 25.35/25.56 [81]~P3(x811)+P42(f25(x811),f26(x811)) % 25.35/25.56 [82]~P3(x821)+P42(f26(x821),f27(x821)) % 25.35/25.56 [83]~P3(x831)+P42(f27(x831),f28(x831)) % 25.35/25.56 [84]~P3(x841)+P42(f28(x841),f29(x841)) % 25.35/25.56 [85]~P3(x851)+P42(f29(x851),f30(x851)) % 25.35/25.56 [86]~P3(x861)+P42(f30(x861),f31(x861)) % 25.35/25.56 [87]~P3(x871)+P42(f31(x871),f32(x871)) % 25.35/25.56 [88]~P3(x881)+P42(f32(x881),f33(x881)) % 25.35/25.56 [89]~P3(x891)+P42(f33(x891),f36(x891)) % 25.35/25.56 [90]~P3(x901)+P42(f36(x901),f37(x901)) % 25.35/25.56 [91]~P3(x911)+P42(f37(x911),f38(x911)) % 25.35/25.56 [92]~P3(x921)+P42(f38(x921),f39(x921)) % 25.35/25.56 [93]~P3(x931)+P42(f39(x931),f40(x931)) % 25.35/25.56 [94]~P3(x941)+P42(f40(x941),f41(x941)) % 25.35/25.56 [95]~P3(x951)+P42(f41(x951),f42(x951)) % 25.35/25.56 [96]~P3(x961)+P42(f42(x961),f43(x961)) % 25.35/25.56 [12]~P3(x121)+P2(f44(x121))+P4(f44(x121)) % 25.35/25.56 [13]~P3(x131)+P15(f44(x131))+P16(f44(x131)) % 25.35/25.56 [14]~P3(x141)+P16(f44(x141))+P17(f44(x141)) % 25.35/25.56 [15]~P3(x151)+P17(f44(x151))+P18(f44(x151)) % 25.35/25.56 [16]~P3(x161)+P18(f44(x161))+P19(f44(x161)) % 25.35/25.56 [17]~P3(x171)+P19(f44(x171))+P20(f44(x171)) % 25.35/25.56 [18]~P3(x181)+P20(f44(x181))+P21(f44(x181)) % 25.35/25.56 [19]~P3(x191)+P21(f44(x191))+P22(f44(x191)) % 25.35/25.56 [20]~P3(x201)+P22(f44(x201))+P23(f44(x201)) % 25.35/25.56 [21]~P3(x211)+P23(f44(x211))+P24(f44(x211)) % 25.35/25.56 [22]~P3(x221)+P24(f44(x221))+P25(f44(x221)) % 25.35/25.56 [23]~P3(x231)+P25(f44(x231))+P26(f44(x231)) % 25.35/25.56 [24]~P3(x241)+P26(f44(x241))+P27(f44(x241)) % 25.35/25.56 [25]~P3(x251)+P27(f44(x251))+P28(f44(x251)) % 25.35/25.56 [26]~P3(x261)+P28(f44(x261))+P29(f44(x261)) % 25.35/25.56 [27]~P3(x271)+P29(f44(x271))+P30(f44(x271)) % 25.35/25.56 [28]~P3(x281)+P30(f44(x281))+P31(f44(x281)) % 25.35/25.56 [29]~P3(x291)+P31(f44(x291))+P32(f44(x291)) % 25.35/25.56 [30]~P3(x301)+P32(f44(x301))+P33(f44(x301)) % 25.35/25.56 [31]~P3(x311)+P33(f44(x311))+P34(f44(x311)) % 25.35/25.56 [32]~P3(x321)+P34(f44(x321))+P35(f44(x321)) % 25.35/25.56 [33]~P3(x331)+P35(f44(x331))+P36(f44(x331)) % 25.35/25.56 [34]~P3(x341)+P36(f44(x341))+P37(f44(x341)) % 25.35/25.56 [35]~P3(x351)+P37(f44(x351))+P38(f44(x351)) % 25.35/25.56 [36]~P3(x361)+P38(f44(x361))+P39(f44(x361)) % 25.35/25.56 [37]~P3(x371)+P39(f44(x371))+P5(f44(x371)) % 25.35/25.56 [38]~P3(x381)+P5(f44(x381))+P6(f44(x381)) % 25.35/25.56 [39]~P3(x391)+P6(f44(x391))+P7(f44(x391)) % 25.35/25.56 [40]~P3(x401)+P7(f44(x401))+P8(f44(x401)) % 25.35/25.56 [41]~P3(x411)+P8(f44(x411))+P9(f44(x411)) % 25.35/25.56 [42]~P3(x421)+P9(f44(x421))+P10(f44(x421)) % 25.35/25.56 [43]~P3(x431)+P10(f44(x431))+P11(f44(x431)) % 25.35/25.56 [44]~P3(x441)+P11(f44(x441))+P12(f44(x441)) % 25.35/25.56 [45]~P3(x451)+P12(f44(x451))+P13(f44(x451)) % 25.35/25.56 [46]~P3(x461)+P13(f44(x461))+P14(f44(x461)) % 25.35/25.56 [47]~P3(x471)+P14(f44(x471))+P43(f44(x471)) % 25.35/25.56 [48]~P3(x481)+P43(f44(x481))+P44(f44(x481)) % 25.35/25.56 [49]~P3(x491)+P44(f44(x491))+P45(f44(x491)) % 25.35/25.56 [50]~P3(x501)+P45(f44(x501))+P46(f44(x501)) % 25.35/25.56 [51]~P3(x511)+P46(f44(x511))+P47(f44(x511)) % 25.35/25.56 [52]~P3(x521)+P47(f44(x521))+P41(f44(x521)) % 25.35/25.56 [53]~P3(x531)+P41(f44(x531))+P40(f44(x531)) % 25.35/25.56 [54]~P3(x541)+P40(f44(x541))+P4(f44(x541)) % 25.35/25.56 [97]~P3(x971)+~P2(f44(x971))+~P4(f44(x971)) % 25.35/25.56 [98]~P3(x981)+~P15(f44(x981))+~P16(f44(x981)) % 25.35/25.56 [99]~P3(x991)+~P16(f44(x991))+~P17(f44(x991)) % 25.35/25.56 [100]~P3(x1001)+~P17(f44(x1001))+~P18(f44(x1001)) % 25.35/25.56 [101]~P3(x1011)+~P18(f44(x1011))+~P19(f44(x1011)) % 25.35/25.56 [102]~P3(x1021)+~P19(f44(x1021))+~P20(f44(x1021)) % 25.35/25.56 [103]~P3(x1031)+~P20(f44(x1031))+~P21(f44(x1031)) % 25.35/25.56 [104]~P3(x1041)+~P21(f44(x1041))+~P22(f44(x1041)) % 25.35/25.56 [105]~P3(x1051)+~P22(f44(x1051))+~P23(f44(x1051)) % 25.35/25.56 [106]~P3(x1061)+~P23(f44(x1061))+~P24(f44(x1061)) % 25.35/25.56 [107]~P3(x1071)+~P24(f44(x1071))+~P25(f44(x1071)) % 25.35/25.56 [108]~P3(x1081)+~P25(f44(x1081))+~P26(f44(x1081)) % 25.35/25.56 [109]~P3(x1091)+~P26(f44(x1091))+~P27(f44(x1091)) % 25.35/25.56 [110]~P3(x1101)+~P27(f44(x1101))+~P28(f44(x1101)) % 25.35/25.56 [111]~P3(x1111)+~P28(f44(x1111))+~P29(f44(x1111)) % 25.35/25.56 [112]~P3(x1121)+~P29(f44(x1121))+~P30(f44(x1121)) % 25.35/25.56 [113]~P3(x1131)+~P30(f44(x1131))+~P31(f44(x1131)) % 25.35/25.56 [114]~P3(x1141)+~P31(f44(x1141))+~P32(f44(x1141)) % 25.35/25.56 [115]~P3(x1151)+~P32(f44(x1151))+~P33(f44(x1151)) % 25.35/25.56 [116]~P3(x1161)+~P33(f44(x1161))+~P34(f44(x1161)) % 25.35/25.56 [117]~P3(x1171)+~P34(f44(x1171))+~P35(f44(x1171)) % 25.35/25.56 [118]~P3(x1181)+~P35(f44(x1181))+~P36(f44(x1181)) % 25.35/25.56 [119]~P3(x1191)+~P36(f44(x1191))+~P37(f44(x1191)) % 25.35/25.56 [120]~P3(x1201)+~P37(f44(x1201))+~P38(f44(x1201)) % 25.35/25.56 [121]~P3(x1211)+~P38(f44(x1211))+~P39(f44(x1211)) % 25.35/25.56 [122]~P3(x1221)+~P39(f44(x1221))+~P5(f44(x1221)) % 25.35/25.56 [123]~P3(x1231)+~P5(f44(x1231))+~P6(f44(x1231)) % 25.35/25.56 [124]~P3(x1241)+~P6(f44(x1241))+~P7(f44(x1241)) % 25.35/25.56 [125]~P3(x1251)+~P7(f44(x1251))+~P8(f44(x1251)) % 25.35/25.56 [126]~P3(x1261)+~P8(f44(x1261))+~P9(f44(x1261)) % 25.35/25.56 [127]~P3(x1271)+~P9(f44(x1271))+~P10(f44(x1271)) % 25.35/25.56 [128]~P3(x1281)+~P10(f44(x1281))+~P11(f44(x1281)) % 25.35/25.56 [129]~P3(x1291)+~P11(f44(x1291))+~P12(f44(x1291)) % 25.35/25.56 [130]~P3(x1301)+~P12(f44(x1301))+~P13(f44(x1301)) % 25.35/25.56 [131]~P3(x1311)+~P13(f44(x1311))+~P14(f44(x1311)) % 25.35/25.56 [132]~P3(x1321)+~P14(f44(x1321))+~P43(f44(x1321)) % 25.35/25.56 [133]~P3(x1331)+~P43(f44(x1331))+~P44(f44(x1331)) % 25.35/25.56 [134]~P3(x1341)+~P44(f44(x1341))+~P45(f44(x1341)) % 25.35/25.56 [135]~P3(x1351)+~P45(f44(x1351))+~P46(f44(x1351)) % 25.35/25.56 [136]~P3(x1361)+~P46(f44(x1361))+~P47(f44(x1361)) % 25.35/25.56 [137]~P3(x1371)+~P47(f44(x1371))+~P41(f44(x1371)) % 25.35/25.56 [138]~P3(x1381)+~P41(f44(x1381))+~P40(f44(x1381)) % 25.35/25.56 [139]~P3(x1391)+~P40(f44(x1391))+~P4(f44(x1391)) % 25.35/25.56 [226]~P42(x2261,x2263)+P42(x2261,x2262)+~P42(x2263,x2262) % 25.35/25.56 [140]~P4(x1401)+~P42(x1402,x1401)+P2(x1401)+~P3(x1402) % 25.35/25.56 [141]~P2(x1411)+~P42(x1412,x1411)+P4(x1411)+~P3(x1412) % 25.35/25.56 [142]~P16(x1421)+P15(x1421)+~P3(x1422)+~P42(f42(x1422),x1421) % 25.35/25.56 [143]~P15(x1431)+P16(x1431)+~P3(x1432)+~P42(f42(x1432),x1431) % 25.35/25.56 [144]~P17(x1441)+P16(x1441)+~P3(x1442)+~P42(f41(x1442),x1441) % 25.35/25.56 [145]~P16(x1451)+P17(x1451)+~P3(x1452)+~P42(f41(x1452),x1451) % 25.35/25.56 [146]~P18(x1461)+P17(x1461)+~P3(x1462)+~P42(f40(x1462),x1461) % 25.35/25.56 [147]~P17(x1471)+P18(x1471)+~P3(x1472)+~P42(f40(x1472),x1471) % 25.35/25.56 [148]~P19(x1481)+P18(x1481)+~P3(x1482)+~P42(f39(x1482),x1481) % 25.35/25.56 [149]~P18(x1491)+P19(x1491)+~P3(x1492)+~P42(f39(x1492),x1491) % 25.35/25.56 [150]~P20(x1501)+P19(x1501)+~P3(x1502)+~P42(f38(x1502),x1501) % 25.35/25.56 [151]~P19(x1511)+P20(x1511)+~P3(x1512)+~P42(f38(x1512),x1511) % 25.35/25.56 [152]~P21(x1521)+P20(x1521)+~P3(x1522)+~P42(f37(x1522),x1521) % 25.35/25.56 [153]~P20(x1531)+P21(x1531)+~P3(x1532)+~P42(f37(x1532),x1531) % 25.35/25.56 [154]~P22(x1541)+P21(x1541)+~P3(x1542)+~P42(f36(x1542),x1541) % 25.35/25.56 [155]~P21(x1551)+P22(x1551)+~P3(x1552)+~P42(f36(x1552),x1551) % 25.35/25.56 [156]~P23(x1561)+P22(x1561)+~P3(x1562)+~P42(f33(x1562),x1561) % 25.35/25.56 [157]~P22(x1571)+P23(x1571)+~P3(x1572)+~P42(f33(x1572),x1571) % 25.35/25.56 [158]~P24(x1581)+P23(x1581)+~P3(x1582)+~P42(f32(x1582),x1581) % 25.35/25.56 [159]~P23(x1591)+P24(x1591)+~P3(x1592)+~P42(f32(x1592),x1591) % 25.35/25.56 [160]~P25(x1601)+P24(x1601)+~P3(x1602)+~P42(f31(x1602),x1601) % 25.35/25.56 [161]~P24(x1611)+P25(x1611)+~P3(x1612)+~P42(f31(x1612),x1611) % 25.35/25.56 [162]~P26(x1621)+P25(x1621)+~P3(x1622)+~P42(f30(x1622),x1621) % 25.35/25.56 [163]~P25(x1631)+P26(x1631)+~P3(x1632)+~P42(f30(x1632),x1631) % 25.35/25.56 [164]~P27(x1641)+P26(x1641)+~P3(x1642)+~P42(f29(x1642),x1641) % 25.35/25.56 [165]~P26(x1651)+P27(x1651)+~P3(x1652)+~P42(f29(x1652),x1651) % 25.35/25.56 [166]~P28(x1661)+P27(x1661)+~P3(x1662)+~P42(f28(x1662),x1661) % 25.35/25.56 [167]~P27(x1671)+P28(x1671)+~P3(x1672)+~P42(f28(x1672),x1671) % 25.35/25.56 [168]~P29(x1681)+P28(x1681)+~P3(x1682)+~P42(f27(x1682),x1681) % 25.35/25.56 [169]~P28(x1691)+P29(x1691)+~P3(x1692)+~P42(f27(x1692),x1691) % 25.35/25.56 [170]~P30(x1701)+P29(x1701)+~P3(x1702)+~P42(f26(x1702),x1701) % 25.35/25.56 [171]~P29(x1711)+P30(x1711)+~P3(x1712)+~P42(f26(x1712),x1711) % 25.35/25.56 [172]~P31(x1721)+P30(x1721)+~P3(x1722)+~P42(f25(x1722),x1721) % 25.35/25.56 [173]~P30(x1731)+P31(x1731)+~P3(x1732)+~P42(f25(x1732),x1731) % 25.35/25.56 [174]~P32(x1741)+P31(x1741)+~P3(x1742)+~P42(f24(x1742),x1741) % 25.35/25.56 [175]~P31(x1751)+P32(x1751)+~P3(x1752)+~P42(f24(x1752),x1751) % 25.35/25.56 [176]~P33(x1761)+P32(x1761)+~P3(x1762)+~P42(f22(x1762),x1761) % 25.35/25.56 [177]~P32(x1771)+P33(x1771)+~P3(x1772)+~P42(f22(x1772),x1771) % 25.35/25.56 [178]~P34(x1781)+P33(x1781)+~P3(x1782)+~P42(f21(x1782),x1781) % 25.35/25.56 [179]~P33(x1791)+P34(x1791)+~P3(x1792)+~P42(f21(x1792),x1791) % 25.35/25.56 [180]~P35(x1801)+P34(x1801)+~P3(x1802)+~P42(f20(x1802),x1801) % 25.35/25.56 [181]~P34(x1811)+P35(x1811)+~P3(x1812)+~P42(f20(x1812),x1811) % 25.35/25.56 [182]~P36(x1821)+P35(x1821)+~P3(x1822)+~P42(f19(x1822),x1821) % 25.35/25.56 [183]~P35(x1831)+P36(x1831)+~P3(x1832)+~P42(f19(x1832),x1831) % 25.35/25.56 [184]~P37(x1841)+P36(x1841)+~P3(x1842)+~P42(f18(x1842),x1841) % 25.35/25.56 [185]~P36(x1851)+P37(x1851)+~P3(x1852)+~P42(f18(x1852),x1851) % 25.35/25.56 [186]~P38(x1861)+P37(x1861)+~P3(x1862)+~P42(f17(x1862),x1861) % 25.35/25.56 [187]~P37(x1871)+P38(x1871)+~P3(x1872)+~P42(f17(x1872),x1871) % 25.35/25.56 [188]~P39(x1881)+P38(x1881)+~P3(x1882)+~P42(f16(x1882),x1881) % 25.35/25.56 [189]~P38(x1891)+P39(x1891)+~P3(x1892)+~P42(f16(x1892),x1891) % 25.35/25.56 [190]~P5(x1901)+P39(x1901)+~P3(x1902)+~P42(f15(x1902),x1901) % 25.35/25.56 [191]~P39(x1911)+P5(x1911)+~P3(x1912)+~P42(f15(x1912),x1911) % 25.35/25.56 [192]~P6(x1921)+P5(x1921)+~P3(x1922)+~P42(f14(x1922),x1921) % 25.35/25.56 [193]~P5(x1931)+P6(x1931)+~P3(x1932)+~P42(f14(x1932),x1931) % 25.35/25.56 [194]~P7(x1941)+P6(x1941)+~P3(x1942)+~P42(f13(x1942),x1941) % 25.35/25.56 [195]~P6(x1951)+P7(x1951)+~P3(x1952)+~P42(f13(x1952),x1951) % 25.35/25.56 [196]~P8(x1961)+P7(x1961)+~P3(x1962)+~P42(f12(x1962),x1961) % 25.35/25.56 [197]~P7(x1971)+P8(x1971)+~P3(x1972)+~P42(f12(x1972),x1971) % 25.35/25.56 [198]~P9(x1981)+P8(x1981)+~P3(x1982)+~P42(f11(x1982),x1981) % 25.35/25.56 [199]~P8(x1991)+P9(x1991)+~P3(x1992)+~P42(f11(x1992),x1991) % 25.35/25.56 [200]~P10(x2001)+P9(x2001)+~P3(x2002)+~P42(f10(x2002),x2001) % 25.35/25.56 [201]~P9(x2011)+P10(x2011)+~P3(x2012)+~P42(f10(x2012),x2011) % 25.35/25.56 [202]~P11(x2021)+P10(x2021)+~P3(x2022)+~P42(f9(x2022),x2021) % 25.35/25.56 [203]~P10(x2031)+P11(x2031)+~P3(x2032)+~P42(f9(x2032),x2031) % 25.35/25.56 [204]~P12(x2041)+P11(x2041)+~P3(x2042)+~P42(f8(x2042),x2041) % 25.35/25.56 [205]~P11(x2051)+P12(x2051)+~P3(x2052)+~P42(f8(x2052),x2051) % 25.35/25.56 [206]~P13(x2061)+P12(x2061)+~P3(x2062)+~P42(f7(x2062),x2061) % 25.35/25.56 [207]~P12(x2071)+P13(x2071)+~P3(x2072)+~P42(f7(x2072),x2071) % 25.35/25.56 [208]~P14(x2081)+P13(x2081)+~P3(x2082)+~P42(f6(x2082),x2081) % 25.35/25.56 [209]~P13(x2091)+P14(x2091)+~P3(x2092)+~P42(f6(x2092),x2091) % 25.35/25.56 [210]~P43(x2101)+P14(x2101)+~P3(x2102)+~P42(f5(x2102),x2101) % 25.35/25.56 [211]~P14(x2111)+P43(x2111)+~P3(x2112)+~P42(f5(x2112),x2111) % 25.35/25.56 [212]~P44(x2121)+P43(x2121)+~P3(x2122)+~P42(f4(x2122),x2121) % 25.35/25.56 [213]~P43(x2131)+P44(x2131)+~P3(x2132)+~P42(f4(x2132),x2131) % 25.35/25.56 [214]~P45(x2141)+P44(x2141)+~P3(x2142)+~P42(f3(x2142),x2141) % 25.35/25.56 [215]~P44(x2151)+P45(x2151)+~P3(x2152)+~P42(f3(x2152),x2151) % 25.35/25.56 [216]~P46(x2161)+P45(x2161)+~P3(x2162)+~P42(f49(x2162),x2161) % 25.35/25.56 [217]~P45(x2171)+P46(x2171)+~P3(x2172)+~P42(f49(x2172),x2171) % 25.35/25.56 [218]~P47(x2181)+P46(x2181)+~P3(x2182)+~P42(f48(x2182),x2181) % 25.35/25.56 [219]~P46(x2191)+P47(x2191)+~P3(x2192)+~P42(f48(x2192),x2191) % 25.35/25.56 [220]~P41(x2201)+P47(x2201)+~P3(x2202)+~P42(f47(x2202),x2201) % 25.35/25.56 [221]~P47(x2211)+P41(x2211)+~P3(x2212)+~P42(f47(x2212),x2211) % 25.35/25.56 [222]~P40(x2221)+P41(x2221)+~P3(x2222)+~P42(f46(x2222),x2221) % 25.35/25.56 [223]~P41(x2231)+P40(x2231)+~P3(x2232)+~P42(f46(x2232),x2231) % 25.35/25.56 [224]~P4(x2241)+P40(x2241)+~P3(x2242)+~P42(f45(x2242),x2241) % 25.35/25.56 [225]~P40(x2251)+P4(x2251)+~P3(x2252)+~P42(f45(x2252),x2251) % 25.35/25.56 %EqnAxiom % 25.35/25.56 % 25.35/25.56 %------------------------------------------- % 25.35/25.56 cnf(227,plain, % 25.35/25.56 (P3(a34)), % 25.35/25.56 inference(scs_inference,[],[6,8])). % 25.35/25.56 cnf(457,plain, % 25.35/25.56 (P42(a34,f45(a34))), % 25.35/25.56 inference(scs_inference,[],[6,9,8])). % 25.35/25.56 cnf(458,plain, % 25.35/25.56 (P3(f45(a34))), % 25.35/25.56 inference(scs_inference,[],[457,8])). % 25.35/25.56 cnf(3170,plain, % 25.35/25.56 (P23(f44(f45(a34)))+P24(f44(f45(a34)))), % 25.35/25.56 inference(scs_inference,[],[457,21,8])). % 25.35/25.56 cnf(3291,plain, % 25.35/25.56 (P45(f44(f45(a34)))+P46(f44(f45(a34)))), % 25.35/25.56 inference(scs_inference,[],[457,50,8])). % 25.35/25.56 cnf(3292,plain, % 25.35/25.56 (P46(f44(f45(a34)))+~P44(f44(f45(a34)))), % 25.35/25.56 inference(scs_inference,[],[458,3291,134])). % 25.35/25.56 cnf(3293,plain, % 25.35/25.56 (~P44(f44(f45(a34)))+~P45(f44(f45(a34)))), % 25.35/25.56 inference(scs_inference,[],[458,3292,135])). % 25.35/25.56 cnf(3294,plain, % 25.35/25.56 (~P45(f44(f45(a34)))+P43(f44(f45(a34)))), % 25.35/25.56 inference(scs_inference,[],[458,3293,48])). % 25.35/25.56 cnf(3295,plain, % 25.35/25.56 (P43(f44(f45(a34)))+P46(f44(f45(a34)))), % 25.35/25.56 inference(scs_inference,[],[3294,3291])). % 25.35/25.56 cnf(3296,plain, % 25.35/25.56 (P46(f44(f45(a34)))+~P14(f44(f45(a34)))), % 25.35/25.56 inference(scs_inference,[],[458,3295,132])). % 25.35/25.56 cnf(3297,plain, % 25.35/25.56 (~P14(f44(f45(a34)))+~P47(f44(f45(a34)))), % 25.35/25.56 inference(scs_inference,[],[458,3296,136])). % 25.35/25.56 cnf(3298,plain, % 25.35/25.56 (~P47(f44(f45(a34)))+P13(f44(f45(a34)))), % 25.35/25.56 inference(scs_inference,[],[458,3297,46])). % 25.35/25.56 cnf(3299,plain, % 25.35/25.56 (P13(f44(f45(a34)))+P46(f44(f45(a34)))), % 25.35/25.56 inference(scs_inference,[],[458,3298,51])). % 25.35/25.56 cnf(3300,plain, % 25.35/25.56 (P46(f44(f45(a34)))+~P12(f44(f45(a34)))), % 25.35/25.56 inference(scs_inference,[],[458,3299,130])). % 25.35/25.56 cnf(3301,plain, % 25.35/25.56 (~P12(f44(f45(a34)))+~P45(f44(f45(a34)))), % 25.35/25.56 inference(scs_inference,[],[458,3300,135])). % 25.35/25.56 cnf(3302,plain, % 25.35/25.56 (~P45(f44(f45(a34)))+P11(f44(f45(a34)))), % 25.35/25.56 inference(scs_inference,[],[458,3301,44])). % 25.35/25.56 cnf(3303,plain, % 25.35/25.56 (P11(f44(f45(a34)))+P46(f44(f45(a34)))), % 25.35/25.56 inference(scs_inference,[],[3302,3291])). % 25.35/25.56 cnf(3304,plain, % 25.35/25.56 (P46(f44(f45(a34)))+~P10(f44(f45(a34)))), % 25.35/25.56 inference(scs_inference,[],[458,3303,128])). % 25.35/25.56 cnf(3305,plain, % 25.35/25.56 (~P10(f44(f45(a34)))+~P47(f44(f45(a34)))), % 25.35/25.56 inference(scs_inference,[],[458,3304,136])). % 25.35/25.56 cnf(3306,plain, % 25.35/25.56 (~P47(f44(f45(a34)))+P9(f44(f45(a34)))), % 25.35/25.56 inference(scs_inference,[],[458,3305,42])). % 25.35/25.56 cnf(3307,plain, % 25.35/25.56 (P9(f44(f45(a34)))+P41(f44(f45(a34)))), % 25.35/25.56 inference(scs_inference,[],[458,3306,52])). % 25.35/25.56 cnf(3308,plain, % 25.35/25.56 (P41(f44(f45(a34)))+~P8(f44(f45(a34)))), % 25.35/25.56 inference(scs_inference,[],[458,3307,126])). % 25.35/25.56 cnf(3309,plain, % 25.35/25.56 (~P8(f44(f45(a34)))+~P47(f44(f45(a34)))), % 25.35/25.56 inference(scs_inference,[],[458,3308,137])). % 25.35/25.56 cnf(3310,plain, % 25.35/25.56 (~P47(f44(f45(a34)))+P7(f44(f45(a34)))), % 25.35/25.56 inference(scs_inference,[],[458,3309,40])). % 25.35/25.56 cnf(3311,plain, % 25.35/25.56 (P7(f44(f45(a34)))+P46(f44(f45(a34)))), % 25.35/25.56 inference(scs_inference,[],[458,3310,51])). % 25.35/25.56 cnf(3312,plain, % 25.35/25.56 (P46(f44(f45(a34)))+~P6(f44(f45(a34)))), % 25.35/25.56 inference(scs_inference,[],[458,3311,124])). % 25.35/25.56 cnf(3313,plain, % 25.35/25.56 (~P6(f44(f45(a34)))+~P45(f44(f45(a34)))), % 25.35/25.56 inference(scs_inference,[],[458,3312,135])). % 25.35/25.56 cnf(3314,plain, % 25.35/25.56 (~P45(f44(f45(a34)))+P5(f44(f45(a34)))), % 25.35/25.56 inference(scs_inference,[],[458,3313,38])). % 25.35/25.56 cnf(3315,plain, % 25.35/25.56 (P5(f44(f45(a34)))+P46(f44(f45(a34)))), % 25.35/25.56 inference(scs_inference,[],[3314,3291])). % 25.35/25.56 cnf(3316,plain, % 25.35/25.56 (P46(f44(f45(a34)))+~P39(f44(f45(a34)))), % 25.35/25.56 inference(scs_inference,[],[458,3315,122])). % 25.35/25.56 cnf(3317,plain, % 25.35/25.56 (~P39(f44(f45(a34)))+~P47(f44(f45(a34)))), % 25.35/25.56 inference(scs_inference,[],[458,3316,136])). % 25.35/25.56 cnf(3318,plain, % 25.35/25.56 (~P47(f44(f45(a34)))+P38(f44(f45(a34)))), % 25.35/25.56 inference(scs_inference,[],[458,3317,36])). % 25.35/25.56 cnf(3319,plain, % 25.35/25.56 (P38(f44(f45(a34)))+P41(f44(f45(a34)))), % 25.35/25.56 inference(scs_inference,[],[458,3318,52])). % 25.35/25.56 cnf(3320,plain, % 25.35/25.56 (P41(f44(f45(a34)))+~P37(f44(f45(a34)))), % 25.35/25.56 inference(scs_inference,[],[458,3319,120])). % 25.35/25.56 cnf(3321,plain, % 25.35/25.56 (~P37(f44(f45(a34)))+~P40(f44(f45(a34)))), % 25.35/25.56 inference(scs_inference,[],[458,3320,138])). % 25.35/25.56 cnf(3322,plain, % 25.35/25.56 (~P40(f44(f45(a34)))+P36(f44(f45(a34)))), % 25.35/25.56 inference(scs_inference,[],[458,3321,34])). % 25.35/25.56 cnf(3323,plain, % 25.35/25.56 (P36(f44(f45(a34)))+P41(f44(f45(a34)))), % 25.35/25.56 inference(scs_inference,[],[458,3322,53])). % 25.35/25.56 cnf(3324,plain, % 25.35/25.56 (P41(f44(f45(a34)))+~P35(f44(f45(a34)))), % 25.35/25.56 inference(scs_inference,[],[458,3323,118])). % 25.35/25.56 cnf(3325,plain, % 25.35/25.56 (~P35(f44(f45(a34)))+~P47(f44(f45(a34)))), % 25.35/25.56 inference(scs_inference,[],[458,3324,137])). % 25.35/25.56 cnf(3326,plain, % 25.35/25.56 (~P47(f44(f45(a34)))+P34(f44(f45(a34)))), % 25.35/25.56 inference(scs_inference,[],[458,3325,32])). % 25.35/25.56 cnf(3327,plain, % 25.35/25.56 (P34(f44(f45(a34)))+P46(f44(f45(a34)))), % 25.35/25.56 inference(scs_inference,[],[458,3326,51])). % 25.35/25.56 cnf(3328,plain, % 25.35/25.56 (P46(f44(f45(a34)))+~P33(f44(f45(a34)))), % 25.35/25.56 inference(scs_inference,[],[458,3327,116])). % 25.35/25.56 cnf(3329,plain, % 25.35/25.56 (~P33(f44(f45(a34)))+~P45(f44(f45(a34)))), % 25.35/25.56 inference(scs_inference,[],[458,3328,135])). % 25.35/25.56 cnf(3330,plain, % 25.35/25.56 (~P45(f44(f45(a34)))+P32(f44(f45(a34)))), % 25.35/25.56 inference(scs_inference,[],[458,3329,30])). % 25.35/25.56 cnf(3331,plain, % 25.35/25.56 (P32(f44(f45(a34)))+P46(f44(f45(a34)))), % 25.35/25.56 inference(scs_inference,[],[3330,3291])). % 25.35/25.56 cnf(3332,plain, % 25.35/25.56 (P46(f44(f45(a34)))+~P31(f44(f45(a34)))), % 25.35/25.56 inference(scs_inference,[],[458,3331,114])). % 25.35/25.56 cnf(3333,plain, % 25.35/25.56 (~P31(f44(f45(a34)))+~P47(f44(f45(a34)))), % 25.35/25.56 inference(scs_inference,[],[458,3332,136])). % 25.35/25.56 cnf(3334,plain, % 25.35/25.56 (~P47(f44(f45(a34)))+P30(f44(f45(a34)))), % 25.35/25.56 inference(scs_inference,[],[458,3333,28])). % 25.35/25.56 cnf(3335,plain, % 25.35/25.56 (P30(f44(f45(a34)))+P41(f44(f45(a34)))), % 25.35/25.56 inference(scs_inference,[],[458,3334,52])). % 25.35/25.56 cnf(3336,plain, % 25.35/25.56 (P41(f44(f45(a34)))+~P29(f44(f45(a34)))), % 25.35/25.56 inference(scs_inference,[],[458,3335,112])). % 25.35/25.56 cnf(3337,plain, % 25.35/25.56 (~P29(f44(f45(a34)))+~P40(f44(f45(a34)))), % 25.35/25.56 inference(scs_inference,[],[458,3336,138])). % 25.35/25.56 cnf(3338,plain, % 25.35/25.56 (~P40(f44(f45(a34)))+P28(f44(f45(a34)))), % 25.35/25.56 inference(scs_inference,[],[458,3337,26])). % 25.35/25.56 cnf(3339,plain, % 25.35/25.56 (P28(f44(f45(a34)))+P4(f44(f45(a34)))), % 25.35/25.57 inference(scs_inference,[],[458,3338,54])). % 25.35/25.57 cnf(3340,plain, % 25.35/25.57 (P4(f44(f45(a34)))+~P27(f44(f45(a34)))), % 25.35/25.57 inference(scs_inference,[],[458,3339,110])). % 25.35/25.57 cnf(3341,plain, % 25.35/25.57 (~P27(f44(f45(a34)))+~P2(f44(f45(a34)))), % 25.35/25.57 inference(scs_inference,[],[458,3340,97])). % 25.35/25.57 cnf(3342,plain, % 25.35/25.57 (~P2(f44(f45(a34)))+P26(f44(f45(a34)))), % 25.35/25.57 inference(scs_inference,[],[458,3341,24])). % 25.35/25.57 cnf(3343,plain, % 25.35/25.57 (P26(f44(f45(a34)))+P4(f44(f45(a34)))), % 25.35/25.57 inference(scs_inference,[],[458,3342,12])). % 25.35/25.57 cnf(3344,plain, % 25.35/25.57 (P4(f44(f45(a34)))+~P25(f44(f45(a34)))), % 25.35/25.57 inference(scs_inference,[],[458,3343,108])). % 25.35/25.57 cnf(3345,plain, % 25.35/25.57 (~P25(f44(f45(a34)))+~P40(f44(f45(a34)))), % 25.35/25.57 inference(scs_inference,[],[458,3344,139])). % 25.35/25.57 cnf(3346,plain, % 25.35/25.57 (~P40(f44(f45(a34)))+P24(f44(f45(a34)))), % 25.35/25.57 inference(scs_inference,[],[458,3345,22])). % 25.35/25.57 cnf(3347,plain, % 25.35/25.57 (P24(f44(f45(a34)))+P41(f44(f45(a34)))), % 25.35/25.57 inference(scs_inference,[],[458,3346,53])). % 25.35/25.57 cnf(3348,plain, % 25.35/25.57 (P41(f44(f45(a34)))+~P23(f44(f45(a34)))), % 25.35/25.57 inference(scs_inference,[],[458,3347,106])). % 25.35/25.57 cnf(3349,plain, % 25.35/25.57 (~P23(f44(f45(a34)))+~P47(f44(f45(a34)))), % 25.35/25.57 inference(scs_inference,[],[458,3348,137])). % 25.35/25.57 cnf(3350,plain, % 25.35/25.57 (~P47(f44(f45(a34)))+P24(f44(f45(a34)))), % 25.35/25.57 inference(scs_inference,[],[3349,3170])). % 25.35/25.57 cnf(3351,plain, % 25.35/25.57 (P24(f44(f45(a34)))+P46(f44(f45(a34)))), % 25.35/25.57 inference(scs_inference,[],[458,3350,51])). % 25.35/25.57 cnf(3352,plain, % 25.35/25.57 (P46(f44(f45(a34)))+~P25(f44(f45(a34)))), % 25.35/25.57 inference(scs_inference,[],[458,3351,107])). % 25.35/25.57 cnf(3353,plain, % 25.35/25.57 (~P25(f44(f45(a34)))+~P45(f44(f45(a34)))), % 25.35/25.57 inference(scs_inference,[],[458,3352,135])). % 25.35/25.57 cnf(3354,plain, % 25.35/25.57 (~P45(f44(f45(a34)))+P26(f44(f45(a34)))), % 25.35/25.57 inference(scs_inference,[],[458,3353,23])). % 25.35/25.57 cnf(3355,plain, % 25.35/25.57 (P26(f44(f45(a34)))+P46(f44(f45(a34)))), % 25.35/25.57 inference(scs_inference,[],[3354,3291])). % 25.35/25.57 cnf(3356,plain, % 25.35/25.57 (P46(f44(f45(a34)))+~P27(f44(f45(a34)))), % 25.35/25.57 inference(scs_inference,[],[458,3355,109])). % 25.35/25.57 cnf(3357,plain, % 25.35/25.57 (~P27(f44(f45(a34)))+~P47(f44(f45(a34)))), % 25.35/25.57 inference(scs_inference,[],[458,3356,136])). % 25.35/25.57 cnf(3358,plain, % 25.35/25.57 (~P47(f44(f45(a34)))+P28(f44(f45(a34)))), % 25.35/25.57 inference(scs_inference,[],[458,3357,25])). % 25.35/25.57 cnf(3359,plain, % 25.35/25.57 (P28(f44(f45(a34)))+P41(f44(f45(a34)))), % 25.35/25.57 inference(scs_inference,[],[458,3358,52])). % 25.35/25.57 cnf(3360,plain, % 25.35/25.57 (P41(f44(f45(a34)))+~P27(f44(f45(a34)))), % 25.35/25.57 inference(scs_inference,[],[458,3359,110])). % 25.35/25.57 cnf(3361,plain, % 25.35/25.57 (~P27(f44(f45(a34)))+~P40(f44(f45(a34)))), % 25.35/25.57 inference(scs_inference,[],[458,3360,138])). % 25.35/25.57 cnf(3362,plain, % 25.35/25.57 (~P40(f44(f45(a34)))+P26(f44(f45(a34)))), % 25.35/25.57 inference(scs_inference,[],[458,3361,24])). % 25.35/25.57 cnf(12896,plain, % 25.35/25.57 (P42(f45(a34),f44(f45(a34)))), % 25.35/25.57 inference(scs_inference,[],[457,8,11])). % 25.35/25.57 cnf(12897,plain, % 25.35/25.57 (P42(a34,f44(f45(a34)))), % 25.35/25.57 inference(scs_inference,[],[457,12896,226])). % 25.35/25.57 cnf(12899,plain, % 25.35/25.57 (P3(f44(f45(a34)))), % 25.35/25.57 inference(scs_inference,[],[457,12896,226,8])). % 25.35/25.57 cnf(12901,plain, % 25.35/25.57 (P4(f44(f45(a34)))+~P40(f44(f45(a34)))), % 25.35/25.57 inference(scs_inference,[],[457,227,12896,226,8,225])). % 25.35/25.57 cnf(12933,plain, % 25.35/25.57 (~P40(f44(f45(a34)))+~P2(f44(f45(a34)))), % 25.35/25.57 inference(scs_inference,[],[458,12901,97])). % 25.35/25.57 cnf(12951,plain, % 25.35/25.57 (~P4(f44(f45(a34)))), % 25.35/25.57 inference(scs_inference,[],[4,227,458,12897,12896,226,224,3322,3338,3346,3362,12933,107,109,111,119,139])). % 25.35/25.57 cnf(12988,plain, % 25.35/25.57 (~P2(f44(f45(a34)))), % 25.35/25.57 inference(scs_inference,[],[12899,6,12951,141])). % 25.35/25.57 cnf(12992,plain, % 25.35/25.57 ($false), % 25.35/25.57 inference(scs_inference,[],[12988,458,12951,12]), % 25.35/25.57 ['proof']). % 25.35/25.57 % SZS output end Proof % 25.35/25.57 % Total time :24.973443s %------------------------------------------------------------------------------