%------------------------------------------------------------------------------ % File : Otter---3.3 % Problem : NUM413+1 : TPTP v8.1.0. Released v3.2.0. % Transfm : none % Format : tptp:raw % Command : otter-tptp-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 : 300s % DateTime : Wed Jul 27 13:08:16 EDT 2022 % Result : Unknown 36.46s 36.62s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : NUM413+1 : TPTP v8.1.0. Released v3.2.0. % 0.11/0.13 % Command : otter-tptp-script %s % 0.13/0.33 % Computer : n006.cluster.edu % 0.13/0.33 % Model : x86_64 x86_64 % 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.33 % Memory : 8042.1875MB % 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.33 % CPULimit : 300 % 0.13/0.33 % WCLimit : 300 % 0.13/0.33 % DateTime : Wed Jul 27 09:43:47 EDT 2022 % 0.13/0.34 % CPUTime : % 2.44/2.62 ----- Otter 3.3f, August 2004 ----- % 2.44/2.62 The process was started by sandbox2 on n006.cluster.edu, % 2.44/2.62 Wed Jul 27 09:43:47 2022 % 2.44/2.62 The command was "./otter". The process ID is 20265. % 2.44/2.62 % 2.44/2.62 set(prolog_style_variables). % 2.44/2.62 set(auto). % 2.44/2.62 dependent: set(auto1). % 2.44/2.62 dependent: set(process_input). % 2.44/2.62 dependent: clear(print_kept). % 2.44/2.62 dependent: clear(print_new_demod). % 2.44/2.62 dependent: clear(print_back_demod). % 2.44/2.62 dependent: clear(print_back_sub). % 2.44/2.62 dependent: set(control_memory). % 2.44/2.62 dependent: assign(max_mem, 12000). % 2.44/2.62 dependent: assign(pick_given_ratio, 4). % 2.44/2.62 dependent: assign(stats_level, 1). % 2.44/2.62 dependent: assign(max_seconds, 10800). % 2.44/2.62 clear(print_given). % 2.44/2.62 % 2.44/2.62 formula_list(usable). % 2.44/2.62 all A (A=A). % 2.44/2.62 all A B (in(A,B)-> -in(B,A)). % 2.44/2.62 all A (empty(A)->function(A)). % 2.44/2.62 all A (ordinal(A)->epsilon_transitive(A)&epsilon_connected(A)). % 2.44/2.62 all A (empty(A)->relation(A)). % 2.44/2.62 all A (relation(A)&empty(A)&function(A)->relation(A)&function(A)&one_to_one(A)). % 2.44/2.62 all A (epsilon_transitive(A)&epsilon_connected(A)->ordinal(A)). % 2.44/2.62 all A (empty(A)->epsilon_transitive(A)&epsilon_connected(A)&ordinal(A)). % 2.44/2.62 all A B (unordered_pair(A,B)=unordered_pair(B,A)). % 2.44/2.62 all A B (ordinal(A)&ordinal(B)->ordinal_subset(A,B)|ordinal_subset(B,A)). % 2.44/2.62 all A B (A=B<->subset(A,B)&subset(B,A)). % 2.44/2.62 all A (function(A)<-> (all B C D (in(ordered_pair(B,C),A)&in(ordered_pair(B,D),A)->C=D))). % 2.44/2.62 all A (relation(A)<-> (all B (-(in(B,A)& (all C D (B!=ordered_pair(C,D))))))). % 2.44/2.62 all A (epsilon_transitive(A)<-> (all B (in(B,A)->subset(B,A)))). % 2.44/2.62 all A B (subset(A,B)<-> (all C (in(C,A)->in(C,B)))). % 2.44/2.62 all A (relation(A)-> (all B (B=relation_dom(A)<-> (all C (in(C,B)<-> (exists D in(ordered_pair(C,D),A))))))). % 2.44/2.62 all A B (B=union(A)<-> (all C (in(C,B)<-> (exists D (in(C,D)&in(D,A)))))). % 2.44/2.62 all A (relation(A)&function(A)-> (all B (B=relation_rng(A)<-> (all C (in(C,B)<-> (exists D (in(D,relation_dom(A))&C=apply(A,D)))))))). % 2.44/2.62 all A B (ordered_pair(A,B)=unordered_pair(unordered_pair(A,B),singleton(A))). % 2.44/2.62 all A (relation(A)&function(A)-> (transfinite_se_quence(A)<->ordinal(relation_dom(A)))). % 2.44/2.62 all A (inclusion_linear(A)<-> (all B C (in(B,A)&in(C,A)->inclusion_comparable(B,C)))). % 2.44/2.62 all A B (inclusion_comparable(A,B)<->subset(A,B)|subset(B,A)). % 2.44/2.62 all A exists B element(B,A). % 2.44/2.62 empty(empty_set). % 2.44/2.62 relation(empty_set). % 2.44/2.62 relation_empty_yielding(empty_set). % 2.44/2.62 empty(empty_set). % 2.44/2.62 all A B (-empty(ordered_pair(A,B))). % 2.44/2.62 relation(empty_set). % 2.44/2.62 relation_empty_yielding(empty_set). % 2.44/2.62 function(empty_set). % 2.44/2.62 one_to_one(empty_set). % 2.44/2.62 empty(empty_set). % 2.44/2.62 epsilon_transitive(empty_set). % 2.44/2.62 epsilon_connected(empty_set). % 2.44/2.62 ordinal(empty_set). % 2.44/2.62 all A (ordinal(A)->epsilon_transitive(union(A))&epsilon_connected(union(A))&ordinal(union(A))). % 2.44/2.62 empty(empty_set). % 2.44/2.62 relation(empty_set). % 2.44/2.62 all A (relation(A)&function(A)&transfinite_se_quence(A)->epsilon_transitive(relation_dom(A))&epsilon_connected(relation_dom(A))&ordinal(relation_dom(A))). % 2.44/2.62 all A (-empty(A)&relation(A)-> -empty(relation_dom(A))). % 2.44/2.62 all A (relation(A)&relation_non_empty(A)&function(A)->with_non_empty_elements(relation_rng(A))). % 2.44/2.62 all A (-empty(A)&relation(A)-> -empty(relation_rng(A))). % 2.44/2.62 all A (empty(A)->empty(relation_dom(A))&relation(relation_dom(A))). % 2.44/2.62 all A (empty(A)->empty(relation_rng(A))&relation(relation_rng(A))). % 2.44/2.62 exists A (relation(A)&function(A)). % 2.44/2.62 exists A (epsilon_transitive(A)&epsilon_connected(A)&ordinal(A)). % 2.44/2.62 exists A (empty(A)&relation(A)). % 2.44/2.62 exists A empty(A). % 2.44/2.62 exists A (relation(A)&empty(A)&function(A)). % 2.44/2.62 exists A (relation(A)&function(A)&one_to_one(A)&empty(A)&epsilon_transitive(A)&epsilon_connected(A)&ordinal(A)). % 2.44/2.62 exists A (-empty(A)&relation(A)). % 2.44/2.62 exists A (-empty(A)). % 2.44/2.62 exists A (relation(A)&function(A)&one_to_one(A)). % 2.44/2.62 exists A (-empty(A)&epsilon_transitive(A)&epsilon_connected(A)&ordinal(A)). % 2.44/2.62 exists A (relation(A)&relation_empty_yielding(A)). % 2.44/2.62 exists A (relation(A)&relation_empty_yielding(A)&function(A)). % 2.44/2.62 exists A (relation(A)&function(A)&transfinite_se_quence(A)). % 2.44/2.62 exists A (relation(A)&relation_non_empty(A)&function(A)). % 2.44/2.62 all A B (ordinal(A)&ordinal(B)-> (ordinal_subset(A,B)<->subset(A,B))). % 2.44/2.62 all A B (ordinal(A)&ordinal(B)->ordinal_subset(A,A)). % 2.44/2.62 all A B subset(A,A). % 2.44/2.62 all A B inclusion_comparable(A,A). % 2.44/2.62 all A ((all B C D (in(B,A)& (all E (relation(E)&function(E)&transfinite_se_quence(E)-> (E=B->relation_dom(E)=C)))&in(B,A)& (all F (relation(F)&function(F)&transfinite_se_quence(F)-> (F=B->relation_dom(F)=D)))->C=D))-> (exists B (relation(B)&function(B)& (all C D (in(ordered_pair(C,D),B)<->in(C,A)&in(C,A)& (all G (relation(G)&function(G)&transfinite_se_quence(G)-> (G=C->relation_dom(G)=D)))))))). % 2.44/2.63 all A (relation(A)&function(A)-> ((exists B (ordinal(B)& (all C (ordinal(C)-> (in(C,relation_rng(A))->ordinal_subset(C,B))))))-> (exists B (ordinal(B)& (all D (ordinal(D)-> (in(D,relation_rng(A))->ordinal_subset(D,B))))& (all E (ordinal(E)-> ((all F (ordinal(F)-> (in(F,relation_rng(A))->ordinal_subset(F,E))))->ordinal_subset(B,E)))))))). % 2.44/2.63 all A B (inclusion_comparable(A,B)->inclusion_comparable(B,A)). % 2.44/2.63 all A B (in(A,B)->element(A,B)). % 2.44/2.63 all A B (ordinal(B)-> (in(A,B)->ordinal(A))). % 2.44/2.63 all A (ordinal(A)-> (all B (ordinal(B)->ordinal_subset(A,B)|in(B,A)))). % 2.44/2.63 all A B (element(A,B)->empty(B)|in(A,B)). % 2.44/2.63 all A (-((all B (in(B,A)->ordinal(B)))& (all B (ordinal(B)-> -subset(A,B))))). % 2.44/2.63 all A B (element(A,powerset(B))<->subset(A,B)). % 2.44/2.63 -(all A ((all B (in(B,A)->relation(B)&function(B)&transfinite_se_quence(B)))&inclusion_linear(A)->relation(union(A))&function(union(A))&transfinite_se_quence(union(A)))). % 2.44/2.63 all A B C (in(A,B)&element(B,powerset(C))->element(A,C)). % 2.44/2.63 all A B C (-(in(A,B)&element(B,powerset(C))&empty(C))). % 2.44/2.63 all A (empty(A)->A=empty_set). % 2.44/2.63 all A B (-(in(A,B)&empty(B))). % 2.44/2.63 all A B (-(empty(A)&A!=B&empty(B))). % 2.44/2.63 all A B C (relation(C)&function(C)-> (in(ordered_pair(A,B),C)<->in(A,relation_dom(C))&B=apply(C,A))). % 2.44/2.63 all A B (in(A,B)->subset(A,union(B))). % 2.44/2.63 end_of_list. % 2.44/2.63 % 2.44/2.63 -------> usable clausifies to: % 2.44/2.63 % 2.44/2.63 list(usable). % 2.44/2.63 0 [] A=A. % 2.44/2.63 0 [] -in(A,B)| -in(B,A). % 2.44/2.63 0 [] -empty(A)|function(A). % 2.44/2.63 0 [] -ordinal(A)|epsilon_transitive(A). % 2.44/2.63 0 [] -ordinal(A)|epsilon_connected(A). % 2.44/2.63 0 [] -empty(A)|relation(A). % 2.44/2.63 0 [] -relation(A)| -empty(A)| -function(A)|one_to_one(A). % 2.44/2.63 0 [] -epsilon_transitive(A)| -epsilon_connected(A)|ordinal(A). % 2.44/2.63 0 [] -empty(A)|epsilon_transitive(A). % 2.44/2.63 0 [] -empty(A)|epsilon_connected(A). % 2.44/2.63 0 [] -empty(A)|ordinal(A). % 2.44/2.63 0 [] unordered_pair(A,B)=unordered_pair(B,A). % 2.44/2.63 0 [] -ordinal(A)| -ordinal(B)|ordinal_subset(A,B)|ordinal_subset(B,A). % 2.44/2.63 0 [] A!=B|subset(A,B). % 2.44/2.63 0 [] A!=B|subset(B,A). % 2.44/2.63 0 [] A=B| -subset(A,B)| -subset(B,A). % 2.44/2.63 0 [] -function(A)| -in(ordered_pair(B,C),A)| -in(ordered_pair(B,D),A)|C=D. % 2.44/2.63 0 [] function(A)|in(ordered_pair($f3(A),$f2(A)),A). % 2.44/2.63 0 [] function(A)|in(ordered_pair($f3(A),$f1(A)),A). % 2.44/2.63 0 [] function(A)|$f2(A)!=$f1(A). % 2.44/2.63 0 [] -relation(A)| -in(B,A)|B=ordered_pair($f5(A,B),$f4(A,B)). % 2.44/2.63 0 [] relation(A)|in($f6(A),A). % 2.44/2.63 0 [] relation(A)|$f6(A)!=ordered_pair(C,D). % 2.44/2.63 0 [] -epsilon_transitive(A)| -in(B,A)|subset(B,A). % 2.44/2.63 0 [] epsilon_transitive(A)|in($f7(A),A). % 2.44/2.63 0 [] epsilon_transitive(A)| -subset($f7(A),A). % 2.44/2.63 0 [] -subset(A,B)| -in(C,A)|in(C,B). % 2.44/2.63 0 [] subset(A,B)|in($f8(A,B),A). % 2.44/2.63 0 [] subset(A,B)| -in($f8(A,B),B). % 2.44/2.63 0 [] -relation(A)|B!=relation_dom(A)| -in(C,B)|in(ordered_pair(C,$f9(A,B,C)),A). % 2.44/2.63 0 [] -relation(A)|B!=relation_dom(A)|in(C,B)| -in(ordered_pair(C,D),A). % 2.44/2.63 0 [] -relation(A)|B=relation_dom(A)|in($f11(A,B),B)|in(ordered_pair($f11(A,B),$f10(A,B)),A). % 2.44/2.63 0 [] -relation(A)|B=relation_dom(A)| -in($f11(A,B),B)| -in(ordered_pair($f11(A,B),X1),A). % 2.44/2.63 0 [] B!=union(A)| -in(C,B)|in(C,$f12(A,B,C)). % 2.44/2.63 0 [] B!=union(A)| -in(C,B)|in($f12(A,B,C),A). % 2.44/2.63 0 [] B!=union(A)|in(C,B)| -in(C,D)| -in(D,A). % 2.44/2.63 0 [] B=union(A)|in($f14(A,B),B)|in($f14(A,B),$f13(A,B)). % 2.44/2.63 0 [] B=union(A)|in($f14(A,B),B)|in($f13(A,B),A). % 2.44/2.63 0 [] B=union(A)| -in($f14(A,B),B)| -in($f14(A,B),X2)| -in(X2,A). % 2.44/2.63 0 [] -relation(A)| -function(A)|B!=relation_rng(A)| -in(C,B)|in($f15(A,B,C),relation_dom(A)). % 2.44/2.63 0 [] -relation(A)| -function(A)|B!=relation_rng(A)| -in(C,B)|C=apply(A,$f15(A,B,C)). % 2.44/2.63 0 [] -relation(A)| -function(A)|B!=relation_rng(A)|in(C,B)| -in(D,relation_dom(A))|C!=apply(A,D). % 2.44/2.63 0 [] -relation(A)| -function(A)|B=relation_rng(A)|in($f17(A,B),B)|in($f16(A,B),relation_dom(A)). % 2.44/2.63 0 [] -relation(A)| -function(A)|B=relation_rng(A)|in($f17(A,B),B)|$f17(A,B)=apply(A,$f16(A,B)). % 2.44/2.63 0 [] -relation(A)| -function(A)|B=relation_rng(A)| -in($f17(A,B),B)| -in(X3,relation_dom(A))|$f17(A,B)!=apply(A,X3). % 2.44/2.63 0 [] ordered_pair(A,B)=unordered_pair(unordered_pair(A,B),singleton(A)). % 2.44/2.63 0 [] -relation(A)| -function(A)| -transfinite_se_quence(A)|ordinal(relation_dom(A)). % 2.44/2.63 0 [] -relation(A)| -function(A)|transfinite_se_quence(A)| -ordinal(relation_dom(A)). % 2.44/2.63 0 [] -inclusion_linear(A)| -in(B,A)| -in(C,A)|inclusion_comparable(B,C). % 2.44/2.63 0 [] inclusion_linear(A)|in($f19(A),A). % 2.44/2.63 0 [] inclusion_linear(A)|in($f18(A),A). % 2.44/2.63 0 [] inclusion_linear(A)| -inclusion_comparable($f19(A),$f18(A)). % 2.44/2.63 0 [] -inclusion_comparable(A,B)|subset(A,B)|subset(B,A). % 2.44/2.63 0 [] inclusion_comparable(A,B)| -subset(A,B). % 2.44/2.63 0 [] inclusion_comparable(A,B)| -subset(B,A). % 2.44/2.63 0 [] element($f20(A),A). % 2.44/2.63 0 [] empty(empty_set). % 2.44/2.63 0 [] relation(empty_set). % 2.44/2.63 0 [] relation_empty_yielding(empty_set). % 2.44/2.63 0 [] empty(empty_set). % 2.44/2.63 0 [] -empty(ordered_pair(A,B)). % 2.44/2.63 0 [] relation(empty_set). % 2.44/2.63 0 [] relation_empty_yielding(empty_set). % 2.44/2.63 0 [] function(empty_set). % 2.44/2.63 0 [] one_to_one(empty_set). % 2.44/2.63 0 [] empty(empty_set). % 2.44/2.63 0 [] epsilon_transitive(empty_set). % 2.44/2.63 0 [] epsilon_connected(empty_set). % 2.44/2.63 0 [] ordinal(empty_set). % 2.44/2.63 0 [] -ordinal(A)|epsilon_transitive(union(A)). % 2.44/2.63 0 [] -ordinal(A)|epsilon_connected(union(A)). % 2.44/2.63 0 [] -ordinal(A)|ordinal(union(A)). % 2.44/2.63 0 [] empty(empty_set). % 2.44/2.63 0 [] relation(empty_set). % 2.44/2.63 0 [] -relation(A)| -function(A)| -transfinite_se_quence(A)|epsilon_transitive(relation_dom(A)). % 2.44/2.63 0 [] -relation(A)| -function(A)| -transfinite_se_quence(A)|epsilon_connected(relation_dom(A)). % 2.44/2.63 0 [] -relation(A)| -function(A)| -transfinite_se_quence(A)|ordinal(relation_dom(A)). % 2.44/2.63 0 [] empty(A)| -relation(A)| -empty(relation_dom(A)). % 2.44/2.63 0 [] -relation(A)| -relation_non_empty(A)| -function(A)|with_non_empty_elements(relation_rng(A)). % 2.44/2.63 0 [] empty(A)| -relation(A)| -empty(relation_rng(A)). % 2.44/2.63 0 [] -empty(A)|empty(relation_dom(A)). % 2.44/2.63 0 [] -empty(A)|relation(relation_dom(A)). % 2.44/2.63 0 [] -empty(A)|empty(relation_rng(A)). % 2.44/2.63 0 [] -empty(A)|relation(relation_rng(A)). % 2.44/2.63 0 [] relation($c1). % 2.44/2.63 0 [] function($c1). % 2.44/2.63 0 [] epsilon_transitive($c2). % 2.44/2.63 0 [] epsilon_connected($c2). % 2.44/2.63 0 [] ordinal($c2). % 2.44/2.63 0 [] empty($c3). % 2.44/2.63 0 [] relation($c3). % 2.44/2.63 0 [] empty($c4). % 2.44/2.63 0 [] relation($c5). % 2.44/2.63 0 [] empty($c5). % 2.44/2.63 0 [] function($c5). % 2.44/2.63 0 [] relation($c6). % 2.44/2.63 0 [] function($c6). % 2.44/2.63 0 [] one_to_one($c6). % 2.44/2.63 0 [] empty($c6). % 2.44/2.63 0 [] epsilon_transitive($c6). % 2.44/2.63 0 [] epsilon_connected($c6). % 2.44/2.63 0 [] ordinal($c6). % 2.44/2.63 0 [] -empty($c7). % 2.44/2.63 0 [] relation($c7). % 2.44/2.63 0 [] -empty($c8). % 2.44/2.63 0 [] relation($c9). % 2.44/2.63 0 [] function($c9). % 2.44/2.63 0 [] one_to_one($c9). % 2.44/2.63 0 [] -empty($c10). % 2.44/2.63 0 [] epsilon_transitive($c10). % 2.44/2.63 0 [] epsilon_connected($c10). % 2.44/2.63 0 [] ordinal($c10). % 2.44/2.63 0 [] relation($c11). % 2.44/2.63 0 [] relation_empty_yielding($c11). % 2.44/2.63 0 [] relation($c12). % 2.44/2.63 0 [] relation_empty_yielding($c12). % 2.44/2.63 0 [] function($c12). % 2.44/2.63 0 [] relation($c13). % 2.44/2.63 0 [] function($c13). % 2.44/2.63 0 [] transfinite_se_quence($c13). % 2.44/2.63 0 [] relation($c14). % 2.44/2.63 0 [] relation_non_empty($c14). % 2.44/2.63 0 [] function($c14). % 2.44/2.63 0 [] -ordinal(A)| -ordinal(B)| -ordinal_subset(A,B)|subset(A,B). % 2.44/2.63 0 [] -ordinal(A)| -ordinal(B)|ordinal_subset(A,B)| -subset(A,B). % 2.44/2.63 0 [] -ordinal(A)| -ordinal(B)|ordinal_subset(A,A). % 2.44/2.63 0 [] subset(A,A). % 2.44/2.63 0 [] inclusion_comparable(A,A). % 2.44/2.63 0 [] in($f23(A),A)|relation($f25(A)). % 2.44/2.63 0 [] in($f23(A),A)|function($f25(A)). % 2.44/2.63 0 [] in($f23(A),A)| -in(ordered_pair(C,D),$f25(A))|in(C,A). % 2.44/2.63 0 [] in($f23(A),A)| -in(ordered_pair(C,D),$f25(A))| -relation(G)| -function(G)| -transfinite_se_quence(G)|G!=C|relation_dom(G)=D. % 2.44/2.63 0 [] in($f23(A),A)|in(ordered_pair(C,D),$f25(A))| -in(C,A)|relation($f24(A,C,D)). % 2.44/2.63 0 [] in($f23(A),A)|in(ordered_pair(C,D),$f25(A))| -in(C,A)|function($f24(A,C,D)). % 2.44/2.63 0 [] in($f23(A),A)|in(ordered_pair(C,D),$f25(A))| -in(C,A)|transfinite_se_quence($f24(A,C,D)). % 2.44/2.63 0 [] in($f23(A),A)|in(ordered_pair(C,D),$f25(A))| -in(C,A)|$f24(A,C,D)=C. % 2.44/2.63 0 [] in($f23(A),A)|in(ordered_pair(C,D),$f25(A))| -in(C,A)|relation_dom($f24(A,C,D))!=D. % 2.44/2.63 0 [] -relation(E)| -function(E)| -transfinite_se_quence(E)|E!=$f23(A)|relation_dom(E)=$f22(A)|relation($f25(A)). % 2.44/2.63 0 [] -relation(E)| -function(E)| -transfinite_se_quence(E)|E!=$f23(A)|relation_dom(E)=$f22(A)|function($f25(A)). % 2.44/2.63 0 [] -relation(E)| -function(E)| -transfinite_se_quence(E)|E!=$f23(A)|relation_dom(E)=$f22(A)| -in(ordered_pair(C,D),$f25(A))|in(C,A). % 2.44/2.63 0 [] -relation(E)| -function(E)| -transfinite_se_quence(E)|E!=$f23(A)|relation_dom(E)=$f22(A)| -in(ordered_pair(C,D),$f25(A))| -relation(G)| -function(G)| -transfinite_se_quence(G)|G!=C|relation_dom(G)=D. % 2.44/2.63 0 [] -relation(E)| -function(E)| -transfinite_se_quence(E)|E!=$f23(A)|relation_dom(E)=$f22(A)|in(ordered_pair(C,D),$f25(A))| -in(C,A)|relation($f24(A,C,D)). % 2.44/2.63 0 [] -relation(E)| -function(E)| -transfinite_se_quence(E)|E!=$f23(A)|relation_dom(E)=$f22(A)|in(ordered_pair(C,D),$f25(A))| -in(C,A)|function($f24(A,C,D)). % 2.44/2.63 0 [] -relation(E)| -function(E)| -transfinite_se_quence(E)|E!=$f23(A)|relation_dom(E)=$f22(A)|in(ordered_pair(C,D),$f25(A))| -in(C,A)|transfinite_se_quence($f24(A,C,D)). % 2.44/2.63 0 [] -relation(E)| -function(E)| -transfinite_se_quence(E)|E!=$f23(A)|relation_dom(E)=$f22(A)|in(ordered_pair(C,D),$f25(A))| -in(C,A)|$f24(A,C,D)=C. % 2.44/2.63 0 [] -relation(E)| -function(E)| -transfinite_se_quence(E)|E!=$f23(A)|relation_dom(E)=$f22(A)|in(ordered_pair(C,D),$f25(A))| -in(C,A)|relation_dom($f24(A,C,D))!=D. % 2.44/2.63 0 [] -relation(F)| -function(F)| -transfinite_se_quence(F)|F!=$f23(A)|relation_dom(F)=$f21(A)|relation($f25(A)). % 2.44/2.63 0 [] -relation(F)| -function(F)| -transfinite_se_quence(F)|F!=$f23(A)|relation_dom(F)=$f21(A)|function($f25(A)). % 2.44/2.63 0 [] -relation(F)| -function(F)| -transfinite_se_quence(F)|F!=$f23(A)|relation_dom(F)=$f21(A)| -in(ordered_pair(C,D),$f25(A))|in(C,A). % 2.44/2.63 0 [] -relation(F)| -function(F)| -transfinite_se_quence(F)|F!=$f23(A)|relation_dom(F)=$f21(A)| -in(ordered_pair(C,D),$f25(A))| -relation(G)| -function(G)| -transfinite_se_quence(G)|G!=C|relation_dom(G)=D. % 2.44/2.63 0 [] -relation(F)| -function(F)| -transfinite_se_quence(F)|F!=$f23(A)|relation_dom(F)=$f21(A)|in(ordered_pair(C,D),$f25(A))| -in(C,A)|relation($f24(A,C,D)). % 2.44/2.63 0 [] -relation(F)| -function(F)| -transfinite_se_quence(F)|F!=$f23(A)|relation_dom(F)=$f21(A)|in(ordered_pair(C,D),$f25(A))| -in(C,A)|function($f24(A,C,D)). % 2.44/2.63 0 [] -relation(F)| -function(F)| -transfinite_se_quence(F)|F!=$f23(A)|relation_dom(F)=$f21(A)|in(ordered_pair(C,D),$f25(A))| -in(C,A)|transfinite_se_quence($f24(A,C,D)). % 2.44/2.63 0 [] -relation(F)| -function(F)| -transfinite_se_quence(F)|F!=$f23(A)|relation_dom(F)=$f21(A)|in(ordered_pair(C,D),$f25(A))| -in(C,A)|$f24(A,C,D)=C. % 2.44/2.63 0 [] -relation(F)| -function(F)| -transfinite_se_quence(F)|F!=$f23(A)|relation_dom(F)=$f21(A)|in(ordered_pair(C,D),$f25(A))| -in(C,A)|relation_dom($f24(A,C,D))!=D. % 2.44/2.63 0 [] $f22(A)!=$f21(A)|relation($f25(A)). % 2.44/2.63 0 [] $f22(A)!=$f21(A)|function($f25(A)). % 2.44/2.63 0 [] $f22(A)!=$f21(A)| -in(ordered_pair(C,D),$f25(A))|in(C,A). % 2.44/2.63 0 [] $f22(A)!=$f21(A)| -in(ordered_pair(C,D),$f25(A))| -relation(G)| -function(G)| -transfinite_se_quence(G)|G!=C|relation_dom(G)=D. % 2.44/2.63 0 [] $f22(A)!=$f21(A)|in(ordered_pair(C,D),$f25(A))| -in(C,A)|relation($f24(A,C,D)). % 2.44/2.63 0 [] $f22(A)!=$f21(A)|in(ordered_pair(C,D),$f25(A))| -in(C,A)|function($f24(A,C,D)). % 2.44/2.63 0 [] $f22(A)!=$f21(A)|in(ordered_pair(C,D),$f25(A))| -in(C,A)|transfinite_se_quence($f24(A,C,D)). % 2.44/2.63 0 [] $f22(A)!=$f21(A)|in(ordered_pair(C,D),$f25(A))| -in(C,A)|$f24(A,C,D)=C. % 2.44/2.63 0 [] $f22(A)!=$f21(A)|in(ordered_pair(C,D),$f25(A))| -in(C,A)|relation_dom($f24(A,C,D))!=D. % 2.44/2.63 0 [] -relation(A)| -function(A)| -ordinal(B)|ordinal($f26(A,B))|ordinal($f28(A)). % 2.44/2.63 0 [] -relation(A)| -function(A)| -ordinal(B)|ordinal($f26(A,B))| -ordinal(D)| -in(D,relation_rng(A))|ordinal_subset(D,$f28(A)). % 2.44/2.63 0 [] -relation(A)| -function(A)| -ordinal(B)|ordinal($f26(A,B))| -ordinal(E)|ordinal($f27(A,E))|ordinal_subset($f28(A),E). % 2.44/2.63 0 [] -relation(A)| -function(A)| -ordinal(B)|ordinal($f26(A,B))| -ordinal(E)|in($f27(A,E),relation_rng(A))|ordinal_subset($f28(A),E). % 2.44/2.63 0 [] -relation(A)| -function(A)| -ordinal(B)|ordinal($f26(A,B))| -ordinal(E)| -ordinal_subset($f27(A,E),E)|ordinal_subset($f28(A),E). % 2.44/2.63 0 [] -relation(A)| -function(A)| -ordinal(B)|in($f26(A,B),relation_rng(A))|ordinal($f28(A)). % 2.44/2.63 0 [] -relation(A)| -function(A)| -ordinal(B)|in($f26(A,B),relation_rng(A))| -ordinal(D)| -in(D,relation_rng(A))|ordinal_subset(D,$f28(A)). % 2.44/2.63 0 [] -relation(A)| -function(A)| -ordinal(B)|in($f26(A,B),relation_rng(A))| -ordinal(E)|ordinal($f27(A,E))|ordinal_subset($f28(A),E). % 2.44/2.63 0 [] -relation(A)| -function(A)| -ordinal(B)|in($f26(A,B),relation_rng(A))| -ordinal(E)|in($f27(A,E),relation_rng(A))|ordinal_subset($f28(A),E). % 2.44/2.63 0 [] -relation(A)| -function(A)| -ordinal(B)|in($f26(A,B),relation_rng(A))| -ordinal(E)| -ordinal_subset($f27(A,E),E)|ordinal_subset($f28(A),E). % 2.44/2.63 0 [] -relation(A)| -function(A)| -ordinal(B)| -ordinal_subset($f26(A,B),B)|ordinal($f28(A)). % 2.44/2.63 0 [] -relation(A)| -function(A)| -ordinal(B)| -ordinal_subset($f26(A,B),B)| -ordinal(D)| -in(D,relation_rng(A))|ordinal_subset(D,$f28(A)). % 2.44/2.63 0 [] -relation(A)| -function(A)| -ordinal(B)| -ordinal_subset($f26(A,B),B)| -ordinal(E)|ordinal($f27(A,E))|ordinal_subset($f28(A),E). % 2.44/2.63 0 [] -relation(A)| -function(A)| -ordinal(B)| -ordinal_subset($f26(A,B),B)| -ordinal(E)|in($f27(A,E),relation_rng(A))|ordinal_subset($f28(A),E). % 2.44/2.63 0 [] -relation(A)| -function(A)| -ordinal(B)| -ordinal_subset($f26(A,B),B)| -ordinal(E)| -ordinal_subset($f27(A,E),E)|ordinal_subset($f28(A),E). % 2.44/2.63 0 [] -inclusion_comparable(A,B)|inclusion_comparable(B,A). % 2.44/2.63 0 [] -in(A,B)|element(A,B). % 2.44/2.63 0 [] -ordinal(B)| -in(A,B)|ordinal(A). % 2.44/2.63 0 [] -ordinal(A)| -ordinal(B)|ordinal_subset(A,B)|in(B,A). % 2.44/2.63 0 [] -element(A,B)|empty(B)|in(A,B). % 2.44/2.63 0 [] in($f29(A),A)|ordinal($f30(A)). % 2.44/2.63 0 [] in($f29(A),A)|subset(A,$f30(A)). % 2.44/2.63 0 [] -ordinal($f29(A))|ordinal($f30(A)). % 2.44/2.63 0 [] -ordinal($f29(A))|subset(A,$f30(A)). % 2.44/2.63 0 [] -element(A,powerset(B))|subset(A,B). % 2.44/2.63 0 [] element(A,powerset(B))| -subset(A,B). % 2.44/2.63 0 [] -in(B,$c15)|relation(B). % 2.44/2.63 0 [] -in(B,$c15)|function(B). % 2.44/2.63 0 [] -in(B,$c15)|transfinite_se_quence(B). % 2.44/2.63 0 [] inclusion_linear($c15). % 2.44/2.63 0 [] -relation(union($c15))| -function(union($c15))| -transfinite_se_quence(union($c15)). % 2.44/2.63 0 [] -in(A,B)| -element(B,powerset(C))|element(A,C). % 2.44/2.63 0 [] -in(A,B)| -element(B,powerset(C))| -empty(C). % 2.44/2.63 0 [] -empty(A)|A=empty_set. % 2.44/2.63 0 [] -in(A,B)| -empty(B). % 2.44/2.63 0 [] -empty(A)|A=B| -empty(B). % 2.44/2.63 0 [] -relation(C)| -function(C)| -in(ordered_pair(A,B),C)|in(A,relation_dom(C)). % 2.44/2.63 0 [] -relation(C)| -function(C)| -in(ordered_pair(A,B),C)|B=apply(C,A). % 2.44/2.63 0 [] -relation(C)| -function(C)|in(ordered_pair(A,B),C)| -in(A,relation_dom(C))|B!=apply(C,A). % 2.44/2.63 0 [] -in(A,B)|subset(A,union(B)). % 2.44/2.63 end_of_list. % 2.44/2.63 % 2.44/2.63 SCAN INPUT: prop=0, horn=0, equality=1, symmetry=0, max_lits=11. % 2.44/2.63 % 2.44/2.63 This ia a non-Horn set with equality. The strategy will be % 2.44/2.63 Knuth-Bendix, ordered hyper_res, factoring, and unit % 2.44/2.63 deletion, with positive clauses in sos and nonpositive % 2.44/2.63 clauses in usable. % 2.44/2.63 % 2.44/2.63 dependent: set(knuth_bendix). % 2.44/2.63 dependent: set(anl_eq). % 2.44/2.63 dependent: set(para_from). % 2.44/2.63 dependent: set(para_into). % 2.44/2.63 dependent: clear(para_from_right). % 2.44/2.63 dependent: clear(para_into_right). % 2.44/2.63 dependent: set(para_from_vars). % 2.44/2.63 dependent: set(eq_units_both_ways). % 2.44/2.63 dependent: set(dynamic_demod_all). % 2.44/2.63 dependent: set(dynamic_demod). % 2.44/2.63 dependent: set(order_eq). % 2.44/2.63 dependent: set(back_demod). % 2.44/2.63 dependent: set(lrpo). % 2.44/2.63 dependent: set(hyper_res). % 2.44/2.63 dependent: set(unit_deletion). % 2.44/2.63 dependent: set(factor). % 2.44/2.63 % 2.44/2.63 ------------> process usable: % 2.44/2.63 ** KEPT (pick-wt=6): 1 [] -in(A,B)| -in(B,A). % 2.44/2.63 ** KEPT (pick-wt=4): 2 [] -empty(A)|function(A). % 2.44/2.63 ** KEPT (pick-wt=4): 3 [] -ordinal(A)|epsilon_transitive(A). % 2.44/2.63 ** KEPT (pick-wt=4): 4 [] -ordinal(A)|epsilon_connected(A). % 2.44/2.63 ** KEPT (pick-wt=4): 5 [] -empty(A)|relation(A). % 2.44/2.63 ** KEPT (pick-wt=8): 6 [] -relation(A)| -empty(A)| -function(A)|one_to_one(A). % 2.44/2.63 ** KEPT (pick-wt=6): 7 [] -epsilon_transitive(A)| -epsilon_connected(A)|ordinal(A). % 2.44/2.63 ** KEPT (pick-wt=4): 8 [] -empty(A)|epsilon_transitive(A). % 2.44/2.63 ** KEPT (pick-wt=4): 9 [] -empty(A)|epsilon_connected(A). % 2.44/2.63 ** KEPT (pick-wt=4): 10 [] -empty(A)|ordinal(A). % 2.44/2.63 ** KEPT (pick-wt=10): 11 [] -ordinal(A)| -ordinal(B)|ordinal_subset(A,B)|ordinal_subset(B,A). % 2.44/2.63 ** KEPT (pick-wt=6): 12 [] A!=B|subset(A,B). % 2.44/2.63 ** KEPT (pick-wt=6): 13 [] A!=B|subset(B,A). % 2.44/2.63 ** KEPT (pick-wt=9): 14 [] A=B| -subset(A,B)| -subset(B,A). % 2.44/2.63 ** KEPT (pick-wt=15): 15 [] -function(A)| -in(ordered_pair(B,C),A)| -in(ordered_pair(B,D),A)|C=D. % 2.44/2.63 ** KEPT (pick-wt=7): 16 [] function(A)|$f2(A)!=$f1(A). % 2.44/2.63 ** KEPT (pick-wt=14): 18 [copy,17,flip.3] -relation(A)| -in(B,A)|ordered_pair($f5(A,B),$f4(A,B))=B. % 2.44/2.63 ** KEPT (pick-wt=8): 19 [] relation(A)|$f6(A)!=ordered_pair(B,C). % 2.44/2.63 ** KEPT (pick-wt=8): 20 [] -epsilon_transitive(A)| -in(B,A)|subset(B,A). % 2.44/2.63 ** KEPT (pick-wt=6): 21 [] epsilon_transitive(A)| -subset($f7(A),A). % 2.44/2.63 ** KEPT (pick-wt=9): 22 [] -subset(A,B)| -in(C,A)|in(C,B). % 2.44/2.64 ** KEPT (pick-wt=8): 23 [] subset(A,B)| -in($f8(A,B),B). % 2.44/2.64 ** KEPT (pick-wt=17): 24 [] -relation(A)|B!=relation_dom(A)| -in(C,B)|in(ordered_pair(C,$f9(A,B,C)),A). % 2.44/2.64 ** KEPT (pick-wt=14): 25 [] -relation(A)|B!=relation_dom(A)|in(C,B)| -in(ordered_pair(C,D),A). % 2.44/2.64 ** KEPT (pick-wt=20): 26 [] -relation(A)|B=relation_dom(A)|in($f11(A,B),B)|in(ordered_pair($f11(A,B),$f10(A,B)),A). % 2.44/2.64 ** KEPT (pick-wt=18): 27 [] -relation(A)|B=relation_dom(A)| -in($f11(A,B),B)| -in(ordered_pair($f11(A,B),C),A). % 2.44/2.64 ** KEPT (pick-wt=13): 28 [] A!=union(B)| -in(C,A)|in(C,$f12(B,A,C)). % 2.44/2.64 ** KEPT (pick-wt=13): 29 [] A!=union(B)| -in(C,A)|in($f12(B,A,C),B). % 2.44/2.64 ** KEPT (pick-wt=13): 30 [] A!=union(B)|in(C,A)| -in(C,D)| -in(D,B). % 2.44/2.64 ** KEPT (pick-wt=17): 31 [] A=union(B)| -in($f14(B,A),A)| -in($f14(B,A),C)| -in(C,B). % 2.44/2.64 ** KEPT (pick-wt=18): 32 [] -relation(A)| -function(A)|B!=relation_rng(A)| -in(C,B)|in($f15(A,B,C),relation_dom(A)). % 2.44/2.64 ** KEPT (pick-wt=19): 34 [copy,33,flip.5] -relation(A)| -function(A)|B!=relation_rng(A)| -in(C,B)|apply(A,$f15(A,B,C))=C. % 2.44/2.64 ** KEPT (pick-wt=20): 35 [] -relation(A)| -function(A)|B!=relation_rng(A)|in(C,B)| -in(D,relation_dom(A))|C!=apply(A,D). % 2.44/2.64 ** KEPT (pick-wt=19): 36 [] -relation(A)| -function(A)|B=relation_rng(A)|in($f17(A,B),B)|in($f16(A,B),relation_dom(A)). % 2.44/2.64 ** KEPT (pick-wt=22): 38 [copy,37,flip.5] -relation(A)| -function(A)|B=relation_rng(A)|in($f17(A,B),B)|apply(A,$f16(A,B))=$f17(A,B). % 2.44/2.64 ** KEPT (pick-wt=24): 39 [] -relation(A)| -function(A)|B=relation_rng(A)| -in($f17(A,B),B)| -in(C,relation_dom(A))|$f17(A,B)!=apply(A,C). % 2.44/2.64 ** KEPT (pick-wt=9): 40 [] -relation(A)| -function(A)| -transfinite_se_quence(A)|ordinal(relation_dom(A)). % 2.44/2.64 ** KEPT (pick-wt=9): 41 [] -relation(A)| -function(A)|transfinite_se_quence(A)| -ordinal(relation_dom(A)). % 2.44/2.64 ** KEPT (pick-wt=11): 42 [] -inclusion_linear(A)| -in(B,A)| -in(C,A)|inclusion_comparable(B,C). % 2.44/2.64 ** KEPT (pick-wt=7): 43 [] inclusion_linear(A)| -inclusion_comparable($f19(A),$f18(A)). % 2.44/2.64 ** KEPT (pick-wt=9): 44 [] -inclusion_comparable(A,B)|subset(A,B)|subset(B,A). % 2.44/2.64 ** KEPT (pick-wt=6): 45 [] inclusion_comparable(A,B)| -subset(A,B). % 2.44/2.64 ** KEPT (pick-wt=6): 46 [] inclusion_comparable(A,B)| -subset(B,A). % 2.44/2.64 ** KEPT (pick-wt=4): 47 [] -empty(ordered_pair(A,B)). % 2.44/2.64 ** KEPT (pick-wt=5): 48 [] -ordinal(A)|epsilon_transitive(union(A)). % 2.44/2.64 ** KEPT (pick-wt=5): 49 [] -ordinal(A)|epsilon_connected(union(A)). % 2.44/2.64 ** KEPT (pick-wt=5): 50 [] -ordinal(A)|ordinal(union(A)). % 2.44/2.64 ** KEPT (pick-wt=9): 51 [] -relation(A)| -function(A)| -transfinite_se_quence(A)|epsilon_transitive(relation_dom(A)). % 2.44/2.64 ** KEPT (pick-wt=9): 52 [] -relation(A)| -function(A)| -transfinite_se_quence(A)|epsilon_connected(relation_dom(A)). % 2.44/2.64 Following clause subsumed by 40 during input processing: 0 [] -relation(A)| -function(A)| -transfinite_se_quence(A)|ordinal(relation_dom(A)). % 2.44/2.64 ** KEPT (pick-wt=7): 53 [] empty(A)| -relation(A)| -empty(relation_dom(A)). % 2.44/2.64 ** KEPT (pick-wt=9): 54 [] -relation(A)| -relation_non_empty(A)| -function(A)|with_non_empty_elements(relation_rng(A)). % 2.44/2.64 ** KEPT (pick-wt=7): 55 [] empty(A)| -relation(A)| -empty(relation_rng(A)). % 2.44/2.64 ** KEPT (pick-wt=5): 56 [] -empty(A)|empty(relation_dom(A)). % 2.44/2.64 ** KEPT (pick-wt=5): 57 [] -empty(A)|relation(relation_dom(A)). % 2.44/2.64 ** KEPT (pick-wt=5): 58 [] -empty(A)|empty(relation_rng(A)). % 2.44/2.64 ** KEPT (pick-wt=5): 59 [] -empty(A)|relation(relation_rng(A)). % 2.44/2.64 ** KEPT (pick-wt=2): 60 [] -empty($c7). % 2.44/2.64 ** KEPT (pick-wt=2): 61 [] -empty($c8). % 2.44/2.64 ** KEPT (pick-wt=2): 62 [] -empty($c10). % 2.44/2.64 ** KEPT (pick-wt=10): 63 [] -ordinal(A)| -ordinal(B)| -ordinal_subset(A,B)|subset(A,B). % 2.44/2.64 ** KEPT (pick-wt=10): 64 [] -ordinal(A)| -ordinal(B)|ordinal_subset(A,B)| -subset(A,B). % 2.44/2.64 ** KEPT (pick-wt=5): 66 [copy,65,factor_simp] -ordinal(A)|ordinal_subset(A,A). % 2.44/2.64 ** KEPT (pick-wt=13): 67 [] in($f23(A),A)| -in(ordered_pair(B,C),$f25(A))|in(B,A). % 2.44/2.64 ** KEPT (pick-wt=23): 68 [] in($f23(A),A)| -in(ordered_pair(B,C),$f25(A))| -relation(D)| -function(D)| -transfinite_se_quence(D)|D!=B|relation_dom(D)=C. % 2.44/2.64 ** KEPT (pick-wt=18): 69 [] in($f23(A),A)|in(ordered_pair(B,C),$f25(A))| -in(B,A)|relation($f24(A,B,C)). % 2.44/2.64 ** KEPT (pick-wt=18): 70 [] in($f23(A),A)|in(ordered_pair(B,C),$f25(A))| -in(B,A)|function($f24(A,B,C)). % 2.44/2.64 ** KEPT (pick-wt=18): 71 [] in($f23(A),A)|in(ordered_pair(B,C),$f25(A))| -in(B,A)|transfinite_se_quence($f24(A,B,C)). % 2.44/2.64 ** KEPT (pick-wt=19): 72 [] in($f23(A),A)|in(ordered_pair(B,C),$f25(A))| -in(B,A)|$f24(A,B,C)=B. % 2.44/2.64 ** KEPT (pick-wt=20): 73 [] in($f23(A),A)|in(ordered_pair(B,C),$f25(A))| -in(B,A)|relation_dom($f24(A,B,C))!=C. % 2.44/2.64 ** KEPT (pick-wt=18): 74 [] -relation(A)| -function(A)| -transfinite_se_quence(A)|A!=$f23(B)|relation_dom(A)=$f22(B)|relation($f25(B)). % 2.44/2.64 ** KEPT (pick-wt=18): 75 [] -relation(A)| -function(A)| -transfinite_se_quence(A)|A!=$f23(B)|relation_dom(A)=$f22(B)|function($f25(B)). % 2.44/2.64 ** KEPT (pick-wt=24): 76 [] -relation(A)| -function(A)| -transfinite_se_quence(A)|A!=$f23(B)|relation_dom(A)=$f22(B)| -in(ordered_pair(C,D),$f25(B))|in(C,B). % 2.44/2.64 ** KEPT (pick-wt=34): 77 [] -relation(A)| -function(A)| -transfinite_se_quence(A)|A!=$f23(B)|relation_dom(A)=$f22(B)| -in(ordered_pair(C,D),$f25(B))| -relation(E)| -function(E)| -transfinite_se_quence(E)|E!=C|relation_dom(E)=D. % 2.44/2.64 ** KEPT (pick-wt=29): 78 [] -relation(A)| -function(A)| -transfinite_se_quence(A)|A!=$f23(B)|relation_dom(A)=$f22(B)|in(ordered_pair(C,D),$f25(B))| -in(C,B)|relation($f24(B,C,D)). % 2.44/2.64 ** KEPT (pick-wt=29): 79 [] -relation(A)| -function(A)| -transfinite_se_quence(A)|A!=$f23(B)|relation_dom(A)=$f22(B)|in(ordered_pair(C,D),$f25(B))| -in(C,B)|function($f24(B,C,D)). % 2.44/2.64 ** KEPT (pick-wt=29): 80 [] -relation(A)| -function(A)| -transfinite_se_quence(A)|A!=$f23(B)|relation_dom(A)=$f22(B)|in(ordered_pair(C,D),$f25(B))| -in(C,B)|transfinite_se_quence($f24(B,C,D)). % 2.44/2.64 ** KEPT (pick-wt=30): 81 [] -relation(A)| -function(A)| -transfinite_se_quence(A)|A!=$f23(B)|relation_dom(A)=$f22(B)|in(ordered_pair(C,D),$f25(B))| -in(C,B)|$f24(B,C,D)=C. % 2.44/2.64 ** KEPT (pick-wt=31): 82 [] -relation(A)| -function(A)| -transfinite_se_quence(A)|A!=$f23(B)|relation_dom(A)=$f22(B)|in(ordered_pair(C,D),$f25(B))| -in(C,B)|relation_dom($f24(B,C,D))!=D. % 2.44/2.64 ** KEPT (pick-wt=18): 83 [] -relation(A)| -function(A)| -transfinite_se_quence(A)|A!=$f23(B)|relation_dom(A)=$f21(B)|relation($f25(B)). % 2.44/2.64 ** KEPT (pick-wt=18): 84 [] -relation(A)| -function(A)| -transfinite_se_quence(A)|A!=$f23(B)|relation_dom(A)=$f21(B)|function($f25(B)). % 2.44/2.64 ** KEPT (pick-wt=24): 85 [] -relation(A)| -function(A)| -transfinite_se_quence(A)|A!=$f23(B)|relation_dom(A)=$f21(B)| -in(ordered_pair(C,D),$f25(B))|in(C,B). % 2.44/2.64 ** KEPT (pick-wt=34): 86 [] -relation(A)| -function(A)| -transfinite_se_quence(A)|A!=$f23(B)|relation_dom(A)=$f21(B)| -in(ordered_pair(C,D),$f25(B))| -relation(E)| -function(E)| -transfinite_se_quence(E)|E!=C|relation_dom(E)=D. % 2.44/2.64 ** KEPT (pick-wt=29): 87 [] -relation(A)| -function(A)| -transfinite_se_quence(A)|A!=$f23(B)|relation_dom(A)=$f21(B)|in(ordered_pair(C,D),$f25(B))| -in(C,B)|relation($f24(B,C,D)). % 2.44/2.64 ** KEPT (pick-wt=29): 88 [] -relation(A)| -function(A)| -transfinite_se_quence(A)|A!=$f23(B)|relation_dom(A)=$f21(B)|in(ordered_pair(C,D),$f25(B))| -in(C,B)|function($f24(B,C,D)). % 2.44/2.64 ** KEPT (pick-wt=29): 89 [] -relation(A)| -function(A)| -transfinite_se_quence(A)|A!=$f23(B)|relation_dom(A)=$f21(B)|in(ordered_pair(C,D),$f25(B))| -in(C,B)|transfinite_se_quence($f24(B,C,D)). % 2.44/2.64 ** KEPT (pick-wt=30): 90 [] -relation(A)| -function(A)| -transfinite_se_quence(A)|A!=$f23(B)|relation_dom(A)=$f21(B)|in(ordered_pair(C,D),$f25(B))| -in(C,B)|$f24(B,C,D)=C. % 2.44/2.64 ** KEPT (pick-wt=31): 91 [] -relation(A)| -function(A)| -transfinite_se_quence(A)|A!=$f23(B)|relation_dom(A)=$f21(B)|in(ordered_pair(C,D),$f25(B))| -in(C,B)|relation_dom($f24(B,C,D))!=D. % 2.44/2.64 ** KEPT (pick-wt=8): 92 [] $f22(A)!=$f21(A)|relation($f25(A)). % 2.44/2.64 ** KEPT (pick-wt=8): 93 [] $f22(A)!=$f21(A)|function($f25(A)). % 2.44/2.64 ** KEPT (pick-wt=14): 94 [] $f22(A)!=$f21(A)| -in(ordered_pair(B,C),$f25(A))|in(B,A). % 2.44/2.64 ** KEPT (pick-wt=24): 95 [] $f22(A)!=$f21(A)| -in(ordered_pair(B,C),$f25(A))| -relation(D)| -function(D)| -transfinite_se_quence(D)|D!=B|relation_dom(D)=C. % 2.44/2.64 ** KEPT (pick-wt=19): 96 [] $f22(A)!=$f21(A)|in(ordered_pair(B,C),$f25(A))| -in(B,A)|relation($f24(A,B,C)). % 2.44/2.64 ** KEPT (pick-wt=19): 97 [] $f22(A)!=$f21(A)|in(ordered_pair(B,C),$f25(A))| -in(B,A)|function($f24(A,B,C)). % 2.44/2.64 ** KEPT (pick-wt=19): 98 [] $f22(A)!=$f21(A)|in(ordered_pair(B,C),$f25(A))| -in(B,A)|transfinite_se_quence($f24(A,B,C)). % 2.44/2.65 ** KEPT (pick-wt=20): 99 [] $f22(A)!=$f21(A)|in(ordered_pair(B,C),$f25(A))| -in(B,A)|$f24(A,B,C)=B. % 2.44/2.65 ** KEPT (pick-wt=21): 100 [] $f22(A)!=$f21(A)|in(ordered_pair(B,C),$f25(A))| -in(B,A)|relation_dom($f24(A,B,C))!=C. % 2.44/2.65 ** KEPT (pick-wt=13): 101 [] -relation(A)| -function(A)| -ordinal(B)|ordinal($f26(A,B))|ordinal($f28(A)). % 2.44/2.65 ** KEPT (pick-wt=20): 102 [] -relation(A)| -function(A)| -ordinal(B)|ordinal($f26(A,B))| -ordinal(C)| -in(C,relation_rng(A))|ordinal_subset(C,$f28(A)). % 2.44/2.65 ** KEPT (pick-wt=20): 103 [] -relation(A)| -function(A)| -ordinal(B)|ordinal($f26(A,B))| -ordinal(C)|ordinal($f27(A,C))|ordinal_subset($f28(A),C). % 2.44/2.65 ** KEPT (pick-wt=22): 104 [] -relation(A)| -function(A)| -ordinal(B)|ordinal($f26(A,B))| -ordinal(C)|in($f27(A,C),relation_rng(A))|ordinal_subset($f28(A),C). % 2.44/2.65 ** KEPT (pick-wt=21): 105 [] -relation(A)| -function(A)| -ordinal(B)|ordinal($f26(A,B))| -ordinal(C)| -ordinal_subset($f27(A,C),C)|ordinal_subset($f28(A),C). % 2.44/2.65 ** KEPT (pick-wt=15): 106 [] -relation(A)| -function(A)| -ordinal(B)|in($f26(A,B),relation_rng(A))|ordinal($f28(A)). % 2.44/2.65 ** KEPT (pick-wt=22): 107 [] -relation(A)| -function(A)| -ordinal(B)|in($f26(A,B),relation_rng(A))| -ordinal(C)| -in(C,relation_rng(A))|ordinal_subset(C,$f28(A)). % 2.44/2.65 ** KEPT (pick-wt=22): 108 [] -relation(A)| -function(A)| -ordinal(B)|in($f26(A,B),relation_rng(A))| -ordinal(C)|ordinal($f27(A,C))|ordinal_subset($f28(A),C). % 2.44/2.65 ** KEPT (pick-wt=24): 109 [] -relation(A)| -function(A)| -ordinal(B)|in($f26(A,B),relation_rng(A))| -ordinal(C)|in($f27(A,C),relation_rng(A))|ordinal_subset($f28(A),C). % 2.44/2.65 ** KEPT (pick-wt=23): 110 [] -relation(A)| -function(A)| -ordinal(B)|in($f26(A,B),relation_rng(A))| -ordinal(C)| -ordinal_subset($f27(A,C),C)|ordinal_subset($f28(A),C). % 2.44/2.65 ** KEPT (pick-wt=14): 111 [] -relation(A)| -function(A)| -ordinal(B)| -ordinal_subset($f26(A,B),B)|ordinal($f28(A)). % 2.44/2.65 ** KEPT (pick-wt=21): 112 [] -relation(A)| -function(A)| -ordinal(B)| -ordinal_subset($f26(A,B),B)| -ordinal(C)| -in(C,relation_rng(A))|ordinal_subset(C,$f28(A)). % 2.44/2.65 ** KEPT (pick-wt=21): 113 [] -relation(A)| -function(A)| -ordinal(B)| -ordinal_subset($f26(A,B),B)| -ordinal(C)|ordinal($f27(A,C))|ordinal_subset($f28(A),C). % 2.44/2.65 ** KEPT (pick-wt=23): 114 [] -relation(A)| -function(A)| -ordinal(B)| -ordinal_subset($f26(A,B),B)| -ordinal(C)|in($f27(A,C),relation_rng(A))|ordinal_subset($f28(A),C). % 2.44/2.65 ** KEPT (pick-wt=22): 115 [] -relation(A)| -function(A)| -ordinal(B)| -ordinal_subset($f26(A,B),B)| -ordinal(C)| -ordinal_subset($f27(A,C),C)|ordinal_subset($f28(A),C). % 2.44/2.65 ** KEPT (pick-wt=6): 116 [] -inclusion_comparable(A,B)|inclusion_comparable(B,A). % 2.44/2.65 ** KEPT (pick-wt=6): 117 [] -in(A,B)|element(A,B). % 2.44/2.65 ** KEPT (pick-wt=7): 118 [] -ordinal(A)| -in(B,A)|ordinal(B). % 2.44/2.65 ** KEPT (pick-wt=10): 119 [] -ordinal(A)| -ordinal(B)|ordinal_subset(A,B)|in(B,A). % 2.44/2.65 ** KEPT (pick-wt=8): 120 [] -element(A,B)|empty(B)|in(A,B). % 2.44/2.65 ** KEPT (pick-wt=6): 121 [] -ordinal($f29(A))|ordinal($f30(A)). % 2.44/2.65 ** KEPT (pick-wt=7): 122 [] -ordinal($f29(A))|subset(A,$f30(A)). % 2.44/2.65 ** KEPT (pick-wt=7): 123 [] -element(A,powerset(B))|subset(A,B). % 2.44/2.65 ** KEPT (pick-wt=7): 124 [] element(A,powerset(B))| -subset(A,B). % 2.44/2.65 ** KEPT (pick-wt=5): 125 [] -in(A,$c15)|relation(A). % 2.44/2.65 ** KEPT (pick-wt=5): 126 [] -in(A,$c15)|function(A). % 2.44/2.65 ** KEPT (pick-wt=5): 127 [] -in(A,$c15)|transfinite_se_quence(A). % 2.44/2.65 ** KEPT (pick-wt=9): 128 [] -relation(union($c15))| -function(union($c15))| -transfinite_se_quence(union($c15)). % 2.44/2.65 ** KEPT (pick-wt=10): 129 [] -in(A,B)| -element(B,powerset(C))|element(A,C). % 2.44/2.65 ** KEPT (pick-wt=9): 130 [] -in(A,B)| -element(B,powerset(C))| -empty(C). % 2.44/2.65 ** KEPT (pick-wt=5): 131 [] -empty(A)|A=empty_set. % 2.44/2.65 ** KEPT (pick-wt=5): 132 [] -in(A,B)| -empty(B). % 2.44/2.65 ** KEPT (pick-wt=7): 133 [] -empty(A)|A=B| -empty(B). % 2.44/2.65 ** KEPT (pick-wt=13): 134 [] -relation(A)| -function(A)| -in(ordered_pair(B,C),A)|in(B,relation_dom(A)). % 2.44/2.65 ** KEPT (pick-wt=14): 135 [] -relation(A)| -function(A)| -in(ordered_pair(B,C),A)|C=apply(A,B). % 2.44/2.65 ** KEPT (pick-wt=18): 136 [] -relation(A)| -function(A)|in(ordered_pair(B,C),A)| -in(B,relation_dom(A))|C!=apply(A,B). % 2.44/2.65 ** KEPT (pick-wt=7): 137 [] -in(A,B)|subset(A,union(B)). % 2.44/2.65 % 2.44/2.65 ------------> process sos: % 2.44/2.65 ** KEPT (pick-wt=3): 171 [] A=A. % 2.44/2.65 ** KEPT (pick-wt=7): 172 [] unordered_pair(A,B)=unordered_pair(B,A). % 2.44/2.65 ** KEPT (pick-wt=9): 173 [] function(A)|in(ordered_pair($f3(A),$f2(A)),A). % 2.44/2.65 ** KEPT (pick-wt=9): 174 [] function(A)|in(ordered_pair($f3(A),$f1(A)),A). % 2.44/2.65 ** KEPT (pick-wt=6): 175 [] relation(A)|in($f6(A),A). % 2.44/2.65 ** KEPT (pick-wt=6): 176 [] epsilon_transitive(A)|in($f7(A),A). % 2.44/2.65 ** KEPT (pick-wt=8): 177 [] subset(A,B)|in($f8(A,B),A). % 2.44/2.65 ** KEPT (pick-wt=16): 178 [] A=union(B)|in($f14(B,A),A)|in($f14(B,A),$f13(B,A)). % 2.44/2.65 ** KEPT (pick-wt=14): 179 [] A=union(B)|in($f14(B,A),A)|in($f13(B,A),B). % 2.44/2.65 ** KEPT (pick-wt=10): 181 [copy,180,flip.1] unordered_pair(unordered_pair(A,B),singleton(A))=ordered_pair(A,B). % 2.44/2.65 ---> New Demodulator: 182 [new_demod,181] unordered_pair(unordered_pair(A,B),singleton(A))=ordered_pair(A,B). % 2.44/2.65 ** KEPT (pick-wt=6): 183 [] inclusion_linear(A)|in($f19(A),A). % 2.44/2.65 ** KEPT (pick-wt=6): 184 [] inclusion_linear(A)|in($f18(A),A). % 2.44/2.65 ** KEPT (pick-wt=4): 185 [] element($f20(A),A). % 2.44/2.65 ** KEPT (pick-wt=2): 186 [] empty(empty_set). % 2.44/2.65 ** KEPT (pick-wt=2): 187 [] relation(empty_set). % 2.44/2.65 ** KEPT (pick-wt=2): 188 [] relation_empty_yielding(empty_set). % 2.44/2.65 Following clause subsumed by 186 during input processing: 0 [] empty(empty_set). % 2.44/2.65 Following clause subsumed by 187 during input processing: 0 [] relation(empty_set). % 2.44/2.65 Following clause subsumed by 188 during input processing: 0 [] relation_empty_yielding(empty_set). % 2.44/2.65 ** KEPT (pick-wt=2): 189 [] function(empty_set). % 2.44/2.65 ** KEPT (pick-wt=2): 190 [] one_to_one(empty_set). % 2.44/2.65 Following clause subsumed by 186 during input processing: 0 [] empty(empty_set). % 2.44/2.65 ** KEPT (pick-wt=2): 191 [] epsilon_transitive(empty_set). % 2.44/2.65 ** KEPT (pick-wt=2): 192 [] epsilon_connected(empty_set). % 2.44/2.65 ** KEPT (pick-wt=2): 193 [] ordinal(empty_set). % 2.44/2.65 Following clause subsumed by 186 during input processing: 0 [] empty(empty_set). % 2.44/2.65 Following clause subsumed by 187 during input processing: 0 [] relation(empty_set). % 2.44/2.65 ** KEPT (pick-wt=2): 194 [] relation($c1). % 2.44/2.65 ** KEPT (pick-wt=2): 195 [] function($c1). % 2.44/2.65 ** KEPT (pick-wt=2): 196 [] epsilon_transitive($c2). % 2.44/2.65 ** KEPT (pick-wt=2): 197 [] epsilon_connected($c2). % 2.44/2.65 ** KEPT (pick-wt=2): 198 [] ordinal($c2). % 2.44/2.65 ** KEPT (pick-wt=2): 199 [] empty($c3). % 2.44/2.65 ** KEPT (pick-wt=2): 200 [] relation($c3). % 2.44/2.65 ** KEPT (pick-wt=2): 201 [] empty($c4). % 2.44/2.65 ** KEPT (pick-wt=2): 202 [] relation($c5). % 2.44/2.65 ** KEPT (pick-wt=2): 203 [] empty($c5). % 2.44/2.65 ** KEPT (pick-wt=2): 204 [] function($c5). % 2.44/2.65 ** KEPT (pick-wt=2): 205 [] relation($c6). % 2.44/2.65 ** KEPT (pick-wt=2): 206 [] function($c6). % 2.44/2.65 ** KEPT (pick-wt=2): 207 [] one_to_one($c6). % 2.44/2.65 ** KEPT (pick-wt=2): 208 [] empty($c6). % 2.44/2.65 ** KEPT (pick-wt=2): 209 [] epsilon_transitive($c6). % 2.44/2.65 ** KEPT (pick-wt=2): 210 [] epsilon_connected($c6). % 2.44/2.65 ** KEPT (pick-wt=2): 211 [] ordinal($c6). % 2.44/2.65 ** KEPT (pick-wt=2): 212 [] relation($c7). % 2.44/2.65 ** KEPT (pick-wt=2): 213 [] relation($c9). % 2.44/2.65 ** KEPT (pick-wt=2): 214 [] function($c9). % 2.44/2.65 ** KEPT (pick-wt=2): 215 [] one_to_one($c9). % 2.44/2.65 ** KEPT (pick-wt=2): 216 [] epsilon_transitive($c10). % 2.44/2.65 ** KEPT (pick-wt=2): 217 [] epsilon_connected($c10). % 2.44/2.65 ** KEPT (pick-wt=2): 218 [] ordinal($c10). % 2.44/2.65 ** KEPT (pick-wt=2): 219 [] relation($c11). % 2.44/2.65 ** KEPT (pick-wt=2): 220 [] relation_empty_yielding($c11). % 2.44/2.65 ** KEPT (pick-wt=2): 221 [] relation($c12). % 2.44/2.65 ** KEPT (pick-wt=2): 222 [] relation_empty_yielding($c12). % 2.44/2.65 ** KEPT (pick-wt=2): 223 [] function($c12). % 2.44/2.65 ** KEPT (pick-wt=2): 224 [] relation($c13). % 2.44/2.65 ** KEPT (pick-wt=2): 225 [] function($c13). % 2.44/2.65 ** KEPT (pick-wt=2): 226 [] transfinite_se_quence($c13). % 2.44/2.65 ** KEPT (pick-wt=2): 227 [] relation($c14). % 2.44/2.65 ** KEPT (pick-wt=2): 228 [] relation_non_empty($c14). % 2.44/2.65 ** KEPT (pick-wt=2): 229 [] function($c14). % 2.44/2.65 ** KEPT (pick-wt=3): 230 [] subset(A,A). % 2.44/2.65 ** KEPT (pick-wt=3): 231 [] inclusion_comparable(A,A). % 2.44/2.65 ** KEPT (pick-wt=7): 232 [] in($f23(A),A)|relation($f25(A)). % 2.44/2.65 ** KEPT (pick-wt=7): 233 [] in($f23(A),A)|function($f25(A)). % 2.44/2.65 ** KEPT (pick-wt=7): 234 [] in($f29(A),A)|ordinal($f30(A)). % 2.44/2.65 ** KEPT (pick-wt=8): 235 [] in($f29(A),A)|subset(A,$f30(A)). % 2.44/2.65 ** KEPT (pick-wt=2): 236 [] inclusion_linear($c15). % 2.44/2.65 Following clause subsumed by 171 during input processing: 0 [copy,171,flip.1] A=A. % 36.46/36.62 171 back subsumes 168. % 36.46/36.62 171 back subsumes 140. % 36.46/36.62 171 back subsumes 139. % 36.46/36.62 Following clause subsumed by 172 during input processing: 0 [copy,172,flip.1] unordered_pair(A,B)=unordered_pair(B,A). % 36.46/36.62 >>>> Starting back demodulation with 182. % 36.46/36.62 230 back subsumes 145. % 36.46/36.62 230 back subsumes 144. % 36.46/36.62 231 back subsumes 143. % 36.46/36.62 % 36.46/36.62 ======= end of input processing ======= % 36.46/36.62 % 36.46/36.62 =========== start of search =========== % 36.46/36.62 % 36.46/36.62 % 36.46/36.62 Resetting weight limit to 2. % 36.46/36.62 % 36.46/36.62 % 36.46/36.62 Resetting weight limit to 2. % 36.46/36.62 % 36.46/36.62 sos_size=379 % 36.46/36.62 % 36.46/36.62 Search stopped because sos empty. % 36.46/36.62 % 36.46/36.62 % 36.46/36.62 Search stopped because sos empty. % 36.46/36.62 % 36.46/36.62 ============ end of search ============ % 36.46/36.62 % 36.46/36.62 -------------- statistics ------------- % 36.46/36.62 clauses given 408 % 36.46/36.62 clauses generated 1358111 % 36.46/36.62 clauses kept 715 % 36.46/36.62 clauses forward subsumed 535 % 36.46/36.62 clauses back subsumed 15 % 36.46/36.62 Kbytes malloced 5859 % 36.46/36.62 % 36.46/36.62 ----------- times (seconds) ----------- % 36.46/36.62 user CPU time 33.99 (0 hr, 0 min, 33 sec) % 36.46/36.62 system CPU time 0.01 (0 hr, 0 min, 0 sec) % 36.46/36.62 wall-clock time 36 (0 hr, 0 min, 36 sec) % 36.46/36.62 % 36.46/36.62 Process 20265 finished Wed Jul 27 09:44:23 2022 % 36.46/36.62 Otter interrupted % 36.46/36.62 PROOF NOT FOUND %------------------------------------------------------------------------------