The cow is not rough. The cow likes the lion. The cow does not like the rabbit. The cow needs the rabbit. The cow does not visit the lion. The cow visits the rabbit. The lion does not need the cow. The rabbit is not rough. The rabbit likes the lion. The rabbit needs the lion. The rabbit visits the cow. The rabbit visits the lion. If something visits the lion and the lion likes the cow then the lion is not cold. If something is green then it is cold. If something needs the lion then the lion likes the cow.
The cow is not rough.
("cow" "is" "rough" "-")
The cow likes the lion.
("cow" "likes" "lion" "+")
The cow does not like the rabbit.
("cow" "likes" "rabbit" "-")
The cow needs the rabbit.
("cow" "needs" "rabbit" "+")
The cow does not visit the lion.
("cow" "visits" "lion" "-")
The cow visits the rabbit.
("cow" "visits" "rabbit" "+")
The lion does not need the cow.
("lion" "needs" "cow" "-")
The rabbit is not rough.
("rabbit" "is" "rough" "-")
The rabbit likes the lion.
("rabbit" "likes" "lion" "+")
The rabbit needs the lion.
("rabbit" "needs" "lion" "+")
The rabbit visits the cow.
("rabbit" "visits" "cow" "+")
The rabbit visits the lion.
("rabbit" "visits" "lion" "+")
If something visits the lion and the lion likes the cow then the lion is not cold.
((("something" "visits" "lion" "+") ("lion" "likes" "cow" "+")) -> ("lion" "is" "cold" "-"))
If something is green then it is cold.
((("something" "is" "green" "+")) -> ("something" "is" "cold" "+"))
If something needs the lion then the lion likes the cow.
((("something" "needs" "lion" "+")) -> ("lion" "likes" "cow" "+"))
The cow needs the rabbit.
True
1
proof
[(triple4)]
("cow" "needs" "rabbit" "+")
triple4
The rabbit does not like the lion.
False
1
inv-proof
[(triple9)]
("rabbit" "likes" "lion" "-")
triple9
The lion likes the cow.
True
2
proof
[(((triple10) -> rule3))]
("lion" "likes" "cow" "+")
((triple10) -> (rule3 % int1))
The lion likes the cow.
("lion" "likes" "cow" "+")
int1
The lion does not like the cow.
False
2
inv-proof
[(((triple10) -> rule3))]
("lion" "likes" "cow" "-")
((triple10) -> (rule3 % int1))
The lion likes the cow.
("lion" "likes" "cow" "+")
int1
The lion is not cold.
True
4
proof
[(((triple12 ((triple10) -> rule3)) -> rule1))]
("lion" "is" "cold" "-")
((triple12 ((triple10) -> (rule3 % int2))) -> (rule1 % int1))
The lion is not cold.
("lion" "is" "cold" "-")
int1
The lion likes the cow.
("lion" "likes" "cow" "+")
int2
The lion is cold.
False
4
inv-proof
[(((triple12 ((triple10) -> rule3)) -> rule1))]
("lion" "is" "cold" "+")
((triple12 ((triple10) -> (rule3 % int2))) -> (rule1 % int1))
The lion is not cold.
("lion" "is" "cold" "-")
int1
The lion likes the cow.
("lion" "likes" "cow" "+")
int2
The rabbit is not cold.
Unknown
inv-rconc
[@1: The rabbit is cold.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("rabbit" "is" "cold" "-")
The cow is cold.
Unknown
rconc
[@1: The cow is cold.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cow" "is" "cold" "+")
The rabbit does not need the rabbit.
Unknown
inv-random
[@0: The rabbit needs the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "needs" "rabbit" "-")
The cow is blue.
Unknown
random
[@0: The cow is blue.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "blue" "+")
The cow is not green.
Unknown
inv-random
[@0: The cow is green.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "green" "-")
The lion visits the rabbit.
Unknown
random
[@0: The lion visits the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("lion" "visits" "rabbit" "+")
@0: The cow does not like the rabbit.[(triple3)] The cow does not visit the lion.[(triple5)] The cow is not rough.[(triple1)] The cow likes the lion.[(triple2)] The cow needs the rabbit.[(triple4)] The cow visits the rabbit.[(triple6)] The lion does not need the cow.[(triple7)] The rabbit is not rough.[(triple8)] The rabbit likes the lion.[(triple9)] The rabbit needs the lion.[(triple10)] The rabbit visits the cow.[(triple11)] The rabbit visits the lion.[(triple12)] @1: The lion likes the cow.[(((triple10) -> rule3))] @2: The lion is not cold.[(((triple12 ((triple10) -> rule3)) -> rule1))]
The cow does not like the rabbit.
("cow" "likes" "rabbit" "-")
triple3
The cow does not visit the lion.
("cow" "visits" "lion" "-")
triple5
The cow is not rough.
("cow" "is" "rough" "-")
triple1
The cow likes the lion.
("cow" "likes" "lion" "+")
triple2
The cow needs the rabbit.
("cow" "needs" "rabbit" "+")
triple4
The cow visits the rabbit.
("cow" "visits" "rabbit" "+")
triple6
The lion does not need the cow.
("lion" "needs" "cow" "-")
triple7
The rabbit is not rough.
("rabbit" "is" "rough" "-")
triple8
The rabbit likes the lion.
("rabbit" "likes" "lion" "+")
triple9
The rabbit needs the lion.
("rabbit" "needs" "lion" "+")
triple10
The rabbit visits the cow.
("rabbit" "visits" "cow" "+")
triple11
The rabbit visits the lion.
("rabbit" "visits" "lion" "+")
triple12
The lion likes the cow.
("lion" "likes" "cow" "+")
((triple10) -> (rule3 % int1))
The lion likes the cow.
("lion" "likes" "cow" "+")
int1
The lion is not cold.
("lion" "is" "cold" "-")
((triple12 ((triple10) -> (rule3 % int2))) -> (rule1 % int1))
The lion is not cold.
("lion" "is" "cold" "-")
int1
The lion likes the cow.
("lion" "likes" "cow" "+")
int2