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