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