%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : GRP189-1 : TPTP v8.1.2. Bugfixed v1.2.1.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n003.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:26 EDT 2024
% Result : Unsatisfiable 88.77s 88.93s
% Output : Refutation 88.77s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 8
% Syntax : Number of clauses : 19 ( 12 unt; 0 nHn; 8 RR)
% Number of literals : 28 ( 27 equ; 10 neg)
% Maximal clause size : 3 ( 1 avg)
% Maximal term depth : 3 ( 1 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 : 41 ( 8 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(prove_p38b,negated_conjecture,
greatest_lower_bound(b,least_upper_bound(a,b)) != b,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_p38b) ).
cnf(symmetry,axiom,
( X7 != X6
| X6 = X7 ),
theory(equality) ).
cnf(symmetry_of_glb,axiom,
greatest_lower_bound(X20,X19) = greatest_lower_bound(X19,X20),
file('/export/starexec/sandbox/benchmark/Axioms/GRP004-2.ax',symmetry_of_glb) ).
cnf(transitivity,axiom,
( X49 != X48
| X48 != X47
| X49 = X47 ),
theory(equality) ).
cnf(c40,plain,
( X253 != greatest_lower_bound(X255,X254)
| X253 = greatest_lower_bound(X254,X255) ),
inference(resolution,[status(thm)],[transitivity,symmetry_of_glb]) ).
cnf(glb_absorbtion,axiom,
greatest_lower_bound(X29,least_upper_bound(X29,X28)) = X29,
file('/export/starexec/sandbox/benchmark/Axioms/GRP004-2.ax',glb_absorbtion) ).
cnf(c39,plain,
( X242 != greatest_lower_bound(X241,least_upper_bound(X241,X243))
| X242 = X241 ),
inference(resolution,[status(thm)],[transitivity,glb_absorbtion]) ).
cnf(c879,plain,
greatest_lower_bound(least_upper_bound(X248,X247),X248) = X248,
inference(resolution,[status(thm)],[c39,symmetry_of_glb]) ).
cnf(c898,plain,
( X1729 != greatest_lower_bound(least_upper_bound(X1730,X1731),X1730)
| X1729 = X1730 ),
inference(resolution,[status(thm)],[c879,transitivity]) ).
cnf(symmetry_of_lub,axiom,
least_upper_bound(X22,X21) = least_upper_bound(X21,X22),
file('/export/starexec/sandbox/benchmark/Axioms/GRP004-2.ax',symmetry_of_lub) ).
cnf(reflexivity,axiom,
X2 = X2,
theory(equality) ).
cnf(c2,axiom,
( X109 != X108
| X111 != X110
| greatest_lower_bound(X109,X111) = greatest_lower_bound(X108,X110) ),
theory(equality) ).
cnf(c238,plain,
( X634 != X633
| greatest_lower_bound(X634,X632) = greatest_lower_bound(X633,X632) ),
inference(resolution,[status(thm)],[c2,reflexivity]) ).
cnf(c3149,plain,
greatest_lower_bound(least_upper_bound(X4497,X4498),X4496) = greatest_lower_bound(least_upper_bound(X4498,X4497),X4496),
inference(resolution,[status(thm)],[c238,symmetry_of_lub]) ).
cnf(c160192,plain,
greatest_lower_bound(least_upper_bound(X4501,X4502),X4502) = X4502,
inference(resolution,[status(thm)],[c3149,c898]) ).
cnf(c160570,plain,
X4503 = greatest_lower_bound(least_upper_bound(X4504,X4503),X4503),
inference(resolution,[status(thm)],[c160192,symmetry]) ).
cnf(c160904,plain,
X4509 = greatest_lower_bound(X4509,least_upper_bound(X4508,X4509)),
inference(resolution,[status(thm)],[c160570,c40]) ).
cnf(c160970,plain,
greatest_lower_bound(X4514,least_upper_bound(X4513,X4514)) = X4514,
inference(resolution,[status(thm)],[c160904,symmetry]) ).
cnf(c161438,plain,
$false,
inference(resolution,[status(thm)],[c160970,prove_p38b]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.13 % Problem : GRP189-1 : TPTP v8.1.2. Bugfixed v1.2.1.
% 0.07/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.15/0.35 % Computer : n003.cluster.edu
% 0.15/0.35 % Model : x86_64 x86_64
% 0.15/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.35 % Memory : 8042.1875MB
% 0.15/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.35 % CPULimit : 300
% 0.15/0.35 % WCLimit : 300
% 0.15/0.35 % DateTime : Thu May 9 04:47:53 EDT 2024
% 0.15/0.36 % CPUTime :
% 88.77/88.93 % Version: 1.5
% 88.77/88.93 % SZS status Unsatisfiable
% 88.77/88.93 % SZS output start CNFRefutation
% See solution above
% 88.77/88.93
% 88.77/88.93 % Initial clauses : 23
% 88.77/88.93 % Processed clauses : 1069
% 88.77/88.93 % Factors computed : 4
% 88.77/88.93 % Resolvents computed: 161516
% 88.77/88.93 % Tautologies deleted: 2
% 88.77/88.93 % Forward subsumed : 1805
% 88.77/88.93 % Backward subsumed : 11
% 88.77/88.93 % -------- CPU Time ---------
% 88.77/88.93 % User time : 88.226 s
% 88.77/88.93 % System time : 0.341 s
% 88.77/88.93 % Total time : 88.567 s
%------------------------------------------------------------------------------