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