The mouse is big. The mouse is kind. The mouse is not nice. The mouse is rough. The mouse is not round. The mouse likes the tiger. The mouse sees the tiger. The mouse visits the tiger. The tiger is big. The tiger is rough. The tiger is round. The tiger likes the mouse. If the mouse visits the tiger then the tiger visits the mouse. If someone is kind then they like the tiger. If the mouse does not visit the tiger then the mouse does not like the tiger.
The mouse is big.
("mouse" "is" "big" "+")
The mouse is kind.
("mouse" "is" "kind" "+")
The mouse is not nice.
("mouse" "is" "nice" "-")
The mouse is rough.
("mouse" "is" "rough" "+")
The mouse is not round.
("mouse" "is" "round" "-")
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
The tiger is big.
("tiger" "is" "big" "+")
The tiger is rough.
("tiger" "is" "rough" "+")
The tiger is round.
("tiger" "is" "round" "+")
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
If the mouse visits the tiger then the tiger visits the mouse.
((("mouse" "visits" "tiger" "+")) -> ("tiger" "visits" "mouse" "+"))
If someone is kind then they like the tiger.
((("someone" "is" "kind" "+")) -> ("someone" "likes" "tiger" "+"))
If the mouse does not visit the tiger then the mouse does not like the tiger.
((("mouse" "visits" "tiger" "~")) -> ("mouse" "likes" "tiger" "-"))
The mouse is not nice.
True
1
proof
[(triple3)]
("mouse" "is" "nice" "-")
triple3
The mouse is not rough.
False
1
inv-proof
[(triple4)]
("mouse" "is" "rough" "-")
triple4
The tiger does not like the tiger.
Unknown
inv-rconc
[@1: The tiger likes the tiger.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("tiger" "likes" "tiger" "-")
The mouse sees the mouse.
Unknown
random
[@0: The mouse sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "sees" "mouse" "+")
@0: The mouse is big.[(triple1)] The mouse is kind.[(triple2)] The mouse is not nice.[(triple3)] The mouse is not round.[(triple5)] The mouse is rough.[(triple4)] The mouse likes the tiger.[(triple6 OR ((triple2) -> rule2))] The mouse sees the tiger.[(triple7)] The mouse visits the tiger.[(triple8)] The tiger is big.[(triple9)] The tiger is rough.[(triple10)] The tiger is round.[(triple11)] The tiger likes the mouse.[(triple12)] @1: The tiger visits the mouse.[(((triple8) -> rule1))]
The mouse is big.
("mouse" "is" "big" "+")
triple1
The mouse is kind.
("mouse" "is" "kind" "+")
triple2
The mouse is not nice.
("mouse" "is" "nice" "-")
triple3
The mouse is not round.
("mouse" "is" "round" "-")
triple5
The mouse is rough.
("mouse" "is" "rough" "+")
triple4
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
triple6
((triple2) -> (rule2 % int1))
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
int1
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
triple7
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
triple8
The tiger is big.
("tiger" "is" "big" "+")
triple9
The tiger is rough.
("tiger" "is" "rough" "+")
triple10
The tiger is round.
("tiger" "is" "round" "+")
triple11
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
triple12
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
((triple8) -> (rule1 % int1))
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
int1