Anne is cold. Anne is quiet. Anne is smart. Anne is young. Erin is green. Erin is quiet. Erin is young. Fiona is furry. Fiona is smart. Fiona is young. Harry is kind. Harry is young. Kind people are green. If someone is green then they are not cold. All green people are kind. If someone is young and smart then they are furry. All cold, smart people are furry. Quiet, smart people are young. Furry, kind people are quiet. If someone is cold and not kind then they are smart. If someone is kind and not cold then they are smart.
Anne is cold.
("Anne" "is" "cold" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Anne is young.
("Anne" "is" "young" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is young.
("Erin" "is" "young" "+")
Fiona is furry.
("Fiona" "is" "furry" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
Fiona is young.
("Fiona" "is" "young" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is young.
("Harry" "is" "young" "+")
Kind people are green.
((("someone" "is" "kind" "+")) -> ("someone" "is" "green" "+"))
If someone is green then they are not cold.
((("someone" "is" "green" "+")) -> ("someone" "is" "cold" "-"))
All green people are kind.
((("someone" "is" "green" "+")) -> ("someone" "is" "kind" "+"))
If someone is young and smart then they are furry.
((("someone" "is" "young" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "furry" "+"))
All cold, smart people are furry.
((("someone" "is" "cold" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "furry" "+"))
Quiet, smart people are young.
((("someone" "is" "quiet" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "young" "+"))
Furry, kind people are quiet.
((("someone" "is" "furry" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "quiet" "+"))
If someone is cold and not kind then they are smart.
((("someone" "is" "cold" "+") ("someone" "is" "kind" "~")) -> ("someone" "is" "smart" "+"))
If someone is kind and not cold then they are smart.
((("someone" "is" "kind" "+") ("someone" "is" "cold" "~")) -> ("someone" "is" "smart" "+"))
Fiona is young.
True
1
proof
[(triple10)]
("Fiona" "is" "young" "+")
triple10
Fiona is not young.
False
1
inv-proof
[(triple10)]
("Fiona" "is" "young" "-")
triple10
Erin is not cold.
True
2
proof
[(((triple5) -> rule2))]
("Erin" "is" "cold" "-")
((triple5) -> (rule2 % int1))
Erin is not cold.
("Erin" "is" "cold" "-")
int1
Harry is not green.
False
2
inv-proof
[(((triple11) -> rule1))]
("Harry" "is" "green" "-")
((triple11) -> (rule1 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Erin is smart.
True
5
proof
[(((((triple5) -> rule3) ((triple5) -> rule2)) -> rule9))]
("Erin" "is" "smart" "+")
((((triple5) -> (rule3 % int3)) ((triple5) -> (rule2 % int2))) -> (rule9 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is not cold.
("Erin" "is" "cold" "-")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
Harry is cold.
False
3
inv-proof
[(((((triple11) -> rule1)) -> rule2))]
("Harry" "is" "cold" "+")
((((triple11) -> (rule1 % int2))) -> (rule2 % int1))
Harry is not cold.
("Harry" "is" "cold" "-")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is smart.
True
5
proof
[(((triple11 ((((triple11) -> rule1)) -> rule2)) -> rule9))]
("Harry" "is" "smart" "+")
((triple11 ((((triple11) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule9 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is not cold.
("Harry" "is" "cold" "-")
int2
Harry is green.
("Harry" "is" "green" "+")
int3
Erin is not furry.
False
7
inv-proof
[(((triple7 ((((triple5) -> rule3) ((triple5) -> rule2)) -> rule9)) -> rule4) OR ((((triple6 ((((triple5) -> rule3) ((triple5) -> rule2)) -> rule9)) -> rule6) ((((triple5) -> rule3) ((triple5) -> rule2)) -> rule9)) -> rule4))]
("Erin" "is" "furry" "-")
((triple7 ((((triple5) -> (rule3 % int4)) ((triple5) -> (rule2 % int3))) -> (rule9 % int2))) -> (rule4 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is not cold.
("Erin" "is" "cold" "-")
int3
Erin is kind.
("Erin" "is" "kind" "+")
int4
((((triple6 ((((triple5) -> (rule3 % int5)) ((triple5) -> (rule2 % int4))) -> (rule9 % int3))) -> (rule6 % int2)) ((((triple5) -> (rule3 % int5)) ((triple5) -> (rule2 % int4))) -> (rule9 % int3))) -> (rule4 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
Erin is not cold.
("Erin" "is" "cold" "-")
int4
Erin is kind.
("Erin" "is" "kind" "+")
int5
Harry is furry.
True
7
proof
[(((triple12 ((triple11 ((((triple11) -> rule1)) -> rule2)) -> rule9)) -> rule4))]
("Harry" "is" "furry" "+")
((triple12 ((triple11 ((((triple11) -> (rule1 % int4))) -> (rule2 % int3))) -> (rule9 % int2))) -> (rule4 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is not cold.
("Harry" "is" "cold" "-")
int3
Harry is green.
("Harry" "is" "green" "+")
int4
Harry is not furry.
False
7
inv-proof
[(((triple12 ((triple11 ((((triple11) -> rule1)) -> rule2)) -> rule9)) -> rule4))]
("Harry" "is" "furry" "-")
((triple12 ((triple11 ((((triple11) -> (rule1 % int4))) -> (rule2 % int3))) -> (rule9 % int2))) -> (rule4 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is not cold.
("Harry" "is" "cold" "-")
int3
Harry is green.
("Harry" "is" "green" "+")
int4
Harry is quiet.
True
9
proof
[(((((triple12 ((triple11 ((((triple11) -> rule1)) -> rule2)) -> rule9)) -> rule4) triple11) -> rule7))]
("Harry" "is" "quiet" "+")
((((triple12 ((triple11 ((((triple11) -> (rule1 % int5))) -> (rule2 % int4))) -> (rule9 % int3))) -> (rule4 % int2)) triple11) -> (rule7 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
int3
Harry is not cold.
("Harry" "is" "cold" "-")
int4
Harry is green.
("Harry" "is" "green" "+")
int5
Harry is not quiet.
False
9
inv-proof
[(((((triple12 ((triple11 ((((triple11) -> rule1)) -> rule2)) -> rule9)) -> rule4) triple11) -> rule7))]
("Harry" "is" "quiet" "-")
((((triple12 ((triple11 ((((triple11) -> (rule1 % int5))) -> (rule2 % int4))) -> (rule9 % int3))) -> (rule4 % int2)) triple11) -> (rule7 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
int3
Harry is not cold.
("Harry" "is" "cold" "-")
int4
Harry is green.
("Harry" "is" "green" "+")
int5
Fiona is not green.
Unknown
inv-rconc
[@2: Fiona is green.[CWA. Example of deepest failure = (rule1 <- rule3 <- FAIL)]]
("Fiona" "is" "green" "-")
Anne is kind.
Unknown
rconc
[@2: Anne is kind.[CWA. Example of deepest failure = (rule3 <- rule1 <- FAIL)]]
("Anne" "is" "kind" "+")
Anne is not green.
Unknown
inv-rconc
[@2: Anne is green.[CWA. Example of deepest failure = (rule1 <- rule3 <- FAIL)]]
("Anne" "is" "green" "-")
Fiona is kind.
Unknown
rconc
[@2: Fiona is kind.[CWA. Example of deepest failure = (rule3 <- rule1 <- FAIL)]]
("Fiona" "is" "kind" "+")
Fiona is not quiet.
Unknown
inv-rconc
[@3: Fiona is quiet.[CWA. Example of deepest failure = (rule7 <- rule3 <- rule1 <- FAIL)]]
("Fiona" "is" "quiet" "-")
Fiona is cold.
Unknown
random
[@0: Fiona is cold.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "cold" "+")
@0: Anne is cold.[(triple1)] Anne is quiet.[(triple2)] Anne is smart.[(triple3)] Anne is young.[(triple4 OR ((triple2 triple3) -> rule6))] Erin is green.[(triple5)] Erin is quiet.[(triple6 OR ((((triple7 ((((triple5) -> rule3) ((triple5) -> rule2)) -> rule9)) -> rule4) ((triple5) -> rule3)) -> rule7))] Erin is young.[(triple7 OR ((triple6 ((((triple5) -> rule3) ((triple5) -> rule2)) -> rule9)) -> rule6))] Fiona is furry.[(triple8 OR ((triple10 triple9) -> rule4))] Fiona is smart.[(triple9)] Fiona is young.[(triple10)] Harry is kind.[(triple11)] Harry is young.[(triple12)] @1: Anne is furry.[(((triple1 triple3) -> rule5) OR ((triple4 triple3) -> rule4) OR ((((triple2 triple3) -> rule6) triple3) -> rule4))] Erin is kind.[(((triple5) -> rule3))] Erin is not cold.[(((triple5) -> rule2))] Harry is green.[(((triple11) -> rule1))] @2: Erin is smart.[(((((triple5) -> rule3) ((triple5) -> rule2)) -> rule9))] Harry is not cold.[(((((triple11) -> rule1)) -> rule2))] @3: Erin is furry.[(((triple7 ((((triple5) -> rule3) ((triple5) -> rule2)) -> rule9)) -> rule4) OR ((((triple6 ((((triple5) -> rule3) ((triple5) -> rule2)) -> rule9)) -> rule6) ((((triple5) -> rule3) ((triple5) -> rule2)) -> rule9)) -> rule4))] Harry is smart.[(((triple11 ((((triple11) -> rule1)) -> rule2)) -> rule9))] @4: Harry is furry.[(((triple12 ((triple11 ((((triple11) -> rule1)) -> rule2)) -> rule9)) -> rule4))] @5: Harry is quiet.[(((((triple12 ((triple11 ((((triple11) -> rule1)) -> rule2)) -> rule9)) -> rule4) triple11) -> rule7))]
Anne is cold.
("Anne" "is" "cold" "+")
triple1
Anne is quiet.
("Anne" "is" "quiet" "+")
triple2
Anne is smart.
("Anne" "is" "smart" "+")
triple3
Anne is young.
("Anne" "is" "young" "+")
triple4
((triple2 triple3) -> (rule6 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
triple5
Erin is quiet.
("Erin" "is" "quiet" "+")
triple6
((((triple7 ((((triple5) -> (rule3 % int5)) ((triple5) -> (rule2 % int4))) -> (rule9 % int3))) -> (rule4 % int2)) ((triple5) -> (rule3 % int5))) -> (rule7 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
Erin is not cold.
("Erin" "is" "cold" "-")
int4
Erin is kind.
("Erin" "is" "kind" "+")
int5
Erin is young.
("Erin" "is" "young" "+")
triple7
((triple6 ((((triple5) -> (rule3 % int4)) ((triple5) -> (rule2 % int3))) -> (rule9 % int2))) -> (rule6 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is not cold.
("Erin" "is" "cold" "-")
int3
Erin is kind.
("Erin" "is" "kind" "+")
int4
Fiona is furry.
("Fiona" "is" "furry" "+")
triple8
((triple10 triple9) -> (rule4 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
triple9
Fiona is young.
("Fiona" "is" "young" "+")
triple10
Harry is kind.
("Harry" "is" "kind" "+")
triple11
Harry is young.
("Harry" "is" "young" "+")
triple12
Anne is furry.
("Anne" "is" "furry" "+")
((triple1 triple3) -> (rule5 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
((triple4 triple3) -> (rule4 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
((((triple2 triple3) -> (rule6 % int2)) triple3) -> (rule4 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
((triple5) -> (rule3 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is not cold.
("Erin" "is" "cold" "-")
((triple5) -> (rule2 % int1))
Erin is not cold.
("Erin" "is" "cold" "-")
int1
Harry is green.
("Harry" "is" "green" "+")
((triple11) -> (rule1 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
((((triple5) -> (rule3 % int3)) ((triple5) -> (rule2 % int2))) -> (rule9 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is not cold.
("Erin" "is" "cold" "-")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
Harry is not cold.
("Harry" "is" "cold" "-")
((((triple11) -> (rule1 % int2))) -> (rule2 % int1))
Harry is not cold.
("Harry" "is" "cold" "-")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Erin is furry.
("Erin" "is" "furry" "+")
((triple7 ((((triple5) -> (rule3 % int4)) ((triple5) -> (rule2 % int3))) -> (rule9 % int2))) -> (rule4 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is not cold.
("Erin" "is" "cold" "-")
int3
Erin is kind.
("Erin" "is" "kind" "+")
int4
((((triple6 ((((triple5) -> (rule3 % int5)) ((triple5) -> (rule2 % int4))) -> (rule9 % int3))) -> (rule6 % int2)) ((((triple5) -> (rule3 % int5)) ((triple5) -> (rule2 % int4))) -> (rule9 % int3))) -> (rule4 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
Erin is not cold.
("Erin" "is" "cold" "-")
int4
Erin is kind.
("Erin" "is" "kind" "+")
int5
Harry is smart.
("Harry" "is" "smart" "+")
((triple11 ((((triple11) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule9 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is not cold.
("Harry" "is" "cold" "-")
int2
Harry is green.
("Harry" "is" "green" "+")
int3
Harry is furry.
("Harry" "is" "furry" "+")
((triple12 ((triple11 ((((triple11) -> (rule1 % int4))) -> (rule2 % int3))) -> (rule9 % int2))) -> (rule4 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is not cold.
("Harry" "is" "cold" "-")
int3
Harry is green.
("Harry" "is" "green" "+")
int4
Harry is quiet.
("Harry" "is" "quiet" "+")
((((triple12 ((triple11 ((((triple11) -> (rule1 % int5))) -> (rule2 % int4))) -> (rule9 % int3))) -> (rule4 % int2)) triple11) -> (rule7 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
int3
Harry is not cold.
("Harry" "is" "cold" "-")
int4
Harry is green.
("Harry" "is" "green" "+")
int5