%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SWV189+1 : TPTP v8.1.2. Bugfixed v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n021.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 41.86s 42.06s
% Output : Refutation 41.86s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12 % Problem : SWV189+1 : TPTP v8.1.2. Bugfixed v3.3.0.
% 0.06/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.34 % Computer : n021.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Thu May 9 06:09:38 EDT 2024
% 0.13/0.34 % CPUTime :
% 41.86/42.06 % Version: 1.5
% 41.86/42.06 % SZS status Theorem
% 41.86/42.06 % SZS output start CNFRefutation
% 41.86/42.06 fof(irreflexivity_gt,axiom,(![X]:(~gt(X,X))),file('/export/starexec/sandbox2/benchmark/Axioms/SWV003+0.ax', irreflexivity_gt)).
% 41.86/42.06 fof(c455,plain,(![X]:~gt(X,X)),inference(fof_simplification,[status(thm)],[irreflexivity_gt])).
% 41.86/42.06 fof(c456,plain,(![X177]:~gt(X177,X177)),inference(variable_rename,[status(thm)],[c455])).
% 41.86/42.06 cnf(c457,plain,~gt(X185,X185),inference(split_conjunct,[status(thm)],[c456])).
% 41.86/42.06 fof(leq_succ_gt,axiom,(![X]:(![Y]:(leq(succ(X),Y)=>gt(Y,X)))),file('/export/starexec/sandbox2/benchmark/Axioms/SWV003+0.ax', leq_succ_gt)).
% 41.86/42.06 fof(c112,plain,(![X]:(![Y]:(~leq(succ(X),Y)|gt(Y,X)))),inference(fof_nnf,[status(thm)],[leq_succ_gt])).
% 41.86/42.06 fof(c113,plain,(![X45]:(![X46]:(~leq(succ(X45),X46)|gt(X46,X45)))),inference(variable_rename,[status(thm)],[c112])).
% 41.86/42.06 cnf(c114,plain,~leq(succ(X323),X322)|gt(X322,X323),inference(split_conjunct,[status(thm)],[c113])).
% 41.86/42.06 fof(cl5_nebula_init_0121,conjecture,((![A]:((leq(n0,A)&leq(A,n4))=>a_select3(center_init,A,n0)=init))=>(![B]:((leq(n0,B)&leq(B,tptp_minus_1))=>(![C]:((leq(n0,C)&leq(C,n4))=>a_select3(q_init,B,C)=init))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', cl5_nebula_init_0121)).
% 41.86/42.06 fof(c66,negated_conjecture,(~((![A]:((leq(n0,A)&leq(A,n4))=>a_select3(center_init,A,n0)=init))=>(![B]:((leq(n0,B)&leq(B,tptp_minus_1))=>(![C]:((leq(n0,C)&leq(C,n4))=>a_select3(q_init,B,C)=init)))))),inference(assume_negation,[status(cth)],[cl5_nebula_init_0121])).
% 41.86/42.06 fof(c67,negated_conjecture,((![A]:((~leq(n0,A)|~leq(A,n4))|a_select3(center_init,A,n0)=init))&(?[B]:((leq(n0,B)&leq(B,tptp_minus_1))&(?[C]:((leq(n0,C)&leq(C,n4))&a_select3(q_init,B,C)!=init))))),inference(fof_nnf,[status(thm)],[c66])).
% 41.86/42.06 fof(c68,negated_conjecture,((![X8]:((~leq(n0,X8)|~leq(X8,n4))|a_select3(center_init,X8,n0)=init))&(?[X9]:((leq(n0,X9)&leq(X9,tptp_minus_1))&(?[X10]:((leq(n0,X10)&leq(X10,n4))&a_select3(q_init,X9,X10)!=init))))),inference(variable_rename,[status(thm)],[c67])).
% 41.86/42.06 fof(c70,negated_conjecture,(![X8]:(((~leq(n0,X8)|~leq(X8,n4))|a_select3(center_init,X8,n0)=init)&((leq(n0,skolem0001)&leq(skolem0001,tptp_minus_1))&((leq(n0,skolem0002)&leq(skolem0002,n4))&a_select3(q_init,skolem0001,skolem0002)!=init)))),inference(shift_quantors,[status(thm)],[fof(c69,negated_conjecture,((![X8]:((~leq(n0,X8)|~leq(X8,n4))|a_select3(center_init,X8,n0)=init))&((leq(n0,skolem0001)&leq(skolem0001,tptp_minus_1))&((leq(n0,skolem0002)&leq(skolem0002,n4))&a_select3(q_init,skolem0001,skolem0002)!=init))),inference(skolemize,[status(esa)],[c68])).])).
% 41.86/42.06 cnf(c73,negated_conjecture,leq(skolem0001,tptp_minus_1),inference(split_conjunct,[status(thm)],[c70])).
% 41.86/42.06 fof(transitivity_leq,axiom,(![X]:(![Y]:(![Z]:((leq(X,Y)&leq(Y,Z))=>leq(X,Z))))),file('/export/starexec/sandbox2/benchmark/Axioms/SWV003+0.ax', transitivity_leq)).
% 41.86/42.06 fof(c450,plain,(![X]:(![Y]:(![Z]:((~leq(X,Y)|~leq(Y,Z))|leq(X,Z))))),inference(fof_nnf,[status(thm)],[transitivity_leq])).
% 41.86/42.06 fof(c451,plain,(![X173]:(![X174]:(![X175]:((~leq(X173,X174)|~leq(X174,X175))|leq(X173,X175))))),inference(variable_rename,[status(thm)],[c450])).
% 41.86/42.06 cnf(c452,plain,~leq(X2246,X2245)|~leq(X2245,X2244)|leq(X2246,X2244),inference(split_conjunct,[status(thm)],[c451])).
% 41.86/42.06 cnf(c27927,plain,~leq(X2369,skolem0001)|leq(X2369,tptp_minus_1),inference(resolution,[status(thm)],[c452, c73])).
% 41.86/42.06 cnf(c72,negated_conjecture,leq(n0,skolem0001),inference(split_conjunct,[status(thm)],[c70])).
% 41.86/42.06 cnf(c27974,plain,~leq(X2655,n0)|leq(X2655,skolem0001),inference(resolution,[status(thm)],[c452, c72])).
% 41.86/42.06 cnf(symmetry,axiom,X186!=X187|X187=X186,theory(equality)).
% 41.86/42.06 fof(succ_tptp_minus_1,axiom,succ(tptp_minus_1)=n0,file('/export/starexec/sandbox2/benchmark/Axioms/SWV003+0.ax', succ_tptp_minus_1)).
% 41.86/42.06 cnf(c147,plain,succ(tptp_minus_1)=n0,inference(split_conjunct,[status(thm)],[succ_tptp_minus_1])).
% 41.86/42.06 cnf(c496,plain,n0=succ(tptp_minus_1),inference(resolution,[status(thm)],[c147, symmetry])).
% 41.86/42.06 cnf(reflexivity,axiom,X183=X183,theory(equality)).
% 41.86/42.06 fof(reflexivity_leq,axiom,(![X]:leq(X,X)),file('/export/starexec/sandbox2/benchmark/Axioms/SWV003+0.ax', reflexivity_leq)).
% 41.86/42.06 fof(c453,plain,(![X176]:leq(X176,X176)),inference(variable_rename,[status(thm)],[reflexivity_leq])).
% 41.86/42.06 cnf(c454,plain,leq(X184,X184),inference(split_conjunct,[status(thm)],[c453])).
% 41.86/42.06 cnf(c19,axiom,X287!=X289|X288!=X286|~leq(X287,X288)|leq(X289,X286),theory(equality)).
% 41.86/42.06 cnf(c693,plain,X2939!=X2938|X2939!=X2940|leq(X2938,X2940),inference(resolution,[status(thm)],[c19, c454])).
% 41.86/42.06 cnf(c51025,plain,X2944!=X2943|leq(X2943,X2944),inference(resolution,[status(thm)],[c693, reflexivity])).
% 41.86/42.06 cnf(c51080,plain,leq(succ(tptp_minus_1),n0),inference(resolution,[status(thm)],[c51025, c496])).
% 41.86/42.06 cnf(c51294,plain,leq(succ(tptp_minus_1),skolem0001),inference(resolution,[status(thm)],[c51080, c27974])).
% 41.86/42.06 cnf(c52285,plain,leq(succ(tptp_minus_1),tptp_minus_1),inference(resolution,[status(thm)],[c51294, c27927])).
% 41.86/42.06 cnf(c53616,plain,gt(tptp_minus_1,tptp_minus_1),inference(resolution,[status(thm)],[c52285, c114])).
% 41.86/42.06 cnf(c53660,plain,$false,inference(resolution,[status(thm)],[c53616, c457])).
% 41.86/42.06 % SZS output end CNFRefutation
% 41.86/42.06
% 41.86/42.06 % Initial clauses : 318
% 41.86/42.06 % Processed clauses : 1402
% 41.86/42.06 % Factors computed : 445
% 41.86/42.06 % Resolvents computed: 52756
% 41.86/42.06 % Tautologies deleted: 5
% 41.86/42.06 % Forward subsumed : 1128
% 41.86/42.06 % Backward subsumed : 0
% 41.86/42.06 % -------- CPU Time ---------
% 41.86/42.06 % User time : 41.506 s
% 41.86/42.06 % System time : 0.206 s
% 41.86/42.06 % Total time : 41.712 s
%------------------------------------------------------------------------------