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