Anne is young. Dave is kind. Gary is kind. Harry is blue. Young things are kind. All blue things are round. If something is kind and round then it is green. If Dave is kind then Dave is blue. Kind things are green. If Dave is blue and Dave is round then Dave is rough.
Anne is young.
("Anne" "is" "young" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Young things are kind.
((("something" "is" "young" "+")) -> ("something" "is" "kind" "+"))
All blue things are round.
((("something" "is" "blue" "+")) -> ("something" "is" "round" "+"))
If something is kind and round then it is green.
((("something" "is" "kind" "+") ("something" "is" "round" "+")) -> ("something" "is" "green" "+"))
If Dave is kind then Dave is blue.
((("Dave" "is" "kind" "+")) -> ("Dave" "is" "blue" "+"))
Kind things are green.
((("something" "is" "kind" "+")) -> ("something" "is" "green" "+"))
If Dave is blue and Dave is round then Dave is rough.
((("Dave" "is" "blue" "+") ("Dave" "is" "round" "+")) -> ("Dave" "is" "rough" "+"))
Harry is blue.
True
1
proof
[(triple4)]
("Harry" "is" "blue" "+")
triple4
Anne is not young.
False
1
inv-proof
[(triple1)]
("Anne" "is" "young" "-")
triple1
Dave is blue.
True
2
proof
[(((triple2) -> rule4))]
("Dave" "is" "blue" "+")
((triple2) -> (rule4 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Gary is not green.
False
2
inv-proof
[(((triple3) -> rule5))]
("Gary" "is" "green" "-")
((triple3) -> (rule5 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Anne is green.
True
3
proof
[(((((triple1) -> rule1)) -> rule5))]
("Anne" "is" "green" "+")
((((triple1) -> (rule1 % int2))) -> (rule5 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is not green.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule5))]
("Anne" "is" "green" "-")
((((triple1) -> (rule1 % int2))) -> (rule5 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Dave is rough.
True
6
proof
[(((((triple2) -> rule4) ((((triple2) -> rule4)) -> rule2)) -> rule6))]
("Dave" "is" "rough" "+")
((((triple2) -> (rule4 % int3)) ((((triple2) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3
Dave is not rough.
False
6
inv-proof
[(((((triple2) -> rule4) ((((triple2) -> rule4)) -> rule2)) -> rule6))]
("Dave" "is" "rough" "-")
((((triple2) -> (rule4 % int3)) ((((triple2) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3
Gary is not round.
Unknown
inv-rconc
[@1: Gary is round.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Gary" "is" "round" "-")
Harry is kind.
Unknown
rconc
[@1: Harry is kind.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Harry" "is" "kind" "+")
Harry is not green.
Unknown
inv-rconc
[@2: Harry is green.[CWA. Example of deepest failure = (rule3 <- rule1 <- FAIL)]]
("Harry" "is" "green" "-")
Anne is round.
Unknown
rconc
[@1: Anne is round.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Anne" "is" "round" "+")
Anne is not cold.
Unknown
inv-random
[@0: Anne is cold.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "cold" "-")
Harry is cold.
Unknown
random
[@0: Harry is cold.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "cold" "+")
Gary is not rough.
Unknown
inv-random
[@0: Gary is rough.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "rough" "-")
Dave is cold.
Unknown
random
[@0: Dave is cold.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "cold" "+")
@0: Anne is young.[(triple1)] Dave is kind.[(triple2)] Gary is kind.[(triple3)] Harry is blue.[(triple4)] @1: Anne is kind.[(((triple1) -> rule1))] Dave is blue.[(((triple2) -> rule4))] Dave is green.[(((triple2) -> rule5) OR ((triple2 ((((triple2) -> rule4)) -> rule2)) -> rule3))] Gary is green.[(((triple3) -> rule5))] Harry is round.[(((triple4) -> rule2))] @2: Anne is green.[(((((triple1) -> rule1)) -> rule5))] Dave is round.[(((((triple2) -> rule4)) -> rule2))] @3: Dave is rough.[(((((triple2) -> rule4) ((((triple2) -> rule4)) -> rule2)) -> rule6))]
Anne is young.
("Anne" "is" "young" "+")
triple1
Dave is kind.
("Dave" "is" "kind" "+")
triple2
Gary is kind.
("Gary" "is" "kind" "+")
triple3
Harry is blue.
("Harry" "is" "blue" "+")
triple4
Anne is kind.
("Anne" "is" "kind" "+")
((triple1) -> (rule1 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
((triple2) -> (rule4 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
((triple2) -> (rule5 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
((triple2 ((((triple2) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3
Gary is green.
("Gary" "is" "green" "+")
((triple3) -> (rule5 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
((triple4) -> (rule2 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
((((triple1) -> (rule1 % int2))) -> (rule5 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
((((triple2) -> (rule4 % int2))) -> (rule2 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
((((triple2) -> (rule4 % int3)) ((((triple2) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3