Charlie is blue. Charlie is cold. Charlie is furry. Charlie is green. Charlie is nice. Charlie is round. Dave is cold. Erin is blue. Erin is cold. Erin is furry. Erin is green. Erin is red. Erin is round. Fiona is blue. Fiona is furry. Fiona is round. All round things are cold. If something is furry then it is cold. If something is round then it is cold. All blue, furry things are green. If Dave is round then Dave is furry. If something is red then it is furry. All red, green things are cold. Cold things are green.
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is red.
("Erin" "is" "red" "+")
Erin is round.
("Erin" "is" "round" "+")
Fiona is blue.
("Fiona" "is" "blue" "+")
Fiona is furry.
("Fiona" "is" "furry" "+")
Fiona is round.
("Fiona" "is" "round" "+")
All round things are cold.
((("something" "is" "round" "+")) -> ("something" "is" "cold" "+"))
If something is furry then it is cold.
((("something" "is" "furry" "+")) -> ("something" "is" "cold" "+"))
If something is round then it is cold.
((("something" "is" "round" "+")) -> ("something" "is" "cold" "+"))
All blue, furry things are green.
((("something" "is" "blue" "+") ("something" "is" "furry" "+")) -> ("something" "is" "green" "+"))
If Dave is round then Dave is furry.
((("Dave" "is" "round" "+")) -> ("Dave" "is" "furry" "+"))
If something is red then it is furry.
((("something" "is" "red" "+")) -> ("something" "is" "furry" "+"))
All red, green things are cold.
((("something" "is" "red" "+") ("something" "is" "green" "+")) -> ("something" "is" "cold" "+"))
Cold things are green.
((("something" "is" "cold" "+")) -> ("something" "is" "green" "+"))
Charlie is blue.
True
1
proof
[(triple1)]
("Charlie" "is" "blue" "+")
triple1
Fiona is not blue.
False
1
inv-proof
[(triple14)]
("Fiona" "is" "blue" "-")
triple14
Fiona is green.
True
3
proof
[(((triple14 triple15) -> rule4) OR ((((triple15) -> rule2)) -> rule8) OR ((((triple16) -> rule1)) -> rule8) OR ((((triple16) -> rule3)) -> rule8))]
("Fiona" "is" "green" "+")
((triple14 triple15) -> (rule4 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
((((triple15) -> (rule2 % int2))) -> (rule8 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
((((triple16) -> (rule1 % int2))) -> (rule8 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
((((triple16) -> (rule3 % int2))) -> (rule8 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Fiona is not cold.
False
2
inv-proof
[(((triple15) -> rule2) OR ((triple16) -> rule1) OR ((triple16) -> rule3))]
("Fiona" "is" "cold" "-")
((triple15) -> (rule2 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
((triple16) -> (rule1 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
((triple16) -> (rule3 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Dave is not furry.
Unknown
inv-rconc
[@1: Dave is furry.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Dave" "is" "furry" "-")
Erin is nice.
Unknown
random
[@0: Erin is nice.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "nice" "+")
Fiona is not nice.
Unknown
inv-random
[@0: Fiona is nice.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "nice" "-")
Dave is red.
Unknown
random
[@0: Dave is red.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "red" "+")
@0: Charlie is blue.[(triple1)] Charlie is cold.[(triple2 OR ((triple3) -> rule2) OR ((triple6) -> rule1) OR ((triple6) -> rule3))] Charlie is furry.[(triple3)] Charlie is green.[(triple4 OR ((triple2) -> rule8) OR ((triple1 triple3) -> rule4) OR ((((triple3) -> rule2)) -> rule8) OR ((((triple6) -> rule1)) -> rule8) OR ((((triple6) -> rule3)) -> rule8))] Charlie is nice.[(triple5)] Charlie is round.[(triple6)] Dave is cold.[(triple7)] Erin is blue.[(triple8)] Erin is cold.[(triple9 OR ((triple10) -> rule2) OR ((triple13) -> rule1) OR ((triple13) -> rule3) OR ((triple12 triple11) -> rule7) OR ((((triple12) -> rule6)) -> rule2) OR ((triple12 ((triple8 triple10) -> rule4)) -> rule7) OR ((triple12 ((triple8 ((triple12) -> rule6)) -> rule4)) -> rule7))] Erin is furry.[(triple10 OR ((triple12) -> rule6))] Erin is green.[(triple11 OR ((triple9) -> rule8) OR ((triple8 triple10) -> rule4) OR ((((triple10) -> rule2)) -> rule8) OR ((((triple13) -> rule1)) -> rule8) OR ((((triple13) -> rule3)) -> rule8) OR ((triple8 ((triple12) -> rule6)) -> rule4) OR ((((((triple12) -> rule6)) -> rule2)) -> rule8))] Erin is red.[(triple12)] Erin is round.[(triple13)] Fiona is blue.[(triple14)] Fiona is furry.[(triple15)] Fiona is round.[(triple16)] @1: Dave is green.[(((triple7) -> rule8))] Fiona is cold.[(((triple15) -> rule2) OR ((triple16) -> rule1) OR ((triple16) -> rule3))] Fiona is green.[(((triple14 triple15) -> rule4) OR ((((triple15) -> rule2)) -> rule8) OR ((((triple16) -> rule1)) -> rule8) OR ((((triple16) -> rule3)) -> rule8))]
Charlie is blue.
("Charlie" "is" "blue" "+")
triple1
Charlie is cold.
("Charlie" "is" "cold" "+")
triple2
((triple3) -> (rule2 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
((triple6) -> (rule1 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
((triple6) -> (rule3 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
triple3
Charlie is green.
("Charlie" "is" "green" "+")
triple4
((triple2) -> (rule8 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
((triple1 triple3) -> (rule4 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
((((triple3) -> (rule2 % int2))) -> (rule8 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
((((triple6) -> (rule1 % int2))) -> (rule8 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
((((triple6) -> (rule3 % int2))) -> (rule8 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
triple5
Charlie is round.
("Charlie" "is" "round" "+")
triple6
Dave is cold.
("Dave" "is" "cold" "+")
triple7
Erin is blue.
("Erin" "is" "blue" "+")
triple8
Erin is cold.
("Erin" "is" "cold" "+")
triple9
((triple10) -> (rule2 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
((triple13) -> (rule1 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
((triple13) -> (rule3 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
((triple12 triple11) -> (rule7 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
((((triple12) -> (rule6 % int2))) -> (rule2 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
((triple12 ((triple8 triple10) -> (rule4 % int2))) -> (rule7 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
((triple12 ((triple8 ((triple12) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is furry.
("Erin" "is" "furry" "+")
int3
Erin is furry.
("Erin" "is" "furry" "+")
triple10
((triple12) -> (rule6 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
triple11
((triple9) -> (rule8 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
((triple8 triple10) -> (rule4 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
((((triple10) -> (rule2 % int2))) -> (rule8 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
((((triple13) -> (rule1 % int2))) -> (rule8 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
((((triple13) -> (rule3 % int2))) -> (rule8 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
((triple8 ((triple12) -> (rule6 % int2))) -> (rule4 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
((((((triple12) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule8 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is furry.
("Erin" "is" "furry" "+")
int3
Erin is red.
("Erin" "is" "red" "+")
triple12
Erin is round.
("Erin" "is" "round" "+")
triple13
Fiona is blue.
("Fiona" "is" "blue" "+")
triple14
Fiona is furry.
("Fiona" "is" "furry" "+")
triple15
Fiona is round.
("Fiona" "is" "round" "+")
triple16
Dave is green.
("Dave" "is" "green" "+")
((triple7) -> (rule8 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
((triple15) -> (rule2 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
((triple16) -> (rule1 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
((triple16) -> (rule3 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
((triple14 triple15) -> (rule4 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
((((triple15) -> (rule2 % int2))) -> (rule8 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
((((triple16) -> (rule1 % int2))) -> (rule8 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
((((triple16) -> (rule3 % int2))) -> (rule8 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2