%------------------------------------------------------------------------------
% File : ConnectPP---0.7.2
% Problem : NUM492+3 : TPTP v9.3.1. Released v4.0.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 : n018.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:52:24 AM UTC 2026
% Result : Theorem 243.15s 243.47s
% Output : Proof 243.15s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 10
% Syntax : Number of formulae : 71 ( 34 unt; 0 def)
% Number of atoms : 225 ( 64 equ)
% Maximal formula atoms : 15 ( 3 avg)
% Number of connectives : 237 ( 83 ~; 68 |; 82 &)
% ( 0 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 14 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 6 ( 4 usr; 1 prp; 0-2 aty)
% Number of functors : 12 ( 12 usr; 9 con; 0-2 aty)
% Number of variables : 59 ( 0 sgn 36 !; 13 ?)
% Comments :
%------------------------------------------------------------------------------
fof(mSortsB_02,axiom,
! [W0,W1] :
( ( aNaturalNumber0(W1)
& aNaturalNumber0(W0) )
=> aNaturalNumber0(sdtasdt0(W0,W1)) ),
file('theBenchmark.p',mSortsB_02) ).
fof(mDivMin,axiom,
! [W0,W1,W2] :
( ( aNaturalNumber0(W2)
& aNaturalNumber0(W1)
& aNaturalNumber0(W0) )
=> ( ( doDivides0(W0,sdtpldt0(W1,W2))
& doDivides0(W0,W1) )
=> doDivides0(W0,W2) ) ),
file('theBenchmark.p',mDivMin) ).
fof(m__1837,hypothesis,
( aNaturalNumber0(xp)
& aNaturalNumber0(xm)
& aNaturalNumber0(xn) ),
file('theBenchmark.p',m__1837) ).
fof(m__1860,hypothesis,
( doDivides0(xp,sdtasdt0(xn,xm))
& ? [W0] :
( sdtasdt0(xn,xm) = sdtasdt0(xp,W0)
& aNaturalNumber0(W0) )
& isPrime0(xp)
& ! [W0] :
( ( ( doDivides0(W0,xp)
| ? [W1] :
( xp = sdtasdt0(W0,W1)
& aNaturalNumber0(W1) ) )
& aNaturalNumber0(W0) )
=> ( W0 = xp
| W0 = sz10 ) )
& xp != sz10
& xp != sz00 ),
file('theBenchmark.p',m__1860) ).
fof(m__1883,hypothesis,
( xr = sdtmndt0(xn,xp)
& sdtpldt0(xp,xr) = xn
& aNaturalNumber0(xr) ),
file('theBenchmark.p',m__1883) ).
fof(m__1951,hypothesis,
sdtasdt0(xn,xm) = sdtpldt0(sdtasdt0(xp,xm),sdtasdt0(xr,xm)),
file('theBenchmark.p',m__1951) ).
fof(m__2001,hypothesis,
( doDivides0(xp,sdtasdt0(xp,xm))
& ? [W0] :
( sdtasdt0(xp,xm) = sdtasdt0(xp,W0)
& aNaturalNumber0(W0) )
& ? [W0] :
( sdtasdt0(xn,xm) = sdtasdt0(xp,W0)
& aNaturalNumber0(W0) ) ),
file('theBenchmark.p',m__2001) ).
fof(m__,conjecture,
( doDivides0(xp,sdtasdt0(xr,xm))
| ? [W0] :
( sdtasdt0(xr,xm) = sdtasdt0(xp,W0)
& aNaturalNumber0(W0) ) ),
file('theBenchmark.p',m__) ).
fof(f_5_1,plain,
! [W0,W1] :
( aNaturalNumber0(sdtasdt0(W0,W1))
| ~ aNaturalNumber0(W1)
| ~ aNaturalNumber0(W0) ),
inference(fof_nnf,[status(thm)],[mSortsB_02]) ).
fof(f_5_2,plain,
! [U_4,U_3] :
( aNaturalNumber0(sdtasdt0(U_4,U_3))
| ~ aNaturalNumber0(U_3)
| ~ aNaturalNumber0(U_4) ),
inference(variable_rename,[status(thm)],[f_5_1]) ).
fof(f_5_3,plain,
! [U_3,U_4] :
( aNaturalNumber0(sdtasdt0(U_4,U_3))
| ~ aNaturalNumber0(U_3)
| ~ aNaturalNumber0(U_4) ),
inference(definitional_conversion,[status(esa)],[f_5_2]) ).
cnf(f_5_4,plain,
( aNaturalNumber0(sdtasdt0(U_4,U_3))
| ~ aNaturalNumber0(U_3)
| ~ aNaturalNumber0(U_4) ),
inference(clausify,[status(thm)],[f_5_3]) ).
fof(f_34_1,plain,
! [W0,W1,W2] :
( doDivides0(W0,W2)
| ~ doDivides0(W0,sdtpldt0(W1,W2))
| ~ doDivides0(W0,W1)
| ~ aNaturalNumber0(W2)
| ~ aNaturalNumber0(W1)
| ~ aNaturalNumber0(W0) ),
inference(fof_nnf,[status(thm)],[mDivMin]) ).
fof(f_34_2,plain,
! [U_78,U_77,U_76] :
( doDivides0(U_78,U_76)
| ~ doDivides0(U_78,sdtpldt0(U_77,U_76))
| ~ doDivides0(U_78,U_77)
| ~ aNaturalNumber0(U_76)
| ~ aNaturalNumber0(U_77)
| ~ aNaturalNumber0(U_78) ),
inference(variable_rename,[status(thm)],[f_34_1]) ).
fof(f_34_3,plain,
! [U_78,U_77,U_76] :
( doDivides0(U_78,U_76)
| ~ doDivides0(U_78,sdtpldt0(U_77,U_76))
| ~ doDivides0(U_78,U_77)
| ~ aNaturalNumber0(U_76)
| ~ aNaturalNumber0(U_77)
| ~ aNaturalNumber0(U_78) ),
inference(definitional_conversion,[status(esa)],[f_34_2]) ).
cnf(f_34_4,plain,
( doDivides0(U_78,U_76)
| ~ doDivides0(U_78,sdtpldt0(U_77,U_76))
| ~ doDivides0(U_78,U_77)
| ~ aNaturalNumber0(U_76)
| ~ aNaturalNumber0(U_77)
| ~ aNaturalNumber0(U_78) ),
inference(clausify,[status(thm)],[f_34_3]) ).
fof(f_39_1,plain,
( aNaturalNumber0(xp)
& aNaturalNumber0(xm)
& aNaturalNumber0(xn) ),
inference(fof_nnf,[status(thm)],[m__1837]) ).
fof(f_39_2,plain,
( aNaturalNumber0(xp)
& aNaturalNumber0(xm)
& aNaturalNumber0(xn) ),
inference(definitional_conversion,[status(esa)],[f_39_1]) ).
cnf(f_39_4,plain,
aNaturalNumber0(xm),
inference(clausify,[status(thm)],[f_39_2]) ).
cnf(f_39_5,plain,
aNaturalNumber0(xp),
inference(clausify,[status(thm)],[f_39_2]) ).
fof(f_41_1,plain,
( doDivides0(xp,sdtasdt0(xn,xm))
& ? [W0] :
( sdtasdt0(xn,xm) = sdtasdt0(xp,W0)
& aNaturalNumber0(W0) )
& isPrime0(xp)
& ! [W0] :
( W0 = xp
| W0 = sz10
| ( ~ doDivides0(W0,xp)
& ! [W1] :
( xp != sdtasdt0(W0,W1)
| ~ aNaturalNumber0(W1) ) )
| ~ aNaturalNumber0(W0) )
& xp != sz10
& xp != sz00 ),
inference(fof_nnf,[status(thm)],[m__1860]) ).
fof(f_41_2,plain,
( doDivides0(xp,sdtasdt0(xn,xm))
& ? [U_99] :
( sdtasdt0(xn,xm) = sdtasdt0(xp,U_99)
& aNaturalNumber0(U_99) )
& isPrime0(xp)
& ! [U_98] :
( U_98 = xp
| U_98 = sz10
| ( ~ doDivides0(U_98,xp)
& ! [U_97] :
( xp != sdtasdt0(U_98,U_97)
| ~ aNaturalNumber0(U_97) ) )
| ~ aNaturalNumber0(U_98) )
& xp != sz10
& xp != sz00 ),
inference(variable_rename,[status(thm)],[f_41_1]) ).
fof(f_41_3,plain,
( doDivides0(xp,sdtasdt0(xn,xm))
& sdtasdt0(xn,xm) = sdtasdt0(xp,sK9)
& aNaturalNumber0(sK9)
& isPrime0(xp)
& ! [U_98] :
( U_98 = xp
| U_98 = sz10
| ( ~ doDivides0(U_98,xp)
& ! [U_97] :
( xp != sdtasdt0(U_98,U_97)
| ~ aNaturalNumber0(U_97) ) )
| ~ aNaturalNumber0(U_98) )
& xp != sz10
& xp != sz00 ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK9]),skolemize(U_99,sK9)],[f_41_2]) ).
fof(f_41_4,plain,
( ! [U_97,U_98] :
( ~ doDivides0(U_98,xp)
| ~ sP28(U_97,U_98) )
& ! [U_97,U_98] :
( xp != sdtasdt0(U_98,U_97)
| ~ aNaturalNumber0(U_97)
| ~ sP28(U_97,U_98) )
& doDivides0(xp,sdtasdt0(xn,xm))
& sdtasdt0(xn,xm) = sdtasdt0(xp,sK9)
& aNaturalNumber0(sK9)
& isPrime0(xp)
& ! [U_97,U_98] :
( U_98 = xp
| U_98 = sz10
| sP28(U_97,U_98)
| ~ aNaturalNumber0(U_98) )
& xp != sz10
& xp != sz00 ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP28])],[f_41_3]) ).
cnf(f_41_11,plain,
doDivides0(xp,sdtasdt0(xn,xm)),
inference(clausify,[status(thm)],[f_41_4]) ).
fof(f_43_1,plain,
( xr = sdtmndt0(xn,xp)
& sdtpldt0(xp,xr) = xn
& aNaturalNumber0(xr) ),
inference(fof_nnf,[status(thm)],[m__1883]) ).
fof(f_43_2,plain,
( xr = sdtmndt0(xn,xp)
& sdtpldt0(xp,xr) = xn
& aNaturalNumber0(xr) ),
inference(definitional_conversion,[status(esa)],[f_43_1]) ).
cnf(f_43_3,plain,
aNaturalNumber0(xr),
inference(clausify,[status(thm)],[f_43_2]) ).
fof(f_46_1,plain,
sdtasdt0(xn,xm) = sdtpldt0(sdtasdt0(xp,xm),sdtasdt0(xr,xm)),
inference(fof_nnf,[status(thm)],[m__1951]) ).
fof(f_46_2,plain,
sdtasdt0(xn,xm) = sdtpldt0(sdtasdt0(xp,xm),sdtasdt0(xr,xm)),
inference(definitional_conversion,[status(esa)],[f_46_1]) ).
cnf(f_46_3,plain,
sdtasdt0(xn,xm) = sdtpldt0(sdtasdt0(xp,xm),sdtasdt0(xr,xm)),
inference(clausify,[status(thm)],[f_46_2]) ).
fof(f_48_1,plain,
( doDivides0(xp,sdtasdt0(xp,xm))
& ? [W0] :
( sdtasdt0(xp,xm) = sdtasdt0(xp,W0)
& aNaturalNumber0(W0) )
& ? [W0] :
( sdtasdt0(xn,xm) = sdtasdt0(xp,W0)
& aNaturalNumber0(W0) ) ),
inference(fof_nnf,[status(thm)],[m__2001]) ).
fof(f_48_2,plain,
( doDivides0(xp,sdtasdt0(xp,xm))
& ? [U_103] :
( sdtasdt0(xp,xm) = sdtasdt0(xp,U_103)
& aNaturalNumber0(U_103) )
& ? [U_102] :
( sdtasdt0(xn,xm) = sdtasdt0(xp,U_102)
& aNaturalNumber0(U_102) ) ),
inference(variable_rename,[status(thm)],[f_48_1]) ).
fof(f_48_3,plain,
( doDivides0(xp,sdtasdt0(xp,xm))
& ? [U_103] :
( sdtasdt0(xp,xm) = sdtasdt0(xp,U_103)
& aNaturalNumber0(U_103) )
& sdtasdt0(xn,xm) = sdtasdt0(xp,sK12)
& aNaturalNumber0(sK12) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK12]),skolemize(U_102,sK12)],[f_48_2]) ).
fof(f_48_4,plain,
( doDivides0(xp,sdtasdt0(xp,xm))
& sdtasdt0(xp,xm) = sdtasdt0(xp,sK13)
& aNaturalNumber0(sK13)
& sdtasdt0(xn,xm) = sdtasdt0(xp,sK12)
& aNaturalNumber0(sK12) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK13]),skolemize(U_103,sK13)],[f_48_3]) ).
fof(f_48_5,plain,
( doDivides0(xp,sdtasdt0(xp,xm))
& sdtasdt0(xp,xm) = sdtasdt0(xp,sK13)
& aNaturalNumber0(sK13)
& sdtasdt0(xn,xm) = sdtasdt0(xp,sK12)
& aNaturalNumber0(sK12) ),
inference(definitional_conversion,[status(esa)],[f_48_4]) ).
cnf(f_48_10,plain,
doDivides0(xp,sdtasdt0(xp,xm)),
inference(clausify,[status(thm)],[f_48_5]) ).
fof(f_49_1,negated_conjecture,
~ ( doDivides0(xp,sdtasdt0(xr,xm))
| ? [W0] :
( sdtasdt0(xr,xm) = sdtasdt0(xp,W0)
& aNaturalNumber0(W0) ) ),
inference(negate,[status(cth)],[m__]) ).
fof(f_49_2,negated_conjecture,
( ~ doDivides0(xp,sdtasdt0(xr,xm))
& ! [W0] :
( sdtasdt0(xr,xm) != sdtasdt0(xp,W0)
| ~ aNaturalNumber0(W0) ) ),
inference(fof_nnf,[status(thm)],[f_49_1]) ).
fof(f_49_3,negated_conjecture,
( ~ doDivides0(xp,sdtasdt0(xr,xm))
& ! [U_104] :
( sdtasdt0(xr,xm) != sdtasdt0(xp,U_104)
| ~ aNaturalNumber0(U_104) ) ),
inference(variable_rename,[status(thm)],[f_49_2]) ).
fof(f_49_4,negated_conjecture,
( ~ doDivides0(xp,sdtasdt0(xr,xm))
& ! [U_104] :
( sdtasdt0(xr,xm) != sdtasdt0(xp,U_104)
| ~ aNaturalNumber0(U_104) ) ),
inference(definitional_conversion,[status(esa)],[f_49_3]) ).
cnf(f_49_6,negated_conjecture,
~ doDivides0(xp,sdtasdt0(xr,xm)),
inference(clausify,[status(thm)],[f_49_4]) ).
cnf(equality_1,axiom,
Eq_x_0 = Eq_x_0,
theory(equality,[reflexivity]) ).
cnf(equality_19,axiom,
( doDivides0(Eq_y_0,Eq_y_1)
| ~ doDivides0(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(t1,plain,
~ doDivides0(xp,sdtasdt0(xr,xm)),
inference(start,[status(thm),parent(0:0)],[f_49_6]) ).
cnf(t2,plain,
( ~ aNaturalNumber0(xp)
| ~ doDivides0(xp,sdtpldt0(sdtasdt0(xp,xm),sdtasdt0(xr,xm)))
| ~ aNaturalNumber0(sdtasdt0(xp,xm))
| ~ doDivides0(xp,sdtasdt0(xp,xm))
| ~ aNaturalNumber0(sdtasdt0(xr,xm))
| doDivides0(xp,sdtasdt0(xr,xm)) ),
inference(extension,[status(thm),parent(t1:1)],[f_34_4]) ).
cnf(t3,plain,
$false,
inference(connection,[status(thm),parent(t2:1)],[t2:1,t1:1]) ).
cnf(t4,plain,
( ~ aNaturalNumber0(xr)
| ~ aNaturalNumber0(xm)
| aNaturalNumber0(sdtasdt0(xr,xm)) ),
inference(extension,[status(thm),parent(t2:2)],[f_5_4]) ).
cnf(t5,plain,
$false,
inference(connection,[status(thm),parent(t4:1)],[t4:1,t2:2]) ).
cnf(t6,plain,
aNaturalNumber0(xm),
inference(extension,[status(thm),parent(t4:2)],[f_39_4]) ).
cnf(t7,plain,
$false,
inference(connection,[status(thm),parent(t6:1)],[t6:1,t4:2]) ).
cnf(t8,plain,
aNaturalNumber0(xr),
inference(extension,[status(thm),parent(t4:3)],[f_43_3]) ).
cnf(t9,plain,
$false,
inference(connection,[status(thm),parent(t8:1)],[t8:1,t4:3]) ).
cnf(t10,plain,
doDivides0(xp,sdtasdt0(xp,xm)),
inference(extension,[status(thm),parent(t2:3)],[f_48_10]) ).
cnf(t11,plain,
$false,
inference(connection,[status(thm),parent(t10:1)],[t10:1,t2:3]) ).
cnf(t12,plain,
( ~ aNaturalNumber0(xp)
| ~ aNaturalNumber0(xm)
| aNaturalNumber0(sdtasdt0(xp,xm)) ),
inference(extension,[status(thm),parent(t2:4)],[f_5_4]) ).
cnf(t13,plain,
$false,
inference(connection,[status(thm),parent(t12:1)],[t12:1,t2:4]) ).
cnf(t14,plain,
aNaturalNumber0(xm),
inference(extension,[status(thm),parent(t12:2)],[f_39_4]) ).
cnf(t15,plain,
$false,
inference(connection,[status(thm),parent(t14:1)],[t14:1,t12:2]) ).
cnf(t16,plain,
aNaturalNumber0(xp),
inference(extension,[status(thm),parent(t12:3)],[f_39_5]) ).
cnf(t17,plain,
$false,
inference(connection,[status(thm),parent(t16:1)],[t16:1,t12:3]) ).
cnf(t18,plain,
( xp != xp
| ~ doDivides0(xp,sdtasdt0(xn,xm))
| sdtasdt0(xn,xm) != sdtpldt0(sdtasdt0(xp,xm),sdtasdt0(xr,xm))
| doDivides0(xp,sdtpldt0(sdtasdt0(xp,xm),sdtasdt0(xr,xm))) ),
inference(extension,[status(thm),parent(t2:5)],[equality_19]) ).
cnf(t19,plain,
$false,
inference(connection,[status(thm),parent(t18:1)],[t18:1,t2:5]) ).
cnf(t20,plain,
sdtasdt0(xn,xm) = sdtpldt0(sdtasdt0(xp,xm),sdtasdt0(xr,xm)),
inference(extension,[status(thm),parent(t18:2)],[f_46_3]) ).
cnf(t21,plain,
$false,
inference(connection,[status(thm),parent(t20:1)],[t20:1,t18:2]) ).
cnf(t22,plain,
doDivides0(xp,sdtasdt0(xn,xm)),
inference(extension,[status(thm),parent(t18:3)],[f_41_11]) ).
cnf(t23,plain,
$false,
inference(connection,[status(thm),parent(t22:1)],[t22:1,t18:3]) ).
cnf(t24,plain,
xp = xp,
inference(extension,[status(thm),parent(t18:4)],[equality_1]) ).
cnf(t25,plain,
$false,
inference(connection,[status(thm),parent(t24:1)],[t24:1,t18:4]) ).
cnf(t26,plain,
aNaturalNumber0(xp),
inference(extension,[status(thm),parent(t2:6)],[f_39_5]) ).
cnf(t27,plain,
$false,
inference(connection,[status(thm),parent(t26:1)],[t26:1,t2:6]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM492+3 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 This is a FOF_THM_RFO_SEQ 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.10/0.36 % Computer : n018.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Sat Sep 19 18:38:41 UTC 2026
% 0.10/0.36 % CPUTime :
% 243.15/243.47 % SZS status Theorem for theBenchmark
% 243.15/243.47 % SZS output start Proof for theBenchmark
% See solution above
%------------------------------------------------------------------------------