Charlie is blue. Erin is blue. Erin is kind. Erin is round. Erin is young. Harry is blue. Harry is furry. Cold things are big. Kind, blue things are young. All kind, furry things are young. All young, cold things are round. If something is young then it is cold. All round things are kind. If Harry is big then Harry is blue. All round, big things are blue.
Charlie is blue.
("Charlie" "is" "blue" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is round.
("Erin" "is" "round" "+")
Erin is young.
("Erin" "is" "young" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Cold things are big.
((("something" "is" "cold" "+")) -> ("something" "is" "big" "+"))
Kind, blue things are young.
((("something" "is" "kind" "+") ("something" "is" "blue" "+")) -> ("something" "is" "young" "+"))
All kind, furry things are young.
((("something" "is" "kind" "+") ("something" "is" "furry" "+")) -> ("something" "is" "young" "+"))
All young, cold things are round.
((("something" "is" "young" "+") ("something" "is" "cold" "+")) -> ("something" "is" "round" "+"))
If something is young then it is cold.
((("something" "is" "young" "+")) -> ("something" "is" "cold" "+"))
All round things are kind.
((("something" "is" "round" "+")) -> ("something" "is" "kind" "+"))
If Harry is big then Harry is blue.
((("Harry" "is" "big" "+")) -> ("Harry" "is" "blue" "+"))
All round, big things are blue.
((("something" "is" "round" "+") ("something" "is" "big" "+")) -> ("something" "is" "blue" "+"))
Erin is young.
True
1
proof
[(triple5 OR ((triple3 triple2) -> rule2) OR ((((triple4) -> rule6) triple2) -> rule2))]
("Erin" "is" "young" "+")
triple5
((triple3 triple2) -> (rule2 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
((((triple4) -> (rule6 % int2)) triple2) -> (rule2 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is not kind.
False
1
inv-proof
[(triple3 OR ((triple4) -> rule6) OR ((((triple5 ((triple5) -> rule5)) -> rule4)) -> rule6))]
("Erin" "is" "kind" "-")
triple3
((triple4) -> (rule6 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
((((triple5 ((triple5) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3
Charlie is not big.
Unknown
inv-rconc
[@5: Charlie is big.[CWA. Example of deepest failure = (rule1 <- rule5 <- rule2 <- rule6 <- rule4 <- FAIL)]]
("Charlie" "is" "big" "-")
Erin is furry.
Unknown
random
[@0: Erin is furry.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "furry" "+")
@0: Charlie is blue.[(triple1)] Erin is blue.[(triple2 OR ((triple4 ((((triple5) -> rule5)) -> rule1)) -> rule8) OR ((((triple5 ((triple5) -> rule5)) -> rule4) ((((triple5) -> rule5)) -> rule1)) -> rule8))] Erin is kind.[(triple3 OR ((triple4) -> rule6) OR ((((triple5 ((triple5) -> rule5)) -> rule4)) -> rule6))] Erin is round.[(triple4 OR ((triple5 ((triple5) -> rule5)) -> rule4) OR ((((triple3 triple2) -> rule2) ((triple5) -> rule5)) -> rule4) OR ((triple5 ((((triple3 triple2) -> rule2)) -> rule5)) -> rule4) OR ((((triple3 triple2) -> rule2) ((((triple3 triple2) -> rule2)) -> rule5)) -> rule4))] Erin is young.[(triple5 OR ((triple3 triple2) -> rule2) OR ((((triple4) -> rule6) triple2) -> rule2))] Harry is blue.[(triple6)] Harry is furry.[(triple7)] @1: Erin is cold.[(((triple5) -> rule5) OR ((((triple3 triple2) -> rule2)) -> rule5) OR ((((((triple4) -> rule6) triple2) -> rule2)) -> rule5))] @2: Erin is big.[(((((triple5) -> rule5)) -> rule1) OR ((((((triple3 triple2) -> rule2)) -> rule5)) -> rule1) OR ((((((((triple4) -> rule6) triple2) -> rule2)) -> rule5)) -> rule1))]
Charlie is blue.
("Charlie" "is" "blue" "+")
triple1
Erin is blue.
("Erin" "is" "blue" "+")
triple2
((triple4 ((((triple5) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule8 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3
((((triple5 ((triple5) -> (rule5 % int4))) -> (rule4 % int3)) ((((triple5) -> (rule5 % int4))) -> (rule1 % int2))) -> (rule8 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3
Erin is cold.
("Erin" "is" "cold" "+")
int4
Erin is kind.
("Erin" "is" "kind" "+")
triple3
((triple4) -> (rule6 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
((((triple5 ((triple5) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3
Erin is round.
("Erin" "is" "round" "+")
triple4
((triple5 ((triple5) -> (rule5 % int2))) -> (rule4 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
((((triple3 triple2) -> (rule2 % int3)) ((triple5) -> (rule5 % int2))) -> (rule4 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
int3
((triple5 ((((triple3 triple2) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
int3
((((triple3 triple2) -> (rule2 % int3)) ((((triple3 triple2) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
int3
Erin is young.
("Erin" "is" "young" "+")
triple5
((triple3 triple2) -> (rule2 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
((((triple4) -> (rule6 % int2)) triple2) -> (rule2 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
triple6
Harry is furry.
("Harry" "is" "furry" "+")
triple7
Erin is cold.
("Erin" "is" "cold" "+")
((triple5) -> (rule5 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
((((triple3 triple2) -> (rule2 % int2))) -> (rule5 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
((((((triple4) -> (rule6 % int3)) triple2) -> (rule2 % int2))) -> (rule5 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
Erin is big.
("Erin" "is" "big" "+")
((((triple5) -> (rule5 % int2))) -> (rule1 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
((((((triple3 triple2) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
int3
((((((((triple4) -> (rule6 % int4)) triple2) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
int3
Erin is kind.
("Erin" "is" "kind" "+")
int4