The bear is nice. The bear visits the rabbit. The cow chases the bear. The cow is not kind. The cow is not nice. The mouse visits the cow. The rabbit chases the mouse. The rabbit is cold. The rabbit is nice. The rabbit likes the cow. If someone is blue then they do not visit the cow. If someone chases the bear then they like the cow. If someone likes the cow and they are not nice then the cow is blue. If someone is cold then they chase the bear. If someone chases the bear and the bear is blue then the bear visits the mouse. If someone visits the mouse and they are not nice then the mouse chases the cow. If someone chases the mouse then the mouse does not visit the rabbit. If someone is blue and they do not chase the cow then they visit the rabbit.
The bear is nice.
("bear" "is" "nice" "+")
The bear visits the rabbit.
("bear" "visits" "rabbit" "+")
The cow chases the bear.
("cow" "chases" "bear" "+")
The cow is not kind.
("cow" "is" "kind" "-")
The cow is not nice.
("cow" "is" "nice" "-")
The mouse visits the cow.
("mouse" "visits" "cow" "+")
The rabbit chases the mouse.
("rabbit" "chases" "mouse" "+")
The rabbit is cold.
("rabbit" "is" "cold" "+")
The rabbit is nice.
("rabbit" "is" "nice" "+")
The rabbit likes the cow.
("rabbit" "likes" "cow" "+")
If someone is blue then they do not visit the cow.
((("someone" "is" "blue" "+")) -> ("someone" "visits" "cow" "-"))
If someone chases the bear then they like the cow.
((("someone" "chases" "bear" "+")) -> ("someone" "likes" "cow" "+"))
If someone likes the cow and they are not nice then the cow is blue.
((("someone" "likes" "cow" "+") ("someone" "is" "nice" "~")) -> ("cow" "is" "blue" "+"))
If someone is cold then they chase the bear.
((("someone" "is" "cold" "+")) -> ("someone" "chases" "bear" "+"))
If someone chases the bear and the bear is blue then the bear visits the mouse.
((("someone" "chases" "bear" "+") ("bear" "is" "blue" "+")) -> ("bear" "visits" "mouse" "+"))
If someone visits the mouse and they are not nice then the mouse chases the cow.
((("someone" "visits" "mouse" "+") ("someone" "is" "nice" "~")) -> ("mouse" "chases" "cow" "+"))
If someone chases the mouse then the mouse does not visit the rabbit.
((("someone" "chases" "mouse" "+")) -> ("mouse" "visits" "rabbit" "-"))
If someone is blue and they do not chase the cow then they visit the rabbit.
((("someone" "is" "blue" "+") ("someone" "chases" "cow" "~")) -> ("someone" "visits" "rabbit" "+"))
The cow is not nice.
True
1
proof
[(triple5)]
("cow" "is" "nice" "-")
triple5
The bear is not nice.
False
1
inv-proof
[(triple1)]
("bear" "is" "nice" "-")
triple1
The rabbit chases the bear.
True
2
proof
[(((triple8) -> rule4))]
("rabbit" "chases" "bear" "+")
((triple8) -> (rule4 % int1))
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
int1
The mouse visits the rabbit.
False
2
inv-proof
[(((triple7) -> rule7))]
("mouse" "visits" "rabbit" "+")
((triple7) -> (rule7 % int1))
The mouse does not visit the rabbit.
("mouse" "visits" "rabbit" "-")
int1
The cow is blue.
True
4
proof
[(((((triple3) -> rule2) triple5) -> rule3))]
("cow" "is" "blue" "+")
((((triple3) -> (rule2 % int2)) triple5) -> (rule3 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
The cow likes the cow.
("cow" "likes" "cow" "+")
int2
The cow is not blue.
False
4
inv-proof
[(((((triple3) -> rule2) triple5) -> rule3))]
("cow" "is" "blue" "-")
((((triple3) -> (rule2 % int2)) triple5) -> (rule3 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
The cow likes the cow.
("cow" "likes" "cow" "+")
int2
The cow does not visit the cow.
True
5
proof
[(((((((triple3) -> rule2) triple5) -> rule3)) -> rule1))]
("cow" "visits" "cow" "-")
((((((triple3) -> (rule2 % int3)) triple5) -> (rule3 % int2))) -> (rule1 % int1))
The cow does not visit the cow.
("cow" "visits" "cow" "-")
int1
The cow is blue.
("cow" "is" "blue" "+")
int2
The cow likes the cow.
("cow" "likes" "cow" "+")
int3
The cow visits the cow.
False
5
inv-proof
[(((((((triple3) -> rule2) triple5) -> rule3)) -> rule1))]
("cow" "visits" "cow" "+")
((((((triple3) -> (rule2 % int3)) triple5) -> (rule3 % int2))) -> (rule1 % int1))
The cow does not visit the cow.
("cow" "visits" "cow" "-")
int1
The cow is blue.
("cow" "is" "blue" "+")
int2
The cow likes the cow.
("cow" "likes" "cow" "+")
int3
The bear does not like the cow.
Unknown
inv-rconc
[@2: The bear likes the cow.[CWA. Example of deepest failure = (rule2 <- rule4 <- FAIL)]]
("bear" "likes" "cow" "-")
The bear visits the mouse.
Unknown
rconc
[@1: The bear visits the mouse.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("bear" "visits" "mouse" "+")
The mouse does not like the cow.
Unknown
inv-rconc
[@2: The mouse likes the cow.[CWA. Example of deepest failure = (rule2 <- rule4 <- FAIL)]]
("mouse" "likes" "cow" "-")
The rabbit visits the rabbit.
Unknown
rconc
[@1: The rabbit visits the rabbit.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("rabbit" "visits" "rabbit" "+")
The rabbit does not like the mouse.
Unknown
inv-random
[@0: The rabbit likes the mouse.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "likes" "mouse" "-")
The rabbit likes the rabbit.
Unknown
random
[@0: The rabbit likes the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "likes" "rabbit" "+")
The rabbit is not rough.
Unknown
inv-random
[@0: The rabbit is rough.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "rough" "-")
The bear is cold.
Unknown
random
[@0: The bear is cold.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "cold" "+")
@0: The bear is nice.[(triple1)] The bear visits the rabbit.[(triple2)] The cow chases the bear.[(triple3)] The cow is not kind.[(triple4)] The cow is not nice.[(triple5)] The mouse visits the cow.[(triple6)] The rabbit chases the mouse.[(triple7)] The rabbit is cold.[(triple8)] The rabbit is nice.[(triple9)] The rabbit likes the cow.[(triple10 OR ((((triple8) -> rule4)) -> rule2))] @1: The cow likes the cow.[(((triple3) -> rule2))] The mouse does not visit the rabbit.[(((triple7) -> rule7))] The rabbit chases the bear.[(((triple8) -> rule4))] @2: The cow is blue.[(((((triple3) -> rule2) triple5) -> rule3))] @3: The cow does not visit the cow.[(((((((triple3) -> rule2) triple5) -> rule3)) -> rule1))]
The bear is nice.
("bear" "is" "nice" "+")
triple1
The bear visits the rabbit.
("bear" "visits" "rabbit" "+")
triple2
The cow chases the bear.
("cow" "chases" "bear" "+")
triple3
The cow is not kind.
("cow" "is" "kind" "-")
triple4
The cow is not nice.
("cow" "is" "nice" "-")
triple5
The mouse visits the cow.
("mouse" "visits" "cow" "+")
triple6
The rabbit chases the mouse.
("rabbit" "chases" "mouse" "+")
triple7
The rabbit is cold.
("rabbit" "is" "cold" "+")
triple8
The rabbit is nice.
("rabbit" "is" "nice" "+")
triple9
The rabbit likes the cow.
("rabbit" "likes" "cow" "+")
triple10
((((triple8) -> (rule4 % int2))) -> (rule2 % int1))
The rabbit likes the cow.
("rabbit" "likes" "cow" "+")
int1
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
int2
The cow likes the cow.
("cow" "likes" "cow" "+")
((triple3) -> (rule2 % int1))
The cow likes the cow.
("cow" "likes" "cow" "+")
int1
The mouse does not visit the rabbit.
("mouse" "visits" "rabbit" "-")
((triple7) -> (rule7 % int1))
The mouse does not visit the rabbit.
("mouse" "visits" "rabbit" "-")
int1
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
((triple8) -> (rule4 % int1))
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
int1
The cow is blue.
("cow" "is" "blue" "+")
((((triple3) -> (rule2 % int2)) triple5) -> (rule3 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
The cow likes the cow.
("cow" "likes" "cow" "+")
int2
The cow does not visit the cow.
("cow" "visits" "cow" "-")
((((((triple3) -> (rule2 % int3)) triple5) -> (rule3 % int2))) -> (rule1 % int1))
The cow does not visit the cow.
("cow" "visits" "cow" "-")
int1
The cow is blue.
("cow" "is" "blue" "+")
int2
The cow likes the cow.
("cow" "likes" "cow" "+")
int3