Dave is big. Dave is green. Erin is quiet. Gary is big. Gary is cold. Gary is green. Gary is kind. Gary is quiet. Gary is rough. Gary is smart. Harry is big. Harry is cold. Harry is green. Harry is kind. Harry is rough. All cold things are smart. All rough things are green.
Dave is big.
("Dave" "is" "big" "+")
Dave is green.
("Dave" "is" "green" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is rough.
("Harry" "is" "rough" "+")
All cold things are smart.
((("something" "is" "cold" "+")) -> ("something" "is" "smart" "+"))
All rough things are green.
((("something" "is" "rough" "+")) -> ("something" "is" "green" "+"))
Gary is rough.
True
1
proof
[(triple9)]
("Gary" "is" "rough" "+")
triple9
Harry is not cold.
False
1
inv-proof
[(triple12)]
("Harry" "is" "cold" "-")
triple12
Erin is not smart.
Unknown
inv-rconc
[@1: Erin is smart.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Erin" "is" "smart" "-")
Dave is quiet.
Unknown
random
[@0: Dave is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "quiet" "+")
@0: Dave is big.[(triple1)] Dave is green.[(triple2)] Erin is quiet.[(triple3)] Gary is big.[(triple4)] Gary is cold.[(triple5)] Gary is green.[(triple6 OR ((triple9) -> rule2))] Gary is kind.[(triple7)] Gary is quiet.[(triple8)] Gary is rough.[(triple9)] Gary is smart.[(triple10 OR ((triple5) -> rule1))] Harry is big.[(triple11)] Harry is cold.[(triple12)] Harry is green.[(triple13 OR ((triple15) -> rule2))] Harry is kind.[(triple14)] Harry is rough.[(triple15)] @1: Harry is smart.[(((triple12) -> rule1))]
Dave is big.
("Dave" "is" "big" "+")
triple1
Dave is green.
("Dave" "is" "green" "+")
triple2
Erin is quiet.
("Erin" "is" "quiet" "+")
triple3
Gary is big.
("Gary" "is" "big" "+")
triple4
Gary is cold.
("Gary" "is" "cold" "+")
triple5
Gary is green.
("Gary" "is" "green" "+")
triple6
((triple9) -> (rule2 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
triple7
Gary is quiet.
("Gary" "is" "quiet" "+")
triple8
Gary is rough.
("Gary" "is" "rough" "+")
triple9
Gary is smart.
("Gary" "is" "smart" "+")
triple10
((triple5) -> (rule1 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
triple11
Harry is cold.
("Harry" "is" "cold" "+")
triple12
Harry is green.
("Harry" "is" "green" "+")
triple13
((triple15) -> (rule2 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
triple14
Harry is rough.
("Harry" "is" "rough" "+")
triple15
Harry is smart.
("Harry" "is" "smart" "+")
((triple12) -> (rule1 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1