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