%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : PRO010+4 : 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 : n019.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Mon Jun 24 13:39:44 EDT 2024 % Result : Theorem 88.15s 88.33s % Output : CNFRefutation 88.15s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : PRO010+4 : 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.32 % Computer : n019.cluster.edu % 0.12/0.32 % Model : x86_64 x86_64 % 0.12/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.32 % Memory : 8042.1875MB % 0.12/0.32 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.32 % CPULimit : 300 % 0.12/0.32 % WCLimit : 300 % 0.12/0.32 % DateTime : Thu Jun 20 06:22:24 EDT 2024 % 0.12/0.32 % CPUTime : % 0.53/0.61 start to proof:theBenchmark % 88.09/88.30 %------------------------------------------- % 88.09/88.30 % File :CSE---1.7 % 88.09/88.30 % Problem :theBenchmark % 88.09/88.30 % Transform :cnf % 88.09/88.30 % Format :tptp:raw % 88.09/88.30 % Command :java -jar mcs_scs.jar %d %s % 88.09/88.30 % 88.09/88.31 % Result :Theorem 87.430000s % 88.09/88.31 % Output :CNFRefutation 87.430000s % 88.09/88.31 %------------------------------------------- % 88.09/88.31 %------------------------------------------------------------------------------ % 88.09/88.31 % File : PRO010+4 : TPTP v8.2.0. Released v4.0.0. % 88.09/88.31 % Domain : Processes % 88.09/88.31 % Problem : PSL cliff problem coe-7.1.3 % 88.09/88.31 % Version : Especial : Augmented > Especial. % 88.09/88.31 % English : % 88.09/88.31 % Refs : [Hal09] Halcomb (2009), Email to G. Sutcliffe % 88.09/88.31 % Source : [Hal09] % 88.09/88.31 % Names : unique-cat-p9x__coe-7.1.3-pd [Hal09] % 88.09/88.31 % 88.09/88.31 % Status : Theorem % 88.09/88.31 % Rating : 0.22 v8.1.0, 0.25 v7.5.0, 0.28 v7.4.0, 0.20 v7.3.0, 0.21 v7.2.0, 0.17 v7.0.0, 0.13 v6.4.0, 0.15 v6.3.0, 0.12 v6.2.0, 0.20 v6.0.0, 0.17 v5.5.0, 0.11 v5.3.0, 0.15 v5.2.0, 0.05 v5.1.0, 0.14 v5.0.0, 0.12 v4.1.0, 0.13 v4.0.1, 0.17 v4.0.0 % 88.09/88.31 % Syntax : Number of formulae : 46 ( 12 unt; 0 def) % 88.09/88.31 % Number of atoms : 145 ( 12 equ) % 88.09/88.31 % Maximal formula atoms : 9 ( 3 avg) % 88.09/88.31 % Number of connectives : 119 ( 20 ~; 4 |; 58 &) % 88.09/88.31 % ( 7 <=>; 30 =>; 0 <=; 0 <~>) % 88.09/88.31 % Maximal formula depth : 13 ( 6 avg) % 88.09/88.31 % Maximal term depth : 1 ( 1 avg) % 88.09/88.31 % Number of predicates : 18 ( 17 usr; 0 prp; 1-3 aty) % 88.09/88.31 % Number of functors : 5 ( 5 usr; 5 con; 0-0 aty) % 88.09/88.31 % Number of variables : 110 ( 89 !; 21 ?) % 88.09/88.31 % SPC : FOF_THM_RFO_SEQ % 88.09/88.31 % 88.09/88.31 % Comments : % 88.09/88.31 %------------------------------------------------------------------------------ % 88.09/88.31 fof(sos,axiom, % 88.09/88.31 ! [X0,X1] : % 88.09/88.31 ( ( occurrence_of(X1,X0) % 88.09/88.31 & ~ atomic(X0) ) % 88.09/88.31 => ? [X2] : % 88.09/88.32 ( root(X2,X0) % 88.09/88.32 & subactivity_occurrence(X2,X1) ) ) ). % 88.09/88.32 % 88.09/88.32 fof(sos_01,axiom, % 88.09/88.32 ! [X3,X4,X5,X6,X7] : % 88.09/88.32 ( ( occurrence_of(X4,X3) % 88.09/88.32 & root_occ(X6,X4) % 88.09/88.32 & leaf_occ(X7,X4) % 88.09/88.32 & subactivity_occurrence(X5,X4) % 88.09/88.32 & min_precedes(X6,X5,X3) % 88.09/88.32 & X5 != X7 ) % 88.09/88.32 => min_precedes(X5,X7,X3) ) ). % 88.09/88.32 % 88.09/88.32 fof(sos_02,axiom, % 88.09/88.32 ! [X8,X9,X10,X11] : % 88.09/88.32 ( ( occurrence_of(X9,X8) % 88.09/88.32 & subactivity_occurrence(X10,X9) % 88.09/88.32 & leaf_occ(X11,X9) % 88.09/88.32 & arboreal(X10) % 88.09/88.32 & ~ min_precedes(X10,X11,X8) ) % 88.09/88.32 => X11 = X10 ) ). % 88.09/88.32 % 88.09/88.32 fof(sos_03,axiom, % 88.09/88.32 ! [X12,X13] : % 88.09/88.32 ( occurrence_of(X13,X12) % 88.09/88.32 => ( activity(X12) % 88.09/88.32 & activity_occurrence(X13) ) ) ). % 88.09/88.32 % 88.09/88.32 fof(sos_04,axiom, % 88.09/88.32 ! [X14,X15,X16,X17] : % 88.09/88.32 ( ( occurrence_of(X15,X14) % 88.09/88.32 & arboreal(X16) % 88.09/88.32 & arboreal(X17) % 88.09/88.32 & subactivity_occurrence(X16,X15) % 88.09/88.32 & subactivity_occurrence(X17,X15) ) % 88.09/88.32 => ( min_precedes(X16,X17,X14) % 88.09/88.32 | min_precedes(X17,X16,X14) % 88.09/88.32 | X16 = X17 ) ) ). % 88.09/88.32 % 88.09/88.32 fof(sos_05,axiom, % 88.09/88.32 ! [X18,X19] : % 88.09/88.32 ( root(X19,X18) % 88.09/88.32 => ? [X20] : % 88.09/88.32 ( subactivity(X20,X18) % 88.09/88.32 & atocc(X19,X20) ) ) ). % 88.09/88.32 % 88.09/88.32 fof(sos_06,axiom, % 88.09/88.32 ! [X21,X22,X23] : % 88.09/88.32 ( min_precedes(X22,X23,X21) % 88.09/88.32 => ? [X24] : % 88.09/88.32 ( occurrence_of(X24,X21) % 88.09/88.32 & subactivity_occurrence(X22,X24) % 88.09/88.32 & subactivity_occurrence(X23,X24) ) ) ). % 88.09/88.32 % 88.09/88.32 fof(sos_07,axiom, % 88.09/88.32 ! [X25,X26] : % 88.09/88.32 ( ( leaf(X25,X26) % 88.09/88.32 & ~ atomic(X26) ) % 88.09/88.32 => ? [X27] : % 88.09/88.32 ( occurrence_of(X27,X26) % 88.09/88.32 & leaf_occ(X25,X27) ) ) ). % 88.09/88.32 % 88.09/88.32 fof(sos_08,axiom, % 88.09/88.32 ! [X28,X29,X30] : % 88.09/88.32 ( ( occurrence_of(X28,X29) % 88.09/88.32 & occurrence_of(X28,X30) ) % 88.09/88.32 => X29 = X30 ) ). % 88.09/88.32 % 88.09/88.32 fof(sos_09,axiom, % 88.09/88.32 ! [X31,X32,X33] : % 88.09/88.32 ( ( occurrence_of(X31,X33) % 88.09/88.32 & leaf_occ(X32,X31) ) % 88.09/88.32 => ~ ? [X34] : min_precedes(X32,X34,X33) ) ). % 88.09/88.32 % 88.09/88.32 fof(sos_10,axiom, % 88.09/88.32 ! [X35,X36,X37] : % 88.09/88.32 ( ( occurrence_of(X35,X37) % 88.09/88.32 & root_occ(X36,X35) ) % 88.09/88.32 => ~ ? [X38] : min_precedes(X38,X36,X37) ) ). % 88.09/88.32 % 88.09/88.32 fof(sos_11,axiom, % 88.09/88.32 ! [X39,X40] : % 88.09/88.32 ( subactivity_occurrence(X39,X40) % 88.09/88.32 => ( activity_occurrence(X39) % 88.09/88.32 & activity_occurrence(X40) ) ) ). % 88.09/88.32 % 88.09/88.32 fof(sos_12,axiom, % 88.09/88.32 ! [X41] : % 88.09/88.32 ( activity_occurrence(X41) % 88.09/88.32 => ? [X42] : % 88.09/88.32 ( activity(X42) % 88.09/88.32 & occurrence_of(X41,X42) ) ) ). % 88.09/88.32 % 88.09/88.32 fof(sos_13,axiom, % 88.09/88.32 ! [X43] : % 88.09/88.32 ( legal(X43) % 88.09/88.32 => arboreal(X43) ) ). % 88.09/88.32 % 88.09/88.32 fof(sos_14,axiom, % 88.09/88.32 ! [X44,X45] : % 88.09/88.32 ( atocc(X44,X45) % 88.09/88.32 <=> ? [X46] : % 88.09/88.32 ( subactivity(X45,X46) % 88.09/88.32 & atomic(X46) % 88.09/88.32 & occurrence_of(X44,X46) ) ) ). % 88.09/88.32 % 88.09/88.32 fof(sos_15,axiom, % 88.09/88.32 ! [X47,X48] : % 88.09/88.32 ( leaf(X47,X48) % 88.09/88.32 <=> ( ( root(X47,X48) % 88.09/88.32 | ? [X49] : min_precedes(X49,X47,X48) ) % 88.09/88.32 & ~ ? [X50] : min_precedes(X47,X50,X48) ) ) ). % 88.09/88.32 % 88.09/88.32 fof(sos_16,axiom, % 88.09/88.32 ! [X51,X52] : % 88.09/88.32 ( occurrence_of(X51,X52) % 88.09/88.32 => ( arboreal(X51) % 88.09/88.32 <=> atomic(X52) ) ) ). % 88.09/88.32 % 88.09/88.32 fof(sos_17,axiom, % 88.09/88.32 ! [X53,X54] : % 88.09/88.32 ( root(X53,X54) % 88.09/88.32 => legal(X53) ) ). % 88.09/88.32 % 88.09/88.32 fof(sos_18,axiom, % 88.09/88.32 ! [X55,X56] : % 88.09/88.32 ( leaf_occ(X55,X56) % 88.09/88.32 <=> ? [X57] : % 88.09/88.32 ( occurrence_of(X56,X57) % 88.09/88.32 & subactivity_occurrence(X55,X56) % 88.09/88.32 & leaf(X55,X57) ) ) ). % 88.09/88.32 % 88.09/88.32 fof(sos_19,axiom, % 88.09/88.32 ! [X58,X59] : % 88.09/88.32 ( root_occ(X58,X59) % 88.09/88.32 <=> ? [X60] : % 88.09/88.32 ( occurrence_of(X59,X60) % 88.09/88.32 & subactivity_occurrence(X58,X59) % 88.09/88.32 & root(X58,X60) ) ) ). % 88.09/88.32 % 88.09/88.32 fof(sos_20,axiom, % 88.09/88.32 ! [X61,X62] : % 88.09/88.32 ( earlier(X61,X62) % 88.09/88.32 => ~ earlier(X62,X61) ) ). % 88.09/88.32 % 88.09/88.32 fof(sos_21,axiom, % 88.09/88.32 ! [X63,X64] : % 88.09/88.32 ( precedes(X63,X64) % 88.09/88.32 <=> ( earlier(X63,X64) % 88.09/88.32 & legal(X64) ) ) ). % 88.09/88.32 % 88.09/88.32 fof(sos_22,axiom, % 88.09/88.32 ! [X65,X66,X67] : % 88.09/88.32 ( min_precedes(X65,X66,X67) % 88.09/88.32 => ~ root(X66,X67) ) ). % 88.09/88.32 % 88.09/88.32 fof(sos_23,axiom, % 88.09/88.32 ! [X68,X69,X70] : % 88.09/88.32 ( min_precedes(X68,X69,X70) % 88.09/88.32 => ? [X71] : % 88.09/88.32 ( root(X71,X70) % 88.09/88.32 & min_precedes(X71,X69,X70) ) ) ). % 88.09/88.32 % 88.09/88.32 fof(sos_24,axiom, % 88.09/88.32 ! [X72,X73,X74] : % 88.09/88.32 ( min_precedes(X72,X73,X74) % 88.09/88.32 => precedes(X72,X73) ) ). % 88.09/88.32 % 88.09/88.32 fof(sos_25,axiom, % 88.09/88.32 ! [X75,X76,X77] : % 88.09/88.32 ( next_subocc(X75,X76,X77) % 88.09/88.32 => ( arboreal(X75) % 88.09/88.32 & arboreal(X76) ) ) ). % 88.09/88.32 % 88.09/88.32 fof(sos_26,axiom, % 88.09/88.32 ! [X78,X79,X80] : % 88.09/88.32 ( next_subocc(X78,X79,X80) % 88.09/88.32 <=> ( min_precedes(X78,X79,X80) % 88.09/88.32 & ~ ? [X81] : % 88.09/88.32 ( min_precedes(X78,X81,X80) % 88.09/88.32 & min_precedes(X81,X79,X80) ) ) ) ). % 88.09/88.32 % 88.09/88.32 fof(sos_27,axiom, % 88.09/88.32 ! [X82,X83,X84,X85] : % 88.09/88.32 ( ( min_precedes(X82,X83,X84) % 88.09/88.32 & occurrence_of(X85,X84) % 88.09/88.32 & subactivity_occurrence(X83,X85) ) % 88.09/88.32 => subactivity_occurrence(X82,X85) ) ). % 88.09/88.32 % 88.09/88.32 fof(sos_28,axiom, % 88.09/88.32 ! [X86,X87,X88,X89] : % 88.09/88.32 ( ( occurrence_of(X88,X89) % 88.09/88.32 & ~ atomic(X89) % 88.09/88.32 & leaf_occ(X86,X88) % 88.09/88.32 & leaf_occ(X87,X88) ) % 88.09/88.32 => X86 = X87 ) ). % 88.09/88.32 % 88.09/88.32 fof(sos_29,axiom, % 88.09/88.32 ! [X90,X91,X92,X93] : % 88.09/88.32 ( ( occurrence_of(X92,X93) % 88.09/88.32 & root_occ(X90,X92) % 88.09/88.32 & root_occ(X91,X92) ) % 88.09/88.32 => X90 = X91 ) ). % 88.09/88.32 % 88.09/88.32 fof(sos_30,axiom, % 88.09/88.32 ! [X94,X95,X96] : % 88.09/88.32 ( ( earlier(X94,X95) % 88.09/88.32 & earlier(X95,X96) ) % 88.09/88.32 => earlier(X94,X96) ) ). % 88.09/88.32 % 88.09/88.32 fof(sos_31,axiom, % 88.09/88.32 ! [X97,X98,X99,X100] : % 88.09/88.32 ( ( min_precedes(X97,X98,X100) % 88.09/88.32 & min_precedes(X97,X99,X100) % 88.09/88.32 & precedes(X98,X99) ) % 88.09/88.32 => min_precedes(X98,X99,X100) ) ). % 88.09/88.32 % 88.09/88.32 fof(sos_32,axiom, % 88.09/88.32 ! [X101] : % 88.09/88.32 ( occurrence_of(X101,tptp0) % 88.09/88.32 => ? [X102,X103,X104] : % 88.09/88.32 ( occurrence_of(X102,tptp3) % 88.09/88.32 & root_occ(X102,X101) % 88.09/88.32 & occurrence_of(X103,tptp4) % 88.09/88.32 & next_subocc(X102,X103,tptp0) % 88.15/88.32 & ( occurrence_of(X104,tptp1) % 88.15/88.32 | occurrence_of(X104,tptp2) ) % 88.15/88.32 & next_subocc(X103,X104,tptp0) % 88.15/88.32 & leaf_occ(X104,X101) ) ) ). % 88.15/88.32 % 88.15/88.32 fof(sos_33,axiom, % 88.15/88.32 activity(tptp0) ). % 88.15/88.32 % 88.15/88.32 fof(sos_34,axiom, % 88.15/88.32 ~ atomic(tptp0) ). % 88.15/88.32 % 88.15/88.32 fof(sos_35,axiom, % 88.15/88.32 atomic(tptp4) ). % 88.15/88.32 % 88.15/88.32 fof(sos_36,axiom, % 88.15/88.32 atomic(tptp1) ). % 88.15/88.32 % 88.15/88.32 fof(sos_37,axiom, % 88.15/88.32 atomic(tptp2) ). % 88.15/88.32 % 88.15/88.32 fof(sos_38,axiom, % 88.15/88.32 atomic(tptp3) ). % 88.15/88.32 % 88.15/88.32 fof(sos_39,axiom, % 88.15/88.32 tptp4 != tptp3 ). % 88.15/88.32 % 88.15/88.32 fof(sos_40,axiom, % 88.15/88.32 tptp4 != tptp1 ). % 88.15/88.32 % 88.15/88.32 fof(sos_41,axiom, % 88.15/88.32 tptp4 != tptp2 ). % 88.15/88.32 % 88.15/88.32 fof(sos_42,axiom, % 88.15/88.32 tptp3 != tptp1 ). % 88.15/88.32 % 88.15/88.32 fof(sos_43,axiom, % 88.15/88.32 tptp3 != tptp2 ). % 88.15/88.32 % 88.15/88.32 fof(sos_44,axiom, % 88.15/88.32 tptp1 != tptp2 ). % 88.15/88.32 % 88.15/88.32 fof(goals,conjecture, % 88.15/88.32 ! [X105] : % 88.15/88.33 ( occurrence_of(X105,tptp0) % 88.15/88.33 => ? [X106,X107] : % 88.15/88.33 ( leaf_occ(X107,X105) % 88.15/88.33 & ( occurrence_of(X107,tptp1) % 88.15/88.33 => ~ ? [X108] : % 88.15/88.33 ( occurrence_of(X108,tptp2) % 88.15/88.33 & min_precedes(X106,X108,tptp0) ) ) % 88.15/88.33 & ( occurrence_of(X107,tptp2) % 88.15/88.33 => ~ ? [X109] : % 88.15/88.33 ( occurrence_of(X109,tptp1) % 88.15/88.33 & min_precedes(X106,X109,tptp0) ) ) ) ) ). % 88.15/88.33 % 88.15/88.33 %------------------------------------------------------------------------------ % 88.15/88.33 %------------------------------------------- % 88.15/88.33 % Proof found % 88.15/88.33 % SZS status Theorem for theBenchmark % 88.15/88.33 % SZS output start Proof % 88.15/88.33 %ClaNum:156(EqnAxiom:67) % 88.15/88.33 %VarNum:437(SingletonVarNum:181) % 88.15/88.33 %MaxLitNum:8 % 88.15/88.33 %MaxfuncDepth:1 % 88.15/88.33 %SharedTerms:19 % 88.15/88.33 %goalClause: 73 101 120 121 129 133 134 140 141 144 % 88.15/88.33 %singleGoalClaCount:1 % 88.15/88.33 [68]P1(a1) % 88.15/88.33 [69]P1(a23) % 88.15/88.33 [70]P1(a2) % 88.15/88.33 [71]P1(a22) % 88.15/88.33 [72]P2(a3) % 88.15/88.33 [73]P6(a4,a3) % 88.15/88.33 [74]~E(a1,a23) % 88.15/88.33 [75]~E(a1,a2) % 88.15/88.33 [76]~E(a2,a23) % 88.15/88.33 [77]~E(a1,a22) % 88.15/88.33 [78]~E(a22,a23) % 88.15/88.33 [79]~E(a22,a2) % 88.15/88.33 [80]~P1(a3) % 88.15/88.33 [81]~P7(x811)+P3(x811) % 88.15/88.33 [82]~P4(x821)+P2(f11(x821)) % 88.15/88.33 [89]~P4(x891)+P6(x891,f11(x891)) % 88.15/88.33 [95]~P6(x951,a3)+P6(f5(x951),a1) % 88.15/88.33 [96]~P6(x961,a3)+P6(f9(x961),a23) % 88.15/88.33 [97]~P6(x971,a3)+P16(f5(x971),x971) % 88.15/88.33 [98]~P6(x981,a3)+P8(f10(x981),x981) % 88.15/88.33 [125]~P6(x1251,a3)+P11(f5(x1251),f9(x1251),a3) % 88.15/88.33 [126]~P6(x1261,a3)+P11(f9(x1261),f10(x1261),a3) % 88.15/88.33 [83]P2(x831)+~P6(x832,x831) % 88.15/88.33 [84]P4(x841)+~P6(x841,x842) % 88.15/88.33 [85]P4(x851)+~P13(x852,x851) % 88.15/88.33 [86]P4(x861)+~P13(x861,x862) % 88.15/88.33 [87]P7(x871)+~P14(x871,x872) % 88.15/88.33 [88]P7(x881)+~P15(x882,x881) % 88.15/88.33 [92]~P16(x921,x922)+P13(x921,x922) % 88.15/88.33 [93]~P8(x931,x932)+P13(x931,x932) % 88.15/88.33 [94]~P15(x941,x942)+P9(x941,x942) % 88.15/88.33 [100]~P9(x1002,x1001)+~P9(x1001,x1002) % 88.15/88.33 [103]~P5(x1031,x1032)+P1(f18(x1031,x1032)) % 88.15/88.33 [106]~P5(x1061,x1062)+P6(x1061,f18(x1061,x1062)) % 88.15/88.33 [107]~P8(x1072,x1071)+P6(x1071,f19(x1072,x1071)) % 88.15/88.33 [108]~P16(x1082,x1081)+P6(x1081,f6(x1082,x1081)) % 88.15/88.33 [109]~P16(x1091,x1092)+P14(x1091,f6(x1091,x1092)) % 88.15/88.33 [110]~P5(x1102,x1101)+P17(x1101,f18(x1102,x1101)) % 88.15/88.33 [111]~P14(x1111,x1112)+P5(x1111,f12(x1112,x1111)) % 88.15/88.33 [112]~P8(x1121,x1122)+P10(x1121,f19(x1121,x1122)) % 88.15/88.33 [113]~P14(x1132,x1131)+P17(f12(x1131,x1132),x1131) % 88.15/88.33 [127]P3(x1271)+~P11(x1272,x1271,x1273) % 88.15/88.33 [128]P3(x1281)+~P11(x1281,x1282,x1283) % 88.15/88.33 [130]P15(x1301,x1302)+~P12(x1301,x1302,x1303) % 88.15/88.33 [131]~P14(x1311,x1312)+~P12(x1313,x1311,x1312) % 88.15/88.33 [132]~P10(x1321,x1322)+~P12(x1321,x1323,x1322) % 88.15/88.33 [142]~P11(x1421,x1422,x1423)+P12(x1421,x1422,x1423) % 88.15/88.33 [147]~P12(x1473,x1471,x1472)+P13(x1471,f17(x1472,x1473,x1471)) % 88.15/88.33 [148]~P12(x1481,x1483,x1482)+P13(x1481,f17(x1482,x1481,x1483)) % 88.15/88.33 [149]~P12(x1492,x1493,x1491)+P6(f17(x1491,x1492,x1493),x1491) % 88.15/88.33 [150]~P12(x1501,x1502,x1503)+P14(f7(x1501,x1502,x1503),x1503) % 88.15/88.33 [152]~P12(x1521,x1522,x1523)+P12(f7(x1521,x1522,x1523),x1522,x1523) % 88.15/88.33 [101]P6(x1011,a22)+~P8(x1011,a4)+P6(x1011,a2) % 88.15/88.33 [104]~P6(x1041,a3)+P6(f10(x1041),a2)+P6(f10(x1041),a22) % 88.15/88.33 [90]~P6(x902,x901)+P1(x901)+~P3(x902) % 88.15/88.33 [91]~P6(x911,x912)+P3(x911)+~P1(x912) % 88.15/88.33 [99]~P7(x992)+~P9(x991,x992)+P15(x991,x992) % 88.15/88.33 [115]~P10(x1152,x1151)+P1(x1151)+P8(x1152,f16(x1152,x1151)) % 88.15/88.33 [116]~P10(x1162,x1161)+P1(x1161)+P6(f16(x1162,x1161),x1161) % 88.15/88.33 [117]~P6(x1172,x1171)+P1(x1171)+P14(f13(x1171,x1172),x1171) % 88.15/88.33 [118]~P6(x1182,x1181)+P1(x1181)+P13(f13(x1181,x1182),x1182) % 88.15/88.33 [120]~P8(x1201,a4)+P6(x1201,a2)+P6(f14(x1202,x1201),a2) % 88.15/88.33 [121]~P8(x1211,a4)+P6(x1211,a22)+P6(f15(x1212,x1211),a22) % 88.15/88.33 [129]~P8(x1292,a4)+P6(f14(x1291,x1292),a2)+P6(f15(x1291,x1292),a22) % 88.15/88.33 [133]~P8(x1331,a4)+P6(x1331,a2)+P12(x1332,f14(x1332,x1331),a3) % 88.15/88.33 [134]~P8(x1341,a4)+P6(x1341,a22)+P12(x1342,f15(x1342,x1341),a3) % 88.15/88.33 [135]~P14(x1351,x1352)+P10(x1351,x1352)+P12(x1351,f20(x1351,x1352),x1352) % 88.15/88.33 [136]~P10(x1361,x1362)+P14(x1361,x1362)+P12(f21(x1361,x1362),x1361,x1362) % 88.15/88.33 [140]~P8(x1402,a4)+P12(x1401,f14(x1401,x1402),a3)+P6(f15(x1401,x1402),a22) % 88.15/88.33 [141]~P8(x1412,a4)+P12(x1411,f15(x1411,x1412),a3)+P6(f14(x1411,x1412),a2) % 88.15/88.33 [144]~P8(x1442,a4)+P12(x1441,f14(x1441,x1442),a3)+P12(x1441,f15(x1441,x1442),a3) % 88.15/88.33 [102]~P6(x1023,x1021)+E(x1021,x1022)+~P6(x1023,x1022) % 88.15/88.33 [105]~P9(x1051,x1053)+P9(x1051,x1052)+~P9(x1053,x1052) % 88.15/88.33 [145]P10(x1451,x1452)+~P12(x1453,x1451,x1452)+P12(x1451,f20(x1451,x1452),x1452) % 88.15/88.33 [155]~P12(x1551,x1552,x1553)+P11(x1551,x1552,x1553)+P12(x1551,f8(x1551,x1552,x1553),x1553) % 88.15/88.33 [156]~P12(x1561,x1562,x1563)+P11(x1561,x1562,x1563)+P12(f8(x1561,x1562,x1563),x1562,x1563) % 88.15/88.33 [137]~P6(x1371,x1372)+~P12(x1374,x1373,x1372)+~P16(x1373,x1371) % 88.15/88.33 [138]~P6(x1381,x1382)+~P12(x1383,x1384,x1382)+~P8(x1383,x1381) % 88.15/88.33 [154]~P11(x1544,x1542,x1543)+~P12(x1541,x1542,x1543)+~P12(x1544,x1541,x1543) % 88.15/88.33 [114]~P6(x1141,x1143)+~P17(x1142,x1143)+P5(x1141,x1142)+~P1(x1143) % 88.15/88.33 [123]~P14(x1231,x1233)+~P13(x1231,x1232)+P16(x1231,x1232)+~P6(x1232,x1233) % 88.15/88.33 [124]~P13(x1241,x1242)+~P10(x1241,x1243)+P8(x1241,x1242)+~P6(x1242,x1243) % 88.15/88.33 [119]~P16(x1192,x1193)+~P16(x1191,x1193)+E(x1191,x1192)+~P6(x1193,x1194) % 88.15/88.33 [143]~P12(x1431,x1434,x1433)+P13(x1431,x1432)+~P6(x1432,x1433)+~P13(x1434,x1432) % 88.15/88.33 [153]~P15(x1531,x1532)+~P12(x1534,x1531,x1533)+P12(x1531,x1532,x1533)+~P12(x1534,x1532,x1533) % 88.15/88.33 [122]~P8(x1222,x1224)+~P8(x1221,x1224)+E(x1221,x1222)+~P6(x1224,x1223)+P1(x1223) % 88.15/88.33 [139]~P3(x1391)+~P13(x1391,x1394)+~P8(x1392,x1394)+E(x1391,x1392)+P12(x1391,x1392,x1393)+~P6(x1394,x1393) % 88.15/88.33 [151]~P13(x1512,x1514)+~P8(x1511,x1514)+~P12(x1515,x1512,x1513)+E(x1511,x1512)+P12(x1512,x1511,x1513)+~P6(x1514,x1513)+~P16(x1515,x1514) % 88.15/88.33 [146]P12(x1461,x1462,x1463)+~P3(x1462)+~P3(x1461)+~P13(x1462,x1464)+~P13(x1461,x1464)+E(x1461,x1462)+P12(x1462,x1461,x1463)+~P6(x1464,x1463) % 88.15/88.33 %EqnAxiom % 88.15/88.33 [1]E(x11,x11) % 88.15/88.33 [2]E(x22,x21)+~E(x21,x22) % 88.15/88.33 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 88.15/88.33 [4]~E(x41,x42)+E(f11(x41),f11(x42)) % 88.15/88.33 [5]~E(x51,x52)+E(f8(x51,x53,x54),f8(x52,x53,x54)) % 88.15/88.33 [6]~E(x61,x62)+E(f8(x63,x61,x64),f8(x63,x62,x64)) % 88.15/88.33 [7]~E(x71,x72)+E(f8(x73,x74,x71),f8(x73,x74,x72)) % 88.15/88.33 [8]~E(x81,x82)+E(f5(x81),f5(x82)) % 88.15/88.33 [9]~E(x91,x92)+E(f9(x91),f9(x92)) % 88.15/88.33 [10]~E(x101,x102)+E(f7(x101,x103,x104),f7(x102,x103,x104)) % 88.15/88.33 [11]~E(x111,x112)+E(f7(x113,x111,x114),f7(x113,x112,x114)) % 88.15/88.33 [12]~E(x121,x122)+E(f7(x123,x124,x121),f7(x123,x124,x122)) % 88.15/88.33 [13]~E(x131,x132)+E(f10(x131),f10(x132)) % 88.15/88.33 [14]~E(x141,x142)+E(f18(x141,x143),f18(x142,x143)) % 88.15/88.33 [15]~E(x151,x152)+E(f18(x153,x151),f18(x153,x152)) % 88.15/88.33 [16]~E(x161,x162)+E(f20(x161,x163),f20(x162,x163)) % 88.15/88.33 [17]~E(x171,x172)+E(f20(x173,x171),f20(x173,x172)) % 88.15/88.33 [18]~E(x181,x182)+E(f14(x181,x183),f14(x182,x183)) % 88.15/88.33 [19]~E(x191,x192)+E(f14(x193,x191),f14(x193,x192)) % 88.15/88.33 [20]~E(x201,x202)+E(f15(x201,x203),f15(x202,x203)) % 88.15/88.33 [21]~E(x211,x212)+E(f15(x213,x211),f15(x213,x212)) % 88.15/88.33 [22]~E(x221,x222)+E(f19(x221,x223),f19(x222,x223)) % 88.15/88.33 [23]~E(x231,x232)+E(f19(x233,x231),f19(x233,x232)) % 88.15/88.33 [24]~E(x241,x242)+E(f6(x241,x243),f6(x242,x243)) % 88.15/88.33 [25]~E(x251,x252)+E(f6(x253,x251),f6(x253,x252)) % 88.15/88.33 [26]~E(x261,x262)+E(f17(x261,x263,x264),f17(x262,x263,x264)) % 88.15/88.33 [27]~E(x271,x272)+E(f17(x273,x271,x274),f17(x273,x272,x274)) % 88.15/88.33 [28]~E(x281,x282)+E(f17(x283,x284,x281),f17(x283,x284,x282)) % 88.15/88.33 [29]~E(x291,x292)+E(f21(x291,x293),f21(x292,x293)) % 88.15/88.33 [30]~E(x301,x302)+E(f21(x303,x301),f21(x303,x302)) % 88.15/88.33 [31]~E(x311,x312)+E(f12(x311,x313),f12(x312,x313)) % 88.15/88.33 [32]~E(x321,x322)+E(f12(x323,x321),f12(x323,x322)) % 88.15/88.33 [33]~E(x331,x332)+E(f13(x331,x333),f13(x332,x333)) % 88.15/88.33 [34]~E(x341,x342)+E(f13(x343,x341),f13(x343,x342)) % 88.15/88.33 [35]~E(x351,x352)+E(f16(x351,x353),f16(x352,x353)) % 88.15/88.33 [36]~E(x361,x362)+E(f16(x363,x361),f16(x363,x362)) % 88.15/88.33 [37]~P1(x371)+P1(x372)+~E(x371,x372) % 88.15/88.33 [38]P12(x382,x383,x384)+~E(x381,x382)+~P12(x381,x383,x384) % 88.15/88.33 [39]P12(x393,x392,x394)+~E(x391,x392)+~P12(x393,x391,x394) % 88.15/88.33 [40]P12(x403,x404,x402)+~E(x401,x402)+~P12(x403,x404,x401) % 88.15/88.33 [41]P8(x412,x413)+~E(x411,x412)+~P8(x411,x413) % 88.15/88.33 [42]P8(x423,x422)+~E(x421,x422)+~P8(x423,x421) % 88.15/88.33 [43]P11(x432,x433,x434)+~E(x431,x432)+~P11(x431,x433,x434) % 88.15/88.33 [44]P11(x443,x442,x444)+~E(x441,x442)+~P11(x443,x441,x444) % 88.15/88.33 [45]P11(x453,x454,x452)+~E(x451,x452)+~P11(x453,x454,x451) % 88.15/88.33 [46]~P2(x461)+P2(x462)+~E(x461,x462) % 88.15/88.33 [47]P6(x472,x473)+~E(x471,x472)+~P6(x471,x473) % 88.15/88.33 [48]P6(x483,x482)+~E(x481,x482)+~P6(x483,x481) % 88.15/88.33 [49]P16(x492,x493)+~E(x491,x492)+~P16(x491,x493) % 88.15/88.33 [50]P16(x503,x502)+~E(x501,x502)+~P16(x503,x501) % 88.15/88.33 [51]~P3(x511)+P3(x512)+~E(x511,x512) % 88.15/88.33 [52]~P7(x521)+P7(x522)+~E(x521,x522) % 88.15/88.33 [53]P13(x532,x533)+~E(x531,x532)+~P13(x531,x533) % 88.15/88.33 [54]P13(x543,x542)+~E(x541,x542)+~P13(x543,x541) % 88.15/88.33 [55]~P4(x551)+P4(x552)+~E(x551,x552) % 88.15/88.33 [56]P10(x562,x563)+~E(x561,x562)+~P10(x561,x563) % 88.15/88.33 [57]P10(x573,x572)+~E(x571,x572)+~P10(x573,x571) % 88.15/88.33 [58]P15(x582,x583)+~E(x581,x582)+~P15(x581,x583) % 88.15/88.33 [59]P15(x593,x592)+~E(x591,x592)+~P15(x593,x591) % 88.15/88.33 [60]P9(x602,x603)+~E(x601,x602)+~P9(x601,x603) % 88.15/88.33 [61]P9(x613,x612)+~E(x611,x612)+~P9(x613,x611) % 88.15/88.33 [62]P14(x622,x623)+~E(x621,x622)+~P14(x621,x623) % 88.15/88.33 [63]P14(x633,x632)+~E(x631,x632)+~P14(x633,x631) % 88.15/88.33 [64]P5(x642,x643)+~E(x641,x642)+~P5(x641,x643) % 88.15/88.33 [65]P5(x653,x652)+~E(x651,x652)+~P5(x653,x651) % 88.15/88.33 [66]P17(x662,x663)+~E(x661,x662)+~P17(x661,x663) % 88.15/88.33 [67]P17(x673,x672)+~E(x671,x672)+~P17(x673,x671) % 88.15/88.33 % 88.15/88.33 %------------------------------------------- % 88.15/88.33 cnf(4064,plain, % 88.15/88.33 (~P6(x40641,a2)+~P6(x40641,a22)), % 88.15/88.33 inference(scs_inference,[],[79,102])). % 88.15/88.33 cnf(4588,plain, % 88.15/88.33 (P8(f10(a4),a4)), % 88.15/88.33 inference(scs_inference,[],[73,98])). % 88.15/88.33 cnf(6291,plain, % 88.15/88.33 (~P12(f10(a4),x62911,a3)), % 88.15/88.33 inference(scs_inference,[],[4588,73,138])). % 88.15/88.33 cnf(6296,plain, % 88.15/88.33 (P6(f10(a4),a2)), % 88.15/88.33 inference(scs_inference,[],[6291,4588,133])). % 88.15/88.33 cnf(6309,plain, % 88.15/88.33 ($false), % 88.15/88.33 inference(scs_inference,[],[6296,6291,4588,4064,134]), % 88.15/88.33 ['proof']). % 88.15/88.33 % SZS output end Proof % 88.15/88.33 % Total time :87.430000s %------------------------------------------------------------------------------