%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SYN069+1 : TPTP v8.1.2. Released v2.0.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n019.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:47:16 EDT 2024
% Result : Theorem 0.20s 0.52s
% Output : Refutation 0.20s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.05/0.14 % Problem : SYN069+1 : TPTP v8.1.2. Released v2.0.0.
% 0.05/0.15 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.36 % Computer : n019.cluster.edu
% 0.13/0.36 % Model : x86_64 x86_64
% 0.13/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.36 % Memory : 8042.1875MB
% 0.13/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.36 % CPULimit : 300
% 0.13/0.36 % WCLimit : 300
% 0.13/0.36 % DateTime : Wed May 8 20:00:08 EDT 2024
% 0.13/0.36 % CPUTime :
% 0.20/0.52 % Version: 1.5
% 0.20/0.52 % SZS status Theorem
% 0.20/0.52 % SZS output start CNFRefutation
% 0.20/0.52 fof(pel45_3,axiom,(?[X]:((big_f(X)&(![Y]:(big_h(X,Y)=>big_l(Y))))&(![Y1]:((big_g(Y1)&big_h(X,Y1))=>big_j(X,Y1))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', pel45_3)).
% 0.20/0.52 fof(c7,plain,(?[X]:((big_f(X)&(![Y]:(~big_h(X,Y)|big_l(Y))))&(![Y1]:((~big_g(Y1)|~big_h(X,Y1))|big_j(X,Y1))))),inference(fof_nnf,[status(thm)],[pel45_3])).
% 0.20/0.52 fof(c8,plain,(?[X4]:((big_f(X4)&(![X5]:(~big_h(X4,X5)|big_l(X5))))&(![X6]:((~big_g(X6)|~big_h(X4,X6))|big_j(X4,X6))))),inference(variable_rename,[status(thm)],[c7])).
% 0.20/0.52 fof(c10,plain,(![X5]:(![X6]:((big_f(skolem0002)&(~big_h(skolem0002,X5)|big_l(X5)))&((~big_g(X6)|~big_h(skolem0002,X6))|big_j(skolem0002,X6))))),inference(shift_quantors,[status(thm)],[fof(c9,plain,((big_f(skolem0002)&(![X5]:(~big_h(skolem0002,X5)|big_l(X5))))&(![X6]:((~big_g(X6)|~big_h(skolem0002,X6))|big_j(skolem0002,X6)))),inference(skolemize,[status(esa)],[c8])).])).
% 0.20/0.52 cnf(c12,plain,~big_h(skolem0002,X15)|big_l(X15),inference(split_conjunct,[status(thm)],[c10])).
% 0.20/0.52 cnf(c11,plain,big_f(skolem0002),inference(split_conjunct,[status(thm)],[c10])).
% 0.20/0.52 fof(pel45,conjecture,(?[X]:(big_f(X)&(~(?[Y]:(big_g(Y)&big_h(X,Y)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', pel45)).
% 0.20/0.52 fof(c0,negated_conjecture,(~(?[X]:(big_f(X)&(~(?[Y]:(big_g(Y)&big_h(X,Y))))))),inference(assume_negation,[status(cth)],[pel45])).
% 0.20/0.52 fof(c1,negated_conjecture,(![X]:(~big_f(X)|(?[Y]:(big_g(Y)&big_h(X,Y))))),inference(fof_nnf,[status(thm)],[c0])).
% 0.20/0.52 fof(c2,negated_conjecture,(![X2]:(~big_f(X2)|(?[X3]:(big_g(X3)&big_h(X2,X3))))),inference(variable_rename,[status(thm)],[c1])).
% 0.20/0.52 fof(c3,negated_conjecture,(![X2]:(~big_f(X2)|(big_g(skolem0001(X2))&big_h(X2,skolem0001(X2))))),inference(skolemize,[status(esa)],[c2])).
% 0.20/0.52 fof(c4,negated_conjecture,(![X2]:((~big_f(X2)|big_g(skolem0001(X2)))&(~big_f(X2)|big_h(X2,skolem0001(X2))))),inference(distribute,[status(thm)],[c3])).
% 0.20/0.52 cnf(c6,negated_conjecture,~big_f(X16)|big_h(X16,skolem0001(X16)),inference(split_conjunct,[status(thm)],[c4])).
% 0.20/0.52 cnf(c33,plain,big_h(skolem0002,skolem0001(skolem0002)),inference(resolution,[status(thm)],[c6, c11])).
% 0.20/0.52 cnf(c34,plain,big_l(skolem0001(skolem0002)),inference(resolution,[status(thm)],[c33, c12])).
% 0.20/0.52 fof(pel45_2,axiom,(~(?[Y]:(big_l(Y)&big_k(Y)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', pel45_2)).
% 0.20/0.52 fof(c14,plain,(![Y]:(~big_l(Y)|~big_k(Y))),inference(fof_nnf,[status(thm)],[pel45_2])).
% 0.20/0.52 fof(c15,plain,(![X7]:(~big_l(X7)|~big_k(X7))),inference(variable_rename,[status(thm)],[c14])).
% 0.20/0.52 cnf(c16,plain,~big_l(X13)|~big_k(X13),inference(split_conjunct,[status(thm)],[c15])).
% 0.20/0.52 fof(pel45_1,axiom,(![X]:((big_f(X)&(![Y]:((big_g(Y)&big_h(X,Y))=>big_j(X,Y))))=>(![Y1]:((big_g(Y1)&big_h(X,Y1))&big_k(Y1))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', pel45_1)).
% 0.20/0.52 fof(c17,plain,(![X]:((~big_f(X)|(?[Y]:((big_g(Y)&big_h(X,Y))&~big_j(X,Y))))|(![Y1]:((big_g(Y1)&big_h(X,Y1))&big_k(Y1))))),inference(fof_nnf,[status(thm)],[pel45_1])).
% 0.20/0.52 fof(c18,plain,(![X]:((~big_f(X)|(?[Y]:((big_g(Y)&big_h(X,Y))&~big_j(X,Y))))|(((![Y1]:big_g(Y1))&(![Y1]:big_h(X,Y1)))&(![Y1]:big_k(Y1))))),inference(shift_quantors,[status(thm)],[c17])).
% 0.20/0.52 fof(c19,plain,(![X8]:((~big_f(X8)|(?[X9]:((big_g(X9)&big_h(X8,X9))&~big_j(X8,X9))))|(((![X10]:big_g(X10))&(![X11]:big_h(X8,X11)))&(![X12]:big_k(X12))))),inference(variable_rename,[status(thm)],[c18])).
% 0.20/0.52 fof(c21,plain,(![X8]:(![X10]:(![X11]:(![X12]:((~big_f(X8)|((big_g(skolem0003(X8))&big_h(X8,skolem0003(X8)))&~big_j(X8,skolem0003(X8))))|((big_g(X10)&big_h(X8,X11))&big_k(X12))))))),inference(shift_quantors,[status(thm)],[fof(c20,plain,(![X8]:((~big_f(X8)|((big_g(skolem0003(X8))&big_h(X8,skolem0003(X8)))&~big_j(X8,skolem0003(X8))))|(((![X10]:big_g(X10))&(![X11]:big_h(X8,X11)))&(![X12]:big_k(X12))))),inference(skolemize,[status(esa)],[c19])).])).
% 0.20/0.52 fof(c22,plain,(![X8]:(![X10]:(![X11]:(![X12]:((((((~big_f(X8)|big_g(skolem0003(X8)))|big_g(X10))&((~big_f(X8)|big_g(skolem0003(X8)))|big_h(X8,X11)))&((~big_f(X8)|big_g(skolem0003(X8)))|big_k(X12)))&((((~big_f(X8)|big_h(X8,skolem0003(X8)))|big_g(X10))&((~big_f(X8)|big_h(X8,skolem0003(X8)))|big_h(X8,X11)))&((~big_f(X8)|big_h(X8,skolem0003(X8)))|big_k(X12))))&((((~big_f(X8)|~big_j(X8,skolem0003(X8)))|big_g(X10))&((~big_f(X8)|~big_j(X8,skolem0003(X8)))|big_h(X8,X11)))&((~big_f(X8)|~big_j(X8,skolem0003(X8)))|big_k(X12)))))))),inference(distribute,[status(thm)],[c21])).
% 0.20/0.52 cnf(c28,plain,~big_f(X33)|big_h(X33,skolem0003(X33))|big_k(X34),inference(split_conjunct,[status(thm)],[c22])).
% 0.20/0.52 cnf(c44,plain,big_h(skolem0002,skolem0003(skolem0002))|big_k(X35),inference(resolution,[status(thm)],[c28, c11])).
% 0.20/0.52 cnf(c45,plain,big_k(X36)|big_l(skolem0003(skolem0002)),inference(resolution,[status(thm)],[c44, c12])).
% 0.20/0.52 cnf(c48,plain,big_l(skolem0003(skolem0002))|~big_l(X39),inference(resolution,[status(thm)],[c45, c16])).
% 0.20/0.52 cnf(c51,plain,big_l(skolem0003(skolem0002)),inference(resolution,[status(thm)],[c48, c34])).
% 0.20/0.52 cnf(c31,plain,~big_f(X45)|~big_j(X45,skolem0003(X45))|big_k(X46),inference(split_conjunct,[status(thm)],[c22])).
% 0.20/0.52 cnf(c23,plain,~big_f(X17)|big_g(skolem0003(X17))|big_g(X18),inference(split_conjunct,[status(thm)],[c22])).
% 0.20/0.52 cnf(c35,plain,big_g(skolem0003(skolem0002))|big_g(X19),inference(resolution,[status(thm)],[c23, c11])).
% 0.20/0.52 cnf(c36,plain,big_g(skolem0003(skolem0002)),inference(factor,[status(thm)],[c35])).
% 0.20/0.52 cnf(c13,plain,~big_g(X20)|~big_h(skolem0002,X20)|big_j(skolem0002,X20),inference(split_conjunct,[status(thm)],[c10])).
% 0.20/0.52 cnf(c47,plain,big_h(skolem0002,skolem0003(skolem0002))|~big_l(X42),inference(resolution,[status(thm)],[c44, c16])).
% 0.20/0.52 cnf(c52,plain,big_h(skolem0002,skolem0003(skolem0002)),inference(resolution,[status(thm)],[c47, c51])).
% 0.20/0.52 cnf(c55,plain,~big_g(skolem0003(skolem0002))|big_j(skolem0002,skolem0003(skolem0002)),inference(resolution,[status(thm)],[c52, c13])).
% 0.20/0.52 cnf(c57,plain,big_j(skolem0002,skolem0003(skolem0002)),inference(resolution,[status(thm)],[c55, c36])).
% 0.20/0.52 cnf(c60,plain,~big_f(skolem0002)|big_k(X51),inference(resolution,[status(thm)],[c57, c31])).
% 0.20/0.52 cnf(c62,plain,big_k(X52),inference(resolution,[status(thm)],[c60, c11])).
% 0.20/0.52 cnf(c63,plain,~big_l(X53),inference(resolution,[status(thm)],[c62, c16])).
% 0.20/0.52 cnf(c64,plain,$false,inference(resolution,[status(thm)],[c63, c51])).
% 0.20/0.52 % SZS output end CNFRefutation
% 0.20/0.52
% 0.20/0.52 % Initial clauses : 15
% 0.20/0.52 % Processed clauses : 37
% 0.20/0.52 % Factors computed : 1
% 0.20/0.52 % Resolvents computed: 33
% 0.20/0.52 % Tautologies deleted: 0
% 0.20/0.52 % Forward subsumed : 8
% 0.20/0.52 % Backward subsumed : 22
% 0.20/0.52 % -------- CPU Time ---------
% 0.20/0.52 % User time : 0.151 s
% 0.20/0.52 % System time : 0.010 s
% 0.20/0.52 % Total time : 0.161 s
%------------------------------------------------------------------------------