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