The cat chases the lion. The cat does not chase the rabbit. The cat eats the rabbit. The cat visits the dog. The dog chases the cat. The dog chases the rabbit. The dog is young. The lion does not chase the cat. The lion is cold. The lion is young. The lion visits the cat. The rabbit chases the cat. The rabbit is young. The rabbit visits the cat. If someone eats the dog then the dog is kind. If someone visits the dog then they eat the dog. If someone is big then they visit the dog. If someone visits the dog and they are big then the dog is green. All kind people are big. If the dog visits the rabbit then the rabbit visits the lion. If the cat is cold and the rabbit does not visit the cat then the rabbit chases the lion. If someone visits the lion and the lion is kind then the lion eats the cat. If someone chases the lion and they are not green then they do not eat the cat.
The cat chases the lion.
("cat" "chases" "lion" "+")
The cat does not chase the rabbit.
("cat" "chases" "rabbit" "-")
The cat eats the rabbit.
("cat" "eats" "rabbit" "+")
The cat visits the dog.
("cat" "visits" "dog" "+")
The dog chases the cat.
("dog" "chases" "cat" "+")
The dog chases the rabbit.
("dog" "chases" "rabbit" "+")
The dog is young.
("dog" "is" "young" "+")
The lion does not chase the cat.
("lion" "chases" "cat" "-")
The lion is cold.
("lion" "is" "cold" "+")
The lion is young.
("lion" "is" "young" "+")
The lion visits the cat.
("lion" "visits" "cat" "+")
The rabbit chases the cat.
("rabbit" "chases" "cat" "+")
The rabbit is young.
("rabbit" "is" "young" "+")
The rabbit visits the cat.
("rabbit" "visits" "cat" "+")
If someone eats the dog then the dog is kind.
((("someone" "eats" "dog" "+")) -> ("dog" "is" "kind" "+"))
If someone visits the dog then they eat the dog.
((("someone" "visits" "dog" "+")) -> ("someone" "eats" "dog" "+"))
If someone is big then they visit the dog.
((("someone" "is" "big" "+")) -> ("someone" "visits" "dog" "+"))
If someone visits the dog and they are big then the dog is green.
((("someone" "visits" "dog" "+") ("someone" "is" "big" "+")) -> ("dog" "is" "green" "+"))
All kind people are big.
((("someone" "is" "kind" "+")) -> ("someone" "is" "big" "+"))
If the dog visits the rabbit then the rabbit visits the lion.
((("dog" "visits" "rabbit" "+")) -> ("rabbit" "visits" "lion" "+"))
If the cat is cold and the rabbit does not visit the cat then the rabbit chases the lion.
((("cat" "is" "cold" "+") ("rabbit" "visits" "cat" "~")) -> ("rabbit" "chases" "lion" "+"))
If someone visits the lion and the lion is kind then the lion eats the cat.
((("someone" "visits" "lion" "+") ("lion" "is" "kind" "+")) -> ("lion" "eats" "cat" "+"))
If someone chases the lion and they are not green then they do not eat the cat.
((("someone" "chases" "lion" "+") ("someone" "is" "green" "~")) -> ("someone" "eats" "cat" "-"))
The dog chases the cat.
True
1
proof
[(triple5)]
("dog" "chases" "cat" "+")
triple5
The dog is not young.
False
1
inv-proof
[(triple7)]
("dog" "is" "young" "-")
triple7
The cat eats the dog.
True
2
proof
[(((triple4) -> rule2))]
("cat" "eats" "dog" "+")
((triple4) -> (rule2 % int1))
The cat eats the dog.
("cat" "eats" "dog" "+")
int1
The cat does not eat the dog.
False
2
inv-proof
[(((triple4) -> rule2))]
("cat" "eats" "dog" "-")
((triple4) -> (rule2 % int1))
The cat eats the dog.
("cat" "eats" "dog" "+")
int1
The dog is kind.
True
3
proof
[(((((triple4) -> rule2)) -> rule1))]
("dog" "is" "kind" "+")
((((triple4) -> (rule2 % int2))) -> (rule1 % int1))
The dog is kind.
("dog" "is" "kind" "+")
int1
The cat eats the dog.
("cat" "eats" "dog" "+")
int2
The dog is not kind.
False
3
inv-proof
[(((((triple4) -> rule2)) -> rule1))]
("dog" "is" "kind" "-")
((((triple4) -> (rule2 % int2))) -> (rule1 % int1))
The dog is kind.
("dog" "is" "kind" "+")
int1
The cat eats the dog.
("cat" "eats" "dog" "+")
int2
The dog is big.
True
4
proof
[(((((((triple4) -> rule2)) -> rule1)) -> rule5))]
("dog" "is" "big" "+")
((((((triple4) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
The dog is big.
("dog" "is" "big" "+")
int1
The dog is kind.
("dog" "is" "kind" "+")
int2
The cat eats the dog.
("cat" "eats" "dog" "+")
int3
The dog is not big.
False
4
inv-proof
[(((((((triple4) -> rule2)) -> rule1)) -> rule5))]
("dog" "is" "big" "-")
((((((triple4) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
The dog is big.
("dog" "is" "big" "+")
int1
The dog is kind.
("dog" "is" "kind" "+")
int2
The cat eats the dog.
("cat" "eats" "dog" "+")
int3
The dog visits the dog.
True
5
proof
[(((((((((triple4) -> rule2)) -> rule1)) -> rule5)) -> rule3))]
("dog" "visits" "dog" "+")
((((((((triple4) -> (rule2 % int4))) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
The dog visits the dog.
("dog" "visits" "dog" "+")
int1
The dog is big.
("dog" "is" "big" "+")
int2
The dog is kind.
("dog" "is" "kind" "+")
int3
The cat eats the dog.
("cat" "eats" "dog" "+")
int4
The dog does not visit the dog.
False
5
inv-proof
[(((((((((triple4) -> rule2)) -> rule1)) -> rule5)) -> rule3))]
("dog" "visits" "dog" "-")
((((((((triple4) -> (rule2 % int4))) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
The dog visits the dog.
("dog" "visits" "dog" "+")
int1
The dog is big.
("dog" "is" "big" "+")
int2
The dog is kind.
("dog" "is" "kind" "+")
int3
The cat eats the dog.
("cat" "eats" "dog" "+")
int4
The dog is green.
True
10
proof
[(((((((((((triple4) -> rule2)) -> rule1)) -> rule5)) -> rule3) ((((((triple4) -> rule2)) -> rule1)) -> rule5)) -> rule4))]
("dog" "is" "green" "+")
((((((((((triple4) -> (rule2 % int5))) -> (rule1 % int4))) -> (rule5 % int3))) -> (rule3 % int2)) ((((((triple4) -> (rule2 % int5))) -> (rule1 % int4))) -> (rule5 % int3))) -> (rule4 % int1))
The dog is green.
("dog" "is" "green" "+")
int1
The dog visits the dog.
("dog" "visits" "dog" "+")
int2
The dog is big.
("dog" "is" "big" "+")
int3
The dog is kind.
("dog" "is" "kind" "+")
int4
The cat eats the dog.
("cat" "eats" "dog" "+")
int5
The dog is not green.
False
10
inv-proof
[(((((((((((triple4) -> rule2)) -> rule1)) -> rule5)) -> rule3) ((((((triple4) -> rule2)) -> rule1)) -> rule5)) -> rule4))]
("dog" "is" "green" "-")
((((((((((triple4) -> (rule2 % int5))) -> (rule1 % int4))) -> (rule5 % int3))) -> (rule3 % int2)) ((((((triple4) -> (rule2 % int5))) -> (rule1 % int4))) -> (rule5 % int3))) -> (rule4 % int1))
The dog is green.
("dog" "is" "green" "+")
int1
The dog visits the dog.
("dog" "visits" "dog" "+")
int2
The dog is big.
("dog" "is" "big" "+")
int3
The dog is kind.
("dog" "is" "kind" "+")
int4
The cat eats the dog.
("cat" "eats" "dog" "+")
int5
The lion does not visit the dog.
Unknown
inv-rconc
[@2: The lion visits the dog.[CWA. Example of deepest failure = (rule3 <- rule5 <- FAIL)]]
("lion" "visits" "dog" "-")
The rabbit chases the lion.
Unknown
rconc
[@1: The rabbit chases the lion.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("rabbit" "chases" "lion" "+")
The lion does not eat the cat.
Unknown
inv-rconc
[@1: The lion eats the cat.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("lion" "eats" "cat" "-")
The rabbit visits the dog.
Unknown
rconc
[@2: The rabbit visits the dog.[CWA. Example of deepest failure = (rule3 <- rule5 <- FAIL)]]
("rabbit" "visits" "dog" "+")
The lion is not big.
Unknown
inv-rconc
[@1: The lion is big.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("lion" "is" "big" "-")
The rabbit visits the lion.
Unknown
rconc
[@1: The rabbit visits the lion.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("rabbit" "visits" "lion" "+")
The dog does not visit the cat.
Unknown
inv-random
[@0: The dog visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("dog" "visits" "cat" "-")
The cat is green.
Unknown
random
[@0: The cat is green.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "green" "+")
The lion is not green.
Unknown
inv-random
[@0: The lion is green.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "green" "-")
The dog chases the dog.
Unknown
random
[@0: The dog chases the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "chases" "dog" "+")
The lion does not visit the lion.
Unknown
inv-random
[@0: The lion visits the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "visits" "lion" "-")
The dog eats the cat.
Unknown
random
[@0: The dog eats the cat.[CWA. Example of deepest failure = (FAIL)]]
("dog" "eats" "cat" "+")
@0: The cat chases the lion.[(triple1)] The cat does not chase the rabbit.[(triple2)] The cat eats the rabbit.[(triple3)] The cat visits the dog.[(triple4)] The dog chases the cat.[(triple5)] The dog chases the rabbit.[(triple6)] The dog is young.[(triple7)] The lion does not chase the cat.[(triple8)] The lion is cold.[(triple9)] The lion is young.[(triple10)] The lion visits the cat.[(triple11)] The rabbit chases the cat.[(triple12)] The rabbit is young.[(triple13)] The rabbit visits the cat.[(triple14)] @1: The cat eats the dog.[(((triple4) -> rule2))] @2: The dog is kind.[(((((triple4) -> rule2)) -> rule1))] @3: The dog is big.[(((((((triple4) -> rule2)) -> rule1)) -> rule5))] @4: The dog visits the dog.[(((((((((triple4) -> rule2)) -> rule1)) -> rule5)) -> rule3))] @5: The dog eats the dog.[(((((((((((triple4) -> rule2)) -> rule1)) -> rule5)) -> rule3)) -> rule2))] The dog is green.[(((((((((((triple4) -> rule2)) -> rule1)) -> rule5)) -> rule3) ((((((triple4) -> rule2)) -> rule1)) -> rule5)) -> rule4))]
The cat chases the lion.
("cat" "chases" "lion" "+")
triple1
The cat does not chase the rabbit.
("cat" "chases" "rabbit" "-")
triple2
The cat eats the rabbit.
("cat" "eats" "rabbit" "+")
triple3
The cat visits the dog.
("cat" "visits" "dog" "+")
triple4
The dog chases the cat.
("dog" "chases" "cat" "+")
triple5
The dog chases the rabbit.
("dog" "chases" "rabbit" "+")
triple6
The dog is young.
("dog" "is" "young" "+")
triple7
The lion does not chase the cat.
("lion" "chases" "cat" "-")
triple8
The lion is cold.
("lion" "is" "cold" "+")
triple9
The lion is young.
("lion" "is" "young" "+")
triple10
The lion visits the cat.
("lion" "visits" "cat" "+")
triple11
The rabbit chases the cat.
("rabbit" "chases" "cat" "+")
triple12
The rabbit is young.
("rabbit" "is" "young" "+")
triple13
The rabbit visits the cat.
("rabbit" "visits" "cat" "+")
triple14
The cat eats the dog.
("cat" "eats" "dog" "+")
((triple4) -> (rule2 % int1))
The cat eats the dog.
("cat" "eats" "dog" "+")
int1
The dog is kind.
("dog" "is" "kind" "+")
((((triple4) -> (rule2 % int2))) -> (rule1 % int1))
The dog is kind.
("dog" "is" "kind" "+")
int1
The cat eats the dog.
("cat" "eats" "dog" "+")
int2
The dog is big.
("dog" "is" "big" "+")
((((((triple4) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
The dog is big.
("dog" "is" "big" "+")
int1
The dog is kind.
("dog" "is" "kind" "+")
int2
The cat eats the dog.
("cat" "eats" "dog" "+")
int3
The dog visits the dog.
("dog" "visits" "dog" "+")
((((((((triple4) -> (rule2 % int4))) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
The dog visits the dog.
("dog" "visits" "dog" "+")
int1
The dog is big.
("dog" "is" "big" "+")
int2
The dog is kind.
("dog" "is" "kind" "+")
int3
The cat eats the dog.
("cat" "eats" "dog" "+")
int4
The dog eats the dog.
("dog" "eats" "dog" "+")
((((((((((triple4) -> (rule2 % int5))) -> (rule1 % int4))) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The dog eats the dog.
("dog" "eats" "dog" "+")
int1
The dog visits the dog.
("dog" "visits" "dog" "+")
int2
The dog is big.
("dog" "is" "big" "+")
int3
The dog is kind.
("dog" "is" "kind" "+")
int4
The cat eats the dog.
("cat" "eats" "dog" "+")
int5
The dog is green.
("dog" "is" "green" "+")
((((((((((triple4) -> (rule2 % int5))) -> (rule1 % int4))) -> (rule5 % int3))) -> (rule3 % int2)) ((((((triple4) -> (rule2 % int5))) -> (rule1 % int4))) -> (rule5 % int3))) -> (rule4 % int1))
The dog is green.
("dog" "is" "green" "+")
int1
The dog visits the dog.
("dog" "visits" "dog" "+")
int2
The dog is big.
("dog" "is" "big" "+")
int3
The dog is kind.
("dog" "is" "kind" "+")
int4
The cat eats the dog.
("cat" "eats" "dog" "+")
int5