%------------------------------------------------------------------------------
% File : SOS---2.0
% Problem : LCL767-1 : TPTP v8.1.0. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : sos-script %s
% Computer : n006.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 600s
% DateTime : Sun Jul 17 14:32:46 EDT 2022
% Result : Unknown 2.76s 2.93s
% Output : None
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.11 % Problem : LCL767-1 : TPTP v8.1.0. Released v4.1.0.
% 0.06/0.12 % Command : sos-script %s
% 0.12/0.33 % Computer : n006.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 600
% 0.12/0.33 % DateTime : Sun Jul 3 08:09:07 EDT 2022
% 0.12/0.33 % CPUTime :
% 0.12/0.37 ----- Otter 3.2, August 2001 -----
% 0.12/0.37 The process was started by sandbox on n006.cluster.edu,
% 0.12/0.37 Sun Jul 3 08:09:07 2022
% 0.12/0.37 The command was "./sos". The process ID is 25745.
% 0.12/0.37
% 0.12/0.37 set(prolog_style_variables).
% 0.12/0.37 set(auto).
% 0.12/0.37 dependent: set(auto1).
% 0.12/0.37 dependent: set(process_input).
% 0.12/0.37 dependent: clear(print_kept).
% 0.12/0.37 dependent: clear(print_new_demod).
% 0.12/0.37 dependent: clear(print_back_demod).
% 0.12/0.37 dependent: clear(print_back_sub).
% 0.12/0.37 dependent: set(control_memory).
% 0.12/0.37 dependent: assign(max_mem, 12000).
% 0.12/0.37 dependent: assign(pick_given_ratio, 4).
% 0.12/0.37 dependent: assign(stats_level, 1).
% 0.12/0.37 dependent: assign(pick_semantic_ratio, 3).
% 0.12/0.37 dependent: assign(sos_limit, 5000).
% 0.12/0.37 dependent: assign(max_weight, 60).
% 0.12/0.37 clear(print_given).
% 0.12/0.37
% 0.12/0.37 list(usable).
% 0.12/0.37
% 0.12/0.37 SCAN INPUT: prop=0, horn=0, equality=1, symmetry=0, max_lits=4.
% 0.12/0.37
% 0.12/0.37 This ia a non-Horn set with equality. The strategy will be
% 0.12/0.37 Knuth-Bendix, ordered hyper_res, ur_res, factoring, and
% 0.12/0.37 unit deletion, with positive clauses in sos and nonpositive
% 0.12/0.37 clauses in usable.
% 0.12/0.37
% 0.12/0.37 dependent: set(knuth_bendix).
% 0.12/0.37 dependent: set(para_from).
% 0.12/0.37 dependent: set(para_into).
% 0.12/0.37 dependent: clear(para_from_right).
% 0.12/0.37 dependent: clear(para_into_right).
% 0.12/0.37 dependent: set(para_from_vars).
% 0.12/0.37 dependent: set(eq_units_both_ways).
% 0.12/0.37 dependent: set(dynamic_demod_all).
% 0.12/0.37 dependent: set(dynamic_demod).
% 0.12/0.37 dependent: set(order_eq).
% 0.12/0.37 dependent: set(back_demod).
% 0.12/0.37 dependent: set(lrpo).
% 0.12/0.37 dependent: set(hyper_res).
% 0.12/0.37 dependent: set(unit_deletion).
% 0.12/0.37 dependent: set(factor).
% 0.12/0.37
% 0.12/0.37 ------------> process usable:
% 0.12/0.37 Following clause subsumed by 24 during input processing: 0 [] {-} c_Suc(A)!=c_Suc(B)|A=B.
% 0.12/0.37 Following clause subsumed by 34 during input processing: 0 [] {-} A=B| -c_HOL_Oord__class_Oless(A,c_Suc(B),tc_nat)|c_HOL_Oord__class_Oless(A,B,tc_nat).
% 0.12/0.37 Following clause subsumed by 36 during input processing: 0 [] {-} -c_HOL_Oord__class_Oless(A,A,tc_nat).
% 0.12/0.37 Following clause subsumed by 42 during input processing: 0 [] {-} -class_Orderings_Olinorder(A)|c_HOL_Oord__class_Oless(B,C,A)|c_HOL_Oord__class_Oless(C,B,A)|C=B.
% 0.12/0.37 Following clause subsumed by 42 during input processing: 0 [] {-} -class_Orderings_Olinorder(A)|c_HOL_Oord__class_Oless(B,C,A)|C=B|c_HOL_Oord__class_Oless(C,B,A).
% 0.12/0.37 Following clause subsumed by 42 during input processing: 0 [] {-} -class_Orderings_Olinorder(A)|B=C|c_HOL_Oord__class_Oless(B,C,A)|c_HOL_Oord__class_Oless(C,B,A).
% 0.12/0.37 Following clause subsumed by 45 during input processing: 0 [] {-} c_Suc(A)!=c_HOL_Ozero__class_Ozero(tc_nat).
% 0.12/0.37 Following clause subsumed by 36 during input processing: 0 [] {-} -c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),c_HOL_Ozero__class_Ozero(tc_nat),tc_nat).
% 0.12/0.37 Following clause subsumed by 55 during input processing: 0 [flip.1] {-} c_Suc(A)!=A.
% 0.12/0.37 Following clause subsumed by 72 during input processing: 0 [] {-} -class_Orderings_Opreorder(A)| -c_HOL_Oord__class_Oless(B,C,A)| -c_HOL_Oord__class_Oless(C,B,A).
% 0.12/0.37 Following clause subsumed by 94 during input processing: 0 [] {-} hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),A),B)!=A|B=c_HOL_Ozero__class_Ozero(tc_nat).
% 0.12/0.37 Following clause subsumed by 97 during input processing: 0 [] {-} -class_Ring__and__Field_Ocomm__semiring__1(A)|hAPP(hAPP(c_HOL_Oplus__class_Oplus(A),B),C)=hAPP(hAPP(c_HOL_Oplus__class_Oplus(A),C),B).
% 0.12/0.37 Following clause subsumed by 100 during input processing: 0 [] {-} c_HOL_Oord__class_Oless(A,hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),B),C),tc_nat)| -c_HOL_Oord__class_Oless(A,C,tc_nat).
% 0.12/0.37 Following clause subsumed by 101 during input processing: 0 [] {-} c_HOL_Oord__class_Oless(A,hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),B),C),tc_nat)| -c_HOL_Oord__class_Oless(A,B,tc_nat).
% 0.12/0.37 Following clause subsumed by 45 during input processing: 0 [flip.1] {-} c_Suc(A)!=c_HOL_Ozero__class_Ozero(tc_nat).
% 0.12/0.37 Following clause subsumed by 45 during input processing: 0 [flip.1] {-} c_Suc(A)!=c_HOL_Ozero__class_Ozero(tc_nat).
% 0.12/0.37 Following clause subsumed by 109 during input processing: 0 [flip.2] {-} -class_Ring__and__Field_Ocomm__semiring__1(A)|hAPP(hAPP(c_HOL_Oplus__class_Oplus(A),hAPP(hAPP(c_HOL_Oplus__class_Oplus(A),B),C)),D)=hAPP(hAPP(c_HOL_Oplus__class_Oplus(A),B),hAPP(hAPP(c_HOL_Oplus__class_Oplus(A),C),D)).
% 0.12/0.37 Following clause subsumed by 109 during input processing: 0 [] {-} -class_Ring__and__Field_Ocomm__semiring__1(A)|hAPP(hAPP(c_HOL_Oplus__class_Oplus(A),hAPP(hAPP(c_HOL_Oplus__class_Oplus(A),B),C)),D)=hAPP(hAPP(c_HOL_Oplus__class_Oplus(A),B),hAPP(hAPP(c_HOL_Oplus__class_Oplus(A),C),D)).
% 0.12/0.37 Following clause subsumed by 117 during input processing: 0 [] {-} -c_HOL_Oord__class_Oless(A,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat).
% 0.12/0.37 Following clause subsumed by 125 during input processing: 0 [] {-} hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),A),B)!=hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),A),C)|B=C.
% 0.12/0.37 Following clause subsumed by 136 during input processing: 0 [] {-} -class_Ring__and__Field_Ocomm__semiring__1(A)|hAPP(hAPP(c_HOL_Oplus__class_Oplus(A),c_HOL_Ozero__class_Ozero(A)),B)=B.
% 0.12/0.37 Following clause subsumed by 146 during input processing: 0 [] {-} c_HOL_Oord__class_Oless(c_Suc(A),c_Suc(B),tc_nat)| -c_HOL_Oord__class_Oless(A,B,tc_nat).
% 0.12/0.37 Following clause subsumed by 100 during input processing: 0 [] {-} c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),A),B),tc_nat)| -c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),B,tc_nat).
% 0.12/0.37 Following clause subsumed by 101 during input processing: 0 [] {-} c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),A),B),tc_nat)| -c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),A,tc_nat).
% 0.12/0.37 Following clause subsumed by 256 during input processing: 0 [] {-} c_List_Oappend(A,B,C)!=B|A=c_List_Olist_ONil(C).
% 0.12/0.37 Following clause subsumed by 258 during input processing: 0 [] {-} c_List_Oappend(A,B,C)!=A|B=c_List_Olist_ONil(C).
% 0.12/0.37 Following clause subsumed by 277 during input processing: 0 [] {-} c_List_Olist_OCons(A,B,C)!=c_List_Olist_ONil(C).
% 0.12/0.37 Following clause subsumed by 279 during input processing: 0 [flip.1] {-} c_List_Olist_OCons(B,A,C)!=A.
% 0.12/0.37 Following clause subsumed by 194 during input processing: 0 [copy,193,flip.1] {-} c_Lambda_OdB_OAbs(A)!=c_Lambda_OdB_OVar(B).
% 0.12/0.37 Following clause subsumed by 193 during input processing: 0 [copy,194,flip.1] {-} c_Lambda_OdB_OVar(A)!=c_Lambda_OdB_OAbs(B).
% 0.12/0.37 Following clause subsumed by 198 during input processing: 0 [copy,197,flip.1] {-} hAPP(hAPP(c_Lambda_OdB_OApp,A),B)!=c_Lambda_OdB_OAbs(C).
% 0.12/0.37 Following clause subsumed by 197 during input processing: 0 [copy,198,flip.1] {-} c_Lambda_OdB_OAbs(A)!=hAPP(hAPP(c_Lambda_OdB_OApp,B),C).
% 0.12/0.37 Following clause subsumed by 277 during input processing: 0 [copy,261,flip.1] {-} c_List_Olist_OCons(A,B,C)!=c_List_Olist_ONil(C).
% 0.12/0.37 Following clause subsumed by 281 during input processing: 0 [copy,266,flip.1] {-} hAPP(hAPP(c_Lambda_OdB_OApp,A),B)!=c_Lambda_OdB_OVar(C).
% 0.12/0.37 Following clause subsumed by 261 during input processing: 0 [copy,277,flip.1] {-} c_List_Olist_ONil(A)!=c_List_Olist_OCons(B,C,A).
% 0.12/0.37 Following clause subsumed by 266 during input processing: 0 [copy,281,flip.1] {-} c_Lambda_OdB_OVar(A)!=hAPP(hAPP(c_Lambda_OdB_OApp,B),C).
% 0.12/0.37 Following clause subsumed by 240 during input processing: 0 [copy,307,flip.1] {-} c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_OdB_OVar(A),B,tc_Lambda_OdB,tc_Lambda_OdB)!=c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_OdB_OAbs(C),D,tc_Lambda_OdB,tc_Lambda_OdB).
% 0.12/0.37 Following clause subsumed by 241 during input processing: 0 [copy,308,flip.1] {-} hAPP(hAPP(c_Lambda_OdB_OApp,c_Lambda_OdB_OAbs(A)),B)!=c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_OdB_OVar(C),D,tc_Lambda_OdB,tc_Lambda_OdB).
% 0.12/0.37
% 0.12/0.37 ------------> process sos:
% 0.12/0.37 Following clause subsumed by 359 during input processing: 0 [] {-} c_List_Otake(c_HOL_Ozero__class_Ozero(tc_nat),c_List_Olist_OCons(A,B,C),C)=c_List_Olist_ONil(C).
% 0.12/0.37 Following clause subsumed by 400 during input processing: 0 [] {-} hBOOL(hAPP(hAPP(A,B),C))|c_HOL_Oord__class_Oless(B,C,tc_nat)|C=B|c_HOL_Oord__class_Oless(C,B,tc_nat).
% 0.12/0.37 Following clause subsumed by 400 during input processing: 0 [] {-} c_HOL_Oord__class_Oless(A,B,tc_nat)|c_HOL_Oord__class_Oless(B,A,tc_nat)|B=A.
% 0.12/0.37 Following clause subsumed by 401 during input processing: 0 [] {-} c_HOL_Oord__class_Oless(A,c_Suc(A),tc_nat).
% 0.12/0.37 Following clause subsumed by 429 during input processing: 0 [] {-} c_HOL_Oord__class_Oless(A,c_Suc(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),A),B)),tc_nat).
% 0.12/0.37 Following clause subsumed by 437 during input processing: 0 [demod,404] {-} c_Suc(c_HOL_Ozero__class_Ozero(tc_nat))=c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)).
% 0.12/0.37 Following clause subsumed by 444 during input processing: 0 [] {-} c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),c_Suc(A),tc_nat).
% 0.12/0.37 Following clause subsumed by 401 during input processing: 0 [unit_del,36] {-} c_HOL_Oord__class_Oless(A,c_Suc(A),tc_nat).
% 0.12/0.37 Following clause subsumed by 453 during input processing: 0 [demod,501] {-} c_List_Olist_OCons(A,c_List_Olist_ONil(B),B)=c_List_Olist_OCons(A,c_List_Olist_ONil(B),B).
% 0.12/0.37 Following clause subsumed by 453 during input processing: 0 [demod,479] {-} B=B.
% 0.12/0.37 Following clause subsumed by 453 during input processing: 0 [demod,519] {-} c_List_Olist_ONil(A)=c_List_Olist_ONil(A).
% 0.12/0.37 Following clause subsumed by 453 during input processing: 0 [demod,529] {-} A=A.
% 0.12/0.37 Following clause subsumed by 453 during input processing: 0 [demod,529] {-} A=A.
% 0.12/0.37 Following clause subsumed by 453 during input processing: 0 [demod,549] {-} c_Lambda_OdB_OAbs(A)=c_Lambda_OdB_OAbs(A).
% 0.12/0.37 Following clause subsumed by 453 during input processing: 0 [demod,553] {-} c_List_Oappend(A,c_List_Oappend(B,D,C),C)=c_List_Oappend(A,c_List_Oappend(B,D,C),C).
% 0.12/0.37 Following clause subsumed by 453 during input processing: 0 [demod,553] {-} c_List_Oappend(A,c_List_Oappend(B,C,D),D)=c_List_Oappend(A,c_List_Oappend(B,C,D),D).
% 0.12/0.37 Following clause subsumed by 453 during input processing: 0 [demod,553] {-} c_List_Oappend(A,c_List_Oappend(B,D,C),C)=c_List_Oappend(A,c_List_Oappend(B,D,C),C).
% 0.12/0.37 Following clause subsumed by 453 during input processing: 0 [demod,568] {-} B=B.
% 0.12/0.37 Following clause subsumed by 453 during input processing: 0 [demod,568] {-} A=A.
% 0.12/0.37 Following clause subsumed by 453 during input processing: 0 [demod,571] {-} A=A.
% 0.12/0.37 Following clause subsumed by 453 during input processing: 0 [demod,564] {-} c_Lambda_OdB_OVar(A)=c_Lambda_OdB_OVar(A).
% 0.12/0.37 Following clause subsumed by 453 during input processing: 0 [demod,580] {-} c_List_Oappend(c_List_Olist_OCons(A,B,C),D,C)=c_List_Oappend(c_List_Olist_OCons(A,B,C),D,C).
% 0.12/0.37 Following clause subsumed by 453 during input processing: 0 [demod,580] {-} c_List_Oappend(c_List_Olist_OCons(A,B,D),C,D)=c_List_Oappend(c_List_Olist_OCons(A,B,D),C,D).
% 0.12/0.37 Following clause subsumed by 453 during input processing: 0 [demod,580] {-} c_List_Oappend(c_List_Olist_OCons(A,B,D),C,D)=c_List_Oappend(c_List_Olist_OCons(A,B,D),C,D).
% 0.12/0.37 Following clause subsumed by 453 during input processing: 0 [demod,568] {-} c_List_Olist_OCons(A,B,C)=c_List_Olist_OCons(A,B,C).
% 0.12/0.37 Following clause subsumed by 453 during input processing: 0 [demod,571] {-} c_List_Olist_ONil(A)=c_List_Olist_ONil(A).
% 0.12/0.37 Following clause subsumed by 576 during input processing: 0 [] {-} hAPP(c_COMBS(A,B,C,D,E),F)=hAPP(hAPP(A,F),hAPP(B,F)).
% 0.12/0.37 Following clause subsumed by 575 during input processing: 0 [] {-} hAPP(hAPP(c_COMBC(A,B,C,D),E),F)=hAPP(hAPP(A,F),E).
% 0.12/0.37 Following clause subsumed by 453 during input processing: 0 [demod,574] {-} hAPP(A,hAPP(B,F))=hAPP(A,hAPP(B,F)).
% 0.12/0.37 Following clause subsumed by 453 during input processing: 0 [] {-} A=A.
% 0.12/0.37 Following clause subsumed by 453 during input processing: 0 [copy,326,flip.1] {-} c_List_Odrop(A,c_List_Obutlast(B,C),C)=c_List_Odrop(A,c_List_Obutlast(B,C),C).
% 0.12/0.37 Following clause subsumed by 453 during input processing: 0 [copy,335,flip.1] {-} c_List_Olist_OCons(A,B,C)=c_List_Olist_OCons(A,B,C).
% 0.12/0.37 Following clause subsumed by 453 during input processing: 0 [copy,337,flip.1] {-} c_List_Odrop(A,c_List_Otl(B,C),C)=c_List_Odrop(A,c_List_Otl(B,C),C).
% 0.12/0.37 Following clause subsumed by 453 during input processing: 0 [copy,356,flip.1] {-} c_HOL_Ozero__class_Ozero(tc_nat)=c_HOL_Ozero__class_Ozero(tc_nat).
% 0.12/0.37 Following clause subsumed by 381 during input processing: 0 [copy,380,flip.1] {-} c_Nat_Osize__class_Osize(c_List_Olist_OCons(A,B,C),tc_List_Olist(C))=c_Suc(c_Nat_Osize__class_Osize(B,tc_List_Olist(C))).
% 0.12/0.37 Following clause subsumed by 380 during input processing: 0 [copy,381,flip.1] {-} c_Suc(c_Nat_Osize__class_Osize(A,tc_List_Olist(B)))=c_Nat_Osize__class_Osize(c_List_Olist_OCons(C,A,B),tc_List_Olist(B)).
% 0.12/0.37 401 back subsumes 393.
% 0.12/0.37 Following clause subsumed by 428 during input processing: 0 [copy,428,flip.1] {-} hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),A),B)=hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),B),A).
% 0.12/0.37 Following clause subsumed by 443 during input processing: 0 [copy,435,flip.1] {-} hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),c_Suc(A)),B)=hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),A),c_Suc(B)).
% 0.12/0.37 Following clause subsumed by 453 during input processing: 0 [copy,437,flip.1] {-} c_Suc(c_HOL_Ozero__class_Ozero(tc_nat))=c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)).
% 0.12/0.37 Following clause subsumed by 440 during input processing: 0 [copy,440,flip.1] {-} hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),A),hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),B),C))=hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),B),hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),A),C)).
% 0.12/0.37 Following clause subsumed by 435 during input processing: 0 [copy,443,flip.1] {-} hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),A),c_Suc(B))=hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),c_Suc(A)),B).
% 0.12/0.37 Following clause subsumed by 445 during input processing: 0 [copy,445,flip.1] {-} c_List_Oreplicate(c_HOL_Ozero__class_Ozero(tc_nat),A,B)=c_List_Oreplicate(c_HOL_Ozero__class_Ozero(tc_nat),C,B).
% 0.12/0.37 Following clause subsumed by 453 during input processing: 0 [copy,453,flip.1] {-} A=A.
% 0.12/0.37 453 back subsumes 437.
% 0.12/0.37 453 back subsumes 356.
% 0.12/0.37 453 back subsumes 337.
% 0.12/0.37 453 back subsumes 335.
% 0.12/0.37 453 back subsumes 326.
% 0.12/0.37 453 back subsumes 306.
% 0.12/0.37 453 back subsumes 291.
% 0.12/0.37 453 back subsumes 290.
% 0.12/0.37 Following clause subsumed by 474 during input processing: 0 [copy,473,flip.1] {-} c_List_Olist_ONil(A)=c_List_Oreplicate(c_HOL_Ozero__class_Ozero(tc_nat),B,A).
% 0.12/0.37 Following clause subsumed by 473 during input processing: 0 [copy,474,flip.1] {-} c_List_Oreplicate(c_HOL_Ozero__class_Ozero(tc_nat),A,B)=c_List_Olist_ONil(B).
% 0.12/0.37 Following clause subsumed by 514 during input processing: 0 [copy,514,flip.1] {-} c_List_Oappend(c_List_Oreplicate(A,B,C),c_List_Oreplicate(D,B,C),C)=c_List_Oappend(c_List_Oreplicate(D,B,C),c_List_Oreplicate(A,B,C),C).
% 0.12/0.37 560 back subsumes 554.
% 0.12/0.37 Following clause subsumed by 315 during input processing: 0 [copy,600,flip.1] {-} c_List_Odrop(c_Suc(A),B,C)=c_List_Odrop(A,c_List_Otl(B,C),C).
% 0.12/0.37 Following clause subsumed by 359 during input processing: 0 [copy,601,flip.1] {-} c_List_Otake(c_HOL_Ozero__class_Ozero(tc_nat),A,B)=c_List_Olist_ONil(B).
% 0.12/0.37 Following clause subsumed by 417 during input processing: 0 [copy,604,flip.1] {-} c_Nat_Osize__class_Osize(c_Lambda_OdB_OAbs(A),tc_Lambda_OdB)=hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),c_Nat_Osize__class_Osize(A,tc_Lambda_OdB)),c_Suc(c_HOL_Ozero__class_Ozero(tc_nat))).
% 0.12/0.37 Following clause subsumed by 418 during input processing: 0 [copy,605,flip.1] {-} c_Lambda_OdB_OdB__size(c_Lambda_OdB_OAbs(A))=hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),c_Lambda_OdB_OdB__size(A)),c_Suc(c_HOL_Ozero__class_Ozero(tc_nat))).
% 0.12/0.37 Following clause subsumed by 614 during input processing: 0 [copy,606,flip.1] {-} c_Lambda_OdB_OdB__size(hAPP(hAPP(c_Lambda_OdB_OApp,A),B))=hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),c_Lambda_OdB_OdB__size(A)),hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),c_Lambda_OdB_OdB__size(B)),c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)))).
% 0.12/0.37 Following clause subsumed by 423 during input processing: 0 [copy,607,flip.1] {-} c_Nat_Osize__class_Osize(c_List_Olist_OCons(A,B,C),tc_List_Olist(C))=hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),c_Nat_Osize__class_Osize(B,tc_List_Olist(C))),c_Suc(c_HOL_Ozero__class_Ozero(tc_nat))).
% 0.12/0.37 Following clause subsumed by 427 during input processing: 0 [copy,608,flip.1] {-} c_Type_Oshift(c_Type_Oshift(A,B,C,D),c_HOL_Ozero__class_Ozero(tc_nat),E,D)=c_Type_Oshift(c_Type_Oshift(A,c_HOL_Ozero__class_Ozero(tc_nat),E,D),c_Suc(B),C,D).
% 0.12/0.37 Following clause subsumed by 606 during input processing: 0 [copy,614,flip.1] {-} hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),c_Lambda_OdB_OdB__size(A)),hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),c_Lambda_OdB_OdB__size(B)),c_Suc(c_HOL_Ozero__class_Ozero(tc_nat))))=c_Lambda_OdB_OdB__size(hAPP(hAPP(c_Lambda_OdB_OApp,A),B)).
% 0.12/0.37 Following clause subsumed by 487 during input processing: 0 [copy,622,flip.1] {-} c_List_Ofoldr(A,B,C,D,E)=c_List_Ofoldl(c_COMBC(A,D,E,E),C,c_List_Orev(B,D),E,D).
% 0.12/0.37 Following clause subsumed by 539 during input processing: 0 [copy,625,flip.1] {-} c_List_Orev(c_List_Olist_OCons(A,B,C),C)=c_List_Oappend(c_List_Orev(B,C),c_List_Olist_OCons(A,c_List_Olist_ONil(C),C),C).
% 0.12/0.37 Following clause subsumed by 541 during input processing: 0 [copy,626,flip.1] {-} c_List_Oappend(c_List_Olist_OCons(A,c_List_Olist_ONil(B),B),C,B)=c_List_Olist_OCons(A,C,B).
% 0.12/0.37 Following clause subsumed by 542 during input processing: 0 [copy,627,flip.1] {-} c_List_Orotate1(c_List_Olist_OCons(A,B,C),C)=c_List_Oappend(B,c_List_Olist_OCons(A,c_List_Olist_ONil(C),C),C).
% 0.12/0.37 Following clause subsumed by 543 during input processing: 0 [copy,628,flip.1] {-} c_List_Oappend(c_List_Oreplicate(A,B,C),c_List_Olist_OCons(B,c_List_Olist_ONil(C),C),C)=c_List_Olist_OCons(B,c_List_Oreplicate(A,B,C),C).
% 0.12/0.37 Following clause subsumed by 550 during input processing: 0 [copy,629,flip.1] {-} c_List_Olistsp(c_COMBS(c_COMBB(c_and,A,tc_bool,tc_fun(tc_bool,tc_bool),t_a),B,t_a,tc_bool,tc_bool),v_x,t_a)=hAPP(hAPP(c_and,c_List_Olistsp(A,v_x,t_a)),c_List_Olistsp(B,v_x,t_a)).
% 0.12/0.37 Following clause subsumed by 560 during input processing: 0 [copy,630,flip.1] {-} hAPP(hAPP(c_Lambda_OdB_OApp,c_List_Ofoldl(c_Lambda_OdB_OApp,A,B,tc_Lambda_OdB,tc_Lambda_OdB)),C)=c_List_Ofoldl(c_Lambda_OdB_OApp,A,c_List_Oappend(B,c_List_Olist_OCons(C,c_List_Olist_ONil(tc_Lambda_OdB),tc_Lambda_OdB),tc_Lambda_OdB),tc_Lambda_OdB,tc_Lambda_OdB).
% 0.12/0.37 Following clause subsumed by 575 during input processing: 0 [copy,631,flip.1] {-} hAPP(hAPP(c_COMBC(A,B,C,D),E),F)=hAPP(hAPP(A,F),E).
% 0.12/0.37 Following clause subsumed by 576 during input processing: 0 [copy,632,flip.1] {-} hAPP(c_COMBS(A,B,C,D,E),F)=hAPP(hAPP(A,F),hAPP(B,F)).
% 0.12/0.37 Following clause subsumed by 577 during input processing: 0 [copy,633,flip.1] {-} c_List_Ofoldl(A,B,c_List_Olist_OCons(C,D,E),F,E)=c_List_Ofoldl(A,hAPP(hAPP(A,B),C),D,F,E).
% 0.12/0.37 Following clause subsumed by 581 during input processing: 0 [copy,635,flip.1] {-} c_List_Ofoldl(A,B,c_List_Oappend(C,D,E),F,E)=c_List_Ofoldl(A,c_List_Ofoldl(A,B,C,F,E),D,F,E).
% 0.12/0.37 Following clause subsumed by 634 during input processing: 0 [copy,636,flip.1] {-} c_List_Oappend(c_List_Olist_OCons(A,c_List_Oreplicate(B,A,C),C),D,C)=c_List_Oappend(c_List_Oreplicate(B,A,C),c_List_Olist_OCons(A,D,C),C).
% 0.12/0.37
% 0.12/0.37 ======= end of input processing =======
% 0.34/0.52
% 0.34/0.52
% 0.34/0.52 Failed to model usable list: disabling FINDER
% 0.34/0.52
% 0.34/0.52
% 0.34/0.52
% 0.34/0.52 -------------- Softie stats --------------
% 0.34/0.52
% 0.34/0.52 UPDATE_STOP: 300
% 0.34/0.52 SFINDER_TIME_LIMIT: 2
% 0.34/0.52 SHORT_CLAUSE_CUTOFF: 4
% 0.34/0.52 number of clauses in intial UL: 270
% 0.34/0.52 number of clauses initially in problem: 514
% 0.34/0.52 percentage of clauses intially in UL: 52
% 0.34/0.52 percentage of distinct symbols occuring in initial UL: 79
% 0.34/0.52 percent of all initial clauses that are short: 99
% 0.34/0.52 absolute distinct symbol count: 112
% 0.34/0.52 distinct predicate count: 27
% 0.34/0.52 distinct function count: 64
% 0.34/0.52 distinct constant count: 21
% 0.34/0.52
% 0.34/0.52 ---------- no more Softie stats ----------
% 0.34/0.52
% 0.34/0.52
% 0.34/0.52
% 0.34/0.52 =========== start of search ===========
% 0.94/1.14
% 0.94/1.14
% 0.94/1.14 Changing weight limit from 60 to 36.
% 0.94/1.14
% 0.94/1.14 Resetting weight limit to 36 after 30 givens.
% 0.94/1.14
% 1.41/1.65
% 1.41/1.65
% 1.41/1.65 Changing weight limit from 36 to 28.
% 1.41/1.65
% 1.41/1.65 Resetting weight limit to 28 after 35 givens.
% 1.41/1.65
% 1.58/1.77
% 1.58/1.77
% 1.58/1.77 Changing weight limit from 28 to 26.
% 1.58/1.77
% 1.58/1.77 Resetting weight limit to 26 after 40 givens.
% 1.58/1.77
% 1.70/1.90
% 1.70/1.90
% 1.70/1.90 Changing weight limit from 26 to 24.
% 1.70/1.90
% 1.70/1.90 Resetting weight limit to 24 after 45 givens.
% 1.70/1.90
% 1.81/2.02
% 1.81/2.02
% 1.81/2.02 Changing weight limit from 24 to 23.
% 1.81/2.02
% 1.81/2.02 Resetting weight limit to 23 after 50 givens.
% 1.81/2.02
% 1.88/2.11
% 1.88/2.11
% 1.88/2.11 Changing weight limit from 23 to 22.
% 1.88/2.11
% 1.88/2.11 Resetting weight limit to 22 after 55 givens.
% 1.88/2.11
% 2.13/2.31
% 2.13/2.31
% 2.13/2.31 Changing weight limit from 22 to 20.
% 2.13/2.31
% 2.13/2.31 Resetting weight limit to 20 after 60 givens.
% 2.13/2.31
% 2.24/2.40
% 2.24/2.40
% 2.24/2.40 Changing weight limit from 20 to 19.
% 2.24/2.40
% 2.24/2.40 Resetting weight limit to 19 after 65 givens.
% 2.24/2.40
% 2.30/2.54
% 2.30/2.54
% 2.30/2.54 Changing weight limit from 19 to 18.
% 2.30/2.54
% 2.30/2.54 Resetting weight limit to 18 after 80 givens.
% 2.30/2.54
% 2.55/2.75
% 2.55/2.75
% 2.55/2.75 Changing weight limit from 18 to 17.
% 2.55/2.75
% 2.55/2.75 Resetting weight limit to 17 after 95 givens.
% 2.55/2.75
% 2.76/2.93 c_List_Oappend(c_List_Odrop(c_Nat_Osize__class_Osize(A,tc_List_Olist(B)),A,B),c_List_Oappend(c_List_Odrop(c_Nat_Osize__class_Osize(A,tc_List_Olist(B)),A,B),C,B),B)=C.
% 2.76/2.93
% 2.76/2.93 ------------- memory usage ------------
% 2.76/2.93 360 mallocs of 32700 bytes each, 11496.1 K.
% 2.76/2.93 type (bytes each) gets frees in use avail bytes
% 2.76/2.93 sym_ent ( 304) 273 0 273 0 81.0 K
% 2.76/2.93 term ( 32) 740354 716682 23672 13604 1164.9 K
% 2.76/2.93 rel ( 40) 649712 610397 39315 25997 2551.2 K
% 2.76/2.93 term_ptr ( 16) 621404 503376 118028 118493 3695.6 K
% 2.76/2.93 formula_ptr_2 ( 56) 0 0 0 0 0.0 K
% 2.76/2.93 fpa_head ( 24) 22068 13170 8898 7439 382.9 K
% 2.76/2.93 fpa_tree ( 56) 33591 33591 0 1735 94.9 K
% 2.76/2.93 context (1288) 133878 133878 0 6 7.5 K
% 2.76/2.93 trail ( 24) 2975401 2975401 0 8 0.2 K
% 2.76/2.93 imd_tree ( 32) 856 98 758 0 23.7 K
% 2.76/2.93 imd_pos (4024) 125268 125268 0 9 35.4 K
% 2.76/2.93 is_tree ( 24) 52415 41963 10452 23768 802.0 K
% 2.76/2.93 is_pos (2424) 2030645 2030645 0 20 47.3 K
% 2.76/2.93 fsub_pos ( 16) 95634 95634 0 1 0.0 K
% 2.76/2.93 literal ( 32) 85241 70719 14522 3629 567.2 K
% 2.76/2.93 clause ( 88) 30727 24631 6096 1113 619.5 K
% 2.76/2.93 list ( 272) 10 3 7 1 2.1 K
% 2.76/2.93 clash_nd ( 80) 312 312 0 2 0.2 K
% 2.76/2.93 clause_ptr ( 16) 14091 8349 5742 1111 107.1 K
% 2.76/2.93 int_ptr ( 16) 272341 222862 49479 10900 943.4 K
% 2.76/2.93 ci_ptr ( 24) 0 0 0 0 0.0 K
% 2.76/2.93 link_node ( 120) 0 0 0 0 0.0 K
% 2.76/2.93 ans_lit_node( 24) 0 0 0 0 0.0 K
% 2.76/2.93 formula_box( 168) 0 0 0 0 0.0 K
% 2.76/2.93 formula( 40) 0 0 0 0 0.0 K
% 2.76/2.93 formula_ptr( 16) 0 0 0 0 0.0 K
% 2.76/2.93 cl_attribute( 24) 0 0 0 0 0.0 K
% 2.76/2.93
% 2.76/2.93 ********** is_delete, can't find end.
% 2.76/2.93 ct time 0.00
% 2.76/2.93 new demod time 0.00
% 2.76/2.93 post_process time 0.00
% 2.76/2.93 back demod time 0.00
% 2.76/2.93 back subsume 0.00
% 2.76/2.93 factor time 0.00
% 2.76/2.93 FINDER time 0.00
% 2.76/2.93 unindex time 0.00
% 2.76/2.93
% 2.76/2.93 Forward subsumption counts, subsumer:number_subsumed.
% 2.76/2.93 1:0 2:0 3:1 4:0 5:0 6:0 7:0 8:0 9:0 10:0
% 2.76/2.93 11:0 12:2 13:0 14:0 15:0 16:0 17:0 18:0 19:5 20:0
% 2.76/2.93 21:0 22:0 23:0 24:1 25:0 26:0 27:0 28:0 29:0 30:0
% 2.76/2.93 31:2 32:0 33:0 34:22 35:21 36:16 37:1 38:1 39:1 40:0
% 2.76/2.93 41:25 42:28 43:0 44:0 45:27 46:0 47:0 48:0 49:0 50:0
% 2.76/2.93 51:0 52:0 53:0 54:0 55:21 56:0 57:0 58:0 59:0 60:0
% 2.76/2.93 61:0 62:0 63:0 64:0 65:0 66:3 67:1 68:0 69:2 70:0
% 2.76/2.93 71:0 72:1 73:0 74:0 75:0 76:0 77:0 78:0 79:0 80:0
% 2.76/2.93 81:0 82:0 83:0 84:0 85:0 86:0 87:0 88:0 89:0 90:0
% 2.76/2.93 91:6 92:6 93:0 94:11 95:0 96:0 97:1 98:0 99:0
% 2.76/2.93 All others: 3572.
% 2.76/2.93
% 2.76/2.93 ********** ABNORMAL END **********
% 2.76/2.93
% 2.76/2.93 ********** is_delete, can't find end.
%------------------------------------------------------------------------------