The bald eagle is big. The bald eagle is rough. The bald eagle does not need the cow. The bald eagle does not need the lion. The cow is blue. The cow needs the lion. The cow sees the lion. The lion is cold. The lion sees the mouse. The mouse chases the lion. The mouse needs the bald eagle. The mouse needs the lion. The mouse sees the bald eagle. The mouse sees the lion. If something is rough and blue then it is big. If something is cold then it sees the mouse. If something is big then it is cold. If the cow is blue then the cow is rough. If something sees the lion and it sees the mouse then the lion is young. If the cow is rough and the cow is not cold then the cow sees the mouse.
The bald eagle is big.
("bald eagle" "is" "big" "+")
The bald eagle is rough.
("bald eagle" "is" "rough" "+")
The bald eagle does not need the cow.
("bald eagle" "needs" "cow" "-")
The bald eagle does not need the lion.
("bald eagle" "needs" "lion" "-")
The cow is blue.
("cow" "is" "blue" "+")
The cow needs the lion.
("cow" "needs" "lion" "+")
The cow sees the lion.
("cow" "sees" "lion" "+")
The lion is cold.
("lion" "is" "cold" "+")
The lion sees the mouse.
("lion" "sees" "mouse" "+")
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 sees the bald eagle.
("mouse" "sees" "bald eagle" "+")
The mouse sees the lion.
("mouse" "sees" "lion" "+")
If something is rough and blue then it is big.
((("something" "is" "rough" "+") ("something" "is" "blue" "+")) -> ("something" "is" "big" "+"))
If something is cold then it sees the mouse.
((("something" "is" "cold" "+")) -> ("something" "sees" "mouse" "+"))
If something is big then it is cold.
((("something" "is" "big" "+")) -> ("something" "is" "cold" "+"))
If the cow is blue then the cow is rough.
((("cow" "is" "blue" "+")) -> ("cow" "is" "rough" "+"))
If something sees the lion and it sees the mouse then the lion is young.
((("something" "sees" "lion" "+") ("something" "sees" "mouse" "+")) -> ("lion" "is" "young" "+"))
If the cow is rough and the cow is not cold then the cow sees the mouse.
((("cow" "is" "rough" "+") ("cow" "is" "cold" "~")) -> ("cow" "sees" "mouse" "+"))
The mouse sees the lion.
True
1
proof
[(triple14)]
("mouse" "sees" "lion" "+")
triple14
The bald eagle is not big.
False
1
inv-proof
[(triple1)]
("bald eagle" "is" "big" "-")
triple1
The cow is rough.
True
2
proof
[(((triple5) -> rule4))]
("cow" "is" "rough" "+")
((triple5) -> (rule4 % int1))
The cow is rough.
("cow" "is" "rough" "+")
int1
The bald eagle is not cold.
False
2
inv-proof
[(((triple1) -> rule3))]
("bald eagle" "is" "cold" "-")
((triple1) -> (rule3 % int1))
The bald eagle is cold.
("bald eagle" "is" "cold" "+")
int1
The bald eagle sees the mouse.
True
3
proof
[(((((triple1) -> rule3)) -> rule2))]
("bald eagle" "sees" "mouse" "+")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
The bald eagle sees the mouse.
("bald eagle" "sees" "mouse" "+")
int1
The bald eagle is cold.
("bald eagle" "is" "cold" "+")
int2
The cow is not big.
False
4
inv-proof
[(((((triple5) -> rule4) triple5) -> rule1))]
("cow" "is" "big" "-")
((((triple5) -> (rule4 % int2)) triple5) -> (rule1 % int1))
The cow is big.
("cow" "is" "big" "+")
int1
The cow is rough.
("cow" "is" "rough" "+")
int2
The cow is cold.
True
5
proof
[(((((((triple5) -> rule4) triple5) -> rule1)) -> rule3))]
("cow" "is" "cold" "+")
((((((triple5) -> (rule4 % int3)) triple5) -> (rule1 % int2))) -> (rule3 % int1))
The cow is cold.
("cow" "is" "cold" "+")
int1
The cow is big.
("cow" "is" "big" "+")
int2
The cow is rough.
("cow" "is" "rough" "+")
int3
The cow is not cold.
False
5
inv-proof
[(((((((triple5) -> rule4) triple5) -> rule1)) -> rule3))]
("cow" "is" "cold" "-")
((((((triple5) -> (rule4 % int3)) triple5) -> (rule1 % int2))) -> (rule3 % int1))
The cow is cold.
("cow" "is" "cold" "+")
int1
The cow is big.
("cow" "is" "big" "+")
int2
The cow is rough.
("cow" "is" "rough" "+")
int3
The cow sees the mouse.
True
6
proof
[(((((((((triple5) -> rule4) triple5) -> rule1)) -> rule3)) -> rule2))]
("cow" "sees" "mouse" "+")
((((((((triple5) -> (rule4 % int4)) triple5) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The cow sees the mouse.
("cow" "sees" "mouse" "+")
int1
The cow is cold.
("cow" "is" "cold" "+")
int2
The cow is big.
("cow" "is" "big" "+")
int3
The cow is rough.
("cow" "is" "rough" "+")
int4
The cow does not see the mouse.
False
6
inv-proof
[(((((((((triple5) -> rule4) triple5) -> rule1)) -> rule3)) -> rule2))]
("cow" "sees" "mouse" "-")
((((((((triple5) -> (rule4 % int4)) triple5) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The cow sees the mouse.
("cow" "sees" "mouse" "+")
int1
The cow is cold.
("cow" "is" "cold" "+")
int2
The cow is big.
("cow" "is" "big" "+")
int3
The cow is rough.
("cow" "is" "rough" "+")
int4
The lion is young.
True
8
proof
[(((triple7 ((((((((triple5) -> rule4) triple5) -> rule1)) -> rule3)) -> rule2)) -> rule5))]
("lion" "is" "young" "+")
((triple7 ((((((((triple5) -> (rule4 % int5)) triple5) -> (rule1 % int4))) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
The cow sees the mouse.
("cow" "sees" "mouse" "+")
int2
The cow is cold.
("cow" "is" "cold" "+")
int3
The cow is big.
("cow" "is" "big" "+")
int4
The cow is rough.
("cow" "is" "rough" "+")
int5
The lion is not young.
False
8
inv-proof
[(((triple7 ((((((((triple5) -> rule4) triple5) -> rule1)) -> rule3)) -> rule2)) -> rule5))]
("lion" "is" "young" "-")
((triple7 ((((((((triple5) -> (rule4 % int5)) triple5) -> (rule1 % int4))) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
The cow sees the mouse.
("cow" "sees" "mouse" "+")
int2
The cow is cold.
("cow" "is" "cold" "+")
int3
The cow is big.
("cow" "is" "big" "+")
int4
The cow is rough.
("cow" "is" "rough" "+")
int5
The mouse is not cold.
Unknown
inv-rconc
[@2: The mouse is cold.[CWA. Example of deepest failure = (rule3 <- rule1 <- FAIL)]]
("mouse" "is" "cold" "-")
The mouse sees the mouse.
Unknown
rconc
[@3: The mouse sees the mouse.[CWA. Example of deepest failure = (rule2 <- rule3 <- rule1 <- FAIL)]]
("mouse" "sees" "mouse" "+")
The lion is not big.
Unknown
inv-rconc
[@1: The lion is big.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("lion" "is" "big" "-")
The mouse is big.
Unknown
rconc
[@1: The mouse is big.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("mouse" "is" "big" "+")
The bald eagle does not chase the lion.
Unknown
inv-random
[@0: The bald eagle chases the lion.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "chases" "lion" "-")
The bald eagle needs the bald eagle.
Unknown
random
[@0: The bald eagle needs the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "needs" "bald eagle" "+")
The cow does not need the bald eagle.
Unknown
inv-random
[@0: The cow needs the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("cow" "needs" "bald eagle" "-")
The mouse chases the mouse.
Unknown
random
[@0: The mouse chases the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "chases" "mouse" "+")
The bald eagle does not see the cow.
Unknown
inv-random
[@0: The bald eagle sees the cow.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "sees" "cow" "-")
The lion needs the bald eagle.
Unknown
random
[@0: The lion needs the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("lion" "needs" "bald eagle" "+")
The lion does not see the bald eagle.
Unknown
inv-random
[@0: The lion sees the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "bald eagle" "-")
The cow needs the cow.
Unknown
random
[@0: The cow needs the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "needs" "cow" "+")
@0: The bald eagle does not need the cow.[(triple3)] The bald eagle does not need the lion.[(triple4)] The bald eagle is big.[(triple1)] The bald eagle is rough.[(triple2)] The cow is blue.[(triple5)] The cow needs the lion.[(triple6)] The cow sees the lion.[(triple7)] The lion is cold.[(triple8)] The lion sees the mouse.[(triple9 OR ((triple8) -> rule2))] The mouse chases the lion.[(triple10)] The mouse needs the bald eagle.[(triple11)] The mouse needs the lion.[(triple12)] The mouse sees the bald eagle.[(triple13)] The mouse sees the lion.[(triple14)] @1: The bald eagle is cold.[(((triple1) -> rule3))] The cow is rough.[(((triple5) -> rule4))] @2: The bald eagle sees the mouse.[(((((triple1) -> rule3)) -> rule2))] The cow is big.[(((((triple5) -> rule4) triple5) -> rule1))] @3: The cow is cold.[(((((((triple5) -> rule4) triple5) -> rule1)) -> rule3))] @4: The cow sees the mouse.[(((((((((triple5) -> rule4) triple5) -> rule1)) -> rule3)) -> rule2))] @5: The lion is young.[(((triple7 ((((((((triple5) -> rule4) triple5) -> rule1)) -> rule3)) -> rule2)) -> rule5))]
The bald eagle does not need the cow.
("bald eagle" "needs" "cow" "-")
triple3
The bald eagle does not need the lion.
("bald eagle" "needs" "lion" "-")
triple4
The bald eagle is big.
("bald eagle" "is" "big" "+")
triple1
The bald eagle is rough.
("bald eagle" "is" "rough" "+")
triple2
The cow is blue.
("cow" "is" "blue" "+")
triple5
The cow needs the lion.
("cow" "needs" "lion" "+")
triple6
The cow sees the lion.
("cow" "sees" "lion" "+")
triple7
The lion is cold.
("lion" "is" "cold" "+")
triple8
The lion sees the mouse.
("lion" "sees" "mouse" "+")
triple9
((triple8) -> (rule2 % int1))
The lion sees the mouse.
("lion" "sees" "mouse" "+")
int1
The mouse chases the lion.
("mouse" "chases" "lion" "+")
triple10
The mouse needs the bald eagle.
("mouse" "needs" "bald eagle" "+")
triple11
The mouse needs the lion.
("mouse" "needs" "lion" "+")
triple12
The mouse sees the bald eagle.
("mouse" "sees" "bald eagle" "+")
triple13
The mouse sees the lion.
("mouse" "sees" "lion" "+")
triple14
The bald eagle is cold.
("bald eagle" "is" "cold" "+")
((triple1) -> (rule3 % int1))
The bald eagle is cold.
("bald eagle" "is" "cold" "+")
int1
The cow is rough.
("cow" "is" "rough" "+")
((triple5) -> (rule4 % int1))
The cow is rough.
("cow" "is" "rough" "+")
int1
The bald eagle sees the mouse.
("bald eagle" "sees" "mouse" "+")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
The bald eagle sees the mouse.
("bald eagle" "sees" "mouse" "+")
int1
The bald eagle is cold.
("bald eagle" "is" "cold" "+")
int2
The cow is big.
("cow" "is" "big" "+")
((((triple5) -> (rule4 % int2)) triple5) -> (rule1 % int1))
The cow is big.
("cow" "is" "big" "+")
int1
The cow is rough.
("cow" "is" "rough" "+")
int2
The cow is cold.
("cow" "is" "cold" "+")
((((((triple5) -> (rule4 % int3)) triple5) -> (rule1 % int2))) -> (rule3 % int1))
The cow is cold.
("cow" "is" "cold" "+")
int1
The cow is big.
("cow" "is" "big" "+")
int2
The cow is rough.
("cow" "is" "rough" "+")
int3
The cow sees the mouse.
("cow" "sees" "mouse" "+")
((((((((triple5) -> (rule4 % int4)) triple5) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The cow sees the mouse.
("cow" "sees" "mouse" "+")
int1
The cow is cold.
("cow" "is" "cold" "+")
int2
The cow is big.
("cow" "is" "big" "+")
int3
The cow is rough.
("cow" "is" "rough" "+")
int4
The lion is young.
("lion" "is" "young" "+")
((triple7 ((((((((triple5) -> (rule4 % int5)) triple5) -> (rule1 % int4))) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
The cow sees the mouse.
("cow" "sees" "mouse" "+")
int2
The cow is cold.
("cow" "is" "cold" "+")
int3
The cow is big.
("cow" "is" "big" "+")
int4
The cow is rough.
("cow" "is" "rough" "+")
int5