%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SET162+3 : TPTP v8.1.2. Released v2.2.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n028.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:19 EDT 2024
% Result : Theorem 190.00s 190.18s
% Output : Refutation 190.00s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.13 % Problem : SET162+3 : TPTP v8.1.2. Released v2.2.0.
% 0.03/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.35 % Computer : n028.cluster.edu
% 0.13/0.35 % Model : x86_64 x86_64
% 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.35 % Memory : 8042.1875MB
% 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.35 % CPULimit : 300
% 0.13/0.35 % WCLimit : 300
% 0.13/0.35 % DateTime : Wed May 8 19:25:53 EDT 2024
% 0.13/0.35 % CPUTime :
% 190.00/190.18 % Version: 1.5
% 190.00/190.18 % SZS status Theorem
% 190.00/190.18 % SZS output start CNFRefutation
% 190.00/190.18 fof(prove_union_empty_set,conjecture,(![B]:union(B,empty_set)=B),file('/export/starexec/sandbox/benchmark/theBenchmark.p', prove_union_empty_set)).
% 190.00/190.18 fof(c4,negated_conjecture,(~(![B]:union(B,empty_set)=B)),inference(assume_negation,[status(cth)],[prove_union_empty_set])).
% 190.00/190.18 fof(c5,negated_conjecture,(?[B]:union(B,empty_set)!=B),inference(fof_nnf,[status(thm)],[c4])).
% 190.00/190.18 fof(c6,negated_conjecture,(?[X2]:union(X2,empty_set)!=X2),inference(variable_rename,[status(thm)],[c5])).
% 190.00/190.18 fof(c7,negated_conjecture,union(skolem0001,empty_set)!=skolem0001,inference(skolemize,[status(esa)],[c6])).
% 190.00/190.18 cnf(c8,negated_conjecture,union(skolem0001,empty_set)!=skolem0001,inference(split_conjunct,[status(thm)],[c7])).
% 190.00/190.18 fof(equal_defn,axiom,(![B]:(![C]:(B=C<=>(subset(B,C)&subset(C,B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', equal_defn)).
% 190.00/190.18 fof(c40,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])).
% 190.00/190.18 fof(c41,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)],[c40])).
% 190.00/190.18 fof(c43,plain,(![X23]:(![X24]:(![X25]:(![X26]:((X23!=X24|(subset(X23,X24)&subset(X24,X23)))&((~subset(X25,X26)|~subset(X26,X25))|X25=X26)))))),inference(shift_quantors,[status(thm)],[fof(c42,plain,((![X23]:(![X24]:(X23!=X24|(subset(X23,X24)&subset(X24,X23)))))&(![X25]:(![X26]:((~subset(X25,X26)|~subset(X26,X25))|X25=X26)))),inference(variable_rename,[status(thm)],[c41])).])).
% 190.00/190.18 fof(c44,plain,(![X23]:(![X24]:(![X25]:(![X26]:(((X23!=X24|subset(X23,X24))&(X23!=X24|subset(X24,X23)))&((~subset(X25,X26)|~subset(X26,X25))|X25=X26)))))),inference(distribute,[status(thm)],[c43])).
% 190.00/190.18 cnf(c47,plain,~subset(X108,X109)|~subset(X109,X108)|X108=X109,inference(split_conjunct,[status(thm)],[c44])).
% 190.00/190.18 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)).
% 190.00/190.18 fof(c29,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])).
% 190.00/190.18 fof(c30,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)],[c29])).
% 190.00/190.18 fof(c31,plain,((![X15]:(![X16]:(~subset(X15,X16)|(![X17]:(~member(X17,X15)|member(X17,X16))))))&(![X18]:(![X19]:((?[X20]:(member(X20,X18)&~member(X20,X19)))|subset(X18,X19))))),inference(variable_rename,[status(thm)],[c30])).
% 190.00/190.18 fof(c33,plain,(![X15]:(![X16]:(![X17]:(![X18]:(![X19]:((~subset(X15,X16)|(~member(X17,X15)|member(X17,X16)))&((member(skolem0004(X18,X19),X18)&~member(skolem0004(X18,X19),X19))|subset(X18,X19)))))))),inference(shift_quantors,[status(thm)],[fof(c32,plain,((![X15]:(![X16]:(~subset(X15,X16)|(![X17]:(~member(X17,X15)|member(X17,X16))))))&(![X18]:(![X19]:((member(skolem0004(X18,X19),X18)&~member(skolem0004(X18,X19),X19))|subset(X18,X19))))),inference(skolemize,[status(esa)],[c31])).])).
% 190.00/190.18 fof(c34,plain,(![X15]:(![X16]:(![X17]:(![X18]:(![X19]:((~subset(X15,X16)|(~member(X17,X15)|member(X17,X16)))&((member(skolem0004(X18,X19),X18)|subset(X18,X19))&(~member(skolem0004(X18,X19),X19)|subset(X18,X19))))))))),inference(distribute,[status(thm)],[c33])).
% 190.00/190.18 cnf(c37,plain,~member(skolem0004(X93,X94),X94)|subset(X93,X94),inference(split_conjunct,[status(thm)],[c34])).
% 190.00/190.18 cnf(c36,plain,member(skolem0004(X79,X80),X79)|subset(X79,X80),inference(split_conjunct,[status(thm)],[c34])).
% 190.00/190.18 fof(union_defn,axiom,(![B]:(![C]:(![D]:(member(D,union(B,C))<=>(member(D,B)|member(D,C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', union_defn)).
% 190.00/190.18 fof(c51,plain,(![B]:(![C]:(![D]:((~member(D,union(B,C))|(member(D,B)|member(D,C)))&((~member(D,B)&~member(D,C))|member(D,union(B,C))))))),inference(fof_nnf,[status(thm)],[union_defn])).
% 190.00/190.18 fof(c52,plain,((![B]:(![C]:(![D]:(~member(D,union(B,C))|(member(D,B)|member(D,C))))))&(![B]:(![C]:(![D]:((~member(D,B)&~member(D,C))|member(D,union(B,C))))))),inference(shift_quantors,[status(thm)],[c51])).
% 190.00/190.18 fof(c54,plain,(![X28]:(![X29]:(![X30]:(![X31]:(![X32]:(![X33]:((~member(X30,union(X28,X29))|(member(X30,X28)|member(X30,X29)))&((~member(X33,X31)&~member(X33,X32))|member(X33,union(X31,X32)))))))))),inference(shift_quantors,[status(thm)],[fof(c53,plain,((![X28]:(![X29]:(![X30]:(~member(X30,union(X28,X29))|(member(X30,X28)|member(X30,X29))))))&(![X31]:(![X32]:(![X33]:((~member(X33,X31)&~member(X33,X32))|member(X33,union(X31,X32))))))),inference(variable_rename,[status(thm)],[c52])).])).
% 190.00/190.18 fof(c55,plain,(![X28]:(![X29]:(![X30]:(![X31]:(![X32]:(![X33]:((~member(X30,union(X28,X29))|(member(X30,X28)|member(X30,X29)))&((~member(X33,X31)|member(X33,union(X31,X32)))&(~member(X33,X32)|member(X33,union(X31,X32))))))))))),inference(distribute,[status(thm)],[c54])).
% 190.00/190.18 cnf(c57,plain,~member(X99,X101)|member(X99,union(X101,X100)),inference(split_conjunct,[status(thm)],[c55])).
% 190.00/190.18 cnf(c98,plain,member(skolem0004(X282,X280),union(X282,X281))|subset(X282,X280),inference(resolution,[status(thm)],[c57, c36])).
% 190.00/190.18 cnf(c498,plain,subset(X283,union(X283,X284)),inference(resolution,[status(thm)],[c98, c37])).
% 190.00/190.18 cnf(c507,plain,~subset(union(X445,X444),X445)|union(X445,X444)=X445,inference(resolution,[status(thm)],[c498, c47])).
% 190.00/190.18 fof(empty_set_defn,axiom,(![B]:(~member(B,empty_set))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', empty_set_defn)).
% 190.00/190.18 fof(c48,plain,(![B]:~member(B,empty_set)),inference(fof_simplification,[status(thm)],[empty_set_defn])).
% 190.00/190.18 fof(c49,plain,(![X27]:~member(X27,empty_set)),inference(variable_rename,[status(thm)],[c48])).
% 190.00/190.18 cnf(c50,plain,~member(X36,empty_set),inference(split_conjunct,[status(thm)],[c49])).
% 190.00/190.18 cnf(c56,plain,~member(X122,union(X120,X121))|member(X122,X120)|member(X122,X121),inference(split_conjunct,[status(thm)],[c55])).
% 190.00/190.18 cnf(c158,plain,member(skolem0004(union(X628,X626),X627),X628)|member(skolem0004(union(X628,X626),X627),X626)|subset(union(X628,X626),X627),inference(resolution,[status(thm)],[c56, c36])).
% 190.00/190.18 cnf(c1734,plain,member(skolem0004(union(X11325,X11326),X11325),X11326)|subset(union(X11325,X11326),X11325),inference(resolution,[status(thm)],[c158, c37])).
% 190.00/190.18 cnf(c168730,plain,subset(union(X11331,empty_set),X11331),inference(resolution,[status(thm)],[c1734, c50])).
% 190.00/190.18 cnf(c168836,plain,union(X11332,empty_set)=X11332,inference(resolution,[status(thm)],[c168730, c507])).
% 190.00/190.18 cnf(c168936,plain,$false,inference(resolution,[status(thm)],[c168836, c8])).
% 190.00/190.18 % SZS output end CNFRefutation
% 190.00/190.18
% 190.00/190.18 % Initial clauses : 26
% 190.00/190.18 % Processed clauses : 1416
% 190.00/190.18 % Factors computed : 377
% 190.00/190.18 % Resolvents computed: 168716
% 190.00/190.18 % Tautologies deleted: 20
% 190.00/190.18 % Forward subsumed : 5238
% 190.00/190.18 % Backward subsumed : 77
% 190.00/190.18 % -------- CPU Time ---------
% 190.00/190.18 % User time : 189.381 s
% 190.00/190.18 % System time : 0.446 s
% 190.00/190.18 % Total time : 189.827 s
%------------------------------------------------------------------------------