The dog chases the lion. The dog does not chase the rabbit. The dog sees the lion. The lion is not rough. The lion sees the dog. The lion does not visit the rabbit. The rabbit does not chase the lion. The rabbit is cold. The rabbit sees the dog. The rabbit sees the lion. The rabbit visits the dog. The rabbit visits the lion. Young, rough people are not blue. If someone visits the lion then the lion visits the dog.
The dog chases the lion.
("dog" "chases" "lion" "+")
The dog does not chase the rabbit.
("dog" "chases" "rabbit" "-")
The dog sees the lion.
("dog" "sees" "lion" "+")
The lion is not rough.
("lion" "is" "rough" "-")
The lion sees the dog.
("lion" "sees" "dog" "+")
The lion does not visit the rabbit.
("lion" "visits" "rabbit" "-")
The rabbit does not chase the lion.
("rabbit" "chases" "lion" "-")
The rabbit is cold.
("rabbit" "is" "cold" "+")
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
The rabbit visits the dog.
("rabbit" "visits" "dog" "+")
The rabbit visits the lion.
("rabbit" "visits" "lion" "+")
Young, rough people are not blue.
((("someone" "is" "young" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "blue" "-"))
If someone visits the lion then the lion visits the dog.
((("someone" "visits" "lion" "+")) -> ("lion" "visits" "dog" "+"))
The rabbit visits the dog.
True
1
proof
[(triple11)]
("rabbit" "visits" "dog" "+")
triple11
The rabbit does not see the dog.
False
1
inv-proof
[(triple9)]
("rabbit" "sees" "dog" "-")
triple9
The lion visits the dog.
True
2
proof
[(((triple12) -> rule2))]
("lion" "visits" "dog" "+")
((triple12) -> (rule2 % int1))
The lion visits the dog.
("lion" "visits" "dog" "+")
int1
The lion does not visit the dog.
False
2
inv-proof
[(((triple12) -> rule2))]
("lion" "visits" "dog" "-")
((triple12) -> (rule2 % int1))
The lion visits the dog.
("lion" "visits" "dog" "+")
int1
The lion does not chase the lion.
Unknown
inv-random
[@0: The lion chases the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "lion" "-")
The lion is blue.
Unknown
random
[@0: The lion is blue.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "blue" "+")
The dog is not cold.
Unknown
inv-random
[@0: The dog is cold.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "cold" "-")
The dog is nice.
Unknown
random
[@0: The dog is nice.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "nice" "+")
@0: The dog chases the lion.[(triple1)] The dog does not chase the rabbit.[(triple2)] The dog sees the lion.[(triple3)] The lion does not visit the rabbit.[(triple6)] The lion is not rough.[(triple4)] The lion sees the dog.[(triple5)] The rabbit does not chase the lion.[(triple7)] The rabbit is cold.[(triple8)] The rabbit sees the dog.[(triple9)] The rabbit sees the lion.[(triple10)] The rabbit visits the dog.[(triple11)] The rabbit visits the lion.[(triple12)] @1: The lion visits the dog.[(((triple12) -> rule2))]
The dog chases the lion.
("dog" "chases" "lion" "+")
triple1
The dog does not chase the rabbit.
("dog" "chases" "rabbit" "-")
triple2
The dog sees the lion.
("dog" "sees" "lion" "+")
triple3
The lion does not visit the rabbit.
("lion" "visits" "rabbit" "-")
triple6
The lion is not rough.
("lion" "is" "rough" "-")
triple4
The lion sees the dog.
("lion" "sees" "dog" "+")
triple5
The rabbit does not chase the lion.
("rabbit" "chases" "lion" "-")
triple7
The rabbit is cold.
("rabbit" "is" "cold" "+")
triple8
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
triple9
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
triple10
The rabbit visits the dog.
("rabbit" "visits" "dog" "+")
triple11
The rabbit visits the lion.
("rabbit" "visits" "lion" "+")
triple12
The lion visits the dog.
("lion" "visits" "dog" "+")
((triple12) -> (rule2 % int1))
The lion visits the dog.
("lion" "visits" "dog" "+")
int1