%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SEU121+1 : TPTP v8.1.2. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n010.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 0.19s 0.58s
% Output : Refutation 0.19s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : SEU121+1 : TPTP v8.1.2. Released v3.3.0.
% 0.07/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.34 % Computer : n010.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Wed May 8 11:59:08 EDT 2024
% 0.13/0.34 % CPUTime :
% 0.19/0.58 % Version: 1.5
% 0.19/0.58 % SZS status Theorem
% 0.19/0.58 % SZS output start CNFRefutation
% 0.19/0.58 fof(t1_xboole_1,conjecture,(![A]:(![B]:(![C]:((subset(A,B)&subset(B,C))=>subset(A,C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', t1_xboole_1)).
% 0.19/0.58 fof(c12,negated_conjecture,(~(![A]:(![B]:(![C]:((subset(A,B)&subset(B,C))=>subset(A,C)))))),inference(assume_negation,[status(cth)],[t1_xboole_1])).
% 0.19/0.58 fof(c13,negated_conjecture,(?[A]:(?[B]:(?[C]:((subset(A,B)&subset(B,C))&~subset(A,C))))),inference(fof_nnf,[status(thm)],[c12])).
% 0.19/0.58 fof(c14,negated_conjecture,(?[X7]:(?[X8]:(?[X9]:((subset(X7,X8)&subset(X8,X9))&~subset(X7,X9))))),inference(variable_rename,[status(thm)],[c13])).
% 0.19/0.58 fof(c15,negated_conjecture,((subset(skolem0001,skolem0002)&subset(skolem0002,skolem0003))&~subset(skolem0001,skolem0003)),inference(skolemize,[status(esa)],[c14])).
% 0.19/0.58 cnf(c18,negated_conjecture,~subset(skolem0001,skolem0003),inference(split_conjunct,[status(thm)],[c15])).
% 0.19/0.58 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.19/0.58 fof(c31,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.19/0.58 fof(c32,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)],[c31])).
% 0.19/0.58 fof(c33,plain,((![X13]:(![X14]:(~subset(X13,X14)|(![X15]:(~in(X15,X13)|in(X15,X14))))))&(![X16]:(![X17]:((?[X18]:(in(X18,X16)&~in(X18,X17)))|subset(X16,X17))))),inference(variable_rename,[status(thm)],[c32])).
% 0.19/0.58 fof(c35,plain,(![X13]:(![X14]:(![X15]:(![X16]:(![X17]:((~subset(X13,X14)|(~in(X15,X13)|in(X15,X14)))&((in(skolem0006(X16,X17),X16)&~in(skolem0006(X16,X17),X17))|subset(X16,X17)))))))),inference(shift_quantors,[status(thm)],[fof(c34,plain,((![X13]:(![X14]:(~subset(X13,X14)|(![X15]:(~in(X15,X13)|in(X15,X14))))))&(![X16]:(![X17]:((in(skolem0006(X16,X17),X16)&~in(skolem0006(X16,X17),X17))|subset(X16,X17))))),inference(skolemize,[status(esa)],[c33])).])).
% 0.19/0.58 fof(c36,plain,(![X13]:(![X14]:(![X15]:(![X16]:(![X17]:((~subset(X13,X14)|(~in(X15,X13)|in(X15,X14)))&((in(skolem0006(X16,X17),X16)|subset(X16,X17))&(~in(skolem0006(X16,X17),X17)|subset(X16,X17))))))))),inference(distribute,[status(thm)],[c35])).
% 0.19/0.58 cnf(c39,plain,~in(skolem0006(X65,X64),X64)|subset(X65,X64),inference(split_conjunct,[status(thm)],[c36])).
% 0.19/0.58 cnf(c17,negated_conjecture,subset(skolem0002,skolem0003),inference(split_conjunct,[status(thm)],[c15])).
% 0.19/0.58 cnf(c37,plain,~subset(X53,X52)|~in(X51,X53)|in(X51,X52),inference(split_conjunct,[status(thm)],[c36])).
% 0.19/0.58 cnf(c16,negated_conjecture,subset(skolem0001,skolem0002),inference(split_conjunct,[status(thm)],[c15])).
% 0.19/0.58 cnf(c38,plain,in(skolem0006(X58,X57),X58)|subset(X58,X57),inference(split_conjunct,[status(thm)],[c36])).
% 0.19/0.58 cnf(c69,plain,in(skolem0006(skolem0001,skolem0003),skolem0001),inference(resolution,[status(thm)],[c38, c18])).
% 0.19/0.58 cnf(c88,plain,~subset(skolem0001,X115)|in(skolem0006(skolem0001,skolem0003),X115),inference(resolution,[status(thm)],[c69, c37])).
% 0.19/0.58 cnf(c123,plain,in(skolem0006(skolem0001,skolem0003),skolem0002),inference(resolution,[status(thm)],[c88, c16])).
% 0.19/0.58 cnf(c126,plain,~subset(skolem0002,X142)|in(skolem0006(skolem0001,skolem0003),X142),inference(resolution,[status(thm)],[c123, c37])).
% 0.19/0.58 cnf(c167,plain,in(skolem0006(skolem0001,skolem0003),skolem0003),inference(resolution,[status(thm)],[c126, c17])).
% 0.19/0.58 cnf(c175,plain,subset(skolem0001,skolem0003),inference(resolution,[status(thm)],[c167, c39])).
% 0.19/0.58 cnf(c178,plain,$false,inference(resolution,[status(thm)],[c175, c18])).
% 0.19/0.58 % SZS output end CNFRefutation
% 0.19/0.58
% 0.19/0.58 % Initial clauses : 21
% 0.19/0.58 % Processed clauses : 64
% 0.19/0.58 % Factors computed : 8
% 0.19/0.58 % Resolvents computed: 129
% 0.19/0.58 % Tautologies deleted: 3
% 0.19/0.58 % Forward subsumed : 47
% 0.19/0.58 % Backward subsumed : 5
% 0.19/0.58 % -------- CPU Time ---------
% 0.19/0.58 % User time : 0.217 s
% 0.19/0.58 % System time : 0.017 s
% 0.19/0.58 % Total time : 0.234 s
%------------------------------------------------------------------------------