%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SYN059+1 : TPTP v8.1.2. Released v2.0.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:47:14 EDT 2024
% Result : Theorem 0.20s 0.55s
% Output : Refutation 0.20s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : SYN059+1 : TPTP v8.1.2. Released v2.0.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 20:16:23 EDT 2024
% 0.13/0.34 % CPUTime :
% 0.20/0.55 % Version: 1.5
% 0.20/0.55 % SZS status Theorem
% 0.20/0.55 % SZS output start CNFRefutation
% 0.20/0.55 fof(pel29_2,axiom,(?[Y]:big_g(Y)),file('/export/starexec/sandbox/benchmark/theBenchmark.p', pel29_2)).
% 0.20/0.55 fof(c22,plain,(?[X10]:big_g(X10)),inference(variable_rename,[status(thm)],[pel29_2])).
% 0.20/0.55 fof(c23,plain,big_g(skolem0005),inference(skolemize,[status(esa)],[c22])).
% 0.20/0.55 cnf(c24,plain,big_g(skolem0005),inference(split_conjunct,[status(thm)],[c23])).
% 0.20/0.55 fof(pel29,conjecture,(((![X]:(big_f(X)=>big_h(X)))&(![U]:(big_g(U)=>big_j(U))))<=>(![W]:(![Y]:((big_f(W)&big_g(Y))=>(big_h(W)&big_j(Y)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', pel29)).
% 0.20/0.55 fof(c0,negated_conjecture,(~(((![X]:(big_f(X)=>big_h(X)))&(![U]:(big_g(U)=>big_j(U))))<=>(![W]:(![Y]:((big_f(W)&big_g(Y))=>(big_h(W)&big_j(Y))))))),inference(assume_negation,[status(cth)],[pel29])).
% 0.20/0.55 fof(c1,negated_conjecture,((((?[X]:(big_f(X)&~big_h(X)))|(?[U]:(big_g(U)&~big_j(U))))|(?[W]:(?[Y]:((big_f(W)&big_g(Y))&(~big_h(W)|~big_j(Y))))))&(((![X]:(~big_f(X)|big_h(X)))&(![U]:(~big_g(U)|big_j(U))))|(![W]:(![Y]:((~big_f(W)|~big_g(Y))|(big_h(W)&big_j(Y))))))),inference(fof_nnf,[status(thm)],[c0])).
% 0.20/0.55 fof(c2,negated_conjecture,((((?[X2]:(big_f(X2)&~big_h(X2)))|(?[X3]:(big_g(X3)&~big_j(X3))))|(?[X4]:(?[X5]:((big_f(X4)&big_g(X5))&(~big_h(X4)|~big_j(X5))))))&(((![X6]:(~big_f(X6)|big_h(X6)))&(![X7]:(~big_g(X7)|big_j(X7))))|(![X8]:(![X9]:((~big_f(X8)|~big_g(X9))|(big_h(X8)&big_j(X9))))))),inference(variable_rename,[status(thm)],[c1])).
% 0.20/0.55 fof(c4,negated_conjecture,(![X6]:(![X7]:(![X8]:(![X9]:((((big_f(skolem0001)&~big_h(skolem0001))|(big_g(skolem0002)&~big_j(skolem0002)))|((big_f(skolem0003)&big_g(skolem0004))&(~big_h(skolem0003)|~big_j(skolem0004))))&(((~big_f(X6)|big_h(X6))&(~big_g(X7)|big_j(X7)))|((~big_f(X8)|~big_g(X9))|(big_h(X8)&big_j(X9))))))))),inference(shift_quantors,[status(thm)],[fof(c3,negated_conjecture,((((big_f(skolem0001)&~big_h(skolem0001))|(big_g(skolem0002)&~big_j(skolem0002)))|((big_f(skolem0003)&big_g(skolem0004))&(~big_h(skolem0003)|~big_j(skolem0004))))&(((![X6]:(~big_f(X6)|big_h(X6)))&(![X7]:(~big_g(X7)|big_j(X7))))|(![X8]:(![X9]:((~big_f(X8)|~big_g(X9))|(big_h(X8)&big_j(X9))))))),inference(skolemize,[status(esa)],[c2])).])).
% 0.20/0.55 fof(c5,negated_conjecture,(![X6]:(![X7]:(![X8]:(![X9]:(((((((big_f(skolem0001)|big_g(skolem0002))|big_f(skolem0003))&((big_f(skolem0001)|big_g(skolem0002))|big_g(skolem0004)))&((big_f(skolem0001)|big_g(skolem0002))|(~big_h(skolem0003)|~big_j(skolem0004))))&((((big_f(skolem0001)|~big_j(skolem0002))|big_f(skolem0003))&((big_f(skolem0001)|~big_j(skolem0002))|big_g(skolem0004)))&((big_f(skolem0001)|~big_j(skolem0002))|(~big_h(skolem0003)|~big_j(skolem0004)))))&(((((~big_h(skolem0001)|big_g(skolem0002))|big_f(skolem0003))&((~big_h(skolem0001)|big_g(skolem0002))|big_g(skolem0004)))&((~big_h(skolem0001)|big_g(skolem0002))|(~big_h(skolem0003)|~big_j(skolem0004))))&((((~big_h(skolem0001)|~big_j(skolem0002))|big_f(skolem0003))&((~big_h(skolem0001)|~big_j(skolem0002))|big_g(skolem0004)))&((~big_h(skolem0001)|~big_j(skolem0002))|(~big_h(skolem0003)|~big_j(skolem0004))))))&((((~big_f(X6)|big_h(X6))|((~big_f(X8)|~big_g(X9))|big_h(X8)))&((~big_f(X6)|big_h(X6))|((~big_f(X8)|~big_g(X9))|big_j(X9))))&(((~big_g(X7)|big_j(X7))|((~big_f(X8)|~big_g(X9))|big_h(X8)))&((~big_g(X7)|big_j(X7))|((~big_f(X8)|~big_g(X9))|big_j(X9)))))))))),inference(distribute,[status(thm)],[c4])).
% 0.20/0.55 cnf(c18,negated_conjecture,~big_f(X14)|big_h(X14)|~big_f(X12)|~big_g(X13)|big_h(X12),inference(split_conjunct,[status(thm)],[c5])).
% 0.20/0.55 cnf(c31,plain,~big_f(X16)|big_h(X16)|~big_f(X15)|big_h(X15),inference(resolution,[status(thm)],[c18, c24])).
% 0.20/0.55 cnf(c32,plain,~big_f(X17)|big_h(X17),inference(factor,[status(thm)],[c31])).
% 0.20/0.55 fof(pel29_1,axiom,(?[X]:big_f(X)),file('/export/starexec/sandbox/benchmark/theBenchmark.p', pel29_1)).
% 0.20/0.55 fof(c25,plain,(?[X11]:big_f(X11)),inference(variable_rename,[status(thm)],[pel29_1])).
% 0.20/0.55 fof(c26,plain,big_f(skolem0006),inference(skolemize,[status(esa)],[c25])).
% 0.20/0.55 cnf(c27,plain,big_f(skolem0006),inference(split_conjunct,[status(thm)],[c26])).
% 0.20/0.55 cnf(c21,negated_conjecture,~big_g(X27)|big_j(X27)|~big_f(X25)|~big_g(X26)|big_j(X26),inference(split_conjunct,[status(thm)],[c5])).
% 0.20/0.55 cnf(c46,plain,~big_g(X29)|big_j(X29)|~big_f(X28),inference(factor,[status(thm)],[c21])).
% 0.20/0.55 cnf(c52,plain,~big_g(X30)|big_j(X30),inference(resolution,[status(thm)],[c46, c27])).
% 0.20/0.55 cnf(c15,negated_conjecture,~big_h(skolem0001)|~big_j(skolem0002)|big_f(skolem0003),inference(split_conjunct,[status(thm)],[c5])).
% 0.20/0.55 cnf(c12,negated_conjecture,~big_h(skolem0001)|big_g(skolem0002)|big_f(skolem0003),inference(split_conjunct,[status(thm)],[c5])).
% 0.20/0.55 cnf(c6,negated_conjecture,big_f(skolem0001)|big_g(skolem0002)|big_f(skolem0003),inference(split_conjunct,[status(thm)],[c5])).
% 0.20/0.55 cnf(c37,plain,big_h(skolem0001)|big_g(skolem0002)|big_f(skolem0003),inference(resolution,[status(thm)],[c32, c6])).
% 0.20/0.55 cnf(c41,plain,big_g(skolem0002)|big_f(skolem0003),inference(resolution,[status(thm)],[c37, c12])).
% 0.20/0.55 cnf(c56,plain,big_j(skolem0002)|big_f(skolem0003),inference(resolution,[status(thm)],[c52, c41])).
% 0.20/0.55 cnf(c70,plain,big_f(skolem0003)|~big_h(skolem0001),inference(resolution,[status(thm)],[c56, c15])).
% 0.20/0.55 cnf(c9,negated_conjecture,big_f(skolem0001)|~big_j(skolem0002)|big_f(skolem0003),inference(split_conjunct,[status(thm)],[c5])).
% 0.20/0.55 cnf(c69,plain,big_f(skolem0003)|big_f(skolem0001),inference(resolution,[status(thm)],[c56, c9])).
% 0.20/0.55 cnf(c89,plain,big_f(skolem0003)|big_h(skolem0001),inference(resolution,[status(thm)],[c69, c32])).
% 0.20/0.55 cnf(c105,plain,big_f(skolem0003),inference(resolution,[status(thm)],[c89, c70])).
% 0.20/0.55 cnf(c106,plain,big_h(skolem0003),inference(resolution,[status(thm)],[c105, c32])).
% 0.20/0.55 cnf(c14,negated_conjecture,~big_h(skolem0001)|big_g(skolem0002)|~big_h(skolem0003)|~big_j(skolem0004),inference(split_conjunct,[status(thm)],[c5])).
% 0.20/0.55 cnf(c13,negated_conjecture,~big_h(skolem0001)|big_g(skolem0002)|big_g(skolem0004),inference(split_conjunct,[status(thm)],[c5])).
% 0.20/0.55 cnf(c7,negated_conjecture,big_f(skolem0001)|big_g(skolem0002)|big_g(skolem0004),inference(split_conjunct,[status(thm)],[c5])).
% 0.20/0.55 cnf(c39,plain,big_h(skolem0001)|big_g(skolem0002)|big_g(skolem0004),inference(resolution,[status(thm)],[c32, c7])).
% 0.20/0.55 cnf(c45,plain,big_g(skolem0002)|big_g(skolem0004),inference(resolution,[status(thm)],[c39, c13])).
% 0.20/0.55 cnf(c54,plain,big_j(skolem0004)|big_g(skolem0002),inference(resolution,[status(thm)],[c52, c45])).
% 0.20/0.55 cnf(c60,plain,big_g(skolem0002)|~big_h(skolem0001)|~big_h(skolem0003),inference(resolution,[status(thm)],[c54, c14])).
% 0.20/0.55 cnf(c107,plain,big_g(skolem0002)|~big_h(skolem0001),inference(resolution,[status(thm)],[c60, c106])).
% 0.20/0.55 cnf(c8,negated_conjecture,big_f(skolem0001)|big_g(skolem0002)|~big_h(skolem0003)|~big_j(skolem0004),inference(split_conjunct,[status(thm)],[c5])).
% 0.20/0.55 cnf(c62,plain,big_g(skolem0002)|big_f(skolem0001)|~big_h(skolem0003),inference(resolution,[status(thm)],[c54, c8])).
% 0.20/0.55 cnf(c108,plain,big_g(skolem0002)|big_f(skolem0001),inference(resolution,[status(thm)],[c62, c106])).
% 0.20/0.55 cnf(c110,plain,big_g(skolem0002)|big_h(skolem0001),inference(resolution,[status(thm)],[c108, c32])).
% 0.20/0.55 cnf(c113,plain,big_g(skolem0002),inference(resolution,[status(thm)],[c110, c107])).
% 0.20/0.55 cnf(c114,plain,big_j(skolem0002),inference(resolution,[status(thm)],[c113, c52])).
% 0.20/0.55 cnf(c11,negated_conjecture,big_f(skolem0001)|~big_j(skolem0002)|~big_h(skolem0003)|~big_j(skolem0004),inference(split_conjunct,[status(thm)],[c5])).
% 0.20/0.55 cnf(c10,negated_conjecture,big_f(skolem0001)|~big_j(skolem0002)|big_g(skolem0004),inference(split_conjunct,[status(thm)],[c5])).
% 0.20/0.55 cnf(c55,plain,big_j(skolem0002)|big_g(skolem0004),inference(resolution,[status(thm)],[c52, c45])).
% 0.20/0.55 cnf(c67,plain,big_g(skolem0004)|big_f(skolem0001),inference(resolution,[status(thm)],[c55, c10])).
% 0.20/0.55 cnf(c86,plain,big_f(skolem0001)|big_j(skolem0004),inference(resolution,[status(thm)],[c67, c52])).
% 0.20/0.55 cnf(c93,plain,big_f(skolem0001)|~big_j(skolem0002)|~big_h(skolem0003),inference(resolution,[status(thm)],[c86, c11])).
% 0.20/0.55 cnf(c115,plain,big_f(skolem0001)|~big_j(skolem0002),inference(resolution,[status(thm)],[c93, c106])).
% 0.20/0.55 cnf(c116,plain,big_f(skolem0001),inference(resolution,[status(thm)],[c115, c114])).
% 0.20/0.55 cnf(c117,plain,big_h(skolem0001),inference(resolution,[status(thm)],[c116, c32])).
% 0.20/0.55 cnf(c17,negated_conjecture,~big_h(skolem0001)|~big_j(skolem0002)|~big_h(skolem0003)|~big_j(skolem0004),inference(split_conjunct,[status(thm)],[c5])).
% 0.20/0.55 cnf(c16,negated_conjecture,~big_h(skolem0001)|~big_j(skolem0002)|big_g(skolem0004),inference(split_conjunct,[status(thm)],[c5])).
% 0.20/0.55 cnf(c66,plain,big_g(skolem0004)|~big_h(skolem0001),inference(resolution,[status(thm)],[c55, c16])).
% 0.20/0.55 cnf(c87,plain,big_g(skolem0004)|big_h(skolem0001),inference(resolution,[status(thm)],[c67, c32])).
% 0.20/0.55 cnf(c96,plain,big_g(skolem0004),inference(resolution,[status(thm)],[c87, c66])).
% 0.20/0.55 cnf(c98,plain,big_j(skolem0004),inference(resolution,[status(thm)],[c96, c52])).
% 0.20/0.55 cnf(c99,plain,~big_h(skolem0001)|~big_j(skolem0002)|~big_h(skolem0003),inference(resolution,[status(thm)],[c98, c17])).
% 0.20/0.55 cnf(c118,plain,~big_h(skolem0001)|~big_j(skolem0002),inference(resolution,[status(thm)],[c99, c106])).
% 0.20/0.55 cnf(c119,plain,~big_h(skolem0001),inference(resolution,[status(thm)],[c118, c114])).
% 0.20/0.55 cnf(c120,plain,$false,inference(resolution,[status(thm)],[c119, c117])).
% 0.20/0.55 % SZS output end CNFRefutation
% 0.20/0.55
% 0.20/0.55 % Initial clauses : 18
% 0.20/0.55 % Processed clauses : 59
% 0.20/0.55 % Factors computed : 2
% 0.20/0.55 % Resolvents computed: 91
% 0.20/0.55 % Tautologies deleted: 0
% 0.20/0.55 % Forward subsumed : 40
% 0.20/0.55 % Backward subsumed : 44
% 0.20/0.55 % -------- CPU Time ---------
% 0.20/0.55 % User time : 0.197 s
% 0.20/0.55 % System time : 0.012 s
% 0.20/0.55 % Total time : 0.209 s
%------------------------------------------------------------------------------