The bear is nice. The cat needs the cow. The cow visits the cat. If someone visits the cat and they are round then they visit the bear. If someone likes the cat and the cat visits the bear then they are big. If someone is nice then they need the cat. If someone is nice then they are round. If someone is round then they are cold. If someone is cold and nice then they need the cow. If someone likes the cat then the cat needs the bear. If someone likes the bear and the bear visits the cat then the bear needs the cow.
The bear is nice.
("bear" "is" "nice" "+")
The cat needs the cow.
("cat" "needs" "cow" "+")
The cow visits the cat.
("cow" "visits" "cat" "+")
If someone visits the cat and they are round then they visit the bear.
((("someone" "visits" "cat" "+") ("someone" "is" "round" "+")) -> ("someone" "visits" "bear" "+"))
If someone likes the cat and the cat visits the bear then they are big.
((("someone" "likes" "cat" "+") ("cat" "visits" "bear" "+")) -> ("someone" "is" "big" "+"))
If someone is nice then they need the cat.
((("someone" "is" "nice" "+")) -> ("someone" "needs" "cat" "+"))
If someone is nice then they are round.
((("someone" "is" "nice" "+")) -> ("someone" "is" "round" "+"))
If someone is round then they are cold.
((("someone" "is" "round" "+")) -> ("someone" "is" "cold" "+"))
If someone is cold and nice then they need the cow.
((("someone" "is" "cold" "+") ("someone" "is" "nice" "+")) -> ("someone" "needs" "cow" "+"))
If someone likes the cat then the cat needs the bear.
((("someone" "likes" "cat" "+")) -> ("cat" "needs" "bear" "+"))
If someone likes the bear and the bear visits the cat then the bear needs the cow.
((("someone" "likes" "bear" "+") ("bear" "visits" "cat" "+")) -> ("bear" "needs" "cow" "+"))
The cow visits the cat.
True
1
proof
[(triple3)]
("cow" "visits" "cat" "+")
triple3
The cow does not visit the cat.
False
1
inv-proof
[(triple3)]
("cow" "visits" "cat" "-")
triple3
The bear is round.
True
2
proof
[(((triple1) -> rule4))]
("bear" "is" "round" "+")
((triple1) -> (rule4 % int1))
The bear is round.
("bear" "is" "round" "+")
int1
The bear is not round.
False
2
inv-proof
[(((triple1) -> rule4))]
("bear" "is" "round" "-")
((triple1) -> (rule4 % int1))
The bear is round.
("bear" "is" "round" "+")
int1
The bear is cold.
True
3
proof
[(((((triple1) -> rule4)) -> rule5))]
("bear" "is" "cold" "+")
((((triple1) -> (rule4 % int2))) -> (rule5 % int1))
The bear is cold.
("bear" "is" "cold" "+")
int1
The bear is round.
("bear" "is" "round" "+")
int2
The bear is not cold.
False
3
inv-proof
[(((((triple1) -> rule4)) -> rule5))]
("bear" "is" "cold" "-")
((((triple1) -> (rule4 % int2))) -> (rule5 % int1))
The bear is cold.
("bear" "is" "cold" "+")
int1
The bear is round.
("bear" "is" "round" "+")
int2
The bear needs the cow.
True
5
proof
[(((((((triple1) -> rule4)) -> rule5) triple1) -> rule6))]
("bear" "needs" "cow" "+")
((((((triple1) -> (rule4 % int3))) -> (rule5 % int2)) triple1) -> (rule6 % int1))
The bear needs the cow.
("bear" "needs" "cow" "+")
int1
The bear is cold.
("bear" "is" "cold" "+")
int2
The bear is round.
("bear" "is" "round" "+")
int3
The bear does not need the cow.
False
5
inv-proof
[(((((((triple1) -> rule4)) -> rule5) triple1) -> rule6))]
("bear" "needs" "cow" "-")
((((((triple1) -> (rule4 % int3))) -> (rule5 % int2)) triple1) -> (rule6 % int1))
The bear needs the cow.
("bear" "needs" "cow" "+")
int1
The bear is cold.
("bear" "is" "cold" "+")
int2
The bear is round.
("bear" "is" "round" "+")
int3
The cat is not big.
Unknown
inv-rconc
[@1: The cat is big.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cat" "is" "big" "-")
The bear is big.
Unknown
rconc
[@1: The bear is big.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("bear" "is" "big" "+")
The cat is not round.
Unknown
inv-rconc
[@1: The cat is round.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cat" "is" "round" "-")
The cow is round.
Unknown
rconc
[@1: The cow is round.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cow" "is" "round" "+")
The bear does not like the bear.
Unknown
inv-random
[@0: The bear likes the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "likes" "bear" "-")
The cow is nice.
Unknown
random
[@0: The cow is nice.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "nice" "+")
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 cow visits the cow.
Unknown
random
[@0: The cow visits the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "visits" "cow" "+")
@0: The bear is nice.[(triple1)] The cat needs the cow.[(triple2)] The cow visits the cat.[(triple3)] @1: The bear is round.[(((triple1) -> rule4))] The bear needs the cat.[(((triple1) -> rule3))] @2: The bear is cold.[(((((triple1) -> rule4)) -> rule5))] @3: The bear needs the cow.[(((((((triple1) -> rule4)) -> rule5) triple1) -> rule6))]
The bear is nice.
("bear" "is" "nice" "+")
triple1
The cat needs the cow.
("cat" "needs" "cow" "+")
triple2
The cow visits the cat.
("cow" "visits" "cat" "+")
triple3
The bear is round.
("bear" "is" "round" "+")
((triple1) -> (rule4 % int1))
The bear is round.
("bear" "is" "round" "+")
int1
The bear needs the cat.
("bear" "needs" "cat" "+")
((triple1) -> (rule3 % int1))
The bear needs the cat.
("bear" "needs" "cat" "+")
int1
The bear is cold.
("bear" "is" "cold" "+")
((((triple1) -> (rule4 % int2))) -> (rule5 % int1))
The bear is cold.
("bear" "is" "cold" "+")
int1
The bear is round.
("bear" "is" "round" "+")
int2
The bear needs the cow.
("bear" "needs" "cow" "+")
((((((triple1) -> (rule4 % int3))) -> (rule5 % int2)) triple1) -> (rule6 % int1))
The bear needs the cow.
("bear" "needs" "cow" "+")
int1
The bear is cold.
("bear" "is" "cold" "+")
int2
The bear is round.
("bear" "is" "round" "+")
int3