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