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