The bear likes the tiger. The cat chases the tiger. The cat is young. The cow is big. The cow likes the bear. The cow likes the cat. The cow sees the cat. The tiger likes the cat. The tiger sees the bear. The tiger sees the cow. If someone sees the tiger then the tiger is round. If someone likes the tiger and they like the bear then the tiger chases the cow. If someone is young then they are rough. If someone chases the cow then the cow is rough. If the cat is nice and the cat likes the cow then the cat likes the bear. If someone is big then they like the tiger. If someone likes the tiger then they see the cow. If someone is round and not rough then they do not like the cat.
The bear likes the tiger.
("bear" "likes" "tiger" "+")
The cat chases the tiger.
("cat" "chases" "tiger" "+")
The cat is young.
("cat" "is" "young" "+")
The cow is big.
("cow" "is" "big" "+")
The cow likes the bear.
("cow" "likes" "bear" "+")
The cow likes the cat.
("cow" "likes" "cat" "+")
The cow sees the cat.
("cow" "sees" "cat" "+")
The tiger likes the cat.
("tiger" "likes" "cat" "+")
The tiger sees the bear.
("tiger" "sees" "bear" "+")
The tiger sees the cow.
("tiger" "sees" "cow" "+")
If someone sees the tiger then the tiger is round.
((("someone" "sees" "tiger" "+")) -> ("tiger" "is" "round" "+"))
If someone likes the tiger and they like the bear then the tiger chases the cow.
((("someone" "likes" "tiger" "+") ("someone" "likes" "bear" "+")) -> ("tiger" "chases" "cow" "+"))
If someone is young then they are rough.
((("someone" "is" "young" "+")) -> ("someone" "is" "rough" "+"))
If someone chases the cow then the cow is rough.
((("someone" "chases" "cow" "+")) -> ("cow" "is" "rough" "+"))
If the cat is nice and the cat likes the cow then the cat likes the bear.
((("cat" "is" "nice" "+") ("cat" "likes" "cow" "+")) -> ("cat" "likes" "bear" "+"))
If someone is big then they like the tiger.
((("someone" "is" "big" "+")) -> ("someone" "likes" "tiger" "+"))
If someone likes the tiger then they see the cow.
((("someone" "likes" "tiger" "+")) -> ("someone" "sees" "cow" "+"))
If someone is round and not rough then they do not like the cat.
((("someone" "is" "round" "+") ("someone" "is" "rough" "~")) -> ("someone" "likes" "cat" "-"))
The cat chases the tiger.
True
1
proof
[(triple2)]
("cat" "chases" "tiger" "+")
triple2
The cat is not young.
False
1
inv-proof
[(triple3)]
("cat" "is" "young" "-")
triple3
The cow likes the tiger.
True
2
proof
[(((triple4) -> rule6))]
("cow" "likes" "tiger" "+")
((triple4) -> (rule6 % int1))
The cow likes the tiger.
("cow" "likes" "tiger" "+")
int1
The cat is not rough.
False
2
inv-proof
[(((triple3) -> rule3))]
("cat" "is" "rough" "-")
((triple3) -> (rule3 % int1))
The cat is rough.
("cat" "is" "rough" "+")
int1
The cow sees the cow.
True
3
proof
[(((((triple4) -> rule6)) -> rule7))]
("cow" "sees" "cow" "+")
((((triple4) -> (rule6 % int2))) -> (rule7 % int1))
The cow sees the cow.
("cow" "sees" "cow" "+")
int1
The cow likes the tiger.
("cow" "likes" "tiger" "+")
int2
The tiger does not chase the cow.
False
4
inv-proof
[(((((triple4) -> rule6) triple5) -> rule2))]
("tiger" "chases" "cow" "-")
((((triple4) -> (rule6 % int2)) triple5) -> (rule2 % int1))
The tiger chases the cow.
("tiger" "chases" "cow" "+")
int1
The cow likes the tiger.
("cow" "likes" "tiger" "+")
int2
The cow is rough.
True
5
proof
[(((((((triple4) -> rule6) triple5) -> rule2)) -> rule4))]
("cow" "is" "rough" "+")
((((((triple4) -> (rule6 % int3)) triple5) -> (rule2 % int2))) -> (rule4 % int1))
The cow is rough.
("cow" "is" "rough" "+")
int1
The tiger chases the cow.
("tiger" "chases" "cow" "+")
int2
The cow likes the tiger.
("cow" "likes" "tiger" "+")
int3
The cow is not rough.
False
5
inv-proof
[(((((((triple4) -> rule6) triple5) -> rule2)) -> rule4))]
("cow" "is" "rough" "-")
((((((triple4) -> (rule6 % int3)) triple5) -> (rule2 % int2))) -> (rule4 % int1))
The cow is rough.
("cow" "is" "rough" "+")
int1
The tiger chases the cow.
("tiger" "chases" "cow" "+")
int2
The cow likes the tiger.
("cow" "likes" "tiger" "+")
int3
The tiger does not like the tiger.
Unknown
inv-rconc
[@1: The tiger likes the tiger.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("tiger" "likes" "tiger" "-")
The tiger is rough.
Unknown
rconc
[@1: The tiger is rough.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("tiger" "is" "rough" "+")
The cat does not see the cow.
Unknown
inv-rconc
[@2: The cat sees the cow.[CWA. Example of deepest failure = (rule7 <- rule6 <- FAIL)]]
("cat" "sees" "cow" "-")
The bear is rough.
Unknown
rconc
[@1: The bear is rough.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("bear" "is" "rough" "+")
The tiger does not like the bear.
Unknown
inv-random
[@0: The tiger likes the bear.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "likes" "bear" "-")
The tiger is big.
Unknown
random
[@0: The tiger is big.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "big" "+")
The bear does not like the bear.
Unknown
inv-random
[@0: The bear likes the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "likes" "bear" "-")
The tiger sees the cat.
Unknown
random
[@0: The tiger sees the cat.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "cat" "+")
@0: The bear likes the tiger.[(triple1)] The cat chases the tiger.[(triple2)] The cat is young.[(triple3)] The cow is big.[(triple4)] The cow likes the bear.[(triple5)] The cow likes the cat.[(triple6)] The cow sees the cat.[(triple7)] The tiger likes the cat.[(triple8)] The tiger sees the bear.[(triple9)] The tiger sees the cow.[(triple10)] @1: The bear sees the cow.[(((triple1) -> rule7))] The cat is rough.[(((triple3) -> rule3))] The cow likes the tiger.[(((triple4) -> rule6))] @2: The cow sees the cow.[(((((triple4) -> rule6)) -> rule7))] The tiger chases the cow.[(((((triple4) -> rule6) triple5) -> rule2))] @3: The cow is rough.[(((((((triple4) -> rule6) triple5) -> rule2)) -> rule4))]
The bear likes the tiger.
("bear" "likes" "tiger" "+")
triple1
The cat chases the tiger.
("cat" "chases" "tiger" "+")
triple2
The cat is young.
("cat" "is" "young" "+")
triple3
The cow is big.
("cow" "is" "big" "+")
triple4
The cow likes the bear.
("cow" "likes" "bear" "+")
triple5
The cow likes the cat.
("cow" "likes" "cat" "+")
triple6
The cow sees the cat.
("cow" "sees" "cat" "+")
triple7
The tiger likes the cat.
("tiger" "likes" "cat" "+")
triple8
The tiger sees the bear.
("tiger" "sees" "bear" "+")
triple9
The tiger sees the cow.
("tiger" "sees" "cow" "+")
triple10
The bear sees the cow.
("bear" "sees" "cow" "+")
((triple1) -> (rule7 % int1))
The bear sees the cow.
("bear" "sees" "cow" "+")
int1
The cat is rough.
("cat" "is" "rough" "+")
((triple3) -> (rule3 % int1))
The cat is rough.
("cat" "is" "rough" "+")
int1
The cow likes the tiger.
("cow" "likes" "tiger" "+")
((triple4) -> (rule6 % int1))
The cow likes the tiger.
("cow" "likes" "tiger" "+")
int1
The cow sees the cow.
("cow" "sees" "cow" "+")
((((triple4) -> (rule6 % int2))) -> (rule7 % int1))
The cow sees the cow.
("cow" "sees" "cow" "+")
int1
The cow likes the tiger.
("cow" "likes" "tiger" "+")
int2
The tiger chases the cow.
("tiger" "chases" "cow" "+")
((((triple4) -> (rule6 % int2)) triple5) -> (rule2 % int1))
The tiger chases the cow.
("tiger" "chases" "cow" "+")
int1
The cow likes the tiger.
("cow" "likes" "tiger" "+")
int2
The cow is rough.
("cow" "is" "rough" "+")
((((((triple4) -> (rule6 % int3)) triple5) -> (rule2 % int2))) -> (rule4 % int1))
The cow is rough.
("cow" "is" "rough" "+")
int1
The tiger chases the cow.
("tiger" "chases" "cow" "+")
int2
The cow likes the tiger.
("cow" "likes" "tiger" "+")
int3