%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : GRP001-4 : TPTP v8.1.2. Released v1.0.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:22:43 EDT 2024
% Result : Unsatisfiable 25.64s 25.83s
% Output : Refutation 25.64s
% Verified :
% SZS Type : Refutation
% Derivation depth : 23
% Number of leaves : 9
% Syntax : Number of clauses : 45 ( 31 unt; 0 nHn; 15 RR)
% Number of literals : 61 ( 60 equ; 17 neg)
% Maximal clause size : 3 ( 1 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 5 ( 5 usr; 4 con; 0-2 aty)
% Number of variables : 93 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(prove_b_times_a_is_c,negated_conjecture,
multiply(b,a) != c,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_b_times_a_is_c) ).
cnf(a_times_b_is_c,plain,
multiply(a,b) = c,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',a_times_b_is_c) ).
cnf(transitivity,axiom,
( X15 != X16
| X16 != X17
| X15 = X17 ),
theory(equality) ).
cnf(c11,plain,
( X49 != multiply(a,b)
| X49 = c ),
inference(resolution,[status(thm)],[transitivity,a_times_b_is_c]) ).
cnf(symmetry,axiom,
( X5 != X6
| X6 = X5 ),
theory(equality) ).
cnf(associativity,axiom,
multiply(multiply(X8,X9),X10) = multiply(X8,multiply(X9,X10)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',associativity) ).
cnf(c4,plain,
multiply(X31,multiply(X30,X32)) = multiply(multiply(X31,X30),X32),
inference(resolution,[status(thm)],[associativity,symmetry]) ).
cnf(c40,plain,
( X135 != multiply(X137,multiply(X134,X136))
| X135 = multiply(multiply(X137,X134),X136) ),
inference(resolution,[status(thm)],[c4,transitivity]) ).
cnf(left_identity,axiom,
multiply(identity,X3) = X3,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',left_identity) ).
cnf(c16,plain,
( X34 != multiply(identity,X35)
| X34 = X35 ),
inference(resolution,[status(thm)],[transitivity,left_identity]) ).
cnf(reflexivity,axiom,
X2 = X2,
theory(equality) ).
cnf(squareness,plain,
multiply(X4,X4) = identity,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',squareness) ).
cnf(c0,axiom,
( X22 != X23
| X21 != X24
| multiply(X22,X21) = multiply(X23,X24) ),
theory(equality) ).
cnf(c24,plain,
( X101 != X100
| multiply(X101,multiply(X99,X99)) = multiply(X100,identity) ),
inference(resolution,[status(thm)],[c0,squareness]) ).
cnf(c282,plain,
multiply(X211,multiply(X212,X212)) = multiply(X211,identity),
inference(resolution,[status(thm)],[c24,reflexivity]) ).
cnf(c2,plain,
identity = multiply(X11,X11),
inference(resolution,[status(thm)],[symmetry,squareness]) ).
cnf(c26,plain,
( X121 != X120
| multiply(X121,identity) = multiply(X120,multiply(X119,X119)) ),
inference(resolution,[status(thm)],[c0,c2]) ).
cnf(c379,plain,
multiply(X236,identity) = multiply(X236,multiply(X237,X237)),
inference(resolution,[status(thm)],[c26,reflexivity]) ).
cnf(c10,plain,
( X38 != multiply(multiply(X40,X41),X39)
| X38 = multiply(X40,multiply(X41,X39)) ),
inference(resolution,[status(thm)],[transitivity,associativity]) ).
cnf(c21,plain,
( X75 != X74
| multiply(X75,X73) = multiply(X74,X73) ),
inference(resolution,[status(thm)],[c0,reflexivity]) ).
cnf(c121,plain,
multiply(multiply(X153,X153),X152) = multiply(identity,X152),
inference(resolution,[status(thm)],[c21,squareness]) ).
cnf(c558,plain,
multiply(multiply(X154,X154),X155) = X155,
inference(resolution,[status(thm)],[c121,c16]) ).
cnf(c574,plain,
X159 = multiply(multiply(X160,X160),X159),
inference(resolution,[status(thm)],[c558,symmetry]) ).
cnf(c604,plain,
X167 = multiply(X166,multiply(X166,X167)),
inference(resolution,[status(thm)],[c574,c10]) ).
cnf(c609,plain,
multiply(X172,multiply(X172,X173)) = X173,
inference(resolution,[status(thm)],[c604,symmetry]) ).
cnf(c637,plain,
( X357 != multiply(X358,multiply(X358,X359))
| X357 = X359 ),
inference(resolution,[status(thm)],[c609,transitivity]) ).
cnf(c1646,plain,
multiply(X363,identity) = X363,
inference(resolution,[status(thm)],[c637,c379]) ).
cnf(c1701,plain,
( X391 != multiply(X392,identity)
| X391 = X392 ),
inference(resolution,[status(thm)],[c1646,transitivity]) ).
cnf(c1824,plain,
multiply(X404,multiply(X405,X405)) = X404,
inference(resolution,[status(thm)],[c1701,c282]) ).
cnf(c1902,plain,
X406 = multiply(X406,multiply(X407,X407)),
inference(resolution,[status(thm)],[c1824,symmetry]) ).
cnf(c1946,plain,
X426 = multiply(multiply(X426,X425),X425),
inference(resolution,[status(thm)],[c1902,c40]) ).
cnf(c2010,plain,
multiply(multiply(X436,X435),X435) = X436,
inference(resolution,[status(thm)],[c1946,symmetry]) ).
cnf(c2052,plain,
( X924 != multiply(multiply(X925,X923),X923)
| X924 = X925 ),
inference(resolution,[status(thm)],[c2010,transitivity]) ).
cnf(c54,plain,
identity = multiply(X103,multiply(X102,multiply(X103,X102))),
inference(resolution,[status(thm)],[c10,c2]) ).
cnf(c289,plain,
multiply(identity,X1891) = multiply(multiply(X1892,multiply(X1893,multiply(X1892,X1893))),X1891),
inference(resolution,[status(thm)],[c54,c21]) ).
cnf(c13222,plain,
multiply(identity,multiply(X2117,multiply(X2118,X2117))) = X2118,
inference(resolution,[status(thm)],[c289,c2052]) ).
cnf(c16419,plain,
X2228 = multiply(identity,multiply(X2229,multiply(X2228,X2229))),
inference(resolution,[status(thm)],[c13222,symmetry]) ).
cnf(c17996,plain,
X2233 = multiply(X2234,multiply(X2233,X2234)),
inference(resolution,[status(thm)],[c16419,c16]) ).
cnf(c18099,plain,
X2243 = multiply(multiply(X2242,X2243),X2242),
inference(resolution,[status(thm)],[c17996,c40]) ).
cnf(c18235,plain,
multiply(multiply(X2254,X2255),X2254) = X2255,
inference(resolution,[status(thm)],[c18099,symmetry]) ).
cnf(c18259,plain,
( X2492 != multiply(multiply(X2493,X2494),X2493)
| X2492 = X2494 ),
inference(resolution,[status(thm)],[c18235,transitivity]) ).
cnf(c607,plain,
multiply(X3529,X3530) = multiply(multiply(X3528,multiply(X3528,X3529)),X3530),
inference(resolution,[status(thm)],[c604,c21]) ).
cnf(c34724,plain,
multiply(X3532,X3531) = multiply(X3531,X3532),
inference(resolution,[status(thm)],[c607,c18259]) ).
cnf(c34825,plain,
multiply(b,a) = c,
inference(resolution,[status(thm)],[c34724,c11]) ).
cnf(c35025,plain,
$false,
inference(resolution,[status(thm)],[c34825,prove_b_times_a_is_c]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.13 % Problem : GRP001-4 : TPTP v8.1.2. Released v1.0.0.
% 0.07/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 04:39:22 EDT 2024
% 0.15/0.36 % CPUTime :
% 25.64/25.83 % Version: 1.5
% 25.64/25.83 % SZS status Unsatisfiable
% 25.64/25.83 % SZS output start CNFRefutation
% See solution above
% 25.64/25.83
% 25.64/25.83 % Initial clauses : 9
% 25.64/25.83 % Processed clauses : 721
% 25.64/25.83 % Factors computed : 2
% 25.64/25.83 % Resolvents computed: 35051
% 25.64/25.83 % Tautologies deleted: 2
% 25.64/25.83 % Forward subsumed : 1770
% 25.64/25.83 % Backward subsumed : 41
% 25.64/25.83 % -------- CPU Time ---------
% 25.64/25.83 % User time : 25.369 s
% 25.64/25.83 % System time : 0.095 s
% 25.64/25.83 % Total time : 25.464 s
%------------------------------------------------------------------------------