The dog likes the lion. The lion needs the dog. If something likes the dog then it is cold. If the dog likes the lion and the dog sees the lion then the dog needs the lion. If something likes the lion and it needs the lion then the lion is green. If something needs the lion and it sees the lion then the lion likes the dog. If the lion needs the dog then the lion sees the dog. If the lion sees the dog and the dog likes the lion then the dog needs the lion.
The dog likes the lion.
("dog" "likes" "lion" "+")
The lion needs the dog.
("lion" "needs" "dog" "+")
If something likes the dog then it is cold.
((("something" "likes" "dog" "+")) -> ("something" "is" "cold" "+"))
If the dog likes the lion and the dog sees the lion then the dog needs the lion.
((("dog" "likes" "lion" "+") ("dog" "sees" "lion" "+")) -> ("dog" "needs" "lion" "+"))
If something likes the lion and it needs the lion then the lion is green.
((("something" "likes" "lion" "+") ("something" "needs" "lion" "+")) -> ("lion" "is" "green" "+"))
If something needs the lion and it sees the lion then the lion likes the dog.
((("something" "needs" "lion" "+") ("something" "sees" "lion" "+")) -> ("lion" "likes" "dog" "+"))
If the lion needs the dog then the lion sees the dog.
((("lion" "needs" "dog" "+")) -> ("lion" "sees" "dog" "+"))
If the lion sees the dog and the dog likes the lion then the dog needs the lion.
((("lion" "sees" "dog" "+") ("dog" "likes" "lion" "+")) -> ("dog" "needs" "lion" "+"))
The dog likes the lion.
True
1
proof
[(triple1)]
("dog" "likes" "lion" "+")
triple1
The lion does not need the dog.
False
1
inv-proof
[(triple2)]
("lion" "needs" "dog" "-")
triple2
The lion sees the dog.
True
2
proof
[(((triple2) -> rule5))]
("lion" "sees" "dog" "+")
((triple2) -> (rule5 % int1))
The lion sees the dog.
("lion" "sees" "dog" "+")
int1
The lion does not see the dog.
False
2
inv-proof
[(((triple2) -> rule5))]
("lion" "sees" "dog" "-")
((triple2) -> (rule5 % int1))
The lion sees the dog.
("lion" "sees" "dog" "+")
int1
The dog needs the lion.
True
4
proof
[(((((triple2) -> rule5) triple1) -> rule6))]
("dog" "needs" "lion" "+")
((((triple2) -> (rule5 % int2)) triple1) -> (rule6 % int1))
The dog needs the lion.
("dog" "needs" "lion" "+")
int1
The lion sees the dog.
("lion" "sees" "dog" "+")
int2
The dog does not need the lion.
False
4
inv-proof
[(((((triple2) -> rule5) triple1) -> rule6))]
("dog" "needs" "lion" "-")
((((triple2) -> (rule5 % int2)) triple1) -> (rule6 % int1))
The dog needs the lion.
("dog" "needs" "lion" "+")
int1
The lion sees the dog.
("lion" "sees" "dog" "+")
int2
The lion is green.
True
6
proof
[(((triple1 ((((triple2) -> rule5) triple1) -> rule6)) -> rule3))]
("lion" "is" "green" "+")
((triple1 ((((triple2) -> (rule5 % int3)) triple1) -> (rule6 % int2))) -> (rule3 % int1))
The lion is green.
("lion" "is" "green" "+")
int1
The dog needs the lion.
("dog" "needs" "lion" "+")
int2
The lion sees the dog.
("lion" "sees" "dog" "+")
int3
The lion is not green.
False
6
inv-proof
[(((triple1 ((((triple2) -> rule5) triple1) -> rule6)) -> rule3))]
("lion" "is" "green" "-")
((triple1 ((((triple2) -> (rule5 % int3)) triple1) -> (rule6 % int2))) -> (rule3 % int1))
The lion is green.
("lion" "is" "green" "+")
int1
The dog needs the lion.
("dog" "needs" "lion" "+")
int2
The lion sees the dog.
("lion" "sees" "dog" "+")
int3
The lion does not like the dog.
Unknown
inv-rconc
[@1: The lion likes the dog.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("lion" "likes" "dog" "-")
The dog is cold.
Unknown
rconc
[@1: The dog is cold.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("dog" "is" "cold" "+")
The lion is not cold.
Unknown
inv-rconc
[@2: The lion is cold.[CWA. Example of deepest failure = (rule1 <- rule4 <- FAIL)]]
("lion" "is" "cold" "-")
The lion is blue.
Unknown
random
[@0: The lion is blue.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "blue" "+")
The lion is not red.
Unknown
inv-random
[@0: The lion is red.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "red" "-")
The dog needs the dog.
Unknown
random
[@0: The dog needs the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "needs" "dog" "+")
The dog does not see the lion.
Unknown
inv-random
[@0: The dog sees the lion.[CWA. Example of deepest failure = (FAIL)]]
("dog" "sees" "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 dog likes the lion.[(triple1)] The lion needs the dog.[(triple2)] @1: The lion sees the dog.[(((triple2) -> rule5))] @2: The dog needs the lion.[(((((triple2) -> rule5) triple1) -> rule6))] @3: The lion is green.[(((triple1 ((((triple2) -> rule5) triple1) -> rule6)) -> rule3))]
The dog likes the lion.
("dog" "likes" "lion" "+")
triple1
The lion needs the dog.
("lion" "needs" "dog" "+")
triple2
The lion sees the dog.
("lion" "sees" "dog" "+")
((triple2) -> (rule5 % int1))
The lion sees the dog.
("lion" "sees" "dog" "+")
int1
The dog needs the lion.
("dog" "needs" "lion" "+")
((((triple2) -> (rule5 % int2)) triple1) -> (rule6 % int1))
The dog needs the lion.
("dog" "needs" "lion" "+")
int1
The lion sees the dog.
("lion" "sees" "dog" "+")
int2
The lion is green.
("lion" "is" "green" "+")
((triple1 ((((triple2) -> (rule5 % int3)) triple1) -> (rule6 % int2))) -> (rule3 % int1))
The lion is green.
("lion" "is" "green" "+")
int1
The dog needs the lion.
("dog" "needs" "lion" "+")
int2
The lion sees the dog.
("lion" "sees" "dog" "+")
int3