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