Bob is furry. Bob is kind. Bob is smart. Dave is blue. Dave is cold. Dave is furry. Dave is kind. Dave is nice. Dave is rough. Dave is smart. Erin is blue. Erin is kind. If someone is furry then they are rough. Cold people are blue. If someone is rough then they are cold.
Bob is furry.
("Bob" "is" "furry" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is kind.
("Erin" "is" "kind" "+")
If someone is furry then they are rough.
((("someone" "is" "furry" "+")) -> ("someone" "is" "rough" "+"))
Cold people are blue.
((("someone" "is" "cold" "+")) -> ("someone" "is" "blue" "+"))
If someone is rough then they are cold.
((("someone" "is" "rough" "+")) -> ("someone" "is" "cold" "+"))
Bob is furry.
True
1
proof
[(triple1)]
("Bob" "is" "furry" "+")
triple1
Dave is not cold.
False
1
inv-proof
[(triple5 OR ((triple9) -> rule3) OR ((((triple6) -> rule1)) -> rule3))]
("Dave" "is" "cold" "-")
triple5
((triple9) -> (rule3 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
((((triple6) -> (rule1 % int2))) -> (rule3 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Bob is rough.
True
2
proof
[(((triple1) -> rule1))]
("Bob" "is" "rough" "+")
((triple1) -> (rule1 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is not rough.
False
2
inv-proof
[(((triple1) -> rule1))]
("Bob" "is" "rough" "-")
((triple1) -> (rule1 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is cold.
True
3
proof
[(((((triple1) -> rule1)) -> rule3))]
("Bob" "is" "cold" "+")
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is not cold.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule3))]
("Bob" "is" "cold" "-")
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Erin is not rough.
Unknown
inv-rconc
[@1: Erin is rough.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Erin" "is" "rough" "-")
Erin is cold.
Unknown
rconc
[@2: Erin is cold.[CWA. Example of deepest failure = (rule3 <- rule1 <- FAIL)]]
("Erin" "is" "cold" "+")
Erin is not smart.
Unknown
inv-random
[@0: Erin is smart.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "smart" "-")
Erin is furry.
Unknown
random
[@0: Erin is furry.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "furry" "+")
Erin is not nice.
Unknown
inv-random
[@0: Erin is nice.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "nice" "-")
Bob is nice.
Unknown
random
[@0: Bob is nice.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "nice" "+")
@0: Bob is furry.[(triple1)] Bob is kind.[(triple2)] Bob is smart.[(triple3)] Dave is blue.[(triple4 OR ((triple5) -> rule2) OR ((((triple9) -> rule3)) -> rule2) OR ((((((triple6) -> rule1)) -> rule3)) -> rule2))] Dave is cold.[(triple5 OR ((triple9) -> rule3) OR ((((triple6) -> rule1)) -> rule3))] Dave is furry.[(triple6)] Dave is kind.[(triple7)] Dave is nice.[(triple8)] Dave is rough.[(triple9 OR ((triple6) -> rule1))] Dave is smart.[(triple10)] Erin is blue.[(triple11)] Erin is kind.[(triple12)] @1: Bob is rough.[(((triple1) -> rule1))] @2: Bob is cold.[(((((triple1) -> rule1)) -> rule3))] @3: Bob is blue.[(((((((triple1) -> rule1)) -> rule3)) -> rule2))]
Bob is furry.
("Bob" "is" "furry" "+")
triple1
Bob is kind.
("Bob" "is" "kind" "+")
triple2
Bob is smart.
("Bob" "is" "smart" "+")
triple3
Dave is blue.
("Dave" "is" "blue" "+")
triple4
((triple5) -> (rule2 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
((((triple9) -> (rule3 % int2))) -> (rule2 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
((((((triple6) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
Dave is cold.
("Dave" "is" "cold" "+")
triple5
((triple9) -> (rule3 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
((((triple6) -> (rule1 % int2))) -> (rule3 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
triple6
Dave is kind.
("Dave" "is" "kind" "+")
triple7
Dave is nice.
("Dave" "is" "nice" "+")
triple8
Dave is rough.
("Dave" "is" "rough" "+")
triple9
((triple6) -> (rule1 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
triple10
Erin is blue.
("Erin" "is" "blue" "+")
triple11
Erin is kind.
("Erin" "is" "kind" "+")
triple12
Bob is rough.
("Bob" "is" "rough" "+")
((triple1) -> (rule1 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
((((((triple1) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
int3