The bear chases the cow. The bear is blue. The bear is round. The bear does not visit the cow. The bear visits the mouse. The cow is blue. The cow is kind. The cow is young. The lion is nice. The lion is not young. The lion sees the cow. The lion does not see the mouse. The lion visits the cow. The lion visits the mouse. The mouse does not visit the bear. If something sees the lion and the lion does not see the mouse then the mouse does not visit the lion. If something chases the mouse then it visits the mouse. If something sees the cow then the cow does not see the lion. If something sees the bear then the bear sees the cow. If something is young then it chases the mouse. If something is kind and it visits the bear then it is young.
The bear chases the cow.
("bear" "chases" "cow" "+")
The bear is blue.
("bear" "is" "blue" "+")
The bear is round.
("bear" "is" "round" "+")
The bear does not visit the cow.
("bear" "visits" "cow" "-")
The bear visits the mouse.
("bear" "visits" "mouse" "+")
The cow is blue.
("cow" "is" "blue" "+")
The cow is kind.
("cow" "is" "kind" "+")
The cow is young.
("cow" "is" "young" "+")
The lion is nice.
("lion" "is" "nice" "+")
The lion is not young.
("lion" "is" "young" "-")
The lion sees the cow.
("lion" "sees" "cow" "+")
The lion does not see the mouse.
("lion" "sees" "mouse" "-")
The lion visits the cow.
("lion" "visits" "cow" "+")
The lion visits the mouse.
("lion" "visits" "mouse" "+")
The mouse does not visit the bear.
("mouse" "visits" "bear" "-")
If something sees the lion and the lion does not see the mouse then the mouse does not visit the lion.
((("something" "sees" "lion" "+") ("lion" "sees" "mouse" "~")) -> ("mouse" "visits" "lion" "-"))
If something chases the mouse then it visits the mouse.
((("something" "chases" "mouse" "+")) -> ("something" "visits" "mouse" "+"))
If something sees the cow then the cow does not see the lion.
((("something" "sees" "cow" "+")) -> ("cow" "sees" "lion" "-"))
If something sees the bear then the bear sees the cow.
((("something" "sees" "bear" "+")) -> ("bear" "sees" "cow" "+"))
If something is young then it chases the mouse.
((("something" "is" "young" "+")) -> ("something" "chases" "mouse" "+"))
If something is kind and it visits the bear then it is young.
((("something" "is" "kind" "+") ("something" "visits" "bear" "+")) -> ("something" "is" "young" "+"))
The mouse does not visit the bear.
True
1
proof
[(triple15)]
("mouse" "visits" "bear" "-")
triple15
The bear is not round.
False
1
inv-proof
[(triple3)]
("bear" "is" "round" "-")
triple3
The cow chases the mouse.
True
2
proof
[(((triple8) -> rule5))]
("cow" "chases" "mouse" "+")
((triple8) -> (rule5 % int1))
The cow chases the mouse.
("cow" "chases" "mouse" "+")
int1
The cow sees the lion.
False
2
inv-proof
[(((triple11) -> rule3))]
("cow" "sees" "lion" "+")
((triple11) -> (rule3 % int1))
The cow does not see the lion.
("cow" "sees" "lion" "-")
int1
The cow visits the mouse.
True
3
proof
[(((((triple8) -> rule5)) -> rule2))]
("cow" "visits" "mouse" "+")
((((triple8) -> (rule5 % int2))) -> (rule2 % int1))
The cow visits the mouse.
("cow" "visits" "mouse" "+")
int1
The cow chases the mouse.
("cow" "chases" "mouse" "+")
int2
The cow does not visit the mouse.
False
3
inv-proof
[(((((triple8) -> rule5)) -> rule2))]
("cow" "visits" "mouse" "-")
((((triple8) -> (rule5 % int2))) -> (rule2 % int1))
The cow visits the mouse.
("cow" "visits" "mouse" "+")
int1
The cow chases the mouse.
("cow" "chases" "mouse" "+")
int2
The mouse does not visit the mouse.
Unknown
inv-rconc
[@3: The mouse visits the mouse.[CWA. Example of deepest failure = (rule2 <- rule5 <- rule6 <- FAIL)]]
("mouse" "visits" "mouse" "-")
The mouse chases the mouse.
Unknown
rconc
[@2: The mouse chases the mouse.[CWA. Example of deepest failure = (rule5 <- rule6 <- FAIL)]]
("mouse" "chases" "mouse" "+")
The bear is not young.
Unknown
inv-rconc
[@1: The bear is young.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("bear" "is" "young" "-")
The mouse is kind.
Unknown
random
[@0: The mouse is kind.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "kind" "+")
The lion does not chase the cow.
Unknown
inv-random
[@0: The lion chases the cow.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "cow" "-")
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 cow.[(triple1)] The bear does not visit the cow.[(triple4)] The bear is blue.[(triple2)] The bear is round.[(triple3)] The bear visits the mouse.[(triple5)] The cow is blue.[(triple6)] The cow is kind.[(triple7)] The cow is young.[(triple8)] The lion does not see the mouse.[(triple12)] The lion is nice.[(triple9)] The lion is not young.[(triple10)] The lion sees the cow.[(triple11)] The lion visits the cow.[(triple13)] The lion visits the mouse.[(triple14)] The mouse does not visit the bear.[(triple15)] @1: The cow chases the mouse.[(((triple8) -> rule5))] The cow does not see the lion.[(((triple11) -> rule3))] @2: The cow visits the mouse.[(((((triple8) -> rule5)) -> rule2))]
The bear chases the cow.
("bear" "chases" "cow" "+")
triple1
The bear does not visit the cow.
("bear" "visits" "cow" "-")
triple4
The bear is blue.
("bear" "is" "blue" "+")
triple2
The bear is round.
("bear" "is" "round" "+")
triple3
The bear visits the mouse.
("bear" "visits" "mouse" "+")
triple5
The cow is blue.
("cow" "is" "blue" "+")
triple6
The cow is kind.
("cow" "is" "kind" "+")
triple7
The cow is young.
("cow" "is" "young" "+")
triple8
The lion does not see the mouse.
("lion" "sees" "mouse" "-")
triple12
The lion is nice.
("lion" "is" "nice" "+")
triple9
The lion is not young.
("lion" "is" "young" "-")
triple10
The lion sees the cow.
("lion" "sees" "cow" "+")
triple11
The lion visits the cow.
("lion" "visits" "cow" "+")
triple13
The lion visits the mouse.
("lion" "visits" "mouse" "+")
triple14
The mouse does not visit the bear.
("mouse" "visits" "bear" "-")
triple15
The cow chases the mouse.
("cow" "chases" "mouse" "+")
((triple8) -> (rule5 % int1))
The cow chases the mouse.
("cow" "chases" "mouse" "+")
int1
The cow does not see the lion.
("cow" "sees" "lion" "-")
((triple11) -> (rule3 % int1))
The cow does not see the lion.
("cow" "sees" "lion" "-")
int1
The cow visits the mouse.
("cow" "visits" "mouse" "+")
((((triple8) -> (rule5 % int2))) -> (rule2 % int1))
The cow visits the mouse.
("cow" "visits" "mouse" "+")
int1
The cow chases the mouse.
("cow" "chases" "mouse" "+")
int2