%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GEO474+1 : TPTP v9.3.1. Released v7.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n018.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 12:26:32 PM UTC 2026
% Result : Theorem 2.40s 3.02s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GEO474+1 : TPTP v9.3.1. Released v7.0.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.03/0.36 % Computer : n018.cluster.edu
% 0.03/0.36 % Model : x86_64 x86_64
% 0.03/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.03/0.36 % Memory : 8046.5625MB
% 0.03/0.36 % OS : Linux 6.8.0-71-generic
% 0.03/0.36 % CPULimit : 300
% 0.03/0.36 % WCLimit : 300
% 0.03/0.36 % DateTime : Sun Sep 20 16:36:42 UTC 2026
% 0.03/0.36 % CPUTime :
% 2.25/2.56 % Drodi V4.1.1
% 2.40/3.02 % Refutation found
% 2.40/3.02 % SZS status Theorem for theBenchmark: Theorem is valid
% 2.40/3.02 % SZS output start CNFRefutation for theBenchmark
% 2.40/3.02 fof(f200,axiom,(
% 2.40/3.02 (! [N0] : s(num,i(s(fun(num,num),numeral),s(num,N0))) = s(num,N0) )),
% 2.40/3.02 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.40/3.02 fof(f3502,axiom,(
% 2.40/3.02 (! [M,N,A5] :( s(num,i(s(fun(cart(cart(real,M),N),num),rank),s(cart(cart(real,M),N),A5))) = s(num,i(s(fun(num,num),numeral),s(num,u_0)))<=> s(cart(cart(real,M),N),A5) = s(cart(cart(real,M),N),i(s(fun(num,cart(cart(real,M),N)),mat),s(num,i(s(fun(num,num),numeral),s(num,u_0))))) ) )),
% 2.40/3.02 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.40/3.02 fof(f3503,conjecture,(
% 2.40/3.02 (! [Q133117,Q133118] : s(num,i(s(fun(cart(cart(real,Q133117),Q133118),num),rank),s(cart(cart(real,Q133117),Q133118),i(s(fun(num,cart(cart(real,Q133117),Q133118)),mat),s(num,i(s(fun(num,num),numeral),s(num,u_0))))))) = s(num,i(s(fun(num,num),numeral),s(num,u_0))) )),
% 2.40/3.02 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.40/3.02 fof(f3504,negated_conjecture,(
% 2.40/3.02 ~((! [Q133117,Q133118] : s(num,i(s(fun(cart(cart(real,Q133117),Q133118),num),rank),s(cart(cart(real,Q133117),Q133118),i(s(fun(num,cart(cart(real,Q133117),Q133118)),mat),s(num,i(s(fun(num,num),numeral),s(num,u_0))))))) = s(num,i(s(fun(num,num),numeral),s(num,u_0))) ))),
% 2.40/3.02 inference(negated_conjecture,[status(cth)],[f3503])).
% 2.40/3.02 fof(f4521,plain,(
% 2.40/3.02 ![X0]: (s(num,i(s(fun(num,num),numeral),s(num,X0)))=s(num,X0))),
% 2.40/3.02 inference(cnf_transformation,[status(thm)],[f200])).
% 2.40/3.02 fof(f15465,plain,(
% 2.40/3.02 ![M,N,A5]: ((~s(num,i(s(fun(cart(cart(real,M),N),num),rank),s(cart(cart(real,M),N),A5)))=s(num,i(s(fun(num,num),numeral),s(num,u_0)))|s(cart(cart(real,M),N),A5)=s(cart(cart(real,M),N),i(s(fun(num,cart(cart(real,M),N)),mat),s(num,i(s(fun(num,num),numeral),s(num,u_0))))))&(s(num,i(s(fun(cart(cart(real,M),N),num),rank),s(cart(cart(real,M),N),A5)))=s(num,i(s(fun(num,num),numeral),s(num,u_0)))|~s(cart(cart(real,M),N),A5)=s(cart(cart(real,M),N),i(s(fun(num,cart(cart(real,M),N)),mat),s(num,i(s(fun(num,num),numeral),s(num,u_0)))))))),
% 2.40/3.02 inference(NNF_transformation,[status(thm)],[f3502])).
% 2.40/3.02 fof(f15466,plain,(
% 2.40/3.02 (![M,N,A5]: (~s(num,i(s(fun(cart(cart(real,M),N),num),rank),s(cart(cart(real,M),N),A5)))=s(num,i(s(fun(num,num),numeral),s(num,u_0)))|s(cart(cart(real,M),N),A5)=s(cart(cart(real,M),N),i(s(fun(num,cart(cart(real,M),N)),mat),s(num,i(s(fun(num,num),numeral),s(num,u_0)))))))&(![M,N,A5]: (s(num,i(s(fun(cart(cart(real,M),N),num),rank),s(cart(cart(real,M),N),A5)))=s(num,i(s(fun(num,num),numeral),s(num,u_0)))|~s(cart(cart(real,M),N),A5)=s(cart(cart(real,M),N),i(s(fun(num,cart(cart(real,M),N)),mat),s(num,i(s(fun(num,num),numeral),s(num,u_0)))))))),
% 2.40/3.02 inference(miniscoping,[status(thm)],[f15465])).
% 2.40/3.02 fof(f15468,plain,(
% 2.40/3.02 ![X0,X1,X2]: (s(num,i(s(fun(cart(cart(real,X0),X1),num),rank),s(cart(cart(real,X0),X1),X2)))=s(num,i(s(fun(num,num),numeral),s(num,u_0)))|~s(cart(cart(real,X0),X1),X2)=s(cart(cart(real,X0),X1),i(s(fun(num,cart(cart(real,X0),X1)),mat),s(num,i(s(fun(num,num),numeral),s(num,u_0))))))),
% 2.40/3.02 inference(cnf_transformation,[status(thm)],[f15466])).
% 2.40/3.02 fof(f15469,plain,(
% 2.40/3.02 (?[Q133117,Q133118]: ~s(num,i(s(fun(cart(cart(real,Q133117),Q133118),num),rank),s(cart(cart(real,Q133117),Q133118),i(s(fun(num,cart(cart(real,Q133117),Q133118)),mat),s(num,i(s(fun(num,num),numeral),s(num,u_0)))))))=s(num,i(s(fun(num,num),numeral),s(num,u_0))))),
% 2.40/3.02 inference(pre_NNF_transformation,[status(thm)],[f3504])).
% 2.40/3.02 fof(f15470,plain,(
% 2.40/3.02 ~s(num,i(s(fun(cart(cart(real,sK3705_skl),sK3706_skl),num),rank),s(cart(cart(real,sK3705_skl),sK3706_skl),i(s(fun(num,cart(cart(real,sK3705_skl),sK3706_skl)),mat),s(num,i(s(fun(num,num),numeral),s(num,u_0)))))))=s(num,i(s(fun(num,num),numeral),s(num,u_0)))),
% 2.40/3.02 inference(skolemize,[status(esa),new_symbols(skolem,[sK3705_skl,sK3706_skl]),skolemize(Q133117,sK3705_skl),skolemize(Q133118,sK3706_skl)],[f15469])).
% 2.40/3.02 fof(f15471,plain,(
% 2.40/3.02 ~s(num,i(s(fun(cart(cart(real,sK3705_skl),sK3706_skl),num),rank),s(cart(cart(real,sK3705_skl),sK3706_skl),i(s(fun(num,cart(cart(real,sK3705_skl),sK3706_skl)),mat),s(num,i(s(fun(num,num),numeral),s(num,u_0)))))))=s(num,i(s(fun(num,num),numeral),s(num,u_0)))),
% 5.90/3.18 inference(cnf_transformation,[status(thm)],[f15470])).
% 5.90/3.18 fof(f18042,plain,(
% 5.90/3.18 ~s(num,i(s(fun(cart(cart(real,sK3705_skl),sK3706_skl),num),rank),s(cart(cart(real,sK3705_skl),sK3706_skl),i(s(fun(num,cart(cart(real,sK3705_skl),sK3706_skl)),mat),s(num,i(s(fun(num,num),numeral),s(num,u_0)))))))=s(num,u_0)),
% 5.90/3.18 inference(backward_demodulation,[status(thm)],[f4521,f15471])).
% 5.90/3.18 fof(f18048,plain,(
% 5.90/3.18 ~s(num,i(s(fun(cart(cart(real,sK3705_skl),sK3706_skl),num),rank),s(cart(cart(real,sK3705_skl),sK3706_skl),i(s(fun(num,cart(cart(real,sK3705_skl),sK3706_skl)),mat),s(num,u_0)))))=s(num,u_0)),
% 5.90/3.18 inference(forward_demodulation,[status(thm)],[f4521,f18042])).
% 5.90/3.18 fof(f18242,plain,(
% 5.90/3.18 ![X0,X1,X2]: (s(num,i(s(fun(cart(cart(real,X0),X1),num),rank),s(cart(cart(real,X0),X1),X2)))=s(num,u_0)|~s(cart(cart(real,X0),X1),X2)=s(cart(cart(real,X0),X1),i(s(fun(num,cart(cart(real,X0),X1)),mat),s(num,i(s(fun(num,num),numeral),s(num,u_0))))))),
% 5.90/3.18 inference(forward_demodulation,[status(thm)],[f4521,f15468])).
% 5.90/3.18 fof(f18243,plain,(
% 5.90/3.18 ![X0,X1,X2]: (s(num,i(s(fun(cart(cart(real,X0),X1),num),rank),s(cart(cart(real,X0),X1),X2)))=s(num,u_0)|~s(cart(cart(real,X0),X1),X2)=s(cart(cart(real,X0),X1),i(s(fun(num,cart(cart(real,X0),X1)),mat),s(num,u_0))))),
% 5.90/3.18 inference(forward_demodulation,[status(thm)],[f4521,f18242])).
% 5.90/3.18 fof(f18244,plain,(
% 5.90/3.18 ~s(cart(cart(real,sK3705_skl),sK3706_skl),i(s(fun(num,cart(cart(real,sK3705_skl),sK3706_skl)),mat),s(num,u_0)))=s(cart(cart(real,sK3705_skl),sK3706_skl),i(s(fun(num,cart(cart(real,sK3705_skl),sK3706_skl)),mat),s(num,u_0)))),
% 5.90/3.18 inference(resolution,[status(thm)],[f18243,f18048])).
% 5.90/3.18 fof(f18253,plain,(
% 5.90/3.18 $false),
% 5.90/3.18 inference(trivial_equality_resolution,[status(thm)],[f18244])).
% 5.90/3.18 % SZS output end CNFRefutation for theBenchmark.p
% 2.44/3.23 % Elapsed time: 2.835012 seconds
% 2.44/3.23 % CPU time: 5.857108 seconds
% 2.44/3.23 % Total memory used: 1.563 GB
% 2.44/3.23 % Net memory used: 1.559 GB
%------------------------------------------------------------------------------