%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SWV194+1 : TPTP v8.1.2. Bugfixed v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n032.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 121.26s 121.51s
% Output : Refutation 121.26s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.11 % Problem : SWV194+1 : TPTP v8.1.2. Bugfixed v3.3.0.
% 0.03/0.12 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.11/0.31 % Computer : n032.cluster.edu
% 0.11/0.31 % Model : x86_64 x86_64
% 0.11/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.31 % Memory : 8042.1875MB
% 0.11/0.31 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.31 % CPULimit : 300
% 0.11/0.31 % WCLimit : 300
% 0.11/0.31 % DateTime : Thu May 9 06:09:07 EDT 2024
% 0.11/0.31 % CPUTime :
% 121.26/121.51 % Version: 1.5
% 121.26/121.51 % SZS status Theorem
% 121.26/121.51 % SZS output start CNFRefutation
% 121.26/121.51 fof(irreflexivity_gt,axiom,(![X]:(~gt(X,X))),file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax', irreflexivity_gt)).
% 121.26/121.51 fof(c494,plain,(![X]:~gt(X,X)),inference(fof_simplification,[status(thm)],[irreflexivity_gt])).
% 121.26/121.51 fof(c495,plain,(![X180]:~gt(X180,X180)),inference(variable_rename,[status(thm)],[c494])).
% 121.26/121.51 cnf(c496,plain,~gt(X188,X188),inference(split_conjunct,[status(thm)],[c495])).
% 121.26/121.51 fof(quaternion_ds1_inuse_0005,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))=>a_select3(u_defuse,E,F)=use)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', quaternion_ds1_inuse_0005)).
% 121.26/121.51 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))=>a_select3(u_defuse,E,F)=use))))),inference(assume_negation,[status(cth)],[quaternion_ds1_inuse_0005])).
% 121.26/121.51 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))&a_select3(u_defuse,E,F)!=use)))),inference(fof_nnf,[status(thm)],[c73])).
% 121.26/121.51 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))&a_select3(u_defuse,X12,X13)!=use)))),inference(variable_rename,[status(thm)],[c74])).
% 121.26/121.51 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))&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))&a_select3(u_defuse,skolem0001,skolem0002)!=use)),inference(skolemize,[status(esa)],[c75])).])).
% 121.26/121.51 cnf(c105,negated_conjecture,leq(n0,pv5),inference(split_conjunct,[status(thm)],[c77])).
% 121.26/121.51 cnf(c106,negated_conjecture,leq(pv5,n0),inference(split_conjunct,[status(thm)],[c77])).
% 121.26/121.51 fof(finite_domain_0,axiom,(![X]:((leq(n0,X)&leq(X,n0))=>X=n0)),file('/export/starexec/sandbox/benchmark/theBenchmark.p', finite_domain_0)).
% 121.26/121.51 fof(c36,plain,(![X]:((~leq(n0,X)|~leq(X,n0))|X=n0)),inference(fof_nnf,[status(thm)],[finite_domain_0])).
% 121.26/121.51 fof(c37,plain,(![X5]:((~leq(n0,X5)|~leq(X5,n0))|X5=n0)),inference(variable_rename,[status(thm)],[c36])).
% 121.26/121.51 cnf(c38,plain,~leq(n0,X308)|~leq(X308,n0)|X308=n0,inference(split_conjunct,[status(thm)],[c37])).
% 121.26/121.51 cnf(c964,plain,~leq(n0,pv5)|pv5=n0,inference(resolution,[status(thm)],[c38, c106])).
% 121.26/121.51 cnf(c83613,plain,pv5=n0,inference(resolution,[status(thm)],[c964, c105])).
% 121.26/121.51 cnf(reflexivity,axiom,X186=X186,theory(equality)).
% 121.26/121.51 cnf(c108,negated_conjecture,gt(pv5,n0),inference(split_conjunct,[status(thm)],[c77])).
% 121.26/121.51 cnf(c18,axiom,X287!=X284|X285!=X286|~gt(X287,X285)|gt(X284,X286),theory(equality)).
% 121.26/121.51 cnf(c731,plain,pv5!=X2688|n0!=X2687|gt(X2688,X2687),inference(resolution,[status(thm)],[c18, c108])).
% 121.26/121.51 cnf(c60218,plain,pv5!=X3672|gt(X3672,n0),inference(resolution,[status(thm)],[c731, reflexivity])).
% 121.26/121.51 cnf(c115017,plain,gt(n0,n0),inference(resolution,[status(thm)],[c60218, c83613])).
% 121.26/121.51 cnf(c115019,plain,$false,inference(resolution,[status(thm)],[c115017, c496])).
% 121.26/121.51 % SZS output end CNFRefutation
% 121.26/121.51
% 121.26/121.51 % Initial clauses : 357
% 121.26/121.51 % Processed clauses : 2320
% 121.26/121.51 % Factors computed : 504
% 121.26/121.51 % Resolvents computed: 114021
% 121.26/121.51 % Tautologies deleted: 5
% 121.26/121.51 % Forward subsumed : 2101
% 121.26/121.51 % Backward subsumed : 4
% 121.26/121.51 % -------- CPU Time ---------
% 121.26/121.51 % User time : 120.813 s
% 121.26/121.51 % System time : 0.333 s
% 121.26/121.51 % Total time : 121.146 s
%------------------------------------------------------------------------------