The bear chases the lion. The bear chases the mouse. The bear eats the lion. The bear eats the mouse. The bear is cold. The bear is young. The bear visits the lion. The bear visits the mouse. The lion chases the bear. The lion is cold. The lion visits the bear. The lion visits the mouse. The mouse eats the bear. The mouse is big. The mouse visits the lion. All green people are round. If someone visits the lion and they chase the bear then the lion eats the bear. If someone chases the mouse and the mouse is big then they chase the bear. If someone eats the lion then the lion chases the bear. If someone is round then they visit the bear. If the bear chases the mouse then the bear is young. If the mouse chases the bear then the mouse is young. If someone eats the mouse then the mouse chases the lion.
The bear chases the lion.
("bear" "chases" "lion" "+")
The bear chases the mouse.
("bear" "chases" "mouse" "+")
The bear eats the lion.
("bear" "eats" "lion" "+")
The bear eats the mouse.
("bear" "eats" "mouse" "+")
The bear is cold.
("bear" "is" "cold" "+")
The bear is young.
("bear" "is" "young" "+")
The bear visits the lion.
("bear" "visits" "lion" "+")
The bear visits the mouse.
("bear" "visits" "mouse" "+")
The lion chases the bear.
("lion" "chases" "bear" "+")
The lion is cold.
("lion" "is" "cold" "+")
The lion visits the bear.
("lion" "visits" "bear" "+")
The lion visits the mouse.
("lion" "visits" "mouse" "+")
The mouse eats the bear.
("mouse" "eats" "bear" "+")
The mouse is big.
("mouse" "is" "big" "+")
The mouse visits the lion.
("mouse" "visits" "lion" "+")
All green people are round.
((("someone" "is" "green" "+")) -> ("someone" "is" "round" "+"))
If someone visits the lion and they chase the bear then the lion eats the bear.
((("someone" "visits" "lion" "+") ("someone" "chases" "bear" "+")) -> ("lion" "eats" "bear" "+"))
If someone chases the mouse and the mouse is big then they chase the bear.
((("someone" "chases" "mouse" "+") ("mouse" "is" "big" "+")) -> ("someone" "chases" "bear" "+"))
If someone eats the lion then the lion chases the bear.
((("someone" "eats" "lion" "+")) -> ("lion" "chases" "bear" "+"))
If someone is round then they visit the bear.
((("someone" "is" "round" "+")) -> ("someone" "visits" "bear" "+"))
If the bear chases the mouse then the bear is young.
((("bear" "chases" "mouse" "+")) -> ("bear" "is" "young" "+"))
If the mouse chases the bear then the mouse is young.
((("mouse" "chases" "bear" "+")) -> ("mouse" "is" "young" "+"))
If someone eats the mouse then the mouse chases the lion.
((("someone" "eats" "mouse" "+")) -> ("mouse" "chases" "lion" "+"))
The lion chases the bear.
True
1
proof
[(triple9 OR ((triple3) -> rule4))]
("lion" "chases" "bear" "+")
triple9
((triple3) -> (rule4 % int1))
The lion chases the bear.
("lion" "chases" "bear" "+")
int1
The bear does not eat the mouse.
False
1
inv-proof
[(triple4)]
("bear" "eats" "mouse" "-")
triple4
The bear chases the bear.
True
3
proof
[(((triple2 triple14) -> rule3))]
("bear" "chases" "bear" "+")
((triple2 triple14) -> (rule3 % int1))
The bear chases the bear.
("bear" "chases" "bear" "+")
int1
The mouse does not chase the lion.
False
2
inv-proof
[(((triple4) -> rule8))]
("mouse" "chases" "lion" "-")
((triple4) -> (rule8 % int1))
The mouse chases the lion.
("mouse" "chases" "lion" "+")
int1
The lion eats the bear.
True
5
proof
[(((triple7 ((triple2 triple14) -> rule3)) -> rule2))]
("lion" "eats" "bear" "+")
((triple7 ((triple2 triple14) -> (rule3 % int2))) -> (rule2 % int1))
The lion eats the bear.
("lion" "eats" "bear" "+")
int1
The bear chases the bear.
("bear" "chases" "bear" "+")
int2
The lion does not eat the bear.
False
5
inv-proof
[(((triple7 ((triple2 triple14) -> rule3)) -> rule2))]
("lion" "eats" "bear" "-")
((triple7 ((triple2 triple14) -> (rule3 % int2))) -> (rule2 % int1))
The lion eats the bear.
("lion" "eats" "bear" "+")
int1
The bear chases the bear.
("bear" "chases" "bear" "+")
int2
The mouse is not young.
Unknown
inv-rconc
[@2: The mouse is young.[CWA. Example of deepest failure = (rule7 <- rule3 <- FAIL)]]
("mouse" "is" "young" "-")
The bear visits the bear.
Unknown
rconc
[@2: The bear visits the bear.[CWA. Example of deepest failure = (rule5 <- rule1 <- FAIL)]]
("bear" "visits" "bear" "+")
The mouse does not visit the bear.
Unknown
inv-rconc
[@2: The mouse visits the bear.[CWA. Example of deepest failure = (rule5 <- rule1 <- FAIL)]]
("mouse" "visits" "bear" "-")
The bear is big.
Unknown
random
[@0: The bear is big.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "big" "+")
The lion does not chase the mouse.
Unknown
inv-random
[@0: The lion chases the mouse.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "mouse" "-")
The mouse visits the mouse.
Unknown
random
[@0: The mouse visits the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "visits" "mouse" "+")
@0: The bear chases the lion.[(triple1)] The bear chases the mouse.[(triple2)] The bear eats the lion.[(triple3)] The bear eats the mouse.[(triple4)] The bear is cold.[(triple5)] The bear is young.[(triple6 OR ((triple2) -> rule6))] The bear visits the lion.[(triple7)] The bear visits the mouse.[(triple8)] The lion chases the bear.[(triple9 OR ((triple3) -> rule4))] The lion is cold.[(triple10)] The lion visits the bear.[(triple11)] The lion visits the mouse.[(triple12)] The mouse eats the bear.[(triple13)] The mouse is big.[(triple14)] The mouse visits the lion.[(triple15)] @1: The bear chases the bear.[(((triple2 triple14) -> rule3))] The mouse chases the lion.[(((triple4) -> rule8))] @2: The lion eats the bear.[(((triple7 ((triple2 triple14) -> rule3)) -> rule2))]
The bear chases the lion.
("bear" "chases" "lion" "+")
triple1
The bear chases the mouse.
("bear" "chases" "mouse" "+")
triple2
The bear eats the lion.
("bear" "eats" "lion" "+")
triple3
The bear eats the mouse.
("bear" "eats" "mouse" "+")
triple4
The bear is cold.
("bear" "is" "cold" "+")
triple5
The bear is young.
("bear" "is" "young" "+")
triple6
((triple2) -> (rule6 % int1))
The bear is young.
("bear" "is" "young" "+")
int1
The bear visits the lion.
("bear" "visits" "lion" "+")
triple7
The bear visits the mouse.
("bear" "visits" "mouse" "+")
triple8
The lion chases the bear.
("lion" "chases" "bear" "+")
triple9
((triple3) -> (rule4 % int1))
The lion chases the bear.
("lion" "chases" "bear" "+")
int1
The lion is cold.
("lion" "is" "cold" "+")
triple10
The lion visits the bear.
("lion" "visits" "bear" "+")
triple11
The lion visits the mouse.
("lion" "visits" "mouse" "+")
triple12
The mouse eats the bear.
("mouse" "eats" "bear" "+")
triple13
The mouse is big.
("mouse" "is" "big" "+")
triple14
The mouse visits the lion.
("mouse" "visits" "lion" "+")
triple15
The bear chases the bear.
("bear" "chases" "bear" "+")
((triple2 triple14) -> (rule3 % int1))
The bear chases the bear.
("bear" "chases" "bear" "+")
int1
The mouse chases the lion.
("mouse" "chases" "lion" "+")
((triple4) -> (rule8 % int1))
The mouse chases the lion.
("mouse" "chases" "lion" "+")
int1
The lion eats the bear.
("lion" "eats" "bear" "+")
((triple7 ((triple2 triple14) -> (rule3 % int2))) -> (rule2 % int1))
The lion eats the bear.
("lion" "eats" "bear" "+")
int1
The bear chases the bear.
("bear" "chases" "bear" "+")
int2