%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SWC254+1 : TPTP v8.1.2. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n024.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:43:41 EDT 2024
% Result : Theorem 53.71s 53.93s
% Output : Refutation 53.71s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12 % Problem : SWC254+1 : TPTP v8.1.2. Released v2.4.0.
% 0.06/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.12/0.34 % Computer : n024.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 02:37:53 EDT 2024
% 0.12/0.34 % CPUTime :
% 53.71/53.93 % Version: 1.5
% 53.71/53.93 % SZS status Theorem
% 53.71/53.93 % SZS output start CNFRefutation
% 53.71/53.93 fof(co1,conjecture,(![U]:(ssList(U)=>(![V]:(ssList(V)=>(![W]:(ssList(W)=>(![X]:(ssList(X)=>((V!=X|U!=W)|((((~neq(V,nil))|(![Y]:(ssItem(Y)=>(![Z]:(ssList(Z)=>(cons(Y,nil)!=W|app(Z,cons(Y,nil))!=X))))))|singletonP(U))&((~neq(V,nil))|neq(X,nil)))))))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', co1)).
% 53.71/53.93 fof(c23,negated_conjecture,(~(![U]:(ssList(U)=>(![V]:(ssList(V)=>(![W]:(ssList(W)=>(![X]:(ssList(X)=>((V!=X|U!=W)|((((~neq(V,nil))|(![Y]:(ssItem(Y)=>(![Z]:(ssList(Z)=>(cons(Y,nil)!=W|app(Z,cons(Y,nil))!=X))))))|singletonP(U))&((~neq(V,nil))|neq(X,nil))))))))))))),inference(assume_negation,[status(cth)],[co1])).
% 53.71/53.93 fof(c24,negated_conjecture,(~(![U]:(ssList(U)=>(![V]:(ssList(V)=>(![W]:(ssList(W)=>(![X]:(ssList(X)=>((V!=X|U!=W)|(((~neq(V,nil)|(![Y]:(ssItem(Y)=>(![Z]:(ssList(Z)=>(cons(Y,nil)!=W|app(Z,cons(Y,nil))!=X))))))|singletonP(U))&(~neq(V,nil)|neq(X,nil))))))))))))),inference(fof_simplification,[status(thm)],[c23])).
% 53.71/53.93 fof(c25,negated_conjecture,(?[U]:(ssList(U)&(?[V]:(ssList(V)&(?[W]:(ssList(W)&(?[X]:(ssList(X)&((V=X&U=W)&(((neq(V,nil)&(?[Y]:(ssItem(Y)&(?[Z]:(ssList(Z)&(cons(Y,nil)=W&app(Z,cons(Y,nil))=X))))))&~singletonP(U))|(neq(V,nil)&~neq(X,nil)))))))))))),inference(fof_nnf,[status(thm)],[c24])).
% 53.71/53.93 fof(c26,negated_conjecture,(?[X2]:(ssList(X2)&(?[X3]:(ssList(X3)&(?[X4]:(ssList(X4)&(?[X5]:(ssList(X5)&((X3=X5&X2=X4)&(((neq(X3,nil)&(?[X6]:(ssItem(X6)&(?[X7]:(ssList(X7)&(cons(X6,nil)=X4&app(X7,cons(X6,nil))=X5))))))&~singletonP(X2))|(neq(X3,nil)&~neq(X5,nil)))))))))))),inference(variable_rename,[status(thm)],[c25])).
% 53.71/53.93 fof(c27,negated_conjecture,(ssList(skolem0001)&(ssList(skolem0002)&(ssList(skolem0003)&(ssList(skolem0004)&((skolem0002=skolem0004&skolem0001=skolem0003)&(((neq(skolem0002,nil)&(ssItem(skolem0005)&(ssList(skolem0006)&(cons(skolem0005,nil)=skolem0003&app(skolem0006,cons(skolem0005,nil))=skolem0004))))&~singletonP(skolem0001))|(neq(skolem0002,nil)&~neq(skolem0004,nil)))))))),inference(skolemize,[status(esa)],[c26])).
% 53.71/53.93 fof(c28,negated_conjecture,(ssList(skolem0001)&(ssList(skolem0002)&(ssList(skolem0003)&(ssList(skolem0004)&((skolem0002=skolem0004&skolem0001=skolem0003)&((((neq(skolem0002,nil)|neq(skolem0002,nil))&(neq(skolem0002,nil)|~neq(skolem0004,nil)))&(((ssItem(skolem0005)|neq(skolem0002,nil))&(ssItem(skolem0005)|~neq(skolem0004,nil)))&(((ssList(skolem0006)|neq(skolem0002,nil))&(ssList(skolem0006)|~neq(skolem0004,nil)))&(((cons(skolem0005,nil)=skolem0003|neq(skolem0002,nil))&(cons(skolem0005,nil)=skolem0003|~neq(skolem0004,nil)))&((app(skolem0006,cons(skolem0005,nil))=skolem0004|neq(skolem0002,nil))&(app(skolem0006,cons(skolem0005,nil))=skolem0004|~neq(skolem0004,nil)))))))&((~singletonP(skolem0001)|neq(skolem0002,nil))&(~singletonP(skolem0001)|~neq(skolem0004,nil))))))))),inference(distribute,[status(thm)],[c27])).
% 53.71/53.93 cnf(c46,negated_conjecture,~singletonP(skolem0001)|~neq(skolem0004,nil),inference(split_conjunct,[status(thm)],[c28])).
% 53.71/53.93 cnf(c33,negated_conjecture,skolem0002=skolem0004,inference(split_conjunct,[status(thm)],[c28])).
% 53.71/53.93 cnf(reflexivity,axiom,X252=X252,theory(equality)).
% 53.71/53.93 cnf(c5,axiom,X279!=X280|X278!=X277|~neq(X279,X278)|neq(X280,X277),theory(equality)).
% 53.71/53.93 cnf(c35,negated_conjecture,neq(skolem0002,nil)|neq(skolem0002,nil),inference(split_conjunct,[status(thm)],[c28])).
% 53.71/53.93 cnf(c677,plain,neq(skolem0002,nil),inference(factor,[status(thm)],[c35])).
% 53.71/53.93 cnf(c680,plain,skolem0002!=X862|nil!=X863|neq(X862,X863),inference(resolution,[status(thm)],[c677, c5])).
% 53.71/53.93 cnf(c20621,plain,skolem0002!=X895|neq(X895,nil),inference(resolution,[status(thm)],[c680, reflexivity])).
% 53.71/53.93 cnf(c21319,plain,neq(skolem0004,nil),inference(resolution,[status(thm)],[c20621, c33])).
% 53.71/53.93 cnf(c21324,plain,~singletonP(skolem0001),inference(resolution,[status(thm)],[c21319, c46])).
% 53.71/53.93 cnf(symmetry,axiom,X254!=X253|X253=X254,theory(equality)).
% 53.71/53.93 cnf(c34,negated_conjecture,skolem0001=skolem0003,inference(split_conjunct,[status(thm)],[c28])).
% 53.71/53.93 cnf(c524,plain,skolem0003=skolem0001,inference(resolution,[status(thm)],[c34, symmetry])).
% 53.71/53.93 cnf(c8,axiom,X292!=X293|~singletonP(X292)|singletonP(X293),theory(equality)).
% 53.71/53.93 cnf(c584,plain,~singletonP(skolem0003)|singletonP(skolem0001),inference(resolution,[status(thm)],[c8, c524])).
% 53.71/53.93 cnf(c31,negated_conjecture,ssList(skolem0003),inference(split_conjunct,[status(thm)],[c28])).
% 53.71/53.93 cnf(c38,negated_conjecture,ssItem(skolem0005)|~neq(skolem0004,nil),inference(split_conjunct,[status(thm)],[c28])).
% 53.71/53.93 cnf(c21327,plain,ssItem(skolem0005),inference(resolution,[status(thm)],[c21319, c38])).
% 53.71/53.93 fof(ax4,axiom,(![U]:(ssList(U)=>(singletonP(U)<=>(?[V]:(ssItem(V)&cons(V,nil)=U))))),file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax4)).
% 53.71/53.93 fof(c488,plain,(![U]:(~ssList(U)|((~singletonP(U)|(?[V]:(ssItem(V)&cons(V,nil)=U)))&((![V]:(~ssItem(V)|cons(V,nil)!=U))|singletonP(U))))),inference(fof_nnf,[status(thm)],[ax4])).
% 53.71/53.93 fof(c489,plain,(![X239]:(~ssList(X239)|((~singletonP(X239)|(?[X240]:(ssItem(X240)&cons(X240,nil)=X239)))&((![X241]:(~ssItem(X241)|cons(X241,nil)!=X239))|singletonP(X239))))),inference(variable_rename,[status(thm)],[c488])).
% 53.71/53.93 fof(c491,plain,(![X239]:(![X241]:(~ssList(X239)|((~singletonP(X239)|(ssItem(skolem0049(X239))&cons(skolem0049(X239),nil)=X239))&((~ssItem(X241)|cons(X241,nil)!=X239)|singletonP(X239)))))),inference(shift_quantors,[status(thm)],[fof(c490,plain,(![X239]:(~ssList(X239)|((~singletonP(X239)|(ssItem(skolem0049(X239))&cons(skolem0049(X239),nil)=X239))&((![X241]:(~ssItem(X241)|cons(X241,nil)!=X239))|singletonP(X239))))),inference(skolemize,[status(esa)],[c489])).])).
% 53.71/53.93 fof(c492,plain,(![X239]:(![X241]:(((~ssList(X239)|(~singletonP(X239)|ssItem(skolem0049(X239))))&(~ssList(X239)|(~singletonP(X239)|cons(skolem0049(X239),nil)=X239)))&(~ssList(X239)|((~ssItem(X241)|cons(X241,nil)!=X239)|singletonP(X239)))))),inference(distribute,[status(thm)],[c491])).
% 53.71/53.93 cnf(c495,plain,~ssList(X684)|~ssItem(X683)|cons(X683,nil)!=X684|singletonP(X684),inference(split_conjunct,[status(thm)],[c492])).
% 53.71/53.93 cnf(c42,negated_conjecture,cons(skolem0005,nil)=skolem0003|~neq(skolem0004,nil),inference(split_conjunct,[status(thm)],[c28])).
% 53.71/53.93 cnf(c21329,plain,cons(skolem0005,nil)=skolem0003,inference(resolution,[status(thm)],[c21319, c42])).
% 53.71/53.93 cnf(c22355,plain,~ssList(skolem0003)|~ssItem(skolem0005)|singletonP(skolem0003),inference(resolution,[status(thm)],[c21329, c495])).
% 53.71/53.93 cnf(c95234,plain,~ssList(skolem0003)|singletonP(skolem0003),inference(resolution,[status(thm)],[c22355, c21327])).
% 53.71/53.93 cnf(c95235,plain,singletonP(skolem0003),inference(resolution,[status(thm)],[c95234, c31])).
% 53.71/53.93 cnf(c95238,plain,singletonP(skolem0001),inference(resolution,[status(thm)],[c95235, c584])).
% 53.71/53.93 cnf(c95245,plain,$false,inference(resolution,[status(thm)],[c95238, c21324])).
% 53.71/53.93 % SZS output end CNFRefutation
% 53.71/53.93
% 53.71/53.93 % Initial clauses : 234
% 53.71/53.93 % Processed clauses : 2773
% 53.71/53.93 % Factors computed : 53
% 53.71/53.93 % Resolvents computed: 94677
% 53.71/53.93 % Tautologies deleted: 23
% 53.71/53.93 % Forward subsumed : 684
% 53.71/53.93 % Backward subsumed : 347
% 53.71/53.93 % -------- CPU Time ---------
% 53.71/53.93 % User time : 53.378 s
% 53.71/53.93 % System time : 0.200 s
% 53.71/53.93 % Total time : 53.578 s
%------------------------------------------------------------------------------