%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : KRS096+1 : TPTP v8.1.2. Released v3.1.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:28:41 EDT 2024
% Result : Unsatisfiable 0.21s 0.57s
% Output : Refutation 0.21s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.13 % Problem : KRS096+1 : TPTP v8.1.2. Released v3.1.0.
% 0.07/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.35 % Computer : n010.cluster.edu
% 0.13/0.35 % Model : x86_64 x86_64
% 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.35 % Memory : 8042.1875MB
% 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.35 % CPULimit : 300
% 0.13/0.35 % WCLimit : 300
% 0.13/0.35 % DateTime : Thu May 9 00:13:08 EDT 2024
% 0.13/0.35 % CPUTime :
% 0.21/0.57 % Version: 1.5
% 0.21/0.57 % SZS status Unsatisfiable
% 0.21/0.57 % SZS output start CNFRefutation
% 0.21/0.57 fof(axiom_3,axiom,(![X]:(cc(X)=>(~cd(X)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_3)).
% 0.21/0.57 fof(c9,plain,(![X]:(cc(X)=>~cd(X))),inference(fof_simplification,[status(thm)],[axiom_3])).
% 0.21/0.57 fof(c10,plain,(![X]:(~cc(X)|~cd(X))),inference(fof_nnf,[status(thm)],[c9])).
% 0.21/0.57 fof(c11,plain,(![X2]:(~cc(X2)|~cd(X2))),inference(variable_rename,[status(thm)],[c10])).
% 0.21/0.57 cnf(c12,plain,~cc(X40)|~cd(X40),inference(split_conjunct,[status(thm)],[c11])).
% 0.21/0.57 fof(axiom_4,axiom,cUnsatisfiable(i2003_11_14_17_20_18265),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_4)).
% 0.21/0.57 cnf(c8,plain,cUnsatisfiable(i2003_11_14_17_20_18265),inference(split_conjunct,[status(thm)],[axiom_4])).
% 0.21/0.57 fof(axiom_2,axiom,(![X]:(cUnsatisfiable(X)<=>(((?[Y]:(rr(X,Y)&cc(Y)))&(?[Y]:(rr(X,Y)&cd(Y))))&(![Y0]:(![Y1]:((rr(X,Y0)&rr(X,Y1))=>Y0=Y1)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_2)).
% 0.21/0.57 fof(c13,plain,(![X]:((~cUnsatisfiable(X)|(((?[Y]:(rr(X,Y)&cc(Y)))&(?[Y]:(rr(X,Y)&cd(Y))))&(![Y0]:(![Y1]:((~rr(X,Y0)|~rr(X,Y1))|Y0=Y1)))))&((((![Y]:(~rr(X,Y)|~cc(Y)))|(![Y]:(~rr(X,Y)|~cd(Y))))|(?[Y0]:(?[Y1]:((rr(X,Y0)&rr(X,Y1))&Y0!=Y1))))|cUnsatisfiable(X)))),inference(fof_nnf,[status(thm)],[axiom_2])).
% 0.21/0.57 fof(c14,plain,((![X]:(~cUnsatisfiable(X)|(((?[Y]:(rr(X,Y)&cc(Y)))&(?[Y]:(rr(X,Y)&cd(Y))))&(![Y0]:(![Y1]:((~rr(X,Y0)|~rr(X,Y1))|Y0=Y1))))))&(![X]:((((![Y]:(~rr(X,Y)|~cc(Y)))|(![Y]:(~rr(X,Y)|~cd(Y))))|(?[Y0]:(?[Y1]:((rr(X,Y0)&rr(X,Y1))&Y0!=Y1))))|cUnsatisfiable(X)))),inference(shift_quantors,[status(thm)],[c13])).
% 0.21/0.57 fof(c15,plain,((![X3]:(~cUnsatisfiable(X3)|(((?[X4]:(rr(X3,X4)&cc(X4)))&(?[X5]:(rr(X3,X5)&cd(X5))))&(![X6]:(![X7]:((~rr(X3,X6)|~rr(X3,X7))|X6=X7))))))&(![X8]:((((![X9]:(~rr(X8,X9)|~cc(X9)))|(![X10]:(~rr(X8,X10)|~cd(X10))))|(?[X11]:(?[X12]:((rr(X8,X11)&rr(X8,X12))&X11!=X12))))|cUnsatisfiable(X8)))),inference(variable_rename,[status(thm)],[c14])).
% 0.21/0.57 fof(c17,plain,(![X3]:(![X6]:(![X7]:(![X8]:(![X9]:(![X10]:((~cUnsatisfiable(X3)|(((rr(X3,skolem0001(X3))&cc(skolem0001(X3)))&(rr(X3,skolem0002(X3))&cd(skolem0002(X3))))&((~rr(X3,X6)|~rr(X3,X7))|X6=X7)))&((((~rr(X8,X9)|~cc(X9))|(~rr(X8,X10)|~cd(X10)))|((rr(X8,skolem0003(X8))&rr(X8,skolem0004(X8)))&skolem0003(X8)!=skolem0004(X8)))|cUnsatisfiable(X8))))))))),inference(shift_quantors,[status(thm)],[fof(c16,plain,((![X3]:(~cUnsatisfiable(X3)|(((rr(X3,skolem0001(X3))&cc(skolem0001(X3)))&(rr(X3,skolem0002(X3))&cd(skolem0002(X3))))&(![X6]:(![X7]:((~rr(X3,X6)|~rr(X3,X7))|X6=X7))))))&(![X8]:((((![X9]:(~rr(X8,X9)|~cc(X9)))|(![X10]:(~rr(X8,X10)|~cd(X10))))|((rr(X8,skolem0003(X8))&rr(X8,skolem0004(X8)))&skolem0003(X8)!=skolem0004(X8)))|cUnsatisfiable(X8)))),inference(skolemize,[status(esa)],[c15])).])).
% 0.21/0.57 fof(c18,plain,(![X3]:(![X6]:(![X7]:(![X8]:(![X9]:(![X10]:(((((~cUnsatisfiable(X3)|rr(X3,skolem0001(X3)))&(~cUnsatisfiable(X3)|cc(skolem0001(X3))))&((~cUnsatisfiable(X3)|rr(X3,skolem0002(X3)))&(~cUnsatisfiable(X3)|cd(skolem0002(X3)))))&(~cUnsatisfiable(X3)|((~rr(X3,X6)|~rr(X3,X7))|X6=X7)))&((((((~rr(X8,X9)|~cc(X9))|(~rr(X8,X10)|~cd(X10)))|rr(X8,skolem0003(X8)))|cUnsatisfiable(X8))&((((~rr(X8,X9)|~cc(X9))|(~rr(X8,X10)|~cd(X10)))|rr(X8,skolem0004(X8)))|cUnsatisfiable(X8)))&((((~rr(X8,X9)|~cc(X9))|(~rr(X8,X10)|~cd(X10)))|skolem0003(X8)!=skolem0004(X8))|cUnsatisfiable(X8)))))))))),inference(distribute,[status(thm)],[c17])).
% 0.21/0.57 cnf(c22,plain,~cUnsatisfiable(X51)|cd(skolem0002(X51)),inference(split_conjunct,[status(thm)],[c18])).
% 0.21/0.57 cnf(c72,plain,cd(skolem0002(i2003_11_14_17_20_18265)),inference(resolution,[status(thm)],[c22, c8])).
% 0.21/0.57 cnf(c73,plain,~cc(skolem0002(i2003_11_14_17_20_18265)),inference(resolution,[status(thm)],[c72, c12])).
% 0.21/0.57 cnf(c20,plain,~cUnsatisfiable(X47)|cc(skolem0001(X47)),inference(split_conjunct,[status(thm)],[c18])).
% 0.21/0.57 cnf(c69,plain,cc(skolem0001(i2003_11_14_17_20_18265)),inference(resolution,[status(thm)],[c20, c8])).
% 0.21/0.57 cnf(c1,axiom,X61!=X60|~cc(X61)|cc(X60),theory(equality)).
% 0.21/0.57 cnf(c19,plain,~cUnsatisfiable(X58)|rr(X58,skolem0001(X58)),inference(split_conjunct,[status(thm)],[c18])).
% 0.21/0.57 cnf(c75,plain,rr(i2003_11_14_17_20_18265,skolem0001(i2003_11_14_17_20_18265)),inference(resolution,[status(thm)],[c19, c8])).
% 0.21/0.57 cnf(c21,plain,~cUnsatisfiable(X59)|rr(X59,skolem0002(X59)),inference(split_conjunct,[status(thm)],[c18])).
% 0.21/0.57 cnf(c76,plain,rr(i2003_11_14_17_20_18265,skolem0002(i2003_11_14_17_20_18265)),inference(resolution,[status(thm)],[c21, c8])).
% 0.21/0.57 cnf(c23,plain,~cUnsatisfiable(X93)|~rr(X93,X94)|~rr(X93,X92)|X94=X92,inference(split_conjunct,[status(thm)],[c18])).
% 0.21/0.57 cnf(c84,plain,~cUnsatisfiable(i2003_11_14_17_20_18265)|~rr(i2003_11_14_17_20_18265,X124)|X124=skolem0002(i2003_11_14_17_20_18265),inference(resolution,[status(thm)],[c23, c76])).
% 0.21/0.57 cnf(c103,plain,~cUnsatisfiable(i2003_11_14_17_20_18265)|skolem0001(i2003_11_14_17_20_18265)=skolem0002(i2003_11_14_17_20_18265),inference(resolution,[status(thm)],[c84, c75])).
% 0.21/0.57 cnf(c104,plain,skolem0001(i2003_11_14_17_20_18265)=skolem0002(i2003_11_14_17_20_18265),inference(resolution,[status(thm)],[c103, c8])).
% 0.21/0.57 cnf(c108,plain,~cc(skolem0001(i2003_11_14_17_20_18265))|cc(skolem0002(i2003_11_14_17_20_18265)),inference(resolution,[status(thm)],[c104, c1])).
% 0.21/0.57 cnf(c125,plain,cc(skolem0002(i2003_11_14_17_20_18265)),inference(resolution,[status(thm)],[c108, c69])).
% 0.21/0.57 cnf(c126,plain,$false,inference(resolution,[status(thm)],[c125, c73])).
% 0.21/0.57 % SZS output end CNFRefutation
% 0.21/0.57
% 0.21/0.57 % Initial clauses : 34
% 0.21/0.57 % Processed clauses : 43
% 0.21/0.57 % Factors computed : 4
% 0.21/0.57 % Resolvents computed: 56
% 0.21/0.57 % Tautologies deleted: 8
% 0.21/0.57 % Forward subsumed : 23
% 0.21/0.57 % Backward subsumed : 2
% 0.21/0.57 % -------- CPU Time ---------
% 0.21/0.57 % User time : 0.207 s
% 0.21/0.57 % System time : 0.013 s
% 0.21/0.57 % Total time : 0.220 s
%------------------------------------------------------------------------------