The bear does not chase the rabbit. The bear chases the tiger. The bear eats the rabbit. The bear visits the tiger. The rabbit visits the tiger. The tiger is cold. The tiger is rough. The tiger is round. The tiger visits the bear. The tiger visits the rabbit. If something chases the rabbit and the rabbit is not young then it visits the tiger. If something visits the rabbit then the rabbit visits the bear. If something eats the tiger then it chases the rabbit. If something chases the rabbit then it does not visit the rabbit. If something eats the bear and it is round then it does not eat the rabbit. If something visits the bear and it eats the rabbit then the bear chases the tiger. If something is cold then it eats the bear. If something is kind and it does not chase the rabbit then it eats the bear.
The bear does not chase the rabbit.
("bear" "chases" "rabbit" "-")
The bear chases the tiger.
("bear" "chases" "tiger" "+")
The bear eats the rabbit.
("bear" "eats" "rabbit" "+")
The bear visits the tiger.
("bear" "visits" "tiger" "+")
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
The tiger is cold.
("tiger" "is" "cold" "+")
The tiger is rough.
("tiger" "is" "rough" "+")
The tiger is round.
("tiger" "is" "round" "+")
The tiger visits the bear.
("tiger" "visits" "bear" "+")
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
If something chases the rabbit and the rabbit is not young then it visits the tiger.
((("something" "chases" "rabbit" "+") ("rabbit" "is" "young" "~")) -> ("something" "visits" "tiger" "+"))
If something visits the rabbit then the rabbit visits the bear.
((("something" "visits" "rabbit" "+")) -> ("rabbit" "visits" "bear" "+"))
If something eats the tiger then it chases the rabbit.
((("something" "eats" "tiger" "+")) -> ("something" "chases" "rabbit" "+"))
If something chases the rabbit then it does not visit the rabbit.
((("something" "chases" "rabbit" "+")) -> ("something" "visits" "rabbit" "-"))
If something eats the bear and it is round then it does not eat the rabbit.
((("something" "eats" "bear" "+") ("something" "is" "round" "+")) -> ("something" "eats" "rabbit" "-"))
If something visits the bear and it eats the rabbit then the bear chases the tiger.
((("something" "visits" "bear" "+") ("something" "eats" "rabbit" "+")) -> ("bear" "chases" "tiger" "+"))
If something is cold then it eats the bear.
((("something" "is" "cold" "+")) -> ("something" "eats" "bear" "+"))
If something is kind and it does not chase the rabbit then it eats the bear.
((("something" "is" "kind" "+") ("something" "chases" "rabbit" "~")) -> ("something" "eats" "bear" "+"))
The tiger visits the bear.
True
1
proof
[(triple9)]
("tiger" "visits" "bear" "+")
triple9
The bear does not eat the rabbit.
False
1
inv-proof
[(triple3)]
("bear" "eats" "rabbit" "-")
triple3
The tiger eats the bear.
True
2
proof
[(((triple6) -> rule7))]
("tiger" "eats" "bear" "+")
((triple6) -> (rule7 % int1))
The tiger eats the bear.
("tiger" "eats" "bear" "+")
int1
The rabbit does not visit the bear.
False
2
inv-proof
[(((triple10) -> rule2))]
("rabbit" "visits" "bear" "-")
((triple10) -> (rule2 % int1))
The rabbit visits the bear.
("rabbit" "visits" "bear" "+")
int1
The tiger does not eat the rabbit.
True
4
proof
[(((((triple6) -> rule7) triple8) -> rule5))]
("tiger" "eats" "rabbit" "-")
((((triple6) -> (rule7 % int2)) triple8) -> (rule5 % int1))
The tiger does not eat the rabbit.
("tiger" "eats" "rabbit" "-")
int1
The tiger eats the bear.
("tiger" "eats" "bear" "+")
int2
The tiger eats the rabbit.
False
4
inv-proof
[(((((triple6) -> rule7) triple8) -> rule5))]
("tiger" "eats" "rabbit" "+")
((((triple6) -> (rule7 % int2)) triple8) -> (rule5 % int1))
The tiger does not eat the rabbit.
("tiger" "eats" "rabbit" "-")
int1
The tiger eats the bear.
("tiger" "eats" "bear" "+")
int2
The bear does not eat the bear.
Unknown
inv-rconc
[@1: The bear eats the bear.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("bear" "eats" "bear" "-")
The tiger chases the rabbit.
Unknown
rconc
[@1: The tiger chases the rabbit.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("tiger" "chases" "rabbit" "+")
The tiger does not visit the tiger.
Unknown
inv-rconc
[@1: The tiger visits the tiger.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("tiger" "visits" "tiger" "-")
The bear is round.
Unknown
random
[@0: The bear is round.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "round" "+")
The rabbit is not round.
Unknown
inv-random
[@0: The rabbit is round.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "round" "-")
The bear eats the tiger.
Unknown
random
[@0: The bear eats the tiger.[CWA. Example of deepest failure = (FAIL)]]
("bear" "eats" "tiger" "+")
@0: The bear chases the tiger.[(triple2)] The bear does not chase the rabbit.[(triple1)] The bear eats the rabbit.[(triple3)] The bear visits the tiger.[(triple4)] The rabbit visits the tiger.[(triple5)] The tiger is cold.[(triple6)] The tiger is rough.[(triple7)] The tiger is round.[(triple8)] The tiger visits the bear.[(triple9)] The tiger visits the rabbit.[(triple10)] @1: The rabbit visits the bear.[(((triple10) -> rule2))] The tiger eats the bear.[(((triple6) -> rule7))] @2: The tiger does not eat the rabbit.[(((((triple6) -> rule7) triple8) -> rule5))]
The bear chases the tiger.
("bear" "chases" "tiger" "+")
triple2
The bear does not chase the rabbit.
("bear" "chases" "rabbit" "-")
triple1
The bear eats the rabbit.
("bear" "eats" "rabbit" "+")
triple3
The bear visits the tiger.
("bear" "visits" "tiger" "+")
triple4
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
triple5
The tiger is cold.
("tiger" "is" "cold" "+")
triple6
The tiger is rough.
("tiger" "is" "rough" "+")
triple7
The tiger is round.
("tiger" "is" "round" "+")
triple8
The tiger visits the bear.
("tiger" "visits" "bear" "+")
triple9
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
triple10
The rabbit visits the bear.
("rabbit" "visits" "bear" "+")
((triple10) -> (rule2 % int1))
The rabbit visits the bear.
("rabbit" "visits" "bear" "+")
int1
The tiger eats the bear.
("tiger" "eats" "bear" "+")
((triple6) -> (rule7 % int1))
The tiger eats the bear.
("tiger" "eats" "bear" "+")
int1
The tiger does not eat the rabbit.
("tiger" "eats" "rabbit" "-")
((((triple6) -> (rule7 % int2)) triple8) -> (rule5 % int1))
The tiger does not eat the rabbit.
("tiger" "eats" "rabbit" "-")
int1
The tiger eats the bear.
("tiger" "eats" "bear" "+")
int2