The dog is blue. The dog is cold. The dog is red. The dog needs the lion. The dog does not see the lion. The dog visits the lion. The lion is cold. The lion does not need the dog. The lion sees the dog. The lion visits the dog. All red things are kind. If something visits the lion then the lion sees the dog. If something visits the lion then the lion is kind. If something sees the dog then it visits the dog. If something sees the lion then it sees the dog. If something needs the dog and the dog is not kind then it sees the dog. If the lion sees the dog and the lion is red then the lion is not blue. If something is kind and it needs the lion then the lion is blue.
The dog is blue.
("dog" "is" "blue" "+")
The dog is cold.
("dog" "is" "cold" "+")
The dog is red.
("dog" "is" "red" "+")
The dog needs the lion.
("dog" "needs" "lion" "+")
The dog does not see the lion.
("dog" "sees" "lion" "-")
The dog visits the lion.
("dog" "visits" "lion" "+")
The lion is cold.
("lion" "is" "cold" "+")
The lion does not need the dog.
("lion" "needs" "dog" "-")
The lion sees the dog.
("lion" "sees" "dog" "+")
The lion visits the dog.
("lion" "visits" "dog" "+")
All red things are kind.
((("something" "is" "red" "+")) -> ("something" "is" "kind" "+"))
If something visits the lion then the lion sees the dog.
((("something" "visits" "lion" "+")) -> ("lion" "sees" "dog" "+"))
If something visits the lion then the lion is kind.
((("something" "visits" "lion" "+")) -> ("lion" "is" "kind" "+"))
If something sees the dog then it visits the dog.
((("something" "sees" "dog" "+")) -> ("something" "visits" "dog" "+"))
If something sees the lion then it sees the dog.
((("something" "sees" "lion" "+")) -> ("something" "sees" "dog" "+"))
If something needs the dog and the dog is not kind then it sees the dog.
((("something" "needs" "dog" "+") ("dog" "is" "kind" "~")) -> ("something" "sees" "dog" "+"))
If the lion sees the dog and the lion is red then the lion is not blue.
((("lion" "sees" "dog" "+") ("lion" "is" "red" "+")) -> ("lion" "is" "blue" "-"))
If something is kind and it needs the lion then the lion is blue.
((("something" "is" "kind" "+") ("something" "needs" "lion" "+")) -> ("lion" "is" "blue" "+"))
The dog is blue.
True
1
proof
[(triple1)]
("dog" "is" "blue" "+")
triple1
The dog does not need the lion.
False
1
inv-proof
[(triple4)]
("dog" "needs" "lion" "-")
triple4
The dog is kind.
True
2
proof
[(((triple3) -> rule1))]
("dog" "is" "kind" "+")
((triple3) -> (rule1 % int1))
The dog is kind.
("dog" "is" "kind" "+")
int1
The dog is not kind.
False
2
inv-proof
[(((triple3) -> rule1))]
("dog" "is" "kind" "-")
((triple3) -> (rule1 % int1))
The dog is kind.
("dog" "is" "kind" "+")
int1
The lion is blue.
True
4
proof
[(((((triple3) -> rule1) triple4) -> rule8))]
("lion" "is" "blue" "+")
((((triple3) -> (rule1 % int2)) triple4) -> (rule8 % int1))
The lion is blue.
("lion" "is" "blue" "+")
int1
The dog is kind.
("dog" "is" "kind" "+")
int2
The lion is not blue.
False
4
inv-proof
[(((((triple3) -> rule1) triple4) -> rule8))]
("lion" "is" "blue" "-")
((((triple3) -> (rule1 % int2)) triple4) -> (rule8 % int1))
The lion is blue.
("lion" "is" "blue" "+")
int1
The dog is kind.
("dog" "is" "kind" "+")
int2
The dog does not visit the dog.
Unknown
inv-rconc
[@2: The dog visits the dog.[CWA. Example of deepest failure = (rule4 <- rule5 <- FAIL)]]
("dog" "visits" "dog" "-")
The dog sees the dog.
Unknown
rconc
[@1: The dog sees the dog.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("dog" "sees" "dog" "+")
The lion does not need the lion.
Unknown
inv-random
[@0: The lion needs the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "needs" "lion" "-")
The lion is nice.
Unknown
random
[@0: The lion is nice.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "nice" "+")
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 is nice.
Unknown
random
[@0: The dog is nice.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "nice" "+")
@0: The dog does not see the lion.[(triple5)] The dog is blue.[(triple1)] The dog is cold.[(triple2)] The dog is red.[(triple3)] The dog needs the lion.[(triple4)] The dog visits the lion.[(triple6)] The lion does not need the dog.[(triple8)] The lion is cold.[(triple7)] The lion sees the dog.[(triple9 OR ((triple6) -> rule2))] The lion visits the dog.[(triple10 OR ((triple9) -> rule4) OR ((((triple6) -> rule2)) -> rule4))] @1: The dog is kind.[(((triple3) -> rule1))] The lion is kind.[(((triple6) -> rule3))] @2: The lion is blue.[(((((triple3) -> rule1) triple4) -> rule8))]
The dog does not see the lion.
("dog" "sees" "lion" "-")
triple5
The dog is blue.
("dog" "is" "blue" "+")
triple1
The dog is cold.
("dog" "is" "cold" "+")
triple2
The dog is red.
("dog" "is" "red" "+")
triple3
The dog needs the lion.
("dog" "needs" "lion" "+")
triple4
The dog visits the lion.
("dog" "visits" "lion" "+")
triple6
The lion does not need the dog.
("lion" "needs" "dog" "-")
triple8
The lion is cold.
("lion" "is" "cold" "+")
triple7
The lion sees the dog.
("lion" "sees" "dog" "+")
triple9
((triple6) -> (rule2 % int1))
The lion sees the dog.
("lion" "sees" "dog" "+")
int1
The lion visits the dog.
("lion" "visits" "dog" "+")
triple10
((triple9) -> (rule4 % int1))
The lion visits the dog.
("lion" "visits" "dog" "+")
int1
((((triple6) -> (rule2 % int2))) -> (rule4 % int1))
The lion visits the dog.
("lion" "visits" "dog" "+")
int1
The lion sees the dog.
("lion" "sees" "dog" "+")
int2
The dog is kind.
("dog" "is" "kind" "+")
((triple3) -> (rule1 % int1))
The dog is kind.
("dog" "is" "kind" "+")
int1
The lion is kind.
("lion" "is" "kind" "+")
((triple6) -> (rule3 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
The lion is blue.
("lion" "is" "blue" "+")
((((triple3) -> (rule1 % int2)) triple4) -> (rule8 % int1))
The lion is blue.
("lion" "is" "blue" "+")
int1
The dog is kind.
("dog" "is" "kind" "+")
int2