The bear visits the lion. The cat eats the bear. The lion visits the bear. If someone visits the bear then the bear is nice. If someone visits the cat then they chase the cat. If the lion eats the cat then the lion does not eat the bear. If someone visits the bear then they are red. If the cat visits the lion then the lion is cold. If someone visits the cat and they chase the cat then they are big. If someone visits the bear then the bear visits the cat. If someone is nice and they do not chase the bear then they visit the bear.
The bear visits the lion.
("bear" "visits" "lion" "+")
The cat eats the bear.
("cat" "eats" "bear" "+")
The lion visits the bear.
("lion" "visits" "bear" "+")
If someone visits the bear then the bear is nice.
((("someone" "visits" "bear" "+")) -> ("bear" "is" "nice" "+"))
If someone visits the cat then they chase the cat.
((("someone" "visits" "cat" "+")) -> ("someone" "chases" "cat" "+"))
If the lion eats the cat then the lion does not eat the bear.
((("lion" "eats" "cat" "+")) -> ("lion" "eats" "bear" "-"))
If someone visits the bear then they are red.
((("someone" "visits" "bear" "+")) -> ("someone" "is" "red" "+"))
If the cat visits the lion then the lion is cold.
((("cat" "visits" "lion" "+")) -> ("lion" "is" "cold" "+"))
If someone visits the cat and they chase the cat then they are big.
((("someone" "visits" "cat" "+") ("someone" "chases" "cat" "+")) -> ("someone" "is" "big" "+"))
If someone visits the bear then the bear visits the cat.
((("someone" "visits" "bear" "+")) -> ("bear" "visits" "cat" "+"))
If someone is nice and they do not chase the bear then they visit the bear.
((("someone" "is" "nice" "+") ("someone" "chases" "bear" "~")) -> ("someone" "visits" "bear" "+"))
The cat eats the bear.
True
1
proof
[(triple2)]
("cat" "eats" "bear" "+")
triple2
The lion does not visit the bear.
False
1
inv-proof
[(triple3)]
("lion" "visits" "bear" "-")
triple3
The lion is red.
True
2
proof
[(((triple3) -> rule4))]
("lion" "is" "red" "+")
((triple3) -> (rule4 % int1))
The lion is red.
("lion" "is" "red" "+")
int1
The bear is not nice.
False
2
inv-proof
[(((triple3) -> rule1))]
("bear" "is" "nice" "-")
((triple3) -> (rule1 % int1))
The bear is nice.
("bear" "is" "nice" "+")
int1
The bear chases the cat.
True
3
proof
[(((((triple3) -> rule7)) -> rule2))]
("bear" "chases" "cat" "+")
((((triple3) -> (rule7 % int2))) -> (rule2 % int1))
The bear chases the cat.
("bear" "chases" "cat" "+")
int1
The bear visits the cat.
("bear" "visits" "cat" "+")
int2
The bear does not chase the cat.
False
3
inv-proof
[(((((triple3) -> rule7)) -> rule2))]
("bear" "chases" "cat" "-")
((((triple3) -> (rule7 % int2))) -> (rule2 % int1))
The bear chases the cat.
("bear" "chases" "cat" "+")
int1
The bear visits the cat.
("bear" "visits" "cat" "+")
int2
The bear is big.
True
6
proof
[(((((triple3) -> rule7) ((((triple3) -> rule7)) -> rule2)) -> rule6))]
("bear" "is" "big" "+")
((((triple3) -> (rule7 % int3)) ((((triple3) -> (rule7 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
The bear is big.
("bear" "is" "big" "+")
int1
The bear chases the cat.
("bear" "chases" "cat" "+")
int2
The bear visits the cat.
("bear" "visits" "cat" "+")
int3
The bear is not big.
False
6
inv-proof
[(((((triple3) -> rule7) ((((triple3) -> rule7)) -> rule2)) -> rule6))]
("bear" "is" "big" "-")
((((triple3) -> (rule7 % int3)) ((((triple3) -> (rule7 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
The bear is big.
("bear" "is" "big" "+")
int1
The bear chases the cat.
("bear" "chases" "cat" "+")
int2
The bear visits the cat.
("bear" "visits" "cat" "+")
int3
The bear is not red.
Unknown
inv-rconc
[@2: The bear is red.[CWA. Example of deepest failure = (rule4 <- rule8 <- FAIL)]]
("bear" "is" "red" "-")
The lion is cold.
Unknown
rconc
[@1: The lion is cold.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("lion" "is" "cold" "+")
The cat does not chase the cat.
Unknown
inv-rconc
[@1: The cat chases the cat.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cat" "chases" "cat" "-")
The cat is red.
Unknown
rconc
[@2: The cat is red.[CWA. Example of deepest failure = (rule4 <- rule8 <- FAIL)]]
("cat" "is" "red" "+")
The lion does not chase the bear.
Unknown
inv-random
[@0: The lion chases the bear.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "bear" "-")
The cat visits the lion.
Unknown
random
[@0: The cat visits the lion.[CWA. Example of deepest failure = (FAIL)]]
("cat" "visits" "lion" "+")
The lion is not kind.
Unknown
inv-random
[@0: The lion is kind.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "kind" "-")
The cat is nice.
Unknown
random
[@0: The cat is nice.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "nice" "+")
@0: The bear visits the lion.[(triple1)] The cat eats the bear.[(triple2)] The lion visits the bear.[(triple3)] @1: The bear is nice.[(((triple3) -> rule1))] The bear visits the cat.[(((triple3) -> rule7))] The lion is red.[(((triple3) -> rule4))] @2: The bear chases the cat.[(((((triple3) -> rule7)) -> rule2))] @3: The bear is big.[(((((triple3) -> rule7) ((((triple3) -> rule7)) -> rule2)) -> rule6))]
The bear visits the lion.
("bear" "visits" "lion" "+")
triple1
The cat eats the bear.
("cat" "eats" "bear" "+")
triple2
The lion visits the bear.
("lion" "visits" "bear" "+")
triple3
The bear is nice.
("bear" "is" "nice" "+")
((triple3) -> (rule1 % int1))
The bear is nice.
("bear" "is" "nice" "+")
int1
The bear visits the cat.
("bear" "visits" "cat" "+")
((triple3) -> (rule7 % int1))
The bear visits the cat.
("bear" "visits" "cat" "+")
int1
The lion is red.
("lion" "is" "red" "+")
((triple3) -> (rule4 % int1))
The lion is red.
("lion" "is" "red" "+")
int1
The bear chases the cat.
("bear" "chases" "cat" "+")
((((triple3) -> (rule7 % int2))) -> (rule2 % int1))
The bear chases the cat.
("bear" "chases" "cat" "+")
int1
The bear visits the cat.
("bear" "visits" "cat" "+")
int2
The bear is big.
("bear" "is" "big" "+")
((((triple3) -> (rule7 % int3)) ((((triple3) -> (rule7 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
The bear is big.
("bear" "is" "big" "+")
int1
The bear chases the cat.
("bear" "chases" "cat" "+")
int2
The bear visits the cat.
("bear" "visits" "cat" "+")
int3