%------------------------------------------------------------------------------ % File : Metis---2.4 % Problem : MSC013-10 : TPTP v8.1.0. Released v7.3.0. % Transfm : none % Format : tptp:raw % Command : metis --show proof --show saturation %s % Computer : n026.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 : 600s % DateTime : Sun Jul 17 22:51:31 EDT 2022 % Result : Satisfiable 1.17s 1.33s % Output : Saturation 1.17s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.12/0.12 % Problem : MSC013-10 : TPTP v8.1.0. Released v7.3.0. % 0.12/0.13 % Command : metis --show proof --show saturation %s % 0.13/0.34 % Computer : n026.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 600 % 0.13/0.34 % DateTime : Fri Jul 1 15:24:04 EDT 2022 % 0.13/0.34 % CPUTime : % 0.13/0.35 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 1.17/1.33 % SZS status Satisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 1.17/1.33 % 1.17/1.33 SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 1.17/1.33 |- ifeq $A $A $B $C = $B % 1.17/1.33 |- equalish n0 n0 = true % 1.17/1.33 |- equalish n1 n1 = true % 1.17/1.33 |- ifeq (equalish n0 n1) true goal true = true % 1.17/1.33 |- ifeq (equalish n1 n0) true goal true = true % 1.17/1.33 |- ifeq (equalish $E $E) true % 1.17/1.33 (ifeq (equalish $D $D) true % 1.17/1.33 (ifeq (equalish $C $C) true % 1.17/1.33 (ifeq (equalish $B $B) true % 1.17/1.33 (ifeq (equalish $A $A) true % 1.17/1.33 (f $A $B $C $D $E (sK1_relation_exists_F $A $B $C $D $E)) % 1.17/1.33 true) true) true) true) true = true % 1.17/1.33 |- ifeq (f $F $G $H $I $J $K) true % 1.17/1.33 (ifeq (f $A $B $C $D $E $K) true (equalish $E $J) true) true = true % 1.17/1.33 |- ifeq (f $F $G $H $I $J $K) true % 1.17/1.33 (ifeq (f $A $B $C $D $E $K) true (equalish $D $I) true) true = true % 1.17/1.33 |- ifeq (f $F $G $H $I $J $K) true % 1.17/1.33 (ifeq (f $A $B $C $D $E $K) true (equalish $C $H) true) true = true % 1.17/1.33 |- ifeq (f $F $G $H $I $J $K) true % 1.17/1.33 (ifeq (f $A $B $C $D $E $K) true (equalish $B $G) true) true = true % 1.17/1.33 |- ifeq (f $F $G $H $I $J $K) true % 1.17/1.33 (ifeq (f $A $B $C $D $E $K) true (equalish $A $F) true) true = true % 1.17/1.33 |- ~(goal = true) % 1.17/1.33 |- ifeq (f $_8 $_9 $_10 $_11 n0 $_13) true % 1.17/1.33 (ifeq (f $_3 $_4 $_5 $_6 n0 $_13) true true true) true = true % 1.17/1.33 |- ifeq (f $_8 $_9 $_10 $_11 n1 $_13) true % 1.17/1.33 (ifeq (f $_3 $_4 $_5 $_6 n1 $_13) true true true) true = true % 1.17/1.33 |- ifeq (f $_28 $_29 n0 $_31 $_32 $_33) true % 1.17/1.33 (ifeq (f $_23 $_24 n0 $_26 $_27 $_33) true true true) true = true % 1.17/1.33 |- ifeq (f $_28 $_29 n1 $_31 $_32 $_33) true % 1.17/1.33 (ifeq (f $_23 $_24 n1 $_26 $_27 $_33) true true true) true = true % 1.17/1.33 |- ifeq (f n0 $_49 $_50 $_51 $_52 $_53) true % 1.17/1.33 (ifeq (f n0 $_44 $_45 $_46 $_47 $_53) true true true) true = true % 1.17/1.33 |- ifeq (f n1 $_49 $_50 $_51 $_52 $_53) true % 1.17/1.33 (ifeq (f n1 $_44 $_45 $_46 $_47 $_53) true true true) true = true % 1.17/1.33 |- ifeq (equalish $_67 $_67) true % 1.17/1.33 (ifeq (equalish $_66 $_66) true % 1.17/1.33 (ifeq (equalish $_65 $_65) true % 1.17/1.33 (ifeq (equalish $_64 $_64) true % 1.17/1.33 (f n0 $_64 $_65 $_66 $_67 % 1.17/1.33 (sK1_relation_exists_F n0 $_64 $_65 $_66 $_67)) true) % 1.17/1.33 true) true) true = true % 1.17/1.33 |- ifeq (equalish $_67 $_67) true % 1.17/1.33 (ifeq (equalish $_66 $_66) true % 1.17/1.33 (ifeq (equalish $_65 $_65) true % 1.17/1.33 (ifeq (equalish $_64 $_64) true % 1.17/1.33 (f n1 $_64 $_65 $_66 $_67 % 1.17/1.33 (sK1_relation_exists_F n1 $_64 $_65 $_66 $_67)) true) % 1.17/1.33 true) true) true = true % 1.17/1.33 |- ifeq (equalish $_67 $_67) true % 1.17/1.33 (ifeq (equalish $_66 $_66) true % 1.17/1.33 (ifeq (equalish $_65 $_65) true % 1.17/1.33 (ifeq (equalish $_63 $_63) true % 1.17/1.33 (f $_63 n0 $_65 $_66 $_67 % 1.17/1.33 (sK1_relation_exists_F $_63 n0 $_65 $_66 $_67)) true) % 1.17/1.33 true) true) true = true % 1.17/1.33 |- ifeq (equalish $_67 $_67) true % 1.17/1.33 (ifeq (equalish $_66 $_66) true % 1.17/1.33 (ifeq (equalish $_65 $_65) true % 1.17/1.33 (ifeq (equalish $_63 $_63) true % 1.17/1.33 (f $_63 n1 $_65 $_66 $_67 % 1.17/1.33 (sK1_relation_exists_F $_63 n1 $_65 $_66 $_67)) true) % 1.17/1.33 true) true) true = true % 1.17/1.33 |- ifeq (equalish $_67 $_67) true % 1.17/1.33 (ifeq (equalish $_66 $_66) true % 1.17/1.33 (ifeq (equalish $_64 $_64) true % 1.17/1.33 (ifeq (equalish $_63 $_63) true % 1.17/1.33 (f $_63 $_64 n0 $_66 $_67 % 1.17/1.33 (sK1_relation_exists_F $_63 $_64 n0 $_66 $_67)) true) % 1.17/1.33 true) true) true = true % 1.17/1.33 |- ifeq (equalish $_67 $_67) true % 1.17/1.33 (ifeq (equalish $_66 $_66) true % 1.17/1.33 (ifeq (equalish $_64 $_64) true % 1.17/1.33 (ifeq (equalish $_63 $_63) true % 1.17/1.33 (f $_63 $_64 n1 $_66 $_67 % 1.17/1.33 (sK1_relation_exists_F $_63 $_64 n1 $_66 $_67)) true) % 1.17/1.33 true) true) true = true % 1.17/1.33 |- ifeq (equalish $_67 $_67) true % 1.17/1.33 (ifeq (equalish $_65 $_65) true % 1.17/1.33 (ifeq (equalish $_64 $_64) true % 1.17/1.33 (ifeq (equalish $_63 $_63) true % 1.17/1.33 (f $_63 $_64 $_65 n0 $_67 % 1.17/1.33 (sK1_relation_exists_F $_63 $_64 $_65 n0 $_67)) true) % 1.17/1.33 true) true) true = true % 1.17/1.33 |- ifeq (equalish $_67 $_67) true % 1.17/1.33 (ifeq (equalish $_65 $_65) true % 1.17/1.33 (ifeq (equalish $_64 $_64) true % 1.17/1.33 (ifeq (equalish $_63 $_63) true % 1.17/1.33 (f $_63 $_64 $_65 n1 $_67 % 1.17/1.33 (sK1_relation_exists_F $_63 $_64 $_65 n1 $_67)) true) % 1.17/1.33 true) true) true = true % 1.17/1.33 |- ifeq (equalish $_66 $_66) true % 1.17/1.33 (ifeq (equalish $_65 $_65) true % 1.17/1.33 (ifeq (equalish $_64 $_64) true % 1.17/1.33 (ifeq (equalish $_63 $_63) true % 1.17/1.33 (f $_63 $_64 $_65 $_66 n0 % 1.17/1.33 (sK1_relation_exists_F $_63 $_64 $_65 $_66 n0)) true) % 1.17/1.33 true) true) true = true % 1.17/1.33 |- ifeq (equalish $_66 $_66) true % 1.17/1.33 (ifeq (equalish $_65 $_65) true % 1.17/1.33 (ifeq (equalish $_64 $_64) true % 1.17/1.33 (ifeq (equalish $_63 $_63) true % 1.17/1.33 (f $_63 $_64 $_65 $_66 n1 % 1.17/1.33 (sK1_relation_exists_F $_63 $_64 $_65 $_66 n1)) true) % 1.17/1.33 true) true) true = true % 1.17/1.33 |- ifeq (equalish $_71 $_71) true % 1.17/1.33 (ifeq (equalish $_70 $_70) true % 1.17/1.33 (ifeq (equalish $_69 $_69) true % 1.17/1.33 (f n0 n0 $_69 $_70 $_71 % 1.17/1.33 (sK1_relation_exists_F n0 n0 $_69 $_70 $_71)) true) true) % 1.17/1.33 true = true % 1.17/1.33 |- ifeq (equalish $_71 $_71) true % 1.17/1.33 (ifeq (equalish $_70 $_70) true % 1.17/1.33 (ifeq (equalish $_69 $_69) true % 1.17/1.33 (f n0 n1 $_69 $_70 $_71 % 1.17/1.33 (sK1_relation_exists_F n0 n1 $_69 $_70 $_71)) true) true) % 1.17/1.33 true = true % 1.17/1.33 |- ifeq (equalish $_71 $_71) true % 1.17/1.33 (ifeq (equalish $_70 $_70) true % 1.17/1.33 (ifeq (equalish $_68 $_68) true % 1.17/1.33 (f n0 $_68 n0 $_70 $_71 % 1.17/1.33 (sK1_relation_exists_F n0 $_68 n0 $_70 $_71)) true) true) % 1.17/1.33 true = true % 1.17/1.33 |- ifeq (equalish $_71 $_71) true % 1.17/1.33 (ifeq (equalish $_70 $_70) true % 1.17/1.33 (ifeq (equalish $_68 $_68) true % 1.17/1.33 (f n0 $_68 n1 $_70 $_71 % 1.17/1.33 (sK1_relation_exists_F n0 $_68 n1 $_70 $_71)) true) true) % 1.17/1.33 true = true % 1.17/1.33 |- ifeq (equalish $_71 $_71) true % 1.17/1.33 (ifeq (equalish $_69 $_69) true % 1.17/1.33 (ifeq (equalish $_68 $_68) true % 1.17/1.33 (f n0 $_68 $_69 n0 $_71 % 1.17/1.33 (sK1_relation_exists_F n0 $_68 $_69 n0 $_71)) true) true) % 1.17/1.33 true = true % 1.17/1.33 |- ifeq (equalish $_71 $_71) true % 1.17/1.33 (ifeq (equalish $_69 $_69) true % 1.17/1.33 (ifeq (equalish $_68 $_68) true % 1.17/1.33 (f n0 $_68 $_69 n1 $_71 % 1.17/1.33 (sK1_relation_exists_F n0 $_68 $_69 n1 $_71)) true) true) % 1.17/1.33 true = true % 1.17/1.33 |- ifeq (equalish $_70 $_70) true % 1.17/1.33 (ifeq (equalish $_69 $_69) true % 1.17/1.33 (ifeq (equalish $_68 $_68) true % 1.17/1.33 (f n0 $_68 $_69 $_70 n0 % 1.17/1.33 (sK1_relation_exists_F n0 $_68 $_69 $_70 n0)) true) true) % 1.17/1.33 true = true % 1.17/1.33 |- ifeq (equalish $_70 $_70) true % 1.17/1.33 (ifeq (equalish $_69 $_69) true % 1.17/1.33 (ifeq (equalish $_68 $_68) true % 1.17/1.33 (f n0 $_68 $_69 $_70 n1 % 1.17/1.33 (sK1_relation_exists_F n0 $_68 $_69 $_70 n1)) true) true) % 1.17/1.33 true = true % 1.17/1.33 |- ifeq (equalish $_75 $_75) true % 1.17/1.33 (ifeq (equalish $_74 $_74) true % 1.17/1.33 (ifeq (equalish $_73 $_73) true % 1.17/1.33 (f n1 n0 $_73 $_74 $_75 % 1.17/1.33 (sK1_relation_exists_F n1 n0 $_73 $_74 $_75)) true) true) % 1.17/1.33 true = true % 1.17/1.33 |- ifeq (equalish $_75 $_75) true % 1.17/1.33 (ifeq (equalish $_74 $_74) true % 1.17/1.33 (ifeq (equalish $_73 $_73) true % 1.17/1.33 (f n1 n1 $_73 $_74 $_75 % 1.17/1.33 (sK1_relation_exists_F n1 n1 $_73 $_74 $_75)) true) true) % 1.17/1.33 true = true % 1.17/1.33 |- ifeq (equalish $_75 $_75) true % 1.17/1.33 (ifeq (equalish $_74 $_74) true % 1.17/1.33 (ifeq (equalish $_72 $_72) true % 1.17/1.33 (f n1 $_72 n0 $_74 $_75 % 1.17/1.33 (sK1_relation_exists_F n1 $_72 n0 $_74 $_75)) true) true) % 1.17/1.33 true = true % 1.17/1.33 |- ifeq (equalish $_75 $_75) true % 1.17/1.33 (ifeq (equalish $_74 $_74) true % 1.17/1.33 (ifeq (equalish $_72 $_72) true % 1.17/1.33 (f n1 $_72 n1 $_74 $_75 % 1.17/1.33 (sK1_relation_exists_F n1 $_72 n1 $_74 $_75)) true) true) % 1.17/1.33 true = true % 1.17/1.33 |- ifeq (equalish $_75 $_75) true % 1.17/1.33 (ifeq (equalish $_73 $_73) true % 1.17/1.33 (ifeq (equalish $_72 $_72) true % 1.17/1.33 (f n1 $_72 $_73 n0 $_75 % 1.17/1.33 (sK1_relation_exists_F n1 $_72 $_73 n0 $_75)) true) true) % 1.17/1.33 true = true % 1.17/1.33 |- ifeq (equalish $_75 $_75) true % 1.17/1.33 (ifeq (equalish $_73 $_73) true % 1.17/1.33 (ifeq (equalish $_72 $_72) true % 1.17/1.33 (f n1 $_72 $_73 n1 $_75 % 1.17/1.33 (sK1_relation_exists_F n1 $_72 $_73 n1 $_75)) true) true) % 1.17/1.33 true = true % 1.17/1.33 |- ifeq (equalish $_74 $_74) true % 1.17/1.33 (ifeq (equalish $_73 $_73) true % 1.17/1.33 (ifeq (equalish $_72 $_72) true % 1.17/1.33 (f n1 $_72 $_73 $_74 n0 % 1.17/1.33 (sK1_relation_exists_F n1 $_72 $_73 $_74 n0)) true) true) % 1.17/1.33 true = true % 1.17/1.33 |- ifeq (equalish $_74 $_74) true % 1.17/1.33 (ifeq (equalish $_73 $_73) true % 1.17/1.33 (ifeq (equalish $_72 $_72) true % 1.17/1.33 (f n1 $_72 $_73 $_74 n1 % 1.17/1.33 (sK1_relation_exists_F n1 $_72 $_73 $_74 n1)) true) true) % 1.17/1.33 true = true % 1.17/1.33 |- ifeq (equalish $_79 $_79) true % 1.17/1.33 (ifeq (equalish $_78 $_78) true % 1.17/1.33 (ifeq (equalish $_76 $_76) true % 1.17/1.33 (f $_76 n0 n0 $_78 $_79 % 1.17/1.33 (sK1_relation_exists_F $_76 n0 n0 $_78 $_79)) true) true) % 1.17/1.33 true = true % 1.17/1.33 |- ifeq (equalish $_79 $_79) true % 1.17/1.33 (ifeq (equalish $_78 $_78) true % 1.17/1.33 (ifeq (equalish $_76 $_76) true % 1.17/1.33 (f $_76 n0 n1 $_78 $_79 % 1.17/1.33 (sK1_relation_exists_F $_76 n0 n1 $_78 $_79)) true) true) % 1.17/1.33 true = true % 1.17/1.33 |- ifeq (equalish $_79 $_79) true % 1.17/1.33 (ifeq (equalish $_77 $_77) true % 1.17/1.33 (ifeq (equalish $_76 $_76) true % 1.17/1.33 (f $_76 n0 $_77 n0 $_79 % 1.17/1.33 (sK1_relation_exists_F $_76 n0 $_77 n0 $_79)) true) true) % 1.17/1.33 true = true % 1.17/1.33 |- ifeq (equalish $_79 $_79) true % 1.17/1.33 (ifeq (equalish $_77 $_77) true % 1.17/1.33 (ifeq (equalish $_76 $_76) true % 1.17/1.33 (f $_76 n0 $_77 n1 $_79 % 1.17/1.33 (sK1_relation_exists_F $_76 n0 $_77 n1 $_79)) true) true) % 1.17/1.33 true = true % 1.17/1.33 |- ifeq (equalish $_78 $_78) true % 1.17/1.33 (ifeq (equalish $_77 $_77) true % 1.17/1.33 (ifeq (equalish $_76 $_76) true % 1.17/1.33 (f $_76 n0 $_77 $_78 n0 % 1.17/1.33 (sK1_relation_exists_F $_76 n0 $_77 $_78 n0)) true) true) % 1.17/1.33 true = true % 1.17/1.33 |- ifeq (equalish $_78 $_78) true % 1.17/1.33 (ifeq (equalish $_77 $_77) true % 1.17/1.33 (ifeq (equalish $_76 $_76) true % 1.17/1.33 (f $_76 n0 $_77 $_78 n1 % 1.17/1.33 (sK1_relation_exists_F $_76 n0 $_77 $_78 n1)) true) true) % 1.17/1.33 true = true % 1.17/1.33 |- ifeq (equalish $_83 $_83) true % 1.17/1.33 (ifeq (equalish $_82 $_82) true % 1.17/1.33 (ifeq (equalish $_80 $_80) true % 1.17/1.33 (f $_80 n1 n0 $_82 $_83 % 1.17/1.33 (sK1_relation_exists_F $_80 n1 n0 $_82 $_83)) true) true) % 1.17/1.33 true = true % 1.17/1.33 |- ifeq (equalish $_83 $_83) true % 1.17/1.33 (ifeq (equalish $_82 $_82) true % 1.17/1.33 (ifeq (equalish $_80 $_80) true % 1.17/1.33 (f $_80 n1 n1 $_82 $_83 % 1.17/1.33 (sK1_relation_exists_F $_80 n1 n1 $_82 $_83)) true) true) % 1.17/1.33 true = true % 1.17/1.33 |- ifeq (equalish $_83 $_83) true % 1.17/1.33 (ifeq (equalish $_81 $_81) true % 1.17/1.33 (ifeq (equalish $_80 $_80) true % 1.17/1.33 (f $_80 n1 $_81 n0 $_83 % 1.17/1.33 (sK1_relation_exists_F $_80 n1 $_81 n0 $_83)) true) true) % 1.17/1.33 true = true % 1.17/1.33 |- ifeq (equalish $_83 $_83) true % 1.17/1.33 (ifeq (equalish $_81 $_81) true % 1.17/1.33 (ifeq (equalish $_80 $_80) true % 1.17/1.33 (f $_80 n1 $_81 n1 $_83 % 1.17/1.33 (sK1_relation_exists_F $_80 n1 $_81 n1 $_83)) true) true) % 1.17/1.33 true = true % 1.17/1.33 |- ifeq (equalish $_82 $_82) true % 1.17/1.33 (ifeq (equalish $_81 $_81) true % 1.17/1.33 (ifeq (equalish $_80 $_80) true % 1.17/1.33 (f $_80 n1 $_81 $_82 n0 % 1.17/1.33 (sK1_relation_exists_F $_80 n1 $_81 $_82 n0)) true) true) % 1.17/1.33 true = true % 1.17/1.33 |- ifeq (equalish $_82 $_82) true % 1.17/1.33 (ifeq (equalish $_81 $_81) true % 1.17/1.33 (ifeq (equalish $_80 $_80) true % 1.17/1.33 (f $_80 n1 $_81 $_82 n1 % 1.17/1.33 (sK1_relation_exists_F $_80 n1 $_81 $_82 n1)) true) true) % 1.17/1.33 true = true % 1.17/1.33 |- ifeq (equalish $_87 $_87) true % 1.17/1.33 (ifeq (equalish $_85 $_85) true % 1.17/1.33 (ifeq (equalish $_84 $_84) true % 1.17/1.33 (f $_84 $_85 n0 n0 $_87 % 1.17/1.33 (sK1_relation_exists_F $_84 $_85 n0 n0 $_87)) true) true) % 1.17/1.33 true = true % 1.17/1.33 |- ifeq (equalish $_87 $_87) true % 1.17/1.33 (ifeq (equalish $_85 $_85) true % 1.17/1.33 (ifeq (equalish $_84 $_84) true % 1.17/1.33 (f $_84 $_85 n0 n1 $_87 % 1.17/1.33 (sK1_relation_exists_F $_84 $_85 n0 n1 $_87)) true) true) % 1.17/1.33 true = true % 1.17/1.33 |- ifeq (equalish $_86 $_86) true % 1.17/1.33 (ifeq (equalish $_85 $_85) true % 1.17/1.33 (ifeq (equalish $_84 $_84) true % 1.17/1.33 (f $_84 $_85 n0 $_86 n0 % 1.17/1.33 (sK1_relation_exists_F $_84 $_85 n0 $_86 n0)) true) true) % 1.17/1.33 true = true % 1.17/1.33 |- ifeq (equalish $_86 $_86) true % 1.17/1.33 (ifeq (equalish $_85 $_85) true % 1.17/1.33 (ifeq (equalish $_84 $_84) true % 1.17/1.33 (f $_84 $_85 n0 $_86 n1 % 1.17/1.33 (sK1_relation_exists_F $_84 $_85 n0 $_86 n1)) true) true) % 1.17/1.33 true = true % 1.17/1.33 |- ifeq (equalish $_90 $_90) true % 1.17/1.33 (ifeq (equalish $_89 $_89) true % 1.17/1.33 (f n0 $_89 n0 $_90 n0 (sK1_relation_exists_F n0 $_89 n0 $_90 n0)) % 1.17/1.33 true) true = true % 1.17/1.33 |- ifeq (equalish $_90 $_90) true % 1.17/1.33 (ifeq (equalish $_89 $_89) true % 1.17/1.33 (f n1 $_89 n0 $_90 n0 (sK1_relation_exists_F n1 $_89 n0 $_90 n0)) % 1.17/1.33 true) true = true % 1.17/1.33 |- ifeq (equalish $_90 $_90) true % 1.17/1.33 (ifeq (equalish $_88 $_88) true % 1.17/1.33 (f $_88 n0 n0 $_90 n0 (sK1_relation_exists_F $_88 n0 n0 $_90 n0)) % 1.17/1.33 true) true = true % 1.17/1.33 |- ifeq (equalish $_90 $_90) true % 1.17/1.33 (ifeq (equalish $_88 $_88) true % 1.17/1.33 (f $_88 n1 n0 $_90 n0 (sK1_relation_exists_F $_88 n1 n0 $_90 n0)) % 1.17/1.33 true) true = true % 1.17/1.33 |- ifeq (equalish $_89 $_89) true % 1.17/1.33 (ifeq (equalish $_88 $_88) true % 1.17/1.33 (f $_88 $_89 n0 n0 n0 (sK1_relation_exists_F $_88 $_89 n0 n0 n0)) % 1.17/1.33 true) true = true % 1.17/1.34 |- ifeq (equalish $_89 $_89) true % 1.17/1.34 (ifeq (equalish $_88 $_88) true % 1.17/1.34 (f $_88 $_89 n0 n1 n0 (sK1_relation_exists_F $_88 $_89 n0 n1 n0)) % 1.17/1.34 true) true = true % 1.17/1.34 |- ifeq (equalish $_92 $_92) true % 1.17/1.34 (f n0 n0 n0 $_92 n0 (sK1_relation_exists_F n0 n0 n0 $_92 n0)) true = % 1.17/1.34 true % 1.17/1.34 |- ifeq (equalish $_92 $_92) true % 1.17/1.34 (f n0 n1 n0 $_92 n0 (sK1_relation_exists_F n0 n1 n0 $_92 n0)) true = % 1.17/1.34 true % 1.17/1.34 |- ifeq (equalish $_91 $_91) true % 1.17/1.34 (f n0 $_91 n0 n0 n0 (sK1_relation_exists_F n0 $_91 n0 n0 n0)) true = % 1.17/1.34 true % 1.17/1.34 |- ifeq (equalish $_91 $_91) true % 1.17/1.34 (f n0 $_91 n0 n1 n0 (sK1_relation_exists_F n0 $_91 n0 n1 n0)) true = % 1.17/1.34 true % 1.17/1.34 |- f n0 n0 n0 n0 n0 (sK1_relation_exists_F n0 n0 n0 n0 n0) = true % 1.17/1.34 |- f n0 n0 n0 n1 n0 (sK1_relation_exists_F n0 n0 n0 n1 n0) = true % 1.17/1.34 |- ifeq (f $A $B $C $D $E (sK1_relation_exists_F n0 n0 n0 n0 n0)) true % 1.17/1.34 (equalish $A n0) true = true % 1.17/1.34 |- ifeq (f $F $G $H $I $J (sK1_relation_exists_F n0 n0 n0 n0 n0)) true % 1.17/1.34 (equalish n0 $F) true = true % 1.17/1.34 |- ifeq (f $A $B $C $D $E (sK1_relation_exists_F n0 n0 n0 n0 n0)) true % 1.17/1.34 (equalish $C n0) true = true % 1.17/1.34 |- ifeq (f $F $G $H $I $J (sK1_relation_exists_F n0 n0 n0 n0 n0)) true % 1.17/1.34 (equalish n0 $H) true = true % 1.17/1.34 |- ifeq (f $A $B $C $D $E (sK1_relation_exists_F n0 n0 n0 n0 n0)) true % 1.17/1.34 (equalish $E n0) true = true % 1.17/1.34 |- ifeq (f $F $G $H $I $J (sK1_relation_exists_F n0 n0 n0 n0 n0)) true % 1.17/1.34 (equalish n0 $J) true = true % 1.17/1.34 |- ifeq (f $A $B $C $D $E (sK1_relation_exists_F n0 n0 n0 n1 n0)) true % 1.17/1.34 (equalish $A n0) true = true % 1.17/1.34 |- ifeq (f $F $G $H $I $J (sK1_relation_exists_F n0 n0 n0 n1 n0)) true % 1.17/1.34 (equalish n0 $F) true = true % 1.17/1.34 |- ifeq (f $A $B $C $D $E (sK1_relation_exists_F n0 n0 n0 n1 n0)) true % 1.17/1.34 (equalish $C n0) true = true % 1.17/1.34 |- ifeq (f $F $G $H $I $J (sK1_relation_exists_F n0 n0 n0 n1 n0)) true % 1.17/1.34 (equalish n0 $H) true = true % 1.17/1.34 |- ifeq (f $A $B $C $D $E (sK1_relation_exists_F n0 n0 n0 n1 n0)) true % 1.17/1.34 (equalish $E n0) true = true % 1.17/1.34 |- ifeq (f $F $G $H $I $J (sK1_relation_exists_F n0 n0 n0 n1 n0)) true % 1.17/1.34 (equalish n0 $J) true = true % 1.17/1.34 |- f n0 n1 n0 n0 n0 (sK1_relation_exists_F n0 n1 n0 n0 n0) = true % 1.17/1.34 |- f n0 n1 n0 n1 n0 (sK1_relation_exists_F n0 n1 n0 n1 n0) = true % 1.17/1.34 |- ifeq (f $A $B $C $D $E (sK1_relation_exists_F n0 n1 n0 n0 n0)) true % 1.17/1.34 (equalish $A n0) true = true % 1.17/1.34 |- ifeq (f $F $G $H $I $J (sK1_relation_exists_F n0 n1 n0 n0 n0)) true % 1.17/1.34 (equalish n0 $F) true = true % 1.17/1.34 |- ifeq (f $A $B $C $D $E (sK1_relation_exists_F n0 n1 n0 n0 n0)) true % 1.17/1.34 (equalish $C n0) true = true % 1.17/1.34 |- ifeq (f $F $G $H $I $J (sK1_relation_exists_F n0 n1 n0 n0 n0)) true % 1.17/1.34 (equalish n0 $H) true = true % 1.17/1.34 |- ifeq (f $A $B $C $D $E (sK1_relation_exists_F n0 n1 n0 n0 n0)) true % 1.17/1.34 (equalish $E n0) true = true % 1.17/1.34 |- ifeq (f $F $G $H $I $J (sK1_relation_exists_F n0 n1 n0 n0 n0)) true % 1.17/1.34 (equalish n0 $J) true = true % 1.17/1.34 |- ifeq (f $A $B $C $D $E (sK1_relation_exists_F n0 n1 n0 n1 n0)) true % 1.17/1.34 (equalish $A n0) true = true % 1.17/1.34 |- ifeq (f $F $G $H $I $J (sK1_relation_exists_F n0 n1 n0 n1 n0)) true % 1.17/1.34 (equalish n0 $F) true = true % 1.17/1.34 |- ifeq (f $A $B $C $D $E (sK1_relation_exists_F n0 n1 n0 n1 n0)) true % 1.17/1.34 (equalish $C n0) true = true % 1.17/1.34 |- ifeq (f $F $G $H $I $J (sK1_relation_exists_F n0 n1 n0 n1 n0)) true % 1.17/1.34 (equalish n0 $H) true = true % 1.17/1.34 |- ifeq (f $A $B $C $D $E (sK1_relation_exists_F n0 n1 n0 n1 n0)) true % 1.17/1.34 (equalish $E n0) true = true % 1.17/1.34 |- ifeq (f $F $G $H $I $J (sK1_relation_exists_F n0 n1 n0 n1 n0)) true % 1.17/1.34 (equalish n0 $J) true = true % 1.17/1.34 |- ifeq (equalish $_98 $_98) true % 1.17/1.34 (f n1 n0 n0 $_98 n0 (sK1_relation_exists_F n1 n0 n0 $_98 n0)) true = % 1.17/1.34 true % 1.17/1.34 |- ifeq (equalish $_98 $_98) true % 1.17/1.34 (f n1 n1 n0 $_98 n0 (sK1_relation_exists_F n1 n1 n0 $_98 n0)) true = % 1.17/1.34 true % 1.17/1.34 |- ifeq (equalish $_97 $_97) true % 1.17/1.34 (f n1 $_97 n0 n0 n0 (sK1_relation_exists_F n1 $_97 n0 n0 n0)) true = % 1.17/1.34 true % 1.17/1.34 |- ifeq (equalish $_97 $_97) true % 1.17/1.34 (f n1 $_97 n0 n1 n0 (sK1_relation_exists_F n1 $_97 n0 n1 n0)) true = % 1.17/1.34 true % 1.17/1.34 |- f n1 n0 n0 n0 n0 (sK1_relation_exists_F n1 n0 n0 n0 n0) = true % 1.17/1.34 |- f n1 n0 n0 n1 n0 (sK1_relation_exists_F n1 n0 n0 n1 n0) = true % 1.17/1.34 |- ifeq (f $A $B $C $D $E (sK1_relation_exists_F n1 n0 n0 n1 n0)) true % 1.17/1.34 (equalish $A n1) true = true % 1.17/1.34 |- ifeq (f $F $G $H $I $J (sK1_relation_exists_F n1 n0 n0 n1 n0)) true % 1.17/1.34 (equalish n1 $F) true = true % 1.17/1.34 |- ifeq (f $A $B $C $D $E (sK1_relation_exists_F n1 n0 n0 n1 n0)) true % 1.17/1.34 (equalish $C n0) true = true % 1.17/1.34 |- ifeq (f $F $G $H $I $J (sK1_relation_exists_F n1 n0 n0 n1 n0)) true % 1.17/1.34 (equalish n0 $H) true = true % 1.17/1.34 |- ifeq (f $A $B $C $D $E (sK1_relation_exists_F n1 n0 n0 n1 n0)) true % 1.17/1.34 (equalish $E n0) true = true % 1.17/1.34 |- ifeq (f $F $G $H $I $J (sK1_relation_exists_F n1 n0 n0 n1 n0)) true % 1.17/1.34 (equalish n0 $J) true = true % 1.17/1.34 |- ifeq (f $A $B $C $D $E (sK1_relation_exists_F n1 n0 n0 n0 n0)) true % 1.17/1.34 (equalish $A n1) true = true % 1.17/1.34 |- ifeq (f $F $G $H $I $J (sK1_relation_exists_F n1 n0 n0 n0 n0)) true % 1.17/1.34 (equalish n1 $F) true = true % 1.17/1.34 |- ifeq (f $A $B $C $D $E (sK1_relation_exists_F n1 n0 n0 n0 n0)) true % 1.17/1.34 (equalish $C n0) true = true % 1.17/1.34 |- ifeq (f $F $G $H $I $J (sK1_relation_exists_F n1 n0 n0 n0 n0)) true % 1.17/1.34 (equalish n0 $H) true = true % 1.17/1.34 |- ifeq (f $A $B $C $D $E (sK1_relation_exists_F n1 n0 n0 n0 n0)) true % 1.17/1.34 (equalish $E n0) true = true % 1.17/1.34 |- ifeq (f $F $G $H $I $J (sK1_relation_exists_F n1 n0 n0 n0 n0)) true % 1.17/1.34 (equalish n0 $J) true = true % 1.17/1.34 |- f n1 n1 n0 n0 n0 (sK1_relation_exists_F n1 n1 n0 n0 n0) = true % 1.17/1.34 |- f n1 n1 n0 n1 n0 (sK1_relation_exists_F n1 n1 n0 n1 n0) = true % 1.17/1.34 |- ifeq (f $A $B $C $D $E (sK1_relation_exists_F n1 n1 n0 n0 n0)) true % 1.17/1.34 (equalish $A n1) true = true % 1.17/1.34 |- ifeq (f $F $G $H $I $J (sK1_relation_exists_F n1 n1 n0 n0 n0)) true % 1.17/1.34 (equalish n1 $F) true = true % 1.17/1.34 |- ifeq (f $A $B $C $D $E (sK1_relation_exists_F n1 n1 n0 n0 n0)) true % 1.17/1.34 (equalish $C n0) true = true % 1.17/1.34 |- ifeq (f $F $G $H $I $J (sK1_relation_exists_F n1 n1 n0 n0 n0)) true % 1.17/1.34 (equalish n0 $H) true = true % 1.17/1.34 |- ifeq (f $A $B $C $D $E (sK1_relation_exists_F n1 n1 n0 n0 n0)) true % 1.17/1.34 (equalish $E n0) true = true % 1.17/1.34 |- ifeq (f $F $G $H $I $J (sK1_relation_exists_F n1 n1 n0 n0 n0)) true % 1.17/1.34 (equalish n0 $J) true = true % 1.17/1.34 |- ifeq (f $A $B $C $D $E (sK1_relation_exists_F n1 n1 n0 n1 n0)) true % 1.17/1.34 (equalish $A n1) true = true % 1.17/1.34 |- ifeq (f $F $G $H $I $J (sK1_relation_exists_F n1 n1 n0 n1 n0)) true % 1.17/1.34 (equalish n1 $F) true = true % 1.17/1.34 |- ifeq (f $A $B $C $D $E (sK1_relation_exists_F n1 n1 n0 n1 n0)) true % 1.17/1.34 (equalish $C n0) true = true % 1.17/1.34 |- ifeq (f $F $G $H $I $J (sK1_relation_exists_F n1 n1 n0 n1 n0)) true % 1.17/1.34 (equalish n0 $H) true = true % 1.17/1.34 |- ifeq (f $A $B $C $D $E (sK1_relation_exists_F n1 n1 n0 n1 n0)) true % 1.17/1.34 (equalish $E n0) true = true % 1.17/1.34 |- ifeq (f $F $G $H $I $J (sK1_relation_exists_F n1 n1 n0 n1 n0)) true % 1.17/1.34 (equalish n0 $J) true = true % 1.17/1.34 |- ifeq (equalish $_103 $_103) true % 1.17/1.34 (f $_103 n0 n0 n0 n0 (sK1_relation_exists_F $_103 n0 n0 n0 n0)) true = % 1.17/1.34 true % 1.17/1.34 |- ifeq (equalish $_103 $_103) true % 1.17/1.34 (f $_103 n0 n0 n1 n0 (sK1_relation_exists_F $_103 n0 n0 n1 n0)) true = % 1.17/1.34 true % 1.17/1.34 |- ifeq (equalish $_107 $_107) true % 1.17/1.34 (f $_107 n1 n0 n0 n0 (sK1_relation_exists_F $_107 n1 n0 n0 n0)) true = % 1.17/1.34 true % 1.17/1.34 |- ifeq (equalish $_107 $_107) true % 1.17/1.34 (f $_107 n1 n0 n1 n0 (sK1_relation_exists_F $_107 n1 n0 n1 n0)) true = % 1.17/1.34 true % 1.17/1.34 |- ifeq (equalish $_117 $_117) true % 1.17/1.34 (ifeq (equalish $_116 $_116) true % 1.17/1.34 (f n0 $_116 n0 n0 $_117 % 1.17/1.34 (sK1_relation_exists_F n0 $_116 n0 n0 $_117)) true) true = true % 1.17/1.34 |- ifeq (equalish $_117 $_117) true % 1.17/1.34 (ifeq (equalish $_116 $_116) true % 1.17/1.34 (f n1 $_116 n0 n0 $_117 % 1.17/1.34 (sK1_relation_exists_F n1 $_116 n0 n0 $_117)) true) true = true % 1.17/1.34 |- ifeq (equalish $_117 $_117) true % 1.17/1.34 (ifeq (equalish $_115 $_115) true % 1.17/1.34 (f $_115 n0 n0 n0 $_117 % 1.17/1.34 (sK1_relation_exists_F $_115 n0 n0 n0 $_117)) true) true = true % 1.17/1.34 |- ifeq (equalish $_117 $_117) true % 1.17/1.34 (ifeq (equalish $_115 $_115) true % 1.17/1.34 (f $_115 n1 n0 n0 $_117 % 1.17/1.34 (sK1_relation_exists_F $_115 n1 n0 n0 $_117)) true) true = true % 1.17/1.35 |- ifeq (equalish $_116 $_116) true % 1.17/1.35 (ifeq (equalish $_115 $_115) true % 1.17/1.35 (f $_115 $_116 n0 n0 n1 % 1.17/1.35 (sK1_relation_exists_F $_115 $_116 n0 n0 n1)) true) true = true % 1.17/1.35 |- ifeq (equalish $_119 $_119) true % 1.17/1.35 (f n0 n0 n0 n0 $_119 (sK1_relation_exists_F n0 n0 n0 n0 $_119)) true = % 1.17/1.35 true % 1.17/1.35 |- ifeq (equalish $_119 $_119) true % 1.17/1.35 (f n0 n1 n0 n0 $_119 (sK1_relation_exists_F n0 n1 n0 n0 $_119)) true = % 1.17/1.35 true % 1.17/1.35 |- ifeq (equalish $_118 $_118) true % 1.17/1.35 (f n0 $_118 n0 n0 n1 (sK1_relation_exists_F n0 $_118 n0 n0 n1)) true = % 1.17/1.35 true % 1.17/1.35 |- f n0 n0 n0 n0 n1 (sK1_relation_exists_F n0 n0 n0 n0 n1) = true % 1.17/1.35 |- ifeq (f $A $B $C $D $E (sK1_relation_exists_F n0 n0 n0 n0 n1)) true % 1.17/1.35 (equalish $A n0) true = true % 1.17/1.35 |- ifeq (f $F $G $H $I $J (sK1_relation_exists_F n0 n0 n0 n0 n1)) true % 1.17/1.35 (equalish n0 $F) true = true % 1.17/1.35 |- ifeq (f $A $B $C $D $E (sK1_relation_exists_F n0 n0 n0 n0 n1)) true % 1.17/1.35 (equalish $C n0) true = true % 1.17/1.35 |- ifeq (f $F $G $H $I $J (sK1_relation_exists_F n0 n0 n0 n0 n1)) true % 1.17/1.35 (equalish n0 $H) true = true % 1.17/1.35 |- ifeq (f $A $B $C $D $E (sK1_relation_exists_F n0 n0 n0 n0 n1)) true % 1.17/1.35 (equalish $E n1) true = true % 1.17/1.35 |- ifeq (f $F $G $H $I $J (sK1_relation_exists_F n0 n0 n0 n0 n1)) true % 1.17/1.35 (equalish n1 $J) true = true % 1.17/1.35 |- f n0 n1 n0 n0 n1 (sK1_relation_exists_F n0 n1 n0 n0 n1) = true % 1.17/1.35 |- ifeq (f $A $B $C $D $E (sK1_relation_exists_F n0 n1 n0 n0 n1)) true % 1.17/1.35 (equalish $A n0) true = true % 1.17/1.35 |- ifeq (f $F $G $H $I $J (sK1_relation_exists_F n0 n1 n0 n0 n1)) true % 1.17/1.35 (equalish n0 $F) true = true % 1.17/1.35 |- ifeq (f $A $B $C $D $E (sK1_relation_exists_F n0 n1 n0 n0 n1)) true % 1.17/1.35 (equalish $C n0) true = true % 1.17/1.35 |- ifeq (f $F $G $H $I $J (sK1_relation_exists_F n0 n1 n0 n0 n1)) true % 1.17/1.35 (equalish n0 $H) true = true % 1.17/1.35 |- ifeq (f $A $B $C $D $E (sK1_relation_exists_F n0 n1 n0 n0 n1)) true % 1.17/1.35 (equalish $E n1) true = true % 1.17/1.35 |- ifeq (f $F $G $H $I $J (sK1_relation_exists_F n0 n1 n0 n0 n1)) true % 1.17/1.35 (equalish n1 $J) true = true % 1.17/1.35 |- ifeq (equalish $_124 $_124) true % 1.17/1.35 (f n1 n0 n0 n0 $_124 (sK1_relation_exists_F n1 n0 n0 n0 $_124)) true = % 1.17/1.35 true % 1.17/1.35 |- ifeq (equalish $_124 $_124) true % 1.17/1.35 (f n1 n1 n0 n0 $_124 (sK1_relation_exists_F n1 n1 n0 n0 $_124)) true = % 1.17/1.35 true % 1.17/1.35 |- ifeq (equalish $_123 $_123) true % 1.17/1.35 (f n1 $_123 n0 n0 n1 (sK1_relation_exists_F n1 $_123 n0 n0 n1)) true = % 1.17/1.35 true % 1.17/1.35 |- f n1 n0 n0 n0 n1 (sK1_relation_exists_F n1 n0 n0 n0 n1) = true % 1.17/1.35 |- ifeq (f $A $B $C $D $E (sK1_relation_exists_F n1 n0 n0 n0 n1)) true % 1.17/1.35 (equalish $A n1) true = true % 1.17/1.35 |- ifeq (f $F $G $H $I $J (sK1_relation_exists_F n1 n0 n0 n0 n1)) true % 1.17/1.35 (equalish n1 $F) true = true % 1.17/1.35 |- ifeq (f $A $B $C $D $E (sK1_relation_exists_F n1 n0 n0 n0 n1)) true % 1.17/1.35 (equalish $C n0) true = true % 1.17/1.35 |- ifeq (f $F $G $H $I $J (sK1_relation_exists_F n1 n0 n0 n0 n1)) true % 1.17/1.35 (equalish n0 $H) true = true % 1.17/1.35 |- ifeq (f $A $B $C $D $E (sK1_relation_exists_F n1 n0 n0 n0 n1)) true % 1.17/1.35 (equalish $E n1) true = true % 1.17/1.35 |- ifeq (f $F $G $H $I $J (sK1_relation_exists_F n1 n0 n0 n0 n1)) true % 1.17/1.35 (equalish n1 $J) true = true % 1.17/1.35 |- f n1 n1 n0 n0 n1 (sK1_relation_exists_F n1 n1 n0 n0 n1) = true % 1.17/1.35 |- ifeq (f $A $B $C $D $E (sK1_relation_exists_F n1 n1 n0 n0 n1)) true % 1.17/1.35 (equalish $A n1) true = true % 1.17/1.35 |- ifeq (f $F $G $H $I $J (sK1_relation_exists_F n1 n1 n0 n0 n1)) true % 1.17/1.35 (equalish n1 $F) true = true % 1.17/1.35 |- ifeq (f $A $B $C $D $E (sK1_relation_exists_F n1 n1 n0 n0 n1)) true % 1.17/1.35 (equalish $C n0) true = true % 1.17/1.35 |- ifeq (f $F $G $H $I $J (sK1_relation_exists_F n1 n1 n0 n0 n1)) true % 1.17/1.35 (equalish n0 $H) true = true % 1.17/1.35 |- ifeq (f $A $B $C $D $E (sK1_relation_exists_F n1 n1 n0 n0 n1)) true % 1.17/1.35 (equalish $E n1) true = true % 1.17/1.35 |- ifeq (f $F $G $H $I $J (sK1_relation_exists_F n1 n1 n0 n0 n1)) true % 1.17/1.35 (equalish n1 $J) true = true % 1.17/1.35 |- ifeq (equalish $_128 $_128) true % 1.17/1.35 (f $_128 n1 n0 n0 n1 (sK1_relation_exists_F $_128 n1 n0 n0 n1)) true = % 1.17/1.35 true % 1.17/1.35 |- ifeq (equalish $_131 $_131) true % 1.17/1.35 (f $_131 n0 n0 n0 n1 (sK1_relation_exists_F $_131 n0 n0 n0 n1)) true = % 1.17/1.35 true % 1.17/1.35 |- ifeq (equalish $_136 $_136) true % 1.17/1.35 (ifeq (equalish $_135 $_135) true % 1.17/1.35 (f n0 $_135 n0 n1 $_136 % 1.17/1.35 (sK1_relation_exists_F n0 $_135 n0 n1 $_136)) true) true = true % 1.17/1.35 |- ifeq (equalish $_136 $_136) true % 1.17/1.35 (ifeq (equalish $_135 $_135) true % 1.17/1.35 (f n1 $_135 n0 n1 $_136 % 1.17/1.35 (sK1_relation_exists_F n1 $_135 n0 n1 $_136)) true) true = true % 1.17/1.35 |- ifeq (equalish $_136 $_136) true % 1.17/1.35 (ifeq (equalish $_134 $_134) true % 1.17/1.35 (f $_134 n0 n0 n1 $_136 % 1.17/1.35 (sK1_relation_exists_F $_134 n0 n0 n1 $_136)) true) true = true % 1.17/1.35 |- ifeq (equalish $_136 $_136) true % 1.17/1.35 (ifeq (equalish $_134 $_134) true % 1.17/1.35 (f $_134 n1 n0 n1 $_136 % 1.17/1.35 (sK1_relation_exists_F $_134 n1 n0 n1 $_136)) true) true = true % 1.17/1.35 |- ifeq (equalish $_135 $_135) true % 1.17/1.35 (ifeq (equalish $_134 $_134) true % 1.17/1.35 (f $_134 $_135 n0 n1 n1 % 1.17/1.35 (sK1_relation_exists_F $_134 $_135 n0 n1 n1)) true) true = true % 1.17/1.35 |- ifeq (equalish $_138 $_138) true % 1.17/1.35 (f n0 n0 n0 n1 $_138 (sK1_relation_exists_F n0 n0 n0 n1 $_138)) true = % 1.17/1.35 true % 1.17/1.35 |- ifeq (equalish $_138 $_138) true % 1.17/1.35 (f n0 n1 n0 n1 $_138 (sK1_relation_exists_F n0 n1 n0 n1 $_138)) true = % 1.17/1.35 true % 1.17/1.35 |- ifeq (equalish $_137 $_137) true % 1.17/1.35 (f n0 $_137 n0 n1 n1 (sK1_relation_exists_F n0 $_137 n0 n1 n1)) true = % 1.17/1.35 true % 1.17/1.35 |- f n0 n0 n0 n1 n1 (sK1_relation_exists_F n0 n0 n0 n1 n1) = true % 1.17/1.35 |- ifeq (f $A $B $C $D $E (sK1_relation_exists_F n0 n0 n0 n1 n1)) true % 1.17/1.35 (equalish $A n0) true = true % 1.17/1.35 |- ifeq (f $F $G $H $I $J (sK1_relation_exists_F n0 n0 n0 n1 n1)) true % 1.17/1.35 (equalish n0 $F) true = true % 1.17/1.35 |- ifeq (f $A $B $C $D $E (sK1_relation_exists_F n0 n0 n0 n1 n1)) true % 1.17/1.35 (equalish $C n0) true = true % 1.17/1.35 |- ifeq (f $F $G $H $I $J (sK1_relation_exists_F n0 n0 n0 n1 n1)) true % 1.17/1.35 (equalish n0 $H) true = true % 1.17/1.35 |- ifeq (f $A $B $C $D $E (sK1_relation_exists_F n0 n0 n0 n1 n1)) true % 1.17/1.35 (equalish $E n1) true = true % 1.17/1.35 |- ifeq (f $F $G $H $I $J (sK1_relation_exists_F n0 n0 n0 n1 n1)) true % 1.17/1.35 (equalish n1 $J) true = true % 1.17/1.35 |- f n0 n1 n0 n1 n1 (sK1_relation_exists_F n0 n1 n0 n1 n1) = true % 1.17/1.35 |- ifeq (f $A $B $C $D $E (sK1_relation_exists_F n0 n1 n0 n1 n1)) true % 1.17/1.35 (equalish $A n0) true = true % 1.17/1.35 |- ifeq (f $F $G $H $I $J (sK1_relation_exists_F n0 n1 n0 n1 n1)) true % 1.17/1.35 (equalish n0 $F) true = true % 1.17/1.35 |- ifeq (f $A $B $C $D $E (sK1_relation_exists_F n0 n1 n0 n1 n1)) true % 1.17/1.35 (equalish $C n0) true = true % 1.17/1.35 |- ifeq (f $F $G $H $I $J (sK1_relation_exists_F n0 n1 n0 n1 n1)) true % 1.17/1.35 (equalish n0 $H) true = true % 1.17/1.35 |- ifeq (f $A $B $C $D $E (sK1_relation_exists_F n0 n1 n0 n1 n1)) true % 1.17/1.35 (equalish $E n1) true = true % 1.17/1.35 |- ifeq (f $F $G $H $I $J (sK1_relation_exists_F n0 n1 n0 n1 n1)) true % 1.17/1.35 (equalish n1 $J) true = true % 1.17/1.35 |- ifeq (equalish $_143 $_143) true % 1.17/1.35 (f n1 n0 n0 n1 $_143 (sK1_relation_exists_F n1 n0 n0 n1 $_143)) true = % 1.17/1.35 true % 1.17/1.35 |- ifeq (equalish $_143 $_143) true % 1.17/1.35 (f n1 n1 n0 n1 $_143 (sK1_relation_exists_F n1 n1 n0 n1 $_143)) true = % 1.17/1.35 true % 1.17/1.35 |- ifeq (equalish $_142 $_142) true % 1.17/1.35 (f n1 $_142 n0 n1 n1 (sK1_relation_exists_F n1 $_142 n0 n1 n1)) true = % 1.17/1.35 true % 1.17/1.35 |- f n1 n0 n0 n1 n1 (sK1_relation_exists_F n1 n0 n0 n1 n1) = true % 1.17/1.35 |- ifeq (f $A $B $C $D $E (sK1_relation_exists_F n1 n0 n0 n1 n1)) true % 1.17/1.35 (equalish $A n1) true = true % 1.17/1.35 |- ifeq (f $F $G $H $I $J (sK1_relation_exists_F n1 n0 n0 n1 n1)) true % 1.17/1.35 (equalish n1 $F) true = true % 1.17/1.35 |- ifeq (f $A $B $C $D $E (sK1_relation_exists_F n1 n0 n0 n1 n1)) true % 1.17/1.35 (equalish $C n0) true = true % 1.17/1.35 |- ifeq (f $F $G $H $I $J (sK1_relation_exists_F n1 n0 n0 n1 n1)) true % 1.17/1.35 (equalish n0 $H) true = true % 1.17/1.35 |- ifeq (f $A $B $C $D $E (sK1_relation_exists_F n1 n0 n0 n1 n1)) true % 1.17/1.35 (equalish $E n1) true = true % 1.17/1.35 |- ifeq (f $F $G $H $I $J (sK1_relation_exists_F n1 n0 n0 n1 n1)) true % 1.17/1.35 (equalish n1 $J) true = true % 1.17/1.35 |- f n1 n1 n0 n1 n1 (sK1_relation_exists_F n1 n1 n0 n1 n1) = true % 1.17/1.35 |- ifeq (f $A $B $C $D $E (sK1_relation_exists_F n1 n1 n0 n1 n1)) true % 1.17/1.35 (equalish $A n1) true = true % 1.17/1.35 |- ifeq (f $F $G $H $I $J (sK1_relation_exists_F n1 n1 n0 n1 n1)) true % 1.17/1.35 (equalish n1 $F) true = true % 1.17/1.35 |- ifeq (f $A $B $C $D $E (sK1_relation_exists_F n1 n1 n0 n1 n1)) true % 1.17/1.35 (equalish $C n0) true = true % 1.17/1.35 |- ifeq (f $F $G $H $I $J (sK1_relation_exists_F n1 n1 n0 n1 n1)) true % 1.17/1.35 (equalish n0 $H) true = true % 1.17/1.35 |- ifeq (f $A $B $C $D $E (sK1_relation_exists_F n1 n1 n0 n1 n1)) true % 1.17/1.35 (equalish $E n1) true = true % 1.17/1.35 |- ifeq (f $F $G $H $I $J (sK1_relation_exists_F n1 n1 n0 n1 n1)) true % 1.17/1.35 (equalish n1 $J) true = true % 1.17/1.35 |- ifeq (equalish $_147 $_147) true % 1.17/1.35 (f $_147 n0 n0 n1 n1 (sK1_relation_exists_F $_147 n0 n0 n1 n1)) true = % 1.17/1.35 true % 1.17/1.35 |- ifeq (equalish $_150 $_150) true % 1.17/1.35 (f $_150 n1 n0 n1 n1 (sK1_relation_exists_F $_150 n1 n0 n1 n1)) true = % 1.17/1.35 true % 1.17/1.35 |- ifeq (equalish $_157 $_157) true % 1.17/1.35 (ifeq (equalish $_156 $_156) true % 1.17/1.35 (f n0 $_156 n0 $_157 n1 % 1.17/1.35 (sK1_relation_exists_F n0 $_156 n0 $_157 n1)) true) true = true % 1.17/1.35 |- ifeq (equalish $_157 $_157) true % 1.17/1.35 (ifeq (equalish $_156 $_156) true % 1.17/1.35 (f n1 $_156 n0 $_157 n1 % 1.17/1.35 (sK1_relation_exists_F n1 $_156 n0 $_157 n1)) true) true = true % 1.17/1.35 |- ifeq (equalish $_157 $_157) true % 1.17/1.35 (ifeq (equalish $_155 $_155) true % 1.17/1.35 (f $_155 n0 n0 $_157 n1 % 1.17/1.35 (sK1_relation_exists_F $_155 n0 n0 $_157 n1)) true) true = true % 1.17/1.35 |- ifeq (equalish $_157 $_157) true % 1.17/1.35 (ifeq (equalish $_155 $_155) true % 1.17/1.35 (f $_155 n1 n0 $_157 n1 % 1.17/1.35 (sK1_relation_exists_F $_155 n1 n0 $_157 n1)) true) true = true % 1.17/1.35 |- ifeq (equalish $_159 $_159) true % 1.17/1.35 (f n0 n0 n0 $_159 n1 (sK1_relation_exists_F n0 n0 n0 $_159 n1)) true = % 1.17/1.35 true % 1.17/1.35 |- ifeq (equalish $_159 $_159) true % 1.17/1.35 (f n0 n1 n0 $_159 n1 (sK1_relation_exists_F n0 n1 n0 $_159 n1)) true = % 1.17/1.35 true % 1.17/1.35 |- ifeq (equalish $_163 $_163) true % 1.17/1.35 (f n1 n0 n0 $_163 n1 (sK1_relation_exists_F n1 n0 n0 $_163 n1)) true = % 1.17/1.35 true % 1.17/1.35 |- ifeq (equalish $_163 $_163) true % 1.17/1.35 (f n1 n1 n0 $_163 n1 (sK1_relation_exists_F n1 n1 n0 $_163 n1)) true = % 1.17/1.35 true % 1.17/1.35 |- ifeq (equalish $_173 $_173) true % 1.17/1.35 (ifeq (equalish $_171 $_171) true % 1.17/1.35 (ifeq (equalish $_170 $_170) true % 1.17/1.35 (f $_170 $_171 n1 n0 $_173 % 1.17/1.35 (sK1_relation_exists_F $_170 $_171 n1 n0 $_173)) true) true) % 1.17/1.35 true = true % 1.17/1.35 |- ifeq (equalish $_173 $_173) true % 1.17/1.35 (ifeq (equalish $_171 $_171) true % 1.17/1.35 (ifeq (equalish $_170 $_170) true % 1.17/1.35 (f $_170 $_171 n1 n1 $_173 % 1.17/1.35 (sK1_relation_exists_F $_170 $_171 n1 n1 $_173)) true) true) % 1.17/1.35 true = true % 1.17/1.35 |- ifeq (equalish $_172 $_172) true % 1.17/1.35 (ifeq (equalish $_171 $_171) true % 1.17/1.35 (ifeq (equalish $_170 $_170) true % 1.17/1.35 (f $_170 $_171 n1 $_172 n0 % 1.17/1.35 (sK1_relation_exists_F $_170 $_171 n1 $_172 n0)) true) true) % 1.17/1.35 true = true % 1.17/1.35 |- ifeq (equalish $_172 $_172) true % 1.17/1.35 (ifeq (equalish $_171 $_171) true % 1.17/1.35 (ifeq (equalish $_170 $_170) true % 1.17/1.35 (f $_170 $_171 n1 $_172 n1 % 1.17/1.35 (sK1_relation_exists_F $_170 $_171 n1 $_172 n1)) true) true) % 1.17/1.35 true = true % 1.17/1.35 |- ifeq (equalish $_176 $_176) true % 1.17/1.35 (ifeq (equalish $_175 $_175) true % 1.17/1.35 (f n0 $_175 n1 n1 $_176 % 1.17/1.35 (sK1_relation_exists_F n0 $_175 n1 n1 $_176)) true) true = true % 1.17/1.35 |- ifeq (equalish $_176 $_176) true % 1.17/1.35 (ifeq (equalish $_175 $_175) true % 1.17/1.35 (f n1 $_175 n1 n1 $_176 % 1.17/1.35 (sK1_relation_exists_F n1 $_175 n1 n1 $_176)) true) true = true % 1.17/1.35 |- ifeq (equalish $_176 $_176) true % 1.17/1.35 (ifeq (equalish $_174 $_174) true % 1.17/1.35 (f $_174 n0 n1 n1 $_176 % 1.17/1.35 (sK1_relation_exists_F $_174 n0 n1 n1 $_176)) true) true = true % 1.17/1.35 |- ifeq (equalish $_176 $_176) true % 1.17/1.35 (ifeq (equalish $_174 $_174) true % 1.17/1.35 (f $_174 n1 n1 n1 $_176 % 1.17/1.35 (sK1_relation_exists_F $_174 n1 n1 n1 $_176)) true) true = true % 1.17/1.35 |- ifeq (equalish $_175 $_175) true % 1.17/1.35 (ifeq (equalish $_174 $_174) true % 1.17/1.35 (f $_174 $_175 n1 n1 n0 % 1.17/1.35 (sK1_relation_exists_F $_174 $_175 n1 n1 n0)) true) true = true % 1.17/1.35 |- ifeq (equalish $_175 $_175) true % 1.17/1.35 (ifeq (equalish $_174 $_174) true % 1.17/1.35 (f $_174 $_175 n1 n1 n1 % 1.17/1.35 (sK1_relation_exists_F $_174 $_175 n1 n1 n1)) true) true = true % 1.17/1.35 |- ifeq (equalish $_178 $_178) true % 1.17/1.35 (f n1 n0 n1 n1 $_178 (sK1_relation_exists_F n1 n0 n1 n1 $_178)) true = % 1.17/1.35 true % 1.17/1.35 |- ifeq (equalish $_178 $_178) true % 1.17/1.35 (f n1 n1 n1 n1 $_178 (sK1_relation_exists_F n1 n1 n1 n1 $_178)) true = % 1.17/1.35 true % 1.17/1.35 |- ifeq (equalish $_177 $_177) true % 1.17/1.35 (f n1 $_177 n1 n1 n0 (sK1_relation_exists_F n1 $_177 n1 n1 n0)) true = % 1.17/1.35 true % 1.17/1.35 |- ifeq (equalish $_177 $_177) true % 1.17/1.35 (f n1 $_177 n1 n1 n1 (sK1_relation_exists_F n1 $_177 n1 n1 n1)) true = % 1.17/1.35 true % 1.17/1.35 |- f n1 n0 n1 n1 n0 (sK1_relation_exists_F n1 n0 n1 n1 n0) = true % 1.17/1.35 |- f n1 n0 n1 n1 n1 (sK1_relation_exists_F n1 n0 n1 n1 n1) = true % 1.17/1.35 |- ifeq (f $A $B $C $D $E (sK1_relation_exists_F n1 n0 n1 n1 n0)) true % 1.17/1.35 (equalish $A n1) true = true % 1.17/1.35 |- ifeq (f $F $G $H $I $J (sK1_relation_exists_F n1 n0 n1 n1 n0)) true % 1.17/1.35 (equalish n1 $F) true = true % 1.17/1.35 |- ifeq (f $A $B $C $D $E (sK1_relation_exists_F n1 n0 n1 n1 n0)) true % 1.17/1.35 (equalish $C n1) true = true % 1.17/1.35 |- ifeq (f $F $G $H $I $J (sK1_relation_exists_F n1 n0 n1 n1 n0)) true % 1.17/1.35 (equalish n1 $H) true = true % 1.17/1.35 |- ifeq (f $A $B $C $D $E (sK1_relation_exists_F n1 n0 n1 n1 n0)) true % 1.17/1.35 (equalish $E n0) true = true % 1.17/1.35 |- ifeq (f $F $G $H $I $J (sK1_relation_exists_F n1 n0 n1 n1 n0)) true % 1.17/1.35 (equalish n0 $J) true = true % 1.17/1.35 |- ifeq (f $A $B $C $D $E (sK1_relation_exists_F n1 n0 n1 n1 n1)) true % 1.17/1.35 (equalish $A n1) true = true % 1.17/1.35 |- ifeq (f $F $G $H $I $J (sK1_relation_exists_F n1 n0 n1 n1 n1)) true % 1.17/1.35 (equalish n1 $F) true = true % 1.17/1.35 |- ifeq (f $A $B $C $D $E (sK1_relation_exists_F n1 n0 n1 n1 n1)) true % 1.17/1.35 (equalish $C n1) true = true % 1.17/1.35 |- ifeq (f $F $G $H $I $J (sK1_relation_exists_F n1 n0 n1 n1 n1)) true % 1.17/1.35 (equalish n1 $H) true = true % 1.17/1.35 |- ifeq (f $A $B $C $D $E (sK1_relation_exists_F n1 n0 n1 n1 n1)) true % 1.17/1.35 (equalish $E n1) true = true % 1.17/1.35 |- ifeq (f $F $G $H $I $J (sK1_relation_exists_F n1 n0 n1 n1 n1)) true % 1.17/1.35 (equalish n1 $J) true = true % 1.17/1.35 |- f n1 n1 n1 n1 n0 (sK1_relation_exists_F n1 n1 n1 n1 n0) = true % 1.17/1.35 |- f n1 n1 n1 n1 n1 (sK1_relation_exists_F n1 n1 n1 n1 n1) = true % 1.17/1.35 |- ifeq (f $A $B $C $D $E (sK1_relation_exists_F n1 n1 n1 n1 n0)) true % 1.17/1.35 (equalish $A n1) true = true % 1.17/1.35 |- ifeq (f $F $G $H $I $J (sK1_relation_exists_F n1 n1 n1 n1 n0)) true % 1.17/1.35 (equalish n1 $F) true = true % 1.17/1.35 |- ifeq (f $A $B $C $D $E (sK1_relation_exists_F n1 n1 n1 n1 n0)) true % 1.17/1.35 (equalish $C n1) true = true % 1.17/1.35 |- ifeq (f $F $G $H $I $J (sK1_relation_exists_F n1 n1 n1 n1 n0)) true % 1.17/1.35 (equalish n1 $H) true = true % 1.17/1.35 |- ifeq (f $A $B $C $D $E (sK1_relation_exists_F n1 n1 n1 n1 n0)) true % 1.17/1.35 (equalish $E n0) true = true % 1.17/1.35 |- ifeq (f $F $G $H $I $J (sK1_relation_exists_F n1 n1 n1 n1 n0)) true % 1.17/1.35 (equalish n0 $J) true = true % 1.17/1.35 |- ifeq (f $A $B $C $D $E (sK1_relation_exists_F n1 n1 n1 n1 n1)) true % 1.17/1.35 (equalish $A n1) true = true % 1.17/1.35 |- ifeq (f $F $G $H $I $J (sK1_relation_exists_F n1 n1 n1 n1 n1)) true % 1.17/1.35 (equalish n1 $F) true = true % 1.17/1.35 |- ifeq (f $A $B $C $D $E (sK1_relation_exists_F n1 n1 n1 n1 n1)) true % 1.17/1.35 (equalish $C n1) true = true % 1.17/1.36 |- ifeq (f $F $G $H $I $J (sK1_relation_exists_F n1 n1 n1 n1 n1)) true % 1.17/1.36 (equalish n1 $H) true = true % 1.17/1.36 |- ifeq (f $A $B $C $D $E (sK1_relation_exists_F n1 n1 n1 n1 n1)) true % 1.17/1.36 (equalish $E n1) true = true % 1.17/1.36 |- ifeq (f $F $G $H $I $J (sK1_relation_exists_F n1 n1 n1 n1 n1)) true % 1.17/1.36 (equalish n1 $J) true = true % 1.17/1.36 |- ifeq (equalish $_184 $_184) true % 1.17/1.36 (f n0 n0 n1 n1 $_184 (sK1_relation_exists_F n0 n0 n1 n1 $_184)) true = % 1.17/1.36 true % 1.17/1.36 |- ifeq (equalish $_183 $_183) true % 1.17/1.36 (f $_183 n0 n1 n1 n0 (sK1_relation_exists_F $_183 n0 n1 n1 n0)) true = % 1.17/1.36 true % 1.17/1.36 |- ifeq (equalish $_183 $_183) true % 1.17/1.36 (f $_183 n0 n1 n1 n1 (sK1_relation_exists_F $_183 n0 n1 n1 n1)) true = % 1.17/1.36 true % 1.17/1.36 |- f n0 n0 n1 n1 n0 (sK1_relation_exists_F n0 n0 n1 n1 n0) = true % 1.17/1.36 |- f n0 n0 n1 n1 n1 (sK1_relation_exists_F n0 n0 n1 n1 n1) = true % 1.17/1.36 |- ifeq (f $A $B $C $D $E (sK1_relation_exists_F n0 n0 n1 n1 n0)) true % 1.17/1.36 (equalish $A n0) true = true % 1.17/1.36 |- ifeq (f $F $G $H $I $J (sK1_relation_exists_F n0 n0 n1 n1 n0)) true % 1.17/1.36 (equalish n0 $F) true = true % 1.17/1.36 |- ifeq (f $A $B $C $D $E (sK1_relation_exists_F n0 n0 n1 n1 n0)) true % 1.17/1.36 (equalish $C n1) true = true % 1.17/1.36 |- ifeq (f $F $G $H $I $J (sK1_relation_exists_F n0 n0 n1 n1 n0)) true % 1.17/1.36 (equalish n1 $H) true = true % 1.17/1.36 |- ifeq (f $A $B $C $D $E (sK1_relation_exists_F n0 n0 n1 n1 n0)) true % 1.17/1.36 (equalish $E n0) true = true % 1.17/1.36 |- ifeq (f $F $G $H $I $J (sK1_relation_exists_F n0 n0 n1 n1 n0)) true % 1.17/1.36 (equalish n0 $J) true = true % 1.17/1.36 |- ifeq (f $A $B $C $D $E (sK1_relation_exists_F n0 n0 n1 n1 n1)) true % 1.17/1.36 (equalish $A n0) true = true % 1.17/1.36 |- ifeq (f $F $G $H $I $J (sK1_relation_exists_F n0 n0 n1 n1 n1)) true % 1.17/1.36 (equalish n0 $F) true = true % 1.17/1.36 |- ifeq (f $A $B $C $D $E (sK1_relation_exists_F n0 n0 n1 n1 n1)) true % 1.17/1.36 (equalish $C n1) true = true % 1.17/1.36 |- ifeq (f $F $G $H $I $J (sK1_relation_exists_F n0 n0 n1 n1 n1)) true % 1.17/1.36 (equalish n1 $H) true = true % 1.17/1.36 |- ifeq (f $A $B $C $D $E (sK1_relation_exists_F n0 n0 n1 n1 n1)) true % 1.17/1.36 (equalish $E n1) true = true % 1.17/1.36 |- ifeq (f $F $G $H $I $J (sK1_relation_exists_F n0 n0 n1 n1 n1)) true % 1.17/1.36 (equalish n1 $J) true = true % 1.17/1.36 |- ifeq (equalish $_189 $_189) true % 1.17/1.36 (f n0 n1 n1 n1 $_189 (sK1_relation_exists_F n0 n1 n1 n1 $_189)) true = % 1.17/1.36 true % 1.17/1.36 |- ifeq (equalish $_188 $_188) true % 1.17/1.36 (f $_188 n1 n1 n1 n0 (sK1_relation_exists_F $_188 n1 n1 n1 n0)) true = % 1.17/1.36 true % 1.17/1.36 |- ifeq (equalish $_188 $_188) true % 1.17/1.36 (f $_188 n1 n1 n1 n1 (sK1_relation_exists_F $_188 n1 n1 n1 n1)) true = % 1.17/1.36 true % 1.17/1.36 |- f n0 n1 n1 n1 n0 (sK1_relation_exists_F n0 n1 n1 n1 n0) = true % 1.17/1.36 |- f n0 n1 n1 n1 n1 (sK1_relation_exists_F n0 n1 n1 n1 n1) = true % 1.17/1.36 |- ifeq (f $A $B $C $D $E (sK1_relation_exists_F n0 n1 n1 n1 n0)) true % 1.17/1.36 (equalish $A n0) true = true % 1.17/1.36 |- ifeq (f $F $G $H $I $J (sK1_relation_exists_F n0 n1 n1 n1 n0)) true % 1.17/1.36 (equalish n0 $F) true = true % 1.17/1.36 |- ifeq (f $A $B $C $D $E (sK1_relation_exists_F n0 n1 n1 n1 n0)) true % 1.17/1.36 (equalish $C n1) true = true % 1.17/1.36 |- ifeq (f $F $G $H $I $J (sK1_relation_exists_F n0 n1 n1 n1 n0)) true % 1.17/1.36 (equalish n1 $H) true = true % 1.17/1.36 |- ifeq (f $A $B $C $D $E (sK1_relation_exists_F n0 n1 n1 n1 n0)) true % 1.17/1.36 (equalish $E n0) true = true % 1.17/1.36 |- ifeq (f $F $G $H $I $J (sK1_relation_exists_F n0 n1 n1 n1 n0)) true % 1.17/1.36 (equalish n0 $J) true = true % 1.17/1.36 |- ifeq (f $A $B $C $D $E (sK1_relation_exists_F n0 n1 n1 n1 n1)) true % 1.17/1.36 (equalish $A n0) true = true % 1.17/1.36 |- ifeq (f $F $G $H $I $J (sK1_relation_exists_F n0 n1 n1 n1 n1)) true % 1.17/1.36 (equalish n0 $F) true = true % 1.17/1.36 |- ifeq (f $A $B $C $D $E (sK1_relation_exists_F n0 n1 n1 n1 n1)) true % 1.17/1.36 (equalish $C n1) true = true % 1.17/1.36 |- ifeq (f $F $G $H $I $J (sK1_relation_exists_F n0 n1 n1 n1 n1)) true % 1.17/1.36 (equalish n1 $H) true = true % 1.17/1.36 |- ifeq (f $A $B $C $D $E (sK1_relation_exists_F n0 n1 n1 n1 n1)) true % 1.17/1.36 (equalish $E n1) true = true % 1.17/1.36 |- ifeq (f $F $G $H $I $J (sK1_relation_exists_F n0 n1 n1 n1 n1)) true % 1.17/1.36 (equalish n1 $J) true = true % 1.17/1.36 |- ifeq (equalish $_194 $_194) true % 1.17/1.36 (f n0 $_194 n1 n1 n1 (sK1_relation_exists_F n0 $_194 n1 n1 n1)) true = % 1.17/1.36 true % 1.17/1.36 |- ifeq (equalish $_198 $_198) true % 1.17/1.36 (ifeq (equalish $_197 $_197) true % 1.17/1.36 (f n0 $_197 n1 $_198 n0 % 1.17/1.36 (sK1_relation_exists_F n0 $_197 n1 $_198 n0)) true) true = true % 1.17/1.36 |- ifeq (equalish $_198 $_198) true % 1.17/1.36 (ifeq (equalish $_197 $_197) true % 1.17/1.36 (f n1 $_197 n1 $_198 n0 % 1.17/1.36 (sK1_relation_exists_F n1 $_197 n1 $_198 n0)) true) true = true % 1.17/1.36 |- ifeq (equalish $_198 $_198) true % 1.17/1.36 (ifeq (equalish $_196 $_196) true % 1.17/1.36 (f $_196 n0 n1 $_198 n0 % 1.17/1.36 (sK1_relation_exists_F $_196 n0 n1 $_198 n0)) true) true = true % 1.17/1.36 |- ifeq (equalish $_198 $_198) true % 1.17/1.36 (ifeq (equalish $_196 $_196) true % 1.17/1.36 (f $_196 n1 n1 $_198 n0 % 1.17/1.36 (sK1_relation_exists_F $_196 n1 n1 $_198 n0)) true) true = true % 1.17/1.36 |- ifeq (equalish $_197 $_197) true % 1.17/1.36 (ifeq (equalish $_196 $_196) true % 1.17/1.36 (f $_196 $_197 n1 n0 n0 % 1.17/1.36 (sK1_relation_exists_F $_196 $_197 n1 n0 n0)) true) true = true % 1.17/1.36 |- ifeq (equalish $_200 $_200) true % 1.17/1.36 (f n0 n0 n1 $_200 n0 (sK1_relation_exists_F n0 n0 n1 $_200 n0)) true = % 1.17/1.36 true % 1.17/1.36 |- ifeq (equalish $_200 $_200) true % 1.17/1.36 (f n0 n1 n1 $_200 n0 (sK1_relation_exists_F n0 n1 n1 $_200 n0)) true = % 1.17/1.36 true % 1.17/1.36 |- ifeq (equalish $_199 $_199) true % 1.17/1.36 (f n0 $_199 n1 n0 n0 (sK1_relation_exists_F n0 $_199 n1 n0 n0)) true = % 1.17/1.36 true % 1.17/1.36 |- ifeq (equalish $_199 $_199) true % 1.17/1.36 (f n0 $_199 n1 n1 n0 (sK1_relation_exists_F n0 $_199 n1 n1 n0)) true = % 1.17/1.36 true % 1.17/1.36 |- f n0 n0 n1 n0 n0 (sK1_relation_exists_F n0 n0 n1 n0 n0) = true % 1.17/1.36 |- ifeq (f $A $B $C $D $E (sK1_relation_exists_F n0 n0 n1 n0 n0)) true % 1.17/1.36 (equalish $A n0) true = true % 1.17/1.36 |- ifeq (f $F $G $H $I $J (sK1_relation_exists_F n0 n0 n1 n0 n0)) true % 1.17/1.36 (equalish n0 $F) true = true % 1.17/1.36 |- ifeq (f $A $B $C $D $E (sK1_relation_exists_F n0 n0 n1 n0 n0)) true % 1.17/1.36 (equalish $C n1) true = true % 1.17/1.36 |- ifeq (f $F $G $H $I $J (sK1_relation_exists_F n0 n0 n1 n0 n0)) true % 1.17/1.36 (equalish n1 $H) true = true % 1.17/1.36 |- ifeq (f $A $B $C $D $E (sK1_relation_exists_F n0 n0 n1 n0 n0)) true % 1.17/1.36 (equalish $E n0) true = true % 1.17/1.36 |- ifeq (f $F $G $H $I $J (sK1_relation_exists_F n0 n0 n1 n0 n0)) true % 1.17/1.36 (equalish n0 $J) true = true % 1.17/1.36 |- f n0 n1 n1 n0 n0 (sK1_relation_exists_F n0 n1 n1 n0 n0) = true % 1.17/1.36 |- ifeq (f $A $B $C $D $E (sK1_relation_exists_F n0 n1 n1 n0 n0)) true % 1.17/1.36 (equalish $A n0) true = true % 1.17/1.36 |- ifeq (f $F $G $H $I $J (sK1_relation_exists_F n0 n1 n1 n0 n0)) true % 1.17/1.36 (equalish n0 $F) true = true % 1.17/1.36 |- ifeq (f $A $B $C $D $E (sK1_relation_exists_F n0 n1 n1 n0 n0)) true % 1.17/1.36 (equalish $C n1) true = true % 1.17/1.36 |- ifeq (f $F $G $H $I $J (sK1_relation_exists_F n0 n1 n1 n0 n0)) true % 1.17/1.36 (equalish n1 $H) true = true % 1.17/1.36 |- ifeq (f $A $B $C $D $E (sK1_relation_exists_F n0 n1 n1 n0 n0)) true % 1.17/1.36 (equalish $E n0) true = true % 1.17/1.36 |- ifeq (f $F $G $H $I $J (sK1_relation_exists_F n0 n1 n1 n0 n0)) true % 1.17/1.36 (equalish n0 $J) true = true % 1.17/1.36 |- ifeq (equalish $_206 $_206) true % 1.17/1.36 (f n1 n0 n1 $_206 n0 (sK1_relation_exists_F n1 n0 n1 $_206 n0)) true = % 1.17/1.36 true % 1.17/1.36 |- ifeq (equalish $_206 $_206) true % 1.17/1.36 (f n1 n1 n1 $_206 n0 (sK1_relation_exists_F n1 n1 n1 $_206 n0)) true = % 1.17/1.36 true % 1.17/1.36 |- ifeq (equalish $_205 $_205) true % 1.17/1.36 (f n1 $_205 n1 n0 n0 (sK1_relation_exists_F n1 $_205 n1 n0 n0)) true = % 1.17/1.36 true % 1.17/1.36 |- f n1 n0 n1 n0 n0 (sK1_relation_exists_F n1 n0 n1 n0 n0) = true % 1.17/1.36 |- ifeq (f $A $B $C $D $E (sK1_relation_exists_F n1 n0 n1 n0 n0)) true % 1.17/1.36 (equalish $A n1) true = true % 1.17/1.36 |- ifeq (f $F $G $H $I $J (sK1_relation_exists_F n1 n0 n1 n0 n0)) true % 1.17/1.36 (equalish n1 $F) true = true % 1.17/1.36 |- ifeq (f $A $B $C $D $E (sK1_relation_exists_F n1 n0 n1 n0 n0)) true % 1.17/1.36 (equalish $C n1) true = true % 1.17/1.36 |- ifeq (f $F $G $H $I $J (sK1_relation_exists_F n1 n0 n1 n0 n0)) true % 1.17/1.36 (equalish n1 $H) true = true % 1.17/1.36 |- ifeq (f $A $B $C $D $E (sK1_relation_exists_F n1 n0 n1 n0 n0)) true % 1.17/1.36 (equalish $E n0) true = true % 1.17/1.36 |- ifeq (f $F $G $H $I $J (sK1_relation_exists_F n1 n0 n1 n0 n0)) true % 1.17/1.36 (equalish n0 $J) true = true % 1.17/1.36 |- f n1 n1 n1 n0 n0 (sK1_relation_exists_F n1 n1 n1 n0 n0) = true % 1.17/1.36 |- ifeq (f $A $B $C $D $E (sK1_relation_exists_F n1 n1 n1 n0 n0)) true % 1.17/1.36 (equalish $A n1) true = true % 1.17/1.36 |- ifeq (f $F $G $H $I $J (sK1_relation_exists_F n1 n1 n1 n0 n0)) true % 1.17/1.36 (equalish n1 $F) true = true % 1.17/1.36 |- ifeq (f $A $B $C $D $E (sK1_relation_exists_F n1 n1 n1 n0 n0)) true % 1.17/1.36 (equalish $C n1) true = true % 1.17/1.36 |- ifeq (f $F $G $H $I $J (sK1_relation_exists_F n1 n1 n1 n0 n0)) true % 1.17/1.36 (equalish n1 $H) true = true % 1.17/1.36 |- ifeq (f $A $B $C $D $E (sK1_relation_exists_F n1 n1 n1 n0 n0)) true % 1.17/1.36 (equalish $E n0) true = true % 1.17/1.36 |- ifeq (f $F $G $H $I $J (sK1_relation_exists_F n1 n1 n1 n0 n0)) true % 1.17/1.36 (equalish n0 $J) true = true % 1.17/1.36 |- ifeq (equalish $_210 $_210) true % 1.17/1.36 (f $_210 n0 n1 n0 n0 (sK1_relation_exists_F $_210 n0 n1 n0 n0)) true = % 1.17/1.36 true % 1.17/1.36 |- ifeq (equalish $_213 $_213) true % 1.17/1.36 (f $_213 n1 n1 n0 n0 (sK1_relation_exists_F $_213 n1 n1 n0 n0)) true = % 1.17/1.36 true % 1.17/1.36 |- ifeq (equalish $_220 $_220) true % 1.17/1.36 (ifeq (equalish $_219 $_219) true % 1.17/1.36 (f n0 $_219 n1 n0 $_220 % 1.17/1.36 (sK1_relation_exists_F n0 $_219 n1 n0 $_220)) true) true = true % 1.17/1.36 |- ifeq (equalish $_220 $_220) true % 1.17/1.36 (ifeq (equalish $_219 $_219) true % 1.17/1.36 (f n1 $_219 n1 n0 $_220 % 1.17/1.36 (sK1_relation_exists_F n1 $_219 n1 n0 $_220)) true) true = true % 1.17/1.36 |- ifeq (equalish $_220 $_220) true % 1.17/1.36 (ifeq (equalish $_218 $_218) true % 1.17/1.36 (f $_218 n0 n1 n0 $_220 % 1.17/1.36 (sK1_relation_exists_F $_218 n0 n1 n0 $_220)) true) true = true % 1.17/1.36 |- ifeq (equalish $_220 $_220) true % 1.17/1.36 (ifeq (equalish $_218 $_218) true % 1.17/1.36 (f $_218 n1 n1 n0 $_220 % 1.17/1.36 (sK1_relation_exists_F $_218 n1 n1 n0 $_220)) true) true = true % 1.17/1.36 |- ifeq (equalish $_219 $_219) true % 1.17/1.36 (ifeq (equalish $_218 $_218) true % 1.17/1.36 (f $_218 $_219 n1 n0 n1 % 1.17/1.36 (sK1_relation_exists_F $_218 $_219 n1 n0 n1)) true) true = true % 1.17/1.36 |- ifeq (equalish $_222 $_222) true % 1.17/1.36 (f n0 n0 n1 n0 $_222 (sK1_relation_exists_F n0 n0 n1 n0 $_222)) true = % 1.17/1.36 true % 1.17/1.36 |- ifeq (equalish $_222 $_222) true % 1.17/1.36 (f n0 n1 n1 n0 $_222 (sK1_relation_exists_F n0 n1 n1 n0 $_222)) true = % 1.17/1.36 true % 1.17/1.36 |- ifeq (equalish $_221 $_221) true % 1.17/1.36 (f n0 $_221 n1 n0 n1 (sK1_relation_exists_F n0 $_221 n1 n0 n1)) true = % 1.17/1.36 true % 1.17/1.36 |- f n0 n0 n1 n0 n1 (sK1_relation_exists_F n0 n0 n1 n0 n1) = true % 1.17/1.36 |- ifeq (f $A $B $C $D $E (sK1_relation_exists_F n0 n0 n1 n0 n1)) true % 1.17/1.36 (equalish $A n0) true = true % 1.17/1.36 |- ifeq (f $F $G $H $I $J (sK1_relation_exists_F n0 n0 n1 n0 n1)) true % 1.17/1.36 (equalish n0 $F) true = true % 1.17/1.36 |- ifeq (f $A $B $C $D $E (sK1_relation_exists_F n0 n0 n1 n0 n1)) true % 1.17/1.36 (equalish $C n1) true = true % 1.17/1.36 |- ifeq (f $F $G $H $I $J (sK1_relation_exists_F n0 n0 n1 n0 n1)) true % 1.17/1.36 (equalish n1 $H) true = true % 1.17/1.36 |- ifeq (f $A $B $C $D $E (sK1_relation_exists_F n0 n0 n1 n0 n1)) true % 1.17/1.36 (equalish $E n1) true = true % 1.17/1.36 |- ifeq (f $F $G $H $I $J (sK1_relation_exists_F n0 n0 n1 n0 n1)) true % 1.17/1.36 (equalish n1 $J) true = true % 1.17/1.36 |- f n0 n1 n1 n0 n1 (sK1_relation_exists_F n0 n1 n1 n0 n1) = true % 1.17/1.36 |- ifeq (f $A $B $C $D $E (sK1_relation_exists_F n0 n1 n1 n0 n1)) true % 1.17/1.36 (equalish $A n0) true = true % 1.17/1.36 |- ifeq (f $F $G $H $I $J (sK1_relation_exists_F n0 n1 n1 n0 n1)) true % 1.17/1.36 (equalish n0 $F) true = true % 1.17/1.36 |- ifeq (f $A $B $C $D $E (sK1_relation_exists_F n0 n1 n1 n0 n1)) true % 1.17/1.36 (equalish $C n1) true = true % 1.17/1.36 |- ifeq (f $F $G $H $I $J (sK1_relation_exists_F n0 n1 n1 n0 n1)) true % 1.17/1.36 (equalish n1 $H) true = true % 1.17/1.36 |- ifeq (f $A $B $C $D $E (sK1_relation_exists_F n0 n1 n1 n0 n1)) true % 1.17/1.36 (equalish $E n1) true = true % 1.17/1.36 |- ifeq (f $F $G $H $I $J (sK1_relation_exists_F n0 n1 n1 n0 n1)) true % 1.17/1.36 (equalish n1 $J) true = true % 1.17/1.36 |- ifeq (equalish $_227 $_227) true % 1.17/1.36 (f n1 n0 n1 n0 $_227 (sK1_relation_exists_F n1 n0 n1 n0 $_227)) true = % 1.17/1.36 true % 1.17/1.36 |- ifeq (equalish $_227 $_227) true % 1.17/1.36 (f n1 n1 n1 n0 $_227 (sK1_relation_exists_F n1 n1 n1 n0 $_227)) true = % 1.17/1.36 true % 1.17/1.36 |- ifeq (equalish $_226 $_226) true % 1.17/1.36 (f n1 $_226 n1 n0 n1 (sK1_relation_exists_F n1 $_226 n1 n0 n1)) true = % 1.17/1.36 true % 1.17/1.36 |- f n1 n0 n1 n0 n1 (sK1_relation_exists_F n1 n0 n1 n0 n1) = true % 1.17/1.36 |- ifeq (f $A $B $C $D $E (sK1_relation_exists_F n1 n0 n1 n0 n1)) true % 1.17/1.36 (equalish $A n1) true = true % 1.17/1.36 |- ifeq (f $F $G $H $I $J (sK1_relation_exists_F n1 n0 n1 n0 n1)) true % 1.17/1.36 (equalish n1 $F) true = true % 1.17/1.36 |- ifeq (f $A $B $C $D $E (sK1_relation_exists_F n1 n0 n1 n0 n1)) true % 1.17/1.36 (equalish $C n1) true = true % 1.17/1.36 |- ifeq (f $F $G $H $I $J (sK1_relation_exists_F n1 n0 n1 n0 n1)) true % 1.17/1.36 (equalish n1 $H) true = true % 1.17/1.36 |- ifeq (f $A $B $C $D $E (sK1_relation_exists_F n1 n0 n1 n0 n1)) true % 1.17/1.36 (equalish $E n1) true = true % 1.17/1.36 |- ifeq (f $F $G $H $I $J (sK1_relation_exists_F n1 n0 n1 n0 n1)) true % 1.17/1.36 (equalish n1 $J) true = true % 1.17/1.36 |- f n1 n1 n1 n0 n1 (sK1_relation_exists_F n1 n1 n1 n0 n1) = true % 1.17/1.36 |- ifeq (f $A $B $C $D $E (sK1_relation_exists_F n1 n1 n1 n0 n1)) true % 1.17/1.36 (equalish $A n1) true = true % 1.17/1.36 |- ifeq (f $F $G $H $I $J (sK1_relation_exists_F n1 n1 n1 n0 n1)) true % 1.17/1.36 (equalish n1 $F) true = true % 1.17/1.36 |- ifeq (f $A $B $C $D $E (sK1_relation_exists_F n1 n1 n1 n0 n1)) true % 1.17/1.36 (equalish $C n1) true = true % 1.17/1.37 |- ifeq (f $F $G $H $I $J (sK1_relation_exists_F n1 n1 n1 n0 n1)) true % 1.17/1.37 (equalish n1 $H) true = true % 1.17/1.37 |- ifeq (f $A $B $C $D $E (sK1_relation_exists_F n1 n1 n1 n0 n1)) true % 1.17/1.37 (equalish $E n1) true = true % 1.17/1.37 |- ifeq (f $F $G $H $I $J (sK1_relation_exists_F n1 n1 n1 n0 n1)) true % 1.17/1.37 (equalish n1 $J) true = true % 1.17/1.37 |- ifeq (equalish $_231 $_231) true % 1.17/1.37 (f $_231 n0 n1 n0 n1 (sK1_relation_exists_F $_231 n0 n1 n0 n1)) true = % 1.17/1.37 true % 1.17/1.37 |- ifeq (equalish $_234 $_234) true % 1.17/1.37 (f $_234 n1 n1 n0 n1 (sK1_relation_exists_F $_234 n1 n1 n0 n1)) true = % 1.17/1.37 true % 1.17/1.37 |- ifeq (equalish $_241 $_241) true % 1.17/1.37 (ifeq (equalish $_240 $_240) true % 1.17/1.37 (f n0 $_240 n1 $_241 n1 % 1.17/1.37 (sK1_relation_exists_F n0 $_240 n1 $_241 n1)) true) true = true % 1.17/1.37 |- ifeq (equalish $_241 $_241) true % 1.17/1.37 (ifeq (equalish $_240 $_240) true % 1.17/1.37 (f n1 $_240 n1 $_241 n1 % 1.17/1.37 (sK1_relation_exists_F n1 $_240 n1 $_241 n1)) true) true = true % 1.17/1.37 |- ifeq (equalish $_241 $_241) true % 1.17/1.37 (ifeq (equalish $_239 $_239) true % 1.17/1.37 (f $_239 n0 n1 $_241 n1 % 1.17/1.37 (sK1_relation_exists_F $_239 n0 n1 $_241 n1)) true) true = true % 1.17/1.37 |- ifeq (equalish $_241 $_241) true % 1.17/1.37 (ifeq (equalish $_239 $_239) true % 1.17/1.37 (f $_239 n1 n1 $_241 n1 % 1.17/1.37 (sK1_relation_exists_F $_239 n1 n1 $_241 n1)) true) true = true % 1.17/1.37 |- ifeq (equalish $_243 $_243) true % 1.17/1.37 (f n0 n0 n1 $_243 n1 (sK1_relation_exists_F n0 n0 n1 $_243 n1)) true = % 1.17/1.37 true % 1.17/1.37 |- ifeq (equalish $_243 $_243) true % 1.17/1.37 (f n0 n1 n1 $_243 n1 (sK1_relation_exists_F n0 n1 n1 $_243 n1)) true = % 1.17/1.37 true % 1.17/1.37 |- ifeq (equalish $_247 $_247) true % 1.17/1.37 (f n1 n0 n1 $_247 n1 (sK1_relation_exists_F n1 n0 n1 $_247 n1)) true = % 1.17/1.37 true % 1.17/1.37 |- ifeq (equalish $_247 $_247) true % 1.17/1.37 (f n1 n1 n1 $_247 n1 (sK1_relation_exists_F n1 n1 n1 $_247 n1)) true = % 1.17/1.37 true % 1.17/1.37 |- ifeq (equalish $_254 $_254) true % 1.17/1.37 (ifeq (equalish $_253 $_253) true % 1.17/1.37 (ifeq (equalish $_252 $_252) true % 1.17/1.37 (f $_252 $_253 $_254 n0 n0 % 1.17/1.37 (sK1_relation_exists_F $_252 $_253 $_254 n0 n0)) true) true) % 1.17/1.37 true = true % 1.17/1.37 |- ifeq (equalish $_254 $_254) true % 1.17/1.37 (ifeq (equalish $_253 $_253) true % 1.17/1.37 (ifeq (equalish $_252 $_252) true % 1.17/1.37 (f $_252 $_253 $_254 n0 n1 % 1.17/1.37 (sK1_relation_exists_F $_252 $_253 $_254 n0 n1)) true) true) % 1.17/1.37 true = true % 1.17/1.37 |- ifeq (equalish $_258 $_258) true % 1.17/1.37 (ifeq (equalish $_257 $_257) true % 1.17/1.37 (f n0 $_257 $_258 n0 n1 % 1.17/1.37 (sK1_relation_exists_F n0 $_257 $_258 n0 n1)) true) true = true % 1.17/1.37 |- ifeq (equalish $_258 $_258) true % 1.17/1.37 (ifeq (equalish $_257 $_257) true % 1.17/1.37 (f n1 $_257 $_258 n0 n1 % 1.17/1.37 (sK1_relation_exists_F n1 $_257 $_258 n0 n1)) true) true = true % 1.17/1.37 |- ifeq (equalish $_258 $_258) true % 1.17/1.37 (ifeq (equalish $_256 $_256) true % 1.17/1.37 (f $_256 n0 $_258 n0 n1 % 1.17/1.37 (sK1_relation_exists_F $_256 n0 $_258 n0 n1)) true) true = true % 1.17/1.37 |- ifeq (equalish $_258 $_258) true % 1.17/1.37 (ifeq (equalish $_256 $_256) true % 1.17/1.37 (f $_256 n1 $_258 n0 n1 % 1.17/1.37 (sK1_relation_exists_F $_256 n1 $_258 n0 n1)) true) true = true % 1.17/1.37 |- ifeq (equalish $_260 $_260) true % 1.17/1.37 (f n1 n0 $_260 n0 n1 (sK1_relation_exists_F n1 n0 $_260 n0 n1)) true = % 1.17/1.37 true % 1.17/1.37 |- ifeq (equalish $_260 $_260) true % 1.17/1.37 (f n1 n1 $_260 n0 n1 (sK1_relation_exists_F n1 n1 $_260 n0 n1)) true = % 1.17/1.37 true % 1.17/1.37 |- ifeq (equalish $_264 $_264) true % 1.17/1.37 (f n0 n0 $_264 n0 n1 (sK1_relation_exists_F n0 n0 $_264 n0 n1)) true = % 1.17/1.37 true % 1.17/1.37 |- ifeq (equalish $_267 $_267) true % 1.17/1.37 (f n0 n1 $_267 n0 n1 (sK1_relation_exists_F n0 n1 $_267 n0 n1)) true = % 1.17/1.37 true % 1.17/1.37 |- ifeq (equalish $_271 $_271) true % 1.17/1.37 (ifeq (equalish $_270 $_270) true % 1.17/1.37 (f n0 $_270 $_271 n0 n0 % 1.17/1.37 (sK1_relation_exists_F n0 $_270 $_271 n0 n0)) true) true = true % 1.17/1.37 |- ifeq (equalish $_271 $_271) true % 1.17/1.37 (ifeq (equalish $_270 $_270) true % 1.17/1.37 (f n1 $_270 $_271 n0 n0 % 1.17/1.37 (sK1_relation_exists_F n1 $_270 $_271 n0 n0)) true) true = true % 1.17/1.37 |- ifeq (equalish $_271 $_271) true % 1.17/1.37 (ifeq (equalish $_269 $_269) true % 1.17/1.37 (f $_269 n0 $_271 n0 n0 % 1.17/1.37 (sK1_relation_exists_F $_269 n0 $_271 n0 n0)) true) true = true % 1.17/1.37 |- ifeq (equalish $_271 $_271) true % 1.17/1.37 (ifeq (equalish $_269 $_269) true % 1.17/1.37 (f $_269 n1 $_271 n0 n0 % 1.17/1.37 (sK1_relation_exists_F $_269 n1 $_271 n0 n0)) true) true = true % 1.17/1.37 |- ifeq (equalish $_273 $_273) true % 1.17/1.37 (f n0 n0 $_273 n0 n0 (sK1_relation_exists_F n0 n0 $_273 n0 n0)) true = % 1.17/1.37 true % 1.17/1.37 |- ifeq (equalish $_273 $_273) true % 1.17/1.37 (f n0 n1 $_273 n0 n0 (sK1_relation_exists_F n0 n1 $_273 n0 n0)) true = % 1.17/1.37 true % 1.17/1.37 |- ifeq (equalish $_277 $_277) true % 1.17/1.37 (f n1 n0 $_277 n0 n0 (sK1_relation_exists_F n1 n0 $_277 n0 n0)) true = % 1.17/1.37 true % 1.17/1.37 |- ifeq (equalish $_277 $_277) true % 1.17/1.37 (f n1 n1 $_277 n0 n0 (sK1_relation_exists_F n1 n1 $_277 n0 n0)) true = % 1.17/1.37 true % 1.17/1.37 |- ifeq (equalish $_286 $_286) true % 1.17/1.37 (ifeq (equalish $_285 $_285) true % 1.17/1.37 (ifeq (equalish $_284 $_284) true % 1.17/1.37 (f $_284 $_285 $_286 n1 n0 % 1.17/1.37 (sK1_relation_exists_F $_284 $_285 $_286 n1 n0)) true) true) % 1.17/1.37 true = true % 1.17/1.37 |- ifeq (equalish $_286 $_286) true % 1.17/1.37 (ifeq (equalish $_285 $_285) true % 1.17/1.37 (ifeq (equalish $_284 $_284) true % 1.17/1.37 (f $_284 $_285 $_286 n1 n1 % 1.17/1.37 (sK1_relation_exists_F $_284 $_285 $_286 n1 n1)) true) true) % 1.17/1.37 true = true % 1.17/1.37 |- ifeq (equalish $_290 $_290) true % 1.17/1.37 (ifeq (equalish $_289 $_289) true % 1.17/1.37 (f n0 $_289 $_290 n1 n0 % 1.17/1.37 (sK1_relation_exists_F n0 $_289 $_290 n1 n0)) true) true = true % 1.17/1.37 |- ifeq (equalish $_290 $_290) true % 1.17/1.37 (ifeq (equalish $_289 $_289) true % 1.17/1.37 (f n1 $_289 $_290 n1 n0 % 1.17/1.37 (sK1_relation_exists_F n1 $_289 $_290 n1 n0)) true) true = true % 1.17/1.37 |- ifeq (equalish $_290 $_290) true % 1.17/1.37 (ifeq (equalish $_288 $_288) true % 1.17/1.37 (f $_288 n0 $_290 n1 n0 % 1.17/1.37 (sK1_relation_exists_F $_288 n0 $_290 n1 n0)) true) true = true % 1.17/1.37 |- ifeq (equalish $_290 $_290) true % 1.17/1.37 (ifeq (equalish $_288 $_288) true % 1.17/1.37 (f $_288 n1 $_290 n1 n0 % 1.17/1.37 (sK1_relation_exists_F $_288 n1 $_290 n1 n0)) true) true = true % 1.17/1.37 |- ifeq (equalish $_292 $_292) true % 1.17/1.37 (f n0 n0 $_292 n1 n0 (sK1_relation_exists_F n0 n0 $_292 n1 n0)) true = % 1.17/1.37 true % 1.17/1.37 |- ifeq (equalish $_292 $_292) true % 1.17/1.37 (f n0 n1 $_292 n1 n0 (sK1_relation_exists_F n0 n1 $_292 n1 n0)) true = % 1.17/1.37 true % 1.17/1.37 |- ifeq (equalish $_296 $_296) true % 1.17/1.37 (f n1 n0 $_296 n1 n0 (sK1_relation_exists_F n1 n0 $_296 n1 n0)) true = % 1.17/1.37 true % 1.17/1.37 |- ifeq (equalish $_299 $_299) true % 1.17/1.37 (f n1 n1 $_299 n1 n0 (sK1_relation_exists_F n1 n1 $_299 n1 n0)) true = % 1.17/1.37 true % 1.17/1.37 |- ifeq (equalish $_303 $_303) true % 1.17/1.37 (ifeq (equalish $_302 $_302) true % 1.17/1.37 (f n0 $_302 $_303 n1 n1 % 1.17/1.37 (sK1_relation_exists_F n0 $_302 $_303 n1 n1)) true) true = true % 1.17/1.37 |- ifeq (equalish $_303 $_303) true % 1.17/1.37 (ifeq (equalish $_302 $_302) true % 1.17/1.37 (f n1 $_302 $_303 n1 n1 % 1.17/1.37 (sK1_relation_exists_F n1 $_302 $_303 n1 n1)) true) true = true % 1.17/1.37 |- ifeq (equalish $_303 $_303) true % 1.17/1.37 (ifeq (equalish $_301 $_301) true % 1.17/1.37 (f $_301 n0 $_303 n1 n1 % 1.17/1.37 (sK1_relation_exists_F $_301 n0 $_303 n1 n1)) true) true = true % 1.17/1.37 |- ifeq (equalish $_303 $_303) true % 1.17/1.37 (ifeq (equalish $_301 $_301) true % 1.17/1.37 (f $_301 n1 $_303 n1 n1 % 1.17/1.37 (sK1_relation_exists_F $_301 n1 $_303 n1 n1)) true) true = true % 1.17/1.37 |- ifeq (equalish $_305 $_305) true % 1.17/1.37 (f n0 n0 $_305 n1 n1 (sK1_relation_exists_F n0 n0 $_305 n1 n1)) true = % 1.17/1.37 true % 1.17/1.37 |- ifeq (equalish $_305 $_305) true % 1.17/1.37 (f n0 n1 $_305 n1 n1 (sK1_relation_exists_F n0 n1 $_305 n1 n1)) true = % 1.17/1.37 true % 1.17/1.37 |- ifeq (equalish $_309 $_309) true % 1.17/1.37 (f n1 n0 $_309 n1 n1 (sK1_relation_exists_F n1 n0 $_309 n1 n1)) true = % 1.17/1.37 true % 1.17/1.37 |- ifeq (equalish $_309 $_309) true % 1.17/1.37 (f n1 n1 $_309 n1 n1 (sK1_relation_exists_F n1 n1 $_309 n1 n1)) true = % 1.17/1.37 true % 1.17/1.37 |- ifeq (equalish $_881 $_881) true % 1.17/1.37 (ifeq (equalish $_880 $_880) true % 1.17/1.37 (f n0 n0 n0 $_880 $_881 % 1.17/1.37 (sK1_relation_exists_F n0 n0 n0 $_880 $_881)) true) true = true % 1.17/1.37 |- ifeq (equalish $_881 $_881) true % 1.17/1.37 (ifeq (equalish $_880 $_880) true % 1.17/1.37 (f n1 n0 n0 $_880 $_881 % 1.17/1.37 (sK1_relation_exists_F n1 n0 n0 $_880 $_881)) true) true = true % 1.17/1.37 |- ifeq (equalish $_888 $_888) true % 1.17/1.37 (ifeq (equalish $_887 $_887) true % 1.17/1.37 (f n0 n0 $_887 n0 $_888 % 1.17/1.37 (sK1_relation_exists_F n0 n0 $_887 n0 $_888)) true) true = true % 1.17/1.37 |- ifeq (equalish $_888 $_888) true % 1.17/1.37 (ifeq (equalish $_887 $_887) true % 1.17/1.37 (f n1 n0 $_887 n0 $_888 % 1.17/1.37 (sK1_relation_exists_F n1 n0 $_887 n0 $_888)) true) true = true % 1.17/1.37 |- ifeq (equalish $_895 $_895) true % 1.17/1.37 (ifeq (equalish $_894 $_894) true % 1.17/1.37 (f n0 n0 $_894 $_895 n1 % 1.17/1.37 (sK1_relation_exists_F n0 n0 $_894 $_895 n1)) true) true = true % 1.17/1.37 |- ifeq (equalish $_895 $_895) true % 1.17/1.37 (ifeq (equalish $_894 $_894) true % 1.17/1.37 (f n1 n0 $_894 $_895 n1 % 1.17/1.37 (sK1_relation_exists_F n1 n0 $_894 $_895 n1)) true) true = true % 1.17/1.37 |- ifeq (equalish $_902 $_902) true % 1.17/1.37 (ifeq (equalish $_901 $_901) true % 1.17/1.37 (f n0 n1 n0 $_901 $_902 % 1.17/1.37 (sK1_relation_exists_F n0 n1 n0 $_901 $_902)) true) true = true % 1.17/1.37 |- ifeq (equalish $_902 $_902) true % 1.17/1.37 (ifeq (equalish $_901 $_901) true % 1.17/1.37 (f n1 n1 n0 $_901 $_902 % 1.17/1.37 (sK1_relation_exists_F n1 n1 n0 $_901 $_902)) true) true = true % 1.17/1.37 |- ifeq (equalish $_907 $_907) true % 1.17/1.37 (ifeq (equalish $_906 $_906) true % 1.17/1.37 (f n0 n1 n1 $_906 $_907 % 1.17/1.37 (sK1_relation_exists_F n0 n1 n1 $_906 $_907)) true) true = true % 1.17/1.37 |- ifeq (equalish $_907 $_907) true % 1.17/1.37 (ifeq (equalish $_906 $_906) true % 1.17/1.37 (f n1 n1 n1 $_906 $_907 % 1.17/1.37 (sK1_relation_exists_F n1 n1 n1 $_906 $_907)) true) true = true % 1.17/1.37 |- ifeq (equalish $_914 $_914) true % 1.17/1.37 (ifeq (equalish $_913 $_913) true % 1.17/1.37 (f n0 n1 $_913 n1 $_914 % 1.17/1.37 (sK1_relation_exists_F n0 n1 $_913 n1 $_914)) true) true = true % 1.17/1.37 |- ifeq (equalish $_914 $_914) true % 1.17/1.37 (ifeq (equalish $_913 $_913) true % 1.17/1.37 (f n1 n1 $_913 n1 $_914 % 1.17/1.37 (sK1_relation_exists_F n1 n1 $_913 n1 $_914)) true) true = true % 1.17/1.37 |- ifeq (f $_922 $_923 $_924 n0 $_926 $_927) true % 1.17/1.37 (ifeq (f $_917 $_918 $_919 n0 $_921 $_927) true true true) true = true % 1.17/1.37 |- ifeq (f $_922 $_923 $_924 n1 $_926 $_927) true % 1.17/1.37 (ifeq (f $_917 $_918 $_919 n1 $_921 $_927) true true true) true = true % 1.17/1.37 |- ifeq % 1.17/1.37 (f $_922 $_923 $_924 $_925 $_926 % 1.17/1.37 (sK1_relation_exists_F n0 n0 n0 n0 n0)) true (equalish n0 $_925) % 1.17/1.37 true = true % 1.17/1.37 |- ifeq % 1.17/1.37 (f $_922 $_923 $_924 $_925 $_926 % 1.17/1.37 (sK1_relation_exists_F n0 n0 n0 n0 n1)) true (equalish n0 $_925) % 1.17/1.37 true = true % 1.17/1.37 |- ifeq % 1.17/1.37 (f $_922 $_923 $_924 $_925 $_926 % 1.17/1.37 (sK1_relation_exists_F n0 n0 n0 n1 n0)) true (equalish n1 $_925) % 1.17/1.37 true = true % 1.17/1.37 |- ifeq % 1.17/1.37 (f $_922 $_923 $_924 $_925 $_926 % 1.17/1.37 (sK1_relation_exists_F n0 n0 n0 n1 n1)) true (equalish n1 $_925) % 1.17/1.37 true = true % 1.17/1.37 |- ifeq % 1.17/1.37 (f $_922 $_923 $_924 $_925 $_926 % 1.17/1.37 (sK1_relation_exists_F n0 n0 n1 n0 n0)) true (equalish n0 $_925) % 1.17/1.37 true = true % 1.17/1.37 |- ifeq % 1.17/1.37 (f $_922 $_923 $_924 $_925 $_926 % 1.17/1.37 (sK1_relation_exists_F n0 n0 n1 n0 n1)) true (equalish n0 $_925) % 1.17/1.37 true = true % 1.17/1.37 |- ifeq % 1.17/1.37 (f $_922 $_923 $_924 $_925 $_926 % 1.17/1.37 (sK1_relation_exists_F n0 n0 n1 n1 n0)) true (equalish n1 $_925) % 1.17/1.37 true = true % 1.17/1.37 |- ifeq % 1.17/1.37 (f $_922 $_923 $_924 $_925 $_926 % 1.17/1.37 (sK1_relation_exists_F n0 n0 n1 n1 n1)) true (equalish n1 $_925) % 1.17/1.37 true = true % 1.17/1.37 |- ifeq % 1.17/1.37 (f $_922 $_923 $_924 $_925 $_926 % 1.17/1.37 (sK1_relation_exists_F n0 n1 n0 n0 n0)) true (equalish n0 $_925) % 1.17/1.37 true = true % 1.17/1.37 |- ifeq % 1.17/1.37 (f $_922 $_923 $_924 $_925 $_926 % 1.17/1.37 (sK1_relation_exists_F n0 n1 n0 n0 n1)) true (equalish n0 $_925) % 1.17/1.37 true = true % 1.17/1.37 |- ifeq % 1.17/1.37 (f $_922 $_923 $_924 $_925 $_926 % 1.17/1.37 (sK1_relation_exists_F n0 n1 n0 n1 n0)) true (equalish n1 $_925) % 1.17/1.37 true = true % 1.17/1.37 |- ifeq % 1.17/1.37 (f $_922 $_923 $_924 $_925 $_926 % 1.17/1.37 (sK1_relation_exists_F n0 n1 n0 n1 n1)) true (equalish n1 $_925) % 1.17/1.37 true = true % 1.17/1.37 |- ifeq % 1.17/1.37 (f $_922 $_923 $_924 $_925 $_926 % 1.17/1.37 (sK1_relation_exists_F n0 n1 n1 n0 n0)) true (equalish n0 $_925) % 1.17/1.37 true = true % 1.17/1.37 |- ifeq % 1.17/1.37 (f $_922 $_923 $_924 $_925 $_926 % 1.17/1.37 (sK1_relation_exists_F n0 n1 n1 n0 n1)) true (equalish n0 $_925) % 1.17/1.37 true = true % 1.17/1.37 |- ifeq % 1.17/1.37 (f $_922 $_923 $_924 $_925 $_926 % 1.17/1.37 (sK1_relation_exists_F n0 n1 n1 n1 n0)) true (equalish n1 $_925) % 1.17/1.37 true = true % 1.17/1.37 |- ifeq % 1.17/1.37 (f $_922 $_923 $_924 $_925 $_926 % 1.17/1.37 (sK1_relation_exists_F n0 n1 n1 n1 n1)) true (equalish n1 $_925) % 1.17/1.37 true = true % 1.17/1.37 |- ifeq % 1.17/1.37 (f $_922 $_923 $_924 $_925 $_926 % 1.17/1.37 (sK1_relation_exists_F n1 n0 n0 n0 n0)) true (equalish n0 $_925) % 1.17/1.37 true = true % 1.17/1.37 |- ifeq % 1.17/1.37 (f $_922 $_923 $_924 $_925 $_926 % 1.17/1.37 (sK1_relation_exists_F n1 n0 n0 n0 n1)) true (equalish n0 $_925) % 1.17/1.37 true = true % 1.17/1.37 |- ifeq % 1.17/1.37 (f $_922 $_923 $_924 $_925 $_926 % 1.17/1.37 (sK1_relation_exists_F n1 n0 n0 n1 n0)) true (equalish n1 $_925) % 1.17/1.37 true = true % 1.17/1.37 |- ifeq % 1.17/1.37 (f $_922 $_923 $_924 $_925 $_926 % 1.17/1.37 (sK1_relation_exists_F n1 n0 n0 n1 n1)) true (equalish n1 $_925) % 1.17/1.37 true = true % 1.17/1.37 |- ifeq % 1.17/1.37 (f $_922 $_923 $_924 $_925 $_926 % 1.17/1.37 (sK1_relation_exists_F n1 n0 n1 n0 n0)) true (equalish n0 $_925) % 1.17/1.37 true = true % 1.17/1.37 |- ifeq % 1.17/1.37 (f $_922 $_923 $_924 $_925 $_926 % 1.17/1.37 (sK1_relation_exists_F n1 n0 n1 n0 n1)) true (equalish n0 $_925) % 1.17/1.37 true = true % 1.17/1.37 |- ifeq % 1.17/1.37 (f $_922 $_923 $_924 $_925 $_926 % 1.17/1.37 (sK1_relation_exists_F n1 n0 n1 n1 n0)) true (equalish n1 $_925) % 1.17/1.37 true = true % 1.17/1.37 |- ifeq % 1.17/1.37 (f $_922 $_923 $_924 $_925 $_926 % 1.17/1.37 (sK1_relation_exists_F n1 n0 n1 n1 n1)) true (equalish n1 $_925) % 1.17/1.37 true = true % 1.17/1.37 |- ifeq % 1.17/1.37 (f $_922 $_923 $_924 $_925 $_926 % 1.17/1.37 (sK1_relation_exists_F n1 n1 n0 n0 n0)) true (equalish n0 $_925) % 1.17/1.37 true = true % 1.17/1.37 |- ifeq % 1.17/1.37 (f $_922 $_923 $_924 $_925 $_926 % 1.17/1.37 (sK1_relation_exists_F n1 n1 n0 n0 n1)) true (equalish n0 $_925) % 1.17/1.37 true = true % 1.17/1.37 |- ifeq % 1.17/1.37 (f $_922 $_923 $_924 $_925 $_926 % 1.17/1.37 (sK1_relation_exists_F n1 n1 n0 n1 n0)) true (equalish n1 $_925) % 1.17/1.37 true = true % 1.17/1.37 |- ifeq % 1.17/1.37 (f $_922 $_923 $_924 $_925 $_926 % 1.17/1.37 (sK1_relation_exists_F n1 n1 n0 n1 n1)) true (equalish n1 $_925) % 1.17/1.37 true = true % 1.17/1.37 |- ifeq % 1.17/1.37 (f $_922 $_923 $_924 $_925 $_926 % 1.17/1.37 (sK1_relation_exists_F n1 n1 n1 n0 n0)) true (equalish n0 $_925) % 1.17/1.37 true = true % 1.17/1.37 |- ifeq % 1.17/1.37 (f $_922 $_923 $_924 $_925 $_926 % 1.17/1.37 (sK1_relation_exists_F n1 n1 n1 n0 n1)) true (equalish n0 $_925) % 1.17/1.37 true = true % 1.17/1.37 |- ifeq % 1.17/1.37 (f $_922 $_923 $_924 $_925 $_926 % 1.17/1.37 (sK1_relation_exists_F n1 n1 n1 n1 n0)) true (equalish n1 $_925) % 1.17/1.37 true = true % 1.17/1.37 |- ifeq % 1.17/1.37 (f $_922 $_923 $_924 $_925 $_926 % 1.17/1.37 (sK1_relation_exists_F n1 n1 n1 n1 n1)) true (equalish n1 $_925) % 1.17/1.37 true = true % 1.17/1.37 |- ifeq % 1.17/1.37 (f $_917 $_918 $_919 $_920 $_921 % 1.17/1.37 (sK1_relation_exists_F n0 n0 n0 n0 n0)) true (equalish $_920 n0) % 1.17/1.37 true = true % 1.17/1.37 |- ifeq % 1.17/1.37 (f $_917 $_918 $_919 $_920 $_921 % 1.17/1.37 (sK1_relation_exists_F n0 n0 n0 n0 n1)) true (equalish $_920 n0) % 1.17/1.37 true = true % 1.17/1.37 |- ifeq % 1.17/1.37 (f $_917 $_918 $_919 $_920 $_921 % 1.17/1.37 (sK1_relation_exists_F n0 n0 n0 n1 n0)) true (equalish $_920 n1) % 1.17/1.37 true = true % 1.17/1.37 |- ifeq % 1.17/1.37 (f $_917 $_918 $_919 $_920 $_921 % 1.17/1.37 (sK1_relation_exists_F n0 n0 n0 n1 n1)) true (equalish $_920 n1) % 1.17/1.37 true = true % 1.17/1.37 |- ifeq % 1.17/1.37 (f $_917 $_918 $_919 $_920 $_921 % 1.17/1.37 (sK1_relation_exists_F n0 n0 n1 n0 n0)) true (equalish $_920 n0) % 1.17/1.37 true = true % 1.17/1.37 |- ifeq % 1.17/1.37 (f $_917 $_918 $_919 $_920 $_921 % 1.17/1.37 (sK1_relation_exists_F n0 n0 n1 n0 n1)) true (equalish $_920 n0) % 1.17/1.37 true = true % 1.17/1.37 |- ifeq % 1.17/1.37 (f $_917 $_918 $_919 $_920 $_921 % 1.17/1.37 (sK1_relation_exists_F n0 n0 n1 n1 n0)) true (equalish $_920 n1) % 1.17/1.37 true = true % 1.17/1.37 |- ifeq % 1.17/1.37 (f $_917 $_918 $_919 $_920 $_921 % 1.17/1.37 (sK1_relation_exists_F n0 n0 n1 n1 n1)) true (equalish $_920 n1) % 1.17/1.37 true = true % 1.17/1.37 |- ifeq % 1.17/1.37 (f $_917 $_918 $_919 $_920 $_921 % 1.17/1.37 (sK1_relation_exists_F n0 n1 n0 n0 n0)) true (equalish $_920 n0) % 1.17/1.37 true = true % 1.17/1.37 |- ifeq % 1.17/1.37 (f $_917 $_918 $_919 $_920 $_921 % 1.17/1.37 (sK1_relation_exists_F n0 n1 n0 n0 n1)) true (equalish $_920 n0) % 1.17/1.37 true = true % 1.17/1.37 |- ifeq % 1.17/1.37 (f $_917 $_918 $_919 $_920 $_921 % 1.17/1.37 (sK1_relation_exists_F n0 n1 n0 n1 n0)) true (equalish $_920 n1) % 1.17/1.37 true = true % 1.17/1.37 |- ifeq % 1.17/1.37 (f $_917 $_918 $_919 $_920 $_921 % 1.17/1.37 (sK1_relation_exists_F n0 n1 n0 n1 n1)) true (equalish $_920 n1) % 1.17/1.37 true = true % 1.17/1.37 |- ifeq % 1.17/1.37 (f $_917 $_918 $_919 $_920 $_921 % 1.17/1.37 (sK1_relation_exists_F n0 n1 n1 n0 n0)) true (equalish $_920 n0) % 1.17/1.37 true = true % 1.17/1.37 |- ifeq % 1.17/1.37 (f $_917 $_918 $_919 $_920 $_921 % 1.17/1.37 (sK1_relation_exists_F n0 n1 n1 n0 n1)) true (equalish $_920 n0) % 1.17/1.37 true = true % 1.17/1.37 |- ifeq % 1.17/1.37 (f $_917 $_918 $_919 $_920 $_921 % 1.17/1.37 (sK1_relation_exists_F n0 n1 n1 n1 n0)) true (equalish $_920 n1) % 1.17/1.37 true = true % 1.17/1.37 |- ifeq % 1.17/1.37 (f $_917 $_918 $_919 $_920 $_921 % 1.17/1.37 (sK1_relation_exists_F n0 n1 n1 n1 n1)) true (equalish $_920 n1) % 1.17/1.37 true = true % 1.17/1.37 |- ifeq % 1.17/1.37 (f $_917 $_918 $_919 $_920 $_921 % 1.17/1.37 (sK1_relation_exists_F n1 n0 n0 n0 n0)) true (equalish $_920 n0) % 1.17/1.37 true = true % 1.17/1.37 |- ifeq % 1.17/1.37 (f $_917 $_918 $_919 $_920 $_921 % 1.17/1.37 (sK1_relation_exists_F n1 n0 n0 n0 n1)) true (equalish $_920 n0) % 1.17/1.37 true = true % 1.17/1.37 |- ifeq % 1.17/1.37 (f $_917 $_918 $_919 $_920 $_921 % 1.17/1.37 (sK1_relation_exists_F n1 n0 n0 n1 n0)) true (equalish $_920 n1) % 1.17/1.37 true = true % 1.17/1.37 |- ifeq % 1.17/1.37 (f $_917 $_918 $_919 $_920 $_921 % 1.17/1.37 (sK1_relation_exists_F n1 n0 n0 n1 n1)) true (equalish $_920 n1) % 1.17/1.37 true = true % 1.17/1.37 |- ifeq % 1.17/1.37 (f $_917 $_918 $_919 $_920 $_921 % 1.17/1.37 (sK1_relation_exists_F n1 n0 n1 n0 n0)) true (equalish $_920 n0) % 1.17/1.37 true = true % 1.17/1.37 |- ifeq % 1.17/1.37 (f $_917 $_918 $_919 $_920 $_921 % 1.17/1.37 (sK1_relation_exists_F n1 n0 n1 n0 n1)) true (equalish $_920 n0) % 1.17/1.37 true = true % 1.17/1.37 |- ifeq % 1.17/1.37 (f $_917 $_918 $_919 $_920 $_921 % 1.17/1.37 (sK1_relation_exists_F n1 n0 n1 n1 n0)) true (equalish $_920 n1) % 1.17/1.37 true = true % 1.17/1.37 |- ifeq % 1.17/1.37 (f $_917 $_918 $_919 $_920 $_921 % 1.17/1.37 (sK1_relation_exists_F n1 n0 n1 n1 n1)) true (equalish $_920 n1) % 1.17/1.37 true = true % 1.17/1.37 |- ifeq % 1.17/1.37 (f $_917 $_918 $_919 $_920 $_921 % 1.17/1.37 (sK1_relation_exists_F n1 n1 n0 n0 n0)) true (equalish $_920 n0) % 1.17/1.37 true = true % 1.17/1.37 |- ifeq % 1.17/1.37 (f $_917 $_918 $_919 $_920 $_921 % 1.17/1.37 (sK1_relation_exists_F n1 n1 n0 n0 n1)) true (equalish $_920 n0) % 1.17/1.37 true = true % 1.17/1.37 |- ifeq % 1.17/1.37 (f $_917 $_918 $_919 $_920 $_921 % 1.17/1.37 (sK1_relation_exists_F n1 n1 n0 n1 n0)) true (equalish $_920 n1) % 1.17/1.37 true = true % 1.17/1.37 |- ifeq % 1.17/1.37 (f $_917 $_918 $_919 $_920 $_921 % 1.17/1.37 (sK1_relation_exists_F n1 n1 n0 n1 n1)) true (equalish $_920 n1) % 1.17/1.37 true = true % 1.17/1.38 |- ifeq % 1.17/1.38 (f $_917 $_918 $_919 $_920 $_921 % 1.17/1.38 (sK1_relation_exists_F n1 n1 n1 n0 n0)) true (equalish $_920 n0) % 1.17/1.38 true = true % 1.17/1.38 |- ifeq % 1.17/1.38 (f $_917 $_918 $_919 $_920 $_921 % 1.17/1.38 (sK1_relation_exists_F n1 n1 n1 n0 n1)) true (equalish $_920 n0) % 1.17/1.38 true = true % 1.17/1.38 |- ifeq % 1.17/1.38 (f $_917 $_918 $_919 $_920 $_921 % 1.17/1.38 (sK1_relation_exists_F n1 n1 n1 n1 n0)) true (equalish $_920 n1) % 1.17/1.38 true = true % 1.17/1.38 |- ifeq % 1.17/1.38 (f $_917 $_918 $_919 $_920 $_921 % 1.17/1.38 (sK1_relation_exists_F n1 n1 n1 n1 n1)) true (equalish $_920 n1) % 1.17/1.38 true = true % 1.17/1.38 |- ifeq (f $F $G $H $I $J (sK1_relation_exists_F n0 n0 n0 n1 n0)) true true % 1.17/1.38 true = true % 1.17/1.38 |- ifeq (f $F $G $H $I $J (sK1_relation_exists_F n0 n0 n1 n0 n0)) true true % 1.17/1.38 true = true % 1.17/1.38 |- ifeq (f $F $G $H $I $J (sK1_relation_exists_F n0 n0 n1 n0 n1)) true true % 1.17/1.38 true = true % 1.17/1.38 |- ifeq (f $F $G $H $I $J (sK1_relation_exists_F n0 n0 n1 n1 n1)) true true % 1.17/1.38 true = true % 1.17/1.38 |- ifeq (f $F $G $H $I $J (sK1_relation_exists_F n0 n1 n0 n1 n0)) true true % 1.17/1.38 true = true % 1.17/1.38 |- ifeq (f $F $G $H $I $J (sK1_relation_exists_F n0 n1 n1 n0 n0)) true true % 1.17/1.38 true = true % 1.17/1.38 |- ifeq (f $F $G $H $I $J (sK1_relation_exists_F n0 n1 n1 n0 n1)) true true % 1.17/1.38 true = true % 1.17/1.38 |- ifeq (f $F $G $H $I $J (sK1_relation_exists_F n0 n1 n1 n1 n1)) true true % 1.17/1.38 true = true % 1.17/1.38 |- ifeq (f $F $G $H $I $J (sK1_relation_exists_F n1 n0 n0 n1 n0)) true true % 1.17/1.38 true = true % 1.17/1.38 |- ifeq (f $F $G $H $I $J (sK1_relation_exists_F n1 n0 n1 n0 n0)) true true % 1.17/1.38 true = true % 1.17/1.38 |- ifeq (f $F $G $H $I $J (sK1_relation_exists_F n1 n0 n1 n0 n1)) true true % 1.17/1.38 true = true % 1.17/1.38 |- ifeq (f $F $G $H $I $J (sK1_relation_exists_F n1 n0 n1 n1 n1)) true true % 1.17/1.38 true = true % 1.17/1.38 |- ifeq (f $F $G $H $I $J (sK1_relation_exists_F n1 n1 n0 n1 n0)) true true % 1.17/1.38 true = true % 1.17/1.38 |- ifeq (f $F $G $H $I $J (sK1_relation_exists_F n1 n1 n1 n0 n0)) true true % 1.17/1.38 true = true % 1.17/1.38 |- ifeq (f $F $G $H $I $J (sK1_relation_exists_F n1 n1 n1 n0 n1)) true true % 1.17/1.38 true = true % 1.17/1.38 |- ifeq (f $F $G $H $I $J (sK1_relation_exists_F n1 n1 n1 n1 n1)) true true % 1.17/1.38 true = true % 1.17/1.38 |- ifeq (f $F $G $H $I $J (sK1_relation_exists_F n0 n0 n0 n0 n0)) true true % 1.17/1.38 true = true % 1.17/1.38 |- ifeq (f $F $G $H $I $J (sK1_relation_exists_F n0 n0 n0 n0 n1)) true true % 1.17/1.38 true = true % 1.17/1.38 |- ifeq (f $F $G $H $I $J (sK1_relation_exists_F n0 n0 n0 n1 n1)) true true % 1.17/1.38 true = true % 1.17/1.38 |- ifeq (f $F $G $H $I $J (sK1_relation_exists_F n0 n0 n1 n1 n0)) true true % 1.17/1.38 true = true % 1.17/1.38 |- ifeq (f $F $G $H $I $J (sK1_relation_exists_F n0 n1 n0 n0 n0)) true true % 1.17/1.38 true = true % 1.17/1.38 |- ifeq (f $F $G $H $I $J (sK1_relation_exists_F n0 n1 n0 n0 n1)) true true % 1.17/1.38 true = true % 1.17/1.38 |- ifeq (f $F $G $H $I $J (sK1_relation_exists_F n0 n1 n0 n1 n1)) true true % 1.17/1.38 true = true % 1.17/1.38 |- ifeq (f $F $G $H $I $J (sK1_relation_exists_F n0 n1 n1 n1 n0)) true true % 1.17/1.38 true = true % 1.17/1.38 |- ifeq (f $F $G $H $I $J (sK1_relation_exists_F n1 n0 n0 n0 n0)) true true % 1.17/1.38 true = true % 1.17/1.38 |- ifeq (f $F $G $H $I $J (sK1_relation_exists_F n1 n0 n0 n0 n1)) true true % 1.17/1.38 true = true % 1.17/1.38 |- ifeq (f $F $G $H $I $J (sK1_relation_exists_F n1 n0 n0 n1 n1)) true true % 1.17/1.38 true = true % 1.17/1.38 |- ifeq (f $F $G $H $I $J (sK1_relation_exists_F n1 n0 n1 n1 n0)) true true % 1.17/1.38 true = true % 1.17/1.38 |- ifeq (f $F $G $H $I $J (sK1_relation_exists_F n1 n1 n0 n0 n0)) true true % 1.17/1.38 true = true % 1.17/1.38 |- ifeq (f $F $G $H $I $J (sK1_relation_exists_F n1 n1 n0 n0 n1)) true true % 1.17/1.38 true = true % 1.17/1.38 |- ifeq (f $F $G $H $I $J (sK1_relation_exists_F n1 n1 n0 n1 n1)) true true % 1.17/1.38 true = true % 1.17/1.38 |- ifeq (f $F $G $H $I $J (sK1_relation_exists_F n1 n1 n1 n1 n0)) true true % 1.17/1.38 true = true % 1.17/1.38 |- ifeq (f $_1413 n0 $_1415 $_1416 $_1417 $_1418) true % 1.17/1.38 (ifeq (f $_1408 n0 $_1410 $_1411 $_1412 $_1418) true true true) true = % 1.17/1.38 true % 1.17/1.38 |- ifeq (f $_1413 n1 $_1415 $_1416 $_1417 $_1418) true % 1.17/1.38 (ifeq (f $_1408 n1 $_1410 $_1411 $_1412 $_1418) true true true) true = % 1.17/1.38 true % 1.17/1.38 |- ifeq % 1.17/1.38 (f $_1413 $_1414 $_1415 $_1416 $_1417 % 1.17/1.38 (sK1_relation_exists_F n0 n0 n0 n0 n0)) true (equalish n0 $_1414) % 1.17/1.38 true = true % 1.17/1.38 |- ifeq % 1.17/1.38 (f $_1413 $_1414 $_1415 $_1416 $_1417 % 1.17/1.38 (sK1_relation_exists_F n0 n0 n0 n0 n1)) true (equalish n0 $_1414) % 1.17/1.38 true = true % 1.17/1.38 |- ifeq % 1.17/1.38 (f $_1413 $_1414 $_1415 $_1416 $_1417 % 1.17/1.38 (sK1_relation_exists_F n0 n0 n0 n1 n0)) true (equalish n0 $_1414) % 1.17/1.38 true = true % 1.17/1.38 |- ifeq % 1.17/1.38 (f $_1413 $_1414 $_1415 $_1416 $_1417 % 1.17/1.38 (sK1_relation_exists_F n0 n0 n0 n1 n1)) true (equalish n0 $_1414) % 1.17/1.38 true = true % 1.17/1.38 |- ifeq % 1.17/1.38 (f $_1413 $_1414 $_1415 $_1416 $_1417 % 1.17/1.38 (sK1_relation_exists_F n0 n0 n1 n0 n0)) true (equalish n0 $_1414) % 1.17/1.38 true = true % 1.17/1.38 |- ifeq % 1.17/1.38 (f $_1413 $_1414 $_1415 $_1416 $_1417 % 1.17/1.38 (sK1_relation_exists_F n0 n0 n1 n0 n1)) true (equalish n0 $_1414) % 1.17/1.38 true = true % 1.17/1.38 |- ifeq % 1.17/1.38 (f $_1413 $_1414 $_1415 $_1416 $_1417 % 1.17/1.38 (sK1_relation_exists_F n0 n0 n1 n1 n0)) true (equalish n0 $_1414) % 1.17/1.38 true = true % 1.17/1.38 |- ifeq % 1.17/1.38 (f $_1413 $_1414 $_1415 $_1416 $_1417 % 1.17/1.38 (sK1_relation_exists_F n0 n0 n1 n1 n1)) true (equalish n0 $_1414) % 1.17/1.38 true = true % 1.17/1.38 |- ifeq % 1.17/1.38 (f $_1413 $_1414 $_1415 $_1416 $_1417 % 1.17/1.38 (sK1_relation_exists_F n0 n1 n0 n0 n0)) true (equalish n1 $_1414) % 1.17/1.38 true = true % 1.17/1.38 |- ifeq % 1.17/1.38 (f $_1413 $_1414 $_1415 $_1416 $_1417 % 1.17/1.38 (sK1_relation_exists_F n0 n1 n0 n0 n1)) true (equalish n1 $_1414) % 1.17/1.38 true = true % 1.17/1.38 |- ifeq % 1.17/1.38 (f $_1413 $_1414 $_1415 $_1416 $_1417 % 1.17/1.38 (sK1_relation_exists_F n0 n1 n0 n1 n0)) true (equalish n1 $_1414) % 1.17/1.38 true = true % 1.17/1.38 |- ifeq % 1.17/1.38 (f $_1413 $_1414 $_1415 $_1416 $_1417 % 1.17/1.38 (sK1_relation_exists_F n0 n1 n0 n1 n1)) true (equalish n1 $_1414) % 1.17/1.38 true = true % 1.17/1.38 |- ifeq % 1.17/1.38 (f $_1413 $_1414 $_1415 $_1416 $_1417 % 1.17/1.38 (sK1_relation_exists_F n0 n1 n1 n0 n0)) true (equalish n1 $_1414) % 1.17/1.38 true = true % 1.17/1.38 |- ifeq % 1.17/1.38 (f $_1413 $_1414 $_1415 $_1416 $_1417 % 1.17/1.38 (sK1_relation_exists_F n0 n1 n1 n0 n1)) true (equalish n1 $_1414) % 1.17/1.38 true = true % 1.17/1.38 |- ifeq % 1.17/1.38 (f $_1413 $_1414 $_1415 $_1416 $_1417 % 1.17/1.38 (sK1_relation_exists_F n0 n1 n1 n1 n0)) true (equalish n1 $_1414) % 1.17/1.38 true = true % 1.17/1.38 |- ifeq % 1.17/1.38 (f $_1413 $_1414 $_1415 $_1416 $_1417 % 1.17/1.38 (sK1_relation_exists_F n0 n1 n1 n1 n1)) true (equalish n1 $_1414) % 1.17/1.38 true = true % 1.17/1.38 |- ifeq % 1.17/1.38 (f $_1413 $_1414 $_1415 $_1416 $_1417 % 1.17/1.38 (sK1_relation_exists_F n1 n0 n0 n0 n0)) true (equalish n0 $_1414) % 1.17/1.38 true = true % 1.17/1.38 |- ifeq % 1.17/1.38 (f $_1413 $_1414 $_1415 $_1416 $_1417 % 1.17/1.38 (sK1_relation_exists_F n1 n0 n0 n0 n1)) true (equalish n0 $_1414) % 1.17/1.38 true = true % 1.17/1.38 |- ifeq % 1.17/1.38 (f $_1413 $_1414 $_1415 $_1416 $_1417 % 1.17/1.38 (sK1_relation_exists_F n1 n0 n0 n1 n0)) true (equalish n0 $_1414) % 1.17/1.38 true = true % 1.17/1.38 |- ifeq % 1.17/1.38 (f $_1413 $_1414 $_1415 $_1416 $_1417 % 1.17/1.38 (sK1_relation_exists_F n1 n0 n0 n1 n1)) true (equalish n0 $_1414) % 1.17/1.38 true = true % 1.17/1.38 |- ifeq % 1.17/1.38 (f $_1413 $_1414 $_1415 $_1416 $_1417 % 1.17/1.38 (sK1_relation_exists_F n1 n0 n1 n0 n0)) true (equalish n0 $_1414) % 1.17/1.38 true = true % 1.17/1.38 |- ifeq % 1.17/1.38 (f $_1413 $_1414 $_1415 $_1416 $_1417 % 1.17/1.38 (sK1_relation_exists_F n1 n0 n1 n0 n1)) true (equalish n0 $_1414) % 1.17/1.38 true = true % 1.17/1.38 |- ifeq % 1.17/1.38 (f $_1413 $_1414 $_1415 $_1416 $_1417 % 1.17/1.38 (sK1_relation_exists_F n1 n0 n1 n1 n0)) true (equalish n0 $_1414) % 1.17/1.38 true = true % 1.17/1.38 |- ifeq % 1.17/1.38 (f $_1413 $_1414 $_1415 $_1416 $_1417 % 1.17/1.38 (sK1_relation_exists_F n1 n0 n1 n1 n1)) true (equalish n0 $_1414) % 1.17/1.38 true = true % 1.17/1.38 |- ifeq % 1.17/1.38 (f $_1413 $_1414 $_1415 $_1416 $_1417 % 1.17/1.38 (sK1_relation_exists_F n1 n1 n0 n0 n0)) true (equalish n1 $_1414) % 1.17/1.38 true = true % 1.17/1.38 |- ifeq % 1.17/1.38 (f $_1413 $_1414 $_1415 $_1416 $_1417 % 1.17/1.38 (sK1_relation_exists_F n1 n1 n0 n0 n1)) true (equalish n1 $_1414) % 1.17/1.38 true = true % 1.17/1.38 |- ifeq % 1.17/1.38 (f $_1413 $_1414 $_1415 $_1416 $_1417 % 1.17/1.38 (sK1_relation_exists_F n1 n1 n0 n1 n0)) true (equalish n1 $_1414) % 1.17/1.38 true = true % 1.17/1.38 |- ifeq % 1.17/1.38 (f $_1413 $_1414 $_1415 $_1416 $_1417 % 1.17/1.38 (sK1_relation_exists_F n1 n1 n0 n1 n1)) true (equalish n1 $_1414) % 1.17/1.38 true = true % 1.17/1.38 |- ifeq % 1.17/1.38 (f $_1413 $_1414 $_1415 $_1416 $_1417 % 1.17/1.38 (sK1_relation_exists_F n1 n1 n1 n0 n0)) true (equalish n1 $_1414) % 1.17/1.38 true = true % 1.17/1.38 |- ifeq % 1.17/1.38 (f $_1413 $_1414 $_1415 $_1416 $_1417 % 1.17/1.38 (sK1_relation_exists_F n1 n1 n1 n0 n1)) true (equalish n1 $_1414) % 1.17/1.38 true = true % 1.17/1.38 |- ifeq % 1.17/1.38 (f $_1413 $_1414 $_1415 $_1416 $_1417 % 1.17/1.38 (sK1_relation_exists_F n1 n1 n1 n1 n0)) true (equalish n1 $_1414) % 1.17/1.38 true = true % 1.17/1.38 |- ifeq % 1.17/1.38 (f $_1413 $_1414 $_1415 $_1416 $_1417 % 1.17/1.38 (sK1_relation_exists_F n1 n1 n1 n1 n1)) true (equalish n1 $_1414) % 1.17/1.38 true = true % 1.17/1.38 |- ifeq % 1.17/1.38 (f $_1408 $_1409 $_1410 $_1411 $_1412 % 1.17/1.38 (sK1_relation_exists_F n0 n0 n0 n0 n0)) true (equalish $_1409 n0) % 1.17/1.38 true = true % 1.17/1.38 |- ifeq % 1.17/1.38 (f $_1408 $_1409 $_1410 $_1411 $_1412 % 1.17/1.38 (sK1_relation_exists_F n0 n0 n0 n0 n1)) true (equalish $_1409 n0) % 1.17/1.38 true = true % 1.17/1.38 |- ifeq % 1.17/1.38 (f $_1408 $_1409 $_1410 $_1411 $_1412 % 1.17/1.38 (sK1_relation_exists_F n0 n0 n0 n1 n0)) true (equalish $_1409 n0) % 1.17/1.38 true = true % 1.17/1.38 |- ifeq % 1.17/1.38 (f $_1408 $_1409 $_1410 $_1411 $_1412 % 1.17/1.38 (sK1_relation_exists_F n0 n0 n0 n1 n1)) true (equalish $_1409 n0) % 1.17/1.38 true = true % 1.17/1.38 |- ifeq % 1.17/1.38 (f $_1408 $_1409 $_1410 $_1411 $_1412 % 1.17/1.38 (sK1_relation_exists_F n0 n0 n1 n0 n0)) true (equalish $_1409 n0) % 1.17/1.38 true = true % 1.17/1.38 |- ifeq % 1.17/1.38 (f $_1408 $_1409 $_1410 $_1411 $_1412 % 1.17/1.38 (sK1_relation_exists_F n0 n0 n1 n0 n1)) true (equalish $_1409 n0) % 1.17/1.38 true = true % 1.17/1.38 |- ifeq % 1.17/1.38 (f $_1408 $_1409 $_1410 $_1411 $_1412 % 1.17/1.38 (sK1_relation_exists_F n0 n0 n1 n1 n0)) true (equalish $_1409 n0) % 1.17/1.38 true = true % 1.17/1.38 |- ifeq % 1.17/1.38 (f $_1408 $_1409 $_1410 $_1411 $_1412 % 1.17/1.38 (sK1_relation_exists_F n0 n0 n1 n1 n1)) true (equalish $_1409 n0) % 1.17/1.38 true = true % 1.17/1.38 |- ifeq % 1.17/1.38 (f $_1408 $_1409 $_1410 $_1411 $_1412 % 1.17/1.38 (sK1_relation_exists_F n0 n1 n0 n0 n0)) true (equalish $_1409 n1) % 1.17/1.38 true = true % 1.17/1.38 |- ifeq % 1.17/1.38 (f $_1408 $_1409 $_1410 $_1411 $_1412 % 1.17/1.38 (sK1_relation_exists_F n0 n1 n0 n0 n1)) true (equalish $_1409 n1) % 1.17/1.38 true = true % 1.17/1.38 |- ifeq % 1.17/1.38 (f $_1408 $_1409 $_1410 $_1411 $_1412 % 1.17/1.38 (sK1_relation_exists_F n0 n1 n0 n1 n0)) true (equalish $_1409 n1) % 1.17/1.38 true = true % 1.17/1.38 |- ifeq % 1.17/1.38 (f $_1408 $_1409 $_1410 $_1411 $_1412 % 1.17/1.38 (sK1_relation_exists_F n0 n1 n0 n1 n1)) true (equalish $_1409 n1) % 1.17/1.38 true = true % 1.17/1.38 |- ifeq % 1.17/1.38 (f $_1408 $_1409 $_1410 $_1411 $_1412 % 1.17/1.38 (sK1_relation_exists_F n0 n1 n1 n0 n0)) true (equalish $_1409 n1) % 1.17/1.38 true = true % 1.17/1.38 |- ifeq % 1.17/1.38 (f $_1408 $_1409 $_1410 $_1411 $_1412 % 1.17/1.38 (sK1_relation_exists_F n0 n1 n1 n0 n1)) true (equalish $_1409 n1) % 1.17/1.38 true = true % 1.17/1.38 |- ifeq % 1.17/1.38 (f $_1408 $_1409 $_1410 $_1411 $_1412 % 1.17/1.38 (sK1_relation_exists_F n0 n1 n1 n1 n0)) true (equalish $_1409 n1) % 1.17/1.38 true = true % 1.17/1.38 |- ifeq % 1.17/1.38 (f $_1408 $_1409 $_1410 $_1411 $_1412 % 1.17/1.38 (sK1_relation_exists_F n0 n1 n1 n1 n1)) true (equalish $_1409 n1) % 1.17/1.38 true = true % 1.17/1.38 |- ifeq % 1.17/1.38 (f $_1408 $_1409 $_1410 $_1411 $_1412 % 1.17/1.38 (sK1_relation_exists_F n1 n0 n0 n0 n0)) true (equalish $_1409 n0) % 1.17/1.38 true = true % 1.17/1.38 |- ifeq % 1.17/1.38 (f $_1408 $_1409 $_1410 $_1411 $_1412 % 1.17/1.38 (sK1_relation_exists_F n1 n0 n0 n0 n1)) true (equalish $_1409 n0) % 1.17/1.38 true = true % 1.17/1.38 |- ifeq % 1.17/1.38 (f $_1408 $_1409 $_1410 $_1411 $_1412 % 1.17/1.38 (sK1_relation_exists_F n1 n0 n0 n1 n0)) true (equalish $_1409 n0) % 1.17/1.38 true = true % 1.17/1.38 |- ifeq % 1.17/1.38 (f $_1408 $_1409 $_1410 $_1411 $_1412 % 1.17/1.38 (sK1_relation_exists_F n1 n0 n0 n1 n1)) true (equalish $_1409 n0) % 1.17/1.38 true = true % 1.17/1.38 |- ifeq % 1.17/1.38 (f $_1408 $_1409 $_1410 $_1411 $_1412 % 1.17/1.38 (sK1_relation_exists_F n1 n0 n1 n0 n0)) true (equalish $_1409 n0) % 1.17/1.38 true = true % 1.17/1.38 |- ifeq % 1.17/1.38 (f $_1408 $_1409 $_1410 $_1411 $_1412 % 1.17/1.38 (sK1_relation_exists_F n1 n0 n1 n0 n1)) true (equalish $_1409 n0) % 1.17/1.38 true = true % 1.17/1.38 |- ifeq % 1.17/1.38 (f $_1408 $_1409 $_1410 $_1411 $_1412 % 1.17/1.38 (sK1_relation_exists_F n1 n0 n1 n1 n0)) true (equalish $_1409 n0) % 1.17/1.38 true = true % 1.17/1.38 |- ifeq % 1.17/1.38 (f $_1408 $_1409 $_1410 $_1411 $_1412 % 1.17/1.38 (sK1_relation_exists_F n1 n0 n1 n1 n1)) true (equalish $_1409 n0) % 1.17/1.38 true = true % 1.17/1.38 |- ifeq % 1.17/1.38 (f $_1408 $_1409 $_1410 $_1411 $_1412 % 1.17/1.38 (sK1_relation_exists_F n1 n1 n0 n0 n0)) true (equalish $_1409 n1) % 1.17/1.38 true = true % 1.17/1.38 |- ifeq % 1.17/1.38 (f $_1408 $_1409 $_1410 $_1411 $_1412 % 1.17/1.38 (sK1_relation_exists_F n1 n1 n0 n0 n1)) true (equalish $_1409 n1) % 1.17/1.38 true = true % 1.17/1.38 |- ifeq % 1.17/1.38 (f $_1408 $_1409 $_1410 $_1411 $_1412 % 1.17/1.38 (sK1_relation_exists_F n1 n1 n0 n1 n0)) true (equalish $_1409 n1) % 1.17/1.38 true = true % 1.17/1.38 |- ifeq % 1.17/1.38 (f $_1408 $_1409 $_1410 $_1411 $_1412 % 1.17/1.38 (sK1_relation_exists_F n1 n1 n0 n1 n1)) true (equalish $_1409 n1) % 1.17/1.38 true = true % 1.17/1.38 |- ifeq % 1.17/1.38 (f $_1408 $_1409 $_1410 $_1411 $_1412 % 1.17/1.38 (sK1_relation_exists_F n1 n1 n1 n0 n0)) true (equalish $_1409 n1) % 1.17/1.38 true = true % 1.17/1.38 |- ifeq % 1.17/1.38 (f $_1408 $_1409 $_1410 $_1411 $_1412 % 1.17/1.38 (sK1_relation_exists_F n1 n1 n1 n0 n1)) true (equalish $_1409 n1) % 1.17/1.38 true = true % 1.17/1.38 |- ifeq % 1.17/1.38 (f $_1408 $_1409 $_1410 $_1411 $_1412 % 1.17/1.38 (sK1_relation_exists_F n1 n1 n1 n1 n0)) true (equalish $_1409 n1) % 1.17/1.38 true = true % 1.17/1.38 |- ifeq % 1.17/1.38 (f $_1408 $_1409 $_1410 $_1411 $_1412 % 1.17/1.38 (sK1_relation_exists_F n1 n1 n1 n1 n1)) true (equalish $_1409 n1) % 1.17/1.38 true = true % 1.17/1.38 |- ifeq (equalish $_1741 $_1741) true % 1.17/1.38 (ifeq (equalish $_1740 $_1740) true % 1.17/1.38 (f n0 n0 n1 $_1740 $_1741 % 1.17/1.38 (sK1_relation_exists_F n0 n0 n1 $_1740 $_1741)) true) true = % 1.17/1.38 true % 1.17/1.38 |- ifeq (equalish $_1741 $_1741) true % 1.17/1.38 (ifeq (equalish $_1739 $_1739) true % 1.17/1.38 (f n0 n0 $_1739 n1 $_1741 % 1.17/1.38 (sK1_relation_exists_F n0 n0 $_1739 n1 $_1741)) true) true = % 1.17/1.38 true % 1.17/1.38 |- ifeq (equalish $_1740 $_1740) true % 1.17/1.38 (ifeq (equalish $_1739 $_1739) true % 1.17/1.38 (f n0 n0 $_1739 $_1740 n0 % 1.17/1.38 (sK1_relation_exists_F n0 n0 $_1739 $_1740 n0)) true) true = % 1.17/1.38 true % 1.17/1.38 |- ifeq (equalish $_1754 $_1754) true % 1.17/1.38 (ifeq (equalish $_1753 $_1753) true % 1.17/1.38 (f n0 n1 $_1753 $_1754 n0 % 1.17/1.38 (sK1_relation_exists_F n0 n1 $_1753 $_1754 n0)) true) true = % 1.17/1.38 true % 1.17/1.38 |- ifeq (equalish $_1759 $_1759) true % 1.17/1.38 (ifeq (equalish $_1758 $_1758) true % 1.17/1.38 (f n1 n0 n1 $_1758 $_1759 % 1.17/1.38 (sK1_relation_exists_F n1 n0 n1 $_1758 $_1759)) true) true = % 1.17/1.38 true % 1.17/1.38 |- ifeq (equalish $_1759 $_1759) true % 1.17/1.38 (ifeq (equalish $_1757 $_1757) true % 1.17/1.38 (f n1 n0 $_1757 n1 $_1759 % 1.17/1.38 (sK1_relation_exists_F n1 n0 $_1757 n1 $_1759)) true) true = % 1.17/1.38 true % 1.17/1.38 |- ifeq (equalish $_1758 $_1758) true % 1.17/1.38 (ifeq (equalish $_1757 $_1757) true % 1.17/1.38 (f n1 n0 $_1757 $_1758 n0 % 1.17/1.38 (sK1_relation_exists_F n1 n0 $_1757 $_1758 n0)) true) true = % 1.17/1.38 true % 1.17/1.38 |- ifeq (equalish $_1786 $_1786) true % 1.17/1.38 (ifeq (equalish $_1785 $_1785) true % 1.17/1.38 (f n0 n1 $_1785 n0 $_1786 % 1.17/1.38 (sK1_relation_exists_F n0 n1 $_1785 n0 $_1786)) true) true = % 1.17/1.38 true % 1.17/1.38 |- ifeq (equalish $_1786 $_1786) true % 1.17/1.38 (ifeq (equalish $_1785 $_1785) true % 1.17/1.38 (f n1 n1 $_1785 n0 $_1786 % 1.17/1.38 (sK1_relation_exists_F n1 n1 $_1785 n0 $_1786)) true) true = % 1.17/1.38 true % 1.17/1.38 |- ifeq (equalish $_1793 $_1793) true % 1.17/1.38 (ifeq (equalish $_1792 $_1792) true % 1.17/1.38 (f n1 n1 $_1792 $_1793 n0 % 1.17/1.38 (sK1_relation_exists_F n1 n1 $_1792 $_1793 n0)) true) true = % 1.17/1.38 true % 1.17/1.38 |- ifeq (equalish $_1798 $_1798) true % 1.17/1.38 (ifeq (equalish $_1797 $_1797) true % 1.17/1.38 (f n0 n1 $_1797 $_1798 n1 % 1.17/1.38 (sK1_relation_exists_F n0 n1 $_1797 $_1798 n1)) true) true = % 1.17/1.38 true % 1.17/1.38 |- ifeq (equalish $_1798 $_1798) true % 1.17/1.38 (ifeq (equalish $_1797 $_1797) true % 1.17/1.38 (f n1 n1 $_1797 $_1798 n1 % 1.17/1.38 (sK1_relation_exists_F n1 n1 $_1797 $_1798 n1)) true) true = % 1.17/1.38 true % 1.17/1.38 SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 1.17/1.38 %------------------------------------------------------------------------------