The cat chases the lion. The cat likes the lion. The cow chases the cat. The cow chases the lion. The cow likes the lion. The cow does not see the lion. The dog chases the cat. The dog does not like the cow. The lion chases the cow. The lion is big. The lion sees the cat. If something is kind and it chases the cat then it chases the cow. If something chases the cat then it sees the cow. If something likes the lion then it chases the cat. If something likes the cat and it is red then it chases the cat. If something sees the dog then it is kind. If something sees the dog then it sees the cat. If something sees the cow then it sees the dog.
The cat chases the lion.
("cat" "chases" "lion" "+")
The cat likes the lion.
("cat" "likes" "lion" "+")
The cow chases the cat.
("cow" "chases" "cat" "+")
The cow chases the lion.
("cow" "chases" "lion" "+")
The cow likes the lion.
("cow" "likes" "lion" "+")
The cow does not see the lion.
("cow" "sees" "lion" "-")
The dog chases the cat.
("dog" "chases" "cat" "+")
The dog does not like the cow.
("dog" "likes" "cow" "-")
The lion chases the cow.
("lion" "chases" "cow" "+")
The lion is big.
("lion" "is" "big" "+")
The lion sees the cat.
("lion" "sees" "cat" "+")
If something is kind and it chases the cat then it chases the cow.
((("something" "is" "kind" "+") ("something" "chases" "cat" "+")) -> ("something" "chases" "cow" "+"))
If something chases the cat then it sees the cow.
((("something" "chases" "cat" "+")) -> ("something" "sees" "cow" "+"))
If something likes the lion then it chases the cat.
((("something" "likes" "lion" "+")) -> ("something" "chases" "cat" "+"))
If something likes the cat and it is red then it chases the cat.
((("something" "likes" "cat" "+") ("something" "is" "red" "+")) -> ("something" "chases" "cat" "+"))
If something sees the dog then it is kind.
((("something" "sees" "dog" "+")) -> ("something" "is" "kind" "+"))
If something sees the dog then it sees the cat.
((("something" "sees" "dog" "+")) -> ("something" "sees" "cat" "+"))
If something sees the cow then it sees the dog.
((("something" "sees" "cow" "+")) -> ("something" "sees" "dog" "+"))
The cow likes the lion.
True
1
proof
[(triple5)]
("cow" "likes" "lion" "+")
triple5
The dog does not chase the cat.
False
1
inv-proof
[(triple7)]
("dog" "chases" "cat" "-")
triple7
The cow sees the cow.
True
2
proof
[(((triple3) -> rule2) OR ((((triple5) -> rule3)) -> rule2))]
("cow" "sees" "cow" "+")
((triple3) -> (rule2 % int1))
The cow sees the cow.
("cow" "sees" "cow" "+")
int1
((((triple5) -> (rule3 % int2))) -> (rule2 % int1))
The cow sees the cow.
("cow" "sees" "cow" "+")
int1
The cow chases the cat.
("cow" "chases" "cat" "+")
int2
The dog does not see the cow.
False
2
inv-proof
[(((triple7) -> rule2))]
("dog" "sees" "cow" "-")
((triple7) -> (rule2 % int1))
The dog sees the cow.
("dog" "sees" "cow" "+")
int1
The dog sees the dog.
True
3
proof
[(((((triple7) -> rule2)) -> rule7))]
("dog" "sees" "dog" "+")
((((triple7) -> (rule2 % int2))) -> (rule7 % int1))
The dog sees the dog.
("dog" "sees" "dog" "+")
int1
The dog sees the cow.
("dog" "sees" "cow" "+")
int2
The dog does not see the dog.
False
3
inv-proof
[(((((triple7) -> rule2)) -> rule7))]
("dog" "sees" "dog" "-")
((((triple7) -> (rule2 % int2))) -> (rule7 % int1))
The dog sees the dog.
("dog" "sees" "dog" "+")
int1
The dog sees the cow.
("dog" "sees" "cow" "+")
int2
The cow sees the cat.
True
4
proof
[(((((((triple3) -> rule2)) -> rule7)) -> rule6) OR ((((((((triple5) -> rule3)) -> rule2)) -> rule7)) -> rule6))]
("cow" "sees" "cat" "+")
((((((triple3) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
The cow sees the cat.
("cow" "sees" "cat" "+")
int1
The cow sees the dog.
("cow" "sees" "dog" "+")
int2
The cow sees the cow.
("cow" "sees" "cow" "+")
int3
((((((((triple5) -> (rule3 % int4))) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
The cow sees the cat.
("cow" "sees" "cat" "+")
int1
The cow sees the dog.
("cow" "sees" "dog" "+")
int2
The cow sees the cow.
("cow" "sees" "cow" "+")
int3
The cow chases the cat.
("cow" "chases" "cat" "+")
int4
The cow is not kind.
False
4
inv-proof
[(((((((triple3) -> rule2)) -> rule7)) -> rule5) OR ((((((((triple5) -> rule3)) -> rule2)) -> rule7)) -> rule5))]
("cow" "is" "kind" "-")
((((((triple3) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
The cow is kind.
("cow" "is" "kind" "+")
int1
The cow sees the dog.
("cow" "sees" "dog" "+")
int2
The cow sees the cow.
("cow" "sees" "cow" "+")
int3
((((((((triple5) -> (rule3 % int4))) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
The cow is kind.
("cow" "is" "kind" "+")
int1
The cow sees the dog.
("cow" "sees" "dog" "+")
int2
The cow sees the cow.
("cow" "sees" "cow" "+")
int3
The cow chases the cat.
("cow" "chases" "cat" "+")
int4
The dog chases the cow.
True
6
proof
[(((((((((triple7) -> rule2)) -> rule7)) -> rule5) triple7) -> rule1))]
("dog" "chases" "cow" "+")
((((((((triple7) -> (rule2 % int4))) -> (rule7 % int3))) -> (rule5 % int2)) triple7) -> (rule1 % int1))
The dog chases the cow.
("dog" "chases" "cow" "+")
int1
The dog is kind.
("dog" "is" "kind" "+")
int2
The dog sees the dog.
("dog" "sees" "dog" "+")
int3
The dog sees the cow.
("dog" "sees" "cow" "+")
int4
The cat is not kind.
False
5
inv-proof
[(((((((((triple2) -> rule3)) -> rule2)) -> rule7)) -> rule5))]
("cat" "is" "kind" "-")
((((((((triple2) -> (rule3 % int4))) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
The cat is kind.
("cat" "is" "kind" "+")
int1
The cat sees the dog.
("cat" "sees" "dog" "+")
int2
The cat sees the cow.
("cat" "sees" "cow" "+")
int3
The cat chases the cat.
("cat" "chases" "cat" "+")
int4
The cat chases the cow.
True
8
proof
[(((((((((((triple2) -> rule3)) -> rule2)) -> rule7)) -> rule5) ((triple2) -> rule3)) -> rule1))]
("cat" "chases" "cow" "+")
((((((((((triple2) -> (rule3 % int5))) -> (rule2 % int4))) -> (rule7 % int3))) -> (rule5 % int2)) ((triple2) -> (rule3 % int5))) -> (rule1 % int1))
The cat chases the cow.
("cat" "chases" "cow" "+")
int1
The cat is kind.
("cat" "is" "kind" "+")
int2
The cat sees the dog.
("cat" "sees" "dog" "+")
int3
The cat sees the cow.
("cat" "sees" "cow" "+")
int4
The cat chases the cat.
("cat" "chases" "cat" "+")
int5
The cat does not chase the cow.
False
8
inv-proof
[(((((((((((triple2) -> rule3)) -> rule2)) -> rule7)) -> rule5) ((triple2) -> rule3)) -> rule1))]
("cat" "chases" "cow" "-")
((((((((((triple2) -> (rule3 % int5))) -> (rule2 % int4))) -> (rule7 % int3))) -> (rule5 % int2)) ((triple2) -> (rule3 % int5))) -> (rule1 % int1))
The cat chases the cow.
("cat" "chases" "cow" "+")
int1
The cat is kind.
("cat" "is" "kind" "+")
int2
The cat sees the dog.
("cat" "sees" "dog" "+")
int3
The cat sees the cow.
("cat" "sees" "cow" "+")
int4
The cat chases the cat.
("cat" "chases" "cat" "+")
int5
The lion does not see the cow.
Unknown
inv-rconc
[@2: The lion sees the cow.[CWA. Example of deepest failure = (rule2 <- rule3 <- FAIL)]]
("lion" "sees" "cow" "-")
The lion sees the dog.
Unknown
rconc
[@3: The lion sees the dog.[CWA. Example of deepest failure = (rule7 <- rule2 <- rule3 <- FAIL)]]
("lion" "sees" "dog" "+")
The lion is not kind.
Unknown
inv-rconc
[@4: The lion is kind.[CWA. Example of deepest failure = (rule5 <- rule7 <- rule2 <- rule3 <- FAIL)]]
("lion" "is" "kind" "-")
The lion chases the cat.
Unknown
rconc
[@1: The lion chases the cat.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("lion" "chases" "cat" "+")
The cow does not like the dog.
Unknown
inv-random
[@0: The cow likes the dog.[CWA. Example of deepest failure = (FAIL)]]
("cow" "likes" "dog" "-")
The lion chases the lion.
Unknown
random
[@0: The lion chases the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "lion" "+")
The lion does not like the dog.
Unknown
inv-random
[@0: The lion likes the dog.[CWA. Example of deepest failure = (FAIL)]]
("lion" "likes" "dog" "-")
The cow likes the cow.
Unknown
random
[@0: The cow likes the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "likes" "cow" "+")
The cat does not like the dog.
Unknown
inv-random
[@0: The cat likes the dog.[CWA. Example of deepest failure = (FAIL)]]
("cat" "likes" "dog" "-")
The cow is cold.
Unknown
random
[@0: The cow is cold.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "cold" "+")
The cow is not nice.
Unknown
inv-random
[@0: The cow is nice.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "nice" "-")
The dog likes the cat.
Unknown
random
[@0: The dog likes the cat.[CWA. Example of deepest failure = (FAIL)]]
("dog" "likes" "cat" "+")
@0: The cat chases the lion.[(triple1)] The cat likes the lion.[(triple2)] The cow chases the cat.[(triple3 OR ((triple5) -> rule3))] The cow chases the lion.[(triple4)] The cow does not see the lion.[(triple6)] The cow likes the lion.[(triple5)] The dog chases the cat.[(triple7)] The dog does not like the cow.[(triple8)] The lion chases the cow.[(triple9)] The lion is big.[(triple10)] The lion sees the cat.[(triple11)] @1: The cat chases the cat.[(((triple2) -> rule3))] The cow sees the cow.[(((triple3) -> rule2) OR ((((triple5) -> rule3)) -> rule2))] The dog sees the cow.[(((triple7) -> rule2))] @2: The cat sees the cow.[(((((triple2) -> rule3)) -> rule2))] The cow sees the dog.[(((((triple3) -> rule2)) -> rule7) OR ((((((triple5) -> rule3)) -> rule2)) -> rule7))] The dog sees the dog.[(((((triple7) -> rule2)) -> rule7))] @3: The cat sees the dog.[(((((((triple2) -> rule3)) -> rule2)) -> rule7))] The cow is kind.[(((((((triple3) -> rule2)) -> rule7)) -> rule5) OR ((((((((triple5) -> rule3)) -> rule2)) -> rule7)) -> rule5))] The cow sees the cat.[(((((((triple3) -> rule2)) -> rule7)) -> rule6) OR ((((((((triple5) -> rule3)) -> rule2)) -> rule7)) -> rule6))] The dog is kind.[(((((((triple7) -> rule2)) -> rule7)) -> rule5))] The dog sees the cat.[(((((((triple7) -> rule2)) -> rule7)) -> rule6))] @4: The cat is kind.[(((((((((triple2) -> rule3)) -> rule2)) -> rule7)) -> rule5))] The cat sees the cat.[(((((((((triple2) -> rule3)) -> rule2)) -> rule7)) -> rule6))] The cow chases the cow.[(((((((((triple3) -> rule2)) -> rule7)) -> rule5) triple3) -> rule1) OR ((((((((triple3) -> rule2)) -> rule7)) -> rule5) ((triple5) -> rule3)) -> rule1) OR ((((((((((triple5) -> rule3)) -> rule2)) -> rule7)) -> rule5) triple3) -> rule1) OR ((((((((((triple5) -> rule3)) -> rule2)) -> rule7)) -> rule5) ((triple5) -> rule3)) -> rule1))] The dog chases the cow.[(((((((((triple7) -> rule2)) -> rule7)) -> rule5) triple7) -> rule1))] @5: The cat chases the cow.[(((((((((((triple2) -> rule3)) -> rule2)) -> rule7)) -> rule5) ((triple2) -> rule3)) -> rule1))]
The cat chases the lion.
("cat" "chases" "lion" "+")
triple1
The cat likes the lion.
("cat" "likes" "lion" "+")
triple2
The cow chases the cat.
("cow" "chases" "cat" "+")
triple3
((triple5) -> (rule3 % int1))
The cow chases the cat.
("cow" "chases" "cat" "+")
int1
The cow chases the lion.
("cow" "chases" "lion" "+")
triple4
The cow does not see the lion.
("cow" "sees" "lion" "-")
triple6
The cow likes the lion.
("cow" "likes" "lion" "+")
triple5
The dog chases the cat.
("dog" "chases" "cat" "+")
triple7
The dog does not like the cow.
("dog" "likes" "cow" "-")
triple8
The lion chases the cow.
("lion" "chases" "cow" "+")
triple9
The lion is big.
("lion" "is" "big" "+")
triple10
The lion sees the cat.
("lion" "sees" "cat" "+")
triple11
The cat chases the cat.
("cat" "chases" "cat" "+")
((triple2) -> (rule3 % int1))
The cat chases the cat.
("cat" "chases" "cat" "+")
int1
The cow sees the cow.
("cow" "sees" "cow" "+")
((triple3) -> (rule2 % int1))
The cow sees the cow.
("cow" "sees" "cow" "+")
int1
((((triple5) -> (rule3 % int2))) -> (rule2 % int1))
The cow sees the cow.
("cow" "sees" "cow" "+")
int1
The cow chases the cat.
("cow" "chases" "cat" "+")
int2
The dog sees the cow.
("dog" "sees" "cow" "+")
((triple7) -> (rule2 % int1))
The dog sees the cow.
("dog" "sees" "cow" "+")
int1
The cat sees the cow.
("cat" "sees" "cow" "+")
((((triple2) -> (rule3 % int2))) -> (rule2 % int1))
The cat sees the cow.
("cat" "sees" "cow" "+")
int1
The cat chases the cat.
("cat" "chases" "cat" "+")
int2
The cow sees the dog.
("cow" "sees" "dog" "+")
((((triple3) -> (rule2 % int2))) -> (rule7 % int1))
The cow sees the dog.
("cow" "sees" "dog" "+")
int1
The cow sees the cow.
("cow" "sees" "cow" "+")
int2
((((((triple5) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
The cow sees the dog.
("cow" "sees" "dog" "+")
int1
The cow sees the cow.
("cow" "sees" "cow" "+")
int2
The cow chases the cat.
("cow" "chases" "cat" "+")
int3
The dog sees the dog.
("dog" "sees" "dog" "+")
((((triple7) -> (rule2 % int2))) -> (rule7 % int1))
The dog sees the dog.
("dog" "sees" "dog" "+")
int1
The dog sees the cow.
("dog" "sees" "cow" "+")
int2
The cat sees the dog.
("cat" "sees" "dog" "+")
((((((triple2) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
The cat sees the dog.
("cat" "sees" "dog" "+")
int1
The cat sees the cow.
("cat" "sees" "cow" "+")
int2
The cat chases the cat.
("cat" "chases" "cat" "+")
int3
The cow is kind.
("cow" "is" "kind" "+")
((((((triple3) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
The cow is kind.
("cow" "is" "kind" "+")
int1
The cow sees the dog.
("cow" "sees" "dog" "+")
int2
The cow sees the cow.
("cow" "sees" "cow" "+")
int3
((((((((triple5) -> (rule3 % int4))) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
The cow is kind.
("cow" "is" "kind" "+")
int1
The cow sees the dog.
("cow" "sees" "dog" "+")
int2
The cow sees the cow.
("cow" "sees" "cow" "+")
int3
The cow chases the cat.
("cow" "chases" "cat" "+")
int4
The cow sees the cat.
("cow" "sees" "cat" "+")
((((((triple3) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
The cow sees the cat.
("cow" "sees" "cat" "+")
int1
The cow sees the dog.
("cow" "sees" "dog" "+")
int2
The cow sees the cow.
("cow" "sees" "cow" "+")
int3
((((((((triple5) -> (rule3 % int4))) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
The cow sees the cat.
("cow" "sees" "cat" "+")
int1
The cow sees the dog.
("cow" "sees" "dog" "+")
int2
The cow sees the cow.
("cow" "sees" "cow" "+")
int3
The cow chases the cat.
("cow" "chases" "cat" "+")
int4
The dog is kind.
("dog" "is" "kind" "+")
((((((triple7) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
The dog is kind.
("dog" "is" "kind" "+")
int1
The dog sees the dog.
("dog" "sees" "dog" "+")
int2
The dog sees the cow.
("dog" "sees" "cow" "+")
int3
The dog sees the cat.
("dog" "sees" "cat" "+")
((((((triple7) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
The dog sees the cat.
("dog" "sees" "cat" "+")
int1
The dog sees the dog.
("dog" "sees" "dog" "+")
int2
The dog sees the cow.
("dog" "sees" "cow" "+")
int3
The cat is kind.
("cat" "is" "kind" "+")
((((((((triple2) -> (rule3 % int4))) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
The cat is kind.
("cat" "is" "kind" "+")
int1
The cat sees the dog.
("cat" "sees" "dog" "+")
int2
The cat sees the cow.
("cat" "sees" "cow" "+")
int3
The cat chases the cat.
("cat" "chases" "cat" "+")
int4
The cat sees the cat.
("cat" "sees" "cat" "+")
((((((((triple2) -> (rule3 % int4))) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
The cat sees the cat.
("cat" "sees" "cat" "+")
int1
The cat sees the dog.
("cat" "sees" "dog" "+")
int2
The cat sees the cow.
("cat" "sees" "cow" "+")
int3
The cat chases the cat.
("cat" "chases" "cat" "+")
int4
The cow chases the cow.
("cow" "chases" "cow" "+")
((((((((triple3) -> (rule2 % int4))) -> (rule7 % int3))) -> (rule5 % int2)) triple3) -> (rule1 % int1))
The cow chases the cow.
("cow" "chases" "cow" "+")
int1
The cow is kind.
("cow" "is" "kind" "+")
int2
The cow sees the dog.
("cow" "sees" "dog" "+")
int3
The cow sees the cow.
("cow" "sees" "cow" "+")
int4
((((((((triple3) -> (rule2 % int5))) -> (rule7 % int4))) -> (rule5 % int3)) ((triple5) -> (rule3 % int2))) -> (rule1 % int1))
The cow chases the cow.
("cow" "chases" "cow" "+")
int1
The cow chases the cat.
("cow" "chases" "cat" "+")
int2
The cow is kind.
("cow" "is" "kind" "+")
int3
The cow sees the dog.
("cow" "sees" "dog" "+")
int4
The cow sees the cow.
("cow" "sees" "cow" "+")
int5
((((((((((triple5) -> (rule3 % int5))) -> (rule2 % int4))) -> (rule7 % int3))) -> (rule5 % int2)) triple3) -> (rule1 % int1))
The cow chases the cow.
("cow" "chases" "cow" "+")
int1
The cow is kind.
("cow" "is" "kind" "+")
int2
The cow sees the dog.
("cow" "sees" "dog" "+")
int3
The cow sees the cow.
("cow" "sees" "cow" "+")
int4
The cow chases the cat.
("cow" "chases" "cat" "+")
int5
((((((((((triple5) -> (rule3 % int5))) -> (rule2 % int4))) -> (rule7 % int3))) -> (rule5 % int2)) ((triple5) -> (rule3 % int5))) -> (rule1 % int1))
The cow chases the cow.
("cow" "chases" "cow" "+")
int1
The cow is kind.
("cow" "is" "kind" "+")
int2
The cow sees the dog.
("cow" "sees" "dog" "+")
int3
The cow sees the cow.
("cow" "sees" "cow" "+")
int4
The cow chases the cat.
("cow" "chases" "cat" "+")
int5
The dog chases the cow.
("dog" "chases" "cow" "+")
((((((((triple7) -> (rule2 % int4))) -> (rule7 % int3))) -> (rule5 % int2)) triple7) -> (rule1 % int1))
The dog chases the cow.
("dog" "chases" "cow" "+")
int1
The dog is kind.
("dog" "is" "kind" "+")
int2
The dog sees the dog.
("dog" "sees" "dog" "+")
int3
The dog sees the cow.
("dog" "sees" "cow" "+")
int4
The cat chases the cow.
("cat" "chases" "cow" "+")
((((((((((triple2) -> (rule3 % int5))) -> (rule2 % int4))) -> (rule7 % int3))) -> (rule5 % int2)) ((triple2) -> (rule3 % int5))) -> (rule1 % int1))
The cat chases the cow.
("cat" "chases" "cow" "+")
int1
The cat is kind.
("cat" "is" "kind" "+")
int2
The cat sees the dog.
("cat" "sees" "dog" "+")
int3
The cat sees the cow.
("cat" "sees" "cow" "+")
int4
The cat chases the cat.
("cat" "chases" "cat" "+")
int5