The dog chases the tiger. The dog is blue. The dog likes the rabbit. The rabbit chases the dog. The rabbit chases the tiger. The rabbit needs the dog. The tiger chases the dog. The tiger chases the rabbit. The tiger is cold. The tiger likes the dog. The tiger needs the dog. The tiger needs the rabbit. If something is blue then it is rough. If something needs the rabbit then the rabbit is blue. If something likes the rabbit then the rabbit is round.
The dog chases the tiger.
("dog" "chases" "tiger" "+")
The dog is blue.
("dog" "is" "blue" "+")
The dog likes the rabbit.
("dog" "likes" "rabbit" "+")
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
The rabbit chases the tiger.
("rabbit" "chases" "tiger" "+")
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
The tiger chases the dog.
("tiger" "chases" "dog" "+")
The tiger chases the rabbit.
("tiger" "chases" "rabbit" "+")
The tiger is cold.
("tiger" "is" "cold" "+")
The tiger likes the dog.
("tiger" "likes" "dog" "+")
The tiger needs the dog.
("tiger" "needs" "dog" "+")
The tiger needs the rabbit.
("tiger" "needs" "rabbit" "+")
If something is blue then it is rough.
((("something" "is" "blue" "+")) -> ("something" "is" "rough" "+"))
If something needs the rabbit then the rabbit is blue.
((("something" "needs" "rabbit" "+")) -> ("rabbit" "is" "blue" "+"))
If something likes the rabbit then the rabbit is round.
((("something" "likes" "rabbit" "+")) -> ("rabbit" "is" "round" "+"))
The tiger needs the rabbit.
True
1
proof
[(triple12)]
("tiger" "needs" "rabbit" "+")
triple12
The tiger does not need the dog.
False
1
inv-proof
[(triple11)]
("tiger" "needs" "dog" "-")
triple11
The rabbit is blue.
True
2
proof
[(((triple12) -> rule2))]
("rabbit" "is" "blue" "+")
((triple12) -> (rule2 % int1))
The rabbit is blue.
("rabbit" "is" "blue" "+")
int1
The rabbit is not blue.
False
2
inv-proof
[(((triple12) -> rule2))]
("rabbit" "is" "blue" "-")
((triple12) -> (rule2 % int1))
The rabbit is blue.
("rabbit" "is" "blue" "+")
int1
The rabbit is rough.
True
3
proof
[(((((triple12) -> rule2)) -> rule1))]
("rabbit" "is" "rough" "+")
((((triple12) -> (rule2 % int2))) -> (rule1 % int1))
The rabbit is rough.
("rabbit" "is" "rough" "+")
int1
The rabbit is blue.
("rabbit" "is" "blue" "+")
int2
The rabbit is not rough.
False
3
inv-proof
[(((((triple12) -> rule2)) -> rule1))]
("rabbit" "is" "rough" "-")
((((triple12) -> (rule2 % int2))) -> (rule1 % int1))
The rabbit is rough.
("rabbit" "is" "rough" "+")
int1
The rabbit is blue.
("rabbit" "is" "blue" "+")
int2
The tiger is not rough.
Unknown
inv-rconc
[@1: The tiger is rough.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("tiger" "is" "rough" "-")
The tiger likes the tiger.
Unknown
random
[@0: The tiger likes the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "likes" "tiger" "+")
The rabbit does not like the rabbit.
Unknown
inv-random
[@0: The rabbit likes the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "likes" "rabbit" "-")
The tiger is blue.
Unknown
random
[@0: The tiger is blue.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "blue" "+")
The tiger does not need the tiger.
Unknown
inv-random
[@0: The tiger needs the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "needs" "tiger" "-")
The tiger is round.
Unknown
random
[@0: The tiger is round.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "round" "+")
@0: The dog chases the tiger.[(triple1)] The dog is blue.[(triple2)] The dog likes the rabbit.[(triple3)] The rabbit chases the dog.[(triple4)] The rabbit chases the tiger.[(triple5)] The rabbit needs the dog.[(triple6)] The tiger chases the dog.[(triple7)] The tiger chases the rabbit.[(triple8)] The tiger is cold.[(triple9)] The tiger likes the dog.[(triple10)] The tiger needs the dog.[(triple11)] The tiger needs the rabbit.[(triple12)] @1: The dog is rough.[(((triple2) -> rule1))] The rabbit is blue.[(((triple12) -> rule2))] The rabbit is round.[(((triple3) -> rule3))] @2: The rabbit is rough.[(((((triple12) -> rule2)) -> rule1))]
The dog chases the tiger.
("dog" "chases" "tiger" "+")
triple1
The dog is blue.
("dog" "is" "blue" "+")
triple2
The dog likes the rabbit.
("dog" "likes" "rabbit" "+")
triple3
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
triple4
The rabbit chases the tiger.
("rabbit" "chases" "tiger" "+")
triple5
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
triple6
The tiger chases the dog.
("tiger" "chases" "dog" "+")
triple7
The tiger chases the rabbit.
("tiger" "chases" "rabbit" "+")
triple8
The tiger is cold.
("tiger" "is" "cold" "+")
triple9
The tiger likes the dog.
("tiger" "likes" "dog" "+")
triple10
The tiger needs the dog.
("tiger" "needs" "dog" "+")
triple11
The tiger needs the rabbit.
("tiger" "needs" "rabbit" "+")
triple12
The dog is rough.
("dog" "is" "rough" "+")
((triple2) -> (rule1 % int1))
The dog is rough.
("dog" "is" "rough" "+")
int1
The rabbit is blue.
("rabbit" "is" "blue" "+")
((triple12) -> (rule2 % int1))
The rabbit is blue.
("rabbit" "is" "blue" "+")
int1
The rabbit is round.
("rabbit" "is" "round" "+")
((triple3) -> (rule3 % int1))
The rabbit is round.
("rabbit" "is" "round" "+")
int1
The rabbit is rough.
("rabbit" "is" "rough" "+")
((((triple12) -> (rule2 % int2))) -> (rule1 % int1))
The rabbit is rough.
("rabbit" "is" "rough" "+")
int1
The rabbit is blue.
("rabbit" "is" "blue" "+")
int2