The bear is not green. The bear is nice. The bear is red. The bear visits the rabbit. The bear visits the tiger. The rabbit chases the tiger. The rabbit eats the bear. The rabbit eats the tiger. The rabbit is blue. The rabbit visits the tiger. The tiger does not chase the rabbit. The tiger visits the rabbit. If something chases the bear and the bear does not chase the tiger then the bear does not eat the tiger. If something visits the rabbit and the rabbit chases the tiger then the rabbit chases the bear. If something is green then it eats the tiger. If something chases the tiger then it chases the rabbit. If something visits the tiger and it does not visit the bear then the bear is young. If the tiger visits the rabbit then the tiger does not eat the rabbit. If something is blue and it visits the bear then the bear does not chase the rabbit. If something is young then it eats the bear.
The bear is not green.
("bear" "is" "green" "-")
The bear is nice.
("bear" "is" "nice" "+")
The bear is red.
("bear" "is" "red" "+")
The bear visits the rabbit.
("bear" "visits" "rabbit" "+")
The bear visits the tiger.
("bear" "visits" "tiger" "+")
The rabbit chases the tiger.
("rabbit" "chases" "tiger" "+")
The rabbit eats the bear.
("rabbit" "eats" "bear" "+")
The rabbit eats the tiger.
("rabbit" "eats" "tiger" "+")
The rabbit is blue.
("rabbit" "is" "blue" "+")
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
The tiger does not chase the rabbit.
("tiger" "chases" "rabbit" "-")
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
If something chases the bear and the bear does not chase the tiger then the bear does not eat the tiger.
((("something" "chases" "bear" "+") ("bear" "chases" "tiger" "~")) -> ("bear" "eats" "tiger" "-"))
If something visits the rabbit and the rabbit chases the tiger then the rabbit chases the bear.
((("something" "visits" "rabbit" "+") ("rabbit" "chases" "tiger" "+")) -> ("rabbit" "chases" "bear" "+"))
If something is green then it eats the tiger.
((("something" "is" "green" "+")) -> ("something" "eats" "tiger" "+"))
If something chases the tiger then it chases the rabbit.
((("something" "chases" "tiger" "+")) -> ("something" "chases" "rabbit" "+"))
If something visits the tiger and it does not visit the bear then the bear is young.
((("something" "visits" "tiger" "+") ("something" "visits" "bear" "~")) -> ("bear" "is" "young" "+"))
If the tiger visits the rabbit then the tiger does not eat the rabbit.
((("tiger" "visits" "rabbit" "+")) -> ("tiger" "eats" "rabbit" "-"))
If something is blue and it visits the bear then the bear does not chase the rabbit.
((("something" "is" "blue" "+") ("something" "visits" "bear" "+")) -> ("bear" "chases" "rabbit" "-"))
If something is young then it eats the bear.
((("something" "is" "young" "+")) -> ("something" "eats" "bear" "+"))
The rabbit is blue.
True
1
proof
[(triple9)]
("rabbit" "is" "blue" "+")
triple9
The bear does not visit the rabbit.
False
1
inv-proof
[(triple4)]
("bear" "visits" "rabbit" "-")
triple4
The rabbit chases the bear.
True
3
proof
[(((triple12 triple6) -> rule2) OR ((triple4 triple6) -> rule2))]
("rabbit" "chases" "bear" "+")
((triple12 triple6) -> (rule2 % int1))
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
int1
((triple4 triple6) -> (rule2 % int1))
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
int1
The tiger eats the rabbit.
False
2
inv-proof
[(((triple12) -> rule6))]
("tiger" "eats" "rabbit" "+")
((triple12) -> (rule6 % int1))
The tiger does not eat the rabbit.
("tiger" "eats" "rabbit" "-")
int1
The bear is not young.
Unknown
inv-rconc
[@1: The bear is young.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("bear" "is" "young" "-")
The tiger eats the bear.
Unknown
rconc
[@1: The tiger eats the bear.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("tiger" "eats" "bear" "+")
The rabbit does not visit the bear.
Unknown
inv-random
[@0: The rabbit visits the bear.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "visits" "bear" "-")
The rabbit is red.
Unknown
random
[@0: The rabbit is red.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "red" "+")
@0: The bear is nice.[(triple2)] The bear is not green.[(triple1)] The bear is red.[(triple3)] The bear visits the rabbit.[(triple4)] The bear visits the tiger.[(triple5)] The rabbit chases the tiger.[(triple6)] The rabbit eats the bear.[(triple7)] The rabbit eats the tiger.[(triple8)] The rabbit is blue.[(triple9)] The rabbit visits the tiger.[(triple10)] The tiger does not chase the rabbit.[(triple11)] The tiger visits the rabbit.[(triple12)] @1: The rabbit chases the bear.[(((triple12 triple6) -> rule2) OR ((triple4 triple6) -> rule2))] The rabbit chases the rabbit.[(((triple6) -> rule4))] The tiger does not eat the rabbit.[(((triple12) -> rule6))]
The bear is nice.
("bear" "is" "nice" "+")
triple2
The bear is not green.
("bear" "is" "green" "-")
triple1
The bear is red.
("bear" "is" "red" "+")
triple3
The bear visits the rabbit.
("bear" "visits" "rabbit" "+")
triple4
The bear visits the tiger.
("bear" "visits" "tiger" "+")
triple5
The rabbit chases the tiger.
("rabbit" "chases" "tiger" "+")
triple6
The rabbit eats the bear.
("rabbit" "eats" "bear" "+")
triple7
The rabbit eats the tiger.
("rabbit" "eats" "tiger" "+")
triple8
The rabbit is blue.
("rabbit" "is" "blue" "+")
triple9
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
triple10
The tiger does not chase the rabbit.
("tiger" "chases" "rabbit" "-")
triple11
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
triple12
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
((triple12 triple6) -> (rule2 % int1))
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
int1
((triple4 triple6) -> (rule2 % int1))
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
int1
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
((triple6) -> (rule4 % int1))
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int1
The tiger does not eat the rabbit.
("tiger" "eats" "rabbit" "-")
((triple12) -> (rule6 % int1))
The tiger does not eat the rabbit.
("tiger" "eats" "rabbit" "-")
int1