Charlie is blue. Charlie is green. Charlie is kind. Charlie is nice. Charlie is red. Dave is blue. Dave is kind. Dave is quiet. Dave is smart. Erin is green. Erin is nice. Erin is quiet. Harry is blue. Harry is red. Harry is smart. If someone is quiet then they are nice. Quiet, red people are blue. If someone is red and blue then they are kind. If someone is blue and kind then they are quiet. If someone is smart and green then they are nice. If someone is quiet and red then they are nice. If someone is quiet and kind then they are blue. If Harry is nice and Harry is smart then Harry is blue.
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is smart.
("Harry" "is" "smart" "+")
If someone is quiet then they are nice.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "nice" "+"))
Quiet, red people are blue.
((("someone" "is" "quiet" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "blue" "+"))
If someone is red and blue then they are kind.
((("someone" "is" "red" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "kind" "+"))
If someone is blue and kind then they are quiet.
((("someone" "is" "blue" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "quiet" "+"))
If someone is smart and green then they are nice.
((("someone" "is" "smart" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "nice" "+"))
If someone is quiet and red then they are nice.
((("someone" "is" "quiet" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "nice" "+"))
If someone is quiet and kind then they are blue.
((("someone" "is" "quiet" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "blue" "+"))
If Harry is nice and Harry is smart then Harry is blue.
((("Harry" "is" "nice" "+") ("Harry" "is" "smart" "+")) -> ("Harry" "is" "blue" "+"))
Charlie is green.
True
1
proof
[(triple2)]
("Charlie" "is" "green" "+")
triple2
Charlie is not nice.
False
1
inv-proof
[(triple4 OR ((((triple1 triple3) -> rule4)) -> rule1) OR ((((triple1 triple3) -> rule4) triple5) -> rule6) OR ((((triple1 ((triple5 triple1) -> rule3)) -> rule4)) -> rule1) OR ((((triple1 ((triple5 triple1) -> rule3)) -> rule4) triple5) -> rule6))]
("Charlie" "is" "nice" "-")
triple4
((((triple1 triple3) -> (rule4 % int2))) -> (rule1 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
((((triple1 triple3) -> (rule4 % int2)) triple5) -> (rule6 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
((((triple1 ((triple5 triple1) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3
((((triple1 ((triple5 triple1) -> (rule3 % int3))) -> (rule4 % int2)) triple5) -> (rule6 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3
Erin is not kind.
Unknown
inv-rconc
[@1: Erin is kind.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Erin" "is" "kind" "-")
Dave is green.
Unknown
random
[@0: Dave is green.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "green" "+")
@0: Charlie is blue.[(triple1)] Charlie is green.[(triple2)] Charlie is kind.[(triple3 OR ((triple5 triple1) -> rule3))] Charlie is nice.[(triple4 OR ((((triple1 triple3) -> rule4)) -> rule1) OR ((((triple1 triple3) -> rule4) triple5) -> rule6) OR ((((triple1 ((triple5 triple1) -> rule3)) -> rule4)) -> rule1) OR ((((triple1 ((triple5 triple1) -> rule3)) -> rule4) triple5) -> rule6))] Charlie is red.[(triple5)] Dave is blue.[(triple6 OR ((triple8 triple7) -> rule7))] Dave is kind.[(triple7)] Dave is quiet.[(triple8 OR ((triple6 triple7) -> rule4))] Dave is smart.[(triple9)] Erin is green.[(triple10)] Erin is nice.[(triple11 OR ((triple12) -> rule1))] Erin is quiet.[(triple12)] Harry is blue.[(triple13)] Harry is red.[(triple14)] Harry is smart.[(triple15)] @1: Charlie is quiet.[(((triple1 triple3) -> rule4) OR ((triple1 ((triple5 triple1) -> rule3)) -> rule4))] Dave is nice.[(((triple8) -> rule1) OR ((((triple6 triple7) -> rule4)) -> rule1))] Harry is kind.[(((triple14 triple13) -> rule3))] @2: Harry is quiet.[(((triple13 ((triple14 triple13) -> rule3)) -> rule4))] @3: Harry is nice.[(((((triple13 ((triple14 triple13) -> rule3)) -> rule4)) -> rule1) OR ((((triple13 ((triple14 triple13) -> rule3)) -> rule4) triple14) -> rule6))]
Charlie is blue.
("Charlie" "is" "blue" "+")
triple1
Charlie is green.
("Charlie" "is" "green" "+")
triple2
Charlie is kind.
("Charlie" "is" "kind" "+")
triple3
((triple5 triple1) -> (rule3 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
triple4
((((triple1 triple3) -> (rule4 % int2))) -> (rule1 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
((((triple1 triple3) -> (rule4 % int2)) triple5) -> (rule6 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
((((triple1 ((triple5 triple1) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3
((((triple1 ((triple5 triple1) -> (rule3 % int3))) -> (rule4 % int2)) triple5) -> (rule6 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3
Charlie is red.
("Charlie" "is" "red" "+")
triple5
Dave is blue.
("Dave" "is" "blue" "+")
triple6
((triple8 triple7) -> (rule7 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
triple7
Dave is quiet.
("Dave" "is" "quiet" "+")
triple8
((triple6 triple7) -> (rule4 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
triple9
Erin is green.
("Erin" "is" "green" "+")
triple10
Erin is nice.
("Erin" "is" "nice" "+")
triple11
((triple12) -> (rule1 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
triple12
Harry is blue.
("Harry" "is" "blue" "+")
triple13
Harry is red.
("Harry" "is" "red" "+")
triple14
Harry is smart.
("Harry" "is" "smart" "+")
triple15
Charlie is quiet.
("Charlie" "is" "quiet" "+")
((triple1 triple3) -> (rule4 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
((triple1 ((triple5 triple1) -> (rule3 % int2))) -> (rule4 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
((triple8) -> (rule1 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
((((triple6 triple7) -> (rule4 % int2))) -> (rule1 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
((triple14 triple13) -> (rule3 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
((triple13 ((triple14 triple13) -> (rule3 % int2))) -> (rule4 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
((((triple13 ((triple14 triple13) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
int3
((((triple13 ((triple14 triple13) -> (rule3 % int3))) -> (rule4 % int2)) triple14) -> (rule6 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
int3