%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : GRP519-1 : TPTP v8.1.2. Released v2.6.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n026.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:57 EDT 2024
% Result : Unsatisfiable 192.86s 193.05s
% Output : Refutation 192.86s
% Verified :
% SZS Type : Refutation
% Derivation depth : 46
% Number of leaves : 7
% Syntax : Number of clauses : 91 ( 64 unt; 0 nHn; 24 RR)
% Number of literals : 120 ( 119 equ; 30 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 : 5 ( 5 usr; 3 con; 0-2 aty)
% Number of variables : 262 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(prove_these_axioms_3,negated_conjecture,
multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_these_axioms_3) ).
cnf(transitivity,axiom,
( X6 != X7
| X7 != X8
| X6 = X8 ),
theory(equality) ).
cnf(symmetry,axiom,
( X3 != X4
| X4 = X3 ),
theory(equality) ).
cnf(single_axiom,axiom,
multiply(X12,multiply(multiply(inverse(multiply(X12,X11)),X10),X11)) = X10,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',single_axiom) ).
cnf(c6,plain,
( X36 != multiply(X39,multiply(multiply(inverse(multiply(X39,X37)),X38),X37))
| X36 = X38 ),
inference(resolution,[status(thm)],[single_axiom,transitivity]) ).
cnf(reflexivity,axiom,
X2 = X2,
theory(equality) ).
cnf(c0,axiom,
( X19 != X20
| X18 != X21
| multiply(X19,X18) = multiply(X20,X21) ),
theory(equality) ).
cnf(c10,plain,
( X27 != X26
| multiply(X27,X25) = multiply(X26,X25) ),
inference(resolution,[status(thm)],[c0,reflexivity]) ).
cnf(c15,plain,
multiply(multiply(X71,multiply(multiply(inverse(multiply(X71,X68)),X69),X68)),X70) = multiply(X69,X70),
inference(resolution,[status(thm)],[c10,single_axiom]) ).
cnf(c54,plain,
( X490 != X487
| multiply(X490,multiply(multiply(X489,multiply(multiply(inverse(multiply(X489,X491)),X488),X491)),X492)) = multiply(X487,multiply(X488,X492)) ),
inference(resolution,[status(thm)],[c15,c0]) ).
cnf(c832,plain,
multiply(X494,multiply(multiply(X497,multiply(multiply(inverse(multiply(X497,X495)),X493),X495)),X496)) = multiply(X494,multiply(X493,X496)),
inference(resolution,[status(thm)],[c54,reflexivity]) ).
cnf(c863,plain,
multiply(X500,multiply(X499,X498)) = multiply(X500,multiply(multiply(X501,multiply(multiply(inverse(multiply(X501,X502)),X499),X502)),X498)),
inference(resolution,[status(thm)],[c832,symmetry]) ).
cnf(c892,plain,
multiply(X503,multiply(X505,X506)) = multiply(multiply(inverse(multiply(inverse(multiply(X503,X506)),X504)),X505),X504),
inference(resolution,[status(thm)],[c863,c6]) ).
cnf(c900,plain,
multiply(multiply(inverse(multiply(inverse(multiply(X509,X508)),X507)),X510),X507) = multiply(X509,multiply(X510,X508)),
inference(resolution,[status(thm)],[c892,symmetry]) ).
cnf(c924,plain,
( X567 != multiply(multiply(inverse(multiply(inverse(multiply(X570,X568)),X566)),X569),X566)
| X567 = multiply(X570,multiply(X569,X568)) ),
inference(resolution,[status(thm)],[c900,transitivity]) ).
cnf(c1,axiom,
( X15 != X16
| inverse(X15) = inverse(X16) ),
theory(equality) ).
cnf(c11,plain,
( X57 != X54
| multiply(X57,multiply(X58,multiply(multiply(inverse(multiply(X58,X55)),X56),X55))) = multiply(X54,X56) ),
inference(resolution,[status(thm)],[c0,single_axiom]) ).
cnf(c35,plain,
multiply(X79,multiply(X81,multiply(multiply(inverse(multiply(X81,X80)),X82),X80))) = multiply(X79,X82),
inference(resolution,[status(thm)],[c11,reflexivity]) ).
cnf(c80,plain,
( X896 != X894
| multiply(X896,multiply(X898,multiply(X897,multiply(multiply(inverse(multiply(X897,X895)),X899),X895)))) = multiply(X894,multiply(X898,X899)) ),
inference(resolution,[status(thm)],[c35,c0]) ).
cnf(c1941,plain,
multiply(X906,multiply(X907,multiply(X904,multiply(multiply(inverse(multiply(X904,X908)),X905),X908)))) = multiply(X906,multiply(X907,X905)),
inference(resolution,[status(thm)],[c80,reflexivity]) ).
cnf(c1999,plain,
( X1350 != multiply(X1351,multiply(X1347,multiply(X1348,multiply(multiply(inverse(multiply(X1348,X1352)),X1349),X1352))))
| X1350 = multiply(X1351,multiply(X1347,X1349)) ),
inference(resolution,[status(thm)],[c1941,transitivity]) ).
cnf(c8,plain,
inverse(multiply(X46,multiply(multiply(inverse(multiply(X46,X44)),X45),X44))) = inverse(X45),
inference(resolution,[status(thm)],[c1,single_axiom]) ).
cnf(c27,plain,
multiply(inverse(multiply(X143,multiply(multiply(inverse(multiply(X143,X146)),X145),X146))),X144) = multiply(inverse(X145),X144),
inference(resolution,[status(thm)],[c8,c10]) ).
cnf(c150,plain,
( X426 != multiply(inverse(multiply(X425,multiply(multiply(inverse(multiply(X425,X427)),X424),X427))),X428)
| X426 = multiply(inverse(X424),X428) ),
inference(resolution,[status(thm)],[c27,transitivity]) ).
cnf(c898,plain,
( X2283 != X2281
| multiply(X2283,multiply(X2284,multiply(X2282,X2279))) = multiply(X2281,multiply(multiply(inverse(multiply(inverse(multiply(X2284,X2279)),X2280)),X2282),X2280)) ),
inference(resolution,[status(thm)],[c892,c0]) ).
cnf(c7876,plain,
multiply(X2289,multiply(X2288,multiply(X2286,X2285))) = multiply(X2289,multiply(multiply(inverse(multiply(inverse(multiply(X2288,X2285)),X2287)),X2286),X2287)),
inference(resolution,[status(thm)],[c898,reflexivity]) ).
cnf(c8080,plain,
multiply(inverse(multiply(X2292,X2290)),multiply(X2292,multiply(X2291,X2290))) = X2291,
inference(resolution,[status(thm)],[c7876,c6]) ).
cnf(c8113,plain,
X2294 = multiply(inverse(multiply(X2293,X2295)),multiply(X2293,multiply(X2294,X2295))),
inference(resolution,[status(thm)],[c8080,symmetry]) ).
cnf(c8186,plain,
X2383 = multiply(inverse(X2381),multiply(X2380,multiply(X2383,multiply(multiply(inverse(multiply(X2380,X2382)),X2381),X2382)))),
inference(resolution,[status(thm)],[c8113,c150]) ).
cnf(c8984,plain,
X2392 = multiply(inverse(X2391),multiply(X2392,X2391)),
inference(resolution,[status(thm)],[c8186,c1999]) ).
cnf(c9057,plain,
multiply(inverse(multiply(inverse(X2399),X2399)),X2398) = X2398,
inference(resolution,[status(thm)],[c8984,c6]) ).
cnf(c9162,plain,
X2405 = multiply(inverse(multiply(inverse(X2404),X2404)),X2405),
inference(resolution,[status(thm)],[c9057,symmetry]) ).
cnf(c9037,plain,
multiply(inverse(X2395),multiply(X2394,X2395)) = X2394,
inference(resolution,[status(thm)],[c8984,symmetry]) ).
cnf(c9107,plain,
( X2423 != multiply(inverse(X2424),multiply(X2425,X2424))
| X2423 = X2425 ),
inference(resolution,[status(thm)],[c9037,transitivity]) ).
cnf(c9754,plain,
multiply(X2429,multiply(inverse(X2428),X2428)) = X2429,
inference(resolution,[status(thm)],[c9107,c9162]) ).
cnf(c9842,plain,
X2439 = multiply(X2439,multiply(inverse(X2438),X2438)),
inference(resolution,[status(thm)],[c9754,symmetry]) ).
cnf(c9990,plain,
inverse(X2491) = inverse(multiply(X2491,multiply(inverse(X2492),X2492))),
inference(resolution,[status(thm)],[c9842,c1]) ).
cnf(c10597,plain,
inverse(inverse(X2913)) = inverse(inverse(multiply(X2913,multiply(inverse(X2912),X2912)))),
inference(resolution,[status(thm)],[c9990,c1]) ).
cnf(c8130,plain,
( X2306 != multiply(inverse(multiply(X2307,X2308)),multiply(X2307,multiply(X2309,X2308)))
| X2306 = X2309 ),
inference(resolution,[status(thm)],[c8080,transitivity]) ).
cnf(c9976,plain,
inverse(multiply(inverse(multiply(X2452,X2451)),X2451)) = X2452,
inference(resolution,[status(thm)],[c9842,c8130]) ).
cnf(c10034,plain,
( X2566 != inverse(multiply(inverse(multiply(X2568,X2567)),X2567))
| X2566 = X2568 ),
inference(resolution,[status(thm)],[c9976,transitivity]) ).
cnf(c11447,plain,
inverse(inverse(multiply(X2577,multiply(inverse(X2578),X2578)))) = X2577,
inference(resolution,[status(thm)],[c10034,c9990]) ).
cnf(c11554,plain,
( X3047 != inverse(inverse(multiply(X3049,multiply(inverse(X3048),X3048))))
| X3047 = X3049 ),
inference(resolution,[status(thm)],[c11447,transitivity]) ).
cnf(c16460,plain,
inverse(inverse(X3051)) = X3051,
inference(resolution,[status(thm)],[c11554,c10597]) ).
cnf(c16491,plain,
( X3061 != inverse(inverse(X3062))
| X3061 = X3062 ),
inference(resolution,[status(thm)],[c16460,transitivity]) ).
cnf(c10015,plain,
X2454 = inverse(multiply(inverse(multiply(X2454,X2453)),X2453)),
inference(resolution,[status(thm)],[c9976,symmetry]) ).
cnf(c10104,plain,
inverse(X2593) = inverse(inverse(multiply(inverse(multiply(X2593,X2594)),X2594))),
inference(resolution,[status(thm)],[c10015,c1]) ).
cnf(c16924,plain,
inverse(X3117) = multiply(inverse(multiply(X3117,X3118)),X3118),
inference(resolution,[status(thm)],[c16491,c10104]) ).
cnf(c17929,plain,
multiply(inverse(multiply(X3144,X3143)),X3143) = inverse(X3144),
inference(resolution,[status(thm)],[c16924,symmetry]) ).
cnf(c18203,plain,
multiply(inverse(multiply(inverse(X3175),X3174)),X3174) = X3175,
inference(resolution,[status(thm)],[c17929,c16491]) ).
cnf(c18668,plain,
X3192 = multiply(inverse(multiply(inverse(X3192),X3191)),X3191),
inference(resolution,[status(thm)],[c18203,symmetry]) ).
cnf(c18747,plain,
multiply(X7913,X7911) = multiply(multiply(inverse(multiply(inverse(X7913),X7912)),X7912),X7911),
inference(resolution,[status(thm)],[c18668,c10]) ).
cnf(c83524,plain,
multiply(multiply(X7915,X7914),X7916) = multiply(X7915,multiply(X7916,X7914)),
inference(resolution,[status(thm)],[c18747,c924]) ).
cnf(c17900,plain,
multiply(inverse(X7655),X7654) = multiply(multiply(inverse(multiply(X7655,X7656)),X7656),X7654),
inference(resolution,[status(thm)],[c16924,c10]) ).
cnf(c16559,plain,
X3052 = inverse(inverse(X3052)),
inference(resolution,[status(thm)],[c16460,symmetry]) ).
cnf(c16588,plain,
multiply(X3102,X3101) = multiply(inverse(inverse(X3102)),X3101),
inference(resolution,[status(thm)],[c16559,c10]) ).
cnf(c17658,plain,
multiply(X3103,multiply(X3104,inverse(X3103))) = X3104,
inference(resolution,[status(thm)],[c16588,c9107]) ).
cnf(c17764,plain,
X3112 = multiply(X3113,multiply(X3112,inverse(X3113))),
inference(resolution,[status(thm)],[c17658,symmetry]) ).
cnf(c17854,plain,
multiply(inverse(multiply(X3134,inverse(X3134))),X3135) = X3135,
inference(resolution,[status(thm)],[c17764,c6]) ).
cnf(c18114,plain,
X3151 = multiply(inverse(multiply(X3152,inverse(X3152))),X3151),
inference(resolution,[status(thm)],[c17854,symmetry]) ).
cnf(c18317,plain,
multiply(X3160,multiply(X3159,inverse(X3159))) = X3160,
inference(resolution,[status(thm)],[c18114,c9107]) ).
cnf(c18397,plain,
( X3456 != multiply(X3457,multiply(X3458,inverse(X3458)))
| X3456 = X3457 ),
inference(resolution,[status(thm)],[c18317,transitivity]) ).
cnf(c83633,plain,
multiply(multiply(X7928,inverse(X7929)),X7929) = X7928,
inference(resolution,[status(thm)],[c83524,c18397]) ).
cnf(c83949,plain,
( X8120 != multiply(multiply(X8122,inverse(X8121)),X8121)
| X8120 = X8122 ),
inference(resolution,[status(thm)],[c83633,transitivity]) ).
cnf(c87477,plain,
multiply(inverse(X8471),X8472) = inverse(multiply(X8471,inverse(X8472))),
inference(resolution,[status(thm)],[c83949,c17900]) ).
cnf(c9038,plain,
multiply(X2518,X2516) = multiply(multiply(inverse(X2517),multiply(X2518,X2517)),X2516),
inference(resolution,[status(thm)],[c8984,c10]) ).
cnf(c9861,plain,
( X2467 != multiply(X2469,multiply(inverse(X2468),X2468))
| X2467 = X2469 ),
inference(resolution,[status(thm)],[c9754,transitivity]) ).
cnf(c83619,plain,
multiply(multiply(X7927,X7926),inverse(X7926)) = X7927,
inference(resolution,[status(thm)],[c83524,c9861]) ).
cnf(c83799,plain,
( X8005 != multiply(multiply(X8007,X8006),inverse(X8006))
| X8005 = X8007 ),
inference(resolution,[status(thm)],[c83619,transitivity]) ).
cnf(c85878,plain,
multiply(X8073,inverse(multiply(X8073,X8072))) = inverse(X8072),
inference(resolution,[status(thm)],[c83799,c9038]) ).
cnf(c86524,plain,
inverse(multiply(X9040,inverse(multiply(X9040,X9039)))) = inverse(inverse(X9039)),
inference(resolution,[status(thm)],[c85878,c1]) ).
cnf(c105693,plain,
inverse(multiply(X9050,inverse(multiply(X9050,X9049)))) = X9049,
inference(resolution,[status(thm)],[c86524,c16491]) ).
cnf(c105879,plain,
( X9888 != inverse(multiply(X9890,inverse(multiply(X9890,X9889))))
| X9888 = X9889 ),
inference(resolution,[status(thm)],[c105693,transitivity]) ).
cnf(c122905,plain,
multiply(inverse(X9923),multiply(X9923,X9922)) = X9922,
inference(resolution,[status(thm)],[c105879,c87477]) ).
cnf(c123409,plain,
( X10004 != multiply(inverse(X10006),multiply(X10006,X10005))
| X10004 = X10005 ),
inference(resolution,[status(thm)],[c122905,transitivity]) ).
cnf(c125097,plain,
multiply(multiply(inverse(X10101),X10102),X10101) = X10102,
inference(resolution,[status(thm)],[c123409,c83524]) ).
cnf(c125848,plain,
( X10586 != multiply(multiply(inverse(X10588),X10587),X10588)
| X10586 = X10587 ),
inference(resolution,[status(thm)],[c125097,transitivity]) ).
cnf(c123536,plain,
X9926 = multiply(inverse(X9927),multiply(X9927,X9926)),
inference(resolution,[status(thm)],[c122905,symmetry]) ).
cnf(c123770,plain,
multiply(X11812,X11811) = multiply(multiply(inverse(X11813),multiply(X11813,X11812)),X11811),
inference(resolution,[status(thm)],[c123536,c10]) ).
cnf(c158792,plain,
multiply(X11815,X11814) = multiply(X11814,X11815),
inference(resolution,[status(thm)],[c123770,c125848]) ).
cnf(c158897,plain,
( X11876 != multiply(X11877,X11878)
| X11876 = multiply(X11878,X11877) ),
inference(resolution,[status(thm)],[c158792,transitivity]) ).
cnf(c9270,plain,
multiply(X2643,X2642) = multiply(multiply(inverse(multiply(inverse(X2641),X2641)),X2643),X2642),
inference(resolution,[status(thm)],[c9162,c10]) ).
cnf(c12301,plain,
multiply(X2646,multiply(X2645,X2644)) = multiply(X2645,multiply(X2646,X2644)),
inference(resolution,[status(thm)],[c9270,c924]) ).
cnf(c12349,plain,
( X5830 != multiply(X5832,multiply(X5833,X5831))
| X5830 = multiply(X5833,multiply(X5832,X5831)) ),
inference(resolution,[status(thm)],[c12301,transitivity]) ).
cnf(c158924,plain,
multiply(multiply(X12199,X12200),X12198) = multiply(multiply(X12200,X12199),X12198),
inference(resolution,[status(thm)],[c158792,c10]) ).
cnf(c166266,plain,
multiply(multiply(X12631,X12633),X12632) = multiply(X12632,multiply(X12633,X12631)),
inference(resolution,[status(thm)],[c158924,c158897]) ).
cnf(c171399,plain,
multiply(multiply(X12853,X12851),X12852) = multiply(X12851,multiply(X12852,X12853)),
inference(resolution,[status(thm)],[c166266,c12349]) ).
cnf(c174211,plain,
multiply(multiply(X12947,X12948),X12946) = multiply(multiply(X12946,X12947),X12948),
inference(resolution,[status(thm)],[c171399,c158897]) ).
cnf(c175547,plain,
multiply(multiply(X13029,X13030),X13028) = multiply(multiply(X13030,X13028),X13029),
inference(resolution,[status(thm)],[c174211,symmetry]) ).
cnf(c176604,plain,
multiply(multiply(X13117,X13115),X13116) = multiply(X13117,multiply(X13115,X13116)),
inference(resolution,[status(thm)],[c175547,c158897]) ).
cnf(c178858,plain,
$false,
inference(resolution,[status(thm)],[c176604,prove_these_axioms_3]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.12 % Problem : GRP519-1 : TPTP v8.1.2. Released v2.6.0.
% 0.04/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.34 % Computer : n026.cluster.edu
% 0.14/0.34 % Model : x86_64 x86_64
% 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.34 % Memory : 8042.1875MB
% 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.34 % CPULimit : 300
% 0.14/0.34 % WCLimit : 300
% 0.14/0.34 % DateTime : Thu May 9 03:32:53 EDT 2024
% 0.14/0.34 % CPUTime :
% 192.86/193.05 % Version: 1.5
% 192.86/193.05 % SZS status Unsatisfiable
% 192.86/193.05 % SZS output start CNFRefutation
% See solution above
% 192.86/193.06
% 192.86/193.06 % Initial clauses : 7
% 192.86/193.06 % Processed clauses : 1540
% 192.86/193.06 % Factors computed : 2
% 192.86/193.06 % Resolvents computed: 178968
% 192.86/193.06 % Tautologies deleted: 2
% 192.86/193.06 % Forward subsumed : 2923
% 192.86/193.06 % Backward subsumed : 34
% 192.86/193.06 % -------- CPU Time ---------
% 192.86/193.06 % User time : 192.203 s
% 192.86/193.06 % System time : 0.516 s
% 192.86/193.06 % Total time : 192.719 s
%------------------------------------------------------------------------------