%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SEU305+2 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n020.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 02:22:17 PM UTC 2026
% Result : Theorem 0.25s 0.60s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SEU305+2 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.18/0.45 % Computer : n020.cluster.edu
% 0.18/0.45 % Model : x86_64 x86_64
% 0.18/0.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.45 % Memory : 8046.5625MB
% 0.18/0.45 % OS : Linux 6.8.0-71-generic
% 0.18/0.45 % CPULimit : 300
% 0.18/0.45 % WCLimit : 300
% 0.18/0.45 % DateTime : Mon Sep 21 06:11:02 UTC 2026
% 0.18/0.45 % CPUTime :
% 0.25/0.54 % Drodi V4.1.1
% 0.25/0.60 % Refutation found
% 0.25/0.60 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.25/0.60 % SZS output start CNFRefutation for theBenchmark
% 0.25/0.60 fof(f19,axiom,(
% 0.25/0.60 (! [A,B,C] :( ( ~ empty_carrier(A)& join_commutative(A)& join_semilatt_str(A)& element(B,the_carrier(A))& element(C,the_carrier(A)) )=> join_commut(A,B,C) = join_commut(A,C,B) ) )),
% 0.25/0.60 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.25/0.60 fof(f59,axiom,(
% 0.25/0.60 (! [A] :( ( ~ empty_carrier(A)& join_semilatt_str(A) )=> (! [B] :( element(B,the_carrier(A))=> (! [C] :( element(C,the_carrier(A))=> ( below(A,B,C)<=> join(A,B,C) = C ) ) )) )) )),
% 0.25/0.60 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.25/0.60 fof(f247,axiom,(
% 0.25/0.60 (! [A,B,C] :( ( ~ empty_carrier(A)& join_commutative(A)& join_semilatt_str(A)& element(B,the_carrier(A))& element(C,the_carrier(A)) )=> join_commut(A,B,C) = join(A,B,C) ) )),
% 0.25/0.60 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.25/0.60 fof(f352,conjecture,(
% 0.25/0.60 (! [A] :( ( ~ empty_carrier(A)& join_commutative(A)& join_semilatt_str(A) )=> (! [B] :( element(B,the_carrier(A))=> (! [C] :( element(C,the_carrier(A))=> ( ( below(A,B,C)& below(A,C,B) )=> B = C ) ) )) )) )),
% 0.25/0.60 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.25/0.60 fof(f353,negated_conjecture,(
% 0.25/0.60 ~((! [A] :( ( ~ empty_carrier(A)& join_commutative(A)& join_semilatt_str(A) )=> (! [B] :( element(B,the_carrier(A))=> (! [C] :( element(C,the_carrier(A))=> ( ( below(A,B,C)& below(A,C,B) )=> B = C ) ) )) )) ))),
% 0.25/0.60 inference(negated_conjecture,[status(cth)],[f352])).
% 0.25/0.60 fof(f505,plain,(
% 0.25/0.60 ![A,B,C]: (((((empty_carrier(A)|~join_commutative(A))|~join_semilatt_str(A))|~element(B,the_carrier(A)))|~element(C,the_carrier(A)))|join_commut(A,B,C)=join_commut(A,C,B))),
% 0.25/0.60 inference(pre_NNF_transformation,[status(thm)],[f19])).
% 0.25/0.60 fof(f506,plain,(
% 0.25/0.60 ![X0,X1,X2]: (empty_carrier(X0)|~join_commutative(X0)|~join_semilatt_str(X0)|~element(X1,the_carrier(X0))|~element(X2,the_carrier(X0))|join_commut(X0,X1,X2)=join_commut(X0,X2,X1))),
% 0.25/0.60 inference(cnf_transformation,[status(thm)],[f505])).
% 0.25/0.60 fof(f779,plain,(
% 0.25/0.60 ![A]: ((empty_carrier(A)|~join_semilatt_str(A))|(![B]: (~element(B,the_carrier(A))|(![C]: (~element(C,the_carrier(A))|(below(A,B,C)<=>join(A,B,C)=C))))))),
% 0.25/0.60 inference(pre_NNF_transformation,[status(thm)],[f59])).
% 0.25/0.60 fof(f780,plain,(
% 0.25/0.60 ![A]: ((empty_carrier(A)|~join_semilatt_str(A))|(![B]: (~element(B,the_carrier(A))|(![C]: (~element(C,the_carrier(A))|((~below(A,B,C)|join(A,B,C)=C)&(below(A,B,C)|~join(A,B,C)=C)))))))),
% 0.25/0.60 inference(NNF_transformation,[status(thm)],[f779])).
% 0.25/0.60 fof(f781,plain,(
% 0.25/0.60 ![X0,X1,X2]: (empty_carrier(X0)|~join_semilatt_str(X0)|~element(X1,the_carrier(X0))|~element(X2,the_carrier(X0))|~below(X0,X1,X2)|join(X0,X1,X2)=X2)),
% 0.25/0.60 inference(cnf_transformation,[status(thm)],[f780])).
% 0.25/0.60 fof(f1416,plain,(
% 0.25/0.60 ![A,B,C]: (((((empty_carrier(A)|~join_commutative(A))|~join_semilatt_str(A))|~element(B,the_carrier(A)))|~element(C,the_carrier(A)))|join_commut(A,B,C)=join(A,B,C))),
% 0.25/0.60 inference(pre_NNF_transformation,[status(thm)],[f247])).
% 0.25/0.60 fof(f1417,plain,(
% 0.25/0.60 ![X0,X1,X2]: (empty_carrier(X0)|~join_commutative(X0)|~join_semilatt_str(X0)|~element(X1,the_carrier(X0))|~element(X2,the_carrier(X0))|join_commut(X0,X1,X2)=join(X0,X1,X2))),
% 0.25/0.60 inference(cnf_transformation,[status(thm)],[f1416])).
% 0.25/0.60 fof(f1959,plain,(
% 0.25/0.60 (?[A]: (((~empty_carrier(A)&join_commutative(A))&join_semilatt_str(A))&(?[B]: (element(B,the_carrier(A))&(?[C]: (element(C,the_carrier(A))&((below(A,B,C)&below(A,C,B))&~B=C)))))))),
% 0.25/0.60 inference(pre_NNF_transformation,[status(thm)],[f353])).
% 0.25/0.60 fof(f1960,plain,(
% 0.25/0.60 (((~empty_carrier(sK256_skl)&join_commutative(sK256_skl))&join_semilatt_str(sK256_skl))&(element(sK257_skl,the_carrier(sK256_skl))&(element(sK258_skl,the_carrier(sK256_skl))&((below(sK256_skl,sK257_skl,sK258_skl)&below(sK256_skl,sK258_skl,sK257_skl))&~sK257_skl=sK258_skl))))),
% 0.25/0.60 inference(skolemize,[status(esa),new_symbols(skolem,[sK256_skl,sK257_skl,sK258_skl]),skolemize(A,sK256_skl),skolemize(B,sK257_skl),skolemize(C,sK258_skl)],[f1959])).
% 0.25/0.60 fof(f1961,plain,(
% 0.25/0.60 ~empty_carrier(sK256_skl)),
% 0.25/0.60 inference(cnf_transformation,[status(thm)],[f1960])).
% 0.25/0.60 fof(f1962,plain,(
% 0.25/0.60 join_commutative(sK256_skl)),
% 0.25/0.60 inference(cnf_transformation,[status(thm)],[f1960])).
% 0.25/0.60 fof(f1963,plain,(
% 0.25/0.60 join_semilatt_str(sK256_skl)),
% 0.25/0.60 inference(cnf_transformation,[status(thm)],[f1960])).
% 0.25/0.60 fof(f1964,plain,(
% 0.25/0.60 element(sK257_skl,the_carrier(sK256_skl))),
% 0.25/0.60 inference(cnf_transformation,[status(thm)],[f1960])).
% 0.25/0.60 fof(f1965,plain,(
% 0.25/0.60 element(sK258_skl,the_carrier(sK256_skl))),
% 0.25/0.60 inference(cnf_transformation,[status(thm)],[f1960])).
% 0.25/0.60 fof(f1966,plain,(
% 0.25/0.60 below(sK256_skl,sK257_skl,sK258_skl)),
% 0.25/0.60 inference(cnf_transformation,[status(thm)],[f1960])).
% 0.25/0.60 fof(f1967,plain,(
% 0.25/0.60 below(sK256_skl,sK258_skl,sK257_skl)),
% 0.25/0.60 inference(cnf_transformation,[status(thm)],[f1960])).
% 0.25/0.60 fof(f1968,plain,(
% 0.25/0.60 ~sK257_skl=sK258_skl),
% 0.25/0.60 inference(cnf_transformation,[status(thm)],[f1960])).
% 0.25/0.60 fof(f2842,plain,(
% 0.25/0.60 ![X0,X1]: (empty_carrier(sK256_skl)|~join_commutative(sK256_skl)|~element(X0,the_carrier(sK256_skl))|~element(X1,the_carrier(sK256_skl))|join_commut(sK256_skl,X0,X1)=join_commut(sK256_skl,X1,X0))),
% 0.25/0.60 inference(resolution,[status(thm)],[f506,f1963])).
% 0.25/0.60 fof(f2843,plain,(
% 0.25/0.60 ![X0,X1]: (~join_commutative(sK256_skl)|~element(X0,the_carrier(sK256_skl))|~element(X1,the_carrier(sK256_skl))|join_commut(sK256_skl,X0,X1)=join_commut(sK256_skl,X1,X0))),
% 0.25/0.60 inference(forward_subsumption_resolution,[status(thm)],[f2842,f1961])).
% 0.25/0.60 fof(f2846,plain,(
% 0.25/0.60 empty_carrier(sK256_skl)|~join_semilatt_str(sK256_skl)|~element(sK257_skl,the_carrier(sK256_skl))|~element(sK258_skl,the_carrier(sK256_skl))|join(sK256_skl,sK257_skl,sK258_skl)=sK258_skl),
% 0.25/0.60 inference(resolution,[status(thm)],[f1966,f781])).
% 0.25/0.60 fof(f2847,plain,(
% 0.25/0.60 ~join_semilatt_str(sK256_skl)|~element(sK257_skl,the_carrier(sK256_skl))|~element(sK258_skl,the_carrier(sK256_skl))|join(sK256_skl,sK257_skl,sK258_skl)=sK258_skl),
% 0.25/0.60 inference(forward_subsumption_resolution,[status(thm)],[f2846,f1961])).
% 0.25/0.60 fof(f2848,plain,(
% 0.25/0.60 empty_carrier(sK256_skl)|~join_semilatt_str(sK256_skl)|~element(sK258_skl,the_carrier(sK256_skl))|~element(sK257_skl,the_carrier(sK256_skl))|join(sK256_skl,sK258_skl,sK257_skl)=sK257_skl),
% 0.25/0.60 inference(resolution,[status(thm)],[f1967,f781])).
% 0.25/0.60 fof(f2849,plain,(
% 0.25/0.60 ~join_semilatt_str(sK256_skl)|~element(sK258_skl,the_carrier(sK256_skl))|~element(sK257_skl,the_carrier(sK256_skl))|join(sK256_skl,sK258_skl,sK257_skl)=sK257_skl),
% 0.25/0.60 inference(forward_subsumption_resolution,[status(thm)],[f2848,f1961])).
% 0.25/0.60 fof(f2850,plain,(
% 0.25/0.60 ![X0,X1]: (empty_carrier(sK256_skl)|~join_commutative(sK256_skl)|~element(X0,the_carrier(sK256_skl))|~element(X1,the_carrier(sK256_skl))|join_commut(sK256_skl,X0,X1)=join(sK256_skl,X0,X1))),
% 0.25/0.60 inference(resolution,[status(thm)],[f1417,f1963])).
% 0.25/0.60 fof(f2851,plain,(
% 0.25/0.60 ![X0,X1]: (~join_commutative(sK256_skl)|~element(X0,the_carrier(sK256_skl))|~element(X1,the_carrier(sK256_skl))|join_commut(sK256_skl,X0,X1)=join(sK256_skl,X0,X1))),
% 0.25/0.60 inference(forward_subsumption_resolution,[status(thm)],[f2850,f1961])).
% 0.25/0.60 fof(f2852,plain,(
% 0.25/0.60 ![X0,X1]: (~element(X0,the_carrier(sK256_skl))|~element(X1,the_carrier(sK256_skl))|join_commut(sK256_skl,X0,X1)=join_commut(sK256_skl,X1,X0))),
% 0.25/0.60 inference(forward_subsumption_resolution,[status(thm)],[f2843,f1962])).
% 0.25/0.60 fof(f2854,plain,(
% 0.25/0.60 ![X0]: (~element(X0,the_carrier(sK256_skl))|join_commut(sK256_skl,X0,sK258_skl)=join_commut(sK256_skl,sK258_skl,X0))),
% 0.25/0.60 inference(resolution,[status(thm)],[f2852,f1965])).
% 0.25/0.60 fof(f2866,plain,(
% 0.25/0.60 join_commut(sK256_skl,sK257_skl,sK258_skl)=join_commut(sK256_skl,sK258_skl,sK257_skl)),
% 0.25/0.60 inference(resolution,[status(thm)],[f2854,f1964])).
% 0.25/0.60 fof(f2871,plain,(
% 0.25/0.60 ~element(sK257_skl,the_carrier(sK256_skl))|~element(sK258_skl,the_carrier(sK256_skl))|join(sK256_skl,sK257_skl,sK258_skl)=sK258_skl),
% 0.25/0.60 inference(forward_subsumption_resolution,[status(thm)],[f2847,f1963])).
% 0.25/0.60 fof(f2872,plain,(
% 0.25/0.60 ~element(sK257_skl,the_carrier(sK256_skl))|join(sK256_skl,sK257_skl,sK258_skl)=sK258_skl),
% 0.25/0.60 inference(resolution,[status(thm)],[f2871,f1965])).
% 0.25/0.60 fof(f2875,plain,(
% 0.25/0.60 join(sK256_skl,sK257_skl,sK258_skl)=sK258_skl),
% 0.25/0.60 inference(forward_subsumption_resolution,[status(thm)],[f2872,f1964])).
% 0.25/0.60 fof(f2880,plain,(
% 0.25/0.60 ~element(sK258_skl,the_carrier(sK256_skl))|~element(sK257_skl,the_carrier(sK256_skl))|join(sK256_skl,sK258_skl,sK257_skl)=sK257_skl),
% 0.25/0.62 inference(forward_subsumption_resolution,[status(thm)],[f2849,f1963])).
% 0.25/0.62 fof(f2881,plain,(
% 0.25/0.62 ~element(sK257_skl,the_carrier(sK256_skl))|join(sK256_skl,sK258_skl,sK257_skl)=sK257_skl),
% 0.25/0.62 inference(resolution,[status(thm)],[f2880,f1965])).
% 0.25/0.62 fof(f2884,plain,(
% 0.25/0.62 join(sK256_skl,sK258_skl,sK257_skl)=sK257_skl),
% 0.25/0.62 inference(forward_subsumption_resolution,[status(thm)],[f2881,f1964])).
% 0.25/0.62 fof(f2887,plain,(
% 0.25/0.62 ![X0,X1]: (~element(X0,the_carrier(sK256_skl))|~element(X1,the_carrier(sK256_skl))|join_commut(sK256_skl,X0,X1)=join(sK256_skl,X0,X1))),
% 0.25/0.62 inference(forward_subsumption_resolution,[status(thm)],[f2851,f1962])).
% 0.25/0.62 fof(f2889,plain,(
% 0.25/0.62 ![X0]: (~element(X0,the_carrier(sK256_skl))|join_commut(sK256_skl,X0,sK258_skl)=join(sK256_skl,X0,sK258_skl))),
% 0.25/0.62 inference(resolution,[status(thm)],[f2887,f1965])).
% 0.25/0.62 fof(f2890,plain,(
% 0.25/0.62 ![X0]: (~element(X0,the_carrier(sK256_skl))|join_commut(sK256_skl,X0,sK257_skl)=join(sK256_skl,X0,sK257_skl))),
% 0.25/0.62 inference(resolution,[status(thm)],[f2887,f1964])).
% 0.25/0.62 fof(f2940,plain,(
% 0.25/0.62 join_commut(sK256_skl,sK257_skl,sK258_skl)=join(sK256_skl,sK257_skl,sK258_skl)),
% 0.25/0.62 inference(resolution,[status(thm)],[f2889,f1964])).
% 0.25/0.62 fof(f2944,plain,(
% 0.25/0.62 join_commut(sK256_skl,sK257_skl,sK258_skl)=sK258_skl),
% 0.25/0.62 inference(forward_demodulation,[status(thm)],[f2875,f2940])).
% 0.25/0.62 fof(f2946,plain,(
% 0.25/0.62 join_commut(sK256_skl,sK258_skl,sK257_skl)=join(sK256_skl,sK258_skl,sK257_skl)),
% 0.25/0.62 inference(resolution,[status(thm)],[f2890,f1965])).
% 0.25/0.62 fof(f2951,plain,(
% 0.25/0.62 join_commut(sK256_skl,sK257_skl,sK258_skl)=join(sK256_skl,sK258_skl,sK257_skl)),
% 0.25/0.62 inference(forward_demodulation,[status(thm)],[f2866,f2946])).
% 0.25/0.62 fof(f2952,plain,(
% 0.25/0.62 join_commut(sK256_skl,sK257_skl,sK258_skl)=sK257_skl),
% 0.25/0.62 inference(forward_demodulation,[status(thm)],[f2884,f2951])).
% 0.25/0.62 fof(f2960,plain,(
% 0.25/0.62 sK257_skl=sK258_skl),
% 0.25/0.62 inference(backward_demodulation,[status(thm)],[f2952,f2944])).
% 0.25/0.62 fof(f2962,plain,(
% 0.25/0.62 $false),
% 0.25/0.62 inference(forward_subsumption_resolution,[status(thm)],[f2960,f1968])).
% 0.25/0.62 % SZS output end CNFRefutation for theBenchmark.p
% 0.25/0.69 % Elapsed time: 0.221271 seconds
% 0.25/0.69 % CPU time: 0.454398 seconds
% 0.25/0.69 % Total memory used: 77.521 MB
% 0.25/0.69 % Net memory used: 77.067 MB
%------------------------------------------------------------------------------