%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : PUZ040-1 : TPTP v8.1.2. Bugfixed v2.6.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n016.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:37:41 EDT 2024
% Result : Unsatisfiable 31.56s 31.77s
% Output : Refutation 31.56s
% Verified :
% SZS Type : Refutation
% Derivation depth : 20
% Number of leaves : 14
% Syntax : Number of clauses : 34 ( 22 unt; 0 nHn; 34 RR)
% Number of literals : 46 ( 0 equ; 13 neg)
% Maximal clause size : 2 ( 1 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 2 ( 1 usr; 1 prp; 0-12 aty)
% Number of functors : 14 ( 14 usr; 1 con; 0-2 aty)
% Number of variables : 155 ( 11 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(goal_state,negated_conjecture,
~ state(bb(o,o),X6,X10,X8,X9,X7,X2,X5,X11,X3,X4,X12),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',goal_state) ).
cnf(b_left,axiom,
( ~ state(bb(X463,s(X461)),X465,X469,X467,X468,X466,X460,X464,X470,X462,e1(X463,X461),e2(s(X463),X461))
| state(bb(X463,X461),X465,X469,X467,X468,X466,X460,X464,X470,X462,e1(X463,s(s(X461))),e2(s(X463),s(s(X461)))) ),
file('/export/starexec/sandbox/benchmark/Axioms/PUZ004-0.ax',b_left) ).
cnf(swap_blanks,axiom,
( ~ state(X16,X21,X25,X23,X24,X22,X13,X20,X26,X15,e1(X19,X14),e2(X17,X18))
| state(X16,X21,X25,X23,X24,X22,X13,X20,X26,X15,e1(X17,X18),e2(X19,X14)) ),
file('/export/starexec/sandbox/benchmark/Axioms/PUZ004-0.ax',swap_blanks) ).
cnf(v1_down,axiom,
( ~ state(X222,v1(X223,X220),X228,X226,X227,X225,X219,X224,X229,X221,e1(s(s(X223)),X220),X230)
| state(X222,v1(s(X223),X220),X228,X226,X227,X225,X219,X224,X229,X221,e1(X223,X220),X230) ),
file('/export/starexec/sandbox/benchmark/Axioms/PUZ004-0.ax',v1_down) ).
cnf(s1_down,axiom,
( ~ state(X53,X56,X60,X58,X59,X57,s1(X54,X51),X55,X61,X52,e1(s(X54),X51),X62)
| state(X53,X56,X60,X58,X59,X57,s1(s(X54),X51),X55,X61,X52,e1(X54,X51),X62) ),
file('/export/starexec/sandbox/benchmark/Axioms/PUZ004-0.ax',s1_down) ).
cnf(v3_right,axiom,
( ~ state(X385,X389,X384,v3(X387,X392),X391,X390,X383,X388,X393,X386,e1(X387,s(X392)),e2(s(X387),s(X392)))
| state(X385,X389,X384,v3(X387,s(X392)),X391,X390,X383,X388,X393,X386,e1(X387,X392),e2(s(X387),X392)) ),
file('/export/starexec/sandbox/benchmark/Axioms/PUZ004-0.ax',v3_right) ).
cnf(s3_up,axiom,
( ~ state(X162,X165,X169,X167,X168,X166,X159,X164,s3(s(X163),X160),X161,e1(X163,X160),X170)
| state(X162,X165,X169,X167,X168,X166,X159,X164,s3(X163,X160),X161,e1(s(X163),X160),X170) ),
file('/export/starexec/sandbox/benchmark/Axioms/PUZ004-0.ax',s3_up) ).
cnf(s1_left,axiom,
( ~ state(X41,X44,X48,X46,X47,X45,s1(X42,s(X39)),X43,X49,X40,e1(X42,X39),X50)
| state(X41,X44,X48,X46,X47,X45,s1(X42,X39),X43,X49,X40,e1(X42,s(X39)),X50) ),
file('/export/starexec/sandbox/benchmark/Axioms/PUZ004-0.ax',s1_left) ).
cnf(v1_up,axiom,
( ~ state(X234,v1(s(X235),X232),X240,X238,X239,X237,X231,X236,X241,X233,e1(X235,X232),X242)
| state(X234,v1(X235,X232),X240,X238,X239,X237,X231,X236,X241,X233,e1(s(s(X235)),X232),X242) ),
file('/export/starexec/sandbox/benchmark/Axioms/PUZ004-0.ax',v1_up) ).
cnf(s1_up,axiom,
( ~ state(X65,X68,X72,X70,X71,X69,s1(s(X66),X63),X67,X73,X64,e1(X66,X63),X74)
| state(X65,X68,X72,X70,X71,X69,s1(X66,X63),X67,X73,X64,e1(s(X66),X63),X74) ),
file('/export/starexec/sandbox/benchmark/Axioms/PUZ004-0.ax',s1_up) ).
cnf(h_right,axiom,
( ~ state(X329,X332,X335,X333,X334,h(X330,X327),X326,X331,X336,X328,e1(X330,s(s(X327))),X337)
| state(X329,X332,X335,X333,X334,h(X330,s(X327)),X326,X331,X336,X328,e1(X330,X327),X337) ),
file('/export/starexec/sandbox/benchmark/Axioms/PUZ004-0.ax',h_right) ).
cnf(v4_down,axiom,
( ~ state(X305,X308,X312,X310,v4(X306,X303),X309,X302,X307,X311,X304,e1(s(s(X306)),X303),X313)
| state(X305,X308,X312,X310,v4(s(X306),X303),X309,X302,X307,X311,X304,e1(X306,X303),X313) ),
file('/export/starexec/sandbox/benchmark/Axioms/PUZ004-0.ax',v4_down) ).
cnf(v3_down,axiom,
( ~ state(X269,X273,X268,v3(X271,X276),X275,X274,X267,X272,X277,X270,e1(s(s(X271)),X276),X278)
| state(X269,X273,X268,v3(s(X271),X276),X275,X274,X267,X272,X277,X270,e1(X271,X276),X278) ),
file('/export/starexec/sandbox/benchmark/Axioms/PUZ004-0.ax',v3_down) ).
cnf(initial_state,plain,
state(bb(o,s(o)),v1(o,o),v2(o,s(s(s(o)))),v3(s(s(o)),o),v4(s(s(o)),s(s(s(o)))),h(s(s(o)),s(o)),s1(s(s(s(o))),s(o)),s2(s(s(s(o))),s(s(o))),s3(s(s(s(s(o)))),s(o)),s4(s(s(s(s(o)))),s(s(o))),e1(s(s(s(s(o)))),o),e2(s(s(s(s(o)))),s(s(s(o))))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',initial_state) ).
cnf(c0,plain,
state(bb(o,s(o)),v1(o,o),v2(o,s(s(s(o)))),v3(s(s(s(o))),o),v4(s(s(o)),s(s(s(o)))),h(s(s(o)),s(o)),s1(s(s(s(o))),s(o)),s2(s(s(s(o))),s(s(o))),s3(s(s(s(s(o)))),s(o)),s4(s(s(s(s(o)))),s(s(o))),e1(s(s(o)),o),e2(s(s(s(s(o)))),s(s(s(o))))),
inference(resolution,[status(thm)],[initial_state,v3_down]) ).
cnf(c3,plain,
state(bb(o,s(o)),v1(s(o),o),v2(o,s(s(s(o)))),v3(s(s(s(o))),o),v4(s(s(o)),s(s(s(o)))),h(s(s(o)),s(o)),s1(s(s(s(o))),s(o)),s2(s(s(s(o))),s(s(o))),s3(s(s(s(s(o)))),s(o)),s4(s(s(s(s(o)))),s(s(o))),e1(o,o),e2(s(s(s(s(o)))),s(s(s(o))))),
inference(resolution,[status(thm)],[c0,v1_down]) ).
cnf(c8,plain,
state(bb(o,s(o)),v1(s(o),o),v2(o,s(s(s(o)))),v3(s(s(s(o))),o),v4(s(s(o)),s(s(s(o)))),h(s(s(o)),s(o)),s1(s(s(s(o))),s(o)),s2(s(s(s(o))),s(s(o))),s3(s(s(s(s(o)))),s(o)),s4(s(s(s(s(o)))),s(s(o))),e1(s(s(s(s(o)))),s(s(s(o)))),e2(o,o)),
inference(resolution,[status(thm)],[c3,swap_blanks]) ).
cnf(c11,plain,
state(bb(o,s(o)),v1(s(o),o),v2(o,s(s(s(o)))),v3(s(s(s(o))),o),v4(s(s(s(o))),s(s(s(o)))),h(s(s(o)),s(o)),s1(s(s(s(o))),s(o)),s2(s(s(s(o))),s(s(o))),s3(s(s(s(s(o)))),s(o)),s4(s(s(s(s(o)))),s(s(o))),e1(s(s(o)),s(s(s(o)))),e2(o,o)),
inference(resolution,[status(thm)],[c8,v4_down]) ).
cnf(c13,plain,
state(bb(o,s(o)),v1(s(o),o),v2(o,s(s(s(o)))),v3(s(s(s(o))),o),v4(s(s(s(o))),s(s(s(o)))),h(s(s(o)),s(s(o))),s1(s(s(s(o))),s(o)),s2(s(s(s(o))),s(s(o))),s3(s(s(s(s(o)))),s(o)),s4(s(s(s(s(o)))),s(s(o))),e1(s(s(o)),s(o)),e2(o,o)),
inference(resolution,[status(thm)],[c11,h_right]) ).
cnf(c19,plain,
state(bb(o,s(o)),v1(s(o),o),v2(o,s(s(s(o)))),v3(s(s(s(o))),o),v4(s(s(s(o))),s(s(s(o)))),h(s(s(o)),s(s(o))),s1(s(s(o)),s(o)),s2(s(s(s(o))),s(s(o))),s3(s(s(s(s(o)))),s(o)),s4(s(s(s(s(o)))),s(s(o))),e1(s(s(s(o))),s(o)),e2(o,o)),
inference(resolution,[status(thm)],[c13,s1_up]) ).
cnf(c25,plain,
state(bb(o,s(o)),v1(s(o),o),v2(o,s(s(s(o)))),v3(s(s(s(o))),o),v4(s(s(s(o))),s(s(s(o)))),h(s(s(o)),s(s(o))),s1(s(s(o)),s(o)),s2(s(s(s(o))),s(s(o))),s3(s(s(s(o))),s(o)),s4(s(s(s(s(o)))),s(s(o))),e1(s(s(s(s(o)))),s(o)),e2(o,o)),
inference(resolution,[status(thm)],[c19,s3_up]) ).
cnf(c37,plain,
state(bb(o,s(o)),v1(s(o),o),v2(o,s(s(s(o)))),v3(s(s(s(o))),o),v4(s(s(s(o))),s(s(s(o)))),h(s(s(o)),s(s(o))),s1(s(s(o)),s(o)),s2(s(s(s(o))),s(s(o))),s3(s(s(s(o))),s(o)),s4(s(s(s(s(o)))),s(s(o))),e1(o,o),e2(s(s(s(s(o)))),s(o))),
inference(resolution,[status(thm)],[c25,swap_blanks]) ).
cnf(c50,plain,
state(bb(o,s(o)),v1(o,o),v2(o,s(s(s(o)))),v3(s(s(s(o))),o),v4(s(s(s(o))),s(s(s(o)))),h(s(s(o)),s(s(o))),s1(s(s(o)),s(o)),s2(s(s(s(o))),s(s(o))),s3(s(s(s(o))),s(o)),s4(s(s(s(s(o)))),s(s(o))),e1(s(s(o)),o),e2(s(s(s(s(o)))),s(o))),
inference(resolution,[status(thm)],[c37,v1_up]) ).
cnf(c142,plain,
state(bb(o,s(o)),v1(o,o),v2(o,s(s(s(o)))),v3(s(s(s(o))),o),v4(s(s(s(o))),s(s(s(o)))),h(s(s(o)),s(s(o))),s1(s(s(o)),o),s2(s(s(s(o))),s(s(o))),s3(s(s(s(o))),s(o)),s4(s(s(s(s(o)))),s(s(o))),e1(s(s(o)),s(o)),e2(s(s(s(s(o)))),s(o))),
inference(resolution,[status(thm)],[c50,s1_left]) ).
cnf(c237,plain,
state(bb(o,s(o)),v1(o,o),v2(o,s(s(s(o)))),v3(s(s(s(o))),o),v4(s(s(s(o))),s(s(s(o)))),h(s(s(o)),s(s(o))),s1(s(s(o)),o),s2(s(s(s(o))),s(s(o))),s3(s(s(o)),s(o)),s4(s(s(s(s(o)))),s(s(o))),e1(s(s(s(o))),s(o)),e2(s(s(s(s(o)))),s(o))),
inference(resolution,[status(thm)],[c142,s3_up]) ).
cnf(c355,plain,
state(bb(o,s(o)),v1(o,o),v2(o,s(s(s(o)))),v3(s(s(s(o))),s(o)),v4(s(s(s(o))),s(s(s(o)))),h(s(s(o)),s(s(o))),s1(s(s(o)),o),s2(s(s(s(o))),s(s(o))),s3(s(s(o)),s(o)),s4(s(s(s(s(o)))),s(s(o))),e1(s(s(s(o))),o),e2(s(s(s(s(o)))),o)),
inference(resolution,[status(thm)],[c237,v3_right]) ).
cnf(c359,plain,
state(bb(o,s(o)),v1(o,o),v2(o,s(s(s(o)))),v3(s(s(s(o))),s(o)),v4(s(s(s(o))),s(s(s(o)))),h(s(s(o)),s(s(o))),s1(s(s(s(o))),o),s2(s(s(s(o))),s(s(o))),s3(s(s(o)),s(o)),s4(s(s(s(s(o)))),s(s(o))),e1(s(s(o)),o),e2(s(s(s(s(o)))),o)),
inference(resolution,[status(thm)],[c355,s1_down]) ).
cnf(c361,plain,
state(bb(o,s(o)),v1(s(o),o),v2(o,s(s(s(o)))),v3(s(s(s(o))),s(o)),v4(s(s(s(o))),s(s(s(o)))),h(s(s(o)),s(s(o))),s1(s(s(s(o))),o),s2(s(s(s(o))),s(s(o))),s3(s(s(o)),s(o)),s4(s(s(s(s(o)))),s(s(o))),e1(o,o),e2(s(s(s(s(o)))),o)),
inference(resolution,[status(thm)],[c359,v1_down]) ).
cnf(c366,plain,
state(bb(o,s(o)),v1(s(o),o),v2(o,s(s(s(o)))),v3(s(s(s(o))),s(o)),v4(s(s(s(o))),s(s(s(o)))),h(s(s(o)),s(s(o))),s1(s(s(s(o))),o),s2(s(s(s(o))),s(s(o))),s3(s(s(o)),s(o)),s4(s(s(s(s(o)))),s(s(o))),e1(s(s(s(s(o)))),o),e2(o,o)),
inference(resolution,[status(thm)],[c361,swap_blanks]) ).
cnf(c370,plain,
state(bb(o,s(o)),v1(s(o),o),v2(o,s(s(s(o)))),v3(s(s(s(o))),s(o)),v4(s(s(s(o))),s(s(s(o)))),h(s(s(o)),s(s(o))),s1(s(s(s(s(o)))),o),s2(s(s(s(o))),s(s(o))),s3(s(s(o)),s(o)),s4(s(s(s(s(o)))),s(s(o))),e1(s(s(s(o))),o),e2(o,o)),
inference(resolution,[status(thm)],[c366,s1_down]) ).
cnf(c372,plain,
state(bb(o,s(o)),v1(s(s(o)),o),v2(o,s(s(s(o)))),v3(s(s(s(o))),s(o)),v4(s(s(s(o))),s(s(s(o)))),h(s(s(o)),s(s(o))),s1(s(s(s(s(o)))),o),s2(s(s(s(o))),s(s(o))),s3(s(s(o)),s(o)),s4(s(s(s(s(o)))),s(s(o))),e1(s(o),o),e2(o,o)),
inference(resolution,[status(thm)],[c370,v1_down]) ).
cnf(c376,plain,
state(bb(o,s(o)),v1(s(s(o)),o),v2(o,s(s(s(o)))),v3(s(s(s(o))),s(o)),v4(s(s(s(o))),s(s(s(o)))),h(s(s(o)),s(s(o))),s1(s(s(s(s(o)))),o),s2(s(s(s(o))),s(s(o))),s3(s(s(o)),s(o)),s4(s(s(s(s(o)))),s(s(o))),e1(o,o),e2(s(o),o)),
inference(resolution,[status(thm)],[c372,swap_blanks]) ).
cnf(c377,plain,
state(bb(o,o),v1(s(s(o)),o),v2(o,s(s(s(o)))),v3(s(s(s(o))),s(o)),v4(s(s(s(o))),s(s(s(o)))),h(s(s(o)),s(s(o))),s1(s(s(s(s(o)))),o),s2(s(s(s(o))),s(s(o))),s3(s(s(o)),s(o)),s4(s(s(s(s(o)))),s(s(o))),e1(o,s(s(o))),e2(s(o),s(s(o)))),
inference(resolution,[status(thm)],[c376,b_left]) ).
cnf(c921,plain,
$false,
inference(resolution,[status(thm)],[c377,goal_state]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : PUZ040-1 : TPTP v8.1.2. Bugfixed v2.6.0.
% 0.07/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.34 % Computer : n016.cluster.edu
% 0.14/0.34 % Model : x86_64 x86_64
% 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.34 % Memory : 8042.1875MB
% 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.34 % CPULimit : 300
% 0.14/0.34 % WCLimit : 300
% 0.14/0.34 % DateTime : Wed May 8 20:47:08 EDT 2024
% 0.14/0.34 % CPUTime :
% 31.56/31.77 % Version: 1.5
% 31.56/31.77 % SZS status Unsatisfiable
% 31.56/31.77 % SZS output start CNFRefutation
% See solution above
% 31.56/31.77
% 31.56/31.77 % Initial clauses : 43
% 31.56/31.77 % Processed clauses : 361
% 31.56/31.77 % Factors computed : 0
% 31.56/31.77 % Resolvents computed: 922
% 31.56/31.77 % Tautologies deleted: 0
% 31.56/31.77 % Forward subsumed : 285
% 31.56/31.77 % Backward subsumed : 0
% 31.56/31.77 % -------- CPU Time ---------
% 31.56/31.77 % User time : 31.412 s
% 31.56/31.77 % System time : 0.016 s
% 31.56/31.77 % Total time : 31.428 s
%------------------------------------------------------------------------------