%------------------------------------------------------------------------------
% File : ConnectPP---0.7.2
% Problem : KRS138+1 : TPTP v9.3.1. Released v3.1.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 : 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:47:21 AM UTC 2026
% Result : Theorem 33.36s 33.67s
% Output : Proof 33.36s
% Verified :
% SZS Type : Refutation
% Derivation depth : 16
% Number of leaves : 15
% Syntax : Number of formulae : 207 ( 108 unt; 0 def)
% Number of atoms : 594 ( 129 equ)
% Maximal formula atoms : 30 ( 2 avg)
% Number of connectives : 683 ( 296 ~; 264 |; 112 &)
% ( 4 <=>; 7 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 3 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 13 ( 11 usr; 5 prp; 0-2 aty)
% Number of functors : 11 ( 11 usr; 11 con; 0-0 aty)
% Number of variables : 137 ( 3 sgn 67 !; 48 ?)
% Comments :
%------------------------------------------------------------------------------
fof(requalityOnA_substitution_2,axiom,
! [A,B,C] :
( ( requalityOnA(C,A)
& A = B )
=> requalityOnA(C,B) ),
file('theBenchmark.p',requalityOnA_substitution_2) ).
fof(axiom_0,axiom,
! [X] :
( ~ cowlNothing(X)
& cowlThing(X) ),
file('theBenchmark.p',axiom_0) ).
fof(axiom_1,axiom,
! [X] :
( xsd_string(X)
<=> ~ xsd_integer(X) ),
file('theBenchmark.p',axiom_1) ).
fof(axiom_2,axiom,
! [X] :
( cA(X)
<=> ( X = ia
| X = ib ) ),
file('theBenchmark.p',axiom_2) ).
fof(axiom_3,axiom,
! [X,Y,Z] :
( ( requalityOnA(Z,X)
& requalityOnA(Y,X) )
=> Y = Z ),
file('theBenchmark.p',axiom_3) ).
fof(axiom_4,axiom,
! [X,Y] :
( requalityOnA(X,Y)
=> cA(Y) ),
file('theBenchmark.p',axiom_4) ).
fof(axiom_5,axiom,
cowlThing(ia),
file('theBenchmark.p',axiom_5) ).
fof(axiom_6,axiom,
requalityOnA(ia,ia),
file('theBenchmark.p',axiom_6) ).
fof(axiom_7,axiom,
cowlThing(ib),
file('theBenchmark.p',axiom_7) ).
fof(axiom_8,axiom,
requalityOnA(ib,ib),
file('theBenchmark.p',axiom_8) ).
fof(axiom_9,axiom,
cowlThing(ic),
file('theBenchmark.p',axiom_9) ).
fof(the_axiom,conjecture,
( cowlThing(ic)
& cowlThing(ib)
& requalityOnA(ia,ia)
& cowlThing(ia)
& ! [X,Y] :
( requalityOnA(X,Y)
=> requalityOnA(Y,X) )
& ! [X,Y] :
( requalityOnA(X,Y)
=> ( X = ic
| X = ib
| X = ia ) )
& ! [X] :
( xsd_string(X)
<=> ~ xsd_integer(X) )
& ! [X] :
( ~ cowlNothing(X)
& cowlThing(X) ) ),
file('theBenchmark.p',the_axiom) ).
fof(f_5_1,plain,
! [A,B,C] :
( requalityOnA(C,B)
| ~ requalityOnA(C,A)
| A != B ),
inference(fof_nnf,[status(thm)],[requalityOnA_substitution_2]) ).
fof(f_5_2,plain,
! [U_11,U_10,U_9] :
( requalityOnA(U_9,U_10)
| ~ requalityOnA(U_9,U_11)
| U_11 != U_10 ),
inference(variable_rename,[status(thm)],[f_5_1]) ).
fof(f_5_3,plain,
! [U_11,U_9,U_10] :
( requalityOnA(U_9,U_10)
| ~ requalityOnA(U_9,U_11)
| U_11 != U_10 ),
inference(definitional_conversion,[status(esa)],[f_5_2]) ).
cnf(f_5_4,plain,
( requalityOnA(U_9,U_10)
| ~ requalityOnA(U_9,U_11)
| U_11 != U_10 ),
inference(clausify,[status(thm)],[f_5_3]) ).
fof(f_8_1,plain,
! [X] :
( ~ cowlNothing(X)
& cowlThing(X) ),
inference(fof_nnf,[status(thm)],[axiom_0]) ).
fof(f_8_2,plain,
! [U_16] :
( ~ cowlNothing(U_16)
& cowlThing(U_16) ),
inference(variable_rename,[status(thm)],[f_8_1]) ).
fof(f_8_3,plain,
( ! [U_18] : ~ cowlNothing(U_18)
& ! [U_17] : cowlThing(U_17) ),
inference(miniscope,[status(thm)],[f_8_2]) ).
fof(f_8_4,plain,
( ! [U_18] : ~ cowlNothing(U_18)
& ! [U_17] : cowlThing(U_17) ),
inference(definitional_conversion,[status(esa)],[f_8_3]) ).
cnf(f_8_5,plain,
cowlThing(U_17),
inference(clausify,[status(thm)],[f_8_4]) ).
cnf(f_8_6,plain,
~ cowlNothing(U_18),
inference(clausify,[status(thm)],[f_8_4]) ).
fof(f_9_1,plain,
! [X] :
( ( xsd_string(X)
| xsd_integer(X) )
& ( ~ xsd_integer(X)
| ~ xsd_string(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_1]) ).
fof(f_9_2,plain,
! [U_19] :
( ( xsd_string(U_19)
| xsd_integer(U_19) )
& ( ~ xsd_integer(U_19)
| ~ xsd_string(U_19) ) ),
inference(variable_rename,[status(thm)],[f_9_1]) ).
fof(f_9_3,plain,
( ! [U_21] :
( xsd_string(U_21)
| xsd_integer(U_21) )
& ! [U_20] :
( ~ xsd_integer(U_20)
| ~ xsd_string(U_20) ) ),
inference(miniscope,[status(thm)],[f_9_2]) ).
fof(f_9_4,plain,
( ! [U_21] :
( xsd_string(U_21)
| xsd_integer(U_21) )
& ! [U_20] :
( ~ xsd_integer(U_20)
| ~ xsd_string(U_20) ) ),
inference(definitional_conversion,[status(esa)],[f_9_3]) ).
cnf(f_9_5,plain,
( ~ xsd_integer(U_20)
| ~ xsd_string(U_20) ),
inference(clausify,[status(thm)],[f_9_4]) ).
cnf(f_9_6,plain,
( xsd_string(U_21)
| xsd_integer(U_21) ),
inference(clausify,[status(thm)],[f_9_4]) ).
fof(f_10_1,plain,
! [X] :
( ( cA(X)
| ( X != ia
& X != ib ) )
& ( X = ia
| X = ib
| ~ cA(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_2]) ).
fof(f_10_2,plain,
! [U_22] :
( ( cA(U_22)
| ( U_22 != ia
& U_22 != ib ) )
& ( U_22 = ia
| U_22 = ib
| ~ cA(U_22) ) ),
inference(variable_rename,[status(thm)],[f_10_1]) ).
fof(f_10_3,plain,
( ! [U_24] :
( cA(U_24)
| ( U_24 != ia
& U_24 != ib ) )
& ! [U_23] :
( U_23 = ia
| U_23 = ib
| ~ cA(U_23) ) ),
inference(miniscope,[status(thm)],[f_10_2]) ).
fof(f_10_4,plain,
( ! [U_24] :
( U_24 != ia
| ~ sP0(U_24) )
& ! [U_24] :
( U_24 != ib
| ~ sP0(U_24) )
& ! [U_24] :
( cA(U_24)
| sP0(U_24) )
& ! [U_23] :
( U_23 = ia
| U_23 = ib
| ~ cA(U_23) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP0])],[f_10_3]) ).
cnf(f_10_5,plain,
( U_23 = ia
| U_23 = ib
| ~ cA(U_23) ),
inference(clausify,[status(thm)],[f_10_4]) ).
fof(f_11_1,plain,
! [X,Y,Z] :
( Y = Z
| ~ requalityOnA(Z,X)
| ~ requalityOnA(Y,X) ),
inference(fof_nnf,[status(thm)],[axiom_3]) ).
fof(f_11_2,plain,
! [U_27,U_26,U_25] :
( U_26 = U_25
| ~ requalityOnA(U_25,U_27)
| ~ requalityOnA(U_26,U_27) ),
inference(variable_rename,[status(thm)],[f_11_1]) ).
fof(f_11_3,plain,
! [U_25,U_26,U_27] :
( U_26 = U_25
| ~ requalityOnA(U_25,U_27)
| ~ requalityOnA(U_26,U_27) ),
inference(definitional_conversion,[status(esa)],[f_11_2]) ).
cnf(f_11_4,plain,
( U_26 = U_25
| ~ requalityOnA(U_25,U_27)
| ~ requalityOnA(U_26,U_27) ),
inference(clausify,[status(thm)],[f_11_3]) ).
fof(f_12_1,plain,
! [X,Y] :
( cA(Y)
| ~ requalityOnA(X,Y) ),
inference(fof_nnf,[status(thm)],[axiom_4]) ).
fof(f_12_2,plain,
! [U_29,U_28] :
( cA(U_28)
| ~ requalityOnA(U_29,U_28) ),
inference(variable_rename,[status(thm)],[f_12_1]) ).
fof(f_12_3,plain,
! [U_29,U_28] :
( cA(U_28)
| ~ requalityOnA(U_29,U_28) ),
inference(definitional_conversion,[status(esa)],[f_12_2]) ).
cnf(f_12_4,plain,
( cA(U_28)
| ~ requalityOnA(U_29,U_28) ),
inference(clausify,[status(thm)],[f_12_3]) ).
fof(f_13_1,plain,
cowlThing(ia),
inference(fof_nnf,[status(thm)],[axiom_5]) ).
fof(f_13_2,plain,
cowlThing(ia),
inference(definitional_conversion,[status(esa)],[f_13_1]) ).
cnf(f_13_3,plain,
cowlThing(ia),
inference(clausify,[status(thm)],[f_13_2]) ).
fof(f_14_1,plain,
requalityOnA(ia,ia),
inference(fof_nnf,[status(thm)],[axiom_6]) ).
fof(f_14_2,plain,
requalityOnA(ia,ia),
inference(definitional_conversion,[status(esa)],[f_14_1]) ).
cnf(f_14_3,plain,
requalityOnA(ia,ia),
inference(clausify,[status(thm)],[f_14_2]) ).
fof(f_15_1,plain,
cowlThing(ib),
inference(fof_nnf,[status(thm)],[axiom_7]) ).
fof(f_15_2,plain,
cowlThing(ib),
inference(definitional_conversion,[status(esa)],[f_15_1]) ).
cnf(f_15_3,plain,
cowlThing(ib),
inference(clausify,[status(thm)],[f_15_2]) ).
fof(f_16_1,plain,
requalityOnA(ib,ib),
inference(fof_nnf,[status(thm)],[axiom_8]) ).
fof(f_16_2,plain,
requalityOnA(ib,ib),
inference(definitional_conversion,[status(esa)],[f_16_1]) ).
cnf(f_16_3,plain,
requalityOnA(ib,ib),
inference(clausify,[status(thm)],[f_16_2]) ).
fof(f_17_1,plain,
cowlThing(ic),
inference(fof_nnf,[status(thm)],[axiom_9]) ).
fof(f_17_2,plain,
cowlThing(ic),
inference(definitional_conversion,[status(esa)],[f_17_1]) ).
cnf(f_17_3,plain,
cowlThing(ic),
inference(clausify,[status(thm)],[f_17_2]) ).
fof(f_18_1,negated_conjecture,
~ ( cowlThing(ic)
& cowlThing(ib)
& requalityOnA(ia,ia)
& cowlThing(ia)
& ! [X,Y] :
( requalityOnA(X,Y)
=> requalityOnA(Y,X) )
& ! [X,Y] :
( requalityOnA(X,Y)
=> ( X = ic
| X = ib
| X = ia ) )
& ! [X] :
( xsd_string(X)
<=> ~ xsd_integer(X) )
& ! [X] :
( ~ cowlNothing(X)
& cowlThing(X) ) ),
inference(negate,[status(cth)],[the_axiom]) ).
fof(f_18_2,negated_conjecture,
( ~ cowlThing(ic)
| ~ cowlThing(ib)
| ~ requalityOnA(ia,ia)
| ~ cowlThing(ia)
| ? [X,Y] :
( ~ requalityOnA(Y,X)
& requalityOnA(X,Y) )
| ? [X,Y] :
( X != ic
& X != ib
& X != ia
& requalityOnA(X,Y) )
| ? [X] :
( ( ~ xsd_string(X)
& ~ xsd_integer(X) )
| ( xsd_integer(X)
& xsd_string(X) ) )
| ? [X] :
( cowlNothing(X)
| ~ cowlThing(X) ) ),
inference(fof_nnf,[status(thm)],[f_18_1]) ).
fof(f_18_3,negated_conjecture,
( ~ cowlThing(ic)
| ~ cowlThing(ib)
| ~ requalityOnA(ia,ia)
| ~ cowlThing(ia)
| ? [U_35,U_34] :
( ~ requalityOnA(U_34,U_35)
& requalityOnA(U_35,U_34) )
| ? [U_33,U_32] :
( U_33 != ic
& U_33 != ib
& U_33 != ia
& requalityOnA(U_33,U_32) )
| ? [U_31] :
( ( ~ xsd_string(U_31)
& ~ xsd_integer(U_31) )
| ( xsd_integer(U_31)
& xsd_string(U_31) ) )
| ? [U_30] :
( cowlNothing(U_30)
| ~ cowlThing(U_30) ) ),
inference(variable_rename,[status(thm)],[f_18_2]) ).
fof(f_18_4,negated_conjecture,
( ~ cowlThing(ic)
| ~ cowlThing(ib)
| ~ requalityOnA(ia,ia)
| ~ cowlThing(ia)
| ? [U_35,U_34] :
( ~ requalityOnA(U_34,U_35)
& requalityOnA(U_35,U_34) )
| ? [U_33] :
( ? [U_32] : requalityOnA(U_33,U_32)
& U_33 != ic
& U_33 != ib
& U_33 != ia )
| ? [U_39] :
( ~ xsd_string(U_39)
& ~ xsd_integer(U_39) )
| ? [U_38] :
( xsd_integer(U_38)
& xsd_string(U_38) )
| ? [U_37] : cowlNothing(U_37)
| ? [U_36] : ~ cowlThing(U_36) ),
inference(miniscope,[status(thm)],[f_18_3]) ).
fof(f_18_5,negated_conjecture,
( ~ cowlThing(ic)
| ~ cowlThing(ib)
| ~ requalityOnA(ia,ia)
| ~ cowlThing(ia)
| ? [U_35,U_34] :
( ~ requalityOnA(U_34,U_35)
& requalityOnA(U_35,U_34) )
| ? [U_33] :
( ? [U_32] : requalityOnA(U_33,U_32)
& U_33 != ic
& U_33 != ib
& U_33 != ia )
| ? [U_39] :
( ~ xsd_string(U_39)
& ~ xsd_integer(U_39) )
| ? [U_38] :
( xsd_integer(U_38)
& xsd_string(U_38) )
| ? [U_37] : cowlNothing(U_37)
| ~ cowlThing(sK1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1]),skolemize(U_36,sK1)],[f_18_4]) ).
fof(f_18_6,negated_conjecture,
( ~ cowlThing(ic)
| ~ cowlThing(ib)
| ~ requalityOnA(ia,ia)
| ~ cowlThing(ia)
| ? [U_35,U_34] :
( ~ requalityOnA(U_34,U_35)
& requalityOnA(U_35,U_34) )
| ? [U_33] :
( ? [U_32] : requalityOnA(U_33,U_32)
& U_33 != ic
& U_33 != ib
& U_33 != ia )
| ? [U_39] :
( ~ xsd_string(U_39)
& ~ xsd_integer(U_39) )
| ? [U_38] :
( xsd_integer(U_38)
& xsd_string(U_38) )
| cowlNothing(sK2)
| ~ cowlThing(sK1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2]),skolemize(U_37,sK2)],[f_18_5]) ).
fof(f_18_7,negated_conjecture,
( ~ cowlThing(ic)
| ~ cowlThing(ib)
| ~ requalityOnA(ia,ia)
| ~ cowlThing(ia)
| ? [U_35,U_34] :
( ~ requalityOnA(U_34,U_35)
& requalityOnA(U_35,U_34) )
| ? [U_33] :
( ? [U_32] : requalityOnA(U_33,U_32)
& U_33 != ic
& U_33 != ib
& U_33 != ia )
| ? [U_39] :
( ~ xsd_string(U_39)
& ~ xsd_integer(U_39) )
| ( xsd_integer(sK3)
& xsd_string(sK3) )
| cowlNothing(sK2)
| ~ cowlThing(sK1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3]),skolemize(U_38,sK3)],[f_18_6]) ).
fof(f_18_8,negated_conjecture,
( ~ cowlThing(ic)
| ~ cowlThing(ib)
| ~ requalityOnA(ia,ia)
| ~ cowlThing(ia)
| ? [U_35,U_34] :
( ~ requalityOnA(U_34,U_35)
& requalityOnA(U_35,U_34) )
| ? [U_33] :
( ? [U_32] : requalityOnA(U_33,U_32)
& U_33 != ic
& U_33 != ib
& U_33 != ia )
| ( ~ xsd_string(sK4)
& ~ xsd_integer(sK4) )
| ( xsd_integer(sK3)
& xsd_string(sK3) )
| cowlNothing(sK2)
| ~ cowlThing(sK1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4]),skolemize(U_39,sK4)],[f_18_7]) ).
fof(f_18_9,negated_conjecture,
( ~ cowlThing(ic)
| ~ cowlThing(ib)
| ~ requalityOnA(ia,ia)
| ~ cowlThing(ia)
| ? [U_35,U_34] :
( ~ requalityOnA(U_34,U_35)
& requalityOnA(U_35,U_34) )
| ( ? [U_32] : requalityOnA(sK5,U_32)
& sK5 != ic
& sK5 != ib
& sK5 != ia )
| ( ~ xsd_string(sK4)
& ~ xsd_integer(sK4) )
| ( xsd_integer(sK3)
& xsd_string(sK3) )
| cowlNothing(sK2)
| ~ cowlThing(sK1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK5]),skolemize(U_33,sK5)],[f_18_8]) ).
fof(f_18_10,negated_conjecture,
( ~ cowlThing(ic)
| ~ cowlThing(ib)
| ~ requalityOnA(ia,ia)
| ~ cowlThing(ia)
| ? [U_35,U_34] :
( ~ requalityOnA(U_34,U_35)
& requalityOnA(U_35,U_34) )
| ( requalityOnA(sK5,sK6)
& sK5 != ic
& sK5 != ib
& sK5 != ia )
| ( ~ xsd_string(sK4)
& ~ xsd_integer(sK4) )
| ( xsd_integer(sK3)
& xsd_string(sK3) )
| cowlNothing(sK2)
| ~ cowlThing(sK1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK6]),skolemize(U_32,sK6)],[f_18_9]) ).
fof(f_18_11,negated_conjecture,
( ~ cowlThing(ic)
| ~ cowlThing(ib)
| ~ requalityOnA(ia,ia)
| ~ cowlThing(ia)
| ? [U_34] :
( ~ requalityOnA(U_34,sK7)
& requalityOnA(sK7,U_34) )
| ( requalityOnA(sK5,sK6)
& sK5 != ic
& sK5 != ib
& sK5 != ia )
| ( ~ xsd_string(sK4)
& ~ xsd_integer(sK4) )
| ( xsd_integer(sK3)
& xsd_string(sK3) )
| cowlNothing(sK2)
| ~ cowlThing(sK1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK7]),skolemize(U_35,sK7)],[f_18_10]) ).
fof(f_18_12,negated_conjecture,
( ~ cowlThing(ic)
| ~ cowlThing(ib)
| ~ requalityOnA(ia,ia)
| ~ cowlThing(ia)
| ( ~ requalityOnA(sK8,sK7)
& requalityOnA(sK7,sK8) )
| ( requalityOnA(sK5,sK6)
& sK5 != ic
& sK5 != ib
& sK5 != ia )
| ( ~ xsd_string(sK4)
& ~ xsd_integer(sK4) )
| ( xsd_integer(sK3)
& xsd_string(sK3) )
| cowlNothing(sK2)
| ~ cowlThing(sK1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK8]),skolemize(U_34,sK8)],[f_18_11]) ).
fof(f_18_13,negated_conjecture,
( ( ~ requalityOnA(sK8,sK7)
| ~ sP4 )
& ( requalityOnA(sK7,sK8)
| ~ sP4 )
& ( requalityOnA(sK5,sK6)
| ~ sP3 )
& ( sK5 != ic
| ~ sP3 )
& ( sK5 != ib
| ~ sP3 )
& ( sK5 != ia
| ~ sP3 )
& ( ~ xsd_string(sK4)
| ~ sP2 )
& ( ~ xsd_integer(sK4)
| ~ sP2 )
& ( xsd_integer(sK3)
| ~ sP1 )
& ( xsd_string(sK3)
| ~ sP1 )
& ( ~ cowlThing(ic)
| ~ cowlThing(ib)
| ~ requalityOnA(ia,ia)
| ~ cowlThing(ia)
| sP4
| sP3
| sP2
| sP1
| cowlNothing(sK2)
| ~ cowlThing(sK1) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP1,sP2,sP3,sP4])],[f_18_12]) ).
cnf(f_18_14,negated_conjecture,
( ~ cowlThing(ic)
| ~ cowlThing(ib)
| ~ requalityOnA(ia,ia)
| ~ cowlThing(ia)
| sP4
| sP3
| sP2
| sP1
| cowlNothing(sK2)
| ~ cowlThing(sK1) ),
inference(clausify,[status(thm)],[f_18_13]) ).
cnf(f_18_15,negated_conjecture,
( xsd_string(sK3)
| ~ sP1 ),
inference(clausify,[status(thm)],[f_18_13]) ).
cnf(f_18_16,negated_conjecture,
( xsd_integer(sK3)
| ~ sP1 ),
inference(clausify,[status(thm)],[f_18_13]) ).
cnf(f_18_17,negated_conjecture,
( ~ xsd_integer(sK4)
| ~ sP2 ),
inference(clausify,[status(thm)],[f_18_13]) ).
cnf(f_18_18,negated_conjecture,
( ~ xsd_string(sK4)
| ~ sP2 ),
inference(clausify,[status(thm)],[f_18_13]) ).
cnf(f_18_19,negated_conjecture,
( sK5 != ia
| ~ sP3 ),
inference(clausify,[status(thm)],[f_18_13]) ).
cnf(f_18_20,negated_conjecture,
( sK5 != ib
| ~ sP3 ),
inference(clausify,[status(thm)],[f_18_13]) ).
cnf(f_18_22,negated_conjecture,
( requalityOnA(sK5,sK6)
| ~ sP3 ),
inference(clausify,[status(thm)],[f_18_13]) ).
cnf(f_18_23,negated_conjecture,
( requalityOnA(sK7,sK8)
| ~ sP4 ),
inference(clausify,[status(thm)],[f_18_13]) ).
cnf(f_18_24,negated_conjecture,
( ~ requalityOnA(sK8,sK7)
| ~ sP4 ),
inference(clausify,[status(thm)],[f_18_13]) ).
cnf(equality_2,axiom,
( Eq_x_1 = Eq_x_0
| Eq_x_0 != Eq_x_1 ),
theory(equality,[symmetry]) ).
cnf(equality_3,axiom,
( Eq_x_0 = Eq_x_2
| Eq_x_1 != Eq_x_2
| Eq_x_0 != Eq_x_1 ),
theory(equality,[transitivity]) ).
cnf(equality_7,axiom,
( requalityOnA(Eq_y_0,Eq_y_1)
| ~ requalityOnA(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,
( cowlNothing(sK2)
| sP1
| sP2
| sP3
| sP4
| ~ cowlThing(ia)
| ~ requalityOnA(ia,ia)
| ~ cowlThing(ib)
| ~ cowlThing(ic)
| ~ cowlThing(sK1) ),
inference(start,[status(thm),parent(0:0)],[f_18_14]) ).
cnf(t2,plain,
cowlThing(sK1),
inference(extension,[status(thm),parent(t1:1)],[f_8_5]) ).
cnf(t3,plain,
$false,
inference(connection,[status(thm),parent(t2:1)],[t2:1,t1:1]) ).
cnf(t4,plain,
cowlThing(ic),
inference(extension,[status(thm),parent(t1:2)],[f_17_3]) ).
cnf(t5,plain,
$false,
inference(connection,[status(thm),parent(t4:1)],[t4:1,t1:2]) ).
cnf(t6,plain,
cowlThing(ib),
inference(extension,[status(thm),parent(t1:3)],[f_15_3]) ).
cnf(t7,plain,
$false,
inference(connection,[status(thm),parent(t6:1)],[t6:1,t1:3]) ).
cnf(t8,plain,
requalityOnA(ia,ia),
inference(extension,[status(thm),parent(t1:4)],[f_14_3]) ).
cnf(t9,plain,
$false,
inference(connection,[status(thm),parent(t8:1)],[t8:1,t1:4]) ).
cnf(t10,plain,
cowlThing(ia),
inference(extension,[status(thm),parent(t1:5)],[f_13_3]) ).
cnf(t11,plain,
$false,
inference(connection,[status(thm),parent(t10:1)],[t10:1,t1:5]) ).
cnf(t12,plain,
( requalityOnA(sK7,sK8)
| ~ sP4 ),
inference(extension,[status(thm),parent(t1:6)],[f_18_23]) ).
cnf(t13,plain,
$false,
inference(connection,[status(thm),parent(t12:1)],[t12:1,t1:6]) ).
cnf(t14,plain,
( cA(sK8)
| ~ requalityOnA(sK7,sK8) ),
inference(extension,[status(thm),parent(t12:2)],[f_12_4]) ).
cnf(t15,plain,
$false,
inference(connection,[status(thm),parent(t14:1)],[t14:1,t12:2]) ).
cnf(t16,plain,
( sK8 = ib
| sK8 = ia
| ~ cA(sK8) ),
inference(extension,[status(thm),parent(t14:2)],[f_10_5]) ).
cnf(t17,plain,
$false,
inference(connection,[status(thm),parent(t16:1)],[t16:1,t14:2]) ).
cnf(t18,plain,
( ia != sK7
| sK8 = sK7
| sK8 != ia ),
inference(extension,[status(thm),parent(t16:2)],[equality_3]) ).
cnf(t19,plain,
$false,
inference(connection,[status(thm),parent(t18:1)],[t18:1,t16:2]) ).
cnf(t20,plain,
( sK7 = sK8
| sK8 != sK7 ),
inference(extension,[status(thm),parent(t18:2)],[equality_2]) ).
cnf(t21,plain,
$false,
inference(connection,[status(thm),parent(t20:1)],[t20:1,t18:2]) ).
cnf(t22,plain,
( sK8 != sK7
| ~ requalityOnA(sK7,sK8)
| requalityOnA(sK8,sK7)
| sK7 != sK8 ),
inference(extension,[status(thm),parent(t20:2)],[equality_7]) ).
cnf(t23,plain,
$false,
inference(connection,[status(thm),parent(t22:1)],[t22:1,t20:2]) ).
cnf(t24,plain,
( ~ sP4
| ~ requalityOnA(sK8,sK7) ),
inference(extension,[status(thm),parent(t22:2)],[f_18_24]) ).
cnf(t25,plain,
$false,
inference(connection,[status(thm),parent(t24:1)],[t24:1,t22:2]) ).
cnf(t26,plain,
$false,
inference(reduction,[status(thm),parent(t24:2)],[t24:2,t1:6]) ).
cnf(t27,plain,
$false,
inference(reduction,[status(thm),parent(t22:3)],[t22:3,t12:2]) ).
cnf(t28,plain,
$false,
inference(reduction,[status(thm),parent(t22:4)],[t22:4,t18:2]) ).
cnf(t29,plain,
( ~ requalityOnA(sK7,ia)
| ~ requalityOnA(ia,ia)
| ia = sK7 ),
inference(extension,[status(thm),parent(t18:3)],[f_11_4]) ).
cnf(t30,plain,
$false,
inference(connection,[status(thm),parent(t29:1)],[t29:1,t18:3]) ).
cnf(t31,plain,
requalityOnA(ia,ia),
inference(extension,[status(thm),parent(t29:2)],[f_14_3]) ).
cnf(t32,plain,
$false,
inference(connection,[status(thm),parent(t31:1)],[t31:1,t29:2]) ).
cnf(t33,plain,
( ~ requalityOnA(sK7,sK8)
| sK8 != ia
| requalityOnA(sK7,ia) ),
inference(extension,[status(thm),parent(t29:3)],[f_5_4]) ).
cnf(t34,plain,
$false,
inference(connection,[status(thm),parent(t33:1)],[t33:1,t29:3]) ).
cnf(t35,plain,
$false,
inference(reduction,[status(thm),parent(t33:2)],[t33:2,t16:2]) ).
cnf(t36,plain,
$false,
inference(reduction,[status(thm),parent(t33:3)],[t33:3,t12:2]) ).
cnf(t37,plain,
( ib != sK7
| sK8 = sK7
| sK8 != ib ),
inference(extension,[status(thm),parent(t16:3)],[equality_3]) ).
cnf(t38,plain,
$false,
inference(connection,[status(thm),parent(t37:1)],[t37:1,t16:3]) ).
cnf(t39,plain,
( sK7 = sK8
| sK8 != sK7 ),
inference(extension,[status(thm),parent(t37:2)],[equality_2]) ).
cnf(t40,plain,
$false,
inference(connection,[status(thm),parent(t39:1)],[t39:1,t37:2]) ).
cnf(t41,plain,
( sK8 != sK7
| ~ requalityOnA(sK7,sK8)
| requalityOnA(sK8,sK7)
| sK7 != sK8 ),
inference(extension,[status(thm),parent(t39:2)],[equality_7]) ).
cnf(t42,plain,
$false,
inference(connection,[status(thm),parent(t41:1)],[t41:1,t39:2]) ).
cnf(t43,plain,
( ~ sP4
| ~ requalityOnA(sK8,sK7) ),
inference(extension,[status(thm),parent(t41:2)],[f_18_24]) ).
cnf(t44,plain,
$false,
inference(connection,[status(thm),parent(t43:1)],[t43:1,t41:2]) ).
cnf(t45,plain,
$false,
inference(reduction,[status(thm),parent(t43:2)],[t43:2,t1:6]) ).
cnf(t46,plain,
$false,
inference(reduction,[status(thm),parent(t41:3)],[t41:3,t12:2]) ).
cnf(t47,plain,
$false,
inference(reduction,[status(thm),parent(t41:4)],[t41:4,t37:2]) ).
cnf(t48,plain,
( ~ requalityOnA(sK7,ib)
| ~ requalityOnA(ib,ib)
| ib = sK7 ),
inference(extension,[status(thm),parent(t37:3)],[f_11_4]) ).
cnf(t49,plain,
$false,
inference(connection,[status(thm),parent(t48:1)],[t48:1,t37:3]) ).
cnf(t50,plain,
requalityOnA(ib,ib),
inference(extension,[status(thm),parent(t48:2)],[f_16_3]) ).
cnf(t51,plain,
$false,
inference(connection,[status(thm),parent(t50:1)],[t50:1,t48:2]) ).
cnf(t52,plain,
( ~ requalityOnA(sK7,sK8)
| sK8 != ib
| requalityOnA(sK7,ib) ),
inference(extension,[status(thm),parent(t48:3)],[f_5_4]) ).
cnf(t53,plain,
$false,
inference(connection,[status(thm),parent(t52:1)],[t52:1,t48:3]) ).
cnf(t54,plain,
$false,
inference(reduction,[status(thm),parent(t52:2)],[t52:2,t16:3]) ).
cnf(t55,plain,
$false,
inference(reduction,[status(thm),parent(t52:3)],[t52:3,t12:2]) ).
cnf(t56,plain,
( requalityOnA(sK5,sK6)
| ~ sP3 ),
inference(extension,[status(thm),parent(t1:7)],[f_18_22]) ).
cnf(t57,plain,
$false,
inference(connection,[status(thm),parent(t56:1)],[t56:1,t1:7]) ).
cnf(t58,plain,
( cA(sK6)
| ~ requalityOnA(sK5,sK6) ),
inference(extension,[status(thm),parent(t56:2)],[f_12_4]) ).
cnf(t59,plain,
$false,
inference(connection,[status(thm),parent(t58:1)],[t58:1,t56:2]) ).
cnf(t60,plain,
( sK6 = ib
| sK6 = ia
| ~ cA(sK6) ),
inference(extension,[status(thm),parent(t58:2)],[f_10_5]) ).
cnf(t61,plain,
$false,
inference(connection,[status(thm),parent(t60:1)],[t60:1,t58:2]) ).
cnf(t62,plain,
( requalityOnA(ia,ia)
| ~ requalityOnA(sK6,sK6)
| sK6 != ia
| sK6 != ia ),
inference(extension,[status(thm),parent(t60:2)],[equality_7]) ).
cnf(t63,plain,
$false,
inference(connection,[status(thm),parent(t62:1)],[t62:1,t60:2]) ).
cnf(t64,plain,
$false,
inference(reduction,[status(thm),parent(t62:2)],[t62:2,t60:2]) ).
cnf(t65,plain,
( ia != sK6
| ~ requalityOnA(ia,ia)
| ia != sK6
| requalityOnA(sK6,sK6) ),
inference(extension,[status(thm),parent(t62:3)],[equality_7]) ).
cnf(t66,plain,
$false,
inference(connection,[status(thm),parent(t65:1)],[t65:1,t62:3]) ).
cnf(t67,plain,
( sK6 != ia
| ia = sK6 ),
inference(extension,[status(thm),parent(t65:2)],[equality_2]) ).
cnf(t68,plain,
$false,
inference(connection,[status(thm),parent(t67:1)],[t67:1,t65:2]) ).
cnf(t69,plain,
$false,
inference(reduction,[status(thm),parent(t67:2)],[t67:2,t60:2]) ).
cnf(l39,lemma,
ia = sK6,
inference(lemma,[status(cth),parent(t65:2),below(t62:3)],[t65:2]) ).
cnf(t70,plain,
requalityOnA(ia,ia),
inference(extension,[status(thm),parent(t65:3)],[f_14_3]) ).
cnf(t71,plain,
$false,
inference(connection,[status(thm),parent(t70:1)],[t70:1,t65:3]) ).
cnf(t72,plain,
ia = sK6,
inference(lemma_extension,[status(thm),parent(t65:4)],[l39:1]) ).
cnf(t73,plain,
$false,
inference(connection,[status(thm),parent(t72:1)],[t72:1,t65:4]) ).
cnf(t74,plain,
( ~ requalityOnA(sK5,ia)
| ia = sK5
| ~ requalityOnA(ia,ia) ),
inference(extension,[status(thm),parent(t62:4)],[f_11_4]) ).
cnf(t75,plain,
$false,
inference(connection,[status(thm),parent(t74:1)],[t74:1,t62:4]) ).
cnf(t76,plain,
( sK5 = ia
| ia != sK5 ),
inference(extension,[status(thm),parent(t74:2)],[equality_2]) ).
cnf(t77,plain,
$false,
inference(connection,[status(thm),parent(t76:1)],[t76:1,t74:2]) ).
cnf(t78,plain,
( ~ sP3
| sK5 != ia ),
inference(extension,[status(thm),parent(t76:2)],[f_18_19]) ).
cnf(t79,plain,
$false,
inference(connection,[status(thm),parent(t78:1)],[t78:1,t76:2]) ).
cnf(t80,plain,
$false,
inference(reduction,[status(thm),parent(t78:2)],[t78:2,t1:7]) ).
cnf(t81,plain,
( ~ requalityOnA(sK5,sK6)
| sK6 != ia
| requalityOnA(sK5,ia) ),
inference(extension,[status(thm),parent(t74:3)],[f_5_4]) ).
cnf(t82,plain,
$false,
inference(connection,[status(thm),parent(t81:1)],[t81:1,t74:3]) ).
cnf(t83,plain,
$false,
inference(reduction,[status(thm),parent(t81:2)],[t81:2,t60:2]) ).
cnf(t84,plain,
$false,
inference(reduction,[status(thm),parent(t81:3)],[t81:3,t56:2]) ).
cnf(t85,plain,
( requalityOnA(ib,ib)
| ~ requalityOnA(sK6,sK6)
| sK6 != ib
| sK6 != ib ),
inference(extension,[status(thm),parent(t60:3)],[equality_7]) ).
cnf(t86,plain,
$false,
inference(connection,[status(thm),parent(t85:1)],[t85:1,t60:3]) ).
cnf(t87,plain,
$false,
inference(reduction,[status(thm),parent(t85:2)],[t85:2,t60:3]) ).
cnf(t88,plain,
( ib != sK6
| ~ requalityOnA(ib,ib)
| ib != sK6
| requalityOnA(sK6,sK6) ),
inference(extension,[status(thm),parent(t85:3)],[equality_7]) ).
cnf(t89,plain,
$false,
inference(connection,[status(thm),parent(t88:1)],[t88:1,t85:3]) ).
cnf(t90,plain,
( sK6 != ib
| ib = sK6 ),
inference(extension,[status(thm),parent(t88:2)],[equality_2]) ).
cnf(t91,plain,
$false,
inference(connection,[status(thm),parent(t90:1)],[t90:1,t88:2]) ).
cnf(t92,plain,
$false,
inference(reduction,[status(thm),parent(t90:2)],[t90:2,t60:3]) ).
cnf(l52,lemma,
ib = sK6,
inference(lemma,[status(cth),parent(t88:2),below(t85:3)],[t88:2]) ).
cnf(t93,plain,
requalityOnA(ib,ib),
inference(extension,[status(thm),parent(t88:3)],[f_16_3]) ).
cnf(t94,plain,
$false,
inference(connection,[status(thm),parent(t93:1)],[t93:1,t88:3]) ).
cnf(t95,plain,
ib = sK6,
inference(lemma_extension,[status(thm),parent(t88:4)],[l52:1]) ).
cnf(t96,plain,
$false,
inference(connection,[status(thm),parent(t95:1)],[t95:1,t88:4]) ).
cnf(t97,plain,
( ~ requalityOnA(sK5,ib)
| ib = sK5
| ~ requalityOnA(ib,ib) ),
inference(extension,[status(thm),parent(t85:4)],[f_11_4]) ).
cnf(t98,plain,
$false,
inference(connection,[status(thm),parent(t97:1)],[t97:1,t85:4]) ).
cnf(t99,plain,
( sK5 = ib
| ib != sK5 ),
inference(extension,[status(thm),parent(t97:2)],[equality_2]) ).
cnf(t100,plain,
$false,
inference(connection,[status(thm),parent(t99:1)],[t99:1,t97:2]) ).
cnf(t101,plain,
( ~ sP3
| sK5 != ib ),
inference(extension,[status(thm),parent(t99:2)],[f_18_20]) ).
cnf(t102,plain,
$false,
inference(connection,[status(thm),parent(t101:1)],[t101:1,t99:2]) ).
cnf(t103,plain,
$false,
inference(reduction,[status(thm),parent(t101:2)],[t101:2,t1:7]) ).
cnf(t104,plain,
( ~ requalityOnA(sK5,sK6)
| sK6 != ib
| requalityOnA(sK5,ib) ),
inference(extension,[status(thm),parent(t97:3)],[f_5_4]) ).
cnf(t105,plain,
$false,
inference(connection,[status(thm),parent(t104:1)],[t104:1,t97:3]) ).
cnf(t106,plain,
$false,
inference(reduction,[status(thm),parent(t104:2)],[t104:2,t60:3]) ).
cnf(t107,plain,
$false,
inference(reduction,[status(thm),parent(t104:3)],[t104:3,t56:2]) ).
cnf(t108,plain,
( ~ xsd_string(sK4)
| ~ sP2 ),
inference(extension,[status(thm),parent(t1:8)],[f_18_18]) ).
cnf(t109,plain,
$false,
inference(connection,[status(thm),parent(t108:1)],[t108:1,t1:8]) ).
cnf(t110,plain,
( xsd_integer(sK4)
| xsd_string(sK4) ),
inference(extension,[status(thm),parent(t108:2)],[f_9_6]) ).
cnf(t111,plain,
$false,
inference(connection,[status(thm),parent(t110:1)],[t110:1,t108:2]) ).
cnf(t112,plain,
( ~ sP2
| ~ xsd_integer(sK4) ),
inference(extension,[status(thm),parent(t110:2)],[f_18_17]) ).
cnf(t113,plain,
$false,
inference(connection,[status(thm),parent(t112:1)],[t112:1,t110:2]) ).
cnf(t114,plain,
$false,
inference(reduction,[status(thm),parent(t112:2)],[t112:2,t1:8]) ).
cnf(t115,plain,
( xsd_integer(sK3)
| ~ sP1 ),
inference(extension,[status(thm),parent(t1:9)],[f_18_16]) ).
cnf(t116,plain,
$false,
inference(connection,[status(thm),parent(t115:1)],[t115:1,t1:9]) ).
cnf(t117,plain,
( ~ xsd_string(sK3)
| ~ xsd_integer(sK3) ),
inference(extension,[status(thm),parent(t115:2)],[f_9_5]) ).
cnf(t118,plain,
$false,
inference(connection,[status(thm),parent(t117:1)],[t117:1,t115:2]) ).
cnf(t119,plain,
( ~ sP1
| xsd_string(sK3) ),
inference(extension,[status(thm),parent(t117:2)],[f_18_15]) ).
cnf(t120,plain,
$false,
inference(connection,[status(thm),parent(t119:1)],[t119:1,t117:2]) ).
cnf(t121,plain,
$false,
inference(reduction,[status(thm),parent(t119:2)],[t119:2,t1:9]) ).
cnf(t122,plain,
~ cowlNothing(sK2),
inference(extension,[status(thm),parent(t1:10)],[f_8_6]) ).
cnf(t123,plain,
$false,
inference(connection,[status(thm),parent(t122:1)],[t122:1,t1:10]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : KRS138+1 : TPTP v9.3.1. Released v3.1.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.08/0.36 % Computer : n018.cluster.edu
% 0.08/0.36 % Model : x86_64 x86_64
% 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36 % Memory : 8046.5625MB
% 0.08/0.36 % OS : Linux 6.8.0-71-generic
% 0.08/0.36 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.08/0.36 % DateTime : Sat Sep 19 12:17:56 UTC 2026
% 0.08/0.36 % CPUTime :
% 33.36/33.67 % SZS status Theorem for theBenchmark
% 33.36/33.67 % SZS output start Proof for theBenchmark
% See solution above
%------------------------------------------------------------------------------