Erin is big. Harry is big. If something is big then it is young. Big, young things are white. If something is white and not big then it is not round. Young things are round. If something is white then it is not rough. If something is rough and not young then it is furry. If something is big then it is smart. Rough, furry things are smart.
Erin is big.
("Erin" "is" "big" "+")
Harry is big.
("Harry" "is" "big" "+")
If something is big then it is young.
((("something" "is" "big" "+")) -> ("something" "is" "young" "+"))
Big, young things are white.
((("something" "is" "big" "+") ("something" "is" "young" "+")) -> ("something" "is" "white" "+"))
If something is white and not big then it is not round.
((("something" "is" "white" "+") ("something" "is" "big" "~")) -> ("something" "is" "round" "-"))
Young things are round.
((("something" "is" "young" "+")) -> ("something" "is" "round" "+"))
If something is white then it is not rough.
((("something" "is" "white" "+")) -> ("something" "is" "rough" "-"))
If something is rough and not young then it is furry.
((("something" "is" "rough" "+") ("something" "is" "young" "~")) -> ("something" "is" "furry" "+"))
If something is big then it is smart.
((("something" "is" "big" "+")) -> ("something" "is" "smart" "+"))
Rough, furry things are smart.
((("something" "is" "rough" "+") ("something" "is" "furry" "+")) -> ("something" "is" "smart" "+"))
Erin is big.
True
1
proof
[(triple1)]
("Erin" "is" "big" "+")
triple1
Harry is not big.
False
1
inv-proof
[(triple2)]
("Harry" "is" "big" "-")
triple2
Harry is young.
True
2
proof
[(((triple2) -> rule1))]
("Harry" "is" "young" "+")
((triple2) -> (rule1 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is not smart.
False
2
inv-proof
[(((triple2) -> rule7))]
("Harry" "is" "smart" "-")
((triple2) -> (rule7 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Erin is round.
True
3
proof
[(((((triple1) -> rule1)) -> rule4))]
("Erin" "is" "round" "+")
((((triple1) -> (rule1 % int2))) -> (rule4 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is not round.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule4))]
("Erin" "is" "round" "-")
((((triple1) -> (rule1 % int2))) -> (rule4 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Harry is not rough.
True
5
proof
[(((((triple2 ((triple2) -> rule1)) -> rule2)) -> rule5))]
("Harry" "is" "rough" "-")
((((triple2 ((triple2) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Harry is not rough.
("Harry" "is" "rough" "-")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
int3
Harry is rough.
False
5
inv-proof
[(((((triple2 ((triple2) -> rule1)) -> rule2)) -> rule5))]
("Harry" "is" "rough" "+")
((((triple2 ((triple2) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Harry is not rough.
("Harry" "is" "rough" "-")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
int3
Erin is not furry.
Unknown
inv-rconc
[@1: Erin is furry.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Erin" "is" "furry" "-")
Harry is furry.
Unknown
rconc
[@1: Harry is furry.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Harry" "is" "furry" "+")
@0: Erin is big.[(triple1)] Harry is big.[(triple2)] @1: Erin is smart.[(((triple1) -> rule7))] Erin is young.[(((triple1) -> rule1))] Harry is smart.[(((triple2) -> rule7))] Harry is young.[(((triple2) -> rule1))] @2: Erin is round.[(((((triple1) -> rule1)) -> rule4))] Erin is white.[(((triple1 ((triple1) -> rule1)) -> rule2))] Harry is round.[(((((triple2) -> rule1)) -> rule4))] Harry is white.[(((triple2 ((triple2) -> rule1)) -> rule2))] @3: Erin is not rough.[(((((triple1 ((triple1) -> rule1)) -> rule2)) -> rule5))] Harry is not rough.[(((((triple2 ((triple2) -> rule1)) -> rule2)) -> rule5))]
Erin is big.
("Erin" "is" "big" "+")
triple1
Harry is big.
("Harry" "is" "big" "+")
triple2
Erin is smart.
("Erin" "is" "smart" "+")
((triple1) -> (rule7 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
((triple1) -> (rule1 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
((triple2) -> (rule7 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
((triple2) -> (rule1 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
((((triple1) -> (rule1 % int2))) -> (rule4 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is white.
("Erin" "is" "white" "+")
((triple1 ((triple1) -> (rule1 % int2))) -> (rule2 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
((((triple2) -> (rule1 % int2))) -> (rule4 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
((triple2 ((triple2) -> (rule1 % int2))) -> (rule2 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Erin is not rough.
("Erin" "is" "rough" "-")
((((triple1 ((triple1) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Erin is not rough.
("Erin" "is" "rough" "-")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
int3
Harry is not rough.
("Harry" "is" "rough" "-")
((((triple2 ((triple2) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Harry is not rough.
("Harry" "is" "rough" "-")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
int3