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