Bob is rough. Bob is round. Bob is young. Charlie is kind. Charlie is quiet. Charlie is red. Charlie is rough. Erin is blue. Erin is kind. Erin is quiet. All quiet people are round. If someone is young and red then they are kind.
Bob is rough.
("Bob" "is" "rough" "+")
Bob is round.
("Bob" "is" "round" "+")
Bob is young.
("Bob" "is" "young" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
All quiet people are round.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "round" "+"))
If someone is young and red then they are kind.
((("someone" "is" "young" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "kind" "+"))
Bob is rough.
True
1
proof
[(triple1)]
("Bob" "is" "rough" "+")
triple1
Charlie is not rough.
False
1
inv-proof
[(triple7)]
("Charlie" "is" "rough" "-")
triple7
Bob is not kind.
Unknown
inv-rconc
[@1: Bob is kind.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Bob" "is" "kind" "-")
Bob is quiet.
Unknown
random
[@0: Bob is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "quiet" "+")
@0: Bob is rough.[(triple1)] Bob is round.[(triple2)] Bob is young.[(triple3)] Charlie is kind.[(triple4)] Charlie is quiet.[(triple5)] Charlie is red.[(triple6)] Charlie is rough.[(triple7)] Erin is blue.[(triple8)] Erin is kind.[(triple9)] Erin is quiet.[(triple10)] @1: Charlie is round.[(((triple5) -> rule1))] Erin is round.[(((triple10) -> rule1))]
Bob is rough.
("Bob" "is" "rough" "+")
triple1
Bob is round.
("Bob" "is" "round" "+")
triple2
Bob is young.
("Bob" "is" "young" "+")
triple3
Charlie is kind.
("Charlie" "is" "kind" "+")
triple4
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple5
Charlie is red.
("Charlie" "is" "red" "+")
triple6
Charlie is rough.
("Charlie" "is" "rough" "+")
triple7
Erin is blue.
("Erin" "is" "blue" "+")
triple8
Erin is kind.
("Erin" "is" "kind" "+")
triple9
Erin is quiet.
("Erin" "is" "quiet" "+")
triple10
Charlie is round.
("Charlie" "is" "round" "+")
((triple5) -> (rule1 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
((triple10) -> (rule1 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1