Bob is smart. Charlie is green. Erin is young. Gary is round. All green, round things are quiet. All green things are kind. If something is quiet then it is round.
Bob is smart.
("Bob" "is" "smart" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Erin is young.
("Erin" "is" "young" "+")
Gary is round.
("Gary" "is" "round" "+")
All green, round things are quiet.
((("something" "is" "green" "+") ("something" "is" "round" "+")) -> ("something" "is" "quiet" "+"))
All green things are kind.
((("something" "is" "green" "+")) -> ("something" "is" "kind" "+"))
If something is quiet then it is round.
((("something" "is" "quiet" "+")) -> ("something" "is" "round" "+"))
Erin is young.
True
1
proof
[(triple3)]
("Erin" "is" "young" "+")
triple3
Erin is not young.
False
1
inv-proof
[(triple3)]
("Erin" "is" "young" "-")
triple3
Charlie is not round.
Unknown
inv-rconc
[@2: Charlie is round.[CWA. Example of deepest failure = (rule3 <- rule1 <- FAIL)]]
("Charlie" "is" "round" "-")
Bob is young.
Unknown
random
[@0: Bob is young.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "young" "+")
@0: Bob is smart.[(triple1)] Charlie is green.[(triple2)] Erin is young.[(triple3)] Gary is round.[(triple4)] @1: Charlie is kind.[(((triple2) -> rule2))]
Bob is smart.
("Bob" "is" "smart" "+")
triple1
Charlie is green.
("Charlie" "is" "green" "+")
triple2
Erin is young.
("Erin" "is" "young" "+")
triple3
Gary is round.
("Gary" "is" "round" "+")
triple4
Charlie is kind.
("Charlie" "is" "kind" "+")
((triple2) -> (rule2 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1