The bear sees the dog. The bear sees the lion. The dog is big. The dog sees the lion. The lion likes the dog. The squirrel is rough. The squirrel needs the bear. If something likes the dog then it sees the bear. If something likes the lion then it is big. If something likes the dog then the dog needs the lion.
The bear sees the dog.
("bear" "sees" "dog" "+")
The bear sees the lion.
("bear" "sees" "lion" "+")
The dog is big.
("dog" "is" "big" "+")
The dog sees the lion.
("dog" "sees" "lion" "+")
The lion likes the dog.
("lion" "likes" "dog" "+")
The squirrel is rough.
("squirrel" "is" "rough" "+")
The squirrel needs the bear.
("squirrel" "needs" "bear" "+")
If something likes the dog then it sees the bear.
((("something" "likes" "dog" "+")) -> ("something" "sees" "bear" "+"))
If something likes the lion then it is big.
((("something" "likes" "lion" "+")) -> ("something" "is" "big" "+"))
If something likes the dog then the dog needs the lion.
((("something" "likes" "dog" "+")) -> ("dog" "needs" "lion" "+"))
The squirrel needs the bear.
True
1
proof
[(triple7)]
("squirrel" "needs" "bear" "+")
triple7
The lion does not like the dog.
False
1
inv-proof
[(triple5)]
("lion" "likes" "dog" "-")
triple5
The dog needs the lion.
True
2
proof
[(((triple5) -> rule3))]
("dog" "needs" "lion" "+")
((triple5) -> (rule3 % int1))
The dog needs the lion.
("dog" "needs" "lion" "+")
int1
The lion does not see the bear.
False
2
inv-proof
[(((triple5) -> rule1))]
("lion" "sees" "bear" "-")
((triple5) -> (rule1 % int1))
The lion sees the bear.
("lion" "sees" "bear" "+")
int1
The bear is not big.
Unknown
inv-rconc
[@1: The bear is big.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("bear" "is" "big" "-")
The squirrel is big.
Unknown
rconc
[@1: The squirrel is big.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("squirrel" "is" "big" "+")
The dog does not like the bear.
Unknown
inv-random
[@0: The dog likes the bear.[CWA. Example of deepest failure = (FAIL)]]
("dog" "likes" "bear" "-")
The squirrel is kind.
Unknown
random
[@0: The squirrel is kind.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "kind" "+")
@0: The bear sees the dog.[(triple1)] The bear sees the lion.[(triple2)] The dog is big.[(triple3)] The dog sees the lion.[(triple4)] The lion likes the dog.[(triple5)] The squirrel is rough.[(triple6)] The squirrel needs the bear.[(triple7)] @1: The dog needs the lion.[(((triple5) -> rule3))] The lion sees the bear.[(((triple5) -> rule1))]
The bear sees the dog.
("bear" "sees" "dog" "+")
triple1
The bear sees the lion.
("bear" "sees" "lion" "+")
triple2
The dog is big.
("dog" "is" "big" "+")
triple3
The dog sees the lion.
("dog" "sees" "lion" "+")
triple4
The lion likes the dog.
("lion" "likes" "dog" "+")
triple5
The squirrel is rough.
("squirrel" "is" "rough" "+")
triple6
The squirrel needs the bear.
("squirrel" "needs" "bear" "+")
triple7
The dog needs the lion.
("dog" "needs" "lion" "+")
((triple5) -> (rule3 % int1))
The dog needs the lion.
("dog" "needs" "lion" "+")
int1
The lion sees the bear.
("lion" "sees" "bear" "+")
((triple5) -> (rule1 % int1))
The lion sees the bear.
("lion" "sees" "bear" "+")
int1