%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : LCL686+1.020 : TPTP v9.3.1. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % Computer : n002.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 30.29s 30.42s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : LCL686+1.020 : TPTP v9.3.1. Released v4.0.0. % 0.00/0.03 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.10/0.35 % Computer : n002.cluster.edu % 0.10/0.35 % Model : x86_64 x86_64 % 0.10/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.35 % Memory : 8046.5625MB % 0.10/0.35 % OS : Linux 6.8.0-71-generic % 0.10/0.35 % CPULimit : 300 % 0.10/0.35 % WCLimit : 300 % 0.10/0.35 % DateTime : Sun Sep 6 00:34:51 UTC 2026 % 0.10/0.36 % CPUTime : % 0.25/0.53 start to proof:theBenchmark % 30.18/30.39 %------------------------------------------- % 30.18/30.39 % File :CSE---1.7 % 30.18/30.39 % Problem :theBenchmark % 30.18/30.39 % Transform :cnf % 30.18/30.39 % Format :tptp:raw % 30.18/30.39 % Command :java -jar mcs_scs.jar %d %s % 30.18/30.39 % 30.18/30.39 % Result :Theorem 29.807445s % 30.18/30.39 % Output :CNFRefutation 29.807445s % 30.18/30.39 %------------------------------------------- % 30.18/30.39 %------------------------------------------------------------------------------ % 30.18/30.39 % File : LCL686+1.020 : TPTP v9.3.1. Released v4.0.0. % 30.18/30.39 % Domain : Logic Calculi (Modal Logic) % 30.18/30.39 % Problem : In S4, formula provable in S5 embedding, size 20 % 30.18/30.39 % Version : Especial. % 30.18/30.39 % English : % 30.18/30.39 % 30.18/30.39 % Refs : [BHS00] Balsiger et al. (2000), A Benchmark Method for the Pro % 30.18/30.39 % : [Kam08] Kaminski (2008), Email to G. Sutcliffe % 30.18/30.39 % Source : [Kam08] % 30.18/30.39 % Names : s4_s5_p [BHS00] % 30.18/30.39 % 30.18/30.39 % Status : Theorem % 30.18/30.39 % Rating : 0.00 v9.3.0, 0.05 v9.1.0, 0.07 v9.0.0, 0.06 v8.2.0, 0.07 v7.5.0, 0.14 v7.4.0, 0.06 v7.3.0, 0.14 v7.2.0, 0.00 v7.0.0, 0.07 v6.4.0, 0.00 v6.3.0, 0.08 v6.2.0, 0.09 v6.1.0, 0.16 v6.0.0, 0.25 v5.4.0, 0.22 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 % 30.18/30.39 % Syntax : Number of formulae : 3 ( 1 unt; 0 def) % 30.18/30.39 % Number of atoms : 594 ( 0 equ) % 30.18/30.39 % Maximal formula atoms : 590 ( 198 avg) % 30.18/30.39 % Number of connectives : 1067 ( 476 ~; 357 |; 233 &) % 30.18/30.39 % ( 0 <=>; 1 =>; 0 <=; 0 <~>) % 30.18/30.39 % Maximal formula depth : 190 ( 66 avg) % 30.18/30.39 % Maximal term depth : 1 ( 1 avg) % 30.18/30.39 % Number of predicates : 62 ( 61 usr; 1 prp; 0-2 aty) % 30.18/30.39 % Number of functors : 0 ( 0 usr; 0 con; --- aty) % 30.18/30.39 % Number of variables : 127 ( 126 !; 1 ?) % 30.18/30.39 % SPC : FOF_THM_RFO_NEQ % 30.18/30.39 % 30.18/30.39 % Comments : A naive relational encoding of the modal logic problem into % 30.18/30.39 % first-order logic. % 30.18/30.39 %------------------------------------------------------------------------------ % 30.18/30.39 fof(reflexivity,axiom, % 30.18/30.39 ! [X] : r1(X,X) ). % 30.18/30.39 % 30.18/30.39 fof(transitivity,axiom, % 30.18/30.39 ! [X,Y,Z] : % 30.18/30.39 ( ( r1(X,Y) % 30.18/30.39 & r1(Y,Z) ) % 30.18/30.39 => r1(X,Z) ) ). % 30.18/30.39 % 30.18/30.39 fof(main,conjecture, % 30.18/30.39 ~ ? [X] : % 30.18/30.39 ~ ( ! [Y] : % 30.18/30.39 ( ~ r1(X,Y) % 30.18/30.39 | ~ p60(Y) % 30.18/30.39 | ! [X] : % 30.18/30.39 ( ~ r1(Y,X) % 30.18/30.39 | ~ p1(X) ) ) % 30.18/30.39 | ! [Y] : % 30.18/30.39 ( ~ r1(X,Y) % 30.18/30.39 | ~ ! [X] : % 30.18/30.39 ( ~ r1(Y,X) % 30.18/30.39 | ~ ( ! [Y] : % 30.18/30.39 ( ~ r1(X,Y) % 30.18/30.39 | ! [X] : % 30.18/30.39 ( ~ r1(Y,X) % 30.18/30.39 | ! [Y] : % 30.18/30.39 ( ~ r1(X,Y) % 30.18/30.39 | ! [X] : % 30.18/30.39 ( ~ r1(Y,X) % 30.18/30.39 | ! [Y] : % 30.18/30.39 ( ~ r1(X,Y) % 30.18/30.39 | ! [X] : % 30.18/30.39 ( ~ r1(Y,X) % 30.18/30.39 | ! [Y] : % 30.18/30.39 ( ~ r1(X,Y) % 30.18/30.39 | ! [X] : % 30.18/30.39 ( ~ r1(Y,X) % 30.18/30.39 | ! [Y] : % 30.18/30.39 ( ~ r1(X,Y) % 30.18/30.39 | ! [X] : % 30.18/30.40 ( ~ r1(Y,X) % 30.18/30.40 | ! [Y] : % 30.18/30.40 ( ~ r1(X,Y) % 30.18/30.40 | ! [X] : % 30.18/30.40 ( ~ r1(Y,X) % 30.18/30.40 | ! [Y] : % 30.18/30.40 ( ~ r1(X,Y) % 30.18/30.40 | ! [X] : % 30.18/30.40 ( ~ r1(Y,X) % 30.18/30.40 | ! [Y] : % 30.18/30.40 ( ~ r1(X,Y) % 30.18/30.40 | ! [X] : % 30.18/30.40 ( ~ r1(Y,X) % 30.18/30.40 | ! [Y] : % 30.18/30.40 ( ~ r1(X,Y) % 30.18/30.40 | ! [X] : % 30.18/30.40 ( ~ r1(Y,X) % 30.18/30.40 | ! [Y] : % 30.18/30.40 ( ~ r1(X,Y) % 30.18/30.40 | ! [X] : % 30.18/30.40 ( ~ r1(Y,X) % 30.18/30.40 | ! [Y] : % 30.18/30.40 ( ~ r1(X,Y) % 30.18/30.40 | ! [X] : % 30.18/30.40 ( ~ r1(Y,X) % 30.18/30.40 | ! [Y] : % 30.18/30.40 ( ~ r1(X,Y) % 30.18/30.40 | ! [X] : % 30.29/30.40 ( ~ r1(Y,X) % 30.29/30.40 | ! [Y] : % 30.29/30.40 ( ~ r1(X,Y) % 30.29/30.40 | ! [X] : % 30.29/30.40 ( ~ r1(Y,X) % 30.29/30.40 | ! [Y] : % 30.29/30.40 ( ~ r1(X,Y) % 30.29/30.40 | ! [X] : % 30.29/30.40 ( ~ r1(Y,X) % 30.29/30.40 | ! [Y] : % 30.29/30.40 ( ~ r1(X,Y) % 30.29/30.40 | ! [X] : % 30.29/30.40 ( ~ r1(Y,X) % 30.29/30.40 | ! [Y] : % 30.29/30.40 ( ~ r1(X,Y) % 30.29/30.40 | ! [X] : % 30.29/30.40 ( ~ r1(Y,X) % 30.29/30.40 | ! [Y] : % 30.29/30.40 ( ~ r1(X,Y) % 30.29/30.40 | ! [X] : % 30.29/30.40 ( ~ r1(Y,X) % 30.29/30.40 | ! [Y] : % 30.29/30.40 ( ~ r1(X,Y) % 30.29/30.40 | ! [X] : % 30.29/30.40 ( ~ r1(Y,X) % 30.29/30.40 | ! [Y] : % 30.29/30.40 ( ~ r1(X,Y) % 30.29/30.40 | ! [X] : % 30.29/30.40 ( ~ r1(Y,X) % 30.29/30.40 | ! [Y] : % 30.29/30.40 ( ~ r1(X,Y) % 30.29/30.40 | ! [X] : % 30.29/30.40 ( ~ r1(Y,X) % 30.29/30.40 | ! [Y] : % 30.29/30.40 ( ~ r1(X,Y) % 30.29/30.40 | ! [X] : % 30.29/30.40 ( ~ r1(Y,X) % 30.29/30.40 | ! [Y] : % 30.29/30.40 ( ~ r1(X,Y) % 30.29/30.40 | ! [X] : % 30.29/30.40 ( ~ r1(Y,X) % 30.29/30.40 | ! [Y] : % 30.29/30.40 ( ~ r1(X,Y) % 30.29/30.40 | ! [X] : % 30.29/30.40 ( ~ r1(Y,X) % 30.29/30.40 | ! [Y] : % 30.29/30.40 ( ~ r1(X,Y) % 30.29/30.40 | ! [X] : % 30.29/30.40 ( ~ r1(Y,X) % 30.29/30.40 | ! [Y] : % 30.29/30.40 ( ~ r1(X,Y) % 30.29/30.40 | ! [X] : % 30.29/30.40 ( ~ r1(Y,X) % 30.29/30.40 | ! [Y] : % 30.29/30.40 ( ~ r1(X,Y) % 30.29/30.40 | ! [X] : % 30.29/30.40 ( ~ r1(Y,X) % 30.29/30.40 | ! [Y] : % 30.29/30.40 ( ~ r1(X,Y) % 30.29/30.40 | ! [X] : % 30.29/30.40 ( ~ r1(Y,X) % 30.29/30.40 | ! [Y] : % 30.29/30.40 ( ~ r1(X,Y) % 30.29/30.40 | ! [X] : % 30.29/30.40 ( ~ r1(Y,X) % 30.29/30.40 | ! [Y] : % 30.29/30.40 ( ~ r1(X,Y) % 30.29/30.40 | ! [X] : % 30.29/30.40 ( ~ r1(Y,X) % 30.29/30.40 | $false ) % 30.29/30.40 | ~ ! [X] : % 30.29/30.40 ( ~ r1(Y,X) % 30.29/30.40 | ~ ( ( p59(X) % 30.29/30.40 & ~ p58(X) ) % 30.29/30.40 | ( ~ p59(X) % 30.29/30.40 & p58(X) ) ) ) ) % 30.29/30.40 | ~ ! [Y] : % 30.29/30.40 ( ~ r1(X,Y) % 30.29/30.40 | ~ ( ( p58(Y) % 30.29/30.40 & ~ p57(Y) ) % 30.29/30.40 | ( ~ p58(Y) % 30.29/30.40 & p57(Y) ) ) ) ) % 30.29/30.40 | ~ ! [X] : % 30.29/30.40 ( ~ r1(Y,X) % 30.29/30.40 | ~ ( ( p57(X) % 30.29/30.40 & ~ p56(X) ) % 30.29/30.40 | ( ~ p57(X) % 30.29/30.40 & p56(X) ) ) ) ) % 30.29/30.40 | ~ ! [Y] : % 30.29/30.40 ( ~ r1(X,Y) % 30.29/30.40 | ~ ( ( p56(Y) % 30.29/30.40 & ~ p55(Y) ) % 30.29/30.40 | ( ~ p56(Y) % 30.29/30.40 & p55(Y) ) ) ) ) % 30.29/30.40 | ~ ! [X] : % 30.29/30.40 ( ~ r1(Y,X) % 30.29/30.40 | ~ ( ( p55(X) % 30.29/30.40 & ~ p54(X) ) % 30.29/30.40 | ( ~ p55(X) % 30.29/30.40 & p54(X) ) ) ) ) % 30.29/30.40 | ~ ! [Y] : % 30.29/30.40 ( ~ r1(X,Y) % 30.29/30.40 | ~ ( ( p54(Y) % 30.29/30.40 & ~ p53(Y) ) % 30.29/30.40 | ( ~ p54(Y) % 30.29/30.40 & p53(Y) ) ) ) ) % 30.29/30.40 | ~ ! [X] : % 30.29/30.40 ( ~ r1(Y,X) % 30.29/30.40 | ~ ( ( p53(X) % 30.29/30.40 & ~ p52(X) ) % 30.29/30.40 | ( ~ p53(X) % 30.29/30.40 & p52(X) ) ) ) ) % 30.29/30.40 | ~ ! [Y] : % 30.29/30.40 ( ~ r1(X,Y) % 30.29/30.40 | ~ ( ( p52(Y) % 30.29/30.40 & ~ p51(Y) ) % 30.29/30.40 | ( ~ p52(Y) % 30.29/30.40 & p51(Y) ) ) ) ) % 30.29/30.40 | ~ ! [X] : % 30.29/30.40 ( ~ r1(Y,X) % 30.29/30.41 | ~ ( ( p51(X) % 30.29/30.41 & ~ p50(X) ) % 30.29/30.41 | ( ~ p51(X) % 30.29/30.41 & p50(X) ) ) ) ) % 30.29/30.41 | ~ ! [Y] : % 30.29/30.41 ( ~ r1(X,Y) % 30.29/30.41 | ~ ( ( p50(Y) % 30.29/30.41 & ~ p49(Y) ) % 30.29/30.41 | ( ~ p50(Y) % 30.29/30.41 & p49(Y) ) ) ) ) % 30.29/30.41 | ~ ! [X] : % 30.29/30.41 ( ~ r1(Y,X) % 30.29/30.41 | ~ ( ( p49(X) % 30.29/30.41 & ~ p48(X) ) % 30.29/30.41 | ( ~ p49(X) % 30.29/30.41 & p48(X) ) ) ) ) % 30.29/30.41 | ~ ! [Y] : % 30.29/30.41 ( ~ r1(X,Y) % 30.29/30.41 | ~ ( ( p48(Y) % 30.29/30.41 & ~ p47(Y) ) % 30.29/30.41 | ( ~ p48(Y) % 30.29/30.41 & p47(Y) ) ) ) ) % 30.29/30.41 | ~ ! [X] : % 30.29/30.41 ( ~ r1(Y,X) % 30.29/30.41 | ~ ( ( p47(X) % 30.29/30.41 & ~ p46(X) ) % 30.29/30.41 | ( ~ p47(X) % 30.29/30.41 & p46(X) ) ) ) ) % 30.29/30.41 | ~ ! [Y] : % 30.29/30.41 ( ~ r1(X,Y) % 30.29/30.41 | ~ ( ( p46(Y) % 30.29/30.41 & ~ p45(Y) ) % 30.29/30.41 | ( ~ p46(Y) % 30.29/30.41 & p45(Y) ) ) ) ) % 30.29/30.41 | ~ ! [X] : % 30.29/30.41 ( ~ r1(Y,X) % 30.29/30.41 | ~ ( ( p45(X) % 30.29/30.41 & ~ p44(X) ) % 30.29/30.41 | ( ~ p45(X) % 30.29/30.41 & p44(X) ) ) ) ) % 30.29/30.41 | ~ ! [Y] : % 30.29/30.41 ( ~ r1(X,Y) % 30.29/30.41 | ~ ( ( p44(Y) % 30.29/30.41 & ~ p43(Y) ) % 30.29/30.41 | ( ~ p44(Y) % 30.29/30.41 & p43(Y) ) ) ) ) % 30.29/30.41 | ~ ! [X] : % 30.29/30.41 ( ~ r1(Y,X) % 30.29/30.41 | ~ ( ( p43(X) % 30.29/30.41 & ~ p42(X) ) % 30.29/30.41 | ( ~ p43(X) % 30.29/30.41 & p42(X) ) ) ) ) % 30.29/30.41 | ~ ! [Y] : % 30.29/30.41 ( ~ r1(X,Y) % 30.29/30.41 | ~ ( ( p42(Y) % 30.29/30.41 & ~ p41(Y) ) % 30.29/30.41 | ( ~ p42(Y) % 30.29/30.41 & p41(Y) ) ) ) ) % 30.29/30.41 | ~ ! [X] : % 30.29/30.41 ( ~ r1(Y,X) % 30.29/30.41 | ~ ( ( p41(X) % 30.29/30.41 & ~ p40(X) ) % 30.29/30.41 | ( ~ p41(X) % 30.29/30.41 & p40(X) ) ) ) ) % 30.29/30.41 | ~ ! [Y] : % 30.29/30.41 ( ~ r1(X,Y) % 30.29/30.41 | ~ ( ( p40(Y) % 30.29/30.41 & ~ p39(Y) ) % 30.29/30.41 | ( ~ p40(Y) % 30.29/30.41 & p39(Y) ) ) ) ) % 30.29/30.41 | ~ ! [X] : % 30.29/30.41 ( ~ r1(Y,X) % 30.29/30.41 | ~ ( ( p39(X) % 30.29/30.41 & ~ p38(X) ) % 30.29/30.41 | ( ~ p39(X) % 30.29/30.41 & p38(X) ) ) ) ) % 30.29/30.41 | ~ ! [Y] : % 30.29/30.41 ( ~ r1(X,Y) % 30.29/30.41 | ~ ( ( p38(Y) % 30.29/30.41 & ~ p37(Y) ) % 30.29/30.41 | ( ~ p38(Y) % 30.29/30.41 & p37(Y) ) ) ) ) % 30.29/30.41 | ~ ! [X] : % 30.29/30.41 ( ~ r1(Y,X) % 30.29/30.41 | ~ ( ( p37(X) % 30.29/30.41 & ~ p36(X) ) % 30.29/30.41 | ( ~ p37(X) % 30.29/30.41 & p36(X) ) ) ) ) % 30.29/30.41 | ~ ! [Y] : % 30.29/30.41 ( ~ r1(X,Y) % 30.29/30.41 | ~ ( ( p36(Y) % 30.29/30.41 & ~ p35(Y) ) % 30.29/30.41 | ( ~ p36(Y) % 30.29/30.41 & p35(Y) ) ) ) ) % 30.29/30.41 | ~ ! [X] : % 30.29/30.41 ( ~ r1(Y,X) % 30.29/30.41 | ~ ( ( p35(X) % 30.29/30.41 & ~ p34(X) ) % 30.29/30.41 | ( ~ p35(X) % 30.29/30.41 & p34(X) ) ) ) ) % 30.29/30.41 | ~ ! [Y] : % 30.29/30.41 ( ~ r1(X,Y) % 30.29/30.41 | ~ ( ( p34(Y) % 30.29/30.41 & ~ p33(Y) ) % 30.29/30.41 | ( ~ p34(Y) % 30.29/30.41 & p33(Y) ) ) ) ) % 30.29/30.41 | ~ ! [X] : % 30.29/30.41 ( ~ r1(Y,X) % 30.29/30.41 | ~ ( ( p33(X) % 30.29/30.41 & ~ p32(X) ) % 30.29/30.41 | ( ~ p33(X) % 30.29/30.41 & p32(X) ) ) ) ) % 30.29/30.41 | ~ ! [Y] : % 30.29/30.41 ( ~ r1(X,Y) % 30.29/30.41 | ~ ( ( p32(Y) % 30.29/30.41 & ~ p31(Y) ) % 30.29/30.41 | ( ~ p32(Y) % 30.29/30.41 & p31(Y) ) ) ) ) % 30.29/30.41 | ~ ! [X] : % 30.29/30.41 ( ~ r1(Y,X) % 30.29/30.41 | ~ ( ( p31(X) % 30.29/30.41 & ~ p30(X) ) % 30.29/30.41 | ( ~ p31(X) % 30.29/30.41 & p30(X) ) ) ) ) % 30.29/30.41 | ~ ! [Y] : % 30.29/30.41 ( ~ r1(X,Y) % 30.29/30.41 | ~ ( ( p30(Y) % 30.29/30.41 & ~ p29(Y) ) % 30.29/30.41 | ( ~ p30(Y) % 30.29/30.41 & p29(Y) ) ) ) ) % 30.29/30.41 | ~ ! [X] : % 30.29/30.41 ( ~ r1(Y,X) % 30.29/30.41 | ~ ( ( p29(X) % 30.29/30.41 & ~ p28(X) ) % 30.29/30.41 | ( ~ p29(X) % 30.29/30.41 & p28(X) ) ) ) ) % 30.29/30.41 | ~ ! [Y] : % 30.29/30.41 ( ~ r1(X,Y) % 30.29/30.41 | ~ ( ( p28(Y) % 30.29/30.41 & ~ p27(Y) ) % 30.29/30.41 | ( ~ p28(Y) % 30.29/30.41 & p27(Y) ) ) ) ) % 30.29/30.41 | ~ ! [X] : % 30.29/30.41 ( ~ r1(Y,X) % 30.29/30.41 | ~ ( ( p27(X) % 30.29/30.41 & ~ p26(X) ) % 30.29/30.41 | ( ~ p27(X) % 30.29/30.41 & p26(X) ) ) ) ) % 30.29/30.41 | ~ ! [Y] : % 30.29/30.41 ( ~ r1(X,Y) % 30.29/30.41 | ~ ( ( p26(Y) % 30.29/30.41 & ~ p25(Y) ) % 30.29/30.41 | ( ~ p26(Y) % 30.29/30.41 & p25(Y) ) ) ) ) % 30.29/30.41 | ~ ! [X] : % 30.29/30.41 ( ~ r1(Y,X) % 30.29/30.41 | ~ ( ( p25(X) % 30.29/30.41 & ~ p24(X) ) % 30.29/30.41 | ( ~ p25(X) % 30.29/30.41 & p24(X) ) ) ) ) % 30.29/30.41 | ~ ! [Y] : % 30.29/30.41 ( ~ r1(X,Y) % 30.29/30.41 | ~ ( ( p24(Y) % 30.29/30.41 & ~ p23(Y) ) % 30.29/30.41 | ( ~ p24(Y) % 30.29/30.41 & p23(Y) ) ) ) ) % 30.29/30.41 | ~ ! [X] : % 30.29/30.41 ( ~ r1(Y,X) % 30.29/30.41 | ~ ( ( p23(X) % 30.29/30.41 & ~ p22(X) ) % 30.29/30.41 | ( ~ p23(X) % 30.29/30.41 & p22(X) ) ) ) ) % 30.29/30.41 | ~ ! [Y] : % 30.29/30.41 ( ~ r1(X,Y) % 30.29/30.41 | ~ ( ( p22(Y) % 30.29/30.41 & ~ p21(Y) ) % 30.29/30.41 | ( ~ p22(Y) % 30.29/30.41 & p21(Y) ) ) ) ) % 30.29/30.41 | ~ ! [X] : % 30.29/30.41 ( ~ r1(Y,X) % 30.29/30.41 | ~ ( ( p21(X) % 30.29/30.41 & ~ p20(X) ) % 30.29/30.41 | ( ~ p21(X) % 30.29/30.41 & p20(X) ) ) ) ) % 30.29/30.41 | ~ ! [Y] : % 30.29/30.41 ( ~ r1(X,Y) % 30.29/30.41 | ~ ( ( p20(Y) % 30.29/30.41 & ~ p19(Y) ) % 30.29/30.41 | ( ~ p20(Y) % 30.29/30.41 & p19(Y) ) ) ) ) % 30.29/30.41 | ~ ! [X] : % 30.29/30.41 ( ~ r1(Y,X) % 30.29/30.41 | ~ ( ( p19(X) % 30.29/30.41 & ~ p18(X) ) % 30.29/30.41 | ( ~ p19(X) % 30.29/30.41 & p18(X) ) ) ) ) % 30.29/30.41 | ~ ! [Y] : % 30.29/30.41 ( ~ r1(X,Y) % 30.29/30.41 | ~ ( ( p18(Y) % 30.29/30.41 & ~ p17(Y) ) % 30.29/30.41 | ( ~ p18(Y) % 30.29/30.41 & p17(Y) ) ) ) ) % 30.29/30.41 | ~ ! [X] : % 30.29/30.41 ( ~ r1(Y,X) % 30.29/30.41 | ~ ( ( p17(X) % 30.29/30.41 & ~ p16(X) ) % 30.29/30.41 | ( ~ p17(X) % 30.29/30.41 & p16(X) ) ) ) ) % 30.29/30.41 | ~ ! [Y] : % 30.29/30.41 ( ~ r1(X,Y) % 30.29/30.41 | ~ ( ( p16(Y) % 30.29/30.41 & ~ p15(Y) ) % 30.29/30.41 | ( ~ p16(Y) % 30.29/30.41 & p15(Y) ) ) ) ) % 30.29/30.41 | ~ ! [X] : % 30.29/30.41 ( ~ r1(Y,X) % 30.29/30.41 | ~ ( ( p15(X) % 30.29/30.41 & ~ p14(X) ) % 30.29/30.41 | ( ~ p15(X) % 30.29/30.41 & p14(X) ) ) ) ) % 30.29/30.41 | ~ ! [Y] : % 30.29/30.41 ( ~ r1(X,Y) % 30.29/30.41 | ~ ( ( p14(Y) % 30.29/30.41 & ~ p13(Y) ) % 30.29/30.42 | ( ~ p14(Y) % 30.29/30.42 & p13(Y) ) ) ) ) % 30.29/30.42 | ~ ! [X] : % 30.29/30.42 ( ~ r1(Y,X) % 30.29/30.42 | ~ ( ( p13(X) % 30.29/30.42 & ~ p12(X) ) % 30.29/30.42 | ( ~ p13(X) % 30.29/30.42 & p12(X) ) ) ) ) % 30.29/30.42 | ~ ! [Y] : % 30.29/30.42 ( ~ r1(X,Y) % 30.29/30.42 | ~ ( ( p12(Y) % 30.29/30.42 & ~ p11(Y) ) % 30.29/30.42 | ( ~ p12(Y) % 30.29/30.42 & p11(Y) ) ) ) ) % 30.29/30.42 | ~ ! [X] : % 30.29/30.42 ( ~ r1(Y,X) % 30.29/30.42 | ~ ( ( p11(X) % 30.29/30.42 & ~ p10(X) ) % 30.29/30.42 | ( ~ p11(X) % 30.29/30.42 & p10(X) ) ) ) ) % 30.29/30.42 | ~ ! [Y] : % 30.29/30.42 ( ~ r1(X,Y) % 30.29/30.42 | ~ ( ( p10(Y) % 30.29/30.42 & ~ p9(Y) ) % 30.29/30.42 | ( ~ p10(Y) % 30.29/30.42 & p9(Y) ) ) ) ) % 30.29/30.42 | ~ ! [X] : % 30.29/30.42 ( ~ r1(Y,X) % 30.29/30.42 | ~ ( ( p9(X) % 30.29/30.42 & ~ p8(X) ) % 30.29/30.42 | ( ~ p9(X) % 30.29/30.42 & p8(X) ) ) ) ) % 30.29/30.42 | ~ ! [Y] : % 30.29/30.42 ( ~ r1(X,Y) % 30.29/30.42 | ~ ( ( p8(Y) % 30.29/30.42 & ~ p7(Y) ) % 30.29/30.42 | ( ~ p8(Y) % 30.29/30.42 & p7(Y) ) ) ) ) % 30.29/30.42 | ~ ! [X] : % 30.29/30.42 ( ~ r1(Y,X) % 30.29/30.42 | ~ ( ( p7(X) % 30.29/30.42 & ~ p6(X) ) % 30.29/30.42 | ( ~ p7(X) % 30.29/30.42 & p6(X) ) ) ) ) % 30.29/30.42 | ~ ! [Y] : % 30.29/30.42 ( ~ r1(X,Y) % 30.29/30.42 | ~ ( ( p6(Y) % 30.29/30.42 & ~ p5(Y) ) % 30.29/30.42 | ( ~ p6(Y) % 30.29/30.42 & p5(Y) ) ) ) ) % 30.29/30.42 | ~ ! [X] : % 30.29/30.42 ( ~ r1(Y,X) % 30.29/30.42 | ~ ( ( p5(X) % 30.29/30.42 & ~ p4(X) ) % 30.29/30.42 | ( ~ p5(X) % 30.29/30.42 & p4(X) ) ) ) ) % 30.29/30.42 | ~ ! [Y] : % 30.29/30.42 ( ~ r1(X,Y) % 30.29/30.42 | ~ ( ( p4(Y) % 30.29/30.42 & ~ p3(Y) ) % 30.29/30.42 | ( ~ p4(Y) % 30.29/30.42 & p3(Y) ) ) ) ) % 30.29/30.42 | ~ ! [X] : % 30.29/30.42 ( ~ r1(Y,X) % 30.29/30.42 | ~ ( ( p3(X) % 30.29/30.42 & ~ p2(X) ) % 30.29/30.42 | ( ~ p3(X) % 30.29/30.42 & p2(X) ) ) ) ) % 30.29/30.42 | ~ ! [Y] : % 30.29/30.42 ( ~ r1(X,Y) % 30.29/30.42 | ~ ( ( p2(Y) % 30.29/30.42 & ~ p1(Y) ) % 30.29/30.42 | ( ~ p2(Y) % 30.29/30.42 & p1(Y) ) ) ) % 30.29/30.42 | ! [Y] : % 30.29/30.42 ( ~ r1(X,Y) % 30.29/30.42 | p60(Y) ) % 30.29/30.42 | ! [Y] : % 30.29/30.42 ( ~ r1(X,Y) % 30.29/30.42 | ( ~ p58(Y) % 30.29/30.42 & ~ p59(Y) ) % 30.29/30.42 | ( p59(Y) % 30.29/30.42 & p58(Y) ) % 30.29/30.42 | ( ~ p57(Y) % 30.29/30.42 & ~ p58(Y) ) % 30.29/30.42 | ( p58(Y) % 30.29/30.42 & p57(Y) ) % 30.29/30.42 | ( ~ p56(Y) % 30.29/30.42 & ~ p57(Y) ) % 30.29/30.42 | ( p57(Y) % 30.29/30.42 & p56(Y) ) % 30.29/30.42 | ( ~ p55(Y) % 30.29/30.42 & ~ p56(Y) ) % 30.29/30.42 | ( p56(Y) % 30.29/30.42 & p55(Y) ) % 30.29/30.42 | ( ~ p54(Y) % 30.29/30.42 & ~ p55(Y) ) % 30.29/30.42 | ( p55(Y) % 30.29/30.42 & p54(Y) ) % 30.29/30.42 | ( ~ p53(Y) % 30.29/30.42 & ~ p54(Y) ) % 30.29/30.42 | ( p54(Y) % 30.29/30.42 & p53(Y) ) % 30.29/30.42 | ( ~ p52(Y) % 30.29/30.42 & ~ p53(Y) ) % 30.29/30.42 | ( p53(Y) % 30.29/30.42 & p52(Y) ) % 30.29/30.42 | ( ~ p51(Y) % 30.29/30.42 & ~ p52(Y) ) % 30.29/30.42 | ( p52(Y) % 30.29/30.42 & p51(Y) ) % 30.29/30.42 | ( ~ p50(Y) % 30.29/30.42 & ~ p51(Y) ) % 30.29/30.42 | ( p51(Y) % 30.29/30.42 & p50(Y) ) % 30.29/30.42 | ( ~ p49(Y) % 30.29/30.42 & ~ p50(Y) ) % 30.29/30.42 | ( p50(Y) % 30.29/30.42 & p49(Y) ) % 30.29/30.42 | ( ~ p48(Y) % 30.29/30.42 & ~ p49(Y) ) % 30.29/30.42 | ( p49(Y) % 30.29/30.42 & p48(Y) ) % 30.29/30.42 | ( ~ p47(Y) % 30.29/30.42 & ~ p48(Y) ) % 30.29/30.42 | ( p48(Y) % 30.29/30.42 & p47(Y) ) % 30.29/30.42 | ( ~ p46(Y) % 30.29/30.42 & ~ p47(Y) ) % 30.29/30.42 | ( p47(Y) % 30.29/30.42 & p46(Y) ) % 30.29/30.42 | ( ~ p45(Y) % 30.29/30.42 & ~ p46(Y) ) % 30.29/30.42 | ( p46(Y) % 30.29/30.42 & p45(Y) ) % 30.29/30.42 | ( ~ p44(Y) % 30.29/30.42 & ~ p45(Y) ) % 30.29/30.42 | ( p45(Y) % 30.29/30.42 & p44(Y) ) % 30.29/30.42 | ( ~ p43(Y) % 30.29/30.42 & ~ p44(Y) ) % 30.29/30.42 | ( p44(Y) % 30.29/30.42 & p43(Y) ) % 30.29/30.42 | ( ~ p42(Y) % 30.29/30.42 & ~ p43(Y) ) % 30.29/30.42 | ( p43(Y) % 30.29/30.42 & p42(Y) ) % 30.29/30.42 | ( ~ p41(Y) % 30.29/30.42 & ~ p42(Y) ) % 30.29/30.42 | ( p42(Y) % 30.29/30.42 & p41(Y) ) % 30.29/30.42 | ( ~ p40(Y) % 30.29/30.42 & ~ p41(Y) ) % 30.29/30.42 | ( p41(Y) % 30.29/30.42 & p40(Y) ) % 30.29/30.42 | ( ~ p39(Y) % 30.29/30.42 & ~ p40(Y) ) % 30.29/30.42 | ( p40(Y) % 30.29/30.42 & p39(Y) ) % 30.29/30.42 | ( ~ p38(Y) % 30.29/30.42 & ~ p39(Y) ) % 30.29/30.42 | ( p39(Y) % 30.29/30.42 & p38(Y) ) % 30.29/30.42 | ( ~ p37(Y) % 30.29/30.42 & ~ p38(Y) ) % 30.29/30.42 | ( p38(Y) % 30.29/30.42 & p37(Y) ) % 30.29/30.42 | ( ~ p36(Y) % 30.29/30.42 & ~ p37(Y) ) % 30.29/30.42 | ( p37(Y) % 30.29/30.42 & p36(Y) ) % 30.29/30.42 | ( ~ p35(Y) % 30.29/30.42 & ~ p36(Y) ) % 30.29/30.42 | ( p36(Y) % 30.29/30.42 & p35(Y) ) % 30.29/30.42 | ( ~ p34(Y) % 30.29/30.42 & ~ p35(Y) ) % 30.29/30.42 | ( p35(Y) % 30.29/30.42 & p34(Y) ) % 30.29/30.42 | ( ~ p33(Y) % 30.29/30.42 & ~ p34(Y) ) % 30.29/30.42 | ( p34(Y) % 30.29/30.42 & p33(Y) ) % 30.29/30.42 | ( ~ p32(Y) % 30.29/30.42 & ~ p33(Y) ) % 30.29/30.42 | ( p33(Y) % 30.29/30.42 & p32(Y) ) % 30.29/30.42 | ( ~ p31(Y) % 30.29/30.42 & ~ p32(Y) ) % 30.29/30.42 | ( p32(Y) % 30.29/30.42 & p31(Y) ) % 30.29/30.42 | ( ~ p30(Y) % 30.29/30.42 & ~ p31(Y) ) % 30.29/30.42 | ( p31(Y) % 30.29/30.42 & p30(Y) ) % 30.29/30.42 | ( ~ p29(Y) % 30.29/30.42 & ~ p30(Y) ) % 30.29/30.42 | ( p30(Y) % 30.29/30.42 & p29(Y) ) % 30.29/30.42 | ( ~ p28(Y) % 30.29/30.42 & ~ p29(Y) ) % 30.29/30.42 | ( p29(Y) % 30.29/30.42 & p28(Y) ) % 30.29/30.42 | ( ~ p27(Y) % 30.29/30.42 & ~ p28(Y) ) % 30.29/30.42 | ( p28(Y) % 30.29/30.42 & p27(Y) ) % 30.29/30.42 | ( ~ p26(Y) % 30.29/30.42 & ~ p27(Y) ) % 30.29/30.42 | ( p27(Y) % 30.29/30.42 & p26(Y) ) % 30.29/30.42 | ( ~ p25(Y) % 30.29/30.42 & ~ p26(Y) ) % 30.29/30.42 | ( p26(Y) % 30.29/30.42 & p25(Y) ) % 30.29/30.42 | ( ~ p24(Y) % 30.29/30.42 & ~ p25(Y) ) % 30.29/30.42 | ( p25(Y) % 30.29/30.42 & p24(Y) ) % 30.29/30.42 | ( ~ p23(Y) % 30.29/30.42 & ~ p24(Y) ) % 30.29/30.42 | ( p24(Y) % 30.29/30.42 & p23(Y) ) % 30.29/30.42 | ( ~ p22(Y) % 30.29/30.42 & ~ p23(Y) ) % 30.29/30.42 | ( p23(Y) % 30.29/30.42 & p22(Y) ) % 30.29/30.42 | ( ~ p21(Y) % 30.29/30.42 & ~ p22(Y) ) % 30.29/30.42 | ( p22(Y) % 30.29/30.42 & p21(Y) ) % 30.29/30.42 | ( ~ p20(Y) % 30.29/30.42 & ~ p21(Y) ) % 30.29/30.42 | ( p21(Y) % 30.29/30.42 & p20(Y) ) % 30.29/30.42 | ( ~ p19(Y) % 30.29/30.42 & ~ p20(Y) ) % 30.29/30.42 | ( p20(Y) % 30.29/30.42 & p19(Y) ) % 30.29/30.42 | ( ~ p18(Y) % 30.29/30.42 & ~ p19(Y) ) % 30.29/30.42 | ( p19(Y) % 30.29/30.42 & p18(Y) ) % 30.29/30.42 | ( ~ p17(Y) % 30.29/30.42 & ~ p18(Y) ) % 30.29/30.42 | ( p18(Y) % 30.29/30.42 & p17(Y) ) % 30.29/30.42 | ( ~ p16(Y) % 30.29/30.42 & ~ p17(Y) ) % 30.29/30.42 | ( p17(Y) % 30.29/30.42 & p16(Y) ) % 30.29/30.42 | ( ~ p15(Y) % 30.29/30.42 & ~ p16(Y) ) % 30.29/30.42 | ( p16(Y) % 30.29/30.42 & p15(Y) ) % 30.29/30.42 | ( ~ p14(Y) % 30.29/30.42 & ~ p15(Y) ) % 30.29/30.42 | ( p15(Y) % 30.29/30.42 & p14(Y) ) % 30.29/30.42 | ( ~ p13(Y) % 30.29/30.42 & ~ p14(Y) ) % 30.29/30.42 | ( p14(Y) % 30.29/30.42 & p13(Y) ) % 30.29/30.42 | ( ~ p12(Y) % 30.29/30.42 & ~ p13(Y) ) % 30.29/30.42 | ( p13(Y) % 30.29/30.42 & p12(Y) ) % 30.29/30.42 | ( ~ p11(Y) % 30.29/30.42 & ~ p12(Y) ) % 30.29/30.42 | ( p12(Y) % 30.29/30.42 & p11(Y) ) % 30.29/30.42 | ( ~ p10(Y) % 30.29/30.42 & ~ p11(Y) ) % 30.29/30.42 | ( p11(Y) % 30.29/30.42 & p10(Y) ) % 30.29/30.42 | ( ~ p9(Y) % 30.29/30.42 & ~ p10(Y) ) % 30.29/30.42 | ( p10(Y) % 30.29/30.42 & p9(Y) ) % 30.29/30.42 | ( ~ p8(Y) % 30.29/30.42 & ~ p9(Y) ) % 30.29/30.42 | ( p9(Y) % 30.29/30.42 & p8(Y) ) % 30.29/30.42 | ( ~ p7(Y) % 30.29/30.42 & ~ p8(Y) ) % 30.29/30.42 | ( p8(Y) % 30.29/30.42 & p7(Y) ) % 30.29/30.42 | ( ~ p6(Y) % 30.29/30.42 & ~ p7(Y) ) % 30.29/30.42 | ( p7(Y) % 30.29/30.42 & p6(Y) ) % 30.29/30.42 | ( ~ p5(Y) % 30.29/30.42 & ~ p6(Y) ) % 30.29/30.42 | ( p6(Y) % 30.29/30.42 & p5(Y) ) % 30.29/30.42 | ( ~ p4(Y) % 30.29/30.42 & ~ p5(Y) ) % 30.29/30.42 | ( p5(Y) % 30.29/30.42 & p4(Y) ) % 30.29/30.42 | ( ~ p3(Y) % 30.29/30.42 & ~ p4(Y) ) % 30.29/30.42 | ( p4(Y) % 30.29/30.42 & p3(Y) ) % 30.29/30.42 | ( ~ p2(Y) % 30.29/30.42 & ~ p3(Y) ) % 30.29/30.42 | ( p3(Y) % 30.29/30.42 & p2(Y) ) % 30.29/30.42 | ( ~ p1(Y) % 30.29/30.42 & ~ p2(Y) ) % 30.29/30.42 | ( p2(Y) % 30.29/30.42 & p1(Y) ) ) ) ) ) ) ). % 30.29/30.42 % 30.29/30.42 %------------------------------------------------------------------------------ % 30.29/30.42 %------------------------------------------- % 30.29/30.42 % Proof found % 30.29/30.42 % SZS status Theorem for theBenchmark % 30.29/30.42 % SZS output start Proof % 30.29/30.42 %ClaNum:301(EqnAxiom:0) % 30.29/30.42 %VarNum:1120(SingletonVarNum:414) % 30.29/30.42 %MaxLitNum:4 % 30.29/30.42 %MaxfuncDepth:1 % 30.29/30.42 %SharedTerms:9 % 30.29/30.42 %goalClause: 1 2 3 4 5 8 % 30.29/30.42 %singleGoalClaCount:5 % 30.29/30.42 [1]P1(a1) % 30.29/30.42 [2]P2(a23) % 30.29/30.42 [3]P59(a2,a1) % 30.29/30.42 [4]P59(a2,a34) % 30.29/30.42 [5]P59(a1,a23) % 30.29/30.42 [6]P59(x61,x61) % 30.29/30.42 [8]P3(x81)+~P59(a34,x81) % 30.29/30.42 [7]~P3(x71)+~P1(f45(x71)) % 30.29/30.42 [9]~P3(x91)+P59(x91,f46(x91)) % 30.29/30.42 [10]~P3(x101)+P59(x101,f45(x101)) % 30.29/30.42 [11]~P3(x111)+P59(x111,f60(x111)) % 30.29/30.42 [70]~P3(x701)+P59(f46(x701),f61(x701)) % 30.29/30.42 [71]~P3(x711)+P59(f61(x711),f62(x711)) % 30.29/30.42 [72]~P3(x721)+P59(f62(x721),f63(x721)) % 30.29/30.42 [73]~P3(x731)+P59(f63(x731),f64(x731)) % 30.29/30.42 [74]~P3(x741)+P59(f64(x741),f3(x741)) % 30.29/30.42 [75]~P3(x751)+P59(f3(x751),f4(x751)) % 30.29/30.42 [76]~P3(x761)+P59(f4(x761),f5(x761)) % 30.29/30.42 [77]~P3(x771)+P59(f5(x771),f6(x771)) % 30.29/30.42 [78]~P3(x781)+P59(f6(x781),f7(x781)) % 30.29/30.42 [79]~P3(x791)+P59(f7(x791),f8(x791)) % 30.29/30.43 [80]~P3(x801)+P59(f8(x801),f9(x801)) % 30.29/30.43 [81]~P3(x811)+P59(f9(x811),f10(x811)) % 30.29/30.43 [82]~P3(x821)+P59(f10(x821),f11(x821)) % 30.29/30.43 [83]~P3(x831)+P59(f11(x831),f12(x831)) % 30.29/30.43 [84]~P3(x841)+P59(f12(x841),f13(x841)) % 30.29/30.43 [85]~P3(x851)+P59(f13(x851),f14(x851)) % 30.29/30.43 [86]~P3(x861)+P59(f14(x861),f15(x861)) % 30.29/30.43 [87]~P3(x871)+P59(f15(x871),f16(x871)) % 30.29/30.43 [88]~P3(x881)+P59(f16(x881),f17(x881)) % 30.29/30.43 [89]~P3(x891)+P59(f17(x891),f18(x891)) % 30.29/30.43 [90]~P3(x901)+P59(f18(x901),f19(x901)) % 30.29/30.43 [91]~P3(x911)+P59(f19(x911),f20(x911)) % 30.29/30.43 [92]~P3(x921)+P59(f20(x921),f21(x921)) % 30.29/30.43 [93]~P3(x931)+P59(f21(x931),f22(x931)) % 30.29/30.43 [94]~P3(x941)+P59(f22(x941),f24(x941)) % 30.29/30.43 [95]~P3(x951)+P59(f24(x951),f25(x951)) % 30.29/30.43 [96]~P3(x961)+P59(f25(x961),f26(x961)) % 30.29/30.43 [97]~P3(x971)+P59(f26(x971),f27(x971)) % 30.29/30.43 [98]~P3(x981)+P59(f27(x981),f28(x981)) % 30.29/30.43 [99]~P3(x991)+P59(f28(x991),f29(x991)) % 30.29/30.43 [100]~P3(x1001)+P59(f29(x1001),f30(x1001)) % 30.29/30.43 [101]~P3(x1011)+P59(f30(x1011),f31(x1011)) % 30.29/30.43 [102]~P3(x1021)+P59(f31(x1021),f32(x1021)) % 30.29/30.43 [103]~P3(x1031)+P59(f32(x1031),f33(x1031)) % 30.29/30.43 [104]~P3(x1041)+P59(f33(x1041),f35(x1041)) % 30.29/30.43 [105]~P3(x1051)+P59(f35(x1051),f36(x1051)) % 30.29/30.43 [106]~P3(x1061)+P59(f36(x1061),f37(x1061)) % 30.29/30.43 [107]~P3(x1071)+P59(f37(x1071),f38(x1071)) % 30.29/30.43 [108]~P3(x1081)+P59(f38(x1081),f39(x1081)) % 30.29/30.43 [109]~P3(x1091)+P59(f39(x1091),f40(x1091)) % 30.29/30.43 [110]~P3(x1101)+P59(f40(x1101),f41(x1101)) % 30.29/30.43 [111]~P3(x1111)+P59(f41(x1111),f42(x1111)) % 30.29/30.43 [112]~P3(x1121)+P59(f42(x1121),f43(x1121)) % 30.29/30.43 [113]~P3(x1131)+P59(f43(x1131),f44(x1131)) % 30.29/30.43 [114]~P3(x1141)+P59(f44(x1141),f47(x1141)) % 30.29/30.43 [115]~P3(x1151)+P59(f47(x1151),f48(x1151)) % 30.29/30.43 [116]~P3(x1161)+P59(f48(x1161),f49(x1161)) % 30.29/30.43 [117]~P3(x1171)+P59(f49(x1171),f50(x1171)) % 30.29/30.43 [118]~P3(x1181)+P59(f50(x1181),f51(x1181)) % 30.29/30.43 [119]~P3(x1191)+P59(f51(x1191),f52(x1191)) % 30.29/30.43 [120]~P3(x1201)+P59(f52(x1201),f53(x1201)) % 30.29/30.43 [121]~P3(x1211)+P59(f53(x1211),f54(x1211)) % 30.29/30.43 [122]~P3(x1221)+P59(f54(x1221),f55(x1221)) % 30.29/30.43 [123]~P3(x1231)+P59(f55(x1231),f56(x1231)) % 30.29/30.43 [124]~P3(x1241)+P59(f56(x1241),f57(x1241)) % 30.29/30.43 [125]~P3(x1251)+P59(f57(x1251),f58(x1251)) % 30.29/30.43 [126]~P3(x1261)+P59(f58(x1261),f59(x1261)) % 30.29/30.43 [12]~P3(x121)+P2(f60(x121))+P4(f60(x121)) % 30.29/30.43 [13]~P3(x131)+P15(f60(x131))+P16(f60(x131)) % 30.29/30.43 [14]~P3(x141)+P16(f60(x141))+P17(f60(x141)) % 30.29/30.43 [15]~P3(x151)+P17(f60(x151))+P18(f60(x151)) % 30.29/30.43 [16]~P3(x161)+P18(f60(x161))+P19(f60(x161)) % 30.29/30.43 [17]~P3(x171)+P19(f60(x171))+P20(f60(x171)) % 30.29/30.43 [18]~P3(x181)+P20(f60(x181))+P21(f60(x181)) % 30.29/30.43 [19]~P3(x191)+P21(f60(x191))+P22(f60(x191)) % 30.29/30.43 [20]~P3(x201)+P22(f60(x201))+P23(f60(x201)) % 30.29/30.43 [21]~P3(x211)+P23(f60(x211))+P24(f60(x211)) % 30.29/30.43 [22]~P3(x221)+P24(f60(x221))+P25(f60(x221)) % 30.29/30.43 [23]~P3(x231)+P25(f60(x231))+P26(f60(x231)) % 30.29/30.43 [24]~P3(x241)+P26(f60(x241))+P27(f60(x241)) % 30.29/30.43 [25]~P3(x251)+P27(f60(x251))+P28(f60(x251)) % 30.29/30.43 [26]~P3(x261)+P28(f60(x261))+P29(f60(x261)) % 30.29/30.43 [27]~P3(x271)+P29(f60(x271))+P30(f60(x271)) % 30.29/30.43 [28]~P3(x281)+P30(f60(x281))+P31(f60(x281)) % 30.29/30.43 [29]~P3(x291)+P31(f60(x291))+P32(f60(x291)) % 30.29/30.43 [30]~P3(x301)+P32(f60(x301))+P33(f60(x301)) % 30.29/30.43 [31]~P3(x311)+P33(f60(x311))+P34(f60(x311)) % 30.29/30.43 [32]~P3(x321)+P34(f60(x321))+P35(f60(x321)) % 30.29/30.43 [33]~P3(x331)+P35(f60(x331))+P36(f60(x331)) % 30.29/30.43 [34]~P3(x341)+P36(f60(x341))+P37(f60(x341)) % 30.29/30.43 [35]~P3(x351)+P37(f60(x351))+P38(f60(x351)) % 30.29/30.43 [36]~P3(x361)+P38(f60(x361))+P39(f60(x361)) % 30.29/30.43 [37]~P3(x371)+P39(f60(x371))+P40(f60(x371)) % 30.29/30.43 [38]~P3(x381)+P40(f60(x381))+P41(f60(x381)) % 30.29/30.43 [39]~P3(x391)+P41(f60(x391))+P42(f60(x391)) % 30.29/30.43 [40]~P3(x401)+P42(f60(x401))+P43(f60(x401)) % 30.29/30.43 [41]~P3(x411)+P43(f60(x411))+P44(f60(x411)) % 30.29/30.43 [42]~P3(x421)+P44(f60(x421))+P45(f60(x421)) % 30.29/30.43 [43]~P3(x431)+P45(f60(x431))+P46(f60(x431)) % 30.29/30.43 [44]~P3(x441)+P46(f60(x441))+P47(f60(x441)) % 30.29/30.43 [45]~P3(x451)+P47(f60(x451))+P48(f60(x451)) % 30.29/30.43 [46]~P3(x461)+P48(f60(x461))+P49(f60(x461)) % 30.29/30.43 [47]~P3(x471)+P49(f60(x471))+P50(f60(x471)) % 30.29/30.43 [48]~P3(x481)+P50(f60(x481))+P51(f60(x481)) % 30.29/30.43 [49]~P3(x491)+P51(f60(x491))+P52(f60(x491)) % 30.29/30.43 [50]~P3(x501)+P52(f60(x501))+P53(f60(x501)) % 30.29/30.43 [51]~P3(x511)+P53(f60(x511))+P54(f60(x511)) % 30.29/30.43 [52]~P3(x521)+P54(f60(x521))+P5(f60(x521)) % 30.29/30.43 [53]~P3(x531)+P5(f60(x531))+P6(f60(x531)) % 30.29/30.43 [54]~P3(x541)+P6(f60(x541))+P7(f60(x541)) % 30.29/30.43 [55]~P3(x551)+P7(f60(x551))+P8(f60(x551)) % 30.29/30.43 [56]~P3(x561)+P8(f60(x561))+P9(f60(x561)) % 30.29/30.43 [57]~P3(x571)+P9(f60(x571))+P10(f60(x571)) % 30.29/30.43 [58]~P3(x581)+P10(f60(x581))+P11(f60(x581)) % 30.29/30.43 [59]~P3(x591)+P11(f60(x591))+P12(f60(x591)) % 30.29/30.43 [60]~P3(x601)+P12(f60(x601))+P13(f60(x601)) % 30.29/30.43 [61]~P3(x611)+P13(f60(x611))+P14(f60(x611)) % 30.29/30.43 [62]~P3(x621)+P14(f60(x621))+P60(f60(x621)) % 30.29/30.43 [63]~P3(x631)+P60(f60(x631))+P61(f60(x631)) % 30.29/30.43 [64]~P3(x641)+P61(f60(x641))+P62(f60(x641)) % 30.29/30.43 [65]~P3(x651)+P62(f60(x651))+P58(f60(x651)) % 30.29/30.43 [66]~P3(x661)+P58(f60(x661))+P57(f60(x661)) % 30.29/30.43 [67]~P3(x671)+P57(f60(x671))+P56(f60(x671)) % 30.29/30.43 [68]~P3(x681)+P56(f60(x681))+P55(f60(x681)) % 30.29/30.43 [69]~P3(x691)+P55(f60(x691))+P4(f60(x691)) % 30.29/30.43 [127]~P3(x1271)+~P2(f60(x1271))+~P4(f60(x1271)) % 30.29/30.43 [128]~P3(x1281)+~P15(f60(x1281))+~P16(f60(x1281)) % 30.29/30.43 [129]~P3(x1291)+~P16(f60(x1291))+~P17(f60(x1291)) % 30.29/30.43 [130]~P3(x1301)+~P17(f60(x1301))+~P18(f60(x1301)) % 30.29/30.43 [131]~P3(x1311)+~P18(f60(x1311))+~P19(f60(x1311)) % 30.29/30.43 [132]~P3(x1321)+~P19(f60(x1321))+~P20(f60(x1321)) % 30.29/30.43 [133]~P3(x1331)+~P20(f60(x1331))+~P21(f60(x1331)) % 30.29/30.43 [134]~P3(x1341)+~P21(f60(x1341))+~P22(f60(x1341)) % 30.29/30.43 [135]~P3(x1351)+~P22(f60(x1351))+~P23(f60(x1351)) % 30.29/30.43 [136]~P3(x1361)+~P23(f60(x1361))+~P24(f60(x1361)) % 30.29/30.43 [137]~P3(x1371)+~P24(f60(x1371))+~P25(f60(x1371)) % 30.29/30.43 [138]~P3(x1381)+~P25(f60(x1381))+~P26(f60(x1381)) % 30.29/30.43 [139]~P3(x1391)+~P26(f60(x1391))+~P27(f60(x1391)) % 30.29/30.43 [140]~P3(x1401)+~P27(f60(x1401))+~P28(f60(x1401)) % 30.29/30.43 [141]~P3(x1411)+~P28(f60(x1411))+~P29(f60(x1411)) % 30.29/30.43 [142]~P3(x1421)+~P29(f60(x1421))+~P30(f60(x1421)) % 30.29/30.43 [143]~P3(x1431)+~P30(f60(x1431))+~P31(f60(x1431)) % 30.29/30.43 [144]~P3(x1441)+~P31(f60(x1441))+~P32(f60(x1441)) % 30.29/30.43 [145]~P3(x1451)+~P32(f60(x1451))+~P33(f60(x1451)) % 30.29/30.43 [146]~P3(x1461)+~P33(f60(x1461))+~P34(f60(x1461)) % 30.29/30.43 [147]~P3(x1471)+~P34(f60(x1471))+~P35(f60(x1471)) % 30.29/30.43 [148]~P3(x1481)+~P35(f60(x1481))+~P36(f60(x1481)) % 30.29/30.43 [149]~P3(x1491)+~P36(f60(x1491))+~P37(f60(x1491)) % 30.29/30.43 [150]~P3(x1501)+~P37(f60(x1501))+~P38(f60(x1501)) % 30.29/30.43 [151]~P3(x1511)+~P38(f60(x1511))+~P39(f60(x1511)) % 30.29/30.43 [152]~P3(x1521)+~P39(f60(x1521))+~P40(f60(x1521)) % 30.29/30.43 [153]~P3(x1531)+~P40(f60(x1531))+~P41(f60(x1531)) % 30.29/30.43 [154]~P3(x1541)+~P41(f60(x1541))+~P42(f60(x1541)) % 30.29/30.43 [155]~P3(x1551)+~P42(f60(x1551))+~P43(f60(x1551)) % 30.29/30.43 [156]~P3(x1561)+~P43(f60(x1561))+~P44(f60(x1561)) % 30.29/30.43 [157]~P3(x1571)+~P44(f60(x1571))+~P45(f60(x1571)) % 30.29/30.43 [158]~P3(x1581)+~P45(f60(x1581))+~P46(f60(x1581)) % 30.29/30.43 [159]~P3(x1591)+~P46(f60(x1591))+~P47(f60(x1591)) % 30.29/30.43 [160]~P3(x1601)+~P47(f60(x1601))+~P48(f60(x1601)) % 30.29/30.43 [161]~P3(x1611)+~P48(f60(x1611))+~P49(f60(x1611)) % 30.29/30.43 [162]~P3(x1621)+~P49(f60(x1621))+~P50(f60(x1621)) % 30.29/30.43 [163]~P3(x1631)+~P50(f60(x1631))+~P51(f60(x1631)) % 30.29/30.43 [164]~P3(x1641)+~P51(f60(x1641))+~P52(f60(x1641)) % 30.29/30.43 [165]~P3(x1651)+~P52(f60(x1651))+~P53(f60(x1651)) % 30.29/30.43 [166]~P3(x1661)+~P53(f60(x1661))+~P54(f60(x1661)) % 30.29/30.43 [167]~P3(x1671)+~P54(f60(x1671))+~P5(f60(x1671)) % 30.29/30.43 [168]~P3(x1681)+~P5(f60(x1681))+~P6(f60(x1681)) % 30.29/30.43 [169]~P3(x1691)+~P6(f60(x1691))+~P7(f60(x1691)) % 30.29/30.43 [170]~P3(x1701)+~P7(f60(x1701))+~P8(f60(x1701)) % 30.29/30.43 [171]~P3(x1711)+~P8(f60(x1711))+~P9(f60(x1711)) % 30.29/30.43 [172]~P3(x1721)+~P9(f60(x1721))+~P10(f60(x1721)) % 30.29/30.43 [173]~P3(x1731)+~P10(f60(x1731))+~P11(f60(x1731)) % 30.29/30.43 [174]~P3(x1741)+~P11(f60(x1741))+~P12(f60(x1741)) % 30.29/30.43 [175]~P3(x1751)+~P12(f60(x1751))+~P13(f60(x1751)) % 30.29/30.43 [176]~P3(x1761)+~P13(f60(x1761))+~P14(f60(x1761)) % 30.29/30.43 [177]~P3(x1771)+~P14(f60(x1771))+~P60(f60(x1771)) % 30.29/30.43 [178]~P3(x1781)+~P60(f60(x1781))+~P61(f60(x1781)) % 30.29/30.43 [179]~P3(x1791)+~P61(f60(x1791))+~P62(f60(x1791)) % 30.29/30.43 [180]~P3(x1801)+~P62(f60(x1801))+~P58(f60(x1801)) % 30.29/30.43 [181]~P3(x1811)+~P58(f60(x1811))+~P57(f60(x1811)) % 30.29/30.43 [182]~P3(x1821)+~P57(f60(x1821))+~P56(f60(x1821)) % 30.29/30.43 [183]~P3(x1831)+~P56(f60(x1831))+~P55(f60(x1831)) % 30.29/30.43 [184]~P3(x1841)+~P55(f60(x1841))+~P4(f60(x1841)) % 30.29/30.43 [301]~P59(x3011,x3013)+P59(x3011,x3012)+~P59(x3013,x3012) % 30.29/30.43 [185]~P4(x1851)+~P59(x1852,x1851)+P2(x1851)+~P3(x1852) % 30.29/30.43 [186]~P2(x1861)+~P59(x1862,x1861)+P4(x1861)+~P3(x1862) % 30.29/30.43 [187]~P16(x1871)+P15(x1871)+~P3(x1872)+~P59(f58(x1872),x1871) % 30.29/30.43 [188]~P15(x1881)+P16(x1881)+~P3(x1882)+~P59(f58(x1882),x1881) % 30.29/30.43 [189]~P17(x1891)+P16(x1891)+~P3(x1892)+~P59(f57(x1892),x1891) % 30.29/30.43 [190]~P16(x1901)+P17(x1901)+~P3(x1902)+~P59(f57(x1902),x1901) % 30.29/30.43 [191]~P18(x1911)+P17(x1911)+~P3(x1912)+~P59(f56(x1912),x1911) % 30.29/30.43 [192]~P17(x1921)+P18(x1921)+~P3(x1922)+~P59(f56(x1922),x1921) % 30.29/30.43 [193]~P19(x1931)+P18(x1931)+~P3(x1932)+~P59(f55(x1932),x1931) % 30.29/30.43 [194]~P18(x1941)+P19(x1941)+~P3(x1942)+~P59(f55(x1942),x1941) % 30.29/30.43 [195]~P20(x1951)+P19(x1951)+~P3(x1952)+~P59(f54(x1952),x1951) % 30.29/30.43 [196]~P19(x1961)+P20(x1961)+~P3(x1962)+~P59(f54(x1962),x1961) % 30.29/30.43 [197]~P21(x1971)+P20(x1971)+~P3(x1972)+~P59(f53(x1972),x1971) % 30.29/30.43 [198]~P20(x1981)+P21(x1981)+~P3(x1982)+~P59(f53(x1982),x1981) % 30.29/30.43 [199]~P22(x1991)+P21(x1991)+~P3(x1992)+~P59(f52(x1992),x1991) % 30.29/30.43 [200]~P21(x2001)+P22(x2001)+~P3(x2002)+~P59(f52(x2002),x2001) % 30.29/30.43 [201]~P23(x2011)+P22(x2011)+~P3(x2012)+~P59(f51(x2012),x2011) % 30.29/30.43 [202]~P22(x2021)+P23(x2021)+~P3(x2022)+~P59(f51(x2022),x2021) % 30.29/30.43 [203]~P24(x2031)+P23(x2031)+~P3(x2032)+~P59(f50(x2032),x2031) % 30.29/30.43 [204]~P23(x2041)+P24(x2041)+~P3(x2042)+~P59(f50(x2042),x2041) % 30.29/30.43 [205]~P25(x2051)+P24(x2051)+~P3(x2052)+~P59(f49(x2052),x2051) % 30.29/30.43 [206]~P24(x2061)+P25(x2061)+~P3(x2062)+~P59(f49(x2062),x2061) % 30.29/30.43 [207]~P26(x2071)+P25(x2071)+~P3(x2072)+~P59(f48(x2072),x2071) % 30.29/30.43 [208]~P25(x2081)+P26(x2081)+~P3(x2082)+~P59(f48(x2082),x2081) % 30.29/30.43 [209]~P27(x2091)+P26(x2091)+~P3(x2092)+~P59(f47(x2092),x2091) % 30.29/30.43 [210]~P26(x2101)+P27(x2101)+~P3(x2102)+~P59(f47(x2102),x2101) % 30.29/30.43 [211]~P28(x2111)+P27(x2111)+~P3(x2112)+~P59(f44(x2112),x2111) % 30.29/30.43 [212]~P27(x2121)+P28(x2121)+~P3(x2122)+~P59(f44(x2122),x2121) % 30.29/30.43 [213]~P29(x2131)+P28(x2131)+~P3(x2132)+~P59(f43(x2132),x2131) % 30.29/30.43 [214]~P28(x2141)+P29(x2141)+~P3(x2142)+~P59(f43(x2142),x2141) % 30.29/30.43 [215]~P30(x2151)+P29(x2151)+~P3(x2152)+~P59(f42(x2152),x2151) % 30.29/30.43 [216]~P29(x2161)+P30(x2161)+~P3(x2162)+~P59(f42(x2162),x2161) % 30.29/30.43 [217]~P31(x2171)+P30(x2171)+~P3(x2172)+~P59(f41(x2172),x2171) % 30.29/30.43 [218]~P30(x2181)+P31(x2181)+~P3(x2182)+~P59(f41(x2182),x2181) % 30.29/30.43 [219]~P32(x2191)+P31(x2191)+~P3(x2192)+~P59(f40(x2192),x2191) % 30.29/30.43 [220]~P31(x2201)+P32(x2201)+~P3(x2202)+~P59(f40(x2202),x2201) % 30.29/30.43 [221]~P33(x2211)+P32(x2211)+~P3(x2212)+~P59(f39(x2212),x2211) % 30.29/30.43 [222]~P32(x2221)+P33(x2221)+~P3(x2222)+~P59(f39(x2222),x2221) % 30.29/30.43 [223]~P34(x2231)+P33(x2231)+~P3(x2232)+~P59(f38(x2232),x2231) % 30.29/30.43 [224]~P33(x2241)+P34(x2241)+~P3(x2242)+~P59(f38(x2242),x2241) % 30.29/30.43 [225]~P35(x2251)+P34(x2251)+~P3(x2252)+~P59(f37(x2252),x2251) % 30.29/30.43 [226]~P34(x2261)+P35(x2261)+~P3(x2262)+~P59(f37(x2262),x2261) % 30.29/30.43 [227]~P36(x2271)+P35(x2271)+~P3(x2272)+~P59(f36(x2272),x2271) % 30.29/30.43 [228]~P35(x2281)+P36(x2281)+~P3(x2282)+~P59(f36(x2282),x2281) % 30.29/30.43 [229]~P37(x2291)+P36(x2291)+~P3(x2292)+~P59(f35(x2292),x2291) % 30.29/30.43 [230]~P36(x2301)+P37(x2301)+~P3(x2302)+~P59(f35(x2302),x2301) % 30.29/30.43 [231]~P38(x2311)+P37(x2311)+~P3(x2312)+~P59(f33(x2312),x2311) % 30.29/30.43 [232]~P37(x2321)+P38(x2321)+~P3(x2322)+~P59(f33(x2322),x2321) % 30.29/30.43 [233]~P39(x2331)+P38(x2331)+~P3(x2332)+~P59(f32(x2332),x2331) % 30.29/30.43 [234]~P38(x2341)+P39(x2341)+~P3(x2342)+~P59(f32(x2342),x2341) % 30.29/30.43 [235]~P40(x2351)+P39(x2351)+~P3(x2352)+~P59(f31(x2352),x2351) % 30.29/30.43 [236]~P39(x2361)+P40(x2361)+~P3(x2362)+~P59(f31(x2362),x2361) % 30.29/30.43 [237]~P41(x2371)+P40(x2371)+~P3(x2372)+~P59(f30(x2372),x2371) % 30.29/30.43 [238]~P40(x2381)+P41(x2381)+~P3(x2382)+~P59(f30(x2382),x2381) % 30.29/30.43 [239]~P42(x2391)+P41(x2391)+~P3(x2392)+~P59(f29(x2392),x2391) % 30.29/30.43 [240]~P41(x2401)+P42(x2401)+~P3(x2402)+~P59(f29(x2402),x2401) % 30.29/30.43 [241]~P43(x2411)+P42(x2411)+~P3(x2412)+~P59(f28(x2412),x2411) % 30.29/30.43 [242]~P42(x2421)+P43(x2421)+~P3(x2422)+~P59(f28(x2422),x2421) % 30.29/30.43 [243]~P44(x2431)+P43(x2431)+~P3(x2432)+~P59(f27(x2432),x2431) % 30.29/30.43 [244]~P43(x2441)+P44(x2441)+~P3(x2442)+~P59(f27(x2442),x2441) % 30.29/30.43 [245]~P45(x2451)+P44(x2451)+~P3(x2452)+~P59(f26(x2452),x2451) % 30.29/30.43 [246]~P44(x2461)+P45(x2461)+~P3(x2462)+~P59(f26(x2462),x2461) % 30.29/30.43 [247]~P46(x2471)+P45(x2471)+~P3(x2472)+~P59(f25(x2472),x2471) % 30.29/30.43 [248]~P45(x2481)+P46(x2481)+~P3(x2482)+~P59(f25(x2482),x2481) % 30.29/30.43 [249]~P47(x2491)+P46(x2491)+~P3(x2492)+~P59(f24(x2492),x2491) % 30.29/30.43 [250]~P46(x2501)+P47(x2501)+~P3(x2502)+~P59(f24(x2502),x2501) % 30.29/30.43 [251]~P48(x2511)+P47(x2511)+~P3(x2512)+~P59(f22(x2512),x2511) % 30.29/30.43 [252]~P47(x2521)+P48(x2521)+~P3(x2522)+~P59(f22(x2522),x2521) % 30.29/30.43 [253]~P49(x2531)+P48(x2531)+~P3(x2532)+~P59(f21(x2532),x2531) % 30.29/30.43 [254]~P48(x2541)+P49(x2541)+~P3(x2542)+~P59(f21(x2542),x2541) % 30.29/30.43 [255]~P50(x2551)+P49(x2551)+~P3(x2552)+~P59(f20(x2552),x2551) % 30.29/30.43 [256]~P49(x2561)+P50(x2561)+~P3(x2562)+~P59(f20(x2562),x2561) % 30.29/30.43 [257]~P51(x2571)+P50(x2571)+~P3(x2572)+~P59(f19(x2572),x2571) % 30.29/30.43 [258]~P50(x2581)+P51(x2581)+~P3(x2582)+~P59(f19(x2582),x2581) % 30.29/30.43 [259]~P52(x2591)+P51(x2591)+~P3(x2592)+~P59(f18(x2592),x2591) % 30.29/30.43 [260]~P51(x2601)+P52(x2601)+~P3(x2602)+~P59(f18(x2602),x2601) % 30.29/30.43 [261]~P53(x2611)+P52(x2611)+~P3(x2612)+~P59(f17(x2612),x2611) % 30.29/30.43 [262]~P52(x2621)+P53(x2621)+~P3(x2622)+~P59(f17(x2622),x2621) % 30.29/30.43 [263]~P54(x2631)+P53(x2631)+~P3(x2632)+~P59(f16(x2632),x2631) % 30.29/30.43 [264]~P53(x2641)+P54(x2641)+~P3(x2642)+~P59(f16(x2642),x2641) % 30.29/30.43 [265]~P5(x2651)+P54(x2651)+~P3(x2652)+~P59(f15(x2652),x2651) % 30.29/30.43 [266]~P54(x2661)+P5(x2661)+~P3(x2662)+~P59(f15(x2662),x2661) % 30.29/30.43 [267]~P6(x2671)+P5(x2671)+~P3(x2672)+~P59(f14(x2672),x2671) % 30.29/30.43 [268]~P5(x2681)+P6(x2681)+~P3(x2682)+~P59(f14(x2682),x2681) % 30.29/30.43 [269]~P7(x2691)+P6(x2691)+~P3(x2692)+~P59(f13(x2692),x2691) % 30.29/30.43 [270]~P6(x2701)+P7(x2701)+~P3(x2702)+~P59(f13(x2702),x2701) % 30.29/30.43 [271]~P8(x2711)+P7(x2711)+~P3(x2712)+~P59(f12(x2712),x2711) % 30.29/30.43 [272]~P7(x2721)+P8(x2721)+~P3(x2722)+~P59(f12(x2722),x2721) % 30.29/30.43 [273]~P9(x2731)+P8(x2731)+~P3(x2732)+~P59(f11(x2732),x2731) % 30.29/30.43 [274]~P8(x2741)+P9(x2741)+~P3(x2742)+~P59(f11(x2742),x2741) % 30.29/30.43 [275]~P10(x2751)+P9(x2751)+~P3(x2752)+~P59(f10(x2752),x2751) % 30.29/30.43 [276]~P9(x2761)+P10(x2761)+~P3(x2762)+~P59(f10(x2762),x2761) % 30.29/30.43 [277]~P11(x2771)+P10(x2771)+~P3(x2772)+~P59(f9(x2772),x2771) % 30.29/30.43 [278]~P10(x2781)+P11(x2781)+~P3(x2782)+~P59(f9(x2782),x2781) % 30.29/30.43 [279]~P12(x2791)+P11(x2791)+~P3(x2792)+~P59(f8(x2792),x2791) % 30.29/30.43 [280]~P11(x2801)+P12(x2801)+~P3(x2802)+~P59(f8(x2802),x2801) % 30.29/30.43 [281]~P13(x2811)+P12(x2811)+~P3(x2812)+~P59(f7(x2812),x2811) % 30.29/30.43 [282]~P12(x2821)+P13(x2821)+~P3(x2822)+~P59(f7(x2822),x2821) % 30.29/30.43 [283]~P14(x2831)+P13(x2831)+~P3(x2832)+~P59(f6(x2832),x2831) % 30.29/30.43 [284]~P13(x2841)+P14(x2841)+~P3(x2842)+~P59(f6(x2842),x2841) % 30.29/30.43 [285]~P60(x2851)+P14(x2851)+~P3(x2852)+~P59(f5(x2852),x2851) % 30.29/30.43 [286]~P14(x2861)+P60(x2861)+~P3(x2862)+~P59(f5(x2862),x2861) % 30.29/30.43 [287]~P61(x2871)+P60(x2871)+~P3(x2872)+~P59(f4(x2872),x2871) % 30.29/30.43 [288]~P60(x2881)+P61(x2881)+~P3(x2882)+~P59(f4(x2882),x2881) % 30.29/30.43 [289]~P62(x2891)+P61(x2891)+~P3(x2892)+~P59(f3(x2892),x2891) % 30.29/30.43 [290]~P61(x2901)+P62(x2901)+~P3(x2902)+~P59(f3(x2902),x2901) % 30.29/30.43 [291]~P58(x2911)+P62(x2911)+~P3(x2912)+~P59(f64(x2912),x2911) % 30.29/30.43 [292]~P62(x2921)+P58(x2921)+~P3(x2922)+~P59(f64(x2922),x2921) % 30.29/30.43 [293]~P57(x2931)+P58(x2931)+~P3(x2932)+~P59(f63(x2932),x2931) % 30.29/30.43 [294]~P58(x2941)+P57(x2941)+~P3(x2942)+~P59(f63(x2942),x2941) % 30.29/30.43 [295]~P56(x2951)+P57(x2951)+~P3(x2952)+~P59(f62(x2952),x2951) % 30.29/30.43 [296]~P57(x2961)+P56(x2961)+~P3(x2962)+~P59(f62(x2962),x2961) % 30.29/30.43 [297]~P55(x2971)+P56(x2971)+~P3(x2972)+~P59(f61(x2972),x2971) % 30.29/30.43 [298]~P56(x2981)+P55(x2981)+~P3(x2982)+~P59(f61(x2982),x2981) % 30.29/30.43 [299]~P4(x2991)+P55(x2991)+~P3(x2992)+~P59(f46(x2992),x2991) % 30.29/30.43 [300]~P55(x3001)+P4(x3001)+~P3(x3002)+~P59(f46(x3002),x3001) % 30.29/30.43 %EqnAxiom % 30.29/30.43 % 30.29/30.43 %------------------------------------------- % 30.29/30.43 cnf(302,plain, % 30.29/30.43 (P3(a34)), % 30.29/30.43 inference(scs_inference,[],[6,8])). % 30.29/30.43 cnf(544,plain, % 30.29/30.43 (P59(a34,f46(a34))), % 30.29/30.43 inference(scs_inference,[],[6,9,8])). % 30.29/30.43 cnf(545,plain, % 30.29/30.43 (P3(f46(a34))), % 30.29/30.43 inference(scs_inference,[],[544,8])). % 30.29/30.43 cnf(4810,plain, % 30.29/30.43 (P58(f60(f46(a34)))+P57(f60(f46(a34)))), % 30.29/30.43 inference(scs_inference,[],[544,66,8])). % 30.29/30.43 cnf(4811,plain, % 30.29/30.43 (P57(f60(f46(a34)))+~P62(f60(f46(a34)))), % 30.29/30.43 inference(scs_inference,[],[545,4810,180])). % 30.29/30.43 cnf(4812,plain, % 30.29/30.43 (~P62(f60(f46(a34)))+~P58(f60(f46(a34)))), % 30.29/30.43 inference(scs_inference,[],[545,4811,181])). % 30.29/30.43 cnf(4813,plain, % 30.29/30.43 (~P58(f60(f46(a34)))+P61(f60(f46(a34)))), % 30.29/30.43 inference(scs_inference,[],[545,4812,64])). % 30.29/30.43 cnf(4814,plain, % 30.29/30.43 (P61(f60(f46(a34)))+P57(f60(f46(a34)))), % 30.29/30.43 inference(scs_inference,[],[4813,4810])). % 30.29/30.43 cnf(4815,plain, % 30.29/30.43 (P57(f60(f46(a34)))+~P60(f60(f46(a34)))), % 30.29/30.43 inference(scs_inference,[],[545,4814,178])). % 30.29/30.43 cnf(4816,plain, % 30.29/30.43 (~P60(f60(f46(a34)))+~P56(f60(f46(a34)))), % 30.29/30.43 inference(scs_inference,[],[545,4815,182])). % 30.29/30.43 cnf(4817,plain, % 30.29/30.43 (~P56(f60(f46(a34)))+P14(f60(f46(a34)))), % 30.29/30.43 inference(scs_inference,[],[545,4816,62])). % 30.29/30.43 cnf(4818,plain, % 30.29/30.43 (P14(f60(f46(a34)))+P57(f60(f46(a34)))), % 30.29/30.43 inference(scs_inference,[],[545,4817,67])). % 30.29/30.43 cnf(4819,plain, % 30.29/30.43 (P57(f60(f46(a34)))+~P13(f60(f46(a34)))), % 30.29/30.43 inference(scs_inference,[],[545,4818,176])). % 30.29/30.43 cnf(4820,plain, % 30.29/30.43 (~P13(f60(f46(a34)))+~P58(f60(f46(a34)))), % 30.29/30.43 inference(scs_inference,[],[545,4819,181])). % 30.29/30.43 cnf(4821,plain, % 30.29/30.43 (~P58(f60(f46(a34)))+P12(f60(f46(a34)))), % 30.29/30.43 inference(scs_inference,[],[545,4820,60])). % 30.29/30.43 cnf(4822,plain, % 30.29/30.43 (P12(f60(f46(a34)))+P57(f60(f46(a34)))), % 30.29/30.43 inference(scs_inference,[],[4821,4810])). % 30.29/30.43 cnf(4823,plain, % 30.29/30.43 (P57(f60(f46(a34)))+~P11(f60(f46(a34)))), % 30.29/30.43 inference(scs_inference,[],[545,4822,174])). % 30.29/30.43 cnf(4824,plain, % 30.29/30.43 (~P11(f60(f46(a34)))+~P56(f60(f46(a34)))), % 30.29/30.43 inference(scs_inference,[],[545,4823,182])). % 30.29/30.43 cnf(4825,plain, % 30.29/30.43 (~P56(f60(f46(a34)))+P10(f60(f46(a34)))), % 30.29/30.43 inference(scs_inference,[],[545,4824,58])). % 30.29/30.43 cnf(4826,plain, % 30.29/30.43 (P10(f60(f46(a34)))+P55(f60(f46(a34)))), % 30.29/30.43 inference(scs_inference,[],[545,4825,68])). % 30.29/30.43 cnf(4827,plain, % 30.29/30.43 (P55(f60(f46(a34)))+~P9(f60(f46(a34)))), % 30.29/30.43 inference(scs_inference,[],[545,4826,172])). % 30.29/30.43 cnf(9900,plain, % 30.29/30.43 (P59(f46(a34),f46(f46(a34)))), % 30.29/30.43 inference(scs_inference,[],[544,8,9])). % 30.29/30.43 cnf(9901,plain, % 30.29/30.43 (P59(a34,f46(f46(a34)))), % 30.29/30.43 inference(scs_inference,[],[544,9900,301])). % 30.29/30.43 cnf(9905,plain, % 30.29/30.43 (P59(f46(a34),f60(f46(a34)))), % 30.29/30.43 inference(scs_inference,[],[544,8,11])). % 30.29/30.43 cnf(9908,plain, % 30.29/30.43 (P55(f60(f46(a34)))+~P4(f60(f46(a34)))), % 30.29/30.43 inference(scs_inference,[],[4,302,9901,9905,301,299])). % 30.29/30.43 cnf(9949,plain, % 30.29/30.43 (P4(f60(f46(a34)))), % 30.29/30.43 inference(scs_inference,[],[544,302,545,9905,301,8,300,4827,57,69])). % 30.29/30.43 cnf(9974,plain, % 30.29/30.43 (P55(f60(f46(a34)))), % 30.29/30.43 inference(scs_inference,[],[9949,9908])). % 30.29/30.43 cnf(9979,plain, % 30.29/30.43 ($false), % 30.29/30.43 inference(scs_inference,[],[545,9949,9974,184]), % 30.29/30.43 ['proof']). % 30.29/30.43 % SZS output end Proof % 30.29/30.43 % Total time :29.807445s %------------------------------------------------------------------------------