%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SWV163+1 : TPTP v8.1.2. Bugfixed v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n007.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:21 EDT 2024
% Result : Theorem 53.27s 53.53s
% Output : Refutation 53.27s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.13 % Problem : SWV163+1 : TPTP v8.1.2. Bugfixed v3.3.0.
% 0.07/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.15/0.36 % Computer : n007.cluster.edu
% 0.15/0.36 % Model : x86_64 x86_64
% 0.15/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.36 % Memory : 8042.1875MB
% 0.15/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.36 % CPULimit : 300
% 0.15/0.36 % WCLimit : 300
% 0.15/0.36 % DateTime : Thu May 9 05:12:53 EDT 2024
% 0.15/0.36 % CPUTime :
% 53.27/53.53 % Version: 1.5
% 53.27/53.53 % SZS status Theorem
% 53.27/53.53 % SZS output start CNFRefutation
% 53.27/53.53 fof(irreflexivity_gt,axiom,(![X]:(~gt(X,X))),file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax', irreflexivity_gt)).
% 53.27/53.53 fof(c465,plain,(![X]:~gt(X,X)),inference(fof_simplification,[status(thm)],[irreflexivity_gt])).
% 53.27/53.53 fof(c466,plain,(![X176]:~gt(X176,X176)),inference(variable_rename,[status(thm)],[c465])).
% 53.27/53.53 cnf(c467,plain,~gt(X184,X184),inference(split_conjunct,[status(thm)],[c466])).
% 53.27/53.53 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)).
% 53.27/53.53 fof(c122,plain,(![X]:(![Y]:(~leq(succ(X),Y)|gt(Y,X)))),inference(fof_nnf,[status(thm)],[leq_succ_gt])).
% 53.27/53.53 fof(c123,plain,(![X44]:(![X45]:(~leq(succ(X44),X45)|gt(X45,X44)))),inference(variable_rename,[status(thm)],[c122])).
% 53.27/53.53 cnf(c124,plain,~leq(succ(X350),X349)|gt(X349,X350),inference(split_conjunct,[status(thm)],[c123])).
% 53.27/53.53 fof(cl5_nebula_norm_0013,conjecture,(((leq(n0,pv10)&leq(pv10,n135299))&(![A]:((leq(n0,A)&leq(A,pred(pv10)))=>sum(n0,n4,a_select3(q,A,tptp_sum_index))=n1)))=>(![B]:((leq(n0,B)&leq(B,tptp_minus_1))=>a_select3(q,pv10,B)=divide(sqrt(times(minus(a_select3(center,B,n0),a_select2(x,pv10)),minus(a_select3(center,B,n0),a_select2(x,pv10)))),sum(n0,n4,sqrt(times(minus(a_select3(center,tptp_sum_index,n0),a_select2(x,pv10)),minus(a_select3(center,tptp_sum_index,n0),a_select2(x,pv10))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', cl5_nebula_norm_0013)).
% 53.27/53.53 fof(c76,negated_conjecture,(~(((leq(n0,pv10)&leq(pv10,n135299))&(![A]:((leq(n0,A)&leq(A,pred(pv10)))=>sum(n0,n4,a_select3(q,A,tptp_sum_index))=n1)))=>(![B]:((leq(n0,B)&leq(B,tptp_minus_1))=>a_select3(q,pv10,B)=divide(sqrt(times(minus(a_select3(center,B,n0),a_select2(x,pv10)),minus(a_select3(center,B,n0),a_select2(x,pv10)))),sum(n0,n4,sqrt(times(minus(a_select3(center,tptp_sum_index,n0),a_select2(x,pv10)),minus(a_select3(center,tptp_sum_index,n0),a_select2(x,pv10)))))))))),inference(assume_negation,[status(cth)],[cl5_nebula_norm_0013])).
% 53.27/53.53 fof(c77,negated_conjecture,(((leq(n0,pv10)&leq(pv10,n135299))&(![A]:((~leq(n0,A)|~leq(A,pred(pv10)))|sum(n0,n4,a_select3(q,A,tptp_sum_index))=n1)))&(?[B]:((leq(n0,B)&leq(B,tptp_minus_1))&a_select3(q,pv10,B)!=divide(sqrt(times(minus(a_select3(center,B,n0),a_select2(x,pv10)),minus(a_select3(center,B,n0),a_select2(x,pv10)))),sum(n0,n4,sqrt(times(minus(a_select3(center,tptp_sum_index,n0),a_select2(x,pv10)),minus(a_select3(center,tptp_sum_index,n0),a_select2(x,pv10))))))))),inference(fof_nnf,[status(thm)],[c76])).
% 53.27/53.53 fof(c78,negated_conjecture,(((leq(n0,pv10)&leq(pv10,n135299))&(![X8]:((~leq(n0,X8)|~leq(X8,pred(pv10)))|sum(n0,n4,a_select3(q,X8,tptp_sum_index))=n1)))&(?[X9]:((leq(n0,X9)&leq(X9,tptp_minus_1))&a_select3(q,pv10,X9)!=divide(sqrt(times(minus(a_select3(center,X9,n0),a_select2(x,pv10)),minus(a_select3(center,X9,n0),a_select2(x,pv10)))),sum(n0,n4,sqrt(times(minus(a_select3(center,tptp_sum_index,n0),a_select2(x,pv10)),minus(a_select3(center,tptp_sum_index,n0),a_select2(x,pv10))))))))),inference(variable_rename,[status(thm)],[c77])).
% 53.27/53.53 fof(c80,negated_conjecture,(![X8]:(((leq(n0,pv10)&leq(pv10,n135299))&((~leq(n0,X8)|~leq(X8,pred(pv10)))|sum(n0,n4,a_select3(q,X8,tptp_sum_index))=n1))&((leq(n0,skolem0001)&leq(skolem0001,tptp_minus_1))&a_select3(q,pv10,skolem0001)!=divide(sqrt(times(minus(a_select3(center,skolem0001,n0),a_select2(x,pv10)),minus(a_select3(center,skolem0001,n0),a_select2(x,pv10)))),sum(n0,n4,sqrt(times(minus(a_select3(center,tptp_sum_index,n0),a_select2(x,pv10)),minus(a_select3(center,tptp_sum_index,n0),a_select2(x,pv10))))))))),inference(shift_quantors,[status(thm)],[fof(c79,negated_conjecture,(((leq(n0,pv10)&leq(pv10,n135299))&(![X8]:((~leq(n0,X8)|~leq(X8,pred(pv10)))|sum(n0,n4,a_select3(q,X8,tptp_sum_index))=n1)))&((leq(n0,skolem0001)&leq(skolem0001,tptp_minus_1))&a_select3(q,pv10,skolem0001)!=divide(sqrt(times(minus(a_select3(center,skolem0001,n0),a_select2(x,pv10)),minus(a_select3(center,skolem0001,n0),a_select2(x,pv10)))),sum(n0,n4,sqrt(times(minus(a_select3(center,tptp_sum_index,n0),a_select2(x,pv10)),minus(a_select3(center,tptp_sum_index,n0),a_select2(x,pv10)))))))),inference(skolemize,[status(esa)],[c78])).])).
% 53.27/53.53 cnf(c85,negated_conjecture,leq(skolem0001,tptp_minus_1),inference(split_conjunct,[status(thm)],[c80])).
% 53.27/53.53 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)).
% 53.27/53.53 fof(c460,plain,(![X]:(![Y]:(![Z]:((~leq(X,Y)|~leq(Y,Z))|leq(X,Z))))),inference(fof_nnf,[status(thm)],[transitivity_leq])).
% 53.27/53.53 fof(c461,plain,(![X172]:(![X173]:(![X174]:((~leq(X172,X173)|~leq(X173,X174))|leq(X172,X174))))),inference(variable_rename,[status(thm)],[c460])).
% 53.27/53.53 cnf(c462,plain,~leq(X2185,X2187)|~leq(X2187,X2186)|leq(X2185,X2186),inference(split_conjunct,[status(thm)],[c461])).
% 53.27/53.53 cnf(c34956,plain,~leq(X2409,skolem0001)|leq(X2409,tptp_minus_1),inference(resolution,[status(thm)],[c462, c85])).
% 53.27/53.53 cnf(symmetry,axiom,X185!=X186|X186=X185,theory(equality)).
% 53.27/53.53 fof(succ_tptp_minus_1,axiom,succ(tptp_minus_1)=n0,file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax', succ_tptp_minus_1)).
% 53.27/53.53 cnf(c157,plain,succ(tptp_minus_1)=n0,inference(split_conjunct,[status(thm)],[succ_tptp_minus_1])).
% 53.27/53.53 cnf(c512,plain,n0=succ(tptp_minus_1),inference(resolution,[status(thm)],[c157, symmetry])).
% 53.27/53.53 cnf(reflexivity,axiom,X182=X182,theory(equality)).
% 53.27/53.53 fof(reflexivity_leq,axiom,(![X]:leq(X,X)),file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax', reflexivity_leq)).
% 53.27/53.53 fof(c463,plain,(![X175]:leq(X175,X175)),inference(variable_rename,[status(thm)],[reflexivity_leq])).
% 53.27/53.53 cnf(c464,plain,leq(X183,X183),inference(split_conjunct,[status(thm)],[c463])).
% 53.27/53.53 cnf(c22,axiom,X295!=X298|X297!=X296|~leq(X295,X297)|leq(X298,X296),theory(equality)).
% 53.27/53.53 cnf(c753,plain,X2926!=X2925|X2926!=X2927|leq(X2925,X2927),inference(resolution,[status(thm)],[c22, c464])).
% 53.27/53.53 cnf(c56662,plain,X2930!=X2931|leq(X2931,X2930),inference(resolution,[status(thm)],[c753, reflexivity])).
% 53.27/53.53 cnf(c56741,plain,leq(succ(tptp_minus_1),n0),inference(resolution,[status(thm)],[c56662, c512])).
% 53.27/53.53 cnf(c84,negated_conjecture,leq(n0,skolem0001),inference(split_conjunct,[status(thm)],[c80])).
% 53.27/53.53 cnf(c35154,plain,~leq(X3042,n0)|leq(X3042,skolem0001),inference(resolution,[status(thm)],[c462, c84])).
% 53.27/53.53 cnf(c59640,plain,leq(succ(tptp_minus_1),skolem0001),inference(resolution,[status(thm)],[c35154, c56741])).
% 53.27/53.53 cnf(c59882,plain,leq(succ(tptp_minus_1),tptp_minus_1),inference(resolution,[status(thm)],[c59640, c34956])).
% 53.27/53.53 cnf(c60472,plain,gt(tptp_minus_1,tptp_minus_1),inference(resolution,[status(thm)],[c59882, c124])).
% 53.27/53.53 cnf(c60492,plain,$false,inference(resolution,[status(thm)],[c60472, c467])).
% 53.27/53.53 % SZS output end CNFRefutation
% 53.27/53.53
% 53.27/53.53 % Initial clauses : 328
% 53.27/53.53 % Processed clauses : 1587
% 53.27/53.53 % Factors computed : 448
% 53.27/53.53 % Resolvents computed: 59625
% 53.27/53.53 % Tautologies deleted: 5
% 53.27/53.53 % Forward subsumed : 1306
% 53.27/53.53 % Backward subsumed : 0
% 53.27/53.53 % -------- CPU Time ---------
% 53.27/53.53 % User time : 52.889 s
% 53.27/53.53 % System time : 0.240 s
% 53.27/53.53 % Total time : 53.129 s
%------------------------------------------------------------------------------