The cat chases the mouse. The cat is rough. The cat likes the mouse. The cow chases the mouse. The cow chases the tiger. The cow is round. The cow likes the cat. The cow likes the mouse. The cow likes the tiger. The mouse likes the cow. The mouse likes the tiger. The mouse needs the cow. The tiger is red. The tiger is young. The tiger needs the cat. The tiger needs the cow. If someone needs the cat then the cat needs the cow. If someone is red then they chase the cat. If someone is young then they chase the mouse. If someone likes the mouse then the mouse is rough. If someone is young and they chase the tiger then the tiger likes the mouse. If someone is red then they need the cow. If someone likes the mouse and the mouse likes the cow then they need the cow. If someone needs the cow then they need the mouse.
The cat chases the mouse.
("cat" "chases" "mouse" "+")
The cat is rough.
("cat" "is" "rough" "+")
The cat likes the mouse.
("cat" "likes" "mouse" "+")
The cow chases the mouse.
("cow" "chases" "mouse" "+")
The cow chases the tiger.
("cow" "chases" "tiger" "+")
The cow is round.
("cow" "is" "round" "+")
The cow likes the cat.
("cow" "likes" "cat" "+")
The cow likes the mouse.
("cow" "likes" "mouse" "+")
The cow likes the tiger.
("cow" "likes" "tiger" "+")
The mouse likes the cow.
("mouse" "likes" "cow" "+")
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
The mouse needs the cow.
("mouse" "needs" "cow" "+")
The tiger is red.
("tiger" "is" "red" "+")
The tiger is young.
("tiger" "is" "young" "+")
The tiger needs the cat.
("tiger" "needs" "cat" "+")
The tiger needs the cow.
("tiger" "needs" "cow" "+")
If someone needs the cat then the cat needs the cow.
((("someone" "needs" "cat" "+")) -> ("cat" "needs" "cow" "+"))
If someone is red then they chase the cat.
((("someone" "is" "red" "+")) -> ("someone" "chases" "cat" "+"))
If someone is young then they chase the mouse.
((("someone" "is" "young" "+")) -> ("someone" "chases" "mouse" "+"))
If someone likes the mouse then the mouse is rough.
((("someone" "likes" "mouse" "+")) -> ("mouse" "is" "rough" "+"))
If someone is young and they chase the tiger then the tiger likes the mouse.
((("someone" "is" "young" "+") ("someone" "chases" "tiger" "+")) -> ("tiger" "likes" "mouse" "+"))
If someone is red then they need the cow.
((("someone" "is" "red" "+")) -> ("someone" "needs" "cow" "+"))
If someone likes the mouse and the mouse likes the cow then they need the cow.
((("someone" "likes" "mouse" "+") ("mouse" "likes" "cow" "+")) -> ("someone" "needs" "cow" "+"))
If someone needs the cow then they need the mouse.
((("someone" "needs" "cow" "+")) -> ("someone" "needs" "mouse" "+"))
The cat chases the mouse.
True
1
proof
[(triple1)]
("cat" "chases" "mouse" "+")
triple1
The tiger does not need the cat.
False
1
inv-proof
[(triple15)]
("tiger" "needs" "cat" "-")
triple15
The mouse needs the mouse.
True
2
proof
[(((triple12) -> rule8))]
("mouse" "needs" "mouse" "+")
((triple12) -> (rule8 % int1))
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int1
The tiger does not chase the cat.
False
2
inv-proof
[(((triple13) -> rule2))]
("tiger" "chases" "cat" "-")
((triple13) -> (rule2 % int1))
The tiger chases the cat.
("tiger" "chases" "cat" "+")
int1
The cat needs the mouse.
True
3
proof
[(((((triple15) -> rule1)) -> rule8) OR ((((triple3 triple10) -> rule7)) -> rule8))]
("cat" "needs" "mouse" "+")
((((triple15) -> (rule1 % int2))) -> (rule8 % int1))
The cat needs the mouse.
("cat" "needs" "mouse" "+")
int1
The cat needs the cow.
("cat" "needs" "cow" "+")
int2
((((triple3 triple10) -> (rule7 % int2))) -> (rule8 % int1))
The cat needs the mouse.
("cat" "needs" "mouse" "+")
int1
The cat needs the cow.
("cat" "needs" "cow" "+")
int2
The cow does not need the mouse.
False
4
inv-proof
[(((((triple8 triple10) -> rule7)) -> rule8))]
("cow" "needs" "mouse" "-")
((((triple8 triple10) -> (rule7 % int2))) -> (rule8 % int1))
The cow needs the mouse.
("cow" "needs" "mouse" "+")
int1
The cow needs the cow.
("cow" "needs" "cow" "+")
int2
The mouse does not chase the mouse.
Unknown
inv-rconc
[@1: The mouse chases the mouse.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("mouse" "chases" "mouse" "-")
The cat chases the cat.
Unknown
rconc
[@1: The cat chases the cat.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cat" "chases" "cat" "+")
The mouse does not chase the cat.
Unknown
inv-rconc
[@1: The mouse chases the cat.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("mouse" "chases" "cat" "-")
The cow needs the tiger.
Unknown
random
[@0: The cow needs the tiger.[CWA. Example of deepest failure = (FAIL)]]
("cow" "needs" "tiger" "+")
The cat does not chase the cow.
Unknown
inv-random
[@0: The cat chases the cow.[CWA. Example of deepest failure = (FAIL)]]
("cat" "chases" "cow" "-")
The cat chases the tiger.
Unknown
random
[@0: The cat chases the tiger.[CWA. Example of deepest failure = (FAIL)]]
("cat" "chases" "tiger" "+")
@0: The cat chases the mouse.[(triple1)] The cat is rough.[(triple2)] The cat likes the mouse.[(triple3)] The cow chases the mouse.[(triple4)] The cow chases the tiger.[(triple5)] The cow is round.[(triple6)] The cow likes the cat.[(triple7)] The cow likes the mouse.[(triple8)] The cow likes the tiger.[(triple9)] The mouse likes the cow.[(triple10)] The mouse likes the tiger.[(triple11)] The mouse needs the cow.[(triple12)] The tiger is red.[(triple13)] The tiger is young.[(triple14)] The tiger needs the cat.[(triple15)] The tiger needs the cow.[(triple16 OR ((triple13) -> rule6))] @1: The cat needs the cow.[(((triple15) -> rule1) OR ((triple3 triple10) -> rule7))] The cow needs the cow.[(((triple8 triple10) -> rule7))] The mouse is rough.[(((triple3) -> rule4) OR ((triple8) -> rule4))] The mouse needs the mouse.[(((triple12) -> rule8))] The tiger chases the cat.[(((triple13) -> rule2))] The tiger chases the mouse.[(((triple14) -> rule3))] The tiger needs the mouse.[(((triple16) -> rule8) OR ((((triple13) -> rule6)) -> rule8))] @2: The cat needs the mouse.[(((((triple15) -> rule1)) -> rule8) OR ((((triple3 triple10) -> rule7)) -> rule8))] The cow needs the mouse.[(((((triple8 triple10) -> rule7)) -> rule8))]
The cat chases the mouse.
("cat" "chases" "mouse" "+")
triple1
The cat is rough.
("cat" "is" "rough" "+")
triple2
The cat likes the mouse.
("cat" "likes" "mouse" "+")
triple3
The cow chases the mouse.
("cow" "chases" "mouse" "+")
triple4
The cow chases the tiger.
("cow" "chases" "tiger" "+")
triple5
The cow is round.
("cow" "is" "round" "+")
triple6
The cow likes the cat.
("cow" "likes" "cat" "+")
triple7
The cow likes the mouse.
("cow" "likes" "mouse" "+")
triple8
The cow likes the tiger.
("cow" "likes" "tiger" "+")
triple9
The mouse likes the cow.
("mouse" "likes" "cow" "+")
triple10
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
triple11
The mouse needs the cow.
("mouse" "needs" "cow" "+")
triple12
The tiger is red.
("tiger" "is" "red" "+")
triple13
The tiger is young.
("tiger" "is" "young" "+")
triple14
The tiger needs the cat.
("tiger" "needs" "cat" "+")
triple15
The tiger needs the cow.
("tiger" "needs" "cow" "+")
triple16
((triple13) -> (rule6 % int1))
The tiger needs the cow.
("tiger" "needs" "cow" "+")
int1
The cat needs the cow.
("cat" "needs" "cow" "+")
((triple15) -> (rule1 % int1))
The cat needs the cow.
("cat" "needs" "cow" "+")
int1
((triple3 triple10) -> (rule7 % int1))
The cat needs the cow.
("cat" "needs" "cow" "+")
int1
The cow needs the cow.
("cow" "needs" "cow" "+")
((triple8 triple10) -> (rule7 % int1))
The cow needs the cow.
("cow" "needs" "cow" "+")
int1
The mouse is rough.
("mouse" "is" "rough" "+")
((triple3) -> (rule4 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
((triple8) -> (rule4 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
((triple12) -> (rule8 % int1))
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int1
The tiger chases the cat.
("tiger" "chases" "cat" "+")
((triple13) -> (rule2 % int1))
The tiger chases the cat.
("tiger" "chases" "cat" "+")
int1
The tiger chases the mouse.
("tiger" "chases" "mouse" "+")
((triple14) -> (rule3 % int1))
The tiger chases the mouse.
("tiger" "chases" "mouse" "+")
int1
The tiger needs the mouse.
("tiger" "needs" "mouse" "+")
((triple16) -> (rule8 % int1))
The tiger needs the mouse.
("tiger" "needs" "mouse" "+")
int1
((((triple13) -> (rule6 % int2))) -> (rule8 % int1))
The tiger needs the mouse.
("tiger" "needs" "mouse" "+")
int1
The tiger needs the cow.
("tiger" "needs" "cow" "+")
int2
The cat needs the mouse.
("cat" "needs" "mouse" "+")
((((triple15) -> (rule1 % int2))) -> (rule8 % int1))
The cat needs the mouse.
("cat" "needs" "mouse" "+")
int1
The cat needs the cow.
("cat" "needs" "cow" "+")
int2
((((triple3 triple10) -> (rule7 % int2))) -> (rule8 % int1))
The cat needs the mouse.
("cat" "needs" "mouse" "+")
int1
The cat needs the cow.
("cat" "needs" "cow" "+")
int2
The cow needs the mouse.
("cow" "needs" "mouse" "+")
((((triple8 triple10) -> (rule7 % int2))) -> (rule8 % int1))
The cow needs the mouse.
("cow" "needs" "mouse" "+")
int1
The cow needs the cow.
("cow" "needs" "cow" "+")
int2