%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWW211+1 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n004.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 03:07:26 PM UTC 2026
% Result : Theorem 38.58s 10.53s
% Output : CNFRefutation 39.40s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 11
% Syntax : Number of formulae : 38 ( 32 unt; 0 def)
% Number of atoms : 53 ( 15 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 35 ( 20 ~; 12 |; 0 &)
% ( 0 <=>; 3 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 3 avg)
% Maximal term depth : 8 ( 2 avg)
% Number of predicates : 5 ( 3 usr; 1 prp; 0-3 aty)
% Number of functors : 26 ( 26 usr; 11 con; 0-5 aty)
% Number of variables : 44 ( 44 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f12,axiom,
! [V_xa_2,V_gb_2,V_fa_2,T_c,T_a,T_b] : hAPP(c_Fun_Ocomp(T_b,T_a,T_c,V_fa_2,V_gb_2),V_xa_2) = hAPP(V_fa_2,hAPP(V_gb_2,V_xa_2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f48,axiom,
! [V_z,V_x,V_y,T_a] :
( class_Orderings_Oorder(T_a)
=> ( c_Orderings_Oord__class_Oless(T_a,V_y,V_x)
=> ( c_Orderings_Oord__class_Oless__eq(T_a,V_z,V_y)
=> c_Orderings_Oord__class_Oless(T_a,V_z,V_x) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f274,axiom,
c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_s(hAPP(v_f____,hAPP(v_ga____,v_n____))),c_Complex_Ocomplex_OComplex(v_x____,v_y____))),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_Complex_ORe(v_s(hAPP(v_f____,hAPP(v_ga____,v_n____)))),c_Complex_ORe(c_Complex_Ocomplex_OComplex(v_x____,v_y____)))),c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_Complex_OIm(v_s(hAPP(v_f____,hAPP(v_ga____,v_n____)))),c_Complex_OIm(c_Complex_Ocomplex_OComplex(v_x____,v_y____)))))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f299,axiom,
! [V_y,V_x] : c_Complex_OIm(c_Complex_Ocomplex_OComplex(V_x,V_y)) = V_y,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f300,axiom,
! [V_y,V_x] : c_Complex_ORe(c_Complex_Ocomplex_OComplex(V_x,V_y)) = V_x,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f348,axiom,
c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_Complex_ORe(v_s(hAPP(v_f____,hAPP(v_ga____,v_n____)))),v_x____)),c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_Complex_OIm(v_s(hAPP(v_f____,hAPP(v_ga____,v_n____)))),v_y____))),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,v_e____,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,v_e____,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f358,axiom,
! [V_x] : c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,V_x,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,V_x,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls))))) = V_x,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f509,axiom,
c_Groups_Oone__class_Oone(tc_Int_Oint) = c_Int_Onumber__class_Onumber__of(tc_Int_Oint,c_Int_OBit1(c_Int_OPls)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f541,axiom,
! [V_k] : c_Int_Onumber__class_Onumber__of(tc_Int_Oint,V_k) = V_k,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1144,axiom,
class_Orderings_Oorder(tc_RealDef_Oreal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1230,conjecture,
c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_s(hAPP(c_Fun_Ocomp(tc_Nat_Onat,tc_Nat_Onat,tc_Nat_Onat,v_f____,v_ga____),v_n____)),c_Complex_Ocomplex_OComplex(v_x____,v_y____))),v_e____),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1231,negated_conjecture,
~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_s(hAPP(c_Fun_Ocomp(tc_Nat_Onat,tc_Nat_Onat,tc_Nat_Onat,v_f____,v_ga____),v_n____)),c_Complex_Ocomplex_OComplex(v_x____,v_y____))),v_e____),
inference(negated_conjecture,[status(cth)],[f1230]) ).
fof(f1255,plain,
! [X0,X1,X2,X3,X4,X5] : hAPP(c_Fun_Ocomp(X0,X1,X2,X3,X4),X5) = hAPP(X3,hAPP(X4,X5)),
inference(cnf_transformation,[status(thm)],[f12]) ).
fof(f1370,plain,
! [V_z,V_x,V_y,T_a] :
( c_Orderings_Oord__class_Oless(T_a,V_z,V_x)
| ~ c_Orderings_Oord__class_Oless__eq(T_a,V_z,V_y)
| ~ c_Orderings_Oord__class_Oless(T_a,V_y,V_x)
| ~ class_Orderings_Oorder(T_a) ),
inference(pre_NNF_transformation,[status(thm)],[f48]) ).
fof(f1371,plain,
! [T_a] :
( ! [V_x,V_y] :
( ! [V_z] :
( c_Orderings_Oord__class_Oless(T_a,V_z,V_x)
| ~ c_Orderings_Oord__class_Oless__eq(T_a,V_z,V_y) )
| ~ c_Orderings_Oord__class_Oless(T_a,V_y,V_x) )
| ~ class_Orderings_Oorder(T_a) ),
inference(miniscoping,[status(thm)],[f1370]) ).
fof(f1372,plain,
! [X0,X1,X2,X3] :
( c_Orderings_Oord__class_Oless(X0,X3,X2)
| ~ c_Orderings_Oord__class_Oless__eq(X0,X3,X1)
| ~ c_Orderings_Oord__class_Oless(X0,X1,X2)
| ~ class_Orderings_Oorder(X0) ),
inference(cnf_transformation,[status(thm)],[f1371]) ).
fof(f2080,plain,
c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_s(hAPP(v_f____,hAPP(v_ga____,v_n____))),c_Complex_Ocomplex_OComplex(v_x____,v_y____))),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_Complex_ORe(v_s(hAPP(v_f____,hAPP(v_ga____,v_n____)))),c_Complex_ORe(c_Complex_Ocomplex_OComplex(v_x____,v_y____)))),c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_Complex_OIm(v_s(hAPP(v_f____,hAPP(v_ga____,v_n____)))),c_Complex_OIm(c_Complex_Ocomplex_OComplex(v_x____,v_y____)))))),
inference(cnf_transformation,[status(thm)],[f274]) ).
fof(f2153,plain,
! [X0,X1] : c_Complex_OIm(c_Complex_Ocomplex_OComplex(X0,X1)) = X1,
inference(cnf_transformation,[status(thm)],[f299]) ).
fof(f2154,plain,
! [X0,X1] : c_Complex_ORe(c_Complex_Ocomplex_OComplex(X0,X1)) = X0,
inference(cnf_transformation,[status(thm)],[f300]) ).
fof(f2284,plain,
c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_Complex_ORe(v_s(hAPP(v_f____,hAPP(v_ga____,v_n____)))),v_x____)),c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_Complex_OIm(v_s(hAPP(v_f____,hAPP(v_ga____,v_n____)))),v_y____))),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,v_e____,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,v_e____,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))))),
inference(cnf_transformation,[status(thm)],[f348]) ).
fof(f2320,plain,
! [X0] : c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,X0,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,X0,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls))))) = X0,
inference(cnf_transformation,[status(thm)],[f358]) ).
fof(f2765,plain,
c_Groups_Oone__class_Oone(tc_Int_Oint) = c_Int_Onumber__class_Onumber__of(tc_Int_Oint,c_Int_OBit1(c_Int_OPls)),
inference(cnf_transformation,[status(thm)],[f509]) ).
fof(f2873,plain,
! [X0] : c_Int_Onumber__class_Onumber__of(tc_Int_Oint,X0) = X0,
inference(cnf_transformation,[status(thm)],[f541]) ).
fof(f4421,plain,
class_Orderings_Oorder(tc_RealDef_Oreal),
inference(cnf_transformation,[status(thm)],[f1144]) ).
fof(f4507,plain,
~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_s(hAPP(c_Fun_Ocomp(tc_Nat_Onat,tc_Nat_Onat,tc_Nat_Onat,v_f____,v_ga____),v_n____)),c_Complex_Ocomplex_OComplex(v_x____,v_y____))),v_e____),
inference(cnf_transformation,[status(thm)],[f1231]) ).
fof(f4692,plain,
~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_s(hAPP(v_f____,hAPP(v_ga____,v_n____))),c_Complex_Ocomplex_OComplex(v_x____,v_y____))),v_e____),
inference(backward_demodulation,[status(thm)],[f1255,f4507]) ).
fof(f6712,plain,
! [X0] :
( ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_s(hAPP(v_f____,hAPP(v_ga____,v_n____))),c_Complex_Ocomplex_OComplex(v_x____,v_y____))),X0)
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X0,v_e____)
| ~ class_Orderings_Oorder(tc_RealDef_Oreal) ),
inference(resolution,[status(thm)],[f1372,f4692]) ).
fof(f6810,plain,
! [X0] :
( ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_s(hAPP(v_f____,hAPP(v_ga____,v_n____))),c_Complex_Ocomplex_OComplex(v_x____,v_y____))),X0)
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X0,v_e____) ),
inference(backward_subsumption_resolution,[status(thm)],[f6712,f4421]) ).
fof(f7072,plain,
~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_Complex_ORe(v_s(hAPP(v_f____,hAPP(v_ga____,v_n____)))),c_Complex_ORe(c_Complex_Ocomplex_OComplex(v_x____,v_y____)))),c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_Complex_OIm(v_s(hAPP(v_f____,hAPP(v_ga____,v_n____)))),c_Complex_OIm(c_Complex_Ocomplex_OComplex(v_x____,v_y____))))),v_e____),
inference(resolution,[status(thm)],[f2080,f6810]) ).
fof(f9503,plain,
~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_Complex_ORe(v_s(hAPP(v_f____,hAPP(v_ga____,v_n____)))),c_Complex_ORe(c_Complex_Ocomplex_OComplex(v_x____,v_y____)))),c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_Complex_OIm(v_s(hAPP(v_f____,hAPP(v_ga____,v_n____)))),v_y____))),v_e____),
inference(backward_demodulation,[status(thm)],[f2153,f7072]) ).
fof(f9721,plain,
~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_Complex_ORe(v_s(hAPP(v_f____,hAPP(v_ga____,v_n____)))),v_x____)),c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_Complex_OIm(v_s(hAPP(v_f____,hAPP(v_ga____,v_n____)))),v_y____))),v_e____),
inference(forward_demodulation,[status(thm)],[f2154,f9503]) ).
fof(f16387,plain,
c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_Complex_ORe(v_s(hAPP(v_f____,hAPP(v_ga____,v_n____)))),v_x____)),c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_Complex_OIm(v_s(hAPP(v_f____,hAPP(v_ga____,v_n____)))),v_y____))),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,v_e____,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,v_e____,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Groups_Oone__class_Oone(tc_Int_Oint)))))),
inference(backward_demodulation,[status(thm)],[f16388,f2284]) ).
fof(f16388,plain,
c_Groups_Oone__class_Oone(tc_Int_Oint) = c_Int_OBit1(c_Int_OPls),
inference(forward_demodulation,[status(thm)],[f2873,f2765]) ).
fof(f16395,plain,
c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_Complex_ORe(v_s(hAPP(v_f____,hAPP(v_ga____,v_n____)))),v_x____)),c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_Complex_OIm(v_s(hAPP(v_f____,hAPP(v_ga____,v_n____)))),v_y____))),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,v_e____,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Groups_Oone__class_Oone(tc_Int_Oint)))),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,v_e____,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Groups_Oone__class_Oone(tc_Int_Oint)))))),
inference(forward_demodulation,[status(thm)],[f16388,f16387]) ).
fof(f42801,plain,
! [X0] : c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,X0,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Groups_Oone__class_Oone(tc_Int_Oint)))),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,X0,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls))))) = X0,
inference(forward_demodulation,[status(thm)],[f16388,f2320]) ).
fof(f42802,plain,
c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_Complex_ORe(v_s(hAPP(v_f____,hAPP(v_ga____,v_n____)))),v_x____)),c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_Complex_OIm(v_s(hAPP(v_f____,hAPP(v_ga____,v_n____)))),v_y____))),v_e____),
inference(backward_demodulation,[status(thm)],[f42803,f16395]) ).
fof(f42803,plain,
! [X0] : c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,X0,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Groups_Oone__class_Oone(tc_Int_Oint)))),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,X0,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Groups_Oone__class_Oone(tc_Int_Oint))))) = X0,
inference(forward_demodulation,[status(thm)],[f16388,f42801]) ).
fof(f42899,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f42802,f9721]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SWW211+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.06 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.18/5.45 % Computer : n004.cluster.edu
% 0.18/5.45 % Model : x86_64 x86_64
% 0.18/5.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/5.45 % Memory : 8046.5625MB
% 0.18/5.45 % OS : Linux 6.8.0-71-generic
% 0.18/5.45 % CPULimit : 300
% 0.18/5.45 % WCLimit : 300
% 0.18/5.45 % DateTime : Mon Sep 21 09:40:57 UTC 2026
% 0.18/5.46 % CPUTime :
% 0.23/5.53 % Drodi V4.1.1
% 38.58/10.53 % Refutation found
% 38.58/10.53 % SZS status Theorem for theBenchmark: Theorem is valid
% 38.58/10.53 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 1.02/11.20 % Elapsed time: 5.735377 seconds
% 1.02/11.20 % CPU time: 40.596945 seconds
% 1.02/11.20 % Total memory used: 497.425 MB
% 1.02/11.20 % Net memory used: 477.777 MB
%------------------------------------------------------------------------------