%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : GRP520-1 : TPTP v8.1.2. Bugfixed v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n009.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 148.79s 149.01s
% Output : Refutation 148.79s
% Verified :
% SZS Type : Refutation
% Derivation depth : 41
% Number of leaves : 7
% Syntax : Number of clauses : 87 ( 60 unt; 0 nHn; 24 RR)
% Number of literals : 116 ( 115 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 : 4 ( 4 usr; 2 con; 0-2 aty)
% Number of variables : 248 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(prove_these_axioms_4,negated_conjecture,
multiply(a,b) != multiply(b,a),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_these_axioms_4) ).
cnf(transitivity,axiom,
( X7 != X8
| X8 != X6
| X7 = X6 ),
theory(equality) ).
cnf(reflexivity,axiom,
X2 = X2,
theory(equality) ).
cnf(c0,axiom,
( X20 != X19
| X21 != X18
| multiply(X20,X21) = multiply(X19,X18) ),
theory(equality) ).
cnf(c10,plain,
( X29 != X30
| multiply(X29,X31) = multiply(X30,X31) ),
inference(resolution,[status(thm)],[c0,reflexivity]) ).
cnf(c1,axiom,
( X16 != X15
| inverse(X16) = inverse(X15) ),
theory(equality) ).
cnf(symmetry,axiom,
( X3 != X4
| X4 = X3 ),
theory(equality) ).
cnf(single_axiom,axiom,
multiply(X10,multiply(multiply(inverse(multiply(X10,X11)),X12),X11)) = X12,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',single_axiom) ).
cnf(c5,plain,
( X25 != multiply(X23,multiply(multiply(inverse(multiply(X23,X22)),X24),X22))
| X25 = X24 ),
inference(resolution,[status(thm)],[single_axiom,transitivity]) ).
cnf(c11,plain,
( X57 != X54
| multiply(X57,multiply(X56,multiply(multiply(inverse(multiply(X56,X55)),X58),X55))) = multiply(X54,X58) ),
inference(resolution,[status(thm)],[c0,single_axiom]) ).
cnf(c36,plain,
multiply(X84,multiply(X83,multiply(multiply(inverse(multiply(X83,X82)),X81),X82))) = multiply(X84,X81),
inference(resolution,[status(thm)],[c11,reflexivity]) ).
cnf(c79,plain,
( X895 != X891
| multiply(X895,multiply(X890,multiply(X893,multiply(multiply(inverse(multiply(X893,X892)),X894),X892)))) = multiply(X891,multiply(X890,X894)) ),
inference(resolution,[status(thm)],[c36,c0]) ).
cnf(c1935,plain,
multiply(X898,multiply(X896,multiply(X897,multiply(multiply(inverse(multiply(X897,X900)),X899),X900)))) = multiply(X898,multiply(X896,X899)),
inference(resolution,[status(thm)],[c79,reflexivity]) ).
cnf(c2016,plain,
( X1394 != multiply(X1395,multiply(X1398,multiply(X1397,multiply(multiply(inverse(multiply(X1397,X1396)),X1399),X1396))))
| X1394 = multiply(X1395,multiply(X1398,X1399)) ),
inference(resolution,[status(thm)],[c1935,transitivity]) ).
cnf(c8,plain,
inverse(multiply(X38,multiply(multiply(inverse(multiply(X38,X37)),X39),X37))) = inverse(X39),
inference(resolution,[status(thm)],[c1,single_axiom]) ).
cnf(c26,plain,
multiply(inverse(multiply(X144,multiply(multiply(inverse(multiply(X144,X143)),X145),X143))),X146) = multiply(inverse(X145),X146),
inference(resolution,[status(thm)],[c8,c10]) ).
cnf(c150,plain,
( X426 != multiply(inverse(multiply(X427,multiply(multiply(inverse(multiply(X427,X424)),X428),X424))),X425)
| X426 = multiply(inverse(X428),X425) ),
inference(resolution,[status(thm)],[c26,transitivity]) ).
cnf(c17,plain,
multiply(multiply(X69,multiply(multiply(inverse(multiply(X69,X68)),X70),X68)),X71) = multiply(X70,X71),
inference(resolution,[status(thm)],[c10,single_axiom]) ).
cnf(c52,plain,
( X467 != X464
| multiply(X467,multiply(multiply(X463,multiply(multiply(inverse(multiply(X463,X466)),X468),X466)),X465)) = multiply(X464,multiply(X468,X465)) ),
inference(resolution,[status(thm)],[c17,c0]) ).
cnf(c758,plain,
multiply(X470,multiply(multiply(X472,multiply(multiply(inverse(multiply(X472,X473)),X471),X473)),X469)) = multiply(X470,multiply(X471,X469)),
inference(resolution,[status(thm)],[c52,reflexivity]) ).
cnf(c816,plain,
multiply(X478,multiply(X475,X476)) = multiply(X478,multiply(multiply(X474,multiply(multiply(inverse(multiply(X474,X477)),X475),X477)),X476)),
inference(resolution,[status(thm)],[c758,symmetry]) ).
cnf(c822,plain,
multiply(X482,multiply(X479,X481)) = multiply(multiply(inverse(multiply(inverse(multiply(X482,X481)),X480)),X479),X480),
inference(resolution,[status(thm)],[c816,c5]) ).
cnf(c848,plain,
( X2212 != X2208
| multiply(X2212,multiply(X2213,multiply(X2211,X2210))) = multiply(X2208,multiply(multiply(inverse(multiply(inverse(multiply(X2213,X2210)),X2209)),X2211),X2209)) ),
inference(resolution,[status(thm)],[c822,c0]) ).
cnf(c7289,plain,
multiply(X2221,multiply(X2223,multiply(X2222,X2219))) = multiply(X2221,multiply(multiply(inverse(multiply(inverse(multiply(X2223,X2219)),X2220)),X2222),X2220)),
inference(resolution,[status(thm)],[c848,reflexivity]) ).
cnf(c7624,plain,
multiply(inverse(multiply(X2225,X2224)),multiply(X2225,multiply(X2226,X2224))) = X2226,
inference(resolution,[status(thm)],[c7289,c5]) ).
cnf(c7718,plain,
X2227 = multiply(inverse(multiply(X2228,X2229)),multiply(X2228,multiply(X2227,X2229))),
inference(resolution,[status(thm)],[c7624,symmetry]) ).
cnf(c7723,plain,
X2311 = multiply(inverse(X2310),multiply(X2312,multiply(X2311,multiply(multiply(inverse(multiply(X2312,X2309)),X2310),X2309)))),
inference(resolution,[status(thm)],[c7718,c150]) ).
cnf(c8315,plain,
X2314 = multiply(inverse(X2313),multiply(X2314,X2313)),
inference(resolution,[status(thm)],[c7723,c2016]) ).
cnf(c8333,plain,
multiply(inverse(multiply(inverse(X2327),X2327)),X2328) = X2328,
inference(resolution,[status(thm)],[c8315,c5]) ).
cnf(c8547,plain,
X2330 = multiply(inverse(multiply(inverse(X2329),X2329)),X2330),
inference(resolution,[status(thm)],[c8333,symmetry]) ).
cnf(c8357,plain,
multiply(inverse(X2324),multiply(X2323,X2324)) = X2323,
inference(resolution,[status(thm)],[c8315,symmetry]) ).
cnf(c8457,plain,
( X2356 != multiply(inverse(X2355),multiply(X2354,X2355))
| X2356 = X2354 ),
inference(resolution,[status(thm)],[c8357,transitivity]) ).
cnf(c9143,plain,
multiply(X2362,multiply(inverse(X2361),X2361)) = X2362,
inference(resolution,[status(thm)],[c8457,c8547]) ).
cnf(c9249,plain,
X2370 = multiply(X2370,multiply(inverse(X2369),X2369)),
inference(resolution,[status(thm)],[c9143,symmetry]) ).
cnf(c9322,plain,
inverse(X2418) = inverse(multiply(X2418,multiply(inverse(X2417),X2417))),
inference(resolution,[status(thm)],[c9249,c1]) ).
cnf(c9901,plain,
inverse(inverse(X2815)) = inverse(inverse(multiply(X2815,multiply(inverse(X2814),X2814)))),
inference(resolution,[status(thm)],[c9322,c1]) ).
cnf(c7698,plain,
( X2245 != multiply(inverse(multiply(X2244,X2243)),multiply(X2244,multiply(X2242,X2243)))
| X2245 = X2242 ),
inference(resolution,[status(thm)],[c7624,transitivity]) ).
cnf(c9315,plain,
inverse(multiply(inverse(multiply(X2377,X2376)),X2376)) = X2377,
inference(resolution,[status(thm)],[c9249,c7698]) ).
cnf(c9394,plain,
( X2503 != inverse(multiply(inverse(multiply(X2501,X2502)),X2502))
| X2503 = X2501 ),
inference(resolution,[status(thm)],[c9315,transitivity]) ).
cnf(c11020,plain,
inverse(inverse(multiply(X2508,multiply(inverse(X2509),X2509)))) = X2508,
inference(resolution,[status(thm)],[c9394,c9322]) ).
cnf(c11121,plain,
( X2998 != inverse(inverse(multiply(X2996,multiply(inverse(X2997),X2997))))
| X2998 = X2996 ),
inference(resolution,[status(thm)],[c11020,transitivity]) ).
cnf(c15573,plain,
inverse(inverse(X3006)) = X3006,
inference(resolution,[status(thm)],[c11121,c9901]) ).
cnf(c15732,plain,
multiply(inverse(inverse(X3052)),X3053) = multiply(X3052,X3053),
inference(resolution,[status(thm)],[c15573,c10]) ).
cnf(c16492,plain,
( X3947 != multiply(inverse(inverse(X3946)),X3945)
| X3947 = multiply(X3946,X3945) ),
inference(resolution,[status(thm)],[c15732,transitivity]) ).
cnf(c851,plain,
multiply(multiply(inverse(multiply(inverse(multiply(X485,X483)),X486)),X484),X486) = multiply(X485,multiply(X484,X483)),
inference(resolution,[status(thm)],[c822,symmetry]) ).
cnf(c861,plain,
( X551 != multiply(multiply(inverse(multiply(inverse(multiply(X552,X553)),X554)),X550),X554)
| X551 = multiply(X552,multiply(X550,X553)) ),
inference(resolution,[status(thm)],[c851,transitivity]) ).
cnf(c8581,plain,
multiply(X2576,X2578) = multiply(multiply(inverse(multiply(inverse(X2577),X2577)),X2576),X2578),
inference(resolution,[status(thm)],[c8547,c10]) ).
cnf(c11708,plain,
multiply(X2580,multiply(X2579,X2581)) = multiply(X2579,multiply(X2580,X2581)),
inference(resolution,[status(thm)],[c8581,c861]) ).
cnf(c11783,plain,
( X5793 != multiply(X5791,multiply(X5790,X5792))
| X5793 = multiply(X5790,multiply(X5791,X5792)) ),
inference(resolution,[status(thm)],[c11708,transitivity]) ).
cnf(c15729,plain,
( X3018 != inverse(inverse(X3017))
| X3018 = X3017 ),
inference(resolution,[status(thm)],[c15573,transitivity]) ).
cnf(c9415,plain,
X2386 = inverse(multiply(inverse(multiply(X2386,X2385)),X2385)),
inference(resolution,[status(thm)],[c9315,symmetry]) ).
cnf(c9474,plain,
inverse(X2520) = inverse(inverse(multiply(inverse(multiply(X2520,X2521)),X2521))),
inference(resolution,[status(thm)],[c9415,c1]) ).
cnf(c15910,plain,
inverse(X3069) = multiply(inverse(multiply(X3069,X3070)),X3070),
inference(resolution,[status(thm)],[c15729,c9474]) ).
cnf(c16748,plain,
multiply(inverse(multiply(X3087,X3088)),X3088) = inverse(X3087),
inference(resolution,[status(thm)],[c15910,symmetry]) ).
cnf(c16984,plain,
multiply(inverse(multiply(inverse(X3122),X3121)),X3121) = X3122,
inference(resolution,[status(thm)],[c16748,c15729]) ).
cnf(c17409,plain,
X3139 = multiply(inverse(multiply(inverse(X3139),X3138)),X3138),
inference(resolution,[status(thm)],[c16984,symmetry]) ).
cnf(c17532,plain,
multiply(X7838,X7840) = multiply(multiply(inverse(multiply(inverse(X7838),X7839)),X7839),X7840),
inference(resolution,[status(thm)],[c17409,c10]) ).
cnf(c81516,plain,
multiply(multiply(X7841,X7843),X7842) = multiply(X7841,multiply(X7842,X7843)),
inference(resolution,[status(thm)],[c17532,c861]) ).
cnf(c81686,plain,
multiply(multiply(X7919,X7917),X7918) = multiply(X7918,multiply(X7919,X7917)),
inference(resolution,[status(thm)],[c81516,c11783]) ).
cnf(c15718,plain,
X3007 = inverse(inverse(X3007)),
inference(resolution,[status(thm)],[c15573,symmetry]) ).
cnf(c15789,plain,
multiply(X3054,X3055) = multiply(inverse(inverse(X3054)),X3055),
inference(resolution,[status(thm)],[c15718,c10]) ).
cnf(c16577,plain,
multiply(X3056,multiply(X3057,inverse(X3056))) = X3057,
inference(resolution,[status(thm)],[c15789,c8457]) ).
cnf(c16622,plain,
X3059 = multiply(X3058,multiply(X3059,inverse(X3058))),
inference(resolution,[status(thm)],[c16577,symmetry]) ).
cnf(c16700,plain,
multiply(inverse(multiply(X3086,inverse(X3086))),X3085) = X3085,
inference(resolution,[status(thm)],[c16622,c5]) ).
cnf(c16916,plain,
X3104 = multiply(inverse(multiply(X3103,inverse(X3103))),X3104),
inference(resolution,[status(thm)],[c16700,symmetry]) ).
cnf(c17178,plain,
multiply(X3108,multiply(X3107,inverse(X3107))) = X3108,
inference(resolution,[status(thm)],[c16916,c8457]) ).
cnf(c17234,plain,
( X3391 != multiply(X3389,multiply(X3390,inverse(X3390)))
| X3391 = X3389 ),
inference(resolution,[status(thm)],[c17178,transitivity]) ).
cnf(c81653,plain,
multiply(multiply(X7857,inverse(X7856)),X7856) = X7857,
inference(resolution,[status(thm)],[c81516,c17234]) ).
cnf(c82073,plain,
( X8055 != multiply(multiply(X8053,inverse(X8054)),X8054)
| X8055 = X8053 ),
inference(resolution,[status(thm)],[c81653,transitivity]) ).
cnf(c85788,plain,
multiply(X8425,X8426) = inverse(multiply(inverse(X8425),inverse(X8426))),
inference(resolution,[status(thm)],[c82073,c17532]) ).
cnf(c8348,plain,
multiply(X2439,X2440) = multiply(multiply(inverse(X2438),multiply(X2439,X2438)),X2440),
inference(resolution,[status(thm)],[c8315,c10]) ).
cnf(c9228,plain,
( X2404 != multiply(X2402,multiply(inverse(X2403),X2403))
| X2404 = X2402 ),
inference(resolution,[status(thm)],[c9143,transitivity]) ).
cnf(c81635,plain,
multiply(multiply(X7855,X7854),inverse(X7854)) = X7855,
inference(resolution,[status(thm)],[c81516,c9228]) ).
cnf(c81926,plain,
( X7941 != multiply(multiply(X7939,X7940),inverse(X7940))
| X7941 = X7939 ),
inference(resolution,[status(thm)],[c81635,transitivity]) ).
cnf(c84136,plain,
multiply(X8002,inverse(multiply(X8002,X8003))) = inverse(X8003),
inference(resolution,[status(thm)],[c81926,c8348]) ).
cnf(c84745,plain,
inverse(multiply(X8822,inverse(multiply(X8822,X8821)))) = inverse(inverse(X8821)),
inference(resolution,[status(thm)],[c84136,c1]) ).
cnf(c100007,plain,
inverse(multiply(X8823,inverse(multiply(X8823,X8824)))) = X8824,
inference(resolution,[status(thm)],[c84745,c15729]) ).
cnf(c100153,plain,
( X9782 != inverse(multiply(X9780,inverse(multiply(X9780,X9781))))
| X9782 = X9781 ),
inference(resolution,[status(thm)],[c100007,transitivity]) ).
cnf(c120126,plain,
multiply(X9805,multiply(inverse(X9805),X9806)) = X9806,
inference(resolution,[status(thm)],[c100153,c85788]) ).
cnf(c120440,plain,
( X9899 != multiply(X9898,multiply(inverse(X9898),X9897))
| X9899 = X9897 ),
inference(resolution,[status(thm)],[c120126,transitivity]) ).
cnf(c121807,plain,
multiply(multiply(inverse(X9934),X9933),X9934) = X9933,
inference(resolution,[status(thm)],[c120440,c81686]) ).
cnf(c122669,plain,
( X10374 != multiply(multiply(inverse(X10373),X10372),X10373)
| X10374 = X10372 ),
inference(resolution,[status(thm)],[c121807,transitivity]) ).
cnf(c120417,plain,
X9818 = multiply(X9817,multiply(inverse(X9817),X9818)),
inference(resolution,[status(thm)],[c120126,symmetry]) ).
cnf(c120750,plain,
multiply(X11727,X11728) = multiply(multiply(X11726,multiply(inverse(X11726),X11727)),X11728),
inference(resolution,[status(thm)],[c120417,c10]) ).
cnf(c155433,plain,
multiply(X11730,X11729) = multiply(inverse(inverse(X11729)),X11730),
inference(resolution,[status(thm)],[c120750,c122669]) ).
cnf(c155671,plain,
multiply(X11732,X11731) = multiply(X11731,X11732),
inference(resolution,[status(thm)],[c155433,c16492]) ).
cnf(c155812,plain,
$false,
inference(resolution,[status(thm)],[c155671,prove_these_axioms_4]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12 % Problem : GRP520-1 : TPTP v8.1.2. Bugfixed v2.7.0.
% 0.06/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.12/0.34 % Computer : n009.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 300
% 0.12/0.34 % DateTime : Thu May 9 04:59:08 EDT 2024
% 0.12/0.34 % CPUTime :
% 148.79/149.01 % Version: 1.5
% 148.79/149.01 % SZS status Unsatisfiable
% 148.79/149.01 % SZS output start CNFRefutation
% See solution above
% 148.79/149.01
% 148.79/149.01 % Initial clauses : 7
% 148.79/149.01 % Processed clauses : 1428
% 148.79/149.01 % Factors computed : 2
% 148.79/149.01 % Resolvents computed: 155841
% 148.79/149.01 % Tautologies deleted: 2
% 148.79/149.01 % Forward subsumed : 2558
% 148.79/149.01 % Backward subsumed : 31
% 148.79/149.01 % -------- CPU Time ---------
% 148.79/149.01 % User time : 148.168 s
% 148.79/149.01 % System time : 0.498 s
% 148.79/149.01 % Total time : 148.666 s
%------------------------------------------------------------------------------