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