The cow sees the lion. The lion sees the cow. If something chases the cow then the cow is rough. If something sees the cow then it chases the cow.
The cow sees the lion.
("cow" "sees" "lion" "+")
The lion sees the cow.
("lion" "sees" "cow" "+")
If something chases the cow then the cow is rough.
((("something" "chases" "cow" "+")) -> ("cow" "is" "rough" "+"))
If something sees the cow then it chases the cow.
((("something" "sees" "cow" "+")) -> ("something" "chases" "cow" "+"))
The cow sees the lion.
True
1
proof
[(triple1)]
("cow" "sees" "lion" "+")
triple1
The cow does not see the lion.
False
1
inv-proof
[(triple1)]
("cow" "sees" "lion" "-")
triple1
The lion chases the cow.
True
2
proof
[(((triple2) -> rule2))]
("lion" "chases" "cow" "+")
((triple2) -> (rule2 % int1))
The lion chases the cow.
("lion" "chases" "cow" "+")
int1
The lion does not chase the cow.
False
2
inv-proof
[(((triple2) -> rule2))]
("lion" "chases" "cow" "-")
((triple2) -> (rule2 % int1))
The lion chases the cow.
("lion" "chases" "cow" "+")
int1
The cow is rough.
True
3
proof
[(((((triple2) -> rule2)) -> rule1))]
("cow" "is" "rough" "+")
((((triple2) -> (rule2 % int2))) -> (rule1 % int1))
The cow is rough.
("cow" "is" "rough" "+")
int1
The lion chases the cow.
("lion" "chases" "cow" "+")
int2
The cow is not rough.
False
3
inv-proof
[(((((triple2) -> rule2)) -> rule1))]
("cow" "is" "rough" "-")
((((triple2) -> (rule2 % int2))) -> (rule1 % int1))
The cow is rough.
("cow" "is" "rough" "+")
int1
The lion chases the cow.
("lion" "chases" "cow" "+")
int2
The cow does not chase the cow.
Unknown
inv-rconc
[@1: The cow chases the cow.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cow" "chases" "cow" "-")
The lion is rough.
Unknown
random
[@0: The lion is rough.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "rough" "+")
The cow is not kind.
Unknown
inv-random
[@0: The cow is kind.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "kind" "-")
The lion eats the cow.
Unknown
random
[@0: The lion eats the cow.[CWA. Example of deepest failure = (FAIL)]]
("lion" "eats" "cow" "+")
The lion is not blue.
Unknown
inv-random
[@0: The lion is blue.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "blue" "-")
The lion sees the lion.
Unknown
random
[@0: The lion sees the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "lion" "+")
@0: The cow sees the lion.[(triple1)] The lion sees the cow.[(triple2)] @1: The lion chases the cow.[(((triple2) -> rule2))] @2: The cow is rough.[(((((triple2) -> rule2)) -> rule1))]
The cow sees the lion.
("cow" "sees" "lion" "+")
triple1
The lion sees the cow.
("lion" "sees" "cow" "+")
triple2
The lion chases the cow.
("lion" "chases" "cow" "+")
((triple2) -> (rule2 % int1))
The lion chases the cow.
("lion" "chases" "cow" "+")
int1
The cow is rough.
("cow" "is" "rough" "+")
((((triple2) -> (rule2 % int2))) -> (rule1 % int1))
The cow is rough.
("cow" "is" "rough" "+")
int1
The lion chases the cow.
("lion" "chases" "cow" "+")
int2