%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : PRO009+1 : TPTP v8.2.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % Computer : n028.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Mon Jun 24 13:39:43 EDT 2024 % Result : Theorem 79.20s 79.28s % Output : CNFRefutation 79.20s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : PRO009+1 : TPTP v8.2.0. Released v4.0.0. % 0.03/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.12/0.33 % Computer : n028.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 300 % 0.12/0.33 % DateTime : Thu Jun 20 06:43:09 EDT 2024 % 0.12/0.33 % CPUTime : % 0.51/0.56 start to proof:theBenchmark % 79.20/79.26 %------------------------------------------- % 79.20/79.26 % File :CSE---1.7 % 79.20/79.26 % Problem :theBenchmark % 79.20/79.26 % Transform :cnf % 79.20/79.26 % Format :tptp:raw % 79.20/79.26 % Command :java -jar mcs_scs.jar %d %s % 79.20/79.26 % 79.20/79.26 % Result :Theorem 78.640000s % 79.20/79.26 % Output :CNFRefutation 78.640000s % 79.20/79.26 %------------------------------------------- % 79.20/79.27 %------------------------------------------------------------------------------ % 79.20/79.27 % File : PRO009+1 : TPTP v8.2.0. Released v4.0.0. % 79.20/79.27 % Domain : Processes % 79.20/79.27 % Problem : PSL cliff problem coe-7.1.2 % 79.20/79.27 % Version : Especial. % 79.20/79.27 % English : % 79.20/79.27 % Refs : [Hal09] Halcomb (2009), Email to G. Sutcliffe % 79.20/79.27 % Source : [Hal09] % 79.20/79.27 % Names : psl-subset-1016__coe-7.1.2-pd [Hal09] % 79.20/79.27 % 79.20/79.27 % Status : Theorem % 79.20/79.27 % Rating : 0.31 v8.2.0, 0.28 v8.1.0, 0.25 v7.5.0, 0.28 v7.4.0, 0.30 v7.3.0, 0.24 v7.2.0, 0.21 v7.1.0, 0.26 v7.0.0, 0.20 v6.4.0, 0.23 v6.3.0, 0.29 v6.2.0, 0.36 v6.1.0, 0.53 v6.0.0, 0.43 v5.5.0, 0.52 v5.4.0, 0.50 v5.3.0, 0.48 v5.2.0, 0.35 v5.1.0, 0.43 v5.0.0, 0.42 v4.1.0, 0.39 v4.0.1, 0.43 v4.0.0 % 79.20/79.27 % Syntax : Number of formulae : 49 ( 12 unt; 0 def) % 79.20/79.27 % Number of atoms : 151 ( 9 equ) % 79.20/79.27 % Maximal formula atoms : 9 ( 3 avg) % 79.20/79.27 % Number of connectives : 119 ( 17 ~; 7 |; 57 &) % 79.20/79.27 % ( 7 <=>; 31 =>; 0 <=; 0 <~>) % 79.20/79.27 % Maximal formula depth : 12 ( 5 avg) % 79.20/79.27 % Maximal term depth : 1 ( 1 avg) % 79.20/79.27 % Number of predicates : 18 ( 17 usr; 0 prp; 1-3 aty) % 79.20/79.27 % Number of functors : 5 ( 5 usr; 5 con; 0-0 aty) % 79.20/79.27 % Number of variables : 112 ( 92 !; 20 ?) % 79.20/79.27 % SPC : FOF_THM_RFO_SEQ % 79.20/79.27 % 79.20/79.27 % Comments : % 79.20/79.27 %------------------------------------------------------------------------------ % 79.20/79.27 fof(sos,axiom, % 79.20/79.27 ! [X0,X1] : % 79.20/79.27 ( occurrence_of(X1,X0) % 79.20/79.27 => ( activity(X0) % 79.20/79.27 & activity_occurrence(X1) ) ) ). % 79.20/79.27 % 79.20/79.27 fof(sos_01,axiom, % 79.20/79.27 ! [X2] : % 79.20/79.27 ( activity_occurrence(X2) % 79.20/79.27 => ? [X3] : % 79.20/79.27 ( activity(X3) % 79.20/79.27 & occurrence_of(X2,X3) ) ) ). % 79.20/79.27 % 79.20/79.27 fof(sos_02,axiom, % 79.20/79.27 ! [X4,X5,X6] : % 79.20/79.27 ( ( occurrence_of(X4,X5) % 79.20/79.27 & occurrence_of(X4,X6) ) % 79.20/79.27 => X5 = X6 ) ). % 79.20/79.27 % 79.20/79.27 fof(sos_03,axiom, % 79.20/79.27 ! [X7] : % 79.20/79.27 ( activity(X7) % 79.20/79.27 => subactivity(X7,X7) ) ). % 79.20/79.27 % 79.20/79.27 fof(sos_04,axiom, % 79.20/79.27 ! [X8,X9] : % 79.20/79.27 ( earlier(X8,X9) % 79.20/79.27 => ~ earlier(X9,X8) ) ). % 79.20/79.27 % 79.20/79.27 fof(sos_05,axiom, % 79.20/79.27 ! [X10,X11,X12] : % 79.20/79.27 ( ( earlier(X10,X11) % 79.20/79.27 & earlier(X11,X12) ) % 79.20/79.27 => earlier(X10,X12) ) ). % 79.20/79.27 % 79.20/79.27 fof(sos_06,axiom, % 79.20/79.27 ! [X13,X14,X15] : % 79.20/79.27 ( ( earlier(X13,X14) % 79.20/79.27 & earlier(X15,X14) ) % 79.20/79.27 => ( earlier(X15,X13) % 79.20/79.27 | earlier(X13,X15) % 79.20/79.27 | X13 = X15 ) ) ). % 79.20/79.27 % 79.20/79.27 fof(sos_07,axiom, % 79.20/79.27 ! [X16,X17] : % 79.20/79.27 ( occurrence_of(X16,X17) % 79.20/79.27 => ( arboreal(X16) % 79.20/79.27 <=> atomic(X17) ) ) ). % 79.20/79.27 % 79.20/79.27 fof(sos_08,axiom, % 79.20/79.27 ! [X18] : % 79.20/79.27 ( legal(X18) % 79.20/79.27 => arboreal(X18) ) ). % 79.20/79.27 % 79.20/79.27 fof(sos_09,axiom, % 79.20/79.27 ! [X19,X20] : % 79.20/79.27 ( ( legal(X19) % 79.20/79.27 & earlier(X20,X19) ) % 79.20/79.27 => legal(X20) ) ). % 79.20/79.27 % 79.20/79.27 fof(sos_10,axiom, % 79.20/79.27 ! [X21,X22] : % 79.20/79.27 ( precedes(X21,X22) % 79.20/79.27 <=> ( earlier(X21,X22) % 79.20/79.27 & legal(X22) ) ) ). % 79.20/79.27 % 79.20/79.27 fof(sos_11,axiom, % 79.20/79.27 ! [X23,X24,X25] : % 79.20/79.27 ( min_precedes(X24,X25,X23) % 79.20/79.27 => ? [X26,X27] : % 79.20/79.27 ( subactivity(X26,X23) % 79.20/79.27 & subactivity(X27,X23) % 79.20/79.27 & atocc(X24,X26) % 79.20/79.27 & atocc(X25,X27) ) ) ). % 79.20/79.27 % 79.20/79.27 fof(sos_12,axiom, % 79.20/79.27 ! [X28,X29] : % 79.20/79.27 ( root(X29,X28) % 79.20/79.27 => ? [X30] : % 79.20/79.27 ( subactivity(X30,X28) % 79.20/79.27 & atocc(X29,X30) ) ) ). % 79.20/79.27 % 79.20/79.27 fof(sos_13,axiom, % 79.20/79.27 ! [X31,X32,X33] : % 79.20/79.27 ( min_precedes(X31,X32,X33) % 79.20/79.28 => ? [X34] : % 79.20/79.28 ( root(X34,X33) % 79.20/79.28 & min_precedes(X34,X32,X33) ) ) ). % 79.20/79.28 % 79.20/79.28 fof(sos_14,axiom, % 79.20/79.28 ! [X35,X36,X37] : % 79.20/79.28 ( min_precedes(X35,X36,X37) % 79.20/79.28 => ~ root(X36,X37) ) ). % 79.20/79.28 % 79.20/79.28 fof(sos_15,axiom, % 79.20/79.28 ! [X38,X39,X40] : % 79.20/79.28 ( min_precedes(X38,X39,X40) % 79.20/79.28 => precedes(X38,X39) ) ). % 79.20/79.28 % 79.20/79.28 fof(sos_16,axiom, % 79.20/79.28 ! [X41,X42] : % 79.20/79.28 ( root(X41,X42) % 79.20/79.28 => legal(X41) ) ). % 79.20/79.28 % 79.20/79.28 fof(sos_17,axiom, % 79.20/79.28 ! [X43,X44] : % 79.20/79.28 ( ( atocc(X43,X44) % 79.20/79.28 & legal(X43) ) % 79.20/79.28 => root(X43,X44) ) ). % 79.20/79.28 % 79.20/79.28 fof(sos_18,axiom, % 79.20/79.28 ! [X45,X46,X47,X48] : % 79.20/79.28 ( ( min_precedes(X45,X46,X48) % 79.20/79.28 & min_precedes(X45,X47,X48) % 79.20/79.28 & precedes(X46,X47) ) % 79.20/79.28 => min_precedes(X46,X47,X48) ) ). % 79.20/79.28 % 79.20/79.28 fof(sos_19,axiom, % 79.20/79.28 ! [X49,X50,X51] : % 79.20/79.28 ( min_precedes(X49,X50,X51) % 79.20/79.28 => ~ atomic(X51) ) ). % 79.20/79.28 % 79.20/79.28 fof(sos_20,axiom, % 79.20/79.28 ! [X52,X53,X54,X55] : % 79.20/79.28 ( ( min_precedes(X53,X52,X55) % 79.20/79.28 & min_precedes(X54,X52,X55) % 79.20/79.28 & precedes(X53,X54) ) % 79.20/79.28 => min_precedes(X53,X54,X55) ) ). % 79.20/79.28 % 79.20/79.28 fof(sos_21,axiom, % 79.20/79.28 ! [X56,X57] : % 79.20/79.28 ( leaf(X56,X57) % 79.20/79.28 <=> ( ( root(X56,X57) % 79.20/79.28 | ? [X58] : min_precedes(X58,X56,X57) ) % 79.20/79.28 & ~ ? [X59] : min_precedes(X56,X59,X57) ) ) ). % 79.20/79.28 % 79.20/79.28 fof(sos_22,axiom, % 79.20/79.28 ! [X60,X61,X62] : % 79.20/79.28 ( next_subocc(X60,X61,X62) % 79.20/79.28 <=> ( min_precedes(X60,X61,X62) % 79.20/79.28 & ~ ? [X63] : % 79.20/79.28 ( min_precedes(X60,X63,X62) % 79.20/79.28 & min_precedes(X63,X61,X62) ) ) ) ). % 79.20/79.28 % 79.20/79.28 fof(sos_23,axiom, % 79.20/79.28 ! [X64,X65] : % 79.20/79.28 ( atocc(X64,X65) % 79.20/79.28 <=> ? [X66] : % 79.20/79.28 ( subactivity(X65,X66) % 79.20/79.28 & atomic(X66) % 79.20/79.28 & occurrence_of(X64,X66) ) ) ). % 79.20/79.28 % 79.20/79.28 fof(sos_24,axiom, % 79.20/79.28 ! [X67,X68] : % 79.20/79.28 ( subactivity_occurrence(X67,X68) % 79.20/79.28 => ( activity_occurrence(X67) % 79.20/79.28 & activity_occurrence(X68) ) ) ). % 79.20/79.28 % 79.20/79.28 fof(sos_25,axiom, % 79.20/79.28 ! [X69,X70,X71] : % 79.20/79.28 ( min_precedes(X70,X71,X69) % 79.20/79.28 => ? [X72] : % 79.20/79.28 ( occurrence_of(X72,X69) % 79.20/79.28 & subactivity_occurrence(X70,X72) % 79.20/79.28 & subactivity_occurrence(X71,X72) ) ) ). % 79.20/79.28 % 79.20/79.28 fof(sos_26,axiom, % 79.20/79.28 ! [X73,X74] : % 79.20/79.28 ( ( root(X74,X73) % 79.20/79.28 & ~ atomic(X73) ) % 79.20/79.28 => ? [X75] : % 79.20/79.28 ( occurrence_of(X75,X73) % 79.20/79.28 & subactivity_occurrence(X74,X75) ) ) ). % 79.20/79.28 % 79.20/79.28 fof(sos_27,axiom, % 79.20/79.28 ! [X76,X77] : % 79.20/79.28 ( ( occurrence_of(X77,X76) % 79.20/79.28 & ~ atomic(X76) ) % 79.20/79.28 => ? [X78] : % 79.20/79.28 ( root(X78,X76) % 79.20/79.28 & subactivity_occurrence(X78,X77) ) ) ). % 79.20/79.28 % 79.20/79.28 fof(sos_28,axiom, % 79.20/79.28 ! [X79,X80,X81,X82] : % 79.20/79.28 ( ( occurrence_of(X80,X79) % 79.20/79.28 & arboreal(X81) % 79.20/79.28 & arboreal(X82) % 79.20/79.28 & subactivity_occurrence(X81,X80) % 79.20/79.28 & subactivity_occurrence(X82,X80) ) % 79.20/79.28 => ( min_precedes(X81,X82,X79) % 79.20/79.28 | min_precedes(X82,X81,X79) % 79.20/79.28 | X81 = X82 ) ) ). % 79.20/79.28 % 79.20/79.28 fof(sos_29,axiom, % 79.20/79.28 ! [X83,X84,X85,X86] : % 79.20/79.28 ( ( min_precedes(X83,X84,X85) % 79.20/79.28 & occurrence_of(X86,X85) % 79.20/79.28 & subactivity_occurrence(X84,X86) ) % 79.20/79.28 => subactivity_occurrence(X83,X86) ) ). % 79.20/79.28 % 79.20/79.28 fof(sos_30,axiom, % 79.20/79.28 ! [X87,X88,X89,X90] : % 79.20/79.28 ( ( occurrence_of(X89,X87) % 79.20/79.28 & occurrence_of(X90,X88) % 79.20/79.28 & ~ atomic(X87) % 79.20/79.28 & subactivity_occurrence(X89,X90) ) % 79.20/79.28 => subactivity(X87,X88) ) ). % 79.20/79.28 % 79.20/79.28 fof(sos_31,axiom, % 79.20/79.28 ! [X91,X92,X93] : % 79.20/79.28 ( ( subactivity_occurrence(X91,X92) % 79.20/79.28 & subactivity_occurrence(X92,X93) ) % 79.20/79.28 => subactivity_occurrence(X91,X93) ) ). % 79.20/79.28 % 79.20/79.28 fof(sos_32,axiom, % 79.20/79.28 ! [X94,X95,X96,X97] : % 79.20/79.28 ( ( occurrence_of(X96,X94) % 79.20/79.28 & occurrence_of(X97,X95) % 79.20/79.28 & subactivity(X94,X95) % 79.20/79.28 & ~ subactivity_occurrence(X96,X97) ) % 79.20/79.28 => ? [X98] : % 79.20/79.28 ( subactivity_occurrence(X98,X97) % 79.20/79.28 & ~ subactivity_occurrence(X98,X96) ) ) ). % 79.20/79.28 % 79.20/79.28 fof(sos_33,axiom, % 79.20/79.28 ! [X99,X100] : % 79.20/79.28 ( root_occ(X99,X100) % 79.20/79.28 <=> ? [X101] : % 79.20/79.28 ( occurrence_of(X100,X101) % 79.20/79.28 & subactivity_occurrence(X99,X100) % 79.20/79.28 & root(X99,X101) ) ) ). % 79.20/79.28 % 79.20/79.28 fof(sos_34,axiom, % 79.20/79.28 ! [X102,X103] : % 79.20/79.28 ( leaf_occ(X102,X103) % 79.20/79.28 <=> ? [X104] : % 79.20/79.28 ( occurrence_of(X103,X104) % 79.20/79.28 & subactivity_occurrence(X102,X103) % 79.20/79.28 & leaf(X102,X104) ) ) ). % 79.20/79.28 % 79.20/79.28 fof(sos_35,axiom, % 79.20/79.28 ! [X105] : % 79.20/79.28 ( occurrence_of(X105,tptp0) % 79.20/79.28 => ? [X106,X107,X108] : % 79.20/79.28 ( occurrence_of(X106,tptp3) % 79.20/79.28 & root_occ(X106,X105) % 79.20/79.28 & occurrence_of(X107,tptp4) % 79.20/79.28 & next_subocc(X106,X107,tptp0) % 79.20/79.28 & ( occurrence_of(X108,tptp2) % 79.20/79.28 | occurrence_of(X108,tptp1) ) % 79.20/79.28 & next_subocc(X107,X108,tptp0) % 79.20/79.28 & leaf_occ(X108,X105) ) ) ). % 79.20/79.28 % 79.20/79.28 fof(sos_36,axiom, % 79.20/79.28 activity(tptp0) ). % 79.20/79.28 % 79.20/79.28 fof(sos_37,axiom, % 79.20/79.28 ~ atomic(tptp0) ). % 79.20/79.28 % 79.20/79.28 fof(sos_38,axiom, % 79.20/79.28 atomic(tptp4) ). % 79.20/79.28 % 79.20/79.28 fof(sos_39,axiom, % 79.20/79.28 atomic(tptp2) ). % 79.20/79.28 % 79.20/79.28 fof(sos_40,axiom, % 79.20/79.28 atomic(tptp1) ). % 79.20/79.28 % 79.20/79.28 fof(sos_41,axiom, % 79.20/79.28 atomic(tptp3) ). % 79.20/79.28 % 79.20/79.28 fof(sos_42,axiom, % 79.20/79.28 tptp4 != tptp3 ). % 79.20/79.28 % 79.20/79.28 fof(sos_43,axiom, % 79.20/79.28 tptp4 != tptp2 ). % 79.20/79.28 % 79.20/79.28 fof(sos_44,axiom, % 79.20/79.28 tptp4 != tptp1 ). % 79.20/79.28 % 79.20/79.28 fof(sos_45,axiom, % 79.20/79.28 tptp3 != tptp2 ). % 79.20/79.28 % 79.20/79.28 fof(sos_46,axiom, % 79.20/79.28 tptp3 != tptp1 ). % 79.20/79.28 % 79.20/79.28 fof(sos_47,axiom, % 79.20/79.28 tptp2 != tptp1 ). % 79.20/79.28 % 79.20/79.28 fof(goals,conjecture, % 79.20/79.28 ! [X109] : % 79.20/79.28 ( occurrence_of(X109,tptp0) % 79.20/79.28 => ? [X110,X111] : % 79.20/79.28 ( occurrence_of(X110,tptp3) % 79.20/79.28 & root_occ(X110,X109) % 79.20/79.28 & ( occurrence_of(X111,tptp2) % 79.20/79.28 | occurrence_of(X111,tptp1) ) % 79.20/79.28 & min_precedes(X110,X111,tptp0) % 79.20/79.28 & leaf_occ(X111,X109) ) ) ). % 79.20/79.28 % 79.20/79.28 %------------------------------------------------------------------------------ % 79.20/79.28 %------------------------------------------- % 79.20/79.28 % Proof found % 79.20/79.28 % SZS status Theorem for theBenchmark % 79.20/79.28 % SZS output start Proof % 79.20/79.28 %ClaNum:161(EqnAxiom:73) % 79.20/79.28 %VarNum:443(SingletonVarNum:179) % 79.20/79.28 %MaxLitNum:8 % 79.20/79.28 %MaxfuncDepth:1 % 79.20/79.28 %SharedTerms:19 % 79.20/79.28 %goalClause: 79 142 143 % 79.20/79.28 %singleGoalClaCount:1 % 79.20/79.28 [74]P1(a1) % 79.20/79.28 [75]P2(a21) % 79.20/79.28 [76]P2(a24) % 79.20/79.28 [77]P2(a22) % 79.20/79.28 [78]P2(a23) % 79.20/79.28 [79]P6(a2,a1) % 79.20/79.28 [80]~E(a24,a21) % 79.20/79.28 [81]~E(a22,a21) % 79.20/79.28 [82]~E(a22,a24) % 79.20/79.28 [83]~E(a23,a21) % 79.20/79.28 [84]~E(a23,a24) % 79.20/79.28 [85]~E(a23,a22) % 79.20/79.28 [86]~P2(a1) % 79.20/79.28 [87]~P7(x871)+P3(x871) % 79.20/79.28 [89]~P1(x891)+P13(x891,x891) % 79.20/79.28 [88]~P4(x881)+P1(f12(x881)) % 79.20/79.28 [96]~P4(x961)+P6(x961,f12(x961)) % 79.20/79.28 [103]~P6(x1031,a1)+P6(f3(x1031),a21) % 79.20/79.28 [104]~P6(x1041,a1)+P6(f10(x1041),a24) % 79.20/79.28 [105]~P6(x1051,a1)+P16(f3(x1051),x1051) % 79.20/79.28 [106]~P6(x1061,a1)+P9(f11(x1061),x1061) % 79.20/79.28 [131]~P6(x1311,a1)+P11(f3(x1311),f10(x1311),a1) % 79.20/79.28 [132]~P6(x1321,a1)+P11(f10(x1321),f11(x1321),a1) % 79.20/79.28 [90]P1(x901)+~P6(x902,x901) % 79.20/79.28 [91]P4(x911)+~P6(x911,x912) % 79.20/79.28 [92]P4(x921)+~P17(x922,x921) % 79.20/79.28 [93]P4(x931)+~P17(x931,x932) % 79.20/79.28 [94]P7(x941)+~P14(x942,x941) % 79.20/79.28 [95]P7(x951)+~P15(x951,x952) % 79.20/79.28 [100]~P14(x1001,x1002)+P8(x1001,x1002) % 79.20/79.28 [101]~P16(x1011,x1012)+P17(x1011,x1012) % 79.20/79.28 [102]~P9(x1021,x1022)+P17(x1021,x1022) % 79.20/79.28 [109]~P8(x1092,x1091)+~P8(x1091,x1092) % 79.20/79.28 [111]~P5(x1111,x1112)+P2(f13(x1111,x1112)) % 79.20/79.28 [115]~P5(x1151,x1152)+P6(x1151,f13(x1151,x1152)) % 79.20/79.28 [116]~P16(x1162,x1161)+P6(x1161,f4(x1162,x1161)) % 79.20/79.28 [117]~P9(x1172,x1171)+P6(x1171,f9(x1172,x1171)) % 79.20/79.28 [118]~P5(x1182,x1181)+P13(x1181,f13(x1182,x1181)) % 79.20/79.28 [119]~P15(x1191,x1192)+P5(x1191,f14(x1192,x1191)) % 79.20/79.28 [120]~P16(x1201,x1202)+P15(x1201,f4(x1201,x1202)) % 79.20/79.28 [121]~P9(x1211,x1212)+P10(x1211,f9(x1211,x1212)) % 79.20/79.28 [122]~P15(x1222,x1221)+P13(f14(x1221,x1222),x1221) % 79.20/79.29 [134]~P2(x1341)+~P12(x1342,x1343,x1341) % 79.20/79.29 [135]P14(x1351,x1352)+~P12(x1351,x1352,x1353) % 79.20/79.29 [136]~P15(x1361,x1362)+~P12(x1363,x1361,x1362) % 79.20/79.29 [137]~P10(x1371,x1372)+~P12(x1371,x1373,x1372) % 79.20/79.29 [140]~P11(x1401,x1402,x1403)+P12(x1401,x1402,x1403) % 79.20/79.29 [146]~P12(x1461,x1463,x1462)+P5(x1461,f15(x1462,x1461,x1463)) % 79.20/79.29 [147]~P12(x1473,x1471,x1472)+P5(x1471,f16(x1472,x1473,x1471)) % 79.20/79.29 [148]~P12(x1483,x1481,x1482)+P17(x1481,f6(x1482,x1483,x1481)) % 79.20/79.29 [149]~P12(x1491,x1493,x1492)+P17(x1491,f6(x1492,x1491,x1493)) % 79.20/79.29 [150]~P12(x1502,x1503,x1501)+P6(f6(x1501,x1502,x1503),x1501) % 79.20/79.29 [151]~P12(x1512,x1513,x1511)+P13(f15(x1511,x1512,x1513),x1511) % 79.20/79.29 [152]~P12(x1522,x1523,x1521)+P13(f16(x1521,x1522,x1523),x1521) % 79.20/79.29 [153]~P12(x1531,x1532,x1533)+P15(f19(x1531,x1532,x1533),x1533) % 79.20/79.29 [154]~P12(x1541,x1542,x1543)+P12(f19(x1541,x1542,x1543),x1542,x1543) % 79.20/79.29 [112]~P6(x1121,a1)+P6(f11(x1121),a22)+P6(f11(x1121),a23) % 79.20/79.29 [97]~P6(x971,x972)+P3(x971)+~P2(x972) % 79.20/79.29 [98]~P6(x982,x981)+P2(x981)+~P3(x982) % 79.20/79.29 [99]~P8(x991,x992)+P7(x991)+~P7(x992) % 79.20/79.29 [107]~P7(x1072)+~P8(x1071,x1072)+P14(x1071,x1072) % 79.20/79.29 [108]~P7(x1081)+~P5(x1081,x1082)+P15(x1081,x1082) % 79.20/79.29 [124]~P15(x1242,x1241)+P2(x1241)+P17(x1242,f5(x1241,x1242)) % 79.20/79.29 [125]~P15(x1252,x1251)+P2(x1251)+P6(f5(x1251,x1252),x1251) % 79.20/79.29 [126]~P6(x1262,x1261)+P2(x1261)+P15(f7(x1261,x1262),x1261) % 79.20/79.29 [127]~P6(x1272,x1271)+P2(x1271)+P17(f7(x1271,x1272),x1272) % 79.20/79.29 [138]~P15(x1381,x1382)+P10(x1381,x1382)+P12(x1381,f17(x1381,x1382),x1382) % 79.20/79.29 [139]~P10(x1391,x1392)+P15(x1391,x1392)+P12(f18(x1391,x1392),x1391,x1392) % 79.20/79.29 [110]~P6(x1103,x1101)+E(x1101,x1102)+~P6(x1103,x1102) % 79.20/79.29 [113]~P8(x1131,x1133)+P8(x1131,x1132)+~P8(x1133,x1132) % 79.20/79.29 [114]~P17(x1141,x1143)+P17(x1141,x1142)+~P17(x1143,x1142) % 79.20/79.29 [144]P10(x1441,x1442)+~P12(x1443,x1441,x1442)+P12(x1441,f17(x1441,x1442),x1442) % 79.20/79.29 [158]~P12(x1581,x1582,x1583)+P11(x1581,x1582,x1583)+P12(x1581,f20(x1581,x1582,x1583),x1583) % 79.20/79.29 [159]~P12(x1591,x1592,x1593)+P11(x1591,x1592,x1593)+P12(f20(x1591,x1592,x1593),x1592,x1593) % 79.20/79.29 [157]~P11(x1574,x1572,x1573)+~P12(x1571,x1572,x1573)+~P12(x1574,x1571,x1573) % 79.20/79.29 [123]~P6(x1231,x1233)+~P13(x1232,x1233)+P5(x1231,x1232)+~P2(x1233) % 79.20/79.29 [129]~P15(x1291,x1293)+~P17(x1291,x1292)+P16(x1291,x1292)+~P6(x1292,x1293) % 79.20/79.29 [130]~P10(x1301,x1303)+~P17(x1301,x1302)+P9(x1301,x1302)+~P6(x1302,x1303) % 79.20/79.29 [141]~P12(x1411,x1414,x1413)+P17(x1411,x1412)+~P6(x1412,x1413)+~P17(x1414,x1412) % 79.20/79.29 [155]~P14(x1551,x1552)+~P12(x1554,x1551,x1553)+P12(x1551,x1552,x1553)+~P12(x1554,x1552,x1553) % 79.20/79.29 [156]~P14(x1561,x1562)+~P12(x1561,x1564,x1563)+P12(x1561,x1562,x1563)+~P12(x1562,x1564,x1563) % 79.20/79.29 [142]~P12(x1421,x1422,a1)+~P16(x1421,a2)+~P9(x1422,a2)+~P6(x1421,a21)+~P6(x1422,a22) % 79.20/79.29 [143]~P12(x1431,x1432,a1)+~P16(x1431,a2)+~P9(x1432,a2)+~P6(x1431,a21)+~P6(x1432,a23) % 79.20/79.29 [128]P8(x1282,x1281)+P8(x1281,x1282)+~P8(x1281,x1283)+E(x1281,x1282)+~P8(x1282,x1283) % 79.20/79.29 [133]~P17(x1334,x1333)+P2(x1331)+P13(x1331,x1332)+~P6(x1333,x1332)+~P6(x1334,x1331) % 79.20/79.29 [160]~P6(x1602,x1604)+~P6(x1601,x1603)+~P13(x1603,x1604)+P17(x1601,x1602)+P17(f8(x1603,x1604,x1601,x1602),x1602) % 79.20/79.29 [161]~P13(x1614,x1613)+P17(x1611,x1612)+~P6(x1612,x1613)+~P6(x1611,x1614)+~P17(f8(x1614,x1613,x1611,x1612),x1611) % 79.20/79.29 [145]P12(x1451,x1452,x1453)+~P3(x1452)+~P3(x1451)+~P17(x1452,x1454)+~P17(x1451,x1454)+E(x1451,x1452)+P12(x1452,x1451,x1453)+~P6(x1454,x1453) % 79.20/79.29 %EqnAxiom % 79.20/79.29 [1]E(x11,x11) % 79.20/79.29 [2]E(x22,x21)+~E(x21,x22) % 79.20/79.29 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 79.20/79.29 [4]~E(x41,x42)+E(f12(x41),f12(x42)) % 79.20/79.29 [5]~E(x51,x52)+E(f8(x51,x53,x54,x55),f8(x52,x53,x54,x55)) % 79.20/79.29 [6]~E(x61,x62)+E(f8(x63,x61,x64,x65),f8(x63,x62,x64,x65)) % 79.20/79.29 [7]~E(x71,x72)+E(f8(x73,x74,x71,x75),f8(x73,x74,x72,x75)) % 79.20/79.29 [8]~E(x81,x82)+E(f8(x83,x84,x85,x81),f8(x83,x84,x85,x82)) % 79.20/79.29 [9]~E(x91,x92)+E(f3(x91),f3(x92)) % 79.20/79.29 [10]~E(x101,x102)+E(f10(x101),f10(x102)) % 79.20/79.29 [11]~E(x111,x112)+E(f20(x111,x113,x114),f20(x112,x113,x114)) % 79.20/79.29 [12]~E(x121,x122)+E(f20(x123,x121,x124),f20(x123,x122,x124)) % 79.20/79.29 [13]~E(x131,x132)+E(f20(x133,x134,x131),f20(x133,x134,x132)) % 79.20/79.29 [14]~E(x141,x142)+E(f11(x141),f11(x142)) % 79.20/79.29 [15]~E(x151,x152)+E(f13(x151,x153),f13(x152,x153)) % 79.20/79.29 [16]~E(x161,x162)+E(f13(x163,x161),f13(x163,x162)) % 79.20/79.29 [17]~E(x171,x172)+E(f15(x171,x173,x174),f15(x172,x173,x174)) % 79.20/79.29 [18]~E(x181,x182)+E(f15(x183,x181,x184),f15(x183,x182,x184)) % 79.20/79.29 [19]~E(x191,x192)+E(f15(x193,x194,x191),f15(x193,x194,x192)) % 79.20/79.29 [20]~E(x201,x202)+E(f6(x201,x203,x204),f6(x202,x203,x204)) % 79.20/79.29 [21]~E(x211,x212)+E(f6(x213,x211,x214),f6(x213,x212,x214)) % 79.20/79.29 [22]~E(x221,x222)+E(f6(x223,x224,x221),f6(x223,x224,x222)) % 79.20/79.29 [23]~E(x231,x232)+E(f17(x231,x233),f17(x232,x233)) % 79.20/79.29 [24]~E(x241,x242)+E(f17(x243,x241),f17(x243,x242)) % 79.20/79.29 [25]~E(x251,x252)+E(f4(x251,x253),f4(x252,x253)) % 79.20/79.29 [26]~E(x261,x262)+E(f4(x263,x261),f4(x263,x262)) % 79.20/79.29 [27]~E(x271,x272)+E(f9(x271,x273),f9(x272,x273)) % 79.20/79.29 [28]~E(x281,x282)+E(f9(x283,x281),f9(x283,x282)) % 79.20/79.29 [29]~E(x291,x292)+E(f16(x291,x293,x294),f16(x292,x293,x294)) % 79.20/79.29 [30]~E(x301,x302)+E(f16(x303,x301,x304),f16(x303,x302,x304)) % 79.20/79.29 [31]~E(x311,x312)+E(f16(x313,x314,x311),f16(x313,x314,x312)) % 79.20/79.29 [32]~E(x321,x322)+E(f14(x321,x323),f14(x322,x323)) % 79.20/79.29 [33]~E(x331,x332)+E(f14(x333,x331),f14(x333,x332)) % 79.20/79.29 [34]~E(x341,x342)+E(f18(x341,x343),f18(x342,x343)) % 79.20/79.29 [35]~E(x351,x352)+E(f18(x353,x351),f18(x353,x352)) % 79.20/79.29 [36]~E(x361,x362)+E(f19(x361,x363,x364),f19(x362,x363,x364)) % 79.20/79.29 [37]~E(x371,x372)+E(f19(x373,x371,x374),f19(x373,x372,x374)) % 79.20/79.29 [38]~E(x381,x382)+E(f19(x383,x384,x381),f19(x383,x384,x382)) % 79.20/79.29 [39]~E(x391,x392)+E(f7(x391,x393),f7(x392,x393)) % 79.20/79.29 [40]~E(x401,x402)+E(f7(x403,x401),f7(x403,x402)) % 79.20/79.29 [41]~E(x411,x412)+E(f5(x411,x413),f5(x412,x413)) % 79.20/79.29 [42]~E(x421,x422)+E(f5(x423,x421),f5(x423,x422)) % 79.20/79.29 [43]~P1(x431)+P1(x432)+~E(x431,x432) % 79.20/79.29 [44]~P2(x441)+P2(x442)+~E(x441,x442) % 79.20/79.29 [45]P6(x452,x453)+~E(x451,x452)+~P6(x451,x453) % 79.20/79.29 [46]P6(x463,x462)+~E(x461,x462)+~P6(x463,x461) % 79.20/79.29 [47]P17(x472,x473)+~E(x471,x472)+~P17(x471,x473) % 79.20/79.29 [48]P17(x483,x482)+~E(x481,x482)+~P17(x483,x481) % 79.20/79.29 [49]P13(x492,x493)+~E(x491,x492)+~P13(x491,x493) % 79.20/79.29 [50]P13(x503,x502)+~E(x501,x502)+~P13(x503,x501) % 79.20/79.29 [51]P12(x512,x513,x514)+~E(x511,x512)+~P12(x511,x513,x514) % 79.20/79.29 [52]P12(x523,x522,x524)+~E(x521,x522)+~P12(x523,x521,x524) % 79.20/79.29 [53]P12(x533,x534,x532)+~E(x531,x532)+~P12(x533,x534,x531) % 79.20/79.29 [54]P11(x542,x543,x544)+~E(x541,x542)+~P11(x541,x543,x544) % 79.20/79.29 [55]P11(x553,x552,x554)+~E(x551,x552)+~P11(x553,x551,x554) % 79.20/79.29 [56]P11(x563,x564,x562)+~E(x561,x562)+~P11(x563,x564,x561) % 79.20/79.29 [57]~P3(x571)+P3(x572)+~E(x571,x572) % 79.20/79.29 [58]~P7(x581)+P7(x582)+~E(x581,x582) % 79.20/79.29 [59]P16(x592,x593)+~E(x591,x592)+~P16(x591,x593) % 79.20/79.29 [60]P16(x603,x602)+~E(x601,x602)+~P16(x603,x601) % 79.20/79.29 [61]~P4(x611)+P4(x612)+~E(x611,x612) % 79.20/79.29 [62]P10(x622,x623)+~E(x621,x622)+~P10(x621,x623) % 79.20/79.29 [63]P10(x633,x632)+~E(x631,x632)+~P10(x633,x631) % 79.20/79.29 [64]P5(x642,x643)+~E(x641,x642)+~P5(x641,x643) % 79.20/79.29 [65]P5(x653,x652)+~E(x651,x652)+~P5(x653,x651) % 79.20/79.29 [66]P8(x662,x663)+~E(x661,x662)+~P8(x661,x663) % 79.20/79.29 [67]P8(x673,x672)+~E(x671,x672)+~P8(x673,x671) % 79.20/79.29 [68]P15(x682,x683)+~E(x681,x682)+~P15(x681,x683) % 79.20/79.29 [69]P15(x693,x692)+~E(x691,x692)+~P15(x693,x691) % 79.20/79.29 [70]P14(x702,x703)+~E(x701,x702)+~P14(x701,x703) % 79.20/79.29 [71]P14(x713,x712)+~E(x711,x712)+~P14(x713,x711) % 79.20/79.29 [72]P9(x722,x723)+~E(x721,x722)+~P9(x721,x723) % 79.20/79.29 [73]P9(x733,x732)+~E(x731,x732)+~P9(x733,x731) % 79.20/79.29 % 79.20/79.29 %------------------------------------------- % 79.20/79.29 cnf(162,plain, % 79.20/79.29 (~P12(x1621,x1622,a21)), % 79.20/79.29 inference(scs_inference,[],[75,134])). % 79.20/79.29 cnf(164,plain, % 79.20/79.29 (~P3(a2)), % 79.20/79.29 inference(scs_inference,[],[79,75,86,134,98])). % 79.20/79.29 cnf(168,plain, % 79.20/79.29 (~P7(a2)), % 79.20/79.29 inference(scs_inference,[],[79,75,86,134,98,140,87])). % 79.20/79.29 cnf(170,plain, % 79.20/79.29 (~P15(a2,x1701)), % 79.20/79.29 inference(scs_inference,[],[79,75,86,134,98,140,87,95])). % 79.20/79.29 cnf(176,plain, % 79.20/79.29 (~P12(x1761,a2,x1762)), % 79.20/79.29 inference(scs_inference,[],[79,75,86,134,98,140,87,95,120,94,135])). % 79.20/79.29 cnf(185,plain, % 79.20/79.29 (P6(x1851,a1)+~E(a2,x1851)), % 79.20/79.29 inference(scs_inference,[],[79,75,86,134,98,140,87,95,120,94,135,97,138,139,46,45])). % 79.20/79.29 cnf(191,plain, % 79.20/79.29 (~P12(x1911,x1912,a24)), % 79.20/79.29 inference(scs_inference,[],[76,176,140,134])). % 79.20/79.29 cnf(197,plain, % 79.20/79.29 (~P6(a2,a24)), % 79.20/79.29 inference(scs_inference,[],[164,162,170,76,176,140,134,139,97])). % 79.20/79.29 cnf(207,plain, % 79.20/79.29 (~P12(x2071,x2072,a22)), % 79.20/79.29 inference(scs_inference,[],[191,77,140,134])). % 79.20/79.29 cnf(209,plain, % 79.20/79.29 (~P6(a2,a22)), % 79.20/79.29 inference(scs_inference,[],[164,191,77,140,134,97])). % 79.20/79.29 cnf(232,plain, % 79.20/79.29 (~P7(x2321)+~P8(a2,x2321)), % 79.20/79.29 inference(scs_inference,[],[79,164,209,168,207,78,170,140,134,139,97,46,99])). % 79.20/79.29 cnf(234,plain, % 79.20/79.29 (~P14(x2341,x2342)+~P8(a2,x2342)), % 79.20/79.29 inference(scs_inference,[],[79,164,209,168,207,78,170,140,134,139,97,46,99,94])). % 79.20/79.29 cnf(261,plain, % 79.20/79.29 (~P17(x2611,a2)+~P12(x2612,x2611,a1)+P17(x2612,a2)), % 79.20/79.29 inference(scs_inference,[],[79,162,141])). % 79.20/79.29 cnf(326,plain, % 79.20/79.29 (~P17(x3261,x3262)+P6(x3262,f12(x3262))), % 79.20/79.29 inference(scs_inference,[],[92,96])). % 79.20/79.29 cnf(391,plain, % 79.20/79.29 (~P8(x3911,x3912)+~P14(x3912,x3911)), % 79.20/79.29 inference(scs_inference,[],[100,109])). % 79.20/79.29 cnf(474,plain, % 79.20/79.29 (~P12(x4741,x4742,x4743)+~P8(a2,x4742)), % 79.20/79.29 inference(scs_inference,[],[234,135])). % 79.20/79.29 cnf(528,plain, % 79.20/79.29 (~P8(x5281,x5282)+~P12(x5282,x5281,x5283)), % 79.20/79.29 inference(scs_inference,[],[391,135])). % 79.20/79.29 cnf(560,plain, % 79.20/79.29 (~E(a2,x5601)+P6(f10(x5601),a24)), % 79.20/79.29 inference(scs_inference,[],[104,185])). % 79.20/79.29 cnf(561,plain, % 79.20/79.29 (P6(f10(a2),a24)), % 79.20/79.29 inference(equality_inference,[],[560])). % 79.20/79.29 cnf(714,plain, % 79.20/79.29 (P17(f11(a2),a2)), % 79.20/79.29 inference(scs_inference,[],[79,106,102])). % 79.20/79.29 cnf(768,plain, % 79.20/79.29 (~P12(x7681,f7(a1,a2),a1)), % 79.20/79.29 inference(scs_inference,[],[86,79,136,126])). % 79.20/79.29 cnf(769,plain, % 79.20/79.29 (~P11(x7691,f7(a1,a2),a1)), % 79.20/79.29 inference(scs_inference,[],[768,140])). % 79.20/79.29 cnf(809,plain, % 79.20/79.29 (~P11(x8091,x8092,x8093)+~P8(a2,x8092)), % 79.20/79.29 inference(scs_inference,[],[474,140])). % 79.20/79.29 cnf(825,plain, % 79.20/79.29 (~P12(x8251,x8252,x8253)+~P14(x8252,x8251)), % 79.20/79.29 inference(scs_inference,[],[528,100])). % 79.20/79.29 cnf(984,plain, % 79.20/79.29 (~P8(a2,f10(a2))), % 79.20/79.29 inference(scs_inference,[],[79,809,131])). % 79.20/79.29 cnf(987,plain, % 79.20/79.29 (~P12(a2,f10(a2),x9871)), % 79.20/79.29 inference(scs_inference,[],[984,100,135])). % 79.20/79.29 cnf(1006,plain, % 79.20/79.29 (~P12(x10061,x10062,x10063)+~P12(x10062,x10061,x10064)), % 79.20/79.29 inference(scs_inference,[],[825,135])). % 79.20/79.29 cnf(1912,plain, % 79.20/79.29 (~P11(x19121,x19122,x19123)+~P12(x19122,x19121,x19124)), % 79.20/79.29 inference(scs_inference,[],[1006,140])). % 79.20/79.29 cnf(2299,plain, % 79.20/79.29 (~P12(f10(a2),f3(a2),x22991)), % 79.20/79.29 inference(scs_inference,[],[79,1912,131])). % 79.20/79.29 cnf(2300,plain, % 79.20/79.29 (~P11(f10(a2),f3(a2),x23001)), % 79.20/79.29 inference(scs_inference,[],[2299,140])). % 79.20/79.29 cnf(4093,plain, % 79.20/79.29 (~P6(f10(a2),a21)), % 79.20/79.29 inference(scs_inference,[],[561,80,110])). % 79.20/79.29 cnf(4116,plain, % 79.20/79.29 (~P6(x41161,a21)+~P6(x41161,a22)), % 79.20/79.29 inference(scs_inference,[],[81,110])). % 79.20/79.29 cnf(4122,plain, % 79.20/79.29 (~P6(x41221,a21)+~P6(x41221,a23)), % 79.20/79.29 inference(scs_inference,[],[83,110])). % 79.20/79.29 cnf(4180,plain, % 79.20/79.29 (~P6(f11(a2),a21)+P6(f11(a2),a22)), % 79.20/79.29 inference(scs_inference,[],[79,4122,112])). % 79.20/79.29 cnf(4192,plain, % 79.20/79.29 (P13(a24,a24)), % 79.20/79.29 inference(scs_inference,[],[561,81,2,90,89])). % 79.20/79.29 cnf(4194,plain, % 79.20/79.29 (~P12(x41941,x41942,a1)+~E(x41942,f7(a1,a2))), % 79.20/79.29 inference(scs_inference,[],[561,768,81,2,90,89,52])). % 79.20/79.29 cnf(4207,plain, % 79.20/79.29 (~P11(f10(a2),x42071,x42072)+~E(x42071,f3(a2))), % 79.20/79.29 inference(scs_inference,[],[2300,83,2,55])). % 79.20/79.29 cnf(4342,plain, % 79.20/79.29 (P6(a2,f12(a2))), % 79.20/79.29 inference(scs_inference,[],[714,326])). % 79.20/79.29 cnf(5420,plain, % 79.20/79.29 (P16(f3(a2),a2)), % 79.20/79.29 inference(scs_inference,[],[79,105])). % 79.20/79.29 cnf(5422,plain, % 79.20/79.29 (P9(f11(a2),a2)), % 79.20/79.29 inference(scs_inference,[],[79,105,106])). % 79.20/79.29 cnf(5426,plain, % 79.20/79.29 (P11(f10(a2),f11(a2),a1)), % 79.20/79.29 inference(scs_inference,[],[79,105,106,131,132])). % 79.20/79.29 cnf(5428,plain, % 79.20/79.29 (P6(f3(a2),a21)), % 79.20/79.29 inference(scs_inference,[],[79,105,106,131,132,103])). % 79.20/79.29 cnf(5434,plain, % 79.20/79.29 (P12(f3(a2),f10(a2),a1)), % 79.20/79.29 inference(scs_inference,[],[79,561,714,105,106,131,132,103,91,93,140])). % 79.20/79.29 cnf(5436,plain, % 79.20/79.29 (P17(f7(a1,a2),a2)), % 79.20/79.29 inference(scs_inference,[],[79,561,86,714,105,106,131,132,103,91,93,140,127])). % 79.20/79.29 cnf(5440,plain, % 79.20/79.29 (~P12(f3(a2),f3(a2),a1)), % 79.20/79.29 inference(scs_inference,[],[79,987,561,86,714,105,106,131,132,103,91,93,140,127,51,157])). % 79.20/79.29 cnf(5452,plain, % 79.20/79.29 (P5(f10(a2),a24)), % 79.20/79.29 inference(scs_inference,[],[79,4093,4342,987,769,4192,197,76,561,86,170,714,105,106,131,132,103,91,93,140,127,51,157,97,46,126,55,45,68,123])). % 79.20/79.29 cnf(5456,plain, % 79.20/79.29 (~P14(f3(a2),f3(a2))), % 79.20/79.29 inference(scs_inference,[],[79,4093,4342,987,769,4192,197,76,561,86,170,714,105,106,131,132,103,91,93,140,127,51,157,97,46,126,55,45,68,123,129,156])). % 79.20/79.29 cnf(5458,plain, % 79.20/79.29 (P17(f3(a2),a2)), % 79.20/79.29 inference(scs_inference,[],[79,4093,4342,987,769,4192,197,76,561,86,170,714,105,106,131,132,103,91,93,140,127,51,157,97,46,126,55,45,68,123,129,156,101])). % 79.20/79.29 cnf(5464,plain, % 79.20/79.29 (~P8(f10(a2),f3(a2))), % 79.20/79.29 inference(scs_inference,[],[79,4093,4342,987,769,4192,197,76,561,86,170,714,105,106,131,132,103,91,93,140,127,51,157,97,46,126,55,45,68,123,129,156,101,136,137,528])). % 79.20/79.29 cnf(5474,plain, % 79.20/79.29 (~E(f11(a2),f3(a2))), % 79.20/79.29 inference(scs_inference,[],[79,4093,4342,987,769,4192,197,76,561,86,170,714,105,106,131,132,103,91,93,140,127,51,157,97,46,126,55,45,68,123,129,156,101,136,137,528,825,809,4116,4122,4207])). % 79.20/79.29 cnf(5475,plain, % 79.20/79.29 (P14(f3(a2),f10(a2))), % 79.20/79.29 inference(scs_inference,[],[79,4093,4342,987,769,4192,197,76,561,86,170,714,105,106,131,132,103,91,93,140,127,51,157,97,46,126,55,45,68,123,129,156,101,136,137,528,825,809,4116,4122,4207,135])). % 79.20/79.29 cnf(5479,plain, % 79.20/79.29 (P8(f3(a2),f10(a2))), % 79.20/79.29 inference(scs_inference,[],[79,4093,4342,984,987,769,4192,197,76,561,86,170,714,105,106,131,132,103,91,93,140,127,51,157,97,46,126,55,45,68,123,129,156,101,136,137,528,825,809,4116,4122,4207,135,113,100])). % 79.20/79.29 cnf(5481,plain, % 79.20/79.29 (P7(f10(a2))), % 79.20/79.29 inference(scs_inference,[],[79,4093,4342,984,987,769,4192,197,76,561,86,170,714,105,106,131,132,103,91,93,140,127,51,157,97,46,126,55,45,68,123,129,156,101,136,137,528,825,809,4116,4122,4207,135,113,100,94])). % 79.20/79.29 cnf(5496,plain, % 79.20/79.29 (P3(f3(a2))), % 79.20/79.29 inference(scs_inference,[],[5426,5428,5436,75,714,93,91,140,157,261,97])). % 79.20/79.29 cnf(5501,plain, % 79.20/79.29 (P7(f3(a2))), % 79.20/79.29 inference(scs_inference,[],[5426,5428,5436,5479,5481,5434,5440,5452,75,714,93,91,140,157,261,97,52,108,99])). % 79.20/79.29 cnf(5511,plain, % 79.20/79.29 (~P15(f11(a2),a1)), % 79.20/79.29 inference(scs_inference,[],[5426,5428,5436,5479,5481,5434,5440,5452,75,714,93,91,140,157,261,97,52,108,99,155,232,1006,1912,136])). % 79.20/79.29 cnf(5515,plain, % 79.20/79.29 (~P14(f11(a2),f10(a2))), % 79.20/79.29 inference(scs_inference,[],[5426,5428,5436,5479,5481,5434,5440,5452,75,714,93,91,140,157,261,97,52,108,99,155,232,1006,1912,136,137,825])). % 79.20/79.29 cnf(5527,plain, % 79.20/79.29 (P8(f10(a2),f11(a2))), % 79.20/79.29 inference(scs_inference,[],[5426,5428,5436,5456,5479,5481,5434,5440,5452,2300,75,714,191,93,91,140,157,261,97,52,108,99,155,232,1006,1912,136,137,825,528,135,54,107,138,100])). % 79.20/79.29 cnf(5529,plain, % 79.20/79.29 (P7(f11(a2))), % 79.20/79.29 inference(scs_inference,[],[5426,5428,5436,5456,5479,5481,5434,5440,5452,2300,75,714,191,93,91,140,157,261,97,52,108,99,155,232,1006,1912,136,137,825,528,135,54,107,138,100,94])). % 79.20/79.29 cnf(5534,plain, % 79.20/79.29 (P3(f11(a2))), % 79.20/79.29 inference(scs_inference,[],[5529,87])). % 79.20/79.29 cnf(5536,plain, % 79.20/79.29 (~E(f3(a2),f11(a2))), % 79.20/79.29 inference(scs_inference,[],[5515,5529,5475,87,70])). % 79.20/79.29 cnf(5537,plain, % 79.20/79.29 (~P8(f11(a2),f3(a2))), % 79.20/79.29 inference(scs_inference,[],[5515,5527,5529,5475,5464,87,70,113])). % 79.20/79.29 cnf(5542,plain, % 79.20/79.29 (~P2(f12(a2))), % 79.20/79.29 inference(scs_inference,[],[5515,5527,5529,5511,5475,5464,4342,164,87,70,113,108,64,97])). % 79.20/79.29 cnf(5555,plain, % 79.20/79.29 (P15(f3(a2),x55551)+~P5(f3(a2),x55551)), % 79.20/79.29 inference(scs_inference,[],[5534,5501,5542,78,98,44,108])). % 79.20/79.29 cnf(5575,plain, % 79.20/79.29 (~P8(x55751,f3(a2))+~P8(f11(a2),x55751)), % 79.20/79.29 inference(scs_inference,[],[5537,113])). % 79.20/79.29 cnf(5664,plain, % 79.20/79.29 (P14(f11(a2),f3(a2))+~P6(f11(a2),a22)), % 79.20/79.29 inference(scs_inference,[],[79,5422,5536,5420,5496,5534,5458,5428,714,142,145,1912,1006,136,825,137,528,135])). % 79.20/79.29 cnf(5714,plain, % 79.20/79.29 (P12(f3(a2),f11(a2),a1)+P12(f11(a2),f3(a2),a1)), % 79.20/79.29 inference(scs_inference,[],[79,5474,5496,5534,5458,714,145])). % 79.20/79.29 cnf(6131,plain, % 79.20/79.29 (~P14(f11(a2),x61311)+~P8(x61311,f3(a2))), % 79.20/79.29 inference(scs_inference,[],[5575,100])). % 79.20/79.29 cnf(6239,plain, % 79.20/79.29 (~P14(x62391,f3(a2))+~P14(f11(a2),x62391)), % 79.20/79.29 inference(scs_inference,[],[6131,100])). % 79.20/79.29 cnf(6335,plain, % 79.20/79.29 (~P12(f11(a2),x63351,x63352)+~P14(x63351,f3(a2))), % 79.20/79.29 inference(scs_inference,[],[6239,135])). % 79.20/79.29 cnf(6526,plain, % 79.20/79.29 (~P12(x65261,f3(a2),x65262)+~P12(f11(a2),x65261,x65263)), % 79.20/79.29 inference(scs_inference,[],[6335,135])). % 79.20/79.29 cnf(7493,plain, % 79.20/79.29 (~P14(f11(a2),f3(a2))), % 79.20/79.29 inference(scs_inference,[],[5537,100])). % 79.20/79.29 cnf(7510,plain, % 79.20/79.29 (P12(f11(a2),f3(a2),a1)), % 79.20/79.29 inference(scs_inference,[],[5537,75,5420,5428,5422,79,100,5664,4180,90,89,112,70,123,143,5555,5714])). % 79.20/79.29 cnf(7535,plain, % 79.20/79.29 ($false), % 79.20/79.29 inference(scs_inference,[],[7510,7493,6526,4194,135]), % 79.20/79.29 ['proof']). % 79.20/79.29 % SZS output end Proof % 79.20/79.29 % Total time :78.640000s %------------------------------------------------------------------------------