%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : COL099-1 : TPTP v8.1.2. Released v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n019.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:31 EDT 2024
% Result : Unsatisfiable 0.59s 0.77s
% Output : Refutation 0.59s
% Verified :
% SZS Type : Refutation
% Derivation depth : 6
% Number of leaves : 7
% Syntax : Number of clauses : 16 ( 8 unt; 0 nHn; 16 RR)
% Number of literals : 30 ( 0 equ; 16 neg)
% Maximal clause size : 4 ( 1 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 3 ( 2 usr; 1 prp; 0-2 aty)
% Number of functors : 7 ( 7 usr; 4 con; 0-4 aty)
% Number of variables : 14 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(diamond_trancl_1h1,plain,
diamond(r),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',diamond_trancl_1h1) ).
cnf(diamond_trancl_1h2,plain,
member(pair(y,ya),r),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',diamond_trancl_1h2) ).
cnf(diamond_trancl_1c1,negated_conjecture,
member(pair(y,yp),trancl(r)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',diamond_trancl_1c1) ).
cnf(diamond_strip_lemmaD1,axiom,
( ~ diamond(X60)
| ~ member(pair(X59,X61),trancl(X60))
| ~ member(pair(X59,X62),X60)
| member(pair(X62,diamond_strip_lemmaD_sk1(X59,X61,X62,X60)),trancl(X60)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',diamond_strip_lemmaD1) ).
cnf(c38,plain,
( ~ diamond(r)
| ~ member(pair(y,X133),r)
| member(pair(X133,diamond_strip_lemmaD_sk1(y,yp,X133,r)),trancl(r)) ),
inference(resolution,[status(thm)],[diamond_strip_lemmaD1,diamond_trancl_1c1]) ).
cnf(c122,plain,
( ~ diamond(r)
| member(pair(ya,diamond_strip_lemmaD_sk1(y,yp,ya,r)),trancl(r)) ),
inference(resolution,[status(thm)],[c38,diamond_trancl_1h2]) ).
cnf(c137,plain,
member(pair(ya,diamond_strip_lemmaD_sk1(y,yp,ya,r)),trancl(r)),
inference(resolution,[status(thm)],[c122,diamond_trancl_1h1]) ).
cnf(diamond_trancl_1c2,negated_conjecture,
( ~ member(pair(ya,X88),trancl(r))
| ~ member(pair(yp,X88),trancl(r)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',diamond_trancl_1c2) ).
cnf(r_into_trancl,axiom,
( ~ member(pair(X50,X48),X49)
| member(pair(X50,X48),trancl(X49)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',r_into_trancl) ).
cnf(diamond_strip_lemmaD2,axiom,
( ~ diamond(X76)
| ~ member(pair(X75,X77),trancl(X76))
| ~ member(pair(X75,X78),X76)
| member(pair(X77,diamond_strip_lemmaD_sk1(X75,X77,X78,X76)),X76) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',diamond_strip_lemmaD2) ).
cnf(c50,plain,
( ~ diamond(r)
| ~ member(pair(y,X223),r)
| member(pair(yp,diamond_strip_lemmaD_sk1(y,yp,X223,r)),r) ),
inference(resolution,[status(thm)],[diamond_strip_lemmaD2,diamond_trancl_1c1]) ).
cnf(c187,plain,
( ~ diamond(r)
| member(pair(yp,diamond_strip_lemmaD_sk1(y,yp,ya,r)),r) ),
inference(resolution,[status(thm)],[c50,diamond_trancl_1h2]) ).
cnf(c188,plain,
member(pair(yp,diamond_strip_lemmaD_sk1(y,yp,ya,r)),r),
inference(resolution,[status(thm)],[c187,diamond_trancl_1h1]) ).
cnf(c190,plain,
member(pair(yp,diamond_strip_lemmaD_sk1(y,yp,ya,r)),trancl(r)),
inference(resolution,[status(thm)],[c188,r_into_trancl]) ).
cnf(c196,plain,
~ member(pair(ya,diamond_strip_lemmaD_sk1(y,yp,ya,r)),trancl(r)),
inference(resolution,[status(thm)],[c190,diamond_trancl_1c2]) ).
cnf(c198,plain,
$false,
inference(resolution,[status(thm)],[c196,c137]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.13 % Problem : COL099-1 : TPTP v8.1.2. Released v2.7.0.
% 0.08/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.35 % Computer : n019.cluster.edu
% 0.13/0.35 % Model : x86_64 x86_64
% 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.35 % Memory : 8042.1875MB
% 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.35 % CPULimit : 300
% 0.13/0.35 % WCLimit : 300
% 0.13/0.35 % DateTime : Wed May 8 21:41:53 EDT 2024
% 0.13/0.36 % CPUTime :
% 0.59/0.77 % Version: 1.5
% 0.59/0.77 % SZS status Unsatisfiable
% 0.59/0.77 % SZS output start CNFRefutation
% See solution above
% 0.59/0.77
% 0.59/0.77 % Initial clauses : 25
% 0.59/0.77 % Processed clauses : 101
% 0.59/0.77 % Factors computed : 17
% 0.59/0.77 % Resolvents computed: 175
% 0.59/0.77 % Tautologies deleted: 5
% 0.59/0.77 % Forward subsumed : 30
% 0.59/0.77 % Backward subsumed : 5
% 0.59/0.77 % -------- CPU Time ---------
% 0.59/0.77 % User time : 0.391 s
% 0.59/0.77 % System time : 0.017 s
% 0.59/0.77 % Total time : 0.408 s
%------------------------------------------------------------------------------