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