Gary is kind. Gary is smart. Harry is smart. Smart, red people are blue. All red people are blue. All smart, kind people are blue. If someone is blue then they are not quiet. All smart people are kind. All nice, kind people are red. All nice people are green. Green, blue people are smart.
Gary is kind.
("Gary" "is" "kind" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Harry is smart.
("Harry" "is" "smart" "+")
Smart, red people are blue.
((("someone" "is" "smart" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "blue" "+"))
All red people are blue.
((("someone" "is" "red" "+")) -> ("someone" "is" "blue" "+"))
All smart, kind people are blue.
((("someone" "is" "smart" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "blue" "+"))
If someone is blue then they are not quiet.
((("someone" "is" "blue" "+")) -> ("someone" "is" "quiet" "-"))
All smart people are kind.
((("someone" "is" "smart" "+")) -> ("someone" "is" "kind" "+"))
All nice, kind people are red.
((("someone" "is" "nice" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "red" "+"))
All nice people are green.
((("someone" "is" "nice" "+")) -> ("someone" "is" "green" "+"))
Green, blue people are smart.
((("someone" "is" "green" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "smart" "+"))
Gary is smart.
True
1
proof
[(triple2)]
("Gary" "is" "smart" "+")
triple2
Harry is not smart.
False
1
inv-proof
[(triple3)]
("Harry" "is" "smart" "-")
triple3
Gary is blue.
True
3
proof
[(((triple2 triple1) -> rule3) OR ((triple2 ((triple2) -> rule5)) -> rule3))]
("Gary" "is" "blue" "+")
((triple2 triple1) -> (rule3 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
((triple2 ((triple2) -> (rule5 % int2))) -> (rule3 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is not blue.
False
3
inv-proof
[(((triple2 triple1) -> rule3) OR ((triple2 ((triple2) -> rule5)) -> rule3))]
("Gary" "is" "blue" "-")
((triple2 triple1) -> (rule3 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
((triple2 ((triple2) -> (rule5 % int2))) -> (rule3 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Harry is blue.
True
4
proof
[(((triple3 ((triple3) -> rule5)) -> rule3))]
("Harry" "is" "blue" "+")
((triple3 ((triple3) -> (rule5 % int2))) -> (rule3 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is not blue.
False
4
inv-proof
[(((triple3 ((triple3) -> rule5)) -> rule3))]
("Harry" "is" "blue" "-")
((triple3 ((triple3) -> (rule5 % int2))) -> (rule3 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is not quiet.
True
5
proof
[(((((triple3 ((triple3) -> rule5)) -> rule3)) -> rule4))]
("Harry" "is" "quiet" "-")
((((triple3 ((triple3) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Harry is not quiet.
("Harry" "is" "quiet" "-")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
int3
Harry is quiet.
False
5
inv-proof
[(((((triple3 ((triple3) -> rule5)) -> rule3)) -> rule4))]
("Harry" "is" "quiet" "+")
((((triple3 ((triple3) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Harry is not quiet.
("Harry" "is" "quiet" "-")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
int3
Harry is not green.
Unknown
inv-rconc
[@1: Harry is green.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Harry" "is" "green" "-")
Gary is green.
Unknown
rconc
[@1: Gary is green.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Gary" "is" "green" "+")
Harry is not red.
Unknown
inv-rconc
[@1: Harry is red.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Harry" "is" "red" "-")
Gary is red.
Unknown
rconc
[@1: Gary is red.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Gary" "is" "red" "+")
Harry is not nice.
Unknown
inv-random
[@0: Harry is nice.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "nice" "-")
Gary is nice.
Unknown
random
[@0: Gary is nice.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "nice" "+")
@0: Gary is kind.[(triple1 OR ((triple2) -> rule5))] Gary is smart.[(triple2)] Harry is smart.[(triple3)] @1: Gary is blue.[(((triple2 triple1) -> rule3) OR ((triple2 ((triple2) -> rule5)) -> rule3))] Harry is kind.[(((triple3) -> rule5))] @2: Gary is not quiet.[(((((triple2 triple1) -> rule3)) -> rule4) OR ((((triple2 ((triple2) -> rule5)) -> rule3)) -> rule4))] Harry is blue.[(((triple3 ((triple3) -> rule5)) -> rule3))] @3: Harry is not quiet.[(((((triple3 ((triple3) -> rule5)) -> rule3)) -> rule4))]
Gary is kind.
("Gary" "is" "kind" "+")
triple1
((triple2) -> (rule5 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
triple2
Harry is smart.
("Harry" "is" "smart" "+")
triple3
Gary is blue.
("Gary" "is" "blue" "+")
((triple2 triple1) -> (rule3 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
((triple2 ((triple2) -> (rule5 % int2))) -> (rule3 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
((triple3) -> (rule5 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Gary is not quiet.
("Gary" "is" "quiet" "-")
((((triple2 triple1) -> (rule3 % int2))) -> (rule4 % int1))
Gary is not quiet.
("Gary" "is" "quiet" "-")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
((((triple2 ((triple2) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Gary is not quiet.
("Gary" "is" "quiet" "-")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
int3
Harry is blue.
("Harry" "is" "blue" "+")
((triple3 ((triple3) -> (rule5 % int2))) -> (rule3 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is not quiet.
("Harry" "is" "quiet" "-")
((((triple3 ((triple3) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Harry is not quiet.
("Harry" "is" "quiet" "-")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
int3