Anne is rough. Anne is not smart. Anne is white. Anne is young. Dave is furry. Dave is green. Dave is kind. Dave is rough. Dave is smart. Dave is young. Fiona is rough. Fiona is smart. Harry is furry. Harry is green. Harry is kind. Harry is smart. Kind things are rough. Green things are kind. If something is kind then it is white. White, kind things are green. If something is white and not green then it is smart. All smart, rough things are young.
Anne is rough.
("Anne" "is" "rough" "+")
Anne is not smart.
("Anne" "is" "smart" "-")
Anne is white.
("Anne" "is" "white" "+")
Anne is young.
("Anne" "is" "young" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Dave is young.
("Dave" "is" "young" "+")
Fiona is rough.
("Fiona" "is" "rough" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is smart.
("Harry" "is" "smart" "+")
Kind things are rough.
((("something" "is" "kind" "+")) -> ("something" "is" "rough" "+"))
Green things are kind.
((("something" "is" "green" "+")) -> ("something" "is" "kind" "+"))
If something is kind then it is white.
((("something" "is" "kind" "+")) -> ("something" "is" "white" "+"))
White, kind things are green.
((("something" "is" "white" "+") ("something" "is" "kind" "+")) -> ("something" "is" "green" "+"))
If something is white and not green then it is smart.
((("something" "is" "white" "+") ("something" "is" "green" "~")) -> ("something" "is" "smart" "+"))
All smart, rough things are young.
((("something" "is" "smart" "+") ("something" "is" "rough" "+")) -> ("something" "is" "young" "+"))
Dave is smart.
True
1
proof
[(triple9)]
("Dave" "is" "smart" "+")
triple9
Harry is not kind.
False
1
inv-proof
[(triple15 OR ((triple14) -> rule2))]
("Harry" "is" "kind" "-")
triple15
((triple14) -> (rule2 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Fiona is young.
True
3
proof
[(((triple12 triple11) -> rule6))]
("Fiona" "is" "young" "+")
((triple12 triple11) -> (rule6 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Dave is not white.
False
2
inv-proof
[(((triple7) -> rule3) OR ((((triple6) -> rule2)) -> rule3))]
("Dave" "is" "white" "-")
((triple7) -> (rule3 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
((((triple6) -> (rule2 % int2))) -> (rule3 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Fiona is not green.
Unknown
inv-rconc
[@2: Fiona is green.[CWA. Example of deepest failure = (rule4 <- rule2 <- FAIL)]]
("Fiona" "is" "green" "-")
Anne is kind.
Unknown
rconc
[@2: Anne is kind.[CWA. Example of deepest failure = (rule2 <- rule4 <- FAIL)]]
("Anne" "is" "kind" "+")
Fiona is not furry.
Unknown
inv-random
[@0: Fiona is furry.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "furry" "-")
Anne is furry.
Unknown
random
[@0: Anne is furry.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "furry" "+")
@0: Anne is not smart.[(triple2)] Anne is rough.[(triple1)] Anne is white.[(triple3)] Anne is young.[(triple4)] Dave is furry.[(triple5)] Dave is green.[(triple6 OR ((((triple7) -> rule3) triple7) -> rule4))] Dave is kind.[(triple7 OR ((triple6) -> rule2))] Dave is rough.[(triple8 OR ((triple7) -> rule1) OR ((((triple6) -> rule2)) -> rule1))] Dave is smart.[(triple9)] Dave is young.[(triple10 OR ((triple9 triple8) -> rule6) OR ((triple9 ((triple7) -> rule1)) -> rule6) OR ((triple9 ((((triple6) -> rule2)) -> rule1)) -> rule6))] Fiona is rough.[(triple11)] Fiona is smart.[(triple12)] Harry is furry.[(triple13)] Harry is green.[(triple14 OR ((((triple15) -> rule3) triple15) -> rule4))] Harry is kind.[(triple15 OR ((triple14) -> rule2))] Harry is smart.[(triple16)] @1: Dave is white.[(((triple7) -> rule3) OR ((((triple6) -> rule2)) -> rule3))] Fiona is young.[(((triple12 triple11) -> rule6))] Harry is rough.[(((triple15) -> rule1) OR ((((triple14) -> rule2)) -> rule1))] Harry is white.[(((triple15) -> rule3) OR ((((triple14) -> rule2)) -> rule3))] @2: Harry is young.[(((triple16 ((triple15) -> rule1)) -> rule6) OR ((triple16 ((((triple14) -> rule2)) -> rule1)) -> rule6))]
Anne is not smart.
("Anne" "is" "smart" "-")
triple2
Anne is rough.
("Anne" "is" "rough" "+")
triple1
Anne is white.
("Anne" "is" "white" "+")
triple3
Anne is young.
("Anne" "is" "young" "+")
triple4
Dave is furry.
("Dave" "is" "furry" "+")
triple5
Dave is green.
("Dave" "is" "green" "+")
triple6
((((triple7) -> (rule3 % int2)) triple7) -> (rule4 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
triple7
((triple6) -> (rule2 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
triple8
((triple7) -> (rule1 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
((((triple6) -> (rule2 % int2))) -> (rule1 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
triple9
Dave is young.
("Dave" "is" "young" "+")
triple10
((triple9 triple8) -> (rule6 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
((triple9 ((triple7) -> (rule1 % int2))) -> (rule6 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
((triple9 ((((triple6) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
int3
Fiona is rough.
("Fiona" "is" "rough" "+")
triple11
Fiona is smart.
("Fiona" "is" "smart" "+")
triple12
Harry is furry.
("Harry" "is" "furry" "+")
triple13
Harry is green.
("Harry" "is" "green" "+")
triple14
((((triple15) -> (rule3 % int2)) triple15) -> (rule4 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
triple15
((triple14) -> (rule2 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
triple16
Dave is white.
("Dave" "is" "white" "+")
((triple7) -> (rule3 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
((((triple6) -> (rule2 % int2))) -> (rule3 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Fiona is young.
("Fiona" "is" "young" "+")
((triple12 triple11) -> (rule6 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
((triple15) -> (rule1 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
((((triple14) -> (rule2 % int2))) -> (rule1 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
((triple15) -> (rule3 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
((((triple14) -> (rule2 % int2))) -> (rule3 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
((triple16 ((triple15) -> (rule1 % int2))) -> (rule6 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
((triple16 ((((triple14) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
int3