%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SYN414+1 : TPTP v8.1.2. Released v2.0.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n015.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:10 EDT 2024
% Result : CounterSatisfiable 0.46s 0.68s
% Output : Saturation 0.46s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : SYN414+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 : n015.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:14:08 EDT 2024
% 0.13/0.34 % CPUTime :
% 0.46/0.68 % Version: 1.5
% 0.46/0.68 % SZS status CounterSatisfiable
% 0.46/0.68 % SZS output start Saturation
% 0.46/0.68 fof(kalish265,conjecture,((![X]:((?[Y]:(h(X,Y)&f(Y)))=>(?[Z]:(h(X,Z)&g(Z)))))<=>(![U]:(![V]:(![W]:((h(U,V)&f(V))=>(h(U,W)&g(W))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', kalish265)).
% 0.46/0.68 fof(c0,negated_conjecture,(~((![X]:((?[Y]:(h(X,Y)&f(Y)))=>(?[Z]:(h(X,Z)&g(Z)))))<=>(![U]:(![V]:(![W]:((h(U,V)&f(V))=>(h(U,W)&g(W)))))))),inference(assume_negation,[status(cth)],[kalish265])).
% 0.46/0.68 fof(c1,negated_conjecture,(((?[X]:((?[Y]:(h(X,Y)&f(Y)))&(![Z]:(~h(X,Z)|~g(Z)))))|(?[U]:(?[V]:(?[W]:((h(U,V)&f(V))&(~h(U,W)|~g(W)))))))&((![X]:((![Y]:(~h(X,Y)|~f(Y)))|(?[Z]:(h(X,Z)&g(Z)))))|(![U]:(![V]:(![W]:((~h(U,V)|~f(V))|(h(U,W)&g(W)))))))),inference(fof_nnf,[status(thm)],[c0])).
% 0.46/0.68 fof(c2,negated_conjecture,(((?[X]:((?[Y]:(h(X,Y)&f(Y)))&(![Z]:(~h(X,Z)|~g(Z)))))|(?[U]:((?[V]:(h(U,V)&f(V)))&((?[W]:~h(U,W))|(?[W]:~g(W))))))&((![X]:((![Y]:(~h(X,Y)|~f(Y)))|(?[Z]:(h(X,Z)&g(Z)))))|(![U]:((![V]:(~h(U,V)|~f(V)))|((![W]:h(U,W))&(![W]:g(W))))))),inference(shift_quantors,[status(thm)],[c1])).
% 0.46/0.68 fof(c3,negated_conjecture,(((?[X2]:((?[X3]:(h(X2,X3)&f(X3)))&(![X4]:(~h(X2,X4)|~g(X4)))))|(?[X5]:((?[X6]:(h(X5,X6)&f(X6)))&((?[X7]:~h(X5,X7))|(?[X8]:~g(X8))))))&((![X9]:((![X10]:(~h(X9,X10)|~f(X10)))|(?[X11]:(h(X9,X11)&g(X11)))))|(![X12]:((![X13]:(~h(X12,X13)|~f(X13)))|((![X14]:h(X12,X14))&(![X15]:g(X15))))))),inference(variable_rename,[status(thm)],[c2])).
% 0.46/0.68 fof(c5,negated_conjecture,(![X4]:(![X9]:(![X10]:(![X12]:(![X13]:(![X14]:(![X15]:((((h(skolem0001,skolem0002)&f(skolem0002))&(~h(skolem0001,X4)|~g(X4)))|((h(skolem0003,skolem0004)&f(skolem0004))&(~h(skolem0003,skolem0005)|~g(skolem0006))))&(((~h(X9,X10)|~f(X10))|(h(X9,skolem0007(X9))&g(skolem0007(X9))))|((~h(X12,X13)|~f(X13))|(h(X12,X14)&g(X15)))))))))))),inference(shift_quantors,[status(thm)],[fof(c4,negated_conjecture,((((h(skolem0001,skolem0002)&f(skolem0002))&(![X4]:(~h(skolem0001,X4)|~g(X4))))|((h(skolem0003,skolem0004)&f(skolem0004))&(~h(skolem0003,skolem0005)|~g(skolem0006))))&((![X9]:((![X10]:(~h(X9,X10)|~f(X10)))|(h(X9,skolem0007(X9))&g(skolem0007(X9)))))|(![X12]:((![X13]:(~h(X12,X13)|~f(X13)))|((![X14]:h(X12,X14))&(![X15]:g(X15))))))),inference(skolemize,[status(esa)],[c3])).])).
% 0.46/0.68 fof(c6,negated_conjecture,(![X4]:(![X9]:(![X10]:(![X12]:(![X13]:(![X14]:(![X15]:((((((h(skolem0001,skolem0002)|h(skolem0003,skolem0004))&(h(skolem0001,skolem0002)|f(skolem0004)))&(h(skolem0001,skolem0002)|(~h(skolem0003,skolem0005)|~g(skolem0006))))&(((f(skolem0002)|h(skolem0003,skolem0004))&(f(skolem0002)|f(skolem0004)))&(f(skolem0002)|(~h(skolem0003,skolem0005)|~g(skolem0006)))))&((((~h(skolem0001,X4)|~g(X4))|h(skolem0003,skolem0004))&((~h(skolem0001,X4)|~g(X4))|f(skolem0004)))&((~h(skolem0001,X4)|~g(X4))|(~h(skolem0003,skolem0005)|~g(skolem0006)))))&(((((~h(X9,X10)|~f(X10))|h(X9,skolem0007(X9)))|((~h(X12,X13)|~f(X13))|h(X12,X14)))&(((~h(X9,X10)|~f(X10))|h(X9,skolem0007(X9)))|((~h(X12,X13)|~f(X13))|g(X15))))&((((~h(X9,X10)|~f(X10))|g(skolem0007(X9)))|((~h(X12,X13)|~f(X13))|h(X12,X14)))&(((~h(X9,X10)|~f(X10))|g(skolem0007(X9)))|((~h(X12,X13)|~f(X13))|g(X15))))))))))))),inference(distribute,[status(thm)],[c5])).
% 0.46/0.68 cnf(c16,negated_conjecture,~h(X29,X31)|~f(X31)|h(X29,skolem0007(X29))|~h(X33,X30)|~f(X30)|h(X33,X32),inference(split_conjunct,[status(thm)],[c6])).
% 0.46/0.68 cnf(c11,negated_conjecture,f(skolem0002)|f(skolem0004),inference(split_conjunct,[status(thm)],[c6])).
% 0.46/0.68 cnf(c8,negated_conjecture,h(skolem0001,skolem0002)|f(skolem0004),inference(split_conjunct,[status(thm)],[c6])).
% 0.46/0.68 cnf(c19,negated_conjecture,~h(X19,X21)|~f(X21)|g(skolem0007(X19))|~h(X23,X20)|~f(X20)|g(X22),inference(split_conjunct,[status(thm)],[c6])).
% 0.46/0.68 cnf(c24,plain,~h(X26,X25)|~f(X25)|g(skolem0007(X26))|g(X24),inference(factor,[status(thm)],[c19])).
% 0.46/0.68 cnf(c30,plain,~f(skolem0002)|g(skolem0007(skolem0001))|g(X27)|f(skolem0004),inference(resolution,[status(thm)],[c24, c8])).
% 0.46/0.68 cnf(c34,plain,g(skolem0007(skolem0001))|g(X28)|f(skolem0004),inference(resolution,[status(thm)],[c30, c11])).
% 0.46/0.68 cnf(c35,plain,g(skolem0007(skolem0001))|f(skolem0004),inference(factor,[status(thm)],[c34])).
% 0.46/0.68 cnf(c14,negated_conjecture,~h(skolem0001,X16)|~g(X16)|f(skolem0004),inference(split_conjunct,[status(thm)],[c6])).
% 0.46/0.68 cnf(c20,plain,~g(skolem0002)|f(skolem0004),inference(resolution,[status(thm)],[c14, c8])).
% 0.46/0.68 cnf(c17,negated_conjecture,~h(X36,X38)|~f(X38)|h(X36,skolem0007(X36))|~h(X40,X37)|~f(X37)|g(X39),inference(split_conjunct,[status(thm)],[c6])).
% 0.46/0.68 cnf(c49,plain,~h(X43,X41)|~f(X41)|h(X43,skolem0007(X43))|g(X42),inference(factor,[status(thm)],[c17])).
% 0.46/0.68 cnf(c55,plain,~f(skolem0002)|h(skolem0001,skolem0007(skolem0001))|g(X72)|f(skolem0004),inference(resolution,[status(thm)],[c49, c8])).
% 0.46/0.68 cnf(c112,plain,h(skolem0001,skolem0007(skolem0001))|g(X73)|f(skolem0004),inference(resolution,[status(thm)],[c55, c11])).
% 0.46/0.68 cnf(c122,plain,h(skolem0001,skolem0007(skolem0001))|f(skolem0004),inference(resolution,[status(thm)],[c112, c20])).
% 0.46/0.68 cnf(c126,plain,f(skolem0004)|~g(skolem0007(skolem0001)),inference(resolution,[status(thm)],[c122, c14])).
% 0.46/0.68 cnf(c133,plain,f(skolem0004),inference(resolution,[status(thm)],[c126, c35])).
% 0.46/0.68 cnf(c38,plain,~h(X44,X46)|~f(X46)|h(X44,skolem0007(X44))|h(X44,X45),inference(factor,[status(thm)],[c16])).
% 0.46/0.68 cnf(c10,negated_conjecture,f(skolem0002)|h(skolem0003,skolem0004),inference(split_conjunct,[status(thm)],[c6])).
% 0.46/0.68 cnf(c7,negated_conjecture,h(skolem0001,skolem0002)|h(skolem0003,skolem0004),inference(split_conjunct,[status(thm)],[c6])).
% 0.46/0.68 cnf(c32,plain,~f(skolem0002)|g(skolem0007(skolem0001))|g(X61)|h(skolem0003,skolem0004),inference(resolution,[status(thm)],[c24, c7])).
% 0.46/0.68 cnf(c95,plain,g(skolem0007(skolem0001))|g(X65)|h(skolem0003,skolem0004),inference(resolution,[status(thm)],[c32, c10])).
% 0.46/0.68 cnf(c96,plain,g(skolem0007(skolem0001))|h(skolem0003,skolem0004),inference(factor,[status(thm)],[c95])).
% 0.46/0.68 cnf(c13,negated_conjecture,~h(skolem0001,X17)|~g(X17)|h(skolem0003,skolem0004),inference(split_conjunct,[status(thm)],[c6])).
% 0.46/0.68 cnf(c23,plain,~g(skolem0002)|h(skolem0003,skolem0004),inference(resolution,[status(thm)],[c13, c7])).
% 0.46/0.68 cnf(c57,plain,~f(skolem0002)|h(skolem0001,skolem0007(skolem0001))|g(X107)|h(skolem0003,skolem0004),inference(resolution,[status(thm)],[c49, c7])).
% 0.46/0.68 cnf(c188,plain,h(skolem0001,skolem0007(skolem0001))|g(X108)|h(skolem0003,skolem0004),inference(resolution,[status(thm)],[c57, c10])).
% 0.46/0.68 cnf(c200,plain,h(skolem0001,skolem0007(skolem0001))|h(skolem0003,skolem0004),inference(resolution,[status(thm)],[c188, c23])).
% 0.46/0.68 cnf(c216,plain,h(skolem0003,skolem0004)|~g(skolem0007(skolem0001)),inference(resolution,[status(thm)],[c200, c13])).
% 0.46/0.68 cnf(c231,plain,h(skolem0003,skolem0004),inference(resolution,[status(thm)],[c216, c96])).
% 0.46/0.68 cnf(c237,plain,~f(skolem0004)|h(skolem0003,skolem0007(skolem0003))|h(skolem0003,X121),inference(resolution,[status(thm)],[c231, c38])).
% 0.46/0.68 cnf(c252,plain,h(skolem0003,skolem0007(skolem0003))|h(skolem0003,X122),inference(resolution,[status(thm)],[c237, c133])).
% 0.46/0.68 cnf(c253,plain,h(skolem0003,skolem0007(skolem0003)),inference(factor,[status(thm)],[c252])).
% 0.46/0.68 cnf(c274,plain,~h(X272,X273)|~f(X273)|h(X272,skolem0007(X272))|~f(skolem0007(skolem0003))|h(skolem0003,X271),inference(resolution,[status(thm)],[c253, c16])).
% 0.46/0.68 cnf(c289,plain,~h(X275,skolem0007(skolem0003))|~f(skolem0007(skolem0003))|h(X275,skolem0007(X275))|h(skolem0003,X274),inference(factor,[status(thm)],[c274])).
% 0.46/0.68 cnf(c18,negated_conjecture,~h(X47,X49)|~f(X49)|g(skolem0007(X47))|~h(X51,X48)|~f(X48)|h(X51,X50),inference(split_conjunct,[status(thm)],[c6])).
% 0.46/0.68 cnf(c273,plain,~h(X229,X228)|~f(X228)|g(skolem0007(X229))|~f(skolem0007(skolem0003))|h(skolem0003,X230),inference(resolution,[status(thm)],[c253, c18])).
% 0.46/0.68 cnf(c287,plain,~h(X233,skolem0007(skolem0003))|~f(skolem0007(skolem0003))|g(skolem0007(X233))|h(skolem0003,X232),inference(factor,[status(thm)],[c273])).
% 0.46/0.68 cnf(c234,plain,~h(X194,X195)|~f(X195)|h(X194,skolem0007(X194))|~f(skolem0004)|h(skolem0003,X193),inference(resolution,[status(thm)],[c231, c16])).
% 0.46/0.68 cnf(c233,plain,~h(X173,X172)|~f(X172)|g(skolem0007(X173))|~f(skolem0004)|h(skolem0003,X174),inference(resolution,[status(thm)],[c231, c18])).
% 0.46/0.68 cnf(c239,plain,~f(skolem0004)|g(skolem0007(skolem0003))|g(X112),inference(resolution,[status(thm)],[c231, c24])).
% 0.46/0.68 cnf(c241,plain,g(skolem0007(skolem0003))|g(X113),inference(resolution,[status(thm)],[c239, c133])).
% 0.46/0.68 cnf(c242,plain,g(skolem0007(skolem0003)),inference(factor,[status(thm)],[c241])).
% 0.46/0.68 cnf(c62,plain,~h(X53,X54)|~f(X54)|g(skolem0007(X53))|h(X53,X52),inference(factor,[status(thm)],[c18])).
% 0.46/0.68 cnf(c15,negated_conjecture,~h(skolem0001,X18)|~g(X18)|~h(skolem0003,skolem0005)|~g(skolem0006),inference(split_conjunct,[status(thm)],[c6])).
% 0.46/0.68 cnf(c12,negated_conjecture,f(skolem0002)|~h(skolem0003,skolem0005)|~g(skolem0006),inference(split_conjunct,[status(thm)],[c6])).
% 0.46/0.68 cnf(c9,negated_conjecture,h(skolem0001,skolem0002)|~h(skolem0003,skolem0005)|~g(skolem0006),inference(split_conjunct,[status(thm)],[c6])).
% 0.46/0.68 % SZS output end Saturation
% 0.46/0.68
% 0.46/0.68 % Initial clauses : 13
% 0.46/0.68 % Processed clauses : 66
% 0.46/0.68 % Factors computed : 14
% 0.46/0.68 % Resolvents computed: 257
% 0.46/0.68 % Tautologies deleted: 5
% 0.46/0.68 % Forward subsumed : 213
% 0.46/0.68 % Backward subsumed : 47
% 0.46/0.68 % -------- CPU Time ---------
% 0.46/0.68 % User time : 0.302 s
% 0.46/0.68 % System time : 0.017 s
% 0.46/0.68 % Total time : 0.319 s
%------------------------------------------------------------------------------