The dog is big. The dog is cold. The dog needs the lion. The dog needs the rabbit. The dog sees the lion. The dog sees the rabbit. The lion is cold. The lion needs the dog. The lion sees the rabbit. The rabbit is rough. If the dog sees the lion then the dog likes the lion. If something likes the rabbit and the rabbit is young then the rabbit likes the lion. If the lion likes the dog then the lion needs the rabbit. If the dog likes the rabbit then the rabbit likes the lion. If something likes the lion then it sees the dog. If something sees the dog then the dog is rough.
The dog is big.
("dog" "is" "big" "+")
The dog is cold.
("dog" "is" "cold" "+")
The dog needs the lion.
("dog" "needs" "lion" "+")
The dog needs the rabbit.
("dog" "needs" "rabbit" "+")
The dog sees the lion.
("dog" "sees" "lion" "+")
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
The lion is cold.
("lion" "is" "cold" "+")
The lion needs the dog.
("lion" "needs" "dog" "+")
The lion sees the rabbit.
("lion" "sees" "rabbit" "+")
The rabbit is rough.
("rabbit" "is" "rough" "+")
If the dog sees the lion then the dog likes the lion.
((("dog" "sees" "lion" "+")) -> ("dog" "likes" "lion" "+"))
If something likes the rabbit and the rabbit is young then the rabbit likes the lion.
((("something" "likes" "rabbit" "+") ("rabbit" "is" "young" "+")) -> ("rabbit" "likes" "lion" "+"))
If the lion likes the dog then the lion needs the rabbit.
((("lion" "likes" "dog" "+")) -> ("lion" "needs" "rabbit" "+"))
If the dog likes the rabbit then the rabbit likes the lion.
((("dog" "likes" "rabbit" "+")) -> ("rabbit" "likes" "lion" "+"))
If something likes the lion then it sees the dog.
((("something" "likes" "lion" "+")) -> ("something" "sees" "dog" "+"))
If something sees the dog then the dog is rough.
((("something" "sees" "dog" "+")) -> ("dog" "is" "rough" "+"))
The dog needs the rabbit.
True
1
proof
[(triple4)]
("dog" "needs" "rabbit" "+")
triple4
The lion does not see the rabbit.
False
1
inv-proof
[(triple9)]
("lion" "sees" "rabbit" "-")
triple9
The dog likes the lion.
True
2
proof
[(((triple5) -> rule1))]
("dog" "likes" "lion" "+")
((triple5) -> (rule1 % int1))
The dog likes the lion.
("dog" "likes" "lion" "+")
int1
The dog does not like the lion.
False
2
inv-proof
[(((triple5) -> rule1))]
("dog" "likes" "lion" "-")
((triple5) -> (rule1 % int1))
The dog likes the lion.
("dog" "likes" "lion" "+")
int1
The dog sees the dog.
True
3
proof
[(((((triple5) -> rule1)) -> rule5))]
("dog" "sees" "dog" "+")
((((triple5) -> (rule1 % int2))) -> (rule5 % int1))
The dog sees the dog.
("dog" "sees" "dog" "+")
int1
The dog likes the lion.
("dog" "likes" "lion" "+")
int2
The dog does not see the dog.
False
3
inv-proof
[(((((triple5) -> rule1)) -> rule5))]
("dog" "sees" "dog" "-")
((((triple5) -> (rule1 % int2))) -> (rule5 % int1))
The dog sees the dog.
("dog" "sees" "dog" "+")
int1
The dog likes the lion.
("dog" "likes" "lion" "+")
int2
The dog is rough.
True
4
proof
[(((((((triple5) -> rule1)) -> rule5)) -> rule6))]
("dog" "is" "rough" "+")
((((((triple5) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
The dog is rough.
("dog" "is" "rough" "+")
int1
The dog sees the dog.
("dog" "sees" "dog" "+")
int2
The dog likes the lion.
("dog" "likes" "lion" "+")
int3
The dog is not rough.
False
4
inv-proof
[(((((((triple5) -> rule1)) -> rule5)) -> rule6))]
("dog" "is" "rough" "-")
((((((triple5) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
The dog is rough.
("dog" "is" "rough" "+")
int1
The dog sees the dog.
("dog" "sees" "dog" "+")
int2
The dog likes the lion.
("dog" "likes" "lion" "+")
int3
The rabbit does not like the lion.
Unknown
inv-rconc
[@1: The rabbit likes the lion.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("rabbit" "likes" "lion" "-")
The lion needs the rabbit.
Unknown
rconc
[@1: The lion needs the rabbit.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("lion" "needs" "rabbit" "+")
The lion does not see the dog.
Unknown
inv-rconc
[@1: The lion sees the dog.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("lion" "sees" "dog" "-")
The rabbit sees the dog.
Unknown
rconc
[@2: The rabbit sees the dog.[CWA. Example of deepest failure = (rule5 <- rule2 <- FAIL)]]
("rabbit" "sees" "dog" "+")
The rabbit does not see the rabbit.
Unknown
inv-random
[@0: The rabbit sees the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "sees" "rabbit" "-")
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 like the dog.
Unknown
inv-random
[@0: The dog likes the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "likes" "dog" "-")
The lion is nice.
Unknown
random
[@0: The lion is nice.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "nice" "+")
@0: The dog is big.[(triple1)] The dog is cold.[(triple2)] The dog needs the lion.[(triple3)] The dog needs the rabbit.[(triple4)] The dog sees the lion.[(triple5)] The dog sees the rabbit.[(triple6)] The lion is cold.[(triple7)] The lion needs the dog.[(triple8)] The lion sees the rabbit.[(triple9)] The rabbit is rough.[(triple10)] @1: The dog likes the lion.[(((triple5) -> rule1))] @2: The dog sees the dog.[(((((triple5) -> rule1)) -> rule5))] @3: The dog is rough.[(((((((triple5) -> rule1)) -> rule5)) -> rule6))]
The dog is big.
("dog" "is" "big" "+")
triple1
The dog is cold.
("dog" "is" "cold" "+")
triple2
The dog needs the lion.
("dog" "needs" "lion" "+")
triple3
The dog needs the rabbit.
("dog" "needs" "rabbit" "+")
triple4
The dog sees the lion.
("dog" "sees" "lion" "+")
triple5
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
triple6
The lion is cold.
("lion" "is" "cold" "+")
triple7
The lion needs the dog.
("lion" "needs" "dog" "+")
triple8
The lion sees the rabbit.
("lion" "sees" "rabbit" "+")
triple9
The rabbit is rough.
("rabbit" "is" "rough" "+")
triple10
The dog likes the lion.
("dog" "likes" "lion" "+")
((triple5) -> (rule1 % int1))
The dog likes the lion.
("dog" "likes" "lion" "+")
int1
The dog sees the dog.
("dog" "sees" "dog" "+")
((((triple5) -> (rule1 % int2))) -> (rule5 % int1))
The dog sees the dog.
("dog" "sees" "dog" "+")
int1
The dog likes the lion.
("dog" "likes" "lion" "+")
int2
The dog is rough.
("dog" "is" "rough" "+")
((((((triple5) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
The dog is rough.
("dog" "is" "rough" "+")
int1
The dog sees the dog.
("dog" "sees" "dog" "+")
int2
The dog likes the lion.
("dog" "likes" "lion" "+")
int3