The cat eats the mouse. The cat is nice. The cat is round. The cat is not young. The cat sees the mouse. The cat visits the mouse. The mouse eats the cat. The mouse is big. The mouse is nice. The mouse is round. The mouse sees the cat. The mouse visits the cat. If something is kind and round then it sees the cat. If something eats the cat then the cat visits the mouse. If something sees the cat then it eats the mouse. If the cat visits the mouse and the cat is big then the mouse sees the cat. If something visits the mouse and it eats the mouse then it is not big. If something visits the mouse and it is not round then it does not visit the cat.
The cat eats the mouse.
("cat" "eats" "mouse" "+")
The cat is nice.
("cat" "is" "nice" "+")
The cat is round.
("cat" "is" "round" "+")
The cat is not young.
("cat" "is" "young" "-")
The cat sees the mouse.
("cat" "sees" "mouse" "+")
The cat visits the mouse.
("cat" "visits" "mouse" "+")
The mouse eats the cat.
("mouse" "eats" "cat" "+")
The mouse is big.
("mouse" "is" "big" "+")
The mouse is nice.
("mouse" "is" "nice" "+")
The mouse is round.
("mouse" "is" "round" "+")
The mouse sees the cat.
("mouse" "sees" "cat" "+")
The mouse visits the cat.
("mouse" "visits" "cat" "+")
If something is kind and round then it sees the cat.
((("something" "is" "kind" "+") ("something" "is" "round" "+")) -> ("something" "sees" "cat" "+"))
If something eats the cat then the cat visits the mouse.
((("something" "eats" "cat" "+")) -> ("cat" "visits" "mouse" "+"))
If something sees the cat then it eats the mouse.
((("something" "sees" "cat" "+")) -> ("something" "eats" "mouse" "+"))
If the cat visits the mouse and the cat is big then the mouse sees the cat.
((("cat" "visits" "mouse" "+") ("cat" "is" "big" "+")) -> ("mouse" "sees" "cat" "+"))
If something visits the mouse and it eats the mouse then it is not big.
((("something" "visits" "mouse" "+") ("something" "eats" "mouse" "+")) -> ("something" "is" "big" "-"))
If something visits the mouse and it is not round then it does not visit the cat.
((("something" "visits" "mouse" "+") ("something" "is" "round" "~")) -> ("something" "visits" "cat" "-"))
The mouse is nice.
True
1
proof
[(triple9)]
("mouse" "is" "nice" "+")
triple9
The cat does not eat the mouse.
False
1
inv-proof
[(triple1)]
("cat" "eats" "mouse" "-")
triple1
The mouse eats the mouse.
True
2
proof
[(((triple11) -> rule3))]
("mouse" "eats" "mouse" "+")
((triple11) -> (rule3 % int1))
The mouse eats the mouse.
("mouse" "eats" "mouse" "+")
int1
The cat is big.
False
3
inv-proof
[(((triple6 triple1) -> rule5) OR ((((triple7) -> rule2) triple1) -> rule5))]
("cat" "is" "big" "+")
((triple6 triple1) -> (rule5 % int1))
The cat is not big.
("cat" "is" "big" "-")
int1
((((triple7) -> (rule2 % int2)) triple1) -> (rule5 % int1))
The cat is not big.
("cat" "is" "big" "-")
int1
The cat visits the mouse.
("cat" "visits" "mouse" "+")
int2
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 mouse is young.
Unknown
random
[@0: The mouse is young.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "young" "+")
The cat does not eat the cat.
Unknown
inv-random
[@0: The cat eats the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "eats" "cat" "-")
The cat is kind.
Unknown
random
[@0: The cat is kind.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "kind" "+")
@0: The cat eats the mouse.[(triple1)] The cat is nice.[(triple2)] The cat is not young.[(triple4)] The cat is round.[(triple3)] The cat sees the mouse.[(triple5)] The cat visits the mouse.[(triple6 OR ((triple7) -> rule2))] The mouse eats the cat.[(triple7)] The mouse is big.[(triple8)] The mouse is nice.[(triple9)] The mouse is round.[(triple10)] The mouse sees the cat.[(triple11)] The mouse visits the cat.[(triple12)] @1: The cat is not big.[(((triple6 triple1) -> rule5) OR ((((triple7) -> rule2) triple1) -> rule5))] The mouse eats the mouse.[(((triple11) -> rule3))]
The cat eats the mouse.
("cat" "eats" "mouse" "+")
triple1
The cat is nice.
("cat" "is" "nice" "+")
triple2
The cat is not young.
("cat" "is" "young" "-")
triple4
The cat is round.
("cat" "is" "round" "+")
triple3
The cat sees the mouse.
("cat" "sees" "mouse" "+")
triple5
The cat visits the mouse.
("cat" "visits" "mouse" "+")
triple6
((triple7) -> (rule2 % int1))
The cat visits the mouse.
("cat" "visits" "mouse" "+")
int1
The mouse eats the cat.
("mouse" "eats" "cat" "+")
triple7
The mouse is big.
("mouse" "is" "big" "+")
triple8
The mouse is nice.
("mouse" "is" "nice" "+")
triple9
The mouse is round.
("mouse" "is" "round" "+")
triple10
The mouse sees the cat.
("mouse" "sees" "cat" "+")
triple11
The mouse visits the cat.
("mouse" "visits" "cat" "+")
triple12
The cat is not big.
("cat" "is" "big" "-")
((triple6 triple1) -> (rule5 % int1))
The cat is not big.
("cat" "is" "big" "-")
int1
((((triple7) -> (rule2 % int2)) triple1) -> (rule5 % int1))
The cat is not big.
("cat" "is" "big" "-")
int1
The cat visits the mouse.
("cat" "visits" "mouse" "+")
int2
The mouse eats the mouse.
("mouse" "eats" "mouse" "+")
((triple11) -> (rule3 % int1))
The mouse eats the mouse.
("mouse" "eats" "mouse" "+")
int1