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