%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SEU408+1 : TPTP v9.3.1. Released v3.4.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 02:22:33 PM UTC 2026
% Result : Theorem 0.13s 5.44s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU408+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/5.35 % Computer : n001.cluster.edu
% 0.09/5.35 % Model : x86_64 x86_64
% 0.09/5.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/5.35 % Memory : 8046.5625MB
% 0.09/5.35 % OS : Linux 6.8.0-71-generic
% 0.09/5.36 % CPULimit : 300
% 0.09/5.36 % WCLimit : 300
% 0.09/5.36 % DateTime : Mon Sep 21 06:26:49 UTC 2026
% 0.09/5.36 % CPUTime :
% 0.09/5.37 % Drodi V4.1.1
% 0.13/5.44 % Refutation found
% 0.13/5.44 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.13/5.44 % SZS output start CNFRefutation for theBenchmark
% 0.13/5.44 fof(f1,conjecture,(
% 0.13/5.44 (! [A] :( ( ~ v3_struct_0(A)& v2_orders_2(A)& v3_orders_2(A)& v4_orders_2(A)& v1_lattice3(A)& l1_orders_2(A) )=> (! [B] :( ( ~ v3_struct_0(B)& v2_orders_2(B)& v3_orders_2(B)& v4_orders_2(B)& v1_lattice3(B)& l1_orders_2(B) )=> (! [C] :( r2_hidden(C,u1_struct_0(B))=> m1_subset_1(C,u1_struct_0(k1_latsum_1(A,B))) ) )) )) )),
% 0.13/5.44 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/5.44 fof(f2,negated_conjecture,(
% 0.13/5.44 ~((! [A] :( ( ~ v3_struct_0(A)& v2_orders_2(A)& v3_orders_2(A)& v4_orders_2(A)& v1_lattice3(A)& l1_orders_2(A) )=> (! [B] :( ( ~ v3_struct_0(B)& v2_orders_2(B)& v3_orders_2(B)& v4_orders_2(B)& v1_lattice3(B)& l1_orders_2(B) )=> (! [C] :( r2_hidden(C,u1_struct_0(B))=> m1_subset_1(C,u1_struct_0(k1_latsum_1(A,B))) ) )) )) ))),
% 0.13/5.44 inference(negated_conjecture,[status(cth)],[f1])).
% 0.13/5.44 fof(f7,axiom,(
% 0.13/5.44 (! [A] :( l1_orders_2(A)=> (! [B] :( l1_orders_2(B)=> (! [C] :( ( v1_orders_2(C)& l1_orders_2(C) )=> ( C = k1_latsum_1(A,B)<=> ( u1_struct_0(C) = k2_xboole_0(u1_struct_0(A),u1_struct_0(B))& u1_orders_2(C) = k2_xboole_0(k2_xboole_0(u1_orders_2(A),u1_orders_2(B)),k7_relset_1(u1_struct_0(A),u1_struct_0(A),u1_struct_0(B),u1_struct_0(B),u1_orders_2(A),u1_orders_2(B))) ) ) ) )) )) )),
% 0.13/5.44 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/5.44 fof(f8,axiom,(
% 0.13/5.44 (! [A,B,C] :( C = k2_xboole_0(A,B)<=> (! [D] :( r2_hidden(D,C)<=> ( r2_hidden(D,A)| r2_hidden(D,B) ) ) )) )),
% 0.13/5.44 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/5.44 fof(f10,axiom,(
% 0.13/5.44 (! [A,B] :( ( l1_orders_2(A)& l1_orders_2(B) )=> ( v1_orders_2(k1_latsum_1(A,B))& l1_orders_2(k1_latsum_1(A,B)) ) ) )),
% 0.13/5.44 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/5.44 fof(f29,axiom,(
% 0.13/5.44 (! [A,B] :( ( l1_orders_2(A)& ~ v3_struct_0(B)& l1_orders_2(B) )=> ( ~ v3_struct_0(k1_latsum_1(A,B))& v1_orders_2(k1_latsum_1(A,B)) ) ) )),
% 0.13/5.44 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/5.44 fof(f45,axiom,(
% 0.13/5.44 (! [A,B] :( r2_hidden(A,B)=> m1_subset_1(A,B) ) )),
% 0.13/5.44 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/5.44 fof(f53,plain,(
% 0.13/5.44 (?[A]: ((((((~v3_struct_0(A)&v2_orders_2(A))&v3_orders_2(A))&v4_orders_2(A))&v1_lattice3(A))&l1_orders_2(A))&(?[B]: ((((((~v3_struct_0(B)&v2_orders_2(B))&v3_orders_2(B))&v4_orders_2(B))&v1_lattice3(B))&l1_orders_2(B))&(?[C]: (r2_hidden(C,u1_struct_0(B))&~m1_subset_1(C,u1_struct_0(k1_latsum_1(A,B)))))))))),
% 0.13/5.44 inference(pre_NNF_transformation,[status(thm)],[f2])).
% 0.13/5.44 fof(f54,plain,(
% 0.13/5.44 ((((((~v3_struct_0(sK0_skl)&v2_orders_2(sK0_skl))&v3_orders_2(sK0_skl))&v4_orders_2(sK0_skl))&v1_lattice3(sK0_skl))&l1_orders_2(sK0_skl))&((((((~v3_struct_0(sK1_skl)&v2_orders_2(sK1_skl))&v3_orders_2(sK1_skl))&v4_orders_2(sK1_skl))&v1_lattice3(sK1_skl))&l1_orders_2(sK1_skl))&(r2_hidden(sK2_skl,u1_struct_0(sK1_skl))&~m1_subset_1(sK2_skl,u1_struct_0(k1_latsum_1(sK0_skl,sK1_skl))))))),
% 0.13/5.44 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl,sK2_skl]),skolemize(A,sK0_skl),skolemize(B,sK1_skl),skolemize(C,sK2_skl)],[f53])).
% 0.13/5.44 fof(f60,plain,(
% 0.13/5.44 l1_orders_2(sK0_skl)),
% 0.13/5.44 inference(cnf_transformation,[status(thm)],[f54])).
% 0.13/5.44 fof(f61,plain,(
% 0.13/5.44 ~v3_struct_0(sK1_skl)),
% 0.13/5.44 inference(cnf_transformation,[status(thm)],[f54])).
% 0.13/5.44 fof(f66,plain,(
% 0.13/5.44 l1_orders_2(sK1_skl)),
% 0.13/5.44 inference(cnf_transformation,[status(thm)],[f54])).
% 0.13/5.44 fof(f67,plain,(
% 0.13/5.44 r2_hidden(sK2_skl,u1_struct_0(sK1_skl))),
% 0.13/5.44 inference(cnf_transformation,[status(thm)],[f54])).
% 0.13/5.44 fof(f68,plain,(
% 0.13/5.44 ~m1_subset_1(sK2_skl,u1_struct_0(k1_latsum_1(sK0_skl,sK1_skl)))),
% 0.13/5.44 inference(cnf_transformation,[status(thm)],[f54])).
% 0.13/5.44 fof(f77,plain,(
% 0.13/5.44 ![A]: (~l1_orders_2(A)|(![B]: (~l1_orders_2(B)|(![C]: ((~v1_orders_2(C)|~l1_orders_2(C))|(C=k1_latsum_1(A,B)<=>(u1_struct_0(C)=k2_xboole_0(u1_struct_0(A),u1_struct_0(B))&u1_orders_2(C)=k2_xboole_0(k2_xboole_0(u1_orders_2(A),u1_orders_2(B)),k7_relset_1(u1_struct_0(A),u1_struct_0(A),u1_struct_0(B),u1_struct_0(B),u1_orders_2(A),u1_orders_2(B))))))))))),
% 0.13/5.44 inference(pre_NNF_transformation,[status(thm)],[f7])).
% 0.13/5.44 fof(f78,plain,(
% 0.13/5.44 ![A]: (~l1_orders_2(A)|(![B]: (~l1_orders_2(B)|(![C]: ((~v1_orders_2(C)|~l1_orders_2(C))|((~C=k1_latsum_1(A,B)|(u1_struct_0(C)=k2_xboole_0(u1_struct_0(A),u1_struct_0(B))&u1_orders_2(C)=k2_xboole_0(k2_xboole_0(u1_orders_2(A),u1_orders_2(B)),k7_relset_1(u1_struct_0(A),u1_struct_0(A),u1_struct_0(B),u1_struct_0(B),u1_orders_2(A),u1_orders_2(B)))))&(C=k1_latsum_1(A,B)|(~u1_struct_0(C)=k2_xboole_0(u1_struct_0(A),u1_struct_0(B))|~u1_orders_2(C)=k2_xboole_0(k2_xboole_0(u1_orders_2(A),u1_orders_2(B)),k7_relset_1(u1_struct_0(A),u1_struct_0(A),u1_struct_0(B),u1_struct_0(B),u1_orders_2(A),u1_orders_2(B)))))))))))),
% 0.13/5.44 inference(NNF_transformation,[status(thm)],[f77])).
% 0.13/5.44 fof(f79,plain,(
% 0.13/5.44 ![X0,X1,X2]: (~l1_orders_2(X0)|~l1_orders_2(X1)|~v1_orders_2(X2)|~l1_orders_2(X2)|~X2=k1_latsum_1(X0,X1)|u1_struct_0(X2)=k2_xboole_0(u1_struct_0(X0),u1_struct_0(X1)))),
% 0.13/5.44 inference(cnf_transformation,[status(thm)],[f78])).
% 0.13/5.44 fof(f82,plain,(
% 0.13/5.44 ![A,B,C]: ((~C=k2_xboole_0(A,B)|(![D]: ((~r2_hidden(D,C)|(r2_hidden(D,A)|r2_hidden(D,B)))&(r2_hidden(D,C)|(~r2_hidden(D,A)&~r2_hidden(D,B))))))&(C=k2_xboole_0(A,B)|(?[D]: ((~r2_hidden(D,C)|(~r2_hidden(D,A)&~r2_hidden(D,B)))&(r2_hidden(D,C)|(r2_hidden(D,A)|r2_hidden(D,B)))))))),
% 0.13/5.44 inference(NNF_transformation,[status(thm)],[f8])).
% 0.13/5.44 fof(f83,plain,(
% 0.13/5.44 (![A,B,C]: (~C=k2_xboole_0(A,B)|((![D]: (~r2_hidden(D,C)|(r2_hidden(D,A)|r2_hidden(D,B))))&(![D]: (r2_hidden(D,C)|(~r2_hidden(D,A)&~r2_hidden(D,B)))))))&(![A,B,C]: (C=k2_xboole_0(A,B)|(?[D]: ((~r2_hidden(D,C)|(~r2_hidden(D,A)&~r2_hidden(D,B)))&(r2_hidden(D,C)|(r2_hidden(D,A)|r2_hidden(D,B)))))))),
% 0.13/5.44 inference(miniscoping,[status(thm)],[f82])).
% 0.13/5.44 fof(f84,plain,(
% 0.13/5.44 (![A,B,C]: (~C=k2_xboole_0(A,B)|((![D]: (~r2_hidden(D,C)|(r2_hidden(D,A)|r2_hidden(D,B))))&(![D]: (r2_hidden(D,C)|(~r2_hidden(D,A)&~r2_hidden(D,B)))))))&(![A,B,C]: (C=k2_xboole_0(A,B)|((~r2_hidden(sK3_skl(C,B,A),C)|(~r2_hidden(sK3_skl(C,B,A),A)&~r2_hidden(sK3_skl(C,B,A),B)))&(r2_hidden(sK3_skl(C,B,A),C)|(r2_hidden(sK3_skl(C,B,A),A)|r2_hidden(sK3_skl(C,B,A),B))))))),
% 0.13/5.44 inference(skolemize,[status(esa),new_symbols(skolem,[sK3_skl]),skolemize(D,sK3_skl(C,B,A))],[f83])).
% 0.13/5.44 fof(f87,plain,(
% 0.13/5.44 ![X0,X1,X2,X3]: (~X0=k2_xboole_0(X1,X2)|r2_hidden(X3,X0)|~r2_hidden(X3,X2))),
% 0.13/5.44 inference(cnf_transformation,[status(thm)],[f84])).
% 0.13/5.44 fof(f94,plain,(
% 0.13/5.44 ![A,B]: ((~l1_orders_2(A)|~l1_orders_2(B))|(v1_orders_2(k1_latsum_1(A,B))&l1_orders_2(k1_latsum_1(A,B))))),
% 0.13/5.44 inference(pre_NNF_transformation,[status(thm)],[f10])).
% 0.13/5.44 fof(f96,plain,(
% 0.13/5.44 ![X0,X1]: (~l1_orders_2(X0)|~l1_orders_2(X1)|l1_orders_2(k1_latsum_1(X0,X1)))),
% 0.13/5.44 inference(cnf_transformation,[status(thm)],[f94])).
% 0.13/5.44 fof(f117,plain,(
% 0.13/5.44 ![A,B]: (((~l1_orders_2(A)|v3_struct_0(B))|~l1_orders_2(B))|(~v3_struct_0(k1_latsum_1(A,B))&v1_orders_2(k1_latsum_1(A,B))))),
% 0.13/5.44 inference(pre_NNF_transformation,[status(thm)],[f29])).
% 0.13/5.44 fof(f119,plain,(
% 0.13/5.44 ![X0,X1]: (~l1_orders_2(X0)|v3_struct_0(X1)|~l1_orders_2(X1)|v1_orders_2(k1_latsum_1(X0,X1)))),
% 0.13/5.44 inference(cnf_transformation,[status(thm)],[f117])).
% 0.13/5.44 fof(f157,plain,(
% 0.13/5.44 ![A,B]: (~r2_hidden(A,B)|m1_subset_1(A,B))),
% 0.13/5.44 inference(pre_NNF_transformation,[status(thm)],[f45])).
% 0.13/5.44 fof(f158,plain,(
% 0.13/5.44 ![X0,X1]: (~r2_hidden(X0,X1)|m1_subset_1(X0,X1))),
% 0.13/5.44 inference(cnf_transformation,[status(thm)],[f157])).
% 0.13/5.44 fof(f179,plain,(
% 0.13/5.44 ![X0,X1]: (~l1_orders_2(X0)|~l1_orders_2(X1)|~v1_orders_2(k1_latsum_1(X0,X1))|~l1_orders_2(k1_latsum_1(X0,X1))|u1_struct_0(k1_latsum_1(X0,X1))=k2_xboole_0(u1_struct_0(X0),u1_struct_0(X1)))),
% 0.13/5.44 inference(destructive_equality_resolution,[status(thm)],[f79])).
% 0.13/5.44 fof(f183,plain,(
% 0.13/5.44 ![X0,X1,X2]: (r2_hidden(X0,k2_xboole_0(X1,X2))|~r2_hidden(X0,X2))),
% 0.13/5.44 inference(destructive_equality_resolution,[status(thm)],[f87])).
% 0.13/5.44 fof(f185,plain,(
% 0.13/5.44 ~r2_hidden(sK2_skl,u1_struct_0(k1_latsum_1(sK0_skl,sK1_skl)))),
% 0.13/5.44 inference(resolution,[status(thm)],[f158,f68])).
% 0.13/5.44 fof(f195,plain,(
% 0.13/5.44 ![X0,X1]: (~l1_orders_2(X0)|~l1_orders_2(X1)|~v1_orders_2(k1_latsum_1(X0,X1))|u1_struct_0(k1_latsum_1(X0,X1))=k2_xboole_0(u1_struct_0(X0),u1_struct_0(X1)))),
% 0.13/5.44 inference(forward_subsumption_resolution,[status(thm)],[f179,f96])).
% 0.13/5.44 fof(f196,plain,(
% 0.13/5.44 ![X0,X1]: (~l1_orders_2(X0)|~l1_orders_2(X1)|u1_struct_0(k1_latsum_1(X0,X1))=k2_xboole_0(u1_struct_0(X0),u1_struct_0(X1))|~l1_orders_2(X0)|v3_struct_0(X1)|~l1_orders_2(X1))),
% 0.13/5.45 inference(resolution,[status(thm)],[f195,f119])).
% 0.13/5.45 fof(f197,plain,(
% 0.13/5.45 ![X0,X1]: (~l1_orders_2(X0)|~l1_orders_2(X1)|u1_struct_0(k1_latsum_1(X0,X1))=k2_xboole_0(u1_struct_0(X0),u1_struct_0(X1))|v3_struct_0(X1))),
% 0.13/5.45 inference(duplicate_literals_removal,[status(thm)],[f196])).
% 0.13/5.45 fof(f203,plain,(
% 0.13/5.45 ![X0]: (~l1_orders_2(X0)|u1_struct_0(k1_latsum_1(X0,sK1_skl))=k2_xboole_0(u1_struct_0(X0),u1_struct_0(sK1_skl))|v3_struct_0(sK1_skl))),
% 0.13/5.45 inference(resolution,[status(thm)],[f197,f66])).
% 0.13/5.45 fof(f212,definition,(
% 0.13/5.45 ![X0]: (sQ2_spl <=> (~l1_orders_2(X0)|u1_struct_0(k1_latsum_1(X0,sK1_skl))=k2_xboole_0(u1_struct_0(X0),u1_struct_0(sK1_skl))))),
% 0.13/5.45 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.13/5.45 fof(f213,plain,(
% 0.13/5.45 ![X0]: (~l1_orders_2(X0)|u1_struct_0(k1_latsum_1(X0,sK1_skl))=k2_xboole_0(u1_struct_0(X0),u1_struct_0(sK1_skl))|~sQ2_spl)),
% 0.13/5.45 inference(component_clause,[status(thm)],[f212])).
% 0.13/5.45 fof(f215,definition,(
% 0.13/5.45 sQ3_spl <=> (v3_struct_0(sK1_skl))),
% 0.13/5.45 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 0.13/5.45 fof(f216,plain,(
% 0.13/5.45 v3_struct_0(sK1_skl)|~sQ3_spl),
% 0.13/5.45 inference(component_clause,[status(thm)],[f215])).
% 0.13/5.45 fof(f218,plain,(
% 0.13/5.45 sQ2_spl|sQ3_spl),
% 0.13/5.45 inference(split_clause,[status(thm)],[f203,f212,f215])).
% 0.13/5.45 fof(f233,plain,(
% 0.13/5.45 u1_struct_0(k1_latsum_1(sK0_skl,sK1_skl))=k2_xboole_0(u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))|~sQ2_spl),
% 0.13/5.45 inference(resolution,[status(thm)],[f213,f60])).
% 0.13/5.45 fof(f264,plain,(
% 0.13/5.45 $false|~sQ3_spl),
% 0.13/5.45 inference(forward_subsumption_resolution,[status(thm)],[f216,f61])).
% 0.13/5.45 fof(f265,plain,(
% 0.13/5.45 ~sQ3_spl),
% 0.13/5.45 inference(contradiction_clause,[status(thm)],[f264])).
% 0.13/5.45 fof(f339,plain,(
% 0.13/5.45 ![X0]: (r2_hidden(sK2_skl,k2_xboole_0(X0,u1_struct_0(sK1_skl))))),
% 0.13/5.45 inference(resolution,[status(thm)],[f183,f67])).
% 0.13/5.45 fof(f345,plain,(
% 0.13/5.45 r2_hidden(sK2_skl,u1_struct_0(k1_latsum_1(sK0_skl,sK1_skl)))|~sQ2_spl),
% 0.13/5.45 inference(paramodulation,[status(thm)],[f233,f339])).
% 0.13/5.45 fof(f350,plain,(
% 0.13/5.45 $false|~sQ2_spl),
% 0.13/5.45 inference(forward_subsumption_resolution,[status(thm)],[f345,f185])).
% 0.13/5.45 fof(f351,plain,(
% 0.13/5.45 ~sQ2_spl),
% 0.13/5.45 inference(contradiction_clause,[status(thm)],[f350])).
% 0.13/5.45 fof(f352,plain,(
% 0.13/5.45 $false),
% 0.13/5.45 inference(sat_refutation,[status(thm)],[f218,f265,f351])).
% 0.13/5.45 % SZS output end CNFRefutation for theBenchmark.p
% 0.13/5.47 % Elapsed time: 0.101346 seconds
% 0.13/5.47 % CPU time: 0.497504 seconds
% 0.13/5.47 % Total memory used: 113.391 MB
% 0.13/5.47 % Net memory used: 112.828 MB
%------------------------------------------------------------------------------