The cow chases the mouse. The cow does not like the mouse. The mouse does not chase the rabbit. The mouse is blue. The mouse is kind. The mouse is red. The mouse likes the cow. The mouse likes the tiger. The mouse sees the cow. The rabbit is blue. The rabbit is red. The rabbit likes the cow. The tiger does not chase the mouse. The tiger is cold. The tiger likes the cow. The tiger sees the rabbit. If someone sees the tiger then the tiger is kind. If someone chases the mouse and the mouse is not kind then the mouse sees the cow. If the tiger chases the cow and the tiger likes the rabbit then the rabbit likes the tiger. If someone is kind then they like the tiger. If the mouse is kind then the mouse sees the tiger. If the cow chases the mouse then the cow is red. If someone likes the cow then the cow is not cold. If someone chases the mouse then the mouse is cold.
The cow chases the mouse.
("cow" "chases" "mouse" "+")
The cow does not like the mouse.
("cow" "likes" "mouse" "-")
The mouse does not chase the rabbit.
("mouse" "chases" "rabbit" "-")
The mouse is blue.
("mouse" "is" "blue" "+")
The mouse is kind.
("mouse" "is" "kind" "+")
The mouse is red.
("mouse" "is" "red" "+")
The mouse likes the cow.
("mouse" "likes" "cow" "+")
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
The mouse sees the cow.
("mouse" "sees" "cow" "+")
The rabbit is blue.
("rabbit" "is" "blue" "+")
The rabbit is red.
("rabbit" "is" "red" "+")
The rabbit likes the cow.
("rabbit" "likes" "cow" "+")
The tiger does not chase the mouse.
("tiger" "chases" "mouse" "-")
The tiger is cold.
("tiger" "is" "cold" "+")
The tiger likes the cow.
("tiger" "likes" "cow" "+")
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
If someone sees the tiger then the tiger is kind.
((("someone" "sees" "tiger" "+")) -> ("tiger" "is" "kind" "+"))
If someone chases the mouse and the mouse is not kind then the mouse sees the cow.
((("someone" "chases" "mouse" "+") ("mouse" "is" "kind" "~")) -> ("mouse" "sees" "cow" "+"))
If the tiger chases the cow and the tiger likes the rabbit then the rabbit likes the tiger.
((("tiger" "chases" "cow" "+") ("tiger" "likes" "rabbit" "+")) -> ("rabbit" "likes" "tiger" "+"))
If someone is kind then they like the tiger.
((("someone" "is" "kind" "+")) -> ("someone" "likes" "tiger" "+"))
If the mouse is kind then the mouse sees the tiger.
((("mouse" "is" "kind" "+")) -> ("mouse" "sees" "tiger" "+"))
If the cow chases the mouse then the cow is red.
((("cow" "chases" "mouse" "+")) -> ("cow" "is" "red" "+"))
If someone likes the cow then the cow is not cold.
((("someone" "likes" "cow" "+")) -> ("cow" "is" "cold" "-"))
If someone chases the mouse then the mouse is cold.
((("someone" "chases" "mouse" "+")) -> ("mouse" "is" "cold" "+"))
The rabbit is blue.
True
1
proof
[(triple10)]
("rabbit" "is" "blue" "+")
triple10
The cow does not chase the mouse.
False
1
inv-proof
[(triple1)]
("cow" "chases" "mouse" "-")
triple1
The mouse is cold.
True
2
proof
[(((triple1) -> rule8))]
("mouse" "is" "cold" "+")
((triple1) -> (rule8 % int1))
The mouse is cold.
("mouse" "is" "cold" "+")
int1
The cow is cold.
False
2
inv-proof
[(((triple12) -> rule7) OR ((triple15) -> rule7) OR ((triple7) -> rule7))]
("cow" "is" "cold" "+")
((triple12) -> (rule7 % int1))
The cow is not cold.
("cow" "is" "cold" "-")
int1
((triple15) -> (rule7 % int1))
The cow is not cold.
("cow" "is" "cold" "-")
int1
((triple7) -> (rule7 % int1))
The cow is not cold.
("cow" "is" "cold" "-")
int1
The tiger is kind.
True
3
proof
[(((((triple5) -> rule5)) -> rule1))]
("tiger" "is" "kind" "+")
((((triple5) -> (rule5 % int2))) -> (rule1 % int1))
The tiger is kind.
("tiger" "is" "kind" "+")
int1
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
int2
The tiger is not kind.
False
3
inv-proof
[(((((triple5) -> rule5)) -> rule1))]
("tiger" "is" "kind" "-")
((((triple5) -> (rule5 % int2))) -> (rule1 % int1))
The tiger is kind.
("tiger" "is" "kind" "+")
int1
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
int2
The tiger likes the tiger.
True
4
proof
[(((((((triple5) -> rule5)) -> rule1)) -> rule4))]
("tiger" "likes" "tiger" "+")
((((((triple5) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int1
The tiger is kind.
("tiger" "is" "kind" "+")
int2
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
int3
The tiger does not like the tiger.
False
4
inv-proof
[(((((((triple5) -> rule5)) -> rule1)) -> rule4))]
("tiger" "likes" "tiger" "-")
((((((triple5) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int1
The tiger is kind.
("tiger" "is" "kind" "+")
int2
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
int3
The cow does not like the tiger.
Unknown
inv-rconc
[@1: The cow likes the tiger.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cow" "likes" "tiger" "-")
The rabbit likes the tiger.
Unknown
rconc
[@1: The rabbit likes the tiger.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("rabbit" "likes" "tiger" "+")
The tiger does not see the cow.
Unknown
inv-random
[@0: The tiger sees the cow.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "cow" "-")
The tiger chases the rabbit.
Unknown
random
[@0: The tiger chases the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "chases" "rabbit" "+")
The rabbit does not see the cow.
Unknown
inv-random
[@0: The rabbit sees the cow.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "sees" "cow" "-")
The cow sees the cow.
Unknown
random
[@0: The cow sees the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "cow" "+")
The tiger does not see the tiger.
Unknown
inv-random
[@0: The tiger sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "tiger" "-")
The mouse sees the mouse.
Unknown
random
[@0: The mouse sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "sees" "mouse" "+")
@0: The cow chases the mouse.[(triple1)] The cow does not like the mouse.[(triple2)] The mouse does not chase the rabbit.[(triple3)] The mouse is blue.[(triple4)] The mouse is kind.[(triple5)] The mouse is red.[(triple6)] The mouse likes the cow.[(triple7)] The mouse likes the tiger.[(triple8 OR ((triple5) -> rule4))] The mouse sees the cow.[(triple9)] The rabbit is blue.[(triple10)] The rabbit is red.[(triple11)] The rabbit likes the cow.[(triple12)] The tiger does not chase the mouse.[(triple13)] The tiger is cold.[(triple14)] The tiger likes the cow.[(triple15)] The tiger sees the rabbit.[(triple16)] @1: The cow is not cold.[(((triple12) -> rule7) OR ((triple15) -> rule7) OR ((triple7) -> rule7))] The cow is red.[(((triple1) -> rule6))] The mouse is cold.[(((triple1) -> rule8))] The mouse sees the tiger.[(((triple5) -> rule5))] @2: The tiger is kind.[(((((triple5) -> rule5)) -> rule1))] @3: The tiger likes the tiger.[(((((((triple5) -> rule5)) -> rule1)) -> rule4))]
The cow chases the mouse.
("cow" "chases" "mouse" "+")
triple1
The cow does not like the mouse.
("cow" "likes" "mouse" "-")
triple2
The mouse does not chase the rabbit.
("mouse" "chases" "rabbit" "-")
triple3
The mouse is blue.
("mouse" "is" "blue" "+")
triple4
The mouse is kind.
("mouse" "is" "kind" "+")
triple5
The mouse is red.
("mouse" "is" "red" "+")
triple6
The mouse likes the cow.
("mouse" "likes" "cow" "+")
triple7
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
triple8
((triple5) -> (rule4 % int1))
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
int1
The mouse sees the cow.
("mouse" "sees" "cow" "+")
triple9
The rabbit is blue.
("rabbit" "is" "blue" "+")
triple10
The rabbit is red.
("rabbit" "is" "red" "+")
triple11
The rabbit likes the cow.
("rabbit" "likes" "cow" "+")
triple12
The tiger does not chase the mouse.
("tiger" "chases" "mouse" "-")
triple13
The tiger is cold.
("tiger" "is" "cold" "+")
triple14
The tiger likes the cow.
("tiger" "likes" "cow" "+")
triple15
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
triple16
The cow is not cold.
("cow" "is" "cold" "-")
((triple12) -> (rule7 % int1))
The cow is not cold.
("cow" "is" "cold" "-")
int1
((triple15) -> (rule7 % int1))
The cow is not cold.
("cow" "is" "cold" "-")
int1
((triple7) -> (rule7 % int1))
The cow is not cold.
("cow" "is" "cold" "-")
int1
The cow is red.
("cow" "is" "red" "+")
((triple1) -> (rule6 % int1))
The cow is red.
("cow" "is" "red" "+")
int1
The mouse is cold.
("mouse" "is" "cold" "+")
((triple1) -> (rule8 % int1))
The mouse is cold.
("mouse" "is" "cold" "+")
int1
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
((triple5) -> (rule5 % int1))
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
int1
The tiger is kind.
("tiger" "is" "kind" "+")
((((triple5) -> (rule5 % int2))) -> (rule1 % int1))
The tiger is kind.
("tiger" "is" "kind" "+")
int1
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
int2
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
((((((triple5) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int1
The tiger is kind.
("tiger" "is" "kind" "+")
int2
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
int3