The bear chases the mouse. The bear is big. The bear is cold. The bear is green. The bear is not round. The bear is not young. The bear needs the mouse. The bear does not visit the mouse. The mouse does not chase the bear. The mouse is not big. The mouse is cold. The mouse is not green. The mouse is round. The mouse is young. The mouse needs the bear. The mouse visits the bear. If something is cold then it needs the bear. If something chases the bear then it chases the mouse.
The bear chases the mouse.
("bear" "chases" "mouse" "+")
The bear is big.
("bear" "is" "big" "+")
The bear is cold.
("bear" "is" "cold" "+")
The bear is green.
("bear" "is" "green" "+")
The bear is not round.
("bear" "is" "round" "-")
The bear is not young.
("bear" "is" "young" "-")
The bear needs the mouse.
("bear" "needs" "mouse" "+")
The bear does not visit the mouse.
("bear" "visits" "mouse" "-")
The mouse does not chase the bear.
("mouse" "chases" "bear" "-")
The mouse is not big.
("mouse" "is" "big" "-")
The mouse is cold.
("mouse" "is" "cold" "+")
The mouse is not green.
("mouse" "is" "green" "-")
The mouse is round.
("mouse" "is" "round" "+")
The mouse is young.
("mouse" "is" "young" "+")
The mouse needs the bear.
("mouse" "needs" "bear" "+")
The mouse visits the bear.
("mouse" "visits" "bear" "+")
If something is cold then it needs the bear.
((("something" "is" "cold" "+")) -> ("something" "needs" "bear" "+"))
If something chases the bear then it chases the mouse.
((("something" "chases" "bear" "+")) -> ("something" "chases" "mouse" "+"))
The bear chases the mouse.
True
1
proof
[(triple1)]
("bear" "chases" "mouse" "+")
triple1
The mouse is not cold.
False
1
inv-proof
[(triple11)]
("mouse" "is" "cold" "-")
triple11
The bear needs the bear.
True
2
proof
[(((triple3) -> rule1))]
("bear" "needs" "bear" "+")
((triple3) -> (rule1 % int1))
The bear needs the bear.
("bear" "needs" "bear" "+")
int1
The bear does not need the bear.
False
2
inv-proof
[(((triple3) -> rule1))]
("bear" "needs" "bear" "-")
((triple3) -> (rule1 % int1))
The bear needs the bear.
("bear" "needs" "bear" "+")
int1
The mouse does not chase the mouse.
Unknown
inv-rconc
[@1: The mouse chases the mouse.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("mouse" "chases" "mouse" "-")
The bear visits the bear.
Unknown
random
[@0: The bear visits the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "visits" "bear" "+")
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 chases the bear.
Unknown
random
[@0: The bear chases the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "chases" "bear" "+")
@0: The bear chases the mouse.[(triple1)] The bear does not visit the mouse.[(triple8)] The bear is big.[(triple2)] The bear is cold.[(triple3)] The bear is green.[(triple4)] The bear is not round.[(triple5)] The bear is not young.[(triple6)] The bear needs the mouse.[(triple7)] The mouse does not chase the bear.[(triple9)] The mouse is cold.[(triple11)] The mouse is not big.[(triple10)] The mouse is not green.[(triple12)] The mouse is round.[(triple13)] The mouse is young.[(triple14)] The mouse needs the bear.[(triple15 OR ((triple11) -> rule1))] The mouse visits the bear.[(triple16)] @1: The bear needs the bear.[(((triple3) -> rule1))]
The bear chases the mouse.
("bear" "chases" "mouse" "+")
triple1
The bear does not visit the mouse.
("bear" "visits" "mouse" "-")
triple8
The bear is big.
("bear" "is" "big" "+")
triple2
The bear is cold.
("bear" "is" "cold" "+")
triple3
The bear is green.
("bear" "is" "green" "+")
triple4
The bear is not round.
("bear" "is" "round" "-")
triple5
The bear is not young.
("bear" "is" "young" "-")
triple6
The bear needs the mouse.
("bear" "needs" "mouse" "+")
triple7
The mouse does not chase the bear.
("mouse" "chases" "bear" "-")
triple9
The mouse is cold.
("mouse" "is" "cold" "+")
triple11
The mouse is not big.
("mouse" "is" "big" "-")
triple10
The mouse is not green.
("mouse" "is" "green" "-")
triple12
The mouse is round.
("mouse" "is" "round" "+")
triple13
The mouse is young.
("mouse" "is" "young" "+")
triple14
The mouse needs the bear.
("mouse" "needs" "bear" "+")
triple15
((triple11) -> (rule1 % int1))
The mouse needs the bear.
("mouse" "needs" "bear" "+")
int1
The mouse visits the bear.
("mouse" "visits" "bear" "+")
triple16
The bear needs the bear.
("bear" "needs" "bear" "+")
((triple3) -> (rule1 % int1))
The bear needs the bear.
("bear" "needs" "bear" "+")
int1