%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SWV195+1 : TPTP v8.1.2. Bugfixed v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n008.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:24 EDT 2024
% Result : Theorem 113.81s 114.00s
% Output : Refutation 113.81s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.13 % Problem : SWV195+1 : TPTP v8.1.2. Bugfixed v3.3.0.
% 0.07/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.35 % Computer : n008.cluster.edu
% 0.13/0.35 % Model : x86_64 x86_64
% 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.35 % Memory : 8042.1875MB
% 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.35 % CPULimit : 300
% 0.13/0.35 % WCLimit : 300
% 0.13/0.35 % DateTime : Thu May 9 05:49:08 EDT 2024
% 0.13/0.35 % CPUTime :
% 113.81/114.00 % Version: 1.5
% 113.81/114.00 % SZS status Theorem
% 113.81/114.00 % SZS output start CNFRefutation
% 113.81/114.00 fof(irreflexivity_gt,axiom,(![X]:(~gt(X,X))),file('/export/starexec/sandbox2/benchmark/Axioms/SWV003+0.ax', irreflexivity_gt)).
% 113.81/114.00 fof(c497,plain,(![X]:~gt(X,X)),inference(fof_simplification,[status(thm)],[irreflexivity_gt])).
% 113.81/114.00 fof(c498,plain,(![X180]:~gt(X180,X180)),inference(variable_rename,[status(thm)],[c497])).
% 113.81/114.00 cnf(c499,plain,~gt(X188,X188),inference(split_conjunct,[status(thm)],[c498])).
% 113.81/114.00 fof(quaternion_ds1_inuse_0006,conjecture,(((((((((((((((((((((((((((((((((a_select2(rho_defuse,n0)=use&a_select2(rho_defuse,n1)=use)&a_select2(rho_defuse,n2)=use)&a_select2(sigma_defuse,n0)=use)&a_select2(sigma_defuse,n1)=use)&a_select2(sigma_defuse,n2)=use)&a_select2(sigma_defuse,n3)=use)&a_select2(sigma_defuse,n4)=use)&a_select2(sigma_defuse,n5)=use)&a_select3(u_defuse,n0,n0)=use)&a_select3(u_defuse,n1,n0)=use)&a_select3(u_defuse,n2,n0)=use)&a_select2(xinit_defuse,n3)=use)&a_select2(xinit_defuse,n4)=use)&a_select2(xinit_defuse,n5)=use)&a_select2(xinit_mean_defuse,n0)=use)&a_select2(xinit_mean_defuse,n1)=use)&a_select2(xinit_mean_defuse,n2)=use)&a_select2(xinit_mean_defuse,n3)=use)&a_select2(xinit_mean_defuse,n4)=use)&a_select2(xinit_mean_defuse,n5)=use)&a_select2(xinit_noise_defuse,n0)=use)&a_select2(xinit_noise_defuse,n1)=use)&a_select2(xinit_noise_defuse,n2)=use)&a_select2(xinit_noise_defuse,n3)=use)&a_select2(xinit_noise_defuse,n4)=use)&a_select2(xinit_noise_defuse,n5)=use)&leq(n0,pv5))&leq(pv5,n0))&leq(pv5,n998))>(pv5,n0))&(![A]:(![B]:((((leq(n0,A)&leq(n0,B))&leq(A,n2))&leq(B,pred(pv5)))=>a_select3(u_defuse,A,B)=use))))&(![C]:(![D]:((((leq(n0,C)&leq(n0,D))&leq(C,n2))&leq(D,pred(pv5)))=>a_select3(z_defuse,C,D)=use))))=>(![E]:(![F]:((((leq(n0,E)&leq(n0,F))&leq(E,n2))&leq(F,pv5))=>((((~(n0=E&pv5=F))&(~(n1=E&pv5=F)))&(~(n2=E&pv5=F)))=>a_select3(u_defuse,E,F)=use))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', quaternion_ds1_inuse_0006)).
% 113.81/114.00 fof(c73,negated_conjecture,(~(((((((((((((((((((((((((((((((((a_select2(rho_defuse,n0)=use&a_select2(rho_defuse,n1)=use)&a_select2(rho_defuse,n2)=use)&a_select2(sigma_defuse,n0)=use)&a_select2(sigma_defuse,n1)=use)&a_select2(sigma_defuse,n2)=use)&a_select2(sigma_defuse,n3)=use)&a_select2(sigma_defuse,n4)=use)&a_select2(sigma_defuse,n5)=use)&a_select3(u_defuse,n0,n0)=use)&a_select3(u_defuse,n1,n0)=use)&a_select3(u_defuse,n2,n0)=use)&a_select2(xinit_defuse,n3)=use)&a_select2(xinit_defuse,n4)=use)&a_select2(xinit_defuse,n5)=use)&a_select2(xinit_mean_defuse,n0)=use)&a_select2(xinit_mean_defuse,n1)=use)&a_select2(xinit_mean_defuse,n2)=use)&a_select2(xinit_mean_defuse,n3)=use)&a_select2(xinit_mean_defuse,n4)=use)&a_select2(xinit_mean_defuse,n5)=use)&a_select2(xinit_noise_defuse,n0)=use)&a_select2(xinit_noise_defuse,n1)=use)&a_select2(xinit_noise_defuse,n2)=use)&a_select2(xinit_noise_defuse,n3)=use)&a_select2(xinit_noise_defuse,n4)=use)&a_select2(xinit_noise_defuse,n5)=use)&leq(n0,pv5))&leq(pv5,n0))&leq(pv5,n998))>(pv5,n0))&(![A]:(![B]:((((leq(n0,A)&leq(n0,B))&leq(A,n2))&leq(B,pred(pv5)))=>a_select3(u_defuse,A,B)=use))))&(![C]:(![D]:((((leq(n0,C)&leq(n0,D))&leq(C,n2))&leq(D,pred(pv5)))=>a_select3(z_defuse,C,D)=use))))=>(![E]:(![F]:((((leq(n0,E)&leq(n0,F))&leq(E,n2))&leq(F,pv5))=>((((~(n0=E&pv5=F))&(~(n1=E&pv5=F)))&(~(n2=E&pv5=F)))=>a_select3(u_defuse,E,F)=use)))))),inference(assume_negation,[status(cth)],[quaternion_ds1_inuse_0006])).
% 113.81/114.00 fof(c74,negated_conjecture,(((((((((((((((((((((((((((((((((a_select2(rho_defuse,n0)=use&a_select2(rho_defuse,n1)=use)&a_select2(rho_defuse,n2)=use)&a_select2(sigma_defuse,n0)=use)&a_select2(sigma_defuse,n1)=use)&a_select2(sigma_defuse,n2)=use)&a_select2(sigma_defuse,n3)=use)&a_select2(sigma_defuse,n4)=use)&a_select2(sigma_defuse,n5)=use)&a_select3(u_defuse,n0,n0)=use)&a_select3(u_defuse,n1,n0)=use)&a_select3(u_defuse,n2,n0)=use)&a_select2(xinit_defuse,n3)=use)&a_select2(xinit_defuse,n4)=use)&a_select2(xinit_defuse,n5)=use)&a_select2(xinit_mean_defuse,n0)=use)&a_select2(xinit_mean_defuse,n1)=use)&a_select2(xinit_mean_defuse,n2)=use)&a_select2(xinit_mean_defuse,n3)=use)&a_select2(xinit_mean_defuse,n4)=use)&a_select2(xinit_mean_defuse,n5)=use)&a_select2(xinit_noise_defuse,n0)=use)&a_select2(xinit_noise_defuse,n1)=use)&a_select2(xinit_noise_defuse,n2)=use)&a_select2(xinit_noise_defuse,n3)=use)&a_select2(xinit_noise_defuse,n4)=use)&a_select2(xinit_noise_defuse,n5)=use)&leq(n0,pv5))&leq(pv5,n0))&leq(pv5,n998))>(pv5,n0))&(![A]:(![B]:((((~leq(n0,A)|~leq(n0,B))|~leq(A,n2))|~leq(B,pred(pv5)))|a_select3(u_defuse,A,B)=use))))&(![C]:(![D]:((((~leq(n0,C)|~leq(n0,D))|~leq(C,n2))|~leq(D,pred(pv5)))|a_select3(z_defuse,C,D)=use))))&(?[E]:(?[F]:((((leq(n0,E)&leq(n0,F))&leq(E,n2))&leq(F,pv5))&((((n0!=E|pv5!=F)&(n1!=E|pv5!=F))&(n2!=E|pv5!=F))&a_select3(u_defuse,E,F)!=use))))),inference(fof_nnf,[status(thm)],[c73])).
% 113.81/114.00 fof(c75,negated_conjecture,(((((((((((((((((((((((((((((((((a_select2(rho_defuse,n0)=use&a_select2(rho_defuse,n1)=use)&a_select2(rho_defuse,n2)=use)&a_select2(sigma_defuse,n0)=use)&a_select2(sigma_defuse,n1)=use)&a_select2(sigma_defuse,n2)=use)&a_select2(sigma_defuse,n3)=use)&a_select2(sigma_defuse,n4)=use)&a_select2(sigma_defuse,n5)=use)&a_select3(u_defuse,n0,n0)=use)&a_select3(u_defuse,n1,n0)=use)&a_select3(u_defuse,n2,n0)=use)&a_select2(xinit_defuse,n3)=use)&a_select2(xinit_defuse,n4)=use)&a_select2(xinit_defuse,n5)=use)&a_select2(xinit_mean_defuse,n0)=use)&a_select2(xinit_mean_defuse,n1)=use)&a_select2(xinit_mean_defuse,n2)=use)&a_select2(xinit_mean_defuse,n3)=use)&a_select2(xinit_mean_defuse,n4)=use)&a_select2(xinit_mean_defuse,n5)=use)&a_select2(xinit_noise_defuse,n0)=use)&a_select2(xinit_noise_defuse,n1)=use)&a_select2(xinit_noise_defuse,n2)=use)&a_select2(xinit_noise_defuse,n3)=use)&a_select2(xinit_noise_defuse,n4)=use)&a_select2(xinit_noise_defuse,n5)=use)&leq(n0,pv5))&leq(pv5,n0))&leq(pv5,n998))>(pv5,n0))&(![X8]:(![X9]:((((~leq(n0,X8)|~leq(n0,X9))|~leq(X8,n2))|~leq(X9,pred(pv5)))|a_select3(u_defuse,X8,X9)=use))))&(![X10]:(![X11]:((((~leq(n0,X10)|~leq(n0,X11))|~leq(X10,n2))|~leq(X11,pred(pv5)))|a_select3(z_defuse,X10,X11)=use))))&(?[X12]:(?[X13]:((((leq(n0,X12)&leq(n0,X13))&leq(X12,n2))&leq(X13,pv5))&((((n0!=X12|pv5!=X13)&(n1!=X12|pv5!=X13))&(n2!=X12|pv5!=X13))&a_select3(u_defuse,X12,X13)!=use))))),inference(variable_rename,[status(thm)],[c74])).
% 113.81/114.00 fof(c77,negated_conjecture,(![X8]:(![X9]:(![X10]:(![X11]:(((((((((((((((((((((((((((((((((a_select2(rho_defuse,n0)=use&a_select2(rho_defuse,n1)=use)&a_select2(rho_defuse,n2)=use)&a_select2(sigma_defuse,n0)=use)&a_select2(sigma_defuse,n1)=use)&a_select2(sigma_defuse,n2)=use)&a_select2(sigma_defuse,n3)=use)&a_select2(sigma_defuse,n4)=use)&a_select2(sigma_defuse,n5)=use)&a_select3(u_defuse,n0,n0)=use)&a_select3(u_defuse,n1,n0)=use)&a_select3(u_defuse,n2,n0)=use)&a_select2(xinit_defuse,n3)=use)&a_select2(xinit_defuse,n4)=use)&a_select2(xinit_defuse,n5)=use)&a_select2(xinit_mean_defuse,n0)=use)&a_select2(xinit_mean_defuse,n1)=use)&a_select2(xinit_mean_defuse,n2)=use)&a_select2(xinit_mean_defuse,n3)=use)&a_select2(xinit_mean_defuse,n4)=use)&a_select2(xinit_mean_defuse,n5)=use)&a_select2(xinit_noise_defuse,n0)=use)&a_select2(xinit_noise_defuse,n1)=use)&a_select2(xinit_noise_defuse,n2)=use)&a_select2(xinit_noise_defuse,n3)=use)&a_select2(xinit_noise_defuse,n4)=use)&a_select2(xinit_noise_defuse,n5)=use)&leq(n0,pv5))&leq(pv5,n0))&leq(pv5,n998))>(pv5,n0))&((((~leq(n0,X8)|~leq(n0,X9))|~leq(X8,n2))|~leq(X9,pred(pv5)))|a_select3(u_defuse,X8,X9)=use))&((((~leq(n0,X10)|~leq(n0,X11))|~leq(X10,n2))|~leq(X11,pred(pv5)))|a_select3(z_defuse,X10,X11)=use))&((((leq(n0,skolem0001)&leq(n0,skolem0002))&leq(skolem0001,n2))&leq(skolem0002,pv5))&((((n0!=skolem0001|pv5!=skolem0002)&(n1!=skolem0001|pv5!=skolem0002))&(n2!=skolem0001|pv5!=skolem0002))&a_select3(u_defuse,skolem0001,skolem0002)!=use))))))),inference(shift_quantors,[status(thm)],[fof(c76,negated_conjecture,(((((((((((((((((((((((((((((((((a_select2(rho_defuse,n0)=use&a_select2(rho_defuse,n1)=use)&a_select2(rho_defuse,n2)=use)&a_select2(sigma_defuse,n0)=use)&a_select2(sigma_defuse,n1)=use)&a_select2(sigma_defuse,n2)=use)&a_select2(sigma_defuse,n3)=use)&a_select2(sigma_defuse,n4)=use)&a_select2(sigma_defuse,n5)=use)&a_select3(u_defuse,n0,n0)=use)&a_select3(u_defuse,n1,n0)=use)&a_select3(u_defuse,n2,n0)=use)&a_select2(xinit_defuse,n3)=use)&a_select2(xinit_defuse,n4)=use)&a_select2(xinit_defuse,n5)=use)&a_select2(xinit_mean_defuse,n0)=use)&a_select2(xinit_mean_defuse,n1)=use)&a_select2(xinit_mean_defuse,n2)=use)&a_select2(xinit_mean_defuse,n3)=use)&a_select2(xinit_mean_defuse,n4)=use)&a_select2(xinit_mean_defuse,n5)=use)&a_select2(xinit_noise_defuse,n0)=use)&a_select2(xinit_noise_defuse,n1)=use)&a_select2(xinit_noise_defuse,n2)=use)&a_select2(xinit_noise_defuse,n3)=use)&a_select2(xinit_noise_defuse,n4)=use)&a_select2(xinit_noise_defuse,n5)=use)&leq(n0,pv5))&leq(pv5,n0))&leq(pv5,n998))>(pv5,n0))&(![X8]:(![X9]:((((~leq(n0,X8)|~leq(n0,X9))|~leq(X8,n2))|~leq(X9,pred(pv5)))|a_select3(u_defuse,X8,X9)=use))))&(![X10]:(![X11]:((((~leq(n0,X10)|~leq(n0,X11))|~leq(X10,n2))|~leq(X11,pred(pv5)))|a_select3(z_defuse,X10,X11)=use))))&((((leq(n0,skolem0001)&leq(n0,skolem0002))&leq(skolem0001,n2))&leq(skolem0002,pv5))&((((n0!=skolem0001|pv5!=skolem0002)&(n1!=skolem0001|pv5!=skolem0002))&(n2!=skolem0001|pv5!=skolem0002))&a_select3(u_defuse,skolem0001,skolem0002)!=use))),inference(skolemize,[status(esa)],[c75])).])).
% 113.81/114.00 cnf(c105,negated_conjecture,leq(n0,pv5),inference(split_conjunct,[status(thm)],[c77])).
% 113.81/114.00 cnf(c106,negated_conjecture,leq(pv5,n0),inference(split_conjunct,[status(thm)],[c77])).
% 113.81/114.00 fof(finite_domain_0,axiom,(![X]:((leq(n0,X)&leq(X,n0))=>X=n0)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', finite_domain_0)).
% 113.81/114.00 fof(c36,plain,(![X]:((~leq(n0,X)|~leq(X,n0))|X=n0)),inference(fof_nnf,[status(thm)],[finite_domain_0])).
% 113.81/114.00 fof(c37,plain,(![X5]:((~leq(n0,X5)|~leq(X5,n0))|X5=n0)),inference(variable_rename,[status(thm)],[c36])).
% 113.81/114.00 cnf(c38,plain,~leq(n0,X308)|~leq(X308,n0)|X308=n0,inference(split_conjunct,[status(thm)],[c37])).
% 113.81/114.00 cnf(c968,plain,~leq(n0,pv5)|pv5=n0,inference(resolution,[status(thm)],[c38, c106])).
% 113.81/114.00 cnf(c83597,plain,pv5=n0,inference(resolution,[status(thm)],[c968, c105])).
% 113.81/114.00 cnf(reflexivity,axiom,X186=X186,theory(equality)).
% 113.81/114.00 cnf(c108,negated_conjecture,gt(pv5,n0),inference(split_conjunct,[status(thm)],[c77])).
% 113.81/114.00 cnf(c18,axiom,X286!=X285|X283!=X284|~gt(X286,X283)|gt(X285,X284),theory(equality)).
% 113.81/114.00 cnf(c739,plain,pv5!=X2705|n0!=X2704|gt(X2705,X2704),inference(resolution,[status(thm)],[c18, c108])).
% 113.81/114.00 cnf(c58175,plain,pv5!=X3627|gt(X3627,n0),inference(resolution,[status(thm)],[c739, reflexivity])).
% 113.81/114.00 cnf(c110293,plain,gt(n0,n0),inference(resolution,[status(thm)],[c58175, c83597])).
% 113.81/114.00 cnf(c110298,plain,$false,inference(resolution,[status(thm)],[c110293, c499])).
% 113.81/114.00 % SZS output end CNFRefutation
% 113.81/114.00
% 113.81/114.00 % Initial clauses : 360
% 113.81/114.00 % Processed clauses : 2283
% 113.81/114.00 % Factors computed : 499
% 113.81/114.00 % Resolvents computed: 109528
% 113.81/114.00 % Tautologies deleted: 5
% 113.81/114.00 % Forward subsumed : 2044
% 113.81/114.00 % Backward subsumed : 4
% 113.81/114.00 % -------- CPU Time ---------
% 113.81/114.00 % User time : 113.225 s
% 113.81/114.00 % System time : 0.411 s
% 113.81/114.00 % Total time : 113.636 s
%------------------------------------------------------------------------------