The bear eats the rabbit. The bear is round. The bear likes the rabbit. The cow does not eat the bear. The cow visits the bear. The rabbit likes the bear. The squirrel visits the rabbit. If something is round and it likes the rabbit then it visits the rabbit. If the bear eats the cow then the bear is rough. If the bear visits the rabbit and the rabbit visits the squirrel then the bear is cold. If something is cold then it visits the cow. If something likes the squirrel and the squirrel is not rough then it is not cold. If something is rough then it eats the rabbit.
The bear eats the rabbit.
("bear" "eats" "rabbit" "+")
The bear is round.
("bear" "is" "round" "+")
The bear likes the rabbit.
("bear" "likes" "rabbit" "+")
The cow does not eat the bear.
("cow" "eats" "bear" "-")
The cow visits the bear.
("cow" "visits" "bear" "+")
The rabbit likes the bear.
("rabbit" "likes" "bear" "+")
The squirrel visits the rabbit.
("squirrel" "visits" "rabbit" "+")
If something is round and it likes the rabbit then it visits the rabbit.
((("something" "is" "round" "+") ("something" "likes" "rabbit" "+")) -> ("something" "visits" "rabbit" "+"))
If the bear eats the cow then the bear is rough.
((("bear" "eats" "cow" "+")) -> ("bear" "is" "rough" "+"))
If the bear visits the rabbit and the rabbit visits the squirrel then the bear is cold.
((("bear" "visits" "rabbit" "+") ("rabbit" "visits" "squirrel" "+")) -> ("bear" "is" "cold" "+"))
If something is cold then it visits the cow.
((("something" "is" "cold" "+")) -> ("something" "visits" "cow" "+"))
If something likes the squirrel and the squirrel is not rough then it is not cold.
((("something" "likes" "squirrel" "+") ("squirrel" "is" "rough" "~")) -> ("something" "is" "cold" "-"))
If something is rough then it eats the rabbit.
((("something" "is" "rough" "+")) -> ("something" "eats" "rabbit" "+"))
The bear is round.
True
1
proof
[(triple2)]
("bear" "is" "round" "+")
triple2
The rabbit does not like the bear.
False
1
inv-proof
[(triple6)]
("rabbit" "likes" "bear" "-")
triple6
The bear visits the rabbit.
True
3
proof
[(((triple2 triple3) -> rule1))]
("bear" "visits" "rabbit" "+")
((triple2 triple3) -> (rule1 % int1))
The bear visits the rabbit.
("bear" "visits" "rabbit" "+")
int1
The bear does not visit the rabbit.
False
3
inv-proof
[(((triple2 triple3) -> rule1))]
("bear" "visits" "rabbit" "-")
((triple2 triple3) -> (rule1 % int1))
The bear visits the rabbit.
("bear" "visits" "rabbit" "+")
int1
The squirrel does not eat the rabbit.
Unknown
inv-rconc
[@1: The squirrel eats the rabbit.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("squirrel" "eats" "rabbit" "-")
The rabbit visits the cow.
Unknown
rconc
[@1: The rabbit visits the cow.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("rabbit" "visits" "cow" "+")
The cow is not young.
Unknown
inv-random
[@0: The cow is young.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "young" "-")
The cow likes the squirrel.
Unknown
random
[@0: The cow likes the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("cow" "likes" "squirrel" "+")
@0: The bear eats the rabbit.[(triple1)] The bear is round.[(triple2)] The bear likes the rabbit.[(triple3)] The cow does not eat the bear.[(triple4)] The cow visits the bear.[(triple5)] The rabbit likes the bear.[(triple6)] The squirrel visits the rabbit.[(triple7)] @1: The bear visits the rabbit.[(((triple2 triple3) -> rule1))]
The bear eats the rabbit.
("bear" "eats" "rabbit" "+")
triple1
The bear is round.
("bear" "is" "round" "+")
triple2
The bear likes the rabbit.
("bear" "likes" "rabbit" "+")
triple3
The cow does not eat the bear.
("cow" "eats" "bear" "-")
triple4
The cow visits the bear.
("cow" "visits" "bear" "+")
triple5
The rabbit likes the bear.
("rabbit" "likes" "bear" "+")
triple6
The squirrel visits the rabbit.
("squirrel" "visits" "rabbit" "+")
triple7
The bear visits the rabbit.
("bear" "visits" "rabbit" "+")
((triple2 triple3) -> (rule1 % int1))
The bear visits the rabbit.
("bear" "visits" "rabbit" "+")
int1