Dave is not red. Erin is blue. Gary is green. Gary is young. Harry is not nice. Harry is quiet. Harry is not young. All green people are blue. If someone is red and young then they are nice. Green, quiet people are not nice. All red people are green. If someone is smart and not red then they are green. All red people are quiet. Blue people are quiet. If Dave is blue and Dave is not quiet then Dave is not nice.
Dave is not red.
("Dave" "is" "red" "-")
Erin is blue.
("Erin" "is" "blue" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is young.
("Gary" "is" "young" "+")
Harry is not nice.
("Harry" "is" "nice" "-")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is not young.
("Harry" "is" "young" "-")
All green people are blue.
((("someone" "is" "green" "+")) -> ("someone" "is" "blue" "+"))
If someone is red and young then they are nice.
((("someone" "is" "red" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "nice" "+"))
Green, quiet people are not nice.
((("someone" "is" "green" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "nice" "-"))
All red people are green.
((("someone" "is" "red" "+")) -> ("someone" "is" "green" "+"))
If someone is smart and not red then they are green.
((("someone" "is" "smart" "+") ("someone" "is" "red" "~")) -> ("someone" "is" "green" "+"))
All red people are quiet.
((("someone" "is" "red" "+")) -> ("someone" "is" "quiet" "+"))
Blue people are quiet.
((("someone" "is" "blue" "+")) -> ("someone" "is" "quiet" "+"))
If Dave is blue and Dave is not quiet then Dave is not nice.
((("Dave" "is" "blue" "+") ("Dave" "is" "quiet" "~")) -> ("Dave" "is" "nice" "-"))
Gary is young.
True
1
proof
[(triple4)]
("Gary" "is" "young" "+")
triple4
Harry is not quiet.
False
1
inv-proof
[(triple6)]
("Harry" "is" "quiet" "-")
triple6
Erin is quiet.
True
2
proof
[(((triple2) -> rule7))]
("Erin" "is" "quiet" "+")
((triple2) -> (rule7 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is not quiet.
False
2
inv-proof
[(((triple2) -> rule7))]
("Erin" "is" "quiet" "-")
((triple2) -> (rule7 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Gary is quiet.
True
3
proof
[(((((triple3) -> rule1)) -> rule7))]
("Gary" "is" "quiet" "+")
((((triple3) -> (rule1 % int2))) -> (rule7 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is not quiet.
False
3
inv-proof
[(((((triple3) -> rule1)) -> rule7))]
("Gary" "is" "quiet" "-")
((((triple3) -> (rule1 % int2))) -> (rule7 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is not nice.
True
5
proof
[(((triple3 ((((triple3) -> rule1)) -> rule7)) -> rule3))]
("Gary" "is" "nice" "-")
((triple3 ((((triple3) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule3 % int1))
Gary is not nice.
("Gary" "is" "nice" "-")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
int3
Gary is nice.
False
5
inv-proof
[(((triple3 ((((triple3) -> rule1)) -> rule7)) -> rule3))]
("Gary" "is" "nice" "+")
((triple3 ((((triple3) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule3 % int1))
Gary is not nice.
("Gary" "is" "nice" "-")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
int3
Harry is not green.
Unknown
inv-rconc
[@1: Harry is green.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Harry" "is" "green" "-")
Dave is blue.
Unknown
rconc
[@2: Dave is blue.[CWA. Example of deepest failure = (rule1 <- rule4 <- FAIL)]]
("Dave" "is" "blue" "+")
Dave is not quiet.
Unknown
inv-rconc
[@3: Dave is quiet.[CWA. Example of deepest failure = (rule7 <- rule1 <- rule4 <- FAIL)]]
("Dave" "is" "quiet" "-")
Erin is nice.
Unknown
rconc
[@1: Erin is nice.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Erin" "is" "nice" "+")
Erin is not smart.
Unknown
inv-random
[@0: Erin is smart.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "smart" "-")
Dave is smart.
Unknown
random
[@0: Dave is smart.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "smart" "+")
Gary is not smart.
Unknown
inv-random
[@0: Gary is smart.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "smart" "-")
Harry is red.
Unknown
random
[@0: Harry is red.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "red" "+")
@0: Dave is not red.[(triple1)] Erin is blue.[(triple2)] Gary is green.[(triple3)] Gary is young.[(triple4)] Harry is not nice.[(triple5)] Harry is not young.[(triple7)] Harry is quiet.[(triple6)] @1: Erin is quiet.[(((triple2) -> rule7))] Gary is blue.[(((triple3) -> rule1))] @2: Gary is quiet.[(((((triple3) -> rule1)) -> rule7))] @3: Gary is not nice.[(((triple3 ((((triple3) -> rule1)) -> rule7)) -> rule3))]
Dave is not red.
("Dave" "is" "red" "-")
triple1
Erin is blue.
("Erin" "is" "blue" "+")
triple2
Gary is green.
("Gary" "is" "green" "+")
triple3
Gary is young.
("Gary" "is" "young" "+")
triple4
Harry is not nice.
("Harry" "is" "nice" "-")
triple5
Harry is not young.
("Harry" "is" "young" "-")
triple7
Harry is quiet.
("Harry" "is" "quiet" "+")
triple6
Erin is quiet.
("Erin" "is" "quiet" "+")
((triple2) -> (rule7 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
((triple3) -> (rule1 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
((((triple3) -> (rule1 % int2))) -> (rule7 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is not nice.
("Gary" "is" "nice" "-")
((triple3 ((((triple3) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule3 % int1))
Gary is not nice.
("Gary" "is" "nice" "-")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
int3