- : unit = () h : heuristic = - : unit = () APPLY CRITERIA (Marked dependency pairs) TRS termination of: [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 Sub problem: guided: DP termination of: END GUIDED APPLY CRITERIA (Graph splitting) Found 2 components: { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } { --> --> --> --> } APPLY CRITERIA (Choosing graph) Trying to solve the following constraints: { intersect'ii'in(cons(X,X0),cons(X,X1)) >= intersect'ii'out ; intersect'ii'in(cons(X0,Xs),Ys) >= u'2'1(intersect'ii'in(Xs,Ys)) ; intersect'ii'in(Xs,cons(X0,Ys)) >= u'1'1(intersect'ii'in(Xs,Ys)) ; u'1'1(intersect'ii'out) >= intersect'ii'out ; u'2'1(intersect'ii'out) >= intersect'ii'out ; u'3'1(reduce'ii'out) >= reduce'ii'out ; 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) ; reduce'ii'in(sequent(cons(x'2d(F1),Fs),Gs),NF) >= u'7'1(reduce'ii'in( sequent(Fs, cons(F1,Gs)), NF)) ; 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)) ; 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)) ; 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)) ; 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))) ; 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)))) ; reduce'ii'in(sequent(nil,nil),sequent(F1,F2)) >= u'15'1(intersect'ii'in( F1,F2)) ; 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)) ; reduce'ii'in(sequent(Fs,cons(x'2d(G1),Gs)),NF) >= u'13'1(reduce'ii'in( sequent(cons(G1,Fs), Gs),NF)) ; 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)) ; 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) ; 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)) ; u'4'1(reduce'ii'out) >= reduce'ii'out ; u'5'1(reduce'ii'out) >= reduce'ii'out ; u'6'1(reduce'ii'out,F2,Fs,Gs,NF) >= u'6'2(reduce'ii'in(sequent(cons(F2,Fs), Gs),NF)) ; u'6'2(reduce'ii'out) >= reduce'ii'out ; u'7'1(reduce'ii'out) >= reduce'ii'out ; u'8'1(reduce'ii'out) >= reduce'ii'out ; u'9'1(reduce'ii'out) >= reduce'ii'out ; u'10'1(reduce'ii'out) >= reduce'ii'out ; u'11'1(reduce'ii'out) >= reduce'ii'out ; u'12'1(reduce'ii'out,Fs,G2,Gs,NF) >= u'12'2(reduce'ii'in(sequent(Fs, cons(G2,Gs)), NF)) ; u'12'2(reduce'ii'out) >= reduce'ii'out ; u'13'1(reduce'ii'out) >= reduce'ii'out ; u'14'1(reduce'ii'out) >= reduce'ii'out ; u'15'1(intersect'ii'out) >= reduce'ii'out ; u'16'1(reduce'ii'out) >= tautology'i'out ; tautology'i'in(F) >= u'16'1(reduce'ii'in(sequent(nil,cons(F,nil)), sequent(nil,nil))) ; Marked_reduce'ii'in(sequent(cons(x'2b(F1,F2),Fs),Gs),NF) >= Marked_reduce'ii'in( sequent( cons( F1,Fs), Gs),NF) ; Marked_reduce'ii'in(sequent(cons(x'2b(F1,F2),Fs),Gs),NF) >= Marked_u'6'1( reduce'ii'in( sequent( cons( F1, Fs), Gs), NF),F2, Fs,Gs, NF) ; Marked_reduce'ii'in(sequent(cons(x'2d(F1),Fs),Gs),NF) >= Marked_reduce'ii'in( sequent(Fs, cons(F1,Gs)), NF) ; Marked_reduce'ii'in(sequent(cons(if(A,B),Fs),Gs),NF) >= Marked_reduce'ii'in( sequent(cons( x'2b( x'2d( B), A), Fs), Gs),NF) ; Marked_reduce'ii'in(sequent(cons(x'2a(F1,F2),Fs),Gs),NF) >= Marked_reduce'ii'in( sequent( cons( F1, cons(F2,Fs)), Gs),NF) ; Marked_reduce'ii'in(sequent(cons(iff(A,B),Fs),Gs),NF) >= Marked_reduce'ii'in( sequent(cons( x'2a( if( A, B), if(B,A)), Fs), Gs),NF) ; Marked_reduce'ii'in(sequent(cons(p(V),Fs),Gs),sequent(Left,Right)) >= Marked_reduce'ii'in(sequent(Fs,Gs),sequent(cons(p(V),Left),Right)) ; Marked_reduce'ii'in(sequent(nil,cons(p(V),Gs)),sequent(Left,Right)) >= Marked_reduce'ii'in(sequent(nil,Gs),sequent(Left,cons(p(V),Right))) ; Marked_reduce'ii'in(sequent(Fs,cons(x'2b(G1,G2),Gs)),NF) >= Marked_reduce'ii'in( sequent( Fs, cons( G1, cons(G2,Gs))), NF) ; Marked_reduce'ii'in(sequent(Fs,cons(x'2d(G1),Gs)),NF) >= Marked_reduce'ii'in( sequent(cons(G1,Fs), Gs),NF) ; Marked_reduce'ii'in(sequent(Fs,cons(if(A,B),Gs)),NF) >= Marked_reduce'ii'in( sequent(Fs, cons(x'2b( x'2d(B), A), Gs)),NF) ; Marked_reduce'ii'in(sequent(Fs,cons(x'2a(G1,G2),Gs)),NF) >= Marked_reduce'ii'in( sequent( Fs,cons(G1,Gs)), NF) ; Marked_reduce'ii'in(sequent(Fs,cons(x'2a(G1,G2),Gs)),NF) >= Marked_u'12'1( reduce'ii'in( sequent( Fs, cons(G1,Gs)), NF),Fs, G2,Gs, NF) ; Marked_reduce'ii'in(sequent(Fs,cons(iff(A,B),Gs)),NF) >= Marked_reduce'ii'in( sequent(Fs, cons(x'2a( if(A,B), if(B,A)), Gs)),NF) ; Marked_u'12'1(reduce'ii'out,Fs,G2,Gs,NF) >= Marked_reduce'ii'in(sequent( Fs, cons(G2,Gs)), NF) ; Marked_u'6'1(reduce'ii'out,F2,Fs,Gs,NF) >= Marked_reduce'ii'in(sequent( cons( F2, Fs), Gs), NF) ; } + Disjunctions:{ { Marked_reduce'ii'in(sequent(cons(x'2b(F1,F2),Fs),Gs),NF) > Marked_reduce'ii'in( sequent( cons(F1, Fs),Gs), NF) ; } { Marked_reduce'ii'in(sequent(cons(x'2b(F1,F2),Fs),Gs),NF) > Marked_u'6'1( reduce'ii'in( sequent( cons( F1,Fs), Gs),NF), F2,Fs,Gs, NF) ; } { Marked_reduce'ii'in(sequent(cons(x'2d(F1),Fs),Gs),NF) > Marked_reduce'ii'in( sequent(Fs, cons(F1,Gs)), NF) ; } { Marked_reduce'ii'in(sequent(cons(if(A,B),Fs),Gs),NF) > Marked_reduce'ii'in( sequent(cons( x'2b( x'2d(B), A), Fs), Gs),NF) ; } { Marked_reduce'ii'in(sequent(cons(x'2a(F1,F2),Fs),Gs),NF) > Marked_reduce'ii'in( sequent( cons(F1, cons(F2,Fs)), Gs),NF) ; } { Marked_reduce'ii'in(sequent(cons(iff(A,B),Fs),Gs),NF) > Marked_reduce'ii'in( sequent(cons( x'2a( if( A, B), if(B,A)), Fs), Gs),NF) ; } { Marked_reduce'ii'in(sequent(cons(p(V),Fs),Gs),sequent(Left,Right)) > Marked_reduce'ii'in(sequent(Fs,Gs),sequent(cons(p(V),Left),Right)) ; } { Marked_reduce'ii'in(sequent(nil,cons(p(V),Gs)),sequent(Left,Right)) > Marked_reduce'ii'in(sequent(nil,Gs),sequent(Left,cons(p(V),Right))) ; } { Marked_reduce'ii'in(sequent(Fs,cons(x'2b(G1,G2),Gs)),NF) > Marked_reduce'ii'in( sequent( Fs, cons(G1, cons(G2,Gs))), NF) ; } { Marked_reduce'ii'in(sequent(Fs,cons(x'2d(G1),Gs)),NF) > Marked_reduce'ii'in( sequent(cons(G1,Fs), Gs),NF) ; } { Marked_reduce'ii'in(sequent(Fs,cons(if(A,B),Gs)),NF) > Marked_reduce'ii'in( sequent(Fs, cons(x'2b(x'2d(B),A), Gs)),NF) ; } { Marked_reduce'ii'in(sequent(Fs,cons(x'2a(G1,G2),Gs)),NF) > Marked_reduce'ii'in( sequent( Fs,cons(G1,Gs)), NF) ; } { Marked_reduce'ii'in(sequent(Fs,cons(x'2a(G1,G2),Gs)),NF) > Marked_u'12'1( reduce'ii'in( sequent( Fs,cons(G1,Gs)), NF),Fs, G2,Gs,NF) ; } { Marked_reduce'ii'in(sequent(Fs,cons(iff(A,B),Gs)),NF) > Marked_reduce'ii'in( sequent(Fs, cons(x'2a( if(A,B), if(B,A)), Gs)),NF) ; } { Marked_u'12'1(reduce'ii'out,Fs,G2,Gs,NF) > Marked_reduce'ii'in(sequent( Fs, cons(G2,Gs)), NF) ; } { Marked_u'6'1(reduce'ii'out,F2,Fs,Gs,NF) > Marked_reduce'ii'in(sequent( cons( F2, Fs), Gs), NF) ; } } === TIMER virtual : 10.000000 === Entering poly_solver Starting Sat solver initialization Calling Sat solver... === STOPING TIMER virtual === === TIMER real : 10.000000 === === STOPING TIMER real === Sat solver returned Sat solver result read === STOPING TIMER real === === STOPING TIMER virtual === constraint: intersect'ii'in(cons(X,X0),cons(X,X1)) >= intersect'ii'out constraint: intersect'ii'in(cons(X0,Xs),Ys) >= u'2'1(intersect'ii'in(Xs,Ys)) constraint: intersect'ii'in(Xs,cons(X0,Ys)) >= u'1'1(intersect'ii'in(Xs,Ys)) constraint: u'1'1(intersect'ii'out) >= intersect'ii'out constraint: u'2'1(intersect'ii'out) >= intersect'ii'out constraint: u'3'1(reduce'ii'out) >= reduce'ii'out constraint: 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) constraint: reduce'ii'in(sequent(cons(x'2d(F1),Fs),Gs),NF) >= u'7'1(reduce'ii'in( sequent( Fs, cons(F1,Gs)), NF)) constraint: 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)) constraint: 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)) constraint: 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)) constraint: 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))) constraint: 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)))) constraint: reduce'ii'in(sequent(nil,nil),sequent(F1,F2)) >= u'15'1(intersect'ii'in( F1, F2)) constraint: 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)) constraint: reduce'ii'in(sequent(Fs,cons(x'2d(G1),Gs)),NF) >= u'13'1( reduce'ii'in( sequent( cons( G1, Fs), Gs), NF)) constraint: 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)) constraint: 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) constraint: 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)) constraint: u'4'1(reduce'ii'out) >= reduce'ii'out constraint: u'5'1(reduce'ii'out) >= reduce'ii'out constraint: u'6'1(reduce'ii'out,F2,Fs,Gs,NF) >= u'6'2(reduce'ii'in(sequent( cons( F2, Fs), Gs), NF)) constraint: u'6'2(reduce'ii'out) >= reduce'ii'out constraint: u'7'1(reduce'ii'out) >= reduce'ii'out constraint: u'8'1(reduce'ii'out) >= reduce'ii'out constraint: u'9'1(reduce'ii'out) >= reduce'ii'out constraint: u'10'1(reduce'ii'out) >= reduce'ii'out constraint: u'11'1(reduce'ii'out) >= reduce'ii'out constraint: u'12'1(reduce'ii'out,Fs,G2,Gs,NF) >= u'12'2(reduce'ii'in( sequent(Fs, cons(G2,Gs)), NF)) constraint: u'12'2(reduce'ii'out) >= reduce'ii'out constraint: u'13'1(reduce'ii'out) >= reduce'ii'out constraint: u'14'1(reduce'ii'out) >= reduce'ii'out constraint: u'15'1(intersect'ii'out) >= reduce'ii'out constraint: u'16'1(reduce'ii'out) >= tautology'i'out constraint: tautology'i'in(F) >= u'16'1(reduce'ii'in(sequent(nil,cons(F,nil)), sequent(nil,nil))) constraint: Marked_reduce'ii'in(sequent(cons(x'2b(F1,F2),Fs),Gs),NF) >= Marked_reduce'ii'in(sequent(cons(F1,Fs),Gs),NF) constraint: Marked_reduce'ii'in(sequent(cons(x'2b(F1,F2),Fs),Gs),NF) >= Marked_u'6'1(reduce'ii'in(sequent(cons(F1,Fs),Gs),NF),F2,Fs,Gs,NF) constraint: Marked_reduce'ii'in(sequent(cons(x'2d(F1),Fs),Gs),NF) >= Marked_reduce'ii'in(sequent(Fs,cons(F1,Gs)),NF) constraint: Marked_reduce'ii'in(sequent(cons(if(A,B),Fs),Gs),NF) >= Marked_reduce'ii'in( sequent( cons( x'2b( x'2d( B), A), Fs), Gs), NF) constraint: Marked_reduce'ii'in(sequent(cons(x'2a(F1,F2),Fs),Gs),NF) >= Marked_reduce'ii'in(sequent(cons(F1,cons(F2,Fs)),Gs),NF) constraint: Marked_reduce'ii'in(sequent(cons(iff(A,B),Fs),Gs),NF) >= Marked_reduce'ii'in(sequent(cons(x'2a(if(A,B),if(B,A)),Fs),Gs),NF) constraint: Marked_reduce'ii'in(sequent(cons(p(V),Fs),Gs),sequent(Left,Right)) >= Marked_reduce'ii'in(sequent(Fs,Gs),sequent(cons(p(V),Left),Right)) constraint: Marked_reduce'ii'in(sequent(nil,cons(p(V),Gs)),sequent(Left,Right)) >= Marked_reduce'ii'in(sequent(nil,Gs),sequent(Left,cons(p(V),Right))) constraint: Marked_reduce'ii'in(sequent(Fs,cons(x'2b(G1,G2),Gs)),NF) >= Marked_reduce'ii'in(sequent(Fs,cons(G1,cons(G2,Gs))),NF) constraint: Marked_reduce'ii'in(sequent(Fs,cons(x'2d(G1),Gs)),NF) >= Marked_reduce'ii'in(sequent(cons(G1,Fs),Gs),NF) constraint: Marked_reduce'ii'in(sequent(Fs,cons(if(A,B),Gs)),NF) >= Marked_reduce'ii'in( sequent( Fs, cons( x'2b( x'2d( B), A), Gs)), NF) constraint: Marked_reduce'ii'in(sequent(Fs,cons(x'2a(G1,G2),Gs)),NF) >= Marked_reduce'ii'in(sequent(Fs,cons(G1,Gs)),NF) constraint: Marked_reduce'ii'in(sequent(Fs,cons(x'2a(G1,G2),Gs)),NF) >= Marked_u'12'1(reduce'ii'in(sequent(Fs,cons(G1,Gs)),NF),Fs,G2,Gs,NF) constraint: Marked_reduce'ii'in(sequent(Fs,cons(iff(A,B),Gs)),NF) >= Marked_reduce'ii'in(sequent(Fs,cons(x'2a(if(A,B),if(B,A)),Gs)),NF) constraint: Marked_u'12'1(reduce'ii'out,Fs,G2,Gs,NF) >= Marked_reduce'ii'in( sequent(Fs, cons(G2,Gs)), NF) constraint: Marked_u'6'1(reduce'ii'out,F2,Fs,Gs,NF) >= Marked_reduce'ii'in( sequent(cons(F2,Fs), Gs),NF) APPLY CRITERIA (Choosing graph) Trying to solve the following constraints: { intersect'ii'in(cons(X,X0),cons(X,X1)) >= intersect'ii'out ; intersect'ii'in(cons(X0,Xs),Ys) >= u'2'1(intersect'ii'in(Xs,Ys)) ; intersect'ii'in(Xs,cons(X0,Ys)) >= u'1'1(intersect'ii'in(Xs,Ys)) ; u'1'1(intersect'ii'out) >= intersect'ii'out ; u'2'1(intersect'ii'out) >= intersect'ii'out ; u'3'1(reduce'ii'out) >= reduce'ii'out ; 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) ; reduce'ii'in(sequent(cons(x'2d(F1),Fs),Gs),NF) >= u'7'1(reduce'ii'in( sequent(Fs, cons(F1,Gs)), NF)) ; 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)) ; 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)) ; 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)) ; 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))) ; 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)))) ; reduce'ii'in(sequent(nil,nil),sequent(F1,F2)) >= u'15'1(intersect'ii'in( F1,F2)) ; 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)) ; reduce'ii'in(sequent(Fs,cons(x'2d(G1),Gs)),NF) >= u'13'1(reduce'ii'in( sequent(cons(G1,Fs), Gs),NF)) ; 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)) ; 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) ; 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)) ; u'4'1(reduce'ii'out) >= reduce'ii'out ; u'5'1(reduce'ii'out) >= reduce'ii'out ; u'6'1(reduce'ii'out,F2,Fs,Gs,NF) >= u'6'2(reduce'ii'in(sequent(cons(F2,Fs), Gs),NF)) ; u'6'2(reduce'ii'out) >= reduce'ii'out ; u'7'1(reduce'ii'out) >= reduce'ii'out ; u'8'1(reduce'ii'out) >= reduce'ii'out ; u'9'1(reduce'ii'out) >= reduce'ii'out ; u'10'1(reduce'ii'out) >= reduce'ii'out ; u'11'1(reduce'ii'out) >= reduce'ii'out ; u'12'1(reduce'ii'out,Fs,G2,Gs,NF) >= u'12'2(reduce'ii'in(sequent(Fs, cons(G2,Gs)), NF)) ; u'12'2(reduce'ii'out) >= reduce'ii'out ; u'13'1(reduce'ii'out) >= reduce'ii'out ; u'14'1(reduce'ii'out) >= reduce'ii'out ; u'15'1(intersect'ii'out) >= reduce'ii'out ; u'16'1(reduce'ii'out) >= tautology'i'out ; tautology'i'in(F) >= u'16'1(reduce'ii'in(sequent(nil,cons(F,nil)), sequent(nil,nil))) ; Marked_intersect'ii'in(cons(X0,Xs),Ys) >= Marked_intersect'ii'in(Xs,Ys) ; Marked_intersect'ii'in(Xs,cons(X0,Ys)) >= Marked_intersect'ii'in(Xs,Ys) ; } + Disjunctions:{ { Marked_intersect'ii'in(cons(X0,Xs),Ys) > Marked_intersect'ii'in(Xs,Ys) ; } { Marked_intersect'ii'in(Xs,cons(X0,Ys)) > Marked_intersect'ii'in(Xs,Ys) ; } } === TIMER virtual : 10.000000 === Entering poly_solver Starting Sat solver initialization Calling Sat solver... === STOPING TIMER virtual === === TIMER real : 10.000000 === === STOPING TIMER real === Sat solver returned Sat solver result read === STOPING TIMER real === === STOPING TIMER virtual === constraint: intersect'ii'in(cons(X,X0),cons(X,X1)) >= intersect'ii'out constraint: intersect'ii'in(cons(X0,Xs),Ys) >= u'2'1(intersect'ii'in(Xs,Ys)) constraint: intersect'ii'in(Xs,cons(X0,Ys)) >= u'1'1(intersect'ii'in(Xs,Ys)) constraint: u'1'1(intersect'ii'out) >= intersect'ii'out constraint: u'2'1(intersect'ii'out) >= intersect'ii'out constraint: u'3'1(reduce'ii'out) >= reduce'ii'out constraint: 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) constraint: reduce'ii'in(sequent(cons(x'2d(F1),Fs),Gs),NF) >= u'7'1(reduce'ii'in( sequent( Fs, cons(F1,Gs)), NF)) constraint: 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)) constraint: 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)) constraint: 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)) constraint: 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))) constraint: 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)))) constraint: reduce'ii'in(sequent(nil,nil),sequent(F1,F2)) >= u'15'1(intersect'ii'in( F1, F2)) constraint: 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)) constraint: reduce'ii'in(sequent(Fs,cons(x'2d(G1),Gs)),NF) >= u'13'1( reduce'ii'in( sequent( cons( G1, Fs), Gs), NF)) constraint: 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)) constraint: 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) constraint: 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)) constraint: u'4'1(reduce'ii'out) >= reduce'ii'out constraint: u'5'1(reduce'ii'out) >= reduce'ii'out constraint: u'6'1(reduce'ii'out,F2,Fs,Gs,NF) >= u'6'2(reduce'ii'in(sequent( cons( F2, Fs), Gs), NF)) constraint: u'6'2(reduce'ii'out) >= reduce'ii'out constraint: u'7'1(reduce'ii'out) >= reduce'ii'out constraint: u'8'1(reduce'ii'out) >= reduce'ii'out constraint: u'9'1(reduce'ii'out) >= reduce'ii'out constraint: u'10'1(reduce'ii'out) >= reduce'ii'out constraint: u'11'1(reduce'ii'out) >= reduce'ii'out constraint: u'12'1(reduce'ii'out,Fs,G2,Gs,NF) >= u'12'2(reduce'ii'in( sequent(Fs, cons(G2,Gs)), NF)) constraint: u'12'2(reduce'ii'out) >= reduce'ii'out constraint: u'13'1(reduce'ii'out) >= reduce'ii'out constraint: u'14'1(reduce'ii'out) >= reduce'ii'out constraint: u'15'1(intersect'ii'out) >= reduce'ii'out constraint: u'16'1(reduce'ii'out) >= tautology'i'out constraint: tautology'i'in(F) >= u'16'1(reduce'ii'in(sequent(nil,cons(F,nil)), sequent(nil,nil))) constraint: Marked_intersect'ii'in(cons(X0,Xs),Ys) >= Marked_intersect'ii'in( Xs,Ys) constraint: Marked_intersect'ii'in(Xs,cons(X0,Ys)) >= Marked_intersect'ii'in( Xs,Ys) APPLY CRITERIA (Graph splitting) Found 1 components: { --> --> --> --> --> --> --> --> --> --> --> --> --> --> -->