The dog is nice. The dog likes the tiger. The dog visits the tiger. The tiger is blue. The tiger is red. The tiger is rough. The tiger is round. The tiger likes the dog. The tiger sees the dog. The tiger visits the dog. If someone is blue then they like the tiger. If the tiger visits the dog then the tiger likes the dog. If the tiger is round then the tiger visits the dog.
The dog is nice.
("dog" "is" "nice" "+")
The dog likes the tiger.
("dog" "likes" "tiger" "+")
The dog visits the tiger.
("dog" "visits" "tiger" "+")
The tiger is blue.
("tiger" "is" "blue" "+")
The tiger is red.
("tiger" "is" "red" "+")
The tiger is rough.
("tiger" "is" "rough" "+")
The tiger is round.
("tiger" "is" "round" "+")
The tiger likes the dog.
("tiger" "likes" "dog" "+")
The tiger sees the dog.
("tiger" "sees" "dog" "+")
The tiger visits the dog.
("tiger" "visits" "dog" "+")
If someone is blue then they like the tiger.
((("someone" "is" "blue" "+")) -> ("someone" "likes" "tiger" "+"))
If the tiger visits the dog then the tiger likes the dog.
((("tiger" "visits" "dog" "+")) -> ("tiger" "likes" "dog" "+"))
If the tiger is round then the tiger visits the dog.
((("tiger" "is" "round" "+")) -> ("tiger" "visits" "dog" "+"))
The tiger is round.
True
1
proof
[(triple7)]
("tiger" "is" "round" "+")
triple7
The tiger is not blue.
False
1
inv-proof
[(triple4)]
("tiger" "is" "blue" "-")
triple4
The tiger likes the tiger.
True
2
proof
[(((triple4) -> rule1))]
("tiger" "likes" "tiger" "+")
((triple4) -> (rule1 % int1))
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int1
The tiger does not like the tiger.
False
2
inv-proof
[(((triple4) -> rule1))]
("tiger" "likes" "tiger" "-")
((triple4) -> (rule1 % int1))
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int1
The tiger is not nice.
Unknown
inv-random
[@0: The tiger is nice.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "nice" "-")
The dog sees the dog.
Unknown
random
[@0: The dog sees the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "sees" "dog" "+")
The dog does not see the tiger.
Unknown
inv-random
[@0: The dog sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("dog" "sees" "tiger" "-")
The dog likes the dog.
Unknown
random
[@0: The dog likes the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "likes" "dog" "+")
@0: The dog is nice.[(triple1)] The dog likes the tiger.[(triple2)] The dog visits the tiger.[(triple3)] The tiger is blue.[(triple4)] The tiger is red.[(triple5)] The tiger is rough.[(triple6)] The tiger is round.[(triple7)] The tiger likes the dog.[(triple8 OR ((triple10) -> rule2) OR ((((triple7) -> rule3)) -> rule2))] The tiger sees the dog.[(triple9)] The tiger visits the dog.[(triple10 OR ((triple7) -> rule3))] @1: The tiger likes the tiger.[(((triple4) -> rule1))]
The dog is nice.
("dog" "is" "nice" "+")
triple1
The dog likes the tiger.
("dog" "likes" "tiger" "+")
triple2
The dog visits the tiger.
("dog" "visits" "tiger" "+")
triple3
The tiger is blue.
("tiger" "is" "blue" "+")
triple4
The tiger is red.
("tiger" "is" "red" "+")
triple5
The tiger is rough.
("tiger" "is" "rough" "+")
triple6
The tiger is round.
("tiger" "is" "round" "+")
triple7
The tiger likes the dog.
("tiger" "likes" "dog" "+")
triple8
((triple10) -> (rule2 % int1))
The tiger likes the dog.
("tiger" "likes" "dog" "+")
int1
((((triple7) -> (rule3 % int2))) -> (rule2 % int1))
The tiger likes the dog.
("tiger" "likes" "dog" "+")
int1
The tiger visits the dog.
("tiger" "visits" "dog" "+")
int2
The tiger sees the dog.
("tiger" "sees" "dog" "+")
triple9
The tiger visits the dog.
("tiger" "visits" "dog" "+")
triple10
((triple7) -> (rule3 % int1))
The tiger visits the dog.
("tiger" "visits" "dog" "+")
int1
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
((triple4) -> (rule1 % int1))
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int1