%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : SET512-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 : n007.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:47:21 PM UTC 2026
% Result : Unsatisfiable 103.63s 15.00s
% Output : CNFRefutation 103.63s
% Verified :
% SZS Type : Refutation
% Derivation depth : 33
% Number of leaves : 27
% Syntax : Number of formulae : 189 ( 52 unt; 6 def)
% Number of atoms : 657 ( 140 equ)
% Maximal formula atoms : 4 ( 3 avg)
% Number of connectives : 313 ( 135 ~; 178 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 10 ( 8 usr; 7 prp; 0-2 aty)
% Number of functors : 10 ( 10 usr; 3 con; 0-2 aty)
% Number of variables : 211 ( 0 sgn 211 !; 0 ?; 170 :)
% 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(f3,axiom,
! [X0,X1] :
( subclass(X0,X1)
| ~ member(not_subclass_element(X0,X1),X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-0.ax',not_subclass_members2) ).
fof(f4,axiom,
! [X0] : subclass(X0,universal_class),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-0.ax',class_elements_are_sets) ).
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(f10,axiom,
! [X0,X1] :
( member(X0,unordered_pair(X1,X0))
| ~ member(X0,universal_class) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-0.ax',unordered_pair3) ).
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(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(f23,axiom,
! [X2,X0,X1] :
( member(X0,intersection(X1,X2))
| ~ member(X0,X2)
| ~ member(X0,X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-0.ax',intersection3) ).
fof(f24,axiom,
! [X0,X1] :
( ~ member(X0,X1)
| ~ member(X0,complement(X1)) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-0.ax',complement1) ).
fof(f25,axiom,
! [X0,X1] :
( member(X0,X1)
| member(X0,complement(X1))
| ~ member(X0,universal_class) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-0.ax',complement2) ).
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(f122,negated_conjecture,
unordered_pair(null_class,singleton(singleton(y))) != ordered_pair(universal_class,y),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_corollary_2_to_property_1_of_ordered_pair_1) ).
fof(f127,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(f185,plain,
unordered_pair(null_class,unordered_pair(unordered_pair(y,y),unordered_pair(y,y))) != unordered_pair(unordered_pair(universal_class,universal_class),unordered_pair(universal_class,unordered_pair(y,y))),
inference(definition_unfolding,[],[f122,f12,f12,f127]) ).
tcf(c_162,plain,
! [X0: $i,X1: $i,X2: $i] :
( member(X2,X1)
| ~ member(X2,X0)
| ~ subclass(X0,X1) ),
inference(cnf_transformation,[],[f1]) ).
tcf(c_163,plain,
! [X0: $i,X1: $i] :
( subclass(X0,X1)
| member(not_subclass_element(X0,X1),X0) ),
inference(cnf_transformation,[],[f2]) ).
tcf(c_164,plain,
! [X0: $i,X1: $i] :
( subclass(X0,X1)
| ~ member(not_subclass_element(X0,X1),X1) ),
inference(cnf_transformation,[],[f3]) ).
tcf(c_165,plain,
! [X0: $i] : subclass(X0,universal_class),
inference(cnf_transformation,[],[f4]) ).
tcf(c_168,plain,
! [X0: $i,X1: $i] :
( ( X0 = X1 )
| ~ subclass(X1,X0)
| ~ subclass(X0,X1) ),
inference(cnf_transformation,[],[f7]) ).
tcf(c_169,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X0 = X2 )
| ( X0 = X1 )
| ~ member(X0,unordered_pair(X1,X2)) ),
inference(cnf_transformation,[],[f8]) ).
tcf(c_170,plain,
! [X0: $i,X1: $i] :
( member(X0,unordered_pair(X0,X1))
| ~ member(X0,universal_class) ),
inference(cnf_transformation,[],[f9]) ).
tcf(c_171,plain,
! [X0: $i,X1: $i] :
( member(X0,unordered_pair(X1,X0))
| ~ member(X0,universal_class) ),
inference(cnf_transformation,[],[f10]) ).
tcf(c_172,plain,
! [X0: $i,X1: $i] : member(unordered_pair(X0,X1),universal_class),
inference(cnf_transformation,[],[f11]) ).
tcf(c_180,plain,
! [X0: $i,X1: $i,X2: $i] :
( member(X0,X1)
| ~ member(X0,intersection(X1,X2)) ),
inference(cnf_transformation,[],[f21]) ).
tcf(c_181,plain,
! [X0: $i,X1: $i,X2: $i] :
( member(X0,X2)
| ~ member(X0,intersection(X1,X2)) ),
inference(cnf_transformation,[],[f22]) ).
tcf(c_182,plain,
! [X0: $i,X1: $i,X2: $i] :
( member(X0,intersection(X1,X2))
| ~ member(X0,X2)
| ~ member(X0,X1) ),
inference(cnf_transformation,[],[f23]) ).
tcf(c_183,plain,
! [X0: $i,X1: $i] :
( ~ member(X0,X1)
| ~ member(X0,complement(X1)) ),
inference(cnf_transformation,[],[f24]) ).
tcf(c_184,plain,
! [X0: $i,X1: $i] :
( member(X0,X1)
| member(X0,complement(X1))
| ~ member(X0,universal_class) ),
inference(cnf_transformation,[],[f25]) ).
tcf(c_214,plain,
! [X0: $i] :
( member(regular(X0),X0)
| ( X0 = null_class ) ),
inference(cnf_transformation,[],[f68]) ).
tcf(c_215,plain,
! [X0: $i] :
( ( X0 = null_class )
| ( intersection(X0,regular(X0)) = null_class ) ),
inference(cnf_transformation,[],[f70]) ).
tcf(c_255,negated_conjecture,
unordered_pair(unordered_pair(universal_class,universal_class),unordered_pair(universal_class,unordered_pair(y,y))) != unordered_pair(null_class,unordered_pair(unordered_pair(y,y),unordered_pair(y,y))),
inference(cnf_transformation,[],[f185]) ).
tcf(c_2974,definition,
iPr_def_10 = unordered_pair(universal_class,universal_class),
introduced(definition,[new_symbols(definition,[iPr_def_10])],[]) ).
tcf(c_2975,definition,
iPr_def_11 = unordered_pair(y,y),
introduced(definition,[new_symbols(definition,[iPr_def_11])],[]) ).
tcf(c_2976,definition,
iPr_def_12 = unordered_pair(universal_class,iPr_def_11),
introduced(definition,[new_symbols(definition,[iPr_def_12])],[]) ).
tcf(c_2977,definition,
iPr_def_13 = unordered_pair(iPr_def_10,iPr_def_12),
introduced(definition,[new_symbols(definition,[iPr_def_13])],[]) ).
tcf(c_2978,definition,
iPr_def_14 = unordered_pair(iPr_def_11,iPr_def_11),
introduced(definition,[new_symbols(definition,[iPr_def_14])],[]) ).
tcf(c_2979,definition,
iPr_def_15 = unordered_pair(null_class,iPr_def_14),
introduced(definition,[new_symbols(definition,[iPr_def_15])],[]) ).
tcf(c_2980,negated_conjecture,
iPr_def_13 != iPr_def_15,
inference(demodulation,[status(thm)],[c_255,c_2978,c_2979,c_2975,c_2976,c_2974,c_2977]) ).
tcf(c_2983,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X2 = X0 )
| ( X2 != X1 )
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_2984,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( unordered_pair(X0,X2) = unordered_pair(X1,X3) )
| ( X2 != X3 )
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_3841,plain,
member(iPr_def_11,universal_class),
inference(superposition,[status(thm)],[c_2975,c_172]) ).
tcf(c_3887,plain,
( member(universal_class,iPr_def_10)
| ~ member(universal_class,universal_class) ),
inference(superposition,[status(thm)],[c_2974,c_170]) ).
tcf(c_3916,plain,
( member(iPr_def_11,iPr_def_12)
| ~ member(iPr_def_11,universal_class) ),
inference(superposition,[status(thm)],[c_2976,c_171]) ).
tcf(c_3922,plain,
member(iPr_def_11,iPr_def_12),
inference(forward_subsumption_resolution,[status(thm)],[c_3916,c_3841]) ).
tcf(c_3975,plain,
! [X0: $i,X1: $i] :
( subclass(complement(X0),X1)
| ~ member(not_subclass_element(complement(X0),X1),X0) ),
inference(superposition,[status(thm)],[c_163,c_183]) ).
tcf(c_3976,plain,
! [X0: $i] :
( ( complement(X0) = null_class )
| ~ member(regular(complement(X0)),X0) ),
inference(superposition,[status(thm)],[c_214,c_183]) ).
tcf(c_3981,plain,
( ( complement(universal_class) = null_class )
| ~ member(regular(complement(universal_class)),universal_class) ),
inference(instantiation,[status(thm)],[c_3976]) ).
tcf(c_4049,plain,
! [X0: $i,X1: $i] :
( member(X0,universal_class)
| ~ member(X0,X1) ),
inference(superposition,[status(thm)],[c_165,c_162]) ).
tcf(c_4170,plain,
! [X0: $i,X1: $i] :
( subclass(X0,X1)
| member(not_subclass_element(X0,X1),universal_class) ),
inference(superposition,[status(thm)],[c_163,c_4049]) ).
tcf(c_4176,plain,
! [X0: $i] :
( member(regular(X0),universal_class)
| ( X0 = null_class ) ),
inference(superposition,[status(thm)],[c_214,c_4049]) ).
tcf(c_4343,plain,
! [X0: $i] :
( ( X0 = universal_class )
| ~ member(X0,iPr_def_10) ),
inference(superposition,[status(thm)],[c_2974,c_169]) ).
tcf(c_4346,plain,
! [X0: $i] :
( ( X0 = iPr_def_11 )
| ~ member(X0,iPr_def_14) ),
inference(superposition,[status(thm)],[c_2978,c_169]) ).
tcf(c_4407,plain,
! [X0: $i] :
( subclass(iPr_def_10,X0)
| ( not_subclass_element(iPr_def_10,X0) = universal_class ) ),
inference(superposition,[status(thm)],[c_163,c_4343]) ).
tcf(c_4408,plain,
( ( null_class = iPr_def_10 )
| ( regular(iPr_def_10) = universal_class ) ),
inference(superposition,[status(thm)],[c_214,c_4343]) ).
tcf(c_4667,plain,
! [X0: $i] :
( ( iPr_def_13 = iPr_def_15 )
| ( iPr_def_15 != X0 )
| ( iPr_def_13 != X0 ) ),
inference(instantiation,[status(thm)],[c_2983]) ).
tcf(c_4701,plain,
( member(universal_class,universal_class)
| ( null_class = iPr_def_10 ) ),
inference(superposition,[status(thm)],[c_4408,c_4176]) ).
tcf(c_4702,plain,
( member(universal_class,iPr_def_10)
| ( null_class = iPr_def_10 ) ),
inference(superposition,[status(thm)],[c_4408,c_214]) ).
tcf(c_4703,plain,
( ( null_class = iPr_def_10 )
| ( intersection(iPr_def_10,universal_class) = null_class ) ),
inference(superposition,[status(thm)],[c_4408,c_215]) ).
tcf(c_4952,plain,
! [X0: $i] :
( member(X0,null_class)
| ( null_class = iPr_def_10 )
| ~ member(X0,iPr_def_10)
| ~ member(X0,universal_class) ),
inference(superposition,[status(thm)],[c_4703,c_182]) ).
tcf(c_4967,plain,
( member(universal_class,null_class)
| ( null_class = iPr_def_10 )
| ~ member(universal_class,iPr_def_10)
| ~ member(universal_class,universal_class) ),
inference(instantiation,[status(thm)],[c_4952]) ).
tcf(c_5002,plain,
! [X0: $i,X1: $i] :
( ( iPr_def_13 = X0 )
| ( iPr_def_13 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_2983]) ).
tcf(c_5026,plain,
! [X0: $i] : subclass(complement(universal_class),X0),
inference(superposition,[status(thm)],[c_4170,c_3975]) ).
tcf(c_5047,plain,
! [X0: $i] :
( ( complement(universal_class) = X0 )
| ~ subclass(X0,complement(universal_class)) ),
inference(superposition,[status(thm)],[c_5026,c_168]) ).
tcf(c_5048,plain,
! [X0: $i,X1: $i] :
( member(X0,X1)
| ~ member(X0,complement(universal_class)) ),
inference(superposition,[status(thm)],[c_5026,c_162]) ).
tcf(c_5061,plain,
! [X0: $i] :
( member(regular(complement(universal_class)),X0)
| ( complement(universal_class) = null_class ) ),
inference(superposition,[status(thm)],[c_214,c_5048]) ).
tcf(c_5064,plain,
( member(regular(complement(universal_class)),universal_class)
| ( complement(universal_class) = null_class ) ),
inference(instantiation,[status(thm)],[c_5061]) ).
tcf(c_5206,plain,
complement(universal_class) = null_class,
inference(global_subsumption_just,[status(thm)],[c_5061,c_3981,c_5064]) ).
tcf(c_5208,plain,
! [X0: $i] :
( ( X0 = null_class )
| ~ subclass(X0,null_class) ),
inference(demodulation,[status(thm)],[c_5047,c_5206]) ).
tcf(c_5209,plain,
! [X0: $i,X1: $i] :
( member(X0,X1)
| ~ member(X0,null_class) ),
inference(demodulation,[status(thm)],[c_5048,c_5206]) ).
tcf(c_5221,plain,
! [X0: $i] :
( ~ member(X0,universal_class)
| ~ member(X0,null_class) ),
inference(superposition,[status(thm)],[c_5206,c_183]) ).
tcf(c_5230,plain,
! [X0: $i] : ~ member(X0,null_class),
inference(global_subsumption_just,[status(thm)],[c_5209,c_4049,c_5209,c_5221]) ).
tcf(c_5232,plain,
~ member(universal_class,null_class),
inference(instantiation,[status(thm)],[c_5230]) ).
tcf(c_5241,plain,
( ( null_class = iPr_def_10 )
| ( not_subclass_element(iPr_def_10,null_class) = universal_class ) ),
inference(superposition,[status(thm)],[c_4407,c_5208]) ).
tcf(c_5263,plain,
null_class = iPr_def_10,
inference(global_subsumption_just,[status(thm)],[c_5241,c_4702,c_4701,c_4967,c_5232]) ).
tcf(c_5267,plain,
! [X0: $i] : ~ member(X0,iPr_def_10),
inference(demodulation,[status(thm)],[c_5230,c_5263]) ).
tcf(c_5289,plain,
! [X0: $i] :
( member(regular(X0),X0)
| ( X0 = iPr_def_10 ) ),
inference(demodulation,[status(thm)],[c_214,c_5263]) ).
tcf(c_5334,plain,
~ member(universal_class,universal_class),
inference(backward_subsumption_resolution,[status(thm)],[c_3887,c_5267]) ).
tcf(c_5606,plain,
! [X0: $i,X1: $i] :
( member(regular(intersection(X0,X1)),X1)
| ( intersection(X0,X1) = iPr_def_10 ) ),
inference(superposition,[status(thm)],[c_5289,c_181]) ).
tcf(c_5607,plain,
! [X0: $i,X1: $i] :
( member(regular(intersection(X0,X1)),X0)
| ( intersection(X0,X1) = iPr_def_10 ) ),
inference(superposition,[status(thm)],[c_5289,c_180]) ).
tcf(c_8668,plain,
! [X0: $i] :
( ( intersection(X0,iPr_def_14) = iPr_def_10 )
| ( regular(intersection(X0,iPr_def_14)) = iPr_def_11 ) ),
inference(superposition,[status(thm)],[c_5606,c_4346]) ).
tcf(c_9128,plain,
! [X0: $i] :
( ( X0 = universal_class )
| ~ member(X0,iPr_def_10) ),
inference(superposition,[status(thm)],[c_2974,c_169]) ).
tcf(c_9425,plain,
! [X0: $i] :
( ( iPr_def_13 = X0 )
| ( iPr_def_13 != unordered_pair(iPr_def_10,iPr_def_12) )
| ( X0 != unordered_pair(iPr_def_10,iPr_def_12) ) ),
inference(instantiation,[status(thm)],[c_5002]) ).
tcf(c_9439,plain,
! [X0: $i] : ~ member(X0,iPr_def_10),
inference(global_subsumption_just,[status(thm)],[c_9128,c_5267]) ).
tcf(c_9442,plain,
null_class = iPr_def_10,
inference(superposition,[status(thm)],[c_214,c_9439]) ).
tcf(c_20388,plain,
( ( iPr_def_13 = iPr_def_15 )
| ( iPr_def_15 != unordered_pair(null_class,iPr_def_14) )
| ( iPr_def_13 != unordered_pair(null_class,iPr_def_14) ) ),
inference(instantiation,[status(thm)],[c_4667]) ).
tcf(c_23184,plain,
! [X0: $i] :
( member(iPr_def_11,X0)
| ( intersection(X0,iPr_def_14) = iPr_def_10 ) ),
inference(superposition,[status(thm)],[c_8668,c_5607]) ).
tcf(c_23242,plain,
! [X0: $i] :
( ( intersection(complement(X0),iPr_def_14) = iPr_def_10 )
| ~ member(iPr_def_11,X0) ),
inference(superposition,[status(thm)],[c_23184,c_183]) ).
tcf(c_23454,plain,
( ( iPr_def_13 = unordered_pair(null_class,iPr_def_14) )
| ( iPr_def_13 != unordered_pair(iPr_def_10,iPr_def_12) )
| ( unordered_pair(null_class,iPr_def_14) != unordered_pair(iPr_def_10,iPr_def_12) ) ),
inference(instantiation,[status(thm)],[c_9425]) ).
tcf(c_24568,plain,
! [X0: $i] :
( member(iPr_def_11,X0)
| ( intersection(complement(complement(X0)),iPr_def_14) = iPr_def_10 )
| ~ member(iPr_def_11,universal_class) ),
inference(superposition,[status(thm)],[c_184,c_23242]) ).
tcf(c_24571,plain,
intersection(complement(iPr_def_12),iPr_def_14) = iPr_def_10,
inference(superposition,[status(thm)],[c_3922,c_23242]) ).
tcf(c_24668,plain,
! [X0: $i] :
( member(iPr_def_11,X0)
| ( intersection(complement(complement(X0)),iPr_def_14) = iPr_def_10 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_24568,c_3841]) ).
tcf(c_24908,plain,
intersection(complement(complement(iPr_def_10)),iPr_def_14) = iPr_def_10,
inference(superposition,[status(thm)],[c_24668,c_5267]) ).
tcf(c_25182,plain,
! [X0: $i] :
( member(X0,iPr_def_10)
| ~ member(X0,iPr_def_14)
| ~ member(X0,complement(iPr_def_12)) ),
inference(superposition,[status(thm)],[c_24571,c_182]) ).
tcf(c_25193,plain,
! [X0: $i] :
( ~ member(X0,iPr_def_14)
| ~ member(X0,complement(iPr_def_12)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_25182,c_5267]) ).
tcf(c_25213,plain,
! [X0: $i] :
( member(X0,iPr_def_10)
| ~ member(X0,iPr_def_14)
| ~ member(X0,complement(complement(iPr_def_10))) ),
inference(superposition,[status(thm)],[c_24908,c_182]) ).
tcf(c_25224,plain,
! [X0: $i] :
( ~ member(X0,iPr_def_14)
| ~ member(X0,complement(complement(iPr_def_10))) ),
inference(forward_subsumption_resolution,[status(thm)],[c_25213,c_5267]) ).
tcf(c_25237,plain,
! [X0: $i] :
( member(X0,iPr_def_12)
| ~ member(X0,iPr_def_14)
| ~ member(X0,universal_class) ),
inference(superposition,[status(thm)],[c_184,c_25193]) ).
tcf(c_25704,plain,
! [X0: $i] :
( member(X0,iPr_def_12)
| ~ member(X0,iPr_def_14) ),
inference(forward_subsumption_resolution,[status(thm)],[c_25237,c_4049]) ).
tcf(c_25711,plain,
! [X0: $i] :
( subclass(iPr_def_14,X0)
| member(not_subclass_element(iPr_def_14,X0),iPr_def_12) ),
inference(superposition,[status(thm)],[c_163,c_25704]) ).
tcf(c_25904,plain,
subclass(iPr_def_14,iPr_def_12),
inference(superposition,[status(thm)],[c_25711,c_164]) ).
tcf(c_26064,plain,
! [X0: $i] :
( member(X0,complement(iPr_def_10))
| ~ member(X0,iPr_def_14)
| ~ member(X0,universal_class) ),
inference(superposition,[status(thm)],[c_184,c_25224]) ).
tcf(c_26288,plain,
! [X0: $i] :
( member(X0,complement(iPr_def_10))
| ~ member(X0,iPr_def_14) ),
inference(forward_subsumption_resolution,[status(thm)],[c_26064,c_4049]) ).
tcf(c_26297,plain,
! [X0: $i] :
( member(X0,universal_class)
| ~ member(X0,iPr_def_14) ),
inference(superposition,[status(thm)],[c_26288,c_4049]) ).
tcf(c_36129,plain,
( ( unordered_pair(null_class,iPr_def_14) = unordered_pair(iPr_def_10,iPr_def_12) )
| ( iPr_def_14 != iPr_def_12 )
| ( null_class != iPr_def_10 ) ),
inference(instantiation,[status(thm)],[c_2984]) ).
tcf(c_38742,plain,
member(iPr_def_11,universal_class),
inference(superposition,[status(thm)],[c_2975,c_172]) ).
tcf(c_38764,plain,
! [X0: $i] :
( member(regular(X0),X0)
| ( X0 = iPr_def_10 ) ),
inference(light_normalisation,[status(thm)],[c_214,c_9442]) ).
tcf(c_38787,plain,
( member(universal_class,iPr_def_10)
| ~ member(universal_class,universal_class) ),
inference(superposition,[status(thm)],[c_2974,c_170]) ).
tcf(c_38807,plain,
( member(iPr_def_11,iPr_def_12)
| ~ member(iPr_def_11,universal_class) ),
inference(superposition,[status(thm)],[c_2976,c_171]) ).
tcf(c_38813,plain,
member(iPr_def_11,iPr_def_12),
inference(forward_subsumption_resolution,[status(thm)],[c_38807,c_38742]) ).
tcf(c_38819,plain,
! [X0: $i,X1: $i] :
( member(regular(intersection(X0,X1)),X0)
| ( intersection(X0,X1) = iPr_def_10 ) ),
inference(superposition,[status(thm)],[c_38764,c_180]) ).
tcf(c_38828,plain,
! [X0: $i,X1: $i,X2: $i] :
( subclass(intersection(X0,X1),X2)
| member(not_subclass_element(intersection(X0,X1),X2),X1) ),
inference(superposition,[status(thm)],[c_163,c_181]) ).
tcf(c_38829,plain,
! [X0: $i,X1: $i] :
( member(regular(intersection(X0,X1)),X1)
| ( intersection(X0,X1) = iPr_def_10 ) ),
inference(superposition,[status(thm)],[c_38764,c_181]) ).
tcf(c_38834,plain,
~ member(universal_class,universal_class),
inference(global_subsumption_just,[status(thm)],[c_38787,c_5334]) ).
tcf(c_38888,plain,
! [X0: $i,X1: $i] :
( member(X0,universal_class)
| ~ member(X0,X1) ),
inference(superposition,[status(thm)],[c_165,c_162]) ).
tcf(c_38994,plain,
! [X0: $i] :
( member(regular(X0),universal_class)
| ( X0 = iPr_def_10 ) ),
inference(superposition,[status(thm)],[c_38764,c_38888]) ).
tcf(c_39259,plain,
! [X0: $i] :
( ( X0 = universal_class )
| ~ member(X0,iPr_def_10) ),
inference(superposition,[status(thm)],[c_2974,c_169]) ).
tcf(c_39262,plain,
! [X0: $i] :
( ( X0 = iPr_def_11 )
| ~ member(X0,iPr_def_14) ),
inference(superposition,[status(thm)],[c_2978,c_169]) ).
tcf(c_39307,plain,
! [X0: $i] : ~ member(X0,iPr_def_10),
inference(global_subsumption_just,[status(thm)],[c_39259,c_5267]) ).
tcf(c_39309,plain,
! [X0: $i] : subclass(iPr_def_10,X0),
inference(superposition,[status(thm)],[c_163,c_39307]) ).
tcf(c_39311,plain,
! [X0: $i] :
( ( X0 = iPr_def_10 )
| ~ subclass(X0,iPr_def_10) ),
inference(superposition,[status(thm)],[c_39309,c_168]) ).
tcf(c_49429,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( intersection(unordered_pair(X0,X1),X2) = iPr_def_10 )
| ( regular(intersection(unordered_pair(X0,X1),X2)) = X1 )
| ( regular(intersection(unordered_pair(X0,X1),X2)) = X0 ) ),
inference(superposition,[status(thm)],[c_38819,c_169]) ).
tcf(c_49446,plain,
! [X0: $i] :
( ( intersection(iPr_def_14,X0) = iPr_def_10 )
| ( regular(intersection(iPr_def_14,X0)) = iPr_def_11 ) ),
inference(superposition,[status(thm)],[c_38819,c_39262]) ).
tcf(c_51098,plain,
! [X0: $i,X1: $i] : subclass(intersection(X0,X1),X1),
inference(superposition,[status(thm)],[c_38828,c_164]) ).
tcf(c_51102,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( subclass(intersection(X0,intersection(X1,X2)),X3)
| member(not_subclass_element(intersection(X0,intersection(X1,X2)),X3),X2) ),
inference(superposition,[status(thm)],[c_38828,c_181]) ).
tcf(c_52934,plain,
! [X0: $i] : intersection(X0,iPr_def_10) = iPr_def_10,
inference(superposition,[status(thm)],[c_51098,c_39311]) ).
tcf(c_54546,plain,
! [X0: $i] :
( member(iPr_def_11,X0)
| ( intersection(iPr_def_14,X0) = iPr_def_10 ) ),
inference(superposition,[status(thm)],[c_49446,c_38829]) ).
tcf(c_55032,plain,
! [X0: $i] :
( ( intersection(iPr_def_14,complement(X0)) = iPr_def_10 )
| ~ member(iPr_def_11,X0) ),
inference(superposition,[status(thm)],[c_54546,c_183]) ).
tcf(c_61500,plain,
( ( iPr_def_14 = iPr_def_12 )
| ~ subclass(iPr_def_14,iPr_def_12)
| ~ subclass(iPr_def_12,iPr_def_14) ),
inference(instantiation,[status(thm)],[c_168]) ).
tcf(c_66788,plain,
! [X0: $i] :
( ( regular(intersection(iPr_def_12,X0)) = universal_class )
| ( intersection(unordered_pair(universal_class,iPr_def_11),X0) = iPr_def_10 )
| ( regular(intersection(unordered_pair(universal_class,iPr_def_11),X0)) = iPr_def_11 ) ),
inference(superposition,[status(thm)],[c_2976,c_49429]) ).
tcf(c_66854,plain,
! [X0: $i] :
( ( intersection(iPr_def_12,X0) = iPr_def_10 )
| ( regular(intersection(iPr_def_12,X0)) = iPr_def_11 )
| ( regular(intersection(iPr_def_12,X0)) = universal_class ) ),
inference(light_normalisation,[status(thm)],[c_66788,c_2976]) ).
tcf(c_67486,plain,
intersection(iPr_def_14,complement(iPr_def_12)) = iPr_def_10,
inference(superposition,[status(thm)],[c_38813,c_55032]) ).
tcf(c_75708,plain,
! [X0: $i] :
( member(X0,iPr_def_10)
| ~ member(X0,iPr_def_14)
| ~ member(X0,complement(iPr_def_12)) ),
inference(superposition,[status(thm)],[c_67486,c_182]) ).
tcf(c_75716,plain,
! [X0: $i] :
( ~ member(X0,iPr_def_14)
| ~ member(X0,complement(iPr_def_12)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_75708,c_39307]) ).
tcf(c_78751,plain,
! [X0: $i] :
( member(X0,iPr_def_12)
| ~ member(X0,iPr_def_14)
| ~ member(X0,universal_class) ),
inference(superposition,[status(thm)],[c_184,c_75716]) ).
tcf(c_84893,plain,
! [X0: $i] :
( member(X0,iPr_def_12)
| ~ member(X0,iPr_def_14) ),
inference(global_subsumption_just,[status(thm)],[c_78751,c_25237,c_26297]) ).
tcf(c_113389,plain,
! [X0: $i] :
( member(universal_class,universal_class)
| ( intersection(iPr_def_12,X0) = iPr_def_10 )
| ( regular(intersection(iPr_def_12,X0)) = iPr_def_11 ) ),
inference(superposition,[status(thm)],[c_66854,c_38994]) ).
tcf(c_113405,plain,
! [X0: $i] :
( ( intersection(iPr_def_12,X0) = iPr_def_10 )
| ( regular(intersection(iPr_def_12,X0)) = iPr_def_11 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_113389,c_38834]) ).
tcf(c_133789,plain,
! [X0: $i,X1: $i,X2: $i] : subclass(intersection(X0,intersection(X1,X2)),X2),
inference(superposition,[status(thm)],[c_51102,c_164]) ).
tcf(c_142796,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( member(X0,X3)
| ~ member(X0,intersection(X1,intersection(X2,X3))) ),
inference(superposition,[status(thm)],[c_133789,c_162]) ).
tcf(c_222007,plain,
! [X0: $i,X1: $i] :
( member(X0,iPr_def_10)
| ~ member(X0,intersection(X1,iPr_def_10)) ),
inference(superposition,[status(thm)],[c_52934,c_142796]) ).
tcf(c_222054,plain,
! [X0: $i,X1: $i] : ~ member(X0,intersection(X1,iPr_def_10)),
inference(forward_subsumption_resolution,[status(thm)],[c_222007,c_39307]) ).
tcf(c_267652,plain,
member(iPr_def_11,universal_class),
inference(superposition,[status(thm)],[c_2975,c_172]) ).
tcf(c_267685,plain,
! [X0: $i] :
( member(regular(X0),X0)
| ( X0 = iPr_def_10 ) ),
inference(light_normalisation,[status(thm)],[c_214,c_9442]) ).
tcf(c_267692,plain,
! [X0: $i] : intersection(X0,iPr_def_10) = iPr_def_10,
inference(superposition,[status(thm)],[c_267685,c_222054]) ).
tcf(c_267694,plain,
! [X0: $i] : ~ member(X0,iPr_def_10),
inference(demodulation,[status(thm)],[c_222054,c_267692]) ).
tcf(c_267708,plain,
( member(iPr_def_11,iPr_def_14)
| ~ member(iPr_def_11,universal_class) ),
inference(superposition,[status(thm)],[c_2978,c_170]) ).
tcf(c_267711,plain,
member(iPr_def_11,iPr_def_14),
inference(forward_subsumption_resolution,[status(thm)],[c_267708,c_267652]) ).
tcf(c_267733,plain,
( member(iPr_def_11,iPr_def_12)
| ~ member(iPr_def_11,universal_class) ),
inference(superposition,[status(thm)],[c_2976,c_171]) ).
tcf(c_267739,plain,
member(iPr_def_11,iPr_def_12),
inference(forward_subsumption_resolution,[status(thm)],[c_267733,c_267652]) ).
tcf(c_267745,plain,
! [X0: $i,X1: $i] :
( member(regular(intersection(X0,X1)),X0)
| ( intersection(X0,X1) = iPr_def_10 ) ),
inference(superposition,[status(thm)],[c_267685,c_180]) ).
tcf(c_267759,plain,
! [X0: $i,X1: $i] :
( member(regular(intersection(X0,X1)),X1)
| ( intersection(X0,X1) = iPr_def_10 ) ),
inference(superposition,[status(thm)],[c_267685,c_181]) ).
tcf(c_267858,plain,
! [X0: $i,X1: $i] :
( member(X0,universal_class)
| ~ member(X0,X1) ),
inference(superposition,[status(thm)],[c_165,c_162]) ).
tcf(c_268164,plain,
! [X0: $i] :
( ( X0 = iPr_def_11 )
| ~ member(X0,iPr_def_14) ),
inference(superposition,[status(thm)],[c_2978,c_169]) ).
tcf(c_272458,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( intersection(unordered_pair(X0,X1),X2) = iPr_def_10 )
| ( regular(intersection(unordered_pair(X0,X1),X2)) = X1 )
| ( regular(intersection(unordered_pair(X0,X1),X2)) = X0 ) ),
inference(superposition,[status(thm)],[c_267745,c_169]) ).
tcf(c_272476,plain,
! [X0: $i] :
( ( intersection(iPr_def_14,X0) = iPr_def_10 )
| ( regular(intersection(iPr_def_14,X0)) = iPr_def_11 ) ),
inference(superposition,[status(thm)],[c_267745,c_268164]) ).
tcf(c_272696,plain,
! [X0: $i] :
( member(iPr_def_11,intersection(iPr_def_14,X0))
| ( intersection(iPr_def_14,X0) = iPr_def_10 ) ),
inference(superposition,[status(thm)],[c_272476,c_267685]) ).
tcf(c_275131,plain,
! [X0: $i] :
( member(iPr_def_11,X0)
| ( intersection(iPr_def_14,X0) = iPr_def_10 ) ),
inference(superposition,[status(thm)],[c_272696,c_181]) ).
tcf(c_275541,plain,
! [X0: $i] :
( ( intersection(iPr_def_14,complement(X0)) = iPr_def_10 )
| ~ member(iPr_def_11,X0) ),
inference(superposition,[status(thm)],[c_275131,c_183]) ).
tcf(c_277614,plain,
! [X0: $i] :
( ( regular(intersection(iPr_def_12,X0)) = universal_class )
| ( intersection(unordered_pair(universal_class,iPr_def_11),X0) = iPr_def_10 )
| ( regular(intersection(unordered_pair(universal_class,iPr_def_11),X0)) = iPr_def_11 ) ),
inference(superposition,[status(thm)],[c_2976,c_272458]) ).
tcf(c_277674,plain,
! [X0: $i] :
( ( intersection(iPr_def_12,X0) = iPr_def_10 )
| ( regular(intersection(iPr_def_12,X0)) = iPr_def_11 )
| ( regular(intersection(iPr_def_12,X0)) = universal_class ) ),
inference(light_normalisation,[status(thm)],[c_277614,c_2976]) ).
tcf(c_284485,plain,
intersection(iPr_def_14,complement(iPr_def_12)) = iPr_def_10,
inference(superposition,[status(thm)],[c_267739,c_275541]) ).
tcf(c_286149,plain,
! [X0: $i] :
( member(X0,iPr_def_10)
| ~ member(X0,iPr_def_14)
| ~ member(X0,complement(iPr_def_12)) ),
inference(superposition,[status(thm)],[c_284485,c_182]) ).
tcf(c_286157,plain,
! [X0: $i] :
( ~ member(X0,iPr_def_14)
| ~ member(X0,complement(iPr_def_12)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_286149,c_267694]) ).
tcf(c_291043,plain,
! [X0: $i] :
( member(X0,iPr_def_12)
| ~ member(X0,iPr_def_14)
| ~ member(X0,universal_class) ),
inference(superposition,[status(thm)],[c_184,c_286157]) ).
tcf(c_293191,plain,
! [X0: $i] :
( member(X0,iPr_def_12)
| ~ member(X0,iPr_def_14) ),
inference(global_subsumption_just,[status(thm)],[c_291043,c_84893]) ).
tcf(c_293197,plain,
! [X0: $i] :
( subclass(iPr_def_14,X0)
| member(not_subclass_element(iPr_def_14,X0),iPr_def_12) ),
inference(superposition,[status(thm)],[c_163,c_293191]) ).
tcf(c_293256,plain,
subclass(iPr_def_14,iPr_def_12),
inference(superposition,[status(thm)],[c_293197,c_164]) ).
tcf(c_293347,plain,
( ( iPr_def_12 = iPr_def_14 )
| ~ subclass(iPr_def_12,iPr_def_14) ),
inference(superposition,[status(thm)],[c_293256,c_168]) ).
tcf(c_293655,plain,
~ subclass(iPr_def_12,iPr_def_14),
inference(global_subsumption_just,[status(thm)],[c_293347,c_2977,c_2979,c_2980,c_4702,c_4701,c_4967,c_5232,c_20388,c_23454,c_25904,c_36129,c_61500]) ).
tcf(c_301108,plain,
! [X0: $i] :
( ( intersection(iPr_def_12,X0) = iPr_def_10 )
| ( regular(intersection(iPr_def_12,X0)) = iPr_def_11 ) ),
inference(global_subsumption_just,[status(thm)],[c_277674,c_113405]) ).
tcf(c_301119,plain,
! [X0: $i] :
( member(iPr_def_11,X0)
| ( intersection(iPr_def_12,X0) = iPr_def_10 ) ),
inference(superposition,[status(thm)],[c_301108,c_267759]) ).
tcf(c_307905,plain,
! [X0: $i] :
( ( intersection(iPr_def_12,complement(X0)) = iPr_def_10 )
| ~ member(iPr_def_11,X0) ),
inference(superposition,[status(thm)],[c_301119,c_183]) ).
tcf(c_315429,plain,
intersection(iPr_def_12,complement(iPr_def_14)) = iPr_def_10,
inference(superposition,[status(thm)],[c_267711,c_307905]) ).
tcf(c_317167,plain,
! [X0: $i] :
( member(X0,iPr_def_10)
| ~ member(X0,iPr_def_12)
| ~ member(X0,complement(iPr_def_14)) ),
inference(superposition,[status(thm)],[c_315429,c_182]) ).
tcf(c_317172,plain,
! [X0: $i] :
( ~ member(X0,iPr_def_12)
| ~ member(X0,complement(iPr_def_14)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_317167,c_267694]) ).
tcf(c_317310,plain,
! [X0: $i] :
( member(X0,iPr_def_14)
| ~ member(X0,iPr_def_12)
| ~ member(X0,universal_class) ),
inference(superposition,[status(thm)],[c_184,c_317172]) ).
tcf(c_319324,plain,
! [X0: $i] :
( member(X0,iPr_def_14)
| ~ member(X0,iPr_def_12) ),
inference(forward_subsumption_resolution,[status(thm)],[c_317310,c_267858]) ).
tcf(c_319331,plain,
! [X0: $i] :
( subclass(iPr_def_12,X0)
| member(not_subclass_element(iPr_def_12,X0),iPr_def_14) ),
inference(superposition,[status(thm)],[c_163,c_319324]) ).
tcf(c_320474,plain,
subclass(iPr_def_12,iPr_def_14),
inference(superposition,[status(thm)],[c_319331,c_164]) ).
tcf(c_320481,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[c_320474,c_293655]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SET512-6 : TPTP v9.3.1. Bugfixed v2.1.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.09/0.35 % Computer : n007.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Thu Sep 24 11:07:07 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.36 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.14/0.39 Running first-order theorem proving
% 0.14/0.39 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.14/0.41
% 0.14/0.41 % ======== iProver multi-core TPTP/SMT =========
% 0.14/0.41
% 0.14/0.41 % Detected problem language: tptp
% 0.14/0.42 % Proving...
% 103.63/15.00 % SZS status Started for theBenchmark.p
% 103.63/15.00 % SZS status Unsatisfiable for theBenchmark.p
% 103.63/15.00
% 103.63/15.00 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 103.63/15.00
% 103.63/15.00 % ------ iProver source info
% 103.63/15.00
% 103.63/15.00 % git: date: 2026-07-19 20:42:38 +0200
% 103.63/15.00 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 103.63/15.00 % git: non_committed_changes: false
% 103.63/15.00
% 103.63/15.00 % ------ Parsing...% successful
% 103.63/15.00
% 103.63/15.00
% 103.63/15.00 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 103.63/15.00
% 103.63/15.00 % ------ Preprocessing... sup_sim: 0 sf_s rm: 1 0s sf_e pe_s pe:1:0s pe:2:0s pe:4:0s pe_e sup_sim: 0 sf_s rm: 3 0s sf_e pe_s pe_e %
% 103.63/15.00
% 103.63/15.00 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 103.63/15.00
% 103.63/15.00 % ------ Preprocessing... sf_s rm: 1 0s sf_e sf_s rm: 0 0s sf_e
% 103.63/15.00 % ------ Proving...
% 103.63/15.00 % ------ Problem Properties
% 103.63/15.00
% 103.63/15.00 %
% 103.63/15.00 % clauses 88
% 103.63/15.00 % conjectures 1
% 103.63/15.00 % EPR 13
% 103.63/15.00 % Horn 80
% 103.63/15.00 % unary 27
% 103.63/15.00 % binary 40
% 103.63/15.00 % lits 176
% 103.63/15.00 % lits eq 32
% 103.63/15.00 % fd_pure 0
% 103.63/15.00 % fd_pseudo 0
% 103.63/15.00 % fd_cond 3
% 103.63/15.00 % fd_pseudo_cond 7
% 103.63/15.00 % AC symbols 0
% 103.63/15.00
% 103.63/15.00 % ------ Schedule dynamic 5 is on
% 103.63/15.00
% 103.63/15.00 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" Time Limit: 10.
% 103.63/15.00
% 103.63/15.00
% 103.63/15.00 % ------
% 103.63/15.00 % Current options:
% 103.63/15.00 % ------
% 103.63/15.00
% 103.63/15.00
% 103.63/15.00 %
% 103.63/15.00
% 103.63/15.00 % ------ Proving...
% 103.63/15.00 % Proof_search_loop: time out after: 8037 full_loop iterations
% 103.63/15.00
% 103.63/15.00 % ------ Input Options"1. --res_lit_sel adaptive --res_lit_sel_side num_symb" Time Limit: 15.
% 103.63/15.00
% 103.63/15.00
% 103.63/15.00 % ------
% 103.63/15.00 % Current options:
% 103.63/15.00 % ------
% 103.63/15.00
% 103.63/15.00
% 103.63/15.00 %
% 103.63/15.00
% 103.63/15.00 % ------ Proving...
% 103.63/15.00 %
% 103.63/15.00
% 103.63/15.00 % SZS status Unsatisfiable for theBenchmark.p
% 103.63/15.00
% 103.63/15.00 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 103.63/15.00
% 103.63/15.00
%------------------------------------------------------------------------------