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