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