Bob is kind. Charlie is round. If something is round then it is rough. If Bob is big then Bob is blue. Rough, round things are nice. If something is blue and rough then it is furry. All nice things are not furry. Rough things are round.
Bob is kind.
("Bob" "is" "kind" "+")
Charlie is round.
("Charlie" "is" "round" "+")
If something is round then it is rough.
((("something" "is" "round" "+")) -> ("something" "is" "rough" "+"))
If Bob is big then Bob is blue.
((("Bob" "is" "big" "+")) -> ("Bob" "is" "blue" "+"))
Rough, round things are nice.
((("something" "is" "rough" "+") ("something" "is" "round" "+")) -> ("something" "is" "nice" "+"))
If something is blue and rough then it is furry.
((("something" "is" "blue" "+") ("something" "is" "rough" "+")) -> ("something" "is" "furry" "+"))
All nice things are not furry.
((("something" "is" "nice" "+")) -> ("something" "is" "furry" "-"))
Rough things are round.
((("something" "is" "rough" "+")) -> ("something" "is" "round" "+"))
Charlie is round.
True
1
proof
[(triple2)]
("Charlie" "is" "round" "+")
triple2
Charlie is not round.
False
1
inv-proof
[(triple2)]
("Charlie" "is" "round" "-")
triple2
Charlie is rough.
True
2
proof
[(((triple2) -> rule1))]
("Charlie" "is" "rough" "+")
((triple2) -> (rule1 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is not rough.
False
2
inv-proof
[(((triple2) -> rule1))]
("Charlie" "is" "rough" "-")
((triple2) -> (rule1 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is nice.
True
4
proof
[(((((triple2) -> rule1) triple2) -> rule3))]
("Charlie" "is" "nice" "+")
((((triple2) -> (rule1 % int2)) triple2) -> (rule3 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is not nice.
False
4
inv-proof
[(((((triple2) -> rule1) triple2) -> rule3))]
("Charlie" "is" "nice" "-")
((((triple2) -> (rule1 % int2)) triple2) -> (rule3 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is not furry.
True
5
proof
[(((((((triple2) -> rule1) triple2) -> rule3)) -> rule5))]
("Charlie" "is" "furry" "-")
((((((triple2) -> (rule1 % int3)) triple2) -> (rule3 % int2))) -> (rule5 % int1))
Charlie is not furry.
("Charlie" "is" "furry" "-")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3
Charlie is furry.
False
5
inv-proof
[(((((((triple2) -> rule1) triple2) -> rule3)) -> rule5))]
("Charlie" "is" "furry" "+")
((((((triple2) -> (rule1 % int3)) triple2) -> (rule3 % int2))) -> (rule5 % int1))
Charlie is not furry.
("Charlie" "is" "furry" "-")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3
Bob is not rough.
Unknown
inv-rconc
[@2: Bob is rough.[CWA. Example of deepest failure = (rule1 <- rule6 <- FAIL)]]
("Bob" "is" "rough" "-")
Bob is nice.
Unknown
rconc
[@3: Bob is nice.[CWA. Example of deepest failure = (rule3 <- rule1 <- rule6 <- FAIL)]]
("Bob" "is" "nice" "+")
Bob is not round.
Unknown
inv-rconc
[@2: Bob is round.[CWA. Example of deepest failure = (rule6 <- rule1 <- FAIL)]]
("Bob" "is" "round" "-")
Bob is blue.
Unknown
rconc
[@1: Bob is blue.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Bob" "is" "blue" "+")
Charlie is not kind.
Unknown
inv-random
[@0: Charlie is kind.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "kind" "-")
Charlie is big.
Unknown
random
[@0: Charlie is big.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "big" "+")
Charlie is not blue.
Unknown
inv-random
[@0: Charlie is blue.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "blue" "-")
Bob is big.
Unknown
random
[@0: Bob is big.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "big" "+")
@0: Bob is kind.[(triple1)] Charlie is round.[(triple2)] @1: Charlie is rough.[(((triple2) -> rule1))] @2: Charlie is nice.[(((((triple2) -> rule1) triple2) -> rule3))] @3: Charlie is not furry.[(((((((triple2) -> rule1) triple2) -> rule3)) -> rule5))]
Bob is kind.
("Bob" "is" "kind" "+")
triple1
Charlie is round.
("Charlie" "is" "round" "+")
triple2
Charlie is rough.
("Charlie" "is" "rough" "+")
((triple2) -> (rule1 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
((((triple2) -> (rule1 % int2)) triple2) -> (rule3 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is not furry.
("Charlie" "is" "furry" "-")
((((((triple2) -> (rule1 % int3)) triple2) -> (rule3 % int2))) -> (rule5 % int1))
Charlie is not furry.
("Charlie" "is" "furry" "-")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3