The cat is blue. The cow is round. The cow needs the cat. The dog is nice. The dog is round. The dog needs the cat. The dog needs the rabbit. The dog sees the cat. The rabbit needs the dog. The rabbit sees the cow. Round people are kind. If the cow needs the dog then the dog chases the cat. If someone sees the cow and they are blue then the cow chases the rabbit. Kind people are rough. If someone is blue then they see the cat. If someone chases the cat then the cat sees the rabbit. If someone is nice and they need the dog then the dog needs the cat. If someone is round then they see the rabbit. If someone is rough then they need the dog.
The cat is blue.
("cat" "is" "blue" "+")
The cow is round.
("cow" "is" "round" "+")
The cow needs the cat.
("cow" "needs" "cat" "+")
The dog is nice.
("dog" "is" "nice" "+")
The dog is round.
("dog" "is" "round" "+")
The dog needs the cat.
("dog" "needs" "cat" "+")
The dog needs the rabbit.
("dog" "needs" "rabbit" "+")
The dog sees the cat.
("dog" "sees" "cat" "+")
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
The rabbit sees the cow.
("rabbit" "sees" "cow" "+")
Round people are kind.
((("someone" "is" "round" "+")) -> ("someone" "is" "kind" "+"))
If the cow needs the dog then the dog chases the cat.
((("cow" "needs" "dog" "+")) -> ("dog" "chases" "cat" "+"))
If someone sees the cow and they are blue then the cow chases the rabbit.
((("someone" "sees" "cow" "+") ("someone" "is" "blue" "+")) -> ("cow" "chases" "rabbit" "+"))
Kind people are rough.
((("someone" "is" "kind" "+")) -> ("someone" "is" "rough" "+"))
If someone is blue then they see the cat.
((("someone" "is" "blue" "+")) -> ("someone" "sees" "cat" "+"))
If someone chases the cat then the cat sees the rabbit.
((("someone" "chases" "cat" "+")) -> ("cat" "sees" "rabbit" "+"))
If someone is nice and they need the dog then the dog needs the cat.
((("someone" "is" "nice" "+") ("someone" "needs" "dog" "+")) -> ("dog" "needs" "cat" "+"))
If someone is round then they see the rabbit.
((("someone" "is" "round" "+")) -> ("someone" "sees" "rabbit" "+"))
If someone is rough then they need the dog.
((("someone" "is" "rough" "+")) -> ("someone" "needs" "dog" "+"))
The cow needs the cat.
True
1
proof
[(triple3)]
("cow" "needs" "cat" "+")
triple3
The dog is not nice.
False
1
inv-proof
[(triple4)]
("dog" "is" "nice" "-")
triple4
The dog sees the rabbit.
True
2
proof
[(((triple5) -> rule8))]
("dog" "sees" "rabbit" "+")
((triple5) -> (rule8 % int1))
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
int1
The dog is not kind.
False
2
inv-proof
[(((triple5) -> rule1))]
("dog" "is" "kind" "-")
((triple5) -> (rule1 % int1))
The dog is kind.
("dog" "is" "kind" "+")
int1
The cow is rough.
True
3
proof
[(((((triple2) -> rule1)) -> rule4))]
("cow" "is" "rough" "+")
((((triple2) -> (rule1 % int2))) -> (rule4 % int1))
The cow is rough.
("cow" "is" "rough" "+")
int1
The cow is kind.
("cow" "is" "kind" "+")
int2
The cow is not rough.
False
3
inv-proof
[(((((triple2) -> rule1)) -> rule4))]
("cow" "is" "rough" "-")
((((triple2) -> (rule1 % int2))) -> (rule4 % int1))
The cow is rough.
("cow" "is" "rough" "+")
int1
The cow is kind.
("cow" "is" "kind" "+")
int2
The cow needs the dog.
True
4
proof
[(((((((triple2) -> rule1)) -> rule4)) -> rule9))]
("cow" "needs" "dog" "+")
((((((triple2) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule9 % int1))
The cow needs the dog.
("cow" "needs" "dog" "+")
int1
The cow is rough.
("cow" "is" "rough" "+")
int2
The cow is kind.
("cow" "is" "kind" "+")
int3
The cow does not need the dog.
False
4
inv-proof
[(((((((triple2) -> rule1)) -> rule4)) -> rule9))]
("cow" "needs" "dog" "-")
((((((triple2) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule9 % int1))
The cow needs the dog.
("cow" "needs" "dog" "+")
int1
The cow is rough.
("cow" "is" "rough" "+")
int2
The cow is kind.
("cow" "is" "kind" "+")
int3
The dog chases the cat.
True
5
proof
[(((((((((triple2) -> rule1)) -> rule4)) -> rule9)) -> rule2))]
("dog" "chases" "cat" "+")
((((((((triple2) -> (rule1 % int4))) -> (rule4 % int3))) -> (rule9 % int2))) -> (rule2 % int1))
The dog chases the cat.
("dog" "chases" "cat" "+")
int1
The cow needs the dog.
("cow" "needs" "dog" "+")
int2
The cow is rough.
("cow" "is" "rough" "+")
int3
The cow is kind.
("cow" "is" "kind" "+")
int4
The dog does not chase the cat.
False
5
inv-proof
[(((((((((triple2) -> rule1)) -> rule4)) -> rule9)) -> rule2))]
("dog" "chases" "cat" "-")
((((((((triple2) -> (rule1 % int4))) -> (rule4 % int3))) -> (rule9 % int2))) -> (rule2 % int1))
The dog chases the cat.
("dog" "chases" "cat" "+")
int1
The cow needs the dog.
("cow" "needs" "dog" "+")
int2
The cow is rough.
("cow" "is" "rough" "+")
int3
The cow is kind.
("cow" "is" "kind" "+")
int4
The cat sees the rabbit.
True
6
proof
[(((((((((((triple2) -> rule1)) -> rule4)) -> rule9)) -> rule2)) -> rule6))]
("cat" "sees" "rabbit" "+")
((((((((((triple2) -> (rule1 % int5))) -> (rule4 % int4))) -> (rule9 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
int1
The dog chases the cat.
("dog" "chases" "cat" "+")
int2
The cow needs the dog.
("cow" "needs" "dog" "+")
int3
The cow is rough.
("cow" "is" "rough" "+")
int4
The cow is kind.
("cow" "is" "kind" "+")
int5
The cat does not see the rabbit.
False
6
inv-proof
[(((((((((((triple2) -> rule1)) -> rule4)) -> rule9)) -> rule2)) -> rule6))]
("cat" "sees" "rabbit" "-")
((((((((((triple2) -> (rule1 % int5))) -> (rule4 % int4))) -> (rule9 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
int1
The dog chases the cat.
("dog" "chases" "cat" "+")
int2
The cow needs the dog.
("cow" "needs" "dog" "+")
int3
The cow is rough.
("cow" "is" "rough" "+")
int4
The cow is kind.
("cow" "is" "kind" "+")
int5
The cat is not rough.
Unknown
inv-rconc
[@2: The cat is rough.[CWA. Example of deepest failure = (rule4 <- rule1 <- FAIL)]]
("cat" "is" "rough" "-")
The rabbit is rough.
Unknown
rconc
[@2: The rabbit is rough.[CWA. Example of deepest failure = (rule4 <- rule1 <- FAIL)]]
("rabbit" "is" "rough" "+")
The cow does not see the cat.
Unknown
inv-rconc
[@1: The cow sees the cat.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("cow" "sees" "cat" "-")
The cow chases the rabbit.
Unknown
rconc
[@1: The cow chases the rabbit.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cow" "chases" "rabbit" "+")
The cat does not need the dog.
Unknown
inv-rconc
[@3: The cat needs the dog.[CWA. Example of deepest failure = (rule9 <- rule4 <- rule1 <- FAIL)]]
("cat" "needs" "dog" "-")
The rabbit sees the rabbit.
Unknown
rconc
[@1: The rabbit sees the rabbit.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("rabbit" "sees" "rabbit" "+")
The cat does not chase the cow.
Unknown
inv-random
[@0: The cat chases the cow.[CWA. Example of deepest failure = (FAIL)]]
("cat" "chases" "cow" "-")
The cow needs the cow.
Unknown
random
[@0: The cow needs the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "needs" "cow" "+")
The cat does not chase the rabbit.
Unknown
inv-random
[@0: The cat chases the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("cat" "chases" "rabbit" "-")
The cow sees the dog.
Unknown
random
[@0: The cow sees the dog.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "dog" "+")
The cat does not see the dog.
Unknown
inv-random
[@0: The cat sees the dog.[CWA. Example of deepest failure = (FAIL)]]
("cat" "sees" "dog" "-")
The dog needs the cow.
Unknown
random
[@0: The dog needs the cow.[CWA. Example of deepest failure = (FAIL)]]
("dog" "needs" "cow" "+")
@0: The cat is blue.[(triple1)] The cow is round.[(triple2)] The cow needs the cat.[(triple3)] The dog is nice.[(triple4)] The dog is round.[(triple5)] The dog needs the cat.[(triple6 OR ((triple4 ((((((triple5) -> rule1)) -> rule4)) -> rule9)) -> rule7))] The dog needs the rabbit.[(triple7)] The dog sees the cat.[(triple8)] The rabbit needs the dog.[(triple9)] The rabbit sees the cow.[(triple10)] @1: The cat sees the cat.[(((triple1) -> rule5))] The cow is kind.[(((triple2) -> rule1))] The cow sees the rabbit.[(((triple2) -> rule8))] The dog is kind.[(((triple5) -> rule1))] The dog sees the rabbit.[(((triple5) -> rule8))] @2: The cow is rough.[(((((triple2) -> rule1)) -> rule4))] The dog is rough.[(((((triple5) -> rule1)) -> rule4))] @3: The cow needs the dog.[(((((((triple2) -> rule1)) -> rule4)) -> rule9))] The dog needs the dog.[(((((((triple5) -> rule1)) -> rule4)) -> rule9))] @4: The dog chases the cat.[(((((((((triple2) -> rule1)) -> rule4)) -> rule9)) -> rule2))] @5: The cat sees the rabbit.[(((((((((((triple2) -> rule1)) -> rule4)) -> rule9)) -> rule2)) -> rule6))]
The cat is blue.
("cat" "is" "blue" "+")
triple1
The cow is round.
("cow" "is" "round" "+")
triple2
The cow needs the cat.
("cow" "needs" "cat" "+")
triple3
The dog is nice.
("dog" "is" "nice" "+")
triple4
The dog is round.
("dog" "is" "round" "+")
triple5
The dog needs the cat.
("dog" "needs" "cat" "+")
triple6
((triple4 ((((((triple5) -> (rule1 % int4))) -> (rule4 % int3))) -> (rule9 % int2))) -> (rule7 % int1))
The dog needs the cat.
("dog" "needs" "cat" "+")
int1
The dog needs the dog.
("dog" "needs" "dog" "+")
int2
The dog is rough.
("dog" "is" "rough" "+")
int3
The dog is kind.
("dog" "is" "kind" "+")
int4
The dog needs the rabbit.
("dog" "needs" "rabbit" "+")
triple7
The dog sees the cat.
("dog" "sees" "cat" "+")
triple8
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
triple9
The rabbit sees the cow.
("rabbit" "sees" "cow" "+")
triple10
The cat sees the cat.
("cat" "sees" "cat" "+")
((triple1) -> (rule5 % int1))
The cat sees the cat.
("cat" "sees" "cat" "+")
int1
The cow is kind.
("cow" "is" "kind" "+")
((triple2) -> (rule1 % int1))
The cow is kind.
("cow" "is" "kind" "+")
int1
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
((triple2) -> (rule8 % int1))
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
int1
The dog is kind.
("dog" "is" "kind" "+")
((triple5) -> (rule1 % int1))
The dog is kind.
("dog" "is" "kind" "+")
int1
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
((triple5) -> (rule8 % int1))
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
int1
The cow is rough.
("cow" "is" "rough" "+")
((((triple2) -> (rule1 % int2))) -> (rule4 % int1))
The cow is rough.
("cow" "is" "rough" "+")
int1
The cow is kind.
("cow" "is" "kind" "+")
int2
The dog is rough.
("dog" "is" "rough" "+")
((((triple5) -> (rule1 % int2))) -> (rule4 % int1))
The dog is rough.
("dog" "is" "rough" "+")
int1
The dog is kind.
("dog" "is" "kind" "+")
int2
The cow needs the dog.
("cow" "needs" "dog" "+")
((((((triple2) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule9 % int1))
The cow needs the dog.
("cow" "needs" "dog" "+")
int1
The cow is rough.
("cow" "is" "rough" "+")
int2
The cow is kind.
("cow" "is" "kind" "+")
int3
The dog needs the dog.
("dog" "needs" "dog" "+")
((((((triple5) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule9 % int1))
The dog needs the dog.
("dog" "needs" "dog" "+")
int1
The dog is rough.
("dog" "is" "rough" "+")
int2
The dog is kind.
("dog" "is" "kind" "+")
int3
The dog chases the cat.
("dog" "chases" "cat" "+")
((((((((triple2) -> (rule1 % int4))) -> (rule4 % int3))) -> (rule9 % int2))) -> (rule2 % int1))
The dog chases the cat.
("dog" "chases" "cat" "+")
int1
The cow needs the dog.
("cow" "needs" "dog" "+")
int2
The cow is rough.
("cow" "is" "rough" "+")
int3
The cow is kind.
("cow" "is" "kind" "+")
int4
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
((((((((((triple2) -> (rule1 % int5))) -> (rule4 % int4))) -> (rule9 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
int1
The dog chases the cat.
("dog" "chases" "cat" "+")
int2
The cow needs the dog.
("cow" "needs" "dog" "+")
int3
The cow is rough.
("cow" "is" "rough" "+")
int4
The cow is kind.
("cow" "is" "kind" "+")
int5