%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SYN037-1 : TPTP v8.1.2. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n004.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.08s
% Output : Refutation 0.92s
% Verified :
% SZS Type : Refutation
% Derivation depth : 82
% Number of leaves : 36
% Syntax : Number of clauses : 162 ( 20 unt; 105 nHn; 126 RR)
% Number of literals : 416 ( 0 equ; 96 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 : 52 ( 36 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(clause_23,negated_conjecture,
( ~ n1(X7)
| n2 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_23) ).
cnf(clause_25,negated_conjecture,
( ~ p(X18)
| ~ p(s1(X18))
| n1(X18) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_25) ).
cnf(clause_20,negated_conjecture,
( ~ n4
| p(X5) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_20) ).
cnf(clause_19,negated_conjecture,
( ~ p(s4)
| n4 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_19) ).
cnf(clause_26,negated_conjecture,
( p(X21)
| p(s1(X21))
| n1(X21) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_26) ).
cnf(clause_28,negated_conjecture,
( ~ n1(X28)
| p(X28)
| ~ p(X27) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_28) ).
cnf(clause_12,negated_conjecture,
( ~ n7
| p(s7) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_12) ).
cnf(clause_36,negated_conjecture,
( n7
| ~ n8
| ~ n10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_36) ).
cnf(clause_11,negated_conjecture,
( ~ p(X3)
| n7 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_11) ).
cnf(c128,plain,
( p(X30)
| n1(X30)
| n7 ),
inference(resolution,[status(thm)],[clause_26,clause_11]) ).
cnf(c152,plain,
( n1(X31)
| n7 ),
inference(resolution,[status(thm)],[c128,clause_11]) ).
cnf(c159,plain,
( n7
| n2 ),
inference(resolution,[status(thm)],[c152,clause_23]) ).
cnf(clause_30,negated_conjecture,
( n3
| n4
| n9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_30) ).
cnf(c1,plain,
( n3
| n9
| p(X8) ),
inference(resolution,[status(thm)],[clause_30,clause_20]) ).
cnf(c27,plain,
( n3
| n9
| n7 ),
inference(resolution,[status(thm)],[c1,clause_11]) ).
cnf(clause_13,negated_conjecture,
( ~ n5(X4)
| n6 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_13) ).
cnf(clause_21,negated_conjecture,
( ~ q(X6)
| n3 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_21) ).
cnf(clause_16,negated_conjecture,
( q(s5(X13))
| q(X13)
| n5(X13) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_16) ).
cnf(c77,plain,
( q(X19)
| n5(X19)
| n3 ),
inference(resolution,[status(thm)],[clause_16,clause_21]) ).
cnf(c106,plain,
( n5(X20)
| n3 ),
inference(resolution,[status(thm)],[c77,clause_21]) ).
cnf(c113,plain,
( n3
| n6 ),
inference(resolution,[status(thm)],[c106,clause_13]) ).
cnf(clause_1,negated_conjecture,
( ~ n2
| ~ n9
| ~ n6
| ~ n10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_1) ).
cnf(clause_10,negated_conjecture,
( ~ n8
| q(X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_10) ).
cnf(clause_34,negated_conjecture,
( n7
| n8
| n10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_34) ).
cnf(c8,plain,
( n7
| n10
| q(X9) ),
inference(resolution,[status(thm)],[clause_34,clause_10]) ).
cnf(c44,plain,
( n7
| n10
| n3 ),
inference(resolution,[status(thm)],[c8,clause_21]) ).
cnf(c46,plain,
( n7
| n3
| ~ n2
| ~ n9
| ~ n6 ),
inference(resolution,[status(thm)],[c44,clause_1]) ).
cnf(c485,plain,
( n7
| n3
| ~ n2
| ~ n9 ),
inference(resolution,[status(thm)],[c46,c113]) ).
cnf(c495,plain,
( n7
| n3
| ~ n2 ),
inference(resolution,[status(thm)],[c485,c27]) ).
cnf(c509,plain,
( n7
| n3 ),
inference(resolution,[status(thm)],[c495,c159]) ).
cnf(clause_31,negated_conjecture,
( ~ n3
| n4
| ~ n9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_31) ).
cnf(clause_5,negated_conjecture,
( ~ n2
| n9
| ~ n6
| n10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_5) ).
cnf(clause_15,negated_conjecture,
( ~ q(s5(X12))
| ~ q(X12)
| n5(X12) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_15) ).
cnf(c65,plain,
( ~ q(X89)
| n5(X89)
| n7
| n10 ),
inference(resolution,[status(thm)],[clause_15,c8]) ).
cnf(c551,plain,
( n5(X90)
| n7
| n10 ),
inference(resolution,[status(thm)],[c65,c8]) ).
cnf(c565,plain,
( n7
| n10
| n6 ),
inference(resolution,[status(thm)],[c551,clause_13]) ).
cnf(c583,plain,
( n7
| n10
| ~ n2
| n9 ),
inference(resolution,[status(thm)],[c565,clause_5]) ).
cnf(c641,plain,
( n7
| n10
| n9 ),
inference(resolution,[status(thm)],[c583,c159]) ).
cnf(c664,plain,
( n7
| n10
| ~ n3
| n4 ),
inference(resolution,[status(thm)],[c641,clause_31]) ).
cnf(c803,plain,
( n7
| n10
| n4 ),
inference(resolution,[status(thm)],[c664,c509]) ).
cnf(c829,plain,
( n7
| n10
| p(X100) ),
inference(resolution,[status(thm)],[c803,clause_20]) ).
cnf(c844,plain,
( n7
| n10 ),
inference(resolution,[status(thm)],[c829,clause_11]) ).
cnf(c853,plain,
( n7
| ~ n8 ),
inference(resolution,[status(thm)],[c844,clause_36]) ).
cnf(clause_9,negated_conjecture,
( ~ q(s8)
| n8 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_9) ).
cnf(clause_14,negated_conjecture,
( ~ n6
| n5(s6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_14) ).
cnf(clause_6,negated_conjecture,
( ~ n2
| n9
| n6
| ~ n10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_6) ).
cnf(c36,plain,
( ~ n2
| n9
| n6
| n7
| n8 ),
inference(resolution,[status(thm)],[clause_6,clause_34]) ).
cnf(c388,plain,
( n9
| n6
| n7
| n8 ),
inference(resolution,[status(thm)],[c36,c159]) ).
cnf(c579,plain,
( n7
| n6
| ~ n8 ),
inference(resolution,[status(thm)],[c565,clause_36]) ).
cnf(c590,plain,
( n7
| n6
| n9 ),
inference(resolution,[status(thm)],[c579,c388]) ).
cnf(c603,plain,
( n7
| n6
| ~ n3
| n4 ),
inference(resolution,[status(thm)],[c590,clause_31]) ).
cnf(c706,plain,
( n7
| n6
| n4 ),
inference(resolution,[status(thm)],[c603,c113]) ).
cnf(c717,plain,
( n7
| n6
| p(X95) ),
inference(resolution,[status(thm)],[c706,clause_20]) ).
cnf(c726,plain,
( n7
| n6 ),
inference(resolution,[status(thm)],[c717,clause_11]) ).
cnf(c734,plain,
( n7
| n5(s6) ),
inference(resolution,[status(thm)],[c726,clause_14]) ).
cnf(clause_18,negated_conjecture,
( ~ n5(X16)
| q(X17)
| ~ q(X16) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_18) ).
cnf(clause_17,negated_conjecture,
( ~ n5(X14)
| ~ q(X15)
| q(X14) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_17) ).
cnf(clause_22,negated_conjecture,
( ~ n3
| q(s3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_22) ).
cnf(c522,plain,
( n7
| q(s3) ),
inference(resolution,[status(thm)],[c509,clause_22]) ).
cnf(c530,plain,
( n7
| ~ n5(X76)
| q(X76) ),
inference(resolution,[status(thm)],[c522,clause_17]) ).
cnf(c760,plain,
( n7
| q(s6) ),
inference(resolution,[status(thm)],[c734,c530]) ).
cnf(c764,plain,
( n7
| ~ n5(s6)
| q(X126) ),
inference(resolution,[status(thm)],[c760,clause_18]) ).
cnf(c933,plain,
( n7
| q(X127) ),
inference(resolution,[status(thm)],[c764,c734]) ).
cnf(c944,plain,
( n7
| n8 ),
inference(resolution,[status(thm)],[c933,clause_9]) ).
cnf(c948,plain,
n7,
inference(resolution,[status(thm)],[c944,c853]) ).
cnf(c949,plain,
p(s7),
inference(resolution,[status(thm)],[c948,clause_12]) ).
cnf(c950,plain,
( ~ n1(X129)
| p(X129) ),
inference(resolution,[status(thm)],[c949,clause_28]) ).
cnf(c953,plain,
( p(X137)
| p(s1(X137)) ),
inference(resolution,[status(thm)],[c950,clause_26]) ).
cnf(c955,plain,
( p(s1(s4))
| n4 ),
inference(resolution,[status(thm)],[c953,clause_19]) ).
cnf(c962,plain,
( p(s1(s4))
| p(X157) ),
inference(resolution,[status(thm)],[c955,clause_20]) ).
cnf(c967,plain,
p(s1(s4)),
inference(factor,[status(thm)],[c962]) ).
cnf(c974,plain,
( ~ p(s4)
| n1(s4) ),
inference(resolution,[status(thm)],[c967,clause_25]) ).
cnf(clause_32,negated_conjecture,
( n3
| ~ n4
| ~ n9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_32) ).
cnf(clause_35,negated_conjecture,
( ~ n7
| n8
| ~ n10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_35) ).
cnf(c116,plain,
( n3
| ~ n2
| n9
| n10 ),
inference(resolution,[status(thm)],[c113,clause_5]) ).
cnf(c982,plain,
( n1(s4)
| n3
| n9 ),
inference(resolution,[status(thm)],[c974,c1]) ).
cnf(c984,plain,
( n3
| n9
| n2 ),
inference(resolution,[status(thm)],[c982,clause_23]) ).
cnf(c1005,plain,
( n3
| n9
| n10 ),
inference(resolution,[status(thm)],[c984,c116]) ).
cnf(c1028,plain,
( n3
| n9
| ~ n7
| n8 ),
inference(resolution,[status(thm)],[c1005,clause_35]) ).
cnf(c1143,plain,
( n3
| n9
| n8 ),
inference(resolution,[status(thm)],[c1028,c948]) ).
cnf(c1152,plain,
( n3
| n9
| q(X175) ),
inference(resolution,[status(thm)],[c1143,clause_10]) ).
cnf(c1167,plain,
( n3
| n9 ),
inference(resolution,[status(thm)],[c1152,clause_21]) ).
cnf(c1178,plain,
( n3
| ~ n4 ),
inference(resolution,[status(thm)],[c1167,clause_32]) ).
cnf(clause_24,negated_conjecture,
( ~ n2
| n1(s2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_24) ).
cnf(clause_7,negated_conjecture,
( n2
| ~ n9
| ~ n6
| n10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_7) ).
cnf(c117,plain,
( n3
| n2
| ~ n9
| n10 ),
inference(resolution,[status(thm)],[c113,clause_7]) ).
cnf(c997,plain,
( n3
| n2
| n10 ),
inference(resolution,[status(thm)],[c984,c117]) ).
cnf(c1010,plain,
( n3
| n2
| ~ n7
| n8 ),
inference(resolution,[status(thm)],[c997,clause_35]) ).
cnf(c1091,plain,
( n3
| n2
| n8 ),
inference(resolution,[status(thm)],[c1010,c948]) ).
cnf(c1094,plain,
( n3
| n2
| q(X173) ),
inference(resolution,[status(thm)],[c1091,clause_10]) ).
cnf(c1098,plain,
( n3
| n2 ),
inference(resolution,[status(thm)],[c1094,clause_21]) ).
cnf(c1105,plain,
( n3
| n1(s2) ),
inference(resolution,[status(thm)],[c1098,clause_24]) ).
cnf(clause_27,negated_conjecture,
( ~ n1(X26)
| ~ p(X26)
| p(X25) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_27) ).
cnf(c1124,plain,
( n3
| p(s2) ),
inference(resolution,[status(thm)],[c1105,c950]) ).
cnf(c1126,plain,
( n3
| ~ n1(s2)
| p(X207) ),
inference(resolution,[status(thm)],[c1124,clause_27]) ).
cnf(c1233,plain,
( n3
| p(X209) ),
inference(resolution,[status(thm)],[c1126,c1105]) ).
cnf(c1237,plain,
( n3
| n4 ),
inference(resolution,[status(thm)],[c1233,clause_19]) ).
cnf(c1243,plain,
n3,
inference(resolution,[status(thm)],[c1237,c1178]) ).
cnf(c1244,plain,
q(s3),
inference(resolution,[status(thm)],[c1243,clause_22]) ).
cnf(c1247,plain,
( ~ n5(X212)
| q(X212) ),
inference(resolution,[status(thm)],[c1244,clause_17]) ).
cnf(c1250,plain,
( q(X220)
| q(s5(X220)) ),
inference(resolution,[status(thm)],[c1247,clause_16]) ).
cnf(c1255,plain,
( q(s5(s8))
| n8 ),
inference(resolution,[status(thm)],[c1250,clause_9]) ).
cnf(c1262,plain,
( q(s5(s8))
| q(X237) ),
inference(resolution,[status(thm)],[c1255,clause_10]) ).
cnf(c1264,plain,
q(s5(s8)),
inference(factor,[status(thm)],[c1262]) ).
cnf(c1272,plain,
( ~ q(s8)
| n5(s8) ),
inference(resolution,[status(thm)],[c1264,clause_15]) ).
cnf(clause_4,negated_conjecture,
( n2
| n9
| n6
| n10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_4) ).
cnf(c19,plain,
( n2
| n9
| n6
| ~ n7
| n8 ),
inference(resolution,[status(thm)],[clause_4,clause_35]) ).
cnf(c284,plain,
( n2
| n9
| n6
| n8 ),
inference(resolution,[status(thm)],[c19,c159]) ).
cnf(c304,plain,
( n2
| n9
| n6
| q(X60) ),
inference(resolution,[status(thm)],[c284,clause_10]) ).
cnf(clause_8,negated_conjecture,
( n2
| ~ n9
| n6
| ~ n10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_8) ).
cnf(c15,plain,
( n2
| n6
| n10
| ~ n3
| n4 ),
inference(resolution,[status(thm)],[clause_4,clause_31]) ).
cnf(c233,plain,
( n2
| n6
| n10
| n4 ),
inference(resolution,[status(thm)],[c15,c113]) ).
cnf(c250,plain,
( n2
| n6
| n10
| p(X59) ),
inference(resolution,[status(thm)],[c233,clause_20]) ).
cnf(c978,plain,
( n1(s4)
| n2
| n6
| n10 ),
inference(resolution,[status(thm)],[c974,c250]) ).
cnf(c1385,plain,
( n2
| n6
| n10 ),
inference(resolution,[status(thm)],[c978,clause_23]) ).
cnf(c1402,plain,
( n2
| n6
| ~ n9 ),
inference(resolution,[status(thm)],[c1385,clause_8]) ).
cnf(c1419,plain,
( n2
| n6
| q(X306) ),
inference(resolution,[status(thm)],[c1402,c304]) ).
cnf(c1432,plain,
( n2
| n6
| n5(s8) ),
inference(resolution,[status(thm)],[c1419,c1272]) ).
cnf(c1464,plain,
( n2
| n6 ),
inference(resolution,[status(thm)],[c1432,clause_13]) ).
cnf(clause_2,negated_conjecture,
( ~ n2
| ~ n9
| n6
| n10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_2) ).
cnf(clause_29,negated_conjecture,
( ~ n3
| ~ n4
| n9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_29) ).
cnf(c1465,plain,
( n6
| n1(s2) ),
inference(resolution,[status(thm)],[c1464,clause_24]) ).
cnf(c1471,plain,
( n6
| p(s2) ),
inference(resolution,[status(thm)],[c1465,c950]) ).
cnf(c1478,plain,
( n6
| ~ n1(s2)
| p(X317) ),
inference(resolution,[status(thm)],[c1471,clause_27]) ).
cnf(c1500,plain,
( n6
| p(X318) ),
inference(resolution,[status(thm)],[c1478,c1465]) ).
cnf(c1505,plain,
( n6
| n4 ),
inference(resolution,[status(thm)],[c1500,clause_19]) ).
cnf(c1511,plain,
( n6
| ~ n3
| n9 ),
inference(resolution,[status(thm)],[c1505,clause_29]) ).
cnf(c1520,plain,
( n6
| n9 ),
inference(resolution,[status(thm)],[c1511,c1243]) ).
cnf(c1525,plain,
( n6
| ~ n2
| n10 ),
inference(resolution,[status(thm)],[c1520,clause_2]) ).
cnf(c1540,plain,
( n6
| n10 ),
inference(resolution,[status(thm)],[c1525,c1464]) ).
cnf(c1543,plain,
( n6
| ~ n7
| n8 ),
inference(resolution,[status(thm)],[c1540,clause_35]) ).
cnf(c1554,plain,
( n6
| n8 ),
inference(resolution,[status(thm)],[c1543,c948]) ).
cnf(c1556,plain,
( n6
| q(X321) ),
inference(resolution,[status(thm)],[c1554,clause_10]) ).
cnf(c1562,plain,
( n6
| n5(s8) ),
inference(resolution,[status(thm)],[c1556,c1272]) ).
cnf(c1575,plain,
n6,
inference(resolution,[status(thm)],[c1562,clause_13]) ).
cnf(clause_3,negated_conjecture,
( n2
| n9
| ~ n6
| ~ n10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_3) ).
cnf(clause_33,negated_conjecture,
( ~ n7
| ~ n8
| n10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_33) ).
cnf(c1576,plain,
n5(s6),
inference(resolution,[status(thm)],[c1575,clause_14]) ).
cnf(c1577,plain,
q(s6),
inference(resolution,[status(thm)],[c1576,c1247]) ).
cnf(c1579,plain,
( ~ n5(s6)
| q(X327) ),
inference(resolution,[status(thm)],[c1577,clause_18]) ).
cnf(c1580,plain,
q(X328),
inference(resolution,[status(thm)],[c1579,c1576]) ).
cnf(c1583,plain,
n8,
inference(resolution,[status(thm)],[c1580,clause_9]) ).
cnf(c1584,plain,
( ~ n7
| n10 ),
inference(resolution,[status(thm)],[c1583,clause_33]) ).
cnf(c1585,plain,
n10,
inference(resolution,[status(thm)],[c1584,c948]) ).
cnf(c1587,plain,
( n2
| n9
| ~ n6 ),
inference(resolution,[status(thm)],[c1585,clause_3]) ).
cnf(c1590,plain,
( n2
| n9 ),
inference(resolution,[status(thm)],[c1587,c1575]) ).
cnf(c1592,plain,
( n2
| ~ n3
| n4 ),
inference(resolution,[status(thm)],[c1590,clause_31]) ).
cnf(c1598,plain,
( n2
| n4 ),
inference(resolution,[status(thm)],[c1592,c1243]) ).
cnf(c1600,plain,
( n2
| p(X331) ),
inference(resolution,[status(thm)],[c1598,clause_20]) ).
cnf(c1603,plain,
( n2
| n1(s4) ),
inference(resolution,[status(thm)],[c1600,c974]) ).
cnf(c1617,plain,
n2,
inference(resolution,[status(thm)],[c1603,clause_23]) ).
cnf(c1586,plain,
( ~ n2
| ~ n9
| ~ n6 ),
inference(resolution,[status(thm)],[c1585,clause_1]) ).
cnf(c1589,plain,
( ~ n2
| ~ n9 ),
inference(resolution,[status(thm)],[c1586,c1575]) ).
cnf(c1619,plain,
n1(s2),
inference(resolution,[status(thm)],[c1617,clause_24]) ).
cnf(c1620,plain,
p(s2),
inference(resolution,[status(thm)],[c1619,c950]) ).
cnf(c1622,plain,
( ~ n1(s2)
| p(X334) ),
inference(resolution,[status(thm)],[c1620,clause_27]) ).
cnf(c1623,plain,
p(X336),
inference(resolution,[status(thm)],[c1622,c1619]) ).
cnf(c1625,plain,
n4,
inference(resolution,[status(thm)],[c1623,clause_19]) ).
cnf(c1627,plain,
( ~ n3
| n9 ),
inference(resolution,[status(thm)],[c1625,clause_29]) ).
cnf(c1628,plain,
n9,
inference(resolution,[status(thm)],[c1627,c1243]) ).
cnf(c1629,plain,
~ n2,
inference(resolution,[status(thm)],[c1628,c1589]) ).
cnf(c1630,plain,
$false,
inference(resolution,[status(thm)],[c1629,c1617]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.13 % Problem : SYN037-1 : TPTP v8.1.2. Released v1.0.0.
% 0.08/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.35 % Computer : n004.cluster.edu
% 0.14/0.35 % Model : x86_64 x86_64
% 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.35 % Memory : 8042.1875MB
% 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.35 % CPULimit : 300
% 0.14/0.35 % WCLimit : 300
% 0.14/0.35 % DateTime : Wed May 8 20:13:23 EDT 2024
% 0.14/0.35 % CPUTime :
% 0.92/1.08 % Version: 1.5
% 0.92/1.08 % SZS status Unsatisfiable
% 0.92/1.08 % SZS output start CNFRefutation
% See solution above
% 0.92/1.08
% 0.92/1.08 % Initial clauses : 36
% 0.92/1.08 % Processed clauses : 280
% 0.92/1.08 % Factors computed : 2
% 0.92/1.08 % Resolvents computed: 1629
% 0.92/1.08 % Tautologies deleted: 78
% 0.92/1.08 % Forward subsumed : 597
% 0.92/1.08 % Backward subsumed : 265
% 0.92/1.08 % -------- CPU Time ---------
% 0.92/1.08 % User time : 0.713 s
% 0.92/1.08 % System time : 0.020 s
% 0.92/1.08 % Total time : 0.733 s
%------------------------------------------------------------------------------