The bear is round. The cow is round. The lion chases the cow. The mouse chases the lion. If someone chases the lion and they visit the lion then they chase the cow. If the bear visits the mouse then the mouse chases the cow. If the cow chases the bear then the bear visits the lion. If someone eats the bear then they are green. If someone is green then they visit the lion. If someone is round then they eat the bear.
The bear is round.
("bear" "is" "round" "+")
The cow is round.
("cow" "is" "round" "+")
The lion chases the cow.
("lion" "chases" "cow" "+")
The mouse chases the lion.
("mouse" "chases" "lion" "+")
If someone chases the lion and they visit the lion then they chase the cow.
((("someone" "chases" "lion" "+") ("someone" "visits" "lion" "+")) -> ("someone" "chases" "cow" "+"))
If the bear visits the mouse then the mouse chases the cow.
((("bear" "visits" "mouse" "+")) -> ("mouse" "chases" "cow" "+"))
If the cow chases the bear then the bear visits the lion.
((("cow" "chases" "bear" "+")) -> ("bear" "visits" "lion" "+"))
If someone eats the bear then they are green.
((("someone" "eats" "bear" "+")) -> ("someone" "is" "green" "+"))
If someone is green then they visit the lion.
((("someone" "is" "green" "+")) -> ("someone" "visits" "lion" "+"))
If someone is round then they eat the bear.
((("someone" "is" "round" "+")) -> ("someone" "eats" "bear" "+"))
The lion chases the cow.
True
1
proof
[(triple3)]
("lion" "chases" "cow" "+")
triple3
The mouse does not chase the lion.
False
1
inv-proof
[(triple4)]
("mouse" "chases" "lion" "-")
triple4
The bear eats the bear.
True
2
proof
[(((triple1) -> rule6))]
("bear" "eats" "bear" "+")
((triple1) -> (rule6 % int1))
The bear eats the bear.
("bear" "eats" "bear" "+")
int1
The bear does not eat the bear.
False
2
inv-proof
[(((triple1) -> rule6))]
("bear" "eats" "bear" "-")
((triple1) -> (rule6 % int1))
The bear eats the bear.
("bear" "eats" "bear" "+")
int1
The cow is green.
True
3
proof
[(((((triple2) -> rule6)) -> rule4))]
("cow" "is" "green" "+")
((((triple2) -> (rule6 % int2))) -> (rule4 % int1))
The cow is green.
("cow" "is" "green" "+")
int1
The cow eats the bear.
("cow" "eats" "bear" "+")
int2
The cow is not green.
False
3
inv-proof
[(((((triple2) -> rule6)) -> rule4))]
("cow" "is" "green" "-")
((((triple2) -> (rule6 % int2))) -> (rule4 % int1))
The cow is green.
("cow" "is" "green" "+")
int1
The cow eats the bear.
("cow" "eats" "bear" "+")
int2
The bear visits the lion.
True
4
proof
[(((((((triple1) -> rule6)) -> rule4)) -> rule5))]
("bear" "visits" "lion" "+")
((((((triple1) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
The bear visits the lion.
("bear" "visits" "lion" "+")
int1
The bear is green.
("bear" "is" "green" "+")
int2
The bear eats the bear.
("bear" "eats" "bear" "+")
int3
The cow does not visit the lion.
False
4
inv-proof
[(((((((triple2) -> rule6)) -> rule4)) -> rule5))]
("cow" "visits" "lion" "-")
((((((triple2) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
The cow visits the lion.
("cow" "visits" "lion" "+")
int1
The cow is green.
("cow" "is" "green" "+")
int2
The cow eats the bear.
("cow" "eats" "bear" "+")
int3
The mouse does not visit the lion.
Unknown
inv-rconc
[@3: The mouse visits the lion.[CWA. Example of deepest failure = (rule5 <- rule4 <- rule6 <- FAIL)]]
("mouse" "visits" "lion" "-")
The lion eats the bear.
Unknown
rconc
[@1: The lion eats the bear.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("lion" "eats" "bear" "+")
The lion does not visit the lion.
Unknown
inv-rconc
[@3: The lion visits the lion.[CWA. Example of deepest failure = (rule5 <- rule4 <- rule6 <- FAIL)]]
("lion" "visits" "lion" "-")
The mouse chases the cow.
Unknown
rconc
[@4: The mouse chases the cow.[CWA. Example of deepest failure = (rule1 <- rule5 <- rule4 <- rule6 <- FAIL)]]
("mouse" "chases" "cow" "+")
The lion does not chase the bear.
Unknown
inv-random
[@0: The lion chases the bear.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "bear" "-")
The lion chases the lion.
Unknown
random
[@0: The lion chases the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "lion" "+")
The lion does not eat the lion.
Unknown
inv-random
[@0: The lion eats the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "eats" "lion" "-")
The mouse visits the bear.
Unknown
random
[@0: The mouse visits the bear.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "visits" "bear" "+")
@0: The bear is round.[(triple1)] The cow is round.[(triple2)] The lion chases the cow.[(triple3)] The mouse chases the lion.[(triple4)] @1: The bear eats the bear.[(((triple1) -> rule6))] The cow eats the bear.[(((triple2) -> rule6))] @2: The bear is green.[(((((triple1) -> rule6)) -> rule4))] The cow is green.[(((((triple2) -> rule6)) -> rule4))] @3: The bear visits the lion.[(((((((triple1) -> rule6)) -> rule4)) -> rule5))] The cow visits the lion.[(((((((triple2) -> rule6)) -> rule4)) -> rule5))]
The bear is round.
("bear" "is" "round" "+")
triple1
The cow is round.
("cow" "is" "round" "+")
triple2
The lion chases the cow.
("lion" "chases" "cow" "+")
triple3
The mouse chases the lion.
("mouse" "chases" "lion" "+")
triple4
The bear eats the bear.
("bear" "eats" "bear" "+")
((triple1) -> (rule6 % int1))
The bear eats the bear.
("bear" "eats" "bear" "+")
int1
The cow eats the bear.
("cow" "eats" "bear" "+")
((triple2) -> (rule6 % int1))
The cow eats the bear.
("cow" "eats" "bear" "+")
int1
The bear is green.
("bear" "is" "green" "+")
((((triple1) -> (rule6 % int2))) -> (rule4 % int1))
The bear is green.
("bear" "is" "green" "+")
int1
The bear eats the bear.
("bear" "eats" "bear" "+")
int2
The cow is green.
("cow" "is" "green" "+")
((((triple2) -> (rule6 % int2))) -> (rule4 % int1))
The cow is green.
("cow" "is" "green" "+")
int1
The cow eats the bear.
("cow" "eats" "bear" "+")
int2
The bear visits the lion.
("bear" "visits" "lion" "+")
((((((triple1) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
The bear visits the lion.
("bear" "visits" "lion" "+")
int1
The bear is green.
("bear" "is" "green" "+")
int2
The bear eats the bear.
("bear" "eats" "bear" "+")
int3
The cow visits the lion.
("cow" "visits" "lion" "+")
((((((triple2) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
The cow visits the lion.
("cow" "visits" "lion" "+")
int1
The cow is green.
("cow" "is" "green" "+")
int2
The cow eats the bear.
("cow" "eats" "bear" "+")
int3