The bear is not round. The lion needs the bear. The mouse is green. The rabbit is kind. If something chases the lion then the lion is cold. If something needs the lion then the lion likes the mouse. If something chases the lion and the lion likes the bear then the lion is not green. If something chases the lion and it does not need the lion then it is round. If something likes the lion then the lion is not round. If something is green then it chases the lion. If the bear is round and the bear needs the mouse then the bear likes the mouse. If the lion is cold then the lion needs the rabbit.
The bear is not round.
("bear" "is" "round" "-")
The lion needs the bear.
("lion" "needs" "bear" "+")
The mouse is green.
("mouse" "is" "green" "+")
The rabbit is kind.
("rabbit" "is" "kind" "+")
If something chases the lion then the lion is cold.
((("something" "chases" "lion" "+")) -> ("lion" "is" "cold" "+"))
If something needs the lion then the lion likes the mouse.
((("something" "needs" "lion" "+")) -> ("lion" "likes" "mouse" "+"))
If something chases the lion and the lion likes the bear then the lion is not green.
((("something" "chases" "lion" "+") ("lion" "likes" "bear" "+")) -> ("lion" "is" "green" "-"))
If something chases the lion and it does not need the lion then it is round.
((("something" "chases" "lion" "+") ("something" "needs" "lion" "~")) -> ("something" "is" "round" "+"))
If something likes the lion then the lion is not round.
((("something" "likes" "lion" "+")) -> ("lion" "is" "round" "-"))
If something is green then it chases the lion.
((("something" "is" "green" "+")) -> ("something" "chases" "lion" "+"))
If the bear is round and the bear needs the mouse then the bear likes the mouse.
((("bear" "is" "round" "+") ("bear" "needs" "mouse" "+")) -> ("bear" "likes" "mouse" "+"))
If the lion is cold then the lion needs the rabbit.
((("lion" "is" "cold" "+")) -> ("lion" "needs" "rabbit" "+"))
The bear is not round.
True
1
proof
[(triple1)]
("bear" "is" "round" "-")
triple1
The rabbit is not kind.
False
1
inv-proof
[(triple4)]
("rabbit" "is" "kind" "-")
triple4
The mouse chases the lion.
True
2
proof
[(((triple3) -> rule6))]
("mouse" "chases" "lion" "+")
((triple3) -> (rule6 % int1))
The mouse chases the lion.
("mouse" "chases" "lion" "+")
int1
The mouse does not chase the lion.
False
2
inv-proof
[(((triple3) -> rule6))]
("mouse" "chases" "lion" "-")
((triple3) -> (rule6 % int1))
The mouse chases the lion.
("mouse" "chases" "lion" "+")
int1
The lion is cold.
True
3
proof
[(((((triple3) -> rule6)) -> rule1))]
("lion" "is" "cold" "+")
((((triple3) -> (rule6 % int2))) -> (rule1 % int1))
The lion is cold.
("lion" "is" "cold" "+")
int1
The mouse chases the lion.
("mouse" "chases" "lion" "+")
int2
The lion is not cold.
False
3
inv-proof
[(((((triple3) -> rule6)) -> rule1))]
("lion" "is" "cold" "-")
((((triple3) -> (rule6 % int2))) -> (rule1 % int1))
The lion is cold.
("lion" "is" "cold" "+")
int1
The mouse chases the lion.
("mouse" "chases" "lion" "+")
int2
The lion needs the rabbit.
True
4
proof
[(((((((triple3) -> rule6)) -> rule1)) -> rule8))]
("lion" "needs" "rabbit" "+")
((((((triple3) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule8 % int1))
The lion needs the rabbit.
("lion" "needs" "rabbit" "+")
int1
The lion is cold.
("lion" "is" "cold" "+")
int2
The mouse chases the lion.
("mouse" "chases" "lion" "+")
int3
The lion does not need the rabbit.
False
4
inv-proof
[(((((((triple3) -> rule6)) -> rule1)) -> rule8))]
("lion" "needs" "rabbit" "-")
((((((triple3) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule8 % int1))
The lion needs the rabbit.
("lion" "needs" "rabbit" "+")
int1
The lion is cold.
("lion" "is" "cold" "+")
int2
The mouse chases the lion.
("mouse" "chases" "lion" "+")
int3
The lion does not chase the lion.
Unknown
inv-rconc
[@1: The lion chases the lion.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("lion" "chases" "lion" "-")
The bear chases the lion.
Unknown
rconc
[@1: The bear chases the lion.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("bear" "chases" "lion" "+")
The rabbit does not chase the lion.
Unknown
inv-rconc
[@1: The rabbit chases the lion.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("rabbit" "chases" "lion" "-")
The mouse is round.
Unknown
rconc
[@1: The mouse is round.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("mouse" "is" "round" "+")
The bear does not chase the mouse.
Unknown
inv-random
[@0: The bear chases the mouse.[CWA. Example of deepest failure = (FAIL)]]
("bear" "chases" "mouse" "-")
The bear likes the lion.
Unknown
random
[@0: The bear likes the lion.[CWA. Example of deepest failure = (FAIL)]]
("bear" "likes" "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 bear likes the bear.
Unknown
random
[@0: The bear likes the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "likes" "bear" "+")
@0: The bear is not round.[(triple1)] The lion needs the bear.[(triple2)] The mouse is green.[(triple3)] The rabbit is kind.[(triple4)] @1: The mouse chases the lion.[(((triple3) -> rule6))] @2: The lion is cold.[(((((triple3) -> rule6)) -> rule1))] @3: The lion needs the rabbit.[(((((((triple3) -> rule6)) -> rule1)) -> rule8))]
The bear is not round.
("bear" "is" "round" "-")
triple1
The lion needs the bear.
("lion" "needs" "bear" "+")
triple2
The mouse is green.
("mouse" "is" "green" "+")
triple3
The rabbit is kind.
("rabbit" "is" "kind" "+")
triple4
The mouse chases the lion.
("mouse" "chases" "lion" "+")
((triple3) -> (rule6 % int1))
The mouse chases the lion.
("mouse" "chases" "lion" "+")
int1
The lion is cold.
("lion" "is" "cold" "+")
((((triple3) -> (rule6 % int2))) -> (rule1 % int1))
The lion is cold.
("lion" "is" "cold" "+")
int1
The mouse chases the lion.
("mouse" "chases" "lion" "+")
int2
The lion needs the rabbit.
("lion" "needs" "rabbit" "+")
((((((triple3) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule8 % int1))
The lion needs the rabbit.
("lion" "needs" "rabbit" "+")
int1
The lion is cold.
("lion" "is" "cold" "+")
int2
The mouse chases the lion.
("mouse" "chases" "lion" "+")
int3