%------------------------------------------------------------------------------ % File : Fiesta---2 % Problem : GRP114-1 : TPTP v8.1.0. Released v1.2.0. % Transfm : none % Format : dedam % Command : fiesta-wrapper %s % Computer : n012.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 : Sat Jul 16 09:12:30 EDT 2022 % Result : Unsatisfiable 1.86s 2.24s % Output : CNFRefutation 1.86s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : GRP114-1 : TPTP v8.1.0. Released v1.2.0. % 0.03/0.13 % Command : fiesta-wrapper %s % 0.13/0.34 % Computer : n012.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 : Tue Jun 14 01:39:40 EDT 2022 % 0.13/0.34 % CPUTime : % 1.86/2.24 Theorem Proved. % 1.86/2.24 % SZS status Unsatisfiable % 1.86/2.24 % SZS output start CNFRefutation % 1.86/2.24 [1=axiom,[], % 1.86/2.24 intersection(X10,identity) = negative_part(X10)]. % 1.86/2.24 [2=axiom,[], % 1.86/2.24 union(X10,identity) = positive_part(X10)]. % 1.86/2.24 [3=axiom,[], % 1.86/2.24 multiply(intersection(X10,X11),X12) = intersection(multiply(X10,X12),multiply(X11,X12))]. % 1.86/2.24 [4=axiom,[], % 1.86/2.24 multiply(union(X10,X11),X12) = union(multiply(X10,X12),multiply(X11,X12))]. % 1.86/2.24 [5=axiom,[], % 1.86/2.24 multiply(X10,intersection(X11,X12)) = intersection(multiply(X10,X11),multiply(X10,X12))]. % 1.86/2.24 [6=axiom,[], % 1.86/2.24 multiply(X10,union(X11,X12)) = union(multiply(X10,X11),multiply(X10,X12))]. % 1.86/2.24 [7=axiom,[], % 1.86/2.24 intersection(union(X10,X11),X11) = X11]. % 1.86/2.24 [8=axiom,[], % 1.86/2.24 union(intersection(X10,X11),X11) = X11]. % 1.86/2.24 [9=axiom,[], % 1.86/2.24 union(union(X10,X11),X12) = union(X10,union(X11,X12))]. % 1.86/2.24 [10=axiom,[], % 1.86/2.24 intersection(intersection(X10,X11),X12) = intersection(X10,intersection(X11,X12))]. % 1.86/2.24 [11=axiom,[], % 1.86/2.24 union(X10,X11) = union(X11,X10)]. % 1.86/2.24 [12=demod(8),[11], % 1.86/2.24 union(X10,intersection(X11,X10)) = X10]. % 1.86/2.24 [13=axiom,[], % 1.86/2.24 intersection(X10,X11) = intersection(X11,X10)]. % 1.86/2.24 [14=demod(7),[13], % 1.86/2.24 intersection(X10,union(X11,X10)) = X10]. % 1.86/2.24 [15=axiom,[], % 1.86/2.24 union(X10,X10) = X10]. % 1.86/2.24 [16=axiom,[], % 1.86/2.24 intersection(X10,X10) = X10]. % 1.86/2.24 [17=axiom,[], % 1.86/2.24 inverse(multiply(X10,X11)) = multiply(inverse(X11),inverse(X10))]. % 1.86/2.24 [18=axiom,[], % 1.86/2.24 inverse(inverse(X10)) = X10]. % 1.86/2.24 [19=axiom,[], % 1.86/2.24 inverse(identity) = identity]. % 1.86/2.24 [20=axiom,[], % 1.86/2.24 multiply(multiply(X10,X11),X12) = multiply(X10,multiply(X11,X12))]. % 1.86/2.24 [21=axiom,[], % 1.86/2.24 multiply(inverse(X10),X10) = identity]. % 1.86/2.24 [22=axiom,[], % 1.86/2.24 multiply(identity,X10) = X10]. % 1.86/2.24 [23=axiom,[], % 1.86/2.24 thtop(X10,X10) = thmfalse]. % 1.86/2.24 [24=axiom,[], % 1.86/2.24 thtop(multiply(positive_part(a),negative_part(a)),a) = thmtrue]. % 1.86/2.24 [27=param(3,1),[22,13], % 1.86/2.24 multiply(negative_part(X10),X11) = intersection(X11,multiply(X10,X11))]. % 1.86/2.24 [28=param(21,18),[], % 1.86/2.24 multiply(X10,inverse(X10)) = identity]. % 1.86/2.24 [29=param(28,3),[], % 1.86/2.24 intersection(multiply(X10,inverse(intersection(X10,X11))),multiply(X11,inverse(intersection(X10,X11)))) = identity]. % 1.86/2.24 [31=param(4,28),[], % 1.86/2.24 union(multiply(X10,inverse(union(X10,X11))),multiply(X11,inverse(union(X10,X11)))) = identity]. % 1.86/2.24 [32=param(14,2),[], % 1.86/2.24 intersection(identity,positive_part(X10)) = identity]. % 1.86/2.24 [34=param(5,1),[], % 1.86/2.24 multiply(X10,negative_part(X11)) = intersection(multiply(X10,X11),multiply(X10,identity))]. % 1.86/2.24 [35=param(5,21),[], % 1.86/2.24 intersection(multiply(inverse(intersection(X10,X11)),X10),multiply(inverse(intersection(X10,X11)),X11)) = identity]. % 1.86/2.24 [37=param(12,1),[], % 1.86/2.24 union(identity,negative_part(X10)) = identity]. % 1.86/2.24 [38=param(12,14),[11], % 1.86/2.24 union(X10,union(X11,X10)) = union(X11,X10)]. % 1.86/2.24 [39=param(14,12),[13], % 1.86/2.24 intersection(X10,intersection(X11,X10)) = intersection(X11,X10)]. % 1.86/2.24 [40=param(12,32),[2], % 1.86/2.24 positive_part(positive_part(X10)) = positive_part(X10)]. % 1.86/2.24 [41=param(6,2),[], % 1.86/2.24 multiply(X10,positive_part(X11)) = union(multiply(X10,X11),multiply(X10,identity))]. % 1.86/2.24 [42=param(6,21),[], % 1.86/2.24 union(multiply(inverse(union(X10,X11)),X10),multiply(inverse(union(X10,X11)),X11)) = identity]. % 1.86/2.24 [44=param(14,37),[1], % 1.86/2.24 negative_part(negative_part(X10)) = negative_part(X10)]. % 1.86/2.24 [45=param(9,2),[2], % 1.86/2.24 union(X10,positive_part(X11)) = positive_part(union(X10,X11))]. % 1.86/2.24 [46=param(9,2),[], % 1.86/2.24 union(positive_part(X10),X11) = union(X10,union(identity,X11))]. % 1.86/2.24 [50=param(9,15),[38], % 1.86/2.24 union(X10,union(X10,X11)) = union(X10,X11)]. % 1.86/2.24 [52=param(13,1),[], % 1.86/2.24 intersection(identity,X10) = negative_part(X10)]. % 1.86/2.24 [55=param(10,1),[1], % 1.86/2.24 intersection(X10,negative_part(X11)) = negative_part(intersection(X10,X11))]. % 1.86/2.24 [56=param(10,1),[52,55], % 1.86/2.24 intersection(negative_part(X10),X11) = negative_part(intersection(X10,X11))]. % 1.86/2.24 [62=param(10,16),[39], % 1.86/2.24 intersection(X10,intersection(X10,X11)) = intersection(X10,X11)]. % 1.86/2.24 [63=param(12,52),[], % 1.86/2.24 union(X10,negative_part(X10)) = X10]. % 1.86/2.24 [66=param(11,2),[], % 1.86/2.24 union(identity,X10) = positive_part(X10)]. % 1.86/2.24 [68=demod(46),[66,45], % 1.86/2.24 union(positive_part(X10),X11) = positive_part(union(X10,X11))]. % 1.86/2.24 [72=param(14,11),[], % 1.86/2.24 intersection(X10,union(X10,X11)) = X10]. % 1.86/2.24 [73=param(14,66),[], % 1.86/2.24 intersection(X10,positive_part(X10)) = X10]. % 1.86/2.24 [75=param(18,17),[], % 1.86/2.24 inverse(multiply(inverse(X10),inverse(X11))) = multiply(X11,X10)]. % 1.86/2.24 [76=demod(35),[-75,18,5,21,52,-75,18,5,21,1], % 1.86/2.24 intersection(inverse(negative_part(multiply(inverse(X10),X11))),inverse(negative_part(multiply(inverse(X11),X10)))) = identity]. % 1.86/2.24 [77=demod(42),[-75,18,6,21,66,-75,18,6,21,2], % 1.86/2.24 union(inverse(positive_part(multiply(inverse(X10),X11))),inverse(positive_part(multiply(inverse(X11),X10)))) = identity]. % 1.86/2.24 [80=param(17,18),[], % 1.86/2.24 multiply(X10,inverse(X11)) = inverse(multiply(X11,inverse(X10)))]. % 1.86/2.24 [82=param(17,19),[22], % 1.86/2.24 inverse(multiply(X10,identity)) = inverse(X10)]. % 1.86/2.24 [88=param(18,82),[18], % 1.86/2.24 multiply(X10,identity) = X10]. % 1.86/2.24 [89=demod(41),[88,11], % 1.86/2.24 multiply(X10,positive_part(X11)) = union(X10,multiply(X10,X11))]. % 1.86/2.24 [90=demod(34),[88,13], % 1.86/2.24 multiply(X10,negative_part(X11)) = intersection(X10,multiply(X10,X11))]. % 1.86/2.24 [93=param(20,21),[22], % 1.86/2.24 multiply(inverse(X11),multiply(X11,X10)) = X10]. % 1.86/2.24 [95=param(20,28),[22], % 1.86/2.24 multiply(X11,multiply(inverse(X11),X10)) = X10]. % 1.86/2.24 [117=param(72,68),[], % 1.86/2.24 intersection(positive_part(X10),positive_part(union(X10,X11))) = positive_part(X10)]. % 1.86/2.24 [163=param(93,27),[5], % 1.86/2.24 intersection(multiply(inverse(negative_part(X10)),X11),multiply(inverse(negative_part(X10)),multiply(X10,X11))) = X11]. % 1.86/2.24 [170=param(62,29),[1,29], % 1.86/2.24 negative_part(multiply(X10,inverse(intersection(X10,X11)))) = identity]. % 1.86/2.24 [178=param(50,31),[2,31], % 1.86/2.24 positive_part(multiply(X10,inverse(union(X10,X11)))) = identity]. % 1.86/2.24 [205=param(89,178),[88], % 1.86/2.24 union(X10,multiply(X10,multiply(X11,inverse(union(X11,X12))))) = X10]. % 1.86/2.24 [220=param(90,170),[88], % 1.86/2.24 intersection(X10,multiply(X10,multiply(X11,inverse(intersection(X11,X12))))) = X10]. % 1.86/2.24 [363=param(76,170),[19,18,3,21,52,44,52], % 1.86/2.24 negative_part(inverse(negative_part(multiply(X10,X11)))) = identity]. % 1.86/2.24 [369=param(363,22),[], % 1.86/2.24 negative_part(inverse(negative_part(X10))) = identity]. % 1.86/2.24 [373=param(63,369),[2], % 1.86/2.24 positive_part(inverse(negative_part(X10))) = inverse(negative_part(X10))]. % 1.86/2.24 [381=param(77,178),[19,18,4,21,66,40,66], % 1.86/2.24 positive_part(inverse(positive_part(multiply(X10,X11)))) = identity]. % 1.86/2.24 [390=param(381,22),[], % 1.86/2.24 positive_part(inverse(positive_part(X10))) = identity]. % 1.86/2.24 [401=param(73,390),[1], % 1.86/2.24 negative_part(inverse(positive_part(X10))) = inverse(positive_part(X10))]. % 1.86/2.24 [951=param(163,28),[80,18,90,88,13], % 1.86/2.24 intersection(inverse(negative_part(X10)),inverse(intersection(X10,multiply(X10,X10)))) = inverse(X10)]. % 1.86/2.24 [1381=param(205,93),[], % 1.86/2.24 union(inverse(X10),inverse(union(X10,X11))) = inverse(X10)]. % 1.86/2.24 [1604=param(1381,2),[], % 1.86/2.24 union(inverse(X10),inverse(positive_part(X10))) = inverse(X10)]. % 1.86/2.24 [1629=param(220,95),[], % 1.86/2.24 intersection(X10,inverse(intersection(inverse(X10),X11))) = X10]. % 1.86/2.24 [1632=param(14,1604),[13], % 1.86/2.24 intersection(inverse(X10),inverse(positive_part(X10))) = inverse(positive_part(X10))]. % 1.86/2.24 [1659=param(1629,1),[], % 1.86/2.24 intersection(X10,inverse(negative_part(inverse(X10)))) = X10]. % 1.86/2.24 [1665=param(1629,13),[], % 1.86/2.24 intersection(X10,inverse(intersection(X11,inverse(X10)))) = X10]. % 1.86/2.24 [1689=param(12,1659),[11], % 1.86/2.24 union(X10,inverse(negative_part(inverse(X10)))) = inverse(negative_part(inverse(X10)))]. % 1.86/2.24 [1723=param(117,1689),[373], % 1.86/2.24 intersection(positive_part(X10),inverse(negative_part(inverse(X10)))) = positive_part(X10)]. % 1.86/2.24 [1745=param(1665,1723),[56,1632,401], % 1.86/2.24 inverse(positive_part(X10)) = negative_part(inverse(X10))]. % 1.86/2.24 [1802=param(18,1745),[], % 1.86/2.24 inverse(negative_part(inverse(X10))) = positive_part(X10)]. % 1.86/2.24 [1831=param(1802,18),[], % 1.86/2.24 inverse(negative_part(X10)) = positive_part(inverse(X10))]. % 1.86/2.24 [1856=demod(951),[1831], % 1.86/2.24 intersection(positive_part(inverse(X10)),inverse(intersection(X10,multiply(X10,X10)))) = inverse(X10)]. % 1.86/2.24 [4065=param(24,75),[1831,1745,90,80,1745,18,90,1856,18,23], % 1.86/2.24 thmtrue = thmfalse]. % 1.86/2.24 % SZS output end CNFRefutation % 1.86/2.24 Space: 9143 KB %------------------------------------------------------------------------------