The cow is rough. The cow is round. The cow needs the tiger. The cow sees the tiger. The dog is green. The dog is young. The tiger chases the cow. The tiger is green. The tiger is rough. The tiger needs the dog. If someone is kind then they see the dog. If someone sees the dog then they need the tiger. If someone sees the dog and they chase the dog then the dog chases the cow. If someone is green then they are kind. If someone sees the tiger and the tiger chases the cow then the cow is young. If someone is round then they need the tiger.
The cow is rough.
("cow" "is" "rough" "+")
The cow is round.
("cow" "is" "round" "+")
The cow needs the tiger.
("cow" "needs" "tiger" "+")
The cow sees the tiger.
("cow" "sees" "tiger" "+")
The dog is green.
("dog" "is" "green" "+")
The dog is young.
("dog" "is" "young" "+")
The tiger chases the cow.
("tiger" "chases" "cow" "+")
The tiger is green.
("tiger" "is" "green" "+")
The tiger is rough.
("tiger" "is" "rough" "+")
The tiger needs the dog.
("tiger" "needs" "dog" "+")
If someone is kind then they see the dog.
((("someone" "is" "kind" "+")) -> ("someone" "sees" "dog" "+"))
If someone sees the dog then they need the tiger.
((("someone" "sees" "dog" "+")) -> ("someone" "needs" "tiger" "+"))
If someone sees the dog and they chase the dog then the dog chases the cow.
((("someone" "sees" "dog" "+") ("someone" "chases" "dog" "+")) -> ("dog" "chases" "cow" "+"))
If someone is green then they are kind.
((("someone" "is" "green" "+")) -> ("someone" "is" "kind" "+"))
If someone sees the tiger and the tiger chases the cow then the cow is young.
((("someone" "sees" "tiger" "+") ("tiger" "chases" "cow" "+")) -> ("cow" "is" "young" "+"))
If someone is round then they need the tiger.
((("someone" "is" "round" "+")) -> ("someone" "needs" "tiger" "+"))
The dog is green.
True
1
proof
[(triple5)]
("dog" "is" "green" "+")
triple5
The tiger does not chase the cow.
False
1
inv-proof
[(triple7)]
("tiger" "chases" "cow" "-")
triple7
The dog is kind.
True
2
proof
[(((triple5) -> rule4))]
("dog" "is" "kind" "+")
((triple5) -> (rule4 % int1))
The dog is kind.
("dog" "is" "kind" "+")
int1
The dog is not kind.
False
2
inv-proof
[(((triple5) -> rule4))]
("dog" "is" "kind" "-")
((triple5) -> (rule4 % int1))
The dog is kind.
("dog" "is" "kind" "+")
int1
The tiger sees the dog.
True
3
proof
[(((((triple8) -> rule4)) -> rule1))]
("tiger" "sees" "dog" "+")
((((triple8) -> (rule4 % int2))) -> (rule1 % int1))
The tiger sees the dog.
("tiger" "sees" "dog" "+")
int1
The tiger is kind.
("tiger" "is" "kind" "+")
int2
The tiger does not see the dog.
False
3
inv-proof
[(((((triple8) -> rule4)) -> rule1))]
("tiger" "sees" "dog" "-")
((((triple8) -> (rule4 % int2))) -> (rule1 % int1))
The tiger sees the dog.
("tiger" "sees" "dog" "+")
int1
The tiger is kind.
("tiger" "is" "kind" "+")
int2
The tiger needs the tiger.
True
4
proof
[(((((((triple8) -> rule4)) -> rule1)) -> rule2))]
("tiger" "needs" "tiger" "+")
((((((triple8) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int1
The tiger sees the dog.
("tiger" "sees" "dog" "+")
int2
The tiger is kind.
("tiger" "is" "kind" "+")
int3
The dog does not need the tiger.
False
4
inv-proof
[(((((((triple5) -> rule4)) -> rule1)) -> rule2))]
("dog" "needs" "tiger" "-")
((((((triple5) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
The dog needs the tiger.
("dog" "needs" "tiger" "+")
int1
The dog sees the dog.
("dog" "sees" "dog" "+")
int2
The dog is kind.
("dog" "is" "kind" "+")
int3
The cow is not kind.
Unknown
inv-rconc
[@1: The cow is kind.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cow" "is" "kind" "-")
The dog chases the cow.
Unknown
rconc
[@1: The dog chases the cow.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("dog" "chases" "cow" "+")
The cow does not see the dog.
Unknown
inv-rconc
[@2: The cow sees the dog.[CWA. Example of deepest failure = (rule1 <- rule4 <- FAIL)]]
("cow" "sees" "dog" "-")
The cow chases the tiger.
Unknown
random
[@0: The cow chases the tiger.[CWA. Example of deepest failure = (FAIL)]]
("cow" "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 dog sees the tiger.
Unknown
random
[@0: The dog sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("dog" "sees" "tiger" "+")
The tiger does not chase the tiger.
Unknown
inv-random
[@0: The tiger chases the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "chases" "tiger" "-")
The cow is green.
Unknown
random
[@0: The cow is green.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "green" "+")
@0: The cow is rough.[(triple1)] The cow is round.[(triple2)] The cow needs the tiger.[(triple3 OR ((triple2) -> rule6))] The cow sees the tiger.[(triple4)] The dog is green.[(triple5)] The dog is young.[(triple6)] The tiger chases the cow.[(triple7)] The tiger is green.[(triple8)] The tiger is rough.[(triple9)] The tiger needs the dog.[(triple10)] @1: The cow is young.[(((triple4 triple7) -> rule5))] The dog is kind.[(((triple5) -> rule4))] The tiger is kind.[(((triple8) -> rule4))] @2: The dog sees the dog.[(((((triple5) -> rule4)) -> rule1))] The tiger sees the dog.[(((((triple8) -> rule4)) -> rule1))] @3: The dog needs the tiger.[(((((((triple5) -> rule4)) -> rule1)) -> rule2))] The tiger needs the tiger.[(((((((triple8) -> rule4)) -> rule1)) -> rule2))]
The cow is rough.
("cow" "is" "rough" "+")
triple1
The cow is round.
("cow" "is" "round" "+")
triple2
The cow needs the tiger.
("cow" "needs" "tiger" "+")
triple3
((triple2) -> (rule6 % int1))
The cow needs the tiger.
("cow" "needs" "tiger" "+")
int1
The cow sees the tiger.
("cow" "sees" "tiger" "+")
triple4
The dog is green.
("dog" "is" "green" "+")
triple5
The dog is young.
("dog" "is" "young" "+")
triple6
The tiger chases the cow.
("tiger" "chases" "cow" "+")
triple7
The tiger is green.
("tiger" "is" "green" "+")
triple8
The tiger is rough.
("tiger" "is" "rough" "+")
triple9
The tiger needs the dog.
("tiger" "needs" "dog" "+")
triple10
The cow is young.
("cow" "is" "young" "+")
((triple4 triple7) -> (rule5 % int1))
The cow is young.
("cow" "is" "young" "+")
int1
The dog is kind.
("dog" "is" "kind" "+")
((triple5) -> (rule4 % int1))
The dog is kind.
("dog" "is" "kind" "+")
int1
The tiger is kind.
("tiger" "is" "kind" "+")
((triple8) -> (rule4 % int1))
The tiger is kind.
("tiger" "is" "kind" "+")
int1
The dog sees the dog.
("dog" "sees" "dog" "+")
((((triple5) -> (rule4 % int2))) -> (rule1 % int1))
The dog sees the dog.
("dog" "sees" "dog" "+")
int1
The dog is kind.
("dog" "is" "kind" "+")
int2
The tiger sees the dog.
("tiger" "sees" "dog" "+")
((((triple8) -> (rule4 % int2))) -> (rule1 % int1))
The tiger sees the dog.
("tiger" "sees" "dog" "+")
int1
The tiger is kind.
("tiger" "is" "kind" "+")
int2
The dog needs the tiger.
("dog" "needs" "tiger" "+")
((((((triple5) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
The dog needs the tiger.
("dog" "needs" "tiger" "+")
int1
The dog sees the dog.
("dog" "sees" "dog" "+")
int2
The dog is kind.
("dog" "is" "kind" "+")
int3
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
((((((triple8) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int1
The tiger sees the dog.
("tiger" "sees" "dog" "+")
int2
The tiger is kind.
("tiger" "is" "kind" "+")
int3