%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SEU169+1 : TPTP v8.1.2. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n012.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:45 EDT 2024
% Result : Theorem 0.54s 0.75s
% Output : Refutation 0.54s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : SEU169+1 : TPTP v8.1.2. Released v3.3.0.
% 0.07/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.33 % Computer : n012.cluster.edu
% 0.13/0.33 % Model : x86_64 x86_64
% 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.33 % Memory : 8042.1875MB
% 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.33 % CPULimit : 300
% 0.13/0.33 % WCLimit : 300
% 0.13/0.33 % DateTime : Wed May 8 10:52:38 EDT 2024
% 0.13/0.33 % CPUTime :
% 0.54/0.75 % Version: 1.5
% 0.54/0.75 % SZS status Theorem
% 0.54/0.75 % SZS output start CNFRefutation
% 0.54/0.75 fof(l3_subset_1,conjecture,(![A]:(![B]:(element(B,powerset(A))=>(![C]:(in(C,B)=>in(C,A)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', l3_subset_1)).
% 0.54/0.75 fof(c31,negated_conjecture,(~(![A]:(![B]:(element(B,powerset(A))=>(![C]:(in(C,B)=>in(C,A))))))),inference(assume_negation,[status(cth)],[l3_subset_1])).
% 0.54/0.75 fof(c32,negated_conjecture,(?[A]:(?[B]:(element(B,powerset(A))&(?[C]:(in(C,B)&~in(C,A)))))),inference(fof_nnf,[status(thm)],[c31])).
% 0.54/0.75 fof(c33,negated_conjecture,(?[X12]:(?[X13]:(element(X13,powerset(X12))&(?[X14]:(in(X14,X13)&~in(X14,X12)))))),inference(variable_rename,[status(thm)],[c32])).
% 0.54/0.75 fof(c34,negated_conjecture,(element(skolem0005,powerset(skolem0004))&(in(skolem0006,skolem0005)&~in(skolem0006,skolem0004))),inference(skolemize,[status(esa)],[c33])).
% 0.54/0.75 cnf(c37,negated_conjecture,~in(skolem0006,skolem0004),inference(split_conjunct,[status(thm)],[c34])).
% 0.54/0.75 cnf(c36,negated_conjecture,in(skolem0006,skolem0005),inference(split_conjunct,[status(thm)],[c34])).
% 0.54/0.75 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)).
% 0.54/0.75 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])).
% 0.54/0.75 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])).
% 0.54/0.75 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])).
% 0.54/0.75 fof(c52,plain,(![X18]:(![X19]:(![X20]:(![X21]:(![X22]:((~subset(X18,X19)|(~in(X20,X18)|in(X20,X19)))&((in(skolem0008(X21,X22),X21)&~in(skolem0008(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(skolem0008(X21,X22),X21)&~in(skolem0008(X21,X22),X22))|subset(X21,X22))))),inference(skolemize,[status(esa)],[c50])).])).
% 0.54/0.75 fof(c53,plain,(![X18]:(![X19]:(![X20]:(![X21]:(![X22]:((~subset(X18,X19)|(~in(X20,X18)|in(X20,X19)))&((in(skolem0008(X21,X22),X21)|subset(X21,X22))&(~in(skolem0008(X21,X22),X22)|subset(X21,X22))))))))),inference(distribute,[status(thm)],[c52])).
% 0.54/0.75 cnf(c54,plain,~subset(X88,X86)|~in(X87,X88)|in(X87,X86),inference(split_conjunct,[status(thm)],[c53])).
% 0.54/0.75 cnf(c122,plain,~subset(skolem0005,X127)|in(skolem0006,X127),inference(resolution,[status(thm)],[c54, c36])).
% 0.54/0.75 cnf(reflexivity,axiom,X39=X39,theory(equality)).
% 0.54/0.75 fof(d1_zfmisc_1,axiom,(![A]:(![B]:(B=powerset(A)<=>(![C]:(in(C,B)<=>subset(C,A)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', d1_zfmisc_1)).
% 0.54/0.75 fof(c67,plain,(![A]:(![B]:((B!=powerset(A)|(![C]:((~in(C,B)|subset(C,A))&(~subset(C,A)|in(C,B)))))&((?[C]:((~in(C,B)|~subset(C,A))&(in(C,B)|subset(C,A))))|B=powerset(A))))),inference(fof_nnf,[status(thm)],[d1_zfmisc_1])).
% 0.54/0.75 fof(c68,plain,((![A]:(![B]:(B!=powerset(A)|((![C]:(~in(C,B)|subset(C,A)))&(![C]:(~subset(C,A)|in(C,B)))))))&(![A]:(![B]:((?[C]:((~in(C,B)|~subset(C,A))&(in(C,B)|subset(C,A))))|B=powerset(A))))),inference(shift_quantors,[status(thm)],[c67])).
% 0.54/0.75 fof(c69,plain,((![X30]:(![X31]:(X31!=powerset(X30)|((![X32]:(~in(X32,X31)|subset(X32,X30)))&(![X33]:(~subset(X33,X30)|in(X33,X31)))))))&(![X34]:(![X35]:((?[X36]:((~in(X36,X35)|~subset(X36,X34))&(in(X36,X35)|subset(X36,X34))))|X35=powerset(X34))))),inference(variable_rename,[status(thm)],[c68])).
% 0.54/0.75 fof(c71,plain,(![X30]:(![X31]:(![X32]:(![X33]:(![X34]:(![X35]:((X31!=powerset(X30)|((~in(X32,X31)|subset(X32,X30))&(~subset(X33,X30)|in(X33,X31))))&(((~in(skolem0009(X34,X35),X35)|~subset(skolem0009(X34,X35),X34))&(in(skolem0009(X34,X35),X35)|subset(skolem0009(X34,X35),X34)))|X35=powerset(X34))))))))),inference(shift_quantors,[status(thm)],[fof(c70,plain,((![X30]:(![X31]:(X31!=powerset(X30)|((![X32]:(~in(X32,X31)|subset(X32,X30)))&(![X33]:(~subset(X33,X30)|in(X33,X31)))))))&(![X34]:(![X35]:(((~in(skolem0009(X34,X35),X35)|~subset(skolem0009(X34,X35),X34))&(in(skolem0009(X34,X35),X35)|subset(skolem0009(X34,X35),X34)))|X35=powerset(X34))))),inference(skolemize,[status(esa)],[c69])).])).
% 0.54/0.75 fof(c72,plain,(![X30]:(![X31]:(![X32]:(![X33]:(![X34]:(![X35]:(((X31!=powerset(X30)|(~in(X32,X31)|subset(X32,X30)))&(X31!=powerset(X30)|(~subset(X33,X30)|in(X33,X31))))&(((~in(skolem0009(X34,X35),X35)|~subset(skolem0009(X34,X35),X34))|X35=powerset(X34))&((in(skolem0009(X34,X35),X35)|subset(skolem0009(X34,X35),X34))|X35=powerset(X34)))))))))),inference(distribute,[status(thm)],[c71])).
% 0.54/0.75 cnf(c73,plain,X112!=powerset(X113)|~in(X111,X112)|subset(X111,X113),inference(split_conjunct,[status(thm)],[c72])).
% 0.54/0.75 cnf(c237,plain,~in(X165,powerset(X166))|subset(X165,X166),inference(resolution,[status(thm)],[c73, reflexivity])).
% 0.54/0.75 fof(fc1_subset_1,axiom,(![A]:(~empty(powerset(A)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', fc1_subset_1)).
% 0.54/0.75 fof(c39,plain,(![A]:~empty(powerset(A))),inference(fof_simplification,[status(thm)],[fc1_subset_1])).
% 0.54/0.75 fof(c40,plain,(![X15]:~empty(powerset(X15))),inference(variable_rename,[status(thm)],[c39])).
% 0.54/0.75 cnf(c41,plain,~empty(powerset(X44)),inference(split_conjunct,[status(thm)],[c40])).
% 0.54/0.75 cnf(c35,negated_conjecture,element(skolem0005,powerset(skolem0004)),inference(split_conjunct,[status(thm)],[c34])).
% 0.54/0.75 fof(d2_subset_1,axiom,(![A]:(![B]:(((~empty(A))=>(element(B,A)<=>in(B,A)))&(empty(A)=>(element(B,A)<=>empty(B)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', d2_subset_1)).
% 0.54/0.75 fof(c57,plain,(![A]:(![B]:((~empty(A)=>(element(B,A)<=>in(B,A)))&(empty(A)=>(element(B,A)<=>empty(B)))))),inference(fof_simplification,[status(thm)],[d2_subset_1])).
% 0.54/0.75 fof(c58,plain,(![A]:(![B]:((empty(A)|((~element(B,A)|in(B,A))&(~in(B,A)|element(B,A))))&(~empty(A)|((~element(B,A)|empty(B))&(~empty(B)|element(B,A))))))),inference(fof_nnf,[status(thm)],[c57])).
% 0.54/0.75 fof(c59,plain,((![A]:(empty(A)|((![B]:(~element(B,A)|in(B,A)))&(![B]:(~in(B,A)|element(B,A))))))&(![A]:(~empty(A)|((![B]:(~element(B,A)|empty(B)))&(![B]:(~empty(B)|element(B,A))))))),inference(shift_quantors,[status(thm)],[c58])).
% 0.54/0.75 fof(c61,plain,(![X24]:(![X25]:(![X26]:(![X27]:(![X28]:(![X29]:((empty(X24)|((~element(X25,X24)|in(X25,X24))&(~in(X26,X24)|element(X26,X24))))&(~empty(X27)|((~element(X28,X27)|empty(X28))&(~empty(X29)|element(X29,X27))))))))))),inference(shift_quantors,[status(thm)],[fof(c60,plain,((![X24]:(empty(X24)|((![X25]:(~element(X25,X24)|in(X25,X24)))&(![X26]:(~in(X26,X24)|element(X26,X24))))))&(![X27]:(~empty(X27)|((![X28]:(~element(X28,X27)|empty(X28)))&(![X29]:(~empty(X29)|element(X29,X27))))))),inference(variable_rename,[status(thm)],[c59])).])).
% 0.54/0.75 fof(c62,plain,(![X24]:(![X25]:(![X26]:(![X27]:(![X28]:(![X29]:(((empty(X24)|(~element(X25,X24)|in(X25,X24)))&(empty(X24)|(~in(X26,X24)|element(X26,X24))))&((~empty(X27)|(~element(X28,X27)|empty(X28)))&(~empty(X27)|(~empty(X29)|element(X29,X27))))))))))),inference(distribute,[status(thm)],[c61])).
% 0.54/0.75 cnf(c63,plain,empty(X100)|~element(X101,X100)|in(X101,X100),inference(split_conjunct,[status(thm)],[c62])).
% 0.54/0.75 cnf(c178,plain,empty(powerset(skolem0004))|in(skolem0005,powerset(skolem0004)),inference(resolution,[status(thm)],[c63, c35])).
% 0.54/0.75 cnf(c1039,plain,in(skolem0005,powerset(skolem0004)),inference(resolution,[status(thm)],[c178, c41])).
% 0.54/0.75 cnf(c1051,plain,subset(skolem0005,skolem0004),inference(resolution,[status(thm)],[c1039, c237])).
% 0.54/0.75 cnf(c1054,plain,in(skolem0006,skolem0004),inference(resolution,[status(thm)],[c1051, c122])).
% 0.54/0.75 cnf(c1058,plain,$false,inference(resolution,[status(thm)],[c1054, c37])).
% 0.54/0.75 % SZS output end CNFRefutation
% 0.54/0.75
% 0.54/0.75 % Initial clauses : 37
% 0.54/0.75 % Processed clauses : 175
% 0.54/0.75 % Factors computed : 10
% 0.54/0.75 % Resolvents computed: 972
% 0.54/0.75 % Tautologies deleted: 6
% 0.54/0.75 % Forward subsumed : 153
% 0.54/0.75 % Backward subsumed : 6
% 0.54/0.75 % -------- CPU Time ---------
% 0.54/0.75 % User time : 0.392 s
% 0.54/0.75 % System time : 0.021 s
% 0.54/0.75 % Total time : 0.413 s
%------------------------------------------------------------------------------