%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : GEO482+1 : TPTP v9.3.1. Released v7.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n017.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:25:06 PM UTC 2026
% Result : Theorem 20.01s 5.38s
% Output : CNFRefutation 21.85s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 6
% Syntax : Number of formulae : 30 ( 15 unt; 0 def)
% Number of atoms : 61 ( 60 equ)
% Maximal formula atoms : 4 ( 2 avg)
% Number of connectives : 60 ( 29 ~; 21 |; 7 &)
% ( 0 <=>; 3 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 5 avg)
% Maximal term depth : 15 ( 3 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 13 ( 13 usr; 8 con; 0-2 aty)
% Number of variables : 89 ( 83 !; 6 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f18,axiom,
! [A,X,Y,Z0] :
( ( s(A,Y) = s(A,Z0)
& s(A,X) = s(A,Y) )
=> s(A,X) = s(A,Z0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f51,axiom,
! [A,A5] :
( ! [X,XI_] :
( ( s(A,XI_) = s(A,A5)
& s(A,X) = s(A,A5) )
=> s(A,X) = s(A,XI_) )
& ? [X] : s(A,X) = s(A,A5) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f3644,axiom,
! [Q146935,Q146944,F0,G0] :
( ( 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,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(Q146935,Q146944),i(s(fun(fun(Q146944,Q146935),fun(Q146935,Q146944)),inverse),s(fun(Q146944,Q146935),F0))) = s(fun(Q146935,Q146944),G0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f3648,axiom,
! [Q147019,A5,B0] : s(fun(Q147019,Q147019),i(s(fun(prod(Q147019,Q147019),fun(Q147019,Q147019)),swap),s(prod(Q147019,Q147019),i(s(fun(Q147019,prod(Q147019,Q147019)),i(s(fun(Q147019,fun(Q147019,prod(Q147019,Q147019))),c_),s(Q147019,A5))),s(Q147019,B0))))) = s(fun(Q147019,Q147019),i(s(fun(prod(Q147019,Q147019),fun(Q147019,Q147019)),swap),s(prod(Q147019,Q147019),i(s(fun(Q147019,prod(Q147019,Q147019)),i(s(fun(Q147019,fun(Q147019,prod(Q147019,Q147019))),c_),s(Q147019,B0))),s(Q147019,A5))))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f3649,axiom,
! [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),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f3650,conjecture,
! [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))))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f3651,negated_conjecture,
~ ! [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))))),
inference(negated_conjecture,[status(cth)],[f3650]) ).
fof(f3722,plain,
! [A,X,Y,Z0] :
( s(A,X) = s(A,Z0)
| s(A,Y) != s(A,Z0)
| s(A,X) != s(A,Y) ),
inference(pre_NNF_transformation,[status(thm)],[f18]) ).
fof(f3723,plain,
! [A,X,Z0] :
( s(A,X) = s(A,Z0)
| ! [Y] :
( s(A,Y) != s(A,Z0)
| s(A,X) != s(A,Y) ) ),
inference(miniscoping,[status(thm)],[f3722]) ).
fof(f3724,plain,
! [X0,X1,X2,X3] :
( s(X0,X1) = s(X0,X3)
| s(X0,X2) != s(X0,X3)
| s(X0,X1) != s(X0,X2) ),
inference(cnf_transformation,[status(thm)],[f3723]) ).
fof(f3942,plain,
! [A,A5] :
( ! [X,XI_] :
( s(A,X) = s(A,XI_)
| s(A,XI_) != s(A,A5)
| s(A,X) != s(A,A5) )
& ? [X] : s(A,X) = s(A,A5) ),
inference(pre_NNF_transformation,[status(thm)],[f51]) ).
fof(f3943,plain,
( ! [A,X,XI_] :
( s(A,X) = s(A,XI_)
| ! [A5] :
( s(A,XI_) != s(A,A5)
| s(A,X) != s(A,A5) ) )
& ! [A,A5] :
? [X] : s(A,X) = s(A,A5) ),
inference(miniscoping,[status(thm)],[f3942]) ).
fof(f3944,plain,
( ! [A,X,XI_] :
( s(A,X) = s(A,XI_)
| ! [A5] :
( s(A,XI_) != s(A,A5)
| s(A,X) != s(A,A5) ) )
& ! [A,A5] : s(A,sK13_skl(A5,A)) = s(A,A5) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK13_skl]),skolemize(X,sK13_skl(A5,A))],[f3943]) ).
fof(f3945,plain,
! [X0,X1] : s(X0,sK13_skl(X1,X0)) = s(X0,X1),
inference(cnf_transformation,[status(thm)],[f3944]) ).
fof(f16305,plain,
! [Q146935,Q146944,F0,G0] :
( s(fun(Q146935,Q146944),i(s(fun(fun(Q146944,Q146935),fun(Q146935,Q146944)),inverse),s(fun(Q146944,Q146935),F0))) = s(fun(Q146935,Q146944),G0)
| 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,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) ),
inference(pre_NNF_transformation,[status(thm)],[f3644]) ).
fof(f16306,plain,
! [X0,X1,X2,X3] :
( s(fun(X0,X1),i(s(fun(fun(X1,X0),fun(X0,X1)),inverse),s(fun(X1,X0),X2))) = s(fun(X0,X1),X3)
| 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,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) ),
inference(cnf_transformation,[status(thm)],[f16305]) ).
fof(f16316,plain,
! [X0,X1,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),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,X2))),s(X0,X1))))),
inference(cnf_transformation,[status(thm)],[f3648]) ).
fof(f16317,plain,
! [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),
inference(cnf_transformation,[status(thm)],[f3649]) ).
fof(f16318,plain,
? [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))))),
inference(pre_NNF_transformation,[status(thm)],[f3651]) ).
fof(f16319,plain,
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))))),
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]) ).
fof(f16320,plain,
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))))),
inference(cnf_transformation,[status(thm)],[f16319]) ).
fof(f20407,plain,
! [X0,X1,X2,X3,X4] :
( s(fun(X0,X0),X1) = 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,X4))),s(X0,X3)))))
| s(fun(X0,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,X3))),s(X0,X4)))))
| s(fun(X0,X0),X1) != s(fun(X0,X0),X2) ),
inference(paramodulation,[status(thm)],[f16316,f3724]) ).
fof(f20427,plain,
! [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)))))
| 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) ),
inference(resolution,[status(thm)],[f16317,f16306]) ).
fof(f20471,plain,
! [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)))))
| s(fun(X0,X0),i1) != s(fun(X0,X0),i1) ),
inference(forward_demodulation,[status(thm)],[f16317,f20427]) ).
fof(f20472,plain,
! [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))))),
inference(trivial_equality_resolution,[status(thm)],[f20471]) ).
fof(f23709,plain,
! [X0] :
( s(fun(sK3923_skl,sK3923_skl),X0) != 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,sK3925_skl))),s(sK3923_skl,sK3924_skl)))))
| 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),X0) ),
inference(resolution,[status(thm)],[f20407,f16320]) ).
fof(f23909,plain,
s(fun(sK3923_skl,sK3923_skl),sK13_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)))))),fun(sK3923_skl,sK3923_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,sK3925_skl))),s(sK3923_skl,sK3924_skl))))),
inference(resolution,[status(thm)],[f23709,f3945]) ).
fof(f23919,plain,
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,sK3925_skl))),s(sK3923_skl,sK3924_skl))))),
inference(forward_demodulation,[status(thm)],[f3945,f23909]) ).
fof(f25094,plain,
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,sK3925_skl))),s(sK3923_skl,sK3924_skl))))),
inference(backward_demodulation,[status(thm)],[f20472,f23919]) ).
fof(f25238,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f25094,f16316]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GEO482+1 : TPTP v9.3.1. Released v7.0.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.37 % Computer : n017.cluster.edu
% 0.08/0.37 % Model : x86_64 x86_64
% 0.08/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.37 % Memory : 8046.5625MB
% 0.08/0.37 % OS : Linux 6.8.0-71-generic
% 0.08/0.37 % CPULimit : 300
% 0.08/0.37 % WCLimit : 300
% 0.08/0.37 % DateTime : Sun Sep 20 16:35:26 UTC 2026
% 0.08/0.38 % CPUTime :
% 2.63/3.00 % Drodi V4.1.1
% 20.01/5.38 % Refutation found
% 20.01/5.38 % SZS status Theorem for theBenchmark: Theorem is valid
% 20.01/5.38 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 3.42/5.71 % Elapsed time: 5.297267 seconds
% 3.42/5.71 % CPU time: 21.846457 seconds
% 3.42/5.71 % Total memory used: 1.817 GB
% 3.42/5.71 % Net memory used: 1.813 GB
%------------------------------------------------------------------------------