%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : PUZ008-3 : TPTP v8.1.2. Released v1.2.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n007.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:34 EDT 2024
% Result : Unsatisfiable 0.60s 0.85s
% Output : Refutation 0.60s
% Verified :
% SZS Type : Refutation
% Derivation depth : 35
% Number of leaves : 10
% Syntax : Number of clauses : 51 ( 23 unt; 0 nHn; 42 RR)
% Number of literals : 98 ( 0 equ; 48 neg)
% Maximal clause size : 4 ( 1 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 4 ( 3 usr; 1 prp; 0-3 aty)
% Number of functors : 8 ( 8 usr; 3 con; 0-2 aty)
% Number of variables : 30 ( 10 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(prove_can_get_to_east_bank,negated_conjecture,
~ achievable(west(m(n0),c(n0)),X35,east(m(s(s(s(n0)))),c(s(s(s(n0)))))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_can_get_to_east_bank) ).
cnf(no_missionaries_is_safe,axiom,
safe(n0,X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',no_missionaries_is_safe) ).
cnf(same_or_more_missionaries_is_safe,axiom,
( ~ greater_or_equal(X4,X5)
| safe(X4,X5) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',same_or_more_missionaries_is_safe) ).
cnf(great_eq_recursive,axiom,
( greater_or_equal(s(X7),s(X8))
| ~ greater_or_equal(X7,X8) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',great_eq_recursive) ).
cnf(great_eq_base,axiom,
greater_or_equal(X3,n0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',great_eq_base) ).
cnf(c1,plain,
greater_or_equal(s(X13),s(n0)),
inference(resolution,[status(thm)],[great_eq_recursive,great_eq_base]) ).
cnf(c2,plain,
greater_or_equal(s(s(X15)),s(s(n0))),
inference(resolution,[status(thm)],[c1,great_eq_recursive]) ).
cnf(c4,plain,
greater_or_equal(s(s(s(X17))),s(s(s(n0)))),
inference(resolution,[status(thm)],[c2,great_eq_recursive]) ).
cnf(c7,plain,
safe(s(s(s(X22))),s(s(s(n0)))),
inference(resolution,[status(thm)],[c4,same_or_more_missionaries_is_safe]) ).
cnf(two_cannibals_west_to_east,axiom,
( ~ achievable(west(m(X27),c(s(s(X28)))),boatonwest,east(m(X29),c(X30)))
| ~ safe(X27,X28)
| ~ safe(X29,s(s(X30)))
| achievable(west(m(X27),c(X28)),boatoneast,east(m(X29),c(s(s(X30))))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',two_cannibals_west_to_east) ).
cnf(c3,plain,
safe(s(X14),s(n0)),
inference(resolution,[status(thm)],[c1,same_or_more_missionaries_is_safe]) ).
cnf(cannibal_east_to_west,axiom,
( ~ achievable(west(m(X18),c(X19)),boatoneast,east(m(X20),c(s(X21))))
| ~ safe(X18,s(X19))
| ~ safe(X20,X21)
| achievable(west(m(X18),c(s(X19))),boatonwest,east(m(X20),c(X21))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cannibal_east_to_west) ).
cnf(c5,plain,
safe(s(s(X16)),s(s(n0))),
inference(resolution,[status(thm)],[c2,same_or_more_missionaries_is_safe]) ).
cnf(c0,plain,
safe(X6,n0),
inference(resolution,[status(thm)],[same_or_more_missionaries_is_safe,great_eq_base]) ).
cnf(two_missionaries_west_to_east,axiom,
( ~ achievable(west(m(s(s(X60))),c(X61)),boatonwest,east(m(X62),c(X63)))
| ~ safe(X60,X61)
| ~ safe(s(s(X62)),X63)
| achievable(west(m(X60),c(X61)),boatoneast,east(m(s(s(X62))),c(X63))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',two_missionaries_west_to_east) ).
cnf(missionary_and_cannibal_east_to_west,axiom,
( ~ achievable(west(m(X72),c(X73)),boatoneast,east(m(s(X74)),c(s(X75))))
| ~ safe(s(X72),s(X73))
| ~ safe(X74,X75)
| achievable(west(m(s(X72)),c(s(X73))),boatonwest,east(m(X74),c(X75))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',missionary_and_cannibal_east_to_west) ).
cnf(start_on_west_bank,plain,
achievable(west(m(s(s(s(n0)))),c(s(s(s(n0))))),boatonwest,east(m(n0),c(n0))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',start_on_west_bank) ).
cnf(c17,plain,
( ~ safe(s(s(s(n0))),s(n0))
| ~ safe(n0,s(s(n0)))
| achievable(west(m(s(s(s(n0)))),c(s(n0))),boatoneast,east(m(n0),c(s(s(n0))))) ),
inference(resolution,[status(thm)],[start_on_west_bank,two_cannibals_west_to_east]) ).
cnf(c36,plain,
( ~ safe(n0,s(s(n0)))
| achievable(west(m(s(s(s(n0)))),c(s(n0))),boatoneast,east(m(n0),c(s(s(n0))))) ),
inference(resolution,[status(thm)],[c17,c3]) ).
cnf(c37,plain,
achievable(west(m(s(s(s(n0)))),c(s(n0))),boatoneast,east(m(n0),c(s(s(n0))))),
inference(resolution,[status(thm)],[c36,no_missionaries_is_safe]) ).
cnf(c39,plain,
( ~ safe(s(s(s(n0))),s(s(n0)))
| ~ safe(n0,s(n0))
| achievable(west(m(s(s(s(n0)))),c(s(s(n0)))),boatonwest,east(m(n0),c(s(n0)))) ),
inference(resolution,[status(thm)],[c37,cannibal_east_to_west]) ).
cnf(c47,plain,
( ~ safe(n0,s(n0))
| achievable(west(m(s(s(s(n0)))),c(s(s(n0)))),boatonwest,east(m(n0),c(s(n0)))) ),
inference(resolution,[status(thm)],[c39,c5]) ).
cnf(c48,plain,
achievable(west(m(s(s(s(n0)))),c(s(s(n0)))),boatonwest,east(m(n0),c(s(n0)))),
inference(resolution,[status(thm)],[c47,no_missionaries_is_safe]) ).
cnf(c55,plain,
( ~ safe(s(s(s(n0))),n0)
| ~ safe(n0,s(s(s(n0))))
| achievable(west(m(s(s(s(n0)))),c(n0)),boatoneast,east(m(n0),c(s(s(s(n0)))))) ),
inference(resolution,[status(thm)],[c48,two_cannibals_west_to_east]) ).
cnf(c57,plain,
( ~ safe(s(s(s(n0))),n0)
| achievable(west(m(s(s(s(n0)))),c(n0)),boatoneast,east(m(n0),c(s(s(s(n0)))))) ),
inference(resolution,[status(thm)],[c55,no_missionaries_is_safe]) ).
cnf(c60,plain,
achievable(west(m(s(s(s(n0)))),c(n0)),boatoneast,east(m(n0),c(s(s(s(n0)))))),
inference(resolution,[status(thm)],[c57,c0]) ).
cnf(c62,plain,
( ~ safe(s(s(s(n0))),s(n0))
| ~ safe(n0,s(s(n0)))
| achievable(west(m(s(s(s(n0)))),c(s(n0))),boatonwest,east(m(n0),c(s(s(n0))))) ),
inference(resolution,[status(thm)],[c60,cannibal_east_to_west]) ).
cnf(c63,plain,
( ~ safe(n0,s(s(n0)))
| achievable(west(m(s(s(s(n0)))),c(s(n0))),boatonwest,east(m(n0),c(s(s(n0))))) ),
inference(resolution,[status(thm)],[c62,c3]) ).
cnf(c64,plain,
achievable(west(m(s(s(s(n0)))),c(s(n0))),boatonwest,east(m(n0),c(s(s(n0))))),
inference(resolution,[status(thm)],[c63,no_missionaries_is_safe]) ).
cnf(c65,plain,
( ~ safe(s(n0),s(n0))
| ~ safe(s(s(n0)),s(s(n0)))
| achievable(west(m(s(n0)),c(s(n0))),boatoneast,east(m(s(s(n0))),c(s(s(n0))))) ),
inference(resolution,[status(thm)],[c64,two_missionaries_west_to_east]) ).
cnf(c69,plain,
( ~ safe(s(n0),s(n0))
| achievable(west(m(s(n0)),c(s(n0))),boatoneast,east(m(s(s(n0))),c(s(s(n0))))) ),
inference(resolution,[status(thm)],[c65,c5]) ).
cnf(c70,plain,
achievable(west(m(s(n0)),c(s(n0))),boatoneast,east(m(s(s(n0))),c(s(s(n0))))),
inference(resolution,[status(thm)],[c69,c3]) ).
cnf(c75,plain,
( ~ safe(s(s(n0)),s(s(n0)))
| ~ safe(s(n0),s(n0))
| achievable(west(m(s(s(n0))),c(s(s(n0)))),boatonwest,east(m(s(n0)),c(s(n0)))) ),
inference(resolution,[status(thm)],[c70,missionary_and_cannibal_east_to_west]) ).
cnf(c79,plain,
( ~ safe(s(n0),s(n0))
| achievable(west(m(s(s(n0))),c(s(s(n0)))),boatonwest,east(m(s(n0)),c(s(n0)))) ),
inference(resolution,[status(thm)],[c75,c5]) ).
cnf(c80,plain,
achievable(west(m(s(s(n0))),c(s(s(n0)))),boatonwest,east(m(s(n0)),c(s(n0)))),
inference(resolution,[status(thm)],[c79,c3]) ).
cnf(c81,plain,
( ~ safe(n0,s(s(n0)))
| ~ safe(s(s(s(n0))),s(n0))
| achievable(west(m(n0),c(s(s(n0)))),boatoneast,east(m(s(s(s(n0)))),c(s(n0)))) ),
inference(resolution,[status(thm)],[c80,two_missionaries_west_to_east]) ).
cnf(c88,plain,
( ~ safe(n0,s(s(n0)))
| achievable(west(m(n0),c(s(s(n0)))),boatoneast,east(m(s(s(s(n0)))),c(s(n0)))) ),
inference(resolution,[status(thm)],[c81,c3]) ).
cnf(c89,plain,
achievable(west(m(n0),c(s(s(n0)))),boatoneast,east(m(s(s(s(n0)))),c(s(n0)))),
inference(resolution,[status(thm)],[c88,no_missionaries_is_safe]) ).
cnf(c91,plain,
( ~ safe(n0,s(s(s(n0))))
| ~ safe(s(s(s(n0))),n0)
| achievable(west(m(n0),c(s(s(s(n0))))),boatonwest,east(m(s(s(s(n0)))),c(n0))) ),
inference(resolution,[status(thm)],[c89,cannibal_east_to_west]) ).
cnf(c94,plain,
( ~ safe(n0,s(s(s(n0))))
| achievable(west(m(n0),c(s(s(s(n0))))),boatonwest,east(m(s(s(s(n0)))),c(n0))) ),
inference(resolution,[status(thm)],[c91,c0]) ).
cnf(c95,plain,
achievable(west(m(n0),c(s(s(s(n0))))),boatonwest,east(m(s(s(s(n0)))),c(n0))),
inference(resolution,[status(thm)],[c94,no_missionaries_is_safe]) ).
cnf(c99,plain,
( ~ safe(n0,s(n0))
| ~ safe(s(s(s(n0))),s(s(n0)))
| achievable(west(m(n0),c(s(n0))),boatoneast,east(m(s(s(s(n0)))),c(s(s(n0))))) ),
inference(resolution,[status(thm)],[c95,two_cannibals_west_to_east]) ).
cnf(c100,plain,
( ~ safe(n0,s(n0))
| achievable(west(m(n0),c(s(n0))),boatoneast,east(m(s(s(s(n0)))),c(s(s(n0))))) ),
inference(resolution,[status(thm)],[c99,c5]) ).
cnf(c101,plain,
achievable(west(m(n0),c(s(n0))),boatoneast,east(m(s(s(s(n0)))),c(s(s(n0))))),
inference(resolution,[status(thm)],[c100,no_missionaries_is_safe]) ).
cnf(c104,plain,
( ~ safe(n0,s(s(n0)))
| ~ safe(s(s(s(n0))),s(n0))
| achievable(west(m(n0),c(s(s(n0)))),boatonwest,east(m(s(s(s(n0)))),c(s(n0)))) ),
inference(resolution,[status(thm)],[c101,cannibal_east_to_west]) ).
cnf(c107,plain,
( ~ safe(n0,s(s(n0)))
| achievable(west(m(n0),c(s(s(n0)))),boatonwest,east(m(s(s(s(n0)))),c(s(n0)))) ),
inference(resolution,[status(thm)],[c104,c3]) ).
cnf(c110,plain,
achievable(west(m(n0),c(s(s(n0)))),boatonwest,east(m(s(s(s(n0)))),c(s(n0)))),
inference(resolution,[status(thm)],[c107,no_missionaries_is_safe]) ).
cnf(c112,plain,
( ~ safe(n0,n0)
| ~ safe(s(s(s(n0))),s(s(s(n0))))
| achievable(west(m(n0),c(n0)),boatoneast,east(m(s(s(s(n0)))),c(s(s(s(n0)))))) ),
inference(resolution,[status(thm)],[c110,two_cannibals_west_to_east]) ).
cnf(c118,plain,
( ~ safe(n0,n0)
| achievable(west(m(n0),c(n0)),boatoneast,east(m(s(s(s(n0)))),c(s(s(s(n0)))))) ),
inference(resolution,[status(thm)],[c112,c7]) ).
cnf(c119,plain,
achievable(west(m(n0),c(n0)),boatoneast,east(m(s(s(s(n0)))),c(s(s(s(n0)))))),
inference(resolution,[status(thm)],[c118,no_missionaries_is_safe]) ).
cnf(c121,plain,
$false,
inference(resolution,[status(thm)],[c119,prove_can_get_to_east_bank]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.13 % Problem : PUZ008-3 : TPTP v8.1.2. Released v1.2.0.
% 0.07/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.15/0.35 % Computer : n007.cluster.edu
% 0.15/0.35 % Model : x86_64 x86_64
% 0.15/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.35 % Memory : 8042.1875MB
% 0.15/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.35 % CPULimit : 300
% 0.15/0.35 % WCLimit : 300
% 0.15/0.35 % DateTime : Wed May 8 20:42:38 EDT 2024
% 0.15/0.36 % CPUTime :
% 0.60/0.85 % Version: 1.5
% 0.60/0.85 % SZS status Unsatisfiable
% 0.60/0.85 % SZS output start CNFRefutation
% See solution above
% 0.60/0.85
% 0.60/0.85 % Initial clauses : 16
% 0.60/0.85 % Processed clauses : 110
% 0.60/0.85 % Factors computed : 0
% 0.60/0.85 % Resolvents computed: 129
% 0.60/0.85 % Tautologies deleted: 0
% 0.60/0.85 % Forward subsumed : 22
% 0.60/0.85 % Backward subsumed : 30
% 0.60/0.85 % -------- CPU Time ---------
% 0.60/0.85 % User time : 0.467 s
% 0.60/0.85 % System time : 0.019 s
% 0.60/0.85 % Total time : 0.486 s
%------------------------------------------------------------------------------