Anne is blue. Anne is nice. Anne is red. Anne is round. Anne is smart. Dave is young. Gary is red. Gary is round. Harry is blue. Harry is green. Harry is red. Harry is smart. If someone is young then they are blue. If Gary is green then Gary is blue. Blue people are nice.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is round.
("Anne" "is" "round" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Dave is young.
("Dave" "is" "young" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is round.
("Gary" "is" "round" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is smart.
("Harry" "is" "smart" "+")
If someone is young then they are blue.
((("someone" "is" "young" "+")) -> ("someone" "is" "blue" "+"))
If Gary is green then Gary is blue.
((("Gary" "is" "green" "+")) -> ("Gary" "is" "blue" "+"))
Blue people are nice.
((("someone" "is" "blue" "+")) -> ("someone" "is" "nice" "+"))
Harry is blue.
True
1
proof
[(triple9)]
("Harry" "is" "blue" "+")
triple9
Anne is not blue.
False
1
inv-proof
[(triple1)]
("Anne" "is" "blue" "-")
triple1
Harry is nice.
True
2
proof
[(((triple9) -> rule3))]
("Harry" "is" "nice" "+")
((triple9) -> (rule3 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Dave is not blue.
False
2
inv-proof
[(((triple6) -> rule1))]
("Dave" "is" "blue" "-")
((triple6) -> (rule1 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is nice.
True
3
proof
[(((((triple6) -> rule1)) -> rule3))]
("Dave" "is" "nice" "+")
((((triple6) -> (rule1 % int2))) -> (rule3 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is not nice.
False
3
inv-proof
[(((((triple6) -> rule1)) -> rule3))]
("Dave" "is" "nice" "-")
((((triple6) -> (rule1 % int2))) -> (rule3 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Gary is not blue.
Unknown
inv-rconc
[@1: Gary is blue.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Gary" "is" "blue" "-")
Gary is nice.
Unknown
rconc
[@2: Gary is nice.[CWA. Example of deepest failure = (rule3 <- rule1 <- FAIL)]]
("Gary" "is" "nice" "+")
Anne is not green.
Unknown
inv-random
[@0: Anne is green.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "green" "-")
Anne is young.
Unknown
random
[@0: Anne is young.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "young" "+")
Gary is not green.
Unknown
inv-random
[@0: Gary is green.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "green" "-")
Harry is round.
Unknown
random
[@0: Harry is round.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "round" "+")
@0: Anne is blue.[(triple1)] Anne is nice.[(triple2 OR ((triple1) -> rule3))] Anne is red.[(triple3)] Anne is round.[(triple4)] Anne is smart.[(triple5)] Dave is young.[(triple6)] Gary is red.[(triple7)] Gary is round.[(triple8)] Harry is blue.[(triple9)] Harry is green.[(triple10)] Harry is red.[(triple11)] Harry is smart.[(triple12)] @1: Dave is blue.[(((triple6) -> rule1))] Harry is nice.[(((triple9) -> rule3))] @2: Dave is nice.[(((((triple6) -> rule1)) -> rule3))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Anne is nice.
("Anne" "is" "nice" "+")
triple2
((triple1) -> (rule3 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
triple3
Anne is round.
("Anne" "is" "round" "+")
triple4
Anne is smart.
("Anne" "is" "smart" "+")
triple5
Dave is young.
("Dave" "is" "young" "+")
triple6
Gary is red.
("Gary" "is" "red" "+")
triple7
Gary is round.
("Gary" "is" "round" "+")
triple8
Harry is blue.
("Harry" "is" "blue" "+")
triple9
Harry is green.
("Harry" "is" "green" "+")
triple10
Harry is red.
("Harry" "is" "red" "+")
triple11
Harry is smart.
("Harry" "is" "smart" "+")
triple12
Dave is blue.
("Dave" "is" "blue" "+")
((triple6) -> (rule1 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
((triple9) -> (rule3 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
((((triple6) -> (rule1 % int2))) -> (rule3 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2