%------------------------------------------------------------------------------
% File : ConnectPP---0.7.2
% Problem : KRS217+1 : TPTP v9.3.1. Bugfixed v5.4.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 : n026.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:47:32 AM UTC 2026
% Result : Theorem 133.35s 138.64s
% Output : Proof 133.35s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 6
% Syntax : Number of formulae : 65 ( 25 unt; 0 def)
% Number of atoms : 238 ( 0 equ)
% Maximal formula atoms : 10 ( 3 avg)
% Number of connectives : 282 ( 109 ~; 86 |; 81 &)
% ( 4 <=>; 2 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 5 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 4 ( 3 usr; 1 prp; 0-3 aty)
% Number of functors : 13 ( 13 usr; 7 con; 0-2 aty)
% Number of variables : 159 ( 0 sgn 94 !; 51 ?)
% Comments :
%------------------------------------------------------------------------------
fof(thm,axiom,
! [Ax,C] :
( ! [I1] :
( model(I1,Ax)
=> model(I1,C) )
<=> status(Ax,C,thm) ),
file('KRS001+0.ax',thm) ).
fof(noc,axiom,
! [Ax,C] :
( ( ? [I2] :
( model(I2,not(C))
& model(I2,Ax) )
& ? [I1] :
( model(I1,C)
& model(I1,Ax) ) )
<=> status(Ax,C,noc) ),
file('KRS001+0.ax',noc) ).
fof(nota,axiom,
! [S1,S2] :
( ? [Ax,C] :
( ~ status(Ax,C,S2)
& status(Ax,C,S1) )
<=> nota(S1,S2) ),
file('KRS001+1.ax',nota) ).
fof(not,axiom,
! [I,F] :
( model(I,F)
<=> ~ model(I,not(F)) ),
file('KRS001+1.ax',not) ).
fof(mixed_pair,axiom,
? [Ax,C] :
( ? [I4] : ~ model(I4,C)
& ? [I3] :
( model(I3,C)
& ~ model(I3,Ax) )
& ! [I2] :
( model(I2,Ax)
=> model(I2,C) )
& ? [I1] : model(I1,Ax) ),
file('KRS001+1.ax',mixed_pair) ).
fof(nota_noc_thm,conjecture,
nota(noc,thm),
file('theBenchmark.p',nota_noc_thm) ).
fof(f_5_1,plain,
! [Ax,C] :
( ( ! [I1] :
( model(I1,C)
| ~ model(I1,Ax) )
| ~ status(Ax,C,thm) )
& ( status(Ax,C,thm)
| ? [I1] :
( ~ model(I1,C)
& model(I1,Ax) ) ) ),
inference(fof_nnf,[status(thm)],[thm]) ).
fof(f_5_2,plain,
! [U_45,U_44] :
( ( ! [U_43] :
( model(U_43,U_44)
| ~ model(U_43,U_45) )
| ~ status(U_45,U_44,thm) )
& ( status(U_45,U_44,thm)
| ? [U_42] :
( ~ model(U_42,U_44)
& model(U_42,U_45) ) ) ),
inference(variable_rename,[status(thm)],[f_5_1]) ).
fof(f_5_3,plain,
( ! [U_49,U_47] :
( ! [U_43] :
( model(U_43,U_47)
| ~ model(U_43,U_49) )
| ~ status(U_49,U_47,thm) )
& ! [U_48,U_46] :
( status(U_48,U_46,thm)
| ? [U_42] :
( ~ model(U_42,U_46)
& model(U_42,U_48) ) ) ),
inference(miniscope,[status(thm)],[f_5_2]) ).
fof(f_5_4,plain,
( ! [U_49,U_47] :
( ! [U_43] :
( model(U_43,U_47)
| ~ model(U_43,U_49) )
| ~ status(U_49,U_47,thm) )
& ! [U_48,U_46] :
( status(U_48,U_46,thm)
| ( ~ model(sK10(U_48,U_46),U_46)
& model(sK10(U_48,U_46),U_48) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK10]),skolemize(U_42,sK10(U_48,U_46))],[f_5_3]) ).
cnf(f_5_7,plain,
( model(U_43,U_47)
| ~ model(U_43,U_49)
| ~ status(U_49,U_47,thm) ),
inference(clausify,[status(thm)],[f_5_4]) ).
fof(f_19_1,plain,
! [Ax,C] :
( ( ( ? [I2] :
( model(I2,not(C))
& model(I2,Ax) )
& ? [I1] :
( model(I1,C)
& model(I1,Ax) ) )
| ~ status(Ax,C,noc) )
& ( status(Ax,C,noc)
| ! [I2] :
( ~ model(I2,not(C))
| ~ model(I2,Ax) )
| ! [I1] :
( ~ model(I1,C)
| ~ model(I1,Ax) ) ) ),
inference(fof_nnf,[status(thm)],[noc]) ).
fof(f_19_2,plain,
! [U_203,U_202] :
( ( ( ? [U_201] :
( model(U_201,not(U_202))
& model(U_201,U_203) )
& ? [U_200] :
( model(U_200,U_202)
& model(U_200,U_203) ) )
| ~ status(U_203,U_202,noc) )
& ( status(U_203,U_202,noc)
| ! [U_199] :
( ~ model(U_199,not(U_202))
| ~ model(U_199,U_203) )
| ! [U_198] :
( ~ model(U_198,U_202)
| ~ model(U_198,U_203) ) ) ),
inference(variable_rename,[status(thm)],[f_19_1]) ).
fof(f_19_3,plain,
( ! [U_207,U_205] :
( ( ? [U_201] :
( model(U_201,not(U_205))
& model(U_201,U_207) )
& ? [U_200] :
( model(U_200,U_205)
& model(U_200,U_207) ) )
| ~ status(U_207,U_205,noc) )
& ! [U_206,U_204] :
( status(U_206,U_204,noc)
| ! [U_199] :
( ~ model(U_199,not(U_204))
| ~ model(U_199,U_206) )
| ! [U_198] :
( ~ model(U_198,U_204)
| ~ model(U_198,U_206) ) ) ),
inference(miniscope,[status(thm)],[f_19_2]) ).
fof(f_19_4,plain,
( ! [U_207,U_205] :
( ( ? [U_201] :
( model(U_201,not(U_205))
& model(U_201,U_207) )
& model(sK43(U_207,U_205),U_205)
& model(sK43(U_207,U_205),U_207) )
| ~ status(U_207,U_205,noc) )
& ! [U_206,U_204] :
( status(U_206,U_204,noc)
| ! [U_199] :
( ~ model(U_199,not(U_204))
| ~ model(U_199,U_206) )
| ! [U_198] :
( ~ model(U_198,U_204)
| ~ model(U_198,U_206) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK43]),skolemize(U_200,sK43(U_207,U_205))],[f_19_3]) ).
fof(f_19_5,plain,
( ! [U_207,U_205] :
( ( model(sK44(U_207,U_205),not(U_205))
& model(sK44(U_207,U_205),U_207)
& model(sK43(U_207,U_205),U_205)
& model(sK43(U_207,U_205),U_207) )
| ~ status(U_207,U_205,noc) )
& ! [U_206,U_204] :
( status(U_206,U_204,noc)
| ! [U_199] :
( ~ model(U_199,not(U_204))
| ~ model(U_199,U_206) )
| ! [U_198] :
( ~ model(U_198,U_204)
| ~ model(U_198,U_206) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK44]),skolemize(U_201,sK44(U_207,U_205))],[f_19_4]) ).
cnf(f_19_6,plain,
( status(U_206,U_204,noc)
| ~ model(U_199,not(U_204))
| ~ model(U_199,U_206)
| ~ model(U_198,U_204)
| ~ model(U_198,U_206) ),
inference(clausify,[status(thm)],[f_19_5]) ).
fof(f_22_1,plain,
! [S1,S2] :
( ( ? [Ax,C] :
( ~ status(Ax,C,S2)
& status(Ax,C,S1) )
| ~ nota(S1,S2) )
& ( nota(S1,S2)
| ! [Ax,C] :
( status(Ax,C,S2)
| ~ status(Ax,C,S1) ) ) ),
inference(fof_nnf,[status(thm)],[nota]) ).
fof(f_22_2,plain,
! [U_233,U_232] :
( ( ? [U_231,U_230] :
( ~ status(U_231,U_230,U_232)
& status(U_231,U_230,U_233) )
| ~ nota(U_233,U_232) )
& ( nota(U_233,U_232)
| ! [U_229,U_228] :
( status(U_229,U_228,U_232)
| ~ status(U_229,U_228,U_233) ) ) ),
inference(variable_rename,[status(thm)],[f_22_1]) ).
fof(f_22_3,plain,
( ! [U_237,U_235] :
( ? [U_231,U_230] :
( ~ status(U_231,U_230,U_235)
& status(U_231,U_230,U_237) )
| ~ nota(U_237,U_235) )
& ! [U_236,U_234] :
( nota(U_236,U_234)
| ! [U_229,U_228] :
( status(U_229,U_228,U_234)
| ~ status(U_229,U_228,U_236) ) ) ),
inference(miniscope,[status(thm)],[f_22_2]) ).
fof(f_22_4,plain,
( ! [U_237,U_235] :
( ? [U_230] :
( ~ status(sK49(U_237,U_235),U_230,U_235)
& status(sK49(U_237,U_235),U_230,U_237) )
| ~ nota(U_237,U_235) )
& ! [U_236,U_234] :
( nota(U_236,U_234)
| ! [U_229,U_228] :
( status(U_229,U_228,U_234)
| ~ status(U_229,U_228,U_236) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK49]),skolemize(U_231,sK49(U_237,U_235))],[f_22_3]) ).
fof(f_22_5,plain,
( ! [U_237,U_235] :
( ( ~ status(sK49(U_237,U_235),sK50(U_237,U_235),U_235)
& status(sK49(U_237,U_235),sK50(U_237,U_235),U_237) )
| ~ nota(U_237,U_235) )
& ! [U_236,U_234] :
( nota(U_236,U_234)
| ! [U_229,U_228] :
( status(U_229,U_228,U_234)
| ~ status(U_229,U_228,U_236) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK50]),skolemize(U_230,sK50(U_237,U_235))],[f_22_4]) ).
cnf(f_22_6,plain,
( nota(U_236,U_234)
| status(U_229,U_228,U_234)
| ~ status(U_229,U_228,U_236) ),
inference(clausify,[status(thm)],[f_22_5]) ).
fof(f_26_1,plain,
! [I,F] :
( ( model(I,F)
| model(I,not(F)) )
& ( ~ model(I,not(F))
| ~ model(I,F) ) ),
inference(fof_nnf,[status(thm)],[not]) ).
fof(f_26_2,plain,
! [U_261,U_260] :
( ( model(U_261,U_260)
| model(U_261,not(U_260)) )
& ( ~ model(U_261,not(U_260))
| ~ model(U_261,U_260) ) ),
inference(variable_rename,[status(thm)],[f_26_1]) ).
fof(f_26_3,plain,
( ! [U_265,U_263] :
( model(U_265,U_263)
| model(U_265,not(U_263)) )
& ! [U_264,U_262] :
( ~ model(U_264,not(U_262))
| ~ model(U_264,U_262) ) ),
inference(miniscope,[status(thm)],[f_26_2]) ).
cnf(f_26_5,plain,
( model(U_265,U_263)
| model(U_265,not(U_263)) ),
inference(clausify,[status(thm)],[f_26_3]) ).
fof(f_31_1,plain,
? [Ax,C] :
( ? [I4] : ~ model(I4,C)
& ? [I3] :
( model(I3,C)
& ~ model(I3,Ax) )
& ! [I2] :
( model(I2,C)
| ~ model(I2,Ax) )
& ? [I1] : model(I1,Ax) ),
inference(fof_nnf,[status(thm)],[mixed_pair]) ).
fof(f_31_2,plain,
? [U_284,U_283] :
( ? [U_282] : ~ model(U_282,U_283)
& ? [U_281] :
( model(U_281,U_283)
& ~ model(U_281,U_284) )
& ! [U_280] :
( model(U_280,U_283)
| ~ model(U_280,U_284) )
& ? [U_279] : model(U_279,U_284) ),
inference(variable_rename,[status(thm)],[f_31_1]) ).
fof(f_31_3,plain,
? [U_284] :
( ? [U_283] :
( ? [U_282] : ~ model(U_282,U_283)
& ? [U_281] :
( model(U_281,U_283)
& ~ model(U_281,U_284) )
& ! [U_280] :
( model(U_280,U_283)
| ~ model(U_280,U_284) ) )
& ? [U_279] : model(U_279,U_284) ),
inference(miniscope,[status(thm)],[f_31_2]) ).
fof(f_31_4,plain,
( ? [U_283] :
( ? [U_282] : ~ model(U_282,U_283)
& ? [U_281] :
( model(U_281,U_283)
& ~ model(U_281,sK65) )
& ! [U_280] :
( model(U_280,U_283)
| ~ model(U_280,sK65) ) )
& ? [U_279] : model(U_279,sK65) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK65]),skolemize(U_284,sK65)],[f_31_3]) ).
fof(f_31_5,plain,
( ? [U_283] :
( ? [U_282] : ~ model(U_282,U_283)
& ? [U_281] :
( model(U_281,U_283)
& ~ model(U_281,sK65) )
& ! [U_280] :
( model(U_280,U_283)
| ~ model(U_280,sK65) ) )
& model(sK66,sK65) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK66]),skolemize(U_279,sK66)],[f_31_4]) ).
fof(f_31_6,plain,
( ? [U_282] : ~ model(U_282,sK67)
& ? [U_281] :
( model(U_281,sK67)
& ~ model(U_281,sK65) )
& ! [U_280] :
( model(U_280,sK67)
| ~ model(U_280,sK65) )
& model(sK66,sK65) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK67]),skolemize(U_283,sK67)],[f_31_5]) ).
fof(f_31_7,plain,
( ? [U_282] : ~ model(U_282,sK67)
& model(sK68,sK67)
& ~ model(sK68,sK65)
& ! [U_280] :
( model(U_280,sK67)
| ~ model(U_280,sK65) )
& model(sK66,sK65) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK68]),skolemize(U_281,sK68)],[f_31_6]) ).
fof(f_31_8,plain,
( ~ model(sK69,sK67)
& model(sK68,sK67)
& ~ model(sK68,sK65)
& ! [U_280] :
( model(U_280,sK67)
| ~ model(U_280,sK65) )
& model(sK66,sK65) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK69]),skolemize(U_282,sK69)],[f_31_7]) ).
cnf(f_31_9,plain,
model(sK66,sK65),
inference(clausify,[status(thm)],[f_31_8]) ).
cnf(f_31_10,plain,
( model(U_280,sK67)
| ~ model(U_280,sK65) ),
inference(clausify,[status(thm)],[f_31_8]) ).
cnf(f_31_11,plain,
~ model(sK68,sK65),
inference(clausify,[status(thm)],[f_31_8]) ).
cnf(f_31_12,plain,
model(sK68,sK67),
inference(clausify,[status(thm)],[f_31_8]) ).
fof(f_33_1,negated_conjecture,
~ nota(noc,thm),
inference(negate,[status(cth)],[nota_noc_thm]) ).
fof(f_33_2,negated_conjecture,
~ nota(noc,thm),
inference(definitional_conversion,[status(esa)],[f_33_1]) ).
cnf(f_33_3,negated_conjecture,
~ nota(noc,thm),
inference(clausify,[status(thm)],[f_33_2]) ).
cnf(t1,plain,
~ nota(noc,thm),
inference(start,[status(thm),parent(0:0)],[f_33_3]) ).
cnf(t2,plain,
( status(sK67,sK65,thm)
| ~ status(sK67,sK65,noc)
| nota(noc,thm) ),
inference(extension,[status(thm),parent(t1:1)],[f_22_6]) ).
cnf(t3,plain,
$false,
inference(connection,[status(thm),parent(t2:1)],[t2:1,t1:1]) ).
cnf(t4,plain,
( ~ model(sK66,sK65)
| ~ model(sK68,sK67)
| ~ model(sK68,not(sK65))
| ~ model(sK66,sK67)
| status(sK67,sK65,noc) ),
inference(extension,[status(thm),parent(t2:2)],[f_19_6]) ).
cnf(t5,plain,
$false,
inference(connection,[status(thm),parent(t4:1)],[t4:1,t2:2]) ).
cnf(t6,plain,
( ~ model(sK66,sK65)
| model(sK66,sK67) ),
inference(extension,[status(thm),parent(t4:2)],[f_31_10]) ).
cnf(t7,plain,
$false,
inference(connection,[status(thm),parent(t6:1)],[t6:1,t4:2]) ).
cnf(t8,plain,
model(sK66,sK65),
inference(extension,[status(thm),parent(t6:2)],[f_31_9]) ).
cnf(t9,plain,
$false,
inference(connection,[status(thm),parent(t8:1)],[t8:1,t6:2]) ).
cnf(t10,plain,
( model(sK68,sK65)
| model(sK68,not(sK65)) ),
inference(extension,[status(thm),parent(t4:3)],[f_26_5]) ).
cnf(t11,plain,
$false,
inference(connection,[status(thm),parent(t10:1)],[t10:1,t4:3]) ).
cnf(t12,plain,
~ model(sK68,sK65),
inference(extension,[status(thm),parent(t10:2)],[f_31_11]) ).
cnf(t13,plain,
$false,
inference(connection,[status(thm),parent(t12:1)],[t12:1,t10:2]) ).
cnf(t14,plain,
model(sK68,sK67),
inference(extension,[status(thm),parent(t4:4)],[f_31_12]) ).
cnf(t15,plain,
$false,
inference(connection,[status(thm),parent(t14:1)],[t14:1,t4:4]) ).
cnf(t16,plain,
model(sK66,sK65),
inference(extension,[status(thm),parent(t4:5)],[f_31_9]) ).
cnf(t17,plain,
$false,
inference(connection,[status(thm),parent(t16:1)],[t16:1,t4:5]) ).
cnf(t18,plain,
( ~ model(sK68,sK67)
| model(sK68,sK65)
| ~ status(sK67,sK65,thm) ),
inference(extension,[status(thm),parent(t2:3)],[f_5_7]) ).
cnf(t19,plain,
$false,
inference(connection,[status(thm),parent(t18:1)],[t18:1,t2:3]) ).
cnf(t20,plain,
~ model(sK68,sK65),
inference(extension,[status(thm),parent(t18:2)],[f_31_11]) ).
cnf(t21,plain,
$false,
inference(connection,[status(thm),parent(t20:1)],[t20:1,t18:2]) ).
cnf(t22,plain,
model(sK68,sK67),
inference(extension,[status(thm),parent(t18:3)],[f_31_12]) ).
cnf(t23,plain,
$false,
inference(connection,[status(thm),parent(t22:1)],[t22:1,t18:3]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : KRS217+1 : TPTP v9.3.1. Bugfixed v5.4.0.
% 0.00/0.04 This is a FOF_THM_RFO_NEQ 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.08/5.37 % Computer : n026.cluster.edu
% 0.08/5.37 % Model : x86_64 x86_64
% 0.08/5.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/5.37 % Memory : 8046.5625MB
% 0.08/5.37 % OS : Linux 6.8.0-71-generic
% 0.08/5.37 % CPULimit : 300
% 0.08/5.37 % WCLimit : 300
% 0.08/5.37 % DateTime : Sat Sep 19 12:20:12 UTC 2026
% 0.08/5.37 % CPUTime :
% 133.35/138.64 % SZS status Theorem for theBenchmark
% 133.35/138.64 % SZS output start Proof for theBenchmark
% See solution above
%------------------------------------------------------------------------------