%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : PRO011+3 : 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 : n020.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 0.62s 0.74s % Output : CNFRefutation 0.62s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.04/0.13 % Problem : PRO011+3 : TPTP v8.2.0. Released v4.0.0. % 0.04/0.13 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.14/0.35 % Computer : n020.cluster.edu % 0.14/0.35 % Model : x86_64 x86_64 % 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.35 % Memory : 8042.1875MB % 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.35 % CPULimit : 300 % 0.14/0.35 % WCLimit : 300 % 0.14/0.35 % DateTime : Thu Jun 20 06:29:39 EDT 2024 % 0.14/0.36 % CPUTime : % 0.43/0.63 start to proof:theBenchmark % 0.59/0.72 %------------------------------------------- % 0.59/0.72 % File :CSE---1.7 % 0.59/0.72 % Problem :theBenchmark % 0.59/0.72 % Transform :cnf % 0.59/0.72 % Format :tptp:raw % 0.59/0.72 % Command :java -jar mcs_scs.jar %d %s % 0.59/0.72 % 0.59/0.72 % Result :Theorem 0.030000s % 0.59/0.72 % Output :CNFRefutation 0.030000s % 0.59/0.72 %------------------------------------------- % 0.59/0.73 %------------------------------------------------------------------------------ % 0.59/0.73 % File : PRO011+3 : TPTP v8.2.0. Released v4.0.0. % 0.59/0.73 % Domain : Processes % 0.59/0.73 % Problem : PSL cliff problem coe-7.1.3-subocc % 0.59/0.73 % Version : Especial : Augmented > Especial. % 0.59/0.73 % English : % 0.59/0.73 % Refs : [Hal09] Halcomb (2009), Email to G. Sutcliffe % 0.59/0.73 % Source : [Hal09] % 0.59/0.73 % Names : psl-1016-subset-618-lemmas__coe-7.1.3-subocc-pd [Hal09] % 0.59/0.73 % 0.59/0.73 % Status : Theorem % 0.59/0.73 % Rating : 0.19 v8.1.0, 0.22 v7.5.0, 0.25 v7.4.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.22 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 % 0.59/0.73 % Syntax : Number of formulae : 63 ( 12 unt; 0 def) % 0.59/0.73 % Number of atoms : 218 ( 18 equ) % 0.59/0.73 % Maximal formula atoms : 10 ( 3 avg) % 0.59/0.73 % Number of connectives : 183 ( 28 ~; 6 |; 95 &) % 0.59/0.73 % ( 7 <=>; 47 =>; 0 <=; 0 <~>) % 0.59/0.73 % Maximal formula depth : 13 ( 6 avg) % 0.59/0.73 % Maximal term depth : 1 ( 1 avg) % 0.59/0.73 % Number of predicates : 18 ( 17 usr; 0 prp; 1-3 aty) % 0.59/0.73 % Number of functors : 5 ( 5 usr; 5 con; 0-0 aty) % 0.59/0.73 % Number of variables : 170 ( 145 !; 25 ?) % 0.59/0.73 % SPC : FOF_THM_RFO_SEQ % 0.59/0.73 % 0.59/0.73 % Comments : % 0.59/0.73 %------------------------------------------------------------------------------ % 0.59/0.73 fof(sos,axiom, % 0.59/0.73 ! [X0,X1] : % 0.59/0.73 ( occurrence_of(X1,X0) % 0.59/0.73 => ( activity(X0) % 0.59/0.73 & activity_occurrence(X1) ) ) ). % 0.59/0.73 % 0.59/0.73 fof(sos_01,axiom, % 0.59/0.73 ! [X2] : % 0.59/0.73 ( activity_occurrence(X2) % 0.59/0.73 => ? [X3] : % 0.59/0.73 ( activity(X3) % 0.59/0.73 & occurrence_of(X2,X3) ) ) ). % 0.59/0.73 % 0.59/0.73 fof(sos_02,axiom, % 0.59/0.73 ! [X4,X5,X6] : % 0.59/0.73 ( ( occurrence_of(X4,X5) % 0.59/0.73 & occurrence_of(X4,X6) ) % 0.59/0.73 => X5 = X6 ) ). % 0.59/0.73 % 0.59/0.73 fof(sos_03,axiom, % 0.59/0.73 ! [X7] : % 0.59/0.73 ( activity(X7) % 0.59/0.73 => subactivity(X7,X7) ) ). % 0.59/0.73 % 0.59/0.73 fof(sos_04,axiom, % 0.59/0.73 ! [X8,X9] : % 0.59/0.73 ( earlier(X8,X9) % 0.59/0.73 => ~ earlier(X9,X8) ) ). % 0.59/0.73 % 0.59/0.73 fof(sos_05,axiom, % 0.59/0.73 ! [X10,X11,X12] : % 0.59/0.73 ( ( earlier(X10,X11) % 0.59/0.73 & earlier(X11,X12) ) % 0.59/0.73 => earlier(X10,X12) ) ). % 0.59/0.73 % 0.59/0.73 fof(sos_06,axiom, % 0.59/0.73 ! [X13,X14,X15] : % 0.59/0.73 ( ( earlier(X13,X14) % 0.59/0.73 & earlier(X15,X14) ) % 0.59/0.73 => ( earlier(X15,X13) % 0.59/0.73 | earlier(X13,X15) % 0.59/0.73 | X13 = X15 ) ) ). % 0.59/0.73 % 0.59/0.73 fof(sos_07,axiom, % 0.59/0.73 ! [X16,X17] : % 0.59/0.73 ( occurrence_of(X16,X17) % 0.59/0.73 => ( arboreal(X16) % 0.59/0.73 <=> atomic(X17) ) ) ). % 0.59/0.73 % 0.59/0.73 fof(sos_08,axiom, % 0.59/0.73 ! [X18] : % 0.59/0.73 ( legal(X18) % 0.59/0.73 => arboreal(X18) ) ). % 0.59/0.73 % 0.59/0.73 fof(sos_09,axiom, % 0.59/0.73 ! [X19,X20] : % 0.59/0.73 ( ( legal(X19) % 0.59/0.73 & earlier(X20,X19) ) % 0.59/0.73 => legal(X20) ) ). % 0.59/0.73 % 0.59/0.73 fof(sos_10,axiom, % 0.59/0.73 ! [X21,X22] : % 0.59/0.73 ( precedes(X21,X22) % 0.59/0.73 <=> ( earlier(X21,X22) % 0.59/0.73 & legal(X22) ) ) ). % 0.59/0.73 % 0.59/0.73 fof(sos_11,axiom, % 0.59/0.73 ! [X23,X24,X25] : % 0.59/0.73 ( min_precedes(X24,X25,X23) % 0.59/0.73 => ? [X26,X27] : % 0.59/0.73 ( subactivity(X26,X23) % 0.59/0.73 & subactivity(X27,X23) % 0.59/0.73 & atocc(X24,X26) % 0.59/0.73 & atocc(X25,X27) ) ) ). % 0.59/0.73 % 0.59/0.73 fof(sos_12,axiom, % 0.59/0.73 ! [X28,X29] : % 0.59/0.73 ( root(X29,X28) % 0.59/0.73 => ? [X30] : % 0.59/0.73 ( subactivity(X30,X28) % 0.59/0.73 & atocc(X29,X30) ) ) ). % 0.59/0.73 % 0.59/0.73 fof(sos_13,axiom, % 0.59/0.73 ! [X31,X32,X33] : % 0.59/0.73 ( min_precedes(X31,X32,X33) % 0.59/0.73 => ? [X34] : % 0.59/0.73 ( root(X34,X33) % 0.59/0.73 & min_precedes(X34,X32,X33) ) ) ). % 0.59/0.73 % 0.59/0.73 fof(sos_14,axiom, % 0.59/0.73 ! [X35,X36,X37] : % 0.59/0.73 ( min_precedes(X35,X36,X37) % 0.59/0.73 => ~ root(X36,X37) ) ). % 0.59/0.73 % 0.59/0.73 fof(sos_15,axiom, % 0.59/0.73 ! [X38,X39,X40] : % 0.59/0.73 ( min_precedes(X38,X39,X40) % 0.59/0.73 => precedes(X38,X39) ) ). % 0.59/0.73 % 0.59/0.73 fof(sos_16,axiom, % 0.59/0.73 ! [X41,X42] : % 0.59/0.73 ( root(X41,X42) % 0.59/0.73 => legal(X41) ) ). % 0.59/0.73 % 0.59/0.73 fof(sos_17,axiom, % 0.59/0.73 ! [X43,X44] : % 0.59/0.73 ( ( atocc(X43,X44) % 0.59/0.73 & legal(X43) ) % 0.59/0.73 => root(X43,X44) ) ). % 0.59/0.73 % 0.59/0.73 fof(sos_18,axiom, % 0.59/0.73 ! [X45,X46,X47,X48] : % 0.59/0.73 ( ( min_precedes(X45,X46,X48) % 0.59/0.73 & min_precedes(X45,X47,X48) % 0.59/0.73 & precedes(X46,X47) ) % 0.59/0.73 => min_precedes(X46,X47,X48) ) ). % 0.59/0.73 % 0.59/0.73 fof(sos_19,axiom, % 0.59/0.73 ! [X49,X50,X51] : % 0.59/0.73 ( min_precedes(X49,X50,X51) % 0.59/0.73 => ~ atomic(X51) ) ). % 0.59/0.73 % 0.59/0.73 fof(sos_20,axiom, % 0.59/0.73 ! [X52,X53,X54,X55] : % 0.59/0.73 ( ( min_precedes(X53,X52,X55) % 0.59/0.73 & min_precedes(X54,X52,X55) % 0.59/0.73 & precedes(X53,X54) ) % 0.59/0.73 => min_precedes(X53,X54,X55) ) ). % 0.59/0.73 % 0.59/0.73 fof(sos_21,axiom, % 0.59/0.73 ! [X56,X57] : % 0.59/0.73 ( leaf(X56,X57) % 0.59/0.73 <=> ( ( root(X56,X57) % 0.59/0.73 | ? [X58] : min_precedes(X58,X56,X57) ) % 0.59/0.73 & ~ ? [X59] : min_precedes(X56,X59,X57) ) ) ). % 0.59/0.73 % 0.59/0.73 fof(sos_22,axiom, % 0.59/0.73 ! [X60,X61,X62] : % 0.59/0.73 ( next_subocc(X60,X61,X62) % 0.59/0.73 <=> ( min_precedes(X60,X61,X62) % 0.59/0.73 & ~ ? [X63] : % 0.59/0.73 ( min_precedes(X60,X63,X62) % 0.59/0.73 & min_precedes(X63,X61,X62) ) ) ) ). % 0.59/0.73 % 0.59/0.73 fof(sos_23,axiom, % 0.59/0.73 ! [X64,X65] : % 0.59/0.73 ( atocc(X64,X65) % 0.59/0.73 <=> ? [X66] : % 0.59/0.73 ( subactivity(X65,X66) % 0.59/0.73 & atomic(X66) % 0.59/0.73 & occurrence_of(X64,X66) ) ) ). % 0.59/0.73 % 0.59/0.73 fof(sos_24,axiom, % 0.59/0.73 ! [X67,X68] : % 0.59/0.73 ( subactivity_occurrence(X67,X68) % 0.59/0.73 => ( activity_occurrence(X67) % 0.59/0.73 & activity_occurrence(X68) ) ) ). % 0.59/0.73 % 0.59/0.73 fof(sos_25,axiom, % 0.59/0.73 ! [X69,X70,X71] : % 0.59/0.73 ( min_precedes(X70,X71,X69) % 0.59/0.73 => ? [X72] : % 0.59/0.73 ( occurrence_of(X72,X69) % 0.59/0.73 & subactivity_occurrence(X70,X72) % 0.59/0.73 & subactivity_occurrence(X71,X72) ) ) ). % 0.59/0.73 % 0.59/0.73 fof(sos_26,axiom, % 0.59/0.73 ! [X73,X74] : % 0.59/0.73 ( ( root(X74,X73) % 0.59/0.73 & ~ atomic(X73) ) % 0.59/0.73 => ? [X75] : % 0.59/0.73 ( occurrence_of(X75,X73) % 0.59/0.73 & subactivity_occurrence(X74,X75) ) ) ). % 0.59/0.73 % 0.59/0.73 fof(sos_27,axiom, % 0.59/0.73 ! [X76,X77] : % 0.59/0.73 ( ( occurrence_of(X77,X76) % 0.59/0.73 & ~ atomic(X76) ) % 0.59/0.73 => ? [X78] : % 0.59/0.73 ( root(X78,X76) % 0.59/0.73 & subactivity_occurrence(X78,X77) ) ) ). % 0.59/0.73 % 0.59/0.73 fof(sos_28,axiom, % 0.59/0.73 ! [X79,X80,X81,X82] : % 0.59/0.73 ( ( occurrence_of(X80,X79) % 0.59/0.73 & arboreal(X81) % 0.59/0.73 & arboreal(X82) % 0.59/0.73 & subactivity_occurrence(X81,X80) % 0.59/0.73 & subactivity_occurrence(X82,X80) ) % 0.59/0.73 => ( min_precedes(X81,X82,X79) % 0.59/0.73 | min_precedes(X82,X81,X79) % 0.59/0.73 | X81 = X82 ) ) ). % 0.59/0.73 % 0.59/0.73 fof(sos_29,axiom, % 0.59/0.73 ! [X83,X84,X85,X86] : % 0.59/0.73 ( ( min_precedes(X83,X84,X85) % 0.59/0.73 & occurrence_of(X86,X85) % 0.59/0.73 & subactivity_occurrence(X84,X86) ) % 0.59/0.73 => subactivity_occurrence(X83,X86) ) ). % 0.59/0.73 % 0.59/0.73 fof(sos_30,axiom, % 0.59/0.73 ! [X87,X88,X89,X90] : % 0.59/0.73 ( ( occurrence_of(X89,X87) % 0.59/0.73 & occurrence_of(X90,X88) % 0.59/0.73 & ~ atomic(X87) % 0.59/0.73 & subactivity_occurrence(X89,X90) ) % 0.59/0.73 => subactivity(X87,X88) ) ). % 0.59/0.73 % 0.59/0.73 fof(sos_31,axiom, % 0.59/0.73 ! [X91,X92,X93] : % 0.59/0.73 ( ( subactivity_occurrence(X91,X92) % 0.59/0.73 & subactivity_occurrence(X92,X93) ) % 0.59/0.73 => subactivity_occurrence(X91,X93) ) ). % 0.59/0.73 % 0.59/0.73 fof(sos_32,axiom, % 0.59/0.73 ! [X94,X95,X96,X97] : % 0.59/0.73 ( ( occurrence_of(X96,X94) % 0.59/0.73 & occurrence_of(X97,X95) % 0.59/0.73 & subactivity(X94,X95) % 0.59/0.73 & ~ subactivity_occurrence(X96,X97) ) % 0.59/0.73 => ? [X98] : % 0.59/0.73 ( subactivity_occurrence(X98,X97) % 0.59/0.73 & ~ subactivity_occurrence(X98,X96) ) ) ). % 0.59/0.73 % 0.59/0.73 fof(sos_33,axiom, % 0.59/0.73 ! [X99,X100] : % 0.59/0.73 ( root_occ(X99,X100) % 0.59/0.73 <=> ? [X101] : % 0.59/0.73 ( occurrence_of(X100,X101) % 0.59/0.73 & subactivity_occurrence(X99,X100) % 0.59/0.73 & root(X99,X101) ) ) ). % 0.59/0.73 % 0.59/0.73 fof(sos_34,axiom, % 0.59/0.73 ! [X102,X103] : % 0.59/0.73 ( leaf_occ(X102,X103) % 0.59/0.73 <=> ? [X104] : % 0.59/0.73 ( occurrence_of(X103,X104) % 0.59/0.73 & subactivity_occurrence(X102,X103) % 0.59/0.73 & leaf(X102,X104) ) ) ). % 0.59/0.73 % 0.59/0.73 fof(sos_35,axiom, % 0.59/0.73 ! [X105,X106,X107,X108] : % 0.59/0.73 ( ( occurrence_of(X107,X108) % 0.59/0.73 & root_occ(X105,X107) % 0.59/0.73 & root_occ(X106,X107) ) % 0.59/0.73 => X105 = X106 ) ). % 0.59/0.73 % 0.59/0.73 fof(sos_36,axiom, % 0.59/0.74 ! [X109,X110,X111,X112] : % 0.59/0.74 ( ( occurrence_of(X111,X112) % 0.59/0.74 & ~ atomic(X112) % 0.59/0.74 & leaf_occ(X109,X111) % 0.59/0.74 & leaf_occ(X110,X111) ) % 0.59/0.74 => X109 = X110 ) ). % 0.59/0.74 % 0.59/0.74 fof(sos_37,axiom, % 0.59/0.74 ! [X113,X114,X115] : % 0.59/0.74 ( ( occurrence_of(X113,X115) % 0.59/0.74 & leaf_occ(X114,X113) ) % 0.59/0.74 => ~ ? [X116] : min_precedes(X114,X116,X115) ) ). % 0.59/0.74 % 0.59/0.74 fof(sos_38,axiom, % 0.59/0.74 ! [X117,X118,X119] : % 0.59/0.74 ( ( occurrence_of(X117,X119) % 0.59/0.74 & root_occ(X118,X117) ) % 0.59/0.74 => ~ ? [X120] : min_precedes(X120,X118,X119) ) ). % 0.59/0.74 % 0.59/0.74 fof(sos_39,axiom, % 0.59/0.74 ! [X121,X122,X123,X124,X125] : % 0.59/0.74 ( ( next_subocc(X121,X122,X124) % 0.59/0.74 & next_subocc(X121,X123,X124) % 0.59/0.74 & occurrence_of(X125,X124) % 0.59/0.74 & subactivity_occurrence(X123,X125) % 0.59/0.74 & subactivity_occurrence(X122,X125) ) % 0.59/0.74 => X122 = X123 ) ). % 0.59/0.74 % 0.59/0.74 fof(sos_40,axiom, % 0.59/0.74 ! [X126,X127,X128,X129] : % 0.59/0.74 ( ( next_subocc(X127,X126,X129) % 0.59/0.74 & next_subocc(X128,X126,X129) ) % 0.59/0.74 => X127 = X128 ) ). % 0.59/0.74 % 0.59/0.74 fof(sos_41,axiom, % 0.59/0.74 ! [X130,X131,X132,X133] : % 0.59/0.74 ( ( occurrence_of(X130,X133) % 0.59/0.74 & leaf_occ(X131,X130) % 0.59/0.74 & root_occ(X132,X130) % 0.59/0.74 & X131 != X132 ) % 0.59/0.74 => min_precedes(X132,X131,X133) ) ). % 0.59/0.74 % 0.59/0.74 fof(sos_42,axiom, % 0.59/0.74 ! [X134,X135,X136,X137] : % 0.59/0.74 ( ( occurrence_of(X135,X134) % 0.59/0.74 & subactivity_occurrence(X136,X135) % 0.59/0.74 & root_occ(X137,X135) % 0.59/0.74 & arboreal(X136) % 0.59/0.74 & ~ min_precedes(X137,X136,X134) ) % 0.59/0.74 => X137 = X136 ) ). % 0.59/0.74 % 0.59/0.74 fof(sos_43,axiom, % 0.59/0.74 ! [X138,X139,X140,X141] : % 0.59/0.74 ( ( occurrence_of(X139,X138) % 0.59/0.74 & subactivity_occurrence(X140,X139) % 0.59/0.74 & leaf_occ(X141,X139) % 0.59/0.74 & arboreal(X140) % 0.59/0.74 & ~ min_precedes(X140,X141,X138) ) % 0.59/0.74 => X141 = X140 ) ). % 0.59/0.74 % 0.59/0.74 fof(sos_44,axiom, % 0.62/0.74 ! [X142,X143,X144] : % 0.62/0.74 ( next_subocc(X142,X143,X144) % 0.62/0.74 => ( arboreal(X142) % 0.62/0.74 & arboreal(X143) ) ) ). % 0.62/0.74 % 0.62/0.74 fof(sos_45,axiom, % 0.62/0.74 ! [X145,X146] : % 0.62/0.74 ( ( leaf(X145,X146) % 0.62/0.74 & ~ atomic(X146) ) % 0.62/0.74 => ? [X147] : % 0.62/0.74 ( occurrence_of(X147,X146) % 0.62/0.74 & leaf_occ(X145,X147) ) ) ). % 0.62/0.74 % 0.62/0.74 fof(sos_46,axiom, % 0.62/0.74 ! [X148,X149,X150] : % 0.62/0.74 ( min_precedes(X148,X149,X150) % 0.62/0.74 => arboreal(X148) ) ). % 0.62/0.74 % 0.62/0.74 fof(sos_47,axiom, % 0.62/0.74 ! [X151,X152,X153,X154,X155] : % 0.62/0.74 ( ( occurrence_of(X152,X151) % 0.62/0.74 & root_occ(X154,X152) % 0.62/0.74 & leaf_occ(X155,X152) % 0.62/0.74 & subactivity_occurrence(X153,X152) % 0.62/0.74 & min_precedes(X153,X155,X151) % 0.62/0.74 & X153 != X154 ) % 0.62/0.74 => min_precedes(X154,X153,X151) ) ). % 0.62/0.74 % 0.62/0.74 fof(sos_48,axiom, % 0.62/0.74 ! [X156,X157,X158,X159,X160] : % 0.62/0.74 ( ( occurrence_of(X157,X156) % 0.62/0.74 & root_occ(X159,X157) % 0.62/0.74 & leaf_occ(X160,X157) % 0.62/0.74 & subactivity_occurrence(X158,X157) % 0.62/0.74 & min_precedes(X159,X158,X156) % 0.62/0.74 & X158 != X160 ) % 0.62/0.74 => min_precedes(X158,X160,X156) ) ). % 0.62/0.74 % 0.62/0.74 fof(sos_49,axiom, % 0.62/0.74 ! [X161] : % 0.62/0.74 ( occurrence_of(X161,tptp0) % 0.62/0.74 => ? [X162,X163,X164] : % 0.62/0.74 ( occurrence_of(X162,tptp3) % 0.62/0.74 & root_occ(X162,X161) % 0.62/0.74 & occurrence_of(X163,tptp4) % 0.62/0.74 & next_subocc(X162,X163,tptp0) % 0.62/0.74 & ( occurrence_of(X164,tptp1) % 0.62/0.74 | occurrence_of(X164,tptp2) ) % 0.62/0.74 & next_subocc(X163,X164,tptp0) % 0.62/0.74 & leaf_occ(X164,X161) ) ) ). % 0.62/0.74 % 0.62/0.74 fof(sos_50,axiom, % 0.62/0.74 activity(tptp0) ). % 0.62/0.74 % 0.62/0.74 fof(sos_51,axiom, % 0.62/0.74 ~ atomic(tptp0) ). % 0.62/0.74 % 0.62/0.74 fof(sos_52,axiom, % 0.62/0.74 atomic(tptp4) ). % 0.62/0.74 % 0.62/0.74 fof(sos_53,axiom, % 0.62/0.74 atomic(tptp1) ). % 0.62/0.74 % 0.62/0.74 fof(sos_54,axiom, % 0.62/0.74 atomic(tptp2) ). % 0.62/0.74 % 0.62/0.74 fof(sos_55,axiom, % 0.62/0.74 atomic(tptp3) ). % 0.62/0.74 % 0.62/0.74 fof(sos_56,axiom, % 0.62/0.74 tptp4 != tptp3 ). % 0.62/0.74 % 0.62/0.74 fof(sos_57,axiom, % 0.62/0.74 tptp4 != tptp1 ). % 0.62/0.74 % 0.62/0.74 fof(sos_58,axiom, % 0.62/0.74 tptp4 != tptp2 ). % 0.62/0.74 % 0.62/0.74 fof(sos_59,axiom, % 0.62/0.74 tptp3 != tptp1 ). % 0.62/0.74 % 0.62/0.74 fof(sos_60,axiom, % 0.62/0.74 tptp3 != tptp2 ). % 0.62/0.74 % 0.62/0.74 fof(sos_61,axiom, % 0.62/0.74 tptp1 != tptp2 ). % 0.62/0.74 % 0.62/0.74 fof(goals,conjecture, % 0.62/0.74 ! [X165] : % 0.62/0.74 ( occurrence_of(X165,tptp0) % 0.62/0.74 => ? [X166,X167] : % 0.62/0.74 ( leaf_occ(X167,X165) % 0.62/0.74 & ( occurrence_of(X167,tptp1) % 0.62/0.74 => ~ ? [X168] : % 0.62/0.74 ( occurrence_of(X168,tptp2) % 0.62/0.74 & subactivity_occurrence(X168,X165) % 0.62/0.74 & min_precedes(X166,X168,tptp0) ) ) % 0.62/0.74 & ( occurrence_of(X167,tptp2) % 0.62/0.74 => ~ ? [X169] : % 0.62/0.74 ( occurrence_of(X169,tptp1) % 0.62/0.74 & subactivity_occurrence(X169,X165) % 0.62/0.74 & min_precedes(X166,X169,tptp0) ) ) ) ) ). % 0.62/0.74 % 0.62/0.74 %------------------------------------------------------------------------------ % 0.62/0.74 %------------------------------------------- % 0.62/0.74 % Proof found % 0.62/0.74 % SZS status Theorem for theBenchmark % 0.62/0.74 % SZS output start Proof % 0.62/0.74 %ClaNum:197(EqnAxiom:79) % 0.62/0.74 %VarNum:655(SingletonVarNum:266) % 0.62/0.74 %MaxLitNum:8 % 0.62/0.74 %MaxfuncDepth:1 % 0.62/0.74 %SharedTerms:19 % 0.62/0.74 %goalClause: 85 116 138 139 140 141 153 154 155 156 160 161 169 170 171 172 176 % 0.62/0.74 %singleGoalClaCount:1 % 0.62/0.74 [80]P1(a1) % 0.62/0.74 [81]P2(a24) % 0.62/0.74 [82]P2(a27) % 0.62/0.74 [83]P2(a25) % 0.62/0.74 [84]P2(a26) % 0.62/0.74 [85]P6(a2,a1) % 0.62/0.74 [86]~E(a27,a24) % 0.62/0.74 [87]~E(a25,a24) % 0.62/0.74 [88]~E(a25,a27) % 0.62/0.74 [89]~E(a26,a24) % 0.62/0.74 [90]~E(a26,a27) % 0.62/0.74 [91]~E(a26,a25) % 0.62/0.74 [92]~P2(a1) % 0.62/0.74 [93]~P7(x931)+P3(x931) % 0.62/0.74 [95]~P1(x951)+P13(x951,x951) % 0.62/0.74 [94]~P4(x941)+P1(f3(x941)) % 0.62/0.74 [102]~P4(x1021)+P6(x1021,f3(x1021)) % 0.62/0.74 [109]~P6(x1091,a1)+P6(f4(x1091),a24) % 0.62/0.74 [110]~P6(x1101,a1)+P6(f12(x1101),a27) % 0.62/0.74 [111]~P6(x1111,a1)+P16(f4(x1111),x1111) % 0.62/0.74 [112]~P6(x1121,a1)+P9(f13(x1121),x1121) % 0.62/0.74 [146]~P6(x1461,a1)+P11(f4(x1461),f12(x1461),a1) % 0.62/0.74 [147]~P6(x1471,a1)+P11(f12(x1471),f13(x1471),a1) % 0.62/0.74 [96]P1(x961)+~P6(x962,x961) % 0.62/0.74 [97]P4(x971)+~P6(x971,x972) % 0.62/0.74 [98]P4(x981)+~P17(x982,x981) % 0.62/0.74 [99]P4(x991)+~P17(x991,x992) % 0.62/0.74 [100]P7(x1001)+~P14(x1002,x1001) % 0.62/0.74 [101]P7(x1011)+~P15(x1011,x1012) % 0.62/0.74 [106]~P14(x1061,x1062)+P8(x1061,x1062) % 0.62/0.74 [107]~P16(x1071,x1072)+P17(x1071,x1072) % 0.62/0.74 [108]~P9(x1081,x1082)+P17(x1081,x1082) % 0.62/0.74 [115]~P8(x1152,x1151)+~P8(x1151,x1152) % 0.62/0.74 [118]~P5(x1181,x1182)+P2(f14(x1181,x1182)) % 0.62/0.74 [122]~P5(x1221,x1222)+P6(x1221,f14(x1221,x1222)) % 0.62/0.74 [123]~P16(x1232,x1231)+P6(x1231,f5(x1232,x1231)) % 0.62/0.74 [124]~P9(x1242,x1241)+P6(x1241,f10(x1242,x1241)) % 0.62/0.74 [125]~P5(x1252,x1251)+P13(x1251,f14(x1252,x1251)) % 0.62/0.74 [126]~P15(x1261,x1262)+P5(x1261,f15(x1262,x1261)) % 0.62/0.74 [127]~P16(x1271,x1272)+P15(x1271,f5(x1271,x1272)) % 0.62/0.74 [128]~P9(x1281,x1282)+P10(x1281,f10(x1281,x1282)) % 0.62/0.74 [129]~P15(x1292,x1291)+P13(f15(x1291,x1292),x1291) % 0.62/0.74 [149]P3(x1491)+~P12(x1491,x1492,x1493) % 0.62/0.74 [150]P3(x1501)+~P11(x1502,x1501,x1503) % 0.62/0.74 [151]P3(x1511)+~P11(x1511,x1512,x1513) % 0.62/0.74 [152]~P2(x1521)+~P12(x1522,x1523,x1521) % 0.62/0.74 [157]P14(x1571,x1572)+~P12(x1571,x1572,x1573) % 0.62/0.74 [158]~P15(x1581,x1582)+~P12(x1583,x1581,x1582) % 0.62/0.74 [159]~P10(x1591,x1592)+~P12(x1591,x1593,x1592) % 0.62/0.74 [173]~P11(x1731,x1732,x1733)+P12(x1731,x1732,x1733) % 0.62/0.74 [179]~P12(x1791,x1793,x1792)+P5(x1791,f18(x1792,x1791,x1793)) % 0.62/0.74 [180]~P12(x1803,x1801,x1802)+P5(x1801,f19(x1802,x1803,x1801)) % 0.62/0.74 [181]~P12(x1813,x1811,x1812)+P17(x1811,f7(x1812,x1813,x1811)) % 0.62/0.74 [182]~P12(x1821,x1823,x1822)+P17(x1821,f7(x1822,x1821,x1823)) % 0.62/0.74 [183]~P12(x1832,x1833,x1831)+P6(f7(x1831,x1832,x1833),x1831) % 0.62/0.74 [184]~P12(x1842,x1843,x1841)+P13(f18(x1841,x1842,x1843),x1841) % 0.62/0.74 [185]~P12(x1852,x1853,x1851)+P13(f19(x1851,x1852,x1853),x1851) % 0.62/0.74 [186]~P12(x1861,x1862,x1863)+P15(f22(x1861,x1862,x1863),x1863) % 0.62/0.74 [190]~P12(x1901,x1902,x1903)+P12(f22(x1901,x1902,x1903),x1902,x1903) % 0.62/0.74 [116]P6(x1161,a26)+~P9(x1161,a2)+P6(x1161,a25) % 0.62/0.74 [119]~P6(x1191,a1)+P6(f13(x1191),a25)+P6(f13(x1191),a26) % 0.62/0.74 [103]~P6(x1031,x1032)+P3(x1031)+~P2(x1032) % 0.62/0.74 [104]~P6(x1042,x1041)+P2(x1041)+~P3(x1042) % 0.62/0.74 [105]~P8(x1051,x1052)+P7(x1051)+~P7(x1052) % 0.62/0.74 [113]~P7(x1132)+~P8(x1131,x1132)+P14(x1131,x1132) % 0.62/0.74 [114]~P7(x1141)+~P5(x1141,x1142)+P15(x1141,x1142) % 0.62/0.74 [131]~P15(x1312,x1311)+P2(x1311)+P17(x1312,f6(x1311,x1312)) % 0.62/0.74 [132]~P10(x1322,x1321)+P2(x1321)+P9(x1322,f11(x1322,x1321)) % 0.62/0.74 [133]~P10(x1332,x1331)+P2(x1331)+P6(f11(x1332,x1331),x1331) % 0.62/0.74 [134]~P15(x1342,x1341)+P2(x1341)+P6(f6(x1341,x1342),x1341) % 0.62/0.74 [135]~P6(x1352,x1351)+P2(x1351)+P15(f8(x1351,x1352),x1351) % 0.62/0.74 [136]~P6(x1362,x1361)+P2(x1361)+P17(f8(x1361,x1362),x1362) % 0.62/0.74 [138]~P9(x1381,a2)+P6(x1381,a25)+P6(f16(x1382,x1381),a25) % 0.62/0.74 [139]~P9(x1391,a2)+P6(x1391,a25)+P17(f16(x1392,x1391),a2) % 0.62/0.74 [140]~P9(x1401,a2)+P6(x1401,a26)+P6(f17(x1402,x1401),a26) % 0.62/0.74 [141]~P9(x1411,a2)+P6(x1411,a26)+P17(f17(x1412,x1411),a2) % 0.62/0.74 [153]~P9(x1532,a2)+P6(f16(x1531,x1532),a25)+P6(f17(x1531,x1532),a26) % 0.62/0.74 [154]~P9(x1542,a2)+P17(f16(x1541,x1542),a2)+P6(f17(x1541,x1542),a26) % 0.62/0.74 [155]~P9(x1552,a2)+P17(f17(x1551,x1552),a2)+P6(f16(x1551,x1552),a25) % 0.62/0.74 [156]~P9(x1562,a2)+P17(f16(x1561,x1562),a2)+P17(f17(x1561,x1562),a2) % 0.62/0.74 [160]~P9(x1601,a2)+P6(x1601,a25)+P12(x1602,f16(x1602,x1601),a1) % 0.62/0.74 [161]~P9(x1611,a2)+P6(x1611,a26)+P12(x1612,f17(x1612,x1611),a1) % 0.62/0.74 [162]~P15(x1621,x1622)+P10(x1621,x1622)+P12(x1621,f20(x1621,x1622),x1622) % 0.62/0.74 [163]~P10(x1631,x1632)+P15(x1631,x1632)+P12(f21(x1631,x1632),x1631,x1632) % 0.62/0.74 [169]~P9(x1692,a2)+P12(x1691,f16(x1691,x1692),a1)+P6(f17(x1691,x1692),a26) % 0.62/0.74 [170]~P9(x1702,a2)+P12(x1701,f17(x1701,x1702),a1)+P6(f16(x1701,x1702),a25) % 0.62/0.75 [171]~P9(x1712,a2)+P12(x1711,f16(x1711,x1712),a1)+P17(f17(x1711,x1712),a2) % 0.62/0.75 [172]~P9(x1722,a2)+P12(x1721,f17(x1721,x1722),a1)+P17(f16(x1721,x1722),a2) % 0.62/0.75 [176]~P9(x1762,a2)+P12(x1761,f16(x1761,x1762),a1)+P12(x1761,f17(x1761,x1762),a1) % 0.62/0.75 [117]~P6(x1173,x1171)+E(x1171,x1172)+~P6(x1173,x1172) % 0.62/0.75 [120]~P8(x1201,x1203)+P8(x1201,x1202)+~P8(x1203,x1202) % 0.62/0.75 [121]~P17(x1211,x1213)+P17(x1211,x1212)+~P17(x1213,x1212) % 0.62/0.75 [177]P10(x1771,x1772)+~P12(x1773,x1771,x1772)+P12(x1771,f20(x1771,x1772),x1772) % 0.62/0.75 [194]~P12(x1941,x1942,x1943)+P11(x1941,x1942,x1943)+P12(x1941,f23(x1941,x1942,x1943),x1943) % 0.62/0.75 [195]~P12(x1951,x1952,x1953)+P11(x1951,x1952,x1953)+P12(f23(x1951,x1952,x1953),x1952,x1953) % 0.62/0.75 [165]~P6(x1651,x1652)+~P12(x1654,x1653,x1652)+~P16(x1653,x1651) % 0.62/0.75 [166]~P6(x1661,x1662)+~P12(x1663,x1664,x1662)+~P9(x1663,x1661) % 0.62/0.75 [175]~P11(x1751,x1753,x1754)+E(x1751,x1752)+~P11(x1752,x1753,x1754) % 0.62/0.75 [193]~P11(x1934,x1932,x1933)+~P12(x1931,x1932,x1933)+~P12(x1934,x1931,x1933) % 0.62/0.75 [130]~P6(x1301,x1303)+~P13(x1302,x1303)+P5(x1301,x1302)+~P2(x1303) % 0.62/0.75 [144]~P15(x1441,x1443)+~P17(x1441,x1442)+P16(x1441,x1442)+~P6(x1442,x1443) % 0.62/0.75 [145]~P10(x1451,x1453)+~P17(x1451,x1452)+P9(x1451,x1452)+~P6(x1452,x1453) % 0.62/0.75 [137]~P16(x1372,x1373)+~P16(x1371,x1373)+E(x1371,x1372)+~P6(x1373,x1374) % 0.62/0.75 [174]~P12(x1741,x1744,x1743)+P17(x1741,x1742)+~P6(x1742,x1743)+~P17(x1744,x1742) % 0.62/0.75 [191]~P14(x1911,x1912)+~P12(x1914,x1911,x1913)+P12(x1911,x1912,x1913)+~P12(x1914,x1912,x1913) % 0.62/0.75 [192]~P14(x1921,x1922)+~P12(x1921,x1924,x1923)+P12(x1921,x1922,x1923)+~P12(x1922,x1924,x1923) % 0.62/0.75 [143]P8(x1432,x1431)+P8(x1431,x1432)+~P8(x1431,x1433)+E(x1431,x1432)+~P8(x1432,x1433) % 0.62/0.75 [142]~P9(x1422,x1424)+~P9(x1421,x1424)+E(x1421,x1422)+~P6(x1424,x1423)+P2(x1423) % 0.62/0.75 [148]~P17(x1484,x1483)+P2(x1481)+P13(x1481,x1482)+~P6(x1483,x1482)+~P6(x1484,x1481) % 0.62/0.75 [164]~P16(x1642,x1644)+~P9(x1641,x1644)+E(x1641,x1642)+P12(x1642,x1641,x1643)+~P6(x1644,x1643) % 0.62/0.75 [196]~P6(x1962,x1964)+~P6(x1961,x1963)+~P13(x1963,x1964)+P17(x1961,x1962)+P17(f9(x1963,x1964,x1961,x1962),x1962) % 0.62/0.75 [197]~P13(x1974,x1973)+P17(x1971,x1972)+~P6(x1972,x1973)+~P6(x1971,x1974)+~P17(f9(x1974,x1973,x1971,x1972),x1971) % 0.62/0.75 [167]~P3(x1671)+~P17(x1671,x1674)+~P16(x1672,x1674)+E(x1671,x1672)+P12(x1672,x1671,x1673)+~P6(x1674,x1673) % 0.62/0.75 [168]~P3(x1681)+~P17(x1681,x1684)+~P9(x1682,x1684)+E(x1681,x1682)+P12(x1681,x1682,x1683)+~P6(x1684,x1683) % 0.62/0.75 [189]~P17(x1892,x1893)+~P17(x1891,x1893)+~P11(x1895,x1891,x1894)+E(x1891,x1892)+~P11(x1895,x1892,x1894)+~P6(x1893,x1894) % 0.62/0.75 [187]~P17(x1872,x1874)+~P9(x1871,x1874)+~P12(x1875,x1872,x1873)+E(x1871,x1872)+P12(x1872,x1871,x1873)+~P6(x1874,x1873)+~P16(x1875,x1874) % 0.62/0.75 [188]~P17(x1882,x1884)+~P16(x1881,x1884)+~P12(x1882,x1885,x1883)+E(x1881,x1882)+P12(x1881,x1882,x1883)+~P6(x1884,x1883)+~P9(x1885,x1884) % 0.62/0.75 [178]P12(x1781,x1782,x1783)+~P3(x1782)+~P3(x1781)+~P17(x1782,x1784)+~P17(x1781,x1784)+E(x1781,x1782)+P12(x1782,x1781,x1783)+~P6(x1784,x1783) % 0.62/0.75 %EqnAxiom % 0.62/0.75 [1]E(x11,x11) % 0.62/0.75 [2]E(x22,x21)+~E(x21,x22) % 0.62/0.75 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 0.62/0.75 [4]~E(x41,x42)+E(f3(x41),f3(x42)) % 0.62/0.75 [5]~E(x51,x52)+E(f9(x51,x53,x54,x55),f9(x52,x53,x54,x55)) % 0.62/0.75 [6]~E(x61,x62)+E(f9(x63,x61,x64,x65),f9(x63,x62,x64,x65)) % 0.62/0.75 [7]~E(x71,x72)+E(f9(x73,x74,x71,x75),f9(x73,x74,x72,x75)) % 0.62/0.75 [8]~E(x81,x82)+E(f9(x83,x84,x85,x81),f9(x83,x84,x85,x82)) % 0.62/0.75 [9]~E(x91,x92)+E(f4(x91),f4(x92)) % 0.62/0.75 [10]~E(x101,x102)+E(f12(x101),f12(x102)) % 0.62/0.75 [11]~E(x111,x112)+E(f23(x111,x113,x114),f23(x112,x113,x114)) % 0.62/0.75 [12]~E(x121,x122)+E(f23(x123,x121,x124),f23(x123,x122,x124)) % 0.62/0.75 [13]~E(x131,x132)+E(f23(x133,x134,x131),f23(x133,x134,x132)) % 0.62/0.75 [14]~E(x141,x142)+E(f13(x141),f13(x142)) % 0.62/0.75 [15]~E(x151,x152)+E(f14(x151,x153),f14(x152,x153)) % 0.62/0.75 [16]~E(x161,x162)+E(f14(x163,x161),f14(x163,x162)) % 0.62/0.75 [17]~E(x171,x172)+E(f18(x171,x173,x174),f18(x172,x173,x174)) % 0.62/0.75 [18]~E(x181,x182)+E(f18(x183,x181,x184),f18(x183,x182,x184)) % 0.62/0.75 [19]~E(x191,x192)+E(f18(x193,x194,x191),f18(x193,x194,x192)) % 0.62/0.75 [20]~E(x201,x202)+E(f7(x201,x203,x204),f7(x202,x203,x204)) % 0.62/0.75 [21]~E(x211,x212)+E(f7(x213,x211,x214),f7(x213,x212,x214)) % 0.62/0.75 [22]~E(x221,x222)+E(f7(x223,x224,x221),f7(x223,x224,x222)) % 0.62/0.75 [23]~E(x231,x232)+E(f20(x231,x233),f20(x232,x233)) % 0.62/0.75 [24]~E(x241,x242)+E(f20(x243,x241),f20(x243,x242)) % 0.62/0.75 [25]~E(x251,x252)+E(f5(x251,x253),f5(x252,x253)) % 0.62/0.75 [26]~E(x261,x262)+E(f5(x263,x261),f5(x263,x262)) % 0.62/0.75 [27]~E(x271,x272)+E(f10(x271,x273),f10(x272,x273)) % 0.62/0.75 [28]~E(x281,x282)+E(f10(x283,x281),f10(x283,x282)) % 0.62/0.75 [29]~E(x291,x292)+E(f19(x291,x293,x294),f19(x292,x293,x294)) % 0.62/0.76 [30]~E(x301,x302)+E(f19(x303,x301,x304),f19(x303,x302,x304)) % 0.62/0.76 [31]~E(x311,x312)+E(f19(x313,x314,x311),f19(x313,x314,x312)) % 0.62/0.76 [32]~E(x321,x322)+E(f15(x321,x323),f15(x322,x323)) % 0.62/0.76 [33]~E(x331,x332)+E(f15(x333,x331),f15(x333,x332)) % 0.62/0.76 [34]~E(x341,x342)+E(f17(x341,x343),f17(x342,x343)) % 0.62/0.76 [35]~E(x351,x352)+E(f17(x353,x351),f17(x353,x352)) % 0.62/0.76 [36]~E(x361,x362)+E(f16(x361,x363),f16(x362,x363)) % 0.62/0.76 [37]~E(x371,x372)+E(f16(x373,x371),f16(x373,x372)) % 0.62/0.76 [38]~E(x381,x382)+E(f22(x381,x383,x384),f22(x382,x383,x384)) % 0.62/0.76 [39]~E(x391,x392)+E(f22(x393,x391,x394),f22(x393,x392,x394)) % 0.62/0.76 [40]~E(x401,x402)+E(f22(x403,x404,x401),f22(x403,x404,x402)) % 0.62/0.76 [41]~E(x411,x412)+E(f6(x411,x413),f6(x412,x413)) % 0.62/0.76 [42]~E(x421,x422)+E(f6(x423,x421),f6(x423,x422)) % 0.62/0.76 [43]~E(x431,x432)+E(f11(x431,x433),f11(x432,x433)) % 0.62/0.76 [44]~E(x441,x442)+E(f11(x443,x441),f11(x443,x442)) % 0.62/0.76 [45]~E(x451,x452)+E(f8(x451,x453),f8(x452,x453)) % 0.62/0.76 [46]~E(x461,x462)+E(f8(x463,x461),f8(x463,x462)) % 0.62/0.76 [47]~E(x471,x472)+E(f21(x471,x473),f21(x472,x473)) % 0.62/0.76 [48]~E(x481,x482)+E(f21(x483,x481),f21(x483,x482)) % 0.62/0.76 [49]~P1(x491)+P1(x492)+~E(x491,x492) % 0.62/0.76 [50]~P2(x501)+P2(x502)+~E(x501,x502) % 0.62/0.76 [51]P6(x512,x513)+~E(x511,x512)+~P6(x511,x513) % 0.62/0.76 [52]P6(x523,x522)+~E(x521,x522)+~P6(x523,x521) % 0.62/0.76 [53]P17(x532,x533)+~E(x531,x532)+~P17(x531,x533) % 0.62/0.76 [54]P17(x543,x542)+~E(x541,x542)+~P17(x543,x541) % 0.62/0.76 [55]P13(x552,x553)+~E(x551,x552)+~P13(x551,x553) % 0.62/0.76 [56]P13(x563,x562)+~E(x561,x562)+~P13(x563,x561) % 0.62/0.76 [57]P12(x572,x573,x574)+~E(x571,x572)+~P12(x571,x573,x574) % 0.62/0.76 [58]P12(x583,x582,x584)+~E(x581,x582)+~P12(x583,x581,x584) % 0.62/0.76 [59]P12(x593,x594,x592)+~E(x591,x592)+~P12(x593,x594,x591) % 0.62/0.76 [60]P14(x602,x603)+~E(x601,x602)+~P14(x601,x603) % 0.62/0.76 [61]P14(x613,x612)+~E(x611,x612)+~P14(x613,x611) % 0.62/0.76 [62]~P3(x621)+P3(x622)+~E(x621,x622) % 0.62/0.76 [63]~P7(x631)+P7(x632)+~E(x631,x632) % 0.62/0.76 [64]P9(x642,x643)+~E(x641,x642)+~P9(x641,x643) % 0.62/0.76 [65]P9(x653,x652)+~E(x651,x652)+~P9(x653,x651) % 0.62/0.76 [66]~P4(x661)+P4(x662)+~E(x661,x662) % 0.62/0.76 [67]P15(x672,x673)+~E(x671,x672)+~P15(x671,x673) % 0.62/0.76 [68]P15(x683,x682)+~E(x681,x682)+~P15(x683,x681) % 0.62/0.76 [69]P10(x692,x693)+~E(x691,x692)+~P10(x691,x693) % 0.62/0.76 [70]P10(x703,x702)+~E(x701,x702)+~P10(x703,x701) % 0.62/0.76 [71]P5(x712,x713)+~E(x711,x712)+~P5(x711,x713) % 0.62/0.76 [72]P5(x723,x722)+~E(x721,x722)+~P5(x723,x721) % 0.62/0.76 [73]P8(x732,x733)+~E(x731,x732)+~P8(x731,x733) % 0.62/0.76 [74]P8(x743,x742)+~E(x741,x742)+~P8(x743,x741) % 0.62/0.76 [75]P11(x752,x753,x754)+~E(x751,x752)+~P11(x751,x753,x754) % 0.62/0.76 [76]P11(x763,x762,x764)+~E(x761,x762)+~P11(x763,x761,x764) % 0.62/0.76 [77]P11(x773,x774,x772)+~E(x771,x772)+~P11(x773,x774,x771) % 0.62/0.76 [78]P16(x782,x783)+~E(x781,x782)+~P16(x781,x783) % 0.62/0.76 [79]P16(x793,x792)+~E(x791,x792)+~P16(x793,x791) % 0.62/0.76 % 0.62/0.76 %------------------------------------------- % 0.62/0.76 cnf(202,plain, % 0.62/0.76 (~P3(a2)), % 0.62/0.76 inference(scs_inference,[],[85,81,92,152,173,104])). % 0.62/0.76 cnf(204,plain, % 0.62/0.76 (~P12(a2,x2041,x2042)), % 0.62/0.76 inference(scs_inference,[],[85,81,92,152,173,104,149])). % 0.62/0.76 cnf(208,plain, % 0.62/0.76 (~P15(a2,x2081)), % 0.62/0.76 inference(scs_inference,[],[85,81,92,152,173,104,149,93,101])). % 0.62/0.76 cnf(216,plain, % 0.62/0.76 (~P14(x2161,a2)), % 0.62/0.76 inference(scs_inference,[],[85,81,92,152,173,104,149,93,101,127,150,151,100])). % 0.62/0.76 cnf(232,plain, % 0.62/0.76 (~P12(x2321,a2,x2322)), % 0.62/0.76 inference(scs_inference,[],[216,157])). % 0.62/0.76 cnf(264,plain, % 0.62/0.76 (~P6(a2,a25)), % 0.62/0.76 inference(scs_inference,[],[202,232,83,208,152,163,103])). % 0.62/0.76 cnf(285,plain, % 0.62/0.76 (~P9(x2851,a2)+P12(a2,f16(a2,x2851),a1)), % 0.62/0.76 inference(scs_inference,[],[85,202,204,264,84,152,103,52,173,176])). % 0.62/0.76 cnf(293,plain, % 0.62/0.76 ($false), % 0.62/0.76 inference(scs_inference,[],[85,204,285,112]), % 0.62/0.76 ['proof']). % 0.62/0.76 % SZS output end Proof % 0.62/0.76 % Total time :0.030000s %------------------------------------------------------------------------------