Bob is round. Dave is furry. Erin is furry. Harry is young. Cold things are not rough. Young things are rough. Round things are not quiet. If something is rough and not round then it is quiet. If something is round and green then it is quiet. If something is rough then it is not cold. If Erin is green and Erin is not round then Erin is cold. If something is cold and not quiet then it is not furry.
Bob is round.
("Bob" "is" "round" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Harry is young.
("Harry" "is" "young" "+")
Cold things are not rough.
((("something" "is" "cold" "+")) -> ("something" "is" "rough" "-"))
Young things are rough.
((("something" "is" "young" "+")) -> ("something" "is" "rough" "+"))
Round things are not quiet.
((("something" "is" "round" "+")) -> ("something" "is" "quiet" "-"))
If something is rough and not round then it is quiet.
((("something" "is" "rough" "+") ("something" "is" "round" "~")) -> ("something" "is" "quiet" "+"))
If something is round and green then it is quiet.
((("something" "is" "round" "+") ("something" "is" "green" "+")) -> ("something" "is" "quiet" "+"))
If something is rough then it is not cold.
((("something" "is" "rough" "+")) -> ("something" "is" "cold" "-"))
If Erin is green and Erin is not round then Erin is cold.
((("Erin" "is" "green" "+") ("Erin" "is" "round" "~")) -> ("Erin" "is" "cold" "+"))
If something is cold and not quiet then it is not furry.
((("something" "is" "cold" "+") ("something" "is" "quiet" "~")) -> ("something" "is" "furry" "-"))
Dave is furry.
True
1
proof
[(triple2)]
("Dave" "is" "furry" "+")
triple2
Bob is not round.
False
1
inv-proof
[(triple1)]
("Bob" "is" "round" "-")
triple1
Bob is not quiet.
True
2
proof
[(((triple1) -> rule3))]
("Bob" "is" "quiet" "-")
((triple1) -> (rule3 % int1))
Bob is not quiet.
("Bob" "is" "quiet" "-")
int1
Harry is not rough.
False
2
inv-proof
[(((triple4) -> rule2))]
("Harry" "is" "rough" "-")
((triple4) -> (rule2 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is not cold.
True
3
proof
[(((((triple4) -> rule2)) -> rule6))]
("Harry" "is" "cold" "-")
((((triple4) -> (rule2 % int2))) -> (rule6 % int1))
Harry is not cold.
("Harry" "is" "cold" "-")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is cold.
False
3
inv-proof
[(((((triple4) -> rule2)) -> rule6))]
("Harry" "is" "cold" "+")
((((triple4) -> (rule2 % int2))) -> (rule6 % int1))
Harry is not cold.
("Harry" "is" "cold" "-")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Erin is not rough.
Unknown
inv-rconc
[@1: Erin is rough.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Erin" "is" "rough" "-")
Erin is cold.
Unknown
rconc
[@1: Erin is cold.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Erin" "is" "cold" "+")
Dave is not rough.
Unknown
inv-rconc
[@1: Dave is rough.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Dave" "is" "rough" "-")
Dave is young.
Unknown
random
[@0: Dave is young.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "young" "+")
Erin is not round.
Unknown
inv-random
[@0: Erin is round.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "round" "-")
Bob is young.
Unknown
random
[@0: Bob is young.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "young" "+")
@0: Bob is round.[(triple1)] Dave is furry.[(triple2)] Erin is furry.[(triple3)] Harry is young.[(triple4)] @1: Bob is not quiet.[(((triple1) -> rule3))] Harry is rough.[(((triple4) -> rule2))] @2: Harry is not cold.[(((((triple4) -> rule2)) -> rule6))]
Bob is round.
("Bob" "is" "round" "+")
triple1
Dave is furry.
("Dave" "is" "furry" "+")
triple2
Erin is furry.
("Erin" "is" "furry" "+")
triple3
Harry is young.
("Harry" "is" "young" "+")
triple4
Bob is not quiet.
("Bob" "is" "quiet" "-")
((triple1) -> (rule3 % int1))
Bob is not quiet.
("Bob" "is" "quiet" "-")
int1
Harry is rough.
("Harry" "is" "rough" "+")
((triple4) -> (rule2 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is not cold.
("Harry" "is" "cold" "-")
((((triple4) -> (rule2 % int2))) -> (rule6 % int1))
Harry is not cold.
("Harry" "is" "cold" "-")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2