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