Bob is big. Harry is rough. Red people are rough. All big people are furry. All nice people are young. All round people are rough. All rough people are nice. If someone is red then they are nice. All rough, red people are nice. If Bob is young and Bob is nice then Bob is furry.
Bob is big.
("Bob" "is" "big" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Red people are rough.
((("someone" "is" "red" "+")) -> ("someone" "is" "rough" "+"))
All big people are furry.
((("someone" "is" "big" "+")) -> ("someone" "is" "furry" "+"))
All nice people are young.
((("someone" "is" "nice" "+")) -> ("someone" "is" "young" "+"))
All round people are rough.
((("someone" "is" "round" "+")) -> ("someone" "is" "rough" "+"))
All rough people are nice.
((("someone" "is" "rough" "+")) -> ("someone" "is" "nice" "+"))
If someone is red then they are nice.
((("someone" "is" "red" "+")) -> ("someone" "is" "nice" "+"))
All rough, red people are nice.
((("someone" "is" "rough" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "nice" "+"))
If Bob is young and Bob is nice then Bob is furry.
((("Bob" "is" "young" "+") ("Bob" "is" "nice" "+")) -> ("Bob" "is" "furry" "+"))
Harry is rough.
True
1
proof
[(triple2)]
("Harry" "is" "rough" "+")
triple2
Harry is not rough.
False
1
inv-proof
[(triple2)]
("Harry" "is" "rough" "-")
triple2
Harry is nice.
True
2
proof
[(((triple2) -> rule5))]
("Harry" "is" "nice" "+")
((triple2) -> (rule5 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Bob is not furry.
False
2
inv-proof
[(((triple1) -> rule2))]
("Bob" "is" "furry" "-")
((triple1) -> (rule2 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Harry is young.
True
3
proof
[(((((triple2) -> rule5)) -> rule3))]
("Harry" "is" "young" "+")
((((triple2) -> (rule5 % int2))) -> (rule3 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is not young.
False
3
inv-proof
[(((((triple2) -> rule5)) -> rule3))]
("Harry" "is" "young" "-")
((((triple2) -> (rule5 % int2))) -> (rule3 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Bob is not rough.
Unknown
inv-rconc
[@1: Bob is rough.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "rough" "-")
Bob is nice.
Unknown
rconc
[@2: Bob is nice.[CWA. Example of deepest failure = (rule5 <- rule1 <- FAIL)]]
("Bob" "is" "nice" "+")
Harry is not furry.
Unknown
inv-rconc
[@1: Harry is furry.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Harry" "is" "furry" "-")
Bob is round.
Unknown
random
[@0: Bob is round.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "round" "+")
Harry is not big.
Unknown
inv-random
[@0: Harry is big.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "big" "-")
Bob is red.
Unknown
random
[@0: Bob is red.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "red" "+")
@0: Bob is big.[(triple1)] Harry is rough.[(triple2)] @1: Bob is furry.[(((triple1) -> rule2))] Harry is nice.[(((triple2) -> rule5))] @2: Harry is young.[(((((triple2) -> rule5)) -> rule3))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Harry is rough.
("Harry" "is" "rough" "+")
triple2
Bob is furry.
("Bob" "is" "furry" "+")
((triple1) -> (rule2 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
((triple2) -> (rule5 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
((((triple2) -> (rule5 % int2))) -> (rule3 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2