%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : MGT034-2 : TPTP v9.3.0. Released v2.4.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % Computer : n001.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 8 06:04:18 AM UTC 2026 % Result : Unsatisfiable 116.11s 116.35s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : MGT034-2 : TPTP v9.3.0. Released v2.4.0. % 0.00/0.03 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.08/0.35 % Computer : n001.cluster.edu % 0.08/0.35 % Model : x86_64 x86_64 % 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.08/0.35 % Memory : 8046.5625MB % 0.08/0.35 % OS : Linux 6.8.0-71-generic % 0.08/0.35 % CPULimit : 300 % 0.08/0.35 % WCLimit : 300 % 0.08/0.35 % DateTime : Mon Sep 7 12:37:37 UTC 2026 % 0.08/0.35 % CPUTime : % 0.26/0.52 start to proof:theBenchmark % 116.11/116.34 %------------------------------------------- % 116.11/116.34 % File :CSE---1.7 % 116.11/116.34 % Problem :theBenchmark % 116.11/116.34 % Transform :cnf % 116.11/116.34 % Format :tptp:raw % 116.11/116.34 % Command :java -jar mcs_scs.jar %d %s % 116.11/116.34 % 116.11/116.34 % Result :Theorem 115.741414s % 116.11/116.34 % Output :CNFRefutation 115.741414s % 116.11/116.34 %------------------------------------------- % 116.11/116.34 %-------------------------------------------------------------------------- % 116.11/116.34 % File : MGT034-2 : TPTP v9.3.0. Released v2.4.0. % 116.11/116.34 % Domain : Management (Organisation Theory) % 116.11/116.34 % Problem : Selection favors FMs above EPs until critical point reached % 116.11/116.34 % Version : [PM93] axioms. % 116.11/116.34 % English : Selection favors first movers above efficient producers past % 116.11/116.34 % the appearance of efficient producers until the critical % 116.11/116.34 % point is reached. % 116.11/116.34 % 116.11/116.34 % Refs : [PM93] Peli & Masuch (1993), The Logic of Propogation Strateg % 116.11/116.34 % : [PM94] Peli & Masuch (1994), The Logic of Propogation Strateg % 116.11/116.34 % : [PB+94] Peli et al. (1994), A Logical Approach to Formalizing % 116.11/116.34 % Source : [TPTP] % 116.11/116.34 % Names : % 116.11/116.34 % 116.11/116.34 % Status : Unsatisfiable % 116.11/116.34 % Rating : 0.08 v9.3.0, 0.05 v9.0.0, 0.10 v8.1.0, 0.00 v7.5.0, 0.05 v7.4.0, 0.06 v7.3.0, 0.08 v7.1.0, 0.00 v7.0.0, 0.07 v6.4.0, 0.00 v6.2.0, 0.10 v6.1.0, 0.21 v6.0.0, 0.20 v5.5.0, 0.30 v5.3.0, 0.22 v5.2.0, 0.12 v5.0.0, 0.07 v4.1.0, 0.00 v4.0.0, 0.09 v3.7.0, 0.00 v3.5.0, 0.09 v3.4.0, 0.17 v3.3.0, 0.21 v3.2.0, 0.15 v3.1.0, 0.27 v2.7.0, 0.25 v2.6.0, 0.22 v2.4.0 % 116.11/116.34 % Syntax : Number of clauses : 30 ( 5 unt; 3 nHn; 30 RR) % 116.11/116.35 % Number of literals : 90 ( 4 equ; 60 neg) % 116.11/116.35 % Maximal clause size : 7 ( 3 avg) % 116.11/116.35 % Maximal term depth : 3 ( 1 avg) % 116.11/116.35 % Number of predicates : 8 ( 7 usr; 0 prp; 1-4 aty) % 116.11/116.35 % Number of functors : 13 ( 13 usr; 5 con; 0-2 aty) % 116.11/116.35 % Number of variables : 49 ( 0 sgn) % 116.11/116.35 % SPC : CNF_UNS_RFO_SEQ_NHN % 116.11/116.35 % 116.11/116.35 % Comments : Created with tptp2X -f tptp -t clausify:otter MGT034+2.p % 116.11/116.35 %-------------------------------------------------------------------------- % 116.11/116.35 cnf(mp1_high_growth_rates_33,axiom, % 116.11/116.35 ( ~ environment(A) % 116.11/116.35 | ~ subpopulations(B,C,A,D) % 116.11/116.35 | ~ greater(growth_rate(C,D),growth_rate(B,D)) % 116.11/116.35 | selection_favors(C,B,D) ) ). % 116.11/116.35 % 116.11/116.35 cnf(l3_34,axiom, % 116.11/116.35 ( ~ environment(A) % 116.11/116.35 | ~ subpopulations(first_movers,efficient_producers,A,B) % 116.11/116.35 | ~ decreases(difference(disbanding_rate(first_movers,B),disbanding_rate(efficient_producers,B))) ) ). % 116.11/116.35 % 116.11/116.35 cnf(mp_critical_point_means_FM_and_EP_35,axiom, % 116.11/116.35 ( ~ environment(A) % 116.11/116.35 | ~ in_environment(A,critical_point(A)) % 116.11/116.35 | subpopulations(first_movers,efficient_producers,A,critical_point(A)) ) ). % 116.11/116.35 % 116.11/116.35 cnf(mp_FM_and_EP_when_EP_appears_36,axiom, % 116.11/116.35 ( ~ environment(A) % 116.11/116.35 | ~ in_environment(A,appear(efficient_producers,A)) % 116.11/116.35 | subpopulations(first_movers,efficient_producers,A,appear(efficient_producers,A)) ) ). % 116.11/116.35 % 116.11/116.35 cnf(mp_difference_between_founding_rates_37,axiom, % 116.11/116.35 ( ~ decreases(difference(founding_rate(first_movers,A),founding_rate(efficient_producers,A))) % 116.11/116.35 | decreases(difference(disbanding_rate(first_movers,A),disbanding_rate(efficient_producers,A))) % 116.11/116.35 | decreases(difference(growth_rate(first_movers,A),growth_rate(efficient_producers,A))) ) ). % 116.11/116.35 % 116.11/116.35 cnf(mp_decreasing_function_38,axiom, % 116.11/116.35 ( ~ environment(A) % 116.11/116.35 | ~ in_environment(A,B) % 116.11/116.35 | ~ greater_or_equal(difference(growth_rate(first_movers,B),growth_rate(efficient_producers,B)),zero) % 116.11/116.35 | ~ greater_or_equal(C,appear(efficient_producers,A)) % 116.11/116.35 | ~ greater(B,C) % 116.11/116.35 | ~ decreases(difference(growth_rate(first_movers,C),growth_rate(efficient_producers,C))) % 116.11/116.35 | greater(difference(growth_rate(first_movers,C),growth_rate(efficient_producers,C)),zero) ) ). % 116.11/116.35 % 116.11/116.35 cnf(mp_negative_growth_rate_difference_39,axiom, % 116.11/116.35 ( ~ greater(zero,difference(growth_rate(first_movers,A),growth_rate(efficient_producers,A))) % 116.11/116.35 | greater(growth_rate(efficient_producers,A),growth_rate(first_movers,A)) ) ). % 116.11/116.35 % 116.11/116.35 cnf(mp_negative_growth_rate_difference_40,axiom, % 116.11/116.35 ( ~ greater(growth_rate(efficient_producers,A),growth_rate(first_movers,A)) % 116.11/116.35 | greater(zero,difference(growth_rate(first_movers,A),growth_rate(efficient_producers,A))) ) ). % 116.11/116.35 % 116.11/116.35 cnf(mp_positive_growth_rate_difference_41,axiom, % 116.11/116.35 ( ~ greater(difference(growth_rate(first_movers,A),growth_rate(efficient_producers,A)),zero) % 116.11/116.35 | greater(growth_rate(first_movers,A),growth_rate(efficient_producers,A)) ) ). % 116.11/116.35 % 116.11/116.35 cnf(mp_positive_growth_rate_difference_42,axiom, % 116.11/116.35 ( ~ greater(growth_rate(first_movers,A),growth_rate(efficient_producers,A)) % 116.11/116.35 | greater(difference(growth_rate(first_movers,A),growth_rate(efficient_producers,A)),zero) ) ). % 116.11/116.35 % 116.11/116.35 cnf(mp_durations_are_time_intervals_43,axiom, % 116.11/116.35 ( ~ environment(A) % 116.11/116.35 | ~ in_environment(A,B) % 116.11/116.35 | ~ in_environment(A,C) % 116.11/116.35 | ~ greater_or_equal(C,D) % 116.11/116.35 | ~ greater_or_equal(D,B) % 116.11/116.35 | in_environment(A,D) ) ). % 116.11/116.35 % 116.11/116.35 cnf(mp_opening_time_in_duration_44,axiom, % 116.11/116.35 ( ~ environment(A) % 116.11/116.35 | in_environment(A,start_time(A)) ) ). % 116.11/116.35 % 116.11/116.35 cnf(mp_no_FM_before_opening_45,axiom, % 116.11/116.35 ( ~ environment(A) % 116.11/116.35 | greater_or_equal(appear(first_movers,A),start_time(A)) ) ). % 116.11/116.35 % 116.11/116.35 cnf(mp_critical_time_points_46,axiom, % 116.11/116.35 ( ~ environment(A) % 116.11/116.35 | ~ in_environment(A,critical_point(A)) % 116.11/116.35 | ~ greater_or_equal(B,appear(efficient_producers,A)) % 116.11/116.35 | ~ greater(critical_point(A),B) % 116.11/116.35 | in_environment(A,B) ) ). % 116.11/116.35 % 116.11/116.35 cnf(mp_contains_FM_and_EP_47,axiom, % 116.11/116.35 ( ~ environment(A) % 116.11/116.35 | ~ in_environment(A,B) % 116.11/116.35 | ~ greater(cardinality_at_time(first_movers,B),zero) % 116.11/116.35 | ~ greater(cardinality_at_time(efficient_producers,B),zero) % 116.11/116.35 | subpopulations(first_movers,efficient_producers,A,B) ) ). % 116.11/116.35 % 116.11/116.35 cnf(mp_symmetry_of_subpopulations_48,axiom, % 116.11/116.35 ( ~ environment(A) % 116.11/116.35 | ~ subpopulations(first_movers,efficient_producers,A,B) % 116.11/116.35 | subpopulations(efficient_producers,first_movers,A,B) ) ). % 116.11/116.35 % 116.11/116.35 cnf(mp_FM_and_EP_members_EP_appeared_49,axiom, % 116.11/116.35 ( ~ environment(A) % 116.11/116.35 | ~ subpopulations(first_movers,efficient_producers,A,B) % 116.11/116.35 | greater_or_equal(B,appear(efficient_producers,A)) ) ). % 116.11/116.35 % 116.11/116.35 cnf(mp_greater_or_equal_50,axiom, % 116.11/116.35 ( ~ greater_or_equal(A,B) % 116.11/116.35 | greater(A,B) % 116.11/116.35 | A = B ) ). % 116.11/116.35 % 116.11/116.35 cnf(mp_greater_or_equal_51,axiom, % 116.11/116.35 ( ~ greater(A,B) % 116.11/116.35 | greater_or_equal(A,B) ) ). % 116.11/116.35 % 116.11/116.35 cnf(mp_greater_or_equal_52,axiom, % 116.11/116.35 ( A != B % 116.11/116.35 | greater_or_equal(A,B) ) ). % 116.11/116.35 % 116.11/116.35 cnf(mp_relationship_of_growth_rates_53,axiom, % 116.11/116.35 ( ~ environment(A) % 116.11/116.35 | ~ subpopulations(first_movers,efficient_producers,A,B) % 116.11/116.35 | greater(zero,difference(growth_rate(first_movers,B),growth_rate(efficient_producers,B))) % 116.11/116.35 | greater_or_equal(difference(growth_rate(first_movers,B),growth_rate(efficient_producers,B)),zero) ) ). % 116.11/116.35 % 116.11/116.35 cnf(d1_54,hypothesis, % 116.11/116.35 ( ~ environment(A) % 116.11/116.35 | B != critical_point(A) % 116.11/116.35 | ~ greater(growth_rate(efficient_producers,B),growth_rate(first_movers,B)) ) ). % 116.11/116.35 % 116.11/116.35 cnf(d1_55,hypothesis, % 116.11/116.35 ( ~ environment(A) % 116.11/116.35 | B != critical_point(A) % 116.11/116.35 | ~ subpopulations(first_movers,efficient_producers,A,C) % 116.11/116.35 | ~ greater(C,B) % 116.11/116.35 | greater(growth_rate(efficient_producers,C),growth_rate(first_movers,C)) ) ). % 116.11/116.35 % 116.11/116.35 cnf(a10_56,hypothesis, % 116.11/116.35 ( ~ environment(A) % 116.11/116.35 | ~ subpopulations(first_movers,efficient_producers,A,B) % 116.11/116.35 | ~ subpopulations(first_movers,efficient_producers,A,C) % 116.11/116.35 | ~ greater_or_equal(D,B) % 116.11/116.35 | ~ greater_or_equal(C,D) % 116.11/116.35 | subpopulations(first_movers,efficient_producers,A,D) ) ). % 116.11/116.35 % 116.11/116.35 cnf(a12_57,hypothesis, % 116.11/116.35 ( ~ environment(A) % 116.11/116.35 | ~ subpopulations(first_movers,efficient_producers,A,B) % 116.11/116.35 | decreases(difference(founding_rate(first_movers,B),founding_rate(efficient_producers,B))) ) ). % 116.11/116.35 % 116.11/116.35 cnf(prove_t3_58,negated_conjecture, % 116.11/116.35 environment(sk1) ). % 116.11/116.35 % 116.11/116.35 cnf(prove_t3_59,negated_conjecture, % 116.11/116.35 in_environment(sk1,critical_point(sk1)) ). % 116.11/116.35 % 116.11/116.35 cnf(prove_t3_60,negated_conjecture, % 116.11/116.35 greater_or_equal(sk2,appear(efficient_producers,sk1)) ). % 116.11/116.35 % 116.11/116.35 cnf(prove_t3_61,negated_conjecture, % 116.11/116.35 greater(critical_point(sk1),sk2) ). % 116.11/116.35 % 116.11/116.35 cnf(prove_t3_62,negated_conjecture, % 116.11/116.35 ~ selection_favors(first_movers,efficient_producers,sk2) ). % 116.11/116.35 % 116.11/116.35 %-------------------------------------------------------------------------- % 116.11/116.35 %------------------------------------------- % 116.11/116.35 % Proof found % 116.11/116.35 % SZS status Theorem for theBenchmark % 116.11/116.35 % SZS output start Proof % 116.11/116.35 %ClaNum:62(EqnAxiom:32) % 116.11/116.35 %VarNum:156(SingletonVarNum:49) % 116.11/116.35 %MaxLitNum:7 % 116.11/116.35 %MaxfuncDepth:2 % 116.11/116.35 %SharedTerms:12 % 116.11/116.35 %goalClause: 33 34 35 36 37 % 116.11/116.36 %singleGoalClaCount:5 % 116.11/116.36 [33]P1(a1) % 116.11/116.36 [37]~P6(a8,a5,a11) % 116.11/116.36 [34]P3(a1,f2(a1)) % 116.11/116.36 [35]P4(f2(a1),a11) % 116.11/116.36 [36]P5(a11,f3(a5,a1)) % 116.11/116.36 [39]~P1(x391)+P3(x391,f12(x391)) % 116.11/116.36 [42]~P1(x421)+P5(f3(a8,x421),f12(x421)) % 116.11/116.36 [46]~P4(f9(a5,x461),f9(a8,x461))+P4(a13,f6(f9(a8,x461),f9(a5,x461))) % 116.11/116.36 [47]~P4(f9(a8,x471),f9(a5,x471))+P4(f6(f9(a8,x471),f9(a5,x471)),a13) % 116.11/116.36 [48]P4(f9(a5,x481),f9(a8,x481))+~P4(a13,f6(f9(a8,x481),f9(a5,x481))) % 116.11/116.36 [49]P4(f9(a8,x491),f9(a5,x491))+~P4(f6(f9(a8,x491),f9(a5,x491)),a13) % 116.11/116.36 [38]~E(x381,x382)+P5(x381,x382) % 116.11/116.36 [40]~P4(x401,x402)+P5(x401,x402) % 116.11/116.36 [50]~P1(x501)+~P3(x501,f2(x501))+P7(a8,a5,x501,f2(x501)) % 116.11/116.36 [51]~P1(x511)+~P3(x511,f3(a5,x511))+P7(a8,a5,x511,f3(a5,x511)) % 116.11/116.36 [54]P2(f6(f7(a8,x541),f7(a5,x541)))+~P2(f6(f10(a8,x541),f10(a5,x541)))+P2(f6(f9(a8,x541),f9(a5,x541))) % 116.11/116.36 [41]P4(x411,x412)+~P5(x411,x412)+E(x411,x412) % 116.11/116.36 [59]~P1(x591)+~P7(a8,a5,x591,x592)+P7(a5,a8,x591,x592) % 116.11/116.36 [43]~P1(x432)+~E(x431,f2(x432))+~P4(f9(a5,x431),f9(a8,x431)) % 116.11/116.36 [53]~P1(x532)+~P7(a8,a5,x532,x531)+P5(x531,f3(a5,x532)) % 116.11/116.36 [56]~P1(x562)+~P7(a8,a5,x562,x561)+P2(f6(f10(a8,x561),f10(a5,x561))) % 116.11/116.36 [58]~P1(x581)+~P7(a8,a5,x581,x582)+~P2(f6(f7(a8,x582),f7(a5,x582))) % 116.11/116.36 [61]~P1(x612)+~P7(a8,a5,x612,x611)+P5(f6(f9(a8,x611),f9(a5,x611)),a13)+P4(a13,f6(f9(a8,x611),f9(a5,x611))) % 116.11/116.36 [57]~P7(x572,x571,x574,x573)+P6(x571,x572,x573)+~P1(x574)+~P4(f9(x571,x573),f9(x572,x573)) % 116.11/116.36 [45]~P1(x451)+P3(x451,x452)+~P3(x451,f2(x451))+~P4(f2(x451),x452)+~P5(x452,f3(a5,x451)) % 116.11/116.36 [52]~P1(x521)+~P3(x521,x522)+P7(a8,a5,x521,x522)+~P4(f4(a8,x522),a13)+~P4(f4(a5,x522),a13) % 116.11/116.36 [55]~P1(x553)+~P4(x551,x552)+~P7(a8,a5,x553,x551)+~E(x552,f2(x553))+P4(f9(a5,x551),f9(a8,x551)) % 116.11/116.36 [44]~P1(x441)+~P5(x442,x444)+~P5(x443,x442)+P3(x441,x442)+~P3(x441,x443)+~P3(x441,x444) % 116.11/116.36 [62]~P1(x621)+~P5(x622,x623)+~P5(x624,x622)+~P7(a8,a5,x621,x624)+~P7(a8,a5,x621,x623)+P7(a8,a5,x621,x622) % 116.11/116.36 [60]~P3(x602,x603)+~P4(x603,x601)+~P1(x602)+~P5(x601,f3(a5,x602))+~P5(f6(f9(a8,x603),f9(a5,x603)),a13)+P4(f6(f9(a8,x601),f9(a5,x601)),a13)+~P2(f6(f9(a8,x601),f9(a5,x601))) % 116.11/116.36 %EqnAxiom % 116.11/116.36 [1]E(x11,x11) % 116.11/116.36 [2]E(x22,x21)+~E(x21,x22) % 116.11/116.36 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 116.11/116.36 [4]~E(x41,x42)+E(f2(x41),f2(x42)) % 116.11/116.36 [5]~E(x51,x52)+E(f6(x51,x53),f6(x52,x53)) % 116.11/116.36 [6]~E(x61,x62)+E(f6(x63,x61),f6(x63,x62)) % 116.11/116.36 [7]~E(x71,x72)+E(f3(x71,x73),f3(x72,x73)) % 116.11/116.36 [8]~E(x81,x82)+E(f3(x83,x81),f3(x83,x82)) % 116.11/116.36 [9]~E(x91,x92)+E(f12(x91),f12(x92)) % 116.11/116.36 [10]~E(x101,x102)+E(f9(x101,x103),f9(x102,x103)) % 116.11/116.36 [11]~E(x111,x112)+E(f9(x113,x111),f9(x113,x112)) % 116.11/116.36 [12]~E(x121,x122)+E(f7(x121,x123),f7(x122,x123)) % 116.11/116.36 [13]~E(x131,x132)+E(f7(x133,x131),f7(x133,x132)) % 116.11/116.36 [14]~E(x141,x142)+E(f10(x141,x143),f10(x142,x143)) % 116.11/116.36 [15]~E(x151,x152)+E(f10(x153,x151),f10(x153,x152)) % 116.11/116.36 [16]~E(x161,x162)+E(f4(x161,x163),f4(x162,x163)) % 116.11/116.36 [17]~E(x171,x172)+E(f4(x173,x171),f4(x173,x172)) % 116.11/116.36 [18]~P1(x181)+P1(x182)+~E(x181,x182) % 116.11/116.36 [19]P3(x192,x193)+~E(x191,x192)+~P3(x191,x193) % 116.11/116.36 [20]P3(x203,x202)+~E(x201,x202)+~P3(x203,x201) % 116.11/116.36 [21]P4(x212,x213)+~E(x211,x212)+~P4(x211,x213) % 116.11/116.36 [22]P4(x223,x222)+~E(x221,x222)+~P4(x223,x221) % 116.11/116.36 [23]P5(x232,x233)+~E(x231,x232)+~P5(x231,x233) % 116.11/116.36 [24]P5(x243,x242)+~E(x241,x242)+~P5(x243,x241) % 116.11/116.36 [25]P6(x252,x253,x254)+~E(x251,x252)+~P6(x251,x253,x254) % 116.11/116.36 [26]P6(x263,x262,x264)+~E(x261,x262)+~P6(x263,x261,x264) % 116.11/116.36 [27]P6(x273,x274,x272)+~E(x271,x272)+~P6(x273,x274,x271) % 116.11/116.36 [28]P7(x282,x283,x284,x285)+~E(x281,x282)+~P7(x281,x283,x284,x285) % 116.11/116.36 [29]P7(x293,x292,x294,x295)+~E(x291,x292)+~P7(x293,x291,x294,x295) % 116.11/116.36 [30]P7(x303,x304,x302,x305)+~E(x301,x302)+~P7(x303,x304,x301,x305) % 116.11/116.36 [31]P7(x313,x314,x315,x312)+~E(x311,x312)+~P7(x313,x314,x315,x311) % 116.11/116.36 [32]~P2(x321)+P2(x322)+~E(x321,x322) % 116.11/116.36 % 116.11/116.36 %------------------------------------------- % 116.11/116.36 cnf(63,plain, % 116.11/116.36 (P5(x631,x631)), % 116.11/116.36 inference(equality_inference,[],[38])). % 116.11/116.36 cnf(64,plain, % 116.11/116.36 (~P1(x641)+~P4(f9(a5,f2(x641)),f9(a8,f2(x641)))), % 116.11/116.36 inference(equality_inference,[],[43])). % 116.11/116.36 cnf(65,plain, % 116.11/116.36 (~P1(x651)+~P4(x652,f2(x651))+~P7(a8,a5,x651,x652)+P4(f9(a5,x652),f9(a8,x652))), % 116.11/116.36 inference(equality_inference,[],[55])). % 116.11/116.36 cnf(66,plain, % 116.11/116.36 (P3(a1,a11)), % 116.11/116.36 inference(scs_inference,[],[33,34,35,36,45])). % 116.11/116.36 cnf(68,plain, % 116.11/116.36 (P3(x681,f2(a1))+~E(a1,x681)), % 116.11/116.36 inference(scs_inference,[],[33,34,35,36,45,19])). % 116.11/116.36 cnf(87,plain, % 116.11/116.36 (P3(a1,f3(a5,a1))+~P4(f2(a1),f3(a5,a1))), % 116.11/116.36 inference(scs_inference,[],[33,36,34,66,63,19,24,23,20,45])). % 116.11/116.36 cnf(94,plain, % 116.11/116.36 (P5(x941,x942)+~E(x942,x941)), % 116.11/116.36 inference(scs_inference,[],[63,23])). % 116.11/116.36 cnf(142,plain, % 116.11/116.36 (~E(a1,x1421)+~P4(f9(a5,f2(x1421)),f9(a8,f2(x1421)))), % 116.11/116.36 inference(scs_inference,[],[33,64,18])). % 116.11/116.36 cnf(143,plain, % 116.11/116.36 (~P4(f9(a5,f2(a1)),f9(a8,f2(a1)))), % 116.11/116.36 inference(equality_inference,[],[142])). % 116.11/116.36 cnf(149,plain, % 116.11/116.36 (~P5(f2(a1),f3(a5,a1))+E(f2(a1),f3(a5,a1))+P3(a1,f3(a5,a1))), % 116.11/116.36 inference(scs_inference,[],[87,41])). % 116.11/116.36 cnf(164,plain, % 116.11/116.36 (~E(a1,x1641)+~P7(a8,a5,x1641,x1642)+P5(x1642,f3(a5,x1641))), % 116.11/116.36 inference(scs_inference,[],[33,53,18])). % 116.11/116.36 cnf(165,plain, % 116.11/116.36 (P5(x1651,f3(a5,a1))+~P7(a8,a5,a1,x1651)), % 116.11/116.36 inference(equality_inference,[],[164])). % 116.11/116.36 cnf(167,plain, % 116.11/116.36 (~E(a1,x1671)+P7(a5,a8,x1671,x1672)+~P7(a8,a5,x1671,x1672)), % 116.11/116.36 inference(scs_inference,[],[33,59,18])). % 116.11/116.36 cnf(168,plain, % 116.11/116.36 (~P7(a8,a5,a1,x1681)+P7(a5,a8,a1,x1681)), % 116.11/116.36 inference(equality_inference,[],[167])). % 116.11/116.36 cnf(169,plain, % 116.11/116.36 (~P4(f9(a8,a11),f9(a5,a11))+~P7(a8,a5,a1,a11)), % 116.11/116.36 inference(scs_inference,[],[37,33,168,57])). % 116.11/116.36 cnf(170,plain, % 116.11/116.36 (~P7(a8,a5,a1,a11)+~P4(f6(f9(a8,a11),f9(a5,a11)),a13)), % 116.11/116.36 inference(scs_inference,[],[169,49])). % 116.11/116.36 cnf(177,plain, % 116.11/116.36 (P7(a5,a8,a1,x1771)+~E(x1772,x1771)+~P7(a8,a5,a1,x1772)), % 116.11/116.36 inference(scs_inference,[],[33,31,59])). % 116.11/116.36 cnf(179,plain, % 116.11/116.36 (~E(a1,x1791)+~P3(x1791,f3(a5,x1791))+P7(a8,a5,x1791,f3(a5,x1791))), % 116.11/116.36 inference(scs_inference,[],[33,51,18])). % 116.11/116.36 cnf(180,plain, % 116.11/116.36 (~P3(a1,f3(a5,a1))+P7(a8,a5,a1,f3(a5,a1))), % 116.11/116.36 inference(equality_inference,[],[179])). % 116.11/116.36 cnf(184,plain, % 116.11/116.36 (~E(a1,x1841)+~P7(a8,a5,x1841,x1842)+P2(f6(f10(a8,x1842),f10(a5,x1842)))), % 116.11/116.36 inference(scs_inference,[],[33,56,18])). % 116.11/116.36 cnf(185,plain, % 116.11/116.36 (P2(f6(f10(a8,x1851),f10(a5,x1851)))+~P7(a8,a5,a1,x1851)), % 116.11/116.36 inference(equality_inference,[],[184])). % 116.11/116.36 cnf(186,plain, % 116.11/116.36 (~E(f6(f10(a8,x1861),f10(a5,x1861)),x1862)+P2(x1862)+~P7(a8,a5,a1,x1861)), % 116.11/116.36 inference(scs_inference,[],[185,32])). % 116.11/116.36 cnf(188,plain, % 116.11/116.36 (~E(a1,x1881)+~P7(a8,a5,x1881,x1882)+~P2(f6(f7(a8,x1882),f7(a5,x1882)))), % 116.11/116.36 inference(scs_inference,[],[33,58,18])). % 116.11/116.36 cnf(189,plain, % 116.11/116.36 (~P2(f6(f7(a8,x1891),f7(a5,x1891)))+~P7(a8,a5,a1,x1891)), % 116.11/116.36 inference(equality_inference,[],[188])). % 116.11/116.36 cnf(190,plain, % 116.11/116.36 (~P7(a8,a5,a1,x1901)+~P2(f6(f10(a8,x1901),f10(a5,x1901)))+P2(f6(f9(a8,x1901),f9(a5,x1901)))), % 116.11/116.36 inference(scs_inference,[],[189,54])). % 116.11/116.36 cnf(198,plain, % 116.11/116.36 (P2(f6(f9(a8,x1981),f9(a5,x1981)))+~P7(a8,a5,a1,x1981)), % 116.11/116.36 inference(scs_inference,[],[33,190,56])). % 116.11/116.36 cnf(199,plain, % 116.11/116.36 (~E(f6(f9(a8,x1991),f9(a5,x1991)),x1992)+P2(x1992)+~P7(a8,a5,a1,x1991)), % 116.11/116.36 inference(scs_inference,[],[198,32])). % 116.11/116.36 cnf(299,plain, % 116.11/116.36 (~E(x2991,a1)+P1(x2991)), % 116.11/116.36 inference(scs_inference,[],[33,2,18])). % 116.11/116.36 cnf(301,plain, % 116.11/116.36 (P7(a8,a5,a1,f2(a1))), % 116.11/116.36 inference(scs_inference,[],[34,299,50])). % 116.11/116.36 cnf(314,plain, % 116.11/116.36 (P3(a1,f3(a5,a1))), % 116.11/116.36 inference(scs_inference,[],[35,34,33,143,301,63,165,65,149,177,31,21,23,20])). % 116.11/116.36 cnf(317,plain, % 116.11/116.36 (P7(a8,a5,a1,f3(a5,a1))), % 116.11/116.36 inference(scs_inference,[],[314,180])). % 116.11/116.36 cnf(606,plain, % 116.11/116.36 (P7(a8,a5,a1,a11)), % 116.11/116.36 inference(scs_inference,[],[35,301,317,33,36,40,62])). % 116.11/116.36 cnf(608,plain, % 116.11/116.36 (~P4(f6(f9(a8,a11),f9(a5,a11)),a13)), % 116.11/116.36 inference(scs_inference,[],[606,170])). % 116.11/116.36 cnf(612,plain, % 116.11/116.36 (P2(f6(f9(a8,a11),f9(a5,a11)))), % 116.11/116.36 inference(scs_inference,[],[606,185,198])). % 116.11/116.36 cnf(614,plain, % 116.11/116.36 (~P2(f6(f7(a8,a11),f7(a5,a11)))), % 116.11/116.36 inference(scs_inference,[],[606,185,198,189])). % 116.11/116.36 cnf(618,plain, % 116.11/116.36 (~E(f6(f10(a8,a11),f10(a5,a11)),f6(f7(a8,a11),f7(a5,a11)))), % 116.11/116.36 inference(scs_inference,[],[606,185,198,189,199,186])). % 116.11/116.36 cnf(702,plain, % 116.11/116.36 (~E(a13,f6(f9(a8,f2(a1)),f9(a5,f2(a1))))), % 116.11/116.36 inference(scs_inference,[],[612,608,36,33,34,35,94,60])). % 116.11/116.36 cnf(704,plain, % 116.11/116.36 (~P5(f6(f9(a8,f2(a1)),f9(a5,f2(a1))),a13)), % 116.11/116.36 inference(scs_inference,[],[612,608,36,33,35,68,60])). % 116.11/116.36 cnf(2006,plain, % 116.11/116.36 ($false), % 116.11/116.36 inference(scs_inference,[],[618,704,702,614,143,301,33,48,2,56,58,41,199,32,186,61]), % 116.11/116.36 ['proof']). % 116.11/116.36 % SZS output end Proof % 116.11/116.36 % Total time :115.741414s %------------------------------------------------------------------------------