Dave is blue. If someone is nice and rough then they are furry. If someone is smart and not big then they are not furry. Blue people are rough. If Dave is rough and Dave is cold then Dave is smart. If Dave is nice and Dave is smart then Dave is furry. Rough people are nice.
Dave is blue.
("Dave" "is" "blue" "+")
If someone is nice and rough then they are furry.
((("someone" "is" "nice" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "furry" "+"))
If someone is smart and not big then they are not furry.
((("someone" "is" "smart" "+") ("someone" "is" "big" "~")) -> ("someone" "is" "furry" "-"))
Blue people are rough.
((("someone" "is" "blue" "+")) -> ("someone" "is" "rough" "+"))
If Dave is rough and Dave is cold then Dave is smart.
((("Dave" "is" "rough" "+") ("Dave" "is" "cold" "+")) -> ("Dave" "is" "smart" "+"))
If Dave is nice and Dave is smart then Dave is furry.
((("Dave" "is" "nice" "+") ("Dave" "is" "smart" "+")) -> ("Dave" "is" "furry" "+"))
Rough people are nice.
((("someone" "is" "rough" "+")) -> ("someone" "is" "nice" "+"))
Dave is blue.
True
1
proof
[(triple1)]
("Dave" "is" "blue" "+")
triple1
Dave is not blue.
False
1
inv-proof
[(triple1)]
("Dave" "is" "blue" "-")
triple1
Dave is rough.
True
2
proof
[(((triple1) -> rule3))]
("Dave" "is" "rough" "+")
((triple1) -> (rule3 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is not rough.
False
2
inv-proof
[(((triple1) -> rule3))]
("Dave" "is" "rough" "-")
((triple1) -> (rule3 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is nice.
True
3
proof
[(((((triple1) -> rule3)) -> rule6))]
("Dave" "is" "nice" "+")
((((triple1) -> (rule3 % int2))) -> (rule6 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is not nice.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule6))]
("Dave" "is" "nice" "-")
((((triple1) -> (rule3 % int2))) -> (rule6 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is furry.
True
6
proof
[(((((((triple1) -> rule3)) -> rule6) ((triple1) -> rule3)) -> rule1))]
("Dave" "is" "furry" "+")
((((((triple1) -> (rule3 % int3))) -> (rule6 % int2)) ((triple1) -> (rule3 % int3))) -> (rule1 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
Dave is not furry.
False
6
inv-proof
[(((((((triple1) -> rule3)) -> rule6) ((triple1) -> rule3)) -> rule1))]
("Dave" "is" "furry" "-")
((((((triple1) -> (rule3 % int3))) -> (rule6 % int2)) ((triple1) -> (rule3 % int3))) -> (rule1 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
Dave is not smart.
Unknown
inv-rconc
[@1: Dave is smart.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Dave" "is" "smart" "-")
Dave is cold.
Unknown
random
[@0: Dave is cold.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "cold" "+")
@0: Dave is blue.[(triple1)] @1: Dave is rough.[(((triple1) -> rule3))] @2: Dave is nice.[(((((triple1) -> rule3)) -> rule6))] @3: Dave is furry.[(((((((triple1) -> rule3)) -> rule6) ((triple1) -> rule3)) -> rule1))]
Dave is blue.
("Dave" "is" "blue" "+")
triple1
Dave is rough.
("Dave" "is" "rough" "+")
((triple1) -> (rule3 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
((((triple1) -> (rule3 % int2))) -> (rule6 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
((((((triple1) -> (rule3 % int3))) -> (rule6 % int2)) ((triple1) -> (rule3 % int3))) -> (rule1 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3