%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : MSC017+1 : TPTP v8.1.2. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n017.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:26 EDT 2024
% Result : Theorem 0.96s 1.16s
% Output : Refutation 0.96s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : MSC017+1 : TPTP v8.1.2. Released v4.0.0.
% 0.03/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.12/0.33 % Computer : n017.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Wed May 8 13:56:52 EDT 2024
% 0.12/0.34 % CPUTime :
% 0.96/1.16 % Version: 1.5
% 0.96/1.16 % SZS status Theorem
% 0.96/1.16 % SZS output start CNFRefutation
% 0.96/1.16 fof(no_bad,conjecture,(![D]:(dive(D)=>(![O]:(outcome(D,O)=>(~bad(O)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', no_bad)).
% 0.96/1.16 fof(c8,negated_conjecture,(~(![D]:(dive(D)=>(![O]:(outcome(D,O)=>(~bad(O))))))),inference(assume_negation,[status(cth)],[no_bad])).
% 0.96/1.16 fof(c9,negated_conjecture,(~(![D]:(dive(D)=>(![O]:(outcome(D,O)=>~bad(O)))))),inference(fof_simplification,[status(thm)],[c8])).
% 0.96/1.16 fof(c10,negated_conjecture,(?[D]:(dive(D)&(?[O]:(outcome(D,O)&bad(O))))),inference(fof_nnf,[status(thm)],[c9])).
% 0.96/1.16 fof(c11,negated_conjecture,(?[X2]:(dive(X2)&(?[X3]:(outcome(X2,X3)&bad(X3))))),inference(variable_rename,[status(thm)],[c10])).
% 0.96/1.16 fof(c12,negated_conjecture,(dive(skolem0001)&(outcome(skolem0001,skolem0002)&bad(skolem0002))),inference(skolemize,[status(esa)],[c11])).
% 0.96/1.16 cnf(c13,negated_conjecture,dive(skolem0001),inference(split_conjunct,[status(thm)],[c12])).
% 0.96/1.16 fof(no_deep_long,axiom,(![D]:(dive(D)=>((~greater(depth(D),depth_limit))&(~greater(time(D),time_limit))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', no_deep_long)).
% 0.96/1.16 fof(c16,plain,(![D]:(dive(D)=>(~greater(depth(D),depth_limit)&~greater(time(D),time_limit)))),inference(fof_simplification,[status(thm)],[no_deep_long])).
% 0.96/1.16 fof(c17,plain,(![D]:(~dive(D)|(~greater(depth(D),depth_limit)&~greater(time(D),time_limit)))),inference(fof_nnf,[status(thm)],[c16])).
% 0.96/1.16 fof(c18,plain,(![X4]:(~dive(X4)|(~greater(depth(X4),depth_limit)&~greater(time(X4),time_limit)))),inference(variable_rename,[status(thm)],[c17])).
% 0.96/1.16 fof(c19,plain,(![X4]:((~dive(X4)|~greater(depth(X4),depth_limit))&(~dive(X4)|~greater(time(X4),time_limit)))),inference(distribute,[status(thm)],[c18])).
% 0.96/1.16 cnf(c21,plain,~dive(X27)|~greater(time(X27),time_limit),inference(split_conjunct,[status(thm)],[c19])).
% 0.96/1.16 cnf(c20,plain,~dive(X26)|~greater(depth(X26),depth_limit),inference(split_conjunct,[status(thm)],[c19])).
% 0.96/1.16 fof(depth_and_time_and_nitrogen,axiom,(![D]:(dive(D)=>((greater(depth(D),depth_limit)|greater(time(D),time_limit))<=>greater(nitrogen(D),nitrogen_limit)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', depth_and_time_and_nitrogen)).
% 0.96/1.16 fof(c32,plain,(![D]:(~dive(D)|(((~greater(depth(D),depth_limit)&~greater(time(D),time_limit))|greater(nitrogen(D),nitrogen_limit))&(~greater(nitrogen(D),nitrogen_limit)|(greater(depth(D),depth_limit)|greater(time(D),time_limit)))))),inference(fof_nnf,[status(thm)],[depth_and_time_and_nitrogen])).
% 0.96/1.16 fof(c33,plain,(![X8]:(~dive(X8)|(((~greater(depth(X8),depth_limit)&~greater(time(X8),time_limit))|greater(nitrogen(X8),nitrogen_limit))&(~greater(nitrogen(X8),nitrogen_limit)|(greater(depth(X8),depth_limit)|greater(time(X8),time_limit)))))),inference(variable_rename,[status(thm)],[c32])).
% 0.96/1.16 fof(c34,plain,(![X8]:(((~dive(X8)|(~greater(depth(X8),depth_limit)|greater(nitrogen(X8),nitrogen_limit)))&(~dive(X8)|(~greater(time(X8),time_limit)|greater(nitrogen(X8),nitrogen_limit))))&(~dive(X8)|(~greater(nitrogen(X8),nitrogen_limit)|(greater(depth(X8),depth_limit)|greater(time(X8),time_limit)))))),inference(distribute,[status(thm)],[c33])).
% 0.96/1.16 cnf(c37,plain,~dive(X65)|~greater(nitrogen(X65),nitrogen_limit)|greater(depth(X65),depth_limit)|greater(time(X65),time_limit),inference(split_conjunct,[status(thm)],[c34])).
% 0.96/1.16 fof(too_much_nitrogen,axiom,(![D]:(dive(D)=>(greater(nitrogen(D),nitrogen_limit)<=>outcome(D,dci)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', too_much_nitrogen)).
% 0.96/1.16 fof(c27,plain,(![D]:(~dive(D)|((~greater(nitrogen(D),nitrogen_limit)|outcome(D,dci))&(~outcome(D,dci)|greater(nitrogen(D),nitrogen_limit))))),inference(fof_nnf,[status(thm)],[too_much_nitrogen])).
% 0.96/1.16 fof(c28,plain,(![X7]:(~dive(X7)|((~greater(nitrogen(X7),nitrogen_limit)|outcome(X7,dci))&(~outcome(X7,dci)|greater(nitrogen(X7),nitrogen_limit))))),inference(variable_rename,[status(thm)],[c27])).
% 0.96/1.16 fof(c29,plain,(![X7]:((~dive(X7)|(~greater(nitrogen(X7),nitrogen_limit)|outcome(X7,dci)))&(~dive(X7)|(~outcome(X7,dci)|greater(nitrogen(X7),nitrogen_limit))))),inference(distribute,[status(thm)],[c28])).
% 0.96/1.16 cnf(c31,plain,~dive(X60)|~outcome(X60,dci)|greater(nitrogen(X60),nitrogen_limit),inference(split_conjunct,[status(thm)],[c29])).
% 0.96/1.16 cnf(reflexivity,axiom,X10=X10,theory(equality)).
% 0.96/1.16 cnf(c15,negated_conjecture,bad(skolem0002),inference(split_conjunct,[status(thm)],[c12])).
% 0.96/1.16 cnf(c14,negated_conjecture,outcome(skolem0001,skolem0002),inference(split_conjunct,[status(thm)],[c12])).
% 0.96/1.16 fof(dci_is_the_only_bad_outcome,axiom,(![D]:(dive(D)=>(![O]:((outcome(D,O)&bad(O))=>O=dci)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', dci_is_the_only_bad_outcome)).
% 0.96/1.16 fof(c22,plain,(![D]:(~dive(D)|(![O]:((~outcome(D,O)|~bad(O))|O=dci)))),inference(fof_nnf,[status(thm)],[dci_is_the_only_bad_outcome])).
% 0.96/1.16 fof(c24,plain,(![X5]:(![X6]:(~dive(X5)|((~outcome(X5,X6)|~bad(X6))|X6=dci)))),inference(shift_quantors,[status(thm)],[fof(c23,plain,(![X5]:(~dive(X5)|(![X6]:((~outcome(X5,X6)|~bad(X6))|X6=dci)))),inference(variable_rename,[status(thm)],[c22])).])).
% 0.96/1.16 cnf(c25,plain,~dive(X53)|~outcome(X53,X54)|~bad(X54)|X54=dci,inference(split_conjunct,[status(thm)],[c24])).
% 0.96/1.16 cnf(c53,plain,~dive(skolem0001)|~bad(skolem0002)|skolem0002=dci,inference(resolution,[status(thm)],[c25, c14])).
% 0.96/1.16 cnf(c55,plain,~dive(skolem0001)|skolem0002=dci,inference(resolution,[status(thm)],[c53, c15])).
% 0.96/1.16 cnf(c56,plain,skolem0002=dci,inference(resolution,[status(thm)],[c55, c13])).
% 0.96/1.16 cnf(c6,axiom,X57!=X58|X55!=X56|~outcome(X57,X55)|outcome(X58,X56),theory(equality)).
% 0.96/1.16 cnf(c54,plain,skolem0001!=X69|skolem0002!=X70|outcome(X69,X70),inference(resolution,[status(thm)],[c6, c14])).
% 0.96/1.16 cnf(c163,plain,skolem0001!=X72|outcome(X72,dci),inference(resolution,[status(thm)],[c54, c56])).
% 0.96/1.16 cnf(c165,plain,outcome(skolem0001,dci),inference(resolution,[status(thm)],[c163, reflexivity])).
% 0.96/1.16 cnf(c166,plain,~dive(skolem0001)|greater(nitrogen(skolem0001),nitrogen_limit),inference(resolution,[status(thm)],[c165, c31])).
% 0.96/1.16 cnf(c191,plain,greater(nitrogen(skolem0001),nitrogen_limit),inference(resolution,[status(thm)],[c166, c13])).
% 0.96/1.16 cnf(c192,plain,~dive(skolem0001)|greater(depth(skolem0001),depth_limit)|greater(time(skolem0001),time_limit),inference(resolution,[status(thm)],[c191, c37])).
% 0.96/1.16 cnf(c1932,plain,greater(depth(skolem0001),depth_limit)|greater(time(skolem0001),time_limit),inference(resolution,[status(thm)],[c192, c13])).
% 0.96/1.16 cnf(c1934,plain,greater(time(skolem0001),time_limit)|~dive(skolem0001),inference(resolution,[status(thm)],[c1932, c20])).
% 0.96/1.16 cnf(c1959,plain,greater(time(skolem0001),time_limit),inference(resolution,[status(thm)],[c1934, c13])).
% 0.96/1.16 cnf(c1961,plain,~dive(skolem0001),inference(resolution,[status(thm)],[c1959, c21])).
% 0.96/1.16 cnf(c1962,plain,$false,inference(resolution,[status(thm)],[c1961, c13])).
% 0.96/1.16 % SZS output end CNFRefutation
% 0.96/1.16
% 0.96/1.16 % Initial clauses : 24
% 0.96/1.16 % Processed clauses : 215
% 0.96/1.16 % Factors computed : 2
% 0.96/1.16 % Resolvents computed: 1920
% 0.96/1.16 % Tautologies deleted: 4
% 0.96/1.16 % Forward subsumed : 120
% 0.96/1.16 % Backward subsumed : 6
% 0.96/1.16 % -------- CPU Time ---------
% 0.96/1.16 % User time : 0.782 s
% 0.96/1.16 % System time : 0.014 s
% 0.96/1.16 % Total time : 0.796 s
%------------------------------------------------------------------------------