The cat likes the rabbit. The cow is kind. The mouse likes the rabbit. The mouse visits the cat. The rabbit is kind. The rabbit likes the cat. The rabbit sees the cow. If something likes the rabbit and it is big then it visits the mouse. If something is nice then it visits the mouse. If the cat visits the cow then the cat is not big. If something is green then it sees the cow. If the cow does not visit the rabbit and the rabbit is not kind then the rabbit is cold. If something likes the cat then the cat is nice. If the rabbit likes the mouse and the rabbit does not like the cat then the cat is nice. If something sees the mouse then it is not cold.
The cat likes the rabbit.
("cat" "likes" "rabbit" "+")
The cow is kind.
("cow" "is" "kind" "+")
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
The mouse visits the cat.
("mouse" "visits" "cat" "+")
The rabbit is kind.
("rabbit" "is" "kind" "+")
The rabbit likes the cat.
("rabbit" "likes" "cat" "+")
The rabbit sees the cow.
("rabbit" "sees" "cow" "+")
If something likes the rabbit and it is big then it visits the mouse.
((("something" "likes" "rabbit" "+") ("something" "is" "big" "+")) -> ("something" "visits" "mouse" "+"))
If something is nice then it visits the mouse.
((("something" "is" "nice" "+")) -> ("something" "visits" "mouse" "+"))
If the cat visits the cow then the cat is not big.
((("cat" "visits" "cow" "+")) -> ("cat" "is" "big" "-"))
If something is green then it sees the cow.
((("something" "is" "green" "+")) -> ("something" "sees" "cow" "+"))
If the cow does not visit the rabbit and the rabbit is not kind then the rabbit is cold.
((("cow" "visits" "rabbit" "~") ("rabbit" "is" "kind" "~")) -> ("rabbit" "is" "cold" "+"))
If something likes the cat then the cat is nice.
((("something" "likes" "cat" "+")) -> ("cat" "is" "nice" "+"))
If the rabbit likes the mouse and the rabbit does not like the cat then the cat is nice.
((("rabbit" "likes" "mouse" "+") ("rabbit" "likes" "cat" "~")) -> ("cat" "is" "nice" "+"))
If something sees the mouse then it is not cold.
((("something" "sees" "mouse" "+")) -> ("something" "is" "cold" "-"))
The mouse likes the rabbit.
True
1
proof
[(triple3)]
("mouse" "likes" "rabbit" "+")
triple3
The rabbit does not like the cat.
False
1
inv-proof
[(triple6)]
("rabbit" "likes" "cat" "-")
triple6
The cat is nice.
True
2
proof
[(((triple6) -> rule6))]
("cat" "is" "nice" "+")
((triple6) -> (rule6 % int1))
The cat is nice.
("cat" "is" "nice" "+")
int1
The cat is not nice.
False
2
inv-proof
[(((triple6) -> rule6))]
("cat" "is" "nice" "-")
((triple6) -> (rule6 % int1))
The cat is nice.
("cat" "is" "nice" "+")
int1
The mouse does not visit the mouse.
Unknown
inv-rconc
[@1: The mouse visits the mouse.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("mouse" "visits" "mouse" "-")
The rabbit is cold.
Unknown
rconc
[@1: The rabbit is cold.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("rabbit" "is" "cold" "+")
The cow does not like the mouse.
Unknown
inv-random
[@0: The cow likes the mouse.[CWA. Example of deepest failure = (FAIL)]]
("cow" "likes" "mouse" "-")
The mouse is cold.
Unknown
random
[@0: The mouse is cold.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "cold" "+")
@0: The cat likes the rabbit.[(triple1)] The cow is kind.[(triple2)] The mouse likes the rabbit.[(triple3)] The mouse visits the cat.[(triple4)] The rabbit is kind.[(triple5)] The rabbit likes the cat.[(triple6)] The rabbit sees the cow.[(triple7)] @1: The cat is nice.[(((triple6) -> rule6))] @2: The cat visits the mouse.[(((((triple6) -> rule6)) -> rule2))]
The cat likes the rabbit.
("cat" "likes" "rabbit" "+")
triple1
The cow is kind.
("cow" "is" "kind" "+")
triple2
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
triple3
The mouse visits the cat.
("mouse" "visits" "cat" "+")
triple4
The rabbit is kind.
("rabbit" "is" "kind" "+")
triple5
The rabbit likes the cat.
("rabbit" "likes" "cat" "+")
triple6
The rabbit sees the cow.
("rabbit" "sees" "cow" "+")
triple7
The cat is nice.
("cat" "is" "nice" "+")
((triple6) -> (rule6 % int1))
The cat is nice.
("cat" "is" "nice" "+")
int1
The cat visits the mouse.
("cat" "visits" "mouse" "+")
((((triple6) -> (rule6 % int2))) -> (rule2 % int1))
The cat visits the mouse.
("cat" "visits" "mouse" "+")
int1
The cat is nice.
("cat" "is" "nice" "+")
int2