The cat eats the mouse. The cat is rough. The cat does not see the mouse. The cat visits the mouse. The mouse eats the cat. The mouse is blue. The mouse is cold. The mouse is not green. The mouse is nice. The mouse is rough. The mouse sees the cat. The mouse does not visit the cat. If someone is nice then they see the cat. If someone is nice then they eat the mouse. If the cat eats the mouse and the cat is not nice then the cat does not see the mouse. If someone sees the cat and the cat does not see the mouse then the cat is blue. Blue people are cold. If someone is cold and they see the mouse then the mouse sees the cat.
The cat eats the mouse.
("cat" "eats" "mouse" "+")
The cat is rough.
("cat" "is" "rough" "+")
The cat does not see the mouse.
("cat" "sees" "mouse" "-")
The cat visits the mouse.
("cat" "visits" "mouse" "+")
The mouse eats the cat.
("mouse" "eats" "cat" "+")
The mouse is blue.
("mouse" "is" "blue" "+")
The mouse is cold.
("mouse" "is" "cold" "+")
The mouse is not green.
("mouse" "is" "green" "-")
The mouse is nice.
("mouse" "is" "nice" "+")
The mouse is rough.
("mouse" "is" "rough" "+")
The mouse sees the cat.
("mouse" "sees" "cat" "+")
The mouse does not visit the cat.
("mouse" "visits" "cat" "-")
If someone is nice then they see the cat.
((("someone" "is" "nice" "+")) -> ("someone" "sees" "cat" "+"))
If someone is nice then they eat the mouse.
((("someone" "is" "nice" "+")) -> ("someone" "eats" "mouse" "+"))
If the cat eats the mouse and the cat is not nice then the cat does not see the mouse.
((("cat" "eats" "mouse" "+") ("cat" "is" "nice" "~")) -> ("cat" "sees" "mouse" "-"))
If someone sees the cat and the cat does not see the mouse then the cat is blue.
((("someone" "sees" "cat" "+") ("cat" "sees" "mouse" "~")) -> ("cat" "is" "blue" "+"))
Blue people are cold.
((("someone" "is" "blue" "+")) -> ("someone" "is" "cold" "+"))
If someone is cold and they see the mouse then the mouse sees the cat.
((("someone" "is" "cold" "+") ("someone" "sees" "mouse" "+")) -> ("mouse" "sees" "cat" "+"))
The mouse is cold.
True
1
proof
[(triple7 OR ((triple6) -> rule5))]
("mouse" "is" "cold" "+")
triple7
((triple6) -> (rule5 % int1))
The mouse is cold.
("mouse" "is" "cold" "+")
int1
The mouse is not nice.
False
1
inv-proof
[(triple9)]
("mouse" "is" "nice" "-")
triple9
The cat is blue.
True
3
proof
[(((triple11 triple3) -> rule4) OR ((((triple9) -> rule1) triple3) -> rule4))]
("cat" "is" "blue" "+")
((triple11 triple3) -> (rule4 % int1))
The cat is blue.
("cat" "is" "blue" "+")
int1
((((triple9) -> (rule1 % int2)) triple3) -> (rule4 % int1))
The cat is blue.
("cat" "is" "blue" "+")
int1
The mouse sees the cat.
("mouse" "sees" "cat" "+")
int2
The mouse does not eat the mouse.
False
2
inv-proof
[(((triple9) -> rule2))]
("mouse" "eats" "mouse" "-")
((triple9) -> (rule2 % int1))
The mouse eats the mouse.
("mouse" "eats" "mouse" "+")
int1
The cat is cold.
True
4
proof
[(((((triple11 triple3) -> rule4)) -> rule5) OR ((((((triple9) -> rule1) triple3) -> rule4)) -> rule5))]
("cat" "is" "cold" "+")
((((triple11 triple3) -> (rule4 % int2))) -> (rule5 % int1))
The cat is cold.
("cat" "is" "cold" "+")
int1
The cat is blue.
("cat" "is" "blue" "+")
int2
((((((triple9) -> (rule1 % int3)) triple3) -> (rule4 % int2))) -> (rule5 % int1))
The cat is cold.
("cat" "is" "cold" "+")
int1
The cat is blue.
("cat" "is" "blue" "+")
int2
The mouse sees the cat.
("mouse" "sees" "cat" "+")
int3
The cat is not cold.
False
4
inv-proof
[(((((triple11 triple3) -> rule4)) -> rule5) OR ((((((triple9) -> rule1) triple3) -> rule4)) -> rule5))]
("cat" "is" "cold" "-")
((((triple11 triple3) -> (rule4 % int2))) -> (rule5 % int1))
The cat is cold.
("cat" "is" "cold" "+")
int1
The cat is blue.
("cat" "is" "blue" "+")
int2
((((((triple9) -> (rule1 % int3)) triple3) -> (rule4 % int2))) -> (rule5 % int1))
The cat is cold.
("cat" "is" "cold" "+")
int1
The cat is blue.
("cat" "is" "blue" "+")
int2
The mouse sees the cat.
("mouse" "sees" "cat" "+")
int3
The cat does not see the cat.
Unknown
inv-rconc
[@1: The cat sees the cat.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "sees" "cat" "-")
The cat is nice.
Unknown
random
[@0: The cat is nice.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "nice" "+")
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 visits the cat.
Unknown
random
[@0: The cat visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "visits" "cat" "+")
The cat is not green.
Unknown
inv-random
[@0: The cat is green.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "green" "-")
The mouse sees the mouse.
Unknown
random
[@0: The mouse sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "sees" "mouse" "+")
@0: The cat does not see the mouse.[(triple3)] The cat eats the mouse.[(triple1)] The cat is rough.[(triple2)] The cat visits the mouse.[(triple4)] The mouse does not visit the cat.[(triple12)] The mouse eats the cat.[(triple5)] The mouse is blue.[(triple6)] The mouse is cold.[(triple7 OR ((triple6) -> rule5))] The mouse is nice.[(triple9)] The mouse is not green.[(triple8)] The mouse is rough.[(triple10)] The mouse sees the cat.[(triple11 OR ((triple9) -> rule1))] @1: The cat is blue.[(((triple11 triple3) -> rule4) OR ((((triple9) -> rule1) triple3) -> rule4))] The mouse eats the mouse.[(((triple9) -> rule2))] @2: The cat is cold.[(((((triple11 triple3) -> rule4)) -> rule5) OR ((((((triple9) -> rule1) triple3) -> rule4)) -> rule5))]
The cat does not see the mouse.
("cat" "sees" "mouse" "-")
triple3
The cat eats the mouse.
("cat" "eats" "mouse" "+")
triple1
The cat is rough.
("cat" "is" "rough" "+")
triple2
The cat visits the mouse.
("cat" "visits" "mouse" "+")
triple4
The mouse does not visit the cat.
("mouse" "visits" "cat" "-")
triple12
The mouse eats the cat.
("mouse" "eats" "cat" "+")
triple5
The mouse is blue.
("mouse" "is" "blue" "+")
triple6
The mouse is cold.
("mouse" "is" "cold" "+")
triple7
((triple6) -> (rule5 % int1))
The mouse is cold.
("mouse" "is" "cold" "+")
int1
The mouse is nice.
("mouse" "is" "nice" "+")
triple9
The mouse is not green.
("mouse" "is" "green" "-")
triple8
The mouse is rough.
("mouse" "is" "rough" "+")
triple10
The mouse sees the cat.
("mouse" "sees" "cat" "+")
triple11
((triple9) -> (rule1 % int1))
The mouse sees the cat.
("mouse" "sees" "cat" "+")
int1
The cat is blue.
("cat" "is" "blue" "+")
((triple11 triple3) -> (rule4 % int1))
The cat is blue.
("cat" "is" "blue" "+")
int1
((((triple9) -> (rule1 % int2)) triple3) -> (rule4 % int1))
The cat is blue.
("cat" "is" "blue" "+")
int1
The mouse sees the cat.
("mouse" "sees" "cat" "+")
int2
The mouse eats the mouse.
("mouse" "eats" "mouse" "+")
((triple9) -> (rule2 % int1))
The mouse eats the mouse.
("mouse" "eats" "mouse" "+")
int1
The cat is cold.
("cat" "is" "cold" "+")
((((triple11 triple3) -> (rule4 % int2))) -> (rule5 % int1))
The cat is cold.
("cat" "is" "cold" "+")
int1
The cat is blue.
("cat" "is" "blue" "+")
int2
((((((triple9) -> (rule1 % int3)) triple3) -> (rule4 % int2))) -> (rule5 % int1))
The cat is cold.
("cat" "is" "cold" "+")
int1
The cat is blue.
("cat" "is" "blue" "+")
int2
The mouse sees the cat.
("mouse" "sees" "cat" "+")
int3