The cow is kind. The cow sees the lion. The lion chases the cow. The lion is big. The lion is blue. The lion sees the cow. The lion visits the cow. If someone sees the lion and the lion is big then the lion is kind. If the lion sees the cow then the lion chases the cow. If someone chases the cow and they are kind then they visit the lion.
The cow is kind.
("cow" "is" "kind" "+")
The cow sees the lion.
("cow" "sees" "lion" "+")
The lion chases the cow.
("lion" "chases" "cow" "+")
The lion is big.
("lion" "is" "big" "+")
The lion is blue.
("lion" "is" "blue" "+")
The lion sees the cow.
("lion" "sees" "cow" "+")
The lion visits the cow.
("lion" "visits" "cow" "+")
If someone sees the lion and the lion is big then the lion is kind.
((("someone" "sees" "lion" "+") ("lion" "is" "big" "+")) -> ("lion" "is" "kind" "+"))
If the lion sees the cow then the lion chases the cow.
((("lion" "sees" "cow" "+")) -> ("lion" "chases" "cow" "+"))
If someone chases the cow and they are kind then they visit the lion.
((("someone" "chases" "cow" "+") ("someone" "is" "kind" "+")) -> ("someone" "visits" "lion" "+"))
The lion chases the cow.
True
1
proof
[(triple3 OR ((triple6) -> rule2))]
("lion" "chases" "cow" "+")
triple3
((triple6) -> (rule2 % int1))
The lion chases the cow.
("lion" "chases" "cow" "+")
int1
The lion does not visit the cow.
False
1
inv-proof
[(triple7)]
("lion" "visits" "cow" "-")
triple7
The lion is kind.
True
3
proof
[(((triple2 triple4) -> rule1))]
("lion" "is" "kind" "+")
((triple2 triple4) -> (rule1 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
The lion is not kind.
False
3
inv-proof
[(((triple2 triple4) -> rule1))]
("lion" "is" "kind" "-")
((triple2 triple4) -> (rule1 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
The lion visits the lion.
True
5
proof
[(((triple3 ((triple2 triple4) -> rule1)) -> rule3) OR ((((triple6) -> rule2) ((triple2 triple4) -> rule1)) -> rule3))]
("lion" "visits" "lion" "+")
((triple3 ((triple2 triple4) -> (rule1 % int2))) -> (rule3 % int1))
The lion visits the lion.
("lion" "visits" "lion" "+")
int1
The lion is kind.
("lion" "is" "kind" "+")
int2
((((triple6) -> (rule2 % int3)) ((triple2 triple4) -> (rule1 % int2))) -> (rule3 % int1))
The lion visits the lion.
("lion" "visits" "lion" "+")
int1
The lion is kind.
("lion" "is" "kind" "+")
int2
The lion chases the cow.
("lion" "chases" "cow" "+")
int3
The lion does not visit the lion.
False
5
inv-proof
[(((triple3 ((triple2 triple4) -> rule1)) -> rule3) OR ((((triple6) -> rule2) ((triple2 triple4) -> rule1)) -> rule3))]
("lion" "visits" "lion" "-")
((triple3 ((triple2 triple4) -> (rule1 % int2))) -> (rule3 % int1))
The lion visits the lion.
("lion" "visits" "lion" "+")
int1
The lion is kind.
("lion" "is" "kind" "+")
int2
((((triple6) -> (rule2 % int3)) ((triple2 triple4) -> (rule1 % int2))) -> (rule3 % int1))
The lion visits the lion.
("lion" "visits" "lion" "+")
int1
The lion is kind.
("lion" "is" "kind" "+")
int2
The lion chases the cow.
("lion" "chases" "cow" "+")
int3
The cow does not visit the lion.
Unknown
inv-rconc
[@1: The cow visits the lion.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cow" "visits" "lion" "-")
The lion is rough.
Unknown
random
[@0: The lion is rough.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "rough" "+")
The lion is not round.
Unknown
inv-random
[@0: The lion is round.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "round" "-")
The cow is rough.
Unknown
random
[@0: The cow is rough.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "rough" "+")
The cow does not visit the cow.
Unknown
inv-random
[@0: The cow visits the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "visits" "cow" "-")
The cow is round.
Unknown
random
[@0: The cow is round.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "round" "+")
@0: The cow is kind.[(triple1)] The cow sees the lion.[(triple2)] The lion chases the cow.[(triple3 OR ((triple6) -> rule2))] The lion is big.[(triple4)] The lion is blue.[(triple5)] The lion sees the cow.[(triple6)] The lion visits the cow.[(triple7)] @1: The lion is kind.[(((triple2 triple4) -> rule1))] @2: The lion visits the lion.[(((triple3 ((triple2 triple4) -> rule1)) -> rule3) OR ((((triple6) -> rule2) ((triple2 triple4) -> rule1)) -> rule3))]
The cow is kind.
("cow" "is" "kind" "+")
triple1
The cow sees the lion.
("cow" "sees" "lion" "+")
triple2
The lion chases the cow.
("lion" "chases" "cow" "+")
triple3
((triple6) -> (rule2 % int1))
The lion chases the cow.
("lion" "chases" "cow" "+")
int1
The lion is big.
("lion" "is" "big" "+")
triple4
The lion is blue.
("lion" "is" "blue" "+")
triple5
The lion sees the cow.
("lion" "sees" "cow" "+")
triple6
The lion visits the cow.
("lion" "visits" "cow" "+")
triple7
The lion is kind.
("lion" "is" "kind" "+")
((triple2 triple4) -> (rule1 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
The lion visits the lion.
("lion" "visits" "lion" "+")
((triple3 ((triple2 triple4) -> (rule1 % int2))) -> (rule3 % int1))
The lion visits the lion.
("lion" "visits" "lion" "+")
int1
The lion is kind.
("lion" "is" "kind" "+")
int2
((((triple6) -> (rule2 % int3)) ((triple2 triple4) -> (rule1 % int2))) -> (rule3 % int1))
The lion visits the lion.
("lion" "visits" "lion" "+")
int1
The lion is kind.
("lion" "is" "kind" "+")
int2
The lion chases the cow.
("lion" "chases" "cow" "+")
int3