The cat eats the mouse. The cat eats the tiger. The cat is big. The cat is not rough. The cat likes the mouse. The cat visits the mouse. The mouse eats the tiger. The mouse is green. The mouse is kind. The mouse does not like the cat. The mouse does not like the tiger. The mouse does not visit the cat. The mouse does not visit the tiger. The tiger is cold. The tiger is green. If the tiger visits the cat then the cat is big. If something is kind and cold then it eats the mouse. If something likes the tiger then it visits the cat. If something is green and it eats the cat then the cat visits the mouse. If something likes the tiger then the tiger does not eat the mouse. If something visits the tiger then the tiger eats the mouse. If something eats the mouse then it likes the mouse. If the tiger is green then the tiger is kind.
The cat eats the mouse.
("cat" "eats" "mouse" "+")
The cat eats the tiger.
("cat" "eats" "tiger" "+")
The cat is big.
("cat" "is" "big" "+")
The cat is not rough.
("cat" "is" "rough" "-")
The cat likes the mouse.
("cat" "likes" "mouse" "+")
The cat visits the mouse.
("cat" "visits" "mouse" "+")
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
The mouse is green.
("mouse" "is" "green" "+")
The mouse is kind.
("mouse" "is" "kind" "+")
The mouse does not like the cat.
("mouse" "likes" "cat" "-")
The mouse does not like the tiger.
("mouse" "likes" "tiger" "-")
The mouse does not visit the cat.
("mouse" "visits" "cat" "-")
The mouse does not visit the tiger.
("mouse" "visits" "tiger" "-")
The tiger is cold.
("tiger" "is" "cold" "+")
The tiger is green.
("tiger" "is" "green" "+")
If the tiger visits the cat then the cat is big.
((("tiger" "visits" "cat" "+")) -> ("cat" "is" "big" "+"))
If something is kind and cold then it eats the mouse.
((("something" "is" "kind" "+") ("something" "is" "cold" "+")) -> ("something" "eats" "mouse" "+"))
If something likes the tiger then it visits the cat.
((("something" "likes" "tiger" "+")) -> ("something" "visits" "cat" "+"))
If something is green and it eats the cat then the cat visits the mouse.
((("something" "is" "green" "+") ("something" "eats" "cat" "+")) -> ("cat" "visits" "mouse" "+"))
If something likes the tiger then the tiger does not eat the mouse.
((("something" "likes" "tiger" "+")) -> ("tiger" "eats" "mouse" "-"))
If something visits the tiger then the tiger eats the mouse.
((("something" "visits" "tiger" "+")) -> ("tiger" "eats" "mouse" "+"))
If something eats the mouse then it likes the mouse.
((("something" "eats" "mouse" "+")) -> ("something" "likes" "mouse" "+"))
If the tiger is green then the tiger is kind.
((("tiger" "is" "green" "+")) -> ("tiger" "is" "kind" "+"))
The tiger is cold.
True
1
proof
[(triple14)]
("tiger" "is" "cold" "+")
triple14
The mouse likes the cat.
False
1
inv-proof
[(triple10)]
("mouse" "likes" "cat" "+")
triple10
The tiger is kind.
True
2
proof
[(((triple15) -> rule8))]
("tiger" "is" "kind" "+")
((triple15) -> (rule8 % int1))
The tiger is kind.
("tiger" "is" "kind" "+")
int1
The tiger is not kind.
False
2
inv-proof
[(((triple15) -> rule8))]
("tiger" "is" "kind" "-")
((triple15) -> (rule8 % int1))
The tiger is kind.
("tiger" "is" "kind" "+")
int1
The tiger eats the mouse.
True
4
proof
[(((((triple15) -> rule8) triple14) -> rule2))]
("tiger" "eats" "mouse" "+")
((((triple15) -> (rule8 % int2)) triple14) -> (rule2 % int1))
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
int1
The tiger is kind.
("tiger" "is" "kind" "+")
int2
The tiger does not eat the mouse.
False
4
inv-proof
[(((((triple15) -> rule8) triple14) -> rule2))]
("tiger" "eats" "mouse" "-")
((((triple15) -> (rule8 % int2)) triple14) -> (rule2 % int1))
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
int1
The tiger is kind.
("tiger" "is" "kind" "+")
int2
The tiger likes the mouse.
True
5
proof
[(((((((triple15) -> rule8) triple14) -> rule2)) -> rule7))]
("tiger" "likes" "mouse" "+")
((((((triple15) -> (rule8 % int3)) triple14) -> (rule2 % int2))) -> (rule7 % int1))
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
int1
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
int2
The tiger is kind.
("tiger" "is" "kind" "+")
int3
The tiger does not like the mouse.
False
5
inv-proof
[(((((((triple15) -> rule8) triple14) -> rule2)) -> rule7))]
("tiger" "likes" "mouse" "-")
((((((triple15) -> (rule8 % int3)) triple14) -> (rule2 % int2))) -> (rule7 % int1))
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
int1
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
int2
The tiger is kind.
("tiger" "is" "kind" "+")
int3
The mouse does not like the mouse.
Unknown
inv-rconc
[@2: The mouse likes the mouse.[CWA. Example of deepest failure = (rule7 <- rule2 <- FAIL)]]
("mouse" "likes" "mouse" "-")
The cat visits the cat.
Unknown
rconc
[@1: The cat visits the cat.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cat" "visits" "cat" "+")
The tiger does not visit the cat.
Unknown
inv-rconc
[@1: The tiger visits the cat.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("tiger" "visits" "cat" "-")
The mouse eats the mouse.
Unknown
rconc
[@1: The mouse eats the mouse.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("mouse" "eats" "mouse" "+")
The tiger does not eat the cat.
Unknown
inv-random
[@0: The tiger eats the cat.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "eats" "cat" "-")
The mouse is cold.
Unknown
random
[@0: The mouse is cold.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "cold" "+")
The cat is not kind.
Unknown
inv-random
[@0: The cat is kind.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "kind" "-")
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 eats the mouse.[(triple1)] The cat eats the tiger.[(triple2)] The cat is big.[(triple3)] The cat is not rough.[(triple4)] The cat likes the mouse.[(triple5 OR ((triple1) -> rule7))] The cat visits the mouse.[(triple6)] The mouse does not like the cat.[(triple10)] The mouse does not like the tiger.[(triple11)] The mouse does not visit the cat.[(triple12)] The mouse does not visit the tiger.[(triple13)] The mouse eats the tiger.[(triple7)] The mouse is green.[(triple8)] The mouse is kind.[(triple9)] The tiger is cold.[(triple14)] The tiger is green.[(triple15)] @1: The tiger is kind.[(((triple15) -> rule8))] @2: The tiger eats the mouse.[(((((triple15) -> rule8) triple14) -> rule2))] @3: The tiger likes the mouse.[(((((((triple15) -> rule8) triple14) -> rule2)) -> rule7))]
The cat eats the mouse.
("cat" "eats" "mouse" "+")
triple1
The cat eats the tiger.
("cat" "eats" "tiger" "+")
triple2
The cat is big.
("cat" "is" "big" "+")
triple3
The cat is not rough.
("cat" "is" "rough" "-")
triple4
The cat likes the mouse.
("cat" "likes" "mouse" "+")
triple5
((triple1) -> (rule7 % int1))
The cat likes the mouse.
("cat" "likes" "mouse" "+")
int1
The cat visits the mouse.
("cat" "visits" "mouse" "+")
triple6
The mouse does not like the cat.
("mouse" "likes" "cat" "-")
triple10
The mouse does not like the tiger.
("mouse" "likes" "tiger" "-")
triple11
The mouse does not visit the cat.
("mouse" "visits" "cat" "-")
triple12
The mouse does not visit the tiger.
("mouse" "visits" "tiger" "-")
triple13
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
triple7
The mouse is green.
("mouse" "is" "green" "+")
triple8
The mouse is kind.
("mouse" "is" "kind" "+")
triple9
The tiger is cold.
("tiger" "is" "cold" "+")
triple14
The tiger is green.
("tiger" "is" "green" "+")
triple15
The tiger is kind.
("tiger" "is" "kind" "+")
((triple15) -> (rule8 % int1))
The tiger is kind.
("tiger" "is" "kind" "+")
int1
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
((((triple15) -> (rule8 % int2)) triple14) -> (rule2 % int1))
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
int1
The tiger is kind.
("tiger" "is" "kind" "+")
int2
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
((((((triple15) -> (rule8 % int3)) triple14) -> (rule2 % int2))) -> (rule7 % int1))
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
int1
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
int2
The tiger is kind.
("tiger" "is" "kind" "+")
int3