The lion is blue. The lion is nice. The lion is red. The lion is rough. The lion is young. If someone is nice and rough then they are young. If someone is rough and nice then they are blue.
The lion is blue.
("lion" "is" "blue" "+")
The lion is nice.
("lion" "is" "nice" "+")
The lion is red.
("lion" "is" "red" "+")
The lion is rough.
("lion" "is" "rough" "+")
The lion is young.
("lion" "is" "young" "+")
If someone is nice and rough then they are young.
((("someone" "is" "nice" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "young" "+"))
If someone is rough and nice then they are blue.
((("someone" "is" "rough" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "blue" "+"))
The lion is young.
True
1
proof
[(triple5 OR ((triple2 triple4) -> rule1))]
("lion" "is" "young" "+")
triple5
((triple2 triple4) -> (rule1 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
The lion is not young.
False
1
inv-proof
[(triple5 OR ((triple2 triple4) -> rule1))]
("lion" "is" "young" "-")
triple5
((triple2 triple4) -> (rule1 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
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 needs the lion.
Unknown
random
[@0: The lion needs the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "needs" "lion" "+")
@0: The lion is blue.[(triple1 OR ((triple4 triple2) -> rule2))] The lion is nice.[(triple2)] The lion is red.[(triple3)] The lion is rough.[(triple4)] The lion is young.[(triple5 OR ((triple2 triple4) -> rule1))]
The lion is blue.
("lion" "is" "blue" "+")
triple1
((triple4 triple2) -> (rule2 % int1))
The lion is blue.
("lion" "is" "blue" "+")
int1
The lion is nice.
("lion" "is" "nice" "+")
triple2
The lion is red.
("lion" "is" "red" "+")
triple3
The lion is rough.
("lion" "is" "rough" "+")
triple4
The lion is young.
("lion" "is" "young" "+")
triple5
((triple2 triple4) -> (rule1 % int1))
The lion is young.
("lion" "is" "young" "+")
int1