The lion is big. The lion is not green. The lion does not like the rabbit. The lion likes the tiger. The rabbit does not like the lion. The tiger is red. The tiger sees the rabbit. If something likes the tiger then the tiger eats the rabbit. If something sees the tiger then it does not eat the tiger. If something is big and it sees the rabbit then the rabbit likes the lion. If something is kind and it does not eat the lion then the lion does not like the rabbit. If something eats the rabbit then the rabbit sees the tiger. All green things are not big. If something eats the rabbit and it is big then the rabbit sees the lion. If something likes the rabbit then the rabbit does not like the tiger.
The lion is big.
("lion" "is" "big" "+")
The lion is not green.
("lion" "is" "green" "-")
The lion does not like the rabbit.
("lion" "likes" "rabbit" "-")
The lion likes the tiger.
("lion" "likes" "tiger" "+")
The rabbit does not like the lion.
("rabbit" "likes" "lion" "-")
The tiger is red.
("tiger" "is" "red" "+")
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
If something likes the tiger then the tiger eats the rabbit.
((("something" "likes" "tiger" "+")) -> ("tiger" "eats" "rabbit" "+"))
If something sees the tiger then it does not eat the tiger.
((("something" "sees" "tiger" "+")) -> ("something" "eats" "tiger" "-"))
If something is big and it sees the rabbit then the rabbit likes the lion.
((("something" "is" "big" "+") ("something" "sees" "rabbit" "+")) -> ("rabbit" "likes" "lion" "+"))
If something is kind and it does not eat the lion then the lion does not like the rabbit.
((("something" "is" "kind" "+") ("something" "eats" "lion" "~")) -> ("lion" "likes" "rabbit" "-"))
If something eats the rabbit then the rabbit sees the tiger.
((("something" "eats" "rabbit" "+")) -> ("rabbit" "sees" "tiger" "+"))
All green things are not big.
((("something" "is" "green" "+")) -> ("something" "is" "big" "-"))
If something eats the rabbit and it is big then the rabbit sees the lion.
((("something" "eats" "rabbit" "+") ("something" "is" "big" "+")) -> ("rabbit" "sees" "lion" "+"))
If something likes the rabbit then the rabbit does not like the tiger.
((("something" "likes" "rabbit" "+")) -> ("rabbit" "likes" "tiger" "-"))
The lion is big.
True
1
proof
[(triple1)]
("lion" "is" "big" "+")
triple1
The tiger is not red.
False
1
inv-proof
[(triple6)]
("tiger" "is" "red" "-")
triple6
The tiger eats the rabbit.
True
2
proof
[(((triple4) -> rule1))]
("tiger" "eats" "rabbit" "+")
((triple4) -> (rule1 % int1))
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
int1
The tiger does not eat the rabbit.
False
2
inv-proof
[(((triple4) -> rule1))]
("tiger" "eats" "rabbit" "-")
((triple4) -> (rule1 % int1))
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
int1
The rabbit sees the tiger.
True
3
proof
[(((((triple4) -> rule1)) -> rule5))]
("rabbit" "sees" "tiger" "+")
((((triple4) -> (rule1 % int2))) -> (rule5 % int1))
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
int1
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
int2
The rabbit does not see the tiger.
False
3
inv-proof
[(((((triple4) -> rule1)) -> rule5))]
("rabbit" "sees" "tiger" "-")
((((triple4) -> (rule1 % int2))) -> (rule5 % int1))
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
int1
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
int2
The rabbit does not eat the tiger.
True
4
proof
[(((((((triple4) -> rule1)) -> rule5)) -> rule2))]
("rabbit" "eats" "tiger" "-")
((((((triple4) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
The rabbit does not eat the tiger.
("rabbit" "eats" "tiger" "-")
int1
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
int2
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
int3
The rabbit eats the tiger.
False
4
inv-proof
[(((((((triple4) -> rule1)) -> rule5)) -> rule2))]
("rabbit" "eats" "tiger" "+")
((((((triple4) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
The rabbit does not eat the tiger.
("rabbit" "eats" "tiger" "-")
int1
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
int2
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
int3
The rabbit does not see the lion.
Unknown
inv-rconc
[@1: The rabbit sees the lion.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("rabbit" "sees" "lion" "-")
The rabbit is green.
Unknown
random
[@0: The rabbit is green.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "green" "+")
The tiger is not nice.
Unknown
inv-random
[@0: The tiger is nice.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "nice" "-")
The rabbit likes the rabbit.
Unknown
random
[@0: The rabbit likes the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "likes" "rabbit" "+")
The rabbit does not like the tiger.
Unknown
inv-random
[@0: The rabbit likes the tiger.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "likes" "tiger" "-")
The lion eats the rabbit.
Unknown
random
[@0: The lion eats the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("lion" "eats" "rabbit" "+")
The tiger does not eat the tiger.
Unknown
inv-random
[@0: The tiger eats the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "eats" "tiger" "-")
The lion sees the tiger.
Unknown
random
[@0: The lion sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "tiger" "+")
@0: The lion does not like the rabbit.[(triple3)] The lion is big.[(triple1)] The lion is not green.[(triple2)] The lion likes the tiger.[(triple4)] The rabbit does not like the lion.[(triple5)] The tiger is red.[(triple6)] The tiger sees the rabbit.[(triple7)] @1: The tiger eats the rabbit.[(((triple4) -> rule1))] @2: The rabbit sees the tiger.[(((((triple4) -> rule1)) -> rule5))] @3: The rabbit does not eat the tiger.[(((((((triple4) -> rule1)) -> rule5)) -> rule2))]
The lion does not like the rabbit.
("lion" "likes" "rabbit" "-")
triple3
The lion is big.
("lion" "is" "big" "+")
triple1
The lion is not green.
("lion" "is" "green" "-")
triple2
The lion likes the tiger.
("lion" "likes" "tiger" "+")
triple4
The rabbit does not like the lion.
("rabbit" "likes" "lion" "-")
triple5
The tiger is red.
("tiger" "is" "red" "+")
triple6
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
triple7
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
((triple4) -> (rule1 % int1))
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
int1
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
((((triple4) -> (rule1 % int2))) -> (rule5 % int1))
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
int1
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
int2
The rabbit does not eat the tiger.
("rabbit" "eats" "tiger" "-")
((((((triple4) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
The rabbit does not eat the tiger.
("rabbit" "eats" "tiger" "-")
int1
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
int2
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
int3