Bob is furry. Bob is young. Charlie is green. Charlie is kind. Gary is furry. Gary is green. Gary is kind. Gary is red. Gary is young. Harry is kind. All rough, furry people are young. White people are rough. Furry, rough people are kind. If someone is kind and white then they are red. All young, white people are red. If Bob is kind and Bob is furry then Bob is white. All young people are kind. All rough, red people are kind.
Bob is furry.
("Bob" "is" "furry" "+")
Bob is young.
("Bob" "is" "young" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is young.
("Gary" "is" "young" "+")
Harry is kind.
("Harry" "is" "kind" "+")
All rough, furry people are young.
((("someone" "is" "rough" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "young" "+"))
White people are rough.
((("someone" "is" "white" "+")) -> ("someone" "is" "rough" "+"))
Furry, rough people are kind.
((("someone" "is" "furry" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "kind" "+"))
If someone is kind and white then they are red.
((("someone" "is" "kind" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "red" "+"))
All young, white people are red.
((("someone" "is" "young" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "red" "+"))
If Bob is kind and Bob is furry then Bob is white.
((("Bob" "is" "kind" "+") ("Bob" "is" "furry" "+")) -> ("Bob" "is" "white" "+"))
All young people are kind.
((("someone" "is" "young" "+")) -> ("someone" "is" "kind" "+"))
All rough, red people are kind.
((("someone" "is" "rough" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "kind" "+"))
Gary is furry.
True
1
proof
[(triple5)]
("Gary" "is" "furry" "+")
triple5
Gary is not green.
False
1
inv-proof
[(triple6)]
("Gary" "is" "green" "-")
triple6
Bob is kind.
True
2
proof
[(((triple2) -> rule7))]
("Bob" "is" "kind" "+")
((triple2) -> (rule7 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is not kind.
False
2
inv-proof
[(((triple2) -> rule7))]
("Bob" "is" "kind" "-")
((triple2) -> (rule7 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is white.
True
4
proof
[(((((triple2) -> rule7) triple1) -> rule6))]
("Bob" "is" "white" "+")
((((triple2) -> (rule7 % int2)) triple1) -> (rule6 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is not white.
False
4
inv-proof
[(((((triple2) -> rule7) triple1) -> rule6))]
("Bob" "is" "white" "-")
((((triple2) -> (rule7 % int2)) triple1) -> (rule6 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is red.
True
6
proof
[(((triple2 ((((triple2) -> rule7) triple1) -> rule6)) -> rule5) OR ((((triple2) -> rule7) ((((triple2) -> rule7) triple1) -> rule6)) -> rule4))]
("Bob" "is" "red" "+")
((triple2 ((((triple2) -> (rule7 % int3)) triple1) -> (rule6 % int2))) -> (rule5 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
int3
((((triple2) -> (rule7 % int3)) ((((triple2) -> (rule7 % int3)) triple1) -> (rule6 % int2))) -> (rule4 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
int3
Bob is not rough.
False
5
inv-proof
[(((((((triple2) -> rule7) triple1) -> rule6)) -> rule2))]
("Bob" "is" "rough" "-")
((((((triple2) -> (rule7 % int3)) triple1) -> (rule6 % int2))) -> (rule2 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
int3
Charlie is not rough.
Unknown
inv-rconc
[@1: Charlie is rough.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Charlie" "is" "rough" "-")
Harry is young.
Unknown
rconc
[@1: Harry is young.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Harry" "is" "young" "+")
Harry is not red.
Unknown
inv-rconc
[@1: Harry is red.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Harry" "is" "red" "-")
Charlie is young.
Unknown
rconc
[@1: Charlie is young.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "young" "+")
Charlie is not white.
Unknown
inv-random
[@0: Charlie is white.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "white" "-")
Gary is white.
Unknown
random
[@0: Gary is white.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "white" "+")
Charlie is not furry.
Unknown
inv-random
[@0: Charlie is furry.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "furry" "-")
Harry is furry.
Unknown
random
[@0: Harry is furry.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "furry" "+")
@0: Bob is furry.[(triple1)] Bob is young.[(triple2)] Charlie is green.[(triple3)] Charlie is kind.[(triple4)] Gary is furry.[(triple5)] Gary is green.[(triple6)] Gary is kind.[(triple7 OR ((triple9) -> rule7))] Gary is red.[(triple8)] Gary is young.[(triple9)] Harry is kind.[(triple10)] @1: Bob is kind.[(((triple2) -> rule7))] @2: Bob is white.[(((((triple2) -> rule7) triple1) -> rule6))] @3: Bob is red.[(((triple2 ((((triple2) -> rule7) triple1) -> rule6)) -> rule5) OR ((((triple2) -> rule7) ((((triple2) -> rule7) triple1) -> rule6)) -> rule4))] Bob is rough.[(((((((triple2) -> rule7) triple1) -> rule6)) -> rule2))]
Bob is furry.
("Bob" "is" "furry" "+")
triple1
Bob is young.
("Bob" "is" "young" "+")
triple2
Charlie is green.
("Charlie" "is" "green" "+")
triple3
Charlie is kind.
("Charlie" "is" "kind" "+")
triple4
Gary is furry.
("Gary" "is" "furry" "+")
triple5
Gary is green.
("Gary" "is" "green" "+")
triple6
Gary is kind.
("Gary" "is" "kind" "+")
triple7
((triple9) -> (rule7 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
triple8
Gary is young.
("Gary" "is" "young" "+")
triple9
Harry is kind.
("Harry" "is" "kind" "+")
triple10
Bob is kind.
("Bob" "is" "kind" "+")
((triple2) -> (rule7 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
((((triple2) -> (rule7 % int2)) triple1) -> (rule6 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
((triple2 ((((triple2) -> (rule7 % int3)) triple1) -> (rule6 % int2))) -> (rule5 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
int3
((((triple2) -> (rule7 % int3)) ((((triple2) -> (rule7 % int3)) triple1) -> (rule6 % int2))) -> (rule4 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
int3
Bob is rough.
("Bob" "is" "rough" "+")
((((((triple2) -> (rule7 % int3)) triple1) -> (rule6 % int2))) -> (rule2 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
int3