The dog likes the rabbit. The dog likes the tiger. The dog sees the tiger. The mouse chases the tiger. The mouse sees the dog. The mouse sees the rabbit. The rabbit likes the dog. The rabbit sees the tiger. The tiger is green. The tiger likes the mouse. If someone chases the mouse and the mouse sees the rabbit then the rabbit is rough. If someone is rough and they like the dog then they are blue. If someone chases the mouse then the mouse is green. If the mouse chases the dog and the mouse sees the dog then the dog sees the mouse. If someone sees the tiger and they are blue then they see the mouse. If someone is green and they chase the rabbit then they chase the dog. If someone likes the tiger then they chase the mouse. If someone sees the dog then they chase the rabbit.
The dog likes the rabbit.
("dog" "likes" "rabbit" "+")
The dog likes the tiger.
("dog" "likes" "tiger" "+")
The dog sees the tiger.
("dog" "sees" "tiger" "+")
The mouse chases the tiger.
("mouse" "chases" "tiger" "+")
The mouse sees the dog.
("mouse" "sees" "dog" "+")
The mouse sees the rabbit.
("mouse" "sees" "rabbit" "+")
The rabbit likes the dog.
("rabbit" "likes" "dog" "+")
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
The tiger is green.
("tiger" "is" "green" "+")
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
If someone chases the mouse and the mouse sees the rabbit then the rabbit is rough.
((("someone" "chases" "mouse" "+") ("mouse" "sees" "rabbit" "+")) -> ("rabbit" "is" "rough" "+"))
If someone is rough and they like the dog then they are blue.
((("someone" "is" "rough" "+") ("someone" "likes" "dog" "+")) -> ("someone" "is" "blue" "+"))
If someone chases the mouse then the mouse is green.
((("someone" "chases" "mouse" "+")) -> ("mouse" "is" "green" "+"))
If the mouse chases the dog and the mouse sees the dog then the dog sees the mouse.
((("mouse" "chases" "dog" "+") ("mouse" "sees" "dog" "+")) -> ("dog" "sees" "mouse" "+"))
If someone sees the tiger and they are blue then they see the mouse.
((("someone" "sees" "tiger" "+") ("someone" "is" "blue" "+")) -> ("someone" "sees" "mouse" "+"))
If someone is green and they chase the rabbit then they chase the dog.
((("someone" "is" "green" "+") ("someone" "chases" "rabbit" "+")) -> ("someone" "chases" "dog" "+"))
If someone likes the tiger then they chase the mouse.
((("someone" "likes" "tiger" "+")) -> ("someone" "chases" "mouse" "+"))
If someone sees the dog then they chase the rabbit.
((("someone" "sees" "dog" "+")) -> ("someone" "chases" "rabbit" "+"))
The dog likes the tiger.
True
1
proof
[(triple2)]
("dog" "likes" "tiger" "+")
triple2
The tiger is not green.
False
1
inv-proof
[(triple9)]
("tiger" "is" "green" "-")
triple9
The dog chases the mouse.
True
2
proof
[(((triple2) -> rule7))]
("dog" "chases" "mouse" "+")
((triple2) -> (rule7 % int1))
The dog chases the mouse.
("dog" "chases" "mouse" "+")
int1
The mouse does not chase the rabbit.
False
2
inv-proof
[(((triple5) -> rule8))]
("mouse" "chases" "rabbit" "-")
((triple5) -> (rule8 % int1))
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
int1
The mouse is green.
True
3
proof
[(((((triple2) -> rule7)) -> rule3))]
("mouse" "is" "green" "+")
((((triple2) -> (rule7 % int2))) -> (rule3 % int1))
The mouse is green.
("mouse" "is" "green" "+")
int1
The dog chases the mouse.
("dog" "chases" "mouse" "+")
int2
The mouse is not green.
False
3
inv-proof
[(((((triple2) -> rule7)) -> rule3))]
("mouse" "is" "green" "-")
((((triple2) -> (rule7 % int2))) -> (rule3 % int1))
The mouse is green.
("mouse" "is" "green" "+")
int1
The dog chases the mouse.
("dog" "chases" "mouse" "+")
int2
The rabbit is blue.
True
6
proof
[(((((((triple2) -> rule7) triple6) -> rule1) triple7) -> rule2))]
("rabbit" "is" "blue" "+")
((((((triple2) -> (rule7 % int3)) triple6) -> (rule1 % int2)) triple7) -> (rule2 % int1))
The rabbit is blue.
("rabbit" "is" "blue" "+")
int1
The rabbit is rough.
("rabbit" "is" "rough" "+")
int2
The dog chases the mouse.
("dog" "chases" "mouse" "+")
int3
The mouse does not chase the dog.
False
6
inv-proof
[(((((((triple2) -> rule7)) -> rule3) ((triple5) -> rule8)) -> rule6))]
("mouse" "chases" "dog" "-")
((((((triple2) -> (rule7 % int4))) -> (rule3 % int3)) ((triple5) -> (rule8 % int2))) -> (rule6 % int1))
The mouse chases the dog.
("mouse" "chases" "dog" "+")
int1
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
int2
The mouse is green.
("mouse" "is" "green" "+")
int3
The dog chases the mouse.
("dog" "chases" "mouse" "+")
int4
The dog does not chase the dog.
Unknown
inv-rconc
[@1: The dog chases the dog.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("dog" "chases" "dog" "-")
The mouse chases the mouse.
Unknown
rconc
[@1: The mouse chases the mouse.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("mouse" "chases" "mouse" "+")
The dog does not chase the rabbit.
Unknown
inv-rconc
[@1: The dog chases the rabbit.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("dog" "chases" "rabbit" "-")
The mouse is blue.
Unknown
rconc
[@1: The mouse is blue.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("mouse" "is" "blue" "+")
The dog does not like the mouse.
Unknown
inv-random
[@0: The dog likes the mouse.[CWA. Example of deepest failure = (FAIL)]]
("dog" "likes" "mouse" "-")
The mouse is rough.
Unknown
random
[@0: The mouse is rough.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "rough" "+")
The dog does not like the dog.
Unknown
inv-random
[@0: The dog likes the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "likes" "dog" "-")
The rabbit is cold.
Unknown
random
[@0: The rabbit is cold.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "cold" "+")
@0: The dog likes the rabbit.[(triple1)] The dog likes the tiger.[(triple2)] The dog sees the tiger.[(triple3)] The mouse chases the tiger.[(triple4)] The mouse sees the dog.[(triple5)] The mouse sees the rabbit.[(triple6)] The rabbit likes the dog.[(triple7)] The rabbit sees the tiger.[(triple8)] The tiger is green.[(triple9)] The tiger likes the mouse.[(triple10)] @1: The dog chases the mouse.[(((triple2) -> rule7))] The mouse chases the rabbit.[(((triple5) -> rule8))] @2: The mouse is green.[(((((triple2) -> rule7)) -> rule3))] The rabbit is rough.[(((((triple2) -> rule7) triple6) -> rule1))] @3: The mouse chases the dog.[(((((((triple2) -> rule7)) -> rule3) ((triple5) -> rule8)) -> rule6))] The rabbit is blue.[(((((((triple2) -> rule7) triple6) -> rule1) triple7) -> rule2))] @4: The dog sees the mouse.[(((((((((triple2) -> rule7)) -> rule3) ((triple5) -> rule8)) -> rule6) triple5) -> rule4))] The rabbit sees the mouse.[(((triple8 ((((((triple2) -> rule7) triple6) -> rule1) triple7) -> rule2)) -> rule5))]
The dog likes the rabbit.
("dog" "likes" "rabbit" "+")
triple1
The dog likes the tiger.
("dog" "likes" "tiger" "+")
triple2
The dog sees the tiger.
("dog" "sees" "tiger" "+")
triple3
The mouse chases the tiger.
("mouse" "chases" "tiger" "+")
triple4
The mouse sees the dog.
("mouse" "sees" "dog" "+")
triple5
The mouse sees the rabbit.
("mouse" "sees" "rabbit" "+")
triple6
The rabbit likes the dog.
("rabbit" "likes" "dog" "+")
triple7
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
triple8
The tiger is green.
("tiger" "is" "green" "+")
triple9
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
triple10
The dog chases the mouse.
("dog" "chases" "mouse" "+")
((triple2) -> (rule7 % int1))
The dog chases the mouse.
("dog" "chases" "mouse" "+")
int1
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
((triple5) -> (rule8 % int1))
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
int1
The mouse is green.
("mouse" "is" "green" "+")
((((triple2) -> (rule7 % int2))) -> (rule3 % int1))
The mouse is green.
("mouse" "is" "green" "+")
int1
The dog chases the mouse.
("dog" "chases" "mouse" "+")
int2
The rabbit is rough.
("rabbit" "is" "rough" "+")
((((triple2) -> (rule7 % int2)) triple6) -> (rule1 % int1))
The rabbit is rough.
("rabbit" "is" "rough" "+")
int1
The dog chases the mouse.
("dog" "chases" "mouse" "+")
int2
The mouse chases the dog.
("mouse" "chases" "dog" "+")
((((((triple2) -> (rule7 % int4))) -> (rule3 % int3)) ((triple5) -> (rule8 % int2))) -> (rule6 % int1))
The mouse chases the dog.
("mouse" "chases" "dog" "+")
int1
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
int2
The mouse is green.
("mouse" "is" "green" "+")
int3
The dog chases the mouse.
("dog" "chases" "mouse" "+")
int4
The rabbit is blue.
("rabbit" "is" "blue" "+")
((((((triple2) -> (rule7 % int3)) triple6) -> (rule1 % int2)) triple7) -> (rule2 % int1))
The rabbit is blue.
("rabbit" "is" "blue" "+")
int1
The rabbit is rough.
("rabbit" "is" "rough" "+")
int2
The dog chases the mouse.
("dog" "chases" "mouse" "+")
int3
The dog sees the mouse.
("dog" "sees" "mouse" "+")
((((((((triple2) -> (rule7 % int5))) -> (rule3 % int4)) ((triple5) -> (rule8 % int3))) -> (rule6 % int2)) triple5) -> (rule4 % int1))
The dog sees the mouse.
("dog" "sees" "mouse" "+")
int1
The mouse chases the dog.
("mouse" "chases" "dog" "+")
int2
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
int3
The mouse is green.
("mouse" "is" "green" "+")
int4
The dog chases the mouse.
("dog" "chases" "mouse" "+")
int5
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
((triple8 ((((((triple2) -> (rule7 % int4)) triple6) -> (rule1 % int3)) triple7) -> (rule2 % int2))) -> (rule5 % int1))
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
int1
The rabbit is blue.
("rabbit" "is" "blue" "+")
int2
The rabbit is rough.
("rabbit" "is" "rough" "+")
int3
The dog chases the mouse.
("dog" "chases" "mouse" "+")
int4