↑ Up

PyRes---1.5.THM-Ref.s

View TPTP
Problem Process solution in
SystemOnTSTP Download .tgz 
%------------------------------------------------------------------------------
% File     : PyRes---1.5
% Problem  : SWV181+1 : TPTP v8.1.2. Bugfixed v3.3.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s

% Computer : n025.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:44:23 EDT 2024

% Result   : Theorem 198.09s 198.37s
% Output   : Refutation 198.09s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.13  % Problem  : SWV181+1 : TPTP v8.1.2. Bugfixed v3.3.0.
% 0.08/0.13  % Command  : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.35  % Computer : n025.cluster.edu
% 0.14/0.35  % Model    : x86_64 x86_64
% 0.14/0.35  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.35  % Memory   : 8042.1875MB
% 0.14/0.35  % OS       : Linux 3.10.0-693.el7.x86_64
% 0.14/0.35  % CPULimit : 300
% 0.14/0.35  % WCLimit  : 300
% 0.14/0.35  % DateTime : Thu May  9 05:46:08 EDT 2024
% 0.14/0.35  % CPUTime  : 
% 198.09/198.37  % Version:  1.5
% 198.09/198.37  % SZS status Theorem
% 198.09/198.37  % SZS output start CNFRefutation
% 198.09/198.37  fof(irreflexivity_gt,axiom,(![X]:(~gt(X,X))),file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax', irreflexivity_gt)).
% 198.09/198.37  fof(c467,plain,(![X]:~gt(X,X)),inference(fof_simplification,[status(thm)],[irreflexivity_gt])).
% 198.09/198.37  fof(c468,plain,(![X181]:~gt(X181,X181)),inference(variable_rename,[status(thm)],[c467])).
% 198.09/198.37  cnf(c469,plain,~gt(X189,X189),inference(split_conjunct,[status(thm)],[c468])).
% 198.09/198.37  fof(leq_succ_gt,axiom,(![X]:(![Y]:(leq(succ(X),Y)=>gt(Y,X)))),file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax', leq_succ_gt)).
% 198.09/198.37  fof(c124,plain,(![X]:(![Y]:(~leq(succ(X),Y)|gt(Y,X)))),inference(fof_nnf,[status(thm)],[leq_succ_gt])).
% 198.09/198.37  fof(c125,plain,(![X49]:(![X50]:(~leq(succ(X49),X50)|gt(X50,X49)))),inference(variable_rename,[status(thm)],[c124])).
% 198.09/198.37  cnf(c126,plain,~leq(succ(X349),X348)|gt(X348,X349),inference(split_conjunct,[status(thm)],[c125])).
% 198.09/198.37  fof(cl5_nebula_init_0081,conjecture,((((((((leq(tptp_float_0_001,pv76)&leq(n1,loopcounter))&gt(n1,loopcounter))&(![A]:((leq(n0,A)&leq(A,n135299))=>(![B]:((leq(n0,B)&leq(B,n4))=>a_select3(q_init,A,B)=init)))))&(![C]:((leq(n0,C)&leq(C,n4))=>a_select3(center_init,C,n0)=init)))&(gt(loopcounter,n0)=>(![D]:((leq(n0,D)&leq(D,n4))=>a_select2(mu_init,D)=init))))&(gt(loopcounter,n0)=>(![E]:((leq(n0,E)&leq(E,n4))=>a_select2(rho_init,E)=init))))&(gt(loopcounter,n0)=>(![F]:((leq(n0,F)&leq(F,n4))=>a_select2(sigma_init,F)=init))))=>(![G]:((leq(n0,G)&leq(G,n4))=>a_select2(muold_init,G)=init))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', cl5_nebula_init_0081)).
% 198.09/198.37  fof(c73,negated_conjecture,(~((((((((leq(tptp_float_0_001,pv76)&leq(n1,loopcounter))&gt(n1,loopcounter))&(![A]:((leq(n0,A)&leq(A,n135299))=>(![B]:((leq(n0,B)&leq(B,n4))=>a_select3(q_init,A,B)=init)))))&(![C]:((leq(n0,C)&leq(C,n4))=>a_select3(center_init,C,n0)=init)))&(gt(loopcounter,n0)=>(![D]:((leq(n0,D)&leq(D,n4))=>a_select2(mu_init,D)=init))))&(gt(loopcounter,n0)=>(![E]:((leq(n0,E)&leq(E,n4))=>a_select2(rho_init,E)=init))))&(gt(loopcounter,n0)=>(![F]:((leq(n0,F)&leq(F,n4))=>a_select2(sigma_init,F)=init))))=>(![G]:((leq(n0,G)&leq(G,n4))=>a_select2(muold_init,G)=init)))),inference(assume_negation,[status(cth)],[cl5_nebula_init_0081])).
% 198.09/198.37  fof(c74,negated_conjecture,((((((((leq(tptp_float_0_001,pv76)&leq(n1,loopcounter))&gt(n1,loopcounter))&(![A]:((~leq(n0,A)|~leq(A,n135299))|(![B]:((~leq(n0,B)|~leq(B,n4))|a_select3(q_init,A,B)=init)))))&(![C]:((~leq(n0,C)|~leq(C,n4))|a_select3(center_init,C,n0)=init)))&(~gt(loopcounter,n0)|(![D]:((~leq(n0,D)|~leq(D,n4))|a_select2(mu_init,D)=init))))&(~gt(loopcounter,n0)|(![E]:((~leq(n0,E)|~leq(E,n4))|a_select2(rho_init,E)=init))))&(~gt(loopcounter,n0)|(![F]:((~leq(n0,F)|~leq(F,n4))|a_select2(sigma_init,F)=init))))&(?[G]:((leq(n0,G)&leq(G,n4))&a_select2(muold_init,G)!=init))),inference(fof_nnf,[status(thm)],[c73])).
% 198.09/198.37  fof(c75,negated_conjecture,((((((((leq(tptp_float_0_001,pv76)&leq(n1,loopcounter))&gt(n1,loopcounter))&(![X8]:((~leq(n0,X8)|~leq(X8,n135299))|(![X9]:((~leq(n0,X9)|~leq(X9,n4))|a_select3(q_init,X8,X9)=init)))))&(![X10]:((~leq(n0,X10)|~leq(X10,n4))|a_select3(center_init,X10,n0)=init)))&(~gt(loopcounter,n0)|(![X11]:((~leq(n0,X11)|~leq(X11,n4))|a_select2(mu_init,X11)=init))))&(~gt(loopcounter,n0)|(![X12]:((~leq(n0,X12)|~leq(X12,n4))|a_select2(rho_init,X12)=init))))&(~gt(loopcounter,n0)|(![X13]:((~leq(n0,X13)|~leq(X13,n4))|a_select2(sigma_init,X13)=init))))&(?[X14]:((leq(n0,X14)&leq(X14,n4))&a_select2(muold_init,X14)!=init))),inference(variable_rename,[status(thm)],[c74])).
% 198.09/198.37  fof(c77,negated_conjecture,(![X8]:(![X9]:(![X10]:(![X11]:(![X12]:(![X13]:((((((((leq(tptp_float_0_001,pv76)&leq(n1,loopcounter))&gt(n1,loopcounter))&((~leq(n0,X8)|~leq(X8,n135299))|((~leq(n0,X9)|~leq(X9,n4))|a_select3(q_init,X8,X9)=init)))&((~leq(n0,X10)|~leq(X10,n4))|a_select3(center_init,X10,n0)=init))&(~gt(loopcounter,n0)|((~leq(n0,X11)|~leq(X11,n4))|a_select2(mu_init,X11)=init)))&(~gt(loopcounter,n0)|((~leq(n0,X12)|~leq(X12,n4))|a_select2(rho_init,X12)=init)))&(~gt(loopcounter,n0)|((~leq(n0,X13)|~leq(X13,n4))|a_select2(sigma_init,X13)=init)))&((leq(n0,skolem0001)&leq(skolem0001,n4))&a_select2(muold_init,skolem0001)!=init)))))))),inference(shift_quantors,[status(thm)],[fof(c76,negated_conjecture,((((((((leq(tptp_float_0_001,pv76)&leq(n1,loopcounter))&gt(n1,loopcounter))&(![X8]:((~leq(n0,X8)|~leq(X8,n135299))|(![X9]:((~leq(n0,X9)|~leq(X9,n4))|a_select3(q_init,X8,X9)=init)))))&(![X10]:((~leq(n0,X10)|~leq(X10,n4))|a_select3(center_init,X10,n0)=init)))&(~gt(loopcounter,n0)|(![X11]:((~leq(n0,X11)|~leq(X11,n4))|a_select2(mu_init,X11)=init))))&(~gt(loopcounter,n0)|(![X12]:((~leq(n0,X12)|~leq(X12,n4))|a_select2(rho_init,X12)=init))))&(~gt(loopcounter,n0)|(![X13]:((~leq(n0,X13)|~leq(X13,n4))|a_select2(sigma_init,X13)=init))))&((leq(n0,skolem0001)&leq(skolem0001,n4))&a_select2(muold_init,skolem0001)!=init)),inference(skolemize,[status(esa)],[c75])).])).
% 198.09/198.37  cnf(c79,negated_conjecture,leq(n1,loopcounter),inference(split_conjunct,[status(thm)],[c77])).
% 198.09/198.37  fof(transitivity_leq,axiom,(![X]:(![Y]:(![Z]:((leq(X,Y)&leq(Y,Z))=>leq(X,Z))))),file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax', transitivity_leq)).
% 198.09/198.37  fof(c462,plain,(![X]:(![Y]:(![Z]:((~leq(X,Y)|~leq(Y,Z))|leq(X,Z))))),inference(fof_nnf,[status(thm)],[transitivity_leq])).
% 198.09/198.37  fof(c463,plain,(![X177]:(![X178]:(![X179]:((~leq(X177,X178)|~leq(X178,X179))|leq(X177,X179))))),inference(variable_rename,[status(thm)],[c462])).
% 198.09/198.37  cnf(c464,plain,~leq(X2185,X2186)|~leq(X2186,X2184)|leq(X2185,X2184),inference(split_conjunct,[status(thm)],[c463])).
% 198.09/198.37  cnf(c35962,plain,~leq(X2700,n1)|leq(X2700,loopcounter),inference(resolution,[status(thm)],[c464, c79])).
% 198.09/198.37  cnf(symmetry,axiom,X191!=X190|X190=X191,theory(equality)).
% 198.09/198.37  fof(successor_1,axiom,succ(n0)=n1,file('/export/starexec/sandbox/benchmark/theBenchmark.p', successor_1)).
% 198.09/198.37  cnf(c24,plain,succ(n0)=n1,inference(split_conjunct,[status(thm)],[successor_1])).
% 198.09/198.37  cnf(c493,plain,n1=succ(n0),inference(resolution,[status(thm)],[c24, symmetry])).
% 198.09/198.37  cnf(reflexivity,axiom,X187=X187,theory(equality)).
% 198.09/198.37  fof(reflexivity_leq,axiom,(![X]:leq(X,X)),file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax', reflexivity_leq)).
% 198.09/198.37  fof(c465,plain,(![X180]:leq(X180,X180)),inference(variable_rename,[status(thm)],[reflexivity_leq])).
% 198.09/198.37  cnf(c466,plain,leq(X188,X188),inference(split_conjunct,[status(thm)],[c465])).
% 198.09/198.37  cnf(c19,axiom,X291!=X289|X290!=X292|~leq(X291,X290)|leq(X289,X292),theory(equality)).
% 198.09/198.37  cnf(c755,plain,X2874!=X2875|X2874!=X2873|leq(X2875,X2873),inference(resolution,[status(thm)],[c19, c466])).
% 198.09/198.37  cnf(c55855,plain,X2879!=X2878|leq(X2878,X2879),inference(resolution,[status(thm)],[c755, reflexivity])).
% 198.09/198.37  cnf(c55900,plain,leq(succ(n0),n1),inference(resolution,[status(thm)],[c55855, c493])).
% 198.09/198.37  cnf(c56613,plain,leq(succ(n0),loopcounter),inference(resolution,[status(thm)],[c55900, c35962])).
% 198.09/198.37  fof(leq_succ_gt_equiv,axiom,(![X]:(![Y]:(leq(X,Y)<=>gt(succ(Y),X)))),file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax', leq_succ_gt_equiv)).
% 198.09/198.37  fof(c427,plain,(![X]:(![Y]:((~leq(X,Y)|gt(succ(Y),X))&(~gt(succ(Y),X)|leq(X,Y))))),inference(fof_nnf,[status(thm)],[leq_succ_gt_equiv])).
% 198.09/198.37  fof(c428,plain,((![X]:(![Y]:(~leq(X,Y)|gt(succ(Y),X))))&(![X]:(![Y]:(~gt(succ(Y),X)|leq(X,Y))))),inference(shift_quantors,[status(thm)],[c427])).
% 198.09/198.37  fof(c430,plain,(![X154]:(![X155]:(![X156]:(![X157]:((~leq(X154,X155)|gt(succ(X155),X154))&(~gt(succ(X157),X156)|leq(X156,X157))))))),inference(shift_quantors,[status(thm)],[fof(c429,plain,((![X154]:(![X155]:(~leq(X154,X155)|gt(succ(X155),X154))))&(![X156]:(![X157]:(~gt(succ(X157),X156)|leq(X156,X157))))),inference(variable_rename,[status(thm)],[c428])).])).
% 198.09/198.37  cnf(c432,plain,~gt(succ(X649),X648)|leq(X648,X649),inference(split_conjunct,[status(thm)],[c430])).
% 198.09/198.37  cnf(c80,negated_conjecture,gt(n1,loopcounter),inference(split_conjunct,[status(thm)],[c77])).
% 198.09/198.37  cnf(c18,axiom,X287!=X285|X286!=X288|~gt(X287,X286)|gt(X285,X288),theory(equality)).
% 198.09/198.37  cnf(c701,plain,n1!=X2713|loopcounter!=X2714|gt(X2713,X2714),inference(resolution,[status(thm)],[c18, c80])).
% 198.09/198.37  cnf(c52514,plain,n1!=X3357|gt(X3357,loopcounter),inference(resolution,[status(thm)],[c701, reflexivity])).
% 198.09/198.37  cnf(c82958,plain,gt(succ(n0),loopcounter),inference(resolution,[status(thm)],[c52514, c493])).
% 198.09/198.37  cnf(c82960,plain,leq(loopcounter,n0),inference(resolution,[status(thm)],[c82958, c432])).
% 198.09/198.37  cnf(c83072,plain,~leq(X4588,loopcounter)|leq(X4588,n0),inference(resolution,[status(thm)],[c82960, c464])).
% 198.09/198.37  cnf(c148278,plain,leq(succ(n0),n0),inference(resolution,[status(thm)],[c83072, c56613])).
% 198.09/198.37  cnf(c148650,plain,gt(n0,n0),inference(resolution,[status(thm)],[c148278, c126])).
% 198.09/198.37  cnf(c148736,plain,$false,inference(resolution,[status(thm)],[c148650, c469])).
% 198.09/198.37  % SZS output end CNFRefutation
% 198.09/198.37  
% 198.09/198.37  % Initial clauses    : 330
% 198.09/198.37  % Processed clauses  : 3090
% 198.09/198.37  % Factors computed   : 691
% 198.09/198.37  % Resolvents computed: 147578
% 198.09/198.37  % Tautologies deleted: 5
% 198.09/198.37  % Forward subsumed   : 2794
% 198.09/198.37  % Backward subsumed  : 6
% 198.09/198.37  % -------- CPU Time ---------
% 198.09/198.37  % User time          : 197.428 s
% 198.09/198.37  % System time        : 0.548 s
% 198.09/198.37  % Total time         : 197.975 s
%------------------------------------------------------------------------------