The cat eats the mouse. The cat is blue. The cat is cold. The cat is red. The cat is round. The cat likes the mouse. The cat sees the mouse. The mouse eats the cat. The mouse is blue. The mouse is cold. The mouse is green. The mouse is red. The mouse is round. The mouse likes the cat. The mouse sees the cat. If someone likes the cat and they like the mouse then they eat the cat. If someone likes the cat then the cat sees the mouse. If someone is green and cold then they like the cat.
The cat eats the mouse.
("cat" "eats" "mouse" "+")
The cat is blue.
("cat" "is" "blue" "+")
The cat is cold.
("cat" "is" "cold" "+")
The cat is red.
("cat" "is" "red" "+")
The cat is round.
("cat" "is" "round" "+")
The cat likes the mouse.
("cat" "likes" "mouse" "+")
The cat sees the mouse.
("cat" "sees" "mouse" "+")
The mouse eats the cat.
("mouse" "eats" "cat" "+")
The mouse is blue.
("mouse" "is" "blue" "+")
The mouse is cold.
("mouse" "is" "cold" "+")
The mouse is green.
("mouse" "is" "green" "+")
The mouse is red.
("mouse" "is" "red" "+")
The mouse is round.
("mouse" "is" "round" "+")
The mouse likes the cat.
("mouse" "likes" "cat" "+")
The mouse sees the cat.
("mouse" "sees" "cat" "+")
If someone likes the cat and they like the mouse then they eat the cat.
((("someone" "likes" "cat" "+") ("someone" "likes" "mouse" "+")) -> ("someone" "eats" "cat" "+"))
If someone likes the cat then the cat sees the mouse.
((("someone" "likes" "cat" "+")) -> ("cat" "sees" "mouse" "+"))
If someone is green and cold then they like the cat.
((("someone" "is" "green" "+") ("someone" "is" "cold" "+")) -> ("someone" "likes" "cat" "+"))
The mouse likes the cat.
True
1
proof
[(triple14 OR ((triple11 triple10) -> rule3))]
("mouse" "likes" "cat" "+")
triple14
((triple11 triple10) -> (rule3 % int1))
The mouse likes the cat.
("mouse" "likes" "cat" "+")
int1
The mouse is not round.
False
1
inv-proof
[(triple13)]
("mouse" "is" "round" "-")
triple13
The cat does not like the cat.
Unknown
inv-rconc
[@1: The cat likes the cat.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cat" "likes" "cat" "-")
The mouse sees the mouse.
Unknown
random
[@0: The mouse sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "sees" "mouse" "+")
@0: The cat eats the mouse.[(triple1)] The cat is blue.[(triple2)] The cat is cold.[(triple3)] The cat is red.[(triple4)] The cat is round.[(triple5)] The cat likes the mouse.[(triple6)] The cat sees the mouse.[(triple7 OR ((triple14) -> rule2) OR ((((triple11 triple10) -> rule3)) -> rule2))] The mouse eats the cat.[(triple8)] The mouse is blue.[(triple9)] The mouse is cold.[(triple10)] The mouse is green.[(triple11)] The mouse is red.[(triple12)] The mouse is round.[(triple13)] The mouse likes the cat.[(triple14 OR ((triple11 triple10) -> rule3))] The mouse sees the cat.[(triple15)]
The cat eats the mouse.
("cat" "eats" "mouse" "+")
triple1
The cat is blue.
("cat" "is" "blue" "+")
triple2
The cat is cold.
("cat" "is" "cold" "+")
triple3
The cat is red.
("cat" "is" "red" "+")
triple4
The cat is round.
("cat" "is" "round" "+")
triple5
The cat likes the mouse.
("cat" "likes" "mouse" "+")
triple6
The cat sees the mouse.
("cat" "sees" "mouse" "+")
triple7
((triple14) -> (rule2 % int1))
The cat sees the mouse.
("cat" "sees" "mouse" "+")
int1
((((triple11 triple10) -> (rule3 % int2))) -> (rule2 % int1))
The cat sees the mouse.
("cat" "sees" "mouse" "+")
int1
The mouse likes the cat.
("mouse" "likes" "cat" "+")
int2
The mouse eats the cat.
("mouse" "eats" "cat" "+")
triple8
The mouse is blue.
("mouse" "is" "blue" "+")
triple9
The mouse is cold.
("mouse" "is" "cold" "+")
triple10
The mouse is green.
("mouse" "is" "green" "+")
triple11
The mouse is red.
("mouse" "is" "red" "+")
triple12
The mouse is round.
("mouse" "is" "round" "+")
triple13
The mouse likes the cat.
("mouse" "likes" "cat" "+")
triple14
((triple11 triple10) -> (rule3 % int1))
The mouse likes the cat.
("mouse" "likes" "cat" "+")
int1
The mouse sees the cat.
("mouse" "sees" "cat" "+")
triple15