%------------------------------------------------------------------------------
% File : ConnectPP---0.7.2
% Problem : SET720+4 : TPTP v9.3.1. Bugfixed v2.2.1.
% 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 : n015.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 228.14s 228.44s
% Output : Proof 228.96s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
fof(subset,axiom,
! [A,B] :
( subset(A,B)
<=> ! [X] :
( member(X,A)
=> member(X,B) ) ),
file('SET006+0.ax',subset) ).
fof(equal_set,axiom,
! [A,B] :
( equal_set(A,B)
<=> ( subset(B,A)
& subset(A,B) ) ),
file('SET006+0.ax',equal_set) ).
fof(power_set,axiom,
! [X,A] :
( member(X,power_set(A))
<=> subset(X,A) ),
file('SET006+0.ax',power_set) ).
fof(intersection,axiom,
! [X,A,B] :
( member(X,intersection(A,B))
<=> ( member(X,B)
& member(X,A) ) ),
file('SET006+0.ax',intersection) ).
fof(union,axiom,
! [X,A,B] :
( member(X,union(A,B))
<=> ( member(X,B)
| member(X,A) ) ),
file('SET006+0.ax',union) ).
fof(empty_set,axiom,
! [X] : ~ member(X,empty_set),
file('SET006+0.ax',empty_set) ).
fof(difference,axiom,
! [B,A,E] :
( member(B,difference(E,A))
<=> ( ~ member(B,A)
& member(B,E) ) ),
file('SET006+0.ax',difference) ).
fof(singleton,axiom,
! [X,A] :
( member(X,singleton(A))
<=> X = A ),
file('SET006+0.ax',singleton) ).
fof(unordered_pair,axiom,
! [X,A,B] :
( member(X,unordered_pair(A,B))
<=> ( X = B
| X = A ) ),
file('SET006+0.ax',unordered_pair) ).
fof(sum,axiom,
! [X,A] :
( member(X,sum(A))
<=> ? [Y] :
( member(X,Y)
& member(Y,A) ) ),
file('SET006+0.ax',sum) ).
fof(product,axiom,
! [X,A] :
( member(X,product(A))
<=> ! [Y] :
( member(Y,A)
=> member(X,Y) ) ),
file('SET006+0.ax',product) ).
fof(maps,axiom,
! [F,A,B] :
( maps(F,A,B)
<=> ( ! [X,Y1,Y2] :
( ( member(Y2,B)
& member(Y1,B)
& member(X,A) )
=> ( ( apply(F,X,Y2)
& apply(F,X,Y1) )
=> Y1 = Y2 ) )
& ! [X] :
( member(X,A)
=> ? [Y] :
( apply(F,X,Y)
& member(Y,B) ) ) ) ),
file('SET006+1.ax',maps) ).
fof(compose_predicate,axiom,
! [H,G,F,A,B,C] :
( compose_predicate(H,G,F,A,B,C)
<=> ! [X,Z] :
( ( member(Z,C)
& member(X,A) )
=> ( apply(H,X,Z)
<=> ? [Y] :
( apply(G,Y,Z)
& apply(F,X,Y)
& member(Y,B) ) ) ) ),
file('SET006+1.ax',compose_predicate) ).
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(equal_maps,axiom,
! [F,G,A,B] :
( equal_maps(F,G,A,B)
<=> ! [X,Y1,Y2] :
( ( member(Y2,B)
& member(Y1,B)
& member(X,A) )
=> ( ( apply(G,X,Y2)
& apply(F,X,Y1) )
=> Y1 = Y2 ) ) ),
file('SET006+1.ax',equal_maps) ).
fof(identity,axiom,
! [F,A] :
( identity(F,A)
<=> ! [X] :
( member(X,A)
=> apply(F,X,X) ) ),
file('SET006+1.ax',identity) ).
fof(injective,axiom,
! [F,A,B] :
( injective(F,A,B)
<=> ! [X1,X2,Y] :
( ( member(Y,B)
& member(X2,A)
& member(X1,A) )
=> ( ( apply(F,X2,Y)
& apply(F,X1,Y) )
=> X1 = X2 ) ) ),
file('SET006+1.ax',injective) ).
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(one_to_one,axiom,
! [F,A,B] :
( one_to_one(F,A,B)
<=> ( surjective(F,A,B)
& injective(F,A,B) ) ),
file('SET006+1.ax',one_to_one) ).
fof(inverse_predicate,axiom,
! [G,F,A,B] :
( inverse_predicate(G,F,A,B)
<=> ! [X,Y] :
( ( member(Y,B)
& member(X,A) )
=> ( apply(F,X,Y)
<=> apply(G,Y,X) ) ) ),
file('SET006+1.ax',inverse_predicate) ).
fof(inverse_function,axiom,
! [F,A,B,X,Y] :
( ( member(Y,B)
& member(X,A) )
=> ( apply(F,X,Y)
<=> apply(inverse_function(F,A,B),Y,X) ) ),
file('SET006+1.ax',inverse_function) ).
fof(image2,axiom,
! [F,A,Y] :
( member(Y,image2(F,A))
<=> ? [X] :
( apply(F,X,Y)
& member(X,A) ) ),
file('SET006+1.ax',image2) ).
fof(image3,axiom,
! [F,A,B,Y] :
( member(Y,image3(F,A,B))
<=> ( ? [X] :
( apply(F,X,Y)
& member(X,A) )
& member(Y,B) ) ),
file('SET006+1.ax',image3) ).
fof(inverse_image2,axiom,
! [F,B,X] :
( member(X,inverse_image2(F,B))
<=> ? [Y] :
( apply(F,X,Y)
& member(Y,B) ) ),
file('SET006+1.ax',inverse_image2) ).
fof(inverse_image3,axiom,
! [F,B,A,X] :
( member(X,inverse_image3(F,B,A))
<=> ( ? [Y] :
( apply(F,X,Y)
& member(Y,B) )
& member(X,A) ) ),
file('SET006+1.ax',inverse_image3) ).
fof(increasing_function,axiom,
! [F,A,R,B,S] :
( increasing(F,A,R,B,S)
<=> ! [X1,Y1,X2,Y2] :
( ( apply(F,X2,Y2)
& apply(F,X1,Y1)
& apply(R,X1,X2)
& member(Y2,B)
& member(X2,A)
& member(Y1,B)
& member(X1,A) )
=> apply(S,Y1,Y2) ) ),
file('SET006+1.ax',increasing_function) ).
fof(decreasing_function,axiom,
! [F,A,R,B,S] :
( decreasing(F,A,R,B,S)
<=> ! [X1,Y1,X2,Y2] :
( ( apply(F,X2,Y2)
& apply(F,X1,Y1)
& apply(R,X1,X2)
& member(Y2,B)
& member(X2,A)
& member(Y1,B)
& member(X1,A) )
=> apply(S,Y2,Y1) ) ),
file('SET006+1.ax',decreasing_function) ).
fof(isomorphism,axiom,
! [F,A,R,B,S] :
( isomorphism(F,A,R,B,S)
<=> ( ! [X1,Y1,X2,Y2] :
( ( apply(F,X2,Y2)
& apply(F,X1,Y1)
& member(Y2,B)
& member(X2,A)
& member(Y1,B)
& member(X1,A) )
=> ( apply(R,X1,X2)
<=> apply(S,Y1,Y2) ) )
& one_to_one(F,A,B)
& maps(F,A,B) ) ),
file('SET006+1.ax',isomorphism) ).
fof(thII11,conjecture,
! [F,A,B] :
( ( one_to_one(F,A,B)
& maps(F,A,B) )
=> equal_maps(inverse_function(inverse_function(F,A,B),B,A),F,A,B) ),
file('theBenchmark.p',thII11) ).
fof(f_1_1,plain,
! [A,B] :
( ( subset(A,B)
| ? [X] :
( ~ member(X,B)
& member(X,A) ) )
& ( ! [X] :
( member(X,B)
| ~ member(X,A) )
| ~ subset(A,B) ) ),
inference(fof_nnf,[status(thm)],[subset]) ).
fof(f_1_2,plain,
! [U_3,U_2] :
( ( subset(U_3,U_2)
| ? [U_1] :
( ~ member(U_1,U_2)
& member(U_1,U_3) ) )
& ( ! [U_0] :
( member(U_0,U_2)
| ~ member(U_0,U_3) )
| ~ subset(U_3,U_2) ) ),
inference(variable_rename,[status(thm)],[f_1_1]) ).
fof(f_1_3,plain,
( ! [U_7,U_5] :
( subset(U_7,U_5)
| ? [U_1] :
( ~ member(U_1,U_5)
& member(U_1,U_7) ) )
& ! [U_6,U_4] :
( ! [U_0] :
( member(U_0,U_4)
| ~ member(U_0,U_6) )
| ~ subset(U_6,U_4) ) ),
inference(miniscope,[status(thm)],[f_1_2]) ).
fof(f_1_4,plain,
( ! [U_7,U_5] :
( subset(U_7,U_5)
| ( ~ member(sK1(U_7,U_5),U_5)
& member(sK1(U_7,U_5),U_7) ) )
& ! [U_6,U_4] :
( ! [U_0] :
( member(U_0,U_4)
| ~ member(U_0,U_6) )
| ~ subset(U_6,U_4) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1]),skolemize(U_1,sK1(U_7,U_5))],[f_1_3]) ).
cnf(f_1_5,plain,
( member(U_0,U_4)
| ~ member(U_0,U_6)
| ~ subset(U_6,U_4) ),
inference(clausify,[status(thm)],[f_1_4]) ).
cnf(f_1_6,plain,
( member(sK1(U_7,U_5),U_7)
| subset(U_7,U_5) ),
inference(clausify,[status(thm)],[f_1_4]) ).
cnf(f_1_7,plain,
( ~ member(sK1(U_7,U_5),U_5)
| subset(U_7,U_5) ),
inference(clausify,[status(thm)],[f_1_4]) ).
fof(f_2_1,plain,
! [A,B] :
( ( equal_set(A,B)
| ~ subset(B,A)
| ~ subset(A,B) )
& ( ( subset(B,A)
& subset(A,B) )
| ~ equal_set(A,B) ) ),
inference(fof_nnf,[status(thm)],[equal_set]) ).
fof(f_2_2,plain,
! [U_9,U_8] :
( ( equal_set(U_9,U_8)
| ~ subset(U_8,U_9)
| ~ subset(U_9,U_8) )
& ( ( subset(U_8,U_9)
& subset(U_9,U_8) )
| ~ equal_set(U_9,U_8) ) ),
inference(variable_rename,[status(thm)],[f_2_1]) ).
fof(f_2_3,plain,
( ! [U_13,U_11] :
( equal_set(U_13,U_11)
| ~ subset(U_11,U_13)
| ~ subset(U_13,U_11) )
& ! [U_12,U_10] :
( ( subset(U_10,U_12)
& subset(U_12,U_10) )
| ~ equal_set(U_12,U_10) ) ),
inference(miniscope,[status(thm)],[f_2_2]) ).
cnf(f_2_4,plain,
( subset(U_12,U_10)
| ~ equal_set(U_12,U_10) ),
inference(clausify,[status(thm)],[f_2_3]) ).
cnf(f_2_5,plain,
( subset(U_10,U_12)
| ~ equal_set(U_12,U_10) ),
inference(clausify,[status(thm)],[f_2_3]) ).
cnf(f_2_6,plain,
( equal_set(U_13,U_11)
| ~ subset(U_11,U_13)
| ~ subset(U_13,U_11) ),
inference(clausify,[status(thm)],[f_2_3]) ).
fof(f_3_1,plain,
! [X,A] :
( ( member(X,power_set(A))
| ~ subset(X,A) )
& ( subset(X,A)
| ~ member(X,power_set(A)) ) ),
inference(fof_nnf,[status(thm)],[power_set]) ).
fof(f_3_2,plain,
! [U_15,U_14] :
( ( member(U_15,power_set(U_14))
| ~ subset(U_15,U_14) )
& ( subset(U_15,U_14)
| ~ member(U_15,power_set(U_14)) ) ),
inference(variable_rename,[status(thm)],[f_3_1]) ).
fof(f_3_3,plain,
( ! [U_19,U_17] :
( member(U_19,power_set(U_17))
| ~ subset(U_19,U_17) )
& ! [U_18,U_16] :
( subset(U_18,U_16)
| ~ member(U_18,power_set(U_16)) ) ),
inference(miniscope,[status(thm)],[f_3_2]) ).
cnf(f_3_4,plain,
( subset(U_18,U_16)
| ~ member(U_18,power_set(U_16)) ),
inference(clausify,[status(thm)],[f_3_3]) ).
cnf(f_3_5,plain,
( member(U_19,power_set(U_17))
| ~ subset(U_19,U_17) ),
inference(clausify,[status(thm)],[f_3_3]) ).
fof(f_4_1,plain,
! [X,A,B] :
( ( member(X,intersection(A,B))
| ~ member(X,B)
| ~ member(X,A) )
& ( ( member(X,B)
& member(X,A) )
| ~ member(X,intersection(A,B)) ) ),
inference(fof_nnf,[status(thm)],[intersection]) ).
fof(f_4_2,plain,
! [U_22,U_21,U_20] :
( ( member(U_22,intersection(U_21,U_20))
| ~ member(U_22,U_20)
| ~ member(U_22,U_21) )
& ( ( member(U_22,U_20)
& member(U_22,U_21) )
| ~ member(U_22,intersection(U_21,U_20)) ) ),
inference(variable_rename,[status(thm)],[f_4_1]) ).
fof(f_4_3,plain,
( ! [U_28,U_26,U_24] :
( member(U_28,intersection(U_26,U_24))
| ~ member(U_28,U_24)
| ~ member(U_28,U_26) )
& ! [U_27,U_25,U_23] :
( ( member(U_27,U_23)
& member(U_27,U_25) )
| ~ member(U_27,intersection(U_25,U_23)) ) ),
inference(miniscope,[status(thm)],[f_4_2]) ).
cnf(f_4_4,plain,
( member(U_27,U_25)
| ~ member(U_27,intersection(U_25,U_23)) ),
inference(clausify,[status(thm)],[f_4_3]) ).
cnf(f_4_5,plain,
( member(U_27,U_23)
| ~ member(U_27,intersection(U_25,U_23)) ),
inference(clausify,[status(thm)],[f_4_3]) ).
cnf(f_4_6,plain,
( member(U_28,intersection(U_26,U_24))
| ~ member(U_28,U_24)
| ~ member(U_28,U_26) ),
inference(clausify,[status(thm)],[f_4_3]) ).
fof(f_5_1,plain,
! [X,A,B] :
( ( member(X,union(A,B))
| ( ~ member(X,B)
& ~ member(X,A) ) )
& ( member(X,B)
| member(X,A)
| ~ member(X,union(A,B)) ) ),
inference(fof_nnf,[status(thm)],[union]) ).
fof(f_5_2,plain,
! [U_31,U_30,U_29] :
( ( member(U_31,union(U_30,U_29))
| ( ~ member(U_31,U_29)
& ~ member(U_31,U_30) ) )
& ( member(U_31,U_29)
| member(U_31,U_30)
| ~ member(U_31,union(U_30,U_29)) ) ),
inference(variable_rename,[status(thm)],[f_5_1]) ).
fof(f_5_3,plain,
( ! [U_37,U_35,U_33] :
( member(U_37,union(U_35,U_33))
| ( ~ member(U_37,U_33)
& ~ member(U_37,U_35) ) )
& ! [U_36,U_34,U_32] :
( member(U_36,U_32)
| member(U_36,U_34)
| ~ member(U_36,union(U_34,U_32)) ) ),
inference(miniscope,[status(thm)],[f_5_2]) ).
cnf(f_5_4,plain,
( member(U_36,U_32)
| member(U_36,U_34)
| ~ member(U_36,union(U_34,U_32)) ),
inference(clausify,[status(thm)],[f_5_3]) ).
cnf(f_5_5,plain,
( ~ member(U_37,U_35)
| member(U_37,union(U_35,U_33)) ),
inference(clausify,[status(thm)],[f_5_3]) ).
cnf(f_5_6,plain,
( ~ member(U_37,U_33)
| member(U_37,union(U_35,U_33)) ),
inference(clausify,[status(thm)],[f_5_3]) ).
fof(f_6_1,plain,
! [X] : ~ member(X,empty_set),
inference(fof_nnf,[status(thm)],[empty_set]) ).
fof(f_6_2,plain,
! [U_38] : ~ member(U_38,empty_set),
inference(variable_rename,[status(thm)],[f_6_1]) ).
cnf(f_6_3,plain,
~ member(U_38,empty_set),
inference(clausify,[status(thm)],[f_6_2]) ).
fof(f_7_1,plain,
! [B,A,E] :
( ( member(B,difference(E,A))
| member(B,A)
| ~ member(B,E) )
& ( ( ~ member(B,A)
& member(B,E) )
| ~ member(B,difference(E,A)) ) ),
inference(fof_nnf,[status(thm)],[difference]) ).
fof(f_7_2,plain,
! [U_41,U_40,U_39] :
( ( member(U_41,difference(U_39,U_40))
| member(U_41,U_40)
| ~ member(U_41,U_39) )
& ( ( ~ member(U_41,U_40)
& member(U_41,U_39) )
| ~ member(U_41,difference(U_39,U_40)) ) ),
inference(variable_rename,[status(thm)],[f_7_1]) ).
fof(f_7_3,plain,
( ! [U_47,U_45,U_43] :
( member(U_47,difference(U_43,U_45))
| member(U_47,U_45)
| ~ member(U_47,U_43) )
& ! [U_46,U_44,U_42] :
( ( ~ member(U_46,U_44)
& member(U_46,U_42) )
| ~ member(U_46,difference(U_42,U_44)) ) ),
inference(miniscope,[status(thm)],[f_7_2]) ).
cnf(f_7_4,plain,
( member(U_46,U_42)
| ~ member(U_46,difference(U_42,U_44)) ),
inference(clausify,[status(thm)],[f_7_3]) ).
cnf(f_7_5,plain,
( ~ member(U_46,U_44)
| ~ member(U_46,difference(U_42,U_44)) ),
inference(clausify,[status(thm)],[f_7_3]) ).
cnf(f_7_6,plain,
( member(U_47,difference(U_43,U_45))
| member(U_47,U_45)
| ~ member(U_47,U_43) ),
inference(clausify,[status(thm)],[f_7_3]) ).
fof(f_8_1,plain,
! [X,A] :
( ( member(X,singleton(A))
| X != A )
& ( X = A
| ~ member(X,singleton(A)) ) ),
inference(fof_nnf,[status(thm)],[singleton]) ).
fof(f_8_2,plain,
! [U_49,U_48] :
( ( member(U_49,singleton(U_48))
| U_49 != U_48 )
& ( U_49 = U_48
| ~ member(U_49,singleton(U_48)) ) ),
inference(variable_rename,[status(thm)],[f_8_1]) ).
fof(f_8_3,plain,
( ! [U_53,U_51] :
( member(U_53,singleton(U_51))
| U_53 != U_51 )
& ! [U_52,U_50] :
( U_52 = U_50
| ~ member(U_52,singleton(U_50)) ) ),
inference(miniscope,[status(thm)],[f_8_2]) ).
cnf(f_8_4,plain,
( U_52 = U_50
| ~ member(U_52,singleton(U_50)) ),
inference(clausify,[status(thm)],[f_8_3]) ).
cnf(f_8_5,plain,
( member(U_53,singleton(U_51))
| U_53 != U_51 ),
inference(clausify,[status(thm)],[f_8_3]) ).
fof(f_9_1,plain,
! [X,A,B] :
( ( member(X,unordered_pair(A,B))
| ( X != B
& X != A ) )
& ( X = B
| X = A
| ~ member(X,unordered_pair(A,B)) ) ),
inference(fof_nnf,[status(thm)],[unordered_pair]) ).
fof(f_9_2,plain,
! [U_56,U_55,U_54] :
( ( member(U_56,unordered_pair(U_55,U_54))
| ( U_56 != U_54
& U_56 != U_55 ) )
& ( U_56 = U_54
| U_56 = U_55
| ~ member(U_56,unordered_pair(U_55,U_54)) ) ),
inference(variable_rename,[status(thm)],[f_9_1]) ).
fof(f_9_3,plain,
( ! [U_62,U_60,U_58] :
( member(U_62,unordered_pair(U_60,U_58))
| ( U_62 != U_58
& U_62 != U_60 ) )
& ! [U_61,U_59,U_57] :
( U_61 = U_57
| U_61 = U_59
| ~ member(U_61,unordered_pair(U_59,U_57)) ) ),
inference(miniscope,[status(thm)],[f_9_2]) ).
cnf(f_9_4,plain,
( U_61 = U_57
| U_61 = U_59
| ~ member(U_61,unordered_pair(U_59,U_57)) ),
inference(clausify,[status(thm)],[f_9_3]) ).
cnf(f_9_5,plain,
( U_62 != U_60
| member(U_62,unordered_pair(U_60,U_58)) ),
inference(clausify,[status(thm)],[f_9_3]) ).
cnf(f_9_6,plain,
( U_62 != U_58
| member(U_62,unordered_pair(U_60,U_58)) ),
inference(clausify,[status(thm)],[f_9_3]) ).
fof(f_10_1,plain,
! [X,A] :
( ( member(X,sum(A))
| ! [Y] :
( ~ member(X,Y)
| ~ member(Y,A) ) )
& ( ? [Y] :
( member(X,Y)
& member(Y,A) )
| ~ member(X,sum(A)) ) ),
inference(fof_nnf,[status(thm)],[sum]) ).
fof(f_10_2,plain,
! [U_66,U_65] :
( ( member(U_66,sum(U_65))
| ! [U_64] :
( ~ member(U_66,U_64)
| ~ member(U_64,U_65) ) )
& ( ? [U_63] :
( member(U_66,U_63)
& member(U_63,U_65) )
| ~ member(U_66,sum(U_65)) ) ),
inference(variable_rename,[status(thm)],[f_10_1]) ).
fof(f_10_3,plain,
( ! [U_70,U_68] :
( member(U_70,sum(U_68))
| ! [U_64] :
( ~ member(U_70,U_64)
| ~ member(U_64,U_68) ) )
& ! [U_69,U_67] :
( ? [U_63] :
( member(U_69,U_63)
& member(U_63,U_67) )
| ~ member(U_69,sum(U_67)) ) ),
inference(miniscope,[status(thm)],[f_10_2]) ).
fof(f_10_4,plain,
( ! [U_70,U_68] :
( member(U_70,sum(U_68))
| ! [U_64] :
( ~ member(U_70,U_64)
| ~ member(U_64,U_68) ) )
& ! [U_69,U_67] :
( ( member(U_69,sK2(U_69,U_67))
& member(sK2(U_69,U_67),U_67) )
| ~ member(U_69,sum(U_67)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2]),skolemize(U_63,sK2(U_69,U_67))],[f_10_3]) ).
cnf(f_10_5,plain,
( member(sK2(U_69,U_67),U_67)
| ~ member(U_69,sum(U_67)) ),
inference(clausify,[status(thm)],[f_10_4]) ).
cnf(f_10_6,plain,
( member(U_69,sK2(U_69,U_67))
| ~ member(U_69,sum(U_67)) ),
inference(clausify,[status(thm)],[f_10_4]) ).
cnf(f_10_7,plain,
( member(U_70,sum(U_68))
| ~ member(U_70,U_64)
| ~ member(U_64,U_68) ),
inference(clausify,[status(thm)],[f_10_4]) ).
fof(f_11_1,plain,
! [X,A] :
( ( member(X,product(A))
| ? [Y] :
( ~ member(X,Y)
& member(Y,A) ) )
& ( ! [Y] :
( member(X,Y)
| ~ member(Y,A) )
| ~ member(X,product(A)) ) ),
inference(fof_nnf,[status(thm)],[product]) ).
fof(f_11_2,plain,
! [U_74,U_73] :
( ( member(U_74,product(U_73))
| ? [U_72] :
( ~ member(U_74,U_72)
& member(U_72,U_73) ) )
& ( ! [U_71] :
( member(U_74,U_71)
| ~ member(U_71,U_73) )
| ~ member(U_74,product(U_73)) ) ),
inference(variable_rename,[status(thm)],[f_11_1]) ).
fof(f_11_3,plain,
( ! [U_78,U_76] :
( member(U_78,product(U_76))
| ? [U_72] :
( ~ member(U_78,U_72)
& member(U_72,U_76) ) )
& ! [U_77,U_75] :
( ! [U_71] :
( member(U_77,U_71)
| ~ member(U_71,U_75) )
| ~ member(U_77,product(U_75)) ) ),
inference(miniscope,[status(thm)],[f_11_2]) ).
fof(f_11_4,plain,
( ! [U_78,U_76] :
( member(U_78,product(U_76))
| ( ~ member(U_78,sK3(U_78,U_76))
& member(sK3(U_78,U_76),U_76) ) )
& ! [U_77,U_75] :
( ! [U_71] :
( member(U_77,U_71)
| ~ member(U_71,U_75) )
| ~ member(U_77,product(U_75)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3]),skolemize(U_72,sK3(U_78,U_76))],[f_11_3]) ).
cnf(f_11_5,plain,
( member(U_77,U_71)
| ~ member(U_71,U_75)
| ~ member(U_77,product(U_75)) ),
inference(clausify,[status(thm)],[f_11_4]) ).
cnf(f_11_6,plain,
( member(sK3(U_78,U_76),U_76)
| member(U_78,product(U_76)) ),
inference(clausify,[status(thm)],[f_11_4]) ).
cnf(f_11_7,plain,
( ~ member(U_78,sK3(U_78,U_76))
| member(U_78,product(U_76)) ),
inference(clausify,[status(thm)],[f_11_4]) ).
fof(f_12_1,plain,
! [F,A,B] :
( ( maps(F,A,B)
| ? [X,Y1,Y2] :
( Y1 != Y2
& apply(F,X,Y2)
& apply(F,X,Y1)
& member(Y2,B)
& member(Y1,B)
& member(X,A) )
| ? [X] :
( ! [Y] :
( ~ apply(F,X,Y)
| ~ member(Y,B) )
& member(X,A) ) )
& ( ( ! [X,Y1,Y2] :
( Y1 = Y2
| ~ apply(F,X,Y2)
| ~ apply(F,X,Y1)
| ~ member(Y2,B)
| ~ member(Y1,B)
| ~ member(X,A) )
& ! [X] :
( ? [Y] :
( apply(F,X,Y)
& member(Y,B) )
| ~ member(X,A) ) )
| ~ maps(F,A,B) ) ),
inference(fof_nnf,[status(thm)],[maps]) ).
fof(f_12_2,plain,
! [U_91,U_90,U_89] :
( ( maps(U_91,U_90,U_89)
| ? [U_88,U_87,U_86] :
( U_87 != U_86
& apply(U_91,U_88,U_86)
& apply(U_91,U_88,U_87)
& member(U_86,U_89)
& member(U_87,U_89)
& member(U_88,U_90) )
| ? [U_85] :
( ! [U_84] :
( ~ apply(U_91,U_85,U_84)
| ~ member(U_84,U_89) )
& member(U_85,U_90) ) )
& ( ( ! [U_83,U_82,U_81] :
( U_82 = U_81
| ~ apply(U_91,U_83,U_81)
| ~ apply(U_91,U_83,U_82)
| ~ member(U_81,U_89)
| ~ member(U_82,U_89)
| ~ member(U_83,U_90) )
& ! [U_80] :
( ? [U_79] :
( apply(U_91,U_80,U_79)
& member(U_79,U_89) )
| ~ member(U_80,U_90) ) )
| ~ maps(U_91,U_90,U_89) ) ),
inference(variable_rename,[status(thm)],[f_12_1]) ).
fof(f_12_3,plain,
( ! [U_97,U_95,U_93] :
( maps(U_97,U_95,U_93)
| ? [U_88,U_87,U_86] :
( U_87 != U_86
& apply(U_97,U_88,U_86)
& apply(U_97,U_88,U_87)
& member(U_86,U_93)
& member(U_87,U_93)
& member(U_88,U_95) )
| ? [U_85] :
( ! [U_84] :
( ~ apply(U_97,U_85,U_84)
| ~ member(U_84,U_93) )
& member(U_85,U_95) ) )
& ! [U_96,U_94,U_92] :
( ( ! [U_83,U_82,U_81] :
( U_82 = U_81
| ~ apply(U_96,U_83,U_81)
| ~ apply(U_96,U_83,U_82)
| ~ member(U_81,U_92)
| ~ member(U_82,U_92)
| ~ member(U_83,U_94) )
& ! [U_80] :
( ? [U_79] :
( apply(U_96,U_80,U_79)
& member(U_79,U_92) )
| ~ member(U_80,U_94) ) )
| ~ maps(U_96,U_94,U_92) ) ),
inference(miniscope,[status(thm)],[f_12_2]) ).
fof(f_12_4,plain,
( ! [U_97,U_95,U_93] :
( maps(U_97,U_95,U_93)
| ? [U_88,U_87,U_86] :
( U_87 != U_86
& apply(U_97,U_88,U_86)
& apply(U_97,U_88,U_87)
& member(U_86,U_93)
& member(U_87,U_93)
& member(U_88,U_95) )
| ? [U_85] :
( ! [U_84] :
( ~ apply(U_97,U_85,U_84)
| ~ member(U_84,U_93) )
& member(U_85,U_95) ) )
& ! [U_96,U_94,U_92] :
( ( ! [U_83,U_82,U_81] :
( U_82 = U_81
| ~ apply(U_96,U_83,U_81)
| ~ apply(U_96,U_83,U_82)
| ~ member(U_81,U_92)
| ~ member(U_82,U_92)
| ~ member(U_83,U_94) )
& ! [U_80] :
( ( apply(U_96,U_80,sK4(U_96,U_94,U_92,U_80))
& member(sK4(U_96,U_94,U_92,U_80),U_92) )
| ~ member(U_80,U_94) ) )
| ~ maps(U_96,U_94,U_92) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4]),skolemize(U_79,sK4(U_96,U_94,U_92,U_80))],[f_12_3]) ).
fof(f_12_5,plain,
( ! [U_97,U_95,U_93] :
( maps(U_97,U_95,U_93)
| ? [U_88,U_87,U_86] :
( U_87 != U_86
& apply(U_97,U_88,U_86)
& apply(U_97,U_88,U_87)
& member(U_86,U_93)
& member(U_87,U_93)
& member(U_88,U_95) )
| ( ! [U_84] :
( ~ apply(U_97,sK5(U_97,U_95,U_93),U_84)
| ~ member(U_84,U_93) )
& member(sK5(U_97,U_95,U_93),U_95) ) )
& ! [U_96,U_94,U_92] :
( ( ! [U_83,U_82,U_81] :
( U_82 = U_81
| ~ apply(U_96,U_83,U_81)
| ~ apply(U_96,U_83,U_82)
| ~ member(U_81,U_92)
| ~ member(U_82,U_92)
| ~ member(U_83,U_94) )
& ! [U_80] :
( ( apply(U_96,U_80,sK4(U_96,U_94,U_92,U_80))
& member(sK4(U_96,U_94,U_92,U_80),U_92) )
| ~ member(U_80,U_94) ) )
| ~ maps(U_96,U_94,U_92) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK5]),skolemize(U_85,sK5(U_97,U_95,U_93))],[f_12_4]) ).
fof(f_12_6,plain,
( ! [U_97,U_95,U_93] :
( maps(U_97,U_95,U_93)
| ? [U_87,U_86] :
( U_87 != U_86
& apply(U_97,sK6(U_97,U_95,U_93),U_86)
& apply(U_97,sK6(U_97,U_95,U_93),U_87)
& member(U_86,U_93)
& member(U_87,U_93)
& member(sK6(U_97,U_95,U_93),U_95) )
| ( ! [U_84] :
( ~ apply(U_97,sK5(U_97,U_95,U_93),U_84)
| ~ member(U_84,U_93) )
& member(sK5(U_97,U_95,U_93),U_95) ) )
& ! [U_96,U_94,U_92] :
( ( ! [U_83,U_82,U_81] :
( U_82 = U_81
| ~ apply(U_96,U_83,U_81)
| ~ apply(U_96,U_83,U_82)
| ~ member(U_81,U_92)
| ~ member(U_82,U_92)
| ~ member(U_83,U_94) )
& ! [U_80] :
( ( apply(U_96,U_80,sK4(U_96,U_94,U_92,U_80))
& member(sK4(U_96,U_94,U_92,U_80),U_92) )
| ~ member(U_80,U_94) ) )
| ~ maps(U_96,U_94,U_92) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK6]),skolemize(U_88,sK6(U_97,U_95,U_93))],[f_12_5]) ).
fof(f_12_7,plain,
( ! [U_97,U_95,U_93] :
( maps(U_97,U_95,U_93)
| ? [U_86] :
( sK7(U_97,U_95,U_93) != U_86
& apply(U_97,sK6(U_97,U_95,U_93),U_86)
& apply(U_97,sK6(U_97,U_95,U_93),sK7(U_97,U_95,U_93))
& member(U_86,U_93)
& member(sK7(U_97,U_95,U_93),U_93)
& member(sK6(U_97,U_95,U_93),U_95) )
| ( ! [U_84] :
( ~ apply(U_97,sK5(U_97,U_95,U_93),U_84)
| ~ member(U_84,U_93) )
& member(sK5(U_97,U_95,U_93),U_95) ) )
& ! [U_96,U_94,U_92] :
( ( ! [U_83,U_82,U_81] :
( U_82 = U_81
| ~ apply(U_96,U_83,U_81)
| ~ apply(U_96,U_83,U_82)
| ~ member(U_81,U_92)
| ~ member(U_82,U_92)
| ~ member(U_83,U_94) )
& ! [U_80] :
( ( apply(U_96,U_80,sK4(U_96,U_94,U_92,U_80))
& member(sK4(U_96,U_94,U_92,U_80),U_92) )
| ~ member(U_80,U_94) ) )
| ~ maps(U_96,U_94,U_92) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK7]),skolemize(U_87,sK7(U_97,U_95,U_93))],[f_12_6]) ).
fof(f_12_8,plain,
( ! [U_97,U_95,U_93] :
( maps(U_97,U_95,U_93)
| ( sK7(U_97,U_95,U_93) != sK8(U_97,U_95,U_93)
& apply(U_97,sK6(U_97,U_95,U_93),sK8(U_97,U_95,U_93))
& apply(U_97,sK6(U_97,U_95,U_93),sK7(U_97,U_95,U_93))
& member(sK8(U_97,U_95,U_93),U_93)
& member(sK7(U_97,U_95,U_93),U_93)
& member(sK6(U_97,U_95,U_93),U_95) )
| ( ! [U_84] :
( ~ apply(U_97,sK5(U_97,U_95,U_93),U_84)
| ~ member(U_84,U_93) )
& member(sK5(U_97,U_95,U_93),U_95) ) )
& ! [U_96,U_94,U_92] :
( ( ! [U_83,U_82,U_81] :
( U_82 = U_81
| ~ apply(U_96,U_83,U_81)
| ~ apply(U_96,U_83,U_82)
| ~ member(U_81,U_92)
| ~ member(U_82,U_92)
| ~ member(U_83,U_94) )
& ! [U_80] :
( ( apply(U_96,U_80,sK4(U_96,U_94,U_92,U_80))
& member(sK4(U_96,U_94,U_92,U_80),U_92) )
| ~ member(U_80,U_94) ) )
| ~ maps(U_96,U_94,U_92) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK8]),skolemize(U_86,sK8(U_97,U_95,U_93))],[f_12_7]) ).
cnf(f_12_9,plain,
( member(sK4(U_96,U_94,U_92,U_80),U_92)
| ~ member(U_80,U_94)
| ~ maps(U_96,U_94,U_92) ),
inference(clausify,[status(thm)],[f_12_8]) ).
cnf(f_12_10,plain,
( apply(U_96,U_80,sK4(U_96,U_94,U_92,U_80))
| ~ member(U_80,U_94)
| ~ maps(U_96,U_94,U_92) ),
inference(clausify,[status(thm)],[f_12_8]) ).
cnf(f_12_11,plain,
( U_82 = U_81
| ~ apply(U_96,U_83,U_81)
| ~ apply(U_96,U_83,U_82)
| ~ member(U_81,U_92)
| ~ member(U_82,U_92)
| ~ member(U_83,U_94)
| ~ maps(U_96,U_94,U_92) ),
inference(clausify,[status(thm)],[f_12_8]) ).
cnf(f_12_12,plain,
( member(sK6(U_97,U_95,U_93),U_95)
| member(sK5(U_97,U_95,U_93),U_95)
| maps(U_97,U_95,U_93) ),
inference(clausify,[status(thm)],[f_12_8]) ).
cnf(f_12_13,plain,
( member(sK7(U_97,U_95,U_93),U_93)
| member(sK5(U_97,U_95,U_93),U_95)
| maps(U_97,U_95,U_93) ),
inference(clausify,[status(thm)],[f_12_8]) ).
cnf(f_12_14,plain,
( member(sK8(U_97,U_95,U_93),U_93)
| member(sK5(U_97,U_95,U_93),U_95)
| maps(U_97,U_95,U_93) ),
inference(clausify,[status(thm)],[f_12_8]) ).
cnf(f_12_15,plain,
( apply(U_97,sK6(U_97,U_95,U_93),sK7(U_97,U_95,U_93))
| member(sK5(U_97,U_95,U_93),U_95)
| maps(U_97,U_95,U_93) ),
inference(clausify,[status(thm)],[f_12_8]) ).
cnf(f_12_16,plain,
( apply(U_97,sK6(U_97,U_95,U_93),sK8(U_97,U_95,U_93))
| member(sK5(U_97,U_95,U_93),U_95)
| maps(U_97,U_95,U_93) ),
inference(clausify,[status(thm)],[f_12_8]) ).
cnf(f_12_17,plain,
( sK7(U_97,U_95,U_93) != sK8(U_97,U_95,U_93)
| member(sK5(U_97,U_95,U_93),U_95)
| maps(U_97,U_95,U_93) ),
inference(clausify,[status(thm)],[f_12_8]) ).
cnf(f_12_18,plain,
( member(sK6(U_97,U_95,U_93),U_95)
| ~ apply(U_97,sK5(U_97,U_95,U_93),U_84)
| ~ member(U_84,U_93)
| maps(U_97,U_95,U_93) ),
inference(clausify,[status(thm)],[f_12_8]) ).
cnf(f_12_19,plain,
( member(sK7(U_97,U_95,U_93),U_93)
| ~ apply(U_97,sK5(U_97,U_95,U_93),U_84)
| ~ member(U_84,U_93)
| maps(U_97,U_95,U_93) ),
inference(clausify,[status(thm)],[f_12_8]) ).
cnf(f_12_20,plain,
( member(sK8(U_97,U_95,U_93),U_93)
| ~ apply(U_97,sK5(U_97,U_95,U_93),U_84)
| ~ member(U_84,U_93)
| maps(U_97,U_95,U_93) ),
inference(clausify,[status(thm)],[f_12_8]) ).
cnf(f_12_21,plain,
( apply(U_97,sK6(U_97,U_95,U_93),sK7(U_97,U_95,U_93))
| ~ apply(U_97,sK5(U_97,U_95,U_93),U_84)
| ~ member(U_84,U_93)
| maps(U_97,U_95,U_93) ),
inference(clausify,[status(thm)],[f_12_8]) ).
cnf(f_12_22,plain,
( apply(U_97,sK6(U_97,U_95,U_93),sK8(U_97,U_95,U_93))
| ~ apply(U_97,sK5(U_97,U_95,U_93),U_84)
| ~ member(U_84,U_93)
| maps(U_97,U_95,U_93) ),
inference(clausify,[status(thm)],[f_12_8]) ).
cnf(f_12_23,plain,
( sK7(U_97,U_95,U_93) != sK8(U_97,U_95,U_93)
| ~ apply(U_97,sK5(U_97,U_95,U_93),U_84)
| ~ member(U_84,U_93)
| maps(U_97,U_95,U_93) ),
inference(clausify,[status(thm)],[f_12_8]) ).
fof(f_13_1,plain,
! [H,G,F,A,B,C] :
( ( compose_predicate(H,G,F,A,B,C)
| ? [X,Z] :
( ( ( ~ apply(H,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(H,X,Z) ) )
& member(Z,C)
& member(X,A) ) )
& ( ! [X,Z] :
( ( ( apply(H,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(H,X,Z) ) )
| ~ member(Z,C)
| ~ member(X,A) )
| ~ compose_predicate(H,G,F,A,B,C) ) ),
inference(fof_nnf,[status(thm)],[compose_predicate]) ).
fof(f_13_2,plain,
! [U_111,U_110,U_109,U_108,U_107,U_106] :
( ( compose_predicate(U_111,U_110,U_109,U_108,U_107,U_106)
| ? [U_105,U_104] :
( ( ( ~ apply(U_111,U_105,U_104)
& ? [U_103] :
( apply(U_110,U_103,U_104)
& apply(U_109,U_105,U_103)
& member(U_103,U_107) ) )
| ( ! [U_102] :
( ~ apply(U_110,U_102,U_104)
| ~ apply(U_109,U_105,U_102)
| ~ member(U_102,U_107) )
& apply(U_111,U_105,U_104) ) )
& member(U_104,U_106)
& member(U_105,U_108) ) )
& ( ! [U_101,U_100] :
( ( ( apply(U_111,U_101,U_100)
| ! [U_99] :
( ~ apply(U_110,U_99,U_100)
| ~ apply(U_109,U_101,U_99)
| ~ member(U_99,U_107) ) )
& ( ? [U_98] :
( apply(U_110,U_98,U_100)
& apply(U_109,U_101,U_98)
& member(U_98,U_107) )
| ~ apply(U_111,U_101,U_100) ) )
| ~ member(U_100,U_106)
| ~ member(U_101,U_108) )
| ~ compose_predicate(U_111,U_110,U_109,U_108,U_107,U_106) ) ),
inference(variable_rename,[status(thm)],[f_13_1]) ).
fof(f_13_3,plain,
( ! [U_123,U_121,U_119,U_117,U_115,U_113] :
( compose_predicate(U_123,U_121,U_119,U_117,U_115,U_113)
| ? [U_105,U_104] :
( ( ( ~ apply(U_123,U_105,U_104)
& ? [U_103] :
( apply(U_121,U_103,U_104)
& apply(U_119,U_105,U_103)
& member(U_103,U_115) ) )
| ( ! [U_102] :
( ~ apply(U_121,U_102,U_104)
| ~ apply(U_119,U_105,U_102)
| ~ member(U_102,U_115) )
& apply(U_123,U_105,U_104) ) )
& member(U_104,U_113)
& member(U_105,U_117) ) )
& ! [U_122,U_120,U_118,U_116,U_114,U_112] :
( ! [U_101,U_100] :
( ( ( apply(U_122,U_101,U_100)
| ! [U_99] :
( ~ apply(U_120,U_99,U_100)
| ~ apply(U_118,U_101,U_99)
| ~ member(U_99,U_114) ) )
& ( ? [U_98] :
( apply(U_120,U_98,U_100)
& apply(U_118,U_101,U_98)
& member(U_98,U_114) )
| ~ apply(U_122,U_101,U_100) ) )
| ~ member(U_100,U_112)
| ~ member(U_101,U_116) )
| ~ compose_predicate(U_122,U_120,U_118,U_116,U_114,U_112) ) ),
inference(miniscope,[status(thm)],[f_13_2]) ).
fof(f_13_4,plain,
( ! [U_123,U_121,U_119,U_117,U_115,U_113] :
( compose_predicate(U_123,U_121,U_119,U_117,U_115,U_113)
| ? [U_105,U_104] :
( ( ( ~ apply(U_123,U_105,U_104)
& ? [U_103] :
( apply(U_121,U_103,U_104)
& apply(U_119,U_105,U_103)
& member(U_103,U_115) ) )
| ( ! [U_102] :
( ~ apply(U_121,U_102,U_104)
| ~ apply(U_119,U_105,U_102)
| ~ member(U_102,U_115) )
& apply(U_123,U_105,U_104) ) )
& member(U_104,U_113)
& member(U_105,U_117) ) )
& ! [U_122,U_120,U_118,U_116,U_114,U_112] :
( ! [U_101,U_100] :
( ( ( apply(U_122,U_101,U_100)
| ! [U_99] :
( ~ apply(U_120,U_99,U_100)
| ~ apply(U_118,U_101,U_99)
| ~ member(U_99,U_114) ) )
& ( ( apply(U_120,sK9(U_122,U_120,U_118,U_116,U_114,U_112,U_101,U_100),U_100)
& apply(U_118,U_101,sK9(U_122,U_120,U_118,U_116,U_114,U_112,U_101,U_100))
& member(sK9(U_122,U_120,U_118,U_116,U_114,U_112,U_101,U_100),U_114) )
| ~ apply(U_122,U_101,U_100) ) )
| ~ member(U_100,U_112)
| ~ member(U_101,U_116) )
| ~ compose_predicate(U_122,U_120,U_118,U_116,U_114,U_112) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK9]),skolemize(U_98,sK9(U_122,U_120,U_118,U_116,U_114,U_112,U_101,U_100))],[f_13_3]) ).
fof(f_13_5,plain,
( ! [U_123,U_121,U_119,U_117,U_115,U_113] :
( compose_predicate(U_123,U_121,U_119,U_117,U_115,U_113)
| ? [U_104] :
( ( ( ~ apply(U_123,sK10(U_123,U_121,U_119,U_117,U_115,U_113),U_104)
& ? [U_103] :
( apply(U_121,U_103,U_104)
& apply(U_119,sK10(U_123,U_121,U_119,U_117,U_115,U_113),U_103)
& member(U_103,U_115) ) )
| ( ! [U_102] :
( ~ apply(U_121,U_102,U_104)
| ~ apply(U_119,sK10(U_123,U_121,U_119,U_117,U_115,U_113),U_102)
| ~ member(U_102,U_115) )
& apply(U_123,sK10(U_123,U_121,U_119,U_117,U_115,U_113),U_104) ) )
& member(U_104,U_113)
& member(sK10(U_123,U_121,U_119,U_117,U_115,U_113),U_117) ) )
& ! [U_122,U_120,U_118,U_116,U_114,U_112] :
( ! [U_101,U_100] :
( ( ( apply(U_122,U_101,U_100)
| ! [U_99] :
( ~ apply(U_120,U_99,U_100)
| ~ apply(U_118,U_101,U_99)
| ~ member(U_99,U_114) ) )
& ( ( apply(U_120,sK9(U_122,U_120,U_118,U_116,U_114,U_112,U_101,U_100),U_100)
& apply(U_118,U_101,sK9(U_122,U_120,U_118,U_116,U_114,U_112,U_101,U_100))
& member(sK9(U_122,U_120,U_118,U_116,U_114,U_112,U_101,U_100),U_114) )
| ~ apply(U_122,U_101,U_100) ) )
| ~ member(U_100,U_112)
| ~ member(U_101,U_116) )
| ~ compose_predicate(U_122,U_120,U_118,U_116,U_114,U_112) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK10]),skolemize(U_105,sK10(U_123,U_121,U_119,U_117,U_115,U_113))],[f_13_4]) ).
fof(f_13_6,plain,
( ! [U_123,U_121,U_119,U_117,U_115,U_113] :
( compose_predicate(U_123,U_121,U_119,U_117,U_115,U_113)
| ( ( ( ~ apply(U_123,sK10(U_123,U_121,U_119,U_117,U_115,U_113),sK11(U_123,U_121,U_119,U_117,U_115,U_113))
& ? [U_103] :
( apply(U_121,U_103,sK11(U_123,U_121,U_119,U_117,U_115,U_113))
& apply(U_119,sK10(U_123,U_121,U_119,U_117,U_115,U_113),U_103)
& member(U_103,U_115) ) )
| ( ! [U_102] :
( ~ apply(U_121,U_102,sK11(U_123,U_121,U_119,U_117,U_115,U_113))
| ~ apply(U_119,sK10(U_123,U_121,U_119,U_117,U_115,U_113),U_102)
| ~ member(U_102,U_115) )
& apply(U_123,sK10(U_123,U_121,U_119,U_117,U_115,U_113),sK11(U_123,U_121,U_119,U_117,U_115,U_113)) ) )
& member(sK11(U_123,U_121,U_119,U_117,U_115,U_113),U_113)
& member(sK10(U_123,U_121,U_119,U_117,U_115,U_113),U_117) ) )
& ! [U_122,U_120,U_118,U_116,U_114,U_112] :
( ! [U_101,U_100] :
( ( ( apply(U_122,U_101,U_100)
| ! [U_99] :
( ~ apply(U_120,U_99,U_100)
| ~ apply(U_118,U_101,U_99)
| ~ member(U_99,U_114) ) )
& ( ( apply(U_120,sK9(U_122,U_120,U_118,U_116,U_114,U_112,U_101,U_100),U_100)
& apply(U_118,U_101,sK9(U_122,U_120,U_118,U_116,U_114,U_112,U_101,U_100))
& member(sK9(U_122,U_120,U_118,U_116,U_114,U_112,U_101,U_100),U_114) )
| ~ apply(U_122,U_101,U_100) ) )
| ~ member(U_100,U_112)
| ~ member(U_101,U_116) )
| ~ compose_predicate(U_122,U_120,U_118,U_116,U_114,U_112) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK11]),skolemize(U_104,sK11(U_123,U_121,U_119,U_117,U_115,U_113))],[f_13_5]) ).
fof(f_13_7,plain,
( ! [U_123,U_121,U_119,U_117,U_115,U_113] :
( compose_predicate(U_123,U_121,U_119,U_117,U_115,U_113)
| ( ( ( ~ apply(U_123,sK10(U_123,U_121,U_119,U_117,U_115,U_113),sK11(U_123,U_121,U_119,U_117,U_115,U_113))
& apply(U_121,sK12(U_123,U_121,U_119,U_117,U_115,U_113),sK11(U_123,U_121,U_119,U_117,U_115,U_113))
& apply(U_119,sK10(U_123,U_121,U_119,U_117,U_115,U_113),sK12(U_123,U_121,U_119,U_117,U_115,U_113))
& member(sK12(U_123,U_121,U_119,U_117,U_115,U_113),U_115) )
| ( ! [U_102] :
( ~ apply(U_121,U_102,sK11(U_123,U_121,U_119,U_117,U_115,U_113))
| ~ apply(U_119,sK10(U_123,U_121,U_119,U_117,U_115,U_113),U_102)
| ~ member(U_102,U_115) )
& apply(U_123,sK10(U_123,U_121,U_119,U_117,U_115,U_113),sK11(U_123,U_121,U_119,U_117,U_115,U_113)) ) )
& member(sK11(U_123,U_121,U_119,U_117,U_115,U_113),U_113)
& member(sK10(U_123,U_121,U_119,U_117,U_115,U_113),U_117) ) )
& ! [U_122,U_120,U_118,U_116,U_114,U_112] :
( ! [U_101,U_100] :
( ( ( apply(U_122,U_101,U_100)
| ! [U_99] :
( ~ apply(U_120,U_99,U_100)
| ~ apply(U_118,U_101,U_99)
| ~ member(U_99,U_114) ) )
& ( ( apply(U_120,sK9(U_122,U_120,U_118,U_116,U_114,U_112,U_101,U_100),U_100)
& apply(U_118,U_101,sK9(U_122,U_120,U_118,U_116,U_114,U_112,U_101,U_100))
& member(sK9(U_122,U_120,U_118,U_116,U_114,U_112,U_101,U_100),U_114) )
| ~ apply(U_122,U_101,U_100) ) )
| ~ member(U_100,U_112)
| ~ member(U_101,U_116) )
| ~ compose_predicate(U_122,U_120,U_118,U_116,U_114,U_112) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK12]),skolemize(U_103,sK12(U_123,U_121,U_119,U_117,U_115,U_113))],[f_13_6]) ).
cnf(f_13_8,plain,
( member(sK9(U_122,U_120,U_118,U_116,U_114,U_112,U_101,U_100),U_114)
| ~ apply(U_122,U_101,U_100)
| ~ member(U_100,U_112)
| ~ member(U_101,U_116)
| ~ compose_predicate(U_122,U_120,U_118,U_116,U_114,U_112) ),
inference(clausify,[status(thm)],[f_13_7]) ).
cnf(f_13_9,plain,
( apply(U_118,U_101,sK9(U_122,U_120,U_118,U_116,U_114,U_112,U_101,U_100))
| ~ apply(U_122,U_101,U_100)
| ~ member(U_100,U_112)
| ~ member(U_101,U_116)
| ~ compose_predicate(U_122,U_120,U_118,U_116,U_114,U_112) ),
inference(clausify,[status(thm)],[f_13_7]) ).
cnf(f_13_10,plain,
( apply(U_120,sK9(U_122,U_120,U_118,U_116,U_114,U_112,U_101,U_100),U_100)
| ~ apply(U_122,U_101,U_100)
| ~ member(U_100,U_112)
| ~ member(U_101,U_116)
| ~ compose_predicate(U_122,U_120,U_118,U_116,U_114,U_112) ),
inference(clausify,[status(thm)],[f_13_7]) ).
cnf(f_13_11,plain,
( apply(U_122,U_101,U_100)
| ~ apply(U_120,U_99,U_100)
| ~ apply(U_118,U_101,U_99)
| ~ member(U_99,U_114)
| ~ member(U_100,U_112)
| ~ member(U_101,U_116)
| ~ compose_predicate(U_122,U_120,U_118,U_116,U_114,U_112) ),
inference(clausify,[status(thm)],[f_13_7]) ).
cnf(f_13_12,plain,
( member(sK10(U_123,U_121,U_119,U_117,U_115,U_113),U_117)
| compose_predicate(U_123,U_121,U_119,U_117,U_115,U_113) ),
inference(clausify,[status(thm)],[f_13_7]) ).
cnf(f_13_13,plain,
( member(sK11(U_123,U_121,U_119,U_117,U_115,U_113),U_113)
| compose_predicate(U_123,U_121,U_119,U_117,U_115,U_113) ),
inference(clausify,[status(thm)],[f_13_7]) ).
cnf(f_13_14,plain,
( member(sK12(U_123,U_121,U_119,U_117,U_115,U_113),U_115)
| apply(U_123,sK10(U_123,U_121,U_119,U_117,U_115,U_113),sK11(U_123,U_121,U_119,U_117,U_115,U_113))
| compose_predicate(U_123,U_121,U_119,U_117,U_115,U_113) ),
inference(clausify,[status(thm)],[f_13_7]) ).
cnf(f_13_15,plain,
( apply(U_119,sK10(U_123,U_121,U_119,U_117,U_115,U_113),sK12(U_123,U_121,U_119,U_117,U_115,U_113))
| apply(U_123,sK10(U_123,U_121,U_119,U_117,U_115,U_113),sK11(U_123,U_121,U_119,U_117,U_115,U_113))
| compose_predicate(U_123,U_121,U_119,U_117,U_115,U_113) ),
inference(clausify,[status(thm)],[f_13_7]) ).
cnf(f_13_16,plain,
( apply(U_121,sK12(U_123,U_121,U_119,U_117,U_115,U_113),sK11(U_123,U_121,U_119,U_117,U_115,U_113))
| apply(U_123,sK10(U_123,U_121,U_119,U_117,U_115,U_113),sK11(U_123,U_121,U_119,U_117,U_115,U_113))
| compose_predicate(U_123,U_121,U_119,U_117,U_115,U_113) ),
inference(clausify,[status(thm)],[f_13_7]) ).
cnf(f_13_17,plain,
( ~ apply(U_123,sK10(U_123,U_121,U_119,U_117,U_115,U_113),sK11(U_123,U_121,U_119,U_117,U_115,U_113))
| apply(U_123,sK10(U_123,U_121,U_119,U_117,U_115,U_113),sK11(U_123,U_121,U_119,U_117,U_115,U_113))
| compose_predicate(U_123,U_121,U_119,U_117,U_115,U_113) ),
inference(clausify,[status(thm)],[f_13_7]) ).
cnf(f_13_18,plain,
( member(sK12(U_123,U_121,U_119,U_117,U_115,U_113),U_115)
| ~ apply(U_121,U_102,sK11(U_123,U_121,U_119,U_117,U_115,U_113))
| ~ apply(U_119,sK10(U_123,U_121,U_119,U_117,U_115,U_113),U_102)
| ~ member(U_102,U_115)
| compose_predicate(U_123,U_121,U_119,U_117,U_115,U_113) ),
inference(clausify,[status(thm)],[f_13_7]) ).
cnf(f_13_19,plain,
( apply(U_119,sK10(U_123,U_121,U_119,U_117,U_115,U_113),sK12(U_123,U_121,U_119,U_117,U_115,U_113))
| ~ apply(U_121,U_102,sK11(U_123,U_121,U_119,U_117,U_115,U_113))
| ~ apply(U_119,sK10(U_123,U_121,U_119,U_117,U_115,U_113),U_102)
| ~ member(U_102,U_115)
| compose_predicate(U_123,U_121,U_119,U_117,U_115,U_113) ),
inference(clausify,[status(thm)],[f_13_7]) ).
cnf(f_13_20,plain,
( apply(U_121,sK12(U_123,U_121,U_119,U_117,U_115,U_113),sK11(U_123,U_121,U_119,U_117,U_115,U_113))
| ~ apply(U_121,U_102,sK11(U_123,U_121,U_119,U_117,U_115,U_113))
| ~ apply(U_119,sK10(U_123,U_121,U_119,U_117,U_115,U_113),U_102)
| ~ member(U_102,U_115)
| compose_predicate(U_123,U_121,U_119,U_117,U_115,U_113) ),
inference(clausify,[status(thm)],[f_13_7]) ).
cnf(f_13_21,plain,
( ~ apply(U_123,sK10(U_123,U_121,U_119,U_117,U_115,U_113),sK11(U_123,U_121,U_119,U_117,U_115,U_113))
| ~ apply(U_121,U_102,sK11(U_123,U_121,U_119,U_117,U_115,U_113))
| ~ apply(U_119,sK10(U_123,U_121,U_119,U_117,U_115,U_113),U_102)
| ~ member(U_102,U_115)
| compose_predicate(U_123,U_121,U_119,U_117,U_115,U_113) ),
inference(clausify,[status(thm)],[f_13_7]) ).
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_5,plain,
( apply(U_131,U_127,sK13(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)
| ~ 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]) ).
cnf(f_14_7,plain,
( apply(compose_function(U_132,U_131,U_130,U_129,U_128),U_127,U_126)
| ~ apply(U_132,U_125,U_126)
| ~ apply(U_131,U_127,U_125)
| ~ member(U_125,U_129)
| ~ member(U_126,U_128)
| ~ member(U_127,U_130) ),
inference(clausify,[status(thm)],[f_14_3]) ).
fof(f_15_1,plain,
! [F,G,A,B] :
( ( equal_maps(F,G,A,B)
| ? [X,Y1,Y2] :
( Y1 != Y2
& apply(G,X,Y2)
& apply(F,X,Y1)
& member(Y2,B)
& member(Y1,B)
& member(X,A) ) )
& ( ! [X,Y1,Y2] :
( Y1 = Y2
| ~ apply(G,X,Y2)
| ~ apply(F,X,Y1)
| ~ member(Y2,B)
| ~ member(Y1,B)
| ~ member(X,A) )
| ~ equal_maps(F,G,A,B) ) ),
inference(fof_nnf,[status(thm)],[equal_maps]) ).
fof(f_15_2,plain,
! [U_142,U_141,U_140,U_139] :
( ( equal_maps(U_142,U_141,U_140,U_139)
| ? [U_138,U_137,U_136] :
( U_137 != U_136
& apply(U_141,U_138,U_136)
& apply(U_142,U_138,U_137)
& member(U_136,U_139)
& member(U_137,U_139)
& member(U_138,U_140) ) )
& ( ! [U_135,U_134,U_133] :
( U_134 = U_133
| ~ apply(U_141,U_135,U_133)
| ~ apply(U_142,U_135,U_134)
| ~ member(U_133,U_139)
| ~ member(U_134,U_139)
| ~ member(U_135,U_140) )
| ~ equal_maps(U_142,U_141,U_140,U_139) ) ),
inference(variable_rename,[status(thm)],[f_15_1]) ).
fof(f_15_3,plain,
( ! [U_150,U_148,U_146,U_144] :
( equal_maps(U_150,U_148,U_146,U_144)
| ? [U_138,U_137,U_136] :
( U_137 != U_136
& apply(U_148,U_138,U_136)
& apply(U_150,U_138,U_137)
& member(U_136,U_144)
& member(U_137,U_144)
& member(U_138,U_146) ) )
& ! [U_149,U_147,U_145,U_143] :
( ! [U_135,U_134,U_133] :
( U_134 = U_133
| ~ apply(U_147,U_135,U_133)
| ~ apply(U_149,U_135,U_134)
| ~ member(U_133,U_143)
| ~ member(U_134,U_143)
| ~ member(U_135,U_145) )
| ~ equal_maps(U_149,U_147,U_145,U_143) ) ),
inference(miniscope,[status(thm)],[f_15_2]) ).
fof(f_15_4,plain,
( ! [U_150,U_148,U_146,U_144] :
( equal_maps(U_150,U_148,U_146,U_144)
| ? [U_137,U_136] :
( U_137 != U_136
& apply(U_148,sK14(U_150,U_148,U_146,U_144),U_136)
& apply(U_150,sK14(U_150,U_148,U_146,U_144),U_137)
& member(U_136,U_144)
& member(U_137,U_144)
& member(sK14(U_150,U_148,U_146,U_144),U_146) ) )
& ! [U_149,U_147,U_145,U_143] :
( ! [U_135,U_134,U_133] :
( U_134 = U_133
| ~ apply(U_147,U_135,U_133)
| ~ apply(U_149,U_135,U_134)
| ~ member(U_133,U_143)
| ~ member(U_134,U_143)
| ~ member(U_135,U_145) )
| ~ equal_maps(U_149,U_147,U_145,U_143) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK14]),skolemize(U_138,sK14(U_150,U_148,U_146,U_144))],[f_15_3]) ).
fof(f_15_5,plain,
( ! [U_150,U_148,U_146,U_144] :
( equal_maps(U_150,U_148,U_146,U_144)
| ? [U_136] :
( sK15(U_150,U_148,U_146,U_144) != U_136
& apply(U_148,sK14(U_150,U_148,U_146,U_144),U_136)
& apply(U_150,sK14(U_150,U_148,U_146,U_144),sK15(U_150,U_148,U_146,U_144))
& member(U_136,U_144)
& member(sK15(U_150,U_148,U_146,U_144),U_144)
& member(sK14(U_150,U_148,U_146,U_144),U_146) ) )
& ! [U_149,U_147,U_145,U_143] :
( ! [U_135,U_134,U_133] :
( U_134 = U_133
| ~ apply(U_147,U_135,U_133)
| ~ apply(U_149,U_135,U_134)
| ~ member(U_133,U_143)
| ~ member(U_134,U_143)
| ~ member(U_135,U_145) )
| ~ equal_maps(U_149,U_147,U_145,U_143) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK15]),skolemize(U_137,sK15(U_150,U_148,U_146,U_144))],[f_15_4]) ).
fof(f_15_6,plain,
( ! [U_150,U_148,U_146,U_144] :
( equal_maps(U_150,U_148,U_146,U_144)
| ( sK15(U_150,U_148,U_146,U_144) != sK16(U_150,U_148,U_146,U_144)
& apply(U_148,sK14(U_150,U_148,U_146,U_144),sK16(U_150,U_148,U_146,U_144))
& apply(U_150,sK14(U_150,U_148,U_146,U_144),sK15(U_150,U_148,U_146,U_144))
& member(sK16(U_150,U_148,U_146,U_144),U_144)
& member(sK15(U_150,U_148,U_146,U_144),U_144)
& member(sK14(U_150,U_148,U_146,U_144),U_146) ) )
& ! [U_149,U_147,U_145,U_143] :
( ! [U_135,U_134,U_133] :
( U_134 = U_133
| ~ apply(U_147,U_135,U_133)
| ~ apply(U_149,U_135,U_134)
| ~ member(U_133,U_143)
| ~ member(U_134,U_143)
| ~ member(U_135,U_145) )
| ~ equal_maps(U_149,U_147,U_145,U_143) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK16]),skolemize(U_136,sK16(U_150,U_148,U_146,U_144))],[f_15_5]) ).
cnf(f_15_7,plain,
( U_134 = U_133
| ~ apply(U_147,U_135,U_133)
| ~ apply(U_149,U_135,U_134)
| ~ member(U_133,U_143)
| ~ member(U_134,U_143)
| ~ member(U_135,U_145)
| ~ equal_maps(U_149,U_147,U_145,U_143) ),
inference(clausify,[status(thm)],[f_15_6]) ).
cnf(f_15_8,plain,
( member(sK14(U_150,U_148,U_146,U_144),U_146)
| equal_maps(U_150,U_148,U_146,U_144) ),
inference(clausify,[status(thm)],[f_15_6]) ).
cnf(f_15_9,plain,
( member(sK15(U_150,U_148,U_146,U_144),U_144)
| equal_maps(U_150,U_148,U_146,U_144) ),
inference(clausify,[status(thm)],[f_15_6]) ).
cnf(f_15_10,plain,
( member(sK16(U_150,U_148,U_146,U_144),U_144)
| equal_maps(U_150,U_148,U_146,U_144) ),
inference(clausify,[status(thm)],[f_15_6]) ).
cnf(f_15_11,plain,
( apply(U_150,sK14(U_150,U_148,U_146,U_144),sK15(U_150,U_148,U_146,U_144))
| equal_maps(U_150,U_148,U_146,U_144) ),
inference(clausify,[status(thm)],[f_15_6]) ).
cnf(f_15_12,plain,
( apply(U_148,sK14(U_150,U_148,U_146,U_144),sK16(U_150,U_148,U_146,U_144))
| equal_maps(U_150,U_148,U_146,U_144) ),
inference(clausify,[status(thm)],[f_15_6]) ).
cnf(f_15_13,plain,
( sK15(U_150,U_148,U_146,U_144) != sK16(U_150,U_148,U_146,U_144)
| equal_maps(U_150,U_148,U_146,U_144) ),
inference(clausify,[status(thm)],[f_15_6]) ).
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]) ).
cnf(f_16_6,plain,
( member(sK17(U_158,U_156),U_156)
| identity(U_158,U_156) ),
inference(clausify,[status(thm)],[f_16_4]) ).
cnf(f_16_7,plain,
( ~ apply(U_158,sK17(U_158,U_156),sK17(U_158,U_156))
| identity(U_158,U_156) ),
inference(clausify,[status(thm)],[f_16_4]) ).
fof(f_17_1,plain,
! [F,A,B] :
( ( injective(F,A,B)
| ? [X1,X2,Y] :
( X1 != X2
& apply(F,X2,Y)
& apply(F,X1,Y)
& member(Y,B)
& member(X2,A)
& member(X1,A) ) )
& ( ! [X1,X2,Y] :
( X1 = X2
| ~ apply(F,X2,Y)
| ~ apply(F,X1,Y)
| ~ member(Y,B)
| ~ member(X2,A)
| ~ member(X1,A) )
| ~ injective(F,A,B) ) ),
inference(fof_nnf,[status(thm)],[injective]) ).
fof(f_17_2,plain,
! [U_167,U_166,U_165] :
( ( injective(U_167,U_166,U_165)
| ? [U_164,U_163,U_162] :
( U_164 != U_163
& apply(U_167,U_163,U_162)
& apply(U_167,U_164,U_162)
& member(U_162,U_165)
& member(U_163,U_166)
& member(U_164,U_166) ) )
& ( ! [U_161,U_160,U_159] :
( U_161 = U_160
| ~ apply(U_167,U_160,U_159)
| ~ apply(U_167,U_161,U_159)
| ~ member(U_159,U_165)
| ~ member(U_160,U_166)
| ~ member(U_161,U_166) )
| ~ injective(U_167,U_166,U_165) ) ),
inference(variable_rename,[status(thm)],[f_17_1]) ).
fof(f_17_3,plain,
( ! [U_173,U_171,U_169] :
( injective(U_173,U_171,U_169)
| ? [U_164,U_163,U_162] :
( U_164 != U_163
& apply(U_173,U_163,U_162)
& apply(U_173,U_164,U_162)
& member(U_162,U_169)
& member(U_163,U_171)
& member(U_164,U_171) ) )
& ! [U_172,U_170,U_168] :
( ! [U_161,U_160,U_159] :
( U_161 = U_160
| ~ apply(U_172,U_160,U_159)
| ~ apply(U_172,U_161,U_159)
| ~ member(U_159,U_168)
| ~ member(U_160,U_170)
| ~ member(U_161,U_170) )
| ~ injective(U_172,U_170,U_168) ) ),
inference(miniscope,[status(thm)],[f_17_2]) ).
fof(f_17_4,plain,
( ! [U_173,U_171,U_169] :
( injective(U_173,U_171,U_169)
| ? [U_163,U_162] :
( sK18(U_173,U_171,U_169) != U_163
& apply(U_173,U_163,U_162)
& apply(U_173,sK18(U_173,U_171,U_169),U_162)
& member(U_162,U_169)
& member(U_163,U_171)
& member(sK18(U_173,U_171,U_169),U_171) ) )
& ! [U_172,U_170,U_168] :
( ! [U_161,U_160,U_159] :
( U_161 = U_160
| ~ apply(U_172,U_160,U_159)
| ~ apply(U_172,U_161,U_159)
| ~ member(U_159,U_168)
| ~ member(U_160,U_170)
| ~ member(U_161,U_170) )
| ~ injective(U_172,U_170,U_168) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK18]),skolemize(U_164,sK18(U_173,U_171,U_169))],[f_17_3]) ).
fof(f_17_5,plain,
( ! [U_173,U_171,U_169] :
( injective(U_173,U_171,U_169)
| ? [U_162] :
( sK18(U_173,U_171,U_169) != sK19(U_173,U_171,U_169)
& apply(U_173,sK19(U_173,U_171,U_169),U_162)
& apply(U_173,sK18(U_173,U_171,U_169),U_162)
& member(U_162,U_169)
& member(sK19(U_173,U_171,U_169),U_171)
& member(sK18(U_173,U_171,U_169),U_171) ) )
& ! [U_172,U_170,U_168] :
( ! [U_161,U_160,U_159] :
( U_161 = U_160
| ~ apply(U_172,U_160,U_159)
| ~ apply(U_172,U_161,U_159)
| ~ member(U_159,U_168)
| ~ member(U_160,U_170)
| ~ member(U_161,U_170) )
| ~ injective(U_172,U_170,U_168) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK19]),skolemize(U_163,sK19(U_173,U_171,U_169))],[f_17_4]) ).
fof(f_17_6,plain,
( ! [U_173,U_171,U_169] :
( injective(U_173,U_171,U_169)
| ( sK18(U_173,U_171,U_169) != sK19(U_173,U_171,U_169)
& apply(U_173,sK19(U_173,U_171,U_169),sK20(U_173,U_171,U_169))
& apply(U_173,sK18(U_173,U_171,U_169),sK20(U_173,U_171,U_169))
& member(sK20(U_173,U_171,U_169),U_169)
& member(sK19(U_173,U_171,U_169),U_171)
& member(sK18(U_173,U_171,U_169),U_171) ) )
& ! [U_172,U_170,U_168] :
( ! [U_161,U_160,U_159] :
( U_161 = U_160
| ~ apply(U_172,U_160,U_159)
| ~ apply(U_172,U_161,U_159)
| ~ member(U_159,U_168)
| ~ member(U_160,U_170)
| ~ member(U_161,U_170) )
| ~ injective(U_172,U_170,U_168) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK20]),skolemize(U_162,sK20(U_173,U_171,U_169))],[f_17_5]) ).
cnf(f_17_7,plain,
( U_161 = U_160
| ~ apply(U_172,U_160,U_159)
| ~ apply(U_172,U_161,U_159)
| ~ member(U_159,U_168)
| ~ member(U_160,U_170)
| ~ member(U_161,U_170)
| ~ injective(U_172,U_170,U_168) ),
inference(clausify,[status(thm)],[f_17_6]) ).
cnf(f_17_8,plain,
( member(sK18(U_173,U_171,U_169),U_171)
| injective(U_173,U_171,U_169) ),
inference(clausify,[status(thm)],[f_17_6]) ).
cnf(f_17_9,plain,
( member(sK19(U_173,U_171,U_169),U_171)
| injective(U_173,U_171,U_169) ),
inference(clausify,[status(thm)],[f_17_6]) ).
cnf(f_17_10,plain,
( member(sK20(U_173,U_171,U_169),U_169)
| injective(U_173,U_171,U_169) ),
inference(clausify,[status(thm)],[f_17_6]) ).
cnf(f_17_11,plain,
( apply(U_173,sK18(U_173,U_171,U_169),sK20(U_173,U_171,U_169))
| injective(U_173,U_171,U_169) ),
inference(clausify,[status(thm)],[f_17_6]) ).
cnf(f_17_12,plain,
( apply(U_173,sK19(U_173,U_171,U_169),sK20(U_173,U_171,U_169))
| injective(U_173,U_171,U_169) ),
inference(clausify,[status(thm)],[f_17_6]) ).
cnf(f_17_13,plain,
( sK18(U_173,U_171,U_169) != sK19(U_173,U_171,U_169)
| injective(U_173,U_171,U_169) ),
inference(clausify,[status(thm)],[f_17_6]) ).
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_6,plain,
( 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(clausify,[status(thm)],[f_18_5]) ).
cnf(f_18_7,plain,
( apply(U_185,sK21(U_185,U_183,U_181,U_175),U_175)
| ~ member(U_175,U_181)
| ~ surjective(U_185,U_183,U_181) ),
inference(clausify,[status(thm)],[f_18_5]) ).
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_19_1,plain,
! [F,A,B] :
( ( one_to_one(F,A,B)
| ~ surjective(F,A,B)
| ~ injective(F,A,B) )
& ( ( surjective(F,A,B)
& injective(F,A,B) )
| ~ one_to_one(F,A,B) ) ),
inference(fof_nnf,[status(thm)],[one_to_one]) ).
fof(f_19_2,plain,
! [U_189,U_188,U_187] :
( ( one_to_one(U_189,U_188,U_187)
| ~ surjective(U_189,U_188,U_187)
| ~ injective(U_189,U_188,U_187) )
& ( ( surjective(U_189,U_188,U_187)
& injective(U_189,U_188,U_187) )
| ~ one_to_one(U_189,U_188,U_187) ) ),
inference(variable_rename,[status(thm)],[f_19_1]) ).
fof(f_19_3,plain,
( ! [U_195,U_193,U_191] :
( one_to_one(U_195,U_193,U_191)
| ~ surjective(U_195,U_193,U_191)
| ~ injective(U_195,U_193,U_191) )
& ! [U_194,U_192,U_190] :
( ( surjective(U_194,U_192,U_190)
& injective(U_194,U_192,U_190) )
| ~ one_to_one(U_194,U_192,U_190) ) ),
inference(miniscope,[status(thm)],[f_19_2]) ).
cnf(f_19_4,plain,
( injective(U_194,U_192,U_190)
| ~ one_to_one(U_194,U_192,U_190) ),
inference(clausify,[status(thm)],[f_19_3]) ).
cnf(f_19_5,plain,
( surjective(U_194,U_192,U_190)
| ~ one_to_one(U_194,U_192,U_190) ),
inference(clausify,[status(thm)],[f_19_3]) ).
cnf(f_19_6,plain,
( one_to_one(U_195,U_193,U_191)
| ~ surjective(U_195,U_193,U_191)
| ~ injective(U_195,U_193,U_191) ),
inference(clausify,[status(thm)],[f_19_3]) ).
fof(f_20_1,plain,
! [G,F,A,B] :
( ( inverse_predicate(G,F,A,B)
| ? [X,Y] :
( ( ( ~ apply(F,X,Y)
& apply(G,Y,X) )
| ( ~ apply(G,Y,X)
& apply(F,X,Y) ) )
& member(Y,B)
& member(X,A) ) )
& ( ! [X,Y] :
( ( ( apply(F,X,Y)
| ~ apply(G,Y,X) )
& ( apply(G,Y,X)
| ~ apply(F,X,Y) ) )
| ~ member(Y,B)
| ~ member(X,A) )
| ~ inverse_predicate(G,F,A,B) ) ),
inference(fof_nnf,[status(thm)],[inverse_predicate]) ).
fof(f_20_2,plain,
! [U_203,U_202,U_201,U_200] :
( ( inverse_predicate(U_203,U_202,U_201,U_200)
| ? [U_199,U_198] :
( ( ( ~ apply(U_202,U_199,U_198)
& apply(U_203,U_198,U_199) )
| ( ~ apply(U_203,U_198,U_199)
& apply(U_202,U_199,U_198) ) )
& member(U_198,U_200)
& member(U_199,U_201) ) )
& ( ! [U_197,U_196] :
( ( ( apply(U_202,U_197,U_196)
| ~ apply(U_203,U_196,U_197) )
& ( apply(U_203,U_196,U_197)
| ~ apply(U_202,U_197,U_196) ) )
| ~ member(U_196,U_200)
| ~ member(U_197,U_201) )
| ~ inverse_predicate(U_203,U_202,U_201,U_200) ) ),
inference(variable_rename,[status(thm)],[f_20_1]) ).
fof(f_20_3,plain,
( ! [U_211,U_209,U_207,U_205] :
( inverse_predicate(U_211,U_209,U_207,U_205)
| ? [U_199,U_198] :
( ( ( ~ apply(U_209,U_199,U_198)
& apply(U_211,U_198,U_199) )
| ( ~ apply(U_211,U_198,U_199)
& apply(U_209,U_199,U_198) ) )
& member(U_198,U_205)
& member(U_199,U_207) ) )
& ! [U_210,U_208,U_206,U_204] :
( ! [U_197,U_196] :
( ( ( apply(U_208,U_197,U_196)
| ~ apply(U_210,U_196,U_197) )
& ( apply(U_210,U_196,U_197)
| ~ apply(U_208,U_197,U_196) ) )
| ~ member(U_196,U_204)
| ~ member(U_197,U_206) )
| ~ inverse_predicate(U_210,U_208,U_206,U_204) ) ),
inference(miniscope,[status(thm)],[f_20_2]) ).
fof(f_20_4,plain,
( ! [U_211,U_209,U_207,U_205] :
( inverse_predicate(U_211,U_209,U_207,U_205)
| ? [U_198] :
( ( ( ~ apply(U_209,sK23(U_211,U_209,U_207,U_205),U_198)
& apply(U_211,U_198,sK23(U_211,U_209,U_207,U_205)) )
| ( ~ apply(U_211,U_198,sK23(U_211,U_209,U_207,U_205))
& apply(U_209,sK23(U_211,U_209,U_207,U_205),U_198) ) )
& member(U_198,U_205)
& member(sK23(U_211,U_209,U_207,U_205),U_207) ) )
& ! [U_210,U_208,U_206,U_204] :
( ! [U_197,U_196] :
( ( ( apply(U_208,U_197,U_196)
| ~ apply(U_210,U_196,U_197) )
& ( apply(U_210,U_196,U_197)
| ~ apply(U_208,U_197,U_196) ) )
| ~ member(U_196,U_204)
| ~ member(U_197,U_206) )
| ~ inverse_predicate(U_210,U_208,U_206,U_204) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK23]),skolemize(U_199,sK23(U_211,U_209,U_207,U_205))],[f_20_3]) ).
fof(f_20_5,plain,
( ! [U_211,U_209,U_207,U_205] :
( inverse_predicate(U_211,U_209,U_207,U_205)
| ( ( ( ~ apply(U_209,sK23(U_211,U_209,U_207,U_205),sK24(U_211,U_209,U_207,U_205))
& apply(U_211,sK24(U_211,U_209,U_207,U_205),sK23(U_211,U_209,U_207,U_205)) )
| ( ~ apply(U_211,sK24(U_211,U_209,U_207,U_205),sK23(U_211,U_209,U_207,U_205))
& apply(U_209,sK23(U_211,U_209,U_207,U_205),sK24(U_211,U_209,U_207,U_205)) ) )
& member(sK24(U_211,U_209,U_207,U_205),U_205)
& member(sK23(U_211,U_209,U_207,U_205),U_207) ) )
& ! [U_210,U_208,U_206,U_204] :
( ! [U_197,U_196] :
( ( ( apply(U_208,U_197,U_196)
| ~ apply(U_210,U_196,U_197) )
& ( apply(U_210,U_196,U_197)
| ~ apply(U_208,U_197,U_196) ) )
| ~ member(U_196,U_204)
| ~ member(U_197,U_206) )
| ~ inverse_predicate(U_210,U_208,U_206,U_204) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK24]),skolemize(U_198,sK24(U_211,U_209,U_207,U_205))],[f_20_4]) ).
cnf(f_20_6,plain,
( apply(U_210,U_196,U_197)
| ~ apply(U_208,U_197,U_196)
| ~ member(U_196,U_204)
| ~ member(U_197,U_206)
| ~ inverse_predicate(U_210,U_208,U_206,U_204) ),
inference(clausify,[status(thm)],[f_20_5]) ).
cnf(f_20_7,plain,
( apply(U_208,U_197,U_196)
| ~ apply(U_210,U_196,U_197)
| ~ member(U_196,U_204)
| ~ member(U_197,U_206)
| ~ inverse_predicate(U_210,U_208,U_206,U_204) ),
inference(clausify,[status(thm)],[f_20_5]) ).
cnf(f_20_8,plain,
( member(sK23(U_211,U_209,U_207,U_205),U_207)
| inverse_predicate(U_211,U_209,U_207,U_205) ),
inference(clausify,[status(thm)],[f_20_5]) ).
cnf(f_20_9,plain,
( member(sK24(U_211,U_209,U_207,U_205),U_205)
| inverse_predicate(U_211,U_209,U_207,U_205) ),
inference(clausify,[status(thm)],[f_20_5]) ).
cnf(f_20_10,plain,
( apply(U_211,sK24(U_211,U_209,U_207,U_205),sK23(U_211,U_209,U_207,U_205))
| apply(U_209,sK23(U_211,U_209,U_207,U_205),sK24(U_211,U_209,U_207,U_205))
| inverse_predicate(U_211,U_209,U_207,U_205) ),
inference(clausify,[status(thm)],[f_20_5]) ).
cnf(f_20_11,plain,
( ~ apply(U_209,sK23(U_211,U_209,U_207,U_205),sK24(U_211,U_209,U_207,U_205))
| apply(U_209,sK23(U_211,U_209,U_207,U_205),sK24(U_211,U_209,U_207,U_205))
| inverse_predicate(U_211,U_209,U_207,U_205) ),
inference(clausify,[status(thm)],[f_20_5]) ).
cnf(f_20_12,plain,
( apply(U_211,sK24(U_211,U_209,U_207,U_205),sK23(U_211,U_209,U_207,U_205))
| ~ apply(U_211,sK24(U_211,U_209,U_207,U_205),sK23(U_211,U_209,U_207,U_205))
| inverse_predicate(U_211,U_209,U_207,U_205) ),
inference(clausify,[status(thm)],[f_20_5]) ).
cnf(f_20_13,plain,
( ~ apply(U_209,sK23(U_211,U_209,U_207,U_205),sK24(U_211,U_209,U_207,U_205))
| ~ apply(U_211,sK24(U_211,U_209,U_207,U_205),sK23(U_211,U_209,U_207,U_205))
| inverse_predicate(U_211,U_209,U_207,U_205) ),
inference(clausify,[status(thm)],[f_20_5]) ).
fof(f_21_1,plain,
! [F,A,B,X,Y] :
( ( ( apply(F,X,Y)
| ~ apply(inverse_function(F,A,B),Y,X) )
& ( apply(inverse_function(F,A,B),Y,X)
| ~ apply(F,X,Y) ) )
| ~ member(Y,B)
| ~ member(X,A) ),
inference(fof_nnf,[status(thm)],[inverse_function]) ).
fof(f_21_2,plain,
! [U_216,U_215,U_214,U_213,U_212] :
( ( ( apply(U_216,U_213,U_212)
| ~ apply(inverse_function(U_216,U_215,U_214),U_212,U_213) )
& ( apply(inverse_function(U_216,U_215,U_214),U_212,U_213)
| ~ apply(U_216,U_213,U_212) ) )
| ~ member(U_212,U_214)
| ~ member(U_213,U_215) ),
inference(variable_rename,[status(thm)],[f_21_1]) ).
cnf(f_21_3,plain,
( apply(inverse_function(U_216,U_215,U_214),U_212,U_213)
| ~ apply(U_216,U_213,U_212)
| ~ member(U_212,U_214)
| ~ member(U_213,U_215) ),
inference(clausify,[status(thm)],[f_21_2]) ).
cnf(f_21_4,plain,
( apply(U_216,U_213,U_212)
| ~ apply(inverse_function(U_216,U_215,U_214),U_212,U_213)
| ~ member(U_212,U_214)
| ~ member(U_213,U_215) ),
inference(clausify,[status(thm)],[f_21_2]) ).
fof(f_22_1,plain,
! [F,A,Y] :
( ( member(Y,image2(F,A))
| ! [X] :
( ~ apply(F,X,Y)
| ~ member(X,A) ) )
& ( ? [X] :
( apply(F,X,Y)
& member(X,A) )
| ~ member(Y,image2(F,A)) ) ),
inference(fof_nnf,[status(thm)],[image2]) ).
fof(f_22_2,plain,
! [U_221,U_220,U_219] :
( ( member(U_219,image2(U_221,U_220))
| ! [U_218] :
( ~ apply(U_221,U_218,U_219)
| ~ member(U_218,U_220) ) )
& ( ? [U_217] :
( apply(U_221,U_217,U_219)
& member(U_217,U_220) )
| ~ member(U_219,image2(U_221,U_220)) ) ),
inference(variable_rename,[status(thm)],[f_22_1]) ).
fof(f_22_3,plain,
( ! [U_227,U_225,U_223] :
( member(U_223,image2(U_227,U_225))
| ! [U_218] :
( ~ apply(U_227,U_218,U_223)
| ~ member(U_218,U_225) ) )
& ! [U_226,U_224,U_222] :
( ? [U_217] :
( apply(U_226,U_217,U_222)
& member(U_217,U_224) )
| ~ member(U_222,image2(U_226,U_224)) ) ),
inference(miniscope,[status(thm)],[f_22_2]) ).
fof(f_22_4,plain,
( ! [U_227,U_225,U_223] :
( member(U_223,image2(U_227,U_225))
| ! [U_218] :
( ~ apply(U_227,U_218,U_223)
| ~ member(U_218,U_225) ) )
& ! [U_226,U_224,U_222] :
( ( apply(U_226,sK25(U_226,U_224,U_222),U_222)
& member(sK25(U_226,U_224,U_222),U_224) )
| ~ member(U_222,image2(U_226,U_224)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK25]),skolemize(U_217,sK25(U_226,U_224,U_222))],[f_22_3]) ).
cnf(f_22_5,plain,
( member(sK25(U_226,U_224,U_222),U_224)
| ~ member(U_222,image2(U_226,U_224)) ),
inference(clausify,[status(thm)],[f_22_4]) ).
cnf(f_22_6,plain,
( apply(U_226,sK25(U_226,U_224,U_222),U_222)
| ~ member(U_222,image2(U_226,U_224)) ),
inference(clausify,[status(thm)],[f_22_4]) ).
cnf(f_22_7,plain,
( member(U_223,image2(U_227,U_225))
| ~ apply(U_227,U_218,U_223)
| ~ member(U_218,U_225) ),
inference(clausify,[status(thm)],[f_22_4]) ).
fof(f_23_1,plain,
! [F,A,B,Y] :
( ( member(Y,image3(F,A,B))
| ! [X] :
( ~ apply(F,X,Y)
| ~ member(X,A) )
| ~ member(Y,B) )
& ( ( ? [X] :
( apply(F,X,Y)
& member(X,A) )
& member(Y,B) )
| ~ member(Y,image3(F,A,B)) ) ),
inference(fof_nnf,[status(thm)],[image3]) ).
fof(f_23_2,plain,
! [U_233,U_232,U_231,U_230] :
( ( member(U_230,image3(U_233,U_232,U_231))
| ! [U_229] :
( ~ apply(U_233,U_229,U_230)
| ~ member(U_229,U_232) )
| ~ member(U_230,U_231) )
& ( ( ? [U_228] :
( apply(U_233,U_228,U_230)
& member(U_228,U_232) )
& member(U_230,U_231) )
| ~ member(U_230,image3(U_233,U_232,U_231)) ) ),
inference(variable_rename,[status(thm)],[f_23_1]) ).
fof(f_23_3,plain,
( ! [U_241,U_239,U_237,U_235] :
( member(U_235,image3(U_241,U_239,U_237))
| ! [U_229] :
( ~ apply(U_241,U_229,U_235)
| ~ member(U_229,U_239) )
| ~ member(U_235,U_237) )
& ! [U_240,U_238,U_236,U_234] :
( ( ? [U_228] :
( apply(U_240,U_228,U_234)
& member(U_228,U_238) )
& member(U_234,U_236) )
| ~ member(U_234,image3(U_240,U_238,U_236)) ) ),
inference(miniscope,[status(thm)],[f_23_2]) ).
fof(f_23_4,plain,
( ! [U_241,U_239,U_237,U_235] :
( member(U_235,image3(U_241,U_239,U_237))
| ! [U_229] :
( ~ apply(U_241,U_229,U_235)
| ~ member(U_229,U_239) )
| ~ member(U_235,U_237) )
& ! [U_240,U_238,U_236,U_234] :
( ( apply(U_240,sK26(U_240,U_238,U_236,U_234),U_234)
& member(sK26(U_240,U_238,U_236,U_234),U_238)
& member(U_234,U_236) )
| ~ member(U_234,image3(U_240,U_238,U_236)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK26]),skolemize(U_228,sK26(U_240,U_238,U_236,U_234))],[f_23_3]) ).
cnf(f_23_5,plain,
( member(U_234,U_236)
| ~ member(U_234,image3(U_240,U_238,U_236)) ),
inference(clausify,[status(thm)],[f_23_4]) ).
cnf(f_23_6,plain,
( member(sK26(U_240,U_238,U_236,U_234),U_238)
| ~ member(U_234,image3(U_240,U_238,U_236)) ),
inference(clausify,[status(thm)],[f_23_4]) ).
cnf(f_23_7,plain,
( apply(U_240,sK26(U_240,U_238,U_236,U_234),U_234)
| ~ member(U_234,image3(U_240,U_238,U_236)) ),
inference(clausify,[status(thm)],[f_23_4]) ).
cnf(f_23_8,plain,
( member(U_235,image3(U_241,U_239,U_237))
| ~ apply(U_241,U_229,U_235)
| ~ member(U_229,U_239)
| ~ member(U_235,U_237) ),
inference(clausify,[status(thm)],[f_23_4]) ).
fof(f_24_1,plain,
! [F,B,X] :
( ( member(X,inverse_image2(F,B))
| ! [Y] :
( ~ apply(F,X,Y)
| ~ member(Y,B) ) )
& ( ? [Y] :
( apply(F,X,Y)
& member(Y,B) )
| ~ member(X,inverse_image2(F,B)) ) ),
inference(fof_nnf,[status(thm)],[inverse_image2]) ).
fof(f_24_2,plain,
! [U_246,U_245,U_244] :
( ( member(U_244,inverse_image2(U_246,U_245))
| ! [U_243] :
( ~ apply(U_246,U_244,U_243)
| ~ member(U_243,U_245) ) )
& ( ? [U_242] :
( apply(U_246,U_244,U_242)
& member(U_242,U_245) )
| ~ member(U_244,inverse_image2(U_246,U_245)) ) ),
inference(variable_rename,[status(thm)],[f_24_1]) ).
fof(f_24_3,plain,
( ! [U_252,U_250,U_248] :
( member(U_248,inverse_image2(U_252,U_250))
| ! [U_243] :
( ~ apply(U_252,U_248,U_243)
| ~ member(U_243,U_250) ) )
& ! [U_251,U_249,U_247] :
( ? [U_242] :
( apply(U_251,U_247,U_242)
& member(U_242,U_249) )
| ~ member(U_247,inverse_image2(U_251,U_249)) ) ),
inference(miniscope,[status(thm)],[f_24_2]) ).
fof(f_24_4,plain,
( ! [U_252,U_250,U_248] :
( member(U_248,inverse_image2(U_252,U_250))
| ! [U_243] :
( ~ apply(U_252,U_248,U_243)
| ~ member(U_243,U_250) ) )
& ! [U_251,U_249,U_247] :
( ( apply(U_251,U_247,sK27(U_251,U_249,U_247))
& member(sK27(U_251,U_249,U_247),U_249) )
| ~ member(U_247,inverse_image2(U_251,U_249)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK27]),skolemize(U_242,sK27(U_251,U_249,U_247))],[f_24_3]) ).
cnf(f_24_5,plain,
( member(sK27(U_251,U_249,U_247),U_249)
| ~ member(U_247,inverse_image2(U_251,U_249)) ),
inference(clausify,[status(thm)],[f_24_4]) ).
cnf(f_24_6,plain,
( apply(U_251,U_247,sK27(U_251,U_249,U_247))
| ~ member(U_247,inverse_image2(U_251,U_249)) ),
inference(clausify,[status(thm)],[f_24_4]) ).
cnf(f_24_7,plain,
( member(U_248,inverse_image2(U_252,U_250))
| ~ apply(U_252,U_248,U_243)
| ~ member(U_243,U_250) ),
inference(clausify,[status(thm)],[f_24_4]) ).
fof(f_25_1,plain,
! [F,B,A,X] :
( ( member(X,inverse_image3(F,B,A))
| ! [Y] :
( ~ apply(F,X,Y)
| ~ member(Y,B) )
| ~ member(X,A) )
& ( ( ? [Y] :
( apply(F,X,Y)
& member(Y,B) )
& member(X,A) )
| ~ member(X,inverse_image3(F,B,A)) ) ),
inference(fof_nnf,[status(thm)],[inverse_image3]) ).
fof(f_25_2,plain,
! [U_258,U_257,U_256,U_255] :
( ( member(U_255,inverse_image3(U_258,U_257,U_256))
| ! [U_254] :
( ~ apply(U_258,U_255,U_254)
| ~ member(U_254,U_257) )
| ~ member(U_255,U_256) )
& ( ( ? [U_253] :
( apply(U_258,U_255,U_253)
& member(U_253,U_257) )
& member(U_255,U_256) )
| ~ member(U_255,inverse_image3(U_258,U_257,U_256)) ) ),
inference(variable_rename,[status(thm)],[f_25_1]) ).
fof(f_25_3,plain,
( ! [U_266,U_264,U_262,U_260] :
( member(U_260,inverse_image3(U_266,U_264,U_262))
| ! [U_254] :
( ~ apply(U_266,U_260,U_254)
| ~ member(U_254,U_264) )
| ~ member(U_260,U_262) )
& ! [U_265,U_263,U_261,U_259] :
( ( ? [U_253] :
( apply(U_265,U_259,U_253)
& member(U_253,U_263) )
& member(U_259,U_261) )
| ~ member(U_259,inverse_image3(U_265,U_263,U_261)) ) ),
inference(miniscope,[status(thm)],[f_25_2]) ).
fof(f_25_4,plain,
( ! [U_266,U_264,U_262,U_260] :
( member(U_260,inverse_image3(U_266,U_264,U_262))
| ! [U_254] :
( ~ apply(U_266,U_260,U_254)
| ~ member(U_254,U_264) )
| ~ member(U_260,U_262) )
& ! [U_265,U_263,U_261,U_259] :
( ( apply(U_265,U_259,sK28(U_265,U_263,U_261,U_259))
& member(sK28(U_265,U_263,U_261,U_259),U_263)
& member(U_259,U_261) )
| ~ member(U_259,inverse_image3(U_265,U_263,U_261)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK28]),skolemize(U_253,sK28(U_265,U_263,U_261,U_259))],[f_25_3]) ).
cnf(f_25_5,plain,
( member(U_259,U_261)
| ~ member(U_259,inverse_image3(U_265,U_263,U_261)) ),
inference(clausify,[status(thm)],[f_25_4]) ).
cnf(f_25_6,plain,
( member(sK28(U_265,U_263,U_261,U_259),U_263)
| ~ member(U_259,inverse_image3(U_265,U_263,U_261)) ),
inference(clausify,[status(thm)],[f_25_4]) ).
cnf(f_25_7,plain,
( apply(U_265,U_259,sK28(U_265,U_263,U_261,U_259))
| ~ member(U_259,inverse_image3(U_265,U_263,U_261)) ),
inference(clausify,[status(thm)],[f_25_4]) ).
cnf(f_25_8,plain,
( member(U_260,inverse_image3(U_266,U_264,U_262))
| ~ apply(U_266,U_260,U_254)
| ~ member(U_254,U_264)
| ~ member(U_260,U_262) ),
inference(clausify,[status(thm)],[f_25_4]) ).
fof(f_26_1,plain,
! [F,A,R,B,S] :
( ( increasing(F,A,R,B,S)
| ? [X1,Y1,X2,Y2] :
( ~ apply(S,Y1,Y2)
& apply(F,X2,Y2)
& apply(F,X1,Y1)
& apply(R,X1,X2)
& member(Y2,B)
& member(X2,A)
& member(Y1,B)
& member(X1,A) ) )
& ( ! [X1,Y1,X2,Y2] :
( apply(S,Y1,Y2)
| ~ apply(F,X2,Y2)
| ~ apply(F,X1,Y1)
| ~ apply(R,X1,X2)
| ~ member(Y2,B)
| ~ member(X2,A)
| ~ member(Y1,B)
| ~ member(X1,A) )
| ~ increasing(F,A,R,B,S) ) ),
inference(fof_nnf,[status(thm)],[increasing_function]) ).
fof(f_26_2,plain,
! [U_279,U_278,U_277,U_276,U_275] :
( ( increasing(U_279,U_278,U_277,U_276,U_275)
| ? [U_274,U_273,U_272,U_271] :
( ~ apply(U_275,U_273,U_271)
& apply(U_279,U_272,U_271)
& apply(U_279,U_274,U_273)
& apply(U_277,U_274,U_272)
& member(U_271,U_276)
& member(U_272,U_278)
& member(U_273,U_276)
& member(U_274,U_278) ) )
& ( ! [U_270,U_269,U_268,U_267] :
( apply(U_275,U_269,U_267)
| ~ apply(U_279,U_268,U_267)
| ~ apply(U_279,U_270,U_269)
| ~ apply(U_277,U_270,U_268)
| ~ member(U_267,U_276)
| ~ member(U_268,U_278)
| ~ member(U_269,U_276)
| ~ member(U_270,U_278) )
| ~ increasing(U_279,U_278,U_277,U_276,U_275) ) ),
inference(variable_rename,[status(thm)],[f_26_1]) ).
fof(f_26_3,plain,
( ! [U_289,U_287,U_285,U_283,U_281] :
( increasing(U_289,U_287,U_285,U_283,U_281)
| ? [U_274,U_273,U_272,U_271] :
( ~ apply(U_281,U_273,U_271)
& apply(U_289,U_272,U_271)
& apply(U_289,U_274,U_273)
& apply(U_285,U_274,U_272)
& member(U_271,U_283)
& member(U_272,U_287)
& member(U_273,U_283)
& member(U_274,U_287) ) )
& ! [U_288,U_286,U_284,U_282,U_280] :
( ! [U_270,U_269,U_268,U_267] :
( apply(U_280,U_269,U_267)
| ~ apply(U_288,U_268,U_267)
| ~ apply(U_288,U_270,U_269)
| ~ apply(U_284,U_270,U_268)
| ~ member(U_267,U_282)
| ~ member(U_268,U_286)
| ~ member(U_269,U_282)
| ~ member(U_270,U_286) )
| ~ increasing(U_288,U_286,U_284,U_282,U_280) ) ),
inference(miniscope,[status(thm)],[f_26_2]) ).
fof(f_26_4,plain,
( ! [U_289,U_287,U_285,U_283,U_281] :
( increasing(U_289,U_287,U_285,U_283,U_281)
| ? [U_273,U_272,U_271] :
( ~ apply(U_281,U_273,U_271)
& apply(U_289,U_272,U_271)
& apply(U_289,sK29(U_289,U_287,U_285,U_283,U_281),U_273)
& apply(U_285,sK29(U_289,U_287,U_285,U_283,U_281),U_272)
& member(U_271,U_283)
& member(U_272,U_287)
& member(U_273,U_283)
& member(sK29(U_289,U_287,U_285,U_283,U_281),U_287) ) )
& ! [U_288,U_286,U_284,U_282,U_280] :
( ! [U_270,U_269,U_268,U_267] :
( apply(U_280,U_269,U_267)
| ~ apply(U_288,U_268,U_267)
| ~ apply(U_288,U_270,U_269)
| ~ apply(U_284,U_270,U_268)
| ~ member(U_267,U_282)
| ~ member(U_268,U_286)
| ~ member(U_269,U_282)
| ~ member(U_270,U_286) )
| ~ increasing(U_288,U_286,U_284,U_282,U_280) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK29]),skolemize(U_274,sK29(U_289,U_287,U_285,U_283,U_281))],[f_26_3]) ).
fof(f_26_5,plain,
( ! [U_289,U_287,U_285,U_283,U_281] :
( increasing(U_289,U_287,U_285,U_283,U_281)
| ? [U_272,U_271] :
( ~ apply(U_281,sK30(U_289,U_287,U_285,U_283,U_281),U_271)
& apply(U_289,U_272,U_271)
& apply(U_289,sK29(U_289,U_287,U_285,U_283,U_281),sK30(U_289,U_287,U_285,U_283,U_281))
& apply(U_285,sK29(U_289,U_287,U_285,U_283,U_281),U_272)
& member(U_271,U_283)
& member(U_272,U_287)
& member(sK30(U_289,U_287,U_285,U_283,U_281),U_283)
& member(sK29(U_289,U_287,U_285,U_283,U_281),U_287) ) )
& ! [U_288,U_286,U_284,U_282,U_280] :
( ! [U_270,U_269,U_268,U_267] :
( apply(U_280,U_269,U_267)
| ~ apply(U_288,U_268,U_267)
| ~ apply(U_288,U_270,U_269)
| ~ apply(U_284,U_270,U_268)
| ~ member(U_267,U_282)
| ~ member(U_268,U_286)
| ~ member(U_269,U_282)
| ~ member(U_270,U_286) )
| ~ increasing(U_288,U_286,U_284,U_282,U_280) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK30]),skolemize(U_273,sK30(U_289,U_287,U_285,U_283,U_281))],[f_26_4]) ).
fof(f_26_6,plain,
( ! [U_289,U_287,U_285,U_283,U_281] :
( increasing(U_289,U_287,U_285,U_283,U_281)
| ? [U_271] :
( ~ apply(U_281,sK30(U_289,U_287,U_285,U_283,U_281),U_271)
& apply(U_289,sK31(U_289,U_287,U_285,U_283,U_281),U_271)
& apply(U_289,sK29(U_289,U_287,U_285,U_283,U_281),sK30(U_289,U_287,U_285,U_283,U_281))
& apply(U_285,sK29(U_289,U_287,U_285,U_283,U_281),sK31(U_289,U_287,U_285,U_283,U_281))
& member(U_271,U_283)
& member(sK31(U_289,U_287,U_285,U_283,U_281),U_287)
& member(sK30(U_289,U_287,U_285,U_283,U_281),U_283)
& member(sK29(U_289,U_287,U_285,U_283,U_281),U_287) ) )
& ! [U_288,U_286,U_284,U_282,U_280] :
( ! [U_270,U_269,U_268,U_267] :
( apply(U_280,U_269,U_267)
| ~ apply(U_288,U_268,U_267)
| ~ apply(U_288,U_270,U_269)
| ~ apply(U_284,U_270,U_268)
| ~ member(U_267,U_282)
| ~ member(U_268,U_286)
| ~ member(U_269,U_282)
| ~ member(U_270,U_286) )
| ~ increasing(U_288,U_286,U_284,U_282,U_280) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK31]),skolemize(U_272,sK31(U_289,U_287,U_285,U_283,U_281))],[f_26_5]) ).
fof(f_26_7,plain,
( ! [U_289,U_287,U_285,U_283,U_281] :
( increasing(U_289,U_287,U_285,U_283,U_281)
| ( ~ apply(U_281,sK30(U_289,U_287,U_285,U_283,U_281),sK32(U_289,U_287,U_285,U_283,U_281))
& apply(U_289,sK31(U_289,U_287,U_285,U_283,U_281),sK32(U_289,U_287,U_285,U_283,U_281))
& apply(U_289,sK29(U_289,U_287,U_285,U_283,U_281),sK30(U_289,U_287,U_285,U_283,U_281))
& apply(U_285,sK29(U_289,U_287,U_285,U_283,U_281),sK31(U_289,U_287,U_285,U_283,U_281))
& member(sK32(U_289,U_287,U_285,U_283,U_281),U_283)
& member(sK31(U_289,U_287,U_285,U_283,U_281),U_287)
& member(sK30(U_289,U_287,U_285,U_283,U_281),U_283)
& member(sK29(U_289,U_287,U_285,U_283,U_281),U_287) ) )
& ! [U_288,U_286,U_284,U_282,U_280] :
( ! [U_270,U_269,U_268,U_267] :
( apply(U_280,U_269,U_267)
| ~ apply(U_288,U_268,U_267)
| ~ apply(U_288,U_270,U_269)
| ~ apply(U_284,U_270,U_268)
| ~ member(U_267,U_282)
| ~ member(U_268,U_286)
| ~ member(U_269,U_282)
| ~ member(U_270,U_286) )
| ~ increasing(U_288,U_286,U_284,U_282,U_280) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK32]),skolemize(U_271,sK32(U_289,U_287,U_285,U_283,U_281))],[f_26_6]) ).
cnf(f_26_8,plain,
( apply(U_280,U_269,U_267)
| ~ apply(U_288,U_268,U_267)
| ~ apply(U_288,U_270,U_269)
| ~ apply(U_284,U_270,U_268)
| ~ member(U_267,U_282)
| ~ member(U_268,U_286)
| ~ member(U_269,U_282)
| ~ member(U_270,U_286)
| ~ increasing(U_288,U_286,U_284,U_282,U_280) ),
inference(clausify,[status(thm)],[f_26_7]) ).
cnf(f_26_9,plain,
( member(sK29(U_289,U_287,U_285,U_283,U_281),U_287)
| increasing(U_289,U_287,U_285,U_283,U_281) ),
inference(clausify,[status(thm)],[f_26_7]) ).
cnf(f_26_10,plain,
( member(sK30(U_289,U_287,U_285,U_283,U_281),U_283)
| increasing(U_289,U_287,U_285,U_283,U_281) ),
inference(clausify,[status(thm)],[f_26_7]) ).
cnf(f_26_11,plain,
( member(sK31(U_289,U_287,U_285,U_283,U_281),U_287)
| increasing(U_289,U_287,U_285,U_283,U_281) ),
inference(clausify,[status(thm)],[f_26_7]) ).
cnf(f_26_12,plain,
( member(sK32(U_289,U_287,U_285,U_283,U_281),U_283)
| increasing(U_289,U_287,U_285,U_283,U_281) ),
inference(clausify,[status(thm)],[f_26_7]) ).
cnf(f_26_13,plain,
( apply(U_285,sK29(U_289,U_287,U_285,U_283,U_281),sK31(U_289,U_287,U_285,U_283,U_281))
| increasing(U_289,U_287,U_285,U_283,U_281) ),
inference(clausify,[status(thm)],[f_26_7]) ).
cnf(f_26_14,plain,
( apply(U_289,sK29(U_289,U_287,U_285,U_283,U_281),sK30(U_289,U_287,U_285,U_283,U_281))
| increasing(U_289,U_287,U_285,U_283,U_281) ),
inference(clausify,[status(thm)],[f_26_7]) ).
cnf(f_26_15,plain,
( apply(U_289,sK31(U_289,U_287,U_285,U_283,U_281),sK32(U_289,U_287,U_285,U_283,U_281))
| increasing(U_289,U_287,U_285,U_283,U_281) ),
inference(clausify,[status(thm)],[f_26_7]) ).
cnf(f_26_16,plain,
( ~ apply(U_281,sK30(U_289,U_287,U_285,U_283,U_281),sK32(U_289,U_287,U_285,U_283,U_281))
| increasing(U_289,U_287,U_285,U_283,U_281) ),
inference(clausify,[status(thm)],[f_26_7]) ).
fof(f_27_1,plain,
! [F,A,R,B,S] :
( ( decreasing(F,A,R,B,S)
| ? [X1,Y1,X2,Y2] :
( ~ apply(S,Y2,Y1)
& apply(F,X2,Y2)
& apply(F,X1,Y1)
& apply(R,X1,X2)
& member(Y2,B)
& member(X2,A)
& member(Y1,B)
& member(X1,A) ) )
& ( ! [X1,Y1,X2,Y2] :
( apply(S,Y2,Y1)
| ~ apply(F,X2,Y2)
| ~ apply(F,X1,Y1)
| ~ apply(R,X1,X2)
| ~ member(Y2,B)
| ~ member(X2,A)
| ~ member(Y1,B)
| ~ member(X1,A) )
| ~ decreasing(F,A,R,B,S) ) ),
inference(fof_nnf,[status(thm)],[decreasing_function]) ).
fof(f_27_2,plain,
! [U_302,U_301,U_300,U_299,U_298] :
( ( decreasing(U_302,U_301,U_300,U_299,U_298)
| ? [U_297,U_296,U_295,U_294] :
( ~ apply(U_298,U_294,U_296)
& apply(U_302,U_295,U_294)
& apply(U_302,U_297,U_296)
& apply(U_300,U_297,U_295)
& member(U_294,U_299)
& member(U_295,U_301)
& member(U_296,U_299)
& member(U_297,U_301) ) )
& ( ! [U_293,U_292,U_291,U_290] :
( apply(U_298,U_290,U_292)
| ~ apply(U_302,U_291,U_290)
| ~ apply(U_302,U_293,U_292)
| ~ apply(U_300,U_293,U_291)
| ~ member(U_290,U_299)
| ~ member(U_291,U_301)
| ~ member(U_292,U_299)
| ~ member(U_293,U_301) )
| ~ decreasing(U_302,U_301,U_300,U_299,U_298) ) ),
inference(variable_rename,[status(thm)],[f_27_1]) ).
fof(f_27_3,plain,
( ! [U_312,U_310,U_308,U_306,U_304] :
( decreasing(U_312,U_310,U_308,U_306,U_304)
| ? [U_297,U_296,U_295,U_294] :
( ~ apply(U_304,U_294,U_296)
& apply(U_312,U_295,U_294)
& apply(U_312,U_297,U_296)
& apply(U_308,U_297,U_295)
& member(U_294,U_306)
& member(U_295,U_310)
& member(U_296,U_306)
& member(U_297,U_310) ) )
& ! [U_311,U_309,U_307,U_305,U_303] :
( ! [U_293,U_292,U_291,U_290] :
( apply(U_303,U_290,U_292)
| ~ apply(U_311,U_291,U_290)
| ~ apply(U_311,U_293,U_292)
| ~ apply(U_307,U_293,U_291)
| ~ member(U_290,U_305)
| ~ member(U_291,U_309)
| ~ member(U_292,U_305)
| ~ member(U_293,U_309) )
| ~ decreasing(U_311,U_309,U_307,U_305,U_303) ) ),
inference(miniscope,[status(thm)],[f_27_2]) ).
fof(f_27_4,plain,
( ! [U_312,U_310,U_308,U_306,U_304] :
( decreasing(U_312,U_310,U_308,U_306,U_304)
| ? [U_296,U_295,U_294] :
( ~ apply(U_304,U_294,U_296)
& apply(U_312,U_295,U_294)
& apply(U_312,sK33(U_312,U_310,U_308,U_306,U_304),U_296)
& apply(U_308,sK33(U_312,U_310,U_308,U_306,U_304),U_295)
& member(U_294,U_306)
& member(U_295,U_310)
& member(U_296,U_306)
& member(sK33(U_312,U_310,U_308,U_306,U_304),U_310) ) )
& ! [U_311,U_309,U_307,U_305,U_303] :
( ! [U_293,U_292,U_291,U_290] :
( apply(U_303,U_290,U_292)
| ~ apply(U_311,U_291,U_290)
| ~ apply(U_311,U_293,U_292)
| ~ apply(U_307,U_293,U_291)
| ~ member(U_290,U_305)
| ~ member(U_291,U_309)
| ~ member(U_292,U_305)
| ~ member(U_293,U_309) )
| ~ decreasing(U_311,U_309,U_307,U_305,U_303) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK33]),skolemize(U_297,sK33(U_312,U_310,U_308,U_306,U_304))],[f_27_3]) ).
fof(f_27_5,plain,
( ! [U_312,U_310,U_308,U_306,U_304] :
( decreasing(U_312,U_310,U_308,U_306,U_304)
| ? [U_295,U_294] :
( ~ apply(U_304,U_294,sK34(U_312,U_310,U_308,U_306,U_304))
& apply(U_312,U_295,U_294)
& apply(U_312,sK33(U_312,U_310,U_308,U_306,U_304),sK34(U_312,U_310,U_308,U_306,U_304))
& apply(U_308,sK33(U_312,U_310,U_308,U_306,U_304),U_295)
& member(U_294,U_306)
& member(U_295,U_310)
& member(sK34(U_312,U_310,U_308,U_306,U_304),U_306)
& member(sK33(U_312,U_310,U_308,U_306,U_304),U_310) ) )
& ! [U_311,U_309,U_307,U_305,U_303] :
( ! [U_293,U_292,U_291,U_290] :
( apply(U_303,U_290,U_292)
| ~ apply(U_311,U_291,U_290)
| ~ apply(U_311,U_293,U_292)
| ~ apply(U_307,U_293,U_291)
| ~ member(U_290,U_305)
| ~ member(U_291,U_309)
| ~ member(U_292,U_305)
| ~ member(U_293,U_309) )
| ~ decreasing(U_311,U_309,U_307,U_305,U_303) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK34]),skolemize(U_296,sK34(U_312,U_310,U_308,U_306,U_304))],[f_27_4]) ).
fof(f_27_6,plain,
( ! [U_312,U_310,U_308,U_306,U_304] :
( decreasing(U_312,U_310,U_308,U_306,U_304)
| ? [U_294] :
( ~ apply(U_304,U_294,sK34(U_312,U_310,U_308,U_306,U_304))
& apply(U_312,sK35(U_312,U_310,U_308,U_306,U_304),U_294)
& apply(U_312,sK33(U_312,U_310,U_308,U_306,U_304),sK34(U_312,U_310,U_308,U_306,U_304))
& apply(U_308,sK33(U_312,U_310,U_308,U_306,U_304),sK35(U_312,U_310,U_308,U_306,U_304))
& member(U_294,U_306)
& member(sK35(U_312,U_310,U_308,U_306,U_304),U_310)
& member(sK34(U_312,U_310,U_308,U_306,U_304),U_306)
& member(sK33(U_312,U_310,U_308,U_306,U_304),U_310) ) )
& ! [U_311,U_309,U_307,U_305,U_303] :
( ! [U_293,U_292,U_291,U_290] :
( apply(U_303,U_290,U_292)
| ~ apply(U_311,U_291,U_290)
| ~ apply(U_311,U_293,U_292)
| ~ apply(U_307,U_293,U_291)
| ~ member(U_290,U_305)
| ~ member(U_291,U_309)
| ~ member(U_292,U_305)
| ~ member(U_293,U_309) )
| ~ decreasing(U_311,U_309,U_307,U_305,U_303) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK35]),skolemize(U_295,sK35(U_312,U_310,U_308,U_306,U_304))],[f_27_5]) ).
fof(f_27_7,plain,
( ! [U_312,U_310,U_308,U_306,U_304] :
( decreasing(U_312,U_310,U_308,U_306,U_304)
| ( ~ apply(U_304,sK36(U_312,U_310,U_308,U_306,U_304),sK34(U_312,U_310,U_308,U_306,U_304))
& apply(U_312,sK35(U_312,U_310,U_308,U_306,U_304),sK36(U_312,U_310,U_308,U_306,U_304))
& apply(U_312,sK33(U_312,U_310,U_308,U_306,U_304),sK34(U_312,U_310,U_308,U_306,U_304))
& apply(U_308,sK33(U_312,U_310,U_308,U_306,U_304),sK35(U_312,U_310,U_308,U_306,U_304))
& member(sK36(U_312,U_310,U_308,U_306,U_304),U_306)
& member(sK35(U_312,U_310,U_308,U_306,U_304),U_310)
& member(sK34(U_312,U_310,U_308,U_306,U_304),U_306)
& member(sK33(U_312,U_310,U_308,U_306,U_304),U_310) ) )
& ! [U_311,U_309,U_307,U_305,U_303] :
( ! [U_293,U_292,U_291,U_290] :
( apply(U_303,U_290,U_292)
| ~ apply(U_311,U_291,U_290)
| ~ apply(U_311,U_293,U_292)
| ~ apply(U_307,U_293,U_291)
| ~ member(U_290,U_305)
| ~ member(U_291,U_309)
| ~ member(U_292,U_305)
| ~ member(U_293,U_309) )
| ~ decreasing(U_311,U_309,U_307,U_305,U_303) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK36]),skolemize(U_294,sK36(U_312,U_310,U_308,U_306,U_304))],[f_27_6]) ).
cnf(f_27_8,plain,
( apply(U_303,U_290,U_292)
| ~ apply(U_311,U_291,U_290)
| ~ apply(U_311,U_293,U_292)
| ~ apply(U_307,U_293,U_291)
| ~ member(U_290,U_305)
| ~ member(U_291,U_309)
| ~ member(U_292,U_305)
| ~ member(U_293,U_309)
| ~ decreasing(U_311,U_309,U_307,U_305,U_303) ),
inference(clausify,[status(thm)],[f_27_7]) ).
cnf(f_27_9,plain,
( member(sK33(U_312,U_310,U_308,U_306,U_304),U_310)
| decreasing(U_312,U_310,U_308,U_306,U_304) ),
inference(clausify,[status(thm)],[f_27_7]) ).
cnf(f_27_10,plain,
( member(sK34(U_312,U_310,U_308,U_306,U_304),U_306)
| decreasing(U_312,U_310,U_308,U_306,U_304) ),
inference(clausify,[status(thm)],[f_27_7]) ).
cnf(f_27_11,plain,
( member(sK35(U_312,U_310,U_308,U_306,U_304),U_310)
| decreasing(U_312,U_310,U_308,U_306,U_304) ),
inference(clausify,[status(thm)],[f_27_7]) ).
cnf(f_27_12,plain,
( member(sK36(U_312,U_310,U_308,U_306,U_304),U_306)
| decreasing(U_312,U_310,U_308,U_306,U_304) ),
inference(clausify,[status(thm)],[f_27_7]) ).
cnf(f_27_13,plain,
( apply(U_308,sK33(U_312,U_310,U_308,U_306,U_304),sK35(U_312,U_310,U_308,U_306,U_304))
| decreasing(U_312,U_310,U_308,U_306,U_304) ),
inference(clausify,[status(thm)],[f_27_7]) ).
cnf(f_27_14,plain,
( apply(U_312,sK33(U_312,U_310,U_308,U_306,U_304),sK34(U_312,U_310,U_308,U_306,U_304))
| decreasing(U_312,U_310,U_308,U_306,U_304) ),
inference(clausify,[status(thm)],[f_27_7]) ).
cnf(f_27_15,plain,
( apply(U_312,sK35(U_312,U_310,U_308,U_306,U_304),sK36(U_312,U_310,U_308,U_306,U_304))
| decreasing(U_312,U_310,U_308,U_306,U_304) ),
inference(clausify,[status(thm)],[f_27_7]) ).
cnf(f_27_16,plain,
( ~ apply(U_304,sK36(U_312,U_310,U_308,U_306,U_304),sK34(U_312,U_310,U_308,U_306,U_304))
| decreasing(U_312,U_310,U_308,U_306,U_304) ),
inference(clausify,[status(thm)],[f_27_7]) ).
fof(f_28_1,plain,
! [F,A,R,B,S] :
( ( isomorphism(F,A,R,B,S)
| ? [X1,Y1,X2,Y2] :
( ( ( ~ apply(R,X1,X2)
& apply(S,Y1,Y2) )
| ( ~ apply(S,Y1,Y2)
& apply(R,X1,X2) ) )
& apply(F,X2,Y2)
& apply(F,X1,Y1)
& member(Y2,B)
& member(X2,A)
& member(Y1,B)
& member(X1,A) )
| ~ one_to_one(F,A,B)
| ~ maps(F,A,B) )
& ( ( ! [X1,Y1,X2,Y2] :
( ( ( apply(R,X1,X2)
| ~ apply(S,Y1,Y2) )
& ( apply(S,Y1,Y2)
| ~ apply(R,X1,X2) ) )
| ~ apply(F,X2,Y2)
| ~ apply(F,X1,Y1)
| ~ member(Y2,B)
| ~ member(X2,A)
| ~ member(Y1,B)
| ~ member(X1,A) )
& one_to_one(F,A,B)
& maps(F,A,B) )
| ~ isomorphism(F,A,R,B,S) ) ),
inference(fof_nnf,[status(thm)],[isomorphism]) ).
fof(f_28_2,plain,
! [U_325,U_324,U_323,U_322,U_321] :
( ( isomorphism(U_325,U_324,U_323,U_322,U_321)
| ? [U_320,U_319,U_318,U_317] :
( ( ( ~ apply(U_323,U_320,U_318)
& apply(U_321,U_319,U_317) )
| ( ~ apply(U_321,U_319,U_317)
& apply(U_323,U_320,U_318) ) )
& apply(U_325,U_318,U_317)
& apply(U_325,U_320,U_319)
& member(U_317,U_322)
& member(U_318,U_324)
& member(U_319,U_322)
& member(U_320,U_324) )
| ~ one_to_one(U_325,U_324,U_322)
| ~ maps(U_325,U_324,U_322) )
& ( ( ! [U_316,U_315,U_314,U_313] :
( ( ( apply(U_323,U_316,U_314)
| ~ apply(U_321,U_315,U_313) )
& ( apply(U_321,U_315,U_313)
| ~ apply(U_323,U_316,U_314) ) )
| ~ apply(U_325,U_314,U_313)
| ~ apply(U_325,U_316,U_315)
| ~ member(U_313,U_322)
| ~ member(U_314,U_324)
| ~ member(U_315,U_322)
| ~ member(U_316,U_324) )
& one_to_one(U_325,U_324,U_322)
& maps(U_325,U_324,U_322) )
| ~ isomorphism(U_325,U_324,U_323,U_322,U_321) ) ),
inference(variable_rename,[status(thm)],[f_28_1]) ).
fof(f_28_3,plain,
( ! [U_335,U_333,U_331,U_329,U_327] :
( isomorphism(U_335,U_333,U_331,U_329,U_327)
| ? [U_320,U_319,U_318,U_317] :
( ( ( ~ apply(U_331,U_320,U_318)
& apply(U_327,U_319,U_317) )
| ( ~ apply(U_327,U_319,U_317)
& apply(U_331,U_320,U_318) ) )
& apply(U_335,U_318,U_317)
& apply(U_335,U_320,U_319)
& member(U_317,U_329)
& member(U_318,U_333)
& member(U_319,U_329)
& member(U_320,U_333) )
| ~ one_to_one(U_335,U_333,U_329)
| ~ maps(U_335,U_333,U_329) )
& ! [U_334,U_332,U_330,U_328,U_326] :
( ( ! [U_316,U_315,U_314,U_313] :
( ( ( apply(U_330,U_316,U_314)
| ~ apply(U_326,U_315,U_313) )
& ( apply(U_326,U_315,U_313)
| ~ apply(U_330,U_316,U_314) ) )
| ~ apply(U_334,U_314,U_313)
| ~ apply(U_334,U_316,U_315)
| ~ member(U_313,U_328)
| ~ member(U_314,U_332)
| ~ member(U_315,U_328)
| ~ member(U_316,U_332) )
& one_to_one(U_334,U_332,U_328)
& maps(U_334,U_332,U_328) )
| ~ isomorphism(U_334,U_332,U_330,U_328,U_326) ) ),
inference(miniscope,[status(thm)],[f_28_2]) ).
fof(f_28_4,plain,
( ! [U_335,U_333,U_331,U_329,U_327] :
( isomorphism(U_335,U_333,U_331,U_329,U_327)
| ? [U_319,U_318,U_317] :
( ( ( ~ apply(U_331,sK37(U_335,U_333,U_331,U_329,U_327),U_318)
& apply(U_327,U_319,U_317) )
| ( ~ apply(U_327,U_319,U_317)
& apply(U_331,sK37(U_335,U_333,U_331,U_329,U_327),U_318) ) )
& apply(U_335,U_318,U_317)
& apply(U_335,sK37(U_335,U_333,U_331,U_329,U_327),U_319)
& member(U_317,U_329)
& member(U_318,U_333)
& member(U_319,U_329)
& member(sK37(U_335,U_333,U_331,U_329,U_327),U_333) )
| ~ one_to_one(U_335,U_333,U_329)
| ~ maps(U_335,U_333,U_329) )
& ! [U_334,U_332,U_330,U_328,U_326] :
( ( ! [U_316,U_315,U_314,U_313] :
( ( ( apply(U_330,U_316,U_314)
| ~ apply(U_326,U_315,U_313) )
& ( apply(U_326,U_315,U_313)
| ~ apply(U_330,U_316,U_314) ) )
| ~ apply(U_334,U_314,U_313)
| ~ apply(U_334,U_316,U_315)
| ~ member(U_313,U_328)
| ~ member(U_314,U_332)
| ~ member(U_315,U_328)
| ~ member(U_316,U_332) )
& one_to_one(U_334,U_332,U_328)
& maps(U_334,U_332,U_328) )
| ~ isomorphism(U_334,U_332,U_330,U_328,U_326) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK37]),skolemize(U_320,sK37(U_335,U_333,U_331,U_329,U_327))],[f_28_3]) ).
fof(f_28_5,plain,
( ! [U_335,U_333,U_331,U_329,U_327] :
( isomorphism(U_335,U_333,U_331,U_329,U_327)
| ? [U_318,U_317] :
( ( ( ~ apply(U_331,sK37(U_335,U_333,U_331,U_329,U_327),U_318)
& apply(U_327,sK38(U_335,U_333,U_331,U_329,U_327),U_317) )
| ( ~ apply(U_327,sK38(U_335,U_333,U_331,U_329,U_327),U_317)
& apply(U_331,sK37(U_335,U_333,U_331,U_329,U_327),U_318) ) )
& apply(U_335,U_318,U_317)
& apply(U_335,sK37(U_335,U_333,U_331,U_329,U_327),sK38(U_335,U_333,U_331,U_329,U_327))
& member(U_317,U_329)
& member(U_318,U_333)
& member(sK38(U_335,U_333,U_331,U_329,U_327),U_329)
& member(sK37(U_335,U_333,U_331,U_329,U_327),U_333) )
| ~ one_to_one(U_335,U_333,U_329)
| ~ maps(U_335,U_333,U_329) )
& ! [U_334,U_332,U_330,U_328,U_326] :
( ( ! [U_316,U_315,U_314,U_313] :
( ( ( apply(U_330,U_316,U_314)
| ~ apply(U_326,U_315,U_313) )
& ( apply(U_326,U_315,U_313)
| ~ apply(U_330,U_316,U_314) ) )
| ~ apply(U_334,U_314,U_313)
| ~ apply(U_334,U_316,U_315)
| ~ member(U_313,U_328)
| ~ member(U_314,U_332)
| ~ member(U_315,U_328)
| ~ member(U_316,U_332) )
& one_to_one(U_334,U_332,U_328)
& maps(U_334,U_332,U_328) )
| ~ isomorphism(U_334,U_332,U_330,U_328,U_326) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK38]),skolemize(U_319,sK38(U_335,U_333,U_331,U_329,U_327))],[f_28_4]) ).
fof(f_28_6,plain,
( ! [U_335,U_333,U_331,U_329,U_327] :
( isomorphism(U_335,U_333,U_331,U_329,U_327)
| ? [U_317] :
( ( ( ~ apply(U_331,sK37(U_335,U_333,U_331,U_329,U_327),sK39(U_335,U_333,U_331,U_329,U_327))
& apply(U_327,sK38(U_335,U_333,U_331,U_329,U_327),U_317) )
| ( ~ apply(U_327,sK38(U_335,U_333,U_331,U_329,U_327),U_317)
& apply(U_331,sK37(U_335,U_333,U_331,U_329,U_327),sK39(U_335,U_333,U_331,U_329,U_327)) ) )
& apply(U_335,sK39(U_335,U_333,U_331,U_329,U_327),U_317)
& apply(U_335,sK37(U_335,U_333,U_331,U_329,U_327),sK38(U_335,U_333,U_331,U_329,U_327))
& member(U_317,U_329)
& member(sK39(U_335,U_333,U_331,U_329,U_327),U_333)
& member(sK38(U_335,U_333,U_331,U_329,U_327),U_329)
& member(sK37(U_335,U_333,U_331,U_329,U_327),U_333) )
| ~ one_to_one(U_335,U_333,U_329)
| ~ maps(U_335,U_333,U_329) )
& ! [U_334,U_332,U_330,U_328,U_326] :
( ( ! [U_316,U_315,U_314,U_313] :
( ( ( apply(U_330,U_316,U_314)
| ~ apply(U_326,U_315,U_313) )
& ( apply(U_326,U_315,U_313)
| ~ apply(U_330,U_316,U_314) ) )
| ~ apply(U_334,U_314,U_313)
| ~ apply(U_334,U_316,U_315)
| ~ member(U_313,U_328)
| ~ member(U_314,U_332)
| ~ member(U_315,U_328)
| ~ member(U_316,U_332) )
& one_to_one(U_334,U_332,U_328)
& maps(U_334,U_332,U_328) )
| ~ isomorphism(U_334,U_332,U_330,U_328,U_326) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK39]),skolemize(U_318,sK39(U_335,U_333,U_331,U_329,U_327))],[f_28_5]) ).
fof(f_28_7,plain,
( ! [U_335,U_333,U_331,U_329,U_327] :
( isomorphism(U_335,U_333,U_331,U_329,U_327)
| ( ( ( ~ apply(U_331,sK37(U_335,U_333,U_331,U_329,U_327),sK39(U_335,U_333,U_331,U_329,U_327))
& apply(U_327,sK38(U_335,U_333,U_331,U_329,U_327),sK40(U_335,U_333,U_331,U_329,U_327)) )
| ( ~ apply(U_327,sK38(U_335,U_333,U_331,U_329,U_327),sK40(U_335,U_333,U_331,U_329,U_327))
& apply(U_331,sK37(U_335,U_333,U_331,U_329,U_327),sK39(U_335,U_333,U_331,U_329,U_327)) ) )
& apply(U_335,sK39(U_335,U_333,U_331,U_329,U_327),sK40(U_335,U_333,U_331,U_329,U_327))
& apply(U_335,sK37(U_335,U_333,U_331,U_329,U_327),sK38(U_335,U_333,U_331,U_329,U_327))
& member(sK40(U_335,U_333,U_331,U_329,U_327),U_329)
& member(sK39(U_335,U_333,U_331,U_329,U_327),U_333)
& member(sK38(U_335,U_333,U_331,U_329,U_327),U_329)
& member(sK37(U_335,U_333,U_331,U_329,U_327),U_333) )
| ~ one_to_one(U_335,U_333,U_329)
| ~ maps(U_335,U_333,U_329) )
& ! [U_334,U_332,U_330,U_328,U_326] :
( ( ! [U_316,U_315,U_314,U_313] :
( ( ( apply(U_330,U_316,U_314)
| ~ apply(U_326,U_315,U_313) )
& ( apply(U_326,U_315,U_313)
| ~ apply(U_330,U_316,U_314) ) )
| ~ apply(U_334,U_314,U_313)
| ~ apply(U_334,U_316,U_315)
| ~ member(U_313,U_328)
| ~ member(U_314,U_332)
| ~ member(U_315,U_328)
| ~ member(U_316,U_332) )
& one_to_one(U_334,U_332,U_328)
& maps(U_334,U_332,U_328) )
| ~ isomorphism(U_334,U_332,U_330,U_328,U_326) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK40]),skolemize(U_317,sK40(U_335,U_333,U_331,U_329,U_327))],[f_28_6]) ).
cnf(f_28_8,plain,
( maps(U_334,U_332,U_328)
| ~ isomorphism(U_334,U_332,U_330,U_328,U_326) ),
inference(clausify,[status(thm)],[f_28_7]) ).
cnf(f_28_9,plain,
( one_to_one(U_334,U_332,U_328)
| ~ isomorphism(U_334,U_332,U_330,U_328,U_326) ),
inference(clausify,[status(thm)],[f_28_7]) ).
cnf(f_28_10,plain,
( apply(U_326,U_315,U_313)
| ~ apply(U_330,U_316,U_314)
| ~ apply(U_334,U_314,U_313)
| ~ apply(U_334,U_316,U_315)
| ~ member(U_313,U_328)
| ~ member(U_314,U_332)
| ~ member(U_315,U_328)
| ~ member(U_316,U_332)
| ~ isomorphism(U_334,U_332,U_330,U_328,U_326) ),
inference(clausify,[status(thm)],[f_28_7]) ).
cnf(f_28_11,plain,
( apply(U_330,U_316,U_314)
| ~ apply(U_326,U_315,U_313)
| ~ apply(U_334,U_314,U_313)
| ~ apply(U_334,U_316,U_315)
| ~ member(U_313,U_328)
| ~ member(U_314,U_332)
| ~ member(U_315,U_328)
| ~ member(U_316,U_332)
| ~ isomorphism(U_334,U_332,U_330,U_328,U_326) ),
inference(clausify,[status(thm)],[f_28_7]) ).
cnf(f_28_12,plain,
( member(sK37(U_335,U_333,U_331,U_329,U_327),U_333)
| ~ one_to_one(U_335,U_333,U_329)
| ~ maps(U_335,U_333,U_329)
| isomorphism(U_335,U_333,U_331,U_329,U_327) ),
inference(clausify,[status(thm)],[f_28_7]) ).
cnf(f_28_13,plain,
( member(sK38(U_335,U_333,U_331,U_329,U_327),U_329)
| ~ one_to_one(U_335,U_333,U_329)
| ~ maps(U_335,U_333,U_329)
| isomorphism(U_335,U_333,U_331,U_329,U_327) ),
inference(clausify,[status(thm)],[f_28_7]) ).
cnf(f_28_14,plain,
( member(sK39(U_335,U_333,U_331,U_329,U_327),U_333)
| ~ one_to_one(U_335,U_333,U_329)
| ~ maps(U_335,U_333,U_329)
| isomorphism(U_335,U_333,U_331,U_329,U_327) ),
inference(clausify,[status(thm)],[f_28_7]) ).
cnf(f_28_15,plain,
( member(sK40(U_335,U_333,U_331,U_329,U_327),U_329)
| ~ one_to_one(U_335,U_333,U_329)
| ~ maps(U_335,U_333,U_329)
| isomorphism(U_335,U_333,U_331,U_329,U_327) ),
inference(clausify,[status(thm)],[f_28_7]) ).
cnf(f_28_16,plain,
( apply(U_335,sK37(U_335,U_333,U_331,U_329,U_327),sK38(U_335,U_333,U_331,U_329,U_327))
| ~ one_to_one(U_335,U_333,U_329)
| ~ maps(U_335,U_333,U_329)
| isomorphism(U_335,U_333,U_331,U_329,U_327) ),
inference(clausify,[status(thm)],[f_28_7]) ).
cnf(f_28_17,plain,
( apply(U_335,sK39(U_335,U_333,U_331,U_329,U_327),sK40(U_335,U_333,U_331,U_329,U_327))
| ~ one_to_one(U_335,U_333,U_329)
| ~ maps(U_335,U_333,U_329)
| isomorphism(U_335,U_333,U_331,U_329,U_327) ),
inference(clausify,[status(thm)],[f_28_7]) ).
cnf(f_28_18,plain,
( apply(U_327,sK38(U_335,U_333,U_331,U_329,U_327),sK40(U_335,U_333,U_331,U_329,U_327))
| apply(U_331,sK37(U_335,U_333,U_331,U_329,U_327),sK39(U_335,U_333,U_331,U_329,U_327))
| ~ one_to_one(U_335,U_333,U_329)
| ~ maps(U_335,U_333,U_329)
| isomorphism(U_335,U_333,U_331,U_329,U_327) ),
inference(clausify,[status(thm)],[f_28_7]) ).
cnf(f_28_19,plain,
( ~ apply(U_331,sK37(U_335,U_333,U_331,U_329,U_327),sK39(U_335,U_333,U_331,U_329,U_327))
| apply(U_331,sK37(U_335,U_333,U_331,U_329,U_327),sK39(U_335,U_333,U_331,U_329,U_327))
| ~ one_to_one(U_335,U_333,U_329)
| ~ maps(U_335,U_333,U_329)
| isomorphism(U_335,U_333,U_331,U_329,U_327) ),
inference(clausify,[status(thm)],[f_28_7]) ).
cnf(f_28_20,plain,
( apply(U_327,sK38(U_335,U_333,U_331,U_329,U_327),sK40(U_335,U_333,U_331,U_329,U_327))
| ~ apply(U_327,sK38(U_335,U_333,U_331,U_329,U_327),sK40(U_335,U_333,U_331,U_329,U_327))
| ~ one_to_one(U_335,U_333,U_329)
| ~ maps(U_335,U_333,U_329)
| isomorphism(U_335,U_333,U_331,U_329,U_327) ),
inference(clausify,[status(thm)],[f_28_7]) ).
cnf(f_28_21,plain,
( ~ apply(U_331,sK37(U_335,U_333,U_331,U_329,U_327),sK39(U_335,U_333,U_331,U_329,U_327))
| ~ apply(U_327,sK38(U_335,U_333,U_331,U_329,U_327),sK40(U_335,U_333,U_331,U_329,U_327))
| ~ one_to_one(U_335,U_333,U_329)
| ~ maps(U_335,U_333,U_329)
| isomorphism(U_335,U_333,U_331,U_329,U_327) ),
inference(clausify,[status(thm)],[f_28_7]) ).
fof(f_29_1,negated_conjecture,
~ ! [F,A,B] :
( ( one_to_one(F,A,B)
& maps(F,A,B) )
=> equal_maps(inverse_function(inverse_function(F,A,B),B,A),F,A,B) ),
inference(negate,[status(cth)],[thII11]) ).
fof(f_29_2,negated_conjecture,
? [F,A,B] :
( ~ equal_maps(inverse_function(inverse_function(F,A,B),B,A),F,A,B)
& one_to_one(F,A,B)
& maps(F,A,B) ),
inference(fof_nnf,[status(thm)],[f_29_1]) ).
fof(f_29_3,negated_conjecture,
? [U_338,U_337,U_336] :
( ~ equal_maps(inverse_function(inverse_function(U_338,U_337,U_336),U_336,U_337),U_338,U_337,U_336)
& one_to_one(U_338,U_337,U_336)
& maps(U_338,U_337,U_336) ),
inference(variable_rename,[status(thm)],[f_29_2]) ).
fof(f_29_4,negated_conjecture,
? [U_337,U_336] :
( ~ equal_maps(inverse_function(inverse_function(sK41,U_337,U_336),U_336,U_337),sK41,U_337,U_336)
& one_to_one(sK41,U_337,U_336)
& maps(sK41,U_337,U_336) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK41]),skolemize(U_338,sK41)],[f_29_3]) ).
fof(f_29_5,negated_conjecture,
? [U_336] :
( ~ equal_maps(inverse_function(inverse_function(sK41,sK42,U_336),U_336,sK42),sK41,sK42,U_336)
& one_to_one(sK41,sK42,U_336)
& maps(sK41,sK42,U_336) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK42]),skolemize(U_337,sK42)],[f_29_4]) ).
fof(f_29_6,negated_conjecture,
( ~ equal_maps(inverse_function(inverse_function(sK41,sK42,sK43),sK43,sK42),sK41,sK42,sK43)
& one_to_one(sK41,sK42,sK43)
& maps(sK41,sK42,sK43) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK43]),skolemize(U_336,sK43)],[f_29_5]) ).
cnf(f_29_7,negated_conjecture,
maps(sK41,sK42,sK43),
inference(clausify,[status(thm)],[f_29_6]) ).
cnf(f_29_8,negated_conjecture,
one_to_one(sK41,sK42,sK43),
inference(clausify,[status(thm)],[f_29_6]) ).
cnf(f_29_9,negated_conjecture,
~ equal_maps(inverse_function(inverse_function(sK41,sK42,sK43),sK43,sK42),sK41,sK42,sK43),
inference(clausify,[status(thm)],[f_29_6]) ).
cnf(f_13_17_true,plain,
$true,
inference(clause_is_true,[status(thm)],[f_13_17]) ).
cnf(f_20_11_true,plain,
$true,
inference(clause_is_true,[status(thm)],[f_20_11]) ).
cnf(f_20_12_true,plain,
$true,
inference(clause_is_true,[status(thm)],[f_20_12]) ).
cnf(f_28_19_true,plain,
$true,
inference(clause_is_true,[status(thm)],[f_28_19]) ).
cnf(f_28_20_true,plain,
$true,
inference(clause_is_true,[status(thm)],[f_28_20]) ).
cnf(equality_1,axiom,
Eq_x_0 = Eq_x_0,
theory(equality,[reflexivity]) ).
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_4,axiom,
( power_set(Eq_x_0) = power_set(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_5,axiom,
( intersection(Eq_x_0,Eq_x_1) = intersection(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_6,axiom,
( union(Eq_x_0,Eq_x_1) = union(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,
( difference(Eq_x_0,Eq_x_1) = difference(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_8,axiom,
( singleton(Eq_x_0) = singleton(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_9,axiom,
( unordered_pair(Eq_x_0,Eq_x_1) = unordered_pair(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_10,axiom,
( sum(Eq_x_0) = sum(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_11,axiom,
( product(Eq_x_0) = product(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_12,axiom,
( compose_function(Eq_x_0,Eq_x_1,Eq_x_2,Eq_x_3,Eq_x_4) = compose_function(Eq_y_0,Eq_y_1,Eq_y_2,Eq_y_3,Eq_y_4)
| Eq_x_4 != Eq_y_4
| Eq_x_3 != Eq_y_3
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_13,axiom,
( inverse_function(Eq_x_0,Eq_x_1,Eq_x_2) = inverse_function(Eq_y_0,Eq_y_1,Eq_y_2)
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_14,axiom,
( image2(Eq_x_0,Eq_x_1) = image2(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_15,axiom,
( image3(Eq_x_0,Eq_x_1,Eq_x_2) = image3(Eq_y_0,Eq_y_1,Eq_y_2)
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_16,axiom,
( inverse_image2(Eq_x_0,Eq_x_1) = inverse_image2(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_17,axiom,
( inverse_image3(Eq_x_0,Eq_x_1,Eq_x_2) = inverse_image3(Eq_y_0,Eq_y_1,Eq_y_2)
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_18,axiom,
( sK1(Eq_x_0,Eq_x_1) = sK1(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_19,axiom,
( sK2(Eq_x_0,Eq_x_1) = sK2(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_20,axiom,
( sK3(Eq_x_0,Eq_x_1) = sK3(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_21,axiom,
( sK4(Eq_x_0,Eq_x_1,Eq_x_2,Eq_x_3) = sK4(Eq_y_0,Eq_y_1,Eq_y_2,Eq_y_3)
| Eq_x_3 != Eq_y_3
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_22,axiom,
( sK5(Eq_x_0,Eq_x_1,Eq_x_2) = sK5(Eq_y_0,Eq_y_1,Eq_y_2)
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_23,axiom,
( sK6(Eq_x_0,Eq_x_1,Eq_x_2) = sK6(Eq_y_0,Eq_y_1,Eq_y_2)
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_24,axiom,
( sK7(Eq_x_0,Eq_x_1,Eq_x_2) = sK7(Eq_y_0,Eq_y_1,Eq_y_2)
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_25,axiom,
( sK8(Eq_x_0,Eq_x_1,Eq_x_2) = sK8(Eq_y_0,Eq_y_1,Eq_y_2)
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_26,axiom,
( sK9(Eq_x_0,Eq_x_1,Eq_x_2,Eq_x_3,Eq_x_4,Eq_x_5,Eq_x_6,Eq_x_7) = sK9(Eq_y_0,Eq_y_1,Eq_y_2,Eq_y_3,Eq_y_4,Eq_y_5,Eq_y_6,Eq_y_7)
| Eq_x_7 != Eq_y_7
| Eq_x_6 != Eq_y_6
| Eq_x_5 != Eq_y_5
| Eq_x_4 != Eq_y_4
| Eq_x_3 != Eq_y_3
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_27,axiom,
( sK10(Eq_x_0,Eq_x_1,Eq_x_2,Eq_x_3,Eq_x_4,Eq_x_5) = sK10(Eq_y_0,Eq_y_1,Eq_y_2,Eq_y_3,Eq_y_4,Eq_y_5)
| Eq_x_5 != Eq_y_5
| Eq_x_4 != Eq_y_4
| Eq_x_3 != Eq_y_3
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_28,axiom,
( sK11(Eq_x_0,Eq_x_1,Eq_x_2,Eq_x_3,Eq_x_4,Eq_x_5) = sK11(Eq_y_0,Eq_y_1,Eq_y_2,Eq_y_3,Eq_y_4,Eq_y_5)
| Eq_x_5 != Eq_y_5
| Eq_x_4 != Eq_y_4
| Eq_x_3 != Eq_y_3
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_29,axiom,
( sK12(Eq_x_0,Eq_x_1,Eq_x_2,Eq_x_3,Eq_x_4,Eq_x_5) = sK12(Eq_y_0,Eq_y_1,Eq_y_2,Eq_y_3,Eq_y_4,Eq_y_5)
| Eq_x_5 != Eq_y_5
| Eq_x_4 != Eq_y_4
| Eq_x_3 != Eq_y_3
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_30,axiom,
( sK13(Eq_x_0,Eq_x_1,Eq_x_2,Eq_x_3,Eq_x_4,Eq_x_5,Eq_x_6) = sK13(Eq_y_0,Eq_y_1,Eq_y_2,Eq_y_3,Eq_y_4,Eq_y_5,Eq_y_6)
| Eq_x_6 != Eq_y_6
| Eq_x_5 != Eq_y_5
| Eq_x_4 != Eq_y_4
| Eq_x_3 != Eq_y_3
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_31,axiom,
( sK14(Eq_x_0,Eq_x_1,Eq_x_2,Eq_x_3) = sK14(Eq_y_0,Eq_y_1,Eq_y_2,Eq_y_3)
| Eq_x_3 != Eq_y_3
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_32,axiom,
( sK15(Eq_x_0,Eq_x_1,Eq_x_2,Eq_x_3) = sK15(Eq_y_0,Eq_y_1,Eq_y_2,Eq_y_3)
| Eq_x_3 != Eq_y_3
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_33,axiom,
( sK16(Eq_x_0,Eq_x_1,Eq_x_2,Eq_x_3) = sK16(Eq_y_0,Eq_y_1,Eq_y_2,Eq_y_3)
| Eq_x_3 != Eq_y_3
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_34,axiom,
( sK17(Eq_x_0,Eq_x_1) = sK17(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_35,axiom,
( sK18(Eq_x_0,Eq_x_1,Eq_x_2) = sK18(Eq_y_0,Eq_y_1,Eq_y_2)
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_36,axiom,
( sK19(Eq_x_0,Eq_x_1,Eq_x_2) = sK19(Eq_y_0,Eq_y_1,Eq_y_2)
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_37,axiom,
( sK20(Eq_x_0,Eq_x_1,Eq_x_2) = sK20(Eq_y_0,Eq_y_1,Eq_y_2)
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_38,axiom,
( sK21(Eq_x_0,Eq_x_1,Eq_x_2,Eq_x_3) = sK21(Eq_y_0,Eq_y_1,Eq_y_2,Eq_y_3)
| Eq_x_3 != Eq_y_3
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_39,axiom,
( sK22(Eq_x_0,Eq_x_1,Eq_x_2) = sK22(Eq_y_0,Eq_y_1,Eq_y_2)
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_40,axiom,
( sK23(Eq_x_0,Eq_x_1,Eq_x_2,Eq_x_3) = sK23(Eq_y_0,Eq_y_1,Eq_y_2,Eq_y_3)
| Eq_x_3 != Eq_y_3
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_41,axiom,
( sK24(Eq_x_0,Eq_x_1,Eq_x_2,Eq_x_3) = sK24(Eq_y_0,Eq_y_1,Eq_y_2,Eq_y_3)
| Eq_x_3 != Eq_y_3
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_42,axiom,
( sK25(Eq_x_0,Eq_x_1,Eq_x_2) = sK25(Eq_y_0,Eq_y_1,Eq_y_2)
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_43,axiom,
( sK26(Eq_x_0,Eq_x_1,Eq_x_2,Eq_x_3) = sK26(Eq_y_0,Eq_y_1,Eq_y_2,Eq_y_3)
| Eq_x_3 != Eq_y_3
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_44,axiom,
( sK27(Eq_x_0,Eq_x_1,Eq_x_2) = sK27(Eq_y_0,Eq_y_1,Eq_y_2)
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_45,axiom,
( sK28(Eq_x_0,Eq_x_1,Eq_x_2,Eq_x_3) = sK28(Eq_y_0,Eq_y_1,Eq_y_2,Eq_y_3)
| Eq_x_3 != Eq_y_3
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_46,axiom,
( sK29(Eq_x_0,Eq_x_1,Eq_x_2,Eq_x_3,Eq_x_4) = sK29(Eq_y_0,Eq_y_1,Eq_y_2,Eq_y_3,Eq_y_4)
| Eq_x_4 != Eq_y_4
| Eq_x_3 != Eq_y_3
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_47,axiom,
( sK30(Eq_x_0,Eq_x_1,Eq_x_2,Eq_x_3,Eq_x_4) = sK30(Eq_y_0,Eq_y_1,Eq_y_2,Eq_y_3,Eq_y_4)
| Eq_x_4 != Eq_y_4
| Eq_x_3 != Eq_y_3
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_48,axiom,
( sK31(Eq_x_0,Eq_x_1,Eq_x_2,Eq_x_3,Eq_x_4) = sK31(Eq_y_0,Eq_y_1,Eq_y_2,Eq_y_3,Eq_y_4)
| Eq_x_4 != Eq_y_4
| Eq_x_3 != Eq_y_3
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_49,axiom,
( sK32(Eq_x_0,Eq_x_1,Eq_x_2,Eq_x_3,Eq_x_4) = sK32(Eq_y_0,Eq_y_1,Eq_y_2,Eq_y_3,Eq_y_4)
| Eq_x_4 != Eq_y_4
| Eq_x_3 != Eq_y_3
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_50,axiom,
( sK33(Eq_x_0,Eq_x_1,Eq_x_2,Eq_x_3,Eq_x_4) = sK33(Eq_y_0,Eq_y_1,Eq_y_2,Eq_y_3,Eq_y_4)
| Eq_x_4 != Eq_y_4
| Eq_x_3 != Eq_y_3
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_51,axiom,
( sK34(Eq_x_0,Eq_x_1,Eq_x_2,Eq_x_3,Eq_x_4) = sK34(Eq_y_0,Eq_y_1,Eq_y_2,Eq_y_3,Eq_y_4)
| Eq_x_4 != Eq_y_4
| Eq_x_3 != Eq_y_3
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_52,axiom,
( sK35(Eq_x_0,Eq_x_1,Eq_x_2,Eq_x_3,Eq_x_4) = sK35(Eq_y_0,Eq_y_1,Eq_y_2,Eq_y_3,Eq_y_4)
| Eq_x_4 != Eq_y_4
| Eq_x_3 != Eq_y_3
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_53,axiom,
( sK36(Eq_x_0,Eq_x_1,Eq_x_2,Eq_x_3,Eq_x_4) = sK36(Eq_y_0,Eq_y_1,Eq_y_2,Eq_y_3,Eq_y_4)
| Eq_x_4 != Eq_y_4
| Eq_x_3 != Eq_y_3
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_54,axiom,
( sK37(Eq_x_0,Eq_x_1,Eq_x_2,Eq_x_3,Eq_x_4) = sK37(Eq_y_0,Eq_y_1,Eq_y_2,Eq_y_3,Eq_y_4)
| Eq_x_4 != Eq_y_4
| Eq_x_3 != Eq_y_3
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_55,axiom,
( sK38(Eq_x_0,Eq_x_1,Eq_x_2,Eq_x_3,Eq_x_4) = sK38(Eq_y_0,Eq_y_1,Eq_y_2,Eq_y_3,Eq_y_4)
| Eq_x_4 != Eq_y_4
| Eq_x_3 != Eq_y_3
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_56,axiom,
( sK39(Eq_x_0,Eq_x_1,Eq_x_2,Eq_x_3,Eq_x_4) = sK39(Eq_y_0,Eq_y_1,Eq_y_2,Eq_y_3,Eq_y_4)
| Eq_x_4 != Eq_y_4
| Eq_x_3 != Eq_y_3
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_57,axiom,
( sK40(Eq_x_0,Eq_x_1,Eq_x_2,Eq_x_3,Eq_x_4) = sK40(Eq_y_0,Eq_y_1,Eq_y_2,Eq_y_3,Eq_y_4)
| Eq_x_4 != Eq_y_4
| Eq_x_3 != Eq_y_3
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_58,axiom,
( subset(Eq_y_0,Eq_y_1)
| ~ subset(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_59,axiom,
( member(Eq_y_0,Eq_y_1)
| ~ member(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_60,axiom,
( equal_set(Eq_y_0,Eq_y_1)
| ~ equal_set(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_61,axiom,
( maps(Eq_y_0,Eq_y_1,Eq_y_2)
| ~ maps(Eq_x_0,Eq_x_1,Eq_x_2)
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_62,axiom,
( apply(Eq_y_0,Eq_y_1,Eq_y_2)
| ~ apply(Eq_x_0,Eq_x_1,Eq_x_2)
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_63,axiom,
( compose_predicate(Eq_y_0,Eq_y_1,Eq_y_2,Eq_y_3,Eq_y_4,Eq_y_5)
| ~ compose_predicate(Eq_x_0,Eq_x_1,Eq_x_2,Eq_x_3,Eq_x_4,Eq_x_5)
| Eq_x_5 != Eq_y_5
| Eq_x_4 != Eq_y_4
| Eq_x_3 != Eq_y_3
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_64,axiom,
( equal_maps(Eq_y_0,Eq_y_1,Eq_y_2,Eq_y_3)
| ~ equal_maps(Eq_x_0,Eq_x_1,Eq_x_2,Eq_x_3)
| Eq_x_3 != Eq_y_3
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_65,axiom,
( identity(Eq_y_0,Eq_y_1)
| ~ identity(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_66,axiom,
( injective(Eq_y_0,Eq_y_1,Eq_y_2)
| ~ injective(Eq_x_0,Eq_x_1,Eq_x_2)
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_67,axiom,
( surjective(Eq_y_0,Eq_y_1,Eq_y_2)
| ~ surjective(Eq_x_0,Eq_x_1,Eq_x_2)
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_68,axiom,
( one_to_one(Eq_y_0,Eq_y_1,Eq_y_2)
| ~ one_to_one(Eq_x_0,Eq_x_1,Eq_x_2)
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_69,axiom,
( inverse_predicate(Eq_y_0,Eq_y_1,Eq_y_2,Eq_y_3)
| ~ inverse_predicate(Eq_x_0,Eq_x_1,Eq_x_2,Eq_x_3)
| Eq_x_3 != Eq_y_3
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_70,axiom,
( increasing(Eq_y_0,Eq_y_1,Eq_y_2,Eq_y_3,Eq_y_4)
| ~ increasing(Eq_x_0,Eq_x_1,Eq_x_2,Eq_x_3,Eq_x_4)
| Eq_x_4 != Eq_y_4
| Eq_x_3 != Eq_y_3
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_71,axiom,
( decreasing(Eq_y_0,Eq_y_1,Eq_y_2,Eq_y_3,Eq_y_4)
| ~ decreasing(Eq_x_0,Eq_x_1,Eq_x_2,Eq_x_3,Eq_x_4)
| Eq_x_4 != Eq_y_4
| Eq_x_3 != Eq_y_3
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_72,axiom,
( isomorphism(Eq_y_0,Eq_y_1,Eq_y_2,Eq_y_3,Eq_y_4)
| ~ isomorphism(Eq_x_0,Eq_x_1,Eq_x_2,Eq_x_3,Eq_x_4)
| Eq_x_4 != Eq_y_4
| Eq_x_3 != Eq_y_3
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(sat_proved,plain,
$false,
inference(cadical,[status(thm)],[]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SET720+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/sandbox/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.07/0.35 % Computer : n015.cluster.edu
% 0.07/0.35 % Model : x86_64 x86_64
% 0.07/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.35 % Memory : 8046.5625MB
% 0.07/0.35 % OS : Linux 6.8.0-71-generic
% 0.07/0.35 % CPULimit : 300
% 0.07/0.35 % WCLimit : 300
% 0.07/0.35 % DateTime : Sat Sep 19 22:53:35 UTC 2026
% 0.07/0.35 % CPUTime :
% 228.14/228.44 % SZS status Theorem for theBenchmark
% 228.14/228.44 % SZS output start Proof for theBenchmark
% See solution above
%------------------------------------------------------------------------------