Bob is nice. Bob is white. Dave is cold. Dave is white. Fiona is rough. Fiona is white. Harry is cold. All rough things are cold. All furry, rough things are blue. If something is blue then it is nice. Furry, white things are smart. If something is white and smart then it is nice. Smart things are furry. All white, nice things are smart. If something is furry then it is white.
Bob is nice.
("Bob" "is" "nice" "+")
Bob is white.
("Bob" "is" "white" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is white.
("Dave" "is" "white" "+")
Fiona is rough.
("Fiona" "is" "rough" "+")
Fiona is white.
("Fiona" "is" "white" "+")
Harry is cold.
("Harry" "is" "cold" "+")
All rough things are cold.
((("something" "is" "rough" "+")) -> ("something" "is" "cold" "+"))
All furry, rough things are blue.
((("something" "is" "furry" "+") ("something" "is" "rough" "+")) -> ("something" "is" "blue" "+"))
If something is blue then it is nice.
((("something" "is" "blue" "+")) -> ("something" "is" "nice" "+"))
Furry, white things are smart.
((("something" "is" "furry" "+") ("something" "is" "white" "+")) -> ("something" "is" "smart" "+"))
If something is white and smart then it is nice.
((("something" "is" "white" "+") ("something" "is" "smart" "+")) -> ("something" "is" "nice" "+"))
Smart things are furry.
((("something" "is" "smart" "+")) -> ("something" "is" "furry" "+"))
All white, nice things are smart.
((("something" "is" "white" "+") ("something" "is" "nice" "+")) -> ("something" "is" "smart" "+"))
If something is furry then it is white.
((("something" "is" "furry" "+")) -> ("something" "is" "white" "+"))
Bob is nice.
True
1
proof
[(triple1)]
("Bob" "is" "nice" "+")
triple1
Fiona is not white.
False
1
inv-proof
[(triple6)]
("Fiona" "is" "white" "-")
triple6
Fiona is cold.
True
2
proof
[(((triple5) -> rule1))]
("Fiona" "is" "cold" "+")
((triple5) -> (rule1 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is not cold.
False
2
inv-proof
[(((triple5) -> rule1))]
("Fiona" "is" "cold" "-")
((triple5) -> (rule1 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Bob is furry.
True
4
proof
[(((((triple2 triple1) -> rule7)) -> rule6))]
("Bob" "is" "furry" "+")
((((triple2 triple1) -> (rule7 % int2))) -> (rule6 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is not furry.
False
4
inv-proof
[(((((triple2 triple1) -> rule7)) -> rule6))]
("Bob" "is" "furry" "-")
((((triple2 triple1) -> (rule7 % int2))) -> (rule6 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Harry is not smart.
Unknown
inv-rconc
[@4: Harry is smart.[CWA. Example of deepest failure = (rule4 <- rule6 <- rule7 <- rule8 <- FAIL)]]
("Harry" "is" "smart" "-")
Harry is furry.
Unknown
rconc
[@3: Harry is furry.[CWA. Example of deepest failure = (rule6 <- rule7 <- rule8 <- FAIL)]]
("Harry" "is" "furry" "+")
Fiona is not smart.
Unknown
inv-rconc
[@5: Fiona is smart.[CWA. Example of deepest failure = (rule4 <- rule6 <- rule7 <- rule3 <- rule2 <- FAIL)]]
("Fiona" "is" "smart" "-")
Dave is rough.
Unknown
random
[@0: Dave is rough.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "rough" "+")
Bob is not rough.
Unknown
inv-random
[@0: Bob is rough.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "rough" "-")
Harry is rough.
Unknown
random
[@0: Harry is rough.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "rough" "+")
@0: Bob is nice.[(triple1)] Bob is white.[(triple2)] Dave is cold.[(triple3)] Dave is white.[(triple4)] Fiona is rough.[(triple5)] Fiona is white.[(triple6)] Harry is cold.[(triple7)] @1: Bob is smart.[(((triple2 triple1) -> rule7))] Fiona is cold.[(((triple5) -> rule1))] @2: Bob is furry.[(((((triple2 triple1) -> rule7)) -> rule6))]
Bob is nice.
("Bob" "is" "nice" "+")
triple1
Bob is white.
("Bob" "is" "white" "+")
triple2
Dave is cold.
("Dave" "is" "cold" "+")
triple3
Dave is white.
("Dave" "is" "white" "+")
triple4
Fiona is rough.
("Fiona" "is" "rough" "+")
triple5
Fiona is white.
("Fiona" "is" "white" "+")
triple6
Harry is cold.
("Harry" "is" "cold" "+")
triple7
Bob is smart.
("Bob" "is" "smart" "+")
((triple2 triple1) -> (rule7 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
((triple5) -> (rule1 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
((((triple2 triple1) -> (rule7 % int2))) -> (rule6 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2