%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : MGT034+2 : TPTP v9.3.0. Released v2.0.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % Computer : n005.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 : Theorem 116.07s 116.19s % 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.0.0. % 0.00/0.03 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.07/0.32 % Computer : n005.cluster.edu % 0.07/0.32 % Model : x86_64 x86_64 % 0.07/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.07/0.32 % Memory : 8046.5625MB % 0.07/0.32 % OS : Linux 6.8.0-71-generic % 0.07/0.32 % CPULimit : 300 % 0.07/0.32 % WCLimit : 300 % 0.07/0.32 % DateTime : Mon Sep 7 12:31:35 UTC 2026 % 0.07/0.32 % CPUTime : % 0.24/0.48 start to proof:theBenchmark % 116.07/116.17 %------------------------------------------- % 116.07/116.17 % File :CSE---1.7 % 116.07/116.17 % Problem :theBenchmark % 116.07/116.17 % Transform :cnf % 116.07/116.17 % Format :tptp:raw % 116.07/116.17 % Command :java -jar mcs_scs.jar %d %s % 116.07/116.17 % 116.07/116.17 % Result :Theorem 115.703992s % 116.07/116.17 % Output :CNFRefutation 115.703992s % 116.07/116.17 %------------------------------------------- % 116.07/116.18 %-------------------------------------------------------------------------- % 116.07/116.18 % File : MGT034+2 : TPTP v9.3.0. Released v2.0.0. % 116.07/116.18 % Domain : Management (Organisation Theory) % 116.07/116.18 % Problem : Selection favors FMs above EPs until critical point reached % 116.07/116.18 % Version : [PM93] axioms. % 116.07/116.18 % English : Selection favors first movers above efficient producers past % 116.07/116.18 % the appearance of efficient producers until the critical % 116.07/116.18 % point is reached. % 116.07/116.18 % 116.07/116.18 % Refs : [PM93] Peli & Masuch (1993), The Logic of Propogation Strateg % 116.07/116.18 % : [PM94] Peli & Masuch (1994), The Logic of Propogation Strateg % 116.07/116.18 % : [PB+94] Peli et al. (1994), A Logical Approach to Formalizing % 116.07/116.18 % Source : [PM93] % 116.07/116.18 % Names : THEOREM 3 [PM93] % 116.07/116.18 % : T3 [PB+94] % 116.07/116.18 % 116.07/116.18 % Status : Theorem % 116.07/116.18 % Rating : 0.17 v9.3.0, 0.21 v9.0.0, 0.25 v8.2.0, 0.22 v8.1.0, 0.19 v7.5.0, 0.22 v7.4.0, 0.17 v7.3.0, 0.24 v7.2.0, 0.21 v7.1.0, 0.17 v6.4.0, 0.23 v6.3.0, 0.17 v6.2.0, 0.20 v6.1.0, 0.30 v6.0.0, 0.09 v5.5.0, 0.33 v5.4.0, 0.32 v5.3.0, 0.41 v5.2.0, 0.25 v5.1.0, 0.19 v5.0.0, 0.17 v4.1.0, 0.22 v4.0.1, 0.17 v3.7.0, 0.15 v3.5.0, 0.16 v3.4.0, 0.26 v3.3.0, 0.29 v3.2.0, 0.18 v3.1.0, 0.33 v2.6.0, 0.29 v2.5.0, 0.25 v2.4.0, 0.25 v2.3.0, 0.33 v2.2.1, 0.00 v2.1.0 % 116.07/116.18 % Syntax : Number of formulae : 21 ( 0 unt; 0 def) % 116.07/116.18 % Number of atoms : 80 ( 2 equ) % 116.07/116.18 % Maximal formula atoms : 7 ( 3 avg) % 116.07/116.18 % Number of connectives : 63 ( 4 ~; 1 |; 35 &) % 116.07/116.18 % ( 3 <=>; 20 =>; 0 <=; 0 <~>) % 116.07/116.18 % Maximal formula depth : 10 ( 6 avg) % 116.07/116.18 % Maximal term depth : 3 ( 1 avg) % 116.07/116.18 % Number of predicates : 8 ( 7 usr; 0 prp; 1-4 aty) % 116.07/116.18 % Number of functors : 11 ( 11 usr; 3 con; 0-2 aty) % 116.07/116.18 % Number of variables : 43 ( 43 !; 0 ?) % 116.07/116.18 % SPC : FOF_THM_RFO_SEQ % 116.07/116.18 % 116.07/116.18 % Comments : % 116.07/116.18 %-------------------------------------------------------------------------- % 116.07/116.18 %----Subsitution axioms % 116.07/116.18 %----Problem axioms % 116.07/116.18 %----MP1. Selection favors subpopulations with higher growth rates. % 116.07/116.18 fof(mp1_high_growth_rates,axiom, % 116.07/116.18 ! [E,S1,S2,T] : % 116.07/116.18 ( ( environment(E) % 116.07/116.18 & subpopulations(S1,S2,E,T) % 116.07/116.18 & greater(growth_rate(S2,T),growth_rate(S1,T)) ) % 116.07/116.18 => selection_favors(S2,S1,T) ) ). % 116.07/116.18 % 116.07/116.18 %----L3. The difference between the disbanding rates of first movers and % 116.07/116.18 %----efficient producers does not decrease. % 116.07/116.18 fof(l3,axiom, % 116.07/116.18 ! [E,T] : % 116.07/116.18 ( ( environment(E) % 116.07/116.18 & subpopulations(first_movers,efficient_producers,E,T) ) % 116.07/116.18 => ~ decreases(difference(disbanding_rate(first_movers,T),disbanding_rate(efficient_producers,T))) ) ). % 116.07/116.18 % 116.07/116.18 %----MP. If the environment contains a critical point, then FM and EP are % 116.07/116.18 %----present at this time. % 116.07/116.18 fof(mp_critical_point_means_FM_and_EP,axiom, % 116.07/116.18 ! [E] : % 116.07/116.18 ( ( environment(E) % 116.07/116.18 & in_environment(E,critical_point(E)) ) % 116.07/116.18 => subpopulations(first_movers,efficient_producers,E,critical_point(E)) ) ). % 116.07/116.18 % 116.07/116.18 %----MP. FM and EP are present when EP appear in the environment. % 116.07/116.18 fof(mp_FM_and_EP_when_EP_appears,axiom, % 116.07/116.18 ! [E] : % 116.07/116.18 ( ( environment(E) % 116.07/116.18 & in_environment(E,appear(efficient_producers,E)) ) % 116.07/116.18 => subpopulations(first_movers,efficient_producers,E,appear(efficient_producers,E)) ) ). % 116.07/116.18 % 116.07/116.18 %----MP. If the difference between the founding rates of FM and EP % 116.07/116.18 %----decreases and the difference between their disbanding rates does % 116.07/116.18 %----not decrease, then the difference between the growth rates decreases. % 116.07/116.18 fof(mp_difference_between_founding_rates,axiom, % 116.07/116.18 ! [T] : % 116.07/116.18 ( ( decreases(difference(founding_rate(first_movers,T),founding_rate(efficient_producers,T))) % 116.07/116.18 & ~ decreases(difference(disbanding_rate(first_movers,T),disbanding_rate(efficient_producers,T))) ) % 116.07/116.18 => decreases(difference(growth_rate(first_movers,T),growth_rate(efficient_producers,T))) ) ). % 116.07/116.18 % 116.07/116.18 %----MP. If function "f" is decreasing until to, and it is not negative at % 116.07/116.18 %----"to, then its value is positive before "to". % 116.07/116.18 %----INSTANTIATION: f(x) = (growth_rate(first_movers,x) - % 116.07/116.18 %----growth_rate(efficient_producers,x) % 116.07/116.18 fof(mp_decreasing_function,axiom, % 116.07/116.18 ! [E,T,To] : % 116.07/116.18 ( ( environment(E) % 116.07/116.18 & in_environment(E,To) % 116.07/116.18 & greater_or_equal(difference(growth_rate(first_movers,To),growth_rate(efficient_producers,To)),zero) % 116.07/116.18 & greater_or_equal(T,appear(efficient_producers,E)) % 116.07/116.18 & greater(To,T) ) % 116.07/116.18 => ( decreases(difference(growth_rate(first_movers,T),growth_rate(efficient_producers,T))) % 116.07/116.18 => greater(difference(growth_rate(first_movers,T),growth_rate(efficient_producers,T)),zero) ) ) ). % 116.07/116.18 % 116.07/116.18 %----MP. The difference between the growth rates of first movers and % 116.07/116.18 %----efficient producers is negative, if and only if, the growth rate of % 116.07/116.18 %----efficient producers is higher. % 116.07/116.18 fof(mp_negative_growth_rate_difference,axiom, % 116.07/116.18 ! [T] : % 116.07/116.18 ( greater(zero,difference(growth_rate(first_movers,T),growth_rate(efficient_producers,T))) % 116.07/116.18 <=> greater(growth_rate(efficient_producers,T),growth_rate(first_movers,T)) ) ). % 116.07/116.18 % 116.07/116.18 %----MP. The difference between the growth rates of first movers and % 116.07/116.18 %----efficient producers is positive, if and only if, the growth rate of % 116.07/116.18 %----first movers is higher. % 116.07/116.18 fof(mp_positive_growth_rate_difference,axiom, % 116.07/116.18 ! [T] : % 116.07/116.18 ( greater(difference(growth_rate(first_movers,T),growth_rate(efficient_producers,T)),zero) % 116.07/116.18 <=> greater(growth_rate(first_movers,T),growth_rate(efficient_producers,T)) ) ). % 116.07/116.18 % 116.07/116.18 %----MP. The durations of environments are time-intervals. % 116.07/116.18 fof(mp_durations_are_time_intervals,axiom, % 116.07/116.18 ! [E,T1,T2,T] : % 116.07/116.18 ( ( environment(E) % 116.07/116.18 & in_environment(E,T1) % 116.07/116.18 & in_environment(E,T2) % 116.07/116.18 & greater_or_equal(T2,T) % 116.07/116.18 & greater_or_equal(T,T1) ) % 116.07/116.18 => in_environment(E,T) ) ). % 116.07/116.18 % 116.07/116.18 %----MP. The opening time of the environment belongs to the environment's % 116.07/116.18 %----duration. % 116.07/116.18 fof(mp_opening_time_in_duration,axiom, % 116.07/116.18 ! [E] : % 116.07/116.18 ( environment(E) % 116.07/116.18 => in_environment(E,start_time(E)) ) ). % 116.07/116.18 % 116.07/116.18 %----MP. FM cannot appear in an environment before it opens. % 116.07/116.18 fof(mp_no_FM_before_opening,axiom, % 116.07/116.18 ! [E] : % 116.07/116.18 ( environment(E) % 116.07/116.18 => greater_or_equal(appear(first_movers,E),start_time(E)) ) ). % 116.07/116.18 % 116.07/116.18 %----MP. If the critical point occurs in the environment, then all the % 116.07/116.18 %----time-points between the appearence of efficient producers and the % 116.07/116.18 %----critical point occur in the environnment. % 116.07/116.18 fof(mp_critical_time_points,axiom, % 116.07/116.18 ! [E,T] : % 116.07/116.19 ( ( environment(E) % 116.07/116.19 & in_environment(E,critical_point(E)) % 116.07/116.19 & greater_or_equal(T,appear(efficient_producers,E)) % 116.07/116.19 & greater(critical_point(E),T) ) % 116.07/116.19 => in_environment(E,T) ) ). % 116.07/116.19 % 116.07/116.19 %----MP. If the number of both first movers and efficient producers is % 116.07/116.19 %----positive in an environment, then the population in this environment % 116.07/116.19 %----contains a first mover and an efficient producer subpopulation. % 116.07/116.19 fof(mp_contains_FM_and_EP,axiom, % 116.07/116.19 ! [E,T] : % 116.07/116.19 ( ( environment(E) % 116.07/116.19 & in_environment(E,T) % 116.07/116.19 & greater(cardinality_at_time(first_movers,T),zero) % 116.07/116.19 & greater(cardinality_at_time(efficient_producers,T),zero) ) % 116.07/116.19 => subpopulations(first_movers,efficient_producers,E,T) ) ). % 116.07/116.19 % 116.07/116.19 %----MP. The "subpopulation" predicate is symmetric: if FM and EP are % 116.07/116.19 %----non-empty subpopulations in E, then EP and FM are also non-empty % 116.07/116.19 %----subpopulations in E. % 116.07/116.19 fof(mp_symmetry_of_subpopulations,axiom, % 116.07/116.19 ! [E,T] : % 116.07/116.19 ( ( environment(E) % 116.07/116.19 & subpopulations(first_movers,efficient_producers,E,T) ) % 116.07/116.19 => subpopulations(efficient_producers,first_movers,E,T) ) ). % 116.07/116.19 % 116.07/116.19 %----MP. If FM and EP have members in an environment at a certain point of % 116.07/116.19 %----time, then EP's appearence time is already passed. % 116.07/116.19 fof(mp_FM_and_EP_members_EP_appeared,axiom, % 116.07/116.19 ! [E,T] : % 116.07/116.19 ( ( environment(E) % 116.07/116.19 & subpopulations(first_movers,efficient_producers,E,T) ) % 116.07/116.19 => greater_or_equal(T,appear(efficient_producers,E)) ) ). % 116.07/116.19 % 116.07/116.19 %----MP. on "greater or equal to" % 116.07/116.19 fof(mp_greater_or_equal,axiom, % 116.07/116.19 ! [X,Y] : % 116.07/116.19 ( greater_or_equal(X,Y) % 116.07/116.19 <=> ( greater(X,Y) % 116.07/116.19 | X = Y ) ) ). % 116.07/116.19 % 116.07/116.19 %----MP. on growth rates % 116.07/116.19 fof(mp_relationship_of_growth_rates,axiom, % 116.07/116.19 ! [E,T] : % 116.07/116.19 ( ( environment(E) % 116.07/116.19 & subpopulations(first_movers,efficient_producers,E,T) % 116.07/116.19 & ~ greater(zero,difference(growth_rate(first_movers,T),growth_rate(efficient_producers,T))) ) % 116.07/116.19 => greater_or_equal(difference(growth_rate(first_movers,T),growth_rate(efficient_producers,T)),zero) ) ). % 116.07/116.19 % 116.07/116.19 %----D1(<=). If a time-point is the critical point of the environment, then % 116.07/116.19 %----it is the earliest time past which the growth rate of efficient % 116.07/116.19 %----producers permanently exceeds growth rate of first movers. % 116.07/116.19 fof(d1,hypothesis, % 116.07/116.19 ! [E,Tc] : % 116.07/116.19 ( ( environment(E) % 116.07/116.19 & Tc = critical_point(E) ) % 116.07/116.19 => ( ~ greater(growth_rate(efficient_producers,Tc),growth_rate(first_movers,Tc)) % 116.07/116.19 & ! [T] : % 116.07/116.19 ( ( subpopulations(first_movers,efficient_producers,E,T) % 116.07/116.19 & greater(T,Tc) ) % 116.07/116.19 => greater(growth_rate(efficient_producers,T),growth_rate(first_movers,T)) ) ) ) ). % 116.07/116.19 % 116.07/116.19 %----A10. If FM and EP are present in the environment at time-points t1 % 116.07/116.19 %----and t2, then they are present during the time-interval between % 116.07/116.19 %----t1 and t2. % 116.07/116.19 fof(a10,hypothesis, % 116.07/116.19 ! [E,T1,T2,T] : % 116.07/116.19 ( ( environment(E) % 116.07/116.19 & subpopulations(first_movers,efficient_producers,E,T1) % 116.07/116.19 & subpopulations(first_movers,efficient_producers,E,T2) % 116.07/116.19 & greater_or_equal(T,T1) % 116.07/116.19 & greater_or_equal(T2,T) ) % 116.07/116.19 => subpopulations(first_movers,efficient_producers,E,T) ) ). % 116.07/116.19 % 116.07/116.19 %----A12. The difference between the founding rates of first movers and % 116.07/116.19 %----efficient producers decreases with time. % 116.07/116.19 fof(a12,hypothesis, % 116.07/116.19 ! [E,T] : % 116.07/116.19 ( ( environment(E) % 116.07/116.19 & subpopulations(first_movers,efficient_producers,E,T) ) % 116.07/116.19 => decreases(difference(founding_rate(first_movers,T),founding_rate(efficient_producers,T))) ) ). % 116.07/116.19 % 116.07/116.19 %----GOAL: T3. Selection favors first movers above efficient producers % 116.07/116.19 %----between the appearence of efficient producers and the critical point. % 116.07/116.19 fof(prove_t3,conjecture, % 116.07/116.19 ! [E,T] : % 116.07/116.19 ( ( environment(E) % 116.07/116.19 & in_environment(E,critical_point(E)) % 116.07/116.19 & greater_or_equal(T,appear(efficient_producers,E)) % 116.07/116.19 & greater(critical_point(E),T) ) % 116.07/116.19 => selection_favors(first_movers,efficient_producers,T) ) ). % 116.07/116.19 % 116.07/116.19 %-------------------------------------------------------------------------- % 116.07/116.19 %------------------------------------------- % 116.07/116.19 % Proof found % 116.07/116.19 % SZS status Theorem for theBenchmark % 116.07/116.19 % SZS output start Proof % 116.07/116.19 %ClaNum:62(EqnAxiom:32) % 116.07/116.19 %VarNum:156(SingletonVarNum:49) % 116.07/116.19 %MaxLitNum:7 % 116.07/116.19 %MaxfuncDepth:2 % 116.07/116.19 %SharedTerms:12 % 116.07/116.19 %goalClause: 33 34 35 36 37 % 116.07/116.19 %singleGoalClaCount:5 % 116.07/116.19 [33]P1(a1) % 116.07/116.19 [37]~P6(a9,a5,a8) % 116.07/116.19 [34]P3(a1,f2(a1)) % 116.07/116.19 [35]P4(f2(a1),a8) % 116.07/116.19 [36]P5(a8,f3(a5,a1)) % 116.07/116.19 [39]~P1(x391)+P3(x391,f10(x391)) % 116.07/116.19 [42]~P1(x421)+P5(f3(a9,x421),f10(x421)) % 116.07/116.19 [46]~P4(f11(a5,x461),f11(a9,x461))+P4(a13,f6(f11(a9,x461),f11(a5,x461))) % 116.07/116.19 [47]~P4(f11(a9,x471),f11(a5,x471))+P4(f6(f11(a9,x471),f11(a5,x471)),a13) % 116.07/116.19 [48]P4(f11(a5,x481),f11(a9,x481))+~P4(a13,f6(f11(a9,x481),f11(a5,x481))) % 116.07/116.19 [49]P4(f11(a9,x491),f11(a5,x491))+~P4(f6(f11(a9,x491),f11(a5,x491)),a13) % 116.07/116.19 [38]~E(x381,x382)+P5(x381,x382) % 116.07/116.19 [40]~P4(x401,x402)+P5(x401,x402) % 116.07/116.19 [50]~P1(x501)+~P3(x501,f2(x501))+P7(a9,a5,x501,f2(x501)) % 116.07/116.19 [51]~P1(x511)+~P3(x511,f3(a5,x511))+P7(a9,a5,x511,f3(a5,x511)) % 116.07/116.19 [54]P2(f6(f7(a9,x541),f7(a5,x541)))+~P2(f6(f12(a9,x541),f12(a5,x541)))+P2(f6(f11(a9,x541),f11(a5,x541))) % 116.07/116.19 [41]P4(x411,x412)+~P5(x411,x412)+E(x411,x412) % 116.07/116.19 [59]~P1(x591)+~P7(a9,a5,x591,x592)+P7(a5,a9,x591,x592) % 116.07/116.19 [43]~P1(x432)+~E(x431,f2(x432))+~P4(f11(a5,x431),f11(a9,x431)) % 116.07/116.19 [53]~P1(x532)+~P7(a9,a5,x532,x531)+P5(x531,f3(a5,x532)) % 116.07/116.19 [56]~P1(x562)+~P7(a9,a5,x562,x561)+P2(f6(f12(a9,x561),f12(a5,x561))) % 116.07/116.19 [58]~P1(x581)+~P7(a9,a5,x581,x582)+~P2(f6(f7(a9,x582),f7(a5,x582))) % 116.07/116.19 [61]~P1(x612)+~P7(a9,a5,x612,x611)+P5(f6(f11(a9,x611),f11(a5,x611)),a13)+P4(a13,f6(f11(a9,x611),f11(a5,x611))) % 116.07/116.19 [57]~P7(x572,x571,x574,x573)+P6(x571,x572,x573)+~P1(x574)+~P4(f11(x571,x573),f11(x572,x573)) % 116.07/116.19 [45]~P1(x451)+P3(x451,x452)+~P3(x451,f2(x451))+~P4(f2(x451),x452)+~P5(x452,f3(a5,x451)) % 116.07/116.19 [52]~P1(x521)+~P3(x521,x522)+P7(a9,a5,x521,x522)+~P4(f4(a9,x522),a13)+~P4(f4(a5,x522),a13) % 116.07/116.19 [55]~P1(x553)+~P4(x551,x552)+~P7(a9,a5,x553,x551)+~E(x552,f2(x553))+P4(f11(a5,x551),f11(a9,x551)) % 116.07/116.19 [44]~P1(x441)+~P5(x442,x444)+~P5(x443,x442)+P3(x441,x442)+~P3(x441,x443)+~P3(x441,x444) % 116.07/116.19 [62]~P1(x621)+~P5(x622,x623)+~P5(x624,x622)+~P7(a9,a5,x621,x624)+~P7(a9,a5,x621,x623)+P7(a9,a5,x621,x622) % 116.07/116.19 [60]~P3(x602,x603)+~P4(x603,x601)+~P1(x602)+~P5(x601,f3(a5,x602))+~P5(f6(f11(a9,x603),f11(a5,x603)),a13)+P4(f6(f11(a9,x601),f11(a5,x601)),a13)+~P2(f6(f11(a9,x601),f11(a5,x601))) % 116.07/116.19 %EqnAxiom % 116.07/116.19 [1]E(x11,x11) % 116.07/116.19 [2]E(x22,x21)+~E(x21,x22) % 116.07/116.19 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 116.07/116.19 [4]~E(x41,x42)+E(f2(x41),f2(x42)) % 116.07/116.19 [5]~E(x51,x52)+E(f6(x51,x53),f6(x52,x53)) % 116.07/116.19 [6]~E(x61,x62)+E(f6(x63,x61),f6(x63,x62)) % 116.07/116.19 [7]~E(x71,x72)+E(f3(x71,x73),f3(x72,x73)) % 116.07/116.19 [8]~E(x81,x82)+E(f3(x83,x81),f3(x83,x82)) % 116.07/116.19 [9]~E(x91,x92)+E(f10(x91),f10(x92)) % 116.07/116.19 [10]~E(x101,x102)+E(f11(x101,x103),f11(x102,x103)) % 116.07/116.19 [11]~E(x111,x112)+E(f11(x113,x111),f11(x113,x112)) % 116.07/116.19 [12]~E(x121,x122)+E(f7(x121,x123),f7(x122,x123)) % 116.07/116.19 [13]~E(x131,x132)+E(f7(x133,x131),f7(x133,x132)) % 116.07/116.19 [14]~E(x141,x142)+E(f12(x141,x143),f12(x142,x143)) % 116.07/116.19 [15]~E(x151,x152)+E(f12(x153,x151),f12(x153,x152)) % 116.07/116.19 [16]~E(x161,x162)+E(f4(x161,x163),f4(x162,x163)) % 116.07/116.19 [17]~E(x171,x172)+E(f4(x173,x171),f4(x173,x172)) % 116.07/116.19 [18]~P1(x181)+P1(x182)+~E(x181,x182) % 116.07/116.19 [19]P3(x192,x193)+~E(x191,x192)+~P3(x191,x193) % 116.07/116.19 [20]P3(x203,x202)+~E(x201,x202)+~P3(x203,x201) % 116.07/116.19 [21]P4(x212,x213)+~E(x211,x212)+~P4(x211,x213) % 116.07/116.19 [22]P4(x223,x222)+~E(x221,x222)+~P4(x223,x221) % 116.07/116.19 [23]P5(x232,x233)+~E(x231,x232)+~P5(x231,x233) % 116.07/116.19 [24]P5(x243,x242)+~E(x241,x242)+~P5(x243,x241) % 116.07/116.19 [25]P6(x252,x253,x254)+~E(x251,x252)+~P6(x251,x253,x254) % 116.07/116.19 [26]P6(x263,x262,x264)+~E(x261,x262)+~P6(x263,x261,x264) % 116.07/116.19 [27]P6(x273,x274,x272)+~E(x271,x272)+~P6(x273,x274,x271) % 116.07/116.19 [28]P7(x282,x283,x284,x285)+~E(x281,x282)+~P7(x281,x283,x284,x285) % 116.07/116.19 [29]P7(x293,x292,x294,x295)+~E(x291,x292)+~P7(x293,x291,x294,x295) % 116.07/116.19 [30]P7(x303,x304,x302,x305)+~E(x301,x302)+~P7(x303,x304,x301,x305) % 116.07/116.19 [31]P7(x313,x314,x315,x312)+~E(x311,x312)+~P7(x313,x314,x315,x311) % 116.07/116.19 [32]~P2(x321)+P2(x322)+~E(x321,x322) % 116.07/116.19 % 116.07/116.19 %------------------------------------------- % 116.07/116.19 cnf(63,plain, % 116.07/116.19 (P5(x631,x631)), % 116.07/116.19 inference(equality_inference,[],[38])). % 116.07/116.19 cnf(64,plain, % 116.07/116.19 (~P1(x641)+~P4(f11(a5,f2(x641)),f11(a9,f2(x641)))), % 116.07/116.19 inference(equality_inference,[],[43])). % 116.07/116.19 cnf(68,plain, % 116.07/116.19 (P3(x681,f2(a1))+~E(a1,x681)), % 116.07/116.19 inference(scs_inference,[],[33,34,35,36,45,19])). % 116.07/116.19 cnf(88,plain, % 116.07/116.19 (P5(x881,x882)+~E(x882,x881)), % 116.07/116.19 inference(scs_inference,[],[63,23])). % 116.07/116.19 cnf(92,plain, % 116.07/116.19 (P3(a1,f3(a5,a1))+~P4(f2(a1),f3(a5,a1))), % 116.07/116.19 inference(scs_inference,[],[33,34,63,45])). % 116.07/116.19 cnf(134,plain, % 116.07/116.19 (~E(a1,x1341)+~P4(f11(a5,f2(x1341)),f11(a9,f2(x1341)))), % 116.07/116.19 inference(scs_inference,[],[33,64,18])). % 116.07/116.19 cnf(135,plain, % 116.07/116.19 (~P4(f11(a5,f2(a1)),f11(a9,f2(a1)))), % 116.07/116.19 inference(equality_inference,[],[134])). % 116.07/116.19 cnf(141,plain, % 116.07/116.19 (~P4(f2(a1),f3(a5,a1))+P7(a9,a5,a1,f3(a5,a1))), % 116.07/116.19 inference(scs_inference,[],[33,92,51])). % 116.07/116.19 cnf(160,plain, % 116.07/116.19 (~E(a1,x1601)+~P7(a9,a5,x1601,x1602)+P5(x1602,f3(a5,x1601))), % 116.07/116.19 inference(scs_inference,[],[33,53,18])). % 116.07/116.19 cnf(161,plain, % 116.07/116.19 (P5(x1611,f3(a5,a1))+~P7(a9,a5,a1,x1611)), % 116.07/116.19 inference(equality_inference,[],[160])). % 116.07/116.19 cnf(163,plain, % 116.07/116.19 (~E(a1,x1631)+P7(a5,a9,x1631,x1632)+~P7(a9,a5,x1631,x1632)), % 116.07/116.19 inference(scs_inference,[],[33,59,18])). % 116.07/116.19 cnf(164,plain, % 116.07/116.19 (~P7(a9,a5,a1,x1641)+P7(a5,a9,a1,x1641)), % 116.07/116.19 inference(equality_inference,[],[163])). % 116.07/116.19 cnf(165,plain, % 116.07/116.19 (~P4(f11(a9,a8),f11(a5,a8))+~P7(a9,a5,a1,a8)), % 116.07/116.19 inference(scs_inference,[],[37,33,164,57])). % 116.07/116.19 cnf(166,plain, % 116.07/116.19 (~P7(a9,a5,a1,a8)+~P4(f6(f11(a9,a8),f11(a5,a8)),a13)), % 116.07/116.19 inference(scs_inference,[],[165,49])). % 116.07/116.20 cnf(175,plain, % 116.07/116.20 (~E(a1,x1751)+~P7(a9,a5,x1751,x1752)+P2(f6(f12(a9,x1752),f12(a5,x1752)))), % 116.07/116.20 inference(scs_inference,[],[33,56,18])). % 116.07/116.20 cnf(176,plain, % 116.07/116.20 (P2(f6(f12(a9,x1761),f12(a5,x1761)))+~P7(a9,a5,a1,x1761)), % 116.07/116.20 inference(equality_inference,[],[175])). % 116.07/116.20 cnf(177,plain, % 116.07/116.20 (~E(f6(f12(a9,x1771),f12(a5,x1771)),x1772)+P2(x1772)+~P7(a9,a5,a1,x1771)), % 116.07/116.20 inference(scs_inference,[],[176,32])). % 116.07/116.20 cnf(179,plain, % 116.07/116.20 (~E(a1,x1791)+~P7(a9,a5,x1791,x1792)+~P2(f6(f7(a9,x1792),f7(a5,x1792)))), % 116.07/116.20 inference(scs_inference,[],[33,58,18])). % 116.07/116.20 cnf(180,plain, % 116.07/116.20 (~P2(f6(f7(a9,x1801),f7(a5,x1801)))+~P7(a9,a5,a1,x1801)), % 116.07/116.20 inference(equality_inference,[],[179])). % 116.07/116.20 cnf(181,plain, % 116.07/116.20 (~P7(a9,a5,a1,x1811)+~P2(f6(f12(a9,x1811),f12(a5,x1811)))+P2(f6(f11(a9,x1811),f11(a5,x1811)))), % 116.07/116.20 inference(scs_inference,[],[180,54])). % 116.07/116.20 cnf(190,plain, % 116.07/116.20 (P2(f6(f11(a9,x1901),f11(a5,x1901)))+~P7(a9,a5,a1,x1901)), % 116.07/116.20 inference(scs_inference,[],[33,181,56])). % 116.07/116.20 cnf(191,plain, % 116.07/116.20 (~E(f6(f11(a9,x1911),f11(a5,x1911)),x1912)+P2(x1912)+~P7(a9,a5,a1,x1911)), % 116.07/116.20 inference(scs_inference,[],[190,32])). % 116.07/116.20 cnf(312,plain, % 116.07/116.20 (~E(x3121,a1)+P1(x3121)), % 116.07/116.20 inference(scs_inference,[],[33,2,18])). % 116.07/116.20 cnf(314,plain, % 116.07/116.20 (P7(a9,a5,a1,f2(a1))), % 116.07/116.20 inference(scs_inference,[],[34,312,50])). % 116.07/116.20 cnf(316,plain, % 116.07/116.20 (P5(f2(a1),f3(a5,a1))), % 116.07/116.20 inference(scs_inference,[],[314,161])). % 116.07/116.20 cnf(343,plain, % 116.07/116.20 (P7(a9,a5,a1,f3(a5,a1))+P4(f2(a1),f3(a5,a1))), % 116.07/116.20 inference(scs_inference,[],[314,316,41,31])). % 116.07/116.20 cnf(399,plain, % 116.07/116.20 (P7(a9,a5,a1,f3(a5,a1))), % 116.21/116.20 inference(scs_inference,[],[343,141])). % 116.21/116.20 cnf(424,plain, % 116.21/116.20 (~E(f3(a5,a1),x4241)+P2(f6(f11(a9,x4241),f11(a5,x4241)))), % 116.21/116.20 inference(scs_inference,[],[399,31,176,190])). % 116.21/116.20 cnf(426,plain, % 116.21/116.20 (~E(f3(a5,a1),x4261)+~P2(f6(f7(a9,x4261),f7(a5,x4261)))), % 116.21/116.20 inference(scs_inference,[],[399,31,176,190,180])). % 116.21/116.20 cnf(435,plain, % 116.21/116.20 (P2(f6(f11(a9,f3(a5,a1)),f11(a5,f3(a5,a1))))), % 116.21/116.20 inference(equality_inference,[],[424])). % 116.21/116.20 cnf(436,plain, % 116.21/116.20 (~P2(f6(f7(a9,f3(a5,a1)),f7(a5,f3(a5,a1))))), % 116.21/116.20 inference(equality_inference,[],[426])). % 116.21/116.20 cnf(631,plain, % 116.21/116.20 (P7(a9,a5,a1,a8)), % 116.21/116.20 inference(scs_inference,[],[35,314,399,33,36,40,62])). % 116.21/116.20 cnf(633,plain, % 116.21/116.20 (~P4(f6(f11(a9,a8),f11(a5,a8)),a13)), % 116.21/116.20 inference(scs_inference,[],[631,166])). % 116.21/116.20 cnf(637,plain, % 116.21/116.20 (P2(f6(f11(a9,a8),f11(a5,a8)))), % 116.21/116.20 inference(scs_inference,[],[631,176,190])). % 116.21/116.20 cnf(643,plain, % 116.21/116.20 (~E(f6(f12(a9,a8),f12(a5,a8)),f6(f7(a9,a8),f7(a5,a8)))), % 116.21/116.20 inference(scs_inference,[],[631,176,190,180,191,177])). % 116.21/116.20 cnf(715,plain, % 116.21/116.20 (~E(a13,f6(f11(a9,f2(a1)),f11(a5,f2(a1))))), % 116.21/116.20 inference(scs_inference,[],[637,633,36,33,34,35,88,60])). % 116.21/116.20 cnf(717,plain, % 116.21/116.20 (~P5(f6(f11(a9,f2(a1)),f11(a5,f2(a1))),a13)), % 116.21/116.20 inference(scs_inference,[],[637,633,36,33,35,68,60])). % 116.21/116.20 cnf(1884,plain, % 116.21/116.20 ($false), % 116.21/116.20 inference(scs_inference,[],[435,643,717,436,715,135,314,33,48,2,32,41,191,61]), % 116.21/116.20 ['proof']). % 116.21/116.20 % SZS output end Proof % 116.21/116.20 % Total time :115.703992s %------------------------------------------------------------------------------