Bob is cold. Bob is rough. Bob is young. Charlie is kind. Charlie is nice. Dave is kind. Dave is round. All young, rough people are round. Rough people are kind.
Bob is cold.
("Bob" "is" "cold" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Bob is young.
("Bob" "is" "young" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is round.
("Dave" "is" "round" "+")
All young, rough people are round.
((("someone" "is" "young" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "round" "+"))
Rough people are kind.
((("someone" "is" "rough" "+")) -> ("someone" "is" "kind" "+"))
Bob is young.
True
1
proof
[(triple3)]
("Bob" "is" "young" "+")
triple3
Bob is not young.
False
1
inv-proof
[(triple3)]
("Bob" "is" "young" "-")
triple3
Charlie is not round.
Unknown
inv-rconc
[@1: Charlie is round.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "round" "-")
Charlie is rough.
Unknown
random
[@0: Charlie is rough.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "rough" "+")
@0: Bob is cold.[(triple1)] Bob is rough.[(triple2)] Bob is young.[(triple3)] Charlie is kind.[(triple4)] Charlie is nice.[(triple5)] Dave is kind.[(triple6)] Dave is round.[(triple7)] @1: Bob is kind.[(((triple2) -> rule2))] Bob is round.[(((triple3 triple2) -> rule1))]
Bob is cold.
("Bob" "is" "cold" "+")
triple1
Bob is rough.
("Bob" "is" "rough" "+")
triple2
Bob is young.
("Bob" "is" "young" "+")
triple3
Charlie is kind.
("Charlie" "is" "kind" "+")
triple4
Charlie is nice.
("Charlie" "is" "nice" "+")
triple5
Dave is kind.
("Dave" "is" "kind" "+")
triple6
Dave is round.
("Dave" "is" "round" "+")
triple7
Bob is kind.
("Bob" "is" "kind" "+")
((triple2) -> (rule2 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
((triple3 triple2) -> (rule1 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1