Erin is big. Erin is furry. Erin is red. Erin is rough. Harry is big. Harry is rough. Harry is young. If Harry is rough and Harry is red then Harry is blue. If someone is big and young then they are red. If Harry is blue then Harry is nice. All big, nice people are young. Nice people are blue. All red, nice people are big. If someone is nice then they are blue. Furry people are blue.
Erin is big.
("Erin" "is" "big" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is red.
("Erin" "is" "red" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is young.
("Harry" "is" "young" "+")
If Harry is rough and Harry is red then Harry is blue.
((("Harry" "is" "rough" "+") ("Harry" "is" "red" "+")) -> ("Harry" "is" "blue" "+"))
If someone is big and young then they are red.
((("someone" "is" "big" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "red" "+"))
If Harry is blue then Harry is nice.
((("Harry" "is" "blue" "+")) -> ("Harry" "is" "nice" "+"))
All big, nice people are young.
((("someone" "is" "big" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "young" "+"))
Nice people are blue.
((("someone" "is" "nice" "+")) -> ("someone" "is" "blue" "+"))
All red, nice people are big.
((("someone" "is" "red" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "big" "+"))
If someone is nice then they are blue.
((("someone" "is" "nice" "+")) -> ("someone" "is" "blue" "+"))
Furry people are blue.
((("someone" "is" "furry" "+")) -> ("someone" "is" "blue" "+"))
Harry is rough.
True
1
proof
[(triple6)]
("Harry" "is" "rough" "+")
triple6
Erin is not big.
False
1
inv-proof
[(triple1)]
("Erin" "is" "big" "-")
triple1
Harry is red.
True
3
proof
[(((triple5 triple7) -> rule2))]
("Harry" "is" "red" "+")
((triple5 triple7) -> (rule2 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is not red.
False
3
inv-proof
[(((triple5 triple7) -> rule2))]
("Harry" "is" "red" "-")
((triple5 triple7) -> (rule2 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is blue.
True
5
proof
[(((triple6 ((triple5 triple7) -> rule2)) -> rule1))]
("Harry" "is" "blue" "+")
((triple6 ((triple5 triple7) -> (rule2 % int2))) -> (rule1 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is not blue.
False
5
inv-proof
[(((triple6 ((triple5 triple7) -> rule2)) -> rule1))]
("Harry" "is" "blue" "-")
((triple6 ((triple5 triple7) -> (rule2 % int2))) -> (rule1 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is nice.
True
6
proof
[(((((triple6 ((triple5 triple7) -> rule2)) -> rule1)) -> rule3))]
("Harry" "is" "nice" "+")
((((triple6 ((triple5 triple7) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
int3
Harry is not nice.
False
6
inv-proof
[(((((triple6 ((triple5 triple7) -> rule2)) -> rule1)) -> rule3))]
("Harry" "is" "nice" "-")
((((triple6 ((triple5 triple7) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
int3
Erin is not young.
Unknown
inv-rconc
[@1: Erin is young.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Erin" "is" "young" "-")
Harry is furry.
Unknown
random
[@0: Harry is furry.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "furry" "+")
@0: Erin is big.[(triple1)] Erin is furry.[(triple2)] Erin is red.[(triple3)] Erin is rough.[(triple4)] Harry is big.[(triple5)] Harry is rough.[(triple6)] Harry is young.[(triple7)] @1: Erin is blue.[(((triple2) -> rule8))] Harry is red.[(((triple5 triple7) -> rule2))] @2: Harry is blue.[(((triple6 ((triple5 triple7) -> rule2)) -> rule1))] @3: Harry is nice.[(((((triple6 ((triple5 triple7) -> rule2)) -> rule1)) -> rule3))]
Erin is big.
("Erin" "is" "big" "+")
triple1
Erin is furry.
("Erin" "is" "furry" "+")
triple2
Erin is red.
("Erin" "is" "red" "+")
triple3
Erin is rough.
("Erin" "is" "rough" "+")
triple4
Harry is big.
("Harry" "is" "big" "+")
triple5
Harry is rough.
("Harry" "is" "rough" "+")
triple6
Harry is young.
("Harry" "is" "young" "+")
triple7
Erin is blue.
("Erin" "is" "blue" "+")
((triple2) -> (rule8 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
((triple5 triple7) -> (rule2 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
((triple6 ((triple5 triple7) -> (rule2 % int2))) -> (rule1 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
((((triple6 ((triple5 triple7) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
int3