The cow is nice. The cow is young. The cow likes the dog. The cow likes the lion. The cow sees the dog. The cow sees the lion. The dog is not cold. The dog is round. The dog does not like the lion. The dog sees the cow. The lion sees the cow. The lion sees the dog. If someone sees the lion then they are not round.
The cow is nice.
("cow" "is" "nice" "+")
The cow is young.
("cow" "is" "young" "+")
The cow likes the dog.
("cow" "likes" "dog" "+")
The cow likes the lion.
("cow" "likes" "lion" "+")
The cow sees the dog.
("cow" "sees" "dog" "+")
The cow sees the lion.
("cow" "sees" "lion" "+")
The dog is not cold.
("dog" "is" "cold" "-")
The dog is round.
("dog" "is" "round" "+")
The dog does not like the lion.
("dog" "likes" "lion" "-")
The dog sees the cow.
("dog" "sees" "cow" "+")
The lion sees the cow.
("lion" "sees" "cow" "+")
The lion sees the dog.
("lion" "sees" "dog" "+")
If someone sees the lion then they are not round.
((("someone" "sees" "lion" "+")) -> ("someone" "is" "round" "-"))
The dog sees the cow.
True
1
proof
[(triple10)]
("dog" "sees" "cow" "+")
triple10
The cow is not nice.
False
1
inv-proof
[(triple1)]
("cow" "is" "nice" "-")
triple1
The cow is not round.
True
2
proof
[(((triple6) -> rule1))]
("cow" "is" "round" "-")
((triple6) -> (rule1 % int1))
The cow is not round.
("cow" "is" "round" "-")
int1
The cow is round.
False
2
inv-proof
[(((triple6) -> rule1))]
("cow" "is" "round" "+")
((triple6) -> (rule1 % int1))
The cow is not round.
("cow" "is" "round" "-")
int1
The lion does not need the cow.
Unknown
inv-random
[@0: The lion needs the cow.[CWA. Example of deepest failure = (FAIL)]]
("lion" "needs" "cow" "-")
The cow needs the lion.
Unknown
random
[@0: The cow needs the lion.[CWA. Example of deepest failure = (FAIL)]]
("cow" "needs" "lion" "+")
The dog is not kind.
Unknown
inv-random
[@0: The dog is kind.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "kind" "-")
The lion sees the lion.
Unknown
random
[@0: The lion sees the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "lion" "+")
@0: The cow is nice.[(triple1)] The cow is young.[(triple2)] The cow likes the dog.[(triple3)] The cow likes the lion.[(triple4)] The cow sees the dog.[(triple5)] The cow sees the lion.[(triple6)] The dog does not like the lion.[(triple9)] The dog is not cold.[(triple7)] The dog is round.[(triple8)] The dog sees the cow.[(triple10)] The lion sees the cow.[(triple11)] The lion sees the dog.[(triple12)] @1: The cow is not round.[(((triple6) -> rule1))]
The cow is nice.
("cow" "is" "nice" "+")
triple1
The cow is young.
("cow" "is" "young" "+")
triple2
The cow likes the dog.
("cow" "likes" "dog" "+")
triple3
The cow likes the lion.
("cow" "likes" "lion" "+")
triple4
The cow sees the dog.
("cow" "sees" "dog" "+")
triple5
The cow sees the lion.
("cow" "sees" "lion" "+")
triple6
The dog does not like the lion.
("dog" "likes" "lion" "-")
triple9
The dog is not cold.
("dog" "is" "cold" "-")
triple7
The dog is round.
("dog" "is" "round" "+")
triple8
The dog sees the cow.
("dog" "sees" "cow" "+")
triple10
The lion sees the cow.
("lion" "sees" "cow" "+")
triple11
The lion sees the dog.
("lion" "sees" "dog" "+")
triple12
The cow is not round.
("cow" "is" "round" "-")
((triple6) -> (rule1 % int1))
The cow is not round.
("cow" "is" "round" "-")
int1