Anne is cold. Anne is green. Anne is smart. Anne is white. Charlie is furry. Charlie is quiet. Charlie is smart. Charlie is white. Fiona is quiet. Gary is white. All white people are smart. If someone is smart and white then they are furry.
Anne is cold.
("Anne" "is" "cold" "+")
Anne is green.
("Anne" "is" "green" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Anne is white.
("Anne" "is" "white" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
Gary is white.
("Gary" "is" "white" "+")
All white people are smart.
((("someone" "is" "white" "+")) -> ("someone" "is" "smart" "+"))
If someone is smart and white then they are furry.
((("someone" "is" "smart" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "furry" "+"))
Gary is white.
True
1
proof
[(triple10)]
("Gary" "is" "white" "+")
triple10
Charlie is not furry.
False
1
inv-proof
[(triple5 OR ((triple7 triple8) -> rule2) OR ((((triple8) -> rule1) triple8) -> rule2))]
("Charlie" "is" "furry" "-")
triple5
((triple7 triple8) -> (rule2 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
((((triple8) -> (rule1 % int2)) triple8) -> (rule2 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Fiona is not furry.
Unknown
inv-rconc
[@1: Fiona is furry.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Fiona" "is" "furry" "-")
Gary is cold.
Unknown
random
[@0: Gary is cold.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "cold" "+")
@0: Anne is cold.[(triple1)] Anne is green.[(triple2)] Anne is smart.[(triple3 OR ((triple4) -> rule1))] Anne is white.[(triple4)] Charlie is furry.[(triple5 OR ((triple7 triple8) -> rule2) OR ((((triple8) -> rule1) triple8) -> rule2))] Charlie is quiet.[(triple6)] Charlie is smart.[(triple7 OR ((triple8) -> rule1))] Charlie is white.[(triple8)] Fiona is quiet.[(triple9)] Gary is white.[(triple10)] @1: Anne is furry.[(((triple3 triple4) -> rule2) OR ((((triple4) -> rule1) triple4) -> rule2))] Gary is smart.[(((triple10) -> rule1))] @2: Gary is furry.[(((((triple10) -> rule1) triple10) -> rule2))]
Anne is cold.
("Anne" "is" "cold" "+")
triple1
Anne is green.
("Anne" "is" "green" "+")
triple2
Anne is smart.
("Anne" "is" "smart" "+")
triple3
((triple4) -> (rule1 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
triple4
Charlie is furry.
("Charlie" "is" "furry" "+")
triple5
((triple7 triple8) -> (rule2 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
((((triple8) -> (rule1 % int2)) triple8) -> (rule2 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple6
Charlie is smart.
("Charlie" "is" "smart" "+")
triple7
((triple8) -> (rule1 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
triple8
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple9
Gary is white.
("Gary" "is" "white" "+")
triple10
Anne is furry.
("Anne" "is" "furry" "+")
((triple3 triple4) -> (rule2 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
((((triple4) -> (rule1 % int2)) triple4) -> (rule2 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
((triple10) -> (rule1 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
((((triple10) -> (rule1 % int2)) triple10) -> (rule2 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2