The cat chases the rabbit. The cat likes the rabbit. The mouse chases the tiger. The mouse is nice. The mouse is young. The mouse likes the cat. The rabbit is cold. The rabbit is nice. The rabbit visits the mouse. The tiger chases the cat. The tiger is big. The tiger is cold. If something visits the mouse then the mouse chases the rabbit. If something is cold then it likes the cat. If the tiger chases the mouse then the mouse chases the tiger. If something likes the cat then it is kind. If something is kind and it likes the rabbit then it visits the cat. If something chases the rabbit and it likes the mouse then the rabbit is nice.
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
The cat likes the rabbit.
("cat" "likes" "rabbit" "+")
The mouse chases the tiger.
("mouse" "chases" "tiger" "+")
The mouse is nice.
("mouse" "is" "nice" "+")
The mouse is young.
("mouse" "is" "young" "+")
The mouse likes the cat.
("mouse" "likes" "cat" "+")
The rabbit is cold.
("rabbit" "is" "cold" "+")
The rabbit is nice.
("rabbit" "is" "nice" "+")
The rabbit visits the mouse.
("rabbit" "visits" "mouse" "+")
The tiger chases the cat.
("tiger" "chases" "cat" "+")
The tiger is big.
("tiger" "is" "big" "+")
The tiger is cold.
("tiger" "is" "cold" "+")
If something visits the mouse then the mouse chases the rabbit.
((("something" "visits" "mouse" "+")) -> ("mouse" "chases" "rabbit" "+"))
If something is cold then it likes the cat.
((("something" "is" "cold" "+")) -> ("something" "likes" "cat" "+"))
If the tiger chases the mouse then the mouse chases the tiger.
((("tiger" "chases" "mouse" "+")) -> ("mouse" "chases" "tiger" "+"))
If something likes the cat then it is kind.
((("something" "likes" "cat" "+")) -> ("something" "is" "kind" "+"))
If something is kind and it likes the rabbit then it visits the cat.
((("something" "is" "kind" "+") ("something" "likes" "rabbit" "+")) -> ("something" "visits" "cat" "+"))
If something chases the rabbit and it likes the mouse then the rabbit is nice.
((("something" "chases" "rabbit" "+") ("something" "likes" "mouse" "+")) -> ("rabbit" "is" "nice" "+"))
The mouse chases the tiger.
True
1
proof
[(triple3)]
("mouse" "chases" "tiger" "+")
triple3
The rabbit does not visit the mouse.
False
1
inv-proof
[(triple9)]
("rabbit" "visits" "mouse" "-")
triple9
The tiger likes the cat.
True
2
proof
[(((triple12) -> rule2))]
("tiger" "likes" "cat" "+")
((triple12) -> (rule2 % int1))
The tiger likes the cat.
("tiger" "likes" "cat" "+")
int1
The mouse does not chase the rabbit.
False
2
inv-proof
[(((triple9) -> rule1))]
("mouse" "chases" "rabbit" "-")
((triple9) -> (rule1 % int1))
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
int1
The cat does not visit the cat.
Unknown
inv-rconc
[@3: The cat visits the cat.[CWA. Example of deepest failure = (rule5 <- rule4 <- rule2 <- FAIL)]]
("cat" "visits" "cat" "-")
The tiger visits the cat.
Unknown
rconc
[@1: The tiger visits the cat.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("tiger" "visits" "cat" "+")
The cat does not visit the tiger.
Unknown
inv-random
[@0: The cat visits the tiger.[CWA. Example of deepest failure = (FAIL)]]
("cat" "visits" "tiger" "-")
The tiger likes the mouse.
Unknown
random
[@0: The tiger likes the mouse.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "likes" "mouse" "+")
@0: The cat chases the rabbit.[(triple1)] The cat likes the rabbit.[(triple2)] The mouse chases the tiger.[(triple3)] The mouse is nice.[(triple4)] The mouse is young.[(triple5)] The mouse likes the cat.[(triple6)] The rabbit is cold.[(triple7)] The rabbit is nice.[(triple8)] The rabbit visits the mouse.[(triple9)] The tiger chases the cat.[(triple10)] The tiger is big.[(triple11)] The tiger is cold.[(triple12)] @1: The mouse chases the rabbit.[(((triple9) -> rule1))] The mouse is kind.[(((triple6) -> rule4))] The rabbit likes the cat.[(((triple7) -> rule2))] The tiger likes the cat.[(((triple12) -> rule2))] @2: The rabbit is kind.[(((((triple7) -> rule2)) -> rule4))] The tiger is kind.[(((((triple12) -> rule2)) -> rule4))]
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
triple1
The cat likes the rabbit.
("cat" "likes" "rabbit" "+")
triple2
The mouse chases the tiger.
("mouse" "chases" "tiger" "+")
triple3
The mouse is nice.
("mouse" "is" "nice" "+")
triple4
The mouse is young.
("mouse" "is" "young" "+")
triple5
The mouse likes the cat.
("mouse" "likes" "cat" "+")
triple6
The rabbit is cold.
("rabbit" "is" "cold" "+")
triple7
The rabbit is nice.
("rabbit" "is" "nice" "+")
triple8
The rabbit visits the mouse.
("rabbit" "visits" "mouse" "+")
triple9
The tiger chases the cat.
("tiger" "chases" "cat" "+")
triple10
The tiger is big.
("tiger" "is" "big" "+")
triple11
The tiger is cold.
("tiger" "is" "cold" "+")
triple12
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
((triple9) -> (rule1 % int1))
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
int1
The mouse is kind.
("mouse" "is" "kind" "+")
((triple6) -> (rule4 % int1))
The mouse is kind.
("mouse" "is" "kind" "+")
int1
The rabbit likes the cat.
("rabbit" "likes" "cat" "+")
((triple7) -> (rule2 % int1))
The rabbit likes the cat.
("rabbit" "likes" "cat" "+")
int1
The tiger likes the cat.
("tiger" "likes" "cat" "+")
((triple12) -> (rule2 % int1))
The tiger likes the cat.
("tiger" "likes" "cat" "+")
int1
The rabbit is kind.
("rabbit" "is" "kind" "+")
((((triple7) -> (rule2 % int2))) -> (rule4 % int1))
The rabbit is kind.
("rabbit" "is" "kind" "+")
int1
The rabbit likes the cat.
("rabbit" "likes" "cat" "+")
int2
The tiger is kind.
("tiger" "is" "kind" "+")
((((triple12) -> (rule2 % int2))) -> (rule4 % int1))
The tiger is kind.
("tiger" "is" "kind" "+")
int1
The tiger likes the cat.
("tiger" "likes" "cat" "+")
int2