%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SYO691-1.000 : TPTP v8.1.2. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n012.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:51:10 EDT 2024
% Result : Unsatisfiable 0.41s 0.59s
% Output : Refutation 0.41s
% Verified :
% SZS Type : Refutation
% Derivation depth : 7
% Number of leaves : 6
% Syntax : Number of clauses : 16 ( 10 unt; 0 nHn; 7 RR)
% Number of literals : 23 ( 0 equ; 8 neg)
% Maximal clause size : 3 ( 1 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 4 ( 3 usr; 1 prp; 0-3 aty)
% Number of functors : 4 ( 4 usr; 2 con; 0-2 aty)
% Number of variables : 49 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(prove,negated_conjecture,
~ seq(succ(succ(succ(zero))),X5,X5),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove) ).
cnf(rewrite_left,axiom,
( ~ step(X6,X8)
| step(f(X6,X7),f(X8,X7)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rewrite_left) ).
cnf(rewrite_top,axiom,
( ~ top(X3,X4)
| step(X3,X4) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rewrite_top) ).
cnf(rule_1,axiom,
top(f(f(X13,X14),f(X12,a)),f(f(X12,f(X14,a)),X13)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rule_1) ).
cnf(c0,plain,
step(f(f(X21,X23),f(X22,a)),f(f(X22,f(X23,a)),X21)),
inference(resolution,[status(thm)],[rule_1,rewrite_top]) ).
cnf(c3,plain,
step(f(f(f(X28,X27),f(X30,a)),X29),f(f(f(X30,f(X27,a)),X28),X29)),
inference(resolution,[status(thm)],[c0,rewrite_left]) ).
cnf(c7,plain,
step(f(f(f(f(X50,X47),f(X51,a)),X48),X49),f(f(f(f(X51,f(X47,a)),X50),X48),X49)),
inference(resolution,[status(thm)],[c3,rewrite_left]) ).
cnf(rewrite_sequence_succ,axiom,
( ~ seq(X16,X15,X18)
| ~ step(X18,X17)
| seq(succ(X16),X15,X17) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rewrite_sequence_succ) ).
cnf(rewrite_sequence_zero,axiom,
seq(zero,X2,X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rewrite_sequence_zero) ).
cnf(c1,plain,
( ~ step(X19,X20)
| seq(succ(zero),X19,X20) ),
inference(resolution,[status(thm)],[rewrite_sequence_succ,rewrite_sequence_zero]) ).
cnf(c2,plain,
seq(succ(zero),f(f(X25,X24),f(X26,a)),f(f(X26,f(X24,a)),X25)),
inference(resolution,[status(thm)],[c0,c1]) ).
cnf(c5,plain,
( ~ step(f(f(X36,f(X35,a)),X37),X38)
| seq(succ(succ(zero)),f(f(X37,X35),f(X36,a)),X38) ),
inference(resolution,[status(thm)],[c2,rewrite_sequence_succ]) ).
cnf(c13,plain,
seq(succ(succ(zero)),f(f(X67,X70),f(f(X69,X68),a)),f(f(f(X70,f(X68,a)),X69),X67)),
inference(resolution,[status(thm)],[c5,c3]) ).
cnf(c32,plain,
( ~ step(f(f(f(X172,f(X171,a)),X168),X170),X169)
| seq(succ(succ(succ(zero))),f(f(X170,X172),f(f(X168,X171),a)),X169) ),
inference(resolution,[status(thm)],[c13,rewrite_sequence_succ]) ).
cnf(c113,plain,
seq(succ(succ(succ(zero))),f(f(X216,f(X215,X217)),f(f(X218,X219),a)),f(f(f(f(X219,f(X217,a)),X215),X218),X216)),
inference(resolution,[status(thm)],[c32,c7]) ).
cnf(c134,plain,
$false,
inference(resolution,[status(thm)],[c113,prove]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.12 % Problem : SYO691-1.000 : TPTP v8.1.2. Released v7.3.0.
% 0.12/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.12/0.33 % Computer : n012.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 : Wed May 8 17:47:08 EDT 2024
% 0.12/0.34 % CPUTime :
% 0.41/0.59 % Version: 1.5
% 0.41/0.59 % SZS status Unsatisfiable
% 0.41/0.59 % SZS output start CNFRefutation
% See solution above
% 0.41/0.59
% 0.41/0.59 % Initial clauses : 7
% 0.41/0.59 % Processed clauses : 49
% 0.41/0.59 % Factors computed : 0
% 0.41/0.59 % Resolvents computed: 136
% 0.41/0.59 % Tautologies deleted: 0
% 0.41/0.59 % Forward subsumed : 0
% 0.41/0.59 % Backward subsumed : 0
% 0.41/0.59 % -------- CPU Time ---------
% 0.41/0.59 % User time : 0.232 s
% 0.41/0.59 % System time : 0.016 s
% 0.41/0.59 % Total time : 0.248 s
%------------------------------------------------------------------------------