The cat likes the dog. The cat likes the lion. The cat needs the lion. The cat sees the dog. The cat sees the lion. The dog needs the lion. The lion needs the cat. If something sees the dog then the dog needs the cat. If something needs the cat then the cat is round. All rough things are red. If something likes the dog then it is rough. If something is cold and it sees the lion then the lion needs the dog. If something sees the lion then the lion likes the dog. If something sees the cat and the cat sees the lion then it is rough. If the dog is kind and the dog is rough then the dog is round.
The cat likes the dog.
("cat" "likes" "dog" "+")
The cat likes the lion.
("cat" "likes" "lion" "+")
The cat needs the lion.
("cat" "needs" "lion" "+")
The cat sees the dog.
("cat" "sees" "dog" "+")
The cat sees the lion.
("cat" "sees" "lion" "+")
The dog needs the lion.
("dog" "needs" "lion" "+")
The lion needs the cat.
("lion" "needs" "cat" "+")
If something sees the dog then the dog needs the cat.
((("something" "sees" "dog" "+")) -> ("dog" "needs" "cat" "+"))
If something needs the cat then the cat is round.
((("something" "needs" "cat" "+")) -> ("cat" "is" "round" "+"))
All rough things are red.
((("something" "is" "rough" "+")) -> ("something" "is" "red" "+"))
If something likes the dog then it is rough.
((("something" "likes" "dog" "+")) -> ("something" "is" "rough" "+"))
If something is cold and it sees the lion then the lion needs the dog.
((("something" "is" "cold" "+") ("something" "sees" "lion" "+")) -> ("lion" "needs" "dog" "+"))
If something sees the lion then the lion likes the dog.
((("something" "sees" "lion" "+")) -> ("lion" "likes" "dog" "+"))
If something sees the cat and the cat sees the lion then it is rough.
((("something" "sees" "cat" "+") ("cat" "sees" "lion" "+")) -> ("something" "is" "rough" "+"))
If the dog is kind and the dog is rough then the dog is round.
((("dog" "is" "kind" "+") ("dog" "is" "rough" "+")) -> ("dog" "is" "round" "+"))
The cat likes the lion.
True
1
proof
[(triple2)]
("cat" "likes" "lion" "+")
triple2
The cat does not like the dog.
False
1
inv-proof
[(triple1)]
("cat" "likes" "dog" "-")
triple1
The dog needs the cat.
True
2
proof
[(((triple4) -> rule1))]
("dog" "needs" "cat" "+")
((triple4) -> (rule1 % int1))
The dog needs the cat.
("dog" "needs" "cat" "+")
int1
The dog does not need the cat.
False
2
inv-proof
[(((triple4) -> rule1))]
("dog" "needs" "cat" "-")
((triple4) -> (rule1 % int1))
The dog needs the cat.
("dog" "needs" "cat" "+")
int1
The lion is rough.
True
3
proof
[(((((triple5) -> rule6)) -> rule4))]
("lion" "is" "rough" "+")
((((triple5) -> (rule6 % int2))) -> (rule4 % int1))
The lion is rough.
("lion" "is" "rough" "+")
int1
The lion likes the dog.
("lion" "likes" "dog" "+")
int2
The cat is not red.
False
3
inv-proof
[(((((triple1) -> rule4)) -> rule3))]
("cat" "is" "red" "-")
((((triple1) -> (rule4 % int2))) -> (rule3 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The cat is rough.
("cat" "is" "rough" "+")
int2
The lion is red.
True
4
proof
[(((((((triple5) -> rule6)) -> rule4)) -> rule3))]
("lion" "is" "red" "+")
((((((triple5) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
The lion is red.
("lion" "is" "red" "+")
int1
The lion is rough.
("lion" "is" "rough" "+")
int2
The lion likes the dog.
("lion" "likes" "dog" "+")
int3
The lion is not red.
False
4
inv-proof
[(((((((triple5) -> rule6)) -> rule4)) -> rule3))]
("lion" "is" "red" "-")
((((((triple5) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
The lion is red.
("lion" "is" "red" "+")
int1
The lion is rough.
("lion" "is" "rough" "+")
int2
The lion likes the dog.
("lion" "likes" "dog" "+")
int3
The dog is not red.
Unknown
inv-rconc
[@2: The dog is red.[CWA. Example of deepest failure = (rule3 <- rule4 <- FAIL)]]
("dog" "is" "red" "-")
The dog is round.
Unknown
rconc
[@1: The dog is round.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("dog" "is" "round" "+")
The dog is not rough.
Unknown
inv-rconc
[@1: The dog is rough.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("dog" "is" "rough" "-")
The lion needs the dog.
Unknown
rconc
[@1: The lion needs the dog.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("lion" "needs" "dog" "+")
The dog is not kind.
Unknown
inv-random
[@0: The dog is kind.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "kind" "-")
The lion is round.
Unknown
random
[@0: The lion is round.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "round" "+")
The cat does not see the cat.
Unknown
inv-random
[@0: The cat sees the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "sees" "cat" "-")
The lion needs the lion.
Unknown
random
[@0: The lion needs the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "needs" "lion" "+")
@0: The cat likes the dog.[(triple1)] The cat likes the lion.[(triple2)] The cat needs the lion.[(triple3)] The cat sees the dog.[(triple4)] The cat sees the lion.[(triple5)] The dog needs the lion.[(triple6)] The lion needs the cat.[(triple7)] @1: The cat is rough.[(((triple1) -> rule4))] The cat is round.[(((triple7) -> rule2) OR ((((triple4) -> rule1)) -> rule2))] The dog needs the cat.[(((triple4) -> rule1))] The lion likes the dog.[(((triple5) -> rule6))] @2: The cat is red.[(((((triple1) -> rule4)) -> rule3))] The lion is rough.[(((((triple5) -> rule6)) -> rule4))] @3: The lion is red.[(((((((triple5) -> rule6)) -> rule4)) -> rule3))]
The cat likes the dog.
("cat" "likes" "dog" "+")
triple1
The cat likes the lion.
("cat" "likes" "lion" "+")
triple2
The cat needs the lion.
("cat" "needs" "lion" "+")
triple3
The cat sees the dog.
("cat" "sees" "dog" "+")
triple4
The cat sees the lion.
("cat" "sees" "lion" "+")
triple5
The dog needs the lion.
("dog" "needs" "lion" "+")
triple6
The lion needs the cat.
("lion" "needs" "cat" "+")
triple7
The cat is rough.
("cat" "is" "rough" "+")
((triple1) -> (rule4 % int1))
The cat is rough.
("cat" "is" "rough" "+")
int1
The cat is round.
("cat" "is" "round" "+")
((triple7) -> (rule2 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
((((triple4) -> (rule1 % int2))) -> (rule2 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
The dog needs the cat.
("dog" "needs" "cat" "+")
int2
The dog needs the cat.
("dog" "needs" "cat" "+")
((triple4) -> (rule1 % int1))
The dog needs the cat.
("dog" "needs" "cat" "+")
int1
The lion likes the dog.
("lion" "likes" "dog" "+")
((triple5) -> (rule6 % int1))
The lion likes the dog.
("lion" "likes" "dog" "+")
int1
The cat is red.
("cat" "is" "red" "+")
((((triple1) -> (rule4 % int2))) -> (rule3 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The cat is rough.
("cat" "is" "rough" "+")
int2
The lion is rough.
("lion" "is" "rough" "+")
((((triple5) -> (rule6 % int2))) -> (rule4 % int1))
The lion is rough.
("lion" "is" "rough" "+")
int1
The lion likes the dog.
("lion" "likes" "dog" "+")
int2
The lion is red.
("lion" "is" "red" "+")
((((((triple5) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
The lion is red.
("lion" "is" "red" "+")
int1
The lion is rough.
("lion" "is" "rough" "+")
int2
The lion likes the dog.
("lion" "likes" "dog" "+")
int3