Anne is furry. Bob is furry. Erin is blue. Harry is green. All young people are furry. If Bob is green then Bob is blue. Blue people are young.
Anne is furry.
("Anne" "is" "furry" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Harry is green.
("Harry" "is" "green" "+")
All young people are furry.
((("someone" "is" "young" "+")) -> ("someone" "is" "furry" "+"))
If Bob is green then Bob is blue.
((("Bob" "is" "green" "+")) -> ("Bob" "is" "blue" "+"))
Blue people are young.
((("someone" "is" "blue" "+")) -> ("someone" "is" "young" "+"))
Bob is furry.
True
1
proof
[(triple2)]
("Bob" "is" "furry" "+")
triple2
Harry is not green.
False
1
inv-proof
[(triple4)]
("Harry" "is" "green" "-")
triple4
Erin is young.
True
2
proof
[(((triple3) -> rule3))]
("Erin" "is" "young" "+")
((triple3) -> (rule3 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is not young.
False
2
inv-proof
[(((triple3) -> rule3))]
("Erin" "is" "young" "-")
((triple3) -> (rule3 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is furry.
True
3
proof
[(((((triple3) -> rule3)) -> rule1))]
("Erin" "is" "furry" "+")
((((triple3) -> (rule3 % int2))) -> (rule1 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is not furry.
False
3
inv-proof
[(((((triple3) -> rule3)) -> rule1))]
("Erin" "is" "furry" "-")
((((triple3) -> (rule3 % int2))) -> (rule1 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Harry is not young.
Unknown
inv-rconc
[@1: Harry is young.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Harry" "is" "young" "-")
Anne is young.
Unknown
rconc
[@1: Anne is young.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Anne" "is" "young" "+")
Harry is not furry.
Unknown
inv-rconc
[@2: Harry is furry.[CWA. Example of deepest failure = (rule1 <- rule3 <- FAIL)]]
("Harry" "is" "furry" "-")
Harry is rough.
Unknown
random
[@0: Harry is rough.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "rough" "+")
Erin is not red.
Unknown
inv-random
[@0: Erin is red.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "red" "-")
Harry is blue.
Unknown
random
[@0: Harry is blue.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "blue" "+")
@0: Anne is furry.[(triple1)] Bob is furry.[(triple2)] Erin is blue.[(triple3)] Harry is green.[(triple4)] @1: Erin is young.[(((triple3) -> rule3))] @2: Erin is furry.[(((((triple3) -> rule3)) -> rule1))]
Anne is furry.
("Anne" "is" "furry" "+")
triple1
Bob is furry.
("Bob" "is" "furry" "+")
triple2
Erin is blue.
("Erin" "is" "blue" "+")
triple3
Harry is green.
("Harry" "is" "green" "+")
triple4
Erin is young.
("Erin" "is" "young" "+")
((triple3) -> (rule3 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
((((triple3) -> (rule3 % int2))) -> (rule1 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2