The cow needs the lion. The lion chases the cow. The rabbit sees the squirrel. The squirrel chases the lion. If something needs the cow and it does not chase the lion then the cow is nice. If the squirrel is young then the squirrel is kind. If something chases the lion then the lion needs the squirrel. If the lion does not see the cow then the lion chases the cow. If the cow needs the rabbit and the cow does not see the squirrel then the squirrel needs the cow. If something chases the cow then it is red. If something is red and it needs the squirrel then the squirrel needs the lion. If something needs the cow and it is not kind then the cow is red.
The cow needs the lion.
("cow" "needs" "lion" "+")
The lion chases the cow.
("lion" "chases" "cow" "+")
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
The squirrel chases the lion.
("squirrel" "chases" "lion" "+")
If something needs the cow and it does not chase the lion then the cow is nice.
((("something" "needs" "cow" "+") ("something" "chases" "lion" "~")) -> ("cow" "is" "nice" "+"))
If the squirrel is young then the squirrel is kind.
((("squirrel" "is" "young" "+")) -> ("squirrel" "is" "kind" "+"))
If something chases the lion then the lion needs the squirrel.
((("something" "chases" "lion" "+")) -> ("lion" "needs" "squirrel" "+"))
If the lion does not see the cow then the lion chases the cow.
((("lion" "sees" "cow" "~")) -> ("lion" "chases" "cow" "+"))
If the cow needs the rabbit and the cow does not see the squirrel then the squirrel needs the cow.
((("cow" "needs" "rabbit" "+") ("cow" "sees" "squirrel" "~")) -> ("squirrel" "needs" "cow" "+"))
If something chases the cow then it is red.
((("something" "chases" "cow" "+")) -> ("something" "is" "red" "+"))
If something is red and it needs the squirrel then the squirrel needs the lion.
((("something" "is" "red" "+") ("something" "needs" "squirrel" "+")) -> ("squirrel" "needs" "lion" "+"))
If something needs the cow and it is not kind then the cow is red.
((("something" "needs" "cow" "+") ("something" "is" "kind" "~")) -> ("cow" "is" "red" "+"))
The lion chases the cow.
True
1
proof
[(triple2)]
("lion" "chases" "cow" "+")
triple2
The rabbit does not see the squirrel.
False
1
inv-proof
[(triple3)]
("rabbit" "sees" "squirrel" "-")
triple3
The lion needs the squirrel.
True
2
proof
[(((triple4) -> rule3))]
("lion" "needs" "squirrel" "+")
((triple4) -> (rule3 % int1))
The lion needs the squirrel.
("lion" "needs" "squirrel" "+")
int1
The lion is not red.
False
2
inv-proof
[(((triple2) -> rule6))]
("lion" "is" "red" "-")
((triple2) -> (rule6 % int1))
The lion is red.
("lion" "is" "red" "+")
int1
The squirrel needs the lion.
True
5
proof
[(((((triple2) -> rule6) ((triple4) -> rule3)) -> rule7))]
("squirrel" "needs" "lion" "+")
((((triple2) -> (rule6 % int3)) ((triple4) -> (rule3 % int2))) -> (rule7 % int1))
The squirrel needs the lion.
("squirrel" "needs" "lion" "+")
int1
The lion needs the squirrel.
("lion" "needs" "squirrel" "+")
int2
The lion is red.
("lion" "is" "red" "+")
int3
The squirrel does not need the lion.
False
5
inv-proof
[(((((triple2) -> rule6) ((triple4) -> rule3)) -> rule7))]
("squirrel" "needs" "lion" "-")
((((triple2) -> (rule6 % int3)) ((triple4) -> (rule3 % int2))) -> (rule7 % int1))
The squirrel needs the lion.
("squirrel" "needs" "lion" "+")
int1
The lion needs the squirrel.
("lion" "needs" "squirrel" "+")
int2
The lion is red.
("lion" "is" "red" "+")
int3
The squirrel does not need the cow.
Unknown
inv-rconc
[@1: The squirrel needs the cow.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("squirrel" "needs" "cow" "-")
The rabbit is red.
Unknown
rconc
[@1: The rabbit is red.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("rabbit" "is" "red" "+")
The cow is not red.
Unknown
inv-rconc
[@1: The cow is red.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("cow" "is" "red" "-")
The lion is nice.
Unknown
random
[@0: The lion is nice.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "nice" "+")
The rabbit does not see the lion.
Unknown
inv-random
[@0: The rabbit sees the lion.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "sees" "lion" "-")
The rabbit is green.
Unknown
random
[@0: The rabbit is green.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "green" "+")
@0: The cow needs the lion.[(triple1)] The lion chases the cow.[(triple2)] The rabbit sees the squirrel.[(triple3)] The squirrel chases the lion.[(triple4)] @1: The lion is red.[(((triple2) -> rule6))] The lion needs the squirrel.[(((triple4) -> rule3))] @2: The squirrel needs the lion.[(((((triple2) -> rule6) ((triple4) -> rule3)) -> rule7))]
The cow needs the lion.
("cow" "needs" "lion" "+")
triple1
The lion chases the cow.
("lion" "chases" "cow" "+")
triple2
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
triple3
The squirrel chases the lion.
("squirrel" "chases" "lion" "+")
triple4
The lion is red.
("lion" "is" "red" "+")
((triple2) -> (rule6 % int1))
The lion is red.
("lion" "is" "red" "+")
int1
The lion needs the squirrel.
("lion" "needs" "squirrel" "+")
((triple4) -> (rule3 % int1))
The lion needs the squirrel.
("lion" "needs" "squirrel" "+")
int1
The squirrel needs the lion.
("squirrel" "needs" "lion" "+")
((((triple2) -> (rule6 % int3)) ((triple4) -> (rule3 % int2))) -> (rule7 % int1))
The squirrel needs the lion.
("squirrel" "needs" "lion" "+")
int1
The lion needs the squirrel.
("lion" "needs" "squirrel" "+")
int2
The lion is red.
("lion" "is" "red" "+")
int3