%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : GRP188-2 : TPTP v8.1.2. Bugfixed v1.2.1.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n023.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 7.70s 7.87s
% Output : Refutation 7.70s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 8
% Syntax : Number of clauses : 19 ( 13 unt; 0 nHn; 7 RR)
% Number of literals : 27 ( 26 equ; 9 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 : 3 ( 3 usr; 2 con; 0-2 aty)
% Number of variables : 39 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(prove_p38a,negated_conjecture,
least_upper_bound(b,least_upper_bound(a,b)) != least_upper_bound(a,b),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_p38a) ).
cnf(symmetry_of_lub,axiom,
least_upper_bound(X25,X24) = least_upper_bound(X24,X25),
file('/export/starexec/sandbox2/benchmark/Axioms/GRP004-2.ax',symmetry_of_lub) ).
cnf(transitivity,axiom,
( X52 != X51
| X51 != X50
| X52 = X50 ),
theory(equality) ).
cnf(c47,plain,
( X254 != least_upper_bound(X256,X255)
| X254 = least_upper_bound(X255,X256) ),
inference(resolution,[status(thm)],[transitivity,symmetry_of_lub]) ).
cnf(symmetry,axiom,
( X9 != X8
| X8 = X9 ),
theory(equality) ).
cnf(associativity_of_lub,axiom,
least_upper_bound(X42,least_upper_bound(X41,X40)) = least_upper_bound(least_upper_bound(X42,X41),X40),
file('/export/starexec/sandbox2/benchmark/Axioms/GRP004-2.ax',associativity_of_lub) ).
cnf(c44,plain,
( X249 != least_upper_bound(X250,least_upper_bound(X251,X252))
| X249 = least_upper_bound(least_upper_bound(X250,X251),X252) ),
inference(resolution,[status(thm)],[transitivity,associativity_of_lub]) ).
cnf(idempotence_of_lub,axiom,
least_upper_bound(X3,X3) = X3,
file('/export/starexec/sandbox2/benchmark/Axioms/GRP004-2.ax',idempotence_of_lub) ).
cnf(c4,plain,
X11 = least_upper_bound(X11,X11),
inference(resolution,[status(thm)],[symmetry,idempotence_of_lub]) ).
cnf(reflexivity,axiom,
X2 = X2,
theory(equality) ).
cnf(c3,axiom,
( X129 != X127
| X130 != X128
| least_upper_bound(X129,X130) = least_upper_bound(X127,X128) ),
theory(equality) ).
cnf(c408,plain,
( X1266 != X1267
| least_upper_bound(X1266,X1265) = least_upper_bound(X1267,X1265) ),
inference(resolution,[status(thm)],[c3,reflexivity]) ).
cnf(c17065,plain,
least_upper_bound(X1279,X1278) = least_upper_bound(least_upper_bound(X1279,X1279),X1278),
inference(resolution,[status(thm)],[c408,c4]) ).
cnf(c17486,plain,
least_upper_bound(X1311,X1310) = least_upper_bound(X1310,least_upper_bound(X1311,X1311)),
inference(resolution,[status(thm)],[c17065,c47]) ).
cnf(c18507,plain,
least_upper_bound(X1375,X1376) = least_upper_bound(least_upper_bound(X1376,X1375),X1375),
inference(resolution,[status(thm)],[c17486,c44]) ).
cnf(c20190,plain,
least_upper_bound(X1433,X1432) = least_upper_bound(X1433,least_upper_bound(X1432,X1433)),
inference(resolution,[status(thm)],[c18507,c47]) ).
cnf(c21240,plain,
least_upper_bound(X1501,least_upper_bound(X1500,X1501)) = least_upper_bound(X1501,X1500),
inference(resolution,[status(thm)],[c20190,symmetry]) ).
cnf(c22235,plain,
least_upper_bound(X1584,least_upper_bound(X1583,X1584)) = least_upper_bound(X1583,X1584),
inference(resolution,[status(thm)],[c21240,c47]) ).
cnf(c23875,plain,
$false,
inference(resolution,[status(thm)],[c22235,prove_p38a]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : GRP188-2 : TPTP v8.1.2. Bugfixed v1.2.1.
% 0.07/0.12 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.12/0.33 % Computer : n023.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Thu May 9 03:30:53 EDT 2024
% 0.12/0.33 % CPUTime :
% 7.70/7.87 % Version: 1.5
% 7.70/7.87 % SZS status Unsatisfiable
% 7.70/7.87 % SZS output start CNFRefutation
% See solution above
% 7.70/7.87
% 7.70/7.87 % Initial clauses : 26
% 7.70/7.87 % Processed clauses : 455
% 7.70/7.87 % Factors computed : 4
% 7.70/7.87 % Resolvents computed: 23877
% 7.70/7.87 % Tautologies deleted: 2
% 7.70/7.87 % Forward subsumed : 627
% 7.70/7.87 % Backward subsumed : 6
% 7.70/7.87 % -------- CPU Time ---------
% 7.70/7.87 % User time : 7.490 s
% 7.70/7.87 % System time : 0.043 s
% 7.70/7.87 % Total time : 7.533 s
%------------------------------------------------------------------------------