Bob is kind. Bob is nice. Charlie is green. Charlie is nice. Charlie is quiet. Erin is cold. Harry is green. Young people are furry. All green people are kind. All cold people are young. All nice, kind people are young. If someone is young and green then they are kind. If someone is young and kind then they are green. If someone is furry and nice then they are quiet. Kind, furry people are quiet.
Bob is kind.
("Bob" "is" "kind" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Harry is green.
("Harry" "is" "green" "+")
Young people are furry.
((("someone" "is" "young" "+")) -> ("someone" "is" "furry" "+"))
All green people are kind.
((("someone" "is" "green" "+")) -> ("someone" "is" "kind" "+"))
All cold people are young.
((("someone" "is" "cold" "+")) -> ("someone" "is" "young" "+"))
All nice, kind people are young.
((("someone" "is" "nice" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "young" "+"))
If someone is young and green then they are kind.
((("someone" "is" "young" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "kind" "+"))
If someone is young and kind then they are green.
((("someone" "is" "young" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "green" "+"))
If someone is furry and nice then they are quiet.
((("someone" "is" "furry" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "quiet" "+"))
Kind, furry people are quiet.
((("someone" "is" "kind" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "quiet" "+"))
Charlie is nice.
True
1
proof
[(triple4)]
("Charlie" "is" "nice" "+")
triple4
Erin is not cold.
False
1
inv-proof
[(triple6)]
("Erin" "is" "cold" "-")
triple6
Bob is young.
True
3
proof
[(((triple2 triple1) -> rule4))]
("Bob" "is" "young" "+")
((triple2 triple1) -> (rule4 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Harry is not kind.
False
2
inv-proof
[(((triple7) -> rule2))]
("Harry" "is" "kind" "-")
((triple7) -> (rule2 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Bob is furry.
True
4
proof
[(((((triple2 triple1) -> rule4)) -> rule1))]
("Bob" "is" "furry" "+")
((((triple2 triple1) -> (rule4 % int2))) -> (rule1 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is not green.
False
5
inv-proof
[(((((triple2 triple1) -> rule4) triple1) -> rule6))]
("Bob" "is" "green" "-")
((((triple2 triple1) -> (rule4 % int2)) triple1) -> (rule6 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is quiet.
True
6
proof
[(((triple1 ((((triple2 triple1) -> rule4)) -> rule1)) -> rule8) OR ((((((triple2 triple1) -> rule4)) -> rule1) triple2) -> rule7))]
("Bob" "is" "quiet" "+")
((triple1 ((((triple2 triple1) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule8 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3
((((((triple2 triple1) -> (rule4 % int3))) -> (rule1 % int2)) triple2) -> (rule7 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3
Bob is not quiet.
False
6
inv-proof
[(((triple1 ((((triple2 triple1) -> rule4)) -> rule1)) -> rule8) OR ((((((triple2 triple1) -> rule4)) -> rule1) triple2) -> rule7))]
("Bob" "is" "quiet" "-")
((triple1 ((((triple2 triple1) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule8 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3
((((((triple2 triple1) -> (rule4 % int3))) -> (rule1 % int2)) triple2) -> (rule7 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3
Harry is not young.
Unknown
inv-rconc
[@1: Harry is young.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Harry" "is" "young" "-")
Erin is green.
Unknown
rconc
[@2: Erin is green.[CWA. Example of deepest failure = (rule6 <- rule2 <- FAIL)]]
("Erin" "is" "green" "+")
Harry is not furry.
Unknown
inv-rconc
[@2: Harry is furry.[CWA. Example of deepest failure = (rule1 <- rule3 <- FAIL)]]
("Harry" "is" "furry" "-")
Erin is quiet.
Unknown
rconc
[@4: Erin is quiet.[CWA. Example of deepest failure = (rule8 <- rule2 <- rule6 <- rule5 <- FAIL)]]
("Erin" "is" "quiet" "+")
Harry is not cold.
Unknown
inv-random
[@0: Harry is cold.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "cold" "-")
Harry is nice.
Unknown
random
[@0: Harry is nice.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "nice" "+")
Charlie is not cold.
Unknown
inv-random
[@0: Charlie is cold.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "cold" "-")
Bob is cold.
Unknown
random
[@0: Bob is cold.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "cold" "+")
@0: Bob is kind.[(triple1)] Bob is nice.[(triple2)] Charlie is green.[(triple3)] Charlie is nice.[(triple4)] Charlie is quiet.[(triple5 OR ((((((triple4 ((triple3) -> rule2)) -> rule4)) -> rule1) triple4) -> rule7) OR ((((triple3) -> rule2) ((((triple4 ((triple3) -> rule2)) -> rule4)) -> rule1)) -> rule8))] Erin is cold.[(triple6)] Harry is green.[(triple7)] @1: Bob is young.[(((triple2 triple1) -> rule4))] Charlie is kind.[(((triple3) -> rule2))] Erin is young.[(((triple6) -> rule3))] Harry is kind.[(((triple7) -> rule2))] @2: Bob is furry.[(((((triple2 triple1) -> rule4)) -> rule1))] Bob is green.[(((((triple2 triple1) -> rule4) triple1) -> rule6))] Charlie is young.[(((triple4 ((triple3) -> rule2)) -> rule4))] Erin is furry.[(((((triple6) -> rule3)) -> rule1))] @3: Bob is quiet.[(((triple1 ((((triple2 triple1) -> rule4)) -> rule1)) -> rule8) OR ((((((triple2 triple1) -> rule4)) -> rule1) triple2) -> rule7))] Charlie is furry.[(((((triple4 ((triple3) -> rule2)) -> rule4)) -> rule1))]
Bob is kind.
("Bob" "is" "kind" "+")
triple1
Bob is nice.
("Bob" "is" "nice" "+")
triple2
Charlie is green.
("Charlie" "is" "green" "+")
triple3
Charlie is nice.
("Charlie" "is" "nice" "+")
triple4
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple5
((((((triple4 ((triple3) -> (rule2 % int4))) -> (rule4 % int3))) -> (rule1 % int2)) triple4) -> (rule7 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
int3
Charlie is kind.
("Charlie" "is" "kind" "+")
int4
((((triple3) -> (rule2 % int4)) ((((triple4 ((triple3) -> (rule2 % int4))) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule8 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
int3
Charlie is kind.
("Charlie" "is" "kind" "+")
int4
Erin is cold.
("Erin" "is" "cold" "+")
triple6
Harry is green.
("Harry" "is" "green" "+")
triple7
Bob is young.
("Bob" "is" "young" "+")
((triple2 triple1) -> (rule4 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
((triple3) -> (rule2 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
((triple6) -> (rule3 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
((triple7) -> (rule2 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
((((triple2 triple1) -> (rule4 % int2))) -> (rule1 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
((((triple2 triple1) -> (rule4 % int2)) triple1) -> (rule6 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
((triple4 ((triple3) -> (rule2 % int2))) -> (rule4 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Erin is furry.
("Erin" "is" "furry" "+")
((((triple6) -> (rule3 % int2))) -> (rule1 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
((triple1 ((((triple2 triple1) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule8 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3
((((((triple2 triple1) -> (rule4 % int3))) -> (rule1 % int2)) triple2) -> (rule7 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3
Charlie is furry.
("Charlie" "is" "furry" "+")
((((triple4 ((triple3) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3