Anne is furry. Anne is quiet. Anne is red. Anne is round. Anne is smart. Anne is white. Anne is young. Bob is quiet. Bob is round. Gary is furry. Gary is quiet. Gary is red. Gary is round. Gary is smart. Gary is white. Gary is young. If someone is smart and white then they are red. All round people are furry. Smart people are red. All round people are young. Quiet, smart people are white. Red, quiet people are white.
Anne is furry.
("Anne" "is" "furry" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is round.
("Anne" "is" "round" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Anne is white.
("Anne" "is" "white" "+")
Anne is young.
("Anne" "is" "young" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is round.
("Bob" "is" "round" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is round.
("Gary" "is" "round" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Gary is white.
("Gary" "is" "white" "+")
Gary is young.
("Gary" "is" "young" "+")
If someone is smart and white then they are red.
((("someone" "is" "smart" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "red" "+"))
All round people are furry.
((("someone" "is" "round" "+")) -> ("someone" "is" "furry" "+"))
Smart people are red.
((("someone" "is" "smart" "+")) -> ("someone" "is" "red" "+"))
All round people are young.
((("someone" "is" "round" "+")) -> ("someone" "is" "young" "+"))
Quiet, smart people are white.
((("someone" "is" "quiet" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "white" "+"))
Red, quiet people are white.
((("someone" "is" "red" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "white" "+"))
Anne is furry.
True
1
proof
[(triple1 OR ((triple4) -> rule2))]
("Anne" "is" "furry" "+")
triple1
((triple4) -> (rule2 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is not red.
False
1
inv-proof
[(triple3 OR ((triple5) -> rule3) OR ((triple5 triple6) -> rule1) OR ((triple5 ((triple2 triple5) -> rule5)) -> rule1))]
("Anne" "is" "red" "-")
triple3
((triple5) -> (rule3 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
((triple5 triple6) -> (rule1 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
((triple5 ((triple2 triple5) -> (rule5 % int2))) -> (rule1 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Bob is young.
True
2
proof
[(((triple9) -> rule4))]
("Bob" "is" "young" "+")
((triple9) -> (rule4 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is not young.
False
2
inv-proof
[(((triple9) -> rule4))]
("Bob" "is" "young" "-")
((triple9) -> (rule4 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is not red.
Unknown
inv-rconc
[@1: Bob is red.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "red" "-")
Bob is white.
Unknown
rconc
[@2: Bob is white.[CWA. Example of deepest failure = (rule6 <- rule1 <- FAIL)]]
("Bob" "is" "white" "+")
@0: Anne is furry.[(triple1 OR ((triple4) -> rule2))] Anne is quiet.[(triple2)] Anne is red.[(triple3 OR ((triple5) -> rule3) OR ((triple5 triple6) -> rule1) OR ((triple5 ((triple2 triple5) -> rule5)) -> rule1))] Anne is round.[(triple4)] Anne is smart.[(triple5)] Anne is white.[(triple6 OR ((triple2 triple5) -> rule5) OR ((triple3 triple2) -> rule6) OR ((((triple5) -> rule3) triple2) -> rule6))] Anne is young.[(triple7 OR ((triple4) -> rule4))] Bob is quiet.[(triple8)] Bob is round.[(triple9)] Gary is furry.[(triple10 OR ((triple13) -> rule2))] Gary is quiet.[(triple11)] Gary is red.[(triple12 OR ((triple14) -> rule3) OR ((triple14 triple15) -> rule1) OR ((triple14 ((triple11 triple14) -> rule5)) -> rule1))] Gary is round.[(triple13)] Gary is smart.[(triple14)] Gary is white.[(triple15 OR ((triple11 triple14) -> rule5) OR ((triple12 triple11) -> rule6) OR ((((triple14) -> rule3) triple11) -> rule6))] Gary is young.[(triple16 OR ((triple13) -> rule4))] @1: Bob is furry.[(((triple9) -> rule2))] Bob is young.[(((triple9) -> rule4))]
Anne is furry.
("Anne" "is" "furry" "+")
triple1
((triple4) -> (rule2 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
triple2
Anne is red.
("Anne" "is" "red" "+")
triple3
((triple5) -> (rule3 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
((triple5 triple6) -> (rule1 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
((triple5 ((triple2 triple5) -> (rule5 % int2))) -> (rule1 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is round.
("Anne" "is" "round" "+")
triple4
Anne is smart.
("Anne" "is" "smart" "+")
triple5
Anne is white.
("Anne" "is" "white" "+")
triple6
((triple2 triple5) -> (rule5 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
((triple3 triple2) -> (rule6 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
((((triple5) -> (rule3 % int2)) triple2) -> (rule6 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
triple7
((triple4) -> (rule4 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
triple8
Bob is round.
("Bob" "is" "round" "+")
triple9
Gary is furry.
("Gary" "is" "furry" "+")
triple10
((triple13) -> (rule2 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
triple11
Gary is red.
("Gary" "is" "red" "+")
triple12
((triple14) -> (rule3 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
((triple14 triple15) -> (rule1 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
((triple14 ((triple11 triple14) -> (rule5 % int2))) -> (rule1 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
triple13
Gary is smart.
("Gary" "is" "smart" "+")
triple14
Gary is white.
("Gary" "is" "white" "+")
triple15
((triple11 triple14) -> (rule5 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
((triple12 triple11) -> (rule6 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
((((triple14) -> (rule3 % int2)) triple11) -> (rule6 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is young.
("Gary" "is" "young" "+")
triple16
((triple13) -> (rule4 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
((triple9) -> (rule2 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
((triple9) -> (rule4 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1