The bear is cold. The bear sees the lion. The bear visits the rabbit. The lion is cold. The lion needs the bear. The rabbit is cold. The rabbit is round. The rabbit is young. The rabbit needs the bear. The squirrel visits the rabbit. If something is green and it does not see the squirrel then it sees the bear. All young things are not kind.
The bear is cold.
("bear" "is" "cold" "+")
The bear sees the lion.
("bear" "sees" "lion" "+")
The bear visits the rabbit.
("bear" "visits" "rabbit" "+")
The lion is cold.
("lion" "is" "cold" "+")
The lion needs the bear.
("lion" "needs" "bear" "+")
The rabbit is cold.
("rabbit" "is" "cold" "+")
The rabbit is round.
("rabbit" "is" "round" "+")
The rabbit is young.
("rabbit" "is" "young" "+")
The rabbit needs the bear.
("rabbit" "needs" "bear" "+")
The squirrel visits the rabbit.
("squirrel" "visits" "rabbit" "+")
If something is green and it does not see the squirrel then it sees the bear.
((("something" "is" "green" "+") ("something" "sees" "squirrel" "~")) -> ("something" "sees" "bear" "+"))
All young things are not kind.
((("something" "is" "young" "+")) -> ("something" "is" "kind" "-"))
The lion is cold.
True
1
proof
[(triple4)]
("lion" "is" "cold" "+")
triple4
The bear does not visit the rabbit.
False
1
inv-proof
[(triple3)]
("bear" "visits" "rabbit" "-")
triple3
The rabbit is not kind.
True
2
proof
[(((triple8) -> rule2))]
("rabbit" "is" "kind" "-")
((triple8) -> (rule2 % int1))
The rabbit is not kind.
("rabbit" "is" "kind" "-")
int1
The rabbit is kind.
False
2
inv-proof
[(((triple8) -> rule2))]
("rabbit" "is" "kind" "+")
((triple8) -> (rule2 % int1))
The rabbit is not kind.
("rabbit" "is" "kind" "-")
int1
The rabbit does not see the bear.
Unknown
inv-rconc
[@1: The rabbit sees the bear.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("rabbit" "sees" "bear" "-")
The lion sees the bear.
Unknown
rconc
[@1: The lion sees the bear.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("lion" "sees" "bear" "+")
The rabbit does not visit the squirrel.
Unknown
inv-random
[@0: The rabbit visits the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "visits" "squirrel" "-")
The squirrel sees the squirrel.
Unknown
random
[@0: The squirrel sees the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "sees" "squirrel" "+")
@0: The bear is cold.[(triple1)] The bear sees the lion.[(triple2)] The bear visits the rabbit.[(triple3)] The lion is cold.[(triple4)] The lion needs the bear.[(triple5)] The rabbit is cold.[(triple6)] The rabbit is round.[(triple7)] The rabbit is young.[(triple8)] The rabbit needs the bear.[(triple9)] The squirrel visits the rabbit.[(triple10)] @1: The rabbit is not kind.[(((triple8) -> rule2))]
The bear is cold.
("bear" "is" "cold" "+")
triple1
The bear sees the lion.
("bear" "sees" "lion" "+")
triple2
The bear visits the rabbit.
("bear" "visits" "rabbit" "+")
triple3
The lion is cold.
("lion" "is" "cold" "+")
triple4
The lion needs the bear.
("lion" "needs" "bear" "+")
triple5
The rabbit is cold.
("rabbit" "is" "cold" "+")
triple6
The rabbit is round.
("rabbit" "is" "round" "+")
triple7
The rabbit is young.
("rabbit" "is" "young" "+")
triple8
The rabbit needs the bear.
("rabbit" "needs" "bear" "+")
triple9
The squirrel visits the rabbit.
("squirrel" "visits" "rabbit" "+")
triple10
The rabbit is not kind.
("rabbit" "is" "kind" "-")
((triple8) -> (rule2 % int1))
The rabbit is not kind.
("rabbit" "is" "kind" "-")
int1