%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : GRP010-4 : TPTP v8.1.2. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n029.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:45 EDT 2024
% Result : Unsatisfiable 86.12s 86.40s
% Output : Refutation 86.12s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 9
% Syntax : Number of clauses : 36 ( 24 unt; 0 nHn; 17 RR)
% Number of literals : 50 ( 49 equ; 15 neg)
% Maximal clause size : 3 ( 1 avg)
% Maximal term depth : 4 ( 1 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 : 63 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(prove_b_times_c_is_e,negated_conjecture,
multiply(b,c) != identity,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_b_times_c_is_e) ).
cnf(transitivity,axiom,
( X15 != X16
| X16 != X14
| X15 = X14 ),
theory(equality) ).
cnf(left_inverse,axiom,
multiply(inverse(X12),X12) = identity,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',left_inverse) ).
cnf(c11,plain,
( X42 != multiply(inverse(X41),X41)
| X42 = identity ),
inference(resolution,[status(thm)],[transitivity,left_inverse]) ).
cnf(symmetry,axiom,
( X4 != X5
| X5 = X4 ),
theory(equality) ).
cnf(reflexivity,axiom,
X2 = X2,
theory(equality) ).
cnf(left_identity,axiom,
multiply(identity,X3) = X3,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',left_identity) ).
cnf(c2,plain,
X7 = multiply(identity,X7),
inference(resolution,[status(thm)],[symmetry,left_identity]) ).
cnf(c0,axiom,
( X22 != X24
| X23 != X21
| multiply(X22,X23) = multiply(X24,X21) ),
theory(equality) ).
cnf(c22,plain,
( X84 != X86
| multiply(X84,X85) = multiply(X86,multiply(identity,X85)) ),
inference(resolution,[status(thm)],[c0,c2]) ).
cnf(c258,plain,
multiply(X129,X128) = multiply(X129,multiply(identity,X128)),
inference(resolution,[status(thm)],[c22,reflexivity]) ).
cnf(associativity,axiom,
multiply(multiply(X9,X10),X8) = multiply(X9,multiply(X10,X8)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',associativity) ).
cnf(c5,plain,
multiply(X34,multiply(X33,X32)) = multiply(multiply(X34,X33),X32),
inference(resolution,[status(thm)],[associativity,symmetry]) ).
cnf(c42,plain,
( X145 != multiply(X144,multiply(X143,X142))
| X145 = multiply(multiply(X144,X143),X142) ),
inference(resolution,[status(thm)],[c5,transitivity]) ).
cnf(c632,plain,
multiply(X171,X172) = multiply(multiply(X171,identity),X172),
inference(resolution,[status(thm)],[c42,c258]) ).
cnf(c787,plain,
multiply(multiply(X185,identity),X184) = multiply(X185,X184),
inference(resolution,[status(thm)],[c632,symmetry]) ).
cnf(c913,plain,
multiply(multiply(inverse(X194),identity),X194) = identity,
inference(resolution,[status(thm)],[c787,c11]) ).
cnf(c986,plain,
( X1705 != multiply(multiply(inverse(X1704),identity),X1704)
| X1705 = identity ),
inference(resolution,[status(thm)],[c913,transitivity]) ).
cnf(c25,plain,
( X63 != X65
| multiply(X63,X64) = multiply(X65,X64) ),
inference(resolution,[status(thm)],[c0,reflexivity]) ).
cnf(c_times_b_is_e,plain,
multiply(c,b) = identity,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c_times_b_is_e) ).
cnf(c7,plain,
identity = multiply(c,b),
inference(resolution,[status(thm)],[c_times_b_is_e,symmetry]) ).
cnf(c27,plain,
( X111 != X112
| multiply(X111,identity) = multiply(X112,multiply(c,b)) ),
inference(resolution,[status(thm)],[c0,c7]) ).
cnf(c496,plain,
multiply(X310,identity) = multiply(X310,multiply(c,b)),
inference(resolution,[status(thm)],[c27,reflexivity]) ).
cnf(c14,plain,
( X54 != multiply(multiply(X53,X52),X51)
| X54 = multiply(X53,multiply(X52,X51)) ),
inference(resolution,[status(thm)],[transitivity,associativity]) ).
cnf(c10,plain,
( X29 != multiply(identity,X28)
| X29 = X28 ),
inference(resolution,[status(thm)],[transitivity,left_identity]) ).
cnf(c114,plain,
multiply(multiply(inverse(X245),X245),X246) = multiply(identity,X246),
inference(resolution,[status(thm)],[c25,left_inverse]) ).
cnf(c1463,plain,
multiply(multiply(inverse(X248),X248),X247) = X247,
inference(resolution,[status(thm)],[c114,c10]) ).
cnf(c1495,plain,
X249 = multiply(multiply(inverse(X250),X250),X249),
inference(resolution,[status(thm)],[c1463,symmetry]) ).
cnf(c1509,plain,
X251 = multiply(inverse(X252),multiply(X252,X251)),
inference(resolution,[status(thm)],[c1495,c14]) ).
cnf(c1541,plain,
multiply(inverse(X255),multiply(X255,X256)) = X256,
inference(resolution,[status(thm)],[c1509,symmetry]) ).
cnf(c1594,plain,
( X489 != multiply(inverse(X487),multiply(X487,X488))
| X489 = X488 ),
inference(resolution,[status(thm)],[c1541,transitivity]) ).
cnf(c4104,plain,
multiply(inverse(c),identity) = b,
inference(resolution,[status(thm)],[c1594,c496]) ).
cnf(c4302,plain,
b = multiply(inverse(c),identity),
inference(resolution,[status(thm)],[c4104,symmetry]) ).
cnf(c4372,plain,
multiply(b,X3612) = multiply(multiply(inverse(c),identity),X3612),
inference(resolution,[status(thm)],[c4302,c25]) ).
cnf(c92036,plain,
multiply(b,c) = identity,
inference(resolution,[status(thm)],[c4372,c986]) ).
cnf(c92072,plain,
$false,
inference(resolution,[status(thm)],[c92036,prove_b_times_c_is_e]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.13 % Problem : GRP010-4 : TPTP v8.1.2. Released v1.0.0.
% 0.08/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.36 % Computer : n029.cluster.edu
% 0.14/0.36 % Model : x86_64 x86_64
% 0.14/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.36 % Memory : 8042.1875MB
% 0.14/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.36 % CPULimit : 300
% 0.14/0.36 % WCLimit : 300
% 0.14/0.36 % DateTime : Thu May 9 03:35:23 EDT 2024
% 0.14/0.36 % CPUTime :
% 86.12/86.40 % Version: 1.5
% 86.12/86.40 % SZS status Unsatisfiable
% 86.12/86.40 % SZS output start CNFRefutation
% See solution above
% 86.12/86.40
% 86.12/86.40 % Initial clauses : 10
% 86.12/86.40 % Processed clauses : 1271
% 86.12/86.40 % Factors computed : 2
% 86.12/86.40 % Resolvents computed: 92222
% 86.12/86.40 % Tautologies deleted: 2
% 86.12/86.40 % Forward subsumed : 2219
% 86.12/86.40 % Backward subsumed : 6
% 86.12/86.40 % -------- CPU Time ---------
% 86.12/86.40 % User time : 85.758 s
% 86.12/86.40 % System time : 0.258 s
% 86.12/86.40 % Total time : 86.016 s
%------------------------------------------------------------------------------