The cow is big. The cow is green. The cow is nice. The cow sees the lion. The lion is nice. The tiger is big. The tiger sees the cow. Green, nice people are red. If the cow is red and the cow likes the lion then the cow is kind. If someone is red then they like the lion.
The cow is big.
("cow" "is" "big" "+")
The cow is green.
("cow" "is" "green" "+")
The cow is nice.
("cow" "is" "nice" "+")
The cow sees the lion.
("cow" "sees" "lion" "+")
The lion is nice.
("lion" "is" "nice" "+")
The tiger is big.
("tiger" "is" "big" "+")
The tiger sees the cow.
("tiger" "sees" "cow" "+")
Green, nice people are red.
((("someone" "is" "green" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "red" "+"))
If the cow is red and the cow likes the lion then the cow is kind.
((("cow" "is" "red" "+") ("cow" "likes" "lion" "+")) -> ("cow" "is" "kind" "+"))
If someone is red then they like the lion.
((("someone" "is" "red" "+")) -> ("someone" "likes" "lion" "+"))
The tiger sees the cow.
True
1
proof
[(triple7)]
("tiger" "sees" "cow" "+")
triple7
The cow is not nice.
False
1
inv-proof
[(triple3)]
("cow" "is" "nice" "-")
triple3
The cow is red.
True
3
proof
[(((triple2 triple3) -> rule1))]
("cow" "is" "red" "+")
((triple2 triple3) -> (rule1 % int1))
The cow is red.
("cow" "is" "red" "+")
int1
The cow is not red.
False
3
inv-proof
[(((triple2 triple3) -> rule1))]
("cow" "is" "red" "-")
((triple2 triple3) -> (rule1 % int1))
The cow is red.
("cow" "is" "red" "+")
int1
The cow likes the lion.
True
4
proof
[(((((triple2 triple3) -> rule1)) -> rule3))]
("cow" "likes" "lion" "+")
((((triple2 triple3) -> (rule1 % int2))) -> (rule3 % int1))
The cow likes the lion.
("cow" "likes" "lion" "+")
int1
The cow is red.
("cow" "is" "red" "+")
int2
The cow does not like the lion.
False
4
inv-proof
[(((((triple2 triple3) -> rule1)) -> rule3))]
("cow" "likes" "lion" "-")
((((triple2 triple3) -> (rule1 % int2))) -> (rule3 % int1))
The cow likes the lion.
("cow" "likes" "lion" "+")
int1
The cow is red.
("cow" "is" "red" "+")
int2
The cow is kind.
True
8
proof
[(((((triple2 triple3) -> rule1) ((((triple2 triple3) -> rule1)) -> rule3)) -> rule2))]
("cow" "is" "kind" "+")
((((triple2 triple3) -> (rule1 % int3)) ((((triple2 triple3) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The cow is kind.
("cow" "is" "kind" "+")
int1
The cow likes the lion.
("cow" "likes" "lion" "+")
int2
The cow is red.
("cow" "is" "red" "+")
int3
The cow is not kind.
False
8
inv-proof
[(((((triple2 triple3) -> rule1) ((((triple2 triple3) -> rule1)) -> rule3)) -> rule2))]
("cow" "is" "kind" "-")
((((triple2 triple3) -> (rule1 % int3)) ((((triple2 triple3) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The cow is kind.
("cow" "is" "kind" "+")
int1
The cow likes the lion.
("cow" "likes" "lion" "+")
int2
The cow is red.
("cow" "is" "red" "+")
int3
The lion is not red.
Unknown
inv-rconc
[@1: The lion is red.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("lion" "is" "red" "-")
The lion likes the lion.
Unknown
rconc
[@2: The lion likes the lion.[CWA. Example of deepest failure = (rule3 <- rule1 <- FAIL)]]
("lion" "likes" "lion" "+")
The tiger does not like the lion.
Unknown
inv-rconc
[@2: The tiger likes the lion.[CWA. Example of deepest failure = (rule3 <- rule1 <- FAIL)]]
("tiger" "likes" "lion" "-")
The tiger is red.
Unknown
rconc
[@1: The tiger is red.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("tiger" "is" "red" "+")
The cow does not eat the lion.
Unknown
inv-random
[@0: The cow eats the lion.[CWA. Example of deepest failure = (FAIL)]]
("cow" "eats" "lion" "-")
The cow eats the cow.
Unknown
random
[@0: The cow eats the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "eats" "cow" "+")
The cow does not see the cow.
Unknown
inv-random
[@0: The cow sees the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "cow" "-")
The lion eats the lion.
Unknown
random
[@0: The lion eats the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "eats" "lion" "+")
@0: The cow is big.[(triple1)] The cow is green.[(triple2)] The cow is nice.[(triple3)] The cow sees the lion.[(triple4)] The lion is nice.[(triple5)] The tiger is big.[(triple6)] The tiger sees the cow.[(triple7)] @1: The cow is red.[(((triple2 triple3) -> rule1))] @2: The cow likes the lion.[(((((triple2 triple3) -> rule1)) -> rule3))] @3: The cow is kind.[(((((triple2 triple3) -> rule1) ((((triple2 triple3) -> rule1)) -> rule3)) -> rule2))]
The cow is big.
("cow" "is" "big" "+")
triple1
The cow is green.
("cow" "is" "green" "+")
triple2
The cow is nice.
("cow" "is" "nice" "+")
triple3
The cow sees the lion.
("cow" "sees" "lion" "+")
triple4
The lion is nice.
("lion" "is" "nice" "+")
triple5
The tiger is big.
("tiger" "is" "big" "+")
triple6
The tiger sees the cow.
("tiger" "sees" "cow" "+")
triple7
The cow is red.
("cow" "is" "red" "+")
((triple2 triple3) -> (rule1 % int1))
The cow is red.
("cow" "is" "red" "+")
int1
The cow likes the lion.
("cow" "likes" "lion" "+")
((((triple2 triple3) -> (rule1 % int2))) -> (rule3 % int1))
The cow likes the lion.
("cow" "likes" "lion" "+")
int1
The cow is red.
("cow" "is" "red" "+")
int2
The cow is kind.
("cow" "is" "kind" "+")
((((triple2 triple3) -> (rule1 % int3)) ((((triple2 triple3) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The cow is kind.
("cow" "is" "kind" "+")
int1
The cow likes the lion.
("cow" "likes" "lion" "+")
int2
The cow is red.
("cow" "is" "red" "+")
int3