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