%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SEU355+1 : TPTP v8.1.2. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n003.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:41:10 EDT 2024
% Result : Theorem 1.06s 1.25s
% Output : Refutation 1.06s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.13 % Problem : SEU355+1 : TPTP v8.1.2. Released v3.3.0.
% 0.07/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.35 % Computer : n003.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 11:16:53 EDT 2024
% 0.13/0.35 % CPUTime :
% 1.06/1.25 % Version: 1.5
% 1.06/1.25 % SZS status Theorem
% 1.06/1.25 % SZS output start CNFRefutation
% 1.06/1.25 fof(fc1_xboole_0,axiom,empty(empty_set),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', fc1_xboole_0)).
% 1.06/1.25 cnf(c44,plain,empty(empty_set),inference(split_conjunct,[status(thm)],[fc1_xboole_0])).
% 1.06/1.25 fof(t7_boole,axiom,(![A]:(![B]:(~(in(A,B)&empty(B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', t7_boole)).
% 1.06/1.25 fof(c13,plain,(![A]:(![B]:(~in(A,B)|~empty(B)))),inference(fof_nnf,[status(thm)],[t7_boole])).
% 1.06/1.25 fof(c14,plain,(![X4]:(![X5]:(~in(X4,X5)|~empty(X5)))),inference(variable_rename,[status(thm)],[c13])).
% 1.06/1.25 cnf(c15,plain,~in(X50,X51)|~empty(X51),inference(split_conjunct,[status(thm)],[c14])).
% 1.06/1.25 fof(t6_yellow_0,conjecture,(![A]:(rel_str(A)=>(![B]:(element(B,the_carrier(A))=>(relstr_set_smaller(A,empty_set,B)&relstr_element_smaller(A,empty_set,B)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', t6_yellow_0)).
% 1.06/1.25 fof(c16,negated_conjecture,(~(![A]:(rel_str(A)=>(![B]:(element(B,the_carrier(A))=>(relstr_set_smaller(A,empty_set,B)&relstr_element_smaller(A,empty_set,B))))))),inference(assume_negation,[status(cth)],[t6_yellow_0])).
% 1.06/1.25 fof(c17,negated_conjecture,(?[A]:(rel_str(A)&(?[B]:(element(B,the_carrier(A))&(~relstr_set_smaller(A,empty_set,B)|~relstr_element_smaller(A,empty_set,B)))))),inference(fof_nnf,[status(thm)],[c16])).
% 1.06/1.25 fof(c18,negated_conjecture,(?[X6]:(rel_str(X6)&(?[X7]:(element(X7,the_carrier(X6))&(~relstr_set_smaller(X6,empty_set,X7)|~relstr_element_smaller(X6,empty_set,X7)))))),inference(variable_rename,[status(thm)],[c17])).
% 1.06/1.25 fof(c19,negated_conjecture,(rel_str(skolem0001)&(element(skolem0002,the_carrier(skolem0001))&(~relstr_set_smaller(skolem0001,empty_set,skolem0002)|~relstr_element_smaller(skolem0001,empty_set,skolem0002)))),inference(skolemize,[status(esa)],[c18])).
% 1.06/1.25 cnf(c20,negated_conjecture,rel_str(skolem0001),inference(split_conjunct,[status(thm)],[c19])).
% 1.06/1.25 cnf(c21,negated_conjecture,element(skolem0002,the_carrier(skolem0001)),inference(split_conjunct,[status(thm)],[c19])).
% 1.06/1.25 fof(d9_lattice3,axiom,(![A]:(rel_str(A)=>(![B]:(![C]:(element(C,the_carrier(A))=>(relstr_set_smaller(A,B,C)<=>(![D]:(element(D,the_carrier(A))=>(in(D,B)=>related(A,D,C)))))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', d9_lattice3)).
% 1.06/1.25 fof(c61,plain,(![A]:(~rel_str(A)|(![B]:(![C]:(~element(C,the_carrier(A))|((~relstr_set_smaller(A,B,C)|(![D]:(~element(D,the_carrier(A))|(~in(D,B)|related(A,D,C)))))&((?[D]:(element(D,the_carrier(A))&(in(D,B)&~related(A,D,C))))|relstr_set_smaller(A,B,C)))))))),inference(fof_nnf,[status(thm)],[d9_lattice3])).
% 1.06/1.25 fof(c62,plain,(![X21]:(~rel_str(X21)|(![X22]:(![X23]:(~element(X23,the_carrier(X21))|((~relstr_set_smaller(X21,X22,X23)|(![X24]:(~element(X24,the_carrier(X21))|(~in(X24,X22)|related(X21,X24,X23)))))&((?[X25]:(element(X25,the_carrier(X21))&(in(X25,X22)&~related(X21,X25,X23))))|relstr_set_smaller(X21,X22,X23)))))))),inference(variable_rename,[status(thm)],[c61])).
% 1.06/1.25 fof(c64,plain,(![X21]:(![X22]:(![X23]:(![X24]:(~rel_str(X21)|(~element(X23,the_carrier(X21))|((~relstr_set_smaller(X21,X22,X23)|(~element(X24,the_carrier(X21))|(~in(X24,X22)|related(X21,X24,X23))))&((element(skolem0009(X21,X22,X23),the_carrier(X21))&(in(skolem0009(X21,X22,X23),X22)&~related(X21,skolem0009(X21,X22,X23),X23)))|relstr_set_smaller(X21,X22,X23))))))))),inference(shift_quantors,[status(thm)],[fof(c63,plain,(![X21]:(~rel_str(X21)|(![X22]:(![X23]:(~element(X23,the_carrier(X21))|((~relstr_set_smaller(X21,X22,X23)|(![X24]:(~element(X24,the_carrier(X21))|(~in(X24,X22)|related(X21,X24,X23)))))&((element(skolem0009(X21,X22,X23),the_carrier(X21))&(in(skolem0009(X21,X22,X23),X22)&~related(X21,skolem0009(X21,X22,X23),X23)))|relstr_set_smaller(X21,X22,X23)))))))),inference(skolemize,[status(esa)],[c62])).])).
% 1.06/1.25 fof(c65,plain,(![X21]:(![X22]:(![X23]:(![X24]:((~rel_str(X21)|(~element(X23,the_carrier(X21))|(~relstr_set_smaller(X21,X22,X23)|(~element(X24,the_carrier(X21))|(~in(X24,X22)|related(X21,X24,X23))))))&((~rel_str(X21)|(~element(X23,the_carrier(X21))|(element(skolem0009(X21,X22,X23),the_carrier(X21))|relstr_set_smaller(X21,X22,X23))))&((~rel_str(X21)|(~element(X23,the_carrier(X21))|(in(skolem0009(X21,X22,X23),X22)|relstr_set_smaller(X21,X22,X23))))&(~rel_str(X21)|(~element(X23,the_carrier(X21))|(~related(X21,skolem0009(X21,X22,X23),X23)|relstr_set_smaller(X21,X22,X23))))))))))),inference(distribute,[status(thm)],[c64])).
% 1.06/1.25 cnf(c68,plain,~rel_str(X116)|~element(X117,the_carrier(X116))|in(skolem0009(X116,X115,X117),X115)|relstr_set_smaller(X116,X115,X117),inference(split_conjunct,[status(thm)],[c65])).
% 1.06/1.25 cnf(c169,plain,~rel_str(skolem0001)|in(skolem0009(skolem0001,X201,skolem0002),X201)|relstr_set_smaller(skolem0001,X201,skolem0002),inference(resolution,[status(thm)],[c68, c21])).
% 1.06/1.25 cnf(c410,plain,in(skolem0009(skolem0001,X397,skolem0002),X397)|relstr_set_smaller(skolem0001,X397,skolem0002),inference(resolution,[status(thm)],[c169, c20])).
% 1.06/1.25 cnf(c1298,plain,relstr_set_smaller(skolem0001,X398,skolem0002)|~empty(X398),inference(resolution,[status(thm)],[c410, c15])).
% 1.06/1.25 cnf(c1304,plain,relstr_set_smaller(skolem0001,empty_set,skolem0002),inference(resolution,[status(thm)],[c1298, c44])).
% 1.06/1.25 cnf(c22,negated_conjecture,~relstr_set_smaller(skolem0001,empty_set,skolem0002)|~relstr_element_smaller(skolem0001,empty_set,skolem0002),inference(split_conjunct,[status(thm)],[c19])).
% 1.06/1.25 fof(d8_lattice3,axiom,(![A]:(rel_str(A)=>(![B]:(![C]:(element(C,the_carrier(A))=>(relstr_element_smaller(A,B,C)<=>(![D]:(element(D,the_carrier(A))=>(in(D,B)=>related(A,C,D)))))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', d8_lattice3)).
% 1.06/1.25 fof(c70,plain,(![A]:(~rel_str(A)|(![B]:(![C]:(~element(C,the_carrier(A))|((~relstr_element_smaller(A,B,C)|(![D]:(~element(D,the_carrier(A))|(~in(D,B)|related(A,C,D)))))&((?[D]:(element(D,the_carrier(A))&(in(D,B)&~related(A,C,D))))|relstr_element_smaller(A,B,C)))))))),inference(fof_nnf,[status(thm)],[d8_lattice3])).
% 1.06/1.25 fof(c71,plain,(![X26]:(~rel_str(X26)|(![X27]:(![X28]:(~element(X28,the_carrier(X26))|((~relstr_element_smaller(X26,X27,X28)|(![X29]:(~element(X29,the_carrier(X26))|(~in(X29,X27)|related(X26,X28,X29)))))&((?[X30]:(element(X30,the_carrier(X26))&(in(X30,X27)&~related(X26,X28,X30))))|relstr_element_smaller(X26,X27,X28)))))))),inference(variable_rename,[status(thm)],[c70])).
% 1.06/1.25 fof(c73,plain,(![X26]:(![X27]:(![X28]:(![X29]:(~rel_str(X26)|(~element(X28,the_carrier(X26))|((~relstr_element_smaller(X26,X27,X28)|(~element(X29,the_carrier(X26))|(~in(X29,X27)|related(X26,X28,X29))))&((element(skolem0010(X26,X27,X28),the_carrier(X26))&(in(skolem0010(X26,X27,X28),X27)&~related(X26,X28,skolem0010(X26,X27,X28))))|relstr_element_smaller(X26,X27,X28))))))))),inference(shift_quantors,[status(thm)],[fof(c72,plain,(![X26]:(~rel_str(X26)|(![X27]:(![X28]:(~element(X28,the_carrier(X26))|((~relstr_element_smaller(X26,X27,X28)|(![X29]:(~element(X29,the_carrier(X26))|(~in(X29,X27)|related(X26,X28,X29)))))&((element(skolem0010(X26,X27,X28),the_carrier(X26))&(in(skolem0010(X26,X27,X28),X27)&~related(X26,X28,skolem0010(X26,X27,X28))))|relstr_element_smaller(X26,X27,X28)))))))),inference(skolemize,[status(esa)],[c71])).])).
% 1.06/1.25 fof(c74,plain,(![X26]:(![X27]:(![X28]:(![X29]:((~rel_str(X26)|(~element(X28,the_carrier(X26))|(~relstr_element_smaller(X26,X27,X28)|(~element(X29,the_carrier(X26))|(~in(X29,X27)|related(X26,X28,X29))))))&((~rel_str(X26)|(~element(X28,the_carrier(X26))|(element(skolem0010(X26,X27,X28),the_carrier(X26))|relstr_element_smaller(X26,X27,X28))))&((~rel_str(X26)|(~element(X28,the_carrier(X26))|(in(skolem0010(X26,X27,X28),X27)|relstr_element_smaller(X26,X27,X28))))&(~rel_str(X26)|(~element(X28,the_carrier(X26))|(~related(X26,X28,skolem0010(X26,X27,X28))|relstr_element_smaller(X26,X27,X28))))))))))),inference(distribute,[status(thm)],[c73])).
% 1.06/1.25 cnf(c77,plain,~rel_str(X146)|~element(X147,the_carrier(X146))|in(skolem0010(X146,X148,X147),X148)|relstr_element_smaller(X146,X148,X147),inference(split_conjunct,[status(thm)],[c74])).
% 1.06/1.25 cnf(c229,plain,~rel_str(skolem0001)|in(skolem0010(skolem0001,X296,skolem0002),X296)|relstr_element_smaller(skolem0001,X296,skolem0002),inference(resolution,[status(thm)],[c77, c21])).
% 1.06/1.25 cnf(c710,plain,in(skolem0010(skolem0001,X478,skolem0002),X478)|relstr_element_smaller(skolem0001,X478,skolem0002),inference(resolution,[status(thm)],[c229, c20])).
% 1.06/1.25 cnf(c1973,plain,relstr_element_smaller(skolem0001,X481,skolem0002)|~empty(X481),inference(resolution,[status(thm)],[c710, c15])).
% 1.06/1.25 cnf(c1984,plain,relstr_element_smaller(skolem0001,empty_set,skolem0002),inference(resolution,[status(thm)],[c1973, c44])).
% 1.06/1.25 cnf(c1992,plain,~relstr_set_smaller(skolem0001,empty_set,skolem0002),inference(resolution,[status(thm)],[c1984, c22])).
% 1.06/1.25 cnf(c1998,plain,$false,inference(resolution,[status(thm)],[c1992, c1304])).
% 1.06/1.25 % SZS output end CNFRefutation
% 1.06/1.25
% 1.06/1.25 % Initial clauses : 44
% 1.06/1.25 % Processed clauses : 336
% 1.06/1.25 % Factors computed : 11
% 1.06/1.25 % Resolvents computed: 1903
% 1.06/1.25 % Tautologies deleted: 10
% 1.06/1.25 % Forward subsumed : 282
% 1.06/1.25 % Backward subsumed : 3
% 1.06/1.25 % -------- CPU Time ---------
% 1.06/1.25 % User time : 0.871 s
% 1.06/1.25 % System time : 0.014 s
% 1.06/1.25 % Total time : 0.885 s
%------------------------------------------------------------------------------