%------------------------------------------------------------------------------
% File : E---3.5.1
% Problem : SYN798-1 : TPTP v9.3.1. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n002.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 03:26:49 PM UTC 2026
% Result : Satisfiable 52.85s 23.21s
% Output : Saturation 52.85s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named c_0_458ERROR: Could not build tree for root c_0_488ERROR: MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(c_0_52,negated_conjecture,
( ~ ssRr(X3,X5)
| ~ ssRr(X3,X4)
| ~ ssRr(X3,X1)
| ~ ssPv1(X2)
| ~ ssRr(X1,X2)
| ssPv3(X3)
| ssPv1(X5)
| ssPv4(X4) ),
c_0_51,
[final] ).
cnf(c_0_53,negated_conjecture,
ssRr(X1,skf2(X1)),
clause2,
[final] ).
cnf(c_0_56,negated_conjecture,
( ~ ssRr(X4,X3)
| ~ ssRr(X2,X4)
| ~ ssRr(X2,X1)
| ~ ssPv1(X3)
| ssPv1(skf2(X2))
| ssPv3(X2)
| ssPv4(X1) ),
inference(spm,[status(thm)],[c_0_52,c_0_53]),
[final] ).
cnf(c_0_60,negated_conjecture,
( ~ ssRr(X3,X2)
| ~ ssRr(X1,X3)
| ~ ssPv1(X2)
| ssPv1(skf2(X1))
| ssPv3(X1)
| ssPv4(skf2(X1)) ),
inference(spm,[status(thm)],[c_0_56,c_0_53]),
[final] ).
cnf(c_0_77,negated_conjecture,
ssRr(skf3(X1),X1),
clause1,
[final] ).
cnf(c_0_204,negated_conjecture,
( ~ ssRr(X4,X3)
| ~ ssRr(skf3(X2),X4)
| ~ ssRr(skf3(X2),X1)
| ~ ssPv1(X3)
| ssPv1(X2)
| ssPv3(skf3(X2))
| ssPv4(X1) ),
inference(spm,[status(thm)],[c_0_52,c_0_77]),
[final] ).
cnf(c_0_213,negated_conjecture,
( ~ ssRr(X3,X2)
| ~ ssRr(skf3(X1),X3)
| ~ ssPv1(X2)
| ssPv1(X1)
| ssPv3(skf3(X1))
| ssPv4(X1) ),
inference(spm,[status(thm)],[c_0_204,c_0_77]),
[final] ).
cnf(c_0_460,negated_conjecture,
( ~ ssRr(X3,X2)
| ~ ssRr(skf3(X1),X3)
| ~ ssPv1(X2)
| ssPv1(X1)
| ssPv3(skf3(X1))
| ssPv4(skf2(skf3(X1))) ),
inference(spm,[status(thm)],[c_0_204,c_0_53]),
[final] ).
cnf(c_0_467,negated_conjecture,
( ~ ssRr(X2,X5)
| ~ ssRr(X2,X3)
| ~ ssPv3(X4)
| ~ ssRr(X3,X4)
| ~ ssRr(X1,X2)
| ssPv3(X2)
| ssPv3(X5)
| ssPv3(X1) ),
c_0_458,
[final] ).
cnf(c_0_468,negated_conjecture,
( ~ ssRr(X2,X3)
| ~ ssRr(X3,X4)
| ~ ssPv1(X1)
| ~ ssRr(X1,X2)
| ssPv4(X2)
| ssPv1(X2)
| ssPv3(X4) ),
c_0_459,
[final] ).
cnf(c_0_477,negated_conjecture,
( ~ ssRr(X1,X2)
| ~ ssRr(X2,X4)
| ~ ssRr(X2,X3)
| ~ ssPv3(skf2(X4))
| ssPv3(X3)
| ssPv3(X2)
| ssPv3(X1) ),
inference(spm,[status(thm)],[c_0_467,c_0_53]),
[final] ).
cnf(c_0_478,negated_conjecture,
( ~ ssRr(X3,X1)
| ~ ssRr(X1,X2)
| ~ ssPv1(X3)
| ssPv1(X1)
| ssPv3(skf2(X2))
| ssPv4(X1) ),
inference(spm,[status(thm)],[c_0_468,c_0_53]),
[final] ).
cnf(c_0_488,negated_conjecture,
( ~ ssRr(X2,X1)
| ~ ssRr(X1,X3)
| ~ ssPv3(skf2(X3))
| ssPv3(X2)
| ssPv3(X1)
| ssPv3(skf2(X1)) ),
inference(spm,[status(thm)],[c_0_477,c_0_53]),
[final] ).
cnf(c_0_489,negated_conjecture,
( ~ ssRr(X2,X1)
| ~ ssPv1(X2)
| ssPv1(X1)
| ssPv3(skf2(skf2(X1)))
| ssPv4(X1) ),
inference(spm,[status(thm)],[c_0_478,c_0_53]),
[final] ).
cnf(c_0_572,negated_conjecture,
( ~ ssRr(X2,skf3(X1))
| ~ ssPv1(X2)
| ssPv1(skf3(X1))
| ssPv3(skf2(X1))
| ssPv4(skf3(X1)) ),
inference(spm,[status(thm)],[c_0_478,c_0_77]),
[final] ).
cnf(c_0_585,negated_conjecture,
( ~ ssRr(X3,X1)
| ~ ssRr(X1,skf3(X2))
| ~ ssPv1(X3)
| ssPv1(X1)
| ssPv3(X2)
| ssPv4(X1) ),
inference(spm,[status(thm)],[c_0_468,c_0_77]),
[final] ).
cnf(c_0_612,negated_conjecture,
( ~ ssRr(X2,skf3(skf3(X1)))
| ~ ssPv1(X2)
| ssPv1(skf3(skf3(X1)))
| ssPv3(X1)
| ssPv4(skf3(skf3(X1))) ),
inference(spm,[status(thm)],[c_0_585,c_0_77]),
[final] ).
cnf(c_0_653,negated_conjecture,
( ~ ssRr(X6,X3)
| ~ ssRr(X5,X3)
| ~ ssRr(X4,X5)
| ~ ssRr(X2,X3)
| ~ ssPv1(X1)
| ~ ssRr(X1,X2)
| ssPv2(X3)
| ssPv4(X6)
| ssPv1(X4) ),
c_0_632,
[final] ).
cnf(c_0_668,negated_conjecture,
( ~ ssRr(X3,X5)
| ~ ssRr(X2,X4)
| ~ ssRr(X5,skf2(X1))
| ~ ssRr(X4,skf2(X1))
| ~ ssPv1(X3)
| ssPv1(X2)
| ssPv4(X1)
| ssPv2(skf2(X1)) ),
inference(spm,[status(thm)],[c_0_653,c_0_53]),
[final] ).
cnf(c_0_678,negated_conjecture,
( ~ ssRr(X3,X4)
| ~ ssRr(X2,X1)
| ~ ssRr(X4,skf2(X1))
| ~ ssPv1(X3)
| ssPv1(X2)
| ssPv4(X1)
| ssPv2(skf2(X1)) ),
inference(spm,[status(thm)],[c_0_668,c_0_53]),
[final] ).
cnf(c_0_686,negated_conjecture,
( ~ ssRr(X2,X1)
| ~ ssRr(X3,skf3(skf2(X1)))
| ~ ssPv1(X3)
| ssPv1(X2)
| ssPv4(X1)
| ssPv2(skf2(X1)) ),
inference(spm,[status(thm)],[c_0_678,c_0_77]),
[final] ).
cnf(c_0_700,negated_conjecture,
( ~ ssRr(X3,X4)
| ~ ssPv1(X5)
| ~ ssRr(X4,X5)
| ~ ssRr(X3,X1)
| ~ ssPv3(X2)
| ~ ssRr(X1,X2)
| ssPv3(X3)
| ssPv2(X3) ),
c_0_690,
[final] ).
cnf(c_0_712,negated_conjecture,
( ~ ssRr(X4,X2)
| ~ ssRr(X1,X4)
| ~ ssRr(X1,X3)
| ~ ssPv1(skf2(X3))
| ~ ssPv3(X2)
| ssPv3(X1)
| ssPv2(X1) ),
inference(spm,[status(thm)],[c_0_700,c_0_53]),
[final] ).
cnf(c_0_767,negated_conjecture,
( ~ ssRr(X2,X4)
| ~ ssRr(X4,X5)
| ~ ssRr(X3,X2)
| ~ ssPv3(X1)
| ~ ssRr(X1,X2)
| ssPv3(X2)
| ssPv2(X5)
| ssPv3(X3) ),
c_0_759,
[final] ).
cnf(c_0_776,negated_conjecture,
( ~ ssRr(X4,X2)
| ~ ssRr(X2,X1)
| ~ ssRr(X3,X2)
| ~ ssPv3(X4)
| ssPv3(X3)
| ssPv3(X2)
| ssPv2(skf2(X1)) ),
inference(spm,[status(thm)],[c_0_767,c_0_53]),
[final] ).
cnf(c_0_786,negated_conjecture,
( ~ ssRr(X3,skf2(X2))
| ~ ssRr(skf2(X2),X1)
| ~ ssPv3(X3)
| ssPv3(X2)
| ssPv3(skf2(X2))
| ssPv2(skf2(X1)) ),
inference(spm,[status(thm)],[c_0_776,c_0_53]),
[final] ).
cnf(c_0_796,negated_conjecture,
( ~ ssRr(X2,skf2(X1))
| ~ ssPv3(X2)
| ssPv3(X1)
| ssPv3(skf2(X1))
| ssPv2(skf2(skf2(skf2(X1)))) ),
inference(spm,[status(thm)],[c_0_786,c_0_53]),
[final] ).
cnf(c_0_820,negated_conjecture,
( ~ ssRr(X2,skf3(X1))
| ~ ssRr(skf3(X1),X3)
| ~ ssPv3(skf2(X3))
| ssPv3(X2)
| ssPv3(X1)
| ssPv3(skf3(X1)) ),
inference(spm,[status(thm)],[c_0_477,c_0_77]),
[final] ).
cnf(c_0_1257,negated_conjecture,
( ~ ssRr(X3,X2)
| ~ ssRr(X2,X1)
| ~ ssPv3(X3)
| ssPv3(X2)
| ssPv3(skf3(X2))
| ssPv2(skf2(X1)) ),
inference(spm,[status(thm)],[c_0_776,c_0_77]),
[final] ).
cnf(c_0_1264,negated_conjecture,
( ~ ssRr(X2,X1)
| ~ ssPv3(X2)
| ssPv3(X1)
| ssPv3(skf3(X1))
| ssPv2(skf2(skf2(X1))) ),
inference(spm,[status(thm)],[c_0_1257,c_0_53]),
[final] ).
cnf(c_0_1320,negated_conjecture,
( ~ ssRr(X3,X5)
| ~ ssRr(X5,X6)
| ~ ssPv1(X4)
| ~ ssRr(X4,X3)
| ~ ssRr(X2,X3)
| ~ ssPv1(X1)
| ~ ssRr(X1,X2)
| ssPv3(X3)
| ssPv1(X6) ),
c_0_1316,
[final] ).
cnf(c_0_1325,negated_conjecture,
( ~ ssRr(X3,X1)
| ~ ssRr(X2,X1)
| ~ ssPv1(X3)
| ssPv1(X2)
| ssPv4(X1)
| ssPv2(skf2(X1)) ),
inference(spm,[status(thm)],[c_0_678,c_0_53]),
[final] ).
cnf(c_0_1326,negated_conjecture,
( ~ ssRr(X4,X5)
| ~ ssRr(X5,X1)
| ~ ssRr(X1,X2)
| ~ ssRr(X3,X1)
| ~ ssPv1(X4)
| ~ ssPv1(X3)
| ssPv1(skf2(X2))
| ssPv3(X1) ),
inference(spm,[status(thm)],[c_0_1320,c_0_53]),
[final] ).
cnf(c_0_1336,negated_conjecture,
( ~ ssRr(X2,X1)
| ~ ssPv1(X2)
| ssPv1(skf3(X1))
| ssPv4(X1)
| ssPv2(skf2(X1)) ),
inference(spm,[status(thm)],[c_0_1325,c_0_77]),
[final] ).
cnf(c_0_1337,negated_conjecture,
( ~ ssRr(X3,X4)
| ~ ssRr(X4,X1)
| ~ ssRr(X1,X2)
| ~ ssPv1(X3)
| ~ ssPv1(skf3(X1))
| ssPv1(skf2(X2))
| ssPv3(X1) ),
inference(spm,[status(thm)],[c_0_1326,c_0_77]),
[final] ).
cnf(c_0_1346,negated_conjecture,
( ~ ssRr(X3,X5)
| ~ ssRr(X5,X1)
| ~ ssRr(X2,X4)
| ~ ssRr(X4,X1)
| ~ ssPv1(X3)
| ssPv1(X2)
| ssPv4(skf3(X1))
| ssPv2(X1) ),
inference(spm,[status(thm)],[c_0_653,c_0_77]),
[final] ).
cnf(c_0_1357,negated_conjecture,
( ~ ssRr(X3,X4)
| ~ ssRr(X2,X1)
| ~ ssRr(X4,skf2(X1))
| ~ ssPv1(X3)
| ssPv1(X2)
| ssPv4(skf3(skf2(X1)))
| ssPv2(skf2(X1)) ),
inference(spm,[status(thm)],[c_0_1346,c_0_53]),
[final] ).
cnf(c_0_1358,negated_conjecture,
( ~ ssRr(skf2(skf3(X1)),X2)
| ~ ssPv1(X2)
| ssPv1(X1)
| ssPv3(skf3(X1))
| ssPv4(X1) ),
inference(spm,[status(thm)],[c_0_213,c_0_53]),
[final] ).
cnf(c_0_1368,negated_conjecture,
( ~ ssRr(X3,X1)
| ~ ssRr(X2,X1)
| ~ ssPv1(X3)
| ssPv1(X2)
| ssPv4(skf3(skf2(X1)))
| ssPv2(skf2(X1)) ),
inference(spm,[status(thm)],[c_0_1357,c_0_53]),
[final] ).
cnf(c_0_1370,negated_conjecture,
( ~ ssPv1(skf2(skf2(skf3(X1))))
| ssPv1(X1)
| ssPv3(skf3(X1))
| ssPv4(X1) ),
inference(spm,[status(thm)],[c_0_1358,c_0_53]),
[final] ).
cnf(c_0_1378,negated_conjecture,
( ~ ssRr(X2,skf2(X1))
| ~ ssPv1(X2)
| ssPv1(X1)
| ssPv4(skf3(skf2(skf2(X1))))
| ssPv2(skf2(skf2(X1))) ),
inference(spm,[status(thm)],[c_0_1368,c_0_53]),
[final] ).
cnf(c_0_1414,negated_conjecture,
( ~ ssRr(X3,X4)
| ~ ssRr(X4,X1)
| ~ ssRr(X2,skf3(X1))
| ~ ssPv1(X3)
| ssPv1(X2)
| ssPv4(skf3(X1))
| ssPv2(X1) ),
inference(spm,[status(thm)],[c_0_1346,c_0_77]),
[final] ).
cnf(c_0_1429,negated_conjecture,
( ~ ssRr(X2,X3)
| ~ ssRr(X3,X1)
| ~ ssPv1(X2)
| ssPv1(skf3(skf3(X1)))
| ssPv4(skf3(X1))
| ssPv2(X1) ),
inference(spm,[status(thm)],[c_0_1414,c_0_77]),
[final] ).
cnf(c_0_1447,negated_conjecture,
( ~ ssRr(X2,X1)
| ~ ssPv1(X2)
| ssPv1(skf3(skf3(skf2(X1))))
| ssPv4(skf3(skf2(X1)))
| ssPv2(skf2(X1)) ),
inference(spm,[status(thm)],[c_0_1429,c_0_53]),
[final] ).
cnf(c_0_1459,negated_conjecture,
( ~ ssRr(X1,X2)
| ~ ssRr(X2,X3)
| ~ ssRr(X2,skf3(X4))
| ~ ssPv3(X4)
| ssPv3(X3)
| ssPv3(X2)
| ssPv3(X1) ),
inference(spm,[status(thm)],[c_0_467,c_0_77]),
[final] ).
cnf(c_0_1466,negated_conjecture,
( ~ ssPv1(skf3(X1))
| ssPv1(skf3(skf3(skf2(X1))))
| ssPv4(skf3(skf2(X1)))
| ssPv2(skf2(X1)) ),
inference(spm,[status(thm)],[c_0_1447,c_0_77]),
[final] ).
cnf(c_0_1686,negated_conjecture,
( ~ ssRr(X3,X4)
| ~ ssRr(X4,skf2(X1))
| ~ ssRr(X2,skf3(skf2(X1)))
| ~ ssPv1(X3)
| ssPv1(X2)
| ssPv4(X1)
| ssPv2(skf2(X1)) ),
inference(spm,[status(thm)],[c_0_668,c_0_77]),
[final] ).
cnf(c_0_1691,negated_conjecture,
( ~ ssRr(X2,X3)
| ~ ssRr(X3,skf2(X1))
| ~ ssPv1(X2)
| ssPv1(skf3(skf3(skf2(X1))))
| ssPv4(X1)
| ssPv2(skf2(X1)) ),
inference(spm,[status(thm)],[c_0_1686,c_0_77]),
[final] ).
cnf(c_0_1696,negated_conjecture,
( ~ ssRr(X3,X6)
| ~ ssRr(X6,X7)
| ~ ssRr(X5,X3)
| ~ ssRr(X4,X5)
| ~ ssRr(X2,X3)
| ~ ssPv3(X1)
| ~ ssRr(X1,X2)
| ssPv4(X3)
| ssPv2(X7)
| ssPv1(X4) ),
c_0_1687,
[final] ).
cnf(c_0_1701,negated_conjecture,
( ~ ssRr(X2,X1)
| ~ ssPv1(X2)
| ssPv1(skf3(skf3(skf2(X1))))
| ssPv4(X1) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1691,c_0_53]),c_0_1690]),
[final] ).
cnf(c_0_1706,negated_conjecture,
( ~ ssRr(X4,X6)
| ~ ssRr(X6,X2)
| ~ ssRr(X2,X1)
| ~ ssRr(X3,X5)
| ~ ssRr(X5,X2)
| ~ ssPv3(X4)
| ssPv1(X3)
| ssPv4(X2)
| ssPv2(skf2(X1)) ),
inference(spm,[status(thm)],[c_0_1696,c_0_53]),
[final] ).
cnf(c_0_1712,negated_conjecture,
( ~ ssPv1(skf3(X1))
| ssPv1(skf3(skf3(skf2(X1))))
| ssPv4(X1) ),
inference(spm,[status(thm)],[c_0_1701,c_0_77]),
[final] ).
cnf(c_0_1725,negated_conjecture,
( ~ ssRr(X3,X4)
| ~ ssRr(X2,X1)
| ~ ssRr(X4,skf2(X1))
| ~ ssPv3(X3)
| ssPv1(X2)
| ssPv4(skf2(X1)) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1716,c_0_53]),c_0_1690]),
[final] ).
cnf(c_0_1736,negated_conjecture,
( ~ ssRr(X3,X1)
| ~ ssRr(X2,X1)
| ~ ssPv3(X3)
| ssPv1(X2)
| ssPv4(skf2(X1)) ),
inference(spm,[status(thm)],[c_0_1725,c_0_53]),
[final] ).
cnf(c_0_1740,negated_conjecture,
( ~ ssPv1(X1)
| ssPv1(skf3(skf3(skf2(skf2(X1)))))
| ssPv4(skf2(X1)) ),
inference(spm,[status(thm)],[c_0_1701,c_0_53]),
[final] ).
cnf(c_0_1748,negated_conjecture,
( ~ ssRr(X2,X1)
| ~ ssPv3(X2)
| ssPv1(skf3(X1))
| ssPv4(skf2(X1)) ),
inference(spm,[status(thm)],[c_0_1736,c_0_77]),
[final] ).
cnf(c_0_1766,negated_conjecture,
( ~ ssRr(X2,X1)
| ~ ssPv1(X2)
| ssPv1(skf3(X1))
| ssPv4(skf3(skf2(X1)))
| ssPv2(skf2(X1)) ),
inference(spm,[status(thm)],[c_0_1368,c_0_77]),
[final] ).
cnf(c_0_1785,negated_conjecture,
( ~ ssPv3(X1)
| ssPv1(skf3(skf2(X1))) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_1748,c_0_53]),c_0_1783]),
[final] ).
cnf(c_0_1791,negated_conjecture,
~ ssPv4(X1),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_1789,c_0_1222]),c_0_1597]),
[final] ).
cnf(c_0_1793,negated_conjecture,
( ~ ssPv3(X1)
| ssPv1(X1) ),
inference(spm,[status(thm)],[c_0_1791,c_0_1786]),
[final] ).
cnf(c_0_1804,negated_conjecture,
( ~ ssRr(X3,X2)
| ~ ssRr(X1,X3)
| ~ ssPv1(skf3(X1))
| ~ ssPv3(X2)
| ssPv3(X1) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_1797,c_0_53]),c_0_1798]),c_0_1757]),
[final] ).
cnf(c_0_1807,negated_conjecture,
( ~ ssRr(X3,X6)
| ~ ssRr(X6,X7)
| ~ ssRr(X3,X4)
| ~ ssRr(X4,X5)
| ~ ssRr(X3,X1)
| ~ ssPv3(X2)
| ~ ssRr(X1,X2)
| ssPv4(X3)
| ssPv2(X7)
| ssPv3(X5) ),
c_0_1800,
[final] ).
cnf(c_0_1808,negated_conjecture,
( ~ ssRr(X3,X6)
| ~ ssRr(X6,X7)
| ~ ssRr(X5,X3)
| ~ ssRr(X4,X5)
| ~ ssRr(X2,X3)
| ~ ssPv3(X1)
| ~ ssRr(X1,X2)
| ssPv3(X3)
| ssPv3(X7)
| ssPv2(X4) ),
c_0_1801,
[final] ).
cnf(c_0_1811,negated_conjecture,
( ~ ssRr(skf2(X1),X2)
| ~ ssPv1(skf3(X1))
| ~ ssPv3(X2)
| ssPv3(X1) ),
inference(spm,[status(thm)],[c_0_1804,c_0_53]),
[final] ).
cnf(c_0_1812,negated_conjecture,
( ~ ssPv1(skf3(skf2(X1)))
| ssPv1(X1) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1791,c_0_1389]),c_0_1690]),
[final] ).
cnf(c_0_1813,negated_conjecture,
( ~ ssPv3(X1)
| ssPv1(skf3(X1)) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1805,c_0_1806]),c_0_1791]),
[final] ).
cnf(c_0_1815,negated_conjecture,
( ~ ssRr(X3,X2)
| ~ ssRr(skf3(X1),X3)
| ~ ssPv1(X2)
| ssPv1(skf2(skf3(X1)))
| ssPv3(skf3(X1))
| ssPv4(X1) ),
inference(spm,[status(thm)],[c_0_56,c_0_77]),
[final] ).
cnf(c_0_1816,negated_conjecture,
( ~ ssRr(X6,X4)
| ~ ssRr(X2,X6)
| ~ ssRr(X2,X5)
| ~ ssRr(X2,X1)
| ~ ssRr(X5,X3)
| ~ ssPv3(X4)
| ssPv3(X3)
| ssPv4(X2)
| ssPv2(skf2(X1)) ),
inference(spm,[status(thm)],[c_0_1807,c_0_53]),
[final] ).
cnf(c_0_1817,negated_conjecture,
( ~ ssRr(X4,X6)
| ~ ssRr(X6,X3)
| ~ ssRr(X3,X2)
| ~ ssRr(X1,X5)
| ~ ssRr(X5,X3)
| ~ ssPv3(X4)
| ssPv3(X3)
| ssPv3(skf2(X2))
| ssPv2(X1) ),
inference(spm,[status(thm)],[c_0_1808,c_0_53]),
[final] ).
cnf(c_0_1819,negated_conjecture,
( ~ ssRr(X4,X5)
| ~ ssRr(X5,X2)
| ~ ssRr(X2,X1)
| ~ ssRr(X3,skf3(X2))
| ~ ssPv3(X4)
| ssPv1(X3)
| ssPv4(X2)
| ssPv2(skf2(X1)) ),
inference(spm,[status(thm)],[c_0_1706,c_0_77]),
[final] ).
cnf(c_0_1821,negated_conjecture,
( ~ ssPv3(skf2(X1))
| ssPv1(X1) ),
inference(spm,[status(thm)],[c_0_1812,c_0_1813]),
[final] ).
cnf(c_0_1822,negated_conjecture,
( ~ ssPv3(X3)
| ~ ssRr(X3,X6)
| ~ ssRr(X6,X7)
| ~ ssRr(X3,X4)
| ~ ssRr(X4,X5)
| ~ ssRr(X2,X3)
| ~ ssPv3(X1)
| ~ ssRr(X1,X2)
| ssPv2(X7)
| ssPv3(X5) ),
c_0_1814,
[final] ).
cnf(c_0_1823,negated_conjecture,
( ~ ssRr(X3,X4)
| ~ ssRr(X4,skf2(X1))
| ~ ssRr(skf2(X1),X2)
| ~ ssPv1(X3)
| ~ ssPv1(X1)
| ssPv1(skf2(X2))
| ssPv3(skf2(X1)) ),
inference(spm,[status(thm)],[c_0_1326,c_0_53]),
[final] ).
cnf(c_0_1824,negated_conjecture,
( ~ ssRr(X1,X2)
| ~ ssPv1(X2)
| ssPv1(skf2(skf3(X1)))
| ssPv3(skf3(X1))
| ssPv4(X1) ),
inference(spm,[status(thm)],[c_0_1815,c_0_77]),
[final] ).
cnf(c_0_1826,negated_conjecture,
( ~ ssRr(X4,X5)
| ~ ssRr(X5,X3)
| ~ ssRr(X3,X2)
| ~ ssRr(X1,skf3(X3))
| ~ ssPv3(X4)
| ssPv3(X3)
| ssPv3(skf2(X2))
| ssPv2(X1) ),
inference(spm,[status(thm)],[c_0_1817,c_0_77]),
[final] ).
cnf(c_0_1829,negated_conjecture,
( ~ ssPv1(skf3(X1))
| ssPv1(X1) ),
inference(csr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1820,c_0_847]),c_0_1791]),c_0_1793]),
[final] ).
cnf(c_0_1831,negated_conjecture,
( ~ ssRr(X4,X6)
| ~ ssRr(X6,X3)
| ~ ssRr(X3,X5)
| ~ ssRr(X3,X1)
| ~ ssRr(X5,X2)
| ~ ssPv3(X4)
| ~ ssPv3(X3)
| ssPv3(X2)
| ssPv2(skf2(X1)) ),
inference(spm,[status(thm)],[c_0_1822,c_0_53]),
[final] ).
cnf(c_0_1833,negated_conjecture,
( ~ ssPv1(X1)
| ssPv1(skf2(skf3(skf3(X1))))
| ssPv3(skf3(skf3(X1)))
| ssPv4(skf3(X1)) ),
inference(spm,[status(thm)],[c_0_1824,c_0_77]),
[final] ).
cnf(c_0_1834,negated_conjecture,
( ~ ssRr(X4,X3)
| ~ ssRr(X1,X4)
| ~ ssRr(X1,X2)
| ~ ssPv3(X3)
| ssPv3(skf2(X2))
| ssPv4(X1) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1825,c_0_53]),c_0_1690]),
[final] ).
cnf(c_0_1835,negated_conjecture,
( ~ ssRr(X3,X4)
| ~ ssRr(X4,X1)
| ~ ssRr(X1,X2)
| ~ ssPv3(X3)
| ssPv3(X1)
| ssPv3(skf2(X2))
| ssPv2(skf3(skf3(X1))) ),
inference(spm,[status(thm)],[c_0_1826,c_0_77]),
[final] ).
cnf(c_0_1836,negated_conjecture,
~ ssPv2(X1),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_1827,c_0_1775]),c_0_1775]),
[final] ).
cnf(c_0_1837,negated_conjecture,
( ~ ssRr(X2,X3)
| ~ ssRr(X3,X1)
| ~ ssPv3(X2)
| ssPv1(skf3(skf3(X1))) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1828,c_0_53]),c_0_1791]),
[final] ).
cnf(c_0_1838,negated_conjecture,
( ~ ssPv1(skf3(X1))
| ssPv1(skf2(X1)) ),
inference(spm,[status(thm)],[c_0_1829,c_0_1830]),
[final] ).
cnf(c_0_1839,negated_conjecture,
( ~ ssPv3(skf3(X1))
| ssPv1(X1) ),
inference(spm,[status(thm)],[c_0_1829,c_0_1793]),
[final] ).
cnf(c_0_1843,negated_conjecture,
( ~ ssRr(X3,X2)
| ~ ssRr(X1,X3)
| ~ ssPv3(X2)
| ssPv3(skf2(skf2(X1))) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1834,c_0_53]),c_0_1791]),
[final] ).
cnf(c_0_1845,negated_conjecture,
( ~ ssRr(X2,X1)
| ~ ssPv3(X2)
| ssPv1(skf3(skf3(skf2(X1)))) ),
inference(spm,[status(thm)],[c_0_1837,c_0_53]),
[final] ).
cnf(c_0_1846,negated_conjecture,
( ~ ssPv1(skf3(skf2(skf3(X1))))
| ssPv1(X1) ),
inference(csr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1370,c_0_1838]),c_0_1791]),c_0_1839]),
[final] ).
cnf(c_0_1847,negated_conjecture,
( ~ ssPv1(skf3(X1))
| ssPv1(skf3(skf2(X1))) ),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1829,c_0_1466]),c_0_1690]),c_0_1791]),
[final] ).
cnf(c_0_1849,negated_conjecture,
( ~ ssRr(X3,X4)
| ~ ssRr(X4,X2)
| ~ ssRr(X2,X1)
| ~ ssPv3(X3)
| ~ ssPv3(X2)
| ssPv3(skf2(X1)) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1840,c_0_53]),c_0_1690]),
[final] ).
cnf(c_0_1850,negated_conjecture,
( ~ ssRr(X2,X1)
| ~ ssRr(X3,skf3(skf2(X1)))
| ~ ssPv1(X3)
| ssPv1(X2)
| ssPv4(skf3(skf2(X1)))
| ssPv2(skf2(X1)) ),
inference(spm,[status(thm)],[c_0_1357,c_0_77]),
[final] ).
cnf(c_0_1852,negated_conjecture,
( ~ ssPv1(X1)
| ssPv1(skf3(skf3(skf2(skf2(X1)))))
| ssPv4(skf3(skf2(skf2(X1))))
| ssPv2(skf2(skf2(X1))) ),
inference(spm,[status(thm)],[c_0_1447,c_0_53]),
[final] ).
cnf(c_0_1853,negated_conjecture,
( ~ ssPv1(X1)
| ssPv1(skf3(skf3(X1))) ),
inference(csr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1839,c_0_1842]),c_0_1791]),c_0_1791]),c_0_1793]),
[final] ).
cnf(c_0_1854,negated_conjecture,
( ~ ssRr(X1,X2)
| ~ ssPv3(X2)
| ssPv3(skf2(skf2(skf3(X1)))) ),
inference(spm,[status(thm)],[c_0_1843,c_0_77]),
[final] ).
cnf(c_0_1857,negated_conjecture,
( ~ ssPv3(skf3(X1))
| ssPv1(skf3(skf3(skf2(X1)))) ),
inference(spm,[status(thm)],[c_0_1845,c_0_77]),
[final] ).
cnf(c_0_1858,negated_conjecture,
( ~ ssPv1(skf3(skf3(X1)))
| ssPv1(X1) ),
inference(spm,[status(thm)],[c_0_1846,c_0_1847]),
[final] ).
cnf(c_0_1859,negated_conjecture,
( ~ ssRr(X1,X2)
| ~ ssPv3(X2)
| ~ ssPv3(X1) ),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1848,c_0_77]),c_0_1791]),c_0_1791]),
[final] ).
cnf(c_0_1860,negated_conjecture,
( ~ ssRr(X2,X3)
| ~ ssRr(X3,X1)
| ~ ssPv3(X2)
| ssPv3(skf2(skf2(X1))) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_1849,c_0_53]),c_0_1844]),
[final] ).
cnf(c_0_1861,negated_conjecture,
( ~ ssRr(X1,X2)
| ~ ssPv1(skf3(skf3(skf2(X2))))
| ssPv1(X1) ),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1850,c_0_77]),c_0_1690]),c_0_1791]),
[final] ).
cnf(c_0_1862,negated_conjecture,
( ~ ssPv3(X1)
| ssPv1(skf3(skf3(skf2(skf2(X1))))) ),
inference(spm,[status(thm)],[c_0_1845,c_0_53]),
[final] ).
cnf(c_0_1865,negated_conjecture,
( ~ ssRr(X1,X2)
| ~ ssPv1(skf2(X2))
| ssPv1(X1) ),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_696,c_0_1853]),c_0_1690]),c_0_1791]),
[final] ).
cnf(c_0_1866,negated_conjecture,
( ~ ssPv3(X1)
| ssPv1(skf2(X1)) ),
inference(spm,[status(thm)],[c_0_1829,c_0_1785]),
[final] ).
cnf(c_0_1867,negated_conjecture,
( ~ ssPv3(X1)
| ssPv3(skf2(skf2(skf3(skf3(X1))))) ),
inference(spm,[status(thm)],[c_0_1854,c_0_77]),
[final] ).
cnf(c_0_1870,negated_conjecture,
( ~ ssPv3(skf3(X1))
| ssPv1(skf3(skf2(X1))) ),
inference(spm,[status(thm)],[c_0_1829,c_0_1857]),
[final] ).
cnf(c_0_1872,negated_conjecture,
( ~ ssPv3(skf3(X1))
| ssPv1(skf2(X1)) ),
inference(spm,[status(thm)],[c_0_1858,c_0_1857]),
[final] ).
cnf(c_0_1873,negated_conjecture,
( ~ ssPv3(X1)
| ~ ssPv3(skf2(X1)) ),
inference(spm,[status(thm)],[c_0_1859,c_0_53]),
[final] ).
cnf(c_0_1874,negated_conjecture,
( ~ ssRr(X2,X1)
| ~ ssPv3(X2)
| ssPv3(skf2(skf2(skf2(X1)))) ),
inference(spm,[status(thm)],[c_0_1860,c_0_53]),
[final] ).
cnf(c_0_1875,negated_conjecture,
( ~ ssPv3(skf2(X1))
| ssPv3(skf2(skf2(skf3(X1)))) ),
inference(spm,[status(thm)],[c_0_1854,c_0_53]),
[final] ).
cnf(c_0_1877,negated_conjecture,
( ~ ssRr(X1,skf2(X2))
| ~ ssPv3(X2)
| ssPv1(X1) ),
inference(spm,[status(thm)],[c_0_1861,c_0_1862]),
[final] ).
cnf(c_0_1884,negated_conjecture,
( ~ ssRr(X1,X2)
| ~ ssPv3(X2)
| ssPv1(X1) ),
inference(spm,[status(thm)],[c_0_1865,c_0_1866]),
[final] ).
cnf(c_0_1885,negated_conjecture,
( ~ ssPv1(X1)
| ssPv1(skf3(X1)) ),
inference(spm,[status(thm)],[c_0_1839,c_0_1764]),
[final] ).
cnf(c_0_1886,negated_conjecture,
( ~ ssRr(X1,X2)
| ~ ssPv1(X2)
| ssPv1(skf2(skf3(X1)))
| ssPv3(skf3(X1))
| ssPv4(skf2(skf3(X1))) ),
inference(spm,[status(thm)],[c_0_60,c_0_77]),
[final] ).
cnf(c_0_1888,negated_conjecture,
( ~ ssPv3(X1)
| ssPv1(skf2(skf3(skf3(X1)))) ),
inference(spm,[status(thm)],[c_0_1821,c_0_1867]),
[final] ).
cnf(c_0_1889,negated_conjecture,
( ~ ssPv3(X1)
| ~ ssPv3(skf2(skf3(skf3(X1)))) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1791,c_0_1868]),c_0_1791]),
[final] ).
cnf(c_0_1890,negated_conjecture,
( ~ ssPv3(skf3(X1))
| ssPv3(skf2(X1)) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_1820,c_0_1869]),c_0_1870]),
[final] ).
cnf(c_0_1891,negated_conjecture,
( ~ ssPv3(X1)
| ssPv1(skf2(skf2(skf2(X1)))) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_1871,c_0_1862]),c_0_1872]),
[final] ).
cnf(c_0_1892,negated_conjecture,
( ~ ssPv3(skf3(X1))
| ~ ssPv3(skf2(skf2(X1))) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_1873,c_0_1869]),c_0_1873]),
[final] ).
cnf(c_0_1893,negated_conjecture,
( ~ ssPv3(X1)
| ssPv3(skf2(skf2(skf2(skf2(X1))))) ),
inference(spm,[status(thm)],[c_0_1874,c_0_53]),
[final] ).
cnf(c_0_1894,negated_conjecture,
( ~ ssPv3(skf2(X1))
| ssPv1(skf2(skf3(X1))) ),
inference(spm,[status(thm)],[c_0_1821,c_0_1875]),
[final] ).
cnf(c_0_1896,negated_conjecture,
( ~ ssPv3(skf3(X1))
| ssPv1(skf2(skf2(X1))) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_1871,c_0_1857]),c_0_1872]),
[final] ).
cnf(c_0_1897,negated_conjecture,
( ~ ssPv1(X1)
| ssPv1(skf3(skf2(X1))) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1791,c_0_1773]),c_0_1690]),
[final] ).
cnf(c_0_1898,negated_conjecture,
( ~ ssRr(X1,skf2(X2))
| ~ ssPv1(skf3(skf3(X2)))
| ssPv1(X1) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_1865,c_0_1371]),c_0_1829]),c_0_1877]),
[final] ).
cnf(c_0_1901,negated_conjecture,
( ~ ssRr(X3,X6)
| ~ ssPv3(X7)
| ~ ssRr(X6,X7)
| ~ ssRr(X5,X3)
| ~ ssRr(X4,X5)
| ~ ssRr(X2,X3)
| ~ ssPv1(X1)
| ~ ssRr(X1,X2)
| ssPv2(X3)
| ssPv1(X4) ),
c_0_1880,
[final] ).
cnf(c_0_1903,negated_conjecture,
( ~ ssPv1(X1)
| ssPv1(skf2(skf2(X1))) ),
inference(spm,[status(thm)],[c_0_1829,c_0_1882]),
[final] ).
cnf(c_0_1904,negated_conjecture,
( ~ ssRr(X6,X4)
| ~ ssRr(X2,X6)
| ~ ssRr(X2,X5)
| ~ ssRr(X5,X3)
| ~ ssRr(X2,skf3(X1))
| ~ ssPv3(X4)
| ssPv3(X3)
| ssPv4(X2)
| ssPv2(X1) ),
inference(spm,[status(thm)],[c_0_1807,c_0_77]),
[final] ).
cnf(c_0_1905,negated_conjecture,
( ~ ssRr(X1,X2)
| ~ ssPv3(X2)
| ssPv3(skf3(X1)) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_1883,c_0_1853]),c_0_1884]),
[final] ).
cnf(c_0_1909,negated_conjecture,
( ~ ssRr(X5,X4)
| ~ ssRr(X2,X5)
| ~ ssRr(X2,X1)
| ~ ssRr(X2,skf3(X3))
| ~ ssPv3(X4)
| ssPv3(X3)
| ssPv4(X2)
| ssPv2(skf2(X1)) ),
inference(spm,[status(thm)],[c_0_1816,c_0_77]),
[final] ).
cnf(c_0_1910,negated_conjecture,
( ~ ssPv1(skf2(X1))
| ssPv1(X1) ),
inference(spm,[status(thm)],[c_0_1812,c_0_1885]),
[final] ).
cnf(c_0_1911,negated_conjecture,
( ~ ssPv1(skf2(X1))
| ssPv1(skf2(skf3(X1)))
| ssPv3(skf3(X1))
| ssPv4(skf2(skf3(X1))) ),
inference(spm,[status(thm)],[c_0_1886,c_0_53]),
[final] ).
cnf(c_0_1913,negated_conjecture,
( ~ ssRr(X4,X2)
| ~ ssRr(X1,X4)
| ~ ssRr(X1,skf3(skf3(X3)))
| ~ ssPv3(X3)
| ~ ssPv3(X2)
| ssPv3(X1) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_712,c_0_1888]),c_0_1836]),
[final] ).
cnf(c_0_1914,negated_conjecture,
( ~ ssPv3(X1)
| ~ ssPv3(skf3(skf3(skf3(X1)))) ),
inference(spm,[status(thm)],[c_0_1889,c_0_1890]),
[final] ).
cnf(c_0_1915,negated_conjecture,
( ~ ssRr(X4,X2)
| ~ ssRr(X1,X4)
| ~ ssRr(X1,skf2(skf2(X3)))
| ~ ssPv3(X3)
| ~ ssPv3(X2)
| ssPv3(X1) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_712,c_0_1891]),c_0_1836]),
[final] ).
cnf(c_0_1916,negated_conjecture,
( ~ ssPv3(X1)
| ~ ssPv3(skf3(skf2(skf2(X1)))) ),
inference(spm,[status(thm)],[c_0_1892,c_0_1893]),
[final] ).
cnf(c_0_1917,negated_conjecture,
( ~ ssRr(X4,X3)
| ~ ssRr(X1,X4)
| ~ ssRr(X1,skf3(X2))
| ~ ssPv3(X3)
| ~ ssPv3(skf2(X2))
| ssPv3(X1) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_712,c_0_1894]),c_0_1836]),
[final] ).
cnf(c_0_1918,negated_conjecture,
( ~ ssPv3(skf2(X1))
| ~ ssPv3(skf3(skf3(X1))) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_1873,c_0_1895]),c_0_1873]),
[final] ).
cnf(c_0_1919,negated_conjecture,
( ~ ssRr(X4,X3)
| ~ ssRr(X1,X4)
| ~ ssRr(X1,skf2(X2))
| ~ ssPv3(X3)
| ~ ssPv3(skf3(X2))
| ssPv3(X1) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_712,c_0_1896]),c_0_1836]),
[final] ).
cnf(c_0_1920,negated_conjecture,
( ~ ssPv3(skf3(X1))
| ~ ssPv3(skf3(skf2(X1))) ),
inference(spm,[status(thm)],[c_0_1892,c_0_1890]),
[final] ).
cnf(c_0_1921,negated_conjecture,
( ~ ssPv3(X1)
| ssPv1(skf3(skf2(skf2(X1)))) ),
inference(spm,[status(thm)],[c_0_1829,c_0_1862]),
[final] ).
cnf(c_0_1922,negated_conjecture,
( ~ ssPv1(X1)
| ssPv1(skf2(X1)) ),
inference(spm,[status(thm)],[c_0_1829,c_0_1897]),
[final] ).
cnf(c_0_1923,negated_conjecture,
( ~ ssPv1(skf3(skf3(X1)))
| ssPv1(skf3(skf2(X1))) ),
inference(spm,[status(thm)],[c_0_1898,c_0_77]),
[final] ).
cnf(c_0_1925,negated_conjecture,
( ~ ssRr(X4,X6)
| ~ ssRr(X6,X1)
| ~ ssRr(X1,X3)
| ~ ssRr(X2,X5)
| ~ ssRr(X5,X1)
| ~ ssPv1(X4)
| ~ ssPv3(skf2(X3))
| ssPv1(X2)
| ssPv2(X1) ),
inference(spm,[status(thm)],[c_0_1901,c_0_53]),
[final] ).
cnf(c_0_1926,negated_conjecture,
( ~ ssRr(X4,X6)
| ~ ssRr(X6,X1)
| ~ ssRr(X2,X5)
| ~ ssRr(X5,X1)
| ~ ssRr(X1,skf3(X3))
| ~ ssPv1(X4)
| ~ ssPv3(X3)
| ssPv1(X2)
| ssPv2(X1) ),
inference(spm,[status(thm)],[c_0_1901,c_0_77]),
[final] ).
cnf(c_0_1928,negated_conjecture,
( ~ ssRr(X4,X2)
| ~ ssRr(X1,X4)
| ~ ssRr(X1,skf2(X3))
| ~ ssPv1(X3)
| ~ ssPv3(X2)
| ssPv3(X1) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_712,c_0_1903]),c_0_1836]),
[final] ).
cnf(c_0_1929,negated_conjecture,
( ~ ssRr(X5,X3)
| ~ ssRr(X4,X2)
| ~ ssRr(skf3(skf3(X1)),X5)
| ~ ssRr(skf3(skf3(X1)),X4)
| ~ ssPv3(X3)
| ssPv3(X2)
| ssPv4(skf3(skf3(X1)))
| ssPv2(X1) ),
inference(spm,[status(thm)],[c_0_1904,c_0_77]),
[final] ).
cnf(c_0_1930,negated_conjecture,
( ~ ssRr(X4,X6)
| ~ ssRr(X6,X3)
| ~ ssRr(X3,X5)
| ~ ssRr(X5,X2)
| ~ ssRr(X3,skf3(X1))
| ~ ssPv3(X4)
| ~ ssPv3(X3)
| ssPv3(X2)
| ssPv2(X1) ),
inference(spm,[status(thm)],[c_0_1822,c_0_77]),
[final] ).
cnf(c_0_1931,negated_conjecture,
( ~ ssPv3(skf2(X1))
| ssPv3(skf3(X1)) ),
inference(spm,[status(thm)],[c_0_1905,c_0_53]),
[final] ).
cnf(c_0_1936,negated_conjecture,
( ~ ssPv1(skf2(X1))
| ssPv1(skf3(X1)) ),
inference(csr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1910,c_0_1911]),c_0_1791]),c_0_1793]),
[final] ).
cnf(c_0_1938,negated_conjecture,
( ~ ssRr(X4,X5)
| ~ ssRr(X5,X1)
| ~ ssRr(X3,X1)
| ~ ssRr(X1,skf3(X2))
| ~ ssPv1(X4)
| ~ ssPv1(X3)
| ssPv1(X2)
| ssPv3(X1) ),
inference(spm,[status(thm)],[c_0_1320,c_0_77]),
[final] ).
cnf(c_0_1939,negated_conjecture,
( ~ ssRr(X3,X1)
| ~ ssRr(skf3(skf3(skf3(X2))),X3)
| ~ ssPv3(X2)
| ~ ssPv3(X1) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_1913,c_0_77]),c_0_1914]),
[final] ).
cnf(c_0_1940,negated_conjecture,
( ~ ssRr(X3,X1)
| ~ ssRr(skf3(skf2(skf2(X2))),X3)
| ~ ssPv3(X2)
| ~ ssPv3(X1) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_1915,c_0_77]),c_0_1916]),
[final] ).
cnf(c_0_1941,negated_conjecture,
( ~ ssRr(X3,X2)
| ~ ssRr(skf3(skf3(X1)),X3)
| ~ ssPv3(X2)
| ~ ssPv3(skf2(X1)) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_1917,c_0_77]),c_0_1918]),
[final] ).
cnf(c_0_1942,negated_conjecture,
( ~ ssRr(X3,X2)
| ~ ssRr(skf3(skf2(X1)),X3)
| ~ ssPv3(X2)
| ~ ssPv3(skf3(X1)) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_1919,c_0_77]),c_0_1920]),
[final] ).
cnf(c_0_1943,negated_conjecture,
( ~ ssPv3(X1)
| ssPv3(skf2(skf2(X1))) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_1820,c_0_1893]),c_0_1921]),
[final] ).
cnf(c_0_1945,negated_conjecture,
( ~ ssRr(X4,X2)
| ~ ssRr(X1,X4)
| ~ ssRr(X1,X3)
| ~ ssPv1(X3)
| ~ ssPv3(X2)
| ssPv3(X1) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_712,c_0_1922]),c_0_1836]),
[final] ).
cnf(c_0_1946,negated_conjecture,
( ~ ssPv1(X1)
| ssPv1(skf2(skf3(skf3(X1))))
| ssPv3(skf3(skf3(X1)))
| ssPv4(skf2(skf3(skf3(X1)))) ),
inference(spm,[status(thm)],[c_0_1886,c_0_77]),
[final] ).
cnf(c_0_1947,negated_conjecture,
( ~ ssPv1(skf3(skf3(X1)))
| ssPv1(skf2(X1)) ),
inference(spm,[status(thm)],[c_0_1829,c_0_1923]),
[final] ).
cnf(c_0_1948,negated_conjecture,
( ~ ssPv3(X1)
| ~ ssPv3(skf3(X1)) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_1749,c_0_1786]),c_0_1924]),
[final] ).
cnf(c_0_1949,negated_conjecture,
( ~ ssRr(X2,skf3(X1))
| ~ ssPv3(X2)
| ssPv3(skf2(skf2(X1))) ),
inference(spm,[status(thm)],[c_0_1860,c_0_77]),
[final] ).
cnf(c_0_1950,negated_conjecture,
( ~ ssRr(X4,X5)
| ~ ssRr(X5,X1)
| ~ ssRr(X1,X3)
| ~ ssRr(X2,skf3(X1))
| ~ ssPv1(X4)
| ~ ssPv3(skf2(X3))
| ssPv1(X2)
| ssPv2(X1) ),
inference(spm,[status(thm)],[c_0_1925,c_0_77]),
[final] ).
cnf(c_0_1951,negated_conjecture,
( ~ ssRr(X3,X5)
| ~ ssRr(X2,X4)
| ~ ssRr(X5,skf3(skf3(X1)))
| ~ ssRr(X4,skf3(skf3(X1)))
| ~ ssPv1(X3)
| ~ ssPv3(X1)
| ssPv1(X2)
| ssPv2(skf3(skf3(X1))) ),
inference(spm,[status(thm)],[c_0_1926,c_0_77]),
[final] ).
cnf(c_0_1953,negated_conjecture,
( ~ ssRr(X3,X2)
| ~ ssRr(X1,X3)
| ~ ssPv1(X1)
| ~ ssPv3(X2)
| ssPv3(X1) ),
inference(spm,[status(thm)],[c_0_1928,c_0_53]),
[final] ).
cnf(c_0_1954,negated_conjecture,
( ~ ssRr(X1,X2)
| ~ ssPv3(skf2(X2))
| ssPv1(X1) ),
inference(spm,[status(thm)],[c_0_1865,c_0_1793]),
[final] ).
cnf(c_0_1955,negated_conjecture,
( ~ ssRr(X4,X3)
| ~ ssRr(skf3(X1),X2)
| ~ ssRr(skf3(skf3(X1)),X4)
| ~ ssPv3(X3)
| ssPv3(X2)
| ssPv4(skf3(skf3(X1)))
| ssPv2(X1) ),
inference(spm,[status(thm)],[c_0_1929,c_0_77]),
[final] ).
cnf(c_0_1956,negated_conjecture,
( ~ ssRr(X3,X5)
| ~ ssRr(X4,X2)
| ~ ssRr(X5,skf3(skf3(X1)))
| ~ ssRr(skf3(skf3(X1)),X4)
| ~ ssPv3(X3)
| ~ ssPv3(skf3(skf3(X1)))
| ssPv3(X2)
| ssPv2(X1) ),
inference(spm,[status(thm)],[c_0_1930,c_0_77]),
[final] ).
cnf(c_0_1957,negated_conjecture,
( ~ ssRr(X2,X3)
| ~ ssRr(X3,skf3(X1))
| ~ ssPv3(X2)
| ssPv3(skf3(X1)) ),
inference(csr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1835,c_0_77]),c_0_1836]),c_0_1931]),
[final] ).
cnf(c_0_1961,negated_conjecture,
( ~ ssRr(X3,X2)
| ~ ssRr(skf3(skf3(X1)),X3)
| ~ ssPv3(X2)
| ssPv3(X1) ),
inference(spm,[status(thm)],[c_0_1934,c_0_53]),
[final] ).
cnf(c_0_1962,negated_conjecture,
( ~ ssRr(X3,X2)
| ~ ssRr(skf3(X1),X3)
| ~ ssPv3(X2)
| ssPv3(skf2(X1)) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1834,c_0_77]),c_0_1791]),
[final] ).
cnf(c_0_1963,negated_conjecture,
( ~ ssPv3(skf2(X1))
| ~ ssPv3(skf2(skf3(X1))) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1791,c_0_1935]),c_0_1791]),
[final] ).
cnf(c_0_1964,negated_conjecture,
( ~ ssPv1(skf2(X1))
| ssPv1(skf3(skf3(X1))) ),
inference(csr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1936,c_0_1911]),c_0_1791]),c_0_1813]),
[final] ).
cnf(c_0_1967,negated_conjecture,
( ~ ssRr(X3,X4)
| ~ ssRr(X4,skf3(skf3(X1)))
| ~ ssRr(X2,skf3(skf3(X1)))
| ~ ssPv1(X3)
| ~ ssPv1(X2)
| ssPv1(X1)
| ssPv3(skf3(skf3(X1))) ),
inference(spm,[status(thm)],[c_0_1938,c_0_77]),
[final] ).
cnf(c_0_1969,negated_conjecture,
( ~ ssRr(skf2(skf3(skf3(skf3(X2)))),X1)
| ~ ssPv3(X2)
| ~ ssPv3(X1) ),
inference(spm,[status(thm)],[c_0_1939,c_0_53]),
[final] ).
cnf(c_0_1970,negated_conjecture,
( ~ ssRr(skf2(skf3(skf2(skf2(X2)))),X1)
| ~ ssPv3(X2)
| ~ ssPv3(X1) ),
inference(spm,[status(thm)],[c_0_1940,c_0_53]),
[final] ).
cnf(c_0_1971,negated_conjecture,
( ~ ssRr(skf2(skf3(skf3(X1))),X2)
| ~ ssPv3(X2)
| ~ ssPv3(skf2(X1)) ),
inference(spm,[status(thm)],[c_0_1941,c_0_53]),
[final] ).
cnf(c_0_1972,negated_conjecture,
( ~ ssRr(skf2(skf3(skf2(X1))),X2)
| ~ ssPv3(X2)
| ~ ssPv3(skf3(X1)) ),
inference(spm,[status(thm)],[c_0_1942,c_0_53]),
[final] ).
cnf(c_0_1973,negated_conjecture,
( ~ ssRr(X4,X3)
| ~ ssRr(X2,X4)
| ~ ssRr(X2,skf2(skf2(X1)))
| ~ ssPv1(skf3(X1))
| ~ ssPv3(X3)
| ssPv3(X2)
| ssPv3(skf2(X1)) ),
inference(csr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_712,c_0_1851]),c_0_1836]),c_0_1829]),
[final] ).
cnf(c_0_1974,negated_conjecture,
( ~ ssPv3(X1)
| ssPv3(skf3(skf2(X1))) ),
inference(spm,[status(thm)],[c_0_1931,c_0_1943]),
[final] ).
cnf(c_0_1976,negated_conjecture,
( ~ ssPv3(X1)
| ssPv1(skf3(skf3(skf3(X1)))) ),
inference(spm,[status(thm)],[c_0_1936,c_0_1888]),
[final] ).
cnf(c_0_1977,negated_conjecture,
( ~ ssRr(X3,X2)
| ~ ssRr(X1,X3)
| ~ ssPv1(skf2(X1))
| ~ ssPv3(X2)
| ssPv3(X1) ),
inference(spm,[status(thm)],[c_0_1945,c_0_53]),
[final] ).
cnf(c_0_1979,negated_conjecture,
( ~ ssPv1(X1)
| ssPv1(skf3(skf3(skf3(X1)))) ),
inference(csr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1936,c_0_1946]),c_0_1791]),c_0_1813]),
[final] ).
cnf(c_0_1980,negated_conjecture,
( ~ ssPv1(X1)
| ssPv1(skf2(skf2(skf2(X1)))) ),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1947,c_0_1852]),c_0_1836]),c_0_1791]),
[final] ).
cnf(c_0_1981,negated_conjecture,
( ~ ssPv3(skf3(skf3(X1)))
| ssPv1(skf2(X1)) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_1871,c_0_1793]),c_0_1948]),
[final] ).
cnf(c_0_1982,negated_conjecture,
( ~ ssPv3(X1)
| ~ ssPv3(skf2(skf2(skf2(X1)))) ),
inference(spm,[status(thm)],[c_0_1873,c_0_1893]),
[final] ).
cnf(c_0_1983,negated_conjecture,
( ~ ssPv3(skf3(skf3(X1)))
| ssPv3(skf2(skf2(X1))) ),
inference(spm,[status(thm)],[c_0_1949,c_0_77]),
[final] ).
cnf(c_0_1984,negated_conjecture,
( ~ ssRr(X4,X2)
| ~ ssRr(X1,X4)
| ~ ssRr(X1,X3)
| ~ ssPv1(skf3(X3))
| ~ ssPv3(X2)
| ssPv3(X1) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_712,c_0_1838]),c_0_1836]),
[final] ).
cnf(c_0_1985,negated_conjecture,
( ~ ssRr(X3,X4)
| ~ ssRr(X4,X1)
| ~ ssRr(X1,X2)
| ~ ssPv1(X3)
| ~ ssPv3(skf2(X2))
| ssPv1(skf3(skf3(X1)))
| ssPv2(X1) ),
inference(spm,[status(thm)],[c_0_1950,c_0_77]),
[final] ).
cnf(c_0_1986,negated_conjecture,
( ~ ssRr(X3,X4)
| ~ ssRr(X4,skf3(skf3(X2)))
| ~ ssRr(X1,skf3(skf3(skf3(X2))))
| ~ ssPv1(X3)
| ~ ssPv3(X2)
| ssPv1(X1) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_1951,c_0_77]),c_0_1952]),
[final] ).
cnf(c_0_1987,negated_conjecture,
( ~ ssRr(X4,X5)
| ~ ssRr(X2,X1)
| ~ ssRr(X5,skf2(X1))
| ~ ssRr(skf2(X1),X3)
| ~ ssPv1(X4)
| ~ ssPv3(skf2(X3))
| ssPv1(X2)
| ssPv2(skf2(X1)) ),
inference(spm,[status(thm)],[c_0_1925,c_0_53]),
[final] ).
cnf(c_0_1988,negated_conjecture,
( ~ ssRr(skf2(X1),X2)
| ~ ssPv1(X1)
| ~ ssPv3(X2)
| ssPv3(X1) ),
inference(spm,[status(thm)],[c_0_1953,c_0_53]),
[final] ).
cnf(c_0_1989,negated_conjecture,
( ~ ssPv3(skf2(skf2(X1)))
| ssPv1(X1) ),
inference(spm,[status(thm)],[c_0_1954,c_0_53]),
[final] ).
cnf(c_0_1990,negated_conjecture,
( ~ ssRr(skf3(X3),X1)
| ~ ssRr(skf2(skf3(skf3(X3))),X2)
| ~ ssPv3(X2)
| ssPv3(X1) ),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1955,c_0_53]),c_0_1836]),c_0_1791]),
[final] ).
cnf(c_0_1992,negated_conjecture,
( ~ ssRr(X2,skf3(skf3(X1)))
| ~ ssPv3(X2)
| ssPv3(skf3(X1)) ),
inference(spm,[status(thm)],[c_0_1957,c_0_77]),
[final] ).
cnf(c_0_1993,negated_conjecture,
( ~ ssRr(X4,X1)
| ~ ssRr(X3,X4)
| ~ ssRr(X3,X2)
| ~ ssPv3(X2)
| ~ ssPv3(X1) ),
inference(csr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_712,c_0_1866]),c_0_1836]),c_0_1859]),
[final] ).
cnf(c_0_1994,negated_conjecture,
( ~ ssRr(skf2(skf3(skf2(X1))),X2)
| ~ ssPv1(skf3(X1))
| ~ ssPv3(X2)
| ssPv3(X1) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_1958,c_0_53]),c_0_1959]),
[final] ).
cnf(c_0_1996,negated_conjecture,
( ~ ssPv1(X1)
| ssPv1(skf3(skf2(skf2(X1)))) ),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1829,c_0_1852]),c_0_1690]),c_0_1791]),
[final] ).
cnf(c_0_1998,negated_conjecture,
( ~ ssRr(skf2(skf3(skf3(X1))),X2)
| ~ ssPv3(X2)
| ssPv3(X1) ),
inference(spm,[status(thm)],[c_0_1961,c_0_53]),
[final] ).
cnf(c_0_1999,negated_conjecture,
( ~ ssRr(skf2(skf3(X1)),X2)
| ~ ssPv3(X2)
| ssPv3(skf2(X1)) ),
inference(spm,[status(thm)],[c_0_1962,c_0_53]),
[final] ).
cnf(c_0_2001,negated_conjecture,
( ~ ssRr(X1,X2)
| ~ ssPv1(skf2(skf2(X2)))
| ssPv1(X1) ),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_696,c_0_1964]),c_0_1690]),c_0_1791]),
[final] ).
cnf(c_0_2003,negated_conjecture,
( ~ ssRr(skf2(skf3(X1)),X2)
| ~ ssPv3(X2)
| ~ ssPv3(X1) ),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1848,c_0_53]),c_0_1791]),c_0_1791]),
[final] ).
cnf(c_0_2005,negated_conjecture,
( ~ ssPv3(skf3(skf3(X1)))
| ssPv1(X1) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_1966,c_0_1793]),c_0_1948]),
[final] ).
cnf(c_0_2007,negated_conjecture,
( ~ ssRr(X1,X2)
| ~ ssPv1(X2)
| ssPv1(X1) ),
inference(spm,[status(thm)],[c_0_1865,c_0_1922]),
[final] ).
cnf(c_0_2008,negated_conjecture,
( ~ ssRr(X4,X3)
| ~ ssRr(X1,X4)
| ~ ssRr(X1,skf3(skf3(X2)))
| ~ ssPv1(X2)
| ~ ssPv3(X3)
| ssPv3(X1)
| ssPv3(skf3(skf3(X2)))
| ssPv4(skf2(skf3(skf3(X2))))
| ssPv2(X1) ),
inference(spm,[status(thm)],[c_0_712,c_0_1946]),
[final] ).
cnf(c_0_2011,negated_conjecture,
( ~ ssRr(X4,X3)
| ~ ssRr(X1,X4)
| ~ ssRr(X1,skf3(X2))
| ~ ssPv1(skf2(X2))
| ~ ssPv3(X3)
| ssPv3(X1)
| ssPv3(skf3(X2))
| ssPv4(skf2(skf3(X2)))
| ssPv2(X1) ),
inference(spm,[status(thm)],[c_0_712,c_0_1911]),
[final] ).
cnf(c_0_2012,negated_conjecture,
( ~ ssRr(X4,X6)
| ~ ssRr(X6,X2)
| ~ ssRr(X3,X5)
| ~ ssRr(X5,X2)
| ~ ssRr(X2,skf3(X1))
| ~ ssPv3(X4)
| ssPv1(X3)
| ssPv4(X2)
| ssPv2(X1) ),
inference(spm,[status(thm)],[c_0_1696,c_0_77]),
[final] ).
cnf(c_0_2013,negated_conjecture,
( ~ ssRr(X4,X2)
| ~ ssRr(X3,X2)
| ~ ssRr(X2,skf3(X1))
| ~ ssPv3(X4)
| ssPv3(X3)
| ssPv3(X2)
| ssPv2(X1) ),
inference(spm,[status(thm)],[c_0_767,c_0_77]),
[final] ).
cnf(c_0_2014,negated_conjecture,
( ~ ssPv3(X1)
| ~ ssPv3(skf2(skf2(skf3(skf3(skf3(X1)))))) ),
inference(spm,[status(thm)],[c_0_1969,c_0_53]),
[final] ).
cnf(c_0_2015,negated_conjecture,
( ~ ssPv3(X1)
| ~ ssPv3(skf2(skf2(skf3(skf2(skf2(X1)))))) ),
inference(spm,[status(thm)],[c_0_1970,c_0_53]),
[final] ).
cnf(c_0_2016,negated_conjecture,
( ~ ssPv3(skf2(X1))
| ~ ssPv3(skf2(skf2(skf3(skf3(X1))))) ),
inference(spm,[status(thm)],[c_0_1971,c_0_53]),
[final] ).
cnf(c_0_2017,negated_conjecture,
( ~ ssPv3(skf3(X1))
| ~ ssPv3(skf2(skf2(skf3(skf2(X1))))) ),
inference(spm,[status(thm)],[c_0_1972,c_0_53]),
[final] ).
cnf(c_0_2018,negated_conjecture,
( ~ ssPv1(skf3(X1))
| ssPv1(skf2(skf2(X1))) ),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1947,c_0_1466]),c_0_1836]),c_0_1791]),
[final] ).
cnf(c_0_2019,negated_conjecture,
( ~ ssRr(X3,X2)
| ~ ssRr(skf3(skf2(skf2(X1))),X3)
| ~ ssPv1(skf3(X1))
| ~ ssPv3(X2)
| ssPv3(skf3(skf2(skf2(X1)))) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_1973,c_0_77]),c_0_1974]),
[final] ).
cnf(c_0_2020,negated_conjecture,
( ~ ssRr(X3,X2)
| ~ ssRr(skf3(skf2(skf2(X1))),X3)
| ~ ssPv1(X1)
| ~ ssPv3(X2)
| ssPv3(skf3(skf2(skf2(X1)))) ),
inference(spm,[status(thm)],[c_0_1975,c_0_77]),
[final] ).
cnf(c_0_2021,negated_conjecture,
( ~ ssPv3(X1)
| ssPv1(skf2(skf3(X1))) ),
inference(spm,[status(thm)],[c_0_1947,c_0_1976]),
[final] ).
cnf(c_0_2022,negated_conjecture,
( ~ ssRr(X3,X2)
| ~ ssRr(skf3(skf3(X1)),X3)
| ~ ssPv1(X1)
| ~ ssPv3(X2)
| ssPv3(skf3(skf3(X1))) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1977,c_0_1946]),c_0_1791]),
[final] ).
cnf(c_0_2024,negated_conjecture,
( ~ ssPv1(X1)
| ssPv1(skf2(skf3(X1))) ),
inference(spm,[status(thm)],[c_0_1947,c_0_1979]),
[final] ).
cnf(c_0_2025,negated_conjecture,
( ~ ssRr(X3,X2)
| ~ ssRr(skf2(skf2(X1)),X3)
| ~ ssPv1(X1)
| ~ ssPv3(X2)
| ssPv3(skf2(skf2(X1))) ),
inference(spm,[status(thm)],[c_0_1977,c_0_1980]),
[final] ).
cnf(c_0_2026,negated_conjecture,
( ~ ssRr(X3,X2)
| ~ ssRr(skf3(skf2(X1)),X3)
| ~ ssPv1(X1)
| ~ ssPv3(X2)
| ssPv3(skf3(skf2(X1))) ),
inference(spm,[status(thm)],[c_0_1928,c_0_77]),
[final] ).
cnf(c_0_2027,negated_conjecture,
( ~ ssRr(X3,X2)
| ~ ssRr(skf3(X1),X3)
| ~ ssPv1(skf2(X1))
| ~ ssPv3(X2)
| ssPv3(skf3(X1)) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1977,c_0_1911]),c_0_1791]),
[final] ).
cnf(c_0_2028,negated_conjecture,
( ~ ssRr(X4,X3)
| ~ ssRr(X1,X4)
| ~ ssRr(X1,X2)
| ~ ssPv3(X3)
| ~ ssPv3(skf3(skf3(X2)))
| ssPv3(X1) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_712,c_0_1981]),c_0_1836]),
[final] ).
cnf(c_0_2029,negated_conjecture,
( ~ ssPv3(X1)
| ~ ssPv3(skf3(skf3(skf2(X1)))) ),
inference(spm,[status(thm)],[c_0_1982,c_0_1983]),
[final] ).
cnf(c_0_2030,negated_conjecture,
( ~ ssRr(X3,X2)
| ~ ssRr(skf2(X1),X3)
| ~ ssPv1(X1)
| ~ ssPv3(X2)
| ssPv3(skf2(X1)) ),
inference(spm,[status(thm)],[c_0_1977,c_0_1903]),
[final] ).
cnf(c_0_2031,negated_conjecture,
( ~ ssRr(X3,X1)
| ~ ssRr(skf2(X2),X3)
| ~ ssPv3(X2)
| ~ ssPv3(X1) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_1915,c_0_53]),c_0_1873]),
[final] ).
cnf(c_0_2032,negated_conjecture,
( ~ ssRr(X3,X2)
| ~ ssRr(X1,X3)
| ~ ssPv1(skf3(skf2(X1)))
| ~ ssPv3(X2)
| ssPv3(X1) ),
inference(spm,[status(thm)],[c_0_1984,c_0_53]),
[final] ).
cnf(c_0_2033,negated_conjecture,
( ~ ssRr(X3,X2)
| ~ ssRr(skf3(X1),X3)
| ~ ssPv1(X1)
| ~ ssPv3(X2)
| ssPv3(skf3(X1)) ),
inference(spm,[status(thm)],[c_0_1945,c_0_77]),
[final] ).
cnf(c_0_2034,negated_conjecture,
( ~ ssRr(X2,X3)
| ~ ssRr(X3,X1)
| ~ ssPv1(X2)
| ~ ssPv3(skf2(skf2(X1)))
| ssPv1(skf3(skf3(X1))) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1985,c_0_53]),c_0_1836]),
[final] ).
cnf(c_0_2035,negated_conjecture,
( ~ ssRr(X2,X3)
| ~ ssRr(X3,skf3(X1))
| ~ ssPv1(X2)
| ~ ssPv3(skf2(X1))
| ssPv1(skf3(skf3(skf3(X1)))) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1985,c_0_77]),c_0_1836]),
[final] ).
cnf(c_0_2036,negated_conjecture,
( ~ ssRr(X3,X2)
| ~ ssRr(X1,X3)
| ~ ssPv3(X2)
| ~ ssPv3(skf3(X1)) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_1919,c_0_53]),c_0_1948]),
[final] ).
cnf(c_0_2037,negated_conjecture,
( ~ ssRr(X3,X2)
| ~ ssRr(skf2(X1),X3)
| ~ ssPv1(skf3(X1))
| ~ ssPv3(X2)
| ssPv3(skf2(X1)) ),
inference(spm,[status(thm)],[c_0_1973,c_0_53]),
[final] ).
cnf(c_0_2038,negated_conjecture,
( ~ ssRr(X2,X3)
| ~ ssRr(X3,skf3(skf3(X1)))
| ~ ssPv1(X2)
| ~ ssPv3(X1)
| ssPv1(skf3(skf3(skf3(skf3(X1))))) ),
inference(spm,[status(thm)],[c_0_1986,c_0_77]),
[final] ).
cnf(c_0_2039,negated_conjecture,
( ~ ssRr(X3,X4)
| ~ ssRr(X1,X2)
| ~ ssRr(X4,skf2(X2))
| ~ ssPv1(X3)
| ~ ssPv3(skf2(skf2(skf2(X2))))
| ssPv1(X1) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1987,c_0_53]),c_0_1690]),
[final] ).
cnf(c_0_2040,negated_conjecture,
( ~ ssPv3(skf2(skf2(X1)))
| ssPv3(X1) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_1988,c_0_53]),c_0_1989]),
[final] ).
cnf(c_0_2041,negated_conjecture,
( ~ ssRr(skf3(X2),X1)
| ~ ssPv3(skf2(skf2(skf3(skf3(X2)))))
| ssPv3(X1) ),
inference(spm,[status(thm)],[c_0_1990,c_0_53]),
[final] ).
cnf(c_0_2042,negated_conjecture,
( ~ ssRr(skf3(X3),X1)
| ~ ssRr(X2,skf3(skf3(skf3(X3))))
| ~ ssPv3(X2)
| ssPv3(X1) ),
inference(csr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1991,c_0_77]),c_0_1836]),c_0_1992]),
[final] ).
cnf(c_0_2043,negated_conjecture,
( ~ ssRr(X3,X2)
| ~ ssRr(X1,X3)
| ~ ssPv3(X2)
| ~ ssPv3(skf2(X1)) ),
inference(spm,[status(thm)],[c_0_1993,c_0_53]),
[final] ).
cnf(c_0_2044,negated_conjecture,
( ~ ssPv1(skf3(X1))
| ~ ssPv3(skf2(skf2(skf3(skf2(X1)))))
| ssPv3(X1) ),
inference(spm,[status(thm)],[c_0_1994,c_0_53]),
[final] ).
cnf(c_0_2045,negated_conjecture,
( ~ ssPv3(X1)
| ssPv1(skf2(skf2(X1))) ),
inference(spm,[status(thm)],[c_0_1858,c_0_1862]),
[final] ).
cnf(c_0_2046,negated_conjecture,
( ~ ssRr(X1,X2)
| ~ ssPv1(skf3(skf2(X2)))
| ssPv1(X1) ),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_696,c_0_1885]),c_0_1690]),c_0_1791]),
[final] ).
cnf(c_0_2047,negated_conjecture,
( ~ ssRr(X1,skf2(skf2(X2)))
| ~ ssPv1(skf3(X2))
| ssPv1(X1) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_1865,c_0_1851]),c_0_1829]),c_0_1877]),
[final] ).
cnf(c_0_2048,negated_conjecture,
( ~ ssRr(X1,skf2(skf2(skf2(X2))))
| ~ ssPv1(X2)
| ssPv1(X1) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_1865,c_0_1995]),c_0_1996]),c_0_1877]),
[final] ).
cnf(c_0_2050,negated_conjecture,
( ~ ssPv3(skf2(skf2(skf3(skf3(X1)))))
| ssPv3(X1) ),
inference(spm,[status(thm)],[c_0_1998,c_0_53]),
[final] ).
cnf(c_0_2051,negated_conjecture,
( ~ ssPv3(skf2(skf2(skf3(X1))))
| ssPv3(skf2(X1)) ),
inference(spm,[status(thm)],[c_0_1999,c_0_53]),
[final] ).
cnf(c_0_2052,negated_conjecture,
( ~ ssPv3(skf2(X1))
| ssPv1(skf3(X1)) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_1839,c_0_2000]),c_0_1793]),
[final] ).
cnf(c_0_2053,negated_conjecture,
( ~ ssPv3(skf3(X1))
| ssPv3(skf2(skf2(skf2(X1)))) ),
inference(spm,[status(thm)],[c_0_1874,c_0_77]),
[final] ).
cnf(c_0_2054,negated_conjecture,
( ~ ssRr(X1,X2)
| ~ ssPv3(skf2(skf2(X2)))
| ssPv1(X1) ),
inference(spm,[status(thm)],[c_0_2001,c_0_1793]),
[final] ).
cnf(c_0_2055,negated_conjecture,
( ~ ssRr(X1,X2)
| ~ ssPv3(X2)
| ssPv3(skf2(X1)) ),
inference(spm,[status(thm)],[c_0_1962,c_0_77]),
[final] ).
cnf(c_0_2057,negated_conjecture,
( ~ ssPv3(X1)
| ~ ssPv3(skf2(skf2(skf3(X1)))) ),
inference(spm,[status(thm)],[c_0_2003,c_0_53]),
[final] ).
cnf(c_0_2058,negated_conjecture,
( ~ ssRr(X2,X3)
| ~ ssRr(X3,X1)
| ~ ssPv1(X2)
| ssPv1(X1) ),
inference(csr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_2004,c_0_77]),c_0_1836]),c_0_2005]),
[final] ).
cnf(c_0_2059,negated_conjecture,
( ~ ssRr(skf3(X1),X2)
| ~ ssPv3(X2)
| ssPv3(X1) ),
inference(spm,[status(thm)],[c_0_1961,c_0_77]),
[final] ).
cnf(c_0_2061,negated_conjecture,
( ~ ssPv1(skf2(skf3(X1)))
| ssPv1(X1) ),
inference(spm,[status(thm)],[c_0_1846,c_0_1885]),
[final] ).
cnf(c_0_2062,negated_conjecture,
( ~ ssRr(X1,X2)
| ~ ssPv3(skf3(skf3(X2)))
| ssPv1(X1) ),
inference(spm,[status(thm)],[c_0_1865,c_0_1981]),
[final] ).
cnf(c_0_2063,negated_conjecture,
( ~ ssRr(X3,X2)
| ~ ssRr(skf3(skf3(skf3(X1))),X3)
| ~ ssPv1(X1)
| ~ ssPv3(X2)
| ssPv3(skf3(skf3(X1)))
| ssPv3(skf3(skf3(skf3(X1))))
| ssPv2(skf3(skf3(skf3(X1)))) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_2008,c_0_77]),c_0_1792]),
[final] ).
cnf(c_0_2066,negated_conjecture,
( ~ ssRr(X3,X2)
| ~ ssRr(skf3(skf3(X1)),X3)
| ~ ssPv1(skf2(X1))
| ~ ssPv3(X2)
| ssPv3(skf3(X1))
| ssPv3(skf3(skf3(X1)))
| ssPv2(skf3(skf3(X1))) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_2011,c_0_77]),c_0_1792]),
[final] ).
cnf(c_0_2067,negated_conjecture,
( ~ ssRr(X3,X5)
| ~ ssRr(X2,X4)
| ~ ssRr(X5,skf3(skf3(X1)))
| ~ ssRr(X4,skf3(skf3(X1)))
| ~ ssPv3(X3)
| ssPv1(X2)
| ssPv4(skf3(skf3(X1)))
| ssPv2(X1) ),
inference(spm,[status(thm)],[c_0_2012,c_0_77]),
[final] ).
cnf(c_0_2068,negated_conjecture,
( ~ ssPv1(skf2(X1))
| ssPv1(skf2(skf3(X1)))
| ssPv3(skf3(X1))
| ssPv4(X1) ),
inference(spm,[status(thm)],[c_0_1824,c_0_53]),
[final] ).
cnf(c_0_2069,negated_conjecture,
( ~ ssRr(X3,skf3(skf3(X1)))
| ~ ssRr(X2,skf3(skf3(X1)))
| ~ ssPv3(X3)
| ssPv3(X2)
| ssPv3(skf3(skf3(X1)))
| ssPv2(X1) ),
inference(spm,[status(thm)],[c_0_2013,c_0_77]),
[final] ).
cnf(c_0_2070,negated_conjecture,
( ~ ssRr(skf2(skf3(X1)),X2)
| ~ ssPv1(X2)
| ssPv1(X1)
| ssPv3(skf3(X1))
| ssPv4(skf2(skf3(X1))) ),
inference(spm,[status(thm)],[c_0_460,c_0_53]),
[final] ).
cnf(c_0_2071,negated_conjecture,
( ~ ssPv3(X1)
| ~ ssPv3(skf3(skf3(skf3(skf3(skf3(X1)))))) ),
inference(spm,[status(thm)],[c_0_2014,c_0_1983]),
[final] ).
cnf(c_0_2072,negated_conjecture,
( ~ ssPv3(X1)
| ~ ssPv3(skf3(skf2(skf3(skf3(skf3(X1)))))) ),
inference(spm,[status(thm)],[c_0_2014,c_0_1890]),
[final] ).
cnf(c_0_2073,negated_conjecture,
( ~ ssRr(skf3(skf3(X2)),X1)
| ~ ssPv3(X2)
| ~ ssPv3(X1) ),
inference(spm,[status(thm)],[c_0_1939,c_0_77]),
[final] ).
cnf(c_0_2074,negated_conjecture,
( ~ ssPv3(X1)
| ~ ssPv3(skf3(skf3(skf3(skf2(skf2(X1)))))) ),
inference(spm,[status(thm)],[c_0_2015,c_0_1983]),
[final] ).
cnf(c_0_2075,negated_conjecture,
( ~ ssPv3(X1)
| ~ ssPv3(skf3(skf2(skf3(skf2(skf2(X1)))))) ),
inference(spm,[status(thm)],[c_0_2015,c_0_1890]),
[final] ).
cnf(c_0_2076,negated_conjecture,
( ~ ssPv3(skf2(X1))
| ~ ssPv3(skf3(skf3(skf3(skf3(X1))))) ),
inference(spm,[status(thm)],[c_0_2016,c_0_1983]),
[final] ).
cnf(c_0_2077,negated_conjecture,
( ~ ssPv3(skf2(X1))
| ~ ssPv3(skf3(skf2(skf3(skf3(X1))))) ),
inference(spm,[status(thm)],[c_0_2016,c_0_1890]),
[final] ).
cnf(c_0_2078,negated_conjecture,
( ~ ssRr(X4,X2)
| ~ ssRr(X1,X4)
| ~ ssRr(X1,skf2(skf2(X3)))
| ~ ssPv1(X3)
| ~ ssPv3(X2)
| ssPv3(X1) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_712,c_0_1980]),c_0_1836]),
[final] ).
cnf(c_0_2079,negated_conjecture,
( ~ ssRr(skf3(X1),X2)
| ~ ssPv3(X2)
| ~ ssPv3(skf2(X1)) ),
inference(spm,[status(thm)],[c_0_1941,c_0_77]),
[final] ).
cnf(c_0_2080,negated_conjecture,
( ~ ssPv3(skf3(X1))
| ~ ssPv3(skf3(skf3(skf3(skf2(X1))))) ),
inference(spm,[status(thm)],[c_0_2017,c_0_1983]),
[final] ).
cnf(c_0_2081,negated_conjecture,
( ~ ssPv3(skf3(X1))
| ~ ssPv3(skf3(skf2(skf3(skf2(X1))))) ),
inference(spm,[status(thm)],[c_0_2017,c_0_1890]),
[final] ).
cnf(c_0_2082,negated_conjecture,
( ~ ssRr(X4,X2)
| ~ ssRr(X1,X4)
| ~ ssRr(X1,skf2(X3))
| ~ ssPv1(skf3(X3))
| ~ ssPv3(X2)
| ssPv3(X1) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_712,c_0_2018]),c_0_1836]),
[final] ).
cnf(c_0_2083,negated_conjecture,
( ~ ssRr(skf2(skf3(skf2(skf2(X1)))),X2)
| ~ ssPv1(skf3(X1))
| ~ ssPv3(X2)
| ssPv3(skf3(skf2(skf2(X1)))) ),
inference(spm,[status(thm)],[c_0_2019,c_0_53]),
[final] ).
cnf(c_0_2084,negated_conjecture,
( ~ ssRr(skf2(skf3(skf2(skf2(X1)))),X2)
| ~ ssPv1(X1)
| ~ ssPv3(X2)
| ssPv3(skf3(skf2(skf2(X1)))) ),
inference(spm,[status(thm)],[c_0_2020,c_0_53]),
[final] ).
cnf(c_0_2085,negated_conjecture,
( ~ ssRr(X4,X2)
| ~ ssRr(X1,X4)
| ~ ssRr(X1,skf3(X3))
| ~ ssPv3(X3)
| ~ ssPv3(X2)
| ssPv3(X1) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_712,c_0_2021]),c_0_1836]),
[final] ).
cnf(c_0_2086,negated_conjecture,
( ~ ssRr(skf2(skf3(skf3(X1))),X2)
| ~ ssPv1(X1)
| ~ ssPv3(X2)
| ssPv3(skf3(skf3(X1))) ),
inference(spm,[status(thm)],[c_0_2022,c_0_53]),
[final] ).
cnf(c_0_2087,negated_conjecture,
( ~ ssRr(X3,X2)
| ~ ssRr(skf3(skf2(X1)),X3)
| ~ ssPv1(skf3(X1))
| ~ ssPv3(X2)
| ssPv3(skf3(skf2(X1))) ),
inference(spm,[status(thm)],[c_0_2023,c_0_77]),
[final] ).
cnf(c_0_2088,negated_conjecture,
( ~ ssRr(X4,X2)
| ~ ssRr(X1,X4)
| ~ ssRr(X1,skf3(X3))
| ~ ssPv1(X3)
| ~ ssPv3(X2)
| ssPv3(X1) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_712,c_0_2024]),c_0_1836]),
[final] ).
cnf(c_0_2089,negated_conjecture,
( ~ ssRr(skf2(skf2(skf2(X1))),X2)
| ~ ssPv1(X1)
| ~ ssPv3(X2)
| ssPv3(skf2(skf2(X1))) ),
inference(spm,[status(thm)],[c_0_2025,c_0_53]),
[final] ).
cnf(c_0_2090,negated_conjecture,
( ~ ssRr(skf2(skf3(skf2(X1))),X2)
| ~ ssPv1(X1)
| ~ ssPv3(X2)
| ssPv3(skf3(skf2(X1))) ),
inference(spm,[status(thm)],[c_0_2026,c_0_53]),
[final] ).
cnf(c_0_2091,negated_conjecture,
( ~ ssRr(skf2(skf3(X1)),X2)
| ~ ssPv1(skf2(X1))
| ~ ssPv3(X2)
| ssPv3(skf3(X1)) ),
inference(spm,[status(thm)],[c_0_2027,c_0_53]),
[final] ).
cnf(c_0_2092,negated_conjecture,
( ~ ssRr(X3,X2)
| ~ ssRr(X1,X3)
| ~ ssPv3(X2)
| ~ ssPv3(skf3(skf3(skf2(X1)))) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_2028,c_0_53]),c_0_2029]),
[final] ).
cnf(c_0_2093,negated_conjecture,
( ~ ssRr(skf2(skf2(X1)),X2)
| ~ ssPv1(X1)
| ~ ssPv3(X2)
| ssPv3(skf2(X1)) ),
inference(spm,[status(thm)],[c_0_2030,c_0_53]),
[final] ).
cnf(c_0_2094,negated_conjecture,
( ~ ssRr(skf2(skf2(X2)),X1)
| ~ ssPv3(X2)
| ~ ssPv3(X1) ),
inference(spm,[status(thm)],[c_0_2031,c_0_53]),
[final] ).
cnf(c_0_2095,negated_conjecture,
( ~ ssRr(X3,X2)
| ~ ssRr(X1,X3)
| ~ ssPv1(skf3(skf3(X1)))
| ~ ssPv3(X2)
| ssPv3(X1) ),
inference(spm,[status(thm)],[c_0_2032,c_0_1923]),
[final] ).
cnf(c_0_2096,negated_conjecture,
( ~ ssRr(skf2(skf3(X1)),X2)
| ~ ssPv1(X1)
| ~ ssPv3(X2)
| ssPv3(skf3(X1)) ),
inference(spm,[status(thm)],[c_0_2033,c_0_53]),
[final] ).
cnf(c_0_2097,negated_conjecture,
( ~ ssRr(X2,X3)
| ~ ssRr(X3,X1)
| ~ ssPv1(X2)
| ~ ssPv3(skf3(skf2(X1)))
| ssPv1(skf3(skf3(X1))) ),
inference(spm,[status(thm)],[c_0_2034,c_0_1890]),
[final] ).
cnf(c_0_2098,negated_conjecture,
( ~ ssRr(X2,skf3(skf3(X1)))
| ~ ssPv1(X2)
| ~ ssPv3(skf2(X1))
| ssPv1(skf3(skf3(skf3(X1)))) ),
inference(spm,[status(thm)],[c_0_2035,c_0_77]),
[final] ).
cnf(c_0_2099,negated_conjecture,
( ~ ssRr(skf2(X1),X2)
| ~ ssPv3(X2)
| ~ ssPv3(skf3(X1)) ),
inference(spm,[status(thm)],[c_0_2036,c_0_53]),
[final] ).
cnf(c_0_2100,negated_conjecture,
( ~ ssRr(skf2(skf2(X1)),X2)
| ~ ssPv1(skf3(X1))
| ~ ssPv3(X2)
| ssPv3(skf2(X1)) ),
inference(spm,[status(thm)],[c_0_2037,c_0_53]),
[final] ).
cnf(c_0_2101,negated_conjecture,
( ~ ssRr(X2,skf3(skf3(skf3(X1))))
| ~ ssPv1(X2)
| ~ ssPv3(X1)
| ssPv1(skf3(skf3(skf3(skf3(X1))))) ),
inference(spm,[status(thm)],[c_0_2038,c_0_77]),
[final] ).
cnf(c_0_2102,negated_conjecture,
( ~ ssRr(X3,X4)
| ~ ssRr(X1,X2)
| ~ ssRr(X4,skf2(X2))
| ~ ssPv1(X3)
| ~ ssPv3(skf3(skf2(skf2(X2))))
| ssPv1(X1) ),
inference(spm,[status(thm)],[c_0_2039,c_0_1890]),
[final] ).
cnf(c_0_2103,negated_conjecture,
( ~ ssPv3(skf3(skf2(X1)))
| ssPv3(X1) ),
inference(spm,[status(thm)],[c_0_2040,c_0_1890]),
[final] ).
cnf(c_0_2104,negated_conjecture,
( ~ ssRr(skf3(X2),X1)
| ~ ssPv3(skf3(skf2(skf3(skf3(X2)))))
| ssPv3(X1) ),
inference(spm,[status(thm)],[c_0_2041,c_0_1890]),
[final] ).
cnf(c_0_2105,negated_conjecture,
( ~ ssRr(X3,X1)
| ~ ssRr(skf3(X2),X3)
| ~ ssPv3(X2)
| ~ ssPv3(X1) ),
inference(spm,[status(thm)],[c_0_1993,c_0_77]),
[final] ).
cnf(c_0_2106,negated_conjecture,
( ~ ssRr(skf3(X2),X1)
| ~ ssPv3(skf3(skf3(skf3(skf3(X2)))))
| ssPv3(X1) ),
inference(spm,[status(thm)],[c_0_2042,c_0_77]),
[final] ).
cnf(c_0_2107,negated_conjecture,
( ~ ssRr(skf3(X2),X1)
| ~ ssPv3(skf2(skf3(X2)))
| ssPv3(X1) ),
inference(spm,[status(thm)],[c_0_2041,c_0_1875]),
[final] ).
cnf(c_0_2108,negated_conjecture,
( ~ ssRr(skf3(X2),X1)
| ~ ssPv3(skf3(skf3(X2)))
| ssPv3(X1) ),
inference(spm,[status(thm)],[c_0_2041,c_0_1943]),
[final] ).
cnf(c_0_2109,negated_conjecture,
( ~ ssRr(skf3(X2),X1)
| ~ ssPv3(X2)
| ssPv3(X1) ),
inference(spm,[status(thm)],[c_0_2041,c_0_1867]),
[final] ).
cnf(c_0_2110,negated_conjecture,
( ~ ssRr(X1,X2)
| ~ ssPv3(X2)
| ~ ssPv3(skf2(skf3(X1))) ),
inference(spm,[status(thm)],[c_0_2043,c_0_77]),
[final] ).
cnf(c_0_2111,negated_conjecture,
( ~ ssPv1(skf3(X1))
| ~ ssPv3(skf3(skf3(skf3(skf2(X1)))))
| ssPv3(X1) ),
inference(spm,[status(thm)],[c_0_2044,c_0_1983]),
[final] ).
cnf(c_0_2112,negated_conjecture,
( ~ ssPv1(skf3(X1))
| ~ ssPv3(skf3(skf2(skf3(skf2(X1)))))
| ssPv3(X1) ),
inference(spm,[status(thm)],[c_0_2044,c_0_1890]),
[final] ).
cnf(c_0_2113,negated_conjecture,
( ~ ssRr(X4,X2)
| ~ ssRr(X1,X4)
| ~ ssRr(X1,skf2(X3))
| ~ ssPv3(X3)
| ~ ssPv3(X2)
| ssPv3(X1) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_712,c_0_2045]),c_0_1836]),
[final] ).
cnf(c_0_2114,negated_conjecture,
( ~ ssRr(X4,X3)
| ~ ssRr(X1,X4)
| ~ ssRr(X1,X2)
| ~ ssPv3(X3)
| ~ ssPv3(skf3(X2))
| ssPv3(X1) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_712,c_0_1872]),c_0_1836]),
[final] ).
cnf(c_0_2115,negated_conjecture,
( ~ ssRr(X1,skf2(skf2(X2)))
| ~ ssPv1(X2)
| ssPv1(X1) ),
inference(spm,[status(thm)],[c_0_1865,c_0_1980]),
[final] ).
cnf(c_0_2116,negated_conjecture,
( ~ ssRr(X1,skf2(X2))
| ~ ssPv1(skf3(X2))
| ssPv1(X1) ),
inference(spm,[status(thm)],[c_0_1865,c_0_2018]),
[final] ).
cnf(c_0_2117,negated_conjecture,
( ~ ssRr(X1,X2)
| ~ ssPv1(skf3(skf3(X2)))
| ssPv1(X1) ),
inference(spm,[status(thm)],[c_0_2046,c_0_1923]),
[final] ).
cnf(c_0_2118,negated_conjecture,
( ~ ssRr(X1,skf3(X2))
| ~ ssPv3(X2)
| ssPv1(X1) ),
inference(spm,[status(thm)],[c_0_1865,c_0_2021]),
[final] ).
cnf(c_0_2119,negated_conjecture,
( ~ ssRr(X1,skf3(X2))
| ~ ssPv1(X2)
| ssPv1(X1) ),
inference(spm,[status(thm)],[c_0_1865,c_0_2024]),
[final] ).
cnf(c_0_2120,negated_conjecture,
( ~ ssPv1(skf3(X1))
| ssPv1(skf3(skf2(skf2(X1)))) ),
inference(spm,[status(thm)],[c_0_2047,c_0_77]),
[final] ).
cnf(c_0_2121,negated_conjecture,
( ~ ssPv1(X1)
| ssPv1(skf3(skf2(skf2(skf2(X1))))) ),
inference(spm,[status(thm)],[c_0_2048,c_0_77]),
[final] ).
cnf(c_0_2122,negated_conjecture,
( ~ ssRr(skf2(skf3(skf2(X1))),X2)
| ~ ssPv1(skf3(X1))
| ~ ssPv3(X2)
| ssPv3(skf3(skf2(X1))) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_2049,c_0_53]),c_0_2003]),
[final] ).
cnf(c_0_2123,negated_conjecture,
( ~ ssPv3(skf3(skf3(skf3(skf3(X1)))))
| ssPv3(X1) ),
inference(spm,[status(thm)],[c_0_2050,c_0_1983]),
[final] ).
cnf(c_0_2124,negated_conjecture,
( ~ ssPv3(skf3(skf3(skf3(X1))))
| ssPv3(skf2(X1)) ),
inference(spm,[status(thm)],[c_0_2051,c_0_1983]),
[final] ).
cnf(c_0_2125,negated_conjecture,
( ~ ssPv3(skf3(skf3(X1)))
| ssPv1(skf3(skf2(X1))) ),
inference(spm,[status(thm)],[c_0_2052,c_0_1983]),
[final] ).
cnf(c_0_2126,negated_conjecture,
( ~ ssPv3(skf3(skf3(X1)))
| ssPv3(skf3(skf2(X1))) ),
inference(spm,[status(thm)],[c_0_1931,c_0_1983]),
[final] ).
cnf(c_0_2127,negated_conjecture,
( ~ ssPv3(skf3(skf2(skf3(X1))))
| ssPv3(skf2(X1)) ),
inference(spm,[status(thm)],[c_0_2051,c_0_1890]),
[final] ).
cnf(c_0_2128,negated_conjecture,
( ~ ssPv3(X1)
| ssPv1(skf3(skf2(skf2(skf2(X1))))) ),
inference(spm,[status(thm)],[c_0_2052,c_0_1893]),
[final] ).
cnf(c_0_2129,negated_conjecture,
( ~ ssPv3(X1)
| ssPv3(skf3(skf2(skf2(skf2(X1))))) ),
inference(spm,[status(thm)],[c_0_1931,c_0_1893]),
[final] ).
cnf(c_0_2130,negated_conjecture,
( ~ ssPv3(skf3(X1))
| ssPv1(skf3(skf2(skf2(X1)))) ),
inference(spm,[status(thm)],[c_0_2052,c_0_2053]),
[final] ).
cnf(c_0_2131,negated_conjecture,
( ~ ssPv3(skf3(X1))
| ssPv3(skf3(skf2(skf2(X1)))) ),
inference(spm,[status(thm)],[c_0_1931,c_0_2053]),
[final] ).
cnf(c_0_2132,negated_conjecture,
( ~ ssRr(X1,skf3(skf3(X2)))
| ~ ssPv3(X2)
| ssPv1(X1) ),
inference(spm,[status(thm)],[c_0_2054,c_0_1867]),
[final] ).
cnf(c_0_2133,negated_conjecture,
( ~ ssRr(X1,skf3(X2))
| ~ ssPv3(skf2(X2))
| ssPv1(X1) ),
inference(spm,[status(thm)],[c_0_2054,c_0_1875]),
[final] ).
cnf(c_0_2134,negated_conjecture,
( ~ ssPv3(X1)
| ssPv1(skf3(skf2(skf3(skf3(X1))))) ),
inference(spm,[status(thm)],[c_0_2052,c_0_1867]),
[final] ).
cnf(c_0_2135,negated_conjecture,
( ~ ssRr(X4,X3)
| ~ ssRr(X1,X4)
| ~ ssRr(X1,X2)
| ~ ssPv3(X3)
| ~ ssPv3(skf2(X2))
| ssPv3(X1) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_712,c_0_1793]),c_0_1836]),
[final] ).
cnf(c_0_2136,negated_conjecture,
( ~ ssPv3(X1)
| ssPv3(skf3(skf2(skf3(skf3(X1))))) ),
inference(spm,[status(thm)],[c_0_1931,c_0_1867]),
[final] ).
cnf(c_0_2137,negated_conjecture,
( ~ ssPv3(skf2(X1))
| ssPv1(skf3(skf2(skf3(X1)))) ),
inference(spm,[status(thm)],[c_0_2052,c_0_1875]),
[final] ).
cnf(c_0_2138,negated_conjecture,
( ~ ssPv3(skf2(X1))
| ssPv3(skf3(skf2(skf3(X1)))) ),
inference(spm,[status(thm)],[c_0_1931,c_0_1875]),
[final] ).
cnf(c_0_2139,negated_conjecture,
( ~ ssPv3(skf2(X1))
| ssPv1(skf3(skf3(X1))) ),
inference(spm,[status(thm)],[c_0_1936,c_0_1894]),
[final] ).
cnf(c_0_2140,negated_conjecture,
( ~ ssPv3(X1)
| ssPv3(skf2(skf3(X1))) ),
inference(spm,[status(thm)],[c_0_2055,c_0_77]),
[final] ).
cnf(c_0_2141,negated_conjecture,
( ~ ssRr(X1,X2)
| ~ ssPv3(X2)
| ~ ssPv3(skf3(skf3(X1))) ),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_2056,c_0_1890]),c_0_1791]),c_0_1791]),
[final] ).
cnf(c_0_2142,negated_conjecture,
( ~ ssRr(skf3(X3),X2)
| ~ ssRr(skf3(X3),X1)
| ~ ssPv3(X2)
| ssPv3(X1) ),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1955,c_0_77]),c_0_1836]),c_0_1791]),
[final] ).
cnf(c_0_2143,negated_conjecture,
( ~ ssPv3(X1)
| ~ ssPv3(skf3(skf2(skf3(X1)))) ),
inference(spm,[status(thm)],[c_0_2057,c_0_1890]),
[final] ).
cnf(c_0_2144,negated_conjecture,
( ~ ssPv3(skf3(skf2(skf3(skf3(X1)))))
| ssPv3(X1) ),
inference(spm,[status(thm)],[c_0_2050,c_0_1890]),
[final] ).
cnf(c_0_2145,negated_conjecture,
( ~ ssPv3(skf3(skf3(X1)))
| ssPv3(X1) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_1820,c_0_1895]),c_0_1839]),
[final] ).
cnf(c_0_2146,negated_conjecture,
( ~ ssRr(X1,skf2(skf2(X2)))
| ~ ssPv3(X2)
| ssPv1(X1) ),
inference(spm,[status(thm)],[c_0_1865,c_0_1891]),
[final] ).
cnf(c_0_2147,negated_conjecture,
( ~ ssRr(X1,skf2(X2))
| ~ ssPv3(skf3(X2))
| ssPv1(X1) ),
inference(spm,[status(thm)],[c_0_1865,c_0_1896]),
[final] ).
cnf(c_0_2148,negated_conjecture,
( ~ ssRr(X2,skf3(X1))
| ~ ssPv1(X2)
| ssPv1(X1) ),
inference(spm,[status(thm)],[c_0_2058,c_0_77]),
[final] ).
cnf(c_0_2149,negated_conjecture,
( ~ ssRr(X2,X1)
| ~ ssPv1(X2)
| ssPv1(skf2(X1)) ),
inference(spm,[status(thm)],[c_0_2058,c_0_53]),
[final] ).
cnf(c_0_2150,negated_conjecture,
( ~ ssRr(X2,skf3(X1))
| ~ ssPv3(X2)
| ssPv1(skf3(skf3(X1))) ),
inference(spm,[status(thm)],[c_0_1837,c_0_77]),
[final] ).
cnf(c_0_2151,negated_conjecture,
( ~ ssRr(X1,X3)
| ~ ssRr(X2,skf3(skf2(X3)))
| ~ ssPv3(X2)
| ssPv1(X1) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1725,c_0_77]),c_0_1791]),
[final] ).
cnf(c_0_2152,negated_conjecture,
( ~ ssRr(X1,X2)
| ~ ssPv3(skf3(X2))
| ssPv1(X1) ),
inference(spm,[status(thm)],[c_0_1861,c_0_1857]),
[final] ).
cnf(c_0_2153,negated_conjecture,
( ~ ssRr(X1,skf3(skf3(X2)))
| ~ ssPv1(X2)
| ssPv1(X1) ),
inference(csr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1865,c_0_1946]),c_0_1791]),c_0_1884]),
[final] ).
cnf(c_0_2154,negated_conjecture,
( ~ ssRr(X1,skf3(X2))
| ~ ssPv1(skf2(X2))
| ssPv1(X1) ),
inference(csr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1865,c_0_1911]),c_0_1791]),c_0_1884]),
[final] ).
cnf(c_0_2155,negated_conjecture,
( ~ ssPv3(skf2(skf3(X1)))
| ssPv3(X1) ),
inference(spm,[status(thm)],[c_0_2059,c_0_53]),
[final] ).
cnf(c_0_2156,negated_conjecture,
( ~ ssPv3(X1)
| ssPv3(skf3(skf3(X1))) ),
inference(spm,[status(thm)],[c_0_1905,c_0_77]),
[final] ).
cnf(c_0_2157,negated_conjecture,
( ~ ssPv1(skf3(skf3(skf3(X1))))
| ssPv1(X1) ),
inference(spm,[status(thm)],[c_0_2060,c_0_77]),
[final] ).
cnf(c_0_2158,negated_conjecture,
( ~ ssRr(X2,skf3(skf2(X1)))
| ~ ssPv1(X2)
| ssPv1(skf3(skf3(skf2(X1)))) ),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1691,c_0_77]),c_0_1690]),c_0_1791]),
[final] ).
cnf(c_0_2159,negated_conjecture,
( ~ ssPv3(skf3(skf3(skf3(X1))))
| ssPv1(X1) ),
inference(spm,[status(thm)],[c_0_2061,c_0_1981]),
[final] ).
cnf(c_0_2160,negated_conjecture,
( ~ ssPv3(skf3(skf2(skf3(X1))))
| ssPv1(X1) ),
inference(spm,[status(thm)],[c_0_1846,c_0_1793]),
[final] ).
cnf(c_0_2161,negated_conjecture,
( ~ ssPv3(skf2(skf3(X1)))
| ssPv1(X1) ),
inference(spm,[status(thm)],[c_0_1846,c_0_1813]),
[final] ).
cnf(c_0_2162,negated_conjecture,
( ~ ssPv3(skf3(skf3(skf2(X1))))
| ssPv1(X1) ),
inference(spm,[status(thm)],[c_0_2062,c_0_53]),
[final] ).
cnf(c_0_2163,negated_conjecture,
( ~ ssRr(skf2(skf3(skf3(skf3(X1)))),X2)
| ~ ssPv1(X1)
| ~ ssPv3(X2)
| ssPv3(skf3(skf3(X1)))
| ssPv3(skf3(skf3(skf3(X1)))) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_2063,c_0_53]),c_0_2064]),
[final] ).
cnf(c_0_2164,negated_conjecture,
( ~ ssPv3(X1)
| ssPv1(skf3(skf3(X1))) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_1839,c_0_2065]),c_0_1793]),
[final] ).
cnf(c_0_2165,negated_conjecture,
( ~ ssRr(X1,skf2(X2))
| ~ ssPv1(X2)
| ssPv1(X1) ),
inference(spm,[status(thm)],[c_0_1865,c_0_1903]),
[final] ).
cnf(c_0_2166,negated_conjecture,
( ~ ssRr(X1,X2)
| ~ ssPv1(skf3(X2))
| ssPv1(X1) ),
inference(spm,[status(thm)],[c_0_1865,c_0_1838]),
[final] ).
cnf(c_0_2167,negated_conjecture,
( ~ ssRr(skf2(skf3(skf3(X1))),X2)
| ~ ssPv1(skf2(X1))
| ~ ssPv3(X2)
| ssPv3(skf3(X1))
| ssPv3(skf3(skf3(X1)))
| ssPv2(skf3(skf3(X1))) ),
inference(spm,[status(thm)],[c_0_2066,c_0_53]),
[final] ).
cnf(c_0_2168,negated_conjecture,
( ~ ssRr(X2,skf2(X1))
| ~ ssPv3(X2)
| ssPv1(X1) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1736,c_0_53]),c_0_1791]),
[final] ).
cnf(c_0_2169,negated_conjecture,
( ~ ssPv3(skf3(skf3(skf2(skf3(X1)))))
| ssPv1(X1)
| ssPv3(skf3(X1)) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1370,c_0_1981]),c_0_1791]),
[final] ).
cnf(c_0_2170,negated_conjecture,
( ~ ssRr(X1,X2)
| ~ ssPv3(skf3(skf3(skf2(X2))))
| ssPv1(X1) ),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_696,c_0_1793]),c_0_1690]),c_0_1791]),
[final] ).
cnf(c_0_2171,negated_conjecture,
( ~ ssRr(X1,X2)
| ~ ssPv3(skf3(skf2(X2)))
| ssPv1(X1) ),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_696,c_0_1813]),c_0_1690]),c_0_1791]),
[final] ).
cnf(c_0_2172,negated_conjecture,
( ~ ssPv3(skf3(skf2(X1)))
| ssPv1(X1) ),
inference(spm,[status(thm)],[c_0_1812,c_0_1793]),
[final] ).
cnf(c_0_2173,negated_conjecture,
( ~ ssRr(X3,X4)
| ~ ssRr(X4,skf3(skf3(X1)))
| ~ ssRr(skf2(skf3(skf3(X1))),X2)
| ~ ssPv3(X3)
| ~ ssPv3(skf3(skf3(X1)))
| ssPv3(X2)
| ssPv2(X1) ),
inference(spm,[status(thm)],[c_0_1956,c_0_53]),
[final] ).
cnf(c_0_2174,negated_conjecture,
( ~ ssRr(X4,X3)
| ~ ssRr(skf3(skf3(X1)),X4)
| ~ ssRr(skf2(skf3(skf3(X1))),X2)
| ~ ssPv3(X3)
| ssPv3(X2)
| ssPv4(skf3(skf3(X1)))
| ssPv2(X1) ),
inference(spm,[status(thm)],[c_0_1929,c_0_53]),
[final] ).
cnf(c_0_2175,negated_conjecture,
( ~ ssRr(X3,X4)
| ~ ssRr(X4,skf3(skf3(X1)))
| ~ ssRr(X2,skf3(skf3(skf3(X1))))
| ~ ssPv3(X3)
| ssPv1(X2)
| ssPv4(skf3(skf3(X1)))
| ssPv2(X1) ),
inference(spm,[status(thm)],[c_0_2067,c_0_77]),
[final] ).
cnf(c_0_2176,negated_conjecture,
( ~ ssRr(X4,X5)
| ~ ssRr(X5,X3)
| ~ ssRr(X3,X1)
| ~ ssRr(X3,skf3(X2))
| ~ ssPv3(X4)
| ~ ssPv3(X3)
| ssPv3(X2)
| ssPv2(skf2(X1)) ),
inference(spm,[status(thm)],[c_0_1831,c_0_77]),
[final] ).
cnf(c_0_2177,negated_conjecture,
( ~ ssRr(X4,X3)
| ~ ssRr(X1,X4)
| ~ ssRr(X1,skf3(skf3(X2)))
| ~ ssPv1(X2)
| ~ ssPv3(X3)
| ssPv3(X1)
| ssPv3(skf3(skf3(X2)))
| ssPv4(skf3(X2))
| ssPv2(X1) ),
inference(spm,[status(thm)],[c_0_712,c_0_1833]),
[final] ).
cnf(c_0_2178,negated_conjecture,
( ~ ssRr(X4,X3)
| ~ ssRr(X1,X4)
| ~ ssRr(X1,skf3(X2))
| ~ ssPv1(skf2(X2))
| ~ ssPv3(X3)
| ssPv3(X1)
| ssPv3(skf3(X2))
| ssPv4(X2)
| ssPv2(X1) ),
inference(spm,[status(thm)],[c_0_712,c_0_2068]),
[final] ).
cnf(c_0_2179,negated_conjecture,
( ~ ssRr(X4,X5)
| ~ ssRr(X1,X2)
| ~ ssRr(X5,skf2(X2))
| ~ ssRr(skf2(X2),X3)
| ~ ssPv3(X4)
| ssPv3(skf2(X3))
| ssPv3(skf2(X2))
| ssPv2(X1) ),
inference(spm,[status(thm)],[c_0_1817,c_0_53]),
[final] ).
cnf(c_0_2180,negated_conjecture,
( ~ ssRr(X2,skf3(skf3(X1)))
| ~ ssPv3(X2)
| ssPv3(skf3(skf3(X1)))
| ssPv3(skf3(skf3(skf3(X1))))
| ssPv2(X1) ),
inference(spm,[status(thm)],[c_0_2069,c_0_77]),
[final] ).
cnf(c_0_2181,negated_conjecture,
( ~ ssRr(X2,skf2(X1))
| ~ ssPv1(X2)
| ssPv1(X1)
| ssPv4(skf2(X1))
| ssPv2(skf2(skf2(X1))) ),
inference(spm,[status(thm)],[c_0_1325,c_0_53]),
[final] ).
cnf(c_0_2182,negated_conjecture,
( ~ ssRr(X2,skf3(X1))
| ~ ssPv1(X2)
| ssPv1(skf3(skf3(X1)))
| ssPv4(skf3(X1))
| ssPv2(X1) ),
inference(spm,[status(thm)],[c_0_1429,c_0_77]),
[final] ).
cnf(c_0_2183,negated_conjecture,
( ~ ssPv1(skf2(skf2(skf3(X1))))
| ssPv1(X1)
| ssPv3(skf3(X1))
| ssPv4(skf2(skf3(X1))) ),
inference(spm,[status(thm)],[c_0_2070,c_0_53]),
[final] ).
cnf(c_0_2184,negated_conjecture,
( ~ ssRr(X4,X6)
| ~ ssRr(X6,X2)
| ~ ssRr(X1,X5)
| ~ ssRr(X5,X2)
| ~ ssRr(X2,skf3(X3))
| ~ ssPv3(X4)
| ssPv3(X3)
| ssPv3(X2)
| ssPv2(X1) ),
inference(spm,[status(thm)],[c_0_1808,c_0_77]),
[final] ).
cnf(c_0_2185,negated_conjecture,
( ~ ssRr(X2,skf3(X1))
| ~ ssPv3(X2)
| ssPv3(skf3(X1))
| ssPv3(skf3(skf3(X1)))
| ssPv2(skf2(X1)) ),
inference(spm,[status(thm)],[c_0_1257,c_0_77]),
[final] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN798-1 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.05 % Command : run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.14/15.42 % Computer : n002.cluster.edu
% 0.14/15.42 % Model : x86_64 x86_64
% 0.14/15.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/15.42 % Memory : 8046.5625MB
% 0.14/15.42 % OS : Linux 6.8.0-71-generic
% 0.14/15.42 % CPULimit : 300
% 0.14/15.42 % WCLimit : 300
% 0.14/15.42 % DateTime : Mon Sep 21 11:19:47 UTC 2026
% 0.14/15.42 % CPUTime :
% 0.14/15.42 Running run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.14/15.48 Running first-order theorem proving
% 0.14/15.48 Running: /export/starexec/sandbox2/solver/bin/eprover --delete-bad-limit=2000000000 --definitional-cnf=24 -s --print-statistics -R --print-version --proof-object --auto-schedule=8 --cpu-limit=300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 52.85/23.21 % Version: 3.5.1
% 52.85/23.21 % Preprocessing class: FSLSSMSSSSSNFFN.
% 52.85/23.21 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 52.85/23.21 % Starting G-E--_207_C18_F1_SE_CS_SP_PI_PS_S5PRR_S2S with 1500s (5) cores
% 52.85/23.21 % Starting new_bool_3 with 300s (1) cores
% 52.85/23.21 % Starting new_bool_1 with 300s (1) cores
% 52.85/23.21 % Starting sh5l with 300s (1) cores
% 52.85/23.21 % G-E--_207_C18_F1_SE_CS_SP_PI_PS_S5PRR_S2S with pid 3164606 completed with status 1
% 52.85/23.21 % Result found by G-E--_207_C18_F1_SE_CS_SP_PI_PS_S5PRR_S2S
% 52.85/23.21 % Preprocessing class: FSLSSMSSSSSNFFN.
% 52.85/23.21 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 52.85/23.21 % Starting G-E--_207_C18_F1_SE_CS_SP_PI_PS_S5PRR_S2S with 1500s (5) cores
% 52.85/23.21 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 52.85/23.21 % No SInE strategy applied
% 52.85/23.21 % Search class: FGHNS-FSMF11-SFFFFFNN
% 52.85/23.21 % Scheduled 7 strats onto 5 cores with 1500 seconds (1500 total)
% 52.85/23.21 % Starting SubtermCWHack with 136s (1) cores
% 52.85/23.21 % Starting G-E--_207_C18_F1_SE_CS_SP_PI_PS_S5PRR_S2S with 151s (1) cores
% 52.85/23.21 % Starting G-E--_107_C09_12_F1_PI_AE_Q4_CS_SP_PS_S063N with 136s (1) cores
% 52.85/23.21 % Starting new_bool_3 with 136s (1) cores
% 52.85/23.21 % Starting new_bool_1 with 136s (1) cores
% 52.85/23.21 % G-E--_107_C09_12_F1_PI_AE_Q4_CS_SP_PS_S063N with pid 3164612 completed with status 1
% 52.85/23.21 % Result found by G-E--_107_C09_12_F1_PI_AE_Q4_CS_SP_PS_S063N
% 52.85/23.21 % Preprocessing class: FSLSSMSSSSSNFFN.
% 52.85/23.21 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 52.85/23.21 % Starting G-E--_207_C18_F1_SE_CS_SP_PI_PS_S5PRR_S2S with 1500s (5) cores
% 52.85/23.21 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 52.85/23.21 % No SInE strategy applied
% 52.85/23.21 % Search class: FGHNS-FSMF11-SFFFFFNN
% 52.85/23.21 % Scheduled 7 strats onto 5 cores with 1500 seconds (1500 total)
% 52.85/23.21 % Starting SubtermCWHack with 136s (1) cores
% 52.85/23.21 % Starting G-E--_207_C18_F1_SE_CS_SP_PI_PS_S5PRR_S2S with 151s (1) cores
% 52.85/23.21 % Starting G-E--_107_C09_12_F1_PI_AE_Q4_CS_SP_PS_S063N with 136s (1) cores
% 52.85/23.21 % Preprocessing time : 0.004 s
% 52.85/23.21 % Presaturation interreduction done
% 52.85/23.21
% 52.85/23.21 % No proof found!
% 52.85/23.21 % SZS status Satisfiable
% 52.85/23.21 % SZS output start Saturation
% See solution above
% 52.85/23.22 % Parsed axioms : 52
% 52.85/23.22 % Removed by relevancy pruning/SinE : 0
% 52.85/23.22 % Initial clauses : 52
% 52.85/23.22 % Removed in clause preprocessing : 0
% 52.85/23.22 % Initial clauses in saturation : 52
% 52.85/23.22 % Processed clauses : 17514
% 52.85/23.22 % ...of these trivial : 0
% 52.85/23.22 % ...subsumed : 11201
% 52.85/23.22 % ...remaining for further processing : 6313
% 52.85/23.22 % Other redundant clauses eliminated : 0
% 52.85/23.22 % Clauses deleted for lack of memory : 0
% 52.85/23.22 % Backward-subsumed : 5892
% 52.85/23.22 % Backward-rewritten : 0
% 52.85/23.22 % Generated clauses : 169551
% 52.85/23.22 % ...of the previous two non-redundant : 108076
% 52.85/23.22 % ...aggressively subsumed : 0
% 52.85/23.22 % Contextual simplify-reflections : 2329
% 52.85/23.22 % Paramodulations : 169551
% 52.85/23.22 % Factorizations : 0
% 52.85/23.22 % NegExts : 0
% 52.85/23.22 % Equation resolutions : 0
% 52.85/23.22 % Disequality decompositions : 0
% 52.85/23.22 % Total rewrite steps : 0
% 52.85/23.22 % ...of those cached : 0
% 52.85/23.22 % Propositional unsat checks : 0
% 52.85/23.22 % Propositional check models : 0
% 52.85/23.22 % Propositional check unsatisfiable : 0
% 52.85/23.22 % Propositional clauses : 0
% 52.85/23.22 % Propositional clauses after purity: 0
% 52.85/23.22 % Propositional unsat core size : 0
% 52.85/23.22 % Propositional preprocessing time : 0.000
% 52.85/23.22 % Propositional encoding time : 0.000
% 52.85/23.22 % Propositional solver time : 0.000
% 52.85/23.22 % Success case prop preproc time : 0.000
% 52.85/23.22 % Success case prop encoding time : 0.000
% 52.85/23.22 % Success case prop solver time : 0.000
% 52.85/23.22 % Current number of processed clauses : 369
% 52.85/23.22 % Positive orientable unit clauses : 2
% 52.85/23.22 % Positive unorientable unit clauses: 0
% 52.85/23.22 % Negative unit clauses : 2
% 52.85/23.22 % Non-unit-clauses : 365
% 52.85/23.22 % Current number of unprocessed clauses: 0
% 52.85/23.22 % ...number of literals in the above : 0
% 52.85/23.22 % Current number of archived formulas : 0
% 52.85/23.22 % Current number of archived clauses : 5944
% 52.85/23.22 % Clause-clause subsumption calls (NU) : 573709
% 52.85/23.22 % Rec. Clause-clause subsumption calls : 121652
% 52.85/23.22 % Non-unit clause-clause subsumptions : 18718
% 52.85/23.22 % Unit Clause-clause subsumption calls : 1226
% 52.85/23.22 % Rewrite failures with RHS unbound : 0
% 52.85/23.22 % BW rewrite match attempts : 0
% 52.85/23.22 % BW rewrite match successes : 0
% 52.85/23.22 % Condensation attempts : 0
% 52.85/23.22 % Condensation successes : 0
% 52.85/23.22 % Termbank termtop insertions : 4251151
% 52.85/23.22 % Search garbage collected termcells : 365
% 52.85/23.22
% 52.85/23.22 % -------------------------------------------------
% 52.85/23.22 % User time : 7.485 s
% 52.85/23.22 % System time : 0.117 s
% 52.85/23.22 % Total time : 7.602 s
% 52.85/23.22 % Maximum resident set size: 4156 pages
% 52.85/23.22
% 52.85/23.22 % -------------------------------------------------
% 52.85/23.22 % User time : 36.875 s
% 52.85/23.22 % System time : 0.562 s
% 52.85/23.22 % Total time : 37.438 s
% 52.85/23.22 % Maximum resident set size: 5376 pages
% 52.85/23.22 % E exiting
%------------------------------------------------------------------------------