The cat is big. The cat is green. The cat is rough. The cat is not round. The cat likes the mouse. The cat needs the mouse. The cat visits the mouse. The mouse is green. The mouse is not rough. The mouse is round. The mouse likes the cat. The mouse needs the cat. If something is round and it likes the cat then it likes the mouse. If something is round and it visits the cat then the cat is rough.
The cat is big.
("cat" "is" "big" "+")
The cat is green.
("cat" "is" "green" "+")
The cat is rough.
("cat" "is" "rough" "+")
The cat is not round.
("cat" "is" "round" "-")
The cat likes the mouse.
("cat" "likes" "mouse" "+")
The cat needs the mouse.
("cat" "needs" "mouse" "+")
The cat visits the mouse.
("cat" "visits" "mouse" "+")
The mouse is green.
("mouse" "is" "green" "+")
The mouse is not rough.
("mouse" "is" "rough" "-")
The mouse is round.
("mouse" "is" "round" "+")
The mouse likes the cat.
("mouse" "likes" "cat" "+")
The mouse needs the cat.
("mouse" "needs" "cat" "+")
If something is round and it likes the cat then it likes the mouse.
((("something" "is" "round" "+") ("something" "likes" "cat" "+")) -> ("something" "likes" "mouse" "+"))
If something is round and it visits the cat then the cat is rough.
((("something" "is" "round" "+") ("something" "visits" "cat" "+")) -> ("cat" "is" "rough" "+"))
The cat visits the mouse.
True
1
proof
[(triple7)]
("cat" "visits" "mouse" "+")
triple7
The mouse does not like the cat.
False
1
inv-proof
[(triple11)]
("mouse" "likes" "cat" "-")
triple11
The mouse is not big.
Unknown
inv-random
[@0: The mouse is big.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "big" "-")
The mouse visits the cat.
Unknown
random
[@0: The mouse visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "visits" "cat" "+")
@0: The cat is big.[(triple1)] The cat is green.[(triple2)] The cat is not round.[(triple4)] The cat is rough.[(triple3)] The cat likes the mouse.[(triple5)] The cat needs the mouse.[(triple6)] The cat visits the mouse.[(triple7)] The mouse is green.[(triple8)] The mouse is not rough.[(triple9)] The mouse is round.[(triple10)] The mouse likes the cat.[(triple11)] The mouse needs the cat.[(triple12)] @1: The mouse likes the mouse.[(((triple10 triple11) -> rule1))]
The cat is big.
("cat" "is" "big" "+")
triple1
The cat is green.
("cat" "is" "green" "+")
triple2
The cat is not round.
("cat" "is" "round" "-")
triple4
The cat is rough.
("cat" "is" "rough" "+")
triple3
The cat likes the mouse.
("cat" "likes" "mouse" "+")
triple5
The cat needs the mouse.
("cat" "needs" "mouse" "+")
triple6
The cat visits the mouse.
("cat" "visits" "mouse" "+")
triple7
The mouse is green.
("mouse" "is" "green" "+")
triple8
The mouse is not rough.
("mouse" "is" "rough" "-")
triple9
The mouse is round.
("mouse" "is" "round" "+")
triple10
The mouse likes the cat.
("mouse" "likes" "cat" "+")
triple11
The mouse needs the cat.
("mouse" "needs" "cat" "+")
triple12
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
((triple10 triple11) -> (rule1 % int1))
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int1