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