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