%------------------------------------------------------------------------------
% File : E-SAT---3.5.1
% Problem : SYN798-1 : TPTP v9.3.1. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n006.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:36:28 PM UTC 2026
% Result : Satisfiable 24.58s 14.13s
% Output : Saturation 24.58s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named c_0_467ERROR: 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_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_494,negated_conjecture,
( ~ ssPv3(X6)
| ~ ssRr(X3,X6)
| ~ ssRr(X3,X4)
| ~ ssRr(X4,X5)
| ~ ssRr(X3,X1)
| ~ ssPv3(X2)
| ~ ssRr(X1,X2)
| ssPv4(X3)
| ssPv4(X5) ),
c_0_484,
[final] ).
cnf(c_0_506,negated_conjecture,
( ~ ssRr(X5,X4)
| ~ ssRr(X2,X5)
| ~ ssRr(X2,X1)
| ~ ssRr(X2,X3)
| ~ ssPv3(X4)
| ~ ssPv3(X3)
| ssPv4(X2)
| ssPv4(skf2(X1)) ),
inference(spm,[status(thm)],[c_0_494,c_0_53]),
[final] ).
cnf(c_0_519,negated_conjecture,
( ~ ssRr(X4,X3)
| ~ ssRr(X2,X4)
| ~ ssRr(X2,X1)
| ~ ssPv3(X3)
| ~ ssPv3(skf2(X2))
| ssPv4(X2)
| ssPv4(skf2(X1)) ),
inference(spm,[status(thm)],[c_0_506,c_0_53]),
[final] ).
cnf(c_0_534,negated_conjecture,
( ~ ssRr(X3,X2)
| ~ ssRr(X1,X3)
| ~ ssPv3(X2)
| ~ ssPv3(skf2(X1))
| ssPv4(X1)
| ssPv4(skf2(skf2(X1))) ),
inference(spm,[status(thm)],[c_0_519,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_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_941,negated_conjecture,
( ~ ssRr(X4,X3)
| ~ ssRr(skf3(X1),X4)
| ~ ssRr(skf3(X1),X2)
| ~ ssPv3(X3)
| ~ ssPv3(X1)
| ssPv4(skf2(X2))
| ssPv4(skf3(X1)) ),
inference(spm,[status(thm)],[c_0_506,c_0_77]),
[final] ).
cnf(c_0_946,negated_conjecture,
( ~ ssRr(X3,X2)
| ~ ssRr(skf3(X1),X3)
| ~ ssPv3(X2)
| ~ ssPv3(X1)
| ssPv4(skf3(X1))
| ssPv4(skf2(X1)) ),
inference(spm,[status(thm)],[c_0_941,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_1347,negated_conjecture,
( ~ ssRr(X2,X3)
| ~ ssRr(X3,X1)
| ~ ssPv1(X2)
| ~ ssPv1(skf3(X1))
| ssPv1(skf2(skf2(X1)))
| ssPv3(X1) ),
inference(spm,[status(thm)],[c_0_1337,c_0_53]),
[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_1359,negated_conjecture,
( ~ ssRr(X2,skf3(X1))
| ~ ssPv1(X2)
| ~ ssPv1(skf3(X1))
| ssPv1(skf2(skf2(X1)))
| ssPv3(X1) ),
inference(spm,[status(thm)],[c_0_1347,c_0_77]),
[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_1371,negated_conjecture,
( ~ ssPv1(skf3(X1))
| ~ ssPv1(skf3(skf3(X1)))
| ssPv1(skf2(skf2(X1)))
| ssPv3(X1) ),
inference(spm,[status(thm)],[c_0_1359,c_0_77]),
[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_1684,negated_conjecture,
( ~ ssRr(X1,X2)
| ~ ssPv3(X2)
| ~ ssPv3(skf2(skf3(X1)))
| ssPv4(skf3(X1))
| ssPv4(skf2(skf2(skf3(X1)))) ),
inference(spm,[status(thm)],[c_0_534,c_0_77]),
[final] ).
cnf(c_0_1689,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_1694,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_1689,c_0_77]),
[final] ).
cnf(c_0_1695,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_1698,negated_conjecture,
( ~ ssRr(X2,X1)
| ~ ssPv1(X2)
| ssPv1(skf3(skf3(skf2(X1))))
| ssPv4(X1) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1694,c_0_53]),c_0_1691]),
[final] ).
cnf(c_0_1699,negated_conjecture,
( ~ ssRr(X2,X3)
| ~ ssRr(X3,skf2(X1))
| ~ ssPv1(X2)
| ~ ssPv1(X1)
| ssPv1(skf2(skf2(skf2(X1))))
| ssPv3(skf2(X1)) ),
inference(spm,[status(thm)],[c_0_1695,c_0_53]),
[final] ).
cnf(c_0_1703,negated_conjecture,
( ~ ssPv1(skf3(X1))
| ssPv1(skf3(skf3(skf2(X1))))
| ssPv4(X1) ),
inference(spm,[status(thm)],[c_0_1698,c_0_77]),
[final] ).
cnf(c_0_1705,negated_conjecture,
( ~ ssRr(X2,X1)
| ~ ssPv1(X2)
| ~ ssPv1(X1)
| ssPv1(skf2(skf2(skf2(X1))))
| ssPv3(skf2(X1)) ),
inference(spm,[status(thm)],[c_0_1699,c_0_53]),
[final] ).
cnf(c_0_1706,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_1700,
[final] ).
cnf(c_0_1710,negated_conjecture,
( ~ ssPv1(X1)
| ~ ssPv1(skf3(X1))
| ssPv1(skf2(skf2(skf2(X1))))
| ssPv3(skf2(X1)) ),
inference(spm,[status(thm)],[c_0_1705,c_0_77]),
[final] ).
cnf(c_0_1711,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_1706,c_0_53]),
[final] ).
cnf(c_0_1719,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_1715,c_0_53]),c_0_1691]),
[final] ).
cnf(c_0_1725,negated_conjecture,
( ~ ssRr(X3,X1)
| ~ ssRr(X2,X1)
| ~ ssPv3(X3)
| ssPv1(X2)
| ssPv4(skf2(X1)) ),
inference(spm,[status(thm)],[c_0_1719,c_0_53]),
[final] ).
cnf(c_0_1730,negated_conjecture,
( ~ ssRr(X2,X1)
| ~ ssPv3(X2)
| ssPv1(skf3(X1))
| ssPv4(skf2(X1)) ),
inference(spm,[status(thm)],[c_0_1725,c_0_77]),
[final] ).
cnf(c_0_1752,negated_conjecture,
~ ssPv4(X1),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_1748,c_0_1222]),c_0_1597]),
[final] ).
cnf(c_0_1757,negated_conjecture,
( ~ ssPv3(X1)
| ssPv1(X1) ),
inference(spm,[status(thm)],[c_0_1752,c_0_1743]),
[final] ).
cnf(c_0_1775,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_1771,
[final] ).
cnf(c_0_1778,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_1775,c_0_53]),
[final] ).
cnf(c_0_1779,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_1785,negated_conjecture,
( ~ ssRr(X1,X2)
| ~ ssPv1(X2)
| ssPv1(skf2(skf3(X1)))
| ssPv3(skf3(X1))
| ssPv4(X1) ),
inference(spm,[status(thm)],[c_0_1779,c_0_77]),
[final] ).
cnf(c_0_1786,negated_conjecture,
( ~ ssPv1(skf3(skf2(X1)))
| ssPv1(X1) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1752,c_0_1389]),c_0_1691]),
[final] ).
cnf(c_0_1787,negated_conjecture,
( ~ ssPv3(X1)
| ssPv1(skf3(X1)) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1780,c_0_1713]),c_0_1752]),
[final] ).
cnf(c_0_1788,negated_conjecture,
( ~ ssPv1(skf3(X1))
| ssPv1(X1) ),
inference(csr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1781,c_0_847]),c_0_1752]),c_0_1757]),
[final] ).
cnf(c_0_1789,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_1782,
[final] ).
cnf(c_0_1790,negated_conjecture,
~ ssPv2(X1),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_1783,c_0_1769]),c_0_1769]),
[final] ).
cnf(c_0_1791,negated_conjecture,
( ~ ssRr(X4,X2)
| ~ ssRr(X3,X4)
| ~ ssRr(X3,X1)
| ~ ssPv3(X2)
| ssPv3(skf2(X1)) ),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1784,c_0_53]),c_0_1691]),c_0_1752]),
[final] ).
cnf(c_0_1792,negated_conjecture,
( ~ ssPv1(X1)
| ssPv1(skf2(skf3(skf3(X1))))
| ssPv3(skf3(skf3(X1)))
| ssPv4(skf3(X1)) ),
inference(spm,[status(thm)],[c_0_1785,c_0_77]),
[final] ).
cnf(c_0_1793,negated_conjecture,
( ~ ssPv3(skf2(X1))
| ssPv1(X1) ),
inference(spm,[status(thm)],[c_0_1786,c_0_1787]),
[final] ).
cnf(c_0_1794,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_1711,c_0_77]),
[final] ).
cnf(c_0_1795,negated_conjecture,
( ~ ssPv3(skf3(X1))
| ssPv1(X1) ),
inference(spm,[status(thm)],[c_0_1788,c_0_1757]),
[final] ).
cnf(c_0_1796,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_1789,c_0_53]),
[final] ).
cnf(c_0_1805,negated_conjecture,
( ~ ssPv1(X1)
| ssPv1(skf3(X1)) ),
inference(spm,[status(thm)],[c_0_1795,c_0_1762]),
[final] ).
cnf(c_0_1806,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_1807,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_1808,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_1796,c_0_77]),
[final] ).
cnf(c_0_1809,negated_conjecture,
( ~ ssRr(X3,X2)
| ~ ssRr(X1,X3)
| ~ ssPv3(X2)
| ssPv3(X1) ),
inference(spm,[status(thm)],[c_0_1797,c_0_53]),
[final] ).
cnf(c_0_1810,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_1798,
[final] ).
cnf(c_0_1812,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_1800,
[final] ).
cnf(c_0_1813,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_1775,c_0_77]),
[final] ).
cnf(c_0_1814,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_1778,c_0_77]),
[final] ).
cnf(c_0_1815,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_1795,c_0_1801]),c_0_1752]),c_0_1752]),c_0_1757]),
[final] ).
cnf(c_0_1816,negated_conjecture,
( ~ ssPv3(X1)
| ssPv1(skf3(skf2(X1))) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1730,c_0_53]),c_0_1752]),
[final] ).
cnf(c_0_1817,negated_conjecture,
( ~ ssPv1(skf3(X1))
| ssPv1(skf2(X1)) ),
inference(spm,[status(thm)],[c_0_1788,c_0_1802]),
[final] ).
cnf(c_0_1818,negated_conjecture,
( ~ ssRr(X2,X3)
| ~ ssRr(X3,X1)
| ~ ssPv3(X2)
| ssPv1(skf3(skf3(X1))) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1803,c_0_53]),c_0_1752]),
[final] ).
cnf(c_0_1820,negated_conjecture,
( ~ ssPv1(skf2(X1))
| ssPv1(X1) ),
inference(spm,[status(thm)],[c_0_1786,c_0_1805]),
[final] ).
cnf(c_0_1821,negated_conjecture,
( ~ ssPv1(skf2(X1))
| ssPv1(skf2(skf3(X1)))
| ssPv3(skf3(X1))
| ssPv4(skf2(skf3(X1))) ),
inference(spm,[status(thm)],[c_0_1806,c_0_53]),
[final] ).
cnf(c_0_1823,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_1808,c_0_77]),
[final] ).
cnf(c_0_1824,negated_conjecture,
( ~ ssRr(skf2(X1),X2)
| ~ ssPv3(X2)
| ssPv3(X1) ),
inference(spm,[status(thm)],[c_0_1809,c_0_53]),
[final] ).
cnf(c_0_1825,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_1810,c_0_77]),
[final] ).
cnf(c_0_1827,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_1810,c_0_53]),
[final] ).
cnf(c_0_1828,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_1812,c_0_77]),
[final] ).
cnf(c_0_1829,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_1813,c_0_77]),
[final] ).
cnf(c_0_1831,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_1815]),c_0_1691]),c_0_1752]),
[final] ).
cnf(c_0_1832,negated_conjecture,
( ~ ssPv3(X1)
| ssPv1(skf2(X1)) ),
inference(spm,[status(thm)],[c_0_1788,c_0_1816]),
[final] ).
cnf(c_0_1833,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_1817]),c_0_1752]),c_0_1795]),
[final] ).
cnf(c_0_1834,negated_conjecture,
( ~ ssPv1(skf3(X1))
| ssPv1(skf3(skf2(X1))) ),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1788,c_0_1466]),c_0_1691]),c_0_1752]),
[final] ).
cnf(c_0_1835,negated_conjecture,
( ~ ssRr(X2,X1)
| ~ ssPv3(X2)
| ssPv1(skf3(skf3(skf2(X1)))) ),
inference(spm,[status(thm)],[c_0_1818,c_0_53]),
[final] ).
cnf(c_0_1837,negated_conjecture,
( ~ ssPv1(skf2(X1))
| ssPv1(skf3(X1)) ),
inference(csr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1820,c_0_1821]),c_0_1752]),c_0_1757]),
[final] ).
cnf(c_0_1839,negated_conjecture,
( ~ ssRr(X3,X2)
| ~ ssRr(X1,X3)
| ~ ssPv3(X2)
| ssPv3(skf2(skf2(X1))) ),
inference(spm,[status(thm)],[c_0_1791,c_0_53]),
[final] ).
cnf(c_0_1840,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_1841,negated_conjecture,
( ~ ssPv1(X1)
| ssPv1(skf3(skf2(X1))) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1752,c_0_1822]),c_0_1691]),
[final] ).
cnf(c_0_1842,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_1843,negated_conjecture,
( ~ ssRr(X2,X3)
| ~ ssRr(X3,X1)
| ~ ssPv3(X2)
| ssPv3(X1)
| ssPv3(skf2(skf2(X1))) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1823,c_0_53]),c_0_1790]),
[final] ).
cnf(c_0_1844,negated_conjecture,
( ~ ssPv3(skf2(skf2(X1)))
| ssPv3(X1) ),
inference(spm,[status(thm)],[c_0_1824,c_0_53]),
[final] ).
cnf(c_0_1845,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_1825,c_0_77]),
[final] ).
cnf(c_0_1847,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_1827,c_0_77]),
[final] ).
cnf(c_0_1848,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_1849,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_1828,c_0_77]),
[final] ).
cnf(c_0_1850,negated_conjecture,
( ~ ssRr(X4,X3)
| ~ ssRr(skf3(X1),X2)
| ~ ssRr(skf3(skf3(X1)),X4)
| ~ ssPv3(X3)
| ssPv3(X2)
| ssPv2(X1) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1829,c_0_77]),c_0_1752]),
[final] ).
cnf(c_0_1851,negated_conjecture,
( ~ ssRr(X3,X2)
| ~ ssRr(skf3(skf3(X1)),X3)
| ~ ssPv3(X2)
| ssPv3(X1) ),
inference(spm,[status(thm)],[c_0_1830,c_0_53]),
[final] ).
cnf(c_0_1852,negated_conjecture,
( ~ ssRr(X3,X2)
| ~ ssRr(skf3(X1),X3)
| ~ ssPv3(X2)
| ssPv3(skf2(X1)) ),
inference(spm,[status(thm)],[c_0_1791,c_0_77]),
[final] ).
cnf(c_0_1853,negated_conjecture,
( ~ ssRr(X3,X2)
| ~ ssRr(skf3(X1),X3)
| ~ ssPv3(X2)
| ~ ssPv3(X1)
| ssPv4(skf3(X1))
| ssPv4(skf2(skf2(skf3(X1)))) ),
inference(spm,[status(thm)],[c_0_941,c_0_53]),
[final] ).
cnf(c_0_1855,negated_conjecture,
( ~ ssRr(X1,X2)
| ~ ssPv3(X2)
| ssPv1(X1) ),
inference(spm,[status(thm)],[c_0_1831,c_0_1832]),
[final] ).
cnf(c_0_1856,negated_conjecture,
( ~ ssPv1(X1)
| ssPv1(skf2(skf3(skf3(X1))))
| ssPv3(skf3(skf3(X1)))
| ssPv4(skf2(skf3(skf3(X1)))) ),
inference(spm,[status(thm)],[c_0_1806,c_0_77]),
[final] ).
cnf(c_0_1857,negated_conjecture,
( ~ ssPv1(skf3(skf3(X1)))
| ssPv1(X1) ),
inference(spm,[status(thm)],[c_0_1833,c_0_1834]),
[final] ).
cnf(c_0_1858,negated_conjecture,
( ~ ssPv3(skf3(X1))
| ssPv1(skf3(skf3(skf2(X1)))) ),
inference(spm,[status(thm)],[c_0_1835,c_0_77]),
[final] ).
cnf(c_0_1861,negated_conjecture,
( ~ ssPv3(X1)
| ~ ssPv3(skf3(X1)) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1752,c_0_1324]),c_0_1752]),
[final] ).
cnf(c_0_1862,negated_conjecture,
( ~ ssPv1(skf2(X1))
| ssPv1(skf3(skf3(X1))) ),
inference(csr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1837,c_0_1821]),c_0_1752]),c_0_1787]),
[final] ).
cnf(c_0_1863,negated_conjecture,
( ~ ssPv3(skf2(X1))
| ~ ssPv3(skf2(skf3(X1))) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1752,c_0_1838]),c_0_1752]),
[final] ).
cnf(c_0_1864,negated_conjecture,
( ~ ssRr(X1,X2)
| ~ ssPv3(X2)
| ssPv3(skf2(skf2(skf3(X1)))) ),
inference(spm,[status(thm)],[c_0_1839,c_0_77]),
[final] ).
cnf(c_0_1865,negated_conjecture,
( ~ ssRr(X5,X4)
| ~ ssRr(X1,X5)
| ~ ssRr(X1,X3)
| ~ ssRr(X1,skf3(X2))
| ~ ssPv3(X4)
| ~ ssPv3(X3)
| ssPv4(X2)
| ssPv4(X1) ),
inference(spm,[status(thm)],[c_0_494,c_0_77]),
[final] ).
cnf(c_0_1866,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_1840,c_0_77]),
[final] ).
cnf(c_0_1867,negated_conjecture,
( ~ ssPv1(X1)
| ssPv1(skf2(X1)) ),
inference(spm,[status(thm)],[c_0_1788,c_0_1841]),
[final] ).
cnf(c_0_1868,negated_conjecture,
( ~ ssPv1(skf3(skf3(X1)))
| ssPv1(skf2(X1))
| ssPv3(skf3(X1)) ),
inference(spm,[status(thm)],[c_0_1557,c_0_1767]),
[final] ).
cnf(c_0_1870,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_1827,c_0_53]),
[final] ).
cnf(c_0_1871,negated_conjecture,
( ~ ssRr(X2,X1)
| ~ ssPv3(X2)
| ssPv3(skf2(X1)) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_1843,c_0_53]),c_0_1844]),
[final] ).
cnf(c_0_1872,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_1845,c_0_77]),c_0_1846]),
[final] ).
cnf(c_0_1873,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_1847,c_0_77]),
[final] ).
cnf(c_0_1874,negated_conjecture,
( ~ ssPv3(X1)
| ssPv1(skf3(skf3(skf2(skf2(X1))))) ),
inference(spm,[status(thm)],[c_0_1835,c_0_53]),
[final] ).
cnf(c_0_1875,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_1848,c_0_77]),c_0_1691]),c_0_1752]),
[final] ).
cnf(c_0_1877,negated_conjecture,
( ~ ssRr(X2,skf3(X1))
| ~ ssPv3(X2)
| ssPv3(X1) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_1843,c_0_77]),c_0_1844]),
[final] ).
cnf(c_0_1878,negated_conjecture,
( ~ ssRr(skf3(X3),X1)
| ~ ssRr(skf2(skf3(skf3(X3))),X2)
| ~ ssPv3(X2)
| ssPv3(X1) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1850,c_0_53]),c_0_1790]),
[final] ).
cnf(c_0_1879,negated_conjecture,
( ~ ssRr(X3,X2)
| ~ ssRr(skf3(X1),X3)
| ~ ssPv3(X2)
| ~ ssPv3(skf2(skf3(X1)))
| ssPv4(skf2(X1))
| ssPv4(skf3(X1)) ),
inference(spm,[status(thm)],[c_0_519,c_0_77]),
[final] ).
cnf(c_0_1880,negated_conjecture,
( ~ ssRr(skf2(skf3(skf3(X1))),X2)
| ~ ssPv3(X2)
| ssPv3(X1) ),
inference(spm,[status(thm)],[c_0_1851,c_0_53]),
[final] ).
cnf(c_0_1881,negated_conjecture,
( ~ ssRr(skf2(skf3(X1)),X2)
| ~ ssPv3(X2)
| ssPv3(skf2(X1)) ),
inference(spm,[status(thm)],[c_0_1852,c_0_53]),
[final] ).
cnf(c_0_1882,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_1853,c_0_53]),c_0_1752]),c_0_1752]),
[final] ).
cnf(c_0_1883,negated_conjecture,
( ~ ssRr(X1,X2)
| ~ ssPv3(X2)
| ssPv3(skf3(X1)) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_1854,c_0_1815]),c_0_1855]),
[final] ).
cnf(c_0_1884,negated_conjecture,
( ~ ssPv1(X1)
| ssPv1(skf3(skf3(skf3(X1)))) ),
inference(csr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1837,c_0_1856]),c_0_1752]),c_0_1787]),
[final] ).
cnf(c_0_1885,negated_conjecture,
( ~ ssPv3(skf3(X1))
| ssPv1(skf2(X1)) ),
inference(spm,[status(thm)],[c_0_1857,c_0_1858]),
[final] ).
cnf(c_0_1887,negated_conjecture,
( ~ ssPv3(skf3(skf3(X1)))
| ssPv1(X1) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_1860,c_0_1757]),c_0_1861]),
[final] ).
cnf(c_0_1888,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_1862]),c_0_1691]),c_0_1752]),
[final] ).
cnf(c_0_1890,negated_conjecture,
( ~ ssPv3(X1)
| ssPv3(skf2(skf2(skf3(skf3(X1))))) ),
inference(spm,[status(thm)],[c_0_1864,c_0_77]),
[final] ).
cnf(c_0_1891,negated_conjecture,
( ~ ssPv3(skf2(X1))
| ssPv3(skf2(skf2(skf3(X1)))) ),
inference(spm,[status(thm)],[c_0_1864,c_0_53]),
[final] ).
cnf(c_0_1892,negated_conjecture,
( ~ ssRr(X4,X3)
| ~ ssRr(skf3(skf3(X1)),X4)
| ~ ssRr(skf3(skf3(X1)),X2)
| ~ ssPv3(X3)
| ~ ssPv3(X2)
| ssPv4(X1)
| ssPv4(skf3(skf3(X1))) ),
inference(spm,[status(thm)],[c_0_1865,c_0_77]),
[final] ).
cnf(c_0_1893,negated_conjecture,
( ~ ssRr(X1,X2)
| ~ ssPv3(X2)
| ssPv3(skf2(X1)) ),
inference(spm,[status(thm)],[c_0_1852,c_0_77]),
[final] ).
cnf(c_0_1895,negated_conjecture,
( ~ ssRr(X1,X2)
| ~ ssPv1(X2)
| ssPv1(X1) ),
inference(spm,[status(thm)],[c_0_1831,c_0_1867]),
[final] ).
cnf(c_0_1896,negated_conjecture,
( ~ ssPv3(skf3(skf3(X1)))
| ssPv1(skf2(X1)) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_1868,c_0_1757]),c_0_1861]),
[final] ).
cnf(c_0_1897,negated_conjecture,
( ~ ssPv3(X1)
| ~ ssPv3(skf2(skf3(skf3(X1)))) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1752,c_0_1690]),c_0_1752]),
[final] ).
cnf(c_0_1899,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_1706,c_0_77]),
[final] ).
cnf(c_0_1900,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_1901,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_1870,c_0_53]),c_0_1691]),
[final] ).
cnf(c_0_1902,negated_conjecture,
( ~ ssPv3(skf3(X1))
| ssPv3(skf2(X1)) ),
inference(spm,[status(thm)],[c_0_1871,c_0_77]),
[final] ).
cnf(c_0_1903,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_1872,c_0_77]),
[final] ).
cnf(c_0_1904,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_1873,c_0_53]),c_0_1790]),
[final] ).
cnf(c_0_1905,negated_conjecture,
( ~ ssRr(X2,skf3(skf2(X1)))
| ~ ssPv1(X2)
| ~ ssPv1(X1)
| ssPv1(skf2(skf2(skf2(X1))))
| ssPv3(skf2(X1)) ),
inference(spm,[status(thm)],[c_0_1699,c_0_77]),
[final] ).
cnf(c_0_1906,negated_conjecture,
( ~ ssPv3(X1)
| ssPv1(skf2(skf2(X1))) ),
inference(spm,[status(thm)],[c_0_1857,c_0_1874]),
[final] ).
cnf(c_0_1907,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_1873,c_0_77]),c_0_1790]),
[final] ).
cnf(c_0_1908,negated_conjecture,
( ~ ssPv1(X1)
| ssPv1(skf2(skf2(skf2(X1))))
| ssPv3(skf3(skf2(skf2(X1)))) ),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1868,c_0_1842]),c_0_1691]),c_0_1752]),
[final] ).
cnf(c_0_1909,negated_conjecture,
( ~ ssRr(X1,X2)
| ~ ssPv3(skf3(X2))
| ssPv1(X1) ),
inference(spm,[status(thm)],[c_0_1875,c_0_1858]),
[final] ).
cnf(c_0_1910,negated_conjecture,
( ~ ssPv1(skf3(X1))
| ssPv1(skf2(skf2(X1)))
| ssPv3(skf3(skf2(X1))) ),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1868,c_0_1466]),c_0_1691]),c_0_1752]),
[final] ).
cnf(c_0_1911,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_1876,c_0_77]),c_0_1790]),c_0_1877]),
[final] ).
cnf(c_0_1912,negated_conjecture,
( ~ ssRr(skf3(X2),X1)
| ~ ssPv3(skf2(skf2(skf3(skf3(X2)))))
| ssPv3(X1) ),
inference(spm,[status(thm)],[c_0_1878,c_0_53]),
[final] ).
cnf(c_0_1913,negated_conjecture,
( ~ ssRr(X1,X2)
| ~ ssPv3(X2)
| ~ ssPv3(skf2(skf3(X1)))
| ssPv4(skf3(X1))
| ssPv4(skf2(X1)) ),
inference(spm,[status(thm)],[c_0_1879,c_0_77]),
[final] ).
cnf(c_0_1914,negated_conjecture,
( ~ ssPv3(X1)
| ssPv3(skf2(skf2(X1))) ),
inference(spm,[status(thm)],[c_0_1871,c_0_53]),
[final] ).
cnf(c_0_1915,negated_conjecture,
( ~ ssPv3(skf2(skf2(skf3(skf3(X1)))))
| ssPv3(X1) ),
inference(spm,[status(thm)],[c_0_1880,c_0_53]),
[final] ).
cnf(c_0_1916,negated_conjecture,
( ~ ssPv3(skf2(skf2(skf3(X1))))
| ssPv3(skf2(X1)) ),
inference(spm,[status(thm)],[c_0_1881,c_0_53]),
[final] ).
cnf(c_0_1917,negated_conjecture,
( ~ ssPv3(X1)
| ~ ssPv3(skf2(skf2(skf3(X1)))) ),
inference(spm,[status(thm)],[c_0_1882,c_0_53]),
[final] ).
cnf(c_0_1918,negated_conjecture,
( ~ ssPv3(skf2(X1))
| ssPv3(skf3(X1)) ),
inference(spm,[status(thm)],[c_0_1883,c_0_53]),
[final] ).
cnf(c_0_1919,negated_conjecture,
( ~ ssPv1(X1)
| ssPv1(skf2(skf3(X1)))
| ssPv3(skf3(skf3(X1))) ),
inference(spm,[status(thm)],[c_0_1868,c_0_1884]),
[final] ).
cnf(c_0_1920,negated_conjecture,
( ~ ssPv3(X1)
| ssPv1(skf2(skf2(skf2(X1)))) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_1868,c_0_1874]),c_0_1885]),
[final] ).
cnf(c_0_1921,negated_conjecture,
( ~ ssPv3(skf3(X1))
| ssPv1(skf2(skf2(X1))) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_1868,c_0_1858]),c_0_1885]),
[final] ).
cnf(c_0_1922,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_1886,c_0_77]),c_0_1790]),c_0_1887]),
[final] ).
cnf(c_0_1923,negated_conjecture,
( ~ ssRr(X1,X2)
| ~ ssPv3(skf2(skf2(X2)))
| ssPv1(X1) ),
inference(spm,[status(thm)],[c_0_1888,c_0_1757]),
[final] ).
cnf(c_0_1924,negated_conjecture,
( ~ ssPv3(skf2(X1))
| ssPv1(skf3(X1)) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_1795,c_0_1889]),c_0_1757]),
[final] ).
cnf(c_0_1925,negated_conjecture,
( ~ ssPv3(X1)
| ssPv1(skf2(skf3(skf3(X1)))) ),
inference(spm,[status(thm)],[c_0_1793,c_0_1890]),
[final] ).
cnf(c_0_1926,negated_conjecture,
( ~ ssPv3(skf2(X1))
| ssPv1(skf2(skf3(X1))) ),
inference(spm,[status(thm)],[c_0_1793,c_0_1891]),
[final] ).
cnf(c_0_1927,negated_conjecture,
( ~ ssRr(X3,X2)
| ~ ssRr(skf3(skf3(X1)),X3)
| ~ ssPv3(X2)
| ~ ssPv3(skf2(skf3(skf3(X1))))
| ssPv4(X1)
| ssPv4(skf3(skf3(X1))) ),
inference(spm,[status(thm)],[c_0_1892,c_0_53]),
[final] ).
cnf(c_0_1928,negated_conjecture,
( ~ ssPv3(X1)
| ssPv3(skf2(skf3(X1))) ),
inference(spm,[status(thm)],[c_0_1893,c_0_77]),
[final] ).
cnf(c_0_1930,negated_conjecture,
( ~ ssPv1(skf2(skf3(X1)))
| ssPv1(X1) ),
inference(spm,[status(thm)],[c_0_1833,c_0_1805]),
[final] ).
cnf(c_0_1931,negated_conjecture,
( ~ ssRr(X1,X2)
| ~ ssPv3(skf3(skf3(X2)))
| ssPv1(X1) ),
inference(spm,[status(thm)],[c_0_1831,c_0_1896]),
[final] ).
cnf(c_0_1933,negated_conjecture,
( ~ ssPv1(X1)
| ssPv1(skf2(skf2(X1))) ),
inference(spm,[status(thm)],[c_0_1788,c_0_1898]),
[final] ).
cnf(c_0_1934,negated_conjecture,
( ~ ssRr(X1,X2)
| ~ ssPv3(skf2(X2))
| ssPv1(X1) ),
inference(spm,[status(thm)],[c_0_1831,c_0_1757]),
[final] ).
cnf(c_0_1935,negated_conjecture,
( ~ ssRr(skf3(X1),X2)
| ~ ssPv3(X2)
| ssPv3(X1) ),
inference(spm,[status(thm)],[c_0_1851,c_0_77]),
[final] ).
cnf(c_0_1936,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_1899,c_0_77]),
[final] ).
cnf(c_0_1937,negated_conjecture,
( ~ ssRr(X2,X1)
| ~ ssPv1(X2)
| ~ ssPv1(skf3(skf2(X1)))
| ssPv1(skf2(skf2(skf2(X1))))
| ssPv3(skf2(X1)) ),
inference(spm,[status(thm)],[c_0_1347,c_0_53]),
[final] ).
cnf(c_0_1938,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_1900,c_0_77]),
[final] ).
cnf(c_0_1939,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_1940,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_1901,c_0_1902]),
[final] ).
cnf(c_0_1941,negated_conjecture,
( ~ ssRr(X2,skf3(skf3(skf3(X1))))
| ~ ssPv1(X2)
| ~ ssPv3(X1)
| ssPv1(skf3(skf3(skf3(skf3(X1))))) ),
inference(spm,[status(thm)],[c_0_1903,c_0_77]),
[final] ).
cnf(c_0_1942,negated_conjecture,
( ~ ssRr(X2,X3)
| ~ ssRr(X3,X1)
| ~ ssPv1(X2)
| ~ ssPv3(skf3(skf2(X1)))
| ssPv1(skf3(skf3(X1))) ),
inference(spm,[status(thm)],[c_0_1904,c_0_1902]),
[final] ).
cnf(c_0_1943,negated_conjecture,
( ~ ssPv1(X1)
| ~ ssPv1(skf3(skf3(skf2(X1))))
| ssPv1(skf2(skf2(skf2(X1)))) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_1905,c_0_77]),c_0_1906]),
[final] ).
cnf(c_0_1944,negated_conjecture,
( ~ ssRr(X2,skf3(skf3(X1)))
| ~ ssPv1(X2)
| ~ ssPv3(skf2(X1))
| ssPv1(skf3(skf3(skf3(X1)))) ),
inference(spm,[status(thm)],[c_0_1907,c_0_77]),
[final] ).
cnf(c_0_1945,negated_conjecture,
( ~ ssRr(X1,skf2(skf2(X2)))
| ~ ssPv1(X2)
| ssPv1(X1) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_1831,c_0_1908]),c_0_1909]),
[final] ).
cnf(c_0_1946,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_1831,c_0_1856]),c_0_1752]),c_0_1855]),
[final] ).
cnf(c_0_1947,negated_conjecture,
( ~ ssRr(X1,skf2(X2))
| ~ ssPv1(skf3(X2))
| ssPv1(X1) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_1831,c_0_1910]),c_0_1909]),
[final] ).
cnf(c_0_1948,negated_conjecture,
( ~ ssRr(skf3(X2),X1)
| ~ ssPv3(skf3(skf3(skf3(skf3(X2)))))
| ssPv3(X1) ),
inference(spm,[status(thm)],[c_0_1911,c_0_77]),
[final] ).
cnf(c_0_1949,negated_conjecture,
( ~ ssRr(skf3(X2),X1)
| ~ ssPv3(skf3(skf2(skf3(skf3(X2)))))
| ssPv3(X1) ),
inference(spm,[status(thm)],[c_0_1912,c_0_1902]),
[final] ).
cnf(c_0_1950,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_1913,c_0_1902]),c_0_1752]),c_0_1752]),
[final] ).
cnf(c_0_1951,negated_conjecture,
( ~ ssRr(skf3(X2),X1)
| ~ ssPv3(skf3(skf3(X2)))
| ssPv3(X1) ),
inference(spm,[status(thm)],[c_0_1912,c_0_1914]),
[final] ).
cnf(c_0_1952,negated_conjecture,
( ~ ssPv3(skf3(skf2(skf3(skf3(X1)))))
| ssPv3(X1) ),
inference(spm,[status(thm)],[c_0_1915,c_0_1902]),
[final] ).
cnf(c_0_1953,negated_conjecture,
( ~ ssPv3(X1)
| ~ ssPv3(skf3(skf3(skf3(X1)))) ),
inference(spm,[status(thm)],[c_0_1897,c_0_1902]),
[final] ).
cnf(c_0_1954,negated_conjecture,
( ~ ssPv3(skf3(skf2(skf3(X1))))
| ssPv3(skf2(X1)) ),
inference(spm,[status(thm)],[c_0_1916,c_0_1902]),
[final] ).
cnf(c_0_1955,negated_conjecture,
( ~ ssPv3(skf2(X1))
| ~ ssPv3(skf3(skf3(X1))) ),
inference(spm,[status(thm)],[c_0_1863,c_0_1902]),
[final] ).
cnf(c_0_1956,negated_conjecture,
( ~ ssPv3(X1)
| ~ ssPv3(skf3(skf2(skf3(X1)))) ),
inference(spm,[status(thm)],[c_0_1917,c_0_1902]),
[final] ).
cnf(c_0_1957,negated_conjecture,
( ~ ssPv3(X1)
| ssPv3(skf3(skf2(X1))) ),
inference(spm,[status(thm)],[c_0_1918,c_0_1914]),
[final] ).
cnf(c_0_1958,negated_conjecture,
( ~ ssPv3(skf3(skf2(X1)))
| ssPv3(X1) ),
inference(spm,[status(thm)],[c_0_1844,c_0_1902]),
[final] ).
cnf(c_0_1959,negated_conjecture,
( ~ ssPv3(skf3(skf3(X1)))
| ssPv3(X1) ),
inference(spm,[status(thm)],[c_0_1877,c_0_77]),
[final] ).
cnf(c_0_1960,negated_conjecture,
( ~ ssRr(skf3(X3),X2)
| ~ ssRr(skf3(X3),X1)
| ~ ssPv3(X2)
| ssPv3(X1) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1850,c_0_77]),c_0_1790]),
[final] ).
cnf(c_0_1961,negated_conjecture,
( ~ ssRr(X1,skf3(X2))
| ~ ssPv1(X2)
| ssPv1(X1) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_1831,c_0_1919]),c_0_1909]),
[final] ).
cnf(c_0_1962,negated_conjecture,
( ~ ssRr(skf3(X2),X1)
| ~ ssPv3(skf2(skf3(X2)))
| ssPv3(X1) ),
inference(spm,[status(thm)],[c_0_1912,c_0_1891]),
[final] ).
cnf(c_0_1963,negated_conjecture,
( ~ ssRr(skf3(X2),X1)
| ~ ssPv3(X2)
| ssPv3(X1) ),
inference(spm,[status(thm)],[c_0_1912,c_0_1890]),
[final] ).
cnf(c_0_1964,negated_conjecture,
( ~ ssRr(X1,skf2(skf2(X2)))
| ~ ssPv3(X2)
| ssPv1(X1) ),
inference(spm,[status(thm)],[c_0_1831,c_0_1920]),
[final] ).
cnf(c_0_1965,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_1831,c_0_1821]),c_0_1752]),c_0_1855]),
[final] ).
cnf(c_0_1966,negated_conjecture,
( ~ ssRr(X1,skf2(X2))
| ~ ssPv3(skf3(X2))
| ssPv1(X1) ),
inference(spm,[status(thm)],[c_0_1831,c_0_1921]),
[final] ).
cnf(c_0_1967,negated_conjecture,
( ~ ssRr(X2,skf3(X1))
| ~ ssPv3(X2)
| ssPv1(skf3(skf3(X1))) ),
inference(spm,[status(thm)],[c_0_1818,c_0_77]),
[final] ).
cnf(c_0_1968,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_1823,c_0_77]),c_0_1790]),c_0_1918]),
[final] ).
cnf(c_0_1969,negated_conjecture,
( ~ ssRr(X1,skf2(X2))
| ~ ssPv3(X2)
| ssPv1(X1) ),
inference(spm,[status(thm)],[c_0_1875,c_0_1874]),
[final] ).
cnf(c_0_1970,negated_conjecture,
( ~ ssRr(X2,skf3(X1))
| ~ ssPv1(X2)
| ssPv1(X1) ),
inference(spm,[status(thm)],[c_0_1922,c_0_77]),
[final] ).
cnf(c_0_1971,negated_conjecture,
( ~ ssRr(X2,X1)
| ~ ssPv1(X2)
| ssPv1(skf2(X1)) ),
inference(spm,[status(thm)],[c_0_1922,c_0_53]),
[final] ).
cnf(c_0_1972,negated_conjecture,
( ~ ssPv3(X1)
| ssPv1(skf3(skf2(skf2(X1)))) ),
inference(spm,[status(thm)],[c_0_1788,c_0_1874]),
[final] ).
cnf(c_0_1973,negated_conjecture,
( ~ ssPv3(skf3(X1))
| ssPv1(skf3(skf2(X1))) ),
inference(spm,[status(thm)],[c_0_1788,c_0_1858]),
[final] ).
cnf(c_0_1974,negated_conjecture,
( ~ ssRr(X1,X3)
| ~ ssRr(X2,skf3(skf2(X3)))
| ~ ssPv3(X2)
| ssPv1(X1) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1719,c_0_77]),c_0_1752]),
[final] ).
cnf(c_0_1975,negated_conjecture,
( ~ ssRr(X1,skf3(skf3(X2)))
| ~ ssPv3(X2)
| ssPv1(X1) ),
inference(spm,[status(thm)],[c_0_1923,c_0_1890]),
[final] ).
cnf(c_0_1976,negated_conjecture,
( ~ ssRr(X1,skf3(X2))
| ~ ssPv3(skf2(X2))
| ssPv1(X1) ),
inference(spm,[status(thm)],[c_0_1923,c_0_1891]),
[final] ).
cnf(c_0_1977,negated_conjecture,
( ~ ssPv3(X1)
| ssPv3(skf3(skf2(skf3(skf3(X1))))) ),
inference(spm,[status(thm)],[c_0_1918,c_0_1890]),
[final] ).
cnf(c_0_1978,negated_conjecture,
( ~ ssPv3(X1)
| ssPv1(skf3(skf2(skf3(skf3(X1))))) ),
inference(spm,[status(thm)],[c_0_1924,c_0_1890]),
[final] ).
cnf(c_0_1979,negated_conjecture,
( ~ ssPv3(skf2(X1))
| ssPv3(skf3(skf2(skf3(X1)))) ),
inference(spm,[status(thm)],[c_0_1918,c_0_1891]),
[final] ).
cnf(c_0_1980,negated_conjecture,
( ~ ssPv3(skf2(X1))
| ssPv1(skf3(skf2(skf3(X1)))) ),
inference(spm,[status(thm)],[c_0_1924,c_0_1891]),
[final] ).
cnf(c_0_1981,negated_conjecture,
( ~ ssPv3(X1)
| ssPv1(skf3(skf3(skf3(X1)))) ),
inference(spm,[status(thm)],[c_0_1837,c_0_1925]),
[final] ).
cnf(c_0_1982,negated_conjecture,
( ~ ssPv3(skf2(X1))
| ssPv1(skf3(skf3(X1))) ),
inference(spm,[status(thm)],[c_0_1837,c_0_1926]),
[final] ).
cnf(c_0_1983,negated_conjecture,
( ~ ssRr(skf3(X1),X2)
| ~ ssPv3(X2)
| ~ ssPv3(skf2(skf3(skf3(X1)))) ),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1927,c_0_77]),c_0_1752]),c_0_1752]),
[final] ).
cnf(c_0_1984,negated_conjecture,
( ~ ssPv3(X1)
| ssPv3(skf3(skf3(X1))) ),
inference(spm,[status(thm)],[c_0_1883,c_0_77]),
[final] ).
cnf(c_0_1985,negated_conjecture,
( ~ ssRr(X2,X1)
| ~ ssPv3(X2)
| ~ ssPv3(X1) ),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1913,c_0_1928]),c_0_1752]),c_0_1752]),
[final] ).
cnf(c_0_1986,negated_conjecture,
( ~ ssPv3(X1)
| ~ ssPv3(skf2(X1)) ),
inference(spm,[status(thm)],[c_0_1863,c_0_1928]),
[final] ).
cnf(c_0_1987,negated_conjecture,
( ~ ssPv1(skf3(skf3(skf3(X1))))
| ssPv1(X1) ),
inference(spm,[status(thm)],[c_0_1929,c_0_77]),
[final] ).
cnf(c_0_1988,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_1694,c_0_77]),c_0_1691]),c_0_1752]),
[final] ).
cnf(c_0_1989,negated_conjecture,
( ~ ssPv3(skf3(skf3(skf3(X1))))
| ssPv1(X1) ),
inference(spm,[status(thm)],[c_0_1930,c_0_1896]),
[final] ).
cnf(c_0_1990,negated_conjecture,
( ~ ssPv3(skf3(skf2(skf3(X1))))
| ssPv1(X1) ),
inference(spm,[status(thm)],[c_0_1833,c_0_1757]),
[final] ).
cnf(c_0_1991,negated_conjecture,
( ~ ssPv3(skf2(skf3(X1)))
| ssPv1(X1) ),
inference(spm,[status(thm)],[c_0_1833,c_0_1787]),
[final] ).
cnf(c_0_1992,negated_conjecture,
( ~ ssPv3(skf3(skf3(skf2(X1))))
| ssPv1(X1) ),
inference(spm,[status(thm)],[c_0_1931,c_0_53]),
[final] ).
cnf(c_0_1993,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_1805]),c_0_1691]),c_0_1752]),
[final] ).
cnf(c_0_1994,negated_conjecture,
( ~ ssPv3(X1)
| ssPv1(skf3(skf3(X1))) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_1795,c_0_1932]),c_0_1757]),
[final] ).
cnf(c_0_1995,negated_conjecture,
( ~ ssRr(X1,skf2(X2))
| ~ ssPv1(X2)
| ssPv1(X1) ),
inference(spm,[status(thm)],[c_0_1831,c_0_1933]),
[final] ).
cnf(c_0_1996,negated_conjecture,
( ~ ssRr(X1,X2)
| ~ ssPv1(skf3(X2))
| ssPv1(X1) ),
inference(spm,[status(thm)],[c_0_1831,c_0_1817]),
[final] ).
cnf(c_0_1997,negated_conjecture,
( ~ ssPv3(skf2(skf2(X1)))
| ssPv1(X1) ),
inference(spm,[status(thm)],[c_0_1934,c_0_53]),
[final] ).
cnf(c_0_1998,negated_conjecture,
( ~ ssPv1(X1)
| ssPv1(skf3(skf2(skf2(X1)))) ),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1788,c_0_1842]),c_0_1691]),c_0_1752]),
[final] ).
cnf(c_0_1999,negated_conjecture,
( ~ ssPv3(skf2(skf3(X1)))
| ssPv3(X1) ),
inference(spm,[status(thm)],[c_0_1935,c_0_53]),
[final] ).
cnf(c_0_2000,negated_conjecture,
( ~ ssRr(X2,skf2(X1))
| ~ ssPv3(X2)
| ssPv1(X1) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1725,c_0_53]),c_0_1752]),
[final] ).
cnf(c_0_2001,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_1896]),c_0_1752]),
[final] ).
cnf(c_0_2002,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_1757]),c_0_1691]),c_0_1752]),
[final] ).
cnf(c_0_2003,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_1849,c_0_53]),
[final] ).
cnf(c_0_2004,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_1787]),c_0_1691]),c_0_1752]),
[final] ).
cnf(c_0_2005,negated_conjecture,
( ~ ssRr(X4,X3)
| ~ ssRr(skf3(skf3(X1)),X4)
| ~ ssRr(skf2(skf3(skf3(X1))),X2)
| ~ ssPv3(X3)
| ssPv3(X2)
| ssPv2(X1) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1829,c_0_53]),c_0_1752]),
[final] ).
cnf(c_0_2006,negated_conjecture,
( ~ ssPv3(skf3(skf2(X1)))
| ssPv1(X1) ),
inference(spm,[status(thm)],[c_0_1786,c_0_1757]),
[final] ).
cnf(c_0_2007,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_1936,c_0_77]),
[final] ).
cnf(c_0_2008,negated_conjecture,
( ~ ssPv1(X1)
| ~ ssPv1(skf2(X1))
| ssPv1(skf2(skf2(skf2(skf2(X1)))))
| ssPv3(skf2(skf2(X1))) ),
inference(spm,[status(thm)],[c_0_1705,c_0_53]),
[final] ).
cnf(c_0_2009,negated_conjecture,
( ~ ssRr(X3,X2)
| ~ ssRr(skf3(skf3(X1)),X3)
| ~ ssPv3(X2)
| ~ ssPv3(skf3(X1))
| ssPv4(X1)
| ssPv4(skf3(skf3(X1))) ),
inference(spm,[status(thm)],[c_0_1892,c_0_77]),
[final] ).
cnf(c_0_2010,negated_conjecture,
( ~ ssPv1(X1)
| ssPv1(skf3(skf3(skf2(skf2(X1)))))
| ssPv4(skf2(X1)) ),
inference(spm,[status(thm)],[c_0_1698,c_0_53]),
[final] ).
cnf(c_0_2011,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_1796,c_0_53]),
[final] ).
cnf(c_0_2012,negated_conjecture,
( ~ ssPv1(X1)
| ~ ssPv1(skf3(skf2(skf2(X1))))
| ssPv1(skf2(skf2(skf2(skf2(X1)))))
| ssPv3(skf2(skf2(X1))) ),
inference(spm,[status(thm)],[c_0_1937,c_0_53]),
[final] ).
cnf(c_0_2013,negated_conjecture,
( ~ ssPv1(skf3(X1))
| ~ ssPv1(skf3(skf2(X1)))
| ssPv1(skf2(skf2(skf2(X1))))
| ssPv3(skf2(X1)) ),
inference(spm,[status(thm)],[c_0_1937,c_0_77]),
[final] ).
cnf(c_0_2014,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_1938,c_0_77]),
[final] ).
cnf(c_0_2015,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_2016,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_2017,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_1812,c_0_53]),
[final] ).
cnf(c_0_2018,negated_conjecture,
( ~ ssPv1(skf2(X1))
| ssPv1(skf2(skf3(X1)))
| ssPv3(skf3(X1))
| ssPv4(X1) ),
inference(spm,[status(thm)],[c_0_1785,c_0_53]),
[final] ).
cnf(c_0_2019,negated_conjecture,
( ~ ssPv1(skf2(skf2(skf3(X1))))
| ssPv1(X1)
| ssPv3(skf3(X1))
| ssPv4(skf2(skf3(X1))) ),
inference(spm,[status(thm)],[c_0_1939,c_0_53]),
[final] ).
cnf(c_0_2020,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_1789,c_0_77]),
[final] ).
cnf(c_0_2021,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.04 % Problem : SYN798-1 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.07 % Command : run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.18/10.46 % Computer : n006.cluster.edu
% 0.18/10.46 % Model : x86_64 x86_64
% 0.18/10.46 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/10.46 % Memory : 8046.5625MB
% 0.18/10.46 % OS : Linux 6.8.0-71-generic
% 0.18/10.46 % CPULimit : 300
% 0.18/10.46 % WCLimit : 300
% 0.18/10.46 % DateTime : Mon Sep 21 11:16:52 UTC 2026
% 0.18/10.47 % CPUTime :
% 0.18/10.47 Running run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.24/10.53 Running first-order theorem proving
% 0.24/10.54 Running: /export/starexec/sandbox/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/sandbox/benchmark/theBenchmark.p
% 24.58/14.13 % Version: 3.5.1
% 24.58/14.13 % Preprocessing class: FSLSSMSSSSSNFFN.
% 24.58/14.13 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 24.58/14.13 % Starting G-E--_207_C18_F1_SE_CS_SP_PI_PS_S5PRR_S2S with 1500s (5) cores
% 24.58/14.13 % Starting new_bool_3 with 300s (1) cores
% 24.58/14.13 % Starting new_bool_1 with 300s (1) cores
% 24.58/14.13 % Starting sh5l with 300s (1) cores
% 24.58/14.13 % G-E--_207_C18_F1_SE_CS_SP_PI_PS_S5PRR_S2S with pid 2719628 completed with status 1
% 24.58/14.13 % Result found by G-E--_207_C18_F1_SE_CS_SP_PI_PS_S5PRR_S2S
% 24.58/14.13 % Preprocessing class: FSLSSMSSSSSNFFN.
% 24.58/14.13 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 24.58/14.13 % Starting G-E--_207_C18_F1_SE_CS_SP_PI_PS_S5PRR_S2S with 1500s (5) cores
% 24.58/14.13 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 24.58/14.13 % No SInE strategy applied
% 24.58/14.13 % Search class: FGHNS-FSMF11-SFFFFFNN
% 24.58/14.13 % Scheduled 7 strats onto 5 cores with 1500 seconds (1500 total)
% 24.58/14.13 % Starting SubtermCWHack with 136s (1) cores
% 24.58/14.13 % Starting G-E--_207_C18_F1_SE_CS_SP_PI_PS_S5PRR_S2S with 151s (1) cores
% 24.58/14.13 % Starting G-E--_107_C09_12_F1_PI_AE_Q4_CS_SP_PS_S063N with 136s (1) cores
% 24.58/14.13 % Starting new_bool_3 with 136s (1) cores
% 24.58/14.13 % Starting new_bool_1 with 136s (1) cores
% 24.58/14.13 % G-E--_107_C09_12_F1_PI_AE_Q4_CS_SP_PS_S063N with pid 2719634 completed with status 1
% 24.58/14.13 % Result found by G-E--_107_C09_12_F1_PI_AE_Q4_CS_SP_PS_S063N
% 24.58/14.13 % Preprocessing class: FSLSSMSSSSSNFFN.
% 24.58/14.13 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 24.58/14.13 % Starting G-E--_207_C18_F1_SE_CS_SP_PI_PS_S5PRR_S2S with 1500s (5) cores
% 24.58/14.13 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 24.58/14.13 % No SInE strategy applied
% 24.58/14.13 % Search class: FGHNS-FSMF11-SFFFFFNN
% 24.58/14.13 % Scheduled 7 strats onto 5 cores with 1500 seconds (1500 total)
% 24.58/14.13 % Starting SubtermCWHack with 136s (1) cores
% 24.58/14.13 % Starting G-E--_207_C18_F1_SE_CS_SP_PI_PS_S5PRR_S2S with 151s (1) cores
% 24.58/14.13 % Starting G-E--_107_C09_12_F1_PI_AE_Q4_CS_SP_PS_S063N with 136s (1) cores
% 24.58/14.13 % Preprocessing time : 0.002 s
% 24.58/14.13 % Presaturation interreduction done
% 24.58/14.13
% 24.58/14.13 % No proof found!
% 24.58/14.13 % SZS status Satisfiable
% 24.58/14.13 % SZS output start Saturation
% See solution above
% 24.58/14.13 % Parsed axioms : 52
% 24.58/14.13 % Removed by relevancy pruning/SinE : 0
% 24.58/14.13 % Initial clauses : 52
% 24.58/14.13 % Removed in clause preprocessing : 0
% 24.58/14.13 % Initial clauses in saturation : 52
% 24.58/14.13 % Processed clauses : 17046
% 24.58/14.13 % ...of these trivial : 0
% 24.58/14.13 % ...subsumed : 10866
% 24.58/14.13 % ...remaining for further processing : 6180
% 24.58/14.13 % Other redundant clauses eliminated : 0
% 24.58/14.13 % Clauses deleted for lack of memory : 0
% 24.58/14.13 % Backward-subsumed : 5847
% 24.58/14.13 % Backward-rewritten : 0
% 24.58/14.13 % Generated clauses : 168656
% 24.58/14.13 % ...of the previous two non-redundant : 107323
% 24.58/14.13 % ...aggressively subsumed : 0
% 24.58/14.13 % Contextual simplify-reflections : 2306
% 24.58/14.13 % Paramodulations : 168656
% 24.58/14.13 % Factorizations : 0
% 24.58/14.13 % NegExts : 0
% 24.58/14.13 % Equation resolutions : 0
% 24.58/14.13 % Disequality decompositions : 0
% 24.58/14.13 % Total rewrite steps : 0
% 24.58/14.13 % ...of those cached : 0
% 24.58/14.13 % Propositional unsat checks : 0
% 24.58/14.13 % Propositional check models : 0
% 24.58/14.13 % Propositional check unsatisfiable : 0
% 24.58/14.13 % Propositional clauses : 0
% 24.58/14.13 % Propositional clauses after purity: 0
% 24.58/14.13 % Propositional unsat core size : 0
% 24.58/14.13 % Propositional preprocessing time : 0.000
% 24.58/14.13 % Propositional encoding time : 0.000
% 24.58/14.13 % Propositional solver time : 0.000
% 24.58/14.13 % Success case prop preproc time : 0.000
% 24.58/14.13 % Success case prop encoding time : 0.000
% 24.58/14.13 % Success case prop solver time : 0.000
% 24.58/14.13 % Current number of processed clauses : 281
% 24.58/14.13 % Positive orientable unit clauses : 2
% 24.58/14.13 % Positive unorientable unit clauses: 0
% 24.58/14.13 % Negative unit clauses : 2
% 24.58/14.13 % Non-unit-clauses : 277
% 24.58/14.13 % Current number of unprocessed clauses: 0
% 24.58/14.13 % ...number of literals in the above : 0
% 24.58/14.13 % Current number of archived formulas : 0
% 24.58/14.13 % Current number of archived clauses : 5899
% 24.58/14.13 % Clause-clause subsumption calls (NU) : 552809
% 24.58/14.13 % Rec. Clause-clause subsumption calls : 115679
% 24.58/14.13 % Non-unit clause-clause subsumptions : 18258
% 24.58/14.13 % Unit Clause-clause subsumption calls : 1102
% 24.58/14.13 % Rewrite failures with RHS unbound : 0
% 24.58/14.13 % BW rewrite match attempts : 0
% 24.58/14.13 % BW rewrite match successes : 0
% 24.58/14.13 % Condensation attempts : 0
% 24.58/14.13 % Condensation successes : 0
% 24.58/14.13 % Termbank termtop insertions : 4237189
% 24.58/14.13 % Search garbage collected termcells : 365
% 24.58/14.13
% 24.58/14.13 % -------------------------------------------------
% 24.58/14.13 % User time : 3.469 s
% 24.58/14.13 % System time : 0.060 s
% 24.58/14.13 % Total time : 3.529 s
% 24.58/14.13 % Maximum resident set size: 3952 pages
% 24.58/14.13
% 24.58/14.13 % -------------------------------------------------
% 24.58/14.13 % User time : 17.136 s
% 24.58/14.13 % System time : 0.274 s
% 24.58/14.13 % Total time : 17.410 s
% 24.58/14.13 % Maximum resident set size: 4864 pages
% 24.58/14.13 % E exiting
%------------------------------------------------------------------------------