%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : GRP517-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 6.59s 6.79s
% Output : Refutation 6.59s
% Verified :
% SZS Type : Refutation
% Derivation depth : 21
% Number of leaves : 7
% Syntax : Number of clauses : 39 ( 24 unt; 0 nHn; 11 RR)
% Number of literals : 56 ( 55 equ; 18 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 : 130 ( 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(symmetry,axiom,
( X4 != X3
| X3 = X4 ),
theory(equality) ).
cnf(transitivity,axiom,
( X8 != X6
| X6 != X7
| X8 = X7 ),
theory(equality) ).
cnf(single_axiom,axiom,
multiply(X12,multiply(multiply(inverse(multiply(X12,X10)),X11),X10)) = X11,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',single_axiom) ).
cnf(c5,plain,
( X22 != multiply(X25,multiply(multiply(inverse(multiply(X25,X23)),X24),X23))
| X22 = X24 ),
inference(resolution,[status(thm)],[single_axiom,transitivity]) ).
cnf(reflexivity,axiom,
X2 = X2,
theory(equality) ).
cnf(c0,axiom,
( X19 != X18
| X21 != X20
| multiply(X19,X21) = multiply(X18,X20) ),
theory(equality) ).
cnf(c10,plain,
( X31 != X30
| multiply(X31,X29) = multiply(X30,X29) ),
inference(resolution,[status(thm)],[c0,reflexivity]) ).
cnf(c1,axiom,
( X16 != X15
| inverse(X16) = inverse(X15) ),
theory(equality) ).
cnf(c8,plain,
inverse(multiply(X39,multiply(multiply(inverse(multiply(X39,X37)),X38),X37))) = inverse(X38),
inference(resolution,[status(thm)],[c1,single_axiom]) ).
cnf(c25,plain,
multiply(inverse(multiply(X146,multiply(multiply(inverse(multiply(X146,X144)),X143),X144))),X145) = multiply(inverse(X143),X145),
inference(resolution,[status(thm)],[c8,c10]) ).
cnf(c151,plain,
( X424 != multiply(inverse(multiply(X425,multiply(multiply(inverse(multiply(X425,X427)),X426),X427))),X428)
| X424 = multiply(inverse(X426),X428) ),
inference(resolution,[status(thm)],[c25,transitivity]) ).
cnf(c11,plain,
( X54 != X58
| multiply(X54,multiply(X57,multiply(multiply(inverse(multiply(X57,X56)),X55),X56))) = multiply(X58,X55) ),
inference(resolution,[status(thm)],[c0,single_axiom]) ).
cnf(c36,plain,
multiply(X82,multiply(X81,multiply(multiply(inverse(multiply(X81,X84)),X83),X84))) = multiply(X82,X83),
inference(resolution,[status(thm)],[c11,reflexivity]) ).
cnf(c77,plain,
( X889 != X893
| multiply(X889,multiply(X891,multiply(X892,multiply(multiply(inverse(multiply(X892,X894)),X890),X894)))) = multiply(X893,multiply(X891,X890)) ),
inference(resolution,[status(thm)],[c36,c0]) ).
cnf(c1943,plain,
multiply(X895,multiply(X896,multiply(X898,multiply(multiply(inverse(multiply(X898,X899)),X897),X899)))) = multiply(X895,multiply(X896,X897)),
inference(resolution,[status(thm)],[c77,reflexivity]) ).
cnf(c2011,plain,
( X1389 != multiply(X1391,multiply(X1390,multiply(X1394,multiply(multiply(inverse(multiply(X1394,X1393)),X1392),X1393))))
| X1389 = multiply(X1391,multiply(X1390,X1392)) ),
inference(resolution,[status(thm)],[c1943,transitivity]) ).
cnf(c17,plain,
multiply(multiply(X71,multiply(multiply(inverse(multiply(X71,X68)),X70),X68)),X69) = multiply(X70,X69),
inference(resolution,[status(thm)],[c10,single_axiom]) ).
cnf(c50,plain,
( X465 != X468
| multiply(X465,multiply(multiply(X463,multiply(multiply(inverse(multiply(X463,X467)),X464),X467)),X466)) = multiply(X468,multiply(X464,X466)) ),
inference(resolution,[status(thm)],[c17,c0]) ).
cnf(c762,plain,
multiply(X470,multiply(multiply(X469,multiply(multiply(inverse(multiply(X469,X472)),X473),X472)),X471)) = multiply(X470,multiply(X473,X471)),
inference(resolution,[status(thm)],[c50,reflexivity]) ).
cnf(c816,plain,
multiply(X474,multiply(X475,X478)) = multiply(X474,multiply(multiply(X477,multiply(multiply(inverse(multiply(X477,X476)),X475),X476)),X478)),
inference(resolution,[status(thm)],[c762,symmetry]) ).
cnf(c825,plain,
multiply(X479,multiply(X482,X481)) = multiply(multiply(inverse(multiply(inverse(multiply(X479,X481)),X480)),X482),X480),
inference(resolution,[status(thm)],[c816,c5]) ).
cnf(c837,plain,
( X2204 != X2209
| multiply(X2204,multiply(X2205,multiply(X2208,X2206))) = multiply(X2209,multiply(multiply(inverse(multiply(inverse(multiply(X2205,X2206)),X2207)),X2208),X2207)) ),
inference(resolution,[status(thm)],[c825,c0]) ).
cnf(c7439,plain,
multiply(X2211,multiply(X2210,multiply(X2214,X2213))) = multiply(X2211,multiply(multiply(inverse(multiply(inverse(multiply(X2210,X2213)),X2212)),X2214),X2212)),
inference(resolution,[status(thm)],[c837,reflexivity]) ).
cnf(c7600,plain,
multiply(inverse(multiply(X2217,X2215)),multiply(X2217,multiply(X2216,X2215))) = X2216,
inference(resolution,[status(thm)],[c7439,c5]) ).
cnf(c7690,plain,
X2223 = multiply(inverse(multiply(X2221,X2222)),multiply(X2221,multiply(X2223,X2222))),
inference(resolution,[status(thm)],[c7600,symmetry]) ).
cnf(c7727,plain,
X2304 = multiply(inverse(multiply(X2303,multiply(multiply(inverse(multiply(X2304,X2306)),X2305),X2306))),multiply(X2303,X2305)),
inference(resolution,[status(thm)],[c7690,c2011]) ).
cnf(c8294,plain,
X2308 = multiply(inverse(X2307),multiply(X2308,X2307)),
inference(resolution,[status(thm)],[c7727,c151]) ).
cnf(c8344,plain,
multiply(inverse(multiply(inverse(X2321),X2321)),X2320) = X2320,
inference(resolution,[status(thm)],[c8294,c5]) ).
cnf(c8699,plain,
X2322 = multiply(inverse(multiply(inverse(X2323),X2323)),X2322),
inference(resolution,[status(thm)],[c8344,symmetry]) ).
cnf(c8365,plain,
multiply(inverse(X2311),multiply(X2310,X2311)) = X2310,
inference(resolution,[status(thm)],[c8294,symmetry]) ).
cnf(c8389,plain,
( X2342 != multiply(inverse(X2343),multiply(X2344,X2343))
| X2342 = X2344 ),
inference(resolution,[status(thm)],[c8365,transitivity]) ).
cnf(c9093,plain,
multiply(X2353,multiply(inverse(X2354),X2354)) = X2353,
inference(resolution,[status(thm)],[c8389,c8699]) ).
cnf(c9160,plain,
( X2385 != multiply(X2386,multiply(inverse(X2387),X2387))
| X2385 = X2386 ),
inference(resolution,[status(thm)],[c9093,transitivity]) ).
cnf(c9590,plain,
multiply(inverse(X2418),X2418) = inverse(multiply(inverse(X2419),X2419)),
inference(resolution,[status(thm)],[c9160,c8699]) ).
cnf(c10161,plain,
inverse(multiply(inverse(X2424),X2424)) = multiply(inverse(X2425),X2425),
inference(resolution,[status(thm)],[c9590,symmetry]) ).
cnf(c10180,plain,
( X2882 != inverse(multiply(inverse(X2884),X2884))
| X2882 = multiply(inverse(X2883),X2883) ),
inference(resolution,[status(thm)],[c10161,transitivity]) ).
cnf(c14528,plain,
multiply(inverse(X2886),X2886) = multiply(inverse(X2885),X2885),
inference(resolution,[status(thm)],[c10180,c9590]) ).
cnf(c14560,plain,
$false,
inference(resolution,[status(thm)],[c14528,prove_these_axioms_1]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.12 % Problem : GRP517-1 : TPTP v8.1.2. Released v2.6.0.
% 0.04/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.34 % Computer : n026.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Thu May 9 04:14:37 EDT 2024
% 0.13/0.34 % CPUTime :
% 6.59/6.79 % Version: 1.5
% 6.59/6.79 % SZS status Unsatisfiable
% 6.59/6.79 % SZS output start CNFRefutation
% See solution above
% 6.59/6.79
% 6.59/6.79 % Initial clauses : 7
% 6.59/6.79 % Processed clauses : 365
% 6.59/6.79 % Factors computed : 2
% 6.59/6.79 % Resolvents computed: 14599
% 6.59/6.79 % Tautologies deleted: 2
% 6.59/6.79 % Forward subsumed : 368
% 6.59/6.79 % Backward subsumed : 3
% 6.59/6.79 % -------- CPU Time ---------
% 6.59/6.79 % User time : 6.406 s
% 6.59/6.79 % System time : 0.037 s
% 6.59/6.79 % Total time : 6.443 s
%------------------------------------------------------------------------------