%------------------------------------------------------------------------------
% File : ConnectPP---0.7.2
% Problem : KRS101+1 : TPTP v9.3.1. Released v3.1.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 : n011.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:16 AM UTC 2026
% Result : Unsatisfiable 0.57s 0.82s
% Output : Proof 0.57s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 3
% Syntax : Number of formulae : 71 ( 32 unt; 0 def)
% Number of atoms : 388 ( 50 equ)
% Maximal formula atoms : 40 ( 5 avg)
% Number of connectives : 507 ( 190 ~; 182 |; 130 &)
% ( 1 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 18 ( 4 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 10 ( 8 usr; 1 prp; 0-5 aty)
% Number of functors : 8 ( 8 usr; 1 con; 0-1 aty)
% Number of variables : 272 ( 72 sgn 143 !; 45 ?)
% Comments :
%------------------------------------------------------------------------------
fof(axiom_2,axiom,
! [X] :
( cUnsatisfiable(X)
<=> ( ? [Y] :
( ~ ! [Z0,Z1] :
( ( rs(Y,Z1)
& rs(Y,Z0) )
=> Z0 = Z1 )
& rr(X,Y) )
& ! [Y] :
( rr(X,Y)
=> ( cc(Y)
| ~ ? [Z0,Z1] :
( Z0 != Z1
& rs(Y,Z1)
& rs(Y,Z0) ) ) )
& ! [Y] :
( rr(X,Y)
=> cd(Y) ) ) ),
file('theBenchmark.p',axiom_2) ).
fof(axiom_3,axiom,
! [X] :
( cc(X)
=> ~ cd(X) ),
file('theBenchmark.p',axiom_3) ).
fof(axiom_4,axiom,
cUnsatisfiable(i2003_11_14_17_20_36582),
file('theBenchmark.p',axiom_4) ).
fof(f_14_1,plain,
! [X] :
( ( cUnsatisfiable(X)
| ! [Y] :
( ! [Z0,Z1] :
( Z0 = Z1
| ~ rs(Y,Z1)
| ~ rs(Y,Z0) )
| ~ rr(X,Y) )
| ? [Y] :
( ~ cc(Y)
& ? [Z0,Z1] :
( Z0 != Z1
& rs(Y,Z1)
& rs(Y,Z0) )
& rr(X,Y) )
| ? [Y] :
( ~ cd(Y)
& rr(X,Y) ) )
& ( ( ? [Y] :
( ? [Z0,Z1] :
( Z0 != Z1
& rs(Y,Z1)
& rs(Y,Z0) )
& rr(X,Y) )
& ! [Y] :
( cc(Y)
| ! [Z0,Z1] :
( Z0 = Z1
| ~ rs(Y,Z1)
| ~ rs(Y,Z0) )
| ~ rr(X,Y) )
& ! [Y] :
( cd(Y)
| ~ rr(X,Y) ) )
| ~ cUnsatisfiable(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_2]) ).
fof(f_14_2,plain,
! [U_46] :
( ( cUnsatisfiable(U_46)
| ! [U_45] :
( ! [U_44,U_43] :
( U_44 = U_43
| ~ rs(U_45,U_43)
| ~ rs(U_45,U_44) )
| ~ rr(U_46,U_45) )
| ? [U_42] :
( ~ cc(U_42)
& ? [U_41,U_40] :
( U_41 != U_40
& rs(U_42,U_40)
& rs(U_42,U_41) )
& rr(U_46,U_42) )
| ? [U_39] :
( ~ cd(U_39)
& rr(U_46,U_39) ) )
& ( ( ? [U_38] :
( ? [U_37,U_36] :
( U_37 != U_36
& rs(U_38,U_36)
& rs(U_38,U_37) )
& rr(U_46,U_38) )
& ! [U_35] :
( cc(U_35)
| ! [U_34,U_33] :
( U_34 = U_33
| ~ rs(U_35,U_33)
| ~ rs(U_35,U_34) )
| ~ rr(U_46,U_35) )
& ! [U_32] :
( cd(U_32)
| ~ rr(U_46,U_32) ) )
| ~ cUnsatisfiable(U_46) ) ),
inference(variable_rename,[status(thm)],[f_14_1]) ).
fof(f_14_3,plain,
( ! [U_48] :
( cUnsatisfiable(U_48)
| ! [U_45] :
( ! [U_44,U_43] :
( U_44 = U_43
| ~ rs(U_45,U_43)
| ~ rs(U_45,U_44) )
| ~ rr(U_48,U_45) )
| ? [U_42] :
( ~ cc(U_42)
& ? [U_41] :
( ? [U_40] :
( U_41 != U_40
& rs(U_42,U_40) )
& rs(U_42,U_41) )
& rr(U_48,U_42) )
| ? [U_39] :
( ~ cd(U_39)
& rr(U_48,U_39) ) )
& ! [U_47] :
( ( ? [U_38] :
( ? [U_37,U_36] :
( U_37 != U_36
& rs(U_38,U_36)
& rs(U_38,U_37) )
& rr(U_47,U_38) )
& ! [U_35] :
( cc(U_35)
| ! [U_34] :
( ! [U_33] :
( U_34 = U_33
| ~ rs(U_35,U_33) )
| ~ rs(U_35,U_34) )
| ~ rr(U_47,U_35) )
& ! [U_32] :
( cd(U_32)
| ~ rr(U_47,U_32) ) )
| ~ cUnsatisfiable(U_47) ) ),
inference(miniscope,[status(thm)],[f_14_2]) ).
fof(f_14_4,plain,
( ! [U_48] :
( cUnsatisfiable(U_48)
| ! [U_45] :
( ! [U_44,U_43] :
( U_44 = U_43
| ~ rs(U_45,U_43)
| ~ rs(U_45,U_44) )
| ~ rr(U_48,U_45) )
| ? [U_42] :
( ~ cc(U_42)
& ? [U_41] :
( ? [U_40] :
( U_41 != U_40
& rs(U_42,U_40) )
& rs(U_42,U_41) )
& rr(U_48,U_42) )
| ? [U_39] :
( ~ cd(U_39)
& rr(U_48,U_39) ) )
& ! [U_47] :
( ( ? [U_37,U_36] :
( U_37 != U_36
& rs(sK1(U_47),U_36)
& rs(sK1(U_47),U_37) )
& rr(U_47,sK1(U_47))
& ! [U_35] :
( cc(U_35)
| ! [U_34] :
( ! [U_33] :
( U_34 = U_33
| ~ rs(U_35,U_33) )
| ~ rs(U_35,U_34) )
| ~ rr(U_47,U_35) )
& ! [U_32] :
( cd(U_32)
| ~ rr(U_47,U_32) ) )
| ~ cUnsatisfiable(U_47) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1]),skolemize(U_38,sK1(U_47))],[f_14_3]) ).
fof(f_14_5,plain,
( ! [U_48] :
( cUnsatisfiable(U_48)
| ! [U_45] :
( ! [U_44,U_43] :
( U_44 = U_43
| ~ rs(U_45,U_43)
| ~ rs(U_45,U_44) )
| ~ rr(U_48,U_45) )
| ? [U_42] :
( ~ cc(U_42)
& ? [U_41] :
( ? [U_40] :
( U_41 != U_40
& rs(U_42,U_40) )
& rs(U_42,U_41) )
& rr(U_48,U_42) )
| ? [U_39] :
( ~ cd(U_39)
& rr(U_48,U_39) ) )
& ! [U_47] :
( ( ? [U_36] :
( sK2(U_47) != U_36
& rs(sK1(U_47),U_36)
& rs(sK1(U_47),sK2(U_47)) )
& rr(U_47,sK1(U_47))
& ! [U_35] :
( cc(U_35)
| ! [U_34] :
( ! [U_33] :
( U_34 = U_33
| ~ rs(U_35,U_33) )
| ~ rs(U_35,U_34) )
| ~ rr(U_47,U_35) )
& ! [U_32] :
( cd(U_32)
| ~ rr(U_47,U_32) ) )
| ~ cUnsatisfiable(U_47) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2]),skolemize(U_37,sK2(U_47))],[f_14_4]) ).
fof(f_14_6,plain,
( ! [U_48] :
( cUnsatisfiable(U_48)
| ! [U_45] :
( ! [U_44,U_43] :
( U_44 = U_43
| ~ rs(U_45,U_43)
| ~ rs(U_45,U_44) )
| ~ rr(U_48,U_45) )
| ? [U_42] :
( ~ cc(U_42)
& ? [U_41] :
( ? [U_40] :
( U_41 != U_40
& rs(U_42,U_40) )
& rs(U_42,U_41) )
& rr(U_48,U_42) )
| ? [U_39] :
( ~ cd(U_39)
& rr(U_48,U_39) ) )
& ! [U_47] :
( ( sK2(U_47) != sK3(U_47)
& rs(sK1(U_47),sK3(U_47))
& rs(sK1(U_47),sK2(U_47))
& rr(U_47,sK1(U_47))
& ! [U_35] :
( cc(U_35)
| ! [U_34] :
( ! [U_33] :
( U_34 = U_33
| ~ rs(U_35,U_33) )
| ~ rs(U_35,U_34) )
| ~ rr(U_47,U_35) )
& ! [U_32] :
( cd(U_32)
| ~ rr(U_47,U_32) ) )
| ~ cUnsatisfiable(U_47) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3]),skolemize(U_36,sK3(U_47))],[f_14_5]) ).
fof(f_14_7,plain,
( ! [U_48] :
( cUnsatisfiable(U_48)
| ! [U_45] :
( ! [U_44,U_43] :
( U_44 = U_43
| ~ rs(U_45,U_43)
| ~ rs(U_45,U_44) )
| ~ rr(U_48,U_45) )
| ? [U_42] :
( ~ cc(U_42)
& ? [U_41] :
( ? [U_40] :
( U_41 != U_40
& rs(U_42,U_40) )
& rs(U_42,U_41) )
& rr(U_48,U_42) )
| ( ~ cd(sK4(U_48))
& rr(U_48,sK4(U_48)) ) )
& ! [U_47] :
( ( sK2(U_47) != sK3(U_47)
& rs(sK1(U_47),sK3(U_47))
& rs(sK1(U_47),sK2(U_47))
& rr(U_47,sK1(U_47))
& ! [U_35] :
( cc(U_35)
| ! [U_34] :
( ! [U_33] :
( U_34 = U_33
| ~ rs(U_35,U_33) )
| ~ rs(U_35,U_34) )
| ~ rr(U_47,U_35) )
& ! [U_32] :
( cd(U_32)
| ~ rr(U_47,U_32) ) )
| ~ cUnsatisfiable(U_47) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4]),skolemize(U_39,sK4(U_48))],[f_14_6]) ).
fof(f_14_8,plain,
( ! [U_48] :
( cUnsatisfiable(U_48)
| ! [U_45] :
( ! [U_44,U_43] :
( U_44 = U_43
| ~ rs(U_45,U_43)
| ~ rs(U_45,U_44) )
| ~ rr(U_48,U_45) )
| ( ~ cc(sK5(U_48))
& ? [U_41] :
( ? [U_40] :
( U_41 != U_40
& rs(sK5(U_48),U_40) )
& rs(sK5(U_48),U_41) )
& rr(U_48,sK5(U_48)) )
| ( ~ cd(sK4(U_48))
& rr(U_48,sK4(U_48)) ) )
& ! [U_47] :
( ( sK2(U_47) != sK3(U_47)
& rs(sK1(U_47),sK3(U_47))
& rs(sK1(U_47),sK2(U_47))
& rr(U_47,sK1(U_47))
& ! [U_35] :
( cc(U_35)
| ! [U_34] :
( ! [U_33] :
( U_34 = U_33
| ~ rs(U_35,U_33) )
| ~ rs(U_35,U_34) )
| ~ rr(U_47,U_35) )
& ! [U_32] :
( cd(U_32)
| ~ rr(U_47,U_32) ) )
| ~ cUnsatisfiable(U_47) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK5]),skolemize(U_42,sK5(U_48))],[f_14_7]) ).
fof(f_14_9,plain,
( ! [U_48] :
( cUnsatisfiable(U_48)
| ! [U_45] :
( ! [U_44,U_43] :
( U_44 = U_43
| ~ rs(U_45,U_43)
| ~ rs(U_45,U_44) )
| ~ rr(U_48,U_45) )
| ( ~ cc(sK5(U_48))
& ? [U_40] :
( sK6(U_48) != U_40
& rs(sK5(U_48),U_40) )
& rs(sK5(U_48),sK6(U_48))
& rr(U_48,sK5(U_48)) )
| ( ~ cd(sK4(U_48))
& rr(U_48,sK4(U_48)) ) )
& ! [U_47] :
( ( sK2(U_47) != sK3(U_47)
& rs(sK1(U_47),sK3(U_47))
& rs(sK1(U_47),sK2(U_47))
& rr(U_47,sK1(U_47))
& ! [U_35] :
( cc(U_35)
| ! [U_34] :
( ! [U_33] :
( U_34 = U_33
| ~ rs(U_35,U_33) )
| ~ rs(U_35,U_34) )
| ~ rr(U_47,U_35) )
& ! [U_32] :
( cd(U_32)
| ~ rr(U_47,U_32) ) )
| ~ cUnsatisfiable(U_47) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK6]),skolemize(U_41,sK6(U_48))],[f_14_8]) ).
fof(f_14_10,plain,
( ! [U_48] :
( cUnsatisfiable(U_48)
| ! [U_45] :
( ! [U_44,U_43] :
( U_44 = U_43
| ~ rs(U_45,U_43)
| ~ rs(U_45,U_44) )
| ~ rr(U_48,U_45) )
| ( ~ cc(sK5(U_48))
& sK6(U_48) != sK7(U_48)
& rs(sK5(U_48),sK7(U_48))
& rs(sK5(U_48),sK6(U_48))
& rr(U_48,sK5(U_48)) )
| ( ~ cd(sK4(U_48))
& rr(U_48,sK4(U_48)) ) )
& ! [U_47] :
( ( sK2(U_47) != sK3(U_47)
& rs(sK1(U_47),sK3(U_47))
& rs(sK1(U_47),sK2(U_47))
& rr(U_47,sK1(U_47))
& ! [U_35] :
( cc(U_35)
| ! [U_34] :
( ! [U_33] :
( U_34 = U_33
| ~ rs(U_35,U_33) )
| ~ rs(U_35,U_34) )
| ~ rr(U_47,U_35) )
& ! [U_32] :
( cd(U_32)
| ~ rr(U_47,U_32) ) )
| ~ cUnsatisfiable(U_47) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK7]),skolemize(U_40,sK7(U_48))],[f_14_9]) ).
fof(f_14_11,plain,
( ! [U_48] :
( ~ cc(sK5(U_48))
| ~ sP2(U_48) )
& ! [U_48] :
( sK6(U_48) != sK7(U_48)
| ~ sP2(U_48) )
& ! [U_48] :
( rs(sK5(U_48),sK7(U_48))
| ~ sP2(U_48) )
& ! [U_48] :
( rs(sK5(U_48),sK6(U_48))
| ~ sP2(U_48) )
& ! [U_48] :
( rr(U_48,sK5(U_48))
| ~ sP2(U_48) )
& ! [U_48] :
( ~ cd(sK4(U_48))
| ~ sP1(U_48) )
& ! [U_48] :
( rr(U_48,sK4(U_48))
| ~ sP1(U_48) )
& ! [U_32,U_47,U_34,U_35,U_33] :
( sK2(U_47) != sK3(U_47)
| ~ sP0(U_32,U_47,U_34,U_35,U_33) )
& ! [U_32,U_47,U_34,U_35,U_33] :
( rs(sK1(U_47),sK3(U_47))
| ~ sP0(U_32,U_47,U_34,U_35,U_33) )
& ! [U_32,U_47,U_34,U_35,U_33] :
( rs(sK1(U_47),sK2(U_47))
| ~ sP0(U_32,U_47,U_34,U_35,U_33) )
& ! [U_32,U_47,U_34,U_35,U_33] :
( rr(U_47,sK1(U_47))
| ~ sP0(U_32,U_47,U_34,U_35,U_33) )
& ! [U_32,U_47,U_34,U_35,U_33] :
( cc(U_35)
| U_34 = U_33
| ~ rs(U_35,U_33)
| ~ rs(U_35,U_34)
| ~ rr(U_47,U_35)
| ~ sP0(U_32,U_47,U_34,U_35,U_33) )
& ! [U_32,U_47,U_34,U_35,U_33] :
( cd(U_32)
| ~ rr(U_47,U_32)
| ~ sP0(U_32,U_47,U_34,U_35,U_33) )
& ! [U_48,U_45,U_43,U_44] :
( cUnsatisfiable(U_48)
| U_44 = U_43
| ~ rs(U_45,U_43)
| ~ rs(U_45,U_44)
| ~ rr(U_48,U_45)
| sP2(U_48)
| sP1(U_48) )
& ! [U_32,U_47,U_34,U_35,U_33] :
( sP0(U_32,U_47,U_34,U_35,U_33)
| ~ cUnsatisfiable(U_47) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP0,sP1,sP2])],[f_14_10]) ).
cnf(f_14_12,plain,
( sP0(U_32,U_47,U_34,U_35,U_33)
| ~ cUnsatisfiable(U_47) ),
inference(clausify,[status(thm)],[f_14_11]) ).
cnf(f_14_14,plain,
( cd(U_32)
| ~ rr(U_47,U_32)
| ~ sP0(U_32,U_47,U_34,U_35,U_33) ),
inference(clausify,[status(thm)],[f_14_11]) ).
cnf(f_14_15,plain,
( cc(U_35)
| U_34 = U_33
| ~ rs(U_35,U_33)
| ~ rs(U_35,U_34)
| ~ rr(U_47,U_35)
| ~ sP0(U_32,U_47,U_34,U_35,U_33) ),
inference(clausify,[status(thm)],[f_14_11]) ).
cnf(f_14_16,plain,
( rr(U_47,sK1(U_47))
| ~ sP0(U_32,U_47,U_34,U_35,U_33) ),
inference(clausify,[status(thm)],[f_14_11]) ).
cnf(f_14_17,plain,
( rs(sK1(U_47),sK2(U_47))
| ~ sP0(U_32,U_47,U_34,U_35,U_33) ),
inference(clausify,[status(thm)],[f_14_11]) ).
cnf(f_14_18,plain,
( rs(sK1(U_47),sK3(U_47))
| ~ sP0(U_32,U_47,U_34,U_35,U_33) ),
inference(clausify,[status(thm)],[f_14_11]) ).
cnf(f_14_19,plain,
( sK2(U_47) != sK3(U_47)
| ~ sP0(U_32,U_47,U_34,U_35,U_33) ),
inference(clausify,[status(thm)],[f_14_11]) ).
fof(f_15_1,plain,
! [X] :
( ~ cd(X)
| ~ cc(X) ),
inference(fof_nnf,[status(thm)],[axiom_3]) ).
fof(f_15_2,plain,
! [U_49] :
( ~ cd(U_49)
| ~ cc(U_49) ),
inference(variable_rename,[status(thm)],[f_15_1]) ).
fof(f_15_3,plain,
! [U_49] :
( ~ cd(U_49)
| ~ cc(U_49) ),
inference(definitional_conversion,[status(esa)],[f_15_2]) ).
cnf(f_15_4,plain,
( ~ cd(U_49)
| ~ cc(U_49) ),
inference(clausify,[status(thm)],[f_15_3]) ).
fof(f_16_1,plain,
cUnsatisfiable(i2003_11_14_17_20_36582),
inference(fof_nnf,[status(thm)],[axiom_4]) ).
fof(f_16_2,plain,
cUnsatisfiable(i2003_11_14_17_20_36582),
inference(definitional_conversion,[status(esa)],[f_16_1]) ).
cnf(f_16_3,plain,
cUnsatisfiable(i2003_11_14_17_20_36582),
inference(clausify,[status(thm)],[f_16_2]) ).
cnf(t1,plain,
( ~ cd(sK1(i2003_11_14_17_20_36582))
| ~ cc(sK1(i2003_11_14_17_20_36582)) ),
inference(start,[status(thm),parent(0:0)],[f_15_4]) ).
cnf(t2,plain,
( ~ rr(i2003_11_14_17_20_36582,sK1(i2003_11_14_17_20_36582))
| ~ rs(sK1(i2003_11_14_17_20_36582),sK2(i2003_11_14_17_20_36582))
| ~ rs(sK1(i2003_11_14_17_20_36582),sK3(i2003_11_14_17_20_36582))
| sK2(i2003_11_14_17_20_36582) = sK3(i2003_11_14_17_20_36582)
| ~ sP0(U_737,i2003_11_14_17_20_36582,sK2(i2003_11_14_17_20_36582),sK1(i2003_11_14_17_20_36582),sK3(i2003_11_14_17_20_36582))
| cc(sK1(i2003_11_14_17_20_36582)) ),
inference(extension,[status(thm),parent(t1:1)],[f_14_15]) ).
cnf(t3,plain,
$false,
inference(connection,[status(thm),parent(t2:1)],[t2:1,t1:1]) ).
cnf(t4,plain,
( ~ cUnsatisfiable(i2003_11_14_17_20_36582)
| sP0(U_737,i2003_11_14_17_20_36582,sK2(i2003_11_14_17_20_36582),sK1(i2003_11_14_17_20_36582),sK3(i2003_11_14_17_20_36582)) ),
inference(extension,[status(thm),parent(t2:2)],[f_14_12]) ).
cnf(t5,plain,
$false,
inference(connection,[status(thm),parent(t4:1)],[t4:1,t2:2]) ).
cnf(t6,plain,
cUnsatisfiable(i2003_11_14_17_20_36582),
inference(extension,[status(thm),parent(t4:2)],[f_16_3]) ).
cnf(t7,plain,
$false,
inference(connection,[status(thm),parent(t6:1)],[t6:1,t4:2]) ).
cnf(t8,plain,
( ~ sP0(U_747,i2003_11_14_17_20_36582,U_748,U_749,U_750)
| sK2(i2003_11_14_17_20_36582) != sK3(i2003_11_14_17_20_36582) ),
inference(extension,[status(thm),parent(t2:3)],[f_14_19]) ).
cnf(t9,plain,
$false,
inference(connection,[status(thm),parent(t8:1)],[t8:1,t2:3]) ).
cnf(t10,plain,
( ~ cUnsatisfiable(i2003_11_14_17_20_36582)
| sP0(U_747,i2003_11_14_17_20_36582,U_748,U_749,U_750) ),
inference(extension,[status(thm),parent(t8:2)],[f_14_12]) ).
cnf(t11,plain,
$false,
inference(connection,[status(thm),parent(t10:1)],[t10:1,t8:2]) ).
cnf(t12,plain,
cUnsatisfiable(i2003_11_14_17_20_36582),
inference(extension,[status(thm),parent(t10:2)],[f_16_3]) ).
cnf(t13,plain,
$false,
inference(connection,[status(thm),parent(t12:1)],[t12:1,t10:2]) ).
cnf(t14,plain,
( ~ sP0(U_757,i2003_11_14_17_20_36582,U_758,U_759,U_760)
| rs(sK1(i2003_11_14_17_20_36582),sK3(i2003_11_14_17_20_36582)) ),
inference(extension,[status(thm),parent(t2:4)],[f_14_18]) ).
cnf(t15,plain,
$false,
inference(connection,[status(thm),parent(t14:1)],[t14:1,t2:4]) ).
cnf(t16,plain,
( ~ cUnsatisfiable(i2003_11_14_17_20_36582)
| sP0(U_757,i2003_11_14_17_20_36582,U_758,U_759,U_760) ),
inference(extension,[status(thm),parent(t14:2)],[f_14_12]) ).
cnf(t17,plain,
$false,
inference(connection,[status(thm),parent(t16:1)],[t16:1,t14:2]) ).
cnf(t18,plain,
cUnsatisfiable(i2003_11_14_17_20_36582),
inference(extension,[status(thm),parent(t16:2)],[f_16_3]) ).
cnf(t19,plain,
$false,
inference(connection,[status(thm),parent(t18:1)],[t18:1,t16:2]) ).
cnf(t20,plain,
( ~ sP0(U_767,i2003_11_14_17_20_36582,U_768,U_769,U_770)
| rs(sK1(i2003_11_14_17_20_36582),sK2(i2003_11_14_17_20_36582)) ),
inference(extension,[status(thm),parent(t2:5)],[f_14_17]) ).
cnf(t21,plain,
$false,
inference(connection,[status(thm),parent(t20:1)],[t20:1,t2:5]) ).
cnf(t22,plain,
( ~ cUnsatisfiable(i2003_11_14_17_20_36582)
| sP0(U_767,i2003_11_14_17_20_36582,U_768,U_769,U_770) ),
inference(extension,[status(thm),parent(t20:2)],[f_14_12]) ).
cnf(t23,plain,
$false,
inference(connection,[status(thm),parent(t22:1)],[t22:1,t20:2]) ).
cnf(t24,plain,
cUnsatisfiable(i2003_11_14_17_20_36582),
inference(extension,[status(thm),parent(t22:2)],[f_16_3]) ).
cnf(t25,plain,
$false,
inference(connection,[status(thm),parent(t24:1)],[t24:1,t22:2]) ).
cnf(t26,plain,
( ~ sP0(U_777,i2003_11_14_17_20_36582,U_778,U_779,U_780)
| rr(i2003_11_14_17_20_36582,sK1(i2003_11_14_17_20_36582)) ),
inference(extension,[status(thm),parent(t2:6)],[f_14_16]) ).
cnf(t27,plain,
$false,
inference(connection,[status(thm),parent(t26:1)],[t26:1,t2:6]) ).
cnf(t28,plain,
( ~ cUnsatisfiable(i2003_11_14_17_20_36582)
| sP0(U_777,i2003_11_14_17_20_36582,U_778,U_779,U_780) ),
inference(extension,[status(thm),parent(t26:2)],[f_14_12]) ).
cnf(t29,plain,
$false,
inference(connection,[status(thm),parent(t28:1)],[t28:1,t26:2]) ).
cnf(t30,plain,
cUnsatisfiable(i2003_11_14_17_20_36582),
inference(extension,[status(thm),parent(t28:2)],[f_16_3]) ).
cnf(t31,plain,
$false,
inference(connection,[status(thm),parent(t30:1)],[t30:1,t28:2]) ).
cnf(t32,plain,
( ~ rr(i2003_11_14_17_20_36582,sK1(i2003_11_14_17_20_36582))
| ~ sP0(sK1(i2003_11_14_17_20_36582),i2003_11_14_17_20_36582,U_788,U_789,U_790)
| cd(sK1(i2003_11_14_17_20_36582)) ),
inference(extension,[status(thm),parent(t1:2)],[f_14_14]) ).
cnf(t33,plain,
$false,
inference(connection,[status(thm),parent(t32:1)],[t32:1,t1:2]) ).
cnf(t34,plain,
( ~ cUnsatisfiable(i2003_11_14_17_20_36582)
| sP0(sK1(i2003_11_14_17_20_36582),i2003_11_14_17_20_36582,U_788,U_789,U_790) ),
inference(extension,[status(thm),parent(t32:2)],[f_14_12]) ).
cnf(t35,plain,
$false,
inference(connection,[status(thm),parent(t34:1)],[t34:1,t32:2]) ).
cnf(t36,plain,
cUnsatisfiable(i2003_11_14_17_20_36582),
inference(extension,[status(thm),parent(t34:2)],[f_16_3]) ).
cnf(t37,plain,
$false,
inference(connection,[status(thm),parent(t36:1)],[t36:1,t34:2]) ).
cnf(t38,plain,
( ~ sP0(U_797,i2003_11_14_17_20_36582,U_798,U_799,U_800)
| rr(i2003_11_14_17_20_36582,sK1(i2003_11_14_17_20_36582)) ),
inference(extension,[status(thm),parent(t32:3)],[f_14_16]) ).
cnf(t39,plain,
$false,
inference(connection,[status(thm),parent(t38:1)],[t38:1,t32:3]) ).
cnf(t40,plain,
( ~ cUnsatisfiable(i2003_11_14_17_20_36582)
| sP0(U_797,i2003_11_14_17_20_36582,U_798,U_799,U_800) ),
inference(extension,[status(thm),parent(t38:2)],[f_14_12]) ).
cnf(t41,plain,
$false,
inference(connection,[status(thm),parent(t40:1)],[t40:1,t38:2]) ).
cnf(t42,plain,
cUnsatisfiable(i2003_11_14_17_20_36582),
inference(extension,[status(thm),parent(t40:2)],[f_16_3]) ).
cnf(t43,plain,
$false,
inference(connection,[status(thm),parent(t42:1)],[t42:1,t40:2]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : KRS101+1 : TPTP v9.3.1. Released v3.1.0.
% 0.00/0.03 This is a FOF_UNS_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.09/0.36 % Computer : n011.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Sat Sep 19 12:12:26 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.57/0.82 % SZS status Unsatisfiable for theBenchmark
% 0.57/0.82 % SZS output start Proof for theBenchmark
% See solution above
%------------------------------------------------------------------------------