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