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