The bear likes the rabbit. The lion visits the rabbit. The rabbit is cold. The tiger is round. If something likes the rabbit then it visits the bear. If something visits the bear then it likes the bear. If the tiger is nice and the tiger is big then the tiger visits the rabbit. If something likes the rabbit and it likes the bear then it is cold. If something is cold and big then it visits the rabbit. If something likes the lion and it likes the bear then it chases the tiger. If something likes the bear then the bear is nice. If something visits the rabbit then the rabbit visits the lion.
The bear likes the rabbit.
("bear" "likes" "rabbit" "+")
The lion visits the rabbit.
("lion" "visits" "rabbit" "+")
The rabbit is cold.
("rabbit" "is" "cold" "+")
The tiger is round.
("tiger" "is" "round" "+")
If something likes the rabbit then it visits the bear.
((("something" "likes" "rabbit" "+")) -> ("something" "visits" "bear" "+"))
If something visits the bear then it likes the bear.
((("something" "visits" "bear" "+")) -> ("something" "likes" "bear" "+"))
If the tiger is nice and the tiger is big then the tiger visits the rabbit.
((("tiger" "is" "nice" "+") ("tiger" "is" "big" "+")) -> ("tiger" "visits" "rabbit" "+"))
If something likes the rabbit and it likes the bear then it is cold.
((("something" "likes" "rabbit" "+") ("something" "likes" "bear" "+")) -> ("something" "is" "cold" "+"))
If something is cold and big then it visits the rabbit.
((("something" "is" "cold" "+") ("something" "is" "big" "+")) -> ("something" "visits" "rabbit" "+"))
If something likes the lion and it likes the bear then it chases the tiger.
((("something" "likes" "lion" "+") ("something" "likes" "bear" "+")) -> ("something" "chases" "tiger" "+"))
If something likes the bear then the bear is nice.
((("something" "likes" "bear" "+")) -> ("bear" "is" "nice" "+"))
If something visits the rabbit then the rabbit visits the lion.
((("something" "visits" "rabbit" "+")) -> ("rabbit" "visits" "lion" "+"))
The tiger is round.
True
1
proof
[(triple4)]
("tiger" "is" "round" "+")
triple4
The tiger is not round.
False
1
inv-proof
[(triple4)]
("tiger" "is" "round" "-")
triple4
The bear visits the bear.
True
2
proof
[(((triple1) -> rule1))]
("bear" "visits" "bear" "+")
((triple1) -> (rule1 % int1))
The bear visits the bear.
("bear" "visits" "bear" "+")
int1
The bear does not visit the bear.
False
2
inv-proof
[(((triple1) -> rule1))]
("bear" "visits" "bear" "-")
((triple1) -> (rule1 % int1))
The bear visits the bear.
("bear" "visits" "bear" "+")
int1
The bear likes the bear.
True
3
proof
[(((((triple1) -> rule1)) -> rule2))]
("bear" "likes" "bear" "+")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
The bear likes the bear.
("bear" "likes" "bear" "+")
int1
The bear visits the bear.
("bear" "visits" "bear" "+")
int2
The bear does not like the bear.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule2))]
("bear" "likes" "bear" "-")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
The bear likes the bear.
("bear" "likes" "bear" "+")
int1
The bear visits the bear.
("bear" "visits" "bear" "+")
int2
The bear is cold.
True
5
proof
[(((triple1 ((((triple1) -> rule1)) -> rule2)) -> rule4))]
("bear" "is" "cold" "+")
((triple1 ((((triple1) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
The bear is cold.
("bear" "is" "cold" "+")
int1
The bear likes the bear.
("bear" "likes" "bear" "+")
int2
The bear visits the bear.
("bear" "visits" "bear" "+")
int3
The bear is not nice.
False
4
inv-proof
[(((((((triple1) -> rule1)) -> rule2)) -> rule7))]
("bear" "is" "nice" "-")
((((((triple1) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
The bear is nice.
("bear" "is" "nice" "+")
int1
The bear likes the bear.
("bear" "likes" "bear" "+")
int2
The bear visits the bear.
("bear" "visits" "bear" "+")
int3
The rabbit does not like the bear.
Unknown
inv-rconc
[@2: The rabbit likes the bear.[CWA. Example of deepest failure = (rule2 <- rule1 <- FAIL)]]
("rabbit" "likes" "bear" "-")
The rabbit visits the rabbit.
Unknown
rconc
[@1: The rabbit visits the rabbit.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("rabbit" "visits" "rabbit" "+")
The lion does not like the bear.
Unknown
inv-rconc
[@2: The lion likes the bear.[CWA. Example of deepest failure = (rule2 <- rule1 <- FAIL)]]
("lion" "likes" "bear" "-")
The tiger chases the tiger.
Unknown
rconc
[@1: The tiger chases the tiger.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("tiger" "chases" "tiger" "+")
The lion is not nice.
Unknown
inv-random
[@0: The lion is nice.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "nice" "-")
The bear visits the lion.
Unknown
random
[@0: The bear visits the lion.[CWA. Example of deepest failure = (FAIL)]]
("bear" "visits" "lion" "+")
The rabbit does not like the rabbit.
Unknown
inv-random
[@0: The rabbit likes the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "likes" "rabbit" "-")
The lion is young.
Unknown
random
[@0: The lion is young.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "young" "+")
@0: The bear likes the rabbit.[(triple1)] The lion visits the rabbit.[(triple2)] The rabbit is cold.[(triple3)] The tiger is round.[(triple4)] @1: The bear visits the bear.[(((triple1) -> rule1))] The rabbit visits the lion.[(((triple2) -> rule8))] @2: The bear likes the bear.[(((((triple1) -> rule1)) -> rule2))] @3: The bear is cold.[(((triple1 ((((triple1) -> rule1)) -> rule2)) -> rule4))] The bear is nice.[(((((((triple1) -> rule1)) -> rule2)) -> rule7))]
The bear likes the rabbit.
("bear" "likes" "rabbit" "+")
triple1
The lion visits the rabbit.
("lion" "visits" "rabbit" "+")
triple2
The rabbit is cold.
("rabbit" "is" "cold" "+")
triple3
The tiger is round.
("tiger" "is" "round" "+")
triple4
The bear visits the bear.
("bear" "visits" "bear" "+")
((triple1) -> (rule1 % int1))
The bear visits the bear.
("bear" "visits" "bear" "+")
int1
The rabbit visits the lion.
("rabbit" "visits" "lion" "+")
((triple2) -> (rule8 % int1))
The rabbit visits the lion.
("rabbit" "visits" "lion" "+")
int1
The bear likes the bear.
("bear" "likes" "bear" "+")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
The bear likes the bear.
("bear" "likes" "bear" "+")
int1
The bear visits the bear.
("bear" "visits" "bear" "+")
int2
The bear is cold.
("bear" "is" "cold" "+")
((triple1 ((((triple1) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
The bear is cold.
("bear" "is" "cold" "+")
int1
The bear likes the bear.
("bear" "likes" "bear" "+")
int2
The bear visits the bear.
("bear" "visits" "bear" "+")
int3
The bear is nice.
("bear" "is" "nice" "+")
((((((triple1) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
The bear is nice.
("bear" "is" "nice" "+")
int1
The bear likes the bear.
("bear" "likes" "bear" "+")
int2
The bear visits the bear.
("bear" "visits" "bear" "+")
int3