The bear is big. The dog likes the tiger. The tiger is round. If the dog likes the tiger then the tiger visits the dog.
The bear is big.
("bear" "is" "big" "+")
The dog likes the tiger.
("dog" "likes" "tiger" "+")
The tiger is round.
("tiger" "is" "round" "+")
If the dog likes the tiger then the tiger visits the dog.
((("dog" "likes" "tiger" "+")) -> ("tiger" "visits" "dog" "+"))
The tiger is round.
True
1
proof
[(triple3)]
("tiger" "is" "round" "+")
triple3
The dog does not like the tiger.
False
1
inv-proof
[(triple2)]
("dog" "likes" "tiger" "-")
triple2
The tiger visits the dog.
True
2
proof
[(((triple2) -> rule1))]
("tiger" "visits" "dog" "+")
((triple2) -> (rule1 % int1))
The tiger visits the dog.
("tiger" "visits" "dog" "+")
int1
The tiger does not visit the dog.
False
2
inv-proof
[(((triple2) -> rule1))]
("tiger" "visits" "dog" "-")
((triple2) -> (rule1 % int1))
The tiger visits the dog.
("tiger" "visits" "dog" "+")
int1
The tiger does not chase the dog.
Unknown
inv-random
[@0: The tiger chases the dog.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "chases" "dog" "-")
The dog visits the bear.
Unknown
random
[@0: The dog visits the bear.[CWA. Example of deepest failure = (FAIL)]]
("dog" "visits" "bear" "+")
The bear does not chase the bear.
Unknown
inv-random
[@0: The bear chases the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "chases" "bear" "-")
The bear is round.
Unknown
random
[@0: The bear is round.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "round" "+")
@0: The bear is big.[(triple1)] The dog likes the tiger.[(triple2)] The tiger is round.[(triple3)] @1: The tiger visits the dog.[(((triple2) -> rule1))]
The bear is big.
("bear" "is" "big" "+")
triple1
The dog likes the tiger.
("dog" "likes" "tiger" "+")
triple2
The tiger is round.
("tiger" "is" "round" "+")
triple3
The tiger visits the dog.
("tiger" "visits" "dog" "+")
((triple2) -> (rule1 % int1))
The tiger visits the dog.
("tiger" "visits" "dog" "+")
int1