Charlie is cold. Charlie is furry. Charlie is green. Charlie is kind. Charlie is red. Charlie is white. Dave is furry. Dave is kind. Dave is quiet. Dave is white. Fiona is furry. Fiona is quiet. Fiona is red. Harry is furry. Harry is green. Harry is quiet. If something is kind then it is furry. Green things are kind. All kind things are furry. Cold things are red. If something is furry and green then it is kind. If something is cold then it is white. If Harry is kind then Harry is green. Cold, kind things are red.
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is white.
("Dave" "is" "white" "+")
Fiona is furry.
("Fiona" "is" "furry" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
Fiona is red.
("Fiona" "is" "red" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
If something is kind then it is furry.
((("something" "is" "kind" "+")) -> ("something" "is" "furry" "+"))
Green things are kind.
((("something" "is" "green" "+")) -> ("something" "is" "kind" "+"))
All kind things are furry.
((("something" "is" "kind" "+")) -> ("something" "is" "furry" "+"))
Cold things are red.
((("something" "is" "cold" "+")) -> ("something" "is" "red" "+"))
If something is furry and green then it is kind.
((("something" "is" "furry" "+") ("something" "is" "green" "+")) -> ("something" "is" "kind" "+"))
If something is cold then it is white.
((("something" "is" "cold" "+")) -> ("something" "is" "white" "+"))
If Harry is kind then Harry is green.
((("Harry" "is" "kind" "+")) -> ("Harry" "is" "green" "+"))
Cold, kind things are red.
((("something" "is" "cold" "+") ("something" "is" "kind" "+")) -> ("something" "is" "red" "+"))
Charlie is white.
True
1
proof
[(triple6 OR ((triple1) -> rule6))]
("Charlie" "is" "white" "+")
triple6
((triple1) -> (rule6 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Fiona is not furry.
False
1
inv-proof
[(triple11)]
("Fiona" "is" "furry" "-")
triple11
Dave is not red.
Unknown
inv-rconc
[@1: Dave is red.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Dave" "is" "red" "-")
Harry is cold.
Unknown
random
[@0: Harry is cold.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "cold" "+")
@0: Charlie is cold.[(triple1)] Charlie is furry.[(triple2 OR ((triple4) -> rule1) OR ((triple4) -> rule3) OR ((((triple3) -> rule2)) -> rule1) OR ((((triple3) -> rule2)) -> rule3))] Charlie is green.[(triple3)] Charlie is kind.[(triple4 OR ((triple3) -> rule2) OR ((triple2 triple3) -> rule5))] Charlie is red.[(triple5 OR ((triple1) -> rule4) OR ((triple1 triple4) -> rule8) OR ((triple1 ((triple3) -> rule2)) -> rule8) OR ((triple1 ((triple2 triple3) -> rule5)) -> rule8))] Charlie is white.[(triple6 OR ((triple1) -> rule6))] Dave is furry.[(triple7 OR ((triple8) -> rule1) OR ((triple8) -> rule3))] Dave is kind.[(triple8)] Dave is quiet.[(triple9)] Dave is white.[(triple10)] Fiona is furry.[(triple11)] Fiona is quiet.[(triple12)] Fiona is red.[(triple13)] Harry is furry.[(triple14 OR ((((triple15) -> rule2)) -> rule1) OR ((((triple15) -> rule2)) -> rule3))] Harry is green.[(triple15)] Harry is quiet.[(triple16)] @1: Harry is kind.[(((triple15) -> rule2) OR ((triple14 triple15) -> rule5))]
Charlie is cold.
("Charlie" "is" "cold" "+")
triple1
Charlie is furry.
("Charlie" "is" "furry" "+")
triple2
((triple4) -> (rule1 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
((triple4) -> (rule3 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
((((triple3) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
((((triple3) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
triple3
Charlie is kind.
("Charlie" "is" "kind" "+")
triple4
((triple3) -> (rule2 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
((triple2 triple3) -> (rule5 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
triple5
((triple1) -> (rule4 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
((triple1 triple4) -> (rule8 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
((triple1 ((triple3) -> (rule2 % int2))) -> (rule8 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
((triple1 ((triple2 triple3) -> (rule5 % int2))) -> (rule8 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
triple6
((triple1) -> (rule6 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
triple7
((triple8) -> (rule1 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
((triple8) -> (rule3 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
triple8
Dave is quiet.
("Dave" "is" "quiet" "+")
triple9
Dave is white.
("Dave" "is" "white" "+")
triple10
Fiona is furry.
("Fiona" "is" "furry" "+")
triple11
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple12
Fiona is red.
("Fiona" "is" "red" "+")
triple13
Harry is furry.
("Harry" "is" "furry" "+")
triple14
((((triple15) -> (rule2 % int2))) -> (rule1 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
((((triple15) -> (rule2 % int2))) -> (rule3 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
triple15
Harry is quiet.
("Harry" "is" "quiet" "+")
triple16
Harry is kind.
("Harry" "is" "kind" "+")
((triple15) -> (rule2 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
((triple14 triple15) -> (rule5 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1