%------------------------------------------------------------------------------
% File : ConnectPP---0.7.2
% Problem : SET094+1 : TPTP v9.3.1. Bugfixed v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n009.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:56:18 AM UTC 2026
% Result : Theorem 234.14s 234.42s
% Output : Proof 235.21s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
fof(subclass_defn,axiom,
! [X,Y] :
( subclass(X,Y)
<=> ! [U] :
( member(U,X)
=> member(U,Y) ) ),
file('SET005+0.ax',subclass_defn) ).
fof(class_elements_are_sets,axiom,
! [X] : subclass(X,universal_class),
file('SET005+0.ax',class_elements_are_sets) ).
fof(extensionality,axiom,
! [X,Y] :
( X = Y
<=> ( subclass(Y,X)
& subclass(X,Y) ) ),
file('SET005+0.ax',extensionality) ).
fof(unordered_pair_defn,axiom,
! [U,X,Y] :
( member(U,unordered_pair(X,Y))
<=> ( ( U = Y
| U = X )
& member(U,universal_class) ) ),
file('SET005+0.ax',unordered_pair_defn) ).
fof(unordered_pair,axiom,
! [X,Y] : member(unordered_pair(X,Y),universal_class),
file('SET005+0.ax',unordered_pair) ).
fof(singleton_set_defn,axiom,
! [X] : singleton(X) = unordered_pair(X,X),
file('SET005+0.ax',singleton_set_defn) ).
fof(ordered_pair_defn,axiom,
! [X,Y] : ordered_pair(X,Y) = unordered_pair(singleton(X),unordered_pair(X,singleton(Y))),
file('SET005+0.ax',ordered_pair_defn) ).
fof(cross_product_defn,axiom,
! [U,V,X,Y] :
( member(ordered_pair(U,V),cross_product(X,Y))
<=> ( member(V,Y)
& member(U,X) ) ),
file('SET005+0.ax',cross_product_defn) ).
fof(first_second,axiom,
! [X,Y] :
( ( member(Y,universal_class)
& member(X,universal_class) )
=> ( second(ordered_pair(X,Y)) = Y
& first(ordered_pair(X,Y)) = X ) ),
file('SET005+0.ax',first_second) ).
fof(cross_product,axiom,
! [X,Y,Z] :
( member(Z,cross_product(X,Y))
=> Z = ordered_pair(first(Z),second(Z)) ),
file('SET005+0.ax',cross_product) ).
fof(element_relation_defn,axiom,
! [X,Y] :
( member(ordered_pair(X,Y),element_relation)
<=> ( member(X,Y)
& member(Y,universal_class) ) ),
file('SET005+0.ax',element_relation_defn) ).
fof(element_relation,axiom,
subclass(element_relation,cross_product(universal_class,universal_class)),
file('SET005+0.ax',element_relation) ).
fof(intersection,axiom,
! [X,Y,Z] :
( member(Z,intersection(X,Y))
<=> ( member(Z,Y)
& member(Z,X) ) ),
file('SET005+0.ax',intersection) ).
fof(complement,axiom,
! [X,Z] :
( member(Z,complement(X))
<=> ( ~ member(Z,X)
& member(Z,universal_class) ) ),
file('SET005+0.ax',complement) ).
fof(restrict_defn,axiom,
! [X,XR,Y] : restrict(XR,X,Y) = intersection(XR,cross_product(X,Y)),
file('SET005+0.ax',restrict_defn) ).
fof(null_class_defn,axiom,
! [X] : ~ member(X,null_class),
file('SET005+0.ax',null_class_defn) ).
fof(domain_of,axiom,
! [X,Z] :
( member(Z,domain_of(X))
<=> ( restrict(X,singleton(Z),universal_class) != null_class
& member(Z,universal_class) ) ),
file('SET005+0.ax',domain_of) ).
fof(rotate_defn,axiom,
! [X,U,V,W] :
( member(ordered_pair(ordered_pair(U,V),W),rotate(X))
<=> ( member(ordered_pair(ordered_pair(V,W),U),X)
& member(ordered_pair(ordered_pair(U,V),W),cross_product(cross_product(universal_class,universal_class),universal_class)) ) ),
file('SET005+0.ax',rotate_defn) ).
fof(rotate,axiom,
! [X] : subclass(rotate(X),cross_product(cross_product(universal_class,universal_class),universal_class)),
file('SET005+0.ax',rotate) ).
fof(flip_defn,axiom,
! [U,V,W,X] :
( member(ordered_pair(ordered_pair(U,V),W),flip(X))
<=> ( member(ordered_pair(ordered_pair(V,U),W),X)
& member(ordered_pair(ordered_pair(U,V),W),cross_product(cross_product(universal_class,universal_class),universal_class)) ) ),
file('SET005+0.ax',flip_defn) ).
fof(flip,axiom,
! [X] : subclass(flip(X),cross_product(cross_product(universal_class,universal_class),universal_class)),
file('SET005+0.ax',flip) ).
fof(union_defn,axiom,
! [X,Y,Z] :
( member(Z,union(X,Y))
<=> ( member(Z,Y)
| member(Z,X) ) ),
file('SET005+0.ax',union_defn) ).
fof(successor_defn,axiom,
! [X] : successor(X) = union(X,singleton(X)),
file('SET005+0.ax',successor_defn) ).
fof(successor_relation_defn1,axiom,
subclass(successor_relation,cross_product(universal_class,universal_class)),
file('SET005+0.ax',successor_relation_defn1) ).
fof(successor_relation_defn2,axiom,
! [X,Y] :
( member(ordered_pair(X,Y),successor_relation)
<=> ( successor(X) = Y
& member(Y,universal_class)
& member(X,universal_class) ) ),
file('SET005+0.ax',successor_relation_defn2) ).
fof(inverse_defn,axiom,
! [Y] : inverse(Y) = domain_of(flip(cross_product(Y,universal_class))),
file('SET005+0.ax',inverse_defn) ).
fof(range_of_defn,axiom,
! [Z] : range_of(Z) = domain_of(inverse(Z)),
file('SET005+0.ax',range_of_defn) ).
fof(image_defn,axiom,
! [X,XR] : image(XR,X) = range_of(restrict(XR,X,universal_class)),
file('SET005+0.ax',image_defn) ).
fof(inductive_defn,axiom,
! [X] :
( inductive(X)
<=> ( subclass(image(successor_relation,X),X)
& member(null_class,X) ) ),
file('SET005+0.ax',inductive_defn) ).
fof(infinity,axiom,
? [X] :
( ! [Y] :
( inductive(Y)
=> subclass(X,Y) )
& inductive(X)
& member(X,universal_class) ),
file('SET005+0.ax',infinity) ).
fof(sum_class_defn,axiom,
! [U,X] :
( member(U,sum_class(X))
<=> ? [Y] :
( member(Y,X)
& member(U,Y) ) ),
file('SET005+0.ax',sum_class_defn) ).
fof(sum_class,axiom,
! [X] :
( member(X,universal_class)
=> member(sum_class(X),universal_class) ),
file('SET005+0.ax',sum_class) ).
fof(power_class_defn,axiom,
! [U,X] :
( member(U,power_class(X))
<=> ( subclass(U,X)
& member(U,universal_class) ) ),
file('SET005+0.ax',power_class_defn) ).
fof(power_class,axiom,
! [U] :
( member(U,universal_class)
=> member(power_class(U),universal_class) ),
file('SET005+0.ax',power_class) ).
fof(compose_defn1,axiom,
! [XR,YR] : subclass(compose(YR,XR),cross_product(universal_class,universal_class)),
file('SET005+0.ax',compose_defn1) ).
fof(compose_defn2,axiom,
! [XR,YR,U,V] :
( member(ordered_pair(U,V),compose(YR,XR))
<=> ( member(V,image(YR,image(XR,singleton(U))))
& member(U,universal_class) ) ),
file('SET005+0.ax',compose_defn2) ).
fof(identity_relation,axiom,
! [Z] :
( member(Z,identity_relation)
<=> ? [X] :
( Z = ordered_pair(X,X)
& member(X,universal_class) ) ),
file('SET005+0.ax',identity_relation) ).
fof(function_defn,axiom,
! [XF] :
( function(XF)
<=> ( subclass(compose(XF,inverse(XF)),identity_relation)
& subclass(XF,cross_product(universal_class,universal_class)) ) ),
file('SET005+0.ax',function_defn) ).
fof(replacement,axiom,
! [X,XF] :
( ( function(XF)
& member(X,universal_class) )
=> member(image(XF,X),universal_class) ),
file('SET005+0.ax',replacement) ).
fof(disjoint_defn,axiom,
! [X,Y] :
( disjoint(X,Y)
<=> ! [U] :
~ ( member(U,Y)
& member(U,X) ) ),
file('SET005+0.ax',disjoint_defn) ).
fof(regularity,axiom,
! [X] :
( X != null_class
=> ? [U] :
( disjoint(U,X)
& member(U,X)
& member(U,universal_class) ) ),
file('SET005+0.ax',regularity) ).
fof(apply_defn,axiom,
! [XF,Y] : apply(XF,Y) = sum_class(image(XF,singleton(Y))),
file('SET005+0.ax',apply_defn) ).
fof(choice,axiom,
? [XF] :
( ! [Y] :
( member(Y,universal_class)
=> ( member(apply(XF,Y),Y)
| Y = null_class ) )
& function(XF) ),
file('SET005+0.ax',choice) ).
fof(member_singleton_universal,axiom,
! [Y] :
( member(Y,universal_class)
=> member(member_of(singleton(Y)),universal_class) ),
file('theBenchmark.p',member_singleton_universal) ).
fof(member_singleton_singleton,axiom,
! [Y] :
( member(Y,universal_class)
=> singleton(member_of(singleton(Y))) = singleton(Y) ),
file('theBenchmark.p',member_singleton_singleton) ).
fof(member_universal_self,axiom,
! [X] :
( member_of(X) = X
| member(member_of(X),universal_class) ),
file('theBenchmark.p',member_universal_self) ).
fof(singleton_self,axiom,
! [X] :
( member_of(X) = X
| singleton(member_of(X)) = X ),
file('theBenchmark.p',singleton_self) ).
fof(property_of_singletons1_1,conjecture,
! [X,Y] :
( ( member(Y,X)
& singleton(member_of(X)) = X )
=> member_of(X) = Y ),
file('theBenchmark.p',property_of_singletons1_1) ).
fof(f_1_1,plain,
! [X,Y] :
( ( subclass(X,Y)
| ? [U] :
( ~ member(U,Y)
& member(U,X) ) )
& ( ! [U] :
( member(U,Y)
| ~ member(U,X) )
| ~ subclass(X,Y) ) ),
inference(fof_nnf,[status(thm)],[subclass_defn]) ).
fof(f_1_2,plain,
! [U_3,U_2] :
( ( subclass(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) )
| ~ subclass(U_3,U_2) ) ),
inference(variable_rename,[status(thm)],[f_1_1]) ).
fof(f_1_3,plain,
( ! [U_7,U_5] :
( subclass(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) )
| ~ subclass(U_6,U_4) ) ),
inference(miniscope,[status(thm)],[f_1_2]) ).
fof(f_1_4,plain,
( ! [U_7,U_5] :
( subclass(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) )
| ~ subclass(U_6,U_4) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1]),skolemize(U_1,sK1(U_7,U_5))],[f_1_3]) ).
fof(f_1_5,plain,
( ! [U_7,U_5] :
( ~ member(sK1(U_7,U_5),U_5)
| ~ sP0(U_7,U_5) )
& ! [U_7,U_5] :
( member(sK1(U_7,U_5),U_7)
| ~ sP0(U_7,U_5) )
& ! [U_7,U_5] :
( subclass(U_7,U_5)
| sP0(U_7,U_5) )
& ! [U_0,U_4,U_6] :
( member(U_0,U_4)
| ~ member(U_0,U_6)
| ~ subclass(U_6,U_4) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP0])],[f_1_4]) ).
cnf(f_1_6,plain,
( member(U_0,U_4)
| ~ member(U_0,U_6)
| ~ subclass(U_6,U_4) ),
inference(clausify,[status(thm)],[f_1_5]) ).
cnf(f_1_7,plain,
( subclass(U_7,U_5)
| sP0(U_7,U_5) ),
inference(clausify,[status(thm)],[f_1_5]) ).
cnf(f_1_8,plain,
( member(sK1(U_7,U_5),U_7)
| ~ sP0(U_7,U_5) ),
inference(clausify,[status(thm)],[f_1_5]) ).
cnf(f_1_9,plain,
( ~ member(sK1(U_7,U_5),U_5)
| ~ sP0(U_7,U_5) ),
inference(clausify,[status(thm)],[f_1_5]) ).
fof(f_2_1,plain,
! [X] : subclass(X,universal_class),
inference(fof_nnf,[status(thm)],[class_elements_are_sets]) ).
fof(f_2_2,plain,
! [U_8] : subclass(U_8,universal_class),
inference(variable_rename,[status(thm)],[f_2_1]) ).
fof(f_2_3,plain,
! [U_8] : subclass(U_8,universal_class),
inference(definitional_conversion,[status(esa)],[f_2_2]) ).
cnf(f_2_4,plain,
subclass(U_8,universal_class),
inference(clausify,[status(thm)],[f_2_3]) ).
fof(f_3_1,plain,
! [X,Y] :
( ( X = Y
| ~ subclass(Y,X)
| ~ subclass(X,Y) )
& ( ( subclass(Y,X)
& subclass(X,Y) )
| X != Y ) ),
inference(fof_nnf,[status(thm)],[extensionality]) ).
fof(f_3_2,plain,
! [U_10,U_9] :
( ( U_10 = U_9
| ~ subclass(U_9,U_10)
| ~ subclass(U_10,U_9) )
& ( ( subclass(U_9,U_10)
& subclass(U_10,U_9) )
| U_10 != U_9 ) ),
inference(variable_rename,[status(thm)],[f_3_1]) ).
fof(f_3_3,plain,
( ! [U_14,U_12] :
( U_14 = U_12
| ~ subclass(U_12,U_14)
| ~ subclass(U_14,U_12) )
& ! [U_13,U_11] :
( ( subclass(U_11,U_13)
& subclass(U_13,U_11) )
| U_13 != U_11 ) ),
inference(miniscope,[status(thm)],[f_3_2]) ).
fof(f_3_4,plain,
( ! [U_11,U_13] :
( subclass(U_11,U_13)
| ~ sP1(U_11,U_13) )
& ! [U_11,U_13] :
( subclass(U_13,U_11)
| ~ sP1(U_11,U_13) )
& ! [U_12,U_14] :
( U_14 = U_12
| ~ subclass(U_12,U_14)
| ~ subclass(U_14,U_12) )
& ! [U_11,U_13] :
( sP1(U_11,U_13)
| U_13 != U_11 ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP1])],[f_3_3]) ).
cnf(f_3_5,plain,
( sP1(U_11,U_13)
| U_13 != U_11 ),
inference(clausify,[status(thm)],[f_3_4]) ).
cnf(f_3_6,plain,
( U_14 = U_12
| ~ subclass(U_12,U_14)
| ~ subclass(U_14,U_12) ),
inference(clausify,[status(thm)],[f_3_4]) ).
cnf(f_3_7,plain,
( subclass(U_13,U_11)
| ~ sP1(U_11,U_13) ),
inference(clausify,[status(thm)],[f_3_4]) ).
cnf(f_3_8,plain,
( subclass(U_11,U_13)
| ~ sP1(U_11,U_13) ),
inference(clausify,[status(thm)],[f_3_4]) ).
fof(f_4_1,plain,
! [U,X,Y] :
( ( member(U,unordered_pair(X,Y))
| ( U != Y
& U != X )
| ~ member(U,universal_class) )
& ( ( ( U = Y
| U = X )
& member(U,universal_class) )
| ~ member(U,unordered_pair(X,Y)) ) ),
inference(fof_nnf,[status(thm)],[unordered_pair_defn]) ).
fof(f_4_2,plain,
! [U_17,U_16,U_15] :
( ( member(U_17,unordered_pair(U_16,U_15))
| ( U_17 != U_15
& U_17 != U_16 )
| ~ member(U_17,universal_class) )
& ( ( ( U_17 = U_15
| U_17 = U_16 )
& member(U_17,universal_class) )
| ~ member(U_17,unordered_pair(U_16,U_15)) ) ),
inference(variable_rename,[status(thm)],[f_4_1]) ).
fof(f_4_3,plain,
( ! [U_23,U_21,U_19] :
( member(U_23,unordered_pair(U_21,U_19))
| ( U_23 != U_19
& U_23 != U_21 )
| ~ member(U_23,universal_class) )
& ! [U_22,U_20,U_18] :
( ( ( U_22 = U_18
| U_22 = U_20 )
& member(U_22,universal_class) )
| ~ member(U_22,unordered_pair(U_20,U_18)) ) ),
inference(miniscope,[status(thm)],[f_4_2]) ).
fof(f_4_4,plain,
( ! [U_19,U_23,U_21] :
( U_23 != U_19
| ~ sP3(U_19,U_23,U_21) )
& ! [U_19,U_23,U_21] :
( U_23 != U_21
| ~ sP3(U_19,U_23,U_21) )
& ! [U_18,U_22,U_20] :
( U_22 = U_18
| U_22 = U_20
| ~ sP2(U_18,U_22,U_20) )
& ! [U_18,U_22,U_20] :
( member(U_22,universal_class)
| ~ sP2(U_18,U_22,U_20) )
& ! [U_19,U_23,U_21] :
( member(U_23,unordered_pair(U_21,U_19))
| sP3(U_19,U_23,U_21)
| ~ member(U_23,universal_class) )
& ! [U_18,U_22,U_20] :
( sP2(U_18,U_22,U_20)
| ~ member(U_22,unordered_pair(U_20,U_18)) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP2,sP3])],[f_4_3]) ).
cnf(f_4_5,plain,
( sP2(U_18,U_22,U_20)
| ~ member(U_22,unordered_pair(U_20,U_18)) ),
inference(clausify,[status(thm)],[f_4_4]) ).
cnf(f_4_6,plain,
( member(U_23,unordered_pair(U_21,U_19))
| sP3(U_19,U_23,U_21)
| ~ member(U_23,universal_class) ),
inference(clausify,[status(thm)],[f_4_4]) ).
cnf(f_4_7,plain,
( member(U_22,universal_class)
| ~ sP2(U_18,U_22,U_20) ),
inference(clausify,[status(thm)],[f_4_4]) ).
cnf(f_4_8,plain,
( U_22 = U_18
| U_22 = U_20
| ~ sP2(U_18,U_22,U_20) ),
inference(clausify,[status(thm)],[f_4_4]) ).
cnf(f_4_9,plain,
( U_23 != U_21
| ~ sP3(U_19,U_23,U_21) ),
inference(clausify,[status(thm)],[f_4_4]) ).
cnf(f_4_10,plain,
( U_23 != U_19
| ~ sP3(U_19,U_23,U_21) ),
inference(clausify,[status(thm)],[f_4_4]) ).
fof(f_5_1,plain,
! [X,Y] : member(unordered_pair(X,Y),universal_class),
inference(fof_nnf,[status(thm)],[unordered_pair]) ).
fof(f_5_2,plain,
! [U_25,U_24] : member(unordered_pair(U_25,U_24),universal_class),
inference(variable_rename,[status(thm)],[f_5_1]) ).
fof(f_5_3,plain,
! [U_24,U_25] : member(unordered_pair(U_25,U_24),universal_class),
inference(definitional_conversion,[status(esa)],[f_5_2]) ).
cnf(f_5_4,plain,
member(unordered_pair(U_25,U_24),universal_class),
inference(clausify,[status(thm)],[f_5_3]) ).
fof(f_6_1,plain,
! [X] : singleton(X) = unordered_pair(X,X),
inference(fof_nnf,[status(thm)],[singleton_set_defn]) ).
fof(f_6_2,plain,
! [U_26] : singleton(U_26) = unordered_pair(U_26,U_26),
inference(variable_rename,[status(thm)],[f_6_1]) ).
fof(f_6_3,plain,
! [U_26] : singleton(U_26) = unordered_pair(U_26,U_26),
inference(definitional_conversion,[status(esa)],[f_6_2]) ).
cnf(f_6_4,plain,
singleton(U_26) = unordered_pair(U_26,U_26),
inference(clausify,[status(thm)],[f_6_3]) ).
fof(f_7_1,plain,
! [X,Y] : ordered_pair(X,Y) = unordered_pair(singleton(X),unordered_pair(X,singleton(Y))),
inference(fof_nnf,[status(thm)],[ordered_pair_defn]) ).
fof(f_7_2,plain,
! [U_28,U_27] : ordered_pair(U_28,U_27) = unordered_pair(singleton(U_28),unordered_pair(U_28,singleton(U_27))),
inference(variable_rename,[status(thm)],[f_7_1]) ).
fof(f_7_3,plain,
! [U_27,U_28] : ordered_pair(U_28,U_27) = unordered_pair(singleton(U_28),unordered_pair(U_28,singleton(U_27))),
inference(definitional_conversion,[status(esa)],[f_7_2]) ).
cnf(f_7_4,plain,
ordered_pair(U_28,U_27) = unordered_pair(singleton(U_28),unordered_pair(U_28,singleton(U_27))),
inference(clausify,[status(thm)],[f_7_3]) ).
fof(f_8_1,plain,
! [U,V,X,Y] :
( ( member(ordered_pair(U,V),cross_product(X,Y))
| ~ member(V,Y)
| ~ member(U,X) )
& ( ( member(V,Y)
& member(U,X) )
| ~ member(ordered_pair(U,V),cross_product(X,Y)) ) ),
inference(fof_nnf,[status(thm)],[cross_product_defn]) ).
fof(f_8_2,plain,
! [U_32,U_31,U_30,U_29] :
( ( member(ordered_pair(U_32,U_31),cross_product(U_30,U_29))
| ~ member(U_31,U_29)
| ~ member(U_32,U_30) )
& ( ( member(U_31,U_29)
& member(U_32,U_30) )
| ~ member(ordered_pair(U_32,U_31),cross_product(U_30,U_29)) ) ),
inference(variable_rename,[status(thm)],[f_8_1]) ).
fof(f_8_3,plain,
( ! [U_40,U_38,U_36,U_34] :
( member(ordered_pair(U_40,U_38),cross_product(U_36,U_34))
| ~ member(U_38,U_34)
| ~ member(U_40,U_36) )
& ! [U_39,U_37,U_35,U_33] :
( ( member(U_37,U_33)
& member(U_39,U_35) )
| ~ member(ordered_pair(U_39,U_37),cross_product(U_35,U_33)) ) ),
inference(miniscope,[status(thm)],[f_8_2]) ).
fof(f_8_4,plain,
( ! [U_33,U_35,U_37,U_39] :
( member(U_37,U_33)
| ~ sP4(U_33,U_35,U_37,U_39) )
& ! [U_33,U_35,U_37,U_39] :
( member(U_39,U_35)
| ~ sP4(U_33,U_35,U_37,U_39) )
& ! [U_34,U_36,U_40,U_38] :
( member(ordered_pair(U_40,U_38),cross_product(U_36,U_34))
| ~ member(U_38,U_34)
| ~ member(U_40,U_36) )
& ! [U_33,U_35,U_37,U_39] :
( sP4(U_33,U_35,U_37,U_39)
| ~ member(ordered_pair(U_39,U_37),cross_product(U_35,U_33)) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP4])],[f_8_3]) ).
cnf(f_8_5,plain,
( sP4(U_33,U_35,U_37,U_39)
| ~ member(ordered_pair(U_39,U_37),cross_product(U_35,U_33)) ),
inference(clausify,[status(thm)],[f_8_4]) ).
cnf(f_8_6,plain,
( member(ordered_pair(U_40,U_38),cross_product(U_36,U_34))
| ~ member(U_38,U_34)
| ~ member(U_40,U_36) ),
inference(clausify,[status(thm)],[f_8_4]) ).
cnf(f_8_7,plain,
( member(U_39,U_35)
| ~ sP4(U_33,U_35,U_37,U_39) ),
inference(clausify,[status(thm)],[f_8_4]) ).
cnf(f_8_8,plain,
( member(U_37,U_33)
| ~ sP4(U_33,U_35,U_37,U_39) ),
inference(clausify,[status(thm)],[f_8_4]) ).
fof(f_9_1,plain,
! [X,Y] :
( ( second(ordered_pair(X,Y)) = Y
& first(ordered_pair(X,Y)) = X )
| ~ member(Y,universal_class)
| ~ member(X,universal_class) ),
inference(fof_nnf,[status(thm)],[first_second]) ).
fof(f_9_2,plain,
! [U_42,U_41] :
( ( second(ordered_pair(U_42,U_41)) = U_41
& first(ordered_pair(U_42,U_41)) = U_42 )
| ~ member(U_41,universal_class)
| ~ member(U_42,universal_class) ),
inference(variable_rename,[status(thm)],[f_9_1]) ).
fof(f_9_3,plain,
( ! [U_42,U_41] :
( second(ordered_pair(U_42,U_41)) = U_41
| ~ sP5(U_42,U_41) )
& ! [U_42,U_41] :
( first(ordered_pair(U_42,U_41)) = U_42
| ~ sP5(U_42,U_41) )
& ! [U_42,U_41] :
( sP5(U_42,U_41)
| ~ member(U_41,universal_class)
| ~ member(U_42,universal_class) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP5])],[f_9_2]) ).
cnf(f_9_4,plain,
( sP5(U_42,U_41)
| ~ member(U_41,universal_class)
| ~ member(U_42,universal_class) ),
inference(clausify,[status(thm)],[f_9_3]) ).
cnf(f_9_5,plain,
( first(ordered_pair(U_42,U_41)) = U_42
| ~ sP5(U_42,U_41) ),
inference(clausify,[status(thm)],[f_9_3]) ).
cnf(f_9_6,plain,
( second(ordered_pair(U_42,U_41)) = U_41
| ~ sP5(U_42,U_41) ),
inference(clausify,[status(thm)],[f_9_3]) ).
fof(f_10_1,plain,
! [X,Y,Z] :
( Z = ordered_pair(first(Z),second(Z))
| ~ member(Z,cross_product(X,Y)) ),
inference(fof_nnf,[status(thm)],[cross_product]) ).
fof(f_10_2,plain,
! [U_45,U_44,U_43] :
( U_43 = ordered_pair(first(U_43),second(U_43))
| ~ member(U_43,cross_product(U_45,U_44)) ),
inference(variable_rename,[status(thm)],[f_10_1]) ).
fof(f_10_3,plain,
! [U_43,U_44,U_45] :
( U_43 = ordered_pair(first(U_43),second(U_43))
| ~ member(U_43,cross_product(U_45,U_44)) ),
inference(definitional_conversion,[status(esa)],[f_10_2]) ).
cnf(f_10_4,plain,
( U_43 = ordered_pair(first(U_43),second(U_43))
| ~ member(U_43,cross_product(U_45,U_44)) ),
inference(clausify,[status(thm)],[f_10_3]) ).
fof(f_11_1,plain,
! [X,Y] :
( ( member(ordered_pair(X,Y),element_relation)
| ~ member(X,Y)
| ~ member(Y,universal_class) )
& ( ( member(X,Y)
& member(Y,universal_class) )
| ~ member(ordered_pair(X,Y),element_relation) ) ),
inference(fof_nnf,[status(thm)],[element_relation_defn]) ).
fof(f_11_2,plain,
! [U_47,U_46] :
( ( member(ordered_pair(U_47,U_46),element_relation)
| ~ member(U_47,U_46)
| ~ member(U_46,universal_class) )
& ( ( member(U_47,U_46)
& member(U_46,universal_class) )
| ~ member(ordered_pair(U_47,U_46),element_relation) ) ),
inference(variable_rename,[status(thm)],[f_11_1]) ).
fof(f_11_3,plain,
( ! [U_51,U_49] :
( member(ordered_pair(U_51,U_49),element_relation)
| ~ member(U_51,U_49)
| ~ member(U_49,universal_class) )
& ! [U_50,U_48] :
( ( member(U_50,U_48)
& member(U_48,universal_class) )
| ~ member(ordered_pair(U_50,U_48),element_relation) ) ),
inference(miniscope,[status(thm)],[f_11_2]) ).
fof(f_11_4,plain,
( ! [U_48,U_50] :
( member(U_50,U_48)
| ~ sP6(U_48,U_50) )
& ! [U_48,U_50] :
( member(U_48,universal_class)
| ~ sP6(U_48,U_50) )
& ! [U_51,U_49] :
( member(ordered_pair(U_51,U_49),element_relation)
| ~ member(U_51,U_49)
| ~ member(U_49,universal_class) )
& ! [U_48,U_50] :
( sP6(U_48,U_50)
| ~ member(ordered_pair(U_50,U_48),element_relation) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP6])],[f_11_3]) ).
cnf(f_11_5,plain,
( sP6(U_48,U_50)
| ~ member(ordered_pair(U_50,U_48),element_relation) ),
inference(clausify,[status(thm)],[f_11_4]) ).
cnf(f_11_6,plain,
( member(ordered_pair(U_51,U_49),element_relation)
| ~ member(U_51,U_49)
| ~ member(U_49,universal_class) ),
inference(clausify,[status(thm)],[f_11_4]) ).
cnf(f_11_7,plain,
( member(U_48,universal_class)
| ~ sP6(U_48,U_50) ),
inference(clausify,[status(thm)],[f_11_4]) ).
cnf(f_11_8,plain,
( member(U_50,U_48)
| ~ sP6(U_48,U_50) ),
inference(clausify,[status(thm)],[f_11_4]) ).
fof(f_12_1,plain,
subclass(element_relation,cross_product(universal_class,universal_class)),
inference(fof_nnf,[status(thm)],[element_relation]) ).
fof(f_12_2,plain,
subclass(element_relation,cross_product(universal_class,universal_class)),
inference(definitional_conversion,[status(esa)],[f_12_1]) ).
cnf(f_12_3,plain,
subclass(element_relation,cross_product(universal_class,universal_class)),
inference(clausify,[status(thm)],[f_12_2]) ).
fof(f_13_1,plain,
! [X,Y,Z] :
( ( member(Z,intersection(X,Y))
| ~ member(Z,Y)
| ~ member(Z,X) )
& ( ( member(Z,Y)
& member(Z,X) )
| ~ member(Z,intersection(X,Y)) ) ),
inference(fof_nnf,[status(thm)],[intersection]) ).
fof(f_13_2,plain,
! [U_54,U_53,U_52] :
( ( member(U_52,intersection(U_54,U_53))
| ~ member(U_52,U_53)
| ~ member(U_52,U_54) )
& ( ( member(U_52,U_53)
& member(U_52,U_54) )
| ~ member(U_52,intersection(U_54,U_53)) ) ),
inference(variable_rename,[status(thm)],[f_13_1]) ).
fof(f_13_3,plain,
( ! [U_60,U_58,U_56] :
( member(U_56,intersection(U_60,U_58))
| ~ member(U_56,U_58)
| ~ member(U_56,U_60) )
& ! [U_59,U_57,U_55] :
( ( member(U_55,U_57)
& member(U_55,U_59) )
| ~ member(U_55,intersection(U_59,U_57)) ) ),
inference(miniscope,[status(thm)],[f_13_2]) ).
fof(f_13_4,plain,
( ! [U_55,U_57,U_59] :
( member(U_55,U_57)
| ~ sP7(U_55,U_57,U_59) )
& ! [U_55,U_57,U_59] :
( member(U_55,U_59)
| ~ sP7(U_55,U_57,U_59) )
& ! [U_56,U_60,U_58] :
( member(U_56,intersection(U_60,U_58))
| ~ member(U_56,U_58)
| ~ member(U_56,U_60) )
& ! [U_55,U_57,U_59] :
( sP7(U_55,U_57,U_59)
| ~ member(U_55,intersection(U_59,U_57)) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP7])],[f_13_3]) ).
cnf(f_13_5,plain,
( sP7(U_55,U_57,U_59)
| ~ member(U_55,intersection(U_59,U_57)) ),
inference(clausify,[status(thm)],[f_13_4]) ).
cnf(f_13_6,plain,
( member(U_56,intersection(U_60,U_58))
| ~ member(U_56,U_58)
| ~ member(U_56,U_60) ),
inference(clausify,[status(thm)],[f_13_4]) ).
cnf(f_13_7,plain,
( member(U_55,U_59)
| ~ sP7(U_55,U_57,U_59) ),
inference(clausify,[status(thm)],[f_13_4]) ).
cnf(f_13_8,plain,
( member(U_55,U_57)
| ~ sP7(U_55,U_57,U_59) ),
inference(clausify,[status(thm)],[f_13_4]) ).
fof(f_14_1,plain,
! [X,Z] :
( ( member(Z,complement(X))
| member(Z,X)
| ~ member(Z,universal_class) )
& ( ( ~ member(Z,X)
& member(Z,universal_class) )
| ~ member(Z,complement(X)) ) ),
inference(fof_nnf,[status(thm)],[complement]) ).
fof(f_14_2,plain,
! [U_62,U_61] :
( ( member(U_61,complement(U_62))
| member(U_61,U_62)
| ~ member(U_61,universal_class) )
& ( ( ~ member(U_61,U_62)
& member(U_61,universal_class) )
| ~ member(U_61,complement(U_62)) ) ),
inference(variable_rename,[status(thm)],[f_14_1]) ).
fof(f_14_3,plain,
( ! [U_66,U_64] :
( member(U_64,complement(U_66))
| member(U_64,U_66)
| ~ member(U_64,universal_class) )
& ! [U_65,U_63] :
( ( ~ member(U_63,U_65)
& member(U_63,universal_class) )
| ~ member(U_63,complement(U_65)) ) ),
inference(miniscope,[status(thm)],[f_14_2]) ).
fof(f_14_4,plain,
( ! [U_65,U_63] :
( ~ member(U_63,U_65)
| ~ sP8(U_65,U_63) )
& ! [U_65,U_63] :
( member(U_63,universal_class)
| ~ sP8(U_65,U_63) )
& ! [U_64,U_66] :
( member(U_64,complement(U_66))
| member(U_64,U_66)
| ~ member(U_64,universal_class) )
& ! [U_65,U_63] :
( sP8(U_65,U_63)
| ~ member(U_63,complement(U_65)) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP8])],[f_14_3]) ).
cnf(f_14_5,plain,
( sP8(U_65,U_63)
| ~ member(U_63,complement(U_65)) ),
inference(clausify,[status(thm)],[f_14_4]) ).
cnf(f_14_6,plain,
( member(U_64,complement(U_66))
| member(U_64,U_66)
| ~ member(U_64,universal_class) ),
inference(clausify,[status(thm)],[f_14_4]) ).
cnf(f_14_7,plain,
( member(U_63,universal_class)
| ~ sP8(U_65,U_63) ),
inference(clausify,[status(thm)],[f_14_4]) ).
cnf(f_14_8,plain,
( ~ member(U_63,U_65)
| ~ sP8(U_65,U_63) ),
inference(clausify,[status(thm)],[f_14_4]) ).
fof(f_15_1,plain,
! [X,XR,Y] : restrict(XR,X,Y) = intersection(XR,cross_product(X,Y)),
inference(fof_nnf,[status(thm)],[restrict_defn]) ).
fof(f_15_2,plain,
! [U_69,U_68,U_67] : restrict(U_68,U_69,U_67) = intersection(U_68,cross_product(U_69,U_67)),
inference(variable_rename,[status(thm)],[f_15_1]) ).
fof(f_15_3,plain,
! [U_69,U_67,U_68] : restrict(U_68,U_69,U_67) = intersection(U_68,cross_product(U_69,U_67)),
inference(definitional_conversion,[status(esa)],[f_15_2]) ).
cnf(f_15_4,plain,
restrict(U_68,U_69,U_67) = intersection(U_68,cross_product(U_69,U_67)),
inference(clausify,[status(thm)],[f_15_3]) ).
fof(f_16_1,plain,
! [X] : ~ member(X,null_class),
inference(fof_nnf,[status(thm)],[null_class_defn]) ).
fof(f_16_2,plain,
! [U_70] : ~ member(U_70,null_class),
inference(variable_rename,[status(thm)],[f_16_1]) ).
fof(f_16_3,plain,
! [U_70] : ~ member(U_70,null_class),
inference(definitional_conversion,[status(esa)],[f_16_2]) ).
cnf(f_16_4,plain,
~ member(U_70,null_class),
inference(clausify,[status(thm)],[f_16_3]) ).
fof(f_17_1,plain,
! [X,Z] :
( ( member(Z,domain_of(X))
| restrict(X,singleton(Z),universal_class) = null_class
| ~ member(Z,universal_class) )
& ( ( restrict(X,singleton(Z),universal_class) != null_class
& member(Z,universal_class) )
| ~ member(Z,domain_of(X)) ) ),
inference(fof_nnf,[status(thm)],[domain_of]) ).
fof(f_17_2,plain,
! [U_72,U_71] :
( ( member(U_71,domain_of(U_72))
| restrict(U_72,singleton(U_71),universal_class) = null_class
| ~ member(U_71,universal_class) )
& ( ( restrict(U_72,singleton(U_71),universal_class) != null_class
& member(U_71,universal_class) )
| ~ member(U_71,domain_of(U_72)) ) ),
inference(variable_rename,[status(thm)],[f_17_1]) ).
fof(f_17_3,plain,
( ! [U_76,U_74] :
( member(U_74,domain_of(U_76))
| restrict(U_76,singleton(U_74),universal_class) = null_class
| ~ member(U_74,universal_class) )
& ! [U_75,U_73] :
( ( restrict(U_75,singleton(U_73),universal_class) != null_class
& member(U_73,universal_class) )
| ~ member(U_73,domain_of(U_75)) ) ),
inference(miniscope,[status(thm)],[f_17_2]) ).
fof(f_17_4,plain,
( ! [U_73,U_75] :
( restrict(U_75,singleton(U_73),universal_class) != null_class
| ~ sP9(U_73,U_75) )
& ! [U_73,U_75] :
( member(U_73,universal_class)
| ~ sP9(U_73,U_75) )
& ! [U_76,U_74] :
( member(U_74,domain_of(U_76))
| restrict(U_76,singleton(U_74),universal_class) = null_class
| ~ member(U_74,universal_class) )
& ! [U_73,U_75] :
( sP9(U_73,U_75)
| ~ member(U_73,domain_of(U_75)) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP9])],[f_17_3]) ).
cnf(f_17_5,plain,
( sP9(U_73,U_75)
| ~ member(U_73,domain_of(U_75)) ),
inference(clausify,[status(thm)],[f_17_4]) ).
cnf(f_17_6,plain,
( member(U_74,domain_of(U_76))
| restrict(U_76,singleton(U_74),universal_class) = null_class
| ~ member(U_74,universal_class) ),
inference(clausify,[status(thm)],[f_17_4]) ).
cnf(f_17_7,plain,
( member(U_73,universal_class)
| ~ sP9(U_73,U_75) ),
inference(clausify,[status(thm)],[f_17_4]) ).
cnf(f_17_8,plain,
( restrict(U_75,singleton(U_73),universal_class) != null_class
| ~ sP9(U_73,U_75) ),
inference(clausify,[status(thm)],[f_17_4]) ).
fof(f_18_1,plain,
! [X,U,V,W] :
( ( member(ordered_pair(ordered_pair(U,V),W),rotate(X))
| ~ member(ordered_pair(ordered_pair(V,W),U),X)
| ~ member(ordered_pair(ordered_pair(U,V),W),cross_product(cross_product(universal_class,universal_class),universal_class)) )
& ( ( member(ordered_pair(ordered_pair(V,W),U),X)
& member(ordered_pair(ordered_pair(U,V),W),cross_product(cross_product(universal_class,universal_class),universal_class)) )
| ~ member(ordered_pair(ordered_pair(U,V),W),rotate(X)) ) ),
inference(fof_nnf,[status(thm)],[rotate_defn]) ).
fof(f_18_2,plain,
! [U_80,U_79,U_78,U_77] :
( ( member(ordered_pair(ordered_pair(U_79,U_78),U_77),rotate(U_80))
| ~ member(ordered_pair(ordered_pair(U_78,U_77),U_79),U_80)
| ~ member(ordered_pair(ordered_pair(U_79,U_78),U_77),cross_product(cross_product(universal_class,universal_class),universal_class)) )
& ( ( member(ordered_pair(ordered_pair(U_78,U_77),U_79),U_80)
& member(ordered_pair(ordered_pair(U_79,U_78),U_77),cross_product(cross_product(universal_class,universal_class),universal_class)) )
| ~ member(ordered_pair(ordered_pair(U_79,U_78),U_77),rotate(U_80)) ) ),
inference(variable_rename,[status(thm)],[f_18_1]) ).
fof(f_18_3,plain,
( ! [U_88,U_86,U_84,U_82] :
( member(ordered_pair(ordered_pair(U_86,U_84),U_82),rotate(U_88))
| ~ member(ordered_pair(ordered_pair(U_84,U_82),U_86),U_88)
| ~ member(ordered_pair(ordered_pair(U_86,U_84),U_82),cross_product(cross_product(universal_class,universal_class),universal_class)) )
& ! [U_87,U_85,U_83,U_81] :
( ( member(ordered_pair(ordered_pair(U_83,U_81),U_85),U_87)
& member(ordered_pair(ordered_pair(U_85,U_83),U_81),cross_product(cross_product(universal_class,universal_class),universal_class)) )
| ~ member(ordered_pair(ordered_pair(U_85,U_83),U_81),rotate(U_87)) ) ),
inference(miniscope,[status(thm)],[f_18_2]) ).
fof(f_18_4,plain,
( ! [U_85,U_87,U_83,U_81] :
( member(ordered_pair(ordered_pair(U_83,U_81),U_85),U_87)
| ~ sP10(U_85,U_87,U_83,U_81) )
& ! [U_85,U_87,U_83,U_81] :
( member(ordered_pair(ordered_pair(U_85,U_83),U_81),cross_product(cross_product(universal_class,universal_class),universal_class))
| ~ sP10(U_85,U_87,U_83,U_81) )
& ! [U_82,U_88,U_86,U_84] :
( member(ordered_pair(ordered_pair(U_86,U_84),U_82),rotate(U_88))
| ~ member(ordered_pair(ordered_pair(U_84,U_82),U_86),U_88)
| ~ member(ordered_pair(ordered_pair(U_86,U_84),U_82),cross_product(cross_product(universal_class,universal_class),universal_class)) )
& ! [U_85,U_87,U_83,U_81] :
( sP10(U_85,U_87,U_83,U_81)
| ~ member(ordered_pair(ordered_pair(U_85,U_83),U_81),rotate(U_87)) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP10])],[f_18_3]) ).
cnf(f_18_5,plain,
( sP10(U_85,U_87,U_83,U_81)
| ~ member(ordered_pair(ordered_pair(U_85,U_83),U_81),rotate(U_87)) ),
inference(clausify,[status(thm)],[f_18_4]) ).
cnf(f_18_6,plain,
( member(ordered_pair(ordered_pair(U_86,U_84),U_82),rotate(U_88))
| ~ member(ordered_pair(ordered_pair(U_84,U_82),U_86),U_88)
| ~ member(ordered_pair(ordered_pair(U_86,U_84),U_82),cross_product(cross_product(universal_class,universal_class),universal_class)) ),
inference(clausify,[status(thm)],[f_18_4]) ).
cnf(f_18_7,plain,
( member(ordered_pair(ordered_pair(U_85,U_83),U_81),cross_product(cross_product(universal_class,universal_class),universal_class))
| ~ sP10(U_85,U_87,U_83,U_81) ),
inference(clausify,[status(thm)],[f_18_4]) ).
cnf(f_18_8,plain,
( member(ordered_pair(ordered_pair(U_83,U_81),U_85),U_87)
| ~ sP10(U_85,U_87,U_83,U_81) ),
inference(clausify,[status(thm)],[f_18_4]) ).
fof(f_19_1,plain,
! [X] : subclass(rotate(X),cross_product(cross_product(universal_class,universal_class),universal_class)),
inference(fof_nnf,[status(thm)],[rotate]) ).
fof(f_19_2,plain,
! [U_89] : subclass(rotate(U_89),cross_product(cross_product(universal_class,universal_class),universal_class)),
inference(variable_rename,[status(thm)],[f_19_1]) ).
fof(f_19_3,plain,
! [U_89] : subclass(rotate(U_89),cross_product(cross_product(universal_class,universal_class),universal_class)),
inference(definitional_conversion,[status(esa)],[f_19_2]) ).
cnf(f_19_4,plain,
subclass(rotate(U_89),cross_product(cross_product(universal_class,universal_class),universal_class)),
inference(clausify,[status(thm)],[f_19_3]) ).
fof(f_20_1,plain,
! [U,V,W,X] :
( ( member(ordered_pair(ordered_pair(U,V),W),flip(X))
| ~ member(ordered_pair(ordered_pair(V,U),W),X)
| ~ member(ordered_pair(ordered_pair(U,V),W),cross_product(cross_product(universal_class,universal_class),universal_class)) )
& ( ( member(ordered_pair(ordered_pair(V,U),W),X)
& member(ordered_pair(ordered_pair(U,V),W),cross_product(cross_product(universal_class,universal_class),universal_class)) )
| ~ member(ordered_pair(ordered_pair(U,V),W),flip(X)) ) ),
inference(fof_nnf,[status(thm)],[flip_defn]) ).
fof(f_20_2,plain,
! [U_93,U_92,U_91,U_90] :
( ( member(ordered_pair(ordered_pair(U_93,U_92),U_91),flip(U_90))
| ~ member(ordered_pair(ordered_pair(U_92,U_93),U_91),U_90)
| ~ member(ordered_pair(ordered_pair(U_93,U_92),U_91),cross_product(cross_product(universal_class,universal_class),universal_class)) )
& ( ( member(ordered_pair(ordered_pair(U_92,U_93),U_91),U_90)
& member(ordered_pair(ordered_pair(U_93,U_92),U_91),cross_product(cross_product(universal_class,universal_class),universal_class)) )
| ~ member(ordered_pair(ordered_pair(U_93,U_92),U_91),flip(U_90)) ) ),
inference(variable_rename,[status(thm)],[f_20_1]) ).
fof(f_20_3,plain,
( ! [U_101,U_99,U_97,U_95] :
( member(ordered_pair(ordered_pair(U_101,U_99),U_97),flip(U_95))
| ~ member(ordered_pair(ordered_pair(U_99,U_101),U_97),U_95)
| ~ member(ordered_pair(ordered_pair(U_101,U_99),U_97),cross_product(cross_product(universal_class,universal_class),universal_class)) )
& ! [U_100,U_98,U_96,U_94] :
( ( member(ordered_pair(ordered_pair(U_98,U_100),U_96),U_94)
& member(ordered_pair(ordered_pair(U_100,U_98),U_96),cross_product(cross_product(universal_class,universal_class),universal_class)) )
| ~ member(ordered_pair(ordered_pair(U_100,U_98),U_96),flip(U_94)) ) ),
inference(miniscope,[status(thm)],[f_20_2]) ).
fof(f_20_4,plain,
( ! [U_96,U_100,U_98,U_94] :
( member(ordered_pair(ordered_pair(U_98,U_100),U_96),U_94)
| ~ sP11(U_96,U_100,U_98,U_94) )
& ! [U_96,U_100,U_98,U_94] :
( member(ordered_pair(ordered_pair(U_100,U_98),U_96),cross_product(cross_product(universal_class,universal_class),universal_class))
| ~ sP11(U_96,U_100,U_98,U_94) )
& ! [U_95,U_97,U_101,U_99] :
( member(ordered_pair(ordered_pair(U_101,U_99),U_97),flip(U_95))
| ~ member(ordered_pair(ordered_pair(U_99,U_101),U_97),U_95)
| ~ member(ordered_pair(ordered_pair(U_101,U_99),U_97),cross_product(cross_product(universal_class,universal_class),universal_class)) )
& ! [U_96,U_100,U_98,U_94] :
( sP11(U_96,U_100,U_98,U_94)
| ~ member(ordered_pair(ordered_pair(U_100,U_98),U_96),flip(U_94)) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP11])],[f_20_3]) ).
cnf(f_20_5,plain,
( sP11(U_96,U_100,U_98,U_94)
| ~ member(ordered_pair(ordered_pair(U_100,U_98),U_96),flip(U_94)) ),
inference(clausify,[status(thm)],[f_20_4]) ).
cnf(f_20_6,plain,
( member(ordered_pair(ordered_pair(U_101,U_99),U_97),flip(U_95))
| ~ member(ordered_pair(ordered_pair(U_99,U_101),U_97),U_95)
| ~ member(ordered_pair(ordered_pair(U_101,U_99),U_97),cross_product(cross_product(universal_class,universal_class),universal_class)) ),
inference(clausify,[status(thm)],[f_20_4]) ).
cnf(f_20_7,plain,
( member(ordered_pair(ordered_pair(U_100,U_98),U_96),cross_product(cross_product(universal_class,universal_class),universal_class))
| ~ sP11(U_96,U_100,U_98,U_94) ),
inference(clausify,[status(thm)],[f_20_4]) ).
cnf(f_20_8,plain,
( member(ordered_pair(ordered_pair(U_98,U_100),U_96),U_94)
| ~ sP11(U_96,U_100,U_98,U_94) ),
inference(clausify,[status(thm)],[f_20_4]) ).
fof(f_21_1,plain,
! [X] : subclass(flip(X),cross_product(cross_product(universal_class,universal_class),universal_class)),
inference(fof_nnf,[status(thm)],[flip]) ).
fof(f_21_2,plain,
! [U_102] : subclass(flip(U_102),cross_product(cross_product(universal_class,universal_class),universal_class)),
inference(variable_rename,[status(thm)],[f_21_1]) ).
fof(f_21_3,plain,
! [U_102] : subclass(flip(U_102),cross_product(cross_product(universal_class,universal_class),universal_class)),
inference(definitional_conversion,[status(esa)],[f_21_2]) ).
cnf(f_21_4,plain,
subclass(flip(U_102),cross_product(cross_product(universal_class,universal_class),universal_class)),
inference(clausify,[status(thm)],[f_21_3]) ).
fof(f_22_1,plain,
! [X,Y,Z] :
( ( member(Z,union(X,Y))
| ( ~ member(Z,Y)
& ~ member(Z,X) ) )
& ( member(Z,Y)
| member(Z,X)
| ~ member(Z,union(X,Y)) ) ),
inference(fof_nnf,[status(thm)],[union_defn]) ).
fof(f_22_2,plain,
! [U_105,U_104,U_103] :
( ( member(U_103,union(U_105,U_104))
| ( ~ member(U_103,U_104)
& ~ member(U_103,U_105) ) )
& ( member(U_103,U_104)
| member(U_103,U_105)
| ~ member(U_103,union(U_105,U_104)) ) ),
inference(variable_rename,[status(thm)],[f_22_1]) ).
fof(f_22_3,plain,
( ! [U_111,U_109,U_107] :
( member(U_107,union(U_111,U_109))
| ( ~ member(U_107,U_109)
& ~ member(U_107,U_111) ) )
& ! [U_110,U_108,U_106] :
( member(U_106,U_108)
| member(U_106,U_110)
| ~ member(U_106,union(U_110,U_108)) ) ),
inference(miniscope,[status(thm)],[f_22_2]) ).
fof(f_22_4,plain,
( ! [U_107,U_109,U_111] :
( ~ member(U_107,U_109)
| ~ sP12(U_107,U_109,U_111) )
& ! [U_107,U_109,U_111] :
( ~ member(U_107,U_111)
| ~ sP12(U_107,U_109,U_111) )
& ! [U_107,U_109,U_111] :
( member(U_107,union(U_111,U_109))
| sP12(U_107,U_109,U_111) )
& ! [U_106,U_108,U_110] :
( member(U_106,U_108)
| member(U_106,U_110)
| ~ member(U_106,union(U_110,U_108)) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP12])],[f_22_3]) ).
cnf(f_22_5,plain,
( member(U_106,U_108)
| member(U_106,U_110)
| ~ member(U_106,union(U_110,U_108)) ),
inference(clausify,[status(thm)],[f_22_4]) ).
cnf(f_22_6,plain,
( member(U_107,union(U_111,U_109))
| sP12(U_107,U_109,U_111) ),
inference(clausify,[status(thm)],[f_22_4]) ).
cnf(f_22_7,plain,
( ~ member(U_107,U_111)
| ~ sP12(U_107,U_109,U_111) ),
inference(clausify,[status(thm)],[f_22_4]) ).
cnf(f_22_8,plain,
( ~ member(U_107,U_109)
| ~ sP12(U_107,U_109,U_111) ),
inference(clausify,[status(thm)],[f_22_4]) ).
fof(f_23_1,plain,
! [X] : successor(X) = union(X,singleton(X)),
inference(fof_nnf,[status(thm)],[successor_defn]) ).
fof(f_23_2,plain,
! [U_112] : successor(U_112) = union(U_112,singleton(U_112)),
inference(variable_rename,[status(thm)],[f_23_1]) ).
fof(f_23_3,plain,
! [U_112] : successor(U_112) = union(U_112,singleton(U_112)),
inference(definitional_conversion,[status(esa)],[f_23_2]) ).
cnf(f_23_4,plain,
successor(U_112) = union(U_112,singleton(U_112)),
inference(clausify,[status(thm)],[f_23_3]) ).
fof(f_24_1,plain,
subclass(successor_relation,cross_product(universal_class,universal_class)),
inference(fof_nnf,[status(thm)],[successor_relation_defn1]) ).
fof(f_24_2,plain,
subclass(successor_relation,cross_product(universal_class,universal_class)),
inference(definitional_conversion,[status(esa)],[f_24_1]) ).
cnf(f_24_3,plain,
subclass(successor_relation,cross_product(universal_class,universal_class)),
inference(clausify,[status(thm)],[f_24_2]) ).
fof(f_25_1,plain,
! [X,Y] :
( ( member(ordered_pair(X,Y),successor_relation)
| successor(X) != Y
| ~ member(Y,universal_class)
| ~ member(X,universal_class) )
& ( ( successor(X) = Y
& member(Y,universal_class)
& member(X,universal_class) )
| ~ member(ordered_pair(X,Y),successor_relation) ) ),
inference(fof_nnf,[status(thm)],[successor_relation_defn2]) ).
fof(f_25_2,plain,
! [U_114,U_113] :
( ( member(ordered_pair(U_114,U_113),successor_relation)
| successor(U_114) != U_113
| ~ member(U_113,universal_class)
| ~ member(U_114,universal_class) )
& ( ( successor(U_114) = U_113
& member(U_113,universal_class)
& member(U_114,universal_class) )
| ~ member(ordered_pair(U_114,U_113),successor_relation) ) ),
inference(variable_rename,[status(thm)],[f_25_1]) ).
fof(f_25_3,plain,
( ! [U_118,U_116] :
( member(ordered_pair(U_118,U_116),successor_relation)
| successor(U_118) != U_116
| ~ member(U_116,universal_class)
| ~ member(U_118,universal_class) )
& ! [U_117,U_115] :
( ( successor(U_117) = U_115
& member(U_115,universal_class)
& member(U_117,universal_class) )
| ~ member(ordered_pair(U_117,U_115),successor_relation) ) ),
inference(miniscope,[status(thm)],[f_25_2]) ).
fof(f_25_4,plain,
( ! [U_117,U_115] :
( successor(U_117) = U_115
| ~ sP13(U_117,U_115) )
& ! [U_117,U_115] :
( member(U_115,universal_class)
| ~ sP13(U_117,U_115) )
& ! [U_117,U_115] :
( member(U_117,universal_class)
| ~ sP13(U_117,U_115) )
& ! [U_116,U_118] :
( member(ordered_pair(U_118,U_116),successor_relation)
| successor(U_118) != U_116
| ~ member(U_116,universal_class)
| ~ member(U_118,universal_class) )
& ! [U_117,U_115] :
( sP13(U_117,U_115)
| ~ member(ordered_pair(U_117,U_115),successor_relation) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP13])],[f_25_3]) ).
cnf(f_25_5,plain,
( sP13(U_117,U_115)
| ~ member(ordered_pair(U_117,U_115),successor_relation) ),
inference(clausify,[status(thm)],[f_25_4]) ).
cnf(f_25_6,plain,
( member(ordered_pair(U_118,U_116),successor_relation)
| successor(U_118) != U_116
| ~ member(U_116,universal_class)
| ~ member(U_118,universal_class) ),
inference(clausify,[status(thm)],[f_25_4]) ).
cnf(f_25_7,plain,
( member(U_117,universal_class)
| ~ sP13(U_117,U_115) ),
inference(clausify,[status(thm)],[f_25_4]) ).
cnf(f_25_8,plain,
( member(U_115,universal_class)
| ~ sP13(U_117,U_115) ),
inference(clausify,[status(thm)],[f_25_4]) ).
cnf(f_25_9,plain,
( successor(U_117) = U_115
| ~ sP13(U_117,U_115) ),
inference(clausify,[status(thm)],[f_25_4]) ).
fof(f_26_1,plain,
! [Y] : inverse(Y) = domain_of(flip(cross_product(Y,universal_class))),
inference(fof_nnf,[status(thm)],[inverse_defn]) ).
fof(f_26_2,plain,
! [U_119] : inverse(U_119) = domain_of(flip(cross_product(U_119,universal_class))),
inference(variable_rename,[status(thm)],[f_26_1]) ).
fof(f_26_3,plain,
! [U_119] : inverse(U_119) = domain_of(flip(cross_product(U_119,universal_class))),
inference(definitional_conversion,[status(esa)],[f_26_2]) ).
cnf(f_26_4,plain,
inverse(U_119) = domain_of(flip(cross_product(U_119,universal_class))),
inference(clausify,[status(thm)],[f_26_3]) ).
fof(f_27_1,plain,
! [Z] : range_of(Z) = domain_of(inverse(Z)),
inference(fof_nnf,[status(thm)],[range_of_defn]) ).
fof(f_27_2,plain,
! [U_120] : range_of(U_120) = domain_of(inverse(U_120)),
inference(variable_rename,[status(thm)],[f_27_1]) ).
fof(f_27_3,plain,
! [U_120] : range_of(U_120) = domain_of(inverse(U_120)),
inference(definitional_conversion,[status(esa)],[f_27_2]) ).
cnf(f_27_4,plain,
range_of(U_120) = domain_of(inverse(U_120)),
inference(clausify,[status(thm)],[f_27_3]) ).
fof(f_28_1,plain,
! [X,XR] : image(XR,X) = range_of(restrict(XR,X,universal_class)),
inference(fof_nnf,[status(thm)],[image_defn]) ).
fof(f_28_2,plain,
! [U_122,U_121] : image(U_121,U_122) = range_of(restrict(U_121,U_122,universal_class)),
inference(variable_rename,[status(thm)],[f_28_1]) ).
fof(f_28_3,plain,
! [U_121,U_122] : image(U_121,U_122) = range_of(restrict(U_121,U_122,universal_class)),
inference(definitional_conversion,[status(esa)],[f_28_2]) ).
cnf(f_28_4,plain,
image(U_121,U_122) = range_of(restrict(U_121,U_122,universal_class)),
inference(clausify,[status(thm)],[f_28_3]) ).
fof(f_29_1,plain,
! [X] :
( ( inductive(X)
| ~ subclass(image(successor_relation,X),X)
| ~ member(null_class,X) )
& ( ( subclass(image(successor_relation,X),X)
& member(null_class,X) )
| ~ inductive(X) ) ),
inference(fof_nnf,[status(thm)],[inductive_defn]) ).
fof(f_29_2,plain,
! [U_123] :
( ( inductive(U_123)
| ~ subclass(image(successor_relation,U_123),U_123)
| ~ member(null_class,U_123) )
& ( ( subclass(image(successor_relation,U_123),U_123)
& member(null_class,U_123) )
| ~ inductive(U_123) ) ),
inference(variable_rename,[status(thm)],[f_29_1]) ).
fof(f_29_3,plain,
( ! [U_125] :
( inductive(U_125)
| ~ subclass(image(successor_relation,U_125),U_125)
| ~ member(null_class,U_125) )
& ! [U_124] :
( ( subclass(image(successor_relation,U_124),U_124)
& member(null_class,U_124) )
| ~ inductive(U_124) ) ),
inference(miniscope,[status(thm)],[f_29_2]) ).
fof(f_29_4,plain,
( ! [U_124] :
( subclass(image(successor_relation,U_124),U_124)
| ~ sP14(U_124) )
& ! [U_124] :
( member(null_class,U_124)
| ~ sP14(U_124) )
& ! [U_125] :
( inductive(U_125)
| ~ subclass(image(successor_relation,U_125),U_125)
| ~ member(null_class,U_125) )
& ! [U_124] :
( sP14(U_124)
| ~ inductive(U_124) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP14])],[f_29_3]) ).
cnf(f_29_5,plain,
( sP14(U_124)
| ~ inductive(U_124) ),
inference(clausify,[status(thm)],[f_29_4]) ).
cnf(f_29_6,plain,
( inductive(U_125)
| ~ subclass(image(successor_relation,U_125),U_125)
| ~ member(null_class,U_125) ),
inference(clausify,[status(thm)],[f_29_4]) ).
cnf(f_29_7,plain,
( member(null_class,U_124)
| ~ sP14(U_124) ),
inference(clausify,[status(thm)],[f_29_4]) ).
cnf(f_29_8,plain,
( subclass(image(successor_relation,U_124),U_124)
| ~ sP14(U_124) ),
inference(clausify,[status(thm)],[f_29_4]) ).
fof(f_30_1,plain,
? [X] :
( ! [Y] :
( subclass(X,Y)
| ~ inductive(Y) )
& inductive(X)
& member(X,universal_class) ),
inference(fof_nnf,[status(thm)],[infinity]) ).
fof(f_30_2,plain,
? [U_127] :
( ! [U_126] :
( subclass(U_127,U_126)
| ~ inductive(U_126) )
& inductive(U_127)
& member(U_127,universal_class) ),
inference(variable_rename,[status(thm)],[f_30_1]) ).
fof(f_30_3,plain,
( ! [U_126] :
( subclass(sK2,U_126)
| ~ inductive(U_126) )
& inductive(sK2)
& member(sK2,universal_class) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2]),skolemize(U_127,sK2)],[f_30_2]) ).
fof(f_30_4,plain,
( ! [U_126] :
( subclass(sK2,U_126)
| ~ inductive(U_126) )
& inductive(sK2)
& member(sK2,universal_class) ),
inference(definitional_conversion,[status(esa)],[f_30_3]) ).
cnf(f_30_5,plain,
member(sK2,universal_class),
inference(clausify,[status(thm)],[f_30_4]) ).
cnf(f_30_6,plain,
inductive(sK2),
inference(clausify,[status(thm)],[f_30_4]) ).
cnf(f_30_7,plain,
( subclass(sK2,U_126)
| ~ inductive(U_126) ),
inference(clausify,[status(thm)],[f_30_4]) ).
fof(f_31_1,plain,
! [U,X] :
( ( member(U,sum_class(X))
| ! [Y] :
( ~ member(Y,X)
| ~ member(U,Y) ) )
& ( ? [Y] :
( member(Y,X)
& member(U,Y) )
| ~ member(U,sum_class(X)) ) ),
inference(fof_nnf,[status(thm)],[sum_class_defn]) ).
fof(f_31_2,plain,
! [U_131,U_130] :
( ( member(U_131,sum_class(U_130))
| ! [U_129] :
( ~ member(U_129,U_130)
| ~ member(U_131,U_129) ) )
& ( ? [U_128] :
( member(U_128,U_130)
& member(U_131,U_128) )
| ~ member(U_131,sum_class(U_130)) ) ),
inference(variable_rename,[status(thm)],[f_31_1]) ).
fof(f_31_3,plain,
( ! [U_135,U_133] :
( member(U_135,sum_class(U_133))
| ! [U_129] :
( ~ member(U_129,U_133)
| ~ member(U_135,U_129) ) )
& ! [U_134,U_132] :
( ? [U_128] :
( member(U_128,U_132)
& member(U_134,U_128) )
| ~ member(U_134,sum_class(U_132)) ) ),
inference(miniscope,[status(thm)],[f_31_2]) ).
fof(f_31_4,plain,
( ! [U_135,U_133] :
( member(U_135,sum_class(U_133))
| ! [U_129] :
( ~ member(U_129,U_133)
| ~ member(U_135,U_129) ) )
& ! [U_134,U_132] :
( ( member(sK3(U_134,U_132),U_132)
& member(U_134,sK3(U_134,U_132)) )
| ~ member(U_134,sum_class(U_132)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3]),skolemize(U_128,sK3(U_134,U_132))],[f_31_3]) ).
fof(f_31_5,plain,
( ! [U_134,U_132] :
( member(sK3(U_134,U_132),U_132)
| ~ sP15(U_134,U_132) )
& ! [U_134,U_132] :
( member(U_134,sK3(U_134,U_132))
| ~ sP15(U_134,U_132) )
& ! [U_129,U_133,U_135] :
( member(U_135,sum_class(U_133))
| ~ member(U_129,U_133)
| ~ member(U_135,U_129) )
& ! [U_134,U_132] :
( sP15(U_134,U_132)
| ~ member(U_134,sum_class(U_132)) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP15])],[f_31_4]) ).
cnf(f_31_6,plain,
( sP15(U_134,U_132)
| ~ member(U_134,sum_class(U_132)) ),
inference(clausify,[status(thm)],[f_31_5]) ).
cnf(f_31_7,plain,
( member(U_135,sum_class(U_133))
| ~ member(U_129,U_133)
| ~ member(U_135,U_129) ),
inference(clausify,[status(thm)],[f_31_5]) ).
cnf(f_31_8,plain,
( member(U_134,sK3(U_134,U_132))
| ~ sP15(U_134,U_132) ),
inference(clausify,[status(thm)],[f_31_5]) ).
cnf(f_31_9,plain,
( member(sK3(U_134,U_132),U_132)
| ~ sP15(U_134,U_132) ),
inference(clausify,[status(thm)],[f_31_5]) ).
fof(f_32_1,plain,
! [X] :
( member(sum_class(X),universal_class)
| ~ member(X,universal_class) ),
inference(fof_nnf,[status(thm)],[sum_class]) ).
fof(f_32_2,plain,
! [U_136] :
( member(sum_class(U_136),universal_class)
| ~ member(U_136,universal_class) ),
inference(variable_rename,[status(thm)],[f_32_1]) ).
fof(f_32_3,plain,
! [U_136] :
( member(sum_class(U_136),universal_class)
| ~ member(U_136,universal_class) ),
inference(definitional_conversion,[status(esa)],[f_32_2]) ).
cnf(f_32_4,plain,
( member(sum_class(U_136),universal_class)
| ~ member(U_136,universal_class) ),
inference(clausify,[status(thm)],[f_32_3]) ).
fof(f_33_1,plain,
! [U,X] :
( ( member(U,power_class(X))
| ~ subclass(U,X)
| ~ member(U,universal_class) )
& ( ( subclass(U,X)
& member(U,universal_class) )
| ~ member(U,power_class(X)) ) ),
inference(fof_nnf,[status(thm)],[power_class_defn]) ).
fof(f_33_2,plain,
! [U_138,U_137] :
( ( member(U_138,power_class(U_137))
| ~ subclass(U_138,U_137)
| ~ member(U_138,universal_class) )
& ( ( subclass(U_138,U_137)
& member(U_138,universal_class) )
| ~ member(U_138,power_class(U_137)) ) ),
inference(variable_rename,[status(thm)],[f_33_1]) ).
fof(f_33_3,plain,
( ! [U_142,U_140] :
( member(U_142,power_class(U_140))
| ~ subclass(U_142,U_140)
| ~ member(U_142,universal_class) )
& ! [U_141,U_139] :
( ( subclass(U_141,U_139)
& member(U_141,universal_class) )
| ~ member(U_141,power_class(U_139)) ) ),
inference(miniscope,[status(thm)],[f_33_2]) ).
fof(f_33_4,plain,
( ! [U_141,U_139] :
( subclass(U_141,U_139)
| ~ sP16(U_141,U_139) )
& ! [U_141,U_139] :
( member(U_141,universal_class)
| ~ sP16(U_141,U_139) )
& ! [U_142,U_140] :
( member(U_142,power_class(U_140))
| ~ subclass(U_142,U_140)
| ~ member(U_142,universal_class) )
& ! [U_141,U_139] :
( sP16(U_141,U_139)
| ~ member(U_141,power_class(U_139)) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP16])],[f_33_3]) ).
cnf(f_33_5,plain,
( sP16(U_141,U_139)
| ~ member(U_141,power_class(U_139)) ),
inference(clausify,[status(thm)],[f_33_4]) ).
cnf(f_33_6,plain,
( member(U_142,power_class(U_140))
| ~ subclass(U_142,U_140)
| ~ member(U_142,universal_class) ),
inference(clausify,[status(thm)],[f_33_4]) ).
cnf(f_33_7,plain,
( member(U_141,universal_class)
| ~ sP16(U_141,U_139) ),
inference(clausify,[status(thm)],[f_33_4]) ).
cnf(f_33_8,plain,
( subclass(U_141,U_139)
| ~ sP16(U_141,U_139) ),
inference(clausify,[status(thm)],[f_33_4]) ).
fof(f_34_1,plain,
! [U] :
( member(power_class(U),universal_class)
| ~ member(U,universal_class) ),
inference(fof_nnf,[status(thm)],[power_class]) ).
fof(f_34_2,plain,
! [U_143] :
( member(power_class(U_143),universal_class)
| ~ member(U_143,universal_class) ),
inference(variable_rename,[status(thm)],[f_34_1]) ).
fof(f_34_3,plain,
! [U_143] :
( member(power_class(U_143),universal_class)
| ~ member(U_143,universal_class) ),
inference(definitional_conversion,[status(esa)],[f_34_2]) ).
cnf(f_34_4,plain,
( member(power_class(U_143),universal_class)
| ~ member(U_143,universal_class) ),
inference(clausify,[status(thm)],[f_34_3]) ).
fof(f_35_1,plain,
! [XR,YR] : subclass(compose(YR,XR),cross_product(universal_class,universal_class)),
inference(fof_nnf,[status(thm)],[compose_defn1]) ).
fof(f_35_2,plain,
! [U_145,U_144] : subclass(compose(U_144,U_145),cross_product(universal_class,universal_class)),
inference(variable_rename,[status(thm)],[f_35_1]) ).
fof(f_35_3,plain,
! [U_144,U_145] : subclass(compose(U_144,U_145),cross_product(universal_class,universal_class)),
inference(definitional_conversion,[status(esa)],[f_35_2]) ).
cnf(f_35_4,plain,
subclass(compose(U_144,U_145),cross_product(universal_class,universal_class)),
inference(clausify,[status(thm)],[f_35_3]) ).
fof(f_36_1,plain,
! [XR,YR,U,V] :
( ( member(ordered_pair(U,V),compose(YR,XR))
| ~ member(V,image(YR,image(XR,singleton(U))))
| ~ member(U,universal_class) )
& ( ( member(V,image(YR,image(XR,singleton(U))))
& member(U,universal_class) )
| ~ member(ordered_pair(U,V),compose(YR,XR)) ) ),
inference(fof_nnf,[status(thm)],[compose_defn2]) ).
fof(f_36_2,plain,
! [U_149,U_148,U_147,U_146] :
( ( member(ordered_pair(U_147,U_146),compose(U_148,U_149))
| ~ member(U_146,image(U_148,image(U_149,singleton(U_147))))
| ~ member(U_147,universal_class) )
& ( ( member(U_146,image(U_148,image(U_149,singleton(U_147))))
& member(U_147,universal_class) )
| ~ member(ordered_pair(U_147,U_146),compose(U_148,U_149)) ) ),
inference(variable_rename,[status(thm)],[f_36_1]) ).
fof(f_36_3,plain,
( ! [U_157,U_155,U_153,U_151] :
( member(ordered_pair(U_153,U_151),compose(U_155,U_157))
| ~ member(U_151,image(U_155,image(U_157,singleton(U_153))))
| ~ member(U_153,universal_class) )
& ! [U_156,U_154,U_152,U_150] :
( ( member(U_150,image(U_154,image(U_156,singleton(U_152))))
& member(U_152,universal_class) )
| ~ member(ordered_pair(U_152,U_150),compose(U_154,U_156)) ) ),
inference(miniscope,[status(thm)],[f_36_2]) ).
fof(f_36_4,plain,
( ! [U_150,U_154,U_152,U_156] :
( member(U_150,image(U_154,image(U_156,singleton(U_152))))
| ~ sP17(U_150,U_154,U_152,U_156) )
& ! [U_150,U_154,U_152,U_156] :
( member(U_152,universal_class)
| ~ sP17(U_150,U_154,U_152,U_156) )
& ! [U_151,U_153,U_155,U_157] :
( member(ordered_pair(U_153,U_151),compose(U_155,U_157))
| ~ member(U_151,image(U_155,image(U_157,singleton(U_153))))
| ~ member(U_153,universal_class) )
& ! [U_150,U_154,U_152,U_156] :
( sP17(U_150,U_154,U_152,U_156)
| ~ member(ordered_pair(U_152,U_150),compose(U_154,U_156)) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP17])],[f_36_3]) ).
cnf(f_36_5,plain,
( sP17(U_150,U_154,U_152,U_156)
| ~ member(ordered_pair(U_152,U_150),compose(U_154,U_156)) ),
inference(clausify,[status(thm)],[f_36_4]) ).
cnf(f_36_6,plain,
( member(ordered_pair(U_153,U_151),compose(U_155,U_157))
| ~ member(U_151,image(U_155,image(U_157,singleton(U_153))))
| ~ member(U_153,universal_class) ),
inference(clausify,[status(thm)],[f_36_4]) ).
cnf(f_36_7,plain,
( member(U_152,universal_class)
| ~ sP17(U_150,U_154,U_152,U_156) ),
inference(clausify,[status(thm)],[f_36_4]) ).
cnf(f_36_8,plain,
( member(U_150,image(U_154,image(U_156,singleton(U_152))))
| ~ sP17(U_150,U_154,U_152,U_156) ),
inference(clausify,[status(thm)],[f_36_4]) ).
fof(f_37_1,plain,
! [Z] :
( ( member(Z,identity_relation)
| ! [X] :
( Z != ordered_pair(X,X)
| ~ member(X,universal_class) ) )
& ( ? [X] :
( Z = ordered_pair(X,X)
& member(X,universal_class) )
| ~ member(Z,identity_relation) ) ),
inference(fof_nnf,[status(thm)],[identity_relation]) ).
fof(f_37_2,plain,
! [U_160] :
( ( member(U_160,identity_relation)
| ! [U_159] :
( U_160 != ordered_pair(U_159,U_159)
| ~ member(U_159,universal_class) ) )
& ( ? [U_158] :
( U_160 = ordered_pair(U_158,U_158)
& member(U_158,universal_class) )
| ~ member(U_160,identity_relation) ) ),
inference(variable_rename,[status(thm)],[f_37_1]) ).
fof(f_37_3,plain,
( ! [U_162] :
( member(U_162,identity_relation)
| ! [U_159] :
( U_162 != ordered_pair(U_159,U_159)
| ~ member(U_159,universal_class) ) )
& ! [U_161] :
( ? [U_158] :
( U_161 = ordered_pair(U_158,U_158)
& member(U_158,universal_class) )
| ~ member(U_161,identity_relation) ) ),
inference(miniscope,[status(thm)],[f_37_2]) ).
fof(f_37_4,plain,
( ! [U_162] :
( member(U_162,identity_relation)
| ! [U_159] :
( U_162 != ordered_pair(U_159,U_159)
| ~ member(U_159,universal_class) ) )
& ! [U_161] :
( ( U_161 = ordered_pair(sK4(U_161),sK4(U_161))
& member(sK4(U_161),universal_class) )
| ~ member(U_161,identity_relation) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4]),skolemize(U_158,sK4(U_161))],[f_37_3]) ).
fof(f_37_5,plain,
( ! [U_161] :
( U_161 = ordered_pair(sK4(U_161),sK4(U_161))
| ~ sP18(U_161) )
& ! [U_161] :
( member(sK4(U_161),universal_class)
| ~ sP18(U_161) )
& ! [U_159,U_162] :
( member(U_162,identity_relation)
| U_162 != ordered_pair(U_159,U_159)
| ~ member(U_159,universal_class) )
& ! [U_161] :
( sP18(U_161)
| ~ member(U_161,identity_relation) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP18])],[f_37_4]) ).
cnf(f_37_6,plain,
( sP18(U_161)
| ~ member(U_161,identity_relation) ),
inference(clausify,[status(thm)],[f_37_5]) ).
cnf(f_37_7,plain,
( member(U_162,identity_relation)
| U_162 != ordered_pair(U_159,U_159)
| ~ member(U_159,universal_class) ),
inference(clausify,[status(thm)],[f_37_5]) ).
cnf(f_37_8,plain,
( member(sK4(U_161),universal_class)
| ~ sP18(U_161) ),
inference(clausify,[status(thm)],[f_37_5]) ).
cnf(f_37_9,plain,
( U_161 = ordered_pair(sK4(U_161),sK4(U_161))
| ~ sP18(U_161) ),
inference(clausify,[status(thm)],[f_37_5]) ).
fof(f_38_1,plain,
! [XF] :
( ( function(XF)
| ~ subclass(compose(XF,inverse(XF)),identity_relation)
| ~ subclass(XF,cross_product(universal_class,universal_class)) )
& ( ( subclass(compose(XF,inverse(XF)),identity_relation)
& subclass(XF,cross_product(universal_class,universal_class)) )
| ~ function(XF) ) ),
inference(fof_nnf,[status(thm)],[function_defn]) ).
fof(f_38_2,plain,
! [U_163] :
( ( function(U_163)
| ~ subclass(compose(U_163,inverse(U_163)),identity_relation)
| ~ subclass(U_163,cross_product(universal_class,universal_class)) )
& ( ( subclass(compose(U_163,inverse(U_163)),identity_relation)
& subclass(U_163,cross_product(universal_class,universal_class)) )
| ~ function(U_163) ) ),
inference(variable_rename,[status(thm)],[f_38_1]) ).
fof(f_38_3,plain,
( ! [U_165] :
( function(U_165)
| ~ subclass(compose(U_165,inverse(U_165)),identity_relation)
| ~ subclass(U_165,cross_product(universal_class,universal_class)) )
& ! [U_164] :
( ( subclass(compose(U_164,inverse(U_164)),identity_relation)
& subclass(U_164,cross_product(universal_class,universal_class)) )
| ~ function(U_164) ) ),
inference(miniscope,[status(thm)],[f_38_2]) ).
fof(f_38_4,plain,
( ! [U_164] :
( subclass(compose(U_164,inverse(U_164)),identity_relation)
| ~ sP19(U_164) )
& ! [U_164] :
( subclass(U_164,cross_product(universal_class,universal_class))
| ~ sP19(U_164) )
& ! [U_165] :
( function(U_165)
| ~ subclass(compose(U_165,inverse(U_165)),identity_relation)
| ~ subclass(U_165,cross_product(universal_class,universal_class)) )
& ! [U_164] :
( sP19(U_164)
| ~ function(U_164) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP19])],[f_38_3]) ).
cnf(f_38_5,plain,
( sP19(U_164)
| ~ function(U_164) ),
inference(clausify,[status(thm)],[f_38_4]) ).
cnf(f_38_6,plain,
( function(U_165)
| ~ subclass(compose(U_165,inverse(U_165)),identity_relation)
| ~ subclass(U_165,cross_product(universal_class,universal_class)) ),
inference(clausify,[status(thm)],[f_38_4]) ).
cnf(f_38_7,plain,
( subclass(U_164,cross_product(universal_class,universal_class))
| ~ sP19(U_164) ),
inference(clausify,[status(thm)],[f_38_4]) ).
cnf(f_38_8,plain,
( subclass(compose(U_164,inverse(U_164)),identity_relation)
| ~ sP19(U_164) ),
inference(clausify,[status(thm)],[f_38_4]) ).
fof(f_39_1,plain,
! [X,XF] :
( member(image(XF,X),universal_class)
| ~ function(XF)
| ~ member(X,universal_class) ),
inference(fof_nnf,[status(thm)],[replacement]) ).
fof(f_39_2,plain,
! [U_167,U_166] :
( member(image(U_166,U_167),universal_class)
| ~ function(U_166)
| ~ member(U_167,universal_class) ),
inference(variable_rename,[status(thm)],[f_39_1]) ).
fof(f_39_3,plain,
! [U_167,U_166] :
( member(image(U_166,U_167),universal_class)
| ~ function(U_166)
| ~ member(U_167,universal_class) ),
inference(definitional_conversion,[status(esa)],[f_39_2]) ).
cnf(f_39_4,plain,
( member(image(U_166,U_167),universal_class)
| ~ function(U_166)
| ~ member(U_167,universal_class) ),
inference(clausify,[status(thm)],[f_39_3]) ).
fof(f_40_1,plain,
! [X,Y] :
( ( disjoint(X,Y)
| ? [U] :
( member(U,Y)
& member(U,X) ) )
& ( ! [U] :
( ~ member(U,Y)
| ~ member(U,X) )
| ~ disjoint(X,Y) ) ),
inference(fof_nnf,[status(thm)],[disjoint_defn]) ).
fof(f_40_2,plain,
! [U_171,U_170] :
( ( disjoint(U_171,U_170)
| ? [U_169] :
( member(U_169,U_170)
& member(U_169,U_171) ) )
& ( ! [U_168] :
( ~ member(U_168,U_170)
| ~ member(U_168,U_171) )
| ~ disjoint(U_171,U_170) ) ),
inference(variable_rename,[status(thm)],[f_40_1]) ).
fof(f_40_3,plain,
( ! [U_175,U_173] :
( disjoint(U_175,U_173)
| ? [U_169] :
( member(U_169,U_173)
& member(U_169,U_175) ) )
& ! [U_174,U_172] :
( ! [U_168] :
( ~ member(U_168,U_172)
| ~ member(U_168,U_174) )
| ~ disjoint(U_174,U_172) ) ),
inference(miniscope,[status(thm)],[f_40_2]) ).
fof(f_40_4,plain,
( ! [U_175,U_173] :
( disjoint(U_175,U_173)
| ( member(sK5(U_175,U_173),U_173)
& member(sK5(U_175,U_173),U_175) ) )
& ! [U_174,U_172] :
( ! [U_168] :
( ~ member(U_168,U_172)
| ~ member(U_168,U_174) )
| ~ disjoint(U_174,U_172) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK5]),skolemize(U_169,sK5(U_175,U_173))],[f_40_3]) ).
fof(f_40_5,plain,
( ! [U_175,U_173] :
( member(sK5(U_175,U_173),U_173)
| ~ sP20(U_175,U_173) )
& ! [U_175,U_173] :
( member(sK5(U_175,U_173),U_175)
| ~ sP20(U_175,U_173) )
& ! [U_175,U_173] :
( disjoint(U_175,U_173)
| sP20(U_175,U_173) )
& ! [U_174,U_172,U_168] :
( ~ member(U_168,U_172)
| ~ member(U_168,U_174)
| ~ disjoint(U_174,U_172) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP20])],[f_40_4]) ).
cnf(f_40_6,plain,
( ~ member(U_168,U_172)
| ~ member(U_168,U_174)
| ~ disjoint(U_174,U_172) ),
inference(clausify,[status(thm)],[f_40_5]) ).
cnf(f_40_7,plain,
( disjoint(U_175,U_173)
| sP20(U_175,U_173) ),
inference(clausify,[status(thm)],[f_40_5]) ).
cnf(f_40_8,plain,
( member(sK5(U_175,U_173),U_175)
| ~ sP20(U_175,U_173) ),
inference(clausify,[status(thm)],[f_40_5]) ).
cnf(f_40_9,plain,
( member(sK5(U_175,U_173),U_173)
| ~ sP20(U_175,U_173) ),
inference(clausify,[status(thm)],[f_40_5]) ).
fof(f_41_1,plain,
! [X] :
( ? [U] :
( disjoint(U,X)
& member(U,X)
& member(U,universal_class) )
| X = null_class ),
inference(fof_nnf,[status(thm)],[regularity]) ).
fof(f_41_2,plain,
! [U_177] :
( ? [U_176] :
( disjoint(U_176,U_177)
& member(U_176,U_177)
& member(U_176,universal_class) )
| U_177 = null_class ),
inference(variable_rename,[status(thm)],[f_41_1]) ).
fof(f_41_3,plain,
! [U_177] :
( ( disjoint(sK6(U_177),U_177)
& member(sK6(U_177),U_177)
& member(sK6(U_177),universal_class) )
| U_177 = null_class ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK6]),skolemize(U_176,sK6(U_177))],[f_41_2]) ).
fof(f_41_4,plain,
( ! [U_177] :
( disjoint(sK6(U_177),U_177)
| ~ sP21(U_177) )
& ! [U_177] :
( member(sK6(U_177),U_177)
| ~ sP21(U_177) )
& ! [U_177] :
( member(sK6(U_177),universal_class)
| ~ sP21(U_177) )
& ! [U_177] :
( sP21(U_177)
| U_177 = null_class ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP21])],[f_41_3]) ).
cnf(f_41_5,plain,
( sP21(U_177)
| U_177 = null_class ),
inference(clausify,[status(thm)],[f_41_4]) ).
cnf(f_41_6,plain,
( member(sK6(U_177),universal_class)
| ~ sP21(U_177) ),
inference(clausify,[status(thm)],[f_41_4]) ).
cnf(f_41_7,plain,
( member(sK6(U_177),U_177)
| ~ sP21(U_177) ),
inference(clausify,[status(thm)],[f_41_4]) ).
cnf(f_41_8,plain,
( disjoint(sK6(U_177),U_177)
| ~ sP21(U_177) ),
inference(clausify,[status(thm)],[f_41_4]) ).
fof(f_42_1,plain,
! [XF,Y] : apply(XF,Y) = sum_class(image(XF,singleton(Y))),
inference(fof_nnf,[status(thm)],[apply_defn]) ).
fof(f_42_2,plain,
! [U_179,U_178] : apply(U_179,U_178) = sum_class(image(U_179,singleton(U_178))),
inference(variable_rename,[status(thm)],[f_42_1]) ).
fof(f_42_3,plain,
! [U_178,U_179] : apply(U_179,U_178) = sum_class(image(U_179,singleton(U_178))),
inference(definitional_conversion,[status(esa)],[f_42_2]) ).
cnf(f_42_4,plain,
apply(U_179,U_178) = sum_class(image(U_179,singleton(U_178))),
inference(clausify,[status(thm)],[f_42_3]) ).
fof(f_43_1,plain,
? [XF] :
( ! [Y] :
( member(apply(XF,Y),Y)
| Y = null_class
| ~ member(Y,universal_class) )
& function(XF) ),
inference(fof_nnf,[status(thm)],[choice]) ).
fof(f_43_2,plain,
? [U_181] :
( ! [U_180] :
( member(apply(U_181,U_180),U_180)
| U_180 = null_class
| ~ member(U_180,universal_class) )
& function(U_181) ),
inference(variable_rename,[status(thm)],[f_43_1]) ).
fof(f_43_3,plain,
( ! [U_180] :
( member(apply(sK7,U_180),U_180)
| U_180 = null_class
| ~ member(U_180,universal_class) )
& function(sK7) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK7]),skolemize(U_181,sK7)],[f_43_2]) ).
fof(f_43_4,plain,
( ! [U_180] :
( member(apply(sK7,U_180),U_180)
| U_180 = null_class
| ~ member(U_180,universal_class) )
& function(sK7) ),
inference(definitional_conversion,[status(esa)],[f_43_3]) ).
cnf(f_43_5,plain,
function(sK7),
inference(clausify,[status(thm)],[f_43_4]) ).
cnf(f_43_6,plain,
( member(apply(sK7,U_180),U_180)
| U_180 = null_class
| ~ member(U_180,universal_class) ),
inference(clausify,[status(thm)],[f_43_4]) ).
fof(f_44_1,plain,
! [Y] :
( member(member_of(singleton(Y)),universal_class)
| ~ member(Y,universal_class) ),
inference(fof_nnf,[status(thm)],[member_singleton_universal]) ).
fof(f_44_2,plain,
! [U_182] :
( member(member_of(singleton(U_182)),universal_class)
| ~ member(U_182,universal_class) ),
inference(variable_rename,[status(thm)],[f_44_1]) ).
fof(f_44_3,plain,
! [U_182] :
( member(member_of(singleton(U_182)),universal_class)
| ~ member(U_182,universal_class) ),
inference(definitional_conversion,[status(esa)],[f_44_2]) ).
cnf(f_44_4,plain,
( member(member_of(singleton(U_182)),universal_class)
| ~ member(U_182,universal_class) ),
inference(clausify,[status(thm)],[f_44_3]) ).
fof(f_45_1,plain,
! [Y] :
( singleton(member_of(singleton(Y))) = singleton(Y)
| ~ member(Y,universal_class) ),
inference(fof_nnf,[status(thm)],[member_singleton_singleton]) ).
fof(f_45_2,plain,
! [U_183] :
( singleton(member_of(singleton(U_183))) = singleton(U_183)
| ~ member(U_183,universal_class) ),
inference(variable_rename,[status(thm)],[f_45_1]) ).
fof(f_45_3,plain,
! [U_183] :
( singleton(member_of(singleton(U_183))) = singleton(U_183)
| ~ member(U_183,universal_class) ),
inference(definitional_conversion,[status(esa)],[f_45_2]) ).
cnf(f_45_4,plain,
( singleton(member_of(singleton(U_183))) = singleton(U_183)
| ~ member(U_183,universal_class) ),
inference(clausify,[status(thm)],[f_45_3]) ).
fof(f_46_1,plain,
! [X] :
( member_of(X) = X
| member(member_of(X),universal_class) ),
inference(fof_nnf,[status(thm)],[member_universal_self]) ).
fof(f_46_2,plain,
! [U_184] :
( member_of(U_184) = U_184
| member(member_of(U_184),universal_class) ),
inference(variable_rename,[status(thm)],[f_46_1]) ).
fof(f_46_3,plain,
! [U_184] :
( member_of(U_184) = U_184
| member(member_of(U_184),universal_class) ),
inference(definitional_conversion,[status(esa)],[f_46_2]) ).
cnf(f_46_4,plain,
( member_of(U_184) = U_184
| member(member_of(U_184),universal_class) ),
inference(clausify,[status(thm)],[f_46_3]) ).
fof(f_47_1,plain,
! [X] :
( member_of(X) = X
| singleton(member_of(X)) = X ),
inference(fof_nnf,[status(thm)],[singleton_self]) ).
fof(f_47_2,plain,
! [U_185] :
( member_of(U_185) = U_185
| singleton(member_of(U_185)) = U_185 ),
inference(variable_rename,[status(thm)],[f_47_1]) ).
fof(f_47_3,plain,
! [U_185] :
( member_of(U_185) = U_185
| singleton(member_of(U_185)) = U_185 ),
inference(definitional_conversion,[status(esa)],[f_47_2]) ).
cnf(f_47_4,plain,
( member_of(U_185) = U_185
| singleton(member_of(U_185)) = U_185 ),
inference(clausify,[status(thm)],[f_47_3]) ).
fof(f_48_1,negated_conjecture,
~ ! [X,Y] :
( ( member(Y,X)
& singleton(member_of(X)) = X )
=> member_of(X) = Y ),
inference(negate,[status(cth)],[property_of_singletons1_1]) ).
fof(f_48_2,negated_conjecture,
? [X,Y] :
( member_of(X) != Y
& member(Y,X)
& singleton(member_of(X)) = X ),
inference(fof_nnf,[status(thm)],[f_48_1]) ).
fof(f_48_3,negated_conjecture,
? [U_187,U_186] :
( member_of(U_187) != U_186
& member(U_186,U_187)
& singleton(member_of(U_187)) = U_187 ),
inference(variable_rename,[status(thm)],[f_48_2]) ).
fof(f_48_4,negated_conjecture,
? [U_186] :
( member_of(sK8) != U_186
& member(U_186,sK8)
& singleton(member_of(sK8)) = sK8 ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK8]),skolemize(U_187,sK8)],[f_48_3]) ).
fof(f_48_5,negated_conjecture,
( member_of(sK8) != sK9
& member(sK9,sK8)
& singleton(member_of(sK8)) = sK8 ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK9]),skolemize(U_186,sK9)],[f_48_4]) ).
fof(f_48_6,negated_conjecture,
( member_of(sK8) != sK9
& member(sK9,sK8)
& singleton(member_of(sK8)) = sK8 ),
inference(definitional_conversion,[status(esa)],[f_48_5]) ).
cnf(f_48_7,negated_conjecture,
singleton(member_of(sK8)) = sK8,
inference(clausify,[status(thm)],[f_48_6]) ).
cnf(f_48_8,negated_conjecture,
member(sK9,sK8),
inference(clausify,[status(thm)],[f_48_6]) ).
cnf(f_48_9,negated_conjecture,
member_of(sK8) != sK9,
inference(clausify,[status(thm)],[f_48_6]) ).
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,
( 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_5,axiom,
( singleton(Eq_x_0) = singleton(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_6,axiom,
( ordered_pair(Eq_x_0,Eq_x_1) = ordered_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_7,axiom,
( cross_product(Eq_x_0,Eq_x_1) = cross_product(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,
( first(Eq_x_0) = first(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_9,axiom,
( second(Eq_x_0) = second(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_10,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_11,axiom,
( complement(Eq_x_0) = complement(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_12,axiom,
( restrict(Eq_x_0,Eq_x_1,Eq_x_2) = restrict(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_13,axiom,
( domain_of(Eq_x_0) = domain_of(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_14,axiom,
( rotate(Eq_x_0) = rotate(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_15,axiom,
( flip(Eq_x_0) = flip(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_16,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_17,axiom,
( successor(Eq_x_0) = successor(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_18,axiom,
( inverse(Eq_x_0) = inverse(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_19,axiom,
( range_of(Eq_x_0) = range_of(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_20,axiom,
( image(Eq_x_0,Eq_x_1) = image(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_21,axiom,
( sum_class(Eq_x_0) = sum_class(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_22,axiom,
( power_class(Eq_x_0) = power_class(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_23,axiom,
( compose(Eq_x_0,Eq_x_1) = compose(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_24,axiom,
( apply(Eq_x_0,Eq_x_1) = apply(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_25,axiom,
( member_of(Eq_x_0) = member_of(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_26,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_27,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_28,axiom,
( sK4(Eq_x_0) = sK4(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_29,axiom,
( sK5(Eq_x_0,Eq_x_1) = sK5(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_30,axiom,
( sK6(Eq_x_0) = sK6(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_31,axiom,
( subclass(Eq_y_0,Eq_y_1)
| ~ subclass(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_32,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_33,axiom,
( inductive(Eq_y_0)
| ~ inductive(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_34,axiom,
( function(Eq_y_0)
| ~ function(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_35,axiom,
( disjoint(Eq_y_0,Eq_y_1)
| ~ disjoint(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_36,axiom,
( sP0(Eq_y_0,Eq_y_1)
| ~ sP0(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_37,axiom,
( sP1(Eq_y_0,Eq_y_1)
| ~ sP1(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_38,axiom,
( sP2(Eq_y_0,Eq_y_1,Eq_y_2)
| ~ sP2(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_39,axiom,
( sP3(Eq_y_0,Eq_y_1,Eq_y_2)
| ~ sP3(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_40,axiom,
( sP4(Eq_y_0,Eq_y_1,Eq_y_2,Eq_y_3)
| ~ sP4(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_41,axiom,
( sP5(Eq_y_0,Eq_y_1)
| ~ sP5(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_42,axiom,
( sP6(Eq_y_0,Eq_y_1)
| ~ sP6(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_43,axiom,
( sP7(Eq_y_0,Eq_y_1,Eq_y_2)
| ~ sP7(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_44,axiom,
( sP8(Eq_y_0,Eq_y_1)
| ~ sP8(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_45,axiom,
( sP9(Eq_y_0,Eq_y_1)
| ~ sP9(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_46,axiom,
( sP10(Eq_y_0,Eq_y_1,Eq_y_2,Eq_y_3)
| ~ sP10(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_47,axiom,
( sP11(Eq_y_0,Eq_y_1,Eq_y_2,Eq_y_3)
| ~ sP11(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_48,axiom,
( sP12(Eq_y_0,Eq_y_1,Eq_y_2)
| ~ sP12(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_49,axiom,
( sP13(Eq_y_0,Eq_y_1)
| ~ sP13(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_50,axiom,
( sP14(Eq_y_0)
| ~ sP14(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_51,axiom,
( sP15(Eq_y_0,Eq_y_1)
| ~ sP15(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_52,axiom,
( sP16(Eq_y_0,Eq_y_1)
| ~ sP16(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_53,axiom,
( sP17(Eq_y_0,Eq_y_1,Eq_y_2,Eq_y_3)
| ~ sP17(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_54,axiom,
( sP18(Eq_y_0)
| ~ sP18(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_55,axiom,
( sP19(Eq_y_0)
| ~ sP19(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_56,axiom,
( sP20(Eq_y_0,Eq_y_1)
| ~ sP20(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_57,axiom,
( sP21(Eq_y_0)
| ~ sP21(Eq_x_0)
| 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.02 % Problem : SET094+1 : TPTP v9.3.1. Bugfixed v7.3.0.
% 0.00/0.03 This is a FOF_THM_RFO_SEQ problem
% 0.00/0.03 % Command : /export/starexec/sandbox/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.37 % Computer : n009.cluster.edu
% 0.09/0.37 % Model : x86_64 x86_64
% 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37 % Memory : 8046.5625MB
% 0.09/0.37 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Sat Sep 19 21:42:12 UTC 2026
% 0.09/0.37 % CPUTime :
% 234.14/234.42 % SZS status Theorem for theBenchmark
% 234.14/234.42 % SZS output start Proof for theBenchmark
% See solution above
%------------------------------------------------------------------------------