The cat is blue. The cat is green. The cat is young. The cat does not like the rabbit. The cat does not like the tiger. The cat sees the rabbit. The cat sees the tiger. The cat does not visit the rabbit. The cat does not visit the tiger. The rabbit is not green. The rabbit is young. The rabbit sees the tiger. The tiger likes the cat. The tiger sees the cat. The tiger sees the rabbit. The tiger visits the rabbit. If someone is cold and they visit the rabbit then they like the tiger. If someone visits the rabbit then they like the tiger. If someone sees the rabbit and they do not like the cat then they like the tiger. If the tiger likes the cat and the tiger does not see the rabbit then the cat does not visit the tiger. If the rabbit likes the tiger and the tiger does not visit the rabbit then the rabbit does not see the tiger. If someone likes the tiger then the tiger is not young. If someone is blue and cold then they visit the tiger. All green people are young.
The cat is blue.
("cat" "is" "blue" "+")
The cat is green.
("cat" "is" "green" "+")
The cat is young.
("cat" "is" "young" "+")
The cat does not like the rabbit.
("cat" "likes" "rabbit" "-")
The cat does not like the tiger.
("cat" "likes" "tiger" "-")
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
The cat sees the tiger.
("cat" "sees" "tiger" "+")
The cat does not visit the rabbit.
("cat" "visits" "rabbit" "-")
The cat does not visit the tiger.
("cat" "visits" "tiger" "-")
The rabbit is not green.
("rabbit" "is" "green" "-")
The rabbit is young.
("rabbit" "is" "young" "+")
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
The tiger likes the cat.
("tiger" "likes" "cat" "+")
The tiger sees the cat.
("tiger" "sees" "cat" "+")
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
If someone is cold and they visit the rabbit then they like the tiger.
((("someone" "is" "cold" "+") ("someone" "visits" "rabbit" "+")) -> ("someone" "likes" "tiger" "+"))
If someone visits the rabbit then they like the tiger.
((("someone" "visits" "rabbit" "+")) -> ("someone" "likes" "tiger" "+"))
If someone sees the rabbit and they do not like the cat then they like the tiger.
((("someone" "sees" "rabbit" "+") ("someone" "likes" "cat" "~")) -> ("someone" "likes" "tiger" "+"))
If the tiger likes the cat and the tiger does not see the rabbit then the cat does not visit the tiger.
((("tiger" "likes" "cat" "+") ("tiger" "sees" "rabbit" "~")) -> ("cat" "visits" "tiger" "-"))
If the rabbit likes the tiger and the tiger does not visit the rabbit then the rabbit does not see the tiger.
((("rabbit" "likes" "tiger" "+") ("tiger" "visits" "rabbit" "~")) -> ("rabbit" "sees" "tiger" "-"))
If someone likes the tiger then the tiger is not young.
((("someone" "likes" "tiger" "+")) -> ("tiger" "is" "young" "-"))
If someone is blue and cold then they visit the tiger.
((("someone" "is" "blue" "+") ("someone" "is" "cold" "+")) -> ("someone" "visits" "tiger" "+"))
All green people are young.
((("someone" "is" "green" "+")) -> ("someone" "is" "young" "+"))
The tiger visits the rabbit.
True
1
proof
[(triple16)]
("tiger" "visits" "rabbit" "+")
triple16
The cat is not young.
False
1
inv-proof
[(triple3 OR ((triple2) -> rule8))]
("cat" "is" "young" "-")
triple3
((triple2) -> (rule8 % int1))
The cat is young.
("cat" "is" "young" "+")
int1
The tiger likes the tiger.
True
2
proof
[(((triple16) -> rule2))]
("tiger" "likes" "tiger" "+")
((triple16) -> (rule2 % int1))
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int1
The tiger does not like the tiger.
False
2
inv-proof
[(((triple16) -> rule2))]
("tiger" "likes" "tiger" "-")
((triple16) -> (rule2 % int1))
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int1
The tiger is not young.
True
3
proof
[(((((triple16) -> rule2)) -> rule6))]
("tiger" "is" "young" "-")
((((triple16) -> (rule2 % int2))) -> (rule6 % int1))
The tiger is not young.
("tiger" "is" "young" "-")
int1
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int2
The tiger is young.
False
3
inv-proof
[(((((triple16) -> rule2)) -> rule6))]
("tiger" "is" "young" "+")
((((triple16) -> (rule2 % int2))) -> (rule6 % int1))
The tiger is not young.
("tiger" "is" "young" "-")
int1
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int2
The rabbit does not like the tiger.
Unknown
inv-rconc
[@1: The rabbit likes the tiger.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("rabbit" "likes" "tiger" "-")
The rabbit visits the tiger.
Unknown
rconc
[@1: The rabbit visits the tiger.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("rabbit" "visits" "tiger" "+")
The tiger does not visit the tiger.
Unknown
inv-rconc
[@1: The tiger visits the tiger.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("tiger" "visits" "tiger" "-")
The rabbit likes the rabbit.
Unknown
random
[@0: The rabbit likes the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "likes" "rabbit" "+")
The tiger does not visit the cat.
Unknown
inv-random
[@0: The tiger visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "visits" "cat" "-")
The rabbit visits the cat.
Unknown
random
[@0: The rabbit visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "visits" "cat" "+")
@0: The cat does not like the rabbit.[(triple4)] The cat does not like the tiger.[(triple5)] The cat does not visit the rabbit.[(triple8)] The cat does not visit the tiger.[(triple9)] The cat is blue.[(triple1)] The cat is green.[(triple2)] The cat is young.[(triple3 OR ((triple2) -> rule8))] The cat sees the rabbit.[(triple6)] The cat sees the tiger.[(triple7)] The rabbit is not green.[(triple10)] The rabbit is young.[(triple11)] The rabbit sees the tiger.[(triple12)] The tiger likes the cat.[(triple13)] The tiger sees the cat.[(triple14)] The tiger sees the rabbit.[(triple15)] The tiger visits the rabbit.[(triple16)] @1: The tiger likes the tiger.[(((triple16) -> rule2))] @2: The tiger is not young.[(((((triple16) -> rule2)) -> rule6))]
The cat does not like the rabbit.
("cat" "likes" "rabbit" "-")
triple4
The cat does not like the tiger.
("cat" "likes" "tiger" "-")
triple5
The cat does not visit the rabbit.
("cat" "visits" "rabbit" "-")
triple8
The cat does not visit the tiger.
("cat" "visits" "tiger" "-")
triple9
The cat is blue.
("cat" "is" "blue" "+")
triple1
The cat is green.
("cat" "is" "green" "+")
triple2
The cat is young.
("cat" "is" "young" "+")
triple3
((triple2) -> (rule8 % int1))
The cat is young.
("cat" "is" "young" "+")
int1
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
triple6
The cat sees the tiger.
("cat" "sees" "tiger" "+")
triple7
The rabbit is not green.
("rabbit" "is" "green" "-")
triple10
The rabbit is young.
("rabbit" "is" "young" "+")
triple11
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
triple12
The tiger likes the cat.
("tiger" "likes" "cat" "+")
triple13
The tiger sees the cat.
("tiger" "sees" "cat" "+")
triple14
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
triple15
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
triple16
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
((triple16) -> (rule2 % int1))
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int1
The tiger is not young.
("tiger" "is" "young" "-")
((((triple16) -> (rule2 % int2))) -> (rule6 % int1))
The tiger is not young.
("tiger" "is" "young" "-")
int1
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int2