%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : NUM285-1 : TPTP v8.1.2. Released v1.1.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n021.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:35:30 EDT 2024
% Result : Satisfiable 1.50s 1.73s
% Output : Saturation 1.50s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(a0_not_b0_1,negated_conjecture,
( a0
| b0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a0_not_b0_1) ).
cnf(q1_is_b0_plus_b1_2,negated_conjecture,
( ~ q1
| ~ b0
| ~ b1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',q1_is_b0_plus_b1_2) ).
cnf(a1_is_b1_2,negated_conjecture,
( ~ a1
| b1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a1_is_b1_2) ).
cnf(p1_is_a0_plus_a1_1,negated_conjecture,
( ~ p1
| a0
| a1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p1_is_a0_plus_a1_1) ).
cnf(a2_is_b2_2,negated_conjecture,
( ~ a2
| b2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a2_is_b2_2) ).
cnf(p2_is_p1_plus_a2_1,negated_conjecture,
( ~ p2
| p1
| a2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p2_is_p1_plus_a2_1) ).
cnf(p3_is_p2_plus_a3_3,negated_conjecture,
( p3
| p2
| ~ a3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p3_is_p2_plus_a3_3) ).
cnf(a3_is_b3_1,negated_conjecture,
( a3
| ~ b3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a3_is_b3_1) ).
cnf(a2_is_b2_1,negated_conjecture,
( a2
| ~ b2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a2_is_b2_1) ).
cnf(q3_is_q2_plus_b3_2,negated_conjecture,
( ~ q3
| ~ q2
| b3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',q3_is_q2_plus_b3_2) ).
cnf(a3_is_b3_2,negated_conjecture,
( ~ a3
| b3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a3_is_b3_2) ).
cnf(q2_is_q1_plus_b2_4,negated_conjecture,
( q2
| ~ q1
| b2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',q2_is_q1_plus_b2_4) ).
cnf(p3_is_p2_plus_a3_2,negated_conjecture,
( ~ p3
| ~ p2
| a3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p3_is_p2_plus_a3_2) ).
cnf(p2_is_p1_plus_a2_4,negated_conjecture,
( p2
| ~ p1
| a2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p2_is_p1_plus_a2_4) ).
cnf(p1_is_a0_plus_a1_3,negated_conjecture,
( p1
| a0
| ~ a1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p1_is_a0_plus_a1_3) ).
cnf(a1_is_b1_1,negated_conjecture,
( a1
| ~ b1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a1_is_b1_1) ).
cnf(q1_is_b0_plus_b1_4,negated_conjecture,
( q1
| ~ b0
| b1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',q1_is_b0_plus_b1_4) ).
cnf(c11,plain,
( q1
| b1
| a0 ),
inference(resolution,[status(thm)],[q1_is_b0_plus_b1_4,a0_not_b0_1]) ).
cnf(c23,plain,
( q1
| a0
| a1 ),
inference(resolution,[status(thm)],[c11,a1_is_b1_1]) ).
cnf(c48,plain,
( q1
| a0
| p1 ),
inference(resolution,[status(thm)],[c23,p1_is_a0_plus_a1_3]) ).
cnf(a0_not_b0_2,negated_conjecture,
( ~ a0
| ~ b0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a0_not_b0_2) ).
cnf(q1_is_b0_plus_b1_3,negated_conjecture,
( q1
| b0
| ~ b1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',q1_is_b0_plus_b1_3) ).
cnf(p1_is_a0_plus_a1_4,negated_conjecture,
( p1
| ~ a0
| a1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p1_is_a0_plus_a1_4) ).
cnf(c1,plain,
( p1
| a1
| b0 ),
inference(resolution,[status(thm)],[p1_is_a0_plus_a1_4,a0_not_b0_1]) ).
cnf(c14,plain,
( p1
| b0
| b1 ),
inference(resolution,[status(thm)],[c1,a1_is_b1_2]) ).
cnf(c29,plain,
( p1
| b0
| q1 ),
inference(resolution,[status(thm)],[c14,q1_is_b0_plus_b1_3]) ).
cnf(c61,plain,
( p1
| q1
| ~ a0 ),
inference(resolution,[status(thm)],[c29,a0_not_b0_2]) ).
cnf(c79,plain,
( p1
| q1 ),
inference(resolution,[status(thm)],[c61,c48]) ).
cnf(c94,plain,
( q1
| p2
| a2 ),
inference(resolution,[status(thm)],[c79,p2_is_p1_plus_a2_4]) ).
cnf(c100,plain,
( q1
| a2
| ~ p3
| a3 ),
inference(resolution,[status(thm)],[c94,p3_is_p2_plus_a3_2]) ).
cnf(p3_is_p2_plus_a3_4,negated_conjecture,
( p3
| ~ p2
| a3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p3_is_p2_plus_a3_4) ).
cnf(c101,plain,
( q1
| a2
| p3
| a3 ),
inference(resolution,[status(thm)],[c94,p3_is_p2_plus_a3_4]) ).
cnf(c236,plain,
( q1
| a2
| a3 ),
inference(resolution,[status(thm)],[c101,c100]) ).
cnf(c244,plain,
( q1
| a3
| b2 ),
inference(resolution,[status(thm)],[c236,a2_is_b2_2]) ).
cnf(c248,plain,
( a3
| b2
| q2 ),
inference(resolution,[status(thm)],[c244,q2_is_q1_plus_b2_4]) ).
cnf(c263,plain,
( b2
| q2
| b3 ),
inference(resolution,[status(thm)],[c248,a3_is_b3_2]) ).
cnf(c287,plain,
( b2
| b3
| ~ q3 ),
inference(resolution,[status(thm)],[c263,q3_is_q2_plus_b3_2]) ).
cnf(q3_is_q2_plus_b3_4,negated_conjecture,
( q3
| ~ q2
| b3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',q3_is_q2_plus_b3_4) ).
cnf(c289,plain,
( b2
| b3
| q3 ),
inference(resolution,[status(thm)],[c263,q3_is_q2_plus_b3_4]) ).
cnf(c339,plain,
( b2
| b3 ),
inference(resolution,[status(thm)],[c289,c287]) ).
cnf(c342,plain,
( b3
| a2 ),
inference(resolution,[status(thm)],[c339,a2_is_b2_1]) ).
cnf(c346,plain,
( a2
| a3 ),
inference(resolution,[status(thm)],[c342,a3_is_b3_1]) ).
cnf(c358,plain,
( a2
| p3
| p2 ),
inference(resolution,[status(thm)],[c346,p3_is_p2_plus_a3_3]) ).
cnf(c499,plain,
( a2
| p3
| p1 ),
inference(resolution,[status(thm)],[c358,p2_is_p1_plus_a2_1]) ).
cnf(c606,plain,
( p3
| p1
| b2 ),
inference(resolution,[status(thm)],[c499,a2_is_b2_2]) ).
cnf(c696,plain,
( p3
| b2
| a0
| a1 ),
inference(resolution,[status(thm)],[c606,p1_is_a0_plus_a1_1]) ).
cnf(c1210,plain,
( p3
| b2
| a0
| b1 ),
inference(resolution,[status(thm)],[c696,a1_is_b1_2]) ).
cnf(c1570,plain,
( p3
| b2
| a0
| ~ q1
| ~ b0 ),
inference(resolution,[status(thm)],[c1210,q1_is_b0_plus_b1_2]) ).
cnf(c1898,plain,
( p3
| b2
| a0
| ~ q1 ),
inference(resolution,[status(thm)],[c1570,a0_not_b0_1]) ).
cnf(q2_is_q1_plus_b2_2,negated_conjecture,
( ~ q2
| ~ q1
| ~ b2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',q2_is_q1_plus_b2_2) ).
cnf(c1559,plain,
( p3
| a0
| b1
| ~ q2
| ~ q1 ),
inference(resolution,[status(thm)],[c1210,q2_is_q1_plus_b2_2]) ).
cnf(c1886,plain,
( p3
| a0
| b1
| ~ q2 ),
inference(resolution,[status(thm)],[c1559,c11]) ).
cnf(p1_is_a0_plus_a1_2,negated_conjecture,
( ~ p1
| ~ a0
| ~ a1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p1_is_a0_plus_a1_2) ).
cnf(q1_is_b0_plus_b1_1,negated_conjecture,
( ~ q1
| b0
| b1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',q1_is_b0_plus_b1_1) ).
cnf(q2_is_q1_plus_b2_1,negated_conjecture,
( ~ q2
| q1
| b2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',q2_is_q1_plus_b2_1) ).
cnf(q3_is_q2_plus_b3_3,negated_conjecture,
( q3
| q2
| ~ b3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',q3_is_q2_plus_b3_3) ).
cnf(c290,plain,
( b2
| q2
| q3 ),
inference(resolution,[status(thm)],[c263,q3_is_q2_plus_b3_3]) ).
cnf(c364,plain,
( b2
| q3
| q1 ),
inference(resolution,[status(thm)],[c290,q2_is_q1_plus_b2_1]) ).
cnf(c502,plain,
( q3
| q1
| a2 ),
inference(resolution,[status(thm)],[c364,a2_is_b2_1]) ).
cnf(c630,plain,
( q3
| a2
| b0
| b1 ),
inference(resolution,[status(thm)],[c502,q1_is_b0_plus_b1_1]) ).
cnf(c1045,plain,
( q3
| a2
| b0
| a1 ),
inference(resolution,[status(thm)],[c630,a1_is_b1_1]) ).
cnf(c1551,plain,
( q3
| a2
| b0
| ~ p1
| ~ a0 ),
inference(resolution,[status(thm)],[c1045,p1_is_a0_plus_a1_2]) ).
cnf(c1870,plain,
( q3
| a2
| b0
| ~ p1 ),
inference(resolution,[status(thm)],[c1551,a0_not_b0_1]) ).
cnf(p2_is_p1_plus_a2_2,negated_conjecture,
( ~ p2
| ~ p1
| ~ a2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p2_is_p1_plus_a2_2) ).
cnf(c1547,plain,
( q3
| b0
| a1
| ~ p2
| ~ p1 ),
inference(resolution,[status(thm)],[c1045,p2_is_p1_plus_a2_2]) ).
cnf(c1850,plain,
( q3
| b0
| a1
| ~ p2 ),
inference(resolution,[status(thm)],[c1547,c1]) ).
cnf(c612,plain,
( a2
| p3
| a0
| a1 ),
inference(resolution,[status(thm)],[c499,p1_is_a0_plus_a1_1]) ).
cnf(c1032,plain,
( a2
| p3
| a0
| b1 ),
inference(resolution,[status(thm)],[c612,a1_is_b1_2]) ).
cnf(c1533,plain,
( a2
| p3
| a0
| ~ q1
| ~ b0 ),
inference(resolution,[status(thm)],[c1032,q1_is_b0_plus_b1_2]) ).
cnf(c1832,plain,
( a2
| p3
| a0
| ~ q1 ),
inference(resolution,[status(thm)],[c1533,a0_not_b0_1]) ).
cnf(c1524,plain,
( p3
| a0
| b1
| ~ p2
| ~ p1 ),
inference(resolution,[status(thm)],[c1032,p2_is_p1_plus_a2_2]) ).
cnf(c507,plain,
( b2
| q3
| b0
| b1 ),
inference(resolution,[status(thm)],[c364,q1_is_b0_plus_b1_1]) ).
cnf(c999,plain,
( b2
| q3
| b0
| a1 ),
inference(resolution,[status(thm)],[c507,a1_is_b1_1]) ).
cnf(c1520,plain,
( b2
| q3
| b0
| ~ p1
| ~ a0 ),
inference(resolution,[status(thm)],[c999,p1_is_a0_plus_a1_2]) ).
cnf(c1812,plain,
( b2
| q3
| b0
| ~ p1 ),
inference(resolution,[status(thm)],[c1520,a0_not_b0_1]) ).
cnf(c1515,plain,
( q3
| b0
| a1
| ~ q2
| ~ q1 ),
inference(resolution,[status(thm)],[c999,q2_is_q1_plus_b2_2]) ).
cnf(c1197,plain,
( p3
| a0
| a1
| ~ q2
| ~ q1 ),
inference(resolution,[status(thm)],[c696,q2_is_q1_plus_b2_2]) ).
cnf(c1785,plain,
( p3
| a0
| a1
| ~ q2 ),
inference(resolution,[status(thm)],[c1197,c23]) ).
cnf(c1039,plain,
( q3
| b0
| b1
| ~ p2
| ~ p1 ),
inference(resolution,[status(thm)],[c630,p2_is_p1_plus_a2_2]) ).
cnf(c1768,plain,
( q3
| b0
| b1
| ~ p2 ),
inference(resolution,[status(thm)],[c1039,c14]) ).
cnf(q2_is_q1_plus_b2_3,negated_conjecture,
( q2
| q1
| ~ b2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',q2_is_q1_plus_b2_3) ).
cnf(c251,plain,
( q1
| b2
| b3 ),
inference(resolution,[status(thm)],[c244,a3_is_b3_2]) ).
cnf(c272,plain,
( q1
| b3
| q2 ),
inference(resolution,[status(thm)],[c251,q2_is_q1_plus_b2_3]) ).
cnf(c304,plain,
( q1
| b3
| ~ q3 ),
inference(resolution,[status(thm)],[c272,q3_is_q2_plus_b3_2]) ).
cnf(c306,plain,
( q1
| b3
| q3 ),
inference(resolution,[status(thm)],[c272,q3_is_q2_plus_b3_4]) ).
cnf(c386,plain,
( q1
| b3 ),
inference(resolution,[status(thm)],[c306,c304]) ).
cnf(p2_is_p1_plus_a2_3,negated_conjecture,
( p2
| p1
| ~ a2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p2_is_p1_plus_a2_3) ).
cnf(c355,plain,
( a3
| p2
| p1 ),
inference(resolution,[status(thm)],[c346,p2_is_p1_plus_a2_3]) ).
cnf(c477,plain,
( a3
| p1
| ~ p3 ),
inference(resolution,[status(thm)],[c355,p3_is_p2_plus_a3_2]) ).
cnf(c478,plain,
( a3
| p1
| p3 ),
inference(resolution,[status(thm)],[c355,p3_is_p2_plus_a3_4]) ).
cnf(c562,plain,
( a3
| p1 ),
inference(resolution,[status(thm)],[c478,c477]) ).
cnf(c566,plain,
( p1
| b3 ),
inference(resolution,[status(thm)],[c562,a3_is_b3_2]) ).
cnf(c574,plain,
( b3
| a0
| a1 ),
inference(resolution,[status(thm)],[c566,p1_is_a0_plus_a1_1]) ).
cnf(c388,plain,
( b3
| b0
| b1 ),
inference(resolution,[status(thm)],[c386,q1_is_b0_plus_b1_1]) ).
cnf(c514,plain,
( b3
| b0
| a1 ),
inference(resolution,[status(thm)],[c388,a1_is_b1_1]) ).
cnf(c643,plain,
( b3
| a1
| ~ a0 ),
inference(resolution,[status(thm)],[c514,a0_not_b0_2]) ).
cnf(c714,plain,
( b3
| a1 ),
inference(resolution,[status(thm)],[c643,c574]) ).
cnf(c722,plain,
( b3
| b1 ),
inference(resolution,[status(thm)],[c714,a1_is_b1_2]) ).
cnf(c733,plain,
( b3
| ~ q1
| ~ b0 ),
inference(resolution,[status(thm)],[c722,q1_is_b0_plus_b1_2]) ).
cnf(c723,plain,
( b3
| ~ p1
| ~ a0 ),
inference(resolution,[status(thm)],[c714,p1_is_a0_plus_a1_2]) ).
cnf(c753,plain,
( b3
| ~ p1
| b0 ),
inference(resolution,[status(thm)],[c723,a0_not_b0_1]) ).
cnf(c806,plain,
( b3
| b0 ),
inference(resolution,[status(thm)],[c753,c566]) ).
cnf(c823,plain,
( b3
| ~ q1 ),
inference(resolution,[status(thm)],[c806,c733]) ).
cnf(c838,plain,
b3,
inference(resolution,[status(thm)],[c823,c386]) ).
cnf(c849,plain,
( q3
| q2 ),
inference(resolution,[status(thm)],[c838,q3_is_q2_plus_b3_3]) ).
cnf(c698,plain,
( p3
| p1
| ~ q2
| ~ q1 ),
inference(resolution,[status(thm)],[c606,q2_is_q1_plus_b2_2]) ).
cnf(c1225,plain,
( p3
| p1
| ~ q2 ),
inference(resolution,[status(thm)],[c698,c79]) ).
cnf(c1241,plain,
( p3
| p1
| q3 ),
inference(resolution,[status(thm)],[c1225,c849]) ).
cnf(c850,plain,
a3,
inference(resolution,[status(thm)],[c838,a3_is_b3_1]) ).
cnf(c851,plain,
( p3
| p2 ),
inference(resolution,[status(thm)],[c850,p3_is_p2_plus_a3_3]) ).
cnf(c633,plain,
( q3
| q1
| ~ p2
| ~ p1 ),
inference(resolution,[status(thm)],[c502,p2_is_p1_plus_a2_2]) ).
cnf(c1054,plain,
( q3
| q1
| ~ p2 ),
inference(resolution,[status(thm)],[c633,c79]) ).
cnf(c1064,plain,
( q3
| q1
| p3 ),
inference(resolution,[status(thm)],[c1054,c851]) ).
cnf(c1098,plain,
( q3
| p3
| b0
| b1 ),
inference(resolution,[status(thm)],[c1064,q1_is_b0_plus_b1_1]) ).
cnf(c1554,plain,
( q3
| p3
| b1
| ~ a0 ),
inference(resolution,[status(thm)],[c1098,a0_not_b0_2]) ).
cnf(c1266,plain,
( p3
| q3
| a0
| a1 ),
inference(resolution,[status(thm)],[c1241,p1_is_a0_plus_a1_1]) ).
cnf(c1580,plain,
( p3
| q3
| a0
| b1 ),
inference(resolution,[status(thm)],[c1266,a1_is_b1_2]) ).
cnf(c1667,plain,
( p3
| q3
| b1 ),
inference(resolution,[status(thm)],[c1580,c1554]) ).
cnf(c1678,plain,
( p3
| q3
| a1 ),
inference(resolution,[status(thm)],[c1667,a1_is_b1_1]) ).
cnf(c1680,plain,
( p3
| q3
| ~ p1
| ~ a0 ),
inference(resolution,[status(thm)],[c1678,p1_is_a0_plus_a1_2]) ).
cnf(c1677,plain,
( p3
| q3
| ~ q1
| ~ b0 ),
inference(resolution,[status(thm)],[c1667,q1_is_b0_plus_b1_2]) ).
cnf(c1721,plain,
( p3
| q3
| ~ q1
| a0 ),
inference(resolution,[status(thm)],[c1677,a0_not_b0_1]) ).
cnf(c1747,plain,
( p3
| q3
| a0 ),
inference(resolution,[status(thm)],[c1721,c1064]) ).
cnf(c1754,plain,
( p3
| q3
| ~ p1 ),
inference(resolution,[status(thm)],[c1747,c1680]) ).
cnf(c1763,plain,
( p3
| q3 ),
inference(resolution,[status(thm)],[c1754,c1241]) ).
cnf(c96,plain,
( p1
| q2
| b2 ),
inference(resolution,[status(thm)],[c79,q2_is_q1_plus_b2_4]) ).
cnf(c113,plain,
( p1
| q2
| a2 ),
inference(resolution,[status(thm)],[c96,a2_is_b2_1]) ).
cnf(c138,plain,
( p1
| q2
| p2 ),
inference(resolution,[status(thm)],[c113,p2_is_p1_plus_a2_3]) ).
cnf(c104,plain,
( q1
| p2
| b2 ),
inference(resolution,[status(thm)],[c94,a2_is_b2_2]) ).
cnf(c130,plain,
( q1
| p2
| q2 ),
inference(resolution,[status(thm)],[c104,q2_is_q1_plus_b2_3]) ).
cnf(c151,plain,
( p2
| q2
| b0
| b1 ),
inference(resolution,[status(thm)],[c130,q1_is_b0_plus_b1_1]) ).
cnf(c706,plain,
( p2
| q2
| b1
| ~ a0 ),
inference(resolution,[status(thm)],[c151,a0_not_b0_2]) ).
cnf(c168,plain,
( q2
| p2
| a0
| a1 ),
inference(resolution,[status(thm)],[c138,p1_is_a0_plus_a1_1]) ).
cnf(c858,plain,
( q2
| p2
| a0
| b1 ),
inference(resolution,[status(thm)],[c168,a1_is_b1_2]) ).
cnf(c1464,plain,
( q2
| p2
| b1 ),
inference(resolution,[status(thm)],[c858,c706]) ).
cnf(c1479,plain,
( q2
| p2
| a1 ),
inference(resolution,[status(thm)],[c1464,a1_is_b1_1]) ).
cnf(c1485,plain,
( q2
| p2
| ~ p1
| ~ a0 ),
inference(resolution,[status(thm)],[c1479,p1_is_a0_plus_a1_2]) ).
cnf(c1478,plain,
( q2
| p2
| ~ q1
| ~ b0 ),
inference(resolution,[status(thm)],[c1464,q1_is_b0_plus_b1_2]) ).
cnf(c1585,plain,
( q2
| p2
| ~ q1
| a0 ),
inference(resolution,[status(thm)],[c1478,a0_not_b0_1]) ).
cnf(c1687,plain,
( q2
| p2
| a0 ),
inference(resolution,[status(thm)],[c1585,c130]) ).
cnf(c1705,plain,
( q2
| p2
| ~ p1 ),
inference(resolution,[status(thm)],[c1687,c1485]) ).
cnf(c1710,plain,
( q2
| p2 ),
inference(resolution,[status(thm)],[c1705,c138]) ).
cnf(c1549,plain,
( q3
| a2
| a1
| ~ a0 ),
inference(resolution,[status(thm)],[c1045,a0_not_b0_2]) ).
cnf(c1518,plain,
( b2
| q3
| a1
| ~ a0 ),
inference(resolution,[status(thm)],[c999,a0_not_b0_2]) ).
cnf(c1042,plain,
( q3
| a2
| b1
| ~ a0 ),
inference(resolution,[status(thm)],[c630,a0_not_b0_2]) ).
cnf(c996,plain,
( b2
| q3
| b1
| ~ a0 ),
inference(resolution,[status(thm)],[c507,a0_not_b0_2]) ).
cnf(c19,plain,
( b1
| a0
| q2
| b2 ),
inference(resolution,[status(thm)],[c11,q2_is_q1_plus_b2_4]) ).
cnf(c93,plain,
( b1
| a0
| q2
| a2 ),
inference(resolution,[status(thm)],[c19,a2_is_b2_1]) ).
cnf(c217,plain,
( a0
| q2
| a2
| ~ q1
| ~ b0 ),
inference(resolution,[status(thm)],[c93,q1_is_b0_plus_b1_2]) ).
cnf(c986,plain,
( a0
| q2
| a2
| ~ q1 ),
inference(resolution,[status(thm)],[c217,a0_not_b0_1]) ).
cnf(c12,plain,
( a1
| b0
| p2
| a2 ),
inference(resolution,[status(thm)],[c1,p2_is_p1_plus_a2_4]) ).
cnf(c41,plain,
( a1
| b0
| p2
| b2 ),
inference(resolution,[status(thm)],[c12,a2_is_b2_2]) ).
cnf(c180,plain,
( b0
| p2
| b2
| ~ p1
| ~ a0 ),
inference(resolution,[status(thm)],[c41,p1_is_a0_plus_a1_2]) ).
cnf(c894,plain,
( b0
| p2
| b2
| ~ p1 ),
inference(resolution,[status(thm)],[c180,a0_not_b0_1]) ).
cnf(q4_is_q3_plus_b4_3,negated_conjecture,
( q4
| q3
| ~ b4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',q4_is_q3_plus_b4_3) ).
cnf(a4_is_b4_2,negated_conjecture,
( ~ a4
| b4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a4_is_b4_2) ).
cnf(a4_is_b4_1,negated_conjecture,
( a4
| ~ b4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a4_is_b4_1) ).
cnf(q4_is_q3_plus_b4_2,negated_conjecture,
( ~ q4
| ~ q3
| b4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',q4_is_q3_plus_b4_2) ).
cnf(p4_is_p3_plus_a4_4,negated_conjecture,
( p4
| ~ p3
| a4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p4_is_p3_plus_a4_4) ).
cnf(c864,plain,
( p2
| p4
| a4 ),
inference(resolution,[status(thm)],[c851,p4_is_p3_plus_a4_4]) ).
cnf(p4_is_p3_plus_a4_2,negated_conjecture,
( ~ p4
| ~ p3
| a4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p4_is_p3_plus_a4_2) ).
cnf(c865,plain,
( p2
| ~ p4
| a4 ),
inference(resolution,[status(thm)],[c851,p4_is_p3_plus_a4_2]) ).
cnf(c882,plain,
( p2
| a4 ),
inference(resolution,[status(thm)],[c865,c864]) ).
cnf(c885,plain,
( p2
| b4 ),
inference(resolution,[status(thm)],[c882,a4_is_b4_2]) ).
cnf(c1059,plain,
( q3
| q1
| b4 ),
inference(resolution,[status(thm)],[c1054,c885]) ).
cnf(c1074,plain,
( q1
| b4
| ~ q4 ),
inference(resolution,[status(thm)],[c1059,q4_is_q3_plus_b4_2]) ).
cnf(q4_is_q3_plus_b4_4,negated_conjecture,
( q4
| ~ q3
| b4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',q4_is_q3_plus_b4_4) ).
cnf(c1075,plain,
( q1
| b4
| q4 ),
inference(resolution,[status(thm)],[c1059,q4_is_q3_plus_b4_4]) ).
cnf(c1108,plain,
( q1
| b4 ),
inference(resolution,[status(thm)],[c1075,c1074]) ).
cnf(c1114,plain,
( q1
| a4 ),
inference(resolution,[status(thm)],[c1108,a4_is_b4_1]) ).
cnf(c1117,plain,
( a4
| b0
| b1 ),
inference(resolution,[status(thm)],[c1114,q1_is_b0_plus_b1_1]) ).
cnf(c1135,plain,
( a4
| b0
| a1 ),
inference(resolution,[status(thm)],[c1117,a1_is_b1_1]) ).
cnf(c1172,plain,
( a4
| a1
| ~ a0 ),
inference(resolution,[status(thm)],[c1135,a0_not_b0_2]) ).
cnf(p4_is_p3_plus_a4_3,negated_conjecture,
( p4
| p3
| ~ a4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p4_is_p3_plus_a4_3) ).
cnf(c861,plain,
( q2
| ~ q4
| b4 ),
inference(resolution,[status(thm)],[c849,q4_is_q3_plus_b4_2]) ).
cnf(c862,plain,
( q2
| q4
| b4 ),
inference(resolution,[status(thm)],[c849,q4_is_q3_plus_b4_4]) ).
cnf(c869,plain,
( q2
| b4 ),
inference(resolution,[status(thm)],[c862,c861]) ).
cnf(c874,plain,
( q2
| a4 ),
inference(resolution,[status(thm)],[c869,a4_is_b4_1]) ).
cnf(c876,plain,
( q2
| p4
| p3 ),
inference(resolution,[status(thm)],[c874,p4_is_p3_plus_a4_3]) ).
cnf(c1226,plain,
( p3
| p1
| p4 ),
inference(resolution,[status(thm)],[c1225,c876]) ).
cnf(c1242,plain,
( p1
| p4
| a4 ),
inference(resolution,[status(thm)],[c1226,p4_is_p3_plus_a4_4]) ).
cnf(c1237,plain,
( p3
| p1
| a4 ),
inference(resolution,[status(thm)],[c1225,c874]) ).
cnf(c1256,plain,
( p1
| a4
| ~ p4 ),
inference(resolution,[status(thm)],[c1237,p4_is_p3_plus_a4_2]) ).
cnf(c1278,plain,
( p1
| a4 ),
inference(resolution,[status(thm)],[c1256,c1242]) ).
cnf(c1281,plain,
( a4
| a0
| a1 ),
inference(resolution,[status(thm)],[c1278,p1_is_a0_plus_a1_1]) ).
cnf(c1291,plain,
( a4
| a1 ),
inference(resolution,[status(thm)],[c1281,c1172]) ).
cnf(c1307,plain,
( a4
| b1 ),
inference(resolution,[status(thm)],[c1291,a1_is_b1_2]) ).
cnf(c1318,plain,
( a4
| ~ q1
| ~ b0 ),
inference(resolution,[status(thm)],[c1307,q1_is_b0_plus_b1_2]) ).
cnf(c1308,plain,
( a4
| ~ p1
| ~ a0 ),
inference(resolution,[status(thm)],[c1291,p1_is_a0_plus_a1_2]) ).
cnf(c1344,plain,
( a4
| ~ p1
| b0 ),
inference(resolution,[status(thm)],[c1308,a0_not_b0_1]) ).
cnf(c1402,plain,
( a4
| b0 ),
inference(resolution,[status(thm)],[c1344,c1278]) ).
cnf(c1413,plain,
( a4
| ~ q1 ),
inference(resolution,[status(thm)],[c1402,c1318]) ).
cnf(c1425,plain,
a4,
inference(resolution,[status(thm)],[c1413,c1114]) ).
cnf(c1436,plain,
b4,
inference(resolution,[status(thm)],[c1425,a4_is_b4_2]) ).
cnf(c1437,plain,
( q4
| q3 ),
inference(resolution,[status(thm)],[c1436,q4_is_q3_plus_b4_3]) ).
cnf(c1435,plain,
( p4
| p3 ),
inference(resolution,[status(thm)],[c1425,p4_is_p3_plus_a4_3]) ).
cnf(c25,plain,
( b0
| b1
| p2
| a2 ),
inference(resolution,[status(thm)],[c14,p2_is_p1_plus_a2_4]) ).
cnf(c123,plain,
( b0
| b1
| p2
| b2 ),
inference(resolution,[status(thm)],[c25,a2_is_b2_2]) ).
cnf(c530,plain,
( b1
| p2
| b2
| ~ a0 ),
inference(resolution,[status(thm)],[c123,a0_not_b0_2]) ).
cnf(c227,plain,
( b1
| a0
| q2
| ~ p2
| ~ p1 ),
inference(resolution,[status(thm)],[c93,p2_is_p1_plus_a2_2]) ).
cnf(c188,plain,
( a1
| b0
| p2
| ~ q2
| ~ q1 ),
inference(resolution,[status(thm)],[c41,q2_is_q1_plus_b2_2]) ).
cnf(c182,plain,
( a1
| p2
| b2
| ~ a0 ),
inference(resolution,[status(thm)],[c41,a0_not_b0_2]) ).
cnf(c134,plain,
( q2
| a2
| a0
| a1 ),
inference(resolution,[status(thm)],[c113,p1_is_a0_plus_a1_1]) ).
cnf(c114,plain,
( b1
| p2
| a2
| ~ a0 ),
inference(resolution,[status(thm)],[c25,a0_not_b0_2]) ).
cnf(c43,plain,
( a0
| a1
| q2
| b2 ),
inference(resolution,[status(thm)],[c23,q2_is_q1_plus_b2_4]) ).
cnf(c35,plain,
( a1
| p2
| a2
| ~ a0 ),
inference(resolution,[status(thm)],[c12,a0_not_b0_2]) ).
cnf(c27,plain,
( p1
| b1
| ~ a0 ),
inference(resolution,[status(thm)],[c14,a0_not_b0_2]) ).
cnf(a5_is_b5_2,negated_conjecture,
( ~ a5
| b5 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a5_is_b5_2) ).
cnf(equal_sum_2,negated_conjecture,
p5,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',equal_sum_2) ).
cnf(p5_is_p4_plus_a5_1,negated_conjecture,
( ~ p5
| p4
| a5 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p5_is_p4_plus_a5_1) ).
cnf(c2,plain,
( p4
| a5 ),
inference(resolution,[status(thm)],[p5_is_p4_plus_a5_1,equal_sum_2]) ).
cnf(p5_is_p4_plus_a5_2,negated_conjecture,
( ~ p5
| ~ p4
| a5 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p5_is_p4_plus_a5_2) ).
cnf(c7,plain,
( ~ p5
| a5 ),
inference(resolution,[status(thm)],[p5_is_p4_plus_a5_2,c2]) ).
cnf(c9,plain,
a5,
inference(resolution,[status(thm)],[c7,equal_sum_2]) ).
cnf(c10,plain,
b5,
inference(resolution,[status(thm)],[c9,a5_is_b5_2]) ).
cnf(equal_sum_1,negated_conjecture,
q5,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',equal_sum_1) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.09/0.14 % Problem : NUM285-1 : TPTP v8.1.2. Released v1.1.0.
% 0.09/0.15 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.16/0.37 % Computer : n021.cluster.edu
% 0.16/0.37 % Model : x86_64 x86_64
% 0.16/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.37 % Memory : 8042.1875MB
% 0.16/0.37 % OS : Linux 3.10.0-693.el7.x86_64
% 0.16/0.37 % CPULimit : 300
% 0.16/0.37 % WCLimit : 300
% 0.16/0.37 % DateTime : Wed May 8 16:02:38 EDT 2024
% 0.16/0.37 % CPUTime :
% 1.50/1.73 % Version: 1.5
% 1.50/1.73 % SZS status Satisfiable
% 1.50/1.73 % SZS output start Saturation
% See solution above
% 1.50/1.73
% 1.50/1.73 % Initial clauses : 54
% 1.50/1.73 % Processed clauses : 299
% 1.50/1.73 % Factors computed : 0
% 1.50/1.73 % Resolvents computed: 1914
% 1.50/1.73 % Tautologies deleted: 81
% 1.50/1.73 % Forward subsumed : 1588
% 1.50/1.73 % Backward subsumed : 209
% 1.50/1.73 % -------- CPU Time ---------
% 1.50/1.73 % User time : 1.321 s
% 1.50/1.73 % System time : 0.014 s
% 1.50/1.73 % Total time : 1.335 s
%------------------------------------------------------------------------------