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