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