Fiona is smart. Gary is blue. Harry is big. Big things are rough. If Fiona is smart then Fiona is not young. All blue things are young. Rough things are furry. If something is blue and not big then it is not smart. Rough, smart things are blue. Young, cold things are blue. If Gary is cold then Gary is rough.
Fiona is smart.
("Fiona" "is" "smart" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Harry is big.
("Harry" "is" "big" "+")
Big things are rough.
((("something" "is" "big" "+")) -> ("something" "is" "rough" "+"))
If Fiona is smart then Fiona is not young.
((("Fiona" "is" "smart" "+")) -> ("Fiona" "is" "young" "-"))
All blue things are young.
((("something" "is" "blue" "+")) -> ("something" "is" "young" "+"))
Rough things are furry.
((("something" "is" "rough" "+")) -> ("something" "is" "furry" "+"))
If something is blue and not big then it is not smart.
((("something" "is" "blue" "+") ("something" "is" "big" "~")) -> ("something" "is" "smart" "-"))
Rough, smart things are blue.
((("something" "is" "rough" "+") ("something" "is" "smart" "+")) -> ("something" "is" "blue" "+"))
Young, cold things are blue.
((("something" "is" "young" "+") ("something" "is" "cold" "+")) -> ("something" "is" "blue" "+"))
If Gary is cold then Gary is rough.
((("Gary" "is" "cold" "+")) -> ("Gary" "is" "rough" "+"))
Gary is blue.
True
1
proof
[(triple2)]
("Gary" "is" "blue" "+")
triple2
Harry is not big.
False
1
inv-proof
[(triple3)]
("Harry" "is" "big" "-")
triple3
Gary is young.
True
2
proof
[(((triple2) -> rule3))]
("Gary" "is" "young" "+")
((triple2) -> (rule3 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Harry is not rough.
False
2
inv-proof
[(((triple3) -> rule1))]
("Harry" "is" "rough" "-")
((triple3) -> (rule1 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is furry.
True
3
proof
[(((((triple3) -> rule1)) -> rule4))]
("Harry" "is" "furry" "+")
((((triple3) -> (rule1 % int2))) -> (rule4 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is not furry.
False
3
inv-proof
[(((((triple3) -> rule1)) -> rule4))]
("Harry" "is" "furry" "-")
((((triple3) -> (rule1 % int2))) -> (rule4 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is not blue.
Unknown
inv-rconc
[@1: Harry is blue.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Harry" "is" "blue" "-")
Fiona is furry.
Unknown
rconc
[@2: Fiona is furry.[CWA. Example of deepest failure = (rule4 <- rule1 <- FAIL)]]
("Fiona" "is" "furry" "+")
Harry is not young.
Unknown
inv-rconc
[@2: Harry is young.[CWA. Example of deepest failure = (rule3 <- rule6 <- FAIL)]]
("Harry" "is" "young" "-")
Fiona is cold.
Unknown
random
[@0: Fiona is cold.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "cold" "+")
Gary is not smart.
Unknown
inv-random
[@0: Gary is smart.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "smart" "-")
Gary is big.
Unknown
random
[@0: Gary is big.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "big" "+")
@0: Fiona is smart.[(triple1)] Gary is blue.[(triple2)] Harry is big.[(triple3)] @1: Fiona is not young.[(((triple1) -> rule2))] Gary is young.[(((triple2) -> rule3))] Harry is rough.[(((triple3) -> rule1))] @2: Harry is furry.[(((((triple3) -> rule1)) -> rule4))]
Fiona is smart.
("Fiona" "is" "smart" "+")
triple1
Gary is blue.
("Gary" "is" "blue" "+")
triple2
Harry is big.
("Harry" "is" "big" "+")
triple3
Fiona is not young.
("Fiona" "is" "young" "-")
((triple1) -> (rule2 % int1))
Fiona is not young.
("Fiona" "is" "young" "-")
int1
Gary is young.
("Gary" "is" "young" "+")
((triple2) -> (rule3 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
((triple3) -> (rule1 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
((((triple3) -> (rule1 % int2))) -> (rule4 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2