The cat chases the lion. The cat eats the dog. The dog chases the lion. The dog needs the cat. The lion chases the dog. The lion eats the dog. The lion is nice. If someone needs the dog then the dog is rough. If someone chases the cat and the cat eats the lion then they eat the lion. If someone chases the lion then the lion chases the dog. If someone chases the dog and they need the lion then they are red. If someone chases the dog then they eat the cat. If the lion is nice and the lion needs the cat then the lion needs the dog. If someone eats the cat then the cat needs the lion. If the lion is nice then the lion needs the cat.
The cat chases the lion.
("cat" "chases" "lion" "+")
The cat eats the dog.
("cat" "eats" "dog" "+")
The dog chases the lion.
("dog" "chases" "lion" "+")
The dog needs the cat.
("dog" "needs" "cat" "+")
The lion chases the dog.
("lion" "chases" "dog" "+")
The lion eats the dog.
("lion" "eats" "dog" "+")
The lion is nice.
("lion" "is" "nice" "+")
If someone needs the dog then the dog is rough.
((("someone" "needs" "dog" "+")) -> ("dog" "is" "rough" "+"))
If someone chases the cat and the cat eats the lion then they eat the lion.
((("someone" "chases" "cat" "+") ("cat" "eats" "lion" "+")) -> ("someone" "eats" "lion" "+"))
If someone chases the lion then the lion chases the dog.
((("someone" "chases" "lion" "+")) -> ("lion" "chases" "dog" "+"))
If someone chases the dog and they need the lion then they are red.
((("someone" "chases" "dog" "+") ("someone" "needs" "lion" "+")) -> ("someone" "is" "red" "+"))
If someone chases the dog then they eat the cat.
((("someone" "chases" "dog" "+")) -> ("someone" "eats" "cat" "+"))
If the lion is nice and the lion needs the cat then the lion needs the dog.
((("lion" "is" "nice" "+") ("lion" "needs" "cat" "+")) -> ("lion" "needs" "dog" "+"))
If someone eats the cat then the cat needs the lion.
((("someone" "eats" "cat" "+")) -> ("cat" "needs" "lion" "+"))
If the lion is nice then the lion needs the cat.
((("lion" "is" "nice" "+")) -> ("lion" "needs" "cat" "+"))
The cat chases the lion.
True
1
proof
[(triple1)]
("cat" "chases" "lion" "+")
triple1
The cat does not chase the lion.
False
1
inv-proof
[(triple1)]
("cat" "chases" "lion" "-")
triple1
The lion eats the cat.
True
2
proof
[(((triple5) -> rule5) OR ((((triple1) -> rule3)) -> rule5) OR ((((triple3) -> rule3)) -> rule5))]
("lion" "eats" "cat" "+")
((triple5) -> (rule5 % int1))
The lion eats the cat.
("lion" "eats" "cat" "+")
int1
((((triple1) -> (rule3 % int2))) -> (rule5 % int1))
The lion eats the cat.
("lion" "eats" "cat" "+")
int1
The lion chases the dog.
("lion" "chases" "dog" "+")
int2
((((triple3) -> (rule3 % int2))) -> (rule5 % int1))
The lion eats the cat.
("lion" "eats" "cat" "+")
int1
The lion chases the dog.
("lion" "chases" "dog" "+")
int2
The lion does not need the cat.
False
2
inv-proof
[(((triple7) -> rule8))]
("lion" "needs" "cat" "-")
((triple7) -> (rule8 % int1))
The lion needs the cat.
("lion" "needs" "cat" "+")
int1
The cat needs the lion.
True
3
proof
[(((((triple5) -> rule5)) -> rule7) OR ((((((triple1) -> rule3)) -> rule5)) -> rule7) OR ((((((triple3) -> rule3)) -> rule5)) -> rule7))]
("cat" "needs" "lion" "+")
((((triple5) -> (rule5 % int2))) -> (rule7 % int1))
The cat needs the lion.
("cat" "needs" "lion" "+")
int1
The lion eats the cat.
("lion" "eats" "cat" "+")
int2
((((((triple1) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
The cat needs the lion.
("cat" "needs" "lion" "+")
int1
The lion eats the cat.
("lion" "eats" "cat" "+")
int2
The lion chases the dog.
("lion" "chases" "dog" "+")
int3
((((((triple3) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
The cat needs the lion.
("cat" "needs" "lion" "+")
int1
The lion eats the cat.
("lion" "eats" "cat" "+")
int2
The lion chases the dog.
("lion" "chases" "dog" "+")
int3
The cat does not need the lion.
False
3
inv-proof
[(((((triple5) -> rule5)) -> rule7) OR ((((((triple1) -> rule3)) -> rule5)) -> rule7) OR ((((((triple3) -> rule3)) -> rule5)) -> rule7))]
("cat" "needs" "lion" "-")
((((triple5) -> (rule5 % int2))) -> (rule7 % int1))
The cat needs the lion.
("cat" "needs" "lion" "+")
int1
The lion eats the cat.
("lion" "eats" "cat" "+")
int2
((((((triple1) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
The cat needs the lion.
("cat" "needs" "lion" "+")
int1
The lion eats the cat.
("lion" "eats" "cat" "+")
int2
The lion chases the dog.
("lion" "chases" "dog" "+")
int3
((((((triple3) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
The cat needs the lion.
("cat" "needs" "lion" "+")
int1
The lion eats the cat.
("lion" "eats" "cat" "+")
int2
The lion chases the dog.
("lion" "chases" "dog" "+")
int3
The dog is rough.
True
5
proof
[(((((triple7 ((triple7) -> rule8)) -> rule6)) -> rule1))]
("dog" "is" "rough" "+")
((((triple7 ((triple7) -> (rule8 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
The dog is rough.
("dog" "is" "rough" "+")
int1
The lion needs the dog.
("lion" "needs" "dog" "+")
int2
The lion needs the cat.
("lion" "needs" "cat" "+")
int3
The dog is not rough.
False
5
inv-proof
[(((((triple7 ((triple7) -> rule8)) -> rule6)) -> rule1))]
("dog" "is" "rough" "-")
((((triple7 ((triple7) -> (rule8 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
The dog is rough.
("dog" "is" "rough" "+")
int1
The lion needs the dog.
("lion" "needs" "dog" "+")
int2
The lion needs the cat.
("lion" "needs" "cat" "+")
int3
The lion does not eat the lion.
Unknown
inv-rconc
[@1: The lion eats the lion.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("lion" "eats" "lion" "-")
The dog eats the lion.
Unknown
rconc
[@1: The dog eats the lion.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("dog" "eats" "lion" "+")
The lion is not red.
Unknown
inv-rconc
[@1: The lion is red.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("lion" "is" "red" "-")
The cat eats the lion.
Unknown
rconc
[@1: The cat eats the lion.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cat" "eats" "lion" "+")
The lion does not chase the lion.
Unknown
inv-random
[@0: The lion chases the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "lion" "-")
The cat chases the cat.
Unknown
random
[@0: The cat chases the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "chases" "cat" "+")
The dog does not need the lion.
Unknown
inv-random
[@0: The dog needs the lion.[CWA. Example of deepest failure = (FAIL)]]
("dog" "needs" "lion" "-")
The lion is young.
Unknown
random
[@0: The lion is young.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "young" "+")
@0: The cat chases the lion.[(triple1)] The cat eats the dog.[(triple2)] The dog chases the lion.[(triple3)] The dog needs the cat.[(triple4)] The lion chases the dog.[(triple5 OR ((triple1) -> rule3) OR ((triple3) -> rule3))] The lion eats the dog.[(triple6)] The lion is nice.[(triple7)] @1: The lion eats the cat.[(((triple5) -> rule5) OR ((((triple1) -> rule3)) -> rule5) OR ((((triple3) -> rule3)) -> rule5))] The lion needs the cat.[(((triple7) -> rule8))] @2: The cat needs the lion.[(((((triple5) -> rule5)) -> rule7) OR ((((((triple1) -> rule3)) -> rule5)) -> rule7) OR ((((((triple3) -> rule3)) -> rule5)) -> rule7))] The lion needs the dog.[(((triple7 ((triple7) -> rule8)) -> rule6))] @3: The dog is rough.[(((((triple7 ((triple7) -> rule8)) -> rule6)) -> rule1))]
The cat chases the lion.
("cat" "chases" "lion" "+")
triple1
The cat eats the dog.
("cat" "eats" "dog" "+")
triple2
The dog chases the lion.
("dog" "chases" "lion" "+")
triple3
The dog needs the cat.
("dog" "needs" "cat" "+")
triple4
The lion chases the dog.
("lion" "chases" "dog" "+")
triple5
((triple1) -> (rule3 % int1))
The lion chases the dog.
("lion" "chases" "dog" "+")
int1
((triple3) -> (rule3 % int1))
The lion chases the dog.
("lion" "chases" "dog" "+")
int1
The lion eats the dog.
("lion" "eats" "dog" "+")
triple6
The lion is nice.
("lion" "is" "nice" "+")
triple7
The lion eats the cat.
("lion" "eats" "cat" "+")
((triple5) -> (rule5 % int1))
The lion eats the cat.
("lion" "eats" "cat" "+")
int1
((((triple1) -> (rule3 % int2))) -> (rule5 % int1))
The lion eats the cat.
("lion" "eats" "cat" "+")
int1
The lion chases the dog.
("lion" "chases" "dog" "+")
int2
((((triple3) -> (rule3 % int2))) -> (rule5 % int1))
The lion eats the cat.
("lion" "eats" "cat" "+")
int1
The lion chases the dog.
("lion" "chases" "dog" "+")
int2
The lion needs the cat.
("lion" "needs" "cat" "+")
((triple7) -> (rule8 % int1))
The lion needs the cat.
("lion" "needs" "cat" "+")
int1
The cat needs the lion.
("cat" "needs" "lion" "+")
((((triple5) -> (rule5 % int2))) -> (rule7 % int1))
The cat needs the lion.
("cat" "needs" "lion" "+")
int1
The lion eats the cat.
("lion" "eats" "cat" "+")
int2
((((((triple1) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
The cat needs the lion.
("cat" "needs" "lion" "+")
int1
The lion eats the cat.
("lion" "eats" "cat" "+")
int2
The lion chases the dog.
("lion" "chases" "dog" "+")
int3
((((((triple3) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
The cat needs the lion.
("cat" "needs" "lion" "+")
int1
The lion eats the cat.
("lion" "eats" "cat" "+")
int2
The lion chases the dog.
("lion" "chases" "dog" "+")
int3
The lion needs the dog.
("lion" "needs" "dog" "+")
((triple7 ((triple7) -> (rule8 % int2))) -> (rule6 % int1))
The lion needs the dog.
("lion" "needs" "dog" "+")
int1
The lion needs the cat.
("lion" "needs" "cat" "+")
int2
The dog is rough.
("dog" "is" "rough" "+")
((((triple7 ((triple7) -> (rule8 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
The dog is rough.
("dog" "is" "rough" "+")
int1
The lion needs the dog.
("lion" "needs" "dog" "+")
int2
The lion needs the cat.
("lion" "needs" "cat" "+")
int3