%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SET075-7 : TPTP v8.1.2. Bugfixed v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n009.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 : Thu May 9 17:39:06 EDT 2024
% Result : Unsatisfiable 59.63s 59.80s
% Output : Refutation 59.63s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 17
% Syntax : Number of clauses : 42 ( 23 unt; 2 nHn; 19 RR)
% Number of literals : 63 ( 8 equ; 21 neg)
% Maximal clause size : 3 ( 1 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-2 aty)
% Number of functors : 14 ( 14 usr; 6 con; 0-3 aty)
% Number of variables : 73 ( 28 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(domain1,axiom,
( restrict(X173,singleton(X174),universal_class) != null_class
| ~ member(X174,domain_of(X173)) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-0.ax',domain1) ).
cnf(corollary_of_null_class_is_subclass,axiom,
( ~ subclass(X87,null_class)
| X87 = null_class ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',corollary_of_null_class_is_subclass) ).
cnf(transitivity_of_subclass,axiom,
( ~ subclass(X236,X235)
| ~ subclass(X235,X237)
| subclass(X236,X237) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',transitivity_of_subclass) ).
cnf(not_subclass_members2,axiom,
( ~ member(not_subclass_element(X21,X20),X20)
| subclass(X21,X20) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-0.ax',not_subclass_members2) ).
cnf(not_subclass_members1,axiom,
( member(not_subclass_element(X13,X12),X13)
| subclass(X13,X12) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-0.ax',not_subclass_members1) ).
cnf(intersection1,axiom,
( ~ member(X121,intersection(X122,X120))
| member(X121,X122) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-0.ax',intersection1) ).
cnf(c161,plain,
( member(not_subclass_element(intersection(X752,X750),X751),X752)
| subclass(intersection(X752,X750),X751) ),
inference(resolution,[status(thm)],[intersection1,not_subclass_members1]) ).
cnf(c7446,plain,
subclass(intersection(X753,X754),X753),
inference(resolution,[status(thm)],[c161,not_subclass_members2]) ).
cnf(c7481,plain,
( ~ subclass(X819,intersection(X820,X821))
| subclass(X819,X820) ),
inference(resolution,[status(thm)],[c7446,transitivity_of_subclass]) ).
cnf(equal_implies_subclass2,axiom,
( X19 != X18
| subclass(X18,X19) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-0.ax',equal_implies_subclass2) ).
cnf(restriction1,axiom,
intersection(X160,cross_product(X159,X158)) = restrict(X160,X159,X158),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-0.ax',restriction1) ).
cnf(c265,plain,
subclass(restrict(X1081,X1082,X1080),intersection(X1081,cross_product(X1082,X1080))),
inference(resolution,[status(thm)],[restriction1,equal_implies_subclass2]) ).
cnf(c9741,plain,
subclass(restrict(X1084,X1085,X1083),X1084),
inference(resolution,[status(thm)],[c265,c7481]) ).
cnf(null_class_is_subclass,axiom,
subclass(null_class,X9),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',null_class_is_subclass) ).
cnf(c576,plain,
( ~ subclass(X243,null_class)
| subclass(X243,X244) ),
inference(resolution,[status(thm)],[transitivity_of_subclass,null_class_is_subclass]) ).
cnf(singleton_in_unordered_pair1,axiom,
subclass(singleton(X54),unordered_pair(X54,X53)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',singleton_in_unordered_pair1) ).
cnf(equal_implies_subclass1,axiom,
( X16 != X15
| subclass(X16,X15) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-0.ax',equal_implies_subclass1) ).
cnf(prove_corollary_to_unordered_pair_axiom3_2,negated_conjecture,
unordered_pair(x,y) = null_class,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_corollary_to_unordered_pair_axiom3_2) ).
cnf(c102,plain,
subclass(unordered_pair(x,y),null_class),
inference(resolution,[status(thm)],[prove_corollary_to_unordered_pair_axiom3_2,equal_implies_subclass1]) ).
cnf(c565,plain,
( ~ subclass(X2664,unordered_pair(x,y))
| subclass(X2664,null_class) ),
inference(resolution,[status(thm)],[transitivity_of_subclass,c102]) ).
cnf(c28770,plain,
subclass(singleton(x),null_class),
inference(resolution,[status(thm)],[c565,singleton_in_unordered_pair1]) ).
cnf(c28843,plain,
subclass(singleton(x),X2665),
inference(resolution,[status(thm)],[c28770,c576]) ).
cnf(c28852,plain,
( ~ subclass(X3081,singleton(x))
| subclass(X3081,X3082) ),
inference(resolution,[status(thm)],[c28843,transitivity_of_subclass]) ).
cnf(c33965,plain,
subclass(restrict(singleton(x),X3305,X3306),X3307),
inference(resolution,[status(thm)],[c28852,c9741]) ).
cnf(c35478,plain,
restrict(singleton(x),X4023,X4022) = null_class,
inference(resolution,[status(thm)],[c33965,corollary_of_null_class_is_subclass]) ).
cnf(c45545,plain,
~ member(X4024,domain_of(singleton(x))),
inference(resolution,[status(thm)],[c35478,domain1]) ).
cnf(singleton_set,axiom,
unordered_pair(X50,X50) = singleton(X50),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-0.ax',singleton_set) ).
cnf(c63,plain,
subclass(unordered_pair(X63,X63),singleton(X63)),
inference(resolution,[status(thm)],[singleton_set,equal_implies_subclass1]) ).
cnf(c569,plain,
( ~ subclass(X2532,singleton(X2533))
| subclass(X2532,unordered_pair(X2533,X2534)) ),
inference(resolution,[status(thm)],[transitivity_of_subclass,singleton_in_unordered_pair1]) ).
cnf(c28327,plain,
subclass(unordered_pair(X2542,X2542),unordered_pair(X2542,X2541)),
inference(resolution,[status(thm)],[c569,c63]) ).
cnf(c589,plain,
subclass(unordered_pair(x,y),X251),
inference(resolution,[status(thm)],[c576,c102]) ).
cnf(c596,plain,
( ~ subclass(X2760,unordered_pair(x,y))
| subclass(X2760,X2761) ),
inference(resolution,[status(thm)],[c589,transitivity_of_subclass]) ).
cnf(c30145,plain,
subclass(unordered_pair(x,x),X2794),
inference(resolution,[status(thm)],[c596,c28327]) ).
cnf(subclass_members,axiom,
( ~ subclass(X7,X6)
| ~ member(X5,X7)
| member(X5,X6) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-0.ax',subclass_members) ).
cnf(unordered_pair2,axiom,
( ~ member(X49,universal_class)
| member(X49,unordered_pair(X49,X48)) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-0.ax',unordered_pair2) ).
cnf(corollary_1_to_cartesian_product,axiom,
( ~ member(ordered_pair(X429,X431),cross_product(X432,X430))
| member(X429,universal_class) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',corollary_1_to_cartesian_product) ).
cnf(prove_corollary_to_unordered_pair_axiom3_1,negated_conjecture,
member(ordered_pair(x,y),cross_product(u,v)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_corollary_to_unordered_pair_axiom3_1) ).
cnf(c2093,plain,
member(x,universal_class),
inference(resolution,[status(thm)],[prove_corollary_to_unordered_pair_axiom3_1,corollary_1_to_cartesian_product]) ).
cnf(c2105,plain,
member(x,unordered_pair(x,X505)),
inference(resolution,[status(thm)],[c2093,unordered_pair2]) ).
cnf(c2224,plain,
( ~ subclass(unordered_pair(x,X4721),X4722)
| member(x,X4722) ),
inference(resolution,[status(thm)],[c2105,subclass_members]) ).
cnf(c57572,plain,
member(x,X4726),
inference(resolution,[status(thm)],[c2224,c30145]) ).
cnf(c57630,plain,
$false,
inference(resolution,[status(thm)],[c57572,c45545]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : SET075-7 : TPTP v8.1.2. Bugfixed v2.1.0.
% 0.07/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.12/0.34 % Computer : n009.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 300
% 0.12/0.34 % DateTime : Wed May 8 19:11:08 EDT 2024
% 0.12/0.34 % CPUTime :
% 59.63/59.80 % Version: 1.5
% 59.63/59.80 % SZS status Unsatisfiable
% 59.63/59.80 % SZS output start CNFRefutation
% See solution above
% 59.63/59.80
% 59.63/59.80 % Initial clauses : 159
% 59.63/59.80 % Processed clauses : 1955
% 59.63/59.80 % Factors computed : 36
% 59.63/59.80 % Resolvents computed: 57614
% 59.63/59.80 % Tautologies deleted: 13
% 59.63/59.80 % Forward subsumed : 2749
% 59.63/59.80 % Backward subsumed : 57
% 59.63/59.80 % -------- CPU Time ---------
% 59.63/59.80 % User time : 59.313 s
% 59.63/59.80 % System time : 0.137 s
% 59.63/59.80 % Total time : 59.450 s
%------------------------------------------------------------------------------