The bear is cold. The bear visits the dog. The dog sees the bear. The mouse is cold. The mouse visits the rabbit. The rabbit sees the mouse. The rabbit visits the bear. If something sees the dog then it is nice. If something sees the rabbit then it sees the dog. If something likes the mouse and the mouse does not visit the dog then it is round. If something is green then it likes the rabbit. If the rabbit visits the mouse then the mouse is blue. If the mouse likes the dog and the dog is cold then the mouse is blue. If something is nice then it likes the mouse. If the rabbit likes the mouse then the rabbit is not green. If something sees the mouse then it sees the rabbit.
The bear is cold.
("bear" "is" "cold" "+")
The bear visits the dog.
("bear" "visits" "dog" "+")
The dog sees the bear.
("dog" "sees" "bear" "+")
The mouse is cold.
("mouse" "is" "cold" "+")
The mouse visits the rabbit.
("mouse" "visits" "rabbit" "+")
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
The rabbit visits the bear.
("rabbit" "visits" "bear" "+")
If something sees the dog then it is nice.
((("something" "sees" "dog" "+")) -> ("something" "is" "nice" "+"))
If something sees the rabbit then it sees the dog.
((("something" "sees" "rabbit" "+")) -> ("something" "sees" "dog" "+"))
If something likes the mouse and the mouse does not visit the dog then it is round.
((("something" "likes" "mouse" "+") ("mouse" "visits" "dog" "~")) -> ("something" "is" "round" "+"))
If something is green then it likes the rabbit.
((("something" "is" "green" "+")) -> ("something" "likes" "rabbit" "+"))
If the rabbit visits the mouse then the mouse is blue.
((("rabbit" "visits" "mouse" "+")) -> ("mouse" "is" "blue" "+"))
If the mouse likes the dog and the dog is cold then the mouse is blue.
((("mouse" "likes" "dog" "+") ("dog" "is" "cold" "+")) -> ("mouse" "is" "blue" "+"))
If something is nice then it likes the mouse.
((("something" "is" "nice" "+")) -> ("something" "likes" "mouse" "+"))
If the rabbit likes the mouse then the rabbit is not green.
((("rabbit" "likes" "mouse" "+")) -> ("rabbit" "is" "green" "-"))
If something sees the mouse then it sees the rabbit.
((("something" "sees" "mouse" "+")) -> ("something" "sees" "rabbit" "+"))
The mouse visits the rabbit.
True
1
proof
[(triple5)]
("mouse" "visits" "rabbit" "+")
triple5
The mouse does not visit the rabbit.
False
1
inv-proof
[(triple5)]
("mouse" "visits" "rabbit" "-")
triple5
The rabbit sees the rabbit.
True
2
proof
[(((triple6) -> rule9))]
("rabbit" "sees" "rabbit" "+")
((triple6) -> (rule9 % int1))
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int1
The rabbit does not see the rabbit.
False
2
inv-proof
[(((triple6) -> rule9))]
("rabbit" "sees" "rabbit" "-")
((triple6) -> (rule9 % int1))
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int1
The rabbit sees the dog.
True
3
proof
[(((((triple6) -> rule9)) -> rule2))]
("rabbit" "sees" "dog" "+")
((((triple6) -> (rule9 % int2))) -> (rule2 % int1))
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
int1
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int2
The rabbit does not see the dog.
False
3
inv-proof
[(((((triple6) -> rule9)) -> rule2))]
("rabbit" "sees" "dog" "-")
((((triple6) -> (rule9 % int2))) -> (rule2 % int1))
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
int1
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int2
The rabbit is nice.
True
4
proof
[(((((((triple6) -> rule9)) -> rule2)) -> rule1))]
("rabbit" "is" "nice" "+")
((((((triple6) -> (rule9 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
The rabbit is nice.
("rabbit" "is" "nice" "+")
int1
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
int2
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int3
The rabbit is not nice.
False
4
inv-proof
[(((((((triple6) -> rule9)) -> rule2)) -> rule1))]
("rabbit" "is" "nice" "-")
((((((triple6) -> (rule9 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
The rabbit is nice.
("rabbit" "is" "nice" "+")
int1
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
int2
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int3
The rabbit likes the mouse.
True
5
proof
[(((((((((triple6) -> rule9)) -> rule2)) -> rule1)) -> rule7))]
("rabbit" "likes" "mouse" "+")
((((((((triple6) -> (rule9 % int4))) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
int1
The rabbit is nice.
("rabbit" "is" "nice" "+")
int2
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
int3
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int4
The rabbit does not like the mouse.
False
5
inv-proof
[(((((((((triple6) -> rule9)) -> rule2)) -> rule1)) -> rule7))]
("rabbit" "likes" "mouse" "-")
((((((((triple6) -> (rule9 % int4))) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
int1
The rabbit is nice.
("rabbit" "is" "nice" "+")
int2
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
int3
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int4
The rabbit is not green.
True
6
proof
[(((((((((((triple6) -> rule9)) -> rule2)) -> rule1)) -> rule7)) -> rule8))]
("rabbit" "is" "green" "-")
((((((((((triple6) -> (rule9 % int5))) -> (rule2 % int4))) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule8 % int1))
The rabbit is not green.
("rabbit" "is" "green" "-")
int1
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
int2
The rabbit is nice.
("rabbit" "is" "nice" "+")
int3
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
int4
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int5
The rabbit is green.
False
6
inv-proof
[(((((((((((triple6) -> rule9)) -> rule2)) -> rule1)) -> rule7)) -> rule8))]
("rabbit" "is" "green" "+")
((((((((((triple6) -> (rule9 % int5))) -> (rule2 % int4))) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule8 % int1))
The rabbit is not green.
("rabbit" "is" "green" "-")
int1
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
int2
The rabbit is nice.
("rabbit" "is" "nice" "+")
int3
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
int4
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int5
The bear is not nice.
Unknown
inv-rconc
[@3: The bear is nice.[CWA. Example of deepest failure = (rule1 <- rule2 <- rule9 <- FAIL)]]
("bear" "is" "nice" "-")
The mouse likes the rabbit.
Unknown
rconc
[@1: The mouse likes the rabbit.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("mouse" "likes" "rabbit" "+")
The bear does not see the rabbit.
Unknown
inv-rconc
[@1: The bear sees the rabbit.[CWA. Example of deepest failure = (rule9 <- FAIL)]]
("bear" "sees" "rabbit" "-")
The bear sees the dog.
Unknown
rconc
[@2: The bear sees the dog.[CWA. Example of deepest failure = (rule2 <- rule9 <- FAIL)]]
("bear" "sees" "dog" "+")
The mouse does not see the dog.
Unknown
inv-rconc
[@2: The mouse sees the dog.[CWA. Example of deepest failure = (rule2 <- rule9 <- FAIL)]]
("mouse" "sees" "dog" "-")
The dog likes the rabbit.
Unknown
rconc
[@1: The dog likes the rabbit.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("dog" "likes" "rabbit" "+")
The bear does not see the bear.
Unknown
inv-random
[@0: The bear sees the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "sees" "bear" "-")
The mouse sees the bear.
Unknown
random
[@0: The mouse sees the bear.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "sees" "bear" "+")
The bear does not like the dog.
Unknown
inv-random
[@0: The bear likes the dog.[CWA. Example of deepest failure = (FAIL)]]
("bear" "likes" "dog" "-")
The bear visits the bear.
Unknown
random
[@0: The bear visits the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "visits" "bear" "+")
The rabbit does not see the bear.
Unknown
inv-random
[@0: The rabbit sees the bear.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "sees" "bear" "-")
The bear likes the bear.
Unknown
random
[@0: The bear likes the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "likes" "bear" "+")
@0: The bear is cold.[(triple1)] The bear visits the dog.[(triple2)] The dog sees the bear.[(triple3)] The mouse is cold.[(triple4)] The mouse visits the rabbit.[(triple5)] The rabbit sees the mouse.[(triple6)] The rabbit visits the bear.[(triple7)] @1: The rabbit sees the rabbit.[(((triple6) -> rule9))] @2: The rabbit sees the dog.[(((((triple6) -> rule9)) -> rule2))] @3: The rabbit is nice.[(((((((triple6) -> rule9)) -> rule2)) -> rule1))] @4: The rabbit likes the mouse.[(((((((((triple6) -> rule9)) -> rule2)) -> rule1)) -> rule7))] @5: The rabbit is not green.[(((((((((((triple6) -> rule9)) -> rule2)) -> rule1)) -> rule7)) -> rule8))]
The bear is cold.
("bear" "is" "cold" "+")
triple1
The bear visits the dog.
("bear" "visits" "dog" "+")
triple2
The dog sees the bear.
("dog" "sees" "bear" "+")
triple3
The mouse is cold.
("mouse" "is" "cold" "+")
triple4
The mouse visits the rabbit.
("mouse" "visits" "rabbit" "+")
triple5
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
triple6
The rabbit visits the bear.
("rabbit" "visits" "bear" "+")
triple7
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
((triple6) -> (rule9 % int1))
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int1
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
((((triple6) -> (rule9 % int2))) -> (rule2 % int1))
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
int1
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int2
The rabbit is nice.
("rabbit" "is" "nice" "+")
((((((triple6) -> (rule9 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
The rabbit is nice.
("rabbit" "is" "nice" "+")
int1
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
int2
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int3
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
((((((((triple6) -> (rule9 % int4))) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
int1
The rabbit is nice.
("rabbit" "is" "nice" "+")
int2
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
int3
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int4
The rabbit is not green.
("rabbit" "is" "green" "-")
((((((((((triple6) -> (rule9 % int5))) -> (rule2 % int4))) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule8 % int1))
The rabbit is not green.
("rabbit" "is" "green" "-")
int1
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
int2
The rabbit is nice.
("rabbit" "is" "nice" "+")
int3
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
int4
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int5