The dog chases the tiger. The dog is rough. The dog is round. The tiger chases the dog. The tiger is nice. The tiger is rough. The tiger is round. The tiger is young. The tiger likes the dog. The tiger sees the dog. If something is round then it likes the dog. If something is nice then it likes the tiger.
The dog chases the tiger.
("dog" "chases" "tiger" "+")
The dog is rough.
("dog" "is" "rough" "+")
The dog is round.
("dog" "is" "round" "+")
The tiger chases the dog.
("tiger" "chases" "dog" "+")
The tiger is nice.
("tiger" "is" "nice" "+")
The tiger is rough.
("tiger" "is" "rough" "+")
The tiger is round.
("tiger" "is" "round" "+")
The tiger is young.
("tiger" "is" "young" "+")
The tiger likes the dog.
("tiger" "likes" "dog" "+")
The tiger sees the dog.
("tiger" "sees" "dog" "+")
If something is round then it likes the dog.
((("something" "is" "round" "+")) -> ("something" "likes" "dog" "+"))
If something is nice then it likes the tiger.
((("something" "is" "nice" "+")) -> ("something" "likes" "tiger" "+"))
The tiger is round.
True
1
proof
[(triple7)]
("tiger" "is" "round" "+")
triple7
The tiger does not chase the dog.
False
1
inv-proof
[(triple4)]
("tiger" "chases" "dog" "-")
triple4
The dog does not like the tiger.
Unknown
inv-rconc
[@1: The dog likes the tiger.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("dog" "likes" "tiger" "-")
The tiger is kind.
Unknown
random
[@0: The tiger is kind.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "kind" "+")
@0: The dog chases the tiger.[(triple1)] The dog is rough.[(triple2)] The dog is round.[(triple3)] The tiger chases the dog.[(triple4)] The tiger is nice.[(triple5)] The tiger is rough.[(triple6)] The tiger is round.[(triple7)] The tiger is young.[(triple8)] The tiger likes the dog.[(triple9 OR ((triple7) -> rule1))] The tiger sees the dog.[(triple10)] @1: The dog likes the dog.[(((triple3) -> rule1))] The tiger likes the tiger.[(((triple5) -> rule2))]
The dog chases the tiger.
("dog" "chases" "tiger" "+")
triple1
The dog is rough.
("dog" "is" "rough" "+")
triple2
The dog is round.
("dog" "is" "round" "+")
triple3
The tiger chases the dog.
("tiger" "chases" "dog" "+")
triple4
The tiger is nice.
("tiger" "is" "nice" "+")
triple5
The tiger is rough.
("tiger" "is" "rough" "+")
triple6
The tiger is round.
("tiger" "is" "round" "+")
triple7
The tiger is young.
("tiger" "is" "young" "+")
triple8
The tiger likes the dog.
("tiger" "likes" "dog" "+")
triple9
((triple7) -> (rule1 % int1))
The tiger likes the dog.
("tiger" "likes" "dog" "+")
int1
The tiger sees the dog.
("tiger" "sees" "dog" "+")
triple10
The dog likes the dog.
("dog" "likes" "dog" "+")
((triple3) -> (rule1 % int1))
The dog likes the dog.
("dog" "likes" "dog" "+")
int1
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
((triple5) -> (rule2 % int1))
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int1