Anne is smart. Bob is quiet. Bob is smart. Charlie is quiet. Charlie is red. Charlie is smart. Dave is red. All quiet people are nice. If Anne is quiet then Anne is nice. All nice people are rough. Quiet people are red. If Bob is rough then Bob is quiet. All rough people are quiet. Quiet people are green. All smart people are round.
Anne is smart.
("Anne" "is" "smart" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Dave is red.
("Dave" "is" "red" "+")
All quiet people are nice.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "nice" "+"))
If Anne is quiet then Anne is nice.
((("Anne" "is" "quiet" "+")) -> ("Anne" "is" "nice" "+"))
All nice people are rough.
((("someone" "is" "nice" "+")) -> ("someone" "is" "rough" "+"))
Quiet people are red.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "red" "+"))
If Bob is rough then Bob is quiet.
((("Bob" "is" "rough" "+")) -> ("Bob" "is" "quiet" "+"))
All rough people are quiet.
((("someone" "is" "rough" "+")) -> ("someone" "is" "quiet" "+"))
Quiet people are green.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "green" "+"))
All smart people are round.
((("someone" "is" "smart" "+")) -> ("someone" "is" "round" "+"))
Charlie is smart.
True
1
proof
[(triple6)]
("Charlie" "is" "smart" "+")
triple6
Anne is not smart.
False
1
inv-proof
[(triple1)]
("Anne" "is" "smart" "-")
triple1
Charlie is round.
True
2
proof
[(((triple6) -> rule8))]
("Charlie" "is" "round" "+")
((triple6) -> (rule8 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Bob is not nice.
False
2
inv-proof
[(((triple2) -> rule1))]
("Bob" "is" "nice" "-")
((triple2) -> (rule1 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Dave is not nice.
Unknown
inv-rconc
[@3: Dave is nice.[CWA. Example of deepest failure = (rule1 <- rule6 <- rule3 <- FAIL)]]
("Dave" "is" "nice" "-")
Dave is quiet.
Unknown
rconc
[@3: Dave is quiet.[CWA. Example of deepest failure = (rule6 <- rule3 <- rule1 <- FAIL)]]
("Dave" "is" "quiet" "+")
@0: Anne is smart.[(triple1)] Bob is quiet.[(triple2)] Bob is smart.[(triple3)] Charlie is quiet.[(triple4)] Charlie is red.[(triple5 OR ((triple4) -> rule4))] Charlie is smart.[(triple6)] Dave is red.[(triple7)] @1: Anne is round.[(((triple1) -> rule8))] Bob is green.[(((triple2) -> rule7))] Bob is nice.[(((triple2) -> rule1))] Bob is red.[(((triple2) -> rule4))] Bob is round.[(((triple3) -> rule8))] Charlie is green.[(((triple4) -> rule7))] Charlie is nice.[(((triple4) -> rule1))] Charlie is round.[(((triple6) -> rule8))] @2: Bob is rough.[(((((triple2) -> rule1)) -> rule3))] Charlie is rough.[(((((triple4) -> rule1)) -> rule3))]
Anne is smart.
("Anne" "is" "smart" "+")
triple1
Bob is quiet.
("Bob" "is" "quiet" "+")
triple2
Bob is smart.
("Bob" "is" "smart" "+")
triple3
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple4
Charlie is red.
("Charlie" "is" "red" "+")
triple5
((triple4) -> (rule4 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
triple6
Dave is red.
("Dave" "is" "red" "+")
triple7
Anne is round.
("Anne" "is" "round" "+")
((triple1) -> (rule8 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
((triple2) -> (rule7 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
((triple2) -> (rule1 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
((triple2) -> (rule4 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
((triple3) -> (rule8 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
((triple4) -> (rule7 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
((triple4) -> (rule1 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
((triple6) -> (rule8 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
((((triple2) -> (rule1 % int2))) -> (rule3 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
((((triple4) -> (rule1 % int2))) -> (rule3 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2