%------------------------------------------------------------------------------
% File : Matita---1.0
% Problem : REL015-1 : TPTP v8.1.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : matitaprover --timeout %d --tptppath /export/starexec/sandbox2/benchmark %s
% Computer : n003.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:03 EDT 2022
% Result : Unsatisfiable 9.78s 2.79s
% Output : CNFRefutation 9.78s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : REL015-1 : TPTP v8.1.0. Released v4.0.0.
% 0.07/0.12 % Command : matitaprover --timeout %d --tptppath /export/starexec/sandbox2/benchmark %s
% 0.12/0.33 % Computer : n003.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 600
% 0.12/0.33 % DateTime : Fri Jul 8 10:37:58 EDT 2022
% 0.12/0.33 % CPUTime :
% 0.12/0.34 31888: Facts:
% 0.12/0.34 31888: Id : 2, {_}:
% 0.12/0.34 join ?2 ?3 =?= join ?3 ?2
% 0.12/0.34 [3, 2] by maddux1_join_commutativity_1 ?2 ?3
% 0.12/0.34 31888: Id : 3, {_}:
% 0.12/0.34 join ?5 (join ?6 ?7) =?= join (join ?5 ?6) ?7
% 0.12/0.34 [7, 6, 5] by maddux2_join_associativity_2 ?5 ?6 ?7
% 0.12/0.34 31888: Id : 4, {_}:
% 0.12/0.34 ?9
% 0.12/0.34 =<=
% 0.12/0.34 join (complement (join (complement ?9) (complement ?10)))
% 0.12/0.34 (complement (join (complement ?9) ?10))
% 0.12/0.34 [10, 9] by maddux3_a_kind_of_de_Morgan_3 ?9 ?10
% 0.12/0.34 31888: Id : 5, {_}:
% 0.12/0.34 meet ?12 ?13 =<= complement (join (complement ?12) (complement ?13))
% 0.12/0.34 [13, 12] by maddux4_definiton_of_meet_4 ?12 ?13
% 0.12/0.34 31888: Id : 6, {_}:
% 0.12/0.34 composition ?15 (composition ?16 ?17)
% 0.12/0.34 =?=
% 0.12/0.34 composition (composition ?15 ?16) ?17
% 0.12/0.34 [17, 16, 15] by composition_associativity_5 ?15 ?16 ?17
% 0.12/0.34 31888: Id : 7, {_}: composition ?19 one =>= ?19 [19] by composition_identity_6 ?19
% 0.12/0.34 31888: Id : 8, {_}:
% 0.12/0.34 composition (join ?21 ?22) ?23
% 0.12/0.34 =<=
% 0.12/0.34 join (composition ?21 ?23) (composition ?22 ?23)
% 0.12/0.34 [23, 22, 21] by composition_distributivity_7 ?21 ?22 ?23
% 0.12/0.34 31888: Id : 9, {_}:
% 0.12/0.34 converse (converse ?25) =>= ?25
% 0.12/0.34 [25] by converse_idempotence_8 ?25
% 0.12/0.34 31888: Id : 10, {_}:
% 0.12/0.34 converse (join ?27 ?28) =<= join (converse ?27) (converse ?28)
% 0.12/0.34 [28, 27] by converse_additivity_9 ?27 ?28
% 0.12/0.34 31888: Id : 11, {_}:
% 0.12/0.34 converse (composition ?30 ?31)
% 0.12/0.34 =<=
% 0.12/0.34 composition (converse ?31) (converse ?30)
% 0.12/0.34 [31, 30] by converse_multiplicativity_10 ?30 ?31
% 0.12/0.34 31888: Id : 12, {_}:
% 0.12/0.34 join (composition (converse ?33) (complement (composition ?33 ?34)))
% 0.12/0.34 (complement ?34)
% 0.12/0.34 =>=
% 0.12/0.34 complement ?34
% 0.12/0.34 [34, 33] by converse_cancellativity_11 ?33 ?34
% 0.12/0.34 31888: Id : 13, {_}: top =<= join ?36 (complement ?36) [36] by def_top_12 ?36
% 0.12/0.34 31888: Id : 14, {_}: zero =<= meet ?38 (complement ?38) [38] by def_zero_13 ?38
% 0.12/0.34 31888: Goal:
% 0.12/0.34 31888: Id : 1, {_}: composition top top =>= top [] by goals_14
% 9.78/2.79 Statistics :
% 9.78/2.79 Max weight : 16
% 9.78/2.79 Found proof, 2.450339s
% 9.78/2.79 % SZS status Unsatisfiable for theBenchmark.p
% 9.78/2.79 % SZS output start CNFRefutation for theBenchmark.p
% 9.78/2.79 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
% 9.78/2.79 Id : 14, {_}: zero =<= meet ?38 (complement ?38) [38] by def_zero_13 ?38
% 9.78/2.79 Id : 5, {_}: meet ?12 ?13 =<= complement (join (complement ?12) (complement ?13)) [13, 12] by maddux4_definiton_of_meet_4 ?12 ?13
% 9.78/2.79 Id : 3, {_}: join ?5 (join ?6 ?7) =?= join (join ?5 ?6) ?7 [7, 6, 5] by maddux2_join_associativity_2 ?5 ?6 ?7
% 9.78/2.79 Id : 116, {_}: converse (join ?343 ?344) =<= join (converse ?343) (converse ?344) [344, 343] by converse_additivity_9 ?343 ?344
% 9.78/2.79 Id : 11, {_}: converse (composition ?30 ?31) =<= composition (converse ?31) (converse ?30) [31, 30] by converse_multiplicativity_10 ?30 ?31
% 9.78/2.79 Id : 12, {_}: join (composition (converse ?33) (complement (composition ?33 ?34))) (complement ?34) =>= complement ?34 [34, 33] by converse_cancellativity_11 ?33 ?34
% 9.78/2.79 Id : 8, {_}: composition (join ?21 ?22) ?23 =<= join (composition ?21 ?23) (composition ?22 ?23) [23, 22, 21] by composition_distributivity_7 ?21 ?22 ?23
% 9.78/2.79 Id : 7, {_}: composition ?19 one =>= ?19 [19] by composition_identity_6 ?19
% 9.78/2.79 Id : 9, {_}: converse (converse ?25) =>= ?25 [25] by converse_idempotence_8 ?25
% 9.78/2.79 Id : 129, {_}: converse (composition ?373 ?374) =<= composition (converse ?374) (converse ?373) [374, 373] by converse_multiplicativity_10 ?373 ?374
% 9.78/2.79 Id : 13, {_}: top =<= join ?36 (complement ?36) [36] by def_top_12 ?36
% 9.78/2.79 Id : 2, {_}: join ?2 ?3 =?= join ?3 ?2 [3, 2] by maddux1_join_commutativity_1 ?2 ?3
% 9.78/2.79 Id : 154, {_}: join (complement ?432) ?432 =>= top [432] by Super 2 with 13 at 3
% 9.78/2.79 Id : 430, {_}: converse (composition (converse ?816) ?817) =>= composition (converse ?817) ?816 [817, 816] by Super 129 with 9 at 2,3
% 9.78/2.79 Id : 435, {_}: converse (converse ?834) =<= composition (converse one) ?834 [834] by Super 430 with 7 at 1,2
% 9.78/2.79 Id : 450, {_}: ?834 =<= composition (converse one) ?834 [834] by Demod 435 with 9 at 2
% 9.78/2.79 Id : 458, {_}: one =<= converse one [] by Super 7 with 450 at 2
% 9.78/2.79 Id : 475, {_}: ?834 =<= composition one ?834 [834] by Demod 450 with 458 at 1,3
% 9.78/2.79 Id : 134, {_}: join (complement ?34) (composition (converse ?33) (complement (composition ?33 ?34))) =>= complement ?34 [33, 34] by Demod 12 with 2 at 2
% 9.78/2.79 Id : 117, {_}: converse (join ?346 (converse ?347)) =>= join (converse ?346) ?347 [347, 346] by Super 116 with 9 at 2,3
% 9.78/2.79 Id : 483, {_}: join (complement ?885) (composition one (complement (composition one ?885))) =>= complement ?885 [885] by Super 134 with 458 at 1,2,2
% 9.78/2.79 Id : 491, {_}: join (complement ?885) (complement (composition one ?885)) =>= complement ?885 [885] by Demod 483 with 475 at 2,2
% 9.78/2.79 Id : 492, {_}: join (complement ?885) (complement ?885) =>= complement ?885 [885] by Demod 491 with 475 at 1,2,2
% 9.78/2.79 Id : 776, {_}: join (complement ?1206) (complement ?1206) =>= complement ?1206 [1206] by Demod 491 with 475 at 1,2,2
% 9.78/2.79 Id : 157, {_}: meet ?438 (complement ?438) =>= complement top [438] by Super 5 with 13 at 1,3
% 9.78/2.79 Id : 186, {_}: zero =<= complement top [] by Demod 157 with 14 at 2
% 9.78/2.79 Id : 778, {_}: join (complement top) zero =>= complement top [] by Super 776 with 186 at 2,2
% 9.78/2.79 Id : 792, {_}: join zero (complement top) =>= complement top [] by Demod 778 with 2 at 2
% 9.78/2.79 Id : 793, {_}: join zero (complement top) =>= zero [] by Demod 792 with 186 at 3
% 9.78/2.79 Id : 794, {_}: join zero zero =>= zero [] by Demod 793 with 186 at 2,2
% 9.78/2.79 Id : 853, {_}: join zero (join zero ?1248) =>= join zero ?1248 [1248] by Super 3 with 794 at 1,3
% 9.78/2.79 Id : 55, {_}: ?9 =<= join (meet ?9 ?10) (complement (join (complement ?9) ?10)) [10, 9] by Demod 4 with 5 at 1,3
% 9.78/2.79 Id : 56, {_}: ?9 =<= join (complement (join (complement ?9) ?10)) (meet ?9 ?10) [10, 9] by Demod 55 with 2 at 3
% 9.78/2.79 Id : 165, {_}: ?453 =<= join (complement (join (complement ?453) (complement ?453))) zero [453] by Super 56 with 14 at 2,3
% 9.78/2.79 Id : 169, {_}: ?453 =<= join zero (complement (join (complement ?453) (complement ?453))) [453] by Demod 165 with 2 at 3
% 9.78/2.79 Id : 170, {_}: ?453 =<= join zero (meet ?453 ?453) [453] by Demod 169 with 5 at 2,3
% 9.78/2.79 Id : 772, {_}: meet ?1198 ?1198 =>= complement (complement ?1198) [1198] by Super 5 with 492 at 1,3
% 9.78/2.79 Id : 831, {_}: ?453 =<= join zero (complement (complement ?453)) [453] by Demod 170 with 772 at 2,3
% 9.78/2.79 Id : 860, {_}: join zero ?1259 =<= join zero (complement (complement ?1259)) [1259] by Super 853 with 831 at 2,2
% 9.78/2.79 Id : 872, {_}: join zero ?1259 =>= ?1259 [1259] by Demod 860 with 831 at 3
% 9.78/2.79 Id : 895, {_}: top =<= complement zero [] by Super 13 with 872 at 3
% 9.78/2.79 Id : 911, {_}: join (complement zero) top =>= complement zero [] by Super 492 with 895 at 2,2
% 9.78/2.79 Id : 930, {_}: join top (complement zero) =>= complement zero [] by Demod 911 with 2 at 2
% 9.78/2.79 Id : 931, {_}: join top (complement zero) =>= top [] by Demod 930 with 895 at 3
% 9.78/2.79 Id : 932, {_}: join top top =>= top [] by Demod 931 with 895 at 2,2
% 9.78/2.79 Id : 1251, {_}: join top (join top ?1585) =>= join top ?1585 [1585] by Super 3 with 932 at 1,3
% 9.78/2.79 Id : 1252, {_}: join top (join ?1587 top) =>= join top ?1587 [1587] by Super 1251 with 2 at 2,2
% 9.78/2.79 Id : 374, {_}: converse (join ?696 (converse ?697)) =>= join (converse ?696) ?697 [697, 696] by Super 116 with 9 at 2,3
% 9.78/2.79 Id : 378, {_}: converse top =<= join (converse (complement (converse ?709))) ?709 [709] by Super 374 with 154 at 1,2
% 9.78/2.79 Id : 2390, {_}: join top (converse top) =<= join top (converse (complement (converse top))) [] by Super 1252 with 378 at 2,2
% 9.78/2.79 Id : 2478, {_}: converse (join top (converse top)) =<= join (converse top) (complement (converse top)) [] by Super 117 with 2390 at 1,2
% 9.78/2.79 Id : 2481, {_}: join (converse top) top =<= join (converse top) (complement (converse top)) [] by Demod 2478 with 117 at 2
% 9.78/2.79 Id : 2482, {_}: join (converse top) top =>= top [] by Demod 2481 with 13 at 3
% 9.78/2.79 Id : 2483, {_}: join top (converse top) =>= top [] by Demod 2482 with 2 at 2
% 9.78/2.79 Id : 2493, {_}: converse top =<= join (converse top) top [] by Super 117 with 2483 at 1,2
% 9.78/2.79 Id : 2496, {_}: converse top =<= join top (converse top) [] by Demod 2493 with 2 at 3
% 9.78/2.79 Id : 2497, {_}: converse top =>= top [] by Demod 2496 with 2483 at 3
% 9.78/2.79 Id : 2520, {_}: converse (composition top ?2642) =<= composition (converse ?2642) top [2642] by Super 11 with 2497 at 2,3
% 9.78/2.79 Id : 2818, {_}: join (complement top) (composition (converse (converse ?2897)) (complement (converse (composition top ?2897)))) =>= complement top [2897] by Super 134 with 2520 at 1,2,2,2
% 9.78/2.79 Id : 2852, {_}: join zero (composition (converse (converse ?2897)) (complement (converse (composition top ?2897)))) =>= complement top [2897] by Demod 2818 with 186 at 1,2
% 9.78/2.79 Id : 2853, {_}: join zero (composition ?2897 (complement (converse (composition top ?2897)))) =>= complement top [2897] by Demod 2852 with 9 at 1,2,2
% 9.78/2.79 Id : 2854, {_}: join zero (composition ?2897 (complement (converse (composition top ?2897)))) =>= zero [2897] by Demod 2853 with 186 at 3
% 9.78/2.79 Id : 33197, {_}: composition ?23932 (complement (converse (composition top ?23932))) =>= zero [23932] by Demod 2854 with 872 at 2
% 9.78/2.79 Id : 131, {_}: converse (composition ?379 (converse ?380)) =>= composition ?380 (converse ?379) [380, 379] by Super 129 with 9 at 1,3
% 9.78/2.79 Id : 2658, {_}: converse (composition ?2760 top) =<= composition top (converse ?2760) [2760] by Super 131 with 2497 at 2,1,2
% 9.78/2.79 Id : 2675, {_}: converse (composition top top) =>= composition top top [] by Super 2658 with 2497 at 2,3
% 9.78/2.79 Id : 33203, {_}: composition top (complement (composition top top)) =>= zero [] by Super 33197 with 2675 at 1,2,2
% 9.78/2.79 Id : 33299, {_}: composition (join ?23982 top) (complement (composition top top)) =<= join (composition ?23982 (complement (composition top top))) zero [23982] by Super 8 with 33203 at 2,3
% 9.78/2.79 Id : 20513, {_}: join ?13323 (join (complement ?13323) ?13324) =>= join top ?13324 [13324, 13323] by Super 3 with 13 at 1,3
% 9.78/2.79 Id : 20522, {_}: join ?13348 (complement ?13348) =?= join top (complement ?13348) [13348] by Super 20513 with 492 at 2,2
% 9.78/2.79 Id : 20694, {_}: top =<= join top (complement ?13348) [13348] by Demod 20522 with 13 at 2
% 9.78/2.79 Id : 876, {_}: ?453 =<= complement (complement ?453) [453] by Demod 831 with 872 at 3
% 9.78/2.79 Id : 916, {_}: meet zero ?1291 =<= complement (join top (complement ?1291)) [1291] by Super 5 with 895 at 1,1,3
% 9.78/2.79 Id : 1143, {_}: join top (complement ?1491) =>= complement (meet zero ?1491) [1491] by Super 876 with 916 at 1,3
% 9.78/2.79 Id : 20815, {_}: top =<= complement (meet zero ?13466) [13466] by Demod 20694 with 1143 at 3
% 9.78/2.79 Id : 1154, {_}: meet zero ?1517 =<= complement (join top (complement ?1517)) [1517] by Super 5 with 895 at 1,1,3
% 9.78/2.79 Id : 1157, {_}: meet zero (complement ?1523) =>= complement (join top ?1523) [1523] by Super 1154 with 876 at 2,1,3
% 9.78/2.79 Id : 20818, {_}: top =<= complement (complement (join top ?13470)) [13470] by Super 20815 with 1157 at 1,3
% 9.78/2.79 Id : 20848, {_}: top =<= join top ?13470 [13470] by Demod 20818 with 876 at 3
% 9.78/2.79 Id : 21068, {_}: join ?13507 top =>= top [13507] by Super 2 with 20848 at 3
% 9.78/2.79 Id : 33310, {_}: composition top (complement (composition top top)) =<= join (composition ?23982 (complement (composition top top))) zero [23982] by Demod 33299 with 21068 at 1,2
% 9.78/2.79 Id : 33311, {_}: composition top (complement (composition top top)) =<= join zero (composition ?23982 (complement (composition top top))) [23982] by Demod 33310 with 2 at 3
% 9.78/2.79 Id : 33312, {_}: zero =<= join zero (composition ?23982 (complement (composition top top))) [23982] by Demod 33311 with 33203 at 2
% 9.78/2.79 Id : 33313, {_}: zero =<= composition ?23982 (complement (composition top top)) [23982] by Demod 33312 with 872 at 3
% 9.78/2.79 Id : 33346, {_}: complement (composition top top) =>= zero [] by Super 475 with 33313 at 3
% 9.78/2.79 Id : 33692, {_}: join zero (composition top top) =>= top [] by Super 154 with 33346 at 1,2
% 9.78/2.79 Id : 33705, {_}: composition top top =>= top [] by Demod 33692 with 872 at 2
% 9.78/2.79 Id : 33848, {_}: top === top [] by Demod 1 with 33705 at 2
% 9.78/2.79 Id : 1, {_}: composition top top =>= top [] by goals_14
% 9.78/2.79 % SZS output end CNFRefutation for theBenchmark.p
% 9.78/2.79 31891: solved /export/starexec/sandbox2/benchmark/theBenchmark.p in 2.452482 using nrkbo
%------------------------------------------------------------------------------