The cow is round. The dog chases the cow. The lion chases the dog. The lion eats the cow. The lion is round. The mouse eats the dog. The mouse is round. If someone eats the mouse then the mouse chases the dog. If someone is round and kind then they chase the mouse. If someone is rough then they eat the mouse. If the cow chases the dog and the dog eats the cow then the dog is nice. If the mouse is round and the mouse eats the cow then the mouse sees the dog. If someone chases the dog then they are rough. If someone is red then they see the mouse. If someone eats the dog then they chase the lion. If the mouse eats the dog and the dog chases the cow then the dog sees the mouse.
The cow is round.
("cow" "is" "round" "+")
The dog chases the cow.
("dog" "chases" "cow" "+")
The lion chases the dog.
("lion" "chases" "dog" "+")
The lion eats the cow.
("lion" "eats" "cow" "+")
The lion is round.
("lion" "is" "round" "+")
The mouse eats the dog.
("mouse" "eats" "dog" "+")
The mouse is round.
("mouse" "is" "round" "+")
If someone eats the mouse then the mouse chases the dog.
((("someone" "eats" "mouse" "+")) -> ("mouse" "chases" "dog" "+"))
If someone is round and kind then they chase the mouse.
((("someone" "is" "round" "+") ("someone" "is" "kind" "+")) -> ("someone" "chases" "mouse" "+"))
If someone is rough then they eat the mouse.
((("someone" "is" "rough" "+")) -> ("someone" "eats" "mouse" "+"))
If the cow chases the dog and the dog eats the cow then the dog is nice.
((("cow" "chases" "dog" "+") ("dog" "eats" "cow" "+")) -> ("dog" "is" "nice" "+"))
If the mouse is round and the mouse eats the cow then the mouse sees the dog.
((("mouse" "is" "round" "+") ("mouse" "eats" "cow" "+")) -> ("mouse" "sees" "dog" "+"))
If someone chases the dog then they are rough.
((("someone" "chases" "dog" "+")) -> ("someone" "is" "rough" "+"))
If someone is red then they see the mouse.
((("someone" "is" "red" "+")) -> ("someone" "sees" "mouse" "+"))
If someone eats the dog then they chase the lion.
((("someone" "eats" "dog" "+")) -> ("someone" "chases" "lion" "+"))
If the mouse eats the dog and the dog chases the cow then the dog sees the mouse.
((("mouse" "eats" "dog" "+") ("dog" "chases" "cow" "+")) -> ("dog" "sees" "mouse" "+"))
The dog chases the cow.
True
1
proof
[(triple2)]
("dog" "chases" "cow" "+")
triple2
The lion does not chase the dog.
False
1
inv-proof
[(triple3)]
("lion" "chases" "dog" "-")
triple3
The mouse chases the lion.
True
2
proof
[(((triple6) -> rule8))]
("mouse" "chases" "lion" "+")
((triple6) -> (rule8 % int1))
The mouse chases the lion.
("mouse" "chases" "lion" "+")
int1
The mouse does not chase the lion.
False
2
inv-proof
[(((triple6) -> rule8))]
("mouse" "chases" "lion" "-")
((triple6) -> (rule8 % int1))
The mouse chases the lion.
("mouse" "chases" "lion" "+")
int1
The lion eats the mouse.
True
3
proof
[(((((triple3) -> rule6)) -> rule3))]
("lion" "eats" "mouse" "+")
((((triple3) -> (rule6 % int2))) -> (rule3 % int1))
The lion eats the mouse.
("lion" "eats" "mouse" "+")
int1
The lion is rough.
("lion" "is" "rough" "+")
int2
The lion does not eat the mouse.
False
3
inv-proof
[(((((triple3) -> rule6)) -> rule3))]
("lion" "eats" "mouse" "-")
((((triple3) -> (rule6 % int2))) -> (rule3 % int1))
The lion eats the mouse.
("lion" "eats" "mouse" "+")
int1
The lion is rough.
("lion" "is" "rough" "+")
int2
The mouse chases the dog.
True
4
proof
[(((((((triple3) -> rule6)) -> rule3)) -> rule1))]
("mouse" "chases" "dog" "+")
((((((triple3) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The mouse chases the dog.
("mouse" "chases" "dog" "+")
int1
The lion eats the mouse.
("lion" "eats" "mouse" "+")
int2
The lion is rough.
("lion" "is" "rough" "+")
int3
The mouse does not chase the dog.
False
4
inv-proof
[(((((((triple3) -> rule6)) -> rule3)) -> rule1))]
("mouse" "chases" "dog" "-")
((((((triple3) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The mouse chases the dog.
("mouse" "chases" "dog" "+")
int1
The lion eats the mouse.
("lion" "eats" "mouse" "+")
int2
The lion is rough.
("lion" "is" "rough" "+")
int3
The mouse is rough.
True
5
proof
[(((((((((triple3) -> rule6)) -> rule3)) -> rule1)) -> rule6))]
("mouse" "is" "rough" "+")
((((((((triple3) -> (rule6 % int4))) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
The mouse chases the dog.
("mouse" "chases" "dog" "+")
int2
The lion eats the mouse.
("lion" "eats" "mouse" "+")
int3
The lion is rough.
("lion" "is" "rough" "+")
int4
The mouse is not rough.
False
5
inv-proof
[(((((((((triple3) -> rule6)) -> rule3)) -> rule1)) -> rule6))]
("mouse" "is" "rough" "-")
((((((((triple3) -> (rule6 % int4))) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
The mouse chases the dog.
("mouse" "chases" "dog" "+")
int2
The lion eats the mouse.
("lion" "eats" "mouse" "+")
int3
The lion is rough.
("lion" "is" "rough" "+")
int4
The mouse eats the mouse.
True
6
proof
[(((((((((((triple3) -> rule6)) -> rule3)) -> rule1)) -> rule6)) -> rule3))]
("mouse" "eats" "mouse" "+")
((((((((((triple3) -> (rule6 % int5))) -> (rule3 % int4))) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
The mouse eats the mouse.
("mouse" "eats" "mouse" "+")
int1
The mouse is rough.
("mouse" "is" "rough" "+")
int2
The mouse chases the dog.
("mouse" "chases" "dog" "+")
int3
The lion eats the mouse.
("lion" "eats" "mouse" "+")
int4
The lion is rough.
("lion" "is" "rough" "+")
int5
The mouse does not eat the mouse.
False
6
inv-proof
[(((((((((((triple3) -> rule6)) -> rule3)) -> rule1)) -> rule6)) -> rule3))]
("mouse" "eats" "mouse" "-")
((((((((((triple3) -> (rule6 % int5))) -> (rule3 % int4))) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
The mouse eats the mouse.
("mouse" "eats" "mouse" "+")
int1
The mouse is rough.
("mouse" "is" "rough" "+")
int2
The mouse chases the dog.
("mouse" "chases" "dog" "+")
int3
The lion eats the mouse.
("lion" "eats" "mouse" "+")
int4
The lion is rough.
("lion" "is" "rough" "+")
int5
The dog does not eat the mouse.
Unknown
inv-rconc
[@2: The dog eats the mouse.[CWA. Example of deepest failure = (rule3 <- rule6 <- FAIL)]]
("dog" "eats" "mouse" "-")
The lion sees the mouse.
Unknown
rconc
[@1: The lion sees the mouse.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("lion" "sees" "mouse" "+")
The dog is not rough.
Unknown
inv-rconc
[@1: The dog is rough.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("dog" "is" "rough" "-")
The mouse sees the mouse.
Unknown
rconc
[@1: The mouse sees the mouse.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("mouse" "sees" "mouse" "+")
The cow is not rough.
Unknown
inv-rconc
[@1: The cow is rough.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("cow" "is" "rough" "-")
The dog chases the mouse.
Unknown
rconc
[@1: The dog chases the mouse.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("dog" "chases" "mouse" "+")
The mouse does not see the lion.
Unknown
inv-random
[@0: The mouse sees the lion.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "sees" "lion" "-")
The cow sees the lion.
Unknown
random
[@0: The cow sees the lion.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "lion" "+")
The cow does not chase the cow.
Unknown
inv-random
[@0: The cow chases the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "chases" "cow" "-")
The dog eats the lion.
Unknown
random
[@0: The dog eats the lion.[CWA. Example of deepest failure = (FAIL)]]
("dog" "eats" "lion" "+")
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 dog is red.
Unknown
random
[@0: The dog is red.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "red" "+")
@0: The cow is round.[(triple1)] The dog chases the cow.[(triple2)] The lion chases the dog.[(triple3)] The lion eats the cow.[(triple4)] The lion is round.[(triple5)] The mouse eats the dog.[(triple6)] The mouse is round.[(triple7)] @1: The dog sees the mouse.[(((triple6 triple2) -> rule9))] The lion is rough.[(((triple3) -> rule6))] The mouse chases the lion.[(((triple6) -> rule8))] @2: The lion eats the mouse.[(((((triple3) -> rule6)) -> rule3))] @3: The mouse chases the dog.[(((((((triple3) -> rule6)) -> rule3)) -> rule1))] @4: The mouse is rough.[(((((((((triple3) -> rule6)) -> rule3)) -> rule1)) -> rule6))] @5: The mouse eats the mouse.[(((((((((((triple3) -> rule6)) -> rule3)) -> rule1)) -> rule6)) -> rule3))]
The cow is round.
("cow" "is" "round" "+")
triple1
The dog chases the cow.
("dog" "chases" "cow" "+")
triple2
The lion chases the dog.
("lion" "chases" "dog" "+")
triple3
The lion eats the cow.
("lion" "eats" "cow" "+")
triple4
The lion is round.
("lion" "is" "round" "+")
triple5
The mouse eats the dog.
("mouse" "eats" "dog" "+")
triple6
The mouse is round.
("mouse" "is" "round" "+")
triple7
The dog sees the mouse.
("dog" "sees" "mouse" "+")
((triple6 triple2) -> (rule9 % int1))
The dog sees the mouse.
("dog" "sees" "mouse" "+")
int1
The lion is rough.
("lion" "is" "rough" "+")
((triple3) -> (rule6 % int1))
The lion is rough.
("lion" "is" "rough" "+")
int1
The mouse chases the lion.
("mouse" "chases" "lion" "+")
((triple6) -> (rule8 % int1))
The mouse chases the lion.
("mouse" "chases" "lion" "+")
int1
The lion eats the mouse.
("lion" "eats" "mouse" "+")
((((triple3) -> (rule6 % int2))) -> (rule3 % int1))
The lion eats the mouse.
("lion" "eats" "mouse" "+")
int1
The lion is rough.
("lion" "is" "rough" "+")
int2
The mouse chases the dog.
("mouse" "chases" "dog" "+")
((((((triple3) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The mouse chases the dog.
("mouse" "chases" "dog" "+")
int1
The lion eats the mouse.
("lion" "eats" "mouse" "+")
int2
The lion is rough.
("lion" "is" "rough" "+")
int3
The mouse is rough.
("mouse" "is" "rough" "+")
((((((((triple3) -> (rule6 % int4))) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
The mouse chases the dog.
("mouse" "chases" "dog" "+")
int2
The lion eats the mouse.
("lion" "eats" "mouse" "+")
int3
The lion is rough.
("lion" "is" "rough" "+")
int4
The mouse eats the mouse.
("mouse" "eats" "mouse" "+")
((((((((((triple3) -> (rule6 % int5))) -> (rule3 % int4))) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
The mouse eats the mouse.
("mouse" "eats" "mouse" "+")
int1
The mouse is rough.
("mouse" "is" "rough" "+")
int2
The mouse chases the dog.
("mouse" "chases" "dog" "+")
int3
The lion eats the mouse.
("lion" "eats" "mouse" "+")
int4
The lion is rough.
("lion" "is" "rough" "+")
int5