The cat eats the mouse. The cat is kind. The cat does not need the rabbit. The cat visits the rabbit. The cat does not visit the tiger. The mouse is green. The mouse is rough. The mouse needs the cat. The mouse visits the tiger. The rabbit is green. The rabbit is kind. The tiger is green. The tiger is kind. The tiger needs the mouse. The tiger visits the rabbit. If someone needs the rabbit then they eat the mouse. If the mouse eats the tiger and the mouse is green then the tiger eats the rabbit. If someone is round then they need the rabbit. If the mouse needs the rabbit and the mouse is not green then the rabbit needs the cat. If someone eats the tiger then the tiger is green. If someone visits the mouse then they need the tiger. If someone is rough then they are round. If someone eats the cat and the cat is not kind then they visit the tiger.
The cat eats the mouse.
("cat" "eats" "mouse" "+")
The cat is kind.
("cat" "is" "kind" "+")
The cat does not need the rabbit.
("cat" "needs" "rabbit" "-")
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
The cat does not visit the tiger.
("cat" "visits" "tiger" "-")
The mouse is green.
("mouse" "is" "green" "+")
The mouse is rough.
("mouse" "is" "rough" "+")
The mouse needs the cat.
("mouse" "needs" "cat" "+")
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
The rabbit is green.
("rabbit" "is" "green" "+")
The rabbit is kind.
("rabbit" "is" "kind" "+")
The tiger is green.
("tiger" "is" "green" "+")
The tiger is kind.
("tiger" "is" "kind" "+")
The tiger needs the mouse.
("tiger" "needs" "mouse" "+")
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
If someone needs the rabbit then they eat the mouse.
((("someone" "needs" "rabbit" "+")) -> ("someone" "eats" "mouse" "+"))
If the mouse eats the tiger and the mouse is green then the tiger eats the rabbit.
((("mouse" "eats" "tiger" "+") ("mouse" "is" "green" "+")) -> ("tiger" "eats" "rabbit" "+"))
If someone is round then they need the rabbit.
((("someone" "is" "round" "+")) -> ("someone" "needs" "rabbit" "+"))
If the mouse needs the rabbit and the mouse is not green then the rabbit needs the cat.
((("mouse" "needs" "rabbit" "+") ("mouse" "is" "green" "~")) -> ("rabbit" "needs" "cat" "+"))
If someone eats the tiger then the tiger is green.
((("someone" "eats" "tiger" "+")) -> ("tiger" "is" "green" "+"))
If someone visits the mouse then they need the tiger.
((("someone" "visits" "mouse" "+")) -> ("someone" "needs" "tiger" "+"))
If someone is rough then they are round.
((("someone" "is" "rough" "+")) -> ("someone" "is" "round" "+"))
If someone eats the cat and the cat is not kind then they visit the tiger.
((("someone" "eats" "cat" "+") ("cat" "is" "kind" "~")) -> ("someone" "visits" "tiger" "+"))
The cat is kind.
True
1
proof
[(triple2)]
("cat" "is" "kind" "+")
triple2
The rabbit is not kind.
False
1
inv-proof
[(triple11)]
("rabbit" "is" "kind" "-")
triple11
The mouse is round.
True
2
proof
[(((triple7) -> rule7))]
("mouse" "is" "round" "+")
((triple7) -> (rule7 % int1))
The mouse is round.
("mouse" "is" "round" "+")
int1
The mouse is not round.
False
2
inv-proof
[(((triple7) -> rule7))]
("mouse" "is" "round" "-")
((triple7) -> (rule7 % int1))
The mouse is round.
("mouse" "is" "round" "+")
int1
The mouse needs the rabbit.
True
3
proof
[(((((triple7) -> rule7)) -> rule3))]
("mouse" "needs" "rabbit" "+")
((((triple7) -> (rule7 % int2))) -> (rule3 % int1))
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
int1
The mouse is round.
("mouse" "is" "round" "+")
int2
The mouse does not need the rabbit.
False
3
inv-proof
[(((((triple7) -> rule7)) -> rule3))]
("mouse" "needs" "rabbit" "-")
((((triple7) -> (rule7 % int2))) -> (rule3 % int1))
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
int1
The mouse is round.
("mouse" "is" "round" "+")
int2
The mouse eats the mouse.
True
4
proof
[(((((((triple7) -> rule7)) -> rule3)) -> rule1))]
("mouse" "eats" "mouse" "+")
((((((triple7) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The mouse eats the mouse.
("mouse" "eats" "mouse" "+")
int1
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
int2
The mouse is round.
("mouse" "is" "round" "+")
int3
The mouse does not eat the mouse.
False
4
inv-proof
[(((((((triple7) -> rule7)) -> rule3)) -> rule1))]
("mouse" "eats" "mouse" "-")
((((((triple7) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The mouse eats the mouse.
("mouse" "eats" "mouse" "+")
int1
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
int2
The mouse is round.
("mouse" "is" "round" "+")
int3
The tiger does not eat the rabbit.
Unknown
inv-rconc
[@1: The tiger eats the rabbit.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("tiger" "eats" "rabbit" "-")
The rabbit visits the tiger.
Unknown
rconc
[@1: The rabbit visits the tiger.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("rabbit" "visits" "tiger" "+")
The tiger is not round.
Unknown
inv-rconc
[@1: The tiger is round.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("tiger" "is" "round" "-")
The tiger needs the rabbit.
Unknown
rconc
[@2: The tiger needs the rabbit.[CWA. Example of deepest failure = (rule3 <- rule7 <- FAIL)]]
("tiger" "needs" "rabbit" "+")
The mouse does not visit the mouse.
Unknown
inv-random
[@0: The mouse visits the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "visits" "mouse" "-")
The cat eats the cat.
Unknown
random
[@0: The cat eats the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "eats" "cat" "+")
The cat is not rough.
Unknown
inv-random
[@0: The cat is rough.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "rough" "-")
The mouse eats the cat.
Unknown
random
[@0: The mouse eats the cat.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "eats" "cat" "+")
@0: The cat does not need the rabbit.[(triple3)] The cat does not visit the tiger.[(triple5)] The cat eats the mouse.[(triple1)] The cat is kind.[(triple2)] The cat visits the rabbit.[(triple4)] The mouse is green.[(triple6)] The mouse is rough.[(triple7)] The mouse needs the cat.[(triple8)] The mouse visits the tiger.[(triple9)] The rabbit is green.[(triple10)] The rabbit is kind.[(triple11)] The tiger is green.[(triple12)] The tiger is kind.[(triple13)] The tiger needs the mouse.[(triple14)] The tiger visits the rabbit.[(triple15)] @1: The mouse is round.[(((triple7) -> rule7))] @2: The mouse needs the rabbit.[(((((triple7) -> rule7)) -> rule3))] @3: The mouse eats the mouse.[(((((((triple7) -> rule7)) -> rule3)) -> rule1))]
The cat does not need the rabbit.
("cat" "needs" "rabbit" "-")
triple3
The cat does not visit the tiger.
("cat" "visits" "tiger" "-")
triple5
The cat eats the mouse.
("cat" "eats" "mouse" "+")
triple1
The cat is kind.
("cat" "is" "kind" "+")
triple2
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
triple4
The mouse is green.
("mouse" "is" "green" "+")
triple6
The mouse is rough.
("mouse" "is" "rough" "+")
triple7
The mouse needs the cat.
("mouse" "needs" "cat" "+")
triple8
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
triple9
The rabbit is green.
("rabbit" "is" "green" "+")
triple10
The rabbit is kind.
("rabbit" "is" "kind" "+")
triple11
The tiger is green.
("tiger" "is" "green" "+")
triple12
The tiger is kind.
("tiger" "is" "kind" "+")
triple13
The tiger needs the mouse.
("tiger" "needs" "mouse" "+")
triple14
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
triple15
The mouse is round.
("mouse" "is" "round" "+")
((triple7) -> (rule7 % int1))
The mouse is round.
("mouse" "is" "round" "+")
int1
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
((((triple7) -> (rule7 % int2))) -> (rule3 % int1))
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
int1
The mouse is round.
("mouse" "is" "round" "+")
int2
The mouse eats the mouse.
("mouse" "eats" "mouse" "+")
((((((triple7) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The mouse eats the mouse.
("mouse" "eats" "mouse" "+")
int1
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
int2
The mouse is round.
("mouse" "is" "round" "+")
int3