%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SEU124+1 : TPTP v8.1.2. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n025.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:40:35 EDT 2024
% Result : Theorem 2.61s 2.78s
% Output : Refutation 2.61s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : SEU124+1 : TPTP v8.1.2. Released v3.3.0.
% 0.03/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.12/0.33 % Computer : n025.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Wed May 8 11:08:53 EDT 2024
% 0.12/0.34 % CPUTime :
% 2.61/2.78 % Version: 1.5
% 2.61/2.78 % SZS status Theorem
% 2.61/2.78 % SZS output start CNFRefutation
% 2.61/2.78 fof(t7_xboole_1,conjecture,(![A]:(![B]:subset(A,set_union2(A,B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', t7_xboole_1)).
% 2.61/2.78 fof(c7,negated_conjecture,(~(![A]:(![B]:subset(A,set_union2(A,B))))),inference(assume_negation,[status(cth)],[t7_xboole_1])).
% 2.61/2.78 fof(c8,negated_conjecture,(?[A]:(?[B]:~subset(A,set_union2(A,B)))),inference(fof_nnf,[status(thm)],[c7])).
% 2.61/2.78 fof(c9,negated_conjecture,(?[X4]:(?[X5]:~subset(X4,set_union2(X4,X5)))),inference(variable_rename,[status(thm)],[c8])).
% 2.61/2.78 fof(c10,negated_conjecture,~subset(skolem0001,set_union2(skolem0001,skolem0002)),inference(skolemize,[status(esa)],[c9])).
% 2.61/2.78 cnf(c11,negated_conjecture,~subset(skolem0001,set_union2(skolem0001,skolem0002)),inference(split_conjunct,[status(thm)],[c10])).
% 2.61/2.78 fof(d3_tarski,axiom,(![A]:(![B]:(subset(A,B)<=>(![C]:(in(C,A)=>in(C,B)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', d3_tarski)).
% 2.61/2.78 fof(c48,plain,(![A]:(![B]:((~subset(A,B)|(![C]:(~in(C,A)|in(C,B))))&((?[C]:(in(C,A)&~in(C,B)))|subset(A,B))))),inference(fof_nnf,[status(thm)],[d3_tarski])).
% 2.61/2.78 fof(c49,plain,((![A]:(![B]:(~subset(A,B)|(![C]:(~in(C,A)|in(C,B))))))&(![A]:(![B]:((?[C]:(in(C,A)&~in(C,B)))|subset(A,B))))),inference(shift_quantors,[status(thm)],[c48])).
% 2.61/2.78 fof(c50,plain,((![X18]:(![X19]:(~subset(X18,X19)|(![X20]:(~in(X20,X18)|in(X20,X19))))))&(![X21]:(![X22]:((?[X23]:(in(X23,X21)&~in(X23,X22)))|subset(X21,X22))))),inference(variable_rename,[status(thm)],[c49])).
% 2.61/2.78 fof(c52,plain,(![X18]:(![X19]:(![X20]:(![X21]:(![X22]:((~subset(X18,X19)|(~in(X20,X18)|in(X20,X19)))&((in(skolem0005(X21,X22),X21)&~in(skolem0005(X21,X22),X22))|subset(X21,X22)))))))),inference(shift_quantors,[status(thm)],[fof(c51,plain,((![X18]:(![X19]:(~subset(X18,X19)|(![X20]:(~in(X20,X18)|in(X20,X19))))))&(![X21]:(![X22]:((in(skolem0005(X21,X22),X21)&~in(skolem0005(X21,X22),X22))|subset(X21,X22))))),inference(skolemize,[status(esa)],[c50])).])).
% 2.61/2.78 fof(c53,plain,(![X18]:(![X19]:(![X20]:(![X21]:(![X22]:((~subset(X18,X19)|(~in(X20,X18)|in(X20,X19)))&((in(skolem0005(X21,X22),X21)|subset(X21,X22))&(~in(skolem0005(X21,X22),X22)|subset(X21,X22))))))))),inference(distribute,[status(thm)],[c52])).
% 2.61/2.78 cnf(c56,plain,~in(skolem0005(X99,X98),X98)|subset(X99,X98),inference(split_conjunct,[status(thm)],[c53])).
% 2.61/2.78 cnf(c55,plain,in(skolem0005(X93,X92),X93)|subset(X93,X92),inference(split_conjunct,[status(thm)],[c53])).
% 2.61/2.78 cnf(reflexivity,axiom,X37=X37,theory(equality)).
% 2.61/2.78 fof(d2_xboole_0,axiom,(![A]:(![B]:(![C]:(C=set_union2(A,B)<=>(![D]:(in(D,C)<=>(in(D,A)|in(D,B)))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', d2_xboole_0)).
% 2.61/2.78 fof(c57,plain,(![A]:(![B]:(![C]:((C!=set_union2(A,B)|(![D]:((~in(D,C)|(in(D,A)|in(D,B)))&((~in(D,A)&~in(D,B))|in(D,C)))))&((?[D]:((~in(D,C)|(~in(D,A)&~in(D,B)))&(in(D,C)|(in(D,A)|in(D,B)))))|C=set_union2(A,B)))))),inference(fof_nnf,[status(thm)],[d2_xboole_0])).
% 2.61/2.78 fof(c58,plain,((![A]:(![B]:(![C]:(C!=set_union2(A,B)|((![D]:(~in(D,C)|(in(D,A)|in(D,B))))&(![D]:((~in(D,A)&~in(D,B))|in(D,C))))))))&(![A]:(![B]:(![C]:((?[D]:((~in(D,C)|(~in(D,A)&~in(D,B)))&(in(D,C)|(in(D,A)|in(D,B)))))|C=set_union2(A,B)))))),inference(shift_quantors,[status(thm)],[c57])).
% 2.61/2.78 fof(c59,plain,((![X24]:(![X25]:(![X26]:(X26!=set_union2(X24,X25)|((![X27]:(~in(X27,X26)|(in(X27,X24)|in(X27,X25))))&(![X28]:((~in(X28,X24)&~in(X28,X25))|in(X28,X26))))))))&(![X29]:(![X30]:(![X31]:((?[X32]:((~in(X32,X31)|(~in(X32,X29)&~in(X32,X30)))&(in(X32,X31)|(in(X32,X29)|in(X32,X30)))))|X31=set_union2(X29,X30)))))),inference(variable_rename,[status(thm)],[c58])).
% 2.61/2.78 fof(c61,plain,(![X24]:(![X25]:(![X26]:(![X27]:(![X28]:(![X29]:(![X30]:(![X31]:((X26!=set_union2(X24,X25)|((~in(X27,X26)|(in(X27,X24)|in(X27,X25)))&((~in(X28,X24)&~in(X28,X25))|in(X28,X26))))&(((~in(skolem0006(X29,X30,X31),X31)|(~in(skolem0006(X29,X30,X31),X29)&~in(skolem0006(X29,X30,X31),X30)))&(in(skolem0006(X29,X30,X31),X31)|(in(skolem0006(X29,X30,X31),X29)|in(skolem0006(X29,X30,X31),X30))))|X31=set_union2(X29,X30))))))))))),inference(shift_quantors,[status(thm)],[fof(c60,plain,((![X24]:(![X25]:(![X26]:(X26!=set_union2(X24,X25)|((![X27]:(~in(X27,X26)|(in(X27,X24)|in(X27,X25))))&(![X28]:((~in(X28,X24)&~in(X28,X25))|in(X28,X26))))))))&(![X29]:(![X30]:(![X31]:(((~in(skolem0006(X29,X30,X31),X31)|(~in(skolem0006(X29,X30,X31),X29)&~in(skolem0006(X29,X30,X31),X30)))&(in(skolem0006(X29,X30,X31),X31)|(in(skolem0006(X29,X30,X31),X29)|in(skolem0006(X29,X30,X31),X30))))|X31=set_union2(X29,X30)))))),inference(skolemize,[status(esa)],[c59])).])).
% 2.61/2.78 fof(c62,plain,(![X24]:(![X25]:(![X26]:(![X27]:(![X28]:(![X29]:(![X30]:(![X31]:(((X26!=set_union2(X24,X25)|(~in(X27,X26)|(in(X27,X24)|in(X27,X25))))&((X26!=set_union2(X24,X25)|(~in(X28,X24)|in(X28,X26)))&(X26!=set_union2(X24,X25)|(~in(X28,X25)|in(X28,X26)))))&((((~in(skolem0006(X29,X30,X31),X31)|~in(skolem0006(X29,X30,X31),X29))|X31=set_union2(X29,X30))&((~in(skolem0006(X29,X30,X31),X31)|~in(skolem0006(X29,X30,X31),X30))|X31=set_union2(X29,X30)))&((in(skolem0006(X29,X30,X31),X31)|(in(skolem0006(X29,X30,X31),X29)|in(skolem0006(X29,X30,X31),X30)))|X31=set_union2(X29,X30)))))))))))),inference(distribute,[status(thm)],[c61])).
% 2.61/2.78 cnf(c64,plain,X112!=set_union2(X114,X113)|~in(X111,X114)|in(X111,X112),inference(split_conjunct,[status(thm)],[c62])).
% 2.61/2.78 cnf(c178,plain,~in(X172,X171)|in(X172,set_union2(X171,X173)),inference(resolution,[status(thm)],[c64, reflexivity])).
% 2.61/2.78 cnf(c335,plain,in(skolem0005(X1004,X1002),set_union2(X1004,X1003))|subset(X1004,X1002),inference(resolution,[status(thm)],[c178, c55])).
% 2.61/2.78 cnf(c8734,plain,subset(X1006,set_union2(X1006,X1005)),inference(resolution,[status(thm)],[c335, c56])).
% 2.61/2.78 cnf(c8754,plain,$false,inference(resolution,[status(thm)],[c8734, c11])).
% 2.61/2.78 % SZS output end CNFRefutation
% 2.61/2.78
% 2.61/2.78 % Initial clauses : 32
% 2.61/2.78 % Processed clauses : 333
% 2.61/2.78 % Factors computed : 68
% 2.61/2.78 % Resolvents computed: 8617
% 2.61/2.78 % Tautologies deleted: 22
% 2.61/2.78 % Forward subsumed : 696
% 2.61/2.78 % Backward subsumed : 17
% 2.61/2.78 % -------- CPU Time ---------
% 2.61/2.78 % User time : 2.405 s
% 2.61/2.78 % System time : 0.034 s
% 2.61/2.78 % Total time : 2.439 s
%------------------------------------------------------------------------------