The bear is big. The lion eats the tiger. The rabbit sees the tiger. The tiger is nice. If the bear sees the rabbit then the rabbit sees the tiger. If someone likes the lion and the lion sees the rabbit then the rabbit is round. If someone is cold then they like the tiger. All nice people are cold. If someone eats the tiger and they see the tiger then the tiger sees the rabbit. If someone likes the tiger then they like the rabbit.
The bear is big.
("bear" "is" "big" "+")
The lion eats the tiger.
("lion" "eats" "tiger" "+")
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
The tiger is nice.
("tiger" "is" "nice" "+")
If the bear sees the rabbit then the rabbit sees the tiger.
((("bear" "sees" "rabbit" "+")) -> ("rabbit" "sees" "tiger" "+"))
If someone likes the lion and the lion sees the rabbit then the rabbit is round.
((("someone" "likes" "lion" "+") ("lion" "sees" "rabbit" "+")) -> ("rabbit" "is" "round" "+"))
If someone is cold then they like the tiger.
((("someone" "is" "cold" "+")) -> ("someone" "likes" "tiger" "+"))
All nice people are cold.
((("someone" "is" "nice" "+")) -> ("someone" "is" "cold" "+"))
If someone eats the tiger and they see the tiger then the tiger sees the rabbit.
((("someone" "eats" "tiger" "+") ("someone" "sees" "tiger" "+")) -> ("tiger" "sees" "rabbit" "+"))
If someone likes the tiger then they like the rabbit.
((("someone" "likes" "tiger" "+")) -> ("someone" "likes" "rabbit" "+"))
The lion eats the tiger.
True
1
proof
[(triple2)]
("lion" "eats" "tiger" "+")
triple2
The bear is not big.
False
1
inv-proof
[(triple1)]
("bear" "is" "big" "-")
triple1
The tiger is cold.
True
2
proof
[(((triple4) -> rule4))]
("tiger" "is" "cold" "+")
((triple4) -> (rule4 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
The tiger is not cold.
False
2
inv-proof
[(((triple4) -> rule4))]
("tiger" "is" "cold" "-")
((triple4) -> (rule4 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
The tiger likes the tiger.
True
3
proof
[(((((triple4) -> rule4)) -> rule3))]
("tiger" "likes" "tiger" "+")
((((triple4) -> (rule4 % int2))) -> (rule3 % int1))
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int1
The tiger is cold.
("tiger" "is" "cold" "+")
int2
The tiger does not like the tiger.
False
3
inv-proof
[(((((triple4) -> rule4)) -> rule3))]
("tiger" "likes" "tiger" "-")
((((triple4) -> (rule4 % int2))) -> (rule3 % int1))
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int1
The tiger is cold.
("tiger" "is" "cold" "+")
int2
The bear does not like the rabbit.
Unknown
inv-rconc
[@3: The bear likes the rabbit.[CWA. Example of deepest failure = (rule6 <- rule3 <- rule4 <- FAIL)]]
("bear" "likes" "rabbit" "-")
The bear is cold.
Unknown
rconc
[@1: The bear is cold.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("bear" "is" "cold" "+")
The rabbit is not cold.
Unknown
inv-rconc
[@1: The rabbit is cold.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("rabbit" "is" "cold" "-")
The rabbit eats the bear.
Unknown
random
[@0: The rabbit eats the bear.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "eats" "bear" "+")
The bear is not round.
Unknown
inv-random
[@0: The bear is round.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "round" "-")
The rabbit is green.
Unknown
random
[@0: The rabbit is green.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "green" "+")
@0: The bear is big.[(triple1)] The lion eats the tiger.[(triple2)] The rabbit sees the tiger.[(triple3)] The tiger is nice.[(triple4)] @1: The tiger is cold.[(((triple4) -> rule4))] @2: The tiger likes the tiger.[(((((triple4) -> rule4)) -> rule3))] @3: The tiger likes the rabbit.[(((((((triple4) -> rule4)) -> rule3)) -> rule6))]
The bear is big.
("bear" "is" "big" "+")
triple1
The lion eats the tiger.
("lion" "eats" "tiger" "+")
triple2
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
triple3
The tiger is nice.
("tiger" "is" "nice" "+")
triple4
The tiger is cold.
("tiger" "is" "cold" "+")
((triple4) -> (rule4 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
((((triple4) -> (rule4 % int2))) -> (rule3 % int1))
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int1
The tiger is cold.
("tiger" "is" "cold" "+")
int2
The tiger likes the rabbit.
("tiger" "likes" "rabbit" "+")
((((((triple4) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
The tiger likes the rabbit.
("tiger" "likes" "rabbit" "+")
int1
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int2
The tiger is cold.
("tiger" "is" "cold" "+")
int3