Dave is smart. Nice people are cold. If someone is smart then they are young. If someone is smart and rough then they are young. If someone is cold then they are smart. If Dave is smart and Dave is young then Dave is rough. If someone is kind then they are white.
Dave is smart.
("Dave" "is" "smart" "+")
Nice people are cold.
((("someone" "is" "nice" "+")) -> ("someone" "is" "cold" "+"))
If someone is smart then they are young.
((("someone" "is" "smart" "+")) -> ("someone" "is" "young" "+"))
If someone is smart and rough then they are young.
((("someone" "is" "smart" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "young" "+"))
If someone is cold then they are smart.
((("someone" "is" "cold" "+")) -> ("someone" "is" "smart" "+"))
If Dave is smart and Dave is young then Dave is rough.
((("Dave" "is" "smart" "+") ("Dave" "is" "young" "+")) -> ("Dave" "is" "rough" "+"))
If someone is kind then they are white.
((("someone" "is" "kind" "+")) -> ("someone" "is" "white" "+"))
Dave is smart.
True
1
proof
[(triple1)]
("Dave" "is" "smart" "+")
triple1
Dave is not smart.
False
1
inv-proof
[(triple1)]
("Dave" "is" "smart" "-")
triple1
Dave is young.
True
2
proof
[(((triple1) -> rule2))]
("Dave" "is" "young" "+")
((triple1) -> (rule2 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is not young.
False
2
inv-proof
[(((triple1) -> rule2))]
("Dave" "is" "young" "-")
((triple1) -> (rule2 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is rough.
True
4
proof
[(((triple1 ((triple1) -> rule2)) -> rule5))]
("Dave" "is" "rough" "+")
((triple1 ((triple1) -> (rule2 % int2))) -> (rule5 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is not rough.
False
4
inv-proof
[(((triple1 ((triple1) -> rule2)) -> rule5))]
("Dave" "is" "rough" "-")
((triple1 ((triple1) -> (rule2 % int2))) -> (rule5 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is not white.
Unknown
inv-rconc
[@1: Dave is white.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Dave" "is" "white" "-")
Dave is cold.
Unknown
rconc
[@1: Dave is cold.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Dave" "is" "cold" "+")
Dave is not kind.
Unknown
inv-random
[@0: Dave is kind.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "kind" "-")
Dave is nice.
Unknown
random
[@0: Dave is nice.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "nice" "+")
@0: Dave is smart.[(triple1)] @1: Dave is young.[(((triple1) -> rule2))] @2: Dave is rough.[(((triple1 ((triple1) -> rule2)) -> rule5))]
Dave is smart.
("Dave" "is" "smart" "+")
triple1
Dave is young.
("Dave" "is" "young" "+")
((triple1) -> (rule2 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
((triple1 ((triple1) -> (rule2 % int2))) -> (rule5 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2