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