Charlie is big. Charlie is blue. Charlie is furry. Charlie is green. Charlie is not smart. Dave is not big. Dave is cold. Dave is furry. Dave is green. Dave is red. Harry is furry. Harry is smart. All smart people are blue.
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is not smart.
("Charlie" "is" "smart" "-")
Dave is not big.
("Dave" "is" "big" "-")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is red.
("Dave" "is" "red" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is smart.
("Harry" "is" "smart" "+")
All smart people are blue.
((("someone" "is" "smart" "+")) -> ("someone" "is" "blue" "+"))
Harry is furry.
True
1
proof
[(triple11)]
("Harry" "is" "furry" "+")
triple11
Charlie is not big.
False
1
inv-proof
[(triple1)]
("Charlie" "is" "big" "-")
triple1
Harry is blue.
True
2
proof
[(((triple12) -> rule1))]
("Harry" "is" "blue" "+")
((triple12) -> (rule1 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is not blue.
False
2
inv-proof
[(((triple12) -> rule1))]
("Harry" "is" "blue" "-")
((triple12) -> (rule1 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Dave is not blue.
Unknown
inv-rconc
[@1: Dave is blue.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Dave" "is" "blue" "-")
Harry is red.
Unknown
random
[@0: Harry is red.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "red" "+")
Harry is not big.
Unknown
inv-random
[@0: Harry is big.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "big" "-")
Harry is green.
Unknown
random
[@0: Harry is green.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "green" "+")
@0: Charlie is big.[(triple1)] Charlie is blue.[(triple2)] Charlie is furry.[(triple3)] Charlie is green.[(triple4)] Charlie is not smart.[(triple5)] Dave is cold.[(triple7)] Dave is furry.[(triple8)] Dave is green.[(triple9)] Dave is not big.[(triple6)] Dave is red.[(triple10)] Harry is furry.[(triple11)] Harry is smart.[(triple12)] @1: Harry is blue.[(((triple12) -> rule1))]
Charlie is big.
("Charlie" "is" "big" "+")
triple1
Charlie is blue.
("Charlie" "is" "blue" "+")
triple2
Charlie is furry.
("Charlie" "is" "furry" "+")
triple3
Charlie is green.
("Charlie" "is" "green" "+")
triple4
Charlie is not smart.
("Charlie" "is" "smart" "-")
triple5
Dave is cold.
("Dave" "is" "cold" "+")
triple7
Dave is furry.
("Dave" "is" "furry" "+")
triple8
Dave is green.
("Dave" "is" "green" "+")
triple9
Dave is not big.
("Dave" "is" "big" "-")
triple6
Dave is red.
("Dave" "is" "red" "+")
triple10
Harry is furry.
("Harry" "is" "furry" "+")
triple11
Harry is smart.
("Harry" "is" "smart" "+")
triple12
Harry is blue.
("Harry" "is" "blue" "+")
((triple12) -> (rule1 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1