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