Anne is not white. Bob is red. Bob is rough. Bob is smart. Bob is young. Dave is not red. Dave is white. Dave is not young. Harry is nice. Harry is rough. Young things are rough. If something is young and not nice then it is big. Young, red things are white.
Anne is not white.
("Anne" "is" "white" "-")
Bob is red.
("Bob" "is" "red" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Bob is young.
("Bob" "is" "young" "+")
Dave is not red.
("Dave" "is" "red" "-")
Dave is white.
("Dave" "is" "white" "+")
Dave is not young.
("Dave" "is" "young" "-")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Young things are rough.
((("something" "is" "young" "+")) -> ("something" "is" "rough" "+"))
If something is young and not nice then it is big.
((("something" "is" "young" "+") ("something" "is" "nice" "~")) -> ("something" "is" "big" "+"))
Young, red things are white.
((("something" "is" "young" "+") ("something" "is" "red" "+")) -> ("something" "is" "white" "+"))
Bob is rough.
True
1
proof
[(triple3 OR ((triple5) -> rule1))]
("Bob" "is" "rough" "+")
triple3
((triple5) -> (rule1 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Dave is not white.
False
1
inv-proof
[(triple7)]
("Dave" "is" "white" "-")
triple7
Dave is not rough.
Unknown
inv-rconc
[@1: Dave is rough.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Dave" "is" "rough" "-")
Harry is young.
Unknown
random
[@0: Harry is young.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "young" "+")
@0: Anne is not white.[(triple1)] Bob is red.[(triple2)] Bob is rough.[(triple3 OR ((triple5) -> rule1))] Bob is smart.[(triple4)] Bob is young.[(triple5)] Dave is not red.[(triple6)] Dave is not young.[(triple8)] Dave is white.[(triple7)] Harry is nice.[(triple9)] Harry is rough.[(triple10)] @1: Bob is white.[(((triple5 triple2) -> rule3))]
Anne is not white.
("Anne" "is" "white" "-")
triple1
Bob is red.
("Bob" "is" "red" "+")
triple2
Bob is rough.
("Bob" "is" "rough" "+")
triple3
((triple5) -> (rule1 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
triple4
Bob is young.
("Bob" "is" "young" "+")
triple5
Dave is not red.
("Dave" "is" "red" "-")
triple6
Dave is not young.
("Dave" "is" "young" "-")
triple8
Dave is white.
("Dave" "is" "white" "+")
triple7
Harry is nice.
("Harry" "is" "nice" "+")
triple9
Harry is rough.
("Harry" "is" "rough" "+")
triple10
Bob is white.
("Bob" "is" "white" "+")
((triple5 triple2) -> (rule3 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1