The bear chases the cow. The bear is round. The bear sees the mouse. The bear visits the dog. The cow is young. The cow does not visit the mouse. The dog is round. The dog sees the bear. The dog sees the cow. The dog does not visit the cow. The mouse is young. The mouse does not visit the bear. If something visits the cow and the cow does not visit the bear then it chases the bear. If something visits the dog then the dog sees the cow. If something chases the dog and it chases the cow then it sees the bear. If something is red then it sees the bear. If something chases the dog then it chases the cow. If something sees the cow then the cow chases the dog. If the dog is nice then the dog visits the mouse. If something is big and it sees the mouse then it is red.
The bear chases the cow.
("bear" "chases" "cow" "+")
The bear is round.
("bear" "is" "round" "+")
The bear sees the mouse.
("bear" "sees" "mouse" "+")
The bear visits the dog.
("bear" "visits" "dog" "+")
The cow is young.
("cow" "is" "young" "+")
The cow does not visit the mouse.
("cow" "visits" "mouse" "-")
The dog is round.
("dog" "is" "round" "+")
The dog sees the bear.
("dog" "sees" "bear" "+")
The dog sees the cow.
("dog" "sees" "cow" "+")
The dog does not visit the cow.
("dog" "visits" "cow" "-")
The mouse is young.
("mouse" "is" "young" "+")
The mouse does not visit the bear.
("mouse" "visits" "bear" "-")
If something visits the cow and the cow does not visit the bear then it chases the bear.
((("something" "visits" "cow" "+") ("cow" "visits" "bear" "~")) -> ("something" "chases" "bear" "+"))
If something visits the dog then the dog sees the cow.
((("something" "visits" "dog" "+")) -> ("dog" "sees" "cow" "+"))
If something chases the dog and it chases the cow then it sees the bear.
((("something" "chases" "dog" "+") ("something" "chases" "cow" "+")) -> ("something" "sees" "bear" "+"))
If something is red then it sees the bear.
((("something" "is" "red" "+")) -> ("something" "sees" "bear" "+"))
If something chases the dog then it chases the cow.
((("something" "chases" "dog" "+")) -> ("something" "chases" "cow" "+"))
If something sees the cow then the cow chases the dog.
((("something" "sees" "cow" "+")) -> ("cow" "chases" "dog" "+"))
If the dog is nice then the dog visits the mouse.
((("dog" "is" "nice" "+")) -> ("dog" "visits" "mouse" "+"))
If something is big and it sees the mouse then it is red.
((("something" "is" "big" "+") ("something" "sees" "mouse" "+")) -> ("something" "is" "red" "+"))
The dog is round.
True
1
proof
[(triple7)]
("dog" "is" "round" "+")
triple7
The bear does not visit the dog.
False
1
inv-proof
[(triple4)]
("bear" "visits" "dog" "-")
triple4
The cow chases the dog.
True
2
proof
[(((triple9) -> rule6) OR ((((triple4) -> rule2)) -> rule6))]
("cow" "chases" "dog" "+")
((triple9) -> (rule6 % int1))
The cow chases the dog.
("cow" "chases" "dog" "+")
int1
((((triple4) -> (rule2 % int2))) -> (rule6 % int1))
The cow chases the dog.
("cow" "chases" "dog" "+")
int1
The dog sees the cow.
("dog" "sees" "cow" "+")
int2
The cow does not chase the dog.
False
2
inv-proof
[(((triple9) -> rule6) OR ((((triple4) -> rule2)) -> rule6))]
("cow" "chases" "dog" "-")
((triple9) -> (rule6 % int1))
The cow chases the dog.
("cow" "chases" "dog" "+")
int1
((((triple4) -> (rule2 % int2))) -> (rule6 % int1))
The cow chases the dog.
("cow" "chases" "dog" "+")
int1
The dog sees the cow.
("dog" "sees" "cow" "+")
int2
The cow chases the cow.
True
3
proof
[(((((triple9) -> rule6)) -> rule5) OR ((((((triple4) -> rule2)) -> rule6)) -> rule5))]
("cow" "chases" "cow" "+")
((((triple9) -> (rule6 % int2))) -> (rule5 % int1))
The cow chases the cow.
("cow" "chases" "cow" "+")
int1
The cow chases the dog.
("cow" "chases" "dog" "+")
int2
((((((triple4) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The cow chases the cow.
("cow" "chases" "cow" "+")
int1
The cow chases the dog.
("cow" "chases" "dog" "+")
int2
The dog sees the cow.
("dog" "sees" "cow" "+")
int3
The cow does not chase the cow.
False
3
inv-proof
[(((((triple9) -> rule6)) -> rule5) OR ((((((triple4) -> rule2)) -> rule6)) -> rule5))]
("cow" "chases" "cow" "-")
((((triple9) -> (rule6 % int2))) -> (rule5 % int1))
The cow chases the cow.
("cow" "chases" "cow" "+")
int1
The cow chases the dog.
("cow" "chases" "dog" "+")
int2
((((((triple4) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The cow chases the cow.
("cow" "chases" "cow" "+")
int1
The cow chases the dog.
("cow" "chases" "dog" "+")
int2
The dog sees the cow.
("dog" "sees" "cow" "+")
int3
The cow sees the bear.
True
6
proof
[(((((triple9) -> rule6) ((((triple9) -> rule6)) -> rule5)) -> rule3) OR ((((((triple4) -> rule2)) -> rule6) ((((triple9) -> rule6)) -> rule5)) -> rule3) OR ((((triple9) -> rule6) ((((((triple4) -> rule2)) -> rule6)) -> rule5)) -> rule3) OR ((((((triple4) -> rule2)) -> rule6) ((((((triple4) -> rule2)) -> rule6)) -> rule5)) -> rule3))]
("cow" "sees" "bear" "+")
((((triple9) -> (rule6 % int3)) ((((triple9) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
The cow sees the bear.
("cow" "sees" "bear" "+")
int1
The cow chases the cow.
("cow" "chases" "cow" "+")
int2
The cow chases the dog.
("cow" "chases" "dog" "+")
int3
((((((triple4) -> (rule2 % int4))) -> (rule6 % int3)) ((((triple9) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
The cow sees the bear.
("cow" "sees" "bear" "+")
int1
The cow chases the cow.
("cow" "chases" "cow" "+")
int2
The cow chases the dog.
("cow" "chases" "dog" "+")
int3
The dog sees the cow.
("dog" "sees" "cow" "+")
int4
((((triple9) -> (rule6 % int4)) ((((((triple4) -> (rule2 % int3))) -> (rule6 % int4))) -> (rule5 % int2))) -> (rule3 % int1))
The cow sees the bear.
("cow" "sees" "bear" "+")
int1
The cow chases the cow.
("cow" "chases" "cow" "+")
int2
The dog sees the cow.
("dog" "sees" "cow" "+")
int3
The cow chases the dog.
("cow" "chases" "dog" "+")
int4
((((((triple4) -> (rule2 % int4))) -> (rule6 % int3)) ((((((triple4) -> (rule2 % int4))) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
The cow sees the bear.
("cow" "sees" "bear" "+")
int1
The cow chases the cow.
("cow" "chases" "cow" "+")
int2
The cow chases the dog.
("cow" "chases" "dog" "+")
int3
The dog sees the cow.
("dog" "sees" "cow" "+")
int4
The cow does not see the bear.
False
6
inv-proof
[(((((triple9) -> rule6) ((((triple9) -> rule6)) -> rule5)) -> rule3) OR ((((((triple4) -> rule2)) -> rule6) ((((triple9) -> rule6)) -> rule5)) -> rule3) OR ((((triple9) -> rule6) ((((((triple4) -> rule2)) -> rule6)) -> rule5)) -> rule3) OR ((((((triple4) -> rule2)) -> rule6) ((((((triple4) -> rule2)) -> rule6)) -> rule5)) -> rule3))]
("cow" "sees" "bear" "-")
((((triple9) -> (rule6 % int3)) ((((triple9) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
The cow sees the bear.
("cow" "sees" "bear" "+")
int1
The cow chases the cow.
("cow" "chases" "cow" "+")
int2
The cow chases the dog.
("cow" "chases" "dog" "+")
int3
((((((triple4) -> (rule2 % int4))) -> (rule6 % int3)) ((((triple9) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
The cow sees the bear.
("cow" "sees" "bear" "+")
int1
The cow chases the cow.
("cow" "chases" "cow" "+")
int2
The cow chases the dog.
("cow" "chases" "dog" "+")
int3
The dog sees the cow.
("dog" "sees" "cow" "+")
int4
((((triple9) -> (rule6 % int4)) ((((((triple4) -> (rule2 % int3))) -> (rule6 % int4))) -> (rule5 % int2))) -> (rule3 % int1))
The cow sees the bear.
("cow" "sees" "bear" "+")
int1
The cow chases the cow.
("cow" "chases" "cow" "+")
int2
The dog sees the cow.
("dog" "sees" "cow" "+")
int3
The cow chases the dog.
("cow" "chases" "dog" "+")
int4
((((((triple4) -> (rule2 % int4))) -> (rule6 % int3)) ((((((triple4) -> (rule2 % int4))) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
The cow sees the bear.
("cow" "sees" "bear" "+")
int1
The cow chases the cow.
("cow" "chases" "cow" "+")
int2
The cow chases the dog.
("cow" "chases" "dog" "+")
int3
The dog sees the cow.
("dog" "sees" "cow" "+")
int4
The dog does not chase the bear.
Unknown
inv-rconc
[@1: The dog chases the bear.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("dog" "chases" "bear" "-")
The dog is red.
Unknown
rconc
[@1: The dog is red.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("dog" "is" "red" "+")
The mouse does not chase the cow.
Unknown
inv-rconc
[@1: The mouse chases the cow.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("mouse" "chases" "cow" "-")
The bear is red.
Unknown
rconc
[@1: The bear is red.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("bear" "is" "red" "+")
The bear does not visit the bear.
Unknown
inv-random
[@0: The bear visits the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "visits" "bear" "-")
The mouse is round.
Unknown
random
[@0: The mouse is round.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "round" "+")
The dog does not visit the bear.
Unknown
inv-random
[@0: The dog visits the bear.[CWA. Example of deepest failure = (FAIL)]]
("dog" "visits" "bear" "-")
The bear chases the dog.
Unknown
random
[@0: The bear chases the dog.[CWA. Example of deepest failure = (FAIL)]]
("bear" "chases" "dog" "+")
@0: The bear chases the cow.[(triple1)] The bear is round.[(triple2)] The bear sees the mouse.[(triple3)] The bear visits the dog.[(triple4)] The cow does not visit the mouse.[(triple6)] The cow is young.[(triple5)] The dog does not visit the cow.[(triple10)] The dog is round.[(triple7)] The dog sees the bear.[(triple8)] The dog sees the cow.[(triple9 OR ((triple4) -> rule2))] The mouse does not visit the bear.[(triple12)] The mouse is young.[(triple11)] @1: The cow chases the dog.[(((triple9) -> rule6) OR ((((triple4) -> rule2)) -> rule6))] @2: The cow chases the cow.[(((((triple9) -> rule6)) -> rule5) OR ((((((triple4) -> rule2)) -> rule6)) -> rule5))] @3: The cow sees the bear.[(((((triple9) -> rule6) ((((triple9) -> rule6)) -> rule5)) -> rule3) OR ((((((triple4) -> rule2)) -> rule6) ((((triple9) -> rule6)) -> rule5)) -> rule3) OR ((((triple9) -> rule6) ((((((triple4) -> rule2)) -> rule6)) -> rule5)) -> rule3) OR ((((((triple4) -> rule2)) -> rule6) ((((((triple4) -> rule2)) -> rule6)) -> rule5)) -> rule3))]
The bear chases the cow.
("bear" "chases" "cow" "+")
triple1
The bear is round.
("bear" "is" "round" "+")
triple2
The bear sees the mouse.
("bear" "sees" "mouse" "+")
triple3
The bear visits the dog.
("bear" "visits" "dog" "+")
triple4
The cow does not visit the mouse.
("cow" "visits" "mouse" "-")
triple6
The cow is young.
("cow" "is" "young" "+")
triple5
The dog does not visit the cow.
("dog" "visits" "cow" "-")
triple10
The dog is round.
("dog" "is" "round" "+")
triple7
The dog sees the bear.
("dog" "sees" "bear" "+")
triple8
The dog sees the cow.
("dog" "sees" "cow" "+")
triple9
((triple4) -> (rule2 % int1))
The dog sees the cow.
("dog" "sees" "cow" "+")
int1
The mouse does not visit the bear.
("mouse" "visits" "bear" "-")
triple12
The mouse is young.
("mouse" "is" "young" "+")
triple11
The cow chases the dog.
("cow" "chases" "dog" "+")
((triple9) -> (rule6 % int1))
The cow chases the dog.
("cow" "chases" "dog" "+")
int1
((((triple4) -> (rule2 % int2))) -> (rule6 % int1))
The cow chases the dog.
("cow" "chases" "dog" "+")
int1
The dog sees the cow.
("dog" "sees" "cow" "+")
int2
The cow chases the cow.
("cow" "chases" "cow" "+")
((((triple9) -> (rule6 % int2))) -> (rule5 % int1))
The cow chases the cow.
("cow" "chases" "cow" "+")
int1
The cow chases the dog.
("cow" "chases" "dog" "+")
int2
((((((triple4) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The cow chases the cow.
("cow" "chases" "cow" "+")
int1
The cow chases the dog.
("cow" "chases" "dog" "+")
int2
The dog sees the cow.
("dog" "sees" "cow" "+")
int3
The cow sees the bear.
("cow" "sees" "bear" "+")
((((triple9) -> (rule6 % int3)) ((((triple9) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
The cow sees the bear.
("cow" "sees" "bear" "+")
int1
The cow chases the cow.
("cow" "chases" "cow" "+")
int2
The cow chases the dog.
("cow" "chases" "dog" "+")
int3
((((((triple4) -> (rule2 % int4))) -> (rule6 % int3)) ((((triple9) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
The cow sees the bear.
("cow" "sees" "bear" "+")
int1
The cow chases the cow.
("cow" "chases" "cow" "+")
int2
The cow chases the dog.
("cow" "chases" "dog" "+")
int3
The dog sees the cow.
("dog" "sees" "cow" "+")
int4
((((triple9) -> (rule6 % int4)) ((((((triple4) -> (rule2 % int3))) -> (rule6 % int4))) -> (rule5 % int2))) -> (rule3 % int1))
The cow sees the bear.
("cow" "sees" "bear" "+")
int1
The cow chases the cow.
("cow" "chases" "cow" "+")
int2
The dog sees the cow.
("dog" "sees" "cow" "+")
int3
The cow chases the dog.
("cow" "chases" "dog" "+")
int4
((((((triple4) -> (rule2 % int4))) -> (rule6 % int3)) ((((((triple4) -> (rule2 % int4))) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
The cow sees the bear.
("cow" "sees" "bear" "+")
int1
The cow chases the cow.
("cow" "chases" "cow" "+")
int2
The cow chases the dog.
("cow" "chases" "dog" "+")
int3
The dog sees the cow.
("dog" "sees" "cow" "+")
int4