%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : GRP509-1 : TPTP v8.1.2. Released v2.6.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n015.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 : 300s
% DateTime : Thu May 9 17:23:56 EDT 2024
% Result : Unsatisfiable 39.06s 39.25s
% Output : Refutation 39.06s
% Verified :
% SZS Type : Refutation
% Derivation depth : 33
% Number of leaves : 7
% Syntax : Number of clauses : 65 ( 45 unt; 0 nHn; 18 RR)
% Number of literals : 87 ( 86 equ; 23 neg)
% Maximal clause size : 3 ( 1 avg)
% Maximal term depth : 8 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 4 ( 4 usr; 2 con; 0-2 aty)
% Number of variables : 194 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(prove_these_axioms_1,negated_conjecture,
multiply(inverse(a1),a1) != multiply(inverse(b1),b1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_these_axioms_1) ).
cnf(transitivity,axiom,
( X7 != X8
| X8 != X6
| X7 = X6 ),
theory(equality) ).
cnf(reflexivity,axiom,
X2 = X2,
theory(equality) ).
cnf(c0,axiom,
( X21 != X19
| X18 != X20
| multiply(X21,X18) = multiply(X19,X20) ),
theory(equality) ).
cnf(single_axiom,axiom,
multiply(multiply(multiply(X11,X10),X12),inverse(multiply(X11,X12))) = X10,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',single_axiom) ).
cnf(c5,plain,
( X23 != multiply(multiply(multiply(X25,X24),X22),inverse(multiply(X25,X22)))
| X23 = X24 ),
inference(resolution,[status(thm)],[single_axiom,transitivity]) ).
cnf(c10,plain,
( X29 != X30
| multiply(X29,X31) = multiply(X30,X31) ),
inference(resolution,[status(thm)],[c0,reflexivity]) ).
cnf(symmetry,axiom,
( X3 != X4
| X4 = X3 ),
theory(equality) ).
cnf(c6,plain,
X34 = multiply(multiply(multiply(X35,X34),X36),inverse(multiply(X35,X36))),
inference(resolution,[status(thm)],[single_axiom,symmetry]) ).
cnf(c18,plain,
multiply(X74,X75) = multiply(multiply(multiply(multiply(X73,X74),X72),inverse(multiply(X73,X72))),X75),
inference(resolution,[status(thm)],[c6,c10]) ).
cnf(c60,plain,
multiply(X82,inverse(multiply(multiply(X81,X82),inverse(multiply(X81,X83))))) = X83,
inference(resolution,[status(thm)],[c18,c5]) ).
cnf(c76,plain,
( X106 != multiply(X108,inverse(multiply(multiply(X105,X108),inverse(multiply(X105,X107)))))
| X106 = X107 ),
inference(resolution,[status(thm)],[c60,transitivity]) ).
cnf(c17,plain,
multiply(multiply(multiply(multiply(X69,X68),X70),inverse(multiply(X69,X70))),X71) = multiply(X68,X71),
inference(resolution,[status(thm)],[c10,single_axiom]) ).
cnf(c49,plain,
( X212 != multiply(multiply(multiply(multiply(X211,X215),X213),inverse(multiply(X211,X213))),X214)
| X212 = multiply(X215,X214) ),
inference(resolution,[status(thm)],[c17,transitivity]) ).
cnf(c57,plain,
multiply(multiply(X445,X446),X447) = multiply(multiply(multiply(multiply(multiply(X444,X445),X443),inverse(multiply(X444,X443))),X446),X447),
inference(resolution,[status(thm)],[c18,c10]) ).
cnf(c1,axiom,
( X16 != X15
| inverse(X16) = inverse(X15) ),
theory(equality) ).
cnf(c8,plain,
inverse(multiply(multiply(multiply(X38,X37),X39),inverse(multiply(X38,X39)))) = inverse(X37),
inference(resolution,[status(thm)],[c1,single_axiom]) ).
cnf(c27,plain,
( X178 != X181
| multiply(X178,inverse(multiply(multiply(multiply(X177,X179),X180),inverse(multiply(X177,X180))))) = multiply(X181,inverse(X179)) ),
inference(resolution,[status(thm)],[c8,c0]) ).
cnf(c244,plain,
multiply(X351,inverse(multiply(multiply(multiply(X350,X353),X352),inverse(multiply(X350,X352))))) = multiply(X351,inverse(X353)),
inference(resolution,[status(thm)],[c27,reflexivity]) ).
cnf(c567,plain,
multiply(X399,inverse(X400)) = multiply(X399,inverse(multiply(multiply(multiply(X398,X400),X397),inverse(multiply(X398,X397))))),
inference(resolution,[status(thm)],[c244,symmetry]) ).
cnf(c651,plain,
multiply(multiply(multiply(multiply(multiply(X402,X403),X401),X404),inverse(multiply(X402,X401))),inverse(X403)) = X404,
inference(resolution,[status(thm)],[c567,c5]) ).
cnf(c665,plain,
( X716 != multiply(multiply(multiply(multiply(multiply(X714,X712),X715),X713),inverse(multiply(X714,X715))),inverse(X712))
| X716 = X713 ),
inference(resolution,[status(thm)],[c651,transitivity]) ).
cnf(c1829,plain,
multiply(multiply(X733,inverse(multiply(X731,X732))),inverse(X733)) = inverse(multiply(X731,X732)),
inference(resolution,[status(thm)],[c665,c57]) ).
cnf(c1883,plain,
inverse(multiply(X734,X735)) = multiply(multiply(X736,inverse(multiply(X734,X735))),inverse(X736)),
inference(resolution,[status(thm)],[c1829,symmetry]) ).
cnf(c1892,plain,
inverse(multiply(X746,X747)) = multiply(X748,inverse(multiply(multiply(X746,X748),X747))),
inference(resolution,[status(thm)],[c1883,c49]) ).
cnf(c1988,plain,
inverse(multiply(X750,inverse(multiply(X750,X749)))) = X749,
inference(resolution,[status(thm)],[c1892,c76]) ).
cnf(c2022,plain,
( X763 != inverse(multiply(X762,inverse(multiply(X762,X764))))
| X763 = X764 ),
inference(resolution,[status(thm)],[c1988,transitivity]) ).
cnf(c80,plain,
inverse(multiply(X115,inverse(multiply(multiply(X113,X115),inverse(multiply(X113,X114)))))) = inverse(X114),
inference(resolution,[status(thm)],[c60,c1]) ).
cnf(c118,plain,
( X297 != inverse(multiply(X296,inverse(multiply(multiply(X299,X296),inverse(multiply(X299,X298))))))
| X297 = inverse(X298) ),
inference(resolution,[status(thm)],[c80,transitivity]) ).
cnf(c2010,plain,
( X907 != X908
| multiply(X907,inverse(multiply(X910,inverse(multiply(X910,X909))))) = multiply(X908,X909) ),
inference(resolution,[status(thm)],[c1988,c0]) ).
cnf(c2893,plain,
multiply(X911,inverse(multiply(X913,inverse(multiply(X913,X912))))) = multiply(X911,X912),
inference(resolution,[status(thm)],[c2010,reflexivity]) ).
cnf(c2946,plain,
multiply(X915,X914) = multiply(X915,inverse(multiply(X916,inverse(multiply(X916,X914))))),
inference(resolution,[status(thm)],[c2893,symmetry]) ).
cnf(c2006,plain,
multiply(X791,inverse(multiply(multiply(X790,X791),X789))) = inverse(multiply(X790,X789)),
inference(resolution,[status(thm)],[c1892,symmetry]) ).
cnf(c2292,plain,
( X1017 != multiply(X1018,inverse(multiply(multiply(X1020,X1018),X1019)))
| X1017 = inverse(multiply(X1020,X1019)) ),
inference(resolution,[status(thm)],[c2006,transitivity]) ).
cnf(c3830,plain,
multiply(X1037,X1036) = inverse(multiply(X1038,inverse(multiply(multiply(X1038,X1037),X1036)))),
inference(resolution,[status(thm)],[c2292,c2946]) ).
cnf(c3930,plain,
multiply(X1046,inverse(multiply(X1046,X1047))) = inverse(X1047),
inference(resolution,[status(thm)],[c3830,c118]) ).
cnf(c4011,plain,
inverse(X1049) = multiply(X1048,inverse(multiply(X1048,X1049))),
inference(resolution,[status(thm)],[c3930,symmetry]) ).
cnf(c4032,plain,
inverse(inverse(X1082)) = inverse(multiply(X1083,inverse(multiply(X1083,X1082)))),
inference(resolution,[status(thm)],[c4011,c1]) ).
cnf(c4326,plain,
inverse(inverse(X1084)) = X1084,
inference(resolution,[status(thm)],[c4032,c2022]) ).
cnf(c4343,plain,
( X1212 != X1213
| multiply(X1212,inverse(inverse(X1214))) = multiply(X1213,X1214) ),
inference(resolution,[status(thm)],[c4326,c0]) ).
cnf(c5722,plain,
multiply(X1215,inverse(inverse(X1216))) = multiply(X1215,X1216),
inference(resolution,[status(thm)],[c4343,reflexivity]) ).
cnf(c5767,plain,
( X1427 != multiply(X1429,inverse(inverse(X1428)))
| X1427 = multiply(X1429,X1428) ),
inference(resolution,[status(thm)],[c5722,transitivity]) ).
cnf(c4355,plain,
( X1091 != inverse(inverse(X1092))
| X1091 = X1092 ),
inference(resolution,[status(thm)],[c4326,transitivity]) ).
cnf(c4463,plain,
multiply(X1136,inverse(multiply(X1136,inverse(X1137)))) = X1137,
inference(resolution,[status(thm)],[c4355,c3930]) ).
cnf(c5062,plain,
( X1378 != multiply(X1380,inverse(multiply(X1380,inverse(X1379))))
| X1378 = X1379 ),
inference(resolution,[status(thm)],[c4463,transitivity]) ).
cnf(c7669,plain,
multiply(multiply(multiply(X1614,X1615),X1613),inverse(X1615)) = multiply(X1614,X1613),
inference(resolution,[status(thm)],[c5062,c567]) ).
cnf(c9480,plain,
( X4112 != multiply(multiply(multiply(X4114,X4113),X4115),inverse(X4113))
| X4112 = multiply(X4114,X4115) ),
inference(resolution,[status(thm)],[c7669,transitivity]) ).
cnf(c9508,plain,
multiply(X1753,X1754) = multiply(multiply(multiply(X1753,X1752),X1754),inverse(X1752)),
inference(resolution,[status(thm)],[c7669,symmetry]) ).
cnf(c10556,plain,
multiply(multiply(X1983,X1985),inverse(multiply(X1983,X1984))) = multiply(X1985,inverse(X1984)),
inference(resolution,[status(thm)],[c9508,c49]) ).
cnf(c13027,plain,
multiply(X2087,inverse(X2085)) = multiply(multiply(X2086,X2087),inverse(multiply(X2086,X2085))),
inference(resolution,[status(thm)],[c10556,symmetry]) ).
cnf(c82,plain,
X84 = multiply(X86,inverse(multiply(multiply(X85,X86),inverse(multiply(X85,X84))))),
inference(resolution,[status(thm)],[c60,symmetry]) ).
cnf(c84,plain,
multiply(X188,X189) = multiply(multiply(X186,inverse(multiply(multiply(X187,X186),inverse(multiply(X187,X188))))),X189),
inference(resolution,[status(thm)],[c82,c10]) ).
cnf(c266,plain,
multiply(X354,inverse(multiply(X355,inverse(multiply(multiply(X357,multiply(X355,X356)),inverse(multiply(X357,X354))))))) = X356,
inference(resolution,[status(thm)],[c84,c5]) ).
cnf(c588,plain,
X419 = multiply(X421,inverse(multiply(X422,inverse(multiply(multiply(X420,multiply(X422,X419)),inverse(multiply(X420,X421))))))),
inference(resolution,[status(thm)],[c266,symmetry]) ).
cnf(c7695,plain,
X1627 = multiply(multiply(X1626,multiply(X1625,X1627)),inverse(multiply(X1626,X1625))),
inference(resolution,[status(thm)],[c5062,c588]) ).
cnf(c9649,plain,
multiply(multiply(X1767,multiply(X1768,X1766)),inverse(multiply(X1767,X1768))) = X1766,
inference(resolution,[status(thm)],[c7695,symmetry]) ).
cnf(c10649,plain,
( X4743 != multiply(multiply(X4744,multiply(X4745,X4746)),inverse(multiply(X4744,X4745)))
| X4743 = X4746 ),
inference(resolution,[status(thm)],[c9649,transitivity]) ).
cnf(c53803,plain,
multiply(multiply(X4755,X4756),inverse(X4755)) = X4756,
inference(resolution,[status(thm)],[c10649,c13027]) ).
cnf(c54069,plain,
X4759 = multiply(multiply(X4760,X4759),inverse(X4760)),
inference(resolution,[status(thm)],[c53803,symmetry]) ).
cnf(c54296,plain,
multiply(X5341,X5342) = multiply(multiply(multiply(X5340,X5341),inverse(X5340)),X5342),
inference(resolution,[status(thm)],[c54069,c10]) ).
cnf(c63751,plain,
multiply(X5349,inverse(X5349)) = multiply(X5350,inverse(X5350)),
inference(resolution,[status(thm)],[c54296,c9480]) ).
cnf(c64106,plain,
multiply(X5444,inverse(X5444)) = multiply(inverse(X5443),X5443),
inference(resolution,[status(thm)],[c63751,c5767]) ).
cnf(c65616,plain,
multiply(inverse(X5510),X5510) = multiply(X5509,inverse(X5509)),
inference(resolution,[status(thm)],[c64106,symmetry]) ).
cnf(c66745,plain,
multiply(inverse(X5525),X5525) = multiply(inverse(X5526),X5526),
inference(resolution,[status(thm)],[c65616,c5767]) ).
cnf(c66920,plain,
$false,
inference(resolution,[status(thm)],[c66745,prove_these_axioms_1]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.13 % Problem : GRP509-1 : TPTP v8.1.2. Released v2.6.0.
% 0.04/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.35 % Computer : n015.cluster.edu
% 0.14/0.35 % Model : x86_64 x86_64
% 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.35 % Memory : 8042.1875MB
% 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.35 % CPULimit : 300
% 0.14/0.35 % WCLimit : 300
% 0.14/0.35 % DateTime : Thu May 9 04:45:52 EDT 2024
% 0.14/0.35 % CPUTime :
% 39.06/39.25 % Version: 1.5
% 39.06/39.25 % SZS status Unsatisfiable
% 39.06/39.25 % SZS output start CNFRefutation
% See solution above
% 39.06/39.25
% 39.06/39.25 % Initial clauses : 7
% 39.06/39.25 % Processed clauses : 843
% 39.06/39.25 % Factors computed : 2
% 39.06/39.25 % Resolvents computed: 66947
% 39.06/39.25 % Tautologies deleted: 2
% 39.06/39.25 % Forward subsumed : 1149
% 39.06/39.25 % Backward subsumed : 19
% 39.06/39.25 % -------- CPU Time ---------
% 39.06/39.25 % User time : 38.690 s
% 39.06/39.25 % System time : 0.196 s
% 39.06/39.25 % Total time : 38.886 s
%------------------------------------------------------------------------------