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