The bear is not cold. The lion is kind. The lion is young. The lion sees the bear. The mouse chases the bear. The mouse is green. The mouse is kind. The mouse is young. The mouse sees the bear. The mouse sees the lion. If something sees the bear and it is kind then the bear sees the lion. If something sees the lion then it sees the mouse. If something is cold and it needs the lion then the lion does not chase the mouse. If something needs the mouse then the mouse needs the lion. If something sees the bear then it does not chase the lion. If the bear sees the lion then the lion needs the mouse. If something sees the bear then it is cold. If something is red and not kind then it is young.
The bear is not cold.
("bear" "is" "cold" "-")
The lion is kind.
("lion" "is" "kind" "+")
The lion is young.
("lion" "is" "young" "+")
The lion sees the bear.
("lion" "sees" "bear" "+")
The mouse chases the bear.
("mouse" "chases" "bear" "+")
The mouse is green.
("mouse" "is" "green" "+")
The mouse is kind.
("mouse" "is" "kind" "+")
The mouse is young.
("mouse" "is" "young" "+")
The mouse sees the bear.
("mouse" "sees" "bear" "+")
The mouse sees the lion.
("mouse" "sees" "lion" "+")
If something sees the bear and it is kind then the bear sees the lion.
((("something" "sees" "bear" "+") ("something" "is" "kind" "+")) -> ("bear" "sees" "lion" "+"))
If something sees the lion then it sees the mouse.
((("something" "sees" "lion" "+")) -> ("something" "sees" "mouse" "+"))
If something is cold and it needs the lion then the lion does not chase the mouse.
((("something" "is" "cold" "+") ("something" "needs" "lion" "+")) -> ("lion" "chases" "mouse" "-"))
If something needs the mouse then the mouse needs the lion.
((("something" "needs" "mouse" "+")) -> ("mouse" "needs" "lion" "+"))
If something sees the bear then it does not chase the lion.
((("something" "sees" "bear" "+")) -> ("something" "chases" "lion" "-"))
If the bear sees the lion then the lion needs the mouse.
((("bear" "sees" "lion" "+")) -> ("lion" "needs" "mouse" "+"))
If something sees the bear then it is cold.
((("something" "sees" "bear" "+")) -> ("something" "is" "cold" "+"))
If something is red and not kind then it is young.
((("something" "is" "red" "+") ("something" "is" "kind" "~")) -> ("something" "is" "young" "+"))
The mouse is green.
True
1
proof
[(triple6)]
("mouse" "is" "green" "+")
triple6
The lion does not see the bear.
False
1
inv-proof
[(triple4)]
("lion" "sees" "bear" "-")
triple4
The mouse is cold.
True
2
proof
[(((triple9) -> rule7))]
("mouse" "is" "cold" "+")
((triple9) -> (rule7 % int1))
The mouse is cold.
("mouse" "is" "cold" "+")
int1
The mouse does not see the mouse.
False
2
inv-proof
[(((triple10) -> rule2))]
("mouse" "sees" "mouse" "-")
((triple10) -> (rule2 % int1))
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int1
The lion needs the mouse.
True
4
proof
[(((((triple4 triple2) -> rule1)) -> rule6) OR ((((triple9 triple7) -> rule1)) -> rule6))]
("lion" "needs" "mouse" "+")
((((triple4 triple2) -> (rule1 % int2))) -> (rule6 % int1))
The lion needs the mouse.
("lion" "needs" "mouse" "+")
int1
The bear sees the lion.
("bear" "sees" "lion" "+")
int2
((((triple9 triple7) -> (rule1 % int2))) -> (rule6 % int1))
The lion needs the mouse.
("lion" "needs" "mouse" "+")
int1
The bear sees the lion.
("bear" "sees" "lion" "+")
int2
The bear does not see the mouse.
False
4
inv-proof
[(((((triple4 triple2) -> rule1)) -> rule2) OR ((((triple9 triple7) -> rule1)) -> rule2))]
("bear" "sees" "mouse" "-")
((((triple4 triple2) -> (rule1 % int2))) -> (rule2 % int1))
The bear sees the mouse.
("bear" "sees" "mouse" "+")
int1
The bear sees the lion.
("bear" "sees" "lion" "+")
int2
((((triple9 triple7) -> (rule1 % int2))) -> (rule2 % int1))
The bear sees the mouse.
("bear" "sees" "mouse" "+")
int1
The bear sees the lion.
("bear" "sees" "lion" "+")
int2
The mouse needs the lion.
True
5
proof
[(((((((triple4 triple2) -> rule1)) -> rule6)) -> rule4) OR ((((((triple9 triple7) -> rule1)) -> rule6)) -> rule4))]
("mouse" "needs" "lion" "+")
((((((triple4 triple2) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
The mouse needs the lion.
("mouse" "needs" "lion" "+")
int1
The lion needs the mouse.
("lion" "needs" "mouse" "+")
int2
The bear sees the lion.
("bear" "sees" "lion" "+")
int3
((((((triple9 triple7) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
The mouse needs the lion.
("mouse" "needs" "lion" "+")
int1
The lion needs the mouse.
("lion" "needs" "mouse" "+")
int2
The bear sees the lion.
("bear" "sees" "lion" "+")
int3
The mouse does not need the lion.
False
5
inv-proof
[(((((((triple4 triple2) -> rule1)) -> rule6)) -> rule4) OR ((((((triple9 triple7) -> rule1)) -> rule6)) -> rule4))]
("mouse" "needs" "lion" "-")
((((((triple4 triple2) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
The mouse needs the lion.
("mouse" "needs" "lion" "+")
int1
The lion needs the mouse.
("lion" "needs" "mouse" "+")
int2
The bear sees the lion.
("bear" "sees" "lion" "+")
int3
((((((triple9 triple7) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
The mouse needs the lion.
("mouse" "needs" "lion" "+")
int1
The lion needs the mouse.
("lion" "needs" "mouse" "+")
int2
The bear sees the lion.
("bear" "sees" "lion" "+")
int3
The bear is not young.
Unknown
inv-rconc
[@1: The bear is young.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("bear" "is" "young" "-")
The lion sees the mouse.
Unknown
rconc
[@1: The lion sees the mouse.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("lion" "sees" "mouse" "+")
The bear does not need the bear.
Unknown
inv-random
[@0: The bear needs the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "needs" "bear" "-")
The mouse needs the bear.
Unknown
random
[@0: The mouse needs the bear.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "bear" "+")
The lion does not see the lion.
Unknown
inv-random
[@0: The lion sees the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "lion" "-")
The lion needs the bear.
Unknown
random
[@0: The lion needs the bear.[CWA. Example of deepest failure = (FAIL)]]
("lion" "needs" "bear" "+")
The bear does not need the mouse.
Unknown
inv-random
[@0: The bear needs the mouse.[CWA. Example of deepest failure = (FAIL)]]
("bear" "needs" "mouse" "-")
The lion needs the lion.
Unknown
random
[@0: The lion needs the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "needs" "lion" "+")
@0: The bear is not cold.[(triple1)] The lion is kind.[(triple2)] The lion is young.[(triple3)] The lion sees the bear.[(triple4)] The mouse chases the bear.[(triple5)] The mouse is green.[(triple6)] The mouse is kind.[(triple7)] The mouse is young.[(triple8)] The mouse sees the bear.[(triple9)] The mouse sees the lion.[(triple10)] @1: The bear sees the lion.[(((triple4 triple2) -> rule1) OR ((triple9 triple7) -> rule1))] The lion does not chase the lion.[(((triple4) -> rule5))] The lion is cold.[(((triple4) -> rule7))] The mouse does not chase the lion.[(((triple9) -> rule5))] The mouse is cold.[(((triple9) -> rule7))] The mouse sees the mouse.[(((triple10) -> rule2))] @2: The bear sees the mouse.[(((((triple4 triple2) -> rule1)) -> rule2) OR ((((triple9 triple7) -> rule1)) -> rule2))] The lion needs the mouse.[(((((triple4 triple2) -> rule1)) -> rule6) OR ((((triple9 triple7) -> rule1)) -> rule6))] @3: The mouse needs the lion.[(((((((triple4 triple2) -> rule1)) -> rule6)) -> rule4) OR ((((((triple9 triple7) -> rule1)) -> rule6)) -> rule4))] @4: The lion does not chase the mouse.[(((((triple9) -> rule7) ((((((triple4 triple2) -> rule1)) -> rule6)) -> rule4)) -> rule3) OR ((((triple9) -> rule7) ((((((triple9 triple7) -> rule1)) -> rule6)) -> rule4)) -> rule3))]
The bear is not cold.
("bear" "is" "cold" "-")
triple1
The lion is kind.
("lion" "is" "kind" "+")
triple2
The lion is young.
("lion" "is" "young" "+")
triple3
The lion sees the bear.
("lion" "sees" "bear" "+")
triple4
The mouse chases the bear.
("mouse" "chases" "bear" "+")
triple5
The mouse is green.
("mouse" "is" "green" "+")
triple6
The mouse is kind.
("mouse" "is" "kind" "+")
triple7
The mouse is young.
("mouse" "is" "young" "+")
triple8
The mouse sees the bear.
("mouse" "sees" "bear" "+")
triple9
The mouse sees the lion.
("mouse" "sees" "lion" "+")
triple10
The bear sees the lion.
("bear" "sees" "lion" "+")
((triple4 triple2) -> (rule1 % int1))
The bear sees the lion.
("bear" "sees" "lion" "+")
int1
((triple9 triple7) -> (rule1 % int1))
The bear sees the lion.
("bear" "sees" "lion" "+")
int1
The lion does not chase the lion.
("lion" "chases" "lion" "-")
((triple4) -> (rule5 % int1))
The lion does not chase the lion.
("lion" "chases" "lion" "-")
int1
The lion is cold.
("lion" "is" "cold" "+")
((triple4) -> (rule7 % int1))
The lion is cold.
("lion" "is" "cold" "+")
int1
The mouse does not chase the lion.
("mouse" "chases" "lion" "-")
((triple9) -> (rule5 % int1))
The mouse does not chase the lion.
("mouse" "chases" "lion" "-")
int1
The mouse is cold.
("mouse" "is" "cold" "+")
((triple9) -> (rule7 % int1))
The mouse is cold.
("mouse" "is" "cold" "+")
int1
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
((triple10) -> (rule2 % int1))
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int1
The bear sees the mouse.
("bear" "sees" "mouse" "+")
((((triple4 triple2) -> (rule1 % int2))) -> (rule2 % int1))
The bear sees the mouse.
("bear" "sees" "mouse" "+")
int1
The bear sees the lion.
("bear" "sees" "lion" "+")
int2
((((triple9 triple7) -> (rule1 % int2))) -> (rule2 % int1))
The bear sees the mouse.
("bear" "sees" "mouse" "+")
int1
The bear sees the lion.
("bear" "sees" "lion" "+")
int2
The lion needs the mouse.
("lion" "needs" "mouse" "+")
((((triple4 triple2) -> (rule1 % int2))) -> (rule6 % int1))
The lion needs the mouse.
("lion" "needs" "mouse" "+")
int1
The bear sees the lion.
("bear" "sees" "lion" "+")
int2
((((triple9 triple7) -> (rule1 % int2))) -> (rule6 % int1))
The lion needs the mouse.
("lion" "needs" "mouse" "+")
int1
The bear sees the lion.
("bear" "sees" "lion" "+")
int2
The mouse needs the lion.
("mouse" "needs" "lion" "+")
((((((triple4 triple2) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
The mouse needs the lion.
("mouse" "needs" "lion" "+")
int1
The lion needs the mouse.
("lion" "needs" "mouse" "+")
int2
The bear sees the lion.
("bear" "sees" "lion" "+")
int3
((((((triple9 triple7) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
The mouse needs the lion.
("mouse" "needs" "lion" "+")
int1
The lion needs the mouse.
("lion" "needs" "mouse" "+")
int2
The bear sees the lion.
("bear" "sees" "lion" "+")
int3
The lion does not chase the mouse.
("lion" "chases" "mouse" "-")
((((triple9) -> (rule7 % int5)) ((((((triple4 triple2) -> (rule1 % int4))) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
The lion does not chase the mouse.
("lion" "chases" "mouse" "-")
int1
The mouse needs the lion.
("mouse" "needs" "lion" "+")
int2
The lion needs the mouse.
("lion" "needs" "mouse" "+")
int3
The bear sees the lion.
("bear" "sees" "lion" "+")
int4
The mouse is cold.
("mouse" "is" "cold" "+")
int5
((((triple9) -> (rule7 % int5)) ((((((triple9 triple7) -> (rule1 % int4))) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
The lion does not chase the mouse.
("lion" "chases" "mouse" "-")
int1
The mouse needs the lion.
("mouse" "needs" "lion" "+")
int2
The lion needs the mouse.
("lion" "needs" "mouse" "+")
int3
The bear sees the lion.
("bear" "sees" "lion" "+")
int4
The mouse is cold.
("mouse" "is" "cold" "+")
int5