The cat does not chase the lion. The cat does not eat the lion. The cat is green. The cat is not kind. The cat is round. The cat is young. The cat needs the lion. The lion does not chase the cat. The lion eats the cat. The lion is cold. The lion is green. The lion is kind. The lion is not round. The lion is young. The lion needs the cat. If something is green then it needs the cat. If the cat does not need the lion then the lion does not eat the cat. If something eats the lion and it is cold then the lion is round.
The cat does not chase the lion.
("cat" "chases" "lion" "-")
The cat does not eat the lion.
("cat" "eats" "lion" "-")
The cat is green.
("cat" "is" "green" "+")
The cat is not kind.
("cat" "is" "kind" "-")
The cat is round.
("cat" "is" "round" "+")
The cat is young.
("cat" "is" "young" "+")
The cat needs the lion.
("cat" "needs" "lion" "+")
The lion does not chase the cat.
("lion" "chases" "cat" "-")
The lion eats the cat.
("lion" "eats" "cat" "+")
The lion is cold.
("lion" "is" "cold" "+")
The lion is green.
("lion" "is" "green" "+")
The lion is kind.
("lion" "is" "kind" "+")
The lion is not round.
("lion" "is" "round" "-")
The lion is young.
("lion" "is" "young" "+")
The lion needs the cat.
("lion" "needs" "cat" "+")
If something is green then it needs the cat.
((("something" "is" "green" "+")) -> ("something" "needs" "cat" "+"))
If the cat does not need the lion then the lion does not eat the cat.
((("cat" "needs" "lion" "~")) -> ("lion" "eats" "cat" "-"))
If something eats the lion and it is cold then the lion is round.
((("something" "eats" "lion" "+") ("something" "is" "cold" "+")) -> ("lion" "is" "round" "+"))
The lion does not chase the cat.
True
1
proof
[(triple8)]
("lion" "chases" "cat" "-")
triple8
The cat is not round.
False
1
inv-proof
[(triple5)]
("cat" "is" "round" "-")
triple5
The cat needs the cat.
True
2
proof
[(((triple3) -> rule1))]
("cat" "needs" "cat" "+")
((triple3) -> (rule1 % int1))
The cat needs the cat.
("cat" "needs" "cat" "+")
int1
The cat does not need the cat.
False
2
inv-proof
[(((triple3) -> rule1))]
("cat" "needs" "cat" "-")
((triple3) -> (rule1 % int1))
The cat needs the cat.
("cat" "needs" "cat" "+")
int1
The cat does not chase the cat.
Unknown
inv-random
[@0: The cat chases the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "chases" "cat" "-")
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 chase the lion.
Unknown
inv-random
[@0: The lion chases the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "lion" "-")
The cat is cold.
Unknown
random
[@0: The cat is cold.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "cold" "+")
@0: The cat does not chase the lion.[(triple1)] The cat does not eat the lion.[(triple2)] The cat is green.[(triple3)] The cat is not kind.[(triple4)] The cat is round.[(triple5)] The cat is young.[(triple6)] The cat needs the lion.[(triple7)] The lion does not chase the cat.[(triple8)] The lion eats the cat.[(triple9)] The lion is cold.[(triple10)] The lion is green.[(triple11)] The lion is kind.[(triple12)] The lion is not round.[(triple13)] The lion is young.[(triple14)] The lion needs the cat.[(triple15 OR ((triple11) -> rule1))] @1: The cat needs the cat.[(((triple3) -> rule1))]
The cat does not chase the lion.
("cat" "chases" "lion" "-")
triple1
The cat does not eat the lion.
("cat" "eats" "lion" "-")
triple2
The cat is green.
("cat" "is" "green" "+")
triple3
The cat is not kind.
("cat" "is" "kind" "-")
triple4
The cat is round.
("cat" "is" "round" "+")
triple5
The cat is young.
("cat" "is" "young" "+")
triple6
The cat needs the lion.
("cat" "needs" "lion" "+")
triple7
The lion does not chase the cat.
("lion" "chases" "cat" "-")
triple8
The lion eats the cat.
("lion" "eats" "cat" "+")
triple9
The lion is cold.
("lion" "is" "cold" "+")
triple10
The lion is green.
("lion" "is" "green" "+")
triple11
The lion is kind.
("lion" "is" "kind" "+")
triple12
The lion is not round.
("lion" "is" "round" "-")
triple13
The lion is young.
("lion" "is" "young" "+")
triple14
The lion needs the cat.
("lion" "needs" "cat" "+")
triple15
((triple11) -> (rule1 % int1))
The lion needs the cat.
("lion" "needs" "cat" "+")
int1
The cat needs the cat.
("cat" "needs" "cat" "+")
((triple3) -> (rule1 % int1))
The cat needs the cat.
("cat" "needs" "cat" "+")
int1