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