The bear is green. The bear likes the rabbit. The bear sees the rabbit. The rabbit is green. The rabbit is nice. The rabbit is red. The squirrel is green. The squirrel is nice. The squirrel is red. The squirrel likes the bear. The squirrel likes the rabbit. The squirrel sees the bear. If something is green and it sees the squirrel then it is not nice. If something visits the rabbit then the rabbit is not blue. If something sees the bear then it is not blue. If something is nice and it does not like the squirrel then it sees the squirrel. If something visits the rabbit then the rabbit visits the bear. If something sees the squirrel then it visits the bear.
The bear is green.
("bear" "is" "green" "+")
The bear likes the rabbit.
("bear" "likes" "rabbit" "+")
The bear sees the rabbit.
("bear" "sees" "rabbit" "+")
The rabbit is green.
("rabbit" "is" "green" "+")
The rabbit is nice.
("rabbit" "is" "nice" "+")
The rabbit is red.
("rabbit" "is" "red" "+")
The squirrel is green.
("squirrel" "is" "green" "+")
The squirrel is nice.
("squirrel" "is" "nice" "+")
The squirrel is red.
("squirrel" "is" "red" "+")
The squirrel likes the bear.
("squirrel" "likes" "bear" "+")
The squirrel likes the rabbit.
("squirrel" "likes" "rabbit" "+")
The squirrel sees the bear.
("squirrel" "sees" "bear" "+")
If something is green and it sees the squirrel then it is not nice.
((("something" "is" "green" "+") ("something" "sees" "squirrel" "+")) -> ("something" "is" "nice" "-"))
If something visits the rabbit then the rabbit is not blue.
((("something" "visits" "rabbit" "+")) -> ("rabbit" "is" "blue" "-"))
If something sees the bear then it is not blue.
((("something" "sees" "bear" "+")) -> ("something" "is" "blue" "-"))
If something is nice and it does not like the squirrel then it sees the squirrel.
((("something" "is" "nice" "+") ("something" "likes" "squirrel" "~")) -> ("something" "sees" "squirrel" "+"))
If something visits the rabbit then the rabbit visits the bear.
((("something" "visits" "rabbit" "+")) -> ("rabbit" "visits" "bear" "+"))
If something sees the squirrel then it visits the bear.
((("something" "sees" "squirrel" "+")) -> ("something" "visits" "bear" "+"))
The rabbit is green.
True
1
proof
[(triple4)]
("rabbit" "is" "green" "+")
triple4
The squirrel does not like the bear.
False
1
inv-proof
[(triple10)]
("squirrel" "likes" "bear" "-")
triple10
The squirrel is not blue.
True
2
proof
[(((triple12) -> rule3))]
("squirrel" "is" "blue" "-")
((triple12) -> (rule3 % int1))
The squirrel is not blue.
("squirrel" "is" "blue" "-")
int1
The squirrel is blue.
False
2
inv-proof
[(((triple12) -> rule3))]
("squirrel" "is" "blue" "+")
((triple12) -> (rule3 % int1))
The squirrel is not blue.
("squirrel" "is" "blue" "-")
int1
The squirrel does not visit the bear.
Unknown
inv-rconc
[@2: The squirrel visits the bear.[CWA. Example of deepest failure = (rule6 <- rule4 <- FAIL)]]
("squirrel" "visits" "bear" "-")
The squirrel sees the squirrel.
Unknown
rconc
[@1: The squirrel sees the squirrel.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("squirrel" "sees" "squirrel" "+")
The squirrel is not cold.
Unknown
inv-random
[@0: The squirrel is cold.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "cold" "-")
The bear visits the squirrel.
Unknown
random
[@0: The bear visits the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("bear" "visits" "squirrel" "+")
@0: The bear is green.[(triple1)] The bear likes the rabbit.[(triple2)] The bear sees the rabbit.[(triple3)] The rabbit is green.[(triple4)] The rabbit is nice.[(triple5)] The rabbit is red.[(triple6)] The squirrel is green.[(triple7)] The squirrel is nice.[(triple8)] The squirrel is red.[(triple9)] The squirrel likes the bear.[(triple10)] The squirrel likes the rabbit.[(triple11)] The squirrel sees the bear.[(triple12)] @1: The squirrel is not blue.[(((triple12) -> rule3))]
The bear is green.
("bear" "is" "green" "+")
triple1
The bear likes the rabbit.
("bear" "likes" "rabbit" "+")
triple2
The bear sees the rabbit.
("bear" "sees" "rabbit" "+")
triple3
The rabbit is green.
("rabbit" "is" "green" "+")
triple4
The rabbit is nice.
("rabbit" "is" "nice" "+")
triple5
The rabbit is red.
("rabbit" "is" "red" "+")
triple6
The squirrel is green.
("squirrel" "is" "green" "+")
triple7
The squirrel is nice.
("squirrel" "is" "nice" "+")
triple8
The squirrel is red.
("squirrel" "is" "red" "+")
triple9
The squirrel likes the bear.
("squirrel" "likes" "bear" "+")
triple10
The squirrel likes the rabbit.
("squirrel" "likes" "rabbit" "+")
triple11
The squirrel sees the bear.
("squirrel" "sees" "bear" "+")
triple12
The squirrel is not blue.
("squirrel" "is" "blue" "-")
((triple12) -> (rule3 % int1))
The squirrel is not blue.
("squirrel" "is" "blue" "-")
int1