The bear is round. The lion likes the bear. The rabbit visits the lion. If something likes the lion then it visits the rabbit. If something eats the bear then the bear is big. If the lion visits the rabbit and the lion eats the rabbit then the lion eats the bear. If something likes the bear then it is big. If the lion visits the rabbit and the lion likes the rabbit then the lion eats the bear. Kind, rough things are big.
The bear is round.
("bear" "is" "round" "+")
The lion likes the bear.
("lion" "likes" "bear" "+")
The rabbit visits the lion.
("rabbit" "visits" "lion" "+")
If something likes the lion then it visits the rabbit.
((("something" "likes" "lion" "+")) -> ("something" "visits" "rabbit" "+"))
If something eats the bear then the bear is big.
((("something" "eats" "bear" "+")) -> ("bear" "is" "big" "+"))
If the lion visits the rabbit and the lion eats the rabbit then the lion eats the bear.
((("lion" "visits" "rabbit" "+") ("lion" "eats" "rabbit" "+")) -> ("lion" "eats" "bear" "+"))
If something likes the bear then it is big.
((("something" "likes" "bear" "+")) -> ("something" "is" "big" "+"))
If the lion visits the rabbit and the lion likes the rabbit then the lion eats the bear.
((("lion" "visits" "rabbit" "+") ("lion" "likes" "rabbit" "+")) -> ("lion" "eats" "bear" "+"))
Kind, rough things are big.
((("something" "is" "kind" "+") ("something" "is" "rough" "+")) -> ("something" "is" "big" "+"))
The lion likes the bear.
True
1
proof
[(triple2)]
("lion" "likes" "bear" "+")
triple2
The lion does not like the bear.
False
1
inv-proof
[(triple2)]
("lion" "likes" "bear" "-")
triple2
The lion is big.
True
2
proof
[(((triple2) -> rule4))]
("lion" "is" "big" "+")
((triple2) -> (rule4 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The lion is not big.
False
2
inv-proof
[(((triple2) -> rule4))]
("lion" "is" "big" "-")
((triple2) -> (rule4 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The rabbit does not visit the rabbit.
Unknown
inv-rconc
[@1: The rabbit visits the rabbit.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("rabbit" "visits" "rabbit" "-")
The bear visits the rabbit.
Unknown
rconc
[@1: The bear visits the rabbit.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("bear" "visits" "rabbit" "+")
The lion is not rough.
Unknown
inv-random
[@0: The lion is rough.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "rough" "-")
The rabbit eats the lion.
Unknown
random
[@0: The rabbit eats the lion.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "eats" "lion" "+")
@0: The bear is round.[(triple1)] The lion likes the bear.[(triple2)] The rabbit visits the lion.[(triple3)] @1: The lion is big.[(((triple2) -> rule4))]
The bear is round.
("bear" "is" "round" "+")
triple1
The lion likes the bear.
("lion" "likes" "bear" "+")
triple2
The rabbit visits the lion.
("rabbit" "visits" "lion" "+")
triple3
The lion is big.
("lion" "is" "big" "+")
((triple2) -> (rule4 % int1))
The lion is big.
("lion" "is" "big" "+")
int1