Bob is white. Dave is quiet. Fiona is furry. Harry is quiet. If Bob is rough then Bob is furry. All kind things are blue. If something is furry then it is rough. All rough, furry things are young. If something is young then it is kind. Rough, furry things are kind.
Bob is white.
("Bob" "is" "white" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Fiona is furry.
("Fiona" "is" "furry" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
If Bob is rough then Bob is furry.
((("Bob" "is" "rough" "+")) -> ("Bob" "is" "furry" "+"))
All kind things are blue.
((("something" "is" "kind" "+")) -> ("something" "is" "blue" "+"))
If something is furry then it is rough.
((("something" "is" "furry" "+")) -> ("something" "is" "rough" "+"))
All rough, furry things are young.
((("something" "is" "rough" "+") ("something" "is" "furry" "+")) -> ("something" "is" "young" "+"))
If something is young then it is kind.
((("something" "is" "young" "+")) -> ("something" "is" "kind" "+"))
Rough, furry things are kind.
((("something" "is" "rough" "+") ("something" "is" "furry" "+")) -> ("something" "is" "kind" "+"))
Fiona is furry.
True
1
proof
[(triple3)]
("Fiona" "is" "furry" "+")
triple3
Dave is not quiet.
False
1
inv-proof
[(triple2)]
("Dave" "is" "quiet" "-")
triple2
Fiona is rough.
True
2
proof
[(((triple3) -> rule3))]
("Fiona" "is" "rough" "+")
((triple3) -> (rule3 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is not rough.
False
2
inv-proof
[(((triple3) -> rule3))]
("Fiona" "is" "rough" "-")
((triple3) -> (rule3 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is kind.
True
4
proof
[(((((triple3) -> rule3) triple3) -> rule6) OR ((((((triple3) -> rule3) triple3) -> rule4)) -> rule5))]
("Fiona" "is" "kind" "+")
((((triple3) -> (rule3 % int2)) triple3) -> (rule6 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2
((((((triple3) -> (rule3 % int3)) triple3) -> (rule4 % int2))) -> (rule5 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Fiona is rough.
("Fiona" "is" "rough" "+")
int3
Fiona is not young.
False
4
inv-proof
[(((((triple3) -> rule3) triple3) -> rule4))]
("Fiona" "is" "young" "-")
((((triple3) -> (rule3 % int2)) triple3) -> (rule4 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2
Fiona is blue.
True
5
proof
[(((((((triple3) -> rule3) triple3) -> rule6)) -> rule2) OR ((((((((triple3) -> rule3) triple3) -> rule4)) -> rule5)) -> rule2))]
("Fiona" "is" "blue" "+")
((((((triple3) -> (rule3 % int3)) triple3) -> (rule6 % int2))) -> (rule2 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
Fiona is rough.
("Fiona" "is" "rough" "+")
int3
((((((((triple3) -> (rule3 % int4)) triple3) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
Fiona is young.
("Fiona" "is" "young" "+")
int3
Fiona is rough.
("Fiona" "is" "rough" "+")
int4
Fiona is not blue.
False
5
inv-proof
[(((((((triple3) -> rule3) triple3) -> rule6)) -> rule2) OR ((((((((triple3) -> rule3) triple3) -> rule4)) -> rule5)) -> rule2))]
("Fiona" "is" "blue" "-")
((((((triple3) -> (rule3 % int3)) triple3) -> (rule6 % int2))) -> (rule2 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
Fiona is rough.
("Fiona" "is" "rough" "+")
int3
((((((((triple3) -> (rule3 % int4)) triple3) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
Fiona is young.
("Fiona" "is" "young" "+")
int3
Fiona is rough.
("Fiona" "is" "rough" "+")
int4
Dave is not kind.
Unknown
inv-rconc
[@2: Dave is kind.[CWA. Example of deepest failure = (rule5 <- rule4 <- FAIL)]]
("Dave" "is" "kind" "-")
Dave is rough.
Unknown
rconc
[@1: Dave is rough.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Dave" "is" "rough" "+")
Dave is not young.
Unknown
inv-rconc
[@1: Dave is young.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Dave" "is" "young" "-")
Bob is young.
Unknown
rconc
[@3: Bob is young.[CWA. Example of deepest failure = (rule4 <- rule3 <- rule1 <- FAIL)]]
("Bob" "is" "young" "+")
Dave is not white.
Unknown
inv-random
[@0: Dave is white.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "white" "-")
Harry is white.
Unknown
random
[@0: Harry is white.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "white" "+")
Bob is not quiet.
Unknown
inv-random
[@0: Bob is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "quiet" "-")
Fiona is white.
Unknown
random
[@0: Fiona is white.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "white" "+")
@0: Bob is white.[(triple1)] Dave is quiet.[(triple2)] Fiona is furry.[(triple3)] Harry is quiet.[(triple4)] @1: Fiona is rough.[(((triple3) -> rule3))] @2: Fiona is kind.[(((((triple3) -> rule3) triple3) -> rule6) OR ((((((triple3) -> rule3) triple3) -> rule4)) -> rule5))] Fiona is young.[(((((triple3) -> rule3) triple3) -> rule4))] @3: Fiona is blue.[(((((((triple3) -> rule3) triple3) -> rule6)) -> rule2) OR ((((((((triple3) -> rule3) triple3) -> rule4)) -> rule5)) -> rule2))]
Bob is white.
("Bob" "is" "white" "+")
triple1
Dave is quiet.
("Dave" "is" "quiet" "+")
triple2
Fiona is furry.
("Fiona" "is" "furry" "+")
triple3
Harry is quiet.
("Harry" "is" "quiet" "+")
triple4
Fiona is rough.
("Fiona" "is" "rough" "+")
((triple3) -> (rule3 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
((((triple3) -> (rule3 % int2)) triple3) -> (rule6 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2
((((((triple3) -> (rule3 % int3)) triple3) -> (rule4 % int2))) -> (rule5 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Fiona is rough.
("Fiona" "is" "rough" "+")
int3
Fiona is young.
("Fiona" "is" "young" "+")
((((triple3) -> (rule3 % int2)) triple3) -> (rule4 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2
Fiona is blue.
("Fiona" "is" "blue" "+")
((((((triple3) -> (rule3 % int3)) triple3) -> (rule6 % int2))) -> (rule2 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
Fiona is rough.
("Fiona" "is" "rough" "+")
int3
((((((((triple3) -> (rule3 % int4)) triple3) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
Fiona is young.
("Fiona" "is" "young" "+")
int3
Fiona is rough.
("Fiona" "is" "rough" "+")
int4