The dog is cold. The lion is young. The mouse sees the tiger. The tiger sees the lion. If someone sees the lion then the lion visits the tiger. If someone is green then they eat the tiger. If someone is green then they visit the mouse.
The dog is cold.
("dog" "is" "cold" "+")
The lion is young.
("lion" "is" "young" "+")
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
The tiger sees the lion.
("tiger" "sees" "lion" "+")
If someone sees the lion then the lion visits the tiger.
((("someone" "sees" "lion" "+")) -> ("lion" "visits" "tiger" "+"))
If someone is green then they eat the tiger.
((("someone" "is" "green" "+")) -> ("someone" "eats" "tiger" "+"))
If someone is green then they visit the mouse.
((("someone" "is" "green" "+")) -> ("someone" "visits" "mouse" "+"))
The lion is young.
True
1
proof
[(triple2)]
("lion" "is" "young" "+")
triple2
The tiger does not see the lion.
False
1
inv-proof
[(triple4)]
("tiger" "sees" "lion" "-")
triple4
The lion visits the tiger.
True
2
proof
[(((triple4) -> rule1))]
("lion" "visits" "tiger" "+")
((triple4) -> (rule1 % int1))
The lion visits the tiger.
("lion" "visits" "tiger" "+")
int1
The lion does not visit the tiger.
False
2
inv-proof
[(((triple4) -> rule1))]
("lion" "visits" "tiger" "-")
((triple4) -> (rule1 % int1))
The lion visits the tiger.
("lion" "visits" "tiger" "+")
int1
The dog does not eat the tiger.
Unknown
inv-rconc
[@1: The dog eats the tiger.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("dog" "eats" "tiger" "-")
The lion visits the mouse.
Unknown
rconc
[@1: The lion visits the mouse.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("lion" "visits" "mouse" "+")
The lion does not eat the lion.
Unknown
inv-random
[@0: The lion eats the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "eats" "lion" "-")
The tiger is rough.
Unknown
random
[@0: The tiger is rough.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "rough" "+")
@0: The dog is cold.[(triple1)] The lion is young.[(triple2)] The mouse sees the tiger.[(triple3)] The tiger sees the lion.[(triple4)] @1: The lion visits the tiger.[(((triple4) -> rule1))]
The dog is cold.
("dog" "is" "cold" "+")
triple1
The lion is young.
("lion" "is" "young" "+")
triple2
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
triple3
The tiger sees the lion.
("tiger" "sees" "lion" "+")
triple4
The lion visits the tiger.
("lion" "visits" "tiger" "+")
((triple4) -> (rule1 % int1))
The lion visits the tiger.
("lion" "visits" "tiger" "+")
int1