%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SYO691-1.001 : TPTP v8.1.2. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n027.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 99.91s 100.12s
% Output : Refutation 99.91s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 6
% Syntax : Number of clauses : 21 ( 13 unt; 0 nHn; 9 RR)
% Number of literals : 30 ( 0 equ; 10 neg)
% Maximal clause size : 3 ( 1 avg)
% Maximal term depth : 10 ( 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 : 72 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(prove,negated_conjecture,
~ seq(succ(succ(succ(succ(succ(zero))))),X11,X11),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove) ).
cnf(rewrite_left,axiom,
( ~ step(X5,X7)
| step(f(X5,X6),f(X7,X6)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rewrite_left) ).
cnf(rewrite_top,axiom,
( ~ top(X3,X4)
| step(X3,X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rewrite_top) ).
cnf(rule_1,axiom,
top(f(f(f(X13,a),X14),f(X12,a)),f(f(X12,f(f(X14,a),a)),X13)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rule_1) ).
cnf(c0,plain,
step(f(f(f(X23,a),X22),f(X21,a)),f(f(X21,f(f(X22,a),a)),X23)),
inference(resolution,[status(thm)],[rule_1,rewrite_top]) ).
cnf(c4,plain,
step(f(f(f(f(X32,a),X31),f(X34,a)),X33),f(f(f(X34,f(f(X31,a),a)),X32),X33)),
inference(resolution,[status(thm)],[c0,rewrite_left]) ).
cnf(c11,plain,
step(f(f(f(f(f(X64,a),X62),f(X66,a)),X65),X63),f(f(f(f(X66,f(f(X62,a),a)),X64),X65),X63)),
inference(resolution,[status(thm)],[c4,rewrite_left]) ).
cnf(c31,plain,
step(f(f(f(f(f(f(X148,a),X149),f(X150,a)),X147),X151),X152),f(f(f(f(f(X150,f(f(X149,a),a)),X148),X147),X151),X152)),
inference(resolution,[status(thm)],[c11,rewrite_left]) ).
cnf(rewrite_sequence_succ,axiom,
( ~ seq(X17,X15,X18)
| ~ step(X18,X16)
| seq(succ(X17),X15,X16) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rewrite_sequence_succ) ).
cnf(rewrite_sequence_zero,axiom,
seq(zero,X2,X2),
file('/export/starexec/sandbox/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(c3,plain,
seq(succ(zero),f(f(f(X25,a),X24),f(X26,a)),f(f(X26,f(f(X24,a),a)),X25)),
inference(resolution,[status(thm)],[c0,c1]) ).
cnf(c5,plain,
( ~ step(f(f(X36,f(f(X35,a),a)),X38),X37)
| seq(succ(succ(zero)),f(f(f(X38,a),X35),f(X36,a)),X37) ),
inference(resolution,[status(thm)],[c3,rewrite_sequence_succ]) ).
cnf(c14,plain,
seq(succ(succ(zero)),f(f(f(X155,a),X153),f(f(f(X154,a),X156),a)),f(f(f(f(X153,a),f(f(X156,a),a)),X154),X155)),
inference(resolution,[status(thm)],[c5,c4]) ).
cnf(c95,plain,
( ~ step(f(f(f(f(X388,a),f(f(X391,a),a)),X389),X390),X392)
| seq(succ(succ(succ(zero))),f(f(f(X390,a),X388),f(f(f(X389,a),X391),a)),X392) ),
inference(resolution,[status(thm)],[c14,rewrite_sequence_succ]) ).
cnf(c330,plain,
seq(succ(succ(succ(zero))),f(f(f(X924,a),f(X922,a)),f(f(f(X921,a),X923),a)),f(f(f(f(f(X923,a),f(f(a,a),a)),X922),X921),X924)),
inference(resolution,[status(thm)],[c95,c11]) ).
cnf(c1236,plain,
( ~ step(f(f(f(f(f(X2210,a),f(f(a,a),a)),X2213),X2211),X2209),X2212)
| seq(succ(succ(succ(succ(zero)))),f(f(f(X2209,a),f(X2213,a)),f(f(f(X2211,a),X2210),a)),X2212) ),
inference(resolution,[status(thm)],[c330,rewrite_sequence_succ]) ).
cnf(c5252,plain,
seq(succ(succ(succ(succ(zero)))),f(f(f(X3713,a),f(X3714,a)),f(f(f(X3711,a),f(X3712,a)),a)),f(f(f(f(f(f(a,a),f(f(a,a),a)),X3712),X3714),X3711),X3713)),
inference(resolution,[status(thm)],[c1236,c31]) ).
cnf(c11240,plain,
( ~ step(f(f(f(f(f(f(a,a),f(f(a,a),a)),X7521),X7522),X7520),X7524),X7523)
| seq(succ(succ(succ(succ(succ(zero))))),f(f(f(X7524,a),f(X7522,a)),f(f(f(X7520,a),f(X7521,a)),a)),X7523) ),
inference(resolution,[status(thm)],[c5252,rewrite_sequence_succ]) ).
cnf(c48868,plain,
seq(succ(succ(succ(succ(succ(zero))))),f(f(f(X13462,a),f(X13464,a)),f(f(f(X13461,a),f(f(X13463,a),a)),a)),f(f(f(f(f(X13463,f(f(f(f(a,a),a),a),a)),a),X13464),X13461),X13462)),
inference(resolution,[status(thm)],[c11240,c31]) ).
cnf(c116925,plain,
$false,
inference(resolution,[status(thm)],[c48868,prove]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : SYO691-1.001 : TPTP v8.1.2. Released v7.3.0.
% 0.07/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.33 % Computer : n027.cluster.edu
% 0.13/0.33 % Model : x86_64 x86_64
% 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.33 % Memory : 8042.1875MB
% 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.33 % CPULimit : 300
% 0.13/0.33 % WCLimit : 300
% 0.13/0.33 % DateTime : Wed May 8 18:10:07 EDT 2024
% 0.13/0.34 % CPUTime :
% 99.91/100.12 % Version: 1.5
% 99.91/100.12 % SZS status Unsatisfiable
% 99.91/100.12 % SZS output start CNFRefutation
% See solution above
% 99.91/100.12
% 99.91/100.12 % Initial clauses : 7
% 99.91/100.12 % Processed clauses : 1490
% 99.91/100.12 % Factors computed : 0
% 99.91/100.12 % Resolvents computed: 116927
% 99.91/100.12 % Tautologies deleted: 0
% 99.91/100.12 % Forward subsumed : 83
% 99.91/100.12 % Backward subsumed : 0
% 99.91/100.12 % -------- CPU Time ---------
% 99.91/100.12 % User time : 99.282 s
% 99.91/100.12 % System time : 0.476 s
% 99.91/100.12 % Total time : 99.758 s
%------------------------------------------------------------------------------