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