Charlie is white. Dave is cold. Fiona is white. Harry is young. All furry people are white. If someone is young then they are furry.
Charlie is white.
("Charlie" "is" "white" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Fiona is white.
("Fiona" "is" "white" "+")
Harry is young.
("Harry" "is" "young" "+")
All furry people are white.
((("someone" "is" "furry" "+")) -> ("someone" "is" "white" "+"))
If someone is young then they are furry.
((("someone" "is" "young" "+")) -> ("someone" "is" "furry" "+"))
Fiona is white.
True
1
proof
[(triple3)]
("Fiona" "is" "white" "+")
triple3
Dave is not cold.
False
1
inv-proof
[(triple2)]
("Dave" "is" "cold" "-")
triple2
Harry is furry.
True
2
proof
[(((triple4) -> rule2))]
("Harry" "is" "furry" "+")
((triple4) -> (rule2 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is not furry.
False
2
inv-proof
[(((triple4) -> rule2))]
("Harry" "is" "furry" "-")
((triple4) -> (rule2 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is white.
True
3
proof
[(((((triple4) -> rule2)) -> rule1))]
("Harry" "is" "white" "+")
((((triple4) -> (rule2 % int2))) -> (rule1 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is not white.
False
3
inv-proof
[(((((triple4) -> rule2)) -> rule1))]
("Harry" "is" "white" "-")
((((triple4) -> (rule2 % int2))) -> (rule1 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Fiona is not furry.
Unknown
inv-rconc
[@1: Fiona is furry.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Fiona" "is" "furry" "-")
Charlie is furry.
Unknown
rconc
[@1: Charlie is furry.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Charlie" "is" "furry" "+")
Dave is not furry.
Unknown
inv-rconc
[@1: Dave is furry.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Dave" "is" "furry" "-")
Fiona is blue.
Unknown
random
[@0: Fiona is blue.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "blue" "+")
Harry is not blue.
Unknown
inv-random
[@0: Harry is blue.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "blue" "-")
Charlie is blue.
Unknown
random
[@0: Charlie is blue.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "blue" "+")
@0: Charlie is white.[(triple1)] Dave is cold.[(triple2)] Fiona is white.[(triple3)] Harry is young.[(triple4)] @1: Harry is furry.[(((triple4) -> rule2))] @2: Harry is white.[(((((triple4) -> rule2)) -> rule1))]
Charlie is white.
("Charlie" "is" "white" "+")
triple1
Dave is cold.
("Dave" "is" "cold" "+")
triple2
Fiona is white.
("Fiona" "is" "white" "+")
triple3
Harry is young.
("Harry" "is" "young" "+")
triple4
Harry is furry.
("Harry" "is" "furry" "+")
((triple4) -> (rule2 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
((((triple4) -> (rule2 % int2))) -> (rule1 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2