%------------------------------------------------------------------------------
% File : ConnectPP---0.7.2
% Problem : SYO614-1 : TPTP v9.3.1. Released v7.1.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 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 09:12:11 AM UTC 2026
% Result : Unsatisfiable 0.84s 11.32s
% Output : Proof 0.84s
% Verified :
% SZS Type : Refutation
% Derivation depth : 2
% Number of leaves : 6
% Syntax : Number of clauses : 83 ( 47 unt; 7 nHn; 68 RR)
% Number of literals : 128 ( 0 equ; 47 neg)
% Maximal clause size : 3 ( 1 avg)
% Maximal term depth : 14 ( 4 avg)
% Number of predicates : 3 ( 2 usr; 1 prp; 0-2 aty)
% Number of functors : 5 ( 5 usr; 2 con; 0-2 aty)
% Number of variables : 276 ( 2 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(sos_01,axiom,
le(A,A),
file('theBenchmark.p',sos_01) ).
cnf(sos_02,axiom,
( le(A,C)
| ~ le(max(A,B),C) ),
file('theBenchmark.p',sos_02) ).
cnf(sos_03,axiom,
( le(B,C)
| ~ le(max(A,B),C) ),
file('theBenchmark.p',sos_03) ).
cnf(sos_04,axiom,
( eq(f(A),a1)
| eq(f(A),a0) ),
file('theBenchmark.p',sos_04) ).
cnf(sos_05,axiom,
( ~ le(s(A0),A1)
| ~ eq(f(A1),a0)
| ~ eq(f(A0),a0) ),
file('theBenchmark.p',sos_05) ).
cnf(sos_06,axiom,
( ~ le(s(A0),A1)
| ~ eq(f(A1),a1)
| ~ eq(f(A0),a1) ),
file('theBenchmark.p',sos_06) ).
cnf(t1,plain,
( ~ eq(f(max(U_167,max(U_164,max(U_161,max(U_158,max(U_155,max(U_152,s(U_123)))))))),a0)
| ~ le(s(U_123),max(U_167,max(U_164,max(U_161,max(U_158,max(U_155,max(U_152,s(U_123))))))))
| ~ eq(f(U_123),a0) ),
inference(start,[status(thm),parent(0:0)],[sos_05]) ).
cnf(t2,plain,
( eq(f(U_123),a1)
| eq(f(U_123),a0) ),
inference(extension,[status(thm),parent(t1:1)],[sos_04]) ).
cnf(t3,plain,
$false,
inference(connection,[status(thm),parent(t2:1)],[t2:1,t1:1]) ).
cnf(t4,plain,
( ~ eq(f(max(max(U_145,s(s(U_123))),max(U_131,max(U_128,max(U_125,s(U_123)))))),a1)
| ~ le(s(U_123),max(max(U_145,s(s(U_123))),max(U_131,max(U_128,max(U_125,s(U_123))))))
| ~ eq(f(U_123),a1) ),
inference(extension,[status(thm),parent(t2:2)],[sos_06]) ).
cnf(t5,plain,
$false,
inference(connection,[status(thm),parent(t4:1)],[t4:1,t2:2]) ).
cnf(t6,plain,
( ~ le(max(U_125,s(U_123)),max(max(U_145,s(s(U_123))),max(U_131,max(U_128,max(U_125,s(U_123))))))
| le(s(U_123),max(max(U_145,s(s(U_123))),max(U_131,max(U_128,max(U_125,s(U_123)))))) ),
inference(extension,[status(thm),parent(t4:2)],[sos_03]) ).
cnf(t7,plain,
$false,
inference(connection,[status(thm),parent(t6:1)],[t6:1,t4:2]) ).
cnf(t8,plain,
( ~ le(max(U_128,max(U_125,s(U_123))),max(max(U_145,s(s(U_123))),max(U_131,max(U_128,max(U_125,s(U_123))))))
| le(max(U_125,s(U_123)),max(max(U_145,s(s(U_123))),max(U_131,max(U_128,max(U_125,s(U_123)))))) ),
inference(extension,[status(thm),parent(t6:2)],[sos_03]) ).
cnf(t9,plain,
$false,
inference(connection,[status(thm),parent(t8:1)],[t8:1,t6:2]) ).
cnf(t10,plain,
( ~ le(max(U_131,max(U_128,max(U_125,s(U_123)))),max(max(U_145,s(s(U_123))),max(U_131,max(U_128,max(U_125,s(U_123))))))
| le(max(U_128,max(U_125,s(U_123))),max(max(U_145,s(s(U_123))),max(U_131,max(U_128,max(U_125,s(U_123)))))) ),
inference(extension,[status(thm),parent(t8:2)],[sos_03]) ).
cnf(t11,plain,
$false,
inference(connection,[status(thm),parent(t10:1)],[t10:1,t8:2]) ).
cnf(t12,plain,
( ~ le(max(max(U_145,s(s(U_123))),max(U_131,max(U_128,max(U_125,s(U_123))))),max(max(U_145,s(s(U_123))),max(U_131,max(U_128,max(U_125,s(U_123))))))
| le(max(U_131,max(U_128,max(U_125,s(U_123)))),max(max(U_145,s(s(U_123))),max(U_131,max(U_128,max(U_125,s(U_123)))))) ),
inference(extension,[status(thm),parent(t10:2)],[sos_03]) ).
cnf(t13,plain,
$false,
inference(connection,[status(thm),parent(t12:1)],[t12:1,t10:2]) ).
cnf(t14,plain,
le(max(max(U_145,s(s(U_123))),max(U_131,max(U_128,max(U_125,s(U_123))))),max(max(U_145,s(s(U_123))),max(U_131,max(U_128,max(U_125,s(U_123)))))),
inference(extension,[status(thm),parent(t12:2)],[sos_01]) ).
cnf(t15,plain,
$false,
inference(connection,[status(thm),parent(t14:1)],[t14:1,t12:2]) ).
cnf(t16,plain,
( eq(f(max(max(U_145,s(s(U_123))),max(U_131,max(U_128,max(U_125,s(U_123)))))),a0)
| eq(f(max(max(U_145,s(s(U_123))),max(U_131,max(U_128,max(U_125,s(U_123)))))),a1) ),
inference(extension,[status(thm),parent(t4:3)],[sos_04]) ).
cnf(t17,plain,
$false,
inference(connection,[status(thm),parent(t16:1)],[t16:1,t4:3]) ).
cnf(t18,plain,
( ~ le(s(s(U_123)),max(max(U_145,s(s(U_123))),max(U_131,max(U_128,max(U_125,s(U_123))))))
| ~ eq(f(s(U_123)),a0)
| ~ eq(f(max(max(U_145,s(s(U_123))),max(U_131,max(U_128,max(U_125,s(U_123)))))),a0) ),
inference(extension,[status(thm),parent(t16:2)],[sos_05]) ).
cnf(t19,plain,
$false,
inference(connection,[status(thm),parent(t18:1)],[t18:1,t16:2]) ).
cnf(t20,plain,
( eq(f(s(U_123)),a1)
| eq(f(s(U_123)),a0) ),
inference(extension,[status(thm),parent(t18:2)],[sos_04]) ).
cnf(t21,plain,
$false,
inference(connection,[status(thm),parent(t20:1)],[t20:1,t18:2]) ).
cnf(t22,plain,
( ~ le(s(U_123),s(U_123))
| ~ eq(f(U_123),a1)
| ~ eq(f(s(U_123)),a1) ),
inference(extension,[status(thm),parent(t20:2)],[sos_06]) ).
cnf(t23,plain,
$false,
inference(connection,[status(thm),parent(t22:1)],[t22:1,t20:2]) ).
cnf(t24,plain,
$false,
inference(reduction,[status(thm),parent(t22:2)],[t22:2,t2:2]) ).
cnf(t25,plain,
le(s(U_123),s(U_123)),
inference(extension,[status(thm),parent(t22:3)],[sos_01]) ).
cnf(t26,plain,
$false,
inference(connection,[status(thm),parent(t25:1)],[t25:1,t22:3]) ).
cnf(t27,plain,
( ~ le(max(U_145,s(s(U_123))),max(max(U_145,s(s(U_123))),max(U_131,max(U_128,max(U_125,s(U_123))))))
| le(s(s(U_123)),max(max(U_145,s(s(U_123))),max(U_131,max(U_128,max(U_125,s(U_123)))))) ),
inference(extension,[status(thm),parent(t18:3)],[sos_03]) ).
cnf(t28,plain,
$false,
inference(connection,[status(thm),parent(t27:1)],[t27:1,t18:3]) ).
cnf(t29,plain,
( ~ le(max(max(U_145,s(s(U_123))),max(U_131,max(U_128,max(U_125,s(U_123))))),max(max(U_145,s(s(U_123))),max(U_131,max(U_128,max(U_125,s(U_123))))))
| le(max(U_145,s(s(U_123))),max(max(U_145,s(s(U_123))),max(U_131,max(U_128,max(U_125,s(U_123)))))) ),
inference(extension,[status(thm),parent(t27:2)],[sos_02]) ).
cnf(t30,plain,
$false,
inference(connection,[status(thm),parent(t29:1)],[t29:1,t27:2]) ).
cnf(t31,plain,
le(max(max(U_145,s(s(U_123))),max(U_131,max(U_128,max(U_125,s(U_123))))),max(max(U_145,s(s(U_123))),max(U_131,max(U_128,max(U_125,s(U_123)))))),
inference(extension,[status(thm),parent(t29:2)],[sos_01]) ).
cnf(t32,plain,
$false,
inference(connection,[status(thm),parent(t31:1)],[t31:1,t29:2]) ).
cnf(t33,plain,
( ~ le(max(U_152,s(U_123)),max(U_167,max(U_164,max(U_161,max(U_158,max(U_155,max(U_152,s(U_123))))))))
| le(s(U_123),max(U_167,max(U_164,max(U_161,max(U_158,max(U_155,max(U_152,s(U_123)))))))) ),
inference(extension,[status(thm),parent(t1:2)],[sos_03]) ).
cnf(t34,plain,
$false,
inference(connection,[status(thm),parent(t33:1)],[t33:1,t1:2]) ).
cnf(t35,plain,
( ~ le(max(U_155,max(U_152,s(U_123))),max(U_167,max(U_164,max(U_161,max(U_158,max(U_155,max(U_152,s(U_123))))))))
| le(max(U_152,s(U_123)),max(U_167,max(U_164,max(U_161,max(U_158,max(U_155,max(U_152,s(U_123)))))))) ),
inference(extension,[status(thm),parent(t33:2)],[sos_03]) ).
cnf(t36,plain,
$false,
inference(connection,[status(thm),parent(t35:1)],[t35:1,t33:2]) ).
cnf(t37,plain,
( ~ le(max(U_158,max(U_155,max(U_152,s(U_123)))),max(U_167,max(U_164,max(U_161,max(U_158,max(U_155,max(U_152,s(U_123))))))))
| le(max(U_155,max(U_152,s(U_123))),max(U_167,max(U_164,max(U_161,max(U_158,max(U_155,max(U_152,s(U_123)))))))) ),
inference(extension,[status(thm),parent(t35:2)],[sos_03]) ).
cnf(t38,plain,
$false,
inference(connection,[status(thm),parent(t37:1)],[t37:1,t35:2]) ).
cnf(t39,plain,
( ~ le(max(U_161,max(U_158,max(U_155,max(U_152,s(U_123))))),max(U_167,max(U_164,max(U_161,max(U_158,max(U_155,max(U_152,s(U_123))))))))
| le(max(U_158,max(U_155,max(U_152,s(U_123)))),max(U_167,max(U_164,max(U_161,max(U_158,max(U_155,max(U_152,s(U_123)))))))) ),
inference(extension,[status(thm),parent(t37:2)],[sos_03]) ).
cnf(t40,plain,
$false,
inference(connection,[status(thm),parent(t39:1)],[t39:1,t37:2]) ).
cnf(t41,plain,
( ~ le(max(U_164,max(U_161,max(U_158,max(U_155,max(U_152,s(U_123)))))),max(U_167,max(U_164,max(U_161,max(U_158,max(U_155,max(U_152,s(U_123))))))))
| le(max(U_161,max(U_158,max(U_155,max(U_152,s(U_123))))),max(U_167,max(U_164,max(U_161,max(U_158,max(U_155,max(U_152,s(U_123)))))))) ),
inference(extension,[status(thm),parent(t39:2)],[sos_03]) ).
cnf(t42,plain,
$false,
inference(connection,[status(thm),parent(t41:1)],[t41:1,t39:2]) ).
cnf(t43,plain,
( ~ le(max(U_167,max(U_164,max(U_161,max(U_158,max(U_155,max(U_152,s(U_123))))))),max(U_167,max(U_164,max(U_161,max(U_158,max(U_155,max(U_152,s(U_123))))))))
| le(max(U_164,max(U_161,max(U_158,max(U_155,max(U_152,s(U_123)))))),max(U_167,max(U_164,max(U_161,max(U_158,max(U_155,max(U_152,s(U_123)))))))) ),
inference(extension,[status(thm),parent(t41:2)],[sos_03]) ).
cnf(t44,plain,
$false,
inference(connection,[status(thm),parent(t43:1)],[t43:1,t41:2]) ).
cnf(t45,plain,
le(max(U_167,max(U_164,max(U_161,max(U_158,max(U_155,max(U_152,s(U_123))))))),max(U_167,max(U_164,max(U_161,max(U_158,max(U_155,max(U_152,s(U_123)))))))),
inference(extension,[status(thm),parent(t43:2)],[sos_01]) ).
cnf(t46,plain,
$false,
inference(connection,[status(thm),parent(t45:1)],[t45:1,t43:2]) ).
cnf(t47,plain,
( eq(f(max(U_167,max(U_164,max(U_161,max(U_158,max(U_155,max(U_152,s(U_123)))))))),a1)
| eq(f(max(U_167,max(U_164,max(U_161,max(U_158,max(U_155,max(U_152,s(U_123)))))))),a0) ),
inference(extension,[status(thm),parent(t1:3)],[sos_04]) ).
cnf(t48,plain,
$false,
inference(connection,[status(thm),parent(t47:1)],[t47:1,t1:3]) ).
cnf(t49,plain,
( ~ eq(f(max(max(U_194,s(s(max(U_167,max(U_164,max(U_161,max(U_158,max(U_155,max(U_152,s(U_123)))))))))),max(U_180,max(U_177,max(U_174,s(max(U_167,max(U_164,max(U_161,max(U_158,max(U_155,max(U_152,s(U_123))))))))))))),a1)
| ~ le(s(max(U_167,max(U_164,max(U_161,max(U_158,max(U_155,max(U_152,s(U_123)))))))),max(max(U_194,s(s(max(U_167,max(U_164,max(U_161,max(U_158,max(U_155,max(U_152,s(U_123)))))))))),max(U_180,max(U_177,max(U_174,s(max(U_167,max(U_164,max(U_161,max(U_158,max(U_155,max(U_152,s(U_123)))))))))))))
| ~ eq(f(max(U_167,max(U_164,max(U_161,max(U_158,max(U_155,max(U_152,s(U_123)))))))),a1) ),
inference(extension,[status(thm),parent(t47:2)],[sos_06]) ).
cnf(t50,plain,
$false,
inference(connection,[status(thm),parent(t49:1)],[t49:1,t47:2]) ).
cnf(t51,plain,
( ~ le(max(U_174,s(max(U_167,max(U_164,max(U_161,max(U_158,max(U_155,max(U_152,s(U_123))))))))),max(max(U_194,s(s(max(U_167,max(U_164,max(U_161,max(U_158,max(U_155,max(U_152,s(U_123)))))))))),max(U_180,max(U_177,max(U_174,s(max(U_167,max(U_164,max(U_161,max(U_158,max(U_155,max(U_152,s(U_123)))))))))))))
| le(s(max(U_167,max(U_164,max(U_161,max(U_158,max(U_155,max(U_152,s(U_123)))))))),max(max(U_194,s(s(max(U_167,max(U_164,max(U_161,max(U_158,max(U_155,max(U_152,s(U_123)))))))))),max(U_180,max(U_177,max(U_174,s(max(U_167,max(U_164,max(U_161,max(U_158,max(U_155,max(U_152,s(U_123))))))))))))) ),
inference(extension,[status(thm),parent(t49:2)],[sos_03]) ).
cnf(t52,plain,
$false,
inference(connection,[status(thm),parent(t51:1)],[t51:1,t49:2]) ).
cnf(t53,plain,
( ~ le(max(U_177,max(U_174,s(max(U_167,max(U_164,max(U_161,max(U_158,max(U_155,max(U_152,s(U_123)))))))))),max(max(U_194,s(s(max(U_167,max(U_164,max(U_161,max(U_158,max(U_155,max(U_152,s(U_123)))))))))),max(U_180,max(U_177,max(U_174,s(max(U_167,max(U_164,max(U_161,max(U_158,max(U_155,max(U_152,s(U_123)))))))))))))
| le(max(U_174,s(max(U_167,max(U_164,max(U_161,max(U_158,max(U_155,max(U_152,s(U_123))))))))),max(max(U_194,s(s(max(U_167,max(U_164,max(U_161,max(U_158,max(U_155,max(U_152,s(U_123)))))))))),max(U_180,max(U_177,max(U_174,s(max(U_167,max(U_164,max(U_161,max(U_158,max(U_155,max(U_152,s(U_123))))))))))))) ),
inference(extension,[status(thm),parent(t51:2)],[sos_03]) ).
cnf(t54,plain,
$false,
inference(connection,[status(thm),parent(t53:1)],[t53:1,t51:2]) ).
cnf(t55,plain,
( ~ le(max(U_180,max(U_177,max(U_174,s(max(U_167,max(U_164,max(U_161,max(U_158,max(U_155,max(U_152,s(U_123))))))))))),max(max(U_194,s(s(max(U_167,max(U_164,max(U_161,max(U_158,max(U_155,max(U_152,s(U_123)))))))))),max(U_180,max(U_177,max(U_174,s(max(U_167,max(U_164,max(U_161,max(U_158,max(U_155,max(U_152,s(U_123)))))))))))))
| le(max(U_177,max(U_174,s(max(U_167,max(U_164,max(U_161,max(U_158,max(U_155,max(U_152,s(U_123)))))))))),max(max(U_194,s(s(max(U_167,max(U_164,max(U_161,max(U_158,max(U_155,max(U_152,s(U_123)))))))))),max(U_180,max(U_177,max(U_174,s(max(U_167,max(U_164,max(U_161,max(U_158,max(U_155,max(U_152,s(U_123))))))))))))) ),
inference(extension,[status(thm),parent(t53:2)],[sos_03]) ).
cnf(t56,plain,
$false,
inference(connection,[status(thm),parent(t55:1)],[t55:1,t53:2]) ).
cnf(t57,plain,
( ~ le(max(max(U_194,s(s(max(U_167,max(U_164,max(U_161,max(U_158,max(U_155,max(U_152,s(U_123)))))))))),max(U_180,max(U_177,max(U_174,s(max(U_167,max(U_164,max(U_161,max(U_158,max(U_155,max(U_152,s(U_123)))))))))))),max(max(U_194,s(s(max(U_167,max(U_164,max(U_161,max(U_158,max(U_155,max(U_152,s(U_123)))))))))),max(U_180,max(U_177,max(U_174,s(max(U_167,max(U_164,max(U_161,max(U_158,max(U_155,max(U_152,s(U_123)))))))))))))
| le(max(U_180,max(U_177,max(U_174,s(max(U_167,max(U_164,max(U_161,max(U_158,max(U_155,max(U_152,s(U_123))))))))))),max(max(U_194,s(s(max(U_167,max(U_164,max(U_161,max(U_158,max(U_155,max(U_152,s(U_123)))))))))),max(U_180,max(U_177,max(U_174,s(max(U_167,max(U_164,max(U_161,max(U_158,max(U_155,max(U_152,s(U_123))))))))))))) ),
inference(extension,[status(thm),parent(t55:2)],[sos_03]) ).
cnf(t58,plain,
$false,
inference(connection,[status(thm),parent(t57:1)],[t57:1,t55:2]) ).
cnf(t59,plain,
le(max(max(U_194,s(s(max(U_167,max(U_164,max(U_161,max(U_158,max(U_155,max(U_152,s(U_123)))))))))),max(U_180,max(U_177,max(U_174,s(max(U_167,max(U_164,max(U_161,max(U_158,max(U_155,max(U_152,s(U_123)))))))))))),max(max(U_194,s(s(max(U_167,max(U_164,max(U_161,max(U_158,max(U_155,max(U_152,s(U_123)))))))))),max(U_180,max(U_177,max(U_174,s(max(U_167,max(U_164,max(U_161,max(U_158,max(U_155,max(U_152,s(U_123))))))))))))),
inference(extension,[status(thm),parent(t57:2)],[sos_01]) ).
cnf(t60,plain,
$false,
inference(connection,[status(thm),parent(t59:1)],[t59:1,t57:2]) ).
cnf(t61,plain,
( eq(f(max(max(U_194,s(s(max(U_167,max(U_164,max(U_161,max(U_158,max(U_155,max(U_152,s(U_123)))))))))),max(U_180,max(U_177,max(U_174,s(max(U_167,max(U_164,max(U_161,max(U_158,max(U_155,max(U_152,s(U_123))))))))))))),a0)
| eq(f(max(max(U_194,s(s(max(U_167,max(U_164,max(U_161,max(U_158,max(U_155,max(U_152,s(U_123)))))))))),max(U_180,max(U_177,max(U_174,s(max(U_167,max(U_164,max(U_161,max(U_158,max(U_155,max(U_152,s(U_123))))))))))))),a1) ),
inference(extension,[status(thm),parent(t49:3)],[sos_04]) ).
cnf(t62,plain,
$false,
inference(connection,[status(thm),parent(t61:1)],[t61:1,t49:3]) ).
cnf(t63,plain,
( ~ le(s(s(max(U_167,max(U_164,max(U_161,max(U_158,max(U_155,max(U_152,s(U_123))))))))),max(max(U_194,s(s(max(U_167,max(U_164,max(U_161,max(U_158,max(U_155,max(U_152,s(U_123)))))))))),max(U_180,max(U_177,max(U_174,s(max(U_167,max(U_164,max(U_161,max(U_158,max(U_155,max(U_152,s(U_123)))))))))))))
| ~ eq(f(s(max(U_167,max(U_164,max(U_161,max(U_158,max(U_155,max(U_152,s(U_123))))))))),a0)
| ~ eq(f(max(max(U_194,s(s(max(U_167,max(U_164,max(U_161,max(U_158,max(U_155,max(U_152,s(U_123)))))))))),max(U_180,max(U_177,max(U_174,s(max(U_167,max(U_164,max(U_161,max(U_158,max(U_155,max(U_152,s(U_123))))))))))))),a0) ),
inference(extension,[status(thm),parent(t61:2)],[sos_05]) ).
cnf(t64,plain,
$false,
inference(connection,[status(thm),parent(t63:1)],[t63:1,t61:2]) ).
cnf(t65,plain,
( eq(f(s(max(U_167,max(U_164,max(U_161,max(U_158,max(U_155,max(U_152,s(U_123))))))))),a1)
| eq(f(s(max(U_167,max(U_164,max(U_161,max(U_158,max(U_155,max(U_152,s(U_123))))))))),a0) ),
inference(extension,[status(thm),parent(t63:2)],[sos_04]) ).
cnf(t66,plain,
$false,
inference(connection,[status(thm),parent(t65:1)],[t65:1,t63:2]) ).
cnf(t67,plain,
( ~ le(s(max(U_167,max(U_164,max(U_161,max(U_158,max(U_155,max(U_152,s(U_123)))))))),s(max(U_167,max(U_164,max(U_161,max(U_158,max(U_155,max(U_152,s(U_123)))))))))
| ~ eq(f(max(U_167,max(U_164,max(U_161,max(U_158,max(U_155,max(U_152,s(U_123)))))))),a1)
| ~ eq(f(s(max(U_167,max(U_164,max(U_161,max(U_158,max(U_155,max(U_152,s(U_123))))))))),a1) ),
inference(extension,[status(thm),parent(t65:2)],[sos_06]) ).
cnf(t68,plain,
$false,
inference(connection,[status(thm),parent(t67:1)],[t67:1,t65:2]) ).
cnf(t69,plain,
$false,
inference(reduction,[status(thm),parent(t67:2)],[t67:2,t47:2]) ).
cnf(t70,plain,
le(s(max(U_167,max(U_164,max(U_161,max(U_158,max(U_155,max(U_152,s(U_123)))))))),s(max(U_167,max(U_164,max(U_161,max(U_158,max(U_155,max(U_152,s(U_123))))))))),
inference(extension,[status(thm),parent(t67:3)],[sos_01]) ).
cnf(t71,plain,
$false,
inference(connection,[status(thm),parent(t70:1)],[t70:1,t67:3]) ).
cnf(t72,plain,
( ~ le(max(U_194,s(s(max(U_167,max(U_164,max(U_161,max(U_158,max(U_155,max(U_152,s(U_123)))))))))),max(max(U_194,s(s(max(U_167,max(U_164,max(U_161,max(U_158,max(U_155,max(U_152,s(U_123)))))))))),max(U_180,max(U_177,max(U_174,s(max(U_167,max(U_164,max(U_161,max(U_158,max(U_155,max(U_152,s(U_123)))))))))))))
| le(s(s(max(U_167,max(U_164,max(U_161,max(U_158,max(U_155,max(U_152,s(U_123))))))))),max(max(U_194,s(s(max(U_167,max(U_164,max(U_161,max(U_158,max(U_155,max(U_152,s(U_123)))))))))),max(U_180,max(U_177,max(U_174,s(max(U_167,max(U_164,max(U_161,max(U_158,max(U_155,max(U_152,s(U_123))))))))))))) ),
inference(extension,[status(thm),parent(t63:3)],[sos_03]) ).
cnf(t73,plain,
$false,
inference(connection,[status(thm),parent(t72:1)],[t72:1,t63:3]) ).
cnf(t74,plain,
( ~ le(max(max(U_194,s(s(max(U_167,max(U_164,max(U_161,max(U_158,max(U_155,max(U_152,s(U_123)))))))))),max(U_180,max(U_177,max(U_174,s(max(U_167,max(U_164,max(U_161,max(U_158,max(U_155,max(U_152,s(U_123)))))))))))),max(max(U_194,s(s(max(U_167,max(U_164,max(U_161,max(U_158,max(U_155,max(U_152,s(U_123)))))))))),max(U_180,max(U_177,max(U_174,s(max(U_167,max(U_164,max(U_161,max(U_158,max(U_155,max(U_152,s(U_123)))))))))))))
| le(max(U_194,s(s(max(U_167,max(U_164,max(U_161,max(U_158,max(U_155,max(U_152,s(U_123)))))))))),max(max(U_194,s(s(max(U_167,max(U_164,max(U_161,max(U_158,max(U_155,max(U_152,s(U_123)))))))))),max(U_180,max(U_177,max(U_174,s(max(U_167,max(U_164,max(U_161,max(U_158,max(U_155,max(U_152,s(U_123))))))))))))) ),
inference(extension,[status(thm),parent(t72:2)],[sos_02]) ).
cnf(t75,plain,
$false,
inference(connection,[status(thm),parent(t74:1)],[t74:1,t72:2]) ).
cnf(t76,plain,
le(max(max(U_194,s(s(max(U_167,max(U_164,max(U_161,max(U_158,max(U_155,max(U_152,s(U_123)))))))))),max(U_180,max(U_177,max(U_174,s(max(U_167,max(U_164,max(U_161,max(U_158,max(U_155,max(U_152,s(U_123)))))))))))),max(max(U_194,s(s(max(U_167,max(U_164,max(U_161,max(U_158,max(U_155,max(U_152,s(U_123)))))))))),max(U_180,max(U_177,max(U_174,s(max(U_167,max(U_164,max(U_161,max(U_158,max(U_155,max(U_152,s(U_123))))))))))))),
inference(extension,[status(thm),parent(t74:2)],[sos_01]) ).
cnf(t77,plain,
$false,
inference(connection,[status(thm),parent(t76:1)],[t76:1,t74:2]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SYO614-1 : TPTP v9.3.1. Released v7.1.0.
% 0.00/0.02 This is a CNF_UNS_RFO_NEQ_NHN problem
% 0.00/0.03 % Command : /export/starexec/sandbox/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/10.58 % Computer : n002.cluster.edu
% 0.10/10.58 % Model : x86_64 x86_64
% 0.10/10.58 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/10.58 % Memory : 8046.5625MB
% 0.10/10.58 % OS : Linux 6.8.0-71-generic
% 0.10/10.58 % CPULimit : 300
% 0.10/10.58 % WCLimit : 300
% 0.10/10.58 % DateTime : Sun Sep 20 07:45:12 UTC 2026
% 0.10/10.59 % CPUTime :
% 0.84/11.32 % SZS status Unsatisfiable for theBenchmark
% 0.84/11.32 % SZS output start Proof for theBenchmark
% See solution above
%------------------------------------------------------------------------------