Anne is not smart. Erin is cold. Erin is green. Erin is kind. Erin is nice. Fiona is not green. Harry is cold. Kind things are smart. All white, nice things are smart. All cold things are round. Cold, green things are white. If something is white and not green then it is not cold. All round things are kind.
Anne is not smart.
("Anne" "is" "smart" "-")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Fiona is not green.
("Fiona" "is" "green" "-")
Harry is cold.
("Harry" "is" "cold" "+")
Kind things are smart.
((("something" "is" "kind" "+")) -> ("something" "is" "smart" "+"))
All white, nice things are smart.
((("something" "is" "white" "+") ("something" "is" "nice" "+")) -> ("something" "is" "smart" "+"))
All cold things are round.
((("something" "is" "cold" "+")) -> ("something" "is" "round" "+"))
Cold, green things are white.
((("something" "is" "cold" "+") ("something" "is" "green" "+")) -> ("something" "is" "white" "+"))
If something is white and not green then it is not cold.
((("something" "is" "white" "+") ("something" "is" "green" "~")) -> ("something" "is" "cold" "-"))
All round things are kind.
((("something" "is" "round" "+")) -> ("something" "is" "kind" "+"))
Fiona is not green.
True
1
proof
[(triple6)]
("Fiona" "is" "green" "-")
triple6
Harry is not cold.
False
1
inv-proof
[(triple7)]
("Harry" "is" "cold" "-")
triple7
Erin is smart.
True
2
proof
[(((triple4) -> rule1) OR ((((triple2 triple3) -> rule4) triple5) -> rule2) OR ((((((triple2) -> rule3)) -> rule6)) -> rule1))]
("Erin" "is" "smart" "+")
((triple4) -> (rule1 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
((((triple2 triple3) -> (rule4 % int2)) triple5) -> (rule2 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
((((((triple2) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3
Erin is not smart.
False
2
inv-proof
[(((triple4) -> rule1) OR ((((triple2 triple3) -> rule4) triple5) -> rule2) OR ((((((triple2) -> rule3)) -> rule6)) -> rule1))]
("Erin" "is" "smart" "-")
((triple4) -> (rule1 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
((((triple2 triple3) -> (rule4 % int2)) triple5) -> (rule2 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
((((((triple2) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3
Harry is kind.
True
3
proof
[(((((triple7) -> rule3)) -> rule6))]
("Harry" "is" "kind" "+")
((((triple7) -> (rule3 % int2))) -> (rule6 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is not kind.
False
3
inv-proof
[(((((triple7) -> rule3)) -> rule6))]
("Harry" "is" "kind" "-")
((((triple7) -> (rule3 % int2))) -> (rule6 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is smart.
True
4
proof
[(((((((triple7) -> rule3)) -> rule6)) -> rule1))]
("Harry" "is" "smart" "+")
((((((triple7) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
int3
Harry is not smart.
False
4
inv-proof
[(((((((triple7) -> rule3)) -> rule6)) -> rule1))]
("Harry" "is" "smart" "-")
((((((triple7) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
int3
Harry is not white.
Unknown
inv-rconc
[@1: Harry is white.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Harry" "is" "white" "-")
Fiona is white.
Unknown
rconc
[@1: Fiona is white.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Fiona" "is" "white" "+")
Anne is not kind.
Unknown
inv-rconc
[@2: Anne is kind.[CWA. Example of deepest failure = (rule6 <- rule3 <- FAIL)]]
("Anne" "is" "kind" "-")
Fiona is kind.
Unknown
rconc
[@2: Fiona is kind.[CWA. Example of deepest failure = (rule6 <- rule3 <- FAIL)]]
("Fiona" "is" "kind" "+")
Harry is not green.
Unknown
inv-random
[@0: Harry is green.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "green" "-")
Fiona is cold.
Unknown
random
[@0: Fiona is cold.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "cold" "+")
Fiona is not nice.
Unknown
inv-random
[@0: Fiona is nice.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "nice" "-")
Anne is green.
Unknown
random
[@0: Anne is green.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "green" "+")
@0: Anne is not smart.[(triple1)] Erin is cold.[(triple2)] Erin is green.[(triple3)] Erin is kind.[(triple4 OR ((((triple2) -> rule3)) -> rule6))] Erin is nice.[(triple5)] Fiona is not green.[(triple6)] Harry is cold.[(triple7)] @1: Erin is round.[(((triple2) -> rule3))] Erin is smart.[(((triple4) -> rule1) OR ((((triple2 triple3) -> rule4) triple5) -> rule2) OR ((((((triple2) -> rule3)) -> rule6)) -> rule1))] Erin is white.[(((triple2 triple3) -> rule4))] Harry is round.[(((triple7) -> rule3))] @2: Harry is kind.[(((((triple7) -> rule3)) -> rule6))] @3: Harry is smart.[(((((((triple7) -> rule3)) -> rule6)) -> rule1))]
Anne is not smart.
("Anne" "is" "smart" "-")
triple1
Erin is cold.
("Erin" "is" "cold" "+")
triple2
Erin is green.
("Erin" "is" "green" "+")
triple3
Erin is kind.
("Erin" "is" "kind" "+")
triple4
((((triple2) -> (rule3 % int2))) -> (rule6 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is nice.
("Erin" "is" "nice" "+")
triple5
Fiona is not green.
("Fiona" "is" "green" "-")
triple6
Harry is cold.
("Harry" "is" "cold" "+")
triple7
Erin is round.
("Erin" "is" "round" "+")
((triple2) -> (rule3 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
((triple4) -> (rule1 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
((((triple2 triple3) -> (rule4 % int2)) triple5) -> (rule2 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
((((((triple2) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3
Erin is white.
("Erin" "is" "white" "+")
((triple2 triple3) -> (rule4 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
((triple7) -> (rule3 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
((((triple7) -> (rule3 % int2))) -> (rule6 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
((((((triple7) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
int3