Bob is blue. Bob is cold. Erin is blue. Erin is quiet. Erin is rough. Erin is round. Fiona is blue. Fiona is rough. Fiona is round. Gary is blue. Gary is furry. Gary is smart. If something is cold then it is blue. Smart, quiet things are furry. Rough, smart things are quiet. All furry things are smart. If Bob is rough then Bob is blue. All rough, round things are quiet. Rough, round things are cold. Round things are smart.
Bob is blue.
("Bob" "is" "blue" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Erin is round.
("Erin" "is" "round" "+")
Fiona is blue.
("Fiona" "is" "blue" "+")
Fiona is rough.
("Fiona" "is" "rough" "+")
Fiona is round.
("Fiona" "is" "round" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is smart.
("Gary" "is" "smart" "+")
If something is cold then it is blue.
((("something" "is" "cold" "+")) -> ("something" "is" "blue" "+"))
Smart, quiet things are furry.
((("something" "is" "smart" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "furry" "+"))
Rough, smart things are quiet.
((("something" "is" "rough" "+") ("something" "is" "smart" "+")) -> ("something" "is" "quiet" "+"))
All furry things are smart.
((("something" "is" "furry" "+")) -> ("something" "is" "smart" "+"))
If Bob is rough then Bob is blue.
((("Bob" "is" "rough" "+")) -> ("Bob" "is" "blue" "+"))
All rough, round things are quiet.
((("something" "is" "rough" "+") ("something" "is" "round" "+")) -> ("something" "is" "quiet" "+"))
Rough, round things are cold.
((("something" "is" "rough" "+") ("something" "is" "round" "+")) -> ("something" "is" "cold" "+"))
Round things are smart.
((("something" "is" "round" "+")) -> ("something" "is" "smart" "+"))
Erin is blue.
True
1
proof
[(triple3 OR ((((triple5 triple6) -> rule7)) -> rule1))]
("Erin" "is" "blue" "+")
triple3
((((triple5 triple6) -> (rule7 % int2))) -> (rule1 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Gary is not smart.
False
1
inv-proof
[(triple12 OR ((triple11) -> rule4))]
("Gary" "is" "smart" "-")
triple12
((triple11) -> (rule4 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Fiona is quiet.
True
3
proof
[(((triple8 triple9) -> rule6) OR ((triple8 ((triple9) -> rule8)) -> rule3))]
("Fiona" "is" "quiet" "+")
((triple8 triple9) -> (rule6 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
((triple8 ((triple9) -> (rule8 % int2))) -> (rule3 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Erin is not cold.
False
3
inv-proof
[(((triple5 triple6) -> rule7))]
("Erin" "is" "cold" "-")
((triple5 triple6) -> (rule7 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Gary is not cold.
Unknown
inv-rconc
[@1: Gary is cold.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Gary" "is" "cold" "-")
Bob is quiet.
Unknown
rconc
[@1: Bob is quiet.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Bob" "is" "quiet" "+")
Gary is not rough.
Unknown
inv-random
[@0: Gary is rough.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "rough" "-")
Bob is rough.
Unknown
random
[@0: Bob is rough.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "rough" "+")
@0: Bob is blue.[(triple1 OR ((triple2) -> rule1))] Bob is cold.[(triple2)] Erin is blue.[(triple3 OR ((((triple5 triple6) -> rule7)) -> rule1))] Erin is quiet.[(triple4 OR ((triple5 triple6) -> rule6) OR ((triple5 ((triple6) -> rule8)) -> rule3))] Erin is rough.[(triple5)] Erin is round.[(triple6)] Fiona is blue.[(triple7 OR ((((triple8 triple9) -> rule7)) -> rule1))] Fiona is rough.[(triple8)] Fiona is round.[(triple9)] Gary is blue.[(triple10)] Gary is furry.[(triple11)] Gary is smart.[(triple12 OR ((triple11) -> rule4))] @1: Erin is cold.[(((triple5 triple6) -> rule7))] Erin is smart.[(((triple6) -> rule8))] Fiona is cold.[(((triple8 triple9) -> rule7))] Fiona is quiet.[(((triple8 triple9) -> rule6) OR ((triple8 ((triple9) -> rule8)) -> rule3))] Fiona is smart.[(((triple9) -> rule8))] @2: Erin is furry.[(((((triple6) -> rule8) triple4) -> rule2) OR ((((triple6) -> rule8) ((triple5 triple6) -> rule6)) -> rule2) OR ((((triple6) -> rule8) ((triple5 ((triple6) -> rule8)) -> rule3)) -> rule2))] Fiona is furry.[(((((triple9) -> rule8) ((triple8 triple9) -> rule6)) -> rule2) OR ((((triple9) -> rule8) ((triple8 ((triple9) -> rule8)) -> rule3)) -> rule2))]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
((triple2) -> (rule1 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
triple2
Erin is blue.
("Erin" "is" "blue" "+")
triple3
((((triple5 triple6) -> (rule7 % int2))) -> (rule1 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
triple4
((triple5 triple6) -> (rule6 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
((triple5 ((triple6) -> (rule8 % int2))) -> (rule3 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
triple5
Erin is round.
("Erin" "is" "round" "+")
triple6
Fiona is blue.
("Fiona" "is" "blue" "+")
triple7
((((triple8 triple9) -> (rule7 % int2))) -> (rule1 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Fiona is rough.
("Fiona" "is" "rough" "+")
triple8
Fiona is round.
("Fiona" "is" "round" "+")
triple9
Gary is blue.
("Gary" "is" "blue" "+")
triple10
Gary is furry.
("Gary" "is" "furry" "+")
triple11
Gary is smart.
("Gary" "is" "smart" "+")
triple12
((triple11) -> (rule4 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
((triple5 triple6) -> (rule7 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
((triple6) -> (rule8 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
((triple8 triple9) -> (rule7 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
((triple8 triple9) -> (rule6 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
((triple8 ((triple9) -> (rule8 % int2))) -> (rule3 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is smart.
("Fiona" "is" "smart" "+")
((triple9) -> (rule8 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
((((triple6) -> (rule8 % int2)) triple4) -> (rule2 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
((((triple6) -> (rule8 % int3)) ((triple5 triple6) -> (rule6 % int2))) -> (rule2 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
((((triple6) -> (rule8 % int3)) ((triple5 ((triple6) -> (rule8 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
Fiona is furry.
("Fiona" "is" "furry" "+")
((((triple9) -> (rule8 % int3)) ((triple8 triple9) -> (rule6 % int2))) -> (rule2 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Fiona is smart.
("Fiona" "is" "smart" "+")
int3
((((triple9) -> (rule8 % int3)) ((triple8 ((triple9) -> (rule8 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Fiona is smart.
("Fiona" "is" "smart" "+")
int3