%------------------------------------------------------------------------------
% File : ConnectPP---0.7.2
% Problem : SEU208+1 : TPTP v9.3.1. Released v3.3.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 : n001.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:58:29 AM UTC 2026
% Result : Theorem 79.55s 79.82s
% Output : Proof 79.55s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 6
% Syntax : Number of formulae : 193 ( 122 unt; 0 def)
% Number of atoms : 532 ( 96 equ)
% Maximal formula atoms : 15 ( 2 avg)
% Number of connectives : 562 ( 223 ~; 224 |; 105 &)
% ( 6 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 3 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-2 aty)
% Number of functors : 15 ( 15 usr; 4 con; 0-4 aty)
% Number of variables : 199 ( 1 sgn 121 !; 50 ?)
% Comments :
%------------------------------------------------------------------------------
fof(d14_relat_1,axiom,
! [A] :
( relation(A)
=> ! [B,C] :
( C = relation_inverse_image(A,B)
<=> ! [D] :
( in(D,C)
<=> ? [E] :
( in(E,B)
& in(ordered_pair(D,E),A) ) ) ) ),
file('theBenchmark.p',d14_relat_1) ).
fof(d5_relat_1,axiom,
! [A] :
( relation(A)
=> ! [B] :
( B = relation_rng(A)
<=> ! [C] :
( in(C,B)
<=> ? [D] : in(ordered_pair(D,C),A) ) ) ),
file('theBenchmark.p',d5_relat_1) ).
fof(t166_relat_1,conjecture,
! [A,B,C] :
( relation(C)
=> ( in(A,relation_inverse_image(C,B))
<=> ? [D] :
( in(D,B)
& in(ordered_pair(A,D),C)
& in(D,relation_rng(C)) ) ) ),
file('theBenchmark.p',t166_relat_1) ).
fof(f_4_1,plain,
! [A] :
( ! [B,C] :
( ( C = relation_inverse_image(A,B)
| ? [D] :
( ( ~ in(D,C)
& ? [E] :
( in(E,B)
& in(ordered_pair(D,E),A) ) )
| ( ! [E] :
( ~ in(E,B)
| ~ in(ordered_pair(D,E),A) )
& in(D,C) ) ) )
& ( ! [D] :
( ( in(D,C)
| ! [E] :
( ~ in(E,B)
| ~ in(ordered_pair(D,E),A) ) )
& ( ? [E] :
( in(E,B)
& in(ordered_pair(D,E),A) )
| ~ in(D,C) ) )
| C != relation_inverse_image(A,B) ) )
| ~ relation(A) ),
inference(fof_nnf,[status(thm)],[d14_relat_1]) ).
fof(f_4_2,plain,
! [U_13] :
( ! [U_12,U_11] :
( ( U_11 = relation_inverse_image(U_13,U_12)
| ? [U_10] :
( ( ~ in(U_10,U_11)
& ? [U_9] :
( in(U_9,U_12)
& in(ordered_pair(U_10,U_9),U_13) ) )
| ( ! [U_8] :
( ~ in(U_8,U_12)
| ~ in(ordered_pair(U_10,U_8),U_13) )
& in(U_10,U_11) ) ) )
& ( ! [U_7] :
( ( in(U_7,U_11)
| ! [U_6] :
( ~ in(U_6,U_12)
| ~ in(ordered_pair(U_7,U_6),U_13) ) )
& ( ? [U_5] :
( in(U_5,U_12)
& in(ordered_pair(U_7,U_5),U_13) )
| ~ in(U_7,U_11) ) )
| U_11 != relation_inverse_image(U_13,U_12) ) )
| ~ relation(U_13) ),
inference(variable_rename,[status(thm)],[f_4_1]) ).
fof(f_4_3,plain,
! [U_13] :
( ( ! [U_21,U_19] :
( U_19 = relation_inverse_image(U_13,U_21)
| ? [U_17] :
( ~ in(U_17,U_19)
& ? [U_9] :
( in(U_9,U_21)
& in(ordered_pair(U_17,U_9),U_13) ) )
| ? [U_16] :
( ! [U_8] :
( ~ in(U_8,U_21)
| ~ in(ordered_pair(U_16,U_8),U_13) )
& in(U_16,U_19) ) )
& ! [U_20,U_18] :
( ( ! [U_15] :
( in(U_15,U_18)
| ! [U_6] :
( ~ in(U_6,U_20)
| ~ in(ordered_pair(U_15,U_6),U_13) ) )
& ! [U_14] :
( ? [U_5] :
( in(U_5,U_20)
& in(ordered_pair(U_14,U_5),U_13) )
| ~ in(U_14,U_18) ) )
| U_18 != relation_inverse_image(U_13,U_20) ) )
| ~ relation(U_13) ),
inference(miniscope,[status(thm)],[f_4_2]) ).
fof(f_4_4,plain,
! [U_13] :
( ( ! [U_21,U_19] :
( U_19 = relation_inverse_image(U_13,U_21)
| ? [U_17] :
( ~ in(U_17,U_19)
& ? [U_9] :
( in(U_9,U_21)
& in(ordered_pair(U_17,U_9),U_13) ) )
| ? [U_16] :
( ! [U_8] :
( ~ in(U_8,U_21)
| ~ in(ordered_pair(U_16,U_8),U_13) )
& in(U_16,U_19) ) )
& ! [U_20,U_18] :
( ( ! [U_15] :
( in(U_15,U_18)
| ! [U_6] :
( ~ in(U_6,U_20)
| ~ in(ordered_pair(U_15,U_6),U_13) ) )
& ! [U_14] :
( ( in(sK1(U_13,U_20,U_18,U_14),U_20)
& in(ordered_pair(U_14,sK1(U_13,U_20,U_18,U_14)),U_13) )
| ~ in(U_14,U_18) ) )
| U_18 != relation_inverse_image(U_13,U_20) ) )
| ~ relation(U_13) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1]),skolemize(U_5,sK1(U_13,U_20,U_18,U_14))],[f_4_3]) ).
fof(f_4_5,plain,
! [U_13] :
( ( ! [U_21,U_19] :
( U_19 = relation_inverse_image(U_13,U_21)
| ? [U_17] :
( ~ in(U_17,U_19)
& ? [U_9] :
( in(U_9,U_21)
& in(ordered_pair(U_17,U_9),U_13) ) )
| ( ! [U_8] :
( ~ in(U_8,U_21)
| ~ in(ordered_pair(sK2(U_13,U_21,U_19),U_8),U_13) )
& in(sK2(U_13,U_21,U_19),U_19) ) )
& ! [U_20,U_18] :
( ( ! [U_15] :
( in(U_15,U_18)
| ! [U_6] :
( ~ in(U_6,U_20)
| ~ in(ordered_pair(U_15,U_6),U_13) ) )
& ! [U_14] :
( ( in(sK1(U_13,U_20,U_18,U_14),U_20)
& in(ordered_pair(U_14,sK1(U_13,U_20,U_18,U_14)),U_13) )
| ~ in(U_14,U_18) ) )
| U_18 != relation_inverse_image(U_13,U_20) ) )
| ~ relation(U_13) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2]),skolemize(U_16,sK2(U_13,U_21,U_19))],[f_4_4]) ).
fof(f_4_6,plain,
! [U_13] :
( ( ! [U_21,U_19] :
( U_19 = relation_inverse_image(U_13,U_21)
| ( ~ in(sK3(U_13,U_21,U_19),U_19)
& ? [U_9] :
( in(U_9,U_21)
& in(ordered_pair(sK3(U_13,U_21,U_19),U_9),U_13) ) )
| ( ! [U_8] :
( ~ in(U_8,U_21)
| ~ in(ordered_pair(sK2(U_13,U_21,U_19),U_8),U_13) )
& in(sK2(U_13,U_21,U_19),U_19) ) )
& ! [U_20,U_18] :
( ( ! [U_15] :
( in(U_15,U_18)
| ! [U_6] :
( ~ in(U_6,U_20)
| ~ in(ordered_pair(U_15,U_6),U_13) ) )
& ! [U_14] :
( ( in(sK1(U_13,U_20,U_18,U_14),U_20)
& in(ordered_pair(U_14,sK1(U_13,U_20,U_18,U_14)),U_13) )
| ~ in(U_14,U_18) ) )
| U_18 != relation_inverse_image(U_13,U_20) ) )
| ~ relation(U_13) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3]),skolemize(U_17,sK3(U_13,U_21,U_19))],[f_4_5]) ).
fof(f_4_7,plain,
! [U_13] :
( ( ! [U_21,U_19] :
( U_19 = relation_inverse_image(U_13,U_21)
| ( ~ in(sK3(U_13,U_21,U_19),U_19)
& in(sK4(U_13,U_21,U_19),U_21)
& in(ordered_pair(sK3(U_13,U_21,U_19),sK4(U_13,U_21,U_19)),U_13) )
| ( ! [U_8] :
( ~ in(U_8,U_21)
| ~ in(ordered_pair(sK2(U_13,U_21,U_19),U_8),U_13) )
& in(sK2(U_13,U_21,U_19),U_19) ) )
& ! [U_20,U_18] :
( ( ! [U_15] :
( in(U_15,U_18)
| ! [U_6] :
( ~ in(U_6,U_20)
| ~ in(ordered_pair(U_15,U_6),U_13) ) )
& ! [U_14] :
( ( in(sK1(U_13,U_20,U_18,U_14),U_20)
& in(ordered_pair(U_14,sK1(U_13,U_20,U_18,U_14)),U_13) )
| ~ in(U_14,U_18) ) )
| U_18 != relation_inverse_image(U_13,U_20) ) )
| ~ relation(U_13) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4]),skolemize(U_9,sK4(U_13,U_21,U_19))],[f_4_6]) ).
cnf(f_4_8,plain,
( in(ordered_pair(U_14,sK1(U_13,U_20,U_18,U_14)),U_13)
| ~ in(U_14,U_18)
| U_18 != relation_inverse_image(U_13,U_20)
| ~ relation(U_13) ),
inference(clausify,[status(thm)],[f_4_7]) ).
cnf(f_4_9,plain,
( in(sK1(U_13,U_20,U_18,U_14),U_20)
| ~ in(U_14,U_18)
| U_18 != relation_inverse_image(U_13,U_20)
| ~ relation(U_13) ),
inference(clausify,[status(thm)],[f_4_7]) ).
cnf(f_4_10,plain,
( in(U_15,U_18)
| ~ in(U_6,U_20)
| ~ in(ordered_pair(U_15,U_6),U_13)
| U_18 != relation_inverse_image(U_13,U_20)
| ~ relation(U_13) ),
inference(clausify,[status(thm)],[f_4_7]) ).
fof(f_5_1,plain,
! [A] :
( ! [B] :
( ( B = relation_rng(A)
| ? [C] :
( ( ~ in(C,B)
& ? [D] : in(ordered_pair(D,C),A) )
| ( ! [D] : ~ in(ordered_pair(D,C),A)
& in(C,B) ) ) )
& ( ! [C] :
( ( in(C,B)
| ! [D] : ~ in(ordered_pair(D,C),A) )
& ( ? [D] : in(ordered_pair(D,C),A)
| ~ in(C,B) ) )
| B != relation_rng(A) ) )
| ~ relation(A) ),
inference(fof_nnf,[status(thm)],[d5_relat_1]) ).
fof(f_5_2,plain,
! [U_29] :
( ! [U_28] :
( ( U_28 = relation_rng(U_29)
| ? [U_27] :
( ( ~ in(U_27,U_28)
& ? [U_26] : in(ordered_pair(U_26,U_27),U_29) )
| ( ! [U_25] : ~ in(ordered_pair(U_25,U_27),U_29)
& in(U_27,U_28) ) ) )
& ( ! [U_24] :
( ( in(U_24,U_28)
| ! [U_23] : ~ in(ordered_pair(U_23,U_24),U_29) )
& ( ? [U_22] : in(ordered_pair(U_22,U_24),U_29)
| ~ in(U_24,U_28) ) )
| U_28 != relation_rng(U_29) ) )
| ~ relation(U_29) ),
inference(variable_rename,[status(thm)],[f_5_1]) ).
fof(f_5_3,plain,
! [U_29] :
( ( ! [U_35] :
( U_35 = relation_rng(U_29)
| ? [U_33] :
( ~ in(U_33,U_35)
& ? [U_26] : in(ordered_pair(U_26,U_33),U_29) )
| ? [U_32] :
( ! [U_25] : ~ in(ordered_pair(U_25,U_32),U_29)
& in(U_32,U_35) ) )
& ! [U_34] :
( ( ! [U_31] :
( in(U_31,U_34)
| ! [U_23] : ~ in(ordered_pair(U_23,U_31),U_29) )
& ! [U_30] :
( ? [U_22] : in(ordered_pair(U_22,U_30),U_29)
| ~ in(U_30,U_34) ) )
| U_34 != relation_rng(U_29) ) )
| ~ relation(U_29) ),
inference(miniscope,[status(thm)],[f_5_2]) ).
fof(f_5_4,plain,
! [U_29] :
( ( ! [U_35] :
( U_35 = relation_rng(U_29)
| ? [U_33] :
( ~ in(U_33,U_35)
& ? [U_26] : in(ordered_pair(U_26,U_33),U_29) )
| ? [U_32] :
( ! [U_25] : ~ in(ordered_pair(U_25,U_32),U_29)
& in(U_32,U_35) ) )
& ! [U_34] :
( ( ! [U_31] :
( in(U_31,U_34)
| ! [U_23] : ~ in(ordered_pair(U_23,U_31),U_29) )
& ! [U_30] :
( in(ordered_pair(sK5(U_29,U_34,U_30),U_30),U_29)
| ~ in(U_30,U_34) ) )
| U_34 != relation_rng(U_29) ) )
| ~ relation(U_29) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK5]),skolemize(U_22,sK5(U_29,U_34,U_30))],[f_5_3]) ).
fof(f_5_5,plain,
! [U_29] :
( ( ! [U_35] :
( U_35 = relation_rng(U_29)
| ? [U_33] :
( ~ in(U_33,U_35)
& ? [U_26] : in(ordered_pair(U_26,U_33),U_29) )
| ( ! [U_25] : ~ in(ordered_pair(U_25,sK6(U_29,U_35)),U_29)
& in(sK6(U_29,U_35),U_35) ) )
& ! [U_34] :
( ( ! [U_31] :
( in(U_31,U_34)
| ! [U_23] : ~ in(ordered_pair(U_23,U_31),U_29) )
& ! [U_30] :
( in(ordered_pair(sK5(U_29,U_34,U_30),U_30),U_29)
| ~ in(U_30,U_34) ) )
| U_34 != relation_rng(U_29) ) )
| ~ relation(U_29) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK6]),skolemize(U_32,sK6(U_29,U_35))],[f_5_4]) ).
fof(f_5_6,plain,
! [U_29] :
( ( ! [U_35] :
( U_35 = relation_rng(U_29)
| ( ~ in(sK7(U_29,U_35),U_35)
& ? [U_26] : in(ordered_pair(U_26,sK7(U_29,U_35)),U_29) )
| ( ! [U_25] : ~ in(ordered_pair(U_25,sK6(U_29,U_35)),U_29)
& in(sK6(U_29,U_35),U_35) ) )
& ! [U_34] :
( ( ! [U_31] :
( in(U_31,U_34)
| ! [U_23] : ~ in(ordered_pair(U_23,U_31),U_29) )
& ! [U_30] :
( in(ordered_pair(sK5(U_29,U_34,U_30),U_30),U_29)
| ~ in(U_30,U_34) ) )
| U_34 != relation_rng(U_29) ) )
| ~ relation(U_29) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK7]),skolemize(U_33,sK7(U_29,U_35))],[f_5_5]) ).
fof(f_5_7,plain,
! [U_29] :
( ( ! [U_35] :
( U_35 = relation_rng(U_29)
| ( ~ in(sK7(U_29,U_35),U_35)
& in(ordered_pair(sK8(U_29,U_35),sK7(U_29,U_35)),U_29) )
| ( ! [U_25] : ~ in(ordered_pair(U_25,sK6(U_29,U_35)),U_29)
& in(sK6(U_29,U_35),U_35) ) )
& ! [U_34] :
( ( ! [U_31] :
( in(U_31,U_34)
| ! [U_23] : ~ in(ordered_pair(U_23,U_31),U_29) )
& ! [U_30] :
( in(ordered_pair(sK5(U_29,U_34,U_30),U_30),U_29)
| ~ in(U_30,U_34) ) )
| U_34 != relation_rng(U_29) ) )
| ~ relation(U_29) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK8]),skolemize(U_26,sK8(U_29,U_35))],[f_5_6]) ).
cnf(f_5_9,plain,
( in(U_31,U_34)
| ~ in(ordered_pair(U_23,U_31),U_29)
| U_34 != relation_rng(U_29)
| ~ relation(U_29) ),
inference(clausify,[status(thm)],[f_5_7]) ).
fof(f_26_1,negated_conjecture,
~ ! [A,B,C] :
( relation(C)
=> ( in(A,relation_inverse_image(C,B))
<=> ? [D] :
( in(D,B)
& in(ordered_pair(A,D),C)
& in(D,relation_rng(C)) ) ) ),
inference(negate,[status(cth)],[t166_relat_1]) ).
fof(f_26_2,negated_conjecture,
? [A,B,C] :
( ( ( ~ in(A,relation_inverse_image(C,B))
& ? [D] :
( in(D,B)
& in(ordered_pair(A,D),C)
& in(D,relation_rng(C)) ) )
| ( ! [D] :
( ~ in(D,B)
| ~ in(ordered_pair(A,D),C)
| ~ in(D,relation_rng(C)) )
& in(A,relation_inverse_image(C,B)) ) )
& relation(C) ),
inference(fof_nnf,[status(thm)],[f_26_1]) ).
fof(f_26_3,negated_conjecture,
? [U_55,U_54,U_53] :
( ( ( ~ in(U_55,relation_inverse_image(U_53,U_54))
& ? [U_52] :
( in(U_52,U_54)
& in(ordered_pair(U_55,U_52),U_53)
& in(U_52,relation_rng(U_53)) ) )
| ( ! [U_51] :
( ~ in(U_51,U_54)
| ~ in(ordered_pair(U_55,U_51),U_53)
| ~ in(U_51,relation_rng(U_53)) )
& in(U_55,relation_inverse_image(U_53,U_54)) ) )
& relation(U_53) ),
inference(variable_rename,[status(thm)],[f_26_2]) ).
fof(f_26_4,negated_conjecture,
? [U_54,U_53] :
( ( ( ~ in(sK14,relation_inverse_image(U_53,U_54))
& ? [U_52] :
( in(U_52,U_54)
& in(ordered_pair(sK14,U_52),U_53)
& in(U_52,relation_rng(U_53)) ) )
| ( ! [U_51] :
( ~ in(U_51,U_54)
| ~ in(ordered_pair(sK14,U_51),U_53)
| ~ in(U_51,relation_rng(U_53)) )
& in(sK14,relation_inverse_image(U_53,U_54)) ) )
& relation(U_53) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK14]),skolemize(U_55,sK14)],[f_26_3]) ).
fof(f_26_5,negated_conjecture,
? [U_53] :
( ( ( ~ in(sK14,relation_inverse_image(U_53,sK15))
& ? [U_52] :
( in(U_52,sK15)
& in(ordered_pair(sK14,U_52),U_53)
& in(U_52,relation_rng(U_53)) ) )
| ( ! [U_51] :
( ~ in(U_51,sK15)
| ~ in(ordered_pair(sK14,U_51),U_53)
| ~ in(U_51,relation_rng(U_53)) )
& in(sK14,relation_inverse_image(U_53,sK15)) ) )
& relation(U_53) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK15]),skolemize(U_54,sK15)],[f_26_4]) ).
fof(f_26_6,negated_conjecture,
( ( ( ~ in(sK14,relation_inverse_image(sK16,sK15))
& ? [U_52] :
( in(U_52,sK15)
& in(ordered_pair(sK14,U_52),sK16)
& in(U_52,relation_rng(sK16)) ) )
| ( ! [U_51] :
( ~ in(U_51,sK15)
| ~ in(ordered_pair(sK14,U_51),sK16)
| ~ in(U_51,relation_rng(sK16)) )
& in(sK14,relation_inverse_image(sK16,sK15)) ) )
& relation(sK16) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK16]),skolemize(U_53,sK16)],[f_26_5]) ).
fof(f_26_7,negated_conjecture,
( ( ( ~ in(sK14,relation_inverse_image(sK16,sK15))
& in(sK17,sK15)
& in(ordered_pair(sK14,sK17),sK16)
& in(sK17,relation_rng(sK16)) )
| ( ! [U_51] :
( ~ in(U_51,sK15)
| ~ in(ordered_pair(sK14,U_51),sK16)
| ~ in(U_51,relation_rng(sK16)) )
& in(sK14,relation_inverse_image(sK16,sK15)) ) )
& relation(sK16) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK17]),skolemize(U_52,sK17)],[f_26_6]) ).
cnf(f_26_8,negated_conjecture,
relation(sK16),
inference(clausify,[status(thm)],[f_26_7]) ).
cnf(f_26_9,negated_conjecture,
( in(sK17,relation_rng(sK16))
| in(sK14,relation_inverse_image(sK16,sK15)) ),
inference(clausify,[status(thm)],[f_26_7]) ).
cnf(f_26_10,negated_conjecture,
( in(ordered_pair(sK14,sK17),sK16)
| in(sK14,relation_inverse_image(sK16,sK15)) ),
inference(clausify,[status(thm)],[f_26_7]) ).
cnf(f_26_11,negated_conjecture,
( in(sK17,sK15)
| in(sK14,relation_inverse_image(sK16,sK15)) ),
inference(clausify,[status(thm)],[f_26_7]) ).
cnf(f_26_13,negated_conjecture,
( in(sK17,relation_rng(sK16))
| ~ in(U_51,sK15)
| ~ in(ordered_pair(sK14,U_51),sK16)
| ~ in(U_51,relation_rng(sK16)) ),
inference(clausify,[status(thm)],[f_26_7]) ).
cnf(f_26_14,negated_conjecture,
( in(ordered_pair(sK14,sK17),sK16)
| ~ in(U_51,sK15)
| ~ in(ordered_pair(sK14,U_51),sK16)
| ~ in(U_51,relation_rng(sK16)) ),
inference(clausify,[status(thm)],[f_26_7]) ).
cnf(f_26_15,negated_conjecture,
( in(sK17,sK15)
| ~ in(U_51,sK15)
| ~ in(ordered_pair(sK14,U_51),sK16)
| ~ in(U_51,relation_rng(sK16)) ),
inference(clausify,[status(thm)],[f_26_7]) ).
cnf(f_26_16,negated_conjecture,
( ~ in(sK14,relation_inverse_image(sK16,sK15))
| ~ in(U_51,sK15)
| ~ in(ordered_pair(sK14,U_51),sK16)
| ~ in(U_51,relation_rng(sK16)) ),
inference(clausify,[status(thm)],[f_26_7]) ).
cnf(equality_1,axiom,
Eq_x_0 = Eq_x_0,
theory(equality,[reflexivity]) ).
cnf(equality_5,axiom,
( relation_inverse_image(Eq_x_0,Eq_x_1) = relation_inverse_image(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_7,axiom,
( relation_rng(Eq_x_0) = relation_rng(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(t1,plain,
( ~ in(ordered_pair(sK14,sK17),sK16)
| ~ in(sK17,sK15)
| ~ in(sK14,relation_inverse_image(sK16,sK15))
| ~ in(sK17,relation_rng(sK16)) ),
inference(start,[status(thm),parent(0:0)],[f_26_16]) ).
cnf(t2,plain,
( ~ in(ordered_pair(sK14,sK1(sK16,sK15,relation_inverse_image(sK16,sK15),sK14)),sK16)
| ~ in(sK1(sK16,sK15,relation_inverse_image(sK16,sK15),sK14),sK15)
| ~ in(sK1(sK16,sK15,relation_inverse_image(sK16,sK15),sK14),relation_rng(sK16))
| in(sK17,relation_rng(sK16)) ),
inference(extension,[status(thm),parent(t1:1)],[f_26_13]) ).
cnf(t3,plain,
$false,
inference(connection,[status(thm),parent(t2:1)],[t2:1,t1:1]) ).
cnf(t4,plain,
( relation_rng(sK16) != relation_rng(sK16)
| ~ in(ordered_pair(sK14,sK1(sK16,sK15,relation_inverse_image(sK16,sK15),sK14)),sK16)
| ~ relation(sK16)
| in(sK1(sK16,sK15,relation_inverse_image(sK16,sK15),sK14),relation_rng(sK16)) ),
inference(extension,[status(thm),parent(t2:2)],[f_5_9]) ).
cnf(t5,plain,
$false,
inference(connection,[status(thm),parent(t4:1)],[t4:1,t2:2]) ).
cnf(t6,plain,
relation(sK16),
inference(extension,[status(thm),parent(t4:2)],[f_26_8]) ).
cnf(t7,plain,
$false,
inference(connection,[status(thm),parent(t6:1)],[t6:1,t4:2]) ).
cnf(l3,lemma,
relation(sK16),
inference(lemma,[status(cth),parent(t4:2),below(t2:2)],[t4:2]) ).
cnf(t8,plain,
( relation_inverse_image(sK16,sK15) != relation_inverse_image(sK16,sK15)
| ~ in(sK14,relation_inverse_image(sK16,sK15))
| ~ relation(sK16)
| in(ordered_pair(sK14,sK1(sK16,sK15,relation_inverse_image(sK16,sK15),sK14)),sK16) ),
inference(extension,[status(thm),parent(t4:3)],[f_4_8]) ).
cnf(t9,plain,
$false,
inference(connection,[status(thm),parent(t8:1)],[t8:1,t4:3]) ).
cnf(t10,plain,
relation(sK16),
inference(lemma_extension,[status(thm),parent(t8:2)],[l3:1]) ).
cnf(t11,plain,
$false,
inference(connection,[status(thm),parent(t10:1)],[t10:1,t8:2]) ).
cnf(t12,plain,
( in(sK17,relation_rng(sK16))
| in(sK14,relation_inverse_image(sK16,sK15)) ),
inference(extension,[status(thm),parent(t8:3)],[f_26_9]) ).
cnf(t13,plain,
$false,
inference(connection,[status(thm),parent(t12:1)],[t12:1,t8:3]) ).
cnf(t14,plain,
$false,
inference(reduction,[status(thm),parent(t12:2)],[t12:2,t1:1]) ).
cnf(t15,plain,
relation_inverse_image(sK16,sK15) = relation_inverse_image(sK16,sK15),
inference(extension,[status(thm),parent(t8:4)],[equality_1]) ).
cnf(t16,plain,
$false,
inference(connection,[status(thm),parent(t15:1)],[t15:1,t8:4]) ).
cnf(t17,plain,
( sK16 != sK16
| relation_rng(sK16) = relation_rng(sK16) ),
inference(extension,[status(thm),parent(t4:4)],[equality_7]) ).
cnf(t18,plain,
$false,
inference(connection,[status(thm),parent(t17:1)],[t17:1,t4:4]) ).
cnf(t19,plain,
sK16 = sK16,
inference(extension,[status(thm),parent(t17:2)],[equality_1]) ).
cnf(t20,plain,
$false,
inference(connection,[status(thm),parent(t19:1)],[t19:1,t17:2]) ).
cnf(t21,plain,
( relation_inverse_image(sK16,sK15) != relation_inverse_image(sK16,sK15)
| ~ in(sK14,relation_inverse_image(sK16,sK15))
| ~ relation(sK16)
| in(sK1(sK16,sK15,relation_inverse_image(sK16,sK15),sK14),sK15) ),
inference(extension,[status(thm),parent(t2:3)],[f_4_9]) ).
cnf(t22,plain,
$false,
inference(connection,[status(thm),parent(t21:1)],[t21:1,t2:3]) ).
cnf(t23,plain,
relation(sK16),
inference(extension,[status(thm),parent(t21:2)],[f_26_8]) ).
cnf(t24,plain,
$false,
inference(connection,[status(thm),parent(t23:1)],[t23:1,t21:2]) ).
cnf(t25,plain,
( in(sK17,relation_rng(sK16))
| in(sK14,relation_inverse_image(sK16,sK15)) ),
inference(extension,[status(thm),parent(t21:3)],[f_26_9]) ).
cnf(t26,plain,
$false,
inference(connection,[status(thm),parent(t25:1)],[t25:1,t21:3]) ).
cnf(t27,plain,
$false,
inference(reduction,[status(thm),parent(t25:2)],[t25:2,t1:1]) ).
cnf(t28,plain,
( sK15 != sK15
| sK16 != sK16
| relation_inverse_image(sK16,sK15) = relation_inverse_image(sK16,sK15) ),
inference(extension,[status(thm),parent(t21:4)],[equality_5]) ).
cnf(t29,plain,
$false,
inference(connection,[status(thm),parent(t28:1)],[t28:1,t21:4]) ).
cnf(t30,plain,
sK16 = sK16,
inference(extension,[status(thm),parent(t28:2)],[equality_1]) ).
cnf(t31,plain,
$false,
inference(connection,[status(thm),parent(t30:1)],[t30:1,t28:2]) ).
cnf(t32,plain,
sK15 = sK15,
inference(extension,[status(thm),parent(t28:3)],[equality_1]) ).
cnf(t33,plain,
$false,
inference(connection,[status(thm),parent(t32:1)],[t32:1,t28:3]) ).
cnf(t34,plain,
( relation_inverse_image(sK16,sK15) != relation_inverse_image(sK16,sK15)
| ~ in(sK14,relation_inverse_image(sK16,sK15))
| ~ relation(sK16)
| in(ordered_pair(sK14,sK1(sK16,sK15,relation_inverse_image(sK16,sK15),sK14)),sK16) ),
inference(extension,[status(thm),parent(t2:4)],[f_4_8]) ).
cnf(t35,plain,
$false,
inference(connection,[status(thm),parent(t34:1)],[t34:1,t2:4]) ).
cnf(t36,plain,
relation(sK16),
inference(extension,[status(thm),parent(t34:2)],[f_26_8]) ).
cnf(t37,plain,
$false,
inference(connection,[status(thm),parent(t36:1)],[t36:1,t34:2]) ).
cnf(t38,plain,
( in(sK17,relation_rng(sK16))
| in(sK14,relation_inverse_image(sK16,sK15)) ),
inference(extension,[status(thm),parent(t34:3)],[f_26_9]) ).
cnf(t39,plain,
$false,
inference(connection,[status(thm),parent(t38:1)],[t38:1,t34:3]) ).
cnf(t40,plain,
$false,
inference(reduction,[status(thm),parent(t38:2)],[t38:2,t1:1]) ).
cnf(t41,plain,
( sK15 != sK15
| sK16 != sK16
| relation_inverse_image(sK16,sK15) = relation_inverse_image(sK16,sK15) ),
inference(extension,[status(thm),parent(t34:4)],[equality_5]) ).
cnf(t42,plain,
$false,
inference(connection,[status(thm),parent(t41:1)],[t41:1,t34:4]) ).
cnf(t43,plain,
sK16 = sK16,
inference(extension,[status(thm),parent(t41:2)],[equality_1]) ).
cnf(t44,plain,
$false,
inference(connection,[status(thm),parent(t43:1)],[t43:1,t41:2]) ).
cnf(t45,plain,
sK15 = sK15,
inference(extension,[status(thm),parent(t41:3)],[equality_1]) ).
cnf(t46,plain,
$false,
inference(connection,[status(thm),parent(t45:1)],[t45:1,t41:3]) ).
cnf(l1,lemma,
in(sK17,relation_rng(sK16)),
inference(lemma,[status(cth),parent(t1:1),below(0:0)],[t1:1]) ).
cnf(t47,plain,
( in(sK17,sK15)
| in(sK14,relation_inverse_image(sK16,sK15)) ),
inference(extension,[status(thm),parent(t1:2)],[f_26_11]) ).
cnf(t48,plain,
$false,
inference(connection,[status(thm),parent(t47:1)],[t47:1,t1:2]) ).
cnf(t49,plain,
( ~ in(ordered_pair(sK14,sK17),sK16)
| in(ordered_pair(sK14,sK17),sK16)
| ~ in(sK17,relation_rng(sK16))
| ~ in(sK17,sK15) ),
inference(extension,[status(thm),parent(t47:2)],[f_26_14]) ).
cnf(t50,plain,
$false,
inference(connection,[status(thm),parent(t49:1)],[t49:1,t47:2]) ).
cnf(t51,plain,
in(sK17,relation_rng(sK16)),
inference(lemma_extension,[status(thm),parent(t49:2)],[l1:1]) ).
cnf(t52,plain,
$false,
inference(connection,[status(thm),parent(t51:1)],[t51:1,t49:2]) ).
cnf(t53,plain,
( relation_inverse_image(sK16,sK15) != relation_inverse_image(sK16,sK15)
| in(sK14,relation_inverse_image(sK16,sK15))
| ~ in(sK17,sK15)
| ~ relation(sK16)
| ~ in(ordered_pair(sK14,sK17),sK16) ),
inference(extension,[status(thm),parent(t49:3)],[f_4_10]) ).
cnf(t54,plain,
$false,
inference(connection,[status(thm),parent(t53:1)],[t53:1,t49:3]) ).
cnf(t55,plain,
relation(sK16),
inference(extension,[status(thm),parent(t53:2)],[f_26_8]) ).
cnf(t56,plain,
$false,
inference(connection,[status(thm),parent(t55:1)],[t55:1,t53:2]) ).
cnf(t57,plain,
$false,
inference(reduction,[status(thm),parent(t53:3)],[t53:3,t47:2]) ).
cnf(t58,plain,
$false,
inference(reduction,[status(thm),parent(t53:4)],[t53:4,t1:2]) ).
cnf(t59,plain,
relation_inverse_image(sK16,sK15) = relation_inverse_image(sK16,sK15),
inference(extension,[status(thm),parent(t53:5)],[equality_1]) ).
cnf(t60,plain,
$false,
inference(connection,[status(thm),parent(t59:1)],[t59:1,t53:5]) ).
cnf(t61,plain,
( in(sK14,relation_inverse_image(sK16,sK15))
| in(ordered_pair(sK14,sK17),sK16) ),
inference(extension,[status(thm),parent(t49:4)],[f_26_10]) ).
cnf(t62,plain,
$false,
inference(connection,[status(thm),parent(t61:1)],[t61:1,t49:4]) ).
cnf(t63,plain,
$false,
inference(reduction,[status(thm),parent(t61:2)],[t61:2,t1:2]) ).
cnf(l24,lemma,
in(sK14,relation_inverse_image(sK16,sK15)),
inference(lemma,[status(cth),parent(t1:2),below(0:0)],[t1:2]) ).
cnf(t64,plain,
( ~ in(ordered_pair(sK14,sK1(sK16,sK15,relation_inverse_image(sK16,sK15),sK14)),sK16)
| ~ in(sK1(sK16,sK15,relation_inverse_image(sK16,sK15),sK14),sK15)
| ~ in(sK1(sK16,sK15,relation_inverse_image(sK16,sK15),sK14),relation_rng(sK16))
| in(sK17,sK15) ),
inference(extension,[status(thm),parent(t1:3)],[f_26_15]) ).
cnf(t65,plain,
$false,
inference(connection,[status(thm),parent(t64:1)],[t64:1,t1:3]) ).
cnf(t66,plain,
( relation_rng(sK16) != relation_rng(sK16)
| ~ in(ordered_pair(sK14,sK1(sK16,sK15,relation_inverse_image(sK16,sK15),sK14)),sK16)
| ~ relation(sK16)
| in(sK1(sK16,sK15,relation_inverse_image(sK16,sK15),sK14),relation_rng(sK16)) ),
inference(extension,[status(thm),parent(t64:2)],[f_5_9]) ).
cnf(t67,plain,
$false,
inference(connection,[status(thm),parent(t66:1)],[t66:1,t64:2]) ).
cnf(t68,plain,
relation(sK16),
inference(extension,[status(thm),parent(t66:2)],[f_26_8]) ).
cnf(t69,plain,
$false,
inference(connection,[status(thm),parent(t68:1)],[t68:1,t66:2]) ).
cnf(l35,lemma,
relation(sK16),
inference(lemma,[status(cth),parent(t66:2),below(t64:2)],[t66:2]) ).
cnf(t70,plain,
( relation_inverse_image(sK16,sK15) != relation_inverse_image(sK16,sK15)
| ~ in(sK14,relation_inverse_image(sK16,sK15))
| ~ relation(sK16)
| in(ordered_pair(sK14,sK1(sK16,sK15,relation_inverse_image(sK16,sK15),sK14)),sK16) ),
inference(extension,[status(thm),parent(t66:3)],[f_4_8]) ).
cnf(t71,plain,
$false,
inference(connection,[status(thm),parent(t70:1)],[t70:1,t66:3]) ).
cnf(t72,plain,
relation(sK16),
inference(lemma_extension,[status(thm),parent(t70:2)],[l35:1]) ).
cnf(t73,plain,
$false,
inference(connection,[status(thm),parent(t72:1)],[t72:1,t70:2]) ).
cnf(t74,plain,
( in(sK17,sK15)
| in(sK14,relation_inverse_image(sK16,sK15)) ),
inference(extension,[status(thm),parent(t70:3)],[f_26_11]) ).
cnf(t75,plain,
$false,
inference(connection,[status(thm),parent(t74:1)],[t74:1,t70:3]) ).
cnf(t76,plain,
$false,
inference(reduction,[status(thm),parent(t74:2)],[t74:2,t1:3]) ).
cnf(t77,plain,
relation_inverse_image(sK16,sK15) = relation_inverse_image(sK16,sK15),
inference(extension,[status(thm),parent(t70:4)],[equality_1]) ).
cnf(t78,plain,
$false,
inference(connection,[status(thm),parent(t77:1)],[t77:1,t70:4]) ).
cnf(t79,plain,
( sK16 != sK16
| relation_rng(sK16) = relation_rng(sK16) ),
inference(extension,[status(thm),parent(t66:4)],[equality_7]) ).
cnf(t80,plain,
$false,
inference(connection,[status(thm),parent(t79:1)],[t79:1,t66:4]) ).
cnf(t81,plain,
sK16 = sK16,
inference(extension,[status(thm),parent(t79:2)],[equality_1]) ).
cnf(t82,plain,
$false,
inference(connection,[status(thm),parent(t81:1)],[t81:1,t79:2]) ).
cnf(t83,plain,
( relation_inverse_image(sK16,sK15) != relation_inverse_image(sK16,sK15)
| ~ in(sK14,relation_inverse_image(sK16,sK15))
| ~ relation(sK16)
| in(sK1(sK16,sK15,relation_inverse_image(sK16,sK15),sK14),sK15) ),
inference(extension,[status(thm),parent(t64:3)],[f_4_9]) ).
cnf(t84,plain,
$false,
inference(connection,[status(thm),parent(t83:1)],[t83:1,t64:3]) ).
cnf(t85,plain,
relation(sK16),
inference(extension,[status(thm),parent(t83:2)],[f_26_8]) ).
cnf(t86,plain,
$false,
inference(connection,[status(thm),parent(t85:1)],[t85:1,t83:2]) ).
cnf(t87,plain,
in(sK14,relation_inverse_image(sK16,sK15)),
inference(lemma_extension,[status(thm),parent(t83:3)],[l24:1]) ).
cnf(t88,plain,
$false,
inference(connection,[status(thm),parent(t87:1)],[t87:1,t83:3]) ).
cnf(t89,plain,
( sK15 != sK15
| sK16 != sK16
| relation_inverse_image(sK16,sK15) = relation_inverse_image(sK16,sK15) ),
inference(extension,[status(thm),parent(t83:4)],[equality_5]) ).
cnf(t90,plain,
$false,
inference(connection,[status(thm),parent(t89:1)],[t89:1,t83:4]) ).
cnf(t91,plain,
sK16 = sK16,
inference(extension,[status(thm),parent(t89:2)],[equality_1]) ).
cnf(t92,plain,
$false,
inference(connection,[status(thm),parent(t91:1)],[t91:1,t89:2]) ).
cnf(t93,plain,
sK15 = sK15,
inference(extension,[status(thm),parent(t89:3)],[equality_1]) ).
cnf(t94,plain,
$false,
inference(connection,[status(thm),parent(t93:1)],[t93:1,t89:3]) ).
cnf(t95,plain,
( relation_inverse_image(sK16,sK15) != relation_inverse_image(sK16,sK15)
| ~ in(sK14,relation_inverse_image(sK16,sK15))
| ~ relation(sK16)
| in(ordered_pair(sK14,sK1(sK16,sK15,relation_inverse_image(sK16,sK15),sK14)),sK16) ),
inference(extension,[status(thm),parent(t64:4)],[f_4_8]) ).
cnf(t96,plain,
$false,
inference(connection,[status(thm),parent(t95:1)],[t95:1,t64:4]) ).
cnf(t97,plain,
relation(sK16),
inference(extension,[status(thm),parent(t95:2)],[f_26_8]) ).
cnf(t98,plain,
$false,
inference(connection,[status(thm),parent(t97:1)],[t97:1,t95:2]) ).
cnf(t99,plain,
in(sK14,relation_inverse_image(sK16,sK15)),
inference(lemma_extension,[status(thm),parent(t95:3)],[l24:1]) ).
cnf(t100,plain,
$false,
inference(connection,[status(thm),parent(t99:1)],[t99:1,t95:3]) ).
cnf(t101,plain,
( sK15 != sK15
| sK16 != sK16
| relation_inverse_image(sK16,sK15) = relation_inverse_image(sK16,sK15) ),
inference(extension,[status(thm),parent(t95:4)],[equality_5]) ).
cnf(t102,plain,
$false,
inference(connection,[status(thm),parent(t101:1)],[t101:1,t95:4]) ).
cnf(t103,plain,
sK16 = sK16,
inference(extension,[status(thm),parent(t101:2)],[equality_1]) ).
cnf(t104,plain,
$false,
inference(connection,[status(thm),parent(t103:1)],[t103:1,t101:2]) ).
cnf(t105,plain,
sK15 = sK15,
inference(extension,[status(thm),parent(t101:3)],[equality_1]) ).
cnf(t106,plain,
$false,
inference(connection,[status(thm),parent(t105:1)],[t105:1,t101:3]) ).
cnf(t107,plain,
( ~ in(ordered_pair(sK14,sK1(sK16,sK15,relation_inverse_image(sK16,sK15),sK14)),sK16)
| ~ in(sK1(sK16,sK15,relation_inverse_image(sK16,sK15),sK14),sK15)
| ~ in(sK1(sK16,sK15,relation_inverse_image(sK16,sK15),sK14),relation_rng(sK16))
| in(ordered_pair(sK14,sK17),sK16) ),
inference(extension,[status(thm),parent(t1:4)],[f_26_14]) ).
cnf(t108,plain,
$false,
inference(connection,[status(thm),parent(t107:1)],[t107:1,t1:4]) ).
cnf(t109,plain,
( relation_rng(sK16) != relation_rng(sK16)
| ~ in(ordered_pair(sK14,sK1(sK16,sK15,relation_inverse_image(sK16,sK15),sK14)),sK16)
| ~ relation(sK16)
| in(sK1(sK16,sK15,relation_inverse_image(sK16,sK15),sK14),relation_rng(sK16)) ),
inference(extension,[status(thm),parent(t107:2)],[f_5_9]) ).
cnf(t110,plain,
$false,
inference(connection,[status(thm),parent(t109:1)],[t109:1,t107:2]) ).
cnf(t111,plain,
relation(sK16),
inference(extension,[status(thm),parent(t109:2)],[f_26_8]) ).
cnf(t112,plain,
$false,
inference(connection,[status(thm),parent(t111:1)],[t111:1,t109:2]) ).
cnf(l54,lemma,
relation(sK16),
inference(lemma,[status(cth),parent(t109:2),below(t107:2)],[t109:2]) ).
cnf(t113,plain,
( relation_inverse_image(sK16,sK15) != relation_inverse_image(sK16,sK15)
| ~ in(sK14,relation_inverse_image(sK16,sK15))
| ~ relation(sK16)
| in(ordered_pair(sK14,sK1(sK16,sK15,relation_inverse_image(sK16,sK15),sK14)),sK16) ),
inference(extension,[status(thm),parent(t109:3)],[f_4_8]) ).
cnf(t114,plain,
$false,
inference(connection,[status(thm),parent(t113:1)],[t113:1,t109:3]) ).
cnf(t115,plain,
relation(sK16),
inference(lemma_extension,[status(thm),parent(t113:2)],[l54:1]) ).
cnf(t116,plain,
$false,
inference(connection,[status(thm),parent(t115:1)],[t115:1,t113:2]) ).
cnf(t117,plain,
( in(ordered_pair(sK14,sK17),sK16)
| in(sK14,relation_inverse_image(sK16,sK15)) ),
inference(extension,[status(thm),parent(t113:3)],[f_26_10]) ).
cnf(t118,plain,
$false,
inference(connection,[status(thm),parent(t117:1)],[t117:1,t113:3]) ).
cnf(t119,plain,
$false,
inference(reduction,[status(thm),parent(t117:2)],[t117:2,t1:4]) ).
cnf(t120,plain,
relation_inverse_image(sK16,sK15) = relation_inverse_image(sK16,sK15),
inference(extension,[status(thm),parent(t113:4)],[equality_1]) ).
cnf(t121,plain,
$false,
inference(connection,[status(thm),parent(t120:1)],[t120:1,t113:4]) ).
cnf(t122,plain,
( sK16 != sK16
| relation_rng(sK16) = relation_rng(sK16) ),
inference(extension,[status(thm),parent(t109:4)],[equality_7]) ).
cnf(t123,plain,
$false,
inference(connection,[status(thm),parent(t122:1)],[t122:1,t109:4]) ).
cnf(t124,plain,
sK16 = sK16,
inference(extension,[status(thm),parent(t122:2)],[equality_1]) ).
cnf(t125,plain,
$false,
inference(connection,[status(thm),parent(t124:1)],[t124:1,t122:2]) ).
cnf(t126,plain,
( relation_inverse_image(sK16,sK15) != relation_inverse_image(sK16,sK15)
| ~ in(sK14,relation_inverse_image(sK16,sK15))
| ~ relation(sK16)
| in(sK1(sK16,sK15,relation_inverse_image(sK16,sK15),sK14),sK15) ),
inference(extension,[status(thm),parent(t107:3)],[f_4_9]) ).
cnf(t127,plain,
$false,
inference(connection,[status(thm),parent(t126:1)],[t126:1,t107:3]) ).
cnf(t128,plain,
relation(sK16),
inference(extension,[status(thm),parent(t126:2)],[f_26_8]) ).
cnf(t129,plain,
$false,
inference(connection,[status(thm),parent(t128:1)],[t128:1,t126:2]) ).
cnf(t130,plain,
in(sK14,relation_inverse_image(sK16,sK15)),
inference(lemma_extension,[status(thm),parent(t126:3)],[l24:1]) ).
cnf(t131,plain,
$false,
inference(connection,[status(thm),parent(t130:1)],[t130:1,t126:3]) ).
cnf(t132,plain,
( sK15 != sK15
| sK16 != sK16
| relation_inverse_image(sK16,sK15) = relation_inverse_image(sK16,sK15) ),
inference(extension,[status(thm),parent(t126:4)],[equality_5]) ).
cnf(t133,plain,
$false,
inference(connection,[status(thm),parent(t132:1)],[t132:1,t126:4]) ).
cnf(t134,plain,
sK16 = sK16,
inference(extension,[status(thm),parent(t132:2)],[equality_1]) ).
cnf(t135,plain,
$false,
inference(connection,[status(thm),parent(t134:1)],[t134:1,t132:2]) ).
cnf(t136,plain,
sK15 = sK15,
inference(extension,[status(thm),parent(t132:3)],[equality_1]) ).
cnf(t137,plain,
$false,
inference(connection,[status(thm),parent(t136:1)],[t136:1,t132:3]) ).
cnf(t138,plain,
( relation_inverse_image(sK16,sK15) != relation_inverse_image(sK16,sK15)
| ~ in(sK14,relation_inverse_image(sK16,sK15))
| ~ relation(sK16)
| in(ordered_pair(sK14,sK1(sK16,sK15,relation_inverse_image(sK16,sK15),sK14)),sK16) ),
inference(extension,[status(thm),parent(t107:4)],[f_4_8]) ).
cnf(t139,plain,
$false,
inference(connection,[status(thm),parent(t138:1)],[t138:1,t107:4]) ).
cnf(t140,plain,
relation(sK16),
inference(extension,[status(thm),parent(t138:2)],[f_26_8]) ).
cnf(t141,plain,
$false,
inference(connection,[status(thm),parent(t140:1)],[t140:1,t138:2]) ).
cnf(t142,plain,
in(sK14,relation_inverse_image(sK16,sK15)),
inference(lemma_extension,[status(thm),parent(t138:3)],[l24:1]) ).
cnf(t143,plain,
$false,
inference(connection,[status(thm),parent(t142:1)],[t142:1,t138:3]) ).
cnf(t144,plain,
( sK15 != sK15
| sK16 != sK16
| relation_inverse_image(sK16,sK15) = relation_inverse_image(sK16,sK15) ),
inference(extension,[status(thm),parent(t138:4)],[equality_5]) ).
cnf(t145,plain,
$false,
inference(connection,[status(thm),parent(t144:1)],[t144:1,t138:4]) ).
cnf(t146,plain,
sK16 = sK16,
inference(extension,[status(thm),parent(t144:2)],[equality_1]) ).
cnf(t147,plain,
$false,
inference(connection,[status(thm),parent(t146:1)],[t146:1,t144:2]) ).
cnf(t148,plain,
sK15 = sK15,
inference(extension,[status(thm),parent(t144:3)],[equality_1]) ).
cnf(t149,plain,
$false,
inference(connection,[status(thm),parent(t148:1)],[t148:1,t144:3]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU208+1 : TPTP v9.3.1. Released v3.3.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.11/0.35 % Computer : n001.cluster.edu
% 0.11/0.35 % Model : x86_64 x86_64
% 0.11/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.35 % Memory : 8046.5625MB
% 0.11/0.35 % OS : Linux 6.8.0-71-generic
% 0.11/0.35 % CPULimit : 300
% 0.11/0.35 % WCLimit : 300
% 0.11/0.35 % DateTime : Sat Sep 19 23:36:25 UTC 2026
% 0.11/0.36 % CPUTime :
% 79.55/79.82 % SZS status Theorem for theBenchmark
% 79.55/79.82 % SZS output start Proof for theBenchmark
% See solution above
%------------------------------------------------------------------------------