%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : KRS100+1 : TPTP v8.1.2. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n018.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:42 EDT 2024
% Result : Unsatisfiable 0.19s 0.52s
% Output : Refutation 0.19s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : KRS100+1 : TPTP v8.1.2. Released v3.1.0.
% 0.07/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.12/0.34 % Computer : n018.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 300
% 0.12/0.34 % DateTime : Thu May 9 00:12:08 EDT 2024
% 0.12/0.34 % CPUTime :
% 0.19/0.52 % Version: 1.5
% 0.19/0.52 % SZS status Unsatisfiable
% 0.19/0.52 % SZS output start CNFRefutation
% 0.19/0.52 fof(axiom_4,axiom,cUnsatisfiable(i2003_11_14_17_20_32704),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_4)).
% 0.19/0.52 cnf(c0,plain,cUnsatisfiable(i2003_11_14_17_20_32704),inference(split_conjunct,[status(thm)],[axiom_4])).
% 0.19/0.52 fof(axiom_2,axiom,(![X]:(cUnsatisfiable(X)<=>(((![Y]:(rr(X,Y)=>(ce(Y)|(~cd(Y)))))&(![Y]:(rr(X,Y)=>cd(Y))))&(?[Y]:(rr(X,Y)&(~ce(Y))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_2)).
% 0.19/0.52 fof(c5,plain,(![X]:(cUnsatisfiable(X)<=>(((![Y]:(rr(X,Y)=>(ce(Y)|~cd(Y))))&(![Y]:(rr(X,Y)=>cd(Y))))&(?[Y]:(rr(X,Y)&~ce(Y)))))),inference(fof_simplification,[status(thm)],[axiom_2])).
% 0.19/0.52 fof(c6,plain,(![X]:((~cUnsatisfiable(X)|(((![Y]:(~rr(X,Y)|(ce(Y)|~cd(Y))))&(![Y]:(~rr(X,Y)|cd(Y))))&(?[Y]:(rr(X,Y)&~ce(Y)))))&((((?[Y]:(rr(X,Y)&(~ce(Y)&cd(Y))))|(?[Y]:(rr(X,Y)&~cd(Y))))|(![Y]:(~rr(X,Y)|ce(Y))))|cUnsatisfiable(X)))),inference(fof_nnf,[status(thm)],[c5])).
% 0.19/0.52 fof(c7,plain,((![X]:(~cUnsatisfiable(X)|(((![Y]:(~rr(X,Y)|(ce(Y)|~cd(Y))))&(![Y]:(~rr(X,Y)|cd(Y))))&(?[Y]:(rr(X,Y)&~ce(Y))))))&(![X]:((((?[Y]:(rr(X,Y)&(~ce(Y)&cd(Y))))|(?[Y]:(rr(X,Y)&~cd(Y))))|(![Y]:(~rr(X,Y)|ce(Y))))|cUnsatisfiable(X)))),inference(shift_quantors,[status(thm)],[c6])).
% 0.19/0.52 fof(c8,plain,((![X3]:(~cUnsatisfiable(X3)|(((![X4]:(~rr(X3,X4)|(ce(X4)|~cd(X4))))&(![X5]:(~rr(X3,X5)|cd(X5))))&(?[X6]:(rr(X3,X6)&~ce(X6))))))&(![X7]:((((?[X8]:(rr(X7,X8)&(~ce(X8)&cd(X8))))|(?[X9]:(rr(X7,X9)&~cd(X9))))|(![X10]:(~rr(X7,X10)|ce(X10))))|cUnsatisfiable(X7)))),inference(variable_rename,[status(thm)],[c7])).
% 0.19/0.52 fof(c10,plain,(![X3]:(![X4]:(![X5]:(![X7]:(![X10]:((~cUnsatisfiable(X3)|(((~rr(X3,X4)|(ce(X4)|~cd(X4)))&(~rr(X3,X5)|cd(X5)))&(rr(X3,skolem0001(X3))&~ce(skolem0001(X3)))))&((((rr(X7,skolem0002(X7))&(~ce(skolem0002(X7))&cd(skolem0002(X7))))|(rr(X7,skolem0003(X7))&~cd(skolem0003(X7))))|(~rr(X7,X10)|ce(X10)))|cUnsatisfiable(X7)))))))),inference(shift_quantors,[status(thm)],[fof(c9,plain,((![X3]:(~cUnsatisfiable(X3)|(((![X4]:(~rr(X3,X4)|(ce(X4)|~cd(X4))))&(![X5]:(~rr(X3,X5)|cd(X5))))&(rr(X3,skolem0001(X3))&~ce(skolem0001(X3))))))&(![X7]:((((rr(X7,skolem0002(X7))&(~ce(skolem0002(X7))&cd(skolem0002(X7))))|(rr(X7,skolem0003(X7))&~cd(skolem0003(X7))))|(![X10]:(~rr(X7,X10)|ce(X10))))|cUnsatisfiable(X7)))),inference(skolemize,[status(esa)],[c8])).])).
% 0.19/0.52 fof(c11,plain,(![X3]:(![X4]:(![X5]:(![X7]:(![X10]:((((~cUnsatisfiable(X3)|(~rr(X3,X4)|(ce(X4)|~cd(X4))))&(~cUnsatisfiable(X3)|(~rr(X3,X5)|cd(X5))))&((~cUnsatisfiable(X3)|rr(X3,skolem0001(X3)))&(~cUnsatisfiable(X3)|~ce(skolem0001(X3)))))&(((((rr(X7,skolem0002(X7))|rr(X7,skolem0003(X7)))|(~rr(X7,X10)|ce(X10)))|cUnsatisfiable(X7))&(((rr(X7,skolem0002(X7))|~cd(skolem0003(X7)))|(~rr(X7,X10)|ce(X10)))|cUnsatisfiable(X7)))&(((((~ce(skolem0002(X7))|rr(X7,skolem0003(X7)))|(~rr(X7,X10)|ce(X10)))|cUnsatisfiable(X7))&(((~ce(skolem0002(X7))|~cd(skolem0003(X7)))|(~rr(X7,X10)|ce(X10)))|cUnsatisfiable(X7)))&((((cd(skolem0002(X7))|rr(X7,skolem0003(X7)))|(~rr(X7,X10)|ce(X10)))|cUnsatisfiable(X7))&(((cd(skolem0002(X7))|~cd(skolem0003(X7)))|(~rr(X7,X10)|ce(X10)))|cUnsatisfiable(X7))))))))))),inference(distribute,[status(thm)],[c10])).
% 0.19/0.52 cnf(c15,plain,~cUnsatisfiable(X23)|~ce(skolem0001(X23)),inference(split_conjunct,[status(thm)],[c11])).
% 0.19/0.52 cnf(c14,plain,~cUnsatisfiable(X24)|rr(X24,skolem0001(X24)),inference(split_conjunct,[status(thm)],[c11])).
% 0.19/0.52 cnf(c36,plain,rr(i2003_11_14_17_20_32704,skolem0001(i2003_11_14_17_20_32704)),inference(resolution,[status(thm)],[c14, c0])).
% 0.19/0.52 cnf(c13,plain,~cUnsatisfiable(X26)|~rr(X26,X25)|cd(X25),inference(split_conjunct,[status(thm)],[c11])).
% 0.19/0.52 cnf(c38,plain,~cUnsatisfiable(i2003_11_14_17_20_32704)|cd(skolem0001(i2003_11_14_17_20_32704)),inference(resolution,[status(thm)],[c13, c36])).
% 0.19/0.52 cnf(c39,plain,cd(skolem0001(i2003_11_14_17_20_32704)),inference(resolution,[status(thm)],[c38, c0])).
% 0.19/0.52 cnf(c12,plain,~cUnsatisfiable(X20)|~rr(X20,X19)|ce(X19)|~cd(X19),inference(split_conjunct,[status(thm)],[c11])).
% 0.19/0.52 cnf(c37,plain,~cUnsatisfiable(i2003_11_14_17_20_32704)|ce(skolem0001(i2003_11_14_17_20_32704))|~cd(skolem0001(i2003_11_14_17_20_32704)),inference(resolution,[status(thm)],[c36, c12])).
% 0.19/0.52 cnf(c41,plain,~cUnsatisfiable(i2003_11_14_17_20_32704)|ce(skolem0001(i2003_11_14_17_20_32704)),inference(resolution,[status(thm)],[c37, c39])).
% 0.19/0.52 cnf(c42,plain,ce(skolem0001(i2003_11_14_17_20_32704)),inference(resolution,[status(thm)],[c41, c0])).
% 0.19/0.52 cnf(c44,plain,~cUnsatisfiable(i2003_11_14_17_20_32704),inference(resolution,[status(thm)],[c42, c15])).
% 0.19/0.52 cnf(c45,plain,$false,inference(resolution,[status(thm)],[c44, c0])).
% 0.19/0.52 % SZS output end CNFRefutation
% 0.19/0.52
% 0.19/0.52 % Initial clauses : 16
% 0.19/0.52 % Processed clauses : 19
% 0.19/0.52 % Factors computed : 0
% 0.19/0.52 % Resolvents computed: 11
% 0.19/0.52 % Tautologies deleted: 1
% 0.19/0.52 % Forward subsumed : 0
% 0.19/0.52 % Backward subsumed : 3
% 0.19/0.52 % -------- CPU Time ---------
% 0.19/0.52 % User time : 0.161 s
% 0.19/0.52 % System time : 0.018 s
% 0.19/0.52 % Total time : 0.179 s
%------------------------------------------------------------------------------