The bear is blue. The bear is kind. The bear sees the cat. The cat chases the cow. The cat sees the tiger. The cow is cold. The cow sees the cat. The cow visits the bear. The cow visits the tiger. The tiger is cold. The tiger is kind. The tiger visits the cow. If someone chases the cow then they are big. If someone is red and they see the tiger then they see the bear. If someone is cold then they chase the cow. If someone is red and they visit the cow then they see the tiger. If someone is big and they see the cat then the cat is blue. If the cat chases the tiger then the cat chases the bear. If someone is red then they chase the tiger. If the cow sees the bear and the cow chases the tiger then the cow chases the bear.
The bear is blue.
("bear" "is" "blue" "+")
The bear is kind.
("bear" "is" "kind" "+")
The bear sees the cat.
("bear" "sees" "cat" "+")
The cat chases the cow.
("cat" "chases" "cow" "+")
The cat sees the tiger.
("cat" "sees" "tiger" "+")
The cow is cold.
("cow" "is" "cold" "+")
The cow sees the cat.
("cow" "sees" "cat" "+")
The cow visits the bear.
("cow" "visits" "bear" "+")
The cow visits the tiger.
("cow" "visits" "tiger" "+")
The tiger is cold.
("tiger" "is" "cold" "+")
The tiger is kind.
("tiger" "is" "kind" "+")
The tiger visits the cow.
("tiger" "visits" "cow" "+")
If someone chases the cow then they are big.
((("someone" "chases" "cow" "+")) -> ("someone" "is" "big" "+"))
If someone is red and they see the tiger then they see the bear.
((("someone" "is" "red" "+") ("someone" "sees" "tiger" "+")) -> ("someone" "sees" "bear" "+"))
If someone is cold then they chase the cow.
((("someone" "is" "cold" "+")) -> ("someone" "chases" "cow" "+"))
If someone is red and they visit the cow then they see the tiger.
((("someone" "is" "red" "+") ("someone" "visits" "cow" "+")) -> ("someone" "sees" "tiger" "+"))
If someone is big and they see the cat then the cat is blue.
((("someone" "is" "big" "+") ("someone" "sees" "cat" "+")) -> ("cat" "is" "blue" "+"))
If the cat chases the tiger then the cat chases the bear.
((("cat" "chases" "tiger" "+")) -> ("cat" "chases" "bear" "+"))
If someone is red then they chase the tiger.
((("someone" "is" "red" "+")) -> ("someone" "chases" "tiger" "+"))
If the cow sees the bear and the cow chases the tiger then the cow chases the bear.
((("cow" "sees" "bear" "+") ("cow" "chases" "tiger" "+")) -> ("cow" "chases" "bear" "+"))
The bear is blue.
True
1
proof
[(triple1)]
("bear" "is" "blue" "+")
triple1
The cow does not visit the tiger.
False
1
inv-proof
[(triple9)]
("cow" "visits" "tiger" "-")
triple9
The cow chases the cow.
True
2
proof
[(((triple6) -> rule3))]
("cow" "chases" "cow" "+")
((triple6) -> (rule3 % int1))
The cow chases the cow.
("cow" "chases" "cow" "+")
int1
The tiger does not chase the cow.
False
2
inv-proof
[(((triple10) -> rule3))]
("tiger" "chases" "cow" "-")
((triple10) -> (rule3 % int1))
The tiger chases the cow.
("tiger" "chases" "cow" "+")
int1
The tiger does not see the tiger.
Unknown
inv-rconc
[@1: The tiger sees the tiger.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("tiger" "sees" "tiger" "-")
The bear chases the cow.
Unknown
rconc
[@1: The bear chases the cow.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("bear" "chases" "cow" "+")
The tiger does not chase the bear.
Unknown
inv-random
[@0: The tiger chases the bear.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "chases" "bear" "-")
The cat visits the cat.
Unknown
random
[@0: The cat visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "visits" "cat" "+")
@0: The bear is blue.[(triple1)] The bear is kind.[(triple2)] The bear sees the cat.[(triple3)] The cat chases the cow.[(triple4)] The cat sees the tiger.[(triple5)] The cow is cold.[(triple6)] The cow sees the cat.[(triple7)] The cow visits the bear.[(triple8)] The cow visits the tiger.[(triple9)] The tiger is cold.[(triple10)] The tiger is kind.[(triple11)] The tiger visits the cow.[(triple12)] @1: The cat is big.[(((triple4) -> rule1))] The cow chases the cow.[(((triple6) -> rule3))] The tiger chases the cow.[(((triple10) -> rule3))] @2: The cow is big.[(((((triple6) -> rule3)) -> rule1))] The tiger is big.[(((((triple10) -> rule3)) -> rule1))] @3: The cat is blue.[(((((((triple6) -> rule3)) -> rule1) triple7) -> rule5))]
The bear is blue.
("bear" "is" "blue" "+")
triple1
The bear is kind.
("bear" "is" "kind" "+")
triple2
The bear sees the cat.
("bear" "sees" "cat" "+")
triple3
The cat chases the cow.
("cat" "chases" "cow" "+")
triple4
The cat sees the tiger.
("cat" "sees" "tiger" "+")
triple5
The cow is cold.
("cow" "is" "cold" "+")
triple6
The cow sees the cat.
("cow" "sees" "cat" "+")
triple7
The cow visits the bear.
("cow" "visits" "bear" "+")
triple8
The cow visits the tiger.
("cow" "visits" "tiger" "+")
triple9
The tiger is cold.
("tiger" "is" "cold" "+")
triple10
The tiger is kind.
("tiger" "is" "kind" "+")
triple11
The tiger visits the cow.
("tiger" "visits" "cow" "+")
triple12
The cat is big.
("cat" "is" "big" "+")
((triple4) -> (rule1 % int1))
The cat is big.
("cat" "is" "big" "+")
int1
The cow chases the cow.
("cow" "chases" "cow" "+")
((triple6) -> (rule3 % int1))
The cow chases the cow.
("cow" "chases" "cow" "+")
int1
The tiger chases the cow.
("tiger" "chases" "cow" "+")
((triple10) -> (rule3 % int1))
The tiger chases the cow.
("tiger" "chases" "cow" "+")
int1
The cow is big.
("cow" "is" "big" "+")
((((triple6) -> (rule3 % int2))) -> (rule1 % int1))
The cow is big.
("cow" "is" "big" "+")
int1
The cow chases the cow.
("cow" "chases" "cow" "+")
int2
The tiger is big.
("tiger" "is" "big" "+")
((((triple10) -> (rule3 % int2))) -> (rule1 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
The tiger chases the cow.
("tiger" "chases" "cow" "+")
int2
The cat is blue.
("cat" "is" "blue" "+")
((((((triple6) -> (rule3 % int3))) -> (rule1 % int2)) triple7) -> (rule5 % int1))
The cat is blue.
("cat" "is" "blue" "+")
int1
The cow is big.
("cow" "is" "big" "+")
int2
The cow chases the cow.
("cow" "chases" "cow" "+")
int3