Bob is cold. Bob is smart. Bob is white. Charlie is furry. Charlie is quiet. Charlie is rough. Charlie is white. Dave is green. Erin is quiet. Erin is white. If something is furry then it is smart. All furry, green things are rough. Smart, quiet things are white.
Bob is cold.
("Bob" "is" "cold" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Bob is white.
("Bob" "is" "white" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Dave is green.
("Dave" "is" "green" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is white.
("Erin" "is" "white" "+")
If something is furry then it is smart.
((("something" "is" "furry" "+")) -> ("something" "is" "smart" "+"))
All furry, green things are rough.
((("something" "is" "furry" "+") ("something" "is" "green" "+")) -> ("something" "is" "rough" "+"))
Smart, quiet things are white.
((("something" "is" "smart" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "white" "+"))
Charlie is furry.
True
1
proof
[(triple4)]
("Charlie" "is" "furry" "+")
triple4
Charlie is not white.
False
1
inv-proof
[(triple7 OR ((((triple4) -> rule1) triple5) -> rule3))]
("Charlie" "is" "white" "-")
triple7
((((triple4) -> (rule1 % int2)) triple5) -> (rule3 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is smart.
True
2
proof
[(((triple4) -> rule1))]
("Charlie" "is" "smart" "+")
((triple4) -> (rule1 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is not smart.
False
2
inv-proof
[(((triple4) -> rule1))]
("Charlie" "is" "smart" "-")
((triple4) -> (rule1 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Erin is not smart.
Unknown
inv-rconc
[@1: Erin is smart.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Erin" "is" "smart" "-")
Dave is white.
Unknown
rconc
[@1: Dave is white.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Dave" "is" "white" "+")
Bob is not furry.
Unknown
inv-random
[@0: Bob is furry.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "furry" "-")
Erin is green.
Unknown
random
[@0: Erin is green.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "green" "+")
@0: Bob is cold.[(triple1)] Bob is smart.[(triple2)] Bob is white.[(triple3)] Charlie is furry.[(triple4)] Charlie is quiet.[(triple5)] Charlie is rough.[(triple6)] Charlie is white.[(triple7 OR ((((triple4) -> rule1) triple5) -> rule3))] Dave is green.[(triple8)] Erin is quiet.[(triple9)] Erin is white.[(triple10)] @1: Charlie is smart.[(((triple4) -> rule1))]
Bob is cold.
("Bob" "is" "cold" "+")
triple1
Bob is smart.
("Bob" "is" "smart" "+")
triple2
Bob is white.
("Bob" "is" "white" "+")
triple3
Charlie is furry.
("Charlie" "is" "furry" "+")
triple4
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple5
Charlie is rough.
("Charlie" "is" "rough" "+")
triple6
Charlie is white.
("Charlie" "is" "white" "+")
triple7
((((triple4) -> (rule1 % int2)) triple5) -> (rule3 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
triple8
Erin is quiet.
("Erin" "is" "quiet" "+")
triple9
Erin is white.
("Erin" "is" "white" "+")
triple10
Charlie is smart.
("Charlie" "is" "smart" "+")
((triple4) -> (rule1 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1