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