%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GEO482+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 : n001.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 15.79s 4.89s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : GEO482+1 : TPTP v9.3.1. Released v7.0.0.
% 0.00/0.07 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.17/0.41 % Computer : n001.cluster.edu
% 0.17/0.41 % Model : x86_64 x86_64
% 0.17/0.41 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.41 % Memory : 8046.5625MB
% 0.17/0.41 % OS : Linux 6.8.0-71-generic
% 0.17/0.41 % CPULimit : 300
% 0.17/0.41 % WCLimit : 300
% 0.17/0.42 % DateTime : Sun Sep 20 16:45:42 UTC 2026
% 0.17/0.42 % CPUTime :
% 2.78/3.14 % Drodi V4.1.1
% 15.79/4.89 % Refutation found
% 15.79/4.89 % SZS status Theorem for theBenchmark: Theorem is valid
% 15.79/4.89 % SZS output start CNFRefutation for theBenchmark
% 15.79/4.89 fof(f3644,axiom,(
% 15.79/4.89 (! [Q146935,Q146944,F0,G0] :( ( s(fun(Q146935,Q146935),i(s(fun(fun(Q146935,Q146944),fun(Q146935,Q146935)),i(s(fun(fun(Q146944,Q146935),fun(fun(Q146935,Q146944),fun(Q146935,Q146935))),o),s(fun(Q146944,Q146935),F0))),s(fun(Q146935,Q146944),G0))) = s(fun(Q146935,Q146935),i1)& s(fun(Q146944,Q146944),i(s(fun(fun(Q146944,Q146935),fun(Q146944,Q146944)),i(s(fun(fun(Q146935,Q146944),fun(fun(Q146944,Q146935),fun(Q146944,Q146944))),o),s(fun(Q146935,Q146944),G0))),s(fun(Q146944,Q146935),F0))) = s(fun(Q146944,Q146944),i1) )=> s(fun(Q146935,Q146944),i(s(fun(fun(Q146944,Q146935),fun(Q146935,Q146944)),inverse),s(fun(Q146944,Q146935),F0))) = s(fun(Q146935,Q146944),G0) ) )),
% 15.79/4.89 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 15.79/4.89 fof(f3649,axiom,(
% 15.79/4.89 (! [Q147052,A5,B0] : s(fun(Q147052,Q147052),i(s(fun(fun(Q147052,Q147052),fun(Q147052,Q147052)),i(s(fun(fun(Q147052,Q147052),fun(fun(Q147052,Q147052),fun(Q147052,Q147052))),o),s(fun(Q147052,Q147052),i(s(fun(prod(Q147052,Q147052),fun(Q147052,Q147052)),swap),s(prod(Q147052,Q147052),i(s(fun(Q147052,prod(Q147052,Q147052)),i(s(fun(Q147052,fun(Q147052,prod(Q147052,Q147052))),c_),s(Q147052,A5))),s(Q147052,B0))))))),s(fun(Q147052,Q147052),i(s(fun(prod(Q147052,Q147052),fun(Q147052,Q147052)),swap),s(prod(Q147052,Q147052),i(s(fun(Q147052,prod(Q147052,Q147052)),i(s(fun(Q147052,fun(Q147052,prod(Q147052,Q147052))),c_),s(Q147052,A5))),s(Q147052,B0))))))) = s(fun(Q147052,Q147052),i1) )),
% 15.79/4.89 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 15.79/4.89 fof(f3650,conjecture,(
% 15.79/4.89 (! [Q147076,A5,B0] : s(fun(Q147076,Q147076),i(s(fun(fun(Q147076,Q147076),fun(Q147076,Q147076)),inverse),s(fun(Q147076,Q147076),i(s(fun(prod(Q147076,Q147076),fun(Q147076,Q147076)),swap),s(prod(Q147076,Q147076),i(s(fun(Q147076,prod(Q147076,Q147076)),i(s(fun(Q147076,fun(Q147076,prod(Q147076,Q147076))),c_),s(Q147076,A5))),s(Q147076,B0))))))) = s(fun(Q147076,Q147076),i(s(fun(prod(Q147076,Q147076),fun(Q147076,Q147076)),swap),s(prod(Q147076,Q147076),i(s(fun(Q147076,prod(Q147076,Q147076)),i(s(fun(Q147076,fun(Q147076,prod(Q147076,Q147076))),c_),s(Q147076,A5))),s(Q147076,B0))))) )),
% 15.79/4.89 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 15.79/4.89 fof(f3651,negated_conjecture,(
% 15.79/4.89 ~((! [Q147076,A5,B0] : s(fun(Q147076,Q147076),i(s(fun(fun(Q147076,Q147076),fun(Q147076,Q147076)),inverse),s(fun(Q147076,Q147076),i(s(fun(prod(Q147076,Q147076),fun(Q147076,Q147076)),swap),s(prod(Q147076,Q147076),i(s(fun(Q147076,prod(Q147076,Q147076)),i(s(fun(Q147076,fun(Q147076,prod(Q147076,Q147076))),c_),s(Q147076,A5))),s(Q147076,B0))))))) = s(fun(Q147076,Q147076),i(s(fun(prod(Q147076,Q147076),fun(Q147076,Q147076)),swap),s(prod(Q147076,Q147076),i(s(fun(Q147076,prod(Q147076,Q147076)),i(s(fun(Q147076,fun(Q147076,prod(Q147076,Q147076))),c_),s(Q147076,A5))),s(Q147076,B0))))) ))),
% 15.79/4.89 inference(negated_conjecture,[status(cth)],[f3650])).
% 15.79/4.89 fof(f16305,plain,(
% 15.79/4.89 ![Q146935,Q146944,F0,G0]: ((~s(fun(Q146935,Q146935),i(s(fun(fun(Q146935,Q146944),fun(Q146935,Q146935)),i(s(fun(fun(Q146944,Q146935),fun(fun(Q146935,Q146944),fun(Q146935,Q146935))),o),s(fun(Q146944,Q146935),F0))),s(fun(Q146935,Q146944),G0)))=s(fun(Q146935,Q146935),i1)|~s(fun(Q146944,Q146944),i(s(fun(fun(Q146944,Q146935),fun(Q146944,Q146944)),i(s(fun(fun(Q146935,Q146944),fun(fun(Q146944,Q146935),fun(Q146944,Q146944))),o),s(fun(Q146935,Q146944),G0))),s(fun(Q146944,Q146935),F0)))=s(fun(Q146944,Q146944),i1))|s(fun(Q146935,Q146944),i(s(fun(fun(Q146944,Q146935),fun(Q146935,Q146944)),inverse),s(fun(Q146944,Q146935),F0)))=s(fun(Q146935,Q146944),G0))),
% 15.79/4.89 inference(pre_NNF_transformation,[status(thm)],[f3644])).
% 15.79/4.89 fof(f16306,plain,(
% 15.79/4.89 ![X0,X1,X2,X3]: (~s(fun(X0,X0),i(s(fun(fun(X0,X1),fun(X0,X0)),i(s(fun(fun(X1,X0),fun(fun(X0,X1),fun(X0,X0))),o),s(fun(X1,X0),X2))),s(fun(X0,X1),X3)))=s(fun(X0,X0),i1)|~s(fun(X1,X1),i(s(fun(fun(X1,X0),fun(X1,X1)),i(s(fun(fun(X0,X1),fun(fun(X1,X0),fun(X1,X1))),o),s(fun(X0,X1),X3))),s(fun(X1,X0),X2)))=s(fun(X1,X1),i1)|s(fun(X0,X1),i(s(fun(fun(X1,X0),fun(X0,X1)),inverse),s(fun(X1,X0),X2)))=s(fun(X0,X1),X3))),
% 15.79/4.89 inference(cnf_transformation,[status(thm)],[f16305])).
% 15.79/4.89 fof(f16317,plain,(
% 15.79/4.89 ![X0,X1,X2]: (s(fun(X0,X0),i(s(fun(fun(X0,X0),fun(X0,X0)),i(s(fun(fun(X0,X0),fun(fun(X0,X0),fun(X0,X0))),o),s(fun(X0,X0),i(s(fun(prod(X0,X0),fun(X0,X0)),swap),s(prod(X0,X0),i(s(fun(X0,prod(X0,X0)),i(s(fun(X0,fun(X0,prod(X0,X0))),c_),s(X0,X1))),s(X0,X2))))))),s(fun(X0,X0),i(s(fun(prod(X0,X0),fun(X0,X0)),swap),s(prod(X0,X0),i(s(fun(X0,prod(X0,X0)),i(s(fun(X0,fun(X0,prod(X0,X0))),c_),s(X0,X1))),s(X0,X2)))))))=s(fun(X0,X0),i1))),
% 15.79/4.89 inference(cnf_transformation,[status(thm)],[f3649])).
% 15.79/4.89 fof(f16318,plain,(
% 15.79/4.89 (?[Q147076,A5,B0]: ~s(fun(Q147076,Q147076),i(s(fun(fun(Q147076,Q147076),fun(Q147076,Q147076)),inverse),s(fun(Q147076,Q147076),i(s(fun(prod(Q147076,Q147076),fun(Q147076,Q147076)),swap),s(prod(Q147076,Q147076),i(s(fun(Q147076,prod(Q147076,Q147076)),i(s(fun(Q147076,fun(Q147076,prod(Q147076,Q147076))),c_),s(Q147076,A5))),s(Q147076,B0)))))))=s(fun(Q147076,Q147076),i(s(fun(prod(Q147076,Q147076),fun(Q147076,Q147076)),swap),s(prod(Q147076,Q147076),i(s(fun(Q147076,prod(Q147076,Q147076)),i(s(fun(Q147076,fun(Q147076,prod(Q147076,Q147076))),c_),s(Q147076,A5))),s(Q147076,B0))))))),
% 15.79/4.89 inference(pre_NNF_transformation,[status(thm)],[f3651])).
% 15.79/4.89 fof(f16319,plain,(
% 15.79/4.89 ~s(fun(sK3923_skl,sK3923_skl),i(s(fun(fun(sK3923_skl,sK3923_skl),fun(sK3923_skl,sK3923_skl)),inverse),s(fun(sK3923_skl,sK3923_skl),i(s(fun(prod(sK3923_skl,sK3923_skl),fun(sK3923_skl,sK3923_skl)),swap),s(prod(sK3923_skl,sK3923_skl),i(s(fun(sK3923_skl,prod(sK3923_skl,sK3923_skl)),i(s(fun(sK3923_skl,fun(sK3923_skl,prod(sK3923_skl,sK3923_skl))),c_),s(sK3923_skl,sK3924_skl))),s(sK3923_skl,sK3925_skl)))))))=s(fun(sK3923_skl,sK3923_skl),i(s(fun(prod(sK3923_skl,sK3923_skl),fun(sK3923_skl,sK3923_skl)),swap),s(prod(sK3923_skl,sK3923_skl),i(s(fun(sK3923_skl,prod(sK3923_skl,sK3923_skl)),i(s(fun(sK3923_skl,fun(sK3923_skl,prod(sK3923_skl,sK3923_skl))),c_),s(sK3923_skl,sK3924_skl))),s(sK3923_skl,sK3925_skl)))))),
% 15.79/4.89 inference(skolemize,[status(esa),new_symbols(skolem,[sK3923_skl,sK3924_skl,sK3925_skl]),skolemize(Q147076,sK3923_skl),skolemize(A5,sK3924_skl),skolemize(B0,sK3925_skl)],[f16318])).
% 15.79/4.89 fof(f16320,plain,(
% 15.79/4.89 ~s(fun(sK3923_skl,sK3923_skl),i(s(fun(fun(sK3923_skl,sK3923_skl),fun(sK3923_skl,sK3923_skl)),inverse),s(fun(sK3923_skl,sK3923_skl),i(s(fun(prod(sK3923_skl,sK3923_skl),fun(sK3923_skl,sK3923_skl)),swap),s(prod(sK3923_skl,sK3923_skl),i(s(fun(sK3923_skl,prod(sK3923_skl,sK3923_skl)),i(s(fun(sK3923_skl,fun(sK3923_skl,prod(sK3923_skl,sK3923_skl))),c_),s(sK3923_skl,sK3924_skl))),s(sK3923_skl,sK3925_skl)))))))=s(fun(sK3923_skl,sK3923_skl),i(s(fun(prod(sK3923_skl,sK3923_skl),fun(sK3923_skl,sK3923_skl)),swap),s(prod(sK3923_skl,sK3923_skl),i(s(fun(sK3923_skl,prod(sK3923_skl,sK3923_skl)),i(s(fun(sK3923_skl,fun(sK3923_skl,prod(sK3923_skl,sK3923_skl))),c_),s(sK3923_skl,sK3924_skl))),s(sK3923_skl,sK3925_skl)))))),
% 15.79/4.89 inference(cnf_transformation,[status(thm)],[f16319])).
% 15.79/4.89 fof(f19649,plain,(
% 15.79/4.89 ![X0,X1,X2]: (~s(fun(X0,X0),i(s(fun(fun(X0,X0),fun(X0,X0)),i(s(fun(fun(X0,X0),fun(fun(X0,X0),fun(X0,X0))),o),s(fun(X0,X0),i(s(fun(prod(X0,X0),fun(X0,X0)),swap),s(prod(X0,X0),i(s(fun(X0,prod(X0,X0)),i(s(fun(X0,fun(X0,prod(X0,X0))),c_),s(X0,X1))),s(X0,X2))))))),s(fun(X0,X0),i(s(fun(prod(X0,X0),fun(X0,X0)),swap),s(prod(X0,X0),i(s(fun(X0,prod(X0,X0)),i(s(fun(X0,fun(X0,prod(X0,X0))),c_),s(X0,X1))),s(X0,X2)))))))=s(fun(X0,X0),i1)|s(fun(X0,X0),i(s(fun(fun(X0,X0),fun(X0,X0)),inverse),s(fun(X0,X0),i(s(fun(prod(X0,X0),fun(X0,X0)),swap),s(prod(X0,X0),i(s(fun(X0,prod(X0,X0)),i(s(fun(X0,fun(X0,prod(X0,X0))),c_),s(X0,X1))),s(X0,X2)))))))=s(fun(X0,X0),i(s(fun(prod(X0,X0),fun(X0,X0)),swap),s(prod(X0,X0),i(s(fun(X0,prod(X0,X0)),i(s(fun(X0,fun(X0,prod(X0,X0))),c_),s(X0,X1))),s(X0,X2))))))),
% 15.79/4.89 inference(resolution,[status(thm)],[f16317,f16306])).
% 15.79/4.89 fof(f19735,plain,(
% 15.79/4.89 ![X0,X1,X2]: (~s(fun(X0,X0),i1)=s(fun(X0,X0),i1)|s(fun(X0,X0),i(s(fun(fun(X0,X0),fun(X0,X0)),inverse),s(fun(X0,X0),i(s(fun(prod(X0,X0),fun(X0,X0)),swap),s(prod(X0,X0),i(s(fun(X0,prod(X0,X0)),i(s(fun(X0,fun(X0,prod(X0,X0))),c_),s(X0,X1))),s(X0,X2)))))))=s(fun(X0,X0),i(s(fun(prod(X0,X0),fun(X0,X0)),swap),s(prod(X0,X0),i(s(fun(X0,prod(X0,X0)),i(s(fun(X0,fun(X0,prod(X0,X0))),c_),s(X0,X1))),s(X0,X2))))))),
% 17.37/5.11 inference(forward_demodulation,[status(thm)],[f16317,f19649])).
% 17.37/5.11 fof(f19736,plain,(
% 17.37/5.11 ![X0,X1,X2]: (s(fun(X0,X0),i(s(fun(fun(X0,X0),fun(X0,X0)),inverse),s(fun(X0,X0),i(s(fun(prod(X0,X0),fun(X0,X0)),swap),s(prod(X0,X0),i(s(fun(X0,prod(X0,X0)),i(s(fun(X0,fun(X0,prod(X0,X0))),c_),s(X0,X1))),s(X0,X2)))))))=s(fun(X0,X0),i(s(fun(prod(X0,X0),fun(X0,X0)),swap),s(prod(X0,X0),i(s(fun(X0,prod(X0,X0)),i(s(fun(X0,fun(X0,prod(X0,X0))),c_),s(X0,X1))),s(X0,X2))))))),
% 17.37/5.11 inference(trivial_equality_resolution,[status(thm)],[f19735])).
% 17.37/5.11 fof(f19938,plain,(
% 17.37/5.11 ~s(fun(sK3923_skl,sK3923_skl),i(s(fun(prod(sK3923_skl,sK3923_skl),fun(sK3923_skl,sK3923_skl)),swap),s(prod(sK3923_skl,sK3923_skl),i(s(fun(sK3923_skl,prod(sK3923_skl,sK3923_skl)),i(s(fun(sK3923_skl,fun(sK3923_skl,prod(sK3923_skl,sK3923_skl))),c_),s(sK3923_skl,sK3924_skl))),s(sK3923_skl,sK3925_skl)))))=s(fun(sK3923_skl,sK3923_skl),i(s(fun(prod(sK3923_skl,sK3923_skl),fun(sK3923_skl,sK3923_skl)),swap),s(prod(sK3923_skl,sK3923_skl),i(s(fun(sK3923_skl,prod(sK3923_skl,sK3923_skl)),i(s(fun(sK3923_skl,fun(sK3923_skl,prod(sK3923_skl,sK3923_skl))),c_),s(sK3923_skl,sK3924_skl))),s(sK3923_skl,sK3925_skl)))))),
% 17.37/5.11 inference(backward_demodulation,[status(thm)],[f19736,f16320])).
% 17.37/5.11 fof(f20015,plain,(
% 17.37/5.11 $false),
% 17.37/5.11 inference(trivial_equality_resolution,[status(thm)],[f19938])).
% 17.37/5.11 % SZS output end CNFRefutation for theBenchmark.p
% 3.35/5.21 % Elapsed time: 4.746413 seconds
% 3.35/5.21 % CPU time: 16.744329 seconds
% 3.35/5.21 % Total memory used: 1.761 GB
% 3.35/5.21 % Net memory used: 1.757 GB
%------------------------------------------------------------------------------