%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : CAT019-3 : 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:17:04 EDT 2024
% Result : Unsatisfiable 3.55s 3.81s
% Output : Refutation 3.55s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 8
% Syntax : Number of clauses : 18 ( 8 unt; 4 nHn; 15 RR)
% Number of literals : 34 ( 22 equ; 11 neg)
% Maximal clause size : 4 ( 1 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 3 ( 3 usr; 2 con; 0-2 aty)
% Number of variables : 12 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(prove_a_equals_b,negated_conjecture,
a != b,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_a_equals_b) ).
cnf(reflexivity,axiom,
X2 = X2,
theory(equality) ).
cnf(equality_of_a_and_b2,plain,
( ~ there_exists(X74)
| a = X74
| b != X74 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',equality_of_a_and_b2) ).
cnf(c122,plain,
( ~ there_exists(b)
| a = b ),
inference(resolution,[status(thm)],[equality_of_a_and_b2,reflexivity]) ).
cnf(indiscernibles1,axiom,
( there_exists(f1(X27,X28))
| X27 = X28 ),
file('/export/starexec/sandbox/benchmark/Axioms/CAT003-0.ax',indiscernibles1) ).
cnf(c18,plain,
there_exists(f1(a,b)),
inference(resolution,[status(thm)],[indiscernibles1,prove_a_equals_b]) ).
cnf(c5,axiom,
( X29 != X30
| ~ there_exists(X29)
| there_exists(X30) ),
theory(equality) ).
cnf(symmetry,axiom,
( X14 != X15
| X15 = X14 ),
theory(equality) ).
cnf(indiscernibles2,axiom,
( X61 = f1(X61,X62)
| X62 = f1(X61,X62)
| X61 = X62 ),
file('/export/starexec/sandbox/benchmark/Axioms/CAT003-0.ax',indiscernibles2) ).
cnf(equality_of_a_and_b1,plain,
( ~ there_exists(X73)
| a != X73
| b = X73 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',equality_of_a_and_b1) ).
cnf(c115,plain,
( ~ there_exists(f1(a,X564))
| b = f1(a,X564)
| X564 = f1(a,X564)
| a = X564 ),
inference(resolution,[status(thm)],[equality_of_a_and_b1,indiscernibles2]) ).
cnf(c6160,plain,
( b = f1(a,b)
| a = b ),
inference(resolution,[status(thm)],[c115,c18]) ).
cnf(c14443,plain,
b = f1(a,b),
inference(resolution,[status(thm)],[c6160,prove_a_equals_b]) ).
cnf(c14460,plain,
f1(a,b) = b,
inference(resolution,[status(thm)],[c14443,symmetry]) ).
cnf(c14485,plain,
( ~ there_exists(f1(a,b))
| there_exists(b) ),
inference(resolution,[status(thm)],[c14460,c5]) ).
cnf(c14554,plain,
there_exists(b),
inference(resolution,[status(thm)],[c14485,c18]) ).
cnf(c14657,plain,
a = b,
inference(resolution,[status(thm)],[c14554,c122]) ).
cnf(c14808,plain,
$false,
inference(resolution,[status(thm)],[c14657,prove_a_equals_b]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.14 % Problem : CAT019-3 : TPTP v8.1.2. Released v1.0.0.
% 0.08/0.15 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.15/0.37 % Computer : n021.cluster.edu
% 0.15/0.37 % Model : x86_64 x86_64
% 0.15/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.37 % Memory : 8042.1875MB
% 0.15/0.37 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.37 % CPULimit : 300
% 0.15/0.37 % WCLimit : 300
% 0.15/0.37 % DateTime : Wed May 8 21:01:53 EDT 2024
% 0.15/0.37 % CPUTime :
% 3.55/3.81 % Version: 1.5
% 3.55/3.81 % SZS status Unsatisfiable
% 3.55/3.81 % SZS output start CNFRefutation
% See solution above
% 3.55/3.81
% 3.55/3.81 % Initial clauses : 29
% 3.55/3.81 % Processed clauses : 341
% 3.55/3.81 % Factors computed : 13
% 3.55/3.81 % Resolvents computed: 14795
% 3.55/3.81 % Tautologies deleted: 5
% 3.55/3.81 % Forward subsumed : 227
% 3.55/3.81 % Backward subsumed : 4
% 3.55/3.81 % -------- CPU Time ---------
% 3.55/3.81 % User time : 3.399 s
% 3.55/3.81 % System time : 0.035 s
% 3.55/3.81 % Total time : 3.434 s
%------------------------------------------------------------------------------