The cat does not see the lion. The cat sees the rabbit. The lion is round. The rabbit chases the cat. The rabbit sees the cat. The rabbit sees the lion. The rabbit visits the lion. If something sees the lion then the lion does not see the rabbit. If something sees the rabbit and the rabbit sees the cat then it is not round. If the cat is not round then the cat visits the lion.
The cat does not see the lion.
("cat" "sees" "lion" "-")
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
The lion is round.
("lion" "is" "round" "+")
The rabbit chases the cat.
("rabbit" "chases" "cat" "+")
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
The rabbit visits the lion.
("rabbit" "visits" "lion" "+")
If something sees the lion then the lion does not see the rabbit.
((("something" "sees" "lion" "+")) -> ("lion" "sees" "rabbit" "-"))
If something sees the rabbit and the rabbit sees the cat then it is not round.
((("something" "sees" "rabbit" "+") ("rabbit" "sees" "cat" "+")) -> ("something" "is" "round" "-"))
If the cat is not round then the cat visits the lion.
((("cat" "is" "round" "~")) -> ("cat" "visits" "lion" "+"))
The lion is round.
True
1
proof
[(triple3)]
("lion" "is" "round" "+")
triple3
The cat sees the lion.
False
1
inv-proof
[(triple1)]
("cat" "sees" "lion" "+")
triple1
The cat is not round.
True
3
proof
[(((triple2 triple5) -> rule2))]
("cat" "is" "round" "-")
((triple2 triple5) -> (rule2 % int1))
The cat is not round.
("cat" "is" "round" "-")
int1
The cat is round.
False
3
inv-proof
[(((triple2 triple5) -> rule2))]
("cat" "is" "round" "+")
((triple2 triple5) -> (rule2 % int1))
The cat is not round.
("cat" "is" "round" "-")
int1
The cat is not nice.
Unknown
inv-random
[@0: The cat is nice.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "nice" "-")
The rabbit sees the rabbit.
Unknown
random
[@0: The rabbit sees the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "sees" "rabbit" "+")
The lion does not visit the lion.
Unknown
inv-random
[@0: The lion visits the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "visits" "lion" "-")
The lion chases the rabbit.
Unknown
random
[@0: The lion chases the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "rabbit" "+")
@0: The cat does not see the lion.[(triple1)] The cat sees the rabbit.[(triple2)] The lion is round.[(triple3)] The rabbit chases the cat.[(triple4)] The rabbit sees the cat.[(triple5)] The rabbit sees the lion.[(triple6)] The rabbit visits the lion.[(triple7)] @1: The cat is not round.[(((triple2 triple5) -> rule2))] The lion does not see the rabbit.[(((triple6) -> rule1))] @2: The cat visits the lion.[(((((triple2 triple5) -> rule2)) -> rule3))]
The cat does not see the lion.
("cat" "sees" "lion" "-")
triple1
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
triple2
The lion is round.
("lion" "is" "round" "+")
triple3
The rabbit chases the cat.
("rabbit" "chases" "cat" "+")
triple4
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
triple5
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
triple6
The rabbit visits the lion.
("rabbit" "visits" "lion" "+")
triple7
The cat is not round.
("cat" "is" "round" "-")
((triple2 triple5) -> (rule2 % int1))
The cat is not round.
("cat" "is" "round" "-")
int1
The lion does not see the rabbit.
("lion" "sees" "rabbit" "-")
((triple6) -> (rule1 % int1))
The lion does not see the rabbit.
("lion" "sees" "rabbit" "-")
int1
The cat visits the lion.
("cat" "visits" "lion" "+")
((((triple2 triple5) -> (rule2 % int2))) -> (rule3 % int1))
The cat visits the lion.
("cat" "visits" "lion" "+")
int1
The cat is not round.
("cat" "is" "round" "-")
int2