%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : PRO009+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 : n022.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 58.63s 58.73s % Output : CNFRefutation 58.63s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : PRO009+4 : TPTP v8.2.0. Released v4.0.0. % 0.07/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.12/0.33 % Computer : n022.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:40:54 EDT 2024 % 0.12/0.33 % CPUTime : % 0.46/0.56 start to proof:theBenchmark % 58.63/58.70 %------------------------------------------- % 58.63/58.70 % File :CSE---1.7 % 58.63/58.70 % Problem :theBenchmark % 58.63/58.70 % Transform :cnf % 58.63/58.70 % Format :tptp:raw % 58.63/58.70 % Command :java -jar mcs_scs.jar %d %s % 58.63/58.70 % 58.63/58.70 % Result :Theorem 58.090000s % 58.63/58.70 % Output :CNFRefutation 58.090000s % 58.63/58.70 %------------------------------------------- % 58.63/58.71 %------------------------------------------------------------------------------ % 58.63/58.71 % File : PRO009+4 : TPTP v8.2.0. Released v4.0.0. % 58.63/58.71 % Domain : Processes % 58.63/58.71 % Problem : PSL cliff problem coe-7.1.2 % 58.63/58.71 % Version : Especial : Augmented > Especial. % 58.63/58.71 % English : % 58.63/58.71 % Refs : [Hal09] Halcomb (2009), Email to G. Sutcliffe % 58.63/58.71 % Source : [Hal09] % 58.63/58.71 % Names : unique-cat-p9x__coe-7.1.2-pd [Hal09] % 58.63/58.71 % 58.63/58.71 % Status : Theorem % 58.63/58.71 % Rating : 0.19 v8.2.0, 0.17 v8.1.0, 0.19 v7.5.0, 0.22 v7.4.0, 0.10 v7.2.0, 0.07 v7.1.0, 0.09 v7.0.0, 0.10 v6.4.0, 0.15 v6.3.0, 0.17 v6.2.0, 0.24 v6.1.0, 0.27 v6.0.0, 0.17 v5.5.0, 0.19 v5.4.0, 0.25 v5.3.0, 0.33 v5.2.0, 0.10 v5.1.0, 0.19 v5.0.0, 0.17 v4.1.0, 0.22 v4.0.0 % 58.63/58.71 % Syntax : Number of formulae : 46 ( 12 unt; 0 def) % 58.63/58.71 % Number of atoms : 144 ( 12 equ) % 58.63/58.71 % Maximal formula atoms : 9 ( 3 avg) % 58.63/58.71 % Number of connectives : 116 ( 18 ~; 5 |; 58 &) % 58.63/58.71 % ( 7 <=>; 28 =>; 0 <=; 0 <~>) % 58.63/58.71 % Maximal formula depth : 13 ( 6 avg) % 58.63/58.71 % Maximal term depth : 1 ( 1 avg) % 58.63/58.71 % Number of predicates : 18 ( 17 usr; 0 prp; 1-3 aty) % 58.63/58.71 % Number of functors : 5 ( 5 usr; 5 con; 0-0 aty) % 58.63/58.71 % Number of variables : 108 ( 89 !; 19 ?) % 58.63/58.71 % SPC : FOF_THM_RFO_SEQ % 58.63/58.71 % 58.63/58.71 % Comments : % 58.63/58.71 %------------------------------------------------------------------------------ % 58.63/58.71 fof(sos,axiom, % 58.63/58.71 ! [X0,X1] : % 58.63/58.71 ( ( occurrence_of(X1,X0) % 58.63/58.71 & ~ atomic(X0) ) % 58.63/58.71 => ? [X2] : % 58.63/58.71 ( root(X2,X0) % 58.63/58.71 & subactivity_occurrence(X2,X1) ) ) ). % 58.63/58.71 % 58.63/58.71 fof(sos_01,axiom, % 58.63/58.71 ! [X3,X4,X5,X6,X7] : % 58.63/58.71 ( ( occurrence_of(X4,X3) % 58.63/58.71 & root_occ(X6,X4) % 58.63/58.71 & leaf_occ(X7,X4) % 58.63/58.71 & subactivity_occurrence(X5,X4) % 58.63/58.71 & min_precedes(X6,X5,X3) % 58.63/58.71 & X5 != X7 ) % 58.63/58.71 => min_precedes(X5,X7,X3) ) ). % 58.63/58.71 % 58.63/58.71 fof(sos_02,axiom, % 58.63/58.71 ! [X8,X9,X10,X11] : % 58.63/58.71 ( ( occurrence_of(X9,X8) % 58.63/58.71 & subactivity_occurrence(X10,X9) % 58.63/58.71 & leaf_occ(X11,X9) % 58.63/58.71 & arboreal(X10) % 58.63/58.71 & ~ min_precedes(X10,X11,X8) ) % 58.63/58.71 => X11 = X10 ) ). % 58.63/58.71 % 58.63/58.71 fof(sos_03,axiom, % 58.63/58.71 ! [X12,X13] : % 58.63/58.71 ( occurrence_of(X13,X12) % 58.63/58.71 => ( activity(X12) % 58.63/58.71 & activity_occurrence(X13) ) ) ). % 58.63/58.72 % 58.63/58.72 fof(sos_04,axiom, % 58.63/58.72 ! [X14,X15,X16,X17] : % 58.63/58.72 ( ( occurrence_of(X15,X14) % 58.63/58.72 & arboreal(X16) % 58.63/58.72 & arboreal(X17) % 58.63/58.72 & subactivity_occurrence(X16,X15) % 58.63/58.72 & subactivity_occurrence(X17,X15) ) % 58.63/58.72 => ( min_precedes(X16,X17,X14) % 58.63/58.72 | min_precedes(X17,X16,X14) % 58.63/58.72 | X16 = X17 ) ) ). % 58.63/58.72 % 58.63/58.72 fof(sos_05,axiom, % 58.63/58.72 ! [X18,X19] : % 58.63/58.72 ( root(X19,X18) % 58.63/58.72 => ? [X20] : % 58.63/58.72 ( subactivity(X20,X18) % 58.63/58.72 & atocc(X19,X20) ) ) ). % 58.63/58.72 % 58.63/58.72 fof(sos_06,axiom, % 58.63/58.72 ! [X21,X22,X23] : % 58.63/58.72 ( min_precedes(X22,X23,X21) % 58.63/58.72 => ? [X24] : % 58.63/58.72 ( occurrence_of(X24,X21) % 58.63/58.72 & subactivity_occurrence(X22,X24) % 58.63/58.72 & subactivity_occurrence(X23,X24) ) ) ). % 58.63/58.72 % 58.63/58.72 fof(sos_07,axiom, % 58.63/58.72 ! [X25,X26] : % 58.63/58.72 ( ( leaf(X25,X26) % 58.63/58.72 & ~ atomic(X26) ) % 58.63/58.72 => ? [X27] : % 58.63/58.72 ( occurrence_of(X27,X26) % 58.63/58.72 & leaf_occ(X25,X27) ) ) ). % 58.63/58.72 % 58.63/58.72 fof(sos_08,axiom, % 58.63/58.72 ! [X28,X29,X30] : % 58.63/58.72 ( ( occurrence_of(X28,X29) % 58.63/58.72 & occurrence_of(X28,X30) ) % 58.63/58.72 => X29 = X30 ) ). % 58.63/58.72 % 58.63/58.72 fof(sos_09,axiom, % 58.63/58.72 ! [X31,X32,X33] : % 58.63/58.72 ( ( occurrence_of(X31,X33) % 58.63/58.72 & leaf_occ(X32,X31) ) % 58.63/58.72 => ~ ? [X34] : min_precedes(X32,X34,X33) ) ). % 58.63/58.72 % 58.63/58.72 fof(sos_10,axiom, % 58.63/58.72 ! [X35,X36,X37] : % 58.63/58.72 ( ( occurrence_of(X35,X37) % 58.63/58.72 & root_occ(X36,X35) ) % 58.63/58.72 => ~ ? [X38] : min_precedes(X38,X36,X37) ) ). % 58.63/58.72 % 58.63/58.72 fof(sos_11,axiom, % 58.63/58.72 ! [X39,X40] : % 58.63/58.72 ( subactivity_occurrence(X39,X40) % 58.63/58.72 => ( activity_occurrence(X39) % 58.63/58.72 & activity_occurrence(X40) ) ) ). % 58.63/58.72 % 58.63/58.72 fof(sos_12,axiom, % 58.63/58.72 ! [X41] : % 58.63/58.72 ( activity_occurrence(X41) % 58.63/58.72 => ? [X42] : % 58.63/58.72 ( activity(X42) % 58.63/58.72 & occurrence_of(X41,X42) ) ) ). % 58.63/58.72 % 58.63/58.72 fof(sos_13,axiom, % 58.63/58.72 ! [X43] : % 58.63/58.72 ( legal(X43) % 58.63/58.72 => arboreal(X43) ) ). % 58.63/58.72 % 58.63/58.72 fof(sos_14,axiom, % 58.63/58.72 ! [X44,X45] : % 58.63/58.72 ( atocc(X44,X45) % 58.63/58.72 <=> ? [X46] : % 58.63/58.72 ( subactivity(X45,X46) % 58.63/58.72 & atomic(X46) % 58.63/58.72 & occurrence_of(X44,X46) ) ) ). % 58.63/58.72 % 58.63/58.72 fof(sos_15,axiom, % 58.63/58.72 ! [X47,X48] : % 58.63/58.72 ( leaf(X47,X48) % 58.63/58.72 <=> ( ( root(X47,X48) % 58.63/58.72 | ? [X49] : min_precedes(X49,X47,X48) ) % 58.63/58.72 & ~ ? [X50] : min_precedes(X47,X50,X48) ) ) ). % 58.63/58.72 % 58.63/58.72 fof(sos_16,axiom, % 58.63/58.72 ! [X51,X52] : % 58.63/58.72 ( occurrence_of(X51,X52) % 58.63/58.72 => ( arboreal(X51) % 58.63/58.72 <=> atomic(X52) ) ) ). % 58.63/58.72 % 58.63/58.72 fof(sos_17,axiom, % 58.63/58.72 ! [X53,X54] : % 58.63/58.72 ( root(X53,X54) % 58.63/58.72 => legal(X53) ) ). % 58.63/58.72 % 58.63/58.72 fof(sos_18,axiom, % 58.63/58.72 ! [X55,X56] : % 58.63/58.72 ( leaf_occ(X55,X56) % 58.63/58.72 <=> ? [X57] : % 58.63/58.72 ( occurrence_of(X56,X57) % 58.63/58.72 & subactivity_occurrence(X55,X56) % 58.63/58.72 & leaf(X55,X57) ) ) ). % 58.63/58.72 % 58.63/58.72 fof(sos_19,axiom, % 58.63/58.72 ! [X58,X59] : % 58.63/58.72 ( root_occ(X58,X59) % 58.63/58.72 <=> ? [X60] : % 58.63/58.72 ( occurrence_of(X59,X60) % 58.63/58.72 & subactivity_occurrence(X58,X59) % 58.63/58.72 & root(X58,X60) ) ) ). % 58.63/58.72 % 58.63/58.72 fof(sos_20,axiom, % 58.63/58.72 ! [X61,X62] : % 58.63/58.72 ( earlier(X61,X62) % 58.63/58.72 => ~ earlier(X62,X61) ) ). % 58.63/58.72 % 58.63/58.72 fof(sos_21,axiom, % 58.63/58.72 ! [X63,X64] : % 58.63/58.72 ( precedes(X63,X64) % 58.63/58.72 <=> ( earlier(X63,X64) % 58.63/58.72 & legal(X64) ) ) ). % 58.63/58.72 % 58.63/58.72 fof(sos_22,axiom, % 58.63/58.72 ! [X65,X66,X67] : % 58.63/58.72 ( min_precedes(X65,X66,X67) % 58.63/58.72 => ~ root(X66,X67) ) ). % 58.63/58.72 % 58.63/58.72 fof(sos_23,axiom, % 58.63/58.72 ! [X68,X69,X70] : % 58.63/58.72 ( min_precedes(X68,X69,X70) % 58.63/58.72 => ? [X71] : % 58.63/58.72 ( root(X71,X70) % 58.63/58.72 & min_precedes(X71,X69,X70) ) ) ). % 58.63/58.72 % 58.63/58.72 fof(sos_24,axiom, % 58.63/58.72 ! [X72,X73,X74] : % 58.63/58.72 ( min_precedes(X72,X73,X74) % 58.63/58.72 => precedes(X72,X73) ) ). % 58.63/58.72 % 58.63/58.72 fof(sos_25,axiom, % 58.63/58.72 ! [X75,X76,X77] : % 58.63/58.72 ( next_subocc(X75,X76,X77) % 58.63/58.72 => ( arboreal(X75) % 58.63/58.72 & arboreal(X76) ) ) ). % 58.63/58.72 % 58.63/58.72 fof(sos_26,axiom, % 58.63/58.72 ! [X78,X79,X80] : % 58.63/58.72 ( next_subocc(X78,X79,X80) % 58.63/58.72 <=> ( min_precedes(X78,X79,X80) % 58.63/58.72 & ~ ? [X81] : % 58.63/58.72 ( min_precedes(X78,X81,X80) % 58.63/58.72 & min_precedes(X81,X79,X80) ) ) ) ). % 58.63/58.72 % 58.63/58.72 fof(sos_27,axiom, % 58.63/58.72 ! [X82,X83,X84,X85] : % 58.63/58.72 ( ( min_precedes(X82,X83,X84) % 58.63/58.72 & occurrence_of(X85,X84) % 58.63/58.72 & subactivity_occurrence(X83,X85) ) % 58.63/58.72 => subactivity_occurrence(X82,X85) ) ). % 58.63/58.72 % 58.63/58.72 fof(sos_28,axiom, % 58.63/58.72 ! [X86,X87,X88,X89] : % 58.63/58.72 ( ( occurrence_of(X88,X89) % 58.63/58.72 & ~ atomic(X89) % 58.63/58.72 & leaf_occ(X86,X88) % 58.63/58.72 & leaf_occ(X87,X88) ) % 58.63/58.72 => X86 = X87 ) ). % 58.63/58.72 % 58.63/58.72 fof(sos_29,axiom, % 58.63/58.72 ! [X90,X91,X92,X93] : % 58.63/58.72 ( ( occurrence_of(X92,X93) % 58.63/58.72 & root_occ(X90,X92) % 58.63/58.72 & root_occ(X91,X92) ) % 58.63/58.72 => X90 = X91 ) ). % 58.63/58.72 % 58.63/58.72 fof(sos_30,axiom, % 58.63/58.72 ! [X94,X95,X96] : % 58.63/58.72 ( ( earlier(X94,X95) % 58.63/58.72 & earlier(X95,X96) ) % 58.63/58.72 => earlier(X94,X96) ) ). % 58.63/58.72 % 58.63/58.72 fof(sos_31,axiom, % 58.63/58.72 ! [X97,X98,X99,X100] : % 58.63/58.72 ( ( min_precedes(X97,X98,X100) % 58.63/58.72 & min_precedes(X97,X99,X100) % 58.63/58.72 & precedes(X98,X99) ) % 58.63/58.72 => min_precedes(X98,X99,X100) ) ). % 58.63/58.72 % 58.63/58.72 fof(sos_32,axiom, % 58.63/58.72 ! [X101] : % 58.63/58.72 ( occurrence_of(X101,tptp0) % 58.63/58.72 => ? [X102,X103,X104] : % 58.63/58.72 ( occurrence_of(X102,tptp3) % 58.63/58.72 & root_occ(X102,X101) % 58.63/58.72 & occurrence_of(X103,tptp4) % 58.63/58.72 & next_subocc(X102,X103,tptp0) % 58.63/58.72 & ( occurrence_of(X104,tptp2) % 58.63/58.72 | occurrence_of(X104,tptp1) ) % 58.63/58.72 & next_subocc(X103,X104,tptp0) % 58.63/58.72 & leaf_occ(X104,X101) ) ) ). % 58.63/58.72 % 58.63/58.72 fof(sos_33,axiom, % 58.63/58.72 activity(tptp0) ). % 58.63/58.72 % 58.63/58.72 fof(sos_34,axiom, % 58.63/58.72 ~ atomic(tptp0) ). % 58.63/58.72 % 58.63/58.72 fof(sos_35,axiom, % 58.63/58.72 atomic(tptp4) ). % 58.63/58.72 % 58.63/58.72 fof(sos_36,axiom, % 58.63/58.72 atomic(tptp2) ). % 58.63/58.72 % 58.63/58.72 fof(sos_37,axiom, % 58.63/58.72 atomic(tptp1) ). % 58.63/58.72 % 58.63/58.72 fof(sos_38,axiom, % 58.63/58.72 atomic(tptp3) ). % 58.63/58.72 % 58.63/58.72 fof(sos_39,axiom, % 58.63/58.72 tptp4 != tptp3 ). % 58.63/58.72 % 58.63/58.72 fof(sos_40,axiom, % 58.63/58.72 tptp4 != tptp2 ). % 58.63/58.72 % 58.63/58.72 fof(sos_41,axiom, % 58.63/58.72 tptp4 != tptp1 ). % 58.63/58.72 % 58.63/58.72 fof(sos_42,axiom, % 58.63/58.72 tptp3 != tptp2 ). % 58.63/58.72 % 58.63/58.72 fof(sos_43,axiom, % 58.63/58.72 tptp3 != tptp1 ). % 58.63/58.72 % 58.63/58.72 fof(sos_44,axiom, % 58.63/58.72 tptp2 != tptp1 ). % 58.63/58.72 % 58.63/58.72 fof(goals,conjecture, % 58.63/58.72 ! [X105] : % 58.63/58.72 ( occurrence_of(X105,tptp0) % 58.63/58.72 => ? [X106,X107] : % 58.63/58.72 ( occurrence_of(X106,tptp3) % 58.63/58.72 & root_occ(X106,X105) % 58.63/58.72 & ( occurrence_of(X107,tptp2) % 58.63/58.72 | occurrence_of(X107,tptp1) ) % 58.63/58.73 & min_precedes(X106,X107,tptp0) % 58.63/58.73 & leaf_occ(X107,X105) ) ) ). % 58.63/58.73 % 58.63/58.73 %------------------------------------------------------------------------------ % 58.63/58.73 %------------------------------------------- % 58.63/58.73 % Proof found % 58.63/58.73 % SZS status Theorem for theBenchmark % 58.63/58.73 % SZS output start Proof % 58.63/58.73 %ClaNum:145(EqnAxiom:63) % 58.63/58.73 %VarNum:404(SingletonVarNum:168) % 58.63/58.73 %MaxLitNum:8 % 58.63/58.73 %MaxfuncDepth:1 % 58.63/58.73 %SharedTerms:19 % 58.63/58.73 %goalClause: 69 132 133 % 58.63/58.73 %singleGoalClaCount:1 % 58.63/58.73 [64]P1(a1) % 58.63/58.73 [65]P1(a21) % 58.63/58.73 [66]P1(a2) % 58.63/58.73 [67]P1(a3) % 58.63/58.73 [68]P2(a4) % 58.63/58.73 [69]P6(a5,a4) % 58.63/58.73 [70]~E(a1,a21) % 58.63/58.73 [71]~E(a1,a2) % 58.63/58.73 [72]~E(a2,a21) % 58.63/58.73 [73]~E(a1,a3) % 58.63/58.73 [74]~E(a3,a21) % 58.63/58.73 [75]~E(a3,a2) % 58.63/58.73 [76]~P1(a4) % 58.63/58.73 [77]~P7(x771)+P3(x771) % 58.63/58.73 [78]~P4(x781)+P2(f12(x781)) % 58.63/58.73 [85]~P4(x851)+P6(x851,f12(x851)) % 58.63/58.73 [91]~P6(x911,a4)+P6(f6(x911),a1) % 58.63/58.73 [92]~P6(x921,a4)+P6(f10(x921),a21) % 58.63/58.73 [93]~P6(x931,a4)+P16(f6(x931),x931) % 58.63/58.73 [94]~P6(x941,a4)+P8(f11(x941),x941) % 58.63/58.73 [118]~P6(x1181,a4)+P11(f6(x1181),f10(x1181),a4) % 58.63/58.73 [119]~P6(x1191,a4)+P11(f10(x1191),f11(x1191),a4) % 58.63/58.73 [79]P2(x791)+~P6(x792,x791) % 58.63/58.73 [80]P4(x801)+~P6(x801,x802) % 58.63/58.73 [81]P4(x811)+~P13(x812,x811) % 58.63/58.73 [82]P4(x821)+~P13(x821,x822) % 58.63/58.73 [83]P7(x831)+~P14(x831,x832) % 58.63/58.73 [84]P7(x841)+~P15(x842,x841) % 58.63/58.73 [88]~P16(x881,x882)+P13(x881,x882) % 58.63/58.73 [89]~P8(x891,x892)+P13(x891,x892) % 58.63/58.73 [90]~P15(x901,x902)+P9(x901,x902) % 58.63/58.73 [96]~P9(x962,x961)+~P9(x961,x962) % 58.63/58.73 [98]~P5(x981,x982)+P1(f17(x981,x982)) % 58.63/58.73 [101]~P5(x1011,x1012)+P6(x1011,f17(x1011,x1012)) % 58.63/58.73 [102]~P8(x1022,x1021)+P6(x1021,f18(x1022,x1021)) % 58.63/58.73 [103]~P16(x1032,x1031)+P6(x1031,f7(x1032,x1031)) % 58.63/58.73 [104]~P16(x1041,x1042)+P14(x1041,f7(x1041,x1042)) % 58.63/58.73 [105]~P5(x1052,x1051)+P17(x1051,f17(x1052,x1051)) % 58.63/58.73 [106]~P14(x1061,x1062)+P5(x1061,f13(x1062,x1061)) % 58.63/58.73 [107]~P8(x1071,x1072)+P10(x1071,f18(x1071,x1072)) % 58.63/58.73 [108]~P14(x1082,x1081)+P17(f13(x1081,x1082),x1081) % 58.63/58.73 [120]P3(x1201)+~P11(x1202,x1201,x1203) % 58.63/58.73 [121]P3(x1211)+~P11(x1211,x1212,x1213) % 58.63/58.73 [122]P15(x1221,x1222)+~P12(x1221,x1222,x1223) % 58.63/58.73 [123]~P14(x1231,x1232)+~P12(x1233,x1231,x1232) % 58.63/58.73 [124]~P10(x1241,x1242)+~P12(x1241,x1243,x1242) % 58.63/58.73 [130]~P11(x1301,x1302,x1303)+P12(x1301,x1302,x1303) % 58.63/58.73 [136]~P12(x1363,x1361,x1362)+P13(x1361,f16(x1362,x1363,x1361)) % 58.63/58.73 [137]~P12(x1371,x1373,x1372)+P13(x1371,f16(x1372,x1371,x1373)) % 58.63/58.73 [138]~P12(x1382,x1383,x1381)+P6(f16(x1381,x1382,x1383),x1381) % 58.63/58.73 [139]~P12(x1391,x1392,x1393)+P14(f8(x1391,x1392,x1393),x1393) % 58.63/58.73 [141]~P12(x1411,x1412,x1413)+P12(f8(x1411,x1412,x1413),x1412,x1413) % 58.63/58.73 [99]~P6(x991,a4)+P6(f11(x991),a2)+P6(f11(x991),a3) % 58.63/58.73 [86]~P6(x862,x861)+P1(x861)+~P3(x862) % 58.63/58.73 [87]~P6(x871,x872)+P3(x871)+~P1(x872) % 58.63/58.73 [95]~P7(x952)+~P9(x951,x952)+P15(x951,x952) % 58.63/58.73 [110]~P10(x1102,x1101)+P1(x1101)+P8(x1102,f15(x1102,x1101)) % 58.63/58.73 [111]~P10(x1112,x1111)+P1(x1111)+P6(f15(x1112,x1111),x1111) % 58.63/58.73 [112]~P6(x1122,x1121)+P1(x1121)+P14(f14(x1121,x1122),x1121) % 58.63/58.73 [113]~P6(x1132,x1131)+P1(x1131)+P13(f14(x1131,x1132),x1132) % 58.63/58.73 [125]~P14(x1251,x1252)+P10(x1251,x1252)+P12(x1251,f19(x1251,x1252),x1252) % 58.63/58.73 [126]~P10(x1261,x1262)+P14(x1261,x1262)+P12(f20(x1261,x1262),x1261,x1262) % 58.63/58.73 [97]~P6(x973,x971)+E(x971,x972)+~P6(x973,x972) % 58.63/58.73 [100]~P9(x1001,x1003)+P9(x1001,x1002)+~P9(x1003,x1002) % 58.63/58.73 [134]P10(x1341,x1342)+~P12(x1343,x1341,x1342)+P12(x1341,f19(x1341,x1342),x1342) % 58.63/58.73 [144]~P12(x1441,x1442,x1443)+P11(x1441,x1442,x1443)+P12(x1441,f9(x1441,x1442,x1443),x1443) % 58.63/58.73 [145]~P12(x1451,x1452,x1453)+P11(x1451,x1452,x1453)+P12(f9(x1451,x1452,x1453),x1452,x1453) % 58.63/58.73 [127]~P6(x1271,x1272)+~P12(x1274,x1273,x1272)+~P16(x1273,x1271) % 58.63/58.73 [128]~P6(x1281,x1282)+~P12(x1283,x1284,x1282)+~P8(x1283,x1281) % 58.63/58.73 [143]~P11(x1434,x1432,x1433)+~P12(x1431,x1432,x1433)+~P12(x1434,x1431,x1433) % 58.63/58.73 [109]~P6(x1091,x1093)+~P17(x1092,x1093)+P5(x1091,x1092)+~P1(x1093) % 58.63/58.73 [116]~P14(x1161,x1163)+~P13(x1161,x1162)+P16(x1161,x1162)+~P6(x1162,x1163) % 58.63/58.73 [117]~P13(x1171,x1172)+~P10(x1171,x1173)+P8(x1171,x1172)+~P6(x1172,x1173) % 58.63/58.73 [114]~P16(x1142,x1143)+~P16(x1141,x1143)+E(x1141,x1142)+~P6(x1143,x1144) % 58.63/58.73 [131]~P12(x1311,x1314,x1313)+P13(x1311,x1312)+~P6(x1312,x1313)+~P13(x1314,x1312) % 58.63/58.73 [142]~P15(x1421,x1422)+~P12(x1424,x1421,x1423)+P12(x1421,x1422,x1423)+~P12(x1424,x1422,x1423) % 58.63/58.73 [132]~P12(x1321,x1322,a4)+~P16(x1321,a5)+~P8(x1322,a5)+~P6(x1321,a1)+~P6(x1322,a2) % 58.63/58.73 [133]~P12(x1331,x1332,a4)+~P16(x1331,a5)+~P8(x1332,a5)+~P6(x1331,a1)+~P6(x1332,a3) % 58.63/58.73 [115]~P8(x1152,x1154)+~P8(x1151,x1154)+E(x1151,x1152)+~P6(x1154,x1153)+P1(x1153) % 58.63/58.73 [129]~P3(x1291)+~P13(x1291,x1294)+~P8(x1292,x1294)+E(x1291,x1292)+P12(x1291,x1292,x1293)+~P6(x1294,x1293) % 58.63/58.73 [140]~P13(x1402,x1404)+~P8(x1401,x1404)+~P12(x1405,x1402,x1403)+E(x1401,x1402)+P12(x1402,x1401,x1403)+~P6(x1404,x1403)+~P16(x1405,x1404) % 58.63/58.73 [135]P12(x1351,x1352,x1353)+~P3(x1352)+~P3(x1351)+~P13(x1352,x1354)+~P13(x1351,x1354)+E(x1351,x1352)+P12(x1352,x1351,x1353)+~P6(x1354,x1353) % 58.63/58.73 %EqnAxiom % 58.63/58.73 [1]E(x11,x11) % 58.63/58.73 [2]E(x22,x21)+~E(x21,x22) % 58.63/58.73 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 58.63/58.73 [4]~E(x41,x42)+E(f12(x41),f12(x42)) % 58.63/58.73 [5]~E(x51,x52)+E(f9(x51,x53,x54),f9(x52,x53,x54)) % 58.63/58.73 [6]~E(x61,x62)+E(f9(x63,x61,x64),f9(x63,x62,x64)) % 58.63/58.73 [7]~E(x71,x72)+E(f9(x73,x74,x71),f9(x73,x74,x72)) % 58.63/58.73 [8]~E(x81,x82)+E(f6(x81),f6(x82)) % 58.63/58.73 [9]~E(x91,x92)+E(f10(x91),f10(x92)) % 58.63/58.73 [10]~E(x101,x102)+E(f8(x101,x103,x104),f8(x102,x103,x104)) % 58.63/58.73 [11]~E(x111,x112)+E(f8(x113,x111,x114),f8(x113,x112,x114)) % 58.63/58.73 [12]~E(x121,x122)+E(f8(x123,x124,x121),f8(x123,x124,x122)) % 58.63/58.73 [13]~E(x131,x132)+E(f11(x131),f11(x132)) % 58.63/58.73 [14]~E(x141,x142)+E(f17(x141,x143),f17(x142,x143)) % 58.63/58.73 [15]~E(x151,x152)+E(f17(x153,x151),f17(x153,x152)) % 58.63/58.73 [16]~E(x161,x162)+E(f19(x161,x163),f19(x162,x163)) % 58.63/58.73 [17]~E(x171,x172)+E(f19(x173,x171),f19(x173,x172)) % 58.63/58.73 [18]~E(x181,x182)+E(f20(x181,x183),f20(x182,x183)) % 58.63/58.73 [19]~E(x191,x192)+E(f20(x193,x191),f20(x193,x192)) % 58.63/58.73 [20]~E(x201,x202)+E(f16(x201,x203,x204),f16(x202,x203,x204)) % 58.63/58.73 [21]~E(x211,x212)+E(f16(x213,x211,x214),f16(x213,x212,x214)) % 58.63/58.73 [22]~E(x221,x222)+E(f16(x223,x224,x221),f16(x223,x224,x222)) % 58.63/58.73 [23]~E(x231,x232)+E(f18(x231,x233),f18(x232,x233)) % 58.63/58.73 [24]~E(x241,x242)+E(f18(x243,x241),f18(x243,x242)) % 58.63/58.73 [25]~E(x251,x252)+E(f7(x251,x253),f7(x252,x253)) % 58.63/58.73 [26]~E(x261,x262)+E(f7(x263,x261),f7(x263,x262)) % 58.63/58.73 [27]~E(x271,x272)+E(f15(x271,x273),f15(x272,x273)) % 58.63/58.73 [28]~E(x281,x282)+E(f15(x283,x281),f15(x283,x282)) % 58.63/58.73 [29]~E(x291,x292)+E(f14(x291,x293),f14(x292,x293)) % 58.63/58.73 [30]~E(x301,x302)+E(f14(x303,x301),f14(x303,x302)) % 58.63/58.73 [31]~E(x311,x312)+E(f13(x311,x313),f13(x312,x313)) % 58.63/58.73 [32]~E(x321,x322)+E(f13(x323,x321),f13(x323,x322)) % 58.63/58.73 [33]~P1(x331)+P1(x332)+~E(x331,x332) % 58.63/58.73 [34]P12(x342,x343,x344)+~E(x341,x342)+~P12(x341,x343,x344) % 58.63/58.73 [35]P12(x353,x352,x354)+~E(x351,x352)+~P12(x353,x351,x354) % 58.63/58.73 [36]P12(x363,x364,x362)+~E(x361,x362)+~P12(x363,x364,x361) % 58.63/58.73 [37]P8(x372,x373)+~E(x371,x372)+~P8(x371,x373) % 58.63/58.73 [38]P8(x383,x382)+~E(x381,x382)+~P8(x383,x381) % 58.63/58.73 [39]P11(x392,x393,x394)+~E(x391,x392)+~P11(x391,x393,x394) % 58.63/58.73 [40]P11(x403,x402,x404)+~E(x401,x402)+~P11(x403,x401,x404) % 58.63/58.73 [41]P11(x413,x414,x412)+~E(x411,x412)+~P11(x413,x414,x411) % 58.63/58.73 [42]~P2(x421)+P2(x422)+~E(x421,x422) % 58.63/58.73 [43]P6(x432,x433)+~E(x431,x432)+~P6(x431,x433) % 58.63/58.73 [44]P6(x443,x442)+~E(x441,x442)+~P6(x443,x441) % 58.63/58.73 [45]P16(x452,x453)+~E(x451,x452)+~P16(x451,x453) % 58.63/58.73 [46]P16(x463,x462)+~E(x461,x462)+~P16(x463,x461) % 58.63/58.73 [47]~P3(x471)+P3(x472)+~E(x471,x472) % 58.63/58.73 [48]~P7(x481)+P7(x482)+~E(x481,x482) % 58.63/58.73 [49]P13(x492,x493)+~E(x491,x492)+~P13(x491,x493) % 58.63/58.73 [50]P13(x503,x502)+~E(x501,x502)+~P13(x503,x501) % 58.63/58.73 [51]~P4(x511)+P4(x512)+~E(x511,x512) % 58.63/58.73 [52]P10(x522,x523)+~E(x521,x522)+~P10(x521,x523) % 58.63/58.73 [53]P10(x533,x532)+~E(x531,x532)+~P10(x533,x531) % 58.63/58.73 [54]P5(x542,x543)+~E(x541,x542)+~P5(x541,x543) % 58.63/58.73 [55]P5(x553,x552)+~E(x551,x552)+~P5(x553,x551) % 58.63/58.73 [56]P15(x562,x563)+~E(x561,x562)+~P15(x561,x563) % 58.63/58.73 [57]P15(x573,x572)+~E(x571,x572)+~P15(x573,x571) % 58.63/58.73 [58]P14(x582,x583)+~E(x581,x582)+~P14(x581,x583) % 58.63/58.73 [59]P14(x593,x592)+~E(x591,x592)+~P14(x593,x591) % 58.63/58.73 [60]P9(x602,x603)+~E(x601,x602)+~P9(x601,x603) % 58.63/58.73 [61]P9(x613,x612)+~E(x611,x612)+~P9(x613,x611) % 58.63/58.73 [62]P17(x622,x623)+~E(x621,x622)+~P17(x621,x623) % 58.63/58.73 [63]P17(x633,x632)+~E(x631,x632)+~P17(x633,x631) % 58.63/58.73 % 58.63/58.73 %------------------------------------------- % 58.63/58.73 cnf(146,plain, % 58.63/58.73 (~P3(a5)), % 58.63/58.73 inference(scs_inference,[],[69,76,86])). % 58.63/58.73 cnf(148,plain, % 58.63/58.73 (~P6(a5,a1)), % 58.63/58.73 inference(scs_inference,[],[69,64,76,86,87])). % 58.63/58.73 cnf(153,plain, % 58.63/58.73 (~P14(a5,x1531)), % 58.63/58.73 inference(scs_inference,[],[69,64,76,86,87,44,77,83])). % 58.63/58.73 cnf(163,plain, % 58.63/58.73 (~P12(x1631,a5,x1632)), % 58.63/58.73 inference(scs_inference,[],[69,64,76,86,87,44,77,83,104,120,121,84,122])). % 58.63/58.73 cnf(167,plain, % 58.63/58.73 (P6(x1671,a4)+~E(a5,x1671)), % 58.63/58.73 inference(scs_inference,[],[69,64,76,86,87,44,77,83,104,120,121,84,122,126,43])). % 58.63/58.73 cnf(172,plain, % 58.63/58.73 (~P6(a5,a21)), % 58.63/58.73 inference(scs_inference,[],[146,65,87])). % 58.63/58.73 cnf(177,plain, % 58.63/58.73 (~P8(a5,x1771)), % 58.63/58.73 inference(scs_inference,[],[146,153,65,163,87,126,107])). % 58.63/58.73 cnf(257,plain, % 58.63/58.73 (~P13(x2571,x2572)+P6(x2572,f12(x2572))), % 58.63/58.73 inference(scs_inference,[],[81,85])). % 58.63/58.73 cnf(352,plain, % 58.63/58.73 (~P9(x3521,x3522)+~P15(x3522,x3521)), % 58.63/58.73 inference(scs_inference,[],[90,96])). % 58.63/58.73 cnf(725,plain, % 58.63/58.73 (~P9(x7251,x7252)+~P12(x7252,x7251,x7253)), % 58.63/58.73 inference(scs_inference,[],[352,122])). % 58.63/58.73 cnf(757,plain, % 58.63/58.73 (~E(a5,x7571)+P6(f10(x7571),a21)), % 58.63/58.73 inference(scs_inference,[],[92,167])). % 58.63/58.73 cnf(758,plain, % 58.63/58.73 (P6(f10(a5),a21)), % 58.63/58.73 inference(equality_inference,[],[757])). % 58.63/58.73 cnf(809,plain, % 58.63/58.73 (P13(f6(a5),a5)), % 58.63/58.73 inference(scs_inference,[],[69,93,88])). % 58.63/58.73 cnf(831,plain, % 58.63/58.73 (P13(f11(a5),a5)), % 58.63/58.73 inference(scs_inference,[],[69,94,89])). % 58.63/58.73 cnf(868,plain, % 58.63/58.73 (~P12(x8681,f14(a4,a5),a4)), % 58.63/58.73 inference(scs_inference,[],[76,69,123,112])). % 58.63/58.73 cnf(892,plain, % 58.63/58.73 (~P12(x8921,x8922,f18(x8921,x8923))+~P8(x8921,x8923)), % 58.63/58.73 inference(scs_inference,[],[124,107])). % 58.63/58.73 cnf(941,plain, % 58.63/58.73 (~P12(x9411,x9412,x9413)+~P15(x9412,x9411)), % 58.63/58.73 inference(scs_inference,[],[725,90])). % 58.63/58.73 cnf(957,plain, % 58.63/58.73 (~P12(x9571,x9572,x9573)+~P12(x9572,x9571,x9574)), % 58.63/58.73 inference(scs_inference,[],[941,122])). % 58.63/58.73 cnf(1057,plain, % 58.63/58.73 (P6(a5,f18(f11(a5),a5))), % 58.63/58.73 inference(scs_inference,[],[69,102,94])). % 58.63/58.73 cnf(1060,plain, % 58.63/58.73 (E(a4,f18(f11(a5),a5))), % 58.63/58.73 inference(scs_inference,[],[69,148,1057,44,43,97])). % 58.63/58.73 cnf(1167,plain, % 58.63/58.73 (~P12(x11671,f11(a5),a4)+P13(x11671,a5)), % 58.63/58.73 inference(scs_inference,[],[69,831,131])). % 58.63/58.73 cnf(2902,plain, % 58.63/58.73 (~P12(f11(a5),x29021,f18(f11(a5),a5))), % 58.63/58.73 inference(scs_inference,[],[69,892,94])). % 58.63/58.73 cnf(2903,plain, % 58.63/58.73 (~P11(f11(a5),x29031,f18(f11(a5),a5))), % 58.63/58.73 inference(scs_inference,[],[2902,130])). % 58.63/58.73 cnf(4029,plain, % 58.63/58.73 (~P6(f10(a5),a1)), % 58.63/58.73 inference(scs_inference,[],[758,70,97])). % 58.63/58.73 cnf(4147,plain, % 58.63/58.73 (~P11(f11(a5),x41471,a4)), % 58.63/58.73 inference(scs_inference,[],[1060,758,2903,868,71,2,79,35,41])). % 58.63/58.73 cnf(4264,plain, % 58.63/58.73 (P6(a5,f12(a5))), % 58.63/58.73 inference(scs_inference,[],[809,257])). % 58.63/58.73 cnf(6150,plain, % 58.63/58.73 (P8(f11(a5),a5)), % 58.63/58.73 inference(scs_inference,[],[69,94])). % 58.63/58.73 cnf(6152,plain, % 58.63/58.73 (P11(f6(a5),f10(a5),a4)), % 58.63/58.73 inference(scs_inference,[],[69,94,118])). % 58.63/58.73 cnf(6154,plain, % 58.63/58.73 (P11(f10(a5),f11(a5),a4)), % 58.63/58.73 inference(scs_inference,[],[69,94,118,119])). % 58.63/58.73 cnf(6156,plain, % 58.63/58.73 (P16(f6(a5),a5)), % 58.63/58.73 inference(scs_inference,[],[69,94,118,119,93])). % 58.63/58.73 cnf(6158,plain, % 58.63/58.73 (P6(f6(a5),a1)), % 58.63/58.73 inference(scs_inference,[],[69,94,118,119,93,91])). % 58.63/58.73 cnf(6164,plain, % 58.63/58.73 (P3(f6(a5))), % 58.63/58.73 inference(scs_inference,[],[69,758,94,118,119,93,91,80,120,121])). % 58.63/58.73 cnf(6166,plain, % 58.63/58.73 (P12(f6(a5),f10(a5),a4)), % 58.63/58.73 inference(scs_inference,[],[69,758,94,118,119,93,91,80,120,121,130])). % 58.63/58.73 cnf(6168,plain, % 58.63/58.73 (~P16(f10(a5),a5)), % 58.63/58.73 inference(scs_inference,[],[69,758,94,118,119,93,91,80,120,121,130,127])). % 58.63/58.73 cnf(6176,plain, % 58.63/58.73 (~P12(f6(a5),f6(a5),a4)), % 58.63/58.73 inference(scs_inference,[],[69,76,758,94,118,119,93,91,80,120,121,130,127,128,112,113,143])). % 58.63/58.73 cnf(6184,plain, % 58.63/58.73 (P16(f14(a4,a5),a5)), % 58.63/58.73 inference(scs_inference,[],[69,4264,172,146,177,153,76,758,94,118,119,93,91,80,120,121,130,127,128,112,113,143,47,37,44,58,116])). % 58.63/58.73 cnf(6190,plain, % 58.63/58.73 (~P9(f10(a5),f6(a5))), % 58.63/58.73 inference(scs_inference,[],[69,4264,172,146,177,153,76,758,94,118,119,93,91,80,120,121,130,127,128,112,113,143,47,37,44,58,116,123,124,725])). % 58.63/58.73 cnf(6202,plain, % 58.63/58.73 (~P9(x62021,f6(a5))+~P9(f10(a5),x62021)), % 58.63/58.73 inference(scs_inference,[],[69,4264,172,146,177,153,76,758,94,118,119,93,91,80,120,121,130,127,128,112,113,143,47,37,44,58,116,123,124,725,941,957,122,84,83,100])). % 58.63/58.73 cnf(6207,plain, % 58.63/58.73 (P9(f6(a5),f10(a5))), % 58.63/58.73 inference(scs_inference,[],[69,4029,4264,172,146,177,153,76,758,94,118,119,93,91,80,120,121,130,127,128,112,113,143,47,37,44,58,116,123,124,725,941,957,122,84,83,100,87,43,90])). % 58.63/58.73 cnf(6215,plain, % 58.63/58.73 (P3(f11(a5))), % 58.63/58.73 inference(scs_inference,[],[6154,130,120])). % 58.63/58.73 cnf(6217,plain, % 58.63/58.73 (~E(f6(a5),f11(a5))), % 58.63/58.73 inference(scs_inference,[],[6152,6154,4147,130,120,39])). % 58.63/58.73 cnf(6219,plain, % 58.63/58.73 (~P8(f10(a5),a5)), % 58.63/58.73 inference(scs_inference,[],[69,6152,6154,4147,130,120,39,128])). % 58.63/58.73 cnf(6229,plain, % 58.63/58.73 (P13(f10(a5),a5)), % 58.63/58.73 inference(scs_inference,[],[69,6168,6152,6184,6154,6166,6176,4147,130,120,39,128,143,127,35,45,142,1167])). % 58.63/58.73 cnf(6241,plain, % 58.63/58.73 (P15(f10(a5),f11(a5))), % 58.63/58.73 inference(scs_inference,[],[69,6168,6152,6184,6154,6166,6176,4147,130,120,39,128,143,127,35,45,142,1167,725,957,124,123,941,122])). % 58.63/58.73 cnf(6243,plain, % 58.63/58.73 (P7(f11(a5))), % 58.63/58.73 inference(scs_inference,[],[69,6168,6152,6184,6154,6166,6176,4147,130,120,39,128,143,127,35,45,142,1167,725,957,124,123,941,122,84])). % 58.63/58.73 cnf(6245,plain, % 58.63/58.73 (P6(f11(a5),a3)+P6(f11(a5),a2)), % 58.63/58.73 inference(scs_inference,[],[69,6168,6152,6184,6154,6166,6176,4147,130,120,39,128,143,127,35,45,142,1167,725,957,124,123,941,122,84,99])). % 58.63/58.73 cnf(6256,plain, % 58.63/58.73 (~E(f11(a5),f6(a5))), % 58.63/58.73 inference(scs_inference,[],[6241,6190,90,61])). % 58.63/58.73 cnf(6259,plain, % 58.63/58.73 (~P12(f11(a5),x62591,f12(a5))), % 58.63/58.73 inference(scs_inference,[],[6241,6150,6207,6190,4264,90,61,100,128])). % 58.63/58.73 cnf(6273,plain, % 58.63/58.73 (~P12(f6(a5),f11(a5),x62731)+~P6(f11(a5),a2)), % 58.63/58.73 inference(scs_inference,[],[69,6164,6215,6217,6241,6243,6150,6207,6156,6158,6190,4264,831,809,90,61,100,128,127,6202,352,95,132,135,725,957])). % 58.63/58.73 cnf(6280,plain, % 58.63/58.73 (~P10(f10(a5),f12(a5))), % 58.63/58.73 inference(scs_inference,[],[6219,6229,4264,117])). % 58.63/58.73 cnf(6287,plain, % 58.63/58.73 (~P12(f11(a5),x62871,f12(a5))), % 58.63/58.73 inference(rename_variables,[],[6259])). % 58.63/58.73 cnf(6289,plain, % 58.63/58.73 (~P6(f11(a5),a2)), % 58.63/58.73 inference(scs_inference,[],[6217,6259,6164,6215,4264,831,809,135,6273])). % 58.63/58.73 cnf(6291,plain, % 58.63/58.73 (~P12(f11(a5),f6(a5),x62911)), % 58.63/58.73 inference(scs_inference,[],[6217,6259,6164,6215,4264,831,809,135,6273,957])). % 58.63/58.73 cnf(6297,plain, % 58.63/58.73 (P10(f11(a5),f12(a5))), % 58.63/58.73 inference(scs_inference,[],[6217,6259,6287,6164,6215,4264,831,809,135,6273,957,124,123,134])). % 58.63/58.73 cnf(6305,plain, % 58.63/58.73 (P6(f11(a5),a3)), % 58.63/58.73 inference(scs_inference,[],[6289,6245])). % 58.63/58.73 cnf(6310,plain, % 58.63/58.73 (P12(f6(a5),f11(a5),a4)), % 58.63/58.73 inference(scs_inference,[],[69,6256,6291,6280,6297,6164,6215,831,809,52,135])). % 58.63/58.73 cnf(6318,plain, % 58.63/58.73 ($false), % 58.63/58.73 inference(scs_inference,[],[6310,6305,6158,6156,6150,133]), % 58.63/58.73 ['proof']). % 58.63/58.73 % SZS output end Proof % 58.63/58.73 % Total time :58.090000s %------------------------------------------------------------------------------