%------------------------------------------------------------------------------
% File : ConnectPP---0.7.2
% Problem : MED003+1 : TPTP v9.3.1. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox2/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n020.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 08:50:29 AM UTC 2026
% Result : Theorem 33.46s 33.75s
% Output : Proof 33.46s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 3
% Syntax : Number of formulae : 84 ( 34 unt; 0 def)
% Number of atoms : 269 ( 0 equ)
% Maximal formula atoms : 19 ( 3 avg)
% Number of connectives : 313 ( 128 ~; 110 |; 60 &)
% ( 0 <=>; 15 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 3 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 14 ( 13 usr; 1 prp; 0-2 aty)
% Number of functors : 6 ( 6 usr; 2 con; 0-1 aty)
% Number of variables : 81 ( 0 sgn 52 !; 13 ?)
% Comments :
%------------------------------------------------------------------------------
fof(insulin_effect,axiom,
! [X0] :
( ! [X1] :
( ~ gt(X0,X1)
=> drugi(X1) )
=> ! [X1] :
( ~ gt(X0,X1)
=> ( uptakepg(X1)
& uptakelg(X1) ) ) ),
file('MED001+0.ax',insulin_effect) ).
fof(ex_cure,axiom,
! [X0] :
( ( ! [X1] :
( gt(X0,X1)
=> conditionhyper(X1) )
& bcapacityex(X0)
& ! [X1] :
( ~ gt(X0,X1)
=> uptakepg(X1) )
& ! [X1] :
( ~ gt(X0,X1)
=> uptakelg(X1) ) )
=> ! [X1] :
( ~ gt(X0,X1)
=> ( conditionhypo(X1)
| conditionnormo(X1) ) ) ),
file('MED001+0.ax',ex_cure) ).
fof(treatmentex,conjecture,
( ( bcapacityex(n0)
& ! [X0] :
( gt(n0,X0)
=> conditionhyper(X0) )
& ! [X0] :
( ~ gt(n0,X0)
=> drugi(X0) ) )
=> ! [X0] :
( ~ gt(n0,X0)
=> ( conditionhypo(X0)
| conditionnormo(X0) ) ) ),
file('theBenchmark.p',treatmentex) ).
fof(f_11_1,plain,
! [X0] :
( ! [X1] :
( ( uptakepg(X1)
& uptakelg(X1) )
| gt(X0,X1) )
| ? [X1] :
( ~ drugi(X1)
& ~ gt(X0,X1) ) ),
inference(fof_nnf,[status(thm)],[insulin_effect]) ).
fof(f_11_2,plain,
! [U_14] :
( ! [U_13] :
( ( uptakepg(U_13)
& uptakelg(U_13) )
| gt(U_14,U_13) )
| ? [U_12] :
( ~ drugi(U_12)
& ~ gt(U_14,U_12) ) ),
inference(variable_rename,[status(thm)],[f_11_1]) ).
fof(f_11_3,plain,
! [U_14] :
( ! [U_13] :
( ( uptakepg(U_13)
& uptakelg(U_13) )
| gt(U_14,U_13) )
| ( ~ drugi(sK1(U_14))
& ~ gt(U_14,sK1(U_14)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1]),skolemize(U_12,sK1(U_14))],[f_11_2]) ).
fof(f_11_4,plain,
( ! [U_13] :
( uptakepg(U_13)
| ~ sP1(U_13) )
& ! [U_13] :
( uptakelg(U_13)
| ~ sP1(U_13) )
& ! [U_14] :
( ~ drugi(sK1(U_14))
| ~ sP0(U_14) )
& ! [U_14] :
( ~ gt(U_14,sK1(U_14))
| ~ sP0(U_14) )
& ! [U_13,U_14] :
( sP1(U_13)
| gt(U_14,U_13)
| sP0(U_14) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP0,sP1])],[f_11_3]) ).
cnf(f_11_5,plain,
( sP1(U_13)
| gt(U_14,U_13)
| sP0(U_14) ),
inference(clausify,[status(thm)],[f_11_4]) ).
cnf(f_11_6,plain,
( ~ gt(U_14,sK1(U_14))
| ~ sP0(U_14) ),
inference(clausify,[status(thm)],[f_11_4]) ).
cnf(f_11_7,plain,
( ~ drugi(sK1(U_14))
| ~ sP0(U_14) ),
inference(clausify,[status(thm)],[f_11_4]) ).
cnf(f_11_8,plain,
( uptakelg(U_13)
| ~ sP1(U_13) ),
inference(clausify,[status(thm)],[f_11_4]) ).
cnf(f_11_9,plain,
( uptakepg(U_13)
| ~ sP1(U_13) ),
inference(clausify,[status(thm)],[f_11_4]) ).
fof(f_18_1,plain,
! [X0] :
( ! [X1] :
( conditionhypo(X1)
| conditionnormo(X1)
| gt(X0,X1) )
| ? [X1] :
( ~ conditionhyper(X1)
& gt(X0,X1) )
| ~ bcapacityex(X0)
| ? [X1] :
( ~ uptakepg(X1)
& ~ gt(X0,X1) )
| ? [X1] :
( ~ uptakelg(X1)
& ~ gt(X0,X1) ) ),
inference(fof_nnf,[status(thm)],[ex_cure]) ).
fof(f_18_2,plain,
! [U_41] :
( ! [U_40] :
( conditionhypo(U_40)
| conditionnormo(U_40)
| gt(U_41,U_40) )
| ? [U_39] :
( ~ conditionhyper(U_39)
& gt(U_41,U_39) )
| ~ bcapacityex(U_41)
| ? [U_38] :
( ~ uptakepg(U_38)
& ~ gt(U_41,U_38) )
| ? [U_37] :
( ~ uptakelg(U_37)
& ~ gt(U_41,U_37) ) ),
inference(variable_rename,[status(thm)],[f_18_1]) ).
fof(f_18_3,plain,
! [U_41] :
( ! [U_40] :
( conditionhypo(U_40)
| conditionnormo(U_40)
| gt(U_41,U_40) )
| ? [U_39] :
( ~ conditionhyper(U_39)
& gt(U_41,U_39) )
| ~ bcapacityex(U_41)
| ? [U_38] :
( ~ uptakepg(U_38)
& ~ gt(U_41,U_38) )
| ( ~ uptakelg(sK12(U_41))
& ~ gt(U_41,sK12(U_41)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK12]),skolemize(U_37,sK12(U_41))],[f_18_2]) ).
fof(f_18_4,plain,
! [U_41] :
( ! [U_40] :
( conditionhypo(U_40)
| conditionnormo(U_40)
| gt(U_41,U_40) )
| ? [U_39] :
( ~ conditionhyper(U_39)
& gt(U_41,U_39) )
| ~ bcapacityex(U_41)
| ( ~ uptakepg(sK13(U_41))
& ~ gt(U_41,sK13(U_41)) )
| ( ~ uptakelg(sK12(U_41))
& ~ gt(U_41,sK12(U_41)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK13]),skolemize(U_38,sK13(U_41))],[f_18_3]) ).
fof(f_18_5,plain,
! [U_41] :
( ! [U_40] :
( conditionhypo(U_40)
| conditionnormo(U_40)
| gt(U_41,U_40) )
| ( ~ conditionhyper(sK14(U_41))
& gt(U_41,sK14(U_41)) )
| ~ bcapacityex(U_41)
| ( ~ uptakepg(sK13(U_41))
& ~ gt(U_41,sK13(U_41)) )
| ( ~ uptakelg(sK12(U_41))
& ~ gt(U_41,sK12(U_41)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK14]),skolemize(U_39,sK14(U_41))],[f_18_4]) ).
fof(f_18_6,plain,
( ! [U_41] :
( ~ conditionhyper(sK14(U_41))
| ~ sP13(U_41) )
& ! [U_41] :
( gt(U_41,sK14(U_41))
| ~ sP13(U_41) )
& ! [U_41] :
( ~ uptakepg(sK13(U_41))
| ~ sP12(U_41) )
& ! [U_41] :
( ~ gt(U_41,sK13(U_41))
| ~ sP12(U_41) )
& ! [U_41] :
( ~ uptakelg(sK12(U_41))
| ~ sP11(U_41) )
& ! [U_41] :
( ~ gt(U_41,sK12(U_41))
| ~ sP11(U_41) )
& ! [U_41,U_40] :
( conditionhypo(U_40)
| conditionnormo(U_40)
| gt(U_41,U_40)
| sP13(U_41)
| ~ bcapacityex(U_41)
| sP12(U_41)
| sP11(U_41) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP11,sP12,sP13])],[f_18_5]) ).
cnf(f_18_7,plain,
( conditionhypo(U_40)
| conditionnormo(U_40)
| gt(U_41,U_40)
| sP13(U_41)
| ~ bcapacityex(U_41)
| sP12(U_41)
| sP11(U_41) ),
inference(clausify,[status(thm)],[f_18_6]) ).
cnf(f_18_8,plain,
( ~ gt(U_41,sK12(U_41))
| ~ sP11(U_41) ),
inference(clausify,[status(thm)],[f_18_6]) ).
cnf(f_18_9,plain,
( ~ uptakelg(sK12(U_41))
| ~ sP11(U_41) ),
inference(clausify,[status(thm)],[f_18_6]) ).
cnf(f_18_10,plain,
( ~ gt(U_41,sK13(U_41))
| ~ sP12(U_41) ),
inference(clausify,[status(thm)],[f_18_6]) ).
cnf(f_18_11,plain,
( ~ uptakepg(sK13(U_41))
| ~ sP12(U_41) ),
inference(clausify,[status(thm)],[f_18_6]) ).
cnf(f_18_12,plain,
( gt(U_41,sK14(U_41))
| ~ sP13(U_41) ),
inference(clausify,[status(thm)],[f_18_6]) ).
cnf(f_18_13,plain,
( ~ conditionhyper(sK14(U_41))
| ~ sP13(U_41) ),
inference(clausify,[status(thm)],[f_18_6]) ).
fof(f_19_1,negated_conjecture,
( ~ ! [X0] :
( ~ gt(n0,X0)
=> ( conditionhypo(X0)
| conditionnormo(X0) ) )
& bcapacityex(n0)
& ! [X0] :
( gt(n0,X0)
=> conditionhyper(X0) )
& ! [X0] :
( ~ gt(n0,X0)
=> drugi(X0) ) ),
inference(negate,[status(cth)],[treatmentex]) ).
fof(f_19_2,negated_conjecture,
( ? [X0] :
( ~ conditionhypo(X0)
& ~ conditionnormo(X0)
& ~ gt(n0,X0) )
& bcapacityex(n0)
& ! [X0] :
( conditionhyper(X0)
| ~ gt(n0,X0) )
& ! [X0] :
( drugi(X0)
| gt(n0,X0) ) ),
inference(fof_nnf,[status(thm)],[f_19_1]) ).
fof(f_19_3,negated_conjecture,
( ? [U_44] :
( ~ conditionhypo(U_44)
& ~ conditionnormo(U_44)
& ~ gt(n0,U_44) )
& bcapacityex(n0)
& ! [U_43] :
( conditionhyper(U_43)
| ~ gt(n0,U_43) )
& ! [U_42] :
( drugi(U_42)
| gt(n0,U_42) ) ),
inference(variable_rename,[status(thm)],[f_19_2]) ).
fof(f_19_4,negated_conjecture,
( ~ conditionhypo(sK15)
& ~ conditionnormo(sK15)
& ~ gt(n0,sK15)
& bcapacityex(n0)
& ! [U_43] :
( conditionhyper(U_43)
| ~ gt(n0,U_43) )
& ! [U_42] :
( drugi(U_42)
| gt(n0,U_42) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK15]),skolemize(U_44,sK15)],[f_19_3]) ).
fof(f_19_5,negated_conjecture,
( ~ conditionhypo(sK15)
& ~ conditionnormo(sK15)
& ~ gt(n0,sK15)
& bcapacityex(n0)
& ! [U_43] :
( conditionhyper(U_43)
| ~ gt(n0,U_43) )
& ! [U_42] :
( drugi(U_42)
| gt(n0,U_42) ) ),
inference(definitional_conversion,[status(esa)],[f_19_4]) ).
cnf(f_19_6,negated_conjecture,
( drugi(U_42)
| gt(n0,U_42) ),
inference(clausify,[status(thm)],[f_19_5]) ).
cnf(f_19_7,negated_conjecture,
( conditionhyper(U_43)
| ~ gt(n0,U_43) ),
inference(clausify,[status(thm)],[f_19_5]) ).
cnf(f_19_8,negated_conjecture,
bcapacityex(n0),
inference(clausify,[status(thm)],[f_19_5]) ).
cnf(f_19_9,negated_conjecture,
~ gt(n0,sK15),
inference(clausify,[status(thm)],[f_19_5]) ).
cnf(f_19_10,negated_conjecture,
~ conditionnormo(sK15),
inference(clausify,[status(thm)],[f_19_5]) ).
cnf(f_19_11,negated_conjecture,
~ conditionhypo(sK15),
inference(clausify,[status(thm)],[f_19_5]) ).
cnf(t1,plain,
bcapacityex(n0),
inference(start,[status(thm),parent(0:0)],[f_19_8]) ).
cnf(t2,plain,
( sP12(n0)
| conditionhypo(sK15)
| sP13(n0)
| gt(n0,sK15)
| conditionnormo(sK15)
| sP11(n0)
| ~ bcapacityex(n0) ),
inference(extension,[status(thm),parent(t1:1)],[f_18_7]) ).
cnf(t3,plain,
$false,
inference(connection,[status(thm),parent(t2:1)],[t2:1,t1:1]) ).
cnf(t4,plain,
( ~ gt(n0,sK12(n0))
| ~ sP11(n0) ),
inference(extension,[status(thm),parent(t2:2)],[f_18_8]) ).
cnf(t5,plain,
$false,
inference(connection,[status(thm),parent(t4:1)],[t4:1,t2:2]) ).
cnf(t6,plain,
( sP1(sK12(n0))
| sP0(n0)
| gt(n0,sK12(n0)) ),
inference(extension,[status(thm),parent(t4:2)],[f_11_5]) ).
cnf(t7,plain,
$false,
inference(connection,[status(thm),parent(t6:1)],[t6:1,t4:2]) ).
cnf(t8,plain,
( ~ drugi(sK1(n0))
| ~ sP0(n0) ),
inference(extension,[status(thm),parent(t6:2)],[f_11_7]) ).
cnf(t9,plain,
$false,
inference(connection,[status(thm),parent(t8:1)],[t8:1,t6:2]) ).
cnf(t10,plain,
( gt(n0,sK1(n0))
| drugi(sK1(n0)) ),
inference(extension,[status(thm),parent(t8:2)],[f_19_6]) ).
cnf(t11,plain,
$false,
inference(connection,[status(thm),parent(t10:1)],[t10:1,t8:2]) ).
cnf(t12,plain,
( ~ sP0(n0)
| ~ gt(n0,sK1(n0)) ),
inference(extension,[status(thm),parent(t10:2)],[f_11_6]) ).
cnf(t13,plain,
$false,
inference(connection,[status(thm),parent(t12:1)],[t12:1,t10:2]) ).
cnf(t14,plain,
$false,
inference(reduction,[status(thm),parent(t12:2)],[t12:2,t6:2]) ).
cnf(t15,plain,
( uptakelg(sK12(n0))
| ~ sP1(sK12(n0)) ),
inference(extension,[status(thm),parent(t6:3)],[f_11_8]) ).
cnf(t16,plain,
$false,
inference(connection,[status(thm),parent(t15:1)],[t15:1,t6:3]) ).
cnf(t17,plain,
( ~ sP11(n0)
| ~ uptakelg(sK12(n0)) ),
inference(extension,[status(thm),parent(t15:2)],[f_18_9]) ).
cnf(t18,plain,
$false,
inference(connection,[status(thm),parent(t17:1)],[t17:1,t15:2]) ).
cnf(t19,plain,
$false,
inference(reduction,[status(thm),parent(t17:2)],[t17:2,t2:2]) ).
cnf(t20,plain,
~ conditionnormo(sK15),
inference(extension,[status(thm),parent(t2:3)],[f_19_10]) ).
cnf(t21,plain,
$false,
inference(connection,[status(thm),parent(t20:1)],[t20:1,t2:3]) ).
cnf(t22,plain,
~ gt(n0,sK15),
inference(extension,[status(thm),parent(t2:4)],[f_19_9]) ).
cnf(t23,plain,
$false,
inference(connection,[status(thm),parent(t22:1)],[t22:1,t2:4]) ).
cnf(t24,plain,
( ~ conditionhyper(sK14(n0))
| ~ sP13(n0) ),
inference(extension,[status(thm),parent(t2:5)],[f_18_13]) ).
cnf(t25,plain,
$false,
inference(connection,[status(thm),parent(t24:1)],[t24:1,t2:5]) ).
cnf(t26,plain,
( ~ gt(n0,sK14(n0))
| conditionhyper(sK14(n0)) ),
inference(extension,[status(thm),parent(t24:2)],[f_19_7]) ).
cnf(t27,plain,
$false,
inference(connection,[status(thm),parent(t26:1)],[t26:1,t24:2]) ).
cnf(t28,plain,
( ~ sP13(n0)
| gt(n0,sK14(n0)) ),
inference(extension,[status(thm),parent(t26:2)],[f_18_12]) ).
cnf(t29,plain,
$false,
inference(connection,[status(thm),parent(t28:1)],[t28:1,t26:2]) ).
cnf(t30,plain,
$false,
inference(reduction,[status(thm),parent(t28:2)],[t28:2,t2:5]) ).
cnf(t31,plain,
~ conditionhypo(sK15),
inference(extension,[status(thm),parent(t2:6)],[f_19_11]) ).
cnf(t32,plain,
$false,
inference(connection,[status(thm),parent(t31:1)],[t31:1,t2:6]) ).
cnf(t33,plain,
( ~ gt(n0,sK13(n0))
| ~ sP12(n0) ),
inference(extension,[status(thm),parent(t2:7)],[f_18_10]) ).
cnf(t34,plain,
$false,
inference(connection,[status(thm),parent(t33:1)],[t33:1,t2:7]) ).
cnf(t35,plain,
( sP1(sK13(n0))
| sP0(n0)
| gt(n0,sK13(n0)) ),
inference(extension,[status(thm),parent(t33:2)],[f_11_5]) ).
cnf(t36,plain,
$false,
inference(connection,[status(thm),parent(t35:1)],[t35:1,t33:2]) ).
cnf(t37,plain,
( ~ drugi(sK1(n0))
| ~ sP0(n0) ),
inference(extension,[status(thm),parent(t35:2)],[f_11_7]) ).
cnf(t38,plain,
$false,
inference(connection,[status(thm),parent(t37:1)],[t37:1,t35:2]) ).
cnf(t39,plain,
( gt(n0,sK1(n0))
| drugi(sK1(n0)) ),
inference(extension,[status(thm),parent(t37:2)],[f_19_6]) ).
cnf(t40,plain,
$false,
inference(connection,[status(thm),parent(t39:1)],[t39:1,t37:2]) ).
cnf(t41,plain,
( ~ sP0(n0)
| ~ gt(n0,sK1(n0)) ),
inference(extension,[status(thm),parent(t39:2)],[f_11_6]) ).
cnf(t42,plain,
$false,
inference(connection,[status(thm),parent(t41:1)],[t41:1,t39:2]) ).
cnf(t43,plain,
$false,
inference(reduction,[status(thm),parent(t41:2)],[t41:2,t35:2]) ).
cnf(t44,plain,
( uptakepg(sK13(n0))
| ~ sP1(sK13(n0)) ),
inference(extension,[status(thm),parent(t35:3)],[f_11_9]) ).
cnf(t45,plain,
$false,
inference(connection,[status(thm),parent(t44:1)],[t44:1,t35:3]) ).
cnf(t46,plain,
( ~ sP12(n0)
| ~ uptakepg(sK13(n0)) ),
inference(extension,[status(thm),parent(t44:2)],[f_18_11]) ).
cnf(t47,plain,
$false,
inference(connection,[status(thm),parent(t46:1)],[t46:1,t44:2]) ).
cnf(t48,plain,
$false,
inference(reduction,[status(thm),parent(t46:2)],[t46:2,t2:7]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MED003+1 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.03 This is a FOF_THM_RFO_NEQ problem
% 0.00/0.04 % Command : /export/starexec/sandbox2/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.35 % Computer : n020.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Sat Sep 19 16:10:01 UTC 2026
% 0.09/0.35 % CPUTime :
% 33.46/33.75 % SZS status Theorem for theBenchmark
% 33.46/33.75 % SZS output start Proof for theBenchmark
% See solution above
%------------------------------------------------------------------------------