The cow is cold. The cow is young. The cow likes the mouse. The cow visits the mouse. The mouse is red. The mouse visits the tiger. The tiger likes the cow. The tiger likes the mouse. The tiger sees the cow. The tiger sees the mouse. If the cow sees the mouse then the mouse visits the tiger. If someone is red and they like the cow then the cow likes the mouse. If someone sees the mouse and they are round then they are young. If someone is cold then they like the mouse. If someone is young then they visit the tiger. If someone likes the cow then the cow is round.
The cow is cold.
("cow" "is" "cold" "+")
The cow is young.
("cow" "is" "young" "+")
The cow likes the mouse.
("cow" "likes" "mouse" "+")
The cow visits the mouse.
("cow" "visits" "mouse" "+")
The mouse is red.
("mouse" "is" "red" "+")
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
The tiger likes the cow.
("tiger" "likes" "cow" "+")
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
The tiger sees the cow.
("tiger" "sees" "cow" "+")
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
If the cow sees the mouse then the mouse visits the tiger.
((("cow" "sees" "mouse" "+")) -> ("mouse" "visits" "tiger" "+"))
If someone is red and they like the cow then the cow likes the mouse.
((("someone" "is" "red" "+") ("someone" "likes" "cow" "+")) -> ("cow" "likes" "mouse" "+"))
If someone sees the mouse and they are round then they are young.
((("someone" "sees" "mouse" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "young" "+"))
If someone is cold then they like the mouse.
((("someone" "is" "cold" "+")) -> ("someone" "likes" "mouse" "+"))
If someone is young then they visit the tiger.
((("someone" "is" "young" "+")) -> ("someone" "visits" "tiger" "+"))
If someone likes the cow then the cow is round.
((("someone" "likes" "cow" "+")) -> ("cow" "is" "round" "+"))
The tiger sees the mouse.
True
1
proof
[(triple10)]
("tiger" "sees" "mouse" "+")
triple10
The mouse is not red.
False
1
inv-proof
[(triple5)]
("mouse" "is" "red" "-")
triple5
The cow is round.
True
2
proof
[(((triple7) -> rule6))]
("cow" "is" "round" "+")
((triple7) -> (rule6 % int1))
The cow is round.
("cow" "is" "round" "+")
int1
The cow does not visit the tiger.
False
2
inv-proof
[(((triple2) -> rule5))]
("cow" "visits" "tiger" "-")
((triple2) -> (rule5 % int1))
The cow visits the tiger.
("cow" "visits" "tiger" "+")
int1
The mouse does not like the mouse.
Unknown
inv-rconc
[@1: The mouse likes the mouse.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("mouse" "likes" "mouse" "-")
The tiger visits the tiger.
Unknown
rconc
[@2: The tiger visits the tiger.[CWA. Example of deepest failure = (rule5 <- rule3 <- FAIL)]]
("tiger" "visits" "tiger" "+")
The tiger does not see the tiger.
Unknown
inv-random
[@0: The tiger sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "tiger" "-")
The mouse visits the cow.
Unknown
random
[@0: The mouse visits the cow.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "visits" "cow" "+")
@0: The cow is cold.[(triple1)] The cow is young.[(triple2)] The cow likes the mouse.[(triple3 OR ((triple1) -> rule4))] The cow visits the mouse.[(triple4)] The mouse is red.[(triple5)] The mouse visits the tiger.[(triple6)] The tiger likes the cow.[(triple7)] The tiger likes the mouse.[(triple8)] The tiger sees the cow.[(triple9)] The tiger sees the mouse.[(triple10)] @1: The cow is round.[(((triple7) -> rule6))] The cow visits the tiger.[(((triple2) -> rule5))]
The cow is cold.
("cow" "is" "cold" "+")
triple1
The cow is young.
("cow" "is" "young" "+")
triple2
The cow likes the mouse.
("cow" "likes" "mouse" "+")
triple3
((triple1) -> (rule4 % int1))
The cow likes the mouse.
("cow" "likes" "mouse" "+")
int1
The cow visits the mouse.
("cow" "visits" "mouse" "+")
triple4
The mouse is red.
("mouse" "is" "red" "+")
triple5
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
triple6
The tiger likes the cow.
("tiger" "likes" "cow" "+")
triple7
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
triple8
The tiger sees the cow.
("tiger" "sees" "cow" "+")
triple9
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
triple10
The cow is round.
("cow" "is" "round" "+")
((triple7) -> (rule6 % int1))
The cow is round.
("cow" "is" "round" "+")
int1
The cow visits the tiger.
("cow" "visits" "tiger" "+")
((triple2) -> (rule5 % int1))
The cow visits the tiger.
("cow" "visits" "tiger" "+")
int1