Anne is green. Anne is smart. Anne is young. Dave is green. Dave is red. Dave is white. Dave is young. Harry is green. Harry is kind. Harry is young. If Dave is green then Dave is smart. If someone is white then they are green. If Anne is smart then Anne is red. If Harry is green and Harry is smart then Harry is not nice. If someone is young then they are not nice. If someone is red and not white then they are smart. If someone is green then they are red. If someone is green and not nice then they are kind.
Anne is green.
("Anne" "is" "green" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Anne is young.
("Anne" "is" "young" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is white.
("Dave" "is" "white" "+")
Dave is young.
("Dave" "is" "young" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is young.
("Harry" "is" "young" "+")
If Dave is green then Dave is smart.
((("Dave" "is" "green" "+")) -> ("Dave" "is" "smart" "+"))
If someone is white then they are green.
((("someone" "is" "white" "+")) -> ("someone" "is" "green" "+"))
If Anne is smart then Anne is red.
((("Anne" "is" "smart" "+")) -> ("Anne" "is" "red" "+"))
If Harry is green and Harry is smart then Harry is not nice.
((("Harry" "is" "green" "+") ("Harry" "is" "smart" "+")) -> ("Harry" "is" "nice" "-"))
If someone is young then they are not nice.
((("someone" "is" "young" "+")) -> ("someone" "is" "nice" "-"))
If someone is red and not white then they are smart.
((("someone" "is" "red" "+") ("someone" "is" "white" "~")) -> ("someone" "is" "smart" "+"))
If someone is green then they are red.
((("someone" "is" "green" "+")) -> ("someone" "is" "red" "+"))
If someone is green and not nice then they are kind.
((("someone" "is" "green" "+") ("someone" "is" "nice" "~")) -> ("someone" "is" "kind" "+"))
Dave is white.
True
1
proof
[(triple6)]
("Dave" "is" "white" "+")
triple6
Dave is not green.
False
1
inv-proof
[(triple4 OR ((triple6) -> rule2))]
("Dave" "is" "green" "-")
triple4
((triple6) -> (rule2 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is smart.
True
2
proof
[(((triple4) -> rule1) OR ((((triple6) -> rule2)) -> rule1))]
("Dave" "is" "smart" "+")
((triple4) -> (rule1 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
((((triple6) -> (rule2 % int2))) -> (rule1 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Anne is nice.
False
2
inv-proof
[(((triple3) -> rule5))]
("Anne" "is" "nice" "+")
((triple3) -> (rule5 % int1))
Anne is not nice.
("Anne" "is" "nice" "-")
int1
Dave is kind.
True
4
proof
[(((triple4 ((triple7) -> rule5)) -> rule8) OR ((((triple6) -> rule2) ((triple7) -> rule5)) -> rule8))]
("Dave" "is" "kind" "+")
((triple4 ((triple7) -> (rule5 % int2))) -> (rule8 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is not nice.
("Dave" "is" "nice" "-")
int2
((((triple6) -> (rule2 % int3)) ((triple7) -> (rule5 % int2))) -> (rule8 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is not nice.
("Dave" "is" "nice" "-")
int2
Dave is green.
("Dave" "is" "green" "+")
int3
Dave is not kind.
False
4
inv-proof
[(((triple4 ((triple7) -> rule5)) -> rule8) OR ((((triple6) -> rule2) ((triple7) -> rule5)) -> rule8))]
("Dave" "is" "kind" "-")
((triple4 ((triple7) -> (rule5 % int2))) -> (rule8 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is not nice.
("Dave" "is" "nice" "-")
int2
((((triple6) -> (rule2 % int3)) ((triple7) -> (rule5 % int2))) -> (rule8 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is not nice.
("Dave" "is" "nice" "-")
int2
Dave is green.
("Dave" "is" "green" "+")
int3
Harry is not smart.
Unknown
inv-rconc
[@1: Harry is smart.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Harry" "is" "smart" "-")
Harry is white.
Unknown
random
[@0: Harry is white.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "white" "+")
@0: Anne is green.[(triple1)] Anne is smart.[(triple2)] Anne is young.[(triple3)] Dave is green.[(triple4 OR ((triple6) -> rule2))] Dave is red.[(triple5 OR ((triple4) -> rule7) OR ((((triple6) -> rule2)) -> rule7))] Dave is white.[(triple6)] Dave is young.[(triple7)] Harry is green.[(triple8)] Harry is kind.[(triple9 OR ((triple8 ((triple10) -> rule5)) -> rule8))] Harry is young.[(triple10)] @1: Anne is not nice.[(((triple3) -> rule5))] Anne is red.[(((triple1) -> rule7) OR ((triple2) -> rule3))] Dave is not nice.[(((triple7) -> rule5))] Dave is smart.[(((triple4) -> rule1) OR ((((triple6) -> rule2)) -> rule1))] Harry is not nice.[(((triple10) -> rule5))] Harry is red.[(((triple8) -> rule7))] @2: Anne is kind.[(((triple1 ((triple3) -> rule5)) -> rule8))] Dave is kind.[(((triple4 ((triple7) -> rule5)) -> rule8) OR ((((triple6) -> rule2) ((triple7) -> rule5)) -> rule8))]
Anne is green.
("Anne" "is" "green" "+")
triple1
Anne is smart.
("Anne" "is" "smart" "+")
triple2
Anne is young.
("Anne" "is" "young" "+")
triple3
Dave is green.
("Dave" "is" "green" "+")
triple4
((triple6) -> (rule2 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
triple5
((triple4) -> (rule7 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
((((triple6) -> (rule2 % int2))) -> (rule7 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
triple6
Dave is young.
("Dave" "is" "young" "+")
triple7
Harry is green.
("Harry" "is" "green" "+")
triple8
Harry is kind.
("Harry" "is" "kind" "+")
triple9
((triple8 ((triple10) -> (rule5 % int2))) -> (rule8 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is not nice.
("Harry" "is" "nice" "-")
int2
Harry is young.
("Harry" "is" "young" "+")
triple10
Anne is not nice.
("Anne" "is" "nice" "-")
((triple3) -> (rule5 % int1))
Anne is not nice.
("Anne" "is" "nice" "-")
int1
Anne is red.
("Anne" "is" "red" "+")
((triple1) -> (rule7 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
((triple2) -> (rule3 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Dave is not nice.
("Dave" "is" "nice" "-")
((triple7) -> (rule5 % int1))
Dave is not nice.
("Dave" "is" "nice" "-")
int1
Dave is smart.
("Dave" "is" "smart" "+")
((triple4) -> (rule1 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
((((triple6) -> (rule2 % int2))) -> (rule1 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Harry is not nice.
("Harry" "is" "nice" "-")
((triple10) -> (rule5 % int1))
Harry is not nice.
("Harry" "is" "nice" "-")
int1
Harry is red.
("Harry" "is" "red" "+")
((triple8) -> (rule7 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
((triple1 ((triple3) -> (rule5 % int2))) -> (rule8 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is not nice.
("Anne" "is" "nice" "-")
int2
Dave is kind.
("Dave" "is" "kind" "+")
((triple4 ((triple7) -> (rule5 % int2))) -> (rule8 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is not nice.
("Dave" "is" "nice" "-")
int2
((((triple6) -> (rule2 % int3)) ((triple7) -> (rule5 % int2))) -> (rule8 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is not nice.
("Dave" "is" "nice" "-")
int2
Dave is green.
("Dave" "is" "green" "+")
int3