The dog likes the mouse. The mouse is kind. The mouse sees the dog. The mouse sees the rabbit. The mouse sees the tiger. The rabbit likes the mouse. The rabbit does not see the mouse. The rabbit does not visit the dog. The rabbit does not visit the tiger. The tiger likes the dog. The tiger does not see the dog. The tiger does not visit the mouse. If something visits the dog then the dog visits the tiger. If something sees the tiger then it is big. If something likes the rabbit then the rabbit sees the tiger. If something likes the tiger and it sees the mouse then the mouse is kind. If something is big then it likes the rabbit. If something is green and it sees the tiger then it likes the tiger. If something sees the mouse then the mouse sees the rabbit. If something visits the rabbit then the rabbit is not young.
The dog likes the mouse.
("dog" "likes" "mouse" "+")
The mouse is kind.
("mouse" "is" "kind" "+")
The mouse sees the dog.
("mouse" "sees" "dog" "+")
The mouse sees the rabbit.
("mouse" "sees" "rabbit" "+")
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
The rabbit does not see the mouse.
("rabbit" "sees" "mouse" "-")
The rabbit does not visit the dog.
("rabbit" "visits" "dog" "-")
The rabbit does not visit the tiger.
("rabbit" "visits" "tiger" "-")
The tiger likes the dog.
("tiger" "likes" "dog" "+")
The tiger does not see the dog.
("tiger" "sees" "dog" "-")
The tiger does not visit the mouse.
("tiger" "visits" "mouse" "-")
If something visits the dog then the dog visits the tiger.
((("something" "visits" "dog" "+")) -> ("dog" "visits" "tiger" "+"))
If something sees the tiger then it is big.
((("something" "sees" "tiger" "+")) -> ("something" "is" "big" "+"))
If something likes the rabbit then the rabbit sees the tiger.
((("something" "likes" "rabbit" "+")) -> ("rabbit" "sees" "tiger" "+"))
If something likes the tiger and it sees the mouse then the mouse is kind.
((("something" "likes" "tiger" "+") ("something" "sees" "mouse" "+")) -> ("mouse" "is" "kind" "+"))
If something is big then it likes the rabbit.
((("something" "is" "big" "+")) -> ("something" "likes" "rabbit" "+"))
If something is green and it sees the tiger then it likes the tiger.
((("something" "is" "green" "+") ("something" "sees" "tiger" "+")) -> ("something" "likes" "tiger" "+"))
If something sees the mouse then the mouse sees the rabbit.
((("something" "sees" "mouse" "+")) -> ("mouse" "sees" "rabbit" "+"))
If something visits the rabbit then the rabbit is not young.
((("something" "visits" "rabbit" "+")) -> ("rabbit" "is" "young" "-"))
The mouse sees the tiger.
True
1
proof
[(triple5)]
("mouse" "sees" "tiger" "+")
triple5
The tiger visits the mouse.
False
1
inv-proof
[(triple12)]
("tiger" "visits" "mouse" "+")
triple12
The mouse is big.
True
2
proof
[(((triple5) -> rule2))]
("mouse" "is" "big" "+")
((triple5) -> (rule2 % int1))
The mouse is big.
("mouse" "is" "big" "+")
int1
The mouse is not big.
False
2
inv-proof
[(((triple5) -> rule2))]
("mouse" "is" "big" "-")
((triple5) -> (rule2 % int1))
The mouse is big.
("mouse" "is" "big" "+")
int1
The mouse likes the rabbit.
True
3
proof
[(((((triple5) -> rule2)) -> rule5))]
("mouse" "likes" "rabbit" "+")
((((triple5) -> (rule2 % int2))) -> (rule5 % int1))
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
int1
The mouse is big.
("mouse" "is" "big" "+")
int2
The mouse does not like the rabbit.
False
3
inv-proof
[(((((triple5) -> rule2)) -> rule5))]
("mouse" "likes" "rabbit" "-")
((((triple5) -> (rule2 % int2))) -> (rule5 % int1))
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
int1
The mouse is big.
("mouse" "is" "big" "+")
int2
The rabbit sees the tiger.
True
4
proof
[(((((((triple5) -> rule2)) -> rule5)) -> rule3))]
("rabbit" "sees" "tiger" "+")
((((((triple5) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
int1
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
int2
The mouse is big.
("mouse" "is" "big" "+")
int3
The rabbit does not see the tiger.
False
4
inv-proof
[(((((((triple5) -> rule2)) -> rule5)) -> rule3))]
("rabbit" "sees" "tiger" "-")
((((((triple5) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
int1
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
int2
The mouse is big.
("mouse" "is" "big" "+")
int3
The rabbit is big.
True
5
proof
[(((((((((triple5) -> rule2)) -> rule5)) -> rule3)) -> rule2))]
("rabbit" "is" "big" "+")
((((((((triple5) -> (rule2 % int4))) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The rabbit is big.
("rabbit" "is" "big" "+")
int1
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
int2
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
int3
The mouse is big.
("mouse" "is" "big" "+")
int4
The rabbit is not big.
False
5
inv-proof
[(((((((((triple5) -> rule2)) -> rule5)) -> rule3)) -> rule2))]
("rabbit" "is" "big" "-")
((((((((triple5) -> (rule2 % int4))) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The rabbit is big.
("rabbit" "is" "big" "+")
int1
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
int2
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
int3
The mouse is big.
("mouse" "is" "big" "+")
int4
The rabbit likes the rabbit.
True
6
proof
[(((((((((((triple5) -> rule2)) -> rule5)) -> rule3)) -> rule2)) -> rule5))]
("rabbit" "likes" "rabbit" "+")
((((((((((triple5) -> (rule2 % int5))) -> (rule5 % int4))) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
int1
The rabbit is big.
("rabbit" "is" "big" "+")
int2
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
int3
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
int4
The mouse is big.
("mouse" "is" "big" "+")
int5
The rabbit does not like the rabbit.
False
6
inv-proof
[(((((((((((triple5) -> rule2)) -> rule5)) -> rule3)) -> rule2)) -> rule5))]
("rabbit" "likes" "rabbit" "-")
((((((((((triple5) -> (rule2 % int5))) -> (rule5 % int4))) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
int1
The rabbit is big.
("rabbit" "is" "big" "+")
int2
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
int3
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
int4
The mouse is big.
("mouse" "is" "big" "+")
int5
The dog is not big.
Unknown
inv-rconc
[@1: The dog is big.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("dog" "is" "big" "-")
The dog visits the tiger.
Unknown
rconc
[@1: The dog visits the tiger.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("dog" "visits" "tiger" "+")
The dog does not like the rabbit.
Unknown
inv-rconc
[@2: The dog likes the rabbit.[CWA. Example of deepest failure = (rule5 <- rule2 <- FAIL)]]
("dog" "likes" "rabbit" "-")
The tiger likes the tiger.
Unknown
rconc
[@1: The tiger likes the tiger.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("tiger" "likes" "tiger" "+")
The mouse does not like the tiger.
Unknown
inv-rconc
[@1: The mouse likes the tiger.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("mouse" "likes" "tiger" "-")
The dog likes the tiger.
Unknown
rconc
[@1: The dog likes the tiger.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("dog" "likes" "tiger" "+")
The dog is not kind.
Unknown
inv-random
[@0: The dog is kind.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "kind" "-")
The dog visits the mouse.
Unknown
random
[@0: The dog visits the mouse.[CWA. Example of deepest failure = (FAIL)]]
("dog" "visits" "mouse" "+")
The rabbit is not rough.
Unknown
inv-random
[@0: The rabbit is rough.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "rough" "-")
The tiger sees the tiger.
Unknown
random
[@0: The tiger sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "tiger" "+")
The dog does not visit the rabbit.
Unknown
inv-random
[@0: The dog visits the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("dog" "visits" "rabbit" "-")
The dog sees the dog.
Unknown
random
[@0: The dog sees the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "sees" "dog" "+")
@0: The dog likes the mouse.[(triple1)] The mouse is kind.[(triple2)] The mouse sees the dog.[(triple3)] The mouse sees the rabbit.[(triple4)] The mouse sees the tiger.[(triple5)] The rabbit does not see the mouse.[(triple7)] The rabbit does not visit the dog.[(triple8)] The rabbit does not visit the tiger.[(triple9)] The rabbit likes the mouse.[(triple6)] The tiger does not see the dog.[(triple11)] The tiger does not visit the mouse.[(triple12)] The tiger likes the dog.[(triple10)] @1: The mouse is big.[(((triple5) -> rule2))] @2: The mouse likes the rabbit.[(((((triple5) -> rule2)) -> rule5))] @3: The rabbit sees the tiger.[(((((((triple5) -> rule2)) -> rule5)) -> rule3))] @4: The rabbit is big.[(((((((((triple5) -> rule2)) -> rule5)) -> rule3)) -> rule2))] @5: The rabbit likes the rabbit.[(((((((((((triple5) -> rule2)) -> rule5)) -> rule3)) -> rule2)) -> rule5))]
The dog likes the mouse.
("dog" "likes" "mouse" "+")
triple1
The mouse is kind.
("mouse" "is" "kind" "+")
triple2
The mouse sees the dog.
("mouse" "sees" "dog" "+")
triple3
The mouse sees the rabbit.
("mouse" "sees" "rabbit" "+")
triple4
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
triple5
The rabbit does not see the mouse.
("rabbit" "sees" "mouse" "-")
triple7
The rabbit does not visit the dog.
("rabbit" "visits" "dog" "-")
triple8
The rabbit does not visit the tiger.
("rabbit" "visits" "tiger" "-")
triple9
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
triple6
The tiger does not see the dog.
("tiger" "sees" "dog" "-")
triple11
The tiger does not visit the mouse.
("tiger" "visits" "mouse" "-")
triple12
The tiger likes the dog.
("tiger" "likes" "dog" "+")
triple10
The mouse is big.
("mouse" "is" "big" "+")
((triple5) -> (rule2 % int1))
The mouse is big.
("mouse" "is" "big" "+")
int1
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
((((triple5) -> (rule2 % int2))) -> (rule5 % int1))
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
int1
The mouse is big.
("mouse" "is" "big" "+")
int2
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
((((((triple5) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
int1
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
int2
The mouse is big.
("mouse" "is" "big" "+")
int3
The rabbit is big.
("rabbit" "is" "big" "+")
((((((((triple5) -> (rule2 % int4))) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The rabbit is big.
("rabbit" "is" "big" "+")
int1
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
int2
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
int3
The mouse is big.
("mouse" "is" "big" "+")
int4
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
((((((((((triple5) -> (rule2 % int5))) -> (rule5 % int4))) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
int1
The rabbit is big.
("rabbit" "is" "big" "+")
int2
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
int3
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
int4
The mouse is big.
("mouse" "is" "big" "+")
int5