The cow eats the lion. The cow is not big. The cow is not cold. The cow is kind. The cow is not nice. The cow is not red. The cow likes the lion. The cow sees the lion. The lion is big. The lion sees the cow. If someone sees the lion then the lion likes the cow. If someone eats the cow and the cow eats the lion then the lion likes the cow. If someone likes the cow then they like the lion. If someone is red then they like the cow. If someone is kind and big then they see the lion. If someone sees the lion and the lion does not eat the cow then the cow likes the lion.
The cow eats the lion.
("cow" "eats" "lion" "+")
The cow is not big.
("cow" "is" "big" "-")
The cow is not cold.
("cow" "is" "cold" "-")
The cow is kind.
("cow" "is" "kind" "+")
The cow is not nice.
("cow" "is" "nice" "-")
The cow is not red.
("cow" "is" "red" "-")
The cow likes the lion.
("cow" "likes" "lion" "+")
The cow sees the lion.
("cow" "sees" "lion" "+")
The lion is big.
("lion" "is" "big" "+")
The lion sees the cow.
("lion" "sees" "cow" "+")
If someone sees the lion then the lion likes the cow.
((("someone" "sees" "lion" "+")) -> ("lion" "likes" "cow" "+"))
If someone eats the cow and the cow eats the lion then the lion likes the cow.
((("someone" "eats" "cow" "+") ("cow" "eats" "lion" "+")) -> ("lion" "likes" "cow" "+"))
If someone likes the cow then they like the lion.
((("someone" "likes" "cow" "+")) -> ("someone" "likes" "lion" "+"))
If someone is red then they like the cow.
((("someone" "is" "red" "+")) -> ("someone" "likes" "cow" "+"))
If someone is kind and big then they see the lion.
((("someone" "is" "kind" "+") ("someone" "is" "big" "+")) -> ("someone" "sees" "lion" "+"))
If someone sees the lion and the lion does not eat the cow then the cow likes the lion.
((("someone" "sees" "lion" "+") ("lion" "eats" "cow" "~")) -> ("cow" "likes" "lion" "+"))
The lion is big.
True
1
proof
[(triple9)]
("lion" "is" "big" "+")
triple9
The cow does not like the lion.
False
1
inv-proof
[(triple7)]
("cow" "likes" "lion" "-")
triple7
The lion likes the cow.
True
2
proof
[(((triple8) -> rule1))]
("lion" "likes" "cow" "+")
((triple8) -> (rule1 % int1))
The lion likes the cow.
("lion" "likes" "cow" "+")
int1
The lion does not like the cow.
False
2
inv-proof
[(((triple8) -> rule1))]
("lion" "likes" "cow" "-")
((triple8) -> (rule1 % int1))
The lion likes the cow.
("lion" "likes" "cow" "+")
int1
The lion likes the lion.
True
3
proof
[(((((triple8) -> rule1)) -> rule3))]
("lion" "likes" "lion" "+")
((((triple8) -> (rule1 % int2))) -> (rule3 % int1))
The lion likes the lion.
("lion" "likes" "lion" "+")
int1
The lion likes the cow.
("lion" "likes" "cow" "+")
int2
The lion does not like the lion.
False
3
inv-proof
[(((((triple8) -> rule1)) -> rule3))]
("lion" "likes" "lion" "-")
((((triple8) -> (rule1 % int2))) -> (rule3 % int1))
The lion likes the lion.
("lion" "likes" "lion" "+")
int1
The lion likes the cow.
("lion" "likes" "cow" "+")
int2
The cow does not like the cow.
Unknown
inv-rconc
[@1: The cow likes the cow.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cow" "likes" "cow" "-")
The lion sees the lion.
Unknown
rconc
[@1: The lion sees the lion.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("lion" "sees" "lion" "+")
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" "+")
The lion does not eat the cow.
Unknown
inv-random
[@0: The lion eats the cow.[CWA. Example of deepest failure = (FAIL)]]
("lion" "eats" "cow" "-")
The lion is nice.
Unknown
random
[@0: The lion is nice.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "nice" "+")
@0: The cow eats the lion.[(triple1)] The cow is kind.[(triple4)] The cow is not big.[(triple2)] The cow is not cold.[(triple3)] The cow is not nice.[(triple5)] The cow is not red.[(triple6)] The cow likes the lion.[(triple7)] The cow sees the lion.[(triple8)] The lion is big.[(triple9)] The lion sees the cow.[(triple10)] @1: The lion likes the cow.[(((triple8) -> rule1))] @2: The lion likes the lion.[(((((triple8) -> rule1)) -> rule3))]
The cow eats the lion.
("cow" "eats" "lion" "+")
triple1
The cow is kind.
("cow" "is" "kind" "+")
triple4
The cow is not big.
("cow" "is" "big" "-")
triple2
The cow is not cold.
("cow" "is" "cold" "-")
triple3
The cow is not nice.
("cow" "is" "nice" "-")
triple5
The cow is not red.
("cow" "is" "red" "-")
triple6
The cow likes the lion.
("cow" "likes" "lion" "+")
triple7
The cow sees the lion.
("cow" "sees" "lion" "+")
triple8
The lion is big.
("lion" "is" "big" "+")
triple9
The lion sees the cow.
("lion" "sees" "cow" "+")
triple10
The lion likes the cow.
("lion" "likes" "cow" "+")
((triple8) -> (rule1 % int1))
The lion likes the cow.
("lion" "likes" "cow" "+")
int1
The lion likes the lion.
("lion" "likes" "lion" "+")
((((triple8) -> (rule1 % int2))) -> (rule3 % int1))
The lion likes the lion.
("lion" "likes" "lion" "+")
int1
The lion likes the cow.
("lion" "likes" "cow" "+")
int2