The cat is blue. The cat is nice. The cat likes the dog. The cat likes the lion. The cat sees the dog. The cat sees the lion. The dog is nice. The dog likes the cat. The dog sees the cat. The lion sees the dog. Green, nice things are rough. If the lion likes the cat then the cat sees the dog. If the cat likes the dog then the cat visits the lion. If something is nice and it visits the lion then the lion is red. If something visits the cat then it visits the dog. If something sees the cat then the cat is nice. If something visits the dog then the dog visits the lion. If something sees the dog then the dog visits the cat.
The cat is blue.
("cat" "is" "blue" "+")
The cat is nice.
("cat" "is" "nice" "+")
The cat likes the dog.
("cat" "likes" "dog" "+")
The cat likes the lion.
("cat" "likes" "lion" "+")
The cat sees the dog.
("cat" "sees" "dog" "+")
The cat sees the lion.
("cat" "sees" "lion" "+")
The dog is nice.
("dog" "is" "nice" "+")
The dog likes the cat.
("dog" "likes" "cat" "+")
The dog sees the cat.
("dog" "sees" "cat" "+")
The lion sees the dog.
("lion" "sees" "dog" "+")
Green, nice things are rough.
((("something" "is" "green" "+") ("something" "is" "nice" "+")) -> ("something" "is" "rough" "+"))
If the lion likes the cat then the cat sees the dog.
((("lion" "likes" "cat" "+")) -> ("cat" "sees" "dog" "+"))
If the cat likes the dog then the cat visits the lion.
((("cat" "likes" "dog" "+")) -> ("cat" "visits" "lion" "+"))
If something is nice and it visits the lion then the lion is red.
((("something" "is" "nice" "+") ("something" "visits" "lion" "+")) -> ("lion" "is" "red" "+"))
If something visits the cat then it visits the dog.
((("something" "visits" "cat" "+")) -> ("something" "visits" "dog" "+"))
If something sees the cat then the cat is nice.
((("something" "sees" "cat" "+")) -> ("cat" "is" "nice" "+"))
If something visits the dog then the dog visits the lion.
((("something" "visits" "dog" "+")) -> ("dog" "visits" "lion" "+"))
If something sees the dog then the dog visits the cat.
((("something" "sees" "dog" "+")) -> ("dog" "visits" "cat" "+"))
The cat sees the lion.
True
1
proof
[(triple6)]
("cat" "sees" "lion" "+")
triple6
The dog does not see the cat.
False
1
inv-proof
[(triple9)]
("dog" "sees" "cat" "-")
triple9
The dog visits the cat.
True
2
proof
[(((triple10) -> rule8) OR ((triple5) -> rule8))]
("dog" "visits" "cat" "+")
((triple10) -> (rule8 % int1))
The dog visits the cat.
("dog" "visits" "cat" "+")
int1
((triple5) -> (rule8 % int1))
The dog visits the cat.
("dog" "visits" "cat" "+")
int1
The cat does not visit the lion.
False
2
inv-proof
[(((triple3) -> rule3))]
("cat" "visits" "lion" "-")
((triple3) -> (rule3 % int1))
The cat visits the lion.
("cat" "visits" "lion" "+")
int1
The dog visits the dog.
True
3
proof
[(((((triple10) -> rule8)) -> rule5) OR ((((triple5) -> rule8)) -> rule5))]
("dog" "visits" "dog" "+")
((((triple10) -> (rule8 % int2))) -> (rule5 % int1))
The dog visits the dog.
("dog" "visits" "dog" "+")
int1
The dog visits the cat.
("dog" "visits" "cat" "+")
int2
((((triple5) -> (rule8 % int2))) -> (rule5 % int1))
The dog visits the dog.
("dog" "visits" "dog" "+")
int1
The dog visits the cat.
("dog" "visits" "cat" "+")
int2
The dog does not visit the dog.
False
3
inv-proof
[(((((triple10) -> rule8)) -> rule5) OR ((((triple5) -> rule8)) -> rule5))]
("dog" "visits" "dog" "-")
((((triple10) -> (rule8 % int2))) -> (rule5 % int1))
The dog visits the dog.
("dog" "visits" "dog" "+")
int1
The dog visits the cat.
("dog" "visits" "cat" "+")
int2
((((triple5) -> (rule8 % int2))) -> (rule5 % int1))
The dog visits the dog.
("dog" "visits" "dog" "+")
int1
The dog visits the cat.
("dog" "visits" "cat" "+")
int2
The dog visits the lion.
True
4
proof
[(((((((triple10) -> rule8)) -> rule5)) -> rule7) OR ((((((triple5) -> rule8)) -> rule5)) -> rule7))]
("dog" "visits" "lion" "+")
((((((triple10) -> (rule8 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
The dog visits the lion.
("dog" "visits" "lion" "+")
int1
The dog visits the dog.
("dog" "visits" "dog" "+")
int2
The dog visits the cat.
("dog" "visits" "cat" "+")
int3
((((((triple5) -> (rule8 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
The dog visits the lion.
("dog" "visits" "lion" "+")
int1
The dog visits the dog.
("dog" "visits" "dog" "+")
int2
The dog visits the cat.
("dog" "visits" "cat" "+")
int3
The dog does not visit the lion.
False
4
inv-proof
[(((((((triple10) -> rule8)) -> rule5)) -> rule7) OR ((((((triple5) -> rule8)) -> rule5)) -> rule7))]
("dog" "visits" "lion" "-")
((((((triple10) -> (rule8 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
The dog visits the lion.
("dog" "visits" "lion" "+")
int1
The dog visits the dog.
("dog" "visits" "dog" "+")
int2
The dog visits the cat.
("dog" "visits" "cat" "+")
int3
((((((triple5) -> (rule8 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
The dog visits the lion.
("dog" "visits" "lion" "+")
int1
The dog visits the dog.
("dog" "visits" "dog" "+")
int2
The dog visits the cat.
("dog" "visits" "cat" "+")
int3
The lion does not visit the dog.
Unknown
inv-rconc
[@1: The lion visits the dog.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("lion" "visits" "dog" "-")
The cat visits the dog.
Unknown
rconc
[@1: The cat visits the dog.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("cat" "visits" "dog" "+")
The lion is not rough.
Unknown
inv-rconc
[@1: The lion is rough.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("lion" "is" "rough" "-")
The cat is rough.
Unknown
rconc
[@1: The cat is rough.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "is" "rough" "+")
The dog does not see the dog.
Unknown
inv-random
[@0: The dog sees the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "sees" "dog" "-")
The lion sees the lion.
Unknown
random
[@0: The lion sees the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "lion" "+")
The dog does not like the lion.
Unknown
inv-random
[@0: The dog likes the lion.[CWA. Example of deepest failure = (FAIL)]]
("dog" "likes" "lion" "-")
The lion likes the lion.
Unknown
random
[@0: The lion likes the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "likes" "lion" "+")
@0: The cat is blue.[(triple1)] The cat is nice.[(triple2 OR ((triple9) -> rule6))] The cat likes the dog.[(triple3)] The cat likes the lion.[(triple4)] The cat sees the dog.[(triple5)] The cat sees the lion.[(triple6)] The dog is nice.[(triple7)] The dog likes the cat.[(triple8)] The dog sees the cat.[(triple9)] The lion sees the dog.[(triple10)] @1: The cat visits the lion.[(((triple3) -> rule3))] The dog visits the cat.[(((triple10) -> rule8) OR ((triple5) -> rule8))] @2: The dog visits the dog.[(((((triple10) -> rule8)) -> rule5) OR ((((triple5) -> rule8)) -> rule5))] The lion is red.[(((triple2 ((triple3) -> rule3)) -> rule4) OR ((((triple9) -> rule6) ((triple3) -> rule3)) -> rule4) OR ((triple7 ((((((triple10) -> rule8)) -> rule5)) -> rule7)) -> rule4) OR ((triple7 ((((((triple5) -> rule8)) -> rule5)) -> rule7)) -> rule4))] @3: The dog visits the lion.[(((((((triple10) -> rule8)) -> rule5)) -> rule7) OR ((((((triple5) -> rule8)) -> rule5)) -> rule7))]
The cat is blue.
("cat" "is" "blue" "+")
triple1
The cat is nice.
("cat" "is" "nice" "+")
triple2
((triple9) -> (rule6 % int1))
The cat is nice.
("cat" "is" "nice" "+")
int1
The cat likes the dog.
("cat" "likes" "dog" "+")
triple3
The cat likes the lion.
("cat" "likes" "lion" "+")
triple4
The cat sees the dog.
("cat" "sees" "dog" "+")
triple5
The cat sees the lion.
("cat" "sees" "lion" "+")
triple6
The dog is nice.
("dog" "is" "nice" "+")
triple7
The dog likes the cat.
("dog" "likes" "cat" "+")
triple8
The dog sees the cat.
("dog" "sees" "cat" "+")
triple9
The lion sees the dog.
("lion" "sees" "dog" "+")
triple10
The cat visits the lion.
("cat" "visits" "lion" "+")
((triple3) -> (rule3 % int1))
The cat visits the lion.
("cat" "visits" "lion" "+")
int1
The dog visits the cat.
("dog" "visits" "cat" "+")
((triple10) -> (rule8 % int1))
The dog visits the cat.
("dog" "visits" "cat" "+")
int1
((triple5) -> (rule8 % int1))
The dog visits the cat.
("dog" "visits" "cat" "+")
int1
The dog visits the dog.
("dog" "visits" "dog" "+")
((((triple10) -> (rule8 % int2))) -> (rule5 % int1))
The dog visits the dog.
("dog" "visits" "dog" "+")
int1
The dog visits the cat.
("dog" "visits" "cat" "+")
int2
((((triple5) -> (rule8 % int2))) -> (rule5 % int1))
The dog visits the dog.
("dog" "visits" "dog" "+")
int1
The dog visits the cat.
("dog" "visits" "cat" "+")
int2
The lion is red.
("lion" "is" "red" "+")
((triple2 ((triple3) -> (rule3 % int2))) -> (rule4 % int1))
The lion is red.
("lion" "is" "red" "+")
int1
The cat visits the lion.
("cat" "visits" "lion" "+")
int2
((((triple9) -> (rule6 % int3)) ((triple3) -> (rule3 % int2))) -> (rule4 % int1))
The lion is red.
("lion" "is" "red" "+")
int1
The cat visits the lion.
("cat" "visits" "lion" "+")
int2
The cat is nice.
("cat" "is" "nice" "+")
int3
((triple7 ((((((triple10) -> (rule8 % int4))) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule4 % int1))
The lion is red.
("lion" "is" "red" "+")
int1
The dog visits the lion.
("dog" "visits" "lion" "+")
int2
The dog visits the dog.
("dog" "visits" "dog" "+")
int3
The dog visits the cat.
("dog" "visits" "cat" "+")
int4
((triple7 ((((((triple5) -> (rule8 % int4))) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule4 % int1))
The lion is red.
("lion" "is" "red" "+")
int1
The dog visits the lion.
("dog" "visits" "lion" "+")
int2
The dog visits the dog.
("dog" "visits" "dog" "+")
int3
The dog visits the cat.
("dog" "visits" "cat" "+")
int4
The dog visits the lion.
("dog" "visits" "lion" "+")
((((((triple10) -> (rule8 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
The dog visits the lion.
("dog" "visits" "lion" "+")
int1
The dog visits the dog.
("dog" "visits" "dog" "+")
int2
The dog visits the cat.
("dog" "visits" "cat" "+")
int3
((((((triple5) -> (rule8 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
The dog visits the lion.
("dog" "visits" "lion" "+")
int1
The dog visits the dog.
("dog" "visits" "dog" "+")
int2
The dog visits the cat.
("dog" "visits" "cat" "+")
int3