%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SEU407+1 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n009.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:32 PM UTC 2026
% Result : Theorem 0.17s 0.83s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SEU407+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.07 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.17/0.42 % Computer : n009.cluster.edu
% 0.17/0.42 % Model : x86_64 x86_64
% 0.17/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.42 % Memory : 8046.5625MB
% 0.17/0.42 % OS : Linux 6.8.0-71-generic
% 0.17/0.42 % CPULimit : 300
% 0.17/0.42 % WCLimit : 300
% 0.17/0.42 % DateTime : Mon Sep 21 06:20:43 UTC 2026
% 0.17/0.42 % CPUTime :
% 0.17/0.44 % Drodi V4.1.1
% 0.17/0.83 % Refutation found
% 0.17/0.83 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.17/0.83 % SZS output start CNFRefutation for theBenchmark
% 0.17/0.83 fof(f1,conjecture,(
% 0.17/0.83 (! [A] :( ( ~ v3_struct_0(A)& l1_orders_2(A) )=> (! [B] :( ( ~ v3_struct_0(B)& l1_orders_2(B) )=> (! [C] :( m1_subset_1(C,u1_struct_0(k1_latsum_1(A,B)))=> ( r2_hidden(C,u1_struct_0(A))| r2_hidden(C,k4_xboole_0(u1_struct_0(B),u1_struct_0(A))) ) ) )) )) )),
% 0.17/0.83 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.17/0.83 fof(f2,negated_conjecture,(
% 0.17/0.83 ~((! [A] :( ( ~ v3_struct_0(A)& l1_orders_2(A) )=> (! [B] :( ( ~ v3_struct_0(B)& l1_orders_2(B) )=> (! [C] :( m1_subset_1(C,u1_struct_0(k1_latsum_1(A,B)))=> ( r2_hidden(C,u1_struct_0(A))| r2_hidden(C,k4_xboole_0(u1_struct_0(B),u1_struct_0(A))) ) ) )) )) ))),
% 0.17/0.83 inference(negated_conjecture,[status(cth)],[f1])).
% 0.17/0.83 fof(f6,axiom,(
% 0.17/0.83 (! [A,B] : k2_xboole_0(A,B) = k2_xboole_0(B,A) )),
% 0.17/0.83 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.17/0.83 fof(f7,axiom,(
% 0.17/0.83 (! [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.17/0.83 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.17/0.83 fof(f8,axiom,(
% 0.17/0.83 (! [A,B,C] :( C = k2_xboole_0(A,B)<=> (! [D] :( r2_hidden(D,C)<=> ( r2_hidden(D,A)| r2_hidden(D,B) ) ) )) )),
% 0.17/0.83 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.17/0.83 fof(f10,axiom,(
% 0.17/0.83 (! [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.17/0.83 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.17/0.83 fof(f18,axiom,(
% 0.17/0.83 (! [A] :( l1_orders_2(A)=> l1_struct_0(A) ) )),
% 0.17/0.83 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.17/0.83 fof(f31,axiom,(
% 0.17/0.83 (! [A] :( ( ~ v3_struct_0(A)& l1_struct_0(A) )=> ~ v1_xboole_0(u1_struct_0(A)) ) )),
% 0.17/0.83 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.17/0.83 fof(f34,axiom,(
% 0.17/0.83 (! [A,B] :( ~ v1_xboole_0(A)=> ~ v1_xboole_0(k2_xboole_0(A,B)) ) )),
% 0.17/0.83 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.17/0.83 fof(f47,axiom,(
% 0.17/0.83 (! [A,B] :( m1_subset_1(A,B)=> ( v1_xboole_0(B)| r2_hidden(A,B) ) ) )),
% 0.17/0.83 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.17/0.83 fof(f48,axiom,(
% 0.17/0.83 (! [A,B] : k2_xboole_0(A,k4_xboole_0(B,A)) = k2_xboole_0(A,B) )),
% 0.17/0.83 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.17/0.83 fof(f57,plain,(
% 0.17/0.83 (?[A]: ((~v3_struct_0(A)&l1_orders_2(A))&(?[B]: ((~v3_struct_0(B)&l1_orders_2(B))&(?[C]: (m1_subset_1(C,u1_struct_0(k1_latsum_1(A,B)))&(~r2_hidden(C,u1_struct_0(A))&~r2_hidden(C,k4_xboole_0(u1_struct_0(B),u1_struct_0(A))))))))))),
% 0.17/0.83 inference(pre_NNF_transformation,[status(thm)],[f2])).
% 0.17/0.83 fof(f58,plain,(
% 0.17/0.83 ((~v3_struct_0(sK0_skl)&l1_orders_2(sK0_skl))&((~v3_struct_0(sK1_skl)&l1_orders_2(sK1_skl))&(m1_subset_1(sK2_skl,u1_struct_0(k1_latsum_1(sK0_skl,sK1_skl)))&(~r2_hidden(sK2_skl,u1_struct_0(sK0_skl))&~r2_hidden(sK2_skl,k4_xboole_0(u1_struct_0(sK1_skl),u1_struct_0(sK0_skl)))))))),
% 0.17/0.83 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)],[f57])).
% 0.17/0.83 fof(f59,plain,(
% 0.17/0.83 ~v3_struct_0(sK0_skl)),
% 0.17/0.83 inference(cnf_transformation,[status(thm)],[f58])).
% 0.17/0.83 fof(f60,plain,(
% 0.17/0.83 l1_orders_2(sK0_skl)),
% 0.17/0.83 inference(cnf_transformation,[status(thm)],[f58])).
% 0.17/0.83 fof(f62,plain,(
% 0.17/0.83 l1_orders_2(sK1_skl)),
% 0.17/0.83 inference(cnf_transformation,[status(thm)],[f58])).
% 0.17/0.83 fof(f63,plain,(
% 0.17/0.83 m1_subset_1(sK2_skl,u1_struct_0(k1_latsum_1(sK0_skl,sK1_skl)))),
% 0.17/0.83 inference(cnf_transformation,[status(thm)],[f58])).
% 0.17/0.83 fof(f64,plain,(
% 0.17/0.83 ~r2_hidden(sK2_skl,u1_struct_0(sK0_skl))),
% 0.17/0.83 inference(cnf_transformation,[status(thm)],[f58])).
% 0.17/0.83 fof(f65,plain,(
% 0.17/0.83 ~r2_hidden(sK2_skl,k4_xboole_0(u1_struct_0(sK1_skl),u1_struct_0(sK0_skl)))),
% 0.17/0.83 inference(cnf_transformation,[status(thm)],[f58])).
% 0.17/0.83 fof(f73,plain,(
% 0.17/0.83 ![X0,X1]: (k2_xboole_0(X0,X1)=k2_xboole_0(X1,X0))),
% 0.17/0.83 inference(cnf_transformation,[status(thm)],[f6])).
% 0.17/0.83 fof(f74,plain,(
% 0.17/0.83 ![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.17/0.83 inference(pre_NNF_transformation,[status(thm)],[f7])).
% 0.17/0.83 fof(f75,plain,(
% 0.17/0.83 ![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.17/0.83 inference(NNF_transformation,[status(thm)],[f74])).
% 0.17/0.83 fof(f76,plain,(
% 0.17/0.83 ![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.17/0.83 inference(cnf_transformation,[status(thm)],[f75])).
% 0.17/0.83 fof(f79,plain,(
% 0.17/0.83 ![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.17/0.83 inference(NNF_transformation,[status(thm)],[f8])).
% 0.17/0.83 fof(f80,plain,(
% 0.17/0.83 (![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.17/0.83 inference(miniscoping,[status(thm)],[f79])).
% 0.17/0.83 fof(f81,plain,(
% 0.17/0.83 (![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.17/0.83 inference(skolemize,[status(esa),new_symbols(skolem,[sK3_skl]),skolemize(D,sK3_skl(C,B,A))],[f80])).
% 0.17/0.83 fof(f82,plain,(
% 0.17/0.83 ![X0,X1,X2,X3]: (~X0=k2_xboole_0(X1,X2)|~r2_hidden(X3,X0)|r2_hidden(X3,X1)|r2_hidden(X3,X2))),
% 0.17/0.83 inference(cnf_transformation,[status(thm)],[f81])).
% 0.17/0.83 fof(f91,plain,(
% 0.17/0.83 ![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.17/0.83 inference(pre_NNF_transformation,[status(thm)],[f10])).
% 0.17/0.83 fof(f92,plain,(
% 0.17/0.83 ![X0,X1]: (~l1_orders_2(X0)|~l1_orders_2(X1)|v1_orders_2(k1_latsum_1(X0,X1)))),
% 0.17/0.83 inference(cnf_transformation,[status(thm)],[f91])).
% 0.17/0.83 fof(f93,plain,(
% 0.17/0.83 ![X0,X1]: (~l1_orders_2(X0)|~l1_orders_2(X1)|l1_orders_2(k1_latsum_1(X0,X1)))),
% 0.17/0.83 inference(cnf_transformation,[status(thm)],[f91])).
% 0.17/0.83 fof(f98,plain,(
% 0.17/0.83 ![A]: (~l1_orders_2(A)|l1_struct_0(A))),
% 0.17/0.83 inference(pre_NNF_transformation,[status(thm)],[f18])).
% 0.17/0.83 fof(f99,plain,(
% 0.17/0.83 ![X0]: (~l1_orders_2(X0)|l1_struct_0(X0))),
% 0.17/0.83 inference(cnf_transformation,[status(thm)],[f98])).
% 0.17/0.83 fof(f117,plain,(
% 0.17/0.83 ![A]: ((v3_struct_0(A)|~l1_struct_0(A))|~v1_xboole_0(u1_struct_0(A)))),
% 0.17/0.83 inference(pre_NNF_transformation,[status(thm)],[f31])).
% 0.17/0.83 fof(f118,plain,(
% 0.17/0.83 ![X0]: (v3_struct_0(X0)|~l1_struct_0(X0)|~v1_xboole_0(u1_struct_0(X0)))),
% 0.17/0.83 inference(cnf_transformation,[status(thm)],[f117])).
% 0.17/0.83 fof(f123,plain,(
% 0.17/0.83 ![A,B]: (v1_xboole_0(A)|~v1_xboole_0(k2_xboole_0(A,B)))),
% 0.17/0.83 inference(pre_NNF_transformation,[status(thm)],[f34])).
% 0.17/0.83 fof(f124,plain,(
% 0.17/0.83 ![A]: (v1_xboole_0(A)|(![B]: ~v1_xboole_0(k2_xboole_0(A,B))))),
% 0.17/0.83 inference(miniscoping,[status(thm)],[f123])).
% 0.17/0.83 fof(f125,plain,(
% 0.17/0.83 ![X0,X1]: (v1_xboole_0(X0)|~v1_xboole_0(k2_xboole_0(X0,X1)))),
% 0.17/0.83 inference(cnf_transformation,[status(thm)],[f124])).
% 0.17/0.83 fof(f156,plain,(
% 0.17/0.83 ![A,B]: (~m1_subset_1(A,B)|(v1_xboole_0(B)|r2_hidden(A,B)))),
% 0.17/0.83 inference(pre_NNF_transformation,[status(thm)],[f47])).
% 0.17/0.83 fof(f157,plain,(
% 0.17/0.83 ![X0,X1]: (~m1_subset_1(X0,X1)|v1_xboole_0(X1)|r2_hidden(X0,X1))),
% 0.17/0.83 inference(cnf_transformation,[status(thm)],[f156])).
% 0.17/0.83 fof(f158,plain,(
% 0.17/0.83 ![X0,X1]: (k2_xboole_0(X0,k4_xboole_0(X1,X0))=k2_xboole_0(X0,X1))),
% 0.17/0.83 inference(cnf_transformation,[status(thm)],[f48])).
% 0.17/0.83 fof(f179,plain,(
% 0.17/0.83 ![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.17/0.83 inference(destructive_equality_resolution,[status(thm)],[f76])).
% 0.17/0.83 fof(f181,plain,(
% 0.17/0.83 ![X0,X1,X2]: (~r2_hidden(X0,k2_xboole_0(X1,X2))|r2_hidden(X0,X1)|r2_hidden(X0,X2))),
% 0.17/0.83 inference(destructive_equality_resolution,[status(thm)],[f82])).
% 0.17/0.83 fof(f185,plain,(
% 0.17/0.83 ![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)))),
% 0.17/0.83 inference(backward_subsumption_resolution,[status(thm)],[f179,f92])).
% 0.17/0.83 fof(f187,plain,(
% 0.17/0.83 ![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)))),
% 0.17/0.83 inference(forward_subsumption_resolution,[status(thm)],[f185,f93])).
% 0.17/0.83 fof(f190,plain,(
% 0.17/0.83 v1_xboole_0(u1_struct_0(k1_latsum_1(sK0_skl,sK1_skl)))|r2_hidden(sK2_skl,u1_struct_0(k1_latsum_1(sK0_skl,sK1_skl)))),
% 0.17/0.83 inference(resolution,[status(thm)],[f157,f63])).
% 0.17/0.83 fof(f197,plain,(
% 0.17/0.83 l1_struct_0(sK0_skl)),
% 0.17/0.83 inference(resolution,[status(thm)],[f99,f60])).
% 0.17/0.83 fof(f206,plain,(
% 0.17/0.83 ![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)))),
% 0.17/0.83 inference(resolution,[status(thm)],[f187,f62])).
% 0.17/0.83 fof(f207,plain,(
% 0.17/0.83 ![X0]: (~l1_orders_2(X0)|u1_struct_0(k1_latsum_1(X0,sK0_skl))=k2_xboole_0(u1_struct_0(X0),u1_struct_0(sK0_skl)))),
% 0.17/0.83 inference(resolution,[status(thm)],[f187,f60])).
% 0.17/0.83 fof(f285,plain,(
% 0.17/0.83 ![X0,X1,X2]: (~r2_hidden(X0,k2_xboole_0(X1,X2))|r2_hidden(X0,X1)|r2_hidden(X0,k4_xboole_0(X2,X1)))),
% 0.17/0.83 inference(paramodulation,[status(thm)],[f158,f181])).
% 0.17/0.83 fof(f293,plain,(
% 0.17/0.83 u1_struct_0(k1_latsum_1(sK0_skl,sK1_skl))=k2_xboole_0(u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))),
% 0.17/0.83 inference(resolution,[status(thm)],[f206,f60])).
% 0.17/0.83 fof(f302,plain,(
% 0.17/0.83 u1_struct_0(k1_latsum_1(sK1_skl,sK0_skl))=k2_xboole_0(u1_struct_0(sK1_skl),u1_struct_0(sK0_skl))),
% 0.17/0.83 inference(resolution,[status(thm)],[f207,f62])).
% 0.17/0.83 fof(f415,plain,(
% 0.17/0.83 u1_struct_0(k1_latsum_1(sK0_skl,sK1_skl))=k2_xboole_0(u1_struct_0(sK1_skl),u1_struct_0(sK0_skl))),
% 0.17/0.83 inference(paramodulation,[status(thm)],[f73,f293])).
% 0.17/0.83 fof(f418,plain,(
% 0.17/0.83 v1_xboole_0(u1_struct_0(sK0_skl))|~v1_xboole_0(u1_struct_0(k1_latsum_1(sK0_skl,sK1_skl)))),
% 0.17/0.83 inference(paramodulation,[status(thm)],[f293,f125])).
% 0.17/0.83 fof(f427,plain,(
% 0.17/0.83 u1_struct_0(k1_latsum_1(sK1_skl,sK0_skl))=k2_xboole_0(u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))),
% 0.17/0.83 inference(backward_demodulation,[status(thm)],[f433,f293])).
% 0.17/0.83 fof(f429,plain,(
% 0.17/0.83 v1_xboole_0(u1_struct_0(k1_latsum_1(sK0_skl,sK1_skl)))|r2_hidden(sK2_skl,u1_struct_0(k1_latsum_1(sK1_skl,sK0_skl)))),
% 0.17/0.83 inference(backward_demodulation,[status(thm)],[f433,f190])).
% 0.17/0.83 fof(f433,plain,(
% 0.17/0.83 u1_struct_0(k1_latsum_1(sK0_skl,sK1_skl))=u1_struct_0(k1_latsum_1(sK1_skl,sK0_skl))),
% 0.17/0.83 inference(forward_demodulation,[status(thm)],[f302,f415])).
% 0.17/0.83 fof(f436,plain,(
% 0.17/0.83 v1_xboole_0(u1_struct_0(sK0_skl))|~v1_xboole_0(u1_struct_0(k1_latsum_1(sK1_skl,sK0_skl)))),
% 0.17/0.83 inference(forward_demodulation,[status(thm)],[f433,f418])).
% 0.17/0.83 fof(f446,plain,(
% 0.17/0.83 v1_xboole_0(u1_struct_0(k1_latsum_1(sK1_skl,sK0_skl)))|r2_hidden(sK2_skl,u1_struct_0(k1_latsum_1(sK1_skl,sK0_skl)))),
% 0.17/0.83 inference(forward_demodulation,[status(thm)],[f433,f429])).
% 0.17/0.83 fof(f707,plain,(
% 0.17/0.83 ~r2_hidden(sK2_skl,k2_xboole_0(u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)))|r2_hidden(sK2_skl,u1_struct_0(sK0_skl))),
% 0.17/0.83 inference(resolution,[status(thm)],[f285,f65])).
% 0.17/0.83 fof(f714,plain,(
% 0.17/0.83 ~r2_hidden(sK2_skl,u1_struct_0(k1_latsum_1(sK1_skl,sK0_skl)))|r2_hidden(sK2_skl,u1_struct_0(sK0_skl))),
% 0.17/0.87 inference(forward_demodulation,[status(thm)],[f427,f707])).
% 0.17/0.87 fof(f715,plain,(
% 0.17/0.87 v1_xboole_0(u1_struct_0(k1_latsum_1(sK1_skl,sK0_skl)))),
% 0.17/0.87 inference(backward_subsumption_resolution,[status(thm)],[f446,f716])).
% 0.17/0.87 fof(f716,plain,(
% 0.17/0.87 ~r2_hidden(sK2_skl,u1_struct_0(k1_latsum_1(sK1_skl,sK0_skl)))),
% 0.17/0.87 inference(forward_subsumption_resolution,[status(thm)],[f714,f64])).
% 0.17/0.87 fof(f717,plain,(
% 0.17/0.87 v1_xboole_0(u1_struct_0(sK0_skl))),
% 0.17/0.87 inference(backward_subsumption_resolution,[status(thm)],[f436,f715])).
% 0.17/0.87 fof(f782,plain,(
% 0.17/0.87 v3_struct_0(sK0_skl)|~l1_struct_0(sK0_skl)),
% 0.17/0.87 inference(resolution,[status(thm)],[f717,f118])).
% 0.17/0.87 fof(f789,plain,(
% 0.17/0.87 ~l1_struct_0(sK0_skl)),
% 0.17/0.87 inference(forward_subsumption_resolution,[status(thm)],[f782,f59])).
% 0.17/0.87 fof(f790,plain,(
% 0.17/0.87 $false),
% 0.17/0.87 inference(backward_subsumption_resolution,[status(thm)],[f197,f789])).
% 0.17/0.87 % SZS output end CNFRefutation for theBenchmark.p
% 0.42/0.89 % Elapsed time: 0.448312 seconds
% 0.42/0.89 % CPU time: 3.042495 seconds
% 0.42/0.89 % Total memory used: 141.214 MB
% 0.42/0.89 % Net memory used: 139.203 MB
%------------------------------------------------------------------------------