Bob is kind. Charlie is smart. Dave is round. If Charlie is smart then Charlie is rough. If someone is green then they are not quiet. If someone is rough then they are kind. If someone is rough and nice then they are smart. All nice people are not rough. Kind people are not nice. If someone is smart and not quiet then they are round. Nice people are round.
Bob is kind.
("Bob" "is" "kind" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Dave is round.
("Dave" "is" "round" "+")
If Charlie is smart then Charlie is rough.
((("Charlie" "is" "smart" "+")) -> ("Charlie" "is" "rough" "+"))
If someone is green then they are not quiet.
((("someone" "is" "green" "+")) -> ("someone" "is" "quiet" "-"))
If someone is rough then they are kind.
((("someone" "is" "rough" "+")) -> ("someone" "is" "kind" "+"))
If someone is rough and nice then they are smart.
((("someone" "is" "rough" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "smart" "+"))
All nice people are not rough.
((("someone" "is" "nice" "+")) -> ("someone" "is" "rough" "-"))
Kind people are not nice.
((("someone" "is" "kind" "+")) -> ("someone" "is" "nice" "-"))
If someone is smart and not quiet then they are round.
((("someone" "is" "smart" "+") ("someone" "is" "quiet" "~")) -> ("someone" "is" "round" "+"))
Nice people are round.
((("someone" "is" "nice" "+")) -> ("someone" "is" "round" "+"))
Bob is kind.
True
1
proof
[(triple1)]
("Bob" "is" "kind" "+")
triple1
Dave is not round.
False
1
inv-proof
[(triple3)]
("Dave" "is" "round" "-")
triple3
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 kind.
True
3
proof
[(((((triple2) -> rule1)) -> rule3))]
("Charlie" "is" "kind" "+")
((((triple2) -> (rule1 % int2))) -> (rule3 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is not kind.
False
3
inv-proof
[(((((triple2) -> rule1)) -> rule3))]
("Charlie" "is" "kind" "-")
((((triple2) -> (rule1 % int2))) -> (rule3 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is not nice.
True
4
proof
[(((((((triple2) -> rule1)) -> rule3)) -> rule6))]
("Charlie" "is" "nice" "-")
((((((triple2) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Charlie is not nice.
("Charlie" "is" "nice" "-")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3
Charlie is nice.
False
4
inv-proof
[(((((((triple2) -> rule1)) -> rule3)) -> rule6))]
("Charlie" "is" "nice" "+")
((((((triple2) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Charlie is not nice.
("Charlie" "is" "nice" "-")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3
Dave is not kind.
Unknown
inv-rconc
[@1: Dave is kind.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Dave" "is" "kind" "-")
Charlie is round.
Unknown
rconc
[@1: Charlie is round.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Charlie" "is" "round" "+")
Bob is not smart.
Unknown
inv-rconc
[@1: Bob is smart.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Bob" "is" "smart" "-")
Dave is smart.
Unknown
rconc
[@1: Dave is smart.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Dave" "is" "smart" "+")
Bob is not rough.
Unknown
inv-random
[@0: Bob is rough.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "rough" "-")
Charlie is quiet.
Unknown
random
[@0: Charlie is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "quiet" "+")
Bob is not quiet.
Unknown
inv-random
[@0: Bob is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "quiet" "-")
Charlie is green.
Unknown
random
[@0: Charlie is green.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "green" "+")
@0: Bob is kind.[(triple1)] Charlie is smart.[(triple2)] Dave is round.[(triple3)] @1: Bob is not nice.[(((triple1) -> rule6))] Charlie is rough.[(((triple2) -> rule1))] @2: Charlie is kind.[(((((triple2) -> rule1)) -> rule3))] @3: Charlie is not nice.[(((((((triple2) -> rule1)) -> rule3)) -> rule6))]
Bob is kind.
("Bob" "is" "kind" "+")
triple1
Charlie is smart.
("Charlie" "is" "smart" "+")
triple2
Dave is round.
("Dave" "is" "round" "+")
triple3
Bob is not nice.
("Bob" "is" "nice" "-")
((triple1) -> (rule6 % int1))
Bob is not nice.
("Bob" "is" "nice" "-")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
((triple2) -> (rule1 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
((((triple2) -> (rule1 % int2))) -> (rule3 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is not nice.
("Charlie" "is" "nice" "-")
((((((triple2) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Charlie is not nice.
("Charlie" "is" "nice" "-")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3