%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SET009-1 : TPTP v8.1.2. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n005.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:38:48 EDT 2024
% Result : Unsatisfiable 0.97s 1.16s
% Output : Refutation 0.97s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 12
% Syntax : Number of clauses : 29 ( 7 unt; 12 nHn; 21 RR)
% Number of literals : 62 ( 0 equ; 23 neg)
% Maximal clause size : 4 ( 2 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 4 ( 3 usr; 1 prp; 0-3 aty)
% Number of functors : 7 ( 7 usr; 5 con; 0-3 aty)
% Number of variables : 42 ( 2 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(prove_bDa_is_a_subset_of_bDd,negated_conjecture,
~ subset(bDa,bDd),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_bDa_is_a_subset_of_bDd) ).
cnf(subsets_axiom2,axiom,
( ~ member(member_of_1_not_of_2(X13,X12),X12)
| subset(X13,X12) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET001-0.ax',subsets_axiom2) ).
cnf(subsets_axiom1,axiom,
( subset(X11,X10)
| member(member_of_1_not_of_2(X11,X10),X11) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET001-0.ax',subsets_axiom1) ).
cnf(not_member_of_difference,axiom,
( ~ member(X31,X33)
| ~ member(X31,X30)
| ~ difference(X32,X33,X30) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET001-3.ax',not_member_of_difference) ).
cnf(b_minus_a,plain,
difference(b,a,bDa),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',b_minus_a) ).
cnf(c20,plain,
( ~ member(X35,a)
| ~ member(X35,bDa) ),
inference(resolution,[status(thm)],[not_member_of_difference,b_minus_a]) ).
cnf(difference_axiom2,axiom,
( difference(X46,X45,X44)
| member(k(X46,X45,X44),X46)
| member(k(X46,X45,X44),X44) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET001-3.ax',difference_axiom2) ).
cnf(c35,plain,
( difference(X47,X48,X47)
| member(k(X47,X48,X47),X47) ),
inference(factor,[status(thm)],[difference_axiom2]) ).
cnf(c57,plain,
( difference(bDa,X197,bDa)
| ~ member(k(bDa,X197,bDa),a) ),
inference(resolution,[status(thm)],[c35,c20]) ).
cnf(d_is_a_subset_of_a,plain,
subset(d,a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d_is_a_subset_of_a) ).
cnf(membership_in_subsets,axiom,
( ~ member(X6,X8)
| ~ subset(X8,X7)
| member(X6,X7) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET001-0.ax',membership_in_subsets) ).
cnf(c0,plain,
( ~ member(X9,d)
| member(X9,a) ),
inference(resolution,[status(thm)],[membership_in_subsets,d_is_a_subset_of_a]) ).
cnf(difference_axiom3,axiom,
( ~ member(k(X60,X59,X58),X58)
| ~ member(k(X60,X59,X58),X60)
| member(k(X60,X59,X58),X59)
| difference(X60,X59,X58) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET001-3.ax',difference_axiom3) ).
cnf(c77,plain,
( ~ member(k(X227,X226,X227),X227)
| member(k(X227,X226,X227),X226)
| difference(X227,X226,X227) ),
inference(factor,[status(thm)],[difference_axiom3]) ).
cnf(c1043,plain,
( member(k(X229,X228,X229),X228)
| difference(X229,X228,X229) ),
inference(resolution,[status(thm)],[c77,c35]) ).
cnf(c1062,plain,
( difference(X247,d,X247)
| member(k(X247,d,X247),a) ),
inference(resolution,[status(thm)],[c1043,c0]) ).
cnf(c1126,plain,
difference(bDa,d,bDa),
inference(resolution,[status(thm)],[c1062,c57]) ).
cnf(c1131,plain,
( ~ member(X250,d)
| ~ member(X250,bDa) ),
inference(resolution,[status(thm)],[c1126,not_member_of_difference]) ).
cnf(c1151,plain,
( ~ member(member_of_1_not_of_2(bDa,X254),d)
| subset(bDa,X254) ),
inference(resolution,[status(thm)],[c1131,subsets_axiom1]) ).
cnf(member_of_difference,axiom,
( ~ difference(X24,X22,X21)
| ~ member(X23,X21)
| member(X23,X24) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET001-3.ax',member_of_difference) ).
cnf(c15,plain,
( ~ member(X29,bDa)
| member(X29,b) ),
inference(resolution,[status(thm)],[member_of_difference,b_minus_a]) ).
cnf(c18,plain,
( member(member_of_1_not_of_2(bDa,X49),b)
| subset(bDa,X49) ),
inference(resolution,[status(thm)],[c15,subsets_axiom1]) ).
cnf(b_minus_d,plain,
difference(b,d,bDd),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',b_minus_d) ).
cnf(member_of_difference_or_set2,axiom,
( ~ member(X39,X40)
| ~ difference(X40,X38,X37)
| member(X39,X37)
| member(X39,X38) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET001-3.ax',member_of_difference_or_set2) ).
cnf(c25,plain,
( ~ member(X69,b)
| member(X69,bDd)
| member(X69,d) ),
inference(resolution,[status(thm)],[member_of_difference_or_set2,b_minus_d]) ).
cnf(c105,plain,
( member(member_of_1_not_of_2(bDa,X339),bDd)
| member(member_of_1_not_of_2(bDa,X339),d)
| subset(bDa,X339) ),
inference(resolution,[status(thm)],[c25,c18]) ).
cnf(c2344,plain,
( member(member_of_1_not_of_2(bDa,X340),bDd)
| subset(bDa,X340) ),
inference(resolution,[status(thm)],[c105,c1151]) ).
cnf(c2355,plain,
subset(bDa,bDd),
inference(resolution,[status(thm)],[c2344,subsets_axiom2]) ).
cnf(c2378,plain,
$false,
inference(resolution,[status(thm)],[c2355,prove_bDa_is_a_subset_of_bDd]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.13 % Problem : SET009-1 : TPTP v8.1.2. Released v1.0.0.
% 0.08/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.35 % Computer : n005.cluster.edu
% 0.14/0.35 % Model : x86_64 x86_64
% 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.35 % Memory : 8042.1875MB
% 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.35 % CPULimit : 300
% 0.14/0.35 % WCLimit : 300
% 0.14/0.35 % DateTime : Wed May 8 18:47:08 EDT 2024
% 0.14/0.36 % CPUTime :
% 0.97/1.16 % Version: 1.5
% 0.97/1.16 % SZS status Unsatisfiable
% 0.97/1.16 % SZS output start CNFRefutation
% See solution above
% 0.97/1.16
% 0.97/1.16 % Initial clauses : 16
% 0.97/1.16 % Processed clauses : 166
% 0.97/1.16 % Factors computed : 19
% 0.97/1.16 % Resolvents computed: 2361
% 0.97/1.16 % Tautologies deleted: 23
% 0.97/1.16 % Forward subsumed : 125
% 0.97/1.16 % Backward subsumed : 9
% 0.97/1.16 % -------- CPU Time ---------
% 0.97/1.16 % User time : 0.780 s
% 0.97/1.16 % System time : 0.021 s
% 0.97/1.16 % Total time : 0.801 s
%------------------------------------------------------------------------------