Dave is young. Erin is furry. Harry is young. Blue, young things are furry. All young things are blue. If something is furry then it is white.
Dave is young.
("Dave" "is" "young" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Harry is young.
("Harry" "is" "young" "+")
Blue, young things are furry.
((("something" "is" "blue" "+") ("something" "is" "young" "+")) -> ("something" "is" "furry" "+"))
All young things are blue.
((("something" "is" "young" "+")) -> ("something" "is" "blue" "+"))
If something is furry then it is white.
((("something" "is" "furry" "+")) -> ("something" "is" "white" "+"))
Erin is furry.
True
1
proof
[(triple2)]
("Erin" "is" "furry" "+")
triple2
Dave is not young.
False
1
inv-proof
[(triple1)]
("Dave" "is" "young" "-")
triple1
Dave is blue.
True
2
proof
[(((triple1) -> rule2))]
("Dave" "is" "blue" "+")
((triple1) -> (rule2 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Erin is not white.
False
2
inv-proof
[(((triple2) -> rule3))]
("Erin" "is" "white" "-")
((triple2) -> (rule3 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Dave is furry.
True
4
proof
[(((((triple1) -> rule2) triple1) -> rule1))]
("Dave" "is" "furry" "+")
((((triple1) -> (rule2 % int2)) triple1) -> (rule1 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is not furry.
False
4
inv-proof
[(((((triple1) -> rule2) triple1) -> rule1))]
("Dave" "is" "furry" "-")
((((triple1) -> (rule2 % int2)) triple1) -> (rule1 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Harry is white.
True
5
proof
[(((((((triple3) -> rule2) triple3) -> rule1)) -> rule3))]
("Harry" "is" "white" "+")
((((((triple3) -> (rule2 % int3)) triple3) -> (rule1 % int2))) -> (rule3 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
Harry is not white.
False
5
inv-proof
[(((((((triple3) -> rule2) triple3) -> rule1)) -> rule3))]
("Harry" "is" "white" "-")
((((((triple3) -> (rule2 % int3)) triple3) -> (rule1 % int2))) -> (rule3 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
Erin is not blue.
Unknown
inv-rconc
[@1: Erin is blue.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Erin" "is" "blue" "-")
Erin is kind.
Unknown
random
[@0: Erin is kind.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "kind" "+")
Dave is not kind.
Unknown
inv-random
[@0: Dave is kind.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "kind" "-")
Dave is big.
Unknown
random
[@0: Dave is big.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "big" "+")
Harry is not kind.
Unknown
inv-random
[@0: Harry is kind.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "kind" "-")
Harry is big.
Unknown
random
[@0: Harry is big.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "big" "+")
Dave is not rough.
Unknown
inv-random
[@0: Dave is rough.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "rough" "-")
Harry is rough.
Unknown
random
[@0: Harry is rough.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "rough" "+")
@0: Dave is young.[(triple1)] Erin is furry.[(triple2)] Harry is young.[(triple3)] @1: Dave is blue.[(((triple1) -> rule2))] Erin is white.[(((triple2) -> rule3))] Harry is blue.[(((triple3) -> rule2))] @2: Dave is furry.[(((((triple1) -> rule2) triple1) -> rule1))] Harry is furry.[(((((triple3) -> rule2) triple3) -> rule1))] @3: Dave is white.[(((((((triple1) -> rule2) triple1) -> rule1)) -> rule3))] Harry is white.[(((((((triple3) -> rule2) triple3) -> rule1)) -> rule3))]
Dave is young.
("Dave" "is" "young" "+")
triple1
Erin is furry.
("Erin" "is" "furry" "+")
triple2
Harry is young.
("Harry" "is" "young" "+")
triple3
Dave is blue.
("Dave" "is" "blue" "+")
((triple1) -> (rule2 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
((triple2) -> (rule3 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
((triple3) -> (rule2 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
((((triple1) -> (rule2 % int2)) triple1) -> (rule1 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
((((triple3) -> (rule2 % int2)) triple3) -> (rule1 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
((((((triple1) -> (rule2 % int3)) triple1) -> (rule1 % int2))) -> (rule3 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3
Harry is white.
("Harry" "is" "white" "+")
((((((triple3) -> (rule2 % int3)) triple3) -> (rule1 % int2))) -> (rule3 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3