The cat eats the mouse. The cat is big. The cat likes the mouse. The cow is not blue. The cow is kind. The cow likes the mouse. The mouse eats the cat. The mouse eats the cow. The mouse likes the cat. The mouse sees the cat. If someone likes the mouse then they are big. If the cat sees the mouse and the cat likes the mouse then the mouse likes the cow. If someone is green and they see the cow then they do not eat the cat. If someone likes the cat then the cat is cold. If someone is big then they see the cat. If someone sees the cat and they are not green then they eat the mouse.
The cat eats the mouse.
("cat" "eats" "mouse" "+")
The cat is big.
("cat" "is" "big" "+")
The cat likes the mouse.
("cat" "likes" "mouse" "+")
The cow is not blue.
("cow" "is" "blue" "-")
The cow is kind.
("cow" "is" "kind" "+")
The cow likes the mouse.
("cow" "likes" "mouse" "+")
The mouse eats the cat.
("mouse" "eats" "cat" "+")
The mouse eats the cow.
("mouse" "eats" "cow" "+")
The mouse likes the cat.
("mouse" "likes" "cat" "+")
The mouse sees the cat.
("mouse" "sees" "cat" "+")
If someone likes the mouse then they are big.
((("someone" "likes" "mouse" "+")) -> ("someone" "is" "big" "+"))
If the cat sees the mouse and the cat likes the mouse then the mouse likes the cow.
((("cat" "sees" "mouse" "+") ("cat" "likes" "mouse" "+")) -> ("mouse" "likes" "cow" "+"))
If someone is green and they see the cow then they do not eat the cat.
((("someone" "is" "green" "+") ("someone" "sees" "cow" "+")) -> ("someone" "eats" "cat" "-"))
If someone likes the cat then the cat is cold.
((("someone" "likes" "cat" "+")) -> ("cat" "is" "cold" "+"))
If someone is big then they see the cat.
((("someone" "is" "big" "+")) -> ("someone" "sees" "cat" "+"))
If someone sees the cat and they are not green then they eat the mouse.
((("someone" "sees" "cat" "+") ("someone" "is" "green" "~")) -> ("someone" "eats" "mouse" "+"))
The cat eats the mouse.
True
1
proof
[(triple1)]
("cat" "eats" "mouse" "+")
triple1
The mouse does not eat the cat.
False
1
inv-proof
[(triple7)]
("mouse" "eats" "cat" "-")
triple7
The cow is big.
True
2
proof
[(((triple6) -> rule1))]
("cow" "is" "big" "+")
((triple6) -> (rule1 % int1))
The cow is big.
("cow" "is" "big" "+")
int1
The cat does not see the cat.
False
2
inv-proof
[(((triple2) -> rule5) OR ((((triple3) -> rule1)) -> rule5))]
("cat" "sees" "cat" "-")
((triple2) -> (rule5 % int1))
The cat sees the cat.
("cat" "sees" "cat" "+")
int1
((((triple3) -> (rule1 % int2))) -> (rule5 % int1))
The cat sees the cat.
("cat" "sees" "cat" "+")
int1
The cat is big.
("cat" "is" "big" "+")
int2
The mouse does not eat the mouse.
Unknown
inv-rconc
[@1: The mouse eats the mouse.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("mouse" "eats" "mouse" "-")
The mouse is big.
Unknown
rconc
[@1: The mouse is big.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("mouse" "is" "big" "+")
The mouse is not kind.
Unknown
inv-random
[@0: The mouse is kind.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "kind" "-")
The cow sees the mouse.
Unknown
random
[@0: The cow sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "mouse" "+")
@0: The cat eats the mouse.[(triple1)] The cat is big.[(triple2 OR ((triple3) -> rule1))] The cat likes the mouse.[(triple3)] The cow is kind.[(triple5)] The cow is not blue.[(triple4)] The cow likes the mouse.[(triple6)] The mouse eats the cat.[(triple7)] The mouse eats the cow.[(triple8)] The mouse likes the cat.[(triple9)] The mouse sees the cat.[(triple10)] @1: The cat is cold.[(((triple9) -> rule4))] The cat sees the cat.[(((triple2) -> rule5) OR ((((triple3) -> rule1)) -> rule5))] The cow is big.[(((triple6) -> rule1))] @2: The cow sees the cat.[(((((triple6) -> rule1)) -> rule5))]
The cat eats the mouse.
("cat" "eats" "mouse" "+")
triple1
The cat is big.
("cat" "is" "big" "+")
triple2
((triple3) -> (rule1 % int1))
The cat is big.
("cat" "is" "big" "+")
int1
The cat likes the mouse.
("cat" "likes" "mouse" "+")
triple3
The cow is kind.
("cow" "is" "kind" "+")
triple5
The cow is not blue.
("cow" "is" "blue" "-")
triple4
The cow likes the mouse.
("cow" "likes" "mouse" "+")
triple6
The mouse eats the cat.
("mouse" "eats" "cat" "+")
triple7
The mouse eats the cow.
("mouse" "eats" "cow" "+")
triple8
The mouse likes the cat.
("mouse" "likes" "cat" "+")
triple9
The mouse sees the cat.
("mouse" "sees" "cat" "+")
triple10
The cat is cold.
("cat" "is" "cold" "+")
((triple9) -> (rule4 % int1))
The cat is cold.
("cat" "is" "cold" "+")
int1
The cat sees the cat.
("cat" "sees" "cat" "+")
((triple2) -> (rule5 % int1))
The cat sees the cat.
("cat" "sees" "cat" "+")
int1
((((triple3) -> (rule1 % int2))) -> (rule5 % int1))
The cat sees the cat.
("cat" "sees" "cat" "+")
int1
The cat is big.
("cat" "is" "big" "+")
int2
The cow is big.
("cow" "is" "big" "+")
((triple6) -> (rule1 % int1))
The cow is big.
("cow" "is" "big" "+")
int1
The cow sees the cat.
("cow" "sees" "cat" "+")
((((triple6) -> (rule1 % int2))) -> (rule5 % int1))
The cow sees the cat.
("cow" "sees" "cat" "+")
int1
The cow is big.
("cow" "is" "big" "+")
int2