%------------------------------------------------------------------------------
% File : Matita---1.0
% Problem : LAT007-1 : TPTP v8.1.0. Released v2.2.0.
% Transfm : none
% Format : tptp:raw
% Command : matitaprover --timeout %d --tptppath /export/starexec/sandbox/benchmark %s
% Computer : n020.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 05:55:33 EDT 2022
% Result : Unsatisfiable 13.12s 3.60s
% Output : CNFRefutation 13.12s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : LAT007-1 : TPTP v8.1.0. Released v2.2.0.
% 0.07/0.12 % Command : matitaprover --timeout %d --tptppath /export/starexec/sandbox/benchmark %s
% 0.12/0.33 % Computer : n020.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 : Tue Jun 28 22:25:16 EDT 2022
% 0.12/0.34 % CPUTime :
% 0.12/0.34 23978: Facts:
% 0.12/0.34 23978: Id : 2, {_}: meet ?2 (join ?2 ?3) =>= ?2 [3, 2] by absorption ?2 ?3
% 0.12/0.34 23978: Id : 3, {_}:
% 0.12/0.34 meet ?5 (join ?6 ?7) =<= join (meet ?7 ?5) (meet ?6 ?5)
% 0.12/0.34 [7, 6, 5] by distribution ?5 ?6 ?7
% 0.12/0.34 23978: Goal:
% 0.12/0.34 23978: Id : 1, {_}:
% 0.12/0.34 join (join a b) c =>= join a (join b c)
% 0.12/0.34 [] by prove_associativity_of_join
% 13.12/3.60 Statistics :
% 13.12/3.60 Max weight : 22
% 13.12/3.60 Found proof, 3.259222s
% 13.12/3.60 % SZS status Unsatisfiable for theBenchmark.p
% 13.12/3.60 % SZS output start CNFRefutation for theBenchmark.p
% 13.12/3.60 Id : 3, {_}: meet ?5 (join ?6 ?7) =<= join (meet ?7 ?5) (meet ?6 ?5) [7, 6, 5] by distribution ?5 ?6 ?7
% 13.12/3.60 Id : 2, {_}: meet ?2 (join ?2 ?3) =>= ?2 [3, 2] by absorption ?2 ?3
% 13.12/3.60 Id : 7, {_}: meet ?18 (join ?19 ?20) =<= join (meet ?20 ?18) (meet ?19 ?18) [20, 19, 18] by distribution ?18 ?19 ?20
% 13.12/3.60 Id : 8, {_}: meet (join ?22 ?23) (join ?22 ?24) =<= join (meet ?24 (join ?22 ?23)) ?22 [24, 23, 22] by Super 7 with 2 at 2,3
% 13.12/3.60 Id : 13, {_}: meet (meet ?44 ?45) (meet ?45 (join ?46 ?44)) =>= meet ?44 ?45 [46, 45, 44] by Super 2 with 3 at 2,2
% 13.12/3.60 Id : 15, {_}: meet (meet ?53 ?54) ?54 =>= meet ?53 ?54 [54, 53] by Super 13 with 2 at 2,2
% 13.12/3.60 Id : 21, {_}: meet ?68 (join (meet ?69 ?68) ?70) =<= join (meet ?70 ?68) (meet ?69 ?68) [70, 69, 68] by Super 3 with 15 at 2,3
% 13.12/3.60 Id : 69, {_}: meet ?209 (join (meet ?210 ?209) ?211) =>= meet ?209 (join ?210 ?211) [211, 210, 209] by Demod 21 with 3 at 3
% 13.12/3.60 Id : 74, {_}: meet ?231 (meet ?231 (join ?232 ?233)) =<= meet ?231 (join ?233 (meet ?232 ?231)) [233, 232, 231] by Super 69 with 3 at 2,2
% 13.12/3.60 Id : 22, {_}: meet ?72 (join ?73 (meet ?74 ?72)) =<= join (meet ?74 ?72) (meet ?73 ?72) [74, 73, 72] by Super 3 with 15 at 1,3
% 13.12/3.60 Id : 33, {_}: meet ?72 (join ?73 (meet ?74 ?72)) =>= meet ?72 (join ?73 ?74) [74, 73, 72] by Demod 22 with 3 at 3
% 13.12/3.60 Id : 219, {_}: meet ?572 (meet ?572 (join ?573 ?574)) =>= meet ?572 (join ?574 ?573) [574, 573, 572] by Demod 74 with 33 at 3
% 13.12/3.60 Id : 224, {_}: meet ?597 ?597 =<= meet ?597 (join ?598 ?597) [598, 597] by Super 219 with 2 at 2,2
% 13.12/3.60 Id : 244, {_}: meet (join ?635 ?636) (join ?635 ?636) =>= join (meet ?636 ?636) ?635 [636, 635] by Super 8 with 224 at 1,3
% 13.12/3.60 Id : 247, {_}: meet ?644 ?644 =>= ?644 [644] by Super 2 with 224 at 2
% 13.12/3.60 Id : 1720, {_}: join ?635 ?636 =<= join (meet ?636 ?636) ?635 [636, 635] by Demod 244 with 247 at 2
% 13.12/3.60 Id : 1721, {_}: join ?635 ?636 =?= join ?636 ?635 [636, 635] by Demod 1720 with 247 at 1,3
% 13.12/3.60 Id : 359, {_}: meet ?904 (join ?905 ?904) =<= join ?904 (meet ?905 ?904) [905, 904] by Super 3 with 247 at 1,3
% 13.12/3.60 Id : 349, {_}: ?597 =<= meet ?597 (join ?598 ?597) [598, 597] by Demod 224 with 247 at 2
% 13.12/3.60 Id : 386, {_}: ?904 =<= join ?904 (meet ?905 ?904) [905, 904] by Demod 359 with 349 at 2
% 13.12/3.60 Id : 32, {_}: meet ?68 (join (meet ?69 ?68) ?70) =>= meet ?68 (join ?69 ?70) [70, 69, 68] by Demod 21 with 3 at 3
% 13.12/3.60 Id : 36, {_}: meet (join ?109 ?110) (join ?109 ?111) =<= join (meet ?111 (join ?109 ?110)) ?109 [111, 110, 109] by Super 7 with 2 at 2,3
% 13.12/3.60 Id : 39, {_}: meet (join ?123 ?124) (join ?123 ?123) =>= join ?123 ?123 [124, 123] by Super 36 with 2 at 1,3
% 13.12/3.60 Id : 6, {_}: meet (meet ?14 ?15) (meet ?15 (join ?16 ?14)) =>= meet ?14 ?15 [16, 15, 14] by Super 2 with 3 at 2,2
% 13.12/3.60 Id : 11, {_}: meet (meet ?34 (join ?35 ?36)) (join (meet ?36 ?34) ?37) =<= join (meet ?37 (meet ?34 (join ?35 ?36))) (meet ?36 ?34) [37, 36, 35, 34] by Super 3 with 6 at 2,3
% 13.12/3.60 Id : 364, {_}: meet (meet ?919 (join ?920 ?919)) (join (meet ?919 ?919) ?921) =>= join (meet ?921 (meet ?919 (join ?920 ?919))) ?919 [921, 920, 919] by Super 11 with 247 at 2,3
% 13.12/3.60 Id : 370, {_}: meet ?919 (join (meet ?919 ?919) ?921) =<= join (meet ?921 (meet ?919 (join ?920 ?919))) ?919 [920, 921, 919] by Demod 364 with 349 at 1,2
% 13.12/3.60 Id : 371, {_}: meet ?919 (join ?919 ?921) =<= join (meet ?921 (meet ?919 (join ?920 ?919))) ?919 [920, 921, 919] by Demod 370 with 247 at 1,2,2
% 13.12/3.60 Id : 372, {_}: meet ?919 (join ?919 ?921) =<= join (meet ?921 ?919) ?919 [921, 919] by Demod 371 with 349 at 2,1,3
% 13.12/3.60 Id : 411, {_}: ?977 =<= join (meet ?978 ?977) ?977 [978, 977] by Demod 372 with 2 at 2
% 13.12/3.60 Id : 419, {_}: ?1004 =<= join ?1004 ?1004 [1004] by Super 411 with 247 at 1,3
% 13.12/3.60 Id : 438, {_}: meet (join ?123 ?124) ?123 =>= join ?123 ?123 [124, 123] by Demod 39 with 419 at 2,2
% 13.12/3.60 Id : 439, {_}: meet (join ?123 ?124) ?123 =>= ?123 [124, 123] by Demod 438 with 419 at 3
% 13.12/3.60 Id : 420, {_}: join ?1006 ?1007 =<= join ?1007 (join ?1006 ?1007) [1007, 1006] by Super 411 with 349 at 1,3
% 13.12/3.60 Id : 709, {_}: meet (join ?1606 ?1607) ?1607 =>= ?1607 [1607, 1606] by Super 439 with 420 at 1,2
% 13.12/3.60 Id : 1053, {_}: meet ?2271 (join ?2271 ?2272) =<= meet ?2271 (join (join ?2273 ?2271) ?2272) [2273, 2272, 2271] by Super 32 with 709 at 1,2,2
% 13.12/3.60 Id : 1086, {_}: ?2271 =<= meet ?2271 (join (join ?2273 ?2271) ?2272) [2272, 2273, 2271] by Demod 1053 with 2 at 2
% 13.12/3.60 Id : 3027, {_}: join (join ?5716 ?5717) ?5718 =<= join (join (join ?5716 ?5717) ?5718) ?5717 [5718, 5717, 5716] by Super 386 with 1086 at 2,3
% 13.12/3.60 Id : 7549, {_}: join (join ?14001 ?14002) ?14003 =<= join ?14002 (join (join ?14001 ?14002) ?14003) [14003, 14002, 14001] by Demod 3027 with 1721 at 3
% 13.12/3.60 Id : 7550, {_}: join (join ?14005 ?14006) ?14007 =<= join ?14006 (join (join ?14006 ?14005) ?14007) [14007, 14006, 14005] by Super 7549 with 1721 at 1,2,3
% 13.12/3.60 Id : 3039, {_}: ?5765 =<= meet ?5765 (join (join ?5766 ?5765) ?5767) [5767, 5766, 5765] by Demod 1053 with 2 at 2
% 13.12/3.60 Id : 3040, {_}: ?5769 =<= meet ?5769 (join (join ?5769 ?5770) ?5771) [5771, 5770, 5769] by Super 3039 with 1721 at 1,2,3
% 13.12/3.60 Id : 7322, {_}: join (join ?13486 ?13487) ?13488 =<= join (join (join ?13486 ?13487) ?13488) ?13486 [13488, 13487, 13486] by Super 386 with 3040 at 2,3
% 13.12/3.60 Id : 7432, {_}: join (join ?13486 ?13487) ?13488 =<= join ?13486 (join (join ?13486 ?13487) ?13488) [13488, 13487, 13486] by Demod 7322 with 1721 at 3
% 13.12/3.60 Id : 13454, {_}: join (join ?14005 ?14006) ?14007 =?= join (join ?14006 ?14005) ?14007 [14007, 14006, 14005] by Demod 7550 with 7432 at 3
% 13.12/3.60 Id : 706, {_}: meet (join ?1593 (join ?1594 ?1593)) (join ?1593 ?1595) =>= join (meet ?1595 (join ?1594 ?1593)) ?1593 [1595, 1594, 1593] by Super 8 with 420 at 2,1,3
% 13.12/3.60 Id : 729, {_}: meet (join ?1594 ?1593) (join ?1593 ?1595) =<= join (meet ?1595 (join ?1594 ?1593)) ?1593 [1595, 1593, 1594] by Demod 706 with 420 at 1,2
% 13.12/3.60 Id : 2201, {_}: meet (join ?4252 ?4253) (join ?4253 ?4254) =<= join ?4253 (meet ?4254 (join ?4252 ?4253)) [4254, 4253, 4252] by Demod 729 with 1721 at 3
% 13.12/3.60 Id : 446, {_}: meet ?1028 (join ?1029 ?1029) =>= meet ?1029 ?1028 [1029, 1028] by Super 3 with 419 at 3
% 13.12/3.60 Id : 462, {_}: meet ?1028 ?1029 =?= meet ?1029 ?1028 [1029, 1028] by Demod 446 with 419 at 2,2
% 13.12/3.60 Id : 2217, {_}: meet (join ?4318 ?4319) (join ?4319 ?4320) =<= join ?4319 (meet (join ?4318 ?4319) ?4320) [4320, 4319, 4318] by Super 2201 with 462 at 2,3
% 13.12/3.60 Id : 2214, {_}: meet (join (meet ?4307 ?4308) ?4309) (join ?4309 ?4308) =>= join ?4309 (meet ?4308 (join ?4307 ?4309)) [4309, 4308, 4307] by Super 2201 with 32 at 2,3
% 13.12/3.60 Id : 2277, {_}: meet (join ?4309 ?4308) (join (meet ?4307 ?4308) ?4309) =>= join ?4309 (meet ?4308 (join ?4307 ?4309)) [4307, 4308, 4309] by Demod 2214 with 462 at 2
% 13.12/3.60 Id : 2180, {_}: meet (join ?1594 ?1593) (join ?1593 ?1595) =<= join ?1593 (meet ?1595 (join ?1594 ?1593)) [1595, 1593, 1594] by Demod 729 with 1721 at 3
% 13.12/3.60 Id : 2278, {_}: meet (join ?4309 ?4308) (join (meet ?4307 ?4308) ?4309) =>= meet (join ?4307 ?4309) (join ?4309 ?4308) [4307, 4308, 4309] by Demod 2277 with 2180 at 3
% 13.12/3.60 Id : 210, {_}: meet ?231 (meet ?231 (join ?232 ?233)) =>= meet ?231 (join ?233 ?232) [233, 232, 231] by Demod 74 with 33 at 3
% 13.12/3.60 Id : 449, {_}: meet ?1037 (meet ?1037 ?1038) =?= meet ?1037 (join ?1038 ?1038) [1038, 1037] by Super 210 with 419 at 2,2,2
% 13.12/3.60 Id : 457, {_}: meet ?1037 (meet ?1037 ?1038) =>= meet ?1037 ?1038 [1038, 1037] by Demod 449 with 419 at 2,3
% 13.12/3.60 Id : 763, {_}: meet (meet ?1697 ?1698) (join (meet ?1697 ?1698) ?1699) =>= meet (meet ?1697 ?1698) (join ?1697 ?1699) [1699, 1698, 1697] by Super 32 with 457 at 1,2,2
% 13.12/3.60 Id : 794, {_}: meet ?1697 ?1698 =<= meet (meet ?1697 ?1698) (join ?1697 ?1699) [1699, 1698, 1697] by Demod 763 with 2 at 2
% 13.12/3.60 Id : 26874, {_}: meet (join ?49151 ?49152) (join ?49152 (meet ?49151 ?49153)) =>= join ?49152 (meet ?49151 ?49153) [49153, 49152, 49151] by Super 2180 with 794 at 2,3
% 13.12/3.60 Id : 26883, {_}: meet (join ?49192 ?49193) (join ?49193 (meet ?49194 ?49192)) =>= join ?49193 (meet ?49192 ?49194) [49194, 49193, 49192] by Super 26874 with 462 at 2,2,2
% 13.12/3.60 Id : 9, {_}: meet (join ?26 ?27) (join ?28 ?26) =<= join ?26 (meet ?28 (join ?26 ?27)) [28, 27, 26] by Super 7 with 2 at 1,3
% 13.12/3.60 Id : 81, {_}: meet (join ?248 (meet ?249 ?250)) (join ?250 ?248) =>= join ?248 (meet ?250 (join ?248 ?249)) [250, 249, 248] by Super 9 with 33 at 2,3
% 13.12/3.60 Id : 112, {_}: meet (join ?248 (meet ?249 ?250)) (join ?250 ?248) =>= meet (join ?248 ?249) (join ?250 ?248) [250, 249, 248] by Demod 81 with 9 at 3
% 13.12/3.60 Id : 17251, {_}: meet (join ?250 ?248) (join ?248 (meet ?249 ?250)) =>= meet (join ?248 ?249) (join ?250 ?248) [249, 248, 250] by Demod 112 with 462 at 2
% 13.12/3.60 Id : 27121, {_}: meet (join ?49193 ?49194) (join ?49192 ?49193) =>= join ?49193 (meet ?49192 ?49194) [49192, 49194, 49193] by Demod 26883 with 17251 at 2
% 13.12/3.60 Id : 27368, {_}: join ?4309 (meet (meet ?4307 ?4308) ?4308) =?= meet (join ?4307 ?4309) (join ?4309 ?4308) [4308, 4307, 4309] by Demod 2278 with 27121 at 2
% 13.12/3.60 Id : 27369, {_}: join ?4309 (meet ?4308 (meet ?4307 ?4308)) =?= meet (join ?4307 ?4309) (join ?4309 ?4308) [4307, 4308, 4309] by Demod 27368 with 462 at 2,2
% 13.12/3.60 Id : 448, {_}: meet ?1034 (meet ?1035 ?1034) =<= meet ?1034 (join (meet ?1035 ?1034) ?1035) [1035, 1034] by Super 33 with 419 at 2,2
% 13.12/3.60 Id : 458, {_}: meet ?1034 (meet ?1035 ?1034) =?= meet ?1034 (join ?1035 ?1035) [1035, 1034] by Demod 448 with 32 at 3
% 13.12/3.60 Id : 459, {_}: meet ?1034 (meet ?1035 ?1034) =>= meet ?1034 ?1035 [1035, 1034] by Demod 458 with 419 at 2,3
% 13.12/3.60 Id : 27370, {_}: join ?4309 (meet ?4308 ?4307) =<= meet (join ?4307 ?4309) (join ?4309 ?4308) [4307, 4308, 4309] by Demod 27369 with 459 at 2,2
% 13.12/3.60 Id : 27371, {_}: join ?4319 (meet ?4320 ?4318) =<= join ?4319 (meet (join ?4318 ?4319) ?4320) [4318, 4320, 4319] by Demod 2217 with 27370 at 2
% 13.12/3.60 Id : 27465, {_}: join ?50100 (meet (join ?50101 ?50102) ?50102) =?= join ?50100 (join ?50102 (meet ?50101 ?50100)) [50102, 50101, 50100] by Super 27371 with 27121 at 2,3
% 13.12/3.60 Id : 27573, {_}: join ?50100 (meet ?50102 (join ?50101 ?50102)) =?= join ?50100 (join ?50102 (meet ?50101 ?50100)) [50101, 50102, 50100] by Demod 27465 with 462 at 2,2
% 13.12/3.60 Id : 28712, {_}: join ?52633 ?52634 =<= join ?52633 (join ?52634 (meet ?52635 ?52633)) [52635, 52634, 52633] by Demod 27573 with 349 at 2,2
% 13.12/3.60 Id : 28713, {_}: join (join ?52637 ?52638) ?52639 =<= join (join ?52637 ?52638) (join ?52639 ?52637) [52639, 52638, 52637] by Super 28712 with 2 at 2,2,3
% 13.12/3.60 Id : 31066, {_}: join (join ?56469 ?56470) (join ?56470 ?56471) =>= join (join ?56470 ?56471) ?56469 [56471, 56470, 56469] by Super 1721 with 28713 at 3
% 13.12/3.60 Id : 1051, {_}: meet ?2263 (meet ?2263 (join ?2264 (join ?2265 ?2263))) =>= meet (join ?2265 ?2263) ?2263 [2265, 2264, 2263] by Super 6 with 709 at 1,2
% 13.12/3.60 Id : 1088, {_}: meet ?2263 (join ?2264 (join ?2265 ?2263)) =>= meet (join ?2265 ?2263) ?2263 [2265, 2264, 2263] by Demod 1051 with 457 at 2
% 13.12/3.60 Id : 1089, {_}: meet ?2263 (join ?2264 (join ?2265 ?2263)) =>= ?2263 [2265, 2264, 2263] by Demod 1088 with 709 at 3
% 13.12/3.60 Id : 3144, {_}: join ?5918 (join ?5919 ?5920) =<= join (join ?5918 (join ?5919 ?5920)) ?5920 [5920, 5919, 5918] by Super 386 with 1089 at 2,3
% 13.12/3.60 Id : 8382, {_}: join ?15751 (join ?15752 ?15753) =<= join ?15753 (join ?15751 (join ?15752 ?15753)) [15753, 15752, 15751] by Demod 3144 with 1721 at 3
% 13.12/3.60 Id : 8383, {_}: join ?15755 (join ?15756 ?15757) =<= join ?15757 (join ?15755 (join ?15757 ?15756)) [15757, 15756, 15755] by Super 8382 with 1721 at 2,2,3
% 13.12/3.60 Id : 3169, {_}: meet ?6027 (join ?6028 (join ?6029 ?6027)) =>= ?6027 [6029, 6028, 6027] by Demod 1088 with 709 at 3
% 13.12/3.60 Id : 3170, {_}: meet ?6031 (join ?6032 (join ?6031 ?6033)) =>= ?6031 [6033, 6032, 6031] by Super 3169 with 1721 at 2,2,2
% 13.12/3.60 Id : 8138, {_}: join ?15205 (join ?15206 ?15207) =<= join (join ?15205 (join ?15206 ?15207)) ?15206 [15207, 15206, 15205] by Super 386 with 3170 at 2,3
% 13.12/3.60 Id : 8260, {_}: join ?15205 (join ?15206 ?15207) =<= join ?15206 (join ?15205 (join ?15206 ?15207)) [15207, 15206, 15205] by Demod 8138 with 1721 at 3
% 13.12/3.60 Id : 14429, {_}: join ?15755 (join ?15756 ?15757) =?= join ?15755 (join ?15757 ?15756) [15757, 15756, 15755] by Demod 8383 with 8260 at 3
% 13.12/3.60 Id : 27574, {_}: join ?50100 ?50102 =<= join ?50100 (join ?50102 (meet ?50101 ?50100)) [50101, 50102, 50100] by Demod 27573 with 349 at 2,2
% 13.12/3.60 Id : 29546, {_}: join ?54252 (join (meet ?54253 ?54252) ?54254) =>= join ?54252 ?54254 [54254, 54253, 54252] by Super 14429 with 27574 at 3
% 13.12/3.60 Id : 29575, {_}: join (join ?54393 ?54394) (join ?54394 ?54395) =>= join (join ?54393 ?54394) ?54395 [54395, 54394, 54393] by Super 29546 with 349 at 1,2,2
% 13.12/3.60 Id : 32788, {_}: join (join ?56469 ?56470) ?56471 =?= join (join ?56470 ?56471) ?56469 [56471, 56470, 56469] by Demod 31066 with 29575 at 2
% 13.12/3.60 Id : 32881, {_}: join ?60532 (join ?60533 ?60534) =<= join (join ?60534 ?60532) ?60533 [60534, 60533, 60532] by Super 1721 with 32788 at 3
% 13.12/3.60 Id : 33289, {_}: join ?14006 (join ?14007 ?14005) =<= join (join ?14006 ?14005) ?14007 [14005, 14007, 14006] by Demod 13454 with 32881 at 2
% 13.12/3.60 Id : 33290, {_}: join ?14006 (join ?14007 ?14005) =?= join ?14005 (join ?14007 ?14006) [14005, 14007, 14006] by Demod 33289 with 32881 at 3
% 13.12/3.60 Id : 33271, {_}: join ?54394 (join (join ?54394 ?54395) ?54393) =>= join (join ?54393 ?54394) ?54395 [54393, 54395, 54394] by Demod 29575 with 32881 at 2
% 13.12/3.60 Id : 33272, {_}: join ?54394 (join (join ?54394 ?54395) ?54393) =>= join ?54394 (join ?54395 ?54393) [54393, 54395, 54394] by Demod 33271 with 32881 at 3
% 13.12/3.60 Id : 33273, {_}: join ?54394 (join ?54395 (join ?54393 ?54394)) =>= join ?54394 (join ?54395 ?54393) [54393, 54395, 54394] by Demod 33272 with 32881 at 2,2
% 13.12/3.60 Id : 3233, {_}: join ?5918 (join ?5919 ?5920) =<= join ?5920 (join ?5918 (join ?5919 ?5920)) [5920, 5919, 5918] by Demod 3144 with 1721 at 3
% 13.12/3.60 Id : 33320, {_}: join ?54395 (join ?54393 ?54394) =?= join ?54394 (join ?54395 ?54393) [54394, 54393, 54395] by Demod 33273 with 3233 at 2
% 13.12/3.60 Id : 33722, {_}: join a (join b c) =?= join a (join b c) [] by Demod 33721 with 1721 at 2,2
% 13.12/3.60 Id : 33721, {_}: join a (join c b) =?= join a (join b c) [] by Demod 33720 with 33320 at 2
% 13.12/3.60 Id : 33720, {_}: join b (join a c) =>= join a (join b c) [] by Demod 33719 with 33290 at 2
% 13.12/3.60 Id : 33719, {_}: join c (join a b) =>= join a (join b c) [] by Demod 1 with 1721 at 2
% 13.12/3.60 Id : 1, {_}: join (join a b) c =>= join a (join b c) [] by prove_associativity_of_join
% 13.12/3.60 % SZS output end CNFRefutation for theBenchmark.p
% 13.12/3.60 23979: solved /export/starexec/sandbox/benchmark/theBenchmark.p in 3.261955 using kbo
%------------------------------------------------------------------------------