The cat chases the dog. The cat chases the mouse. The cat eats the dog. The cat eats the mouse. The cat is big. The cat is nice. The cat is round. The cat visits the dog. The cat visits the mouse. The dog visits the cat. The mouse chases the dog. The mouse eats the cat. The mouse eats the dog. The mouse visits the cat. The mouse visits the dog. If someone visits the cat then the cat is rough. If someone is round and nice then they eat the cat. If someone visits the dog and they visit the cat then the dog visits the mouse. If someone eats the cat and the cat eats the mouse then they chase the mouse. If someone visits the mouse then they are rough. If someone is rough and they visit the cat then they visit the dog.
The cat chases the dog.
("cat" "chases" "dog" "+")
The cat chases the mouse.
("cat" "chases" "mouse" "+")
The cat eats the dog.
("cat" "eats" "dog" "+")
The cat eats the mouse.
("cat" "eats" "mouse" "+")
The cat is big.
("cat" "is" "big" "+")
The cat is nice.
("cat" "is" "nice" "+")
The cat is round.
("cat" "is" "round" "+")
The cat visits the dog.
("cat" "visits" "dog" "+")
The cat visits the mouse.
("cat" "visits" "mouse" "+")
The dog visits the cat.
("dog" "visits" "cat" "+")
The mouse chases the dog.
("mouse" "chases" "dog" "+")
The mouse eats the cat.
("mouse" "eats" "cat" "+")
The mouse eats the dog.
("mouse" "eats" "dog" "+")
The mouse visits the cat.
("mouse" "visits" "cat" "+")
The mouse visits the dog.
("mouse" "visits" "dog" "+")
If someone visits the cat then the cat is rough.
((("someone" "visits" "cat" "+")) -> ("cat" "is" "rough" "+"))
If someone is round and nice then they eat the cat.
((("someone" "is" "round" "+") ("someone" "is" "nice" "+")) -> ("someone" "eats" "cat" "+"))
If someone visits the dog and they visit the cat then the dog visits the mouse.
((("someone" "visits" "dog" "+") ("someone" "visits" "cat" "+")) -> ("dog" "visits" "mouse" "+"))
If someone eats the cat and the cat eats the mouse then they chase the mouse.
((("someone" "eats" "cat" "+") ("cat" "eats" "mouse" "+")) -> ("someone" "chases" "mouse" "+"))
If someone visits the mouse then they are rough.
((("someone" "visits" "mouse" "+")) -> ("someone" "is" "rough" "+"))
If someone is rough and they visit the cat then they visit the dog.
((("someone" "is" "rough" "+") ("someone" "visits" "cat" "+")) -> ("someone" "visits" "dog" "+"))
The cat chases the dog.
True
1
proof
[(triple1)]
("cat" "chases" "dog" "+")
triple1
The mouse does not eat the dog.
False
1
inv-proof
[(triple13)]
("mouse" "eats" "dog" "-")
triple13
The dog visits the mouse.
True
3
proof
[(((triple15 triple14) -> rule3))]
("dog" "visits" "mouse" "+")
((triple15 triple14) -> (rule3 % int1))
The dog visits the mouse.
("dog" "visits" "mouse" "+")
int1
The dog does not visit the mouse.
False
3
inv-proof
[(((triple15 triple14) -> rule3))]
("dog" "visits" "mouse" "-")
((triple15 triple14) -> (rule3 % int1))
The dog visits the mouse.
("dog" "visits" "mouse" "+")
int1
The dog is rough.
True
4
proof
[(((((triple15 triple14) -> rule3)) -> rule5))]
("dog" "is" "rough" "+")
((((triple15 triple14) -> (rule3 % int2))) -> (rule5 % int1))
The dog is rough.
("dog" "is" "rough" "+")
int1
The dog visits the mouse.
("dog" "visits" "mouse" "+")
int2
The dog is not rough.
False
4
inv-proof
[(((((triple15 triple14) -> rule3)) -> rule5))]
("dog" "is" "rough" "-")
((((triple15 triple14) -> (rule3 % int2))) -> (rule5 % int1))
The dog is rough.
("dog" "is" "rough" "+")
int1
The dog visits the mouse.
("dog" "visits" "mouse" "+")
int2
The dog visits the dog.
True
6
proof
[(((((((triple15 triple14) -> rule3)) -> rule5) triple10) -> rule6))]
("dog" "visits" "dog" "+")
((((((triple15 triple14) -> (rule3 % int3))) -> (rule5 % int2)) triple10) -> (rule6 % int1))
The dog visits the dog.
("dog" "visits" "dog" "+")
int1
The dog is rough.
("dog" "is" "rough" "+")
int2
The dog visits the mouse.
("dog" "visits" "mouse" "+")
int3
The dog does not visit the dog.
False
6
inv-proof
[(((((((triple15 triple14) -> rule3)) -> rule5) triple10) -> rule6))]
("dog" "visits" "dog" "-")
((((((triple15 triple14) -> (rule3 % int3))) -> (rule5 % int2)) triple10) -> (rule6 % int1))
The dog visits the dog.
("dog" "visits" "dog" "+")
int1
The dog is rough.
("dog" "is" "rough" "+")
int2
The dog visits the mouse.
("dog" "visits" "mouse" "+")
int3
The dog does not eat the cat.
Unknown
inv-rconc
[@1: The dog eats the cat.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("dog" "eats" "cat" "-")
The dog chases the mouse.
Unknown
rconc
[@2: The dog chases the mouse.[CWA. Example of deepest failure = (rule4 <- rule2 <- FAIL)]]
("dog" "chases" "mouse" "+")
The mouse is not rough.
Unknown
inv-rconc
[@1: The mouse is rough.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("mouse" "is" "rough" "-")
The cat chases the cat.
Unknown
random
[@0: The cat chases the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "chases" "cat" "+")
The mouse is not blue.
Unknown
inv-random
[@0: The mouse is blue.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "blue" "-")
The mouse visits the mouse.
Unknown
random
[@0: The mouse visits the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "visits" "mouse" "+")
The mouse is not round.
Unknown
inv-random
[@0: The mouse is round.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "round" "-")
The dog is blue.
Unknown
random
[@0: The dog is blue.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "blue" "+")
@0: The cat chases the dog.[(triple1)] The cat chases the mouse.[(triple2 OR ((((triple7 triple6) -> rule2) triple4) -> rule4))] The cat eats the dog.[(triple3)] The cat eats the mouse.[(triple4)] The cat is big.[(triple5)] The cat is nice.[(triple6)] The cat is round.[(triple7)] The cat visits the dog.[(triple8)] The cat visits the mouse.[(triple9)] The dog visits the cat.[(triple10)] The mouse chases the dog.[(triple11)] The mouse eats the cat.[(triple12)] The mouse eats the dog.[(triple13)] The mouse visits the cat.[(triple14)] The mouse visits the dog.[(triple15)] @1: The cat eats the cat.[(((triple7 triple6) -> rule2))] The cat is rough.[(((triple10) -> rule1) OR ((triple14) -> rule1) OR ((triple9) -> rule5))] The dog visits the mouse.[(((triple15 triple14) -> rule3))] The mouse chases the mouse.[(((triple12 triple4) -> rule4))] @2: The dog is rough.[(((((triple15 triple14) -> rule3)) -> rule5))] @3: The dog visits the dog.[(((((((triple15 triple14) -> rule3)) -> rule5) triple10) -> rule6))]
The cat chases the dog.
("cat" "chases" "dog" "+")
triple1
The cat chases the mouse.
("cat" "chases" "mouse" "+")
triple2
((((triple7 triple6) -> (rule2 % int2)) triple4) -> (rule4 % int1))
The cat chases the mouse.
("cat" "chases" "mouse" "+")
int1
The cat eats the cat.
("cat" "eats" "cat" "+")
int2
The cat eats the dog.
("cat" "eats" "dog" "+")
triple3
The cat eats the mouse.
("cat" "eats" "mouse" "+")
triple4
The cat is big.
("cat" "is" "big" "+")
triple5
The cat is nice.
("cat" "is" "nice" "+")
triple6
The cat is round.
("cat" "is" "round" "+")
triple7
The cat visits the dog.
("cat" "visits" "dog" "+")
triple8
The cat visits the mouse.
("cat" "visits" "mouse" "+")
triple9
The dog visits the cat.
("dog" "visits" "cat" "+")
triple10
The mouse chases the dog.
("mouse" "chases" "dog" "+")
triple11
The mouse eats the cat.
("mouse" "eats" "cat" "+")
triple12
The mouse eats the dog.
("mouse" "eats" "dog" "+")
triple13
The mouse visits the cat.
("mouse" "visits" "cat" "+")
triple14
The mouse visits the dog.
("mouse" "visits" "dog" "+")
triple15
The cat eats the cat.
("cat" "eats" "cat" "+")
((triple7 triple6) -> (rule2 % int1))
The cat eats the cat.
("cat" "eats" "cat" "+")
int1
The cat is rough.
("cat" "is" "rough" "+")
((triple10) -> (rule1 % int1))
The cat is rough.
("cat" "is" "rough" "+")
int1
((triple14) -> (rule1 % int1))
The cat is rough.
("cat" "is" "rough" "+")
int1
((triple9) -> (rule5 % int1))
The cat is rough.
("cat" "is" "rough" "+")
int1
The dog visits the mouse.
("dog" "visits" "mouse" "+")
((triple15 triple14) -> (rule3 % int1))
The dog visits the mouse.
("dog" "visits" "mouse" "+")
int1
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
((triple12 triple4) -> (rule4 % int1))
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int1
The dog is rough.
("dog" "is" "rough" "+")
((((triple15 triple14) -> (rule3 % int2))) -> (rule5 % int1))
The dog is rough.
("dog" "is" "rough" "+")
int1
The dog visits the mouse.
("dog" "visits" "mouse" "+")
int2
The dog visits the dog.
("dog" "visits" "dog" "+")
((((((triple15 triple14) -> (rule3 % int3))) -> (rule5 % int2)) triple10) -> (rule6 % int1))
The dog visits the dog.
("dog" "visits" "dog" "+")
int1
The dog is rough.
("dog" "is" "rough" "+")
int2
The dog visits the mouse.
("dog" "visits" "mouse" "+")
int3