%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : GRP510-1 : TPTP v8.1.2. Released v2.6.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n016.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 41.62s 41.81s
% Output : Refutation 41.62s
% Verified :
% SZS Type : Refutation
% Derivation depth : 34
% Number of leaves : 7
% Syntax : Number of clauses : 67 ( 47 unt; 0 nHn; 18 RR)
% Number of literals : 89 ( 88 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 : 198 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(prove_these_axioms_2,negated_conjecture,
multiply(multiply(inverse(b2),b2),a2) != a2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_these_axioms_2) ).
cnf(reflexivity,axiom,
X2 = X2,
theory(equality) ).
cnf(c0,axiom,
( X20 != X21
| X18 != X19
| multiply(X20,X18) = multiply(X21,X19) ),
theory(equality) ).
cnf(c10,plain,
( X28 != X29
| multiply(X28,X30) = multiply(X29,X30) ),
inference(resolution,[status(thm)],[c0,reflexivity]) ).
cnf(symmetry,axiom,
( X3 != X4
| X4 = X3 ),
theory(equality) ).
cnf(transitivity,axiom,
( X6 != X8
| X8 != X7
| X6 = X7 ),
theory(equality) ).
cnf(single_axiom,axiom,
multiply(multiply(multiply(X12,X10),X11),inverse(multiply(X12,X11))) = X10,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',single_axiom) ).
cnf(c6,plain,
( X37 != multiply(multiply(multiply(X38,X36),X39),inverse(multiply(X38,X39)))
| X37 = X36 ),
inference(resolution,[status(thm)],[single_axiom,transitivity]) ).
cnf(c5,plain,
X24 = multiply(multiply(multiply(X23,X24),X22),inverse(multiply(X23,X22))),
inference(resolution,[status(thm)],[single_axiom,symmetry]) ).
cnf(c20,plain,
multiply(X71,X70) = multiply(multiply(multiply(multiply(X69,X71),X68),inverse(multiply(X69,X68))),X70),
inference(resolution,[status(thm)],[c10,c5]) ).
cnf(c50,plain,
multiply(X72,inverse(multiply(multiply(X74,X72),inverse(multiply(X74,X73))))) = X73,
inference(resolution,[status(thm)],[c20,c6]) ).
cnf(c58,plain,
( X102 != multiply(X103,inverse(multiply(multiply(X104,X103),inverse(multiply(X104,X101)))))
| X102 = X101 ),
inference(resolution,[status(thm)],[c50,transitivity]) ).
cnf(c21,plain,
multiply(multiply(multiply(multiply(X88,X86),X87),inverse(multiply(X88,X87))),X89) = multiply(X86,X89),
inference(resolution,[status(thm)],[c10,single_axiom]) ).
cnf(c83,plain,
( X235 != multiply(multiply(multiply(multiply(X239,X237),X238),inverse(multiply(X239,X238))),X236)
| X235 = multiply(X237,X236) ),
inference(resolution,[status(thm)],[c21,transitivity]) ).
cnf(c51,plain,
multiply(multiply(X433,X432),X429) = multiply(multiply(multiply(multiply(multiply(X431,X433),X430),inverse(multiply(X431,X430))),X432),X429),
inference(resolution,[status(thm)],[c20,c10]) ).
cnf(c1,axiom,
( X15 != X16
| inverse(X15) = inverse(X16) ),
theory(equality) ).
cnf(c8,plain,
inverse(multiply(multiply(multiply(X46,X44),X45),inverse(multiply(X46,X45)))) = inverse(X44),
inference(resolution,[status(thm)],[c1,single_axiom]) ).
cnf(c30,plain,
( X201 != X198
| multiply(X201,inverse(multiply(multiply(multiply(X200,X199),X202),inverse(multiply(X200,X202))))) = multiply(X198,inverse(X199)) ),
inference(resolution,[status(thm)],[c8,c0]) ).
cnf(c274,plain,
multiply(X355,inverse(multiply(multiply(multiply(X354,X357),X356),inverse(multiply(X354,X356))))) = multiply(X355,inverse(X357)),
inference(resolution,[status(thm)],[c30,reflexivity]) ).
cnf(c577,plain,
multiply(X397,inverse(X399)) = multiply(X397,inverse(multiply(multiply(multiply(X398,X399),X400),inverse(multiply(X398,X400))))),
inference(resolution,[status(thm)],[c274,symmetry]) ).
cnf(c631,plain,
multiply(multiply(multiply(multiply(multiply(X403,X402),X401),X404),inverse(multiply(X403,X401))),inverse(X402)) = X404,
inference(resolution,[status(thm)],[c577,c6]) ).
cnf(c657,plain,
( X733 != multiply(multiply(multiply(multiply(multiply(X737,X736),X734),X735),inverse(multiply(X737,X734))),inverse(X736))
| X733 = X735 ),
inference(resolution,[status(thm)],[c631,transitivity]) ).
cnf(c1774,plain,
multiply(multiply(X746,inverse(multiply(X747,X745))),inverse(X746)) = inverse(multiply(X747,X745)),
inference(resolution,[status(thm)],[c657,c51]) ).
cnf(c1820,plain,
inverse(multiply(X749,X748)) = multiply(multiply(X750,inverse(multiply(X749,X748))),inverse(X750)),
inference(resolution,[status(thm)],[c1774,symmetry]) ).
cnf(c1853,plain,
inverse(multiply(X755,X754)) = multiply(X753,inverse(multiply(multiply(X755,X753),X754))),
inference(resolution,[status(thm)],[c1820,c83]) ).
cnf(c1868,plain,
inverse(multiply(X756,inverse(multiply(X756,X757)))) = X757,
inference(resolution,[status(thm)],[c1853,c58]) ).
cnf(c1897,plain,
( X771 != inverse(multiply(X770,inverse(multiply(X770,X769))))
| X771 = X769 ),
inference(resolution,[status(thm)],[c1868,transitivity]) ).
cnf(c61,plain,
inverse(multiply(X111,inverse(multiply(multiply(X109,X111),inverse(multiply(X109,X110)))))) = inverse(X110),
inference(resolution,[status(thm)],[c50,c1]) ).
cnf(c119,plain,
( X302 != inverse(multiply(X303,inverse(multiply(multiply(X300,X303),inverse(multiply(X300,X301))))))
| X302 = inverse(X301) ),
inference(resolution,[status(thm)],[c61,transitivity]) ).
cnf(c1892,plain,
( X919 != X921
| multiply(X919,inverse(multiply(X920,inverse(multiply(X920,X922))))) = multiply(X921,X922) ),
inference(resolution,[status(thm)],[c1868,c0]) ).
cnf(c2642,plain,
multiply(X924,inverse(multiply(X923,inverse(multiply(X923,X925))))) = multiply(X924,X925),
inference(resolution,[status(thm)],[c1892,reflexivity]) ).
cnf(c2744,plain,
multiply(X934,X933) = multiply(X934,inverse(multiply(X932,inverse(multiply(X932,X933))))),
inference(resolution,[status(thm)],[c2642,symmetry]) ).
cnf(c1863,plain,
multiply(X802,inverse(multiply(multiply(X801,X802),X800))) = inverse(multiply(X801,X800)),
inference(resolution,[status(thm)],[c1853,symmetry]) ).
cnf(c2165,plain,
( X1044 != multiply(X1046,inverse(multiply(multiply(X1043,X1046),X1045)))
| X1044 = inverse(multiply(X1043,X1045)) ),
inference(resolution,[status(thm)],[c1863,transitivity]) ).
cnf(c3619,plain,
multiply(X1059,X1057) = inverse(multiply(X1058,inverse(multiply(multiply(X1058,X1059),X1057)))),
inference(resolution,[status(thm)],[c2165,c2744]) ).
cnf(c3723,plain,
multiply(X1061,inverse(multiply(X1061,X1060))) = inverse(X1060),
inference(resolution,[status(thm)],[c3619,c119]) ).
cnf(c3732,plain,
inverse(X1063) = multiply(X1062,inverse(multiply(X1062,X1063))),
inference(resolution,[status(thm)],[c3723,symmetry]) ).
cnf(c3782,plain,
inverse(inverse(X1103)) = inverse(multiply(X1102,inverse(multiply(X1102,X1103)))),
inference(resolution,[status(thm)],[c3732,c1]) ).
cnf(c4153,plain,
inverse(inverse(X1104)) = X1104,
inference(resolution,[status(thm)],[c3782,c1897]) ).
cnf(c4182,plain,
( X1234 != X1236
| multiply(X1234,inverse(inverse(X1235))) = multiply(X1236,X1235) ),
inference(resolution,[status(thm)],[c4153,c0]) ).
cnf(c5503,plain,
multiply(X1237,inverse(inverse(X1238))) = multiply(X1237,X1238),
inference(resolution,[status(thm)],[c4182,reflexivity]) ).
cnf(c5648,plain,
multiply(X1240,X1239) = multiply(X1240,inverse(inverse(X1239))),
inference(resolution,[status(thm)],[c5503,symmetry]) ).
cnf(c5705,plain,
multiply(multiply(X1981,X1979),X1980) = multiply(multiply(X1981,inverse(inverse(X1979))),X1980),
inference(resolution,[status(thm)],[c5648,c10]) ).
cnf(c4193,plain,
( X1108 != inverse(inverse(X1107))
| X1108 = X1107 ),
inference(resolution,[status(thm)],[c4153,transitivity]) ).
cnf(c4256,plain,
multiply(X1149,inverse(multiply(X1149,inverse(X1148)))) = X1148,
inference(resolution,[status(thm)],[c4193,c3723]) ).
cnf(c4770,plain,
( X1392 != multiply(X1393,inverse(multiply(X1393,inverse(X1391))))
| X1392 = X1391 ),
inference(resolution,[status(thm)],[c4256,transitivity]) ).
cnf(c7550,plain,
multiply(multiply(multiply(X1625,X1624),X1623),inverse(X1624)) = multiply(X1625,X1623),
inference(resolution,[status(thm)],[c4770,c577]) ).
cnf(c9659,plain,
multiply(X1760,X1762) = multiply(multiply(multiply(X1760,X1761),X1762),inverse(X1761)),
inference(resolution,[status(thm)],[c7550,symmetry]) ).
cnf(c10570,plain,
multiply(multiply(X2000,X1998),inverse(multiply(X2000,X1999))) = multiply(X1998,inverse(X1999)),
inference(resolution,[status(thm)],[c9659,c83]) ).
cnf(c12898,plain,
multiply(X2097,inverse(X2096)) = multiply(multiply(X2095,X2097),inverse(multiply(X2095,X2096))),
inference(resolution,[status(thm)],[c10570,symmetry]) ).
cnf(c57,plain,
X81 = multiply(X82,inverse(multiply(multiply(X80,X82),inverse(multiply(X80,X81))))),
inference(resolution,[status(thm)],[c50,symmetry]) ).
cnf(c75,plain,
multiply(X184,X187) = multiply(multiply(X185,inverse(multiply(multiply(X186,X185),inverse(multiply(X186,X184))))),X187),
inference(resolution,[status(thm)],[c57,c10]) ).
cnf(c253,plain,
multiply(X353,inverse(multiply(X350,inverse(multiply(multiply(X352,multiply(X350,X351)),inverse(multiply(X352,X353))))))) = X351,
inference(resolution,[status(thm)],[c75,c6]) ).
cnf(c557,plain,
X396 = multiply(X394,inverse(multiply(X395,inverse(multiply(multiply(X393,multiply(X395,X396)),inverse(multiply(X393,X394))))))),
inference(resolution,[status(thm)],[c253,symmetry]) ).
cnf(c7524,plain,
X1620 = multiply(multiply(X1619,multiply(X1618,X1620)),inverse(multiply(X1619,X1618))),
inference(resolution,[status(thm)],[c4770,c557]) ).
cnf(c9621,plain,
multiply(multiply(X1752,multiply(X1753,X1751)),inverse(multiply(X1752,X1753))) = X1751,
inference(resolution,[status(thm)],[c7524,symmetry]) ).
cnf(c10468,plain,
( X4731 != multiply(multiply(X4732,multiply(X4733,X4730)),inverse(multiply(X4732,X4733)))
| X4731 = X4730 ),
inference(resolution,[status(thm)],[c9621,transitivity]) ).
cnf(c52662,plain,
multiply(multiply(X4735,X4736),inverse(X4735)) = X4736,
inference(resolution,[status(thm)],[c10468,c12898]) ).
cnf(c52813,plain,
( X4763 != multiply(multiply(X4764,X4762),inverse(X4764))
| X4763 = X4762 ),
inference(resolution,[status(thm)],[c52662,transitivity]) ).
cnf(c52911,plain,
X4744 = multiply(multiply(X4743,X4744),inverse(X4743)),
inference(resolution,[status(thm)],[c52662,symmetry]) ).
cnf(c53226,plain,
multiply(X5333,X5335) = multiply(multiply(multiply(X5334,X5333),inverse(X5334)),X5335),
inference(resolution,[status(thm)],[c52911,c10]) ).
cnf(c62384,plain,
multiply(X5339,inverse(multiply(X5338,inverse(X5338)))) = X5339,
inference(resolution,[status(thm)],[c53226,c6]) ).
cnf(c62599,plain,
X5351 = multiply(X5351,inverse(multiply(X5350,inverse(X5350)))),
inference(resolution,[status(thm)],[c62384,symmetry]) ).
cnf(c63531,plain,
multiply(multiply(X5376,inverse(X5376)),X5375) = X5375,
inference(resolution,[status(thm)],[c62599,c52813]) ).
cnf(c63912,plain,
( X5562 != multiply(multiply(X5563,inverse(X5563)),X5561)
| X5562 = X5561 ),
inference(resolution,[status(thm)],[c63531,transitivity]) ).
cnf(c67590,plain,
multiply(multiply(inverse(X5602),X5602),X5603) = X5603,
inference(resolution,[status(thm)],[c63912,c5705]) ).
cnf(c68100,plain,
$false,
inference(resolution,[status(thm)],[c67590,prove_these_axioms_2]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.13 % Problem : GRP510-1 : TPTP v8.1.2. Released v2.6.0.
% 0.07/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.35 % Computer : n016.cluster.edu
% 0.13/0.35 % Model : x86_64 x86_64
% 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.35 % Memory : 8042.1875MB
% 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.35 % CPULimit : 300
% 0.13/0.35 % WCLimit : 300
% 0.13/0.35 % DateTime : Thu May 9 03:43:53 EDT 2024
% 0.13/0.35 % CPUTime :
% 41.62/41.81 % Version: 1.5
% 41.62/41.81 % SZS status Unsatisfiable
% 41.62/41.81 % SZS output start CNFRefutation
% See solution above
% 41.62/41.81
% 41.62/41.81 % Initial clauses : 7
% 41.62/41.81 % Processed clauses : 851
% 41.62/41.81 % Factors computed : 2
% 41.62/41.81 % Resolvents computed: 68163
% 41.62/41.81 % Tautologies deleted: 2
% 41.62/41.81 % Forward subsumed : 1171
% 41.62/41.81 % Backward subsumed : 20
% 41.62/41.81 % -------- CPU Time ---------
% 41.62/41.81 % User time : 41.263 s
% 41.62/41.81 % System time : 0.186 s
% 41.62/41.81 % Total time : 41.449 s
%------------------------------------------------------------------------------