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