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