Anne is furry. Fiona is furry. Gary is red. Gary is round. Gary is smart. Harry is furry. Harry is young. If something is white then it is big. All round, furry things are white. All young things are round.
Anne is furry.
("Anne" "is" "furry" "+")
Fiona is furry.
("Fiona" "is" "furry" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is round.
("Gary" "is" "round" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is young.
("Harry" "is" "young" "+")
If something is white then it is big.
((("something" "is" "white" "+")) -> ("something" "is" "big" "+"))
All round, furry things are white.
((("something" "is" "round" "+") ("something" "is" "furry" "+")) -> ("something" "is" "white" "+"))
All young things are round.
((("something" "is" "young" "+")) -> ("something" "is" "round" "+"))
Harry is young.
True
1
proof
[(triple7)]
("Harry" "is" "young" "+")
triple7
Gary is not round.
False
1
inv-proof
[(triple4)]
("Gary" "is" "round" "-")
triple4
Harry is round.
True
2
proof
[(((triple7) -> rule3))]
("Harry" "is" "round" "+")
((triple7) -> (rule3 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is not round.
False
2
inv-proof
[(((triple7) -> rule3))]
("Harry" "is" "round" "-")
((triple7) -> (rule3 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is white.
True
4
proof
[(((((triple7) -> rule3) triple6) -> rule2))]
("Harry" "is" "white" "+")
((((triple7) -> (rule3 % int2)) triple6) -> (rule2 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is not white.
False
4
inv-proof
[(((((triple7) -> rule3) triple6) -> rule2))]
("Harry" "is" "white" "-")
((((triple7) -> (rule3 % int2)) triple6) -> (rule2 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is big.
True
5
proof
[(((((((triple7) -> rule3) triple6) -> rule2)) -> rule1))]
("Harry" "is" "big" "+")
((((((triple7) -> (rule3 % int3)) triple6) -> (rule2 % int2))) -> (rule1 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
int3
Harry is not big.
False
5
inv-proof
[(((((((triple7) -> rule3) triple6) -> rule2)) -> rule1))]
("Harry" "is" "big" "-")
((((((triple7) -> (rule3 % int3)) triple6) -> (rule2 % int2))) -> (rule1 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
int3
Gary is not white.
Unknown
inv-rconc
[@1: Gary is white.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Gary" "is" "white" "-")
Anne is white.
Unknown
rconc
[@2: Anne is white.[CWA. Example of deepest failure = (rule2 <- rule3 <- FAIL)]]
("Anne" "is" "white" "+")
Gary is not big.
Unknown
inv-rconc
[@2: Gary is big.[CWA. Example of deepest failure = (rule1 <- rule2 <- FAIL)]]
("Gary" "is" "big" "-")
Fiona is round.
Unknown
rconc
[@1: Fiona is round.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Fiona" "is" "round" "+")
Gary is not furry.
Unknown
inv-random
[@0: Gary is furry.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "furry" "-")
Harry is smart.
Unknown
random
[@0: Harry is smart.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "smart" "+")
Anne is not smart.
Unknown
inv-random
[@0: Anne is smart.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "smart" "-")
Fiona is smart.
Unknown
random
[@0: Fiona is smart.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "smart" "+")
@0: Anne is furry.[(triple1)] Fiona is furry.[(triple2)] Gary is red.[(triple3)] Gary is round.[(triple4)] Gary is smart.[(triple5)] Harry is furry.[(triple6)] Harry is young.[(triple7)] @1: Harry is round.[(((triple7) -> rule3))] @2: Harry is white.[(((((triple7) -> rule3) triple6) -> rule2))] @3: Harry is big.[(((((((triple7) -> rule3) triple6) -> rule2)) -> rule1))]
Anne is furry.
("Anne" "is" "furry" "+")
triple1
Fiona is furry.
("Fiona" "is" "furry" "+")
triple2
Gary is red.
("Gary" "is" "red" "+")
triple3
Gary is round.
("Gary" "is" "round" "+")
triple4
Gary is smart.
("Gary" "is" "smart" "+")
triple5
Harry is furry.
("Harry" "is" "furry" "+")
triple6
Harry is young.
("Harry" "is" "young" "+")
triple7
Harry is round.
("Harry" "is" "round" "+")
((triple7) -> (rule3 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
((((triple7) -> (rule3 % int2)) triple6) -> (rule2 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
((((((triple7) -> (rule3 % int3)) triple6) -> (rule2 % int2))) -> (rule1 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
int3