%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : SET021-6 : TPTP v9.3.1. Bugfixed v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% Computer : n005.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 02:46:07 PM UTC 2026
% Result : Unsatisfiable 32.28s 5.31s
% Output : CNFRefutation 32.28s
% Verified :
% SZS Type : Refutation
% Derivation depth : 18
% Number of leaves : 24
% Syntax : Number of formulae : 117 ( 31 unt; 0 def)
% Number of atoms : 235 ( 91 equ)
% Maximal formula atoms : 4 ( 2 avg)
% Number of connectives : 227 ( 109 ~; 118 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 4 avg)
% Maximal term depth : 8 ( 2 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-2 aty)
% Number of functors : 14 ( 14 usr; 4 con; 0-2 aty)
% Number of variables : 181 ( 0 sgn 181 !; 0 ?; 116 :)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X2,X0,X1] :
( member(X2,X1)
| ~ member(X2,X0)
| ~ subclass(X0,X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-0.ax',subclass_members) ).
fof(f2,axiom,
! [X0,X1] :
( subclass(X0,X1)
| member(not_subclass_element(X0,X1),X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-0.ax',not_subclass_members1) ).
fof(f4,axiom,
! [X0] : subclass(X0,universal_class),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-0.ax',class_elements_are_sets) ).
fof(f6,axiom,
! [X0,X1] :
( subclass(X1,X0)
| X0 != X1 ),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-0.ax',equal_implies_subclass2) ).
fof(f7,axiom,
! [X0,X1] :
( X0 = X1
| ~ subclass(X1,X0)
| ~ subclass(X0,X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-0.ax',subclass_implies_equal) ).
fof(f8,axiom,
! [X2,X0,X1] :
( X0 = X2
| X0 = X1
| ~ member(X0,unordered_pair(X1,X2)) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-0.ax',unordered_pair_member) ).
fof(f9,axiom,
! [X0,X1] :
( member(X0,unordered_pair(X0,X1))
| ~ member(X0,universal_class) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-0.ax',unordered_pair2) ).
fof(f11,axiom,
! [X0,X1] : member(unordered_pair(X0,X1),universal_class),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-0.ax',unordered_pairs_in_universal) ).
fof(f12,axiom,
! [X0] : unordered_pair(X0,X0) = singleton(X0),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-0.ax',singleton_set) ).
fof(f13,axiom,
! [X0,X1] : unordered_pair(singleton(X0),unordered_pair(X0,singleton(X1))) = ordered_pair(X0,X1),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-0.ax',ordered_pair) ).
fof(f14,axiom,
! [X2,X3,X0,X1] :
( member(X0,X2)
| ~ member(ordered_pair(X0,X1),cross_product(X2,X3)) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-0.ax',cartesian_product1) ).
fof(f15,axiom,
! [X2,X3,X0,X1] :
( member(X1,X3)
| ~ member(ordered_pair(X0,X1),cross_product(X2,X3)) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-0.ax',cartesian_product2) ).
fof(f16,axiom,
! [X2,X3,X0,X1] :
( member(ordered_pair(X0,X2),cross_product(X1,X3))
| ~ member(X2,X3)
| ~ member(X0,X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-0.ax',cartesian_product3) ).
fof(f17,axiom,
! [X2,X0,X1] :
( ordered_pair(first(X0),second(X0)) = X0
| ~ member(X0,cross_product(X1,X2)) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-0.ax',cartesian_product4) ).
fof(f21,axiom,
! [X2,X0,X1] :
( member(X0,X1)
| ~ member(X0,intersection(X1,X2)) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-0.ax',intersection1) ).
fof(f22,axiom,
! [X2,X0,X1] :
( member(X0,X2)
| ~ member(X0,intersection(X1,X2)) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-0.ax',intersection2) ).
fof(f24,axiom,
! [X0,X1] :
( ~ member(X0,X1)
| ~ member(X0,complement(X1)) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-0.ax',complement1) ).
fof(f67,axiom,
! [X0] :
( member(regular(X0),X0)
| X0 = null_class ),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-0.ax',regularity1) ).
fof(f68,plain,
! [X0] :
( member(regular(X0),X0)
| null_class = X0 ),
inference(reorient_equations,[],[f67]) ).
fof(f69,axiom,
! [X0] :
( intersection(X0,regular(X0)) = null_class
| X0 = null_class ),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-0.ax',regularity2) ).
fof(f70,plain,
! [X0] :
( null_class = intersection(X0,regular(X0))
| null_class = X0 ),
inference(reorient_equations,[],[f69]) ).
fof(f101,negated_conjecture,
member(ordered_pair(u,v),cross_product(universal_class,universal_class)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_unique_1st_and_2nd_in_pair_of_sets2_1) ).
fof(f102,negated_conjecture,
second(ordered_pair(u,v)) != v,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_unique_1st_and_2nd_in_pair_of_sets2_2) ).
fof(f103,plain,
v != second(ordered_pair(u,v)),
inference(reorient_equations,[],[f102]) ).
fof(f108,plain,
! [X0,X1] : ordered_pair(X0,X1) = unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),
inference(definition_unfolding,[],[f13,f12,f12]) ).
fof(f114,plain,
! [X2,X3,X0,X1] :
( member(X0,X2)
| ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),cross_product(X2,X3)) ),
inference(definition_unfolding,[],[f14,f108]) ).
fof(f115,plain,
! [X2,X3,X0,X1] :
( member(X1,X3)
| ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),cross_product(X2,X3)) ),
inference(definition_unfolding,[],[f15,f108]) ).
fof(f116,plain,
! [X2,X3,X0,X1] :
( member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X2,X2))),cross_product(X1,X3))
| ~ member(X2,X3)
| ~ member(X0,X1) ),
inference(definition_unfolding,[],[f16,f108]) ).
fof(f117,plain,
! [X2,X0,X1] :
( unordered_pair(unordered_pair(first(X0),first(X0)),unordered_pair(first(X0),unordered_pair(second(X0),second(X0)))) = X0
| ~ member(X0,cross_product(X1,X2)) ),
inference(definition_unfolding,[],[f17,f108]) ).
fof(f152,plain,
member(unordered_pair(unordered_pair(u,u),unordered_pair(u,unordered_pair(v,v))),cross_product(universal_class,universal_class)),
inference(definition_unfolding,[],[f101,f108]) ).
fof(f153,plain,
v != second(unordered_pair(unordered_pair(u,u),unordered_pair(u,unordered_pair(v,v)))),
inference(definition_unfolding,[],[f103,f108]) ).
fof(f155,plain,
! [X1] : subclass(X1,X1),
inference(equality_resolution,[],[f6]) ).
tcf(c_142,plain,
! [X0: $i,X1: $i,X2: $i] :
( member(X0,X2)
| ~ subclass(X1,X2)
| ~ member(X0,X1) ),
inference(cnf_transformation,[],[f1]) ).
tcf(c_143,plain,
! [X0: $i,X1: $i] :
( subclass(X0,X1)
| member(not_subclass_element(X0,X1),X0) ),
inference(cnf_transformation,[],[f2]) ).
tcf(c_145,plain,
! [X0: $i] : subclass(X0,universal_class),
inference(cnf_transformation,[],[f4]) ).
tcf(c_147,plain,
! [X0: $i] : subclass(X0,X0),
inference(cnf_transformation,[],[f155]) ).
tcf(c_148,plain,
! [X0: $i,X1: $i] :
( ( X0 = X1 )
| ~ subclass(X1,X0)
| ~ subclass(X0,X1) ),
inference(cnf_transformation,[],[f7]) ).
tcf(c_149,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X0 = X2 )
| ( X0 = X1 )
| ~ member(X0,unordered_pair(X1,X2)) ),
inference(cnf_transformation,[],[f8]) ).
tcf(c_150,plain,
! [X0: $i,X1: $i] :
( member(X0,unordered_pair(X0,X1))
| ~ member(X0,universal_class) ),
inference(cnf_transformation,[],[f9]) ).
tcf(c_152,plain,
! [X0: $i,X1: $i] : member(unordered_pair(X0,X1),universal_class),
inference(cnf_transformation,[],[f11]) ).
tcf(c_153,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( member(X0,X2)
| ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),cross_product(X2,X3)) ),
inference(cnf_transformation,[],[f114]) ).
tcf(c_154,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( member(X1,X3)
| ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),cross_product(X2,X3)) ),
inference(cnf_transformation,[],[f115]) ).
tcf(c_155,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X2,X2))),cross_product(X1,X3))
| ~ member(X2,X3)
| ~ member(X0,X1) ),
inference(cnf_transformation,[],[f116]) ).
tcf(c_156,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( unordered_pair(unordered_pair(first(X0),first(X0)),unordered_pair(first(X0),unordered_pair(second(X0),second(X0)))) = X0 )
| ~ member(X0,cross_product(X1,X2)) ),
inference(cnf_transformation,[],[f117]) ).
tcf(c_160,plain,
! [X0: $i,X1: $i,X2: $i] :
( member(X0,X1)
| ~ member(X0,intersection(X1,X2)) ),
inference(cnf_transformation,[],[f21]) ).
tcf(c_161,plain,
! [X0: $i,X1: $i,X2: $i] :
( member(X0,X2)
| ~ member(X0,intersection(X1,X2)) ),
inference(cnf_transformation,[],[f22]) ).
tcf(c_163,plain,
! [X0: $i,X1: $i] :
( ~ member(X0,X1)
| ~ member(X0,complement(X1)) ),
inference(cnf_transformation,[],[f24]) ).
tcf(c_194,plain,
! [X0: $i] :
( member(regular(X0),X0)
| ( X0 = null_class ) ),
inference(cnf_transformation,[],[f68]) ).
tcf(c_195,plain,
! [X0: $i] :
( ( X0 = null_class )
| ( intersection(X0,regular(X0)) = null_class ) ),
inference(cnf_transformation,[],[f70]) ).
tcf(c_217,negated_conjecture,
member(unordered_pair(unordered_pair(u,u),unordered_pair(u,unordered_pair(v,v))),cross_product(universal_class,universal_class)),
inference(cnf_transformation,[],[f152]) ).
tcf(c_218,negated_conjecture,
second(unordered_pair(unordered_pair(u,u),unordered_pair(u,unordered_pair(v,v)))) != v,
inference(cnf_transformation,[],[f153]) ).
tcf(c_219,plain,
subclass(universal_class,universal_class),
inference(instantiation,[status(thm)],[c_147]) ).
tcf(c_245,plain,
( ( universal_class = universal_class )
| ~ subclass(universal_class,universal_class) ),
inference(instantiation,[status(thm)],[c_148]) ).
tcf(c_2096,plain,
! [X0: $i] : X0 = X0,
theory(equality) ).
tcf(c_2098,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X2 = X0 )
| ( X2 != X1 )
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_2102,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( subclass(X0,X2)
| ~ subclass(X1,X3)
| ( X2 != X3 )
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_3580,plain,
! [X0: $i] :
( ( complement(X0) = null_class )
| ~ member(regular(complement(X0)),X0) ),
inference(superposition,[status(thm)],[c_194,c_163]) ).
tcf(c_3581,plain,
( ( complement(universal_class) = null_class )
| ~ member(regular(complement(universal_class)),universal_class) ),
inference(instantiation,[status(thm)],[c_3580]) ).
tcf(c_3646,plain,
! [X0: $i,X1: $i] :
( member(regular(X0),X1)
| ( X0 = null_class )
| ~ subclass(X0,X1) ),
inference(superposition,[status(thm)],[c_194,c_142]) ).
tcf(c_3647,plain,
! [X0: $i] :
( member(unordered_pair(unordered_pair(u,u),unordered_pair(u,unordered_pair(v,v))),X0)
| ~ subclass(cross_product(universal_class,universal_class),X0) ),
inference(superposition,[status(thm)],[c_217,c_142]) ).
tcf(c_3723,plain,
! [X0: $i,X1: $i] :
( member(unordered_pair(unordered_pair(u,u),unordered_pair(u,unordered_pair(v,v))),X1)
| ~ subclass(X0,X1)
| ~ subclass(cross_product(universal_class,universal_class),X0) ),
inference(superposition,[status(thm)],[c_3647,c_142]) ).
tcf(c_3725,plain,
! [X0: $i,X1: $i] :
( member(unordered_pair(unordered_pair(u,u),unordered_pair(u,unordered_pair(v,v))),X0)
| ~ subclass(cross_product(universal_class,universal_class),intersection(X0,X1)) ),
inference(superposition,[status(thm)],[c_3647,c_160]) ).
tcf(c_3849,plain,
! [X0: $i] :
( member(unordered_pair(unordered_pair(u,u),unordered_pair(u,unordered_pair(v,v))),X0)
| ( X0 = null_class )
| ~ subclass(cross_product(universal_class,universal_class),null_class) ),
inference(superposition,[status(thm)],[c_195,c_3725]) ).
tcf(c_3852,plain,
! [X0: $i,X1: $i] :
( member(X0,X1)
| ( X1 = null_class )
| ~ member(X0,null_class) ),
inference(superposition,[status(thm)],[c_195,c_160]) ).
tcf(c_4066,plain,
! [X0: $i] :
( member(unordered_pair(unordered_pair(u,u),unordered_pair(u,unordered_pair(v,v))),X0)
| ~ subclass(universal_class,X0) ),
inference(superposition,[status(thm)],[c_145,c_3723]) ).
tcf(c_4069,plain,
( member(unordered_pair(unordered_pair(u,u),unordered_pair(u,unordered_pair(v,v))),universal_class)
| ~ subclass(universal_class,universal_class) ),
inference(instantiation,[status(thm)],[c_4066]) ).
tcf(c_4093,plain,
! [X0: $i,X1: $i] :
( member(unordered_pair(unordered_pair(u,u),unordered_pair(u,unordered_pair(v,v))),X1)
| ~ subclass(universal_class,X0)
| ~ subclass(X0,X1) ),
inference(superposition,[status(thm)],[c_4066,c_142]) ).
tcf(c_4096,plain,
! [X0: $i] :
( ~ subclass(universal_class,complement(X0))
| ~ member(unordered_pair(unordered_pair(u,u),unordered_pair(u,unordered_pair(v,v))),X0) ),
inference(superposition,[status(thm)],[c_4066,c_163]) ).
tcf(c_4625,plain,
! [X0: $i,X1: $i] :
( subclass(complement(X0),X1)
| ~ member(not_subclass_element(complement(X0),X1),X0) ),
inference(resolution,[status(thm)],[c_163,c_143]) ).
tcf(c_4679,plain,
! [X0: $i,X1: $i] :
( member(X0,universal_class)
| ~ member(X0,X1) ),
inference(resolution,[status(thm)],[c_142,c_145]) ).
tcf(c_4864,plain,
! [X0: $i,X1: $i] :
( subclass(X0,X1)
| member(not_subclass_element(X0,X1),universal_class) ),
inference(resolution,[status(thm)],[c_4679,c_143]) ).
tcf(c_5270,plain,
! [X0: $i] : subclass(complement(universal_class),X0),
inference(resolution,[status(thm)],[c_4625,c_4864]) ).
tcf(c_5395,plain,
! [X0: $i,X1: $i] :
( member(X0,X1)
| ~ member(X0,complement(universal_class)) ),
inference(resolution,[status(thm)],[c_5270,c_142]) ).
tcf(c_5430,plain,
! [X0: $i] :
( member(regular(complement(universal_class)),X0)
| ( complement(universal_class) = null_class ) ),
inference(resolution,[status(thm)],[c_5395,c_194]) ).
tcf(c_5431,plain,
( member(regular(complement(universal_class)),universal_class)
| ( complement(universal_class) = null_class ) ),
inference(instantiation,[status(thm)],[c_5430]) ).
tcf(c_5474,plain,
complement(universal_class) = null_class,
inference(global_subsumption_just,[status(thm)],[c_5430,c_3581,c_5431]) ).
tcf(c_7785,plain,
! [X0: $i,X1: $i,X2: $i] :
( subclass(X0,null_class)
| ~ subclass(X1,X2)
| ( null_class != X2 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_2102]) ).
tcf(c_7786,plain,
( subclass(universal_class,null_class)
| ~ subclass(universal_class,universal_class)
| ( null_class != universal_class )
| ( universal_class != universal_class ) ),
inference(instantiation,[status(thm)],[c_7785]) ).
tcf(c_7850,plain,
! [X0: $i,X1: $i] :
( ( X1 = X0 )
| ( X0 != X1 ) ),
inference(resolution,[status(thm)],[c_2098,c_2096]) ).
tcf(c_7862,plain,
! [X0: $i] :
( ( complement(universal_class) = X0 )
| ( X0 != null_class ) ),
inference(resolution,[status(thm)],[c_2098,c_5474]) ).
tcf(c_8219,plain,
member(v,universal_class),
inference(superposition,[status(thm)],[c_217,c_154]) ).
tcf(c_8325,plain,
null_class = complement(universal_class),
inference(resolution,[status(thm)],[c_7850,c_5474]) ).
tcf(c_8588,plain,
! [X0: $i] :
( ( null_class = X0 )
| ( X0 != complement(universal_class) ) ),
inference(resolution,[status(thm)],[c_8325,c_2098]) ).
tcf(c_9218,plain,
! [X0: $i] :
( ( X0 = complement(universal_class) )
| ( X0 != null_class ) ),
inference(resolution,[status(thm)],[c_7862,c_7850]) ).
tcf(c_9388,plain,
! [X0: $i] :
( ( null_class = X0 )
| ( X0 != null_class ) ),
inference(resolution,[status(thm)],[c_9218,c_8588]) ).
tcf(c_9389,plain,
( ( null_class = universal_class )
| ( universal_class != null_class ) ),
inference(instantiation,[status(thm)],[c_9388]) ).
tcf(c_10418,plain,
~ subclass(universal_class,complement(universal_class)),
inference(superposition,[status(thm)],[c_152,c_4096]) ).
tcf(c_10429,plain,
! [X0: $i] :
( member(unordered_pair(unordered_pair(u,u),unordered_pair(u,unordered_pair(v,v))),universal_class)
| ~ subclass(universal_class,X0) ),
inference(superposition,[status(thm)],[c_145,c_4093]) ).
tcf(c_10443,plain,
member(unordered_pair(unordered_pair(u,u),unordered_pair(u,unordered_pair(v,v))),universal_class),
inference(global_subsumption_just,[status(thm)],[c_10429,c_219,c_4069]) ).
tcf(c_10483,plain,
! [X0: $i] :
( ( complement(X0) = null_class )
| ~ subclass(cross_product(universal_class,universal_class),null_class)
| ~ member(unordered_pair(unordered_pair(u,u),unordered_pair(u,unordered_pair(v,v))),X0) ),
inference(superposition,[status(thm)],[c_3849,c_163]) ).
tcf(c_10647,plain,
( ( complement(universal_class) = null_class )
| ~ subclass(cross_product(universal_class,universal_class),null_class) ),
inference(superposition,[status(thm)],[c_10443,c_10483]) ).
tcf(c_10675,plain,
complement(universal_class) = null_class,
inference(global_subsumption_just,[status(thm)],[c_10647,c_3581,c_5431]) ).
tcf(c_10689,plain,
! [X0: $i] :
( ~ member(X0,null_class)
| ~ member(X0,universal_class) ),
inference(superposition,[status(thm)],[c_10675,c_163]) ).
tcf(c_10691,plain,
~ subclass(universal_class,null_class),
inference(superposition,[status(thm)],[c_10675,c_10418]) ).
tcf(c_11824,plain,
! [X0: $i,X1: $i] :
( ( X1 = second(unordered_pair(unordered_pair(u,u),unordered_pair(u,unordered_pair(v,v)))) )
| ( X1 != X0 )
| ( second(unordered_pair(unordered_pair(u,u),unordered_pair(u,unordered_pair(v,v)))) != X0 ) ),
inference(instantiation,[status(thm)],[c_2098]) ).
tcf(c_11825,plain,
( ( universal_class = second(unordered_pair(unordered_pair(u,u),unordered_pair(u,unordered_pair(v,v)))) )
| ( universal_class != universal_class )
| ( second(unordered_pair(unordered_pair(u,u),unordered_pair(u,unordered_pair(v,v)))) != universal_class ) ),
inference(instantiation,[status(thm)],[c_11824]) ).
tcf(c_11973,plain,
! [X0: $i,X1: $i] :
( ( X0 = null_class )
| ( null_class != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_2098]) ).
tcf(c_15354,plain,
! [X0: $i] :
( ( null_class = second(unordered_pair(unordered_pair(u,u),unordered_pair(u,unordered_pair(v,v)))) )
| ( null_class != X0 )
| ( second(unordered_pair(unordered_pair(u,u),unordered_pair(u,unordered_pair(v,v)))) != X0 ) ),
inference(instantiation,[status(thm)],[c_11824]) ).
tcf(c_15894,plain,
! [X0: $i] :
( ( X0 = null_class )
| ( null_class != second(unordered_pair(unordered_pair(u,u),unordered_pair(u,unordered_pair(v,v)))) )
| ( X0 != second(unordered_pair(unordered_pair(u,u),unordered_pair(u,unordered_pair(v,v)))) ) ),
inference(instantiation,[status(thm)],[c_11973]) ).
tcf(c_15895,plain,
( ( universal_class = null_class )
| ( null_class != second(unordered_pair(unordered_pair(u,u),unordered_pair(u,unordered_pair(v,v)))) )
| ( universal_class != second(unordered_pair(unordered_pair(u,u),unordered_pair(u,unordered_pair(v,v)))) ) ),
inference(instantiation,[status(thm)],[c_15894]) ).
tcf(c_20145,plain,
! [X0: $i,X1: $i] :
( ~ member(X0,null_class)
| ( X1 = null_class ) ),
inference(global_subsumption_just,[status(thm)],[c_3852,c_3852,c_4679,c_10689]) ).
tcf(c_20146,plain,
! [X0: $i,X1: $i] :
( ( X1 = null_class )
| ~ member(X0,null_class) ),
inference(renaming,[status(thm)],[c_20145]) ).
tcf(c_22880,plain,
member(u,universal_class),
inference(superposition,[status(thm)],[c_217,c_153]) ).
tcf(c_22985,plain,
unordered_pair(unordered_pair(first(unordered_pair(unordered_pair(u,u),unordered_pair(u,unordered_pair(v,v)))),first(unordered_pair(unordered_pair(u,u),unordered_pair(u,unordered_pair(v,v))))),unordered_pair(first(unordered_pair(unordered_pair(u,u),unordered_pair(u,unordered_pair(v,v)))),unordered_pair(second(unordered_pair(unordered_pair(u,u),unordered_pair(u,unordered_pair(v,v)))),second(unordered_pair(unordered_pair(u,u),unordered_pair(u,unordered_pair(v,v))))))) = unordered_pair(unordered_pair(u,u),unordered_pair(u,unordered_pair(v,v))),
inference(superposition,[status(thm)],[c_217,c_156]) ).
tcf(c_23015,plain,
! [X0: $i,X1: $i] :
( member(second(unordered_pair(unordered_pair(u,u),unordered_pair(u,unordered_pair(v,v)))),X1)
| ~ member(unordered_pair(unordered_pair(u,u),unordered_pair(u,unordered_pair(v,v))),cross_product(X0,X1)) ),
inference(superposition,[status(thm)],[c_22985,c_154]) ).
tcf(c_23019,plain,
! [X0: $i,X1: $i] :
( member(second(unordered_pair(unordered_pair(u,u),unordered_pair(u,unordered_pair(v,v)))),X1)
| ~ member(v,X1)
| ~ member(u,X0) ),
inference(superposition,[status(thm)],[c_155,c_23015]) ).
tcf(c_23482,plain,
! [X0: $i] :
( member(second(unordered_pair(unordered_pair(u,u),unordered_pair(u,unordered_pair(v,v)))),X0)
| ~ member(v,X0) ),
inference(superposition,[status(thm)],[c_22880,c_23019]) ).
tcf(c_23485,plain,
! [X0: $i,X1: $i] :
( ( second(unordered_pair(unordered_pair(u,u),unordered_pair(u,unordered_pair(v,v)))) = X1 )
| ( second(unordered_pair(unordered_pair(u,u),unordered_pair(u,unordered_pair(v,v)))) = X0 )
| ~ member(v,unordered_pair(X0,X1)) ),
inference(superposition,[status(thm)],[c_23482,c_149]) ).
tcf(c_23927,plain,
! [X0: $i,X1: $i] :
( ~ member(X0,null_class)
| ( X1 = null_class ) ),
inference(global_subsumption_just,[status(thm)],[c_3852,c_20146]) ).
tcf(c_23928,plain,
! [X0: $i,X1: $i] :
( ( X1 = null_class )
| ~ member(X0,null_class) ),
inference(renaming,[status(thm)],[c_23927]) ).
tcf(c_37116,plain,
! [X0: $i] :
( ( second(unordered_pair(unordered_pair(u,u),unordered_pair(u,unordered_pair(v,v)))) = v )
| ( second(unordered_pair(unordered_pair(u,u),unordered_pair(u,unordered_pair(v,v)))) = X0 )
| ~ member(v,universal_class) ),
inference(superposition,[status(thm)],[c_150,c_23485]) ).
tcf(c_37119,plain,
( ( second(unordered_pair(unordered_pair(u,u),unordered_pair(u,unordered_pair(v,v)))) = universal_class )
| ( second(unordered_pair(unordered_pair(u,u),unordered_pair(u,unordered_pair(v,v)))) = v )
| ~ member(v,universal_class) ),
inference(instantiation,[status(thm)],[c_37116]) ).
tcf(c_37799,plain,
! [X0: $i,X1: $i] :
( member(regular(X0),X1)
| ~ subclass(X0,X1) ),
inference(global_subsumption_just,[status(thm)],[c_3646,c_219,c_245,c_218,c_3646,c_7786,c_8219,c_9388,c_9389,c_10691,c_11825,c_15354,c_15895,c_37116,c_37119]) ).
tcf(c_37805,plain,
! [X0: $i,X1: $i,X2: $i] :
( member(regular(X0),X2)
| ~ subclass(X0,intersection(X1,X2)) ),
inference(superposition,[status(thm)],[c_37799,c_161]) ).
tcf(c_38076,plain,
! [X0: $i,X1: $i] : member(regular(intersection(X0,X1)),X1),
inference(superposition,[status(thm)],[c_147,c_37805]) ).
tcf(c_38401,plain,
! [X0: $i] : X0 = null_class,
inference(superposition,[status(thm)],[c_38076,c_23928]) ).
tcf(c_38411,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_38401,c_37119,c_37116,c_15895,c_15354,c_11825,c_10691,c_9389,c_9388,c_8219,c_7786,c_218,c_245,c_219]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SET021-6 : TPTP v9.3.1. Bugfixed v2.1.0.
% 0.00/0.03 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.08/0.36 % Computer : n005.cluster.edu
% 0.08/0.36 % Model : x86_64 x86_64
% 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36 % Memory : 8046.5625MB
% 0.08/0.36 % OS : Linux 6.8.0-71-generic
% 0.08/0.36 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.08/0.36 % DateTime : Thu Sep 24 09:14:03 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.08/0.36 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.08/0.40 Running first-order theorem proving
% 0.08/0.40 Running: /export/starexec/sandbox/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.41
% 0.08/0.41 % ======== iProver multi-core TPTP/SMT =========
% 0.08/0.41
% 0.08/0.42 % Detected problem language: tptp
% 0.08/0.43 % Proving...
% 32.28/5.31 % SZS status Started for theBenchmark.p
% 32.28/5.31 % SZS status Unsatisfiable for theBenchmark.p
% 32.28/5.31
% 32.28/5.31 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 32.28/5.31
% 32.28/5.31 % ------ iProver source info
% 32.28/5.31
% 32.28/5.31 % git: date: 2026-07-19 20:42:38 +0200
% 32.28/5.31 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 32.28/5.31 % git: non_committed_changes: false
% 32.28/5.31
% 32.28/5.31 % ------ Parsing...% successful
% 32.28/5.31
% 32.28/5.31
% 32.28/5.31 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 32.28/5.31
% 32.28/5.31 % ------ Preprocessing... sup_sim: 0 sf_s rm: 1 0s sf_e pe_s pe:1:0s pe:2:0s pe_e sup_sim: 0 sf_s rm: 2 0s sf_e pe_s pe_e %
% 32.28/5.31
% 32.28/5.31 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 32.28/5.31
% 32.28/5.31 % ------ Preprocessing... sf_s rm: 1 0s sf_e sf_s rm: 0 0s sf_e
% 32.28/5.31 % ------ Proving...
% 32.28/5.31 % ------ Problem Properties
% 32.28/5.31
% 32.28/5.31 %
% 32.28/5.31 % clauses 69
% 32.28/5.31 % conjectures 2
% 32.28/5.31 % EPR 12
% 32.28/5.31 % Horn 61
% 32.28/5.31 % unary 17
% 32.28/5.31 % binary 32
% 32.28/5.31 % lits 147
% 32.28/5.31 % lits eq 21
% 32.28/5.31 % fd_pure 0
% 32.28/5.31 % fd_pseudo 0
% 32.28/5.31 % fd_cond 3
% 32.28/5.31 % fd_pseudo_cond 3
% 32.28/5.31 % AC symbols 0
% 32.28/5.31
% 32.28/5.31 % ------ Input Options Time Limit: Unbounded
% 32.28/5.31
% 32.28/5.31
% 32.28/5.31 % ------
% 32.28/5.31 % Current options:
% 32.28/5.31 % ------
% 32.28/5.31
% 32.28/5.31
% 32.28/5.31 %
% 32.28/5.31
% 32.28/5.31 % ------ Proving...
% 32.28/5.31 %
% 32.28/5.31
% 32.28/5.31 % SZS status Unsatisfiable for theBenchmark.p
% 32.28/5.31
% 32.28/5.31 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 32.28/5.31
% 32.28/5.31
%------------------------------------------------------------------------------