The bear is cold. The bear is nice. The bear needs the rabbit. The bear sees the cat. The bear sees the rabbit. The bear visits the rabbit. The cat is kind. The cat is nice. The cat needs the rabbit. The cat sees the bear. The cat sees the rabbit. The cat visits the bear. The rabbit is cold. The rabbit is red. The rabbit visits the bear. If something sees the bear then the bear visits the rabbit. If something needs the bear and it visits the cat then the cat visits the rabbit. If something visits the cat and the cat needs the rabbit then it is kind. If something needs the rabbit and it sees the cat then it sees the bear. If something sees the cat and it needs the bear then it is red. If something sees the bear then it sees the cat. If something sees the bear then it needs the cat. If something sees the cat then the cat needs the rabbit.
The bear is cold.
("bear" "is" "cold" "+")
The bear is nice.
("bear" "is" "nice" "+")
The bear needs the rabbit.
("bear" "needs" "rabbit" "+")
The bear sees the cat.
("bear" "sees" "cat" "+")
The bear sees the rabbit.
("bear" "sees" "rabbit" "+")
The bear visits the rabbit.
("bear" "visits" "rabbit" "+")
The cat is kind.
("cat" "is" "kind" "+")
The cat is nice.
("cat" "is" "nice" "+")
The cat needs the rabbit.
("cat" "needs" "rabbit" "+")
The cat sees the bear.
("cat" "sees" "bear" "+")
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
The cat visits the bear.
("cat" "visits" "bear" "+")
The rabbit is cold.
("rabbit" "is" "cold" "+")
The rabbit is red.
("rabbit" "is" "red" "+")
The rabbit visits the bear.
("rabbit" "visits" "bear" "+")
If something sees the bear then the bear visits the rabbit.
((("something" "sees" "bear" "+")) -> ("bear" "visits" "rabbit" "+"))
If something needs the bear and it visits the cat then the cat visits the rabbit.
((("something" "needs" "bear" "+") ("something" "visits" "cat" "+")) -> ("cat" "visits" "rabbit" "+"))
If something visits the cat and the cat needs the rabbit then it is kind.
((("something" "visits" "cat" "+") ("cat" "needs" "rabbit" "+")) -> ("something" "is" "kind" "+"))
If something needs the rabbit and it sees the cat then it sees the bear.
((("something" "needs" "rabbit" "+") ("something" "sees" "cat" "+")) -> ("something" "sees" "bear" "+"))
If something sees the cat and it needs the bear then it is red.
((("something" "sees" "cat" "+") ("something" "needs" "bear" "+")) -> ("something" "is" "red" "+"))
If something sees the bear then it sees the cat.
((("something" "sees" "bear" "+")) -> ("something" "sees" "cat" "+"))
If something sees the bear then it needs the cat.
((("something" "sees" "bear" "+")) -> ("something" "needs" "cat" "+"))
If something sees the cat then the cat needs the rabbit.
((("something" "sees" "cat" "+")) -> ("cat" "needs" "rabbit" "+"))
The bear sees the rabbit.
True
1
proof
[(triple5)]
("bear" "sees" "rabbit" "+")
triple5
The bear does not need the rabbit.
False
1
inv-proof
[(triple3)]
("bear" "needs" "rabbit" "-")
triple3
The cat sees the cat.
True
2
proof
[(((triple10) -> rule6))]
("cat" "sees" "cat" "+")
((triple10) -> (rule6 % int1))
The cat sees the cat.
("cat" "sees" "cat" "+")
int1
The cat does not see the cat.
False
2
inv-proof
[(((triple10) -> rule6))]
("cat" "sees" "cat" "-")
((triple10) -> (rule6 % int1))
The cat sees the cat.
("cat" "sees" "cat" "+")
int1
The bear needs the cat.
True
4
proof
[(((((triple3 triple4) -> rule4)) -> rule7))]
("bear" "needs" "cat" "+")
((((triple3 triple4) -> (rule4 % int2))) -> (rule7 % int1))
The bear needs the cat.
("bear" "needs" "cat" "+")
int1
The bear sees the bear.
("bear" "sees" "bear" "+")
int2
The bear does not need the cat.
False
4
inv-proof
[(((((triple3 triple4) -> rule4)) -> rule7))]
("bear" "needs" "cat" "-")
((((triple3 triple4) -> (rule4 % int2))) -> (rule7 % int1))
The bear needs the cat.
("bear" "needs" "cat" "+")
int1
The bear sees the bear.
("bear" "sees" "bear" "+")
int2
The bear is not red.
Unknown
inv-rconc
[@1: The bear is red.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("bear" "is" "red" "-")
The cat is red.
Unknown
rconc
[@1: The cat is red.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("cat" "is" "red" "+")
The rabbit is not kind.
Unknown
inv-rconc
[@1: The rabbit is kind.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("rabbit" "is" "kind" "-")
The rabbit needs the bear.
Unknown
random
[@0: The rabbit needs the bear.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "needs" "bear" "+")
The rabbit is not nice.
Unknown
inv-random
[@0: The rabbit is nice.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "nice" "-")
The bear is blue.
Unknown
random
[@0: The bear is blue.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "blue" "+")
@0: The bear is cold.[(triple1)] The bear is nice.[(triple2)] The bear needs the rabbit.[(triple3)] The bear sees the cat.[(triple4)] The bear sees the rabbit.[(triple5)] The bear visits the rabbit.[(triple6 OR ((triple10) -> rule1) OR ((((triple3 triple4) -> rule4)) -> rule1))] The cat is kind.[(triple7)] The cat is nice.[(triple8)] The cat needs the rabbit.[(triple9 OR ((triple4) -> rule8) OR ((((triple10) -> rule6)) -> rule8))] The cat sees the bear.[(triple10)] The cat sees the rabbit.[(triple11)] The cat visits the bear.[(triple12)] The rabbit is cold.[(triple13)] The rabbit is red.[(triple14)] The rabbit visits the bear.[(triple15)] @1: The bear sees the bear.[(((triple3 triple4) -> rule4))] The cat needs the cat.[(((triple10) -> rule7))] The cat sees the cat.[(((triple10) -> rule6))] @2: The bear needs the cat.[(((((triple3 triple4) -> rule4)) -> rule7))]
The bear is cold.
("bear" "is" "cold" "+")
triple1
The bear is nice.
("bear" "is" "nice" "+")
triple2
The bear needs the rabbit.
("bear" "needs" "rabbit" "+")
triple3
The bear sees the cat.
("bear" "sees" "cat" "+")
triple4
The bear sees the rabbit.
("bear" "sees" "rabbit" "+")
triple5
The bear visits the rabbit.
("bear" "visits" "rabbit" "+")
triple6
((triple10) -> (rule1 % int1))
The bear visits the rabbit.
("bear" "visits" "rabbit" "+")
int1
((((triple3 triple4) -> (rule4 % int2))) -> (rule1 % int1))
The bear visits the rabbit.
("bear" "visits" "rabbit" "+")
int1
The bear sees the bear.
("bear" "sees" "bear" "+")
int2
The cat is kind.
("cat" "is" "kind" "+")
triple7
The cat is nice.
("cat" "is" "nice" "+")
triple8
The cat needs the rabbit.
("cat" "needs" "rabbit" "+")
triple9
((triple4) -> (rule8 % int1))
The cat needs the rabbit.
("cat" "needs" "rabbit" "+")
int1
((((triple10) -> (rule6 % int2))) -> (rule8 % int1))
The cat needs the rabbit.
("cat" "needs" "rabbit" "+")
int1
The cat sees the cat.
("cat" "sees" "cat" "+")
int2
The cat sees the bear.
("cat" "sees" "bear" "+")
triple10
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
triple11
The cat visits the bear.
("cat" "visits" "bear" "+")
triple12
The rabbit is cold.
("rabbit" "is" "cold" "+")
triple13
The rabbit is red.
("rabbit" "is" "red" "+")
triple14
The rabbit visits the bear.
("rabbit" "visits" "bear" "+")
triple15
The bear sees the bear.
("bear" "sees" "bear" "+")
((triple3 triple4) -> (rule4 % int1))
The bear sees the bear.
("bear" "sees" "bear" "+")
int1
The cat needs the cat.
("cat" "needs" "cat" "+")
((triple10) -> (rule7 % int1))
The cat needs the cat.
("cat" "needs" "cat" "+")
int1
The cat sees the cat.
("cat" "sees" "cat" "+")
((triple10) -> (rule6 % int1))
The cat sees the cat.
("cat" "sees" "cat" "+")
int1
The bear needs the cat.
("bear" "needs" "cat" "+")
((((triple3 triple4) -> (rule4 % int2))) -> (rule7 % int1))
The bear needs the cat.
("bear" "needs" "cat" "+")
int1
The bear sees the bear.
("bear" "sees" "bear" "+")
int2