Anne is cold. Anne is kind. Anne is not red. Anne is smart. Dave is green. Dave is kind. Dave is rough. Dave is young. Gary is not green. Harry is cold. Harry is green. Harry is not kind. Harry is red. Harry is rough. Harry is not smart. Harry is young. If someone is cold and not red then they are rough. If someone is kind and not cold then they are not rough. If someone is kind then they are rough. If someone is cold then they are young. All rough people are young. If someone is young and red then they are not kind.
Anne is cold.
("Anne" "is" "cold" "+")
Anne is kind.
("Anne" "is" "kind" "+")
Anne is not red.
("Anne" "is" "red" "-")
Anne is smart.
("Anne" "is" "smart" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Dave is young.
("Dave" "is" "young" "+")
Gary is not green.
("Gary" "is" "green" "-")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is not kind.
("Harry" "is" "kind" "-")
Harry is red.
("Harry" "is" "red" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is not smart.
("Harry" "is" "smart" "-")
Harry is young.
("Harry" "is" "young" "+")
If someone is cold and not red then they are rough.
((("someone" "is" "cold" "+") ("someone" "is" "red" "~")) -> ("someone" "is" "rough" "+"))
If someone is kind and not cold then they are not rough.
((("someone" "is" "kind" "+") ("someone" "is" "cold" "~")) -> ("someone" "is" "rough" "-"))
If someone is kind then they are rough.
((("someone" "is" "kind" "+")) -> ("someone" "is" "rough" "+"))
If someone is cold then they are young.
((("someone" "is" "cold" "+")) -> ("someone" "is" "young" "+"))
All rough people are young.
((("someone" "is" "rough" "+")) -> ("someone" "is" "young" "+"))
If someone is young and red then they are not kind.
((("someone" "is" "young" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "kind" "-"))
Dave is young.
True
1
proof
[(triple8 OR ((triple7) -> rule5) OR ((((triple6) -> rule3)) -> rule5))]
("Dave" "is" "young" "+")
triple8
((triple7) -> (rule5 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
((((triple6) -> (rule3 % int2))) -> (rule5 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is not young.
False
1
inv-proof
[(triple8 OR ((triple7) -> rule5) OR ((((triple6) -> rule3)) -> rule5))]
("Dave" "is" "young" "-")
triple8
((triple7) -> (rule5 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
((((triple6) -> (rule3 % int2))) -> (rule5 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Anne is young.
True
2
proof
[(((triple1) -> rule4) OR ((((triple2) -> rule3)) -> rule5) OR ((((triple1 triple3) -> rule1)) -> rule5))]
("Anne" "is" "young" "+")
((triple1) -> (rule4 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
((((triple2) -> (rule3 % int2))) -> (rule5 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
((((triple1 triple3) -> (rule1 % int2))) -> (rule5 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is not rough.
False
2
inv-proof
[(((triple2) -> rule3) OR ((triple1 triple3) -> rule1))]
("Anne" "is" "rough" "-")
((triple2) -> (rule3 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
((triple1 triple3) -> (rule1 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Gary is not rough.
Unknown
inv-rconc
[@1: Gary is rough.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Gary" "is" "rough" "-")
Gary is young.
Unknown
rconc
[@2: Gary is young.[CWA. Example of deepest failure = (rule5 <- rule1 <- FAIL)]]
("Gary" "is" "young" "+")
Anne is not green.
Unknown
inv-random
[@0: Anne is green.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "green" "-")
Gary is cold.
Unknown
random
[@0: Gary is cold.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "cold" "+")
@0: Anne is cold.[(triple1)] Anne is kind.[(triple2)] Anne is not red.[(triple3)] Anne is smart.[(triple4)] Dave is green.[(triple5)] Dave is kind.[(triple6)] Dave is rough.[(triple7 OR ((triple6) -> rule3))] Dave is young.[(triple8 OR ((triple7) -> rule5) OR ((((triple6) -> rule3)) -> rule5))] Gary is not green.[(triple9)] Harry is cold.[(triple10)] Harry is green.[(triple11)] Harry is not kind.[(triple12 OR ((triple16 triple13) -> rule6) OR ((((triple10) -> rule4) triple13) -> rule6) OR ((((triple14) -> rule5) triple13) -> rule6))] Harry is not smart.[(triple15)] Harry is red.[(triple13)] Harry is rough.[(triple14)] Harry is young.[(triple16 OR ((triple10) -> rule4) OR ((triple14) -> rule5))] @1: Anne is rough.[(((triple2) -> rule3) OR ((triple1 triple3) -> rule1))] Anne is young.[(((triple1) -> rule4) OR ((((triple2) -> rule3)) -> rule5) OR ((((triple1 triple3) -> rule1)) -> rule5))]
Anne is cold.
("Anne" "is" "cold" "+")
triple1
Anne is kind.
("Anne" "is" "kind" "+")
triple2
Anne is not red.
("Anne" "is" "red" "-")
triple3
Anne is smart.
("Anne" "is" "smart" "+")
triple4
Dave is green.
("Dave" "is" "green" "+")
triple5
Dave is kind.
("Dave" "is" "kind" "+")
triple6
Dave is rough.
("Dave" "is" "rough" "+")
triple7
((triple6) -> (rule3 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
triple8
((triple7) -> (rule5 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
((((triple6) -> (rule3 % int2))) -> (rule5 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Gary is not green.
("Gary" "is" "green" "-")
triple9
Harry is cold.
("Harry" "is" "cold" "+")
triple10
Harry is green.
("Harry" "is" "green" "+")
triple11
Harry is not kind.
("Harry" "is" "kind" "-")
triple12
((triple16 triple13) -> (rule6 % int1))
Harry is not kind.
("Harry" "is" "kind" "-")
int1
((((triple10) -> (rule4 % int2)) triple13) -> (rule6 % int1))
Harry is not kind.
("Harry" "is" "kind" "-")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
((((triple14) -> (rule5 % int2)) triple13) -> (rule6 % int1))
Harry is not kind.
("Harry" "is" "kind" "-")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is not smart.
("Harry" "is" "smart" "-")
triple15
Harry is red.
("Harry" "is" "red" "+")
triple13
Harry is rough.
("Harry" "is" "rough" "+")
triple14
Harry is young.
("Harry" "is" "young" "+")
triple16
((triple10) -> (rule4 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
((triple14) -> (rule5 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
((triple2) -> (rule3 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
((triple1 triple3) -> (rule1 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
((triple1) -> (rule4 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
((((triple2) -> (rule3 % int2))) -> (rule5 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
((((triple1 triple3) -> (rule1 % int2))) -> (rule5 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2