%------------------------------------------------------------------------------
% File : ConnectPP---0.7.2
% Problem : SET734+4 : TPTP v9.3.1. Bugfixed v2.2.1.
% 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 : n010.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:57:21 AM UTC 2026
% Result : Theorem 85.27s 85.53s
% Output : Proof 85.27s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 4
% Syntax : Number of formulae : 61 ( 26 unt; 0 def)
% Number of atoms : 202 ( 0 equ)
% Maximal formula atoms : 10 ( 3 avg)
% Number of connectives : 222 ( 81 ~; 75 |; 58 &)
% ( 3 <=>; 5 =>; 0 <=; 0 <~>)
% Maximal formula depth : 16 ( 5 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 6 ( 5 usr; 1 prp; 0-3 aty)
% Number of functors : 9 ( 9 usr; 4 con; 0-7 aty)
% Number of variables : 148 ( 0 sgn 96 !; 28 ?)
% Comments :
%------------------------------------------------------------------------------
fof(compose_function,axiom,
! [G,F,A,B,C,X,Z] :
( ( member(Z,C)
& member(X,A) )
=> ( apply(compose_function(G,F,A,B,C),X,Z)
<=> ? [Y] :
( apply(G,Y,Z)
& apply(F,X,Y)
& member(Y,B) ) ) ),
file('SET006+1.ax',compose_function) ).
fof(identity,axiom,
! [F,A] :
( identity(F,A)
<=> ! [X] :
( member(X,A)
=> apply(F,X,X) ) ),
file('SET006+1.ax',identity) ).
fof(surjective,axiom,
! [F,A,B] :
( surjective(F,A,B)
<=> ! [Y] :
( member(Y,B)
=> ? [E] :
( apply(F,E,Y)
& member(E,A) ) ) ),
file('SET006+1.ax',surjective) ).
fof(thII25,conjecture,
! [F,G,A,B] :
( ( identity(compose_function(G,F,B,A,B),B)
& maps(F,B,A)
& maps(G,A,B) )
=> surjective(G,A,B) ),
file('theBenchmark.p',thII25) ).
fof(f_14_1,plain,
! [G,F,A,B,C,X,Z] :
( ( ( apply(compose_function(G,F,A,B,C),X,Z)
| ! [Y] :
( ~ apply(G,Y,Z)
| ~ apply(F,X,Y)
| ~ member(Y,B) ) )
& ( ? [Y] :
( apply(G,Y,Z)
& apply(F,X,Y)
& member(Y,B) )
| ~ apply(compose_function(G,F,A,B,C),X,Z) ) )
| ~ member(Z,C)
| ~ member(X,A) ),
inference(fof_nnf,[status(thm)],[compose_function]) ).
fof(f_14_2,plain,
! [U_132,U_131,U_130,U_129,U_128,U_127,U_126] :
( ( ( apply(compose_function(U_132,U_131,U_130,U_129,U_128),U_127,U_126)
| ! [U_125] :
( ~ apply(U_132,U_125,U_126)
| ~ apply(U_131,U_127,U_125)
| ~ member(U_125,U_129) ) )
& ( ? [U_124] :
( apply(U_132,U_124,U_126)
& apply(U_131,U_127,U_124)
& member(U_124,U_129) )
| ~ apply(compose_function(U_132,U_131,U_130,U_129,U_128),U_127,U_126) ) )
| ~ member(U_126,U_128)
| ~ member(U_127,U_130) ),
inference(variable_rename,[status(thm)],[f_14_1]) ).
fof(f_14_3,plain,
! [U_132,U_131,U_130,U_129,U_128,U_127,U_126] :
( ( ( apply(compose_function(U_132,U_131,U_130,U_129,U_128),U_127,U_126)
| ! [U_125] :
( ~ apply(U_132,U_125,U_126)
| ~ apply(U_131,U_127,U_125)
| ~ member(U_125,U_129) ) )
& ( ( apply(U_132,sK13(U_132,U_131,U_130,U_129,U_128,U_127,U_126),U_126)
& apply(U_131,U_127,sK13(U_132,U_131,U_130,U_129,U_128,U_127,U_126))
& member(sK13(U_132,U_131,U_130,U_129,U_128,U_127,U_126),U_129) )
| ~ apply(compose_function(U_132,U_131,U_130,U_129,U_128),U_127,U_126) ) )
| ~ member(U_126,U_128)
| ~ member(U_127,U_130) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK13]),skolemize(U_124,sK13(U_132,U_131,U_130,U_129,U_128,U_127,U_126))],[f_14_2]) ).
cnf(f_14_4,plain,
( member(sK13(U_132,U_131,U_130,U_129,U_128,U_127,U_126),U_129)
| ~ apply(compose_function(U_132,U_131,U_130,U_129,U_128),U_127,U_126)
| ~ member(U_126,U_128)
| ~ member(U_127,U_130) ),
inference(clausify,[status(thm)],[f_14_3]) ).
cnf(f_14_6,plain,
( apply(U_132,sK13(U_132,U_131,U_130,U_129,U_128,U_127,U_126),U_126)
| ~ apply(compose_function(U_132,U_131,U_130,U_129,U_128),U_127,U_126)
| ~ member(U_126,U_128)
| ~ member(U_127,U_130) ),
inference(clausify,[status(thm)],[f_14_3]) ).
fof(f_16_1,plain,
! [F,A] :
( ( identity(F,A)
| ? [X] :
( ~ apply(F,X,X)
& member(X,A) ) )
& ( ! [X] :
( apply(F,X,X)
| ~ member(X,A) )
| ~ identity(F,A) ) ),
inference(fof_nnf,[status(thm)],[identity]) ).
fof(f_16_2,plain,
! [U_154,U_153] :
( ( identity(U_154,U_153)
| ? [U_152] :
( ~ apply(U_154,U_152,U_152)
& member(U_152,U_153) ) )
& ( ! [U_151] :
( apply(U_154,U_151,U_151)
| ~ member(U_151,U_153) )
| ~ identity(U_154,U_153) ) ),
inference(variable_rename,[status(thm)],[f_16_1]) ).
fof(f_16_3,plain,
( ! [U_158,U_156] :
( identity(U_158,U_156)
| ? [U_152] :
( ~ apply(U_158,U_152,U_152)
& member(U_152,U_156) ) )
& ! [U_157,U_155] :
( ! [U_151] :
( apply(U_157,U_151,U_151)
| ~ member(U_151,U_155) )
| ~ identity(U_157,U_155) ) ),
inference(miniscope,[status(thm)],[f_16_2]) ).
fof(f_16_4,plain,
( ! [U_158,U_156] :
( identity(U_158,U_156)
| ( ~ apply(U_158,sK17(U_158,U_156),sK17(U_158,U_156))
& member(sK17(U_158,U_156),U_156) ) )
& ! [U_157,U_155] :
( ! [U_151] :
( apply(U_157,U_151,U_151)
| ~ member(U_151,U_155) )
| ~ identity(U_157,U_155) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK17]),skolemize(U_152,sK17(U_158,U_156))],[f_16_3]) ).
cnf(f_16_5,plain,
( apply(U_157,U_151,U_151)
| ~ member(U_151,U_155)
| ~ identity(U_157,U_155) ),
inference(clausify,[status(thm)],[f_16_4]) ).
fof(f_18_1,plain,
! [F,A,B] :
( ( surjective(F,A,B)
| ? [Y] :
( ! [E] :
( ~ apply(F,E,Y)
| ~ member(E,A) )
& member(Y,B) ) )
& ( ! [Y] :
( ? [E] :
( apply(F,E,Y)
& member(E,A) )
| ~ member(Y,B) )
| ~ surjective(F,A,B) ) ),
inference(fof_nnf,[status(thm)],[surjective]) ).
fof(f_18_2,plain,
! [U_180,U_179,U_178] :
( ( surjective(U_180,U_179,U_178)
| ? [U_177] :
( ! [U_176] :
( ~ apply(U_180,U_176,U_177)
| ~ member(U_176,U_179) )
& member(U_177,U_178) ) )
& ( ! [U_175] :
( ? [U_174] :
( apply(U_180,U_174,U_175)
& member(U_174,U_179) )
| ~ member(U_175,U_178) )
| ~ surjective(U_180,U_179,U_178) ) ),
inference(variable_rename,[status(thm)],[f_18_1]) ).
fof(f_18_3,plain,
( ! [U_186,U_184,U_182] :
( surjective(U_186,U_184,U_182)
| ? [U_177] :
( ! [U_176] :
( ~ apply(U_186,U_176,U_177)
| ~ member(U_176,U_184) )
& member(U_177,U_182) ) )
& ! [U_185,U_183,U_181] :
( ! [U_175] :
( ? [U_174] :
( apply(U_185,U_174,U_175)
& member(U_174,U_183) )
| ~ member(U_175,U_181) )
| ~ surjective(U_185,U_183,U_181) ) ),
inference(miniscope,[status(thm)],[f_18_2]) ).
fof(f_18_4,plain,
( ! [U_186,U_184,U_182] :
( surjective(U_186,U_184,U_182)
| ? [U_177] :
( ! [U_176] :
( ~ apply(U_186,U_176,U_177)
| ~ member(U_176,U_184) )
& member(U_177,U_182) ) )
& ! [U_185,U_183,U_181] :
( ! [U_175] :
( ( apply(U_185,sK21(U_185,U_183,U_181,U_175),U_175)
& member(sK21(U_185,U_183,U_181,U_175),U_183) )
| ~ member(U_175,U_181) )
| ~ surjective(U_185,U_183,U_181) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK21]),skolemize(U_174,sK21(U_185,U_183,U_181,U_175))],[f_18_3]) ).
fof(f_18_5,plain,
( ! [U_186,U_184,U_182] :
( surjective(U_186,U_184,U_182)
| ( ! [U_176] :
( ~ apply(U_186,U_176,sK22(U_186,U_184,U_182))
| ~ member(U_176,U_184) )
& member(sK22(U_186,U_184,U_182),U_182) ) )
& ! [U_185,U_183,U_181] :
( ! [U_175] :
( ( apply(U_185,sK21(U_185,U_183,U_181,U_175),U_175)
& member(sK21(U_185,U_183,U_181,U_175),U_183) )
| ~ member(U_175,U_181) )
| ~ surjective(U_185,U_183,U_181) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK22]),skolemize(U_177,sK22(U_186,U_184,U_182))],[f_18_4]) ).
cnf(f_18_8,plain,
( member(sK22(U_186,U_184,U_182),U_182)
| surjective(U_186,U_184,U_182) ),
inference(clausify,[status(thm)],[f_18_5]) ).
cnf(f_18_9,plain,
( ~ apply(U_186,U_176,sK22(U_186,U_184,U_182))
| ~ member(U_176,U_184)
| surjective(U_186,U_184,U_182) ),
inference(clausify,[status(thm)],[f_18_5]) ).
fof(f_29_1,negated_conjecture,
~ ! [F,G,A,B] :
( ( identity(compose_function(G,F,B,A,B),B)
& maps(F,B,A)
& maps(G,A,B) )
=> surjective(G,A,B) ),
inference(negate,[status(cth)],[thII25]) ).
fof(f_29_2,negated_conjecture,
? [F,G,A,B] :
( ~ surjective(G,A,B)
& identity(compose_function(G,F,B,A,B),B)
& maps(F,B,A)
& maps(G,A,B) ),
inference(fof_nnf,[status(thm)],[f_29_1]) ).
fof(f_29_3,negated_conjecture,
? [U_339,U_338,U_337,U_336] :
( ~ surjective(U_338,U_337,U_336)
& identity(compose_function(U_338,U_339,U_336,U_337,U_336),U_336)
& maps(U_339,U_336,U_337)
& maps(U_338,U_337,U_336) ),
inference(variable_rename,[status(thm)],[f_29_2]) ).
fof(f_29_4,negated_conjecture,
? [U_338,U_337,U_336] :
( ~ surjective(U_338,U_337,U_336)
& identity(compose_function(U_338,sK41,U_336,U_337,U_336),U_336)
& maps(sK41,U_336,U_337)
& maps(U_338,U_337,U_336) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK41]),skolemize(U_339,sK41)],[f_29_3]) ).
fof(f_29_5,negated_conjecture,
? [U_337,U_336] :
( ~ surjective(sK42,U_337,U_336)
& identity(compose_function(sK42,sK41,U_336,U_337,U_336),U_336)
& maps(sK41,U_336,U_337)
& maps(sK42,U_337,U_336) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK42]),skolemize(U_338,sK42)],[f_29_4]) ).
fof(f_29_6,negated_conjecture,
? [U_336] :
( ~ surjective(sK42,sK43,U_336)
& identity(compose_function(sK42,sK41,U_336,sK43,U_336),U_336)
& maps(sK41,U_336,sK43)
& maps(sK42,sK43,U_336) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK43]),skolemize(U_337,sK43)],[f_29_5]) ).
fof(f_29_7,negated_conjecture,
( ~ surjective(sK42,sK43,sK44)
& identity(compose_function(sK42,sK41,sK44,sK43,sK44),sK44)
& maps(sK41,sK44,sK43)
& maps(sK42,sK43,sK44) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK44]),skolemize(U_336,sK44)],[f_29_6]) ).
cnf(f_29_10,negated_conjecture,
identity(compose_function(sK42,sK41,sK44,sK43,sK44),sK44),
inference(clausify,[status(thm)],[f_29_7]) ).
cnf(f_29_11,negated_conjecture,
~ surjective(sK42,sK43,sK44),
inference(clausify,[status(thm)],[f_29_7]) ).
cnf(t1,plain,
~ surjective(sK42,sK43,sK44),
inference(start,[status(thm),parent(0:0)],[f_29_11]) ).
cnf(t2,plain,
( ~ member(sK13(sK42,sK41,sK44,sK43,sK44,sK22(sK42,sK43,sK44),sK22(sK42,sK43,sK44)),sK43)
| ~ apply(sK42,sK13(sK42,sK41,sK44,sK43,sK44,sK22(sK42,sK43,sK44),sK22(sK42,sK43,sK44)),sK22(sK42,sK43,sK44))
| surjective(sK42,sK43,sK44) ),
inference(extension,[status(thm),parent(t1:1)],[f_18_9]) ).
cnf(t3,plain,
$false,
inference(connection,[status(thm),parent(t2:1)],[t2:1,t1:1]) ).
cnf(t4,plain,
( ~ member(sK22(sK42,sK43,sK44),sK44)
| ~ apply(compose_function(sK42,sK41,sK44,sK43,sK44),sK22(sK42,sK43,sK44),sK22(sK42,sK43,sK44))
| ~ member(sK22(sK42,sK43,sK44),sK44)
| apply(sK42,sK13(sK42,sK41,sK44,sK43,sK44,sK22(sK42,sK43,sK44),sK22(sK42,sK43,sK44)),sK22(sK42,sK43,sK44)) ),
inference(extension,[status(thm),parent(t2:2)],[f_14_6]) ).
cnf(t5,plain,
$false,
inference(connection,[status(thm),parent(t4:1)],[t4:1,t2:2]) ).
cnf(t6,plain,
( surjective(sK42,sK43,sK44)
| member(sK22(sK42,sK43,sK44),sK44) ),
inference(extension,[status(thm),parent(t4:2)],[f_18_8]) ).
cnf(t7,plain,
$false,
inference(connection,[status(thm),parent(t6:1)],[t6:1,t4:2]) ).
cnf(t8,plain,
$false,
inference(reduction,[status(thm),parent(t6:2)],[t6:2,t1:1]) ).
cnf(l3,lemma,
member(sK22(sK42,sK43,sK44),sK44),
inference(lemma,[status(cth),parent(t4:2),below(t2:2)],[t4:2]) ).
cnf(t9,plain,
( ~ member(sK22(sK42,sK43,sK44),sK44)
| ~ identity(compose_function(sK42,sK41,sK44,sK43,sK44),sK44)
| apply(compose_function(sK42,sK41,sK44,sK43,sK44),sK22(sK42,sK43,sK44),sK22(sK42,sK43,sK44)) ),
inference(extension,[status(thm),parent(t4:3)],[f_16_5]) ).
cnf(t10,plain,
$false,
inference(connection,[status(thm),parent(t9:1)],[t9:1,t4:3]) ).
cnf(t11,plain,
identity(compose_function(sK42,sK41,sK44,sK43,sK44),sK44),
inference(extension,[status(thm),parent(t9:2)],[f_29_10]) ).
cnf(t12,plain,
$false,
inference(connection,[status(thm),parent(t11:1)],[t11:1,t9:2]) ).
cnf(t13,plain,
member(sK22(sK42,sK43,sK44),sK44),
inference(lemma_extension,[status(thm),parent(t9:3)],[l3:1]) ).
cnf(t14,plain,
$false,
inference(connection,[status(thm),parent(t13:1)],[t13:1,t9:3]) ).
cnf(t15,plain,
member(sK22(sK42,sK43,sK44),sK44),
inference(lemma_extension,[status(thm),parent(t4:4)],[l3:1]) ).
cnf(t16,plain,
$false,
inference(connection,[status(thm),parent(t15:1)],[t15:1,t4:4]) ).
cnf(t17,plain,
( ~ member(sK22(sK42,sK43,sK44),sK44)
| ~ apply(compose_function(sK42,sK41,sK44,sK43,sK44),sK22(sK42,sK43,sK44),sK22(sK42,sK43,sK44))
| ~ member(sK22(sK42,sK43,sK44),sK44)
| member(sK13(sK42,sK41,sK44,sK43,sK44,sK22(sK42,sK43,sK44),sK22(sK42,sK43,sK44)),sK43) ),
inference(extension,[status(thm),parent(t2:3)],[f_14_4]) ).
cnf(t18,plain,
$false,
inference(connection,[status(thm),parent(t17:1)],[t17:1,t2:3]) ).
cnf(t19,plain,
( surjective(sK42,sK43,sK44)
| member(sK22(sK42,sK43,sK44),sK44) ),
inference(extension,[status(thm),parent(t17:2)],[f_18_8]) ).
cnf(t20,plain,
$false,
inference(connection,[status(thm),parent(t19:1)],[t19:1,t17:2]) ).
cnf(t21,plain,
$false,
inference(reduction,[status(thm),parent(t19:2)],[t19:2,t1:1]) ).
cnf(l8,lemma,
member(sK22(sK42,sK43,sK44),sK44),
inference(lemma,[status(cth),parent(t17:2),below(t2:3)],[t17:2]) ).
cnf(t22,plain,
( ~ member(sK22(sK42,sK43,sK44),sK44)
| ~ identity(compose_function(sK42,sK41,sK44,sK43,sK44),sK44)
| apply(compose_function(sK42,sK41,sK44,sK43,sK44),sK22(sK42,sK43,sK44),sK22(sK42,sK43,sK44)) ),
inference(extension,[status(thm),parent(t17:3)],[f_16_5]) ).
cnf(t23,plain,
$false,
inference(connection,[status(thm),parent(t22:1)],[t22:1,t17:3]) ).
cnf(t24,plain,
identity(compose_function(sK42,sK41,sK44,sK43,sK44),sK44),
inference(extension,[status(thm),parent(t22:2)],[f_29_10]) ).
cnf(t25,plain,
$false,
inference(connection,[status(thm),parent(t24:1)],[t24:1,t22:2]) ).
cnf(t26,plain,
member(sK22(sK42,sK43,sK44),sK44),
inference(lemma_extension,[status(thm),parent(t22:3)],[l8:1]) ).
cnf(t27,plain,
$false,
inference(connection,[status(thm),parent(t26:1)],[t26:1,t22:3]) ).
cnf(t28,plain,
member(sK22(sK42,sK43,sK44),sK44),
inference(lemma_extension,[status(thm),parent(t17:4)],[l8:1]) ).
cnf(t29,plain,
$false,
inference(connection,[status(thm),parent(t28:1)],[t28:1,t17:4]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SET734+4 : TPTP v9.3.1. Bugfixed v2.2.1.
% 0.00/0.03 This is a FOF_THM_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.10/0.37 % Computer : n010.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Sat Sep 19 22:51:08 UTC 2026
% 0.10/0.37 % CPUTime :
% 85.27/85.53 % SZS status Theorem for theBenchmark
% 85.27/85.53 % SZS output start Proof for theBenchmark
% See solution above
%------------------------------------------------------------------------------