The bald eagle is young. The bear chases the lion. The bear visits the bald eagle. The lion is kind. The mouse does not chase the bear. The mouse chases the lion. The mouse needs the bald eagle. The mouse needs the lion. The mouse does not visit the bear. The mouse does not visit the lion. Kind things are cold. If something needs the lion and it is young then it visits the bear. All young, green things are kind. If something chases the lion and the lion needs the mouse then it is kind. If something is cold then it needs the mouse. If something chases the mouse and the mouse visits the bear then it does not need the mouse.
The bald eagle is young.
("bald eagle" "is" "young" "+")
The bear chases the lion.
("bear" "chases" "lion" "+")
The bear visits the bald eagle.
("bear" "visits" "bald eagle" "+")
The lion is kind.
("lion" "is" "kind" "+")
The mouse does not chase the bear.
("mouse" "chases" "bear" "-")
The mouse chases the lion.
("mouse" "chases" "lion" "+")
The mouse needs the bald eagle.
("mouse" "needs" "bald eagle" "+")
The mouse needs the lion.
("mouse" "needs" "lion" "+")
The mouse does not visit the bear.
("mouse" "visits" "bear" "-")
The mouse does not visit the lion.
("mouse" "visits" "lion" "-")
Kind things are cold.
((("something" "is" "kind" "+")) -> ("something" "is" "cold" "+"))
If something needs the lion and it is young then it visits the bear.
((("something" "needs" "lion" "+") ("something" "is" "young" "+")) -> ("something" "visits" "bear" "+"))
All young, green things are kind.
((("something" "is" "young" "+") ("something" "is" "green" "+")) -> ("something" "is" "kind" "+"))
If something chases the lion and the lion needs the mouse then it is kind.
((("something" "chases" "lion" "+") ("lion" "needs" "mouse" "+")) -> ("something" "is" "kind" "+"))
If something is cold then it needs the mouse.
((("something" "is" "cold" "+")) -> ("something" "needs" "mouse" "+"))
If something chases the mouse and the mouse visits the bear then it does not need the mouse.
((("something" "chases" "mouse" "+") ("mouse" "visits" "bear" "+")) -> ("something" "needs" "mouse" "-"))
The lion is kind.
True
1
proof
[(triple4)]
("lion" "is" "kind" "+")
triple4
The mouse chases the bear.
False
1
inv-proof
[(triple5)]
("mouse" "chases" "bear" "+")
triple5
The lion is cold.
True
2
proof
[(((triple4) -> rule1))]
("lion" "is" "cold" "+")
((triple4) -> (rule1 % int1))
The lion is cold.
("lion" "is" "cold" "+")
int1
The lion is not cold.
False
2
inv-proof
[(((triple4) -> rule1))]
("lion" "is" "cold" "-")
((triple4) -> (rule1 % int1))
The lion is cold.
("lion" "is" "cold" "+")
int1
The lion needs the mouse.
True
3
proof
[(((((triple4) -> rule1)) -> rule5))]
("lion" "needs" "mouse" "+")
((((triple4) -> (rule1 % int2))) -> (rule5 % int1))
The lion needs the mouse.
("lion" "needs" "mouse" "+")
int1
The lion is cold.
("lion" "is" "cold" "+")
int2
The lion does not need the mouse.
False
3
inv-proof
[(((((triple4) -> rule1)) -> rule5))]
("lion" "needs" "mouse" "-")
((((triple4) -> (rule1 % int2))) -> (rule5 % int1))
The lion needs the mouse.
("lion" "needs" "mouse" "+")
int1
The lion is cold.
("lion" "is" "cold" "+")
int2
The mouse is kind.
True
5
proof
[(((triple6 ((((triple4) -> rule1)) -> rule5)) -> rule4))]
("mouse" "is" "kind" "+")
((triple6 ((((triple4) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
The mouse is kind.
("mouse" "is" "kind" "+")
int1
The lion needs the mouse.
("lion" "needs" "mouse" "+")
int2
The lion is cold.
("lion" "is" "cold" "+")
int3
The bear is not kind.
False
5
inv-proof
[(((triple2 ((((triple4) -> rule1)) -> rule5)) -> rule4))]
("bear" "is" "kind" "-")
((triple2 ((((triple4) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
The bear is kind.
("bear" "is" "kind" "+")
int1
The lion needs the mouse.
("lion" "needs" "mouse" "+")
int2
The lion is cold.
("lion" "is" "cold" "+")
int3
The mouse is cold.
True
6
proof
[(((((triple6 ((((triple4) -> rule1)) -> rule5)) -> rule4)) -> rule1))]
("mouse" "is" "cold" "+")
((((triple6 ((((triple4) -> (rule1 % int4))) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
The mouse is cold.
("mouse" "is" "cold" "+")
int1
The mouse is kind.
("mouse" "is" "kind" "+")
int2
The lion needs the mouse.
("lion" "needs" "mouse" "+")
int3
The lion is cold.
("lion" "is" "cold" "+")
int4
The bear is not cold.
False
6
inv-proof
[(((((triple2 ((((triple4) -> rule1)) -> rule5)) -> rule4)) -> rule1))]
("bear" "is" "cold" "-")
((((triple2 ((((triple4) -> (rule1 % int4))) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
The bear is cold.
("bear" "is" "cold" "+")
int1
The bear is kind.
("bear" "is" "kind" "+")
int2
The lion needs the mouse.
("lion" "needs" "mouse" "+")
int3
The lion is cold.
("lion" "is" "cold" "+")
int4
The bear needs the mouse.
True
7
proof
[(((((((triple2 ((((triple4) -> rule1)) -> rule5)) -> rule4)) -> rule1)) -> rule5))]
("bear" "needs" "mouse" "+")
((((((triple2 ((((triple4) -> (rule1 % int5))) -> (rule5 % int4))) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
The bear needs the mouse.
("bear" "needs" "mouse" "+")
int1
The bear is cold.
("bear" "is" "cold" "+")
int2
The bear is kind.
("bear" "is" "kind" "+")
int3
The lion needs the mouse.
("lion" "needs" "mouse" "+")
int4
The lion is cold.
("lion" "is" "cold" "+")
int5
The mouse does not need the mouse.
False
7
inv-proof
[(((((((triple6 ((((triple4) -> rule1)) -> rule5)) -> rule4)) -> rule1)) -> rule5))]
("mouse" "needs" "mouse" "-")
((((((triple6 ((((triple4) -> (rule1 % int5))) -> (rule5 % int4))) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int1
The mouse is cold.
("mouse" "is" "cold" "+")
int2
The mouse is kind.
("mouse" "is" "kind" "+")
int3
The lion needs the mouse.
("lion" "needs" "mouse" "+")
int4
The lion is cold.
("lion" "is" "cold" "+")
int5
The bald eagle is not kind.
Unknown
inv-rconc
[@1: The bald eagle is kind.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("bald eagle" "is" "kind" "-")
The bald eagle is cold.
Unknown
rconc
[@2: The bald eagle is cold.[CWA. Example of deepest failure = (rule1 <- rule3 <- FAIL)]]
("bald eagle" "is" "cold" "+")
The bear does not visit the bear.
Unknown
inv-rconc
[@1: The bear visits the bear.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("bear" "visits" "bear" "-")
The bald eagle needs the mouse.
Unknown
rconc
[@3: The bald eagle needs the mouse.[CWA. Example of deepest failure = (rule5 <- rule1 <- rule3 <- FAIL)]]
("bald eagle" "needs" "mouse" "+")
The bald eagle does not visit the bear.
Unknown
inv-rconc
[@1: The bald eagle visits the bear.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("bald eagle" "visits" "bear" "-")
The lion visits the bear.
Unknown
rconc
[@1: The lion visits the bear.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("lion" "visits" "bear" "+")
The bald eagle does not visit the lion.
Unknown
inv-random
[@0: The bald eagle visits the lion.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "visits" "lion" "-")
The bear visits the lion.
Unknown
random
[@0: The bear visits the lion.[CWA. Example of deepest failure = (FAIL)]]
("bear" "visits" "lion" "+")
The lion is not green.
Unknown
inv-random
[@0: The lion is green.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "green" "-")
The lion chases the mouse.
Unknown
random
[@0: The lion chases the mouse.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "mouse" "+")
The lion does not visit the mouse.
Unknown
inv-random
[@0: The lion visits the mouse.[CWA. Example of deepest failure = (FAIL)]]
("lion" "visits" "mouse" "-")
The mouse is round.
Unknown
random
[@0: The mouse is round.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "round" "+")
@0: The bald eagle is young.[(triple1)] The bear chases the lion.[(triple2)] The bear visits the bald eagle.[(triple3)] The lion is kind.[(triple4)] The mouse chases the lion.[(triple6)] The mouse does not chase the bear.[(triple5)] The mouse does not visit the bear.[(triple9)] The mouse does not visit the lion.[(triple10)] The mouse needs the bald eagle.[(triple7)] The mouse needs the lion.[(triple8)] @1: The lion is cold.[(((triple4) -> rule1))] @2: The lion needs the mouse.[(((((triple4) -> rule1)) -> rule5))] @3: The bear is kind.[(((triple2 ((((triple4) -> rule1)) -> rule5)) -> rule4))] The mouse is kind.[(((triple6 ((((triple4) -> rule1)) -> rule5)) -> rule4))] @4: The bear is cold.[(((((triple2 ((((triple4) -> rule1)) -> rule5)) -> rule4)) -> rule1))] The mouse is cold.[(((((triple6 ((((triple4) -> rule1)) -> rule5)) -> rule4)) -> rule1))] @5: The bear needs the mouse.[(((((((triple2 ((((triple4) -> rule1)) -> rule5)) -> rule4)) -> rule1)) -> rule5))] The mouse needs the mouse.[(((((((triple6 ((((triple4) -> rule1)) -> rule5)) -> rule4)) -> rule1)) -> rule5))]
The bald eagle is young.
("bald eagle" "is" "young" "+")
triple1
The bear chases the lion.
("bear" "chases" "lion" "+")
triple2
The bear visits the bald eagle.
("bear" "visits" "bald eagle" "+")
triple3
The lion is kind.
("lion" "is" "kind" "+")
triple4
The mouse chases the lion.
("mouse" "chases" "lion" "+")
triple6
The mouse does not chase the bear.
("mouse" "chases" "bear" "-")
triple5
The mouse does not visit the bear.
("mouse" "visits" "bear" "-")
triple9
The mouse does not visit the lion.
("mouse" "visits" "lion" "-")
triple10
The mouse needs the bald eagle.
("mouse" "needs" "bald eagle" "+")
triple7
The mouse needs the lion.
("mouse" "needs" "lion" "+")
triple8
The lion is cold.
("lion" "is" "cold" "+")
((triple4) -> (rule1 % int1))
The lion is cold.
("lion" "is" "cold" "+")
int1
The lion needs the mouse.
("lion" "needs" "mouse" "+")
((((triple4) -> (rule1 % int2))) -> (rule5 % int1))
The lion needs the mouse.
("lion" "needs" "mouse" "+")
int1
The lion is cold.
("lion" "is" "cold" "+")
int2
The bear is kind.
("bear" "is" "kind" "+")
((triple2 ((((triple4) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
The bear is kind.
("bear" "is" "kind" "+")
int1
The lion needs the mouse.
("lion" "needs" "mouse" "+")
int2
The lion is cold.
("lion" "is" "cold" "+")
int3
The mouse is kind.
("mouse" "is" "kind" "+")
((triple6 ((((triple4) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
The mouse is kind.
("mouse" "is" "kind" "+")
int1
The lion needs the mouse.
("lion" "needs" "mouse" "+")
int2
The lion is cold.
("lion" "is" "cold" "+")
int3
The bear is cold.
("bear" "is" "cold" "+")
((((triple2 ((((triple4) -> (rule1 % int4))) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
The bear is cold.
("bear" "is" "cold" "+")
int1
The bear is kind.
("bear" "is" "kind" "+")
int2
The lion needs the mouse.
("lion" "needs" "mouse" "+")
int3
The lion is cold.
("lion" "is" "cold" "+")
int4
The mouse is cold.
("mouse" "is" "cold" "+")
((((triple6 ((((triple4) -> (rule1 % int4))) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
The mouse is cold.
("mouse" "is" "cold" "+")
int1
The mouse is kind.
("mouse" "is" "kind" "+")
int2
The lion needs the mouse.
("lion" "needs" "mouse" "+")
int3
The lion is cold.
("lion" "is" "cold" "+")
int4
The bear needs the mouse.
("bear" "needs" "mouse" "+")
((((((triple2 ((((triple4) -> (rule1 % int5))) -> (rule5 % int4))) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
The bear needs the mouse.
("bear" "needs" "mouse" "+")
int1
The bear is cold.
("bear" "is" "cold" "+")
int2
The bear is kind.
("bear" "is" "kind" "+")
int3
The lion needs the mouse.
("lion" "needs" "mouse" "+")
int4
The lion is cold.
("lion" "is" "cold" "+")
int5
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
((((((triple6 ((((triple4) -> (rule1 % int5))) -> (rule5 % int4))) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int1
The mouse is cold.
("mouse" "is" "cold" "+")
int2
The mouse is kind.
("mouse" "is" "kind" "+")
int3
The lion needs the mouse.
("lion" "needs" "mouse" "+")
int4
The lion is cold.
("lion" "is" "cold" "+")
int5