%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : PRO009+3 : TPTP v8.2.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % Computer : n018.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 58.70s 58.75s % Output : CNFRefutation 58.70s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.14 % Problem : PRO009+3 : TPTP v8.2.0. Released v4.0.0. % 0.07/0.14 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.13/0.35 % Computer : n018.cluster.edu % 0.13/0.35 % Model : x86_64 x86_64 % 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.35 % Memory : 8042.1875MB % 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.35 % CPULimit : 300 % 0.13/0.35 % WCLimit : 300 % 0.13/0.35 % DateTime : Thu Jun 20 06:25:23 EDT 2024 % 0.13/0.35 % CPUTime : % 0.21/0.60 start to proof:theBenchmark % 58.66/58.73 %------------------------------------------- % 58.66/58.73 % File :CSE---1.7 % 58.66/58.73 % Problem :theBenchmark % 58.66/58.73 % Transform :cnf % 58.66/58.73 % Format :tptp:raw % 58.66/58.73 % Command :java -jar mcs_scs.jar %d %s % 58.66/58.73 % 58.66/58.73 % Result :Theorem 58.070000s % 58.70/58.73 % Output :CNFRefutation 58.070000s % 58.70/58.73 %------------------------------------------- % 58.70/58.74 %------------------------------------------------------------------------------ % 58.70/58.74 % File : PRO009+3 : TPTP v8.2.0. Released v4.0.0. % 58.70/58.74 % Domain : Processes % 58.70/58.74 % Problem : PSL cliff problem coe-7.1.2 % 58.70/58.74 % Version : Especial : Augmented > Especial. % 58.70/58.74 % English : % 58.70/58.74 % Refs : [Hal09] Halcomb (2009), Email to G. Sutcliffe % 58.70/58.74 % Source : [Hal09] % 58.70/58.74 % Names : psl-1016-subset-618-lemmas__coe-7.1.2-pd [Hal09] % 58.70/58.74 % 58.70/58.74 % Status : Theorem % 58.70/58.74 % Rating : 0.25 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.15 v6.3.0, 0.25 v6.2.0, 0.28 v6.1.0, 0.30 v5.5.0, 0.33 v5.4.0, 0.39 v5.3.0, 0.37 v5.2.0, 0.15 v5.1.0, 0.24 v5.0.0, 0.25 v4.1.0, 0.30 v4.0.0 % 58.70/58.74 % Syntax : Number of formulae : 63 ( 12 unt; 0 def) % 58.70/58.74 % Number of atoms : 215 ( 18 equ) % 58.70/58.74 % Maximal formula atoms : 9 ( 3 avg) % 58.70/58.74 % Number of connectives : 178 ( 26 ~; 7 |; 93 &) % 58.70/58.74 % ( 7 <=>; 45 =>; 0 <=; 0 <~>) % 58.70/58.74 % Maximal formula depth : 13 ( 6 avg) % 58.70/58.74 % Maximal term depth : 1 ( 1 avg) % 58.70/58.74 % Number of predicates : 18 ( 17 usr; 0 prp; 1-3 aty) % 58.70/58.74 % Number of functors : 5 ( 5 usr; 5 con; 0-0 aty) % 58.70/58.74 % Number of variables : 168 ( 145 !; 23 ?) % 58.70/58.74 % SPC : FOF_THM_RFO_SEQ % 58.70/58.74 % 58.70/58.74 % Comments : % 58.70/58.74 %------------------------------------------------------------------------------ % 58.70/58.74 fof(sos,axiom, % 58.70/58.74 ! [X0,X1] : % 58.70/58.74 ( occurrence_of(X1,X0) % 58.70/58.74 => ( activity(X0) % 58.70/58.74 & activity_occurrence(X1) ) ) ). % 58.70/58.74 % 58.70/58.74 fof(sos_01,axiom, % 58.70/58.74 ! [X2] : % 58.70/58.74 ( activity_occurrence(X2) % 58.70/58.74 => ? [X3] : % 58.70/58.74 ( activity(X3) % 58.70/58.74 & occurrence_of(X2,X3) ) ) ). % 58.70/58.74 % 58.70/58.74 fof(sos_02,axiom, % 58.70/58.74 ! [X4,X5,X6] : % 58.70/58.74 ( ( occurrence_of(X4,X5) % 58.70/58.74 & occurrence_of(X4,X6) ) % 58.70/58.74 => X5 = X6 ) ). % 58.70/58.74 % 58.70/58.74 fof(sos_03,axiom, % 58.70/58.74 ! [X7] : % 58.70/58.74 ( activity(X7) % 58.70/58.74 => subactivity(X7,X7) ) ). % 58.70/58.74 % 58.70/58.74 fof(sos_04,axiom, % 58.70/58.74 ! [X8,X9] : % 58.70/58.74 ( earlier(X8,X9) % 58.70/58.74 => ~ earlier(X9,X8) ) ). % 58.70/58.74 % 58.70/58.74 fof(sos_05,axiom, % 58.70/58.74 ! [X10,X11,X12] : % 58.70/58.74 ( ( earlier(X10,X11) % 58.70/58.74 & earlier(X11,X12) ) % 58.70/58.74 => earlier(X10,X12) ) ). % 58.70/58.74 % 58.70/58.74 fof(sos_06,axiom, % 58.70/58.74 ! [X13,X14,X15] : % 58.70/58.74 ( ( earlier(X13,X14) % 58.70/58.74 & earlier(X15,X14) ) % 58.70/58.74 => ( earlier(X15,X13) % 58.70/58.74 | earlier(X13,X15) % 58.70/58.74 | X13 = X15 ) ) ). % 58.70/58.74 % 58.70/58.74 fof(sos_07,axiom, % 58.70/58.74 ! [X16,X17] : % 58.70/58.74 ( occurrence_of(X16,X17) % 58.70/58.74 => ( arboreal(X16) % 58.70/58.74 <=> atomic(X17) ) ) ). % 58.70/58.74 % 58.70/58.74 fof(sos_08,axiom, % 58.70/58.74 ! [X18] : % 58.70/58.74 ( legal(X18) % 58.70/58.74 => arboreal(X18) ) ). % 58.70/58.74 % 58.70/58.74 fof(sos_09,axiom, % 58.70/58.74 ! [X19,X20] : % 58.70/58.74 ( ( legal(X19) % 58.70/58.74 & earlier(X20,X19) ) % 58.70/58.74 => legal(X20) ) ). % 58.70/58.74 % 58.70/58.74 fof(sos_10,axiom, % 58.70/58.74 ! [X21,X22] : % 58.70/58.74 ( precedes(X21,X22) % 58.70/58.74 <=> ( earlier(X21,X22) % 58.70/58.74 & legal(X22) ) ) ). % 58.70/58.74 % 58.70/58.74 fof(sos_11,axiom, % 58.70/58.74 ! [X23,X24,X25] : % 58.70/58.74 ( min_precedes(X24,X25,X23) % 58.70/58.74 => ? [X26,X27] : % 58.70/58.74 ( subactivity(X26,X23) % 58.70/58.74 & subactivity(X27,X23) % 58.70/58.74 & atocc(X24,X26) % 58.70/58.74 & atocc(X25,X27) ) ) ). % 58.70/58.74 % 58.70/58.74 fof(sos_12,axiom, % 58.70/58.74 ! [X28,X29] : % 58.70/58.74 ( root(X29,X28) % 58.70/58.74 => ? [X30] : % 58.70/58.74 ( subactivity(X30,X28) % 58.70/58.74 & atocc(X29,X30) ) ) ). % 58.70/58.74 % 58.70/58.74 fof(sos_13,axiom, % 58.70/58.74 ! [X31,X32,X33] : % 58.70/58.74 ( min_precedes(X31,X32,X33) % 58.70/58.74 => ? [X34] : % 58.70/58.74 ( root(X34,X33) % 58.70/58.74 & min_precedes(X34,X32,X33) ) ) ). % 58.70/58.74 % 58.70/58.74 fof(sos_14,axiom, % 58.70/58.74 ! [X35,X36,X37] : % 58.70/58.74 ( min_precedes(X35,X36,X37) % 58.70/58.74 => ~ root(X36,X37) ) ). % 58.70/58.74 % 58.70/58.74 fof(sos_15,axiom, % 58.70/58.74 ! [X38,X39,X40] : % 58.70/58.74 ( min_precedes(X38,X39,X40) % 58.70/58.74 => precedes(X38,X39) ) ). % 58.70/58.74 % 58.70/58.74 fof(sos_16,axiom, % 58.70/58.74 ! [X41,X42] : % 58.70/58.74 ( root(X41,X42) % 58.70/58.74 => legal(X41) ) ). % 58.70/58.74 % 58.70/58.74 fof(sos_17,axiom, % 58.70/58.74 ! [X43,X44] : % 58.70/58.74 ( ( atocc(X43,X44) % 58.70/58.74 & legal(X43) ) % 58.70/58.74 => root(X43,X44) ) ). % 58.70/58.74 % 58.70/58.74 fof(sos_18,axiom, % 58.70/58.74 ! [X45,X46,X47,X48] : % 58.70/58.74 ( ( min_precedes(X45,X46,X48) % 58.70/58.74 & min_precedes(X45,X47,X48) % 58.70/58.74 & precedes(X46,X47) ) % 58.70/58.74 => min_precedes(X46,X47,X48) ) ). % 58.70/58.74 % 58.70/58.74 fof(sos_19,axiom, % 58.70/58.74 ! [X49,X50,X51] : % 58.70/58.74 ( min_precedes(X49,X50,X51) % 58.70/58.74 => ~ atomic(X51) ) ). % 58.70/58.74 % 58.70/58.74 fof(sos_20,axiom, % 58.70/58.74 ! [X52,X53,X54,X55] : % 58.70/58.74 ( ( min_precedes(X53,X52,X55) % 58.70/58.74 & min_precedes(X54,X52,X55) % 58.70/58.74 & precedes(X53,X54) ) % 58.70/58.74 => min_precedes(X53,X54,X55) ) ). % 58.70/58.74 % 58.70/58.74 fof(sos_21,axiom, % 58.70/58.74 ! [X56,X57] : % 58.70/58.74 ( leaf(X56,X57) % 58.70/58.74 <=> ( ( root(X56,X57) % 58.70/58.74 | ? [X58] : min_precedes(X58,X56,X57) ) % 58.70/58.74 & ~ ? [X59] : min_precedes(X56,X59,X57) ) ) ). % 58.70/58.74 % 58.70/58.74 fof(sos_22,axiom, % 58.70/58.74 ! [X60,X61,X62] : % 58.70/58.74 ( next_subocc(X60,X61,X62) % 58.70/58.74 <=> ( min_precedes(X60,X61,X62) % 58.70/58.74 & ~ ? [X63] : % 58.70/58.74 ( min_precedes(X60,X63,X62) % 58.70/58.74 & min_precedes(X63,X61,X62) ) ) ) ). % 58.70/58.74 % 58.70/58.74 fof(sos_23,axiom, % 58.70/58.74 ! [X64,X65] : % 58.70/58.74 ( atocc(X64,X65) % 58.70/58.74 <=> ? [X66] : % 58.70/58.74 ( subactivity(X65,X66) % 58.70/58.74 & atomic(X66) % 58.70/58.74 & occurrence_of(X64,X66) ) ) ). % 58.70/58.74 % 58.70/58.74 fof(sos_24,axiom, % 58.70/58.74 ! [X67,X68] : % 58.70/58.74 ( subactivity_occurrence(X67,X68) % 58.70/58.74 => ( activity_occurrence(X67) % 58.70/58.74 & activity_occurrence(X68) ) ) ). % 58.70/58.74 % 58.70/58.74 fof(sos_25,axiom, % 58.70/58.74 ! [X69,X70,X71] : % 58.70/58.74 ( min_precedes(X70,X71,X69) % 58.70/58.74 => ? [X72] : % 58.70/58.74 ( occurrence_of(X72,X69) % 58.70/58.74 & subactivity_occurrence(X70,X72) % 58.70/58.74 & subactivity_occurrence(X71,X72) ) ) ). % 58.70/58.74 % 58.70/58.74 fof(sos_26,axiom, % 58.70/58.74 ! [X73,X74] : % 58.70/58.74 ( ( root(X74,X73) % 58.70/58.74 & ~ atomic(X73) ) % 58.70/58.74 => ? [X75] : % 58.70/58.74 ( occurrence_of(X75,X73) % 58.70/58.74 & subactivity_occurrence(X74,X75) ) ) ). % 58.70/58.74 % 58.70/58.74 fof(sos_27,axiom, % 58.70/58.74 ! [X76,X77] : % 58.70/58.74 ( ( occurrence_of(X77,X76) % 58.70/58.74 & ~ atomic(X76) ) % 58.70/58.74 => ? [X78] : % 58.70/58.74 ( root(X78,X76) % 58.70/58.74 & subactivity_occurrence(X78,X77) ) ) ). % 58.70/58.74 % 58.70/58.74 fof(sos_28,axiom, % 58.70/58.74 ! [X79,X80,X81,X82] : % 58.70/58.74 ( ( occurrence_of(X80,X79) % 58.70/58.74 & arboreal(X81) % 58.70/58.74 & arboreal(X82) % 58.70/58.74 & subactivity_occurrence(X81,X80) % 58.70/58.74 & subactivity_occurrence(X82,X80) ) % 58.70/58.74 => ( min_precedes(X81,X82,X79) % 58.70/58.74 | min_precedes(X82,X81,X79) % 58.70/58.74 | X81 = X82 ) ) ). % 58.70/58.74 % 58.70/58.74 fof(sos_29,axiom, % 58.70/58.74 ! [X83,X84,X85,X86] : % 58.70/58.74 ( ( min_precedes(X83,X84,X85) % 58.70/58.74 & occurrence_of(X86,X85) % 58.70/58.74 & subactivity_occurrence(X84,X86) ) % 58.70/58.74 => subactivity_occurrence(X83,X86) ) ). % 58.70/58.74 % 58.70/58.74 fof(sos_30,axiom, % 58.70/58.75 ! [X87,X88,X89,X90] : % 58.70/58.75 ( ( occurrence_of(X89,X87) % 58.70/58.75 & occurrence_of(X90,X88) % 58.70/58.75 & ~ atomic(X87) % 58.70/58.75 & subactivity_occurrence(X89,X90) ) % 58.70/58.75 => subactivity(X87,X88) ) ). % 58.70/58.75 % 58.70/58.75 fof(sos_31,axiom, % 58.70/58.75 ! [X91,X92,X93] : % 58.70/58.75 ( ( subactivity_occurrence(X91,X92) % 58.70/58.75 & subactivity_occurrence(X92,X93) ) % 58.70/58.75 => subactivity_occurrence(X91,X93) ) ). % 58.70/58.75 % 58.70/58.75 fof(sos_32,axiom, % 58.70/58.75 ! [X94,X95,X96,X97] : % 58.70/58.75 ( ( occurrence_of(X96,X94) % 58.70/58.75 & occurrence_of(X97,X95) % 58.70/58.75 & subactivity(X94,X95) % 58.70/58.75 & ~ subactivity_occurrence(X96,X97) ) % 58.70/58.75 => ? [X98] : % 58.70/58.75 ( subactivity_occurrence(X98,X97) % 58.70/58.75 & ~ subactivity_occurrence(X98,X96) ) ) ). % 58.70/58.75 % 58.70/58.75 fof(sos_33,axiom, % 58.70/58.75 ! [X99,X100] : % 58.70/58.75 ( root_occ(X99,X100) % 58.70/58.75 <=> ? [X101] : % 58.70/58.75 ( occurrence_of(X100,X101) % 58.70/58.75 & subactivity_occurrence(X99,X100) % 58.70/58.75 & root(X99,X101) ) ) ). % 58.70/58.75 % 58.70/58.75 fof(sos_34,axiom, % 58.70/58.75 ! [X102,X103] : % 58.70/58.75 ( leaf_occ(X102,X103) % 58.70/58.75 <=> ? [X104] : % 58.70/58.75 ( occurrence_of(X103,X104) % 58.70/58.75 & subactivity_occurrence(X102,X103) % 58.70/58.75 & leaf(X102,X104) ) ) ). % 58.70/58.75 % 58.70/58.75 fof(sos_35,axiom, % 58.70/58.75 ! [X105,X106,X107,X108] : % 58.70/58.75 ( ( occurrence_of(X107,X108) % 58.70/58.75 & root_occ(X105,X107) % 58.70/58.75 & root_occ(X106,X107) ) % 58.70/58.75 => X105 = X106 ) ). % 58.70/58.75 % 58.70/58.75 fof(sos_36,axiom, % 58.70/58.75 ! [X109,X110,X111,X112] : % 58.70/58.75 ( ( occurrence_of(X111,X112) % 58.70/58.75 & ~ atomic(X112) % 58.70/58.75 & leaf_occ(X109,X111) % 58.70/58.75 & leaf_occ(X110,X111) ) % 58.70/58.75 => X109 = X110 ) ). % 58.70/58.75 % 58.70/58.75 fof(sos_37,axiom, % 58.70/58.75 ! [X113,X114,X115] : % 58.70/58.75 ( ( occurrence_of(X113,X115) % 58.70/58.75 & leaf_occ(X114,X113) ) % 58.70/58.75 => ~ ? [X116] : min_precedes(X114,X116,X115) ) ). % 58.70/58.75 % 58.70/58.75 fof(sos_38,axiom, % 58.70/58.75 ! [X117,X118,X119] : % 58.70/58.75 ( ( occurrence_of(X117,X119) % 58.70/58.75 & root_occ(X118,X117) ) % 58.70/58.75 => ~ ? [X120] : min_precedes(X120,X118,X119) ) ). % 58.70/58.75 % 58.70/58.75 fof(sos_39,axiom, % 58.70/58.75 ! [X121,X122,X123,X124,X125] : % 58.70/58.75 ( ( next_subocc(X121,X122,X124) % 58.70/58.75 & next_subocc(X121,X123,X124) % 58.70/58.75 & occurrence_of(X125,X124) % 58.70/58.75 & subactivity_occurrence(X123,X125) % 58.70/58.75 & subactivity_occurrence(X122,X125) ) % 58.70/58.75 => X122 = X123 ) ). % 58.70/58.75 % 58.70/58.75 fof(sos_40,axiom, % 58.70/58.75 ! [X126,X127,X128,X129] : % 58.70/58.75 ( ( next_subocc(X127,X126,X129) % 58.70/58.75 & next_subocc(X128,X126,X129) ) % 58.70/58.75 => X127 = X128 ) ). % 58.70/58.75 % 58.70/58.75 fof(sos_41,axiom, % 58.70/58.75 ! [X130,X131,X132,X133] : % 58.70/58.75 ( ( occurrence_of(X130,X133) % 58.70/58.75 & leaf_occ(X131,X130) % 58.70/58.75 & root_occ(X132,X130) % 58.70/58.75 & X131 != X132 ) % 58.70/58.75 => min_precedes(X132,X131,X133) ) ). % 58.70/58.75 % 58.70/58.75 fof(sos_42,axiom, % 58.70/58.75 ! [X134,X135,X136,X137] : % 58.70/58.75 ( ( occurrence_of(X135,X134) % 58.70/58.75 & subactivity_occurrence(X136,X135) % 58.70/58.75 & root_occ(X137,X135) % 58.70/58.75 & arboreal(X136) % 58.70/58.75 & ~ min_precedes(X137,X136,X134) ) % 58.70/58.75 => X137 = X136 ) ). % 58.70/58.75 % 58.70/58.75 fof(sos_43,axiom, % 58.70/58.75 ! [X138,X139,X140,X141] : % 58.70/58.75 ( ( occurrence_of(X139,X138) % 58.70/58.75 & subactivity_occurrence(X140,X139) % 58.70/58.75 & leaf_occ(X141,X139) % 58.70/58.75 & arboreal(X140) % 58.70/58.75 & ~ min_precedes(X140,X141,X138) ) % 58.70/58.75 => X141 = X140 ) ). % 58.70/58.75 % 58.70/58.75 fof(sos_44,axiom, % 58.70/58.75 ! [X142,X143,X144] : % 58.70/58.75 ( next_subocc(X142,X143,X144) % 58.70/58.75 => ( arboreal(X142) % 58.70/58.75 & arboreal(X143) ) ) ). % 58.70/58.75 % 58.70/58.75 fof(sos_45,axiom, % 58.70/58.75 ! [X145,X146] : % 58.70/58.75 ( ( leaf(X145,X146) % 58.70/58.75 & ~ atomic(X146) ) % 58.70/58.75 => ? [X147] : % 58.70/58.75 ( occurrence_of(X147,X146) % 58.70/58.75 & leaf_occ(X145,X147) ) ) ). % 58.70/58.75 % 58.70/58.75 fof(sos_46,axiom, % 58.70/58.75 ! [X148,X149,X150] : % 58.70/58.75 ( min_precedes(X148,X149,X150) % 58.70/58.75 => arboreal(X148) ) ). % 58.70/58.75 % 58.70/58.75 fof(sos_47,axiom, % 58.70/58.75 ! [X151,X152,X153,X154,X155] : % 58.70/58.75 ( ( occurrence_of(X152,X151) % 58.70/58.75 & root_occ(X154,X152) % 58.70/58.75 & leaf_occ(X155,X152) % 58.70/58.75 & subactivity_occurrence(X153,X152) % 58.70/58.75 & min_precedes(X153,X155,X151) % 58.70/58.75 & X153 != X154 ) % 58.70/58.75 => min_precedes(X154,X153,X151) ) ). % 58.70/58.75 % 58.70/58.75 fof(sos_48,axiom, % 58.70/58.75 ! [X156,X157,X158,X159,X160] : % 58.70/58.75 ( ( occurrence_of(X157,X156) % 58.70/58.75 & root_occ(X159,X157) % 58.70/58.75 & leaf_occ(X160,X157) % 58.70/58.75 & subactivity_occurrence(X158,X157) % 58.70/58.75 & min_precedes(X159,X158,X156) % 58.70/58.75 & X158 != X160 ) % 58.70/58.75 => min_precedes(X158,X160,X156) ) ). % 58.70/58.75 % 58.70/58.75 fof(sos_49,axiom, % 58.70/58.75 ! [X161] : % 58.70/58.75 ( occurrence_of(X161,tptp0) % 58.70/58.75 => ? [X162,X163,X164] : % 58.70/58.75 ( occurrence_of(X162,tptp3) % 58.70/58.75 & root_occ(X162,X161) % 58.70/58.75 & occurrence_of(X163,tptp4) % 58.70/58.75 & next_subocc(X162,X163,tptp0) % 58.70/58.75 & ( occurrence_of(X164,tptp2) % 58.70/58.75 | occurrence_of(X164,tptp1) ) % 58.70/58.75 & next_subocc(X163,X164,tptp0) % 58.70/58.75 & leaf_occ(X164,X161) ) ) ). % 58.70/58.75 % 58.70/58.75 fof(sos_50,axiom, % 58.70/58.75 activity(tptp0) ). % 58.70/58.75 % 58.70/58.75 fof(sos_51,axiom, % 58.70/58.75 ~ atomic(tptp0) ). % 58.70/58.75 % 58.70/58.75 fof(sos_52,axiom, % 58.70/58.75 atomic(tptp4) ). % 58.70/58.75 % 58.70/58.75 fof(sos_53,axiom, % 58.70/58.75 atomic(tptp2) ). % 58.70/58.75 % 58.70/58.75 fof(sos_54,axiom, % 58.70/58.75 atomic(tptp1) ). % 58.70/58.75 % 58.70/58.75 fof(sos_55,axiom, % 58.70/58.75 atomic(tptp3) ). % 58.70/58.75 % 58.70/58.75 fof(sos_56,axiom, % 58.70/58.75 tptp4 != tptp3 ). % 58.70/58.75 % 58.70/58.75 fof(sos_57,axiom, % 58.70/58.75 tptp4 != tptp2 ). % 58.70/58.75 % 58.70/58.75 fof(sos_58,axiom, % 58.70/58.75 tptp4 != tptp1 ). % 58.70/58.75 % 58.70/58.75 fof(sos_59,axiom, % 58.70/58.75 tptp3 != tptp2 ). % 58.70/58.75 % 58.70/58.75 fof(sos_60,axiom, % 58.70/58.75 tptp3 != tptp1 ). % 58.70/58.75 % 58.70/58.75 fof(sos_61,axiom, % 58.70/58.75 tptp2 != tptp1 ). % 58.70/58.75 % 58.70/58.75 fof(goals,conjecture, % 58.70/58.75 ! [X165] : % 58.70/58.75 ( occurrence_of(X165,tptp0) % 58.70/58.75 => ? [X166,X167] : % 58.70/58.75 ( occurrence_of(X166,tptp3) % 58.70/58.75 & root_occ(X166,X165) % 58.70/58.75 & ( occurrence_of(X167,tptp2) % 58.70/58.75 | occurrence_of(X167,tptp1) ) % 58.70/58.75 & min_precedes(X166,X167,tptp0) % 58.70/58.75 & leaf_occ(X167,X165) ) ) ). % 58.70/58.75 % 58.70/58.75 %------------------------------------------------------------------------------ % 58.70/58.75 %------------------------------------------- % 58.70/58.75 % Proof found % 58.70/58.75 % SZS status Theorem for theBenchmark % 58.70/58.75 % SZS output start Proof % 58.70/58.75 %ClaNum:179(EqnAxiom:75) % 58.70/58.75 %VarNum:587(SingletonVarNum:239) % 58.70/58.75 %MaxLitNum:8 % 58.70/58.75 %MaxfuncDepth:1 % 58.70/58.75 %SharedTerms:19 % 58.70/58.75 %goalClause: 81 156 157 % 58.70/58.75 %singleGoalClaCount:1 % 58.70/58.75 [76]P1(a1) % 58.70/58.75 [77]P2(a22) % 58.70/58.75 [78]P2(a25) % 58.70/58.75 [79]P2(a23) % 58.70/58.75 [80]P2(a24) % 58.70/58.75 [81]P6(a2,a1) % 58.70/58.75 [82]~E(a25,a22) % 58.70/58.75 [83]~E(a23,a22) % 58.70/58.75 [84]~E(a23,a25) % 58.70/58.75 [85]~E(a24,a22) % 58.70/58.75 [86]~E(a24,a25) % 58.70/58.75 [87]~E(a24,a23) % 58.70/58.75 [88]~P2(a1) % 58.70/58.75 [89]~P7(x891)+P3(x891) % 58.70/58.75 [91]~P1(x911)+P13(x911,x911) % 58.70/58.75 [90]~P4(x901)+P1(f3(x901)) % 58.70/58.75 [98]~P4(x981)+P6(x981,f3(x981)) % 58.70/58.75 [105]~P6(x1051,a1)+P6(f4(x1051),a22) % 58.70/58.75 [106]~P6(x1061,a1)+P6(f12(x1061),a25) % 58.70/58.75 [107]~P6(x1071,a1)+P16(f4(x1071),x1071) % 58.70/58.75 [108]~P6(x1081,a1)+P9(f13(x1081),x1081) % 58.70/58.75 [137]~P6(x1371,a1)+P11(f4(x1371),f12(x1371),a1) % 58.70/58.75 [138]~P6(x1381,a1)+P11(f12(x1381),f13(x1381),a1) % 58.70/58.75 [92]P1(x921)+~P6(x922,x921) % 58.70/58.75 [93]P4(x931)+~P6(x931,x932) % 58.70/58.75 [94]P4(x941)+~P17(x942,x941) % 58.70/58.75 [95]P4(x951)+~P17(x951,x952) % 58.70/58.75 [96]P7(x961)+~P14(x962,x961) % 58.70/58.75 [97]P7(x971)+~P15(x971,x972) % 58.70/58.75 [102]~P14(x1021,x1022)+P8(x1021,x1022) % 58.70/58.75 [103]~P16(x1031,x1032)+P17(x1031,x1032) % 58.70/58.75 [104]~P9(x1041,x1042)+P17(x1041,x1042) % 58.70/58.75 [111]~P8(x1112,x1111)+~P8(x1111,x1112) % 58.70/58.75 [113]~P5(x1131,x1132)+P2(f14(x1131,x1132)) % 58.70/58.75 [117]~P5(x1171,x1172)+P6(x1171,f14(x1171,x1172)) % 58.70/58.75 [118]~P16(x1182,x1181)+P6(x1181,f5(x1182,x1181)) % 58.70/58.75 [119]~P9(x1192,x1191)+P6(x1191,f10(x1192,x1191)) % 58.70/58.75 [120]~P5(x1202,x1201)+P13(x1201,f14(x1202,x1201)) % 58.70/58.75 [121]~P15(x1211,x1212)+P5(x1211,f15(x1212,x1211)) % 58.70/58.75 [122]~P16(x1221,x1222)+P15(x1221,f5(x1221,x1222)) % 58.70/58.75 [123]~P9(x1231,x1232)+P10(x1231,f10(x1231,x1232)) % 58.70/58.75 [124]~P15(x1242,x1241)+P13(f15(x1241,x1242),x1241) % 58.70/58.75 [140]P3(x1401)+~P12(x1401,x1402,x1403) % 58.70/58.75 [141]P3(x1411)+~P11(x1412,x1411,x1413) % 58.70/58.75 [142]P3(x1421)+~P11(x1421,x1422,x1423) % 58.70/58.75 [143]~P2(x1431)+~P12(x1432,x1433,x1431) % 58.70/58.75 [144]P14(x1441,x1442)+~P12(x1441,x1442,x1443) % 58.70/58.75 [145]~P15(x1451,x1452)+~P12(x1453,x1451,x1452) % 58.70/58.75 [146]~P10(x1461,x1462)+~P12(x1461,x1463,x1462) % 58.70/58.75 [154]~P11(x1541,x1542,x1543)+P12(x1541,x1542,x1543) % 58.70/58.75 [161]~P12(x1611,x1613,x1612)+P5(x1611,f16(x1612,x1611,x1613)) % 58.70/58.75 [162]~P12(x1623,x1621,x1622)+P5(x1621,f17(x1622,x1623,x1621)) % 58.70/58.75 [163]~P12(x1633,x1631,x1632)+P17(x1631,f7(x1632,x1633,x1631)) % 58.70/58.75 [164]~P12(x1641,x1643,x1642)+P17(x1641,f7(x1642,x1641,x1643)) % 58.70/58.75 [165]~P12(x1652,x1653,x1651)+P6(f7(x1651,x1652,x1653),x1651) % 58.70/58.75 [166]~P12(x1662,x1663,x1661)+P13(f16(x1661,x1662,x1663),x1661) % 58.70/58.75 [167]~P12(x1672,x1673,x1671)+P13(f17(x1671,x1672,x1673),x1671) % 58.70/58.75 [168]~P12(x1681,x1682,x1683)+P15(f20(x1681,x1682,x1683),x1683) % 58.70/58.75 [172]~P12(x1721,x1722,x1723)+P12(f20(x1721,x1722,x1723),x1722,x1723) % 58.70/58.75 [114]~P6(x1141,a1)+P6(f13(x1141),a23)+P6(f13(x1141),a24) % 58.70/58.75 [99]~P6(x991,x992)+P3(x991)+~P2(x992) % 58.70/58.75 [100]~P6(x1002,x1001)+P2(x1001)+~P3(x1002) % 58.70/58.75 [101]~P8(x1011,x1012)+P7(x1011)+~P7(x1012) % 58.70/58.75 [109]~P7(x1092)+~P8(x1091,x1092)+P14(x1091,x1092) % 58.70/58.75 [110]~P7(x1101)+~P5(x1101,x1102)+P15(x1101,x1102) % 58.70/58.75 [126]~P15(x1262,x1261)+P2(x1261)+P17(x1262,f6(x1261,x1262)) % 58.70/58.75 [127]~P10(x1272,x1271)+P2(x1271)+P9(x1272,f11(x1272,x1271)) % 58.70/58.75 [128]~P10(x1282,x1281)+P2(x1281)+P6(f11(x1282,x1281),x1281) % 58.70/58.75 [129]~P15(x1292,x1291)+P2(x1291)+P6(f6(x1291,x1292),x1291) % 58.70/58.75 [130]~P6(x1302,x1301)+P2(x1301)+P15(f8(x1301,x1302),x1301) % 58.70/58.75 [131]~P6(x1312,x1311)+P2(x1311)+P17(f8(x1311,x1312),x1312) % 58.70/58.75 [147]~P15(x1471,x1472)+P10(x1471,x1472)+P12(x1471,f18(x1471,x1472),x1472) % 58.70/58.75 [148]~P10(x1481,x1482)+P15(x1481,x1482)+P12(f19(x1481,x1482),x1481,x1482) % 58.70/58.75 [112]~P6(x1123,x1121)+E(x1121,x1122)+~P6(x1123,x1122) % 58.70/58.75 [115]~P8(x1151,x1153)+P8(x1151,x1152)+~P8(x1153,x1152) % 58.70/58.75 [116]~P17(x1161,x1163)+P17(x1161,x1162)+~P17(x1163,x1162) % 58.70/58.75 [159]P10(x1591,x1592)+~P12(x1593,x1591,x1592)+P12(x1591,f18(x1591,x1592),x1592) % 58.70/58.75 [176]~P12(x1761,x1762,x1763)+P11(x1761,x1762,x1763)+P12(x1761,f21(x1761,x1762,x1763),x1763) % 58.70/58.75 [177]~P12(x1771,x1772,x1773)+P11(x1771,x1772,x1773)+P12(f21(x1771,x1772,x1773),x1772,x1773) % 58.70/58.75 [150]~P6(x1501,x1502)+~P12(x1504,x1503,x1502)+~P16(x1503,x1501) % 58.70/58.75 [151]~P6(x1511,x1512)+~P12(x1513,x1514,x1512)+~P9(x1513,x1511) % 58.70/58.75 [158]~P11(x1581,x1583,x1584)+E(x1581,x1582)+~P11(x1582,x1583,x1584) % 58.70/58.75 [175]~P11(x1754,x1752,x1753)+~P12(x1751,x1752,x1753)+~P12(x1754,x1751,x1753) % 58.70/58.75 [125]~P6(x1251,x1253)+~P13(x1252,x1253)+P5(x1251,x1252)+~P2(x1253) % 58.70/58.75 [135]~P15(x1351,x1353)+~P17(x1351,x1352)+P16(x1351,x1352)+~P6(x1352,x1353) % 58.70/58.75 [136]~P10(x1361,x1363)+~P17(x1361,x1362)+P9(x1361,x1362)+~P6(x1362,x1363) % 58.70/58.75 [132]~P16(x1322,x1323)+~P16(x1321,x1323)+E(x1321,x1322)+~P6(x1323,x1324) % 58.70/58.75 [155]~P12(x1551,x1554,x1553)+P17(x1551,x1552)+~P6(x1552,x1553)+~P17(x1554,x1552) % 58.70/58.75 [173]~P14(x1731,x1732)+~P12(x1734,x1731,x1733)+P12(x1731,x1732,x1733)+~P12(x1734,x1732,x1733) % 58.70/58.75 [174]~P14(x1741,x1742)+~P12(x1741,x1744,x1743)+P12(x1741,x1742,x1743)+~P12(x1742,x1744,x1743) % 58.70/58.75 [156]~P12(x1561,x1562,a1)+~P16(x1561,a2)+~P9(x1562,a2)+~P6(x1561,a22)+~P6(x1562,a23) % 58.70/58.75 [157]~P12(x1571,x1572,a1)+~P16(x1571,a2)+~P9(x1572,a2)+~P6(x1571,a22)+~P6(x1572,a24) % 58.70/58.75 [134]P8(x1342,x1341)+P8(x1341,x1342)+~P8(x1341,x1343)+E(x1341,x1342)+~P8(x1342,x1343) % 58.70/58.75 [133]~P9(x1332,x1334)+~P9(x1331,x1334)+E(x1331,x1332)+~P6(x1334,x1333)+P2(x1333) % 58.70/58.75 [139]~P17(x1394,x1393)+P2(x1391)+P13(x1391,x1392)+~P6(x1393,x1392)+~P6(x1394,x1391) % 58.70/58.75 [149]~P16(x1492,x1494)+~P9(x1491,x1494)+E(x1491,x1492)+P12(x1492,x1491,x1493)+~P6(x1494,x1493) % 58.70/58.76 [178]~P6(x1782,x1784)+~P6(x1781,x1783)+~P13(x1783,x1784)+P17(x1781,x1782)+P17(f9(x1783,x1784,x1781,x1782),x1782) % 58.70/58.76 [179]~P13(x1794,x1793)+P17(x1791,x1792)+~P6(x1792,x1793)+~P6(x1791,x1794)+~P17(f9(x1794,x1793,x1791,x1792),x1791) % 58.70/58.76 [152]~P3(x1521)+~P17(x1521,x1524)+~P16(x1522,x1524)+E(x1521,x1522)+P12(x1522,x1521,x1523)+~P6(x1524,x1523) % 58.70/58.76 [153]~P3(x1531)+~P17(x1531,x1534)+~P9(x1532,x1534)+E(x1531,x1532)+P12(x1531,x1532,x1533)+~P6(x1534,x1533) % 58.70/58.76 [171]~P17(x1712,x1713)+~P17(x1711,x1713)+~P11(x1715,x1711,x1714)+E(x1711,x1712)+~P11(x1715,x1712,x1714)+~P6(x1713,x1714) % 58.70/58.76 [169]~P17(x1692,x1694)+~P9(x1691,x1694)+~P12(x1695,x1692,x1693)+E(x1691,x1692)+P12(x1692,x1691,x1693)+~P6(x1694,x1693)+~P16(x1695,x1694) % 58.70/58.76 [170]~P17(x1702,x1704)+~P16(x1701,x1704)+~P12(x1702,x1705,x1703)+E(x1701,x1702)+P12(x1701,x1702,x1703)+~P6(x1704,x1703)+~P9(x1705,x1704) % 58.70/58.76 [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) % 58.70/58.76 %EqnAxiom % 58.70/58.76 [1]E(x11,x11) % 58.70/58.76 [2]E(x22,x21)+~E(x21,x22) % 58.70/58.76 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 58.70/58.76 [4]~E(x41,x42)+E(f3(x41),f3(x42)) % 58.70/58.76 [5]~E(x51,x52)+E(f9(x51,x53,x54,x55),f9(x52,x53,x54,x55)) % 58.70/58.76 [6]~E(x61,x62)+E(f9(x63,x61,x64,x65),f9(x63,x62,x64,x65)) % 58.70/58.76 [7]~E(x71,x72)+E(f9(x73,x74,x71,x75),f9(x73,x74,x72,x75)) % 58.70/58.76 [8]~E(x81,x82)+E(f9(x83,x84,x85,x81),f9(x83,x84,x85,x82)) % 58.70/58.76 [9]~E(x91,x92)+E(f4(x91),f4(x92)) % 58.70/58.76 [10]~E(x101,x102)+E(f12(x101),f12(x102)) % 58.70/58.76 [11]~E(x111,x112)+E(f21(x111,x113,x114),f21(x112,x113,x114)) % 58.70/58.76 [12]~E(x121,x122)+E(f21(x123,x121,x124),f21(x123,x122,x124)) % 58.70/58.76 [13]~E(x131,x132)+E(f21(x133,x134,x131),f21(x133,x134,x132)) % 58.70/58.76 [14]~E(x141,x142)+E(f13(x141),f13(x142)) % 58.70/58.76 [15]~E(x151,x152)+E(f14(x151,x153),f14(x152,x153)) % 58.70/58.76 [16]~E(x161,x162)+E(f14(x163,x161),f14(x163,x162)) % 58.70/58.76 [17]~E(x171,x172)+E(f16(x171,x173,x174),f16(x172,x173,x174)) % 58.70/58.76 [18]~E(x181,x182)+E(f16(x183,x181,x184),f16(x183,x182,x184)) % 58.70/58.76 [19]~E(x191,x192)+E(f16(x193,x194,x191),f16(x193,x194,x192)) % 58.70/58.76 [20]~E(x201,x202)+E(f7(x201,x203,x204),f7(x202,x203,x204)) % 58.70/58.76 [21]~E(x211,x212)+E(f7(x213,x211,x214),f7(x213,x212,x214)) % 58.70/58.76 [22]~E(x221,x222)+E(f7(x223,x224,x221),f7(x223,x224,x222)) % 58.70/58.76 [23]~E(x231,x232)+E(f18(x231,x233),f18(x232,x233)) % 58.70/58.76 [24]~E(x241,x242)+E(f18(x243,x241),f18(x243,x242)) % 58.70/58.76 [25]~E(x251,x252)+E(f5(x251,x253),f5(x252,x253)) % 58.70/58.76 [26]~E(x261,x262)+E(f5(x263,x261),f5(x263,x262)) % 58.70/58.76 [27]~E(x271,x272)+E(f10(x271,x273),f10(x272,x273)) % 58.70/58.76 [28]~E(x281,x282)+E(f10(x283,x281),f10(x283,x282)) % 58.70/58.76 [29]~E(x291,x292)+E(f17(x291,x293,x294),f17(x292,x293,x294)) % 58.70/58.76 [30]~E(x301,x302)+E(f17(x303,x301,x304),f17(x303,x302,x304)) % 58.70/58.76 [31]~E(x311,x312)+E(f17(x313,x314,x311),f17(x313,x314,x312)) % 58.70/58.76 [32]~E(x321,x322)+E(f15(x321,x323),f15(x322,x323)) % 58.70/58.76 [33]~E(x331,x332)+E(f15(x333,x331),f15(x333,x332)) % 58.70/58.76 [34]~E(x341,x342)+E(f19(x341,x343),f19(x342,x343)) % 58.70/58.76 [35]~E(x351,x352)+E(f19(x353,x351),f19(x353,x352)) % 58.70/58.76 [36]~E(x361,x362)+E(f20(x361,x363,x364),f20(x362,x363,x364)) % 58.70/58.76 [37]~E(x371,x372)+E(f20(x373,x371,x374),f20(x373,x372,x374)) % 58.70/58.76 [38]~E(x381,x382)+E(f20(x383,x384,x381),f20(x383,x384,x382)) % 58.70/58.76 [39]~E(x391,x392)+E(f8(x391,x393),f8(x392,x393)) % 58.70/58.76 [40]~E(x401,x402)+E(f8(x403,x401),f8(x403,x402)) % 58.70/58.76 [41]~E(x411,x412)+E(f6(x411,x413),f6(x412,x413)) % 58.70/58.76 [42]~E(x421,x422)+E(f6(x423,x421),f6(x423,x422)) % 58.70/58.76 [43]~E(x431,x432)+E(f11(x431,x433),f11(x432,x433)) % 58.70/58.76 [44]~E(x441,x442)+E(f11(x443,x441),f11(x443,x442)) % 58.70/58.76 [45]~P1(x451)+P1(x452)+~E(x451,x452) % 58.70/58.76 [46]~P2(x461)+P2(x462)+~E(x461,x462) % 58.70/58.76 [47]P6(x472,x473)+~E(x471,x472)+~P6(x471,x473) % 58.70/58.76 [48]P6(x483,x482)+~E(x481,x482)+~P6(x483,x481) % 58.70/58.76 [49]P17(x492,x493)+~E(x491,x492)+~P17(x491,x493) % 58.70/58.76 [50]P17(x503,x502)+~E(x501,x502)+~P17(x503,x501) % 58.70/58.76 [51]P13(x512,x513)+~E(x511,x512)+~P13(x511,x513) % 58.70/58.76 [52]P13(x523,x522)+~E(x521,x522)+~P13(x523,x521) % 58.70/58.76 [53]P12(x532,x533,x534)+~E(x531,x532)+~P12(x531,x533,x534) % 58.70/58.76 [54]P12(x543,x542,x544)+~E(x541,x542)+~P12(x543,x541,x544) % 58.70/58.76 [55]P12(x553,x554,x552)+~E(x551,x552)+~P12(x553,x554,x551) % 58.70/58.76 [56]P14(x562,x563)+~E(x561,x562)+~P14(x561,x563) % 58.70/58.76 [57]P14(x573,x572)+~E(x571,x572)+~P14(x573,x571) % 58.70/58.76 [58]~P3(x581)+P3(x582)+~E(x581,x582) % 58.70/58.76 [59]~P7(x591)+P7(x592)+~E(x591,x592) % 58.70/58.76 [60]P10(x602,x603)+~E(x601,x602)+~P10(x601,x603) % 58.70/58.76 [61]P10(x613,x612)+~E(x611,x612)+~P10(x613,x611) % 58.70/58.76 [62]~P4(x621)+P4(x622)+~E(x621,x622) % 58.70/58.76 [63]P16(x632,x633)+~E(x631,x632)+~P16(x631,x633) % 58.70/58.76 [64]P16(x643,x642)+~E(x641,x642)+~P16(x643,x641) % 58.70/58.76 [65]P9(x652,x653)+~E(x651,x652)+~P9(x651,x653) % 58.70/58.76 [66]P9(x663,x662)+~E(x661,x662)+~P9(x663,x661) % 58.70/58.76 [67]P5(x672,x673)+~E(x671,x672)+~P5(x671,x673) % 58.70/58.76 [68]P5(x683,x682)+~E(x681,x682)+~P5(x683,x681) % 58.70/58.76 [69]P8(x692,x693)+~E(x691,x692)+~P8(x691,x693) % 58.70/58.76 [70]P8(x703,x702)+~E(x701,x702)+~P8(x703,x701) % 58.70/58.76 [71]P11(x712,x713,x714)+~E(x711,x712)+~P11(x711,x713,x714) % 58.70/58.76 [72]P11(x723,x722,x724)+~E(x721,x722)+~P11(x723,x721,x724) % 58.70/58.76 [73]P11(x733,x734,x732)+~E(x731,x732)+~P11(x733,x734,x731) % 58.70/58.76 [74]P15(x742,x743)+~E(x741,x742)+~P15(x741,x743) % 58.70/58.76 [75]P15(x753,x752)+~E(x751,x752)+~P15(x753,x751) % 58.70/58.76 % 58.70/58.76 %------------------------------------------- % 58.70/58.76 cnf(180,plain, % 58.70/58.76 (~P12(x1801,x1802,a22)), % 58.70/58.76 inference(scs_inference,[],[77,143])). % 58.70/58.76 cnf(182,plain, % 58.70/58.76 (~P3(a2)), % 58.70/58.76 inference(scs_inference,[],[81,77,88,143,100])). % 58.70/58.76 cnf(186,plain, % 58.70/58.76 (~P7(a2)), % 58.70/58.76 inference(scs_inference,[],[81,77,88,143,100,154,89])). % 58.70/58.76 cnf(188,plain, % 58.70/58.76 (~P15(a2,x1881)), % 58.70/58.76 inference(scs_inference,[],[81,77,88,143,100,154,89,97])). % 58.70/58.76 cnf(192,plain, % 58.70/58.76 (~P12(a2,x1921,x1922)), % 58.70/58.76 inference(scs_inference,[],[81,77,88,143,100,154,89,97,122,140])). % 58.70/58.76 cnf(194,plain, % 58.70/58.76 (~P11(x1941,a2,x1942)), % 58.70/58.76 inference(scs_inference,[],[81,77,88,143,100,154,89,97,122,140,141])). % 58.70/58.76 cnf(200,plain, % 58.70/58.76 (~P12(x2001,a2,x2002)), % 58.70/58.76 inference(scs_inference,[],[81,77,88,143,100,154,89,97,122,140,141,142,96,144])). % 58.70/58.76 cnf(202,plain, % 58.70/58.76 (~P6(a2,a22)), % 58.70/58.76 inference(scs_inference,[],[81,77,88,143,100,154,89,97,122,140,141,142,96,144,99])). % 58.70/58.76 cnf(209,plain, % 58.70/58.76 (P6(x2091,a1)+~E(a2,x2091)), % 58.70/58.76 inference(scs_inference,[],[81,77,88,143,100,154,89,97,122,140,141,142,96,144,99,147,148,48,47])). % 58.70/58.76 cnf(213,plain, % 58.70/58.76 (~P12(x2131,x2132,a25)), % 58.70/58.76 inference(scs_inference,[],[78,143])). % 58.70/58.76 cnf(229,plain, % 58.70/58.76 (~P14(x2291,x2292)+~P8(a2,x2292)), % 58.70/58.76 inference(scs_inference,[],[182,180,188,78,186,143,148,99,154,101,97,122,96])). % 58.70/58.76 cnf(235,plain, % 58.70/58.76 (~P12(x2351,x2352,a23)), % 58.70/58.76 inference(scs_inference,[],[79,143])). % 58.70/58.76 cnf(241,plain, % 58.70/58.76 (~P6(a2,a23)), % 58.70/58.76 inference(scs_inference,[],[182,213,79,188,143,148,99])). % 58.70/58.76 cnf(253,plain, % 58.70/58.76 (~P12(x2531,x2532,a24)), % 58.70/58.76 inference(scs_inference,[],[80,143])). % 58.70/58.76 cnf(259,plain, % 58.70/58.76 (~P6(a2,a24)), % 58.70/58.76 inference(scs_inference,[],[182,235,80,188,143,148,99])). % 58.70/58.76 cnf(282,plain, % 58.70/58.76 (~P9(a2,x2821)), % 58.70/58.76 inference(scs_inference,[],[188,200,148,123])). % 58.70/58.76 cnf(372,plain, % 58.70/58.76 (P13(a1,a1)), % 58.70/58.76 inference(scs_inference,[],[81,92,91])). % 58.70/58.76 cnf(376,plain, % 58.70/58.76 (~P17(x3761,a2)+~P12(x3762,x3761,a1)+P17(x3762,a2)), % 58.70/58.76 inference(scs_inference,[],[81,180,372,155])). % 58.70/58.76 cnf(393,plain, % 58.70/58.76 (~P17(x3931,x3932)+P6(x3932,f3(x3932))), % 58.70/58.76 inference(scs_inference,[],[94,98])). % 58.70/58.76 cnf(458,plain, % 58.70/58.76 (~P8(x4581,x4582)+~P14(x4582,x4581)), % 58.70/58.76 inference(scs_inference,[],[102,111])). % 58.70/58.76 cnf(474,plain, % 58.70/58.76 (P6(x4741,f3(x4741))+~P16(x4742,x4741)), % 58.70/58.76 inference(scs_inference,[],[103,393])). % 58.70/58.76 cnf(559,plain, % 58.70/58.76 (~P12(x5591,x5592,x5593)+~P8(a2,x5592)), % 58.70/58.76 inference(scs_inference,[],[229,144])). % 58.70/58.76 cnf(949,plain, % 58.70/58.76 (~P8(x9491,x9492)+~P12(x9492,x9491,x9493)), % 58.70/58.76 inference(scs_inference,[],[458,144])). % 58.70/58.76 cnf(997,plain, % 58.70/58.76 (~E(a2,x9971)+P6(f12(x9971),a25)), % 58.70/58.76 inference(scs_inference,[],[106,209])). % 58.70/58.76 cnf(998,plain, % 58.70/58.76 (P6(f12(a2),a25)), % 58.70/58.76 inference(equality_inference,[],[997])). % 58.70/58.76 cnf(1246,plain, % 58.70/58.76 (~P12(x12461,x12462,x12463)+~P14(x12462,x12461)), % 58.70/58.76 inference(scs_inference,[],[949,102])). % 58.70/58.76 cnf(1407,plain, % 58.70/58.76 (~P12(x14071,x14072,x14073)+~P12(x14072,x14071,x14074)), % 58.70/58.76 inference(scs_inference,[],[1246,144])). % 58.70/58.76 cnf(1503,plain, % 58.70/58.76 (P6(a2,f5(f4(a2),a2))), % 58.70/58.76 inference(scs_inference,[],[81,118,107])). % 58.70/58.76 cnf(1504,plain, % 58.70/58.76 (~E(f5(f4(a2),a2),a23)), % 58.70/58.76 inference(scs_inference,[],[241,1503,48])). % 58.70/58.76 cnf(1512,plain, % 58.70/58.76 (~E(f5(f4(a2),a2),a24)), % 58.70/58.76 inference(scs_inference,[],[259,1503,48])). % 58.70/58.76 cnf(2064,plain, % 58.70/58.76 (~P11(x20641,x20642,x20643)+~P12(x20642,x20641,x20644)), % 58.70/58.76 inference(scs_inference,[],[1407,154])). % 58.70/58.76 cnf(2208,plain, % 58.70/58.76 (~P12(f12(a2),f4(a2),x22081)), % 58.70/58.76 inference(scs_inference,[],[81,2064,137])). % 58.70/58.76 cnf(2209,plain, % 58.70/58.76 (~P11(f12(a2),f4(a2),x22091)), % 58.70/58.76 inference(scs_inference,[],[2208,154])). % 58.70/58.76 cnf(4166,plain, % 58.70/58.76 (~E(a25,a24)), % 58.70/58.76 inference(scs_inference,[],[998,86,112,48])). % 58.70/58.76 cnf(4177,plain, % 58.70/58.76 (~P6(x41771,a22)+~P6(x41771,a23)), % 58.70/58.76 inference(scs_inference,[],[83,112])). % 58.70/58.76 cnf(4180,plain, % 58.70/58.76 (~P6(x41801,a22)+~P6(x41801,a24)), % 58.70/58.76 inference(scs_inference,[],[85,112])). % 58.70/58.76 cnf(4222,plain, % 58.70/58.76 (P13(a25,a25)), % 58.70/58.76 inference(scs_inference,[],[1504,998,2,92,91])). % 58.70/58.76 cnf(4262,plain, % 58.70/58.76 (~P11(f12(a2),x42621,x42622)+~E(x42621,f4(a2))), % 58.70/58.76 inference(scs_inference,[],[1512,2209,82,282,2,158,65,72])). % 58.70/58.76 cnf(4364,plain, % 58.70/58.76 (~E(a24,x43641)+~E(a25,x43641)), % 58.70/58.76 inference(scs_inference,[],[4166,3,2])). % 58.70/58.76 cnf(4367,plain, % 58.70/58.76 (~E(x43671,a25)+~E(a23,x43671)), % 58.70/58.76 inference(scs_inference,[],[84,3])). % 58.70/58.76 cnf(4510,plain, % 58.70/58.76 (~P11(x45101,x45102,x45103)+~P11(a25,x45102,x45103)+~E(a24,x45101)), % 58.70/58.76 inference(scs_inference,[],[4364,158])). % 58.70/58.76 cnf(4527,plain, % 58.70/58.76 (~P11(x45271,x45272,x45273)+~P11(a23,x45272,x45273)+~E(x45271,a25)), % 58.70/58.76 inference(scs_inference,[],[4367,158])). % 58.70/58.76 cnf(5483,plain, % 58.70/58.76 (P16(f4(a2),a2)), % 58.70/58.76 inference(scs_inference,[],[81,107])). % 58.70/58.76 cnf(5485,plain, % 58.70/58.76 (P9(f13(a2),a2)), % 58.70/58.76 inference(scs_inference,[],[81,107,108])). % 58.70/58.76 cnf(5487,plain, % 58.70/58.76 (P11(f4(a2),f12(a2),a1)), % 58.70/58.76 inference(scs_inference,[],[81,107,108,137])). % 58.70/58.76 cnf(5489,plain, % 58.70/58.76 (P11(f12(a2),f13(a2),a1)), % 58.70/58.76 inference(scs_inference,[],[81,107,108,137,138])). % 58.70/58.76 cnf(5494,plain, % 58.70/58.76 (P12(f4(a2),f12(a2),a1)), % 58.70/58.76 inference(scs_inference,[],[81,107,108,137,138,4262,93,154])). % 58.70/58.76 cnf(5496,plain, % 58.70/58.76 (P6(a2,f3(a2))), % 58.70/58.76 inference(scs_inference,[],[81,107,108,137,138,4262,93,154,474])). % 58.70/58.76 cnf(5498,plain, % 58.70/58.76 (P6(f4(a2),a22)), % 58.70/58.76 inference(scs_inference,[],[81,107,108,137,138,4262,93,154,474,105])). % 58.70/58.76 cnf(5502,plain, % 58.70/58.76 (P17(f13(a2),a2)), % 58.70/58.76 inference(scs_inference,[],[81,107,108,137,138,4262,93,154,474,105,140,104])). % 58.70/58.76 cnf(5504,plain, % 58.70/58.76 (P3(f12(a2))), % 58.70/58.76 inference(scs_inference,[],[81,107,108,137,138,4262,93,154,474,105,140,104,141])). % 58.70/58.76 cnf(5506,plain, % 58.70/58.76 (~P16(f12(a2),a2)), % 58.70/58.76 inference(scs_inference,[],[81,107,108,137,138,4262,93,154,474,105,140,104,141,150])). % 58.70/58.76 cnf(5510,plain, % 58.70/58.76 (P17(f8(a1,a2),a2)), % 58.70/58.76 inference(scs_inference,[],[81,88,107,108,137,138,4262,93,154,474,105,140,104,141,150,151,131])). % 58.70/58.76 cnf(5525,plain, % 58.70/58.76 (P16(f8(a1,a2),a2)), % 58.70/58.76 inference(scs_inference,[],[81,4222,194,78,202,88,188,998,192,107,108,137,138,4262,93,154,474,105,140,104,141,150,151,131,53,175,130,48,74,72,125,135])). % 58.70/58.76 cnf(5527,plain, % 58.70/58.76 (~P14(f4(a2),f4(a2))), % 58.70/58.76 inference(scs_inference,[],[81,4222,194,78,202,88,188,998,192,107,108,137,138,4262,93,154,474,105,140,104,141,150,151,131,53,175,130,48,74,72,125,135,174])). % 58.70/58.76 cnf(5529,plain, % 58.70/58.76 (P12(f4(a2),f13(a2),a1)), % 58.70/58.76 inference(scs_inference,[],[81,4222,194,78,202,88,188,998,192,107,108,137,138,4262,93,154,474,105,140,104,141,150,151,131,53,175,130,48,74,72,125,135,174,149])). % 58.70/58.76 cnf(5537,plain, % 58.70/58.76 (~P8(f12(a2),f4(a2))), % 58.70/58.76 inference(scs_inference,[],[81,4222,194,78,202,88,188,998,192,107,108,137,138,4262,93,154,474,105,140,104,141,150,151,131,53,175,130,48,74,72,125,135,174,149,103,145,146,949])). % 58.70/58.76 cnf(5551,plain, % 58.70/58.76 (P14(f4(a2),f12(a2))), % 58.70/58.76 inference(scs_inference,[],[81,4222,194,78,202,88,188,998,192,107,108,137,138,4262,93,154,474,105,140,104,141,150,151,131,53,175,130,48,74,72,125,135,174,149,103,145,146,949,1246,559,1407,2064,4177,4180,144])). % 58.70/58.76 cnf(5561,plain, % 58.70/58.76 (~P2(f3(a2))), % 58.70/58.76 inference(scs_inference,[],[81,4222,194,78,202,182,88,188,998,192,107,108,137,138,4262,93,154,474,105,140,104,141,150,151,131,53,175,130,48,74,72,125,135,174,149,103,145,146,949,1246,559,1407,2064,4177,4180,144,95,96,102,4510,99])). % 58.70/58.76 cnf(5572,plain, % 58.70/58.76 (P12(f12(a2),f13(a2),a1)), % 58.70/58.76 inference(scs_inference,[],[5489,5498,93,154])). % 58.70/58.76 cnf(5574,plain, % 58.70/58.76 (~P12(f13(a2),f12(a2),x55741)), % 58.70/58.76 inference(scs_inference,[],[5489,5498,93,154,1407])). % 58.70/58.76 cnf(5590,plain, % 58.70/58.76 (P3(f13(a2))), % 58.70/58.76 inference(scs_inference,[],[5529,5510,5489,5498,93,154,1407,2064,1246,144,145,146,949,95,141])). % 58.70/58.76 cnf(5598,plain, % 58.70/58.76 (~P9(f12(a2),a2)), % 58.70/58.76 inference(scs_inference,[],[81,5487,5529,5551,5527,5510,5489,5498,93,154,1407,2064,1246,144,145,146,949,95,141,96,102,57,71,151])). % 58.70/58.76 cnf(5611,plain, % 58.70/58.76 (P17(f12(a2),a2)), % 58.70/58.76 inference(scs_inference,[],[81,5506,5487,5483,5529,5537,5551,5527,5561,5510,5489,5494,5498,5502,79,93,154,1407,2064,1246,144,145,146,949,95,141,96,102,57,71,151,175,150,46,110,63,173,69,376])). % 58.70/58.76 cnf(5633,plain, % 58.70/58.76 (P12(f12(a2),f13(a2),f3(a2))), % 58.70/58.76 inference(scs_inference,[],[5598,5574,5504,5590,5572,5611,5496,5485,5525,5502,998,1246,144,93,949,102,151,150,65,160])). % 58.70/58.76 cnf(5645,plain, % 58.70/58.76 (~P6(f13(a2),a23)), % 58.70/58.76 inference(scs_inference,[],[5598,5574,5504,5590,5572,5611,5496,5485,5525,5561,5498,5502,5483,5487,78,5529,998,1246,144,93,949,102,151,150,65,160,145,146,4527,159,46,156])). % 58.70/58.76 cnf(5647,plain, % 58.70/58.76 (~P6(f13(a2),a24)), % 58.70/58.76 inference(scs_inference,[],[5598,5574,5504,5590,5572,5611,5496,5485,5525,5561,5498,5502,5483,5487,78,5529,998,1246,144,93,949,102,151,150,65,160,145,146,4527,159,46,156,157])). % 58.70/58.76 cnf(5654,plain, % 58.70/58.76 ($false), % 58.70/58.76 inference(scs_inference,[],[81,5647,5645,5633,253,55,114]), % 58.70/58.76 ['proof']). % 58.70/58.76 % SZS output end Proof % 58.70/58.76 % Total time :58.070000s %------------------------------------------------------------------------------