The bear chases the lion. The dog chases the bear. The lion is big. If something is kind and it chases the lion then it chases the dog. If something sees the bear then it is round. If something chases the lion then the lion sees the bear. If something is round then it chases the bear. If something is kind and it likes the bear then it is red. If something chases the lion and the lion chases the bear then it likes the lion.
The bear chases the lion.
("bear" "chases" "lion" "+")
The dog chases the bear.
("dog" "chases" "bear" "+")
The lion is big.
("lion" "is" "big" "+")
If something is kind and it chases the lion then it chases the dog.
((("something" "is" "kind" "+") ("something" "chases" "lion" "+")) -> ("something" "chases" "dog" "+"))
If something sees the bear then it is round.
((("something" "sees" "bear" "+")) -> ("something" "is" "round" "+"))
If something chases the lion then the lion sees the bear.
((("something" "chases" "lion" "+")) -> ("lion" "sees" "bear" "+"))
If something is round then it chases the bear.
((("something" "is" "round" "+")) -> ("something" "chases" "bear" "+"))
If something is kind and it likes the bear then it is red.
((("something" "is" "kind" "+") ("something" "likes" "bear" "+")) -> ("something" "is" "red" "+"))
If something chases the lion and the lion chases the bear then it likes the lion.
((("something" "chases" "lion" "+") ("lion" "chases" "bear" "+")) -> ("something" "likes" "lion" "+"))
The dog chases the bear.
True
1
proof
[(triple2)]
("dog" "chases" "bear" "+")
triple2
The bear does not chase the lion.
False
1
inv-proof
[(triple1)]
("bear" "chases" "lion" "-")
triple1
The lion sees the bear.
True
2
proof
[(((triple1) -> rule3))]
("lion" "sees" "bear" "+")
((triple1) -> (rule3 % int1))
The lion sees the bear.
("lion" "sees" "bear" "+")
int1
The lion does not see the bear.
False
2
inv-proof
[(((triple1) -> rule3))]
("lion" "sees" "bear" "-")
((triple1) -> (rule3 % int1))
The lion sees the bear.
("lion" "sees" "bear" "+")
int1
The lion is round.
True
3
proof
[(((((triple1) -> rule3)) -> rule2))]
("lion" "is" "round" "+")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
The lion is round.
("lion" "is" "round" "+")
int1
The lion sees the bear.
("lion" "sees" "bear" "+")
int2
The lion is not round.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule2))]
("lion" "is" "round" "-")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
The lion is round.
("lion" "is" "round" "+")
int1
The lion sees the bear.
("lion" "sees" "bear" "+")
int2
The lion chases the bear.
True
4
proof
[(((((((triple1) -> rule3)) -> rule2)) -> rule4))]
("lion" "chases" "bear" "+")
((((((triple1) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
The lion chases the bear.
("lion" "chases" "bear" "+")
int1
The lion is round.
("lion" "is" "round" "+")
int2
The lion sees the bear.
("lion" "sees" "bear" "+")
int3
The lion does not chase the bear.
False
4
inv-proof
[(((((((triple1) -> rule3)) -> rule2)) -> rule4))]
("lion" "chases" "bear" "-")
((((((triple1) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
The lion chases the bear.
("lion" "chases" "bear" "+")
int1
The lion is round.
("lion" "is" "round" "+")
int2
The lion sees the bear.
("lion" "sees" "bear" "+")
int3
The bear is not round.
Unknown
inv-rconc
[@1: The bear is round.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("bear" "is" "round" "-")
The lion chases the dog.
Unknown
rconc
[@1: The lion chases the dog.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("lion" "chases" "dog" "+")
The bear does not chase the bear.
Unknown
inv-rconc
[@2: The bear chases the bear.[CWA. Example of deepest failure = (rule4 <- rule2 <- FAIL)]]
("bear" "chases" "bear" "-")
The bear chases the dog.
Unknown
rconc
[@1: The bear chases the dog.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("bear" "chases" "dog" "+")
The dog is not nice.
Unknown
inv-random
[@0: The dog is nice.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "nice" "-")
The bear sees the dog.
Unknown
random
[@0: The bear sees the dog.[CWA. Example of deepest failure = (FAIL)]]
("bear" "sees" "dog" "+")
The bear is not big.
Unknown
inv-random
[@0: The bear is big.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "big" "-")
The lion sees the lion.
Unknown
random
[@0: The lion sees the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "lion" "+")
@0: The bear chases the lion.[(triple1)] The dog chases the bear.[(triple2)] The lion is big.[(triple3)] @1: The lion sees the bear.[(((triple1) -> rule3))] @2: The lion is round.[(((((triple1) -> rule3)) -> rule2))] @3: The lion chases the bear.[(((((((triple1) -> rule3)) -> rule2)) -> rule4))] @4: The bear likes the lion.[(((triple1 ((((((triple1) -> rule3)) -> rule2)) -> rule4)) -> rule6))]
The bear chases the lion.
("bear" "chases" "lion" "+")
triple1
The dog chases the bear.
("dog" "chases" "bear" "+")
triple2
The lion is big.
("lion" "is" "big" "+")
triple3
The lion sees the bear.
("lion" "sees" "bear" "+")
((triple1) -> (rule3 % int1))
The lion sees the bear.
("lion" "sees" "bear" "+")
int1
The lion is round.
("lion" "is" "round" "+")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
The lion is round.
("lion" "is" "round" "+")
int1
The lion sees the bear.
("lion" "sees" "bear" "+")
int2
The lion chases the bear.
("lion" "chases" "bear" "+")
((((((triple1) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
The lion chases the bear.
("lion" "chases" "bear" "+")
int1
The lion is round.
("lion" "is" "round" "+")
int2
The lion sees the bear.
("lion" "sees" "bear" "+")
int3
The bear likes the lion.
("bear" "likes" "lion" "+")
((triple1 ((((((triple1) -> (rule3 % int4))) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
The bear likes the lion.
("bear" "likes" "lion" "+")
int1
The lion chases the bear.
("lion" "chases" "bear" "+")
int2
The lion is round.
("lion" "is" "round" "+")
int3
The lion sees the bear.
("lion" "sees" "bear" "+")
int4