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