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