%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : PUZ056-2.005 : TPTP v8.1.2. Released v3.5.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n023.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:43 EDT 2024
% Result : Unsatisfiable 4.56s 4.74s
% Output : Refutation 4.56s
% Verified :
% SZS Type : Refutation
% Derivation depth : 69
% Number of leaves : 13
% Syntax : Number of clauses : 82 ( 40 unt; 0 nHn; 65 RR)
% Number of literals : 180 ( 0 equ; 99 neg)
% Maximal clause size : 10 ( 2 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 3 ( 2 usr; 1 prp; 0-5 aty)
% Number of functors : 3 ( 3 usr; 3 con; 0-0 aty)
% Number of variables : 83 ( 18 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(goal,negated_conjecture,
~ p(s2,s2,s2,s2,s2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goal) ).
cnf(rule1,axiom,
( ~ p(X6,X4,X2,X3,X7)
| p(X5,X4,X2,X3,X7) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rule1) ).
cnf(neq2,axiom,
neq(s0,s1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',neq2) ).
cnf(neq3,axiom,
neq(s0,s2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',neq3) ).
cnf(rule2,axiom,
( ~ p(X10,X12,X8,X9,X13)
| ~ neq(X10,X12)
| ~ neq(X10,X11)
| p(X10,X11,X8,X9,X13) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rule2) ).
cnf(neq4,axiom,
neq(s1,s0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',neq4) ).
cnf(neq6,axiom,
neq(s1,s2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',neq6) ).
cnf(rule3,axiom,
( ~ p(X21,X20,X23,X19,X24)
| ~ neq(X21,X23)
| ~ neq(X21,X22)
| ~ neq(X20,X23)
| ~ neq(X20,X22)
| p(X21,X20,X22,X19,X24) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rule3) ).
cnf(neq7,axiom,
neq(s2,s0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',neq7) ).
cnf(neq8,axiom,
neq(s2,s1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',neq8) ).
cnf(rule4,axiom,
( ~ p(X29,X28,X27,X31,X32)
| ~ neq(X29,X31)
| ~ neq(X29,X30)
| ~ neq(X28,X31)
| ~ neq(X28,X30)
| ~ neq(X27,X31)
| ~ neq(X27,X30)
| p(X29,X28,X27,X30,X32) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rule4) ).
cnf(rule5,axiom,
( ~ p(X38,X37,X35,X36,X40)
| ~ neq(X38,X40)
| ~ neq(X38,X39)
| ~ neq(X37,X40)
| ~ neq(X37,X39)
| ~ neq(X35,X40)
| ~ neq(X35,X39)
| ~ neq(X36,X40)
| ~ neq(X36,X39)
| p(X38,X37,X35,X36,X39) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rule5) ).
cnf(init,axiom,
p(s0,s0,s0,s0,s0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',init) ).
cnf(c0,plain,
p(X14,s0,s0,s0,s0),
inference(resolution,[status(thm)],[init,rule1]) ).
cnf(c3,plain,
( ~ neq(X16,s0)
| ~ neq(X16,X17)
| p(X16,X17,s0,s0,s0) ),
inference(resolution,[status(thm)],[c0,rule2]) ).
cnf(c5,plain,
( ~ neq(s2,s0)
| p(s2,s1,s0,s0,s0) ),
inference(resolution,[status(thm)],[c3,neq8]) ).
cnf(c12,plain,
p(s2,s1,s0,s0,s0),
inference(resolution,[status(thm)],[c5,neq7]) ).
cnf(c13,plain,
p(X25,s1,s0,s0,s0),
inference(resolution,[status(thm)],[c12,rule1]) ).
cnf(c17,plain,
( ~ neq(X54,s0)
| ~ neq(X54,X53)
| ~ neq(s1,s0)
| ~ neq(s1,X53)
| p(X54,s1,X53,s0,s0) ),
inference(resolution,[status(thm)],[c13,rule3]) ).
cnf(c51,plain,
( ~ neq(s1,s0)
| ~ neq(s1,X55)
| p(s1,s1,X55,s0,s0) ),
inference(factor,[status(thm)],[c17]) ).
cnf(c56,plain,
( ~ neq(s1,s0)
| p(s1,s1,s2,s0,s0) ),
inference(resolution,[status(thm)],[c51,neq6]) ).
cnf(c58,plain,
p(s1,s1,s2,s0,s0),
inference(resolution,[status(thm)],[c56,neq4]) ).
cnf(c62,plain,
p(X58,s1,s2,s0,s0),
inference(resolution,[status(thm)],[c58,rule1]) ).
cnf(c66,plain,
( ~ neq(X60,s1)
| ~ neq(X60,X61)
| p(X60,X61,s2,s0,s0) ),
inference(resolution,[status(thm)],[c62,rule2]) ).
cnf(c72,plain,
( ~ neq(s0,s1)
| p(s0,s2,s2,s0,s0) ),
inference(resolution,[status(thm)],[c66,neq3]) ).
cnf(c87,plain,
p(s0,s2,s2,s0,s0),
inference(resolution,[status(thm)],[c72,neq2]) ).
cnf(c91,plain,
p(X68,s2,s2,s0,s0),
inference(resolution,[status(thm)],[c87,rule1]) ).
cnf(c93,plain,
( ~ neq(X144,s0)
| ~ neq(X144,X145)
| ~ neq(s2,s0)
| ~ neq(s2,X145)
| p(X144,s2,s2,X145,s0) ),
inference(resolution,[status(thm)],[c91,rule4]) ).
cnf(c205,plain,
( ~ neq(s2,s0)
| ~ neq(s2,X146)
| p(s2,s2,s2,X146,s0) ),
inference(factor,[status(thm)],[c93]) ).
cnf(c210,plain,
( ~ neq(s2,s0)
| p(s2,s2,s2,s1,s0) ),
inference(resolution,[status(thm)],[c205,neq8]) ).
cnf(c212,plain,
p(s2,s2,s2,s1,s0),
inference(resolution,[status(thm)],[c210,neq7]) ).
cnf(c216,plain,
p(X148,s2,s2,s1,s0),
inference(resolution,[status(thm)],[c212,rule1]) ).
cnf(c220,plain,
( ~ neq(X151,s2)
| ~ neq(X151,X152)
| p(X151,X152,s2,s1,s0) ),
inference(resolution,[status(thm)],[c216,rule2]) ).
cnf(c229,plain,
( ~ neq(s1,s2)
| p(s1,s0,s2,s1,s0) ),
inference(resolution,[status(thm)],[c220,neq4]) ).
cnf(c241,plain,
p(s1,s0,s2,s1,s0),
inference(resolution,[status(thm)],[c229,neq6]) ).
cnf(c245,plain,
p(X159,s0,s2,s1,s0),
inference(resolution,[status(thm)],[c241,rule1]) ).
cnf(c251,plain,
( ~ neq(X296,s2)
| ~ neq(X296,X295)
| ~ neq(s0,s2)
| ~ neq(s0,X295)
| p(X296,s0,X295,s1,s0) ),
inference(resolution,[status(thm)],[c245,rule3]) ).
cnf(c450,plain,
( ~ neq(s0,s2)
| ~ neq(s0,X297)
| p(s0,s0,X297,s1,s0) ),
inference(factor,[status(thm)],[c251]) ).
cnf(c456,plain,
( ~ neq(s0,s2)
| p(s0,s0,s1,s1,s0) ),
inference(resolution,[status(thm)],[c450,neq2]) ).
cnf(c457,plain,
p(s0,s0,s1,s1,s0),
inference(resolution,[status(thm)],[c456,neq3]) ).
cnf(c461,plain,
p(X298,s0,s1,s1,s0),
inference(resolution,[status(thm)],[c457,rule1]) ).
cnf(c465,plain,
( ~ neq(X300,s0)
| ~ neq(X300,X301)
| p(X300,X301,s1,s1,s0) ),
inference(resolution,[status(thm)],[c461,rule2]) ).
cnf(c469,plain,
( ~ neq(s2,s0)
| p(s2,s1,s1,s1,s0) ),
inference(resolution,[status(thm)],[c465,neq8]) ).
cnf(c478,plain,
p(s2,s1,s1,s1,s0),
inference(resolution,[status(thm)],[c469,neq7]) ).
cnf(c482,plain,
p(X304,s1,s1,s1,s0),
inference(resolution,[status(thm)],[c478,rule1]) ).
cnf(c485,plain,
( ~ neq(X456,s0)
| ~ neq(X456,X455)
| ~ neq(s1,s0)
| ~ neq(s1,X455)
| p(X456,s1,s1,s1,X455) ),
inference(resolution,[status(thm)],[c482,rule5]) ).
cnf(c720,plain,
( ~ neq(s1,s0)
| ~ neq(s1,X458)
| p(s1,s1,s1,s1,X458) ),
inference(factor,[status(thm)],[c485]) ).
cnf(c728,plain,
( ~ neq(s1,s0)
| p(s1,s1,s1,s1,s2) ),
inference(resolution,[status(thm)],[c720,neq6]) ).
cnf(c730,plain,
p(s1,s1,s1,s1,s2),
inference(resolution,[status(thm)],[c728,neq4]) ).
cnf(c734,plain,
p(X459,s1,s1,s1,s2),
inference(resolution,[status(thm)],[c730,rule1]) ).
cnf(c738,plain,
( ~ neq(X462,s1)
| ~ neq(X462,X463)
| p(X462,X463,s1,s1,s2) ),
inference(resolution,[status(thm)],[c734,rule2]) ).
cnf(c744,plain,
( ~ neq(s0,s1)
| p(s0,s2,s1,s1,s2) ),
inference(resolution,[status(thm)],[c738,neq3]) ).
cnf(c759,plain,
p(s0,s2,s1,s1,s2),
inference(resolution,[status(thm)],[c744,neq2]) ).
cnf(c763,plain,
p(X469,s2,s1,s1,s2),
inference(resolution,[status(thm)],[c759,rule1]) ).
cnf(c769,plain,
( ~ neq(X655,s1)
| ~ neq(X655,X654)
| ~ neq(s2,s1)
| ~ neq(s2,X654)
| p(X655,s2,X654,s1,s2) ),
inference(resolution,[status(thm)],[c763,rule3]) ).
cnf(c998,plain,
( ~ neq(s2,s1)
| ~ neq(s2,X657)
| p(s2,s2,X657,s1,s2) ),
inference(factor,[status(thm)],[c769]) ).
cnf(c1004,plain,
( ~ neq(s2,s1)
| p(s2,s2,s0,s1,s2) ),
inference(resolution,[status(thm)],[c998,neq7]) ).
cnf(c1005,plain,
p(s2,s2,s0,s1,s2),
inference(resolution,[status(thm)],[c1004,neq8]) ).
cnf(c1009,plain,
p(X659,s2,s0,s1,s2),
inference(resolution,[status(thm)],[c1005,rule1]) ).
cnf(c1013,plain,
( ~ neq(X661,s2)
| ~ neq(X661,X662)
| p(X661,X662,s0,s1,s2) ),
inference(resolution,[status(thm)],[c1009,rule2]) ).
cnf(c1022,plain,
( ~ neq(s1,s2)
| p(s1,s0,s0,s1,s2) ),
inference(resolution,[status(thm)],[c1013,neq4]) ).
cnf(c1034,plain,
p(s1,s0,s0,s1,s2),
inference(resolution,[status(thm)],[c1022,neq6]) ).
cnf(c1038,plain,
p(X671,s0,s0,s1,s2),
inference(resolution,[status(thm)],[c1034,rule1]) ).
cnf(c1045,plain,
( ~ neq(X858,s1)
| ~ neq(X858,X859)
| ~ neq(s0,s1)
| ~ neq(s0,X859)
| p(X858,s0,s0,X859,s2) ),
inference(resolution,[status(thm)],[c1038,rule4]) ).
cnf(c1318,plain,
( ~ neq(s0,s1)
| ~ neq(s0,X860)
| p(s0,s0,s0,X860,s2) ),
inference(factor,[status(thm)],[c1045]) ).
cnf(c1323,plain,
( ~ neq(s0,s1)
| p(s0,s0,s0,s2,s2) ),
inference(resolution,[status(thm)],[c1318,neq3]) ).
cnf(c1328,plain,
p(s0,s0,s0,s2,s2),
inference(resolution,[status(thm)],[c1323,neq2]) ).
cnf(c1332,plain,
p(X862,s0,s0,s2,s2),
inference(resolution,[status(thm)],[c1328,rule1]) ).
cnf(c1336,plain,
( ~ neq(X865,s0)
| ~ neq(X865,X866)
| p(X865,X866,s0,s2,s2) ),
inference(resolution,[status(thm)],[c1332,rule2]) ).
cnf(c1340,plain,
( ~ neq(s2,s0)
| p(s2,s1,s0,s2,s2) ),
inference(resolution,[status(thm)],[c1336,neq8]) ).
cnf(c1346,plain,
p(s2,s1,s0,s2,s2),
inference(resolution,[status(thm)],[c1340,neq7]) ).
cnf(c1350,plain,
p(X870,s1,s0,s2,s2),
inference(resolution,[status(thm)],[c1346,rule1]) ).
cnf(c1356,plain,
( ~ neq(X1124,s0)
| ~ neq(X1124,X1123)
| ~ neq(s1,s0)
| ~ neq(s1,X1123)
| p(X1124,s1,X1123,s2,s2) ),
inference(resolution,[status(thm)],[c1350,rule3]) ).
cnf(c1747,plain,
( ~ neq(s1,s0)
| ~ neq(s1,X1125)
| p(s1,s1,X1125,s2,s2) ),
inference(factor,[status(thm)],[c1356]) ).
cnf(c1752,plain,
( ~ neq(s1,s0)
| p(s1,s1,s2,s2,s2) ),
inference(resolution,[status(thm)],[c1747,neq6]) ).
cnf(c1754,plain,
p(s1,s1,s2,s2,s2),
inference(resolution,[status(thm)],[c1752,neq4]) ).
cnf(c1758,plain,
p(X1127,s1,s2,s2,s2),
inference(resolution,[status(thm)],[c1754,rule1]) ).
cnf(c1762,plain,
( ~ neq(X1129,s1)
| ~ neq(X1129,X1130)
| p(X1129,X1130,s2,s2,s2) ),
inference(resolution,[status(thm)],[c1758,rule2]) ).
cnf(c1768,plain,
( ~ neq(s0,s1)
| p(s0,s2,s2,s2,s2) ),
inference(resolution,[status(thm)],[c1762,neq3]) ).
cnf(c1788,plain,
p(s0,s2,s2,s2,s2),
inference(resolution,[status(thm)],[c1768,neq2]) ).
cnf(c1792,plain,
p(X1138,s2,s2,s2,s2),
inference(resolution,[status(thm)],[c1788,rule1]) ).
cnf(c1798,plain,
$false,
inference(resolution,[status(thm)],[c1792,goal]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : PUZ056-2.005 : TPTP v8.1.2. Released v3.5.0.
% 0.07/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.34 % Computer : n023.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:41:23 EDT 2024
% 0.13/0.34 % CPUTime :
% 4.56/4.74 % Version: 1.5
% 4.56/4.74 % SZS status Unsatisfiable
% 4.56/4.74 % SZS output start CNFRefutation
% See solution above
% 4.56/4.74
% 4.56/4.74 % Initial clauses : 16
% 4.56/4.74 % Processed clauses : 438
% 4.56/4.74 % Factors computed : 372
% 4.56/4.74 % Resolvents computed: 1428
% 4.56/4.74 % Tautologies deleted: 0
% 4.56/4.74 % Forward subsumed : 1246
% 4.56/4.74 % Backward subsumed : 139
% 4.56/4.74 % -------- CPU Time ---------
% 4.56/4.74 % User time : 4.370 s
% 4.56/4.74 % System time : 0.020 s
% 4.56/4.74 % Total time : 4.390 s
%------------------------------------------------------------------------------