%------------------------------------------------------------------------------
% File : ConnectPP---0.7.2
% Problem : NUM443+4 : TPTP v9.3.1. Released v4.0.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 : n009.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:16 AM UTC 2026
% Result : Theorem 76.87s 77.18s
% Output : Proof 76.87s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 5
% Syntax : Number of formulae : 67 ( 39 unt; 0 def)
% Number of atoms : 405 ( 55 equ)
% Maximal formula atoms : 34 ( 6 avg)
% Number of connectives : 484 ( 146 ~; 114 |; 210 &)
% ( 0 <=>; 14 =>; 0 <=; 0 <~>)
% Maximal formula depth : 20 ( 5 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 7 ( 5 usr; 1 prp; 0-3 aty)
% Number of functors : 13 ( 13 usr; 6 con; 0-2 aty)
% Number of variables : 89 ( 0 sgn 57 !; 22 ?)
% Comments :
%------------------------------------------------------------------------------
fof(mEquModSym,axiom,
! [W0,W1,W2] :
( ( W2 != sz00
& aInteger0(W2)
& aInteger0(W1)
& aInteger0(W0) )
=> ( sdteqdtlpzmzozddtrp0(W0,W1,W2)
=> sdteqdtlpzmzozddtrp0(W1,W0,W2) ) ),
file('theBenchmark.p',mEquModSym) ).
fof(mEquModTrn,axiom,
! [W0,W1,W2,W3] :
( ( aInteger0(W3)
& W2 != sz00
& aInteger0(W2)
& aInteger0(W1)
& aInteger0(W0) )
=> ( ( sdteqdtlpzmzozddtrp0(W1,W3,W2)
& sdteqdtlpzmzozddtrp0(W0,W1,W2) )
=> sdteqdtlpzmzozddtrp0(W0,W3,W2) ) ),
file('theBenchmark.p',mEquModTrn) ).
fof(m__1962,hypothesis,
( xq != sz00
& aInteger0(xq)
& aInteger0(xa) ),
file('theBenchmark.p',m__1962) ).
fof(m__2010,hypothesis,
( aInteger0(xc)
& aInteger0(xb) ),
file('theBenchmark.p',m__2010) ).
fof(m__,conjecture,
( ( sdteqdtlpzmzozddtrp0(xc,xb,xq)
& aDivisorOf0(xq,sdtpldt0(xc,smndt0(xb)))
& ? [W0] :
( sdtasdt0(xq,W0) = sdtpldt0(xc,smndt0(xb))
& aInteger0(W0) )
& aElementOf0(xb,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
& ~ aElementOf0(xb,szAzrzSzezqlpdtcmdtrp0(xa,xq))
& ! [W0] :
( ( ( ( sdteqdtlpzmzozddtrp0(W0,xa,xq)
| aDivisorOf0(xq,sdtpldt0(W0,smndt0(xa)))
| ? [W1] :
( sdtasdt0(xq,W1) = sdtpldt0(W0,smndt0(xa))
& aInteger0(W1) ) )
& aInteger0(W0) )
=> aElementOf0(W0,szAzrzSzezqlpdtcmdtrp0(xa,xq)) )
& ( aElementOf0(W0,szAzrzSzezqlpdtcmdtrp0(xa,xq))
=> ( sdteqdtlpzmzozddtrp0(W0,xa,xq)
& aDivisorOf0(xq,sdtpldt0(W0,smndt0(xa)))
& ? [W1] :
( sdtasdt0(xq,W1) = sdtpldt0(W0,smndt0(xa))
& aInteger0(W1) )
& aInteger0(W0) ) ) )
& aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq)) )
=> ( ( ! [W0] :
( ( ( ( sdteqdtlpzmzozddtrp0(W0,xa,xq)
| aDivisorOf0(xq,sdtpldt0(W0,smndt0(xa)))
| ? [W1] :
( sdtasdt0(xq,W1) = sdtpldt0(W0,smndt0(xa))
& aInteger0(W1) ) )
& aInteger0(W0) )
=> aElementOf0(W0,szAzrzSzezqlpdtcmdtrp0(xa,xq)) )
& ( aElementOf0(W0,szAzrzSzezqlpdtcmdtrp0(xa,xq))
=> ( sdteqdtlpzmzozddtrp0(W0,xa,xq)
& aDivisorOf0(xq,sdtpldt0(W0,smndt0(xa)))
& ? [W1] :
( sdtasdt0(xq,W1) = sdtpldt0(W0,smndt0(xa))
& aInteger0(W1) )
& aInteger0(W0) ) ) )
& aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq)) )
=> ( aElementOf0(xc,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
| ~ aElementOf0(xc,szAzrzSzezqlpdtcmdtrp0(xa,xq)) ) ) ),
file('theBenchmark.p',m__) ).
fof(f_21_1,plain,
! [W0,W1,W2] :
( sdteqdtlpzmzozddtrp0(W1,W0,W2)
| ~ sdteqdtlpzmzozddtrp0(W0,W1,W2)
| W2 = sz00
| ~ aInteger0(W2)
| ~ aInteger0(W1)
| ~ aInteger0(W0) ),
inference(fof_nnf,[status(thm)],[mEquModSym]) ).
fof(f_21_2,plain,
! [U_39,U_38,U_37] :
( sdteqdtlpzmzozddtrp0(U_38,U_39,U_37)
| ~ sdteqdtlpzmzozddtrp0(U_39,U_38,U_37)
| U_37 = sz00
| ~ aInteger0(U_37)
| ~ aInteger0(U_38)
| ~ aInteger0(U_39) ),
inference(variable_rename,[status(thm)],[f_21_1]) ).
cnf(f_21_3,plain,
( sdteqdtlpzmzozddtrp0(U_38,U_39,U_37)
| ~ sdteqdtlpzmzozddtrp0(U_39,U_38,U_37)
| U_37 = sz00
| ~ aInteger0(U_37)
| ~ aInteger0(U_38)
| ~ aInteger0(U_39) ),
inference(clausify,[status(thm)],[f_21_2]) ).
fof(f_22_1,plain,
! [W0,W1,W2,W3] :
( sdteqdtlpzmzozddtrp0(W0,W3,W2)
| ~ sdteqdtlpzmzozddtrp0(W1,W3,W2)
| ~ sdteqdtlpzmzozddtrp0(W0,W1,W2)
| ~ aInteger0(W3)
| W2 = sz00
| ~ aInteger0(W2)
| ~ aInteger0(W1)
| ~ aInteger0(W0) ),
inference(fof_nnf,[status(thm)],[mEquModTrn]) ).
fof(f_22_2,plain,
! [U_43,U_42,U_41,U_40] :
( sdteqdtlpzmzozddtrp0(U_43,U_40,U_41)
| ~ sdteqdtlpzmzozddtrp0(U_42,U_40,U_41)
| ~ sdteqdtlpzmzozddtrp0(U_43,U_42,U_41)
| ~ aInteger0(U_40)
| U_41 = sz00
| ~ aInteger0(U_41)
| ~ aInteger0(U_42)
| ~ aInteger0(U_43) ),
inference(variable_rename,[status(thm)],[f_22_1]) ).
cnf(f_22_3,plain,
( sdteqdtlpzmzozddtrp0(U_43,U_40,U_41)
| ~ sdteqdtlpzmzozddtrp0(U_42,U_40,U_41)
| ~ sdteqdtlpzmzozddtrp0(U_43,U_42,U_41)
| ~ aInteger0(U_40)
| U_41 = sz00
| ~ aInteger0(U_41)
| ~ aInteger0(U_42)
| ~ aInteger0(U_43) ),
inference(clausify,[status(thm)],[f_22_2]) ).
fof(f_41_1,plain,
( xq != sz00
& aInteger0(xq)
& aInteger0(xa) ),
inference(fof_nnf,[status(thm)],[m__1962]) ).
cnf(f_41_2,plain,
aInteger0(xa),
inference(clausify,[status(thm)],[f_41_1]) ).
cnf(f_41_3,plain,
aInteger0(xq),
inference(clausify,[status(thm)],[f_41_1]) ).
cnf(f_41_4,plain,
xq != sz00,
inference(clausify,[status(thm)],[f_41_1]) ).
fof(f_42_1,plain,
( aInteger0(xc)
& aInteger0(xb) ),
inference(fof_nnf,[status(thm)],[m__2010]) ).
cnf(f_42_2,plain,
aInteger0(xb),
inference(clausify,[status(thm)],[f_42_1]) ).
cnf(f_42_3,plain,
aInteger0(xc),
inference(clausify,[status(thm)],[f_42_1]) ).
fof(f_43_1,negated_conjecture,
( ~ ( aElementOf0(xc,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
| ~ aElementOf0(xc,szAzrzSzezqlpdtcmdtrp0(xa,xq)) )
& ! [W0] :
( ( ( ( sdteqdtlpzmzozddtrp0(W0,xa,xq)
| aDivisorOf0(xq,sdtpldt0(W0,smndt0(xa)))
| ? [W1] :
( sdtasdt0(xq,W1) = sdtpldt0(W0,smndt0(xa))
& aInteger0(W1) ) )
& aInteger0(W0) )
=> aElementOf0(W0,szAzrzSzezqlpdtcmdtrp0(xa,xq)) )
& ( aElementOf0(W0,szAzrzSzezqlpdtcmdtrp0(xa,xq))
=> ( sdteqdtlpzmzozddtrp0(W0,xa,xq)
& aDivisorOf0(xq,sdtpldt0(W0,smndt0(xa)))
& ? [W1] :
( sdtasdt0(xq,W1) = sdtpldt0(W0,smndt0(xa))
& aInteger0(W1) )
& aInteger0(W0) ) ) )
& aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
& sdteqdtlpzmzozddtrp0(xc,xb,xq)
& aDivisorOf0(xq,sdtpldt0(xc,smndt0(xb)))
& ? [W0] :
( sdtasdt0(xq,W0) = sdtpldt0(xc,smndt0(xb))
& aInteger0(W0) )
& aElementOf0(xb,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
& ~ aElementOf0(xb,szAzrzSzezqlpdtcmdtrp0(xa,xq))
& ! [W0] :
( ( ( ( sdteqdtlpzmzozddtrp0(W0,xa,xq)
| aDivisorOf0(xq,sdtpldt0(W0,smndt0(xa)))
| ? [W1] :
( sdtasdt0(xq,W1) = sdtpldt0(W0,smndt0(xa))
& aInteger0(W1) ) )
& aInteger0(W0) )
=> aElementOf0(W0,szAzrzSzezqlpdtcmdtrp0(xa,xq)) )
& ( aElementOf0(W0,szAzrzSzezqlpdtcmdtrp0(xa,xq))
=> ( sdteqdtlpzmzozddtrp0(W0,xa,xq)
& aDivisorOf0(xq,sdtpldt0(W0,smndt0(xa)))
& ? [W1] :
( sdtasdt0(xq,W1) = sdtpldt0(W0,smndt0(xa))
& aInteger0(W1) )
& aInteger0(W0) ) ) )
& aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq)) ),
inference(negate,[status(cth)],[m__]) ).
fof(f_43_2,negated_conjecture,
( ~ aElementOf0(xc,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
& aElementOf0(xc,szAzrzSzezqlpdtcmdtrp0(xa,xq))
& ! [W0] :
( ( aElementOf0(W0,szAzrzSzezqlpdtcmdtrp0(xa,xq))
| ( ~ sdteqdtlpzmzozddtrp0(W0,xa,xq)
& ~ aDivisorOf0(xq,sdtpldt0(W0,smndt0(xa)))
& ! [W1] :
( sdtasdt0(xq,W1) != sdtpldt0(W0,smndt0(xa))
| ~ aInteger0(W1) ) )
| ~ aInteger0(W0) )
& ( ( sdteqdtlpzmzozddtrp0(W0,xa,xq)
& aDivisorOf0(xq,sdtpldt0(W0,smndt0(xa)))
& ? [W1] :
( sdtasdt0(xq,W1) = sdtpldt0(W0,smndt0(xa))
& aInteger0(W1) )
& aInteger0(W0) )
| ~ aElementOf0(W0,szAzrzSzezqlpdtcmdtrp0(xa,xq)) ) )
& aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
& sdteqdtlpzmzozddtrp0(xc,xb,xq)
& aDivisorOf0(xq,sdtpldt0(xc,smndt0(xb)))
& ? [W0] :
( sdtasdt0(xq,W0) = sdtpldt0(xc,smndt0(xb))
& aInteger0(W0) )
& aElementOf0(xb,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
& ~ aElementOf0(xb,szAzrzSzezqlpdtcmdtrp0(xa,xq))
& ! [W0] :
( ( aElementOf0(W0,szAzrzSzezqlpdtcmdtrp0(xa,xq))
| ( ~ sdteqdtlpzmzozddtrp0(W0,xa,xq)
& ~ aDivisorOf0(xq,sdtpldt0(W0,smndt0(xa)))
& ! [W1] :
( sdtasdt0(xq,W1) != sdtpldt0(W0,smndt0(xa))
| ~ aInteger0(W1) ) )
| ~ aInteger0(W0) )
& ( ( sdteqdtlpzmzozddtrp0(W0,xa,xq)
& aDivisorOf0(xq,sdtpldt0(W0,smndt0(xa)))
& ? [W1] :
( sdtasdt0(xq,W1) = sdtpldt0(W0,smndt0(xa))
& aInteger0(W1) )
& aInteger0(W0) )
| ~ aElementOf0(W0,szAzrzSzezqlpdtcmdtrp0(xa,xq)) ) )
& aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq)) ),
inference(fof_nnf,[status(thm)],[f_43_1]) ).
fof(f_43_3,negated_conjecture,
( ~ aElementOf0(xc,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
& aElementOf0(xc,szAzrzSzezqlpdtcmdtrp0(xa,xq))
& ! [U_140] :
( ( aElementOf0(U_140,szAzrzSzezqlpdtcmdtrp0(xa,xq))
| ( ~ sdteqdtlpzmzozddtrp0(U_140,xa,xq)
& ~ aDivisorOf0(xq,sdtpldt0(U_140,smndt0(xa)))
& ! [U_139] :
( sdtasdt0(xq,U_139) != sdtpldt0(U_140,smndt0(xa))
| ~ aInteger0(U_139) ) )
| ~ aInteger0(U_140) )
& ( ( sdteqdtlpzmzozddtrp0(U_140,xa,xq)
& aDivisorOf0(xq,sdtpldt0(U_140,smndt0(xa)))
& ? [U_138] :
( sdtasdt0(xq,U_138) = sdtpldt0(U_140,smndt0(xa))
& aInteger0(U_138) )
& aInteger0(U_140) )
| ~ aElementOf0(U_140,szAzrzSzezqlpdtcmdtrp0(xa,xq)) ) )
& aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
& sdteqdtlpzmzozddtrp0(xc,xb,xq)
& aDivisorOf0(xq,sdtpldt0(xc,smndt0(xb)))
& ? [U_137] :
( sdtasdt0(xq,U_137) = sdtpldt0(xc,smndt0(xb))
& aInteger0(U_137) )
& aElementOf0(xb,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
& ~ aElementOf0(xb,szAzrzSzezqlpdtcmdtrp0(xa,xq))
& ! [U_136] :
( ( aElementOf0(U_136,szAzrzSzezqlpdtcmdtrp0(xa,xq))
| ( ~ sdteqdtlpzmzozddtrp0(U_136,xa,xq)
& ~ aDivisorOf0(xq,sdtpldt0(U_136,smndt0(xa)))
& ! [U_135] :
( sdtasdt0(xq,U_135) != sdtpldt0(U_136,smndt0(xa))
| ~ aInteger0(U_135) ) )
| ~ aInteger0(U_136) )
& ( ( sdteqdtlpzmzozddtrp0(U_136,xa,xq)
& aDivisorOf0(xq,sdtpldt0(U_136,smndt0(xa)))
& ? [U_134] :
( sdtasdt0(xq,U_134) = sdtpldt0(U_136,smndt0(xa))
& aInteger0(U_134) )
& aInteger0(U_136) )
| ~ aElementOf0(U_136,szAzrzSzezqlpdtcmdtrp0(xa,xq)) ) )
& aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq)) ),
inference(variable_rename,[status(thm)],[f_43_2]) ).
fof(f_43_4,negated_conjecture,
( ~ aElementOf0(xc,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
& aElementOf0(xc,szAzrzSzezqlpdtcmdtrp0(xa,xq))
& ! [U_144] :
( aElementOf0(U_144,szAzrzSzezqlpdtcmdtrp0(xa,xq))
| ( ~ sdteqdtlpzmzozddtrp0(U_144,xa,xq)
& ~ aDivisorOf0(xq,sdtpldt0(U_144,smndt0(xa)))
& ! [U_139] :
( sdtasdt0(xq,U_139) != sdtpldt0(U_144,smndt0(xa))
| ~ aInteger0(U_139) ) )
| ~ aInteger0(U_144) )
& ! [U_143] :
( ( sdteqdtlpzmzozddtrp0(U_143,xa,xq)
& aDivisorOf0(xq,sdtpldt0(U_143,smndt0(xa)))
& ? [U_138] :
( sdtasdt0(xq,U_138) = sdtpldt0(U_143,smndt0(xa))
& aInteger0(U_138) )
& aInteger0(U_143) )
| ~ aElementOf0(U_143,szAzrzSzezqlpdtcmdtrp0(xa,xq)) )
& aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
& sdteqdtlpzmzozddtrp0(xc,xb,xq)
& aDivisorOf0(xq,sdtpldt0(xc,smndt0(xb)))
& ? [U_137] :
( sdtasdt0(xq,U_137) = sdtpldt0(xc,smndt0(xb))
& aInteger0(U_137) )
& aElementOf0(xb,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
& ~ aElementOf0(xb,szAzrzSzezqlpdtcmdtrp0(xa,xq))
& ! [U_142] :
( aElementOf0(U_142,szAzrzSzezqlpdtcmdtrp0(xa,xq))
| ( ~ sdteqdtlpzmzozddtrp0(U_142,xa,xq)
& ~ aDivisorOf0(xq,sdtpldt0(U_142,smndt0(xa)))
& ! [U_135] :
( sdtasdt0(xq,U_135) != sdtpldt0(U_142,smndt0(xa))
| ~ aInteger0(U_135) ) )
| ~ aInteger0(U_142) )
& ! [U_141] :
( ( sdteqdtlpzmzozddtrp0(U_141,xa,xq)
& aDivisorOf0(xq,sdtpldt0(U_141,smndt0(xa)))
& ? [U_134] :
( sdtasdt0(xq,U_134) = sdtpldt0(U_141,smndt0(xa))
& aInteger0(U_134) )
& aInteger0(U_141) )
| ~ aElementOf0(U_141,szAzrzSzezqlpdtcmdtrp0(xa,xq)) )
& aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq)) ),
inference(miniscope,[status(thm)],[f_43_3]) ).
fof(f_43_5,negated_conjecture,
( ~ aElementOf0(xc,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
& aElementOf0(xc,szAzrzSzezqlpdtcmdtrp0(xa,xq))
& ! [U_144] :
( aElementOf0(U_144,szAzrzSzezqlpdtcmdtrp0(xa,xq))
| ( ~ sdteqdtlpzmzozddtrp0(U_144,xa,xq)
& ~ aDivisorOf0(xq,sdtpldt0(U_144,smndt0(xa)))
& ! [U_139] :
( sdtasdt0(xq,U_139) != sdtpldt0(U_144,smndt0(xa))
| ~ aInteger0(U_139) ) )
| ~ aInteger0(U_144) )
& ! [U_143] :
( ( sdteqdtlpzmzozddtrp0(U_143,xa,xq)
& aDivisorOf0(xq,sdtpldt0(U_143,smndt0(xa)))
& ? [U_138] :
( sdtasdt0(xq,U_138) = sdtpldt0(U_143,smndt0(xa))
& aInteger0(U_138) )
& aInteger0(U_143) )
| ~ aElementOf0(U_143,szAzrzSzezqlpdtcmdtrp0(xa,xq)) )
& aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
& sdteqdtlpzmzozddtrp0(xc,xb,xq)
& aDivisorOf0(xq,sdtpldt0(xc,smndt0(xb)))
& ? [U_137] :
( sdtasdt0(xq,U_137) = sdtpldt0(xc,smndt0(xb))
& aInteger0(U_137) )
& aElementOf0(xb,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
& ~ aElementOf0(xb,szAzrzSzezqlpdtcmdtrp0(xa,xq))
& ! [U_142] :
( aElementOf0(U_142,szAzrzSzezqlpdtcmdtrp0(xa,xq))
| ( ~ sdteqdtlpzmzozddtrp0(U_142,xa,xq)
& ~ aDivisorOf0(xq,sdtpldt0(U_142,smndt0(xa)))
& ! [U_135] :
( sdtasdt0(xq,U_135) != sdtpldt0(U_142,smndt0(xa))
| ~ aInteger0(U_135) ) )
| ~ aInteger0(U_142) )
& ! [U_141] :
( ( sdteqdtlpzmzozddtrp0(U_141,xa,xq)
& aDivisorOf0(xq,sdtpldt0(U_141,smndt0(xa)))
& sdtasdt0(xq,sK21(U_141)) = sdtpldt0(U_141,smndt0(xa))
& aInteger0(sK21(U_141))
& aInteger0(U_141) )
| ~ aElementOf0(U_141,szAzrzSzezqlpdtcmdtrp0(xa,xq)) )
& aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK21]),skolemize(U_134,sK21(U_141))],[f_43_4]) ).
fof(f_43_6,negated_conjecture,
( ~ aElementOf0(xc,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
& aElementOf0(xc,szAzrzSzezqlpdtcmdtrp0(xa,xq))
& ! [U_144] :
( aElementOf0(U_144,szAzrzSzezqlpdtcmdtrp0(xa,xq))
| ( ~ sdteqdtlpzmzozddtrp0(U_144,xa,xq)
& ~ aDivisorOf0(xq,sdtpldt0(U_144,smndt0(xa)))
& ! [U_139] :
( sdtasdt0(xq,U_139) != sdtpldt0(U_144,smndt0(xa))
| ~ aInteger0(U_139) ) )
| ~ aInteger0(U_144) )
& ! [U_143] :
( ( sdteqdtlpzmzozddtrp0(U_143,xa,xq)
& aDivisorOf0(xq,sdtpldt0(U_143,smndt0(xa)))
& ? [U_138] :
( sdtasdt0(xq,U_138) = sdtpldt0(U_143,smndt0(xa))
& aInteger0(U_138) )
& aInteger0(U_143) )
| ~ aElementOf0(U_143,szAzrzSzezqlpdtcmdtrp0(xa,xq)) )
& aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
& sdteqdtlpzmzozddtrp0(xc,xb,xq)
& aDivisorOf0(xq,sdtpldt0(xc,smndt0(xb)))
& sdtasdt0(xq,sK22) = sdtpldt0(xc,smndt0(xb))
& aInteger0(sK22)
& aElementOf0(xb,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
& ~ aElementOf0(xb,szAzrzSzezqlpdtcmdtrp0(xa,xq))
& ! [U_142] :
( aElementOf0(U_142,szAzrzSzezqlpdtcmdtrp0(xa,xq))
| ( ~ sdteqdtlpzmzozddtrp0(U_142,xa,xq)
& ~ aDivisorOf0(xq,sdtpldt0(U_142,smndt0(xa)))
& ! [U_135] :
( sdtasdt0(xq,U_135) != sdtpldt0(U_142,smndt0(xa))
| ~ aInteger0(U_135) ) )
| ~ aInteger0(U_142) )
& ! [U_141] :
( ( sdteqdtlpzmzozddtrp0(U_141,xa,xq)
& aDivisorOf0(xq,sdtpldt0(U_141,smndt0(xa)))
& sdtasdt0(xq,sK21(U_141)) = sdtpldt0(U_141,smndt0(xa))
& aInteger0(sK21(U_141))
& aInteger0(U_141) )
| ~ aElementOf0(U_141,szAzrzSzezqlpdtcmdtrp0(xa,xq)) )
& aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK22]),skolemize(U_137,sK22)],[f_43_5]) ).
fof(f_43_7,negated_conjecture,
( ~ aElementOf0(xc,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
& aElementOf0(xc,szAzrzSzezqlpdtcmdtrp0(xa,xq))
& ! [U_144] :
( aElementOf0(U_144,szAzrzSzezqlpdtcmdtrp0(xa,xq))
| ( ~ sdteqdtlpzmzozddtrp0(U_144,xa,xq)
& ~ aDivisorOf0(xq,sdtpldt0(U_144,smndt0(xa)))
& ! [U_139] :
( sdtasdt0(xq,U_139) != sdtpldt0(U_144,smndt0(xa))
| ~ aInteger0(U_139) ) )
| ~ aInteger0(U_144) )
& ! [U_143] :
( ( sdteqdtlpzmzozddtrp0(U_143,xa,xq)
& aDivisorOf0(xq,sdtpldt0(U_143,smndt0(xa)))
& sdtasdt0(xq,sK23(U_143)) = sdtpldt0(U_143,smndt0(xa))
& aInteger0(sK23(U_143))
& aInteger0(U_143) )
| ~ aElementOf0(U_143,szAzrzSzezqlpdtcmdtrp0(xa,xq)) )
& aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
& sdteqdtlpzmzozddtrp0(xc,xb,xq)
& aDivisorOf0(xq,sdtpldt0(xc,smndt0(xb)))
& sdtasdt0(xq,sK22) = sdtpldt0(xc,smndt0(xb))
& aInteger0(sK22)
& aElementOf0(xb,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
& ~ aElementOf0(xb,szAzrzSzezqlpdtcmdtrp0(xa,xq))
& ! [U_142] :
( aElementOf0(U_142,szAzrzSzezqlpdtcmdtrp0(xa,xq))
| ( ~ sdteqdtlpzmzozddtrp0(U_142,xa,xq)
& ~ aDivisorOf0(xq,sdtpldt0(U_142,smndt0(xa)))
& ! [U_135] :
( sdtasdt0(xq,U_135) != sdtpldt0(U_142,smndt0(xa))
| ~ aInteger0(U_135) ) )
| ~ aInteger0(U_142) )
& ! [U_141] :
( ( sdteqdtlpzmzozddtrp0(U_141,xa,xq)
& aDivisorOf0(xq,sdtpldt0(U_141,smndt0(xa)))
& sdtasdt0(xq,sK21(U_141)) = sdtpldt0(U_141,smndt0(xa))
& aInteger0(sK21(U_141))
& aInteger0(U_141) )
| ~ aElementOf0(U_141,szAzrzSzezqlpdtcmdtrp0(xa,xq)) )
& aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK23]),skolemize(U_138,sK23(U_143))],[f_43_6]) ).
cnf(f_43_17,negated_conjecture,
~ aElementOf0(xb,szAzrzSzezqlpdtcmdtrp0(xa,xq)),
inference(clausify,[status(thm)],[f_43_7]) ).
cnf(f_43_22,negated_conjecture,
sdteqdtlpzmzozddtrp0(xc,xb,xq),
inference(clausify,[status(thm)],[f_43_7]) ).
cnf(f_43_24,negated_conjecture,
( aInteger0(U_143)
| ~ aElementOf0(U_143,szAzrzSzezqlpdtcmdtrp0(xa,xq)) ),
inference(clausify,[status(thm)],[f_43_7]) ).
cnf(f_43_28,negated_conjecture,
( sdteqdtlpzmzozddtrp0(U_143,xa,xq)
| ~ aElementOf0(U_143,szAzrzSzezqlpdtcmdtrp0(xa,xq)) ),
inference(clausify,[status(thm)],[f_43_7]) ).
cnf(f_43_31,negated_conjecture,
( ~ sdteqdtlpzmzozddtrp0(U_144,xa,xq)
| ~ aInteger0(U_144)
| aElementOf0(U_144,szAzrzSzezqlpdtcmdtrp0(xa,xq)) ),
inference(clausify,[status(thm)],[f_43_7]) ).
cnf(f_43_32,negated_conjecture,
aElementOf0(xc,szAzrzSzezqlpdtcmdtrp0(xa,xq)),
inference(clausify,[status(thm)],[f_43_7]) ).
cnf(t1,plain,
~ aElementOf0(xb,szAzrzSzezqlpdtcmdtrp0(xa,xq)),
inference(start,[status(thm),parent(0:0)],[f_43_17]) ).
cnf(t2,plain,
( ~ aInteger0(xb)
| ~ sdteqdtlpzmzozddtrp0(xb,xa,xq)
| aElementOf0(xb,szAzrzSzezqlpdtcmdtrp0(xa,xq)) ),
inference(extension,[status(thm),parent(t1:1)],[f_43_31]) ).
cnf(t3,plain,
$false,
inference(connection,[status(thm),parent(t2:1)],[t2:1,t1:1]) ).
cnf(t4,plain,
( ~ aInteger0(xc)
| ~ aInteger0(xq)
| xq = sz00
| ~ aInteger0(xa)
| ~ sdteqdtlpzmzozddtrp0(xb,xc,xq)
| ~ sdteqdtlpzmzozddtrp0(xc,xa,xq)
| ~ aInteger0(xb)
| sdteqdtlpzmzozddtrp0(xb,xa,xq) ),
inference(extension,[status(thm),parent(t2:2)],[f_22_3]) ).
cnf(t5,plain,
$false,
inference(connection,[status(thm),parent(t4:1)],[t4:1,t2:2]) ).
cnf(t6,plain,
aInteger0(xb),
inference(extension,[status(thm),parent(t4:2)],[f_42_2]) ).
cnf(t7,plain,
$false,
inference(connection,[status(thm),parent(t6:1)],[t6:1,t4:2]) ).
cnf(l3,lemma,
aInteger0(xb),
inference(lemma,[status(cth),parent(t4:2),below(t2:2)],[t4:2]) ).
cnf(t8,plain,
( ~ aElementOf0(xc,szAzrzSzezqlpdtcmdtrp0(xa,xq))
| sdteqdtlpzmzozddtrp0(xc,xa,xq) ),
inference(extension,[status(thm),parent(t4:3)],[f_43_28]) ).
cnf(t9,plain,
$false,
inference(connection,[status(thm),parent(t8:1)],[t8:1,t4:3]) ).
cnf(t10,plain,
aElementOf0(xc,szAzrzSzezqlpdtcmdtrp0(xa,xq)),
inference(extension,[status(thm),parent(t8:2)],[f_43_32]) ).
cnf(t11,plain,
$false,
inference(connection,[status(thm),parent(t10:1)],[t10:1,t8:2]) ).
cnf(t12,plain,
( ~ aInteger0(xb)
| ~ aInteger0(xq)
| xq = sz00
| ~ sdteqdtlpzmzozddtrp0(xc,xb,xq)
| ~ aInteger0(xc)
| sdteqdtlpzmzozddtrp0(xb,xc,xq) ),
inference(extension,[status(thm),parent(t4:4)],[f_21_3]) ).
cnf(t13,plain,
$false,
inference(connection,[status(thm),parent(t12:1)],[t12:1,t4:4]) ).
cnf(t14,plain,
aInteger0(xc),
inference(extension,[status(thm),parent(t12:2)],[f_42_3]) ).
cnf(t15,plain,
$false,
inference(connection,[status(thm),parent(t14:1)],[t14:1,t12:2]) ).
cnf(t16,plain,
sdteqdtlpzmzozddtrp0(xc,xb,xq),
inference(extension,[status(thm),parent(t12:3)],[f_43_22]) ).
cnf(t17,plain,
$false,
inference(connection,[status(thm),parent(t16:1)],[t16:1,t12:3]) ).
cnf(t18,plain,
xq != sz00,
inference(extension,[status(thm),parent(t12:4)],[f_41_4]) ).
cnf(t19,plain,
$false,
inference(connection,[status(thm),parent(t18:1)],[t18:1,t12:4]) ).
cnf(t20,plain,
aInteger0(xq),
inference(extension,[status(thm),parent(t12:5)],[f_41_3]) ).
cnf(t21,plain,
$false,
inference(connection,[status(thm),parent(t20:1)],[t20:1,t12:5]) ).
cnf(t22,plain,
aInteger0(xb),
inference(lemma_extension,[status(thm),parent(t12:6)],[l3:1]) ).
cnf(t23,plain,
$false,
inference(connection,[status(thm),parent(t22:1)],[t22:1,t12:6]) ).
cnf(t24,plain,
aInteger0(xa),
inference(extension,[status(thm),parent(t4:5)],[f_41_2]) ).
cnf(t25,plain,
$false,
inference(connection,[status(thm),parent(t24:1)],[t24:1,t4:5]) ).
cnf(t26,plain,
xq != sz00,
inference(extension,[status(thm),parent(t4:6)],[f_41_4]) ).
cnf(t27,plain,
$false,
inference(connection,[status(thm),parent(t26:1)],[t26:1,t4:6]) ).
cnf(t28,plain,
aInteger0(xq),
inference(extension,[status(thm),parent(t4:7)],[f_41_3]) ).
cnf(t29,plain,
$false,
inference(connection,[status(thm),parent(t28:1)],[t28:1,t4:7]) ).
cnf(t30,plain,
( ~ aElementOf0(xc,szAzrzSzezqlpdtcmdtrp0(xa,xq))
| aInteger0(xc) ),
inference(extension,[status(thm),parent(t4:8)],[f_43_24]) ).
cnf(t31,plain,
$false,
inference(connection,[status(thm),parent(t30:1)],[t30:1,t4:8]) ).
cnf(t32,plain,
aElementOf0(xc,szAzrzSzezqlpdtcmdtrp0(xa,xq)),
inference(extension,[status(thm),parent(t30:2)],[f_43_32]) ).
cnf(t33,plain,
$false,
inference(connection,[status(thm),parent(t32:1)],[t32:1,t30:2]) ).
cnf(t34,plain,
aInteger0(xb),
inference(extension,[status(thm),parent(t2:3)],[f_42_2]) ).
cnf(t35,plain,
$false,
inference(connection,[status(thm),parent(t34:1)],[t34:1,t2:3]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM443+4 : 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/sandbox/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.37 % Computer : n009.cluster.edu
% 0.09/0.37 % Model : x86_64 x86_64
% 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37 % Memory : 8046.5625MB
% 0.09/0.37 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Sat Sep 19 18:26:56 UTC 2026
% 0.09/0.37 % CPUTime :
% 76.87/77.18 % SZS status Theorem for theBenchmark
% 76.87/77.18 % SZS output start Proof for theBenchmark
% See solution above
%------------------------------------------------------------------------------