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