Dave is rough. Harry is furry. If Dave is cold then Dave is smart. Furry, cold people are quiet. If Harry is furry then Harry is cold.
Dave is rough.
("Dave" "is" "rough" "+")
Harry is furry.
("Harry" "is" "furry" "+")
If Dave is cold then Dave is smart.
((("Dave" "is" "cold" "+")) -> ("Dave" "is" "smart" "+"))
Furry, cold people are quiet.
((("someone" "is" "furry" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "quiet" "+"))
If Harry is furry then Harry is cold.
((("Harry" "is" "furry" "+")) -> ("Harry" "is" "cold" "+"))
Harry is furry.
True
1
proof
[(triple2)]
("Harry" "is" "furry" "+")
triple2
Harry is not furry.
False
1
inv-proof
[(triple2)]
("Harry" "is" "furry" "-")
triple2
Harry is cold.
True
2
proof
[(((triple2) -> rule3))]
("Harry" "is" "cold" "+")
((triple2) -> (rule3 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is not cold.
False
2
inv-proof
[(((triple2) -> rule3))]
("Harry" "is" "cold" "-")
((triple2) -> (rule3 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is quiet.
True
4
proof
[(((triple2 ((triple2) -> rule3)) -> rule2))]
("Harry" "is" "quiet" "+")
((triple2 ((triple2) -> (rule3 % int2))) -> (rule2 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is not quiet.
False
4
inv-proof
[(((triple2 ((triple2) -> rule3)) -> rule2))]
("Harry" "is" "quiet" "-")
((triple2 ((triple2) -> (rule3 % int2))) -> (rule2 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Dave is not quiet.
Unknown
inv-rconc
[@1: Dave is quiet.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Dave" "is" "quiet" "-")
Dave is smart.
Unknown
rconc
[@1: Dave is smart.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Dave" "is" "smart" "+")
Harry is not smart.
Unknown
inv-random
[@0: Harry is smart.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "smart" "-")
Dave is cold.
Unknown
random
[@0: Dave is cold.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "cold" "+")
Dave is not furry.
Unknown
inv-random
[@0: Dave is furry.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "furry" "-")
Harry is rough.
Unknown
random
[@0: Harry is rough.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "rough" "+")
@0: Dave is rough.[(triple1)] Harry is furry.[(triple2)] @1: Harry is cold.[(((triple2) -> rule3))] @2: Harry is quiet.[(((triple2 ((triple2) -> rule3)) -> rule2))]
Dave is rough.
("Dave" "is" "rough" "+")
triple1
Harry is furry.
("Harry" "is" "furry" "+")
triple2
Harry is cold.
("Harry" "is" "cold" "+")
((triple2) -> (rule3 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
((triple2 ((triple2) -> (rule3 % int2))) -> (rule2 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2