The bear visits the cow. The cow needs the lion. The lion needs the bear. The squirrel needs the bear. If someone visits the squirrel and the squirrel needs the lion then the lion is rough. If someone needs the squirrel then they are kind. If someone needs the lion then they visit the lion. If someone chases the squirrel and the squirrel visits the cow then the squirrel needs the lion. If someone needs the bear and the bear visits the cow then the cow needs the squirrel. If someone is kind then they chase the bear.
The bear visits the cow.
("bear" "visits" "cow" "+")
The cow needs the lion.
("cow" "needs" "lion" "+")
The lion needs the bear.
("lion" "needs" "bear" "+")
The squirrel needs the bear.
("squirrel" "needs" "bear" "+")
If someone visits the squirrel and the squirrel needs the lion then the lion is rough.
((("someone" "visits" "squirrel" "+") ("squirrel" "needs" "lion" "+")) -> ("lion" "is" "rough" "+"))
If someone needs the squirrel then they are kind.
((("someone" "needs" "squirrel" "+")) -> ("someone" "is" "kind" "+"))
If someone needs the lion then they visit the lion.
((("someone" "needs" "lion" "+")) -> ("someone" "visits" "lion" "+"))
If someone chases the squirrel and the squirrel visits the cow then the squirrel needs the lion.
((("someone" "chases" "squirrel" "+") ("squirrel" "visits" "cow" "+")) -> ("squirrel" "needs" "lion" "+"))
If someone needs the bear and the bear visits the cow then the cow needs the squirrel.
((("someone" "needs" "bear" "+") ("bear" "visits" "cow" "+")) -> ("cow" "needs" "squirrel" "+"))
If someone is kind then they chase the bear.
((("someone" "is" "kind" "+")) -> ("someone" "chases" "bear" "+"))
The cow needs the lion.
True
1
proof
[(triple2)]
("cow" "needs" "lion" "+")
triple2
The bear does not visit the cow.
False
1
inv-proof
[(triple1)]
("bear" "visits" "cow" "-")
triple1
The cow visits the lion.
True
2
proof
[(((triple2) -> rule3))]
("cow" "visits" "lion" "+")
((triple2) -> (rule3 % int1))
The cow visits the lion.
("cow" "visits" "lion" "+")
int1
The cow does not visit the lion.
False
2
inv-proof
[(((triple2) -> rule3))]
("cow" "visits" "lion" "-")
((triple2) -> (rule3 % int1))
The cow visits the lion.
("cow" "visits" "lion" "+")
int1
The cow is kind.
True
4
proof
[(((((triple3 triple1) -> rule5)) -> rule2) OR ((((triple4 triple1) -> rule5)) -> rule2))]
("cow" "is" "kind" "+")
((((triple3 triple1) -> (rule5 % int2))) -> (rule2 % int1))
The cow is kind.
("cow" "is" "kind" "+")
int1
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
int2
((((triple4 triple1) -> (rule5 % int2))) -> (rule2 % int1))
The cow is kind.
("cow" "is" "kind" "+")
int1
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
int2
The cow is not kind.
False
4
inv-proof
[(((((triple3 triple1) -> rule5)) -> rule2) OR ((((triple4 triple1) -> rule5)) -> rule2))]
("cow" "is" "kind" "-")
((((triple3 triple1) -> (rule5 % int2))) -> (rule2 % int1))
The cow is kind.
("cow" "is" "kind" "+")
int1
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
int2
((((triple4 triple1) -> (rule5 % int2))) -> (rule2 % int1))
The cow is kind.
("cow" "is" "kind" "+")
int1
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
int2
The cow chases the bear.
True
5
proof
[(((((((triple3 triple1) -> rule5)) -> rule2)) -> rule6) OR ((((((triple4 triple1) -> rule5)) -> rule2)) -> rule6))]
("cow" "chases" "bear" "+")
((((((triple3 triple1) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
The cow chases the bear.
("cow" "chases" "bear" "+")
int1
The cow is kind.
("cow" "is" "kind" "+")
int2
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
int3
((((((triple4 triple1) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
The cow chases the bear.
("cow" "chases" "bear" "+")
int1
The cow is kind.
("cow" "is" "kind" "+")
int2
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
int3
The cow does not chase the bear.
False
5
inv-proof
[(((((((triple3 triple1) -> rule5)) -> rule2)) -> rule6) OR ((((((triple4 triple1) -> rule5)) -> rule2)) -> rule6))]
("cow" "chases" "bear" "-")
((((((triple3 triple1) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
The cow chases the bear.
("cow" "chases" "bear" "+")
int1
The cow is kind.
("cow" "is" "kind" "+")
int2
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
int3
((((((triple4 triple1) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
The cow chases the bear.
("cow" "chases" "bear" "+")
int1
The cow is kind.
("cow" "is" "kind" "+")
int2
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
int3
The bear does not visit the lion.
Unknown
inv-rconc
[@1: The bear visits the lion.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("bear" "visits" "lion" "-")
The squirrel visits the lion.
Unknown
rconc
[@2: The squirrel visits the lion.[CWA. Example of deepest failure = (rule3 <- rule4 <- FAIL)]]
("squirrel" "visits" "lion" "+")
The lion does not chase the bear.
Unknown
inv-rconc
[@2: The lion chases the bear.[CWA. Example of deepest failure = (rule6 <- rule2 <- FAIL)]]
("lion" "chases" "bear" "-")
The lion visits the lion.
Unknown
rconc
[@1: The lion visits the lion.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("lion" "visits" "lion" "+")
The cow does not chase the lion.
Unknown
inv-random
[@0: The cow chases the lion.[CWA. Example of deepest failure = (FAIL)]]
("cow" "chases" "lion" "-")
The lion visits the bear.
Unknown
random
[@0: The lion visits the bear.[CWA. Example of deepest failure = (FAIL)]]
("lion" "visits" "bear" "+")
The bear does not chase the cow.
Unknown
inv-random
[@0: The bear chases the cow.[CWA. Example of deepest failure = (FAIL)]]
("bear" "chases" "cow" "-")
The squirrel visits the bear.
Unknown
random
[@0: The squirrel visits the bear.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "visits" "bear" "+")
@0: The bear visits the cow.[(triple1)] The cow needs the lion.[(triple2)] The lion needs the bear.[(triple3)] The squirrel needs the bear.[(triple4)] @1: The cow needs the squirrel.[(((triple3 triple1) -> rule5) OR ((triple4 triple1) -> rule5))] The cow visits the lion.[(((triple2) -> rule3))] @2: The cow is kind.[(((((triple3 triple1) -> rule5)) -> rule2) OR ((((triple4 triple1) -> rule5)) -> rule2))] @3: The cow chases the bear.[(((((((triple3 triple1) -> rule5)) -> rule2)) -> rule6) OR ((((((triple4 triple1) -> rule5)) -> rule2)) -> rule6))]
The bear visits the cow.
("bear" "visits" "cow" "+")
triple1
The cow needs the lion.
("cow" "needs" "lion" "+")
triple2
The lion needs the bear.
("lion" "needs" "bear" "+")
triple3
The squirrel needs the bear.
("squirrel" "needs" "bear" "+")
triple4
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
((triple3 triple1) -> (rule5 % int1))
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
int1
((triple4 triple1) -> (rule5 % int1))
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
int1
The cow visits the lion.
("cow" "visits" "lion" "+")
((triple2) -> (rule3 % int1))
The cow visits the lion.
("cow" "visits" "lion" "+")
int1
The cow is kind.
("cow" "is" "kind" "+")
((((triple3 triple1) -> (rule5 % int2))) -> (rule2 % int1))
The cow is kind.
("cow" "is" "kind" "+")
int1
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
int2
((((triple4 triple1) -> (rule5 % int2))) -> (rule2 % int1))
The cow is kind.
("cow" "is" "kind" "+")
int1
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
int2
The cow chases the bear.
("cow" "chases" "bear" "+")
((((((triple3 triple1) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
The cow chases the bear.
("cow" "chases" "bear" "+")
int1
The cow is kind.
("cow" "is" "kind" "+")
int2
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
int3
((((((triple4 triple1) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
The cow chases the bear.
("cow" "chases" "bear" "+")
int1
The cow is kind.
("cow" "is" "kind" "+")
int2
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
int3