The mouse chases the tiger. The mouse is big. The mouse is cold. The mouse is green. The mouse is kind. The mouse is nice. The mouse likes the tiger. The mouse visits the tiger. The tiger chases the mouse. The tiger is big. The tiger is cold. The tiger is green. The tiger is kind. The tiger likes the mouse. The tiger visits the mouse. If something likes the mouse then it visits the tiger.
The mouse chases the tiger.
("mouse" "chases" "tiger" "+")
The mouse is big.
("mouse" "is" "big" "+")
The mouse is cold.
("mouse" "is" "cold" "+")
The mouse is green.
("mouse" "is" "green" "+")
The mouse is kind.
("mouse" "is" "kind" "+")
The mouse is nice.
("mouse" "is" "nice" "+")
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
The tiger chases the mouse.
("tiger" "chases" "mouse" "+")
The tiger is big.
("tiger" "is" "big" "+")
The tiger is cold.
("tiger" "is" "cold" "+")
The tiger is green.
("tiger" "is" "green" "+")
The tiger is kind.
("tiger" "is" "kind" "+")
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
If something likes the mouse then it visits the tiger.
((("something" "likes" "mouse" "+")) -> ("something" "visits" "tiger" "+"))
The mouse likes the tiger.
True
1
proof
[(triple7)]
("mouse" "likes" "tiger" "+")
triple7
The mouse is not big.
False
1
inv-proof
[(triple2)]
("mouse" "is" "big" "-")
triple2
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 tiger is nice.
Unknown
random
[@0: The tiger is nice.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "nice" "+")
@0: The mouse chases the tiger.[(triple1)] The mouse is big.[(triple2)] The mouse is cold.[(triple3)] The mouse is green.[(triple4)] The mouse is kind.[(triple5)] The mouse is nice.[(triple6)] The mouse likes the tiger.[(triple7)] The mouse visits the tiger.[(triple8)] The tiger chases the mouse.[(triple9)] The tiger is big.[(triple10)] The tiger is cold.[(triple11)] The tiger is green.[(triple12)] The tiger is kind.[(triple13)] The tiger likes the mouse.[(triple14)] The tiger visits the mouse.[(triple15)] @1: The tiger visits the tiger.[(((triple14) -> rule1))]
The mouse chases the tiger.
("mouse" "chases" "tiger" "+")
triple1
The mouse is big.
("mouse" "is" "big" "+")
triple2
The mouse is cold.
("mouse" "is" "cold" "+")
triple3
The mouse is green.
("mouse" "is" "green" "+")
triple4
The mouse is kind.
("mouse" "is" "kind" "+")
triple5
The mouse is nice.
("mouse" "is" "nice" "+")
triple6
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
triple7
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
triple8
The tiger chases the mouse.
("tiger" "chases" "mouse" "+")
triple9
The tiger is big.
("tiger" "is" "big" "+")
triple10
The tiger is cold.
("tiger" "is" "cold" "+")
triple11
The tiger is green.
("tiger" "is" "green" "+")
triple12
The tiger is kind.
("tiger" "is" "kind" "+")
triple13
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
triple14
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
triple15
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
((triple14) -> (rule1 % int1))
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int1