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