The cow chases the lion. The cow sees the tiger. The lion is young. The mouse visits the cow. The tiger chases the mouse. The tiger is rough. The tiger visits the lion. If someone sees the tiger then they visit the mouse. If someone is nice and they visit the tiger then they are cold. If the lion visits the cow and the lion is young then the cow visits the mouse. If someone visits the cow then the cow is cold. If someone chases the mouse and they are nice then the mouse sees the tiger. If someone is cold then they are red.
The cow chases the lion.
("cow" "chases" "lion" "+")
The cow sees the tiger.
("cow" "sees" "tiger" "+")
The lion is young.
("lion" "is" "young" "+")
The mouse visits the cow.
("mouse" "visits" "cow" "+")
The tiger chases the mouse.
("tiger" "chases" "mouse" "+")
The tiger is rough.
("tiger" "is" "rough" "+")
The tiger visits the lion.
("tiger" "visits" "lion" "+")
If someone sees the tiger then they visit the mouse.
((("someone" "sees" "tiger" "+")) -> ("someone" "visits" "mouse" "+"))
If someone is nice and they visit the tiger then they are cold.
((("someone" "is" "nice" "+") ("someone" "visits" "tiger" "+")) -> ("someone" "is" "cold" "+"))
If the lion visits the cow and the lion is young then the cow visits the mouse.
((("lion" "visits" "cow" "+") ("lion" "is" "young" "+")) -> ("cow" "visits" "mouse" "+"))
If someone visits the cow then the cow is cold.
((("someone" "visits" "cow" "+")) -> ("cow" "is" "cold" "+"))
If someone chases the mouse and they are nice then the mouse sees the tiger.
((("someone" "chases" "mouse" "+") ("someone" "is" "nice" "+")) -> ("mouse" "sees" "tiger" "+"))
If someone is cold then they are red.
((("someone" "is" "cold" "+")) -> ("someone" "is" "red" "+"))
The lion is young.
True
1
proof
[(triple3)]
("lion" "is" "young" "+")
triple3
The tiger is not rough.
False
1
inv-proof
[(triple6)]
("tiger" "is" "rough" "-")
triple6
The cow visits the mouse.
True
2
proof
[(((triple2) -> rule1))]
("cow" "visits" "mouse" "+")
((triple2) -> (rule1 % int1))
The cow visits the mouse.
("cow" "visits" "mouse" "+")
int1
The cow is not cold.
False
2
inv-proof
[(((triple4) -> rule4))]
("cow" "is" "cold" "-")
((triple4) -> (rule4 % int1))
The cow is cold.
("cow" "is" "cold" "+")
int1
The cow is red.
True
3
proof
[(((((triple4) -> rule4)) -> rule6))]
("cow" "is" "red" "+")
((((triple4) -> (rule4 % int2))) -> (rule6 % int1))
The cow is red.
("cow" "is" "red" "+")
int1
The cow is cold.
("cow" "is" "cold" "+")
int2
The cow is not red.
False
3
inv-proof
[(((((triple4) -> rule4)) -> rule6))]
("cow" "is" "red" "-")
((((triple4) -> (rule4 % int2))) -> (rule6 % int1))
The cow is red.
("cow" "is" "red" "+")
int1
The cow is cold.
("cow" "is" "cold" "+")
int2
The mouse does not visit the mouse.
Unknown
inv-rconc
[@2: The mouse visits the mouse.[CWA. Example of deepest failure = (rule1 <- rule5 <- FAIL)]]
("mouse" "visits" "mouse" "-")
The lion is red.
Unknown
rconc
[@2: The lion is red.[CWA. Example of deepest failure = (rule6 <- rule2 <- FAIL)]]
("lion" "is" "red" "+")
The tiger does not visit the mouse.
Unknown
inv-rconc
[@1: The tiger visits the mouse.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("tiger" "visits" "mouse" "-")
The lion sees the tiger.
Unknown
random
[@0: The lion sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "tiger" "+")
The lion is not nice.
Unknown
inv-random
[@0: The lion is nice.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "nice" "-")
The tiger sees the tiger.
Unknown
random
[@0: The tiger sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "tiger" "+")
@0: The cow chases the lion.[(triple1)] The cow sees the tiger.[(triple2)] The lion is young.[(triple3)] The mouse visits the cow.[(triple4)] The tiger chases the mouse.[(triple5)] The tiger is rough.[(triple6)] The tiger visits the lion.[(triple7)] @1: The cow is cold.[(((triple4) -> rule4))] The cow visits the mouse.[(((triple2) -> rule1))] @2: The cow is red.[(((((triple4) -> rule4)) -> rule6))]
The cow chases the lion.
("cow" "chases" "lion" "+")
triple1
The cow sees the tiger.
("cow" "sees" "tiger" "+")
triple2
The lion is young.
("lion" "is" "young" "+")
triple3
The mouse visits the cow.
("mouse" "visits" "cow" "+")
triple4
The tiger chases the mouse.
("tiger" "chases" "mouse" "+")
triple5
The tiger is rough.
("tiger" "is" "rough" "+")
triple6
The tiger visits the lion.
("tiger" "visits" "lion" "+")
triple7
The cow is cold.
("cow" "is" "cold" "+")
((triple4) -> (rule4 % int1))
The cow is cold.
("cow" "is" "cold" "+")
int1
The cow visits the mouse.
("cow" "visits" "mouse" "+")
((triple2) -> (rule1 % int1))
The cow visits the mouse.
("cow" "visits" "mouse" "+")
int1
The cow is red.
("cow" "is" "red" "+")
((((triple4) -> (rule4 % int2))) -> (rule6 % int1))
The cow is red.
("cow" "is" "red" "+")
int1
The cow is cold.
("cow" "is" "cold" "+")
int2