The bear is young. The cat is cold. If someone is red then they see the bear. If someone is cold then they see the bear. If someone is red then they do not see the bear. If someone sees the bear then they eat the cat. If someone sees the cat then they eat the cat. If the bear is kind then the bear sees the cat. If someone eats the cat then they visit the bear. If someone visits the bear then they see the cat.
The bear is young.
("bear" "is" "young" "+")
The cat is cold.
("cat" "is" "cold" "+")
If someone is red then they see the bear.
((("someone" "is" "red" "+")) -> ("someone" "sees" "bear" "+"))
If someone is cold then they see the bear.
((("someone" "is" "cold" "+")) -> ("someone" "sees" "bear" "+"))
If someone is red then they do not see the bear.
((("someone" "is" "red" "+")) -> ("someone" "sees" "bear" "-"))
If someone sees the bear then they eat the cat.
((("someone" "sees" "bear" "+")) -> ("someone" "eats" "cat" "+"))
If someone sees the cat then they eat the cat.
((("someone" "sees" "cat" "+")) -> ("someone" "eats" "cat" "+"))
If the bear is kind then the bear sees the cat.
((("bear" "is" "kind" "+")) -> ("bear" "sees" "cat" "+"))
If someone eats the cat then they visit the bear.
((("someone" "eats" "cat" "+")) -> ("someone" "visits" "bear" "+"))
If someone visits the bear then they see the cat.
((("someone" "visits" "bear" "+")) -> ("someone" "sees" "cat" "+"))
The cat is cold.
True
1
proof
[(triple2)]
("cat" "is" "cold" "+")
triple2
The cat is not cold.
False
1
inv-proof
[(triple2)]
("cat" "is" "cold" "-")
triple2
The cat sees the bear.
True
2
proof
[(((triple2) -> rule2))]
("cat" "sees" "bear" "+")
((triple2) -> (rule2 % int1))
The cat sees the bear.
("cat" "sees" "bear" "+")
int1
The cat does not see the bear.
False
2
inv-proof
[(((triple2) -> rule2))]
("cat" "sees" "bear" "-")
((triple2) -> (rule2 % int1))
The cat sees the bear.
("cat" "sees" "bear" "+")
int1
The cat eats the cat.
True
3
proof
[(((((triple2) -> rule2)) -> rule4))]
("cat" "eats" "cat" "+")
((((triple2) -> (rule2 % int2))) -> (rule4 % int1))
The cat eats the cat.
("cat" "eats" "cat" "+")
int1
The cat sees the bear.
("cat" "sees" "bear" "+")
int2
The cat does not eat the cat.
False
3
inv-proof
[(((((triple2) -> rule2)) -> rule4))]
("cat" "eats" "cat" "-")
((((triple2) -> (rule2 % int2))) -> (rule4 % int1))
The cat eats the cat.
("cat" "eats" "cat" "+")
int1
The cat sees the bear.
("cat" "sees" "bear" "+")
int2
The cat visits the bear.
True
4
proof
[(((((((triple2) -> rule2)) -> rule4)) -> rule7))]
("cat" "visits" "bear" "+")
((((((triple2) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
The cat visits the bear.
("cat" "visits" "bear" "+")
int1
The cat eats the cat.
("cat" "eats" "cat" "+")
int2
The cat sees the bear.
("cat" "sees" "bear" "+")
int3
The cat does not visit the bear.
False
4
inv-proof
[(((((((triple2) -> rule2)) -> rule4)) -> rule7))]
("cat" "visits" "bear" "-")
((((((triple2) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
The cat visits the bear.
("cat" "visits" "bear" "+")
int1
The cat eats the cat.
("cat" "eats" "cat" "+")
int2
The cat sees the bear.
("cat" "sees" "bear" "+")
int3
The bear does not see the bear.
Unknown
inv-rconc
[@1: The bear sees the bear.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("bear" "sees" "bear" "-")
The bear visits the bear.
Unknown
rconc
[@3: The bear visits the bear.[CWA. Example of deepest failure = (rule7 <- rule4 <- rule1 <- FAIL)]]
("bear" "visits" "bear" "+")
The bear does not see the cat.
Unknown
inv-rconc
[@4: The bear sees the cat.[CWA. Example of deepest failure = (rule8 <- rule7 <- rule4 <- rule1 <- FAIL)]]
("bear" "sees" "cat" "-")
The bear eats the cat.
Unknown
rconc
[@5: The bear eats the cat.[CWA. Example of deepest failure = (rule5 <- rule8 <- rule7 <- rule4 <- rule1 <- FAIL)]]
("bear" "eats" "cat" "+")
The bear is not cold.
Unknown
inv-random
[@0: The bear is cold.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "cold" "-")
The bear is kind.
Unknown
random
[@0: The bear is kind.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "kind" "+")
The cat is not big.
Unknown
inv-random
[@0: The cat is big.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "big" "-")
The cat is kind.
Unknown
random
[@0: The cat is kind.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "kind" "+")
@0: The bear is young.[(triple1)] The cat is cold.[(triple2)] @1: The cat sees the bear.[(((triple2) -> rule2))] @2: The cat eats the cat.[(((((triple2) -> rule2)) -> rule4))] @3: The cat visits the bear.[(((((((triple2) -> rule2)) -> rule4)) -> rule7))] @4: The cat sees the cat.[(((((((((triple2) -> rule2)) -> rule4)) -> rule7)) -> rule8))]
The bear is young.
("bear" "is" "young" "+")
triple1
The cat is cold.
("cat" "is" "cold" "+")
triple2
The cat sees the bear.
("cat" "sees" "bear" "+")
((triple2) -> (rule2 % int1))
The cat sees the bear.
("cat" "sees" "bear" "+")
int1
The cat eats the cat.
("cat" "eats" "cat" "+")
((((triple2) -> (rule2 % int2))) -> (rule4 % int1))
The cat eats the cat.
("cat" "eats" "cat" "+")
int1
The cat sees the bear.
("cat" "sees" "bear" "+")
int2
The cat visits the bear.
("cat" "visits" "bear" "+")
((((((triple2) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
The cat visits the bear.
("cat" "visits" "bear" "+")
int1
The cat eats the cat.
("cat" "eats" "cat" "+")
int2
The cat sees the bear.
("cat" "sees" "bear" "+")
int3
The cat sees the cat.
("cat" "sees" "cat" "+")
((((((((triple2) -> (rule2 % int4))) -> (rule4 % int3))) -> (rule7 % int2))) -> (rule8 % int1))
The cat sees the cat.
("cat" "sees" "cat" "+")
int1
The cat visits the bear.
("cat" "visits" "bear" "+")
int2
The cat eats the cat.
("cat" "eats" "cat" "+")
int3
The cat sees the bear.
("cat" "sees" "bear" "+")
int4