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