Anne is blue. Charlie is blue. Dave is smart. Harry is quiet. Young, white things are blue. If something is blue then it is furry. If something is furry and young then it is quiet. If Anne is quiet and Anne is blue then Anne is red. Blue things are smart. Smart things are red.
Anne is blue.
("Anne" "is" "blue" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Young, white things are blue.
((("something" "is" "young" "+") ("something" "is" "white" "+")) -> ("something" "is" "blue" "+"))
If something is blue then it is furry.
((("something" "is" "blue" "+")) -> ("something" "is" "furry" "+"))
If something is furry and young then it is quiet.
((("something" "is" "furry" "+") ("something" "is" "young" "+")) -> ("something" "is" "quiet" "+"))
If Anne is quiet and Anne is blue then Anne is red.
((("Anne" "is" "quiet" "+") ("Anne" "is" "blue" "+")) -> ("Anne" "is" "red" "+"))
Blue things are smart.
((("something" "is" "blue" "+")) -> ("something" "is" "smart" "+"))
Smart things are red.
((("something" "is" "smart" "+")) -> ("something" "is" "red" "+"))
Anne is blue.
True
1
proof
[(triple1)]
("Anne" "is" "blue" "+")
triple1
Anne is not blue.
False
1
inv-proof
[(triple1)]
("Anne" "is" "blue" "-")
triple1
Anne is furry.
True
2
proof
[(((triple1) -> rule2))]
("Anne" "is" "furry" "+")
((triple1) -> (rule2 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is not furry.
False
2
inv-proof
[(((triple1) -> rule2))]
("Anne" "is" "furry" "-")
((triple1) -> (rule2 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is red.
True
3
proof
[(((((triple1) -> rule5)) -> rule6))]
("Anne" "is" "red" "+")
((((triple1) -> (rule5 % int2))) -> (rule6 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Charlie is not red.
False
3
inv-proof
[(((((triple2) -> rule5)) -> rule6))]
("Charlie" "is" "red" "-")
((((triple2) -> (rule5 % int2))) -> (rule6 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Harry is not smart.
Unknown
inv-rconc
[@2: Harry is smart.[CWA. Example of deepest failure = (rule5 <- rule1 <- FAIL)]]
("Harry" "is" "smart" "-")
Dave is quiet.
Unknown
rconc
[@1: Dave is quiet.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Dave" "is" "quiet" "+")
Harry is not red.
Unknown
inv-rconc
[@3: Harry is red.[CWA. Example of deepest failure = (rule6 <- rule5 <- rule1 <- FAIL)]]
("Harry" "is" "red" "-")
Harry is young.
Unknown
random
[@0: Harry is young.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "young" "+")
Charlie is not white.
Unknown
inv-random
[@0: Charlie is white.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "white" "-")
Harry is white.
Unknown
random
[@0: Harry is white.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "white" "+")
@0: Anne is blue.[(triple1)] Charlie is blue.[(triple2)] Dave is smart.[(triple3)] Harry is quiet.[(triple4)] @1: Anne is furry.[(((triple1) -> rule2))] Anne is smart.[(((triple1) -> rule5))] Charlie is furry.[(((triple2) -> rule2))] Charlie is smart.[(((triple2) -> rule5))] Dave is red.[(((triple3) -> rule6))] @2: Anne is red.[(((((triple1) -> rule5)) -> rule6))] Charlie is red.[(((((triple2) -> rule5)) -> rule6))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Charlie is blue.
("Charlie" "is" "blue" "+")
triple2
Dave is smart.
("Dave" "is" "smart" "+")
triple3
Harry is quiet.
("Harry" "is" "quiet" "+")
triple4
Anne is furry.
("Anne" "is" "furry" "+")
((triple1) -> (rule2 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
((triple1) -> (rule5 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
((triple2) -> (rule2 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
((triple2) -> (rule5 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
((triple3) -> (rule6 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
((((triple1) -> (rule5 % int2))) -> (rule6 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
((((triple2) -> (rule5 % int2))) -> (rule6 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2