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