%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : MSC009+1 : TPTP v8.1.2. Released v2.0.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n021.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:33:23 EDT 2024
% Result : Satisfiable 0.23s 0.56s
% Output : Saturation 0.23s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.09/0.14 % Problem : MSC009+1 : TPTP v8.1.2. Released v2.0.0.
% 0.09/0.15 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.16/0.37 % Computer : n021.cluster.edu
% 0.16/0.37 % Model : x86_64 x86_64
% 0.16/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.37 % Memory : 8042.1875MB
% 0.16/0.37 % OS : Linux 3.10.0-693.el7.x86_64
% 0.16/0.37 % CPULimit : 300
% 0.16/0.37 % WCLimit : 300
% 0.16/0.37 % DateTime : Wed May 8 13:55:23 EDT 2024
% 0.16/0.37 % CPUTime :
% 0.23/0.56 % Version: 1.5
% 0.23/0.56 % SZS status Satisfiable
% 0.23/0.56 % SZS output start Saturation
% 0.23/0.56 fof(parent,axiom,(![X]:(parent(X)<=>(person(X)&(?[Y]:(child(X,Y)&person(Y)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', parent)).
% 0.23/0.56 fof(c40,plain,(![X]:((~parent(X)|(person(X)&(?[Y]:(child(X,Y)&person(Y)))))&((~person(X)|(![Y]:(~child(X,Y)|~person(Y))))|parent(X)))),inference(fof_nnf,[status(thm)],[parent])).
% 0.23/0.56 fof(c41,plain,((![X]:(~parent(X)|(person(X)&(?[Y]:(child(X,Y)&person(Y))))))&(![X]:((~person(X)|(![Y]:(~child(X,Y)|~person(Y))))|parent(X)))),inference(shift_quantors,[status(thm)],[c40])).
% 0.23/0.56 fof(c42,plain,((![X18]:(~parent(X18)|(person(X18)&(?[X19]:(child(X18,X19)&person(X19))))))&(![X20]:((~person(X20)|(![X21]:(~child(X20,X21)|~person(X21))))|parent(X20)))),inference(variable_rename,[status(thm)],[c41])).
% 0.23/0.56 fof(c44,plain,(![X18]:(![X20]:(![X21]:((~parent(X18)|(person(X18)&(child(X18,skolem0005(X18))&person(skolem0005(X18)))))&((~person(X20)|(~child(X20,X21)|~person(X21)))|parent(X20)))))),inference(shift_quantors,[status(thm)],[fof(c43,plain,((![X18]:(~parent(X18)|(person(X18)&(child(X18,skolem0005(X18))&person(skolem0005(X18))))))&(![X20]:((~person(X20)|(![X21]:(~child(X20,X21)|~person(X21))))|parent(X20)))),inference(skolemize,[status(esa)],[c42])).])).
% 0.23/0.56 fof(c45,plain,(![X18]:(![X20]:(![X21]:(((~parent(X18)|person(X18))&((~parent(X18)|child(X18,skolem0005(X18)))&(~parent(X18)|person(skolem0005(X18)))))&((~person(X20)|(~child(X20,X21)|~person(X21)))|parent(X20)))))),inference(distribute,[status(thm)],[c44])).
% 0.23/0.56 cnf(c49,plain,~person(X61)|~child(X61,X60)|~person(X60)|parent(X61),inference(split_conjunct,[status(thm)],[c45])).
% 0.23/0.56 fof(mother,axiom,(![X]:(mother(X)<=>(parent(X)&(?[Y]:(sex(X,Y)&female(Y)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', mother)).
% 0.23/0.56 fof(c30,plain,(![X]:((~mother(X)|(parent(X)&(?[Y]:(sex(X,Y)&female(Y)))))&((~parent(X)|(![Y]:(~sex(X,Y)|~female(Y))))|mother(X)))),inference(fof_nnf,[status(thm)],[mother])).
% 0.23/0.56 fof(c31,plain,((![X]:(~mother(X)|(parent(X)&(?[Y]:(sex(X,Y)&female(Y))))))&(![X]:((~parent(X)|(![Y]:(~sex(X,Y)|~female(Y))))|mother(X)))),inference(shift_quantors,[status(thm)],[c30])).
% 0.23/0.56 fof(c32,plain,((![X14]:(~mother(X14)|(parent(X14)&(?[X15]:(sex(X14,X15)&female(X15))))))&(![X16]:((~parent(X16)|(![X17]:(~sex(X16,X17)|~female(X17))))|mother(X16)))),inference(variable_rename,[status(thm)],[c31])).
% 0.23/0.56 fof(c34,plain,(![X14]:(![X16]:(![X17]:((~mother(X14)|(parent(X14)&(sex(X14,skolem0004(X14))&female(skolem0004(X14)))))&((~parent(X16)|(~sex(X16,X17)|~female(X17)))|mother(X16)))))),inference(shift_quantors,[status(thm)],[fof(c33,plain,((![X14]:(~mother(X14)|(parent(X14)&(sex(X14,skolem0004(X14))&female(skolem0004(X14))))))&(![X16]:((~parent(X16)|(![X17]:(~sex(X16,X17)|~female(X17))))|mother(X16)))),inference(skolemize,[status(esa)],[c32])).])).
% 0.23/0.56 fof(c35,plain,(![X14]:(![X16]:(![X17]:(((~mother(X14)|parent(X14))&((~mother(X14)|sex(X14,skolem0004(X14)))&(~mother(X14)|female(skolem0004(X14)))))&((~parent(X16)|(~sex(X16,X17)|~female(X17)))|mother(X16)))))),inference(distribute,[status(thm)],[c34])).
% 0.23/0.56 cnf(c39,plain,~parent(X58)|~sex(X58,X59)|~female(X59)|mother(X58),inference(split_conjunct,[status(thm)],[c35])).
% 0.23/0.56 fof(parent_with_sons_only,axiom,(![X]:(parent_with_sons_only(X)<=>(parent(X)&(![Y]:(child(X,Y)=>(?[Z]:(sex(Y,Z)&male(Z)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', parent_with_sons_only)).
% 0.23/0.56 fof(c0,plain,(![X]:((~parent_with_sons_only(X)|(parent(X)&(![Y]:(~child(X,Y)|(?[Z]:(sex(Y,Z)&male(Z)))))))&((~parent(X)|(?[Y]:(child(X,Y)&(![Z]:(~sex(Y,Z)|~male(Z))))))|parent_with_sons_only(X)))),inference(fof_nnf,[status(thm)],[parent_with_sons_only])).
% 0.23/0.56 fof(c1,plain,((![X]:(~parent_with_sons_only(X)|(parent(X)&(![Y]:(~child(X,Y)|(?[Z]:(sex(Y,Z)&male(Z))))))))&(![X]:((~parent(X)|(?[Y]:(child(X,Y)&(![Z]:(~sex(Y,Z)|~male(Z))))))|parent_with_sons_only(X)))),inference(shift_quantors,[status(thm)],[c0])).
% 0.23/0.56 fof(c2,plain,((![X2]:(~parent_with_sons_only(X2)|(parent(X2)&(![X3]:(~child(X2,X3)|(?[X4]:(sex(X3,X4)&male(X4))))))))&(![X5]:((~parent(X5)|(?[X6]:(child(X5,X6)&(![X7]:(~sex(X6,X7)|~male(X7))))))|parent_with_sons_only(X5)))),inference(variable_rename,[status(thm)],[c1])).
% 0.23/0.56 fof(c4,plain,(![X2]:(![X3]:(![X5]:(![X7]:((~parent_with_sons_only(X2)|(parent(X2)&(~child(X2,X3)|(sex(X3,skolem0001(X2,X3))&male(skolem0001(X2,X3))))))&((~parent(X5)|(child(X5,skolem0002(X5))&(~sex(skolem0002(X5),X7)|~male(X7))))|parent_with_sons_only(X5))))))),inference(shift_quantors,[status(thm)],[fof(c3,plain,((![X2]:(~parent_with_sons_only(X2)|(parent(X2)&(![X3]:(~child(X2,X3)|(sex(X3,skolem0001(X2,X3))&male(skolem0001(X2,X3))))))))&(![X5]:((~parent(X5)|(child(X5,skolem0002(X5))&(![X7]:(~sex(skolem0002(X5),X7)|~male(X7)))))|parent_with_sons_only(X5)))),inference(skolemize,[status(esa)],[c2])).])).
% 0.23/0.56 fof(c5,plain,(![X2]:(![X3]:(![X5]:(![X7]:(((~parent_with_sons_only(X2)|parent(X2))&((~parent_with_sons_only(X2)|(~child(X2,X3)|sex(X3,skolem0001(X2,X3))))&(~parent_with_sons_only(X2)|(~child(X2,X3)|male(skolem0001(X2,X3))))))&(((~parent(X5)|child(X5,skolem0002(X5)))|parent_with_sons_only(X5))&((~parent(X5)|(~sex(skolem0002(X5),X7)|~male(X7)))|parent_with_sons_only(X5)))))))),inference(distribute,[status(thm)],[c4])).
% 0.23/0.56 cnf(c10,plain,~parent(X56)|~sex(skolem0002(X56),X57)|~male(X57)|parent_with_sons_only(X56),inference(split_conjunct,[status(thm)],[c5])).
% 0.23/0.56 fof(grandparent,axiom,(![X]:(grandparent(X)<=>(parent(X)&(?[Y]:(child(X,Y)&parent(Y)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', grandparent)).
% 0.23/0.56 fof(c11,plain,(![X]:((~grandparent(X)|(parent(X)&(?[Y]:(child(X,Y)&parent(Y)))))&((~parent(X)|(![Y]:(~child(X,Y)|~parent(Y))))|grandparent(X)))),inference(fof_nnf,[status(thm)],[grandparent])).
% 0.23/0.56 fof(c12,plain,((![X]:(~grandparent(X)|(parent(X)&(?[Y]:(child(X,Y)&parent(Y))))))&(![X]:((~parent(X)|(![Y]:(~child(X,Y)|~parent(Y))))|grandparent(X)))),inference(shift_quantors,[status(thm)],[c11])).
% 0.23/0.56 fof(c13,plain,((![X8]:(~grandparent(X8)|(parent(X8)&(?[X9]:(child(X8,X9)&parent(X9))))))&(![X10]:((~parent(X10)|(![X11]:(~child(X10,X11)|~parent(X11))))|grandparent(X10)))),inference(variable_rename,[status(thm)],[c12])).
% 0.23/0.56 fof(c15,plain,(![X8]:(![X10]:(![X11]:((~grandparent(X8)|(parent(X8)&(child(X8,skolem0003(X8))&parent(skolem0003(X8)))))&((~parent(X10)|(~child(X10,X11)|~parent(X11)))|grandparent(X10)))))),inference(shift_quantors,[status(thm)],[fof(c14,plain,((![X8]:(~grandparent(X8)|(parent(X8)&(child(X8,skolem0003(X8))&parent(skolem0003(X8))))))&(![X10]:((~parent(X10)|(![X11]:(~child(X10,X11)|~parent(X11))))|grandparent(X10)))),inference(skolemize,[status(esa)],[c13])).])).
% 0.23/0.56 fof(c16,plain,(![X8]:(![X10]:(![X11]:(((~grandparent(X8)|parent(X8))&((~grandparent(X8)|child(X8,skolem0003(X8)))&(~grandparent(X8)|parent(skolem0003(X8)))))&((~parent(X10)|(~child(X10,X11)|~parent(X11)))|grandparent(X10)))))),inference(distribute,[status(thm)],[c15])).
% 0.23/0.56 cnf(c20,plain,~parent(X55)|~child(X55,X54)|~parent(X54)|grandparent(X55),inference(split_conjunct,[status(thm)],[c16])).
% 0.23/0.56 fof(person,axiom,(![X]:(person(X)<=>(?[Y]:(sex(X,Y)&(male(Y)|female(Y)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', person)).
% 0.23/0.56 fof(c50,plain,(![X]:((~person(X)|(?[Y]:(sex(X,Y)&(male(Y)|female(Y)))))&((![Y]:(~sex(X,Y)|(~male(Y)&~female(Y))))|person(X)))),inference(fof_nnf,[status(thm)],[person])).
% 0.23/0.56 fof(c51,plain,((![X]:(~person(X)|(?[Y]:(sex(X,Y)&(male(Y)|female(Y))))))&(![X]:((![Y]:(~sex(X,Y)|(~male(Y)&~female(Y))))|person(X)))),inference(shift_quantors,[status(thm)],[c50])).
% 0.23/0.56 fof(c52,plain,((![X22]:(~person(X22)|(?[X23]:(sex(X22,X23)&(male(X23)|female(X23))))))&(![X24]:((![X25]:(~sex(X24,X25)|(~male(X25)&~female(X25))))|person(X24)))),inference(variable_rename,[status(thm)],[c51])).
% 0.23/0.56 fof(c54,plain,(![X22]:(![X24]:(![X25]:((~person(X22)|(sex(X22,skolem0006(X22))&(male(skolem0006(X22))|female(skolem0006(X22)))))&((~sex(X24,X25)|(~male(X25)&~female(X25)))|person(X24)))))),inference(shift_quantors,[status(thm)],[fof(c53,plain,((![X22]:(~person(X22)|(sex(X22,skolem0006(X22))&(male(skolem0006(X22))|female(skolem0006(X22))))))&(![X24]:((![X25]:(~sex(X24,X25)|(~male(X25)&~female(X25))))|person(X24)))),inference(skolemize,[status(esa)],[c52])).])).
% 0.23/0.56 fof(c55,plain,(![X22]:(![X24]:(![X25]:(((~person(X22)|sex(X22,skolem0006(X22)))&(~person(X22)|(male(skolem0006(X22))|female(skolem0006(X22)))))&(((~sex(X24,X25)|~male(X25))|person(X24))&((~sex(X24,X25)|~female(X25))|person(X24))))))),inference(distribute,[status(thm)],[c54])).
% 0.23/0.56 cnf(c59,plain,~sex(X52,X53)|~female(X53)|person(X52),inference(split_conjunct,[status(thm)],[c55])).
% 0.23/0.56 cnf(c58,plain,~sex(X50,X51)|~male(X51)|person(X50),inference(split_conjunct,[status(thm)],[c55])).
% 0.23/0.56 cnf(c56,plain,~person(X49)|sex(X49,skolem0006(X49)),inference(split_conjunct,[status(thm)],[c55])).
% 0.23/0.56 cnf(c47,plain,~parent(X48)|child(X48,skolem0005(X48)),inference(split_conjunct,[status(thm)],[c45])).
% 0.23/0.56 cnf(c9,plain,~parent(X47)|child(X47,skolem0002(X47))|parent_with_sons_only(X47),inference(split_conjunct,[status(thm)],[c5])).
% 0.23/0.56 cnf(c37,plain,~mother(X46)|sex(X46,skolem0004(X46)),inference(split_conjunct,[status(thm)],[c35])).
% 0.23/0.56 fof(father,axiom,(![X]:(father(X)<=>(parent(X)&(~mother(X))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', father)).
% 0.23/0.56 fof(c21,plain,(![X]:(father(X)<=>(parent(X)&~mother(X)))),inference(fof_simplification,[status(thm)],[father])).
% 0.23/0.56 fof(c22,plain,(![X]:((~father(X)|(parent(X)&~mother(X)))&((~parent(X)|mother(X))|father(X)))),inference(fof_nnf,[status(thm)],[c21])).
% 0.23/0.56 fof(c23,plain,((![X]:(~father(X)|(parent(X)&~mother(X))))&(![X]:((~parent(X)|mother(X))|father(X)))),inference(shift_quantors,[status(thm)],[c22])).
% 0.23/0.56 fof(c25,plain,(![X12]:(![X13]:((~father(X12)|(parent(X12)&~mother(X12)))&((~parent(X13)|mother(X13))|father(X13))))),inference(shift_quantors,[status(thm)],[fof(c24,plain,((![X12]:(~father(X12)|(parent(X12)&~mother(X12))))&(![X13]:((~parent(X13)|mother(X13))|father(X13)))),inference(variable_rename,[status(thm)],[c23])).])).
% 0.23/0.56 fof(c26,plain,(![X12]:(![X13]:(((~father(X12)|parent(X12))&(~father(X12)|~mother(X12)))&((~parent(X13)|mother(X13))|father(X13))))),inference(distribute,[status(thm)],[c25])).
% 0.23/0.56 cnf(c29,plain,~parent(X45)|mother(X45)|father(X45),inference(split_conjunct,[status(thm)],[c26])).
% 0.23/0.56 cnf(c18,plain,~grandparent(X44)|child(X44,skolem0003(X44)),inference(split_conjunct,[status(thm)],[c16])).
% 0.23/0.56 cnf(c48,plain,~parent(X43)|person(skolem0005(X43)),inference(split_conjunct,[status(thm)],[c45])).
% 0.23/0.56 cnf(c38,plain,~mother(X42)|female(skolem0004(X42)),inference(split_conjunct,[status(thm)],[c35])).
% 0.23/0.56 cnf(c8,plain,~parent_with_sons_only(X40)|~child(X40,X41)|male(skolem0001(X40,X41)),inference(split_conjunct,[status(thm)],[c5])).
% 0.23/0.56 cnf(c19,plain,~grandparent(X39)|parent(skolem0003(X39)),inference(split_conjunct,[status(thm)],[c16])).
% 0.23/0.56 fof(female,axiom,(![X]:(female(X)<=>(~male(X)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', female)).
% 0.23/0.56 fof(c60,plain,(![X]:(female(X)<=>~male(X))),inference(fof_simplification,[status(thm)],[female])).
% 0.23/0.56 fof(c61,plain,(![X]:((~female(X)|~male(X))&(male(X)|female(X)))),inference(fof_nnf,[status(thm)],[c60])).
% 0.23/0.56 fof(c62,plain,((![X]:(~female(X)|~male(X)))&(![X]:(male(X)|female(X)))),inference(shift_quantors,[status(thm)],[c61])).
% 0.23/0.56 fof(c64,plain,(![X26]:(![X27]:((~female(X26)|~male(X26))&(male(X27)|female(X27))))),inference(shift_quantors,[status(thm)],[fof(c63,plain,((![X26]:(~female(X26)|~male(X26)))&(![X27]:(male(X27)|female(X27)))),inference(variable_rename,[status(thm)],[c62])).])).
% 0.23/0.56 cnf(c66,plain,male(X37)|female(X37),inference(split_conjunct,[status(thm)],[c64])).
% 0.23/0.56 cnf(c65,plain,~female(X36)|~male(X36),inference(split_conjunct,[status(thm)],[c64])).
% 0.23/0.56 cnf(c46,plain,~parent(X35)|person(X35),inference(split_conjunct,[status(thm)],[c45])).
% 0.23/0.56 cnf(c7,plain,~parent_with_sons_only(X33)|~child(X33,X34)|sex(X34,skolem0001(X33,X34)),inference(split_conjunct,[status(thm)],[c5])).
% 0.23/0.56 cnf(c36,plain,~mother(X32)|parent(X32),inference(split_conjunct,[status(thm)],[c35])).
% 0.23/0.56 cnf(c28,plain,~father(X31)|~mother(X31),inference(split_conjunct,[status(thm)],[c26])).
% 0.23/0.56 cnf(c27,plain,~father(X30)|parent(X30),inference(split_conjunct,[status(thm)],[c26])).
% 0.23/0.56 cnf(c17,plain,~grandparent(X29)|parent(X29),inference(split_conjunct,[status(thm)],[c16])).
% 0.23/0.56 cnf(c6,plain,~parent_with_sons_only(X28)|parent(X28),inference(split_conjunct,[status(thm)],[c5])).
% 0.23/0.56 % SZS output end Saturation
% 0.23/0.56
% 0.23/0.56 % Initial clauses : 26
% 0.23/0.56 % Processed clauses : 25
% 0.23/0.56 % Factors computed : 0
% 0.23/0.56 % Resolvents computed: 1
% 0.23/0.56 % Tautologies deleted: 1
% 0.23/0.56 % Forward subsumed : 1
% 0.23/0.56 % Backward subsumed : 0
% 0.23/0.56 % -------- CPU Time ---------
% 0.23/0.56 % User time : 0.175 s
% 0.23/0.56 % System time : 0.015 s
% 0.23/0.56 % Total time : 0.190 s
%------------------------------------------------------------------------------