The cat does not need the cow. The cow needs the lion. The lion does not chase the cat. The lion is kind. The lion does not need the cat. The squirrel does not chase the cow. The squirrel is big. If the cow chases the cat and the cat chases the lion then the cat is big. If someone needs the cat and the cat does not need the lion then the lion needs the squirrel. If someone is kind then they visit the lion. If the cat is round and the cat does not visit the squirrel then the squirrel is round. If someone chases the cat and they are not kind then the cat is nice. If someone chases the cow and they do not chase the lion then the lion needs the cow. If the cow visits the lion then the lion is not big. If someone visits the cat and they do not need the cat then the cat does not chase the squirrel.
The cat does not need the cow.
("cat" "needs" "cow" "-")
The cow needs the lion.
("cow" "needs" "lion" "+")
The lion does not chase the cat.
("lion" "chases" "cat" "-")
The lion is kind.
("lion" "is" "kind" "+")
The lion does not need the cat.
("lion" "needs" "cat" "-")
The squirrel does not chase the cow.
("squirrel" "chases" "cow" "-")
The squirrel is big.
("squirrel" "is" "big" "+")
If the cow chases the cat and the cat chases the lion then the cat is big.
((("cow" "chases" "cat" "+") ("cat" "chases" "lion" "+")) -> ("cat" "is" "big" "+"))
If someone needs the cat and the cat does not need the lion then the lion needs the squirrel.
((("someone" "needs" "cat" "+") ("cat" "needs" "lion" "~")) -> ("lion" "needs" "squirrel" "+"))
If someone is kind then they visit the lion.
((("someone" "is" "kind" "+")) -> ("someone" "visits" "lion" "+"))
If the cat is round and the cat does not visit the squirrel then the squirrel is round.
((("cat" "is" "round" "+") ("cat" "visits" "squirrel" "~")) -> ("squirrel" "is" "round" "+"))
If someone chases the cat and they are not kind then the cat is nice.
((("someone" "chases" "cat" "+") ("someone" "is" "kind" "~")) -> ("cat" "is" "nice" "+"))
If someone chases the cow and they do not chase the lion then the lion needs the cow.
((("someone" "chases" "cow" "+") ("someone" "chases" "lion" "~")) -> ("lion" "needs" "cow" "+"))
If the cow visits the lion then the lion is not big.
((("cow" "visits" "lion" "+")) -> ("lion" "is" "big" "-"))
If someone visits the cat and they do not need the cat then the cat does not chase the squirrel.
((("someone" "visits" "cat" "+") ("someone" "needs" "cat" "~")) -> ("cat" "chases" "squirrel" "-"))
The lion does not chase the cat.
True
1
proof
[(triple3)]
("lion" "chases" "cat" "-")
triple3
The squirrel is not big.
False
1
inv-proof
[(triple7)]
("squirrel" "is" "big" "-")
triple7
The lion visits the lion.
True
2
proof
[(((triple4) -> rule3))]
("lion" "visits" "lion" "+")
((triple4) -> (rule3 % int1))
The lion visits the lion.
("lion" "visits" "lion" "+")
int1
The lion does not visit the lion.
False
2
inv-proof
[(((triple4) -> rule3))]
("lion" "visits" "lion" "-")
((triple4) -> (rule3 % int1))
The lion visits the lion.
("lion" "visits" "lion" "+")
int1
The squirrel is not round.
Unknown
inv-rconc
[@1: The squirrel is round.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("squirrel" "is" "round" "-")
The squirrel visits the lion.
Unknown
rconc
[@1: The squirrel visits the lion.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("squirrel" "visits" "lion" "+")
The squirrel does not need the cow.
Unknown
inv-random
[@0: The squirrel needs the cow.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "needs" "cow" "-")
The lion chases the cow.
Unknown
random
[@0: The lion chases the cow.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "cow" "+")
@0: The cat does not need the cow.[(triple1)] The cow needs the lion.[(triple2)] The lion does not chase the cat.[(triple3)] The lion does not need the cat.[(triple5)] The lion is kind.[(triple4)] The squirrel does not chase the cow.[(triple6)] The squirrel is big.[(triple7)] @1: The lion visits the lion.[(((triple4) -> rule3))]
The cat does not need the cow.
("cat" "needs" "cow" "-")
triple1
The cow needs the lion.
("cow" "needs" "lion" "+")
triple2
The lion does not chase the cat.
("lion" "chases" "cat" "-")
triple3
The lion does not need the cat.
("lion" "needs" "cat" "-")
triple5
The lion is kind.
("lion" "is" "kind" "+")
triple4
The squirrel does not chase the cow.
("squirrel" "chases" "cow" "-")
triple6
The squirrel is big.
("squirrel" "is" "big" "+")
triple7
The lion visits the lion.
("lion" "visits" "lion" "+")
((triple4) -> (rule3 % int1))
The lion visits the lion.
("lion" "visits" "lion" "+")
int1