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