Anne is blue. Anne is quiet. Anne is red. Dave is young. Gary is young. Harry is furry. Harry is kind. If someone is white and kind then they are quiet. If someone is young then they are white. Red, kind people are blue. If someone is young then they are quiet. All furry people are young. If someone is blue then they are furry. If someone is kind and red then they are quiet. Blue people are white.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is red.
("Anne" "is" "red" "+")
Dave is young.
("Dave" "is" "young" "+")
Gary is young.
("Gary" "is" "young" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is kind.
("Harry" "is" "kind" "+")
If someone is white and kind then they are quiet.
((("someone" "is" "white" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "quiet" "+"))
If someone is young then they are white.
((("someone" "is" "young" "+")) -> ("someone" "is" "white" "+"))
Red, kind people are blue.
((("someone" "is" "red" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "blue" "+"))
If someone is young then they are quiet.
((("someone" "is" "young" "+")) -> ("someone" "is" "quiet" "+"))
All furry people are young.
((("someone" "is" "furry" "+")) -> ("someone" "is" "young" "+"))
If someone is blue then they are furry.
((("someone" "is" "blue" "+")) -> ("someone" "is" "furry" "+"))
If someone is kind and red then they are quiet.
((("someone" "is" "kind" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "quiet" "+"))
Blue people are white.
((("someone" "is" "blue" "+")) -> ("someone" "is" "white" "+"))
Anne is red.
True
1
proof
[(triple3)]
("Anne" "is" "red" "+")
triple3
Gary is not young.
False
1
inv-proof
[(triple5)]
("Gary" "is" "young" "-")
triple5
Dave is white.
True
2
proof
[(((triple4) -> rule2))]
("Dave" "is" "white" "+")
((triple4) -> (rule2 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is not white.
False
2
inv-proof
[(((triple4) -> rule2))]
("Dave" "is" "white" "-")
((triple4) -> (rule2 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is not blue.
Unknown
inv-rconc
[@1: Dave is blue.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Dave" "is" "blue" "-")
Harry is blue.
Unknown
rconc
[@1: Harry is blue.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Harry" "is" "blue" "+")
Dave is not red.
Unknown
inv-random
[@0: Dave is red.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "red" "-")
Gary is red.
Unknown
random
[@0: Gary is red.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "red" "+")
@0: Anne is blue.[(triple1)] Anne is quiet.[(triple2 OR ((((((triple1) -> rule6)) -> rule5)) -> rule4))] Anne is red.[(triple3)] Dave is young.[(triple4)] Gary is young.[(triple5)] Harry is furry.[(triple6)] Harry is kind.[(triple7)] @1: Anne is furry.[(((triple1) -> rule6))] Anne is white.[(((triple1) -> rule8) OR ((((((triple1) -> rule6)) -> rule5)) -> rule2))] Dave is quiet.[(((triple4) -> rule4))] Dave is white.[(((triple4) -> rule2))] Gary is quiet.[(((triple5) -> rule4))] Gary is white.[(((triple5) -> rule2))] Harry is young.[(((triple6) -> rule5))] @2: Anne is young.[(((((triple1) -> rule6)) -> rule5))] Harry is quiet.[(((((triple6) -> rule5)) -> rule4) OR ((((((triple6) -> rule5)) -> rule2) triple7) -> rule1))] Harry is white.[(((((triple6) -> rule5)) -> rule2))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Anne is quiet.
("Anne" "is" "quiet" "+")
triple2
((((((triple1) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
int3
Anne is red.
("Anne" "is" "red" "+")
triple3
Dave is young.
("Dave" "is" "young" "+")
triple4
Gary is young.
("Gary" "is" "young" "+")
triple5
Harry is furry.
("Harry" "is" "furry" "+")
triple6
Harry is kind.
("Harry" "is" "kind" "+")
triple7
Anne is furry.
("Anne" "is" "furry" "+")
((triple1) -> (rule6 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
((triple1) -> (rule8 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
((((((triple1) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
int3
Dave is quiet.
("Dave" "is" "quiet" "+")
((triple4) -> (rule4 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
((triple4) -> (rule2 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
((triple5) -> (rule4 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
((triple5) -> (rule2 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
((triple6) -> (rule5 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
((((triple1) -> (rule6 % int2))) -> (rule5 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
((((triple6) -> (rule5 % int2))) -> (rule4 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
((((((triple6) -> (rule5 % int3))) -> (rule2 % int2)) triple7) -> (rule1 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
int3
Harry is white.
("Harry" "is" "white" "+")
((((triple6) -> (rule5 % int2))) -> (rule2 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2