The dog is round. The lion likes the squirrel. The mouse is kind. The squirrel is round. If something visits the dog then it is kind. If the dog likes the lion and the dog likes the mouse then the dog is big. If something is big then it likes the dog. If the lion likes the squirrel then the lion visits the squirrel. If the mouse is nice then the mouse is rough. If something likes the lion and it is kind then the lion is kind. If something likes the dog then it sees the mouse. If something visits the dog and it is big then it is nice.
The dog is round.
("dog" "is" "round" "+")
The lion likes the squirrel.
("lion" "likes" "squirrel" "+")
The mouse is kind.
("mouse" "is" "kind" "+")
The squirrel is round.
("squirrel" "is" "round" "+")
If something visits the dog then it is kind.
((("something" "visits" "dog" "+")) -> ("something" "is" "kind" "+"))
If the dog likes the lion and the dog likes the mouse then the dog is big.
((("dog" "likes" "lion" "+") ("dog" "likes" "mouse" "+")) -> ("dog" "is" "big" "+"))
If something is big then it likes the dog.
((("something" "is" "big" "+")) -> ("something" "likes" "dog" "+"))
If the lion likes the squirrel then the lion visits the squirrel.
((("lion" "likes" "squirrel" "+")) -> ("lion" "visits" "squirrel" "+"))
If the mouse is nice then the mouse is rough.
((("mouse" "is" "nice" "+")) -> ("mouse" "is" "rough" "+"))
If something likes the lion and it is kind then the lion is kind.
((("something" "likes" "lion" "+") ("something" "is" "kind" "+")) -> ("lion" "is" "kind" "+"))
If something likes the dog then it sees the mouse.
((("something" "likes" "dog" "+")) -> ("something" "sees" "mouse" "+"))
If something visits the dog and it is big then it is nice.
((("something" "visits" "dog" "+") ("something" "is" "big" "+")) -> ("something" "is" "nice" "+"))
The dog is round.
True
1
proof
[(triple1)]
("dog" "is" "round" "+")
triple1
The lion does not like the squirrel.
False
1
inv-proof
[(triple2)]
("lion" "likes" "squirrel" "-")
triple2
The lion visits the squirrel.
True
2
proof
[(((triple2) -> rule4))]
("lion" "visits" "squirrel" "+")
((triple2) -> (rule4 % int1))
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
int1
The lion does not visit the squirrel.
False
2
inv-proof
[(((triple2) -> rule4))]
("lion" "visits" "squirrel" "-")
((triple2) -> (rule4 % int1))
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
int1
The mouse is not rough.
Unknown
inv-rconc
[@2: The mouse is rough.[CWA. Example of deepest failure = (rule5 <- rule8 <- FAIL)]]
("mouse" "is" "rough" "-")
The lion likes the dog.
Unknown
rconc
[@1: The lion likes the dog.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("lion" "likes" "dog" "+")
The dog does not like the lion.
Unknown
inv-random
[@0: The dog likes the lion.[CWA. Example of deepest failure = (FAIL)]]
("dog" "likes" "lion" "-")
The mouse is round.
Unknown
random
[@0: The mouse is round.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "round" "+")
@0: The dog is round.[(triple1)] The lion likes the squirrel.[(triple2)] The mouse is kind.[(triple3)] The squirrel is round.[(triple4)] @1: The lion visits the squirrel.[(((triple2) -> rule4))]
The dog is round.
("dog" "is" "round" "+")
triple1
The lion likes the squirrel.
("lion" "likes" "squirrel" "+")
triple2
The mouse is kind.
("mouse" "is" "kind" "+")
triple3
The squirrel is round.
("squirrel" "is" "round" "+")
triple4
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
((triple2) -> (rule4 % int1))
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
int1