Fiona is furry. Gary is furry. Harry is red. If Gary is big and Gary is green then Gary is rough. All big, green things are furry. If something is furry and kind then it is big. All furry things are kind. If something is rough and green then it is red. All kind, big things are round. All big things are red. All kind, furry things are red.
Fiona is furry.
("Fiona" "is" "furry" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Harry is red.
("Harry" "is" "red" "+")
If Gary is big and Gary is green then Gary is rough.
((("Gary" "is" "big" "+") ("Gary" "is" "green" "+")) -> ("Gary" "is" "rough" "+"))
All big, green things are furry.
((("something" "is" "big" "+") ("something" "is" "green" "+")) -> ("something" "is" "furry" "+"))
If something is furry and kind then it is big.
((("something" "is" "furry" "+") ("something" "is" "kind" "+")) -> ("something" "is" "big" "+"))
All furry things are kind.
((("something" "is" "furry" "+")) -> ("something" "is" "kind" "+"))
If something is rough and green then it is red.
((("something" "is" "rough" "+") ("something" "is" "green" "+")) -> ("something" "is" "red" "+"))
All kind, big things are round.
((("something" "is" "kind" "+") ("something" "is" "big" "+")) -> ("something" "is" "round" "+"))
All big things are red.
((("something" "is" "big" "+")) -> ("something" "is" "red" "+"))
All kind, furry things are red.
((("something" "is" "kind" "+") ("something" "is" "furry" "+")) -> ("something" "is" "red" "+"))
Gary is furry.
True
1
proof
[(triple2)]
("Gary" "is" "furry" "+")
triple2
Harry is not red.
False
1
inv-proof
[(triple3)]
("Harry" "is" "red" "-")
triple3
Fiona is kind.
True
2
proof
[(((triple1) -> rule4))]
("Fiona" "is" "kind" "+")
((triple1) -> (rule4 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Gary is not kind.
False
2
inv-proof
[(((triple2) -> rule4))]
("Gary" "is" "kind" "-")
((triple2) -> (rule4 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is red.
True
4
proof
[(((((triple2) -> rule4) triple2) -> rule8) OR ((((triple2 ((triple2) -> rule4)) -> rule3)) -> rule7))]
("Gary" "is" "red" "+")
((((triple2) -> (rule4 % int2)) triple2) -> (rule8 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
((((triple2 ((triple2) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
int3
Fiona is not red.
False
4
inv-proof
[(((((triple1) -> rule4) triple1) -> rule8) OR ((((triple1 ((triple1) -> rule4)) -> rule3)) -> rule7))]
("Fiona" "is" "red" "-")
((((triple1) -> (rule4 % int2)) triple1) -> (rule8 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
((((triple1 ((triple1) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is kind.
("Fiona" "is" "kind" "+")
int3
Fiona is round.
True
7
proof
[(((((triple1) -> rule4) ((triple1 ((triple1) -> rule4)) -> rule3)) -> rule6))]
("Fiona" "is" "round" "+")
((((triple1) -> (rule4 % int3)) ((triple1 ((triple1) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is kind.
("Fiona" "is" "kind" "+")
int3
Gary is not round.
False
7
inv-proof
[(((((triple2) -> rule4) ((triple2 ((triple2) -> rule4)) -> rule3)) -> rule6))]
("Gary" "is" "round" "-")
((((triple2) -> (rule4 % int3)) ((triple2 ((triple2) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
int3
Harry is not kind.
Unknown
inv-rconc
[@2: Harry is kind.[CWA. Example of deepest failure = (rule4 <- rule2 <- FAIL)]]
("Harry" "is" "kind" "-")
Harry is furry.
Unknown
rconc
[@1: Harry is furry.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Harry" "is" "furry" "+")
Harry is not big.
Unknown
inv-rconc
[@2: Harry is big.[CWA. Example of deepest failure = (rule3 <- rule2 <- FAIL)]]
("Harry" "is" "big" "-")
Gary is rough.
Unknown
rconc
[@1: Gary is rough.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Gary" "is" "rough" "+")
Fiona is not green.
Unknown
inv-random
[@0: Fiona is green.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "green" "-")
Harry is green.
Unknown
random
[@0: Harry is green.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "green" "+")
Fiona is not rough.
Unknown
inv-random
[@0: Fiona is rough.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "rough" "-")
Gary is green.
Unknown
random
[@0: Gary is green.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "green" "+")
@0: Fiona is furry.[(triple1)] Gary is furry.[(triple2)] Harry is red.[(triple3)] @1: Fiona is kind.[(((triple1) -> rule4))] Gary is kind.[(((triple2) -> rule4))] @2: Fiona is big.[(((triple1 ((triple1) -> rule4)) -> rule3))] Fiona is red.[(((((triple1) -> rule4) triple1) -> rule8) OR ((((triple1 ((triple1) -> rule4)) -> rule3)) -> rule7))] Gary is big.[(((triple2 ((triple2) -> rule4)) -> rule3))] Gary is red.[(((((triple2) -> rule4) triple2) -> rule8) OR ((((triple2 ((triple2) -> rule4)) -> rule3)) -> rule7))] @3: Fiona is round.[(((((triple1) -> rule4) ((triple1 ((triple1) -> rule4)) -> rule3)) -> rule6))] Gary is round.[(((((triple2) -> rule4) ((triple2 ((triple2) -> rule4)) -> rule3)) -> rule6))]
Fiona is furry.
("Fiona" "is" "furry" "+")
triple1
Gary is furry.
("Gary" "is" "furry" "+")
triple2
Harry is red.
("Harry" "is" "red" "+")
triple3
Fiona is kind.
("Fiona" "is" "kind" "+")
((triple1) -> (rule4 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
((triple2) -> (rule4 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
((triple1 ((triple1) -> (rule4 % int2))) -> (rule3 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
Fiona is red.
("Fiona" "is" "red" "+")
((((triple1) -> (rule4 % int2)) triple1) -> (rule8 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
((((triple1 ((triple1) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is kind.
("Fiona" "is" "kind" "+")
int3
Gary is big.
("Gary" "is" "big" "+")
((triple2 ((triple2) -> (rule4 % int2))) -> (rule3 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
((((triple2) -> (rule4 % int2)) triple2) -> (rule8 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
((((triple2 ((triple2) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
int3
Fiona is round.
("Fiona" "is" "round" "+")
((((triple1) -> (rule4 % int3)) ((triple1 ((triple1) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is kind.
("Fiona" "is" "kind" "+")
int3
Gary is round.
("Gary" "is" "round" "+")
((((triple2) -> (rule4 % int3)) ((triple2 ((triple2) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
int3