Input TRS: 1: intersect'ii'in(cons(X,X0),cons(X,X1)) -> intersect'ii'out() 2: intersect'ii'in(Xs,cons(X0,Ys)) -> u'1'1(intersect'ii'in(Xs,Ys)) 3: u'1'1(intersect'ii'out()) -> intersect'ii'out() 4: intersect'ii'in(cons(X0,Xs),Ys) -> u'2'1(intersect'ii'in(Xs,Ys)) 5: u'2'1(intersect'ii'out()) -> intersect'ii'out() 6: reduce'ii'in(sequent(cons(if(A,B),Fs),Gs),NF) -> u'3'1(reduce'ii'in(sequent(cons(x'2b(x'2d(B),A),Fs),Gs),NF)) 7: u'3'1(reduce'ii'out()) -> reduce'ii'out() 8: reduce'ii'in(sequent(cons(iff(A,B),Fs),Gs),NF) -> u'4'1(reduce'ii'in(sequent(cons(x'2a(if(A,B),if(B,A)),Fs),Gs),NF)) 9: u'4'1(reduce'ii'out()) -> reduce'ii'out() 10: reduce'ii'in(sequent(cons(x'2a(F1,F2),Fs),Gs),NF) -> u'5'1(reduce'ii'in(sequent(cons(F1,cons(F2,Fs)),Gs),NF)) 11: u'5'1(reduce'ii'out()) -> reduce'ii'out() 12: reduce'ii'in(sequent(cons(x'2b(F1,F2),Fs),Gs),NF) -> u'6'1(reduce'ii'in(sequent(cons(F1,Fs),Gs),NF),F2,Fs,Gs,NF) 13: u'6'1(reduce'ii'out(),F2,Fs,Gs,NF) -> u'6'2(reduce'ii'in(sequent(cons(F2,Fs),Gs),NF)) 14: u'6'2(reduce'ii'out()) -> reduce'ii'out() 15: reduce'ii'in(sequent(cons(x'2d(F1),Fs),Gs),NF) -> u'7'1(reduce'ii'in(sequent(Fs,cons(F1,Gs)),NF)) 16: u'7'1(reduce'ii'out()) -> reduce'ii'out() 17: reduce'ii'in(sequent(Fs,cons(if(A,B),Gs)),NF) -> u'8'1(reduce'ii'in(sequent(Fs,cons(x'2b(x'2d(B),A),Gs)),NF)) 18: u'8'1(reduce'ii'out()) -> reduce'ii'out() 19: reduce'ii'in(sequent(Fs,cons(iff(A,B),Gs)),NF) -> u'9'1(reduce'ii'in(sequent(Fs,cons(x'2a(if(A,B),if(B,A)),Gs)),NF)) 20: u'9'1(reduce'ii'out()) -> reduce'ii'out() 21: reduce'ii'in(sequent(cons(p(V),Fs),Gs),sequent(Left,Right)) -> u'10'1(reduce'ii'in(sequent(Fs,Gs),sequent(cons(p(V),Left),Right))) 22: u'10'1(reduce'ii'out()) -> reduce'ii'out() 23: reduce'ii'in(sequent(Fs,cons(x'2b(G1,G2),Gs)),NF) -> u'11'1(reduce'ii'in(sequent(Fs,cons(G1,cons(G2,Gs))),NF)) 24: u'11'1(reduce'ii'out()) -> reduce'ii'out() 25: reduce'ii'in(sequent(Fs,cons(x'2a(G1,G2),Gs)),NF) -> u'12'1(reduce'ii'in(sequent(Fs,cons(G1,Gs)),NF),Fs,G2,Gs,NF) 26: u'12'1(reduce'ii'out(),Fs,G2,Gs,NF) -> u'12'2(reduce'ii'in(sequent(Fs,cons(G2,Gs)),NF)) 27: u'12'2(reduce'ii'out()) -> reduce'ii'out() 28: reduce'ii'in(sequent(Fs,cons(x'2d(G1),Gs)),NF) -> u'13'1(reduce'ii'in(sequent(cons(G1,Fs),Gs),NF)) 29: u'13'1(reduce'ii'out()) -> reduce'ii'out() 30: reduce'ii'in(sequent(nil(),cons(p(V),Gs)),sequent(Left,Right)) -> u'14'1(reduce'ii'in(sequent(nil(),Gs),sequent(Left,cons(p(V),Right)))) 31: u'14'1(reduce'ii'out()) -> reduce'ii'out() 32: reduce'ii'in(sequent(nil(),nil()),sequent(F1,F2)) -> u'15'1(intersect'ii'in(F1,F2)) 33: u'15'1(intersect'ii'out()) -> reduce'ii'out() 34: tautology'i'in(F) -> u'16'1(reduce'ii'in(sequent(nil(),cons(F,nil())),sequent(nil(),nil()))) 35: u'16'1(reduce'ii'out()) -> tautology'i'out() Number of strict rules: 35 Direct Order(PosReal,>,Poly) ... failed. Freezing reduce'ii'in 1: intersect'ii'in(cons(X,X0),cons(X,X1)) -> intersect'ii'out() 2: intersect'ii'in(Xs,cons(X0,Ys)) -> u'1'1(intersect'ii'in(Xs,Ys)) 3: u'1'1(intersect'ii'out()) -> intersect'ii'out() 4: intersect'ii'in(cons(X0,Xs),Ys) -> u'2'1(intersect'ii'in(Xs,Ys)) 5: u'2'1(intersect'ii'out()) -> intersect'ii'out() 6: reduce'ii'in❆1_sequent(cons(if(A,B),Fs),Gs,NF) -> u'3'1(reduce'ii'in❆1_sequent(cons(x'2b(x'2d(B),A),Fs),Gs,NF)) 7: u'3'1(reduce'ii'out()) -> reduce'ii'out() 8: reduce'ii'in❆1_sequent(cons(iff(A,B),Fs),Gs,NF) -> u'4'1(reduce'ii'in❆1_sequent(cons(x'2a(if(A,B),if(B,A)),Fs),Gs,NF)) 9: u'4'1(reduce'ii'out()) -> reduce'ii'out() 10: reduce'ii'in❆1_sequent(cons(x'2a(F1,F2),Fs),Gs,NF) -> u'5'1(reduce'ii'in❆1_sequent(cons(F1,cons(F2,Fs)),Gs,NF)) 11: u'5'1(reduce'ii'out()) -> reduce'ii'out() 12: reduce'ii'in❆1_sequent(cons(x'2b(F1,F2),Fs),Gs,NF) -> u'6'1(reduce'ii'in❆1_sequent(cons(F1,Fs),Gs,NF),F2,Fs,Gs,NF) 13: u'6'1(reduce'ii'out(),F2,Fs,Gs,NF) -> u'6'2(reduce'ii'in❆1_sequent(cons(F2,Fs),Gs,NF)) 14: u'6'2(reduce'ii'out()) -> reduce'ii'out() 15: reduce'ii'in❆1_sequent(cons(x'2d(F1),Fs),Gs,NF) -> u'7'1(reduce'ii'in❆1_sequent(Fs,cons(F1,Gs),NF)) 16: u'7'1(reduce'ii'out()) -> reduce'ii'out() 17: reduce'ii'in❆1_sequent(Fs,cons(if(A,B),Gs),NF) -> u'8'1(reduce'ii'in❆1_sequent(Fs,cons(x'2b(x'2d(B),A),Gs),NF)) 18: u'8'1(reduce'ii'out()) -> reduce'ii'out() 19: reduce'ii'in❆1_sequent(Fs,cons(iff(A,B),Gs),NF) -> u'9'1(reduce'ii'in❆1_sequent(Fs,cons(x'2a(if(A,B),if(B,A)),Gs),NF)) 20: u'9'1(reduce'ii'out()) -> reduce'ii'out() 21: reduce'ii'in❆1_sequent(cons(p(V),Fs),Gs,sequent(Left,Right)) -> u'10'1(reduce'ii'in❆1_sequent(Fs,Gs,sequent(cons(p(V),Left),Right))) 22: u'10'1(reduce'ii'out()) -> reduce'ii'out() 23: reduce'ii'in❆1_sequent(Fs,cons(x'2b(G1,G2),Gs),NF) -> u'11'1(reduce'ii'in❆1_sequent(Fs,cons(G1,cons(G2,Gs)),NF)) 24: u'11'1(reduce'ii'out()) -> reduce'ii'out() 25: reduce'ii'in❆1_sequent(Fs,cons(x'2a(G1,G2),Gs),NF) -> u'12'1(reduce'ii'in❆1_sequent(Fs,cons(G1,Gs),NF),Fs,G2,Gs,NF) 26: u'12'1(reduce'ii'out(),Fs,G2,Gs,NF) -> u'12'2(reduce'ii'in❆1_sequent(Fs,cons(G2,Gs),NF)) 27: u'12'2(reduce'ii'out()) -> reduce'ii'out() 28: reduce'ii'in❆1_sequent(Fs,cons(x'2d(G1),Gs),NF) -> u'13'1(reduce'ii'in❆1_sequent(cons(G1,Fs),Gs,NF)) 29: u'13'1(reduce'ii'out()) -> reduce'ii'out() 30: reduce'ii'in❆1_sequent(nil(),cons(p(V),Gs),sequent(Left,Right)) -> u'14'1(reduce'ii'in❆1_sequent(nil(),Gs,sequent(Left,cons(p(V),Right)))) 31: u'14'1(reduce'ii'out()) -> reduce'ii'out() 32: reduce'ii'in❆1_sequent(nil(),nil(),sequent(F1,F2)) -> u'15'1(intersect'ii'in(F1,F2)) 33: u'15'1(intersect'ii'out()) -> reduce'ii'out() 34: tautology'i'in(F) -> u'16'1(reduce'ii'in❆1_sequent(nil(),cons(F,nil()),sequent(nil(),nil()))) 35: u'16'1(reduce'ii'out()) -> tautology'i'out() 36: reduce'ii'in(sequent(_1,_2),_3) ->= reduce'ii'in❆1_sequent(_1,_2,_3) Number of strict rules: 35 Direct Order(PosReal,>,Poly) ... failed. Dependency Pairs: #1: #intersect'ii'in(Xs,cons(X0,Ys)) -> #u'1'1(intersect'ii'in(Xs,Ys)) #2: #intersect'ii'in(Xs,cons(X0,Ys)) -> #intersect'ii'in(Xs,Ys) #3: #reduce'ii'in❆1_sequent(cons(if(A,B),Fs),Gs,NF) -> #u'3'1(reduce'ii'in❆1_sequent(cons(x'2b(x'2d(B),A),Fs),Gs,NF)) #4: #reduce'ii'in❆1_sequent(cons(if(A,B),Fs),Gs,NF) -> #reduce'ii'in❆1_sequent(cons(x'2b(x'2d(B),A),Fs),Gs,NF) #5: #u'6'1(reduce'ii'out(),F2,Fs,Gs,NF) -> #u'6'2(reduce'ii'in❆1_sequent(cons(F2,Fs),Gs,NF)) #6: #u'6'1(reduce'ii'out(),F2,Fs,Gs,NF) -> #reduce'ii'in❆1_sequent(cons(F2,Fs),Gs,NF) #7: #reduce'ii'in❆1_sequent(Fs,cons(x'2b(G1,G2),Gs),NF) -> #u'11'1(reduce'ii'in❆1_sequent(Fs,cons(G1,cons(G2,Gs)),NF)) #8: #reduce'ii'in❆1_sequent(Fs,cons(x'2b(G1,G2),Gs),NF) -> #reduce'ii'in❆1_sequent(Fs,cons(G1,cons(G2,Gs)),NF) #9: #reduce'ii'in❆1_sequent(cons(x'2b(F1,F2),Fs),Gs,NF) -> #u'6'1(reduce'ii'in❆1_sequent(cons(F1,Fs),Gs,NF),F2,Fs,Gs,NF) #10: #reduce'ii'in❆1_sequent(cons(x'2b(F1,F2),Fs),Gs,NF) -> #reduce'ii'in❆1_sequent(cons(F1,Fs),Gs,NF) #11: #reduce'ii'in❆1_sequent(nil(),cons(p(V),Gs),sequent(Left,Right)) -> #u'14'1(reduce'ii'in❆1_sequent(nil(),Gs,sequent(Left,cons(p(V),Right)))) #12: #reduce'ii'in❆1_sequent(nil(),cons(p(V),Gs),sequent(Left,Right)) -> #reduce'ii'in❆1_sequent(nil(),Gs,sequent(Left,cons(p(V),Right))) #13: #reduce'ii'in❆1_sequent(Fs,cons(x'2a(G1,G2),Gs),NF) -> #u'12'1(reduce'ii'in❆1_sequent(Fs,cons(G1,Gs),NF),Fs,G2,Gs,NF) #14: #reduce'ii'in❆1_sequent(Fs,cons(x'2a(G1,G2),Gs),NF) -> #reduce'ii'in❆1_sequent(Fs,cons(G1,Gs),NF) #15: #reduce'ii'in❆1_sequent(cons(x'2a(F1,F2),Fs),Gs,NF) -> #u'5'1(reduce'ii'in❆1_sequent(cons(F1,cons(F2,Fs)),Gs,NF)) #16: #reduce'ii'in❆1_sequent(cons(x'2a(F1,F2),Fs),Gs,NF) -> #reduce'ii'in❆1_sequent(cons(F1,cons(F2,Fs)),Gs,NF) #17: #reduce'ii'in❆1_sequent(Fs,cons(x'2d(G1),Gs),NF) -> #u'13'1(reduce'ii'in❆1_sequent(cons(G1,Fs),Gs,NF)) #18: #reduce'ii'in❆1_sequent(Fs,cons(x'2d(G1),Gs),NF) -> #reduce'ii'in❆1_sequent(cons(G1,Fs),Gs,NF) #19: #tautology'i'in(F) -> #u'16'1(reduce'ii'in❆1_sequent(nil(),cons(F,nil()),sequent(nil(),nil()))) #20: #tautology'i'in(F) -> #reduce'ii'in❆1_sequent(nil(),cons(F,nil()),sequent(nil(),nil())) #21: #reduce'ii'in❆1_sequent(Fs,cons(if(A,B),Gs),NF) -> #u'8'1(reduce'ii'in❆1_sequent(Fs,cons(x'2b(x'2d(B),A),Gs),NF)) #22: #reduce'ii'in❆1_sequent(Fs,cons(if(A,B),Gs),NF) -> #reduce'ii'in❆1_sequent(Fs,cons(x'2b(x'2d(B),A),Gs),NF) #23: #reduce'ii'in❆1_sequent(Fs,cons(iff(A,B),Gs),NF) -> #u'9'1(reduce'ii'in❆1_sequent(Fs,cons(x'2a(if(A,B),if(B,A)),Gs),NF)) #24: #reduce'ii'in❆1_sequent(Fs,cons(iff(A,B),Gs),NF) -> #reduce'ii'in❆1_sequent(Fs,cons(x'2a(if(A,B),if(B,A)),Gs),NF) #25: #reduce'ii'in❆1_sequent(nil(),nil(),sequent(F1,F2)) -> #u'15'1(intersect'ii'in(F1,F2)) #26: #reduce'ii'in❆1_sequent(nil(),nil(),sequent(F1,F2)) -> #intersect'ii'in(F1,F2) #27: #u'12'1(reduce'ii'out(),Fs,G2,Gs,NF) -> #u'12'2(reduce'ii'in❆1_sequent(Fs,cons(G2,Gs),NF)) #28: #u'12'1(reduce'ii'out(),Fs,G2,Gs,NF) -> #reduce'ii'in❆1_sequent(Fs,cons(G2,Gs),NF) #29: #reduce'ii'in(sequent(_1,_2),_3) ->? #reduce'ii'in❆1_sequent(_1,_2,_3) #30: #reduce'ii'in❆1_sequent(cons(p(V),Fs),Gs,sequent(Left,Right)) -> #u'10'1(reduce'ii'in❆1_sequent(Fs,Gs,sequent(cons(p(V),Left),Right))) #31: #reduce'ii'in❆1_sequent(cons(p(V),Fs),Gs,sequent(Left,Right)) -> #reduce'ii'in❆1_sequent(Fs,Gs,sequent(cons(p(V),Left),Right)) #32: #reduce'ii'in❆1_sequent(cons(iff(A,B),Fs),Gs,NF) -> #u'4'1(reduce'ii'in❆1_sequent(cons(x'2a(if(A,B),if(B,A)),Fs),Gs,NF)) #33: #reduce'ii'in❆1_sequent(cons(iff(A,B),Fs),Gs,NF) -> #reduce'ii'in❆1_sequent(cons(x'2a(if(A,B),if(B,A)),Fs),Gs,NF) #34: #reduce'ii'in❆1_sequent(cons(x'2d(F1),Fs),Gs,NF) -> #u'7'1(reduce'ii'in❆1_sequent(Fs,cons(F1,Gs),NF)) #35: #reduce'ii'in❆1_sequent(cons(x'2d(F1),Fs),Gs,NF) -> #reduce'ii'in❆1_sequent(Fs,cons(F1,Gs),NF) #36: #intersect'ii'in(cons(X0,Xs),Ys) -> #u'2'1(intersect'ii'in(Xs,Ys)) #37: #intersect'ii'in(cons(X0,Xs),Ys) -> #intersect'ii'in(Xs,Ys) Number of SCCs: 2, DPs: 18, edges: 167 SCC { #2 #37 } Removing DPs: Order(PosReal,>,Sum)... succeeded. iff(x1,x2) weight: 0 tautology'i'in(x1) weight: 0 #u'7'1(x1) weight: 0 u'12'1(x1,x2,x3,x4,x5) weight: 0 x'2d(x1) weight: 0 reduce'ii'in❆1_sequent(x1,x2,x3) weight: 0 #u'12'1(x1,x2,x3,x4,x5) weight: 0 #reduce'ii'in(x1,x2) weight: 0 #u'5'1(x1) weight: 0 #u'1'1(x1) weight: 0 reduce'ii'in(x1,x2) weight: 0 u'7'1(x1) weight: 0 x'2b(x1,x2) weight: 0 u'5'1(x1) weight: 0 u'6'2(x1) weight: 0 u'8'1(x1) weight: 0 u'12'2(x1) weight: 0 #u'13'1(x1) weight: 0 #u'16'1(x1) weight: 0 intersect'ii'out() weight: 0 intersect'ii'in(x1,x2) weight: 0 #u'9'1(x1) weight: 0 u'6'1(x1,x2,x3,x4,x5) weight: 0 #u'14'1(x1) weight: 0 p(x1) weight: 0 u'10'1(x1) weight: 0 if(x1,x2) weight: 0 #u'2'1(x1) weight: 0 nil() weight: 0 #intersect'ii'in(x1,x2) weight: x2 u'4'1(x1) weight: 0 #u'6'1(x1,x2,x3,x4,x5) weight: 0 u'2'1(x1) weight: 0 u'9'1(x1) weight: 0 #u'11'1(x1) weight: 0 tautology'i'out() weight: 0 #u'15'1(x1) weight: 0 u'15'1(x1) weight: 0 cons(x1,x2) weight: (/ 1 2) + x2 u'13'1(x1) weight: 0 reduce'ii'out() weight: 0 #u'12'2(x1) weight: 0 x'2a(x1,x2) weight: 0 u'14'1(x1) weight: 0 #tautology'i'in(x1) weight: 0 #u'4'1(x1) weight: 0 u'3'1(x1) weight: 0 #u'8'1(x1) weight: 0 #reduce'ii'in❆1_sequent(x1,x2,x3) weight: 0 sequent(x1,x2) weight: 0 #u'6'2(x1) weight: 0 u'11'1(x1) weight: 0 #u'3'1(x1) weight: 0 u'1'1(x1) weight: 0 #u'10'1(x1) weight: 0 u'16'1(x1) weight: 0 Usable rules: { } Removed DPs: #2 Number of SCCs: 2, DPs: 17, edges: 164 SCC { #37 } Removing DPs: Order(PosReal,>,Sum)... succeeded. iff(x1,x2) weight: 0 tautology'i'in(x1) weight: 0 #u'7'1(x1) weight: 0 u'12'1(x1,x2,x3,x4,x5) weight: 0 x'2d(x1) weight: 0 reduce'ii'in❆1_sequent(x1,x2,x3) weight: 0 #u'12'1(x1,x2,x3,x4,x5) weight: 0 #reduce'ii'in(x1,x2) weight: 0 #u'5'1(x1) weight: 0 #u'1'1(x1) weight: 0 reduce'ii'in(x1,x2) weight: 0 u'7'1(x1) weight: 0 x'2b(x1,x2) weight: 0 u'5'1(x1) weight: 0 u'6'2(x1) weight: 0 u'8'1(x1) weight: 0 u'12'2(x1) weight: 0 #u'13'1(x1) weight: 0 #u'16'1(x1) weight: 0 intersect'ii'out() weight: 0 intersect'ii'in(x1,x2) weight: 0 #u'9'1(x1) weight: 0 u'6'1(x1,x2,x3,x4,x5) weight: 0 #u'14'1(x1) weight: 0 p(x1) weight: 0 u'10'1(x1) weight: 0 if(x1,x2) weight: 0 #u'2'1(x1) weight: 0 nil() weight: 0 #intersect'ii'in(x1,x2) weight: x1 u'4'1(x1) weight: 0 #u'6'1(x1,x2,x3,x4,x5) weight: 0 u'2'1(x1) weight: 0 u'9'1(x1) weight: 0 #u'11'1(x1) weight: 0 tautology'i'out() weight: 0 #u'15'1(x1) weight: 0 u'15'1(x1) weight: 0 cons(x1,x2) weight: (/ 1 2) + x2 u'13'1(x1) weight: 0 reduce'ii'out() weight: 0 #u'12'2(x1) weight: 0 x'2a(x1,x2) weight: 0 u'14'1(x1) weight: 0 #tautology'i'in(x1) weight: 0 #u'4'1(x1) weight: 0 u'3'1(x1) weight: 0 #u'8'1(x1) weight: 0 #reduce'ii'in❆1_sequent(x1,x2,x3) weight: 0 sequent(x1,x2) weight: 0 #u'6'2(x1) weight: 0 u'11'1(x1) weight: 0 #u'3'1(x1) weight: 0 u'1'1(x1) weight: 0 #u'10'1(x1) weight: 0 u'16'1(x1) weight: 0 Usable rules: { } Removed DPs: #37 Number of SCCs: 1, DPs: 16, edges: 163 SCC { #4 #6 #8..10 #12..14 #16 #18 #22 #24 #28 #31 #33 #35 } Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... QLPOpS... Order(PosReal,>,MaxSum)... QWPOpS(PosReal,>,MaxSum)... Order(PosReal,>,Sum-Sum; PosReal,≥,Sum-Sum)... succeeded. iff(x1,x2) weight: (/ 1 4) + x2_1 + x2_2 + x1_1 + x1_2; 27836 + x2_1 + x2_2 + x1_1 + x1_2 tautology'i'in(x1) weight: 0; 0 #u'7'1(x1) weight: 0; 0 u'12'1(x1,x2,x3,x4,x5) weight: (/ 1 4); 0 x'2d(x1) weight: x1_1; x1_2 reduce'ii'in❆1_sequent(x1,x2,x3) weight: (/ 1 4) + x3_2 + x1_2; (/ 1 4) + x3_1 + x1_1 #u'12'1(x1,x2,x3,x4,x5) weight: 18557 + x5_1 + x4_1 + x3_1 + x3_2 + x2_1; (/ 18557 2) + x4_1 + x3_1 + x3_2 + x2_1 #reduce'ii'in(x1,x2) weight: 0; 0 #u'5'1(x1) weight: 0; 0 #u'1'1(x1) weight: 0; 0 reduce'ii'in(x1,x2) weight: 0; 0 u'7'1(x1) weight: x1_1; 9279 x'2b(x1,x2) weight: (/ 17739 2) + x1_2; (/ 1637 4) + x2_1 + x2_2 + x1_1 u'5'1(x1) weight: 0; 0 u'6'2(x1) weight: x1_2; (/ 37117 4) + x1_1 u'8'1(x1) weight: 0; 0 u'12'2(x1) weight: x1_1; x1_1 #u'13'1(x1) weight: 0; 0 #u'16'1(x1) weight: 0; 0 intersect'ii'out() weight: (/ 1 4); (/ 1 4) intersect'ii'in(x1,x2) weight: x2_2; x2_2 #u'9'1(x1) weight: 0; 0 u'6'1(x1,x2,x3,x4,x5) weight: x5_2 + x2_2; (/ 37115 4) + x2_1 + x2_2 + x1_2 #u'14'1(x1) weight: 0; 0 p(x1) weight: (/ 1 4) + x1_1; (/ 75909 4) + x1_1 + x1_2 u'10'1(x1) weight: x1_1; x1_2 if(x1,x2) weight: (/ 1545 4) + x1_1; (/ 17785 2) + x2_1 + x2_2 + x1_2 #u'2'1(x1) weight: 0; 0 nil() weight: 0; 0 #intersect'ii'in(x1,x2) weight: 0; 0 u'4'1(x1) weight: x1_1; x1_2 #u'6'1(x1,x2,x3,x4,x5) weight: (/ 74229 4) + x5_1 + x4_1 + x3_1 + x2_1 + x2_2; (/ 18557 2) + x4_1 + x3_1 + x2_1 + x2_2 u'2'1(x1) weight: (/ 1 4) + x1_1 + x1_2; (/ 1 4) u'9'1(x1) weight: (/ 1 4); (/ 1 4) + x1_1 #u'11'1(x1) weight: 0; 0 tautology'i'out() weight: 0; 0 #u'15'1(x1) weight: 0; 0 u'15'1(x1) weight: (/ 3 4); (/ 1 2) + x1_2 cons(x1,x2) weight: (/ 18557 2) + x2_1 + x1_1 + x1_2; (/ 1 4) + x2_2 u'13'1(x1) weight: 0; (/ 1 2) reduce'ii'out() weight: (/ 1 4); (/ 3 4) #u'12'2(x1) weight: 0; 0 x'2a(x1,x2) weight: (/ 1 4); (/ 37113 4) + x2_1 + x2_2 + x1_1 + x1_2 u'14'1(x1) weight: x1_2; (/ 3 4) #tautology'i'in(x1) weight: 0; 0 #u'4'1(x1) weight: 0; 0 u'3'1(x1) weight: (/ 1 4); (/ 1 4) + x1_2 #u'8'1(x1) weight: 0; 0 #reduce'ii'in❆1_sequent(x1,x2,x3) weight: x3_1 + x2_1 + x1_1; x2_1 + x1_1 sequent(x1,x2) weight: x2_1; (/ 1 4) + x2_1 + x1_1 + x1_2 #u'6'2(x1) weight: 0; 0 u'11'1(x1) weight: x1_2; (/ 1 2) #u'3'1(x1) weight: 0; 0 u'1'1(x1) weight: (/ 1 2) + x1_2; (/ 1 2) #u'10'1(x1) weight: 0; 0 u'16'1(x1) weight: 0; 0 Usable rules: { } Removed DPs: #6 #8 #10 #14 #24 #28 #31 #33 Number of SCCs: 2, DPs: 6, edges: 24 SCC { #4 #12 #16 #18 #22 #35 } Removing DPs: Order(PosReal,>,Sum)... succeeded. iff(x1,x2) weight: (/ 1 4) tautology'i'in(x1) weight: 0 #u'7'1(x1) weight: 0 u'12'1(x1,x2,x3,x4,x5) weight: (/ 1 4) + x1 + x2 + x3 + x4 + x5 x'2d(x1) weight: (/ 1 4) + x1 reduce'ii'in❆1_sequent(x1,x2,x3) weight: (/ 1 4) + x3 #u'12'1(x1,x2,x3,x4,x5) weight: 0 #reduce'ii'in(x1,x2) weight: 0 #u'5'1(x1) weight: 0 #u'1'1(x1) weight: 0 reduce'ii'in(x1,x2) weight: 0 u'7'1(x1) weight: (/ 1 4) + x1 x'2b(x1,x2) weight: (/ 1 4) + x1 u'5'1(x1) weight: (/ 1 4) + x1 u'6'2(x1) weight: (/ 1 4) + x1 u'8'1(x1) weight: (/ 1 4) + x1 u'12'2(x1) weight: (/ 1 4) + x1 #u'13'1(x1) weight: 0 #u'16'1(x1) weight: 0 intersect'ii'out() weight: 0 intersect'ii'in(x1,x2) weight: (/ 1 4) + x1 #u'9'1(x1) weight: 0 u'6'1(x1,x2,x3,x4,x5) weight: (/ 1 4) + x1 + x2 #u'14'1(x1) weight: 0 p(x1) weight: (/ 1 4) + x1 u'10'1(x1) weight: (/ 1 4) + x1 if(x1,x2) weight: (/ 3 4) + x1 + x2 #u'2'1(x1) weight: 0 nil() weight: 0 #intersect'ii'in(x1,x2) weight: 0 u'4'1(x1) weight: (/ 1 4) + x1 #u'6'1(x1,x2,x3,x4,x5) weight: 0 u'2'1(x1) weight: (/ 71909 2) + x1 u'9'1(x1) weight: (/ 1 2) #u'11'1(x1) weight: 0 tautology'i'out() weight: 0 #u'15'1(x1) weight: 0 u'15'1(x1) weight: (/ 1 2) + x1 cons(x1,x2) weight: (/ 143817 4) + x1 + x2 u'13'1(x1) weight: (/ 1 4) + x1 reduce'ii'out() weight: 0 #u'12'2(x1) weight: 0 x'2a(x1,x2) weight: (/ 71909 2) + x1 + x2 u'14'1(x1) weight: (/ 1 4) + x1 #tautology'i'in(x1) weight: 0 #u'4'1(x1) weight: 0 u'3'1(x1) weight: (/ 1 2) #u'8'1(x1) weight: 0 #reduce'ii'in❆1_sequent(x1,x2,x3) weight: x1 + x2 + x3 sequent(x1,x2) weight: (/ 1 4) #u'6'2(x1) weight: 0 u'11'1(x1) weight: (/ 1 2) #u'3'1(x1) weight: 0 u'1'1(x1) weight: (/ 1 2) #u'10'1(x1) weight: 0 u'16'1(x1) weight: 0 Usable rules: { } Removed DPs: #4 #12 #16 #18 #22 #35 Number of SCCs: 1, DPs: 0, edges: 0 YES