The cat is blue. The cat visits the dog. The dog does not eat the lion. The dog eats the mouse. The dog is not big. The dog is red. The dog visits the mouse. The lion eats the mouse. The lion is blue. The lion is nice. The lion visits the cat. The lion visits the dog. The mouse chases the lion. The mouse is young. The mouse visits the dog. Blue, red things are young. If something eats the lion then it is not blue. If something is blue then it chases the lion. If something eats the mouse and it eats the lion then the mouse visits the dog. If something chases the mouse and it is not young then it visits the cat. If something chases the dog then it is nice. If something chases the lion then it chases the dog. If something eats the dog and it does not visit the cat then the dog chases the lion.
The cat is blue.
("cat" "is" "blue" "+")
The cat visits the dog.
("cat" "visits" "dog" "+")
The dog does not eat the lion.
("dog" "eats" "lion" "-")
The dog eats the mouse.
("dog" "eats" "mouse" "+")
The dog is not big.
("dog" "is" "big" "-")
The dog is red.
("dog" "is" "red" "+")
The dog visits the mouse.
("dog" "visits" "mouse" "+")
The lion eats the mouse.
("lion" "eats" "mouse" "+")
The lion is blue.
("lion" "is" "blue" "+")
The lion is nice.
("lion" "is" "nice" "+")
The lion visits the cat.
("lion" "visits" "cat" "+")
The lion visits the dog.
("lion" "visits" "dog" "+")
The mouse chases the lion.
("mouse" "chases" "lion" "+")
The mouse is young.
("mouse" "is" "young" "+")
The mouse visits the dog.
("mouse" "visits" "dog" "+")
Blue, red things are young.
((("something" "is" "blue" "+") ("something" "is" "red" "+")) -> ("something" "is" "young" "+"))
If something eats the lion then it is not blue.
((("something" "eats" "lion" "+")) -> ("something" "is" "blue" "-"))
If something is blue then it chases the lion.
((("something" "is" "blue" "+")) -> ("something" "chases" "lion" "+"))
If something eats the mouse and it eats the lion then the mouse visits the dog.
((("something" "eats" "mouse" "+") ("something" "eats" "lion" "+")) -> ("mouse" "visits" "dog" "+"))
If something chases the mouse and it is not young then it visits the cat.
((("something" "chases" "mouse" "+") ("something" "is" "young" "~")) -> ("something" "visits" "cat" "+"))
If something chases the dog then it is nice.
((("something" "chases" "dog" "+")) -> ("something" "is" "nice" "+"))
If something chases the lion then it chases the dog.
((("something" "chases" "lion" "+")) -> ("something" "chases" "dog" "+"))
If something eats the dog and it does not visit the cat then the dog chases the lion.
((("something" "eats" "dog" "+") ("something" "visits" "cat" "~")) -> ("dog" "chases" "lion" "+"))
The cat visits the dog.
True
1
proof
[(triple2)]
("cat" "visits" "dog" "+")
triple2
The dog does not eat the mouse.
False
1
inv-proof
[(triple4)]
("dog" "eats" "mouse" "-")
triple4
The lion chases the lion.
True
2
proof
[(((triple9) -> rule3))]
("lion" "chases" "lion" "+")
((triple9) -> (rule3 % int1))
The lion chases the lion.
("lion" "chases" "lion" "+")
int1
The mouse does not chase the dog.
False
2
inv-proof
[(((triple13) -> rule7))]
("mouse" "chases" "dog" "-")
((triple13) -> (rule7 % int1))
The mouse chases the dog.
("mouse" "chases" "dog" "+")
int1
The lion chases the dog.
True
3
proof
[(((((triple9) -> rule3)) -> rule7))]
("lion" "chases" "dog" "+")
((((triple9) -> (rule3 % int2))) -> (rule7 % int1))
The lion chases the dog.
("lion" "chases" "dog" "+")
int1
The lion chases the lion.
("lion" "chases" "lion" "+")
int2
The lion does not chase the dog.
False
3
inv-proof
[(((((triple9) -> rule3)) -> rule7))]
("lion" "chases" "dog" "-")
((((triple9) -> (rule3 % int2))) -> (rule7 % int1))
The lion chases the dog.
("lion" "chases" "dog" "+")
int1
The lion chases the lion.
("lion" "chases" "lion" "+")
int2
The dog is not nice.
Unknown
inv-rconc
[@3: The dog is nice.[CWA. Example of deepest failure = (rule6 <- rule7 <- rule3 <- FAIL)]]
("dog" "is" "nice" "-")
The dog visits the cat.
Unknown
rconc
[@1: The dog visits the cat.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("dog" "visits" "cat" "+")
The dog does not chase the dog.
Unknown
inv-rconc
[@2: The dog chases the dog.[CWA. Example of deepest failure = (rule7 <- rule3 <- FAIL)]]
("dog" "chases" "dog" "-")
The dog eats the dog.
Unknown
random
[@0: The dog eats the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "eats" "dog" "+")
The mouse does not visit the mouse.
Unknown
inv-random
[@0: The mouse visits the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "visits" "mouse" "-")
The lion chases the cat.
Unknown
random
[@0: The lion chases the cat.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "cat" "+")
@0: The cat is blue.[(triple1)] The cat visits the dog.[(triple2)] The dog does not eat the lion.[(triple3)] The dog eats the mouse.[(triple4)] The dog is not big.[(triple5)] The dog is red.[(triple6)] The dog visits the mouse.[(triple7)] The lion eats the mouse.[(triple8)] The lion is blue.[(triple9)] The lion is nice.[(triple10 OR ((((((triple9) -> rule3)) -> rule7)) -> rule6))] The lion visits the cat.[(triple11)] The lion visits the dog.[(triple12)] The mouse chases the lion.[(triple13)] The mouse is young.[(triple14)] The mouse visits the dog.[(triple15)] @1: The cat chases the lion.[(((triple1) -> rule3))] The lion chases the lion.[(((triple9) -> rule3))] The mouse chases the dog.[(((triple13) -> rule7))] @2: The cat chases the dog.[(((((triple1) -> rule3)) -> rule7))] The lion chases the dog.[(((((triple9) -> rule3)) -> rule7))] The mouse is nice.[(((((triple13) -> rule7)) -> rule6))] @3: The cat is nice.[(((((((triple1) -> rule3)) -> rule7)) -> rule6))]
The cat is blue.
("cat" "is" "blue" "+")
triple1
The cat visits the dog.
("cat" "visits" "dog" "+")
triple2
The dog does not eat the lion.
("dog" "eats" "lion" "-")
triple3
The dog eats the mouse.
("dog" "eats" "mouse" "+")
triple4
The dog is not big.
("dog" "is" "big" "-")
triple5
The dog is red.
("dog" "is" "red" "+")
triple6
The dog visits the mouse.
("dog" "visits" "mouse" "+")
triple7
The lion eats the mouse.
("lion" "eats" "mouse" "+")
triple8
The lion is blue.
("lion" "is" "blue" "+")
triple9
The lion is nice.
("lion" "is" "nice" "+")
triple10
((((((triple9) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
The lion is nice.
("lion" "is" "nice" "+")
int1
The lion chases the dog.
("lion" "chases" "dog" "+")
int2
The lion chases the lion.
("lion" "chases" "lion" "+")
int3
The lion visits the cat.
("lion" "visits" "cat" "+")
triple11
The lion visits the dog.
("lion" "visits" "dog" "+")
triple12
The mouse chases the lion.
("mouse" "chases" "lion" "+")
triple13
The mouse is young.
("mouse" "is" "young" "+")
triple14
The mouse visits the dog.
("mouse" "visits" "dog" "+")
triple15
The cat chases the lion.
("cat" "chases" "lion" "+")
((triple1) -> (rule3 % int1))
The cat chases the lion.
("cat" "chases" "lion" "+")
int1
The lion chases the lion.
("lion" "chases" "lion" "+")
((triple9) -> (rule3 % int1))
The lion chases the lion.
("lion" "chases" "lion" "+")
int1
The mouse chases the dog.
("mouse" "chases" "dog" "+")
((triple13) -> (rule7 % int1))
The mouse chases the dog.
("mouse" "chases" "dog" "+")
int1
The cat chases the dog.
("cat" "chases" "dog" "+")
((((triple1) -> (rule3 % int2))) -> (rule7 % int1))
The cat chases the dog.
("cat" "chases" "dog" "+")
int1
The cat chases the lion.
("cat" "chases" "lion" "+")
int2
The lion chases the dog.
("lion" "chases" "dog" "+")
((((triple9) -> (rule3 % int2))) -> (rule7 % int1))
The lion chases the dog.
("lion" "chases" "dog" "+")
int1
The lion chases the lion.
("lion" "chases" "lion" "+")
int2
The mouse is nice.
("mouse" "is" "nice" "+")
((((triple13) -> (rule7 % int2))) -> (rule6 % int1))
The mouse is nice.
("mouse" "is" "nice" "+")
int1
The mouse chases the dog.
("mouse" "chases" "dog" "+")
int2
The cat is nice.
("cat" "is" "nice" "+")
((((((triple1) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
The cat is nice.
("cat" "is" "nice" "+")
int1
The cat chases the dog.
("cat" "chases" "dog" "+")
int2
The cat chases the lion.
("cat" "chases" "lion" "+")
int3