%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SYN036-3 : TPTP v8.1.2. Released v1.0.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:47:07 EDT 2024
% Result : Unsatisfiable 0.92s 1.13s
% Output : Refutation 0.92s
% Verified :
% SZS Type : Refutation
% Derivation depth : 72
% Number of leaves : 31
% Syntax : Number of clauses : 158 ( 20 unt; 99 nHn; 121 RR)
% Number of literals : 391 ( 0 equ; 93 neg)
% Maximal clause size : 5 ( 2 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 13 ( 12 usr; 9 prp; 0-1 aty)
% Number of functors : 8 ( 8 usr; 6 con; 0-1 aty)
% Number of variables : 55 ( 37 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(clause_23,negated_conjecture,
( ~ n1(X7)
| n2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_23) ).
cnf(clause_25,negated_conjecture,
( ~ p(X21)
| ~ p(s1(X21))
| n1(X21) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_25) ).
cnf(clause_10,negated_conjecture,
( ~ n8
| p(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_10) ).
cnf(clause_9,negated_conjecture,
( ~ p(s8)
| n8 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_9) ).
cnf(clause_26,negated_conjecture,
( p(X24)
| p(s1(X24))
| n1(X24) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_26) ).
cnf(clause_28,negated_conjecture,
( ~ n1(X30)
| p(X30)
| ~ p(X29) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_28) ).
cnf(clause_12,negated_conjecture,
( ~ n7
| p(s7) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_12) ).
cnf(clause_11,negated_conjecture,
( ~ p(X3)
| n7 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_11) ).
cnf(c110,plain,
( p(X32)
| n1(X32)
| n7 ),
inference(resolution,[status(thm)],[clause_26,clause_11]) ).
cnf(c140,plain,
( n1(X33)
| n7 ),
inference(resolution,[status(thm)],[c110,clause_11]) ).
cnf(c144,plain,
( n7
| n2 ),
inference(resolution,[status(thm)],[c140,clause_23]) ).
cnf(clause_21,negated_conjecture,
( ~ q(X6)
| n3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_21) ).
cnf(clause_20,negated_conjecture,
( ~ n4
| q(X5) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_20) ).
cnf(clause_30,negated_conjecture,
( n3
| n4
| n9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_30) ).
cnf(c1,plain,
( n3
| n9
| q(X8) ),
inference(resolution,[status(thm)],[clause_30,clause_20]) ).
cnf(c27,plain,
( n3
| n9 ),
inference(resolution,[status(thm)],[c1,clause_21]) ).
cnf(clause_1,negated_conjecture,
( ~ n2
| ~ n9
| ~ n6
| ~ n10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_1) ).
cnf(clause_34,negated_conjecture,
( n7
| n8
| n10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_34) ).
cnf(c8,plain,
( n7
| n10
| p(X9) ),
inference(resolution,[status(thm)],[clause_34,clause_10]) ).
cnf(c45,plain,
( n7
| n10 ),
inference(resolution,[status(thm)],[c8,clause_11]) ).
cnf(c49,plain,
( n7
| ~ n2
| ~ n9
| ~ n6 ),
inference(resolution,[status(thm)],[c45,clause_1]) ).
cnf(clause_13,negated_conjecture,
( ~ n5(X4)
| n6 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_13) ).
cnf(clause_16,negated_conjecture,
( q(X13)
| q(s5(X13))
| n5(X13) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_16) ).
cnf(c66,plain,
( q(X16)
| n5(X16)
| n3 ),
inference(resolution,[status(thm)],[clause_16,clause_21]) ).
cnf(c78,plain,
( n5(X17)
| n3 ),
inference(resolution,[status(thm)],[c66,clause_21]) ).
cnf(c83,plain,
( n3
| n6 ),
inference(resolution,[status(thm)],[c78,clause_13]) ).
cnf(c89,plain,
( n3
| n7
| ~ n2
| ~ n9 ),
inference(resolution,[status(thm)],[c83,c49]) ).
cnf(c119,plain,
( n3
| n7
| ~ n2 ),
inference(resolution,[status(thm)],[c89,c27]) ).
cnf(c148,plain,
( n7
| n3 ),
inference(resolution,[status(thm)],[c144,c119]) ).
cnf(clause_35,negated_conjecture,
( ~ n7
| n8
| ~ n10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_35) ).
cnf(clause_24,negated_conjecture,
( ~ n2
| n1(s2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_24) ).
cnf(clause_7,negated_conjecture,
( n2
| ~ n9
| ~ n6
| n10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_7) ).
cnf(c91,plain,
( n3
| n2
| ~ n9
| n10 ),
inference(resolution,[status(thm)],[c83,clause_7]) ).
cnf(c123,plain,
( n3
| n2
| n10 ),
inference(resolution,[status(thm)],[c91,c27]) ).
cnf(c126,plain,
( n3
| n10
| n1(s2) ),
inference(resolution,[status(thm)],[c123,clause_24]) ).
cnf(clause_27,negated_conjecture,
( ~ n1(X28)
| ~ p(X28)
| p(X27) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_27) ).
cnf(c150,plain,
( n3
| p(s7) ),
inference(resolution,[status(thm)],[c148,clause_12]) ).
cnf(c165,plain,
( n3
| ~ n1(X43)
| p(X43) ),
inference(resolution,[status(thm)],[c150,clause_28]) ).
cnf(c132,plain,
( n3
| n2
| ~ n7
| n8 ),
inference(resolution,[status(thm)],[c123,clause_35]) ).
cnf(c205,plain,
( n3
| n2
| n8 ),
inference(resolution,[status(thm)],[c132,c144]) ).
cnf(c211,plain,
( n3
| n8
| n1(s2) ),
inference(resolution,[status(thm)],[c205,clause_24]) ).
cnf(c324,plain,
( n3
| n8
| p(s2) ),
inference(resolution,[status(thm)],[c211,c165]) ).
cnf(c394,plain,
( n3
| p(s2)
| p(X103) ),
inference(resolution,[status(thm)],[c324,clause_10]) ).
cnf(c605,plain,
( n3
| p(s2) ),
inference(factor,[status(thm)],[c394]) ).
cnf(c618,plain,
( n3
| ~ n1(s2)
| p(X131) ),
inference(resolution,[status(thm)],[c605,clause_27]) ).
cnf(c699,plain,
( n3
| p(X132)
| n10 ),
inference(resolution,[status(thm)],[c618,c126]) ).
cnf(c709,plain,
( n3
| n10
| n8 ),
inference(resolution,[status(thm)],[c699,clause_9]) ).
cnf(c721,plain,
( n3
| n8
| ~ n7 ),
inference(resolution,[status(thm)],[c709,clause_35]) ).
cnf(c736,plain,
( n3
| n8 ),
inference(resolution,[status(thm)],[c721,c148]) ).
cnf(c740,plain,
( n3
| p(X133) ),
inference(resolution,[status(thm)],[c736,clause_10]) ).
cnf(c743,plain,
( n3
| ~ p(X154)
| n1(X154) ),
inference(resolution,[status(thm)],[c740,clause_25]) ).
cnf(c869,plain,
( n3
| n1(X155) ),
inference(resolution,[status(thm)],[c743,c740]) ).
cnf(c873,plain,
( n3
| n2 ),
inference(resolution,[status(thm)],[c869,clause_23]) ).
cnf(clause_33,negated_conjecture,
( ~ n7
| ~ n8
| n10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_33) ).
cnf(c723,plain,
( n3
| n10
| ~ n7 ),
inference(resolution,[status(thm)],[c709,clause_33]) ).
cnf(c752,plain,
( n3
| n10 ),
inference(resolution,[status(thm)],[c723,c45]) ).
cnf(c766,plain,
( n3
| ~ n2
| ~ n9
| ~ n6 ),
inference(resolution,[status(thm)],[c752,clause_1]) ).
cnf(c900,plain,
( n3
| ~ n2
| ~ n9 ),
inference(resolution,[status(thm)],[c766,c83]) ).
cnf(c912,plain,
( n3
| ~ n2 ),
inference(resolution,[status(thm)],[c900,c27]) ).
cnf(c922,plain,
n3,
inference(resolution,[status(thm)],[c912,c873]) ).
cnf(clause_29,negated_conjecture,
( ~ n3
| ~ n4
| n9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_29) ).
cnf(clause_19,negated_conjecture,
( ~ q(s4)
| n4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_19) ).
cnf(clause_14,negated_conjecture,
( ~ n6
| n5(s6) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_14) ).
cnf(clause_31,negated_conjecture,
( ~ n3
| n4
| ~ n9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_31) ).
cnf(clause_6,negated_conjecture,
( ~ n2
| n9
| n6
| ~ n10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_6) ).
cnf(c51,plain,
( n7
| ~ n2
| n9
| n6 ),
inference(resolution,[status(thm)],[c45,clause_6]) ).
cnf(c149,plain,
( n7
| n9
| n6 ),
inference(resolution,[status(thm)],[c144,c51]) ).
cnf(c159,plain,
( n7
| n6
| ~ n3
| n4 ),
inference(resolution,[status(thm)],[c149,clause_31]) ).
cnf(c264,plain,
( n7
| n6
| n4 ),
inference(resolution,[status(thm)],[c159,c148]) ).
cnf(c273,plain,
( n7
| n4
| n5(s6) ),
inference(resolution,[status(thm)],[c264,clause_14]) ).
cnf(clause_17,negated_conjecture,
( ~ n5(X15)
| ~ q(X15)
| q(X14) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_17) ).
cnf(clause_18,negated_conjecture,
( ~ n5(X19)
| q(X19)
| ~ q(X18) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_18) ).
cnf(clause_22,negated_conjecture,
( ~ n3
| q(s3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_22) ).
cnf(c151,plain,
( n7
| q(s3) ),
inference(resolution,[status(thm)],[c148,clause_22]) ).
cnf(c169,plain,
( n7
| ~ n5(X45)
| q(X45) ),
inference(resolution,[status(thm)],[c151,clause_18]) ).
cnf(c384,plain,
( n7
| n4
| q(s6) ),
inference(resolution,[status(thm)],[c273,c169]) ).
cnf(c420,plain,
( n7
| q(s6)
| q(X109) ),
inference(resolution,[status(thm)],[c384,clause_20]) ).
cnf(c626,plain,
( n7
| q(s6) ),
inference(factor,[status(thm)],[c420]) ).
cnf(c642,plain,
( n7
| ~ n5(s6)
| q(X179) ),
inference(resolution,[status(thm)],[c626,clause_17]) ).
cnf(c960,plain,
( n7
| q(X180)
| n4 ),
inference(resolution,[status(thm)],[c642,c273]) ).
cnf(c964,plain,
( n7
| n4 ),
inference(resolution,[status(thm)],[c960,clause_19]) ).
cnf(c972,plain,
( n7
| ~ n3
| n9 ),
inference(resolution,[status(thm)],[c964,clause_29]) ).
cnf(c984,plain,
( n7
| n9 ),
inference(resolution,[status(thm)],[c972,c922]) ).
cnf(c971,plain,
( n7
| q(X182) ),
inference(resolution,[status(thm)],[c964,clause_20]) ).
cnf(clause_15,negated_conjecture,
( ~ q(X12)
| ~ q(s5(X12))
| n5(X12) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_15) ).
cnf(c976,plain,
( n7
| ~ q(X196)
| n5(X196) ),
inference(resolution,[status(thm)],[c971,clause_15]) ).
cnf(c1017,plain,
( n7
| n5(X197) ),
inference(resolution,[status(thm)],[c976,c971]) ).
cnf(c1021,plain,
( n7
| n6 ),
inference(resolution,[status(thm)],[c1017,clause_13]) ).
cnf(c1024,plain,
( n7
| ~ n2
| ~ n9 ),
inference(resolution,[status(thm)],[c1021,c49]) ).
cnf(c1038,plain,
( n7
| ~ n2 ),
inference(resolution,[status(thm)],[c1024,c984]) ).
cnf(c1045,plain,
n7,
inference(resolution,[status(thm)],[c1038,c144]) ).
cnf(c1057,plain,
p(s7),
inference(resolution,[status(thm)],[c1045,clause_12]) ).
cnf(c1059,plain,
( ~ n1(X202)
| p(X202) ),
inference(resolution,[status(thm)],[c1057,clause_28]) ).
cnf(c1063,plain,
( p(X210)
| p(s1(X210)) ),
inference(resolution,[status(thm)],[c1059,clause_26]) ).
cnf(c1084,plain,
( p(s1(s8))
| n8 ),
inference(resolution,[status(thm)],[c1063,clause_9]) ).
cnf(c1093,plain,
( p(s1(s8))
| p(X259) ),
inference(resolution,[status(thm)],[c1084,clause_10]) ).
cnf(c1109,plain,
p(s1(s8)),
inference(factor,[status(thm)],[c1093]) ).
cnf(c1117,plain,
( ~ p(s8)
| n1(s8) ),
inference(resolution,[status(thm)],[c1109,clause_25]) ).
cnf(clause_4,negated_conjecture,
( n2
| n9
| n6
| n10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_4) ).
cnf(c15,plain,
( n2
| n6
| n10
| ~ n3
| n4 ),
inference(resolution,[status(thm)],[clause_4,clause_31]) ).
cnf(c220,plain,
( n2
| n6
| n10
| n4 ),
inference(resolution,[status(thm)],[c15,c83]) ).
cnf(c337,plain,
( n2
| n6
| n10
| q(X97) ),
inference(resolution,[status(thm)],[c220,clause_20]) ).
cnf(c936,plain,
q(s3),
inference(resolution,[status(thm)],[c922,clause_22]) ).
cnf(c937,plain,
( ~ n5(X167)
| q(X167) ),
inference(resolution,[status(thm)],[c936,clause_18]) ).
cnf(c945,plain,
( q(X178)
| q(s5(X178)) ),
inference(resolution,[status(thm)],[c937,clause_16]) ).
cnf(c947,plain,
( q(s5(s4))
| n4 ),
inference(resolution,[status(thm)],[c945,clause_19]) ).
cnf(c957,plain,
( q(s5(s4))
| q(X243) ),
inference(resolution,[status(thm)],[c947,clause_20]) ).
cnf(c1095,plain,
q(s5(s4)),
inference(factor,[status(thm)],[c957]) ).
cnf(c1104,plain,
( ~ q(s4)
| n5(s4) ),
inference(resolution,[status(thm)],[c1095,clause_15]) ).
cnf(c1107,plain,
( n5(s4)
| n2
| n6
| n10 ),
inference(resolution,[status(thm)],[c1104,c337]) ).
cnf(c1230,plain,
( n2
| n6
| n10 ),
inference(resolution,[status(thm)],[c1107,clause_13]) ).
cnf(c1242,plain,
( n2
| n10
| ~ n9 ),
inference(resolution,[status(thm)],[c1230,clause_7]) ).
cnf(c19,plain,
( n2
| n9
| n6
| ~ n7
| n8 ),
inference(resolution,[status(thm)],[clause_4,clause_35]) ).
cnf(c256,plain,
( n2
| n9
| n6
| n8 ),
inference(resolution,[status(thm)],[c19,c144]) ).
cnf(c357,plain,
( n2
| n9
| n6
| p(X100) ),
inference(resolution,[status(thm)],[c256,clause_10]) ).
cnf(clause_8,negated_conjecture,
( n2
| ~ n9
| n6
| ~ n10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_8) ).
cnf(c1244,plain,
( n2
| n6
| ~ n9 ),
inference(resolution,[status(thm)],[c1230,clause_8]) ).
cnf(c1258,plain,
( n2
| n6
| p(X340) ),
inference(resolution,[status(thm)],[c1244,c357]) ).
cnf(c1278,plain,
( n2
| n6
| n1(s8) ),
inference(resolution,[status(thm)],[c1258,c1117]) ).
cnf(c1316,plain,
( n2
| n6 ),
inference(resolution,[status(thm)],[c1278,clause_23]) ).
cnf(c1318,plain,
( n6
| n1(s2) ),
inference(resolution,[status(thm)],[c1316,clause_24]) ).
cnf(c1324,plain,
( n6
| p(s2) ),
inference(resolution,[status(thm)],[c1318,c1059]) ).
cnf(c1331,plain,
( n6
| ~ n1(s2)
| p(X349) ),
inference(resolution,[status(thm)],[c1324,clause_27]) ).
cnf(c1352,plain,
( n6
| p(X350) ),
inference(resolution,[status(thm)],[c1331,c1318]) ).
cnf(c1358,plain,
( n6
| n8 ),
inference(resolution,[status(thm)],[c1352,clause_9]) ).
cnf(c1363,plain,
( n6
| ~ n7
| n10 ),
inference(resolution,[status(thm)],[c1358,clause_33]) ).
cnf(c1373,plain,
( n6
| n10 ),
inference(resolution,[status(thm)],[c1363,c1045]) ).
cnf(c1379,plain,
( n6
| ~ n2
| n9 ),
inference(resolution,[status(thm)],[c1373,clause_6]) ).
cnf(c1395,plain,
( n6
| n9 ),
inference(resolution,[status(thm)],[c1379,c1316]) ).
cnf(c1398,plain,
( n6
| ~ n3
| n4 ),
inference(resolution,[status(thm)],[c1395,clause_31]) ).
cnf(c1408,plain,
( n6
| n4 ),
inference(resolution,[status(thm)],[c1398,c922]) ).
cnf(c1410,plain,
( n6
| q(X352) ),
inference(resolution,[status(thm)],[c1408,clause_20]) ).
cnf(c1417,plain,
( n6
| n5(s4) ),
inference(resolution,[status(thm)],[c1410,c1104]) ).
cnf(c1428,plain,
n6,
inference(resolution,[status(thm)],[c1417,clause_13]) ).
cnf(c1429,plain,
n5(s6),
inference(resolution,[status(thm)],[c1428,clause_14]) ).
cnf(c1430,plain,
q(s6),
inference(resolution,[status(thm)],[c1429,c937]) ).
cnf(c1432,plain,
( ~ n5(s6)
| q(X360) ),
inference(resolution,[status(thm)],[c1430,clause_17]) ).
cnf(c1433,plain,
q(X361),
inference(resolution,[status(thm)],[c1432,c1429]) ).
cnf(c1434,plain,
n4,
inference(resolution,[status(thm)],[c1433,clause_19]) ).
cnf(c1437,plain,
( ~ n3
| n9 ),
inference(resolution,[status(thm)],[c1434,clause_29]) ).
cnf(c1438,plain,
n9,
inference(resolution,[status(thm)],[c1437,c922]) ).
cnf(c1439,plain,
( n2
| n10 ),
inference(resolution,[status(thm)],[c1438,c1242]) ).
cnf(c1442,plain,
( n2
| ~ n7
| n8 ),
inference(resolution,[status(thm)],[c1439,clause_35]) ).
cnf(c1448,plain,
( n2
| n8 ),
inference(resolution,[status(thm)],[c1442,c1045]) ).
cnf(c1451,plain,
( n2
| p(X364) ),
inference(resolution,[status(thm)],[c1448,clause_10]) ).
cnf(c1456,plain,
( n2
| n1(s8) ),
inference(resolution,[status(thm)],[c1451,c1117]) ).
cnf(c1467,plain,
n2,
inference(resolution,[status(thm)],[c1456,clause_23]) ).
cnf(c1469,plain,
n1(s2),
inference(resolution,[status(thm)],[c1467,clause_24]) ).
cnf(c1470,plain,
p(s2),
inference(resolution,[status(thm)],[c1469,c1059]) ).
cnf(c1472,plain,
( ~ n1(s2)
| p(X367) ),
inference(resolution,[status(thm)],[c1470,clause_27]) ).
cnf(c1473,plain,
p(X368),
inference(resolution,[status(thm)],[c1472,c1469]) ).
cnf(c1475,plain,
n8,
inference(resolution,[status(thm)],[c1473,clause_9]) ).
cnf(c1477,plain,
( ~ n7
| n10 ),
inference(resolution,[status(thm)],[c1475,clause_33]) ).
cnf(c1478,plain,
n10,
inference(resolution,[status(thm)],[c1477,c1045]) ).
cnf(c1479,plain,
( ~ n2
| ~ n9
| ~ n6 ),
inference(resolution,[status(thm)],[c1478,clause_1]) ).
cnf(c1481,plain,
( ~ n2
| ~ n9 ),
inference(resolution,[status(thm)],[c1479,c1428]) ).
cnf(c1482,plain,
~ n2,
inference(resolution,[status(thm)],[c1481,c1438]) ).
cnf(c1483,plain,
$false,
inference(resolution,[status(thm)],[c1482,c1467]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : SYN036-3 : TPTP v8.1.2. Released v1.0.0.
% 0.03/0.12 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.12/0.33 % Computer : n027.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Wed May 8 19:51:23 EDT 2024
% 0.12/0.34 % CPUTime :
% 0.92/1.13 % Version: 1.5
% 0.92/1.13 % SZS status Unsatisfiable
% 0.92/1.13 % SZS output start CNFRefutation
% See solution above
% 0.92/1.13
% 0.92/1.13 % Initial clauses : 36
% 0.92/1.13 % Processed clauses : 275
% 0.92/1.13 % Factors computed : 4
% 0.92/1.13 % Resolvents computed: 1480
% 0.92/1.13 % Tautologies deleted: 66
% 0.92/1.13 % Forward subsumed : 617
% 0.92/1.13 % Backward subsumed : 262
% 0.92/1.13 % -------- CPU Time ---------
% 0.92/1.13 % User time : 0.777 s
% 0.92/1.13 % System time : 0.015 s
% 0.92/1.13 % Total time : 0.792 s
%------------------------------------------------------------------------------