%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : SET024+1 : TPTP v9.2.1. Bugfixed v5.4.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox2/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox2/solver/bin/cse --final-prover /export/starexec/sandbox2/solver/bin/eprover --proof-time %d --global-time-limit %d
% Computer : n022.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue May 5 05:06:55 PM UTC 2026
% Result : Theorem 0.31s 1.62s
% Output : CNFRefutation 0.31s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named c_0_54)
% Comments :
%------------------------------------------------------------------------------
fof(image_defn,axiom,
! [X1,X6] : image(X6,X1) = range_of(restrict(X6,X1,universal_class)),
file('/export/starexec/sandbox2/benchmark/Axioms/SET005+0.ax',image_defn) ).
fof(range_of_defn,axiom,
! [X5] : range_of(X5) = domain_of(inverse(X5)),
file('/export/starexec/sandbox2/benchmark/Axioms/SET005+0.ax',range_of_defn) ).
fof(inverse_defn,axiom,
! [X2] : inverse(X2) = domain_of(flip(cross_product(X2,universal_class))),
file('/export/starexec/sandbox2/benchmark/Axioms/SET005+0.ax',inverse_defn) ).
fof(ordered_pair_defn,axiom,
! [X1,X2] : ordered_pair(X1,X2) = unordered_pair(singleton(X1),unordered_pair(X1,singleton(X2))),
file('/export/starexec/sandbox2/benchmark/Axioms/SET005+0.ax',ordered_pair_defn) ).
fof(singleton_set_defn,axiom,
! [X1] : singleton(X1) = unordered_pair(X1,X1),
file('/export/starexec/sandbox2/benchmark/Axioms/SET005+0.ax',singleton_set_defn) ).
fof(apply_defn,axiom,
! [X9,X2] : apply(X9,X2) = sum_class(image(X9,singleton(X2))),
file('/export/starexec/sandbox2/benchmark/Axioms/SET005+0.ax',apply_defn) ).
fof(successor_defn,axiom,
! [X1] : successor(X1) = union(X1,singleton(X1)),
file('/export/starexec/sandbox2/benchmark/Axioms/SET005+0.ax',successor_defn) ).
fof(set_in_its_singleton,conjecture,
! [X1] :
( member(X1,universal_class)
=> member(X1,singleton(X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',set_in_its_singleton) ).
fof(compose_defn2,axiom,
! [X6,X8,X3,X4] :
( member(ordered_pair(X3,X4),compose(X8,X6))
<=> ( member(X3,universal_class)
& member(X4,image(X8,image(X6,singleton(X3)))) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET005+0.ax',compose_defn2) ).
fof(restrict_defn,axiom,
! [X1,X6,X2] : restrict(X6,X1,X2) = intersection(X6,cross_product(X1,X2)),
file('/export/starexec/sandbox2/benchmark/Axioms/SET005+0.ax',restrict_defn) ).
fof(flip_defn,axiom,
! [X3,X4,X7,X1] :
( member(ordered_pair(ordered_pair(X3,X4),X7),flip(X1))
<=> ( member(ordered_pair(ordered_pair(X3,X4),X7),cross_product(cross_product(universal_class,universal_class),universal_class))
& member(ordered_pair(ordered_pair(X4,X3),X7),X1) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET005+0.ax',flip_defn) ).
fof(rotate_defn,axiom,
! [X1,X3,X4,X7] :
( member(ordered_pair(ordered_pair(X3,X4),X7),rotate(X1))
<=> ( member(ordered_pair(ordered_pair(X3,X4),X7),cross_product(cross_product(universal_class,universal_class),universal_class))
& member(ordered_pair(ordered_pair(X4,X7),X3),X1) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET005+0.ax',rotate_defn) ).
fof(choice,axiom,
? [X9] :
( function(X9)
& ! [X2] :
( member(X2,universal_class)
=> ( X2 = null_class
| member(apply(X9,X2),X2) ) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET005+0.ax',choice) ).
fof(inductive_defn,axiom,
! [X1] :
( inductive(X1)
<=> ( member(null_class,X1)
& subclass(image(successor_relation,X1),X1) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET005+0.ax',inductive_defn) ).
fof(replacement,axiom,
! [X1,X9] :
( ( member(X1,universal_class)
& function(X9) )
=> member(image(X9,X1),universal_class) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET005+0.ax',replacement) ).
fof(function_defn,axiom,
! [X9] :
( function(X9)
<=> ( subclass(X9,cross_product(universal_class,universal_class))
& subclass(compose(X9,inverse(X9)),identity_relation) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET005+0.ax',function_defn) ).
fof(cross_product_defn,axiom,
! [X3,X4,X1,X2] :
( member(ordered_pair(X3,X4),cross_product(X1,X2))
<=> ( member(X3,X1)
& member(X4,X2) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET005+0.ax',cross_product_defn) ).
fof(successor_relation_defn2,axiom,
! [X1,X2] :
( member(ordered_pair(X1,X2),successor_relation)
<=> ( member(X1,universal_class)
& member(X2,universal_class)
& successor(X1) = X2 ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET005+0.ax',successor_relation_defn2) ).
fof(element_relation_defn,axiom,
! [X1,X2] :
( member(ordered_pair(X1,X2),element_relation)
<=> ( member(X2,universal_class)
& member(X1,X2) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET005+0.ax',element_relation_defn) ).
fof(first_second,axiom,
! [X1,X2] :
( ( member(X1,universal_class)
& member(X2,universal_class) )
=> ( first(ordered_pair(X1,X2)) = X1
& second(ordered_pair(X1,X2)) = X2 ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET005+0.ax',first_second) ).
fof(cross_product,axiom,
! [X1,X2,X5] :
( member(X5,cross_product(X1,X2))
=> X5 = ordered_pair(first(X5),second(X5)) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET005+0.ax',cross_product) ).
fof(identity_relation,axiom,
! [X5] :
( member(X5,identity_relation)
<=> ? [X1] :
( member(X1,universal_class)
& X5 = ordered_pair(X1,X1) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET005+0.ax',identity_relation) ).
fof(domain_of,axiom,
! [X1,X5] :
( member(X5,domain_of(X1))
<=> ( member(X5,universal_class)
& restrict(X1,singleton(X5),universal_class) != null_class ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET005+0.ax',domain_of) ).
fof(complement,axiom,
! [X1,X5] :
( member(X5,complement(X1))
<=> ( member(X5,universal_class)
& ~ member(X5,X1) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET005+0.ax',complement) ).
fof(null_class_defn,axiom,
! [X1] : ~ member(X1,null_class),
file('/export/starexec/sandbox2/benchmark/Axioms/SET005+0.ax',null_class_defn) ).
fof(union_defn,axiom,
! [X1,X2,X5] :
( member(X5,union(X1,X2))
<=> ( member(X5,X1)
| member(X5,X2) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET005+0.ax',union_defn) ).
fof(intersection,axiom,
! [X1,X2,X5] :
( member(X5,intersection(X1,X2))
<=> ( member(X5,X1)
& member(X5,X2) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET005+0.ax',intersection) ).
fof(flip,axiom,
! [X1] : subclass(flip(X1),cross_product(cross_product(universal_class,universal_class),universal_class)),
file('/export/starexec/sandbox2/benchmark/Axioms/SET005+0.ax',flip) ).
fof(rotate,axiom,
! [X1] : subclass(rotate(X1),cross_product(cross_product(universal_class,universal_class),universal_class)),
file('/export/starexec/sandbox2/benchmark/Axioms/SET005+0.ax',rotate) ).
fof(subclass_defn,axiom,
! [X1,X2] :
( subclass(X1,X2)
<=> ! [X3] :
( member(X3,X1)
=> member(X3,X2) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET005+0.ax',subclass_defn) ).
fof(unordered_pair_defn,axiom,
! [X3,X1,X2] :
( member(X3,unordered_pair(X1,X2))
<=> ( member(X3,universal_class)
& ( X3 = X1
| X3 = X2 ) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET005+0.ax',unordered_pair_defn) ).
fof(sum_class_defn,axiom,
! [X3,X1] :
( member(X3,sum_class(X1))
<=> ? [X2] :
( member(X3,X2)
& member(X2,X1) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET005+0.ax',sum_class_defn) ).
fof(disjoint_defn,axiom,
! [X1,X2] :
( disjoint(X1,X2)
<=> ! [X3] :
~ ( member(X3,X1)
& member(X3,X2) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET005+0.ax',disjoint_defn) ).
fof(power_class_defn,axiom,
! [X3,X1] :
( member(X3,power_class(X1))
<=> ( member(X3,universal_class)
& subclass(X3,X1) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET005+0.ax',power_class_defn) ).
fof(compose_defn1,axiom,
! [X6,X8] : subclass(compose(X8,X6),cross_product(universal_class,universal_class)),
file('/export/starexec/sandbox2/benchmark/Axioms/SET005+0.ax',compose_defn1) ).
fof(extensionality,axiom,
! [X1,X2] :
( X1 = X2
<=> ( subclass(X1,X2)
& subclass(X2,X1) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET005+0.ax',extensionality) ).
fof(power_class,axiom,
! [X3] :
( member(X3,universal_class)
=> member(power_class(X3),universal_class) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET005+0.ax',power_class) ).
fof(sum_class,axiom,
! [X1] :
( member(X1,universal_class)
=> member(sum_class(X1),universal_class) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET005+0.ax',sum_class) ).
fof(unordered_pair,axiom,
! [X1,X2] : member(unordered_pair(X1,X2),universal_class),
file('/export/starexec/sandbox2/benchmark/Axioms/SET005+0.ax',unordered_pair) ).
fof(regularity,axiom,
! [X1] :
( X1 != null_class
=> ? [X3] :
( member(X3,universal_class)
& member(X3,X1)
& disjoint(X3,X1) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET005+0.ax',regularity) ).
fof(infinity,axiom,
? [X1] :
( member(X1,universal_class)
& inductive(X1)
& ! [X2] :
( inductive(X2)
=> subclass(X1,X2) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET005+0.ax',infinity) ).
fof(class_elements_are_sets,axiom,
! [X1] : subclass(X1,universal_class),
file('/export/starexec/sandbox2/benchmark/Axioms/SET005+0.ax',class_elements_are_sets) ).
fof(successor_relation_defn1,axiom,
subclass(successor_relation,cross_product(universal_class,universal_class)),
file('/export/starexec/sandbox2/benchmark/Axioms/SET005+0.ax',successor_relation_defn1) ).
fof(element_relation,axiom,
subclass(element_relation,cross_product(universal_class,universal_class)),
file('/export/starexec/sandbox2/benchmark/Axioms/SET005+0.ax',element_relation) ).
fof(i_0_44,plain,
! [X154,X155] : image(X155,X154) = range_of(restrict(X155,X154,universal_class)),
inference(variable_rename,[status(thm)],[image_defn]) ).
fof(i_0_45,plain,
! [X153] : range_of(X153) = domain_of(inverse(X153)),
inference(variable_rename,[status(thm)],[range_of_defn]) ).
fof(i_0_46,plain,
! [X152] : inverse(X152) = domain_of(flip(cross_product(X152,universal_class))),
inference(variable_rename,[status(thm)],[inverse_defn]) ).
fof(i_0_47,plain,
! [X112,X113] : ordered_pair(X112,X113) = unordered_pair(singleton(X112),unordered_pair(X112,singleton(X113))),
inference(variable_rename,[status(thm)],[ordered_pair_defn]) ).
fof(i_0_48,plain,
! [X111] : singleton(X111) = unordered_pair(X111,X111),
inference(variable_rename,[status(thm)],[singleton_set_defn]) ).
fof(i_0_49,plain,
! [X190,X191] : apply(X190,X191) = sum_class(image(X190,singleton(X191))),
inference(variable_rename,[status(thm)],[apply_defn]) ).
fof(i_0_50,plain,
! [X149] : successor(X149) = union(X149,singleton(X149)),
inference(variable_rename,[status(thm)],[successor_defn]) ).
fof(i_0_51,negated_conjecture,
~ ! [X1] :
( member(X1,universal_class)
=> member(X1,singleton(X1)) ),
inference(assume_negation,[status(cth)],[set_in_its_singleton]) ).
fof(i_0_52,plain,
! [X171,X172,X173,X174] :
( ( member(X173,universal_class)
| ~ member(ordered_pair(X173,X174),compose(X172,X171)) )
& ( member(X174,image(X172,image(X171,singleton(X173))))
| ~ member(ordered_pair(X173,X174),compose(X172,X171)) )
& ( ~ member(X173,universal_class)
| ~ member(X174,image(X172,image(X171,singleton(X173))))
| member(ordered_pair(X173,X174),compose(X172,X171)) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[compose_defn2])])]) ).
cnf(i_0_53,plain,
image(X1,X2) = range_of(restrict(X1,X2,universal_class)),
inference(split_conjunct,[status(thm)],[i_0_44]) ).
cnf(i_0_54,plain,
range_of(X1) = domain_of(inverse(X1)),
inference(split_conjunct,[status(thm)],[i_0_45]) ).
cnf(i_0_55,plain,
inverse(X1) = domain_of(flip(cross_product(X1,universal_class))),
inference(split_conjunct,[status(thm)],[i_0_46]) ).
fof(i_0_56,plain,
! [X130,X131,X132] : restrict(X131,X130,X132) = intersection(X131,cross_product(X130,X132)),
inference(variable_rename,[status(thm)],[restrict_defn]) ).
cnf(i_0_57,plain,
ordered_pair(X1,X2) = unordered_pair(singleton(X1),unordered_pair(X1,singleton(X2))),
inference(split_conjunct,[status(thm)],[i_0_47]) ).
cnf(i_0_58,plain,
singleton(X1) = unordered_pair(X1,X1),
inference(split_conjunct,[status(thm)],[i_0_48]) ).
fof(i_0_59,plain,
! [X141,X142,X143,X144] :
( ( member(ordered_pair(ordered_pair(X141,X142),X143),cross_product(cross_product(universal_class,universal_class),universal_class))
| ~ member(ordered_pair(ordered_pair(X141,X142),X143),flip(X144)) )
& ( member(ordered_pair(ordered_pair(X142,X141),X143),X144)
| ~ member(ordered_pair(ordered_pair(X141,X142),X143),flip(X144)) )
& ( ~ member(ordered_pair(ordered_pair(X141,X142),X143),cross_product(cross_product(universal_class,universal_class),universal_class))
| ~ member(ordered_pair(ordered_pair(X142,X141),X143),X144)
| member(ordered_pair(ordered_pair(X141,X142),X143),flip(X144)) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[flip_defn])])]) ).
fof(i_0_60,plain,
! [X136,X137,X138,X139] :
( ( member(ordered_pair(ordered_pair(X137,X138),X139),cross_product(cross_product(universal_class,universal_class),universal_class))
| ~ member(ordered_pair(ordered_pair(X137,X138),X139),rotate(X136)) )
& ( member(ordered_pair(ordered_pair(X138,X139),X137),X136)
| ~ member(ordered_pair(ordered_pair(X137,X138),X139),rotate(X136)) )
& ( ~ member(ordered_pair(ordered_pair(X137,X138),X139),cross_product(cross_product(universal_class,universal_class),universal_class))
| ~ member(ordered_pair(ordered_pair(X138,X139),X137),X136)
| member(ordered_pair(ordered_pair(X137,X138),X139),rotate(X136)) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[rotate_defn])])]) ).
fof(i_0_61,plain,
! [X193] :
( function(esk7_0)
& ( ~ member(X193,universal_class)
| X193 = null_class
| member(apply(esk7_0,X193),X193) ) ),
inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[choice])])])]) ).
cnf(i_0_62,plain,
apply(X1,X2) = sum_class(image(X1,singleton(X2))),
inference(split_conjunct,[status(thm)],[i_0_49]) ).
fof(i_0_63,plain,
! [X156] :
( ( member(null_class,X156)
| ~ inductive(X156) )
& ( subclass(image(successor_relation,X156),X156)
| ~ inductive(X156) )
& ( ~ member(null_class,X156)
| ~ subclass(image(successor_relation,X156),X156)
| inductive(X156) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inductive_defn])])]) ).
fof(i_0_64,plain,
! [X180,X181] :
( ~ member(X180,universal_class)
| ~ function(X181)
| member(image(X181,X180),universal_class) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[replacement])]) ).
fof(i_0_65,plain,
! [X179] :
( ( subclass(X179,cross_product(universal_class,universal_class))
| ~ function(X179) )
& ( subclass(compose(X179,inverse(X179)),identity_relation)
| ~ function(X179) )
& ( ~ subclass(X179,cross_product(universal_class,universal_class))
| ~ subclass(compose(X179,inverse(X179)),identity_relation)
| function(X179) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[function_defn])])]) ).
fof(i_0_66,plain,
! [X114,X115,X116,X117] :
( ( member(X114,X116)
| ~ member(ordered_pair(X114,X115),cross_product(X116,X117)) )
& ( member(X115,X117)
| ~ member(ordered_pair(X114,X115),cross_product(X116,X117)) )
& ( ~ member(X114,X116)
| ~ member(X115,X117)
| member(ordered_pair(X114,X115),cross_product(X116,X117)) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[cross_product_defn])])]) ).
fof(i_0_67,plain,
! [X150,X151] :
( ( member(X150,universal_class)
| ~ member(ordered_pair(X150,X151),successor_relation) )
& ( member(X151,universal_class)
| ~ member(ordered_pair(X150,X151),successor_relation) )
& ( successor(X150) = X151
| ~ member(ordered_pair(X150,X151),successor_relation) )
& ( ~ member(X150,universal_class)
| ~ member(X151,universal_class)
| successor(X150) != X151
| member(ordered_pair(X150,X151),successor_relation) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[successor_relation_defn2])])]) ).
cnf(i_0_68,plain,
successor(X1) = union(X1,singleton(X1)),
inference(split_conjunct,[status(thm)],[i_0_50]) ).
fof(i_0_69,plain,
! [X123,X124] :
( ( member(X124,universal_class)
| ~ member(ordered_pair(X123,X124),element_relation) )
& ( member(X123,X124)
| ~ member(ordered_pair(X123,X124),element_relation) )
& ( ~ member(X124,universal_class)
| ~ member(X123,X124)
| member(ordered_pair(X123,X124),element_relation) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[element_relation_defn])])]) ).
fof(i_0_70,plain,
! [X118,X119] :
( ( first(ordered_pair(X118,X119)) = X118
| ~ member(X118,universal_class)
| ~ member(X119,universal_class) )
& ( second(ordered_pair(X118,X119)) = X119
| ~ member(X118,universal_class)
| ~ member(X119,universal_class) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[first_second])])]) ).
fof(i_0_71,plain,
! [X120,X121,X122] :
( ~ member(X122,cross_product(X120,X121))
| X122 = ordered_pair(first(X122),second(X122)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[cross_product])]) ).
fof(i_0_72,plain,
! [X175,X177,X178] :
( ( member(esk4_1(X175),universal_class)
| ~ member(X175,identity_relation) )
& ( X175 = ordered_pair(esk4_1(X175),esk4_1(X175))
| ~ member(X175,identity_relation) )
& ( ~ member(X178,universal_class)
| X177 != ordered_pair(X178,X178)
| member(X177,identity_relation) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[identity_relation])])])])])]) ).
fof(i_0_73,plain,
! [X134,X135] :
( ( member(X135,universal_class)
| ~ member(X135,domain_of(X134)) )
& ( restrict(X134,singleton(X135),universal_class) != null_class
| ~ member(X135,domain_of(X134)) )
& ( ~ member(X135,universal_class)
| restrict(X134,singleton(X135),universal_class) = null_class
| member(X135,domain_of(X134)) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[domain_of])])]) ).
fof(i_0_74,plain,
! [X1,X5] :
( member(X5,complement(X1))
<=> ( member(X5,universal_class)
& ~ member(X5,X1) ) ),
inference(fof_simplification,[status(thm)],[complement]) ).
fof(i_0_75,negated_conjecture,
( member(esk8_0,universal_class)
& ~ member(esk8_0,singleton(esk8_0)) ),
inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_51])])]) ).
fof(i_0_76,plain,
! [X1] : ~ member(X1,null_class),
inference(fof_simplification,[status(thm)],[null_class_defn]) ).
cnf(i_0_77,plain,
( member(ordered_pair(X1,X2),compose(X3,X4))
| ~ member(X1,universal_class)
| ~ member(X2,image(X3,image(X4,singleton(X1)))) ),
inference(split_conjunct,[status(thm)],[i_0_52]) ).
cnf(i_0_78,plain,
image(X1,X2) = domain_of(domain_of(flip(cross_product(restrict(X1,X2,universal_class),universal_class)))),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_53,c_0_54]),c_0_55]) ).
cnf(i_0_79,plain,
restrict(X1,X2,X3) = intersection(X1,cross_product(X2,X3)),
inference(split_conjunct,[status(thm)],[i_0_56]) ).
cnf(i_0_80,plain,
ordered_pair(X1,X2) = unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X2,X2))),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_57,c_0_58]),c_0_58]) ).
cnf(i_0_81,plain,
( member(X1,image(X2,image(X3,singleton(X4))))
| ~ member(ordered_pair(X4,X1),compose(X2,X3)) ),
inference(split_conjunct,[status(thm)],[i_0_52]) ).
cnf(i_0_82,plain,
( member(ordered_pair(ordered_pair(X1,X2),X3),flip(X4))
| ~ member(ordered_pair(ordered_pair(X1,X2),X3),cross_product(cross_product(universal_class,universal_class),universal_class))
| ~ member(ordered_pair(ordered_pair(X2,X1),X3),X4) ),
inference(split_conjunct,[status(thm)],[i_0_59]) ).
cnf(i_0_83,plain,
( member(ordered_pair(ordered_pair(X1,X2),X3),rotate(X4))
| ~ member(ordered_pair(ordered_pair(X1,X2),X3),cross_product(cross_product(universal_class,universal_class),universal_class))
| ~ member(ordered_pair(ordered_pair(X2,X3),X1),X4) ),
inference(split_conjunct,[status(thm)],[i_0_60]) ).
cnf(i_0_84,plain,
( member(ordered_pair(ordered_pair(X1,X2),X3),cross_product(cross_product(universal_class,universal_class),universal_class))
| ~ member(ordered_pair(ordered_pair(X1,X2),X3),flip(X4)) ),
inference(split_conjunct,[status(thm)],[i_0_59]) ).
cnf(i_0_85,plain,
( member(ordered_pair(ordered_pair(X1,X2),X3),cross_product(cross_product(universal_class,universal_class),universal_class))
| ~ member(ordered_pair(ordered_pair(X1,X2),X3),rotate(X4)) ),
inference(split_conjunct,[status(thm)],[i_0_60]) ).
cnf(i_0_86,plain,
( member(ordered_pair(ordered_pair(X1,X2),X3),X4)
| ~ member(ordered_pair(ordered_pair(X2,X1),X3),flip(X4)) ),
inference(split_conjunct,[status(thm)],[i_0_59]) ).
cnf(i_0_87,plain,
( member(ordered_pair(ordered_pair(X1,X2),X3),X4)
| ~ member(ordered_pair(ordered_pair(X3,X1),X2),rotate(X4)) ),
inference(split_conjunct,[status(thm)],[i_0_60]) ).
cnf(i_0_88,plain,
( X1 = null_class
| member(apply(esk7_0,X1),X1)
| ~ member(X1,universal_class) ),
inference(split_conjunct,[status(thm)],[i_0_61]) ).
cnf(i_0_89,plain,
apply(X1,X2) = sum_class(image(X1,unordered_pair(X2,X2))),
inference(rw,[status(thm)],[i_0_62,c_0_58]) ).
cnf(i_0_90,plain,
( inductive(X1)
| ~ member(null_class,X1)
| ~ subclass(image(successor_relation,X1),X1) ),
inference(split_conjunct,[status(thm)],[i_0_63]) ).
cnf(i_0_91,plain,
( member(image(X2,X1),universal_class)
| ~ member(X1,universal_class)
| ~ function(X2) ),
inference(split_conjunct,[status(thm)],[i_0_64]) ).
cnf(i_0_92,plain,
( subclass(image(successor_relation,X1),X1)
| ~ inductive(X1) ),
inference(split_conjunct,[status(thm)],[i_0_63]) ).
cnf(i_0_93,plain,
( function(X1)
| ~ subclass(X1,cross_product(universal_class,universal_class))
| ~ subclass(compose(X1,inverse(X1)),identity_relation) ),
inference(split_conjunct,[status(thm)],[i_0_65]) ).
cnf(i_0_94,plain,
( member(X1,X2)
| ~ member(ordered_pair(X1,X3),cross_product(X2,X4)) ),
inference(split_conjunct,[status(thm)],[i_0_66]) ).
cnf(i_0_95,plain,
( member(X1,X2)
| ~ member(ordered_pair(X3,X1),cross_product(X4,X2)) ),
inference(split_conjunct,[status(thm)],[i_0_66]) ).
cnf(i_0_96,plain,
( member(X1,universal_class)
| ~ member(ordered_pair(X1,X2),compose(X3,X4)) ),
inference(split_conjunct,[status(thm)],[i_0_52]) ).
cnf(i_0_97,plain,
( successor(X1) = X2
| ~ member(ordered_pair(X1,X2),successor_relation) ),
inference(split_conjunct,[status(thm)],[i_0_67]) ).
cnf(i_0_98,plain,
successor(X1) = union(X1,unordered_pair(X1,X1)),
inference(rw,[status(thm)],[i_0_68,c_0_58]) ).
cnf(i_0_99,plain,
( member(X1,X2)
| ~ member(ordered_pair(X1,X2),element_relation) ),
inference(split_conjunct,[status(thm)],[i_0_69]) ).
cnf(i_0_100,plain,
( member(X1,universal_class)
| ~ member(ordered_pair(X1,X2),successor_relation) ),
inference(split_conjunct,[status(thm)],[i_0_67]) ).
cnf(i_0_101,plain,
( member(X1,universal_class)
| ~ member(ordered_pair(X2,X1),successor_relation) ),
inference(split_conjunct,[status(thm)],[i_0_67]) ).
cnf(i_0_102,plain,
( member(X1,universal_class)
| ~ member(ordered_pair(X2,X1),element_relation) ),
inference(split_conjunct,[status(thm)],[i_0_69]) ).
cnf(i_0_103,plain,
( member(ordered_pair(X1,X2),successor_relation)
| ~ member(X1,universal_class)
| ~ member(X2,universal_class)
| successor(X1) != X2 ),
inference(split_conjunct,[status(thm)],[i_0_67]) ).
cnf(i_0_104,plain,
( member(ordered_pair(X1,X3),cross_product(X2,X4))
| ~ member(X1,X2)
| ~ member(X3,X4) ),
inference(split_conjunct,[status(thm)],[i_0_66]) ).
cnf(i_0_105,plain,
( member(ordered_pair(X2,X1),element_relation)
| ~ member(X1,universal_class)
| ~ member(X2,X1) ),
inference(split_conjunct,[status(thm)],[i_0_69]) ).
cnf(i_0_106,plain,
( second(ordered_pair(X1,X2)) = X2
| ~ member(X1,universal_class)
| ~ member(X2,universal_class) ),
inference(split_conjunct,[status(thm)],[i_0_70]) ).
cnf(i_0_107,plain,
( first(ordered_pair(X1,X2)) = X1
| ~ member(X1,universal_class)
| ~ member(X2,universal_class) ),
inference(split_conjunct,[status(thm)],[i_0_70]) ).
cnf(i_0_108,plain,
( X1 = ordered_pair(first(X1),second(X1))
| ~ member(X1,cross_product(X2,X3)) ),
inference(split_conjunct,[status(thm)],[i_0_71]) ).
cnf(i_0_109,plain,
( subclass(compose(X1,inverse(X1)),identity_relation)
| ~ function(X1) ),
inference(split_conjunct,[status(thm)],[i_0_65]) ).
cnf(i_0_110,plain,
( X1 = ordered_pair(esk4_1(X1),esk4_1(X1))
| ~ member(X1,identity_relation) ),
inference(split_conjunct,[status(thm)],[i_0_72]) ).
cnf(i_0_111,plain,
( member(X2,identity_relation)
| ~ member(X1,universal_class)
| X2 != ordered_pair(X1,X1) ),
inference(split_conjunct,[status(thm)],[i_0_72]) ).
cnf(i_0_112,plain,
( restrict(X1,singleton(X2),universal_class) != null_class
| ~ member(X2,domain_of(X1)) ),
inference(split_conjunct,[status(thm)],[i_0_73]) ).
cnf(i_0_113,plain,
( restrict(X2,singleton(X1),universal_class) = null_class
| member(X1,domain_of(X2))
| ~ member(X1,universal_class) ),
inference(split_conjunct,[status(thm)],[i_0_73]) ).
fof(i_0_114,plain,
! [X146,X147,X148] :
( ( ~ member(X148,union(X146,X147))
| member(X148,X146)
| member(X148,X147) )
& ( ~ member(X148,X146)
| member(X148,union(X146,X147)) )
& ( ~ member(X148,X147)
| member(X148,union(X146,X147)) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[union_defn])])]) ).
fof(i_0_115,plain,
! [X125,X126,X127] :
( ( member(X127,X125)
| ~ member(X127,intersection(X125,X126)) )
& ( member(X127,X126)
| ~ member(X127,intersection(X125,X126)) )
& ( ~ member(X127,X125)
| ~ member(X127,X126)
| member(X127,intersection(X125,X126)) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[intersection])])]) ).
fof(i_0_116,plain,
! [X145] : subclass(flip(X145),cross_product(cross_product(universal_class,universal_class),universal_class)),
inference(variable_rename,[status(thm)],[flip]) ).
fof(i_0_117,plain,
! [X140] : subclass(rotate(X140),cross_product(cross_product(universal_class,universal_class),universal_class)),
inference(variable_rename,[status(thm)],[rotate]) ).
fof(i_0_118,plain,
! [X97,X98,X99,X100,X101] :
( ( ~ subclass(X97,X98)
| ~ member(X99,X97)
| member(X99,X98) )
& ( member(esk1_2(X100,X101),X100)
| subclass(X100,X101) )
& ( ~ member(esk1_2(X100,X101),X101)
| subclass(X100,X101) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[subclass_defn])])])])])]) ).
fof(i_0_119,plain,
! [X106,X107,X108] :
( ( member(X106,universal_class)
| ~ member(X106,unordered_pair(X107,X108)) )
& ( X106 = X107
| X106 = X108
| ~ member(X106,unordered_pair(X107,X108)) )
& ( X106 != X107
| ~ member(X106,universal_class)
| member(X106,unordered_pair(X107,X108)) )
& ( X106 != X108
| ~ member(X106,universal_class)
| member(X106,unordered_pair(X107,X108)) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[unordered_pair_defn])])]) ).
fof(i_0_120,plain,
! [X159,X160,X162,X163,X164] :
( ( member(X159,esk3_2(X159,X160))
| ~ member(X159,sum_class(X160)) )
& ( member(esk3_2(X159,X160),X160)
| ~ member(X159,sum_class(X160)) )
& ( ~ member(X162,X164)
| ~ member(X164,X163)
| member(X162,sum_class(X163)) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[sum_class_defn])])])])])]) ).
fof(i_0_121,plain,
! [X182,X183,X184,X185,X186] :
( ( ~ disjoint(X182,X183)
| ~ member(X184,X182)
| ~ member(X184,X183) )
& ( member(esk5_2(X185,X186),X185)
| disjoint(X185,X186) )
& ( member(esk5_2(X185,X186),X186)
| disjoint(X185,X186) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[disjoint_defn])])])])])]) ).
fof(i_0_122,plain,
! [X166,X167] :
( ( member(X166,universal_class)
| ~ member(X166,power_class(X167)) )
& ( subclass(X166,X167)
| ~ member(X166,power_class(X167)) )
& ( ~ member(X166,universal_class)
| ~ subclass(X166,X167)
| member(X166,power_class(X167)) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[power_class_defn])])]) ).
fof(i_0_123,plain,
! [X169,X170] : subclass(compose(X170,X169),cross_product(universal_class,universal_class)),
inference(variable_rename,[status(thm)],[compose_defn1]) ).
fof(i_0_124,plain,
! [X128,X129] :
( ( member(X129,universal_class)
| ~ member(X129,complement(X128)) )
& ( ~ member(X129,X128)
| ~ member(X129,complement(X128)) )
& ( ~ member(X129,universal_class)
| member(X129,X128)
| member(X129,complement(X128)) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_74])])]) ).
cnf(i_0_125,negated_conjecture,
~ member(esk8_0,singleton(esk8_0)),
inference(split_conjunct,[status(thm)],[i_0_75]) ).
fof(i_0_126,plain,
! [X104,X105] :
( ( subclass(X104,X105)
| X104 != X105 )
& ( subclass(X105,X104)
| X104 != X105 )
& ( ~ subclass(X104,X105)
| ~ subclass(X105,X104)
| X104 = X105 ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[extensionality])])]) ).
fof(i_0_127,plain,
! [X168] :
( ~ member(X168,universal_class)
| member(power_class(X168),universal_class) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[power_class])]) ).
fof(i_0_128,plain,
! [X165] :
( ~ member(X165,universal_class)
| member(sum_class(X165),universal_class) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[sum_class])]) ).
fof(i_0_129,plain,
! [X109,X110] : member(unordered_pair(X109,X110),universal_class),
inference(variable_rename,[status(thm)],[unordered_pair]) ).
fof(i_0_130,plain,
! [X188] :
( ( member(esk6_1(X188),universal_class)
| X188 = null_class )
& ( member(esk6_1(X188),X188)
| X188 = null_class )
& ( disjoint(esk6_1(X188),X188)
| X188 = null_class ) ),
inference(distribute,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[regularity])])])]) ).
fof(i_0_131,plain,
! [X133] : ~ member(X133,null_class),
inference(variable_rename,[status(thm)],[i_0_76]) ).
fof(i_0_132,plain,
! [X158] :
( member(esk2_0,universal_class)
& inductive(esk2_0)
& ( ~ inductive(X158)
| subclass(esk2_0,X158) ) ),
inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[infinity])])])]) ).
fof(i_0_133,plain,
! [X103] : subclass(X103,universal_class),
inference(variable_rename,[status(thm)],[class_elements_are_sets]) ).
cnf(i_0_134,plain,
( member(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X2,X2))),compose(X3,X4))
| ~ member(X1,universal_class)
| ~ member(X2,domain_of(domain_of(flip(cross_product(intersection(X3,cross_product(domain_of(domain_of(flip(cross_product(intersection(X4,cross_product(unordered_pair(X1,X1),universal_class)),universal_class)))),universal_class)),universal_class))))) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_77,c_0_58]),c_0_78]),c_0_78]),c_0_79]),c_0_79]),c_0_80]),
[final] ).
cnf(i_0_135,plain,
( member(X1,domain_of(domain_of(flip(cross_product(intersection(X2,cross_product(domain_of(domain_of(flip(cross_product(intersection(X3,cross_product(unordered_pair(X4,X4),universal_class)),universal_class)))),universal_class)),universal_class)))))
| ~ member(unordered_pair(unordered_pair(X4,X4),unordered_pair(X4,unordered_pair(X1,X1))),compose(X2,X3)) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_81,c_0_58]),c_0_78]),c_0_78]),c_0_79]),c_0_79]),c_0_80]),
[final] ).
cnf(i_0_136,plain,
( member(unordered_pair(unordered_pair(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X2,X2))),unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X2,X2)))),unordered_pair(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X2,X2))),unordered_pair(X3,X3))),flip(X4))
| ~ member(unordered_pair(unordered_pair(unordered_pair(unordered_pair(X2,X2),unordered_pair(X2,unordered_pair(X1,X1))),unordered_pair(unordered_pair(X2,X2),unordered_pair(X2,unordered_pair(X1,X1)))),unordered_pair(unordered_pair(unordered_pair(X2,X2),unordered_pair(X2,unordered_pair(X1,X1))),unordered_pair(X3,X3))),X4)
| ~ member(unordered_pair(unordered_pair(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X2,X2))),unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X2,X2)))),unordered_pair(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X2,X2))),unordered_pair(X3,X3))),cross_product(cross_product(universal_class,universal_class),universal_class)) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_82,c_0_80]),c_0_80]),c_0_80]),c_0_80]),c_0_80]),c_0_80]),
[final] ).
cnf(i_0_137,plain,
( member(unordered_pair(unordered_pair(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X2,X2))),unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X2,X2)))),unordered_pair(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X2,X2))),unordered_pair(X3,X3))),rotate(X4))
| ~ member(unordered_pair(unordered_pair(unordered_pair(unordered_pair(X2,X2),unordered_pair(X2,unordered_pair(X3,X3))),unordered_pair(unordered_pair(X2,X2),unordered_pair(X2,unordered_pair(X3,X3)))),unordered_pair(unordered_pair(unordered_pair(X2,X2),unordered_pair(X2,unordered_pair(X3,X3))),unordered_pair(X1,X1))),X4)
| ~ member(unordered_pair(unordered_pair(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X2,X2))),unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X2,X2)))),unordered_pair(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X2,X2))),unordered_pair(X3,X3))),cross_product(cross_product(universal_class,universal_class),universal_class)) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_83,c_0_80]),c_0_80]),c_0_80]),c_0_80]),c_0_80]),c_0_80]),
[final] ).
cnf(i_0_138,plain,
( member(unordered_pair(unordered_pair(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X2,X2))),unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X2,X2)))),unordered_pair(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X2,X2))),unordered_pair(X3,X3))),cross_product(cross_product(universal_class,universal_class),universal_class))
| ~ member(unordered_pair(unordered_pair(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X2,X2))),unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X2,X2)))),unordered_pair(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X2,X2))),unordered_pair(X3,X3))),flip(X4)) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_84,c_0_80]),c_0_80]),c_0_80]),c_0_80]),
[final] ).
cnf(i_0_139,plain,
( member(unordered_pair(unordered_pair(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X2,X2))),unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X2,X2)))),unordered_pair(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X2,X2))),unordered_pair(X3,X3))),cross_product(cross_product(universal_class,universal_class),universal_class))
| ~ member(unordered_pair(unordered_pair(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X2,X2))),unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X2,X2)))),unordered_pair(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X2,X2))),unordered_pair(X3,X3))),rotate(X4)) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_85,c_0_80]),c_0_80]),c_0_80]),c_0_80]),
[final] ).
cnf(i_0_140,plain,
( member(unordered_pair(unordered_pair(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X2,X2))),unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X2,X2)))),unordered_pair(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X2,X2))),unordered_pair(X3,X3))),X4)
| ~ member(unordered_pair(unordered_pair(unordered_pair(unordered_pair(X2,X2),unordered_pair(X2,unordered_pair(X1,X1))),unordered_pair(unordered_pair(X2,X2),unordered_pair(X2,unordered_pair(X1,X1)))),unordered_pair(unordered_pair(unordered_pair(X2,X2),unordered_pair(X2,unordered_pair(X1,X1))),unordered_pair(X3,X3))),flip(X4)) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_86,c_0_80]),c_0_80]),c_0_80]),c_0_80]),
[final] ).
cnf(i_0_141,plain,
( member(unordered_pair(unordered_pair(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X2,X2))),unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X2,X2)))),unordered_pair(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X2,X2))),unordered_pair(X3,X3))),X4)
| ~ member(unordered_pair(unordered_pair(unordered_pair(unordered_pair(X3,X3),unordered_pair(X3,unordered_pair(X1,X1))),unordered_pair(unordered_pair(X3,X3),unordered_pair(X3,unordered_pair(X1,X1)))),unordered_pair(unordered_pair(unordered_pair(X3,X3),unordered_pair(X3,unordered_pair(X1,X1))),unordered_pair(X2,X2))),rotate(X4)) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_87,c_0_80]),c_0_80]),c_0_80]),c_0_80]),
[final] ).
cnf(i_0_142,plain,
( X1 = null_class
| member(sum_class(domain_of(domain_of(flip(cross_product(intersection(esk7_0,cross_product(unordered_pair(X1,X1),universal_class)),universal_class))))),X1)
| ~ member(X1,universal_class) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_88,c_0_89]),c_0_78]),c_0_79]),
[final] ).
cnf(i_0_143,plain,
( inductive(X1)
| ~ member(null_class,X1)
| ~ subclass(domain_of(domain_of(flip(cross_product(intersection(successor_relation,cross_product(X1,universal_class)),universal_class)))),X1) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_90,c_0_78]),c_0_79]),
[final] ).
cnf(i_0_144,plain,
( member(domain_of(domain_of(flip(cross_product(intersection(X2,cross_product(X1,universal_class)),universal_class)))),universal_class)
| ~ function(X2)
| ~ member(X1,universal_class) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_91,c_0_78]),c_0_79]),
[final] ).
cnf(i_0_145,plain,
( subclass(domain_of(domain_of(flip(cross_product(intersection(successor_relation,cross_product(X1,universal_class)),universal_class)))),X1)
| ~ inductive(X1) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_92,c_0_78]),c_0_79]),
[final] ).
cnf(i_0_146,plain,
( function(X1)
| ~ subclass(X1,cross_product(universal_class,universal_class))
| ~ subclass(compose(X1,domain_of(flip(cross_product(X1,universal_class)))),identity_relation) ),
inference(rw,[status(thm)],[i_0_93,c_0_55]),
[final] ).
cnf(i_0_147,plain,
( member(X1,X2)
| ~ member(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X3,X3))),cross_product(X2,X4)) ),
inference(rw,[status(thm)],[i_0_94,c_0_80]),
[final] ).
cnf(i_0_148,plain,
( member(X1,X2)
| ~ member(unordered_pair(unordered_pair(X3,X3),unordered_pair(X3,unordered_pair(X1,X1))),cross_product(X4,X2)) ),
inference(rw,[status(thm)],[i_0_95,c_0_80]),
[final] ).
cnf(i_0_149,plain,
( member(X1,universal_class)
| ~ member(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X2,X2))),compose(X3,X4)) ),
inference(rw,[status(thm)],[i_0_96,c_0_80]),
[final] ).
cnf(i_0_150,plain,
( union(X1,unordered_pair(X1,X1)) = X2
| ~ member(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X2,X2))),successor_relation) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_97,c_0_98]),c_0_80]),
[final] ).
cnf(i_0_151,plain,
( member(X1,X2)
| ~ member(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X2,X2))),element_relation) ),
inference(rw,[status(thm)],[i_0_99,c_0_80]),
[final] ).
cnf(i_0_152,plain,
( member(X1,universal_class)
| ~ member(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X2,X2))),successor_relation) ),
inference(rw,[status(thm)],[i_0_100,c_0_80]),
[final] ).
cnf(i_0_153,plain,
( member(X1,universal_class)
| ~ member(unordered_pair(unordered_pair(X2,X2),unordered_pair(X2,unordered_pair(X1,X1))),successor_relation) ),
inference(rw,[status(thm)],[i_0_101,c_0_80]),
[final] ).
cnf(i_0_154,plain,
( member(X1,universal_class)
| ~ member(unordered_pair(unordered_pair(X2,X2),unordered_pair(X2,unordered_pair(X1,X1))),element_relation) ),
inference(rw,[status(thm)],[i_0_102,c_0_80]),
[final] ).
cnf(i_0_155,plain,
( member(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X2,X2))),successor_relation)
| union(X1,unordered_pair(X1,X1)) != X2
| ~ member(X2,universal_class)
| ~ member(X1,universal_class) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_103,c_0_98]),c_0_80]),
[final] ).
cnf(i_0_156,plain,
( member(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X3,X3))),cross_product(X2,X4))
| ~ member(X3,X4)
| ~ member(X1,X2) ),
inference(rw,[status(thm)],[i_0_104,c_0_80]),
[final] ).
cnf(i_0_157,plain,
( member(unordered_pair(unordered_pair(X2,X2),unordered_pair(X2,unordered_pair(X1,X1))),element_relation)
| ~ member(X2,X1)
| ~ member(X1,universal_class) ),
inference(rw,[status(thm)],[i_0_105,c_0_80]),
[final] ).
cnf(i_0_158,plain,
( second(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X2,X2)))) = X2
| ~ member(X2,universal_class)
| ~ member(X1,universal_class) ),
inference(rw,[status(thm)],[i_0_106,c_0_80]),
[final] ).
cnf(i_0_159,plain,
( first(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X2,X2)))) = X1
| ~ member(X2,universal_class)
| ~ member(X1,universal_class) ),
inference(rw,[status(thm)],[i_0_107,c_0_80]),
[final] ).
cnf(i_0_160,plain,
( X1 = unordered_pair(unordered_pair(first(X1),first(X1)),unordered_pair(first(X1),unordered_pair(second(X1),second(X1))))
| ~ member(X1,cross_product(X2,X3)) ),
inference(rw,[status(thm)],[i_0_108,c_0_80]),
[final] ).
cnf(i_0_161,plain,
( subclass(compose(X1,domain_of(flip(cross_product(X1,universal_class)))),identity_relation)
| ~ function(X1) ),
inference(rw,[status(thm)],[i_0_109,c_0_55]),
[final] ).
cnf(i_0_162,plain,
( X1 = unordered_pair(unordered_pair(esk4_1(X1),esk4_1(X1)),unordered_pair(esk4_1(X1),unordered_pair(esk4_1(X1),esk4_1(X1))))
| ~ member(X1,identity_relation) ),
inference(rw,[status(thm)],[i_0_110,c_0_80]),
[final] ).
cnf(i_0_163,plain,
( member(X2,identity_relation)
| X2 != unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X1,X1)))
| ~ member(X1,universal_class) ),
inference(rw,[status(thm)],[i_0_111,c_0_80]),
[final] ).
cnf(i_0_164,plain,
( intersection(X1,cross_product(unordered_pair(X2,X2),universal_class)) != null_class
| ~ member(X2,domain_of(X1)) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_112,c_0_58]),c_0_79]),
[final] ).
cnf(i_0_165,plain,
( intersection(X2,cross_product(unordered_pair(X1,X1),universal_class)) = null_class
| member(X1,domain_of(X2))
| ~ member(X1,universal_class) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_113,c_0_58]),c_0_79]),
[final] ).
cnf(i_0_166,plain,
( member(X1,X2)
| member(X1,X3)
| ~ member(X1,union(X2,X3)) ),
inference(split_conjunct,[status(thm)],[i_0_114]),
[final] ).
cnf(i_0_167,plain,
( member(X1,intersection(X2,X3))
| ~ member(X1,X2)
| ~ member(X1,X3) ),
inference(split_conjunct,[status(thm)],[i_0_115]),
[final] ).
cnf(i_0_168,plain,
subclass(flip(X1),cross_product(cross_product(universal_class,universal_class),universal_class)),
inference(split_conjunct,[status(thm)],[i_0_116]),
[final] ).
cnf(i_0_169,plain,
subclass(rotate(X1),cross_product(cross_product(universal_class,universal_class),universal_class)),
inference(split_conjunct,[status(thm)],[i_0_117]),
[final] ).
cnf(i_0_170,plain,
( subclass(X1,X2)
| ~ member(esk1_2(X1,X2),X2) ),
inference(split_conjunct,[status(thm)],[i_0_118]),
[final] ).
cnf(i_0_171,plain,
( member(X1,X2)
| ~ member(X1,intersection(X2,X3)) ),
inference(split_conjunct,[status(thm)],[i_0_115]),
[final] ).
cnf(i_0_172,plain,
( member(X1,X2)
| ~ member(X1,intersection(X3,X2)) ),
inference(split_conjunct,[status(thm)],[i_0_115]),
[final] ).
cnf(i_0_173,plain,
( member(X1,universal_class)
| ~ member(X1,unordered_pair(X2,X3)) ),
inference(split_conjunct,[status(thm)],[i_0_119]),
[final] ).
cnf(i_0_174,plain,
( member(esk3_2(X1,X2),X2)
| ~ member(X1,sum_class(X2)) ),
inference(split_conjunct,[status(thm)],[i_0_120]),
[final] ).
cnf(i_0_175,plain,
( member(X1,esk3_2(X1,X2))
| ~ member(X1,sum_class(X2)) ),
inference(split_conjunct,[status(thm)],[i_0_120]),
[final] ).
cnf(i_0_176,plain,
( ~ disjoint(X1,X2)
| ~ member(X3,X1)
| ~ member(X3,X2) ),
inference(split_conjunct,[status(thm)],[i_0_121]),
[final] ).
cnf(i_0_177,plain,
( X1 = X2
| X1 = X3
| ~ member(X1,unordered_pair(X2,X3)) ),
inference(split_conjunct,[status(thm)],[i_0_119]),
[final] ).
cnf(i_0_178,plain,
( member(X1,sum_class(X3))
| ~ member(X1,X2)
| ~ member(X2,X3) ),
inference(split_conjunct,[status(thm)],[i_0_120]),
[final] ).
cnf(i_0_179,plain,
( member(X1,unordered_pair(X2,X3))
| X1 != X2
| ~ member(X1,universal_class) ),
inference(split_conjunct,[status(thm)],[i_0_119]),
[final] ).
cnf(i_0_180,plain,
( member(X1,unordered_pair(X3,X2))
| X1 != X2
| ~ member(X1,universal_class) ),
inference(split_conjunct,[status(thm)],[i_0_119]),
[final] ).
cnf(i_0_181,plain,
( member(X1,power_class(X2))
| ~ member(X1,universal_class)
| ~ subclass(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_122]),
[final] ).
cnf(i_0_182,plain,
( member(X1,union(X2,X3))
| ~ member(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_114]),
[final] ).
cnf(i_0_183,plain,
( member(X1,union(X3,X2))
| ~ member(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_114]),
[final] ).
cnf(i_0_184,plain,
subclass(compose(X1,X2),cross_product(universal_class,universal_class)),
inference(split_conjunct,[status(thm)],[i_0_123]),
[final] ).
cnf(i_0_185,plain,
( member(X3,X2)
| ~ subclass(X1,X2)
| ~ member(X3,X1) ),
inference(split_conjunct,[status(thm)],[i_0_118]),
[final] ).
cnf(i_0_186,plain,
( member(X1,X2)
| member(X1,complement(X2))
| ~ member(X1,universal_class) ),
inference(split_conjunct,[status(thm)],[i_0_124]),
[final] ).
cnf(i_0_187,plain,
( ~ member(X1,X2)
| ~ member(X1,complement(X2)) ),
inference(split_conjunct,[status(thm)],[i_0_124]),
[final] ).
cnf(i_0_188,plain,
( member(esk5_2(X1,X2),X1)
| disjoint(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_121]),
[final] ).
cnf(i_0_189,plain,
( member(esk5_2(X1,X2),X2)
| disjoint(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_121]),
[final] ).
cnf(i_0_190,plain,
( member(esk1_2(X1,X2),X1)
| subclass(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_118]),
[final] ).
cnf(i_0_191,negated_conjecture,
~ member(esk8_0,unordered_pair(esk8_0,esk8_0)),
inference(rw,[status(thm)],[i_0_125,c_0_58]),
[final] ).
cnf(i_0_192,plain,
( X1 = X2
| ~ subclass(X1,X2)
| ~ subclass(X2,X1) ),
inference(split_conjunct,[status(thm)],[i_0_126]),
[final] ).
cnf(i_0_193,plain,
( subclass(X1,X2)
| ~ member(X1,power_class(X2)) ),
inference(split_conjunct,[status(thm)],[i_0_122]),
[final] ).
cnf(i_0_194,plain,
( member(X1,universal_class)
| ~ member(X1,power_class(X2)) ),
inference(split_conjunct,[status(thm)],[i_0_122]),
[final] ).
cnf(i_0_195,plain,
( member(X1,universal_class)
| ~ member(X1,domain_of(X2)) ),
inference(split_conjunct,[status(thm)],[i_0_73]),
[final] ).
cnf(i_0_196,plain,
( member(X1,universal_class)
| ~ member(X1,complement(X2)) ),
inference(split_conjunct,[status(thm)],[i_0_124]),
[final] ).
cnf(i_0_197,plain,
( subclass(X1,cross_product(universal_class,universal_class))
| ~ function(X1) ),
inference(split_conjunct,[status(thm)],[i_0_65]),
[final] ).
cnf(i_0_198,plain,
( member(esk4_1(X1),universal_class)
| ~ member(X1,identity_relation) ),
inference(split_conjunct,[status(thm)],[i_0_72]),
[final] ).
cnf(i_0_199,plain,
( member(power_class(X1),universal_class)
| ~ member(X1,universal_class) ),
inference(split_conjunct,[status(thm)],[i_0_127]),
[final] ).
cnf(i_0_200,plain,
( member(sum_class(X1),universal_class)
| ~ member(X1,universal_class) ),
inference(split_conjunct,[status(thm)],[i_0_128]),
[final] ).
cnf(i_0_201,plain,
member(unordered_pair(X1,X2),universal_class),
inference(split_conjunct,[status(thm)],[i_0_129]),
[final] ).
cnf(i_0_202,plain,
subclass(successor_relation,cross_product(universal_class,universal_class)),
inference(split_conjunct,[status(thm)],[successor_relation_defn1]),
[final] ).
cnf(i_0_203,plain,
subclass(element_relation,cross_product(universal_class,universal_class)),
inference(split_conjunct,[status(thm)],[element_relation]),
[final] ).
cnf(i_0_204,plain,
( disjoint(esk6_1(X1),X1)
| X1 = null_class ),
inference(split_conjunct,[status(thm)],[i_0_130]),
[final] ).
cnf(i_0_205,plain,
( member(esk6_1(X1),X1)
| X1 = null_class ),
inference(split_conjunct,[status(thm)],[i_0_130]),
[final] ).
cnf(i_0_206,plain,
( member(esk6_1(X1),universal_class)
| X1 = null_class ),
inference(split_conjunct,[status(thm)],[i_0_130]),
[final] ).
cnf(i_0_207,plain,
~ member(X1,null_class),
inference(split_conjunct,[status(thm)],[i_0_131]),
[final] ).
cnf(i_0_208,plain,
( member(null_class,X1)
| ~ inductive(X1) ),
inference(split_conjunct,[status(thm)],[i_0_63]),
[final] ).
cnf(i_0_209,plain,
( subclass(esk2_0,X1)
| ~ inductive(X1) ),
inference(split_conjunct,[status(thm)],[i_0_132]),
[final] ).
cnf(i_0_210,plain,
( subclass(X1,X2)
| X1 != X2 ),
inference(split_conjunct,[status(thm)],[i_0_126]),
[final] ).
cnf(i_0_211,plain,
( subclass(X1,X2)
| X2 != X1 ),
inference(split_conjunct,[status(thm)],[i_0_126]),
[final] ).
cnf(i_0_212,plain,
subclass(X1,universal_class),
inference(split_conjunct,[status(thm)],[i_0_133]),
[final] ).
cnf(i_0_213,negated_conjecture,
member(esk8_0,universal_class),
inference(split_conjunct,[status(thm)],[i_0_75]),
[final] ).
cnf(i_0_214,plain,
member(esk2_0,universal_class),
inference(split_conjunct,[status(thm)],[i_0_132]),
[final] ).
cnf(i_0_215,plain,
function(esk7_0),
inference(split_conjunct,[status(thm)],[i_0_61]),
[final] ).
cnf(i_0_216,plain,
inductive(esk2_0),
inference(split_conjunct,[status(thm)],[i_0_132]),
[final] ).
cnf(i_0_217,axiom,
X1 = X1 ).
cnf(i_0_218,axiom,
( X1 = X2
| X2 != X1 ) ).
cnf(i_0_219,axiom,
( X1 = X2
| X1 != X3
| X3 != X2 ) ).
cnf(i_0_220,axiom,
( X1 != X2
| unordered_pair(X1,X3) = unordered_pair(X2,X3) ) ).
cnf(i_0_221,axiom,
( X1 != X2
| unordered_pair(X3,X1) = unordered_pair(X3,X2) ) ).
cnf(i_0_222,axiom,
( X1 != X2
| second(X1) = second(X2) ) ).
cnf(i_0_223,axiom,
( X1 != X2
| first(X1) = first(X2) ) ).
cnf(i_0_224,axiom,
( X1 != X2
| intersection(X1,X3) = intersection(X2,X3) ) ).
cnf(i_0_225,axiom,
( X1 != X2
| intersection(X3,X1) = intersection(X3,X2) ) ).
cnf(i_0_226,axiom,
( X1 != X2
| union(X1,X3) = union(X2,X3) ) ).
cnf(i_0_227,axiom,
( X1 != X2
| union(X3,X1) = union(X3,X2) ) ).
cnf(i_0_228,axiom,
( X1 != X2
| ~ member(X1,X3)
| member(X2,X3) ) ).
cnf(i_0_229,axiom,
( X1 != X2
| ~ member(X3,X1)
| member(X3,X2) ) ).
cnf(i_0_230,axiom,
( X1 != X2
| ~ inductive(X1)
| inductive(X2) ) ).
cnf(i_0_231,axiom,
( X1 != X2
| ~ subclass(X1,X3)
| subclass(X2,X3) ) ).
cnf(i_0_232,axiom,
( X1 != X2
| ~ subclass(X3,X1)
| subclass(X3,X2) ) ).
cnf(i_0_233,axiom,
( X1 != X2
| ~ function(X1)
| function(X2) ) ).
cnf(i_0_234,axiom,
( X1 != X2
| ~ disjoint(X1,X3)
| disjoint(X2,X3) ) ).
cnf(i_0_235,axiom,
( X1 != X2
| ~ disjoint(X3,X1)
| disjoint(X3,X2) ) ).
cnf(i_0_217_001,axiom,
X1 = X1 ).
cnf(i_0_218_002,axiom,
( X1 = X2
| X2 != X1 ) ).
cnf(i_0_219_003,axiom,
( X1 = X2
| X1 != X3
| X3 != X2 ) ).
cnf(i_0_220_004,axiom,
( X1 != X2
| unordered_pair(X1,X3) = unordered_pair(X2,X3) ) ).
cnf(i_0_221_005,axiom,
( X1 != X2
| unordered_pair(X3,X1) = unordered_pair(X3,X2) ) ).
cnf(i_0_222_006,axiom,
( X1 != X2
| second(X1) = second(X2) ) ).
cnf(i_0_223_007,axiom,
( X1 != X2
| first(X1) = first(X2) ) ).
cnf(i_0_224_008,axiom,
( X1 != X2
| intersection(X1,X3) = intersection(X2,X3) ) ).
cnf(i_0_225_009,axiom,
( X1 != X2
| intersection(X3,X1) = intersection(X3,X2) ) ).
cnf(i_0_226_010,axiom,
( X1 != X2
| union(X1,X3) = union(X2,X3) ) ).
cnf(i_0_227_011,axiom,
( X1 != X2
| union(X3,X1) = union(X3,X2) ) ).
cnf(i_0_228_012,axiom,
( X1 != X2
| ~ member(X1,X3)
| member(X2,X3) ) ).
cnf(i_0_229_013,axiom,
( X1 != X2
| ~ member(X3,X1)
| member(X3,X2) ) ).
cnf(i_0_230_014,axiom,
( X1 != X2
| ~ inductive(X1)
| inductive(X2) ) ).
cnf(i_0_231_015,axiom,
( X1 != X2
| ~ subclass(X1,X3)
| subclass(X2,X3) ) ).
cnf(i_0_232_016,axiom,
( X1 != X2
| ~ subclass(X3,X1)
| subclass(X3,X2) ) ).
cnf(i_0_233_017,axiom,
( X1 != X2
| ~ function(X1)
| function(X2) ) ).
cnf(i_0_234_018,axiom,
( X1 != X2
| ~ disjoint(X1,X3)
| disjoint(X2,X3) ) ).
cnf(i_0_235_019,axiom,
( X1 != X2
| ~ disjoint(X3,X1)
| disjoint(X3,X2) ) ).
cnf(i_0_236,plain,
( ~ member(union(X1,unordered_pair(X1,X1)),universal_class)
| ~ member(X1,universal_class)
| member(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(union(X1,unordered_pair(X1,X1)),union(X1,unordered_pair(X1,X1))))),successor_relation) ),
inference(equality_inference,[],[155]) ).
cnf(i_0_237,plain,
( ~ member(X1,universal_class)
| member(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X1,X1))),identity_relation) ),
inference(equality_inference,[],[163]) ).
cnf(i_0_238,plain,
( ~ member(X1,universal_class)
| member(X1,unordered_pair(X1,X2)) ),
inference(equality_inference,[],[179]) ).
cnf(i_0_239,plain,
( ~ member(X1,universal_class)
| member(X1,unordered_pair(X2,X1)) ),
inference(equality_inference,[],[180]) ).
cnf(i_0_240,plain,
subclass(X1,X1),
inference(equality_inference,[],[210]) ).
cnf(i_0_241,plain,
subclass(X1,X1),
inference(equality_inference,[],[211]) ).
cnf(i_0_242,plain,
$false,
inference(scs_inference,[],[i_0_213,i_0_191,i_0_238]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SET024+1 : TPTP v9.2.1. Bugfixed v5.4.0.
% 0.00/0.12 % Command : /export/starexec/sandbox2/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox2/solver/bin/cse --final-prover /export/starexec/sandbox2/solver/bin/eprover --proof-time %d --global-time-limit %d
% 0.14/0.33 % Computer : n022.cluster.edu
% 0.14/0.33 % Model : x86_64 x86_64
% 0.14/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.33 % Memory : 8042.1875MB
% 0.14/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.33 % CPULimit : 300
% 0.14/0.33 % WCLimit : 300
% 0.14/0.33 % DateTime : Tue May 5 02:05:06 EDT 2026
% 0.14/0.33 % CPUTime :
% 0.14/0.34 % start to proof: theBenchmark
% 0.31/1.62 % Version : CSE_E---1.7
% 0.31/1.62 % Problem : theBenchmark.p
% 0.31/1.62 % SZS status Theorem for theBenchmark.p
% 0.31/1.62 % SZS output start CNFRefutation
% See solution above
% 0.31/1.64 % Total time : 1.272s
%------------------------------------------------------------------------------