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