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