%------------------------------------------------------------------------------
% File : Matita---1.0
% Problem : REL043-2 : TPTP v8.1.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : matitaprover --timeout %d --tptppath /export/starexec/sandbox/benchmark %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 : Mon Jul 18 19:42:46 EDT 2022
% Result : Unsatisfiable 275.22s 69.15s
% Output : CNFRefutation 275.54s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12 % Problem : REL043-2 : TPTP v8.1.0. Released v4.0.0.
% 0.06/0.12 % Command : matitaprover --timeout %d --tptppath /export/starexec/sandbox/benchmark %s
% 0.13/0.33 % Computer : n026.cluster.edu
% 0.13/0.33 % Model : x86_64 x86_64
% 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.33 % Memory : 8042.1875MB
% 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.33 % CPULimit : 300
% 0.13/0.33 % WCLimit : 600
% 0.13/0.33 % DateTime : Fri Jul 8 07:21:24 EDT 2022
% 0.13/0.33 % CPUTime :
% 0.13/0.34 25268: Facts:
% 0.13/0.34 25268: Id : 2, {_}:
% 0.13/0.34 join ?2 ?3 =?= join ?3 ?2
% 0.13/0.34 [3, 2] by maddux1_join_commutativity_1 ?2 ?3
% 0.13/0.34 25268: Id : 3, {_}:
% 0.13/0.34 join ?5 (join ?6 ?7) =?= join (join ?5 ?6) ?7
% 0.13/0.34 [7, 6, 5] by maddux2_join_associativity_2 ?5 ?6 ?7
% 0.13/0.34 25268: Id : 4, {_}:
% 0.13/0.34 ?9
% 0.13/0.34 =<=
% 0.13/0.34 join (complement (join (complement ?9) (complement ?10)))
% 0.13/0.34 (complement (join (complement ?9) ?10))
% 0.13/0.34 [10, 9] by maddux3_a_kind_of_de_Morgan_3 ?9 ?10
% 0.13/0.34 25268: Id : 5, {_}:
% 0.13/0.34 meet ?12 ?13 =<= complement (join (complement ?12) (complement ?13))
% 0.13/0.34 [13, 12] by maddux4_definiton_of_meet_4 ?12 ?13
% 0.13/0.34 25268: Id : 6, {_}:
% 0.13/0.34 composition ?15 (composition ?16 ?17)
% 0.13/0.34 =?=
% 0.13/0.34 composition (composition ?15 ?16) ?17
% 0.13/0.34 [17, 16, 15] by composition_associativity_5 ?15 ?16 ?17
% 0.13/0.34 25268: Id : 7, {_}: composition ?19 one =>= ?19 [19] by composition_identity_6 ?19
% 0.13/0.34 25268: Id : 8, {_}:
% 0.13/0.34 composition (join ?21 ?22) ?23
% 0.13/0.34 =<=
% 0.13/0.34 join (composition ?21 ?23) (composition ?22 ?23)
% 0.13/0.34 [23, 22, 21] by composition_distributivity_7 ?21 ?22 ?23
% 0.13/0.34 25268: Id : 9, {_}:
% 0.13/0.34 converse (converse ?25) =>= ?25
% 0.13/0.34 [25] by converse_idempotence_8 ?25
% 0.13/0.34 25268: Id : 10, {_}:
% 0.13/0.34 converse (join ?27 ?28) =<= join (converse ?27) (converse ?28)
% 0.13/0.34 [28, 27] by converse_additivity_9 ?27 ?28
% 0.13/0.34 25268: Id : 11, {_}:
% 0.13/0.34 converse (composition ?30 ?31)
% 0.13/0.34 =<=
% 0.13/0.34 composition (converse ?31) (converse ?30)
% 0.13/0.34 [31, 30] by converse_multiplicativity_10 ?30 ?31
% 0.13/0.34 25268: Id : 12, {_}:
% 0.13/0.34 join (composition (converse ?33) (complement (composition ?33 ?34)))
% 0.13/0.34 (complement ?34)
% 0.13/0.34 =>=
% 0.13/0.34 complement ?34
% 0.13/0.34 [34, 33] by converse_cancellativity_11 ?33 ?34
% 0.13/0.34 25268: Id : 13, {_}: top =<= join ?36 (complement ?36) [36] by def_top_12 ?36
% 0.13/0.34 25268: Id : 14, {_}: zero =<= meet ?38 (complement ?38) [38] by def_zero_13 ?38
% 0.13/0.34 25268: Id : 15, {_}:
% 0.13/0.34 join (meet (composition ?40 ?41) ?42)
% 0.13/0.34 (composition (meet ?40 (composition ?42 (converse ?41)))
% 0.13/0.34 (meet ?41 (composition (converse ?40) ?42)))
% 0.13/0.34 =>=
% 0.13/0.34 composition (meet ?40 (composition ?42 (converse ?41)))
% 0.13/0.34 (meet ?41 (composition (converse ?40) ?42))
% 0.13/0.34 [42, 41, 40] by dedekind_law_14 ?40 ?41 ?42
% 0.13/0.34 25268: Id : 16, {_}:
% 0.13/0.34 join (meet (composition ?44 ?45) ?46)
% 0.13/0.34 (meet (composition ?44 (meet ?45 (composition (converse ?44) ?46)))
% 0.13/0.34 ?46)
% 0.13/0.34 =>=
% 0.13/0.34 meet (composition ?44 (meet ?45 (composition (converse ?44) ?46)))
% 0.13/0.34 ?46
% 0.13/0.34 [46, 45, 44] by modular_law_1_15 ?44 ?45 ?46
% 0.13/0.34 25268: Id : 17, {_}:
% 0.13/0.34 join (meet (composition ?48 ?49) ?50)
% 0.13/0.34 (meet (composition (meet ?48 (composition ?50 (converse ?49))) ?49)
% 0.13/0.34 ?50)
% 0.13/0.34 =>=
% 0.13/0.34 meet (composition (meet ?48 (composition ?50 (converse ?49))) ?49)
% 0.13/0.34 ?50
% 0.13/0.34 [50, 49, 48] by modular_law_2_16 ?48 ?49 ?50
% 0.13/0.34 25268: Id : 18, {_}: join (composition sk1 (converse sk2)) sk3 =>= sk3 [] by goals_17
% 0.13/0.34 25268: Goal:
% 0.13/0.34 25268: Id : 1, {_}:
% 0.13/0.34 join (composition (complement sk3) sk2) (complement sk1)
% 0.13/0.34 =>=
% 0.13/0.34 complement sk1
% 0.13/0.34 [] by goals_18
% 275.22/69.15 Statistics :
% 275.22/69.15 Max weight : 28
% 275.22/69.15 Found proof, 68.814625s
% 275.22/69.15 % SZS status Unsatisfiable for theBenchmark.p
% 275.22/69.15 % SZS output start CNFRefutation for theBenchmark.p
% 275.22/69.15 Id : 11, {_}: converse (composition ?30 ?31) =<= composition (converse ?31) (converse ?30) [31, 30] by converse_multiplicativity_10 ?30 ?31
% 275.22/69.15 Id : 6, {_}: composition ?15 (composition ?16 ?17) =?= composition (composition ?15 ?16) ?17 [17, 16, 15] by composition_associativity_5 ?15 ?16 ?17
% 275.22/69.15 Id : 15, {_}: join (meet (composition ?40 ?41) ?42) (composition (meet ?40 (composition ?42 (converse ?41))) (meet ?41 (composition (converse ?40) ?42))) =>= composition (meet ?40 (composition ?42 (converse ?41))) (meet ?41 (composition (converse ?40) ?42)) [42, 41, 40] by dedekind_law_14 ?40 ?41 ?42
% 275.22/69.15 Id : 8, {_}: composition (join ?21 ?22) ?23 =<= join (composition ?21 ?23) (composition ?22 ?23) [23, 22, 21] by composition_distributivity_7 ?21 ?22 ?23
% 275.22/69.15 Id : 65, {_}: meet ?208 ?209 =<= complement (join (complement ?208) (complement ?209)) [209, 208] by maddux4_definiton_of_meet_4 ?208 ?209
% 275.22/69.15 Id : 121, {_}: converse (join ?360 ?361) =<= join (converse ?360) (converse ?361) [361, 360] by converse_additivity_9 ?360 ?361
% 275.22/69.15 Id : 10, {_}: converse (join ?27 ?28) =<= join (converse ?27) (converse ?28) [28, 27] by converse_additivity_9 ?27 ?28
% 275.22/69.15 Id : 18, {_}: join (composition sk1 (converse sk2)) sk3 =>= sk3 [] by goals_17
% 275.22/69.15 Id : 17, {_}: join (meet (composition ?48 ?49) ?50) (meet (composition (meet ?48 (composition ?50 (converse ?49))) ?49) ?50) =>= meet (composition (meet ?48 (composition ?50 (converse ?49))) ?49) ?50 [50, 49, 48] by modular_law_2_16 ?48 ?49 ?50
% 275.22/69.15 Id : 2, {_}: join ?2 ?3 =?= join ?3 ?2 [3, 2] by maddux1_join_commutativity_1 ?2 ?3
% 275.22/69.15 Id : 13, {_}: top =<= join ?36 (complement ?36) [36] by def_top_12 ?36
% 275.22/69.15 Id : 3, {_}: join ?5 (join ?6 ?7) =?= join (join ?5 ?6) ?7 [7, 6, 5] by maddux2_join_associativity_2 ?5 ?6 ?7
% 275.22/69.15 Id : 14, {_}: zero =<= meet ?38 (complement ?38) [38] by def_zero_13 ?38
% 275.22/69.15 Id : 9, {_}: converse (converse ?25) =>= ?25 [25] by converse_idempotence_8 ?25
% 275.22/69.15 Id : 134, {_}: converse (composition ?390 ?391) =<= composition (converse ?391) (converse ?390) [391, 390] by converse_multiplicativity_10 ?390 ?391
% 275.22/69.15 Id : 7, {_}: composition ?19 one =>= ?19 [19] by composition_identity_6 ?19
% 275.22/69.15 Id : 12, {_}: join (composition (converse ?33) (complement (composition ?33 ?34))) (complement ?34) =>= complement ?34 [34, 33] by converse_cancellativity_11 ?33 ?34
% 275.22/69.15 Id : 5, {_}: meet ?12 ?13 =<= complement (join (complement ?12) (complement ?13)) [13, 12] by maddux4_definiton_of_meet_4 ?12 ?13
% 275.22/69.15 Id : 4, {_}: ?9 =<= join (complement (join (complement ?9) (complement ?10))) (complement (join (complement ?9) ?10)) [10, 9] by maddux3_a_kind_of_de_Morgan_3 ?9 ?10
% 275.22/69.15 Id : 62, {_}: ?9 =<= join (meet ?9 ?10) (complement (join (complement ?9) ?10)) [10, 9] by Demod 4 with 5 at 1,3
% 275.22/69.15 Id : 565, {_}: converse (composition (converse ?1125) ?1126) =>= composition (converse ?1126) ?1125 [1126, 1125] by Super 134 with 9 at 2,3
% 275.22/69.15 Id : 570, {_}: converse (converse ?1143) =<= composition (converse one) ?1143 [1143] by Super 565 with 7 at 1,2
% 275.22/69.15 Id : 597, {_}: ?1143 =<= composition (converse one) ?1143 [1143] by Demod 570 with 9 at 2
% 275.22/69.15 Id : 608, {_}: one =<= converse one [] by Super 7 with 597 at 2
% 275.22/69.15 Id : 660, {_}: join (composition one (complement (composition one ?1227))) (complement ?1227) =>= complement ?1227 [1227] by Super 12 with 608 at 1,1,2
% 275.22/69.15 Id : 649, {_}: ?1143 =<= composition one ?1143 [1143] by Demod 597 with 608 at 1,3
% 275.22/69.15 Id : 675, {_}: join (complement (composition one ?1227)) (complement ?1227) =>= complement ?1227 [1227] by Demod 660 with 649 at 1,2
% 275.22/69.19 Id : 676, {_}: join (complement ?1227) (complement ?1227) =>= complement ?1227 [1227] by Demod 675 with 649 at 1,1,2
% 275.22/69.19 Id : 959, {_}: ?1598 =<= join (meet ?1598 (complement ?1598)) (complement (complement ?1598)) [1598] by Super 62 with 676 at 1,2,3
% 275.22/69.19 Id : 1020, {_}: ?1636 =<= join zero (complement (complement ?1636)) [1636] by Demod 959 with 14 at 1,3
% 275.22/69.19 Id : 1021, {_}: join (complement ?1638) (complement ?1639) =<= join zero (complement (meet ?1638 ?1639)) [1639, 1638] by Super 1020 with 5 at 1,2,3
% 275.22/69.19 Id : 961, {_}: join (complement ?1603) (complement ?1603) =>= complement ?1603 [1603] by Demod 675 with 649 at 1,1,2
% 275.22/69.19 Id : 155, {_}: meet ?434 (complement ?434) =>= complement top [434] by Super 5 with 13 at 1,3
% 275.22/69.19 Id : 259, {_}: zero =<= complement top [] by Demod 155 with 14 at 2
% 275.22/69.19 Id : 963, {_}: join (complement top) zero =>= complement top [] by Super 961 with 259 at 2,2
% 275.22/69.19 Id : 978, {_}: join zero (complement top) =>= complement top [] by Demod 963 with 2 at 2
% 275.22/69.19 Id : 979, {_}: join zero (complement top) =>= zero [] by Demod 978 with 259 at 3
% 275.22/69.19 Id : 980, {_}: join zero zero =>= zero [] by Demod 979 with 259 at 2,2
% 275.22/69.19 Id : 1057, {_}: join zero (join zero ?1674) =>= join zero ?1674 [1674] by Super 3 with 980 at 1,3
% 275.22/69.19 Id : 170, {_}: ?467 =<= join zero (complement (join (complement ?467) (complement ?467))) [467] by Super 62 with 14 at 1,3
% 275.22/69.19 Id : 174, {_}: ?467 =<= join zero (meet ?467 ?467) [467] by Demod 170 with 5 at 2,3
% 275.22/69.19 Id : 1065, {_}: join zero ?1688 =<= join zero (meet ?1688 ?1688) [1688] by Super 1057 with 174 at 2,2
% 275.22/69.19 Id : 1082, {_}: join zero ?1688 =>= ?1688 [1688] by Demod 1065 with 174 at 3
% 275.22/69.19 Id : 10497, {_}: join (complement ?8867) (complement ?8868) =>= complement (meet ?8867 ?8868) [8868, 8867] by Demod 1021 with 1082 at 3
% 275.22/69.19 Id : 262, {_}: meet top ?674 =<= complement (join zero (complement ?674)) [674] by Super 5 with 259 at 1,1,3
% 275.22/69.19 Id : 1093, {_}: meet top ?674 =<= complement (complement ?674) [674] by Demod 262 with 1082 at 1,3
% 275.22/69.19 Id : 974, {_}: ?1598 =<= join zero (complement (complement ?1598)) [1598] by Demod 959 with 14 at 1,3
% 275.22/69.19 Id : 1090, {_}: ?1598 =<= complement (complement ?1598) [1598] by Demod 974 with 1082 at 3
% 275.22/69.19 Id : 1101, {_}: ?1598 =<= meet top ?1598 [1598] by Demod 1090 with 1093 at 3
% 275.22/69.19 Id : 1105, {_}: ?674 =<= complement (complement ?674) [674] by Demod 1093 with 1101 at 2
% 275.22/69.19 Id : 10500, {_}: join (complement ?8874) ?8875 =<= complement (meet ?8874 (complement ?8875)) [8875, 8874] by Super 10497 with 1105 at 2,2
% 275.22/69.19 Id : 10760, {_}: meet ?9052 (complement ?9053) =<= complement (join (complement ?9052) ?9053) [9053, 9052] by Super 1105 with 10500 at 1,3
% 275.22/69.19 Id : 11244, {_}: ?9 =<= join (meet ?9 ?10) (meet ?9 (complement ?10)) [10, 9] by Demod 62 with 10760 at 2,3
% 275.22/69.19 Id : 11258, {_}: meet ?9450 (complement ?9451) =<= complement (join (complement ?9450) ?9451) [9451, 9450] by Super 1105 with 10500 at 1,3
% 275.22/69.19 Id : 11272, {_}: meet ?9493 (complement (join ?9494 ?9495)) =<= complement (join (join (complement ?9493) ?9494) ?9495) [9495, 9494, 9493] by Super 11258 with 3 at 1,3
% 275.22/69.19 Id : 11268, {_}: meet (meet ?9478 (complement ?9479)) (complement ?9480) =<= complement (join (join (complement ?9478) ?9479) ?9480) [9480, 9479, 9478] by Super 11258 with 10500 at 1,1,3
% 275.22/69.19 Id : 132657, {_}: meet ?126313 (complement (join ?126314 ?126315)) =<= meet (meet ?126313 (complement ?126314)) (complement ?126315) [126315, 126314, 126313] by Demod 11272 with 11268 at 3
% 275.22/69.19 Id : 10509, {_}: join ?8899 (complement ?8900) =<= complement (meet (complement ?8899) ?8900) [8900, 8899] by Super 10497 with 1105 at 1,2
% 275.22/69.19 Id : 11169, {_}: meet (complement ?9343) ?9344 =<= complement (join ?9343 (complement ?9344)) [9344, 9343] by Super 1105 with 10509 at 1,3
% 275.22/69.19 Id : 252, {_}: join sk3 (composition sk1 (converse sk2)) =>= sk3 [] by Demod 18 with 2 at 2
% 275.22/69.19 Id : 22559, {_}: join sk3 (join (composition sk1 (converse sk2)) ?16611) =>= join sk3 ?16611 [16611] by Super 3 with 252 at 1,3
% 275.22/69.19 Id : 22571, {_}: join sk3 top =<= join sk3 (complement (composition sk1 (converse sk2))) [] by Super 22559 with 13 at 2,2
% 275.22/69.19 Id : 22601, {_}: join top sk3 =<= join sk3 (complement (composition sk1 (converse sk2))) [] by Demod 22571 with 2 at 2
% 275.22/69.19 Id : 123, {_}: converse (join (converse ?366) ?367) =>= join ?366 (converse ?367) [367, 366] by Super 121 with 9 at 1,3
% 275.22/69.19 Id : 651, {_}: converse (join one ?1207) =<= join one (converse ?1207) [1207] by Super 123 with 608 at 1,1,2
% 275.22/69.19 Id : 122, {_}: converse (join ?363 (converse ?364)) =>= join (converse ?363) ?364 [364, 363] by Super 121 with 9 at 2,3
% 275.22/69.19 Id : 314, {_}: meet top ?734 =<= complement (join zero (complement ?734)) [734] by Super 5 with 259 at 1,1,3
% 275.22/69.19 Id : 316, {_}: meet top top =<= complement (join zero zero) [] by Super 314 with 259 at 2,1,3
% 275.22/69.19 Id : 965, {_}: join (complement (join zero zero)) (meet top top) =>= complement (join zero zero) [] by Super 961 with 316 at 2,2
% 275.22/69.19 Id : 984, {_}: join (meet top top) (complement (join zero zero)) =>= complement (join zero zero) [] by Demod 965 with 2 at 2
% 275.22/69.19 Id : 985, {_}: join (meet top top) (complement (join zero zero)) =>= meet top top [] by Demod 984 with 316 at 3
% 275.22/69.19 Id : 986, {_}: join (meet top top) (meet top top) =>= meet top top [] by Demod 985 with 316 at 2,2
% 275.22/69.19 Id : 261, {_}: meet ?672 top =<= complement (join (complement ?672) zero) [672] by Super 5 with 259 at 2,1,3
% 275.22/69.19 Id : 270, {_}: meet ?672 top =<= complement (join zero (complement ?672)) [672] by Demod 261 with 2 at 1,3
% 275.22/69.19 Id : 340, {_}: meet ?672 top =?= meet top ?672 [672] by Demod 270 with 262 at 3
% 275.22/69.19 Id : 1104, {_}: meet ?672 top =>= ?672 [672] by Demod 340 with 1101 at 3
% 275.22/69.19 Id : 1880, {_}: join top (meet top top) =>= meet top top [] by Demod 986 with 1104 at 1,2
% 275.22/69.19 Id : 1881, {_}: join top top =>= meet top top [] by Demod 1880 with 1104 at 2,2
% 275.22/69.19 Id : 1882, {_}: join top top =>= top [] by Demod 1881 with 1104 at 3
% 275.22/69.19 Id : 1888, {_}: join top (join top ?2411) =>= join top ?2411 [2411] by Super 3 with 1882 at 1,3
% 275.22/69.19 Id : 1889, {_}: join top (join ?2413 top) =>= join top ?2413 [2413] by Super 1888 with 2 at 2,2
% 275.22/69.19 Id : 493, {_}: converse (join ?965 (converse ?966)) =>= join (converse ?965) ?966 [966, 965] by Super 121 with 9 at 2,3
% 275.22/69.19 Id : 157, {_}: join (complement ?438) ?438 =>= top [438] by Super 2 with 13 at 3
% 275.22/69.19 Id : 497, {_}: converse top =<= join (converse (complement (converse ?978))) ?978 [978] by Super 493 with 157 at 1,2
% 275.22/69.19 Id : 2995, {_}: join top (converse top) =<= join top (converse (complement (converse top))) [] by Super 1889 with 497 at 2,2
% 275.22/69.19 Id : 3075, {_}: converse (join top (converse top)) =<= join (converse top) (complement (converse top)) [] by Super 122 with 2995 at 1,2
% 275.22/69.19 Id : 3086, {_}: join (converse top) top =<= join (converse top) (complement (converse top)) [] by Demod 3075 with 122 at 2
% 275.22/69.19 Id : 3087, {_}: join (converse top) top =>= top [] by Demod 3086 with 13 at 3
% 275.22/69.19 Id : 3088, {_}: join top (converse top) =>= top [] by Demod 3087 with 2 at 2
% 275.22/69.19 Id : 3092, {_}: converse top =<= join (converse top) top [] by Super 122 with 3088 at 1,2
% 275.22/69.19 Id : 3102, {_}: converse top =<= join top (converse top) [] by Demod 3092 with 2 at 3
% 275.22/69.19 Id : 3103, {_}: converse top =>= top [] by Demod 3102 with 3088 at 3
% 275.22/69.19 Id : 3117, {_}: converse (join one top) =>= join one top [] by Super 651 with 3103 at 2,3
% 275.22/69.19 Id : 662, {_}: converse (join ?1232 one) =<= join (converse ?1232) one [1232] by Super 122 with 608 at 2,1,2
% 275.22/69.19 Id : 668, {_}: converse (join ?1232 one) =<= join one (converse ?1232) [1232] by Demod 662 with 2 at 3
% 275.22/69.19 Id : 740, {_}: converse (join ?1232 one) =?= converse (join one ?1232) [1232] by Demod 668 with 651 at 3
% 275.22/69.19 Id : 3149, {_}: converse (join top one) =>= join one top [] by Demod 3117 with 740 at 2
% 275.22/69.19 Id : 3150, {_}: converse (join top one) =>= join top one [] by Demod 3149 with 2 at 3
% 275.22/69.19 Id : 3287, {_}: converse (join (join top one) ?3625) =<= join (join top one) (converse ?3625) [3625] by Super 10 with 3150 at 1,3
% 275.22/69.19 Id : 3305, {_}: converse (join top (join one ?3625)) =<= join (join top one) (converse ?3625) [3625] by Demod 3287 with 3 at 1,2
% 275.22/69.19 Id : 3306, {_}: converse (join top (join one ?3625)) =<= join (converse ?3625) (join top one) [3625] by Demod 3305 with 2 at 3
% 275.22/69.19 Id : 3286, {_}: converse (join ?3623 (join top one)) =<= join (converse ?3623) (join top one) [3623] by Super 10 with 3150 at 2,3
% 275.22/69.19 Id : 7458, {_}: converse (join top (join one ?6788)) =?= converse (join ?6788 (join top one)) [6788] by Demod 3306 with 3286 at 3
% 275.22/69.19 Id : 7460, {_}: converse (join top (join one ?6792)) =<= converse (join (join ?6792 top) one) [6792] by Super 7458 with 3 at 1,3
% 275.22/69.19 Id : 8411, {_}: converse (join top (join one ?7548)) =<= converse (join one (join ?7548 top)) [7548] by Demod 7460 with 740 at 3
% 275.22/69.19 Id : 8412, {_}: converse (join top (join one ?7550)) =<= converse (join one (join top ?7550)) [7550] by Super 8411 with 2 at 2,1,3
% 275.22/69.19 Id : 8586, {_}: converse (converse (join top (join one ?7632))) =>= join one (join top ?7632) [7632] by Super 9 with 8412 at 1,2
% 275.22/69.19 Id : 8653, {_}: join top (join one ?7632) =<= join one (join top ?7632) [7632] by Demod 8586 with 9 at 2
% 275.22/69.19 Id : 9083, {_}: join one (join (converse ?7941) ?7942) =<= join (converse (join one ?7941)) ?7942 [7942, 7941] by Super 3 with 651 at 1,3
% 275.22/69.19 Id : 522, {_}: converse (join (converse ?1043) ?1044) =>= join ?1043 (converse ?1044) [1044, 1043] by Super 121 with 9 at 1,3
% 275.22/69.19 Id : 529, {_}: converse top =<= join ?1066 (converse (complement (converse ?1066))) [1066] by Super 522 with 13 at 1,2
% 275.22/69.19 Id : 8789, {_}: top =<= join ?1066 (converse (complement (converse ?1066))) [1066] by Demod 529 with 3103 at 2
% 275.22/69.19 Id : 9093, {_}: join one (join (converse (converse (complement (converse one)))) ?7967) =>= join (converse top) ?7967 [7967] by Super 9083 with 8789 at 1,1,3
% 275.22/69.19 Id : 9227, {_}: join one (join (complement (converse one)) ?7967) =>= join (converse top) ?7967 [7967] by Demod 9093 with 9 at 1,2,2
% 275.22/69.19 Id : 9228, {_}: join one (join (complement (converse one)) ?7967) =>= join top ?7967 [7967] by Demod 9227 with 3103 at 1,3
% 275.22/69.19 Id : 9291, {_}: join one (join (complement one) ?8039) =>= join top ?8039 [8039] by Demod 9228 with 608 at 1,1,2,2
% 275.22/69.19 Id : 9295, {_}: join one (complement one) =>= join top (complement one) [] by Super 9291 with 676 at 2,2
% 275.22/69.19 Id : 9313, {_}: top =<= join top (complement one) [] by Demod 9295 with 13 at 2
% 275.22/69.19 Id : 9333, {_}: join top (join one (complement one)) =>= join one top [] by Super 8653 with 9313 at 2,3
% 275.22/69.19 Id : 9336, {_}: join top top =<= join one top [] by Demod 9333 with 13 at 2,2
% 275.22/69.19 Id : 9337, {_}: join top top =<= join top one [] by Demod 9336 with 2 at 3
% 275.22/69.19 Id : 9338, {_}: top =<= join top one [] by Demod 9337 with 1882 at 2
% 275.22/69.19 Id : 9516, {_}: join top (join one ?8135) =>= join top ?8135 [8135] by Super 3 with 9338 at 1,3
% 275.22/69.19 Id : 9517, {_}: join top (join ?8137 one) =>= join top ?8137 [8137] by Super 9516 with 2 at 2,2
% 275.22/69.19 Id : 3122, {_}: converse (join ?3489 top) =<= join (converse ?3489) top [3489] by Super 10 with 3103 at 2,3
% 275.22/69.19 Id : 3146, {_}: converse (join ?3489 top) =<= join top (converse ?3489) [3489] by Demod 3122 with 2 at 3
% 275.22/69.19 Id : 3123, {_}: converse (join top ?3491) =<= join top (converse ?3491) [3491] by Super 10 with 3103 at 1,3
% 275.22/69.19 Id : 3616, {_}: converse (join ?3489 top) =?= converse (join top ?3489) [3489] by Demod 3146 with 3123 at 3
% 275.22/69.19 Id : 3647, {_}: converse (join (join ?3977 top) ?3978) =<= join (converse (join top ?3977)) (converse ?3978) [3978, 3977] by Super 10 with 3616 at 1,3
% 275.22/69.19 Id : 3715, {_}: converse (join (join ?3977 top) ?3978) =?= converse (join (join top ?3977) ?3978) [3978, 3977] by Demod 3647 with 10 at 3
% 275.22/69.19 Id : 3716, {_}: converse (join (join ?3977 top) ?3978) =>= converse (join top (join ?3977 ?3978)) [3978, 3977] by Demod 3715 with 3 at 1,3
% 275.22/69.19 Id : 14496, {_}: converse (converse (join top (join ?11572 ?11573))) =>= join (join ?11572 top) ?11573 [11573, 11572] by Super 9 with 3716 at 1,2
% 275.22/69.19 Id : 14566, {_}: join top (join ?11572 ?11573) =<= join (join ?11572 top) ?11573 [11573, 11572] by Demod 14496 with 9 at 2
% 275.22/69.19 Id : 10770, {_}: join (complement ?9085) ?9086 =<= complement (meet ?9085 (complement ?9086)) [9086, 9085] by Super 10497 with 1105 at 2,2
% 275.22/69.19 Id : 1097, {_}: ?467 =<= meet ?467 ?467 [467] by Demod 174 with 1082 at 3
% 275.22/69.19 Id : 10789, {_}: join (complement (complement ?9133)) ?9133 =>= complement (complement ?9133) [9133] by Super 10770 with 1097 at 1,3
% 275.22/69.19 Id : 10854, {_}: join ?9133 ?9133 =?= complement (complement ?9133) [9133] by Demod 10789 with 1105 at 1,2
% 275.22/69.19 Id : 10855, {_}: join ?9133 ?9133 =>= ?9133 [9133] by Demod 10854 with 1105 at 3
% 275.22/69.19 Id : 20921, {_}: join ?15357 (join ?15357 ?15358) =>= join ?15357 ?15358 [15358, 15357] by Super 3 with 10855 at 1,3
% 275.22/69.19 Id : 20953, {_}: join ?15438 top =<= join ?15438 (complement ?15438) [15438] by Super 20921 with 13 at 2,2
% 275.22/69.19 Id : 21084, {_}: join ?15438 top =>= top [15438] by Demod 20953 with 13 at 3
% 275.22/69.19 Id : 21161, {_}: join top (join ?11572 ?11573) =>= join top ?11573 [11573, 11572] by Demod 14566 with 21084 at 1,3
% 275.22/69.19 Id : 21164, {_}: join top one =?= join top ?8137 [8137] by Demod 9517 with 21161 at 2
% 275.22/69.19 Id : 21167, {_}: top =<= join top ?8137 [8137] by Demod 21164 with 9338 at 2
% 275.22/69.19 Id : 22602, {_}: top =<= join sk3 (complement (composition sk1 (converse sk2))) [] by Demod 22601 with 21167 at 2
% 275.22/69.19 Id : 22609, {_}: meet (complement sk3) (composition sk1 (converse sk2)) =>= complement top [] by Super 11169 with 22602 at 1,3
% 275.22/69.19 Id : 11271, {_}: meet ?9490 (complement ?9491) =<= complement (join ?9491 (complement ?9490)) [9491, 9490] by Super 11258 with 2 at 1,3
% 275.22/69.19 Id : 11517, {_}: meet ?9490 (complement ?9491) =?= meet (complement ?9491) ?9490 [9491, 9490] by Demod 11271 with 11169 at 3
% 275.22/69.19 Id : 22630, {_}: meet (composition sk1 (converse sk2)) (complement sk3) =>= complement top [] by Demod 22609 with 11517 at 2
% 275.22/69.19 Id : 22631, {_}: meet (composition sk1 (converse sk2)) (complement sk3) =>= zero [] by Demod 22630 with 259 at 3
% 275.22/69.19 Id : 132726, {_}: meet (composition sk1 (converse sk2)) (complement (join sk3 ?126662)) =>= meet zero (complement ?126662) [126662] by Super 132657 with 22631 at 1,3
% 275.22/69.19 Id : 331, {_}: meet (join zero zero) ?753 =<= complement (join (meet top top) (complement ?753)) [753] by Super 5 with 316 at 1,1,3
% 275.22/69.19 Id : 2407, {_}: meet zero ?753 =<= complement (join (meet top top) (complement ?753)) [753] by Demod 331 with 1082 at 1,2
% 275.22/69.19 Id : 2408, {_}: meet zero ?753 =<= complement (join top (complement ?753)) [753] by Demod 2407 with 1104 at 1,1,3
% 275.22/69.19 Id : 2409, {_}: join top (complement ?2909) =<= complement (meet zero ?2909) [2909] by Super 1105 with 2408 at 1,3
% 275.22/69.19 Id : 2457, {_}: meet zero (meet zero ?2975) =<= complement (join top (join top (complement ?2975))) [2975] by Super 2408 with 2409 at 2,1,3
% 275.22/69.19 Id : 1883, {_}: join top (join top ?2402) =>= join top ?2402 [2402] by Super 3 with 1882 at 1,3
% 275.22/69.19 Id : 2463, {_}: meet zero (meet zero ?2975) =<= complement (join top (complement ?2975)) [2975] by Demod 2457 with 1883 at 1,3
% 275.22/69.19 Id : 2464, {_}: meet zero (meet zero ?2975) =>= meet zero ?2975 [2975] by Demod 2463 with 2408 at 3
% 275.22/69.19 Id : 330, {_}: meet ?751 (join zero zero) =<= complement (join (complement ?751) (meet top top)) [751] by Super 5 with 316 at 2,1,3
% 275.22/69.19 Id : 337, {_}: meet ?751 (join zero zero) =<= complement (join (meet top top) (complement ?751)) [751] by Demod 330 with 2 at 1,3
% 275.22/69.19 Id : 2712, {_}: meet ?751 zero =<= complement (join (meet top top) (complement ?751)) [751] by Demod 337 with 1082 at 2,2
% 275.22/69.19 Id : 2713, {_}: meet ?751 zero =<= complement (join top (complement ?751)) [751] by Demod 2712 with 1104 at 1,1,3
% 275.22/69.19 Id : 2420, {_}: meet zero ?2935 =<= complement (join top (complement ?2935)) [2935] by Demod 2407 with 1104 at 1,1,3
% 275.22/69.19 Id : 2424, {_}: meet zero (complement ?2942) =<= complement (join top ?2942) [2942] by Super 2420 with 1105 at 2,1,3
% 275.22/69.19 Id : 2714, {_}: meet ?751 zero =<= meet zero (complement (complement ?751)) [751] by Demod 2713 with 2424 at 3
% 275.22/69.19 Id : 2715, {_}: meet ?751 zero =?= meet zero ?751 [751] by Demod 2714 with 1105 at 2,3
% 275.22/69.19 Id : 2717, {_}: meet zero (meet ?3159 zero) =>= meet zero ?3159 [3159] by Super 2464 with 2715 at 2,2
% 275.22/69.19 Id : 21321, {_}: meet ?15534 (complement top) =>= complement top [15534] by Super 10760 with 21084 at 1,3
% 275.22/69.19 Id : 21391, {_}: meet ?15534 zero =>= complement top [15534] by Demod 21321 with 259 at 2,2
% 275.22/69.19 Id : 21392, {_}: meet ?15534 zero =>= zero [15534] by Demod 21391 with 259 at 3
% 275.22/69.19 Id : 21420, {_}: meet zero zero =?= meet zero ?3159 [3159] by Demod 2717 with 21392 at 2,2
% 275.22/69.19 Id : 21421, {_}: zero =<= meet zero ?3159 [3159] by Demod 21420 with 21392 at 2
% 275.22/69.19 Id : 436944, {_}: meet (composition sk1 (converse sk2)) (complement (join sk3 ?438689)) =>= zero [438689] by Demod 132726 with 21421 at 3
% 275.22/69.19 Id : 437009, {_}: meet (composition sk1 (converse sk2)) (meet (complement sk3) ?438778) =>= zero [438778] by Super 436944 with 11169 at 2,2
% 275.22/69.19 Id : 68, {_}: meet ?219 ?220 =<= complement (join (complement ?220) (complement ?219)) [220, 219] by Super 65 with 2 at 1,3
% 275.22/69.19 Id : 72, {_}: meet ?219 ?220 =?= meet ?220 ?219 [220, 219] by Demod 68 with 5 at 3
% 275.22/69.19 Id : 437260, {_}: meet (meet (complement sk3) ?438778) (composition sk1 (converse sk2)) =>= zero [438778] by Demod 437009 with 72 at 2
% 275.22/69.19 Id : 692711, {_}: join (meet (composition (meet (complement sk3) ?664421) sk2) sk1) (meet (composition zero sk2) sk1) =>= meet (composition (meet (meet (complement sk3) ?664421) (composition sk1 (converse sk2))) sk2) sk1 [664421] by Super 17 with 437260 at 1,1,2,2
% 275.22/69.19 Id : 692876, {_}: join (meet (composition zero sk2) sk1) (meet (composition (meet (complement sk3) ?664421) sk2) sk1) =>= meet (composition (meet (meet (complement sk3) ?664421) (composition sk1 (converse sk2))) sk2) sk1 [664421] by Demod 692711 with 2 at 2
% 275.22/69.19 Id : 692877, {_}: join (meet (composition zero sk2) sk1) (meet (composition (meet (complement sk3) ?664421) sk2) sk1) =>= meet sk1 (composition (meet (meet (complement sk3) ?664421) (composition sk1 (converse sk2))) sk2) [664421] by Demod 692876 with 72 at 3
% 275.22/69.19 Id : 692878, {_}: join (meet sk1 (composition zero sk2)) (meet (composition (meet (complement sk3) ?664421) sk2) sk1) =>= meet sk1 (composition (meet (meet (complement sk3) ?664421) (composition sk1 (converse sk2))) sk2) [664421] by Demod 692877 with 72 at 1,2
% 275.22/69.19 Id : 692879, {_}: join (meet sk1 (composition zero sk2)) (meet sk1 (composition (meet (complement sk3) ?664421) sk2)) =>= meet sk1 (composition (meet (meet (complement sk3) ?664421) (composition sk1 (converse sk2))) sk2) [664421] by Demod 692878 with 72 at 2,2
% 275.22/69.19 Id : 692880, {_}: join (meet sk1 (composition zero sk2)) (meet sk1 (composition (meet (complement sk3) ?664421) sk2)) =>= meet sk1 (composition zero sk2) [664421] by Demod 692879 with 437260 at 1,2,3
% 275.22/69.19 Id : 135, {_}: converse (composition (converse ?393) ?394) =>= composition (converse ?394) ?393 [394, 393] by Super 134 with 9 at 2,3
% 275.22/69.19 Id : 3118, {_}: converse (composition top ?3480) =<= composition (converse ?3480) top [3480] by Super 135 with 3103 at 1,1,2
% 275.22/69.19 Id : 3320, {_}: join (composition (converse (converse ?3651)) (complement (converse (composition top ?3651)))) (complement top) =>= complement top [3651] by Super 12 with 3118 at 1,2,1,2
% 275.22/69.19 Id : 3366, {_}: join (composition ?3651 (complement (converse (composition top ?3651)))) (complement top) =>= complement top [3651] by Demod 3320 with 9 at 1,1,2
% 275.22/69.19 Id : 3367, {_}: join (composition ?3651 (complement (converse (composition top ?3651)))) zero =>= complement top [3651] by Demod 3366 with 259 at 2,2
% 275.22/69.19 Id : 3368, {_}: join (composition ?3651 (complement (converse (composition top ?3651)))) zero =>= zero [3651] by Demod 3367 with 259 at 3
% 275.22/69.19 Id : 3369, {_}: join zero (composition ?3651 (complement (converse (composition top ?3651)))) =>= zero [3651] by Demod 3368 with 2 at 2
% 275.22/69.19 Id : 31782, {_}: composition ?23973 (complement (converse (composition top ?23973))) =>= zero [23973] by Demod 3369 with 1082 at 2
% 275.22/69.19 Id : 283, {_}: join (complement ?691) (join ?691 ?692) =>= join top ?692 [692, 691] by Super 3 with 157 at 1,2
% 275.22/69.19 Id : 300, {_}: join (join ?691 ?692) (complement ?691) =>= join top ?692 [692, 691] by Demod 283 with 2 at 2
% 275.22/69.19 Id : 22802, {_}: join (join ?16742 ?16743) (complement ?16742) =>= top [16743, 16742] by Demod 300 with 21167 at 3
% 275.22/69.19 Id : 1108, {_}: join ?1697 zero =>= ?1697 [1697] by Super 2 with 1082 at 3
% 275.22/69.19 Id : 1111, {_}: converse (converse ?1704) =<= join (converse zero) ?1704 [1704] by Super 122 with 1082 at 1,2
% 275.22/69.19 Id : 1117, {_}: ?1704 =<= join (converse zero) ?1704 [1704] by Demod 1111 with 9 at 2
% 275.22/69.19 Id : 1163, {_}: zero =<= converse zero [] by Super 1108 with 1117 at 2
% 275.22/69.19 Id : 1181, {_}: converse (composition zero ?1779) =<= composition (converse ?1779) zero [1779] by Super 135 with 1163 at 1,1,2
% 275.22/69.19 Id : 3132, {_}: converse (composition zero top) =>= composition top zero [] by Super 1181 with 3103 at 1,3
% 275.22/69.19 Id : 5453, {_}: converse (join ?5183 (composition zero top)) =<= join (converse ?5183) (composition top zero) [5183] by Super 10 with 3132 at 2,3
% 275.22/69.19 Id : 3327, {_}: converse (composition top ?3671) =<= composition (converse ?3671) top [3671] by Super 135 with 3103 at 1,1,2
% 275.22/69.19 Id : 3344, {_}: converse (composition top top) =>= composition top top [] by Super 3327 with 3103 at 1,3
% 275.22/69.19 Id : 5486, {_}: converse (join (composition top top) (composition zero top)) =>= join (composition top top) (composition top zero) [] by Super 5453 with 3344 at 1,3
% 275.22/69.19 Id : 5594, {_}: converse (join (composition zero top) (composition top top)) =>= join (composition top top) (composition top zero) [] by Demod 5486 with 2 at 1,2
% 275.22/69.19 Id : 5595, {_}: converse (join (composition zero top) (composition top top)) =>= join (composition top zero) (composition top top) [] by Demod 5594 with 2 at 3
% 275.22/69.19 Id : 5596, {_}: converse (composition (join zero top) top) =<= join (composition top zero) (composition top top) [] by Demod 5595 with 8 at 1,2
% 275.22/69.19 Id : 5597, {_}: converse (composition top top) =<= join (composition top zero) (composition top top) [] by Demod 5596 with 1082 at 1,1,2
% 275.22/69.19 Id : 5598, {_}: composition top top =<= join (composition top zero) (composition top top) [] by Demod 5597 with 3344 at 2
% 275.22/69.19 Id : 22850, {_}: join (composition top top) (complement (composition top zero)) =>= top [] by Super 22802 with 5598 at 1,2
% 275.22/69.19 Id : 22966, {_}: meet (complement (composition top top)) (composition top zero) =>= complement top [] by Super 11169 with 22850 at 1,3
% 275.22/69.19 Id : 22988, {_}: meet (composition top zero) (complement (composition top top)) =>= complement top [] by Demod 22966 with 11517 at 2
% 275.22/69.19 Id : 22989, {_}: meet (composition top zero) (complement (composition top top)) =>= zero [] by Demod 22988 with 259 at 3
% 275.22/69.19 Id : 23056, {_}: composition top zero =<= join (meet (composition top zero) (composition top top)) zero [] by Super 11244 with 22989 at 2,3
% 275.22/69.19 Id : 23089, {_}: composition top zero =<= join zero (meet (composition top zero) (composition top top)) [] by Demod 23056 with 2 at 3
% 275.22/69.19 Id : 23090, {_}: composition top zero =<= meet (composition top zero) (composition top top) [] by Demod 23089 with 1082 at 3
% 275.22/69.19 Id : 23096, {_}: join (composition top zero) (composition (meet top (composition (composition top top) (converse zero))) (meet zero (composition (converse top) (composition top top)))) =>= composition (meet top (composition (composition top top) (converse zero))) (meet zero (composition (converse top) (composition top top))) [] by Super 15 with 23090 at 1,2
% 275.22/69.19 Id : 23122, {_}: join (composition top zero) (composition (composition (composition top top) (converse zero)) (meet zero (composition (converse top) (composition top top)))) =>= composition (meet top (composition (composition top top) (converse zero))) (meet zero (composition (converse top) (composition top top))) [] by Demod 23096 with 1101 at 1,2,2
% 275.22/69.19 Id : 23123, {_}: join (composition top zero) (composition (composition (composition top top) (converse zero)) zero) =<= composition (meet top (composition (composition top top) (converse zero))) (meet zero (composition (converse top) (composition top top))) [] by Demod 23122 with 21421 at 2,2,2
% 275.22/69.19 Id : 23124, {_}: join (composition top zero) (composition (composition (composition top top) (converse zero)) zero) =<= composition (composition (composition top top) (converse zero)) (meet zero (composition (converse top) (composition top top))) [] by Demod 23123 with 1101 at 1,3
% 275.22/69.19 Id : 23125, {_}: join (composition top zero) (composition (composition (composition top top) (converse zero)) zero) =>= composition (composition (composition top top) (converse zero)) zero [] by Demod 23124 with 21421 at 2,3
% 275.22/69.19 Id : 23126, {_}: composition (join top (composition (composition top top) (converse zero))) zero =>= composition (composition (composition top top) (converse zero)) zero [] by Demod 23125 with 8 at 2
% 275.22/69.19 Id : 23127, {_}: composition (join top (composition (composition top top) (converse zero))) zero =>= composition (composition top top) (composition (converse zero) zero) [] by Demod 23126 with 6 at 3
% 275.22/69.19 Id : 23128, {_}: composition top zero =<= composition (composition top top) (composition (converse zero) zero) [] by Demod 23127 with 21167 at 1,2
% 275.22/69.19 Id : 23129, {_}: composition top zero =<= composition top (composition top (composition (converse zero) zero)) [] by Demod 23128 with 6 at 3
% 275.22/69.19 Id : 23130, {_}: composition top zero =<= composition top (composition top (converse (composition zero zero))) [] by Demod 23129 with 1181 at 2,2,3
% 275.22/69.19 Id : 3126, {_}: converse (composition ?3496 top) =<= composition top (converse ?3496) [3496] by Super 11 with 3103 at 1,3
% 275.22/69.19 Id : 23131, {_}: composition top zero =<= composition top (converse (composition (composition zero zero) top)) [] by Demod 23130 with 3126 at 2,3
% 275.22/69.19 Id : 23132, {_}: composition top zero =<= converse (composition (composition (composition zero zero) top) top) [] by Demod 23131 with 3126 at 3
% 275.22/69.19 Id : 3413, {_}: converse (composition ?3737 (composition top top)) =<= composition (composition top top) (converse ?3737) [3737] by Super 11 with 3344 at 1,3
% 275.54/69.23 Id : 3448, {_}: converse (composition ?3737 (composition top top)) =<= composition top (composition top (converse ?3737)) [3737] by Demod 3413 with 6 at 3
% 275.54/69.23 Id : 8186, {_}: converse (composition ?3737 (composition top top)) =<= composition top (converse (composition ?3737 top)) [3737] by Demod 3448 with 3126 at 2,3
% 275.54/69.23 Id : 8187, {_}: converse (composition ?3737 (composition top top)) =?= converse (composition (composition ?3737 top) top) [3737] by Demod 8186 with 3126 at 3
% 275.54/69.23 Id : 23133, {_}: composition top zero =<= converse (composition (composition zero zero) (composition top top)) [] by Demod 23132 with 8187 at 3
% 275.54/69.23 Id : 23134, {_}: composition top zero =<= converse (composition zero (composition zero (composition top top))) [] by Demod 23133 with 6 at 1,3
% 275.54/69.23 Id : 1242, {_}: converse (composition zero ?1840) =<= composition (converse ?1840) zero [1840] by Super 135 with 1163 at 1,1,2
% 275.54/69.23 Id : 1253, {_}: converse (composition zero zero) =>= composition zero zero [] by Super 1242 with 1163 at 1,3
% 275.54/69.23 Id : 1288, {_}: converse (composition (composition zero zero) ?1881) =<= composition (converse ?1881) (composition zero zero) [1881] by Super 11 with 1253 at 2,3
% 275.54/69.23 Id : 1307, {_}: converse (composition zero (composition zero ?1881)) =<= composition (converse ?1881) (composition zero zero) [1881] by Demod 1288 with 6 at 1,2
% 275.54/69.23 Id : 3403, {_}: converse (composition zero (composition zero (composition top top))) =>= composition (composition top top) (composition zero zero) [] by Super 1307 with 3344 at 1,3
% 275.54/69.23 Id : 3460, {_}: converse (composition zero (composition zero (composition top top))) =>= composition top (composition top (composition zero zero)) [] by Demod 3403 with 6 at 3
% 275.54/69.23 Id : 23135, {_}: composition top zero =<= composition top (composition top (composition zero zero)) [] by Demod 23134 with 3460 at 3
% 275.54/69.23 Id : 1971, {_}: converse (join ?2478 (composition zero zero)) =<= join (converse ?2478) (composition zero zero) [2478] by Super 122 with 1253 at 2,1,2
% 275.54/69.23 Id : 1331, {_}: converse (composition ?1929 zero) =<= composition zero (converse ?1929) [1929] by Super 11 with 1163 at 1,3
% 275.54/69.23 Id : 701, {_}: converse (join one ?1245) =<= join one (converse ?1245) [1245] by Super 123 with 608 at 1,1,2
% 275.54/69.23 Id : 706, {_}: converse (join one one) =>= join one one [] by Super 701 with 608 at 2,3
% 275.54/69.23 Id : 1337, {_}: converse (composition (join one one) zero) =>= composition zero (join one one) [] by Super 1331 with 706 at 2,3
% 275.54/69.23 Id : 1984, {_}: converse (join (composition (join one one) zero) (composition zero zero)) =>= join (composition zero (join one one)) (composition zero zero) [] by Super 1971 with 1337 at 1,3
% 275.54/69.23 Id : 2028, {_}: converse (join (composition zero zero) (composition (join one one) zero)) =>= join (composition zero (join one one)) (composition zero zero) [] by Demod 1984 with 2 at 1,2
% 275.54/69.23 Id : 2029, {_}: converse (join (composition zero zero) (composition (join one one) zero)) =>= join (composition zero zero) (composition zero (join one one)) [] by Demod 2028 with 2 at 3
% 275.54/69.23 Id : 2030, {_}: converse (composition (join zero (join one one)) zero) =<= join (composition zero zero) (composition zero (join one one)) [] by Demod 2029 with 8 at 1,2
% 275.54/69.23 Id : 2031, {_}: converse (composition (join one one) zero) =<= join (composition zero zero) (composition zero (join one one)) [] by Demod 2030 with 1082 at 1,1,2
% 275.54/69.23 Id : 2032, {_}: composition zero (join one one) =<= join (composition zero zero) (composition zero (join one one)) [] by Demod 2031 with 1337 at 2
% 275.54/69.23 Id : 30298, {_}: composition zero one =<= join (composition zero zero) (composition zero (join one one)) [] by Demod 2032 with 10855 at 2,2
% 275.54/69.23 Id : 30299, {_}: composition zero one =<= join (composition zero zero) (composition zero one) [] by Demod 30298 with 10855 at 2,2,3
% 275.54/69.23 Id : 30300, {_}: zero =<= join (composition zero zero) (composition zero one) [] by Demod 30299 with 7 at 2
% 275.54/69.23 Id : 30301, {_}: zero =<= join (composition zero zero) zero [] by Demod 30300 with 7 at 2,3
% 275.54/69.23 Id : 30302, {_}: zero =<= join zero (composition zero zero) [] by Demod 30301 with 2 at 3
% 275.54/69.23 Id : 30303, {_}: zero =<= composition zero zero [] by Demod 30302 with 1082 at 3
% 275.54/69.23 Id : 30312, {_}: composition top zero =<= composition top (composition top zero) [] by Demod 23135 with 30303 at 2,2,3
% 275.54/69.23 Id : 31786, {_}: composition (composition top zero) (complement (converse (composition top zero))) =>= zero [] by Super 31782 with 30312 at 1,1,2,2
% 275.54/69.23 Id : 31871, {_}: composition top (composition zero (complement (converse (composition top zero)))) =>= zero [] by Demod 31786 with 6 at 2
% 275.54/69.23 Id : 3370, {_}: composition ?3651 (complement (converse (composition top ?3651))) =>= zero [3651] by Demod 3369 with 1082 at 2
% 275.54/69.23 Id : 31872, {_}: composition top zero =>= zero [] by Demod 31871 with 3370 at 2,2
% 275.54/69.23 Id : 32074, {_}: composition (join ?24021 top) zero =>= join (composition ?24021 zero) zero [24021] by Super 8 with 31872 at 2,3
% 275.54/69.23 Id : 32095, {_}: composition top zero =<= join (composition ?24021 zero) zero [24021] by Demod 32074 with 21084 at 1,2
% 275.54/69.23 Id : 32096, {_}: composition top zero =<= join zero (composition ?24021 zero) [24021] by Demod 32095 with 2 at 3
% 275.54/69.23 Id : 32097, {_}: zero =<= join zero (composition ?24021 zero) [24021] by Demod 32096 with 31872 at 2
% 275.54/69.23 Id : 32098, {_}: zero =<= composition ?24021 zero [24021] by Demod 32097 with 1082 at 3
% 275.54/69.23 Id : 32186, {_}: converse zero =<= composition (converse zero) ?24076 [24076] by Super 135 with 32098 at 1,2
% 275.54/69.23 Id : 32197, {_}: zero =<= composition (converse zero) ?24076 [24076] by Demod 32186 with 1163 at 2
% 275.54/69.23 Id : 32198, {_}: zero =<= composition zero ?24076 [24076] by Demod 32197 with 1163 at 1,3
% 275.54/69.23 Id : 692881, {_}: join (meet sk1 zero) (meet sk1 (composition (meet (complement sk3) ?664421) sk2)) =>= meet sk1 (composition zero sk2) [664421] by Demod 692880 with 32198 at 2,1,2
% 275.54/69.23 Id : 692882, {_}: join (meet sk1 zero) (meet sk1 (composition (meet (complement sk3) ?664421) sk2)) =>= meet sk1 zero [664421] by Demod 692881 with 32198 at 2,3
% 275.54/69.23 Id : 692883, {_}: join (meet zero sk1) (meet sk1 (composition (meet (complement sk3) ?664421) sk2)) =>= meet sk1 zero [664421] by Demod 692882 with 72 at 1,2
% 275.54/69.23 Id : 692884, {_}: join (meet zero sk1) (meet sk1 (composition (meet (complement sk3) ?664421) sk2)) =>= meet zero sk1 [664421] by Demod 692883 with 72 at 3
% 275.54/69.23 Id : 692885, {_}: join zero (meet sk1 (composition (meet (complement sk3) ?664421) sk2)) =>= meet zero sk1 [664421] by Demod 692884 with 21421 at 1,2
% 275.54/69.23 Id : 692886, {_}: join zero (meet sk1 (composition (meet (complement sk3) ?664421) sk2)) =>= zero [664421] by Demod 692885 with 21421 at 3
% 275.54/69.23 Id : 693082, {_}: meet sk1 (composition (meet (complement sk3) ?664596) sk2) =>= zero [664596] by Demod 692886 with 1082 at 2
% 275.54/69.23 Id : 693085, {_}: meet sk1 (composition (complement sk3) sk2) =>= zero [] by Super 693082 with 1104 at 1,2,2
% 275.54/69.23 Id : 693322, {_}: sk1 =<= join zero (meet sk1 (complement (composition (complement sk3) sk2))) [] by Super 11244 with 693085 at 1,3
% 275.54/69.23 Id : 693430, {_}: sk1 =<= meet sk1 (complement (composition (complement sk3) sk2)) [] by Demod 693322 with 1082 at 3
% 275.54/69.23 Id : 693512, {_}: join (complement sk1) (composition (complement sk3) sk2) =>= complement sk1 [] by Super 10500 with 693430 at 1,3
% 275.54/69.23 Id : 693564, {_}: join (composition (complement sk3) sk2) (complement sk1) =>= complement sk1 [] by Demod 693512 with 2 at 2
% 275.54/69.23 Id : 693945, {_}: complement sk1 === complement sk1 [] by Demod 1 with 693564 at 2
% 275.54/69.23 Id : 1, {_}: join (composition (complement sk3) sk2) (complement sk1) =>= complement sk1 [] by goals_18
% 275.54/69.23 % SZS output end CNFRefutation for theBenchmark.p
% 275.54/69.23 25271: solved /export/starexec/sandbox/benchmark/theBenchmark.p in 68.840467 using nrkbo
%------------------------------------------------------------------------------