The cat is nice. The cat likes the tiger. The cat sees the tiger. The cow likes the tiger. The tiger is not nice. The tiger likes the cow. The tiger needs the cat. The tiger needs the cow. The tiger sees the cat. The tiger sees the cow. If something sees the cat then the cat is kind.
The cat is nice.
("cat" "is" "nice" "+")
The cat likes the tiger.
("cat" "likes" "tiger" "+")
The cat sees the tiger.
("cat" "sees" "tiger" "+")
The cow likes the tiger.
("cow" "likes" "tiger" "+")
The tiger is not nice.
("tiger" "is" "nice" "-")
The tiger likes the cow.
("tiger" "likes" "cow" "+")
The tiger needs the cat.
("tiger" "needs" "cat" "+")
The tiger needs the cow.
("tiger" "needs" "cow" "+")
The tiger sees the cat.
("tiger" "sees" "cat" "+")
The tiger sees the cow.
("tiger" "sees" "cow" "+")
If something sees the cat then the cat is kind.
((("something" "sees" "cat" "+")) -> ("cat" "is" "kind" "+"))
The tiger sees the cow.
True
1
proof
[(triple10)]
("tiger" "sees" "cow" "+")
triple10
The tiger does not see the cow.
False
1
inv-proof
[(triple10)]
("tiger" "sees" "cow" "-")
triple10
The tiger is not red.
Unknown
inv-random
[@0: The tiger is red.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "red" "-")
The cow is red.
Unknown
random
[@0: The cow is red.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "red" "+")
@0: The cat is nice.[(triple1)] The cat likes the tiger.[(triple2)] The cat sees the tiger.[(triple3)] The cow likes the tiger.[(triple4)] The tiger is not nice.[(triple5)] The tiger likes the cow.[(triple6)] The tiger needs the cat.[(triple7)] The tiger needs the cow.[(triple8)] The tiger sees the cat.[(triple9)] The tiger sees the cow.[(triple10)] @1: The cat is kind.[(((triple9) -> rule1))]
The cat is nice.
("cat" "is" "nice" "+")
triple1
The cat likes the tiger.
("cat" "likes" "tiger" "+")
triple2
The cat sees the tiger.
("cat" "sees" "tiger" "+")
triple3
The cow likes the tiger.
("cow" "likes" "tiger" "+")
triple4
The tiger is not nice.
("tiger" "is" "nice" "-")
triple5
The tiger likes the cow.
("tiger" "likes" "cow" "+")
triple6
The tiger needs the cat.
("tiger" "needs" "cat" "+")
triple7
The tiger needs the cow.
("tiger" "needs" "cow" "+")
triple8
The tiger sees the cat.
("tiger" "sees" "cat" "+")
triple9
The tiger sees the cow.
("tiger" "sees" "cow" "+")
triple10
The cat is kind.
("cat" "is" "kind" "+")
((triple9) -> (rule1 % int1))
The cat is kind.
("cat" "is" "kind" "+")
int1