The bear is blue. The bear likes the rabbit. The cow is nice. The cow likes the rabbit. The cow sees the lion. The cow does not see the rabbit. The cow visits the lion. The lion is blue. The lion is kind. The lion sees the bear. The rabbit is nice. The rabbit does not visit the lion. If something is blue and it visits the lion then it does not see the rabbit. If something likes the cow then it sees the rabbit. If something sees the cow then the cow does not like the lion. If the rabbit sees the lion and the rabbit does not like the bear then the bear sees the lion. If something sees the bear and it sees the rabbit then the bear does not visit the lion. If something sees the bear and the bear is young then the bear visits the rabbit. If something is blue and young then it sees the cow. If something is kind then it is young.
The bear is blue.
("bear" "is" "blue" "+")
The bear likes the rabbit.
("bear" "likes" "rabbit" "+")
The cow is nice.
("cow" "is" "nice" "+")
The cow likes the rabbit.
("cow" "likes" "rabbit" "+")
The cow sees the lion.
("cow" "sees" "lion" "+")
The cow does not see the rabbit.
("cow" "sees" "rabbit" "-")
The cow visits the lion.
("cow" "visits" "lion" "+")
The lion is blue.
("lion" "is" "blue" "+")
The lion is kind.
("lion" "is" "kind" "+")
The lion sees the bear.
("lion" "sees" "bear" "+")
The rabbit is nice.
("rabbit" "is" "nice" "+")
The rabbit does not visit the lion.
("rabbit" "visits" "lion" "-")
If something is blue and it visits the lion then it does not see the rabbit.
((("something" "is" "blue" "+") ("something" "visits" "lion" "+")) -> ("something" "sees" "rabbit" "-"))
If something likes the cow then it sees the rabbit.
((("something" "likes" "cow" "+")) -> ("something" "sees" "rabbit" "+"))
If something sees the cow then the cow does not like the lion.
((("something" "sees" "cow" "+")) -> ("cow" "likes" "lion" "-"))
If the rabbit sees the lion and the rabbit does not like the bear then the bear sees the lion.
((("rabbit" "sees" "lion" "+") ("rabbit" "likes" "bear" "~")) -> ("bear" "sees" "lion" "+"))
If something sees the bear and it sees the rabbit then the bear does not visit the lion.
((("something" "sees" "bear" "+") ("something" "sees" "rabbit" "+")) -> ("bear" "visits" "lion" "-"))
If something sees the bear and the bear is young then the bear visits the rabbit.
((("something" "sees" "bear" "+") ("bear" "is" "young" "+")) -> ("bear" "visits" "rabbit" "+"))
If something is blue and young then it sees the cow.
((("something" "is" "blue" "+") ("something" "is" "young" "+")) -> ("something" "sees" "cow" "+"))
If something is kind then it is young.
((("something" "is" "kind" "+")) -> ("something" "is" "young" "+"))
The cow sees the lion.
True
1
proof
[(triple5)]
("cow" "sees" "lion" "+")
triple5
The cow does not visit the lion.
False
1
inv-proof
[(triple7)]
("cow" "visits" "lion" "-")
triple7
The lion is young.
True
2
proof
[(((triple9) -> rule8))]
("lion" "is" "young" "+")
((triple9) -> (rule8 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
The lion is not young.
False
2
inv-proof
[(((triple9) -> rule8))]
("lion" "is" "young" "-")
((triple9) -> (rule8 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
The lion sees the cow.
True
4
proof
[(((triple8 ((triple9) -> rule8)) -> rule7))]
("lion" "sees" "cow" "+")
((triple8 ((triple9) -> (rule8 % int2))) -> (rule7 % int1))
The lion sees the cow.
("lion" "sees" "cow" "+")
int1
The lion is young.
("lion" "is" "young" "+")
int2
The lion does not see the cow.
False
4
inv-proof
[(((triple8 ((triple9) -> rule8)) -> rule7))]
("lion" "sees" "cow" "-")
((triple8 ((triple9) -> (rule8 % int2))) -> (rule7 % int1))
The lion sees the cow.
("lion" "sees" "cow" "+")
int1
The lion is young.
("lion" "is" "young" "+")
int2
The cow does not like the lion.
True
5
proof
[(((((triple8 ((triple9) -> rule8)) -> rule7)) -> rule3))]
("cow" "likes" "lion" "-")
((((triple8 ((triple9) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule3 % int1))
The cow does not like the lion.
("cow" "likes" "lion" "-")
int1
The lion sees the cow.
("lion" "sees" "cow" "+")
int2
The lion is young.
("lion" "is" "young" "+")
int3
The cow likes the lion.
False
5
inv-proof
[(((((triple8 ((triple9) -> rule8)) -> rule7)) -> rule3))]
("cow" "likes" "lion" "+")
((((triple8 ((triple9) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule3 % int1))
The cow does not like the lion.
("cow" "likes" "lion" "-")
int1
The lion sees the cow.
("lion" "sees" "cow" "+")
int2
The lion is young.
("lion" "is" "young" "+")
int3
The rabbit does not see the rabbit.
Unknown
inv-rconc
[@1: The rabbit sees the rabbit.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("rabbit" "sees" "rabbit" "-")
The bear is young.
Unknown
rconc
[@1: The bear is young.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("bear" "is" "young" "+")
The bear does not visit the rabbit.
Unknown
inv-rconc
[@2: The bear visits the rabbit.[CWA. Example of deepest failure = (rule6 <- rule8 <- FAIL)]]
("bear" "visits" "rabbit" "-")
The bear sees the lion.
Unknown
rconc
[@1: The bear sees the lion.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("bear" "sees" "lion" "+")
The rabbit does not visit the cow.
Unknown
inv-random
[@0: The rabbit visits the cow.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "visits" "cow" "-")
The bear is kind.
Unknown
random
[@0: The bear is kind.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "kind" "+")
The cow does not visit the cow.
Unknown
inv-random
[@0: The cow visits the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "visits" "cow" "-")
The cow likes the cow.
Unknown
random
[@0: The cow likes the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "likes" "cow" "+")
@0: The bear is blue.[(triple1)] The bear likes the rabbit.[(triple2)] The cow does not see the rabbit.[(triple6)] The cow is nice.[(triple3)] The cow likes the rabbit.[(triple4)] The cow sees the lion.[(triple5)] The cow visits the lion.[(triple7)] The lion is blue.[(triple8)] The lion is kind.[(triple9)] The lion sees the bear.[(triple10)] The rabbit does not visit the lion.[(triple12)] The rabbit is nice.[(triple11)] @1: The lion is young.[(((triple9) -> rule8))] @2: The lion sees the cow.[(((triple8 ((triple9) -> rule8)) -> rule7))] @3: The cow does not like the lion.[(((((triple8 ((triple9) -> rule8)) -> rule7)) -> rule3))]
The bear is blue.
("bear" "is" "blue" "+")
triple1
The bear likes the rabbit.
("bear" "likes" "rabbit" "+")
triple2
The cow does not see the rabbit.
("cow" "sees" "rabbit" "-")
triple6
The cow is nice.
("cow" "is" "nice" "+")
triple3
The cow likes the rabbit.
("cow" "likes" "rabbit" "+")
triple4
The cow sees the lion.
("cow" "sees" "lion" "+")
triple5
The cow visits the lion.
("cow" "visits" "lion" "+")
triple7
The lion is blue.
("lion" "is" "blue" "+")
triple8
The lion is kind.
("lion" "is" "kind" "+")
triple9
The lion sees the bear.
("lion" "sees" "bear" "+")
triple10
The rabbit does not visit the lion.
("rabbit" "visits" "lion" "-")
triple12
The rabbit is nice.
("rabbit" "is" "nice" "+")
triple11
The lion is young.
("lion" "is" "young" "+")
((triple9) -> (rule8 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
The lion sees the cow.
("lion" "sees" "cow" "+")
((triple8 ((triple9) -> (rule8 % int2))) -> (rule7 % int1))
The lion sees the cow.
("lion" "sees" "cow" "+")
int1
The lion is young.
("lion" "is" "young" "+")
int2
The cow does not like the lion.
("cow" "likes" "lion" "-")
((((triple8 ((triple9) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule3 % int1))
The cow does not like the lion.
("cow" "likes" "lion" "-")
int1
The lion sees the cow.
("lion" "sees" "cow" "+")
int2
The lion is young.
("lion" "is" "young" "+")
int3