Anne is big. Anne is nice. Bob is green. Bob is rough. Charlie is green. Charlie is smart. Charlie is young. Dave is big. Dave is green. Dave is rough. All nice people are kind. If someone is kind and nice then they are smart. All smart people are green.
Anne is big.
("Anne" "is" "big" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is rough.
("Dave" "is" "rough" "+")
All nice people are kind.
((("someone" "is" "nice" "+")) -> ("someone" "is" "kind" "+"))
If someone is kind and nice then they are smart.
((("someone" "is" "kind" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "smart" "+"))
All smart people are green.
((("someone" "is" "smart" "+")) -> ("someone" "is" "green" "+"))
Charlie is green.
True
1
proof
[(triple5 OR ((triple6) -> rule3))]
("Charlie" "is" "green" "+")
triple5
((triple6) -> (rule3 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Anne is not nice.
False
1
inv-proof
[(triple2)]
("Anne" "is" "nice" "-")
triple2
Charlie is not kind.
Unknown
inv-rconc
[@1: Charlie is kind.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "kind" "-")
Bob is young.
Unknown
random
[@0: Bob is young.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "young" "+")
@0: Anne is big.[(triple1)] Anne is nice.[(triple2)] Bob is green.[(triple3)] Bob is rough.[(triple4)] Charlie is green.[(triple5 OR ((triple6) -> rule3))] Charlie is smart.[(triple6)] Charlie is young.[(triple7)] Dave is big.[(triple8)] Dave is green.[(triple9)] Dave is rough.[(triple10)] @1: Anne is kind.[(((triple2) -> rule1))] @2: Anne is smart.[(((((triple2) -> rule1) triple2) -> rule2))] @3: Anne is green.[(((((((triple2) -> rule1) triple2) -> rule2)) -> rule3))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is nice.
("Anne" "is" "nice" "+")
triple2
Bob is green.
("Bob" "is" "green" "+")
triple3
Bob is rough.
("Bob" "is" "rough" "+")
triple4
Charlie is green.
("Charlie" "is" "green" "+")
triple5
((triple6) -> (rule3 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
triple6
Charlie is young.
("Charlie" "is" "young" "+")
triple7
Dave is big.
("Dave" "is" "big" "+")
triple8
Dave is green.
("Dave" "is" "green" "+")
triple9
Dave is rough.
("Dave" "is" "rough" "+")
triple10
Anne is kind.
("Anne" "is" "kind" "+")
((triple2) -> (rule1 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
((((triple2) -> (rule1 % int2)) triple2) -> (rule2 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
((((((triple2) -> (rule1 % int3)) triple2) -> (rule2 % int2))) -> (rule3 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
int3