Bob is furry. Bob is round. Bob is white. Erin is blue. Erin is quiet. Erin is red. Erin is round. Erin is smart. Fiona is blue. Fiona is furry. Fiona is quiet. Fiona is smart. Harry is blue. Harry is quiet. Harry is red. If someone is blue and white then they are quiet. White, quiet people are smart. Furry people are blue. If someone is quiet and red then they are blue. Smart, white people are quiet. If Harry is red then Harry is quiet.
Bob is furry.
("Bob" "is" "furry" "+")
Bob is round.
("Bob" "is" "round" "+")
Bob is white.
("Bob" "is" "white" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is red.
("Erin" "is" "red" "+")
Erin is round.
("Erin" "is" "round" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Fiona is blue.
("Fiona" "is" "blue" "+")
Fiona is furry.
("Fiona" "is" "furry" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is red.
("Harry" "is" "red" "+")
If someone is blue and white then they are quiet.
((("someone" "is" "blue" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "quiet" "+"))
White, quiet people are smart.
((("someone" "is" "white" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "smart" "+"))
Furry people are blue.
((("someone" "is" "furry" "+")) -> ("someone" "is" "blue" "+"))
If someone is quiet and red then they are blue.
((("someone" "is" "quiet" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "blue" "+"))
Smart, white people are quiet.
((("someone" "is" "smart" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "quiet" "+"))
If Harry is red then Harry is quiet.
((("Harry" "is" "red" "+")) -> ("Harry" "is" "quiet" "+"))
Fiona is quiet.
True
1
proof
[(triple11)]
("Fiona" "is" "quiet" "+")
triple11
Fiona is not quiet.
False
1
inv-proof
[(triple11)]
("Fiona" "is" "quiet" "-")
triple11
Bob is blue.
True
2
proof
[(((triple1) -> rule3))]
("Bob" "is" "blue" "+")
((triple1) -> (rule3 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is not blue.
False
2
inv-proof
[(((triple1) -> rule3))]
("Bob" "is" "blue" "-")
((triple1) -> (rule3 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is quiet.
True
4
proof
[(((((triple1) -> rule3) triple3) -> rule1))]
("Bob" "is" "quiet" "+")
((((triple1) -> (rule3 % int2)) triple3) -> (rule1 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is not quiet.
False
4
inv-proof
[(((((triple1) -> rule3) triple3) -> rule1))]
("Bob" "is" "quiet" "-")
((((triple1) -> (rule3 % int2)) triple3) -> (rule1 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is smart.
True
6
proof
[(((triple3 ((((triple1) -> rule3) triple3) -> rule1)) -> rule2))]
("Bob" "is" "smart" "+")
((triple3 ((((triple1) -> (rule3 % int3)) triple3) -> (rule1 % int2))) -> (rule2 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
int3
Bob is not smart.
False
6
inv-proof
[(((triple3 ((((triple1) -> rule3) triple3) -> rule1)) -> rule2))]
("Bob" "is" "smart" "-")
((triple3 ((((triple1) -> (rule3 % int3)) triple3) -> (rule1 % int2))) -> (rule2 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
int3
Harry is not smart.
Unknown
inv-rconc
[@1: Harry is smart.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Harry" "is" "smart" "-")
Harry is white.
Unknown
random
[@0: Harry is white.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "white" "+")
Fiona is not round.
Unknown
inv-random
[@0: Fiona is round.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "round" "-")
Fiona is white.
Unknown
random
[@0: Fiona is white.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "white" "+")
Fiona is not red.
Unknown
inv-random
[@0: Fiona is red.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "red" "-")
Harry is furry.
Unknown
random
[@0: Harry is furry.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "furry" "+")
Erin is not furry.
Unknown
inv-random
[@0: Erin is furry.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "furry" "-")
Bob is red.
Unknown
random
[@0: Bob is red.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "red" "+")
@0: Bob is furry.[(triple1)] Bob is round.[(triple2)] Bob is white.[(triple3)] Erin is blue.[(triple4 OR ((triple5 triple6) -> rule4))] Erin is quiet.[(triple5)] Erin is red.[(triple6)] Erin is round.[(triple7)] Erin is smart.[(triple8)] Fiona is blue.[(triple9 OR ((triple10) -> rule3))] Fiona is furry.[(triple10)] Fiona is quiet.[(triple11)] Fiona is smart.[(triple12)] Harry is blue.[(triple13 OR ((triple14 triple15) -> rule4) OR ((((triple15) -> rule6) triple15) -> rule4))] Harry is quiet.[(triple14 OR ((triple15) -> rule6))] Harry is red.[(triple15)] @1: Bob is blue.[(((triple1) -> rule3))] @2: Bob is quiet.[(((((triple1) -> rule3) triple3) -> rule1))] @3: Bob is smart.[(((triple3 ((((triple1) -> rule3) triple3) -> rule1)) -> rule2))]
Bob is furry.
("Bob" "is" "furry" "+")
triple1
Bob is round.
("Bob" "is" "round" "+")
triple2
Bob is white.
("Bob" "is" "white" "+")
triple3
Erin is blue.
("Erin" "is" "blue" "+")
triple4
((triple5 triple6) -> (rule4 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
triple5
Erin is red.
("Erin" "is" "red" "+")
triple6
Erin is round.
("Erin" "is" "round" "+")
triple7
Erin is smart.
("Erin" "is" "smart" "+")
triple8
Fiona is blue.
("Fiona" "is" "blue" "+")
triple9
((triple10) -> (rule3 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is furry.
("Fiona" "is" "furry" "+")
triple10
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple11
Fiona is smart.
("Fiona" "is" "smart" "+")
triple12
Harry is blue.
("Harry" "is" "blue" "+")
triple13
((triple14 triple15) -> (rule4 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
((((triple15) -> (rule6 % int2)) triple15) -> (rule4 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
triple14
((triple15) -> (rule6 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
triple15
Bob is blue.
("Bob" "is" "blue" "+")
((triple1) -> (rule3 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
((((triple1) -> (rule3 % int2)) triple3) -> (rule1 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
((triple3 ((((triple1) -> (rule3 % int3)) triple3) -> (rule1 % int2))) -> (rule2 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
int3