The cat needs the cow. The cow is young. The cow likes the tiger. The cow needs the rabbit. The rabbit is young. The rabbit likes the cat. The tiger is blue. The tiger likes the rabbit. The tiger needs the cat. The tiger sees the rabbit. If someone likes the cow and the cow likes the tiger then the tiger likes the cow. If the tiger needs the rabbit then the tiger sees the rabbit. If someone sees the tiger and the tiger likes the rabbit then they like the tiger. If someone likes the cow then they like the rabbit. All young people are red. If the cow needs the tiger and the cow needs the rabbit then the tiger likes the cow. If someone is red then they see the tiger. If someone likes the tiger and they see the tiger then they are red.
The cat needs the cow.
("cat" "needs" "cow" "+")
The cow is young.
("cow" "is" "young" "+")
The cow likes the tiger.
("cow" "likes" "tiger" "+")
The cow needs the rabbit.
("cow" "needs" "rabbit" "+")
The rabbit is young.
("rabbit" "is" "young" "+")
The rabbit likes the cat.
("rabbit" "likes" "cat" "+")
The tiger is blue.
("tiger" "is" "blue" "+")
The tiger likes the rabbit.
("tiger" "likes" "rabbit" "+")
The tiger needs the cat.
("tiger" "needs" "cat" "+")
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
If someone likes the cow and the cow likes the tiger then the tiger likes the cow.
((("someone" "likes" "cow" "+") ("cow" "likes" "tiger" "+")) -> ("tiger" "likes" "cow" "+"))
If the tiger needs the rabbit then the tiger sees the rabbit.
((("tiger" "needs" "rabbit" "+")) -> ("tiger" "sees" "rabbit" "+"))
If someone sees the tiger and the tiger likes the rabbit then they like the tiger.
((("someone" "sees" "tiger" "+") ("tiger" "likes" "rabbit" "+")) -> ("someone" "likes" "tiger" "+"))
If someone likes the cow then they like the rabbit.
((("someone" "likes" "cow" "+")) -> ("someone" "likes" "rabbit" "+"))
All young people are red.
((("someone" "is" "young" "+")) -> ("someone" "is" "red" "+"))
If the cow needs the tiger and the cow needs the rabbit then the tiger likes the cow.
((("cow" "needs" "tiger" "+") ("cow" "needs" "rabbit" "+")) -> ("tiger" "likes" "cow" "+"))
If someone is red then they see the tiger.
((("someone" "is" "red" "+")) -> ("someone" "sees" "tiger" "+"))
If someone likes the tiger and they see the tiger then they are red.
((("someone" "likes" "tiger" "+") ("someone" "sees" "tiger" "+")) -> ("someone" "is" "red" "+"))
The cow needs the rabbit.
True
1
proof
[(triple4)]
("cow" "needs" "rabbit" "+")
triple4
The cow is not young.
False
1
inv-proof
[(triple2)]
("cow" "is" "young" "-")
triple2
The cow is red.
True
2
proof
[(((triple2) -> rule5))]
("cow" "is" "red" "+")
((triple2) -> (rule5 % int1))
The cow is red.
("cow" "is" "red" "+")
int1
The cow is not red.
False
2
inv-proof
[(((triple2) -> rule5))]
("cow" "is" "red" "-")
((triple2) -> (rule5 % int1))
The cow is red.
("cow" "is" "red" "+")
int1
The rabbit sees the tiger.
True
3
proof
[(((((triple5) -> rule5)) -> rule7))]
("rabbit" "sees" "tiger" "+")
((((triple5) -> (rule5 % int2))) -> (rule7 % int1))
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
int1
The rabbit is red.
("rabbit" "is" "red" "+")
int2
The cow does not see the tiger.
False
3
inv-proof
[(((((triple2) -> rule5)) -> rule7))]
("cow" "sees" "tiger" "-")
((((triple2) -> (rule5 % int2))) -> (rule7 % int1))
The cow sees the tiger.
("cow" "sees" "tiger" "+")
int1
The cow is red.
("cow" "is" "red" "+")
int2
The rabbit likes the tiger.
True
5
proof
[(((((((triple5) -> rule5)) -> rule7) triple8) -> rule3))]
("rabbit" "likes" "tiger" "+")
((((((triple5) -> (rule5 % int3))) -> (rule7 % int2)) triple8) -> (rule3 % int1))
The rabbit likes the tiger.
("rabbit" "likes" "tiger" "+")
int1
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
int2
The rabbit is red.
("rabbit" "is" "red" "+")
int3
The rabbit does not like the tiger.
False
5
inv-proof
[(((((((triple5) -> rule5)) -> rule7) triple8) -> rule3))]
("rabbit" "likes" "tiger" "-")
((((((triple5) -> (rule5 % int3))) -> (rule7 % int2)) triple8) -> (rule3 % int1))
The rabbit likes the tiger.
("rabbit" "likes" "tiger" "+")
int1
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
int2
The rabbit is red.
("rabbit" "is" "red" "+")
int3
The tiger is not red.
Unknown
inv-rconc
[@3: The tiger is red.[CWA. Example of deepest failure = (rule8 <- rule7 <- rule5 <- FAIL)]]
("tiger" "is" "red" "-")
The tiger sees the tiger.
Unknown
rconc
[@2: The tiger sees the tiger.[CWA. Example of deepest failure = (rule7 <- rule5 <- FAIL)]]
("tiger" "sees" "tiger" "+")
The cat does not like the tiger.
Unknown
inv-rconc
[@3: The cat likes the tiger.[CWA. Example of deepest failure = (rule3 <- rule7 <- rule5 <- FAIL)]]
("cat" "likes" "tiger" "-")
The tiger likes the cow.
Unknown
rconc
[@2: The tiger likes the cow.[CWA. Example of deepest failure = (rule1 <- rule6 <- FAIL)]]
("tiger" "likes" "cow" "+")
The cow does not see the cat.
Unknown
inv-random
[@0: The cow sees the cat.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "cat" "-")
The cat sees the rabbit.
Unknown
random
[@0: The cat sees the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("cat" "sees" "rabbit" "+")
The tiger is not green.
Unknown
inv-random
[@0: The tiger is green.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "green" "-")
The cat is green.
Unknown
random
[@0: The cat is green.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "green" "+")
@0: The cat needs the cow.[(triple1)] The cow is young.[(triple2)] The cow likes the tiger.[(triple3 OR ((((((triple2) -> rule5)) -> rule7) triple8) -> rule3))] The cow needs the rabbit.[(triple4)] The rabbit is young.[(triple5)] The rabbit likes the cat.[(triple6)] The tiger is blue.[(triple7)] The tiger likes the rabbit.[(triple8)] The tiger needs the cat.[(triple9)] The tiger sees the rabbit.[(triple10)] @1: The cow is red.[(((triple2) -> rule5))] The rabbit is red.[(((triple5) -> rule5))] @2: The cow sees the tiger.[(((((triple2) -> rule5)) -> rule7))] The rabbit sees the tiger.[(((((triple5) -> rule5)) -> rule7))] @3: The rabbit likes the tiger.[(((((((triple5) -> rule5)) -> rule7) triple8) -> rule3))]
The cat needs the cow.
("cat" "needs" "cow" "+")
triple1
The cow is young.
("cow" "is" "young" "+")
triple2
The cow likes the tiger.
("cow" "likes" "tiger" "+")
triple3
((((((triple2) -> (rule5 % int3))) -> (rule7 % int2)) triple8) -> (rule3 % int1))
The cow likes the tiger.
("cow" "likes" "tiger" "+")
int1
The cow sees the tiger.
("cow" "sees" "tiger" "+")
int2
The cow is red.
("cow" "is" "red" "+")
int3
The cow needs the rabbit.
("cow" "needs" "rabbit" "+")
triple4
The rabbit is young.
("rabbit" "is" "young" "+")
triple5
The rabbit likes the cat.
("rabbit" "likes" "cat" "+")
triple6
The tiger is blue.
("tiger" "is" "blue" "+")
triple7
The tiger likes the rabbit.
("tiger" "likes" "rabbit" "+")
triple8
The tiger needs the cat.
("tiger" "needs" "cat" "+")
triple9
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
triple10
The cow is red.
("cow" "is" "red" "+")
((triple2) -> (rule5 % int1))
The cow is red.
("cow" "is" "red" "+")
int1
The rabbit is red.
("rabbit" "is" "red" "+")
((triple5) -> (rule5 % int1))
The rabbit is red.
("rabbit" "is" "red" "+")
int1
The cow sees the tiger.
("cow" "sees" "tiger" "+")
((((triple2) -> (rule5 % int2))) -> (rule7 % int1))
The cow sees the tiger.
("cow" "sees" "tiger" "+")
int1
The cow is red.
("cow" "is" "red" "+")
int2
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
((((triple5) -> (rule5 % int2))) -> (rule7 % int1))
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
int1
The rabbit is red.
("rabbit" "is" "red" "+")
int2
The rabbit likes the tiger.
("rabbit" "likes" "tiger" "+")
((((((triple5) -> (rule5 % int3))) -> (rule7 % int2)) triple8) -> (rule3 % int1))
The rabbit likes the tiger.
("rabbit" "likes" "tiger" "+")
int1
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
int2
The rabbit is red.
("rabbit" "is" "red" "+")
int3