The bear eats the squirrel. The bear sees the squirrel. The lion chases the bear. The lion eats the squirrel. The lion eats the tiger. The lion is not rough. The lion sees the bear. The squirrel is cold. The squirrel is green. The tiger chases the squirrel. The tiger eats the squirrel. The tiger sees the squirrel. If something eats the tiger and the tiger is not rough then it is not young. Big things are young. If something eats the squirrel then it is big. Young things are not cold. If something eats the bear then it is not cold. If the squirrel sees the tiger then the tiger does not see the lion.
The bear eats the squirrel.
("bear" "eats" "squirrel" "+")
The bear sees the squirrel.
("bear" "sees" "squirrel" "+")
The lion chases the bear.
("lion" "chases" "bear" "+")
The lion eats the squirrel.
("lion" "eats" "squirrel" "+")
The lion eats the tiger.
("lion" "eats" "tiger" "+")
The lion is not rough.
("lion" "is" "rough" "-")
The lion sees the bear.
("lion" "sees" "bear" "+")
The squirrel is cold.
("squirrel" "is" "cold" "+")
The squirrel is green.
("squirrel" "is" "green" "+")
The tiger chases the squirrel.
("tiger" "chases" "squirrel" "+")
The tiger eats the squirrel.
("tiger" "eats" "squirrel" "+")
The tiger sees the squirrel.
("tiger" "sees" "squirrel" "+")
If something eats the tiger and the tiger is not rough then it is not young.
((("something" "eats" "tiger" "+") ("tiger" "is" "rough" "~")) -> ("something" "is" "young" "-"))
Big things are young.
((("something" "is" "big" "+")) -> ("something" "is" "young" "+"))
If something eats the squirrel then it is big.
((("something" "eats" "squirrel" "+")) -> ("something" "is" "big" "+"))
Young things are not cold.
((("something" "is" "young" "+")) -> ("something" "is" "cold" "-"))
If something eats the bear then it is not cold.
((("something" "eats" "bear" "+")) -> ("something" "is" "cold" "-"))
If the squirrel sees the tiger then the tiger does not see the lion.
((("squirrel" "sees" "tiger" "+")) -> ("tiger" "sees" "lion" "-"))
The lion eats the tiger.
True
1
proof
[(triple5)]
("lion" "eats" "tiger" "+")
triple5
The lion is rough.
False
1
inv-proof
[(triple6)]
("lion" "is" "rough" "+")
triple6
The bear is big.
True
2
proof
[(((triple1) -> rule3))]
("bear" "is" "big" "+")
((triple1) -> (rule3 % int1))
The bear is big.
("bear" "is" "big" "+")
int1
The lion is not big.
False
2
inv-proof
[(((triple4) -> rule3))]
("lion" "is" "big" "-")
((triple4) -> (rule3 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The lion is young.
True
3
proof
[(((((triple4) -> rule3)) -> rule2))]
("lion" "is" "young" "+")
((((triple4) -> (rule3 % int2))) -> (rule2 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
The lion is big.
("lion" "is" "big" "+")
int2
The bear is not young.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule2))]
("bear" "is" "young" "-")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
The bear is young.
("bear" "is" "young" "+")
int1
The bear is big.
("bear" "is" "big" "+")
int2
The lion is not cold.
True
4
proof
[(((((((triple4) -> rule3)) -> rule2)) -> rule4))]
("lion" "is" "cold" "-")
((((((triple4) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
The lion is not cold.
("lion" "is" "cold" "-")
int1
The lion is young.
("lion" "is" "young" "+")
int2
The lion is big.
("lion" "is" "big" "+")
int3
The tiger is cold.
False
4
inv-proof
[(((((((triple11) -> rule3)) -> rule2)) -> rule4))]
("tiger" "is" "cold" "+")
((((((triple11) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
The tiger is not cold.
("tiger" "is" "cold" "-")
int1
The tiger is young.
("tiger" "is" "young" "+")
int2
The tiger is big.
("tiger" "is" "big" "+")
int3
The squirrel is not young.
Unknown
inv-rconc
[@2: The squirrel is young.[CWA. Example of deepest failure = (rule2 <- rule3 <- FAIL)]]
("squirrel" "is" "young" "-")
The squirrel is big.
Unknown
rconc
[@1: The squirrel is big.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("squirrel" "is" "big" "+")
The squirrel does not chase the squirrel.
Unknown
inv-random
[@0: The squirrel chases the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "chases" "squirrel" "-")
The tiger sees the tiger.
Unknown
random
[@0: The tiger sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "tiger" "+")
The lion is not green.
Unknown
inv-random
[@0: The lion is green.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "green" "-")
The lion eats the lion.
Unknown
random
[@0: The lion eats the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "eats" "lion" "+")
The tiger does not eat the lion.
Unknown
inv-random
[@0: The tiger eats the lion.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "eats" "lion" "-")
The squirrel eats the squirrel.
Unknown
random
[@0: The squirrel eats the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "eats" "squirrel" "+")
@0: The bear eats the squirrel.[(triple1)] The bear sees the squirrel.[(triple2)] The lion chases the bear.[(triple3)] The lion eats the squirrel.[(triple4)] The lion eats the tiger.[(triple5)] The lion is not rough.[(triple6)] The lion sees the bear.[(triple7)] The squirrel is cold.[(triple8)] The squirrel is green.[(triple9)] The tiger chases the squirrel.[(triple10)] The tiger eats the squirrel.[(triple11)] The tiger sees the squirrel.[(triple12)] @1: The bear is big.[(((triple1) -> rule3))] The lion is big.[(((triple4) -> rule3))] The tiger is big.[(((triple11) -> rule3))] @2: The bear is young.[(((((triple1) -> rule3)) -> rule2))] The lion is young.[(((((triple4) -> rule3)) -> rule2))] The tiger is young.[(((((triple11) -> rule3)) -> rule2))] @3: The bear is not cold.[(((((((triple1) -> rule3)) -> rule2)) -> rule4))] The lion is not cold.[(((((((triple4) -> rule3)) -> rule2)) -> rule4))] The tiger is not cold.[(((((((triple11) -> rule3)) -> rule2)) -> rule4))]
The bear eats the squirrel.
("bear" "eats" "squirrel" "+")
triple1
The bear sees the squirrel.
("bear" "sees" "squirrel" "+")
triple2
The lion chases the bear.
("lion" "chases" "bear" "+")
triple3
The lion eats the squirrel.
("lion" "eats" "squirrel" "+")
triple4
The lion eats the tiger.
("lion" "eats" "tiger" "+")
triple5
The lion is not rough.
("lion" "is" "rough" "-")
triple6
The lion sees the bear.
("lion" "sees" "bear" "+")
triple7
The squirrel is cold.
("squirrel" "is" "cold" "+")
triple8
The squirrel is green.
("squirrel" "is" "green" "+")
triple9
The tiger chases the squirrel.
("tiger" "chases" "squirrel" "+")
triple10
The tiger eats the squirrel.
("tiger" "eats" "squirrel" "+")
triple11
The tiger sees the squirrel.
("tiger" "sees" "squirrel" "+")
triple12
The bear is big.
("bear" "is" "big" "+")
((triple1) -> (rule3 % int1))
The bear is big.
("bear" "is" "big" "+")
int1
The lion is big.
("lion" "is" "big" "+")
((triple4) -> (rule3 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The tiger is big.
("tiger" "is" "big" "+")
((triple11) -> (rule3 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
The bear is young.
("bear" "is" "young" "+")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
The bear is young.
("bear" "is" "young" "+")
int1
The bear is big.
("bear" "is" "big" "+")
int2
The lion is young.
("lion" "is" "young" "+")
((((triple4) -> (rule3 % int2))) -> (rule2 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
The lion is big.
("lion" "is" "big" "+")
int2
The tiger is young.
("tiger" "is" "young" "+")
((((triple11) -> (rule3 % int2))) -> (rule2 % int1))
The tiger is young.
("tiger" "is" "young" "+")
int1
The tiger is big.
("tiger" "is" "big" "+")
int2
The bear is not cold.
("bear" "is" "cold" "-")
((((((triple1) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
The bear is not cold.
("bear" "is" "cold" "-")
int1
The bear is young.
("bear" "is" "young" "+")
int2
The bear is big.
("bear" "is" "big" "+")
int3
The lion is not cold.
("lion" "is" "cold" "-")
((((((triple4) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
The lion is not cold.
("lion" "is" "cold" "-")
int1
The lion is young.
("lion" "is" "young" "+")
int2
The lion is big.
("lion" "is" "big" "+")
int3
The tiger is not cold.
("tiger" "is" "cold" "-")
((((((triple11) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
The tiger is not cold.
("tiger" "is" "cold" "-")
int1
The tiger is young.
("tiger" "is" "young" "+")
int2
The tiger is big.
("tiger" "is" "big" "+")
int3