%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : PRO011+2 : 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:45 EDT 2024 % Result : Theorem 5.59s 5.68s % Output : CNFRefutation 5.59s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.08/0.13 % Problem : PRO011+2 : TPTP v8.2.0. Released v4.0.0. % 0.08/0.13 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.13/0.34 % Computer : n022.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 300 % 0.13/0.34 % DateTime : Thu Jun 20 06:29:09 EDT 2024 % 0.13/0.34 % CPUTime : % 0.45/0.58 start to proof:theBenchmark % 5.59/5.66 %------------------------------------------- % 5.59/5.66 % File :CSE---1.7 % 5.59/5.66 % Problem :theBenchmark % 5.59/5.66 % Transform :cnf % 5.59/5.66 % Format :tptp:raw % 5.59/5.66 % Command :java -jar mcs_scs.jar %d %s % 5.59/5.66 % 5.59/5.66 % Result :Theorem 5.020000s % 5.59/5.66 % Output :CNFRefutation 5.020000s % 5.59/5.66 %------------------------------------------- % 5.59/5.66 %------------------------------------------------------------------------------ % 5.59/5.66 % File : PRO011+2 : TPTP v8.2.0. Released v4.0.0. % 5.59/5.66 % Domain : Processes % 5.59/5.66 % Problem : PSL cliff problem coe-7.1.3-subocc % 5.59/5.66 % Version : Especial : Reduced > Especial. % 5.59/5.66 % English : % 5.59/5.66 % Refs : [Hal09] Halcomb (2009), Email to G. Sutcliffe % 5.59/5.66 % Source : [Hal09] % 5.59/5.66 % Names : minimal-subset-p9__coe-7.1.3-subocc-pd [Hal09] % 5.59/5.66 % 5.59/5.66 % Status : Theorem % 5.59/5.66 % Rating : 0.19 v8.2.0, 0.22 v7.5.0, 0.25 v7.4.0, 0.20 v7.3.0, 0.17 v7.2.0, 0.14 v7.1.0, 0.17 v7.0.0, 0.10 v6.4.0, 0.12 v6.3.0, 0.17 v6.2.0, 0.20 v6.0.0, 0.17 v5.5.0, 0.19 v5.4.0, 0.21 v5.3.0, 0.22 v5.2.0, 0.10 v5.1.0, 0.19 v5.0.0, 0.17 v4.0.1, 0.22 v4.0.0 % 5.59/5.66 % Syntax : Number of formulae : 46 ( 12 unt; 0 def) % 5.59/5.66 % Number of atoms : 140 ( 10 equ) % 5.59/5.66 % Maximal formula atoms : 10 ( 3 avg) % 5.59/5.66 % Number of connectives : 113 ( 19 ~; 4 |; 53 &) % 5.59/5.66 % ( 7 <=>; 30 =>; 0 <=; 0 <~>) % 5.59/5.66 % Maximal formula depth : 12 ( 5 avg) % 5.59/5.66 % Maximal term depth : 1 ( 1 avg) % 5.59/5.66 % Number of predicates : 18 ( 17 usr; 0 prp; 1-3 aty) % 5.59/5.66 % Number of functors : 5 ( 5 usr; 5 con; 0-0 aty) % 5.59/5.66 % Number of variables : 104 ( 81 !; 23 ?) % 5.59/5.66 % SPC : FOF_THM_RFO_SEQ % 5.59/5.66 % 5.59/5.66 % Comments : % 5.59/5.66 %------------------------------------------------------------------------------ % 5.59/5.66 fof(sos,axiom, % 5.59/5.66 ! [X0,X1,X2,X3] : % 5.59/5.66 ( ( min_precedes(X0,X1,X3) % 5.59/5.66 & min_precedes(X1,X2,X3) ) % 5.59/5.66 => min_precedes(X0,X2,X3) ) ). % 5.59/5.66 % 5.59/5.66 fof(sos_01,axiom, % 5.59/5.66 ! [X4,X5,X6] : % 5.59/5.66 ( ( earlier(X4,X5) % 5.59/5.66 & earlier(X5,X6) ) % 5.59/5.66 => earlier(X4,X6) ) ). % 5.59/5.66 % 5.59/5.66 fof(sos_02,axiom, % 5.59/5.66 ! [X7,X8,X9,X10] : % 5.59/5.66 ( ( occurrence_of(X9,X10) % 5.59/5.66 & root_occ(X7,X9) % 5.59/5.66 & root_occ(X8,X9) ) % 5.59/5.66 => X7 = X8 ) ). % 5.59/5.66 % 5.59/5.66 fof(sos_03,axiom, % 5.59/5.66 ! [X11,X12,X13,X14] : % 5.59/5.66 ( ( occurrence_of(X13,X14) % 5.59/5.66 & ~ atomic(X14) % 5.59/5.66 & leaf_occ(X11,X13) % 5.59/5.66 & leaf_occ(X12,X13) ) % 5.59/5.66 => X11 = X12 ) ). % 5.59/5.67 % 5.59/5.67 fof(sos_04,axiom, % 5.59/5.67 ! [X15,X16,X17] : % 5.59/5.67 ( next_subocc(X15,X16,X17) % 5.59/5.67 <=> ( min_precedes(X15,X16,X17) % 5.59/5.67 & ~ ? [X18] : % 5.59/5.67 ( min_precedes(X15,X18,X17) % 5.59/5.67 & min_precedes(X18,X16,X17) ) ) ) ). % 5.59/5.67 % 5.59/5.67 fof(sos_05,axiom, % 5.59/5.67 ! [X19,X20,X21] : % 5.59/5.67 ( next_subocc(X19,X20,X21) % 5.59/5.67 => ( arboreal(X19) % 5.59/5.67 & arboreal(X20) ) ) ). % 5.59/5.67 % 5.59/5.67 fof(sos_06,axiom, % 5.59/5.67 ! [X22,X23,X24] : % 5.59/5.67 ( min_precedes(X22,X23,X24) % 5.59/5.67 => precedes(X22,X23) ) ). % 5.59/5.67 % 5.59/5.67 fof(sos_07,axiom, % 5.59/5.67 ! [X25,X26,X27] : % 5.59/5.67 ( min_precedes(X25,X26,X27) % 5.59/5.67 => ~ root(X26,X27) ) ). % 5.59/5.67 % 5.59/5.67 fof(sos_08,axiom, % 5.59/5.67 ! [X28,X29] : % 5.59/5.67 ( precedes(X28,X29) % 5.59/5.67 <=> ( earlier(X28,X29) % 5.59/5.67 & legal(X29) ) ) ). % 5.59/5.67 % 5.59/5.67 fof(sos_09,axiom, % 5.59/5.67 ! [X30,X31] : % 5.59/5.67 ( earlier(X30,X31) % 5.59/5.67 => ~ earlier(X31,X30) ) ). % 5.59/5.67 % 5.59/5.67 fof(sos_10,axiom, % 5.59/5.67 ! [X32,X33] : % 5.59/5.67 ( root_occ(X32,X33) % 5.59/5.67 <=> ? [X34] : % 5.59/5.67 ( occurrence_of(X33,X34) % 5.59/5.67 & subactivity_occurrence(X32,X33) % 5.59/5.67 & root(X32,X34) ) ) ). % 5.59/5.67 % 5.59/5.67 fof(sos_11,axiom, % 5.59/5.67 ! [X35,X36] : % 5.59/5.67 ( leaf_occ(X35,X36) % 5.59/5.67 <=> ? [X37] : % 5.59/5.67 ( occurrence_of(X36,X37) % 5.59/5.67 & subactivity_occurrence(X35,X36) % 5.59/5.67 & leaf(X35,X37) ) ) ). % 5.59/5.67 % 5.59/5.67 fof(sos_12,axiom, % 5.59/5.67 ! [X38,X39] : % 5.59/5.67 ( root(X38,X39) % 5.59/5.67 => legal(X38) ) ). % 5.59/5.67 % 5.59/5.67 fof(sos_13,axiom, % 5.59/5.67 ! [X40,X41] : % 5.59/5.67 ( occurrence_of(X40,X41) % 5.59/5.67 => ( arboreal(X40) % 5.59/5.67 <=> atomic(X41) ) ) ). % 5.59/5.67 % 5.59/5.67 fof(sos_14,axiom, % 5.59/5.67 ! [X42,X43] : % 5.59/5.67 ( leaf(X42,X43) % 5.59/5.67 <=> ( ( root(X42,X43) % 5.59/5.67 | ? [X44] : min_precedes(X44,X42,X43) ) % 5.59/5.67 & ~ ? [X45] : min_precedes(X42,X45,X43) ) ) ). % 5.59/5.67 % 5.59/5.67 fof(sos_15,axiom, % 5.59/5.67 ! [X46,X47] : % 5.59/5.67 ( atocc(X46,X47) % 5.59/5.67 <=> ? [X48] : % 5.59/5.67 ( subactivity(X47,X48) % 5.59/5.67 & atomic(X48) % 5.59/5.67 & occurrence_of(X46,X48) ) ) ). % 5.59/5.67 % 5.59/5.67 fof(sos_16,axiom, % 5.59/5.67 ! [X49,X50] : % 5.59/5.67 ( ( atocc(X49,X50) % 5.59/5.67 & legal(X49) ) % 5.59/5.67 => root(X49,X50) ) ). % 5.59/5.67 % 5.59/5.67 fof(sos_17,axiom, % 5.59/5.67 ! [X51] : % 5.59/5.67 ( legal(X51) % 5.59/5.67 => arboreal(X51) ) ). % 5.59/5.67 % 5.59/5.67 fof(sos_18,axiom, % 5.59/5.67 ! [X52] : % 5.59/5.67 ( activity_occurrence(X52) % 5.59/5.67 => ? [X53] : % 5.59/5.67 ( activity(X53) % 5.59/5.67 & occurrence_of(X52,X53) ) ) ). % 5.59/5.67 % 5.59/5.67 fof(sos_19,axiom, % 5.59/5.67 ! [X54,X55] : % 5.59/5.67 ( subactivity_occurrence(X54,X55) % 5.59/5.67 => ( activity_occurrence(X54) % 5.59/5.67 & activity_occurrence(X55) ) ) ). % 5.59/5.67 % 5.59/5.67 fof(sos_20,axiom, % 5.59/5.67 ! [X56,X57,X58] : % 5.59/5.67 ( ( occurrence_of(X56,X58) % 5.59/5.67 & root_occ(X57,X56) ) % 5.59/5.67 => ~ ? [X59] : min_precedes(X59,X57,X58) ) ). % 5.59/5.67 % 5.59/5.67 fof(sos_21,axiom, % 5.59/5.67 ! [X60,X61,X62] : % 5.59/5.67 ( ( occurrence_of(X60,X62) % 5.59/5.67 & leaf_occ(X61,X60) ) % 5.59/5.67 => ~ ? [X63] : min_precedes(X61,X63,X62) ) ). % 5.59/5.67 % 5.59/5.67 fof(sos_22,axiom, % 5.59/5.67 ! [X64,X65,X66] : % 5.59/5.67 ( ( occurrence_of(X64,X65) % 5.59/5.67 & occurrence_of(X64,X66) ) % 5.59/5.67 => X65 = X66 ) ). % 5.59/5.67 % 5.59/5.67 fof(sos_23,axiom, % 5.59/5.67 ! [X67,X68] : % 5.59/5.67 ( ( leaf(X67,X68) % 5.59/5.67 & ~ atomic(X68) ) % 5.59/5.67 => ? [X69] : % 5.59/5.67 ( occurrence_of(X69,X68) % 5.59/5.67 & leaf_occ(X67,X69) ) ) ). % 5.59/5.67 % 5.59/5.67 fof(sos_24,axiom, % 5.59/5.67 ! [X70,X71,X72] : % 5.59/5.67 ( min_precedes(X71,X72,X70) % 5.59/5.67 => ? [X73] : % 5.59/5.67 ( occurrence_of(X73,X70) % 5.59/5.67 & subactivity_occurrence(X71,X73) % 5.59/5.67 & subactivity_occurrence(X72,X73) ) ) ). % 5.59/5.67 % 5.59/5.67 fof(sos_25,axiom, % 5.59/5.67 ! [X74,X75] : % 5.59/5.67 ( ( leaf(X74,X75) % 5.59/5.67 & ~ atomic(X75) ) % 5.59/5.67 => ? [X76] : % 5.59/5.67 ( occurrence_of(X76,X75) % 5.59/5.67 & leaf_occ(X74,X76) ) ) ). % 5.59/5.67 % 5.59/5.67 fof(sos_26,axiom, % 5.59/5.67 ! [X77,X78,X79] : % 5.59/5.67 ( min_precedes(X78,X79,X77) % 5.59/5.67 => ? [X80,X81] : % 5.59/5.67 ( subactivity(X80,X77) % 5.59/5.67 & subactivity(X81,X77) % 5.59/5.67 & atocc(X78,X80) % 5.59/5.67 & atocc(X79,X81) ) ) ). % 5.59/5.67 % 5.59/5.67 fof(sos_27,axiom, % 5.59/5.67 ! [X82,X83] : % 5.59/5.67 ( root(X83,X82) % 5.59/5.67 => ? [X84] : % 5.59/5.67 ( subactivity(X84,X82) % 5.59/5.67 & atocc(X83,X84) ) ) ). % 5.59/5.67 % 5.59/5.67 fof(sos_28,axiom, % 5.59/5.67 ! [X85,X86,X87,X88] : % 5.59/5.67 ( ( occurrence_of(X86,X85) % 5.59/5.67 & arboreal(X87) % 5.59/5.67 & arboreal(X88) % 5.59/5.67 & subactivity_occurrence(X87,X86) % 5.59/5.67 & subactivity_occurrence(X88,X86) ) % 5.59/5.67 => ( min_precedes(X87,X88,X85) % 5.59/5.67 | min_precedes(X88,X87,X85) % 5.59/5.67 | X87 = X88 ) ) ). % 5.59/5.67 % 5.59/5.67 fof(sos_29,axiom, % 5.59/5.67 ! [X89,X90] : % 5.59/5.67 ( occurrence_of(X90,X89) % 5.59/5.67 => ( activity(X89) % 5.59/5.67 & activity_occurrence(X90) ) ) ). % 5.59/5.67 % 5.59/5.67 fof(sos_30,axiom, % 5.59/5.67 ! [X91,X92] : % 5.59/5.67 ( ( occurrence_of(X92,X91) % 5.59/5.67 & ~ atomic(X91) ) % 5.59/5.67 => ? [X93] : % 5.59/5.67 ( root(X93,X91) % 5.59/5.67 & subactivity_occurrence(X93,X92) ) ) ). % 5.59/5.67 % 5.59/5.67 fof(sos_31,axiom, % 5.59/5.67 ! [X94] : % 5.59/5.67 ( activity(X94) % 5.59/5.67 => subactivity(X94,X94) ) ). % 5.59/5.67 % 5.59/5.67 fof(sos_32,axiom, % 5.59/5.67 ! [X95] : % 5.59/5.67 ( occurrence_of(X95,tptp0) % 5.59/5.67 => ? [X96,X97,X98] : % 5.59/5.67 ( occurrence_of(X96,tptp3) % 5.59/5.67 & root_occ(X96,X95) % 5.59/5.67 & occurrence_of(X97,tptp4) % 5.59/5.67 & next_subocc(X96,X97,tptp0) % 5.59/5.67 & ( occurrence_of(X98,tptp1) % 5.59/5.67 | occurrence_of(X98,tptp2) ) % 5.59/5.67 & next_subocc(X97,X98,tptp0) % 5.59/5.67 & leaf_occ(X98,X95) ) ) ). % 5.59/5.67 % 5.59/5.67 fof(sos_33,axiom, % 5.59/5.67 activity(tptp0) ). % 5.59/5.67 % 5.59/5.67 fof(sos_34,axiom, % 5.59/5.67 ~ atomic(tptp0) ). % 5.59/5.67 % 5.59/5.67 fof(sos_35,axiom, % 5.59/5.67 atomic(tptp4) ). % 5.59/5.67 % 5.59/5.67 fof(sos_36,axiom, % 5.59/5.67 atomic(tptp1) ). % 5.59/5.67 % 5.59/5.67 fof(sos_37,axiom, % 5.59/5.67 atomic(tptp2) ). % 5.59/5.67 % 5.59/5.67 fof(sos_38,axiom, % 5.59/5.67 atomic(tptp3) ). % 5.59/5.67 % 5.59/5.67 fof(sos_39,axiom, % 5.59/5.67 tptp4 != tptp3 ). % 5.59/5.67 % 5.59/5.67 fof(sos_40,axiom, % 5.59/5.67 tptp4 != tptp1 ). % 5.59/5.67 % 5.59/5.67 fof(sos_41,axiom, % 5.59/5.67 tptp4 != tptp2 ). % 5.59/5.67 % 5.59/5.67 fof(sos_42,axiom, % 5.59/5.67 tptp3 != tptp1 ). % 5.59/5.67 % 5.59/5.67 fof(sos_43,axiom, % 5.59/5.67 tptp3 != tptp2 ). % 5.59/5.67 % 5.59/5.67 fof(sos_44,axiom, % 5.59/5.67 tptp1 != tptp2 ). % 5.59/5.67 % 5.59/5.67 fof(goals,conjecture, % 5.59/5.67 ! [X99] : % 5.59/5.67 ( occurrence_of(X99,tptp0) % 5.59/5.67 => ? [X100,X101] : % 5.59/5.67 ( leaf_occ(X101,X99) % 5.59/5.67 & ( occurrence_of(X101,tptp1) % 5.59/5.67 => ~ ? [X102] : % 5.59/5.67 ( occurrence_of(X102,tptp2) % 5.59/5.67 & subactivity_occurrence(X102,X99) % 5.59/5.67 & min_precedes(X100,X102,tptp0) ) ) % 5.59/5.67 & ( occurrence_of(X101,tptp2) % 5.59/5.67 => ~ ? [X103] : % 5.59/5.67 ( occurrence_of(X103,tptp1) % 5.59/5.67 & subactivity_occurrence(X103,X99) % 5.59/5.67 & min_precedes(X100,X103,tptp0) ) ) ) ) ). % 5.59/5.67 % 5.59/5.67 %------------------------------------------------------------------------------ % 5.59/5.68 %------------------------------------------- % 5.59/5.68 % Proof found % 5.59/5.68 % SZS status Theorem for theBenchmark % 5.59/5.68 % SZS output start Proof % 5.59/5.68 %ClaNum:171(EqnAxiom:72) % 5.59/5.68 %VarNum:466(SingletonVarNum:195) % 5.59/5.68 %MaxLitNum:8 % 5.59/5.68 %MaxfuncDepth:1 % 5.59/5.68 %SharedTerms:19 % 5.59/5.68 %goalClause: 78 108 129 130 131 132 140 141 142 143 147 148 153 154 155 156 158 % 5.59/5.68 %singleGoalClaCount:1 % 5.59/5.68 [73]P1(a1) % 5.59/5.68 [74]P1(a25) % 5.59/5.68 [75]P1(a2) % 5.59/5.68 [76]P1(a24) % 5.59/5.68 [77]P2(a3) % 5.59/5.68 [78]P6(a4,a3) % 5.59/5.68 [79]~E(a1,a25) % 5.59/5.68 [80]~E(a1,a2) % 5.59/5.68 [81]~E(a2,a25) % 5.59/5.68 [82]~E(a1,a24) % 5.59/5.68 [83]~E(a24,a25) % 5.59/5.68 [84]~E(a24,a2) % 5.59/5.68 [85]~P1(a3) % 5.59/5.68 [86]~P7(x861)+P3(x861) % 5.59/5.68 [88]~P2(x881)+P13(x881,x881) % 5.59/5.68 [87]~P4(x871)+P2(f13(x871)) % 5.59/5.68 [95]~P4(x951)+P6(x951,f13(x951)) % 5.59/5.68 [101]~P6(x1011,a3)+P6(f5(x1011),a1) % 5.59/5.68 [102]~P6(x1021,a3)+P6(f11(x1021),a25) % 5.59/5.68 [103]~P6(x1031,a3)+P16(f5(x1031),x1031) % 5.59/5.68 [104]~P6(x1041,a3)+P9(f12(x1041),x1041) % 5.59/5.68 [136]~P6(x1361,a3)+P11(f5(x1361),f11(x1361),a3) % 5.59/5.68 [137]~P6(x1371,a3)+P11(f11(x1371),f12(x1371),a3) % 5.59/5.68 [89]P7(x891)+~P14(x892,x891) % 5.59/5.68 [90]P7(x901)+~P15(x901,x902) % 5.59/5.68 [91]P4(x911)+~P6(x911,x912) % 5.59/5.68 [92]P4(x921)+~P17(x922,x921) % 5.59/5.68 [93]P4(x931)+~P17(x931,x932) % 5.59/5.68 [94]P2(x941)+~P6(x942,x941) % 5.59/5.68 [98]~P14(x981,x982)+P8(x981,x982) % 5.59/5.68 [99]~P16(x991,x992)+P17(x991,x992) % 5.59/5.68 [100]~P9(x1001,x1002)+P17(x1001,x1002) % 5.59/5.68 [107]~P8(x1072,x1071)+~P8(x1071,x1072) % 5.59/5.68 [110]~P5(x1101,x1102)+P1(f14(x1101,x1102)) % 5.59/5.68 [113]~P16(x1132,x1131)+P6(x1131,f15(x1132,x1131)) % 5.59/5.68 [114]~P9(x1142,x1141)+P6(x1141,f19(x1142,x1141)) % 5.59/5.68 [115]~P5(x1151,x1152)+P6(x1151,f14(x1151,x1152)) % 5.59/5.68 [116]~P16(x1161,x1162)+P15(x1161,f15(x1161,x1162)) % 5.59/5.68 [117]~P9(x1171,x1172)+P10(x1171,f19(x1171,x1172)) % 5.59/5.68 [118]~P15(x1181,x1182)+P5(x1181,f6(x1182,x1181)) % 5.59/5.68 [119]~P5(x1192,x1191)+P13(x1191,f14(x1192,x1191)) % 5.59/5.68 [120]~P15(x1202,x1201)+P13(f6(x1201,x1202),x1201) % 5.59/5.68 [138]P3(x1381)+~P11(x1382,x1381,x1383) % 5.59/5.68 [139]P3(x1391)+~P11(x1391,x1392,x1393) % 5.59/5.68 [144]P14(x1441,x1442)+~P12(x1441,x1442,x1443) % 5.59/5.68 [145]~P15(x1451,x1452)+~P12(x1453,x1451,x1452) % 5.59/5.68 [146]~P10(x1461,x1462)+~P12(x1461,x1463,x1462) % 5.59/5.68 [157]~P11(x1571,x1572,x1573)+P12(x1571,x1572,x1573) % 5.59/5.68 [161]~P12(x1613,x1611,x1612)+P17(x1611,f23(x1612,x1613,x1611)) % 5.59/5.68 [162]~P12(x1621,x1623,x1622)+P17(x1621,f23(x1622,x1621,x1623)) % 5.59/5.68 [163]~P12(x1631,x1633,x1632)+P5(x1631,f8(x1632,x1631,x1633)) % 5.59/5.68 [164]~P12(x1643,x1641,x1642)+P5(x1641,f9(x1642,x1643,x1641)) % 5.59/5.68 [165]~P12(x1652,x1653,x1651)+P6(f23(x1651,x1652,x1653),x1651) % 5.59/5.68 [166]~P12(x1662,x1663,x1661)+P13(f8(x1661,x1662,x1663),x1661) % 5.59/5.68 [167]~P12(x1672,x1673,x1671)+P13(f9(x1671,x1672,x1673),x1671) % 5.59/5.68 [108]P6(x1081,a24)+~P9(x1081,a4)+P6(x1081,a2) % 5.59/5.68 [111]~P6(x1111,a3)+P6(f12(x1111),a2)+P6(f12(x1111),a24) % 5.59/5.68 [96]~P6(x962,x961)+P1(x961)+~P3(x962) % 5.59/5.68 [97]~P6(x971,x972)+P3(x971)+~P1(x972) % 5.59/5.68 [105]~P7(x1052)+~P8(x1051,x1052)+P14(x1051,x1052) % 5.59/5.68 [106]~P7(x1061)+~P5(x1061,x1062)+P15(x1061,x1062) % 5.59/5.68 [122]~P10(x1222,x1221)+P1(x1221)+P9(x1222,f22(x1222,x1221)) % 5.59/5.68 [123]~P10(x1232,x1231)+P1(x1231)+P9(x1232,f7(x1232,x1231)) % 5.59/5.68 [124]~P10(x1242,x1241)+P1(x1241)+P6(f22(x1242,x1241),x1241) % 5.59/5.68 [125]~P10(x1252,x1251)+P1(x1251)+P6(f7(x1252,x1251),x1251) % 5.59/5.68 [126]~P6(x1262,x1261)+P1(x1261)+P15(f10(x1261,x1262),x1261) % 5.59/5.68 [127]~P6(x1272,x1271)+P1(x1271)+P17(f10(x1271,x1272),x1272) % 5.59/5.68 [129]~P9(x1291,a4)+P6(x1291,a2)+P6(f16(x1292,x1291),a2) % 5.59/5.68 [130]~P9(x1301,a4)+P6(x1301,a2)+P17(f16(x1302,x1301),a4) % 5.59/5.68 [131]~P9(x1311,a4)+P6(x1311,a24)+P6(f17(x1312,x1311),a24) % 5.59/5.68 [132]~P9(x1321,a4)+P6(x1321,a24)+P17(f17(x1322,x1321),a4) % 5.59/5.68 [140]~P9(x1402,a4)+P6(f16(x1401,x1402),a2)+P6(f17(x1401,x1402),a24) % 5.59/5.68 [141]~P9(x1412,a4)+P17(f16(x1411,x1412),a4)+P6(f17(x1411,x1412),a24) % 5.59/5.68 [142]~P9(x1422,a4)+P17(f17(x1421,x1422),a4)+P6(f16(x1421,x1422),a2) % 5.59/5.68 [143]~P9(x1432,a4)+P17(f16(x1431,x1432),a4)+P17(f17(x1431,x1432),a4) % 5.59/5.68 [147]~P9(x1471,a4)+P6(x1471,a2)+P12(x1472,f16(x1472,x1471),a3) % 5.59/5.68 [148]~P9(x1481,a4)+P6(x1481,a24)+P12(x1482,f17(x1482,x1481),a3) % 5.59/5.68 [149]~P15(x1491,x1492)+P10(x1491,x1492)+P12(x1491,f20(x1491,x1492),x1492) % 5.59/5.68 [150]~P10(x1501,x1502)+P15(x1501,x1502)+P12(f21(x1501,x1502),x1501,x1502) % 5.59/5.68 [153]~P9(x1532,a4)+P12(x1531,f16(x1531,x1532),a3)+P6(f17(x1531,x1532),a24) % 5.59/5.68 [154]~P9(x1542,a4)+P12(x1541,f17(x1541,x1542),a3)+P6(f16(x1541,x1542),a2) % 5.59/5.68 [155]~P9(x1552,a4)+P12(x1551,f16(x1551,x1552),a3)+P17(f17(x1551,x1552),a4) % 5.59/5.68 [156]~P9(x1562,a4)+P12(x1561,f17(x1561,x1562),a3)+P17(f16(x1561,x1562),a4) % 5.59/5.68 [158]~P9(x1582,a4)+P12(x1581,f16(x1581,x1582),a3)+P12(x1581,f17(x1581,x1582),a3) % 5.59/5.68 [109]~P6(x1093,x1091)+E(x1091,x1092)+~P6(x1093,x1092) % 5.59/5.68 [112]~P8(x1121,x1123)+P8(x1121,x1122)+~P8(x1123,x1122) % 5.59/5.68 [159]P10(x1591,x1592)+~P12(x1593,x1591,x1592)+P12(x1591,f20(x1591,x1592),x1592) % 5.59/5.68 [170]~P12(x1701,x1702,x1703)+P11(x1701,x1702,x1703)+P12(x1701,f18(x1701,x1702,x1703),x1703) % 5.59/5.68 [171]~P12(x1711,x1712,x1713)+P11(x1711,x1712,x1713)+P12(f18(x1711,x1712,x1713),x1712,x1713) % 5.59/5.68 [151]~P6(x1511,x1512)+~P12(x1514,x1513,x1512)+~P16(x1513,x1511) % 5.59/5.68 [152]~P6(x1521,x1522)+~P12(x1523,x1524,x1522)+~P9(x1523,x1521) % 5.59/5.68 [168]~P12(x1681,x1684,x1683)+P12(x1681,x1682,x1683)+~P12(x1684,x1682,x1683) % 5.59/5.68 [169]~P11(x1694,x1692,x1693)+~P12(x1691,x1692,x1693)+~P12(x1694,x1691,x1693) % 5.59/5.68 [121]~P6(x1211,x1213)+~P13(x1212,x1213)+P5(x1211,x1212)+~P1(x1213) % 5.59/5.68 [134]~P15(x1341,x1343)+~P17(x1341,x1342)+P16(x1341,x1342)+~P6(x1342,x1343) % 5.59/5.68 [135]~P17(x1351,x1352)+~P10(x1351,x1353)+P9(x1351,x1352)+~P6(x1352,x1353) % 5.59/5.68 [128]~P16(x1282,x1283)+~P16(x1281,x1283)+E(x1281,x1282)+~P6(x1283,x1284) % 5.59/5.68 [133]~P9(x1332,x1334)+~P9(x1331,x1334)+E(x1331,x1332)+~P6(x1334,x1333)+P1(x1333) % 5.59/5.68 [160]P12(x1601,x1602,x1603)+~P3(x1602)+~P3(x1601)+~P17(x1602,x1604)+~P17(x1601,x1604)+E(x1601,x1602)+P12(x1602,x1601,x1603)+~P6(x1604,x1603) % 5.59/5.68 %EqnAxiom % 5.59/5.68 [1]E(x11,x11) % 5.59/5.68 [2]E(x22,x21)+~E(x21,x22) % 5.59/5.68 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 5.59/5.68 [4]~E(x41,x42)+E(f13(x41),f13(x42)) % 5.59/5.68 [5]~E(x51,x52)+E(f18(x51,x53,x54),f18(x52,x53,x54)) % 5.59/5.68 [6]~E(x61,x62)+E(f18(x63,x61,x64),f18(x63,x62,x64)) % 5.59/5.68 [7]~E(x71,x72)+E(f18(x73,x74,x71),f18(x73,x74,x72)) % 5.59/5.68 [8]~E(x81,x82)+E(f5(x81),f5(x82)) % 5.59/5.68 [9]~E(x91,x92)+E(f11(x91),f11(x92)) % 5.59/5.68 [10]~E(x101,x102)+E(f9(x101,x103,x104),f9(x102,x103,x104)) % 5.59/5.68 [11]~E(x111,x112)+E(f9(x113,x111,x114),f9(x113,x112,x114)) % 5.59/5.68 [12]~E(x121,x122)+E(f9(x123,x124,x121),f9(x123,x124,x122)) % 5.59/5.68 [13]~E(x131,x132)+E(f12(x131),f12(x132)) % 5.59/5.68 [14]~E(x141,x142)+E(f14(x141,x143),f14(x142,x143)) % 5.59/5.68 [15]~E(x151,x152)+E(f14(x153,x151),f14(x153,x152)) % 5.59/5.68 [16]~E(x161,x162)+E(f23(x161,x163,x164),f23(x162,x163,x164)) % 5.59/5.68 [17]~E(x171,x172)+E(f23(x173,x171,x174),f23(x173,x172,x174)) % 5.59/5.68 [18]~E(x181,x182)+E(f23(x183,x184,x181),f23(x183,x184,x182)) % 5.59/5.68 [19]~E(x191,x192)+E(f17(x191,x193),f17(x192,x193)) % 5.59/5.68 [20]~E(x201,x202)+E(f17(x203,x201),f17(x203,x202)) % 5.59/5.68 [21]~E(x211,x212)+E(f15(x211,x213),f15(x212,x213)) % 5.59/5.68 [22]~E(x221,x222)+E(f15(x223,x221),f15(x223,x222)) % 5.59/5.68 [23]~E(x231,x232)+E(f19(x231,x233),f19(x232,x233)) % 5.59/5.68 [24]~E(x241,x242)+E(f19(x243,x241),f19(x243,x242)) % 5.59/5.68 [25]~E(x251,x252)+E(f16(x251,x253),f16(x252,x253)) % 5.59/5.68 [26]~E(x261,x262)+E(f16(x263,x261),f16(x263,x262)) % 5.59/5.68 [27]~E(x271,x272)+E(f20(x271,x273),f20(x272,x273)) % 5.59/5.68 [28]~E(x281,x282)+E(f20(x283,x281),f20(x283,x282)) % 5.59/5.68 [29]~E(x291,x292)+E(f21(x291,x293),f21(x292,x293)) % 5.59/5.68 [30]~E(x301,x302)+E(f21(x303,x301),f21(x303,x302)) % 5.59/5.68 [31]~E(x311,x312)+E(f6(x311,x313),f6(x312,x313)) % 5.59/5.68 [32]~E(x321,x322)+E(f6(x323,x321),f6(x323,x322)) % 5.59/5.68 [33]~E(x331,x332)+E(f8(x331,x333,x334),f8(x332,x333,x334)) % 5.59/5.68 [34]~E(x341,x342)+E(f8(x343,x341,x344),f8(x343,x342,x344)) % 5.59/5.68 [35]~E(x351,x352)+E(f8(x353,x354,x351),f8(x353,x354,x352)) % 5.59/5.68 [36]~E(x361,x362)+E(f10(x361,x363),f10(x362,x363)) % 5.59/5.68 [37]~E(x371,x372)+E(f10(x373,x371),f10(x373,x372)) % 5.59/5.68 [38]~E(x381,x382)+E(f22(x381,x383),f22(x382,x383)) % 5.59/5.68 [39]~E(x391,x392)+E(f22(x393,x391),f22(x393,x392)) % 5.59/5.68 [40]~E(x401,x402)+E(f7(x401,x403),f7(x402,x403)) % 5.59/5.68 [41]~E(x411,x412)+E(f7(x413,x411),f7(x413,x412)) % 5.59/5.68 [42]~P1(x421)+P1(x422)+~E(x421,x422) % 5.59/5.68 [43]P12(x432,x433,x434)+~E(x431,x432)+~P12(x431,x433,x434) % 5.59/5.68 [44]P12(x443,x442,x444)+~E(x441,x442)+~P12(x443,x441,x444) % 5.59/5.68 [45]P12(x453,x454,x452)+~E(x451,x452)+~P12(x453,x454,x451) % 5.59/5.68 [46]P13(x462,x463)+~E(x461,x462)+~P13(x461,x463) % 5.59/5.68 [47]P13(x473,x472)+~E(x471,x472)+~P13(x473,x471) % 5.59/5.68 [48]P11(x482,x483,x484)+~E(x481,x482)+~P11(x481,x483,x484) % 5.59/5.68 [49]P11(x493,x492,x494)+~E(x491,x492)+~P11(x493,x491,x494) % 5.59/5.68 [50]P11(x503,x504,x502)+~E(x501,x502)+~P11(x503,x504,x501) % 5.59/5.68 [51]~P2(x511)+P2(x512)+~E(x511,x512) % 5.59/5.68 [52]P6(x522,x523)+~E(x521,x522)+~P6(x521,x523) % 5.59/5.68 [53]P6(x533,x532)+~E(x531,x532)+~P6(x533,x531) % 5.59/5.68 [54]P9(x542,x543)+~E(x541,x542)+~P9(x541,x543) % 5.59/5.68 [55]P9(x553,x552)+~E(x551,x552)+~P9(x553,x551) % 5.59/5.68 [56]~P3(x561)+P3(x562)+~E(x561,x562) % 5.59/5.68 [57]~P7(x571)+P7(x572)+~E(x571,x572) % 5.59/5.68 [58]P15(x582,x583)+~E(x581,x582)+~P15(x581,x583) % 5.59/5.68 [59]P15(x593,x592)+~E(x591,x592)+~P15(x593,x591) % 5.59/5.68 [60]~P4(x601)+P4(x602)+~E(x601,x602) % 5.59/5.68 [61]P17(x612,x613)+~E(x611,x612)+~P17(x611,x613) % 5.59/5.68 [62]P17(x623,x622)+~E(x621,x622)+~P17(x623,x621) % 5.59/5.68 [63]P8(x632,x633)+~E(x631,x632)+~P8(x631,x633) % 5.59/5.68 [64]P8(x643,x642)+~E(x641,x642)+~P8(x643,x641) % 5.59/5.68 [65]P5(x652,x653)+~E(x651,x652)+~P5(x651,x653) % 5.59/5.68 [66]P5(x663,x662)+~E(x661,x662)+~P5(x663,x661) % 5.59/5.68 [67]P14(x672,x673)+~E(x671,x672)+~P14(x671,x673) % 5.59/5.68 [68]P14(x683,x682)+~E(x681,x682)+~P14(x683,x681) % 5.59/5.68 [69]P10(x692,x693)+~E(x691,x692)+~P10(x691,x693) % 5.59/5.68 [70]P10(x703,x702)+~E(x701,x702)+~P10(x703,x701) % 5.59/5.68 [71]P16(x712,x713)+~E(x711,x712)+~P16(x711,x713) % 5.59/5.68 [72]P16(x723,x722)+~E(x721,x722)+~P16(x723,x721) % 5.59/5.68 % 5.59/5.68 %------------------------------------------- % 5.59/5.68 cnf(189,plain, % 5.59/5.68 (P6(x1891,a3)+~E(a4,x1891)), % 5.59/5.68 inference(scs_inference,[],[78,73,85,96,97,53,86,90,116,138,139,89,52])). % 5.59/5.68 cnf(329,plain, % 5.59/5.68 (~E(a4,x3291)+P6(f11(x3291),a25)), % 5.59/5.68 inference(scs_inference,[],[102,189])). % 5.59/5.68 cnf(330,plain, % 5.59/5.68 (P6(f11(a4),a25)), % 5.59/5.68 inference(equality_inference,[],[329])). % 5.59/5.68 cnf(671,plain, % 5.59/5.68 (~P6(f11(a4),a2)), % 5.59/5.68 inference(scs_inference,[],[81,330,109])). % 5.59/5.68 cnf(1192,plain, % 5.59/5.68 (~P12(f12(a4),x11921,a3)), % 5.59/5.68 inference(scs_inference,[],[78,152,104])). % 5.59/5.68 cnf(1196,plain, % 5.59/5.68 (~P12(f12(a4),x11961,a3)), % 5.59/5.68 inference(rename_variables,[],[1192])). % 5.59/5.68 cnf(1198,plain, % 5.59/5.68 (~P9(x11981,a4)+P12(f12(a4),f16(f12(a4),x11981),a3)), % 5.59/5.68 inference(scs_inference,[],[1192,1196,671,157,147,158])). % 5.59/5.68 cnf(1209,plain, % 5.59/5.68 ($false), % 5.59/5.68 inference(scs_inference,[],[78,1192,1198,104]), % 5.59/5.68 ['proof']). % 5.59/5.68 % SZS output end Proof % 5.59/5.68 % Total time :5.020000s %------------------------------------------------------------------------------