%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SEU408+2 : 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 : n011.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 74.68s 10.48s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SEU408+2 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.57 % Computer : n011.cluster.edu
% 0.08/0.57 % Model : x86_64 x86_64
% 0.08/0.57 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.57 % Memory : 8046.5625MB
% 0.08/0.57 % OS : Linux 6.8.0-71-generic
% 0.08/0.57 % CPULimit : 300
% 0.08/0.57 % WCLimit : 300
% 0.08/0.57 % DateTime : Mon Sep 21 06:21:12 UTC 2026
% 0.08/0.57 % CPUTime :
% 0.57/1.03 % Drodi V4.1.1
% 74.68/10.48 % Refutation found
% 74.68/10.48 % SZS status Theorem for theBenchmark: Theorem is valid
% 74.68/10.48 % SZS output start CNFRefutation for theBenchmark
% 74.68/10.48 fof(f30,axiom,(
% 74.68/10.48 (! [A,B,C] :( C = k2_xboole_0(A,B)<=> (! [D] :( r2_hidden(D,C)<=> ( r2_hidden(D,A)| r2_hidden(D,B) ) ) )) )),
% 74.68/10.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 74.68/10.48 fof(f444,axiom,(
% 74.68/10.48 ((! [A,B] :( r2_hidden(A,B)=> m1_subset_1(A,B) ) ))),
% 74.68/10.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 74.68/10.48 fof(f4433,axiom,(
% 74.68/10.48 (! [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)) ) ) )),
% 74.68/10.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 74.68/10.48 fof(f4436,axiom,(
% 74.68/10.48 (! [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))) ) ) ) )) )) )),
% 74.68/10.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 74.68/10.48 fof(f4448,conjecture,(
% 74.68/10.48 (! [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))) ) )) )) )),
% 74.68/10.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 74.68/10.48 fof(f4449,negated_conjecture,(
% 74.68/10.48 ~((! [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))) ) )) )) ))),
% 74.68/10.48 inference(negated_conjecture,[status(cth)],[f4448])).
% 74.68/10.48 fof(f4544,plain,(
% 74.68/10.48 ![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)))))))),
% 74.68/10.48 inference(NNF_transformation,[status(thm)],[f30])).
% 74.68/10.48 fof(f4545,plain,(
% 74.68/10.48 (![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)))))))),
% 74.68/10.48 inference(miniscoping,[status(thm)],[f4544])).
% 74.68/10.48 fof(f4546,plain,(
% 74.68/10.48 (![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(sK23_skl(C,B,A),C)|(~r2_hidden(sK23_skl(C,B,A),A)&~r2_hidden(sK23_skl(C,B,A),B)))&(r2_hidden(sK23_skl(C,B,A),C)|(r2_hidden(sK23_skl(C,B,A),A)|r2_hidden(sK23_skl(C,B,A),B))))))),
% 74.68/10.48 inference(skolemize,[status(esa),new_symbols(skolem,[sK23_skl]),skolemize(D,sK23_skl(C,B,A))],[f4545])).
% 74.68/10.48 fof(f4549,plain,(
% 74.68/10.48 ![X0,X1,X2,X3]: (~X0=k2_xboole_0(X1,X2)|r2_hidden(X3,X0)|~r2_hidden(X3,X2))),
% 74.68/10.48 inference(cnf_transformation,[status(thm)],[f4546])).
% 74.68/10.48 fof(f5554,plain,(
% 74.68/10.48 ![A,B]: (~r2_hidden(A,B)|m1_subset_1(A,B))),
% 74.68/10.48 inference(pre_NNF_transformation,[status(thm)],[f444])).
% 74.68/10.48 fof(f5555,plain,(
% 74.68/10.48 ![X0,X1]: (~r2_hidden(X0,X1)|m1_subset_1(X0,X1))),
% 74.68/10.48 inference(cnf_transformation,[status(thm)],[f5554])).
% 74.68/10.48 fof(f18505,plain,(
% 74.68/10.48 ![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))))),
% 74.68/10.48 inference(pre_NNF_transformation,[status(thm)],[f4433])).
% 74.68/10.48 fof(f18506,plain,(
% 74.68/10.48 ![X0,X1]: (~l1_orders_2(X0)|~l1_orders_2(X1)|v1_orders_2(k1_latsum_1(X0,X1)))),
% 74.68/10.48 inference(cnf_transformation,[status(thm)],[f18505])).
% 74.68/10.48 fof(f18507,plain,(
% 74.68/10.48 ![X0,X1]: (~l1_orders_2(X0)|~l1_orders_2(X1)|l1_orders_2(k1_latsum_1(X0,X1)))),
% 74.68/10.48 inference(cnf_transformation,[status(thm)],[f18505])).
% 74.68/10.48 fof(f18524,plain,(
% 74.68/10.48 ![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))))))))))),
% 74.68/10.48 inference(pre_NNF_transformation,[status(thm)],[f4436])).
% 74.68/10.48 fof(f18525,plain,(
% 74.68/10.48 ![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)))))))))))),
% 74.68/10.48 inference(NNF_transformation,[status(thm)],[f18524])).
% 74.68/10.48 fof(f18526,plain,(
% 74.68/10.48 ![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)))),
% 74.68/10.48 inference(cnf_transformation,[status(thm)],[f18525])).
% 74.68/10.48 fof(f18560,plain,(
% 74.68/10.48 (?[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)))))))))),
% 74.68/10.48 inference(pre_NNF_transformation,[status(thm)],[f4449])).
% 74.68/10.48 fof(f18561,plain,(
% 74.68/10.48 ((((((~v3_struct_0(sK1191_skl)&v2_orders_2(sK1191_skl))&v3_orders_2(sK1191_skl))&v4_orders_2(sK1191_skl))&v1_lattice3(sK1191_skl))&l1_orders_2(sK1191_skl))&((((((~v3_struct_0(sK1192_skl)&v2_orders_2(sK1192_skl))&v3_orders_2(sK1192_skl))&v4_orders_2(sK1192_skl))&v1_lattice3(sK1192_skl))&l1_orders_2(sK1192_skl))&(r2_hidden(sK1193_skl,u1_struct_0(sK1192_skl))&~m1_subset_1(sK1193_skl,u1_struct_0(k1_latsum_1(sK1191_skl,sK1192_skl))))))),
% 74.68/10.48 inference(skolemize,[status(esa),new_symbols(skolem,[sK1191_skl,sK1192_skl,sK1193_skl]),skolemize(A,sK1191_skl),skolemize(B,sK1192_skl),skolemize(C,sK1193_skl)],[f18560])).
% 74.68/10.48 fof(f18567,plain,(
% 74.68/10.48 l1_orders_2(sK1191_skl)),
% 74.68/10.48 inference(cnf_transformation,[status(thm)],[f18561])).
% 74.68/10.48 fof(f18573,plain,(
% 74.68/10.48 l1_orders_2(sK1192_skl)),
% 74.68/10.48 inference(cnf_transformation,[status(thm)],[f18561])).
% 74.68/10.48 fof(f18574,plain,(
% 74.68/10.48 r2_hidden(sK1193_skl,u1_struct_0(sK1192_skl))),
% 74.68/10.48 inference(cnf_transformation,[status(thm)],[f18561])).
% 74.68/10.48 fof(f18575,plain,(
% 74.68/10.48 ~m1_subset_1(sK1193_skl,u1_struct_0(k1_latsum_1(sK1191_skl,sK1192_skl)))),
% 74.68/10.48 inference(cnf_transformation,[status(thm)],[f18561])).
% 74.68/10.48 fof(f22165,plain,(
% 74.68/10.48 ![X0,X1,X2]: (r2_hidden(X0,k2_xboole_0(X1,X2))|~r2_hidden(X0,X2))),
% 74.68/10.48 inference(destructive_equality_resolution,[status(thm)],[f4549])).
% 74.68/10.48 fof(f23024,plain,(
% 74.68/10.48 ![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)))),
% 74.68/10.48 inference(destructive_equality_resolution,[status(thm)],[f18526])).
% 74.68/10.48 fof(f23221,plain,(
% 74.68/10.48 ~r2_hidden(sK1193_skl,u1_struct_0(k1_latsum_1(sK1191_skl,sK1192_skl)))),
% 74.68/10.48 inference(resolution,[status(thm)],[f18575,f5555])).
% 74.68/10.48 fof(f23222,plain,(
% 74.68/10.48 ![X0,X1]: (~l1_orders_2(X0)|~l1_orders_2(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)))),
% 74.68/10.48 inference(forward_subsumption_resolution,[status(thm)],[f23024,f18506])).
% 74.68/10.48 fof(f23223,plain,(
% 74.68/10.48 ![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)|~l1_orders_2(X1))),
% 74.68/10.48 inference(resolution,[status(thm)],[f23222,f18507])).
% 74.68/10.48 fof(f23224,plain,(
% 74.68/10.48 ![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)))),
% 74.68/10.48 inference(duplicate_literals_removal,[status(thm)],[f23223])).
% 75.56/10.57 fof(f23226,plain,(
% 75.56/10.57 ![X0]: (~l1_orders_2(X0)|u1_struct_0(k1_latsum_1(X0,sK1192_skl))=k2_xboole_0(u1_struct_0(X0),u1_struct_0(sK1192_skl)))),
% 75.56/10.57 inference(resolution,[status(thm)],[f23224,f18573])).
% 75.56/10.57 fof(f23373,plain,(
% 75.56/10.57 u1_struct_0(k1_latsum_1(sK1191_skl,sK1192_skl))=k2_xboole_0(u1_struct_0(sK1191_skl),u1_struct_0(sK1192_skl))),
% 75.56/10.57 inference(resolution,[status(thm)],[f23226,f18567])).
% 75.56/10.57 fof(f25752,plain,(
% 75.56/10.57 ![X0]: (r2_hidden(sK1193_skl,k2_xboole_0(X0,u1_struct_0(sK1192_skl))))),
% 75.56/10.57 inference(resolution,[status(thm)],[f18574,f22165])).
% 75.56/10.57 fof(f40050,plain,(
% 75.56/10.57 r2_hidden(sK1193_skl,u1_struct_0(k1_latsum_1(sK1191_skl,sK1192_skl)))),
% 75.56/10.57 inference(paramodulation,[status(thm)],[f23373,f25752])).
% 75.56/10.57 fof(f40061,plain,(
% 75.56/10.57 $false),
% 75.56/10.57 inference(forward_subsumption_resolution,[status(thm)],[f40050,f23221])).
% 75.56/10.57 % SZS output end CNFRefutation for theBenchmark.p
% 2.95/10.61 % Elapsed time: 10.017021 seconds
% 2.95/10.61 % CPU time: 75.791674 seconds
% 2.95/10.61 % Total memory used: 1.060 GB
% 2.95/10.61 % Net memory used: 1.005 GB
%------------------------------------------------------------------------------