%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : NUN089+1 : TPTP v8.1.2. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n027.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:37:12 EDT 2024
% Result : Theorem 0.47s 0.68s
% Output : Refutation 0.47s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.10/0.12 % Problem : NUN089+1 : TPTP v8.1.2. Released v7.3.0.
% 0.10/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.34 % Computer : n027.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 22:30:23 EDT 2024
% 0.13/0.34 % CPUTime :
% 0.47/0.68 % Version: 1.5
% 0.47/0.68 % SZS status Theorem
% 0.47/0.68 % SZS output start CNFRefutation
% 0.47/0.68 fof(zerounidtwo,conjecture,(![Y1]:((![Y2]:((![Y3]:((~r1(Y3))|(~r2(Y3,Y2))))|(~r2(Y2,Y1))))|(![Y4]:((~id(Y4,Y1))|(~r1(Y4)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', zerounidtwo)).
% 0.47/0.68 fof(c0,negated_conjecture,(~(![Y1]:((![Y2]:((![Y3]:((~r1(Y3))|(~r2(Y3,Y2))))|(~r2(Y2,Y1))))|(![Y4]:((~id(Y4,Y1))|(~r1(Y4))))))),inference(assume_negation,[status(cth)],[zerounidtwo])).
% 0.47/0.68 fof(c1,negated_conjecture,(~(![Y1]:((![Y2]:((![Y3]:(~r1(Y3)|~r2(Y3,Y2)))|~r2(Y2,Y1)))|(![Y4]:(~id(Y4,Y1)|~r1(Y4)))))),inference(fof_simplification,[status(thm)],[c0])).
% 0.47/0.68 fof(c2,negated_conjecture,(?[Y1]:((?[Y2]:((?[Y3]:(r1(Y3)&r2(Y3,Y2)))&r2(Y2,Y1)))&(?[Y4]:(id(Y4,Y1)&r1(Y4))))),inference(fof_nnf,[status(thm)],[c1])).
% 0.47/0.68 fof(c3,negated_conjecture,(?[X2]:((?[X3]:((?[X4]:(r1(X4)&r2(X4,X3)))&r2(X3,X2)))&(?[X5]:(id(X5,X2)&r1(X5))))),inference(variable_rename,[status(thm)],[c2])).
% 0.47/0.68 fof(c4,negated_conjecture,(((r1(skolem0003)&r2(skolem0003,skolem0002))&r2(skolem0002,skolem0001))&(id(skolem0004,skolem0001)&r1(skolem0004))),inference(skolemize,[status(esa)],[c3])).
% 0.47/0.68 cnf(c9,negated_conjecture,r1(skolem0004),inference(split_conjunct,[status(thm)],[c4])).
% 0.47/0.68 cnf(c8,negated_conjecture,id(skolem0004,skolem0001),inference(split_conjunct,[status(thm)],[c4])).
% 0.47/0.68 cnf(c7,negated_conjecture,r2(skolem0002,skolem0001),inference(split_conjunct,[status(thm)],[c4])).
% 0.47/0.68 fof(axiom_7a,axiom,(![X7]:(![Y10]:((![Y20]:((~id(Y20,Y10))|(~r1(Y20))))|(~r2(X7,Y10))))),file('/export/starexec/sandbox/benchmark/Axioms/NUM009+0.ax', axiom_7a)).
% 0.47/0.68 fof(c10,plain,(![X7]:(![Y10]:((![Y20]:(~id(Y20,Y10)|~r1(Y20)))|~r2(X7,Y10)))),inference(fof_simplification,[status(thm)],[axiom_7a])).
% 0.47/0.68 fof(c12,plain,(![X6]:(![X7]:(![X8]:((~id(X8,X7)|~r1(X8))|~r2(X6,X7))))),inference(shift_quantors,[status(thm)],[fof(c11,plain,(![X6]:(![X7]:((![X8]:(~id(X8,X7)|~r1(X8)))|~r2(X6,X7)))),inference(variable_rename,[status(thm)],[c10])).])).
% 0.47/0.68 cnf(c13,plain,~id(X81,X79)|~r1(X81)|~r2(X80,X79),inference(split_conjunct,[status(thm)],[c12])).
% 0.47/0.68 cnf(c118,plain,~id(X122,skolem0001)|~r1(X122),inference(resolution,[status(thm)],[c13, c7])).
% 0.47/0.68 cnf(c169,plain,~r1(skolem0004),inference(resolution,[status(thm)],[c118, c8])).
% 0.47/0.68 cnf(c170,plain,$false,inference(resolution,[status(thm)],[c169, c9])).
% 0.47/0.68 % SZS output end CNFRefutation
% 0.47/0.68
% 0.47/0.68 % Initial clauses : 63
% 0.47/0.68 % Processed clauses : 44
% 0.47/0.68 % Factors computed : 1
% 0.47/0.68 % Resolvents computed: 53
% 0.47/0.68 % Tautologies deleted: 2
% 0.47/0.68 % Forward subsumed : 14
% 0.47/0.68 % Backward subsumed : 0
% 0.47/0.68 % -------- CPU Time ---------
% 0.47/0.68 % User time : 0.310 s
% 0.47/0.68 % System time : 0.019 s
% 0.47/0.68 % Total time : 0.329 s
%------------------------------------------------------------------------------