%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SET632+3 : TPTP v8.1.2. Released v2.2.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n007.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:53 EDT 2024
% Result : Theorem 0.88s 1.09s
% Output : Refutation 0.88s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.13 % Problem : SET632+3 : TPTP v8.1.2. Released v2.2.0.
% 0.08/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.36 % Computer : n007.cluster.edu
% 0.14/0.36 % Model : x86_64 x86_64
% 0.14/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.36 % Memory : 8042.1875MB
% 0.14/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.36 % CPULimit : 300
% 0.14/0.36 % WCLimit : 300
% 0.14/0.36 % DateTime : Wed May 8 18:57:08 EDT 2024
% 0.14/0.36 % CPUTime :
% 0.88/1.09 % Version: 1.5
% 0.88/1.09 % SZS status Theorem
% 0.88/1.09 % SZS output start CNFRefutation
% 0.88/1.09 fof(prove_th114,conjecture,(![B]:(![C]:(![D]:(((subset(B,C)&subset(B,D))&disjoint(C,D))=>B=empty_set)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', prove_th114)).
% 0.88/1.09 fof(c5,negated_conjecture,(~(![B]:(![C]:(![D]:(((subset(B,C)&subset(B,D))&disjoint(C,D))=>B=empty_set))))),inference(assume_negation,[status(cth)],[prove_th114])).
% 0.88/1.09 fof(c6,negated_conjecture,(?[B]:(?[C]:(?[D]:(((subset(B,C)&subset(B,D))&disjoint(C,D))&B!=empty_set)))),inference(fof_nnf,[status(thm)],[c5])).
% 0.88/1.09 fof(c7,negated_conjecture,(?[B]:((?[C]:(?[D]:((subset(B,C)&subset(B,D))&disjoint(C,D))))&B!=empty_set)),inference(shift_quantors,[status(thm)],[c6])).
% 0.88/1.09 fof(c8,negated_conjecture,(?[X2]:((?[X3]:(?[X4]:((subset(X2,X3)&subset(X2,X4))&disjoint(X3,X4))))&X2!=empty_set)),inference(variable_rename,[status(thm)],[c7])).
% 0.88/1.09 fof(c9,negated_conjecture,(((subset(skolem0001,skolem0002)&subset(skolem0001,skolem0003))&disjoint(skolem0002,skolem0003))&skolem0001!=empty_set),inference(skolemize,[status(esa)],[c8])).
% 0.88/1.09 cnf(c12,negated_conjecture,disjoint(skolem0002,skolem0003),inference(split_conjunct,[status(thm)],[c9])).
% 0.88/1.09 fof(disjoint_defn,axiom,(![B]:(![C]:(disjoint(B,C)<=>(~intersect(B,C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', disjoint_defn)).
% 0.88/1.09 fof(c35,plain,(![B]:(![C]:(disjoint(B,C)<=>~intersect(B,C)))),inference(fof_simplification,[status(thm)],[disjoint_defn])).
% 0.88/1.09 fof(c36,plain,(![B]:(![C]:((~disjoint(B,C)|~intersect(B,C))&(intersect(B,C)|disjoint(B,C))))),inference(fof_nnf,[status(thm)],[c35])).
% 0.88/1.09 fof(c37,plain,((![B]:(![C]:(~disjoint(B,C)|~intersect(B,C))))&(![B]:(![C]:(intersect(B,C)|disjoint(B,C))))),inference(shift_quantors,[status(thm)],[c36])).
% 0.88/1.09 fof(c39,plain,(![X16]:(![X17]:(![X18]:(![X19]:((~disjoint(X16,X17)|~intersect(X16,X17))&(intersect(X18,X19)|disjoint(X18,X19))))))),inference(shift_quantors,[status(thm)],[fof(c38,plain,((![X16]:(![X17]:(~disjoint(X16,X17)|~intersect(X16,X17))))&(![X18]:(![X19]:(intersect(X18,X19)|disjoint(X18,X19))))),inference(variable_rename,[status(thm)],[c37])).])).
% 0.88/1.09 cnf(c40,plain,~disjoint(X53,X52)|~intersect(X53,X52),inference(split_conjunct,[status(thm)],[c39])).
% 0.88/1.09 cnf(c10,negated_conjecture,subset(skolem0001,skolem0002),inference(split_conjunct,[status(thm)],[c9])).
% 0.88/1.09 fof(subset_defn,axiom,(![B]:(![C]:(subset(B,C)<=>(![D]:(member(D,B)=>member(D,C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', subset_defn)).
% 0.88/1.09 fof(c54,plain,(![B]:(![C]:((~subset(B,C)|(![D]:(~member(D,B)|member(D,C))))&((?[D]:(member(D,B)&~member(D,C)))|subset(B,C))))),inference(fof_nnf,[status(thm)],[subset_defn])).
% 0.88/1.09 fof(c55,plain,((![B]:(![C]:(~subset(B,C)|(![D]:(~member(D,B)|member(D,C))))))&(![B]:(![C]:((?[D]:(member(D,B)&~member(D,C)))|subset(B,C))))),inference(shift_quantors,[status(thm)],[c54])).
% 0.88/1.09 fof(c56,plain,((![X27]:(![X28]:(~subset(X27,X28)|(![X29]:(~member(X29,X27)|member(X29,X28))))))&(![X30]:(![X31]:((?[X32]:(member(X32,X30)&~member(X32,X31)))|subset(X30,X31))))),inference(variable_rename,[status(thm)],[c55])).
% 0.88/1.09 fof(c58,plain,(![X27]:(![X28]:(![X29]:(![X30]:(![X31]:((~subset(X27,X28)|(~member(X29,X27)|member(X29,X28)))&((member(skolem0006(X30,X31),X30)&~member(skolem0006(X30,X31),X31))|subset(X30,X31)))))))),inference(shift_quantors,[status(thm)],[fof(c57,plain,((![X27]:(![X28]:(~subset(X27,X28)|(![X29]:(~member(X29,X27)|member(X29,X28))))))&(![X30]:(![X31]:((member(skolem0006(X30,X31),X30)&~member(skolem0006(X30,X31),X31))|subset(X30,X31))))),inference(skolemize,[status(esa)],[c56])).])).
% 0.88/1.10 fof(c59,plain,(![X27]:(![X28]:(![X29]:(![X30]:(![X31]:((~subset(X27,X28)|(~member(X29,X27)|member(X29,X28)))&((member(skolem0006(X30,X31),X30)|subset(X30,X31))&(~member(skolem0006(X30,X31),X31)|subset(X30,X31))))))))),inference(distribute,[status(thm)],[c58])).
% 0.88/1.10 cnf(c60,plain,~subset(X114,X116)|~member(X115,X114)|member(X115,X116),inference(split_conjunct,[status(thm)],[c59])).
% 0.88/1.10 fof(empty_defn,axiom,(![B]:(empty(B)<=>(![C]:(~member(C,B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', empty_defn)).
% 0.88/1.10 fof(c14,plain,(![B]:(empty(B)<=>(![C]:~member(C,B)))),inference(fof_simplification,[status(thm)],[empty_defn])).
% 0.88/1.10 fof(c15,plain,(![B]:((~empty(B)|(![C]:~member(C,B)))&((?[C]:member(C,B))|empty(B)))),inference(fof_nnf,[status(thm)],[c14])).
% 0.88/1.10 fof(c16,plain,((![B]:(~empty(B)|(![C]:~member(C,B))))&(![B]:((?[C]:member(C,B))|empty(B)))),inference(shift_quantors,[status(thm)],[c15])).
% 0.88/1.10 fof(c17,plain,((![X5]:(~empty(X5)|(![X6]:~member(X6,X5))))&(![X7]:((?[X8]:member(X8,X7))|empty(X7)))),inference(variable_rename,[status(thm)],[c16])).
% 0.88/1.10 fof(c19,plain,(![X5]:(![X6]:(![X7]:((~empty(X5)|~member(X6,X5))&(member(skolem0004(X7),X7)|empty(X7)))))),inference(shift_quantors,[status(thm)],[fof(c18,plain,((![X5]:(~empty(X5)|(![X6]:~member(X6,X5))))&(![X7]:(member(skolem0004(X7),X7)|empty(X7)))),inference(skolemize,[status(esa)],[c17])).])).
% 0.88/1.10 cnf(c21,plain,member(skolem0004(X83),X83)|empty(X83),inference(split_conjunct,[status(thm)],[c19])).
% 0.88/1.10 cnf(c20,plain,~empty(X40)|~member(X39,X40),inference(split_conjunct,[status(thm)],[c19])).
% 0.88/1.10 fof(intersect_defn,axiom,(![B]:(![C]:(intersect(B,C)<=>(?[D]:(member(D,B)&member(D,C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', intersect_defn)).
% 0.88/1.10 fof(c45,plain,(![B]:(![C]:((~intersect(B,C)|(?[D]:(member(D,B)&member(D,C))))&((![D]:(~member(D,B)|~member(D,C)))|intersect(B,C))))),inference(fof_nnf,[status(thm)],[intersect_defn])).
% 0.88/1.10 fof(c46,plain,((![B]:(![C]:(~intersect(B,C)|(?[D]:(member(D,B)&member(D,C))))))&(![B]:(![C]:((![D]:(~member(D,B)|~member(D,C)))|intersect(B,C))))),inference(shift_quantors,[status(thm)],[c45])).
% 0.88/1.10 fof(c47,plain,((![X21]:(![X22]:(~intersect(X21,X22)|(?[X23]:(member(X23,X21)&member(X23,X22))))))&(![X24]:(![X25]:((![X26]:(~member(X26,X24)|~member(X26,X25)))|intersect(X24,X25))))),inference(variable_rename,[status(thm)],[c46])).
% 0.88/1.10 fof(c49,plain,(![X21]:(![X22]:(![X24]:(![X25]:(![X26]:((~intersect(X21,X22)|(member(skolem0005(X21,X22),X21)&member(skolem0005(X21,X22),X22)))&((~member(X26,X24)|~member(X26,X25))|intersect(X24,X25)))))))),inference(shift_quantors,[status(thm)],[fof(c48,plain,((![X21]:(![X22]:(~intersect(X21,X22)|(member(skolem0005(X21,X22),X21)&member(skolem0005(X21,X22),X22)))))&(![X24]:(![X25]:((![X26]:(~member(X26,X24)|~member(X26,X25)))|intersect(X24,X25))))),inference(skolemize,[status(esa)],[c47])).])).
% 0.88/1.10 fof(c50,plain,(![X21]:(![X22]:(![X24]:(![X25]:(![X26]:(((~intersect(X21,X22)|member(skolem0005(X21,X22),X21))&(~intersect(X21,X22)|member(skolem0005(X21,X22),X22)))&((~member(X26,X24)|~member(X26,X25))|intersect(X24,X25)))))))),inference(distribute,[status(thm)],[c49])).
% 0.88/1.10 cnf(c52,plain,~intersect(X94,X95)|member(skolem0005(X94,X95),X95),inference(split_conjunct,[status(thm)],[c50])).
% 0.88/1.10 cnf(c13,negated_conjecture,skolem0001!=empty_set,inference(split_conjunct,[status(thm)],[c9])).
% 0.88/1.10 fof(empty_set_defn,axiom,(![B]:(~member(B,empty_set))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', empty_set_defn)).
% 0.88/1.10 fof(c42,plain,(![B]:~member(B,empty_set)),inference(fof_simplification,[status(thm)],[empty_set_defn])).
% 0.88/1.10 fof(c43,plain,(![X20]:~member(X20,empty_set)),inference(variable_rename,[status(thm)],[c42])).
% 0.88/1.10 cnf(c44,plain,~member(X35,empty_set),inference(split_conjunct,[status(thm)],[c43])).
% 0.88/1.10 cnf(c61,plain,member(skolem0006(X97,X96),X97)|subset(X97,X96),inference(split_conjunct,[status(thm)],[c59])).
% 0.88/1.10 cnf(c94,plain,subset(empty_set,X98),inference(resolution,[status(thm)],[c61, c44])).
% 0.88/1.10 fof(equal_defn,axiom,(![B]:(![C]:(B=C<=>(subset(B,C)&subset(C,B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', equal_defn)).
% 0.88/1.10 fof(c27,plain,(![B]:(![C]:((B!=C|(subset(B,C)&subset(C,B)))&((~subset(B,C)|~subset(C,B))|B=C)))),inference(fof_nnf,[status(thm)],[equal_defn])).
% 0.88/1.10 fof(c28,plain,((![B]:(![C]:(B!=C|(subset(B,C)&subset(C,B)))))&(![B]:(![C]:((~subset(B,C)|~subset(C,B))|B=C)))),inference(shift_quantors,[status(thm)],[c27])).
% 0.88/1.10 fof(c30,plain,(![X12]:(![X13]:(![X14]:(![X15]:((X12!=X13|(subset(X12,X13)&subset(X13,X12)))&((~subset(X14,X15)|~subset(X15,X14))|X14=X15)))))),inference(shift_quantors,[status(thm)],[fof(c29,plain,((![X12]:(![X13]:(X12!=X13|(subset(X12,X13)&subset(X13,X12)))))&(![X14]:(![X15]:((~subset(X14,X15)|~subset(X15,X14))|X14=X15)))),inference(variable_rename,[status(thm)],[c28])).])).
% 0.88/1.10 fof(c31,plain,(![X12]:(![X13]:(![X14]:(![X15]:(((X12!=X13|subset(X12,X13))&(X12!=X13|subset(X13,X12)))&((~subset(X14,X15)|~subset(X15,X14))|X14=X15)))))),inference(distribute,[status(thm)],[c30])).
% 0.88/1.10 cnf(c34,plain,~subset(X100,X99)|~subset(X99,X100)|X100=X99,inference(split_conjunct,[status(thm)],[c31])).
% 0.88/1.10 cnf(c100,plain,~subset(X106,empty_set)|X106=empty_set,inference(resolution,[status(thm)],[c34, c94])).
% 0.88/1.10 cnf(c53,plain,~member(X109,X107)|~member(X109,X108)|intersect(X107,X108),inference(split_conjunct,[status(thm)],[c50])).
% 0.88/1.10 cnf(c109,plain,~member(X111,X110)|intersect(X110,X110),inference(factor,[status(thm)],[c53])).
% 0.88/1.10 cnf(c112,plain,intersect(X120,X120)|subset(X120,X121),inference(resolution,[status(thm)],[c109, c61])).
% 0.88/1.10 cnf(c131,plain,intersect(X137,X137)|X137=empty_set,inference(resolution,[status(thm)],[c112, c100])).
% 0.88/1.10 cnf(c142,plain,intersect(skolem0001,skolem0001),inference(resolution,[status(thm)],[c131, c13])).
% 0.88/1.10 cnf(c148,plain,member(skolem0005(skolem0001,skolem0001),skolem0001),inference(resolution,[status(thm)],[c142, c52])).
% 0.88/1.10 cnf(c209,plain,~empty(skolem0001),inference(resolution,[status(thm)],[c148, c20])).
% 0.88/1.10 cnf(c214,plain,member(skolem0004(skolem0001),skolem0001),inference(resolution,[status(thm)],[c209, c21])).
% 0.88/1.10 cnf(c221,plain,~subset(skolem0001,X578)|member(skolem0004(skolem0001),X578),inference(resolution,[status(thm)],[c214, c60])).
% 0.88/1.10 cnf(c806,plain,member(skolem0004(skolem0001),skolem0002),inference(resolution,[status(thm)],[c221, c10])).
% 0.88/1.10 cnf(c11,negated_conjecture,subset(skolem0001,skolem0003),inference(split_conjunct,[status(thm)],[c9])).
% 0.88/1.10 cnf(c804,plain,member(skolem0004(skolem0001),skolem0003),inference(resolution,[status(thm)],[c221, c11])).
% 0.88/1.10 cnf(c812,plain,~member(skolem0004(skolem0001),X826)|intersect(X826,skolem0003),inference(resolution,[status(thm)],[c804, c53])).
% 0.88/1.10 cnf(c1454,plain,intersect(skolem0002,skolem0003),inference(resolution,[status(thm)],[c812, c806])).
% 0.88/1.10 cnf(c1473,plain,~disjoint(skolem0002,skolem0003),inference(resolution,[status(thm)],[c1454, c40])).
% 0.88/1.10 cnf(c1480,plain,$false,inference(resolution,[status(thm)],[c1473, c12])).
% 0.88/1.10 % SZS output end CNFRefutation
% 0.88/1.10
% 0.88/1.10 % Initial clauses : 28
% 0.88/1.10 % Processed clauses : 203
% 0.88/1.10 % Factors computed : 26
% 0.88/1.10 % Resolvents computed: 1412
% 0.88/1.10 % Tautologies deleted: 6
% 0.88/1.10 % Forward subsumed : 487
% 0.88/1.10 % Backward subsumed : 7
% 0.88/1.10 % -------- CPU Time ---------
% 0.88/1.10 % User time : 0.690 s
% 0.88/1.10 % System time : 0.021 s
% 0.88/1.10 % Total time : 0.711 s
%------------------------------------------------------------------------------