%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : PUZ030-2 : TPTP v8.1.2. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n005.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:38 EDT 2024
% Result : Unsatisfiable 0.90s 1.11s
% Output : Refutation 0.90s
% Verified :
% SZS Type : Refutation
% Derivation depth : 29
% Number of leaves : 34
% Syntax : Number of clauses : 105 ( 9 unt; 66 nHn; 105 RR)
% Number of literals : 301 ( 0 equ; 95 neg)
% Maximal clause size : 10 ( 2 avg)
% Maximal term depth : 0 ( 0 avg)
% Number of predicates : 11 ( 10 usr; 11 prp; 0-0 aty)
% Number of functors : 0 ( 0 usr; 0 con; --- aty)
% Number of variables : 0 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(c19,plain,
( ~ mustard_cole
| salt_dix
| mustard_lang ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c19) ).
cnf(c57,plain,
( salt_cole
| mustard_cole
| mustard_lang ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c57) ).
cnf(c24,plain,
( salt_cole
| mustard_lang
| salt_dix ),
inference(resolution,[status(thm)],[c57,c19]) ).
cnf(c16,plain,
( ~ salt_dix
| ~ salt_barry
| salt_cole ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c16) ).
cnf(c43,plain,
( salt_cole
| ~ mustard_cole
| salt_barry ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c43) ).
cnf(c41,plain,
( salt_lang
| ~ mustard_lang
| salt_barry ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c41) ).
cnf(c44,plain,
( ~ salt_cole
| mustard_cole
| salt_barry ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c44) ).
cnf(c16_001,plain,
( mustard_cole
| mustard_lang
| salt_barry ),
inference(resolution,[status(thm)],[c57,c44]) ).
cnf(c138,plain,
( mustard_cole
| salt_barry
| salt_lang ),
inference(resolution,[status(thm)],[c16,c41]) ).
cnf(c36,plain,
( ~ salt_lang
| ~ mustard_lang
| mustard_cole ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c36) ).
cnf(c140,plain,
( mustard_cole
| salt_barry
| ~ salt_lang ),
inference(resolution,[status(thm)],[c16,c36]) ).
cnf(c478,plain,
( mustard_cole
| salt_barry ),
inference(resolution,[status(thm)],[c140,c138]) ).
cnf(c480,plain,
( salt_barry
| salt_cole ),
inference(resolution,[status(thm)],[c478,c43]) ).
cnf(c494,plain,
( salt_cole
| ~ salt_dix ),
inference(resolution,[status(thm)],[c480,c16]) ).
cnf(c526,plain,
( salt_cole
| mustard_lang ),
inference(resolution,[status(thm)],[c494,c24]) ).
cnf(c40,plain,
( ~ salt_mill
| ~ mustard_mill
| mustard_barry ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c40) ).
cnf(c26,plain,
( ~ salt_dix
| mustard_dix
| mustard_mill ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c26) ).
cnf(c62,plain,
( salt_dix
| mustard_dix
| mustard_barry ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c62) ).
cnf(c87,plain,
( mustard_dix
| mustard_barry
| mustard_mill ),
inference(resolution,[status(thm)],[c62,c26]) ).
cnf(c1,plain,
( ~ salt_mill
| mustard_barry
| mustard_lang ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c1) ).
cnf(c56,plain,
( salt_mill
| mustard_mill
| mustard_lang ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c56) ).
cnf(c7,plain,
( mustard_mill
| mustard_lang
| mustard_barry ),
inference(resolution,[status(thm)],[c56,c1]) ).
cnf(c21,plain,
( ~ mustard_barry
| ~ mustard_dix
| mustard_mill ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c21) ).
cnf(c17,plain,
( ~ mustard_cole
| mustard_dix
| mustard_lang ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c17) ).
cnf(c28,plain,
( ~ salt_cole
| mustard_cole
| mustard_mill ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c28) ).
cnf(c17_002,plain,
( mustard_cole
| mustard_lang
| mustard_mill ),
inference(resolution,[status(thm)],[c57,c28]) ).
cnf(c149,plain,
( mustard_lang
| mustard_mill
| mustard_dix ),
inference(resolution,[status(thm)],[c17,c17]) ).
cnf(c554,plain,
( mustard_lang
| mustard_mill
| ~ mustard_barry ),
inference(resolution,[status(thm)],[c149,c21]) ).
cnf(c772,plain,
( mustard_lang
| mustard_mill ),
inference(resolution,[status(thm)],[c554,c7]) ).
cnf(c10,plain,
( ~ mustard_dix
| ~ mustard_lang
| ~ salt_mill ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c10) ).
cnf(c58,plain,
( salt_mill
| mustard_mill
| mustard_dix ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c58) ).
cnf(c42,plain,
( salt_mill
| mustard_mill
| ~ mustard_barry ),
inference(resolution,[status(thm)],[c58,c21]) ).
cnf(c29,plain,
( ~ salt_lang
| ~ mustard_lang
| salt_mill ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c29) ).
cnf(c14,plain,
( salt_mill
| mustard_mill
| ~ salt_lang ),
inference(resolution,[status(thm)],[c56,c29]) ).
cnf(c34,plain,
( ~ salt_barry
| mustard_barry
| salt_lang ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c34) ).
cnf(c3,plain,
( ~ salt_mill
| salt_barry
| mustard_lang ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c3) ).
cnf(c4,plain,
( mustard_mill
| mustard_lang
| salt_barry ),
inference(resolution,[status(thm)],[c56,c3]) ).
cnf(c106,plain,
( mustard_mill
| salt_barry
| salt_lang ),
inference(resolution,[status(thm)],[c4,c41]) ).
cnf(c419,plain,
( mustard_mill
| salt_lang
| mustard_barry ),
inference(resolution,[status(thm)],[c106,c34]) ).
cnf(c627,plain,
( mustard_mill
| mustard_barry
| salt_mill ),
inference(resolution,[status(thm)],[c419,c14]) ).
cnf(c794,plain,
( mustard_mill
| salt_mill ),
inference(resolution,[status(thm)],[c627,c42]) ).
cnf(c817,plain,
( mustard_mill
| ~ mustard_dix
| ~ mustard_lang ),
inference(resolution,[status(thm)],[c794,c10]) ).
cnf(c947,plain,
( mustard_mill
| ~ mustard_dix ),
inference(resolution,[status(thm)],[c817,c772]) ).
cnf(c953,plain,
( mustard_mill
| mustard_barry ),
inference(resolution,[status(thm)],[c947,c87]) ).
cnf(c964,plain,
( mustard_barry
| ~ salt_mill ),
inference(resolution,[status(thm)],[c953,c40]) ).
cnf(c15,plain,
( ~ salt_dix
| ~ salt_barry
| mustard_cole ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c15) ).
cnf(c487,plain,
( mustard_cole
| ~ salt_dix ),
inference(resolution,[status(thm)],[c478,c15]) ).
cnf(c504,plain,
( mustard_cole
| mustard_dix
| mustard_barry ),
inference(resolution,[status(thm)],[c487,c62]) ).
cnf(c730,plain,
( mustard_dix
| mustard_barry
| mustard_lang ),
inference(resolution,[status(thm)],[c504,c17]) ).
cnf(c30,plain,
( ~ salt_barry
| ~ mustard_barry
| salt_mill ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c30) ).
cnf(c39,plain,
( ~ salt_barry
| mustard_barry
| salt_cole ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c39) ).
cnf(c493,plain,
( salt_cole
| mustard_barry ),
inference(resolution,[status(thm)],[c480,c39]) ).
cnf(c512,plain,
( salt_cole
| ~ salt_barry
| salt_mill ),
inference(resolution,[status(thm)],[c493,c30]) ).
cnf(c746,plain,
( salt_cole
| salt_mill ),
inference(resolution,[status(thm)],[c512,c480]) ).
cnf(c7_003,plain,
( ~ mustard_lang
| ~ salt_cole
| ~ mustard_mill ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c7) ).
cnf(c809,plain,
( salt_mill
| ~ mustard_lang
| ~ salt_cole ),
inference(resolution,[status(thm)],[c794,c7]) ).
cnf(c924,plain,
( salt_mill
| ~ mustard_lang ),
inference(resolution,[status(thm)],[c809,c746]) ).
cnf(c930,plain,
( salt_mill
| mustard_dix
| mustard_barry ),
inference(resolution,[status(thm)],[c924,c730]) ).
cnf(c1055,plain,
( mustard_dix
| mustard_barry ),
inference(resolution,[status(thm)],[c930,c964]) ).
cnf(c47,plain,
( ~ salt_cole
| salt_barry
| mustard_barry
| ~ mustard_mill ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c47) ).
cnf(c966,plain,
( mustard_barry
| ~ salt_cole
| salt_barry ),
inference(resolution,[status(thm)],[c953,c47]) ).
cnf(c1135,plain,
( mustard_barry
| salt_barry ),
inference(resolution,[status(thm)],[c966,c480]) ).
cnf(c1141,plain,
( mustard_barry
| salt_lang ),
inference(resolution,[status(thm)],[c1135,c34]) ).
cnf(c11,plain,
( ~ mustard_dix
| ~ salt_lang
| ~ mustard_mill ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c11) ).
cnf(c967,plain,
( mustard_barry
| ~ mustard_dix
| ~ salt_lang ),
inference(resolution,[status(thm)],[c953,c11]) ).
cnf(c1175,plain,
( mustard_barry
| ~ mustard_dix ),
inference(resolution,[status(thm)],[c967,c1141]) ).
cnf(c1182,plain,
mustard_barry,
inference(resolution,[status(thm)],[c1175,c1055]) ).
cnf(c42_004,plain,
( ~ salt_lang
| mustard_lang
| salt_barry ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c42) ).
cnf(c33,plain,
( salt_barry
| ~ mustard_barry
| salt_lang ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c33) ).
cnf(c1137,plain,
( salt_barry
| salt_lang ),
inference(resolution,[status(thm)],[c1135,c33]) ).
cnf(c1146,plain,
( salt_barry
| mustard_lang ),
inference(resolution,[status(thm)],[c1137,c42]) ).
cnf(c6,plain,
( ~ mustard_lang
| ~ mustard_cole
| ~ salt_mill ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c6) ).
cnf(c24_005,plain,
( ~ mustard_barry
| ~ salt_dix
| salt_mill ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c24) ).
cnf(c35,plain,
( ~ salt_cole
| ~ mustard_cole
| salt_dix ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c35) ).
cnf(c483,plain,
( salt_barry
| ~ salt_cole
| salt_dix ),
inference(resolution,[status(thm)],[c478,c35]) ).
cnf(c672,plain,
( salt_barry
| salt_dix ),
inference(resolution,[status(thm)],[c483,c480]) ).
cnf(c677,plain,
( salt_barry
| ~ mustard_barry
| salt_mill ),
inference(resolution,[status(thm)],[c672,c24]) ).
cnf(c1138,plain,
( salt_barry
| salt_mill ),
inference(resolution,[status(thm)],[c1135,c677]) ).
cnf(c1185,plain,
( ~ salt_barry
| salt_mill ),
inference(resolution,[status(thm)],[c1182,c30]) ).
cnf(c1186,plain,
salt_mill,
inference(resolution,[status(thm)],[c1185,c1138]) ).
cnf(c1195,plain,
( ~ mustard_lang
| ~ mustard_cole ),
inference(resolution,[status(thm)],[c1186,c6]) ).
cnf(c1208,plain,
( ~ mustard_lang
| salt_barry ),
inference(resolution,[status(thm)],[c1195,c478]) ).
cnf(c1218,plain,
salt_barry,
inference(resolution,[status(thm)],[c1208,c1146]) ).
cnf(c46,plain,
( ~ salt_cole
| ~ mustard_barry
| ~ salt_barry
| ~ salt_mill ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c46) ).
cnf(c1197,plain,
( ~ salt_cole
| ~ mustard_barry
| ~ salt_barry ),
inference(resolution,[status(thm)],[c1186,c46]) ).
cnf(c1220,plain,
( ~ salt_cole
| ~ mustard_barry ),
inference(resolution,[status(thm)],[c1197,c1218]) ).
cnf(c1221,plain,
~ salt_cole,
inference(resolution,[status(thm)],[c1220,c1182]) ).
cnf(c1222,plain,
mustard_lang,
inference(resolution,[status(thm)],[c1221,c526]) ).
cnf(c1193,plain,
( ~ mustard_dix
| ~ mustard_lang ),
inference(resolution,[status(thm)],[c1186,c10]) ).
cnf(c1225,plain,
~ mustard_dix,
inference(resolution,[status(thm)],[c1222,c1193]) ).
cnf(c50,plain,
( ~ mustard_mill
| salt_cole
| mustard_cole
| salt_dix
| mustard_dix ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c50) ).
cnf(c1224,plain,
( ~ salt_lang
| mustard_cole ),
inference(resolution,[status(thm)],[c1222,c36]) ).
cnf(c151,plain,
( mustard_lang
| mustard_mill
| salt_dix ),
inference(resolution,[status(thm)],[c17,c19]) ).
cnf(prove_who_takes_what,negated_conjecture,
( salt_lang
| ~ mustard_barry
| ~ salt_barry
| ~ salt_mill
| ~ mustard_lang
| salt_cole
| mustard_cole
| salt_dix
| mustard_dix
| mustard_mill ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_who_takes_what) ).
cnf(c588,plain,
( salt_lang
| ~ mustard_barry
| ~ salt_barry
| ~ salt_mill
| salt_cole
| mustard_cole
| salt_dix
| mustard_dix
| mustard_mill ),
inference(resolution,[status(thm)],[prove_who_takes_what,c151]) ).
cnf(c1227,plain,
( salt_lang
| ~ mustard_barry
| ~ salt_barry
| salt_cole
| mustard_cole
| salt_dix
| mustard_dix
| mustard_mill ),
inference(resolution,[status(thm)],[c588,c1186]) ).
cnf(c1228,plain,
( salt_lang
| ~ mustard_barry
| salt_cole
| mustard_cole
| salt_dix
| mustard_dix
| mustard_mill ),
inference(resolution,[status(thm)],[c1227,c1218]) ).
cnf(c1229,plain,
( salt_lang
| salt_cole
| mustard_cole
| salt_dix
| mustard_dix
| mustard_mill ),
inference(resolution,[status(thm)],[c1228,c1182]) ).
cnf(c1230,plain,
( salt_cole
| mustard_cole
| salt_dix
| mustard_dix
| mustard_mill ),
inference(resolution,[status(thm)],[c1229,c1224]) ).
cnf(c1255,plain,
( salt_cole
| mustard_cole
| salt_dix
| mustard_dix ),
inference(resolution,[status(thm)],[c1230,c50]) ).
cnf(c1281,plain,
( mustard_cole
| salt_dix
| mustard_dix ),
inference(resolution,[status(thm)],[c1255,c1221]) ).
cnf(c1293,plain,
( mustard_cole
| mustard_dix ),
inference(resolution,[status(thm)],[c1281,c487]) ).
cnf(c1299,plain,
mustard_cole,
inference(resolution,[status(thm)],[c1293,c1225]) ).
cnf(c1302,plain,
~ mustard_lang,
inference(resolution,[status(thm)],[c1299,c1195]) ).
cnf(c1303,plain,
$false,
inference(resolution,[status(thm)],[c1302,c1222]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : PUZ030-2 : TPTP v8.1.2. Released v1.0.0.
% 0.07/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.34 % Computer : n005.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Wed May 8 20:43:08 EDT 2024
% 0.13/0.34 % CPUTime :
% 0.90/1.11 % Version: 1.5
% 0.90/1.11 % SZS status Unsatisfiable
% 0.90/1.11 % SZS output start CNFRefutation
% See solution above
% 0.90/1.11
% 0.90/1.11 % Initial clauses : 63
% 0.90/1.11 % Processed clauses : 192
% 0.90/1.11 % Factors computed : 0
% 0.90/1.11 % Resolvents computed: 1304
% 0.90/1.11 % Tautologies deleted: 218
% 0.90/1.11 % Forward subsumed : 908
% 0.90/1.11 % Backward subsumed : 178
% 0.90/1.11 % -------- CPU Time ---------
% 0.90/1.11 % User time : 0.749 s
% 0.90/1.11 % System time : 0.019 s
% 0.90/1.11 % Total time : 0.768 s
%------------------------------------------------------------------------------