The cat is rough. The cat is round. The cat likes the tiger. The cat sees the mouse. The mouse is rough. The mouse is not round. The mouse likes the cat. The mouse likes the tiger. The mouse needs the cat. The mouse needs the tiger. The mouse sees the cat. The mouse does not see the tiger. The tiger is nice. The tiger does not like the mouse. The tiger needs the cat. The tiger sees the cat. If the mouse does not see the cat then the mouse is not cold. If someone is nice then they need the cat. If someone likes the cat then the cat needs the mouse. If someone likes the cat then the cat sees the mouse. If the cat likes the mouse then the cat sees the tiger. If the tiger is round and the tiger does not need the cat then the cat sees the tiger.
The cat is rough.
("cat" "is" "rough" "+")
The cat is round.
("cat" "is" "round" "+")
The cat likes the tiger.
("cat" "likes" "tiger" "+")
The cat sees the mouse.
("cat" "sees" "mouse" "+")
The mouse is rough.
("mouse" "is" "rough" "+")
The mouse is not round.
("mouse" "is" "round" "-")
The mouse likes the cat.
("mouse" "likes" "cat" "+")
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
The mouse needs the cat.
("mouse" "needs" "cat" "+")
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
The mouse sees the cat.
("mouse" "sees" "cat" "+")
The mouse does not see the tiger.
("mouse" "sees" "tiger" "-")
The tiger is nice.
("tiger" "is" "nice" "+")
The tiger does not like the mouse.
("tiger" "likes" "mouse" "-")
The tiger needs the cat.
("tiger" "needs" "cat" "+")
The tiger sees the cat.
("tiger" "sees" "cat" "+")
If the mouse does not see the cat then the mouse is not cold.
((("mouse" "sees" "cat" "~")) -> ("mouse" "is" "cold" "-"))
If someone is nice then they need the cat.
((("someone" "is" "nice" "+")) -> ("someone" "needs" "cat" "+"))
If someone likes the cat then the cat needs the mouse.
((("someone" "likes" "cat" "+")) -> ("cat" "needs" "mouse" "+"))
If someone likes the cat then the cat sees the mouse.
((("someone" "likes" "cat" "+")) -> ("cat" "sees" "mouse" "+"))
If the cat likes the mouse then the cat sees the tiger.
((("cat" "likes" "mouse" "+")) -> ("cat" "sees" "tiger" "+"))
If the tiger is round and the tiger does not need the cat then the cat sees the tiger.
((("tiger" "is" "round" "+") ("tiger" "needs" "cat" "~")) -> ("cat" "sees" "tiger" "+"))
The tiger sees the cat.
True
1
proof
[(triple16)]
("tiger" "sees" "cat" "+")
triple16
The mouse does not like the tiger.
False
1
inv-proof
[(triple8)]
("mouse" "likes" "tiger" "-")
triple8
The cat does not need the cat.
Unknown
inv-rconc
[@1: The cat needs the cat.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cat" "needs" "cat" "-")
The tiger sees the tiger.
Unknown
random
[@0: The tiger sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "tiger" "+")
@0: The cat is rough.[(triple1)] The cat is round.[(triple2)] The cat likes the tiger.[(triple3)] The cat sees the mouse.[(triple4 OR ((triple7) -> rule4))] The mouse does not see the tiger.[(triple12)] The mouse is not round.[(triple6)] The mouse is rough.[(triple5)] The mouse likes the cat.[(triple7)] The mouse likes the tiger.[(triple8)] The mouse needs the cat.[(triple9)] The mouse needs the tiger.[(triple10)] The mouse sees the cat.[(triple11)] The tiger does not like the mouse.[(triple14)] The tiger is nice.[(triple13)] The tiger needs the cat.[(triple15 OR ((triple13) -> rule2))] The tiger sees the cat.[(triple16)] @1: The cat needs the mouse.[(((triple7) -> rule3))]
The cat is rough.
("cat" "is" "rough" "+")
triple1
The cat is round.
("cat" "is" "round" "+")
triple2
The cat likes the tiger.
("cat" "likes" "tiger" "+")
triple3
The cat sees the mouse.
("cat" "sees" "mouse" "+")
triple4
((triple7) -> (rule4 % int1))
The cat sees the mouse.
("cat" "sees" "mouse" "+")
int1
The mouse does not see the tiger.
("mouse" "sees" "tiger" "-")
triple12
The mouse is not round.
("mouse" "is" "round" "-")
triple6
The mouse is rough.
("mouse" "is" "rough" "+")
triple5
The mouse likes the cat.
("mouse" "likes" "cat" "+")
triple7
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
triple8
The mouse needs the cat.
("mouse" "needs" "cat" "+")
triple9
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
triple10
The mouse sees the cat.
("mouse" "sees" "cat" "+")
triple11
The tiger does not like the mouse.
("tiger" "likes" "mouse" "-")
triple14
The tiger is nice.
("tiger" "is" "nice" "+")
triple13
The tiger needs the cat.
("tiger" "needs" "cat" "+")
triple15
((triple13) -> (rule2 % int1))
The tiger needs the cat.
("tiger" "needs" "cat" "+")
int1
The tiger sees the cat.
("tiger" "sees" "cat" "+")
triple16
The cat needs the mouse.
("cat" "needs" "mouse" "+")
((triple7) -> (rule3 % int1))
The cat needs the mouse.
("cat" "needs" "mouse" "+")
int1