%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWV926-1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n003.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:53:22 PM UTC 2026
% Result : Unsatisfiable 20.85s 3.30s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SWV926-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.15/0.42 % Computer : n003.cluster.edu
% 0.15/0.42 % Model : x86_64 x86_64
% 0.15/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.42 % Memory : 8046.5625MB
% 0.15/0.42 % OS : Linux 6.8.0-71-generic
% 0.15/0.42 % CPULimit : 300
% 0.15/0.42 % WCLimit : 300
% 0.15/0.42 % DateTime : Mon Sep 21 09:33:32 UTC 2026
% 0.15/0.42 % CPUTime :
% 0.27/0.58 % Drodi V4.1.1
% 20.85/3.30 % Refutation found
% 20.85/3.30 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 20.85/3.30 % SZS output start CNFRefutation for theBenchmark
% 20.85/3.30 fof(f399,axiom,(
% 20.85/3.30 (![V_A,V_C,T_a,V_B]: (( c_lessequals(V_A,V_C,tc_fun(T_a,tc_bool))| ~ c_lessequals(V_B,V_C,tc_fun(T_a,tc_bool))| ~ c_lessequals(V_A,V_B,tc_fun(T_a,tc_bool)) ) ))),
% 20.85/3.30 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 20.85/3.30 fof(f408,axiom,(
% 20.85/3.30 (![V_B,V_C,T_a,V_A]: (( c_lessequals(V_B,V_C,tc_fun(T_a,tc_bool))| ~ c_lessequals(c_Lattices_Oupper__semilattice__class_Osup(V_A,V_B,tc_fun(T_a,tc_bool)),V_C,tc_fun(T_a,tc_bool)) ) ))),
% 20.85/3.30 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 20.85/3.30 fof(f421,axiom,(
% 20.85/3.30 (![V_A,V_B,T_a]: (( c_Lattices_Oupper__semilattice__class_Osup(V_A,V_B,tc_fun(T_a,tc_bool)) = V_B| ~ c_lessequals(V_A,V_B,tc_fun(T_a,tc_bool)) ) ))),
% 20.85/3.30 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 20.85/3.30 fof(f442,axiom,(
% 20.85/3.30 (![V_A,V_B,V_C,T_a]: (c_Lattices_Oupper__semilattice__class_Osup(V_A,c_Lattices_Oupper__semilattice__class_Osup(V_B,V_C,tc_fun(T_a,tc_bool)),tc_fun(T_a,tc_bool)) = c_Lattices_Oupper__semilattice__class_Osup(V_B,c_Lattices_Oupper__semilattice__class_Osup(V_A,V_C,tc_fun(T_a,tc_bool)),tc_fun(T_a,tc_bool)) ))),
% 20.85/3.30 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 20.85/3.30 fof(f449,axiom,(
% 20.85/3.30 (![V_B,V_A,T_a]: (c_lessequals(V_B,c_Lattices_Oupper__semilattice__class_Osup(V_A,V_B,tc_fun(T_a,tc_bool)),tc_fun(T_a,tc_bool)) ))),
% 20.85/3.30 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 20.85/3.30 fof(f450,axiom,(
% 20.85/3.30 (![V_A,V_B,T_a]: (c_lessequals(V_A,c_Lattices_Oupper__semilattice__class_Osup(V_A,V_B,tc_fun(T_a,tc_bool)),tc_fun(T_a,tc_bool)) ))),
% 20.85/3.30 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 20.85/3.30 fof(f459,axiom,(
% 20.85/3.30 (![V_A,V_B,T_a]: (c_Lattices_Oupper__semilattice__class_Osup(V_A,V_B,tc_fun(T_a,tc_bool)) = c_Lattices_Oupper__semilattice__class_Osup(V_B,V_A,tc_fun(T_a,tc_bool)) ))),
% 20.85/3.30 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 20.85/3.30 fof(f466,negated_conjecture,(
% 20.85/3.30 c_lessequals(v_ad,v_ab,tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool)) ),
% 20.85/3.30 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 20.85/3.30 fof(f469,negated_conjecture,(
% 20.85/3.30 c_Lattices_Oupper__semilattice__class_Osup(c_Map_Odom(v_ba,tc_List_Olist(tc_String_Ochar),tc_Value_Oval),v_ac,tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool)) = v_ab ),
% 20.85/3.30 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 20.85/3.30 fof(f471,negated_conjecture,(
% 20.85/3.30 c_Lattices_Oupper__semilattice__class_Osup(c_Map_Odom(v_b,tc_List_Olist(tc_String_Ochar),tc_Value_Oval),v_ae,tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool)) = v_ad ),
% 20.85/3.30 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 20.85/3.30 fof(f473,negated_conjecture,(
% 20.85/3.30 ( ~ c_lessequals(v_x,c_Lattices_Oupper__semilattice__class_Osup(c_Map_Odom(v_ba,tc_List_Olist(tc_String_Ochar),tc_Value_Oval),c_Lattices_Oupper__semilattice__class_Osup(v_ac,v_x,tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool)),tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool)),tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool))| ~ c_lessequals(v_ae,c_Lattices_Oupper__semilattice__class_Osup(c_Map_Odom(v_ba,tc_List_Olist(tc_String_Ochar),tc_Value_Oval),c_Lattices_Oupper__semilattice__class_Osup(v_ac,v_x,tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool)),tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool)),tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool))| ~ c_lessequals(c_Map_Odom(v_b,tc_List_Olist(tc_String_Ochar),tc_Value_Oval),c_Lattices_Oupper__semilattice__class_Osup(c_Map_Odom(v_ba,tc_List_Olist(tc_String_Ochar),tc_Value_Oval),c_Lattices_Oupper__semilattice__class_Osup(v_ac,v_x,tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool)),tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool)),tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool)) ) ),
% 20.85/3.30 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 20.85/3.30 fof(f1054,plain,(
% 20.85/3.30 ![V_A,T_a,V_B]: ((![V_C]: (c_lessequals(V_A,V_C,tc_fun(T_a,tc_bool))|~c_lessequals(V_B,V_C,tc_fun(T_a,tc_bool))))|~c_lessequals(V_A,V_B,tc_fun(T_a,tc_bool)))),
% 20.85/3.30 inference(miniscoping,[status(thm)],[f399])).
% 20.85/3.30 fof(f1055,plain,(
% 20.85/3.30 ![X0,X1,X2,X3]: (c_lessequals(X0,X1,tc_fun(X2,tc_bool))|~c_lessequals(X3,X1,tc_fun(X2,tc_bool))|~c_lessequals(X0,X3,tc_fun(X2,tc_bool)))),
% 20.85/3.30 inference(cnf_transformation,[status(thm)],[f1054])).
% 20.85/3.30 fof(f1070,plain,(
% 20.85/3.30 ![V_B,V_C,T_a]: (c_lessequals(V_B,V_C,tc_fun(T_a,tc_bool))|(![V_A]: ~c_lessequals(c_Lattices_Oupper__semilattice__class_Osup(V_A,V_B,tc_fun(T_a,tc_bool)),V_C,tc_fun(T_a,tc_bool))))),
% 20.85/3.30 inference(miniscoping,[status(thm)],[f408])).
% 20.85/3.30 fof(f1071,plain,(
% 20.85/3.30 ![X0,X1,X2,X3]: (c_lessequals(X0,X1,tc_fun(X2,tc_bool))|~c_lessequals(c_Lattices_Oupper__semilattice__class_Osup(X3,X0,tc_fun(X2,tc_bool)),X1,tc_fun(X2,tc_bool)))),
% 20.85/3.30 inference(cnf_transformation,[status(thm)],[f1070])).
% 20.85/3.30 fof(f1094,plain,(
% 20.85/3.30 ![X0,X1,X2]: (c_Lattices_Oupper__semilattice__class_Osup(X0,X1,tc_fun(X2,tc_bool))=X1|~c_lessequals(X0,X1,tc_fun(X2,tc_bool)))),
% 20.85/3.30 inference(cnf_transformation,[status(thm)],[f421])).
% 20.85/3.30 fof(f1125,plain,(
% 20.85/3.30 ![X0,X1,X2,X3]: (c_Lattices_Oupper__semilattice__class_Osup(X0,c_Lattices_Oupper__semilattice__class_Osup(X1,X2,tc_fun(X3,tc_bool)),tc_fun(X3,tc_bool))=c_Lattices_Oupper__semilattice__class_Osup(X1,c_Lattices_Oupper__semilattice__class_Osup(X0,X2,tc_fun(X3,tc_bool)),tc_fun(X3,tc_bool)))),
% 20.85/3.30 inference(cnf_transformation,[status(thm)],[f442])).
% 20.85/3.30 fof(f1137,plain,(
% 20.85/3.30 ![X0,X1,X2]: (c_lessequals(X0,c_Lattices_Oupper__semilattice__class_Osup(X1,X0,tc_fun(X2,tc_bool)),tc_fun(X2,tc_bool)))),
% 20.85/3.30 inference(cnf_transformation,[status(thm)],[f449])).
% 20.85/3.30 fof(f1138,plain,(
% 20.85/3.30 ![X0,X1,X2]: (c_lessequals(X0,c_Lattices_Oupper__semilattice__class_Osup(X0,X1,tc_fun(X2,tc_bool)),tc_fun(X2,tc_bool)))),
% 20.85/3.30 inference(cnf_transformation,[status(thm)],[f450])).
% 20.85/3.30 fof(f1155,plain,(
% 20.85/3.30 ![X0,X1,X2]: (c_Lattices_Oupper__semilattice__class_Osup(X0,X1,tc_fun(X2,tc_bool))=c_Lattices_Oupper__semilattice__class_Osup(X1,X0,tc_fun(X2,tc_bool)))),
% 20.85/3.30 inference(cnf_transformation,[status(thm)],[f459])).
% 20.85/3.30 fof(f1167,plain,(
% 20.85/3.30 c_lessequals(v_ad,v_ab,tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool))),
% 20.85/3.30 inference(cnf_transformation,[status(thm)],[f466])).
% 20.85/3.30 fof(f1170,plain,(
% 20.85/3.30 c_Lattices_Oupper__semilattice__class_Osup(c_Map_Odom(v_ba,tc_List_Olist(tc_String_Ochar),tc_Value_Oval),v_ac,tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool))=v_ab),
% 20.85/3.30 inference(cnf_transformation,[status(thm)],[f469])).
% 20.85/3.30 fof(f1172,plain,(
% 20.85/3.30 c_Lattices_Oupper__semilattice__class_Osup(c_Map_Odom(v_b,tc_List_Olist(tc_String_Ochar),tc_Value_Oval),v_ae,tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool))=v_ad),
% 20.85/3.30 inference(cnf_transformation,[status(thm)],[f471])).
% 20.85/3.30 fof(f1174,plain,(
% 20.85/3.30 ~c_lessequals(v_x,c_Lattices_Oupper__semilattice__class_Osup(c_Map_Odom(v_ba,tc_List_Olist(tc_String_Ochar),tc_Value_Oval),c_Lattices_Oupper__semilattice__class_Osup(v_ac,v_x,tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool)),tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool)),tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool))|~c_lessequals(v_ae,c_Lattices_Oupper__semilattice__class_Osup(c_Map_Odom(v_ba,tc_List_Olist(tc_String_Ochar),tc_Value_Oval),c_Lattices_Oupper__semilattice__class_Osup(v_ac,v_x,tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool)),tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool)),tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool))|~c_lessequals(c_Map_Odom(v_b,tc_List_Olist(tc_String_Ochar),tc_Value_Oval),c_Lattices_Oupper__semilattice__class_Osup(c_Map_Odom(v_ba,tc_List_Olist(tc_String_Ochar),tc_Value_Oval),c_Lattices_Oupper__semilattice__class_Osup(v_ac,v_x,tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool)),tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool)),tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool))),
% 20.85/3.30 inference(cnf_transformation,[status(thm)],[f473])).
% 20.85/3.30 fof(f1220,plain,(
% 20.85/3.30 c_lessequals(v_ae,v_ad,tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool))),
% 20.85/3.30 inference(paramodulation,[status(thm)],[f1172,f1137])).
% 20.85/3.30 fof(f1250,plain,(
% 20.85/3.30 c_lessequals(c_Map_Odom(v_b,tc_List_Olist(tc_String_Ochar),tc_Value_Oval),v_ad,tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool))),
% 20.85/3.30 inference(paramodulation,[status(thm)],[f1172,f1138])).
% 20.85/3.30 fof(f1253,plain,(
% 20.85/3.30 ~c_lessequals(v_x,c_Lattices_Oupper__semilattice__class_Osup(c_Map_Odom(v_ba,tc_List_Olist(tc_String_Ochar),tc_Value_Oval),c_Lattices_Oupper__semilattice__class_Osup(v_ac,v_x,tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool)),tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool)),tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool))|~c_lessequals(v_ae,c_Lattices_Oupper__semilattice__class_Osup(c_Map_Odom(v_ba,tc_List_Olist(tc_String_Ochar),tc_Value_Oval),c_Lattices_Oupper__semilattice__class_Osup(v_ac,v_x,tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool)),tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool)),tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool))|~c_lessequals(c_Map_Odom(v_b,tc_List_Olist(tc_String_Ochar),tc_Value_Oval),c_Lattices_Oupper__semilattice__class_Osup(c_Map_Odom(v_ba,tc_List_Olist(tc_String_Ochar),tc_Value_Oval),c_Lattices_Oupper__semilattice__class_Osup(v_x,v_ac,tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool)),tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool)),tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool))),
% 20.85/3.30 inference(backward_demodulation,[status(thm)],[f1155,f1174])).
% 20.85/3.30 fof(f1255,plain,(
% 20.85/3.30 c_Lattices_Oupper__semilattice__class_Osup(v_ac,c_Map_Odom(v_ba,tc_List_Olist(tc_String_Ochar),tc_Value_Oval),tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool))=v_ab),
% 20.85/3.30 inference(backward_demodulation,[status(thm)],[f1155,f1170])).
% 20.85/3.30 fof(f1264,plain,(
% 20.85/3.30 ~c_lessequals(v_x,c_Lattices_Oupper__semilattice__class_Osup(c_Map_Odom(v_ba,tc_List_Olist(tc_String_Ochar),tc_Value_Oval),c_Lattices_Oupper__semilattice__class_Osup(v_x,v_ac,tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool)),tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool)),tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool))|~c_lessequals(v_ae,c_Lattices_Oupper__semilattice__class_Osup(c_Map_Odom(v_ba,tc_List_Olist(tc_String_Ochar),tc_Value_Oval),c_Lattices_Oupper__semilattice__class_Osup(v_ac,v_x,tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool)),tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool)),tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool))|~c_lessequals(c_Map_Odom(v_b,tc_List_Olist(tc_String_Ochar),tc_Value_Oval),c_Lattices_Oupper__semilattice__class_Osup(c_Map_Odom(v_ba,tc_List_Olist(tc_String_Ochar),tc_Value_Oval),c_Lattices_Oupper__semilattice__class_Osup(v_x,v_ac,tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool)),tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool)),tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool))),
% 20.85/3.30 inference(forward_demodulation,[status(thm)],[f1155,f1253])).
% 20.85/3.30 fof(f1265,plain,(
% 20.85/3.30 ~c_lessequals(v_x,c_Lattices_Oupper__semilattice__class_Osup(c_Map_Odom(v_ba,tc_List_Olist(tc_String_Ochar),tc_Value_Oval),c_Lattices_Oupper__semilattice__class_Osup(v_x,v_ac,tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool)),tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool)),tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool))|~c_lessequals(v_ae,c_Lattices_Oupper__semilattice__class_Osup(c_Map_Odom(v_ba,tc_List_Olist(tc_String_Ochar),tc_Value_Oval),c_Lattices_Oupper__semilattice__class_Osup(v_x,v_ac,tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool)),tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool)),tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool))|~c_lessequals(c_Map_Odom(v_b,tc_List_Olist(tc_String_Ochar),tc_Value_Oval),c_Lattices_Oupper__semilattice__class_Osup(c_Map_Odom(v_ba,tc_List_Olist(tc_String_Ochar),tc_Value_Oval),c_Lattices_Oupper__semilattice__class_Osup(v_x,v_ac,tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool)),tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool)),tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool))),
% 20.85/3.30 inference(forward_demodulation,[status(thm)],[f1155,f1264])).
% 20.85/3.30 fof(f1423,plain,(
% 20.85/3.30 ![X0]: (c_lessequals(X0,v_ab,tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool))|~c_lessequals(X0,v_ad,tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool)))),
% 20.85/3.30 inference(resolution,[status(thm)],[f1055,f1167])).
% 20.85/3.30 fof(f1535,plain,(
% 20.85/3.30 c_lessequals(c_Map_Odom(v_b,tc_List_Olist(tc_String_Ochar),tc_Value_Oval),v_ab,tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool))),
% 20.85/3.30 inference(resolution,[status(thm)],[f1423,f1250])).
% 20.85/3.30 fof(f1536,plain,(
% 20.85/3.30 c_lessequals(v_ae,v_ab,tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool))),
% 20.85/3.30 inference(resolution,[status(thm)],[f1423,f1220])).
% 20.85/3.30 fof(f1541,plain,(
% 20.85/3.30 c_Lattices_Oupper__semilattice__class_Osup(v_ae,v_ab,tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool))=v_ab),
% 20.85/3.30 inference(resolution,[status(thm)],[f1536,f1094])).
% 20.85/3.30 fof(f1543,plain,(
% 20.85/3.30 c_Lattices_Oupper__semilattice__class_Osup(v_ab,v_ae,tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool))=v_ab),
% 20.85/3.30 inference(forward_demodulation,[status(thm)],[f1155,f1541])).
% 20.85/3.30 fof(f1565,plain,(
% 20.85/3.30 c_Lattices_Oupper__semilattice__class_Osup(c_Map_Odom(v_b,tc_List_Olist(tc_String_Ochar),tc_Value_Oval),v_ab,tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool))=v_ab),
% 20.85/3.30 inference(resolution,[status(thm)],[f1535,f1094])).
% 20.85/3.30 fof(f1567,plain,(
% 20.85/3.30 c_Lattices_Oupper__semilattice__class_Osup(v_ab,c_Map_Odom(v_b,tc_List_Olist(tc_String_Ochar),tc_Value_Oval),tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool))=v_ab),
% 20.85/3.30 inference(forward_demodulation,[status(thm)],[f1155,f1565])).
% 20.85/3.30 fof(f1575,plain,(
% 20.85/3.30 ![X0,X1,X2,X3]: (c_lessequals(X0,c_Lattices_Oupper__semilattice__class_Osup(X1,c_Lattices_Oupper__semilattice__class_Osup(X2,X0,tc_fun(X3,tc_bool)),tc_fun(X3,tc_bool)),tc_fun(X3,tc_bool)))),
% 20.85/3.30 inference(resolution,[status(thm)],[f1071,f1137])).
% 20.85/3.30 fof(f1718,plain,(
% 20.85/3.30 ![X0]: (c_lessequals(v_ae,c_Lattices_Oupper__semilattice__class_Osup(X0,v_ab,tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool)),tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool)))),
% 20.85/3.30 inference(paramodulation,[status(thm)],[f1543,f1575])).
% 20.85/3.30 fof(f1719,plain,(
% 20.85/3.30 ![X0]: (c_lessequals(c_Map_Odom(v_b,tc_List_Olist(tc_String_Ochar),tc_Value_Oval),c_Lattices_Oupper__semilattice__class_Osup(X0,v_ab,tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool)),tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool)))),
% 20.85/3.30 inference(paramodulation,[status(thm)],[f1567,f1575])).
% 20.85/3.30 fof(f1722,plain,(
% 20.85/3.30 ![X0,X1,X2,X3]: (c_lessequals(X0,c_Lattices_Oupper__semilattice__class_Osup(X1,c_Lattices_Oupper__semilattice__class_Osup(X0,X2,tc_fun(X3,tc_bool)),tc_fun(X3,tc_bool)),tc_fun(X3,tc_bool)))),
% 20.85/3.30 inference(paramodulation,[status(thm)],[f1155,f1575])).
% 20.85/3.30 fof(f1865,plain,(
% 20.85/3.30 ~c_lessequals(v_ae,c_Lattices_Oupper__semilattice__class_Osup(c_Map_Odom(v_ba,tc_List_Olist(tc_String_Ochar),tc_Value_Oval),c_Lattices_Oupper__semilattice__class_Osup(v_x,v_ac,tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool)),tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool)),tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool))|~c_lessequals(c_Map_Odom(v_b,tc_List_Olist(tc_String_Ochar),tc_Value_Oval),c_Lattices_Oupper__semilattice__class_Osup(c_Map_Odom(v_ba,tc_List_Olist(tc_String_Ochar),tc_Value_Oval),c_Lattices_Oupper__semilattice__class_Osup(v_x,v_ac,tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool)),tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool)),tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool))),
% 20.85/3.30 inference(backward_subsumption_resolution,[status(thm)],[f1265,f1722])).
% 20.85/3.30 fof(f2277,plain,(
% 20.85/3.30 ~c_lessequals(v_ae,c_Lattices_Oupper__semilattice__class_Osup(c_Map_Odom(v_ba,tc_List_Olist(tc_String_Ochar),tc_Value_Oval),c_Lattices_Oupper__semilattice__class_Osup(v_x,v_ac,tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool)),tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool)),tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool))|~c_lessequals(c_Map_Odom(v_b,tc_List_Olist(tc_String_Ochar),tc_Value_Oval),c_Lattices_Oupper__semilattice__class_Osup(v_x,c_Lattices_Oupper__semilattice__class_Osup(c_Map_Odom(v_ba,tc_List_Olist(tc_String_Ochar),tc_Value_Oval),v_ac,tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool)),tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool)),tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool))),
% 20.85/3.30 inference(backward_demodulation,[status(thm)],[f1125,f1865])).
% 20.85/3.30 fof(f2388,plain,(
% 20.85/3.30 ~c_lessequals(v_ae,c_Lattices_Oupper__semilattice__class_Osup(v_x,c_Lattices_Oupper__semilattice__class_Osup(c_Map_Odom(v_ba,tc_List_Olist(tc_String_Ochar),tc_Value_Oval),v_ac,tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool)),tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool)),tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool))|~c_lessequals(c_Map_Odom(v_b,tc_List_Olist(tc_String_Ochar),tc_Value_Oval),c_Lattices_Oupper__semilattice__class_Osup(v_x,c_Lattices_Oupper__semilattice__class_Osup(c_Map_Odom(v_ba,tc_List_Olist(tc_String_Ochar),tc_Value_Oval),v_ac,tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool)),tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool)),tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool))),
% 20.85/3.30 inference(forward_demodulation,[status(thm)],[f1125,f2277])).
% 20.84/3.38 fof(f2389,plain,(
% 20.84/3.38 ~c_lessequals(v_ae,c_Lattices_Oupper__semilattice__class_Osup(v_x,c_Lattices_Oupper__semilattice__class_Osup(v_ac,c_Map_Odom(v_ba,tc_List_Olist(tc_String_Ochar),tc_Value_Oval),tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool)),tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool)),tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool))|~c_lessequals(c_Map_Odom(v_b,tc_List_Olist(tc_String_Ochar),tc_Value_Oval),c_Lattices_Oupper__semilattice__class_Osup(v_x,c_Lattices_Oupper__semilattice__class_Osup(c_Map_Odom(v_ba,tc_List_Olist(tc_String_Ochar),tc_Value_Oval),v_ac,tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool)),tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool)),tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool))),
% 20.84/3.38 inference(forward_demodulation,[status(thm)],[f1155,f2388])).
% 20.84/3.38 fof(f2390,plain,(
% 20.84/3.38 ~c_lessequals(v_ae,c_Lattices_Oupper__semilattice__class_Osup(v_x,v_ab,tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool)),tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool))|~c_lessequals(c_Map_Odom(v_b,tc_List_Olist(tc_String_Ochar),tc_Value_Oval),c_Lattices_Oupper__semilattice__class_Osup(v_x,c_Lattices_Oupper__semilattice__class_Osup(c_Map_Odom(v_ba,tc_List_Olist(tc_String_Ochar),tc_Value_Oval),v_ac,tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool)),tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool)),tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool))),
% 20.84/3.38 inference(forward_demodulation,[status(thm)],[f1255,f2389])).
% 20.84/3.38 fof(f2391,plain,(
% 20.84/3.38 ~c_lessequals(v_ae,c_Lattices_Oupper__semilattice__class_Osup(v_x,v_ab,tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool)),tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool))|~c_lessequals(c_Map_Odom(v_b,tc_List_Olist(tc_String_Ochar),tc_Value_Oval),c_Lattices_Oupper__semilattice__class_Osup(v_x,c_Lattices_Oupper__semilattice__class_Osup(v_ac,c_Map_Odom(v_ba,tc_List_Olist(tc_String_Ochar),tc_Value_Oval),tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool)),tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool)),tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool))),
% 20.84/3.38 inference(forward_demodulation,[status(thm)],[f1155,f2390])).
% 20.84/3.38 fof(f2392,plain,(
% 20.84/3.38 ~c_lessequals(v_ae,c_Lattices_Oupper__semilattice__class_Osup(v_x,v_ab,tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool)),tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool))|~c_lessequals(c_Map_Odom(v_b,tc_List_Olist(tc_String_Ochar),tc_Value_Oval),c_Lattices_Oupper__semilattice__class_Osup(v_x,v_ab,tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool)),tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool))),
% 20.84/3.38 inference(forward_demodulation,[status(thm)],[f1255,f2391])).
% 20.84/3.38 fof(f2393,plain,(
% 20.84/3.38 ~c_lessequals(c_Map_Odom(v_b,tc_List_Olist(tc_String_Ochar),tc_Value_Oval),c_Lattices_Oupper__semilattice__class_Osup(v_x,v_ab,tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool)),tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool))),
% 20.84/3.38 inference(forward_subsumption_resolution,[status(thm)],[f2392,f1718])).
% 20.84/3.38 fof(f11557,plain,(
% 20.84/3.38 $false),
% 20.84/3.38 inference(backward_subsumption_resolution,[status(thm)],[f2393,f1719])).
% 20.84/3.38 % SZS output end CNFRefutation for theBenchmark.p
% 1.70/3.46 % Elapsed time: 3.017373 seconds
% 1.70/3.46 % CPU time: 22.057240 seconds
% 1.70/3.46 % Total memory used: 430.130 MB
% 1.70/3.46 % Net memory used: 422.622 MB
%------------------------------------------------------------------------------