Dave is young. Harry is cold. Harry is kind. If Harry is kind then Harry is big. If someone is kind then they are young. All young, white people are big. If Harry is rough then Harry is cold. Rough people are white. Young, blue people are rough.
Dave is young.
("Dave" "is" "young" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is kind.
("Harry" "is" "kind" "+")
If Harry is kind then Harry is big.
((("Harry" "is" "kind" "+")) -> ("Harry" "is" "big" "+"))
If someone is kind then they are young.
((("someone" "is" "kind" "+")) -> ("someone" "is" "young" "+"))
All young, white people are big.
((("someone" "is" "young" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "big" "+"))
If Harry is rough then Harry is cold.
((("Harry" "is" "rough" "+")) -> ("Harry" "is" "cold" "+"))
Rough people are white.
((("someone" "is" "rough" "+")) -> ("someone" "is" "white" "+"))
Young, blue people are rough.
((("someone" "is" "young" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "rough" "+"))
Dave is young.
True
1
proof
[(triple1)]
("Dave" "is" "young" "+")
triple1
Dave is not young.
False
1
inv-proof
[(triple1)]
("Dave" "is" "young" "-")
triple1
Harry is young.
True
2
proof
[(((triple3) -> rule2))]
("Harry" "is" "young" "+")
((triple3) -> (rule2 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is not young.
False
2
inv-proof
[(((triple3) -> rule2))]
("Harry" "is" "young" "-")
((triple3) -> (rule2 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is not rough.
Unknown
inv-rconc
[@1: Harry is rough.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Harry" "is" "rough" "-")
Dave is big.
Unknown
rconc
[@3: Dave is big.[CWA. Example of deepest failure = (rule3 <- rule5 <- rule6 <- FAIL)]]
("Dave" "is" "big" "+")
Harry is not blue.
Unknown
inv-random
[@0: Harry is blue.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "blue" "-")
Dave is cold.
Unknown
random
[@0: Dave is cold.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "cold" "+")
@0: Dave is young.[(triple1)] Harry is cold.[(triple2)] Harry is kind.[(triple3)] @1: Harry is big.[(((triple3) -> rule1))] Harry is young.[(((triple3) -> rule2))]
Dave is young.
("Dave" "is" "young" "+")
triple1
Harry is cold.
("Harry" "is" "cold" "+")
triple2
Harry is kind.
("Harry" "is" "kind" "+")
triple3
Harry is big.
("Harry" "is" "big" "+")
((triple3) -> (rule1 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
((triple3) -> (rule2 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1