The bear is rough. The bear needs the squirrel. The mouse chases the bear. The mouse chases the squirrel. The mouse is round. The mouse needs the bear. The mouse needs the squirrel. The mouse sees the bear. The squirrel is not big. The squirrel is young. The squirrel does not need the mouse. The tiger is young. If something chases the tiger then the tiger is big. If something sees the mouse then it does not need the tiger. If the squirrel does not see the mouse then the mouse chases the bear. If something is round then it needs the squirrel. If something sees the bear then the bear chases the tiger. All big things are blue. If something needs the bear and it does not chase the bear then it sees the squirrel. If something sees the squirrel and it is round then the squirrel needs the tiger.
The bear is rough.
("bear" "is" "rough" "+")
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
The mouse chases the bear.
("mouse" "chases" "bear" "+")
The mouse chases the squirrel.
("mouse" "chases" "squirrel" "+")
The mouse is round.
("mouse" "is" "round" "+")
The mouse needs the bear.
("mouse" "needs" "bear" "+")
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
The mouse sees the bear.
("mouse" "sees" "bear" "+")
The squirrel is not big.
("squirrel" "is" "big" "-")
The squirrel is young.
("squirrel" "is" "young" "+")
The squirrel does not need the mouse.
("squirrel" "needs" "mouse" "-")
The tiger is young.
("tiger" "is" "young" "+")
If something chases the tiger then the tiger is big.
((("something" "chases" "tiger" "+")) -> ("tiger" "is" "big" "+"))
If something sees the mouse then it does not need the tiger.
((("something" "sees" "mouse" "+")) -> ("something" "needs" "tiger" "-"))
If the squirrel does not see the mouse then the mouse chases the bear.
((("squirrel" "sees" "mouse" "~")) -> ("mouse" "chases" "bear" "+"))
If something is round then it needs the squirrel.
((("something" "is" "round" "+")) -> ("something" "needs" "squirrel" "+"))
If something sees the bear then the bear chases the tiger.
((("something" "sees" "bear" "+")) -> ("bear" "chases" "tiger" "+"))
All big things are blue.
((("something" "is" "big" "+")) -> ("something" "is" "blue" "+"))
If something needs the bear and it does not chase the bear then it sees the squirrel.
((("something" "needs" "bear" "+") ("something" "chases" "bear" "~")) -> ("something" "sees" "squirrel" "+"))
If something sees the squirrel and it is round then the squirrel needs the tiger.
((("something" "sees" "squirrel" "+") ("something" "is" "round" "+")) -> ("squirrel" "needs" "tiger" "+"))
The mouse needs the squirrel.
True
1
proof
[(triple7 OR ((triple5) -> rule4))]
("mouse" "needs" "squirrel" "+")
triple7
((triple5) -> (rule4 % int1))
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
int1
The squirrel is not young.
False
1
inv-proof
[(triple10)]
("squirrel" "is" "young" "-")
triple10
The bear chases the tiger.
True
2
proof
[(((triple8) -> rule5))]
("bear" "chases" "tiger" "+")
((triple8) -> (rule5 % int1))
The bear chases the tiger.
("bear" "chases" "tiger" "+")
int1
The bear does not chase the tiger.
False
2
inv-proof
[(((triple8) -> rule5))]
("bear" "chases" "tiger" "-")
((triple8) -> (rule5 % int1))
The bear chases the tiger.
("bear" "chases" "tiger" "+")
int1
The tiger is big.
True
3
proof
[(((((triple8) -> rule5)) -> rule1))]
("tiger" "is" "big" "+")
((((triple8) -> (rule5 % int2))) -> (rule1 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
The bear chases the tiger.
("bear" "chases" "tiger" "+")
int2
The tiger is not big.
False
3
inv-proof
[(((((triple8) -> rule5)) -> rule1))]
("tiger" "is" "big" "-")
((((triple8) -> (rule5 % int2))) -> (rule1 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
The bear chases the tiger.
("bear" "chases" "tiger" "+")
int2
The tiger is blue.
True
4
proof
[(((((((triple8) -> rule5)) -> rule1)) -> rule6))]
("tiger" "is" "blue" "+")
((((((triple8) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
The tiger is blue.
("tiger" "is" "blue" "+")
int1
The tiger is big.
("tiger" "is" "big" "+")
int2
The bear chases the tiger.
("bear" "chases" "tiger" "+")
int3
The tiger is not blue.
False
4
inv-proof
[(((((((triple8) -> rule5)) -> rule1)) -> rule6))]
("tiger" "is" "blue" "-")
((((((triple8) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
The tiger is blue.
("tiger" "is" "blue" "+")
int1
The tiger is big.
("tiger" "is" "big" "+")
int2
The bear chases the tiger.
("bear" "chases" "tiger" "+")
int3
The bear is not blue.
Unknown
inv-rconc
[@1: The bear is blue.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("bear" "is" "blue" "-")
The tiger sees the squirrel.
Unknown
rconc
[@1: The tiger sees the squirrel.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("tiger" "sees" "squirrel" "+")
The tiger does not need the squirrel.
Unknown
inv-rconc
[@1: The tiger needs the squirrel.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("tiger" "needs" "squirrel" "-")
The mouse sees the squirrel.
Unknown
rconc
[@1: The mouse sees the squirrel.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("mouse" "sees" "squirrel" "+")
The tiger does not need the mouse.
Unknown
inv-random
[@0: The tiger needs the mouse.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "needs" "mouse" "-")
The mouse needs the mouse.
Unknown
random
[@0: The mouse needs the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "mouse" "+")
The mouse does not need the tiger.
Unknown
inv-random
[@0: The mouse needs the tiger.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "tiger" "-")
The tiger sees the bear.
Unknown
random
[@0: The tiger sees the bear.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "bear" "+")
@0: The bear is rough.[(triple1)] The bear needs the squirrel.[(triple2)] The mouse chases the bear.[(triple3)] The mouse chases the squirrel.[(triple4)] The mouse is round.[(triple5)] The mouse needs the bear.[(triple6)] The mouse needs the squirrel.[(triple7 OR ((triple5) -> rule4))] The mouse sees the bear.[(triple8)] The squirrel does not need the mouse.[(triple11)] The squirrel is not big.[(triple9)] The squirrel is young.[(triple10)] The tiger is young.[(triple12)] @1: The bear chases the tiger.[(((triple8) -> rule5))] @2: The tiger is big.[(((((triple8) -> rule5)) -> rule1))] @3: The tiger is blue.[(((((((triple8) -> rule5)) -> rule1)) -> rule6))]
The bear is rough.
("bear" "is" "rough" "+")
triple1
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
triple2
The mouse chases the bear.
("mouse" "chases" "bear" "+")
triple3
The mouse chases the squirrel.
("mouse" "chases" "squirrel" "+")
triple4
The mouse is round.
("mouse" "is" "round" "+")
triple5
The mouse needs the bear.
("mouse" "needs" "bear" "+")
triple6
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
triple7
((triple5) -> (rule4 % int1))
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
int1
The mouse sees the bear.
("mouse" "sees" "bear" "+")
triple8
The squirrel does not need the mouse.
("squirrel" "needs" "mouse" "-")
triple11
The squirrel is not big.
("squirrel" "is" "big" "-")
triple9
The squirrel is young.
("squirrel" "is" "young" "+")
triple10
The tiger is young.
("tiger" "is" "young" "+")
triple12
The bear chases the tiger.
("bear" "chases" "tiger" "+")
((triple8) -> (rule5 % int1))
The bear chases the tiger.
("bear" "chases" "tiger" "+")
int1
The tiger is big.
("tiger" "is" "big" "+")
((((triple8) -> (rule5 % int2))) -> (rule1 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
The bear chases the tiger.
("bear" "chases" "tiger" "+")
int2
The tiger is blue.
("tiger" "is" "blue" "+")
((((((triple8) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
The tiger is blue.
("tiger" "is" "blue" "+")
int1
The tiger is big.
("tiger" "is" "big" "+")
int2
The bear chases the tiger.
("bear" "chases" "tiger" "+")
int3