The bear is cold. The bear is red. The bear visits the cat. The cat does not chase the bear. The cat does not chase the cow. The cat is blue. The cat is not green. The cat is not red. The cat sees the cow. The cat visits the bear. The cow chases the bear. The cow chases the cat. The cow is blue. The cow does not see the bear. The cow visits the bear. The cow visits the cat. If the bear visits the cow and the cow is cold then the cow is blue. If something visits the bear and the bear visits the cat then the bear does not see the cow. If something sees the cow and the cow is cold then it sees the cat. If the cow is blue and the cat does not chase the cow then the cow is cold. If the bear does not see the cow then the cow chases the cat. If something sees the cat and it does not see the cow then it chases the bear.
The bear is cold.
("bear" "is" "cold" "+")
The bear is red.
("bear" "is" "red" "+")
The bear visits the cat.
("bear" "visits" "cat" "+")
The cat does not chase the bear.
("cat" "chases" "bear" "-")
The cat does not chase the cow.
("cat" "chases" "cow" "-")
The cat is blue.
("cat" "is" "blue" "+")
The cat is not green.
("cat" "is" "green" "-")
The cat is not red.
("cat" "is" "red" "-")
The cat sees the cow.
("cat" "sees" "cow" "+")
The cat visits the bear.
("cat" "visits" "bear" "+")
The cow chases the bear.
("cow" "chases" "bear" "+")
The cow chases the cat.
("cow" "chases" "cat" "+")
The cow is blue.
("cow" "is" "blue" "+")
The cow does not see the bear.
("cow" "sees" "bear" "-")
The cow visits the bear.
("cow" "visits" "bear" "+")
The cow visits the cat.
("cow" "visits" "cat" "+")
If the bear visits the cow and the cow is cold then the cow is blue.
((("bear" "visits" "cow" "+") ("cow" "is" "cold" "+")) -> ("cow" "is" "blue" "+"))
If something visits the bear and the bear visits the cat then the bear does not see the cow.
((("something" "visits" "bear" "+") ("bear" "visits" "cat" "+")) -> ("bear" "sees" "cow" "-"))
If something sees the cow and the cow is cold then it sees the cat.
((("something" "sees" "cow" "+") ("cow" "is" "cold" "+")) -> ("something" "sees" "cat" "+"))
If the cow is blue and the cat does not chase the cow then the cow is cold.
((("cow" "is" "blue" "+") ("cat" "chases" "cow" "~")) -> ("cow" "is" "cold" "+"))
If the bear does not see the cow then the cow chases the cat.
((("bear" "sees" "cow" "~")) -> ("cow" "chases" "cat" "+"))
If something sees the cat and it does not see the cow then it chases the bear.
((("something" "sees" "cat" "+") ("something" "sees" "cow" "~")) -> ("something" "chases" "bear" "+"))
The bear is cold.
True
1
proof
[(triple1)]
("bear" "is" "cold" "+")
triple1
The cat does not visit the bear.
False
1
inv-proof
[(triple10)]
("cat" "visits" "bear" "-")
triple10
The cow is cold.
True
3
proof
[(((triple13 triple5) -> rule4))]
("cow" "is" "cold" "+")
((triple13 triple5) -> (rule4 % int1))
The cow is cold.
("cow" "is" "cold" "+")
int1
The cow is not cold.
False
3
inv-proof
[(((triple13 triple5) -> rule4))]
("cow" "is" "cold" "-")
((triple13 triple5) -> (rule4 % int1))
The cow is cold.
("cow" "is" "cold" "+")
int1
The cat sees the cat.
True
5
proof
[(((triple9 ((triple13 triple5) -> rule4)) -> rule3))]
("cat" "sees" "cat" "+")
((triple9 ((triple13 triple5) -> (rule4 % int2))) -> (rule3 % int1))
The cat sees the cat.
("cat" "sees" "cat" "+")
int1
The cow is cold.
("cow" "is" "cold" "+")
int2
The cat does not see the cat.
False
5
inv-proof
[(((triple9 ((triple13 triple5) -> rule4)) -> rule3))]
("cat" "sees" "cat" "-")
((triple9 ((triple13 triple5) -> (rule4 % int2))) -> (rule3 % int1))
The cat sees the cat.
("cat" "sees" "cat" "+")
int1
The cow is cold.
("cow" "is" "cold" "+")
int2
The bear does not see the cat.
Unknown
inv-rconc
[@1: The bear sees the cat.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("bear" "sees" "cat" "-")
The cow sees the cat.
Unknown
rconc
[@1: The cow sees the cat.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cow" "sees" "cat" "+")
The bear does not chase the bear.
Unknown
inv-rconc
[@1: The bear chases the bear.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("bear" "chases" "bear" "-")
The cat is cold.
Unknown
random
[@0: The cat is cold.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "cold" "+")
The cow does not visit the cow.
Unknown
inv-random
[@0: The cow visits the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "visits" "cow" "-")
The cat is big.
Unknown
random
[@0: The cat is big.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "big" "+")
@0: The bear is cold.[(triple1)] The bear is red.[(triple2)] The bear visits the cat.[(triple3)] The cat does not chase the bear.[(triple4)] The cat does not chase the cow.[(triple5)] The cat is blue.[(triple6)] The cat is not green.[(triple7)] The cat is not red.[(triple8)] The cat sees the cow.[(triple9)] The cat visits the bear.[(triple10)] The cow chases the bear.[(triple11)] The cow chases the cat.[(triple12 OR ((((triple10 triple3) -> rule2)) -> rule5) OR ((((triple15 triple3) -> rule2)) -> rule5))] The cow does not see the bear.[(triple14)] The cow is blue.[(triple13)] The cow visits the bear.[(triple15)] The cow visits the cat.[(triple16)] @1: The bear does not see the cow.[(((triple10 triple3) -> rule2) OR ((triple15 triple3) -> rule2))] The cow is cold.[(((triple13 triple5) -> rule4))] @2: The cat sees the cat.[(((triple9 ((triple13 triple5) -> rule4)) -> rule3))]
The bear is cold.
("bear" "is" "cold" "+")
triple1
The bear is red.
("bear" "is" "red" "+")
triple2
The bear visits the cat.
("bear" "visits" "cat" "+")
triple3
The cat does not chase the bear.
("cat" "chases" "bear" "-")
triple4
The cat does not chase the cow.
("cat" "chases" "cow" "-")
triple5
The cat is blue.
("cat" "is" "blue" "+")
triple6
The cat is not green.
("cat" "is" "green" "-")
triple7
The cat is not red.
("cat" "is" "red" "-")
triple8
The cat sees the cow.
("cat" "sees" "cow" "+")
triple9
The cat visits the bear.
("cat" "visits" "bear" "+")
triple10
The cow chases the bear.
("cow" "chases" "bear" "+")
triple11
The cow chases the cat.
("cow" "chases" "cat" "+")
triple12
((((triple10 triple3) -> (rule2 % int2))) -> (rule5 % int1))
The cow chases the cat.
("cow" "chases" "cat" "+")
int1
The bear does not see the cow.
("bear" "sees" "cow" "-")
int2
((((triple15 triple3) -> (rule2 % int2))) -> (rule5 % int1))
The cow chases the cat.
("cow" "chases" "cat" "+")
int1
The bear does not see the cow.
("bear" "sees" "cow" "-")
int2
The cow does not see the bear.
("cow" "sees" "bear" "-")
triple14
The cow is blue.
("cow" "is" "blue" "+")
triple13
The cow visits the bear.
("cow" "visits" "bear" "+")
triple15
The cow visits the cat.
("cow" "visits" "cat" "+")
triple16
The bear does not see the cow.
("bear" "sees" "cow" "-")
((triple10 triple3) -> (rule2 % int1))
The bear does not see the cow.
("bear" "sees" "cow" "-")
int1
((triple15 triple3) -> (rule2 % int1))
The bear does not see the cow.
("bear" "sees" "cow" "-")
int1
The cow is cold.
("cow" "is" "cold" "+")
((triple13 triple5) -> (rule4 % int1))
The cow is cold.
("cow" "is" "cold" "+")
int1
The cat sees the cat.
("cat" "sees" "cat" "+")
((triple9 ((triple13 triple5) -> (rule4 % int2))) -> (rule3 % int1))
The cat sees the cat.
("cat" "sees" "cat" "+")
int1
The cow is cold.
("cow" "is" "cold" "+")
int2