%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : GRP594-1 : TPTP v8.1.2. Released v2.6.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n021.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:24:05 EDT 2024
% Result : Unsatisfiable 225.99s 226.26s
% Output : Refutation 225.99s
% Verified :
% SZS Type : Refutation
% Derivation depth : 50
% Number of leaves : 9
% Syntax : Number of clauses : 96 ( 69 unt; 0 nHn; 23 RR)
% Number of literals : 126 ( 125 equ; 31 neg)
% Maximal clause size : 3 ( 1 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 5 ( 5 usr; 2 con; 0-2 aty)
% Number of variables : 315 ( 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(transitivity,axiom,
( X10 != X9
| X9 != X8
| X10 = X8 ),
theory(equality) ).
cnf(reflexivity,axiom,
X2 = X2,
theory(equality) ).
cnf(c2,axiom,
( X49 != X48
| X47 != X50
| multiply(X49,X47) = multiply(X48,X50) ),
theory(equality) ).
cnf(single_axiom,axiom,
inverse(double_divide(double_divide(X11,X12),inverse(double_divide(X11,inverse(double_divide(X13,X12)))))) = X13,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',single_axiom) ).
cnf(c9,plain,
( X77 != inverse(double_divide(double_divide(X78,X79),inverse(double_divide(X78,inverse(double_divide(X76,X79))))))
| X77 = X76 ),
inference(resolution,[status(thm)],[single_axiom,transitivity]) ).
cnf(multiply,axiom,
multiply(X6,X7) = inverse(double_divide(X7,X6)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',multiply) ).
cnf(c6,plain,
( X24 != multiply(X26,X25)
| X24 = inverse(double_divide(X25,X26)) ),
inference(resolution,[status(thm)],[transitivity,multiply]) ).
cnf(c49,plain,
( X55 != X56
| multiply(X55,X54) = multiply(X56,X54) ),
inference(resolution,[status(thm)],[c2,reflexivity]) ).
cnf(c57,plain,
multiply(multiply(X86,X85),X84) = multiply(inverse(double_divide(X85,X86)),X84),
inference(resolution,[status(thm)],[c49,multiply]) ).
cnf(c106,plain,
multiply(multiply(X154,X155),X153) = inverse(double_divide(X153,inverse(double_divide(X155,X154)))),
inference(resolution,[status(thm)],[c57,c6]) ).
cnf(c251,plain,
multiply(multiply(inverse(double_divide(X156,X157)),X158),double_divide(X158,X157)) = X156,
inference(resolution,[status(thm)],[c106,c9]) ).
cnf(c266,plain,
( X432 != multiply(multiply(inverse(double_divide(X431,X434)),X433),double_divide(X433,X434))
| X432 = X431 ),
inference(resolution,[status(thm)],[c251,transitivity]) ).
cnf(c99,plain,
multiply(multiply(multiply(X639,X640),X637),X638) = multiply(multiply(inverse(double_divide(X640,X639)),X637),X638),
inference(resolution,[status(thm)],[c57,c49]) ).
cnf(c1924,plain,
multiply(multiply(multiply(X643,X642),X641),double_divide(X641,X643)) = X642,
inference(resolution,[status(thm)],[c99,c266]) ).
cnf(c1950,plain,
( X3683 != X3687
| multiply(X3683,multiply(multiply(multiply(X3686,X3684),X3685),double_divide(X3685,X3686))) = multiply(X3687,X3684) ),
inference(resolution,[status(thm)],[c1924,c2]) ).
cnf(c28790,plain,
multiply(X3688,multiply(multiply(multiply(X3691,X3690),X3689),double_divide(X3689,X3691))) = multiply(X3688,X3690),
inference(resolution,[status(thm)],[c1950,reflexivity]) ).
cnf(c29025,plain,
( X6159 != multiply(X6161,multiply(multiply(multiply(X6160,X6158),X6157),double_divide(X6157,X6160)))
| X6159 = multiply(X6161,X6158) ),
inference(resolution,[status(thm)],[c28790,transitivity]) ).
cnf(symmetry,axiom,
( X4 != X3
| X3 = X4 ),
theory(equality) ).
cnf(c256,plain,
inverse(double_divide(X195,inverse(double_divide(X194,X193)))) = multiply(multiply(X193,X194),X195),
inference(resolution,[status(thm)],[c106,symmetry]) ).
cnf(c352,plain,
( X1290 != inverse(double_divide(X1289,inverse(double_divide(X1292,X1291))))
| X1290 = multiply(multiply(X1291,X1292),X1289) ),
inference(resolution,[status(thm)],[c256,transitivity]) ).
cnf(c1934,plain,
( X681 != multiply(multiply(multiply(X683,X680),X682),double_divide(X682,X683))
| X681 = X680 ),
inference(resolution,[status(thm)],[c1924,transitivity]) ).
cnf(c4,plain,
inverse(double_divide(X20,X21)) = multiply(X21,X20),
inference(resolution,[status(thm)],[multiply,symmetry]) ).
cnf(c15,plain,
( X59 != inverse(double_divide(X60,X61))
| X59 = multiply(X61,X60) ),
inference(resolution,[status(thm)],[c4,transitivity]) ).
cnf(c0,axiom,
( X18 != X17
| inverse(X18) = inverse(X17) ),
theory(equality) ).
cnf(c1955,plain,
X645 = multiply(multiply(multiply(X646,X645),X644),double_divide(X644,X646)),
inference(resolution,[status(thm)],[c1924,symmetry]) ).
cnf(c1970,plain,
multiply(X755,X756) = multiply(multiply(multiply(multiply(X754,X755),X757),double_divide(X757,X754)),X756),
inference(resolution,[status(thm)],[c1955,c49]) ).
cnf(c2692,plain,
multiply(X759,double_divide(double_divide(X758,X760),multiply(X760,X759))) = X758,
inference(resolution,[status(thm)],[c1970,c1934]) ).
cnf(c2736,plain,
X763 = multiply(X761,double_divide(double_divide(X763,X762),multiply(X762,X761))),
inference(resolution,[status(thm)],[c2692,symmetry]) ).
cnf(c2753,plain,
multiply(X936,X937) = multiply(multiply(X935,double_divide(double_divide(X936,X938),multiply(X938,X935))),X937),
inference(resolution,[status(thm)],[c2736,c49]) ).
cnf(c4083,plain,
multiply(multiply(X12187,X12185),X12186) = multiply(multiply(multiply(X12189,double_divide(double_divide(X12187,X12188),multiply(X12188,X12189))),X12185),X12186),
inference(resolution,[status(thm)],[c2753,c49]) ).
cnf(c194734,plain,
multiply(multiply(X12193,X12192),double_divide(X12192,X12190)) = double_divide(double_divide(X12193,X12191),multiply(X12191,X12190)),
inference(resolution,[status(thm)],[c4083,c1934]) ).
cnf(c194935,plain,
double_divide(double_divide(X12196,X12195),multiply(X12195,X12197)) = multiply(multiply(X12196,X12194),double_divide(X12194,X12197)),
inference(resolution,[status(thm)],[c194734,symmetry]) ).
cnf(c195042,plain,
double_divide(double_divide(multiply(X12198,X12200),X12199),multiply(X12199,X12198)) = X12200,
inference(resolution,[status(thm)],[c194935,c1934]) ).
cnf(c195308,plain,
X12208 = double_divide(double_divide(multiply(X12207,X12208),X12206),multiply(X12206,X12207)),
inference(resolution,[status(thm)],[c195042,symmetry]) ).
cnf(c195566,plain,
inverse(X12298) = inverse(double_divide(double_divide(multiply(X12297,X12298),X12296),multiply(X12296,X12297))),
inference(resolution,[status(thm)],[c195308,c0]) ).
cnf(c198700,plain,
inverse(X12299) = multiply(multiply(X12301,X12300),double_divide(multiply(X12300,X12299),X12301)),
inference(resolution,[status(thm)],[c195566,c15]) ).
cnf(c198837,plain,
multiply(inverse(X13053),X13051) = multiply(multiply(multiply(X13050,X13052),double_divide(multiply(X13052,X13053),X13050)),X13051),
inference(resolution,[status(thm)],[c198700,c49]) ).
cnf(c221055,plain,
multiply(inverse(X13056),double_divide(double_divide(multiply(X13055,X13056),X13054),X13054)) = X13055,
inference(resolution,[status(thm)],[c198837,c1934]) ).
cnf(c221170,plain,
( X13087 != multiply(inverse(X13089),double_divide(double_divide(multiply(X13086,X13089),X13088),X13088))
| X13087 = X13086 ),
inference(resolution,[status(thm)],[c221055,transitivity]) ).
cnf(c2729,plain,
( X4035 != X4038
| multiply(X4035,multiply(X4034,double_divide(double_divide(X4037,X4036),multiply(X4036,X4034)))) = multiply(X4038,X4037) ),
inference(resolution,[status(thm)],[c2692,c2]) ).
cnf(c34122,plain,
multiply(X4039,multiply(X4040,double_divide(double_divide(X4042,X4041),multiply(X4041,X4040)))) = multiply(X4039,X4042),
inference(resolution,[status(thm)],[c2729,reflexivity]) ).
cnf(c34383,plain,
( X6412 != multiply(X6410,multiply(X6411,double_divide(double_divide(X6414,X6413),multiply(X6413,X6411))))
| X6412 = multiply(X6410,X6414) ),
inference(resolution,[status(thm)],[c34122,transitivity]) ).
cnf(c1987,plain,
X660 = inverse(double_divide(double_divide(X659,X661),multiply(multiply(X661,X660),X659))),
inference(resolution,[status(thm)],[c1955,c6]) ).
cnf(c2059,plain,
inverse(double_divide(double_divide(X668,X669),multiply(multiply(X669,X670),X668))) = X670,
inference(resolution,[status(thm)],[c1987,symmetry]) ).
cnf(c2108,plain,
( X881 != inverse(double_divide(double_divide(X880,X882),multiply(multiply(X882,X879),X880)))
| X881 = X879 ),
inference(resolution,[status(thm)],[c2059,transitivity]) ).
cnf(c2712,plain,
( X784 != multiply(X783,double_divide(double_divide(X782,X785),multiply(X785,X783)))
| X784 = X782 ),
inference(resolution,[status(thm)],[c2692,transitivity]) ).
cnf(c2681,plain,
multiply(multiply(X8803,X8800),X8801) = multiply(multiply(multiply(multiply(multiply(X8804,X8803),X8802),double_divide(X8802,X8804)),X8800),X8801),
inference(resolution,[status(thm)],[c1970,c49]) ).
cnf(c111229,plain,
multiply(multiply(X8811,X8812),double_divide(X8812,multiply(multiply(X8810,X8811),X8809))) = double_divide(X8809,X8810),
inference(resolution,[status(thm)],[c2681,c1934]) ).
cnf(c111395,plain,
double_divide(X8814,X8815) = multiply(multiply(X8813,X8816),double_divide(X8816,multiply(multiply(X8815,X8813),X8814))),
inference(resolution,[status(thm)],[c111229,symmetry]) ).
cnf(c111494,plain,
double_divide(multiply(X8817,double_divide(X8819,multiply(X8818,X8817))),X8818) = X8819,
inference(resolution,[status(thm)],[c111395,c2712]) ).
cnf(c111576,plain,
( X8847 != double_divide(multiply(X8846,double_divide(X8848,multiply(X8849,X8846))),X8849)
| X8847 = X8848 ),
inference(resolution,[status(thm)],[c111494,transitivity]) ).
cnf(c1,axiom,
( X35 != X34
| X33 != X36
| double_divide(X35,X33) = double_divide(X34,X36) ),
theory(equality) ).
cnf(c26,plain,
( X41 != X42
| double_divide(X41,X40) = double_divide(X42,X40) ),
inference(resolution,[status(thm)],[c1,reflexivity]) ).
cnf(c221338,plain,
X13059 = multiply(inverse(X13057),double_divide(double_divide(multiply(X13059,X13057),X13058),X13058)),
inference(resolution,[status(thm)],[c221055,symmetry]) ).
cnf(c221452,plain,
double_divide(X13740,X13741) = double_divide(multiply(inverse(X13742),double_divide(double_divide(multiply(X13740,X13742),X13739),X13739)),X13741),
inference(resolution,[status(thm)],[c221338,c26]) ).
cnf(c238004,plain,
double_divide(X13743,X13745) = double_divide(multiply(X13743,X13744),multiply(X13745,inverse(X13744))),
inference(resolution,[status(thm)],[c221452,c111576]) ).
cnf(c238170,plain,
inverse(double_divide(X13799,X13798)) = inverse(double_divide(multiply(X13799,X13797),multiply(X13798,inverse(X13797)))),
inference(resolution,[status(thm)],[c238004,c0]) ).
cnf(c240238,plain,
inverse(double_divide(X13801,X13802)) = multiply(multiply(X13802,inverse(X13800)),multiply(X13801,X13800)),
inference(resolution,[status(thm)],[c238170,c15]) ).
cnf(c240442,plain,
multiply(multiply(X13803,inverse(X13804)),multiply(X13805,X13804)) = inverse(double_divide(X13805,X13803)),
inference(resolution,[status(thm)],[c240238,symmetry]) ).
cnf(c240563,plain,
multiply(multiply(X13807,inverse(X13806)),multiply(X13808,X13806)) = multiply(X13807,X13808),
inference(resolution,[status(thm)],[c240442,c15]) ).
cnf(c240680,plain,
( X13963 != multiply(multiply(X13962,inverse(X13965)),multiply(X13964,X13965))
| X13963 = multiply(X13962,X13964) ),
inference(resolution,[status(thm)],[c240563,transitivity]) ).
cnf(c111743,plain,
( X9867 != X9869
| multiply(X9867,double_divide(multiply(X9865,double_divide(X9868,multiply(X9866,X9865))),X9866)) = multiply(X9869,X9868) ),
inference(resolution,[status(thm)],[c111494,c2]) ).
cnf(c137121,plain,
multiply(X9870,double_divide(multiply(X9873,double_divide(X9871,multiply(X9872,X9873))),X9872)) = multiply(X9870,X9871),
inference(resolution,[status(thm)],[c111743,reflexivity]) ).
cnf(c137814,plain,
multiply(X9875,X9876) = multiply(X9875,double_divide(multiply(X9877,double_divide(X9876,multiply(X9874,X9877))),X9874)),
inference(resolution,[status(thm)],[c137121,symmetry]) ).
cnf(c137928,plain,
multiply(multiply(multiply(X9878,X9880),multiply(X9879,double_divide(X9881,multiply(X9878,X9879)))),X9881) = X9880,
inference(resolution,[status(thm)],[c137814,c1934]) ).
cnf(c138024,plain,
( X11060 != multiply(multiply(multiply(X11061,X11059),multiply(X11062,double_divide(X11063,multiply(X11061,X11062)))),X11063)
| X11060 = X11059 ),
inference(resolution,[status(thm)],[c137928,transitivity]) ).
cnf(c45,plain,
( X229 != X230
| multiply(X229,multiply(X227,X228)) = multiply(X230,inverse(double_divide(X228,X227))) ),
inference(resolution,[status(thm)],[c2,multiply]) ).
cnf(c487,plain,
multiply(X231,multiply(X233,X232)) = multiply(X231,inverse(double_divide(X232,X233))),
inference(resolution,[status(thm)],[c45,reflexivity]) ).
cnf(c490,plain,
multiply(multiply(X1385,multiply(X1386,X1388)),X1387) = multiply(multiply(X1385,inverse(double_divide(X1388,X1386))),X1387),
inference(resolution,[status(thm)],[c487,c49]) ).
cnf(c244154,plain,
multiply(multiply(X14132,multiply(X14130,X14131)),multiply(X14133,double_divide(X14131,X14130))) = multiply(X14132,X14133),
inference(resolution,[status(thm)],[c240680,c490]) ).
cnf(c250576,plain,
multiply(X14198,X14201) = multiply(multiply(X14198,multiply(X14200,X14199)),multiply(X14201,double_divide(X14199,X14200))),
inference(resolution,[status(thm)],[c244154,symmetry]) ).
cnf(c252010,plain,
multiply(X14242,multiply(multiply(X14243,X14244),X14241)) = multiply(multiply(X14242,multiply(X14243,X14241)),X14244),
inference(resolution,[status(thm)],[c250576,c29025]) ).
cnf(c252945,plain,
multiply(multiply(X14272,X14271),multiply(multiply(X14273,X14270),double_divide(X14270,multiply(X14272,X14273)))) = X14271,
inference(resolution,[status(thm)],[c252010,c138024]) ).
cnf(c254505,plain,
X14367 = multiply(multiply(X14366,X14367),multiply(multiply(X14368,X14365),double_divide(X14365,multiply(X14366,X14368)))),
inference(resolution,[status(thm)],[c252945,symmetry]) ).
cnf(c257130,plain,
inverse(double_divide(X14375,multiply(X14376,X14374))) = multiply(X14376,multiply(X14374,X14375)),
inference(resolution,[status(thm)],[c254505,c240680]) ).
cnf(c257522,plain,
multiply(X14377,multiply(X14379,X14378)) = inverse(double_divide(X14378,multiply(X14377,X14379))),
inference(resolution,[status(thm)],[c257130,symmetry]) ).
cnf(c257657,plain,
multiply(multiply(X14385,X14384),multiply(X14383,double_divide(X14383,X14385))) = X14384,
inference(resolution,[status(thm)],[c257522,c2108]) ).
cnf(c258121,plain,
X14400 = multiply(multiply(X14398,X14400),multiply(X14399,double_divide(X14399,X14398))),
inference(resolution,[status(thm)],[c257657,symmetry]) ).
cnf(c258596,plain,
X14408 = multiply(multiply(multiply(X14407,double_divide(X14406,X14407)),X14408),X14406),
inference(resolution,[status(thm)],[c258121,c34383]) ).
cnf(c258773,plain,
X14415 = double_divide(double_divide(X14415,X14414),X14414),
inference(resolution,[status(thm)],[c258596,c1934]) ).
cnf(c259062,plain,
inverse(X14431) = inverse(double_divide(double_divide(X14431,X14430),X14430)),
inference(resolution,[status(thm)],[c258773,c0]) ).
cnf(c261171,plain,
inverse(X14432) = multiply(X14433,double_divide(X14432,X14433)),
inference(resolution,[status(thm)],[c259062,c15]) ).
cnf(c261430,plain,
inverse(double_divide(multiply(X14460,X14461),inverse(X14461))) = X14460,
inference(resolution,[status(thm)],[c261171,c221170]) ).
cnf(c262620,plain,
X14465 = inverse(double_divide(multiply(X14465,X14464),inverse(X14464))),
inference(resolution,[status(thm)],[c261430,symmetry]) ).
cnf(c262866,plain,
X14617 = multiply(multiply(X14616,X14615),multiply(X14617,double_divide(X14615,X14616))),
inference(resolution,[status(thm)],[c262620,c352]) ).
cnf(c269302,plain,
multiply(multiply(X14819,X14820),X14818) = multiply(multiply(X14819,X14818),X14820),
inference(resolution,[status(thm)],[c262866,c29025]) ).
cnf(c257646,plain,
multiply(X14380,multiply(X14382,X14381)) = multiply(multiply(X14380,X14382),X14381),
inference(resolution,[status(thm)],[c257522,c15]) ).
cnf(c257871,plain,
multiply(multiply(X14396,X14397),X14395) = multiply(X14396,multiply(X14397,X14395)),
inference(resolution,[status(thm)],[c257646,symmetry]) ).
cnf(c262774,plain,
X14467 = multiply(inverse(X14466),multiply(X14467,X14466)),
inference(resolution,[status(thm)],[c262620,c15]) ).
cnf(c262986,plain,
multiply(inverse(X14468),multiply(X14469,X14468)) = X14469,
inference(resolution,[status(thm)],[c262774,symmetry]) ).
cnf(c263053,plain,
( X14635 != multiply(inverse(X14636),multiply(X14634,X14636))
| X14635 = X14634 ),
inference(resolution,[status(thm)],[c262986,transitivity]) ).
cnf(c271309,plain,
multiply(multiply(inverse(X14644),X14643),X14644) = X14643,
inference(resolution,[status(thm)],[c263053,c257871]) ).
cnf(c271624,plain,
( X14834 != multiply(multiply(inverse(X14833),X14832),X14833)
| X14834 = X14832 ),
inference(resolution,[status(thm)],[c271309,transitivity]) ).
cnf(c277638,plain,
multiply(multiply(inverse(X14847),X14847),X14846) = X14846,
inference(resolution,[status(thm)],[c271624,c269302]) ).
cnf(c278072,plain,
$false,
inference(resolution,[status(thm)],[c277638,prove_these_axioms_2]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.13 % Problem : GRP594-1 : TPTP v8.1.2. Released v2.6.0.
% 0.08/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.15/0.36 % Computer : n021.cluster.edu
% 0.15/0.36 % Model : x86_64 x86_64
% 0.15/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.36 % Memory : 8042.1875MB
% 0.15/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.36 % CPULimit : 300
% 0.15/0.36 % WCLimit : 300
% 0.15/0.36 % DateTime : Thu May 9 03:37:08 EDT 2024
% 0.15/0.36 % CPUTime :
% 225.99/226.26 % Version: 1.5
% 225.99/226.26 % SZS status Unsatisfiable
% 225.99/226.26 % SZS output start CNFRefutation
% See solution above
% 225.99/226.26
% 225.99/226.26 % Initial clauses : 9
% 225.99/226.26 % Processed clauses : 1847
% 225.99/226.26 % Factors computed : 3
% 225.99/226.26 % Resolvents computed: 278303
% 225.99/226.26 % Tautologies deleted: 2
% 225.99/226.26 % Forward subsumed : 2169
% 225.99/226.26 % Backward subsumed : 8
% 225.99/226.26 % -------- CPU Time ---------
% 225.99/226.26 % User time : 225.102 s
% 225.99/226.26 % System time : 0.746 s
% 225.99/226.26 % Total time : 225.848 s
%------------------------------------------------------------------------------