%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : SET055-7 : TPTP v9.2.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox/solver/bin/cse --final-prover /export/starexec/sandbox/solver/bin/eprover --proof-time %d --global-time-limit %d
% Computer : n026.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:07:03 PM UTC 2026
% Result : Unsatisfiable 0.20s 1.78s
% Output : CNFRefutation 0.22s
% Verified :
% SZS Type : Refutation
% Derivation depth : 2
% Number of leaves : 165
% Syntax : Number of clauses : 331 ( 63 unt; 16 nHn; 199 RR)
% Number of literals : 689 ( 0 equ; 348 neg)
% Maximal clause size : 5 ( 2 avg)
% Maximal term depth : 6 ( 1 avg)
% Number of predicates : 11 ( 10 usr; 1 prp; 0-3 aty)
% Number of functors : 39 ( 39 usr; 9 con; 0-3 aty)
% Number of variables : 796 ( 72 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(homomorphism6,axiom,
( homomorphism(X3,X1,X2)
| ~ operation(X1)
| ~ operation(X2)
| ~ compatible(X3,X1,X2)
| ~ equalish(apply(X2,ordered_pair(apply(X3,not_homomorphism1(X3,X1,X2)),apply(X3,not_homomorphism2(X3,X1,X2)))),apply(X3,apply(X1,ordered_pair(not_homomorphism1(X3,X1,X2),not_homomorphism2(X3,X1,X2))))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',homomorphism6) ).
cnf(range,axiom,
equalish(second(not_subclass_element(restrict(X1,singleton(X2),X3),null_class)),range(X1,X2,X3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',range) ).
cnf(domain,axiom,
equalish(first(not_subclass_element(restrict(X1,X2,singleton(X3)),null_class)),domain(X1,X2,X3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',domain) ).
cnf(homomorphism4,axiom,
( equalish(apply(X3,ordered_pair(apply(X1,X4),apply(X1,X5))),apply(X1,apply(X2,ordered_pair(X4,X5))))
| ~ homomorphism(X1,X2,X3)
| ~ member(ordered_pair(X4,X5),domain_of(X2)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',homomorphism4) ).
cnf(homomorphism5,axiom,
( member(ordered_pair(not_homomorphism1(X3,X1,X2),not_homomorphism2(X3,X1,X2)),domain_of(X1))
| homomorphism(X3,X1,X2)
| ~ operation(X1)
| ~ operation(X2)
| ~ compatible(X3,X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',homomorphism5) ).
cnf(subset_relation,axiom,
equalish(intersection(cross_product(universal_class,universal_class),intersection(cross_product(universal_class,universal_class),complement(compose(complement(element_relation),inverse(element_relation))))),subset_relation),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',subset_relation) ).
cnf(flip3,axiom,
( member(ordered_pair(ordered_pair(X2,X1),X3),flip(X4))
| ~ member(ordered_pair(ordered_pair(X1,X2),X3),X4)
| ~ member(ordered_pair(ordered_pair(X2,X1),X3),cross_product(cross_product(universal_class,universal_class),universal_class)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',flip3) ).
cnf(rotate3,axiom,
( member(ordered_pair(ordered_pair(X3,X1),X2),rotate(X4))
| ~ member(ordered_pair(ordered_pair(X1,X2),X3),X4)
| ~ member(ordered_pair(ordered_pair(X3,X1),X2),cross_product(cross_product(universal_class,universal_class),universal_class)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rotate3) ).
cnf(symmetric_difference,axiom,
equalish(intersection(complement(intersection(X1,X2)),complement(intersection(complement(X1),complement(X2)))),symmetric_difference(X1,X2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',symmetric_difference) ).
cnf(compose3,axiom,
( member(ordered_pair(X4,X1),compose(X2,X3))
| ~ member(X1,image(X2,image(X3,singleton(X4))))
| ~ member(ordered_pair(X4,X1),cross_product(universal_class,universal_class)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',compose3) ).
cnf(operation4,axiom,
( operation(X1)
| ~ function(X1)
| ~ equalish(cross_product(domain_of(domain_of(X1)),domain_of(domain_of(X1))),domain_of(X1))
| ~ subclass(range_of(X1),domain_of(domain_of(X1))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',operation4) ).
cnf(image,axiom,
equalish(range_of(restrict(X1,X2,universal_class)),image(X1,X2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',image) ).
cnf(restrict_substitution1,axiom,
( equalish(restrict(X1,X3,X4),restrict(X2,X3,X4))
| ~ equalish(X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',restrict_substitution1) ).
cnf(restrict_substitution2,axiom,
( equalish(restrict(X3,X1,X4),restrict(X3,X2,X4))
| ~ equalish(X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',restrict_substitution2) ).
cnf(restrict_substitution3,axiom,
( equalish(restrict(X3,X4,X1),restrict(X3,X4,X2))
| ~ equalish(X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',restrict_substitution3) ).
cnf(range_substitution1,axiom,
( equalish(range(X1,X3,X4),range(X2,X3,X4))
| ~ equalish(X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',range_substitution1) ).
cnf(range_substitution2,axiom,
( equalish(range(X3,X1,X4),range(X3,X2,X4))
| ~ equalish(X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',range_substitution2) ).
cnf(range_substitution3,axiom,
( equalish(range(X3,X4,X1),range(X3,X4,X2))
| ~ equalish(X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',range_substitution3) ).
cnf(not_homomorphism2_substitution1,axiom,
( equalish(not_homomorphism2(X1,X3,X4),not_homomorphism2(X2,X3,X4))
| ~ equalish(X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',not_homomorphism2_substitution1) ).
cnf(not_homomorphism2_substitution2,axiom,
( equalish(not_homomorphism2(X3,X1,X4),not_homomorphism2(X3,X2,X4))
| ~ equalish(X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',not_homomorphism2_substitution2) ).
cnf(not_homomorphism2_substitution3,axiom,
( equalish(not_homomorphism2(X3,X4,X1),not_homomorphism2(X3,X4,X2))
| ~ equalish(X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',not_homomorphism2_substitution3) ).
cnf(not_homomorphism1_substitution1,axiom,
( equalish(not_homomorphism1(X1,X3,X4),not_homomorphism1(X2,X3,X4))
| ~ equalish(X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',not_homomorphism1_substitution1) ).
cnf(not_homomorphism1_substitution2,axiom,
( equalish(not_homomorphism1(X3,X1,X4),not_homomorphism1(X3,X2,X4))
| ~ equalish(X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',not_homomorphism1_substitution2) ).
cnf(not_homomorphism1_substitution3,axiom,
( equalish(not_homomorphism1(X3,X4,X1),not_homomorphism1(X3,X4,X2))
| ~ equalish(X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',not_homomorphism1_substitution3) ).
cnf(domain_substitution1,axiom,
( equalish(domain(X1,X3,X4),domain(X2,X3,X4))
| ~ equalish(X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',domain_substitution1) ).
cnf(domain_substitution2,axiom,
( equalish(domain(X3,X1,X4),domain(X3,X2,X4))
| ~ equalish(X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',domain_substitution2) ).
cnf(domain_substitution3,axiom,
( equalish(domain(X3,X4,X1),domain(X3,X4,X2))
| ~ equalish(X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',domain_substitution3) ).
cnf(flip2,axiom,
( member(ordered_pair(ordered_pair(X2,X1),X3),X4)
| ~ member(ordered_pair(ordered_pair(X1,X2),X3),flip(X4)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',flip2) ).
cnf(rotate2,axiom,
( member(ordered_pair(ordered_pair(X2,X3),X1),X4)
| ~ member(ordered_pair(ordered_pair(X1,X2),X3),rotate(X4)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rotate2) ).
cnf(domain1,axiom,
( ~ equalish(restrict(X1,singleton(X2),universal_class),null_class)
| ~ member(X2,domain_of(X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',domain1) ).
cnf(sum_class_definition,axiom,
equalish(domain_of(restrict(element_relation,universal_class,X1)),sum_class(X1)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sum_class_definition) ).
cnf(compose2,axiom,
( member(X2,image(X3,image(X4,singleton(X1))))
| ~ member(ordered_pair(X1,X2),compose(X3,X4)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',compose2) ).
cnf(cantor_class,axiom,
equalish(intersection(domain_of(X1),diagonalise(compose(inverse(element_relation),X1))),cantor(X1)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cantor_class) ).
cnf(restriction2,axiom,
equalish(intersection(cross_product(X1,X2),X3),restrict(X3,X1,X2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',restriction2) ).
cnf(restriction1,axiom,
equalish(intersection(X1,cross_product(X2,X3)),restrict(X1,X2,X3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',restriction1) ).
cnf(compatible4,axiom,
( compatible(X4,X2,X3)
| ~ function(X1)
| ~ equalish(domain_of(domain_of(X2)),domain_of(X1))
| ~ subclass(range_of(X1),domain_of(domain_of(X3))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',compatible4) ).
cnf(domain2,axiom,
( equalish(restrict(X2,singleton(X1),universal_class),null_class)
| member(X1,domain_of(X2))
| ~ member(X1,universal_class) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',domain2) ).
cnf(successor_relation3,axiom,
( member(ordered_pair(X1,X2),successor_relation)
| ~ equalish(successor(X1),X2)
| ~ member(ordered_pair(X1,X2),cross_product(universal_class,universal_class)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',successor_relation3) ).
cnf(homomorphism_substitution1,axiom,
( homomorphism(X2,X3,X4)
| ~ equalish(X1,X2)
| ~ homomorphism(X1,X3,X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',homomorphism_substitution1) ).
cnf(homomorphism_substitution2,axiom,
( homomorphism(X3,X2,X4)
| ~ equalish(X1,X2)
| ~ homomorphism(X3,X1,X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',homomorphism_substitution2) ).
cnf(homomorphism_substitution3,axiom,
( homomorphism(X3,X4,X2)
| ~ equalish(X1,X2)
| ~ homomorphism(X3,X4,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',homomorphism_substitution3) ).
cnf(compatible_substitution1,axiom,
( compatible(X2,X3,X4)
| ~ equalish(X1,X2)
| ~ compatible(X1,X3,X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',compatible_substitution1) ).
cnf(compatible_substitution2,axiom,
( compatible(X3,X2,X4)
| ~ equalish(X1,X2)
| ~ compatible(X3,X1,X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',compatible_substitution2) ).
cnf(compatible_substitution3,axiom,
( compatible(X3,X4,X2)
| ~ equalish(X1,X2)
| ~ compatible(X3,X4,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',compatible_substitution3) ).
cnf(element_relation3,axiom,
( member(ordered_pair(X1,X2),element_relation)
| ~ member(ordered_pair(X1,X2),cross_product(universal_class,universal_class))
| ~ member(X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',element_relation3) ).
cnf(ordered_pair,axiom,
equalish(unordered_pair(singleton(X1),unordered_pair(X1,singleton(X2))),ordered_pair(X1,X2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ordered_pair) ).
cnf(union,axiom,
equalish(complement(intersection(complement(X1),complement(X2))),union(X1,X2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',union) ).
cnf(corollary_1_to_unordered_pair,axiom,
( member(X1,unordered_pair(X1,X2))
| ~ member(ordered_pair(X1,X2),cross_product(X3,X4)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',corollary_1_to_unordered_pair) ).
cnf(corollary_2_to_unordered_pair,axiom,
( member(X2,unordered_pair(X1,X2))
| ~ member(ordered_pair(X1,X2),cross_product(X3,X4)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',corollary_2_to_unordered_pair) ).
cnf(homomorphism3,axiom,
( compatible(X1,X2,X3)
| ~ homomorphism(X1,X2,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',homomorphism3) ).
cnf(function3,axiom,
( function(X1)
| ~ subclass(X1,cross_product(universal_class,universal_class))
| ~ subclass(compose(X1,inverse(X1)),identity_relation) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',function3) ).
cnf(inverse,axiom,
equalish(domain_of(flip(cross_product(X1,universal_class))),inverse(X1)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',inverse) ).
cnf(diagonalisation,axiom,
equalish(complement(domain_of(intersection(X1,identity_relation))),diagonalise(X1)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',diagonalisation) ).
cnf(cartesian_product4,axiom,
( equalish(ordered_pair(first(X1),second(X1)),X1)
| ~ member(X1,cross_product(X2,X3)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cartesian_product4) ).
cnf(operation2,axiom,
( equalish(cross_product(domain_of(domain_of(X1)),domain_of(domain_of(X1))),domain_of(X1))
| ~ operation(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',operation2) ).
cnf(compatible2,axiom,
( equalish(domain_of(domain_of(X2)),domain_of(X1))
| ~ compatible(X1,X2,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',compatible2) ).
cnf(compatible3,axiom,
( subclass(range_of(X1),domain_of(domain_of(X3)))
| ~ compatible(X1,X2,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',compatible3) ).
cnf(apply,axiom,
equalish(sum_class(image(X1,singleton(X2))),apply(X1,X2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',apply) ).
cnf(cartesian_product1,axiom,
( member(X1,X3)
| ~ member(ordered_pair(X1,X2),cross_product(X3,X4)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cartesian_product1) ).
cnf(cartesian_product2,axiom,
( member(X2,X4)
| ~ member(ordered_pair(X1,X2),cross_product(X3,X4)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cartesian_product2) ).
cnf(corollary_1_to_cartesian_product,axiom,
( member(X1,universal_class)
| ~ member(ordered_pair(X1,X2),cross_product(X3,X4)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',corollary_1_to_cartesian_product) ).
cnf(corollary_2_to_cartesian_product,axiom,
( member(X2,universal_class)
| ~ member(ordered_pair(X1,X2),cross_product(X3,X4)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',corollary_2_to_cartesian_product) ).
cnf(cartesian_product3,axiom,
( member(ordered_pair(X1,X3),cross_product(X2,X4))
| ~ member(X1,X2)
| ~ member(X3,X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cartesian_product3) ).
cnf(power_class_definition,axiom,
equalish(complement(image(element_relation,complement(X1))),power_class(X1)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',power_class_definition) ).
cnf(unordered_pair_member,axiom,
( equalish(X1,X2)
| equalish(X1,X3)
| ~ member(X1,unordered_pair(X2,X3)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',unordered_pair_member) ).
cnf(homomorphism1,axiom,
( operation(X2)
| ~ homomorphism(X1,X2,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',homomorphism1) ).
cnf(homomorphism2,axiom,
( operation(X3)
| ~ homomorphism(X1,X2,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',homomorphism2) ).
cnf(compatible1,axiom,
( function(X1)
| ~ compatible(X1,X2,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',compatible1) ).
cnf(unordered_pair_substitution1,axiom,
( equalish(unordered_pair(X1,X3),unordered_pair(X2,X3))
| ~ equalish(X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',unordered_pair_substitution1) ).
cnf(unordered_pair_substitution2,axiom,
( equalish(unordered_pair(X3,X1),unordered_pair(X3,X2))
| ~ equalish(X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',unordered_pair_substitution2) ).
cnf(union_substitution1,axiom,
( equalish(union(X1,X3),union(X2,X3))
| ~ equalish(X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',union_substitution1) ).
cnf(union_substitution2,axiom,
( equalish(union(X3,X1),union(X3,X2))
| ~ equalish(X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',union_substitution2) ).
cnf(ordered_pair_substitution1,axiom,
( equalish(ordered_pair(X1,X3),ordered_pair(X2,X3))
| ~ equalish(X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ordered_pair_substitution1) ).
cnf(ordered_pair_substitution2,axiom,
( equalish(ordered_pair(X3,X1),ordered_pair(X3,X2))
| ~ equalish(X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ordered_pair_substitution2) ).
cnf(not_subclass_element_substitution1,axiom,
( equalish(not_subclass_element(X1,X3),not_subclass_element(X2,X3))
| ~ equalish(X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',not_subclass_element_substitution1) ).
cnf(not_subclass_element_substitution2,axiom,
( equalish(not_subclass_element(X3,X1),not_subclass_element(X3,X2))
| ~ equalish(X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',not_subclass_element_substitution2) ).
cnf(intersection_substitution1,axiom,
( equalish(intersection(X1,X3),intersection(X2,X3))
| ~ equalish(X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',intersection_substitution1) ).
cnf(intersection_substitution2,axiom,
( equalish(intersection(X3,X1),intersection(X3,X2))
| ~ equalish(X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',intersection_substitution2) ).
cnf(image_substitution1,axiom,
( equalish(image(X1,X3),image(X2,X3))
| ~ equalish(X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',image_substitution1) ).
cnf(image_substitution2,axiom,
( equalish(image(X3,X1),image(X3,X2))
| ~ equalish(X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',image_substitution2) ).
cnf(symmetric_difference_substitution1,axiom,
( equalish(symmetric_difference(X1,X3),symmetric_difference(X2,X3))
| ~ equalish(X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',symmetric_difference_substitution1) ).
cnf(symmetric_difference_substitution2,axiom,
( equalish(symmetric_difference(X3,X1),symmetric_difference(X3,X2))
| ~ equalish(X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',symmetric_difference_substitution2) ).
cnf(cross_product_substitution1,axiom,
( equalish(cross_product(X1,X3),cross_product(X2,X3))
| ~ equalish(X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cross_product_substitution1) ).
cnf(cross_product_substitution2,axiom,
( equalish(cross_product(X3,X1),cross_product(X3,X2))
| ~ equalish(X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cross_product_substitution2) ).
cnf(compose_substitution1,axiom,
( equalish(compose(X1,X3),compose(X2,X3))
| ~ equalish(X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',compose_substitution1) ).
cnf(compose_substitution2,axiom,
( equalish(compose(X3,X1),compose(X3,X2))
| ~ equalish(X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',compose_substitution2) ).
cnf(apply_substitution1,axiom,
( equalish(apply(X1,X3),apply(X2,X3))
| ~ equalish(X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',apply_substitution1) ).
cnf(apply_substitution2,axiom,
( equalish(apply(X3,X1),apply(X3,X2))
| ~ equalish(X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',apply_substitution2) ).
cnf(intersection3,axiom,
( member(X1,intersection(X2,X3))
| ~ member(X1,X2)
| ~ member(X1,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',intersection3) ).
cnf(single_valued_class2,axiom,
( single_valued_class(X1)
| ~ subclass(compose(X1,inverse(X1)),identity_relation) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',single_valued_class2) ).
cnf(inductive3,axiom,
( inductive(X1)
| ~ member(null_class,X1)
| ~ subclass(image(successor_relation,X1),X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',inductive3) ).
cnf(rotate1,axiom,
subclass(rotate(X1),cross_product(cross_product(universal_class,universal_class),universal_class)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rotate1) ).
cnf(flip1,axiom,
subclass(flip(X1),cross_product(cross_product(universal_class,universal_class),universal_class)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',flip1) ).
cnf(successor_relation2,axiom,
( equalish(successor(X1),X2)
| ~ member(ordered_pair(X1,X2),successor_relation) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',successor_relation2) ).
cnf(not_subclass_members2,axiom,
( subclass(X1,X2)
| ~ member(not_subclass_element(X1,X2),X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',not_subclass_members2) ).
cnf(intersection1,axiom,
( member(X1,X2)
| ~ member(X1,intersection(X2,X3)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',intersection1) ).
cnf(intersection2,axiom,
( member(X1,X3)
| ~ member(X1,intersection(X2,X3)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',intersection2) ).
cnf(element_relation2,axiom,
( member(X1,X2)
| ~ member(ordered_pair(X1,X2),element_relation) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',element_relation2) ).
cnf(choice2,axiom,
( equalish(X1,null_class)
| member(apply(choice,X1),X1)
| ~ member(X1,universal_class) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',choice2) ).
cnf(replacement,axiom,
( member(image(X1,X2),universal_class)
| ~ function(X1)
| ~ member(X2,universal_class) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',replacement) ).
cnf(regularity2,axiom,
( equalish(X1,null_class)
| equalish(intersection(X1,regular(X1)),null_class) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',regularity2) ).
cnf(unordered_pair2,axiom,
( member(X1,unordered_pair(X1,X2))
| ~ member(X1,universal_class) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',unordered_pair2) ).
cnf(unordered_pair3,axiom,
( member(X1,unordered_pair(X2,X1))
| ~ member(X1,universal_class) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',unordered_pair3) ).
cnf(compose1,axiom,
subclass(compose(X1,X2),cross_product(universal_class,universal_class)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',compose1) ).
cnf(transitivity_of_subclass,axiom,
( subclass(X1,X3)
| ~ subclass(X1,X2)
| ~ subclass(X2,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',transitivity_of_subclass) ).
cnf(subclass_substitution1,axiom,
( subclass(X2,X3)
| ~ equalish(X1,X2)
| ~ subclass(X1,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',subclass_substitution1) ).
cnf(subclass_substitution2,axiom,
( subclass(X3,X2)
| ~ equalish(X1,X2)
| ~ subclass(X3,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',subclass_substitution2) ).
cnf(member_substitution1,axiom,
( member(X2,X3)
| ~ equalish(X1,X2)
| ~ member(X1,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',member_substitution1) ).
cnf(subclass_members,axiom,
( member(X3,X2)
| ~ subclass(X1,X2)
| ~ member(X3,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',subclass_members) ).
cnf(member_substitution2,axiom,
( member(X3,X2)
| ~ equalish(X1,X2)
| ~ member(X3,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',member_substitution2) ).
cnf(subclass_implies_equal,axiom,
( equalish(X1,X2)
| ~ subclass(X1,X2)
| ~ subclass(X2,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',subclass_implies_equal) ).
cnf(transitivity,axiom,
( equalish(X1,X3)
| ~ equalish(X1,X2)
| ~ equalish(X2,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',transitivity) ).
cnf(successor,axiom,
equalish(union(X1,singleton(X1)),successor(X1)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',successor) ).
cnf(single_valued_class1,axiom,
( subclass(compose(X1,inverse(X1)),identity_relation)
| ~ single_valued_class(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',single_valued_class1) ).
cnf(function2,axiom,
( subclass(compose(X1,inverse(X1)),identity_relation)
| ~ function(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',function2) ).
cnf(complement2,axiom,
( member(X1,complement(X2))
| member(X1,X2)
| ~ member(X1,universal_class) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',complement2) ).
cnf(complement1,axiom,
( ~ member(X1,complement(X2))
| ~ member(X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',complement1) ).
cnf(not_subclass_members1,axiom,
( member(not_subclass_element(X1,X2),X1)
| subclass(X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',not_subclass_members1) ).
cnf(sum_class_substitution1,axiom,
( equalish(sum_class(X1),sum_class(X2))
| ~ equalish(X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sum_class_substitution1) ).
cnf(successor_substitution1,axiom,
( equalish(successor(X1),successor(X2))
| ~ equalish(X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',successor_substitution1) ).
cnf(singleton_substitution1,axiom,
( equalish(singleton(X1),singleton(X2))
| ~ equalish(X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',singleton_substitution1) ).
cnf(second_substitution1,axiom,
( equalish(second(X1),second(X2))
| ~ equalish(X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',second_substitution1) ).
cnf(rotate_substitution1,axiom,
( equalish(rotate(X1),rotate(X2))
| ~ equalish(X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rotate_substitution1) ).
cnf(regular_substitution1,axiom,
( equalish(regular(X1),regular(X2))
| ~ equalish(X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',regular_substitution1) ).
cnf(range_of_substitution1,axiom,
( equalish(range_of(X1),range_of(X2))
| ~ equalish(X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',range_of_substitution1) ).
cnf(power_class_substitution1,axiom,
( equalish(power_class(X1),power_class(X2))
| ~ equalish(X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',power_class_substitution1) ).
cnf(inverse_substitution1,axiom,
( equalish(inverse(X1),inverse(X2))
| ~ equalish(X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',inverse_substitution1) ).
cnf(flip_substitution1,axiom,
( equalish(flip(X1),flip(X2))
| ~ equalish(X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',flip_substitution1) ).
cnf(first_substitution1,axiom,
( equalish(first(X1),first(X2))
| ~ equalish(X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',first_substitution1) ).
cnf(domain_of_substitution1,axiom,
( equalish(domain_of(X1),domain_of(X2))
| ~ equalish(X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',domain_of_substitution1) ).
cnf(diagonalise_substitution1,axiom,
( equalish(diagonalise(X1),diagonalise(X2))
| ~ equalish(X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',diagonalise_substitution1) ).
cnf(complement_substitution1,axiom,
( equalish(complement(X1),complement(X2))
| ~ equalish(X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',complement_substitution1) ).
cnf(cantor_substitution1,axiom,
( equalish(cantor(X1),cantor(X2))
| ~ equalish(X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cantor_substitution1) ).
cnf(singleton_set,axiom,
equalish(unordered_pair(X1,X1),singleton(X1)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',singleton_set) ).
cnf(operation3,axiom,
( subclass(range_of(X1),domain_of(domain_of(X1)))
| ~ operation(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',operation3) ).
cnf(inductive2,axiom,
( subclass(image(successor_relation,X1),X1)
| ~ inductive(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',inductive2) ).
cnf(identity_relation,axiom,
equalish(intersection(inverse(subset_relation),subset_relation),identity_relation),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',identity_relation) ).
cnf(function1,axiom,
( subclass(X1,cross_product(universal_class,universal_class))
| ~ function(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',function1) ).
cnf(sum_class2,axiom,
( member(sum_class(X1),universal_class)
| ~ member(X1,universal_class) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sum_class2) ).
cnf(power_class2,axiom,
( member(power_class(X1),universal_class)
| ~ member(X1,universal_class) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',power_class2) ).
cnf(range_of,axiom,
equalish(domain_of(inverse(X1)),range_of(X1)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',range_of) ).
cnf(unordered_pairs_in_universal,axiom,
member(unordered_pair(X1,X2),universal_class),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',unordered_pairs_in_universal) ).
cnf(equal_implies_subclass1,axiom,
( subclass(X1,X2)
| ~ equalish(X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',equal_implies_subclass1) ).
cnf(equal_implies_subclass2,axiom,
( subclass(X2,X1)
| ~ equalish(X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',equal_implies_subclass2) ).
cnf(symmetry,axiom,
( equalish(X2,X1)
| ~ equalish(X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',symmetry) ).
cnf(single_valued_class_substitution1,axiom,
( single_valued_class(X2)
| ~ equalish(X1,X2)
| ~ single_valued_class(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',single_valued_class_substitution1) ).
cnf(operation_substitution1,axiom,
( operation(X2)
| ~ equalish(X1,X2)
| ~ operation(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',operation_substitution1) ).
cnf(one_to_one_substitution1,axiom,
( one_to_one(X2)
| ~ equalish(X1,X2)
| ~ one_to_one(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',one_to_one_substitution1) ).
cnf(inductive_substitution1,axiom,
( inductive(X2)
| ~ equalish(X1,X2)
| ~ inductive(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',inductive_substitution1) ).
cnf(function_substitution1,axiom,
( function(X2)
| ~ equalish(X1,X2)
| ~ function(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',function_substitution1) ).
cnf(regularity1,axiom,
( equalish(X1,null_class)
| member(regular(X1),X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',regularity1) ).
cnf(successor_relation1,axiom,
subclass(successor_relation,cross_product(universal_class,universal_class)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',successor_relation1) ).
cnf(element_relation1,axiom,
subclass(element_relation,cross_product(universal_class,universal_class)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',element_relation1) ).
cnf(one_to_one3,axiom,
( one_to_one(X1)
| ~ function(inverse(X1))
| ~ function(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',one_to_one3) ).
cnf(omega_is_inductive2,axiom,
( subclass(omega,X1)
| ~ inductive(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',omega_is_inductive2) ).
cnf(inductive1,axiom,
( member(null_class,X1)
| ~ inductive(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',inductive1) ).
cnf(prove_reflexivity,negated_conjecture,
~ equalish(x,x),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_reflexivity) ).
cnf(one_to_one2,axiom,
( function(inverse(X1))
| ~ one_to_one(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',one_to_one2) ).
cnf(subclass_is_reflexive,axiom,
subclass(X1,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',subclass_is_reflexive) ).
cnf(class_elements_are_sets,axiom,
subclass(X1,universal_class),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',class_elements_are_sets) ).
cnf(operation1,axiom,
( function(X1)
| ~ operation(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',operation1) ).
cnf(one_to_one1,axiom,
( function(X1)
| ~ one_to_one(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',one_to_one1) ).
cnf(omega_in_universal,axiom,
member(omega,universal_class),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',omega_in_universal) ).
cnf(omega_is_inductive1,axiom,
inductive(omega),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',omega_is_inductive1) ).
cnf(choice1,axiom,
function(choice),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',choice1) ).
cnf(i_0_165,axiom,
( homomorphism(X3,X1,X2)
| ~ operation(X1)
| ~ operation(X2)
| ~ compatible(X3,X1,X2)
| ~ equalish(apply(X2,ordered_pair(apply(X3,not_homomorphism1(X3,X1,X2)),apply(X3,not_homomorphism2(X3,X1,X2)))),apply(X3,apply(X1,ordered_pair(not_homomorphism1(X3,X1,X2),not_homomorphism2(X3,X1,X2))))) ),
homomorphism6,
[final] ).
cnf(i_0_166,axiom,
equalish(second(not_subclass_element(restrict(X1,singleton(X2),X3),null_class)),range(X1,X2,X3)),
range,
[final] ).
cnf(i_0_167,axiom,
equalish(first(not_subclass_element(restrict(X1,X2,singleton(X3)),null_class)),domain(X1,X2,X3)),
domain,
[final] ).
cnf(i_0_168,axiom,
( equalish(apply(X3,ordered_pair(apply(X1,X4),apply(X1,X5))),apply(X1,apply(X2,ordered_pair(X4,X5))))
| ~ homomorphism(X1,X2,X3)
| ~ member(ordered_pair(X4,X5),domain_of(X2)) ),
homomorphism4,
[final] ).
cnf(i_0_169,axiom,
( member(ordered_pair(not_homomorphism1(X3,X1,X2),not_homomorphism2(X3,X1,X2)),domain_of(X1))
| homomorphism(X3,X1,X2)
| ~ operation(X1)
| ~ operation(X2)
| ~ compatible(X3,X1,X2) ),
homomorphism5,
[final] ).
cnf(i_0_170,axiom,
equalish(intersection(cross_product(universal_class,universal_class),intersection(cross_product(universal_class,universal_class),complement(compose(complement(element_relation),inverse(element_relation))))),subset_relation),
subset_relation,
[final] ).
cnf(i_0_171,axiom,
( member(ordered_pair(ordered_pair(X2,X1),X3),flip(X4))
| ~ member(ordered_pair(ordered_pair(X1,X2),X3),X4)
| ~ member(ordered_pair(ordered_pair(X2,X1),X3),cross_product(cross_product(universal_class,universal_class),universal_class)) ),
flip3,
[final] ).
cnf(i_0_172,axiom,
( member(ordered_pair(ordered_pair(X3,X1),X2),rotate(X4))
| ~ member(ordered_pair(ordered_pair(X1,X2),X3),X4)
| ~ member(ordered_pair(ordered_pair(X3,X1),X2),cross_product(cross_product(universal_class,universal_class),universal_class)) ),
rotate3,
[final] ).
cnf(i_0_173,axiom,
equalish(intersection(complement(intersection(X1,X2)),complement(intersection(complement(X1),complement(X2)))),symmetric_difference(X1,X2)),
symmetric_difference,
[final] ).
cnf(i_0_174,axiom,
( member(ordered_pair(X4,X1),compose(X2,X3))
| ~ member(X1,image(X2,image(X3,singleton(X4))))
| ~ member(ordered_pair(X4,X1),cross_product(universal_class,universal_class)) ),
compose3,
[final] ).
cnf(i_0_175,axiom,
( operation(X1)
| ~ function(X1)
| ~ equalish(cross_product(domain_of(domain_of(X1)),domain_of(domain_of(X1))),domain_of(X1))
| ~ subclass(range_of(X1),domain_of(domain_of(X1))) ),
operation4,
[final] ).
cnf(i_0_176,axiom,
equalish(range_of(restrict(X1,X2,universal_class)),image(X1,X2)),
image,
[final] ).
cnf(i_0_177,axiom,
( equalish(restrict(X1,X3,X4),restrict(X2,X3,X4))
| ~ equalish(X1,X2) ),
restrict_substitution1,
[final] ).
cnf(i_0_178,axiom,
( equalish(restrict(X3,X1,X4),restrict(X3,X2,X4))
| ~ equalish(X1,X2) ),
restrict_substitution2,
[final] ).
cnf(i_0_179,axiom,
( equalish(restrict(X3,X4,X1),restrict(X3,X4,X2))
| ~ equalish(X1,X2) ),
restrict_substitution3,
[final] ).
cnf(i_0_180,axiom,
( equalish(range(X1,X3,X4),range(X2,X3,X4))
| ~ equalish(X1,X2) ),
range_substitution1,
[final] ).
cnf(i_0_181,axiom,
( equalish(range(X3,X1,X4),range(X3,X2,X4))
| ~ equalish(X1,X2) ),
range_substitution2,
[final] ).
cnf(i_0_182,axiom,
( equalish(range(X3,X4,X1),range(X3,X4,X2))
| ~ equalish(X1,X2) ),
range_substitution3,
[final] ).
cnf(i_0_183,axiom,
( equalish(not_homomorphism2(X1,X3,X4),not_homomorphism2(X2,X3,X4))
| ~ equalish(X1,X2) ),
not_homomorphism2_substitution1,
[final] ).
cnf(i_0_184,axiom,
( equalish(not_homomorphism2(X3,X1,X4),not_homomorphism2(X3,X2,X4))
| ~ equalish(X1,X2) ),
not_homomorphism2_substitution2,
[final] ).
cnf(i_0_185,axiom,
( equalish(not_homomorphism2(X3,X4,X1),not_homomorphism2(X3,X4,X2))
| ~ equalish(X1,X2) ),
not_homomorphism2_substitution3,
[final] ).
cnf(i_0_186,axiom,
( equalish(not_homomorphism1(X1,X3,X4),not_homomorphism1(X2,X3,X4))
| ~ equalish(X1,X2) ),
not_homomorphism1_substitution1,
[final] ).
cnf(i_0_187,axiom,
( equalish(not_homomorphism1(X3,X1,X4),not_homomorphism1(X3,X2,X4))
| ~ equalish(X1,X2) ),
not_homomorphism1_substitution2,
[final] ).
cnf(i_0_188,axiom,
( equalish(not_homomorphism1(X3,X4,X1),not_homomorphism1(X3,X4,X2))
| ~ equalish(X1,X2) ),
not_homomorphism1_substitution3,
[final] ).
cnf(i_0_189,axiom,
( equalish(domain(X1,X3,X4),domain(X2,X3,X4))
| ~ equalish(X1,X2) ),
domain_substitution1,
[final] ).
cnf(i_0_190,axiom,
( equalish(domain(X3,X1,X4),domain(X3,X2,X4))
| ~ equalish(X1,X2) ),
domain_substitution2,
[final] ).
cnf(i_0_191,axiom,
( equalish(domain(X3,X4,X1),domain(X3,X4,X2))
| ~ equalish(X1,X2) ),
domain_substitution3,
[final] ).
cnf(i_0_192,axiom,
( member(ordered_pair(ordered_pair(X2,X1),X3),X4)
| ~ member(ordered_pair(ordered_pair(X1,X2),X3),flip(X4)) ),
flip2,
[final] ).
cnf(i_0_193,axiom,
( member(ordered_pair(ordered_pair(X2,X3),X1),X4)
| ~ member(ordered_pair(ordered_pair(X1,X2),X3),rotate(X4)) ),
rotate2,
[final] ).
cnf(i_0_194,axiom,
( ~ equalish(restrict(X1,singleton(X2),universal_class),null_class)
| ~ member(X2,domain_of(X1)) ),
domain1,
[final] ).
cnf(i_0_195,axiom,
equalish(domain_of(restrict(element_relation,universal_class,X1)),sum_class(X1)),
sum_class_definition,
[final] ).
cnf(i_0_196,axiom,
( member(X2,image(X3,image(X4,singleton(X1))))
| ~ member(ordered_pair(X1,X2),compose(X3,X4)) ),
compose2,
[final] ).
cnf(i_0_197,axiom,
equalish(intersection(domain_of(X1),diagonalise(compose(inverse(element_relation),X1))),cantor(X1)),
cantor_class,
[final] ).
cnf(i_0_198,axiom,
equalish(intersection(cross_product(X1,X2),X3),restrict(X3,X1,X2)),
restriction2,
[final] ).
cnf(i_0_199,axiom,
equalish(intersection(X1,cross_product(X2,X3)),restrict(X1,X2,X3)),
restriction1,
[final] ).
cnf(i_0_200,axiom,
( compatible(X4,X2,X3)
| ~ function(X1)
| ~ equalish(domain_of(domain_of(X2)),domain_of(X1))
| ~ subclass(range_of(X1),domain_of(domain_of(X3))) ),
compatible4,
[final] ).
cnf(i_0_201,axiom,
( equalish(restrict(X2,singleton(X1),universal_class),null_class)
| member(X1,domain_of(X2))
| ~ member(X1,universal_class) ),
domain2,
[final] ).
cnf(i_0_202,axiom,
( member(ordered_pair(X1,X2),successor_relation)
| ~ equalish(successor(X1),X2)
| ~ member(ordered_pair(X1,X2),cross_product(universal_class,universal_class)) ),
successor_relation3,
[final] ).
cnf(i_0_203,axiom,
( homomorphism(X2,X3,X4)
| ~ equalish(X1,X2)
| ~ homomorphism(X1,X3,X4) ),
homomorphism_substitution1,
[final] ).
cnf(i_0_204,axiom,
( homomorphism(X3,X2,X4)
| ~ equalish(X1,X2)
| ~ homomorphism(X3,X1,X4) ),
homomorphism_substitution2,
[final] ).
cnf(i_0_205,axiom,
( homomorphism(X3,X4,X2)
| ~ equalish(X1,X2)
| ~ homomorphism(X3,X4,X1) ),
homomorphism_substitution3,
[final] ).
cnf(i_0_206,axiom,
( compatible(X2,X3,X4)
| ~ equalish(X1,X2)
| ~ compatible(X1,X3,X4) ),
compatible_substitution1,
[final] ).
cnf(i_0_207,axiom,
( compatible(X3,X2,X4)
| ~ equalish(X1,X2)
| ~ compatible(X3,X1,X4) ),
compatible_substitution2,
[final] ).
cnf(i_0_208,axiom,
( compatible(X3,X4,X2)
| ~ equalish(X1,X2)
| ~ compatible(X3,X4,X1) ),
compatible_substitution3,
[final] ).
cnf(i_0_209,axiom,
( member(ordered_pair(X1,X2),element_relation)
| ~ member(ordered_pair(X1,X2),cross_product(universal_class,universal_class))
| ~ member(X1,X2) ),
element_relation3,
[final] ).
cnf(i_0_210,axiom,
equalish(unordered_pair(singleton(X1),unordered_pair(X1,singleton(X2))),ordered_pair(X1,X2)),
ordered_pair,
[final] ).
cnf(i_0_211,axiom,
equalish(complement(intersection(complement(X1),complement(X2))),union(X1,X2)),
union,
[final] ).
cnf(i_0_212,axiom,
( member(X1,unordered_pair(X1,X2))
| ~ member(ordered_pair(X1,X2),cross_product(X3,X4)) ),
corollary_1_to_unordered_pair,
[final] ).
cnf(i_0_213,axiom,
( member(X2,unordered_pair(X1,X2))
| ~ member(ordered_pair(X1,X2),cross_product(X3,X4)) ),
corollary_2_to_unordered_pair,
[final] ).
cnf(i_0_214,axiom,
( compatible(X1,X2,X3)
| ~ homomorphism(X1,X2,X3) ),
homomorphism3,
[final] ).
cnf(i_0_215,axiom,
( function(X1)
| ~ subclass(X1,cross_product(universal_class,universal_class))
| ~ subclass(compose(X1,inverse(X1)),identity_relation) ),
function3,
[final] ).
cnf(i_0_216,axiom,
equalish(domain_of(flip(cross_product(X1,universal_class))),inverse(X1)),
inverse,
[final] ).
cnf(i_0_217,axiom,
equalish(complement(domain_of(intersection(X1,identity_relation))),diagonalise(X1)),
diagonalisation,
[final] ).
cnf(i_0_218,axiom,
( equalish(ordered_pair(first(X1),second(X1)),X1)
| ~ member(X1,cross_product(X2,X3)) ),
cartesian_product4,
[final] ).
cnf(i_0_219,axiom,
( equalish(cross_product(domain_of(domain_of(X1)),domain_of(domain_of(X1))),domain_of(X1))
| ~ operation(X1) ),
operation2,
[final] ).
cnf(i_0_220,axiom,
( equalish(domain_of(domain_of(X2)),domain_of(X1))
| ~ compatible(X1,X2,X3) ),
compatible2,
[final] ).
cnf(i_0_221,axiom,
( subclass(range_of(X1),domain_of(domain_of(X3)))
| ~ compatible(X1,X2,X3) ),
compatible3,
[final] ).
cnf(i_0_222,axiom,
equalish(sum_class(image(X1,singleton(X2))),apply(X1,X2)),
apply,
[final] ).
cnf(i_0_223,axiom,
( member(X1,X3)
| ~ member(ordered_pair(X1,X2),cross_product(X3,X4)) ),
cartesian_product1,
[final] ).
cnf(i_0_224,axiom,
( member(X2,X4)
| ~ member(ordered_pair(X1,X2),cross_product(X3,X4)) ),
cartesian_product2,
[final] ).
cnf(i_0_225,axiom,
( member(X1,universal_class)
| ~ member(ordered_pair(X1,X2),cross_product(X3,X4)) ),
corollary_1_to_cartesian_product,
[final] ).
cnf(i_0_226,axiom,
( member(X2,universal_class)
| ~ member(ordered_pair(X1,X2),cross_product(X3,X4)) ),
corollary_2_to_cartesian_product,
[final] ).
cnf(i_0_227,axiom,
( member(ordered_pair(X1,X3),cross_product(X2,X4))
| ~ member(X1,X2)
| ~ member(X3,X4) ),
cartesian_product3,
[final] ).
cnf(i_0_228,axiom,
equalish(complement(image(element_relation,complement(X1))),power_class(X1)),
power_class_definition,
[final] ).
cnf(i_0_229,axiom,
( equalish(X1,X2)
| equalish(X1,X3)
| ~ member(X1,unordered_pair(X2,X3)) ),
unordered_pair_member,
[final] ).
cnf(i_0_230,axiom,
( operation(X2)
| ~ homomorphism(X1,X2,X3) ),
homomorphism1,
[final] ).
cnf(i_0_231,axiom,
( operation(X3)
| ~ homomorphism(X1,X2,X3) ),
homomorphism2,
[final] ).
cnf(i_0_232,axiom,
( function(X1)
| ~ compatible(X1,X2,X3) ),
compatible1,
[final] ).
cnf(i_0_233,axiom,
( equalish(unordered_pair(X1,X3),unordered_pair(X2,X3))
| ~ equalish(X1,X2) ),
unordered_pair_substitution1,
[final] ).
cnf(i_0_234,axiom,
( equalish(unordered_pair(X3,X1),unordered_pair(X3,X2))
| ~ equalish(X1,X2) ),
unordered_pair_substitution2,
[final] ).
cnf(i_0_235,axiom,
( equalish(union(X1,X3),union(X2,X3))
| ~ equalish(X1,X2) ),
union_substitution1,
[final] ).
cnf(i_0_236,axiom,
( equalish(union(X3,X1),union(X3,X2))
| ~ equalish(X1,X2) ),
union_substitution2,
[final] ).
cnf(i_0_237,axiom,
( equalish(ordered_pair(X1,X3),ordered_pair(X2,X3))
| ~ equalish(X1,X2) ),
ordered_pair_substitution1,
[final] ).
cnf(i_0_238,axiom,
( equalish(ordered_pair(X3,X1),ordered_pair(X3,X2))
| ~ equalish(X1,X2) ),
ordered_pair_substitution2,
[final] ).
cnf(i_0_239,axiom,
( equalish(not_subclass_element(X1,X3),not_subclass_element(X2,X3))
| ~ equalish(X1,X2) ),
not_subclass_element_substitution1,
[final] ).
cnf(i_0_240,axiom,
( equalish(not_subclass_element(X3,X1),not_subclass_element(X3,X2))
| ~ equalish(X1,X2) ),
not_subclass_element_substitution2,
[final] ).
cnf(i_0_241,axiom,
( equalish(intersection(X1,X3),intersection(X2,X3))
| ~ equalish(X1,X2) ),
intersection_substitution1,
[final] ).
cnf(i_0_242,axiom,
( equalish(intersection(X3,X1),intersection(X3,X2))
| ~ equalish(X1,X2) ),
intersection_substitution2,
[final] ).
cnf(i_0_243,axiom,
( equalish(image(X1,X3),image(X2,X3))
| ~ equalish(X1,X2) ),
image_substitution1,
[final] ).
cnf(i_0_244,axiom,
( equalish(image(X3,X1),image(X3,X2))
| ~ equalish(X1,X2) ),
image_substitution2,
[final] ).
cnf(i_0_245,axiom,
( equalish(symmetric_difference(X1,X3),symmetric_difference(X2,X3))
| ~ equalish(X1,X2) ),
symmetric_difference_substitution1,
[final] ).
cnf(i_0_246,axiom,
( equalish(symmetric_difference(X3,X1),symmetric_difference(X3,X2))
| ~ equalish(X1,X2) ),
symmetric_difference_substitution2,
[final] ).
cnf(i_0_247,axiom,
( equalish(cross_product(X1,X3),cross_product(X2,X3))
| ~ equalish(X1,X2) ),
cross_product_substitution1,
[final] ).
cnf(i_0_248,axiom,
( equalish(cross_product(X3,X1),cross_product(X3,X2))
| ~ equalish(X1,X2) ),
cross_product_substitution2,
[final] ).
cnf(i_0_249,axiom,
( equalish(compose(X1,X3),compose(X2,X3))
| ~ equalish(X1,X2) ),
compose_substitution1,
[final] ).
cnf(i_0_250,axiom,
( equalish(compose(X3,X1),compose(X3,X2))
| ~ equalish(X1,X2) ),
compose_substitution2,
[final] ).
cnf(i_0_251,axiom,
( equalish(apply(X1,X3),apply(X2,X3))
| ~ equalish(X1,X2) ),
apply_substitution1,
[final] ).
cnf(i_0_252,axiom,
( equalish(apply(X3,X1),apply(X3,X2))
| ~ equalish(X1,X2) ),
apply_substitution2,
[final] ).
cnf(i_0_253,axiom,
( member(X1,intersection(X2,X3))
| ~ member(X1,X2)
| ~ member(X1,X3) ),
intersection3,
[final] ).
cnf(i_0_254,axiom,
( single_valued_class(X1)
| ~ subclass(compose(X1,inverse(X1)),identity_relation) ),
single_valued_class2,
[final] ).
cnf(i_0_255,axiom,
( inductive(X1)
| ~ member(null_class,X1)
| ~ subclass(image(successor_relation,X1),X1) ),
inductive3,
[final] ).
cnf(i_0_256,axiom,
subclass(rotate(X1),cross_product(cross_product(universal_class,universal_class),universal_class)),
rotate1,
[final] ).
cnf(i_0_257,axiom,
subclass(flip(X1),cross_product(cross_product(universal_class,universal_class),universal_class)),
flip1,
[final] ).
cnf(i_0_258,axiom,
( equalish(successor(X1),X2)
| ~ member(ordered_pair(X1,X2),successor_relation) ),
successor_relation2,
[final] ).
cnf(i_0_259,axiom,
( subclass(X1,X2)
| ~ member(not_subclass_element(X1,X2),X2) ),
not_subclass_members2,
[final] ).
cnf(i_0_260,axiom,
( member(X1,X2)
| ~ member(X1,intersection(X2,X3)) ),
intersection1,
[final] ).
cnf(i_0_261,axiom,
( member(X1,X3)
| ~ member(X1,intersection(X2,X3)) ),
intersection2,
[final] ).
cnf(i_0_262,axiom,
( member(X1,X2)
| ~ member(ordered_pair(X1,X2),element_relation) ),
element_relation2,
[final] ).
cnf(i_0_263,axiom,
( equalish(X1,null_class)
| member(apply(choice,X1),X1)
| ~ member(X1,universal_class) ),
choice2,
[final] ).
cnf(i_0_264,axiom,
( member(image(X1,X2),universal_class)
| ~ function(X1)
| ~ member(X2,universal_class) ),
replacement,
[final] ).
cnf(i_0_265,axiom,
( equalish(X1,null_class)
| equalish(intersection(X1,regular(X1)),null_class) ),
regularity2,
[final] ).
cnf(i_0_266,axiom,
( member(X1,unordered_pair(X1,X2))
| ~ member(X1,universal_class) ),
unordered_pair2,
[final] ).
cnf(i_0_267,axiom,
( member(X1,unordered_pair(X2,X1))
| ~ member(X1,universal_class) ),
unordered_pair3,
[final] ).
cnf(i_0_268,axiom,
subclass(compose(X1,X2),cross_product(universal_class,universal_class)),
compose1,
[final] ).
cnf(i_0_269,axiom,
( subclass(X1,X3)
| ~ subclass(X1,X2)
| ~ subclass(X2,X3) ),
transitivity_of_subclass,
[final] ).
cnf(i_0_270,axiom,
( subclass(X2,X3)
| ~ equalish(X1,X2)
| ~ subclass(X1,X3) ),
subclass_substitution1,
[final] ).
cnf(i_0_271,axiom,
( subclass(X3,X2)
| ~ equalish(X1,X2)
| ~ subclass(X3,X1) ),
subclass_substitution2,
[final] ).
cnf(i_0_272,axiom,
( member(X2,X3)
| ~ equalish(X1,X2)
| ~ member(X1,X3) ),
member_substitution1,
[final] ).
cnf(i_0_273,axiom,
( member(X3,X2)
| ~ subclass(X1,X2)
| ~ member(X3,X1) ),
subclass_members,
[final] ).
cnf(i_0_274,axiom,
( member(X3,X2)
| ~ equalish(X1,X2)
| ~ member(X3,X1) ),
member_substitution2,
[final] ).
cnf(i_0_275,axiom,
( equalish(X1,X2)
| ~ subclass(X1,X2)
| ~ subclass(X2,X1) ),
subclass_implies_equal,
[final] ).
cnf(i_0_276,axiom,
( equalish(X1,X3)
| ~ equalish(X1,X2)
| ~ equalish(X2,X3) ),
transitivity,
[final] ).
cnf(i_0_277,axiom,
equalish(union(X1,singleton(X1)),successor(X1)),
successor,
[final] ).
cnf(i_0_278,axiom,
( subclass(compose(X1,inverse(X1)),identity_relation)
| ~ single_valued_class(X1) ),
single_valued_class1,
[final] ).
cnf(i_0_279,axiom,
( subclass(compose(X1,inverse(X1)),identity_relation)
| ~ function(X1) ),
function2,
[final] ).
cnf(i_0_280,axiom,
( member(X1,complement(X2))
| member(X1,X2)
| ~ member(X1,universal_class) ),
complement2,
[final] ).
cnf(i_0_281,axiom,
( ~ member(X1,complement(X2))
| ~ member(X1,X2) ),
complement1,
[final] ).
cnf(i_0_282,axiom,
( member(not_subclass_element(X1,X2),X1)
| subclass(X1,X2) ),
not_subclass_members1,
[final] ).
cnf(i_0_283,axiom,
( equalish(sum_class(X1),sum_class(X2))
| ~ equalish(X1,X2) ),
sum_class_substitution1,
[final] ).
cnf(i_0_284,axiom,
( equalish(successor(X1),successor(X2))
| ~ equalish(X1,X2) ),
successor_substitution1,
[final] ).
cnf(i_0_285,axiom,
( equalish(singleton(X1),singleton(X2))
| ~ equalish(X1,X2) ),
singleton_substitution1,
[final] ).
cnf(i_0_286,axiom,
( equalish(second(X1),second(X2))
| ~ equalish(X1,X2) ),
second_substitution1,
[final] ).
cnf(i_0_287,axiom,
( equalish(rotate(X1),rotate(X2))
| ~ equalish(X1,X2) ),
rotate_substitution1,
[final] ).
cnf(i_0_288,axiom,
( equalish(regular(X1),regular(X2))
| ~ equalish(X1,X2) ),
regular_substitution1,
[final] ).
cnf(i_0_289,axiom,
( equalish(range_of(X1),range_of(X2))
| ~ equalish(X1,X2) ),
range_of_substitution1,
[final] ).
cnf(i_0_290,axiom,
( equalish(power_class(X1),power_class(X2))
| ~ equalish(X1,X2) ),
power_class_substitution1,
[final] ).
cnf(i_0_291,axiom,
( equalish(inverse(X1),inverse(X2))
| ~ equalish(X1,X2) ),
inverse_substitution1,
[final] ).
cnf(i_0_292,axiom,
( equalish(flip(X1),flip(X2))
| ~ equalish(X1,X2) ),
flip_substitution1,
[final] ).
cnf(i_0_293,axiom,
( equalish(first(X1),first(X2))
| ~ equalish(X1,X2) ),
first_substitution1,
[final] ).
cnf(i_0_294,axiom,
( equalish(domain_of(X1),domain_of(X2))
| ~ equalish(X1,X2) ),
domain_of_substitution1,
[final] ).
cnf(i_0_295,axiom,
( equalish(diagonalise(X1),diagonalise(X2))
| ~ equalish(X1,X2) ),
diagonalise_substitution1,
[final] ).
cnf(i_0_296,axiom,
( equalish(complement(X1),complement(X2))
| ~ equalish(X1,X2) ),
complement_substitution1,
[final] ).
cnf(i_0_297,axiom,
( equalish(cantor(X1),cantor(X2))
| ~ equalish(X1,X2) ),
cantor_substitution1,
[final] ).
cnf(i_0_298,axiom,
equalish(unordered_pair(X1,X1),singleton(X1)),
singleton_set,
[final] ).
cnf(i_0_299,axiom,
( subclass(range_of(X1),domain_of(domain_of(X1)))
| ~ operation(X1) ),
operation3,
[final] ).
cnf(i_0_300,axiom,
( subclass(image(successor_relation,X1),X1)
| ~ inductive(X1) ),
inductive2,
[final] ).
cnf(i_0_301,axiom,
equalish(intersection(inverse(subset_relation),subset_relation),identity_relation),
identity_relation,
[final] ).
cnf(i_0_302,axiom,
( subclass(X1,cross_product(universal_class,universal_class))
| ~ function(X1) ),
function1,
[final] ).
cnf(i_0_303,axiom,
( member(sum_class(X1),universal_class)
| ~ member(X1,universal_class) ),
sum_class2,
[final] ).
cnf(i_0_304,axiom,
( member(power_class(X1),universal_class)
| ~ member(X1,universal_class) ),
power_class2,
[final] ).
cnf(i_0_305,axiom,
equalish(domain_of(inverse(X1)),range_of(X1)),
range_of,
[final] ).
cnf(i_0_306,axiom,
member(unordered_pair(X1,X2),universal_class),
unordered_pairs_in_universal,
[final] ).
cnf(i_0_307,axiom,
( subclass(X1,X2)
| ~ equalish(X1,X2) ),
equal_implies_subclass1,
[final] ).
cnf(i_0_308,axiom,
( subclass(X2,X1)
| ~ equalish(X1,X2) ),
equal_implies_subclass2,
[final] ).
cnf(i_0_309,axiom,
( equalish(X2,X1)
| ~ equalish(X1,X2) ),
symmetry,
[final] ).
cnf(i_0_310,axiom,
( single_valued_class(X2)
| ~ equalish(X1,X2)
| ~ single_valued_class(X1) ),
single_valued_class_substitution1,
[final] ).
cnf(i_0_311,axiom,
( operation(X2)
| ~ equalish(X1,X2)
| ~ operation(X1) ),
operation_substitution1,
[final] ).
cnf(i_0_312,axiom,
( one_to_one(X2)
| ~ equalish(X1,X2)
| ~ one_to_one(X1) ),
one_to_one_substitution1,
[final] ).
cnf(i_0_313,axiom,
( inductive(X2)
| ~ equalish(X1,X2)
| ~ inductive(X1) ),
inductive_substitution1,
[final] ).
cnf(i_0_314,axiom,
( function(X2)
| ~ equalish(X1,X2)
| ~ function(X1) ),
function_substitution1,
[final] ).
cnf(i_0_315,axiom,
( equalish(X1,null_class)
| member(regular(X1),X1) ),
regularity1,
[final] ).
cnf(i_0_316,axiom,
subclass(successor_relation,cross_product(universal_class,universal_class)),
successor_relation1,
[final] ).
cnf(i_0_317,axiom,
subclass(element_relation,cross_product(universal_class,universal_class)),
element_relation1,
[final] ).
cnf(i_0_318,axiom,
( one_to_one(X1)
| ~ function(inverse(X1))
| ~ function(X1) ),
one_to_one3,
[final] ).
cnf(i_0_319,axiom,
( subclass(omega,X1)
| ~ inductive(X1) ),
omega_is_inductive2,
[final] ).
cnf(i_0_320,axiom,
( member(null_class,X1)
| ~ inductive(X1) ),
inductive1,
[final] ).
cnf(i_0_321,negated_conjecture,
~ equalish(x,x),
prove_reflexivity,
[final] ).
cnf(i_0_322,axiom,
( function(inverse(X1))
| ~ one_to_one(X1) ),
one_to_one2,
[final] ).
cnf(i_0_323,axiom,
subclass(X1,X1),
subclass_is_reflexive,
[final] ).
cnf(i_0_324,axiom,
subclass(X1,universal_class),
class_elements_are_sets,
[final] ).
cnf(i_0_325,axiom,
( function(X1)
| ~ operation(X1) ),
operation1,
[final] ).
cnf(i_0_326,axiom,
( function(X1)
| ~ one_to_one(X1) ),
one_to_one1,
[final] ).
cnf(i_0_327,axiom,
member(omega,universal_class),
omega_in_universal,
[final] ).
cnf(i_0_328,axiom,
inductive(omega),
omega_is_inductive1,
[final] ).
cnf(i_0_329,axiom,
function(choice),
choice1,
[final] ).
cnf(i_0_330,plain,
$false,
inference(scs_inference,[],[i_0_321,i_0_323,i_0_275]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.10/0.27 % Problem : SET055-7 : TPTP v9.2.1. Released v1.0.0.
% 0.10/0.27 % Command : /export/starexec/sandbox/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox/solver/bin/cse --final-prover /export/starexec/sandbox/solver/bin/eprover --proof-time %d --global-time-limit %d
% 0.11/0.46 % Computer : n026.cluster.edu
% 0.11/0.46 % Model : x86_64 x86_64
% 0.11/0.46 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.46 % Memory : 8042.1875MB
% 0.11/0.46 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.46 % CPULimit : 300
% 0.11/0.46 % WCLimit : 300
% 0.11/0.46 % DateTime : Tue May 5 02:08:53 EDT 2026
% 0.11/0.46 % CPUTime :
% 0.11/0.47 % start to proof: theBenchmark
% 0.20/1.78 % Version : CSE_E---1.7
% 0.20/1.78 % Problem : theBenchmark.p
% 0.20/1.78 % SZS status Unsatisfiable for theBenchmark.p
% 0.20/1.78 % SZS output start CNFRefutation
% See solution above
% 0.22/1.81 % Total time : 1.302s
%------------------------------------------------------------------------------