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