%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SYN386+1 : TPTP v8.1.2. Released v2.0.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:48:06 EDT 2024
% Result : Theorem 0.21s 0.53s
% Output : Refutation 0.21s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.13 % Problem : SYN386+1 : TPTP v8.1.2. Released v2.0.0.
% 0.12/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.35 % Computer : n025.cluster.edu
% 0.14/0.35 % Model : x86_64 x86_64
% 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.35 % Memory : 8042.1875MB
% 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.35 % CPULimit : 300
% 0.14/0.35 % WCLimit : 300
% 0.14/0.35 % DateTime : Wed May 8 19:48:38 EDT 2024
% 0.14/0.35 % CPUTime :
% 0.21/0.53 % Version: 1.5
% 0.21/0.53 % SZS status Theorem
% 0.21/0.53 % SZS output start CNFRefutation
% 0.21/0.53 fof(x2138,conjecture,((((![X]:(?[Y]:big_f(X,Y)))&(?[X]:(![E]:(?[N]:(![W]:(big_s(N,W)=>big_d(W,X,E)))))))&(![E]:(?[D]:(![A]:(![B]:(big_d(A,B,D)=>(![Y]:(![Z]:((big_f(A,Y)&big_f(B,Z))=>big_d(Y,Z,E))))))))))=>(?[Y]:(![E]:(?[M]:(![W]:(big_s(M,W)=>(![Z]:(big_f(W,Z)=>big_d(Z,Y,E))))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', x2138)).
% 0.21/0.53 fof(c0,negated_conjecture,(~((((![X]:(?[Y]:big_f(X,Y)))&(?[X]:(![E]:(?[N]:(![W]:(big_s(N,W)=>big_d(W,X,E)))))))&(![E]:(?[D]:(![A]:(![B]:(big_d(A,B,D)=>(![Y]:(![Z]:((big_f(A,Y)&big_f(B,Z))=>big_d(Y,Z,E))))))))))=>(?[Y]:(![E]:(?[M]:(![W]:(big_s(M,W)=>(![Z]:(big_f(W,Z)=>big_d(Z,Y,E)))))))))),inference(assume_negation,[status(cth)],[x2138])).
% 0.21/0.53 fof(c1,negated_conjecture,((((![X]:(?[Y]:big_f(X,Y)))&(?[X]:(![E]:(?[N]:(![W]:(~big_s(N,W)|big_d(W,X,E)))))))&(![E]:(?[D]:(![A]:(![B]:(~big_d(A,B,D)|(![Y]:(![Z]:((~big_f(A,Y)|~big_f(B,Z))|big_d(Y,Z,E))))))))))&(![Y]:(?[E]:(![M]:(?[W]:(big_s(M,W)&(?[Z]:(big_f(W,Z)&~big_d(Z,Y,E))))))))),inference(fof_nnf,[status(thm)],[c0])).
% 0.21/0.53 fof(c2,negated_conjecture,((((![X2]:(?[X3]:big_f(X2,X3)))&(?[X4]:(![X5]:(?[X6]:(![X7]:(~big_s(X6,X7)|big_d(X7,X4,X5)))))))&(![X8]:(?[X9]:(![X10]:(![X11]:(~big_d(X10,X11,X9)|(![X12]:(![X13]:((~big_f(X10,X12)|~big_f(X11,X13))|big_d(X12,X13,X8))))))))))&(![X14]:(?[X15]:(![X16]:(?[X17]:(big_s(X16,X17)&(?[X18]:(big_f(X17,X18)&~big_d(X18,X14,X15))))))))),inference(variable_rename,[status(thm)],[c1])).
% 0.21/0.53 fof(c4,negated_conjecture,(![X2]:(![X5]:(![X7]:(![X8]:(![X10]:(![X11]:(![X12]:(![X13]:(![X14]:(![X16]:(((big_f(X2,skolem0001(X2))&(~big_s(skolem0003(X5),X7)|big_d(X7,skolem0002,X5)))&(~big_d(X10,X11,skolem0004(X8))|((~big_f(X10,X12)|~big_f(X11,X13))|big_d(X12,X13,X8))))&(big_s(X16,skolem0006(X14,X16))&(big_f(skolem0006(X14,X16),skolem0007(X14,X16))&~big_d(skolem0007(X14,X16),X14,skolem0005(X14))))))))))))))),inference(shift_quantors,[status(thm)],[fof(c3,negated_conjecture,((((![X2]:big_f(X2,skolem0001(X2)))&(![X5]:(![X7]:(~big_s(skolem0003(X5),X7)|big_d(X7,skolem0002,X5)))))&(![X8]:(![X10]:(![X11]:(~big_d(X10,X11,skolem0004(X8))|(![X12]:(![X13]:((~big_f(X10,X12)|~big_f(X11,X13))|big_d(X12,X13,X8)))))))))&(![X14]:(![X16]:(big_s(X16,skolem0006(X14,X16))&(big_f(skolem0006(X14,X16),skolem0007(X14,X16))&~big_d(skolem0007(X14,X16),X14,skolem0005(X14))))))),inference(skolemize,[status(esa)],[c2])).])).
% 0.21/0.53 cnf(c10,negated_conjecture,~big_d(skolem0007(X25,X24),X25,skolem0005(X25)),inference(split_conjunct,[status(thm)],[c4])).
% 0.21/0.53 cnf(c5,negated_conjecture,big_f(X19,skolem0001(X19)),inference(split_conjunct,[status(thm)],[c4])).
% 0.21/0.53 cnf(c9,negated_conjecture,big_f(skolem0006(X23,X22),skolem0007(X23,X22)),inference(split_conjunct,[status(thm)],[c4])).
% 0.21/0.53 cnf(c7,negated_conjecture,~big_d(X28,X31,skolem0004(X30))|~big_f(X28,X32)|~big_f(X31,X29)|big_d(X32,X29,X30),inference(split_conjunct,[status(thm)],[c4])).
% 0.21/0.53 cnf(c8,negated_conjecture,big_s(X20,skolem0006(X21,X20)),inference(split_conjunct,[status(thm)],[c4])).
% 0.21/0.53 cnf(c6,negated_conjecture,~big_s(skolem0003(X27),X26)|big_d(X26,skolem0002,X27),inference(split_conjunct,[status(thm)],[c4])).
% 0.21/0.53 cnf(c11,plain,big_d(skolem0006(X34,skolem0003(X33)),skolem0002,X33),inference(resolution,[status(thm)],[c6, c8])).
% 0.21/0.53 cnf(c12,plain,~big_f(skolem0006(X35,skolem0003(skolem0004(X38))),X37)|~big_f(skolem0002,X36)|big_d(X37,X36,X38),inference(resolution,[status(thm)],[c11, c7])).
% 0.21/0.53 cnf(c14,plain,~big_f(skolem0002,X40)|big_d(skolem0007(X41,skolem0003(skolem0004(X39))),X40,X39),inference(resolution,[status(thm)],[c12, c9])).
% 0.21/0.53 cnf(c15,plain,big_d(skolem0007(X43,skolem0003(skolem0004(X42))),skolem0001(skolem0002),X42),inference(resolution,[status(thm)],[c14, c5])).
% 0.21/0.53 cnf(c17,plain,$false,inference(resolution,[status(thm)],[c15, c10])).
% 0.21/0.53 % SZS output end CNFRefutation
% 0.21/0.53
% 0.21/0.53 % Initial clauses : 6
% 0.21/0.53 % Processed clauses : 10
% 0.21/0.53 % Factors computed : 0
% 0.21/0.53 % Resolvents computed: 7
% 0.21/0.53 % Tautologies deleted: 0
% 0.21/0.53 % Forward subsumed : 0
% 0.21/0.53 % Backward subsumed : 0
% 0.21/0.53 % -------- CPU Time ---------
% 0.21/0.53 % User time : 0.158 s
% 0.21/0.53 % System time : 0.017 s
% 0.21/0.53 % Total time : 0.175 s
%------------------------------------------------------------------------------