Anne is not furry. Charlie is kind. Charlie is red. Dave is big. Dave is furry. Fiona is cold. Fiona is not furry. Fiona is kind. Fiona is nice. Fiona is red. Fiona is smart. If something is furry and cold then it is nice. Furry, smart things are nice. All smart, kind things are nice. If Charlie is red and Charlie is furry then Charlie is smart. Cold things are red. If something is nice then it is cold. Big things are smart. Cold, red things are kind. If Charlie is not furry then Charlie is cold.
Anne is not furry.
("Anne" "is" "furry" "-")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Fiona is cold.
("Fiona" "is" "cold" "+")
Fiona is not furry.
("Fiona" "is" "furry" "-")
Fiona is kind.
("Fiona" "is" "kind" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
Fiona is red.
("Fiona" "is" "red" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
If something is furry and cold then it is nice.
((("something" "is" "furry" "+") ("something" "is" "cold" "+")) -> ("something" "is" "nice" "+"))
Furry, smart things are nice.
((("something" "is" "furry" "+") ("something" "is" "smart" "+")) -> ("something" "is" "nice" "+"))
All smart, kind things are nice.
((("something" "is" "smart" "+") ("something" "is" "kind" "+")) -> ("something" "is" "nice" "+"))
If Charlie is red and Charlie is furry then Charlie is smart.
((("Charlie" "is" "red" "+") ("Charlie" "is" "furry" "+")) -> ("Charlie" "is" "smart" "+"))
Cold things are red.
((("something" "is" "cold" "+")) -> ("something" "is" "red" "+"))
If something is nice then it is cold.
((("something" "is" "nice" "+")) -> ("something" "is" "cold" "+"))
Big things are smart.
((("something" "is" "big" "+")) -> ("something" "is" "smart" "+"))
Cold, red things are kind.
((("something" "is" "cold" "+") ("something" "is" "red" "+")) -> ("something" "is" "kind" "+"))
If Charlie is not furry then Charlie is cold.
((("Charlie" "is" "furry" "~")) -> ("Charlie" "is" "cold" "+"))
Dave is big.
True
1
proof
[(triple4)]
("Dave" "is" "big" "+")
triple4
Fiona is furry.
False
1
inv-proof
[(triple7)]
("Fiona" "is" "furry" "+")
triple7
Dave is smart.
True
2
proof
[(((triple4) -> rule7))]
("Dave" "is" "smart" "+")
((triple4) -> (rule7 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is not smart.
False
2
inv-proof
[(((triple4) -> rule7))]
("Dave" "is" "smart" "-")
((triple4) -> (rule7 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is nice.
True
4
proof
[(((triple5 ((triple4) -> rule7)) -> rule2))]
("Dave" "is" "nice" "+")
((triple5 ((triple4) -> (rule7 % int2))) -> (rule2 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is not nice.
False
4
inv-proof
[(((triple5 ((triple4) -> rule7)) -> rule2))]
("Dave" "is" "nice" "-")
((triple5 ((triple4) -> (rule7 % int2))) -> (rule2 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is cold.
True
5
proof
[(((((triple5 ((triple4) -> rule7)) -> rule2)) -> rule6))]
("Dave" "is" "cold" "+")
((((triple5 ((triple4) -> (rule7 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
int3
Dave is not cold.
False
5
inv-proof
[(((((triple5 ((triple4) -> rule7)) -> rule2)) -> rule6))]
("Dave" "is" "cold" "-")
((((triple5 ((triple4) -> (rule7 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
int3
Dave is red.
True
6
proof
[(((((((triple5 ((triple4) -> rule7)) -> rule2)) -> rule6)) -> rule5))]
("Dave" "is" "red" "+")
((((((triple5 ((triple4) -> (rule7 % int4))) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
Dave is smart.
("Dave" "is" "smart" "+")
int4
Dave is not red.
False
6
inv-proof
[(((((((triple5 ((triple4) -> rule7)) -> rule2)) -> rule6)) -> rule5))]
("Dave" "is" "red" "-")
((((((triple5 ((triple4) -> (rule7 % int4))) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
Dave is smart.
("Dave" "is" "smart" "+")
int4
Dave is kind.
True
12
proof
[(((((((triple5 ((triple4) -> rule7)) -> rule2)) -> rule6) ((((((triple5 ((triple4) -> rule7)) -> rule2)) -> rule6)) -> rule5)) -> rule8))]
("Dave" "is" "kind" "+")
((((((triple5 ((triple4) -> (rule7 % int5))) -> (rule2 % int4))) -> (rule6 % int3)) ((((((triple5 ((triple4) -> (rule7 % int5))) -> (rule2 % int4))) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is cold.
("Dave" "is" "cold" "+")
int3
Dave is nice.
("Dave" "is" "nice" "+")
int4
Dave is smart.
("Dave" "is" "smart" "+")
int5
Dave is not kind.
False
12
inv-proof
[(((((((triple5 ((triple4) -> rule7)) -> rule2)) -> rule6) ((((((triple5 ((triple4) -> rule7)) -> rule2)) -> rule6)) -> rule5)) -> rule8))]
("Dave" "is" "kind" "-")
((((((triple5 ((triple4) -> (rule7 % int5))) -> (rule2 % int4))) -> (rule6 % int3)) ((((((triple5 ((triple4) -> (rule7 % int5))) -> (rule2 % int4))) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is cold.
("Dave" "is" "cold" "+")
int3
Dave is nice.
("Dave" "is" "nice" "+")
int4
Dave is smart.
("Dave" "is" "smart" "+")
int5
Anne is not red.
Unknown
inv-rconc
[@4: Anne is red.[CWA. Example of deepest failure = (rule5 <- rule6 <- rule3 <- rule7 <- FAIL)]]
("Anne" "is" "red" "-")
Anne is cold.
Unknown
rconc
[@3: Anne is cold.[CWA. Example of deepest failure = (rule6 <- rule3 <- rule7 <- FAIL)]]
("Anne" "is" "cold" "+")
Charlie is not smart.
Unknown
inv-rconc
[@1: Charlie is smart.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Charlie" "is" "smart" "-")
Anne is nice.
Unknown
rconc
[@2: Anne is nice.[CWA. Example of deepest failure = (rule3 <- rule7 <- FAIL)]]
("Anne" "is" "nice" "+")
Anne is not smart.
Unknown
inv-rconc
[@1: Anne is smart.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Anne" "is" "smart" "-")
Charlie is cold.
Unknown
rconc
[@3: Charlie is cold.[CWA. Example of deepest failure = (rule6 <- rule3 <- rule4 <- FAIL)]]
("Charlie" "is" "cold" "+")
Charlie is not furry.
Unknown
inv-random
[@0: Charlie is furry.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "furry" "-")
Anne is big.
Unknown
random
[@0: Anne is big.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "big" "+")
Fiona is not big.
Unknown
inv-random
[@0: Fiona is big.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "big" "-")
Charlie is big.
Unknown
random
[@0: Charlie is big.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "big" "+")
@0: Anne is not furry.[(triple1)] Charlie is kind.[(triple2)] Charlie is red.[(triple3)] Dave is big.[(triple4)] Dave is furry.[(triple5)] Fiona is cold.[(triple6 OR ((triple9) -> rule6) OR ((((triple11 triple8) -> rule3)) -> rule6))] Fiona is kind.[(triple8 OR ((triple6 triple10) -> rule8) OR ((triple6 ((triple6) -> rule5)) -> rule8) OR ((((triple9) -> rule6) triple10) -> rule8) OR ((((triple9) -> rule6) ((triple6) -> rule5)) -> rule8) OR ((triple6 ((((triple9) -> rule6)) -> rule5)) -> rule8) OR ((((triple9) -> rule6) ((((triple9) -> rule6)) -> rule5)) -> rule8))] Fiona is nice.[(triple9 OR ((triple11 triple8) -> rule3) OR ((triple11 ((triple6 triple10) -> rule8)) -> rule3) OR ((triple11 ((triple6 ((triple6) -> rule5)) -> rule8)) -> rule3))] Fiona is not furry.[(triple7)] Fiona is red.[(triple10 OR ((triple6) -> rule5) OR ((((triple9) -> rule6)) -> rule5) OR ((((((triple11 triple8) -> rule3)) -> rule6)) -> rule5))] Fiona is smart.[(triple11)] @1: Dave is smart.[(((triple4) -> rule7))] @2: Dave is nice.[(((triple5 ((triple4) -> rule7)) -> rule2))] @3: Dave is cold.[(((((triple5 ((triple4) -> rule7)) -> rule2)) -> rule6))] @4: Dave is red.[(((((((triple5 ((triple4) -> rule7)) -> rule2)) -> rule6)) -> rule5))] @5: Dave is kind.[(((((((triple5 ((triple4) -> rule7)) -> rule2)) -> rule6) ((((((triple5 ((triple4) -> rule7)) -> rule2)) -> rule6)) -> rule5)) -> rule8))]
Anne is not furry.
("Anne" "is" "furry" "-")
triple1
Charlie is kind.
("Charlie" "is" "kind" "+")
triple2
Charlie is red.
("Charlie" "is" "red" "+")
triple3
Dave is big.
("Dave" "is" "big" "+")
triple4
Dave is furry.
("Dave" "is" "furry" "+")
triple5
Fiona is cold.
("Fiona" "is" "cold" "+")
triple6
((triple9) -> (rule6 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
((((triple11 triple8) -> (rule3 % int2))) -> (rule6 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
Fiona is kind.
("Fiona" "is" "kind" "+")
triple8
((triple6 triple10) -> (rule8 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
((triple6 ((triple6) -> (rule5 % int2))) -> (rule8 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
((((triple9) -> (rule6 % int2)) triple10) -> (rule8 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
((((triple9) -> (rule6 % int3)) ((triple6) -> (rule5 % int2))) -> (rule8 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Fiona is cold.
("Fiona" "is" "cold" "+")
int3
((triple6 ((((triple9) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Fiona is cold.
("Fiona" "is" "cold" "+")
int3
((((triple9) -> (rule6 % int3)) ((((triple9) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Fiona is cold.
("Fiona" "is" "cold" "+")
int3
Fiona is nice.
("Fiona" "is" "nice" "+")
triple9
((triple11 triple8) -> (rule3 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
((triple11 ((triple6 triple10) -> (rule8 % int2))) -> (rule3 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
((triple11 ((triple6 ((triple6) -> (rule5 % int3))) -> (rule8 % int2))) -> (rule3 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
Fiona is red.
("Fiona" "is" "red" "+")
int3
Fiona is not furry.
("Fiona" "is" "furry" "-")
triple7
Fiona is red.
("Fiona" "is" "red" "+")
triple10
((triple6) -> (rule5 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
((((triple9) -> (rule6 % int2))) -> (rule5 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
((((((triple11 triple8) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Fiona is nice.
("Fiona" "is" "nice" "+")
int3
Fiona is smart.
("Fiona" "is" "smart" "+")
triple11
Dave is smart.
("Dave" "is" "smart" "+")
((triple4) -> (rule7 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
((triple5 ((triple4) -> (rule7 % int2))) -> (rule2 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is cold.
("Dave" "is" "cold" "+")
((((triple5 ((triple4) -> (rule7 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
int3
Dave is red.
("Dave" "is" "red" "+")
((((((triple5 ((triple4) -> (rule7 % int4))) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
Dave is smart.
("Dave" "is" "smart" "+")
int4
Dave is kind.
("Dave" "is" "kind" "+")
((((((triple5 ((triple4) -> (rule7 % int5))) -> (rule2 % int4))) -> (rule6 % int3)) ((((((triple5 ((triple4) -> (rule7 % int5))) -> (rule2 % int4))) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is cold.
("Dave" "is" "cold" "+")
int3
Dave is nice.
("Dave" "is" "nice" "+")
int4
Dave is smart.
("Dave" "is" "smart" "+")
int5