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